%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET064-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 : n007.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:24 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET064-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n007.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 04:46:35 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.13/0.40 % Refutation found
% 0.13/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.40 fof(f1,axiom,(
% 0.13/0.40 (![X,Y,U]: (( ~ subclass(X,Y)| ~ member(U,X)| member(U,Y) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f2,axiom,(
% 0.13/0.40 (![X,Y]: (( member(not_subclass_element(X,Y),X)| subclass(X,Y) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f4,axiom,(
% 0.13/0.40 (![X]: (subclass(X,universal_class) ))),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f7,axiom,(
% 0.13/0.40 (![X,Y]: (( ~ subclass(X,Y)| ~ subclass(Y,X)| X = Y ) ))),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f24,axiom,(
% 0.13/0.40 (![Z,X]: (( ~ member(Z,complement(X))| ~ member(Z,X) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f66,axiom,(
% 0.13/0.40 (![X]: (( X = null_class| member(regular(X),X) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f92,negated_conjecture,(
% 0.13/0.40 z != null_class ),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f93,negated_conjecture,(
% 0.13/0.40 ~ member(not_subclass_element(z,null_class),z) ),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f94,plain,(
% 0.13/0.40 ![Y,U]: ((![X]: (~subclass(X,Y)|~member(U,X)))|member(U,Y))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f1])).
% 0.13/0.40 fof(f95,plain,(
% 0.13/0.40 ![X0,X1,X2]: (~subclass(X0,X1)|~member(X2,X0)|member(X2,X1))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f94])).
% 0.13/0.40 fof(f96,plain,(
% 0.13/0.40 ![X0,X1]: (member(not_subclass_element(X0,X1),X0)|subclass(X0,X1))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.40 fof(f98,plain,(
% 0.13/0.40 ![X0]: (subclass(X0,universal_class))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.40 fof(f101,plain,(
% 0.13/0.40 ![X0,X1]: (~subclass(X0,X1)|~subclass(X1,X0)|X0=X1)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.13/0.40 fof(f126,plain,(
% 0.13/0.40 ![X0,X1]: (~member(X0,complement(X1))|~member(X0,X1))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f24])).
% 0.13/0.40 fof(f168,plain,(
% 0.13/0.40 ![X0]: (X0=null_class|member(regular(X0),X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f66])).
% 0.13/0.40 fof(f199,plain,(
% 0.13/0.40 ~z=null_class),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f92])).
% 0.13/0.40 fof(f200,plain,(
% 0.13/0.40 ~member(not_subclass_element(z,null_class),z)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f93])).
% 0.13/0.40 fof(f204,plain,(
% 0.13/0.40 subclass(z,null_class)),
% 0.13/0.40 inference(resolution,[status(thm)],[f96,f200])).
% 0.13/0.40 fof(f209,plain,(
% 0.13/0.40 ![X0,X1]: (~member(X0,X1)|member(X0,universal_class))),
% 0.13/0.40 inference(resolution,[status(thm)],[f95,f98])).
% 0.13/0.40 fof(f215,definition,(
% 0.13/0.40 sQ0_spl <=> (z=null_class)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f216,plain,(
% 0.13/0.40 z=null_class|~sQ0_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f215])).
% 0.13/0.40 fof(f222,plain,(
% 0.13/0.40 $false|~sQ0_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f216,f199])).
% 0.13/0.40 fof(f223,plain,(
% 0.13/0.40 ~sQ0_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f222])).
% 0.13/0.40 fof(f230,plain,(
% 0.13/0.40 ![X0,X1]: (member(not_subclass_element(X0,X1),universal_class)|subclass(X0,X1))),
% 0.13/0.40 inference(resolution,[status(thm)],[f209,f96])).
% 0.13/0.40 fof(f233,plain,(
% 0.13/0.40 ~subclass(null_class,z)|null_class=z),
% 0.13/0.40 inference(resolution,[status(thm)],[f101,f204])).
% 0.13/0.40 fof(f236,definition,(
% 0.13/0.40 sQ2_spl <=> (subclass(null_class,z))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f238,plain,(
% 0.13/0.40 ~subclass(null_class,z)|sQ2_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f236])).
% 0.13/0.40 fof(f239,plain,(
% 0.13/0.40 ~sQ2_spl|sQ0_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f233,f236,f215])).
% 0.13/0.40 fof(f394,plain,(
% 0.13/0.40 ![X0,X1]: (~member(not_subclass_element(complement(X0),X1),X0)|subclass(complement(X0),X1))),
% 0.13/0.40 inference(resolution,[status(thm)],[f126,f96])).
% 0.13/0.40 fof(f606,plain,(
% 0.13/0.40 ![X0]: (subclass(complement(universal_class),X0)|subclass(complement(universal_class),X0))),
% 0.13/0.40 inference(resolution,[status(thm)],[f394,f230])).
% 0.13/0.40 fof(f607,plain,(
% 0.13/0.40 ![X0]: (subclass(complement(universal_class),X0))),
% 0.13/0.40 inference(duplicate_literals_removal,[status(thm)],[f606])).
% 0.13/0.40 fof(f815,plain,(
% 0.13/0.40 ![X0,X1]: (~member(X0,complement(universal_class))|member(X0,X1))),
% 0.13/0.40 inference(resolution,[status(thm)],[f607,f95])).
% 0.13/0.40 fof(f967,plain,(
% 0.13/0.40 ![X0]: (member(regular(complement(universal_class)),X0)|complement(universal_class)=null_class)),
% 0.13/0.40 inference(resolution,[status(thm)],[f815,f168])).
% 0.13/0.40 fof(f970,definition,(
% 0.13/0.40 ![X0]: (sQ54_spl <=> (member(regular(complement(universal_class)),X0)))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f971,plain,(
% 0.13/0.40 ![X0]: (member(regular(complement(universal_class)),X0)|~sQ54_spl)),
% 0.13/0.40 inference(component_clause,[status(thm)],[f970])).
% 0.13/0.40 fof(f973,definition,(
% 0.13/0.40 sQ55_spl <=> (complement(universal_class)=null_class)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f974,plain,(
% 0.13/0.40 complement(universal_class)=null_class|~sQ55_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f973])).
% 0.13/0.40 fof(f976,plain,(
% 0.13/0.40 sQ54_spl|sQ55_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f967,f970,f973])).
% 0.13/0.40 fof(f981,plain,(
% 0.13/0.40 ![X0]: (~member(regular(complement(universal_class)),X0)|~sQ54_spl)),
% 0.13/0.41 inference(resolution,[status(thm)],[f971,f126])).
% 0.13/0.41 fof(f990,plain,(
% 0.13/0.41 $false|~sQ54_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f981,f971])).
% 0.13/0.41 fof(f991,plain,(
% 0.13/0.41 ~sQ54_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f990])).
% 0.13/0.41 fof(f993,plain,(
% 0.13/0.41 ![X0]: (subclass(null_class,X0)|~sQ55_spl)),
% 0.13/0.41 inference(backward_demodulation,[status(thm)],[f974,f607])).
% 0.13/0.41 fof(f998,plain,(
% 0.13/0.41 $false|~sQ55_spl|sQ2_spl),
% 0.13/0.41 inference(backward_subsumption_resolution,[status(thm)],[f238,f993])).
% 0.13/0.41 fof(f1004,plain,(
% 0.13/0.41 ~sQ55_spl|sQ2_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f998])).
% 0.13/0.41 fof(f1005,plain,(
% 0.13/0.41 $false),
% 0.13/0.41 inference(sat_refutation,[status(thm)],[f223,f239,f976,f991,f1004])).
% 0.13/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.43 % Elapsed time: 0.063543 seconds
% 0.13/0.43 % CPU time: 0.244588 seconds
% 0.13/0.43 % Total memory used: 104.188 MB
% 0.13/0.43 % Net memory used: 103.910 MB
%------------------------------------------------------------------------------