%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM051-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 : n004.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:12 PM UTC 2026
% Result : Unsatisfiable 69.70s 15.02s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM051-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/5.87 % Computer : n004.cluster.edu
% 0.18/5.87 % Model : x86_64 x86_64
% 0.18/5.87 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.87 % Memory : 8046.5625MB
% 0.18/5.87 % OS : Linux 6.8.0-71-generic
% 0.18/5.87 % CPULimit : 300
% 0.18/5.87 % WCLimit : 300
% 0.18/5.87 % DateTime : Mon Sep 21 02:00:58 UTC 2026
% 0.18/5.87 % CPUTime :
% 0.23/5.90 % Drodi V4.1.1
% 69.70/15.02 % Refutation found
% 69.70/15.02 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 69.70/15.02 % SZS output start CNFRefutation for theBenchmark
% 69.70/15.02 fof(f2,axiom,(
% 69.70/15.02 (![X,Y]: (( member(not_subclass_element(X,Y),X)| subclass(X,Y) ) ))),
% 69.70/15.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 69.70/15.02 fof(f3,axiom,(
% 69.70/15.02 (![X,Y]: (( ~ member(not_subclass_element(X,Y),Y)| subclass(X,Y) ) ))),
% 69.70/15.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 69.70/15.02 fof(f7,axiom,(
% 69.70/15.02 (![X,Y]: (( ~ subclass(X,Y)| ~ subclass(Y,X)| X = Y ) ))),
% 69.70/15.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 69.70/15.02 fof(f15,axiom,(
% 69.70/15.02 (![U,V,X,Y]: (( ~ member(ordered_pair(U,V),cross_product(X,Y))| member(V,Y) ) ))),
% 69.70/15.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 69.70/15.02 fof(f17,axiom,(
% 69.70/15.02 (![Z,X,Y]: (( ~ member(Z,cross_product(X,Y))| ordered_pair(first(Z),second(Z)) = Z ) ))),
% 69.70/15.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 69.70/15.02 fof(f21,axiom,(
% 69.70/15.02 (![Z,X,Y]: (( ~ member(Z,intersection(X,Y))| member(Z,X) ) ))),
% 69.70/15.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 69.70/15.02 fof(f28,axiom,(
% 69.70/15.02 (![Xr,X,Y]: (intersection(Xr,cross_product(X,Y)) = restrict(Xr,X,Y) ))),
% 69.70/15.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 69.70/15.02 fof(f30,axiom,(
% 69.70/15.02 (![X,Z]: (( restrict(X,singleton(Z),universal_class) != null_class| ~ member(Z,domain_of(X)) ) ))),
% 69.70/15.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 69.70/15.02 fof(f66,axiom,(
% 69.70/15.02 (![X]: (( X = null_class| member(regular(X),X) ) ))),
% 69.70/15.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 69.70/15.02 fof(f67,axiom,(
% 69.70/15.02 (![X]: (( X = null_class| intersection(X,regular(X)) = null_class ) ))),
% 69.70/15.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 69.70/15.02 fof(f117,axiom,(
% 69.70/15.02 (![Y,X]: (( ~ subclass(cross_product(Y,Y),union(identity_relation,symmetrization_of(X)))| connected(X,Y) ) ))),
% 69.70/15.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 69.70/15.02 fof(f159,negated_conjecture,(
% 69.70/15.02 ~ connected(x,null_class) ),
% 69.70/15.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 69.70/15.02 fof(f162,plain,(
% 69.70/15.02 ![X0,X1]: (member(not_subclass_element(X0,X1),X0)|subclass(X0,X1))),
% 69.70/15.02 inference(cnf_transformation,[status(thm)],[f2])).
% 69.70/15.02 fof(f163,plain,(
% 69.70/15.02 ![X0,X1]: (~member(not_subclass_element(X0,X1),X1)|subclass(X0,X1))),
% 69.70/15.02 inference(cnf_transformation,[status(thm)],[f3])).
% 69.70/15.02 fof(f167,plain,(
% 69.70/15.02 ![X0,X1]: (~subclass(X0,X1)|~subclass(X1,X0)|X0=X1)),
% 69.70/15.02 inference(cnf_transformation,[status(thm)],[f7])).
% 69.70/15.02 fof(f179,plain,(
% 69.70/15.02 ![V,Y]: ((![U,X]: ~member(ordered_pair(U,V),cross_product(X,Y)))|member(V,Y))),
% 69.70/15.02 inference(miniscoping,[status(thm)],[f15])).
% 69.70/15.02 fof(f180,plain,(
% 69.70/15.02 ![X0,X1,X2,X3]: (~member(ordered_pair(X0,X1),cross_product(X2,X3))|member(X1,X3))),
% 69.70/15.02 inference(cnf_transformation,[status(thm)],[f179])).
% 69.70/15.02 fof(f182,plain,(
% 69.70/15.02 ![Z]: ((![X,Y]: ~member(Z,cross_product(X,Y)))|ordered_pair(first(Z),second(Z))=Z)),
% 69.70/15.02 inference(miniscoping,[status(thm)],[f17])).
% 69.70/15.02 fof(f183,plain,(
% 69.70/15.02 ![X0,X1,X2]: (~member(X0,cross_product(X1,X2))|ordered_pair(first(X0),second(X0))=X0)),
% 69.70/15.02 inference(cnf_transformation,[status(thm)],[f182])).
% 69.70/15.02 fof(f187,plain,(
% 69.70/15.02 ![Z,X]: ((![Y]: ~member(Z,intersection(X,Y)))|member(Z,X))),
% 69.70/15.02 inference(miniscoping,[status(thm)],[f21])).
% 69.70/15.02 fof(f188,plain,(
% 69.70/15.02 ![X0,X1,X2]: (~member(X0,intersection(X1,X2))|member(X0,X1))),
% 69.70/15.02 inference(cnf_transformation,[status(thm)],[f187])).
% 69.70/15.02 fof(f196,plain,(
% 69.70/15.02 ![X0,X1,X2]: (intersection(X0,cross_product(X1,X2))=restrict(X0,X1,X2))),
% 69.70/15.02 inference(cnf_transformation,[status(thm)],[f28])).
% 69.70/15.02 fof(f198,plain,(
% 69.70/15.02 ![X0,X1]: (~restrict(X0,singleton(X1),universal_class)=null_class|~member(X1,domain_of(X0)))),
% 69.70/15.02 inference(cnf_transformation,[status(thm)],[f30])).
% 69.70/15.02 fof(f234,plain,(
% 69.70/15.02 ![X0]: (X0=null_class|member(regular(X0),X0))),
% 69.70/15.02 inference(cnf_transformation,[status(thm)],[f66])).
% 69.70/15.02 fof(f235,plain,(
% 69.70/15.02 ![X0]: (X0=null_class|intersection(X0,regular(X0))=null_class)),
% 69.70/15.02 inference(cnf_transformation,[status(thm)],[f67])).
% 69.70/15.02 fof(f295,plain,(
% 69.70/15.02 ![X0,X1]: (~subclass(cross_product(X0,X0),union(identity_relation,symmetrization_of(X1)))|connected(X1,X0))),
% 69.70/15.02 inference(cnf_transformation,[status(thm)],[f117])).
% 69.70/15.02 fof(f347,plain,(
% 69.70/15.02 ~connected(x,null_class)),
% 69.70/15.02 inference(cnf_transformation,[status(thm)],[f159])).
% 69.70/15.07 fof(f389,plain,(
% 69.70/15.07 ![X0,X1,X2]: (ordered_pair(first(not_subclass_element(cross_product(X0,X1),X2)),second(not_subclass_element(cross_product(X0,X1),X2)))=not_subclass_element(cross_product(X0,X1),X2)|subclass(cross_product(X0,X1),X2))),
% 69.70/15.07 inference(resolution,[status(thm)],[f183,f162])).
% 69.70/15.07 fof(f397,plain,(
% 69.70/15.07 ![X0,X1,X2]: (member(not_subclass_element(intersection(X0,X1),X2),X0)|subclass(intersection(X0,X1),X2))),
% 69.70/15.07 inference(resolution,[status(thm)],[f188,f162])).
% 69.70/15.07 fof(f949,plain,(
% 69.70/15.07 ![X0,X1]: (ordered_pair(first(not_subclass_element(cross_product(X0,X0),union(identity_relation,symmetrization_of(X1)))),second(not_subclass_element(cross_product(X0,X0),union(identity_relation,symmetrization_of(X1)))))=not_subclass_element(cross_product(X0,X0),union(identity_relation,symmetrization_of(X1)))|connected(X1,X0))),
% 69.70/15.07 inference(resolution,[status(thm)],[f389,f295])).
% 69.70/15.07 fof(f1009,plain,(
% 69.70/15.07 ![X0,X1]: (subclass(intersection(X0,X1),X0)|subclass(intersection(X0,X1),X0))),
% 69.70/15.07 inference(resolution,[status(thm)],[f397,f163])).
% 69.70/15.07 fof(f1038,plain,(
% 69.70/15.07 ![X0,X1]: (subclass(intersection(X0,X1),X0))),
% 69.70/15.07 inference(duplicate_literals_removal,[status(thm)],[f1009])).
% 69.70/15.07 fof(f1077,plain,(
% 69.70/15.07 ![X0]: (subclass(null_class,X0)|X0=null_class)),
% 69.70/15.07 inference(paramodulation,[status(thm)],[f235,f1038])).
% 69.70/15.07 fof(f1078,plain,(
% 69.70/15.07 ![X0,X1,X2]: (subclass(restrict(X0,X1,X2),X0))),
% 69.70/15.07 inference(paramodulation,[status(thm)],[f196,f1038])).
% 69.70/15.07 fof(f1351,plain,(
% 69.70/15.07 ![X0]: (X0=null_class|~subclass(X0,null_class)|X0=null_class)),
% 69.70/15.07 inference(resolution,[status(thm)],[f1077,f167])).
% 69.70/15.07 fof(f1352,plain,(
% 69.70/15.07 ![X0]: (X0=null_class|~subclass(X0,null_class))),
% 69.70/15.07 inference(duplicate_literals_removal,[status(thm)],[f1351])).
% 69.70/15.07 fof(f1578,plain,(
% 69.70/15.07 ![X0,X1]: (restrict(null_class,X0,X1)=null_class)),
% 69.70/15.07 inference(resolution,[status(thm)],[f1352,f1078])).
% 69.70/15.07 fof(f1715,plain,(
% 69.70/15.07 ![X0]: (~member(X0,domain_of(null_class)))),
% 69.70/15.07 inference(resolution,[status(thm)],[f1578,f198])).
% 69.70/15.07 fof(f1763,plain,(
% 69.70/15.07 domain_of(null_class)=null_class),
% 69.70/15.07 inference(resolution,[status(thm)],[f1715,f234])).
% 69.70/15.07 fof(f1770,plain,(
% 69.70/15.07 ![X0]: (~member(X0,null_class))),
% 69.70/15.07 inference(backward_demodulation,[status(thm)],[f1763,f1715])).
% 69.70/15.07 fof(f12267,plain,(
% 69.70/15.07 ordered_pair(first(not_subclass_element(cross_product(null_class,null_class),union(identity_relation,symmetrization_of(x)))),second(not_subclass_element(cross_product(null_class,null_class),union(identity_relation,symmetrization_of(x)))))=not_subclass_element(cross_product(null_class,null_class),union(identity_relation,symmetrization_of(x)))),
% 69.70/15.07 inference(resolution,[status(thm)],[f949,f347])).
% 69.70/15.07 fof(f12336,plain,(
% 69.70/15.07 ![X0,X1]: (~member(not_subclass_element(cross_product(null_class,null_class),union(identity_relation,symmetrization_of(x))),cross_product(X0,X1))|member(second(not_subclass_element(cross_product(null_class,null_class),union(identity_relation,symmetrization_of(x)))),X1))),
% 69.70/15.07 inference(paramodulation,[status(thm)],[f12267,f180])).
% 69.70/15.07 fof(f15217,plain,(
% 69.70/15.07 member(second(not_subclass_element(cross_product(null_class,null_class),union(identity_relation,symmetrization_of(x)))),null_class)|subclass(cross_product(null_class,null_class),union(identity_relation,symmetrization_of(x)))),
% 69.70/15.07 inference(resolution,[status(thm)],[f12336,f162])).
% 69.70/15.07 fof(f15219,plain,(
% 69.70/15.07 subclass(cross_product(null_class,null_class),union(identity_relation,symmetrization_of(x)))),
% 69.70/15.07 inference(forward_subsumption_resolution,[status(thm)],[f15217,f1770])).
% 69.70/15.07 fof(f15230,plain,(
% 69.70/15.07 connected(x,null_class)),
% 69.70/15.07 inference(resolution,[status(thm)],[f15219,f295])).
% 69.70/15.07 fof(f15236,plain,(
% 69.70/15.07 $false),
% 69.70/15.07 inference(forward_subsumption_resolution,[status(thm)],[f15230,f347])).
% 69.70/15.07 % SZS output end CNFRefutation for theBenchmark.p
% 4.78/15.11 % Elapsed time: 9.213679 seconds
% 4.78/15.11 % CPU time: 72.634969 seconds
% 4.78/15.11 % Total memory used: 577.384 MB
% 4.78/15.11 % Net memory used: 518.656 MB
%------------------------------------------------------------------------------