%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU098+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.13s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU098+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n026.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 05:52:53 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.13/0.39 % Drodi V4.1.1
% 0.13/0.53 % Refutation found
% 0.13/0.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.53 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.53 fof(f15,axiom,(
% 0.13/0.53 (! [A,B] :( relation(first_projection(A,B))& function(first_projection(A,B)) ) )),
% 0.13/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f16,axiom,(
% 0.13/0.53 (! [A,B] :( function(first_projection_as_func_of(A,B))& quasi_total(first_projection_as_func_of(A,B),cartesian_product2(A,B),A)& relation_of2_as_subset(first_projection_as_func_of(A,B),cartesian_product2(A,B),A) ) )),
% 0.13/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f22,axiom,(
% 0.13/0.53 (! [A,B] :( ( relation(A)& function(A)& finite(B) )=> finite(relation_image(A,B)) ) )),
% 0.13/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f23,axiom,(
% 0.13/0.53 (! [A,B] :( ( finite(A)& finite(B) )=> finite(cartesian_product2(A,B)) ) )),
% 0.13/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f62,axiom,(
% 0.13/0.53 (! [A,B,C,D] :( ( function(C)& quasi_total(C,A,B)& relation_of2(C,A,B) )=> function_image(A,B,C,D) = relation_image(C,D) ) )),
% 0.13/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f63,axiom,(
% 0.13/0.53 (! [A,B] : first_projection_as_func_of(A,B) = first_projection(A,B) )),
% 0.13/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f64,axiom,(
% 0.13/0.53 (! [A,B,C] :( relation_of2_as_subset(C,A,B)<=> relation_of2(C,A,B) ) )),
% 0.13/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f66,axiom,(
% 0.13/0.53 (! [A] :( ( relation(A)& function(A) )=> function_image(cartesian_product2(relation_dom(A),relation_rng(A)),relation_dom(A),first_projection_as_func_of(relation_dom(A),relation_rng(A)),A) = relation_dom(A) ) )),
% 0.13/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f67,axiom,(
% 0.13/0.53 (! [A,B] :( ( subset(A,B)& finite(B) )=> finite(A) ) )),
% 0.13/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f71,axiom,(
% 0.13/0.53 (! [A] :( relation(A)=> subset(A,cartesian_product2(relation_dom(A),relation_rng(A))) ) )),
% 0.13/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f72,axiom,(
% 0.13/0.53 (! [A] :( ( relation(A)& function(A) )=> ( finite(relation_dom(A))=> finite(relation_rng(A)) ) ) )),
% 0.13/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f73,conjecture,(
% 0.13/0.53 (! [A] :( ( relation(A)& function(A) )=> ( finite(relation_dom(A))<=> finite(A) ) ) )),
% 0.13/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f74,negated_conjecture,(
% 0.13/0.53 ~((! [A] :( ( relation(A)& function(A) )=> ( finite(relation_dom(A))<=> finite(A) ) ) ))),
% 0.13/0.53 inference(negated_conjecture,[status(cth)],[f73])).
% 0.13/0.53 fof(f125,plain,(
% 0.13/0.53 (![A,B]: relation(first_projection(A,B)))&(![A,B]: function(first_projection(A,B)))),
% 0.13/0.53 inference(miniscoping,[status(thm)],[f15])).
% 0.13/0.53 fof(f126,plain,(
% 0.13/0.53 ![X0,X1]: (relation(first_projection(X0,X1)))),
% 0.13/0.53 inference(cnf_transformation,[status(thm)],[f125])).
% 0.13/0.53 fof(f128,plain,(
% 0.13/0.53 ((![A,B]: function(first_projection_as_func_of(A,B)))&(![A,B]: quasi_total(first_projection_as_func_of(A,B),cartesian_product2(A,B),A)))&(![A,B]: relation_of2_as_subset(first_projection_as_func_of(A,B),cartesian_product2(A,B),A))),
% 0.13/0.53 inference(miniscoping,[status(thm)],[f16])).
% 0.13/0.53 fof(f129,plain,(
% 0.13/0.53 ![X0,X1]: (function(first_projection_as_func_of(X0,X1)))),
% 0.13/0.53 inference(cnf_transformation,[status(thm)],[f128])).
% 0.13/0.53 fof(f130,plain,(
% 0.13/0.53 ![X0,X1]: (quasi_total(first_projection_as_func_of(X0,X1),cartesian_product2(X0,X1),X0))),
% 0.13/0.53 inference(cnf_transformation,[status(thm)],[f128])).
% 0.13/0.53 fof(f131,plain,(
% 0.13/0.53 ![X0,X1]: (relation_of2_as_subset(first_projection_as_func_of(X0,X1),cartesian_product2(X0,X1),X0))),
% 0.13/0.53 inference(cnf_transformation,[status(thm)],[f128])).
% 0.13/0.53 fof(f143,plain,(
% 0.13/0.53 ![A,B]: (((~relation(A)|~function(A))|~finite(B))|finite(relation_image(A,B)))),
% 0.13/0.53 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.13/0.53 fof(f144,plain,(
% 0.13/0.53 ![X0,X1]: (~relation(X0)|~function(X0)|~finite(X1)|finite(relation_image(X0,X1)))),
% 0.13/0.53 inference(cnf_transformation,[status(thm)],[f143])).
% 0.13/0.53 fof(f145,plain,(
% 0.13/0.53 ![A,B]: ((~finite(A)|~finite(B))|finite(cartesian_product2(A,B)))),
% 0.13/0.53 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 0.13/0.53 fof(f146,plain,(
% 0.13/0.53 ![X0,X1]: (~finite(X0)|~finite(X1)|finite(cartesian_product2(X0,X1)))),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f145])).
% 0.13/0.54 fof(f295,plain,(
% 0.13/0.54 ![A,B,C,D]: (((~function(C)|~quasi_total(C,A,B))|~relation_of2(C,A,B))|function_image(A,B,C,D)=relation_image(C,D))),
% 0.13/0.54 inference(pre_NNF_transformation,[status(thm)],[f62])).
% 0.13/0.54 fof(f296,plain,(
% 0.13/0.54 ![A,B,C]: (((~function(C)|~quasi_total(C,A,B))|~relation_of2(C,A,B))|(![D]: function_image(A,B,C,D)=relation_image(C,D)))),
% 0.13/0.54 inference(miniscoping,[status(thm)],[f295])).
% 0.13/0.54 fof(f297,plain,(
% 0.13/0.54 ![X0,X1,X2,X3]: (~function(X0)|~quasi_total(X0,X1,X2)|~relation_of2(X0,X1,X2)|function_image(X1,X2,X0,X3)=relation_image(X0,X3))),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f296])).
% 0.13/0.54 fof(f298,plain,(
% 0.13/0.54 ![X0,X1]: (first_projection_as_func_of(X0,X1)=first_projection(X0,X1))),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f63])).
% 0.13/0.54 fof(f299,plain,(
% 0.13/0.54 ![A,B,C]: ((~relation_of2_as_subset(C,A,B)|relation_of2(C,A,B))&(relation_of2_as_subset(C,A,B)|~relation_of2(C,A,B)))),
% 0.13/0.54 inference(NNF_transformation,[status(thm)],[f64])).
% 0.13/0.54 fof(f300,plain,(
% 0.13/0.54 (![A,B,C]: (~relation_of2_as_subset(C,A,B)|relation_of2(C,A,B)))&(![A,B,C]: (relation_of2_as_subset(C,A,B)|~relation_of2(C,A,B)))),
% 0.13/0.54 inference(miniscoping,[status(thm)],[f299])).
% 0.13/0.54 fof(f301,plain,(
% 0.13/0.54 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|relation_of2(X0,X1,X2))),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f300])).
% 0.13/0.54 fof(f305,plain,(
% 0.13/0.54 ![A]: ((~relation(A)|~function(A))|function_image(cartesian_product2(relation_dom(A),relation_rng(A)),relation_dom(A),first_projection_as_func_of(relation_dom(A),relation_rng(A)),A)=relation_dom(A))),
% 0.13/0.54 inference(pre_NNF_transformation,[status(thm)],[f66])).
% 0.13/0.54 fof(f306,plain,(
% 0.13/0.54 ![X0]: (~relation(X0)|~function(X0)|function_image(cartesian_product2(relation_dom(X0),relation_rng(X0)),relation_dom(X0),first_projection_as_func_of(relation_dom(X0),relation_rng(X0)),X0)=relation_dom(X0))),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f305])).
% 0.13/0.54 fof(f307,plain,(
% 0.13/0.54 ![A,B]: ((~subset(A,B)|~finite(B))|finite(A))),
% 0.13/0.54 inference(pre_NNF_transformation,[status(thm)],[f67])).
% 0.13/0.54 fof(f308,plain,(
% 0.13/0.54 ![A]: ((![B]: (~subset(A,B)|~finite(B)))|finite(A))),
% 0.13/0.54 inference(miniscoping,[status(thm)],[f307])).
% 0.13/0.54 fof(f309,plain,(
% 0.13/0.54 ![X0,X1]: (~subset(X0,X1)|~finite(X1)|finite(X0))),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f308])).
% 0.13/0.54 fof(f317,plain,(
% 0.13/0.54 ![A]: (~relation(A)|subset(A,cartesian_product2(relation_dom(A),relation_rng(A))))),
% 0.13/0.54 inference(pre_NNF_transformation,[status(thm)],[f71])).
% 0.13/0.54 fof(f318,plain,(
% 0.13/0.54 ![X0]: (~relation(X0)|subset(X0,cartesian_product2(relation_dom(X0),relation_rng(X0))))),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f317])).
% 0.13/0.54 fof(f319,plain,(
% 0.13/0.54 ![A]: ((~relation(A)|~function(A))|(~finite(relation_dom(A))|finite(relation_rng(A))))),
% 0.13/0.54 inference(pre_NNF_transformation,[status(thm)],[f72])).
% 0.13/0.54 fof(f320,plain,(
% 0.13/0.54 ![X0]: (~relation(X0)|~function(X0)|~finite(relation_dom(X0))|finite(relation_rng(X0)))),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f319])).
% 0.13/0.54 fof(f321,plain,(
% 0.13/0.54 (?[A]: ((relation(A)&function(A))&(finite(relation_dom(A))<~>finite(A))))),
% 0.13/0.54 inference(pre_NNF_transformation,[status(thm)],[f74])).
% 0.13/0.54 fof(f322,plain,(
% 0.13/0.54 ?[A]: ((relation(A)&function(A))&((finite(relation_dom(A))|finite(A))&(~finite(relation_dom(A))|~finite(A))))),
% 0.13/0.54 inference(NNF_transformation,[status(thm)],[f321])).
% 0.13/0.54 fof(f323,plain,(
% 0.13/0.54 ((relation(sK29_skl)&function(sK29_skl))&((finite(relation_dom(sK29_skl))|finite(sK29_skl))&(~finite(relation_dom(sK29_skl))|~finite(sK29_skl))))),
% 0.13/0.54 inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(A,sK29_skl)],[f322])).
% 0.13/0.54 fof(f324,plain,(
% 0.13/0.54 relation(sK29_skl)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f323])).
% 0.13/0.54 fof(f325,plain,(
% 0.13/0.54 function(sK29_skl)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f323])).
% 0.13/0.54 fof(f326,plain,(
% 0.13/0.54 finite(relation_dom(sK29_skl))|finite(sK29_skl)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f323])).
% 0.13/0.54 fof(f327,plain,(
% 0.13/0.54 ~finite(relation_dom(sK29_skl))|~finite(sK29_skl)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f323])).
% 0.13/0.54 fof(f351,plain,(
% 0.13/0.54 ![X0,X1]: (relation(first_projection_as_func_of(X0,X1)))),
% 0.13/0.54 inference(backward_demodulation,[status(thm)],[f298,f126])).
% 0.13/0.54 fof(f1386,plain,(
% 0.13/0.54 ![X0,X1,X2]: (~function(first_projection_as_func_of(X0,X1))|~relation_of2(first_projection_as_func_of(X0,X1),cartesian_product2(X0,X1),X0)|function_image(cartesian_product2(X0,X1),X0,first_projection_as_func_of(X0,X1),X2)=relation_image(first_projection_as_func_of(X0,X1),X2))),
% 0.13/0.54 inference(resolution,[status(thm)],[f297,f130])).
% 0.13/0.54 fof(f1387,plain,(
% 0.13/0.54 ![X0,X1,X2]: (~relation_of2(first_projection_as_func_of(X0,X1),cartesian_product2(X0,X1),X0)|function_image(cartesian_product2(X0,X1),X0,first_projection_as_func_of(X0,X1),X2)=relation_image(first_projection_as_func_of(X0,X1),X2))),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f1386,f129])).
% 0.13/0.54 fof(f1411,plain,(
% 0.13/0.54 ~relation(sK29_skl)|function_image(cartesian_product2(relation_dom(sK29_skl),relation_rng(sK29_skl)),relation_dom(sK29_skl),first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)),sK29_skl)=relation_dom(sK29_skl)),
% 0.13/0.54 inference(resolution,[status(thm)],[f306,f325])).
% 0.13/0.54 fof(f1427,plain,(
% 0.13/0.54 function_image(cartesian_product2(relation_dom(sK29_skl),relation_rng(sK29_skl)),relation_dom(sK29_skl),first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)),sK29_skl)=relation_dom(sK29_skl)),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f1411,f324])).
% 0.13/0.54 fof(f1428,plain,(
% 0.13/0.54 ![X0]: (~relation(X0)|~finite(cartesian_product2(relation_dom(X0),relation_rng(X0)))|finite(X0))),
% 0.13/0.54 inference(resolution,[status(thm)],[f318,f309])).
% 0.13/0.54 fof(f1433,plain,(
% 0.13/0.54 ~relation(sK29_skl)|~function(sK29_skl)|finite(relation_rng(sK29_skl))|finite(sK29_skl)),
% 0.13/0.54 inference(resolution,[status(thm)],[f320,f326])).
% 0.13/0.54 fof(f1435,plain,(
% 0.13/0.54 ~function(sK29_skl)|finite(relation_rng(sK29_skl))|finite(sK29_skl)),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f1433,f324])).
% 0.13/0.54 fof(f1524,plain,(
% 0.13/0.54 ![X0,X1,X2]: (function_image(cartesian_product2(X0,X1),X0,first_projection_as_func_of(X0,X1),X2)=relation_image(first_projection_as_func_of(X0,X1),X2)|~relation_of2_as_subset(first_projection_as_func_of(X0,X1),cartesian_product2(X0,X1),X0))),
% 0.13/0.54 inference(resolution,[status(thm)],[f1387,f301])).
% 0.13/0.54 fof(f1526,plain,(
% 0.13/0.54 relation_image(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)),sK29_skl)=relation_dom(sK29_skl)),
% 0.13/0.54 inference(backward_demodulation,[status(thm)],[f1538,f1427])).
% 0.13/0.54 fof(f1538,plain,(
% 0.13/0.54 ![X0,X1,X2]: (function_image(cartesian_product2(X0,X1),X0,first_projection_as_func_of(X0,X1),X2)=relation_image(first_projection_as_func_of(X0,X1),X2))),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f1524,f131])).
% 0.13/0.54 fof(f1539,plain,(
% 0.13/0.54 ~relation(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)))|~function(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)))|~finite(sK29_skl)|finite(relation_dom(sK29_skl))),
% 0.13/0.54 inference(paramodulation,[status(thm)],[f1526,f144])).
% 0.13/0.54 fof(f1540,plain,(
% 0.13/0.54 ~function(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)))|~finite(sK29_skl)|finite(relation_dom(sK29_skl))),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f1539,f351])).
% 0.13/0.54 fof(f1586,plain,(
% 0.13/0.54 ![X0]: (~relation(X0)|finite(X0)|~finite(relation_dom(X0))|~finite(relation_rng(X0)))),
% 0.13/0.54 inference(resolution,[status(thm)],[f1428,f146])).
% 0.13/0.54 fof(f1891,plain,(
% 0.13/0.54 ~relation(sK29_skl)|finite(sK29_skl)|~finite(relation_rng(sK29_skl))|finite(sK29_skl)),
% 0.13/0.54 inference(resolution,[status(thm)],[f1586,f326])).
% 0.13/0.54 fof(f1893,plain,(
% 0.13/0.54 ~relation(sK29_skl)|finite(sK29_skl)|~finite(relation_rng(sK29_skl))),
% 0.13/0.54 inference(duplicate_literals_removal,[status(thm)],[f1891])).
% 0.13/0.54 fof(f1894,plain,(
% 0.13/0.54 ~function(sK29_skl)|finite(sK29_skl)),
% 0.13/0.54 inference(backward_subsumption_resolution,[status(thm)],[f1435,f1895])).
% 0.13/0.54 fof(f1895,plain,(
% 0.13/0.54 finite(sK29_skl)|~finite(relation_rng(sK29_skl))),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f1893,f324])).
% 0.13/0.54 fof(f1896,plain,(
% 0.13/0.54 ~function(first_projection_as_func_of(relation_dom(sK29_skl),relation_rng(sK29_skl)))|finite(relation_dom(sK29_skl))),
% 0.13/0.54 inference(backward_subsumption_resolution,[status(thm)],[f1540,f1898])).
% 0.13/0.55 fof(f1897,plain,(
% 0.13/0.55 ~finite(relation_dom(sK29_skl))),
% 0.13/0.55 inference(backward_subsumption_resolution,[status(thm)],[f327,f1898])).
% 0.13/0.55 fof(f1898,plain,(
% 0.13/0.55 finite(sK29_skl)),
% 0.13/0.55 inference(forward_subsumption_resolution,[status(thm)],[f1894,f325])).
% 0.13/0.55 fof(f1899,plain,(
% 0.13/0.55 finite(relation_dom(sK29_skl))),
% 0.13/0.55 inference(forward_subsumption_resolution,[status(thm)],[f1896,f129])).
% 0.13/0.55 fof(f1900,plain,(
% 0.13/0.55 $false),
% 0.13/0.55 inference(forward_subsumption_resolution,[status(thm)],[f1897,f1899])).
% 0.13/0.55 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.55 % Elapsed time: 0.173730 seconds
% 0.13/0.55 % CPU time: 1.057358 seconds
% 0.13/0.55 % Total memory used: 129.646 MB
% 0.13/0.55 % Net memory used: 127.834 MB
%------------------------------------------------------------------------------