%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET015-4 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:11:11 PM UTC 2026
% Result : Unsatisfiable 3.81s 0.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SET015-4 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 04:42:37 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 % Drodi V4.1.1
% 3.81/0.87 % Refutation found
% 3.81/0.87 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 3.81/0.87 % SZS output start CNFRefutation for theBenchmark
% 3.81/0.87 fof(f1,axiom,(
% 3.81/0.87 (![X,Y]: (( ~ member(X,Y)| little_set(X) ) ))),
% 3.81/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.81/0.87 fof(f2,axiom,(
% 3.81/0.87 (![X,Y]: (( little_set(f1(X,Y))| X = Y ) ))),
% 3.81/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.81/0.87 fof(f3,axiom,(
% 3.81/0.87 (![X,Y]: (( member(f1(X,Y),X)| member(f1(X,Y),Y)| X = Y ) ))),
% 3.81/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.81/0.87 fof(f4,axiom,(
% 3.81/0.87 (![X,Y]: (( ~ member(f1(X,Y),X)| ~ member(f1(X,Y),Y)| X = Y ) ))),
% 3.81/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.81/0.87 fof(f5,axiom,(
% 3.81/0.87 (![Z,X,Y]: (( ~ member(Z,intersection(X,Y))| member(Z,X) ) ))),
% 3.81/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.81/0.87 fof(f6,axiom,(
% 3.81/0.87 (![Z,X,Y]: (( ~ member(Z,intersection(X,Y))| member(Z,Y) ) ))),
% 3.81/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.81/0.87 fof(f7,axiom,(
% 3.81/0.87 (![Z,X,Y]: (( member(Z,intersection(X,Y))| ~ member(Z,X)| ~ member(Z,Y) ) ))),
% 3.81/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.81/0.87 fof(f8,axiom,(
% 3.81/0.87 (![Z,X]: (( ~ member(Z,complement(X))| ~ member(Z,X) ) ))),
% 3.81/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.81/0.87 fof(f9,axiom,(
% 3.81/0.87 (![Z,X]: (( member(Z,complement(X))| ~ little_set(Z)| member(Z,X) ) ))),
% 3.81/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.81/0.87 fof(f10,axiom,(
% 3.81/0.87 (![X,Y]: (union(X,Y) = complement(intersection(complement(X),complement(Y))) ))),
% 3.81/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.81/0.87 fof(f13,hypothesis,(
% 3.81/0.87 union(as,bs) = cs ),
% 3.81/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.81/0.87 fof(f14,hypothesis,(
% 3.81/0.87 union(bs,as) = ds ),
% 3.81/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.81/0.87 fof(f15,negated_conjecture,(
% 3.81/0.87 cs != ds ),
% 3.81/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.81/0.87 fof(f16,plain,(
% 3.81/0.87 ![X]: ((![Y]: ~member(X,Y))|little_set(X))),
% 3.81/0.87 inference(miniscoping,[status(thm)],[f1])).
% 3.81/0.87 fof(f17,plain,(
% 3.81/0.87 ![X0,X1]: (~member(X0,X1)|little_set(X0))),
% 3.81/0.87 inference(cnf_transformation,[status(thm)],[f16])).
% 3.81/0.87 fof(f18,plain,(
% 3.81/0.87 ![X0,X1]: (little_set(f1(X0,X1))|X0=X1)),
% 3.81/0.87 inference(cnf_transformation,[status(thm)],[f2])).
% 3.81/0.87 fof(f19,plain,(
% 3.81/0.87 ![X0,X1]: (member(f1(X0,X1),X0)|member(f1(X0,X1),X1)|X0=X1)),
% 3.81/0.87 inference(cnf_transformation,[status(thm)],[f3])).
% 3.81/0.87 fof(f20,plain,(
% 3.81/0.87 ![X0,X1]: (~member(f1(X0,X1),X0)|~member(f1(X0,X1),X1)|X0=X1)),
% 3.81/0.87 inference(cnf_transformation,[status(thm)],[f4])).
% 3.81/0.87 fof(f21,plain,(
% 3.81/0.87 ![Z,X]: ((![Y]: ~member(Z,intersection(X,Y)))|member(Z,X))),
% 3.81/0.87 inference(miniscoping,[status(thm)],[f5])).
% 3.81/0.87 fof(f22,plain,(
% 3.81/0.87 ![X0,X1,X2]: (~member(X0,intersection(X1,X2))|member(X0,X1))),
% 3.81/0.87 inference(cnf_transformation,[status(thm)],[f21])).
% 3.81/0.87 fof(f23,plain,(
% 3.81/0.87 ![Z,Y]: ((![X]: ~member(Z,intersection(X,Y)))|member(Z,Y))),
% 3.81/0.87 inference(miniscoping,[status(thm)],[f6])).
% 3.81/0.87 fof(f24,plain,(
% 3.81/0.87 ![X0,X1,X2]: (~member(X0,intersection(X1,X2))|member(X0,X2))),
% 3.81/0.87 inference(cnf_transformation,[status(thm)],[f23])).
% 3.81/0.87 fof(f25,plain,(
% 3.81/0.87 ![Z,Y]: ((![X]: (member(Z,intersection(X,Y))|~member(Z,X)))|~member(Z,Y))),
% 3.81/0.87 inference(miniscoping,[status(thm)],[f7])).
% 3.81/0.87 fof(f26,plain,(
% 3.81/0.87 ![X0,X1,X2]: (member(X0,intersection(X1,X2))|~member(X0,X1)|~member(X0,X2))),
% 3.81/0.87 inference(cnf_transformation,[status(thm)],[f25])).
% 3.81/0.87 fof(f27,plain,(
% 3.81/0.87 ![X0,X1]: (~member(X0,complement(X1))|~member(X0,X1))),
% 3.81/0.87 inference(cnf_transformation,[status(thm)],[f8])).
% 3.81/0.87 fof(f28,plain,(
% 3.81/0.87 ![X0,X1]: (member(X0,complement(X1))|~little_set(X0)|member(X0,X1))),
% 3.81/0.87 inference(cnf_transformation,[status(thm)],[f9])).
% 3.81/0.87 fof(f29,plain,(
% 3.81/0.87 ![X0,X1]: (union(X0,X1)=complement(intersection(complement(X0),complement(X1))))),
% 3.81/0.87 inference(cnf_transformation,[status(thm)],[f10])).
% 3.81/0.87 fof(f32,plain,(
% 3.81/0.87 union(as,bs)=cs),
% 3.81/0.87 inference(cnf_transformation,[status(thm)],[f13])).
% 3.81/0.87 fof(f33,plain,(
% 3.81/0.87 union(bs,as)=ds),
% 3.81/0.87 inference(cnf_transformation,[status(thm)],[f14])).
% 3.81/0.87 fof(f34,plain,(
% 3.81/0.87 ~cs=ds),
% 3.81/0.87 inference(cnf_transformation,[status(thm)],[f15])).
% 3.81/0.87 fof(f40,plain,(
% 3.81/0.87 ![X0,X1,X2]: (~member(X0,union(X1,X2))|~member(X0,intersection(complement(X1),complement(X2))))),
% 3.81/0.87 inference(paramodulation,[status(thm)],[f29,f27])).
% 3.81/0.87 fof(f42,plain,(
% 3.81/0.87 ![X0]: (~member(X0,ds)|~member(X0,intersection(complement(bs),complement(as))))),
% 3.81/0.87 inference(paramodulation,[status(thm)],[f33,f40])).
% 3.81/0.87 fof(f43,plain,(
% 3.81/0.87 ![X0]: (~member(X0,cs)|~member(X0,intersection(complement(as),complement(bs))))),
% 3.81/0.87 inference(paramodulation,[status(thm)],[f32,f40])).
% 3.81/0.87 fof(f78,plain,(
% 3.81/0.87 ![X0,X1,X2]: (member(f1(X0,X1),complement(X2))|member(f1(X0,X1),X2)|X0=X1)),
% 3.81/0.87 inference(resolution,[status(thm)],[f28,f18])).
% 3.81/0.87 fof(f88,plain,(
% 3.81/0.87 ![X0]: (member(f1(ds,X0),X0)|ds=X0|~member(f1(ds,X0),intersection(complement(bs),complement(as))))),
% 3.81/0.87 inference(resolution,[status(thm)],[f19,f42])).
% 3.81/0.87 fof(f102,plain,(
% 3.81/0.87 ![X0]: (member(f1(X0,cs),X0)|X0=cs|~member(f1(X0,cs),intersection(complement(as),complement(bs))))),
% 3.81/0.87 inference(resolution,[status(thm)],[f19,f43])).
% 3.81/0.87 fof(f120,plain,(
% 3.81/0.87 ![X0]: (member(f1(ds,X0),X0)|ds=X0|~member(f1(ds,X0),complement(bs))|~member(f1(ds,X0),complement(as)))),
% 3.81/0.87 inference(resolution,[status(thm)],[f88,f26])).
% 3.81/0.87 fof(f123,plain,(
% 3.81/0.87 ![X0]: (member(f1(X0,cs),X0)|X0=cs|~member(f1(X0,cs),complement(as))|~member(f1(X0,cs),complement(bs)))),
% 3.81/0.87 inference(resolution,[status(thm)],[f102,f26])).
% 3.81/0.87 fof(f209,plain,(
% 3.81/0.87 ![X0]: (member(f1(ds,X0),bs)|ds=X0|member(f1(ds,X0),X0)|ds=X0|~member(f1(ds,X0),complement(as)))),
% 3.81/0.87 inference(resolution,[status(thm)],[f78,f120])).
% 3.81/0.87 fof(f212,plain,(
% 3.81/0.87 ![X0]: (member(f1(X0,cs),bs)|X0=cs|member(f1(X0,cs),X0)|X0=cs|~member(f1(X0,cs),complement(as)))),
% 3.81/0.87 inference(resolution,[status(thm)],[f78,f123])).
% 3.81/0.87 fof(f223,plain,(
% 3.81/0.87 ![X0]: (member(f1(ds,X0),bs)|ds=X0|member(f1(ds,X0),X0)|~member(f1(ds,X0),complement(as)))),
% 3.81/0.87 inference(duplicate_literals_removal,[status(thm)],[f209])).
% 3.81/0.87 fof(f226,plain,(
% 3.81/0.87 ![X0]: (member(f1(X0,cs),bs)|X0=cs|member(f1(X0,cs),X0)|~member(f1(X0,cs),complement(as)))),
% 3.81/0.87 inference(duplicate_literals_removal,[status(thm)],[f212])).
% 3.81/0.87 fof(f232,plain,(
% 3.81/0.87 ![X0]: (member(f1(ds,X0),bs)|ds=X0|member(f1(ds,X0),X0)|member(f1(ds,X0),as)|ds=X0)),
% 3.81/0.87 inference(resolution,[status(thm)],[f223,f78])).
% 3.81/0.87 fof(f234,plain,(
% 3.81/0.87 ![X0]: (member(f1(ds,X0),bs)|ds=X0|member(f1(ds,X0),X0)|member(f1(ds,X0),as))),
% 3.81/0.87 inference(duplicate_literals_removal,[status(thm)],[f232])).
% 3.81/0.87 fof(f247,plain,(
% 3.81/0.87 ![X0]: (member(f1(ds,X0),bs)|ds=X0|member(f1(ds,X0),as)|~member(f1(ds,X0),ds)|ds=X0)),
% 3.81/0.87 inference(resolution,[status(thm)],[f234,f20])).
% 3.81/0.87 fof(f270,plain,(
% 3.81/0.87 ![X0]: (member(f1(ds,X0),bs)|ds=X0|member(f1(ds,X0),as)|~member(f1(ds,X0),ds))),
% 3.81/0.87 inference(duplicate_literals_removal,[status(thm)],[f247])).
% 3.81/0.87 fof(f330,plain,(
% 3.81/0.87 ![X0]: (member(f1(X0,cs),bs)|X0=cs|member(f1(X0,cs),X0)|member(f1(X0,cs),as)|X0=cs)),
% 3.81/0.87 inference(resolution,[status(thm)],[f226,f78])).
% 3.81/0.87 fof(f332,plain,(
% 3.81/0.87 ![X0]: (member(f1(X0,cs),bs)|X0=cs|member(f1(X0,cs),X0)|member(f1(X0,cs),as))),
% 3.81/0.87 inference(duplicate_literals_removal,[status(thm)],[f330])).
% 3.81/0.87 fof(f355,plain,(
% 3.81/0.87 member(f1(ds,cs),bs)|ds=cs|member(f1(ds,cs),as)|member(f1(ds,cs),bs)|ds=cs|member(f1(ds,cs),as)),
% 3.81/0.87 inference(resolution,[status(thm)],[f332,f270])).
% 3.81/0.87 fof(f368,plain,(
% 3.81/0.87 member(f1(ds,cs),bs)|ds=cs|member(f1(ds,cs),as)),
% 3.81/0.87 inference(duplicate_literals_removal,[status(thm)],[f355])).
% 3.81/0.87 fof(f369,plain,(
% 3.81/0.87 member(f1(ds,cs),bs)|member(f1(ds,cs),as)),
% 3.81/0.87 inference(forward_subsumption_resolution,[status(thm)],[f368,f34])).
% 3.81/0.87 fof(f380,plain,(
% 3.81/0.87 member(f1(ds,cs),as)|little_set(f1(ds,cs))),
% 3.81/0.87 inference(resolution,[status(thm)],[f369,f17])).
% 3.81/0.87 fof(f381,plain,(
% 3.81/0.87 little_set(f1(ds,cs))),
% 3.81/0.87 inference(forward_subsumption_resolution,[status(thm)],[f380,f17])).
% 3.81/0.87 fof(f1142,plain,(
% 3.81/0.87 ![X0]: (member(f1(ds,cs),complement(X0))|member(f1(ds,cs),X0))),
% 3.81/0.87 inference(resolution,[status(thm)],[f381,f28])).
% 3.81/0.87 fof(f1717,plain,(
% 3.81/0.87 ![X0,X1]: (member(f1(ds,cs),union(X0,X1))|member(f1(ds,cs),intersection(complement(X0),complement(X1))))),
% 3.81/0.87 inference(paramodulation,[status(thm)],[f29,f1142])).
% 3.81/0.87 fof(f1721,plain,(
% 3.81/0.87 ![X0,X1]: (member(f1(ds,cs),union(X0,X1))|member(f1(ds,cs),complement(X1)))),
% 3.81/0.87 inference(resolution,[status(thm)],[f1717,f24])).
% 3.81/0.87 fof(f1722,plain,(
% 3.81/0.87 ![X0,X1]: (member(f1(ds,cs),union(X0,X1))|member(f1(ds,cs),complement(X0)))),
% 3.81/0.87 inference(resolution,[status(thm)],[f1717,f22])).
% 3.81/0.88 fof(f1745,plain,(
% 3.81/0.88 member(f1(ds,cs),ds)|member(f1(ds,cs),complement(as))),
% 3.81/0.88 inference(paramodulation,[status(thm)],[f33,f1721])).
% 3.81/0.88 fof(f1746,plain,(
% 3.81/0.88 member(f1(ds,cs),cs)|member(f1(ds,cs),complement(bs))),
% 3.81/0.88 inference(paramodulation,[status(thm)],[f32,f1721])).
% 3.81/0.88 fof(f1752,plain,(
% 3.81/0.88 member(f1(ds,cs),ds)|member(f1(ds,cs),bs)|ds=cs|member(f1(ds,cs),ds)),
% 3.81/0.88 inference(resolution,[status(thm)],[f1745,f226])).
% 3.81/0.88 fof(f1755,plain,(
% 3.81/0.88 member(f1(ds,cs),ds)|member(f1(ds,cs),bs)|ds=cs),
% 3.81/0.88 inference(duplicate_literals_removal,[status(thm)],[f1752])).
% 3.81/0.88 fof(f1756,plain,(
% 3.81/0.88 member(f1(ds,cs),ds)|member(f1(ds,cs),bs)),
% 3.81/0.88 inference(forward_subsumption_resolution,[status(thm)],[f1755,f34])).
% 3.81/0.88 fof(f1763,plain,(
% 3.81/0.88 member(f1(ds,cs),cs)|~member(f1(ds,cs),bs)),
% 3.81/0.88 inference(resolution,[status(thm)],[f1746,f27])).
% 3.81/0.88 fof(f1803,plain,(
% 3.81/0.88 member(f1(ds,cs),ds)|member(f1(ds,cs),complement(bs))),
% 3.81/0.88 inference(paramodulation,[status(thm)],[f33,f1722])).
% 3.81/0.88 fof(f1804,plain,(
% 3.81/0.88 member(f1(ds,cs),cs)|member(f1(ds,cs),complement(as))),
% 3.81/0.88 inference(paramodulation,[status(thm)],[f32,f1722])).
% 3.81/0.88 fof(f1813,plain,(
% 3.81/0.88 member(f1(ds,cs),ds)|~member(f1(ds,cs),bs)),
% 3.81/0.88 inference(resolution,[status(thm)],[f1803,f27])).
% 3.81/0.88 fof(f1817,plain,(
% 3.81/0.88 member(f1(ds,cs),ds)),
% 3.81/0.88 inference(forward_subsumption_resolution,[status(thm)],[f1813,f1756])).
% 3.81/0.88 fof(f1818,plain,(
% 3.81/0.88 member(f1(ds,cs),cs)|member(f1(ds,cs),bs)|ds=cs|member(f1(ds,cs),cs)),
% 3.81/0.88 inference(resolution,[status(thm)],[f1804,f223])).
% 3.81/0.88 fof(f1822,plain,(
% 3.81/0.88 member(f1(ds,cs),cs)|member(f1(ds,cs),bs)|ds=cs),
% 3.81/0.88 inference(duplicate_literals_removal,[status(thm)],[f1818])).
% 3.81/0.88 fof(f1823,plain,(
% 3.81/0.88 member(f1(ds,cs),cs)|member(f1(ds,cs),bs)),
% 3.81/0.88 inference(forward_subsumption_resolution,[status(thm)],[f1822,f34])).
% 3.81/0.88 fof(f1824,plain,(
% 3.81/0.88 member(f1(ds,cs),bs)|~member(f1(ds,cs),ds)|ds=cs),
% 3.81/0.88 inference(resolution,[status(thm)],[f1823,f20])).
% 3.81/0.88 fof(f1827,plain,(
% 3.81/0.88 member(f1(ds,cs),bs)|ds=cs),
% 3.81/0.88 inference(forward_subsumption_resolution,[status(thm)],[f1824,f1756])).
% 3.81/0.88 fof(f1828,plain,(
% 3.81/0.88 member(f1(ds,cs),bs)),
% 3.81/0.88 inference(forward_subsumption_resolution,[status(thm)],[f1827,f34])).
% 3.81/0.88 fof(f3112,plain,(
% 3.81/0.88 member(f1(ds,cs),cs)),
% 3.81/0.88 inference(forward_subsumption_resolution,[status(thm)],[f1763,f1828])).
% 3.81/0.88 fof(f3113,plain,(
% 3.81/0.88 ~member(f1(ds,cs),ds)|ds=cs),
% 3.81/0.88 inference(resolution,[status(thm)],[f3112,f20])).
% 3.81/0.88 fof(f3116,plain,(
% 3.81/0.88 ds=cs),
% 3.81/0.88 inference(forward_subsumption_resolution,[status(thm)],[f3113,f1817])).
% 3.81/0.88 fof(f3117,plain,(
% 3.81/0.88 $false),
% 3.81/0.88 inference(forward_subsumption_resolution,[status(thm)],[f3116,f34])).
% 3.81/0.88 % SZS output end CNFRefutation for theBenchmark.p
% 3.60/0.91 % Elapsed time: 0.594614 seconds
% 3.60/0.91 % CPU time: 4.408788 seconds
% 3.60/0.91 % Total memory used: 192.326 MB
% 3.60/0.91 % Net memory used: 187.615 MB
%------------------------------------------------------------------------------