%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET347-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 : n017.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:56 PM UTC 2026
% Result : Unsatisfiable 196.84s 25.24s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET347-6 : 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.09/0.37 % Computer : n017.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 05:05:44 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 196.84/25.24 % Refutation found
% 196.84/25.24 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 196.84/25.24 % SZS output start CNFRefutation for theBenchmark
% 196.84/25.24 fof(f1,axiom,(
% 196.84/25.24 (![X,Y,U]: (( ~ subclass(X,Y)| ~ member(U,X)| member(U,Y) ) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f2,axiom,(
% 196.84/25.24 (![X,Y]: (( member(not_subclass_element(X,Y),X)| subclass(X,Y) ) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f3,axiom,(
% 196.84/25.24 (![X,Y]: (( ~ member(not_subclass_element(X,Y),Y)| subclass(X,Y) ) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f4,axiom,(
% 196.84/25.24 (![X]: (subclass(X,universal_class) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f7,axiom,(
% 196.84/25.24 (![X,Y]: (( ~ subclass(X,Y)| ~ subclass(Y,X)| X = Y ) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f8,axiom,(
% 196.84/25.24 (![U,X,Y]: (( ~ member(U,unordered_pair(X,Y))| U = X| U = Y ) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f12,axiom,(
% 196.84/25.24 (![X]: (unordered_pair(X,X) = singleton(X) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f15,axiom,(
% 196.84/25.24 (![U,V,X,Y]: (( ~ member(ordered_pair(U,V),cross_product(X,Y))| member(V,Y) ) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f17,axiom,(
% 196.84/25.24 (![Z,X,Y]: (( ~ member(Z,cross_product(X,Y))| ordered_pair(first(Z),second(Z)) = Z ) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f21,axiom,(
% 196.84/25.24 (![Z,X,Y]: (( ~ member(Z,intersection(X,Y))| member(Z,X) ) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f22,axiom,(
% 196.84/25.24 (![Z,X,Y]: (( ~ member(Z,intersection(X,Y))| member(Z,Y) ) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f23,axiom,(
% 196.84/25.24 (![Z,X,Y]: (( ~ member(Z,X)| ~ member(Z,Y)| member(Z,intersection(X,Y)) ) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f24,axiom,(
% 196.84/25.24 (![Z,X]: (( ~ member(Z,complement(X))| ~ member(Z,X) ) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f25,axiom,(
% 196.84/25.24 (![Z,X]: (( ~ member(Z,universal_class)| member(Z,complement(X))| member(Z,X) ) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f28,axiom,(
% 196.84/25.24 (![Xr,X,Y]: (intersection(Xr,cross_product(X,Y)) = restrict(Xr,X,Y) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f29,axiom,(
% 196.84/25.24 (![X,Y,Xr]: (intersection(cross_product(X,Y),Xr) = restrict(Xr,X,Y) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f30,axiom,(
% 196.84/25.24 (![X,Z]: (( restrict(X,singleton(Z),universal_class) != null_class| ~ member(Z,domain_of(X)) ) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f53,axiom,(
% 196.84/25.24 (![X]: (domain_of(restrict(element_relation,universal_class,X)) = sum_class(X) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f66,axiom,(
% 196.84/25.24 (![X]: (( X = null_class| member(regular(X),X) ) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f67,axiom,(
% 196.84/25.24 (![X]: (( X = null_class| intersection(X,regular(X)) = null_class ) ))),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f113,negated_conjecture,(
% 196.84/25.24 sum_class(null_class) != null_class ),
% 196.84/25.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.84/25.24 fof(f114,plain,(
% 196.84/25.24 ![Y,U]: ((![X]: (~subclass(X,Y)|~member(U,X)))|member(U,Y))),
% 196.84/25.24 inference(miniscoping,[status(thm)],[f1])).
% 196.84/25.24 fof(f115,plain,(
% 196.84/25.24 ![X0,X1,X2]: (~subclass(X0,X1)|~member(X2,X0)|member(X2,X1))),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f114])).
% 196.84/25.24 fof(f116,plain,(
% 196.84/25.24 ![X0,X1]: (member(not_subclass_element(X0,X1),X0)|subclass(X0,X1))),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f2])).
% 196.84/25.24 fof(f117,plain,(
% 196.84/25.24 ![X0,X1]: (~member(not_subclass_element(X0,X1),X1)|subclass(X0,X1))),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f3])).
% 196.84/25.24 fof(f118,plain,(
% 196.84/25.24 ![X0]: (subclass(X0,universal_class))),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f4])).
% 196.84/25.24 fof(f121,plain,(
% 196.84/25.24 ![X0,X1]: (~subclass(X0,X1)|~subclass(X1,X0)|X0=X1)),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f7])).
% 196.84/25.24 fof(f122,plain,(
% 196.84/25.24 ![U,Y]: ((![X]: (~member(U,unordered_pair(X,Y))|U=X))|U=Y)),
% 196.84/25.24 inference(miniscoping,[status(thm)],[f8])).
% 196.84/25.24 fof(f123,plain,(
% 196.84/25.24 ![X0,X1,X2]: (~member(X0,unordered_pair(X1,X2))|X0=X1|X0=X2)),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f122])).
% 196.84/25.24 fof(f129,plain,(
% 196.84/25.24 ![X0]: (unordered_pair(X0,X0)=singleton(X0))),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f12])).
% 196.84/25.24 fof(f133,plain,(
% 196.84/25.24 ![V,Y]: ((![U,X]: ~member(ordered_pair(U,V),cross_product(X,Y)))|member(V,Y))),
% 196.84/25.24 inference(miniscoping,[status(thm)],[f15])).
% 196.84/25.24 fof(f134,plain,(
% 196.84/25.24 ![X0,X1,X2,X3]: (~member(ordered_pair(X0,X1),cross_product(X2,X3))|member(X1,X3))),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f133])).
% 196.84/25.24 fof(f136,plain,(
% 196.84/25.24 ![Z]: ((![X,Y]: ~member(Z,cross_product(X,Y)))|ordered_pair(first(Z),second(Z))=Z)),
% 196.84/25.24 inference(miniscoping,[status(thm)],[f17])).
% 196.84/25.24 fof(f137,plain,(
% 196.84/25.24 ![X0,X1,X2]: (~member(X0,cross_product(X1,X2))|ordered_pair(first(X0),second(X0))=X0)),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f136])).
% 196.84/25.24 fof(f141,plain,(
% 196.84/25.24 ![Z,X]: ((![Y]: ~member(Z,intersection(X,Y)))|member(Z,X))),
% 196.84/25.24 inference(miniscoping,[status(thm)],[f21])).
% 196.84/25.24 fof(f142,plain,(
% 196.84/25.24 ![X0,X1,X2]: (~member(X0,intersection(X1,X2))|member(X0,X1))),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f141])).
% 196.84/25.24 fof(f143,plain,(
% 196.84/25.24 ![Z,Y]: ((![X]: ~member(Z,intersection(X,Y)))|member(Z,Y))),
% 196.84/25.24 inference(miniscoping,[status(thm)],[f22])).
% 196.84/25.24 fof(f144,plain,(
% 196.84/25.24 ![X0,X1,X2]: (~member(X0,intersection(X1,X2))|member(X0,X2))),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f143])).
% 196.84/25.24 fof(f145,plain,(
% 196.84/25.24 ![X0,X1,X2]: (~member(X0,X1)|~member(X0,X2)|member(X0,intersection(X1,X2)))),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f23])).
% 196.84/25.24 fof(f146,plain,(
% 196.84/25.24 ![X0,X1]: (~member(X0,complement(X1))|~member(X0,X1))),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f24])).
% 196.84/25.24 fof(f147,plain,(
% 196.84/25.24 ![X0,X1]: (~member(X0,universal_class)|member(X0,complement(X1))|member(X0,X1))),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f25])).
% 196.84/25.24 fof(f150,plain,(
% 196.84/25.24 ![X0,X1,X2]: (intersection(X0,cross_product(X1,X2))=restrict(X0,X1,X2))),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f28])).
% 196.84/25.24 fof(f151,plain,(
% 196.84/25.24 ![X0,X1,X2]: (intersection(cross_product(X0,X1),X2)=restrict(X2,X0,X1))),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f29])).
% 196.84/25.24 fof(f152,plain,(
% 196.84/25.24 ![X0,X1]: (~restrict(X0,singleton(X1),universal_class)=null_class|~member(X1,domain_of(X0)))),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f30])).
% 196.84/25.24 fof(f175,plain,(
% 196.84/25.24 ![X0]: (domain_of(restrict(element_relation,universal_class,X0))=sum_class(X0))),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f53])).
% 196.84/25.24 fof(f188,plain,(
% 196.84/25.24 ![X0]: (X0=null_class|member(regular(X0),X0))),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f66])).
% 196.84/25.24 fof(f189,plain,(
% 196.84/25.24 ![X0]: (X0=null_class|intersection(X0,regular(X0))=null_class)),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f67])).
% 196.84/25.24 fof(f245,plain,(
% 196.84/25.24 ~sum_class(null_class)=null_class),
% 196.84/25.24 inference(cnf_transformation,[status(thm)],[f113])).
% 196.84/25.24 fof(f251,plain,(
% 196.84/25.24 ![X0,X1]: (~member(X0,X1)|member(X0,universal_class))),
% 196.84/25.24 inference(resolution,[status(thm)],[f118,f115])).
% 196.84/25.24 fof(f262,plain,(
% 196.84/25.24 ![X0]: (~subclass(universal_class,X0)|universal_class=X0)),
% 196.84/25.24 inference(resolution,[status(thm)],[f121,f118])).
% 196.84/25.24 fof(f349,plain,(
% 196.84/25.24 ![X0,X1]: (regular(unordered_pair(X0,X1))=X0|regular(unordered_pair(X0,X1))=X1|unordered_pair(X0,X1)=null_class)),
% 196.84/25.24 inference(resolution,[status(thm)],[f123,f188])).
% 196.84/25.24 fof(f367,plain,(
% 196.84/25.24 ![X0,X1]: (~member(X0,singleton(X1))|X0=X1|X0=X1)),
% 196.84/25.24 inference(paramodulation,[status(thm)],[f129,f123])).
% 196.84/25.24 fof(f368,plain,(
% 196.84/25.24 ![X0,X1]: (~member(X0,singleton(X1))|X0=X1)),
% 196.84/25.24 inference(duplicate_literals_removal,[status(thm)],[f367])).
% 196.84/25.24 fof(f369,plain,(
% 196.84/25.24 ![X0,X1]: (member(not_subclass_element(universal_class,X0),complement(X1))|member(not_subclass_element(universal_class,X0),X1)|subclass(universal_class,X0))),
% 196.84/25.24 inference(resolution,[status(thm)],[f147,f116])).
% 196.84/25.24 fof(f455,plain,(
% 196.84/25.24 ![X0]: (regular(singleton(X0))=X0|regular(unordered_pair(X0,X0))=X0|unordered_pair(X0,X0)=null_class)),
% 196.84/25.24 inference(paramodulation,[status(thm)],[f129,f349])).
% 196.84/25.24 fof(f460,plain,(
% 196.84/25.24 ![X0]: (regular(singleton(X0))=X0|regular(singleton(X0))=X0|unordered_pair(X0,X0)=null_class)),
% 196.84/25.24 inference(forward_demodulation,[status(thm)],[f129,f455])).
% 196.84/25.24 fof(f461,plain,(
% 196.84/25.24 ![X0]: (regular(singleton(X0))=X0|regular(singleton(X0))=X0|singleton(X0)=null_class)),
% 196.84/25.24 inference(forward_demodulation,[status(thm)],[f129,f460])).
% 196.84/25.24 fof(f462,plain,(
% 196.84/25.24 ![X0]: (regular(singleton(X0))=X0|singleton(X0)=null_class)),
% 196.84/25.24 inference(duplicate_literals_removal,[status(thm)],[f461])).
% 196.84/25.24 fof(f468,plain,(
% 196.84/25.24 ![X0]: (singleton(X0)=null_class|intersection(singleton(X0),X0)=null_class|singleton(X0)=null_class)),
% 196.84/25.24 inference(paramodulation,[status(thm)],[f462,f189])).
% 196.84/25.24 fof(f470,plain,(
% 196.84/25.24 ![X0]: (singleton(X0)=null_class|intersection(singleton(X0),X0)=null_class)),
% 196.84/25.24 inference(duplicate_literals_removal,[status(thm)],[f468])).
% 196.84/25.24 fof(f609,plain,(
% 196.84/25.24 ![X0]: (member(not_subclass_element(universal_class,complement(X0)),X0)|subclass(universal_class,complement(X0))|subclass(universal_class,complement(X0)))),
% 196.84/25.24 inference(resolution,[status(thm)],[f369,f117])).
% 196.84/25.24 fof(f610,plain,(
% 196.84/25.24 ![X0]: (member(not_subclass_element(universal_class,complement(X0)),X0)|subclass(universal_class,complement(X0)))),
% 196.84/25.24 inference(duplicate_literals_removal,[status(thm)],[f609])).
% 196.84/25.24 fof(f738,plain,(
% 196.84/25.24 ![X0]: (member(regular(X0),universal_class)|X0=null_class)),
% 196.84/25.24 inference(resolution,[status(thm)],[f251,f188])).
% 196.84/25.24 fof(f1801,plain,(
% 196.84/25.24 ![X0,X1,X2]: (member(not_subclass_element(intersection(X0,X1),X2),X0)|subclass(intersection(X0,X1),X2))),
% 196.84/25.24 inference(resolution,[status(thm)],[f142,f116])).
% 196.84/25.24 fof(f1811,plain,(
% 196.84/25.24 ![X0,X1]: (~member(X0,null_class)|member(X0,X1)|X1=null_class)),
% 196.84/25.24 inference(paramodulation,[status(thm)],[f189,f142])).
% 196.84/25.24 fof(f2045,plain,(
% 196.84/25.24 ![X0,X1]: (ordered_pair(first(regular(cross_product(X0,X1))),second(regular(cross_product(X0,X1))))=regular(cross_product(X0,X1))|cross_product(X0,X1)=null_class)),
% 196.84/25.24 inference(resolution,[status(thm)],[f137,f188])).
% 196.84/25.24 fof(f3095,plain,(
% 196.84/25.24 ![X0,X1]: (member(not_subclass_element(null_class,X0),X1)|X1=null_class|subclass(null_class,X0))),
% 196.84/25.24 inference(resolution,[status(thm)],[f1811,f116])).
% 196.84/25.24 fof(f3162,plain,(
% 196.84/25.24 ![X0]: (X0=null_class|subclass(null_class,X0)|subclass(null_class,X0))),
% 196.84/25.24 inference(resolution,[status(thm)],[f3095,f117])).
% 196.84/25.24 fof(f3182,plain,(
% 196.84/25.24 ![X0]: (X0=null_class|subclass(null_class,X0))),
% 196.84/25.24 inference(duplicate_literals_removal,[status(thm)],[f3162])).
% 196.84/25.24 fof(f3185,plain,(
% 196.84/25.24 ![X0]: (X0=null_class|~subclass(X0,null_class)|X0=null_class)),
% 196.84/25.24 inference(resolution,[status(thm)],[f3182,f121])).
% 196.84/25.24 fof(f3189,plain,(
% 196.84/25.24 ![X0]: (X0=null_class|~subclass(X0,null_class))),
% 196.84/25.24 inference(duplicate_literals_removal,[status(thm)],[f3185])).
% 196.84/25.24 fof(f3240,plain,(
% 196.84/25.24 ![X0,X1]: (subclass(intersection(X0,X1),X0)|subclass(intersection(X0,X1),X0))),
% 196.84/25.24 inference(resolution,[status(thm)],[f1801,f117])).
% 196.84/25.24 fof(f3264,plain,(
% 196.84/25.24 ![X0,X1]: (subclass(intersection(X0,X1),X0))),
% 196.84/25.24 inference(duplicate_literals_removal,[status(thm)],[f3240])).
% 196.84/25.24 fof(f4591,plain,(
% 196.84/25.24 ![X0,X1,X2,X3]: (~member(regular(cross_product(X0,X1)),cross_product(X2,X3))|member(second(regular(cross_product(X0,X1))),X3)|cross_product(X0,X1)=null_class)),
% 196.84/25.24 inference(paramodulation,[status(thm)],[f2045,f134])).
% 196.84/25.24 fof(f5701,plain,(
% 196.84/25.24 ![X0]: (intersection(null_class,X0)=null_class)),
% 196.84/25.24 inference(resolution,[status(thm)],[f3189,f3264])).
% 196.84/25.24 fof(f5764,plain,(
% 196.84/25.24 ![X0,X1]: (~member(X0,null_class)|member(X0,X1))),
% 196.84/25.24 inference(paramodulation,[status(thm)],[f5701,f144])).
% 196.84/25.24 fof(f5894,plain,(
% 196.84/25.24 ![X0,X1]: (~member(regular(X0),X1)|member(regular(X0),intersection(X0,X1))|X0=null_class)),
% 196.84/25.24 inference(resolution,[status(thm)],[f145,f188])).
% 196.84/25.24 fof(f7905,plain,(
% 196.84/25.24 ![X0]: (member(regular(X0),intersection(X0,universal_class))|X0=null_class|X0=null_class)),
% 196.84/25.24 inference(resolution,[status(thm)],[f5894,f738])).
% 196.84/25.24 fof(f7947,plain,(
% 196.84/25.24 ![X0]: (member(regular(X0),intersection(X0,universal_class))|X0=null_class)),
% 196.84/25.24 inference(duplicate_literals_removal,[status(thm)],[f7905])).
% 196.84/25.24 fof(f11811,plain,(
% 196.84/25.24 ![X0,X1]: (null_class=restrict(null_class,X0,X1))),
% 196.84/25.24 inference(paramodulation,[status(thm)],[f5701,f150])).
% 196.84/25.24 fof(f13648,plain,(
% 196.84/25.24 member(regular(singleton(universal_class)),null_class)|singleton(universal_class)=null_class|singleton(universal_class)=null_class),
% 196.84/25.24 inference(paramodulation,[status(thm)],[f470,f7947])).
% 196.84/25.24 fof(f13655,plain,(
% 196.84/25.24 member(regular(singleton(universal_class)),null_class)|singleton(universal_class)=null_class),
% 196.84/25.24 inference(duplicate_literals_removal,[status(thm)],[f13648])).
% 196.84/25.24 fof(f14006,plain,(
% 196.84/25.24 ![X0]: (singleton(universal_class)=null_class|member(regular(singleton(universal_class)),X0))),
% 196.84/25.24 inference(resolution,[status(thm)],[f13655,f5764])).
% 196.84/25.24 fof(f14043,plain,(
% 196.84/25.24 ![X0]: (singleton(universal_class)=null_class|regular(singleton(universal_class))=X0)),
% 196.84/25.24 inference(resolution,[status(thm)],[f14006,f368])).
% 196.84/25.24 fof(f14268,plain,(
% 196.84/25.24 ![X0,X1]: (singleton(universal_class)=null_class|X0=X1|singleton(universal_class)=null_class)),
% 196.84/25.24 inference(paramodulation,[status(thm)],[f14043,f14043])).
% 196.84/25.24 fof(f14332,plain,(
% 196.84/25.24 ![X0,X1]: (singleton(universal_class)=null_class|X0=X1)),
% 196.84/25.24 inference(duplicate_literals_removal,[status(thm)],[f14268])).
% 196.84/25.24 fof(f14395,plain,(
% 196.84/25.24 singleton(universal_class)=null_class),
% 196.84/25.24 inference(resolution,[status(thm)],[f14332,f245])).
% 196.84/25.24 fof(f16855,plain,(
% 196.84/25.24 ![X0]: (~member(X0,null_class)|X0=universal_class)),
% 196.84/25.24 inference(paramodulation,[status(thm)],[f14395,f368])).
% 196.84/25.24 fof(f16928,plain,(
% 196.84/25.24 not_subclass_element(universal_class,complement(null_class))=universal_class|subclass(universal_class,complement(null_class))),
% 196.84/25.24 inference(resolution,[status(thm)],[f16855,f610])).
% 196.84/25.24 fof(f17296,plain,(
% 196.84/25.24 ![X0]: (~member(X0,domain_of(null_class)))),
% 196.84/25.24 inference(resolution,[status(thm)],[f152,f11811])).
% 196.84/25.24 fof(f17349,plain,(
% 196.84/25.24 not_subclass_element(universal_class,complement(null_class))=universal_class|universal_class=complement(null_class)),
% 196.84/25.24 inference(resolution,[status(thm)],[f16928,f262])).
% 196.84/25.24 fof(f17353,plain,(
% 196.84/25.24 member(universal_class,null_class)|subclass(universal_class,complement(null_class))|universal_class=complement(null_class)),
% 196.84/25.24 inference(paramodulation,[status(thm)],[f17349,f610])).
% 196.84/25.24 fof(f17410,plain,(
% 196.84/25.24 member(universal_class,null_class)|universal_class=complement(null_class)),
% 196.84/25.24 inference(forward_subsumption_resolution,[status(thm)],[f17353,f262])).
% 196.84/25.24 fof(f17468,plain,(
% 196.84/25.24 ![X0]: (universal_class=complement(null_class)|member(universal_class,X0))),
% 196.84/25.24 inference(resolution,[status(thm)],[f17410,f5764])).
% 196.84/25.24 fof(f17503,plain,(
% 196.84/25.24 ![X0]: (universal_class=complement(null_class)|~member(universal_class,X0))),
% 196.84/25.24 inference(resolution,[status(thm)],[f17468,f146])).
% 196.84/25.24 fof(f17539,plain,(
% 196.84/25.24 universal_class=complement(null_class)),
% 196.84/25.24 inference(forward_subsumption_resolution,[status(thm)],[f17503,f17468])).
% 196.84/25.24 fof(f21007,plain,(
% 196.84/25.24 ![X0]: (~member(X0,universal_class)|~member(X0,null_class))),
% 196.84/25.24 inference(paramodulation,[status(thm)],[f17539,f146])).
% 196.84/25.24 fof(f21035,plain,(
% 196.84/25.24 ![X0]: (~member(X0,null_class))),
% 196.84/25.24 inference(forward_subsumption_resolution,[status(thm)],[f21007,f251])).
% 196.84/25.24 fof(f21347,plain,(
% 196.84/25.24 domain_of(null_class)=null_class),
% 196.84/25.24 inference(resolution,[status(thm)],[f17296,f188])).
% 196.84/25.24 fof(f53735,plain,(
% 196.84/25.24 ![X0,X1]: (member(second(regular(cross_product(X0,X1))),X1)|cross_product(X0,X1)=null_class|cross_product(X0,X1)=null_class)),
% 196.84/25.24 inference(resolution,[status(thm)],[f4591,f188])).
% 196.84/25.24 fof(f53756,plain,(
% 196.84/25.24 ![X0,X1]: (member(second(regular(cross_product(X0,X1))),X1)|cross_product(X0,X1)=null_class)),
% 196.84/25.24 inference(duplicate_literals_removal,[status(thm)],[f53735])).
% 196.84/25.24 fof(f59964,plain,(
% 196.84/25.24 ![X0]: (cross_product(X0,null_class)=null_class)),
% 196.84/25.24 inference(resolution,[status(thm)],[f53756,f21035])).
% 196.84/25.24 fof(f63831,plain,(
% 196.84/25.24 ![X0,X1]: (intersection(null_class,X0)=restrict(X0,X1,null_class))),
% 196.84/25.24 inference(paramodulation,[status(thm)],[f59964,f151])).
% 196.84/25.24 fof(f63867,plain,(
% 196.84/25.24 ![X0,X1]: (null_class=restrict(X0,X1,null_class))),
% 196.84/25.24 inference(forward_demodulation,[status(thm)],[f5701,f63831])).
% 196.84/25.24 fof(f64031,plain,(
% 196.84/25.24 domain_of(null_class)=sum_class(null_class)),
% 196.84/25.24 inference(paramodulation,[status(thm)],[f63867,f175])).
% 196.84/25.24 fof(f64038,plain,(
% 196.84/25.24 null_class=sum_class(null_class)),
% 196.84/25.24 inference(forward_demodulation,[status(thm)],[f21347,f64031])).
% 196.84/25.24 fof(f64039,plain,(
% 196.84/25.24 $false),
% 196.84/25.24 inference(forward_subsumption_resolution,[status(thm)],[f64038,f245])).
% 196.84/25.24 % SZS output end CNFRefutation for theBenchmark.p
% 24.89/25.46 % Elapsed time: 25.052420 seconds
% 24.89/25.46 % CPU time: 198.431540 seconds
% 24.89/25.46 % Total memory used: 1.520 GB
% 24.89/25.46 % Net memory used: 1.360 GB
%------------------------------------------------------------------------------