%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : KRS272^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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:11:53 AM UTC 2026
% Result : Theorem 75.35s 15.52s
% Output : Refutation 63.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS272^7 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.10/0.21 % Computer : n018.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Tue Sep 29 08:40:25 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.06/0.86 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.32/1.30 % [INFO] Parsing done (432ms).
% 2.32/1.32 % [INFO] Running in sequential loop mode.
% 3.23/1.93 % [INFO] eprover registered as external prover.
% 3.23/1.94 % [INFO] Scanning for conjecture ...
% 3.90/2.21 % [INFO] Found a conjecture (or negated_conjecture) and 9 axioms. Running axiom selection ...
% 3.90/2.27 % [INFO] Axiom selection finished. Selected 9 axioms (removed 0 axioms).
% 3.90/2.29 % [INFO] Problem is higher-order (TPTP THF).
% 3.90/2.29 % [INFO] Type checking passed.
% 3.90/2.30 % [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 ...
% 75.35/15.51 % External prover 'e' found a proof!
% 75.35/15.51 % [INFO] Killing All external provers ...
% 75.35/15.51 % Time passed: 15161ms (effective reasoning time: 14181ms)
% 75.35/15.51 % 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)>
% 75.35/15.52 % Axioms used in derivation (9): existence_of_u_ax, ax1, cumulative_ax, existence_of_one_ax, ax2, a1, nonempty_ax, ax3, a2
% 75.35/15.52 % No. of inferences in proof: 106
% 75.35/15.52 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 15161 ms resp. 14181 ms w/o parsing
% 63.68/15.71 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 63.68/15.71 thf(mu_type, type, mu: $tType).
% 63.68/15.71 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 63.68/15.71 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 63.68/15.71 thf(mand_decl, type, mand: (($i > $o) > (($i > $o) > ($i > $o)))).
% 63.68/15.71 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 63.68/15.71 thf(exists_in_world_decl, type, exists_in_world: (mu > ($i > $o))).
% 63.68/15.71 thf(mforall_ind_decl, type, mforall_ind: ((mu > ($i > $o)) > ($i > $o))).
% 63.68/15.71 thf(mexists_ind_decl, type, mexists_ind: ((mu > ($i > $o)) > ($i > $o))).
% 63.68/15.71 thf(mreflexive_decl, type, mreflexive: (($i > ($i > $o)) > $o)).
% 63.68/15.71 thf(mtransitive_decl, type, mtransitive: (($i > ($i > $o)) > $o)).
% 63.68/15.71 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 63.68/15.71 thf(rel_s4_decl, type, rel_s4: ($i > ($i > $o))).
% 63.68/15.71 thf(mbox_s4_decl, type, mbox_s4: (($i > $o) > ($i > $o))).
% 63.68/15.71 thf(string_decl, type, string: (mu > ($i > $o))).
% 63.68/15.71 thf(in_decl, type, in: (mu > (mu > (mu > ($i > $o))))).
% 63.68/15.71 thf(do_decl, type, do: (mu > (mu > (mu > ($i > $o))))).
% 63.68/15.71 thf(number_decl, type, number: (mu > (mu > ($i > $o)))).
% 63.68/15.71 thf(entry_box_decl, type, entry_box: (mu > ($i > $o))).
% 63.68/15.71 thf(userid_decl, type, userid: (mu > (mu > ($i > $o)))).
% 63.68/15.71 thf(one_decl, type, one: mu).
% 63.68/15.71 thf(u_decl, type, u: mu).
% 63.68/15.71 thf(sk1_decl, type, sk1: $i).
% 63.68/15.71 thf(sk2_decl, type, sk2: $i).
% 63.68/15.71 thf(sk3_decl, type, sk3: (mu > (mu > (mu > (mu > $o))))).
% 63.68/15.71 thf(sk4_decl, type, sk4: (mu > (mu > (mu > (mu > $i))))).
% 63.68/15.71 thf(sk5_decl, type, sk5: (mu > (mu > (mu > (mu > $i))))).
% 63.68/15.71 thf(sk6_decl, type, sk6: (mu > (mu > (mu > (mu > mu))))).
% 63.68/15.71 thf(sk7_decl, type, sk7: ($i > mu)).
% 63.68/15.71 thf(sk8_decl, type, sk8: ($i > ($i > mu))).
% 63.68/15.71 thf(sk9_decl, type, sk9: ($i > mu)).
% 63.68/15.71 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 63.68/15.71 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 63.68/15.71 thf(mand_def, definition, mand = (^ [A:($i > $o),B:($i > $o)]: (mnot @ (mor @ (mnot @ A) @ (mnot @ B)))) ).
% 63.68/15.71 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 63.68/15.71 thf(mforall_ind_def, definition, mforall_ind = (^ [A:(mu > ($i > $o)),B:$i]: ! [C:mu]: ((exists_in_world @ C @ B) => (A @ C @ B))) ).
% 63.68/15.71 thf(mexists_ind_def, definition, mexists_ind = (^ [A:(mu > ($i > $o))]: (mnot @ (mforall_ind @ (^ [B:mu]: (mnot @ (A @ B)))))) ).
% 63.68/15.71 thf(mreflexive_def, definition, mreflexive = (^ [A:($i > ($i > $o))]: ! [B:$i]: (A @ B @ B)) ).
% 63.68/15.71 thf(mtransitive_def, definition, mtransitive = (^ [A:($i > ($i > $o))]: ! [B:$i,C:$i,D:$i]: (((A @ B @ C) & (A @ C @ D)) => (A @ B @ D))) ).
% 63.68/15.71 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 63.68/15.71 thf(mbox_s4_def, definition, mbox_s4 = (^ [A:($i > $o),B:$i]: ! [C:$i]: (~ (rel_s4 @ B @ C) | (A @ C))) ).
% 63.68/15.71 thf(sk1_def, definition, sk1 = (@+ [A:$i]: ~ (! [B:$i]: (~ (rel_s4 @ A @ B) | ~ (! [C:mu]: ((exists_in_world @ C @ B) => (! [D:mu]: ((exists_in_world @ D @ B) => (! [E:mu]: ((exists_in_world @ E @ B) => (! [F:mu]: ((exists_in_world @ F @ B) => (~ (! [G:$i]: (~ (rel_s4 @ B @ G) | ~ (~ (userid @ u @ C @ G) | ~ (entry_box @ D @ G) | ~ (number @ D @ one @ G)))) | ~ (! [G:$i]: (~ (rel_s4 @ B @ G) | ! [H:mu]: ((exists_in_world @ H @ G) => (~ (do @ F @ E @ H @ G) | (in @ C @ D @ H @ G))))))))))))))))) ).
% 63.68/15.71 thf(sk2_def, definition, sk2 = (@+ [A:$i]: ~ (~ (rel_s4 @ sk1 @ A) | ~ (! [B:mu]: ((exists_in_world @ B @ A) => (! [C:mu]: ((exists_in_world @ C @ A) => (! [D:mu]: ((exists_in_world @ D @ A) => (! [E:mu]: ((exists_in_world @ E @ A) => (~ (! [F:$i]: (~ (rel_s4 @ A @ F) | ~ (~ (userid @ u @ B @ F) | ~ (entry_box @ C @ F) | ~ (number @ C @ one @ F)))) | ~ (! [F:$i]: (~ (rel_s4 @ A @ F) | ! [G:mu]: ((exists_in_world @ G @ F) => (~ (do @ E @ D @ G @ F) | (in @ B @ C @ G @ F)))))))))))))))) ).
% 63.68/15.71 thf(sk4_def, definition, sk4 = (^ [A:mu,B:mu,C:mu,D:mu]: (@+ [E:$i]: ~ (~ (rel_s4 @ sk2 @ E) | ~ (~ (userid @ u @ D @ E) | ~ (entry_box @ C @ E) | ~ (number @ C @ one @ E))))) ).
% 63.68/15.71 thf(sk5_def, definition, sk5 = (^ [A:mu,B:mu,C:mu,D:mu]: (@+ [E:$i]: ~ (~ (rel_s4 @ sk2 @ E) | ! [F:mu]: ((exists_in_world @ F @ E) => (~ (do @ A @ B @ F @ E) | (in @ D @ C @ F @ E)))))) ).
% 63.68/15.71 thf(sk6_def, definition, sk6 = (^ [A:mu,B:mu,C:mu,D:mu]: (@+ [E:mu]: ~ ((exists_in_world @ E @ (sk5 @ A @ B @ C @ D)) => (~ (do @ A @ B @ E @ (sk5 @ A @ B @ C @ D)) | (in @ D @ C @ E @ (sk5 @ A @ B @ C @ D)))))) ).
% 63.68/15.71 thf(sk7_def, definition, sk7 = (^ [A:$i]: (@+ [B:mu]: (exists_in_world @ B @ A))) ).
% 63.68/15.71 thf(sk8_def, definition, sk8 = (^ [A:$i,B:$i]: (@+ [C:mu]: ~ ((exists_in_world @ C @ A) => (~ (! [D:$i]: (~ (rel_s4 @ A @ D) | ~ (~ (userid @ u @ C @ D) | ~ (string @ C @ D)))))))) ).
% 63.68/15.71 thf(sk9_def, definition, sk9 = (^ [A:$i]: (@+ [B:mu]: ~ ((exists_in_world @ B @ A) => (~ (! [C:$i]: (~ (rel_s4 @ A @ C) | ~ (~ (entry_box @ B @ C) | ~ (number @ B @ one @ C)))))))) ).
% 63.68/15.71 thf(1,conjecture,((mvalid @ (mbox_s4 @ (mexists_ind @ (^ [A:mu]: (mexists_ind @ (^ [B:mu]: (mexists_ind @ (^ [C:mu]: (mexists_ind @ (^ [D:mu]: (mand @ (mbox_s4 @ (mand @ (userid @ u @ A) @ (mand @ (entry_box @ B) @ (number @ B @ one)))) @ (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mimplies @ (do @ D @ C @ E) @ (in @ A @ B @ E))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 63.68/15.71 thf(2,negated_conjecture,((~ (mvalid @ (mbox_s4 @ (mexists_ind @ (^ [A:mu]: (mexists_ind @ (^ [B:mu]: (mexists_ind @ (^ [C:mu]: (mexists_ind @ (^ [D:mu]: (mand @ (mbox_s4 @ (mand @ (userid @ u @ A) @ (mand @ (entry_box @ B) @ (number @ B @ one)))) @ (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mimplies @ (do @ D @ C @ E) @ (in @ A @ B @ E)))))))))))))))))),inference(neg_conjecture,[status(cth)],[1])).
% 63.68/15.71 thf(12,plain,((~ (! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ~ (! [C:mu]: ((exists_in_world @ C @ B) => (! [D:mu]: ((exists_in_world @ D @ B) => (! [E:mu]: ((exists_in_world @ E @ B) => (! [F:mu]: ((exists_in_world @ F @ B) => (~ (! [G:$i]: (~ (rel_s4 @ B @ G) | ~ (~ (userid @ u @ C @ G) | ~ (entry_box @ D @ G) | ~ (number @ D @ one @ G)))) | ~ (! [G:$i]: (~ (rel_s4 @ B @ G) | ! [H:mu]: ((exists_in_world @ H @ G) => (~ (do @ F @ E @ H @ G) | (in @ C @ D @ H @ G)))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 63.68/15.71 thf(13,plain,(! [D:mu,C:mu,B:mu,A:mu] : (((rel_s4 @ sk1 @ sk2) & (~ (exists_in_world @ A @ sk2) | ~ (exists_in_world @ B @ sk2) | ~ (exists_in_world @ C @ sk2) | ~ (exists_in_world @ D @ sk2) | (rel_s4 @ sk2 @ (sk4 @ D @ C @ B @ A)) | (sk3 @ A @ C @ D @ B)) & (~ (exists_in_world @ A @ sk2) | ~ (exists_in_world @ B @ sk2) | ~ (exists_in_world @ C @ sk2) | ~ (exists_in_world @ D @ sk2) | ~ (userid @ u @ A @ (sk4 @ D @ C @ B @ A)) | ~ (entry_box @ B @ (sk4 @ D @ C @ B @ A)) | ~ (number @ B @ one @ (sk4 @ D @ C @ B @ A)) | (sk3 @ A @ C @ D @ B)) & (~ (exists_in_world @ A @ sk2) | ~ (exists_in_world @ B @ sk2) | ~ (exists_in_world @ C @ sk2) | ~ (exists_in_world @ D @ sk2) | ~ (sk3 @ A @ C @ D @ B) | (rel_s4 @ sk2 @ (sk5 @ D @ C @ B @ A))) & (~ (exists_in_world @ A @ sk2) | ~ (exists_in_world @ B @ sk2) | ~ (exists_in_world @ C @ sk2) | ~ (exists_in_world @ D @ sk2) | ~ (sk3 @ A @ C @ D @ B) | (exists_in_world @ (sk6 @ D @ C @ B @ A) @ (sk5 @ D @ C @ B @ A))) & (~ (exists_in_world @ A @ sk2) | ~ (exists_in_world @ B @ sk2) | ~ (exists_in_world @ C @ sk2) | ~ (exists_in_world @ D @ sk2) | ~ (sk3 @ A @ C @ D @ B) | (do @ D @ C @ (sk6 @ D @ C @ B @ A) @ (sk5 @ D @ C @ B @ A))) & (~ (exists_in_world @ A @ sk2) | ~ (exists_in_world @ B @ sk2) | ~ (exists_in_world @ C @ sk2) | ~ (exists_in_world @ D @ sk2) | ~ (sk3 @ A @ C @ D @ B) | ~ (in @ A @ B @ (sk6 @ D @ C @ B @ A) @ (sk5 @ D @ C @ B @ A)))))),inference(cnf,[status(esa)],[12])).
% 63.68/15.71 thf(18,plain,((rel_s4 @ sk1 @ sk2)),inference(cnfConj,[status(thm)],[13])).
% 63.68/15.71 thf(5,axiom,((mtransitive @ rel_s4)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2)).
% 63.68/15.71 thf(25,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)],[5])).
% 63.68/15.71 thf(26,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (rel_s4 @ A @ C))),inference(cnf,[status(esa)],[25])).
% 63.68/15.71 thf(664,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | ~ (($true)) | (rel_s4 @ A @ C) | ((rel_s4 @ sk1 @ sk2) != (rel_s4 @ B @ C)))),inference(paramod_ordered,[status(thm)],[18,26])).
% 63.68/15.71 thf(665,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (rel_s4 @ A @ C) | ((rel_s4 @ sk1 @ sk2) != (rel_s4 @ B @ C)))),inference(simp,[status(thm)],[664])).
% 63.68/15.71 thf(666,plain,(! [A:$i] : ((~ (rel_s4 @ A @ sk1)) | (rel_s4 @ A @ sk2))),inference(pattern_uni,[status(thm)],[665:[bind(A, $thf(A)),bind(B, $thf(sk1)),bind(C, $thf(sk2))]])).
% 63.68/15.71 thf(10,axiom,((mvalid @ (mexists_ind @ (^ [A:mu]: (mbox_s4 @ (mand @ (entry_box @ A) @ (number @ A @ one))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2)).
% 63.68/15.71 thf(38,plain,((! [A:$i]: ~ (! [B:mu]: ((exists_in_world @ B @ A) => (~ (! [C:$i]: (~ (rel_s4 @ A @ C) | ~ (~ (entry_box @ B @ C) | ~ (number @ B @ one @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 63.68/15.71 thf(39,plain,((~ (? [A:$i]: ! [B:mu]: ((exists_in_world @ B @ A) => (~ (! [C:$i]: (~ (rel_s4 @ A @ C) | ~ (~ (entry_box @ B @ C) | ~ (number @ B @ one @ C))))))))),inference(miniscope,[status(thm)],[38])).
% 63.68/15.71 thf(40,plain,(! [B:$i,A:$i] : (((exists_in_world @ (sk9 @ A) @ A) & (~ (rel_s4 @ A @ B) | (entry_box @ (sk9 @ A) @ B)) & (~ (rel_s4 @ A @ B) | (number @ (sk9 @ A) @ one @ B))))),inference(cnf,[status(esa)],[39])).
% 63.68/15.71 thf(42,plain,(! [B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (entry_box @ (sk9 @ A) @ B))),inference(cnfConj,[status(thm)],[40])).
% 63.68/15.71 thf(274,plain,(! [B:$i,A:$i] : (~ (($true)) | (entry_box @ (sk9 @ A) @ B) | ((rel_s4 @ sk1 @ sk2) != (rel_s4 @ A @ B)))),inference(paramod_ordered,[status(thm)],[18,42])).
% 63.68/15.71 thf(275,plain,(! [B:$i,A:$i] : ((entry_box @ (sk9 @ A) @ B) | ((rel_s4 @ sk1 @ sk2) != (rel_s4 @ A @ B)))),inference(simp,[status(thm)],[274])).
% 63.68/15.71 thf(276,plain,((entry_box @ (sk9 @ sk1) @ sk2)),inference(pattern_uni,[status(thm)],[275:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 63.68/15.71 thf(9,axiom,((mvalid @ (mbox_s4 @ (mexists_ind @ (^ [A:mu]: (mbox_s4 @ (mand @ (userid @ u @ A) @ (string @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1)).
% 63.68/15.71 thf(33,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ~ (! [C:mu]: ((exists_in_world @ C @ B) => (~ (! [D:$i]: (~ (rel_s4 @ B @ D) | ~ (~ (userid @ u @ C @ D) | ~ (string @ C @ D)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 63.68/15.71 thf(34,plain,(! [C:$i,B:$i,A:$i] : (((~ (rel_s4 @ A @ B) | (exists_in_world @ (sk8 @ B @ A) @ B)) & (~ (rel_s4 @ A @ B) | ~ (rel_s4 @ B @ C) | (userid @ u @ (sk8 @ B @ A) @ C)) & (~ (rel_s4 @ A @ B) | ~ (rel_s4 @ B @ C) | (string @ (sk8 @ B @ A) @ C))))),inference(cnf,[status(esa)],[33])).
% 63.68/15.71 thf(35,plain,(! [B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (exists_in_world @ (sk8 @ B @ A) @ B))),inference(cnfConj,[status(thm)],[34])).
% 63.68/15.71 thf(472,plain,(! [B:$i,A:$i] : (~ (($true)) | (exists_in_world @ (sk8 @ B @ A) @ B) | ((rel_s4 @ sk1 @ sk2) != (rel_s4 @ A @ B)))),inference(paramod_ordered,[status(thm)],[18,35])).
% 63.68/15.71 thf(473,plain,(! [B:$i,A:$i] : ((exists_in_world @ (sk8 @ B @ A) @ B) | ((rel_s4 @ sk1 @ sk2) != (rel_s4 @ A @ B)))),inference(simp,[status(thm)],[472])).
% 63.68/15.71 thf(474,plain,((exists_in_world @ (sk8 @ sk2 @ sk1) @ sk2)),inference(pattern_uni,[status(thm)],[473:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 63.68/15.71 thf(7,axiom,((! [A:$i]: (exists_in_world @ one @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_one_ax)).
% 63.68/15.71 thf(29,plain,((! [A:$i]: (exists_in_world @ one @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 63.68/15.71 thf(30,plain,(! [A:$i] : ((exists_in_world @ one @ A))),inference(cnf,[status(esa)],[29])).
% 63.68/15.71 thf(8,axiom,((! [A:$i]: (exists_in_world @ u @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_u_ax)).
% 63.68/15.71 thf(31,plain,((! [A:$i]: (exists_in_world @ u @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 63.68/15.71 thf(32,plain,(! [A:$i] : ((exists_in_world @ u @ A))),inference(cnf,[status(esa)],[31])).
% 63.68/15.71 thf(14,plain,(! [D:mu,C:mu,B:mu,A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (exists_in_world @ C @ sk2)) | (~ (exists_in_world @ D @ sk2)) | (~ (sk3 @ A @ C @ D @ B)) | (~ (in @ A @ B @ (sk6 @ D @ C @ B @ A) @ (sk5 @ D @ C @ B @ A))))),inference(cnfConj,[status(thm)],[13])).
% 63.68/15.71 thf(63,plain,(! [E:mu,D:mu,C:mu,B:mu,A:$i] : ((~ (exists_in_world @ B @ sk2)) | ~ (($true)) | (~ (exists_in_world @ D @ sk2)) | (~ (exists_in_world @ E @ sk2)) | (~ (sk3 @ B @ D @ E @ C)) | (~ (in @ B @ C @ (sk6 @ E @ D @ C @ B) @ (sk5 @ E @ D @ C @ B))) | ((exists_in_world @ one @ A) != (exists_in_world @ C @ sk2)))),inference(paramod_ordered,[status(thm)],[30,14])).
% 63.68/15.71 thf(64,plain,(! [E:mu,D:mu,C:mu,B:mu,A:$i] : ((~ (exists_in_world @ B @ sk2)) | (~ (exists_in_world @ D @ sk2)) | (~ (exists_in_world @ E @ sk2)) | (~ (sk3 @ B @ D @ E @ C)) | (~ (in @ B @ C @ (sk6 @ E @ D @ C @ B) @ (sk5 @ E @ D @ C @ B))) | ((exists_in_world @ one @ A) != (exists_in_world @ C @ sk2)))),inference(simp,[status(thm)],[63])).
% 63.68/15.71 thf(65,plain,(! [C:mu,B:mu,A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (exists_in_world @ C @ sk2)) | (~ (sk3 @ A @ B @ C @ one)) | (~ (in @ A @ one @ (sk6 @ C @ B @ one @ A) @ (sk5 @ C @ B @ one @ A))))),inference(pattern_uni,[status(thm)],[64:[bind(A, $thf(sk2)),bind(B, $thf(B)),bind(C, $thf(one))]])).
% 63.68/15.71 thf(72,plain,(! [C:mu,B:mu,A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (exists_in_world @ C @ sk2)) | (~ (sk3 @ A @ B @ C @ one)) | (~ (in @ A @ one @ (sk6 @ C @ B @ one @ A) @ (sk5 @ C @ B @ one @ A))))),inference(simp,[status(thm)],[65])).
% 63.68/15.71 thf(80,plain,(! [D:mu,C:mu,B:mu,A:$i] : (~ (($true)) | (~ (exists_in_world @ C @ sk2)) | (~ (exists_in_world @ D @ sk2)) | (~ (sk3 @ B @ C @ D @ one)) | (~ (in @ B @ one @ (sk6 @ D @ C @ one @ B) @ (sk5 @ D @ C @ one @ B))) | ((exists_in_world @ u @ A) != (exists_in_world @ B @ sk2)))),inference(paramod_ordered,[status(thm)],[32,72])).
% 63.68/15.71 thf(81,plain,(! [D:mu,C:mu,B:mu,A:$i] : ((~ (exists_in_world @ C @ sk2)) | (~ (exists_in_world @ D @ sk2)) | (~ (sk3 @ B @ C @ D @ one)) | (~ (in @ B @ one @ (sk6 @ D @ C @ one @ B) @ (sk5 @ D @ C @ one @ B))) | ((exists_in_world @ u @ A) != (exists_in_world @ B @ sk2)))),inference(simp,[status(thm)],[80])).
% 63.68/15.71 thf(82,plain,(! [B:mu,A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (sk3 @ u @ A @ B @ one)) | (~ (in @ u @ one @ (sk6 @ B @ A @ one @ u) @ (sk5 @ B @ A @ one @ u))))),inference(pattern_uni,[status(thm)],[81:[bind(A, $thf(sk2)),bind(B, $thf(u))]])).
% 63.68/15.71 thf(99,plain,(! [B:mu,A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (sk3 @ u @ A @ B @ one)) | (~ (in @ u @ one @ (sk6 @ B @ A @ one @ u) @ (sk5 @ B @ A @ one @ u))))),inference(simp,[status(thm)],[82])).
% 63.68/15.71 thf(144,plain,(! [C:mu,B:mu,A:$i] : (~ (($true)) | (~ (exists_in_world @ C @ sk2)) | (~ (sk3 @ u @ B @ C @ one)) | (~ (in @ u @ one @ (sk6 @ C @ B @ one @ u) @ (sk5 @ C @ B @ one @ u))) | ((exists_in_world @ one @ A) != (exists_in_world @ B @ sk2)))),inference(paramod_ordered,[status(thm)],[30,99])).
% 63.68/15.71 thf(145,plain,(! [C:mu,B:mu,A:$i] : ((~ (exists_in_world @ C @ sk2)) | (~ (sk3 @ u @ B @ C @ one)) | (~ (in @ u @ one @ (sk6 @ C @ B @ one @ u) @ (sk5 @ C @ B @ one @ u))) | ((exists_in_world @ one @ A) != (exists_in_world @ B @ sk2)))),inference(simp,[status(thm)],[144])).
% 63.68/15.71 thf(146,plain,(! [A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (sk3 @ u @ one @ A @ one)) | (~ (in @ u @ one @ (sk6 @ A @ one @ one @ u) @ (sk5 @ A @ one @ one @ u))))),inference(pattern_uni,[status(thm)],[145:[bind(A, $thf(sk2)),bind(B, $thf(one))]])).
% 63.68/15.71 thf(150,plain,(! [A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (sk3 @ u @ one @ A @ one)) | (~ (in @ u @ one @ (sk6 @ A @ one @ one @ u) @ (sk5 @ A @ one @ one @ u))))),inference(simp,[status(thm)],[146])).
% 63.68/15.71 thf(548,plain,(! [A:mu] : (~ (($true)) | (~ (sk3 @ u @ one @ A @ one)) | (~ (in @ u @ one @ (sk6 @ A @ one @ one @ u) @ (sk5 @ A @ one @ one @ u))) | ((exists_in_world @ (sk8 @ sk2 @ sk1) @ sk2) != (exists_in_world @ A @ sk2)))),inference(paramod_ordered,[status(thm)],[474,150])).
% 63.68/15.71 thf(549,plain,(! [A:mu] : ((~ (sk3 @ u @ one @ A @ one)) | (~ (in @ u @ one @ (sk6 @ A @ one @ one @ u) @ (sk5 @ A @ one @ one @ u))) | ((exists_in_world @ (sk8 @ sk2 @ sk1) @ sk2) != (exists_in_world @ A @ sk2)))),inference(simp,[status(thm)],[548])).
% 63.68/15.71 thf(550,plain,((~ (sk3 @ u @ one @ (sk8 @ sk2 @ sk1) @ one)) | (~ (in @ u @ one @ (sk6 @ (sk8 @ sk2 @ sk1) @ one @ one @ u) @ (sk5 @ (sk8 @ sk2 @ sk1) @ one @ one @ u)))),inference(pattern_uni,[status(thm)],[549:[bind(A, $thf(sk8 @ sk2 @ sk1))]])).
% 63.68/15.71 thf(162,plain,(! [B:mu,A:$i] : (~ (($true)) | (~ (sk3 @ u @ one @ B @ one)) | (~ (in @ u @ one @ (sk6 @ B @ one @ one @ u) @ (sk5 @ B @ one @ one @ u))) | ((exists_in_world @ one @ A) != (exists_in_world @ B @ sk2)))),inference(paramod_ordered,[status(thm)],[30,150])).
% 63.68/15.71 thf(163,plain,(! [B:mu,A:$i] : ((~ (sk3 @ u @ one @ B @ one)) | (~ (in @ u @ one @ (sk6 @ B @ one @ one @ u) @ (sk5 @ B @ one @ one @ u))) | ((exists_in_world @ one @ A) != (exists_in_world @ B @ sk2)))),inference(simp,[status(thm)],[162])).
% 63.68/15.71 thf(164,plain,((~ (sk3 @ u @ one @ one @ one)) | (~ (in @ u @ one @ (sk6 @ one @ one @ one @ u) @ (sk5 @ one @ one @ one @ u)))),inference(pattern_uni,[status(thm)],[163:[bind(A, $thf(sk2)),bind(B, $thf(one))]])).
% 63.68/15.71 thf(4,axiom,((mreflexive @ rel_s4)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1)).
% 63.68/15.71 thf(23,plain,((! [A:$i]: (rel_s4 @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 63.68/15.71 thf(24,plain,(! [A:$i] : ((rel_s4 @ A @ A))),inference(cnf,[status(esa)],[23])).
% 63.68/15.71 thf(469,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (exists_in_world @ (sk8 @ C @ B) @ C) | ((rel_s4 @ A @ A) != (rel_s4 @ B @ C)))),inference(paramod_ordered,[status(thm)],[24,35])).
% 63.68/15.71 thf(470,plain,(! [C:$i,B:$i,A:$i] : ((exists_in_world @ (sk8 @ C @ B) @ C) | ((rel_s4 @ A @ A) != (rel_s4 @ B @ C)))),inference(simp,[status(thm)],[469])).
% 63.68/15.71 thf(471,plain,(! [A:$i] : ((exists_in_world @ (sk8 @ A @ A) @ A))),inference(pattern_uni,[status(thm)],[470:[bind(A, $thf(A)),bind(B, $thf(A)),bind(C, $thf(A))]])).
% 63.68/15.71 thf(41,plain,(! [A:$i] : ((exists_in_world @ (sk9 @ A) @ A))),inference(cnfConj,[status(thm)],[40])).
% 63.68/15.71 thf(614,plain,(! [B:mu,A:$i] : (~ (($true)) | (~ (sk3 @ u @ one @ B @ one)) | (~ (in @ u @ one @ (sk6 @ B @ one @ one @ u) @ (sk5 @ B @ one @ one @ u))) | ((exists_in_world @ (sk8 @ A @ A) @ A) != (exists_in_world @ B @ sk2)))),inference(paramod_ordered,[status(thm)],[471,150])).
% 63.68/15.71 thf(615,plain,(! [B:mu,A:$i] : ((~ (sk3 @ u @ one @ B @ one)) | (~ (in @ u @ one @ (sk6 @ B @ one @ one @ u) @ (sk5 @ B @ one @ one @ u))) | ((exists_in_world @ (sk8 @ A @ A) @ A) != (exists_in_world @ B @ sk2)))),inference(simp,[status(thm)],[614])).
% 63.68/15.71 thf(616,plain,((~ (sk3 @ u @ one @ (sk8 @ sk2 @ sk2) @ one)) | (~ (in @ u @ one @ (sk6 @ (sk8 @ sk2 @ sk2) @ one @ one @ u) @ (sk5 @ (sk8 @ sk2 @ sk2) @ one @ one @ u)))),inference(pattern_uni,[status(thm)],[615:[bind(A, $thf(sk2)),bind(B, $thf(sk8 @ sk2 @ sk2))]])).
% 63.68/15.71 thf(661,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (~ (rel_s4 @ B @ C)) | (rel_s4 @ A @ C) | ((rel_s4 @ sk1 @ sk2) != (rel_s4 @ A @ B)))),inference(paramod_ordered,[status(thm)],[18,26])).
% 63.68/15.71 thf(662,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel_s4 @ B @ C)) | (rel_s4 @ A @ C) | ((rel_s4 @ sk1 @ sk2) != (rel_s4 @ A @ B)))),inference(simp,[status(thm)],[661])).
% 63.68/15.71 thf(663,plain,(! [A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (rel_s4 @ sk1 @ A))),inference(pattern_uni,[status(thm)],[662:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 63.68/15.71 thf(680,plain,(! [A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (rel_s4 @ sk1 @ A))),inference(simp,[status(thm)],[663])).
% 63.68/15.71 thf(15,plain,(! [D:mu,C:mu,B:mu,A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (exists_in_world @ C @ sk2)) | (~ (exists_in_world @ D @ sk2)) | (~ (sk3 @ A @ C @ D @ B)) | (rel_s4 @ sk2 @ (sk5 @ D @ C @ B @ A)))),inference(cnfConj,[status(thm)],[13])).
% 63.68/15.71 thf(252,plain,(! [B:mu,A:$i] : (~ (($true)) | (~ (sk3 @ u @ one @ B @ one)) | (~ (in @ u @ one @ (sk6 @ B @ one @ one @ u) @ (sk5 @ B @ one @ one @ u))) | ((exists_in_world @ (sk9 @ A) @ A) != (exists_in_world @ B @ sk2)))),inference(paramod_ordered,[status(thm)],[41,150])).
% 63.68/15.71 thf(253,plain,(! [B:mu,A:$i] : ((~ (sk3 @ u @ one @ B @ one)) | (~ (in @ u @ one @ (sk6 @ B @ one @ one @ u) @ (sk5 @ B @ one @ one @ u))) | ((exists_in_world @ (sk9 @ A) @ A) != (exists_in_world @ B @ sk2)))),inference(simp,[status(thm)],[252])).
% 63.68/15.71 thf(254,plain,((~ (sk3 @ u @ one @ (sk9 @ sk2) @ one)) | (~ (in @ u @ one @ (sk6 @ (sk9 @ sk2) @ one @ one @ u) @ (sk5 @ (sk9 @ sk2) @ one @ one @ u)))),inference(pattern_uni,[status(thm)],[253:[bind(A, $thf(sk2)),bind(B, $thf(sk9 @ sk2))]])).
% 63.68/15.71 thf(685,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ sk1)) | ~ (($true)) | (exists_in_world @ (sk8 @ C @ B) @ C) | ((rel_s4 @ A @ sk2) != (rel_s4 @ B @ C)))),inference(paramod_ordered,[status(thm)],[666,35])).
% 63.68/15.71 thf(686,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ sk1)) | (exists_in_world @ (sk8 @ C @ B) @ C) | ((rel_s4 @ A @ sk2) != (rel_s4 @ B @ C)))),inference(simp,[status(thm)],[685])).
% 63.68/15.71 thf(687,plain,(! [A:$i] : ((~ (rel_s4 @ A @ sk1)) | (exists_in_world @ (sk8 @ sk2 @ A) @ sk2))),inference(pattern_uni,[status(thm)],[686:[bind(A, $thf(A)),bind(B, $thf(A)),bind(C, $thf(sk2))]])).
% 63.68/15.71 thf(690,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ sk1)) | ~ (($true)) | (entry_box @ (sk9 @ B) @ C) | ((rel_s4 @ A @ sk2) != (rel_s4 @ B @ C)))),inference(paramod_ordered,[status(thm)],[666,42])).
% 63.68/15.71 thf(691,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ sk1)) | (entry_box @ (sk9 @ B) @ C) | ((rel_s4 @ A @ sk2) != (rel_s4 @ B @ C)))),inference(simp,[status(thm)],[690])).
% 63.68/15.71 thf(692,plain,(! [A:$i] : ((~ (rel_s4 @ A @ sk1)) | (entry_box @ (sk9 @ A) @ sk2))),inference(pattern_uni,[status(thm)],[691:[bind(A, $thf(A)),bind(B, $thf(A)),bind(C, $thf(sk2))]])).
% 63.68/15.71 thf(3,axiom,((! [A:$i]: ? [B:mu]: (exists_in_world @ B @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',nonempty_ax)).
% 63.68/15.71 thf(21,plain,((! [A:$i]: ? [B:mu]: (exists_in_world @ B @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 63.68/15.71 thf(22,plain,(! [A:$i] : ((exists_in_world @ (sk7 @ A) @ A))),inference(cnf,[status(esa)],[21])).
% 63.68/15.71 thf(159,plain,(! [B:mu,A:$i] : (~ (($true)) | (~ (sk3 @ u @ one @ B @ one)) | (~ (in @ u @ one @ (sk6 @ B @ one @ one @ u) @ (sk5 @ B @ one @ one @ u))) | ((exists_in_world @ (sk7 @ A) @ A) != (exists_in_world @ B @ sk2)))),inference(paramod_ordered,[status(thm)],[22,150])).
% 63.68/15.71 thf(160,plain,(! [B:mu,A:$i] : ((~ (sk3 @ u @ one @ B @ one)) | (~ (in @ u @ one @ (sk6 @ B @ one @ one @ u) @ (sk5 @ B @ one @ one @ u))) | ((exists_in_world @ (sk7 @ A) @ A) != (exists_in_world @ B @ sk2)))),inference(simp,[status(thm)],[159])).
% 63.68/15.71 thf(161,plain,((~ (sk3 @ u @ one @ (sk7 @ sk2) @ one)) | (~ (in @ u @ one @ (sk6 @ (sk7 @ sk2) @ one @ one @ u) @ (sk5 @ (sk7 @ sk2) @ one @ one @ u)))),inference(pattern_uni,[status(thm)],[160:[bind(A, $thf(sk2)),bind(B, $thf(sk7 @ sk2))]])).
% 63.68/15.71 thf(17,plain,(! [D:mu,C:mu,B:mu,A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (exists_in_world @ C @ sk2)) | (~ (exists_in_world @ D @ sk2)) | (~ (userid @ u @ A @ (sk4 @ D @ C @ B @ A))) | (~ (entry_box @ B @ (sk4 @ D @ C @ B @ A))) | (~ (number @ B @ one @ (sk4 @ D @ C @ B @ A))) | (sk3 @ A @ C @ D @ B))),inference(cnfConj,[status(thm)],[13])).
% 63.68/15.71 thf(11,axiom,((mvalid @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mforall_ind @ (^ [B:mu]: (mforall_ind @ (^ [C:mu]: (mimplies @ (mand @ (string @ B) @ (entry_box @ C)) @ (mexists_ind @ (^ [D:mu]: (mbox_s4 @ (mforall_ind @ (^ [E:mu]: (mimplies @ (do @ A @ D @ E) @ (in @ B @ C @ E))))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3)).
% 63.68/15.71 thf(44,plain,((! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:mu]: ((exists_in_world @ D @ B) => (! [E:mu]: ((exists_in_world @ E @ B) => (~ (string @ D @ B) | ~ (entry_box @ E @ B) | ~ (! [F:mu]: ((exists_in_world @ F @ B) => (~ (! [G:$i]: (~ (rel_s4 @ B @ G) | ! [H:mu]: ((exists_in_world @ H @ G) => (~ (do @ C @ F @ H @ G) | (in @ D @ E @ H @ G))))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 63.68/15.71 thf(43,plain,(! [B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (number @ (sk9 @ A) @ one @ B))),inference(cnfConj,[status(thm)],[40])).
% 63.68/15.71 thf(284,plain,(! [B:$i,A:$i] : (~ (($true)) | (number @ (sk9 @ A) @ one @ B) | ((rel_s4 @ sk1 @ sk2) != (rel_s4 @ A @ B)))),inference(paramod_ordered,[status(thm)],[18,43])).
% 63.68/15.71 thf(285,plain,(! [B:$i,A:$i] : ((number @ (sk9 @ A) @ one @ B) | ((rel_s4 @ sk1 @ sk2) != (rel_s4 @ A @ B)))),inference(simp,[status(thm)],[284])).
% 63.68/15.71 thf(286,plain,((number @ (sk9 @ sk1) @ one @ sk2)),inference(pattern_uni,[status(thm)],[285:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 63.68/15.71 thf(6,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)).
% 63.68/15.71 thf(27,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)],[6])).
% 63.68/15.71 thf(16,plain,(! [D:mu,C:mu,B:mu,A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (exists_in_world @ C @ sk2)) | (~ (exists_in_world @ D @ sk2)) | (~ (sk3 @ A @ C @ D @ B)) | (exists_in_world @ (sk6 @ D @ C @ B @ A) @ (sk5 @ D @ C @ B @ A)))),inference(cnfConj,[status(thm)],[13])).
% 63.68/15.71 thf(156,plain,(! [B:mu,A:$i] : (~ (($true)) | (~ (sk3 @ u @ one @ B @ one)) | (~ (in @ u @ one @ (sk6 @ B @ one @ one @ u) @ (sk5 @ B @ one @ one @ u))) | ((exists_in_world @ u @ A) != (exists_in_world @ B @ sk2)))),inference(paramod_ordered,[status(thm)],[32,150])).
% 63.68/15.71 thf(157,plain,(! [B:mu,A:$i] : ((~ (sk3 @ u @ one @ B @ one)) | (~ (in @ u @ one @ (sk6 @ B @ one @ one @ u) @ (sk5 @ B @ one @ one @ u))) | ((exists_in_world @ u @ A) != (exists_in_world @ B @ sk2)))),inference(simp,[status(thm)],[156])).
% 63.68/15.71 thf(158,plain,((~ (sk3 @ u @ one @ u @ one)) | (~ (in @ u @ one @ (sk6 @ u @ one @ one @ u) @ (sk5 @ u @ one @ one @ u)))),inference(pattern_uni,[status(thm)],[157:[bind(A, $thf(sk2)),bind(B, $thf(u))]])).
% 63.68/15.71 thf(147,plain,(! [C:mu,B:mu,A:$i] : ((~ (exists_in_world @ B @ sk2)) | ~ (($true)) | (~ (sk3 @ u @ B @ C @ one)) | (~ (in @ u @ one @ (sk6 @ C @ B @ one @ u) @ (sk5 @ C @ B @ one @ u))) | ((exists_in_world @ one @ A) != (exists_in_world @ C @ sk2)))),inference(paramod_ordered,[status(thm)],[30,99])).
% 63.68/15.71 thf(148,plain,(! [C:mu,B:mu,A:$i] : ((~ (exists_in_world @ B @ sk2)) | (~ (sk3 @ u @ B @ C @ one)) | (~ (in @ u @ one @ (sk6 @ C @ B @ one @ u) @ (sk5 @ C @ B @ one @ u))) | ((exists_in_world @ one @ A) != (exists_in_world @ C @ sk2)))),inference(simp,[status(thm)],[147])).
% 63.68/15.71 thf(149,plain,(! [A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (sk3 @ u @ A @ one @ one)) | (~ (in @ u @ one @ (sk6 @ one @ A @ one @ u) @ (sk5 @ one @ A @ one @ u))))),inference(pattern_uni,[status(thm)],[148:[bind(A, $thf(sk2)),bind(B, $thf(B)),bind(C, $thf(one))]])).
% 63.68/15.71 thf(151,plain,(! [A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (sk3 @ u @ A @ one @ one)) | (~ (in @ u @ one @ (sk6 @ one @ A @ one @ u) @ (sk5 @ one @ A @ one @ u))))),inference(simp,[status(thm)],[149])).
% 63.68/15.71 thf(19,plain,(! [D:mu,C:mu,B:mu,A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (exists_in_world @ C @ sk2)) | (~ (exists_in_world @ D @ sk2)) | (rel_s4 @ sk2 @ (sk4 @ D @ C @ B @ A)) | (sk3 @ A @ C @ D @ B))),inference(cnfConj,[status(thm)],[13])).
% 63.68/15.71 thf(271,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (entry_box @ (sk9 @ B) @ C) | ((rel_s4 @ A @ A) != (rel_s4 @ B @ C)))),inference(paramod_ordered,[status(thm)],[24,42])).
% 63.68/15.71 thf(272,plain,(! [C:$i,B:$i,A:$i] : ((entry_box @ (sk9 @ B) @ C) | ((rel_s4 @ A @ A) != (rel_s4 @ B @ C)))),inference(simp,[status(thm)],[271])).
% 63.68/15.71 thf(273,plain,(! [A:$i] : ((entry_box @ (sk9 @ A) @ A))),inference(pattern_uni,[status(thm)],[272:[bind(A, $thf(A)),bind(B, $thf(A)),bind(C, $thf(A))]])).
% 63.68/15.71 thf(281,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (number @ (sk9 @ B) @ one @ C) | ((rel_s4 @ A @ A) != (rel_s4 @ B @ C)))),inference(paramod_ordered,[status(thm)],[24,43])).
% 63.68/15.71 thf(282,plain,(! [C:$i,B:$i,A:$i] : ((number @ (sk9 @ B) @ one @ C) | ((rel_s4 @ A @ A) != (rel_s4 @ B @ C)))),inference(simp,[status(thm)],[281])).
% 63.68/15.71 thf(283,plain,(! [A:$i] : ((number @ (sk9 @ A) @ one @ A))),inference(pattern_uni,[status(thm)],[282:[bind(A, $thf(A)),bind(B, $thf(A)),bind(C, $thf(A))]])).
% 63.68/15.71 thf(12849,plain,(($false)),inference(e,[status(thm)],[666,276,550,14,29,164,471,41,12,616,35,680,99,15,254,42,24,25,687,692,38,21,33,32,161,17,22,44,286,27,18,150,16,31,72,43,26,158,23,151,30,19,273,474,283])).
% 63.68/15.71 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 63.68/15.71 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------