%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET138-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:38 PM UTC 2026
% Result : Unsatisfiable 0.03s 0.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SET138-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Mon Sep 21 04:55:52 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.31 % Drodi V4.1.1
% 0.03/0.37 % Refutation found
% 0.03/0.37 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.03/0.37 % SZS output start CNFRefutation for theBenchmark
% 0.03/0.37 fof(f1,axiom,(
% 0.03/0.37 (![X,Y,U]: (( ~ subclass(X,Y)| ~ member(U,X)| member(U,Y) ) ))),
% 0.03/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.37 fof(f5,axiom,(
% 0.03/0.37 (![X,Y]: (( X != Y| subclass(X,Y) ) ))),
% 0.03/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.37 fof(f8,axiom,(
% 0.03/0.37 (![U,X,Y]: (( ~ member(U,unordered_pair(X,Y))| U = X| U = Y ) ))),
% 0.03/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.37 fof(f9,axiom,(
% 0.03/0.37 (![X,Y]: (( ~ member(X,universal_class)| member(X,unordered_pair(X,Y)) ) ))),
% 0.03/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.37 fof(f11,axiom,(
% 0.03/0.37 (![X,Y]: (member(unordered_pair(X,Y),universal_class) ))),
% 0.03/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.37 fof(f12,axiom,(
% 0.03/0.37 (![X]: (unordered_pair(X,X) = singleton(X) ))),
% 0.03/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.37 fof(f21,axiom,(
% 0.03/0.37 (![Z,X,Y]: (( ~ member(Z,intersection(X,Y))| member(Z,X) ) ))),
% 0.03/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.37 fof(f24,axiom,(
% 0.03/0.37 (![Z,X]: (( ~ member(Z,complement(X))| ~ member(Z,X) ) ))),
% 0.03/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.37 fof(f25,axiom,(
% 0.03/0.37 (![Z,X]: (( ~ member(Z,universal_class)| member(Z,complement(X))| member(Z,X) ) ))),
% 0.03/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.37 fof(f26,axiom,(
% 0.03/0.37 (![X,Y]: (complement(intersection(complement(X),complement(Y))) = union(X,Y) ))),
% 0.03/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.37 fof(f66,axiom,(
% 0.03/0.37 (![X]: (( X = null_class| member(regular(X),X) ) ))),
% 0.03/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.37 fof(f92,axiom,(
% 0.03/0.37 (![X,Y]: (union(singleton(X),Y) = set_builder(X,Y) ))),
% 0.03/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.37 fof(f93,negated_conjecture,(
% 0.03/0.37 member(u,universal_class) ),
% 0.03/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.37 fof(f96,negated_conjecture,(
% 0.03/0.37 ~ member(u,set_builder(u,set_builder(v,set_builder(w,null_class)))) ),
% 0.03/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.37 fof(f97,plain,(
% 0.03/0.37 ![Y,U]: ((![X]: (~subclass(X,Y)|~member(U,X)))|member(U,Y))),
% 0.03/0.37 inference(miniscoping,[status(thm)],[f1])).
% 0.03/0.37 fof(f98,plain,(
% 0.03/0.37 ![X0,X1,X2]: (~subclass(X0,X1)|~member(X2,X0)|member(X2,X1))),
% 0.03/0.37 inference(cnf_transformation,[status(thm)],[f97])).
% 0.03/0.37 fof(f102,plain,(
% 0.03/0.37 ![X0,X1]: (~X0=X1|subclass(X0,X1))),
% 0.03/0.37 inference(cnf_transformation,[status(thm)],[f5])).
% 0.03/0.37 fof(f105,plain,(
% 0.03/0.37 ![U,Y]: ((![X]: (~member(U,unordered_pair(X,Y))|U=X))|U=Y)),
% 0.03/0.37 inference(miniscoping,[status(thm)],[f8])).
% 0.03/0.37 fof(f106,plain,(
% 0.03/0.37 ![X0,X1,X2]: (~member(X0,unordered_pair(X1,X2))|X0=X1|X0=X2)),
% 0.03/0.37 inference(cnf_transformation,[status(thm)],[f105])).
% 0.03/0.37 fof(f107,plain,(
% 0.03/0.37 ![X]: (~member(X,universal_class)|(![Y]: member(X,unordered_pair(X,Y))))),
% 0.03/0.37 inference(miniscoping,[status(thm)],[f9])).
% 0.03/0.37 fof(f108,plain,(
% 0.03/0.37 ![X0,X1]: (~member(X0,universal_class)|member(X0,unordered_pair(X0,X1)))),
% 0.03/0.37 inference(cnf_transformation,[status(thm)],[f107])).
% 0.03/0.37 fof(f111,plain,(
% 0.03/0.37 ![X0,X1]: (member(unordered_pair(X0,X1),universal_class))),
% 0.03/0.37 inference(cnf_transformation,[status(thm)],[f11])).
% 0.03/0.37 fof(f112,plain,(
% 0.03/0.37 ![X0]: (unordered_pair(X0,X0)=singleton(X0))),
% 0.03/0.37 inference(cnf_transformation,[status(thm)],[f12])).
% 0.03/0.37 fof(f124,plain,(
% 0.03/0.37 ![Z,X]: ((![Y]: ~member(Z,intersection(X,Y)))|member(Z,X))),
% 0.03/0.37 inference(miniscoping,[status(thm)],[f21])).
% 0.03/0.37 fof(f125,plain,(
% 0.03/0.37 ![X0,X1,X2]: (~member(X0,intersection(X1,X2))|member(X0,X1))),
% 0.03/0.37 inference(cnf_transformation,[status(thm)],[f124])).
% 0.03/0.37 fof(f129,plain,(
% 0.03/0.37 ![X0,X1]: (~member(X0,complement(X1))|~member(X0,X1))),
% 0.03/0.37 inference(cnf_transformation,[status(thm)],[f24])).
% 0.03/0.37 fof(f130,plain,(
% 0.03/0.37 ![X0,X1]: (~member(X0,universal_class)|member(X0,complement(X1))|member(X0,X1))),
% 0.03/0.37 inference(cnf_transformation,[status(thm)],[f25])).
% 0.03/0.37 fof(f131,plain,(
% 0.03/0.37 ![X0,X1]: (complement(intersection(complement(X0),complement(X1)))=union(X0,X1))),
% 0.03/0.37 inference(cnf_transformation,[status(thm)],[f26])).
% 0.03/0.37 fof(f171,plain,(
% 0.03/0.37 ![X0]: (X0=null_class|member(regular(X0),X0))),
% 0.03/0.37 inference(cnf_transformation,[status(thm)],[f66])).
% 0.03/0.37 fof(f202,plain,(
% 0.03/0.37 ![X0,X1]: (union(singleton(X0),X1)=set_builder(X0,X1))),
% 0.03/0.37 inference(cnf_transformation,[status(thm)],[f92])).
% 0.03/0.37 fof(f203,plain,(
% 0.03/0.37 member(u,universal_class)),
% 0.03/0.37 inference(cnf_transformation,[status(thm)],[f93])).
% 0.03/0.37 fof(f206,plain,(
% 0.03/0.37 ~member(u,set_builder(u,set_builder(v,set_builder(w,null_class))))),
% 0.03/0.37 inference(cnf_transformation,[status(thm)],[f96])).
% 0.03/0.37 fof(f207,plain,(
% 0.03/0.37 ![X0]: (subclass(X0,X0))),
% 0.03/0.37 inference(destructive_equality_resolution,[status(thm)],[f102])).
% 0.03/0.37 fof(f210,plain,(
% 0.03/0.37 ![X0]: (~subclass(X0,set_builder(u,set_builder(v,set_builder(w,null_class))))|~member(u,X0))),
% 0.03/0.37 inference(resolution,[status(thm)],[f98,f206])).
% 0.03/0.37 fof(f230,plain,(
% 0.03/0.37 ![X0,X1]: (~member(X0,singleton(X1))|X0=X1|X0=X1)),
% 0.03/0.37 inference(paramodulation,[status(thm)],[f112,f106])).
% 0.03/0.37 fof(f231,plain,(
% 0.03/0.37 ![X0,X1]: (~member(X0,singleton(X1))|X0=X1)),
% 0.03/0.37 inference(duplicate_literals_removal,[status(thm)],[f230])).
% 0.03/0.37 fof(f237,plain,(
% 0.03/0.37 ![X0]: (singleton(X0)=null_class|regular(singleton(X0))=X0)),
% 0.03/0.37 inference(resolution,[status(thm)],[f171,f231])).
% 0.03/0.37 fof(f240,plain,(
% 0.03/0.37 ![X0]: (~member(X0,universal_class)|member(X0,singleton(X0)))),
% 0.03/0.37 inference(paramodulation,[status(thm)],[f112,f108])).
% 0.03/0.37 fof(f344,plain,(
% 0.03/0.37 ![X0]: (~member(u,universal_class)|member(u,X0)|~subclass(complement(X0),set_builder(u,set_builder(v,set_builder(w,null_class)))))),
% 0.03/0.37 inference(resolution,[status(thm)],[f130,f210])).
% 0.03/0.37 fof(f346,definition,(
% 0.03/0.37 sQ15_spl <=> (member(u,universal_class))),
% 0.03/0.37 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.03/0.37 fof(f348,plain,(
% 0.03/0.37 ~member(u,universal_class)|sQ15_spl),
% 0.03/0.37 inference(component_clause,[status(thm)],[f346])).
% 0.03/0.37 fof(f349,definition,(
% 0.03/0.37 ![X0]: (sQ16_spl <=> (member(u,X0)|~subclass(complement(X0),set_builder(u,set_builder(v,set_builder(w,null_class))))))),
% 0.03/0.37 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.03/0.37 fof(f350,plain,(
% 0.03/0.37 ![X0]: (member(u,X0)|~subclass(complement(X0),set_builder(u,set_builder(v,set_builder(w,null_class))))|~sQ16_spl)),
% 0.03/0.37 inference(component_clause,[status(thm)],[f349])).
% 0.03/0.37 fof(f352,plain,(
% 0.03/0.37 ~sQ15_spl|sQ16_spl),
% 0.03/0.37 inference(split_clause,[status(thm)],[f344,f346,f349])).
% 0.03/0.37 fof(f353,plain,(
% 0.03/0.37 $false|sQ15_spl),
% 0.03/0.37 inference(forward_subsumption_resolution,[status(thm)],[f348,f203])).
% 0.03/0.37 fof(f354,plain,(
% 0.03/0.37 sQ15_spl),
% 0.03/0.37 inference(contradiction_clause,[status(thm)],[f353])).
% 0.03/0.37 fof(f359,definition,(
% 0.03/0.37 sQ17_spl <=> (subclass(omega,omega))),
% 0.03/0.37 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.03/0.37 fof(f361,plain,(
% 0.03/0.37 ~subclass(omega,omega)|sQ17_spl),
% 0.03/0.37 inference(component_clause,[status(thm)],[f359])).
% 0.03/0.37 fof(f366,plain,(
% 0.03/0.37 $false|sQ17_spl),
% 0.03/0.37 inference(forward_subsumption_resolution,[status(thm)],[f361,f207])).
% 0.03/0.37 fof(f367,plain,(
% 0.03/0.37 sQ17_spl),
% 0.03/0.37 inference(contradiction_clause,[status(thm)],[f366])).
% 0.03/0.37 fof(f370,plain,(
% 0.03/0.37 ![X0]: (singleton(X0)=null_class|member(X0,singleton(X0))|singleton(X0)=null_class)),
% 0.03/0.37 inference(paramodulation,[status(thm)],[f237,f171])).
% 0.03/0.37 fof(f373,plain,(
% 0.03/0.37 ![X0]: (singleton(X0)=null_class|member(X0,singleton(X0)))),
% 0.03/0.37 inference(duplicate_literals_removal,[status(thm)],[f370])).
% 0.03/0.37 fof(f437,definition,(
% 0.03/0.37 sQ28_spl <=> (singleton(u)=null_class)),
% 0.03/0.37 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.03/0.37 fof(f438,plain,(
% 0.03/0.37 singleton(u)=null_class|~sQ28_spl),
% 0.03/0.37 inference(component_clause,[status(thm)],[f437])).
% 0.03/0.37 fof(f441,plain,(
% 0.03/0.37 ~member(u,universal_class)|member(u,null_class)|~sQ28_spl),
% 0.03/0.37 inference(paramodulation,[status(thm)],[f438,f240])).
% 0.03/0.37 fof(f451,definition,(
% 0.03/0.37 sQ29_spl <=> (member(u,null_class))),
% 0.03/0.37 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.03/0.37 fof(f452,plain,(
% 0.03/0.37 member(u,null_class)|~sQ29_spl),
% 0.03/0.37 inference(component_clause,[status(thm)],[f451])).
% 0.03/0.37 fof(f454,plain,(
% 0.03/0.37 ~sQ15_spl|sQ29_spl|~sQ28_spl),
% 0.03/0.37 inference(split_clause,[status(thm)],[f441,f346,f451,f437])).
% 0.03/0.37 fof(f519,definition,(
% 0.03/0.37 ![X0]: (sQ33_spl <=> (~member(X0,universal_class)))),
% 0.03/0.37 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.03/0.37 fof(f520,plain,(
% 0.03/0.37 ![X0]: (~member(X0,universal_class)|~sQ33_spl)),
% 0.03/0.37 inference(component_clause,[status(thm)],[f519])).
% 0.03/0.37 fof(f531,plain,(
% 0.03/0.37 ![X0,X1]: (member(u,intersection(complement(X0),complement(X1)))|~subclass(union(X0,X1),set_builder(u,set_builder(v,set_builder(w,null_class))))|~sQ16_spl)),
% 0.03/0.37 inference(paramodulation,[status(thm)],[f131,f350])).
% 0.03/0.37 fof(f535,plain,(
% 0.03/0.37 $false|~sQ33_spl),
% 0.03/0.37 inference(backward_subsumption_resolution,[status(thm)],[f111,f520])).
% 0.03/0.37 fof(f542,plain,(
% 0.03/0.37 ~sQ33_spl),
% 0.03/0.37 inference(contradiction_clause,[status(thm)],[f535])).
% 0.03/0.37 fof(f544,plain,(
% 0.03/0.37 ![X0,X1]: (member(u,intersection(complement(singleton(X0)),complement(X1)))|~subclass(set_builder(X0,X1),set_builder(u,set_builder(v,set_builder(w,null_class))))|~sQ16_spl)),
% 0.03/0.37 inference(paramodulation,[status(thm)],[f202,f531])).
% 0.03/0.37 fof(f546,plain,(
% 0.03/0.37 member(u,intersection(complement(singleton(u)),complement(set_builder(v,set_builder(w,null_class)))))|~sQ16_spl),
% 0.03/0.37 inference(resolution,[status(thm)],[f544,f207])).
% 0.03/0.37 fof(f564,plain,(
% 0.03/0.37 member(u,complement(singleton(u)))|~sQ16_spl),
% 0.03/0.37 inference(resolution,[status(thm)],[f125,f546])).
% 0.03/0.37 fof(f569,plain,(
% 0.03/0.37 ~member(u,singleton(u))|~sQ16_spl),
% 0.03/0.37 inference(resolution,[status(thm)],[f564,f129])).
% 0.03/0.37 fof(f584,plain,(
% 0.03/0.37 singleton(u)=null_class|~sQ16_spl),
% 0.03/0.37 inference(resolution,[status(thm)],[f373,f569])).
% 0.03/0.37 fof(f586,plain,(
% 0.03/0.37 sQ28_spl|~sQ16_spl),
% 0.03/0.37 inference(split_clause,[status(thm)],[f584,f437,f349])).
% 0.03/0.37 fof(f587,plain,(
% 0.03/0.37 ~member(u,null_class)|~sQ28_spl|~sQ16_spl),
% 0.03/0.37 inference(backward_demodulation,[status(thm)],[f438,f569])).
% 0.03/0.37 fof(f606,plain,(
% 0.03/0.37 $false|~sQ29_spl|~sQ28_spl|~sQ16_spl),
% 0.03/0.37 inference(forward_subsumption_resolution,[status(thm)],[f587,f452])).
% 0.03/0.37 fof(f607,plain,(
% 0.03/0.37 ~sQ29_spl|~sQ28_spl|~sQ16_spl),
% 0.03/0.37 inference(contradiction_clause,[status(thm)],[f606])).
% 0.03/0.37 fof(f608,plain,(
% 0.03/0.37 $false),
% 0.03/0.37 inference(sat_refutation,[status(thm)],[f352,f354,f367,f454,f542,f586,f607])).
% 0.03/0.37 % SZS output end CNFRefutation for theBenchmark.p
% 0.03/0.37 % Elapsed time: 0.070623 seconds
% 0.03/0.37 % CPU time: 0.286266 seconds
% 0.03/0.37 % Total memory used: 77.840 MB
% 0.03/0.37 % Net memory used: 77.250 MB
%------------------------------------------------------------------------------