%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM078-1 : 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 : n026.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 01:42:13 PM UTC 2026
% Result : Unsatisfiable 4.05s 0.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM078-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n026.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 02:05:36 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 4.05/0.95 % Refutation found
% 4.05/0.95 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 4.05/0.95 % SZS output start CNFRefutation for theBenchmark
% 4.05/0.95 fof(f1,axiom,(
% 4.05/0.95 (![X,Y,U]: (( ~ subclass(X,Y)| ~ member(U,X)| member(U,Y) ) ))),
% 4.05/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.05/0.95 fof(f2,axiom,(
% 4.05/0.95 (![X,Y]: (( member(not_subclass_element(X,Y),X)| subclass(X,Y) ) ))),
% 4.05/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.05/0.95 fof(f3,axiom,(
% 4.05/0.95 (![X,Y]: (( ~ member(not_subclass_element(X,Y),Y)| subclass(X,Y) ) ))),
% 4.05/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.05/0.95 fof(f4,axiom,(
% 4.05/0.95 (![X]: (subclass(X,universal_class) ))),
% 4.05/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.05/0.95 fof(f7,axiom,(
% 4.05/0.95 (![X,Y]: (( ~ subclass(X,Y)| ~ subclass(Y,X)| X = Y ) ))),
% 4.05/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.05/0.95 fof(f8,axiom,(
% 4.05/0.95 (![U,X,Y]: (( ~ member(U,unordered_pair(X,Y))| U = X| U = Y ) ))),
% 4.05/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.05/0.95 fof(f9,axiom,(
% 4.05/0.95 (![X,Y]: (( ~ member(X,universal_class)| member(X,unordered_pair(X,Y)) ) ))),
% 4.05/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.05/0.95 fof(f12,axiom,(
% 4.05/0.95 (![X]: (unordered_pair(X,X) = singleton(X) ))),
% 4.05/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.05/0.95 fof(f21,axiom,(
% 4.05/0.95 (![Z,X,Y]: (( ~ member(Z,intersection(X,Y))| member(Z,X) ) ))),
% 4.05/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.05/0.95 fof(f22,axiom,(
% 4.05/0.95 (![Z,X,Y]: (( ~ member(Z,intersection(X,Y))| member(Z,Y) ) ))),
% 4.05/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.05/0.95 fof(f23,axiom,(
% 4.05/0.95 (![Z,X,Y]: (( ~ member(Z,X)| ~ member(Z,Y)| member(Z,intersection(X,Y)) ) ))),
% 4.05/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.05/0.95 fof(f24,axiom,(
% 4.05/0.95 (![Z,X]: (( ~ member(Z,complement(X))| ~ member(Z,X) ) ))),
% 4.05/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.05/0.95 fof(f66,axiom,(
% 4.05/0.95 (![X]: (( X = null_class| member(regular(X),X) ) ))),
% 4.05/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.05/0.95 fof(f67,axiom,(
% 4.05/0.95 (![X]: (( X = null_class| intersection(X,regular(X)) = null_class ) ))),
% 4.05/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.05/0.95 fof(f161,negated_conjecture,(
% 4.05/0.95 member(u,intersection(u,y)) ),
% 4.05/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.05/0.95 fof(f162,plain,(
% 4.05/0.95 ![Y,U]: ((![X]: (~subclass(X,Y)|~member(U,X)))|member(U,Y))),
% 4.05/0.95 inference(miniscoping,[status(thm)],[f1])).
% 4.05/0.95 fof(f163,plain,(
% 4.05/0.95 ![X0,X1,X2]: (~subclass(X0,X1)|~member(X2,X0)|member(X2,X1))),
% 4.05/0.95 inference(cnf_transformation,[status(thm)],[f162])).
% 4.05/0.95 fof(f164,plain,(
% 4.05/0.95 ![X0,X1]: (member(not_subclass_element(X0,X1),X0)|subclass(X0,X1))),
% 4.05/0.95 inference(cnf_transformation,[status(thm)],[f2])).
% 4.05/0.95 fof(f165,plain,(
% 4.05/0.95 ![X0,X1]: (~member(not_subclass_element(X0,X1),X1)|subclass(X0,X1))),
% 4.05/0.95 inference(cnf_transformation,[status(thm)],[f3])).
% 4.05/0.95 fof(f166,plain,(
% 4.05/0.95 ![X0]: (subclass(X0,universal_class))),
% 4.05/0.95 inference(cnf_transformation,[status(thm)],[f4])).
% 4.05/0.95 fof(f169,plain,(
% 4.05/0.95 ![X0,X1]: (~subclass(X0,X1)|~subclass(X1,X0)|X0=X1)),
% 4.05/0.95 inference(cnf_transformation,[status(thm)],[f7])).
% 4.05/0.95 fof(f170,plain,(
% 4.05/0.95 ![U,Y]: ((![X]: (~member(U,unordered_pair(X,Y))|U=X))|U=Y)),
% 4.05/0.95 inference(miniscoping,[status(thm)],[f8])).
% 4.05/0.95 fof(f171,plain,(
% 4.05/0.95 ![X0,X1,X2]: (~member(X0,unordered_pair(X1,X2))|X0=X1|X0=X2)),
% 4.05/0.95 inference(cnf_transformation,[status(thm)],[f170])).
% 4.05/0.95 fof(f172,plain,(
% 4.05/0.95 ![X]: (~member(X,universal_class)|(![Y]: member(X,unordered_pair(X,Y))))),
% 4.05/0.95 inference(miniscoping,[status(thm)],[f9])).
% 4.05/0.95 fof(f173,plain,(
% 4.05/0.95 ![X0,X1]: (~member(X0,universal_class)|member(X0,unordered_pair(X0,X1)))),
% 4.05/0.95 inference(cnf_transformation,[status(thm)],[f172])).
% 4.05/0.95 fof(f177,plain,(
% 4.05/0.95 ![X0]: (unordered_pair(X0,X0)=singleton(X0))),
% 4.05/0.95 inference(cnf_transformation,[status(thm)],[f12])).
% 4.05/0.95 fof(f189,plain,(
% 4.05/0.95 ![Z,X]: ((![Y]: ~member(Z,intersection(X,Y)))|member(Z,X))),
% 4.05/0.95 inference(miniscoping,[status(thm)],[f21])).
% 4.05/0.95 fof(f190,plain,(
% 4.05/0.95 ![X0,X1,X2]: (~member(X0,intersection(X1,X2))|member(X0,X1))),
% 4.05/0.95 inference(cnf_transformation,[status(thm)],[f189])).
% 4.05/0.95 fof(f191,plain,(
% 4.05/0.95 ![Z,Y]: ((![X]: ~member(Z,intersection(X,Y)))|member(Z,Y))),
% 4.05/0.95 inference(miniscoping,[status(thm)],[f22])).
% 4.05/0.95 fof(f192,plain,(
% 4.05/0.95 ![X0,X1,X2]: (~member(X0,intersection(X1,X2))|member(X0,X2))),
% 4.05/0.95 inference(cnf_transformation,[status(thm)],[f191])).
% 4.05/0.95 fof(f193,plain,(
% 4.05/0.95 ![X0,X1,X2]: (~member(X0,X1)|~member(X0,X2)|member(X0,intersection(X1,X2)))),
% 4.05/0.95 inference(cnf_transformation,[status(thm)],[f23])).
% 4.05/0.95 fof(f194,plain,(
% 4.05/0.95 ![X0,X1]: (~member(X0,complement(X1))|~member(X0,X1))),
% 4.05/0.95 inference(cnf_transformation,[status(thm)],[f24])).
% 4.05/0.95 fof(f236,plain,(
% 4.05/0.95 ![X0]: (X0=null_class|member(regular(X0),X0))),
% 4.05/0.95 inference(cnf_transformation,[status(thm)],[f66])).
% 4.05/0.95 fof(f237,plain,(
% 4.05/0.95 ![X0]: (X0=null_class|intersection(X0,regular(X0))=null_class)),
% 4.05/0.95 inference(cnf_transformation,[status(thm)],[f67])).
% 4.05/0.95 fof(f351,plain,(
% 4.05/0.95 member(u,intersection(u,y))),
% 4.05/0.95 inference(cnf_transformation,[status(thm)],[f161])).
% 4.05/0.95 fof(f354,plain,(
% 4.05/0.95 member(u,u)),
% 4.05/0.95 inference(resolution,[status(thm)],[f190,f351])).
% 4.05/0.95 fof(f368,plain,(
% 4.05/0.95 ![X0]: (~member(u,X0)|member(u,intersection(X0,u)))),
% 4.05/0.95 inference(resolution,[status(thm)],[f193,f354])).
% 4.05/0.95 fof(f385,plain,(
% 4.05/0.95 ![X0,X1]: (~member(X0,X1)|member(X0,universal_class))),
% 4.05/0.95 inference(resolution,[status(thm)],[f163,f166])).
% 4.05/0.95 fof(f390,plain,(
% 4.05/0.95 ![X0]: (~subclass(u,X0)|member(u,X0))),
% 4.05/0.95 inference(resolution,[status(thm)],[f163,f354])).
% 4.05/0.95 fof(f395,plain,(
% 4.05/0.95 ![X0,X1,X2]: (subclass(intersection(X0,X1),X2)|member(not_subclass_element(intersection(X0,X1),X2),X1))),
% 4.05/0.95 inference(resolution,[status(thm)],[f164,f192])).
% 4.05/0.95 fof(f396,plain,(
% 4.05/0.95 ![X0,X1,X2]: (subclass(intersection(X0,X1),X2)|member(not_subclass_element(intersection(X0,X1),X2),X0))),
% 4.05/0.95 inference(resolution,[status(thm)],[f164,f190])).
% 4.05/0.95 fof(f418,plain,(
% 4.05/0.95 member(u,universal_class)),
% 4.05/0.95 inference(resolution,[status(thm)],[f390,f166])).
% 4.05/0.95 fof(f424,plain,(
% 4.05/0.95 ![X0]: (~member(u,X0)|member(u,intersection(universal_class,X0)))),
% 4.05/0.95 inference(resolution,[status(thm)],[f418,f193])).
% 4.05/0.95 fof(f478,plain,(
% 4.05/0.95 ![X0]: (X0=null_class|member(regular(X0),intersection(X0,X0)))),
% 4.05/0.95 inference(resolution,[status(thm)],[f236,f193])).
% 4.05/0.95 fof(f492,plain,(
% 4.05/0.95 ![X0,X1]: (~member(X0,singleton(X1))|X0=X1|X0=X1)),
% 4.05/0.95 inference(paramodulation,[status(thm)],[f177,f171])).
% 4.05/0.95 fof(f493,plain,(
% 4.05/0.95 ![X0,X1]: (~member(X0,singleton(X1))|X0=X1)),
% 4.05/0.95 inference(duplicate_literals_removal,[status(thm)],[f492])).
% 4.05/0.95 fof(f499,plain,(
% 4.05/0.95 ![X0]: (member(u,unordered_pair(u,X0)))),
% 4.05/0.95 inference(resolution,[status(thm)],[f173,f418])).
% 4.05/0.95 fof(f506,plain,(
% 4.05/0.95 member(u,singleton(u))),
% 4.05/0.95 inference(paramodulation,[status(thm)],[f177,f499])).
% 4.05/0.95 fof(f583,plain,(
% 4.05/0.95 ![X0]: (regular(singleton(X0))=X0|singleton(X0)=null_class)),
% 4.05/0.95 inference(resolution,[status(thm)],[f493,f236])).
% 4.05/0.95 fof(f593,plain,(
% 4.05/0.95 ![X0]: (member(regular(X0),universal_class)|X0=null_class)),
% 4.05/0.95 inference(resolution,[status(thm)],[f385,f478])).
% 4.05/0.95 fof(f790,plain,(
% 4.05/0.95 ![X0]: (~member(regular(complement(X0)),X0)|complement(X0)=null_class)),
% 4.05/0.95 inference(resolution,[status(thm)],[f194,f236])).
% 4.05/0.95 fof(f1325,plain,(
% 4.05/0.95 ![X0]: (singleton(X0)=null_class|intersection(singleton(X0),X0)=null_class|singleton(X0)=null_class)),
% 4.05/0.95 inference(paramodulation,[status(thm)],[f583,f237])).
% 4.05/0.95 fof(f1329,plain,(
% 4.05/0.95 ![X0]: (singleton(X0)=null_class|intersection(singleton(X0),X0)=null_class)),
% 4.05/0.95 inference(duplicate_literals_removal,[status(thm)],[f1325])).
% 4.05/0.95 fof(f1386,plain,(
% 4.05/0.95 member(u,intersection(singleton(u),u))),
% 4.05/0.95 inference(resolution,[status(thm)],[f368,f506])).
% 4.05/0.95 fof(f1625,plain,(
% 4.05/0.95 ![X0,X1]: (subclass(intersection(X0,X1),X1)|subclass(intersection(X0,X1),X1))),
% 4.05/0.95 inference(resolution,[status(thm)],[f395,f165])).
% 4.05/0.95 fof(f1667,plain,(
% 4.05/0.95 ![X0,X1]: (subclass(intersection(X0,X1),X1))),
% 4.05/0.95 inference(duplicate_literals_removal,[status(thm)],[f1625])).
% 4.05/0.95 fof(f1677,plain,(
% 4.05/0.95 ![X0,X1]: (subclass(intersection(X0,X1),X0)|subclass(intersection(X0,X1),X0))),
% 4.05/0.95 inference(resolution,[status(thm)],[f396,f165])).
% 4.05/0.95 fof(f1719,plain,(
% 4.05/0.95 ![X0,X1]: (subclass(intersection(X0,X1),X0))),
% 4.05/0.95 inference(duplicate_literals_removal,[status(thm)],[f1677])).
% 4.05/0.95 fof(f1753,plain,(
% 4.05/0.95 ![X0]: (subclass(null_class,X0)|X0=null_class)),
% 4.05/0.95 inference(paramodulation,[status(thm)],[f237,f1719])).
% 4.05/0.95 fof(f1767,plain,(
% 4.05/0.95 ![X0]: (X0=null_class|~subclass(X0,null_class)|X0=null_class)),
% 4.05/0.96 inference(resolution,[status(thm)],[f1753,f169])).
% 4.05/0.96 fof(f1771,plain,(
% 4.05/0.96 ![X0]: (X0=null_class|~subclass(X0,null_class))),
% 4.05/0.96 inference(duplicate_literals_removal,[status(thm)],[f1767])).
% 4.05/0.96 fof(f1775,plain,(
% 4.05/0.96 ![X0]: (intersection(null_class,X0)=null_class)),
% 4.05/0.96 inference(resolution,[status(thm)],[f1771,f1719])).
% 4.05/0.96 fof(f1776,plain,(
% 4.05/0.96 ![X0]: (intersection(X0,null_class)=null_class)),
% 4.05/0.96 inference(resolution,[status(thm)],[f1771,f1667])).
% 4.05/0.96 fof(f1790,plain,(
% 4.05/0.96 ![X0,X1]: (~member(X0,null_class)|member(X0,X1))),
% 4.05/0.96 inference(paramodulation,[status(thm)],[f1775,f192])).
% 4.05/0.96 fof(f5443,plain,(
% 4.05/0.96 member(u,intersection(universal_class,singleton(u)))),
% 4.05/0.96 inference(resolution,[status(thm)],[f424,f506])).
% 4.05/0.96 fof(f6202,plain,(
% 4.05/0.96 complement(universal_class)=null_class|complement(universal_class)=null_class),
% 4.05/0.96 inference(resolution,[status(thm)],[f790,f593])).
% 4.05/0.96 fof(f6212,plain,(
% 4.05/0.96 complement(universal_class)=null_class),
% 4.05/0.96 inference(duplicate_literals_removal,[status(thm)],[f6202])).
% 4.05/0.96 fof(f6230,plain,(
% 4.05/0.96 ![X0]: (~member(X0,null_class)|~member(X0,universal_class))),
% 4.05/0.96 inference(paramodulation,[status(thm)],[f6212,f194])).
% 4.05/0.96 fof(f6236,plain,(
% 4.05/0.96 ![X0]: (~member(X0,null_class))),
% 4.05/0.96 inference(forward_subsumption_resolution,[status(thm)],[f6230,f1790])).
% 4.05/0.96 fof(f6906,plain,(
% 4.05/0.96 member(u,null_class)|singleton(u)=null_class),
% 4.05/0.96 inference(paramodulation,[status(thm)],[f1329,f1386])).
% 4.05/0.96 fof(f6924,plain,(
% 4.05/0.96 singleton(u)=null_class),
% 4.05/0.96 inference(forward_subsumption_resolution,[status(thm)],[f6906,f6236])).
% 4.05/0.96 fof(f6930,plain,(
% 4.05/0.96 member(u,intersection(universal_class,null_class))),
% 4.05/0.96 inference(backward_demodulation,[status(thm)],[f6924,f5443])).
% 4.05/0.96 fof(f6970,plain,(
% 4.05/0.96 member(u,null_class)),
% 4.05/0.96 inference(forward_demodulation,[status(thm)],[f1776,f6930])).
% 4.05/0.96 fof(f6971,plain,(
% 4.05/0.96 $false),
% 4.05/0.96 inference(forward_subsumption_resolution,[status(thm)],[f6970,f6236])).
% 4.05/0.96 % SZS output end CNFRefutation for theBenchmark.p
% 4.05/0.98 % Elapsed time: 0.609508 seconds
% 4.05/0.98 % CPU time: 4.587309 seconds
% 4.05/0.98 % Total memory used: 185.450 MB
% 4.05/0.98 % Net memory used: 177.339 MB
%------------------------------------------------------------------------------