%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET961+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:12:55 PM UTC 2026
% Result : Theorem 0.20s 0.79s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SET961+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.63 % Computer : n020.cluster.edu
% 0.16/0.63 % Model : x86_64 x86_64
% 0.16/0.63 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.63 % Memory : 8046.5625MB
% 0.16/0.63 % OS : Linux 6.8.0-71-generic
% 0.16/0.63 % CPULimit : 300
% 0.16/0.63 % WCLimit : 300
% 0.16/0.63 % DateTime : Mon Sep 21 05:46:33 UTC 2026
% 0.16/0.64 % CPUTime :
% 0.16/0.65 % Drodi V4.1.1
% 0.20/0.79 % Refutation found
% 0.20/0.79 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.20/0.79 % SZS output start CNFRefutation for theBenchmark
% 0.20/0.79 fof(f3,axiom,(
% 0.20/0.79 (! [A] :( A = empty_set<=> (! [B] : ~ in(B,A) )) )),
% 0.20/0.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.79 fof(f7,axiom,(
% 0.20/0.79 (! [A,B,C,D] :( in(ordered_pair(A,B),cartesian_product2(C,D))<=> ( in(A,C)& in(B,D) ) ) )),
% 0.20/0.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.79 fof(f10,conjecture,(
% 0.20/0.79 (! [A,B] :( cartesian_product2(A,B) = cartesian_product2(B,A)=> ( A = empty_set| B = empty_set| A = B ) ) )),
% 0.20/0.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.79 fof(f11,negated_conjecture,(
% 0.20/0.79 ~((! [A,B] :( cartesian_product2(A,B) = cartesian_product2(B,A)=> ( A = empty_set| B = empty_set| A = B ) ) ))),
% 0.20/0.79 inference(negated_conjecture,[status(cth)],[f10])).
% 0.20/0.79 fof(f12,axiom,(
% 0.20/0.79 (! [A,B] :( (! [C] :( in(C,A)<=> in(C,B) ))=> A = B ) )),
% 0.20/0.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.79 fof(f16,plain,(
% 0.20/0.79 ![A]: ((~A=empty_set|(![B]: ~in(B,A)))&(A=empty_set|(?[B]: in(B,A))))),
% 0.20/0.79 inference(NNF_transformation,[status(thm)],[f3])).
% 0.20/0.79 fof(f17,plain,(
% 0.20/0.79 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|(?[B]: in(B,A))))),
% 0.20/0.79 inference(miniscoping,[status(thm)],[f16])).
% 0.20/0.79 fof(f18,plain,(
% 0.20/0.79 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|in(sK0_skl(A),A)))),
% 0.20/0.79 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f17])).
% 0.20/0.79 fof(f20,plain,(
% 0.20/0.79 ![X0]: (X0=empty_set|in(sK0_skl(X0),X0))),
% 0.20/0.79 inference(cnf_transformation,[status(thm)],[f18])).
% 0.20/0.79 fof(f24,plain,(
% 0.20/0.79 ![A,B,C,D]: ((~in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D)))&(in(ordered_pair(A,B),cartesian_product2(C,D))|(~in(A,C)|~in(B,D))))),
% 0.20/0.79 inference(NNF_transformation,[status(thm)],[f7])).
% 0.20/0.79 fof(f25,plain,(
% 0.20/0.79 (![A,B,C,D]: (~in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D))))&(![A,B,C,D]: (in(ordered_pair(A,B),cartesian_product2(C,D))|(~in(A,C)|~in(B,D))))),
% 0.20/0.79 inference(miniscoping,[status(thm)],[f24])).
% 0.20/0.79 fof(f26,plain,(
% 0.20/0.79 ![X0,X1,X2,X3]: (~in(ordered_pair(X0,X1),cartesian_product2(X2,X3))|in(X0,X2))),
% 0.20/0.79 inference(cnf_transformation,[status(thm)],[f25])).
% 0.20/0.79 fof(f28,plain,(
% 0.20/0.79 ![X0,X1,X2,X3]: (in(ordered_pair(X0,X1),cartesian_product2(X2,X3))|~in(X0,X2)|~in(X1,X3))),
% 0.20/0.79 inference(cnf_transformation,[status(thm)],[f25])).
% 0.20/0.79 fof(f33,plain,(
% 0.20/0.79 (?[A,B]: (cartesian_product2(A,B)=cartesian_product2(B,A)&((~A=empty_set&~B=empty_set)&~A=B)))),
% 0.20/0.79 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.20/0.79 fof(f34,plain,(
% 0.20/0.79 (cartesian_product2(sK3_skl,sK4_skl)=cartesian_product2(sK4_skl,sK3_skl)&((~sK3_skl=empty_set&~sK4_skl=empty_set)&~sK3_skl=sK4_skl))),
% 0.20/0.79 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl]),skolemize(A,sK3_skl),skolemize(B,sK4_skl)],[f33])).
% 0.20/0.79 fof(f35,plain,(
% 0.20/0.79 cartesian_product2(sK3_skl,sK4_skl)=cartesian_product2(sK4_skl,sK3_skl)),
% 0.20/0.79 inference(cnf_transformation,[status(thm)],[f34])).
% 0.20/0.79 fof(f36,plain,(
% 0.20/0.79 ~sK3_skl=empty_set),
% 0.20/0.79 inference(cnf_transformation,[status(thm)],[f34])).
% 0.20/0.79 fof(f37,plain,(
% 0.20/0.79 ~sK4_skl=empty_set),
% 0.20/0.79 inference(cnf_transformation,[status(thm)],[f34])).
% 0.20/0.79 fof(f38,plain,(
% 0.20/0.79 ~sK3_skl=sK4_skl),
% 0.20/0.79 inference(cnf_transformation,[status(thm)],[f34])).
% 0.20/0.79 fof(f39,plain,(
% 0.20/0.79 ![A,B]: ((?[C]: (in(C,A)<~>in(C,B)))|A=B)),
% 0.20/0.79 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.20/0.79 fof(f40,plain,(
% 0.20/0.79 ![A,B]: ((?[C]: ((in(C,A)|in(C,B))&(~in(C,A)|~in(C,B))))|A=B)),
% 0.20/0.79 inference(NNF_transformation,[status(thm)],[f39])).
% 0.20/0.79 fof(f41,plain,(
% 0.20/0.79 ![A,B]: (((in(sK5_skl(B,A),A)|in(sK5_skl(B,A),B))&(~in(sK5_skl(B,A),A)|~in(sK5_skl(B,A),B)))|A=B)),
% 0.20/0.79 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(C,sK5_skl(B,A))],[f40])).
% 0.20/0.79 fof(f42,plain,(
% 0.20/0.79 ![X0,X1]: (in(sK5_skl(X0,X1),X1)|in(sK5_skl(X0,X1),X0)|X1=X0)),
% 0.20/0.79 inference(cnf_transformation,[status(thm)],[f41])).
% 0.20/0.79 fof(f43,plain,(
% 0.20/0.79 ![X0,X1]: (~in(sK5_skl(X0,X1),X1)|~in(sK5_skl(X0,X1),X0)|X1=X0)),
% 0.20/0.79 inference(cnf_transformation,[status(thm)],[f41])).
% 0.20/0.79 fof(f45,plain,(
% 0.20/0.79 ![X0,X1]: (~in(ordered_pair(X0,X1),cartesian_product2(sK3_skl,sK4_skl))|in(X0,sK4_skl))),
% 0.20/0.79 inference(paramodulation,[status(thm)],[f35,f26])).
% 0.20/0.79 fof(f53,plain,(
% 0.20/0.79 ![X0,X1,X2]: (X0=empty_set|in(ordered_pair(X1,sK0_skl(X0)),cartesian_product2(X2,X0))|~in(X1,X2))),
% 0.20/0.79 inference(resolution,[status(thm)],[f20,f28])).
% 0.20/0.79 fof(f80,plain,(
% 0.20/0.79 ![X0,X1,X2]: (X0=empty_set|in(ordered_pair(sK5_skl(X1,X2),sK0_skl(X0)),cartesian_product2(X1,X0))|in(sK5_skl(X1,X2),X2)|X2=X1)),
% 0.20/0.79 inference(resolution,[status(thm)],[f53,f42])).
% 0.20/0.79 fof(f118,definition,(
% 0.20/0.79 sQ2_spl <=> (sK4_skl=empty_set)),
% 0.20/0.79 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.20/0.79 fof(f119,plain,(
% 0.20/0.79 sK4_skl=empty_set|~sQ2_spl),
% 0.20/0.79 inference(component_clause,[status(thm)],[f118])).
% 0.20/0.79 fof(f121,definition,(
% 0.20/0.79 sQ3_spl <=> (sK3_skl=empty_set)),
% 0.20/0.79 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.20/0.79 fof(f122,plain,(
% 0.20/0.79 sK3_skl=empty_set|~sQ3_spl),
% 0.20/0.79 inference(component_clause,[status(thm)],[f121])).
% 0.20/0.79 fof(f144,plain,(
% 0.20/0.79 $false|~sQ2_spl),
% 0.20/0.79 inference(forward_subsumption_resolution,[status(thm)],[f119,f37])).
% 0.20/0.79 fof(f145,plain,(
% 0.20/0.79 ~sQ2_spl),
% 0.20/0.79 inference(contradiction_clause,[status(thm)],[f144])).
% 0.20/0.79 fof(f146,plain,(
% 0.20/0.79 $false|~sQ3_spl),
% 0.20/0.79 inference(forward_subsumption_resolution,[status(thm)],[f122,f36])).
% 0.20/0.79 fof(f147,plain,(
% 0.20/0.79 ~sQ3_spl),
% 0.20/0.79 inference(contradiction_clause,[status(thm)],[f146])).
% 0.20/0.79 fof(f167,plain,(
% 0.20/0.79 ![X0]: (sK4_skl=empty_set|in(sK5_skl(sK3_skl,X0),X0)|X0=sK3_skl|in(sK5_skl(sK3_skl,X0),sK4_skl))),
% 0.20/0.79 inference(resolution,[status(thm)],[f80,f45])).
% 0.20/0.79 fof(f187,definition,(
% 0.20/0.79 ![X0]: (sQ10_spl <=> (in(sK5_skl(sK3_skl,X0),X0)|X0=sK3_skl|in(sK5_skl(sK3_skl,X0),sK4_skl)))),
% 0.20/0.79 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.20/0.79 fof(f188,plain,(
% 0.20/0.79 ![X0]: (in(sK5_skl(sK3_skl,X0),X0)|X0=sK3_skl|in(sK5_skl(sK3_skl,X0),sK4_skl)|~sQ10_spl)),
% 0.20/0.79 inference(component_clause,[status(thm)],[f187])).
% 0.20/0.79 fof(f190,plain,(
% 0.20/0.79 sQ2_spl|sQ10_spl),
% 0.20/0.79 inference(split_clause,[status(thm)],[f167,f118,f187])).
% 0.20/0.79 fof(f271,plain,(
% 0.20/0.79 sK4_skl=sK3_skl|~in(sK5_skl(sK3_skl,sK4_skl),sK3_skl)|sK4_skl=sK3_skl|~sQ10_spl),
% 0.20/0.79 inference(resolution,[status(thm)],[f188,f43])).
% 0.20/0.79 fof(f287,definition,(
% 0.20/0.79 sQ14_spl <=> (sK4_skl=sK3_skl)),
% 0.20/0.79 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.20/0.79 fof(f288,plain,(
% 0.20/0.79 sK4_skl=sK3_skl|~sQ14_spl),
% 0.20/0.79 inference(component_clause,[status(thm)],[f287])).
% 0.20/0.79 fof(f290,definition,(
% 0.20/0.79 sQ15_spl <=> (in(sK5_skl(sK3_skl,sK4_skl),sK3_skl))),
% 0.20/0.79 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.20/0.79 fof(f292,plain,(
% 0.20/0.79 ~in(sK5_skl(sK3_skl,sK4_skl),sK3_skl)|sQ15_spl),
% 0.20/0.79 inference(component_clause,[status(thm)],[f290])).
% 0.20/0.79 fof(f293,plain,(
% 0.20/0.79 sQ14_spl|~sQ15_spl|~sQ10_spl),
% 0.20/0.79 inference(split_clause,[status(thm)],[f271,f287,f290,f187])).
% 0.20/0.79 fof(f315,definition,(
% 0.20/0.79 sQ21_spl <=> (in(sK5_skl(sK3_skl,sK4_skl),sK4_skl))),
% 0.20/0.79 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.20/0.79 fof(f316,plain,(
% 0.20/0.79 in(sK5_skl(sK3_skl,sK4_skl),sK4_skl)|~sQ21_spl),
% 0.20/0.79 inference(component_clause,[status(thm)],[f315])).
% 0.20/0.79 fof(f319,plain,(
% 0.20/0.79 $false|~sQ14_spl),
% 0.20/0.79 inference(forward_subsumption_resolution,[status(thm)],[f288,f38])).
% 0.20/0.79 fof(f320,plain,(
% 0.20/0.79 ~sQ14_spl),
% 0.20/0.79 inference(contradiction_clause,[status(thm)],[f319])).
% 0.20/0.79 fof(f325,plain,(
% 0.20/0.79 in(sK5_skl(sK3_skl,sK4_skl),sK4_skl)|sK4_skl=sK3_skl|sQ15_spl),
% 0.20/0.79 inference(resolution,[status(thm)],[f292,f42])).
% 0.20/0.79 fof(f326,plain,(
% 0.20/0.79 sQ21_spl|sQ14_spl|sQ15_spl),
% 0.20/0.79 inference(split_clause,[status(thm)],[f325,f315,f287,f290])).
% 0.20/0.79 fof(f335,plain,(
% 0.20/0.79 ![X0]: (sK3_skl=empty_set|in(ordered_pair(X0,sK0_skl(sK3_skl)),cartesian_product2(sK3_skl,sK4_skl))|~in(X0,sK4_skl))),
% 0.20/0.79 inference(paramodulation,[status(thm)],[f35,f53])).
% 0.20/0.79 fof(f352,definition,(
% 0.20/0.79 ![X0]: (sQ26_spl <=> (in(ordered_pair(X0,sK0_skl(sK3_skl)),cartesian_product2(sK3_skl,sK4_skl))|~in(X0,sK4_skl)))),
% 0.20/0.79 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.20/0.79 fof(f353,plain,(
% 0.20/0.79 ![X0]: (in(ordered_pair(X0,sK0_skl(sK3_skl)),cartesian_product2(sK3_skl,sK4_skl))|~in(X0,sK4_skl)|~sQ26_spl)),
% 0.20/0.79 inference(component_clause,[status(thm)],[f352])).
% 0.20/0.79 fof(f355,plain,(
% 0.20/0.79 sQ3_spl|sQ26_spl),
% 0.20/0.79 inference(split_clause,[status(thm)],[f335,f121,f352])).
% 0.20/0.79 fof(f655,plain,(
% 0.20/0.79 ![X0]: (~in(X0,sK4_skl)|in(X0,sK3_skl)|~sQ26_spl)),
% 0.20/0.79 inference(resolution,[status(thm)],[f353,f26])).
% 0.20/0.79 fof(f668,plain,(
% 0.20/0.79 in(sK5_skl(sK3_skl,sK4_skl),sK3_skl)|~sQ26_spl|~sQ21_spl),
% 0.20/0.79 inference(resolution,[status(thm)],[f655,f316])).
% 0.20/0.79 fof(f682,plain,(
% 0.20/0.79 $false|sQ15_spl|~sQ26_spl|~sQ21_spl),
% 0.20/0.79 inference(forward_subsumption_resolution,[status(thm)],[f668,f292])).
% 0.20/0.79 fof(f683,plain,(
% 0.20/0.79 sQ15_spl|~sQ26_spl|~sQ21_spl),
% 0.20/0.79 inference(contradiction_clause,[status(thm)],[f682])).
% 0.20/0.79 fof(f684,plain,(
% 0.20/0.79 $false),
% 0.20/0.79 inference(sat_refutation,[status(thm)],[f145,f147,f190,f293,f320,f326,f355,f683])).
% 0.20/0.79 % SZS output end CNFRefutation for theBenchmark.p
% 0.20/0.82 % Elapsed time: 0.169293 seconds
% 0.20/0.82 % CPU time: 0.912202 seconds
% 0.20/0.82 % Total memory used: 108.071 MB
% 0.20/0.82 % Net memory used: 106.044 MB
%------------------------------------------------------------------------------