%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET013-4 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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:10 PM UTC 2026
% Result : Unsatisfiable 0.09s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET013-4 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n008.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 04:42:09 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.41 % Refutation found
% 0.09/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.41 fof(f3,axiom,(
% 0.09/0.41 (![X,Y]: (( member(f1(X,Y),X)| member(f1(X,Y),Y)| X = Y ) ))),
% 0.09/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f4,axiom,(
% 0.09/0.41 (![X,Y]: (( ~ member(f1(X,Y),X)| ~ member(f1(X,Y),Y)| X = Y ) ))),
% 0.09/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f5,axiom,(
% 0.09/0.41 (![Z,X,Y]: (( ~ member(Z,intersection(X,Y))| member(Z,X) ) ))),
% 0.09/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f6,axiom,(
% 0.09/0.41 (![Z,X,Y]: (( ~ member(Z,intersection(X,Y))| member(Z,Y) ) ))),
% 0.09/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f7,axiom,(
% 0.09/0.41 (![Z,X,Y]: (( member(Z,intersection(X,Y))| ~ member(Z,X)| ~ member(Z,Y) ) ))),
% 0.09/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f10,hypothesis,(
% 0.09/0.41 intersection(as,bs) = cs ),
% 0.09/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f11,hypothesis,(
% 0.09/0.41 intersection(bs,as) = ds ),
% 0.09/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f12,negated_conjecture,(
% 0.09/0.41 cs != ds ),
% 0.09/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.41 fof(f16,plain,(
% 0.09/0.41 ![X0,X1]: (member(f1(X0,X1),X0)|member(f1(X0,X1),X1)|X0=X1)),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f3])).
% 0.09/0.41 fof(f17,plain,(
% 0.09/0.41 ![X0,X1]: (~member(f1(X0,X1),X0)|~member(f1(X0,X1),X1)|X0=X1)),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.41 fof(f18,plain,(
% 0.09/0.41 ![Z,X]: ((![Y]: ~member(Z,intersection(X,Y)))|member(Z,X))),
% 0.09/0.41 inference(miniscoping,[status(thm)],[f5])).
% 0.09/0.41 fof(f19,plain,(
% 0.09/0.41 ![X0,X1,X2]: (~member(X0,intersection(X1,X2))|member(X0,X1))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f18])).
% 0.09/0.41 fof(f20,plain,(
% 0.09/0.41 ![Z,Y]: ((![X]: ~member(Z,intersection(X,Y)))|member(Z,Y))),
% 0.09/0.41 inference(miniscoping,[status(thm)],[f6])).
% 0.09/0.41 fof(f21,plain,(
% 0.09/0.41 ![X0,X1,X2]: (~member(X0,intersection(X1,X2))|member(X0,X2))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f20])).
% 0.09/0.41 fof(f22,plain,(
% 0.09/0.41 ![Z,Y]: ((![X]: (member(Z,intersection(X,Y))|~member(Z,X)))|~member(Z,Y))),
% 0.09/0.41 inference(miniscoping,[status(thm)],[f7])).
% 0.09/0.41 fof(f23,plain,(
% 0.09/0.41 ![X0,X1,X2]: (member(X0,intersection(X1,X2))|~member(X0,X1)|~member(X0,X2))),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f22])).
% 0.09/0.41 fof(f26,plain,(
% 0.09/0.41 intersection(as,bs)=cs),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f10])).
% 0.09/0.41 fof(f27,plain,(
% 0.09/0.41 intersection(bs,as)=ds),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f11])).
% 0.09/0.41 fof(f28,plain,(
% 0.09/0.41 ~cs=ds),
% 0.09/0.41 inference(cnf_transformation,[status(thm)],[f12])).
% 0.09/0.41 fof(f30,plain,(
% 0.09/0.41 ![X0]: (~member(X0,ds)|member(X0,bs))),
% 0.09/0.41 inference(paramodulation,[status(thm)],[f27,f19])).
% 0.09/0.41 fof(f31,plain,(
% 0.09/0.41 ![X0]: (~member(X0,cs)|member(X0,as))),
% 0.09/0.41 inference(paramodulation,[status(thm)],[f26,f19])).
% 0.09/0.41 fof(f32,plain,(
% 0.09/0.41 ![X0]: (~member(X0,ds)|member(X0,as))),
% 0.09/0.41 inference(paramodulation,[status(thm)],[f27,f21])).
% 0.09/0.41 fof(f33,plain,(
% 0.09/0.41 ![X0]: (~member(X0,cs)|member(X0,bs))),
% 0.09/0.41 inference(paramodulation,[status(thm)],[f26,f21])).
% 0.09/0.41 fof(f35,plain,(
% 0.09/0.41 ![X0]: (member(f1(cs,X0),X0)|cs=X0|member(f1(cs,X0),bs))),
% 0.09/0.41 inference(resolution,[status(thm)],[f16,f33])).
% 0.09/0.41 fof(f37,plain,(
% 0.09/0.41 ![X0]: (member(f1(cs,X0),X0)|cs=X0|member(f1(cs,X0),as))),
% 0.09/0.41 inference(resolution,[status(thm)],[f16,f31])).
% 0.09/0.41 fof(f61,plain,(
% 0.09/0.41 cs=ds|member(f1(cs,ds),bs)|member(f1(cs,ds),bs)),
% 0.09/0.41 inference(resolution,[status(thm)],[f35,f30])).
% 0.09/0.41 fof(f69,plain,(
% 0.09/0.41 cs=ds|member(f1(cs,ds),bs)),
% 0.09/0.41 inference(duplicate_literals_removal,[status(thm)],[f61])).
% 0.09/0.41 fof(f70,plain,(
% 0.09/0.41 member(f1(cs,ds),bs)),
% 0.09/0.41 inference(forward_subsumption_resolution,[status(thm)],[f69,f28])).
% 0.09/0.41 fof(f110,plain,(
% 0.09/0.41 ![X0]: (member(X0,ds)|~member(X0,bs)|~member(X0,as))),
% 0.09/0.41 inference(paramodulation,[status(thm)],[f27,f23])).
% 0.09/0.41 fof(f111,plain,(
% 0.09/0.41 ![X0]: (member(X0,cs)|~member(X0,as)|~member(X0,bs))),
% 0.09/0.41 inference(paramodulation,[status(thm)],[f26,f23])).
% 0.09/0.41 fof(f198,plain,(
% 0.09/0.41 cs=ds|member(f1(cs,ds),as)|member(f1(cs,ds),as)),
% 0.09/0.41 inference(resolution,[status(thm)],[f37,f32])).
% 0.09/0.41 fof(f208,plain,(
% 0.09/0.41 cs=ds|member(f1(cs,ds),as)),
% 0.09/0.41 inference(duplicate_literals_removal,[status(thm)],[f198])).
% 0.09/0.41 fof(f209,plain,(
% 0.09/0.41 member(f1(cs,ds),as)),
% 0.09/0.41 inference(forward_subsumption_resolution,[status(thm)],[f208,f28])).
% 0.09/0.41 fof(f211,plain,(
% 0.09/0.41 member(f1(cs,ds),cs)|~member(f1(cs,ds),bs)),
% 0.09/0.41 inference(resolution,[status(thm)],[f209,f111])).
% 0.09/0.41 fof(f212,plain,(
% 0.09/0.41 member(f1(cs,ds),ds)|~member(f1(cs,ds),bs)),
% 0.09/0.41 inference(resolution,[status(thm)],[f209,f110])).
% 0.09/0.41 fof(f214,plain,(
% 0.09/0.41 member(f1(cs,ds),cs)),
% 0.09/0.41 inference(forward_subsumption_resolution,[status(thm)],[f211,f70])).
% 0.09/0.41 fof(f215,plain,(
% 0.09/0.41 member(f1(cs,ds),ds)),
% 0.09/0.41 inference(forward_subsumption_resolution,[status(thm)],[f212,f70])).
% 0.09/0.41 fof(f216,plain,(
% 0.09/0.41 ~member(f1(cs,ds),ds)|cs=ds),
% 0.09/0.41 inference(resolution,[status(thm)],[f214,f17])).
% 0.09/0.41 fof(f236,plain,(
% 0.09/0.41 ~ds=ds),
% 0.09/0.41 inference(backward_demodulation,[status(thm)],[f262,f28])).
% 0.09/0.41 fof(f262,plain,(
% 0.09/0.41 cs=ds),
% 0.09/0.41 inference(forward_subsumption_resolution,[status(thm)],[f216,f215])).
% 0.09/0.41 fof(f277,plain,(
% 0.09/0.41 $false),
% 0.09/0.41 inference(trivial_equality_resolution,[status(thm)],[f236])).
% 0.09/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.44 % Elapsed time: 0.074545 seconds
% 0.09/0.44 % CPU time: 0.293648 seconds
% 0.09/0.44 % Total memory used: 103.838 MB
% 0.09/0.44 % Net memory used: 103.310 MB
%------------------------------------------------------------------------------