%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET091+1 : TPTP v8.1.2. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:39:10 EDT 2024
% Result : Theorem 151.53s 151.72s
% Output : Refutation 151.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SET091+1 : TPTP v8.1.2. Bugfixed v7.3.0.
% 0.08/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n012.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 18:50:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 151.53/151.72 % Version: 1.5
% 151.53/151.72 % SZS status Theorem
% 151.53/151.72 % SZS output start CNFRefutation
% 151.53/151.72 fof(member_when_not_a_singleton,conjecture,(![X]:(![U]:(((~(?[Y]:(member(Y,universal_class)&X=singleton(Y))))&X=U)=>member_of(X)=U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', member_when_not_a_singleton)).
% 151.53/151.72 fof(c27,negated_conjecture,(~(![X]:(![U]:(((~(?[Y]:(member(Y,universal_class)&X=singleton(Y))))&X=U)=>member_of(X)=U)))),inference(assume_negation,[status(cth)],[member_when_not_a_singleton])).
% 151.53/151.72 fof(c28,negated_conjecture,(?[X]:(?[U]:(((![Y]:(~member(Y,universal_class)|X!=singleton(Y)))&X=U)&member_of(X)!=U))),inference(fof_nnf,[status(thm)],[c27])).
% 151.53/151.72 fof(c29,negated_conjecture,(?[X2]:(?[X3]:(((![X4]:(~member(X4,universal_class)|X2!=singleton(X4)))&X2=X3)&member_of(X2)!=X3))),inference(variable_rename,[status(thm)],[c28])).
% 151.53/151.72 fof(c31,negated_conjecture,(![X4]:(((~member(X4,universal_class)|skolem0001!=singleton(X4))&skolem0001=skolem0002)&member_of(skolem0001)!=skolem0002)),inference(shift_quantors,[status(thm)],[fof(c30,negated_conjecture,(((![X4]:(~member(X4,universal_class)|skolem0001!=singleton(X4)))&skolem0001=skolem0002)&member_of(skolem0001)!=skolem0002),inference(skolemize,[status(esa)],[c29])).])).
% 151.53/151.72 cnf(c34,negated_conjecture,member_of(skolem0001)!=skolem0002,inference(split_conjunct,[status(thm)],[c31])).
% 151.53/151.72 cnf(c33,negated_conjecture,skolem0001=skolem0002,inference(split_conjunct,[status(thm)],[c31])).
% 151.53/151.72 cnf(transitivity,axiom,X151!=X153|X153!=X152|X151=X152,theory(equality)).
% 151.53/151.72 cnf(c276,plain,X210!=skolem0001|X210=skolem0002,inference(resolution,[status(thm)],[transitivity, c33])).
% 151.53/151.72 fof(member_universal_self,axiom,(![X]:(member(member_of(X),universal_class)|member_of(X)=X)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', member_universal_self)).
% 151.53/151.72 fof(c37,plain,(![X6]:(member(member_of(X6),universal_class)|member_of(X6)=X6)),inference(variable_rename,[status(thm)],[member_universal_self])).
% 151.53/151.72 cnf(c38,plain,member(member_of(X284),universal_class)|member_of(X284)=X284,inference(split_conjunct,[status(thm)],[c37])).
% 151.53/151.72 cnf(c32,negated_conjecture,~member(X282,universal_class)|skolem0001!=singleton(X282),inference(split_conjunct,[status(thm)],[c31])).
% 151.53/151.72 cnf(symmetry,axiom,X148!=X149|X149=X148,theory(equality)).
% 151.53/151.72 fof(singleton_self,axiom,(![X]:(singleton(member_of(X))=X|member_of(X)=X)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', singleton_self)).
% 151.53/151.72 fof(c35,plain,(![X5]:(singleton(member_of(X5))=X5|member_of(X5)=X5)),inference(variable_rename,[status(thm)],[singleton_self])).
% 151.53/151.72 cnf(c36,plain,singleton(member_of(X283))=X283|member_of(X283)=X283,inference(split_conjunct,[status(thm)],[c35])).
% 151.53/151.72 cnf(c1246,plain,singleton(member_of(skolem0001))=skolem0001|member_of(skolem0001)=skolem0002,inference(resolution,[status(thm)],[c36, c276])).
% 151.53/151.72 cnf(c200590,plain,singleton(member_of(skolem0001))=skolem0001,inference(resolution,[status(thm)],[c1246, c34])).
% 151.53/151.72 cnf(c201205,plain,skolem0001=singleton(member_of(skolem0001)),inference(resolution,[status(thm)],[c200590, symmetry])).
% 151.53/151.72 cnf(c201746,plain,~member(member_of(skolem0001),universal_class),inference(resolution,[status(thm)],[c201205, c32])).
% 151.53/151.72 cnf(c201955,plain,member_of(skolem0001)=skolem0001,inference(resolution,[status(thm)],[c201746, c38])).
% 151.53/151.72 cnf(c202569,plain,member_of(skolem0001)=skolem0002,inference(resolution,[status(thm)],[c201955, c276])).
% 151.53/151.72 cnf(c203261,plain,$false,inference(resolution,[status(thm)],[c202569, c34])).
% 151.53/151.72 % SZS output end CNFRefutation
% 151.53/151.72
% 151.53/151.72 % Initial clauses : 126
% 151.53/151.72 % Processed clauses : 2122
% 151.53/151.72 % Factors computed : 62
% 151.53/151.72 % Resolvents computed: 203253
% 151.53/151.72 % Tautologies deleted: 7
% 151.53/151.72 % Forward subsumed : 2943
% 151.53/151.72 % Backward subsumed : 105
% 151.53/151.72 % -------- CPU Time ---------
% 151.53/151.72 % User time : 150.937 s
% 151.53/151.72 % System time : 0.432 s
% 151.53/151.72 % Total time : 151.369 s
%------------------------------------------------------------------------------