%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYO932^9 : TPTP v9.3.1. Released v3.7.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 : n001.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:46:15 AM UTC 2026
% Result : Theorem 70.85s 18.13s
% Output : Refutation 71.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO932^9 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.12/0.22 % Computer : n001.cluster.edu
% 0.12/0.22 % Model : x86_64 x86_64
% 0.12/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.22 % Memory : 8046.5625MB
% 0.12/0.22 % OS : Linux 6.8.0-71-generic
% 0.12/0.22 % CPULimit : 300
% 0.12/0.22 % WCLimit : 300
% 0.12/0.22 % DateTime : Tue Sep 29 17:34:21 UTC 2026
% 0.12/0.22 % CPUTime :
% 0.12/0.22 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.92/0.80 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.57/1.10 % [INFO] Parsing done (300ms).
% 1.57/1.11 % [INFO] Running in sequential loop mode.
% 2.47/1.52 % [INFO] eprover registered as external prover.
% 2.47/1.53 % [INFO] Scanning for conjecture ...
% 2.68/1.67 % [INFO] Found a conjecture (or negated_conjecture) and 5 axioms. Running axiom selection ...
% 2.89/1.71 % [INFO] Axiom selection finished. Selected 5 axioms (removed 0 axioms).
% 2.89/1.72 % [INFO] Problem is higher-order (TPTP THF).
% 2.89/1.72 % [INFO] Type checking passed.
% 2.89/1.73 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 84.52/18.12 % External prover 'e' found a proof!
% 84.52/18.12 % [INFO] Killing All external provers ...
% 84.52/18.13 % Time passed: 17759ms (effective reasoning time: 17006ms)
% 84.52/18.13 % 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)>
% 70.85/18.13 % Axioms used in derivation (5): trans_axiom_i, trans_axiom_r, refl_axiom_r, ax_i_r_commute, refl_axiom_i
% 70.85/18.13 % No. of inferences in proof: 383
% 70.85/18.13 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 17759 ms resp. 17006 ms w/o parsing
% 71.58/18.30 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 71.58/18.30 thf(individuals_type, type, individuals: $tType).
% 71.58/18.30 thf(prop_a_decl, type, prop_a: ($i > $o)).
% 71.58/18.30 thf(prop_b_decl, type, prop_b: ($i > $o)).
% 71.58/18.30 thf(prop_c_decl, type, prop_c: ($i > $o)).
% 71.58/18.30 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 71.58/18.30 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 71.58/18.30 thf(mimpl_decl, type, mimpl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 71.58/18.30 thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 71.58/18.30 thf(mall_decl, type, mall: ((individuals > ($i > $o)) > ($i > $o))).
% 71.58/18.30 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 71.58/18.30 thf(reli_decl, type, reli: ($i > ($i > $o))).
% 71.58/18.30 thf(relr_decl, type, relr: ($i > ($i > $o))).
% 71.58/18.30 thf(cs4_atom_decl, type, cs4_atom: (($i > $o) > ($i > $o))).
% 71.58/18.30 thf(cs4_impl_decl, type, cs4_impl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 71.58/18.30 thf(cs4_all_decl, type, cs4_all: ((individuals > ($i > $o)) > ($i > $o))).
% 71.58/18.30 thf(cs4_box_decl, type, cs4_box: (($i > $o) > ($i > $o))).
% 71.58/18.30 thf(cs4_valid_decl, type, cs4_valid: (($i > $o) > $o)).
% 71.58/18.30 thf(sk1_decl, type, sk1: (individuals > ($i > $o))).
% 71.58/18.30 thf(sk2_decl, type, sk2: $i).
% 71.58/18.30 thf(sk3_decl, type, sk3: $i).
% 71.58/18.30 thf(sk4_decl, type, sk4: $i).
% 71.58/18.30 thf(sk5_decl, type, sk5: individuals).
% 71.58/18.30 thf(sk6_decl, type, sk6: $i).
% 71.58/18.30 thf(sk7_decl, type, sk7: $i).
% 71.58/18.30 thf(sk8_decl, type, sk8: $i).
% 71.58/18.30 thf(sk9_decl, type, sk9: ($i > (($i > $o) > $i))).
% 71.58/18.30 thf(sk10_decl, type, sk10: ($i > (($i > $o) > $i))).
% 71.58/18.30 thf(sk11_decl, type, sk11: ($i > (($i > $o) > $i))).
% 71.58/18.30 thf(sk12_decl, type, sk12: ($i > (($i > $o) > $i))).
% 71.58/18.30 thf(sk13_decl, type, sk13: ($i > (($i > $o) > $i))).
% 71.58/18.30 thf(sk14_decl, type, sk14: ($i > (($i > $o) > $i))).
% 71.58/18.30 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 71.58/18.30 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 71.58/18.30 thf(mimpl_def, definition, mimpl = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 71.58/18.30 thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: ((A @ C @ D) => (B @ D))) ).
% 71.58/18.30 thf(mall_def, definition, mall = (^ [A:(individuals > ($i > $o)),B:$i]: ! [C:individuals]: (A @ C @ B)) ).
% 71.58/18.30 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 71.58/18.30 thf(cs4_atom_def, definition, cs4_atom = (mbox @ reli) ).
% 71.58/18.30 thf(cs4_impl_def, definition, cs4_impl = (^ [A:($i > $o),B:($i > $o)]: (mbox @ reli @ (mimpl @ A @ B))) ).
% 71.58/18.30 thf(cs4_all_def, definition, cs4_all = (^ [A:(individuals > ($i > $o))]: (mbox @ reli @ (mall @ A))) ).
% 71.58/18.30 thf(cs4_box_def, definition, cs4_box = (^ [A:($i > $o)]: (mbox @ reli @ (mbox @ relr @ A))) ).
% 71.58/18.30 thf(cs4_valid_def, definition, cs4_valid = (mvalid) ).
% 71.58/18.30 thf(sk1_def, definition, sk1 = (@+ [A:(individuals > ($i > $o))]: ~ (! [B:$i,C:$i]: ((reli @ B @ C) => (~ (! [D:$i]: ((reli @ C @ D) => (! [E:$i]: ((relr @ D @ E) => (! [F:$i]: ((reli @ E @ F) => (! [G:individuals,H:$i]: ((reli @ F @ H) => (A @ G @ H))))))))) | ! [D:$i]: ((reli @ C @ D) => (! [E:individuals,F:$i]: ((reli @ D @ F) => (! [G:$i]: ((relr @ F @ G) => (! [H:$i]: ((reli @ G @ H) => (A @ E @ H)))))))))))) ).
% 71.58/18.30 thf(sk2_def, definition, sk2 = (@+ [A:$i]: ~ (! [B:$i]: ((reli @ A @ B) => (~ (! [C:$i]: ((reli @ B @ C) => (! [D:$i]: ((relr @ C @ D) => (! [E:$i]: ((reli @ D @ E) => (! [F:individuals,G:$i]: ((reli @ E @ G) => (sk1 @ F @ G))))))))) | ! [C:$i]: ((reli @ B @ C) => (! [D:individuals,E:$i]: ((reli @ C @ E) => (! [F:$i]: ((relr @ E @ F) => (! [G:$i]: ((reli @ F @ G) => (sk1 @ D @ G)))))))))))) ).
% 71.58/18.30 thf(sk3_def, definition, sk3 = (@+ [A:$i]: ~ ((reli @ sk2 @ A) => (~ (! [B:$i]: ((reli @ A @ B) => (! [C:$i]: ((relr @ B @ C) => (! [D:$i]: ((reli @ C @ D) => (! [E:individuals,F:$i]: ((reli @ D @ F) => (sk1 @ E @ F))))))))) | ! [B:$i]: ((reli @ A @ B) => (! [C:individuals,D:$i]: ((reli @ B @ D) => (! [E:$i]: ((relr @ D @ E) => (! [F:$i]: ((reli @ E @ F) => (sk1 @ C @ F))))))))))) ).
% 71.58/18.30 thf(sk4_def, definition, sk4 = (@+ [A:$i]: ~ ((reli @ sk3 @ A) => (! [B:individuals,C:$i]: ((reli @ A @ C) => (! [D:$i]: ((relr @ C @ D) => (! [E:$i]: ((reli @ D @ E) => (sk1 @ B @ E))))))))) ).
% 71.58/18.30 thf(sk5_def, definition, sk5 = (@+ [A:individuals]: ~ (! [B:$i]: ((reli @ sk4 @ B) => (! [C:$i]: ((relr @ B @ C) => (! [D:$i]: ((reli @ C @ D) => (sk1 @ A @ D)))))))) ).
% 71.58/18.30 thf(sk6_def, definition, sk6 = (@+ [A:$i]: ~ ((reli @ sk4 @ A) => (! [B:$i]: ((relr @ A @ B) => (! [C:$i]: ((reli @ B @ C) => (sk1 @ sk5 @ C))))))) ).
% 71.58/18.30 thf(sk7_def, definition, sk7 = (@+ [A:$i]: ~ ((relr @ sk6 @ A) => (! [B:$i]: ((reli @ A @ B) => (sk1 @ sk5 @ B))))) ).
% 71.58/18.30 thf(sk8_def, definition, sk8 = (@+ [A:$i]: ~ ((reli @ sk7 @ A) => (sk1 @ sk5 @ A))) ).
% 71.58/18.30 thf(sk9_def, definition, sk9 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((reli @ A @ C) => (B @ C)))) ).
% 71.58/18.30 thf(sk10_def, definition, sk10 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((relr @ A @ C) => (B @ C)))) ).
% 71.58/18.30 thf(sk11_def, definition, sk11 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((reli @ A @ C) => (B @ C)))) ).
% 71.58/18.30 thf(sk12_def, definition, sk12 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((relr @ A @ C) => (B @ C)))) ).
% 71.58/18.30 thf(sk13_def, definition, sk13 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((reli @ A @ C) => (! [D:$i]: ((relr @ C @ D) => (B @ D)))))) ).
% 71.58/18.30 thf(sk14_def, definition, sk14 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((relr @ (sk13 @ A @ B) @ C) => (B @ C)))) ).
% 71.58/18.30 thf(4,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ relr @ A) @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',refl_axiom_r)).
% 71.58/18.30 thf(23,plain,((! [A:($i > $o),B:$i]: (~ (! [C:$i]: ((relr @ B @ C) => (A @ C))) | (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 71.58/18.30 thf(24,plain,(! [B:$i,A:($i > $o)] : ((((relr @ B @ (sk10 @ B @ (A))) | (A @ B)) & (~ (A @ (sk10 @ B @ (A))) | (A @ B))))),inference(cnf,[status(esa)],[23])).
% 71.58/18.30 thf(25,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk10 @ B @ (A))) | (A @ B))),inference(cnfConj,[status(thm)],[24])).
% 71.58/18.30 thf(1,conjecture,((! [A:(individuals > ($i > $o))]: (cs4_valid @ (cs4_impl @ (cs4_box @ (cs4_all @ (^ [B:individuals]: (cs4_atom @ (A @ B))))) @ (cs4_all @ (^ [B:individuals]: (cs4_box @ (cs4_atom @ (A @ B))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cs4_cbarcan)).
% 71.58/18.30 thf(2,negated_conjecture,((~ (! [A:(individuals > ($i > $o))]: (cs4_valid @ (cs4_impl @ (cs4_box @ (cs4_all @ (^ [B:individuals]: (cs4_atom @ (A @ B))))) @ (cs4_all @ (^ [B:individuals]: (cs4_box @ (cs4_atom @ (A @ B)))))))))),inference(neg_conjecture,[status(cth)],[1])).
% 71.58/18.30 thf(8,plain,((~ (! [A:(individuals > ($i > $o)),B:$i,C:$i]: ((reli @ B @ C) => (~ (! [D:$i]: ((reli @ C @ D) => (! [E:$i]: ((relr @ D @ E) => (! [F:$i]: ((reli @ E @ F) => (! [G:individuals,H:$i]: ((reli @ F @ H) => (A @ G @ H))))))))) | ! [D:$i]: ((reli @ C @ D) => (! [E:individuals,F:$i]: ((reli @ D @ F) => (! [G:$i]: ((relr @ F @ G) => (! [H:$i]: ((reli @ G @ H) => (A @ E @ H))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 71.58/18.30 thf(9,plain,(! [E:$i,D:individuals,C:$i,B:$i,A:$i] : (((reli @ sk2 @ sk3) & (~ (reli @ sk3 @ A) | ~ (relr @ A @ B) | ~ (reli @ B @ C) | ~ (reli @ C @ E) | (sk1 @ D @ E)) & (reli @ sk3 @ sk4) & (reli @ sk4 @ sk6) & (relr @ sk6 @ sk7) & (reli @ sk7 @ sk8) & ~ (sk1 @ sk5 @ sk8)))),inference(cnf,[status(esa)],[8])).
% 71.58/18.30 thf(15,plain,((reli @ sk3 @ sk4)),inference(cnfConj,[status(thm)],[9])).
% 71.58/18.30 thf(14,plain,((reli @ sk7 @ sk8)),inference(cnfConj,[status(thm)],[9])).
% 71.58/18.30 thf(10,plain,(! [E:$i,D:individuals,C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (~ (reli @ C @ E)) | (sk1 @ D @ E))),inference(cnfConj,[status(thm)],[9])).
% 71.58/18.30 thf(13,plain,((~ (sk1 @ sk5 @ sk8))),inference(cnfConj,[status(thm)],[9])).
% 71.58/18.30 thf(56,plain,(! [E:$i,D:individuals,C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (~ (reli @ C @ E)) | ~ (($true)) | ((sk1 @ D @ E) != (sk1 @ sk5 @ sk8)))),inference(paramod_ordered,[status(thm)],[10,13])).
% 71.58/18.30 thf(57,plain,(! [E:$i,D:individuals,C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (~ (reli @ C @ E)) | ((sk1 @ D @ E) != (sk1 @ sk5 @ sk8)))),inference(simp,[status(thm)],[56])).
% 71.58/18.30 thf(58,plain,(! [C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (~ (reli @ C @ sk8)))),inference(pattern_uni,[status(thm)],[57:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(sk5)),bind(E, $thf(sk8))]])).
% 71.58/18.30 thf(90,plain,(! [C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | ~ (($true)) | (~ (reli @ C @ sk8)) | ((reli @ sk7 @ sk8) != (reli @ B @ C)))),inference(paramod_ordered,[status(thm)],[14,58])).
% 71.58/18.30 thf(91,plain,(! [C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ C @ sk8)) | ((reli @ sk7 @ sk8) != (reli @ B @ C)))),inference(simp,[status(thm)],[90])).
% 71.58/18.30 thf(92,plain,(! [A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ sk7)) | (~ (reli @ sk8 @ sk8)))),inference(pattern_uni,[status(thm)],[91:[bind(A, $thf(A)),bind(B, $thf(sk7)),bind(C, $thf(sk8))]])).
% 71.58/18.30 thf(182,plain,(! [A:$i] : (~ (($true)) | (~ (relr @ A @ sk7)) | (~ (reli @ sk8 @ sk8)) | ((reli @ sk3 @ sk4) != (reli @ sk3 @ A)))),inference(paramod_ordered,[status(thm)],[15,92])).
% 71.58/18.30 thf(183,plain,(! [A:$i] : ((~ (relr @ A @ sk7)) | (~ (reli @ sk8 @ sk8)) | ((reli @ sk3 @ sk4) != (reli @ sk3 @ A)))),inference(simp,[status(thm)],[182])).
% 71.58/18.30 thf(184,plain,((~ (relr @ sk4 @ sk7)) | (~ (reli @ sk8 @ sk8))),inference(pattern_uni,[status(thm)],[183:[bind(A, $thf(sk4))]])).
% 71.58/18.30 thf(990,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk10 @ B @ (A))) | (~ (relr @ sk4 @ sk7)) | ~ (($true)) | ((A @ B) != (reli @ sk8 @ sk8)))),inference(paramod_ordered,[status(thm)],[25,184])).
% 71.58/18.30 thf(991,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk10 @ B @ (A))) | (~ (relr @ sk4 @ sk7)) | ((A @ B) != (reli @ sk8 @ sk8)))),inference(simp,[status(thm)],[990])).
% 71.58/18.30 thf(1086,plain,((relr @ sk8 @ (sk10 @ sk8 @ (^ [A:$i]: (reli @ A @ A)))) | (~ (relr @ sk4 @ sk7))),inference(pre_uni,[status(thm)],[991:[bind(A, $thf(^ [C:$i]: (reli @ C @ C))),bind(B, $thf(sk8))]])).
% 71.58/18.30 thf(1028,plain,(! [A:$i] : ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) | ($false))),inference(prim_subst,[status(thm)],[25:[bind(A, $thf(^ [C:$i]: (($false))))]])).
% 71.58/18.30 thf(1105,plain,(! [A:$i] : ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))))),inference(simp,[status(thm)],[1028])).
% 71.58/18.30 thf(12,plain,((reli @ sk4 @ sk6)),inference(cnfConj,[status(thm)],[9])).
% 71.58/18.30 thf(1186,plain,(! [A:$i] : (~ (($true)) | (~ (reli @ sk8 @ sk8)) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ sk4 @ sk7)))),inference(paramod_ordered,[status(thm)],[1105,184])).
% 71.58/18.30 thf(1187,plain,(! [A:$i] : ((~ (reli @ sk8 @ sk8)) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ sk4 @ sk7)))),inference(simp,[status(thm)],[1186])).
% 71.58/18.30 thf(1198,plain,(! [A:$i] : ((~ (reli @ sk8 @ sk8)) | (A != sk4) | ((sk10 @ A @ (^ [B:$i]: (($false)))) != sk7))),inference(simp,[status(thm)],[1187])).
% 71.58/18.30 thf(1207,plain,((~ (reli @ sk8 @ sk8)) | ((sk10 @ sk4 @ (^ [A:$i]: (($false)))) != sk7)),inference(simp,[status(thm)],[1198])).
% 71.58/18.30 thf(2567,plain,(~ (($true)) | ((sk10 @ sk4 @ (^ [A:$i]: (($false)))) != sk7) | ((reli @ sk8 @ sk8) != (reli @ sk4 @ sk6))),inference(paramod_ordered,[status(thm)],[12,1207])).
% 71.58/18.30 thf(2568,plain,(((sk10 @ sk4 @ (^ [A:$i]: (($false)))) != sk7) | ((reli @ sk8 @ sk8) != (reli @ sk4 @ sk6))),inference(simp,[status(thm)],[2567])).
% 71.58/18.30 thf(2595,plain,(((sk10 @ sk4 @ (^ [A:$i]: (($false)))) != sk7) | (sk8 != sk4) | (sk8 != sk6)),inference(simp,[status(thm)],[2568])).
% 71.58/18.30 thf(3,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ reli @ A) @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',refl_axiom_i)).
% 71.58/18.30 thf(17,plain,((! [A:($i > $o),B:$i]: (~ (! [C:$i]: ((reli @ B @ C) => (A @ C))) | (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 71.58/18.30 thf(18,plain,(! [B:$i,A:($i > $o)] : ((((reli @ B @ (sk9 @ B @ (A))) | (A @ B)) & (~ (A @ (sk9 @ B @ (A))) | (A @ B))))),inference(cnf,[status(esa)],[17])).
% 71.58/18.30 thf(19,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | (A @ B))),inference(cnfConj,[status(thm)],[18])).
% 71.58/18.30 thf(693,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | (~ (relr @ sk4 @ sk7)) | ~ (($true)) | ((A @ B) != (reli @ sk8 @ sk8)))),inference(paramod_ordered,[status(thm)],[19,184])).
% 71.58/18.30 thf(694,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | (~ (relr @ sk4 @ sk7)) | ((A @ B) != (reli @ sk8 @ sk8)))),inference(simp,[status(thm)],[693])).
% 71.58/18.30 thf(705,plain,((reli @ sk8 @ (sk9 @ sk8 @ (^ [A:$i]: (reli @ A @ A)))) | (~ (relr @ sk4 @ sk7))),inference(pre_uni,[status(thm)],[694:[bind(A, $thf(^ [C:$i]: (reli @ C @ C))),bind(B, $thf(sk8))]])).
% 71.58/18.30 thf(10578,plain,((~ (relr @ sk4 @ sk7)) | (~ (relr @ sk4 @ sk7)) | ~ (($true)) | ((reli @ sk8 @ (sk9 @ sk8 @ (^ [A:$i]: (reli @ A @ A)))) != (reli @ sk8 @ sk8))),inference(paramod_ordered,[status(thm)],[705,184])).
% 71.58/18.30 thf(10579,plain,((~ (relr @ sk4 @ sk7)) | ((reli @ sk8 @ (sk9 @ sk8 @ (^ [A:$i]: (reli @ A @ A)))) != (reli @ sk8 @ sk8))),inference(simp,[status(thm)],[10578])).
% 71.58/18.30 thf(10691,plain,((~ (relr @ sk4 @ sk7)) | (sk8 != sk8) | ((sk9 @ sk8 @ (^ [A:$i]: (reli @ A @ A))) != sk8)),inference(simp,[status(thm)],[10579])).
% 71.58/18.30 thf(10753,plain,((~ (relr @ sk4 @ sk7)) | ((sk9 @ sk8 @ (^ [A:$i]: (reli @ A @ A))) != sk8)),inference(simp,[status(thm)],[10691])).
% 71.58/18.30 thf(107,plain,(! [C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | ((reli @ C @ sk8) != (reli @ sk3 @ A)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[58])).
% 71.58/18.30 thf(113,plain,(! [A:$i] : ((~ (reli @ sk3 @ sk8)) | (~ (relr @ sk8 @ A)) | (~ (reli @ A @ sk3)))),inference(pattern_uni,[status(thm)],[107:[bind(A, $thf(sk8)),bind(B, $thf(B)),bind(C, $thf(sk3))]])).
% 71.58/18.30 thf(115,plain,(! [A:$i] : ((~ (reli @ sk3 @ sk8)) | (~ (relr @ sk8 @ A)) | (~ (reli @ A @ sk3)))),inference(simp,[status(thm)],[113])).
% 71.58/18.30 thf(108,plain,(! [C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | ((reli @ C @ sk8) != (reli @ B @ C)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[58])).
% 71.58/18.30 thf(112,plain,(! [A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ sk8)) | (~ (reli @ sk8 @ sk8)))),inference(pattern_uni,[status(thm)],[108:[bind(A, $thf(A)),bind(B, $thf(sk8)),bind(C, $thf(sk8))]])).
% 71.58/18.30 thf(30498,plain,(! [A:$i] : (~ (($true)) | (~ (relr @ A @ sk8)) | (~ (reli @ sk8 @ sk8)) | ((reli @ sk3 @ sk4) != (reli @ sk3 @ A)))),inference(paramod_ordered,[status(thm)],[15,112])).
% 71.58/18.30 thf(30499,plain,(! [A:$i] : ((~ (relr @ A @ sk8)) | (~ (reli @ sk8 @ sk8)) | ((reli @ sk3 @ sk4) != (reli @ sk3 @ A)))),inference(simp,[status(thm)],[30498])).
% 71.58/18.30 thf(30500,plain,((~ (relr @ sk4 @ sk8)) | (~ (reli @ sk8 @ sk8))),inference(pattern_uni,[status(thm)],[30499:[bind(A, $thf(sk4))]])).
% 71.58/18.30 thf(30794,plain,((~ (relr @ sk4 @ sk8)) | ~ (($true)) | ((reli @ sk8 @ sk8) != (reli @ sk7 @ sk8))),inference(paramod_ordered,[status(thm)],[14,30500])).
% 71.58/18.30 thf(30795,plain,((~ (relr @ sk4 @ sk8)) | ((reli @ sk8 @ sk8) != (reli @ sk7 @ sk8))),inference(simp,[status(thm)],[30794])).
% 71.58/18.30 thf(30944,plain,((~ (relr @ sk4 @ sk8)) | (sk8 != sk7) | (sk8 != sk8)),inference(simp,[status(thm)],[30795])).
% 71.58/18.30 thf(31084,plain,((~ (relr @ sk4 @ sk8)) | (sk8 != sk7)),inference(simp,[status(thm)],[30944])).
% 71.58/18.30 thf(254,plain,(! [A:$i] : ((reli @ A @ (sk9 @ A @ (^ [B:$i]: (($false))))) | ($false))),inference(prim_subst,[status(thm)],[19:[bind(A, $thf(^ [C:$i]: (($false))))]])).
% 71.58/18.30 thf(319,plain,(! [A:$i] : ((reli @ A @ (sk9 @ A @ (^ [B:$i]: (($false))))))),inference(simp,[status(thm)],[254])).
% 71.58/18.30 thf(362,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (relr @ B @ sk7)) | (~ (reli @ sk8 @ sk8)) | ((reli @ A @ (sk9 @ A @ (^ [C:$i]: (($false))))) != (reli @ sk3 @ B)))),inference(paramod_ordered,[status(thm)],[319,92])).
% 71.58/18.30 thf(363,plain,(! [B:$i,A:$i] : ((~ (relr @ B @ sk7)) | (~ (reli @ sk8 @ sk8)) | ((reli @ A @ (sk9 @ A @ (^ [C:$i]: (($false))))) != (reli @ sk3 @ B)))),inference(simp,[status(thm)],[362])).
% 71.58/18.30 thf(364,plain,((~ (relr @ (sk9 @ sk3 @ (^ [A:$i]: (($false)))) @ sk7)) | (~ (reli @ sk8 @ sk8))),inference(pattern_uni,[status(thm)],[363:[bind(A, $thf(sk3)),bind(B, $thf(sk9 @ sk3 @ (^ [C:$i]: (($false)))))]])).
% 71.58/18.30 thf(2649,plain,((~ (relr @ (sk9 @ sk3 @ (^ [A:$i]: (($false)))) @ sk7)) | ~ (($true)) | ((reli @ sk8 @ sk8) != (reli @ sk7 @ sk8))),inference(paramod_ordered,[status(thm)],[14,364])).
% 71.58/18.30 thf(2650,plain,((~ (relr @ (sk9 @ sk3 @ (^ [A:$i]: (($false)))) @ sk7)) | ((reli @ sk8 @ sk8) != (reli @ sk7 @ sk8))),inference(simp,[status(thm)],[2649])).
% 71.58/18.30 thf(2696,plain,((~ (relr @ (sk9 @ sk3 @ (^ [A:$i]: (($false)))) @ sk7)) | (sk8 != sk7) | (sk8 != sk8)),inference(simp,[status(thm)],[2650])).
% 71.58/18.30 thf(2745,plain,((~ (relr @ (sk9 @ sk3 @ (^ [A:$i]: (($false)))) @ sk7)) | (sk8 != sk7)),inference(simp,[status(thm)],[2696])).
% 71.58/18.30 thf(2777,plain,(! [A:$i] : (~ (($true)) | (sk8 != sk7) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ (sk9 @ sk3 @ (^ [B:$i]: (($false)))) @ sk7)))),inference(paramod_ordered,[status(thm)],[1105,2745])).
% 71.58/18.30 thf(2778,plain,(! [A:$i] : ((sk8 != sk7) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ (sk9 @ sk3 @ (^ [B:$i]: (($false)))) @ sk7)))),inference(simp,[status(thm)],[2777])).
% 71.58/18.30 thf(2810,plain,(! [A:$i] : ((sk8 != sk7) | (A != (sk9 @ sk3 @ (^ [B:$i]: (($false))))) | ((sk10 @ A @ (^ [B:$i]: (($false)))) != sk7))),inference(simp,[status(thm)],[2778])).
% 71.58/18.30 thf(2837,plain,((sk8 != sk7) | ((sk10 @ (sk9 @ sk3 @ (^ [A:$i]: (($false)))) @ (^ [A:$i]: (($false)))) != sk7)),inference(simp,[status(thm)],[2810])).
% 71.58/18.30 thf(677,plain,((~ (relr @ sk4 @ sk7)) | ~ (($true)) | ((reli @ sk8 @ sk8) != (reli @ sk3 @ sk4))),inference(paramod_ordered,[status(thm)],[15,184])).
% 71.58/18.30 thf(678,plain,((~ (relr @ sk4 @ sk7)) | ((reli @ sk8 @ sk8) != (reli @ sk3 @ sk4))),inference(simp,[status(thm)],[677])).
% 71.58/18.30 thf(698,plain,((~ (relr @ sk4 @ sk7)) | (sk8 != sk3) | (sk8 != sk4)),inference(simp,[status(thm)],[678])).
% 71.58/18.30 thf(1991,plain,(! [A:$i] : (~ (($true)) | (sk8 != sk3) | (sk8 != sk4) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ sk4 @ sk7)))),inference(paramod_ordered,[status(thm)],[1105,698])).
% 71.58/18.30 thf(1992,plain,(! [A:$i] : ((sk8 != sk3) | (sk8 != sk4) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ sk4 @ sk7)))),inference(simp,[status(thm)],[1991])).
% 71.58/18.30 thf(2014,plain,(! [A:$i] : ((sk8 != sk3) | (sk8 != sk4) | (A != sk4) | ((sk10 @ A @ (^ [B:$i]: (($false)))) != sk7))),inference(simp,[status(thm)],[1992])).
% 71.58/18.30 thf(2035,plain,((sk8 != sk3) | (sk8 != sk4) | ((sk10 @ sk4 @ (^ [A:$i]: (($false)))) != sk7)),inference(simp,[status(thm)],[2014])).
% 71.58/18.30 thf(11,plain,((relr @ sk6 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 71.58/18.30 thf(179,plain,(! [A:$i] : ((~ (reli @ sk3 @ A)) | ~ (($true)) | (~ (reli @ sk8 @ sk8)) | ((relr @ sk6 @ sk7) != (relr @ A @ sk7)))),inference(paramod_ordered,[status(thm)],[11,92])).
% 71.58/18.30 thf(180,plain,(! [A:$i] : ((~ (reli @ sk3 @ A)) | (~ (reli @ sk8 @ sk8)) | ((relr @ sk6 @ sk7) != (relr @ A @ sk7)))),inference(simp,[status(thm)],[179])).
% 71.58/18.30 thf(181,plain,((~ (reli @ sk3 @ sk6)) | (~ (reli @ sk8 @ sk8))),inference(pattern_uni,[status(thm)],[180:[bind(A, $thf(sk6))]])).
% 71.58/18.30 thf(410,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | (~ (reli @ sk3 @ sk6)) | ~ (($true)) | ((A @ B) != (reli @ sk8 @ sk8)))),inference(paramod_ordered,[status(thm)],[19,181])).
% 71.58/18.30 thf(411,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | (~ (reli @ sk3 @ sk6)) | ((A @ B) != (reli @ sk8 @ sk8)))),inference(simp,[status(thm)],[410])).
% 71.58/18.30 thf(439,plain,((reli @ sk8 @ (sk9 @ sk8 @ (reli @ sk8))) | (~ (reli @ sk3 @ sk6))),inference(pre_uni,[status(thm)],[411:[bind(A, $thf(reli @ sk8)),bind(B, $thf(sk8))]])).
% 71.58/18.30 thf(20,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk9 @ B @ (A)))) | (A @ B))),inference(cnfConj,[status(thm)],[18])).
% 71.58/18.30 thf(22161,plain,(! [B:$i,A:($i > $o)] : ((~ (reli @ sk3 @ sk6)) | ~ (($true)) | (A @ B) | ((reli @ sk8 @ (sk9 @ sk8 @ (reli @ sk8))) != (A @ (sk9 @ B @ (A)))))),inference(paramod_ordered,[status(thm)],[439,20])).
% 71.58/18.30 thf(22162,plain,(! [B:$i,A:($i > $o)] : ((~ (reli @ sk3 @ sk6)) | (A @ B) | ((reli @ sk8 @ (sk9 @ sk8 @ (reli @ sk8))) != (A @ (sk9 @ B @ (A)))))),inference(simp,[status(thm)],[22161])).
% 71.58/18.30 thf(22480,plain,((~ (reli @ sk3 @ sk6)) | (reli @ sk8 @ sk8)),inference(pre_uni,[status(thm)],[22162:[bind(A, $thf(reli @ sk8)),bind(B, $thf(sk8))]])).
% 71.58/18.30 thf(22704,plain,((~ (reli @ sk3 @ sk6)) | (~ (reli @ sk3 @ sk6)) | ~ (($true)) | ((reli @ sk8 @ sk8) != (reli @ sk8 @ sk8))),inference(paramod_ordered,[status(thm)],[22480,181])).
% 71.58/18.30 thf(22705,plain,((~ (reli @ sk3 @ sk6)) | ((reli @ sk8 @ sk8) != (reli @ sk8 @ sk8))),inference(simp,[status(thm)],[22704])).
% 71.58/18.30 thf(22706,plain,((~ (reli @ sk3 @ sk6))),inference(pattern_uni,[status(thm)],[22705:[]])).
% 71.58/18.30 thf(675,plain,(! [A:$i] : ((~ (relr @ sk4 @ sk7)) | ~ (($true)) | ((reli @ A @ (sk9 @ A @ (^ [B:$i]: (($false))))) != (reli @ sk8 @ sk8)))),inference(paramod_ordered,[status(thm)],[319,184])).
% 71.58/18.30 thf(676,plain,(! [A:$i] : ((~ (relr @ sk4 @ sk7)) | ((reli @ A @ (sk9 @ A @ (^ [B:$i]: (($false))))) != (reli @ sk8 @ sk8)))),inference(simp,[status(thm)],[675])).
% 71.58/18.30 thf(710,plain,(! [A:$i] : ((~ (relr @ sk4 @ sk7)) | (A != sk8) | ((sk9 @ A @ (^ [B:$i]: (($false)))) != sk8))),inference(simp,[status(thm)],[676])).
% 71.58/18.30 thf(715,plain,((~ (relr @ sk4 @ sk7)) | ((sk9 @ sk8 @ (^ [A:$i]: (($false)))) != sk8)),inference(simp,[status(thm)],[710])).
% 71.58/18.30 thf(10576,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk10 @ B @ (A))) | (reli @ sk8 @ (sk9 @ sk8 @ (^ [C:$i]: (reli @ C @ C)))) | ~ (($true)) | ((A @ B) != (relr @ sk4 @ sk7)))),inference(paramod_ordered,[status(thm)],[25,705])).
% 71.58/18.30 thf(10577,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk10 @ B @ (A))) | (reli @ sk8 @ (sk9 @ sk8 @ (^ [C:$i]: (reli @ C @ C)))) | ((A @ B) != (relr @ sk4 @ sk7)))),inference(simp,[status(thm)],[10576])).
% 71.58/18.30 thf(10698,plain,((relr @ sk4 @ (sk10 @ sk4 @ (^ [A:$i]: (relr @ A @ sk7)))) | (reli @ sk8 @ (sk9 @ sk8 @ (^ [A:$i]: (reli @ A @ A))))),inference(pre_uni,[status(thm)],[10577:[bind(A, $thf(^ [C:$i]: (relr @ C @ sk7))),bind(B, $thf(sk4))]])).
% 71.58/18.30 thf(6,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ relr @ A) @ (mbox @ relr @ (mbox @ relr @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',trans_axiom_r)).
% 71.58/18.30 thf(35,plain,((! [A:($i > $o),B:$i]: (~ (! [C:$i]: ((relr @ B @ C) => (A @ C))) | ! [C:$i]: ((relr @ B @ C) => (! [D:$i]: ((relr @ C @ D) => (A @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 71.58/18.30 thf(36,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((((relr @ B @ (sk12 @ B @ (A))) | ~ (relr @ B @ C) | ~ (relr @ C @ D) | (A @ D)) & (~ (A @ (sk12 @ B @ (A))) | ~ (relr @ B @ C) | ~ (relr @ C @ D) | (A @ D))))),inference(cnf,[status(esa)],[35])).
% 71.58/18.30 thf(37,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((relr @ B @ (sk12 @ B @ (A))) | (~ (relr @ B @ C)) | (~ (relr @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[36])).
% 71.58/18.30 thf(22990,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk10 @ B @ (A))) | ~ (($true)) | ((A @ B) != (reli @ sk3 @ sk6)))),inference(paramod_ordered,[status(thm)],[25,22706])).
% 71.58/18.30 thf(22991,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk10 @ B @ (A))) | ((A @ B) != (reli @ sk3 @ sk6)))),inference(simp,[status(thm)],[22990])).
% 71.58/18.30 thf(23123,plain,((relr @ sk6 @ (sk10 @ sk6 @ (reli @ sk3)))),inference(pre_uni,[status(thm)],[22991:[bind(A, $thf(reli @ sk3)),bind(B, $thf(sk6))]])).
% 71.58/18.30 thf(679,plain,((~ (relr @ sk4 @ sk7)) | ~ (($true)) | ((reli @ sk8 @ sk8) != (reli @ sk7 @ sk8))),inference(paramod_ordered,[status(thm)],[14,184])).
% 71.58/18.30 thf(680,plain,((~ (relr @ sk4 @ sk7)) | ((reli @ sk8 @ sk8) != (reli @ sk7 @ sk8))),inference(simp,[status(thm)],[679])).
% 71.58/18.30 thf(706,plain,((~ (relr @ sk4 @ sk7)) | (sk8 != sk7) | (sk8 != sk8)),inference(simp,[status(thm)],[680])).
% 71.58/18.30 thf(711,plain,((~ (relr @ sk4 @ sk7)) | (sk8 != sk7)),inference(simp,[status(thm)],[706])).
% 71.58/18.30 thf(997,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk10 @ B @ (A))) | ~ (($true)) | (sk8 != sk7) | ((A @ B) != (relr @ sk4 @ sk7)))),inference(paramod_ordered,[status(thm)],[25,711])).
% 71.58/18.30 thf(998,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk10 @ B @ (A))) | (sk8 != sk7) | ((A @ B) != (relr @ sk4 @ sk7)))),inference(simp,[status(thm)],[997])).
% 71.58/18.30 thf(1033,plain,((relr @ sk4 @ (sk10 @ sk4 @ (^ [A:$i]: (relr @ A @ sk7)))) | (sk8 != sk7)),inference(pre_uni,[status(thm)],[998:[bind(A, $thf(^ [C:$i]: (relr @ C @ sk7))),bind(B, $thf(sk4))]])).
% 71.58/18.30 thf(12539,plain,((sk8 != sk7) | ~ (($true)) | (sk8 != sk7) | ((relr @ sk4 @ (sk10 @ sk4 @ (^ [A:$i]: (relr @ A @ sk7)))) != (relr @ sk4 @ sk7))),inference(paramod_ordered,[status(thm)],[1033,711])).
% 71.58/18.30 thf(12540,plain,((sk8 != sk7) | ((relr @ sk4 @ (sk10 @ sk4 @ (^ [A:$i]: (relr @ A @ sk7)))) != (relr @ sk4 @ sk7))),inference(simp,[status(thm)],[12539])).
% 71.58/18.30 thf(12584,plain,((sk8 != sk7) | (sk4 != sk4) | ((sk10 @ sk4 @ (^ [A:$i]: (relr @ A @ sk7))) != sk7)),inference(simp,[status(thm)],[12540])).
% 71.58/18.30 thf(12606,plain,((sk8 != sk7) | ((sk10 @ sk4 @ (^ [A:$i]: (relr @ A @ sk7))) != sk7)),inference(simp,[status(thm)],[12584])).
% 71.58/18.30 thf(16,plain,((reli @ sk2 @ sk3)),inference(cnfConj,[status(thm)],[9])).
% 71.58/18.30 thf(175,plain,(! [A:$i] : (~ (($true)) | (~ (relr @ A @ sk7)) | (~ (reli @ sk8 @ sk8)) | ((reli @ sk3 @ A) != (reli @ sk2 @ sk3)))),inference(paramod_ordered,[status(thm)],[16,92])).
% 71.58/18.30 thf(176,plain,(! [A:$i] : ((~ (relr @ A @ sk7)) | (~ (reli @ sk8 @ sk8)) | ((reli @ sk3 @ A) != (reli @ sk2 @ sk3)))),inference(simp,[status(thm)],[175])).
% 71.58/18.30 thf(189,plain,(! [A:$i] : ((~ (relr @ A @ sk7)) | (~ (reli @ sk8 @ sk8)) | (sk3 != sk2) | (A != sk3))),inference(simp,[status(thm)],[176])).
% 71.58/18.30 thf(196,plain,((~ (relr @ sk3 @ sk7)) | (~ (reli @ sk8 @ sk8)) | (sk3 != sk2)),inference(simp,[status(thm)],[189])).
% 71.58/18.30 thf(10800,plain,(! [A:$i] : (~ (($true)) | ((sk9 @ sk8 @ (^ [B:$i]: (reli @ B @ B))) != sk8) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ sk4 @ sk7)))),inference(paramod_ordered,[status(thm)],[1105,10753])).
% 71.58/18.30 thf(10801,plain,(! [A:$i] : (((sk9 @ sk8 @ (^ [B:$i]: (reli @ B @ B))) != sk8) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ sk4 @ sk7)))),inference(simp,[status(thm)],[10800])).
% 71.58/18.30 thf(10864,plain,(! [A:$i] : (((sk9 @ sk8 @ (^ [B:$i]: (reli @ B @ B))) != sk8) | (A != sk4) | ((sk10 @ A @ (^ [B:$i]: (($false)))) != sk7))),inference(simp,[status(thm)],[10801])).
% 71.58/18.30 thf(10891,plain,(((sk9 @ sk8 @ (^ [A:$i]: (reli @ A @ A))) != sk8) | ((sk10 @ sk4 @ (^ [A:$i]: (($false)))) != sk7)),inference(simp,[status(thm)],[10864])).
% 71.58/18.30 thf(64,plain,(! [E:$i,D:individuals,C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | ~ (($true)) | (sk1 @ D @ E) | ((reli @ sk4 @ sk6) != (reli @ C @ E)))),inference(paramod_ordered,[status(thm)],[12,10])).
% 71.58/18.30 thf(65,plain,(! [E:$i,D:individuals,C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (sk1 @ D @ E) | ((reli @ sk4 @ sk6) != (reli @ C @ E)))),inference(simp,[status(thm)],[64])).
% 71.58/18.30 thf(66,plain,(! [C:individuals,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ sk4)) | (sk1 @ C @ sk6))),inference(pattern_uni,[status(thm)],[65:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(sk4)),bind(D, $thf(D)),bind(E, $thf(sk6))]])).
% 71.58/18.30 thf(78,plain,(! [C:individuals,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ sk4)) | (sk1 @ C @ sk6))),inference(simp,[status(thm)],[66])).
% 71.58/18.30 thf(5,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ reli @ A) @ (mbox @ reli @ (mbox @ reli @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',trans_axiom_i)).
% 71.58/18.30 thf(29,plain,((! [A:($i > $o),B:$i]: (~ (! [C:$i]: ((reli @ B @ C) => (A @ C))) | ! [C:$i]: ((reli @ B @ C) => (! [D:$i]: ((reli @ C @ D) => (A @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 71.58/18.30 thf(703,plain,((reli @ sk8 @ (sk9 @ sk8 @ (^ [A:$i]: (reli @ A @ sk8)))) | (~ (relr @ sk4 @ sk7))),inference(pre_uni,[status(thm)],[694:[bind(A, $thf(^ [C:$i]: (reli @ C @ sk8))),bind(B, $thf(sk8))]])).
% 71.58/18.30 thf(26827,plain,((~ (relr @ sk4 @ sk7)) | (~ (relr @ sk4 @ sk7)) | ~ (($true)) | ((reli @ sk8 @ (sk9 @ sk8 @ (^ [A:$i]: (reli @ A @ sk8)))) != (reli @ sk8 @ sk8))),inference(paramod_ordered,[status(thm)],[703,184])).
% 71.58/18.31 thf(26828,plain,((~ (relr @ sk4 @ sk7)) | ((reli @ sk8 @ (sk9 @ sk8 @ (^ [A:$i]: (reli @ A @ sk8)))) != (reli @ sk8 @ sk8))),inference(simp,[status(thm)],[26827])).
% 71.58/18.31 thf(27014,plain,((~ (relr @ sk4 @ sk7)) | (sk8 != sk8) | ((sk9 @ sk8 @ (^ [A:$i]: (reli @ A @ sk8))) != sk8)),inference(simp,[status(thm)],[26828])).
% 71.58/18.31 thf(27067,plain,((~ (relr @ sk4 @ sk7)) | ((sk9 @ sk8 @ (^ [A:$i]: (reli @ A @ sk8))) != sk8)),inference(simp,[status(thm)],[27014])).
% 71.58/18.31 thf(23066,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | ~ (($true)) | ((A @ B) != (reli @ sk3 @ sk6)))),inference(paramod_ordered,[status(thm)],[19,22706])).
% 71.58/18.31 thf(23067,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | ((A @ B) != (reli @ sk3 @ sk6)))),inference(simp,[status(thm)],[23066])).
% 71.58/18.31 thf(23115,plain,((reli @ sk3 @ (sk9 @ sk3 @ (^ [A:$i]: (reli @ A @ sk6))))),inference(pre_uni,[status(thm)],[23067:[bind(A, $thf(^ [C:$i]: (reli @ C @ sk6))),bind(B, $thf(sk3))]])).
% 71.58/18.31 thf(6677,plain,((~ (relr @ sk3 @ sk7)) | ~ (($true)) | (sk3 != sk2) | ((reli @ sk8 @ sk8) != (reli @ sk7 @ sk8))),inference(paramod_ordered,[status(thm)],[14,196])).
% 71.58/18.31 thf(6678,plain,((~ (relr @ sk3 @ sk7)) | (sk3 != sk2) | ((reli @ sk8 @ sk8) != (reli @ sk7 @ sk8))),inference(simp,[status(thm)],[6677])).
% 71.58/18.31 thf(6774,plain,((~ (relr @ sk3 @ sk7)) | (sk3 != sk2) | (sk8 != sk7) | (sk8 != sk8)),inference(simp,[status(thm)],[6678])).
% 71.58/18.31 thf(6841,plain,((~ (relr @ sk3 @ sk7)) | (sk3 != sk2) | (sk8 != sk7)),inference(simp,[status(thm)],[6774])).
% 71.58/18.31 thf(72,plain,(! [E:$i,D:individuals,C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (sk1 @ D @ E) | ((reli @ C @ E) != (reli @ B @ C)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[10])).
% 71.58/18.31 thf(75,plain,(! [C:$i,B:individuals,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ C)) | (~ (reli @ C @ C)) | (sk1 @ B @ C))),inference(pattern_uni,[status(thm)],[72:[bind(A, $thf(A)),bind(B, $thf(E)),bind(C, $thf(E))]])).
% 71.58/18.31 thf(84,plain,(! [C:$i,B:individuals,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ C)) | (~ (reli @ C @ C)) | (sk1 @ B @ C))),inference(simp,[status(thm)],[75])).
% 71.58/18.31 thf(226,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | ~ (($true)) | ((A @ B) != (sk1 @ sk5 @ sk8)))),inference(paramod_ordered,[status(thm)],[19,13])).
% 71.58/18.31 thf(227,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | ((A @ B) != (sk1 @ sk5 @ sk8)))),inference(simp,[status(thm)],[226])).
% 71.58/18.31 thf(280,plain,((reli @ sk8 @ (sk9 @ sk8 @ (sk1 @ sk5)))),inference(pre_uni,[status(thm)],[227:[bind(A, $thf(sk1 @ sk5)),bind(B, $thf(sk8))]])).
% 71.58/18.31 thf(1188,plain,(! [A:$i] : (~ (($true)) | (sk8 != sk7) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ sk4 @ sk7)))),inference(paramod_ordered,[status(thm)],[1105,711])).
% 71.58/18.31 thf(1189,plain,(! [A:$i] : ((sk8 != sk7) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ sk4 @ sk7)))),inference(simp,[status(thm)],[1188])).
% 71.58/18.31 thf(1200,plain,(! [A:$i] : ((sk8 != sk7) | (A != sk4) | ((sk10 @ A @ (^ [B:$i]: (($false)))) != sk7))),inference(simp,[status(thm)],[1189])).
% 71.58/18.31 thf(1201,plain,((sk8 != sk7) | ((sk10 @ sk4 @ (^ [A:$i]: (($false)))) != sk7)),inference(simp,[status(thm)],[1200])).
% 71.58/18.31 thf(246,plain,(! [A:$i] : ((reli @ A @ (sk9 @ A @ (prop_a))) | (prop_a @ A))),inference(prim_subst,[status(thm)],[19:[bind(A, $thf(prop_a))]])).
% 71.58/18.31 thf(312,plain,(! [A:$i] : ((reli @ A @ (sk9 @ A @ (prop_a))) | (prop_a @ A))),inference(simp,[status(thm)],[246])).
% 71.58/18.31 thf(98,plain,(! [C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | ~ (($true)) | (~ (reli @ C @ sk8)) | ((reli @ sk4 @ sk6) != (reli @ B @ C)))),inference(paramod_ordered,[status(thm)],[12,58])).
% 71.58/18.31 thf(99,plain,(! [C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ C @ sk8)) | ((reli @ sk4 @ sk6) != (reli @ B @ C)))),inference(simp,[status(thm)],[98])).
% 71.58/18.31 thf(100,plain,(! [A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ sk4)) | (~ (reli @ sk6 @ sk8)))),inference(pattern_uni,[status(thm)],[99:[bind(A, $thf(A)),bind(B, $thf(sk4)),bind(C, $thf(sk6))]])).
% 71.58/18.31 thf(28770,plain,(! [A:$i] : (~ (($true)) | (~ (relr @ A @ sk4)) | (~ (reli @ sk6 @ sk8)) | ((reli @ sk3 @ sk4) != (reli @ sk3 @ A)))),inference(paramod_ordered,[status(thm)],[15,100])).
% 71.58/18.31 thf(28771,plain,(! [A:$i] : ((~ (relr @ A @ sk4)) | (~ (reli @ sk6 @ sk8)) | ((reli @ sk3 @ sk4) != (reli @ sk3 @ A)))),inference(simp,[status(thm)],[28770])).
% 71.58/18.31 thf(28772,plain,((~ (relr @ sk4 @ sk4)) | (~ (reli @ sk6 @ sk8))),inference(pattern_uni,[status(thm)],[28771:[bind(A, $thf(sk4))]])).
% 71.58/18.31 thf(71,plain,(! [E:$i,D:individuals,C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (sk1 @ D @ E) | ((reli @ C @ E) != (reli @ sk3 @ A)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[10])).
% 71.58/18.31 thf(76,plain,(! [C:$i,B:individuals,A:$i] : ((~ (reli @ sk3 @ C)) | (~ (relr @ C @ A)) | (~ (reli @ A @ sk3)) | (sk1 @ B @ C))),inference(pattern_uni,[status(thm)],[71:[bind(A, $thf(E)),bind(B, $thf(B)),bind(C, $thf(sk3))]])).
% 71.58/18.31 thf(85,plain,(! [C:$i,B:individuals,A:$i] : ((~ (reli @ sk3 @ C)) | (~ (relr @ C @ A)) | (~ (reli @ A @ sk3)) | (sk1 @ B @ C))),inference(simp,[status(thm)],[76])).
% 71.58/18.31 thf(22992,plain,(~ (($true)) | ((reli @ sk7 @ sk8) != (reli @ sk3 @ sk6))),inference(paramod_ordered,[status(thm)],[14,22706])).
% 71.58/18.31 thf(22993,plain,(((reli @ sk7 @ sk8) != (reli @ sk3 @ sk6))),inference(simp,[status(thm)],[22992])).
% 71.58/18.31 thf(23131,plain,((sk7 != sk3) | (sk8 != sk6)),inference(simp,[status(thm)],[22993])).
% 71.58/18.31 thf(979,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk10 @ B @ (A))) | ~ (($true)) | ((A @ B) != (sk1 @ sk5 @ sk8)))),inference(paramod_ordered,[status(thm)],[25,13])).
% 71.58/18.31 thf(980,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk10 @ B @ (A))) | ((A @ B) != (sk1 @ sk5 @ sk8)))),inference(simp,[status(thm)],[979])).
% 71.58/18.31 thf(1047,plain,((relr @ sk8 @ (sk10 @ sk8 @ (sk1 @ sk5)))),inference(pre_uni,[status(thm)],[980:[bind(A, $thf(sk1 @ sk5)),bind(B, $thf(sk8))]])).
% 71.58/18.31 thf(22994,plain,(~ (($true)) | ((reli @ sk8 @ (sk9 @ sk8 @ (sk1 @ sk5))) != (reli @ sk3 @ sk6))),inference(paramod_ordered,[status(thm)],[280,22706])).
% 71.58/18.31 thf(22995,plain,(((reli @ sk8 @ (sk9 @ sk8 @ (sk1 @ sk5))) != (reli @ sk3 @ sk6))),inference(simp,[status(thm)],[22994])).
% 71.58/18.31 thf(23081,plain,((sk8 != sk3) | ((sk9 @ sk8 @ (sk1 @ sk5)) != sk6)),inference(simp,[status(thm)],[22995])).
% 71.58/18.31 thf(10699,plain,((relr @ sk7 @ (sk10 @ sk7 @ (relr @ sk4))) | (reli @ sk8 @ (sk9 @ sk8 @ (^ [A:$i]: (reli @ A @ A))))),inference(pre_uni,[status(thm)],[10577:[bind(A, $thf(relr @ sk4)),bind(B, $thf(sk7))]])).
% 71.58/18.31 thf(23058,plain,(! [A:$i] : (~ (($true)) | ((reli @ A @ (sk9 @ A @ (^ [B:$i]: (($false))))) != (reli @ sk3 @ sk6)))),inference(paramod_ordered,[status(thm)],[319,22706])).
% 71.58/18.31 thf(23059,plain,(! [A:$i] : (((reli @ A @ (sk9 @ A @ (^ [B:$i]: (($false))))) != (reli @ sk3 @ sk6)))),inference(simp,[status(thm)],[23058])).
% 71.58/18.31 thf(23086,plain,(! [A:$i] : ((A != sk3) | ((sk9 @ A @ (^ [B:$i]: (($false)))) != sk6))),inference(simp,[status(thm)],[23059])).
% 71.58/18.31 thf(23143,plain,(((sk9 @ sk3 @ (^ [A:$i]: (($false)))) != sk6)),inference(simp,[status(thm)],[23086])).
% 71.58/18.31 thf(23116,plain,((reli @ sk6 @ (sk9 @ sk6 @ (reli @ sk3)))),inference(pre_uni,[status(thm)],[23067:[bind(A, $thf(reli @ sk3)),bind(B, $thf(sk6))]])).
% 71.58/18.31 thf(29037,plain,((~ (relr @ sk4 @ sk4)) | ~ (($true)) | ((reli @ sk7 @ sk8) != (reli @ sk6 @ sk8))),inference(paramod_ordered,[status(thm)],[14,28772])).
% 71.58/18.31 thf(29038,plain,((~ (relr @ sk4 @ sk4)) | ((reli @ sk7 @ sk8) != (reli @ sk6 @ sk8))),inference(simp,[status(thm)],[29037])).
% 71.58/18.31 thf(29236,plain,((~ (relr @ sk4 @ sk4)) | (sk7 != sk6) | (sk8 != sk8)),inference(simp,[status(thm)],[29038])).
% 71.58/18.31 thf(29300,plain,((~ (relr @ sk4 @ sk4)) | (sk7 != sk6)),inference(simp,[status(thm)],[29236])).
% 71.58/18.31 thf(29346,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk10 @ B @ (A))) | ~ (($true)) | (sk7 != sk6) | ((A @ B) != (relr @ sk4 @ sk4)))),inference(paramod_ordered,[status(thm)],[25,29300])).
% 71.58/18.31 thf(29347,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk10 @ B @ (A))) | (sk7 != sk6) | ((A @ B) != (relr @ sk4 @ sk4)))),inference(simp,[status(thm)],[29346])).
% 71.58/18.31 thf(29444,plain,((relr @ sk4 @ (sk10 @ sk4 @ (^ [A:$i]: (relr @ A @ A)))) | (sk7 != sk6)),inference(pre_uni,[status(thm)],[29347:[bind(A, $thf(^ [C:$i]: (relr @ C @ C))),bind(B, $thf(sk4))]])).
% 71.58/18.31 thf(2571,plain,(~ (($true)) | ((sk10 @ sk4 @ (^ [A:$i]: (($false)))) != sk7) | ((reli @ sk8 @ sk8) != (reli @ sk2 @ sk3))),inference(paramod_ordered,[status(thm)],[16,1207])).
% 71.58/18.31 thf(2572,plain,(((sk10 @ sk4 @ (^ [A:$i]: (($false)))) != sk7) | ((reli @ sk8 @ sk8) != (reli @ sk2 @ sk3))),inference(simp,[status(thm)],[2571])).
% 71.58/18.31 thf(2606,plain,(((sk10 @ sk4 @ (^ [A:$i]: (($false)))) != sk7) | (sk8 != sk2) | (sk8 != sk3)),inference(simp,[status(thm)],[2572])).
% 71.58/18.31 thf(26,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk10 @ B @ (A)))) | (A @ B))),inference(cnfConj,[status(thm)],[24])).
% 71.58/18.31 thf(27,plain,(! [B:$i,A:($i > $o)] : ((~ ((sk10 @ B @ (A)) = (sk10 @ B @ ((=) @ $i @ (sk10 @ B @ A))))) | ((sk10 @ B @ (A)) = B))),inference(replace_leibeq,[status(thm)],[26:[bind(A, $thf((=) @ $i @ (sk10 @ B @ A)))]])).
% 71.58/18.31 thf(28,plain,(! [B:$i,A:($i > $o)] : (((sk10 @ B @ (A)) != (sk10 @ B @ ((=) @ $i @ (sk10 @ B @ A)))) | ((sk10 @ B @ (A)) = B))),inference(lifteq,[status(thm)],[27])).
% 71.58/18.31 thf(38,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk12 @ B @ (A)))) | (~ (relr @ B @ C)) | (~ (relr @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[36])).
% 71.58/18.31 thf(1029,plain,(! [A:$i] : ((relr @ A @ (sk10 @ A @ (prop_a))) | (prop_a @ A))),inference(prim_subst,[status(thm)],[25:[bind(A, $thf(prop_a))]])).
% 71.58/18.31 thf(1106,plain,(! [A:$i] : ((relr @ A @ (sk10 @ A @ (prop_a))) | (prop_a @ A))),inference(simp,[status(thm)],[1029])).
% 71.58/18.31 thf(691,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | ~ (($true)) | (~ (reli @ sk8 @ sk8)) | ((A @ B) != (relr @ sk4 @ sk7)))),inference(paramod_ordered,[status(thm)],[19,184])).
% 71.58/18.31 thf(692,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | (~ (reli @ sk8 @ sk8)) | ((A @ B) != (relr @ sk4 @ sk7)))),inference(simp,[status(thm)],[691])).
% 71.58/18.31 thf(697,plain,((reli @ sk7 @ (sk9 @ sk7 @ (relr @ sk4))) | (~ (reli @ sk8 @ sk8))),inference(pre_uni,[status(thm)],[692:[bind(A, $thf(relr @ sk4)),bind(B, $thf(sk7))]])).
% 71.58/18.31 thf(1031,plain,(! [A:$i] : ((relr @ A @ (sk10 @ A @ (prop_b))) | (prop_b @ A))),inference(prim_subst,[status(thm)],[25:[bind(A, $thf(prop_b))]])).
% 71.58/18.31 thf(1108,plain,(! [A:$i] : ((relr @ A @ (sk10 @ A @ (prop_b))) | (prop_b @ A))),inference(simp,[status(thm)],[1031])).
% 71.58/18.31 thf(1966,plain,(! [A:$i] : ((prop_b @ A) | ~ (($true)) | (sk8 != sk7) | ((relr @ A @ (sk10 @ A @ (prop_b))) != (relr @ sk4 @ sk7)))),inference(paramod_ordered,[status(thm)],[1108,711])).
% 71.58/18.31 thf(1967,plain,(! [A:$i] : ((prop_b @ A) | (sk8 != sk7) | ((relr @ A @ (sk10 @ A @ (prop_b))) != (relr @ sk4 @ sk7)))),inference(simp,[status(thm)],[1966])).
% 71.58/18.31 thf(1973,plain,(! [A:$i] : ((prop_b @ A) | (sk8 != sk7) | (A != sk4) | ((sk10 @ A @ (prop_b)) != sk7))),inference(simp,[status(thm)],[1967])).
% 71.58/18.31 thf(1983,plain,((prop_b @ sk4) | (sk8 != sk7) | ((sk10 @ sk4 @ (prop_b)) != sk7)),inference(simp,[status(thm)],[1973])).
% 71.58/18.31 thf(412,plain,(~ (($true)) | (~ (reli @ sk8 @ sk8)) | ((reli @ sk3 @ sk6) != (reli @ sk3 @ sk4))),inference(paramod_ordered,[status(thm)],[15,181])).
% 71.58/18.31 thf(413,plain,((~ (reli @ sk8 @ sk8)) | ((reli @ sk3 @ sk6) != (reli @ sk3 @ sk4))),inference(simp,[status(thm)],[412])).
% 71.58/18.31 thf(425,plain,((~ (reli @ sk8 @ sk8)) | (sk3 != sk3) | (sk6 != sk4)),inference(simp,[status(thm)],[413])).
% 71.58/18.31 thf(446,plain,((~ (reli @ sk8 @ sk8)) | (sk6 != sk4)),inference(simp,[status(thm)],[425])).
% 71.58/18.31 thf(537,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | ~ (($true)) | (sk6 != sk4) | ((A @ B) != (reli @ sk8 @ sk8)))),inference(paramod_ordered,[status(thm)],[19,446])).
% 71.58/18.31 thf(538,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | (sk6 != sk4) | ((A @ B) != (reli @ sk8 @ sk8)))),inference(simp,[status(thm)],[537])).
% 71.58/18.31 thf(549,plain,((reli @ sk8 @ (sk9 @ sk8 @ (reli @ sk8))) | (sk6 != sk4)),inference(pre_uni,[status(thm)],[538:[bind(A, $thf(reli @ sk8)),bind(B, $thf(sk8))]])).
% 71.58/18.31 thf(6527,plain,(! [B:$i,A:($i > $o)] : ((sk6 != sk4) | ~ (($true)) | (A @ B) | ((reli @ sk8 @ (sk9 @ sk8 @ (reli @ sk8))) != (A @ (sk9 @ B @ (A)))))),inference(paramod_ordered,[status(thm)],[549,20])).
% 71.58/18.31 thf(6528,plain,(! [B:$i,A:($i > $o)] : ((sk6 != sk4) | (A @ B) | ((reli @ sk8 @ (sk9 @ sk8 @ (reli @ sk8))) != (A @ (sk9 @ B @ (A)))))),inference(simp,[status(thm)],[6527])).
% 71.58/18.31 thf(6611,plain,((sk6 != sk4) | (reli @ sk8 @ sk8)),inference(pre_uni,[status(thm)],[6528:[bind(A, $thf(reli @ sk8)),bind(B, $thf(sk8))]])).
% 71.58/18.31 thf(7203,plain,((sk6 != sk4) | ~ (($true)) | (sk6 != sk4) | ((reli @ sk8 @ sk8) != (reli @ sk8 @ sk8))),inference(paramod_ordered,[status(thm)],[6611,446])).
% 71.58/18.31 thf(7204,plain,((sk6 != sk4) | ((reli @ sk8 @ sk8) != (reli @ sk8 @ sk8))),inference(simp,[status(thm)],[7203])).
% 71.58/18.31 thf(7205,plain,((sk6 != sk4)),inference(pattern_uni,[status(thm)],[7204:[]])).
% 71.58/18.31 thf(10674,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | (reli @ sk8 @ (sk9 @ sk8 @ (^ [C:$i]: (reli @ C @ C)))) | ~ (($true)) | ((A @ B) != (relr @ sk4 @ sk7)))),inference(paramod_ordered,[status(thm)],[19,705])).
% 71.58/18.31 thf(10675,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | (reli @ sk8 @ (sk9 @ sk8 @ (^ [C:$i]: (reli @ C @ C)))) | ((A @ B) != (relr @ sk4 @ sk7)))),inference(simp,[status(thm)],[10674])).
% 71.58/18.31 thf(10731,plain,((reli @ sk4 @ (sk9 @ sk4 @ (^ [A:$i]: (relr @ A @ sk7)))) | (reli @ sk8 @ (sk9 @ sk8 @ (^ [A:$i]: (reli @ A @ A))))),inference(pre_uni,[status(thm)],[10675:[bind(A, $thf(^ [C:$i]: (relr @ C @ sk7))),bind(B, $thf(sk4))]])).
% 71.58/18.31 thf(721,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | ~ (($true)) | (sk8 != sk7) | ((A @ B) != (relr @ sk4 @ sk7)))),inference(paramod_ordered,[status(thm)],[19,711])).
% 71.58/18.31 thf(722,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | (sk8 != sk7) | ((A @ B) != (relr @ sk4 @ sk7)))),inference(simp,[status(thm)],[721])).
% 71.58/18.31 thf(725,plain,((reli @ sk4 @ (sk9 @ sk4 @ (^ [A:$i]: (relr @ A @ sk7)))) | (sk8 != sk7)),inference(pre_uni,[status(thm)],[722:[bind(A, $thf(^ [C:$i]: (relr @ C @ sk7))),bind(B, $thf(sk4))]])).
% 71.58/18.31 thf(16069,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | (relr @ sk8 @ (sk10 @ sk8 @ (^ [C:$i]: (reli @ C @ C)))) | ~ (($true)) | ((A @ B) != (relr @ sk4 @ sk7)))),inference(paramod_ordered,[status(thm)],[19,1086])).
% 71.58/18.31 thf(16070,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | (relr @ sk8 @ (sk10 @ sk8 @ (^ [C:$i]: (reli @ C @ C)))) | ((A @ B) != (relr @ sk4 @ sk7)))),inference(simp,[status(thm)],[16069])).
% 71.58/18.31 thf(16144,plain,((reli @ sk4 @ (sk9 @ sk4 @ (^ [A:$i]: (relr @ A @ sk7)))) | (relr @ sk8 @ (sk10 @ sk8 @ (^ [A:$i]: (reli @ A @ A))))),inference(pre_uni,[status(thm)],[16070:[bind(A, $thf(^ [C:$i]: (relr @ C @ sk7))),bind(B, $thf(sk4))]])).
% 71.58/18.31 thf(22996,plain,(! [A:$i] : ((prop_a @ A) | ~ (($true)) | ((reli @ A @ (sk9 @ A @ (prop_a))) != (reli @ sk3 @ sk6)))),inference(paramod_ordered,[status(thm)],[312,22706])).
% 71.58/18.31 thf(22997,plain,(! [A:$i] : ((prop_a @ A) | ((reli @ A @ (sk9 @ A @ (prop_a))) != (reli @ sk3 @ sk6)))),inference(simp,[status(thm)],[22996])).
% 71.58/18.31 thf(23103,plain,(! [A:$i] : ((prop_a @ A) | (A != sk3) | ((sk9 @ A @ (prop_a)) != sk6))),inference(simp,[status(thm)],[22997])).
% 71.58/18.31 thf(23154,plain,((prop_a @ sk3) | ((sk9 @ sk3 @ (prop_a)) != sk6)),inference(simp,[status(thm)],[23103])).
% 71.58/18.31 thf(1719,plain,(! [A:$i] : ((prop_a @ A) | ~ (($true)) | (sk8 != sk7) | ((relr @ A @ (sk10 @ A @ (prop_a))) != (relr @ sk4 @ sk7)))),inference(paramod_ordered,[status(thm)],[1106,711])).
% 71.58/18.31 thf(1720,plain,(! [A:$i] : ((prop_a @ A) | (sk8 != sk7) | ((relr @ A @ (sk10 @ A @ (prop_a))) != (relr @ sk4 @ sk7)))),inference(simp,[status(thm)],[1719])).
% 71.58/18.31 thf(1727,plain,(! [A:$i] : ((prop_a @ A) | (sk8 != sk7) | (A != sk4) | ((sk10 @ A @ (prop_a)) != sk7))),inference(simp,[status(thm)],[1720])).
% 71.58/18.31 thf(1739,plain,((prop_a @ sk4) | (sk8 != sk7) | ((sk10 @ sk4 @ (prop_a)) != sk7)),inference(simp,[status(thm)],[1727])).
% 71.58/18.31 thf(673,plain,((~ (relr @ sk4 @ sk7)) | ~ (($true)) | ((reli @ sk8 @ sk8) != (reli @ sk2 @ sk3))),inference(paramod_ordered,[status(thm)],[16,184])).
% 71.58/18.31 thf(674,plain,((~ (relr @ sk4 @ sk7)) | ((reli @ sk8 @ sk8) != (reli @ sk2 @ sk3))),inference(simp,[status(thm)],[673])).
% 71.58/18.31 thf(701,plain,((~ (relr @ sk4 @ sk7)) | (sk8 != sk2) | (sk8 != sk3)),inference(simp,[status(thm)],[674])).
% 71.58/18.31 thf(7,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ reli @ (mbox @ relr @ A)) @ (mbox @ relr @ (mbox @ reli @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_i_r_commute)).
% 71.58/18.31 thf(41,plain,((! [A:($i > $o),B:$i]: (~ (! [C:$i]: ((reli @ B @ C) => (! [D:$i]: ((relr @ C @ D) => (A @ D))))) | ! [C:$i]: ((relr @ B @ C) => (! [D:$i]: ((reli @ C @ D) => (A @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 71.58/18.31 thf(23122,plain,((relr @ sk3 @ (sk10 @ sk3 @ (^ [A:$i]: (reli @ A @ sk6))))),inference(pre_uni,[status(thm)],[22991:[bind(A, $thf(^ [C:$i]: (reli @ C @ sk6))),bind(B, $thf(sk3))]])).
% 71.58/18.31 thf(1026,plain,(! [A:$i] : ((relr @ A @ (sk10 @ A @ (prop_c))) | (prop_c @ A))),inference(prim_subst,[status(thm)],[25:[bind(A, $thf(prop_c))]])).
% 71.58/18.31 thf(1103,plain,(! [A:$i] : ((relr @ A @ (sk10 @ A @ (prop_c))) | (prop_c @ A))),inference(simp,[status(thm)],[1026])).
% 71.58/18.31 thf(42,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((((reli @ B @ (sk13 @ B @ (A))) | ~ (relr @ B @ C) | ~ (reli @ C @ D) | (A @ D)) & ((relr @ (sk13 @ B @ (A)) @ (sk14 @ B @ (A))) | ~ (relr @ B @ C) | ~ (reli @ C @ D) | (A @ D)) & (~ (A @ (sk14 @ B @ (A))) | ~ (relr @ B @ C) | ~ (reli @ C @ D) | (A @ D))))),inference(cnf,[status(esa)],[41])).
% 71.58/18.31 thf(45,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk14 @ B @ (A)))) | (~ (relr @ B @ C)) | (~ (reli @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[42])).
% 71.58/18.31 thf(30,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((((reli @ B @ (sk11 @ B @ (A))) | ~ (reli @ B @ C) | ~ (reli @ C @ D) | (A @ D)) & (~ (A @ (sk11 @ B @ (A))) | ~ (reli @ B @ C) | ~ (reli @ C @ D) | (A @ D))))),inference(cnf,[status(esa)],[29])).
% 71.58/18.31 thf(32,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk11 @ B @ (A)))) | (~ (reli @ B @ C)) | (~ (reli @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[30])).
% 71.58/18.31 thf(33,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ ((sk11 @ B @ (A)) = (sk11 @ B @ ((=) @ $i @ (sk11 @ B @ A))))) | (~ (reli @ B @ C)) | (~ (reli @ C @ D)) | ((sk11 @ B @ (A)) = D))),inference(replace_leibeq,[status(thm)],[32:[bind(A, $thf((=) @ $i @ (sk11 @ B @ A)))]])).
% 71.58/18.31 thf(34,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : (((sk11 @ B @ (A)) != (sk11 @ B @ ((=) @ $i @ (sk11 @ B @ A)))) | ((sk11 @ B @ (A)) = D) | (~ (reli @ B @ C)) | (~ (reli @ C @ D)))),inference(lifteq,[status(thm)],[33])).
% 71.58/18.31 thf(29019,plain,(! [A:$i] : (~ (($true)) | (~ (reli @ sk6 @ sk8)) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ sk4 @ sk4)))),inference(paramod_ordered,[status(thm)],[1105,28772])).
% 71.58/18.31 thf(29020,plain,(! [A:$i] : ((~ (reli @ sk6 @ sk8)) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ sk4 @ sk4)))),inference(simp,[status(thm)],[29019])).
% 71.58/18.31 thf(29245,plain,(! [A:$i] : ((~ (reli @ sk6 @ sk8)) | (A != sk4) | ((sk10 @ A @ (^ [B:$i]: (($false)))) != sk4))),inference(simp,[status(thm)],[29020])).
% 71.58/18.31 thf(29308,plain,((~ (reli @ sk6 @ sk8)) | ((sk10 @ sk4 @ (^ [A:$i]: (($false)))) != sk4)),inference(simp,[status(thm)],[29245])).
% 71.58/18.31 thf(21,plain,(! [B:$i,A:($i > $o)] : ((~ ((sk9 @ B @ (A)) = (sk9 @ B @ ((=) @ $i @ (sk9 @ B @ A))))) | ((sk9 @ B @ (A)) = B))),inference(replace_leibeq,[status(thm)],[20:[bind(A, $thf((=) @ $i @ (sk9 @ B @ A)))]])).
% 71.58/18.31 thf(22,plain,(! [B:$i,A:($i > $o)] : (((sk9 @ B @ (A)) != (sk9 @ B @ ((=) @ $i @ (sk9 @ B @ A)))) | ((sk9 @ B @ (A)) = B))),inference(lifteq,[status(thm)],[21])).
% 71.58/18.31 thf(44,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((relr @ (sk13 @ B @ (A)) @ (sk14 @ B @ (A))) | (~ (relr @ B @ C)) | (~ (reli @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[42])).
% 71.58/18.31 thf(48,plain,(! [E:$i,D:individuals,C:$i,B:$i,A:$i] : (~ (($true)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (~ (reli @ C @ E)) | (sk1 @ D @ E) | ((reli @ sk7 @ sk8) != (reli @ sk3 @ A)))),inference(paramod_ordered,[status(thm)],[14,10])).
% 71.58/18.31 thf(49,plain,(! [E:$i,D:individuals,C:$i,B:$i,A:$i] : ((~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (~ (reli @ C @ E)) | (sk1 @ D @ E) | ((reli @ sk7 @ sk8) != (reli @ sk3 @ A)))),inference(simp,[status(thm)],[48])).
% 71.58/18.31 thf(77,plain,(! [E:$i,D:individuals,C:$i,B:$i,A:$i] : ((sk1 @ D @ E) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (~ (reli @ C @ E)) | (sk7 != sk3) | (sk8 != A))),inference(simp,[status(thm)],[49])).
% 71.58/18.31 thf(86,plain,(! [D:$i,C:individuals,B:$i,A:$i] : ((sk1 @ C @ D) | (~ (relr @ sk8 @ A)) | (~ (reli @ A @ B)) | (~ (reli @ B @ D)) | (sk7 != sk3))),inference(simp,[status(thm)],[77])).
% 71.58/18.31 thf(32670,plain,(! [A:$i] : ((~ (reli @ sk3 @ sk8)) | (~ (relr @ sk8 @ A)) | ~ (($true)) | ((reli @ sk2 @ sk3) != (reli @ A @ sk3)))),inference(paramod_ordered,[status(thm)],[16,115])).
% 71.58/18.31 thf(32671,plain,(! [A:$i] : ((~ (reli @ sk3 @ sk8)) | (~ (relr @ sk8 @ A)) | ((reli @ sk2 @ sk3) != (reli @ A @ sk3)))),inference(simp,[status(thm)],[32670])).
% 71.58/18.31 thf(32672,plain,((~ (reli @ sk3 @ sk8)) | (~ (relr @ sk8 @ sk2))),inference(pattern_uni,[status(thm)],[32671:[bind(A, $thf(sk2))]])).
% 71.58/18.31 thf(33154,plain,(~ (($true)) | (~ (relr @ sk8 @ sk2)) | ((reli @ sk3 @ sk8) != (reli @ sk3 @ sk4))),inference(paramod_ordered,[status(thm)],[15,32672])).
% 71.58/18.31 thf(33155,plain,((~ (relr @ sk8 @ sk2)) | ((reli @ sk3 @ sk8) != (reli @ sk3 @ sk4))),inference(simp,[status(thm)],[33154])).
% 71.58/18.31 thf(33184,plain,((~ (relr @ sk8 @ sk2)) | (sk3 != sk3) | (sk8 != sk4)),inference(simp,[status(thm)],[33155])).
% 71.58/18.31 thf(33279,plain,((~ (relr @ sk8 @ sk2)) | (sk8 != sk4)),inference(simp,[status(thm)],[33184])).
% 71.58/18.31 thf(253,plain,(! [A:$i] : ((reli @ A @ (sk9 @ A @ (prop_c))) | (prop_c @ A))),inference(prim_subst,[status(thm)],[19:[bind(A, $thf(prop_c))]])).
% 71.58/18.31 thf(318,plain,(! [A:$i] : ((reli @ A @ (sk9 @ A @ (prop_c))) | (prop_c @ A))),inference(simp,[status(thm)],[253])).
% 71.58/18.31 thf(29107,plain,((~ (relr @ sk4 @ sk4)) | ~ (($true)) | ((reli @ sk6 @ sk8) != (reli @ sk2 @ sk3))),inference(paramod_ordered,[status(thm)],[16,28772])).
% 71.58/18.31 thf(29108,plain,((~ (relr @ sk4 @ sk4)) | ((reli @ sk6 @ sk8) != (reli @ sk2 @ sk3))),inference(simp,[status(thm)],[29107])).
% 71.58/18.31 thf(29174,plain,((~ (relr @ sk4 @ sk4)) | (sk6 != sk2) | (sk8 != sk3)),inference(simp,[status(thm)],[29108])).
% 71.58/18.31 thf(726,plain,((reli @ sk7 @ (sk9 @ sk7 @ (relr @ sk4))) | (sk8 != sk7)),inference(pre_uni,[status(thm)],[722:[bind(A, $thf(relr @ sk4)),bind(B, $thf(sk7))]])).
% 71.58/18.31 thf(10732,plain,((reli @ sk7 @ (sk9 @ sk7 @ (relr @ sk4))) | (reli @ sk8 @ (sk9 @ sk8 @ (^ [A:$i]: (reli @ A @ A))))),inference(pre_uni,[status(thm)],[10675:[bind(A, $thf(relr @ sk4)),bind(B, $thf(sk7))]])).
% 71.58/18.31 thf(685,plain,((~ (relr @ sk4 @ sk7)) | ~ (($true)) | ((reli @ sk8 @ sk8) != (reli @ sk4 @ sk6))),inference(paramod_ordered,[status(thm)],[12,184])).
% 71.58/18.31 thf(686,plain,((~ (relr @ sk4 @ sk7)) | ((reli @ sk8 @ sk8) != (reli @ sk4 @ sk6))),inference(simp,[status(thm)],[685])).
% 71.58/18.31 thf(700,plain,((~ (relr @ sk4 @ sk7)) | (sk8 != sk4) | (sk8 != sk6)),inference(simp,[status(thm)],[686])).
% 71.58/18.31 thf(167,plain,(! [A:$i] : (~ (($true)) | (~ (relr @ A @ sk7)) | (~ (reli @ sk8 @ sk8)) | ((reli @ sk7 @ sk8) != (reli @ sk3 @ A)))),inference(paramod_ordered,[status(thm)],[14,92])).
% 71.58/18.31 thf(168,plain,(! [A:$i] : ((~ (relr @ A @ sk7)) | (~ (reli @ sk8 @ sk8)) | ((reli @ sk7 @ sk8) != (reli @ sk3 @ A)))),inference(simp,[status(thm)],[167])).
% 71.58/18.31 thf(192,plain,(! [A:$i] : ((~ (relr @ A @ sk7)) | (~ (reli @ sk8 @ sk8)) | (sk7 != sk3) | (sk8 != A))),inference(simp,[status(thm)],[168])).
% 71.58/18.31 thf(194,plain,((~ (relr @ sk8 @ sk7)) | (~ (reli @ sk8 @ sk8)) | (sk7 != sk3)),inference(simp,[status(thm)],[192])).
% 71.58/18.31 thf(3360,plain,((~ (relr @ sk8 @ sk7)) | ~ (($true)) | (sk7 != sk3) | ((reli @ sk8 @ sk8) != (reli @ sk7 @ sk8))),inference(paramod_ordered,[status(thm)],[14,194])).
% 71.58/18.31 thf(3361,plain,((~ (relr @ sk8 @ sk7)) | (sk7 != sk3) | ((reli @ sk8 @ sk8) != (reli @ sk7 @ sk8))),inference(simp,[status(thm)],[3360])).
% 71.58/18.31 thf(3445,plain,((~ (relr @ sk8 @ sk7)) | (sk7 != sk3) | (sk8 != sk7) | (sk8 != sk8)),inference(simp,[status(thm)],[3361])).
% 71.58/18.31 thf(3480,plain,((~ (relr @ sk8 @ sk7)) | (sk7 != sk3) | (sk8 != sk7)),inference(simp,[status(thm)],[3445])).
% 71.58/18.31 thf(416,plain,(~ (($true)) | (~ (reli @ sk8 @ sk8)) | ((reli @ sk4 @ sk6) != (reli @ sk3 @ sk6))),inference(paramod_ordered,[status(thm)],[12,181])).
% 71.58/18.31 thf(417,plain,((~ (reli @ sk8 @ sk8)) | ((reli @ sk4 @ sk6) != (reli @ sk3 @ sk6))),inference(simp,[status(thm)],[416])).
% 71.58/18.31 thf(421,plain,((~ (reli @ sk8 @ sk8)) | (sk4 != sk3) | (sk6 != sk6)),inference(simp,[status(thm)],[417])).
% 71.58/18.31 thf(444,plain,((~ (reli @ sk8 @ sk8)) | (sk4 != sk3)),inference(simp,[status(thm)],[421])).
% 71.58/18.31 thf(464,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | ~ (($true)) | (sk4 != sk3) | ((A @ B) != (reli @ sk8 @ sk8)))),inference(paramod_ordered,[status(thm)],[19,444])).
% 71.58/18.31 thf(465,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | (sk4 != sk3) | ((A @ B) != (reli @ sk8 @ sk8)))),inference(simp,[status(thm)],[464])).
% 71.58/18.31 thf(475,plain,((reli @ sk8 @ (sk9 @ sk8 @ (reli @ sk8))) | (sk4 != sk3)),inference(pre_uni,[status(thm)],[465:[bind(A, $thf(reli @ sk8)),bind(B, $thf(sk8))]])).
% 71.58/18.31 thf(4539,plain,(! [B:$i,A:($i > $o)] : ((sk4 != sk3) | ~ (($true)) | (A @ B) | ((reli @ sk8 @ (sk9 @ sk8 @ (reli @ sk8))) != (A @ (sk9 @ B @ (A)))))),inference(paramod_ordered,[status(thm)],[475,20])).
% 71.58/18.31 thf(4540,plain,(! [B:$i,A:($i > $o)] : ((sk4 != sk3) | (A @ B) | ((reli @ sk8 @ (sk9 @ sk8 @ (reli @ sk8))) != (A @ (sk9 @ B @ (A)))))),inference(simp,[status(thm)],[4539])).
% 71.58/18.31 thf(4606,plain,((sk4 != sk3) | (reli @ sk8 @ sk8)),inference(pre_uni,[status(thm)],[4540:[bind(A, $thf(reli @ sk8)),bind(B, $thf(sk8))]])).
% 71.58/18.31 thf(4952,plain,((sk4 != sk3) | ~ (($true)) | (sk4 != sk3) | ((reli @ sk8 @ sk8) != (reli @ sk8 @ sk8))),inference(paramod_ordered,[status(thm)],[4606,444])).
% 71.58/18.31 thf(4953,plain,((sk4 != sk3) | ((reli @ sk8 @ sk8) != (reli @ sk8 @ sk8))),inference(simp,[status(thm)],[4952])).
% 71.58/18.31 thf(4954,plain,((sk4 != sk3)),inference(pattern_uni,[status(thm)],[4953:[]])).
% 71.58/18.31 thf(1034,plain,((relr @ sk7 @ (sk10 @ sk7 @ (relr @ sk4))) | (sk8 != sk7)),inference(pre_uni,[status(thm)],[998:[bind(A, $thf(relr @ sk4)),bind(B, $thf(sk7))]])).
% 71.58/18.31 thf(23030,plain,(! [A:$i] : ((prop_c @ A) | ~ (($true)) | ((reli @ A @ (sk9 @ A @ (prop_c))) != (reli @ sk3 @ sk6)))),inference(paramod_ordered,[status(thm)],[318,22706])).
% 71.58/18.31 thf(23031,plain,(! [A:$i] : ((prop_c @ A) | ((reli @ A @ (sk9 @ A @ (prop_c))) != (reli @ sk3 @ sk6)))),inference(simp,[status(thm)],[23030])).
% 71.58/18.31 thf(23124,plain,(! [A:$i] : ((prop_c @ A) | (A != sk3) | ((sk9 @ A @ (prop_c)) != sk6))),inference(simp,[status(thm)],[23031])).
% 71.58/18.31 thf(23168,plain,((prop_c @ sk3) | ((sk9 @ sk3 @ (prop_c)) != sk6)),inference(simp,[status(thm)],[23124])).
% 71.58/18.31 thf(15963,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk10 @ B @ (A))) | (relr @ sk8 @ (sk10 @ sk8 @ (^ [C:$i]: (reli @ C @ C)))) | ~ (($true)) | ((A @ B) != (relr @ sk4 @ sk7)))),inference(paramod_ordered,[status(thm)],[25,1086])).
% 71.58/18.31 thf(15964,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk10 @ B @ (A))) | (relr @ sk8 @ (sk10 @ sk8 @ (^ [C:$i]: (reli @ C @ C)))) | ((A @ B) != (relr @ sk4 @ sk7)))),inference(simp,[status(thm)],[15963])).
% 71.58/18.31 thf(16148,plain,((relr @ sk4 @ (sk10 @ sk4 @ (^ [A:$i]: (relr @ A @ sk7)))) | (relr @ sk8 @ (sk10 @ sk8 @ (^ [A:$i]: (reli @ A @ A))))),inference(pre_uni,[status(thm)],[15964:[bind(A, $thf(^ [C:$i]: (relr @ C @ sk7))),bind(B, $thf(sk4))]])).
% 71.58/18.31 thf(93,plain,(! [C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | ~ (($true)) | ((reli @ sk7 @ sk8) != (reli @ C @ sk8)))),inference(paramod_ordered,[status(thm)],[14,58])).
% 71.58/18.31 thf(94,plain,(! [C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | ((reli @ sk7 @ sk8) != (reli @ C @ sk8)))),inference(simp,[status(thm)],[93])).
% 71.58/18.31 thf(95,plain,(! [B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ sk7)))),inference(pattern_uni,[status(thm)],[94:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(sk7))]])).
% 71.58/18.31 thf(29388,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | ~ (($true)) | (sk7 != sk6) | ((A @ B) != (relr @ sk4 @ sk4)))),inference(paramod_ordered,[status(thm)],[19,29300])).
% 71.58/18.31 thf(29389,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk9 @ B @ (A))) | (sk7 != sk6) | ((A @ B) != (relr @ sk4 @ sk4)))),inference(simp,[status(thm)],[29388])).
% 71.58/18.31 thf(29437,plain,((reli @ sk4 @ (sk9 @ sk4 @ (^ [A:$i]: (relr @ A @ A)))) | (sk7 != sk6)),inference(pre_uni,[status(thm)],[29389:[bind(A, $thf(^ [C:$i]: (relr @ C @ C))),bind(B, $thf(sk4))]])).
% 71.58/18.31 thf(681,plain,((~ (relr @ sk4 @ sk7)) | ~ (($true)) | ((reli @ sk8 @ (sk9 @ sk8 @ (sk1 @ sk5))) != (reli @ sk8 @ sk8))),inference(paramod_ordered,[status(thm)],[280,184])).
% 71.58/18.31 thf(682,plain,((~ (relr @ sk4 @ sk7)) | ((reli @ sk8 @ (sk9 @ sk8 @ (sk1 @ sk5))) != (reli @ sk8 @ sk8))),inference(simp,[status(thm)],[681])).
% 71.58/18.31 thf(699,plain,((~ (relr @ sk4 @ sk7)) | (sk8 != sk8) | ((sk9 @ sk8 @ (sk1 @ sk5)) != sk8)),inference(simp,[status(thm)],[682])).
% 71.58/18.31 thf(717,plain,((~ (relr @ sk4 @ sk7)) | ((sk9 @ sk8 @ (sk1 @ sk5)) != sk8)),inference(simp,[status(thm)],[699])).
% 71.58/18.31 thf(248,plain,(! [A:$i] : ((reli @ A @ (sk9 @ A @ (prop_b))) | (prop_b @ A))),inference(prim_subst,[status(thm)],[19:[bind(A, $thf(prop_b))]])).
% 71.58/18.31 thf(314,plain,(! [A:$i] : ((reli @ A @ (sk9 @ A @ (prop_b))) | (prop_b @ A))),inference(simp,[status(thm)],[248])).
% 71.58/18.31 thf(23052,plain,(! [A:$i] : ((prop_b @ A) | ~ (($true)) | ((reli @ A @ (sk9 @ A @ (prop_b))) != (reli @ sk3 @ sk6)))),inference(paramod_ordered,[status(thm)],[314,22706])).
% 71.58/18.31 thf(23053,plain,(! [A:$i] : ((prop_b @ A) | ((reli @ A @ (sk9 @ A @ (prop_b))) != (reli @ sk3 @ sk6)))),inference(simp,[status(thm)],[23052])).
% 71.58/18.31 thf(23078,plain,(! [A:$i] : ((prop_b @ A) | (A != sk3) | ((sk9 @ A @ (prop_b)) != sk6))),inference(simp,[status(thm)],[23053])).
% 71.58/18.31 thf(23138,plain,((prop_b @ sk3) | ((sk9 @ sk3 @ (prop_b)) != sk6)),inference(simp,[status(thm)],[23078])).
% 71.58/18.31 thf(31,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk11 @ B @ (A))) | (~ (reli @ B @ C)) | (~ (reli @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[30])).
% 71.58/18.31 thf(43,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk13 @ B @ (A))) | (~ (relr @ B @ C)) | (~ (reli @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[42])).
% 71.58/18.31 thf(61,plain,(! [E:$i,D:individuals,C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | ~ (($true)) | (~ (reli @ C @ E)) | (sk1 @ D @ E) | ((reli @ sk4 @ sk6) != (reli @ B @ C)))),inference(paramod_ordered,[status(thm)],[12,10])).
% 71.58/18.31 thf(62,plain,(! [E:$i,D:individuals,C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ C @ E)) | (sk1 @ D @ E) | ((reli @ sk4 @ sk6) != (reli @ B @ C)))),inference(simp,[status(thm)],[61])).
% 71.58/18.31 thf(63,plain,(! [C:$i,B:individuals,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ sk4)) | (~ (reli @ sk6 @ C)) | (sk1 @ B @ C))),inference(pattern_uni,[status(thm)],[62:[bind(A, $thf(A)),bind(B, $thf(sk4)),bind(C, $thf(sk6))]])).
% 71.58/18.31 thf(87,plain,(! [C:$i,B:individuals,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ sk4)) | (~ (reli @ sk6 @ C)) | (sk1 @ B @ C))),inference(simp,[status(thm)],[63])).
% 71.58/18.31 thf(33026,plain,(~ (($true)) | (~ (relr @ sk8 @ sk2)) | ((reli @ sk7 @ sk8) != (reli @ sk3 @ sk8))),inference(paramod_ordered,[status(thm)],[14,32672])).
% 71.58/18.31 thf(33027,plain,((~ (relr @ sk8 @ sk2)) | ((reli @ sk7 @ sk8) != (reli @ sk3 @ sk8))),inference(simp,[status(thm)],[33026])).
% 71.58/18.31 thf(33202,plain,((~ (relr @ sk8 @ sk2)) | (sk7 != sk3) | (sk8 != sk8)),inference(simp,[status(thm)],[33027])).
% 71.58/18.31 thf(33293,plain,((~ (relr @ sk8 @ sk2)) | (sk7 != sk3)),inference(simp,[status(thm)],[33202])).
% 71.58/18.31 thf(31107,plain,(! [A:$i] : (~ (($true)) | (sk8 != sk7) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ sk4 @ sk8)))),inference(paramod_ordered,[status(thm)],[1105,31084])).
% 71.58/18.31 thf(31108,plain,(! [A:$i] : ((sk8 != sk7) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ sk4 @ sk8)))),inference(simp,[status(thm)],[31107])).
% 71.58/18.31 thf(31203,plain,(! [A:$i] : ((sk8 != sk7) | (A != sk4) | ((sk10 @ A @ (^ [B:$i]: (($false)))) != sk8))),inference(simp,[status(thm)],[31108])).
% 71.58/18.31 thf(31238,plain,((sk8 != sk7) | ((sk10 @ sk4 @ (^ [A:$i]: (($false)))) != sk8)),inference(simp,[status(thm)],[31203])).
% 71.58/18.31 thf(1277,plain,(! [A:$i] : ((prop_c @ A) | ~ (($true)) | (sk8 != sk7) | ((relr @ A @ (sk10 @ A @ (prop_c))) != (relr @ sk4 @ sk7)))),inference(paramod_ordered,[status(thm)],[1103,711])).
% 71.58/18.31 thf(1278,plain,(! [A:$i] : ((prop_c @ A) | (sk8 != sk7) | ((relr @ A @ (sk10 @ A @ (prop_c))) != (relr @ sk4 @ sk7)))),inference(simp,[status(thm)],[1277])).
% 71.58/18.31 thf(1283,plain,(! [A:$i] : ((prop_c @ A) | (sk8 != sk7) | (A != sk4) | ((sk10 @ A @ (prop_c)) != sk7))),inference(simp,[status(thm)],[1278])).
% 71.58/18.31 thf(1289,plain,((prop_c @ sk4) | (sk8 != sk7) | ((sk10 @ sk4 @ (prop_c)) != sk7)),inference(simp,[status(thm)],[1283])).
% 71.58/18.31 thf(29153,plain,((~ (relr @ sk4 @ sk4)) | ~ (($true)) | ((reli @ sk6 @ sk8) != (reli @ sk3 @ sk4))),inference(paramod_ordered,[status(thm)],[15,28772])).
% 71.58/18.31 thf(29154,plain,((~ (relr @ sk4 @ sk4)) | ((reli @ sk6 @ sk8) != (reli @ sk3 @ sk4))),inference(simp,[status(thm)],[29153])).
% 71.58/18.31 thf(29251,plain,((~ (relr @ sk4 @ sk4)) | (sk6 != sk3) | (sk8 != sk4)),inference(simp,[status(thm)],[29154])).
% 71.58/18.31 thf(23232,plain,(~ (($true)) | ((reli @ sk3 @ (sk9 @ sk3 @ (^ [A:$i]: (reli @ A @ sk6)))) != (reli @ sk3 @ sk6))),inference(paramod_ordered,[status(thm)],[23115,22706])).
% 71.58/18.31 thf(23233,plain,(((reli @ sk3 @ (sk9 @ sk3 @ (^ [A:$i]: (reli @ A @ sk6)))) != (reli @ sk3 @ sk6))),inference(simp,[status(thm)],[23232])).
% 71.58/18.31 thf(23339,plain,((sk3 != sk3) | ((sk9 @ sk3 @ (^ [A:$i]: (reli @ A @ sk6))) != sk6)),inference(simp,[status(thm)],[23233])).
% 71.58/18.31 thf(23360,plain,(((sk9 @ sk3 @ (^ [A:$i]: (reli @ A @ sk6))) != sk6)),inference(simp,[status(thm)],[23339])).
% 71.58/18.31 thf(39,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ ((sk12 @ B @ (A)) = (sk12 @ B @ ((=) @ $i @ (sk12 @ B @ A))))) | (~ (relr @ B @ C)) | (~ (relr @ C @ D)) | ((sk12 @ B @ (A)) = D))),inference(replace_leibeq,[status(thm)],[38:[bind(A, $thf((=) @ $i @ (sk12 @ B @ A)))]])).
% 71.58/18.31 thf(40,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : (((sk12 @ B @ (A)) != (sk12 @ B @ ((=) @ $i @ (sk12 @ B @ A)))) | ((sk12 @ B @ (A)) = D) | (~ (relr @ B @ C)) | (~ (relr @ C @ D)))),inference(lifteq,[status(thm)],[39])).
% 71.58/18.31 thf(29129,plain,(! [A:$i] : ((~ (relr @ sk4 @ sk4)) | ~ (($true)) | ((reli @ A @ (sk9 @ A @ (^ [B:$i]: (($false))))) != (reli @ sk6 @ sk8)))),inference(paramod_ordered,[status(thm)],[319,28772])).
% 71.58/18.31 thf(29130,plain,(! [A:$i] : ((~ (relr @ sk4 @ sk4)) | ((reli @ A @ (sk9 @ A @ (^ [B:$i]: (($false))))) != (reli @ sk6 @ sk8)))),inference(simp,[status(thm)],[29129])).
% 71.58/18.31 thf(29231,plain,(! [A:$i] : ((~ (relr @ sk4 @ sk4)) | (A != sk6) | ((sk9 @ A @ (^ [B:$i]: (($false)))) != sk8))),inference(simp,[status(thm)],[29130])).
% 71.58/18.31 thf(29295,plain,((~ (relr @ sk4 @ sk4)) | ((sk9 @ sk6 @ (^ [A:$i]: (($false)))) != sk8)),inference(simp,[status(thm)],[29231])).
% 71.58/18.31 thf(16149,plain,((relr @ sk7 @ (sk10 @ sk7 @ (relr @ sk4))) | (relr @ sk8 @ (sk10 @ sk8 @ (^ [A:$i]: (reli @ A @ A))))),inference(pre_uni,[status(thm)],[15964:[bind(A, $thf(relr @ sk4)),bind(B, $thf(sk7))]])).
% 71.58/18.31 thf(1862,plain,(! [A:$i] : (~ (($true)) | ((sk9 @ sk8 @ (^ [B:$i]: (($false)))) != sk8) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ sk4 @ sk7)))),inference(paramod_ordered,[status(thm)],[1105,715])).
% 71.58/18.31 thf(1863,plain,(! [A:$i] : (((sk9 @ sk8 @ (^ [B:$i]: (($false)))) != sk8) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ sk4 @ sk7)))),inference(simp,[status(thm)],[1862])).
% 71.58/18.31 thf(1890,plain,(! [A:$i] : (((sk9 @ sk8 @ (^ [B:$i]: (($false)))) != sk8) | (A != sk4) | ((sk10 @ A @ (^ [B:$i]: (($false)))) != sk7))),inference(simp,[status(thm)],[1863])).
% 71.58/18.31 thf(1893,plain,(((sk9 @ sk8 @ (^ [A:$i]: (($false)))) != sk8) | ((sk10 @ sk4 @ (^ [A:$i]: (($false)))) != sk7)),inference(simp,[status(thm)],[1890])).
% 71.58/18.31 thf(23888,plain,(~ (($true)) | ((reli @ sk6 @ (sk9 @ sk6 @ (reli @ sk3))) != (reli @ sk3 @ sk6))),inference(paramod_ordered,[status(thm)],[23116,22706])).
% 71.58/18.31 thf(23889,plain,(((reli @ sk6 @ (sk9 @ sk6 @ (reli @ sk3))) != (reli @ sk3 @ sk6))),inference(simp,[status(thm)],[23888])).
% 71.58/18.31 thf(23987,plain,((sk6 != sk3) | ((sk9 @ sk6 @ (reli @ sk3)) != sk6)),inference(simp,[status(thm)],[23889])).
% 71.58/18.31 thf(16145,plain,((reli @ sk7 @ (sk9 @ sk7 @ (relr @ sk4))) | (relr @ sk8 @ (sk10 @ sk8 @ (^ [A:$i]: (reli @ A @ A))))),inference(pre_uni,[status(thm)],[16070:[bind(A, $thf(relr @ sk4)),bind(B, $thf(sk7))]])).
% 71.58/18.31 thf(23046,plain,(~ (($true)) | ((reli @ sk3 @ sk6) != (reli @ sk2 @ sk3))),inference(paramod_ordered,[status(thm)],[16,22706])).
% 71.58/18.31 thf(23047,plain,(((reli @ sk3 @ sk6) != (reli @ sk2 @ sk3))),inference(simp,[status(thm)],[23046])).
% 71.58/18.31 thf(23088,plain,((sk3 != sk2) | (sk6 != sk3)),inference(simp,[status(thm)],[23047])).
% 71.58/18.31 thf(696,plain,((reli @ sk4 @ (sk9 @ sk4 @ (^ [A:$i]: (relr @ A @ sk7)))) | (~ (reli @ sk8 @ sk8))),inference(pre_uni,[status(thm)],[692:[bind(A, $thf(^ [C:$i]: (relr @ C @ sk7))),bind(B, $thf(sk4))]])).
% 71.58/18.31 thf(50,plain,(! [E:$i,D:individuals,C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | ~ (($true)) | (~ (reli @ C @ E)) | (sk1 @ D @ E) | ((reli @ sk7 @ sk8) != (reli @ B @ C)))),inference(paramod_ordered,[status(thm)],[14,10])).
% 71.58/18.31 thf(51,plain,(! [E:$i,D:individuals,C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ C @ E)) | (sk1 @ D @ E) | ((reli @ sk7 @ sk8) != (reli @ B @ C)))),inference(simp,[status(thm)],[50])).
% 71.58/18.31 thf(52,plain,(! [C:$i,B:individuals,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ sk7)) | (~ (reli @ sk8 @ C)) | (sk1 @ B @ C))),inference(pattern_uni,[status(thm)],[51:[bind(A, $thf(A)),bind(B, $thf(sk7)),bind(C, $thf(sk8))]])).
% 71.58/18.31 thf(79,plain,(! [C:$i,B:individuals,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ sk7)) | (~ (reli @ sk8 @ C)) | (sk1 @ B @ C))),inference(simp,[status(thm)],[52])).
% 71.58/18.31 thf(32378,plain,((sk7 != sk6) | ~ (($true)) | (sk7 != sk6) | ((relr @ sk4 @ (sk10 @ sk4 @ (^ [A:$i]: (relr @ A @ A)))) != (relr @ sk4 @ sk4))),inference(paramod_ordered,[status(thm)],[29444,29300])).
% 71.58/18.31 thf(32379,plain,((sk7 != sk6) | ((relr @ sk4 @ (sk10 @ sk4 @ (^ [A:$i]: (relr @ A @ A)))) != (relr @ sk4 @ sk4))),inference(simp,[status(thm)],[32378])).
% 71.58/18.31 thf(32433,plain,((sk7 != sk6) | (sk4 != sk4) | ((sk10 @ sk4 @ (^ [A:$i]: (relr @ A @ A))) != sk4)),inference(simp,[status(thm)],[32379])).
% 71.58/18.31 thf(32478,plain,((sk7 != sk6) | ((sk10 @ sk4 @ (^ [A:$i]: (relr @ A @ A))) != sk4)),inference(simp,[status(thm)],[32433])).
% 71.58/18.31 thf(46,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ ((sk14 @ B @ (A)) = (sk14 @ B @ ((=) @ $i @ (sk14 @ B @ A))))) | (~ (relr @ B @ C)) | (~ (reli @ C @ D)) | ((sk14 @ B @ (A)) = D))),inference(replace_leibeq,[status(thm)],[45:[bind(A, $thf((=) @ $i @ (sk14 @ B @ A)))]])).
% 71.58/18.31 thf(47,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : (((sk14 @ B @ (A)) != (sk14 @ B @ ((=) @ $i @ (sk14 @ B @ A)))) | ((sk14 @ B @ (A)) = D) | (~ (relr @ B @ C)) | (~ (reli @ C @ D)))),inference(lifteq,[status(thm)],[46])).
% 71.58/18.31 thf(70,plain,(! [E:$i,D:individuals,C:$i,B:$i,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ C @ E)) | (sk1 @ D @ E) | ((reli @ B @ C) != (reli @ sk3 @ A)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[10])).
% 71.58/18.31 thf(74,plain,(! [C:$i,B:individuals,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ sk3)) | (~ (reli @ A @ C)) | (sk1 @ B @ C))),inference(pattern_uni,[status(thm)],[70:[bind(A, $thf(C)),bind(B, $thf(sk3))]])).
% 71.58/18.31 thf(83,plain,(! [C:$i,B:individuals,A:$i] : ((~ (reli @ sk3 @ A)) | (~ (relr @ A @ sk3)) | (~ (reli @ A @ C)) | (sk1 @ B @ C))),inference(simp,[status(thm)],[74])).
% 71.58/18.31 thf(29336,plain,(! [A:$i] : (~ (($true)) | (sk7 != sk6) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ sk4 @ sk4)))),inference(paramod_ordered,[status(thm)],[1105,29300])).
% 71.58/18.31 thf(29337,plain,(! [A:$i] : ((sk7 != sk6) | ((relr @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))) != (relr @ sk4 @ sk4)))),inference(simp,[status(thm)],[29336])).
% 71.58/18.31 thf(29408,plain,(! [A:$i] : ((sk7 != sk6) | (A != sk4) | ((sk10 @ A @ (^ [B:$i]: (($false)))) != sk4))),inference(simp,[status(thm)],[29337])).
% 71.58/18.31 thf(29466,plain,((sk7 != sk6) | ((sk10 @ sk4 @ (^ [A:$i]: (($false)))) != sk4)),inference(simp,[status(thm)],[29408])).
% 71.58/18.31 thf(38591,plain,(($false)),inference(e,[status(thm)],[1086,1105,2595,10753,115,31084,2837,10,2035,22706,715,698,10698,37,25,14,184,23123,12606,196,2745,20,10891,78,29,27067,23115,6841,84,280,1201,312,28772,85,23131,1047,23081,10699,23143,23116,29444,2606,28,38,92,1106,697,1983,7205,10731,725,16144,23154,1739,1207,701,13,41,23122,1103,45,32,34,17,29308,22,44,711,12,86,33279,318,29174,726,10732,700,3480,4954,32672,35,1034,23168,112,16148,194,95,705,29437,16,717,23138,31,29300,703,11,314,43,87,30500,33293,31238,1289,1108,29251,23360,319,40,26,29295,23,8,58,16149,1893,23987,19,16145,23088,1033,696,79,32478,47,15,83,364,100,29466])).
% 71.58/18.31 % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 71.58/18.31 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------