%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYN052^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 : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:41:29 AM UTC 2026
% Result : Theorem 82.17s 25.91s
% Output : Refutation 82.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN052^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.12/0.19 % Computer : n013.cluster.edu
% 0.12/0.19 % Model : x86_64 x86_64
% 0.12/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.19 % Memory : 8046.5625MB
% 0.12/0.19 % OS : Linux 6.8.0-71-generic
% 0.12/0.19 % CPULimit : 300
% 0.12/0.19 % WCLimit : 300
% 0.12/0.19 % DateTime : Tue Sep 29 16:13:36 UTC 2026
% 0.12/0.19 % CPUTime :
% 0.12/0.19 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.90/0.78 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.60/1.04 % [INFO] Parsing done (261ms).
% 1.60/1.06 % [INFO] Running in sequential loop mode.
% 2.13/1.46 % [INFO] eprover registered as external prover.
% 2.13/1.46 % [INFO] Scanning for conjecture ...
% 2.56/1.65 % [INFO] Found a conjecture (or negated_conjecture) and 4 axioms. Running axiom selection ...
% 2.56/1.69 % [INFO] Axiom selection finished. Selected 4 axioms (removed 0 axioms).
% 2.76/1.70 % [INFO] Problem is higher-order (TPTP THF).
% 2.76/1.70 % [INFO] Type checking passed.
% 2.76/1.71 % [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 ...
% 82.17/25.90 % External prover 'e' found a proof!
% 82.17/25.90 % [INFO] Killing All external provers ...
% 82.17/25.90 % Time passed: 25566ms (effective reasoning time: 24839ms)
% 82.17/25.90 % 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)>
% 82.17/25.90 % Axioms used in derivation (4): a2, a1, cumulative_ax, nonempty_ax
% 82.17/25.90 % No. of inferences in proof: 234
% 82.17/25.91 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 25566 ms resp. 24839 ms w/o parsing
% 82.65/26.09 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 82.65/26.09 thf(mu_type, type, mu: $tType).
% 82.65/26.09 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 82.65/26.09 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 82.65/26.09 thf(mand_decl, type, mand: (($i > $o) > (($i > $o) > ($i > $o)))).
% 82.65/26.09 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 82.65/26.09 thf(exists_in_world_decl, type, exists_in_world: (mu > ($i > $o))).
% 82.65/26.09 thf(mforall_ind_decl, type, mforall_ind: ((mu > ($i > $o)) > ($i > $o))).
% 82.65/26.09 thf(mreflexive_decl, type, mreflexive: (($i > ($i > $o)) > $o)).
% 82.65/26.09 thf(mtransitive_decl, type, mtransitive: (($i > ($i > $o)) > $o)).
% 82.65/26.09 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 82.65/26.09 thf(rel_s4_decl, type, rel_s4: ($i > ($i > $o))).
% 82.65/26.09 thf(mbox_s4_decl, type, mbox_s4: (($i > $o) > ($i > $o))).
% 82.65/26.09 thf(p_decl, type, p: ($i > $o)).
% 82.65/26.09 thf(big_f_decl, type, big_f: (mu > ($i > $o))).
% 82.65/26.09 thf(sk1_decl, type, sk1: $i).
% 82.65/26.09 thf(sk2_decl, type, sk2: $i).
% 82.65/26.09 thf(sk3_decl, type, sk3: ($i > (mu > ($i > $i)))).
% 82.65/26.09 thf(sk4_decl, type, sk4: ($i > (mu > ($i > $i)))).
% 82.65/26.09 thf(sk5_decl, type, sk5: $o).
% 82.65/26.09 thf(sk6_decl, type, sk6: $i).
% 82.65/26.09 thf(sk7_decl, type, sk7: $i).
% 82.65/26.09 thf(sk8_decl, type, sk8: mu).
% 82.65/26.09 thf(sk9_decl, type, sk9: $i).
% 82.65/26.09 thf(sk10_decl, type, sk10: $i).
% 82.65/26.09 thf(sk11_decl, type, sk11: $i).
% 82.65/26.09 thf(sk12_decl, type, sk12: ($i > mu)).
% 82.65/26.09 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 82.65/26.09 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 82.65/26.09 thf(mand_def, definition, mand = (^ [A:($i > $o),B:($i > $o)]: (mnot @ (mor @ (mnot @ A) @ (mnot @ B)))) ).
% 82.65/26.09 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 82.65/26.09 thf(mforall_ind_def, definition, mforall_ind = (^ [A:(mu > ($i > $o)),B:$i]: ! [C:mu]: ((exists_in_world @ C @ B) => (A @ C @ B))) ).
% 82.65/26.09 thf(mreflexive_def, definition, mreflexive = (^ [A:($i > ($i > $o))]: ! [B:$i]: (A @ B @ B)) ).
% 82.65/26.09 thf(mtransitive_def, definition, mtransitive = (^ [A:($i > ($i > $o))]: ! [B:$i,C:$i,D:$i]: (((A @ B @ C) & (A @ C @ D)) => (A @ B @ D))) ).
% 82.65/26.09 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 82.65/26.09 thf(mbox_s4_def, definition, mbox_s4 = (^ [A:($i > $o),B:$i]: ! [C:$i]: (~ (rel_s4 @ B @ C) | (A @ C))) ).
% 82.65/26.09 thf(sk1_def, definition, sk1 = (@+ [A:$i]: ~ (! [B:$i]: (~ (rel_s4 @ A @ B) | ~ (! [C:$i]: (~ (rel_s4 @ B @ C) | ! [D:mu]: ((exists_in_world @ D @ C) => (~ (~ (! [E:$i]: (~ (rel_s4 @ C @ E) | ~ (! [F:$i]: (~ (rel_s4 @ E @ F) | (p @ F))) | ! [F:$i]: (~ (rel_s4 @ E @ F) | (big_f @ D @ F)))) | ~ (! [E:$i]: (~ (rel_s4 @ C @ E) | ~ (! [F:$i]: (~ (rel_s4 @ E @ F) | (big_f @ D @ F))) | ! [F:$i]: (~ (rel_s4 @ E @ F) | (p @ F))))))))) | ~ (~ (! [C:$i]: (~ (rel_s4 @ B @ C) | ~ (! [D:$i]: (~ (rel_s4 @ C @ D) | (p @ D))) | ! [D:$i]: (~ (rel_s4 @ C @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | (big_f @ E @ F))))))) | ~ (! [C:$i]: (~ (rel_s4 @ B @ C) | ~ (! [D:$i]: (~ (rel_s4 @ C @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | (big_f @ E @ F)))))) | ! [D:$i]: (~ (rel_s4 @ C @ D) | (p @ D)))))))) ).
% 82.65/26.09 thf(sk2_def, definition, sk2 = (@+ [A:$i]: ~ (~ (rel_s4 @ sk1 @ A) | ~ (! [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) | (p @ E))) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (big_f @ C @ E)))) | ~ (! [D:$i]: (~ (rel_s4 @ B @ D) | ~ (! [E:$i]: (~ (rel_s4 @ D @ E) | (big_f @ C @ E))) | ! [E:$i]: (~ (rel_s4 @ D @ E) | (p @ E))))))))) | ~ (~ (! [B:$i]: (~ (rel_s4 @ A @ B) | ~ (! [C:$i]: (~ (rel_s4 @ B @ C) | (p @ C))) | ! [C:$i]: (~ (rel_s4 @ B @ C) | ! [D:mu]: ((exists_in_world @ D @ C) => (! [E:$i]: (~ (rel_s4 @ C @ E) | (big_f @ D @ E))))))) | ~ (! [B:$i]: (~ (rel_s4 @ A @ B) | ~ (! [C:$i]: (~ (rel_s4 @ B @ C) | ! [D:mu]: ((exists_in_world @ D @ C) => (! [E:$i]: (~ (rel_s4 @ C @ E) | (big_f @ D @ E)))))) | ! [C:$i]: (~ (rel_s4 @ B @ C) | (p @ C))))))) ).
% 82.65/26.09 thf(sk3_def, definition, sk3 = (^ [A:$i,B:mu,C:$i]: (@+ [D:$i]: ~ (~ (rel_s4 @ A @ D) | (p @ D)))) ).
% 82.65/26.09 thf(sk4_def, definition, sk4 = (^ [A:$i,B:mu,C:$i]: (@+ [D:$i]: ~ (~ (rel_s4 @ A @ D) | (big_f @ B @ D)))) ).
% 82.65/26.09 thf(sk6_def, definition, sk6 = (@+ [A:$i]: ~ (~ (rel_s4 @ sk2 @ A) | ~ (! [B:$i]: (~ (rel_s4 @ A @ B) | (p @ B))) | ! [B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (big_f @ C @ D))))))) ).
% 82.65/26.09 thf(sk7_def, definition, sk7 = (@+ [A:$i]: ~ (~ (rel_s4 @ sk6 @ A) | ! [B:mu]: ((exists_in_world @ B @ A) => (! [C:$i]: (~ (rel_s4 @ A @ C) | (big_f @ B @ C)))))) ).
% 82.65/26.09 thf(sk8_def, definition, sk8 = (@+ [A:mu]: ~ ((exists_in_world @ A @ sk7) => (! [B:$i]: (~ (rel_s4 @ sk7 @ B) | (big_f @ A @ B))))) ).
% 82.65/26.09 thf(sk9_def, definition, sk9 = (@+ [A:$i]: ~ (~ (rel_s4 @ sk7 @ A) | (big_f @ sk8 @ A))) ).
% 82.65/26.09 thf(sk10_def, definition, sk10 = (@+ [A:$i]: ~ (~ (rel_s4 @ sk2 @ A) | ~ (! [B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (! [D:$i]: (~ (rel_s4 @ B @ D) | (big_f @ C @ D)))))) | ! [B:$i]: (~ (rel_s4 @ A @ B) | (p @ B)))) ).
% 82.65/26.09 thf(sk11_def, definition, sk11 = (@+ [A:$i]: ~ (~ (rel_s4 @ sk10 @ A) | (p @ A))) ).
% 82.65/26.09 thf(sk12_def, definition, sk12 = (^ [A:$i]: (@+ [B:mu]: (exists_in_world @ B @ A))) ).
% 82.65/26.09 thf(1,conjecture,((mvalid @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mand @ (mbox_s4 @ (mimplies @ (mbox_s4 @ p) @ (mbox_s4 @ (big_f @ A)))) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (big_f @ A)) @ (mbox_s4 @ p))))))) @ (mand @ (mbox_s4 @ (mimplies @ (mbox_s4 @ p) @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (big_f @ A))))))) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (big_f @ A))))) @ (mbox_s4 @ p)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',pel22)).
% 82.65/26.09 thf(2,negated_conjecture,((~ (mvalid @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mand @ (mbox_s4 @ (mimplies @ (mbox_s4 @ p) @ (mbox_s4 @ (big_f @ A)))) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (big_f @ A)) @ (mbox_s4 @ p))))))) @ (mand @ (mbox_s4 @ (mimplies @ (mbox_s4 @ p) @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (big_f @ A))))))) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (big_f @ A))))) @ (mbox_s4 @ p))))))))),inference(neg_conjecture,[status(cth)],[1])).
% 82.65/26.09 thf(7,plain,((~ (! [A:$i,B:$i]: (~ (rel_s4 @ A @ B) | ~ (! [C:$i]: (~ (rel_s4 @ B @ C) | ! [D:mu]: ((exists_in_world @ D @ C) => (~ (~ (! [E:$i]: (~ (rel_s4 @ C @ E) | ~ (! [F:$i]: (~ (rel_s4 @ E @ F) | (p @ F))) | ! [F:$i]: (~ (rel_s4 @ E @ F) | (big_f @ D @ F)))) | ~ (! [E:$i]: (~ (rel_s4 @ C @ E) | ~ (! [F:$i]: (~ (rel_s4 @ E @ F) | (big_f @ D @ F))) | ! [F:$i]: (~ (rel_s4 @ E @ F) | (p @ F))))))))) | ~ (~ (! [C:$i]: (~ (rel_s4 @ B @ C) | ~ (! [D:$i]: (~ (rel_s4 @ C @ D) | (p @ D))) | ! [D:$i]: (~ (rel_s4 @ C @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | (big_f @ E @ F))))))) | ~ (! [C:$i]: (~ (rel_s4 @ B @ C) | ~ (! [D:$i]: (~ (rel_s4 @ C @ D) | ! [E:mu]: ((exists_in_world @ E @ D) => (! [F:$i]: (~ (rel_s4 @ D @ F) | (big_f @ E @ F)))))) | ! [D:$i]: (~ (rel_s4 @ C @ D) | (p @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 82.65/26.09 thf(8,plain,(! [J:$i,I:mu,H:$i,G:$i,F:$i,E:$i,D:$i,C:$i,B:mu,A:$i] : (((rel_s4 @ sk1 @ sk2) & (~ (rel_s4 @ sk2 @ A) | ~ (exists_in_world @ B @ A) | ~ (rel_s4 @ A @ C) | (rel_s4 @ C @ (sk3 @ C @ B @ A)) | ~ (rel_s4 @ C @ D) | (big_f @ B @ D)) & (~ (rel_s4 @ sk2 @ A) | ~ (exists_in_world @ B @ A) | ~ (rel_s4 @ A @ C) | ~ (p @ (sk3 @ C @ B @ A)) | ~ (rel_s4 @ C @ D) | (big_f @ B @ D)) & (~ (rel_s4 @ sk2 @ A) | ~ (exists_in_world @ B @ A) | ~ (rel_s4 @ A @ E) | (rel_s4 @ E @ (sk4 @ E @ B @ A)) | ~ (rel_s4 @ E @ F) | (p @ F)) & (~ (rel_s4 @ sk2 @ A) | ~ (exists_in_world @ B @ A) | ~ (rel_s4 @ A @ E) | ~ (big_f @ B @ (sk4 @ E @ B @ A)) | ~ (rel_s4 @ E @ F) | (p @ F)) & ((rel_s4 @ sk2 @ sk6) | (sk5)) & (~ (rel_s4 @ sk6 @ G) | (p @ G) | (sk5)) & ((rel_s4 @ sk6 @ sk7) | (sk5)) & ((exists_in_world @ sk8 @ sk7) | (sk5)) & ((rel_s4 @ sk7 @ sk9) | (sk5)) & (~ (big_f @ sk8 @ sk9) | (sk5)) & (~ (sk5) | (rel_s4 @ sk2 @ sk10)) & (~ (sk5) | ~ (rel_s4 @ sk10 @ H) | ~ (exists_in_world @ I @ H) | ~ (rel_s4 @ H @ J) | (big_f @ I @ J)) & (~ (sk5) | (rel_s4 @ sk10 @ sk11)) & (~ (sk5) | ~ (p @ sk11))))),inference(cnf,[status(esa)],[7])).
% 82.65/26.09 thf(10,plain,((rel_s4 @ sk7 @ sk9) | sk5),inference(cnfConj,[status(thm)],[8])).
% 82.65/26.09 thf(15,plain,((rel_s4 @ sk6 @ sk7) | sk5),inference(cnfConj,[status(thm)],[8])).
% 82.65/26.09 thf(5,axiom,((mtransitive @ rel_s4)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2)).
% 82.65/26.09 thf(32,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])).
% 82.65/26.09 thf(33,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (rel_s4 @ A @ C))),inference(cnf,[status(esa)],[32])).
% 82.65/26.09 thf(449,plain,(! [C:$i,B:$i,A:$i] : (sk5 | (~ (rel_s4 @ A @ B)) | ~ (($true)) | (rel_s4 @ A @ C) | ((rel_s4 @ sk7 @ sk9) != (rel_s4 @ B @ C)))),inference(paramod_ordered,[status(thm)],[10,33])).
% 82.65/26.09 thf(450,plain,(! [C:$i,B:$i,A:$i] : (sk5 | (~ (rel_s4 @ A @ B)) | (rel_s4 @ A @ C) | ((rel_s4 @ sk7 @ sk9) != (rel_s4 @ B @ C)))),inference(simp,[status(thm)],[449])).
% 82.65/26.09 thf(451,plain,(! [A:$i] : (sk5 | (~ (rel_s4 @ A @ sk7)) | (rel_s4 @ A @ sk9))),inference(pattern_uni,[status(thm)],[450:[bind(A, $thf(A)),bind(B, $thf(sk7)),bind(C, $thf(sk9))]])).
% 82.65/26.09 thf(5043,plain,(! [A:$i] : (sk5 | sk5 | ~ (($true)) | (rel_s4 @ A @ sk9) | ((rel_s4 @ sk6 @ sk7) != (rel_s4 @ A @ sk7)))),inference(paramod_ordered,[status(thm)],[15,451])).
% 82.65/26.09 thf(5044,plain,(! [A:$i] : (sk5 | (rel_s4 @ A @ sk9) | ((rel_s4 @ sk6 @ sk7) != (rel_s4 @ A @ sk7)))),inference(simp,[status(thm)],[5043])).
% 82.65/26.09 thf(5045,plain,(sk5 | (rel_s4 @ sk6 @ sk9)),inference(pattern_uni,[status(thm)],[5044:[bind(A, $thf(sk6))]])).
% 82.65/26.09 thf(17,plain,((rel_s4 @ sk1 @ sk2)),inference(cnfConj,[status(thm)],[8])).
% 82.65/26.09 thf(467,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)],[17,33])).
% 82.65/26.09 thf(468,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)],[467])).
% 82.65/26.09 thf(469,plain,(! [A:$i] : ((~ (rel_s4 @ A @ sk1)) | (rel_s4 @ A @ sk2))),inference(pattern_uni,[status(thm)],[468:[bind(A, $thf(A)),bind(B, $thf(sk1)),bind(C, $thf(sk2))]])).
% 82.65/26.09 thf(20,plain,(~ (sk5) | (rel_s4 @ sk10 @ sk11)),inference(cnfConj,[status(thm)],[8])).
% 82.65/26.09 thf(576,plain,(! [A:$i] : (~ (sk5) | ~ (($true)) | (rel_s4 @ A @ sk2) | ((rel_s4 @ sk10 @ sk11) != (rel_s4 @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[20,469])).
% 82.65/26.09 thf(577,plain,(! [A:$i] : (~ (sk5) | (rel_s4 @ A @ sk2) | ((rel_s4 @ sk10 @ sk11) != (rel_s4 @ A @ sk1)))),inference(simp,[status(thm)],[576])).
% 82.65/26.09 thf(610,plain,(! [A:$i] : ((rel_s4 @ A @ sk2) | ~ (sk5) | (sk10 != A) | (sk11 != sk1))),inference(simp,[status(thm)],[577])).
% 82.65/26.09 thf(614,plain,((rel_s4 @ sk10 @ sk2) | ~ (sk5) | (sk11 != sk1)),inference(simp,[status(thm)],[610])).
% 82.65/26.09 thf(13,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (~ (p @ (sk3 @ C @ B @ A))) | (~ (rel_s4 @ C @ D)) | (big_f @ B @ D))),inference(cnfConj,[status(thm)],[8])).
% 82.65/26.09 thf(39,plain,(! [D:$i,C:$i,B:mu,A:$i] : (~ (($true)) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (~ (p @ (sk3 @ C @ B @ A))) | (~ (rel_s4 @ C @ D)) | (big_f @ B @ D) | ((rel_s4 @ sk2 @ A) != (rel_s4 @ sk1 @ sk2)))),inference(paramod_ordered,[status(thm)],[17,13])).
% 82.65/26.09 thf(40,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (~ (p @ (sk3 @ C @ B @ A))) | (~ (rel_s4 @ C @ D)) | (big_f @ B @ D) | ((rel_s4 @ sk2 @ A) != (rel_s4 @ sk1 @ sk2)))),inference(simp,[status(thm)],[39])).
% 82.65/26.09 thf(62,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((big_f @ B @ D) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (~ (p @ (sk3 @ C @ B @ A))) | (~ (rel_s4 @ C @ D)) | (sk2 != sk1) | (A != sk2))),inference(simp,[status(thm)],[40])).
% 82.65/26.09 thf(70,plain,(! [C:$i,B:$i,A:mu] : ((big_f @ A @ C) | (~ (exists_in_world @ A @ sk2)) | (~ (rel_s4 @ sk2 @ B)) | (~ (p @ (sk3 @ B @ A @ sk2))) | (~ (rel_s4 @ B @ C)) | (sk2 != sk1))),inference(simp,[status(thm)],[62])).
% 82.65/26.09 thf(153,plain,(! [C:$i,B:$i,A:mu] : (~ (sk5) | (big_f @ A @ C) | (~ (exists_in_world @ A @ sk2)) | ~ (($true)) | (~ (p @ (sk3 @ B @ A @ sk2))) | (~ (rel_s4 @ B @ C)) | (sk2 != sk1) | ((rel_s4 @ sk10 @ sk11) != (rel_s4 @ sk2 @ B)))),inference(paramod_ordered,[status(thm)],[20,70])).
% 82.65/26.09 thf(154,plain,(! [C:$i,B:$i,A:mu] : (~ (sk5) | (big_f @ A @ C) | (~ (exists_in_world @ A @ sk2)) | (~ (p @ (sk3 @ B @ A @ sk2))) | (~ (rel_s4 @ B @ C)) | (sk2 != sk1) | ((rel_s4 @ sk10 @ sk11) != (rel_s4 @ sk2 @ B)))),inference(simp,[status(thm)],[153])).
% 82.65/26.09 thf(167,plain,(! [C:$i,B:$i,A:mu] : ((big_f @ A @ C) | ~ (sk5) | (~ (exists_in_world @ A @ sk2)) | (~ (p @ (sk3 @ B @ A @ sk2))) | (~ (rel_s4 @ B @ C)) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != B))),inference(simp,[status(thm)],[154])).
% 82.65/26.09 thf(170,plain,(! [B:$i,A:mu] : ((big_f @ A @ B) | ~ (sk5) | (~ (exists_in_world @ A @ sk2)) | (~ (p @ (sk3 @ sk11 @ A @ sk2))) | (~ (rel_s4 @ sk11 @ B)) | (sk2 != sk1) | (sk10 != sk2))),inference(simp,[status(thm)],[167])).
% 82.65/26.09 thf(443,plain,(! [E:$i,D:mu,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (big_f @ D @ E) | ~ (sk5) | (~ (exists_in_world @ D @ sk2)) | (~ (p @ (sk3 @ sk11 @ D @ sk2))) | ~ (($true)) | (sk2 != sk1) | (sk10 != sk2) | ((rel_s4 @ A @ C) != (rel_s4 @ sk11 @ E)))),inference(paramod_ordered,[status(thm)],[33,170])).
% 82.65/26.09 thf(444,plain,(! [E:$i,D:mu,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (big_f @ D @ E) | ~ (sk5) | (~ (exists_in_world @ D @ sk2)) | (~ (p @ (sk3 @ sk11 @ D @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | ((rel_s4 @ A @ C) != (rel_s4 @ sk11 @ E)))),inference(simp,[status(thm)],[443])).
% 82.65/26.09 thf(445,plain,(! [C:mu,B:$i,A:$i] : ((~ (rel_s4 @ sk11 @ A)) | (~ (rel_s4 @ A @ B)) | (big_f @ C @ B) | ~ (sk5) | (~ (exists_in_world @ C @ sk2)) | (~ (p @ (sk3 @ sk11 @ C @ sk2))) | (sk2 != sk1) | (sk10 != sk2))),inference(pattern_uni,[status(thm)],[444:[bind(A, $thf(sk11)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf(C))]])).
% 82.65/26.09 thf(544,plain,(! [C:mu,B:$i,A:$i] : ((~ (rel_s4 @ sk11 @ A)) | (~ (rel_s4 @ A @ B)) | (big_f @ C @ B) | ~ (sk5) | (~ (exists_in_world @ C @ sk2)) | (~ (p @ (sk3 @ sk11 @ C @ sk2))) | (sk2 != sk1) | (sk10 != sk2))),inference(simp,[status(thm)],[445])).
% 82.65/26.09 thf(685,plain,(! [F:mu,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | ~ (($true)) | (~ (rel_s4 @ D @ E)) | (big_f @ F @ E) | ~ (sk5) | (~ (exists_in_world @ F @ sk2)) | (~ (p @ (sk3 @ sk11 @ F @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | ((rel_s4 @ A @ C) != (rel_s4 @ sk11 @ D)))),inference(paramod_ordered,[status(thm)],[33,544])).
% 82.65/26.09 thf(686,plain,(! [F:mu,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ D @ E)) | (big_f @ F @ E) | ~ (sk5) | (~ (exists_in_world @ F @ sk2)) | (~ (p @ (sk3 @ sk11 @ F @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | ((rel_s4 @ A @ C) != (rel_s4 @ sk11 @ D)))),inference(simp,[status(thm)],[685])).
% 82.65/26.09 thf(687,plain,(! [D:mu,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ sk11 @ A)) | (~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (big_f @ D @ C) | ~ (sk5) | (~ (exists_in_world @ D @ sk2)) | (~ (p @ (sk3 @ sk11 @ D @ sk2))) | (sk2 != sk1) | (sk10 != sk2))),inference(pattern_uni,[status(thm)],[686:[bind(A, $thf(sk11)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(C))]])).
% 82.65/26.09 thf(708,plain,(! [D:mu,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ sk11 @ A)) | (~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (big_f @ D @ C) | ~ (sk5) | (~ (exists_in_world @ D @ sk2)) | (~ (p @ (sk3 @ sk11 @ D @ sk2))) | (sk2 != sk1) | (sk10 != sk2))),inference(simp,[status(thm)],[687])).
% 82.65/26.09 thf(791,plain,(! [G:mu,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | ~ (($true)) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ E @ F)) | (big_f @ G @ F) | ~ (sk5) | (~ (exists_in_world @ G @ sk2)) | (~ (p @ (sk3 @ sk11 @ G @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | ((rel_s4 @ A @ C) != (rel_s4 @ sk11 @ D)))),inference(paramod_ordered,[status(thm)],[33,708])).
% 82.65/26.09 thf(792,plain,(! [G:mu,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ E @ F)) | (big_f @ G @ F) | ~ (sk5) | (~ (exists_in_world @ G @ sk2)) | (~ (p @ (sk3 @ sk11 @ G @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | ((rel_s4 @ A @ C) != (rel_s4 @ sk11 @ D)))),inference(simp,[status(thm)],[791])).
% 82.65/26.09 thf(793,plain,(! [E:mu,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ sk11 @ A)) | (~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ C @ D)) | (big_f @ E @ D) | ~ (sk5) | (~ (exists_in_world @ E @ sk2)) | (~ (p @ (sk3 @ sk11 @ E @ sk2))) | (sk2 != sk1) | (sk10 != sk2))),inference(pattern_uni,[status(thm)],[792:[bind(A, $thf(sk11)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(C))]])).
% 82.65/26.09 thf(833,plain,(! [E:mu,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ sk11 @ A)) | (~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ C @ D)) | (big_f @ E @ D) | ~ (sk5) | (~ (exists_in_world @ E @ sk2)) | (~ (p @ (sk3 @ sk11 @ E @ sk2))) | (sk2 != sk1) | (sk10 != sk2))),inference(simp,[status(thm)],[793])).
% 82.65/26.09 thf(1249,plain,(! [H:mu,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | ~ (($true)) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ E @ F)) | (~ (rel_s4 @ F @ G)) | (big_f @ H @ G) | ~ (sk5) | (~ (exists_in_world @ H @ sk2)) | (~ (p @ (sk3 @ sk11 @ H @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | ((rel_s4 @ A @ C) != (rel_s4 @ sk11 @ D)))),inference(paramod_ordered,[status(thm)],[33,833])).
% 82.65/26.09 thf(1250,plain,(! [H:mu,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ E @ F)) | (~ (rel_s4 @ F @ G)) | (big_f @ H @ G) | ~ (sk5) | (~ (exists_in_world @ H @ sk2)) | (~ (p @ (sk3 @ sk11 @ H @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | ((rel_s4 @ A @ C) != (rel_s4 @ sk11 @ D)))),inference(simp,[status(thm)],[1249])).
% 82.65/26.09 thf(1251,plain,(! [F:mu,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ sk11 @ A)) | (~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ C @ D)) | (~ (rel_s4 @ D @ E)) | (big_f @ F @ E) | ~ (sk5) | (~ (exists_in_world @ F @ sk2)) | (~ (p @ (sk3 @ sk11 @ F @ sk2))) | (sk2 != sk1) | (sk10 != sk2))),inference(pattern_uni,[status(thm)],[1250:[bind(A, $thf(sk11)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(C))]])).
% 82.65/26.09 thf(1357,plain,(! [F:mu,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ sk11 @ A)) | (~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ C @ D)) | (~ (rel_s4 @ D @ E)) | (big_f @ F @ E) | ~ (sk5) | (~ (exists_in_world @ F @ sk2)) | (~ (p @ (sk3 @ sk11 @ F @ sk2))) | (sk2 != sk1) | (sk10 != sk2))),inference(simp,[status(thm)],[1251])).
% 82.65/26.09 thf(1707,plain,(! [F:mu,E:$i,D:$i,C:$i,B:$i,A:$i] : (~ (sk5) | (sk11 != sk1) | ~ (($true)) | (~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ C @ D)) | (~ (rel_s4 @ D @ E)) | (big_f @ F @ E) | ~ (sk5) | (~ (exists_in_world @ F @ sk2)) | (~ (p @ (sk3 @ sk11 @ F @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | ((rel_s4 @ sk11 @ A) != (rel_s4 @ sk10 @ sk2)))),inference(paramod_ordered,[status(thm)],[614,1357])).
% 82.65/26.09 thf(1708,plain,(! [F:mu,E:$i,D:$i,C:$i,B:$i,A:$i] : (~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ C @ D)) | (~ (rel_s4 @ D @ E)) | (big_f @ F @ E) | (~ (exists_in_world @ F @ sk2)) | (~ (p @ (sk3 @ sk11 @ F @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | ((rel_s4 @ sk11 @ A) != (rel_s4 @ sk10 @ sk2)))),inference(simp,[status(thm)],[1707])).
% 82.65/26.09 thf(1738,plain,(! [F:mu,E:$i,D:$i,C:$i,B:$i,A:$i] : ((big_f @ F @ E) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ C @ D)) | (~ (rel_s4 @ D @ E)) | (~ (exists_in_world @ F @ sk2)) | (~ (p @ (sk3 @ sk11 @ F @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (A != sk2))),inference(simp,[status(thm)],[1708])).
% 82.65/26.09 thf(1752,plain,(! [E:mu,D:$i,C:$i,B:$i,A:$i] : ((big_f @ E @ D) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ sk2 @ A)) | (~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ C @ D)) | (~ (exists_in_world @ E @ sk2)) | (~ (p @ (sk3 @ sk11 @ E @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10))),inference(simp,[status(thm)],[1738])).
% 82.65/26.09 thf(2373,plain,(! [H:mu,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (big_f @ H @ G) | ~ (sk5) | (sk11 != sk1) | ~ (($true)) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ E @ F)) | (~ (rel_s4 @ F @ G)) | (~ (exists_in_world @ H @ sk2)) | (~ (p @ (sk3 @ sk11 @ H @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | ((rel_s4 @ A @ C) != (rel_s4 @ sk2 @ D)))),inference(paramod_ordered,[status(thm)],[33,1752])).
% 82.65/26.09 thf(2374,plain,(! [H:mu,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (big_f @ H @ G) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ E @ F)) | (~ (rel_s4 @ F @ G)) | (~ (exists_in_world @ H @ sk2)) | (~ (p @ (sk3 @ sk11 @ H @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | ((rel_s4 @ A @ C) != (rel_s4 @ sk2 @ D)))),inference(simp,[status(thm)],[2373])).
% 82.65/26.09 thf(2375,plain,(! [F:mu,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (~ (rel_s4 @ A @ B)) | (big_f @ F @ E) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ C @ D)) | (~ (rel_s4 @ D @ E)) | (~ (exists_in_world @ F @ sk2)) | (~ (p @ (sk3 @ sk11 @ F @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10))),inference(pattern_uni,[status(thm)],[2374:[bind(A, $thf(sk2)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(C))]])).
% 82.65/26.09 thf(2501,plain,(! [F:mu,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (~ (rel_s4 @ A @ B)) | (big_f @ F @ E) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ C @ D)) | (~ (rel_s4 @ D @ E)) | (~ (exists_in_world @ F @ sk2)) | (~ (p @ (sk3 @ sk11 @ F @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10))),inference(simp,[status(thm)],[2375])).
% 82.65/26.09 thf(19,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (~ (big_f @ B @ (sk4 @ C @ B @ A))) | (~ (rel_s4 @ C @ D)) | (p @ D))),inference(cnfConj,[status(thm)],[8])).
% 82.65/26.09 thf(27,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (~ (big_f @ B @ (sk4 @ C @ B @ A))) | (~ (rel_s4 @ C @ D)) | (p @ D))),inference(simp,[status(thm)],[19])).
% 82.65/26.09 thf(3362,plain,(! [J:$i,I:$i,H:mu,G:$i,F:mu,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (~ (rel_s4 @ A @ B)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ C @ D)) | (~ (rel_s4 @ D @ E)) | (~ (exists_in_world @ F @ sk2)) | (~ (p @ (sk3 @ sk11 @ F @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ G)) | (~ (exists_in_world @ H @ G)) | (~ (rel_s4 @ G @ I)) | ~ (($true)) | (~ (rel_s4 @ I @ J)) | (p @ J) | ((big_f @ F @ E) != (big_f @ H @ (sk4 @ I @ H @ G))))),inference(paramod_ordered,[status(thm)],[2501,27])).
% 82.65/26.09 thf(3363,plain,(! [J:$i,I:$i,H:mu,G:$i,F:mu,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (~ (rel_s4 @ A @ B)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ C @ D)) | (~ (rel_s4 @ D @ E)) | (~ (exists_in_world @ F @ sk2)) | (~ (p @ (sk3 @ sk11 @ F @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ G)) | (~ (exists_in_world @ H @ G)) | (~ (rel_s4 @ G @ I)) | (~ (rel_s4 @ I @ J)) | (p @ J) | ((big_f @ F @ E) != (big_f @ H @ (sk4 @ I @ H @ G))))),inference(simp,[status(thm)],[3362])).
% 82.65/26.09 thf(3364,plain,(! [H:$i,G:mu,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (~ (rel_s4 @ A @ B)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ C @ D)) | (~ (rel_s4 @ D @ (sk4 @ F @ G @ H))) | (~ (exists_in_world @ G @ sk2)) | (~ (p @ (sk3 @ sk11 @ G @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ H)) | (~ (exists_in_world @ G @ H)) | (~ (rel_s4 @ H @ F)) | (~ (rel_s4 @ F @ E)) | (p @ E))),inference(pattern_uni,[status(thm)],[3363:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf(sk4 @ K @ L @ M)),bind(F, $thf(L)),bind(G, $thf(M)),bind(H, $thf(L)),bind(I, $thf(K))]])).
% 82.65/26.09 thf(3533,plain,(! [H:$i,G:mu,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (~ (rel_s4 @ A @ B)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ C @ D)) | (~ (rel_s4 @ D @ (sk4 @ F @ G @ H))) | (~ (exists_in_world @ G @ sk2)) | (~ (p @ (sk3 @ sk11 @ G @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ H)) | (~ (exists_in_world @ G @ H)) | (~ (rel_s4 @ H @ F)) | (~ (rel_s4 @ F @ E)) | (p @ E))),inference(simp,[status(thm)],[3364])).
% 82.65/26.09 thf(4005,plain,(! [I:$i,H:mu,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ sk1)) | (~ (rel_s4 @ sk2 @ B)) | (~ (rel_s4 @ B @ C)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ C @ D)) | (~ (rel_s4 @ D @ E)) | ~ (($true)) | (~ (exists_in_world @ H @ sk2)) | (~ (p @ (sk3 @ sk11 @ H @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ I)) | (~ (exists_in_world @ H @ I)) | (~ (rel_s4 @ I @ G)) | (~ (rel_s4 @ G @ F)) | (p @ F) | ((rel_s4 @ A @ sk2) != (rel_s4 @ E @ (sk4 @ G @ H @ I))))),inference(paramod_ordered,[status(thm)],[469,3533])).
% 82.65/26.09 thf(4006,plain,(! [I:$i,H:mu,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ sk1)) | (~ (rel_s4 @ sk2 @ B)) | (~ (rel_s4 @ B @ C)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ C @ D)) | (~ (rel_s4 @ D @ E)) | (~ (exists_in_world @ H @ sk2)) | (~ (p @ (sk3 @ sk11 @ H @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ I)) | (~ (exists_in_world @ H @ I)) | (~ (rel_s4 @ I @ G)) | (~ (rel_s4 @ G @ F)) | (p @ F) | ((rel_s4 @ A @ sk2) != (rel_s4 @ E @ (sk4 @ G @ H @ I))))),inference(simp,[status(thm)],[4005])).
% 82.65/26.09 thf(4081,plain,(! [I:$i,H:mu,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((p @ F) | (~ (rel_s4 @ A @ sk1)) | (~ (rel_s4 @ sk2 @ B)) | (~ (rel_s4 @ B @ C)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ C @ D)) | (~ (rel_s4 @ D @ E)) | (~ (exists_in_world @ H @ sk2)) | (~ (p @ (sk3 @ sk11 @ H @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ I)) | (~ (exists_in_world @ H @ I)) | (~ (rel_s4 @ I @ G)) | (~ (rel_s4 @ G @ F)) | (A != E) | ((sk4 @ G @ H @ I) != sk2))),inference(simp,[status(thm)],[4006])).
% 82.65/26.09 thf(4193,plain,(! [H:$i,G:mu,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((p @ E) | (~ (rel_s4 @ D @ sk1)) | (~ (rel_s4 @ sk2 @ A)) | (~ (rel_s4 @ A @ B)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ C @ D)) | (~ (exists_in_world @ G @ sk2)) | (~ (p @ (sk3 @ sk11 @ G @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ H)) | (~ (exists_in_world @ G @ H)) | (~ (rel_s4 @ H @ F)) | (~ (rel_s4 @ F @ E)) | ((sk4 @ F @ G @ H) != sk2))),inference(simp,[status(thm)],[4081])).
% 82.65/26.09 thf(4398,plain,(! [K:$i,J:mu,I:$i,H:$i,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (p @ H) | ~ (($true)) | (~ (rel_s4 @ sk2 @ D)) | (~ (rel_s4 @ D @ E)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ E @ F)) | (~ (rel_s4 @ F @ G)) | (~ (exists_in_world @ J @ sk2)) | (~ (p @ (sk3 @ sk11 @ J @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ K)) | (~ (exists_in_world @ J @ K)) | (~ (rel_s4 @ K @ I)) | (~ (rel_s4 @ I @ H)) | ((sk4 @ I @ J @ K) != sk2) | ((rel_s4 @ A @ C) != (rel_s4 @ G @ sk1)))),inference(paramod_ordered,[status(thm)],[33,4193])).
% 82.65/26.09 thf(4399,plain,(! [K:$i,J:mu,I:$i,H:$i,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (p @ H) | (~ (rel_s4 @ sk2 @ D)) | (~ (rel_s4 @ D @ E)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ E @ F)) | (~ (rel_s4 @ F @ G)) | (~ (exists_in_world @ J @ sk2)) | (~ (p @ (sk3 @ sk11 @ J @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ K)) | (~ (exists_in_world @ J @ K)) | (~ (rel_s4 @ K @ I)) | (~ (rel_s4 @ I @ H)) | ((sk4 @ I @ J @ K) != sk2) | ((rel_s4 @ A @ C) != (rel_s4 @ G @ sk1)))),inference(simp,[status(thm)],[4398])).
% 82.65/26.09 thf(4400,plain,(! [I:$i,H:mu,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ sk1)) | (p @ F) | (~ (rel_s4 @ sk2 @ C)) | (~ (rel_s4 @ C @ D)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ E @ A)) | (~ (exists_in_world @ H @ sk2)) | (~ (p @ (sk3 @ sk11 @ H @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ I)) | (~ (exists_in_world @ H @ I)) | (~ (rel_s4 @ I @ G)) | (~ (rel_s4 @ G @ F)) | ((sk4 @ G @ H @ I) != sk2))),inference(pattern_uni,[status(thm)],[4399:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(sk1)),bind(D, $thf(D)),bind(E, $thf(E)),bind(F, $thf(F)),bind(G, $thf(A))]])).
% 82.65/26.09 thf(4732,plain,(! [I:$i,H:mu,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ sk1)) | (p @ F) | (~ (rel_s4 @ sk2 @ C)) | (~ (rel_s4 @ C @ D)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ E @ A)) | (~ (exists_in_world @ H @ sk2)) | (~ (p @ (sk3 @ sk11 @ H @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ I)) | (~ (exists_in_world @ H @ I)) | (~ (rel_s4 @ I @ G)) | (~ (rel_s4 @ G @ F)) | ((sk4 @ G @ H @ I) != sk2))),inference(simp,[status(thm)],[4400])).
% 82.65/26.09 thf(464,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)],[17,33])).
% 82.65/26.09 thf(465,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)],[464])).
% 82.65/26.09 thf(466,plain,(! [A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (rel_s4 @ sk1 @ A))),inference(pattern_uni,[status(thm)],[465:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 82.65/26.09 thf(537,plain,(! [A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (rel_s4 @ sk1 @ A))),inference(simp,[status(thm)],[466])).
% 82.65/26.09 thf(4,axiom,((mreflexive @ rel_s4)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1)).
% 82.65/26.09 thf(30,plain,((! [A:$i]: (rel_s4 @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 82.65/26.09 thf(31,plain,(! [A:$i] : ((rel_s4 @ A @ A))),inference(cnf,[status(esa)],[30])).
% 82.65/26.09 thf(12,plain,(! [A:$i] : ((~ (rel_s4 @ sk6 @ A)) | (p @ A) | sk5)),inference(cnfConj,[status(thm)],[8])).
% 82.65/26.09 thf(25,plain,(! [A:$i] : ((~ (rel_s4 @ sk6 @ A)) | (p @ A) | sk5)),inference(simp,[status(thm)],[12])).
% 82.65/26.09 thf(203,plain,(! [B:$i,A:$i] : (~ (($true)) | (p @ B) | sk5 | ((rel_s4 @ A @ A) != (rel_s4 @ sk6 @ B)))),inference(paramod_ordered,[status(thm)],[31,25])).
% 82.65/26.09 thf(204,plain,(! [B:$i,A:$i] : ((p @ B) | sk5 | ((rel_s4 @ A @ A) != (rel_s4 @ sk6 @ B)))),inference(simp,[status(thm)],[203])).
% 82.65/26.09 thf(205,plain,((p @ sk6) | sk5),inference(pattern_uni,[status(thm)],[204:[bind(A, $thf(sk6)),bind(B, $thf(sk6))]])).
% 82.65/26.09 thf(23,plain,((rel_s4 @ sk2 @ sk6) | sk5),inference(cnfConj,[status(thm)],[8])).
% 82.65/26.09 thf(993,plain,(! [A:$i] : (sk5 | ~ (($true)) | (rel_s4 @ sk1 @ A) | ((rel_s4 @ sk2 @ sk6) != (rel_s4 @ sk2 @ A)))),inference(paramod_ordered,[status(thm)],[23,537])).
% 82.65/26.09 thf(994,plain,(! [A:$i] : (sk5 | (rel_s4 @ sk1 @ A) | ((rel_s4 @ sk2 @ sk6) != (rel_s4 @ sk2 @ A)))),inference(simp,[status(thm)],[993])).
% 82.65/26.09 thf(995,plain,(sk5 | (rel_s4 @ sk1 @ sk6)),inference(pattern_uni,[status(thm)],[994:[bind(A, $thf(sk6))]])).
% 82.65/26.09 thf(4997,plain,(! [A:$i] : (sk5 | sk5 | ~ (($true)) | (rel_s4 @ A @ sk9) | ((rel_s4 @ sk1 @ sk6) != (rel_s4 @ A @ sk7)))),inference(paramod_ordered,[status(thm)],[995,451])).
% 82.65/26.09 thf(4998,plain,(! [A:$i] : (sk5 | (rel_s4 @ A @ sk9) | ((rel_s4 @ sk1 @ sk6) != (rel_s4 @ A @ sk7)))),inference(simp,[status(thm)],[4997])).
% 82.65/26.09 thf(5068,plain,(! [A:$i] : (sk5 | (rel_s4 @ A @ sk9) | (sk1 != A) | (sk7 != sk6))),inference(simp,[status(thm)],[4998])).
% 82.65/26.09 thf(5082,plain,(sk5 | (rel_s4 @ sk1 @ sk9) | (sk7 != sk6)),inference(simp,[status(thm)],[5068])).
% 82.65/26.09 thf(237,plain,(! [B:$i,A:mu] : (~ (sk5) | (big_f @ A @ B) | ~ (sk5) | (~ (exists_in_world @ A @ sk2)) | (~ (p @ (sk3 @ sk11 @ A @ sk2))) | ~ (($true)) | (sk2 != sk1) | (sk10 != sk2) | ((rel_s4 @ sk11 @ B) != (rel_s4 @ sk10 @ sk11)))),inference(paramod_ordered,[status(thm)],[20,170])).
% 82.65/26.09 thf(238,plain,(! [B:$i,A:mu] : (~ (sk5) | (big_f @ A @ B) | (~ (exists_in_world @ A @ sk2)) | (~ (p @ (sk3 @ sk11 @ A @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | ((rel_s4 @ sk11 @ B) != (rel_s4 @ sk10 @ sk11)))),inference(simp,[status(thm)],[237])).
% 82.65/26.09 thf(242,plain,(! [B:$i,A:mu] : ((big_f @ A @ B) | ~ (sk5) | (~ (exists_in_world @ A @ sk2)) | (~ (p @ (sk3 @ sk11 @ A @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (B != sk11))),inference(simp,[status(thm)],[238])).
% 82.65/26.09 thf(246,plain,(! [A:mu] : ((big_f @ A @ sk11) | ~ (sk5) | (~ (exists_in_world @ A @ sk2)) | (~ (p @ (sk3 @ sk11 @ A @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10))),inference(simp,[status(thm)],[242])).
% 82.65/26.09 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)).
% 82.65/26.09 thf(34,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])).
% 82.65/26.09 thf(35,plain,(! [C:$i,B:$i,A:mu] : ((~ (exists_in_world @ A @ B)) | (~ (rel_s4 @ B @ C)) | (exists_in_world @ A @ C))),inference(cnf,[status(esa)],[34])).
% 82.65/26.09 thf(5327,plain,(! [C:$i,B:$i,A:mu] : ((~ (exists_in_world @ A @ B)) | ~ (($true)) | (exists_in_world @ A @ C) | ((rel_s4 @ sk1 @ sk2) != (rel_s4 @ B @ C)))),inference(paramod_ordered,[status(thm)],[17,35])).
% 82.65/26.09 thf(5328,plain,(! [C:$i,B:$i,A:mu] : ((~ (exists_in_world @ A @ B)) | (exists_in_world @ A @ C) | ((rel_s4 @ sk1 @ sk2) != (rel_s4 @ B @ C)))),inference(simp,[status(thm)],[5327])).
% 82.65/26.09 thf(5329,plain,(! [A:mu] : ((~ (exists_in_world @ A @ sk1)) | (exists_in_world @ A @ sk2))),inference(pattern_uni,[status(thm)],[5328:[bind(A, $thf(A)),bind(B, $thf(sk1)),bind(C, $thf(sk2))]])).
% 82.65/26.09 thf(3,axiom,((! [A:$i]: ? [B:mu]: (exists_in_world @ B @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',nonempty_ax)).
% 82.65/26.09 thf(28,plain,((! [A:$i]: ? [B:mu]: (exists_in_world @ B @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 82.65/26.09 thf(29,plain,(! [A:$i] : ((exists_in_world @ (sk12 @ A) @ A))),inference(cnf,[status(esa)],[28])).
% 82.65/26.09 thf(5363,plain,(! [D:$i,C:$i,B:mu,A:$i] : (~ (($true)) | (~ (rel_s4 @ C @ D)) | (exists_in_world @ B @ D) | ((exists_in_world @ (sk12 @ A) @ A) != (exists_in_world @ B @ C)))),inference(paramod_ordered,[status(thm)],[29,35])).
% 82.65/26.09 thf(5364,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (rel_s4 @ C @ D)) | (exists_in_world @ B @ D) | ((exists_in_world @ (sk12 @ A) @ A) != (exists_in_world @ B @ C)))),inference(simp,[status(thm)],[5363])).
% 82.65/26.09 thf(5365,plain,(! [B:$i,A:$i] : ((~ (rel_s4 @ B @ A)) | (exists_in_world @ (sk12 @ B) @ A))),inference(pattern_uni,[status(thm)],[5364:[bind(A, $thf(E)),bind(B, $thf(sk12 @ E)),bind(C, $thf(E))]])).
% 82.65/26.09 thf(5453,plain,(! [B:$i,A:$i] : ((~ (rel_s4 @ B @ A)) | (exists_in_world @ (sk12 @ B) @ A))),inference(simp,[status(thm)],[5365])).
% 82.65/26.09 thf(7796,plain,(! [B:$i,A:$i] : (~ (sk5) | ~ (($true)) | (exists_in_world @ (sk12 @ B) @ A) | ((rel_s4 @ sk10 @ sk11) != (rel_s4 @ B @ A)))),inference(paramod_ordered,[status(thm)],[20,5453])).
% 82.65/26.09 thf(7797,plain,(! [B:$i,A:$i] : (~ (sk5) | (exists_in_world @ (sk12 @ B) @ A) | ((rel_s4 @ sk10 @ sk11) != (rel_s4 @ B @ A)))),inference(simp,[status(thm)],[7796])).
% 82.65/26.09 thf(7798,plain,(~ (sk5) | (exists_in_world @ (sk12 @ sk10) @ sk11)),inference(pattern_uni,[status(thm)],[7797:[bind(A, $thf(sk11)),bind(B, $thf(sk10))]])).
% 82.65/26.09 thf(5847,plain,(! [L:$i,K:mu,J:$i,I:$i,H:$i,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:mu] : ((~ (exists_in_world @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ E @ sk1)) | (p @ I) | (~ (rel_s4 @ sk2 @ F)) | (~ (rel_s4 @ F @ G)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ G @ H)) | (~ (rel_s4 @ H @ D)) | (~ (exists_in_world @ K @ sk2)) | (~ (p @ (sk3 @ sk11 @ K @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ L)) | ~ (($true)) | (~ (rel_s4 @ L @ J)) | (~ (rel_s4 @ J @ I)) | ((sk4 @ J @ K @ L) != sk2) | ((exists_in_world @ A @ C) != (exists_in_world @ K @ L)))),inference(paramod_ordered,[status(thm)],[35,4732])).
% 82.65/26.09 thf(5848,plain,(! [L:$i,K:mu,J:$i,I:$i,H:$i,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:mu] : ((~ (exists_in_world @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ E @ sk1)) | (p @ I) | (~ (rel_s4 @ sk2 @ F)) | (~ (rel_s4 @ F @ G)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ G @ H)) | (~ (rel_s4 @ H @ D)) | (~ (exists_in_world @ K @ sk2)) | (~ (p @ (sk3 @ sk11 @ K @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ L)) | (~ (rel_s4 @ L @ J)) | (~ (rel_s4 @ J @ I)) | ((sk4 @ J @ K @ L) != sk2) | ((exists_in_world @ A @ C) != (exists_in_world @ K @ L)))),inference(simp,[status(thm)],[5847])).
% 82.65/26.09 thf(5849,plain,(! [J:$i,I:$i,H:$i,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:mu] : ((~ (exists_in_world @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ E @ sk1)) | (p @ I) | (~ (rel_s4 @ sk2 @ F)) | (~ (rel_s4 @ F @ G)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ G @ H)) | (~ (rel_s4 @ H @ D)) | (~ (exists_in_world @ A @ sk2)) | (~ (p @ (sk3 @ sk11 @ A @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ C)) | (~ (rel_s4 @ C @ J)) | (~ (rel_s4 @ J @ I)) | ((sk4 @ J @ A @ C) != sk2))),inference(pattern_uni,[status(thm)],[5848:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf(E)),bind(F, $thf(F)),bind(G, $thf(G)),bind(H, $thf(H)),bind(I, $thf(I)),bind(J, $thf(J)),bind(K, $thf(A)),bind(L, $thf(C))]])).
% 82.65/26.09 thf(6803,plain,(! [M:$i,L:$i,K:$i,J:$i,I:$i,H:$i,G:$i,F:$i,E:$i,D:mu,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (exists_in_world @ D @ E)) | (~ (rel_s4 @ E @ F)) | (~ (rel_s4 @ G @ H)) | (~ (rel_s4 @ H @ sk1)) | (p @ L) | (~ (rel_s4 @ sk2 @ I)) | (~ (rel_s4 @ I @ J)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ J @ K)) | (~ (rel_s4 @ K @ G)) | (~ (exists_in_world @ D @ sk2)) | (~ (p @ (sk3 @ sk11 @ D @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ F)) | (~ (rel_s4 @ F @ M)) | ~ (($true)) | ((sk4 @ M @ D @ F) != sk2) | ((rel_s4 @ A @ C) != (rel_s4 @ M @ L)))),inference(paramod_ordered,[status(thm)],[33,5849])).
% 82.65/26.09 thf(6804,plain,(! [M:$i,L:$i,K:$i,J:$i,I:$i,H:$i,G:$i,F:$i,E:$i,D:mu,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (exists_in_world @ D @ E)) | (~ (rel_s4 @ E @ F)) | (~ (rel_s4 @ G @ H)) | (~ (rel_s4 @ H @ sk1)) | (p @ L) | (~ (rel_s4 @ sk2 @ I)) | (~ (rel_s4 @ I @ J)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ J @ K)) | (~ (rel_s4 @ K @ G)) | (~ (exists_in_world @ D @ sk2)) | (~ (p @ (sk3 @ sk11 @ D @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ F)) | (~ (rel_s4 @ F @ M)) | ((sk4 @ M @ D @ F) != sk2) | ((rel_s4 @ A @ C) != (rel_s4 @ M @ L)))),inference(simp,[status(thm)],[6803])).
% 82.65/26.09 thf(6805,plain,(! [K:$i,J:$i,I:$i,H:$i,G:$i,F:$i,E:$i,D:mu,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (exists_in_world @ D @ E)) | (~ (rel_s4 @ E @ F)) | (~ (rel_s4 @ G @ H)) | (~ (rel_s4 @ H @ sk1)) | (p @ C) | (~ (rel_s4 @ sk2 @ I)) | (~ (rel_s4 @ I @ J)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ J @ K)) | (~ (rel_s4 @ K @ G)) | (~ (exists_in_world @ D @ sk2)) | (~ (p @ (sk3 @ sk11 @ D @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ F)) | (~ (rel_s4 @ F @ A)) | ((sk4 @ A @ D @ F) != sk2))),inference(pattern_uni,[status(thm)],[6804:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf(E)),bind(F, $thf(F)),bind(G, $thf(G)),bind(H, $thf(H)),bind(I, $thf(I)),bind(J, $thf(J)),bind(K, $thf(K)),bind(L, $thf(C)),bind(M, $thf(A))]])).
% 82.65/26.09 thf(8198,plain,(! [N:$i,M:$i,L:$i,K:$i,J:$i,I:$i,H:$i,G:mu,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ E @ F)) | (~ (exists_in_world @ G @ H)) | (~ (rel_s4 @ H @ I)) | (~ (rel_s4 @ J @ K)) | (~ (rel_s4 @ K @ sk1)) | (p @ F) | (~ (rel_s4 @ sk2 @ L)) | (~ (rel_s4 @ L @ M)) | ~ (sk5) | (sk11 != sk1) | ~ (($true)) | (~ (rel_s4 @ N @ J)) | (~ (exists_in_world @ G @ sk2)) | (~ (p @ (sk3 @ sk11 @ G @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ I)) | (~ (rel_s4 @ I @ D)) | ((sk4 @ D @ G @ I) != sk2) | ((rel_s4 @ A @ C) != (rel_s4 @ M @ N)))),inference(paramod_ordered,[status(thm)],[33,6805])).
% 82.65/26.09 thf(8199,plain,(! [N:$i,M:$i,L:$i,K:$i,J:$i,I:$i,H:$i,G:mu,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ E @ F)) | (~ (exists_in_world @ G @ H)) | (~ (rel_s4 @ H @ I)) | (~ (rel_s4 @ J @ K)) | (~ (rel_s4 @ K @ sk1)) | (p @ F) | (~ (rel_s4 @ sk2 @ L)) | (~ (rel_s4 @ L @ M)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ N @ J)) | (~ (exists_in_world @ G @ sk2)) | (~ (p @ (sk3 @ sk11 @ G @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ I)) | (~ (rel_s4 @ I @ D)) | ((sk4 @ D @ G @ I) != sk2) | ((rel_s4 @ A @ C) != (rel_s4 @ M @ N)))),inference(simp,[status(thm)],[8198])).
% 82.65/26.09 thf(8200,plain,(! [L:$i,K:$i,J:$i,I:$i,H:$i,G:mu,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ E @ F)) | (~ (exists_in_world @ G @ H)) | (~ (rel_s4 @ H @ I)) | (~ (rel_s4 @ J @ K)) | (~ (rel_s4 @ K @ sk1)) | (p @ F) | (~ (rel_s4 @ sk2 @ L)) | (~ (rel_s4 @ L @ A)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ C @ J)) | (~ (exists_in_world @ G @ sk2)) | (~ (p @ (sk3 @ sk11 @ G @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ I)) | (~ (rel_s4 @ I @ D)) | ((sk4 @ D @ G @ I) != sk2))),inference(pattern_uni,[status(thm)],[8199:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf(E)),bind(F, $thf(F)),bind(G, $thf(G)),bind(H, $thf(H)),bind(I, $thf(I)),bind(J, $thf(J)),bind(K, $thf(K)),bind(L, $thf(L)),bind(M, $thf(A)),bind(N, $thf(C))]])).
% 82.65/26.09 thf(9,plain,(! [C:$i,B:mu,A:$i] : (~ (sk5) | (~ (rel_s4 @ sk10 @ A)) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (big_f @ B @ C))),inference(cnfConj,[status(thm)],[8])).
% 82.65/26.09 thf(24,plain,(! [C:$i,B:mu,A:$i] : (~ (sk5) | (~ (rel_s4 @ sk10 @ A)) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (big_f @ B @ C))),inference(simp,[status(thm)],[9])).
% 82.65/26.09 thf(14,plain,(~ (sk5) | (~ (p @ sk11))),inference(cnfConj,[status(thm)],[8])).
% 82.65/26.09 thf(7820,plain,(! [B:$i,A:$i] : (sk5 | ~ (($true)) | (exists_in_world @ (sk12 @ B) @ A) | ((rel_s4 @ sk2 @ sk6) != (rel_s4 @ B @ A)))),inference(paramod_ordered,[status(thm)],[23,5453])).
% 82.65/26.09 thf(7821,plain,(! [B:$i,A:$i] : (sk5 | (exists_in_world @ (sk12 @ B) @ A) | ((rel_s4 @ sk2 @ sk6) != (rel_s4 @ B @ A)))),inference(simp,[status(thm)],[7820])).
% 82.65/26.09 thf(7822,plain,(sk5 | (exists_in_world @ (sk12 @ sk2) @ sk6)),inference(pattern_uni,[status(thm)],[7821:[bind(A, $thf(sk6)),bind(B, $thf(sk2))]])).
% 82.65/26.09 thf(5125,plain,(! [A:$i] : (sk5 | ~ (($true)) | (p @ A) | sk5 | ((rel_s4 @ sk6 @ sk9) != (rel_s4 @ sk6 @ A)))),inference(paramod_ordered,[status(thm)],[5045,25])).
% 82.65/26.09 thf(5126,plain,(! [A:$i] : (sk5 | (p @ A) | ((rel_s4 @ sk6 @ sk9) != (rel_s4 @ sk6 @ A)))),inference(simp,[status(thm)],[5125])).
% 82.65/26.09 thf(5127,plain,(sk5 | (p @ sk9)),inference(pattern_uni,[status(thm)],[5126:[bind(A, $thf(sk9))]])).
% 82.65/26.09 thf(44,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (~ (p @ (sk3 @ C @ B @ A))) | ~ (($true)) | (big_f @ B @ D) | ((rel_s4 @ sk1 @ sk2) != (rel_s4 @ C @ D)))),inference(paramod_ordered,[status(thm)],[17,13])).
% 82.65/26.09 thf(45,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (~ (p @ (sk3 @ C @ B @ A))) | (big_f @ B @ D) | ((rel_s4 @ sk1 @ sk2) != (rel_s4 @ C @ D)))),inference(simp,[status(thm)],[44])).
% 82.65/26.09 thf(46,plain,(! [B:mu,A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ sk1)) | (~ (p @ (sk3 @ sk1 @ B @ A))) | (big_f @ B @ sk2))),inference(pattern_uni,[status(thm)],[45:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(sk1)),bind(D, $thf(sk2))]])).
% 82.65/26.09 thf(551,plain,(! [B:$i,A:$i] : ((~ (rel_s4 @ A @ sk1)) | ~ (($true)) | (p @ B) | sk5 | ((rel_s4 @ A @ sk2) != (rel_s4 @ sk6 @ B)))),inference(paramod_ordered,[status(thm)],[469,25])).
% 82.65/26.09 thf(552,plain,(! [B:$i,A:$i] : ((~ (rel_s4 @ A @ sk1)) | (p @ B) | sk5 | ((rel_s4 @ A @ sk2) != (rel_s4 @ sk6 @ B)))),inference(simp,[status(thm)],[551])).
% 82.65/26.09 thf(553,plain,((~ (rel_s4 @ sk6 @ sk1)) | (p @ sk2) | sk5),inference(pattern_uni,[status(thm)],[552:[bind(A, $thf(sk6)),bind(B, $thf(sk2))]])).
% 82.65/26.09 thf(860,plain,(sk5 | ~ (($true)) | (p @ sk2) | sk5 | ((rel_s4 @ sk6 @ sk7) != (rel_s4 @ sk6 @ sk1))),inference(paramod_ordered,[status(thm)],[15,553])).
% 82.65/26.09 thf(861,plain,(sk5 | (p @ sk2) | ((rel_s4 @ sk6 @ sk7) != (rel_s4 @ sk6 @ sk1))),inference(simp,[status(thm)],[860])).
% 82.65/26.09 thf(873,plain,(sk5 | (p @ sk2) | (sk6 != sk6) | (sk7 != sk1)),inference(simp,[status(thm)],[861])).
% 82.65/26.09 thf(881,plain,(sk5 | (p @ sk2) | (sk7 != sk1)),inference(simp,[status(thm)],[873])).
% 82.65/26.09 thf(549,plain,(! [A:$i] : (sk5 | ~ (($true)) | (rel_s4 @ A @ sk2) | ((rel_s4 @ sk7 @ sk9) != (rel_s4 @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[10,469])).
% 82.65/26.09 thf(550,plain,(! [A:$i] : (sk5 | (rel_s4 @ A @ sk2) | ((rel_s4 @ sk7 @ sk9) != (rel_s4 @ A @ sk1)))),inference(simp,[status(thm)],[549])).
% 82.65/26.09 thf(604,plain,(! [A:$i] : (sk5 | (rel_s4 @ A @ sk2) | (sk7 != A) | (sk9 != sk1))),inference(simp,[status(thm)],[550])).
% 82.65/26.09 thf(623,plain,(sk5 | (rel_s4 @ sk7 @ sk2) | (sk9 != sk1)),inference(simp,[status(thm)],[604])).
% 82.65/26.09 thf(18,plain,(~ (sk5) | (rel_s4 @ sk2 @ sk10)),inference(cnfConj,[status(thm)],[8])).
% 82.65/26.09 thf(7790,plain,(! [B:$i,A:$i] : (~ (sk5) | ~ (($true)) | (exists_in_world @ (sk12 @ B) @ A) | ((rel_s4 @ sk2 @ sk10) != (rel_s4 @ B @ A)))),inference(paramod_ordered,[status(thm)],[18,5453])).
% 82.65/26.09 thf(7791,plain,(! [B:$i,A:$i] : (~ (sk5) | (exists_in_world @ (sk12 @ B) @ A) | ((rel_s4 @ sk2 @ sk10) != (rel_s4 @ B @ A)))),inference(simp,[status(thm)],[7790])).
% 82.65/26.09 thf(7792,plain,(~ (sk5) | (exists_in_world @ (sk12 @ sk2) @ sk10)),inference(pattern_uni,[status(thm)],[7791:[bind(A, $thf(sk10)),bind(B, $thf(sk2))]])).
% 82.65/26.09 thf(7784,plain,(! [B:$i,A:$i] : (sk5 | ~ (($true)) | (exists_in_world @ (sk12 @ B) @ A) | ((rel_s4 @ sk6 @ sk9) != (rel_s4 @ B @ A)))),inference(paramod_ordered,[status(thm)],[5045,5453])).
% 82.65/26.09 thf(7785,plain,(! [B:$i,A:$i] : (sk5 | (exists_in_world @ (sk12 @ B) @ A) | ((rel_s4 @ sk6 @ sk9) != (rel_s4 @ B @ A)))),inference(simp,[status(thm)],[7784])).
% 82.65/26.09 thf(7786,plain,(sk5 | (exists_in_world @ (sk12 @ sk6) @ sk9)),inference(pattern_uni,[status(thm)],[7785:[bind(A, $thf(sk9)),bind(B, $thf(sk6))]])).
% 82.65/26.09 thf(7832,plain,(! [B:$i,A:$i] : (sk5 | ~ (($true)) | (exists_in_world @ (sk12 @ B) @ A) | ((rel_s4 @ sk6 @ sk7) != (rel_s4 @ B @ A)))),inference(paramod_ordered,[status(thm)],[15,5453])).
% 82.65/26.09 thf(7833,plain,(! [B:$i,A:$i] : (sk5 | (exists_in_world @ (sk12 @ B) @ A) | ((rel_s4 @ sk6 @ sk7) != (rel_s4 @ B @ A)))),inference(simp,[status(thm)],[7832])).
% 82.65/26.09 thf(7834,plain,(sk5 | (exists_in_world @ (sk12 @ sk6) @ sk7)),inference(pattern_uni,[status(thm)],[7833:[bind(A, $thf(sk7)),bind(B, $thf(sk6))]])).
% 82.65/26.09 thf(21,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (rel_s4 @ C @ (sk3 @ C @ B @ A)) | (~ (rel_s4 @ C @ D)) | (big_f @ B @ D))),inference(cnfConj,[status(thm)],[8])).
% 82.65/26.09 thf(5486,plain,(! [B:mu,A:$i] : (~ (($true)) | (exists_in_world @ B @ sk2) | ((exists_in_world @ (sk12 @ A) @ A) != (exists_in_world @ B @ sk1)))),inference(paramod_ordered,[status(thm)],[29,5329])).
% 82.65/26.09 thf(5487,plain,(! [B:mu,A:$i] : ((exists_in_world @ B @ sk2) | ((exists_in_world @ (sk12 @ A) @ A) != (exists_in_world @ B @ sk1)))),inference(simp,[status(thm)],[5486])).
% 82.65/26.09 thf(5488,plain,((exists_in_world @ (sk12 @ sk1) @ sk2)),inference(pattern_uni,[status(thm)],[5487:[bind(A, $thf(sk1)),bind(B, $thf(sk12 @ sk1))]])).
% 82.65/26.09 thf(5544,plain,(! [C:$i,B:$i,A:mu] : (~ (($true)) | (~ (rel_s4 @ B @ C)) | (exists_in_world @ A @ C) | ((exists_in_world @ (sk12 @ sk1) @ sk2) != (exists_in_world @ A @ B)))),inference(paramod_ordered,[status(thm)],[5488,35])).
% 82.65/26.09 thf(5545,plain,(! [C:$i,B:$i,A:mu] : ((~ (rel_s4 @ B @ C)) | (exists_in_world @ A @ C) | ((exists_in_world @ (sk12 @ sk1) @ sk2) != (exists_in_world @ A @ B)))),inference(simp,[status(thm)],[5544])).
% 82.65/26.09 thf(5546,plain,(! [A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (exists_in_world @ (sk12 @ sk1) @ A))),inference(pattern_uni,[status(thm)],[5545:[bind(A, $thf(sk12 @ sk1)),bind(B, $thf(sk2)),bind(C, $thf(C))]])).
% 82.65/26.09 thf(5601,plain,(! [A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (exists_in_world @ (sk12 @ sk1) @ A))),inference(simp,[status(thm)],[5546])).
% 82.65/26.09 thf(5624,plain,(! [A:$i] : (~ (sk5) | ~ (($true)) | (exists_in_world @ (sk12 @ sk1) @ A) | ((rel_s4 @ sk2 @ sk10) != (rel_s4 @ sk2 @ A)))),inference(paramod_ordered,[status(thm)],[18,5601])).
% 82.65/26.09 thf(5625,plain,(! [A:$i] : (~ (sk5) | (exists_in_world @ (sk12 @ sk1) @ A) | ((rel_s4 @ sk2 @ sk10) != (rel_s4 @ sk2 @ A)))),inference(simp,[status(thm)],[5624])).
% 82.65/26.09 thf(5626,plain,(~ (sk5) | (exists_in_world @ (sk12 @ sk1) @ sk10)),inference(pattern_uni,[status(thm)],[5625:[bind(A, $thf(sk10))]])).
% 82.65/26.09 thf(998,plain,(! [A:$i] : (~ (sk5) | ~ (($true)) | (rel_s4 @ sk1 @ A) | ((rel_s4 @ sk10 @ sk11) != (rel_s4 @ sk2 @ A)))),inference(paramod_ordered,[status(thm)],[20,537])).
% 82.65/26.09 thf(999,plain,(! [A:$i] : (~ (sk5) | (rel_s4 @ sk1 @ A) | ((rel_s4 @ sk10 @ sk11) != (rel_s4 @ sk2 @ A)))),inference(simp,[status(thm)],[998])).
% 82.65/26.09 thf(1013,plain,(! [A:$i] : ((rel_s4 @ sk1 @ A) | ~ (sk5) | (sk10 != sk2) | (sk11 != A))),inference(simp,[status(thm)],[999])).
% 82.65/26.09 thf(1017,plain,((rel_s4 @ sk1 @ sk11) | ~ (sk5) | (sk10 != sk2)),inference(simp,[status(thm)],[1013])).
% 82.65/26.09 thf(5251,plain,(! [A:$i] : (sk5 | ~ (($true)) | (rel_s4 @ A @ sk2) | ((rel_s4 @ sk6 @ sk9) != (rel_s4 @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[5045,469])).
% 82.65/26.09 thf(5252,plain,(! [A:$i] : (sk5 | (rel_s4 @ A @ sk2) | ((rel_s4 @ sk6 @ sk9) != (rel_s4 @ A @ sk1)))),inference(simp,[status(thm)],[5251])).
% 82.65/26.09 thf(5262,plain,(! [A:$i] : (sk5 | (rel_s4 @ A @ sk2) | (sk6 != A) | (sk9 != sk1))),inference(simp,[status(thm)],[5252])).
% 82.65/26.09 thf(5273,plain,(sk5 | (rel_s4 @ sk6 @ sk2) | (sk9 != sk1)),inference(simp,[status(thm)],[5262])).
% 82.65/26.09 thf(5645,plain,(! [A:$i] : (sk5 | ~ (($true)) | (exists_in_world @ (sk12 @ sk1) @ A) | ((rel_s4 @ sk2 @ sk6) != (rel_s4 @ sk2 @ A)))),inference(paramod_ordered,[status(thm)],[23,5601])).
% 82.65/26.09 thf(5646,plain,(! [A:$i] : (sk5 | (exists_in_world @ (sk12 @ sk1) @ A) | ((rel_s4 @ sk2 @ sk6) != (rel_s4 @ sk2 @ A)))),inference(simp,[status(thm)],[5645])).
% 82.65/26.09 thf(5647,plain,(sk5 | (exists_in_world @ (sk12 @ sk1) @ sk6)),inference(pattern_uni,[status(thm)],[5646:[bind(A, $thf(sk6))]])).
% 82.65/26.09 thf(22,plain,((~ (big_f @ sk8 @ sk9)) | sk5),inference(cnfConj,[status(thm)],[8])).
% 82.65/26.09 thf(996,plain,(! [A:$i] : (sk5 | ~ (($true)) | (rel_s4 @ sk1 @ A) | ((rel_s4 @ sk6 @ sk7) != (rel_s4 @ sk2 @ A)))),inference(paramod_ordered,[status(thm)],[15,537])).
% 82.65/26.09 thf(997,plain,(! [A:$i] : (sk5 | (rel_s4 @ sk1 @ A) | ((rel_s4 @ sk6 @ sk7) != (rel_s4 @ sk2 @ A)))),inference(simp,[status(thm)],[996])).
% 82.65/26.09 thf(1014,plain,(! [A:$i] : (sk5 | (rel_s4 @ sk1 @ A) | (sk6 != sk2) | (sk7 != A))),inference(simp,[status(thm)],[997])).
% 82.65/26.09 thf(1018,plain,(sk5 | (rel_s4 @ sk1 @ sk7) | (sk6 != sk2)),inference(simp,[status(thm)],[1014])).
% 82.65/26.09 thf(47,plain,(! [E:$i,D:$i,C:mu,B:$i,A:$i] : (~ (($true)) | (~ (exists_in_world @ C @ B)) | (~ (rel_s4 @ B @ D)) | (~ (p @ (sk3 @ D @ C @ B))) | (~ (rel_s4 @ D @ E)) | (big_f @ C @ E) | ((rel_s4 @ A @ A) != (rel_s4 @ sk2 @ B)))),inference(paramod_ordered,[status(thm)],[31,13])).
% 82.65/26.09 thf(48,plain,(! [E:$i,D:$i,C:mu,B:$i,A:$i] : ((~ (exists_in_world @ C @ B)) | (~ (rel_s4 @ B @ D)) | (~ (p @ (sk3 @ D @ C @ B))) | (~ (rel_s4 @ D @ E)) | (big_f @ C @ E) | ((rel_s4 @ A @ A) != (rel_s4 @ sk2 @ B)))),inference(simp,[status(thm)],[47])).
% 82.65/26.09 thf(49,plain,(! [C:$i,B:$i,A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (rel_s4 @ sk2 @ B)) | (~ (p @ (sk3 @ B @ A @ sk2))) | (~ (rel_s4 @ B @ C)) | (big_f @ A @ C))),inference(pattern_uni,[status(thm)],[48:[bind(A, $thf(sk2)),bind(B, $thf(sk2))]])).
% 82.65/26.09 thf(63,plain,(! [C:$i,B:$i,A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (rel_s4 @ sk2 @ B)) | (~ (p @ (sk3 @ B @ A @ sk2))) | (~ (rel_s4 @ B @ C)) | (big_f @ A @ C))),inference(simp,[status(thm)],[49])).
% 82.65/26.09 thf(4995,plain,(! [A:$i] : (sk5 | sk5 | ~ (($true)) | (rel_s4 @ A @ sk9) | ((rel_s4 @ sk2 @ sk6) != (rel_s4 @ A @ sk7)))),inference(paramod_ordered,[status(thm)],[23,451])).
% 82.65/26.09 thf(4996,plain,(! [A:$i] : (sk5 | (rel_s4 @ A @ sk9) | ((rel_s4 @ sk2 @ sk6) != (rel_s4 @ A @ sk7)))),inference(simp,[status(thm)],[4995])).
% 82.65/26.09 thf(5066,plain,(! [A:$i] : (sk5 | (rel_s4 @ A @ sk9) | (sk2 != A) | (sk7 != sk6))),inference(simp,[status(thm)],[4996])).
% 82.65/26.09 thf(5079,plain,(sk5 | (rel_s4 @ sk2 @ sk9) | (sk7 != sk6)),inference(simp,[status(thm)],[5066])).
% 82.65/26.09 thf(11,plain,((exists_in_world @ sk8 @ sk7) | sk5),inference(cnfConj,[status(thm)],[8])).
% 82.65/26.09 thf(199,plain,(! [A:$i] : (~ (($true)) | (p @ A) | sk5 | ((rel_s4 @ sk6 @ A) != (rel_s4 @ sk1 @ sk2)))),inference(paramod_ordered,[status(thm)],[17,25])).
% 82.65/26.09 thf(200,plain,(! [A:$i] : ((p @ A) | sk5 | ((rel_s4 @ sk6 @ A) != (rel_s4 @ sk1 @ sk2)))),inference(simp,[status(thm)],[199])).
% 82.65/26.09 thf(215,plain,(! [A:$i] : ((p @ A) | sk5 | (sk6 != sk1) | (A != sk2))),inference(simp,[status(thm)],[200])).
% 82.65/26.09 thf(218,plain,((p @ sk2) | sk5 | (sk6 != sk1)),inference(simp,[status(thm)],[215])).
% 82.65/26.09 thf(16,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (rel_s4 @ C @ (sk4 @ C @ B @ A)) | (~ (rel_s4 @ C @ D)) | (p @ D))),inference(cnfConj,[status(thm)],[8])).
% 82.65/26.09 thf(26,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (rel_s4 @ sk2 @ A)) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (rel_s4 @ C @ (sk4 @ C @ B @ A)) | (~ (rel_s4 @ C @ D)) | (p @ D))),inference(simp,[status(thm)],[16])).
% 82.65/26.09 thf(7838,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ sk1)) | ~ (($true)) | (exists_in_world @ (sk12 @ C) @ B) | ((rel_s4 @ A @ sk2) != (rel_s4 @ C @ B)))),inference(paramod_ordered,[status(thm)],[469,5453])).
% 82.65/26.09 thf(7839,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ sk1)) | (exists_in_world @ (sk12 @ C) @ B) | ((rel_s4 @ A @ sk2) != (rel_s4 @ C @ B)))),inference(simp,[status(thm)],[7838])).
% 82.65/26.09 thf(7840,plain,(! [A:$i] : ((~ (rel_s4 @ A @ sk1)) | (exists_in_world @ (sk12 @ A) @ sk2))),inference(pattern_uni,[status(thm)],[7839:[bind(A, $thf(A)),bind(B, $thf(sk2)),bind(C, $thf(A))]])).
% 82.65/26.09 thf(53,plain,(! [E:$i,D:$i,C:mu,B:$i,A:$i] : ((~ (rel_s4 @ sk2 @ B)) | (~ (exists_in_world @ C @ B)) | (~ (rel_s4 @ B @ D)) | (~ (p @ (sk3 @ D @ C @ B))) | ~ (($true)) | (big_f @ C @ E) | ((rel_s4 @ A @ A) != (rel_s4 @ D @ E)))),inference(paramod_ordered,[status(thm)],[31,13])).
% 82.65/26.09 thf(54,plain,(! [E:$i,D:$i,C:mu,B:$i,A:$i] : ((~ (rel_s4 @ sk2 @ B)) | (~ (exists_in_world @ C @ B)) | (~ (rel_s4 @ B @ D)) | (~ (p @ (sk3 @ D @ C @ B))) | (big_f @ C @ E) | ((rel_s4 @ A @ A) != (rel_s4 @ D @ E)))),inference(simp,[status(thm)],[53])).
% 82.65/26.09 thf(55,plain,(! [C:mu,B:$i,A:$i] : ((~ (rel_s4 @ sk2 @ B)) | (~ (exists_in_world @ C @ B)) | (~ (rel_s4 @ B @ A)) | (~ (p @ (sk3 @ A @ C @ B))) | (big_f @ C @ A))),inference(pattern_uni,[status(thm)],[54:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(A)),bind(E, $thf(A))]])).
% 82.65/26.09 thf(208,plain,(! [A:$i] : (sk5 | ~ (($true)) | (p @ A) | sk5 | ((rel_s4 @ sk6 @ sk7) != (rel_s4 @ sk6 @ A)))),inference(paramod_ordered,[status(thm)],[15,25])).
% 82.65/26.09 thf(209,plain,(! [A:$i] : (sk5 | (p @ A) | ((rel_s4 @ sk6 @ sk7) != (rel_s4 @ sk6 @ A)))),inference(simp,[status(thm)],[208])).
% 82.65/26.09 thf(210,plain,(sk5 | (p @ sk7)),inference(pattern_uni,[status(thm)],[209:[bind(A, $thf(sk7))]])).
% 82.65/26.09 thf(986,plain,(! [A:$i] : (sk5 | ~ (($true)) | (rel_s4 @ sk1 @ A) | ((rel_s4 @ sk7 @ sk9) != (rel_s4 @ sk2 @ A)))),inference(paramod_ordered,[status(thm)],[10,537])).
% 82.65/26.09 thf(987,plain,(! [A:$i] : (sk5 | (rel_s4 @ sk1 @ A) | ((rel_s4 @ sk7 @ sk9) != (rel_s4 @ sk2 @ A)))),inference(simp,[status(thm)],[986])).
% 82.65/26.09 thf(1015,plain,(! [A:$i] : (sk5 | (rel_s4 @ sk1 @ A) | (sk7 != sk2) | (sk9 != A))),inference(simp,[status(thm)],[987])).
% 82.65/26.09 thf(1019,plain,(sk5 | (rel_s4 @ sk1 @ sk9) | (sk7 != sk2)),inference(simp,[status(thm)],[1015])).
% 82.65/26.09 thf(990,plain,(! [A:$i] : (~ (sk5) | ~ (($true)) | (rel_s4 @ sk1 @ A) | ((rel_s4 @ sk2 @ sk10) != (rel_s4 @ sk2 @ A)))),inference(paramod_ordered,[status(thm)],[18,537])).
% 82.65/26.09 thf(991,plain,(! [A:$i] : (~ (sk5) | (rel_s4 @ sk1 @ A) | ((rel_s4 @ sk2 @ sk10) != (rel_s4 @ sk2 @ A)))),inference(simp,[status(thm)],[990])).
% 82.65/26.09 thf(992,plain,(~ (sk5) | (rel_s4 @ sk1 @ sk10)),inference(pattern_uni,[status(thm)],[991:[bind(A, $thf(sk10))]])).
% 82.65/26.09 thf(7778,plain,(! [B:$i,A:$i] : (sk5 | ~ (($true)) | (exists_in_world @ (sk12 @ B) @ A) | ((rel_s4 @ sk7 @ sk9) != (rel_s4 @ B @ A)))),inference(paramod_ordered,[status(thm)],[10,5453])).
% 82.65/26.09 thf(7779,plain,(! [B:$i,A:$i] : (sk5 | (exists_in_world @ (sk12 @ B) @ A) | ((rel_s4 @ sk7 @ sk9) != (rel_s4 @ B @ A)))),inference(simp,[status(thm)],[7778])).
% 82.65/26.09 thf(7780,plain,(sk5 | (exists_in_world @ (sk12 @ sk7) @ sk9)),inference(pattern_uni,[status(thm)],[7779:[bind(A, $thf(sk9)),bind(B, $thf(sk7))]])).
% 82.65/26.09 thf(9214,plain,(! [O:$i,N:$i,M:$i,L:$i,K:$i,J:mu,I:$i,H:$i,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ D @ E)) | ~ (($true)) | (~ (rel_s4 @ G @ H)) | (~ (rel_s4 @ H @ I)) | (~ (exists_in_world @ J @ K)) | (~ (rel_s4 @ K @ L)) | (~ (rel_s4 @ M @ N)) | (~ (rel_s4 @ N @ sk1)) | (p @ I) | (~ (rel_s4 @ sk2 @ O)) | (~ (rel_s4 @ O @ D)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ F @ M)) | (~ (exists_in_world @ J @ sk2)) | (~ (p @ (sk3 @ sk11 @ J @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ L)) | (~ (rel_s4 @ L @ G)) | ((sk4 @ G @ J @ L) != sk2) | ((rel_s4 @ A @ C) != (rel_s4 @ E @ F)))),inference(paramod_ordered,[status(thm)],[33,8200])).
% 82.65/26.09 thf(9215,plain,(! [O:$i,N:$i,M:$i,L:$i,K:$i,J:mu,I:$i,H:$i,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ G @ H)) | (~ (rel_s4 @ H @ I)) | (~ (exists_in_world @ J @ K)) | (~ (rel_s4 @ K @ L)) | (~ (rel_s4 @ M @ N)) | (~ (rel_s4 @ N @ sk1)) | (p @ I) | (~ (rel_s4 @ sk2 @ O)) | (~ (rel_s4 @ O @ D)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ F @ M)) | (~ (exists_in_world @ J @ sk2)) | (~ (p @ (sk3 @ sk11 @ J @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ L)) | (~ (rel_s4 @ L @ G)) | ((sk4 @ G @ J @ L) != sk2) | ((rel_s4 @ A @ C) != (rel_s4 @ E @ F)))),inference(simp,[status(thm)],[9214])).
% 82.65/26.09 thf(9216,plain,(! [M:$i,L:$i,K:$i,J:$i,I:$i,H:mu,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ D @ A)) | (~ (rel_s4 @ E @ F)) | (~ (rel_s4 @ F @ G)) | (~ (exists_in_world @ H @ I)) | (~ (rel_s4 @ I @ J)) | (~ (rel_s4 @ K @ L)) | (~ (rel_s4 @ L @ sk1)) | (p @ G) | (~ (rel_s4 @ sk2 @ M)) | (~ (rel_s4 @ M @ D)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ C @ K)) | (~ (exists_in_world @ H @ sk2)) | (~ (p @ (sk3 @ sk11 @ H @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ J)) | (~ (rel_s4 @ J @ E)) | ((sk4 @ E @ H @ J) != sk2))),inference(pattern_uni,[status(thm)],[9215:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf(A)),bind(F, $thf(C))]])).
% 82.65/26.09 thf(9842,plain,(! [M:$i,L:$i,K:$i,J:$i,I:$i,H:mu,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (rel_s4 @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ D @ A)) | (~ (rel_s4 @ E @ F)) | (~ (rel_s4 @ F @ G)) | (~ (exists_in_world @ H @ I)) | (~ (rel_s4 @ I @ J)) | (~ (rel_s4 @ K @ L)) | (~ (rel_s4 @ L @ sk1)) | (p @ G) | (~ (rel_s4 @ sk2 @ M)) | (~ (rel_s4 @ M @ D)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ C @ K)) | (~ (exists_in_world @ H @ sk2)) | (~ (p @ (sk3 @ sk11 @ H @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ J)) | (~ (rel_s4 @ J @ E)) | ((sk4 @ E @ H @ J) != sk2))),inference(simp,[status(thm)],[9216])).
% 82.65/26.09 thf(11299,plain,(! [P:$i,O:$i,N:$i,M:$i,L:$i,K:mu,J:$i,I:$i,H:$i,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:mu] : ((~ (exists_in_world @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ E @ F)) | (~ (rel_s4 @ G @ D)) | (~ (rel_s4 @ H @ I)) | (~ (rel_s4 @ I @ J)) | (~ (exists_in_world @ K @ L)) | (~ (rel_s4 @ L @ M)) | (~ (rel_s4 @ N @ O)) | (~ (rel_s4 @ O @ sk1)) | (p @ J) | (~ (rel_s4 @ sk2 @ P)) | (~ (rel_s4 @ P @ G)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ F @ N)) | ~ (($true)) | (~ (p @ (sk3 @ sk11 @ K @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ M)) | (~ (rel_s4 @ M @ H)) | ((sk4 @ H @ K @ M) != sk2) | ((exists_in_world @ A @ C) != (exists_in_world @ K @ sk2)))),inference(paramod_ordered,[status(thm)],[35,9842])).
% 82.65/26.09 thf(11300,plain,(! [P:$i,O:$i,N:$i,M:$i,L:$i,K:mu,J:$i,I:$i,H:$i,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:mu] : ((~ (exists_in_world @ A @ B)) | (~ (rel_s4 @ B @ C)) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ E @ F)) | (~ (rel_s4 @ G @ D)) | (~ (rel_s4 @ H @ I)) | (~ (rel_s4 @ I @ J)) | (~ (exists_in_world @ K @ L)) | (~ (rel_s4 @ L @ M)) | (~ (rel_s4 @ N @ O)) | (~ (rel_s4 @ O @ sk1)) | (p @ J) | (~ (rel_s4 @ sk2 @ P)) | (~ (rel_s4 @ P @ G)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ F @ N)) | (~ (p @ (sk3 @ sk11 @ K @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ M)) | (~ (rel_s4 @ M @ H)) | ((sk4 @ H @ K @ M) != sk2) | ((exists_in_world @ A @ C) != (exists_in_world @ K @ sk2)))),inference(simp,[status(thm)],[11299])).
% 82.65/26.09 thf(11301,plain,(! [N:$i,M:$i,L:$i,K:$i,J:$i,I:$i,H:$i,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:mu] : ((~ (exists_in_world @ A @ B)) | (~ (rel_s4 @ B @ sk2)) | (~ (rel_s4 @ C @ D)) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ F @ C)) | (~ (rel_s4 @ G @ H)) | (~ (rel_s4 @ H @ I)) | (~ (exists_in_world @ A @ J)) | (~ (rel_s4 @ J @ K)) | (~ (rel_s4 @ L @ M)) | (~ (rel_s4 @ M @ sk1)) | (p @ I) | (~ (rel_s4 @ sk2 @ N)) | (~ (rel_s4 @ N @ F)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ E @ L)) | (~ (p @ (sk3 @ sk11 @ A @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ K)) | (~ (rel_s4 @ K @ G)) | ((sk4 @ G @ A @ K) != sk2))),inference(pattern_uni,[status(thm)],[11300:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(sk2)),bind(D, $thf(D)),bind(E, $thf(E)),bind(F, $thf(F)),bind(G, $thf(G)),bind(H, $thf(H)),bind(I, $thf(I)),bind(J, $thf(J)),bind(K, $thf(A))]])).
% 82.65/26.09 thf(11910,plain,(! [N:$i,M:$i,L:$i,K:$i,J:$i,I:$i,H:$i,G:$i,F:$i,E:$i,D:$i,C:$i,B:$i,A:mu] : ((~ (exists_in_world @ A @ B)) | (~ (rel_s4 @ B @ sk2)) | (~ (rel_s4 @ C @ D)) | (~ (rel_s4 @ D @ E)) | (~ (rel_s4 @ F @ C)) | (~ (rel_s4 @ G @ H)) | (~ (rel_s4 @ H @ I)) | (~ (exists_in_world @ A @ J)) | (~ (rel_s4 @ J @ K)) | (~ (rel_s4 @ L @ M)) | (~ (rel_s4 @ M @ sk1)) | (p @ I) | (~ (rel_s4 @ sk2 @ N)) | (~ (rel_s4 @ N @ F)) | ~ (sk5) | (sk11 != sk1) | (~ (rel_s4 @ E @ L)) | (~ (p @ (sk3 @ sk11 @ A @ sk2))) | (sk2 != sk1) | (sk10 != sk2) | (sk11 != sk10) | (~ (rel_s4 @ sk2 @ K)) | (~ (rel_s4 @ K @ G)) | ((sk4 @ G @ A @ K) != sk2))),inference(simp,[status(thm)],[11301])).
% 82.65/26.09 thf(572,plain,(! [A:$i] : (sk5 | ~ (($true)) | (rel_s4 @ A @ sk2) | ((rel_s4 @ sk6 @ sk7) != (rel_s4 @ A @ sk1)))),inference(paramod_ordered,[status(thm)],[15,469])).
% 82.65/26.09 thf(573,plain,(! [A:$i] : (sk5 | (rel_s4 @ A @ sk2) | ((rel_s4 @ sk6 @ sk7) != (rel_s4 @ A @ sk1)))),inference(simp,[status(thm)],[572])).
% 82.65/26.09 thf(605,plain,(! [A:$i] : (sk5 | (rel_s4 @ A @ sk2) | (sk6 != A) | (sk7 != sk1))),inference(simp,[status(thm)],[573])).
% 82.65/26.09 thf(624,plain,(sk5 | (rel_s4 @ sk6 @ sk2) | (sk7 != sk1)),inference(simp,[status(thm)],[605])).
% 82.65/26.09 thf(5180,plain,(sk5 | ~ (($true)) | (p @ sk2) | sk5 | ((rel_s4 @ sk6 @ sk9) != (rel_s4 @ sk6 @ sk1))),inference(paramod_ordered,[status(thm)],[5045,553])).
% 82.65/26.09 thf(5181,plain,(sk5 | (p @ sk2) | ((rel_s4 @ sk6 @ sk9) != (rel_s4 @ sk6 @ sk1))),inference(simp,[status(thm)],[5180])).
% 82.65/26.09 thf(5264,plain,(sk5 | (p @ sk2) | (sk6 != sk6) | (sk9 != sk1)),inference(simp,[status(thm)],[5181])).
% 82.65/26.09 thf(5275,plain,(sk5 | (p @ sk2) | (sk9 != sk1)),inference(simp,[status(thm)],[5264])).
% 82.65/26.09 thf(4947,plain,(! [A:$i] : (sk5 | (sk6 != sk2) | sk5 | ~ (($true)) | (rel_s4 @ A @ sk9) | ((rel_s4 @ sk1 @ sk7) != (rel_s4 @ A @ sk7)))),inference(paramod_ordered,[status(thm)],[1018,451])).
% 82.65/26.09 thf(4948,plain,(! [A:$i] : (sk5 | (sk6 != sk2) | (rel_s4 @ A @ sk9) | ((rel_s4 @ sk1 @ sk7) != (rel_s4 @ A @ sk7)))),inference(simp,[status(thm)],[4947])).
% 82.65/26.09 thf(4949,plain,(sk5 | (sk6 != sk2) | (rel_s4 @ sk1 @ sk9)),inference(pattern_uni,[status(thm)],[4948:[bind(A, $thf(sk1))]])).
% 82.65/26.09 thf(19516,plain,(($false)),inference(e,[status(thm)],[10,5045,4732,537,205,5082,246,5329,7798,8200,170,614,24,25,14,7822,2501,20,5127,46,881,29,623,7792,7786,28,7834,21,33,5626,1017,5273,6805,13,32,34,17,5647,1752,27,22,5488,451,7,5849,35,1018,553,63,18,5079,544,31,5453,11,3533,218,26,7840,55,23,995,833,30,5601,210,4193,1019,1357,992,15,7780,11910,9842,624,5275,469,4949,708])).
% 82.65/26.09 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 82.65/26.09 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------