%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU196+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 : n011.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:57 PM UTC 2026
% Result : Theorem 0.17s 0.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU196+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.51 % Computer : n011.cluster.edu
% 0.09/0.51 % Model : x86_64 x86_64
% 0.09/0.51 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.51 % Memory : 8046.5625MB
% 0.09/0.51 % OS : Linux 6.8.0-71-generic
% 0.09/0.51 % CPULimit : 300
% 0.09/0.51 % WCLimit : 300
% 0.09/0.51 % DateTime : Mon Sep 21 05:56:25 UTC 2026
% 0.09/0.52 % CPUTime :
% 0.09/0.54 % Drodi V4.1.1
% 0.17/0.56 % Refutation found
% 0.17/0.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.56 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.56 fof(f58,axiom,(
% 0.17/0.56 (! [A,B] :( relation(A)=> relation(relation_dom_restriction(A,B)) ) )),
% 0.17/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.56 fof(f122,lemma,(
% 0.17/0.56 (! [A] :( relation(A)=> (! [B] :( relation(B)=> ( subset(A,B)=> ( subset(relation_dom(A),relation_dom(B))& subset(relation_rng(A),relation_rng(B)) ) ) ) )) )),
% 0.17/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.56 fof(f177,lemma,(
% 0.17/0.56 (! [A,B] :( relation(B)=> subset(relation_dom_restriction(B,A),B) ) )),
% 0.17/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.56 fof(f184,conjecture,(
% 0.17/0.56 (! [A,B] :( relation(B)=> subset(relation_rng(relation_dom_restriction(B,A)),relation_rng(B)) ) )),
% 0.17/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.56 fof(f185,negated_conjecture,(
% 0.17/0.56 ~((! [A,B] :( relation(B)=> subset(relation_rng(relation_dom_restriction(B,A)),relation_rng(B)) ) ))),
% 0.17/0.56 inference(negated_conjecture,[status(cth)],[f184])).
% 0.17/0.56 fof(f414,plain,(
% 0.17/0.56 ![A,B]: (~relation(A)|relation(relation_dom_restriction(A,B)))),
% 0.17/0.56 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 0.17/0.56 fof(f415,plain,(
% 0.17/0.56 ![A]: (~relation(A)|(![B]: relation(relation_dom_restriction(A,B))))),
% 0.17/0.56 inference(miniscoping,[status(thm)],[f414])).
% 0.17/0.56 fof(f416,plain,(
% 0.17/0.56 ![X0,X1]: (~relation(X0)|relation(relation_dom_restriction(X0,X1)))),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f415])).
% 0.17/0.56 fof(f570,plain,(
% 0.17/0.56 ![A]: (~relation(A)|(![B]: (~relation(B)|(~subset(A,B)|(subset(relation_dom(A),relation_dom(B))&subset(relation_rng(A),relation_rng(B)))))))),
% 0.17/0.56 inference(pre_NNF_transformation,[status(thm)],[f122])).
% 0.17/0.56 fof(f572,plain,(
% 0.17/0.56 ![X0,X1]: (~relation(X0)|~relation(X1)|~subset(X0,X1)|subset(relation_rng(X0),relation_rng(X1)))),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f570])).
% 0.17/0.56 fof(f723,plain,(
% 0.17/0.56 ![A,B]: (~relation(B)|subset(relation_dom_restriction(B,A),B))),
% 0.17/0.56 inference(pre_NNF_transformation,[status(thm)],[f177])).
% 0.17/0.56 fof(f724,plain,(
% 0.17/0.56 ![B]: (~relation(B)|(![A]: subset(relation_dom_restriction(B,A),B)))),
% 0.17/0.56 inference(miniscoping,[status(thm)],[f723])).
% 0.17/0.56 fof(f725,plain,(
% 0.17/0.56 ![X0,X1]: (~relation(X0)|subset(relation_dom_restriction(X0,X1),X0))),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f724])).
% 0.17/0.56 fof(f742,plain,(
% 0.17/0.56 (?[A,B]: (relation(B)&~subset(relation_rng(relation_dom_restriction(B,A)),relation_rng(B))))),
% 0.17/0.56 inference(pre_NNF_transformation,[status(thm)],[f185])).
% 0.17/0.56 fof(f743,plain,(
% 0.17/0.56 ?[B]: (relation(B)&(?[A]: ~subset(relation_rng(relation_dom_restriction(B,A)),relation_rng(B))))),
% 0.17/0.56 inference(miniscoping,[status(thm)],[f742])).
% 0.17/0.56 fof(f744,plain,(
% 0.17/0.56 (relation(sK57_skl)&~subset(relation_rng(relation_dom_restriction(sK57_skl,sK58_skl)),relation_rng(sK57_skl)))),
% 0.17/0.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK57_skl,sK58_skl]),skolemize(B,sK57_skl),skolemize(A,sK58_skl)],[f743])).
% 0.17/0.56 fof(f745,plain,(
% 0.17/0.56 relation(sK57_skl)),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f744])).
% 0.17/0.56 fof(f746,plain,(
% 0.17/0.56 ~subset(relation_rng(relation_dom_restriction(sK57_skl,sK58_skl)),relation_rng(sK57_skl))),
% 0.17/0.56 inference(cnf_transformation,[status(thm)],[f744])).
% 0.17/0.56 fof(f818,plain,(
% 0.17/0.56 ![X0]: (relation(relation_dom_restriction(sK57_skl,X0)))),
% 0.17/0.56 inference(resolution,[status(thm)],[f416,f745])).
% 0.17/0.56 fof(f821,plain,(
% 0.17/0.56 ![X0]: (subset(relation_dom_restriction(sK57_skl,X0),sK57_skl))),
% 0.17/0.56 inference(resolution,[status(thm)],[f725,f745])).
% 0.17/0.56 fof(f1139,plain,(
% 0.17/0.56 ![X0]: (~relation(relation_dom_restriction(sK57_skl,X0))|~relation(sK57_skl)|subset(relation_rng(relation_dom_restriction(sK57_skl,X0)),relation_rng(sK57_skl)))),
% 0.17/0.56 inference(resolution,[status(thm)],[f572,f821])).
% 0.17/0.56 fof(f1150,definition,(
% 0.17/0.56 sQ17_spl <=> (relation(sK57_skl))),
% 0.17/0.56 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.17/0.56 fof(f1152,plain,(
% 0.17/0.56 ~relation(sK57_skl)|sQ17_spl),
% 0.17/0.56 inference(component_clause,[status(thm)],[f1150])).
% 0.17/0.56 fof(f1160,definition,(
% 0.17/0.56 ![X0]: (sQ19_spl <=> (~relation(relation_dom_restriction(sK57_skl,X0))|subset(relation_rng(relation_dom_restriction(sK57_skl,X0)),relation_rng(sK57_skl))))),
% 0.17/0.56 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.17/0.56 fof(f1161,plain,(
% 0.17/0.56 ![X0]: (~relation(relation_dom_restriction(sK57_skl,X0))|subset(relation_rng(relation_dom_restriction(sK57_skl,X0)),relation_rng(sK57_skl))|~sQ19_spl)),
% 0.17/0.56 inference(component_clause,[status(thm)],[f1160])).
% 0.17/0.56 fof(f1163,plain,(
% 0.17/0.56 sQ19_spl|~sQ17_spl),
% 0.17/0.56 inference(split_clause,[status(thm)],[f1139,f1160,f1150])).
% 0.17/0.56 fof(f1165,plain,(
% 0.17/0.56 $false|sQ17_spl),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1152,f745])).
% 0.17/0.56 fof(f1166,plain,(
% 0.17/0.56 sQ17_spl),
% 0.17/0.56 inference(contradiction_clause,[status(thm)],[f1165])).
% 0.17/0.56 fof(f1170,plain,(
% 0.17/0.56 ![X0]: (subset(relation_rng(relation_dom_restriction(sK57_skl,X0)),relation_rng(sK57_skl))|~sQ19_spl)),
% 0.17/0.56 inference(forward_subsumption_resolution,[status(thm)],[f1161,f818])).
% 0.17/0.56 fof(f1240,plain,(
% 0.17/0.56 $false|~sQ19_spl),
% 0.17/0.56 inference(backward_subsumption_resolution,[status(thm)],[f746,f1170])).
% 0.17/0.56 fof(f1245,plain,(
% 0.17/0.56 ~sQ19_spl),
% 0.17/0.56 inference(contradiction_clause,[status(thm)],[f1240])).
% 0.17/0.56 fof(f1246,plain,(
% 0.17/0.56 $false),
% 0.17/0.56 inference(sat_refutation,[status(thm)],[f1163,f1166,f1245])).
% 0.17/0.56 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/0.59 % Elapsed time: 0.065826 seconds
% 0.17/0.59 % CPU time: 0.207340 seconds
% 0.17/0.59 % Total memory used: 88.135 MB
% 0.17/0.59 % Net memory used: 87.802 MB
%------------------------------------------------------------------------------