%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU101+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 : n018.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 5.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU101+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/5.43 % Computer : n018.cluster.edu
% 0.16/5.43 % Model : x86_64 x86_64
% 0.16/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.43 % Memory : 8046.5625MB
% 0.16/5.43 % OS : Linux 6.8.0-71-generic
% 0.16/5.43 % CPULimit : 300
% 0.16/5.43 % WCLimit : 300
% 0.16/5.43 % DateTime : Mon Sep 21 05:52:50 UTC 2026
% 0.16/5.44 % CPUTime :
% 0.16/5.45 % Drodi V4.1.1
% 0.16/5.49 % Refutation found
% 0.16/5.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/5.49 % SZS output start CNFRefutation for theBenchmark
% 0.16/5.49 fof(f3,axiom,(
% 0.16/5.49 (! [A] :( preboolean(A)=> ( cup_closed(A)& diff_closed(A) ) ) )),
% 0.16/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.49 fof(f5,axiom,(
% 0.16/5.49 (! [A] :( ( cup_closed(A)& diff_closed(A) )=> preboolean(A) ) )),
% 0.16/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.49 fof(f7,axiom,(
% 0.16/5.49 (! [A] :( cup_closed(A)<=> (! [B,C] :( ( in(B,A)& in(C,A) )=> in(set_union2(B,C),A) ) )) )),
% 0.16/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.49 fof(f8,axiom,(
% 0.16/5.49 (! [A] :( diff_closed(A)<=> (! [B,C] :( ( in(B,A)& in(C,A) )=> in(set_difference(B,C),A) ) )) )),
% 0.16/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.49 fof(f28,conjecture,(
% 0.16/5.49 (! [A] :( preboolean(A)<=> (! [B,C] :( ( in(B,A)& in(C,A) )=> ( in(set_union2(B,C),A)& in(set_difference(B,C),A) ) ) )) )),
% 0.16/5.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/5.49 fof(f29,negated_conjecture,(
% 0.16/5.49 ~((! [A] :( preboolean(A)<=> (! [B,C] :( ( in(B,A)& in(C,A) )=> ( in(set_union2(B,C),A)& in(set_difference(B,C),A) ) ) )) ))),
% 0.16/5.49 inference(negated_conjecture,[status(cth)],[f28])).
% 0.16/5.49 fof(f45,plain,(
% 0.16/5.49 ![A]: (~preboolean(A)|(cup_closed(A)&diff_closed(A)))),
% 0.16/5.49 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.16/5.49 fof(f46,plain,(
% 0.16/5.49 ![X0]: (~preboolean(X0)|cup_closed(X0))),
% 0.16/5.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.16/5.49 fof(f47,plain,(
% 0.16/5.49 ![X0]: (~preboolean(X0)|diff_closed(X0))),
% 0.16/5.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.16/5.49 fof(f50,plain,(
% 0.16/5.49 ![A]: ((~cup_closed(A)|~diff_closed(A))|preboolean(A))),
% 0.16/5.49 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.16/5.49 fof(f51,plain,(
% 0.16/5.49 ![X0]: (~cup_closed(X0)|~diff_closed(X0)|preboolean(X0))),
% 0.16/5.49 inference(cnf_transformation,[status(thm)],[f50])).
% 0.16/5.49 fof(f53,plain,(
% 0.16/5.49 ![A]: (cup_closed(A)<=>(![B,C]: ((~in(B,A)|~in(C,A))|in(set_union2(B,C),A))))),
% 0.16/5.49 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.16/5.49 fof(f54,plain,(
% 0.16/5.49 ![A]: ((~cup_closed(A)|(![B,C]: ((~in(B,A)|~in(C,A))|in(set_union2(B,C),A))))&(cup_closed(A)|(?[B,C]: ((in(B,A)&in(C,A))&~in(set_union2(B,C),A)))))),
% 0.16/5.49 inference(NNF_transformation,[status(thm)],[f53])).
% 0.16/5.49 fof(f55,plain,(
% 0.16/5.49 (![A]: (~cup_closed(A)|(![B,C]: ((~in(B,A)|~in(C,A))|in(set_union2(B,C),A)))))&(![A]: (cup_closed(A)|(?[B,C]: ((in(B,A)&in(C,A))&~in(set_union2(B,C),A)))))),
% 0.16/5.49 inference(miniscoping,[status(thm)],[f54])).
% 0.16/5.49 fof(f56,plain,(
% 0.16/5.49 (![A]: (~cup_closed(A)|(![B,C]: ((~in(B,A)|~in(C,A))|in(set_union2(B,C),A)))))&(![A]: (cup_closed(A)|((in(sK0_skl(A),A)&in(sK1_skl(A),A))&~in(set_union2(sK0_skl(A),sK1_skl(A)),A))))),
% 0.16/5.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(B,sK0_skl(A)),skolemize(C,sK1_skl(A))],[f55])).
% 0.16/5.49 fof(f57,plain,(
% 0.16/5.49 ![X0,X1,X2]: (~cup_closed(X0)|~in(X1,X0)|~in(X2,X0)|in(set_union2(X1,X2),X0))),
% 0.16/5.49 inference(cnf_transformation,[status(thm)],[f56])).
% 0.16/5.49 fof(f58,plain,(
% 0.16/5.49 ![X0]: (cup_closed(X0)|in(sK0_skl(X0),X0))),
% 0.16/5.49 inference(cnf_transformation,[status(thm)],[f56])).
% 0.16/5.49 fof(f59,plain,(
% 0.16/5.49 ![X0]: (cup_closed(X0)|in(sK1_skl(X0),X0))),
% 0.16/5.49 inference(cnf_transformation,[status(thm)],[f56])).
% 0.16/5.49 fof(f60,plain,(
% 0.16/5.49 ![X0]: (cup_closed(X0)|~in(set_union2(sK0_skl(X0),sK1_skl(X0)),X0))),
% 0.16/5.49 inference(cnf_transformation,[status(thm)],[f56])).
% 0.16/5.49 fof(f61,plain,(
% 0.16/5.49 ![A]: (diff_closed(A)<=>(![B,C]: ((~in(B,A)|~in(C,A))|in(set_difference(B,C),A))))),
% 0.16/5.49 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.16/5.49 fof(f62,plain,(
% 0.16/5.49 ![A]: ((~diff_closed(A)|(![B,C]: ((~in(B,A)|~in(C,A))|in(set_difference(B,C),A))))&(diff_closed(A)|(?[B,C]: ((in(B,A)&in(C,A))&~in(set_difference(B,C),A)))))),
% 0.16/5.49 inference(NNF_transformation,[status(thm)],[f61])).
% 0.16/5.49 fof(f63,plain,(
% 0.16/5.49 (![A]: (~diff_closed(A)|(![B,C]: ((~in(B,A)|~in(C,A))|in(set_difference(B,C),A)))))&(![A]: (diff_closed(A)|(?[B,C]: ((in(B,A)&in(C,A))&~in(set_difference(B,C),A)))))),
% 0.16/5.49 inference(miniscoping,[status(thm)],[f62])).
% 0.16/5.49 fof(f64,plain,(
% 0.16/5.49 (![A]: (~diff_closed(A)|(![B,C]: ((~in(B,A)|~in(C,A))|in(set_difference(B,C),A)))))&(![A]: (diff_closed(A)|((in(sK2_skl(A),A)&in(sK3_skl(A),A))&~in(set_difference(sK2_skl(A),sK3_skl(A)),A))))),
% 0.16/5.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(B,sK2_skl(A)),skolemize(C,sK3_skl(A))],[f63])).
% 0.16/5.49 fof(f65,plain,(
% 0.16/5.49 ![X0,X1,X2]: (~diff_closed(X0)|~in(X1,X0)|~in(X2,X0)|in(set_difference(X1,X2),X0))),
% 0.16/5.49 inference(cnf_transformation,[status(thm)],[f64])).
% 0.16/5.49 fof(f66,plain,(
% 0.16/5.49 ![X0]: (diff_closed(X0)|in(sK2_skl(X0),X0))),
% 0.16/5.49 inference(cnf_transformation,[status(thm)],[f64])).
% 0.16/5.49 fof(f67,plain,(
% 0.16/5.49 ![X0]: (diff_closed(X0)|in(sK3_skl(X0),X0))),
% 0.16/5.49 inference(cnf_transformation,[status(thm)],[f64])).
% 0.16/5.49 fof(f68,plain,(
% 0.16/5.49 ![X0]: (diff_closed(X0)|~in(set_difference(sK2_skl(X0),sK3_skl(X0)),X0))),
% 0.16/5.49 inference(cnf_transformation,[status(thm)],[f64])).
% 0.16/5.49 fof(f134,plain,(
% 0.16/5.49 (?[A]: (preboolean(A)<~>(![B,C]: ((~in(B,A)|~in(C,A))|(in(set_union2(B,C),A)&in(set_difference(B,C),A))))))),
% 0.16/5.49 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.16/5.49 fof(f135,plain,(
% 0.16/5.49 ?[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.16/5.49 inference(NNF_transformation,[status(thm)],[f134])).
% 0.16/5.49 fof(f136,plain,(
% 0.16/5.49 ((preboolean(sK14_skl)|(![B,C]: ((~in(B,sK14_skl)|~in(C,sK14_skl))|(in(set_union2(B,C),sK14_skl)&in(set_difference(B,C),sK14_skl)))))&(~preboolean(sK14_skl)|((in(sK15_skl,sK14_skl)&in(sK16_skl,sK14_skl))&(~in(set_union2(sK15_skl,sK16_skl),sK14_skl)|~in(set_difference(sK15_skl,sK16_skl),sK14_skl)))))),
% 0.16/5.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl]),skolemize(A,sK14_skl),skolemize(B,sK15_skl),skolemize(C,sK16_skl)],[f135])).
% 0.16/5.49 fof(f137,plain,(
% 0.16/5.49 ![X0,X1]: (preboolean(sK14_skl)|~in(X0,sK14_skl)|~in(X1,sK14_skl)|in(set_union2(X0,X1),sK14_skl))),
% 0.16/5.49 inference(cnf_transformation,[status(thm)],[f136])).
% 0.16/5.49 fof(f138,plain,(
% 0.16/5.49 ![X0,X1]: (preboolean(sK14_skl)|~in(X0,sK14_skl)|~in(X1,sK14_skl)|in(set_difference(X0,X1),sK14_skl))),
% 0.16/5.49 inference(cnf_transformation,[status(thm)],[f136])).
% 0.16/5.49 fof(f139,plain,(
% 0.16/5.49 ~preboolean(sK14_skl)|in(sK15_skl,sK14_skl)),
% 0.16/5.49 inference(cnf_transformation,[status(thm)],[f136])).
% 0.16/5.49 fof(f140,plain,(
% 0.16/5.49 ~preboolean(sK14_skl)|in(sK16_skl,sK14_skl)),
% 0.16/5.49 inference(cnf_transformation,[status(thm)],[f136])).
% 0.16/5.49 fof(f141,plain,(
% 0.16/5.49 ~preboolean(sK14_skl)|~in(set_union2(sK15_skl,sK16_skl),sK14_skl)|~in(set_difference(sK15_skl,sK16_skl),sK14_skl)),
% 0.16/5.49 inference(cnf_transformation,[status(thm)],[f136])).
% 0.16/5.49 fof(f200,plain,(
% 0.16/5.49 cup_closed(sK14_skl)|preboolean(sK14_skl)|~in(sK0_skl(sK14_skl),sK14_skl)|~in(sK1_skl(sK14_skl),sK14_skl)),
% 0.16/5.49 inference(resolution,[status(thm)],[f60,f137])).
% 0.16/5.49 fof(f201,plain,(
% 0.16/5.49 cup_closed(sK14_skl)|~in(sK0_skl(sK14_skl),sK14_skl)|~in(sK1_skl(sK14_skl),sK14_skl)),
% 0.16/5.49 inference(forward_subsumption_resolution,[status(thm)],[f200,f46])).
% 0.16/5.49 fof(f210,plain,(
% 0.16/5.49 diff_closed(sK14_skl)|preboolean(sK14_skl)|~in(sK2_skl(sK14_skl),sK14_skl)|~in(sK3_skl(sK14_skl),sK14_skl)),
% 0.16/5.49 inference(resolution,[status(thm)],[f68,f138])).
% 0.16/5.49 fof(f211,plain,(
% 0.16/5.49 diff_closed(sK14_skl)|~in(sK2_skl(sK14_skl),sK14_skl)|~in(sK3_skl(sK14_skl),sK14_skl)),
% 0.16/5.49 inference(forward_subsumption_resolution,[status(thm)],[f210,f47])).
% 0.16/5.49 fof(f215,plain,(
% 0.16/5.49 cup_closed(sK14_skl)|~in(sK1_skl(sK14_skl),sK14_skl)),
% 0.16/5.49 inference(forward_subsumption_resolution,[status(thm)],[f201,f58])).
% 0.16/5.49 fof(f216,plain,(
% 0.16/5.49 cup_closed(sK14_skl)|cup_closed(sK14_skl)),
% 0.16/5.49 inference(resolution,[status(thm)],[f215,f59])).
% 0.16/5.49 fof(f217,plain,(
% 0.16/5.49 cup_closed(sK14_skl)),
% 0.16/5.49 inference(duplicate_literals_removal,[status(thm)],[f216])).
% 0.16/5.49 fof(f218,plain,(
% 0.16/5.49 diff_closed(sK14_skl)|~in(sK3_skl(sK14_skl),sK14_skl)),
% 0.16/5.49 inference(forward_subsumption_resolution,[status(thm)],[f211,f66])).
% 0.16/5.49 fof(f219,plain,(
% 0.16/5.49 diff_closed(sK14_skl)|diff_closed(sK14_skl)),
% 0.16/5.49 inference(resolution,[status(thm)],[f218,f67])).
% 0.16/5.49 fof(f220,plain,(
% 0.16/5.49 diff_closed(sK14_skl)),
% 0.16/5.49 inference(duplicate_literals_removal,[status(thm)],[f219])).
% 0.16/5.49 fof(f229,plain,(
% 0.16/5.49 ![X0,X1]: (~in(X0,sK14_skl)|~in(X1,sK14_skl)|in(set_union2(X0,X1),sK14_skl))),
% 0.16/5.49 inference(resolution,[status(thm)],[f217,f57])).
% 0.16/5.49 fof(f249,plain,(
% 0.16/5.49 ~cup_closed(sK14_skl)|preboolean(sK14_skl)),
% 0.16/5.49 inference(resolution,[status(thm)],[f220,f51])).
% 0.16/5.50 fof(f250,plain,(
% 0.16/5.50 ![X0,X1]: (~in(X0,sK14_skl)|~in(X1,sK14_skl)|in(set_difference(X0,X1),sK14_skl))),
% 0.16/5.50 inference(resolution,[status(thm)],[f220,f65])).
% 0.16/5.50 fof(f251,plain,(
% 0.16/5.50 preboolean(sK14_skl)),
% 0.16/5.50 inference(forward_subsumption_resolution,[status(thm)],[f249,f217])).
% 0.16/5.50 fof(f254,plain,(
% 0.16/5.50 ~in(set_union2(sK15_skl,sK16_skl),sK14_skl)|~in(set_difference(sK15_skl,sK16_skl),sK14_skl)),
% 0.16/5.50 inference(backward_subsumption_resolution,[status(thm)],[f141,f251])).
% 0.16/5.50 fof(f255,plain,(
% 0.16/5.50 in(sK16_skl,sK14_skl)),
% 0.16/5.50 inference(backward_subsumption_resolution,[status(thm)],[f140,f251])).
% 0.16/5.50 fof(f256,plain,(
% 0.16/5.50 in(sK15_skl,sK14_skl)),
% 0.16/5.50 inference(backward_subsumption_resolution,[status(thm)],[f139,f251])).
% 0.16/5.50 fof(f293,plain,(
% 0.16/5.50 ~in(sK15_skl,sK14_skl)|~in(sK16_skl,sK14_skl)|~in(set_union2(sK15_skl,sK16_skl),sK14_skl)),
% 0.16/5.50 inference(resolution,[status(thm)],[f250,f254])).
% 0.16/5.50 fof(f297,plain,(
% 0.16/5.50 ~in(sK16_skl,sK14_skl)|~in(set_union2(sK15_skl,sK16_skl),sK14_skl)),
% 0.16/5.50 inference(forward_subsumption_resolution,[status(thm)],[f293,f256])).
% 0.16/5.50 fof(f347,plain,(
% 0.16/5.50 ~in(set_union2(sK15_skl,sK16_skl),sK14_skl)),
% 0.16/5.50 inference(forward_subsumption_resolution,[status(thm)],[f297,f255])).
% 0.16/5.50 fof(f348,plain,(
% 0.16/5.50 ~in(sK15_skl,sK14_skl)|~in(sK16_skl,sK14_skl)),
% 0.16/5.50 inference(resolution,[status(thm)],[f347,f229])).
% 0.16/5.50 fof(f349,plain,(
% 0.16/5.50 ~in(sK16_skl,sK14_skl)),
% 0.16/5.50 inference(forward_subsumption_resolution,[status(thm)],[f348,f256])).
% 0.16/5.50 fof(f350,plain,(
% 0.16/5.50 $false),
% 0.16/5.50 inference(forward_subsumption_resolution,[status(thm)],[f349,f255])).
% 0.16/5.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.21/5.52 % Elapsed time: 0.070630 seconds
% 0.21/5.52 % CPU time: 0.288949 seconds
% 0.21/5.52 % Total memory used: 63.872 MB
% 0.21/5.52 % Net memory used: 63.693 MB
%------------------------------------------------------------------------------