%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : PHI046^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 : n020.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 10.20s 3.42s
% Output : Refutation 10.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PHI046^9 : TPTP v9.3.1. Released v9.1.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.08/0.19 % Computer : n020.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 13:21:19 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.20 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.87/0.78 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.21/0.97 % [INFO] Parsing done (189ms).
% 1.21/1.00 % [INFO] Input problem is non-classical (logic $modal). Running HOL transformation from semantics specification contained in the problem file ...
% 1.69/1.13 % [INFO] Running in sequential loop mode.
% 2.44/1.51 % [INFO] eprover registered as external prover.
% 2.44/1.52 % [INFO] Scanning for conjecture ...
% 2.61/1.64 % [INFO] Found a conjecture (or negated_conjecture) and 4 axioms. Running axiom selection ...
% 2.61/1.67 % [INFO] Axiom selection finished. Selected 4 axioms (removed 0 axioms).
% 2.83/1.70 % [INFO] Problem is higher-order (TPTP THF).
% 2.83/1.71 % [INFO] Type checking passed.
% 2.83/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 ...
% 10.20/3.41 % External prover 'e' found a proof!
% 10.20/3.41 % [INFO] Killing All external provers ...
% 10.20/3.41 % Time passed: 3073ms (effective reasoning time: 2275ms)
% 10.20/3.41 % 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)>
% 10.20/3.42 % Axioms used in derivation (4): axiomV1, axiomV4, axiomV2, mrel_symmetric
% 10.20/3.42 % No. of inferences in proof: 98
% 10.20/3.42 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 3073 ms resp. 2275 ms w/o parsing
% 10.20/3.47 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.20/3.47 thf(individual_type, type, individual: $tType).
% 10.20/3.47 thf(mworld_type, type, mworld: $tType).
% 10.20/3.47 thf(mrel_decl, type, mrel: (mworld > (mworld > $o))).
% 10.20/3.47 thf(mbox_decl, type, mbox: ((mworld > $o) > (mworld > $o))).
% 10.20/3.47 thf(mactual_decl, type, mactual: mworld).
% 10.20/3.47 thf(mlocal_decl, type, mlocal: ((mworld > $o) > $o)).
% 10.20/3.47 thf(mglobal_decl, type, mglobal: ((mworld > $o) > $o)).
% 10.20/3.47 thf(positive_decl, type, positive: (mworld > ((individual > $o) > $o))).
% 10.20/3.47 thf(godlike_decl, type, godlike: (mworld > (individual > $o))).
% 10.20/3.47 thf(exists_decl, type, exists: (mworld > (individual > $o))).
% 10.20/3.47 thf(sk1_decl, type, sk1: mworld).
% 10.20/3.47 thf(sk2_decl, type, sk2: (individual > (individual > $o))).
% 10.20/3.47 thf(sk3_decl, type, sk3: (individual > mworld)).
% 10.20/3.47 thf(sk4_decl, type, sk4: ((individual > $o) > ((individual > $o) > (mworld > mworld)))).
% 10.20/3.47 thf(sk5_decl, type, sk5: ((individual > $o) > ((individual > $o) > (mworld > individual)))).
% 10.20/3.47 thf(sk6_decl, type, sk6: (mworld > individual)).
% 10.20/3.47 thf(sk7_decl, type, sk7: individual).
% 10.20/3.47 thf(sk9_decl, type, sk9: individual).
% 10.20/3.47 thf(sk10_decl, type, sk10: individual).
% 10.20/3.47 thf(sk11_decl, type, sk11: individual).
% 10.20/3.47 thf(mbox_def, definition, mbox = (^ [A:(mworld > $o),B:mworld]: ! [C:mworld]: ((mrel @ B @ C) => (A @ C))) ).
% 10.20/3.47 thf(mlocal_def, definition, mlocal = (^ [A:(mworld > $o)]: (A @ mactual)) ).
% 10.20/3.47 thf(mglobal_def, definition, mglobal = ((!) @ mworld) ).
% 10.20/3.47 thf(godlike_def, definition, godlike = (^ [A:mworld,B:individual]: ! [C:(individual > $o)]: ((positive @ A @ C) => (mbox @ (^ [D:mworld]: (C @ B)) @ A))) ).
% 10.20/3.47 thf(exists_def, definition, exists = (^ [A:mworld,B:individual]: ? [C:individual]: ((exists @ A @ C) & (B = C))) ).
% 10.20/3.47 thf(sk1_def, definition, sk1 = (@+ [A:mworld]: ~ ((mrel @ mactual @ A) => (? [B:individual]: ((exists @ A @ B) & ! [C:(individual > $o)]: ((positive @ A @ (C)) => ((? [D:mworld]: (mrel @ A @ D)) => (C @ B))))))) ).
% 10.20/3.47 thf(sk2_def, definition, sk2 = (^ [A:individual]: (@+ [B:(individual > $o)]: ~ ((positive @ sk1 @ B) => ((? [C:mworld]: (mrel @ sk1 @ C)) => (B @ A))))) ).
% 10.20/3.47 thf(sk3_def, definition, sk3 = (^ [A:individual]: (@+ [B:mworld]: (mrel @ sk1 @ B))) ).
% 10.20/3.47 thf(sk4_def, definition, sk4 = (^ [A:(individual > $o),B:(individual > $o),C:mworld]: (@+ [D:mworld]: ~ ((mrel @ C @ D) => (! [E:individual]: ((exists @ D @ E) => ((B @ E) = (A @ E))))))) ).
% 10.20/3.47 thf(sk5_def, definition, sk5 = (^ [A:(individual > $o),B:(individual > $o),C:mworld]: (@+ [D:individual]: ~ ((exists @ (sk4 @ A @ B @ C) @ D) => ((B @ D) = (A @ D))))) ).
% 10.20/3.47 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)).
% 10.20/3.47 thf(16,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])).
% 10.20/3.47 thf(17,plain,(! [C:(individual > $o),B:(individual > $o),A:mworld] : ((((mrel @ A @ (sk4 @ (C) @ (B) @ A)) | ((positive @ A @ (B)) = (positive @ A @ (C)))) & ((exists @ (sk4 @ (C) @ (B) @ A) @ (sk5 @ (C) @ (B) @ A)) | ((positive @ A @ (B)) = (positive @ A @ (C)))) & (~ ((B @ (sk5 @ (C) @ (B) @ A)) = (C @ (sk5 @ (C) @ (B) @ A))) | ((positive @ A @ (B)) = (positive @ A @ (C))))))),inference(cnf,[status(esa)],[16])).
% 10.20/3.47 thf(18,plain,(! [C:(individual > $o),B:(individual > $o),A:mworld] : ((mrel @ A @ (sk4 @ (C) @ (B) @ A)) | ((positive @ A @ (B)) = (positive @ A @ (C))))),inference(cnfConj,[status(thm)],[17])).
% 10.20/3.47 thf(21,plain,(! [C:(individual > $o),B:(individual > $o),A:mworld] : (((positive @ A @ (B)) = (positive @ A @ (C))) | (mrel @ A @ (sk4 @ (C) @ (B) @ A)))),inference(lifteq,[status(thm)],[18])).
% 10.20/3.47 thf(6,axiom,((mglobal @ (^ [A:mworld]: (positive @ A @ (^ [B:individual]: ((godlike @ A @ B) & (exists @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiomV4)).
% 10.20/3.47 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(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 10.20/3.47 thf(28,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)],[27])).
% 10.20/3.47 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)).
% 10.20/3.47 thf(24,plain,((! [A:mworld]: ~ (positive @ A @ (^ [B:individual]: (($false)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 10.20/3.47 thf(25,plain,((~ (? [A:mworld]: (positive @ A @ (^ [B:individual]: (($false))))))),inference(miniscope,[status(thm)],[24])).
% 10.20/3.47 thf(26,plain,(! [A:mworld] : ((~ (positive @ A @ (^ [B:individual]: (($false))))))),inference(cnf,[status(esa)],[25])).
% 10.20/3.47 thf(29,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)],[28,26])).
% 10.20/3.47 thf(30,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)],[29])).
% 10.20/3.47 thf(31,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)],[30])).
% 10.20/3.47 thf(32,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)],[31])).
% 10.20/3.47 thf(33,plain,(! [A:mworld] : ((! [B:(individual > $o)]: ((positive @ A @ (B)) => (! [C:mworld]: ((mrel @ A @ C) => (B @ (sk6 @ A))))) & (exists @ A @ (sk6 @ A))))),inference(func_ext,[status(esa)],[32])).
% 10.20/3.47 thf(34,plain,(! [C:mworld,B:(individual > $o),A:mworld] : (((~ (positive @ A @ (B)) | ~ (mrel @ A @ C) | (B @ (sk6 @ A))) & (exists @ A @ (sk6 @ A))))),inference(cnf,[status(esa)],[33])).
% 10.20/3.47 thf(36,plain,(! [A:mworld] : ((exists @ A @ (sk6 @ A)))),inference(cnfConj,[status(thm)],[34])).
% 10.20/3.47 thf(1,conjecture,((mlocal @ (mbox @ (^ [A:mworld]: ? [B:individual]: ((exists @ A @ B) & (godlike @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',theoremV5)).
% 10.20/3.47 thf(2,negated_conjecture,((~ (mlocal @ (mbox @ (^ [A:mworld]: ? [B:individual]: ((exists @ A @ B) & (godlike @ A @ B))))))),inference(neg_conjecture,[status(cth)],[1])).
% 10.20/3.47 thf(7,plain,((~ (! [A:mworld]: ((mrel @ mactual @ A) => (? [B:individual]: ((exists @ A @ B) & ! [C:(individual > $o)]: ((positive @ A @ (C)) => (! [D:mworld]: ((mrel @ A @ D) => (C @ B)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 10.20/3.47 thf(8,plain,((~ (! [A:mworld]: ((mrel @ mactual @ A) => (? [B:individual]: ((exists @ A @ B) & ! [C:(individual > $o)]: ((positive @ A @ (C)) => ((? [D:mworld]: (mrel @ A @ D)) => (C @ B))))))))),inference(miniscope,[status(thm)],[7])).
% 10.20/3.47 thf(9,plain,(! [A:individual] : (((mrel @ mactual @ sk1) & (~ (exists @ sk1 @ A) | (positive @ sk1 @ (sk2 @ A))) & (~ (exists @ sk1 @ A) | (mrel @ sk1 @ (sk3 @ A))) & (~ (exists @ sk1 @ A) | ~ (sk2 @ A @ A))))),inference(cnf,[status(esa)],[8])).
% 10.20/3.47 thf(11,plain,(! [A:individual] : ((~ (exists @ sk1 @ A)) | (positive @ sk1 @ (sk2 @ A)))),inference(cnfConj,[status(thm)],[9])).
% 10.20/3.47 thf(130,plain,(! [B:individual,A:mworld] : (~ (($true)) | (positive @ sk1 @ (sk2 @ B)) | ((exists @ A @ (sk6 @ A)) != (exists @ sk1 @ B)))),inference(paramod_ordered,[status(thm)],[36,11])).
% 10.20/3.47 thf(131,plain,(! [B:individual,A:mworld] : ((positive @ sk1 @ (sk2 @ B)) | ((exists @ A @ (sk6 @ A)) != (exists @ sk1 @ B)))),inference(simp,[status(thm)],[130])).
% 10.20/3.47 thf(132,plain,((positive @ sk1 @ (sk2 @ (sk6 @ sk1)))),inference(pattern_uni,[status(thm)],[131:[bind(A, $thf(sk1)),bind(B, $thf(sk6 @ sk1))]])).
% 10.20/3.47 thf(191,plain,(! [C:(individual > $o),B:(individual > $o),A:mworld] : ((mrel @ A @ (sk4 @ (C) @ (B) @ A)) | (positive @ A @ (B)) | ((positive @ A @ (C)) != (positive @ sk1 @ (sk2 @ (sk6 @ sk1)))))),inference(paramod_ordered,[status(thm)],[21,132])).
% 10.20/3.47 thf(192,plain,(! [A:(individual > $o)] : ((mrel @ sk1 @ (sk4 @ (sk2 @ (sk6 @ sk1)) @ (A) @ sk1)) | (positive @ sk1 @ (A)))),inference(pattern_uni,[status(thm)],[191:[bind(A, $thf(sk1)),bind(B, $thf(B)),bind(C, $thf(sk2 @ (sk6 @ sk1)))]])).
% 10.20/3.47 thf(236,plain,(! [A:(individual > $o)] : ((mrel @ sk1 @ (sk4 @ (sk2 @ (sk6 @ sk1)) @ (A) @ sk1)) | (positive @ sk1 @ (A)))),inference(simp,[status(thm)],[192])).
% 10.20/3.47 thf(306,plain,(! [B:mworld,A:(individual > $o)] : ((mrel @ sk1 @ (sk4 @ (sk2 @ (sk6 @ sk1)) @ (A) @ sk1)) | ~ (($true)) | ((positive @ sk1 @ (A)) != (positive @ B @ (^ [C:individual]: (($false))))))),inference(paramod_ordered,[status(thm)],[236,26])).
% 10.20/3.47 thf(307,plain,(! [B:mworld,A:(individual > $o)] : ((mrel @ sk1 @ (sk4 @ (sk2 @ (sk6 @ sk1)) @ (A) @ sk1)) | ((positive @ sk1 @ (A)) != (positive @ B @ (^ [C:individual]: (($false))))))),inference(simp,[status(thm)],[306])).
% 10.20/3.47 thf(308,plain,((mrel @ sk1 @ (sk4 @ (sk2 @ (sk6 @ sk1)) @ (^ [A:individual]: (($false))) @ sk1))),inference(pattern_uni,[status(thm)],[307:[bind(A, $thf(^ [C:individual]: (($false)))),bind(B, $thf(sk1))]])).
% 10.20/3.47 thf(10,plain,((mrel @ mactual @ sk1)),inference(cnfConj,[status(thm)],[9])).
% 10.20/3.47 thf(3,axiom,((! [A:mworld,B:mworld]: ((mrel @ A @ B) => (mrel @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',mrel_symmetric)).
% 10.20/3.47 thf(14,plain,((! [A:mworld,B:mworld]: ((mrel @ A @ B) => (mrel @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 10.20/3.47 thf(145,plain,(! [A:mworld] : (~ (($true)) | ((positive @ sk1 @ (sk2 @ (sk6 @ sk1))) != (positive @ A @ (^ [B:individual]: (($false))))))),inference(paramod_ordered,[status(thm)],[132,26])).
% 10.20/3.47 thf(146,plain,(! [A:mworld] : (((positive @ sk1 @ (sk2 @ (sk6 @ sk1))) != (positive @ A @ (^ [B:individual]: (($false))))))),inference(simp,[status(thm)],[145])).
% 10.20/3.47 thf(148,plain,(! [A:mworld] : ((sk1 != A) | ((sk2 @ (sk6 @ sk1)) != (^ [B:individual]: (($false)))))),inference(simp,[status(thm)],[146])).
% 10.20/3.47 thf(151,plain,(((sk2 @ (sk6 @ sk1)) != (^ [A:individual]: (($false))))),inference(simp,[status(thm)],[148])).
% 10.20/3.47 thf(152,plain,((sk2 @ (sk6 @ sk1) @ sk7)),inference(func_ext,[status(esa)],[151])).
% 10.20/3.47 thf(12,plain,(! [A:individual] : ((~ (exists @ sk1 @ A)) | (mrel @ sk1 @ (sk3 @ A)))),inference(cnfConj,[status(thm)],[9])).
% 10.20/3.47 thf(263,plain,(! [B:individual,A:mworld] : (~ (($true)) | (mrel @ sk1 @ (sk3 @ B)) | ((exists @ A @ (sk6 @ A)) != (exists @ sk1 @ B)))),inference(paramod_ordered,[status(thm)],[36,12])).
% 10.20/3.47 thf(264,plain,(! [B:individual,A:mworld] : ((mrel @ sk1 @ (sk3 @ B)) | ((exists @ A @ (sk6 @ A)) != (exists @ sk1 @ B)))),inference(simp,[status(thm)],[263])).
% 10.20/3.47 thf(265,plain,((mrel @ sk1 @ (sk3 @ (sk6 @ sk1)))),inference(pattern_uni,[status(thm)],[264:[bind(A, $thf(sk1)),bind(B, $thf(sk6 @ sk1))]])).
% 10.20/3.47 thf(35,plain,(! [C:mworld,B:(individual > $o),A:mworld] : ((~ (positive @ A @ (B))) | (~ (mrel @ A @ C)) | (B @ (sk6 @ A)))),inference(cnfConj,[status(thm)],[34])).
% 10.20/3.47 thf(13,plain,(! [A:individual] : ((~ (exists @ sk1 @ A)) | (~ (sk2 @ A @ A)))),inference(cnfConj,[status(thm)],[9])).
% 10.20/3.47 thf(92,plain,(! [B:individual,A:mworld] : (~ (($true)) | (~ (sk2 @ B @ B)) | ((exists @ A @ (sk6 @ A)) != (exists @ sk1 @ B)))),inference(paramod_ordered,[status(thm)],[36,13])).
% 10.20/3.47 thf(93,plain,(! [B:individual,A:mworld] : ((~ (sk2 @ B @ B)) | ((exists @ A @ (sk6 @ A)) != (exists @ sk1 @ B)))),inference(simp,[status(thm)],[92])).
% 10.20/3.47 thf(94,plain,((~ (sk2 @ (sk6 @ sk1) @ (sk6 @ sk1)))),inference(pattern_uni,[status(thm)],[93:[bind(A, $thf(sk1)),bind(B, $thf(sk6 @ sk1))]])).
% 10.20/3.47 thf(95,plain,(! [C:mworld,B:(individual > $o),A:mworld] : ((~ (positive @ A @ (B))) | (~ (mrel @ A @ C)) | ~ (($true)) | ((B @ (sk6 @ A)) != (sk2 @ (sk6 @ sk1) @ (sk6 @ sk1))))),inference(paramod_ordered,[status(thm)],[35,94])).
% 10.20/3.47 thf(96,plain,(! [C:mworld,B:(individual > $o),A:mworld] : ((~ (positive @ A @ (B))) | (~ (mrel @ A @ C)) | ((B @ (sk6 @ A)) != (sk2 @ (sk6 @ sk1) @ (sk6 @ sk1))))),inference(simp,[status(thm)],[95])).
% 10.20/3.47 thf(97,plain,(! [A:mworld] : ((~ (positive @ sk1 @ (^ [B:individual]: (sk2 @ B @ B)))) | (~ (mrel @ sk1 @ A)))),inference(pre_uni,[status(thm)],[96:[bind(A, $thf(sk1)),bind(B, $thf(^ [D:individual]: (sk2 @ D @ D))),bind(C, $thf(C))]])).
% 10.20/3.47 thf(101,plain,(! [A:mworld] : ((~ (positive @ sk1 @ (^ [B:individual]: (sk2 @ B @ B)))) | (~ (mrel @ sk1 @ A)))),inference(simp,[status(thm)],[97])).
% 10.20/3.47 thf(268,plain,(! [A:mworld] : ((~ (positive @ sk1 @ (^ [B:individual]: (sk2 @ B @ B)))) | ~ (($true)) | ((mrel @ sk1 @ (sk3 @ (sk6 @ sk1))) != (mrel @ sk1 @ A)))),inference(paramod_ordered,[status(thm)],[265,101])).
% 10.20/3.47 thf(269,plain,(! [A:mworld] : ((~ (positive @ sk1 @ (^ [B:individual]: (sk2 @ B @ B)))) | ((mrel @ sk1 @ (sk3 @ (sk6 @ sk1))) != (mrel @ sk1 @ A)))),inference(simp,[status(thm)],[268])).
% 10.20/3.47 thf(270,plain,((~ (positive @ sk1 @ (^ [A:individual]: (sk2 @ A @ A))))),inference(pattern_uni,[status(thm)],[269:[bind(A, $thf(sk3 @ (sk6 @ sk1)))]])).
% 10.20/3.47 thf(15,plain,(! [B:mworld,A:mworld] : ((~ (mrel @ A @ B)) | (mrel @ B @ A))),inference(cnf,[status(esa)],[14])).
% 10.20/3.47 thf(341,plain,(! [B:mworld,A:mworld] : (~ (($true)) | (mrel @ B @ A) | ((mrel @ mactual @ sk1) != (mrel @ A @ B)))),inference(paramod_ordered,[status(thm)],[10,15])).
% 10.20/3.47 thf(342,plain,(! [B:mworld,A:mworld] : ((mrel @ B @ A) | ((mrel @ mactual @ sk1) != (mrel @ A @ B)))),inference(simp,[status(thm)],[341])).
% 10.20/3.47 thf(343,plain,((mrel @ sk1 @ mactual)),inference(pattern_uni,[status(thm)],[342:[bind(A, $thf(mactual)),bind(B, $thf(sk1))]])).
% 10.20/3.47 thf(279,plain,(~ (($true)) | ((positive @ sk1 @ (sk2 @ (sk6 @ sk1))) != (positive @ sk1 @ (^ [A:individual]: (sk2 @ A @ A))))),inference(paramod_ordered,[status(thm)],[132,270])).
% 10.20/3.47 thf(280,plain,(((positive @ sk1 @ (sk2 @ (sk6 @ sk1))) != (positive @ sk1 @ (^ [A:individual]: (sk2 @ A @ A))))),inference(simp,[status(thm)],[279])).
% 10.20/3.47 thf(288,plain,((sk1 != sk1) | ((sk2 @ (sk6 @ sk1)) != (^ [A:individual]: (sk2 @ A @ A)))),inference(simp,[status(thm)],[280])).
% 10.20/3.47 thf(291,plain,(((sk2 @ (sk6 @ sk1)) != (^ [A:individual]: (sk2 @ A @ A)))),inference(simp,[status(thm)],[288])).
% 10.20/3.47 thf(298,plain,(((sk2 @ (sk6 @ sk1) @ sk10) != (sk2 @ sk10 @ sk10))),inference(func_ext,[status(esa)],[291])).
% 10.20/3.47 thf(332,plain,((~ (sk2 @ sk10 @ sk10)) | ((sk2 @ (sk6 @ sk1) @ sk10) != (sk2 @ (sk6 @ sk1) @ sk7))),inference(paramod_ordered,[status(thm)],[152,298])).
% 10.20/3.47 thf(336,plain,((~ (sk2 @ sk10 @ sk10)) | ((sk6 @ sk1) != (sk6 @ sk1)) | (sk10 != sk7)),inference(simp,[status(thm)],[332])).
% 10.20/3.47 thf(337,plain,((~ (sk2 @ sk10 @ sk10)) | (sk10 != sk7)),inference(simp,[status(thm)],[336])).
% 10.20/3.47 thf(155,plain,(~ (($true)) | ((sk2 @ (sk6 @ sk1) @ (sk6 @ sk1)) != (sk2 @ (sk6 @ sk1) @ sk7))),inference(paramod_ordered,[status(thm)],[152,94])).
% 10.20/3.47 thf(156,plain,(((sk2 @ (sk6 @ sk1) @ (sk6 @ sk1)) != (sk2 @ (sk6 @ sk1) @ sk7))),inference(simp,[status(thm)],[155])).
% 10.20/3.47 thf(158,plain,(((sk6 @ sk1) != (sk6 @ sk1)) | ((sk6 @ sk1) != sk7)),inference(simp,[status(thm)],[156])).
% 10.20/3.47 thf(160,plain,(((sk6 @ sk1) != sk7)),inference(simp,[status(thm)],[158])).
% 10.20/3.47 thf(105,plain,(! [A:mworld] : ((~ (positive @ sk1 @ (^ [B:individual]: (sk2 @ B @ B)))) | ~ (($true)) | ((mrel @ sk1 @ A) != (mrel @ mactual @ sk1)))),inference(paramod_ordered,[status(thm)],[10,101])).
% 10.20/3.47 thf(106,plain,(! [A:mworld] : ((~ (positive @ sk1 @ (^ [B:individual]: (sk2 @ B @ B)))) | ((mrel @ sk1 @ A) != (mrel @ mactual @ sk1)))),inference(simp,[status(thm)],[105])).
% 10.20/3.47 thf(113,plain,(! [A:mworld] : ((~ (positive @ sk1 @ (^ [B:individual]: (sk2 @ B @ B)))) | (sk1 != mactual) | (A != sk1))),inference(simp,[status(thm)],[106])).
% 10.20/3.47 thf(117,plain,((~ (positive @ sk1 @ (^ [A:individual]: (sk2 @ A @ A)))) | (sk1 != mactual)),inference(simp,[status(thm)],[113])).
% 10.20/3.47 thf(161,plain,(~ (($true)) | (sk1 != mactual) | ((positive @ sk1 @ (sk2 @ (sk6 @ sk1))) != (positive @ sk1 @ (^ [A:individual]: (sk2 @ A @ A))))),inference(paramod_ordered,[status(thm)],[132,117])).
% 10.20/3.47 thf(162,plain,((sk1 != mactual) | ((positive @ sk1 @ (sk2 @ (sk6 @ sk1))) != (positive @ sk1 @ (^ [A:individual]: (sk2 @ A @ A))))),inference(simp,[status(thm)],[161])).
% 10.20/3.47 thf(169,plain,((sk1 != mactual) | (sk1 != sk1) | ((sk2 @ (sk6 @ sk1)) != (^ [A:individual]: (sk2 @ A @ A)))),inference(simp,[status(thm)],[162])).
% 10.20/3.47 thf(173,plain,((sk1 != mactual) | ((sk2 @ (sk6 @ sk1)) != (^ [A:individual]: (sk2 @ A @ A)))),inference(simp,[status(thm)],[169])).
% 10.20/3.47 thf(177,plain,((sk1 != mactual) | ((^ [A:individual]: (sk6 @ sk1)) != (^ [A:individual]: (A))) | ((^ [A:individual]: (A)) != (^ [A:individual]: (A)))),inference(simp,[status(thm)],[173])).
% 10.20/3.47 thf(179,plain,((sk1 != mactual) | ((^ [A:individual]: (sk6 @ sk1)) != (^ [A:individual]: (A)))),inference(simp,[status(thm)],[177])).
% 10.20/3.47 thf(260,plain,(((sk6 @ sk1) != sk9) | (sk1 != mactual)),inference(func_ext,[status(esa)],[179])).
% 10.20/3.47 thf(347,plain,(! [B:mworld,A:mworld] : (~ (($true)) | (mrel @ B @ A) | ((mrel @ sk1 @ (sk3 @ (sk6 @ sk1))) != (mrel @ A @ B)))),inference(paramod_ordered,[status(thm)],[265,15])).
% 10.20/3.47 thf(348,plain,(! [B:mworld,A:mworld] : ((mrel @ B @ A) | ((mrel @ sk1 @ (sk3 @ (sk6 @ sk1))) != (mrel @ A @ B)))),inference(simp,[status(thm)],[347])).
% 10.20/3.47 thf(349,plain,((mrel @ (sk3 @ (sk6 @ sk1)) @ sk1)),inference(pattern_uni,[status(thm)],[348:[bind(A, $thf(sk1)),bind(B, $thf(sk3 @ (sk6 @ sk1)))]])).
% 10.20/3.47 thf(297,plain,(((^ [A:individual]: (sk6 @ sk1)) != (^ [A:individual]: (A))) | ((^ [A:individual]: (A)) != (^ [A:individual]: (A)))),inference(simp,[status(thm)],[291])).
% 10.20/3.47 thf(299,plain,(((^ [A:individual]: (sk6 @ sk1)) != (^ [A:individual]: (A)))),inference(simp,[status(thm)],[297])).
% 10.20/3.47 thf(331,plain,((sk2 @ (sk6 @ sk1) @ sk10) | (sk2 @ sk10 @ sk10)),inference(bool_ext,[status(thm)],[298])).
% 10.20/3.47 thf(329,plain,(((sk6 @ sk1) != sk10) | (sk10 != sk10)),inference(simp,[status(thm)],[298])).
% 10.20/3.47 thf(338,plain,(((sk6 @ sk1) != sk10)),inference(simp,[status(thm)],[329])).
% 10.20/3.47 thf(300,plain,(((sk6 @ sk1) != sk11)),inference(func_ext,[status(esa)],[299])).
% 10.20/3.47 thf(303,plain,(! [A:(individual > $o)] : ((mrel @ sk1 @ (sk4 @ (sk2 @ (sk6 @ sk1)) @ (A) @ sk1)) | ~ (($true)) | ((positive @ sk1 @ (A)) != (positive @ sk1 @ (^ [B:individual]: (sk2 @ B @ B)))))),inference(paramod_ordered,[status(thm)],[236,270])).
% 10.20/3.47 thf(304,plain,(! [A:(individual > $o)] : ((mrel @ sk1 @ (sk4 @ (sk2 @ (sk6 @ sk1)) @ (A) @ sk1)) | ((positive @ sk1 @ (A)) != (positive @ sk1 @ (^ [B:individual]: (sk2 @ B @ B)))))),inference(simp,[status(thm)],[303])).
% 10.20/3.47 thf(305,plain,((mrel @ sk1 @ (sk4 @ (sk2 @ (sk6 @ sk1)) @ (^ [A:individual]: (sk2 @ A @ A)) @ sk1))),inference(pattern_uni,[status(thm)],[304:[bind(A, $thf(^ [B:individual]: (sk2 @ B @ B)))]])).
% 10.20/3.47 thf(513,plain,(($false)),inference(e,[status(thm)],[308,10,24,14,152,270,13,343,7,11,26,15,337,132,265,28,160,21,260,349,298,32,291,27,12,236,299,35,331,16,338,151,300,36,305,94])).
% 10.20/3.47 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.20/3.47 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------