%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYO442^1 : TPTP v9.3.1. Released v4.0.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 : n016.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:45:48 AM UTC 2026
% Result : Theorem 10.92s 3.63s
% Output : Refutation 9.98s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO442^1 : TPTP v9.3.1. Released v4.0.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.18 % Computer : n016.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 16:56:49 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 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.91/0.76 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.27/1.02 % [INFO] Parsing done (252ms).
% 1.68/1.03 % [INFO] Running in sequential loop mode.
% 2.27/1.43 % [INFO] eprover registered as external prover.
% 2.27/1.44 % [INFO] Scanning for conjecture ...
% 2.72/1.62 % [INFO] Found a conjecture (or negated_conjecture) and 3 axioms. Running axiom selection ...
% 2.72/1.66 % [INFO] Axiom selection finished. Selected 3 axioms (removed 0 axioms).
% 2.72/1.66 % [INFO] Problem is higher-order (TPTP THF).
% 2.72/1.66 % [INFO] Type checking passed.
% 2.72/1.67 % [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.92/3.62 % External prover 'e' found a proof!
% 10.92/3.62 % [INFO] Killing All external provers ...
% 10.92/3.62 % Time passed: 3307ms (effective reasoning time: 2580ms)
% 10.92/3.62 % 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.92/3.62 % Axioms used in derivation (3): a1, a3, a2
% 10.92/3.62 % No. of inferences in proof: 102
% 10.92/3.63 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 3307 ms resp. 2580 ms w/o parsing
% 9.98/3.73 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.98/3.73 thf(mu_type, type, mu: $tType).
% 9.98/3.73 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 9.98/3.73 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 9.98/3.73 thf(mand_decl, type, mand: (($i > $o) > (($i > $o) > ($i > $o)))).
% 9.98/3.73 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 9.98/3.73 thf(mequiv_decl, type, mequiv: (($i > $o) > (($i > $o) > ($i > $o)))).
% 9.98/3.73 thf(mreflexive_decl, type, mreflexive: (($i > ($i > $o)) > $o)).
% 9.98/3.73 thf(msymmetric_decl, type, msymmetric: (($i > ($i > $o)) > $o)).
% 9.98/3.73 thf(mtransitive_decl, type, mtransitive: (($i > ($i > $o)) > $o)).
% 9.98/3.73 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 9.98/3.73 thf(rel_s5_decl, type, rel_s5: ($i > ($i > $o))).
% 9.98/3.73 thf(mbox_s5_decl, type, mbox_s5: (($i > $o) > ($i > $o))).
% 9.98/3.73 thf(mdia_s5_decl, type, mdia_s5: (($i > $o) > ($i > $o))).
% 9.98/3.73 thf(p_decl, type, p: ($i > $o)).
% 9.98/3.73 thf(sk1_decl, type, sk1: $o).
% 9.98/3.73 thf(sk2_decl, type, sk2: $i).
% 9.98/3.73 thf(sk3_decl, type, sk3: ($i > $i)).
% 9.98/3.73 thf(sk4_decl, type, sk4: ($i > $i)).
% 9.98/3.73 thf(sk5_decl, type, sk5: $i).
% 9.98/3.73 thf(sk6_decl, type, sk6: $i).
% 9.98/3.73 thf(sk7_decl, type, sk7: $i).
% 9.98/3.73 thf(sk8_decl, type, sk8: $i).
% 9.98/3.73 thf(sk9_decl, type, sk9: ($i > ($i > $i))).
% 9.98/3.73 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 9.98/3.73 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 9.98/3.73 thf(mand_def, definition, mand = (^ [A:($i > $o),B:($i > $o)]: (mnot @ (mor @ (mnot @ A) @ (mnot @ B)))) ).
% 9.98/3.73 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 9.98/3.73 thf(mequiv_def, definition, mequiv = (^ [A:($i > $o),B:($i > $o)]: (mand @ (mimplies @ A @ B) @ (mimplies @ B @ A))) ).
% 9.98/3.73 thf(mreflexive_def, definition, mreflexive = (^ [A:($i > ($i > $o))]: ! [B:$i]: (A @ B @ B)) ).
% 9.98/3.73 thf(msymmetric_def, definition, msymmetric = (^ [A:($i > ($i > $o))]: ! [B:$i,C:$i]: ((A @ B @ C) => (A @ C @ B))) ).
% 9.98/3.73 thf(mtransitive_def, definition, mtransitive = (^ [A:($i > ($i > $o))]: ! [B:$i,C:$i,D:$i]: (((A @ B @ C) & (A @ C @ D)) => (A @ B @ D))) ).
% 9.98/3.73 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 9.98/3.73 thf(mbox_s5_def, definition, mbox_s5 = (^ [A:($i > $o),B:$i]: ! [C:$i]: (~ (rel_s5 @ B @ C) | (A @ C))) ).
% 9.98/3.73 thf(mdia_s5_def, definition, mdia_s5 = (^ [A:($i > $o)]: (mnot @ (mbox_s5 @ (mnot @ A)))) ).
% 9.98/3.73 thf(sk2_def, definition, sk2 = (@+ [A:$i]: ~ (~ (! [B:$i]: (~ (rel_s5 @ A @ B) | ~ (! [C:$i]: (~ (rel_s5 @ B @ C) | ! [D:$i]: (~ (rel_s5 @ C @ D) | ~ (! [E:$i]: (~ (rel_s5 @ D @ E) | (p @ E)))))))) | ! [B:$i]: (~ (rel_s5 @ A @ B) | ! [C:$i]: (~ (rel_s5 @ B @ C) | (p @ C))))) ).
% 9.98/3.73 thf(sk3_def, definition, sk3 = (^ [A:$i]: (@+ [B:$i]: ~ (~ (rel_s5 @ A @ B) | ! [C:$i]: (~ (rel_s5 @ B @ C) | ~ (! [D:$i]: (~ (rel_s5 @ C @ D) | (p @ D))))))) ).
% 9.98/3.73 thf(sk4_def, definition, sk4 = (^ [A:$i]: (@+ [B:$i]: ~ (~ (rel_s5 @ (sk3 @ A) @ B) | ~ (! [C:$i]: (~ (rel_s5 @ B @ C) | (p @ C)))))) ).
% 9.98/3.73 thf(sk5_def, definition, sk5 = (@+ [A:$i]: ~ (~ (rel_s5 @ sk2 @ A) | ! [B:$i]: (~ (rel_s5 @ A @ B) | (p @ B)))) ).
% 9.98/3.73 thf(sk6_def, definition, sk6 = (@+ [A:$i]: ~ (~ (rel_s5 @ sk5 @ A) | (p @ A))) ).
% 9.98/3.73 thf(sk7_def, definition, sk7 = (@+ [A:$i]: ~ (~ (! [B:$i]: (~ (rel_s5 @ A @ B) | ! [C:$i]: (~ (rel_s5 @ B @ C) | (p @ C)))) | ! [B:$i]: (~ (rel_s5 @ A @ B) | ~ (! [C:$i]: (~ (rel_s5 @ B @ C) | ! [D:$i]: (~ (rel_s5 @ C @ D) | ~ (! [E:$i]: (~ (rel_s5 @ D @ E) | (p @ E))))))))) ).
% 9.98/3.73 thf(sk8_def, definition, sk8 = (@+ [A:$i]: ~ (~ (rel_s5 @ sk7 @ A) | ~ (! [B:$i]: (~ (rel_s5 @ A @ B) | ! [C:$i]: (~ (rel_s5 @ B @ C) | ~ (! [D:$i]: (~ (rel_s5 @ C @ D) | (p @ D)))))))) ).
% 9.98/3.73 thf(sk9_def, definition, sk9 = (^ [A:$i,B:$i]: (@+ [C:$i]: ~ (~ (rel_s5 @ A @ C) | (p @ C)))) ).
% 9.98/3.73 thf(1,conjecture,((mvalid @ (mequiv @ (mbox_s5 @ (mdia_s5 @ (mdia_s5 @ (mbox_s5 @ p)))) @ (mbox_s5 @ (mbox_s5 @ p))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove)).
% 9.98/3.73 thf(2,negated_conjecture,((~ (mvalid @ (mequiv @ (mbox_s5 @ (mdia_s5 @ (mdia_s5 @ (mbox_s5 @ p)))) @ (mbox_s5 @ (mbox_s5 @ p)))))),inference(neg_conjecture,[status(cth)],[1])).
% 9.98/3.73 thf(6,plain,((~ (! [A:$i]: ~ (~ (~ (! [B:$i]: (~ (rel_s5 @ A @ B) | ~ (! [C:$i]: (~ (rel_s5 @ B @ C) | ! [D:$i]: (~ (rel_s5 @ C @ D) | ~ (! [E:$i]: (~ (rel_s5 @ D @ E) | (p @ E)))))))) | ! [B:$i]: (~ (rel_s5 @ A @ B) | ! [C:$i]: (~ (rel_s5 @ B @ C) | (p @ C)))) | ~ (~ (! [B:$i]: (~ (rel_s5 @ A @ B) | ! [C:$i]: (~ (rel_s5 @ B @ C) | (p @ C)))) | ! [B:$i]: (~ (rel_s5 @ A @ B) | ~ (! [C:$i]: (~ (rel_s5 @ B @ C) | ! [D:$i]: (~ (rel_s5 @ C @ D) | ~ (! [E:$i]: (~ (rel_s5 @ D @ E) | (p @ E)))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 9.98/3.73 thf(7,plain,((~ (~ (~ (! [A:$i]: (~ (! [B:$i]: (~ (rel_s5 @ A @ B) | ~ (! [C:$i]: (~ (rel_s5 @ B @ C) | ! [D:$i]: (~ (rel_s5 @ C @ D) | ~ (! [E:$i]: (~ (rel_s5 @ D @ E) | (p @ E)))))))) | ! [B:$i]: (~ (rel_s5 @ A @ B) | ! [C:$i]: (~ (rel_s5 @ B @ C) | (p @ C))))) | ~ (! [A:$i]: (~ (! [B:$i]: (~ (rel_s5 @ A @ B) | ! [C:$i]: (~ (rel_s5 @ B @ C) | (p @ C)))) | ! [B:$i]: (~ (rel_s5 @ A @ B) | ~ (! [C:$i]: (~ (rel_s5 @ B @ C) | ! [D:$i]: (~ (rel_s5 @ C @ D) | ~ (! [E:$i]: (~ (rel_s5 @ D @ E) | (p @ E))))))))))))),inference(miniscope,[status(thm)],[6])).
% 9.98/3.73 thf(8,plain,(! [F:$i,E:$i,D:$i,C:$i,B:$i,A:$i] : (((~ (rel_s5 @ sk2 @ A) | (rel_s5 @ A @ (sk3 @ A)) | (sk1)) & (~ (rel_s5 @ sk2 @ A) | (rel_s5 @ (sk3 @ A) @ (sk4 @ A)) | (sk1)) & (~ (rel_s5 @ sk2 @ A) | ~ (rel_s5 @ (sk4 @ A) @ B) | (p @ B) | (sk1)) & ((rel_s5 @ sk2 @ sk5) | (sk1)) & ((rel_s5 @ sk5 @ sk6) | (sk1)) & (~ (p @ sk6) | (sk1)) & (~ (sk1) | ~ (rel_s5 @ sk7 @ C) | ~ (rel_s5 @ C @ D) | (p @ D)) & (~ (sk1) | (rel_s5 @ sk7 @ sk8)) & (~ (sk1) | ~ (rel_s5 @ sk8 @ E) | ~ (rel_s5 @ E @ F) | (rel_s5 @ F @ (sk9 @ F @ E))) & (~ (sk1) | ~ (rel_s5 @ sk8 @ E) | ~ (rel_s5 @ E @ F) | ~ (p @ (sk9 @ F @ E)))))),inference(cnf,[status(esa)],[7])).
% 9.98/3.73 thf(10,plain,(! [B:$i,A:$i] : ((~ (rel_s5 @ sk2 @ A)) | (~ (rel_s5 @ (sk4 @ A) @ B)) | (p @ B) | sk1)),inference(cnfConj,[status(thm)],[8])).
% 9.98/3.73 thf(3,axiom,((mreflexive @ rel_s5)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1)).
% 9.98/3.73 thf(22,plain,((! [A:$i]: (rel_s5 @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 9.98/3.73 thf(23,plain,(! [A:$i] : ((rel_s5 @ A @ A))),inference(cnf,[status(esa)],[22])).
% 9.98/3.73 thf(14,plain,(! [A:$i] : ((~ (rel_s5 @ sk2 @ A)) | (rel_s5 @ (sk3 @ A) @ (sk4 @ A)) | sk1)),inference(cnfConj,[status(thm)],[8])).
% 9.98/3.73 thf(236,plain,(! [B:$i,A:$i] : (~ (($true)) | (rel_s5 @ (sk3 @ B) @ (sk4 @ B)) | sk1 | ((rel_s5 @ A @ A) != (rel_s5 @ sk2 @ B)))),inference(paramod_ordered,[status(thm)],[23,14])).
% 9.98/3.73 thf(237,plain,(! [B:$i,A:$i] : ((rel_s5 @ (sk3 @ B) @ (sk4 @ B)) | sk1 | ((rel_s5 @ A @ A) != (rel_s5 @ sk2 @ B)))),inference(simp,[status(thm)],[236])).
% 9.98/3.73 thf(238,plain,((rel_s5 @ (sk3 @ sk2) @ (sk4 @ sk2)) | sk1),inference(pattern_uni,[status(thm)],[237:[bind(A, $thf(sk2)),bind(B, $thf(sk2))]])).
% 9.98/3.73 thf(5,axiom,((msymmetric @ rel_s5)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a3)).
% 9.98/3.73 thf(26,plain,((! [A:$i,B:$i]: ((rel_s5 @ A @ B) => (rel_s5 @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 9.98/3.73 thf(27,plain,(! [B:$i,A:$i] : ((~ (rel_s5 @ A @ B)) | (rel_s5 @ B @ A))),inference(cnf,[status(esa)],[26])).
% 9.98/3.73 thf(308,plain,(! [B:$i,A:$i] : (sk1 | ~ (($true)) | (rel_s5 @ B @ A) | ((rel_s5 @ (sk3 @ sk2) @ (sk4 @ sk2)) != (rel_s5 @ A @ B)))),inference(paramod_ordered,[status(thm)],[238,27])).
% 9.98/3.73 thf(309,plain,(! [B:$i,A:$i] : (sk1 | (rel_s5 @ B @ A) | ((rel_s5 @ (sk3 @ sk2) @ (sk4 @ sk2)) != (rel_s5 @ A @ B)))),inference(simp,[status(thm)],[308])).
% 9.98/3.73 thf(310,plain,(sk1 | (rel_s5 @ (sk4 @ sk2) @ (sk3 @ sk2))),inference(pattern_uni,[status(thm)],[309:[bind(A, $thf(sk3 @ sk2)),bind(B, $thf(sk4 @ sk2))]])).
% 9.98/3.73 thf(79,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (~ (rel_s5 @ (sk4 @ B) @ C)) | (p @ C) | sk1 | ((rel_s5 @ A @ A) != (rel_s5 @ sk2 @ B)))),inference(paramod_ordered,[status(thm)],[23,10])).
% 9.98/3.73 thf(80,plain,(! [C:$i,B:$i,A:$i] : ((~ (rel_s5 @ (sk4 @ B) @ C)) | (p @ C) | sk1 | ((rel_s5 @ A @ A) != (rel_s5 @ sk2 @ B)))),inference(simp,[status(thm)],[79])).
% 9.98/3.73 thf(81,plain,(! [A:$i] : ((~ (rel_s5 @ (sk4 @ sk2) @ A)) | (p @ A) | sk1)),inference(pattern_uni,[status(thm)],[80:[bind(A, $thf(sk2)),bind(B, $thf(sk2))]])).
% 9.98/3.73 thf(91,plain,(! [A:$i] : ((~ (rel_s5 @ (sk4 @ sk2) @ A)) | (p @ A) | sk1)),inference(simp,[status(thm)],[81])).
% 9.98/3.73 thf(347,plain,(! [A:$i] : (sk1 | ~ (($true)) | (p @ A) | sk1 | ((rel_s5 @ (sk4 @ sk2) @ (sk3 @ sk2)) != (rel_s5 @ (sk4 @ sk2) @ A)))),inference(paramod_ordered,[status(thm)],[310,91])).
% 9.98/3.73 thf(348,plain,(! [A:$i] : (sk1 | (p @ A) | ((rel_s5 @ (sk4 @ sk2) @ (sk3 @ sk2)) != (rel_s5 @ (sk4 @ sk2) @ A)))),inference(simp,[status(thm)],[347])).
% 9.98/3.73 thf(349,plain,(sk1 | (p @ (sk3 @ sk2))),inference(pattern_uni,[status(thm)],[348:[bind(A, $thf(sk3 @ sk2))]])).
% 9.98/3.73 thf(12,plain,((~ (p @ sk6)) | sk1),inference(cnfConj,[status(thm)],[8])).
% 9.98/3.73 thf(13,plain,((rel_s5 @ sk5 @ sk6) | sk1),inference(cnfConj,[status(thm)],[8])).
% 9.98/3.73 thf(110,plain,(! [B:$i,A:$i] : (sk1 | ~ (($true)) | (rel_s5 @ B @ A) | ((rel_s5 @ sk5 @ sk6) != (rel_s5 @ A @ B)))),inference(paramod_ordered,[status(thm)],[13,27])).
% 9.98/3.73 thf(111,plain,(! [B:$i,A:$i] : (sk1 | (rel_s5 @ B @ A) | ((rel_s5 @ sk5 @ sk6) != (rel_s5 @ A @ B)))),inference(simp,[status(thm)],[110])).
% 9.98/3.73 thf(112,plain,(sk1 | (rel_s5 @ sk6 @ sk5)),inference(pattern_uni,[status(thm)],[111:[bind(A, $thf(sk5)),bind(B, $thf(sk6))]])).
% 9.98/3.73 thf(16,plain,(! [A:$i] : ((~ (rel_s5 @ sk2 @ A)) | (rel_s5 @ A @ (sk3 @ A)) | sk1)),inference(cnfConj,[status(thm)],[8])).
% 9.98/3.73 thf(11,plain,(~ (sk1) | (rel_s5 @ sk7 @ sk8)),inference(cnfConj,[status(thm)],[8])).
% 9.98/3.73 thf(372,plain,(sk1 | ~ (($true)) | sk1 | ((p @ (sk3 @ sk2)) != (p @ sk6))),inference(paramod_ordered,[status(thm)],[349,12])).
% 9.98/3.73 thf(373,plain,(sk1 | ((p @ (sk3 @ sk2)) != (p @ sk6))),inference(simp,[status(thm)],[372])).
% 9.98/3.73 thf(378,plain,(sk1 | ((sk3 @ sk2) != sk6)),inference(simp,[status(thm)],[373])).
% 9.98/3.73 thf(17,plain,(! [B:$i,A:$i] : (~ (sk1) | (~ (rel_s5 @ sk8 @ A)) | (~ (rel_s5 @ A @ B)) | (~ (p @ (sk9 @ B @ A))))),inference(cnfConj,[status(thm)],[8])).
% 9.98/3.73 thf(19,plain,(! [B:$i,A:$i] : (~ (sk1) | (~ (rel_s5 @ sk8 @ A)) | (~ (rel_s5 @ A @ B)) | (~ (p @ (sk9 @ B @ A))))),inference(simp,[status(thm)],[17])).
% 9.98/3.73 thf(9,plain,((rel_s5 @ sk2 @ sk5) | sk1),inference(cnfConj,[status(thm)],[8])).
% 9.98/3.73 thf(186,plain,(! [A:$i] : (sk1 | ~ (($true)) | (p @ A) | sk1 | ((rel_s5 @ (sk4 @ sk2) @ A) != (rel_s5 @ sk2 @ sk5)))),inference(paramod_ordered,[status(thm)],[9,91])).
% 9.98/3.73 thf(187,plain,(! [A:$i] : (sk1 | (p @ A) | ((rel_s5 @ (sk4 @ sk2) @ A) != (rel_s5 @ sk2 @ sk5)))),inference(simp,[status(thm)],[186])).
% 9.98/3.73 thf(206,plain,(! [A:$i] : (sk1 | (p @ A) | ((sk4 @ sk2) != sk2) | (A != sk5))),inference(simp,[status(thm)],[187])).
% 9.98/3.73 thf(210,plain,(sk1 | (p @ sk5) | ((sk4 @ sk2) != sk2)),inference(simp,[status(thm)],[206])).
% 9.98/3.73 thf(38,plain,(! [C:$i,B:$i,A:$i] : (~ (sk1) | ~ (($true)) | (~ (rel_s5 @ B @ C)) | (~ (p @ (sk9 @ C @ B))) | ((rel_s5 @ A @ A) != (rel_s5 @ sk8 @ B)))),inference(paramod_ordered,[status(thm)],[23,19])).
% 9.98/3.73 thf(39,plain,(! [C:$i,B:$i,A:$i] : (~ (sk1) | (~ (rel_s5 @ B @ C)) | (~ (p @ (sk9 @ C @ B))) | ((rel_s5 @ A @ A) != (rel_s5 @ sk8 @ B)))),inference(simp,[status(thm)],[38])).
% 9.98/3.73 thf(40,plain,(! [A:$i] : (~ (sk1) | (~ (rel_s5 @ sk8 @ A)) | (~ (p @ (sk9 @ A @ sk8))))),inference(pattern_uni,[status(thm)],[39:[bind(A, $thf(sk8)),bind(B, $thf(sk8))]])).
% 9.98/3.73 thf(47,plain,(! [A:$i] : (~ (sk1) | (~ (rel_s5 @ sk8 @ A)) | (~ (p @ (sk9 @ A @ sk8))))),inference(simp,[status(thm)],[40])).
% 9.98/3.73 thf(225,plain,(! [A:$i] : (sk1 | ~ (($true)) | (rel_s5 @ (sk3 @ A) @ (sk4 @ A)) | sk1 | ((rel_s5 @ sk2 @ sk5) != (rel_s5 @ sk2 @ A)))),inference(paramod_ordered,[status(thm)],[9,14])).
% 9.98/3.73 thf(226,plain,(! [A:$i] : (sk1 | (rel_s5 @ (sk3 @ A) @ (sk4 @ A)) | ((rel_s5 @ sk2 @ sk5) != (rel_s5 @ sk2 @ A)))),inference(simp,[status(thm)],[225])).
% 9.98/3.73 thf(227,plain,(sk1 | (rel_s5 @ (sk3 @ sk5) @ (sk4 @ sk5))),inference(pattern_uni,[status(thm)],[226:[bind(A, $thf(sk5))]])).
% 9.98/3.73 thf(116,plain,(! [B:$i,A:$i] : (~ (sk1) | ~ (($true)) | (rel_s5 @ B @ A) | ((rel_s5 @ sk7 @ sk8) != (rel_s5 @ A @ B)))),inference(paramod_ordered,[status(thm)],[11,27])).
% 9.98/3.73 thf(117,plain,(! [B:$i,A:$i] : (~ (sk1) | (rel_s5 @ B @ A) | ((rel_s5 @ sk7 @ sk8) != (rel_s5 @ A @ B)))),inference(simp,[status(thm)],[116])).
% 9.98/3.73 thf(118,plain,(~ (sk1) | (rel_s5 @ sk8 @ sk7)),inference(pattern_uni,[status(thm)],[117:[bind(A, $thf(sk7)),bind(B, $thf(sk8))]])).
% 9.98/3.73 thf(177,plain,(! [B:$i,A:$i] : (~ (sk1) | ~ (sk1) | (~ (rel_s5 @ sk8 @ A)) | ~ (($true)) | (~ (p @ (sk9 @ B @ A))) | ((rel_s5 @ sk8 @ sk7) != (rel_s5 @ A @ B)))),inference(paramod_ordered,[status(thm)],[118,19])).
% 9.98/3.73 thf(178,plain,(! [B:$i,A:$i] : (~ (sk1) | (~ (rel_s5 @ sk8 @ A)) | (~ (p @ (sk9 @ B @ A))) | ((rel_s5 @ sk8 @ sk7) != (rel_s5 @ A @ B)))),inference(simp,[status(thm)],[177])).
% 9.98/3.73 thf(179,plain,(~ (sk1) | (~ (rel_s5 @ sk8 @ sk8)) | (~ (p @ (sk9 @ sk7 @ sk8)))),inference(pattern_uni,[status(thm)],[178:[bind(A, $thf(sk8)),bind(B, $thf(sk7))]])).
% 9.98/3.73 thf(364,plain,(~ (sk1) | ~ (($true)) | (~ (p @ (sk9 @ sk7 @ sk8)))),inference(rewrite,[status(thm)],[179,23])).
% 9.98/3.73 thf(365,plain,(~ (sk1) | (~ (p @ (sk9 @ sk7 @ sk8)))),inference(simp,[status(thm)],[364])).
% 9.98/3.73 thf(387,plain,(! [A:$i] : (sk1 | ~ (($true)) | (rel_s5 @ A @ (sk3 @ A)) | sk1 | ((rel_s5 @ sk2 @ sk5) != (rel_s5 @ sk2 @ A)))),inference(paramod_ordered,[status(thm)],[9,16])).
% 9.98/3.73 thf(388,plain,(! [A:$i] : (sk1 | (rel_s5 @ A @ (sk3 @ A)) | ((rel_s5 @ sk2 @ sk5) != (rel_s5 @ sk2 @ A)))),inference(simp,[status(thm)],[387])).
% 9.98/3.73 thf(389,plain,(sk1 | (rel_s5 @ sk5 @ (sk3 @ sk5))),inference(pattern_uni,[status(thm)],[388:[bind(A, $thf(sk5))]])).
% 9.98/3.73 thf(466,plain,(! [B:$i,A:$i] : (sk1 | ~ (($true)) | (rel_s5 @ B @ A) | ((rel_s5 @ sk5 @ (sk3 @ sk5)) != (rel_s5 @ A @ B)))),inference(paramod_ordered,[status(thm)],[389,27])).
% 9.98/3.73 thf(467,plain,(! [B:$i,A:$i] : (sk1 | (rel_s5 @ B @ A) | ((rel_s5 @ sk5 @ (sk3 @ sk5)) != (rel_s5 @ A @ B)))),inference(simp,[status(thm)],[466])).
% 9.98/3.73 thf(468,plain,(sk1 | (rel_s5 @ (sk3 @ sk5) @ sk5)),inference(pattern_uni,[status(thm)],[467:[bind(A, $thf(sk5)),bind(B, $thf(sk3 @ sk5))]])).
% 9.98/3.73 thf(44,plain,(! [B:$i,A:$i] : (~ (sk1) | (~ (rel_s5 @ sk8 @ A)) | (~ (p @ (sk9 @ B @ A))) | ((rel_s5 @ A @ B) != (rel_s5 @ sk8 @ A)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[19])).
% 9.98/3.73 thf(46,plain,(~ (sk1) | (~ (rel_s5 @ sk8 @ sk8)) | (~ (p @ (sk9 @ sk8 @ sk8)))),inference(pattern_uni,[status(thm)],[44:[bind(A, $thf(sk8)),bind(B, $thf(sk8))]])).
% 9.98/3.73 thf(184,plain,(~ (sk1) | ~ (($true)) | (~ (p @ (sk9 @ sk8 @ sk8)))),inference(rewrite,[status(thm)],[46,23])).
% 9.98/3.73 thf(185,plain,(~ (sk1) | (~ (p @ (sk9 @ sk8 @ sk8)))),inference(simp,[status(thm)],[184])).
% 9.98/3.73 thf(4,axiom,((mtransitive @ rel_s5)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2)).
% 9.98/3.73 thf(24,plain,((! [A:$i,B:$i,C:$i]: (((rel_s5 @ A @ B) & (rel_s5 @ B @ C)) => (rel_s5 @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 9.98/3.73 thf(194,plain,(! [B:$i,A:$i] : (~ (($true)) | (p @ B) | sk1 | ((rel_s5 @ A @ A) != (rel_s5 @ (sk4 @ sk2) @ B)))),inference(paramod_ordered,[status(thm)],[23,91])).
% 9.98/3.73 thf(195,plain,(! [B:$i,A:$i] : ((p @ B) | sk1 | ((rel_s5 @ A @ A) != (rel_s5 @ (sk4 @ sk2) @ B)))),inference(simp,[status(thm)],[194])).
% 9.98/3.73 thf(196,plain,((p @ (sk4 @ sk2)) | sk1),inference(pattern_uni,[status(thm)],[195:[bind(A, $thf(sk4 @ sk2)),bind(B, $thf(sk4 @ sk2))]])).
% 9.98/3.73 thf(214,plain,(sk1 | ~ (($true)) | sk1 | ((p @ (sk4 @ sk2)) != (p @ sk6))),inference(paramod_ordered,[status(thm)],[196,12])).
% 9.98/3.73 thf(215,plain,(sk1 | ((p @ (sk4 @ sk2)) != (p @ sk6))),inference(simp,[status(thm)],[214])).
% 9.98/3.73 thf(220,plain,(sk1 | ((sk4 @ sk2) != sk6)),inference(simp,[status(thm)],[215])).
% 9.98/3.73 thf(404,plain,(! [B:$i,A:$i] : (~ (($true)) | (rel_s5 @ B @ (sk3 @ B)) | sk1 | ((rel_s5 @ A @ A) != (rel_s5 @ sk2 @ B)))),inference(paramod_ordered,[status(thm)],[23,16])).
% 9.98/3.73 thf(405,plain,(! [B:$i,A:$i] : ((rel_s5 @ B @ (sk3 @ B)) | sk1 | ((rel_s5 @ A @ A) != (rel_s5 @ sk2 @ B)))),inference(simp,[status(thm)],[404])).
% 9.98/3.73 thf(406,plain,((rel_s5 @ sk2 @ (sk3 @ sk2)) | sk1),inference(pattern_uni,[status(thm)],[405:[bind(A, $thf(sk2)),bind(B, $thf(sk2))]])).
% 9.98/3.73 thf(497,plain,(! [B:$i,A:$i] : (sk1 | ~ (($true)) | (rel_s5 @ B @ A) | ((rel_s5 @ sk2 @ (sk3 @ sk2)) != (rel_s5 @ A @ B)))),inference(paramod_ordered,[status(thm)],[406,27])).
% 9.98/3.73 thf(498,plain,(! [B:$i,A:$i] : (sk1 | (rel_s5 @ B @ A) | ((rel_s5 @ sk2 @ (sk3 @ sk2)) != (rel_s5 @ A @ B)))),inference(simp,[status(thm)],[497])).
% 9.98/3.73 thf(499,plain,(sk1 | (rel_s5 @ (sk3 @ sk2) @ sk2)),inference(pattern_uni,[status(thm)],[498:[bind(A, $thf(sk2)),bind(B, $thf(sk3 @ sk2))]])).
% 9.98/3.73 thf(107,plain,(! [B:$i,A:$i] : (sk1 | ~ (($true)) | (rel_s5 @ B @ A) | ((rel_s5 @ sk2 @ sk5) != (rel_s5 @ A @ B)))),inference(paramod_ordered,[status(thm)],[9,27])).
% 9.98/3.73 thf(108,plain,(! [B:$i,A:$i] : (sk1 | (rel_s5 @ B @ A) | ((rel_s5 @ sk2 @ sk5) != (rel_s5 @ A @ B)))),inference(simp,[status(thm)],[107])).
% 9.98/3.73 thf(109,plain,(sk1 | (rel_s5 @ sk5 @ sk2)),inference(pattern_uni,[status(thm)],[108:[bind(A, $thf(sk2)),bind(B, $thf(sk5))]])).
% 9.98/3.73 thf(486,plain,(! [A:$i] : (sk1 | ~ (($true)) | (rel_s5 @ A @ (sk3 @ A)) | sk1 | ((rel_s5 @ sk2 @ (sk3 @ sk2)) != (rel_s5 @ sk2 @ A)))),inference(paramod_ordered,[status(thm)],[406,16])).
% 9.98/3.73 thf(487,plain,(! [A:$i] : (sk1 | (rel_s5 @ A @ (sk3 @ A)) | ((rel_s5 @ sk2 @ (sk3 @ sk2)) != (rel_s5 @ sk2 @ A)))),inference(simp,[status(thm)],[486])).
% 9.98/3.73 thf(488,plain,(sk1 | (rel_s5 @ (sk3 @ sk2) @ (sk3 @ (sk3 @ sk2)))),inference(pattern_uni,[status(thm)],[487:[bind(A, $thf(sk3 @ sk2))]])).
% 9.98/3.73 thf(35,plain,(! [B:$i,A:$i] : (~ (sk1) | ~ (sk1) | (~ (rel_s5 @ sk8 @ A)) | ~ (($true)) | (~ (p @ (sk9 @ B @ A))) | ((rel_s5 @ sk7 @ sk8) != (rel_s5 @ A @ B)))),inference(paramod_ordered,[status(thm)],[11,19])).
% 9.98/3.73 thf(36,plain,(! [B:$i,A:$i] : (~ (sk1) | (~ (rel_s5 @ sk8 @ A)) | (~ (p @ (sk9 @ B @ A))) | ((rel_s5 @ sk7 @ sk8) != (rel_s5 @ A @ B)))),inference(simp,[status(thm)],[35])).
% 9.98/3.73 thf(37,plain,(~ (sk1) | (~ (rel_s5 @ sk8 @ sk7)) | (~ (p @ (sk9 @ sk8 @ sk7)))),inference(pattern_uni,[status(thm)],[36:[bind(A, $thf(sk7)),bind(B, $thf(sk8))]])).
% 9.98/3.73 thf(171,plain,(~ (sk1) | ~ (sk1) | ~ (($true)) | (~ (p @ (sk9 @ sk8 @ sk7))) | ((rel_s5 @ sk8 @ sk7) != (rel_s5 @ sk8 @ sk7))),inference(paramod_ordered,[status(thm)],[118,37])).
% 9.98/3.73 thf(172,plain,(~ (sk1) | (~ (p @ (sk9 @ sk8 @ sk7))) | ((rel_s5 @ sk8 @ sk7) != (rel_s5 @ sk8 @ sk7))),inference(simp,[status(thm)],[171])).
% 9.98/3.73 thf(173,plain,(~ (sk1) | (~ (p @ (sk9 @ sk8 @ sk7)))),inference(pattern_uni,[status(thm)],[172:[]])).
% 9.98/3.73 thf(284,plain,(! [B:$i,A:$i] : (sk1 | ~ (($true)) | (rel_s5 @ B @ A) | ((rel_s5 @ (sk3 @ sk5) @ (sk4 @ sk5)) != (rel_s5 @ A @ B)))),inference(paramod_ordered,[status(thm)],[227,27])).
% 9.98/3.73 thf(285,plain,(! [B:$i,A:$i] : (sk1 | (rel_s5 @ B @ A) | ((rel_s5 @ (sk3 @ sk5) @ (sk4 @ sk5)) != (rel_s5 @ A @ B)))),inference(simp,[status(thm)],[284])).
% 9.98/3.73 thf(286,plain,(sk1 | (rel_s5 @ (sk4 @ sk5) @ (sk3 @ sk5))),inference(pattern_uni,[status(thm)],[285:[bind(A, $thf(sk3 @ sk5)),bind(B, $thf(sk4 @ sk5))]])).
% 9.98/3.73 thf(188,plain,(! [A:$i] : (sk1 | ~ (($true)) | (p @ A) | sk1 | ((rel_s5 @ (sk4 @ sk2) @ A) != (rel_s5 @ sk5 @ sk2)))),inference(paramod_ordered,[status(thm)],[109,91])).
% 9.98/3.73 thf(189,plain,(! [A:$i] : (sk1 | (p @ A) | ((rel_s5 @ (sk4 @ sk2) @ A) != (rel_s5 @ sk5 @ sk2)))),inference(simp,[status(thm)],[188])).
% 9.98/3.73 thf(204,plain,(! [A:$i] : (sk1 | (p @ A) | ((sk4 @ sk2) != sk5) | (A != sk2))),inference(simp,[status(thm)],[189])).
% 9.98/3.73 thf(208,plain,(sk1 | (p @ sk2) | ((sk4 @ sk2) != sk5)),inference(simp,[status(thm)],[204])).
% 9.98/3.73 thf(1165,plain,(($false)),inference(e,[status(thm)],[10,238,349,12,91,112,310,16,11,378,19,210,47,227,365,468,185,24,389,14,196,6,220,9,499,109,488,173,13,22,286,118,27,406,208,26,23])).
% 9.98/3.73 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.98/3.73 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------