%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU096+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:40 PM UTC 2026
% Result : Theorem 0.16s 0.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU096+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n026.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 05:52:37 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 0.16/0.47 % Refutation found
% 0.16/0.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.47 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.47 fof(f15,axiom,(
% 0.16/0.47 (! [A,B] :( ( relation(A)& function(A)& finite(B) )=> finite(relation_image(A,B)) ) )),
% 0.16/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.47 fof(f18,axiom,(
% 0.16/0.47 ( relation(empty_set)& relation_empty_yielding(empty_set)& function(empty_set)& one_to_one(empty_set)& empty(empty_set)& epsilon_transitive(empty_set)& epsilon_connected(empty_set)& ordinal(empty_set) ) ),
% 0.16/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.47 fof(f50,axiom,(
% 0.16/0.47 (! [A,B] :( ( relation(B)& function(B) )=> ( subset(A,relation_rng(B))=> relation_image(B,relation_inverse_image(B,A)) = A ) ) )),
% 0.16/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.47 fof(f53,conjecture,(
% 0.16/0.47 (! [A,B] :( ( relation(B)& function(B) )=> ( ( subset(A,relation_rng(B))& finite(relation_inverse_image(B,A)) )=> finite(A) ) ) )),
% 0.16/0.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.47 fof(f54,negated_conjecture,(
% 0.16/0.47 ~((! [A,B] :( ( relation(B)& function(B) )=> ( ( subset(A,relation_rng(B))& finite(relation_inverse_image(B,A)) )=> finite(A) ) ) ))),
% 0.16/0.47 inference(negated_conjecture,[status(cth)],[f53])).
% 0.16/0.47 fof(f104,plain,(
% 0.16/0.47 ![A,B]: (((~relation(A)|~function(A))|~finite(B))|finite(relation_image(A,B)))),
% 0.16/0.47 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.16/0.47 fof(f105,plain,(
% 0.16/0.47 ![X0,X1]: (~relation(X0)|~function(X0)|~finite(X1)|finite(relation_image(X0,X1)))),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f104])).
% 0.16/0.47 fof(f113,plain,(
% 0.16/0.47 epsilon_transitive(empty_set)),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f18])).
% 0.16/0.47 fof(f240,plain,(
% 0.16/0.47 ![A,B]: ((~relation(B)|~function(B))|(~subset(A,relation_rng(B))|relation_image(B,relation_inverse_image(B,A))=A))),
% 0.16/0.47 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.16/0.47 fof(f241,plain,(
% 0.16/0.47 ![B]: ((~relation(B)|~function(B))|(![A]: (~subset(A,relation_rng(B))|relation_image(B,relation_inverse_image(B,A))=A)))),
% 0.16/0.47 inference(miniscoping,[status(thm)],[f240])).
% 0.16/0.47 fof(f242,plain,(
% 0.16/0.47 ![X0,X1]: (~relation(X0)|~function(X0)|~subset(X1,relation_rng(X0))|relation_image(X0,relation_inverse_image(X0,X1))=X1)),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f241])).
% 0.16/0.47 fof(f248,plain,(
% 0.16/0.47 (?[A,B]: ((relation(B)&function(B))&((subset(A,relation_rng(B))&finite(relation_inverse_image(B,A)))&~finite(A))))),
% 0.16/0.47 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 0.16/0.47 fof(f249,plain,(
% 0.16/0.47 ?[B]: ((relation(B)&function(B))&(?[A]: ((subset(A,relation_rng(B))&finite(relation_inverse_image(B,A)))&~finite(A))))),
% 0.16/0.47 inference(miniscoping,[status(thm)],[f248])).
% 0.16/0.47 fof(f250,plain,(
% 0.16/0.47 ((relation(sK26_skl)&function(sK26_skl))&((subset(sK27_skl,relation_rng(sK26_skl))&finite(relation_inverse_image(sK26_skl,sK27_skl)))&~finite(sK27_skl)))),
% 0.16/0.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl,sK27_skl]),skolemize(B,sK26_skl),skolemize(A,sK27_skl)],[f249])).
% 0.16/0.47 fof(f251,plain,(
% 0.16/0.47 relation(sK26_skl)),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f250])).
% 0.16/0.47 fof(f252,plain,(
% 0.16/0.47 function(sK26_skl)),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f250])).
% 0.16/0.47 fof(f253,plain,(
% 0.16/0.47 subset(sK27_skl,relation_rng(sK26_skl))),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f250])).
% 0.16/0.47 fof(f254,plain,(
% 0.16/0.47 finite(relation_inverse_image(sK26_skl,sK27_skl))),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f250])).
% 0.16/0.47 fof(f255,plain,(
% 0.16/0.47 ~finite(sK27_skl)),
% 0.16/0.47 inference(cnf_transformation,[status(thm)],[f250])).
% 0.16/0.47 fof(f291,plain,(
% 0.16/0.47 ~relation(sK26_skl)|~function(sK26_skl)|relation_image(sK26_skl,relation_inverse_image(sK26_skl,sK27_skl))=sK27_skl),
% 0.16/0.47 inference(resolution,[status(thm)],[f242,f253])).
% 0.16/0.47 fof(f293,definition,(
% 0.16/0.47 sQ2_spl <=> (relation(sK26_skl))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f295,plain,(
% 0.16/0.47 ~relation(sK26_skl)|sQ2_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f293])).
% 0.16/0.47 fof(f296,definition,(
% 0.16/0.47 sQ3_spl <=> (function(sK26_skl))),
% 0.16/0.47 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.16/0.47 fof(f298,plain,(
% 0.16/0.47 ~function(sK26_skl)|sQ3_spl),
% 0.16/0.47 inference(component_clause,[status(thm)],[f296])).
% 0.16/0.48 fof(f299,definition,(
% 0.16/0.48 sQ4_spl <=> (relation_image(sK26_skl,relation_inverse_image(sK26_skl,sK27_skl))=sK27_skl)),
% 0.16/0.48 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.16/0.48 fof(f300,plain,(
% 0.16/0.48 relation_image(sK26_skl,relation_inverse_image(sK26_skl,sK27_skl))=sK27_skl|~sQ4_spl),
% 0.16/0.48 inference(component_clause,[status(thm)],[f299])).
% 0.16/0.48 fof(f302,plain,(
% 0.16/0.48 ~sQ2_spl|~sQ3_spl|sQ4_spl),
% 0.16/0.48 inference(split_clause,[status(thm)],[f291,f293,f296,f299])).
% 0.16/0.48 fof(f383,plain,(
% 0.16/0.48 $false|sQ3_spl),
% 0.16/0.48 inference(forward_subsumption_resolution,[status(thm)],[f298,f252])).
% 0.16/0.48 fof(f384,plain,(
% 0.16/0.48 sQ3_spl),
% 0.16/0.48 inference(contradiction_clause,[status(thm)],[f383])).
% 0.16/0.48 fof(f389,plain,(
% 0.16/0.48 $false|sQ2_spl),
% 0.16/0.48 inference(forward_subsumption_resolution,[status(thm)],[f295,f251])).
% 0.16/0.48 fof(f390,plain,(
% 0.16/0.48 sQ2_spl),
% 0.16/0.48 inference(contradiction_clause,[status(thm)],[f389])).
% 0.16/0.48 fof(f397,definition,(
% 0.16/0.48 sQ19_spl <=> (epsilon_transitive(empty_set))),
% 0.16/0.48 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.16/0.48 fof(f399,plain,(
% 0.16/0.48 ~epsilon_transitive(empty_set)|sQ19_spl),
% 0.16/0.48 inference(component_clause,[status(thm)],[f397])).
% 0.16/0.48 fof(f404,plain,(
% 0.16/0.48 $false|sQ19_spl),
% 0.16/0.48 inference(forward_subsumption_resolution,[status(thm)],[f399,f113])).
% 0.16/0.48 fof(f405,plain,(
% 0.16/0.48 sQ19_spl),
% 0.16/0.48 inference(contradiction_clause,[status(thm)],[f404])).
% 0.16/0.48 fof(f423,plain,(
% 0.16/0.48 ![X0]: (~function(sK26_skl)|~finite(X0)|finite(relation_image(sK26_skl,X0)))),
% 0.16/0.48 inference(resolution,[status(thm)],[f105,f251])).
% 0.16/0.48 fof(f432,definition,(
% 0.16/0.48 ![X0]: (sQ25_spl <=> (~finite(X0)|finite(relation_image(sK26_skl,X0))))),
% 0.16/0.48 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.16/0.48 fof(f433,plain,(
% 0.16/0.48 ![X0]: (~finite(X0)|finite(relation_image(sK26_skl,X0))|~sQ25_spl)),
% 0.16/0.48 inference(component_clause,[status(thm)],[f432])).
% 0.16/0.48 fof(f435,plain,(
% 0.16/0.48 ~sQ3_spl|sQ25_spl),
% 0.16/0.48 inference(split_clause,[status(thm)],[f423,f296,f432])).
% 0.16/0.48 fof(f439,plain,(
% 0.16/0.48 finite(relation_image(sK26_skl,relation_inverse_image(sK26_skl,sK27_skl)))|~sQ25_spl),
% 0.16/0.48 inference(resolution,[status(thm)],[f433,f254])).
% 0.16/0.48 fof(f440,plain,(
% 0.16/0.48 finite(sK27_skl)|~sQ4_spl|~sQ25_spl),
% 0.16/0.48 inference(forward_demodulation,[status(thm)],[f300,f439])).
% 0.16/0.48 fof(f441,plain,(
% 0.16/0.48 $false|~sQ4_spl|~sQ25_spl),
% 0.16/0.48 inference(forward_subsumption_resolution,[status(thm)],[f440,f255])).
% 0.16/0.48 fof(f442,plain,(
% 0.16/0.48 ~sQ4_spl|~sQ25_spl),
% 0.16/0.48 inference(contradiction_clause,[status(thm)],[f441])).
% 0.16/0.48 fof(f443,plain,(
% 0.16/0.48 $false),
% 0.16/0.48 inference(sat_refutation,[status(thm)],[f302,f384,f390,f405,f435,f442])).
% 0.16/0.48 % SZS output end CNFRefutation for theBenchmark.p
% 0.24/0.51 % Elapsed time: 0.072146 seconds
% 0.24/0.51 % CPU time: 0.188249 seconds
% 0.24/0.51 % Total memory used: 73.938 MB
% 0.24/0.51 % Net memory used: 73.903 MB
%------------------------------------------------------------------------------