%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM071-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 : n018.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 31.06s 4.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM071-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n018.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:04:13 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 31.06/4.53 % Refutation found
% 31.06/4.53 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 31.06/4.53 % SZS output start CNFRefutation for theBenchmark
% 31.06/4.53 fof(f1,axiom,(
% 31.06/4.53 (![X,Y,U]: (( ~ subclass(X,Y)| ~ member(U,X)| member(U,Y) ) ))),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f2,axiom,(
% 31.06/4.53 (![X,Y]: (( member(not_subclass_element(X,Y),X)| subclass(X,Y) ) ))),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f3,axiom,(
% 31.06/4.53 (![X,Y]: (( ~ member(not_subclass_element(X,Y),Y)| subclass(X,Y) ) ))),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f4,axiom,(
% 31.06/4.53 (![X]: (subclass(X,universal_class) ))),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f5,axiom,(
% 31.06/4.53 (![X,Y]: (( X != Y| subclass(X,Y) ) ))),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f8,axiom,(
% 31.06/4.53 (![U,X,Y]: (( ~ member(U,unordered_pair(X,Y))| U = X| U = Y ) ))),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f10,axiom,(
% 31.06/4.53 (![Y,X]: (( ~ member(Y,universal_class)| member(Y,unordered_pair(X,Y)) ) ))),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f11,axiom,(
% 31.06/4.53 (![X,Y]: (member(unordered_pair(X,Y),universal_class) ))),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f12,axiom,(
% 31.06/4.53 (![X]: (unordered_pair(X,X) = singleton(X) ))),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f13,axiom,(
% 31.06/4.53 (![X,Y]: (unordered_pair(singleton(X),unordered_pair(X,singleton(Y))) = ordered_pair(X,Y) ))),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f21,axiom,(
% 31.06/4.53 (![Z,X,Y]: (( ~ member(Z,intersection(X,Y))| member(Z,X) ) ))),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f66,axiom,(
% 31.06/4.53 (![X]: (( X = null_class| member(regular(X),X) ) ))),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f67,axiom,(
% 31.06/4.53 (![X]: (( X = null_class| intersection(X,regular(X)) = null_class ) ))),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f124,axiom,(
% 31.06/4.53 (![Xr,Y,U]: (( ~ well_ordering(Xr,Y)| ~ subclass(U,Y)| U = null_class| member(least(Xr,U),U) ) ))),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f127,axiom,(
% 31.06/4.53 (![Xr,Y,U,V]: (( ~ well_ordering(Xr,Y)| ~ subclass(U,Y)| ~ member(V,U)| ~ member(ordered_pair(V,least(Xr,U)),Xr) ) ))),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f159,negated_conjecture,(
% 31.06/4.53 well_ordering(xr,y) ),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f160,negated_conjecture,(
% 31.06/4.53 member(ordered_pair(u,u),xr) ),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f161,negated_conjecture,(
% 31.06/4.53 member(u,y) ),
% 31.06/4.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 31.06/4.53 fof(f162,plain,(
% 31.06/4.53 ![Y,U]: ((![X]: (~subclass(X,Y)|~member(U,X)))|member(U,Y))),
% 31.06/4.53 inference(miniscoping,[status(thm)],[f1])).
% 31.06/4.53 fof(f163,plain,(
% 31.06/4.53 ![X0,X1,X2]: (~subclass(X0,X1)|~member(X2,X0)|member(X2,X1))),
% 31.06/4.53 inference(cnf_transformation,[status(thm)],[f162])).
% 31.06/4.53 fof(f164,plain,(
% 31.06/4.53 ![X0,X1]: (member(not_subclass_element(X0,X1),X0)|subclass(X0,X1))),
% 31.06/4.53 inference(cnf_transformation,[status(thm)],[f2])).
% 31.06/4.53 fof(f165,plain,(
% 31.06/4.53 ![X0,X1]: (~member(not_subclass_element(X0,X1),X1)|subclass(X0,X1))),
% 31.06/4.53 inference(cnf_transformation,[status(thm)],[f3])).
% 31.06/4.53 fof(f166,plain,(
% 31.06/4.53 ![X0]: (subclass(X0,universal_class))),
% 31.06/4.53 inference(cnf_transformation,[status(thm)],[f4])).
% 31.06/4.53 fof(f167,plain,(
% 31.06/4.53 ![X0,X1]: (~X0=X1|subclass(X0,X1))),
% 31.06/4.53 inference(cnf_transformation,[status(thm)],[f5])).
% 31.06/4.53 fof(f170,plain,(
% 31.06/4.53 ![U,Y]: ((![X]: (~member(U,unordered_pair(X,Y))|U=X))|U=Y)),
% 31.06/4.53 inference(miniscoping,[status(thm)],[f8])).
% 31.06/4.53 fof(f171,plain,(
% 31.06/4.53 ![X0,X1,X2]: (~member(X0,unordered_pair(X1,X2))|X0=X1|X0=X2)),
% 31.06/4.53 inference(cnf_transformation,[status(thm)],[f170])).
% 31.06/4.53 fof(f174,plain,(
% 31.06/4.53 ![Y]: (~member(Y,universal_class)|(![X]: member(Y,unordered_pair(X,Y))))),
% 31.06/4.53 inference(miniscoping,[status(thm)],[f10])).
% 31.06/4.53 fof(f175,plain,(
% 31.06/4.53 ![X0,X1]: (~member(X0,universal_class)|member(X0,unordered_pair(X1,X0)))),
% 31.06/4.53 inference(cnf_transformation,[status(thm)],[f174])).
% 31.06/4.53 fof(f176,plain,(
% 31.06/4.53 ![X0,X1]: (member(unordered_pair(X0,X1),universal_class))),
% 31.88/4.53 inference(cnf_transformation,[status(thm)],[f11])).
% 31.88/4.53 fof(f177,plain,(
% 31.88/4.53 ![X0]: (unordered_pair(X0,X0)=singleton(X0))),
% 31.88/4.53 inference(cnf_transformation,[status(thm)],[f12])).
% 31.88/4.53 fof(f178,plain,(
% 31.88/4.53 ![X0,X1]: (unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1)))=ordered_pair(X0,X1))),
% 31.88/4.53 inference(cnf_transformation,[status(thm)],[f13])).
% 31.88/4.53 fof(f189,plain,(
% 31.88/4.53 ![Z,X]: ((![Y]: ~member(Z,intersection(X,Y)))|member(Z,X))),
% 31.88/4.53 inference(miniscoping,[status(thm)],[f21])).
% 31.88/4.53 fof(f190,plain,(
% 31.88/4.53 ![X0,X1,X2]: (~member(X0,intersection(X1,X2))|member(X0,X1))),
% 31.88/4.53 inference(cnf_transformation,[status(thm)],[f189])).
% 31.88/4.53 fof(f236,plain,(
% 31.88/4.53 ![X0]: (X0=null_class|member(regular(X0),X0))),
% 31.88/4.53 inference(cnf_transformation,[status(thm)],[f66])).
% 31.88/4.53 fof(f237,plain,(
% 31.88/4.53 ![X0]: (X0=null_class|intersection(X0,regular(X0))=null_class)),
% 31.88/4.53 inference(cnf_transformation,[status(thm)],[f67])).
% 31.88/4.53 fof(f304,plain,(
% 31.88/4.53 ![Xr,U]: (((![Y]: (~well_ordering(Xr,Y)|~subclass(U,Y)))|U=null_class)|member(least(Xr,U),U))),
% 31.88/4.53 inference(miniscoping,[status(thm)],[f124])).
% 31.88/4.53 fof(f305,plain,(
% 31.88/4.53 ![X0,X1,X2]: (~well_ordering(X0,X1)|~subclass(X2,X1)|X2=null_class|member(least(X0,X2),X2))),
% 31.88/4.53 inference(cnf_transformation,[status(thm)],[f304])).
% 31.88/4.53 fof(f310,plain,(
% 31.88/4.53 ![Xr,U,V]: (((![Y]: (~well_ordering(Xr,Y)|~subclass(U,Y)))|~member(V,U))|~member(ordered_pair(V,least(Xr,U)),Xr))),
% 31.88/4.53 inference(miniscoping,[status(thm)],[f127])).
% 31.88/4.53 fof(f311,plain,(
% 31.88/4.53 ![X0,X1,X2,X3]: (~well_ordering(X0,X1)|~subclass(X2,X1)|~member(X3,X2)|~member(ordered_pair(X3,least(X0,X2)),X0))),
% 31.88/4.53 inference(cnf_transformation,[status(thm)],[f310])).
% 31.88/4.53 fof(f349,plain,(
% 31.88/4.53 well_ordering(xr,y)),
% 31.88/4.53 inference(cnf_transformation,[status(thm)],[f159])).
% 31.88/4.53 fof(f350,plain,(
% 31.88/4.53 member(ordered_pair(u,u),xr)),
% 31.88/4.53 inference(cnf_transformation,[status(thm)],[f160])).
% 31.88/4.53 fof(f351,plain,(
% 31.88/4.53 member(u,y)),
% 31.88/4.53 inference(cnf_transformation,[status(thm)],[f161])).
% 31.88/4.53 fof(f352,plain,(
% 31.88/4.53 ![X0]: (subclass(X0,X0))),
% 31.88/4.53 inference(destructive_equality_resolution,[status(thm)],[f167])).
% 31.88/4.53 fof(f375,plain,(
% 31.88/4.53 ![X0]: (~member(X0,universal_class)|member(X0,singleton(X0)))),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f177,f175])).
% 31.88/4.53 fof(f377,plain,(
% 31.88/4.53 ![X0,X1]: (~member(X0,singleton(X1))|X0=X1|X0=X1)),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f177,f171])).
% 31.88/4.53 fof(f379,plain,(
% 31.88/4.53 ![X0,X1]: (~member(X0,singleton(X1))|X0=X1)),
% 31.88/4.53 inference(duplicate_literals_removal,[status(thm)],[f377])).
% 31.88/4.53 fof(f380,plain,(
% 31.88/4.53 ![X0,X1]: (not_subclass_element(singleton(X0),X1)=X0|subclass(singleton(X0),X1))),
% 31.88/4.53 inference(resolution,[status(thm)],[f379,f164])).
% 31.88/4.53 fof(f387,plain,(
% 31.88/4.53 ![X0]: (unordered_pair(singleton(singleton(X0)),singleton(singleton(X0)))=ordered_pair(singleton(X0),X0))),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f177,f178])).
% 31.88/4.53 fof(f388,plain,(
% 31.88/4.53 ![X0,X1]: (~member(unordered_pair(X0,singleton(X1)),universal_class)|member(unordered_pair(X0,singleton(X1)),ordered_pair(X0,X1)))),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f178,f175])).
% 31.88/4.53 fof(f392,plain,(
% 31.88/4.53 ![X0]: (singleton(singleton(singleton(X0)))=ordered_pair(singleton(X0),X0))),
% 31.88/4.53 inference(forward_demodulation,[status(thm)],[f177,f387])).
% 31.88/4.53 fof(f393,plain,(
% 31.88/4.53 ![X0,X1]: (member(unordered_pair(X0,singleton(X1)),ordered_pair(X0,X1)))),
% 31.88/4.53 inference(forward_subsumption_resolution,[status(thm)],[f388,f176])).
% 31.88/4.53 fof(f397,plain,(
% 31.88/4.53 ![X0,X1]: (~subclass(X0,y)|~member(X1,X0)|~member(ordered_pair(X1,least(xr,X0)),xr))),
% 31.88/4.53 inference(resolution,[status(thm)],[f311,f349])).
% 31.88/4.53 fof(f404,plain,(
% 31.88/4.53 ![X0,X1,X2]: (~subclass(X0,y)|~member(X1,X0)|~subclass(X2,xr)|~member(ordered_pair(X1,least(xr,X0)),X2))),
% 31.88/4.53 inference(resolution,[status(thm)],[f397,f163])).
% 31.88/4.53 fof(f405,plain,(
% 31.88/4.53 ![X0,X1]: (~member(X0,y)|~subclass(X1,xr)|~member(ordered_pair(X0,least(xr,y)),X1))),
% 31.88/4.53 inference(resolution,[status(thm)],[f404,f352])).
% 31.88/4.53 fof(f406,plain,(
% 31.88/4.53 ![X0]: (~member(X0,y)|~member(ordered_pair(X0,least(xr,y)),xr))),
% 31.88/4.53 inference(resolution,[status(thm)],[f405,f352])).
% 31.88/4.53 fof(f439,plain,(
% 31.88/4.53 ![X0]: (singleton(X0)=null_class|regular(singleton(X0))=X0)),
% 31.88/4.53 inference(resolution,[status(thm)],[f236,f379])).
% 31.88/4.53 fof(f506,plain,(
% 31.88/4.53 ![X0,X1]: (~member(X0,null_class)|member(X0,X1)|X1=null_class)),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f237,f190])).
% 31.88/4.53 fof(f537,plain,(
% 31.88/4.53 ![X0]: (singleton(X0)=null_class|member(X0,singleton(X0))|singleton(X0)=null_class)),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f439,f236])).
% 31.88/4.53 fof(f539,plain,(
% 31.88/4.53 ![X0]: (singleton(X0)=null_class|member(X0,singleton(X0)))),
% 31.88/4.53 inference(duplicate_literals_removal,[status(thm)],[f537])).
% 31.88/4.53 fof(f565,plain,(
% 31.88/4.53 ![X0]: (member(singleton(singleton(X0)),ordered_pair(singleton(X0),X0)))),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f177,f393])).
% 31.88/4.53 fof(f566,plain,(
% 31.88/4.53 ![X0]: (member(singleton(singleton(X0)),singleton(singleton(singleton(X0)))))),
% 31.88/4.53 inference(forward_demodulation,[status(thm)],[f392,f565])).
% 31.88/4.53 fof(f627,plain,(
% 31.88/4.53 ![X0,X1,X2]: (not_subclass_element(singleton(X0),y)=X0|~member(X1,singleton(X0))|~subclass(X2,xr)|~member(ordered_pair(X1,least(xr,singleton(X0))),X2))),
% 31.88/4.53 inference(resolution,[status(thm)],[f380,f404])).
% 31.88/4.53 fof(f629,plain,(
% 31.88/4.53 ~member(singleton(least(xr,y)),y)|~member(singleton(singleton(singleton(least(xr,y)))),xr)),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f392,f406])).
% 31.88/4.53 fof(f705,plain,(
% 31.88/4.53 ![X0,X1]: (not_subclass_element(singleton(X0),y)=X0|~member(X1,singleton(X0))|~member(ordered_pair(X1,least(xr,singleton(X0))),xr))),
% 31.88/4.53 inference(resolution,[status(thm)],[f627,f352])).
% 31.88/4.53 fof(f1315,plain,(
% 31.88/4.53 ![X0]: (~subclass(X0,y)|X0=null_class|member(least(xr,X0),X0))),
% 31.88/4.53 inference(resolution,[status(thm)],[f305,f349])).
% 31.88/4.53 fof(f1319,plain,(
% 31.88/4.53 ![X0]: (singleton(X0)=null_class|member(least(xr,singleton(X0)),singleton(X0))|not_subclass_element(singleton(X0),y)=X0)),
% 31.88/4.53 inference(resolution,[status(thm)],[f1315,f380])).
% 31.88/4.53 fof(f1331,plain,(
% 31.88/4.53 ![X0]: (singleton(X0)=null_class|not_subclass_element(singleton(X0),y)=X0|least(xr,singleton(X0))=X0)),
% 31.88/4.53 inference(resolution,[status(thm)],[f1319,f379])).
% 31.88/4.53 fof(f1352,plain,(
% 31.88/4.53 ![X0,X1]: (not_subclass_element(singleton(X0),y)=X0|~member(X1,singleton(X0))|~member(ordered_pair(X1,X0),xr)|singleton(X0)=null_class|not_subclass_element(singleton(X0),y)=X0)),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f1331,f705])).
% 31.88/4.53 fof(f1371,plain,(
% 31.88/4.53 ![X0,X1]: (not_subclass_element(singleton(X0),y)=X0|~member(X1,singleton(X0))|~member(ordered_pair(X1,X0),xr)|singleton(X0)=null_class)),
% 31.88/4.53 inference(duplicate_literals_removal,[status(thm)],[f1352])).
% 31.88/4.53 fof(f1373,plain,(
% 31.88/4.53 not_subclass_element(singleton(u),y)=u|~member(u,singleton(u))|singleton(u)=null_class),
% 31.88/4.53 inference(resolution,[status(thm)],[f1371,f350])).
% 31.88/4.53 fof(f1376,plain,(
% 31.88/4.53 not_subclass_element(singleton(u),y)=u|singleton(u)=null_class),
% 31.88/4.53 inference(forward_subsumption_resolution,[status(thm)],[f1373,f539])).
% 31.88/4.53 fof(f1377,plain,(
% 31.88/4.53 ~member(u,y)|subclass(singleton(u),y)|singleton(u)=null_class),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f1376,f165])).
% 31.88/4.53 fof(f1379,plain,(
% 31.88/4.53 subclass(singleton(u),y)|singleton(u)=null_class),
% 31.88/4.53 inference(forward_subsumption_resolution,[status(thm)],[f1377,f351])).
% 31.88/4.53 fof(f1380,plain,(
% 31.88/4.53 singleton(u)=null_class|singleton(u)=null_class|member(least(xr,singleton(u)),singleton(u))),
% 31.88/4.53 inference(resolution,[status(thm)],[f1379,f1315])).
% 31.88/4.53 fof(f1387,plain,(
% 31.88/4.53 singleton(u)=null_class|member(least(xr,singleton(u)),singleton(u))),
% 31.88/4.53 inference(duplicate_literals_removal,[status(thm)],[f1380])).
% 31.88/4.53 fof(f1561,plain,(
% 31.88/4.53 singleton(u)=null_class|least(xr,singleton(u))=u),
% 31.88/4.53 inference(resolution,[status(thm)],[f1387,f379])).
% 31.88/4.53 fof(f1587,plain,(
% 31.88/4.53 ![X0]: (~subclass(singleton(u),y)|~member(X0,singleton(u))|~member(ordered_pair(X0,u),xr)|singleton(u)=null_class)),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f1561,f397])).
% 31.88/4.53 fof(f1593,plain,(
% 31.88/4.53 ![X0]: (~member(X0,singleton(u))|~member(ordered_pair(X0,u),xr)|singleton(u)=null_class)),
% 31.88/4.53 inference(forward_subsumption_resolution,[status(thm)],[f1587,f1379])).
% 31.88/4.53 fof(f1898,plain,(
% 31.88/4.53 ~member(u,singleton(u))|singleton(u)=null_class),
% 31.88/4.53 inference(resolution,[status(thm)],[f1593,f350])).
% 31.88/4.53 fof(f1936,plain,(
% 31.88/4.53 singleton(u)=null_class),
% 31.88/4.53 inference(forward_subsumption_resolution,[status(thm)],[f1898,f539])).
% 31.88/4.53 fof(f2023,plain,(
% 31.88/4.53 member(singleton(singleton(u)),singleton(singleton(null_class)))),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f1936,f566])).
% 31.88/4.53 fof(f2059,plain,(
% 31.88/4.53 singleton(singleton(singleton(u)))=ordered_pair(null_class,u)),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f1936,f392])).
% 31.88/4.53 fof(f2066,plain,(
% 31.88/4.53 ~member(u,universal_class)|member(u,null_class)),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f1936,f375])).
% 31.88/4.53 fof(f2075,plain,(
% 31.88/4.53 ![X0]: (~member(X0,null_class)|X0=u)),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f1936,f379])).
% 31.88/4.53 fof(f2111,plain,(
% 31.88/4.53 member(singleton(null_class),singleton(singleton(null_class)))),
% 31.88/4.53 inference(forward_demodulation,[status(thm)],[f1936,f2023])).
% 31.88/4.53 fof(f2184,plain,(
% 31.88/4.53 singleton(singleton(null_class))=ordered_pair(null_class,u)),
% 31.88/4.53 inference(forward_demodulation,[status(thm)],[f1936,f2059])).
% 31.88/4.53 fof(f2407,plain,(
% 31.88/4.53 ![X0]: (member(u,null_class)|~subclass(X0,universal_class)|~member(u,X0))),
% 31.88/4.53 inference(resolution,[status(thm)],[f2066,f163])).
% 31.88/4.53 fof(f2408,plain,(
% 31.88/4.53 ![X0]: (member(u,null_class)|~member(u,X0))),
% 31.88/4.53 inference(forward_subsumption_resolution,[status(thm)],[f2407,f166])).
% 31.88/4.53 fof(f2413,plain,(
% 31.88/4.53 ![X0,X1]: (~member(u,X0)|member(u,X1)|X1=null_class)),
% 31.88/4.53 inference(resolution,[status(thm)],[f2408,f506])).
% 31.88/4.53 fof(f2475,plain,(
% 31.88/4.53 ![X0]: (member(u,X0)|X0=null_class)),
% 31.88/4.53 inference(resolution,[status(thm)],[f2413,f351])).
% 31.88/4.53 fof(f2521,plain,(
% 31.88/4.53 ![X0]: (singleton(X0)=null_class|u=X0)),
% 31.88/4.53 inference(resolution,[status(thm)],[f2475,f379])).
% 31.88/4.53 fof(f2744,plain,(
% 31.88/4.53 member(null_class,singleton(singleton(null_class)))|u=null_class),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f2521,f2111])).
% 31.88/4.53 fof(f2767,plain,(
% 31.88/4.53 member(singleton(null_class),null_class)|u=singleton(null_class)),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f2521,f2111])).
% 31.88/4.53 fof(f2779,plain,(
% 31.88/4.53 ![X0]: (member(singleton(singleton(X0)),null_class)|u=singleton(singleton(X0)))),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f2521,f566])).
% 31.88/4.53 fof(f2795,plain,(
% 31.88/4.53 ~member(null_class,y)|~member(singleton(singleton(singleton(least(xr,y)))),xr)|u=least(xr,y)),
% 31.88/4.53 inference(paramodulation,[status(thm)],[f2521,f629])).
% 31.88/4.53 fof(f2873,plain,(
% 31.88/4.53 singleton(u)=ordered_pair(null_class,u)),
% 31.88/4.53 inference(backward_demodulation,[status(thm)],[f2930,f2184])).
% 31.88/4.53 fof(f2884,plain,(
% 31.88/4.53 member(null_class,singleton(u))|u=null_class),
% 31.88/4.53 inference(backward_demodulation,[status(thm)],[f2930,f2744])).
% 31.88/4.53 fof(f2930,plain,(
% 31.88/4.53 u=singleton(null_class)),
% 31.88/4.53 inference(forward_subsumption_resolution,[status(thm)],[f2767,f2075])).
% 31.88/4.53 fof(f2951,plain,(
% 31.88/4.53 ~member(singleton(least(xr,y)),y)|~member(singleton(u),xr)),
% 31.88/4.53 inference(backward_demodulation,[status(thm)],[f3054,f629])).
% 31.88/4.53 fof(f3054,plain,(
% 31.88/4.53 ![X0]: (u=singleton(singleton(X0)))),
% 31.88/4.53 inference(forward_subsumption_resolution,[status(thm)],[f2779,f2075])).
% 31.88/4.53 fof(f3071,plain,(
% 31.88/4.53 ~member(null_class,y)|~member(u,xr)|u=least(xr,y)),
% 31.88/4.53 inference(forward_demodulation,[status(thm)],[f3054,f2795])).
% 31.88/4.53 fof(f3102,plain,(
% 31.88/4.53 null_class=ordered_pair(null_class,u)),
% 31.88/4.53 inference(forward_demodulation,[status(thm)],[f1936,f2873])).
% 31.88/4.53 fof(f3113,plain,(
% 31.88/4.53 member(null_class,null_class)|u=null_class),
% 31.88/4.53 inference(forward_demodulation,[status(thm)],[f1936,f2884])).
% 31.88/4.53 fof(f3123,plain,(
% 31.88/4.53 singleton(null_class)=null_class),
% 31.88/4.53 inference(backward_demodulation,[status(thm)],[f3347,f1936])).
% 31.88/4.53 fof(f3134,plain,(
% 31.88/4.53 member(ordered_pair(u,null_class),xr)),
% 31.88/4.53 inference(backward_demodulation,[status(thm)],[f3347,f350])).
% 31.88/4.53 fof(f3135,plain,(
% 31.88/4.53 member(null_class,y)),
% 31.88/4.53 inference(backward_demodulation,[status(thm)],[f3347,f351])).
% 31.88/4.53 fof(f3146,plain,(
% 31.88/4.53 null_class=ordered_pair(null_class,null_class)),
% 31.88/4.53 inference(backward_demodulation,[status(thm)],[f3347,f3102])).
% 31.88/4.53 fof(f3205,plain,(
% 31.88/4.53 ~member(null_class,y)|~member(u,xr)|null_class=least(xr,y)),
% 31.88/4.53 inference(backward_demodulation,[status(thm)],[f3347,f3071])).
% 31.88/4.53 fof(f3347,plain,(
% 31.88/4.53 u=null_class),
% 31.88/4.53 inference(forward_subsumption_resolution,[status(thm)],[f3113,f2075])).
% 31.88/4.53 fof(f3515,plain,(
% 31.88/4.53 ~member(singleton(least(xr,y)),y)|~member(null_class,xr)),
% 31.88/4.53 inference(forward_demodulation,[status(thm)],[f1936,f2951])).
% 31.88/4.53 fof(f3686,plain,(
% 31.88/4.53 member(ordered_pair(null_class,null_class),xr)),
% 31.88/4.53 inference(forward_demodulation,[status(thm)],[f3347,f3134])).
% 31.88/4.53 fof(f3694,plain,(
% 31.88/4.53 member(null_class,xr)),
% 31.88/4.53 inference(backward_demodulation,[status(thm)],[f3146,f3686])).
% 31.88/4.58 fof(f3728,plain,(
% 31.88/4.58 ~member(null_class,y)|~member(null_class,xr)|null_class=least(xr,y)),
% 31.88/4.58 inference(forward_demodulation,[status(thm)],[f3347,f3205])).
% 31.88/4.58 fof(f3729,plain,(
% 31.88/4.58 ~member(null_class,xr)|null_class=least(xr,y)),
% 31.88/4.58 inference(forward_subsumption_resolution,[status(thm)],[f3728,f3135])).
% 31.88/4.58 fof(f3816,plain,(
% 31.88/4.58 null_class=least(xr,y)),
% 31.88/4.58 inference(backward_subsumption_resolution,[status(thm)],[f3729,f3694])).
% 31.88/4.58 fof(f3824,plain,(
% 31.88/4.58 ~member(singleton(least(xr,y)),y)),
% 31.88/4.58 inference(backward_subsumption_resolution,[status(thm)],[f3515,f3694])).
% 31.88/4.58 fof(f4040,plain,(
% 31.88/4.58 ~member(singleton(null_class),y)),
% 31.88/4.58 inference(forward_demodulation,[status(thm)],[f3816,f3824])).
% 31.88/4.58 fof(f4041,plain,(
% 31.88/4.58 ~member(null_class,y)),
% 31.88/4.58 inference(forward_demodulation,[status(thm)],[f3123,f4040])).
% 31.88/4.58 fof(f4042,plain,(
% 31.88/4.58 $false),
% 31.88/4.58 inference(forward_subsumption_resolution,[status(thm)],[f4041,f3135])).
% 31.88/4.58 % SZS output end CNFRefutation for theBenchmark.p
% 31.88/4.59 % Elapsed time: 4.146192 seconds
% 31.88/4.59 % CPU time: 32.302448 seconds
% 31.88/4.59 % Total memory used: 373.386 MB
% 31.88/4.59 % Net memory used: 336.269 MB
%------------------------------------------------------------------------------