%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU104+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 : n019.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:41 PM UTC 2026
% Result : Theorem 0.12s 0.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU104+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.08/0.35 % Computer : n019.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 05:51:04 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.12/0.51 % Refutation found
% 0.12/0.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.51 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.51 fof(f6,axiom,(
% 0.12/0.51 (! [A,B] : set_union2(A,B) = set_union2(B,A) )),
% 0.12/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51 fof(f18,axiom,(
% 0.12/0.51 (? [A] :( ~ empty(A)& finite(A) ) )),
% 0.12/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51 fof(f21,axiom,(
% 0.12/0.51 (? [A] : empty(A) )),
% 0.12/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51 fof(f28,axiom,(
% 0.12/0.51 (! [A] :( preboolean(A)<=> (! [B,C] :( ( in(B,A)& in(C,A) )=> ( in(set_union2(B,C),A)& in(set_difference(B,C),A) ) ) )) )),
% 0.12/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51 fof(f29,conjecture,(
% 0.12/0.51 (! [A] :( ~ empty(A)=> ( (! [B] :( element(B,A)=> (! [C] :( element(C,A)=> ( in(symmetric_difference(B,C),A)& in(set_difference(B,C),A) ) ) )))=> preboolean(A) ) ) )),
% 0.12/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51 fof(f30,negated_conjecture,(
% 0.12/0.51 ~((! [A] :( ~ empty(A)=> ( (! [B] :( element(B,A)=> (! [C] :( element(C,A)=> ( in(symmetric_difference(B,C),A)& in(set_difference(B,C),A) ) ) )))=> preboolean(A) ) ) ))),
% 0.12/0.51 inference(negated_conjecture,[status(cth)],[f29])).
% 0.12/0.51 fof(f32,axiom,(
% 0.12/0.51 (! [A,B] :( in(A,B)=> element(A,B) ) )),
% 0.12/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51 fof(f43,axiom,(
% 0.12/0.51 (! [A,B] : set_union2(A,B) = symmetric_difference(A,set_difference(B,A)) )),
% 0.12/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.51 fof(f55,plain,(
% 0.12/0.51 ![X0,X1]: (set_union2(X0,X1)=set_union2(X1,X0))),
% 0.12/0.51 inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/0.51 fof(f77,plain,(
% 0.12/0.51 (~empty(sK1_skl)&finite(sK1_skl))),
% 0.12/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(A,sK1_skl)],[f18])).
% 0.12/0.51 fof(f78,plain,(
% 0.12/0.51 ~empty(sK1_skl)),
% 0.12/0.51 inference(cnf_transformation,[status(thm)],[f77])).
% 0.12/0.51 fof(f90,plain,(
% 0.12/0.51 empty(sK4_skl)),
% 0.12/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f21])).
% 0.12/0.51 fof(f91,plain,(
% 0.12/0.51 empty(sK4_skl)),
% 0.12/0.51 inference(cnf_transformation,[status(thm)],[f90])).
% 0.12/0.51 fof(f120,plain,(
% 0.12/0.51 ![A]: (preboolean(A)<=>(![B,C]: ((~in(B,A)|~in(C,A))|(in(set_union2(B,C),A)&in(set_difference(B,C),A)))))),
% 0.12/0.51 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.12/0.51 fof(f121,plain,(
% 0.12/0.51 ![A]: ((~preboolean(A)|(![B,C]: ((~in(B,A)|~in(C,A))|(in(set_union2(B,C),A)&in(set_difference(B,C),A)))))&(preboolean(A)|(?[B,C]: ((in(B,A)&in(C,A))&(~in(set_union2(B,C),A)|~in(set_difference(B,C),A))))))),
% 0.12/0.51 inference(NNF_transformation,[status(thm)],[f120])).
% 0.12/0.51 fof(f122,plain,(
% 0.12/0.51 (![A]: (~preboolean(A)|(![B,C]: ((~in(B,A)|~in(C,A))|(in(set_union2(B,C),A)&in(set_difference(B,C),A))))))&(![A]: (preboolean(A)|(?[B,C]: ((in(B,A)&in(C,A))&(~in(set_union2(B,C),A)|~in(set_difference(B,C),A))))))),
% 0.12/0.51 inference(miniscoping,[status(thm)],[f121])).
% 0.12/0.51 fof(f123,plain,(
% 0.12/0.51 (![A]: (~preboolean(A)|(![B,C]: ((~in(B,A)|~in(C,A))|(in(set_union2(B,C),A)&in(set_difference(B,C),A))))))&(![A]: (preboolean(A)|((in(sK10_skl(A),A)&in(sK11_skl(A),A))&(~in(set_union2(sK10_skl(A),sK11_skl(A)),A)|~in(set_difference(sK10_skl(A),sK11_skl(A)),A)))))),
% 0.12/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl]),skolemize(B,sK10_skl(A)),skolemize(C,sK11_skl(A))],[f122])).
% 0.12/0.51 fof(f126,plain,(
% 0.12/0.51 ![X0]: (preboolean(X0)|in(sK10_skl(X0),X0))),
% 0.12/0.51 inference(cnf_transformation,[status(thm)],[f123])).
% 0.12/0.51 fof(f127,plain,(
% 0.12/0.51 ![X0]: (preboolean(X0)|in(sK11_skl(X0),X0))),
% 0.12/0.51 inference(cnf_transformation,[status(thm)],[f123])).
% 0.12/0.51 fof(f128,plain,(
% 0.12/0.51 ![X0]: (preboolean(X0)|~in(set_union2(sK10_skl(X0),sK11_skl(X0)),X0)|~in(set_difference(sK10_skl(X0),sK11_skl(X0)),X0))),
% 0.12/0.51 inference(cnf_transformation,[status(thm)],[f123])).
% 0.12/0.51 fof(f129,plain,(
% 0.12/0.51 (?[A]: (~empty(A)&((![B]: (~element(B,A)|(![C]: (~element(C,A)|(in(symmetric_difference(B,C),A)&in(set_difference(B,C),A))))))&~preboolean(A))))),
% 0.12/0.51 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.12/0.51 fof(f130,plain,(
% 0.12/0.51 (~empty(sK12_skl)&((![B]: (~element(B,sK12_skl)|(![C]: (~element(C,sK12_skl)|(in(symmetric_difference(B,C),sK12_skl)&in(set_difference(B,C),sK12_skl))))))&~preboolean(sK12_skl)))),
% 0.12/0.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f129])).
% 0.12/0.51 fof(f132,plain,(
% 0.12/0.51 ![X0,X1]: (~element(X0,sK12_skl)|~element(X1,sK12_skl)|in(symmetric_difference(X0,X1),sK12_skl))),
% 0.12/0.51 inference(cnf_transformation,[status(thm)],[f130])).
% 0.12/0.51 fof(f133,plain,(
% 0.12/0.51 ![X0,X1]: (~element(X0,sK12_skl)|~element(X1,sK12_skl)|in(set_difference(X0,X1),sK12_skl))),
% 0.12/0.51 inference(cnf_transformation,[status(thm)],[f130])).
% 0.12/0.51 fof(f134,plain,(
% 0.12/0.51 ~preboolean(sK12_skl)),
% 0.12/0.51 inference(cnf_transformation,[status(thm)],[f130])).
% 0.12/0.51 fof(f136,plain,(
% 0.12/0.51 ![A,B]: (~in(A,B)|element(A,B))),
% 0.12/0.51 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 0.12/0.51 fof(f137,plain,(
% 0.12/0.51 ![X0,X1]: (~in(X0,X1)|element(X0,X1))),
% 0.12/0.51 inference(cnf_transformation,[status(thm)],[f136])).
% 0.12/0.51 fof(f161,plain,(
% 0.12/0.51 ![X0,X1]: (set_union2(X0,X1)=symmetric_difference(X0,set_difference(X1,X0)))),
% 0.12/0.51 inference(cnf_transformation,[status(thm)],[f43])).
% 0.12/0.51 fof(f314,definition,(
% 0.12/0.51 sQ2_spl <=> (preboolean(sK12_skl))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f315,plain,(
% 0.12/0.51 preboolean(sK12_skl)|~sQ2_spl),
% 0.12/0.51 inference(component_clause,[status(thm)],[f314])).
% 0.12/0.51 fof(f437,definition,(
% 0.12/0.51 ![X0]: (sQ14_spl <=> (~empty(X0)))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f438,plain,(
% 0.12/0.51 ![X0]: (~empty(X0)|~sQ14_spl)),
% 0.12/0.51 inference(component_clause,[status(thm)],[f437])).
% 0.12/0.51 fof(f451,plain,(
% 0.12/0.51 ![X0]: (preboolean(X0)|element(sK10_skl(X0),X0))),
% 0.12/0.51 inference(resolution,[status(thm)],[f126,f137])).
% 0.12/0.51 fof(f532,plain,(
% 0.12/0.51 ![X0]: (preboolean(sK12_skl)|~element(X0,sK12_skl)|in(set_difference(sK10_skl(sK12_skl),X0),sK12_skl))),
% 0.12/0.51 inference(resolution,[status(thm)],[f451,f133])).
% 0.12/0.51 fof(f551,definition,(
% 0.12/0.51 ![X0]: (sQ25_spl <=> (~element(X0,sK12_skl)|in(set_difference(sK10_skl(sK12_skl),X0),sK12_skl)))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f552,plain,(
% 0.12/0.51 ![X0]: (~element(X0,sK12_skl)|in(set_difference(sK10_skl(sK12_skl),X0),sK12_skl)|~sQ25_spl)),
% 0.12/0.51 inference(component_clause,[status(thm)],[f551])).
% 0.12/0.51 fof(f554,plain,(
% 0.12/0.51 sQ2_spl|sQ25_spl),
% 0.12/0.51 inference(split_clause,[status(thm)],[f532,f314,f551])).
% 0.12/0.51 fof(f559,plain,(
% 0.12/0.51 $false|~sQ2_spl),
% 0.12/0.51 inference(forward_subsumption_resolution,[status(thm)],[f315,f134])).
% 0.12/0.51 fof(f560,plain,(
% 0.12/0.51 ~sQ2_spl),
% 0.12/0.51 inference(contradiction_clause,[status(thm)],[f559])).
% 0.12/0.51 fof(f584,plain,(
% 0.12/0.51 ![X0]: (preboolean(X0)|element(sK11_skl(X0),X0))),
% 0.12/0.51 inference(resolution,[status(thm)],[f127,f137])).
% 0.12/0.51 fof(f592,plain,(
% 0.12/0.51 ![X0]: (preboolean(sK12_skl)|~element(X0,sK12_skl)|in(symmetric_difference(sK11_skl(sK12_skl),X0),sK12_skl))),
% 0.12/0.51 inference(resolution,[status(thm)],[f584,f132])).
% 0.12/0.51 fof(f614,definition,(
% 0.12/0.51 ![X0]: (sQ32_spl <=> (~element(X0,sK12_skl)|in(symmetric_difference(sK11_skl(sK12_skl),X0),sK12_skl)))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f615,plain,(
% 0.12/0.51 ![X0]: (~element(X0,sK12_skl)|in(symmetric_difference(sK11_skl(sK12_skl),X0),sK12_skl)|~sQ32_spl)),
% 0.12/0.51 inference(component_clause,[status(thm)],[f614])).
% 0.12/0.51 fof(f617,plain,(
% 0.12/0.51 sQ2_spl|sQ32_spl),
% 0.12/0.51 inference(split_clause,[status(thm)],[f592,f314,f614])).
% 0.12/0.51 fof(f740,plain,(
% 0.12/0.51 in(set_difference(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)|preboolean(sK12_skl)|~sQ25_spl),
% 0.12/0.51 inference(resolution,[status(thm)],[f552,f584])).
% 0.12/0.51 fof(f746,definition,(
% 0.12/0.51 sQ42_spl <=> (in(set_difference(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f747,plain,(
% 0.12/0.51 in(set_difference(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)|~sQ42_spl),
% 0.12/0.51 inference(component_clause,[status(thm)],[f746])).
% 0.12/0.51 fof(f749,plain,(
% 0.12/0.51 sQ42_spl|sQ2_spl|~sQ25_spl),
% 0.12/0.51 inference(split_clause,[status(thm)],[f740,f746,f314,f551])).
% 0.12/0.51 fof(f888,definition,(
% 0.12/0.51 sQ52_spl <=> (empty(sK1_skl))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f889,plain,(
% 0.12/0.51 empty(sK1_skl)|~sQ52_spl),
% 0.12/0.51 inference(component_clause,[status(thm)],[f888])).
% 0.12/0.51 fof(f910,plain,(
% 0.12/0.51 $false|~sQ52_spl),
% 0.12/0.51 inference(forward_subsumption_resolution,[status(thm)],[f889,f78])).
% 0.12/0.51 fof(f911,plain,(
% 0.12/0.51 ~sQ52_spl),
% 0.12/0.51 inference(contradiction_clause,[status(thm)],[f910])).
% 0.12/0.51 fof(f1105,plain,(
% 0.12/0.51 $false|~sQ14_spl),
% 0.12/0.51 inference(backward_subsumption_resolution,[status(thm)],[f91,f438])).
% 0.12/0.51 fof(f1232,plain,(
% 0.12/0.51 preboolean(sK12_skl)|~in(set_union2(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)|~sQ42_spl),
% 0.12/0.51 inference(resolution,[status(thm)],[f747,f128])).
% 0.12/0.51 fof(f1236,plain,(
% 0.12/0.51 element(set_difference(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)|~sQ42_spl),
% 0.12/0.51 inference(resolution,[status(thm)],[f747,f137])).
% 0.12/0.51 fof(f1238,definition,(
% 0.12/0.51 sQ66_spl <=> (in(set_union2(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl))),
% 0.12/0.51 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.12/0.51 fof(f1240,plain,(
% 0.12/0.51 ~in(set_union2(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)|sQ66_spl),
% 0.12/0.51 inference(component_clause,[status(thm)],[f1238])).
% 0.12/0.51 fof(f1241,plain,(
% 0.12/0.51 sQ2_spl|~sQ66_spl|~sQ42_spl),
% 0.12/0.51 inference(split_clause,[status(thm)],[f1232,f314,f1238,f746])).
% 0.12/0.51 fof(f1447,plain,(
% 0.12/0.51 ~sQ14_spl),
% 0.12/0.51 inference(contradiction_clause,[status(thm)],[f1105])).
% 0.12/0.51 fof(f1544,plain,(
% 0.12/0.51 in(symmetric_difference(sK11_skl(sK12_skl),set_difference(sK10_skl(sK12_skl),sK11_skl(sK12_skl))),sK12_skl)|~sQ32_spl|~sQ42_spl),
% 0.12/0.51 inference(resolution,[status(thm)],[f615,f1236])).
% 0.12/0.51 fof(f1560,plain,(
% 0.12/0.51 in(set_union2(sK11_skl(sK12_skl),sK10_skl(sK12_skl)),sK12_skl)|~sQ32_spl|~sQ42_spl),
% 0.12/0.51 inference(forward_demodulation,[status(thm)],[f161,f1544])).
% 0.12/0.51 fof(f1561,plain,(
% 0.12/0.51 in(set_union2(sK10_skl(sK12_skl),sK11_skl(sK12_skl)),sK12_skl)|~sQ32_spl|~sQ42_spl),
% 0.12/0.51 inference(forward_demodulation,[status(thm)],[f55,f1560])).
% 0.12/0.51 fof(f1562,plain,(
% 0.12/0.51 $false|sQ66_spl|~sQ32_spl|~sQ42_spl),
% 0.12/0.51 inference(forward_subsumption_resolution,[status(thm)],[f1561,f1240])).
% 0.12/0.51 fof(f1563,plain,(
% 0.12/0.51 sQ66_spl|~sQ32_spl|~sQ42_spl),
% 0.12/0.51 inference(contradiction_clause,[status(thm)],[f1562])).
% 0.12/0.51 fof(f1564,plain,(
% 0.12/0.51 $false),
% 0.12/0.51 inference(sat_refutation,[status(thm)],[f554,f560,f617,f749,f911,f1241,f1447,f1563])).
% 0.12/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.53 % Elapsed time: 0.166149 seconds
% 0.12/0.53 % CPU time: 1.164096 seconds
% 0.12/0.53 % Total memory used: 126.010 MB
% 0.12/0.53 % Net memory used: 124.057 MB
%------------------------------------------------------------------------------