%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU189+1 : 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 : n001.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.13s 10.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU189+1 : 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/10.37 % Computer : n001.cluster.edu
% 0.09/10.37 % Model : x86_64 x86_64
% 0.09/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.37 % Memory : 8046.5625MB
% 0.09/10.37 % OS : Linux 6.8.0-71-generic
% 0.09/10.37 % CPULimit : 300
% 0.09/10.37 % WCLimit : 300
% 0.09/10.37 % DateTime : Mon Sep 21 06:02:09 UTC 2026
% 0.09/10.37 % CPUTime :
% 0.09/10.38 % Drodi V4.1.1
% 0.13/10.40 % Refutation found
% 0.13/10.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/10.40 % SZS output start CNFRefutation for theBenchmark
% 0.13/10.40 fof(f10,axiom,(
% 0.13/10.40 (! [A] :( ( ~ empty(A)& relation(A) )=> ~ empty(relation_rng(A)) ) )),
% 0.13/10.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/10.40 fof(f11,axiom,(
% 0.13/10.40 (! [A] :( empty(A)=> ( empty(relation_dom(A))& relation(relation_dom(A)) ) ) )),
% 0.13/10.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/10.40 fof(f20,axiom,(
% 0.13/10.40 ( empty(empty_set)& relation(empty_set) ) ),
% 0.13/10.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/10.40 fof(f22,axiom,(
% 0.13/10.40 (! [A] :( empty(A)=> A = empty_set ) )),
% 0.13/10.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/10.40 fof(f23,conjecture,(
% 0.13/10.40 (! [A] :( relation(A)=> ( relation_dom(A) = empty_set<=> relation_rng(A) = empty_set ) ) )),
% 0.13/10.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/10.40 fof(f24,negated_conjecture,(
% 0.13/10.40 ~((! [A] :( relation(A)=> ( relation_dom(A) = empty_set<=> relation_rng(A) = empty_set ) ) ))),
% 0.13/10.40 inference(negated_conjecture,[status(cth)],[f23])).
% 0.13/10.40 fof(f25,axiom,(
% 0.13/10.40 ( relation_dom(empty_set) = empty_set& relation_rng(empty_set) = empty_set ) ),
% 0.13/10.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/10.40 fof(f26,axiom,(
% 0.13/10.40 (! [A] :( relation(A)=> ( ( relation_dom(A) = empty_set| relation_rng(A) = empty_set )=> A = empty_set ) ) )),
% 0.13/10.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/10.40 fof(f45,plain,(
% 0.13/10.40 ![A]: ((empty(A)|~relation(A))|~empty(relation_rng(A)))),
% 0.13/10.40 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.13/10.40 fof(f46,plain,(
% 0.13/10.40 ![X0]: (empty(X0)|~relation(X0)|~empty(relation_rng(X0)))),
% 0.13/10.40 inference(cnf_transformation,[status(thm)],[f45])).
% 0.13/10.40 fof(f47,plain,(
% 0.13/10.40 ![A]: (~empty(A)|(empty(relation_dom(A))&relation(relation_dom(A))))),
% 0.13/10.40 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.13/10.40 fof(f48,plain,(
% 0.13/10.40 ![X0]: (~empty(X0)|empty(relation_dom(X0)))),
% 0.13/10.40 inference(cnf_transformation,[status(thm)],[f47])).
% 0.13/10.40 fof(f63,plain,(
% 0.13/10.40 empty(empty_set)),
% 0.13/10.40 inference(cnf_transformation,[status(thm)],[f20])).
% 0.13/10.40 fof(f66,plain,(
% 0.13/10.40 ![A]: (~empty(A)|A=empty_set)),
% 0.13/10.40 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.13/10.40 fof(f67,plain,(
% 0.13/10.40 ![X0]: (~empty(X0)|X0=empty_set)),
% 0.13/10.40 inference(cnf_transformation,[status(thm)],[f66])).
% 0.13/10.40 fof(f68,plain,(
% 0.13/10.40 (?[A]: (relation(A)&(relation_dom(A)=empty_set<~>relation_rng(A)=empty_set)))),
% 0.13/10.40 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.13/10.40 fof(f69,plain,(
% 0.13/10.40 ?[A]: (relation(A)&((relation_dom(A)=empty_set|relation_rng(A)=empty_set)&(~relation_dom(A)=empty_set|~relation_rng(A)=empty_set)))),
% 0.13/10.40 inference(NNF_transformation,[status(thm)],[f68])).
% 0.13/10.40 fof(f70,plain,(
% 0.13/10.40 (relation(sK5_skl)&((relation_dom(sK5_skl)=empty_set|relation_rng(sK5_skl)=empty_set)&(~relation_dom(sK5_skl)=empty_set|~relation_rng(sK5_skl)=empty_set)))),
% 0.13/10.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f69])).
% 0.13/10.40 fof(f71,plain,(
% 0.13/10.40 relation(sK5_skl)),
% 0.13/10.40 inference(cnf_transformation,[status(thm)],[f70])).
% 0.13/10.40 fof(f72,plain,(
% 0.13/10.40 relation_dom(sK5_skl)=empty_set|relation_rng(sK5_skl)=empty_set),
% 0.13/10.40 inference(cnf_transformation,[status(thm)],[f70])).
% 0.13/10.40 fof(f73,plain,(
% 0.13/10.40 ~relation_dom(sK5_skl)=empty_set|~relation_rng(sK5_skl)=empty_set),
% 0.13/10.40 inference(cnf_transformation,[status(thm)],[f70])).
% 0.13/10.40 fof(f75,plain,(
% 0.13/10.40 relation_rng(empty_set)=empty_set),
% 0.13/10.40 inference(cnf_transformation,[status(thm)],[f25])).
% 0.13/10.40 fof(f76,plain,(
% 0.13/10.40 ![A]: (~relation(A)|((~relation_dom(A)=empty_set&~relation_rng(A)=empty_set)|A=empty_set))),
% 0.13/10.40 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.13/10.40 fof(f77,plain,(
% 0.13/10.40 ![X0]: (~relation(X0)|~relation_dom(X0)=empty_set|X0=empty_set)),
% 0.13/10.40 inference(cnf_transformation,[status(thm)],[f76])).
% 0.13/10.40 fof(f80,plain,(
% 0.13/10.40 empty(sK5_skl)|~relation(sK5_skl)|~empty(empty_set)|relation_dom(sK5_skl)=empty_set),
% 0.13/10.40 inference(paramodulation,[status(thm)],[f72,f46])).
% 0.13/10.40 fof(f81,plain,(
% 0.13/10.40 empty(sK5_skl)|~empty(empty_set)|relation_dom(sK5_skl)=empty_set),
% 0.13/10.40 inference(forward_subsumption_resolution,[status(thm)],[f80,f71])).
% 0.13/10.40 fof(f100,plain,(
% 0.13/10.40 empty(relation_dom(sK5_skl))|~empty(empty_set)|relation_dom(sK5_skl)=empty_set),
% 0.13/10.40 inference(resolution,[status(thm)],[f48,f81])).
% 0.13/10.40 fof(f102,plain,(
% 0.13/10.40 ~empty(empty_set)|relation_dom(sK5_skl)=empty_set),
% 0.13/10.40 inference(forward_subsumption_resolution,[status(thm)],[f100,f67])).
% 0.13/10.40 fof(f114,plain,(
% 0.13/10.40 relation_dom(sK5_skl)=empty_set),
% 0.13/10.40 inference(resolution,[status(thm)],[f102,f63])).
% 0.13/10.40 fof(f117,plain,(
% 0.13/10.40 ~empty_set=empty_set|~relation_rng(sK5_skl)=empty_set),
% 0.13/10.40 inference(backward_demodulation,[status(thm)],[f114,f73])).
% 0.13/10.40 fof(f119,plain,(
% 0.13/10.40 ~relation_rng(sK5_skl)=empty_set),
% 0.13/10.40 inference(trivial_equality_resolution,[status(thm)],[f117])).
% 0.13/10.40 fof(f122,plain,(
% 0.13/10.40 ~relation_dom(sK5_skl)=empty_set|sK5_skl=empty_set),
% 0.13/10.40 inference(resolution,[status(thm)],[f77,f71])).
% 0.13/10.40 fof(f124,plain,(
% 0.13/10.40 ~empty_set=empty_set|sK5_skl=empty_set),
% 0.13/10.40 inference(forward_demodulation,[status(thm)],[f114,f122])).
% 0.13/10.40 fof(f126,plain,(
% 0.13/10.40 ~relation_rng(empty_set)=empty_set),
% 0.13/10.40 inference(backward_demodulation,[status(thm)],[f129,f119])).
% 0.13/10.40 fof(f129,plain,(
% 0.13/10.40 sK5_skl=empty_set),
% 0.13/10.40 inference(trivial_equality_resolution,[status(thm)],[f124])).
% 0.13/10.40 fof(f130,plain,(
% 0.13/10.40 ~empty_set=empty_set),
% 0.13/10.40 inference(forward_demodulation,[status(thm)],[f75,f126])).
% 0.13/10.40 fof(f131,plain,(
% 0.13/10.40 $false),
% 0.13/10.40 inference(trivial_equality_resolution,[status(thm)],[f130])).
% 0.13/10.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/10.43 % Elapsed time: 0.054150 seconds
% 0.13/10.43 % CPU time: 0.161047 seconds
% 0.13/10.43 % Total memory used: 101.947 MB
% 0.13/10.43 % Net memory used: 101.685 MB
%------------------------------------------------------------------------------