%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU189+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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 : Thu Sep 24 02:21:56 PM UTC 2026
% Result : Theorem 0.14s 5.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU189+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.54 % Computer : n004.cluster.edu
% 0.11/5.54 % Model : x86_64 x86_64
% 0.11/5.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.54 % Memory : 8046.5625MB
% 0.11/5.54 % OS : Linux 6.8.0-71-generic
% 0.11/5.54 % CPULimit : 300
% 0.11/5.54 % WCLimit : 300
% 0.11/5.54 % DateTime : Mon Sep 21 05:56:27 UTC 2026
% 0.11/5.54 % CPUTime :
% 0.11/5.56 % Drodi V4.1.1
% 0.14/5.60 % Refutation found
% 0.14/5.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/5.60 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.60 fof(f3,axiom,(
% 0.14/5.60 (! [A] :( empty(A)=> relation(A) ) )),
% 0.14/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f57,axiom,(
% 0.14/5.60 empty(empty_set) ),
% 0.14/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f64,axiom,(
% 0.14/5.60 ( empty(empty_set)& relation(empty_set) ) ),
% 0.14/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f66,axiom,(
% 0.14/5.60 (! [A] :( ( ~ empty(A)& relation(A) )=> ~ empty(relation_dom(A)) ) )),
% 0.14/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f67,axiom,(
% 0.14/5.60 (! [A] :( ( ~ empty(A)& relation(A) )=> ~ empty(relation_rng(A)) ) )),
% 0.14/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f68,axiom,(
% 0.14/5.60 (! [A] :( empty(A)=> ( empty(relation_dom(A))& relation(relation_dom(A)) ) ) )),
% 0.14/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f69,axiom,(
% 0.14/5.60 (! [A] :( empty(A)=> ( empty(relation_rng(A))& relation(relation_rng(A)) ) ) )),
% 0.14/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f88,axiom,(
% 0.14/5.60 (? [A] :( empty(A)& relation(A) ) )),
% 0.14/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f90,axiom,(
% 0.14/5.60 (? [A] : empty(A) )),
% 0.14/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f113,lemma,(
% 0.14/5.60 (! [A] :( relation(A)=> (! [B] :( relation(B)=> ( subset(A,B)=> ( subset(relation_dom(A),relation_dom(B))& subset(relation_rng(A),relation_rng(B)) ) ) ) )) )),
% 0.14/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f119,lemma,(
% 0.14/5.60 (! [A] : subset(empty_set,A) )),
% 0.14/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f157,conjecture,(
% 0.14/5.60 (! [A] :( relation(A)=> ( relation_dom(A) = empty_set<=> relation_rng(A) = empty_set ) ) )),
% 0.14/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f158,negated_conjecture,(
% 0.14/5.60 ~((! [A] :( relation(A)=> ( relation_dom(A) = empty_set<=> relation_rng(A) = empty_set ) ) ))),
% 0.14/5.60 inference(negated_conjecture,[status(cth)],[f157])).
% 0.14/5.60 fof(f161,axiom,(
% 0.14/5.60 (! [A] :( empty(A)=> A = empty_set ) )),
% 0.14/5.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/5.60 fof(f177,plain,(
% 0.14/5.60 ![A]: (~empty(A)|relation(A))),
% 0.14/5.60 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.14/5.60 fof(f178,plain,(
% 0.14/5.60 ![X0]: (~empty(X0)|relation(X0))),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f177])).
% 0.14/5.60 fof(f368,plain,(
% 0.14/5.60 empty(empty_set)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f57])).
% 0.14/5.60 fof(f381,plain,(
% 0.14/5.60 relation(empty_set)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f64])).
% 0.14/5.60 fof(f384,plain,(
% 0.14/5.60 ![A]: ((empty(A)|~relation(A))|~empty(relation_dom(A)))),
% 0.14/5.60 inference(pre_NNF_transformation,[status(thm)],[f66])).
% 0.14/5.60 fof(f385,plain,(
% 0.14/5.60 ![X0]: (empty(X0)|~relation(X0)|~empty(relation_dom(X0)))),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f384])).
% 0.14/5.60 fof(f386,plain,(
% 0.14/5.60 ![A]: ((empty(A)|~relation(A))|~empty(relation_rng(A)))),
% 0.14/5.60 inference(pre_NNF_transformation,[status(thm)],[f67])).
% 0.14/5.60 fof(f387,plain,(
% 0.14/5.60 ![X0]: (empty(X0)|~relation(X0)|~empty(relation_rng(X0)))),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f386])).
% 0.14/5.60 fof(f388,plain,(
% 0.14/5.60 ![A]: (~empty(A)|(empty(relation_dom(A))&relation(relation_dom(A))))),
% 0.14/5.60 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 0.14/5.60 fof(f389,plain,(
% 0.14/5.60 ![X0]: (~empty(X0)|empty(relation_dom(X0)))),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f388])).
% 0.14/5.60 fof(f391,plain,(
% 0.14/5.60 ![A]: (~empty(A)|(empty(relation_rng(A))&relation(relation_rng(A))))),
% 0.14/5.60 inference(pre_NNF_transformation,[status(thm)],[f69])).
% 0.14/5.60 fof(f392,plain,(
% 0.14/5.60 ![X0]: (~empty(X0)|empty(relation_rng(X0)))),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f391])).
% 0.14/5.60 fof(f442,plain,(
% 0.14/5.60 (empty(sK37_skl)&relation(sK37_skl))),
% 0.14/5.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK37_skl]),skolemize(A,sK37_skl)],[f88])).
% 0.14/5.60 fof(f443,plain,(
% 0.14/5.60 empty(sK37_skl)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f442])).
% 0.14/5.60 fof(f444,plain,(
% 0.14/5.60 relation(sK37_skl)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f442])).
% 0.14/5.60 fof(f449,plain,(
% 0.14/5.60 empty(sK39_skl)),
% 0.14/5.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK39_skl]),skolemize(A,sK39_skl)],[f90])).
% 0.14/5.60 fof(f450,plain,(
% 0.14/5.60 empty(sK39_skl)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f449])).
% 0.14/5.60 fof(f508,plain,(
% 0.14/5.60 ![A]: (~relation(A)|(![B]: (~relation(B)|(~subset(A,B)|(subset(relation_dom(A),relation_dom(B))&subset(relation_rng(A),relation_rng(B)))))))),
% 0.14/5.60 inference(pre_NNF_transformation,[status(thm)],[f113])).
% 0.14/5.60 fof(f509,plain,(
% 0.14/5.60 ![X0,X1]: (~relation(X0)|~relation(X1)|~subset(X0,X1)|subset(relation_dom(X0),relation_dom(X1)))),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f508])).
% 0.14/5.60 fof(f510,plain,(
% 0.14/5.60 ![X0,X1]: (~relation(X0)|~relation(X1)|~subset(X0,X1)|subset(relation_rng(X0),relation_rng(X1)))),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f508])).
% 0.14/5.60 fof(f524,plain,(
% 0.14/5.60 ![X0]: (subset(empty_set,X0))),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f119])).
% 0.14/5.60 fof(f625,plain,(
% 0.14/5.60 (?[A]: (relation(A)&(relation_dom(A)=empty_set<~>relation_rng(A)=empty_set)))),
% 0.14/5.60 inference(pre_NNF_transformation,[status(thm)],[f158])).
% 0.14/5.60 fof(f626,plain,(
% 0.14/5.60 ?[A]: (relation(A)&((relation_dom(A)=empty_set|relation_rng(A)=empty_set)&(~relation_dom(A)=empty_set|~relation_rng(A)=empty_set)))),
% 0.14/5.60 inference(NNF_transformation,[status(thm)],[f625])).
% 0.14/5.60 fof(f627,plain,(
% 0.14/5.60 (relation(sK49_skl)&((relation_dom(sK49_skl)=empty_set|relation_rng(sK49_skl)=empty_set)&(~relation_dom(sK49_skl)=empty_set|~relation_rng(sK49_skl)=empty_set)))),
% 0.14/5.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK49_skl]),skolemize(A,sK49_skl)],[f626])).
% 0.14/5.60 fof(f628,plain,(
% 0.14/5.60 relation(sK49_skl)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f627])).
% 0.14/5.60 fof(f629,plain,(
% 0.14/5.60 relation_dom(sK49_skl)=empty_set|relation_rng(sK49_skl)=empty_set),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f627])).
% 0.14/5.60 fof(f630,plain,(
% 0.14/5.60 ~relation_dom(sK49_skl)=empty_set|~relation_rng(sK49_skl)=empty_set),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f627])).
% 0.14/5.60 fof(f636,plain,(
% 0.14/5.60 ![A]: (~empty(A)|A=empty_set)),
% 0.14/5.60 inference(pre_NNF_transformation,[status(thm)],[f161])).
% 0.14/5.60 fof(f637,plain,(
% 0.14/5.60 ![X0]: (~empty(X0)|X0=empty_set)),
% 0.14/5.60 inference(cnf_transformation,[status(thm)],[f636])).
% 0.14/5.60 fof(f676,definition,(
% 0.14/5.61 sQ0_spl <=> (relation_dom(sK49_skl)=empty_set)),
% 0.14/5.61 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/5.61 fof(f677,plain,(
% 0.14/5.61 relation_dom(sK49_skl)=empty_set|~sQ0_spl),
% 0.14/5.61 inference(component_clause,[status(thm)],[f676])).
% 0.14/5.61 fof(f679,definition,(
% 0.14/5.61 sQ1_spl <=> (relation_rng(sK49_skl)=empty_set)),
% 0.14/5.61 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/5.61 fof(f680,plain,(
% 0.14/5.61 relation_rng(sK49_skl)=empty_set|~sQ1_spl),
% 0.14/5.61 inference(component_clause,[status(thm)],[f679])).
% 0.14/5.61 fof(f681,plain,(
% 0.14/5.61 ~relation_rng(sK49_skl)=empty_set|sQ1_spl),
% 0.14/5.61 inference(component_clause,[status(thm)],[f679])).
% 0.14/5.61 fof(f682,plain,(
% 0.14/5.61 sQ0_spl|sQ1_spl),
% 0.14/5.61 inference(split_clause,[status(thm)],[f629,f676,f679])).
% 0.14/5.61 fof(f683,plain,(
% 0.14/5.61 ~sQ0_spl|~sQ1_spl),
% 0.14/5.61 inference(split_clause,[status(thm)],[f630,f676,f679])).
% 0.14/5.61 fof(f732,definition,(
% 0.14/5.61 sQ2_spl <=> (empty(empty_set))),
% 0.14/5.61 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/5.61 fof(f734,plain,(
% 0.14/5.61 ~empty(empty_set)|sQ2_spl),
% 0.14/5.61 inference(component_clause,[status(thm)],[f732])).
% 0.14/5.61 fof(f735,definition,(
% 0.14/5.61 sQ3_spl <=> (relation(empty_set))),
% 0.14/5.61 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/5.61 fof(f737,plain,(
% 0.14/5.61 ~relation(empty_set)|sQ3_spl),
% 0.14/5.61 inference(component_clause,[status(thm)],[f735])).
% 0.14/5.61 fof(f739,plain,(
% 0.14/5.61 empty(sK49_skl)|~relation(sK49_skl)|~empty(empty_set)|~sQ0_spl),
% 0.14/5.61 inference(paramodulation,[status(thm)],[f677,f385])).
% 0.14/5.61 fof(f740,definition,(
% 0.14/5.61 sQ4_spl <=> (empty(sK49_skl))),
% 0.14/5.61 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/5.61 fof(f741,plain,(
% 0.14/5.61 empty(sK49_skl)|~sQ4_spl),
% 0.14/5.61 inference(component_clause,[status(thm)],[f740])).
% 0.14/5.61 fof(f743,definition,(
% 0.14/5.61 sQ5_spl <=> (relation(sK49_skl))),
% 0.14/5.61 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/5.61 fof(f745,plain,(
% 0.14/5.61 ~relation(sK49_skl)|sQ5_spl),
% 0.14/5.61 inference(component_clause,[status(thm)],[f743])).
% 0.14/5.61 fof(f746,plain,(
% 0.14/5.61 sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ0_spl),
% 0.14/5.61 inference(split_clause,[status(thm)],[f739,f740,f743,f732,f676])).
% 0.14/5.61 fof(f759,plain,(
% 0.14/5.61 empty(relation_rng(sK37_skl))),
% 0.14/5.61 inference(resolution,[status(thm)],[f443,f392])).
% 0.14/5.61 fof(f763,plain,(
% 0.14/5.61 empty(relation_rng(sK39_skl))),
% 0.14/5.61 inference(resolution,[status(thm)],[f450,f392])).
% 0.14/5.61 fof(f766,plain,(
% 0.14/5.61 $false|sQ2_spl),
% 0.14/5.61 inference(forward_subsumption_resolution,[status(thm)],[f734,f368])).
% 0.14/5.61 fof(f767,plain,(
% 0.14/5.61 sQ2_spl),
% 0.14/5.61 inference(contradiction_clause,[status(thm)],[f766])).
% 0.14/5.61 fof(f768,plain,(
% 0.14/5.61 relation(sK39_skl)),
% 0.14/5.61 inference(resolution,[status(thm)],[f178,f450])).
% 0.14/5.61 fof(f775,plain,(
% 0.14/5.61 empty(relation_dom(sK49_skl))|~sQ4_spl),
% 0.14/5.61 inference(resolution,[status(thm)],[f741,f389])).
% 0.14/5.61 fof(f798,plain,(
% 0.14/5.61 $false|sQ5_spl),
% 0.14/5.61 inference(forward_subsumption_resolution,[status(thm)],[f745,f628])).
% 0.14/5.61 fof(f799,plain,(
% 0.14/5.61 sQ5_spl),
% 0.14/5.61 inference(contradiction_clause,[status(thm)],[f798])).
% 0.14/5.61 fof(f800,plain,(
% 0.14/5.61 empty(sK37_skl)|~relation(sK37_skl)),
% 0.14/5.61 inference(resolution,[status(thm)],[f759,f387])).
% 0.14/5.61 fof(f806,definition,(
% 0.14/5.61 sQ8_spl <=> (empty(sK37_skl))),
% 0.14/5.61 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/5.61 fof(f809,definition,(
% 0.14/5.61 sQ9_spl <=> (relation(sK37_skl))),
% 0.14/5.61 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/5.61 fof(f811,plain,(
% 0.14/5.61 ~relation(sK37_skl)|sQ9_spl),
% 0.14/5.61 inference(component_clause,[status(thm)],[f809])).
% 0.14/5.61 fof(f812,plain,(
% 0.14/5.61 sQ8_spl|~sQ9_spl),
% 0.14/5.61 inference(split_clause,[status(thm)],[f800,f806,f809])).
% 0.14/5.61 fof(f813,plain,(
% 0.14/5.61 $false|sQ9_spl),
% 0.14/5.61 inference(forward_subsumption_resolution,[status(thm)],[f811,f444])).
% 0.14/5.61 fof(f814,plain,(
% 0.14/5.61 sQ9_spl),
% 0.14/5.61 inference(contradiction_clause,[status(thm)],[f813])).
% 0.14/5.61 fof(f822,plain,(
% 0.14/5.61 empty(sK39_skl)|~relation(sK39_skl)),
% 0.14/5.61 inference(resolution,[status(thm)],[f763,f387])).
% 0.14/5.61 fof(f828,definition,(
% 0.14/5.61 sQ10_spl <=> (empty(sK39_skl))),
% 0.14/5.61 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/5.61 fof(f831,definition,(
% 0.14/5.61 sQ11_spl <=> (relation(sK39_skl))),
% 0.14/5.61 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/5.61 fof(f833,plain,(
% 0.14/5.61 ~relation(sK39_skl)|sQ11_spl),
% 0.14/5.61 inference(component_clause,[status(thm)],[f831])).
% 0.14/5.61 fof(f834,plain,(
% 0.14/5.61 sQ10_spl|~sQ11_spl),
% 0.14/5.61 inference(split_clause,[status(thm)],[f822,f828,f831])).
% 0.14/5.61 fof(f842,plain,(
% 0.14/5.61 $false|sQ11_spl),
% 0.14/5.61 inference(forward_subsumption_resolution,[status(thm)],[f768,f833])).
% 0.14/5.61 fof(f843,plain,(
% 0.14/5.61 sQ11_spl),
% 0.14/5.61 inference(contradiction_clause,[status(thm)],[f842])).
% 0.14/5.61 fof(f865,plain,(
% 0.14/5.61 empty(sK49_skl)|~relation(sK49_skl)|~empty(empty_set)|~sQ1_spl),
% 0.14/5.61 inference(paramodulation,[status(thm)],[f680,f387])).
% 0.14/5.61 fof(f868,plain,(
% 0.14/5.61 sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl),
% 0.14/5.61 inference(split_clause,[status(thm)],[f865,f740,f743,f732,f679])).
% 0.14/5.61 fof(f939,plain,(
% 0.14/5.61 ![X0]: (~relation(empty_set)|~relation(X0)|subset(relation_dom(empty_set),relation_dom(X0)))),
% 0.14/5.61 inference(resolution,[status(thm)],[f509,f524])).
% 0.14/5.61 fof(f941,definition,(
% 0.14/5.61 ![X0]: (sQ14_spl <=> (~relation(X0)|subset(relation_dom(empty_set),relation_dom(X0))))),
% 0.14/5.61 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/5.61 fof(f944,plain,(
% 0.14/5.61 ~sQ3_spl|sQ14_spl),
% 0.14/5.61 inference(split_clause,[status(thm)],[f939,f735,f941])).
% 0.14/5.61 fof(f946,plain,(
% 0.14/5.61 $false|sQ3_spl),
% 0.14/5.61 inference(forward_subsumption_resolution,[status(thm)],[f737,f381])).
% 0.14/5.61 fof(f947,plain,(
% 0.14/5.61 sQ3_spl),
% 0.14/5.61 inference(contradiction_clause,[status(thm)],[f946])).
% 0.14/5.61 fof(f949,plain,(
% 0.14/5.61 ![X0]: (~relation(empty_set)|~relation(X0)|subset(relation_rng(empty_set),relation_rng(X0)))),
% 0.14/5.61 inference(resolution,[status(thm)],[f510,f524])).
% 0.14/5.61 fof(f951,definition,(
% 0.14/5.61 ![X0]: (sQ15_spl <=> (~relation(X0)|subset(relation_rng(empty_set),relation_rng(X0))))),
% 0.14/5.61 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/5.61 fof(f954,plain,(
% 0.14/5.61 ~sQ3_spl|sQ15_spl),
% 0.14/5.61 inference(split_clause,[status(thm)],[f949,f735,f951])).
% 0.14/5.61 fof(f968,plain,(
% 0.14/5.61 sK49_skl=empty_set|~sQ4_spl),
% 0.14/5.61 inference(resolution,[status(thm)],[f637,f741])).
% 0.14/5.61 fof(f972,plain,(
% 0.14/5.61 relation_dom(sK49_skl)=empty_set|~sQ4_spl),
% 0.14/5.61 inference(resolution,[status(thm)],[f637,f775])).
% 0.14/5.61 fof(f977,plain,(
% 0.14/5.61 relation_rng(sK39_skl)=empty_set),
% 0.14/5.61 inference(resolution,[status(thm)],[f637,f763])).
% 0.14/5.61 fof(f979,plain,(
% 0.14/5.61 sK39_skl=empty_set),
% 0.14/5.61 inference(resolution,[status(thm)],[f637,f450])).
% 0.14/5.61 fof(f982,plain,(
% 0.14/5.61 sQ0_spl|~sQ4_spl),
% 0.14/5.61 inference(split_clause,[status(thm)],[f972,f676,f740])).
% 0.14/5.61 fof(f1005,plain,(
% 0.14/5.61 sK39_skl=sK49_skl|~sQ4_spl),
% 0.14/5.61 inference(forward_demodulation,[status(thm)],[f968,f979])).
% 0.14/5.61 fof(f1052,plain,(
% 0.14/5.61 ~relation_rng(sK49_skl)=sK49_skl|~sQ4_spl|sQ1_spl),
% 0.14/5.61 inference(forward_demodulation,[status(thm)],[f968,f681])).
% 0.14/5.61 fof(f1061,plain,(
% 0.14/5.61 relation_rng(sK49_skl)=empty_set|~sQ4_spl),
% 0.14/5.61 inference(forward_demodulation,[status(thm)],[f1005,f977])).
% 0.14/5.61 fof(f1062,plain,(
% 0.14/5.61 relation_rng(sK49_skl)=sK49_skl|~sQ4_spl),
% 0.14/5.61 inference(forward_demodulation,[status(thm)],[f968,f1061])).
% 0.14/5.61 fof(f1063,plain,(
% 0.14/5.61 $false|sQ1_spl|~sQ4_spl),
% 0.14/5.61 inference(forward_subsumption_resolution,[status(thm)],[f1062,f1052])).
% 0.14/5.61 fof(f1064,plain,(
% 0.14/5.61 sQ1_spl|~sQ4_spl),
% 0.14/5.61 inference(contradiction_clause,[status(thm)],[f1063])).
% 0.14/5.61 fof(f1065,plain,(
% 0.14/5.61 $false),
% 0.14/5.61 inference(sat_refutation,[status(thm)],[f682,f683,f746,f767,f799,f812,f814,f834,f843,f868,f944,f947,f954,f982,f1064])).
% 0.14/5.61 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.64 % Elapsed time: 0.089589 seconds
% 0.14/5.64 % CPU time: 0.217891 seconds
% 0.14/5.64 % Total memory used: 113.868 MB
% 0.14/5.64 % Net memory used: 113.684 MB
%------------------------------------------------------------------------------