%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU263+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 : n002.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:22:10 PM UTC 2026
% Result : Theorem 0.14s 5.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU263+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/5.37 % Computer : n002.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Mon Sep 21 06:07:26 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.38 % Drodi V4.1.1
% 0.14/5.41 % Refutation found
% 0.14/5.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/5.41 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.41 fof(f1,axiom,(
% 0.14/5.41 (! [A,B,C] :( element(C,powerset(cartesian_product2(A,B)))=> relation(C) ) )),
% 0.14/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f2,axiom,(
% 0.14/5.41 (! [A,B,C] :( relation_of2(C,A,B)<=> subset(C,cartesian_product2(A,B)) ) )),
% 0.14/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f9,axiom,(
% 0.14/5.41 (! [A,B,C] :( relation_of2_as_subset(C,A,B)=> element(C,powerset(cartesian_product2(A,B))) ) )),
% 0.14/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f13,axiom,(
% 0.14/5.41 (! [A,B,C] :( relation_of2_as_subset(C,A,B)<=> relation_of2(C,A,B) ) )),
% 0.14/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f15,axiom,(
% 0.14/5.41 (! [A,B,C,D] :( ( subset(A,B)& subset(C,D) )=> subset(cartesian_product2(A,C),cartesian_product2(B,D)) ) )),
% 0.14/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f16,axiom,(
% 0.14/5.41 (! [A,B,C] :( relation_of2_as_subset(C,A,B)=> ( subset(relation_dom(C),A)& subset(relation_rng(C),B) ) ) )),
% 0.14/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f17,conjecture,(
% 0.14/5.41 (! [A,B,C,D] :( relation_of2_as_subset(D,C,A)=> ( subset(relation_rng(D),B)=> relation_of2_as_subset(D,C,B) ) ) )),
% 0.14/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f18,negated_conjecture,(
% 0.14/5.41 ~((! [A,B,C,D] :( relation_of2_as_subset(D,C,A)=> ( subset(relation_rng(D),B)=> relation_of2_as_subset(D,C,B) ) ) ))),
% 0.14/5.41 inference(negated_conjecture,[status(cth)],[f17])).
% 0.14/5.41 fof(f19,axiom,(
% 0.14/5.41 (! [A,B,C] :( ( subset(A,B)& subset(B,C) )=> subset(A,C) ) )),
% 0.14/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f20,axiom,(
% 0.14/5.41 (! [A] :( relation(A)=> subset(A,cartesian_product2(relation_dom(A),relation_rng(A))) ) )),
% 0.14/5.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.41 fof(f22,plain,(
% 0.14/5.41 ![A,B,C]: (~element(C,powerset(cartesian_product2(A,B)))|relation(C))),
% 0.14/5.41 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.14/5.41 fof(f23,plain,(
% 0.14/5.41 ![C]: ((![A,B]: ~element(C,powerset(cartesian_product2(A,B))))|relation(C))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f22])).
% 0.14/5.41 fof(f24,plain,(
% 0.14/5.41 ![X0,X1,X2]: (~element(X0,powerset(cartesian_product2(X1,X2)))|relation(X0))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f23])).
% 0.14/5.41 fof(f25,plain,(
% 0.14/5.41 ![A,B,C]: ((~relation_of2(C,A,B)|subset(C,cartesian_product2(A,B)))&(relation_of2(C,A,B)|~subset(C,cartesian_product2(A,B))))),
% 0.14/5.41 inference(NNF_transformation,[status(thm)],[f2])).
% 0.14/5.41 fof(f26,plain,(
% 0.14/5.41 (![A,B,C]: (~relation_of2(C,A,B)|subset(C,cartesian_product2(A,B))))&(![A,B,C]: (relation_of2(C,A,B)|~subset(C,cartesian_product2(A,B))))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f25])).
% 0.14/5.41 fof(f28,plain,(
% 0.14/5.41 ![X0,X1,X2]: (relation_of2(X0,X1,X2)|~subset(X0,cartesian_product2(X1,X2)))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f26])).
% 0.14/5.41 fof(f29,plain,(
% 0.14/5.41 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|element(C,powerset(cartesian_product2(A,B))))),
% 0.14/5.41 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.14/5.41 fof(f30,plain,(
% 0.14/5.41 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|element(X0,powerset(cartesian_product2(X1,X2))))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f29])).
% 0.14/5.41 fof(f37,plain,(
% 0.14/5.41 ![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.14/5.41 inference(NNF_transformation,[status(thm)],[f13])).
% 0.14/5.41 fof(f38,plain,(
% 0.14/5.41 (![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.14/5.41 inference(miniscoping,[status(thm)],[f37])).
% 0.14/5.41 fof(f40,plain,(
% 0.14/5.41 ![X0,X1,X2]: (relation_of2_as_subset(X0,X1,X2)|~relation_of2(X0,X1,X2))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f38])).
% 0.14/5.41 fof(f43,plain,(
% 0.14/5.41 ![A,B,C,D]: ((~subset(A,B)|~subset(C,D))|subset(cartesian_product2(A,C),cartesian_product2(B,D)))),
% 0.14/5.41 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.14/5.41 fof(f44,plain,(
% 0.14/5.41 ![X0,X1,X2,X3]: (~subset(X0,X1)|~subset(X2,X3)|subset(cartesian_product2(X0,X2),cartesian_product2(X1,X3)))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f43])).
% 0.14/5.41 fof(f45,plain,(
% 0.14/5.41 ![A,B,C]: (~relation_of2_as_subset(C,A,B)|(subset(relation_dom(C),A)&subset(relation_rng(C),B)))),
% 0.14/5.41 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.14/5.41 fof(f46,plain,(
% 0.14/5.41 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|subset(relation_dom(X0),X1))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/5.41 fof(f48,plain,(
% 0.14/5.41 (?[A,B,C,D]: (relation_of2_as_subset(D,C,A)&(subset(relation_rng(D),B)&~relation_of2_as_subset(D,C,B))))),
% 0.14/5.41 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.14/5.41 fof(f49,plain,(
% 0.14/5.41 ?[C,D]: ((?[A]: relation_of2_as_subset(D,C,A))&(?[B]: (subset(relation_rng(D),B)&~relation_of2_as_subset(D,C,B))))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f48])).
% 0.14/5.41 fof(f50,plain,(
% 0.14/5.41 (relation_of2_as_subset(sK4_skl,sK3_skl,sK5_skl)&(subset(relation_rng(sK4_skl),sK6_skl)&~relation_of2_as_subset(sK4_skl,sK3_skl,sK6_skl)))),
% 0.14/5.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl,sK6_skl]),skolemize(C,sK3_skl),skolemize(D,sK4_skl),skolemize(A,sK5_skl),skolemize(B,sK6_skl)],[f49])).
% 0.14/5.41 fof(f51,plain,(
% 0.14/5.41 relation_of2_as_subset(sK4_skl,sK3_skl,sK5_skl)),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f50])).
% 0.14/5.41 fof(f52,plain,(
% 0.14/5.41 subset(relation_rng(sK4_skl),sK6_skl)),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f50])).
% 0.14/5.41 fof(f53,plain,(
% 0.14/5.41 ~relation_of2_as_subset(sK4_skl,sK3_skl,sK6_skl)),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f50])).
% 0.14/5.41 fof(f54,plain,(
% 0.14/5.41 ![A,B,C]: ((~subset(A,B)|~subset(B,C))|subset(A,C))),
% 0.14/5.41 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.14/5.41 fof(f55,plain,(
% 0.14/5.41 ![A,C]: ((![B]: (~subset(A,B)|~subset(B,C)))|subset(A,C))),
% 0.14/5.41 inference(miniscoping,[status(thm)],[f54])).
% 0.14/5.41 fof(f56,plain,(
% 0.14/5.41 ![X0,X1,X2]: (~subset(X0,X1)|~subset(X1,X2)|subset(X0,X2))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f55])).
% 0.14/5.41 fof(f57,plain,(
% 0.14/5.41 ![A]: (~relation(A)|subset(A,cartesian_product2(relation_dom(A),relation_rng(A))))),
% 0.14/5.41 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.14/5.41 fof(f58,plain,(
% 0.14/5.41 ![X0]: (~relation(X0)|subset(X0,cartesian_product2(relation_dom(X0),relation_rng(X0))))),
% 0.14/5.41 inference(cnf_transformation,[status(thm)],[f57])).
% 0.14/5.41 fof(f65,plain,(
% 0.14/5.41 ![X0,X1,X2,X3]: (relation_of2(X0,X1,X2)|~subset(X0,X3)|~subset(X3,cartesian_product2(X1,X2)))),
% 0.14/5.41 inference(resolution,[status(thm)],[f28,f56])).
% 0.14/5.41 fof(f68,plain,(
% 0.14/5.41 ![X0,X1,X2]: (~relation_of2_as_subset(X0,X1,X2)|relation(X0))),
% 0.14/5.41 inference(resolution,[status(thm)],[f30,f24])).
% 0.14/5.41 fof(f76,plain,(
% 0.14/5.41 ![X0,X1,X2,X3]: (~subset(X0,X1)|~subset(X1,cartesian_product2(X2,X3))|relation_of2_as_subset(X0,X2,X3))),
% 0.14/5.41 inference(resolution,[status(thm)],[f65,f40])).
% 0.14/5.41 fof(f81,plain,(
% 0.14/5.41 ![X0]: (~subset(sK4_skl,X0)|~subset(X0,cartesian_product2(sK3_skl,sK6_skl)))),
% 0.14/5.41 inference(resolution,[status(thm)],[f76,f53])).
% 0.14/5.41 fof(f90,plain,(
% 0.14/5.41 relation(sK4_skl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f68,f51])).
% 0.14/5.41 fof(f92,plain,(
% 0.14/5.41 subset(sK4_skl,cartesian_product2(relation_dom(sK4_skl),relation_rng(sK4_skl)))),
% 0.14/5.41 inference(resolution,[status(thm)],[f90,f58])).
% 0.14/5.41 fof(f107,plain,(
% 0.14/5.41 ~subset(cartesian_product2(relation_dom(sK4_skl),relation_rng(sK4_skl)),cartesian_product2(sK3_skl,sK6_skl))),
% 0.14/5.41 inference(resolution,[status(thm)],[f92,f81])).
% 0.14/5.41 fof(f167,plain,(
% 0.14/5.41 ~subset(relation_dom(sK4_skl),sK3_skl)|~subset(relation_rng(sK4_skl),sK6_skl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f107,f44])).
% 0.14/5.41 fof(f171,definition,(
% 0.14/5.41 sQ0_spl <=> (subset(relation_dom(sK4_skl),sK3_skl))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f173,plain,(
% 0.14/5.41 ~subset(relation_dom(sK4_skl),sK3_skl)|sQ0_spl),
% 0.14/5.41 inference(component_clause,[status(thm)],[f171])).
% 0.14/5.41 fof(f174,definition,(
% 0.14/5.41 sQ1_spl <=> (subset(relation_rng(sK4_skl),sK6_skl))),
% 0.14/5.41 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/5.41 fof(f176,plain,(
% 0.14/5.41 ~subset(relation_rng(sK4_skl),sK6_skl)|sQ1_spl),
% 0.14/5.41 inference(component_clause,[status(thm)],[f174])).
% 0.14/5.41 fof(f177,plain,(
% 0.14/5.41 ~sQ0_spl|~sQ1_spl),
% 0.14/5.41 inference(split_clause,[status(thm)],[f167,f171,f174])).
% 0.14/5.41 fof(f179,plain,(
% 0.14/5.41 ![X0]: (~relation_of2_as_subset(sK4_skl,sK3_skl,X0)|sQ0_spl)),
% 0.14/5.41 inference(resolution,[status(thm)],[f173,f46])).
% 0.14/5.41 fof(f191,plain,(
% 0.14/5.42 $false|sQ0_spl),
% 0.14/5.42 inference(backward_subsumption_resolution,[status(thm)],[f51,f179])).
% 0.14/5.42 fof(f193,plain,(
% 0.14/5.42 sQ0_spl),
% 0.14/5.42 inference(contradiction_clause,[status(thm)],[f191])).
% 0.14/5.42 fof(f194,plain,(
% 0.14/5.42 $false|sQ1_spl),
% 0.14/5.42 inference(forward_subsumption_resolution,[status(thm)],[f176,f52])).
% 0.14/5.42 fof(f195,plain,(
% 0.14/5.42 sQ1_spl),
% 0.14/5.42 inference(contradiction_clause,[status(thm)],[f194])).
% 0.14/5.42 fof(f196,plain,(
% 0.14/5.42 $false),
% 0.14/5.42 inference(sat_refutation,[status(thm)],[f177,f193,f195])).
% 0.14/5.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.43 % Elapsed time: 0.045753 seconds
% 0.14/5.43 % CPU time: 0.146862 seconds
% 0.14/5.43 % Total memory used: 41.442 MB
% 0.14/5.43 % Net memory used: 41.128 MB
%------------------------------------------------------------------------------