%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM217-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:22 PM UTC 2026
% Result : Unsatisfiable 9.07s 1.89s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM217-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n015.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 02:16:35 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.47 % Drodi V4.1.1
% 9.07/1.89 % Refutation found
% 9.07/1.89 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 9.07/1.89 % SZS output start CNFRefutation for theBenchmark
% 9.07/1.89 fof(f1,axiom,(
% 9.07/1.89 (![X,Y,U]: (( ~ subclass(X,Y)| ~ member(U,X)| member(U,Y) ) ))),
% 9.07/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.89 fof(f4,axiom,(
% 9.07/1.89 (![X]: (subclass(X,universal_class) ))),
% 9.07/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.89 fof(f17,axiom,(
% 9.07/1.89 (![Z,X,Y]: (( ~ member(Z,cross_product(X,Y))| ordered_pair(first(Z),second(Z)) = Z ) ))),
% 9.07/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.89 fof(f21,axiom,(
% 9.07/1.89 (![Z,X,Y]: (( ~ member(Z,intersection(X,Y))| member(Z,X) ) ))),
% 9.07/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.89 fof(f22,axiom,(
% 9.07/1.89 (![Z,X,Y]: (( ~ member(Z,intersection(X,Y))| member(Z,Y) ) ))),
% 9.07/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.89 fof(f24,axiom,(
% 9.07/1.89 (![Z,X]: (( ~ member(Z,complement(X))| ~ member(Z,X) ) ))),
% 9.07/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.89 fof(f28,axiom,(
% 9.07/1.89 (![Xr,X,Y]: (intersection(Xr,cross_product(X,Y)) = restrict(Xr,X,Y) ))),
% 9.07/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.89 fof(f30,axiom,(
% 9.07/1.89 (![X,Z]: (( restrict(X,singleton(Z),universal_class) != null_class| ~ member(Z,domain_of(X)) ) ))),
% 9.07/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.89 fof(f66,axiom,(
% 9.07/1.89 (![X]: (( X = null_class| member(regular(X),X) ) ))),
% 9.07/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.89 fof(f140,axiom,(
% 9.07/1.89 (![X]: (subclass(rest_of(X),cross_product(universal_class,universal_class)) ))),
% 9.07/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.89 fof(f141,axiom,(
% 9.07/1.89 (![U,V,X]: (( ~ member(ordered_pair(U,V),rest_of(X))| member(U,domain_of(X)) ) ))),
% 9.07/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.89 fof(f143,axiom,(
% 9.07/1.89 (![U,X,V]: (( ~ member(U,domain_of(X))| restrict(X,U,universal_class) != V| member(ordered_pair(U,V),rest_of(X)) ) ))),
% 9.07/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.89 fof(f159,negated_conjecture,(
% 9.07/1.89 rest_of(null_class) != null_class ),
% 9.07/1.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.89 fof(f160,plain,(
% 9.07/1.89 ![Y,U]: ((![X]: (~subclass(X,Y)|~member(U,X)))|member(U,Y))),
% 9.07/1.89 inference(miniscoping,[status(thm)],[f1])).
% 9.07/1.89 fof(f161,plain,(
% 9.07/1.89 ![X0,X1,X2]: (~subclass(X0,X1)|~member(X2,X0)|member(X2,X1))),
% 9.07/1.89 inference(cnf_transformation,[status(thm)],[f160])).
% 9.07/1.89 fof(f164,plain,(
% 9.07/1.89 ![X0]: (subclass(X0,universal_class))),
% 9.07/1.89 inference(cnf_transformation,[status(thm)],[f4])).
% 9.07/1.89 fof(f182,plain,(
% 9.07/1.89 ![Z]: ((![X,Y]: ~member(Z,cross_product(X,Y)))|ordered_pair(first(Z),second(Z))=Z)),
% 9.07/1.89 inference(miniscoping,[status(thm)],[f17])).
% 9.07/1.89 fof(f183,plain,(
% 9.07/1.89 ![X0,X1,X2]: (~member(X0,cross_product(X1,X2))|ordered_pair(first(X0),second(X0))=X0)),
% 9.07/1.89 inference(cnf_transformation,[status(thm)],[f182])).
% 9.07/1.89 fof(f187,plain,(
% 9.07/1.89 ![Z,X]: ((![Y]: ~member(Z,intersection(X,Y)))|member(Z,X))),
% 9.07/1.89 inference(miniscoping,[status(thm)],[f21])).
% 9.07/1.89 fof(f188,plain,(
% 9.07/1.89 ![X0,X1,X2]: (~member(X0,intersection(X1,X2))|member(X0,X1))),
% 9.07/1.89 inference(cnf_transformation,[status(thm)],[f187])).
% 9.07/1.90 fof(f189,plain,(
% 9.07/1.90 ![Z,Y]: ((![X]: ~member(Z,intersection(X,Y)))|member(Z,Y))),
% 9.07/1.90 inference(miniscoping,[status(thm)],[f22])).
% 9.07/1.90 fof(f190,plain,(
% 9.07/1.90 ![X0,X1,X2]: (~member(X0,intersection(X1,X2))|member(X0,X2))),
% 9.07/1.90 inference(cnf_transformation,[status(thm)],[f189])).
% 9.07/1.90 fof(f192,plain,(
% 9.07/1.90 ![X0,X1]: (~member(X0,complement(X1))|~member(X0,X1))),
% 9.07/1.90 inference(cnf_transformation,[status(thm)],[f24])).
% 9.07/1.90 fof(f196,plain,(
% 9.07/1.90 ![X0,X1,X2]: (intersection(X0,cross_product(X1,X2))=restrict(X0,X1,X2))),
% 9.07/1.90 inference(cnf_transformation,[status(thm)],[f28])).
% 9.07/1.90 fof(f198,plain,(
% 9.07/1.90 ![X0,X1]: (~restrict(X0,singleton(X1),universal_class)=null_class|~member(X1,domain_of(X0)))),
% 9.07/1.90 inference(cnf_transformation,[status(thm)],[f30])).
% 9.07/1.90 fof(f234,plain,(
% 9.07/1.90 ![X0]: (X0=null_class|member(regular(X0),X0))),
% 9.07/1.90 inference(cnf_transformation,[status(thm)],[f66])).
% 9.07/1.90 fof(f324,plain,(
% 9.07/1.90 ![X0]: (subclass(rest_of(X0),cross_product(universal_class,universal_class)))),
% 9.07/1.90 inference(cnf_transformation,[status(thm)],[f140])).
% 9.07/1.90 fof(f325,plain,(
% 9.07/1.90 ![U,X]: ((![V]: ~member(ordered_pair(U,V),rest_of(X)))|member(U,domain_of(X)))),
% 9.07/1.90 inference(miniscoping,[status(thm)],[f141])).
% 9.07/1.90 fof(f326,plain,(
% 9.07/1.90 ![X0,X1,X2]: (~member(ordered_pair(X0,X1),rest_of(X2))|member(X0,domain_of(X2)))),
% 9.07/1.90 inference(cnf_transformation,[status(thm)],[f325])).
% 9.07/1.90 fof(f328,plain,(
% 9.07/1.90 ![X0,X1,X2]: (~member(X0,domain_of(X1))|~restrict(X1,X0,universal_class)=X2|member(ordered_pair(X0,X2),rest_of(X1)))),
% 9.07/1.90 inference(cnf_transformation,[status(thm)],[f143])).
% 9.07/1.90 fof(f347,plain,(
% 9.07/1.90 ~rest_of(null_class)=null_class),
% 9.07/1.90 inference(cnf_transformation,[status(thm)],[f159])).
% 9.07/1.90 fof(f355,plain,(
% 9.07/1.90 ![X0,X1]: (~member(X0,domain_of(X1))|member(ordered_pair(X0,restrict(X1,X0,universal_class)),rest_of(X1)))),
% 9.07/1.90 inference(destructive_equality_resolution,[status(thm)],[f328])).
% 9.07/1.90 fof(f428,plain,(
% 9.07/1.90 ![X0]: (domain_of(X0)=null_class|member(ordered_pair(regular(domain_of(X0)),restrict(X0,regular(domain_of(X0)),universal_class)),rest_of(X0)))),
% 9.07/1.90 inference(resolution,[status(thm)],[f234,f355])).
% 9.07/1.90 fof(f429,plain,(
% 9.07/1.90 ![X0,X1]: (X0=null_class|~subclass(X0,X1)|member(regular(X0),X1))),
% 9.07/1.90 inference(resolution,[status(thm)],[f234,f161])).
% 9.07/1.90 fof(f464,plain,(
% 9.07/1.90 ![X0,X1]: (domain_of(X0)=null_class|~subclass(rest_of(X0),X1)|member(ordered_pair(regular(domain_of(X0)),restrict(X0,regular(domain_of(X0)),universal_class)),X1))),
% 9.07/1.90 inference(resolution,[status(thm)],[f428,f161])).
% 9.07/1.90 fof(f475,plain,(
% 9.07/1.90 ![X0]: (domain_of(X0)=null_class|member(ordered_pair(regular(domain_of(X0)),restrict(X0,regular(domain_of(X0)),universal_class)),cross_product(universal_class,universal_class)))),
% 9.07/1.90 inference(resolution,[status(thm)],[f464,f324])).
% 9.07/1.90 fof(f505,plain,(
% 9.07/1.90 ![X0]: (~member(regular(complement(X0)),X0)|complement(X0)=null_class)),
% 9.07/1.90 inference(resolution,[status(thm)],[f192,f234])).
% 9.07/1.90 fof(f521,plain,(
% 9.07/1.90 ![X0]: (ordered_pair(first(ordered_pair(regular(domain_of(X0)),restrict(X0,regular(domain_of(X0)),universal_class))),second(ordered_pair(regular(domain_of(X0)),restrict(X0,regular(domain_of(X0)),universal_class))))=ordered_pair(regular(domain_of(X0)),restrict(X0,regular(domain_of(X0)),universal_class))|domain_of(X0)=null_class)),
% 9.07/1.90 inference(resolution,[status(thm)],[f183,f475])).
% 9.07/1.90 fof(f544,plain,(
% 9.07/1.90 ![X0,X1]: (~member(ordered_pair(regular(domain_of(X0)),restrict(X0,regular(domain_of(X0)),universal_class)),rest_of(X1))|member(first(ordered_pair(regular(domain_of(X0)),restrict(X0,regular(domain_of(X0)),universal_class))),domain_of(X1))|domain_of(X0)=null_class)),
% 9.07/1.90 inference(paramodulation,[status(thm)],[f521,f326])).
% 9.07/1.90 fof(f644,plain,(
% 9.07/1.90 ![X0,X1]: (member(regular(intersection(X0,X1)),X0)|intersection(X0,X1)=null_class)),
% 9.07/1.90 inference(resolution,[status(thm)],[f188,f234])).
% 9.07/1.90 fof(f953,plain,(
% 9.07/1.90 ![X0]: (member(first(ordered_pair(regular(domain_of(X0)),restrict(X0,regular(domain_of(X0)),universal_class))),domain_of(X0))|domain_of(X0)=null_class|domain_of(X0)=null_class)),
% 9.07/1.90 inference(resolution,[status(thm)],[f544,f428])).
% 9.07/1.90 fof(f956,plain,(
% 9.07/1.90 ![X0]: (member(first(ordered_pair(regular(domain_of(X0)),restrict(X0,regular(domain_of(X0)),universal_class))),domain_of(X0))|domain_of(X0)=null_class)),
% 9.07/1.90 inference(duplicate_literals_removal,[status(thm)],[f953])).
% 9.07/1.90 fof(f1934,plain,(
% 9.07/1.90 ![X0]: (rest_of(X0)=null_class|member(regular(rest_of(X0)),cross_product(universal_class,universal_class)))),
% 9.07/1.90 inference(resolution,[status(thm)],[f429,f324])).
% 9.07/1.90 fof(f1935,plain,(
% 9.07/1.90 ![X0]: (X0=null_class|member(regular(X0),universal_class))),
% 9.07/1.90 inference(resolution,[status(thm)],[f429,f164])).
% 9.07/1.90 fof(f1999,plain,(
% 9.07/1.90 complement(universal_class)=null_class|complement(universal_class)=null_class),
% 9.07/1.90 inference(resolution,[status(thm)],[f505,f1935])).
% 9.07/1.90 fof(f2008,plain,(
% 9.07/1.90 complement(universal_class)=null_class),
% 9.07/1.90 inference(duplicate_literals_removal,[status(thm)],[f1999])).
% 9.07/1.90 fof(f2019,plain,(
% 9.07/1.90 ![X0]: (~member(X0,null_class)|~member(X0,universal_class))),
% 9.07/1.90 inference(paramodulation,[status(thm)],[f2008,f192])).
% 9.07/1.90 fof(f2025,plain,(
% 9.07/1.90 ![X0]: (rest_of(X0)=null_class|ordered_pair(first(regular(rest_of(X0))),second(regular(rest_of(X0))))=regular(rest_of(X0)))),
% 9.07/1.90 inference(resolution,[status(thm)],[f1934,f183])).
% 9.07/1.90 fof(f2060,plain,(
% 9.07/1.90 ![X0,X1]: (~member(regular(rest_of(X0)),rest_of(X1))|member(first(regular(rest_of(X0))),domain_of(X1))|rest_of(X0)=null_class)),
% 9.07/1.94 inference(paramodulation,[status(thm)],[f2025,f326])).
% 9.07/1.94 fof(f2426,plain,(
% 9.07/1.94 ![X0]: (member(first(regular(rest_of(X0))),domain_of(X0))|rest_of(X0)=null_class|rest_of(X0)=null_class)),
% 9.07/1.94 inference(resolution,[status(thm)],[f2060,f234])).
% 9.07/1.94 fof(f2427,plain,(
% 9.07/1.94 ![X0]: (member(first(regular(rest_of(X0))),domain_of(X0))|rest_of(X0)=null_class)),
% 9.07/1.94 inference(duplicate_literals_removal,[status(thm)],[f2426])).
% 9.07/1.94 fof(f3562,plain,(
% 9.07/1.94 ![X0]: (intersection(null_class,X0)=null_class|~member(regular(intersection(null_class,X0)),universal_class))),
% 9.07/1.94 inference(resolution,[status(thm)],[f644,f2019])).
% 9.07/1.94 fof(f3617,plain,(
% 9.07/1.94 ![X0]: (intersection(null_class,X0)=null_class)),
% 9.07/1.94 inference(forward_subsumption_resolution,[status(thm)],[f3562,f1935])).
% 9.07/1.94 fof(f3649,plain,(
% 9.07/1.94 ![X0,X1]: (restrict(null_class,X0,X1)=null_class)),
% 9.07/1.94 inference(paramodulation,[status(thm)],[f196,f3617])).
% 9.07/1.94 fof(f3657,plain,(
% 9.07/1.94 ![X0,X1]: (~member(X0,null_class)|member(X0,X1))),
% 9.07/1.94 inference(paramodulation,[status(thm)],[f3617,f190])).
% 9.07/1.94 fof(f3662,plain,(
% 9.07/1.94 ![X0]: (~member(X0,null_class))),
% 9.07/1.94 inference(backward_subsumption_resolution,[status(thm)],[f2019,f3657])).
% 9.07/1.94 fof(f3795,plain,(
% 9.07/1.94 ![X0]: (~member(X0,domain_of(null_class)))),
% 9.07/1.94 inference(resolution,[status(thm)],[f3649,f198])).
% 9.07/1.94 fof(f3798,plain,(
% 9.07/1.94 member(first(ordered_pair(regular(domain_of(null_class)),null_class)),domain_of(null_class))|domain_of(null_class)=null_class),
% 9.07/1.94 inference(paramodulation,[status(thm)],[f3649,f956])).
% 9.07/1.94 fof(f3858,plain,(
% 9.07/1.94 domain_of(null_class)=null_class),
% 9.07/1.94 inference(forward_subsumption_resolution,[status(thm)],[f3798,f3795])).
% 9.07/1.94 fof(f3979,plain,(
% 9.07/1.94 member(first(regular(rest_of(null_class))),null_class)|rest_of(null_class)=null_class),
% 9.07/1.94 inference(paramodulation,[status(thm)],[f3858,f2427])).
% 9.07/1.94 fof(f4055,plain,(
% 9.07/1.94 ~null_class=null_class),
% 9.07/1.94 inference(backward_demodulation,[status(thm)],[f4057,f347])).
% 9.07/1.94 fof(f4057,plain,(
% 9.07/1.94 rest_of(null_class)=null_class),
% 9.07/1.94 inference(forward_subsumption_resolution,[status(thm)],[f3979,f3662])).
% 9.07/1.95 fof(f4223,plain,(
% 9.07/1.95 $false),
% 9.07/1.95 inference(trivial_equality_resolution,[status(thm)],[f4055])).
% 9.07/1.95 % SZS output end CNFRefutation for theBenchmark.p
% 9.07/1.96 % Elapsed time: 1.500448 seconds
% 9.07/1.96 % CPU time: 11.354561 seconds
% 9.07/1.96 % Total memory used: 242.691 MB
% 9.07/1.96 % Net memory used: 228.338 MB
%------------------------------------------------------------------------------