%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SWV430^2 : TPTP v9.3.1. Released v3.6.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 : n007.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:39:52 AM UTC 2026
% Result : Theorem 16.30s 6.20s
% Output : Refutation 16.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV430^2 : TPTP v9.3.1. Released v3.6.0.
% 0.00/0.09 % 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.09/0.26 % Computer : n007.cluster.edu
% 0.09/0.26 % Model : x86_64 x86_64
% 0.09/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.26 % Memory : 8046.5625MB
% 0.09/0.26 % OS : Linux 6.8.0-71-generic
% 0.09/0.26 % CPULimit : 300
% 0.09/0.26 % WCLimit : 300
% 0.09/0.26 % DateTime : Tue Sep 29 16:00:55 UTC 2026
% 0.09/0.26 % CPUTime :
% 0.09/0.26 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.14/0.97 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.10/1.32 % [INFO] Parsing done (347ms).
% 2.10/1.35 % [INFO] Running in sequential loop mode.
% 2.93/1.86 % [INFO] eprover registered as external prover.
% 2.93/1.87 % [INFO] Scanning for conjecture ...
% 3.01/2.01 % [INFO] Found a conjecture (or negated_conjecture) and 2 axioms. Running axiom selection ...
% 3.29/2.04 % [INFO] Axiom selection finished. Selected 2 axioms (removed 0 axioms).
% 3.29/2.04 % [INFO] Problem is higher-order (TPTP THF).
% 3.29/2.05 % [INFO] Type checking passed.
% 3.29/2.05 % [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 ...
% 18.83/6.19 % External prover 'e' found a proof!
% 18.83/6.19 % [INFO] Killing All external provers ...
% 16.30/6.20 % Time passed: 5764ms (effective reasoning time: 4841ms)
% 16.30/6.20 % 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)>
% 16.30/6.20 % Axioms used in derivation (2): trans_axiom, refl_axiom
% 16.30/6.20 % No. of inferences in proof: 105
% 16.30/6.20 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 5764 ms resp. 4841 ms w/o parsing
% 16.83/6.33 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.83/6.33 thf(individuals_type, type, individuals: $tType).
% 16.83/6.33 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 16.83/6.33 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 16.83/6.33 thf(mimpl_decl, type, mimpl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 16.83/6.33 thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 16.83/6.33 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 16.83/6.33 thf(rel_decl, type, rel: ($i > ($i > $o))).
% 16.83/6.33 thf(icl_princ_decl, type, icl_princ: (($i > $o) > ($i > $o))).
% 16.83/6.33 thf(icl_impl_decl, type, icl_impl: (($i > $o) > (($i > $o) > ($i > $o)))).
% 16.83/6.33 thf(iclval_decl, type, iclval: (($i > $o) > $o)).
% 16.83/6.33 thf(icl_impl_princ_decl, type, icl_impl_princ: (($i > $o) > (($i > $o) > ($i > $o)))).
% 16.83/6.33 thf(a_decl, type, a: ($i > $o)).
% 16.83/6.33 thf(b_decl, type, b: ($i > $o)).
% 16.83/6.33 thf(c_decl, type, c: ($i > $o)).
% 16.83/6.33 thf(sk1_decl, type, sk1: $i).
% 16.83/6.33 thf(sk2_decl, type, sk2: $i).
% 16.83/6.33 thf(sk3_decl, type, sk3: $i).
% 16.83/6.33 thf(sk4_decl, type, sk4: $i).
% 16.83/6.33 thf(sk5_decl, type, sk5: ($i > (($i > $o) > $i))).
% 16.83/6.33 thf(sk6_decl, type, sk6: ($i > (($i > $o) > $i))).
% 16.83/6.33 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 16.83/6.33 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 16.83/6.33 thf(mimpl_def, definition, mimpl = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 16.83/6.33 thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: ((A @ C @ D) => (B @ D))) ).
% 16.83/6.33 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 16.83/6.33 thf(icl_princ_def, definition, icl_princ = (^ [A:($i > $o)]: (A)) ).
% 16.83/6.33 thf(icl_impl_def, definition, icl_impl = (^ [A:($i > $o),B:($i > $o)]: (mbox @ rel @ (mimpl @ A @ B))) ).
% 16.83/6.33 thf(iclval_def, definition, iclval = (mvalid) ).
% 16.83/6.33 thf(icl_impl_princ_def, definition, icl_impl_princ = (^ [A:($i > $o),B:($i > $o)]: (mbox @ rel @ (mimpl @ A @ B))) ).
% 16.83/6.33 thf(sk1_def, definition, sk1 = (@+ [A:$i]: ~ (! [B:$i]: ((rel @ A @ B) => (~ (! [C:$i]: ((rel @ B @ C) => (~ (a @ C) | (b @ C)))) | ! [C:$i]: ((rel @ B @ C) => (~ (! [D:$i]: ((rel @ C @ D) => (~ (b @ D) | (c @ D)))) | ! [D:$i]: ((rel @ C @ D) => (~ (a @ D) | (c @ D))))))))) ).
% 16.83/6.33 thf(sk2_def, definition, sk2 = (@+ [A:$i]: ~ ((rel @ sk1 @ A) => (~ (! [B:$i]: ((rel @ A @ B) => (~ (a @ B) | (b @ B)))) | ! [B:$i]: ((rel @ A @ B) => (~ (! [C:$i]: ((rel @ B @ C) => (~ (b @ C) | (c @ C)))) | ! [C:$i]: ((rel @ B @ C) => (~ (a @ C) | (c @ C)))))))) ).
% 16.83/6.33 thf(sk3_def, definition, sk3 = (@+ [A:$i]: ~ ((rel @ sk2 @ A) => (~ (! [B:$i]: ((rel @ A @ B) => (~ (b @ B) | (c @ B)))) | ! [B:$i]: ((rel @ A @ B) => (~ (a @ B) | (c @ B)))))) ).
% 16.83/6.33 thf(sk4_def, definition, sk4 = (@+ [A:$i]: ~ ((rel @ sk3 @ A) => (~ (a @ A) | (c @ A)))) ).
% 16.83/6.33 thf(sk5_def, definition, sk5 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((rel @ A @ C) => (B @ C)))) ).
% 16.83/6.33 thf(sk6_def, definition, sk6 = (^ [A:$i,B:($i > $o)]: (@+ [C:$i]: ~ ((rel @ A @ C) => (B @ C)))) ).
% 16.83/6.33 thf(1,conjecture,((iclval @ (icl_impl @ (icl_impl_princ @ (icl_princ @ a) @ (icl_princ @ b)) @ (icl_impl @ (icl_impl_princ @ (icl_princ @ b) @ (icl_princ @ c)) @ (icl_impl_princ @ (icl_princ @ a) @ (icl_princ @ c)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',trans)).
% 16.83/6.33 thf(2,negated_conjecture,((~ (iclval @ (icl_impl @ (icl_impl_princ @ (icl_princ @ a) @ (icl_princ @ b)) @ (icl_impl @ (icl_impl_princ @ (icl_princ @ b) @ (icl_princ @ c)) @ (icl_impl_princ @ (icl_princ @ a) @ (icl_princ @ c))))))),inference(neg_conjecture,[status(cth)],[1])).
% 16.83/6.33 thf(5,plain,((~ (! [A:$i,B:$i]: ((rel @ A @ B) => (~ (! [C:$i]: ((rel @ B @ C) => (~ (a @ C) | (b @ C)))) | ! [C:$i]: ((rel @ B @ C) => (~ (! [D:$i]: ((rel @ C @ D) => (~ (b @ D) | (c @ D)))) | ! [D:$i]: ((rel @ C @ D) => (~ (a @ D) | (c @ D)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 16.83/6.33 thf(6,plain,(! [B:$i,A:$i] : (((rel @ sk1 @ sk2) & (~ (rel @ sk2 @ A) | ~ (a @ A) | (b @ A)) & (rel @ sk2 @ sk3) & (~ (rel @ sk3 @ B) | ~ (b @ B) | (c @ B)) & (rel @ sk3 @ sk4) & (a @ sk4) & ~ (c @ sk4)))),inference(cnf,[status(esa)],[5])).
% 16.83/6.33 thf(10,plain,((a @ sk4)),inference(cnfConj,[status(thm)],[6])).
% 16.83/6.33 thf(4,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ rel @ A) @ (mbox @ rel @ (mbox @ rel @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',trans_axiom)).
% 16.83/6.33 thf(21,plain,((! [A:($i > $o),B:$i]: (~ (! [C:$i]: ((rel @ B @ C) => (A @ C))) | ! [C:$i]: ((rel @ B @ C) => (! [D:$i]: ((rel @ C @ D) => (A @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 16.83/6.33 thf(22,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((((rel @ B @ (sk6 @ B @ (A))) | ~ (rel @ B @ C) | ~ (rel @ C @ D) | (A @ D)) & (~ (A @ (sk6 @ B @ (A))) | ~ (rel @ B @ C) | ~ (rel @ C @ D) | (A @ D))))),inference(cnf,[status(esa)],[21])).
% 16.83/6.33 thf(24,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk6 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[22])).
% 16.83/6.33 thf(11,plain,(! [A:$i] : ((~ (rel @ sk3 @ A)) | (~ (b @ A)) | (c @ A))),inference(cnfConj,[status(thm)],[6])).
% 16.83/6.33 thf(14,plain,(! [A:$i] : ((~ (rel @ sk3 @ A)) | (~ (b @ A)) | (c @ A))),inference(simp,[status(thm)],[11])).
% 16.83/6.33 thf(3,axiom,((! [A:($i > $o)]: (mvalid @ (mimpl @ (mbox @ rel @ A) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',refl_axiom)).
% 16.83/6.33 thf(15,plain,((! [A:($i > $o),B:$i]: (~ (! [C:$i]: ((rel @ B @ C) => (A @ C))) | (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 16.83/6.33 thf(16,plain,(! [B:$i,A:($i > $o)] : ((((rel @ B @ (sk5 @ B @ (A))) | (A @ B)) & (~ (A @ (sk5 @ B @ (A))) | (A @ B))))),inference(cnf,[status(esa)],[15])).
% 16.83/6.33 thf(17,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk5 @ B @ (A))) | (A @ B))),inference(cnfConj,[status(thm)],[16])).
% 16.83/6.33 thf(9,plain,((rel @ sk2 @ sk3)),inference(cnfConj,[status(thm)],[6])).
% 16.83/6.33 thf(8,plain,((~ (c @ sk4))),inference(cnfConj,[status(thm)],[6])).
% 16.83/6.33 thf(51,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk6 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | ~ (($true)) | ((A @ D) != (c @ sk4)))),inference(paramod_ordered,[status(thm)],[24,8])).
% 16.83/6.33 thf(52,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((~ (A @ (sk6 @ B @ (A)))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | ((A @ D) != (c @ sk4)))),inference(simp,[status(thm)],[51])).
% 16.83/6.33 thf(96,plain,(! [B:$i,A:$i] : ((~ (c @ (sk6 @ A @ (c)))) | (~ (rel @ A @ B)) | (~ (rel @ B @ sk4)))),inference(pre_uni,[status(thm)],[52:[bind(A, $thf(c)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(sk4))]])).
% 16.83/6.33 thf(127,plain,(! [B:$i,A:$i] : ((~ (c @ (sk6 @ A @ (c)))) | (~ (rel @ A @ B)) | (~ (rel @ B @ sk4)))),inference(simp,[status(thm)],[96])).
% 16.83/6.33 thf(259,plain,(! [B:$i,A:$i] : ((~ (c @ (sk6 @ A @ (c)))) | ~ (($true)) | (~ (rel @ B @ sk4)) | ((rel @ sk2 @ sk3) != (rel @ A @ B)))),inference(paramod_ordered,[status(thm)],[9,127])).
% 16.83/6.33 thf(260,plain,(! [B:$i,A:$i] : ((~ (c @ (sk6 @ A @ (c)))) | (~ (rel @ B @ sk4)) | ((rel @ sk2 @ sk3) != (rel @ A @ B)))),inference(simp,[status(thm)],[259])).
% 16.83/6.33 thf(261,plain,((~ (c @ (sk6 @ sk2 @ (c)))) | (~ (rel @ sk3 @ sk4))),inference(pattern_uni,[status(thm)],[260:[bind(A, $thf(sk2)),bind(B, $thf(sk3))]])).
% 16.83/6.33 thf(13,plain,((rel @ sk3 @ sk4)),inference(cnfConj,[status(thm)],[6])).
% 16.83/6.33 thf(1137,plain,((~ (c @ (sk6 @ sk2 @ (c)))) | ~ (($true))),inference(rewrite,[status(thm)],[261,13])).
% 16.83/6.33 thf(1138,plain,((~ (c @ (sk6 @ sk2 @ (c))))),inference(simp,[status(thm)],[1137])).
% 16.83/6.33 thf(1143,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk5 @ B @ (A))) | ~ (($true)) | ((A @ B) != (c @ (sk6 @ sk2 @ (c)))))),inference(paramod_ordered,[status(thm)],[17,1138])).
% 16.83/6.33 thf(1144,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk5 @ B @ (A))) | ((A @ B) != (c @ (sk6 @ sk2 @ (c)))))),inference(simp,[status(thm)],[1143])).
% 16.83/6.33 thf(1155,plain,((rel @ sk2 @ (sk5 @ sk2 @ (^ [A:$i]: (c @ (sk6 @ A @ c)))))),inference(pre_uni,[status(thm)],[1144:[bind(A, $thf(^ [C:$i]: (c @ (sk6 @ C @ c)))),bind(B, $thf(sk2))]])).
% 16.83/6.33 thf(7,plain,((rel @ sk1 @ sk2)),inference(cnfConj,[status(thm)],[6])).
% 16.83/6.33 thf(12,plain,(! [A:$i] : ((~ (rel @ sk2 @ A)) | (~ (a @ A)) | (b @ A))),inference(cnfConj,[status(thm)],[6])).
% 16.83/6.33 thf(181,plain,(! [A:$i] : (~ (($true)) | (~ (a @ A)) | (b @ A) | ((rel @ sk2 @ A) != (rel @ sk1 @ sk2)))),inference(paramod_ordered,[status(thm)],[7,12])).
% 16.83/6.33 thf(182,plain,(! [A:$i] : ((~ (a @ A)) | (b @ A) | ((rel @ sk2 @ A) != (rel @ sk1 @ sk2)))),inference(simp,[status(thm)],[181])).
% 16.83/6.33 thf(186,plain,(! [A:$i] : ((b @ A) | (~ (a @ A)) | (sk2 != sk1) | (A != sk2))),inference(simp,[status(thm)],[182])).
% 16.83/6.33 thf(191,plain,((b @ sk2) | (~ (a @ sk2)) | (sk2 != sk1)),inference(simp,[status(thm)],[186])).
% 16.83/6.33 thf(176,plain,(! [A:$i] : (~ (($true)) | (~ (a @ A)) | (b @ A) | ((rel @ sk2 @ sk3) != (rel @ sk2 @ A)))),inference(paramod_ordered,[status(thm)],[9,12])).
% 16.83/6.33 thf(177,plain,(! [A:$i] : ((~ (a @ A)) | (b @ A) | ((rel @ sk2 @ sk3) != (rel @ sk2 @ A)))),inference(simp,[status(thm)],[176])).
% 16.83/6.33 thf(178,plain,((~ (a @ sk3)) | (b @ sk3)),inference(pattern_uni,[status(thm)],[177:[bind(A, $thf(sk3))]])).
% 16.83/6.33 thf(193,plain,(~ (($true)) | (b @ sk3) | ((a @ sk4) != (a @ sk3))),inference(paramod_ordered,[status(thm)],[10,178])).
% 16.83/6.33 thf(194,plain,((b @ sk3) | ((a @ sk4) != (a @ sk3))),inference(simp,[status(thm)],[193])).
% 16.83/6.33 thf(199,plain,((b @ sk3) | (sk4 != sk3)),inference(simp,[status(thm)],[194])).
% 16.83/6.33 thf(212,plain,(! [A:$i] : (~ (($true)) | (~ (b @ A)) | (c @ A) | ((rel @ sk3 @ sk4) != (rel @ sk3 @ A)))),inference(paramod_ordered,[status(thm)],[13,14])).
% 16.83/6.33 thf(213,plain,(! [A:$i] : ((~ (b @ A)) | (c @ A) | ((rel @ sk3 @ sk4) != (rel @ sk3 @ A)))),inference(simp,[status(thm)],[212])).
% 16.83/6.33 thf(214,plain,((~ (b @ sk4)) | (c @ sk4)),inference(pattern_uni,[status(thm)],[213:[bind(A, $thf(sk4))]])).
% 16.83/6.33 thf(237,plain,((~ (b @ sk4)) | ($false)),inference(rewrite,[status(thm)],[214,8])).
% 16.83/6.33 thf(238,plain,((~ (b @ sk4))),inference(simp,[status(thm)],[237])).
% 16.83/6.33 thf(241,plain,((sk4 != sk3) | ~ (($true)) | ((b @ sk4) != (b @ sk3))),inference(paramod_ordered,[status(thm)],[199,238])).
% 16.83/6.33 thf(242,plain,((sk4 != sk3) | ((b @ sk4) != (b @ sk3))),inference(simp,[status(thm)],[241])).
% 16.83/6.33 thf(247,plain,((sk4 != sk3) | (sk4 != sk3)),inference(simp,[status(thm)],[242])).
% 16.83/6.33 thf(251,plain,((sk4 != sk3)),inference(simp,[status(thm)],[247])).
% 16.83/6.33 thf(169,plain,(! [A:$i] : ((~ (rel @ sk2 @ A)) | ~ (($true)) | (b @ A) | ((a @ sk4) != (a @ A)))),inference(paramod_ordered,[status(thm)],[10,12])).
% 16.83/6.33 thf(170,plain,(! [A:$i] : ((~ (rel @ sk2 @ A)) | (b @ A) | ((a @ sk4) != (a @ A)))),inference(simp,[status(thm)],[169])).
% 16.83/6.33 thf(171,plain,((~ (rel @ sk2 @ sk4)) | (b @ sk4)),inference(pattern_uni,[status(thm)],[170:[bind(A, $thf(sk4))]])).
% 16.83/6.33 thf(430,plain,((~ (rel @ sk2 @ sk4)) | ($false)),inference(rewrite,[status(thm)],[171,238])).
% 16.83/6.33 thf(431,plain,((~ (rel @ sk2 @ sk4))),inference(simp,[status(thm)],[430])).
% 16.83/6.33 thf(18,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk5 @ B @ (A)))) | (A @ B))),inference(cnfConj,[status(thm)],[16])).
% 16.83/6.33 thf(312,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk5 @ B @ (A))) | ~ (($true)) | ((A @ B) != (b @ sk4)))),inference(paramod_ordered,[status(thm)],[17,238])).
% 16.83/6.33 thf(313,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk5 @ B @ (A))) | ((A @ B) != (b @ sk4)))),inference(simp,[status(thm)],[312])).
% 16.83/6.33 thf(377,plain,((rel @ sk4 @ (sk5 @ sk4 @ (b)))),inference(pre_uni,[status(thm)],[313:[bind(A, $thf(b)),bind(B, $thf(sk4))]])).
% 16.83/6.33 thf(580,plain,(~ (($true)) | ((rel @ sk4 @ (sk5 @ sk4 @ (b))) != (rel @ sk2 @ sk4))),inference(paramod_ordered,[status(thm)],[377,431])).
% 16.83/6.33 thf(581,plain,(((rel @ sk4 @ (sk5 @ sk4 @ (b))) != (rel @ sk2 @ sk4))),inference(simp,[status(thm)],[580])).
% 16.83/6.33 thf(595,plain,((sk4 != sk2) | ((sk5 @ sk4 @ (b)) != sk4)),inference(simp,[status(thm)],[581])).
% 16.83/6.33 thf(23,plain,(! [D:$i,C:$i,B:$i,A:($i > $o)] : ((rel @ B @ (sk6 @ B @ (A))) | (~ (rel @ B @ C)) | (~ (rel @ C @ D)) | (A @ D))),inference(cnfConj,[status(thm)],[22])).
% 16.83/6.33 thf(440,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk5 @ B @ (A))) | ~ (($true)) | ((A @ B) != (rel @ sk2 @ sk4)))),inference(paramod_ordered,[status(thm)],[17,431])).
% 16.83/6.33 thf(441,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk5 @ B @ (A))) | ((A @ B) != (rel @ sk2 @ sk4)))),inference(simp,[status(thm)],[440])).
% 16.83/6.33 thf(449,plain,((rel @ sk4 @ (sk5 @ sk4 @ (rel @ sk2)))),inference(pre_uni,[status(thm)],[441:[bind(A, $thf(rel @ sk2)),bind(B, $thf(sk4))]])).
% 16.83/6.33 thf(334,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk5 @ B @ (A))) | ~ (($true)) | (b @ sk3) | ((A @ B) != (a @ sk3)))),inference(paramod_ordered,[status(thm)],[17,178])).
% 16.83/6.33 thf(335,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk5 @ B @ (A))) | (b @ sk3) | ((A @ B) != (a @ sk3)))),inference(simp,[status(thm)],[334])).
% 16.83/6.33 thf(379,plain,((rel @ sk3 @ (sk5 @ sk3 @ (a))) | (b @ sk3)),inference(pre_uni,[status(thm)],[335:[bind(A, $thf(a)),bind(B, $thf(sk3))]])).
% 16.83/6.33 thf(19,plain,(! [B:$i,A:($i > $o)] : ((~ ((sk5 @ B @ (A)) = (sk5 @ B @ ((=) @ $i @ (sk5 @ B @ A))))) | ((sk5 @ B @ (A)) = B))),inference(replace_leibeq,[status(thm)],[18:[bind(A, $thf((=) @ $i @ (sk5 @ B @ A)))]])).
% 16.83/6.33 thf(20,plain,(! [B:$i,A:($i > $o)] : (((sk5 @ B @ (A)) != (sk5 @ B @ ((=) @ $i @ (sk5 @ B @ A)))) | ((sk5 @ B @ (A)) = B))),inference(lifteq,[status(thm)],[19])).
% 16.83/6.33 thf(448,plain,((rel @ sk2 @ (sk5 @ sk2 @ (^ [A:$i]: (rel @ A @ sk4))))),inference(pre_uni,[status(thm)],[441:[bind(A, $thf(^ [C:$i]: (rel @ C @ sk4))),bind(B, $thf(sk2))]])).
% 16.83/6.33 thf(337,plain,(! [A:$i] : ((rel @ A @ (sk5 @ A @ (^ [B:$i]: (($false))))) | ($false))),inference(prim_subst,[status(thm)],[17:[bind(A, $thf(^ [C:$i]: (($false))))]])).
% 16.83/6.33 thf(395,plain,(! [A:$i] : ((rel @ A @ (sk5 @ A @ (^ [B:$i]: (($false))))))),inference(simp,[status(thm)],[337])).
% 16.83/6.33 thf(725,plain,(! [A:$i] : (~ (($true)) | ((rel @ A @ (sk5 @ A @ (^ [B:$i]: (($false))))) != (rel @ sk2 @ sk4)))),inference(paramod_ordered,[status(thm)],[395,431])).
% 16.83/6.33 thf(726,plain,(! [A:$i] : (((rel @ A @ (sk5 @ A @ (^ [B:$i]: (($false))))) != (rel @ sk2 @ sk4)))),inference(simp,[status(thm)],[725])).
% 16.83/6.33 thf(746,plain,(! [A:$i] : ((A != sk2) | ((sk5 @ A @ (^ [B:$i]: (($false)))) != sk4))),inference(simp,[status(thm)],[726])).
% 16.83/6.33 thf(756,plain,(((sk5 @ sk2 @ (^ [A:$i]: (($false)))) != sk4)),inference(simp,[status(thm)],[746])).
% 16.83/6.33 thf(436,plain,(~ (($true)) | ((rel @ sk3 @ sk4) != (rel @ sk2 @ sk4))),inference(paramod_ordered,[status(thm)],[13,431])).
% 16.83/6.33 thf(437,plain,(((rel @ sk3 @ sk4) != (rel @ sk2 @ sk4))),inference(simp,[status(thm)],[436])).
% 16.83/6.33 thf(453,plain,((sk3 != sk2) | (sk4 != sk4)),inference(simp,[status(thm)],[437])).
% 16.83/6.33 thf(457,plain,((sk3 != sk2)),inference(simp,[status(thm)],[453])).
% 16.83/6.33 thf(442,plain,(~ (($true)) | ((rel @ sk2 @ sk4) != (rel @ sk1 @ sk2))),inference(paramod_ordered,[status(thm)],[7,431])).
% 16.83/6.33 thf(443,plain,(((rel @ sk2 @ sk4) != (rel @ sk1 @ sk2))),inference(simp,[status(thm)],[442])).
% 16.83/6.33 thf(444,plain,((sk2 != sk1) | (sk4 != sk2)),inference(simp,[status(thm)],[443])).
% 16.83/6.33 thf(332,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk5 @ B @ (A))) | ~ (($true)) | ((A @ B) != (c @ sk4)))),inference(paramod_ordered,[status(thm)],[17,8])).
% 16.83/6.33 thf(333,plain,(! [B:$i,A:($i > $o)] : ((rel @ B @ (sk5 @ B @ (A))) | ((A @ B) != (c @ sk4)))),inference(simp,[status(thm)],[332])).
% 16.83/6.33 thf(369,plain,((rel @ sk4 @ (sk5 @ sk4 @ (c)))),inference(pre_uni,[status(thm)],[333:[bind(A, $thf(c)),bind(B, $thf(sk4))]])).
% 16.83/6.33 thf(215,plain,(! [A:$i] : (~ (($true)) | (~ (b @ A)) | (c @ A) | ((rel @ sk3 @ A) != (rel @ sk1 @ sk2)))),inference(paramod_ordered,[status(thm)],[7,14])).
% 16.83/6.33 thf(216,plain,(! [A:$i] : ((~ (b @ A)) | (c @ A) | ((rel @ sk3 @ A) != (rel @ sk1 @ sk2)))),inference(simp,[status(thm)],[215])).
% 16.83/6.33 thf(221,plain,(! [A:$i] : ((c @ A) | (~ (b @ A)) | (sk3 != sk1) | (A != sk2))),inference(simp,[status(thm)],[216])).
% 16.83/6.33 thf(227,plain,((c @ sk2) | (~ (b @ sk2)) | (sk3 != sk1)),inference(simp,[status(thm)],[221])).
% 16.83/6.33 thf(543,plain,(~ (($true)) | ((rel @ sk4 @ (sk5 @ sk4 @ (c))) != (rel @ sk2 @ sk4))),inference(paramod_ordered,[status(thm)],[369,431])).
% 16.83/6.33 thf(544,plain,(((rel @ sk4 @ (sk5 @ sk4 @ (c))) != (rel @ sk2 @ sk4))),inference(simp,[status(thm)],[543])).
% 16.83/6.33 thf(560,plain,((sk4 != sk2) | ((sk5 @ sk4 @ (c)) != sk4)),inference(simp,[status(thm)],[544])).
% 16.83/6.33 thf(618,plain,(~ (($true)) | ((rel @ sk2 @ (sk5 @ sk2 @ (^ [A:$i]: (rel @ A @ sk4)))) != (rel @ sk2 @ sk4))),inference(paramod_ordered,[status(thm)],[448,431])).
% 16.83/6.33 thf(619,plain,(((rel @ sk2 @ (sk5 @ sk2 @ (^ [A:$i]: (rel @ A @ sk4)))) != (rel @ sk2 @ sk4))),inference(simp,[status(thm)],[618])).
% 16.83/6.33 thf(632,plain,((sk2 != sk2) | ((sk5 @ sk2 @ (^ [A:$i]: (rel @ A @ sk4))) != sk4)),inference(simp,[status(thm)],[619])).
% 16.83/6.33 thf(639,plain,(((sk5 @ sk2 @ (^ [A:$i]: (rel @ A @ sk4))) != sk4)),inference(simp,[status(thm)],[632])).
% 16.83/6.33 thf(1177,plain,(~ (($true)) | ((rel @ sk2 @ (sk5 @ sk2 @ (^ [A:$i]: (c @ (sk6 @ A @ c))))) != (rel @ sk2 @ sk4))),inference(paramod_ordered,[status(thm)],[1155,431])).
% 16.83/6.33 thf(1178,plain,(((rel @ sk2 @ (sk5 @ sk2 @ (^ [A:$i]: (c @ (sk6 @ A @ c))))) != (rel @ sk2 @ sk4))),inference(simp,[status(thm)],[1177])).
% 16.83/6.33 thf(1198,plain,((sk2 != sk2) | ((sk5 @ sk2 @ (^ [A:$i]: (c @ (sk6 @ A @ c)))) != sk4)),inference(simp,[status(thm)],[1178])).
% 16.83/6.33 thf(1204,plain,(((sk5 @ sk2 @ (^ [A:$i]: (c @ (sk6 @ A @ c)))) != sk4)),inference(simp,[status(thm)],[1198])).
% 16.83/6.33 thf(1323,plain,(($false)),inference(e,[status(thm)],[10,24,14,21,1155,191,12,251,431,18,127,595,23,8,5,449,379,20,448,756,238,9,1138,457,13,17,444,377,7,395,15,178,369,227,560,639,1204])).
% 16.83/6.33 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.83/6.33 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------