%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU180+1 : 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 : n002.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:55 PM UTC 2026
% Result : Theorem 0.15s 0.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU180+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n002.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 05:57:46 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.44 % Drodi V4.1.1
% 0.15/0.50 % Refutation found
% 0.15/0.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.50 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.50 fof(f4,axiom,(
% 0.15/0.50 (! [A,B,C] :( C = set_union2(A,B)<=> (! [D] :( in(D,C)<=> ( in(D,A)| in(D,B) ) ) )) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f5,axiom,(
% 0.15/0.50 (! [A] :( relation(A)=> (! [B] :( B = relation_dom(A)<=> (! [C] :( in(C,B)<=> (? [D] : in(ordered_pair(C,D),A) )) )) )) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f6,axiom,(
% 0.15/0.50 (! [A] :( relation(A)=> (! [B] :( B = relation_rng(A)<=> (! [C] :( in(C,B)<=> (? [D] : in(ordered_pair(D,C),A) )) )) )) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f8,axiom,(
% 0.15/0.50 (! [A] :( relation(A)=> relation_field(A) = set_union2(relation_dom(A),relation_rng(A)) ) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f27,axiom,(
% 0.15/0.50 (? [A] :( empty(A)& relation(A) ) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f28,axiom,(
% 0.15/0.50 (? [A] : empty(A) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f33,conjecture,(
% 0.15/0.50 (! [A,B,C] :( relation(C)=> ( in(ordered_pair(A,B),C)=> ( in(A,relation_field(C))& in(B,relation_field(C)) ) ) ) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f34,negated_conjecture,(
% 0.15/0.50 ~((! [A,B,C] :( relation(C)=> ( in(ordered_pair(A,B),C)=> ( in(A,relation_field(C))& in(B,relation_field(C)) ) ) ) ))),
% 0.15/0.50 inference(negated_conjecture,[status(cth)],[f33])).
% 0.15/0.50 fof(f35,axiom,(
% 0.15/0.50 (! [A] :( empty(A)=> A = empty_set ) )),
% 0.15/0.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.50 fof(f42,plain,(
% 0.15/0.50 ![A,B,C]: ((~C=set_union2(A,B)|(![D]: ((~in(D,C)|(in(D,A)|in(D,B)))&(in(D,C)|(~in(D,A)&~in(D,B))))))&(C=set_union2(A,B)|(?[D]: ((~in(D,C)|(~in(D,A)&~in(D,B)))&(in(D,C)|(in(D,A)|in(D,B)))))))),
% 0.15/0.50 inference(NNF_transformation,[status(thm)],[f4])).
% 0.15/0.50 fof(f43,plain,(
% 0.15/0.50 (![A,B,C]: (~C=set_union2(A,B)|((![D]: (~in(D,C)|(in(D,A)|in(D,B))))&(![D]: (in(D,C)|(~in(D,A)&~in(D,B)))))))&(![A,B,C]: (C=set_union2(A,B)|(?[D]: ((~in(D,C)|(~in(D,A)&~in(D,B)))&(in(D,C)|(in(D,A)|in(D,B)))))))),
% 0.15/0.50 inference(miniscoping,[status(thm)],[f42])).
% 0.15/0.50 fof(f44,plain,(
% 0.15/0.50 (![A,B,C]: (~C=set_union2(A,B)|((![D]: (~in(D,C)|(in(D,A)|in(D,B))))&(![D]: (in(D,C)|(~in(D,A)&~in(D,B)))))))&(![A,B,C]: (C=set_union2(A,B)|((~in(sK0_skl(C,B,A),C)|(~in(sK0_skl(C,B,A),A)&~in(sK0_skl(C,B,A),B)))&(in(sK0_skl(C,B,A),C)|(in(sK0_skl(C,B,A),A)|in(sK0_skl(C,B,A),B))))))),
% 0.15/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(D,sK0_skl(C,B,A))],[f43])).
% 0.15/0.50 fof(f46,plain,(
% 0.15/0.50 ![X0,X1,X2,X3]: (~X0=set_union2(X1,X2)|in(X3,X0)|~in(X3,X1))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f44])).
% 0.15/0.50 fof(f47,plain,(
% 0.15/0.50 ![X0,X1,X2,X3]: (~X0=set_union2(X1,X2)|in(X3,X0)|~in(X3,X2))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f44])).
% 0.15/0.50 fof(f51,plain,(
% 0.15/0.50 ![A]: (~relation(A)|(![B]: (B=relation_dom(A)<=>(![C]: (in(C,B)<=>(?[D]: in(ordered_pair(C,D),A)))))))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.15/0.50 fof(f52,plain,(
% 0.15/0.50 ![A]: (~relation(A)|(![B]: ((~B=relation_dom(A)|(![C]: ((~in(C,B)|(?[D]: in(ordered_pair(C,D),A)))&(in(C,B)|(![D]: ~in(ordered_pair(C,D),A))))))&(B=relation_dom(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))&(in(C,B)|(?[D]: in(ordered_pair(C,D),A)))))))))),
% 0.15/0.50 inference(NNF_transformation,[status(thm)],[f51])).
% 0.15/0.50 fof(f53,plain,(
% 0.15/0.50 ![A]: (~relation(A)|((![B]: (~B=relation_dom(A)|((![C]: (~in(C,B)|(?[D]: in(ordered_pair(C,D),A))))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))))))&(![B]: (B=relation_dom(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))&(in(C,B)|(?[D]: in(ordered_pair(C,D),A)))))))))),
% 0.15/0.50 inference(miniscoping,[status(thm)],[f52])).
% 0.15/0.50 fof(f54,plain,(
% 0.15/0.50 ![A]: (~relation(A)|((![B]: (~B=relation_dom(A)|((![C]: (~in(C,B)|in(ordered_pair(C,sK1_skl(C,B,A)),A)))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))))))&(![B]: (B=relation_dom(A)|((~in(sK2_skl(B,A),B)|(![D]: ~in(ordered_pair(sK2_skl(B,A),D),A)))&(in(sK2_skl(B,A),B)|in(ordered_pair(sK2_skl(B,A),sK3_skl(B,A)),A)))))))),
% 0.15/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl,sK3_skl]),skolemize(D,sK1_skl(C,B,A)),skolemize(C,sK2_skl(B,A)),skolemize(D,sK3_skl(B,A))],[f53])).
% 0.15/0.50 fof(f56,plain,(
% 0.15/0.50 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_dom(X0)|in(X2,X1)|~in(ordered_pair(X2,X3),X0))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f54])).
% 0.15/0.50 fof(f59,plain,(
% 0.15/0.50 ![A]: (~relation(A)|(![B]: (B=relation_rng(A)<=>(![C]: (in(C,B)<=>(?[D]: in(ordered_pair(D,C),A)))))))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.15/0.50 fof(f60,plain,(
% 0.15/0.50 ![A]: (~relation(A)|(![B]: ((~B=relation_rng(A)|(![C]: ((~in(C,B)|(?[D]: in(ordered_pair(D,C),A)))&(in(C,B)|(![D]: ~in(ordered_pair(D,C),A))))))&(B=relation_rng(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))&(in(C,B)|(?[D]: in(ordered_pair(D,C),A)))))))))),
% 0.15/0.50 inference(NNF_transformation,[status(thm)],[f59])).
% 0.15/0.50 fof(f61,plain,(
% 0.15/0.50 ![A]: (~relation(A)|((![B]: (~B=relation_rng(A)|((![C]: (~in(C,B)|(?[D]: in(ordered_pair(D,C),A))))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))))))&(![B]: (B=relation_rng(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))&(in(C,B)|(?[D]: in(ordered_pair(D,C),A)))))))))),
% 0.15/0.50 inference(miniscoping,[status(thm)],[f60])).
% 0.15/0.50 fof(f62,plain,(
% 0.15/0.50 ![A]: (~relation(A)|((![B]: (~B=relation_rng(A)|((![C]: (~in(C,B)|in(ordered_pair(sK4_skl(C,B,A),C),A)))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))))))&(![B]: (B=relation_rng(A)|((~in(sK5_skl(B,A),B)|(![D]: ~in(ordered_pair(D,sK5_skl(B,A)),A)))&(in(sK5_skl(B,A),B)|in(ordered_pair(sK6_skl(B,A),sK5_skl(B,A)),A)))))))),
% 0.15/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl]),skolemize(D,sK4_skl(C,B,A)),skolemize(C,sK5_skl(B,A)),skolemize(D,sK6_skl(B,A))],[f61])).
% 0.15/0.50 fof(f64,plain,(
% 0.15/0.50 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_rng(X0)|in(X2,X1)|~in(ordered_pair(X3,X2),X0))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f62])).
% 0.15/0.50 fof(f68,plain,(
% 0.15/0.50 ![A]: (~relation(A)|relation_field(A)=set_union2(relation_dom(A),relation_rng(A)))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.15/0.50 fof(f69,plain,(
% 0.15/0.50 ![X0]: (~relation(X0)|relation_field(X0)=set_union2(relation_dom(X0),relation_rng(X0)))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f68])).
% 0.15/0.50 fof(f86,plain,(
% 0.15/0.50 (empty(sK8_skl)&relation(sK8_skl))),
% 0.15/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f27])).
% 0.15/0.50 fof(f87,plain,(
% 0.15/0.50 empty(sK8_skl)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f86])).
% 0.15/0.50 fof(f88,plain,(
% 0.15/0.50 relation(sK8_skl)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f86])).
% 0.15/0.50 fof(f89,plain,(
% 0.15/0.50 empty(sK9_skl)),
% 0.15/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(A,sK9_skl)],[f28])).
% 0.15/0.50 fof(f90,plain,(
% 0.15/0.50 empty(sK9_skl)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f89])).
% 0.15/0.50 fof(f98,plain,(
% 0.15/0.50 (?[A,B,C]: (relation(C)&(in(ordered_pair(A,B),C)&(~in(A,relation_field(C))|~in(B,relation_field(C))))))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 0.15/0.50 fof(f99,plain,(
% 0.15/0.50 ?[C]: (relation(C)&(?[A,B]: (in(ordered_pair(A,B),C)&(~in(A,relation_field(C))|~in(B,relation_field(C))))))),
% 0.15/0.50 inference(miniscoping,[status(thm)],[f98])).
% 0.15/0.50 fof(f100,plain,(
% 0.15/0.50 (relation(sK11_skl)&(in(ordered_pair(sK12_skl,sK13_skl),sK11_skl)&(~in(sK12_skl,relation_field(sK11_skl))|~in(sK13_skl,relation_field(sK11_skl)))))),
% 0.15/0.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl,sK13_skl]),skolemize(C,sK11_skl),skolemize(A,sK12_skl),skolemize(B,sK13_skl)],[f99])).
% 0.15/0.50 fof(f101,plain,(
% 0.15/0.50 relation(sK11_skl)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f100])).
% 0.15/0.50 fof(f102,plain,(
% 0.15/0.50 in(ordered_pair(sK12_skl,sK13_skl),sK11_skl)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f100])).
% 0.15/0.50 fof(f103,plain,(
% 0.15/0.50 ~in(sK12_skl,relation_field(sK11_skl))|~in(sK13_skl,relation_field(sK11_skl))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f100])).
% 0.15/0.50 fof(f104,plain,(
% 0.15/0.50 ![A]: (~empty(A)|A=empty_set)),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.15/0.50 fof(f105,plain,(
% 0.15/0.50 ![X0]: (~empty(X0)|X0=empty_set)),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f104])).
% 0.15/0.50 fof(f112,definition,(
% 0.15/0.50 sQ0_spl <=> (in(sK12_skl,relation_field(sK11_skl)))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f114,plain,(
% 0.15/0.50 ~in(sK12_skl,relation_field(sK11_skl))|sQ0_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f112])).
% 0.15/0.50 fof(f115,definition,(
% 0.15/0.50 sQ1_spl <=> (in(sK13_skl,relation_field(sK11_skl)))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f117,plain,(
% 0.15/0.50 ~in(sK13_skl,relation_field(sK11_skl))|sQ1_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f115])).
% 0.15/0.50 fof(f118,plain,(
% 0.15/0.50 ~sQ0_spl|~sQ1_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f103,f112,f115])).
% 0.15/0.50 fof(f120,plain,(
% 0.15/0.50 ![X0,X1,X2]: (in(X0,set_union2(X1,X2))|~in(X0,X1))),
% 0.15/0.50 inference(destructive_equality_resolution,[status(thm)],[f46])).
% 0.15/0.50 fof(f121,plain,(
% 0.15/0.50 ![X0,X1,X2]: (in(X0,set_union2(X1,X2))|~in(X0,X2))),
% 0.15/0.50 inference(destructive_equality_resolution,[status(thm)],[f47])).
% 0.15/0.50 fof(f123,plain,(
% 0.15/0.50 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_dom(X0))|~in(ordered_pair(X1,X2),X0))),
% 0.15/0.50 inference(destructive_equality_resolution,[status(thm)],[f56])).
% 0.15/0.50 fof(f125,plain,(
% 0.15/0.50 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_rng(X0))|~in(ordered_pair(X2,X1),X0))),
% 0.15/0.50 inference(destructive_equality_resolution,[status(thm)],[f64])).
% 0.15/0.50 fof(f135,plain,(
% 0.15/0.50 relation_field(sK11_skl)=set_union2(relation_dom(sK11_skl),relation_rng(sK11_skl))),
% 0.15/0.50 inference(resolution,[status(thm)],[f69,f101])).
% 0.15/0.50 fof(f180,plain,(
% 0.15/0.50 sK9_skl=empty_set),
% 0.15/0.50 inference(resolution,[status(thm)],[f105,f90])).
% 0.15/0.50 fof(f181,plain,(
% 0.15/0.50 sK8_skl=empty_set),
% 0.15/0.50 inference(resolution,[status(thm)],[f105,f87])).
% 0.15/0.50 fof(f186,plain,(
% 0.15/0.50 relation(sK9_skl)),
% 0.15/0.50 inference(backward_demodulation,[status(thm)],[f188,f88])).
% 0.15/0.50 fof(f188,plain,(
% 0.15/0.50 sK8_skl=sK9_skl),
% 0.15/0.50 inference(forward_demodulation,[status(thm)],[f180,f181])).
% 0.15/0.50 fof(f506,definition,(
% 0.15/0.50 sQ17_spl <=> (relation(sK9_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f508,plain,(
% 0.15/0.50 ~relation(sK9_skl)|sQ17_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f506])).
% 0.15/0.50 fof(f513,definition,(
% 0.15/0.50 sQ19_spl <=> (relation(sK11_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f515,plain,(
% 0.15/0.50 ~relation(sK11_skl)|sQ19_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f513])).
% 0.15/0.50 fof(f520,plain,(
% 0.15/0.50 $false|sQ19_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f515,f101])).
% 0.15/0.50 fof(f521,plain,(
% 0.15/0.50 sQ19_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f520])).
% 0.15/0.50 fof(f556,plain,(
% 0.15/0.50 $false|sQ17_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f508,f186])).
% 0.15/0.50 fof(f557,plain,(
% 0.15/0.50 sQ17_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f556])).
% 0.15/0.50 fof(f658,plain,(
% 0.15/0.50 ~relation(sK11_skl)|in(sK12_skl,relation_dom(sK11_skl))),
% 0.15/0.50 inference(resolution,[status(thm)],[f123,f102])).
% 0.15/0.50 fof(f659,definition,(
% 0.15/0.50 sQ29_spl <=> (in(sK12_skl,relation_dom(sK11_skl)))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f660,plain,(
% 0.15/0.50 in(sK12_skl,relation_dom(sK11_skl))|~sQ29_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f659])).
% 0.15/0.50 fof(f662,plain,(
% 0.15/0.50 ~sQ19_spl|sQ29_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f658,f513,f659])).
% 0.15/0.50 fof(f667,plain,(
% 0.15/0.50 ![X0]: (in(sK12_skl,set_union2(relation_dom(sK11_skl),X0))|~sQ29_spl)),
% 0.15/0.50 inference(resolution,[status(thm)],[f660,f120])).
% 0.15/0.50 fof(f737,plain,(
% 0.15/0.50 in(sK12_skl,relation_field(sK11_skl))|~sQ29_spl),
% 0.15/0.50 inference(paramodulation,[status(thm)],[f135,f667])).
% 0.15/0.50 fof(f743,plain,(
% 0.15/0.50 $false|sQ0_spl|~sQ29_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f737,f114])).
% 0.15/0.50 fof(f744,plain,(
% 0.15/0.50 sQ0_spl|~sQ29_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f743])).
% 0.15/0.50 fof(f825,plain,(
% 0.15/0.50 ~relation(sK11_skl)|in(sK13_skl,relation_rng(sK11_skl))),
% 0.15/0.50 inference(resolution,[status(thm)],[f125,f102])).
% 0.15/0.50 fof(f826,definition,(
% 0.15/0.50 sQ37_spl <=> (in(sK13_skl,relation_rng(sK11_skl)))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f827,plain,(
% 0.15/0.50 in(sK13_skl,relation_rng(sK11_skl))|~sQ37_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f826])).
% 0.15/0.50 fof(f829,plain,(
% 0.15/0.50 ~sQ19_spl|sQ37_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f825,f513,f826])).
% 0.15/0.51 fof(f831,plain,(
% 0.15/0.51 ![X0]: (in(sK13_skl,set_union2(X0,relation_rng(sK11_skl)))|~sQ37_spl)),
% 0.15/0.51 inference(resolution,[status(thm)],[f827,f121])).
% 0.15/0.51 fof(f881,plain,(
% 0.15/0.51 in(sK13_skl,relation_field(sK11_skl))|~sQ37_spl),
% 0.15/0.51 inference(paramodulation,[status(thm)],[f135,f831])).
% 0.15/0.51 fof(f890,plain,(
% 0.15/0.51 $false|sQ1_spl|~sQ37_spl),
% 0.15/0.51 inference(forward_subsumption_resolution,[status(thm)],[f881,f117])).
% 0.15/0.51 fof(f891,plain,(
% 0.15/0.51 sQ1_spl|~sQ37_spl),
% 0.15/0.51 inference(contradiction_clause,[status(thm)],[f890])).
% 0.15/0.51 fof(f892,plain,(
% 0.15/0.51 $false),
% 0.15/0.51 inference(sat_refutation,[status(thm)],[f118,f521,f557,f662,f744,f829,f891])).
% 0.15/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.53 % Elapsed time: 0.088606 seconds
% 0.15/0.53 % CPU time: 0.348856 seconds
% 0.15/0.53 % Total memory used: 105.720 MB
% 0.15/0.53 % Net memory used: 105.430 MB
%------------------------------------------------------------------------------