%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYN397^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 : n026.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:33 AM UTC 2026
% Result : Theorem 8.86s 3.54s
% Output : Refutation 8.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN397^7 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.10/0.21 % Computer : n026.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 16:19:12 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.02/0.80 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.58/1.08 % [INFO] Parsing done (273ms).
% 1.58/1.10 % [INFO] Running in sequential loop mode.
% 2.40/1.54 % [INFO] eprover registered as external prover.
% 2.40/1.55 % [INFO] Scanning for conjecture ...
% 2.82/1.73 % [INFO] Found a conjecture (or negated_conjecture) and 4 axioms. Running axiom selection ...
% 2.82/1.77 % [INFO] Axiom selection finished. Selected 4 axioms (removed 0 axioms).
% 2.82/1.77 % [INFO] Problem is higher-order (TPTP THF).
% 2.82/1.78 % [INFO] Type checking passed.
% 2.82/1.78 % [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 ...
% 8.86/3.53 % External prover 'e' found a proof!
% 8.86/3.53 % [INFO] Killing All external provers ...
% 8.86/3.54 % Time passed: 3183ms (effective reasoning time: 2425ms)
% 8.86/3.54 % 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)>
% 8.86/3.54 % Axioms used in derivation (4): a1, nonempty_ax, cumulative_ax, a2
% 8.86/3.54 % No. of inferences in proof: 100
% 8.86/3.54 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 3183 ms resp. 2425 ms w/o parsing
% 8.28/3.65 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.28/3.65 thf(mu_type, type, mu: $tType).
% 8.28/3.65 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 8.28/3.65 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 8.28/3.65 thf(mand_decl, type, mand: (($i > $o) > (($i > $o) > ($i > $o)))).
% 8.28/3.65 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 8.28/3.65 thf(exists_in_world_decl, type, exists_in_world: (mu > ($i > $o))).
% 8.28/3.65 thf(mforall_ind_decl, type, mforall_ind: ((mu > ($i > $o)) > ($i > $o))).
% 8.28/3.65 thf(mexists_ind_decl, type, mexists_ind: ((mu > ($i > $o)) > ($i > $o))).
% 8.28/3.65 thf(mreflexive_decl, type, mreflexive: (($i > ($i > $o)) > $o)).
% 8.28/3.65 thf(mtransitive_decl, type, mtransitive: (($i > ($i > $o)) > $o)).
% 8.28/3.65 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 8.28/3.65 thf(rel_s4_decl, type, rel_s4: ($i > ($i > $o))).
% 8.28/3.65 thf(mbox_s4_decl, type, mbox_s4: (($i > $o) > ($i > $o))).
% 8.28/3.65 thf(f_decl, type, f: (mu > ($i > $o))).
% 8.28/3.65 thf(sk1_decl, type, sk1: $o).
% 8.28/3.65 thf(sk2_decl, type, sk2: $i).
% 8.28/3.65 thf(sk3_decl, type, sk3: $i).
% 8.28/3.65 thf(sk4_decl, type, sk4: (mu > ($i > $i))).
% 8.28/3.65 thf(sk5_decl, type, sk5: $i).
% 8.28/3.65 thf(sk6_decl, type, sk6: mu).
% 8.28/3.65 thf(sk7_decl, type, sk7: $i).
% 8.28/3.65 thf(sk8_decl, type, sk8: $i).
% 8.28/3.65 thf(sk9_decl, type, sk9: $i).
% 8.28/3.65 thf(sk10_decl, type, sk10: ($i > (mu > ($i > $i)))).
% 8.28/3.65 thf(sk11_decl, type, sk11: $i).
% 8.28/3.65 thf(sk12_decl, type, sk12: mu).
% 8.28/3.65 thf(sk13_decl, type, sk13: ($i > mu)).
% 8.28/3.65 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 8.28/3.65 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 8.28/3.65 thf(mand_def, definition, mand = (^ [A:($i > $o),B:($i > $o)]: (mnot @ (mor @ (mnot @ A) @ (mnot @ B)))) ).
% 8.28/3.65 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 8.28/3.65 thf(mforall_ind_def, definition, mforall_ind = (^ [A:(mu > ($i > $o)),B:$i]: ! [C:mu]: ((exists_in_world @ C @ B) => (A @ C @ B))) ).
% 8.28/3.65 thf(mexists_ind_def, definition, mexists_ind = (^ [A:(mu > ($i > $o))]: (mnot @ (mforall_ind @ (^ [B:mu]: (mnot @ (A @ B)))))) ).
% 8.28/3.65 thf(mreflexive_def, definition, mreflexive = (^ [A:($i > ($i > $o))]: ! [B:$i]: (A @ B @ B)) ).
% 8.28/3.65 thf(mtransitive_def, definition, mtransitive = (^ [A:($i > ($i > $o))]: ! [B:$i,C:$i,D:$i]: (((A @ B @ C) & (A @ C @ D)) => (A @ B @ D))) ).
% 8.28/3.65 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 8.28/3.65 thf(mbox_s4_def, definition, mbox_s4 = (^ [A:($i > $o),B:$i]: ! [C:$i]: (~ (rel_s4 @ B @ C) | (A @ C))) ).
% 8.28/3.65 thf(sk2_def, definition, sk2 = (@+ [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 @ D @ E))))))) | ! [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) | (f @ D @ F)))))))))) ).
% 8.28/3.65 thf(sk3_def, definition, sk3 = (@+ [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) | (f @ C @ D))))))) | ! [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) | (f @ C @ E))))))))) ).
% 8.28/3.65 thf(sk4_def, definition, sk4 = (^ [A:mu,B:$i]: (@+ [C:$i]: ~ (~ (rel_s4 @ B @ C) | (f @ A @ C)))) ).
% 8.28/3.65 thf(sk5_def, definition, sk5 = (@+ [A:$i]: ~ (~ (rel_s4 @ sk3 @ A) | ! [B:mu]: ((exists_in_world @ B @ A) => (! [C:$i]: (~ (rel_s4 @ A @ C) | ~ (! [D:$i]: (~ (rel_s4 @ C @ D) | (f @ B @ D)))))))) ).
% 8.28/3.65 thf(sk6_def, definition, sk6 = (@+ [A:mu]: ~ ((exists_in_world @ A @ sk5) => (! [B:$i]: (~ (rel_s4 @ sk5 @ B) | ~ (! [C:$i]: (~ (rel_s4 @ B @ C) | (f @ A @ C))))))) ).
% 8.28/3.65 thf(sk7_def, definition, sk7 = (@+ [A:$i]: ~ (~ (rel_s4 @ sk5 @ A) | ~ (! [B:$i]: (~ (rel_s4 @ A @ B) | (f @ sk6 @ B))))) ).
% 8.28/3.65 thf(sk8_def, definition, sk8 = (@+ [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) | (f @ D @ F)))))))) | ! [C:$i]: (~ (rel_s4 @ B @ C) | ! [D:mu]: ((exists_in_world @ D @ C) => (~ (! [E:$i]: (~ (rel_s4 @ C @ E) | (f @ D @ E))))))))) ).
% 8.28/3.65 thf(sk9_def, definition, sk9 = (@+ [A:$i]: ~ (~ (rel_s4 @ sk8 @ 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) | (f @ C @ E)))))))) | ! [B:$i]: (~ (rel_s4 @ A @ B) | ! [C:mu]: ((exists_in_world @ C @ B) => (~ (! [D:$i]: (~ (rel_s4 @ B @ D) | (f @ C @ D)))))))) ).
% 8.28/3.65 thf(sk10_def, definition, sk10 = (^ [A:$i,B:mu,C:$i]: (@+ [D:$i]: ~ (~ (rel_s4 @ A @ D) | (f @ B @ D)))) ).
% 8.28/3.65 thf(sk11_def, definition, sk11 = (@+ [A:$i]: ~ (~ (rel_s4 @ sk9 @ A) | ! [B:mu]: ((exists_in_world @ B @ A) => (~ (! [C:$i]: (~ (rel_s4 @ A @ C) | (f @ B @ C))))))) ).
% 8.28/3.65 thf(sk12_def, definition, sk12 = (@+ [A:mu]: ~ ((exists_in_world @ A @ sk11) => (~ (! [B:$i]: (~ (rel_s4 @ sk11 @ B) | (f @ A @ B)))))) ).
% 8.28/3.65 thf(sk13_def, definition, sk13 = (^ [A:$i]: (@+ [B:mu]: (exists_in_world @ B @ A))) ).
% 8.28/3.65 thf(1,conjecture,((mvalid @ (mand @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (mnot @ (mexists_ind @ (^ [A:mu]: (mbox_s4 @ (f @ A)))))) @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mnot @ (mbox_s4 @ (f @ A))))))))) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mnot @ (mbox_s4 @ (f @ A))))))) @ (mbox_s4 @ (mnot @ (mexists_ind @ (^ [A:mu]: (mbox_s4 @ (f @ A))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',kalish204)).
% 8.28/3.65 thf(2,negated_conjecture,((~ (mvalid @ (mand @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (mnot @ (mexists_ind @ (^ [A:mu]: (mbox_s4 @ (f @ A)))))) @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mnot @ (mbox_s4 @ (f @ A))))))))) @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (mforall_ind @ (^ [A:mu]: (mbox_s4 @ (mnot @ (mbox_s4 @ (f @ A))))))) @ (mbox_s4 @ (mnot @ (mexists_ind @ (^ [A:mu]: (mbox_s4 @ (f @ A)))))))))))),inference(neg_conjecture,[status(cth)],[1])).
% 8.28/3.65 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 @ D @ E))))))) | ! [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) | (f @ D @ F))))))))) | ~ (! [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) | (f @ D @ F)))))))) | ! [C:$i]: (~ (rel_s4 @ B @ C) | ! [D:mu]: ((exists_in_world @ D @ C) => (~ (! [E:$i]: (~ (rel_s4 @ C @ E) | (f @ D @ E)))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 8.28/3.65 thf(8,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 @ D @ E))))))) | ! [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) | (f @ D @ F))))))))) | ~ (! [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) | (f @ D @ F)))))))) | ! [C:$i]: (~ (rel_s4 @ B @ C) | ! [D:mu]: ((exists_in_world @ D @ C) => (~ (! [E:$i]: (~ (rel_s4 @ C @ E) | (f @ D @ E)))))))))))),inference(miniscope,[status(thm)],[7])).
% 8.28/3.65 thf(9,plain,(! [G:$i,F:$i,E:mu,D:$i,C:$i,B:mu,A:$i] : ((((rel_s4 @ sk2 @ sk3) | (sk1)) & (~ (rel_s4 @ sk3 @ A) | ~ (exists_in_world @ B @ A) | (rel_s4 @ A @ (sk4 @ B @ A)) | (sk1)) & (~ (rel_s4 @ sk3 @ A) | ~ (exists_in_world @ B @ A) | ~ (f @ B @ (sk4 @ B @ A)) | (sk1)) & ((rel_s4 @ sk3 @ sk5) | (sk1)) & ((exists_in_world @ sk6 @ sk5) | (sk1)) & ((rel_s4 @ sk5 @ sk7) | (sk1)) & (~ (rel_s4 @ sk7 @ C) | (f @ sk6 @ C) | (sk1)) & (~ (sk1) | (rel_s4 @ sk8 @ sk9)) & (~ (sk1) | ~ (rel_s4 @ sk9 @ D) | ~ (exists_in_world @ E @ D) | ~ (rel_s4 @ D @ F) | (rel_s4 @ F @ (sk10 @ F @ E @ D))) & (~ (sk1) | ~ (rel_s4 @ sk9 @ D) | ~ (exists_in_world @ E @ D) | ~ (rel_s4 @ D @ F) | ~ (f @ E @ (sk10 @ F @ E @ D))) & (~ (sk1) | (rel_s4 @ sk9 @ sk11)) & (~ (sk1) | (exists_in_world @ sk12 @ sk11)) & (~ (sk1) | ~ (rel_s4 @ sk11 @ G) | (f @ sk12 @ G))))),inference(cnf,[status(esa)],[8])).
% 8.28/3.65 thf(16,plain,(! [A:$i] : (~ (sk1) | (~ (rel_s4 @ sk11 @ A)) | (f @ sk12 @ A))),inference(cnfConj,[status(thm)],[9])).
% 8.28/3.65 thf(25,plain,(! [A:$i] : (~ (sk1) | (~ (rel_s4 @ sk11 @ A)) | (f @ sk12 @ A))),inference(simp,[status(thm)],[16])).
% 8.28/3.65 thf(13,plain,(~ (sk1) | (rel_s4 @ sk9 @ sk11)),inference(cnfConj,[status(thm)],[9])).
% 8.28/3.65 thf(4,axiom,((mreflexive @ rel_s4)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1)).
% 8.28/3.65 thf(29,plain,((! [A:$i]: (rel_s4 @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 8.28/3.65 thf(30,plain,(! [A:$i] : ((rel_s4 @ A @ A))),inference(cnf,[status(esa)],[29])).
% 8.28/3.65 thf(11,plain,(~ (sk1) | (exists_in_world @ sk12 @ sk11)),inference(cnfConj,[status(thm)],[9])).
% 8.28/3.65 thf(20,plain,(! [C:$i,B:mu,A:$i] : (~ (sk1) | (~ (rel_s4 @ sk9 @ A)) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (~ (f @ B @ (sk10 @ C @ B @ A))))),inference(cnfConj,[status(thm)],[9])).
% 8.28/3.65 thf(24,plain,(! [C:$i,B:mu,A:$i] : (~ (sk1) | (~ (rel_s4 @ sk9 @ A)) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (~ (f @ B @ (sk10 @ C @ B @ A))))),inference(simp,[status(thm)],[20])).
% 8.28/3.65 thf(44,plain,(! [C:$i,B:mu,A:$i] : (~ (sk1) | ~ (sk1) | (~ (rel_s4 @ sk9 @ A)) | ~ (($true)) | (~ (rel_s4 @ A @ C)) | (~ (f @ B @ (sk10 @ C @ B @ A))) | ((exists_in_world @ sk12 @ sk11) != (exists_in_world @ B @ A)))),inference(paramod_ordered,[status(thm)],[11,24])).
% 8.28/3.65 thf(45,plain,(! [C:$i,B:mu,A:$i] : (~ (sk1) | (~ (rel_s4 @ sk9 @ A)) | (~ (rel_s4 @ A @ C)) | (~ (f @ B @ (sk10 @ C @ B @ A))) | ((exists_in_world @ sk12 @ sk11) != (exists_in_world @ B @ A)))),inference(simp,[status(thm)],[44])).
% 8.28/3.65 thf(46,plain,(! [A:$i] : (~ (sk1) | (~ (rel_s4 @ sk9 @ sk11)) | (~ (rel_s4 @ sk11 @ A)) | (~ (f @ sk12 @ (sk10 @ A @ sk12 @ sk11))))),inference(pattern_uni,[status(thm)],[45:[bind(A, $thf(sk11)),bind(B, $thf(sk12))]])).
% 8.28/3.65 thf(58,plain,(! [A:$i] : (~ (sk1) | (~ (rel_s4 @ sk9 @ sk11)) | (~ (rel_s4 @ sk11 @ A)) | (~ (f @ sk12 @ (sk10 @ A @ sk12 @ sk11))))),inference(simp,[status(thm)],[46])).
% 8.28/3.65 thf(66,plain,(! [B:$i,A:$i] : (~ (sk1) | (~ (rel_s4 @ sk9 @ sk11)) | ~ (($true)) | (~ (f @ sk12 @ (sk10 @ B @ sk12 @ sk11))) | ((rel_s4 @ A @ A) != (rel_s4 @ sk11 @ B)))),inference(paramod_ordered,[status(thm)],[30,58])).
% 8.28/3.65 thf(67,plain,(! [B:$i,A:$i] : (~ (sk1) | (~ (rel_s4 @ sk9 @ sk11)) | (~ (f @ sk12 @ (sk10 @ B @ sk12 @ sk11))) | ((rel_s4 @ A @ A) != (rel_s4 @ sk11 @ B)))),inference(simp,[status(thm)],[66])).
% 8.28/3.65 thf(68,plain,(~ (sk1) | (~ (rel_s4 @ sk9 @ sk11)) | (~ (f @ sk12 @ (sk10 @ sk11 @ sk12 @ sk11)))),inference(pattern_uni,[status(thm)],[67:[bind(A, $thf(sk11)),bind(B, $thf(sk11))]])).
% 8.28/3.65 thf(167,plain,(~ (sk1) | ~ (sk1) | ~ (($true)) | (~ (f @ sk12 @ (sk10 @ sk11 @ sk12 @ sk11))) | ((rel_s4 @ sk9 @ sk11) != (rel_s4 @ sk9 @ sk11))),inference(paramod_ordered,[status(thm)],[13,68])).
% 8.28/3.65 thf(168,plain,(~ (sk1) | (~ (f @ sk12 @ (sk10 @ sk11 @ sk12 @ sk11))) | ((rel_s4 @ sk9 @ sk11) != (rel_s4 @ sk9 @ sk11))),inference(simp,[status(thm)],[167])).
% 8.28/3.65 thf(169,plain,(~ (sk1) | (~ (f @ sk12 @ (sk10 @ sk11 @ sk12 @ sk11)))),inference(pattern_uni,[status(thm)],[168:[]])).
% 8.28/3.65 thf(406,plain,(! [A:$i] : (~ (sk1) | (~ (rel_s4 @ sk11 @ A)) | ~ (sk1) | ~ (($true)) | ((f @ sk12 @ A) != (f @ sk12 @ (sk10 @ sk11 @ sk12 @ sk11))))),inference(paramod_ordered,[status(thm)],[25,169])).
% 8.28/3.65 thf(407,plain,(! [A:$i] : (~ (sk1) | (~ (rel_s4 @ sk11 @ A)) | ((f @ sk12 @ A) != (f @ sk12 @ (sk10 @ sk11 @ sk12 @ sk11))))),inference(simp,[status(thm)],[406])).
% 8.28/3.65 thf(408,plain,(~ (sk1) | (~ (rel_s4 @ sk11 @ (sk10 @ sk11 @ sk12 @ sk11)))),inference(pattern_uni,[status(thm)],[407:[bind(A, $thf(sk10 @ sk11 @ sk12 @ sk11))]])).
% 8.28/3.65 thf(14,plain,((rel_s4 @ sk3 @ sk5) | sk1),inference(cnfConj,[status(thm)],[9])).
% 8.28/3.65 thf(10,plain,(! [A:$i] : ((~ (rel_s4 @ sk7 @ A)) | (f @ sk6 @ A) | sk1)),inference(cnfConj,[status(thm)],[9])).
% 8.28/3.65 thf(23,plain,(! [A:$i] : ((~ (rel_s4 @ sk7 @ A)) | (f @ sk6 @ A) | sk1)),inference(simp,[status(thm)],[10])).
% 8.28/3.65 thf(15,plain,((exists_in_world @ sk6 @ sk5) | sk1),inference(cnfConj,[status(thm)],[9])).
% 8.28/3.65 thf(12,plain,(! [B:mu,A:$i] : ((~ (rel_s4 @ sk3 @ A)) | (~ (exists_in_world @ B @ A)) | (~ (f @ B @ (sk4 @ B @ A))) | sk1)),inference(cnfConj,[status(thm)],[9])).
% 8.28/3.65 thf(116,plain,(! [B:mu,A:$i] : (sk1 | (~ (rel_s4 @ sk3 @ A)) | ~ (($true)) | (~ (f @ B @ (sk4 @ B @ A))) | sk1 | ((exists_in_world @ sk6 @ sk5) != (exists_in_world @ B @ A)))),inference(paramod_ordered,[status(thm)],[15,12])).
% 8.28/3.65 thf(117,plain,(! [B:mu,A:$i] : (sk1 | (~ (rel_s4 @ sk3 @ A)) | (~ (f @ B @ (sk4 @ B @ A))) | ((exists_in_world @ sk6 @ sk5) != (exists_in_world @ B @ A)))),inference(simp,[status(thm)],[116])).
% 8.28/3.65 thf(118,plain,(sk1 | (~ (rel_s4 @ sk3 @ sk5)) | (~ (f @ sk6 @ (sk4 @ sk6 @ sk5)))),inference(pattern_uni,[status(thm)],[117:[bind(A, $thf(sk5)),bind(B, $thf(sk6))]])).
% 8.28/3.65 thf(148,plain,(sk1 | sk1 | ~ (($true)) | (~ (f @ sk6 @ (sk4 @ sk6 @ sk5))) | ((rel_s4 @ sk3 @ sk5) != (rel_s4 @ sk3 @ sk5))),inference(paramod_ordered,[status(thm)],[14,118])).
% 8.28/3.65 thf(149,plain,(sk1 | (~ (f @ sk6 @ (sk4 @ sk6 @ sk5))) | ((rel_s4 @ sk3 @ sk5) != (rel_s4 @ sk3 @ sk5))),inference(simp,[status(thm)],[148])).
% 8.28/3.65 thf(150,plain,(sk1 | (~ (f @ sk6 @ (sk4 @ sk6 @ sk5)))),inference(pattern_uni,[status(thm)],[149:[]])).
% 8.28/3.65 thf(204,plain,(! [A:$i] : ((~ (rel_s4 @ sk7 @ A)) | sk1 | sk1 | ~ (($true)) | ((f @ sk6 @ A) != (f @ sk6 @ (sk4 @ sk6 @ sk5))))),inference(paramod_ordered,[status(thm)],[23,150])).
% 8.28/3.65 thf(205,plain,(! [A:$i] : ((~ (rel_s4 @ sk7 @ A)) | sk1 | ((f @ sk6 @ A) != (f @ sk6 @ (sk4 @ sk6 @ sk5))))),inference(simp,[status(thm)],[204])).
% 8.28/3.65 thf(206,plain,((~ (rel_s4 @ sk7 @ (sk4 @ sk6 @ sk5))) | sk1),inference(pattern_uni,[status(thm)],[205:[bind(A, $thf(sk4 @ sk6 @ sk5))]])).
% 8.28/3.65 thf(422,plain,(! [B:$i,A:$i] : (~ (sk1) | ~ (($true)) | (f @ sk12 @ B) | ((rel_s4 @ A @ A) != (rel_s4 @ sk11 @ B)))),inference(paramod_ordered,[status(thm)],[30,25])).
% 8.28/3.65 thf(423,plain,(! [B:$i,A:$i] : (~ (sk1) | (f @ sk12 @ B) | ((rel_s4 @ A @ A) != (rel_s4 @ sk11 @ B)))),inference(simp,[status(thm)],[422])).
% 8.28/3.65 thf(424,plain,(~ (sk1) | (f @ sk12 @ sk11)),inference(pattern_uni,[status(thm)],[423:[bind(A, $thf(sk11)),bind(B, $thf(sk11))]])).
% 8.28/3.65 thf(442,plain,(~ (sk1) | ~ (sk1) | ~ (($true)) | ((f @ sk12 @ (sk10 @ sk11 @ sk12 @ sk11)) != (f @ sk12 @ sk11))),inference(paramod_ordered,[status(thm)],[424,169])).
% 8.28/3.65 thf(443,plain,(~ (sk1) | ((f @ sk12 @ (sk10 @ sk11 @ sk12 @ sk11)) != (f @ sk12 @ sk11))),inference(simp,[status(thm)],[442])).
% 8.28/3.65 thf(453,plain,(~ (sk1) | (sk12 != sk12) | ((sk10 @ sk11 @ sk12 @ sk11) != sk11)),inference(simp,[status(thm)],[443])).
% 8.28/3.65 thf(456,plain,(~ (sk1) | ((sk10 @ sk11 @ sk12 @ sk11) != sk11)),inference(simp,[status(thm)],[453])).
% 8.28/3.65 thf(184,plain,(! [A:$i] : (sk1 | ~ (($true)) | (f @ sk6 @ A) | sk1 | ((rel_s4 @ sk7 @ A) != (rel_s4 @ sk3 @ sk5)))),inference(paramod_ordered,[status(thm)],[14,23])).
% 8.28/3.65 thf(185,plain,(! [A:$i] : (sk1 | (f @ sk6 @ A) | ((rel_s4 @ sk7 @ A) != (rel_s4 @ sk3 @ sk5)))),inference(simp,[status(thm)],[184])).
% 8.28/3.65 thf(207,plain,(! [A:$i] : (sk1 | (f @ sk6 @ A) | (sk7 != sk3) | (A != sk5))),inference(simp,[status(thm)],[185])).
% 8.28/3.65 thf(213,plain,(sk1 | (f @ sk6 @ sk5) | (sk7 != sk3)),inference(simp,[status(thm)],[207])).
% 8.28/3.65 thf(17,plain,(~ (sk1) | (rel_s4 @ sk8 @ sk9)),inference(cnfConj,[status(thm)],[9])).
% 8.28/3.65 thf(411,plain,(! [A:$i] : (~ (sk1) | ~ (sk1) | ~ (($true)) | (f @ sk12 @ A) | ((rel_s4 @ sk11 @ A) != (rel_s4 @ sk8 @ sk9)))),inference(paramod_ordered,[status(thm)],[17,25])).
% 8.28/3.65 thf(412,plain,(! [A:$i] : (~ (sk1) | (f @ sk12 @ A) | ((rel_s4 @ sk11 @ A) != (rel_s4 @ sk8 @ sk9)))),inference(simp,[status(thm)],[411])).
% 8.28/3.65 thf(436,plain,(! [A:$i] : ((f @ sk12 @ A) | ~ (sk1) | (sk11 != sk8) | (A != sk9))),inference(simp,[status(thm)],[412])).
% 8.28/3.65 thf(438,plain,((f @ sk12 @ sk9) | ~ (sk1) | (sk11 != sk8)),inference(simp,[status(thm)],[436])).
% 8.28/3.65 thf(3,axiom,((! [A:$i]: ? [B:mu]: (exists_in_world @ B @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',nonempty_ax)).
% 8.28/3.65 thf(27,plain,((! [A:$i]: ? [B:mu]: (exists_in_world @ B @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 8.28/3.65 thf(28,plain,(! [A:$i] : ((exists_in_world @ (sk13 @ A) @ A))),inference(cnf,[status(esa)],[27])).
% 8.28/3.65 thf(281,plain,(sk1 | ~ (($true)) | sk1 | ((rel_s4 @ sk7 @ (sk4 @ sk6 @ sk5)) != (rel_s4 @ sk3 @ sk5))),inference(paramod_ordered,[status(thm)],[14,206])).
% 8.28/3.65 thf(282,plain,(sk1 | ((rel_s4 @ sk7 @ (sk4 @ sk6 @ sk5)) != (rel_s4 @ sk3 @ sk5))),inference(simp,[status(thm)],[281])).
% 8.28/3.65 thf(297,plain,(sk1 | (sk7 != sk3) | ((sk4 @ sk6 @ sk5) != sk5)),inference(simp,[status(thm)],[282])).
% 8.28/3.65 thf(21,plain,((rel_s4 @ sk2 @ sk3) | sk1),inference(cnfConj,[status(thm)],[9])).
% 8.28/3.65 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)).
% 8.28/3.65 thf(33,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])).
% 8.28/3.65 thf(291,plain,(sk1 | ~ (($true)) | sk1 | ((rel_s4 @ sk7 @ (sk4 @ sk6 @ sk5)) != (rel_s4 @ sk2 @ sk3))),inference(paramod_ordered,[status(thm)],[21,206])).
% 8.28/3.65 thf(292,plain,(sk1 | ((rel_s4 @ sk7 @ (sk4 @ sk6 @ sk5)) != (rel_s4 @ sk2 @ sk3))),inference(simp,[status(thm)],[291])).
% 8.28/3.65 thf(296,plain,(sk1 | (sk7 != sk2) | ((sk4 @ sk6 @ sk5) != sk3)),inference(simp,[status(thm)],[292])).
% 8.28/3.65 thf(22,plain,(! [B:mu,A:$i] : ((~ (rel_s4 @ sk3 @ A)) | (~ (exists_in_world @ B @ A)) | (rel_s4 @ A @ (sk4 @ B @ A)) | sk1)),inference(cnfConj,[status(thm)],[9])).
% 8.28/3.65 thf(18,plain,((rel_s4 @ sk5 @ sk7) | sk1),inference(cnfConj,[status(thm)],[9])).
% 8.28/3.65 thf(197,plain,(! [B:$i,A:$i] : (~ (($true)) | (f @ sk6 @ B) | sk1 | ((rel_s4 @ A @ A) != (rel_s4 @ sk7 @ B)))),inference(paramod_ordered,[status(thm)],[30,23])).
% 8.28/3.65 thf(198,plain,(! [B:$i,A:$i] : ((f @ sk6 @ B) | sk1 | ((rel_s4 @ A @ A) != (rel_s4 @ sk7 @ B)))),inference(simp,[status(thm)],[197])).
% 8.28/3.65 thf(199,plain,((f @ sk6 @ sk7) | sk1),inference(pattern_uni,[status(thm)],[198:[bind(A, $thf(sk7)),bind(B, $thf(sk7))]])).
% 8.28/3.65 thf(5,axiom,((mtransitive @ rel_s4)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2)).
% 8.28/3.65 thf(31,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])).
% 8.28/3.65 thf(19,plain,(! [C:$i,B:mu,A:$i] : (~ (sk1) | (~ (rel_s4 @ sk9 @ A)) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (rel_s4 @ C @ (sk10 @ C @ B @ A)))),inference(cnfConj,[status(thm)],[9])).
% 8.28/3.65 thf(26,plain,(! [C:$i,B:mu,A:$i] : (~ (sk1) | (~ (rel_s4 @ sk9 @ A)) | (~ (exists_in_world @ B @ A)) | (~ (rel_s4 @ A @ C)) | (rel_s4 @ C @ (sk10 @ C @ B @ A)))),inference(simp,[status(thm)],[19])).
% 8.28/3.65 thf(200,plain,(! [A:$i] : (sk1 | ~ (($true)) | (f @ sk6 @ A) | sk1 | ((rel_s4 @ sk7 @ A) != (rel_s4 @ sk2 @ sk3)))),inference(paramod_ordered,[status(thm)],[21,23])).
% 8.28/3.65 thf(201,plain,(! [A:$i] : (sk1 | (f @ sk6 @ A) | ((rel_s4 @ sk7 @ A) != (rel_s4 @ sk2 @ sk3)))),inference(simp,[status(thm)],[200])).
% 8.28/3.65 thf(208,plain,(! [A:$i] : (sk1 | (f @ sk6 @ A) | (sk7 != sk2) | (A != sk3))),inference(simp,[status(thm)],[201])).
% 8.28/3.65 thf(210,plain,(sk1 | (f @ sk6 @ sk3) | (sk7 != sk2)),inference(simp,[status(thm)],[208])).
% 8.28/3.65 thf(462,plain,(~ (sk1) | ~ (sk1) | ~ (($true)) | ((rel_s4 @ sk11 @ (sk10 @ sk11 @ sk12 @ sk11)) != (rel_s4 @ sk8 @ sk9))),inference(paramod_ordered,[status(thm)],[17,408])).
% 8.28/3.65 thf(463,plain,(~ (sk1) | ((rel_s4 @ sk11 @ (sk10 @ sk11 @ sk12 @ sk11)) != (rel_s4 @ sk8 @ sk9))),inference(simp,[status(thm)],[462])).
% 8.28/3.65 thf(474,plain,(~ (sk1) | (sk11 != sk8) | ((sk10 @ sk11 @ sk12 @ sk11) != sk9)),inference(simp,[status(thm)],[463])).
% 8.28/3.65 thf(261,plain,(! [B:mu,A:$i] : (sk1 | (~ (rel_s4 @ sk3 @ A)) | ~ (($true)) | (rel_s4 @ A @ (sk4 @ B @ A)) | sk1 | ((exists_in_world @ sk6 @ sk5) != (exists_in_world @ B @ A)))),inference(paramod_ordered,[status(thm)],[15,22])).
% 8.28/3.65 thf(262,plain,(! [B:mu,A:$i] : (sk1 | (~ (rel_s4 @ sk3 @ A)) | (rel_s4 @ A @ (sk4 @ B @ A)) | ((exists_in_world @ sk6 @ sk5) != (exists_in_world @ B @ A)))),inference(simp,[status(thm)],[261])).
% 8.28/3.65 thf(263,plain,(sk1 | (~ (rel_s4 @ sk3 @ sk5)) | (rel_s4 @ sk5 @ (sk4 @ sk6 @ sk5))),inference(pattern_uni,[status(thm)],[262:[bind(A, $thf(sk5)),bind(B, $thf(sk6))]])).
% 8.28/3.65 thf(335,plain,(sk1 | sk1 | ~ (($true)) | (rel_s4 @ sk5 @ (sk4 @ sk6 @ sk5)) | ((rel_s4 @ sk3 @ sk5) != (rel_s4 @ sk3 @ sk5))),inference(paramod_ordered,[status(thm)],[14,263])).
% 8.28/3.65 thf(336,plain,(sk1 | (rel_s4 @ sk5 @ (sk4 @ sk6 @ sk5)) | ((rel_s4 @ sk3 @ sk5) != (rel_s4 @ sk3 @ sk5))),inference(simp,[status(thm)],[335])).
% 8.28/3.65 thf(337,plain,(sk1 | (rel_s4 @ sk5 @ (sk4 @ sk6 @ sk5))),inference(pattern_uni,[status(thm)],[336:[]])).
% 8.28/3.65 thf(384,plain,(sk1 | ~ (($true)) | sk1 | ((rel_s4 @ sk7 @ (sk4 @ sk6 @ sk5)) != (rel_s4 @ sk5 @ (sk4 @ sk6 @ sk5)))),inference(paramod_ordered,[status(thm)],[337,206])).
% 8.28/3.65 thf(385,plain,(sk1 | ((rel_s4 @ sk7 @ (sk4 @ sk6 @ sk5)) != (rel_s4 @ sk5 @ (sk4 @ sk6 @ sk5)))),inference(simp,[status(thm)],[384])).
% 8.28/3.65 thf(396,plain,(sk1 | (sk7 != sk5) | ((sk4 @ sk6 @ sk5) != (sk4 @ sk6 @ sk5))),inference(simp,[status(thm)],[385])).
% 8.28/3.65 thf(400,plain,(sk1 | (sk7 != sk5)),inference(simp,[status(thm)],[396])).
% 8.28/3.65 thf(222,plain,(sk1 | sk1 | ~ (($true)) | ((f @ sk6 @ (sk4 @ sk6 @ sk5)) != (f @ sk6 @ sk7))),inference(paramod_ordered,[status(thm)],[199,150])).
% 8.28/3.65 thf(223,plain,(sk1 | ((f @ sk6 @ (sk4 @ sk6 @ sk5)) != (f @ sk6 @ sk7))),inference(simp,[status(thm)],[222])).
% 8.28/3.65 thf(225,plain,(sk1 | (sk6 != sk6) | ((sk4 @ sk6 @ sk5) != sk7)),inference(simp,[status(thm)],[223])).
% 8.28/3.65 thf(227,plain,(sk1 | ((sk4 @ sk6 @ sk5) != sk7)),inference(simp,[status(thm)],[225])).
% 8.28/3.65 thf(734,plain,(($false)),inference(e,[status(thm)],[408,14,29,206,456,169,13,12,7,213,438,11,58,30,15,24,25,28,297,424,21,33,296,17,22,27,18,150,199,31,26,23,210,474,400,227,337])).
% 8.28/3.65 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.28/3.65 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------