%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU179+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 : 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 : Thu Sep 24 02:21:54 PM UTC 2026
% Result : Theorem 0.11s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU179+1 : 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/0.36 % Computer : n016.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 05:59:52 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 0.11/0.45 % Refutation found
% 0.11/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.45 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.45 fof(f3,axiom,(
% 0.11/0.45 (! [A,B] :( subset(A,B)<=> (! [C] :( in(C,A)=> in(C,B) ) )) )),
% 0.11/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.45 fof(f4,axiom,(
% 0.11/0.45 (! [A] :( relation(A)=> (! [B] :( B = relation_dom(A)<=> (! [C] :( in(C,B)<=> (? [D] : in(ordered_pair(C,D),A) )) )) )) )),
% 0.11/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.45 fof(f5,axiom,(
% 0.11/0.45 (! [A] :( relation(A)=> (! [B] :( B = relation_rng(A)<=> (! [C] :( in(C,B)<=> (? [D] : in(ordered_pair(D,C),A) )) )) )) )),
% 0.11/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.45 fof(f26,axiom,(
% 0.11/0.45 (! [A,B] : subset(A,A) )),
% 0.11/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.45 fof(f28,conjecture,(
% 0.11/0.45 (! [A] :( relation(A)=> (! [B] :( relation(B)=> ( subset(A,B)=> ( subset(relation_dom(A),relation_dom(B))& subset(relation_rng(A),relation_rng(B)) ) ) ) )) )),
% 0.11/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.11/0.45 fof(f29,negated_conjecture,(
% 0.11/0.45 ~((! [A] :( relation(A)=> (! [B] :( relation(B)=> ( subset(A,B)=> ( subset(relation_dom(A),relation_dom(B))& subset(relation_rng(A),relation_rng(B)) ) ) ) )) ))),
% 0.11/0.45 inference(negated_conjecture,[status(cth)],[f28])).
% 0.11/0.45 fof(f40,plain,(
% 0.11/0.45 ![A,B]: (subset(A,B)<=>(![C]: (~in(C,A)|in(C,B))))),
% 0.11/0.45 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.11/0.45 fof(f41,plain,(
% 0.11/0.45 ![A,B]: ((~subset(A,B)|(![C]: (~in(C,A)|in(C,B))))&(subset(A,B)|(?[C]: (in(C,A)&~in(C,B)))))),
% 0.11/0.45 inference(NNF_transformation,[status(thm)],[f40])).
% 0.11/0.45 fof(f42,plain,(
% 0.11/0.45 (![A,B]: (~subset(A,B)|(![C]: (~in(C,A)|in(C,B)))))&(![A,B]: (subset(A,B)|(?[C]: (in(C,A)&~in(C,B)))))),
% 0.11/0.45 inference(miniscoping,[status(thm)],[f41])).
% 0.11/0.45 fof(f43,plain,(
% 0.11/0.45 (![A,B]: (~subset(A,B)|(![C]: (~in(C,A)|in(C,B)))))&(![A,B]: (subset(A,B)|(in(sK0_skl(B,A),A)&~in(sK0_skl(B,A),B))))),
% 0.11/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f42])).
% 0.11/0.45 fof(f44,plain,(
% 0.11/0.45 ![X0,X1,X2]: (~subset(X0,X1)|~in(X2,X0)|in(X2,X1))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f43])).
% 0.11/0.45 fof(f45,plain,(
% 0.11/0.45 ![X0,X1]: (subset(X0,X1)|in(sK0_skl(X1,X0),X0))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f43])).
% 0.11/0.45 fof(f46,plain,(
% 0.11/0.45 ![X0,X1]: (subset(X0,X1)|~in(sK0_skl(X1,X0),X1))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f43])).
% 0.11/0.45 fof(f47,plain,(
% 0.11/0.45 ![A]: (~relation(A)|(![B]: (B=relation_dom(A)<=>(![C]: (in(C,B)<=>(?[D]: in(ordered_pair(C,D),A)))))))),
% 0.11/0.45 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.11/0.45 fof(f48,plain,(
% 0.11/0.45 ![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.11/0.45 inference(NNF_transformation,[status(thm)],[f47])).
% 0.11/0.45 fof(f49,plain,(
% 0.11/0.45 ![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.11/0.45 inference(miniscoping,[status(thm)],[f48])).
% 0.11/0.45 fof(f50,plain,(
% 0.11/0.45 ![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.11/0.45 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))],[f49])).
% 0.11/0.45 fof(f51,plain,(
% 0.11/0.45 ![X0,X1,X2]: (~relation(X0)|~X1=relation_dom(X0)|~in(X2,X1)|in(ordered_pair(X2,sK1_skl(X2,X1,X0)),X0))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f50])).
% 0.11/0.45 fof(f52,plain,(
% 0.11/0.45 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_dom(X0)|in(X2,X1)|~in(ordered_pair(X2,X3),X0))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f50])).
% 0.11/0.45 fof(f55,plain,(
% 0.11/0.45 ![A]: (~relation(A)|(![B]: (B=relation_rng(A)<=>(![C]: (in(C,B)<=>(?[D]: in(ordered_pair(D,C),A)))))))),
% 0.11/0.45 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.11/0.45 fof(f56,plain,(
% 0.11/0.45 ![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.11/0.45 inference(NNF_transformation,[status(thm)],[f55])).
% 0.11/0.45 fof(f57,plain,(
% 0.11/0.45 ![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.11/0.45 inference(miniscoping,[status(thm)],[f56])).
% 0.11/0.45 fof(f58,plain,(
% 0.11/0.45 ![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.11/0.45 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))],[f57])).
% 0.11/0.45 fof(f59,plain,(
% 0.11/0.45 ![X0,X1,X2]: (~relation(X0)|~X1=relation_rng(X0)|~in(X2,X1)|in(ordered_pair(sK4_skl(X2,X1,X0),X2),X0))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f58])).
% 0.11/0.45 fof(f60,plain,(
% 0.11/0.45 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_rng(X0)|in(X2,X1)|~in(ordered_pair(X3,X2),X0))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f58])).
% 0.11/0.45 fof(f85,plain,(
% 0.11/0.45 ![A]: subset(A,A)),
% 0.11/0.45 inference(miniscoping,[status(thm)],[f26])).
% 0.11/0.45 fof(f86,plain,(
% 0.11/0.45 ![X0]: (subset(X0,X0))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f85])).
% 0.11/0.45 fof(f89,plain,(
% 0.11/0.45 (?[A]: (relation(A)&(?[B]: (relation(B)&(subset(A,B)&(~subset(relation_dom(A),relation_dom(B))|~subset(relation_rng(A),relation_rng(B))))))))),
% 0.11/0.45 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.11/0.45 fof(f90,plain,(
% 0.11/0.45 (relation(sK13_skl)&(relation(sK14_skl)&(subset(sK13_skl,sK14_skl)&(~subset(relation_dom(sK13_skl),relation_dom(sK14_skl))|~subset(relation_rng(sK13_skl),relation_rng(sK14_skl))))))),
% 0.11/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(A,sK13_skl),skolemize(B,sK14_skl)],[f89])).
% 0.11/0.45 fof(f91,plain,(
% 0.11/0.45 relation(sK13_skl)),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f90])).
% 0.11/0.45 fof(f92,plain,(
% 0.11/0.45 relation(sK14_skl)),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f90])).
% 0.11/0.45 fof(f93,plain,(
% 0.11/0.45 subset(sK13_skl,sK14_skl)),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f90])).
% 0.11/0.45 fof(f94,plain,(
% 0.11/0.45 ~subset(relation_dom(sK13_skl),relation_dom(sK14_skl))|~subset(relation_rng(sK13_skl),relation_rng(sK14_skl))),
% 0.11/0.45 inference(cnf_transformation,[status(thm)],[f90])).
% 0.11/0.45 fof(f115,definition,(
% 0.11/0.45 sQ0_spl <=> (subset(relation_dom(sK13_skl),relation_dom(sK14_skl)))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f118,definition,(
% 0.11/0.45 sQ1_spl <=> (subset(relation_rng(sK13_skl),relation_rng(sK14_skl)))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f121,plain,(
% 0.11/0.45 ~sQ0_spl|~sQ1_spl),
% 0.11/0.45 inference(split_clause,[status(thm)],[f94,f115,f118])).
% 0.11/0.45 fof(f122,plain,(
% 0.11/0.45 ![X0,X1]: (~relation(X0)|~in(X1,relation_dom(X0))|in(ordered_pair(X1,sK1_skl(X1,relation_dom(X0),X0)),X0))),
% 0.11/0.45 inference(destructive_equality_resolution,[status(thm)],[f51])).
% 0.11/0.45 fof(f123,plain,(
% 0.11/0.45 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_dom(X0))|~in(ordered_pair(X1,X2),X0))),
% 0.11/0.45 inference(destructive_equality_resolution,[status(thm)],[f52])).
% 0.11/0.45 fof(f124,plain,(
% 0.11/0.45 ![X0,X1]: (~relation(X0)|~in(X1,relation_rng(X0))|in(ordered_pair(sK4_skl(X1,relation_rng(X0),X0),X1),X0))),
% 0.11/0.45 inference(destructive_equality_resolution,[status(thm)],[f59])).
% 0.11/0.45 fof(f125,plain,(
% 0.11/0.45 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_rng(X0))|~in(ordered_pair(X2,X1),X0))),
% 0.11/0.45 inference(destructive_equality_resolution,[status(thm)],[f60])).
% 0.11/0.45 fof(f126,plain,(
% 0.11/0.45 ![X0]: (~in(X0,sK13_skl)|in(X0,sK14_skl))),
% 0.11/0.45 inference(resolution,[status(thm)],[f44,f93])).
% 0.11/0.45 fof(f139,definition,(
% 0.11/0.45 sQ3_spl <=> (relation(sK14_skl))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f141,plain,(
% 0.11/0.45 ~relation(sK14_skl)|sQ3_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f139])).
% 0.11/0.45 fof(f147,plain,(
% 0.11/0.45 $false|sQ3_spl),
% 0.11/0.45 inference(forward_subsumption_resolution,[status(thm)],[f141,f92])).
% 0.11/0.45 fof(f148,plain,(
% 0.11/0.45 sQ3_spl),
% 0.11/0.45 inference(contradiction_clause,[status(thm)],[f147])).
% 0.11/0.45 fof(f172,definition,(
% 0.11/0.45 sQ5_spl <=> (relation(sK13_skl))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f174,plain,(
% 0.11/0.45 ~relation(sK13_skl)|sQ5_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f172])).
% 0.11/0.45 fof(f179,plain,(
% 0.11/0.45 $false|sQ5_spl),
% 0.11/0.45 inference(forward_subsumption_resolution,[status(thm)],[f174,f91])).
% 0.11/0.45 fof(f180,plain,(
% 0.11/0.45 sQ5_spl),
% 0.11/0.45 inference(contradiction_clause,[status(thm)],[f179])).
% 0.11/0.45 fof(f210,plain,(
% 0.11/0.45 ![X0]: (subset(sK13_skl,X0)|in(sK0_skl(X0,sK13_skl),sK14_skl))),
% 0.11/0.45 inference(resolution,[status(thm)],[f45,f126])).
% 0.11/0.45 fof(f213,plain,(
% 0.11/0.45 ![X0,X1,X2]: (subset(X0,X1)|~subset(X0,X2)|in(sK0_skl(X1,X0),X2))),
% 0.11/0.45 inference(resolution,[status(thm)],[f45,f44])).
% 0.11/0.45 fof(f215,plain,(
% 0.11/0.45 subset(sK13_skl,sK14_skl)|subset(sK13_skl,sK14_skl)),
% 0.11/0.45 inference(resolution,[status(thm)],[f210,f46])).
% 0.11/0.45 fof(f219,definition,(
% 0.11/0.45 sQ9_spl <=> (subset(sK13_skl,sK14_skl))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f222,plain,(
% 0.11/0.45 sQ9_spl),
% 0.11/0.45 inference(split_clause,[status(thm)],[f215,f219])).
% 0.11/0.45 fof(f405,plain,(
% 0.11/0.45 ![X0,X1,X2]: (subset(X0,X1)|~subset(X0,relation_rng(X2))|~relation(X2)|in(ordered_pair(sK4_skl(sK0_skl(X1,X0),relation_rng(X2),X2),sK0_skl(X1,X0)),X2))),
% 0.11/0.45 inference(resolution,[status(thm)],[f213,f124])).
% 0.11/0.45 fof(f406,plain,(
% 0.11/0.45 ![X0,X1,X2]: (subset(X0,X1)|~subset(X0,relation_dom(X2))|~relation(X2)|in(ordered_pair(sK0_skl(X1,X0),sK1_skl(sK0_skl(X1,X0),relation_dom(X2),X2)),X2))),
% 0.11/0.45 inference(resolution,[status(thm)],[f213,f122])).
% 0.11/0.45 fof(f461,definition,(
% 0.11/0.45 sQ29_spl <=> (subset(sK13_skl,sK13_skl))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f463,plain,(
% 0.11/0.45 ~subset(sK13_skl,sK13_skl)|sQ29_spl),
% 0.11/0.45 inference(component_clause,[status(thm)],[f461])).
% 0.11/0.45 fof(f465,plain,(
% 0.11/0.45 $false|sQ29_spl),
% 0.11/0.45 inference(forward_subsumption_resolution,[status(thm)],[f463,f86])).
% 0.11/0.45 fof(f466,plain,(
% 0.11/0.45 sQ29_spl),
% 0.11/0.45 inference(contradiction_clause,[status(thm)],[f465])).
% 0.11/0.45 fof(f536,plain,(
% 0.11/0.45 ![X0,X1]: (subset(X0,X1)|~subset(X0,relation_rng(sK13_skl))|~relation(sK13_skl)|in(ordered_pair(sK4_skl(sK0_skl(X1,X0),relation_rng(sK13_skl),sK13_skl),sK0_skl(X1,X0)),sK14_skl))),
% 0.11/0.45 inference(resolution,[status(thm)],[f405,f126])).
% 0.11/0.45 fof(f542,definition,(
% 0.11/0.45 ![X0,X1]: (sQ33_spl <=> (subset(X0,X1)|~subset(X0,relation_rng(sK13_skl))|in(ordered_pair(sK4_skl(sK0_skl(X1,X0),relation_rng(sK13_skl),sK13_skl),sK0_skl(X1,X0)),sK14_skl)))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f543,plain,(
% 0.11/0.45 ![X0,X1]: (subset(X0,X1)|~subset(X0,relation_rng(sK13_skl))|in(ordered_pair(sK4_skl(sK0_skl(X1,X0),relation_rng(sK13_skl),sK13_skl),sK0_skl(X1,X0)),sK14_skl)|~sQ33_spl)),
% 0.11/0.45 inference(component_clause,[status(thm)],[f542])).
% 0.11/0.45 fof(f545,plain,(
% 0.11/0.45 sQ33_spl|~sQ5_spl),
% 0.11/0.45 inference(split_clause,[status(thm)],[f536,f542,f172])).
% 0.11/0.45 fof(f551,plain,(
% 0.11/0.45 ![X0,X1]: (subset(X0,X1)|~subset(X0,relation_dom(sK13_skl))|~relation(sK13_skl)|in(ordered_pair(sK0_skl(X1,X0),sK1_skl(sK0_skl(X1,X0),relation_dom(sK13_skl),sK13_skl)),sK14_skl))),
% 0.11/0.45 inference(resolution,[status(thm)],[f406,f126])).
% 0.11/0.45 fof(f557,definition,(
% 0.11/0.45 ![X0,X1]: (sQ34_spl <=> (subset(X0,X1)|~subset(X0,relation_dom(sK13_skl))|in(ordered_pair(sK0_skl(X1,X0),sK1_skl(sK0_skl(X1,X0),relation_dom(sK13_skl),sK13_skl)),sK14_skl)))),
% 0.11/0.45 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.11/0.45 fof(f558,plain,(
% 0.11/0.45 ![X0,X1]: (subset(X0,X1)|~subset(X0,relation_dom(sK13_skl))|in(ordered_pair(sK0_skl(X1,X0),sK1_skl(sK0_skl(X1,X0),relation_dom(sK13_skl),sK13_skl)),sK14_skl)|~sQ34_spl)),
% 0.11/0.46 inference(component_clause,[status(thm)],[f557])).
% 0.11/0.46 fof(f560,plain,(
% 0.11/0.46 sQ34_spl|~sQ5_spl),
% 0.11/0.46 inference(split_clause,[status(thm)],[f551,f557,f172])).
% 0.11/0.46 fof(f664,plain,(
% 0.11/0.46 ![X0,X1]: (subset(X0,X1)|~subset(X0,relation_rng(sK13_skl))|~relation(sK14_skl)|in(sK0_skl(X1,X0),relation_rng(sK14_skl))|~sQ33_spl)),
% 0.11/0.46 inference(resolution,[status(thm)],[f543,f125])).
% 0.11/0.46 fof(f669,definition,(
% 0.11/0.46 ![X0,X1]: (sQ40_spl <=> (subset(X0,X1)|~subset(X0,relation_rng(sK13_skl))|in(sK0_skl(X1,X0),relation_rng(sK14_skl))))),
% 0.11/0.46 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.11/0.46 fof(f670,plain,(
% 0.11/0.46 ![X0,X1]: (subset(X0,X1)|~subset(X0,relation_rng(sK13_skl))|in(sK0_skl(X1,X0),relation_rng(sK14_skl))|~sQ40_spl)),
% 0.11/0.46 inference(component_clause,[status(thm)],[f669])).
% 0.11/0.46 fof(f672,plain,(
% 0.11/0.46 sQ40_spl|~sQ3_spl|~sQ33_spl),
% 0.11/0.46 inference(split_clause,[status(thm)],[f664,f669,f139,f542])).
% 0.11/0.46 fof(f743,plain,(
% 0.11/0.46 ![X0,X1]: (subset(X0,X1)|~subset(X0,relation_dom(sK13_skl))|~relation(sK14_skl)|in(sK0_skl(X1,X0),relation_dom(sK14_skl))|~sQ34_spl)),
% 0.11/0.46 inference(resolution,[status(thm)],[f558,f123])).
% 0.11/0.46 fof(f751,definition,(
% 0.11/0.46 ![X0,X1]: (sQ46_spl <=> (subset(X0,X1)|~subset(X0,relation_dom(sK13_skl))|in(sK0_skl(X1,X0),relation_dom(sK14_skl))))),
% 0.11/0.46 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.11/0.46 fof(f752,plain,(
% 0.11/0.46 ![X0,X1]: (subset(X0,X1)|~subset(X0,relation_dom(sK13_skl))|in(sK0_skl(X1,X0),relation_dom(sK14_skl))|~sQ46_spl)),
% 0.11/0.46 inference(component_clause,[status(thm)],[f751])).
% 0.11/0.46 fof(f754,plain,(
% 0.11/0.46 sQ46_spl|~sQ3_spl|~sQ34_spl),
% 0.11/0.46 inference(split_clause,[status(thm)],[f743,f751,f139,f557])).
% 0.11/0.46 fof(f762,plain,(
% 0.11/0.46 ![X0]: (subset(relation_rng(sK13_skl),X0)|in(sK0_skl(X0,relation_rng(sK13_skl)),relation_rng(sK14_skl))|~sQ40_spl)),
% 0.11/0.46 inference(resolution,[status(thm)],[f670,f86])).
% 0.11/0.46 fof(f773,plain,(
% 0.11/0.46 subset(relation_rng(sK13_skl),relation_rng(sK14_skl))|subset(relation_rng(sK13_skl),relation_rng(sK14_skl))|~sQ40_spl),
% 0.11/0.46 inference(resolution,[status(thm)],[f762,f46])).
% 0.11/0.46 fof(f778,plain,(
% 0.11/0.46 sQ1_spl|~sQ40_spl),
% 0.11/0.46 inference(split_clause,[status(thm)],[f773,f118,f669])).
% 0.11/0.46 fof(f783,plain,(
% 0.11/0.46 ![X0]: (subset(relation_dom(sK13_skl),X0)|in(sK0_skl(X0,relation_dom(sK13_skl)),relation_dom(sK14_skl))|~sQ46_spl)),
% 0.11/0.46 inference(resolution,[status(thm)],[f752,f86])).
% 0.11/0.46 fof(f794,plain,(
% 0.11/0.46 subset(relation_dom(sK13_skl),relation_dom(sK14_skl))|subset(relation_dom(sK13_skl),relation_dom(sK14_skl))|~sQ46_spl),
% 0.11/0.46 inference(resolution,[status(thm)],[f783,f46])).
% 0.11/0.46 fof(f799,plain,(
% 0.11/0.46 sQ0_spl|~sQ46_spl),
% 0.11/0.46 inference(split_clause,[status(thm)],[f794,f115,f751])).
% 0.11/0.46 fof(f804,plain,(
% 0.11/0.46 $false),
% 0.11/0.46 inference(sat_refutation,[status(thm)],[f121,f148,f180,f222,f466,f545,f560,f672,f754,f778,f799])).
% 0.11/0.46 % SZS output end CNFRefutation for theBenchmark.p
% 0.71/0.48 % Elapsed time: 0.098038 seconds
% 0.71/0.48 % CPU time: 0.507169 seconds
% 0.71/0.48 % Total memory used: 109.360 MB
% 0.71/0.48 % Net memory used: 108.320 MB
%------------------------------------------------------------------------------