%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : PHI045^9 : TPTP v9.3.1. Released v9.1.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:20:15 AM UTC 2026
% Result : Theorem 13.56s 4.23s
% Output : Refutation 12.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PHI045^9 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.10/0.21 % Computer : 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 13:23:12 UTC 2026
% 0.10/0.21 % CPUTime :
% 0.10/0.21 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.89/0.79 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.24/0.99 % [INFO] Parsing done (196ms).
% 1.24/1.01 % [INFO] Input problem is non-classical (logic $modal). Running HOL transformation from semantics specification contained in the problem file ...
% 1.71/1.15 % [INFO] Running in sequential loop mode.
% 2.43/1.52 % [INFO] eprover registered as external prover.
% 2.43/1.53 % [INFO] Scanning for conjecture ...
% 2.60/1.65 % [INFO] Found a conjecture (or negated_conjecture) and 4 axioms. Running axiom selection ...
% 2.60/1.68 % [INFO] Axiom selection finished. Selected 4 axioms (removed 0 axioms).
% 2.78/1.71 % [INFO] Problem is higher-order (TPTP THF).
% 2.78/1.72 % [INFO] Type checking passed.
% 2.78/1.72 % [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 ...
% 13.56/4.22 % External prover 'e' found a proof!
% 13.56/4.23 % [INFO] Killing All external provers ...
% 13.56/4.23 % Time passed: 3872ms (effective reasoning time: 3073ms)
% 13.56/4.23 % 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)>
% 13.56/4.23 % Axioms used in derivation (4): mrel_symmetric, axiomV1, axiomV4, axiomV2
% 13.56/4.23 % No. of inferences in proof: 110
% 13.56/4.23 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 3872 ms resp. 3073 ms w/o parsing
% 12.29/4.34 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.29/4.34 thf(individual_type, type, individual: $tType).
% 12.29/4.34 thf(mworld_type, type, mworld: $tType).
% 12.29/4.34 thf(mrel_decl, type, mrel: (mworld > (mworld > $o))).
% 12.29/4.34 thf(mbox_decl, type, mbox: ((mworld > $o) > (mworld > $o))).
% 12.29/4.34 thf(mactual_decl, type, mactual: mworld).
% 12.29/4.34 thf(mlocal_decl, type, mlocal: ((mworld > $o) > $o)).
% 12.29/4.34 thf(mglobal_decl, type, mglobal: ((mworld > $o) > $o)).
% 12.29/4.34 thf(positive_decl, type, positive: (mworld > ((individual > $o) > $o))).
% 12.29/4.34 thf(godlike_decl, type, godlike: (mworld > (individual > $o))).
% 12.29/4.34 thf(exists_decl, type, exists: (mworld > (individual > $o))).
% 12.29/4.34 thf(sk1_decl, type, sk1: (individual > (individual > $o))).
% 12.29/4.34 thf(sk2_decl, type, sk2: (individual > mworld)).
% 12.29/4.34 thf(sk3_decl, type, sk3: ((individual > $o) > ((individual > $o) > (mworld > mworld)))).
% 12.29/4.34 thf(sk4_decl, type, sk4: ((individual > $o) > ((individual > $o) > (mworld > individual)))).
% 12.29/4.34 thf(sk5_decl, type, sk5: (mworld > individual)).
% 12.29/4.34 thf(sk6_decl, type, sk6: individual).
% 12.29/4.34 thf(sk7_decl, type, sk7: (individual > individual)).
% 12.29/4.34 thf(mbox_def, definition, mbox = (^ [A:(mworld > $o),B:mworld]: ! [C:mworld]: ((mrel @ B @ C) => (A @ C))) ).
% 12.29/4.34 thf(mlocal_def, definition, mlocal = (^ [A:(mworld > $o)]: (A @ mactual)) ).
% 12.29/4.34 thf(mglobal_def, definition, mglobal = ((!) @ mworld) ).
% 12.29/4.34 thf(godlike_def, definition, godlike = (^ [A:mworld,B:individual]: ! [C:(individual > $o)]: ((positive @ A @ C) => (mbox @ (^ [D:mworld]: (C @ B)) @ A))) ).
% 12.29/4.34 thf(exists_def, definition, exists = (^ [A:mworld,B:individual]: ? [C:individual]: ((exists @ A @ C) & (B = C))) ).
% 12.29/4.34 thf(sk1_def, definition, sk1 = (^ [A:individual]: (@+ [B:(individual > $o)]: ~ ((positive @ mactual @ B) => ((? [C:mworld]: (mrel @ mactual @ C)) => (B @ A))))) ).
% 12.29/4.34 thf(sk2_def, definition, sk2 = (^ [A:individual]: (@+ [B:mworld]: (mrel @ mactual @ B))) ).
% 12.29/4.34 thf(sk3_def, definition, sk3 = (^ [A:(individual > $o),B:(individual > $o),C:mworld]: (@+ [D:mworld]: ~ ((mrel @ C @ D) => (! [E:individual]: ((exists @ D @ E) => ((B @ E) = (A @ E))))))) ).
% 12.29/4.34 thf(sk4_def, definition, sk4 = (^ [A:(individual > $o),B:(individual > $o),C:mworld]: (@+ [D:individual]: ~ ((exists @ (sk3 @ A @ B @ C) @ D) => ((B @ D) = (A @ D))))) ).
% 12.29/4.34 thf(1,conjecture,((mlocal @ (^ [A:mworld]: ? [B:individual]: ((exists @ A @ B) & (godlike @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',theoremV6)).
% 12.29/4.34 thf(2,negated_conjecture,((~ (mlocal @ (^ [A:mworld]: ? [B:individual]: ((exists @ A @ B) & (godlike @ A @ B)))))),inference(neg_conjecture,[status(cth)],[1])).
% 12.29/4.34 thf(7,plain,((~ (? [A:individual]: ((exists @ mactual @ A) & ! [B:(individual > $o)]: ((positive @ mactual @ (B)) => (! [C:mworld]: ((mrel @ mactual @ C) => (B @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 12.29/4.34 thf(8,plain,((~ (? [A:individual]: ((exists @ mactual @ A) & ! [B:(individual > $o)]: ((positive @ mactual @ (B)) => ((? [C:mworld]: (mrel @ mactual @ C)) => (B @ A))))))),inference(miniscope,[status(thm)],[7])).
% 12.29/4.34 thf(9,plain,(! [A:individual] : (((~ (exists @ mactual @ A) | (positive @ mactual @ (sk1 @ A))) & (~ (exists @ mactual @ A) | (mrel @ mactual @ (sk2 @ A))) & (~ (exists @ mactual @ A) | ~ (sk1 @ A @ A))))),inference(cnf,[status(esa)],[8])).
% 12.29/4.34 thf(10,plain,(! [A:individual] : ((~ (exists @ mactual @ A)) | (positive @ mactual @ (sk1 @ A)))),inference(cnfConj,[status(thm)],[9])).
% 12.29/4.34 thf(3,axiom,((! [A:mworld,B:mworld]: ((mrel @ A @ B) => (mrel @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mrel_symmetric)).
% 12.29/4.34 thf(13,plain,((! [A:mworld,B:mworld]: ((mrel @ A @ B) => (mrel @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 12.29/4.34 thf(14,plain,(! [B:mworld,A:mworld] : ((~ (mrel @ A @ B)) | (mrel @ B @ A))),inference(cnf,[status(esa)],[13])).
% 12.29/4.34 thf(4,axiom,((mglobal @ (^ [A:mworld]: ! [B:(individual > $o),C:(individual > $o)]: ((mbox @ (^ [D:mworld]: ! [E:individual]: ((exists @ D @ E) => ((B @ E) = (C @ E)))) @ A) => ((positive @ A @ B) = (positive @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiomV1)).
% 12.29/4.34 thf(15,plain,((! [A:mworld,B:(individual > $o),C:(individual > $o)]: ((! [D:mworld]: ((mrel @ A @ D) => (! [E:individual]: ((exists @ D @ E) => ((B @ E) = (C @ E)))))) => ((positive @ A @ (B)) = (positive @ A @ (C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 12.29/4.34 thf(16,plain,(! [C:(individual > $o),B:(individual > $o),A:mworld] : ((((mrel @ A @ (sk3 @ (C) @ (B) @ A)) | ((positive @ A @ (B)) = (positive @ A @ (C)))) & ((exists @ (sk3 @ (C) @ (B) @ A) @ (sk4 @ (C) @ (B) @ A)) | ((positive @ A @ (B)) = (positive @ A @ (C)))) & (~ ((B @ (sk4 @ (C) @ (B) @ A)) = (C @ (sk4 @ (C) @ (B) @ A))) | ((positive @ A @ (B)) = (positive @ A @ (C))))))),inference(cnf,[status(esa)],[15])).
% 12.29/4.34 thf(17,plain,(! [C:(individual > $o),B:(individual > $o),A:mworld] : ((mrel @ A @ (sk3 @ (C) @ (B) @ A)) | ((positive @ A @ (B)) = (positive @ A @ (C))))),inference(cnfConj,[status(thm)],[16])).
% 12.29/4.34 thf(20,plain,(! [C:(individual > $o),B:(individual > $o),A:mworld] : (((positive @ A @ (B)) = (positive @ A @ (C))) | (mrel @ A @ (sk3 @ (C) @ (B) @ A)))),inference(lifteq,[status(thm)],[17])).
% 12.29/4.34 thf(6,axiom,((mglobal @ (^ [A:mworld]: (positive @ A @ (^ [B:individual]: ((godlike @ A @ B) & (exists @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiomV4)).
% 12.29/4.34 thf(26,plain,((! [A:mworld]: (positive @ A @ (^ [B:individual]: (! [C:(individual > $o)]: ((positive @ A @ C) => (! [D:mworld]: ((mrel @ A @ D) => (C @ B)))) & (exists @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 12.29/4.34 thf(27,plain,(! [A:mworld] : ((positive @ A @ (^ [B:individual]: (! [C:(individual > $o)]: ((positive @ A @ C) => (! [D:mworld]: ((mrel @ A @ D) => (C @ B)))) & (exists @ A @ B)))))),inference(cnf,[status(esa)],[26])).
% 12.29/4.34 thf(5,axiom,((mglobal @ (^ [A:mworld]: ! [B:(individual > $o)]: ~ (positive @ A @ (^ [C:individual]: ((B @ C) & ~ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiomV2)).
% 12.29/4.34 thf(23,plain,((! [A:mworld]: ~ (positive @ A @ (^ [B:individual]: (($false)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 12.29/4.34 thf(24,plain,((~ (? [A:mworld]: (positive @ A @ (^ [B:individual]: (($false))))))),inference(miniscope,[status(thm)],[23])).
% 12.29/4.34 thf(25,plain,(! [A:mworld] : ((~ (positive @ A @ (^ [B:individual]: (($false))))))),inference(cnf,[status(esa)],[24])).
% 12.29/4.34 thf(28,plain,(! [B:mworld,A:mworld] : (~ (($true)) | ((positive @ A @ (^ [C:individual]: (! [D:(individual > $o)]: ((positive @ A @ D) => (! [E:mworld]: ((mrel @ A @ E) => (D @ C)))) & (exists @ A @ C)))) != (positive @ B @ (^ [C:individual]: (($false))))))),inference(paramod_ordered,[status(thm)],[27,25])).
% 12.29/4.34 thf(29,plain,(! [B:mworld,A:mworld] : (((positive @ A @ (^ [C:individual]: (! [D:(individual > $o)]: ((positive @ A @ D) => (! [E:mworld]: ((mrel @ A @ E) => (D @ C)))) & (exists @ A @ C)))) != (positive @ B @ (^ [C:individual]: (($false))))))),inference(simp,[status(thm)],[28])).
% 12.29/4.34 thf(30,plain,(! [B:mworld,A:mworld] : ((A != B) | ((^ [C:individual]: (! [D:(individual > $o)]: ((positive @ A @ D) => (! [E:mworld]: ((mrel @ A @ E) => (D @ C)))) & (exists @ A @ C))) != (^ [C:individual]: (($false)))))),inference(simp,[status(thm)],[29])).
% 12.29/4.34 thf(31,plain,(! [A:mworld] : (((^ [B:individual]: (! [C:(individual > $o)]: ((positive @ A @ C) => (! [D:mworld]: ((mrel @ A @ D) => (C @ B)))) & (exists @ A @ B))) != (^ [B:individual]: (($false)))))),inference(simp,[status(thm)],[30])).
% 12.29/4.34 thf(32,plain,(! [A:mworld] : ((! [B:(individual > $o)]: ((positive @ A @ (B)) => (! [C:mworld]: ((mrel @ A @ C) => (B @ (sk5 @ A))))) & (exists @ A @ (sk5 @ A))))),inference(func_ext,[status(esa)],[31])).
% 12.29/4.34 thf(33,plain,(! [C:mworld,B:(individual > $o),A:mworld] : (((~ (positive @ A @ (B)) | ~ (mrel @ A @ C) | (B @ (sk5 @ A))) & (exists @ A @ (sk5 @ A))))),inference(cnf,[status(esa)],[32])).
% 12.29/4.34 thf(35,plain,(! [A:mworld] : ((exists @ A @ (sk5 @ A)))),inference(cnfConj,[status(thm)],[33])).
% 12.29/4.34 thf(67,plain,(! [B:individual,A:mworld] : (~ (($true)) | (positive @ mactual @ (sk1 @ B)) | ((exists @ A @ (sk5 @ A)) != (exists @ mactual @ B)))),inference(paramod_ordered,[status(thm)],[35,10])).
% 12.29/4.34 thf(68,plain,(! [B:individual,A:mworld] : ((positive @ mactual @ (sk1 @ B)) | ((exists @ A @ (sk5 @ A)) != (exists @ mactual @ B)))),inference(simp,[status(thm)],[67])).
% 12.29/4.34 thf(69,plain,((positive @ mactual @ (sk1 @ (sk5 @ mactual)))),inference(pattern_uni,[status(thm)],[68:[bind(A, $thf(mactual)),bind(B, $thf(sk5 @ mactual))]])).
% 12.29/4.34 thf(76,plain,(! [A:mworld] : (~ (($true)) | ((positive @ mactual @ (sk1 @ (sk5 @ mactual))) != (positive @ A @ (^ [B:individual]: (($false))))))),inference(paramod_ordered,[status(thm)],[69,25])).
% 12.29/4.34 thf(77,plain,(! [A:mworld] : (((positive @ mactual @ (sk1 @ (sk5 @ mactual))) != (positive @ A @ (^ [B:individual]: (($false))))))),inference(simp,[status(thm)],[76])).
% 12.29/4.34 thf(86,plain,(! [A:mworld] : ((mactual != A) | ((sk1 @ (sk5 @ mactual)) != (^ [B:individual]: (($false)))))),inference(simp,[status(thm)],[77])).
% 12.29/4.34 thf(90,plain,(((sk1 @ (sk5 @ mactual)) != (^ [A:individual]: (($false))))),inference(simp,[status(thm)],[86])).
% 12.29/4.34 thf(95,plain,((sk1 @ (sk5 @ mactual) @ sk6)),inference(func_ext,[status(esa)],[90])).
% 12.29/4.34 thf(12,plain,(! [A:individual] : ((~ (exists @ mactual @ A)) | (~ (sk1 @ A @ A)))),inference(cnfConj,[status(thm)],[9])).
% 12.29/4.34 thf(36,plain,(! [B:individual,A:mworld] : (~ (($true)) | (~ (sk1 @ B @ B)) | ((exists @ A @ (sk5 @ A)) != (exists @ mactual @ B)))),inference(paramod_ordered,[status(thm)],[35,12])).
% 12.29/4.34 thf(37,plain,(! [B:individual,A:mworld] : ((~ (sk1 @ B @ B)) | ((exists @ A @ (sk5 @ A)) != (exists @ mactual @ B)))),inference(simp,[status(thm)],[36])).
% 12.29/4.34 thf(38,plain,((~ (sk1 @ (sk5 @ mactual) @ (sk5 @ mactual)))),inference(pattern_uni,[status(thm)],[37:[bind(A, $thf(mactual)),bind(B, $thf(sk5 @ mactual))]])).
% 12.29/4.34 thf(96,plain,(~ (($true)) | ((sk1 @ (sk5 @ mactual) @ (sk5 @ mactual)) != (sk1 @ (sk5 @ mactual) @ sk6))),inference(paramod_ordered,[status(thm)],[95,38])).
% 12.29/4.34 thf(97,plain,(((sk1 @ (sk5 @ mactual) @ (sk5 @ mactual)) != (sk1 @ (sk5 @ mactual) @ sk6))),inference(simp,[status(thm)],[96])).
% 12.29/4.34 thf(100,plain,(((sk5 @ mactual) != (sk5 @ mactual)) | ((sk5 @ mactual) != sk6)),inference(simp,[status(thm)],[97])).
% 12.29/4.34 thf(102,plain,(((sk5 @ mactual) != sk6)),inference(simp,[status(thm)],[100])).
% 12.29/4.34 thf(57,plain,(! [B:mworld,A:individual] : ((~ (exists @ mactual @ A)) | ~ (($true)) | ((positive @ mactual @ (sk1 @ A)) != (positive @ B @ (^ [C:individual]: (($false))))))),inference(paramod_ordered,[status(thm)],[10,25])).
% 12.29/4.34 thf(58,plain,(! [B:mworld,A:individual] : ((~ (exists @ mactual @ A)) | ((positive @ mactual @ (sk1 @ A)) != (positive @ B @ (^ [C:individual]: (($false))))))),inference(simp,[status(thm)],[57])).
% 12.29/4.34 thf(70,plain,(! [B:mworld,A:individual] : ((~ (exists @ mactual @ A)) | (mactual != B) | ((sk1 @ A) != (^ [C:individual]: (($false)))))),inference(simp,[status(thm)],[58])).
% 12.29/4.34 thf(73,plain,(! [A:individual] : ((~ (exists @ mactual @ A)) | ((sk1 @ A) != (^ [B:individual]: (($false)))))),inference(simp,[status(thm)],[70])).
% 12.29/4.34 thf(106,plain,(! [A:individual] : ((sk1 @ A @ (sk7 @ A)) | (~ (exists @ mactual @ A)))),inference(func_ext,[status(esa)],[73])).
% 12.29/4.34 thf(127,plain,(! [B:individual,A:individual] : ((~ (exists @ mactual @ A)) | (~ (exists @ mactual @ B)) | ~ (($true)) | ((sk1 @ A @ (sk7 @ A)) != (sk1 @ B @ B)))),inference(paramod_ordered,[status(thm)],[106,12])).
% 12.29/4.34 thf(128,plain,(! [B:individual,A:individual] : ((~ (exists @ mactual @ A)) | (~ (exists @ mactual @ B)) | ((sk1 @ A @ (sk7 @ A)) != (sk1 @ B @ B)))),inference(simp,[status(thm)],[127])).
% 12.29/4.34 thf(133,plain,(! [B:individual,A:individual] : ((~ (exists @ mactual @ A)) | (~ (exists @ mactual @ B)) | (A != B) | ((sk7 @ A) != B))),inference(simp,[status(thm)],[128])).
% 12.29/4.34 thf(135,plain,(! [A:individual] : ((~ (exists @ mactual @ A)) | (~ (exists @ mactual @ A)) | ((sk7 @ A) != A))),inference(simp,[status(thm)],[133])).
% 12.29/4.34 thf(256,plain,(! [A:individual] : ((~ (exists @ mactual @ A)) | ((sk7 @ A) != A))),inference(simp,[status(thm)],[135])).
% 12.29/4.34 thf(34,plain,(! [C:mworld,B:(individual > $o),A:mworld] : ((~ (positive @ A @ (B))) | (~ (mrel @ A @ C)) | (B @ (sk5 @ A)))),inference(cnfConj,[status(thm)],[33])).
% 12.29/4.34 thf(11,plain,(! [A:individual] : ((~ (exists @ mactual @ A)) | (mrel @ mactual @ (sk2 @ A)))),inference(cnfConj,[status(thm)],[9])).
% 12.29/4.34 thf(80,plain,(! [C:(individual > $o),B:(individual > $o),A:mworld] : ((positive @ A @ (B)) | (mrel @ A @ (sk3 @ (C) @ (B) @ A)) | ((positive @ mactual @ (sk1 @ (sk5 @ mactual))) != (positive @ A @ (C))))),inference(paramod_ordered,[status(thm)],[69,20])).
% 12.29/4.34 thf(81,plain,(! [A:(individual > $o)] : ((positive @ mactual @ (A)) | (mrel @ mactual @ (sk3 @ (sk1 @ (sk5 @ mactual)) @ (A) @ mactual)))),inference(pattern_uni,[status(thm)],[80:[bind(A, $thf(mactual)),bind(B, $thf(B)),bind(C, $thf(sk1 @ (sk5 @ mactual)))]])).
% 12.29/4.34 thf(87,plain,(! [A:(individual > $o)] : ((positive @ mactual @ (A)) | (mrel @ mactual @ (sk3 @ (sk1 @ (sk5 @ mactual)) @ (A) @ mactual)))),inference(simp,[status(thm)],[81])).
% 12.29/4.34 thf(145,plain,(! [C:mworld,B:mworld,A:(individual > $o)] : ((positive @ mactual @ (A)) | ~ (($true)) | (mrel @ C @ B) | ((mrel @ mactual @ (sk3 @ (sk1 @ (sk5 @ mactual)) @ (A) @ mactual)) != (mrel @ B @ C)))),inference(paramod_ordered,[status(thm)],[87,14])).
% 12.29/4.34 thf(146,plain,(! [C:mworld,B:mworld,A:(individual > $o)] : ((positive @ mactual @ (A)) | (mrel @ C @ B) | ((mrel @ mactual @ (sk3 @ (sk1 @ (sk5 @ mactual)) @ (A) @ mactual)) != (mrel @ B @ C)))),inference(simp,[status(thm)],[145])).
% 12.29/4.34 thf(147,plain,(! [A:(individual > $o)] : ((positive @ mactual @ (A)) | (mrel @ (sk3 @ (sk1 @ (sk5 @ mactual)) @ (A) @ mactual) @ mactual))),inference(pattern_uni,[status(thm)],[146:[bind(A, $thf(E)),bind(B, $thf(mactual)),bind(C, $thf(sk3 @ (sk1 @ (sk5 @ mactual)) @ (E) @ mactual))]])).
% 12.29/4.34 thf(151,plain,(! [A:(individual > $o)] : ((positive @ mactual @ (A)) | (mrel @ (sk3 @ (sk1 @ (sk5 @ mactual)) @ (A) @ mactual) @ mactual))),inference(simp,[status(thm)],[147])).
% 12.29/4.34 thf(92,plain,(! [B:individual,A:mworld] : (~ (($true)) | (mrel @ mactual @ (sk2 @ B)) | ((exists @ A @ (sk5 @ A)) != (exists @ mactual @ B)))),inference(paramod_ordered,[status(thm)],[35,11])).
% 12.29/4.34 thf(93,plain,(! [B:individual,A:mworld] : ((mrel @ mactual @ (sk2 @ B)) | ((exists @ A @ (sk5 @ A)) != (exists @ mactual @ B)))),inference(simp,[status(thm)],[92])).
% 12.29/4.34 thf(94,plain,((mrel @ mactual @ (sk2 @ (sk5 @ mactual)))),inference(pattern_uni,[status(thm)],[93:[bind(A, $thf(mactual)),bind(B, $thf(sk5 @ mactual))]])).
% 12.29/4.34 thf(82,plain,(! [C:(individual > $o),B:(individual > $o),A:mworld] : ((mrel @ A @ (sk3 @ (C) @ (B) @ A)) | (positive @ A @ (C)) | ((positive @ A @ (B)) != (positive @ mactual @ (sk1 @ (sk5 @ mactual)))))),inference(paramod_ordered,[status(thm)],[20,69])).
% 12.29/4.34 thf(83,plain,(! [A:(individual > $o)] : ((mrel @ mactual @ (sk3 @ (A) @ (sk1 @ (sk5 @ mactual)) @ mactual)) | (positive @ mactual @ (A)))),inference(pattern_uni,[status(thm)],[82:[bind(A, $thf(mactual)),bind(B, $thf(sk1 @ (sk5 @ mactual))),bind(C, $thf(C))]])).
% 12.29/4.34 thf(88,plain,(! [A:(individual > $o)] : ((mrel @ mactual @ (sk3 @ (A) @ (sk1 @ (sk5 @ mactual)) @ mactual)) | (positive @ mactual @ (A)))),inference(simp,[status(thm)],[83])).
% 12.29/4.34 thf(174,plain,(! [C:mworld,B:mworld,A:(individual > $o)] : ((positive @ mactual @ (A)) | ~ (($true)) | (mrel @ C @ B) | ((mrel @ mactual @ (sk3 @ (A) @ (sk1 @ (sk5 @ mactual)) @ mactual)) != (mrel @ B @ C)))),inference(paramod_ordered,[status(thm)],[88,14])).
% 12.29/4.34 thf(175,plain,(! [C:mworld,B:mworld,A:(individual > $o)] : ((positive @ mactual @ (A)) | (mrel @ C @ B) | ((mrel @ mactual @ (sk3 @ (A) @ (sk1 @ (sk5 @ mactual)) @ mactual)) != (mrel @ B @ C)))),inference(simp,[status(thm)],[174])).
% 12.29/4.34 thf(176,plain,(! [A:(individual > $o)] : ((positive @ mactual @ (A)) | (mrel @ (sk3 @ (A) @ (sk1 @ (sk5 @ mactual)) @ mactual) @ mactual))),inference(pattern_uni,[status(thm)],[175:[bind(A, $thf(D)),bind(B, $thf(mactual)),bind(C, $thf(sk3 @ (D) @ (sk1 @ (sk5 @ mactual)) @ mactual))]])).
% 12.29/4.34 thf(185,plain,(! [A:(individual > $o)] : ((positive @ mactual @ (A)) | (mrel @ (sk3 @ (A) @ (sk1 @ (sk5 @ mactual)) @ mactual) @ mactual))),inference(simp,[status(thm)],[176])).
% 12.29/4.34 thf(113,plain,(! [D:(individual > $o),C:(individual > $o),B:mworld,A:(individual > $o)] : ((mrel @ mactual @ (sk3 @ (sk1 @ (sk5 @ mactual)) @ (A) @ mactual)) | (positive @ B @ (D)) | (mrel @ B @ (sk3 @ (D) @ (C) @ B)) | ((positive @ mactual @ (A)) != (positive @ B @ (C))))),inference(paramod_ordered,[status(thm)],[87,20])).
% 12.29/4.34 thf(114,plain,(! [B:(individual > $o),A:(individual > $o)] : ((mrel @ mactual @ (sk3 @ (sk1 @ (sk5 @ mactual)) @ (A) @ mactual)) | (positive @ mactual @ (B)) | (mrel @ mactual @ (sk3 @ (B) @ (A) @ mactual)))),inference(pattern_uni,[status(thm)],[113:[bind(A, $thf(A)),bind(B, $thf(mactual)),bind(C, $thf(A))]])).
% 12.29/4.34 thf(121,plain,(! [B:(individual > $o),A:(individual > $o)] : ((mrel @ mactual @ (sk3 @ (sk1 @ (sk5 @ mactual)) @ (A) @ mactual)) | (positive @ mactual @ (B)) | (mrel @ mactual @ (sk3 @ (B) @ (A) @ mactual)))),inference(simp,[status(thm)],[114])).
% 12.29/4.34 thf(171,plain,(! [B:mworld,A:(individual > $o)] : ((mrel @ mactual @ (sk3 @ (A) @ (sk1 @ (sk5 @ mactual)) @ mactual)) | ~ (($true)) | ((positive @ mactual @ (A)) != (positive @ B @ (^ [C:individual]: (($false))))))),inference(paramod_ordered,[status(thm)],[88,25])).
% 12.29/4.34 thf(172,plain,(! [B:mworld,A:(individual > $o)] : ((mrel @ mactual @ (sk3 @ (A) @ (sk1 @ (sk5 @ mactual)) @ mactual)) | ((positive @ mactual @ (A)) != (positive @ B @ (^ [C:individual]: (($false))))))),inference(simp,[status(thm)],[171])).
% 12.29/4.34 thf(173,plain,((mrel @ mactual @ (sk3 @ (^ [A:individual]: (($false))) @ (sk1 @ (sk5 @ mactual)) @ mactual))),inference(pattern_uni,[status(thm)],[172:[bind(A, $thf(^ [C:individual]: (($false)))),bind(B, $thf(mactual))]])).
% 12.29/4.34 thf(190,plain,(! [B:mworld,A:mworld] : (~ (($true)) | (mrel @ B @ A) | ((mrel @ mactual @ (sk3 @ (^ [C:individual]: (($false))) @ (sk1 @ (sk5 @ mactual)) @ mactual)) != (mrel @ A @ B)))),inference(paramod_ordered,[status(thm)],[173,14])).
% 12.29/4.34 thf(191,plain,(! [B:mworld,A:mworld] : ((mrel @ B @ A) | ((mrel @ mactual @ (sk3 @ (^ [C:individual]: (($false))) @ (sk1 @ (sk5 @ mactual)) @ mactual)) != (mrel @ A @ B)))),inference(simp,[status(thm)],[190])).
% 12.29/4.34 thf(192,plain,((mrel @ (sk3 @ (^ [A:individual]: (($false))) @ (sk1 @ (sk5 @ mactual)) @ mactual) @ mactual)),inference(pattern_uni,[status(thm)],[191:[bind(A, $thf(mactual)),bind(B, $thf(sk3 @ (^ [C:individual]: (($false))) @ (sk1 @ (sk5 @ mactual)) @ mactual))]])).
% 12.29/4.34 thf(18,plain,(! [C:(individual > $o),B:(individual > $o),A:mworld] : ((exists @ (sk3 @ (C) @ (B) @ A) @ (sk4 @ (C) @ (B) @ A)) | ((positive @ A @ (B)) = (positive @ A @ (C))))),inference(cnfConj,[status(thm)],[16])).
% 12.29/4.34 thf(21,plain,(! [C:(individual > $o),B:(individual > $o),A:mworld] : (((positive @ A @ (B)) = (positive @ A @ (C))) | (exists @ (sk3 @ (C) @ (B) @ A) @ (sk4 @ (C) @ (B) @ A)))),inference(lifteq,[status(thm)],[18])).
% 12.29/4.34 thf(19,plain,(! [C:(individual > $o),B:(individual > $o),A:mworld] : ((~ ((B @ (sk4 @ (C) @ (B) @ A)) = (C @ (sk4 @ (C) @ (B) @ A)))) | ((positive @ A @ (B)) = (positive @ A @ (C))))),inference(cnfConj,[status(thm)],[16])).
% 12.29/4.34 thf(22,plain,(! [C:(individual > $o),B:(individual > $o),A:mworld] : (((B @ (sk4 @ (C) @ (B) @ A)) != (C @ (sk4 @ (C) @ (B) @ A))) | ((positive @ A @ (B)) = (positive @ A @ (C))))),inference(lifteq,[status(thm)],[19])).
% 12.29/4.34 thf(110,plain,(! [B:mworld,A:(individual > $o)] : ((mrel @ mactual @ (sk3 @ (sk1 @ (sk5 @ mactual)) @ (A) @ mactual)) | ~ (($true)) | ((positive @ mactual @ (A)) != (positive @ B @ (^ [C:individual]: (($false))))))),inference(paramod_ordered,[status(thm)],[87,25])).
% 12.29/4.34 thf(111,plain,(! [B:mworld,A:(individual > $o)] : ((mrel @ mactual @ (sk3 @ (sk1 @ (sk5 @ mactual)) @ (A) @ mactual)) | ((positive @ mactual @ (A)) != (positive @ B @ (^ [C:individual]: (($false))))))),inference(simp,[status(thm)],[110])).
% 12.29/4.34 thf(112,plain,((mrel @ mactual @ (sk3 @ (sk1 @ (sk5 @ mactual)) @ (^ [A:individual]: (($false))) @ mactual))),inference(pattern_uni,[status(thm)],[111:[bind(A, $thf(^ [C:individual]: (($false)))),bind(B, $thf(mactual))]])).
% 12.29/4.34 thf(142,plain,(! [B:mworld,A:mworld] : (~ (($true)) | (mrel @ B @ A) | ((mrel @ mactual @ (sk3 @ (sk1 @ (sk5 @ mactual)) @ (^ [C:individual]: (($false))) @ mactual)) != (mrel @ A @ B)))),inference(paramod_ordered,[status(thm)],[112,14])).
% 12.29/4.34 thf(143,plain,(! [B:mworld,A:mworld] : ((mrel @ B @ A) | ((mrel @ mactual @ (sk3 @ (sk1 @ (sk5 @ mactual)) @ (^ [C:individual]: (($false))) @ mactual)) != (mrel @ A @ B)))),inference(simp,[status(thm)],[142])).
% 12.29/4.34 thf(144,plain,((mrel @ (sk3 @ (sk1 @ (sk5 @ mactual)) @ (^ [A:individual]: (($false))) @ mactual) @ mactual)),inference(pattern_uni,[status(thm)],[143:[bind(A, $thf(mactual)),bind(B, $thf(sk3 @ (sk1 @ (sk5 @ mactual)) @ (^ [C:individual]: (($false))) @ mactual))]])).
% 12.29/4.34 thf(129,plain,(! [B:individual,A:mworld] : ((sk1 @ B @ (sk7 @ B)) | ~ (($true)) | ((exists @ A @ (sk5 @ A)) != (exists @ mactual @ B)))),inference(paramod_ordered,[status(thm)],[35,106])).
% 12.29/4.34 thf(130,plain,(! [B:individual,A:mworld] : ((sk1 @ B @ (sk7 @ B)) | ((exists @ A @ (sk5 @ A)) != (exists @ mactual @ B)))),inference(simp,[status(thm)],[129])).
% 12.29/4.34 thf(131,plain,((sk1 @ (sk5 @ mactual) @ (sk7 @ (sk5 @ mactual)))),inference(pattern_uni,[status(thm)],[130:[bind(A, $thf(mactual)),bind(B, $thf(sk5 @ mactual))]])).
% 12.29/4.34 thf(156,plain,(~ (($true)) | ((sk1 @ (sk5 @ mactual) @ (sk7 @ (sk5 @ mactual))) != (sk1 @ (sk5 @ mactual) @ (sk5 @ mactual)))),inference(paramod_ordered,[status(thm)],[131,38])).
% 12.29/4.34 thf(157,plain,(((sk1 @ (sk5 @ mactual) @ (sk7 @ (sk5 @ mactual))) != (sk1 @ (sk5 @ mactual) @ (sk5 @ mactual)))),inference(simp,[status(thm)],[156])).
% 12.29/4.34 thf(160,plain,(((sk5 @ mactual) != (sk5 @ mactual)) | ((sk7 @ (sk5 @ mactual)) != (sk5 @ mactual))),inference(simp,[status(thm)],[157])).
% 12.29/4.34 thf(162,plain,(((sk7 @ (sk5 @ mactual)) != (sk5 @ mactual))),inference(simp,[status(thm)],[160])).
% 12.29/4.34 thf(148,plain,(! [B:mworld,A:mworld] : (~ (($true)) | (mrel @ B @ A) | ((mrel @ mactual @ (sk2 @ (sk5 @ mactual))) != (mrel @ A @ B)))),inference(paramod_ordered,[status(thm)],[94,14])).
% 12.29/4.34 thf(149,plain,(! [B:mworld,A:mworld] : ((mrel @ B @ A) | ((mrel @ mactual @ (sk2 @ (sk5 @ mactual))) != (mrel @ A @ B)))),inference(simp,[status(thm)],[148])).
% 12.29/4.34 thf(150,plain,((mrel @ (sk2 @ (sk5 @ mactual)) @ mactual)),inference(pattern_uni,[status(thm)],[149:[bind(A, $thf(mactual)),bind(B, $thf(sk2 @ (sk5 @ mactual)))]])).
% 12.29/4.34 thf(337,plain,(! [C:mworld,B:(individual > $o),A:mworld] : ((~ (positive @ A @ (B))) | (~ (mrel @ A @ C)) | ~ (($true)) | ((B @ (sk5 @ A)) != (sk1 @ (sk5 @ mactual) @ (sk5 @ mactual))))),inference(paramod_ordered,[status(thm)],[34,38])).
% 12.29/4.34 thf(338,plain,(! [C:mworld,B:(individual > $o),A:mworld] : ((~ (positive @ A @ (B))) | (~ (mrel @ A @ C)) | ((B @ (sk5 @ A)) != (sk1 @ (sk5 @ mactual) @ (sk5 @ mactual))))),inference(simp,[status(thm)],[337])).
% 12.29/4.34 thf(386,plain,(! [A:mworld] : ((~ (positive @ mactual @ (^ [B:individual]: (sk1 @ B @ B)))) | (~ (mrel @ mactual @ A)))),inference(pre_uni,[status(thm)],[338:[bind(A, $thf(mactual)),bind(B, $thf(^ [D:individual]: (sk1 @ D @ D))),bind(C, $thf(C))]])).
% 12.29/4.34 thf(396,plain,(! [A:mworld] : ((~ (positive @ mactual @ (^ [B:individual]: (sk1 @ B @ B)))) | (~ (mrel @ mactual @ A)))),inference(simp,[status(thm)],[386])).
% 12.29/4.34 thf(500,plain,(! [A:mworld] : ((~ (positive @ mactual @ (^ [B:individual]: (sk1 @ B @ B)))) | ~ (($true)) | ((mrel @ mactual @ (sk3 @ (^ [B:individual]: (($false))) @ (sk1 @ (sk5 @ mactual)) @ mactual)) != (mrel @ mactual @ A)))),inference(paramod_ordered,[status(thm)],[173,396])).
% 12.29/4.34 thf(501,plain,(! [A:mworld] : ((~ (positive @ mactual @ (^ [B:individual]: (sk1 @ B @ B)))) | ((mrel @ mactual @ (sk3 @ (^ [B:individual]: (($false))) @ (sk1 @ (sk5 @ mactual)) @ mactual)) != (mrel @ mactual @ A)))),inference(simp,[status(thm)],[500])).
% 12.29/4.34 thf(502,plain,((~ (positive @ mactual @ (^ [A:individual]: (sk1 @ A @ A))))),inference(pattern_uni,[status(thm)],[501:[bind(A, $thf(sk3 @ (^ [B:individual]: (($false))) @ (sk1 @ (sk5 @ mactual)) @ mactual))]])).
% 12.29/4.34 thf(721,plain,(($false)),inference(e,[status(thm)],[10,14,20,102,256,73,34,7,35,11,87,151,94,90,69,88,185,25,106,121,38,192,21,173,13,22,27,12,144,162,112,150,95,502,31,26,23,131,15])).
% 12.29/4.34 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.29/4.34 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------