%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU146+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:47 PM UTC 2026
% Result : Theorem 0.07s 0.33s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU146+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 05:52:37 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.03/0.30 % Drodi V4.1.1
% 0.07/0.33 % Refutation found
% 0.07/0.33 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.07/0.33 % SZS output start CNFRefutation for theBenchmark
% 0.07/0.33 fof(f6,axiom,(
% 0.07/0.33 (! [A,B] :( A = B<=> ( subset(A,B)& subset(B,A) ) ) )),
% 0.07/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.33 fof(f29,lemma,(
% 0.07/0.33 (! [A,B] :( subset(singleton(A),B)<=> in(A,B) ) )),
% 0.07/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.33 fof(f30,lemma,(
% 0.07/0.33 (! [A,B] :( set_difference(A,B) = empty_set<=> subset(A,B) ) )),
% 0.07/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.33 fof(f31,lemma,(
% 0.07/0.33 (! [A,B,C] :( subset(A,B)=> ( in(C,A)| subset(A,set_difference(B,singleton(C))) ) ) )),
% 0.07/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.33 fof(f32,conjecture,(
% 0.07/0.33 (! [A,B] :( subset(A,singleton(B))<=> ( A = empty_set| A = singleton(B) ) ) )),
% 0.07/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.33 fof(f33,negated_conjecture,(
% 0.07/0.33 ~((! [A,B] :( subset(A,singleton(B))<=> ( A = empty_set| A = singleton(B) ) ) ))),
% 0.07/0.33 inference(negated_conjecture,[status(cth)],[f32])).
% 0.07/0.33 fof(f34,axiom,(
% 0.07/0.33 (? [A] : empty(A) )),
% 0.07/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.33 fof(f47,lemma,(
% 0.07/0.33 (! [A] : subset(empty_set,A) )),
% 0.07/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.33 fof(f54,lemma,(
% 0.07/0.33 (! [A] :( subset(A,empty_set)=> A = empty_set ) )),
% 0.07/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.33 fof(f58,axiom,(
% 0.07/0.33 (! [A] : set_difference(empty_set,A) = empty_set )),
% 0.07/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.33 fof(f63,axiom,(
% 0.07/0.33 (! [A] :( empty(A)=> A = empty_set ) )),
% 0.07/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.33 fof(f76,plain,(
% 0.07/0.33 ![A,B]: ((~A=B|(subset(A,B)&subset(B,A)))&(A=B|(~subset(A,B)|~subset(B,A))))),
% 0.07/0.33 inference(NNF_transformation,[status(thm)],[f6])).
% 0.07/0.33 fof(f77,plain,(
% 0.07/0.33 (![A,B]: (~A=B|(subset(A,B)&subset(B,A))))&(![A,B]: (A=B|(~subset(A,B)|~subset(B,A))))),
% 0.07/0.33 inference(miniscoping,[status(thm)],[f76])).
% 0.07/0.33 fof(f78,plain,(
% 0.07/0.33 ![X0,X1]: (~X0=X1|subset(X0,X1))),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f77])).
% 0.07/0.33 fof(f80,plain,(
% 0.07/0.33 ![X0,X1]: (X0=X1|~subset(X0,X1)|~subset(X1,X0))),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f77])).
% 0.07/0.33 fof(f159,plain,(
% 0.07/0.33 ![A,B]: ((~subset(singleton(A),B)|in(A,B))&(subset(singleton(A),B)|~in(A,B)))),
% 0.07/0.33 inference(NNF_transformation,[status(thm)],[f29])).
% 0.07/0.33 fof(f160,plain,(
% 0.07/0.33 (![A,B]: (~subset(singleton(A),B)|in(A,B)))&(![A,B]: (subset(singleton(A),B)|~in(A,B)))),
% 0.07/0.33 inference(miniscoping,[status(thm)],[f159])).
% 0.07/0.33 fof(f162,plain,(
% 0.07/0.33 ![X0,X1]: (subset(singleton(X0),X1)|~in(X0,X1))),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f160])).
% 0.07/0.33 fof(f163,plain,(
% 0.07/0.33 ![A,B]: ((~set_difference(A,B)=empty_set|subset(A,B))&(set_difference(A,B)=empty_set|~subset(A,B)))),
% 0.07/0.33 inference(NNF_transformation,[status(thm)],[f30])).
% 0.07/0.33 fof(f164,plain,(
% 0.07/0.33 (![A,B]: (~set_difference(A,B)=empty_set|subset(A,B)))&(![A,B]: (set_difference(A,B)=empty_set|~subset(A,B)))),
% 0.07/0.33 inference(miniscoping,[status(thm)],[f163])).
% 0.07/0.33 fof(f165,plain,(
% 0.07/0.33 ![X0,X1]: (~set_difference(X0,X1)=empty_set|subset(X0,X1))),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f164])).
% 0.07/0.33 fof(f166,plain,(
% 0.07/0.33 ![X0,X1]: (set_difference(X0,X1)=empty_set|~subset(X0,X1))),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f164])).
% 0.07/0.33 fof(f167,plain,(
% 0.07/0.33 ![A,B,C]: (~subset(A,B)|(in(C,A)|subset(A,set_difference(B,singleton(C)))))),
% 0.07/0.33 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.07/0.33 fof(f168,plain,(
% 0.07/0.33 ![A,B]: (~subset(A,B)|(![C]: (in(C,A)|subset(A,set_difference(B,singleton(C))))))),
% 0.07/0.33 inference(miniscoping,[status(thm)],[f167])).
% 0.07/0.33 fof(f169,plain,(
% 0.07/0.33 ![X0,X1,X2]: (~subset(X0,X1)|in(X2,X0)|subset(X0,set_difference(X1,singleton(X2))))),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f168])).
% 0.07/0.33 fof(f170,plain,(
% 0.07/0.33 (?[A,B]: (subset(A,singleton(B))<~>(A=empty_set|A=singleton(B))))),
% 0.07/0.33 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.07/0.33 fof(f171,plain,(
% 0.07/0.33 ?[A,B]: ((subset(A,singleton(B))|(A=empty_set|A=singleton(B)))&(~subset(A,singleton(B))|(~A=empty_set&~A=singleton(B))))),
% 0.07/0.33 inference(NNF_transformation,[status(thm)],[f170])).
% 0.07/0.33 fof(f172,plain,(
% 0.07/0.33 ((subset(sK7_skl,singleton(sK8_skl))|(sK7_skl=empty_set|sK7_skl=singleton(sK8_skl)))&(~subset(sK7_skl,singleton(sK8_skl))|(~sK7_skl=empty_set&~sK7_skl=singleton(sK8_skl))))),
% 0.07/0.33 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(A,sK7_skl),skolemize(B,sK8_skl)],[f171])).
% 0.07/0.33 fof(f173,plain,(
% 0.07/0.33 subset(sK7_skl,singleton(sK8_skl))|sK7_skl=empty_set|sK7_skl=singleton(sK8_skl)),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f172])).
% 0.07/0.33 fof(f174,plain,(
% 0.07/0.33 ~subset(sK7_skl,singleton(sK8_skl))|~sK7_skl=empty_set),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f172])).
% 0.07/0.33 fof(f175,plain,(
% 0.07/0.33 ~subset(sK7_skl,singleton(sK8_skl))|~sK7_skl=singleton(sK8_skl)),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f172])).
% 0.07/0.33 fof(f176,plain,(
% 0.07/0.33 empty(sK9_skl)),
% 0.07/0.33 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f34])).
% 0.07/0.33 fof(f177,plain,(
% 0.07/0.33 empty(sK9_skl)),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f176])).
% 0.07/0.33 fof(f204,plain,(
% 0.07/0.33 ![X0]: (subset(empty_set,X0))),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f47])).
% 0.07/0.33 fof(f221,plain,(
% 0.07/0.33 ![A]: (~subset(A,empty_set)|A=empty_set)),
% 0.07/0.33 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 0.07/0.33 fof(f222,plain,(
% 0.07/0.33 ![X0]: (~subset(X0,empty_set)|X0=empty_set)),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f221])).
% 0.07/0.33 fof(f227,plain,(
% 0.07/0.33 ![X0]: (set_difference(empty_set,X0)=empty_set)),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f58])).
% 0.07/0.33 fof(f239,plain,(
% 0.07/0.33 ![A]: (~empty(A)|A=empty_set)),
% 0.07/0.33 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 0.07/0.33 fof(f240,plain,(
% 0.07/0.33 ![X0]: (~empty(X0)|X0=empty_set)),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f239])).
% 0.07/0.33 fof(f254,definition,(
% 0.07/0.33 sQ0_spl <=> (subset(sK7_skl,singleton(sK8_skl)))),
% 0.07/0.33 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.07/0.33 fof(f255,plain,(
% 0.07/0.33 subset(sK7_skl,singleton(sK8_skl))|~sQ0_spl),
% 0.07/0.33 inference(component_clause,[status(thm)],[f254])).
% 0.07/0.33 fof(f256,plain,(
% 0.07/0.33 ~subset(sK7_skl,singleton(sK8_skl))|sQ0_spl),
% 0.07/0.33 inference(component_clause,[status(thm)],[f254])).
% 0.07/0.33 fof(f257,definition,(
% 0.07/0.33 sQ1_spl <=> (sK7_skl=empty_set)),
% 0.07/0.33 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.07/0.33 fof(f258,plain,(
% 0.07/0.33 sK7_skl=empty_set|~sQ1_spl),
% 0.07/0.33 inference(component_clause,[status(thm)],[f257])).
% 0.07/0.33 fof(f259,plain,(
% 0.07/0.33 ~sK7_skl=empty_set|sQ1_spl),
% 0.07/0.33 inference(component_clause,[status(thm)],[f257])).
% 0.07/0.33 fof(f260,definition,(
% 0.07/0.33 sQ2_spl <=> (sK7_skl=singleton(sK8_skl))),
% 0.07/0.33 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.07/0.33 fof(f261,plain,(
% 0.07/0.33 sK7_skl=singleton(sK8_skl)|~sQ2_spl),
% 0.07/0.33 inference(component_clause,[status(thm)],[f260])).
% 0.07/0.33 fof(f263,plain,(
% 0.07/0.33 sQ0_spl|sQ1_spl|sQ2_spl),
% 0.07/0.33 inference(split_clause,[status(thm)],[f173,f254,f257,f260])).
% 0.07/0.33 fof(f264,plain,(
% 0.07/0.33 ~sQ0_spl|~sQ1_spl),
% 0.07/0.33 inference(split_clause,[status(thm)],[f174,f254,f257])).
% 0.07/0.33 fof(f265,plain,(
% 0.07/0.33 ~sQ0_spl|~sQ2_spl),
% 0.07/0.33 inference(split_clause,[status(thm)],[f175,f254,f260])).
% 0.07/0.33 fof(f266,plain,(
% 0.07/0.33 ![X0]: (subset(X0,X0))),
% 0.07/0.33 inference(destructive_equality_resolution,[status(thm)],[f78])).
% 0.07/0.33 fof(f287,plain,(
% 0.07/0.33 $false|~sQ1_spl|sQ0_spl),
% 0.07/0.33 inference(backward_subsumption_resolution,[status(thm)],[f256,f288])).
% 0.07/0.33 fof(f288,plain,(
% 0.07/0.33 ![X0]: (subset(sK7_skl,X0)|~sQ1_spl)),
% 0.07/0.33 inference(forward_demodulation,[status(thm)],[f258,f204])).
% 0.07/0.33 fof(f290,plain,(
% 0.07/0.33 ~sQ1_spl|sQ0_spl),
% 0.07/0.33 inference(contradiction_clause,[status(thm)],[f287])).
% 0.07/0.33 fof(f300,plain,(
% 0.07/0.33 sK9_skl=empty_set),
% 0.07/0.33 inference(resolution,[status(thm)],[f240,f177])).
% 0.07/0.33 fof(f309,plain,(
% 0.07/0.33 ~sK7_skl=sK9_skl|sQ1_spl),
% 0.07/0.33 inference(backward_demodulation,[status(thm)],[f300,f259])).
% 0.07/0.33 fof(f319,plain,(
% 0.07/0.33 singleton(sK8_skl)=sK7_skl|~subset(singleton(sK8_skl),sK7_skl)|~sQ0_spl),
% 0.07/0.33 inference(resolution,[status(thm)],[f255,f80])).
% 0.07/0.33 fof(f320,definition,(
% 0.07/0.33 sQ3_spl <=> (subset(singleton(sK8_skl),sK7_skl))),
% 0.07/0.33 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.07/0.33 fof(f322,plain,(
% 0.07/0.33 ~subset(singleton(sK8_skl),sK7_skl)|sQ3_spl),
% 0.07/0.33 inference(component_clause,[status(thm)],[f320])).
% 0.07/0.33 fof(f323,plain,(
% 0.07/0.33 sQ2_spl|~sQ3_spl|~sQ0_spl),
% 0.07/0.33 inference(split_clause,[status(thm)],[f319,f260,f320,f254])).
% 0.07/0.33 fof(f330,plain,(
% 0.07/0.33 ~subset(sK7_skl,sK7_skl)|~sQ2_spl|sQ0_spl),
% 0.07/0.33 inference(forward_demodulation,[status(thm)],[f261,f256])).
% 0.07/0.33 fof(f331,plain,(
% 0.07/0.33 $false|~sQ2_spl|sQ0_spl),
% 0.07/0.33 inference(forward_subsumption_resolution,[status(thm)],[f330,f266])).
% 0.07/0.33 fof(f332,plain,(
% 0.07/0.33 ~sQ2_spl|sQ0_spl),
% 0.07/0.33 inference(contradiction_clause,[status(thm)],[f331])).
% 0.07/0.33 fof(f334,plain,(
% 0.07/0.33 ![X0]: (set_difference(sK9_skl,X0)=empty_set)),
% 0.07/0.33 inference(forward_demodulation,[status(thm)],[f300,f227])).
% 0.07/0.33 fof(f335,plain,(
% 0.07/0.33 ![X0]: (set_difference(sK9_skl,X0)=sK9_skl)),
% 0.07/0.33 inference(forward_demodulation,[status(thm)],[f300,f334])).
% 0.07/0.33 fof(f338,plain,(
% 0.07/0.33 ![X0]: (~subset(X0,sK9_skl)|X0=empty_set)),
% 0.07/0.33 inference(forward_demodulation,[status(thm)],[f300,f222])).
% 0.07/0.33 fof(f339,plain,(
% 0.07/0.33 ![X0]: (~subset(X0,sK9_skl)|X0=sK9_skl)),
% 0.07/0.33 inference(forward_demodulation,[status(thm)],[f300,f338])).
% 0.07/0.33 fof(f433,plain,(
% 0.07/0.33 ![X0,X1]: (~set_difference(X0,X1)=sK9_skl|subset(X0,X1))),
% 0.07/0.33 inference(forward_demodulation,[status(thm)],[f300,f165])).
% 0.07/0.33 fof(f436,plain,(
% 0.07/0.33 ![X0]: (~sK9_skl=sK9_skl|subset(sK9_skl,X0))),
% 0.07/0.33 inference(paramodulation,[status(thm)],[f335,f433])).
% 0.07/0.33 fof(f438,definition,(
% 0.07/0.33 sQ4_spl <=> (sK9_skl=sK9_skl)),
% 0.07/0.33 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.07/0.33 fof(f440,plain,(
% 0.07/0.33 ~sK9_skl=sK9_skl|sQ4_spl),
% 0.07/0.33 inference(component_clause,[status(thm)],[f438])).
% 0.07/0.33 fof(f441,definition,(
% 0.07/0.33 ![X0]: (sQ5_spl <=> (subset(sK9_skl,X0)))),
% 0.07/0.33 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.07/0.33 fof(f444,plain,(
% 0.07/0.33 ~sQ4_spl|sQ5_spl),
% 0.07/0.33 inference(split_clause,[status(thm)],[f436,f438,f441])).
% 0.07/0.33 fof(f446,plain,(
% 0.07/0.33 $false|sQ4_spl),
% 0.07/0.33 inference(trivial_equality_resolution,[status(thm)],[f440])).
% 0.07/0.33 fof(f447,plain,(
% 0.07/0.33 sQ4_spl),
% 0.07/0.33 inference(contradiction_clause,[status(thm)],[f446])).
% 0.07/0.33 fof(f482,plain,(
% 0.07/0.33 ![X0,X1]: (set_difference(X0,X1)=sK9_skl|~subset(X0,X1))),
% 0.07/0.33 inference(forward_demodulation,[status(thm)],[f300,f166])).
% 0.07/0.33 fof(f490,plain,(
% 0.07/0.33 ![X0]: (set_difference(X0,X0)=sK9_skl)),
% 0.07/0.33 inference(resolution,[status(thm)],[f482,f266])).
% 0.07/0.33 fof(f495,plain,(
% 0.07/0.33 ![X0]: (in(X0,sK7_skl)|subset(sK7_skl,set_difference(singleton(sK8_skl),singleton(X0)))|~sQ0_spl)),
% 0.07/0.33 inference(resolution,[status(thm)],[f169,f255])).
% 0.07/0.33 fof(f515,plain,(
% 0.07/0.33 ![X0]: (~sK9_skl=sK9_skl|subset(X0,X0))),
% 0.07/0.33 inference(paramodulation,[status(thm)],[f490,f433])).
% 0.07/0.33 fof(f517,definition,(
% 0.07/0.33 ![X0]: (sQ6_spl <=> (subset(X0,X0)))),
% 0.07/0.33 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.07/0.33 fof(f520,plain,(
% 0.07/0.33 ~sQ4_spl|sQ6_spl),
% 0.07/0.33 inference(split_clause,[status(thm)],[f515,f438,f517])).
% 0.07/0.33 fof(f577,plain,(
% 0.07/0.33 in(sK8_skl,sK7_skl)|subset(sK7_skl,sK9_skl)|~sQ0_spl),
% 0.07/0.33 inference(paramodulation,[status(thm)],[f490,f495])).
% 0.07/0.33 fof(f578,definition,(
% 0.07/0.33 sQ7_spl <=> (in(sK8_skl,sK7_skl))),
% 0.07/0.33 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.07/0.33 fof(f579,plain,(
% 0.07/0.33 in(sK8_skl,sK7_skl)|~sQ7_spl),
% 0.07/0.33 inference(component_clause,[status(thm)],[f578])).
% 0.07/0.33 fof(f581,definition,(
% 0.07/0.33 sQ8_spl <=> (subset(sK7_skl,sK9_skl))),
% 0.07/0.33 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.07/0.33 fof(f582,plain,(
% 0.07/0.33 subset(sK7_skl,sK9_skl)|~sQ8_spl),
% 0.07/0.33 inference(component_clause,[status(thm)],[f581])).
% 0.07/0.33 fof(f584,plain,(
% 0.07/0.33 sQ7_spl|sQ8_spl|~sQ0_spl),
% 0.07/0.33 inference(split_clause,[status(thm)],[f577,f578,f581,f254])).
% 0.07/0.33 fof(f586,plain,(
% 0.07/0.33 subset(singleton(sK8_skl),sK7_skl)|~sQ7_spl),
% 0.07/0.33 inference(resolution,[status(thm)],[f579,f162])).
% 0.07/0.33 fof(f590,plain,(
% 0.07/0.33 $false|sQ3_spl|~sQ7_spl),
% 0.07/0.33 inference(forward_subsumption_resolution,[status(thm)],[f586,f322])).
% 0.07/0.33 fof(f591,plain,(
% 0.07/0.33 sQ3_spl|~sQ7_spl),
% 0.07/0.33 inference(contradiction_clause,[status(thm)],[f590])).
% 0.07/0.33 fof(f592,plain,(
% 0.07/0.33 sK7_skl=sK9_skl|~sQ8_spl),
% 0.07/0.33 inference(resolution,[status(thm)],[f582,f339])).
% 0.07/0.33 fof(f596,plain,(
% 0.07/0.33 $false|sQ1_spl|~sQ8_spl),
% 0.07/0.33 inference(forward_subsumption_resolution,[status(thm)],[f592,f309])).
% 0.07/0.33 fof(f597,plain,(
% 0.07/0.33 sQ1_spl|~sQ8_spl),
% 0.07/0.33 inference(contradiction_clause,[status(thm)],[f596])).
% 0.07/0.33 fof(f598,plain,(
% 0.07/0.33 $false),
% 0.07/0.33 inference(sat_refutation,[status(thm)],[f263,f264,f265,f290,f323,f332,f444,f447,f520,f584,f591,f597])).
% 0.07/0.33 % SZS output end CNFRefutation for theBenchmark.p
% 0.07/0.34 % Elapsed time: 0.047286 seconds
% 0.07/0.34 % CPU time: 0.111131 seconds
% 0.07/0.34 % Total memory used: 105.454 MB
% 0.07/0.34 % Net memory used: 105.281 MB
%------------------------------------------------------------------------------