%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : LCL690^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:14:09 AM UTC 2026
% Result : Theorem 91.64s 20.84s
% Output : Refutation 89.08s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL690^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.07 % 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.10/0.21 % Computer : n016.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Tue Sep 29 09:38:49 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/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.86/0.79 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.60/1.03 % [INFO] Parsing done (239ms).
% 1.60/1.05 % [INFO] Running in sequential loop mode.
% 2.17/1.45 % [INFO] eprover registered as external prover.
% 2.17/1.45 % [INFO] Scanning for conjecture ...
% 2.55/1.60 % [INFO] Found a conjecture (or negated_conjecture) and 5 axioms. Running axiom selection ...
% 2.55/1.63 % [INFO] Axiom selection finished. Selected 5 axioms (removed 0 axioms).
% 2.55/1.64 % [INFO] Problem is higher-order (TPTP THF).
% 2.55/1.65 % [INFO] Type checking passed.
% 2.55/1.65 % [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 ...
% 91.64/20.84 % External prover 'e' found a proof!
% 91.64/20.84 % [INFO] Killing All external provers ...
% 91.64/20.84 % Time passed: 20480ms (effective reasoning time: 19785ms)
% 91.64/20.84 % 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)>
% 91.64/20.84 % Axioms used in derivation (5): trans_axiom_i, trans_axiom_r, refl_axiom_r, ax_i_r_commute, refl_axiom_i
% 91.64/20.84 % No. of inferences in proof: 204
% 91.64/20.84 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 20480 ms resp. 19785 ms w/o parsing
% 89.08/20.98 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 89.08/20.98 thf(individuals_type, type, individuals: $tType).
% 89.08/20.98 thf(prop_a_decl, type, prop_a: ($i > $o)).
% 89.08/20.98 thf(prop_b_decl, type, prop_b: ($i > $o)).
% 89.08/20.98 thf(prop_c_decl, type, prop_c: ($i > $o)).
% 89.08/20.98 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 89.08/20.98 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 89.08/20.98 thf(mimpl_decl, type, mimpl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 89.08/20.98 thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 89.08/20.98 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 89.08/20.98 thf(reli_decl, type, reli: ($i > ($i > $o))).
% 89.08/20.98 thf(relr_decl, type, relr: ($i > ($i > $o))).
% 89.08/20.98 thf(cs4_atom_decl, type, cs4_atom: (($i > $o) > ($i > $o))).
% 89.08/20.98 thf(cs4_impl_decl, type, cs4_impl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 89.08/20.98 thf(cs4_box_decl, type, cs4_box: (($i > $o) > ($i > $o))).
% 89.08/20.98 thf(cs4_valid_decl, type, cs4_valid: (($i > $o) > $o)).
% 89.08/20.98 thf(sk1_decl, type, sk1: ($i > $o)).
% 89.08/20.98 thf(sk2_decl, type, sk2: ($i > $o)).
% 89.08/20.98 thf(sk3_decl, type, sk3: $i).
% 89.08/20.98 thf(sk4_decl, type, sk4: $i).
% 89.08/20.99 thf(sk5_decl, type, sk5: ($i > ($i > ($i > $i)))).
% 89.08/20.99 thf(sk6_decl, type, sk6: $i).
% 89.08/20.99 thf(sk7_decl, type, sk7: $i).
% 89.08/20.99 thf(sk8_decl, type, sk8: $i).
% 89.08/20.99 thf(sk9_decl, type, sk9: $i).
% 89.08/20.99 thf(sk10_decl, type, sk10: ($i > (($i > $o) > $i))).
% 89.08/20.99 thf(sk11_decl, type, sk11: ($i > (($i > $o) > $i))).
% 89.08/20.99 thf(sk12_decl, type, sk12: ($i > (($i > $o) > $i))).
% 89.08/20.99 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 89.08/20.99 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 89.08/20.99 thf(mimpl_def, definition, mimpl = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 89.08/20.99 thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: ((A @ C @ D) => (B @ D))) ).
% 89.08/20.99 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 89.08/20.99 thf(cs4_atom_def, definition, cs4_atom = (mbox @ reli) ).
% 89.08/20.99 thf(cs4_impl_def, definition, cs4_impl = (^ [A:($i > $o),B:($i > $o)]: (mbox @ reli @ (mimpl @ A @ B))) ).
% 89.08/20.99 thf(cs4_box_def, definition, cs4_box = (^ [A:($i > $o)]: (mbox @ reli @ (mbox @ relr @ A))) ).
% 89.08/20.99 thf(cs4_valid_def, definition, cs4_valid = (mvalid) ).
% 89.08/20.99 thf(sk1_def, definition, sk1 = (@+ [A:($i > $o)]: ~ (! [B:($i > $o),C:$i,D:$i]: ((reli @ C @ D) => (~ (! [E:$i]: ((reli @ D @ E) => (! [F:$i]: ((relr @ E @ F) => (! [G:$i]: ((reli @ F @ G) => (~ (! [H:$i]: ((reli @ G @ H) => (A @ H))) | ! [H:$i]: ((reli @ G @ H) => (B @ H))))))))) | ! [E:$i]: ((reli @ D @ E) => (~ (! [F:$i]: ((reli @ E @ F) => (! [G:$i]: ((relr @ F @ G) => (! [H:$i]: ((reli @ G @ H) => (A @ H))))))) | ! [F:$i]: ((reli @ E @ F) => (! [G:$i]: ((relr @ F @ G) => (! [H:$i]: ((reli @ G @ H) => (B @ H)))))))))))) ).
% 89.08/20.99 thf(sk2_def, definition, sk2 = (@+ [A:($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:$i]: ((reli @ F @ G) => (sk1 @ G))) | ! [G:$i]: ((reli @ F @ G) => (A @ G))))))))) | ! [D:$i]: ((reli @ C @ D) => (~ (! [E:$i]: ((reli @ D @ E) => (! [F:$i]: ((relr @ E @ F) => (! [G:$i]: ((reli @ F @ G) => (sk1 @ G))))))) | ! [E:$i]: ((reli @ D @ E) => (! [F:$i]: ((relr @ E @ F) => (! [G:$i]: ((reli @ F @ G) => (A @ G)))))))))))) ).
% 89.08/20.99 thf(sk3_def, definition, sk3 = (@+ [A:$i]: ~ (! [B:$i]: ((reli @ A @ B) => (~ (! [C:$i]: ((reli @ B @ C) => (! [D:$i]: ((relr @ C @ D) => (! [E:$i]: ((reli @ D @ E) => (~ (! [F:$i]: ((reli @ E @ F) => (sk1 @ F))) | ! [F:$i]: ((reli @ E @ F) => (sk2 @ F))))))))) | ! [C:$i]: ((reli @ B @ C) => (~ (! [D:$i]: ((reli @ C @ D) => (! [E:$i]: ((relr @ D @ E) => (! [F:$i]: ((reli @ E @ F) => (sk1 @ F))))))) | ! [D:$i]: ((reli @ C @ D) => (! [E:$i]: ((relr @ D @ E) => (! [F:$i]: ((reli @ E @ F) => (sk2 @ F)))))))))))) ).
% 89.08/20.99 thf(sk4_def, definition, sk4 = (@+ [A:$i]: ~ ((reli @ sk3 @ A) => (~ (! [B:$i]: ((reli @ A @ B) => (! [C:$i]: ((relr @ B @ C) => (! [D:$i]: ((reli @ C @ D) => (~ (! [E:$i]: ((reli @ D @ E) => (sk1 @ E))) | ! [E:$i]: ((reli @ D @ E) => (sk2 @ E))))))))) | ! [B:$i]: ((reli @ A @ B) => (~ (! [C:$i]: ((reli @ B @ C) => (! [D:$i]: ((relr @ C @ D) => (! [E:$i]: ((reli @ D @ E) => (sk1 @ E))))))) | ! [C:$i]: ((reli @ B @ C) => (! [D:$i]: ((relr @ C @ D) => (! [E:$i]: ((reli @ D @ E) => (sk2 @ E))))))))))) ).
% 89.08/20.99 thf(sk5_def, definition, sk5 = (^ [A:$i,B:$i,C:$i]: (@+ [D:$i]: ~ ((reli @ A @ D) => (sk1 @ D)))) ).
% 89.08/20.99 thf(sk6_def, definition, sk6 = (@+ [A:$i]: ~ ((reli @ sk4 @ A) => (~ (! [B:$i]: ((reli @ A @ B) => (! [C:$i]: ((relr @ B @ C) => (! [D:$i]: ((reli @ C @ D) => (sk1 @ D))))))) | ! [B:$i]: ((reli @ A @ B) => (! [C:$i]: ((relr @ B @ C) => (! [D:$i]: ((reli @ C @ D) => (sk2 @ D))))))))) ).
% 89.08/20.99 thf(sk7_def, definition, sk7 = (@+ [A:$i]: ~ ((reli @ sk6 @ A) => (! [B:$i]: ((relr @ A @ B) => (! [C:$i]: ((reli @ B @ C) => (sk2 @ C))))))) ).
% 89.08/20.99 thf(sk8_def, definition, sk8 = (@+ [A:$i]: ~ ((relr @ sk7 @ A) => (! [B:$i]: ((reli @ A @ B) => (sk2 @ B))))) ).
% 89.08/20.99 thf(sk9_def, definition, sk9 = (@+ [A:$i]: ~ ((reli @ sk8 @ A) => (sk2 @ A))) ).
% 89.08/20.99 thf(sk10_def, definition, sk10 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((reli @ A @ C) => (B @ C)))) ).
% 89.08/20.99 thf(sk11_def, definition, sk11 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((relr @ A @ C) => (B @ C)))) ).
% 89.08/20.99 thf(sk12_def, definition, sk12 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((reli @ A @ C) => (B @ C)))) ).
% 89.08/20.99 thf(1,conjecture,((! [A:($i > $o),B:($i > $o)]: (cs4_valid @ (cs4_impl @ (cs4_box @ (cs4_impl @ (cs4_atom @ A) @ (cs4_atom @ B))) @ (cs4_impl @ (cs4_box @ (cs4_atom @ A)) @ (cs4_box @ (cs4_atom @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',cs4_k)).
% 89.08/20.99 thf(2,negated_conjecture,((~ (! [A:($i > $o),B:($i > $o)]: (cs4_valid @ (cs4_impl @ (cs4_box @ (cs4_impl @ (cs4_atom @ A) @ (cs4_atom @ B))) @ (cs4_impl @ (cs4_box @ (cs4_atom @ A)) @ (cs4_box @ (cs4_atom @ B)))))))),inference(neg_conjecture,[status(cth)],[1])).
% 89.08/20.99 thf(8,plain,((~ (! [A:($i > $o),B:($i > $o),C:$i,D:$i]: ((reli @ C @ D) => (~ (! [E:$i]: ((reli @ D @ E) => (! [F:$i]: ((relr @ E @ F) => (! [G:$i]: ((reli @ F @ G) => (~ (! [H:$i]: ((reli @ G @ H) => (A @ H))) | ! [H:$i]: ((reli @ G @ H) => (B @ H))))))))) | ! [E:$i]: ((reli @ D @ E) => (~ (! [F:$i]: ((reli @ E @ F) => (! [G:$i]: ((relr @ F @ G) => (! [H:$i]: ((reli @ G @ H) => (A @ H))))))) | ! [F:$i]: ((reli @ E @ F) => (! [G:$i]: ((relr @ F @ G) => (! [H:$i]: ((reli @ G @ H) => (B @ H))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 89.08/20.99 thf(9,plain,(! [G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : (((reli @ sk3 @ sk4) & (~ (reli @ sk4 @ A) | ~ (relr @ A @ B) | ~ (reli @ B @ C) | (reli @ C @ (sk5 @ C @ B @ A)) | ~ (reli @ C @ D) | (sk2 @ D)) & (~ (reli @ sk4 @ A) | ~ (relr @ A @ B) | ~ (reli @ B @ C) | ~ (sk1 @ (sk5 @ C @ B @ A)) | ~ (reli @ C @ D) | (sk2 @ D)) & (reli @ sk4 @ sk6) & (~ (reli @ sk6 @ E) | ~ (relr @ E @ F) | ~ (reli @ F @ G) | (sk1 @ G)) & (reli @ sk6 @ sk7) & (relr @ sk7 @ sk8) & (reli @ sk8 @ sk9) & ~ (sk2 @ sk9)))),inference(cnf,[status(esa)],[8])).
% 89.08/20.99 thf(10,plain,(! [D:$i,C:$i,B:$i,A:$i] : ((~ (reli @ sk4 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (reli @ C @ (sk5 @ C @ B @ A)) | (~ (reli @ C @ D)) | (sk2 @ D))),inference(cnfConj,[status(thm)],[9])).
% 89.08/20.99 thf(17,plain,((reli @ sk3 @ sk4)),inference(cnfConj,[status(thm)],[9])).
% 89.08/20.99 thf(3,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ reli @ A) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',refl_axiom_i)).
% 89.08/20.99 thf(20,plain,((! [A:($i > $o),B:$i]: (~ (! [C:$i]: ((reli @ B @ C) => (A @ C))) | (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 89.08/20.99 thf(21,plain,(! [B:$i,A:($i > $o)] : ((((reli @ B @ (sk10 @ B @ (A))) | (A @ B)) & (~ (A @ (sk10 @ B @ (A))) | (A @ B))))),inference(cnf,[status(esa)],[20])).
% 89.08/20.99 thf(23,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk10 @ B @ (A)))) | (A @ B))),inference(cnfConj,[status(thm)],[21])).
% 89.08/20.99 thf(294,plain,(! [B:($i > $o),A:$i] : ((~ (~ (B @ (sk10 @ A @ (^ [C:$i]: ~ (B @ C)))))) | (~ (B @ A)))),inference(prim_subst,[status(thm)],[23:[bind(A, $thf(^ [D:$i]: ~ (C @ D)))]])).
% 89.08/20.99 thf(317,plain,(! [B:($i > $o),A:$i] : ((B @ (sk10 @ A @ (^ [C:$i]: ~ (B @ C)))) | (~ (B @ A)))),inference(cnf,[status(esa)],[294])).
% 89.08/20.99 thf(318,plain,(! [B:($i > $o),A:$i] : ((B @ (sk10 @ A @ (^ [C:$i]: ~ (B @ C)))) | (~ (B @ A)))),inference(simp,[status(thm)],[317])).
% 89.08/20.99 thf(4096,plain,(! [B:($i > $o),A:$i] : ((B @ (sk10 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((reli @ sk3 @ sk4) != (B @ A)))),inference(paramod_ordered,[status(thm)],[17,318])).
% 89.08/20.99 thf(4097,plain,(! [B:($i > $o),A:$i] : ((B @ (sk10 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((reli @ sk3 @ sk4) != (B @ A)))),inference(simp,[status(thm)],[4096])).
% 89.08/20.99 thf(4216,plain,((reli @ sk3 @ (sk10 @ sk4 @ (^ [A:$i]: ~ (reli @ sk3 @ A))))),inference(pre_uni,[status(thm)],[4097:[bind(A, $thf(sk4)),bind(B, $thf(reli @ sk3))]])).
% 89.08/20.99 thf(4,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ relr @ A) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',refl_axiom_r)).
% 89.08/20.99 thf(26,plain,((! [A:($i > $o),B:$i]: (~ (! [C:$i]: ((relr @ B @ C) => (A @ C))) | (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 89.08/20.99 thf(27,plain,(! [B:$i,A:($i > $o)] : ((((relr @ B @ (sk11 @ B @ (A))) | (A @ B)) & (~ (A @ (sk11 @ B @ (A))) | (A @ B))))),inference(cnf,[status(esa)],[26])).
% 89.08/20.99 thf(28,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk11 @ B @ (A))) | (A @ B))),inference(cnfConj,[status(thm)],[27])).
% 89.08/20.99 thf(1117,plain,(! [A:$i] : ((relr @ A @ (sk11 @ A @ (^ [B:$i]: (($false))))) | ($false))),inference(prim_subst,[status(thm)],[28:[bind(A, $thf(^ [C:$i]: (($false))))]])).
% 89.08/20.99 thf(1210,plain,(! [A:$i] : ((relr @ A @ (sk11 @ A @ (^ [B:$i]: (($false))))))),inference(simp,[status(thm)],[1117])).
% 89.08/20.99 thf(298,plain,(! [A:$i] : ((~ (prop_c @ (sk10 @ A @ (prop_c)))) | (prop_c @ A))),inference(prim_subst,[status(thm)],[23:[bind(A, $thf(prop_c))]])).
% 89.08/20.99 thf(321,plain,(! [A:$i] : ((~ (prop_c @ (sk10 @ A @ (prop_c)))) | (prop_c @ A))),inference(simp,[status(thm)],[298])).
% 89.08/20.99 thf(1059,plain,(! [C:$i,B:$i,A:($i > $o)] : ((relr @ B @ (sk11 @ B @ (A))) | ~ (($true)) | (prop_c @ C) | ((A @ B) != (prop_c @ (sk10 @ C @ (prop_c)))))),inference(paramod_ordered,[status(thm)],[28,321])).
% 89.08/20.99 thf(1060,plain,(! [C:$i,B:$i,A:($i > $o)] : ((relr @ B @ (sk11 @ B @ (A))) | (prop_c @ C) | ((A @ B) != (prop_c @ (sk10 @ C @ (prop_c)))))),inference(simp,[status(thm)],[1059])).
% 89.08/20.99 thf(1159,plain,(! [A:$i] : ((relr @ (sk10 @ A @ (prop_c)) @ (sk11 @ (sk10 @ A @ (prop_c)) @ (prop_c))) | (prop_c @ A))),inference(pre_uni,[status(thm)],[1060:[bind(A, $thf(prop_c)),bind(B, $thf(sk10 @ C @ (prop_c))),bind(C, $thf(C))]])).
% 89.08/20.99 thf(1187,plain,(! [A:$i] : ((relr @ (sk10 @ A @ (prop_c)) @ (sk11 @ (sk10 @ A @ (prop_c)) @ (prop_c))) | (prop_c @ A))),inference(simp,[status(thm)],[1159])).
% 89.08/20.99 thf(13,plain,((reli @ sk8 @ sk9)),inference(cnfConj,[status(thm)],[9])).
% 89.08/20.99 thf(12,plain,((reli @ sk6 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 89.08/20.99 thf(16,plain,((relr @ sk7 @ sk8)),inference(cnfConj,[status(thm)],[9])).
% 89.08/20.99 thf(18,plain,(! [D:$i,C:$i,B:$i,A:$i] : ((~ (reli @ sk4 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (~ (sk1 @ (sk5 @ C @ B @ A))) | (~ (reli @ C @ D)) | (sk2 @ D))),inference(cnfConj,[status(thm)],[9])).
% 89.08/20.99 thf(51,plain,(! [D:$i,C:$i,B:$i,A:$i] : (~ (($true)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (~ (sk1 @ (sk5 @ C @ B @ A))) | (~ (reli @ C @ D)) | (sk2 @ D) | ((reli @ sk8 @ sk9) != (reli @ sk4 @ A)))),inference(paramod_ordered,[status(thm)],[13,18])).
% 89.08/20.99 thf(52,plain,(! [D:$i,C:$i,B:$i,A:$i] : ((~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (~ (sk1 @ (sk5 @ C @ B @ A))) | (~ (reli @ C @ D)) | (sk2 @ D) | ((reli @ sk8 @ sk9) != (reli @ sk4 @ A)))),inference(simp,[status(thm)],[51])).
% 89.08/20.99 thf(79,plain,(! [D:$i,C:$i,B:$i,A:$i] : ((sk2 @ D) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (~ (sk1 @ (sk5 @ C @ B @ A))) | (~ (reli @ C @ D)) | (sk8 != sk4) | (sk9 != A))),inference(simp,[status(thm)],[52])).
% 89.08/20.99 thf(86,plain,(! [C:$i,B:$i,A:$i] : ((sk2 @ C) | (~ (relr @ sk9 @ A)) | (~ (reli @ A @ B)) | (~ (sk1 @ (sk5 @ B @ A @ sk9))) | (~ (reli @ B @ C)) | (sk8 != sk4))),inference(simp,[status(thm)],[79])).
% 89.08/20.99 thf(120,plain,(! [C:$i,B:$i,A:$i] : ((sk2 @ C) | ~ (($true)) | (~ (reli @ A @ B)) | (~ (sk1 @ (sk5 @ B @ A @ sk9))) | (~ (reli @ B @ C)) | (sk8 != sk4) | ((relr @ sk9 @ A) != (relr @ sk7 @ sk8)))),inference(paramod_ordered,[status(thm)],[16,86])).
% 89.08/20.99 thf(121,plain,(! [C:$i,B:$i,A:$i] : ((sk2 @ C) | (~ (reli @ A @ B)) | (~ (sk1 @ (sk5 @ B @ A @ sk9))) | (~ (reli @ B @ C)) | (sk8 != sk4) | ((relr @ sk9 @ A) != (relr @ sk7 @ sk8)))),inference(simp,[status(thm)],[120])).
% 89.08/20.99 thf(122,plain,(! [C:$i,B:$i,A:$i] : ((sk2 @ C) | (~ (reli @ A @ B)) | (~ (sk1 @ (sk5 @ B @ A @ sk9))) | (~ (reli @ B @ C)) | (sk8 != sk4) | (sk9 != sk7) | (A != sk8))),inference(simp,[status(thm)],[121])).
% 89.08/20.99 thf(124,plain,(! [B:$i,A:$i] : ((sk2 @ B) | (~ (reli @ sk8 @ A)) | (~ (sk1 @ (sk5 @ A @ sk8 @ sk9))) | (~ (reli @ A @ B)) | (sk8 != sk4) | (sk9 != sk7))),inference(simp,[status(thm)],[122])).
% 89.08/20.99 thf(346,plain,(! [B:$i,A:$i] : ((sk2 @ B) | ~ (($true)) | (~ (sk1 @ (sk5 @ A @ sk8 @ sk9))) | (~ (reli @ A @ B)) | (sk8 != sk4) | (sk9 != sk7) | ((reli @ sk8 @ A) != (reli @ sk6 @ sk7)))),inference(paramod_ordered,[status(thm)],[12,124])).
% 89.08/20.99 thf(347,plain,(! [B:$i,A:$i] : ((sk2 @ B) | (~ (sk1 @ (sk5 @ A @ sk8 @ sk9))) | (~ (reli @ A @ B)) | (sk8 != sk4) | (sk9 != sk7) | ((reli @ sk8 @ A) != (reli @ sk6 @ sk7)))),inference(simp,[status(thm)],[346])).
% 89.08/20.99 thf(352,plain,(! [B:$i,A:$i] : ((sk2 @ B) | (~ (sk1 @ (sk5 @ A @ sk8 @ sk9))) | (~ (reli @ A @ B)) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (A != sk7))),inference(simp,[status(thm)],[347])).
% 89.08/20.99 thf(356,plain,(! [A:$i] : ((sk2 @ A) | (~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (~ (reli @ sk7 @ A)) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6))),inference(simp,[status(thm)],[352])).
% 89.08/20.99 thf(365,plain,(! [A:$i] : ((sk2 @ A) | (~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | ~ (($true)) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | ((reli @ sk8 @ sk9) != (reli @ sk7 @ A)))),inference(paramod_ordered,[status(thm)],[13,356])).
% 89.08/20.99 thf(366,plain,(! [A:$i] : ((sk2 @ A) | (~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | ((reli @ sk8 @ sk9) != (reli @ sk7 @ A)))),inference(simp,[status(thm)],[365])).
% 89.08/20.99 thf(374,plain,(! [A:$i] : ((sk2 @ A) | (~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk8 != sk7) | (sk9 != A))),inference(simp,[status(thm)],[366])).
% 89.08/20.99 thf(378,plain,((sk2 @ sk9) | (~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk8 != sk7)),inference(simp,[status(thm)],[374])).
% 89.08/20.99 thf(14,plain,((~ (sk2 @ sk9))),inference(cnfConj,[status(thm)],[9])).
% 89.08/20.99 thf(1292,plain,(($false) | (~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk8 != sk7)),inference(rewrite,[status(thm)],[378,14])).
% 89.08/20.99 thf(1293,plain,((~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk8 != sk7)),inference(simp,[status(thm)],[1292])).
% 89.08/20.99 thf(1083,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk11 @ B @ (A))) | ~ (($true)) | ((A @ B) != (sk2 @ sk9)))),inference(paramod_ordered,[status(thm)],[28,14])).
% 89.08/20.99 thf(1084,plain,(! [B:$i,A:($i > $o)] : ((relr @ B @ (sk11 @ B @ (A))) | ((A @ B) != (sk2 @ sk9)))),inference(simp,[status(thm)],[1083])).
% 89.08/20.99 thf(1172,plain,((relr @ sk9 @ (sk11 @ sk9 @ (sk2)))),inference(pre_uni,[status(thm)],[1084:[bind(A, $thf(sk2)),bind(B, $thf(sk9))]])).
% 89.08/20.99 thf(15,plain,((reli @ sk4 @ sk6)),inference(cnfConj,[status(thm)],[9])).
% 89.08/20.99 thf(4168,plain,(! [B:($i > $o),A:$i] : ((B @ (sk10 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((reli @ sk4 @ sk6) != (B @ A)))),inference(paramod_ordered,[status(thm)],[15,318])).
% 89.08/20.99 thf(4169,plain,(! [B:($i > $o),A:$i] : ((B @ (sk10 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((reli @ sk4 @ sk6) != (B @ A)))),inference(simp,[status(thm)],[4168])).
% 89.08/20.99 thf(4201,plain,((reli @ sk4 @ (sk10 @ sk6 @ (^ [A:$i]: ~ (reli @ sk4 @ A))))),inference(pre_uni,[status(thm)],[4169:[bind(A, $thf(sk6)),bind(B, $thf(reli @ sk4))]])).
% 89.08/20.99 thf(11,plain,(! [C:$i,B:$i,A:$i] : ((~ (reli @ sk6 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (sk1 @ C))),inference(cnfConj,[status(thm)],[9])).
% 89.08/20.99 thf(19,plain,(! [C:$i,B:$i,A:$i] : ((~ (reli @ sk6 @ A)) | (~ (relr @ A @ B)) | (~ (reli @ B @ C)) | (sk1 @ C))),inference(simp,[status(thm)],[11])).
% 89.08/20.99 thf(145,plain,(! [C:$i,B:$i,A:$i] : ((~ (reli @ sk6 @ A)) | (~ (relr @ A @ B)) | ~ (($true)) | (sk1 @ C) | ((reli @ sk8 @ sk9) != (reli @ B @ C)))),inference(paramod_ordered,[status(thm)],[13,19])).
% 89.08/20.99 thf(146,plain,(! [C:$i,B:$i,A:$i] : ((~ (reli @ sk6 @ A)) | (~ (relr @ A @ B)) | (sk1 @ C) | ((reli @ sk8 @ sk9) != (reli @ B @ C)))),inference(simp,[status(thm)],[145])).
% 89.08/20.99 thf(147,plain,(! [A:$i] : ((~ (reli @ sk6 @ A)) | (~ (relr @ A @ sk8)) | (sk1 @ sk9))),inference(pattern_uni,[status(thm)],[146:[bind(A, $thf(A)),bind(B, $thf(sk8)),bind(C, $thf(sk9))]])).
% 89.08/20.99 thf(977,plain,(! [A:$i] : ((~ (reli @ sk6 @ A)) | ~ (($true)) | (sk1 @ sk9) | ((relr @ sk7 @ sk8) != (relr @ A @ sk8)))),inference(paramod_ordered,[status(thm)],[16,147])).
% 89.08/20.99 thf(978,plain,(! [A:$i] : ((~ (reli @ sk6 @ A)) | (sk1 @ sk9) | ((relr @ sk7 @ sk8) != (relr @ A @ sk8)))),inference(simp,[status(thm)],[977])).
% 89.08/20.99 thf(979,plain,((~ (reli @ sk6 @ sk7)) | (sk1 @ sk9)),inference(pattern_uni,[status(thm)],[978:[bind(A, $thf(sk7))]])).
% 89.08/20.99 thf(1024,plain,(~ (($true)) | (sk1 @ sk9)),inference(rewrite,[status(thm)],[979,12])).
% 89.08/20.99 thf(1025,plain,((sk1 @ sk9)),inference(simp,[status(thm)],[1024])).
% 89.08/20.99 thf(369,plain,(! [A:$i] : ((sk2 @ A) | (~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | ~ (($true)) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | ((reli @ sk7 @ A) != (reli @ sk4 @ sk6)))),inference(paramod_ordered,[status(thm)],[15,356])).
% 89.08/20.99 thf(370,plain,(! [A:$i] : ((sk2 @ A) | (~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | ((reli @ sk7 @ A) != (reli @ sk4 @ sk6)))),inference(simp,[status(thm)],[369])).
% 89.08/20.99 thf(375,plain,(! [A:$i] : ((sk2 @ A) | (~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk4) | (A != sk6))),inference(simp,[status(thm)],[370])).
% 89.08/20.99 thf(379,plain,((sk2 @ sk6) | (~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk4)),inference(simp,[status(thm)],[375])).
% 89.08/20.99 thf(1509,plain,((~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk4) | ~ (($true)) | ((sk2 @ sk9) != (sk2 @ sk6))),inference(paramod_ordered,[status(thm)],[379,14])).
% 89.08/20.99 thf(1510,plain,((~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk4) | ((sk2 @ sk9) != (sk2 @ sk6))),inference(simp,[status(thm)],[1509])).
% 89.08/20.99 thf(1524,plain,((~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk4) | (sk9 != sk6)),inference(simp,[status(thm)],[1510])).
% 89.08/20.99 thf(1719,plain,(~ (($true)) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk4) | (sk9 != sk6) | ((sk1 @ (sk5 @ sk7 @ sk8 @ sk9)) != (sk1 @ sk9))),inference(paramod_ordered,[status(thm)],[1025,1524])).
% 89.08/20.99 thf(1720,plain,((sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk4) | (sk9 != sk6) | ((sk1 @ (sk5 @ sk7 @ sk8 @ sk9)) != (sk1 @ sk9))),inference(simp,[status(thm)],[1719])).
% 89.08/20.99 thf(1729,plain,((sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk4) | (sk9 != sk6) | ((sk5 @ sk7 @ sk8 @ sk9) != sk9)),inference(simp,[status(thm)],[1720])).
% 89.08/20.99 thf(289,plain,(! [A:$i] : ((~ (prop_b @ (sk10 @ A @ (prop_b)))) | (prop_b @ A))),inference(prim_subst,[status(thm)],[23:[bind(A, $thf(prop_b))]])).
% 89.08/20.99 thf(308,plain,(! [A:$i] : ((~ (prop_b @ (sk10 @ A @ (prop_b)))) | (prop_b @ A))),inference(simp,[status(thm)],[289])).
% 89.08/20.99 thf(4215,plain,((reli @ (sk10 @ sk3 @ (^ [A:$i]: ~ (reli @ A @ sk4))) @ sk4)),inference(pre_uni,[status(thm)],[4097:[bind(A, $thf(sk3)),bind(B, $thf(^ [C:$i]: (reli @ C @ sk4)))]])).
% 89.08/20.99 thf(5,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ reli @ A) @ (mbox @ reli @ (mbox @ reli @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',trans_axiom_i)).
% 89.08/20.99 thf(32,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])).
% 89.08/20.99 thf(33,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((((reli @ B @ (sk12 @ B @ (A))) | ~ (reli @ B @ C) | ~ (reli @ C @ D) | (A @ D)) & (~ (A @ (sk12 @ B @ (A))) | ~ (reli @ B @ C) | ~ (reli @ C @ D) | (A @ D))))),inference(cnf,[status(esa)],[32])).
% 89.08/20.99 thf(34,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk12 @ B @ (A))) | (~ (reli @ B @ C)) | (~ (reli @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[33])).
% 89.08/20.99 thf(1780,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk12 @ B @ (A))) | (~ (reli @ B @ C)) | (~ (reli @ C @ D)) | ~ (($true)) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk4) | (sk9 != sk6) | ((A @ D) != (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))))),inference(paramod_ordered,[status(thm)],[34,1524])).
% 89.08/20.99 thf(1781,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk12 @ B @ (A))) | (~ (reli @ B @ C)) | (~ (reli @ C @ D)) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk4) | (sk9 != sk6) | ((A @ D) != (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))))),inference(simp,[status(thm)],[1780])).
% 89.08/20.99 thf(2055,plain,(! [B:$i,A:$i] : ((reli @ A @ (sk12 @ A @ (sk1))) | (~ (reli @ A @ B)) | (~ (reli @ B @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk4) | (sk9 != sk6))),inference(pre_uni,[status(thm)],[1781:[bind(A, $thf(sk1)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(sk5 @ sk7 @ sk8 @ sk9))]])).
% 89.08/20.99 thf(2082,plain,(! [B:$i,A:$i] : ((reli @ A @ (sk12 @ A @ (sk1))) | (~ (reli @ A @ B)) | (~ (reli @ B @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk4) | (sk9 != sk6))),inference(simp,[status(thm)],[2055])).
% 89.08/20.99 thf(35,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk12 @ B @ (A)))) | (~ (reli @ B @ C)) | (~ (reli @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[33])).
% 89.08/20.99 thf(36,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ ((sk12 @ B @ (A)) = (sk12 @ B @ ((=) @ $i @ (sk12 @ B @ A))))) | (~ (reli @ B @ C)) | (~ (reli @ C @ D)) | ((sk12 @ B @ (A)) = D))),inference(replace_leibeq,[status(thm)],[35:[bind(A, $thf((=) @ $i @ (sk12 @ B @ A)))]])).
% 89.08/20.99 thf(37,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : (((sk12 @ B @ (A)) != (sk12 @ B @ ((=) @ $i @ (sk12 @ B @ A)))) | ((sk12 @ B @ (A)) = D) | (~ (reli @ B @ C)) | (~ (reli @ C @ D)))),inference(lifteq,[status(thm)],[36])).
% 89.08/20.99 thf(24,plain,(! [B:$i,A:($i > $o)] : ((~ ((sk10 @ B @ (A)) = (sk10 @ B @ ((=) @ $i @ (sk10 @ B @ A))))) | ((sk10 @ B @ (A)) = B))),inference(replace_leibeq,[status(thm)],[23:[bind(A, $thf((=) @ $i @ (sk10 @ B @ A)))]])).
% 89.08/20.99 thf(25,plain,(! [B:$i,A:($i > $o)] : (((sk10 @ B @ (A)) != (sk10 @ B @ ((=) @ $i @ (sk10 @ B @ A)))) | ((sk10 @ B @ (A)) = B))),inference(lifteq,[status(thm)],[24])).
% 89.08/20.99 thf(22,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk10 @ B @ (A))) | (A @ B))),inference(cnfConj,[status(thm)],[21])).
% 89.08/20.99 thf(486,plain,(! [A:$i] : ((reli @ A @ (sk10 @ A @ (prop_c))) | (prop_c @ A))),inference(prim_subst,[status(thm)],[22:[bind(A, $thf(prop_c))]])).
% 89.08/20.99 thf(587,plain,(! [A:$i] : ((reli @ A @ (sk10 @ A @ (prop_c))) | (prop_c @ A))),inference(simp,[status(thm)],[486])).
% 89.08/20.99 thf(29,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk11 @ B @ (A)))) | (A @ B))),inference(cnfConj,[status(thm)],[27])).
% 89.08/20.99 thf(1377,plain,(! [A:$i] : ((~ (prop_c @ (sk11 @ A @ (prop_c)))) | (prop_c @ A))),inference(prim_subst,[status(thm)],[29:[bind(A, $thf(prop_c))]])).
% 89.08/20.99 thf(1425,plain,(! [A:$i] : ((~ (prop_c @ (sk11 @ A @ (prop_c)))) | (prop_c @ A))),inference(simp,[status(thm)],[1377])).
% 89.08/20.99 thf(1447,plain,(! [C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk10 @ B @ (A))) | ~ (($true)) | (prop_c @ C) | ((A @ B) != (prop_c @ (sk11 @ C @ (prop_c)))))),inference(paramod_ordered,[status(thm)],[22,1425])).
% 89.08/20.99 thf(1448,plain,(! [C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk10 @ B @ (A))) | (prop_c @ C) | ((A @ B) != (prop_c @ (sk11 @ C @ (prop_c)))))),inference(simp,[status(thm)],[1447])).
% 89.08/20.99 thf(1451,plain,(! [A:$i] : ((reli @ (sk11 @ A @ (prop_c)) @ (sk10 @ (sk11 @ A @ (prop_c)) @ (prop_c))) | (prop_c @ A))),inference(pre_uni,[status(thm)],[1448:[bind(A, $thf(prop_c)),bind(B, $thf(sk11 @ C @ (prop_c))),bind(C, $thf(C))]])).
% 89.08/20.99 thf(1455,plain,(! [A:$i] : ((reli @ (sk11 @ A @ (prop_c)) @ (sk10 @ (sk11 @ A @ (prop_c)) @ (prop_c))) | (prop_c @ A))),inference(simp,[status(thm)],[1451])).
% 89.08/20.99 thf(1382,plain,(! [A:$i] : ((~ (prop_b @ (sk11 @ A @ (prop_b)))) | (prop_b @ A))),inference(prim_subst,[status(thm)],[29:[bind(A, $thf(prop_b))]])).
% 89.08/20.99 thf(1431,plain,(! [A:$i] : ((~ (prop_b @ (sk11 @ A @ (prop_b)))) | (prop_b @ A))),inference(simp,[status(thm)],[1382])).
% 89.08/20.99 thf(1471,plain,(! [C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk10 @ B @ (A))) | ~ (($true)) | (prop_b @ C) | ((A @ B) != (prop_b @ (sk11 @ C @ (prop_b)))))),inference(paramod_ordered,[status(thm)],[22,1431])).
% 89.08/20.99 thf(1472,plain,(! [C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk10 @ B @ (A))) | (prop_b @ C) | ((A @ B) != (prop_b @ (sk11 @ C @ (prop_b)))))),inference(simp,[status(thm)],[1471])).
% 89.08/20.99 thf(1475,plain,(! [A:$i] : ((reli @ (sk11 @ A @ (prop_b)) @ (sk10 @ (sk11 @ A @ (prop_b)) @ (prop_b))) | (prop_b @ A))),inference(pre_uni,[status(thm)],[1472:[bind(A, $thf(prop_b)),bind(B, $thf(sk11 @ C @ (prop_b))),bind(C, $thf(C))]])).
% 89.08/20.99 thf(1479,plain,(! [A:$i] : ((reli @ (sk11 @ A @ (prop_b)) @ (sk10 @ (sk11 @ A @ (prop_b)) @ (prop_b))) | (prop_b @ A))),inference(simp,[status(thm)],[1475])).
% 89.08/20.99 thf(293,plain,(! [A:$i] : ((~ (prop_a @ (sk10 @ A @ (prop_a)))) | (prop_a @ A))),inference(prim_subst,[status(thm)],[23:[bind(A, $thf(prop_a))]])).
% 89.08/20.99 thf(316,plain,(! [A:$i] : ((~ (prop_a @ (sk10 @ A @ (prop_a)))) | (prop_a @ A))),inference(simp,[status(thm)],[293])).
% 89.08/20.99 thf(1044,plain,(! [C:$i,B:$i,A:($i > $o)] : ((relr @ B @ (sk11 @ B @ (A))) | ~ (($true)) | (prop_b @ C) | ((A @ B) != (prop_b @ (sk10 @ C @ (prop_b)))))),inference(paramod_ordered,[status(thm)],[28,308])).
% 89.08/20.99 thf(1045,plain,(! [C:$i,B:$i,A:($i > $o)] : ((relr @ B @ (sk11 @ B @ (A))) | (prop_b @ C) | ((A @ B) != (prop_b @ (sk10 @ C @ (prop_b)))))),inference(simp,[status(thm)],[1044])).
% 89.08/20.99 thf(1141,plain,(! [A:$i] : ((relr @ (sk10 @ A @ (prop_b)) @ (sk11 @ (sk10 @ A @ (prop_b)) @ (prop_b))) | (prop_b @ A))),inference(pre_uni,[status(thm)],[1045:[bind(A, $thf(prop_b)),bind(B, $thf(sk10 @ C @ (prop_b))),bind(C, $thf(C))]])).
% 89.08/20.99 thf(1232,plain,(! [A:$i] : ((relr @ (sk10 @ A @ (prop_b)) @ (sk11 @ (sk10 @ A @ (prop_b)) @ (prop_b))) | (prop_b @ A))),inference(simp,[status(thm)],[1141])).
% 89.08/20.99 thf(1380,plain,(! [A:$i] : ((~ (prop_a @ (sk11 @ A @ (prop_a)))) | (prop_a @ A))),inference(prim_subst,[status(thm)],[29:[bind(A, $thf(prop_a))]])).
% 89.08/20.99 thf(1429,plain,(! [A:$i] : ((~ (prop_a @ (sk11 @ A @ (prop_a)))) | (prop_a @ A))),inference(simp,[status(thm)],[1380])).
% 89.08/20.99 thf(1457,plain,(! [C:$i,B:$i,A:($i > $o)] : ((relr @ B @ (sk11 @ B @ (A))) | ~ (($true)) | (prop_a @ C) | ((A @ B) != (prop_a @ (sk11 @ C @ (prop_a)))))),inference(paramod_ordered,[status(thm)],[28,1429])).
% 89.08/20.99 thf(1458,plain,(! [C:$i,B:$i,A:($i > $o)] : ((relr @ B @ (sk11 @ B @ (A))) | (prop_a @ C) | ((A @ B) != (prop_a @ (sk11 @ C @ (prop_a)))))),inference(simp,[status(thm)],[1457])).
% 89.08/20.99 thf(1461,plain,(! [A:$i] : ((relr @ (sk11 @ A @ (prop_a)) @ (sk11 @ (sk11 @ A @ (prop_a)) @ (prop_a))) | (prop_a @ A))),inference(pre_uni,[status(thm)],[1458:[bind(A, $thf(prop_a)),bind(B, $thf(sk11 @ C @ (prop_a))),bind(C, $thf(C))]])).
% 89.08/20.99 thf(1465,plain,(! [A:$i] : ((relr @ (sk11 @ A @ (prop_a)) @ (sk11 @ (sk11 @ A @ (prop_a)) @ (prop_a))) | (prop_a @ A))),inference(simp,[status(thm)],[1461])).
% 89.08/20.99 thf(4148,plain,(! [B:($i > $o),A:$i] : ((B @ (sk10 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((relr @ sk7 @ sk8) != (B @ A)))),inference(paramod_ordered,[status(thm)],[16,318])).
% 89.08/20.99 thf(4149,plain,(! [B:($i > $o),A:$i] : ((B @ (sk10 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((relr @ sk7 @ sk8) != (B @ A)))),inference(simp,[status(thm)],[4148])).
% 89.08/20.99 thf(4297,plain,((relr @ (sk10 @ sk7 @ (^ [A:$i]: ~ (relr @ A @ sk8))) @ sk8)),inference(pre_uni,[status(thm)],[4149:[bind(A, $thf(sk7)),bind(B, $thf(^ [C:$i]: (relr @ C @ sk8)))]])).
% 89.08/20.99 thf(1121,plain,(! [A:$i] : ((relr @ A @ (sk11 @ A @ (prop_b))) | (prop_b @ A))),inference(prim_subst,[status(thm)],[28:[bind(A, $thf(prop_b))]])).
% 89.08/20.99 thf(1215,plain,(! [A:$i] : ((relr @ A @ (sk11 @ A @ (prop_b))) | (prop_b @ A))),inference(simp,[status(thm)],[1121])).
% 89.08/20.99 thf(401,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk10 @ B @ (A))) | ~ (($true)) | ((A @ B) != (sk2 @ sk9)))),inference(paramod_ordered,[status(thm)],[22,14])).
% 89.08/20.99 thf(402,plain,(! [B:$i,A:($i > $o)] : ((reli @ B @ (sk10 @ B @ (A))) | ((A @ B) != (sk2 @ sk9)))),inference(simp,[status(thm)],[401])).
% 89.08/20.99 thf(520,plain,(! [A:$i] : ((reli @ A @ (sk10 @ A @ (^ [B:$i]: (sk2 @ sk9)))))),inference(pre_uni,[status(thm)],[402:[bind(A, $thf(^ [C:$i]: (sk2 @ sk9))),bind(B, $thf(B))]])).
% 89.08/20.99 thf(550,plain,(! [A:$i] : ((reli @ A @ (sk10 @ A @ (^ [B:$i]: (sk2 @ sk9)))))),inference(simp,[status(thm)],[520])).
% 89.08/20.99 thf(660,plain,(! [A:$i] : ((reli @ A @ (sk10 @ A @ (^ [B:$i]: (($false))))))),inference(rewrite,[status(thm)],[550,14])).
% 89.08/20.99 thf(403,plain,(! [C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk10 @ B @ (A))) | ~ (($true)) | (prop_a @ C) | ((A @ B) != (prop_a @ (sk10 @ C @ (prop_a)))))),inference(paramod_ordered,[status(thm)],[22,316])).
% 89.08/20.99 thf(404,plain,(! [C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk10 @ B @ (A))) | (prop_a @ C) | ((A @ B) != (prop_a @ (sk10 @ C @ (prop_a)))))),inference(simp,[status(thm)],[403])).
% 89.08/20.99 thf(497,plain,(! [A:$i] : ((reli @ (sk10 @ A @ (prop_a)) @ (sk10 @ (sk10 @ A @ (prop_a)) @ (prop_a))) | (prop_a @ A))),inference(pre_uni,[status(thm)],[404:[bind(A, $thf(prop_a)),bind(B, $thf(sk10 @ C @ (prop_a))),bind(C, $thf(C))]])).
% 89.08/20.99 thf(598,plain,(! [A:$i] : ((reli @ (sk10 @ A @ (prop_a)) @ (sk10 @ (sk10 @ A @ (prop_a)) @ (prop_a))) | (prop_a @ A))),inference(simp,[status(thm)],[497])).
% 89.08/20.99 thf(4136,plain,(! [B:($i > $o),A:$i] : ((B @ (sk10 @ A @ (^ [C:$i]: ~ (B @ C)))) | ~ (($true)) | ((sk1 @ sk9) != (B @ A)))),inference(paramod_ordered,[status(thm)],[1025,318])).
% 89.08/20.99 thf(4137,plain,(! [B:($i > $o),A:$i] : ((B @ (sk10 @ A @ (^ [C:$i]: ~ (B @ C)))) | ((sk1 @ sk9) != (B @ A)))),inference(simp,[status(thm)],[4136])).
% 89.08/20.99 thf(4221,plain,((sk1 @ (sk10 @ sk9 @ (^ [A:$i]: ~ (sk1 @ A))))),inference(pre_uni,[status(thm)],[4137:[bind(A, $thf(sk9)),bind(B, $thf(sk1))]])).
% 89.08/20.99 thf(4464,plain,(~ (($true)) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk8 != sk7) | ((sk1 @ (sk5 @ sk7 @ sk8 @ sk9)) != (sk1 @ (sk10 @ sk9 @ (^ [A:$i]: ~ (sk1 @ A)))))),inference(paramod_ordered,[status(thm)],[4221,1293])).
% 89.08/20.99 thf(4465,plain,((sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk8 != sk7) | ((sk1 @ (sk5 @ sk7 @ sk8 @ sk9)) != (sk1 @ (sk10 @ sk9 @ (^ [A:$i]: ~ (sk1 @ A)))))),inference(simp,[status(thm)],[4464])).
% 89.08/20.99 thf(4493,plain,((sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk8 != sk7) | ((sk5 @ sk7 @ sk8 @ sk9) != (sk10 @ sk9 @ (^ [A:$i]: ~ (sk1 @ A))))),inference(simp,[status(thm)],[4465])).
% 89.08/20.99 thf(6,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ relr @ A) @ (mbox @ relr @ (mbox @ relr @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',trans_axiom_r)).
% 89.08/20.99 thf(38,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])).
% 89.08/20.99 thf(1120,plain,(! [A:$i] : ((relr @ A @ (sk11 @ A @ (prop_c))) | (prop_c @ A))),inference(prim_subst,[status(thm)],[28:[bind(A, $thf(prop_c))]])).
% 89.08/20.99 thf(1214,plain,(! [A:$i] : ((relr @ A @ (sk11 @ A @ (prop_c))) | (prop_c @ A))),inference(simp,[status(thm)],[1120])).
% 89.08/20.99 thf(2497,plain,(! [F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (reli @ A @ B)) | (~ (reli @ B @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk4) | (sk9 != sk6) | ~ (($true)) | (~ (relr @ C @ D)) | (~ (reli @ D @ E)) | (~ (sk1 @ (sk5 @ E @ D @ C))) | (~ (reli @ E @ F)) | (sk2 @ F) | ((reli @ A @ (sk12 @ A @ (sk1))) != (reli @ sk4 @ C)))),inference(paramod_ordered,[status(thm)],[2082,18])).
% 89.08/20.99 thf(2498,plain,(! [F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (reli @ A @ B)) | (~ (reli @ B @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk4) | (sk9 != sk6) | (~ (relr @ C @ D)) | (~ (reli @ D @ E)) | (~ (sk1 @ (sk5 @ E @ D @ C))) | (~ (reli @ E @ F)) | (sk2 @ F) | ((reli @ A @ (sk12 @ A @ (sk1))) != (reli @ sk4 @ C)))),inference(simp,[status(thm)],[2497])).
% 89.08/20.99 thf(2499,plain,(! [D:$i,C:$i,B:$i,A:$i] : ((~ (reli @ sk4 @ A)) | (~ (reli @ A @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk4) | (sk9 != sk6) | (~ (relr @ (sk12 @ sk4 @ (sk1)) @ B)) | (~ (reli @ B @ C)) | (~ (sk1 @ (sk5 @ C @ B @ (sk12 @ sk4 @ (sk1))))) | (~ (reli @ C @ D)) | (sk2 @ D))),inference(pattern_uni,[status(thm)],[2498:[bind(A, $thf(sk4)),bind(B, $thf(B)),bind(C, $thf(sk12 @ sk4 @ (sk1))),bind(D, $thf(D)),bind(E, $thf(E)),bind(F, $thf(F))]])).
% 89.08/20.99 thf(2570,plain,(! [D:$i,C:$i,B:$i,A:$i] : ((~ (reli @ sk4 @ A)) | (~ (reli @ A @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk4) | (sk9 != sk6) | (~ (relr @ (sk12 @ sk4 @ (sk1)) @ B)) | (~ (reli @ B @ C)) | (~ (sk1 @ (sk5 @ C @ B @ (sk12 @ sk4 @ (sk1))))) | (~ (reli @ C @ D)) | (sk2 @ D))),inference(simp,[status(thm)],[2499])).
% 89.08/20.99 thf(382,plain,(! [C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk10 @ B @ (A))) | ~ (($true)) | (prop_b @ C) | ((A @ B) != (prop_b @ (sk10 @ C @ (prop_b)))))),inference(paramod_ordered,[status(thm)],[22,308])).
% 89.08/20.99 thf(383,plain,(! [C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk10 @ B @ (A))) | (prop_b @ C) | ((A @ B) != (prop_b @ (sk10 @ C @ (prop_b)))))),inference(simp,[status(thm)],[382])).
% 89.08/20.99 thf(535,plain,(! [A:$i] : ((reli @ (sk10 @ A @ (prop_b)) @ (sk10 @ (sk10 @ A @ (prop_b)) @ (prop_b))) | (prop_b @ A))),inference(pre_uni,[status(thm)],[383:[bind(A, $thf(prop_b)),bind(B, $thf(sk10 @ C @ (prop_b))),bind(C, $thf(C))]])).
% 89.08/20.99 thf(562,plain,(! [A:$i] : ((reli @ (sk10 @ A @ (prop_b)) @ (sk10 @ (sk10 @ A @ (prop_b)) @ (prop_b))) | (prop_b @ A))),inference(simp,[status(thm)],[535])).
% 89.08/20.99 thf(7,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ reli @ (mbox @ relr @ A)) @ (mbox @ relr @ (mbox @ reli @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_i_r_commute)).
% 89.08/20.99 thf(44,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])).
% 89.08/20.99 thf(478,plain,(! [A:$i] : ((reli @ A @ (sk10 @ A @ (prop_a))) | (prop_a @ A))),inference(prim_subst,[status(thm)],[22:[bind(A, $thf(prop_a))]])).
% 89.08/20.99 thf(577,plain,(! [A:$i] : ((reli @ A @ (sk10 @ A @ (prop_a))) | (prop_a @ A))),inference(simp,[status(thm)],[478])).
% 89.08/20.99 thf(521,plain,((reli @ sk9 @ (sk10 @ sk9 @ (sk2)))),inference(pre_uni,[status(thm)],[402:[bind(A, $thf(sk2)),bind(B, $thf(sk9))]])).
% 89.08/20.99 thf(1469,plain,(! [C:$i,B:$i,A:($i > $o)] : ((relr @ B @ (sk11 @ B @ (A))) | ~ (($true)) | (prop_b @ C) | ((A @ B) != (prop_b @ (sk11 @ C @ (prop_b)))))),inference(paramod_ordered,[status(thm)],[28,1431])).
% 89.08/20.99 thf(1470,plain,(! [C:$i,B:$i,A:($i > $o)] : ((relr @ B @ (sk11 @ B @ (A))) | (prop_b @ C) | ((A @ B) != (prop_b @ (sk11 @ C @ (prop_b)))))),inference(simp,[status(thm)],[1469])).
% 89.08/20.99 thf(1473,plain,(! [A:$i] : ((relr @ (sk11 @ A @ (prop_b)) @ (sk11 @ (sk11 @ A @ (prop_b)) @ (prop_b))) | (prop_b @ A))),inference(pre_uni,[status(thm)],[1470:[bind(A, $thf(prop_b)),bind(B, $thf(sk11 @ C @ (prop_b))),bind(C, $thf(C))]])).
% 89.08/20.99 thf(1477,plain,(! [A:$i] : ((relr @ (sk11 @ A @ (prop_b)) @ (sk11 @ (sk11 @ A @ (prop_b)) @ (prop_b))) | (prop_b @ A))),inference(simp,[status(thm)],[1473])).
% 89.08/20.99 thf(371,plain,(! [A:$i] : ((sk2 @ A) | (~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | ~ (($true)) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | ((reli @ sk7 @ A) != (reli @ sk6 @ sk7)))),inference(paramod_ordered,[status(thm)],[12,356])).
% 89.08/20.99 thf(372,plain,(! [A:$i] : ((sk2 @ A) | (~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | ((reli @ sk7 @ A) != (reli @ sk6 @ sk7)))),inference(simp,[status(thm)],[371])).
% 89.08/20.99 thf(373,plain,(! [A:$i] : ((sk2 @ A) | (~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk6) | (A != sk7))),inference(simp,[status(thm)],[372])).
% 89.08/20.99 thf(377,plain,((sk2 @ sk7) | (~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk6)),inference(simp,[status(thm)],[373])).
% 89.08/20.99 thf(891,plain,((~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk6) | ~ (($true)) | ((sk2 @ sk9) != (sk2 @ sk7))),inference(paramod_ordered,[status(thm)],[377,14])).
% 89.08/20.99 thf(892,plain,((~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk6) | ((sk2 @ sk9) != (sk2 @ sk7))),inference(simp,[status(thm)],[891])).
% 89.08/20.99 thf(897,plain,((~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk6) | (sk9 != sk7)),inference(simp,[status(thm)],[892])).
% 89.08/20.99 thf(903,plain,((~ (sk1 @ (sk5 @ sk7 @ sk8 @ sk9))) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk6)),inference(simp,[status(thm)],[897])).
% 89.08/20.99 thf(4486,plain,(~ (($true)) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk6) | ((sk1 @ (sk5 @ sk7 @ sk8 @ sk9)) != (sk1 @ (sk10 @ sk9 @ (^ [A:$i]: ~ (sk1 @ A)))))),inference(paramod_ordered,[status(thm)],[4221,903])).
% 89.08/20.99 thf(4487,plain,((sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk6) | ((sk1 @ (sk5 @ sk7 @ sk8 @ sk9)) != (sk1 @ (sk10 @ sk9 @ (^ [A:$i]: ~ (sk1 @ A)))))),inference(simp,[status(thm)],[4486])).
% 89.08/20.99 thf(4497,plain,((sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk6) | ((sk5 @ sk7 @ sk8 @ sk9) != (sk10 @ sk9 @ (^ [A:$i]: ~ (sk1 @ A))))),inference(simp,[status(thm)],[4487])).
% 89.08/20.99 thf(1459,plain,(! [C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk10 @ B @ (A))) | ~ (($true)) | (prop_a @ C) | ((A @ B) != (prop_a @ (sk11 @ C @ (prop_a)))))),inference(paramod_ordered,[status(thm)],[22,1429])).
% 89.08/20.99 thf(1460,plain,(! [C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk10 @ B @ (A))) | (prop_a @ C) | ((A @ B) != (prop_a @ (sk11 @ C @ (prop_a)))))),inference(simp,[status(thm)],[1459])).
% 89.08/20.99 thf(1463,plain,(! [A:$i] : ((reli @ (sk11 @ A @ (prop_a)) @ (sk10 @ (sk11 @ A @ (prop_a)) @ (prop_a))) | (prop_a @ A))),inference(pre_uni,[status(thm)],[1460:[bind(A, $thf(prop_a)),bind(B, $thf(sk11 @ C @ (prop_a))),bind(C, $thf(C))]])).
% 89.08/20.99 thf(1467,plain,(! [A:$i] : ((reli @ (sk11 @ A @ (prop_a)) @ (sk10 @ (sk11 @ A @ (prop_a)) @ (prop_a))) | (prop_a @ A))),inference(simp,[status(thm)],[1463])).
% 89.08/20.99 thf(405,plain,(! [C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk10 @ B @ (A))) | ~ (($true)) | (prop_c @ C) | ((A @ B) != (prop_c @ (sk10 @ C @ (prop_c)))))),inference(paramod_ordered,[status(thm)],[22,321])).
% 89.08/20.99 thf(406,plain,(! [C:$i,B:$i,A:($i > $o)] : ((reli @ B @ (sk10 @ B @ (A))) | (prop_c @ C) | ((A @ B) != (prop_c @ (sk10 @ C @ (prop_c)))))),inference(simp,[status(thm)],[405])).
% 89.08/20.99 thf(524,plain,(! [A:$i] : ((reli @ (sk10 @ A @ (prop_c)) @ (sk10 @ (sk10 @ A @ (prop_c)) @ (prop_c))) | (prop_c @ A))),inference(pre_uni,[status(thm)],[406:[bind(A, $thf(prop_c)),bind(B, $thf(sk10 @ C @ (prop_c))),bind(C, $thf(C))]])).
% 89.08/20.99 thf(553,plain,(! [A:$i] : ((reli @ (sk10 @ A @ (prop_c)) @ (sk10 @ (sk10 @ A @ (prop_c)) @ (prop_c))) | (prop_c @ A))),inference(simp,[status(thm)],[524])).
% 89.08/20.99 thf(4200,plain,((reli @ (sk10 @ sk4 @ (^ [A:$i]: ~ (reli @ A @ sk6))) @ sk6)),inference(pre_uni,[status(thm)],[4169:[bind(A, $thf(sk4)),bind(B, $thf(^ [C:$i]: (reli @ C @ sk6)))]])).
% 89.08/20.99 thf(1030,plain,(~ (($true)) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk6) | ((sk1 @ (sk5 @ sk7 @ sk8 @ sk9)) != (sk1 @ sk9))),inference(paramod_ordered,[status(thm)],[1025,903])).
% 89.08/20.99 thf(1031,plain,((sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk6) | ((sk1 @ (sk5 @ sk7 @ sk8 @ sk9)) != (sk1 @ sk9))),inference(simp,[status(thm)],[1030])).
% 89.08/20.99 thf(1038,plain,((sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk7 != sk6) | ((sk5 @ sk7 @ sk8 @ sk9) != sk9)),inference(simp,[status(thm)],[1031])).
% 89.08/20.99 thf(1125,plain,(! [A:$i] : ((relr @ A @ (sk11 @ A @ (prop_a))) | (prop_a @ A))),inference(prim_subst,[status(thm)],[28:[bind(A, $thf(prop_a))]])).
% 89.08/20.99 thf(1220,plain,(! [A:$i] : ((relr @ A @ (sk11 @ A @ (prop_a))) | (prop_a @ A))),inference(simp,[status(thm)],[1125])).
% 89.08/20.99 thf(30,plain,(! [B:$i,A:($i > $o)] : ((~ ((sk11 @ B @ (A)) = (sk11 @ B @ ((=) @ $i @ (sk11 @ B @ A))))) | ((sk11 @ B @ (A)) = B))),inference(replace_leibeq,[status(thm)],[29:[bind(A, $thf((=) @ $i @ (sk11 @ B @ A)))]])).
% 89.08/20.99 thf(31,plain,(! [B:$i,A:($i > $o)] : (((sk11 @ B @ (A)) != (sk11 @ B @ ((=) @ $i @ (sk11 @ B @ A)))) | ((sk11 @ B @ (A)) = B))),inference(lifteq,[status(thm)],[30])).
% 89.08/20.99 thf(1445,plain,(! [C:$i,B:$i,A:($i > $o)] : ((relr @ B @ (sk11 @ B @ (A))) | ~ (($true)) | (prop_c @ C) | ((A @ B) != (prop_c @ (sk11 @ C @ (prop_c)))))),inference(paramod_ordered,[status(thm)],[28,1425])).
% 89.08/20.99 thf(1446,plain,(! [C:$i,B:$i,A:($i > $o)] : ((relr @ B @ (sk11 @ B @ (A))) | (prop_c @ C) | ((A @ B) != (prop_c @ (sk11 @ C @ (prop_c)))))),inference(simp,[status(thm)],[1445])).
% 89.08/20.99 thf(1449,plain,(! [A:$i] : ((relr @ (sk11 @ A @ (prop_c)) @ (sk11 @ (sk11 @ A @ (prop_c)) @ (prop_c))) | (prop_c @ A))),inference(pre_uni,[status(thm)],[1446:[bind(A, $thf(prop_c)),bind(B, $thf(sk11 @ C @ (prop_c))),bind(C, $thf(C))]])).
% 89.08/20.99 thf(1453,plain,(! [A:$i] : ((relr @ (sk11 @ A @ (prop_c)) @ (sk11 @ (sk11 @ A @ (prop_c)) @ (prop_c))) | (prop_c @ A))),inference(simp,[status(thm)],[1449])).
% 89.08/20.99 thf(487,plain,(! [A:$i] : ((reli @ A @ (sk10 @ A @ (prop_b))) | (prop_b @ A))),inference(prim_subst,[status(thm)],[22:[bind(A, $thf(prop_b))]])).
% 89.08/20.99 thf(588,plain,(! [A:$i] : ((reli @ A @ (sk10 @ A @ (prop_b))) | (prop_b @ A))),inference(simp,[status(thm)],[487])).
% 89.08/20.99 thf(1298,plain,(~ (($true)) | (sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk8 != sk7) | ((sk1 @ (sk5 @ sk7 @ sk8 @ sk9)) != (sk1 @ sk9))),inference(paramod_ordered,[status(thm)],[1025,1293])).
% 89.08/20.99 thf(1299,plain,((sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk8 != sk7) | ((sk1 @ (sk5 @ sk7 @ sk8 @ sk9)) != (sk1 @ sk9))),inference(simp,[status(thm)],[1298])).
% 89.08/20.99 thf(1308,plain,((sk8 != sk4) | (sk9 != sk7) | (sk8 != sk6) | (sk8 != sk7) | ((sk5 @ sk7 @ sk8 @ sk9) != sk9)),inference(simp,[status(thm)],[1299])).
% 89.08/20.99 thf(1057,plain,(! [C:$i,B:$i,A:($i > $o)] : ((relr @ B @ (sk11 @ B @ (A))) | ~ (($true)) | (prop_a @ C) | ((A @ B) != (prop_a @ (sk10 @ C @ (prop_a)))))),inference(paramod_ordered,[status(thm)],[28,316])).
% 89.08/20.99 thf(1058,plain,(! [C:$i,B:$i,A:($i > $o)] : ((relr @ B @ (sk11 @ B @ (A))) | (prop_a @ C) | ((A @ B) != (prop_a @ (sk10 @ C @ (prop_a)))))),inference(simp,[status(thm)],[1057])).
% 89.08/20.99 thf(1138,plain,(! [A:$i] : ((relr @ (sk10 @ A @ (prop_a)) @ (sk11 @ (sk10 @ A @ (prop_a)) @ (prop_a))) | (prop_a @ A))),inference(pre_uni,[status(thm)],[1058:[bind(A, $thf(prop_a)),bind(B, $thf(sk10 @ C @ (prop_a))),bind(C, $thf(C))]])).
% 89.08/20.99 thf(1229,plain,(! [A:$i] : ((relr @ (sk10 @ A @ (prop_a)) @ (sk11 @ (sk10 @ A @ (prop_a)) @ (prop_a))) | (prop_a @ A))),inference(simp,[status(thm)],[1138])).
% 89.08/20.99 thf(22597,plain,(($false)),inference(e,[status(thm)],[10,4216,1210,1187,1293,1172,4201,1729,308,379,4215,2082,37,25,14,587,1455,20,1479,316,1232,29,1465,4297,321,1215,660,598,4493,28,38,1425,356,124,1214,13,1429,2570,17,32,34,562,22,44,577,12,86,1524,318,521,1477,4497,35,1467,553,1025,18,4200,16,1038,1220,31,903,1453,588,26,23,8,1308,1229,19,15,1431,4221])).
% 89.08/20.99 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 89.08/20.99 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------