%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SWV107^7 : TPTP v9.3.1. Released v5.5.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 : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:39:51 AM UTC 2026
% Result : Theorem 34.86s 11.30s
% Output : Refutation 35.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV107^7 : TPTP v9.3.1. Released v5.5.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.22 % Computer : n005.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Tue Sep 29 16:00:38 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
% 1.00/0.81 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.23/1.24 % [INFO] Parsing done (425ms).
% 2.23/1.26 % [INFO] Running in sequential loop mode.
% 3.76/1.76 % [INFO] eprover registered as external prover.
% 3.76/1.76 % [INFO] Scanning for conjecture ...
% 4.52/2.04 % [INFO] Found a conjecture (or negated_conjecture) and 184 axioms. Running axiom selection ...
% 5.14/2.20 % [INFO] Axiom selection finished. Selected 184 axioms (removed 0 axioms).
% 5.41/2.39 % [INFO] Problem is higher-order (TPTP THF).
% 5.74/2.41 % [INFO] Type checking passed.
% 5.74/2.42 % [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 ...
% 34.36/11.30 % External prover 'e' found a proof!
% 34.36/11.30 % [INFO] Killing All external provers ...
% 34.86/11.30 % Time passed: 10932ms (effective reasoning time: 10027ms)
% 34.86/11.30 % 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)>
% 34.86/11.30 % Axioms used in derivation (184): gt_6_0, existence_of_n4_ax, gt_999_1, sel3_update_2, gt_6_1, sum_substitution_1, sel2_update_2, succ_plus_5_l, existence_of_tptp_update2_ax, lt_gt, existence_of_n999_ax, gt_5_tptp_minus_1, succ_plus_3_r, tptp_const_array2_substitution_3, gt_4_3, transitivity_gt, tptp_update3_substitution_1, existence_of_dim_ax, gt_6_4, matrix_symm_inv, existence_of_a_select3_ax, existence_of_n3_ax, finite_domain_1, gt_5_0, a_select3_substitution_1, const_array2_select, matrix_symm_trans, existence_of_n1_ax, finite_domain_6, gt_2_tptp_minus_1, gt_6_tptp_minus_1, existence_of_tptp_const_array2_ax, dim_substitution_1, sel3_update_3, leq_geq, gt_999_5, gt_1_0, leq_gt2, tptp_update2_substitution_2, gt_5_4, gt_999_0, succ_plus_1_l, existence_of_def_ax, gt_3_2, gt_substitution_2, matrix_symm_add, leq_succ_gt, finite_domain_5, tptp_madd_substitution_2, pred_minus_1, a_select2_substitution_1, gt_6_5, successor_3, existence_of_n0_ax, gt_3_tptp_minus_1, tptp_mmul_substitution_1, matrix_symm_update_diagonal, existence_of_minus_ax, sel2_update_1, sum_substitution_2, existence_of_n2_ax, tptp_update3_substitution_2, gt_999_6, geq_substitution_2, uniform_int_rnd_substitution_2, ttrue, pred_substitution_1, gt_4_2, matrix_symm_sub, existence_of_inv_ax, gt_5_3, gt_999_2, successor_4, gt_succ, succ_plus_4_l, reflexivity_leq, plus_substitution_2, existence_of_tptp_float_0_0_ax, successor_2, leq_gt1, gt_1_tptp_minus_1, finite_domain_2, matrix_symm_aba1, matrix_symm_aba2, gt_substitution_1, tptp_update2_substitution_1, succ_tptp_minus_1, existence_of_a_select2_ax, tptp_const_array1_substitution_1, finite_domain_4, tptp_msub_substitution_1, reflexivity, cumulative_ax, succ_plus_5_r, tptp_const_array2_substitution_1, tptp_madd_substitution_1, plus_substitution_1, gt_0_tptp_minus_1, leq_succ_succ, sum_plus_base_float, succ_plus_2_l, succ_substitution_1, tptp_update3_substitution_4, gt_999_3, existence_of_pred_ax, gt_3_1, gt_4_1, sum_substitution_3, gt_2_0, tptp_update3_substitution_3, gt_5_2, gt_999_tptp_minus_1, minus_substitution_1, const_array1_select, defuse, leq_gt_pred, matrix_symm_joseph_update, leq_substitution_1, existence_of_n6_ax, existence_of_tptp_mmul_ax, geq_substitution_1, uniform_int_rnd_substitution_1, existence_of_uniform_int_rnd_ax, succ_pred, trans_substitution_1, existence_of_n5_ax, totality, successor_6, lt_substitution_1, existence_of_plus_ax, existence_of_tptp_madd_ax, transitivity_leq, finite_domain_3, a_select3_substitution_3, existence_of_use_ax, uniform_int_rand_ranges_lo, gt_6_3, existence_of_tptp_minus_1_ax, existence_of_succ_ax, sel3_update_1, successor_1, existence_of_trans_ax, leq_substitution_2, sum_plus_base, irreflexivity_gt, existence_of_tptp_update3_ax, tptp_const_array1_substitution_2, successor_5, a1, nonempty_ax, gt_3_0, sel2_update_3, pred_succ, gt_999_4, tptp_const_array2_substitution_2, succ_plus_1_r, succ_plus_3_l, gt_4_tptp_minus_1, existence_of_tptp_msub_ax, existence_of_sum_ax, succ_plus_4_r, transitivity, a_select3_substitution_2, existence_of_tptp_const_array1_ax, gt_4_0, succ_plus_2_r, tptp_mmul_substitution_2, leq_succ_gt_equiv, tptp_msub_substitution_2, gt_5_1, gt_6_2, lt_substitution_2, uniform_int_rand_ranges_hi, tptp_update2_substitution_3, gt_2_1, minus_substitution_2, a2, inv_substitution_1, dim_substitution_2, a_select2_substitution_2, finite_domain_0, leq_succ, leq_minus, symmetry
% 34.86/11.30 % No. of inferences in proof: 372
% 34.86/11.30 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 10932 ms resp. 10027 ms w/o parsing
% 35.93/11.88 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.93/11.88 thf(mu_type, type, mu: $tType).
% 35.93/11.88 thf(qmltpeq_decl, type, qmltpeq: (mu > (mu > ($i > $o)))).
% 35.93/11.88 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 35.93/11.88 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 35.93/11.88 thf(mand_decl, type, mand: (($i > $o) > (($i > $o) > ($i > $o)))).
% 35.93/11.88 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 35.93/11.88 thf(exists_in_world_decl, type, exists_in_world: (mu > ($i > $o))).
% 35.93/11.88 thf(mforall_ind_decl, type, mforall_ind: ((mu > ($i > $o)) > ($i > $o))).
% 35.93/11.88 thf(mreflexive_decl, type, mreflexive: (($i > ($i > $o)) > $o)).
% 35.93/11.88 thf(mtransitive_decl, type, mtransitive: (($i > ($i > $o)) > $o)).
% 35.93/11.88 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 35.93/11.88 thf(rel_s4_decl, type, rel_s4: ($i > ($i > $o))).
% 35.93/11.88 thf(mbox_s4_decl, type, mbox_s4: (($i > $o) > ($i > $o))).
% 35.93/11.88 thf(true_decl, type, true: ($i > $o)).
% 35.93/11.88 thf(lt_decl, type, lt: (mu > (mu > ($i > $o)))).
% 35.93/11.88 thf(geq_decl, type, geq: (mu > (mu > ($i > $o)))).
% 35.93/11.88 thf(gt_decl, type, gt: (mu > (mu > ($i > $o)))).
% 35.93/11.88 thf(leq_decl, type, leq: (mu > (mu > ($i > $o)))).
% 35.93/11.88 thf(uniform_int_rnd_decl, type, uniform_int_rnd: (mu > (mu > mu))).
% 35.93/11.88 thf(tptp_const_array1_decl, type, tptp_const_array1: (mu > (mu > mu))).
% 35.93/11.88 thf(dim_decl, type, dim: (mu > (mu > mu))).
% 35.93/11.88 thf(tptp_const_array2_decl, type, tptp_const_array2: (mu > (mu > (mu > mu)))).
% 35.93/11.88 thf(inv_decl, type, inv: (mu > mu)).
% 35.93/11.88 thf(tptp_msub_decl, type, tptp_msub: (mu > (mu > mu))).
% 35.93/11.88 thf(trans_decl, type, trans: (mu > mu)).
% 35.93/11.88 thf(tptp_mmul_decl, type, tptp_mmul: (mu > (mu > mu))).
% 35.93/11.88 thf(tptp_madd_decl, type, tptp_madd: (mu > (mu > mu))).
% 35.93/11.88 thf(sum_decl, type, sum: (mu > (mu > (mu > mu)))).
% 35.93/11.88 thf(tptp_float_0_0_decl, type, tptp_float_0_0: mu).
% 35.93/11.88 thf(plus_decl, type, plus: (mu > (mu > mu))).
% 35.93/11.88 thf(pred_decl, type, pred: (mu > mu)).
% 35.93/11.88 thf(tptp_update3_decl, type, tptp_update3: (mu > (mu > (mu > (mu > mu))))).
% 35.93/11.88 thf(a_select3_decl, type, a_select3: (mu > (mu > (mu > mu)))).
% 35.93/11.88 thf(tptp_update2_decl, type, tptp_update2: (mu > (mu > (mu > mu)))).
% 35.93/11.88 thf(a_select2_decl, type, a_select2: (mu > (mu > mu))).
% 35.93/11.88 thf(use_decl, type, use: mu).
% 35.93/11.88 thf(def_decl, type, def: mu).
% 35.93/11.88 thf(minus_decl, type, minus: (mu > (mu > mu))).
% 35.93/11.88 thf(tptp_minus_1_decl, type, tptp_minus_1: mu).
% 35.93/11.88 thf(n999_decl, type, n999: mu).
% 35.93/11.88 thf(n4_decl, type, n4: mu).
% 35.93/11.88 thf(n5_decl, type, n5: mu).
% 35.93/11.88 thf(n6_decl, type, n6: mu).
% 35.93/11.88 thf(n1_decl, type, n1: mu).
% 35.93/11.88 thf(n2_decl, type, n2: mu).
% 35.93/11.88 thf(n3_decl, type, n3: mu).
% 35.93/11.88 thf(n0_decl, type, n0: mu).
% 35.93/11.88 thf(succ_decl, type, succ: (mu > mu)).
% 35.93/11.88 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 35.93/11.88 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 35.93/11.88 thf(mand_def, definition, mand = (^ [A:($i > $o),B:($i > $o)]: (mnot @ (mor @ (mnot @ A) @ (mnot @ B)))) ).
% 35.93/11.88 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 35.93/11.88 thf(mforall_ind_def, definition, mforall_ind = (^ [A:(mu > ($i > $o)),B:$i]: ! [C:mu]: ((exists_in_world @ C @ B) => (A @ C @ B))) ).
% 35.93/11.88 thf(mreflexive_def, definition, mreflexive = (^ [A:($i > ($i > $o))]: ! [B:$i]: (A @ B @ B)) ).
% 35.93/11.88 thf(mtransitive_def, definition, mtransitive = (^ [A:($i > ($i > $o))]: ! [B:$i,C:$i,D:$i]: (((A @ B @ C) & (A @ C @ D)) => (A @ B @ D))) ).
% 35.93/11.88 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 35.93/11.88 thf(mbox_s4_def, definition, mbox_s4 = (^ [A:($i > $o),B:$i]: ! [C:$i]: (~ (rel_s4 @ B @ C) | (A @ C))) ).
% 35.93/11.88 thf(60,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (a_select2 @ C @ A) @ (a_select2 @ C @ B)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_select2_substitution_2)).
% 35.93/11.88 thf(479,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (a_select2 @ G @ C) @ (a_select2 @ G @ E) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 35.93/11.88 thf(172,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (gt @ A @ C))) @ (mbox_s4 @ (gt @ B @ C))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_substitution_1)).
% 35.93/11.88 thf(1083,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (gt @ C @ G @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (gt @ E @ G @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 35.93/11.88 thf(132,axiom,((mvalid @ (mbox_s4 @ (gt @ n999 @ n1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_999_1)).
% 35.93/11.88 thf(941,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n999 @ n1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 35.93/11.88 thf(85,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ A @ B)) @ (mbox_s4 @ (mnot @ (mbox_s4 @ (qmltpeq @ A @ B))))) @ (mbox_s4 @ (gt @ B @ A)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_gt2)).
% 35.93/11.88 thf(628,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ C @ E @ G))) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | ~ (! [H:$i]: (~ (rel_s4 @ G @ H) | (qmltpeq @ C @ E @ H))))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (gt @ E @ C @ G))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 35.93/11.88 thf(157,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_madd @ C @ A) @ (tptp_madd @ C @ B)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_madd_substitution_2)).
% 35.93/11.88 thf(1031,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (tptp_madd @ G @ C) @ (tptp_madd @ G @ E) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 35.93/11.88 thf(20,axiom,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (uniform_int_rnd @ B @ C) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_uniform_int_rnd_ax)).
% 35.93/11.88 thf(249,plain,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (uniform_int_rnd @ B @ C) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 35.93/11.88 thf(144,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (inv @ A) @ (inv @ B))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',inv_substitution_1)).
% 35.93/11.88 thf(977,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (qmltpeq @ C @ E @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (qmltpeq @ (inv @ C) @ (inv @ E) @ G))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 35.93/11.88 thf(4,axiom,((! [A:$i,B:mu]: (exists_in_world @ (pred @ B) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_pred_ax)).
% 35.93/11.88 thf(217,plain,((! [A:$i,B:mu]: (exists_in_world @ (pred @ B) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 35.93/11.88 thf(169,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_const_array1 @ A @ C) @ (tptp_const_array1 @ B @ C)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_const_array1_substitution_1)).
% 35.93/11.88 thf(1073,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (tptp_const_array1 @ C @ G) @ (tptp_const_array1 @ E @ G) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 35.93/11.88 thf(51,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (leq @ n0 @ A)) @ (mbox_s4 @ (leq @ (uniform_int_rnd @ B @ A) @ A)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',uniform_int_rand_ranges_hi)).
% 35.93/11.88 thf(449,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ n0 @ C @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ (uniform_int_rnd @ E @ C) @ C @ G))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 35.93/11.88 thf(19,axiom,((! [A:$i,B:mu,C:mu,D:mu]: (exists_in_world @ (tptp_update2 @ B @ C @ D) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_tptp_update2_ax)).
% 35.93/11.88 thf(247,plain,((! [A:$i,B:mu,C:mu,D:mu]: (exists_in_world @ (tptp_update2 @ B @ C @ D) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 35.93/11.88 thf(70,axiom,((mvalid @ (mbox_s4 @ (gt @ n1 @ n0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_1_0)).
% 35.93/11.88 thf(511,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n1 @ n0 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 35.93/11.88 thf(161,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (minus @ C @ A) @ (minus @ C @ B)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',minus_substitution_2)).
% 35.93/11.88 thf(1041,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (minus @ G @ C) @ (minus @ G @ E) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 35.93/11.88 thf(134,axiom,((mvalid @ (mbox_s4 @ true))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ttrue)).
% 35.93/11.88 thf(945,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (true @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 35.93/11.88 thf(96,axiom,((mvalid @ (mbox_s4 @ (gt @ n999 @ n4)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_999_4)).
% 35.93/11.88 thf(670,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n999 @ n4 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 35.93/11.88 thf(152,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (qmltpeq @ (plus @ A @ n5) @ (succ @ (succ @ (succ @ (succ @ (succ @ A)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_5_r)).
% 35.93/11.88 thf(1001,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (qmltpeq @ (plus @ C @ n5) @ (succ @ (succ @ (succ @ (succ @ (succ @ C))))) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 35.93/11.88 thf(185,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mnot @ (mbox_s4 @ (gt @ A @ A))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',irreflexivity_gt)).
% 35.93/11.88 thf(1127,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (gt @ C @ C @ E))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 35.93/11.88 thf(118,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (qmltpeq @ (plus @ n3 @ A) @ (succ @ (succ @ (succ @ A)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_3_l)).
% 35.93/11.88 thf(841,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (qmltpeq @ (plus @ n3 @ C) @ (succ @ (succ @ (succ @ C))) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 35.93/11.88 thf(142,axiom,((mvalid @ (mbox_s4 @ (gt @ n4 @ n1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_1)).
% 35.93/11.88 thf(973,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n4 @ n1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 35.93/11.88 thf(24,axiom,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (tptp_const_array1 @ B @ C) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_tptp_const_array1_ax)).
% 35.93/11.88 thf(257,plain,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (tptp_const_array1 @ B @ C) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 35.93/11.88 thf(166,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (lt @ C @ A))) @ (mbox_s4 @ (lt @ C @ B))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',lt_substitution_2)).
% 35.93/11.88 thf(1059,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (lt @ G @ C @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (lt @ G @ E @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 35.93/11.88 thf(136,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mand @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (leq @ A @ B)) @ (mbox_s4 @ (gt @ (succ @ B) @ A)))) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (gt @ (succ @ B) @ A)) @ (mbox_s4 @ (leq @ A @ B))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_succ_gt_equiv)).
% 35.93/11.88 thf(949,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (~ (~ (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ C @ E @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (gt @ (succ @ E) @ C @ G)))) | ~ (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (gt @ (succ @ E) @ C @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ C @ E @ G))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 35.93/11.88 thf(45,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_update2 @ A @ C @ D) @ (tptp_update2 @ B @ C @ D))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_update2_substitution_1)).
% 35.93/11.88 thf(421,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ C @ E @ K))) | ! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ (tptp_update2 @ C @ G @ I) @ (tptp_update2 @ E @ G @ I) @ K))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 35.93/11.88 thf(81,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ D)) @ (mand @ (mbox_s4 @ (leq @ D @ C)) @ (mand @ (mbox_s4 @ (leq @ n0 @ E)) @ (mbox_s4 @ (leq @ E @ C))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ B @ D @ E) @ (a_select3 @ B @ E @ D))))))))))) @ (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ D)) @ (mand @ (mbox_s4 @ (leq @ D @ C)) @ (mand @ (mbox_s4 @ (leq @ n0 @ E)) @ (mbox_s4 @ (leq @ E @ C))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ (tptp_mmul @ A @ (tptp_mmul @ B @ (trans @ A))) @ D @ E) @ (a_select3 @ (tptp_mmul @ A @ (tptp_mmul @ B @ (trans @ A))) @ E @ D)))))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',matrix_symm_aba1)).
% 35.93/11.88 thf(606,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | ! [J:mu]: ((exists_in_world @ J @ I) => (! [K:$i]: (~ (rel_s4 @ I @ K) | ! [L:mu]: ((exists_in_world @ L @ K) => (! [M:$i]: (~ (rel_s4 @ K @ M) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ J @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ J @ G @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ L @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ L @ G @ N))) | ! [N:$i]: (~ (rel_s4 @ M @ N) | (qmltpeq @ (a_select3 @ E @ J @ L) @ (a_select3 @ E @ L @ J) @ N)))))))))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | ! [J:mu]: ((exists_in_world @ J @ I) => (! [K:$i]: (~ (rel_s4 @ I @ K) | ! [L:mu]: ((exists_in_world @ L @ K) => (! [M:$i]: (~ (rel_s4 @ K @ M) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ J @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ J @ G @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ L @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ L @ G @ N))) | ! [N:$i]: (~ (rel_s4 @ M @ N) | (qmltpeq @ (a_select3 @ (tptp_mmul @ C @ (tptp_mmul @ E @ (trans @ C))) @ J @ L) @ (a_select3 @ (tptp_mmul @ C @ (tptp_mmul @ E @ (trans @ C))) @ L @ J) @ N))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 35.93/11.88 thf(122,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ A)) @ (mbox_s4 @ (leq @ A @ n2))) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n0)) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n1)) @ (mbox_s4 @ (qmltpeq @ A @ n2))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_2)).
% 35.93/11.88 thf(881,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (leq @ n0 @ C @ E))) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (leq @ C @ n2 @ E))) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n0 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n1 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n2 @ E)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 35.93/11.88 thf(180,axiom,((mvalid @ (mbox_s4 @ (gt @ n999 @ tptp_minus_1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_999_tptp_minus_1)).
% 35.93/11.88 thf(1115,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n999 @ tptp_minus_1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 35.93/11.88 thf(26,axiom,((! [A:$i]: (exists_in_world @ use @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_use_ax)).
% 35.93/11.88 thf(261,plain,((! [A:$i]: (exists_in_world @ use @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 35.93/11.88 thf(59,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (uniform_int_rnd @ C @ A) @ (uniform_int_rnd @ C @ B)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',uniform_int_rnd_substitution_2)).
% 35.93/11.88 thf(475,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (uniform_int_rnd @ G @ C) @ (uniform_int_rnd @ G @ E) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 35.93/11.88 thf(62,axiom,((! [A:mu,B:$i,C:$i]: (((exists_in_world @ A @ B) & (rel_s4 @ B @ C)) => (exists_in_world @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',cumulative_ax)).
% 35.93/11.88 thf(485,plain,((! [A:mu,B:$i,C:$i]: (((exists_in_world @ A @ B) & (rel_s4 @ B @ C)) => (exists_in_world @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 35.93/11.88 thf(130,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (gt @ (succ @ A) @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_succ)).
% 35.93/11.88 thf(937,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (gt @ (succ @ C) @ C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 35.93/11.88 thf(112,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_update2 @ C @ A @ D) @ (tptp_update2 @ C @ B @ D))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_update2_substitution_2)).
% 35.93/11.88 thf(821,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ C @ E @ K))) | ! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ (tptp_update2 @ G @ C @ I) @ (tptp_update2 @ G @ E @ I) @ K))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 35.93/11.88 thf(178,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_update3 @ C @ D @ A @ E) @ (tptp_update3 @ C @ D @ B @ E)))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_update3_substitution_3)).
% 35.93/11.88 thf(1109,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ! [K:mu]: ((exists_in_world @ K @ J) => (! [L:$i]: (~ (rel_s4 @ J @ L) | ~ (! [M:$i]: (~ (rel_s4 @ L @ M) | (qmltpeq @ C @ E @ M))) | ! [M:$i]: (~ (rel_s4 @ L @ M) | (qmltpeq @ (tptp_update3 @ G @ I @ C @ K) @ (tptp_update3 @ G @ I @ E @ K) @ M)))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 35.93/11.88 thf(32,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ C)) @ (mand @ (mbox_s4 @ (leq @ C @ B)) @ (mand @ (mbox_s4 @ (leq @ n0 @ D)) @ (mbox_s4 @ (leq @ D @ B))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ A @ C @ D) @ (a_select3 @ A @ D @ C))))))))))) @ (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mforall_ind @ (^ [F:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ C)) @ (mand @ (mbox_s4 @ (leq @ C @ B)) @ (mand @ (mbox_s4 @ (leq @ n0 @ D)) @ (mand @ (mbox_s4 @ (leq @ D @ B)) @ (mand @ (mbox_s4 @ (leq @ n0 @ E)) @ (mbox_s4 @ (leq @ E @ B))))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ (tptp_update3 @ A @ E @ E @ F) @ C @ D) @ (a_select3 @ (tptp_update3 @ A @ E @ E @ F) @ D @ C))))))))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',matrix_symm_update_diagonal)).
% 35.93/11.88 thf(321,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | ! [H:mu]: ((exists_in_world @ H @ G) => (! [I:$i]: (~ (rel_s4 @ G @ I) | ! [J:mu]: ((exists_in_world @ J @ I) => (! [K:$i]: (~ (rel_s4 @ I @ K) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ n0 @ H @ L))) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ H @ E @ L))) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ n0 @ J @ L))) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ J @ E @ L))) | ! [L:$i]: (~ (rel_s4 @ K @ L) | (qmltpeq @ (a_select3 @ C @ H @ J) @ (a_select3 @ C @ J @ H) @ L)))))))))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | ! [H:mu]: ((exists_in_world @ H @ G) => (! [I:$i]: (~ (rel_s4 @ G @ I) | ! [J:mu]: ((exists_in_world @ J @ I) => (! [K:$i]: (~ (rel_s4 @ I @ K) | ! [L:mu]: ((exists_in_world @ L @ K) => (! [M:$i]: (~ (rel_s4 @ K @ M) | ! [N:mu]: ((exists_in_world @ N @ M) => (! [O:$i]: (~ (rel_s4 @ M @ O) | ~ (! [P:$i]: (~ (rel_s4 @ O @ P) | (leq @ n0 @ H @ P))) | ~ (! [P:$i]: (~ (rel_s4 @ O @ P) | (leq @ H @ E @ P))) | ~ (! [P:$i]: (~ (rel_s4 @ O @ P) | (leq @ n0 @ J @ P))) | ~ (! [P:$i]: (~ (rel_s4 @ O @ P) | (leq @ J @ E @ P))) | ~ (! [P:$i]: (~ (rel_s4 @ O @ P) | (leq @ n0 @ L @ P))) | ~ (! [P:$i]: (~ (rel_s4 @ O @ P) | (leq @ L @ E @ P))) | ! [P:$i]: (~ (rel_s4 @ O @ P) | (qmltpeq @ (a_select3 @ (tptp_update3 @ C @ L @ L @ N) @ H @ J) @ (a_select3 @ (tptp_update3 @ C @ L @ L @ N) @ J @ H) @ P)))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 35.93/11.88 thf(89,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (leq @ A @ C))) @ (mbox_s4 @ (leq @ B @ C))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_substitution_1)).
% 35.93/11.88 thf(646,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (leq @ C @ G @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (leq @ E @ G @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 35.93/11.88 thf(22,axiom,((! [A:$i,B:mu]: (exists_in_world @ (succ @ B) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_succ_ax)).
% 35.93/11.88 thf(253,plain,((! [A:$i,B:mu]: (exists_in_world @ (succ @ B) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 35.93/11.88 thf(6,axiom,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (tptp_msub @ B @ C) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_tptp_msub_ax)).
% 35.93/11.88 thf(221,plain,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (tptp_msub @ B @ C) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 35.93/11.88 thf(52,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (trans @ A) @ (trans @ B))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',trans_substitution_1)).
% 35.93/11.88 thf(453,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (qmltpeq @ C @ E @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (qmltpeq @ (trans @ C) @ (trans @ E) @ G))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 35.93/11.88 thf(92,axiom,((mvalid @ (mbox_s4 @ (qmltpeq @ (succ @ n0) @ n1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_1)).
% 35.93/11.88 thf(660,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (qmltpeq @ (succ @ n0) @ n1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 35.93/11.88 thf(43,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (leq @ (minus @ A @ B) @ A)) @ (mbox_s4 @ (leq @ n0 @ B)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_minus)).
% 35.93/11.88 thf(411,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ (minus @ C @ E) @ C @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ n0 @ E @ G))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 35.93/11.88 thf(17,axiom,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (dim @ B @ C) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_dim_ax)).
% 35.93/11.88 thf(243,plain,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (dim @ B @ C) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 35.93/11.88 thf(121,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ D)) @ (mand @ (mbox_s4 @ (leq @ D @ C)) @ (mand @ (mbox_s4 @ (leq @ n0 @ E)) @ (mbox_s4 @ (leq @ E @ C))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ A @ D @ E) @ (a_select3 @ A @ E @ D))))))))))) @ (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ D)) @ (mand @ (mbox_s4 @ (leq @ D @ C)) @ (mand @ (mbox_s4 @ (leq @ n0 @ E)) @ (mbox_s4 @ (leq @ E @ C))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ B @ D @ E) @ (a_select3 @ B @ E @ D)))))))))))) @ (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ D)) @ (mand @ (mbox_s4 @ (leq @ D @ C)) @ (mand @ (mbox_s4 @ (leq @ n0 @ E)) @ (mbox_s4 @ (leq @ E @ C))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ (tptp_msub @ A @ B) @ D @ E) @ (a_select3 @ (tptp_msub @ A @ B) @ E @ D)))))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',matrix_symm_sub)).
% 35.93/11.88 thf(849,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | ! [J:mu]: ((exists_in_world @ J @ I) => (! [K:$i]: (~ (rel_s4 @ I @ K) | ! [L:mu]: ((exists_in_world @ L @ K) => (! [M:$i]: (~ (rel_s4 @ K @ M) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ J @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ J @ G @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ L @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ L @ G @ N))) | ! [N:$i]: (~ (rel_s4 @ M @ N) | (qmltpeq @ (a_select3 @ C @ J @ L) @ (a_select3 @ C @ L @ J) @ N)))))))))) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | ! [J:mu]: ((exists_in_world @ J @ I) => (! [K:$i]: (~ (rel_s4 @ I @ K) | ! [L:mu]: ((exists_in_world @ L @ K) => (! [M:$i]: (~ (rel_s4 @ K @ M) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ J @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ J @ G @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ L @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ L @ G @ N))) | ! [N:$i]: (~ (rel_s4 @ M @ N) | (qmltpeq @ (a_select3 @ E @ J @ L) @ (a_select3 @ E @ L @ J) @ N)))))))))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | ! [J:mu]: ((exists_in_world @ J @ I) => (! [K:$i]: (~ (rel_s4 @ I @ K) | ! [L:mu]: ((exists_in_world @ L @ K) => (! [M:$i]: (~ (rel_s4 @ K @ M) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ J @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ J @ G @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ L @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ L @ G @ N))) | ! [N:$i]: (~ (rel_s4 @ M @ N) | (qmltpeq @ (a_select3 @ (tptp_msub @ C @ E) @ J @ L) @ (a_select3 @ (tptp_msub @ C @ E) @ L @ J) @ N))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 35.93/11.88 thf(79,axiom,((mvalid @ (mbox_s4 @ (gt @ n6 @ n2)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_2)).
% 35.93/11.88 thf(602,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n6 @ n2 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 35.93/11.88 thf(145,axiom,((mvalid @ (mbox_s4 @ (gt @ n2 @ n0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_2_0)).
% 35.93/11.88 thf(981,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n2 @ n0 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 35.93/11.88 thf(12,axiom,((! [A:$i]: (exists_in_world @ tptp_minus_1 @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_tptp_minus_1_ax)).
% 35.93/11.88 thf(233,plain,((! [A:$i]: (exists_in_world @ tptp_minus_1 @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 35.93/11.88 thf(99,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_update3 @ C @ D @ E @ A) @ (tptp_update3 @ C @ D @ E @ B)))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_update3_substitution_4)).
% 35.93/11.88 thf(678,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ! [K:mu]: ((exists_in_world @ K @ J) => (! [L:$i]: (~ (rel_s4 @ J @ L) | ~ (! [M:$i]: (~ (rel_s4 @ L @ M) | (qmltpeq @ C @ E @ M))) | ! [M:$i]: (~ (rel_s4 @ L @ M) | (qmltpeq @ (tptp_update3 @ G @ I @ K @ C) @ (tptp_update3 @ G @ I @ K @ E) @ M)))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 35.93/11.88 thf(36,axiom,((! [A:$i]: (exists_in_world @ n2 @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_n2_ax)).
% 35.93/11.88 thf(381,plain,((! [A:$i]: (exists_in_world @ n2 @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 35.93/11.88 thf(168,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (geq @ A @ C))) @ (mbox_s4 @ (geq @ B @ C))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',geq_substitution_1)).
% 35.93/11.88 thf(1067,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (geq @ C @ G @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (geq @ E @ G @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 35.93/11.88 thf(163,axiom,((mvalid @ (mbox_s4 @ (gt @ n999 @ n0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_999_0)).
% 35.93/11.88 thf(1047,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n999 @ n0 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 35.93/11.88 thf(137,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_msub @ C @ A) @ (tptp_msub @ C @ B)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_msub_substitution_2)).
% 35.93/11.88 thf(957,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (tptp_msub @ G @ C) @ (tptp_msub @ G @ E) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 35.93/11.88 thf(174,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (mnot @ (mbox_s4 @ (qmltpeq @ A @ B)))) @ (mbox_s4 @ (qmltpeq @ (a_select2 @ C @ B) @ D))) @ (mbox_s4 @ (qmltpeq @ (a_select2 @ (tptp_update2 @ C @ A @ E) @ B) @ D))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',sel2_update_2)).
% 35.93/11.88 thf(1091,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ! [K:mu]: ((exists_in_world @ K @ J) => (! [L:$i]: (~ (rel_s4 @ J @ L) | ~ (! [M:$i]: (~ (rel_s4 @ L @ M) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (qmltpeq @ C @ E @ N))))) | ~ (! [M:$i]: (~ (rel_s4 @ L @ M) | (qmltpeq @ (a_select2 @ G @ E) @ I @ M))) | ! [M:$i]: (~ (rel_s4 @ L @ M) | (qmltpeq @ (a_select2 @ (tptp_update2 @ G @ C @ K) @ E) @ I @ M)))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 35.93/11.88 thf(113,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (lt @ A @ C))) @ (mbox_s4 @ (lt @ B @ C))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',lt_substitution_1)).
% 35.93/11.88 thf(825,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (lt @ C @ G @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (lt @ E @ G @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 35.93/11.88 thf(183,axiom,((! [A:$i]: (exists_in_world @ n0 @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_n0_ax)).
% 35.93/11.88 thf(1123,plain,((! [A:$i]: (exists_in_world @ n0 @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 35.93/11.88 thf(47,axiom,((mvalid @ (mbox_s4 @ (gt @ n2 @ tptp_minus_1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_2_tptp_minus_1)).
% 35.93/11.88 thf(429,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n2 @ tptp_minus_1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 35.93/11.88 thf(110,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ C @ A @ D) @ (a_select3 @ C @ B @ D))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_select3_substitution_2)).
% 35.93/11.88 thf(815,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ C @ E @ K))) | ! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ (a_select3 @ G @ C @ I) @ (a_select3 @ G @ E @ I) @ K))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 35.93/11.88 thf(33,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mforall_ind @ (^ [F:mu]: (mbox_s4 @ (mforall_ind @ (^ [G:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ B @ A)) @ (mand @ (mbox_s4 @ (leq @ A @ C)) @ (mand @ (mbox_s4 @ (leq @ E @ D)) @ (mbox_s4 @ (leq @ D @ F))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ (tptp_const_array2 @ (dim @ B @ C) @ (dim @ E @ F) @ G) @ A @ D) @ G))))))))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',const_array2_select)).
% 35.93/11.88 thf(361,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ! [K:mu]: ((exists_in_world @ K @ J) => (! [L:$i]: (~ (rel_s4 @ J @ L) | ! [M:mu]: ((exists_in_world @ M @ L) => (! [N:$i]: (~ (rel_s4 @ L @ N) | ! [O:mu]: ((exists_in_world @ O @ N) => (! [P:$i]: (~ (rel_s4 @ N @ P) | ~ (! [Q:$i]: (~ (rel_s4 @ P @ Q) | (leq @ E @ C @ Q))) | ~ (! [Q:$i]: (~ (rel_s4 @ P @ Q) | (leq @ C @ G @ Q))) | ~ (! [Q:$i]: (~ (rel_s4 @ P @ Q) | (leq @ K @ I @ Q))) | ~ (! [Q:$i]: (~ (rel_s4 @ P @ Q) | (leq @ I @ M @ Q))) | ! [Q:$i]: (~ (rel_s4 @ P @ Q) | (qmltpeq @ (a_select3 @ (tptp_const_array2 @ (dim @ E @ G) @ (dim @ K @ M) @ O) @ C @ I) @ O @ Q)))))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 35.93/11.88 thf(124,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ A)) @ (mbox_s4 @ (leq @ A @ n3))) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n0)) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n1)) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n2)) @ (mbox_s4 @ (qmltpeq @ A @ n3)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_3)).
% 35.93/11.88 thf(889,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (leq @ n0 @ C @ E))) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (leq @ C @ n3 @ E))) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n0 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n1 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n2 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n3 @ E)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 35.93/11.88 thf(54,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (qmltpeq @ (plus @ A @ n2) @ (succ @ (succ @ A))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_2_r)).
% 35.93/11.88 thf(461,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (qmltpeq @ (plus @ C @ n2) @ (succ @ (succ @ C)) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 35.93/11.88 thf(171,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_update2 @ C @ D @ A) @ (tptp_update2 @ C @ D @ B))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_update2_substitution_3)).
% 35.93/11.88 thf(1079,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ C @ E @ K))) | ! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ (tptp_update2 @ G @ I @ C) @ (tptp_update2 @ G @ I @ E) @ K))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 35.93/11.88 thf(100,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mand @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (lt @ A @ B)) @ (mbox_s4 @ (gt @ B @ A)))) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (gt @ B @ A)) @ (mbox_s4 @ (lt @ A @ B))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',lt_gt)).
% 35.93/11.88 thf(682,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (~ (~ (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (lt @ C @ E @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (gt @ E @ C @ G)))) | ~ (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (gt @ E @ C @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (lt @ C @ E @ G))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 35.93/11.88 thf(10,axiom,((! [A:$i,B:mu]: (exists_in_world @ (trans @ B) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_trans_ax)).
% 35.93/11.88 thf(229,plain,((! [A:$i,B:mu]: (exists_in_world @ (trans @ B) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 35.93/11.88 thf(120,axiom,((mvalid @ (mbox_s4 @ (gt @ n5 @ n4)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_4)).
% 35.93/11.88 thf(847,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n5 @ n4 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 35.93/11.88 thf(173,axiom,((mvalid @ (mbox_s4 @ (gt @ n5 @ tptp_minus_1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_tptp_minus_1)).
% 35.93/11.88 thf(1089,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n5 @ tptp_minus_1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 35.93/11.88 thf(182,axiom,((mvalid @ (mbox_s4 @ (gt @ n3 @ n2)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_2)).
% 35.93/11.88 thf(1121,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n3 @ n2 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 35.93/11.88 thf(147,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_const_array2 @ A @ C @ D) @ (tptp_const_array2 @ B @ C @ D))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_const_array2_substitution_1)).
% 35.93/11.88 thf(989,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ C @ E @ K))) | ! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ (tptp_const_array2 @ C @ G @ I) @ (tptp_const_array2 @ E @ G @ I) @ K))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 35.93/11.88 thf(8,axiom,((! [A:$i,B:mu,C:mu,D:mu]: (exists_in_world @ (sum @ B @ C @ D) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_sum_ax)).
% 35.93/11.88 thf(225,plain,((! [A:$i,B:mu,C:mu,D:mu]: (exists_in_world @ (sum @ B @ C @ D) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 35.93/11.88 thf(128,axiom,((mvalid @ (mbox_s4 @ (gt @ n6 @ n1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_1)).
% 35.93/11.88 thf(933,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n6 @ n1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 35.93/11.88 thf(72,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_update3 @ A @ C @ D @ E) @ (tptp_update3 @ B @ C @ D @ E)))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_update3_substitution_1)).
% 35.93/11.88 thf(537,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ! [K:mu]: ((exists_in_world @ K @ J) => (! [L:$i]: (~ (rel_s4 @ J @ L) | ~ (! [M:$i]: (~ (rel_s4 @ L @ M) | (qmltpeq @ C @ E @ M))) | ! [M:$i]: (~ (rel_s4 @ L @ M) | (qmltpeq @ (tptp_update3 @ C @ G @ I @ K) @ (tptp_update3 @ E @ G @ I @ K) @ M)))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 35.93/11.88 thf(88,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (minus @ A @ C) @ (minus @ B @ C)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',minus_substitution_1)).
% 35.93/11.88 thf(642,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (minus @ C @ G) @ (minus @ E @ G) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 35.93/11.88 thf(64,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (qmltpeq @ (succ @ (pred @ A)) @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_pred)).
% 35.93/11.88 thf(489,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (qmltpeq @ (succ @ (pred @ C)) @ C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 35.93/11.88 thf(160,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (qmltpeq @ (plus @ A @ n1) @ (succ @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_1_r)).
% 35.93/11.88 thf(1039,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (qmltpeq @ (plus @ C @ n1) @ (succ @ C) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 35.93/11.88 thf(116,axiom,((mvalid @ (mbox_s4 @ (gt @ n999 @ n2)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_999_2)).
% 35.93/11.88 thf(837,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n999 @ n2 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 35.93/11.88 thf(39,axiom,((mvalid @ (mbox_s4 @ (gt @ n4 @ n0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_0)).
% 35.93/11.88 thf(393,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n4 @ n0 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 35.93/11.88 thf(150,axiom,((mreflexive @ rel_s4)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1)).
% 35.93/11.88 thf(997,plain,((! [A:$i]: (rel_s4 @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 35.93/11.88 thf(175,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mor @ (mbox_s4 @ (gt @ A @ B)) @ (mor @ (mbox_s4 @ (gt @ B @ A)) @ (mbox_s4 @ (qmltpeq @ A @ B)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',totality)).
% 35.93/11.88 thf(1099,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | (gt @ C @ E @ F)) | ! [F:$i]: (~ (rel_s4 @ D @ F) | (gt @ E @ C @ F)) | ! [F:$i]: (~ (rel_s4 @ D @ F) | (qmltpeq @ C @ E @ F)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 35.93/11.88 thf(186,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (qmltpeq @ (a_select2 @ (tptp_update2 @ A @ B @ C) @ B) @ C))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',sel2_update_1)).
% 35.93/11.88 thf(1131,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | (qmltpeq @ (a_select2 @ (tptp_update2 @ C @ E @ G) @ E) @ G @ H))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 35.93/11.88 thf(53,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_mmul @ C @ A) @ (tptp_mmul @ C @ B)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_mmul_substitution_2)).
% 35.93/11.88 thf(457,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (tptp_mmul @ G @ C) @ (tptp_mmul @ G @ E) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 35.93/11.88 thf(34,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (gt @ A @ B)) @ (mbox_s4 @ (gt @ B @ C))) @ (mbox_s4 @ (gt @ A @ C))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_gt)).
% 35.93/11.88 thf(371,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (gt @ C @ E @ I))) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (gt @ E @ G @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (gt @ C @ G @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 35.93/11.88 thf(68,axiom,((mvalid @ (mbox_s4 @ (gt @ n5 @ n3)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_3)).
% 35.93/11.88 thf(503,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n5 @ n3 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 35.93/11.88 thf(14,axiom,((! [A:$i,B:mu,C:mu,D:mu]: (exists_in_world @ (tptp_const_array2 @ B @ C @ D) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_tptp_const_array2_ax)).
% 35.93/11.88 thf(237,plain,((! [A:$i,B:mu,C:mu,D:mu]: (exists_in_world @ (tptp_const_array2 @ B @ C @ D) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 35.93/11.88 thf(73,axiom,((! [A:$i]: (exists_in_world @ n999 @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_n999_ax)).
% 35.93/11.88 thf(541,plain,((! [A:$i]: (exists_in_world @ n999 @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 35.93/11.88 thf(158,axiom,((mvalid @ (mbox_s4 @ (gt @ n4 @ n2)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_2)).
% 35.93/11.88 thf(1035,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n4 @ n2 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 35.93/11.88 thf(105,axiom,((mvalid @ (mbox_s4 @ (gt @ n3 @ tptp_minus_1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_tptp_minus_1)).
% 35.93/11.88 thf(773,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n3 @ tptp_minus_1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 35.93/11.88 thf(93,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (qmltpeq @ (plus @ A @ n4) @ (succ @ (succ @ (succ @ (succ @ A))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_4_r)).
% 35.93/11.88 thf(662,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (qmltpeq @ (plus @ C @ n4) @ (succ @ (succ @ (succ @ (succ @ C)))) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 35.93/11.88 thf(83,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ A)) @ (mbox_s4 @ (leq @ A @ n6))) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n0)) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n1)) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n2)) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n3)) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n4)) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n5)) @ (mbox_s4 @ (qmltpeq @ A @ n6))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_6)).
% 35.93/11.88 thf(618,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (leq @ n0 @ C @ E))) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (leq @ C @ n6 @ E))) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n0 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n1 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n2 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n3 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n4 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n5 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n6 @ E)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 35.93/11.88 thf(46,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (leq @ n0 @ A)) @ (mbox_s4 @ (leq @ n0 @ (uniform_int_rnd @ B @ A))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',uniform_int_rand_ranges_lo)).
% 35.93/11.88 thf(425,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ n0 @ C @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ n0 @ (uniform_int_rnd @ E @ C) @ G))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 35.93/11.88 thf(71,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ E)) @ (mbox_s4 @ (leq @ E @ B))) @ (mbox_s4 @ (qmltpeq @ (a_select2 @ C @ E) @ D))))))) @ (mand @ (mbox_s4 @ (leq @ n0 @ A)) @ (mbox_s4 @ (leq @ A @ B)))) @ (mbox_s4 @ (qmltpeq @ (a_select2 @ (tptp_update2 @ C @ B @ D) @ A) @ D)))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',sel2_update_3)).
% 35.93/11.88 thf(513,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | ! [L:mu]: ((exists_in_world @ L @ K) => (! [M:$i]: (~ (rel_s4 @ K @ M) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ L @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ L @ E @ N))) | ! [N:$i]: (~ (rel_s4 @ M @ N) | (qmltpeq @ (a_select2 @ G @ L) @ I @ N))))))) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | (leq @ n0 @ C @ K))) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | (leq @ C @ E @ K))) | ! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ (a_select2 @ (tptp_update2 @ G @ E @ I) @ C) @ I @ K))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 35.93/11.88 thf(30,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mforall_ind @ (^ [F:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (mforall_ind @ (^ [G:mu]: (mbox_s4 @ (mforall_ind @ (^ [H:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ G)) @ (mand @ (mbox_s4 @ (leq @ n0 @ H)) @ (mand @ (mbox_s4 @ (leq @ G @ C)) @ (mbox_s4 @ (leq @ H @ D))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ E @ G @ H) @ F)))))))))) @ (mand @ (mbox_s4 @ (leq @ n0 @ A)) @ (mand @ (mbox_s4 @ (leq @ A @ C)) @ (mand @ (mbox_s4 @ (leq @ n0 @ B)) @ (mbox_s4 @ (leq @ B @ D)))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ (tptp_update3 @ E @ C @ D @ F) @ A @ B) @ F)))))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',sel3_update_3)).
% 35.93/11.88 thf(279,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ! [K:mu]: ((exists_in_world @ K @ J) => (! [L:$i]: (~ (rel_s4 @ J @ L) | ! [M:mu]: ((exists_in_world @ M @ L) => (! [N:$i]: (~ (rel_s4 @ L @ N) | ~ (! [O:$i]: (~ (rel_s4 @ N @ O) | ! [P:mu]: ((exists_in_world @ P @ O) => (! [Q:$i]: (~ (rel_s4 @ O @ Q) | ! [R:mu]: ((exists_in_world @ R @ Q) => (! [S:$i]: (~ (rel_s4 @ Q @ S) | ~ (! [T:$i]: (~ (rel_s4 @ S @ T) | (leq @ n0 @ P @ T))) | ~ (! [T:$i]: (~ (rel_s4 @ S @ T) | (leq @ n0 @ R @ T))) | ~ (! [T:$i]: (~ (rel_s4 @ S @ T) | (leq @ P @ G @ T))) | ~ (! [T:$i]: (~ (rel_s4 @ S @ T) | (leq @ R @ I @ T))) | ! [T:$i]: (~ (rel_s4 @ S @ T) | (qmltpeq @ (a_select3 @ K @ P @ R) @ M @ T)))))))))) | ~ (! [O:$i]: (~ (rel_s4 @ N @ O) | (leq @ n0 @ C @ O))) | ~ (! [O:$i]: (~ (rel_s4 @ N @ O) | (leq @ C @ G @ O))) | ~ (! [O:$i]: (~ (rel_s4 @ N @ O) | (leq @ n0 @ E @ O))) | ~ (! [O:$i]: (~ (rel_s4 @ N @ O) | (leq @ E @ I @ O))) | ! [O:$i]: (~ (rel_s4 @ N @ O) | (qmltpeq @ (a_select3 @ (tptp_update3 @ K @ G @ I @ M) @ C @ E) @ M @ O))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 35.93/11.88 thf(111,axiom,((mvalid @ (mbox_s4 @ (gt @ n999 @ n3)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_999_3)).
% 35.93/11.88 thf(819,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n999 @ n3 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 35.93/11.88 thf(143,axiom,((mvalid @ (mbox_s4 @ (qmltpeq @ (succ @ (succ @ (succ @ (succ @ (succ @ n0))))) @ n5)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_5)).
% 35.93/11.88 thf(975,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (qmltpeq @ (succ @ (succ @ (succ @ (succ @ (succ @ n0))))) @ n5 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 35.93/11.88 thf(154,axiom,((mvalid @ (mbox_s4 @ (gt @ n4 @ tptp_minus_1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_tptp_minus_1)).
% 35.93/11.88 thf(1007,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n4 @ tptp_minus_1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 35.93/11.88 thf(104,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mforall_ind @ (^ [F:mu]: (mbox_s4 @ (mforall_ind @ (^ [G:mu]: (mbox_s4 @ (mforall_ind @ (^ [H:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (mforall_ind @ (^ [I:mu]: (mbox_s4 @ (mforall_ind @ (^ [J:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ I)) @ (mand @ (mbox_s4 @ (leq @ I @ H)) @ (mand @ (mbox_s4 @ (leq @ n0 @ J)) @ (mbox_s4 @ (leq @ J @ H))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ D @ I @ J) @ (a_select3 @ D @ J @ I))))))))))) @ (mand @ (mbox_s4 @ (mforall_ind @ (^ [I:mu]: (mbox_s4 @ (mforall_ind @ (^ [J:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ I)) @ (mand @ (mbox_s4 @ (leq @ I @ G)) @ (mand @ (mbox_s4 @ (leq @ n0 @ J)) @ (mbox_s4 @ (leq @ J @ G))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ A @ I @ J) @ (a_select3 @ A @ J @ I))))))))))) @ (mbox_s4 @ (mforall_ind @ (^ [I:mu]: (mbox_s4 @ (mforall_ind @ (^ [J:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ I)) @ (mand @ (mbox_s4 @ (leq @ I @ G)) @ (mand @ (mbox_s4 @ (leq @ n0 @ J)) @ (mbox_s4 @ (leq @ J @ G))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ F @ I @ J) @ (a_select3 @ F @ J @ I))))))))))))) @ (mbox_s4 @ (mforall_ind @ (^ [I:mu]: (mbox_s4 @ (mforall_ind @ (^ [J:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ I)) @ (mand @ (mbox_s4 @ (leq @ I @ G)) @ (mand @ (mbox_s4 @ (leq @ n0 @ J)) @ (mbox_s4 @ (leq @ J @ G))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ (tptp_madd @ A @ (tptp_mmul @ B @ (tptp_mmul @ (tptp_madd @ (tptp_mmul @ C @ (tptp_mmul @ D @ (trans @ C))) @ (tptp_mmul @ E @ (tptp_mmul @ F @ (trans @ E)))) @ (trans @ B)))) @ I @ J) @ (a_select3 @ (tptp_madd @ A @ (tptp_mmul @ B @ (tptp_mmul @ (tptp_madd @ (tptp_mmul @ C @ (tptp_mmul @ D @ (trans @ C))) @ (tptp_mmul @ E @ (tptp_mmul @ F @ (trans @ E)))) @ (trans @ B)))) @ J @ I))))))))))))))))))))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',matrix_symm_joseph_update)).
% 35.93/11.88 thf(711,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ! [K:mu]: ((exists_in_world @ K @ J) => (! [L:$i]: (~ (rel_s4 @ J @ L) | ! [M:mu]: ((exists_in_world @ M @ L) => (! [N:$i]: (~ (rel_s4 @ L @ N) | ! [O:mu]: ((exists_in_world @ O @ N) => (! [P:$i]: (~ (rel_s4 @ N @ P) | ! [Q:mu]: ((exists_in_world @ Q @ P) => (! [R:$i]: (~ (rel_s4 @ P @ R) | ~ (! [S:$i]: (~ (rel_s4 @ R @ S) | ! [T:mu]: ((exists_in_world @ T @ S) => (! [U:$i]: (~ (rel_s4 @ S @ U) | ! [V:mu]: ((exists_in_world @ V @ U) => (! [W:$i]: (~ (rel_s4 @ U @ W) | ~ (! [X:$i]: (~ (rel_s4 @ W @ X) | (leq @ n0 @ T @ X))) | ~ (! [X:$i]: (~ (rel_s4 @ W @ X) | (leq @ T @ Q @ X))) | ~ (! [X:$i]: (~ (rel_s4 @ W @ X) | (leq @ n0 @ V @ X))) | ~ (! [X:$i]: (~ (rel_s4 @ W @ X) | (leq @ V @ Q @ X))) | ! [X:$i]: (~ (rel_s4 @ W @ X) | (qmltpeq @ (a_select3 @ I @ T @ V) @ (a_select3 @ I @ V @ T) @ X)))))))))) | ~ (! [S:$i]: (~ (rel_s4 @ R @ S) | ! [T:mu]: ((exists_in_world @ T @ S) => (! [U:$i]: (~ (rel_s4 @ S @ U) | ! [V:mu]: ((exists_in_world @ V @ U) => (! [W:$i]: (~ (rel_s4 @ U @ W) | ~ (! [X:$i]: (~ (rel_s4 @ W @ X) | (leq @ n0 @ T @ X))) | ~ (! [X:$i]: (~ (rel_s4 @ W @ X) | (leq @ T @ O @ X))) | ~ (! [X:$i]: (~ (rel_s4 @ W @ X) | (leq @ n0 @ V @ X))) | ~ (! [X:$i]: (~ (rel_s4 @ W @ X) | (leq @ V @ O @ X))) | ! [X:$i]: (~ (rel_s4 @ W @ X) | (qmltpeq @ (a_select3 @ C @ T @ V) @ (a_select3 @ C @ V @ T) @ X)))))))))) | ~ (! [S:$i]: (~ (rel_s4 @ R @ S) | ! [T:mu]: ((exists_in_world @ T @ S) => (! [U:$i]: (~ (rel_s4 @ S @ U) | ! [V:mu]: ((exists_in_world @ V @ U) => (! [W:$i]: (~ (rel_s4 @ U @ W) | ~ (! [X:$i]: (~ (rel_s4 @ W @ X) | (leq @ n0 @ T @ X))) | ~ (! [X:$i]: (~ (rel_s4 @ W @ X) | (leq @ T @ O @ X))) | ~ (! [X:$i]: (~ (rel_s4 @ W @ X) | (leq @ n0 @ V @ X))) | ~ (! [X:$i]: (~ (rel_s4 @ W @ X) | (leq @ V @ O @ X))) | ! [X:$i]: (~ (rel_s4 @ W @ X) | (qmltpeq @ (a_select3 @ M @ T @ V) @ (a_select3 @ M @ V @ T) @ X)))))))))) | ! [S:$i]: (~ (rel_s4 @ R @ S) | ! [T:mu]: ((exists_in_world @ T @ S) => (! [U:$i]: (~ (rel_s4 @ S @ U) | ! [V:mu]: ((exists_in_world @ V @ U) => (! [W:$i]: (~ (rel_s4 @ U @ W) | ~ (! [X:$i]: (~ (rel_s4 @ W @ X) | (leq @ n0 @ T @ X))) | ~ (! [X:$i]: (~ (rel_s4 @ W @ X) | (leq @ T @ O @ X))) | ~ (! [X:$i]: (~ (rel_s4 @ W @ X) | (leq @ n0 @ V @ X))) | ~ (! [X:$i]: (~ (rel_s4 @ W @ X) | (leq @ V @ O @ X))) | ! [X:$i]: (~ (rel_s4 @ W @ X) | (qmltpeq @ (a_select3 @ (tptp_madd @ C @ (tptp_mmul @ E @ (tptp_mmul @ (tptp_madd @ (tptp_mmul @ G @ (tptp_mmul @ I @ (trans @ G))) @ (tptp_mmul @ K @ (tptp_mmul @ M @ (trans @ K)))) @ (trans @ E)))) @ T @ V) @ (a_select3 @ (tptp_madd @ C @ (tptp_mmul @ E @ (tptp_mmul @ (tptp_madd @ (tptp_mmul @ G @ (tptp_mmul @ I @ (trans @ G))) @ (tptp_mmul @ K @ (tptp_mmul @ M @ (trans @ K)))) @ (trans @ E)))) @ V @ T) @ X)))))))))))))))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 35.93/11.88 thf(75,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (pred @ A) @ (pred @ B))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',pred_substitution_1)).
% 35.93/11.88 thf(545,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (qmltpeq @ C @ E @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (qmltpeq @ (pred @ C) @ (pred @ E) @ G))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 35.93/11.88 thf(25,axiom,((! [A:$i,B:mu,C:mu,D:mu]: (exists_in_world @ (a_select3 @ B @ C @ D) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_a_select3_ax)).
% 35.93/11.88 thf(259,plain,((! [A:$i,B:mu,C:mu,D:mu]: (exists_in_world @ (a_select3 @ B @ C @ D) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 35.93/11.88 thf(119,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_update3 @ C @ A @ D @ E) @ (tptp_update3 @ C @ B @ D @ E)))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_update3_substitution_2)).
% 35.93/11.88 thf(843,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ! [K:mu]: ((exists_in_world @ K @ J) => (! [L:$i]: (~ (rel_s4 @ J @ L) | ~ (! [M:$i]: (~ (rel_s4 @ L @ M) | (qmltpeq @ C @ E @ M))) | ! [M:$i]: (~ (rel_s4 @ L @ M) | (qmltpeq @ (tptp_update3 @ G @ C @ I @ K) @ (tptp_update3 @ G @ E @ I @ K) @ M)))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 35.93/11.88 thf(184,axiom,((mvalid @ (mbox_s4 @ (gt @ n6 @ n4)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_4)).
% 35.93/11.88 thf(1125,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n6 @ n4 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 35.93/11.88 thf(50,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_msub @ A @ C) @ (tptp_msub @ B @ C)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_msub_substitution_1)).
% 35.93/11.88 thf(445,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (tptp_msub @ C @ G) @ (tptp_msub @ E @ G) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 35.93/11.88 thf(177,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (qmltpeq @ (plus @ n4 @ A) @ (succ @ (succ @ (succ @ (succ @ A))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_4_l)).
% 35.93/11.88 thf(1107,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (qmltpeq @ (plus @ n4 @ C) @ (succ @ (succ @ (succ @ (succ @ C)))) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 35.93/11.88 thf(135,axiom,((mvalid @ (mbox_s4 @ (gt @ n1 @ tptp_minus_1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_1_tptp_minus_1)).
% 35.93/11.88 thf(947,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n1 @ tptp_minus_1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 35.93/11.88 thf(97,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (leq @ (succ @ A) @ B)) @ (mbox_s4 @ (gt @ B @ A)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_succ_gt)).
% 35.93/11.88 thf(672,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ (succ @ C) @ E @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (gt @ E @ C @ G))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 35.93/11.88 thf(80,axiom,((mvalid @ (mbox_s4 @ (qmltpeq @ (succ @ (succ @ (succ @ (succ @ n0)))) @ n4)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_4)).
% 35.93/11.88 thf(604,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (qmltpeq @ (succ @ (succ @ (succ @ (succ @ n0)))) @ n4 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 35.93/11.88 thf(1,conjecture,((mvalid @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (geq @ (minus @ n3 @ n1) @ n0)) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (geq @ (minus @ n6 @ n1) @ n0)) @ (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (geq @ n2 @ n0)) @ (mbox_s4 @ (geq @ (minus @ n999 @ n1) @ n0))) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (geq @ (minus @ n6 @ n1) @ n0)) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (geq @ (minus @ n6 @ n1) @ n0)) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (geq @ (minus @ n6 @ n1) @ n0)) @ (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (geq @ (minus @ n3 @ n1) @ n0)) @ (mbox_s4 @ (geq @ (minus @ n999 @ n1) @ n0))) @ (mbox_s4 @ true))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',quaternion_ds1_inuse_0019)).
% 35.93/11.88 thf(2,negated_conjecture,((~ (mvalid @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (geq @ (minus @ n3 @ n1) @ n0)) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (geq @ (minus @ n6 @ n1) @ n0)) @ (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (geq @ n2 @ n0)) @ (mbox_s4 @ (geq @ (minus @ n999 @ n1) @ n0))) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (geq @ (minus @ n6 @ n1) @ n0)) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (geq @ (minus @ n6 @ n1) @ n0)) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (geq @ (minus @ n6 @ n1) @ n0)) @ (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (geq @ (minus @ n3 @ n1) @ n0)) @ (mbox_s4 @ (geq @ (minus @ n999 @ n1) @ n0))) @ (mbox_s4 @ true)))))))))))))))))),inference(neg_conjecture,[status(cth)],[1])).
% 35.93/11.88 thf(187,plain,((~ (! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ~ (! [C:$i]: (~ (rel_s4 @ B @ C) | (geq @ (minus @ n3 @ n1) @ n0 @ C))) | ! [C:$i]: (~ (rel_s4 @ B @ C) | ~ (! [D:$i]: (~ (rel_s4 @ C @ D) | (geq @ (minus @ n6 @ n1) @ n0 @ D))) | ! [D:$i]: (~ (rel_s4 @ C @ D) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (geq @ n2 @ n0 @ E))) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (geq @ (minus @ n999 @ n1) @ n0 @ E))) | ! [E:$i]: (~ (rel_s4 @ D @ E) | ~ (! [F:$i]: (~ (rel_s4 @ E @ F) | (geq @ (minus @ n6 @ n1) @ n0 @ F))) | ! [F:$i]: (~ (rel_s4 @ E @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (geq @ (minus @ n6 @ n1) @ n0 @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | ~ (! [H:$i]: (~ (rel_s4 @ G @ H) | (geq @ (minus @ n6 @ n1) @ n0 @ H))) | ! [H:$i]: (~ (rel_s4 @ G @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (geq @ (minus @ n3 @ n1) @ n0 @ I))) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (geq @ (minus @ n999 @ n1) @ n0 @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (true @ I)))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 35.93/11.88 thf(114,axiom,((mvalid @ (mbox_s4 @ (gt @ n0 @ tptp_minus_1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_0_tptp_minus_1)).
% 35.93/11.88 thf(831,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n0 @ tptp_minus_1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 35.93/11.88 thf(5,axiom,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (plus @ B @ C) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_plus_ax)).
% 35.93/11.88 thf(219,plain,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (plus @ B @ C) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 35.93/11.88 thf(181,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_mmul @ A @ C) @ (tptp_mmul @ B @ C)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_mmul_substitution_1)).
% 35.93/11.88 thf(1117,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (tptp_mmul @ C @ G) @ (tptp_mmul @ E @ G) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 35.93/11.88 thf(156,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ C)) @ (mand @ (mbox_s4 @ (leq @ C @ B)) @ (mand @ (mbox_s4 @ (leq @ n0 @ D)) @ (mbox_s4 @ (leq @ D @ B))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ A @ C @ D) @ (a_select3 @ A @ D @ C))))))))))) @ (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ C)) @ (mand @ (mbox_s4 @ (leq @ C @ B)) @ (mand @ (mbox_s4 @ (leq @ n0 @ D)) @ (mbox_s4 @ (leq @ D @ B))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ (inv @ A) @ C @ D) @ (a_select3 @ (inv @ A) @ D @ C))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',matrix_symm_inv)).
% 35.93/11.88 thf(1011,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | ! [H:mu]: ((exists_in_world @ H @ G) => (! [I:$i]: (~ (rel_s4 @ G @ I) | ! [J:mu]: ((exists_in_world @ J @ I) => (! [K:$i]: (~ (rel_s4 @ I @ K) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ n0 @ H @ L))) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ H @ E @ L))) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ n0 @ J @ L))) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ J @ E @ L))) | ! [L:$i]: (~ (rel_s4 @ K @ L) | (qmltpeq @ (a_select3 @ C @ H @ J) @ (a_select3 @ C @ J @ H) @ L)))))))))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | ! [H:mu]: ((exists_in_world @ H @ G) => (! [I:$i]: (~ (rel_s4 @ G @ I) | ! [J:mu]: ((exists_in_world @ J @ I) => (! [K:$i]: (~ (rel_s4 @ I @ K) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ n0 @ H @ L))) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ H @ E @ L))) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ n0 @ J @ L))) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ J @ E @ L))) | ! [L:$i]: (~ (rel_s4 @ K @ L) | (qmltpeq @ (a_select3 @ (inv @ C) @ H @ J) @ (a_select3 @ (inv @ C) @ J @ H) @ L)))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 35.93/11.88 thf(35,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (dim @ C @ A) @ (dim @ C @ B)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',dim_substitution_2)).
% 35.93/11.88 thf(377,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (dim @ G @ C) @ (dim @ G @ E) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 35.93/11.88 thf(18,axiom,((! [A:$i]: ? [B:mu]: (exists_in_world @ B @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',nonempty_ax)).
% 35.93/11.88 thf(245,plain,((! [A:$i]: ? [B:mu]: (exists_in_world @ B @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 35.93/11.88 thf(82,axiom,((mvalid @ (mbox_s4 @ (gt @ n6 @ n5)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_5)).
% 35.93/11.88 thf(616,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n6 @ n5 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 35.93/11.88 thf(28,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ A)) @ (mbox_s4 @ (leq @ A @ n0))) @ (mbox_s4 @ (qmltpeq @ A @ n0))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_0)).
% 35.93/11.88 thf(271,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (leq @ n0 @ C @ E))) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (leq @ C @ n0 @ E))) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n0 @ E)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 35.93/11.88 thf(61,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (qmltpeq @ (plus @ A @ n3) @ (succ @ (succ @ (succ @ A)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_3_r)).
% 35.93/11.88 thf(483,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (qmltpeq @ (plus @ C @ n3) @ (succ @ (succ @ (succ @ C))) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 35.93/11.88 thf(21,axiom,((! [A:$i,B:mu,C:mu,D:mu,E:mu]: (exists_in_world @ (tptp_update3 @ B @ C @ D @ E) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_tptp_update3_ax)).
% 35.93/11.88 thf(251,plain,((! [A:$i,B:mu,C:mu,D:mu,E:mu]: (exists_in_world @ (tptp_update3 @ B @ C @ D @ E) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 35.93/11.88 thf(125,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (sum @ A @ C @ D) @ (sum @ B @ C @ D))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_substitution_1)).
% 35.93/11.88 thf(895,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ C @ E @ K))) | ! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ (sum @ C @ G @ I) @ (sum @ E @ G @ I) @ K))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 35.93/11.88 thf(133,axiom,((mvalid @ (mbox_s4 @ (gt @ n5 @ n0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_0)).
% 35.93/11.88 thf(943,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n5 @ n0 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 35.93/11.88 thf(95,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (qmltpeq @ (plus @ n1 @ A) @ (succ @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_1_l)).
% 35.93/11.88 thf(668,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (qmltpeq @ (plus @ n1 @ C) @ (succ @ C) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 35.93/11.88 thf(108,axiom,((mtransitive @ rel_s4)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2)).
% 35.93/11.88 thf(811,plain,((! [A:$i,B:$i,C:$i]: (((rel_s4 @ A @ B) & (rel_s4 @ B @ C)) => (rel_s4 @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 35.93/11.88 thf(38,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (geq @ C @ A))) @ (mbox_s4 @ (geq @ C @ B))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',geq_substitution_2)).
% 35.93/11.88 thf(387,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (geq @ G @ C @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (geq @ G @ E @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 35.93/11.88 thf(146,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ A)) @ (mbox_s4 @ (leq @ A @ n1))) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n0)) @ (mbox_s4 @ (qmltpeq @ A @ n1)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_1)).
% 35.93/11.88 thf(983,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (leq @ n0 @ C @ E))) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (leq @ C @ n1 @ E))) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n0 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n1 @ E)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 35.93/11.88 thf(86,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ C @ D @ A) @ (a_select3 @ C @ D @ B))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_select3_substitution_3)).
% 35.93/11.88 thf(636,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ C @ E @ K))) | ! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ (a_select3 @ G @ I @ C) @ (a_select3 @ G @ I @ E) @ K))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 35.93/11.88 thf(7,axiom,((! [A:$i]: (exists_in_world @ n5 @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_n5_ax)).
% 35.93/11.88 thf(223,plain,((! [A:$i]: (exists_in_world @ n5 @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 35.93/11.88 thf(179,axiom,((mvalid @ (mbox_s4 @ (gt @ n999 @ n6)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_999_6)).
% 35.93/11.88 thf(1113,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n999 @ n6 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 35.93/11.88 thf(69,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ A @ B)) @ (mbox_s4 @ (leq @ B @ C))) @ (mbox_s4 @ (leq @ A @ C))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_leq)).
% 35.93/11.88 thf(505,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (leq @ C @ E @ I))) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (leq @ E @ G @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (leq @ C @ G @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 35.93/11.88 thf(48,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ A)) @ (mbox_s4 @ (leq @ A @ n4))) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n0)) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n1)) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n2)) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n3)) @ (mbox_s4 @ (qmltpeq @ A @ n4))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_4)).
% 35.93/11.88 thf(431,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (leq @ n0 @ C @ E))) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (leq @ C @ n4 @ E))) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n0 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n1 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n2 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n3 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n4 @ E)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 35.93/11.88 thf(16,axiom,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (tptp_madd @ B @ C) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_tptp_madd_ax)).
% 35.93/11.88 thf(241,plain,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (tptp_madd @ B @ C) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 35.93/11.88 thf(58,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (qmltpeq @ (plus @ n5 @ A) @ (succ @ (succ @ (succ @ (succ @ (succ @ A)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_5_l)).
% 35.93/11.88 thf(473,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (qmltpeq @ (plus @ n5 @ C) @ (succ @ (succ @ (succ @ (succ @ (succ @ C))))) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 35.93/11.88 thf(23,axiom,((! [A:$i,B:mu]: (exists_in_world @ (inv @ B) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_inv_ax)).
% 35.93/11.89 thf(255,plain,((! [A:$i,B:mu]: (exists_in_world @ (inv @ B) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 35.93/11.89 thf(63,axiom,((mvalid @ (mbox_s4 @ (qmltpeq @ (succ @ (succ @ (succ @ n0))) @ n3)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_3)).
% 35.93/11.89 thf(487,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (qmltpeq @ (succ @ (succ @ (succ @ n0))) @ n3 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 35.93/11.89 thf(131,axiom,((mvalid @ (mbox_s4 @ (gt @ n3 @ n0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_0)).
% 35.93/11.89 thf(939,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n3 @ n0 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 35.93/11.89 thf(164,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (a_select2 @ A @ C) @ (a_select2 @ B @ C)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_select2_substitution_1)).
% 35.93/11.89 thf(1049,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (a_select2 @ C @ G) @ (a_select2 @ E @ G) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 35.93/11.89 thf(153,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (dim @ A @ C) @ (dim @ B @ C)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',dim_substitution_1)).
% 35.93/11.89 thf(1003,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (dim @ C @ G) @ (dim @ E @ G) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 35.93/11.89 thf(101,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mforall_ind @ (^ [F:mu]: (mbox_s4 @ (mforall_ind @ (^ [G:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (mnot @ (mbox_s4 @ (qmltpeq @ A @ C)))) @ (mand @ (mbox_s4 @ (qmltpeq @ B @ D)) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ E @ C @ D) @ F)))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ (tptp_update3 @ E @ A @ B @ G) @ C @ D) @ F))))))))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',sel3_update_2)).
% 35.93/11.89 thf(690,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ! [K:mu]: ((exists_in_world @ K @ J) => (! [L:$i]: (~ (rel_s4 @ J @ L) | ! [M:mu]: ((exists_in_world @ M @ L) => (! [N:$i]: (~ (rel_s4 @ L @ N) | ! [O:mu]: ((exists_in_world @ O @ N) => (! [P:$i]: (~ (rel_s4 @ N @ P) | ~ (! [Q:$i]: (~ (rel_s4 @ P @ Q) | ~ (! [R:$i]: (~ (rel_s4 @ Q @ R) | (qmltpeq @ C @ G @ R))))) | ~ (! [Q:$i]: (~ (rel_s4 @ P @ Q) | (qmltpeq @ E @ I @ Q))) | ~ (! [Q:$i]: (~ (rel_s4 @ P @ Q) | (qmltpeq @ (a_select3 @ K @ G @ I) @ M @ Q))) | ! [Q:$i]: (~ (rel_s4 @ P @ Q) | (qmltpeq @ (a_select3 @ (tptp_update3 @ K @ C @ E @ O) @ G @ I) @ M @ Q)))))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 35.93/11.89 thf(87,axiom,((mvalid @ (mbox_s4 @ (gt @ n6 @ n3)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_3)).
% 35.93/11.89 thf(640,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n6 @ n3 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 35.93/11.89 thf(103,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ A @ C @ D) @ (a_select3 @ B @ C @ D))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_select3_substitution_1)).
% 35.93/11.89 thf(707,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ C @ E @ K))) | ! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ (a_select3 @ C @ G @ I) @ (a_select3 @ E @ G @ I) @ K))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 35.93/11.89 thf(123,axiom,((mvalid @ (mbox_s4 @ (gt @ n2 @ n1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_2_1)).
% 35.93/11.89 thf(887,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n2 @ n1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 35.93/11.89 thf(141,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (qmltpeq @ (pred @ (succ @ A)) @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',pred_succ)).
% 35.93/11.89 thf(971,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (qmltpeq @ (pred @ (succ @ C)) @ C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 35.93/11.89 thf(42,axiom,((mvalid @ (mbox_s4 @ (gt @ n6 @ tptp_minus_1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_tptp_minus_1)).
% 35.93/11.89 thf(409,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n6 @ tptp_minus_1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 35.93/11.89 thf(27,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mand @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (leq @ (succ @ A) @ (succ @ B))) @ (mbox_s4 @ (leq @ A @ B)))) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (leq @ A @ B)) @ (mbox_s4 @ (leq @ (succ @ A) @ (succ @ B)))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_succ_succ)).
% 35.93/11.89 thf(263,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (~ (~ (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ (succ @ C) @ (succ @ E) @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ C @ E @ G)))) | ~ (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ C @ E @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ (succ @ C) @ (succ @ E) @ G))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 35.93/11.89 thf(148,axiom,((mvalid @ (mbox_s4 @ (gt @ n6 @ n0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_0)).
% 35.93/11.89 thf(993,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n6 @ n0 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 35.93/11.89 thf(165,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (gt @ C @ A))) @ (mbox_s4 @ (gt @ C @ B))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_substitution_2)).
% 35.93/11.89 thf(1053,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (gt @ G @ C @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (gt @ G @ E @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 35.93/11.89 thf(55,axiom,((mvalid @ (mbox_s4 @ (gt @ n4 @ n3)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_3)).
% 35.93/11.89 thf(463,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n4 @ n3 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 35.93/11.89 thf(102,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_const_array2 @ C @ A @ D) @ (tptp_const_array2 @ C @ B @ D))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_const_array2_substitution_2)).
% 35.93/11.89 thf(703,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ C @ E @ K))) | ! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ (tptp_const_array2 @ G @ C @ I) @ (tptp_const_array2 @ G @ E @ I) @ K))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 35.93/11.89 thf(91,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (plus @ A @ C) @ (plus @ B @ C)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus_substitution_1)).
% 35.93/11.89 thf(656,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (plus @ C @ G) @ (plus @ E @ G) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 35.93/11.89 thf(78,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (qmltpeq @ (plus @ n2 @ A) @ (succ @ (succ @ A))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_plus_2_l)).
% 35.93/11.89 thf(600,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (qmltpeq @ (plus @ n2 @ C) @ (succ @ (succ @ C)) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 35.93/11.89 thf(127,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (qmltpeq @ (a_select3 @ (tptp_update3 @ A @ B @ C @ D) @ B @ C) @ D)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',sel3_update_1)).
% 35.93/11.89 thf(931,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | (qmltpeq @ (a_select3 @ (tptp_update3 @ C @ E @ G @ I) @ E @ G) @ I @ J)))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 35.93/11.89 thf(66,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (leq @ C @ A))) @ (mbox_s4 @ (leq @ C @ B))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_substitution_2)).
% 35.93/11.89 thf(495,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (leq @ G @ C @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (leq @ G @ E @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 35.93/11.89 thf(56,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (sum @ C @ D @ A) @ (sum @ C @ D @ B))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_substitution_3)).
% 35.93/11.89 thf(465,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ C @ E @ K))) | ! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ (sum @ G @ I @ C) @ (sum @ G @ I @ E) @ K))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 35.93/11.89 thf(11,axiom,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (tptp_mmul @ B @ C) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_tptp_mmul_ax)).
% 35.93/11.89 thf(231,plain,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (tptp_mmul @ B @ C) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 35.93/11.89 thf(139,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ B @ A)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry)).
% 35.93/11.89 thf(963,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (qmltpeq @ C @ E @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (qmltpeq @ E @ C @ G))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 35.93/11.89 thf(31,axiom,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (minus @ B @ C) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_minus_ax)).
% 35.93/11.89 thf(319,plain,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (minus @ B @ C) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 35.93/11.89 thf(176,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ B @ A)) @ (mbox_s4 @ (leq @ A @ C))) @ (mbox_s4 @ (qmltpeq @ (a_select2 @ (tptp_const_array1 @ (dim @ B @ C) @ D) @ A) @ D)))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',const_array1_select)).
% 35.93/11.89 thf(1101,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | (leq @ E @ C @ K))) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | (leq @ C @ G @ K))) | ! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ (a_select2 @ (tptp_const_array1 @ (dim @ E @ G) @ I) @ C) @ I @ K))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 35.93/11.89 thf(90,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (succ @ A) @ (succ @ B))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_substitution_1)).
% 35.93/11.89 thf(652,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (qmltpeq @ C @ E @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (qmltpeq @ (succ @ C) @ (succ @ E) @ G))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 35.93/11.89 thf(41,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mand @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (geq @ A @ B)) @ (mbox_s4 @ (leq @ B @ A)))) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (leq @ B @ A)) @ (mbox_s4 @ (geq @ A @ B))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_geq)).
% 35.93/11.89 thf(401,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (~ (~ (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (geq @ C @ E @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ E @ C @ G)))) | ~ (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ E @ C @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (geq @ C @ E @ G))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 35.93/11.89 thf(149,axiom,((mvalid @ (mbox_s4 @ (gt @ n5 @ n1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_1)).
% 35.93/11.89 thf(995,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n5 @ n1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 35.93/11.89 thf(138,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (leq @ A @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_leq)).
% 35.93/11.89 thf(961,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (leq @ C @ C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 35.93/11.89 thf(109,axiom,((! [A:$i]: (exists_in_world @ n6 @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_n6_ax)).
% 35.93/11.89 thf(813,plain,((! [A:$i]: (exists_in_world @ n6 @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 35.93/11.89 thf(13,axiom,((! [A:$i]: (exists_in_world @ n4 @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_n4_ax)).
% 35.93/11.89 thf(235,plain,((! [A:$i]: (exists_in_world @ n4 @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 35.93/11.89 thf(170,axiom,((mvalid @ (mbox_s4 @ (gt @ n3 @ n1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_1)).
% 35.93/11.89 thf(1077,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n3 @ n1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 35.93/11.89 thf(37,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_madd @ A @ C) @ (tptp_madd @ B @ C)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_madd_substitution_1)).
% 35.93/11.89 thf(383,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (tptp_madd @ C @ G) @ (tptp_madd @ E @ G) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 35.93/11.89 thf(126,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mforall_ind @ (^ [F:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ E)) @ (mand @ (mbox_s4 @ (leq @ E @ D)) @ (mand @ (mbox_s4 @ (leq @ n0 @ F)) @ (mbox_s4 @ (leq @ F @ D))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ B @ E @ F) @ (a_select3 @ B @ F @ E))))))))))) @ (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mforall_ind @ (^ [F:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ E)) @ (mand @ (mbox_s4 @ (leq @ E @ C)) @ (mand @ (mbox_s4 @ (leq @ n0 @ F)) @ (mbox_s4 @ (leq @ F @ C))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ (tptp_mmul @ A @ (tptp_mmul @ B @ (trans @ A))) @ E @ F) @ (a_select3 @ (tptp_mmul @ A @ (tptp_mmul @ B @ (trans @ A))) @ F @ E))))))))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',matrix_symm_aba2)).
% 35.93/11.89 thf(899,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | ! [L:mu]: ((exists_in_world @ L @ K) => (! [M:$i]: (~ (rel_s4 @ K @ M) | ! [N:mu]: ((exists_in_world @ N @ M) => (! [O:$i]: (~ (rel_s4 @ M @ O) | ~ (! [P:$i]: (~ (rel_s4 @ O @ P) | (leq @ n0 @ L @ P))) | ~ (! [P:$i]: (~ (rel_s4 @ O @ P) | (leq @ L @ I @ P))) | ~ (! [P:$i]: (~ (rel_s4 @ O @ P) | (leq @ n0 @ N @ P))) | ~ (! [P:$i]: (~ (rel_s4 @ O @ P) | (leq @ N @ I @ P))) | ! [P:$i]: (~ (rel_s4 @ O @ P) | (qmltpeq @ (a_select3 @ E @ L @ N) @ (a_select3 @ E @ N @ L) @ P)))))))))) | ! [K:$i]: (~ (rel_s4 @ J @ K) | ! [L:mu]: ((exists_in_world @ L @ K) => (! [M:$i]: (~ (rel_s4 @ K @ M) | ! [N:mu]: ((exists_in_world @ N @ M) => (! [O:$i]: (~ (rel_s4 @ M @ O) | ~ (! [P:$i]: (~ (rel_s4 @ O @ P) | (leq @ n0 @ L @ P))) | ~ (! [P:$i]: (~ (rel_s4 @ O @ P) | (leq @ L @ G @ P))) | ~ (! [P:$i]: (~ (rel_s4 @ O @ P) | (leq @ n0 @ N @ P))) | ~ (! [P:$i]: (~ (rel_s4 @ O @ P) | (leq @ N @ G @ P))) | ! [P:$i]: (~ (rel_s4 @ O @ P) | (qmltpeq @ (a_select3 @ (tptp_mmul @ C @ (tptp_mmul @ E @ (trans @ C))) @ L @ N) @ (a_select3 @ (tptp_mmul @ C @ (tptp_mmul @ E @ (trans @ C))) @ N @ L) @ P)))))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 35.93/11.89 thf(76,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ D)) @ (mand @ (mbox_s4 @ (leq @ D @ C)) @ (mand @ (mbox_s4 @ (leq @ n0 @ E)) @ (mbox_s4 @ (leq @ E @ C))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ A @ D @ E) @ (a_select3 @ A @ E @ D))))))))))) @ (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ D)) @ (mand @ (mbox_s4 @ (leq @ D @ C)) @ (mand @ (mbox_s4 @ (leq @ n0 @ E)) @ (mbox_s4 @ (leq @ E @ C))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ B @ D @ E) @ (a_select3 @ B @ E @ D)))))))))))) @ (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ D)) @ (mand @ (mbox_s4 @ (leq @ D @ C)) @ (mand @ (mbox_s4 @ (leq @ n0 @ E)) @ (mbox_s4 @ (leq @ E @ C))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ (tptp_madd @ A @ B) @ D @ E) @ (a_select3 @ (tptp_madd @ A @ B) @ E @ D)))))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',matrix_symm_add)).
% 35.93/11.89 thf(549,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | ! [J:mu]: ((exists_in_world @ J @ I) => (! [K:$i]: (~ (rel_s4 @ I @ K) | ! [L:mu]: ((exists_in_world @ L @ K) => (! [M:$i]: (~ (rel_s4 @ K @ M) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ J @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ J @ G @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ L @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ L @ G @ N))) | ! [N:$i]: (~ (rel_s4 @ M @ N) | (qmltpeq @ (a_select3 @ C @ J @ L) @ (a_select3 @ C @ L @ J) @ N)))))))))) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | ! [J:mu]: ((exists_in_world @ J @ I) => (! [K:$i]: (~ (rel_s4 @ I @ K) | ! [L:mu]: ((exists_in_world @ L @ K) => (! [M:$i]: (~ (rel_s4 @ K @ M) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ J @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ J @ G @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ L @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ L @ G @ N))) | ! [N:$i]: (~ (rel_s4 @ M @ N) | (qmltpeq @ (a_select3 @ E @ J @ L) @ (a_select3 @ E @ L @ J) @ N)))))))))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | ! [J:mu]: ((exists_in_world @ J @ I) => (! [K:$i]: (~ (rel_s4 @ I @ K) | ! [L:mu]: ((exists_in_world @ L @ K) => (! [M:$i]: (~ (rel_s4 @ K @ M) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ J @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ J @ G @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ n0 @ L @ N))) | ~ (! [N:$i]: (~ (rel_s4 @ M @ N) | (leq @ L @ G @ N))) | ! [N:$i]: (~ (rel_s4 @ M @ N) | (qmltpeq @ (a_select3 @ (tptp_madd @ C @ E) @ J @ L) @ (a_select3 @ (tptp_madd @ C @ E) @ L @ J) @ N))))))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 35.93/11.89 thf(162,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (qmltpeq @ A @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity)).
% 35.93/11.89 thf(1045,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (qmltpeq @ C @ C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 35.93/11.89 thf(151,axiom,((! [A:$i]: (exists_in_world @ n1 @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_n1_ax)).
% 35.93/11.89 thf(999,plain,((! [A:$i]: (exists_in_world @ n1 @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 35.93/11.89 thf(115,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (uniform_int_rnd @ A @ C) @ (uniform_int_rnd @ B @ C)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',uniform_int_rnd_substitution_1)).
% 35.93/11.89 thf(833,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (uniform_int_rnd @ C @ G) @ (uniform_int_rnd @ E @ G) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 35.93/11.89 thf(140,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (leq @ A @ B)) @ (mbox_s4 @ (leq @ A @ (succ @ B))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_succ)).
% 35.93/11.89 thf(967,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ C @ E @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ C @ (succ @ E) @ G))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 35.93/11.89 thf(15,axiom,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (a_select2 @ B @ C) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_a_select2_ax)).
% 35.93/11.89 thf(239,plain,((! [A:$i,B:mu,C:mu]: (exists_in_world @ (a_select2 @ B @ C) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 35.93/11.89 thf(107,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (gt @ B @ A)) @ (mbox_s4 @ (leq @ A @ B)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_gt1)).
% 35.93/11.89 thf(807,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (gt @ E @ C @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ C @ E @ G))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 35.93/11.89 thf(49,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mand @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (leq @ A @ (pred @ B))) @ (mbox_s4 @ (gt @ B @ A)))) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (gt @ B @ A)) @ (mbox_s4 @ (leq @ A @ (pred @ B)))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',leq_gt_pred)).
% 35.93/11.89 thf(437,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (~ (~ (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ C @ (pred @ E) @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (gt @ E @ C @ G)))) | ~ (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | (gt @ E @ C @ G))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | (leq @ C @ (pred @ E) @ G))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 35.93/11.89 thf(94,axiom,((mvalid @ (mbox_s4 @ (mnot @ (mbox_s4 @ (qmltpeq @ def @ use)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',defuse)).
% 35.93/11.89 thf(664,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ~ (! [C:$i]: (~ (rel_s4 @ B @ C) | (qmltpeq @ def @ use @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 35.93/11.89 thf(167,axiom,((mvalid @ (mbox_s4 @ (gt @ n5 @ n2)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_2)).
% 35.93/11.89 thf(1065,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n5 @ n2 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 35.93/11.89 thf(44,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ A)) @ (mbox_s4 @ (leq @ A @ n5))) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n0)) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n1)) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n2)) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n3)) @ (mor @ (mbox_s4 @ (qmltpeq @ A @ n4)) @ (mbox_s4 @ (qmltpeq @ A @ n5)))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_5)).
% 35.93/11.89 thf(415,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (leq @ n0 @ C @ E))) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (leq @ C @ n5 @ E))) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n0 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n1 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n2 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n3 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n4 @ E)) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (qmltpeq @ C @ n5 @ E)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 35.93/11.89 thf(77,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (plus @ C @ A) @ (plus @ C @ B)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus_substitution_2)).
% 35.93/11.89 thf(596,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (plus @ G @ C) @ (plus @ G @ E) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 35.93/11.89 thf(29,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (qmltpeq @ tptp_float_0_0 @ (sum @ n0 @ tptp_minus_1 @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_plus_base_float)).
% 35.93/11.89 thf(277,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (qmltpeq @ tptp_float_0_0 @ (sum @ n0 @ tptp_minus_1 @ C) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 35.93/11.89 thf(67,axiom,((mvalid @ (mbox_s4 @ (qmltpeq @ (succ @ (succ @ (succ @ (succ @ (succ @ (succ @ n0)))))) @ n6)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_6)).
% 35.93/11.89 thf(501,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (qmltpeq @ (succ @ (succ @ (succ @ (succ @ (succ @ (succ @ n0)))))) @ n6 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 35.93/11.89 thf(40,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ B @ C))) @ (mbox_s4 @ (qmltpeq @ A @ C))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity)).
% 35.93/11.89 thf(395,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ E @ G @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ G @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 35.93/11.89 thf(84,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_const_array2 @ C @ D @ A) @ (tptp_const_array2 @ C @ D @ B))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_const_array2_substitution_3)).
% 35.93/11.89 thf(624,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ C @ E @ K))) | ! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ (tptp_const_array2 @ G @ I @ C) @ (tptp_const_array2 @ G @ I @ E) @ K))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 35.93/11.89 thf(117,axiom,((mvalid @ (mbox_s4 @ (qmltpeq @ (succ @ (succ @ n0)) @ n2)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_2)).
% 35.93/11.89 thf(839,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (qmltpeq @ (succ @ (succ @ n0)) @ n2 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 35.93/11.89 thf(9,axiom,((! [A:$i]: (exists_in_world @ tptp_float_0_0 @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_tptp_float_0_0_ax)).
% 35.93/11.89 thf(227,plain,((! [A:$i]: (exists_in_world @ tptp_float_0_0 @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 35.93/11.89 thf(57,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (sum @ C @ A @ D) @ (sum @ C @ B @ D))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_substitution_2)).
% 35.93/11.89 thf(469,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ! [I:mu]: ((exists_in_world @ I @ H) => (! [J:$i]: (~ (rel_s4 @ H @ J) | ~ (! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ C @ E @ K))) | ! [K:$i]: (~ (rel_s4 @ J @ K) | (qmltpeq @ (sum @ G @ C @ I) @ (sum @ G @ E @ I) @ K))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 35.93/11.89 thf(74,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (qmltpeq @ (minus @ A @ n1) @ (pred @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',pred_minus_1)).
% 35.93/11.89 thf(543,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (qmltpeq @ (minus @ C @ n1) @ (pred @ C) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 35.93/11.89 thf(3,axiom,((! [A:$i]: (exists_in_world @ def @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_def_ax)).
% 35.93/11.89 thf(215,plain,((! [A:$i]: (exists_in_world @ def @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 35.93/11.89 thf(98,axiom,((mvalid @ (mbox_s4 @ (gt @ n999 @ n5)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_999_5)).
% 35.93/11.89 thf(676,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (gt @ n999 @ n5 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 35.93/11.89 thf(65,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (qmltpeq @ A @ B)) @ (mbox_s4 @ (qmltpeq @ (tptp_const_array1 @ C @ A) @ (tptp_const_array1 @ C @ B)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tptp_const_array1_substitution_2)).
% 35.93/11.89 thf(491,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (! [H:$i]: (~ (rel_s4 @ F @ H) | ~ (! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ C @ E @ I))) | ! [I:$i]: (~ (rel_s4 @ H @ I) | (qmltpeq @ (tptp_const_array1 @ G @ C) @ (tptp_const_array1 @ G @ E) @ I)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 35.93/11.89 thf(129,axiom,((mvalid @ (mbox_s4 @ (qmltpeq @ (succ @ tptp_minus_1) @ n0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',succ_tptp_minus_1)).
% 35.93/11.89 thf(935,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | (qmltpeq @ (succ @ tptp_minus_1) @ n0 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 35.93/11.89 thf(155,axiom,((! [A:$i]: (exists_in_world @ n3 @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_n3_ax)).
% 35.93/11.89 thf(1009,plain,((! [A:$i]: (exists_in_world @ n3 @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 35.93/11.89 thf(159,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (qmltpeq @ (sum @ n0 @ tptp_minus_1 @ A) @ n0))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',sum_plus_base)).
% 35.93/11.89 thf(1037,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (qmltpeq @ (sum @ n0 @ tptp_minus_1 @ C) @ n0 @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 35.93/11.89 thf(106,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mforall_ind @ (^ [B:mu]: (mbox_s4 @ (mimplies @ (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ C)) @ (mand @ (mbox_s4 @ (leq @ C @ B)) @ (mand @ (mbox_s4 @ (leq @ n0 @ D)) @ (mbox_s4 @ (leq @ D @ B))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ A @ C @ D) @ (a_select3 @ A @ D @ C))))))))))) @ (mbox_s4 @ (mforall_ind @ (^ [C:mu]: (mbox_s4 @ (mforall_ind @ (^ [D:mu]: (mbox_s4 @ (mimplies @ (mand @ (mbox_s4 @ (leq @ n0 @ C)) @ (mand @ (mbox_s4 @ (leq @ C @ B)) @ (mand @ (mbox_s4 @ (leq @ n0 @ D)) @ (mbox_s4 @ (leq @ D @ B))))) @ (mbox_s4 @ (qmltpeq @ (a_select3 @ (trans @ A) @ C @ D) @ (a_select3 @ (trans @ A) @ D @ C))))))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',matrix_symm_trans)).
% 35.93/11.89 thf(775,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | ~ (! [G:$i]: (~ (rel_s4 @ F @ G) | ! [H:mu]: ((exists_in_world @ H @ G) => (! [I:$i]: (~ (rel_s4 @ G @ I) | ! [J:mu]: ((exists_in_world @ J @ I) => (! [K:$i]: (~ (rel_s4 @ I @ K) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ n0 @ H @ L))) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ H @ E @ L))) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ n0 @ J @ L))) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ J @ E @ L))) | ! [L:$i]: (~ (rel_s4 @ K @ L) | (qmltpeq @ (a_select3 @ C @ H @ J) @ (a_select3 @ C @ J @ H) @ L)))))))))) | ! [G:$i]: (~ (rel_s4 @ F @ G) | ! [H:mu]: ((exists_in_world @ H @ G) => (! [I:$i]: (~ (rel_s4 @ G @ I) | ! [J:mu]: ((exists_in_world @ J @ I) => (! [K:$i]: (~ (rel_s4 @ I @ K) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ n0 @ H @ L))) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ H @ E @ L))) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ n0 @ J @ L))) | ~ (! [L:$i]: (~ (rel_s4 @ K @ L) | (leq @ J @ E @ L))) | ! [L:$i]: (~ (rel_s4 @ K @ L) | (qmltpeq @ (a_select3 @ (trans @ C) @ H @ J) @ (a_select3 @ (trans @ C) @ J @ H) @ L)))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 35.93/11.89 thf(1855,plain,(($false)),inference(e,[status(thm)],[479,1083,941,628,1031,249,977,217,1073,449,247,511,1041,945,670,1001,1127,841,973,257,1059,949,421,606,881,1115,261,475,485,937,821,1109,321,646,253,221,453,660,411,243,849,602,981,233,678,381,1067,1047,957,1091,825,1123,429,815,361,889,461,1079,682,229,847,1089,1121,989,225,933,537,642,489,1039,837,393,997,1099,1131,457,371,503,237,541,1035,773,662,618,425,513,279,819,975,1007,711,545,259,843,1125,445,1107,947,672,604,187,831,219,1117,1011,377,245,616,271,483,251,895,943,668,811,387,983,636,223,1113,505,431,241,473,255,487,939,1049,1003,690,640,707,887,971,409,263,993,1053,463,703,656,600,931,495,465,231,963,319,1101,652,401,995,961,813,235,1077,383,899,549,1045,999,833,967,239,807,437,664,1065,415,596,277,501,395,624,839,227,469,543,215,676,491,935,1009,1037,775])).
% 35.93/11.89 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.93/11.89 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------