%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET764+4 : TPTP v8.1.2. Bugfixed v2.2.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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:40:03 EDT 2024
% Result : Theorem 31.44s 31.61s
% Output : Refutation 31.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET764+4 : TPTP v8.1.2. Bugfixed v2.2.1.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n021.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 19:25:38 EDT 2024
% 0.14/0.35 % CPUTime :
% 31.44/31.61 % Version: 1.5
% 31.44/31.61 % SZS status Theorem
% 31.44/31.61 % SZS output start CNFRefutation
% 31.44/31.61 fof(thIIa14,conjecture,(![F]:(![A]:(![B]:(maps(F,A,B)=>equal_set(inverse_image2(F,empty_set),empty_set))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', thIIa14)).
% 31.44/31.61 fof(c29,negated_conjecture,(~(![F]:(![A]:(![B]:(maps(F,A,B)=>equal_set(inverse_image2(F,empty_set),empty_set)))))),inference(assume_negation,[status(cth)],[thIIa14])).
% 31.44/31.61 fof(c30,negated_conjecture,(?[F]:(?[A]:(?[B]:(maps(F,A,B)&~equal_set(inverse_image2(F,empty_set),empty_set))))),inference(fof_nnf,[status(thm)],[c29])).
% 31.44/31.61 fof(c31,negated_conjecture,(?[F]:((?[A]:(?[B]:maps(F,A,B)))&~equal_set(inverse_image2(F,empty_set),empty_set))),inference(shift_quantors,[status(thm)],[c30])).
% 31.44/31.61 fof(c32,negated_conjecture,(?[X2]:((?[X3]:(?[X4]:maps(X2,X3,X4)))&~equal_set(inverse_image2(X2,empty_set),empty_set))),inference(variable_rename,[status(thm)],[c31])).
% 31.44/31.61 fof(c33,negated_conjecture,(maps(skolem0001,skolem0002,skolem0003)&~equal_set(inverse_image2(skolem0001,empty_set),empty_set)),inference(skolemize,[status(esa)],[c32])).
% 31.44/31.61 cnf(c35,negated_conjecture,~equal_set(inverse_image2(skolem0001,empty_set),empty_set),inference(split_conjunct,[status(thm)],[c33])).
% 31.44/31.61 fof(empty_set,axiom,(![X]:(~member(X,empty_set))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', empty_set)).
% 31.44/31.61 fof(c279,plain,(![X]:~member(X,empty_set)),inference(fof_simplification,[status(thm)],[empty_set])).
% 31.44/31.61 fof(c280,plain,(![X233]:~member(X233,empty_set)),inference(variable_rename,[status(thm)],[c279])).
% 31.44/31.61 cnf(c281,plain,~member(X261,empty_set),inference(split_conjunct,[status(thm)],[c280])).
% 31.44/31.61 fof(subset,axiom,(![A]:(![B]:(subset(A,B)<=>(![X]:(member(X,A)=>member(X,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', subset)).
% 31.44/31.61 fof(c312,plain,(![A]:(![B]:((~subset(A,B)|(![X]:(~member(X,A)|member(X,B))))&((?[X]:(member(X,A)&~member(X,B)))|subset(A,B))))),inference(fof_nnf,[status(thm)],[subset])).
% 31.44/31.61 fof(c313,plain,((![A]:(![B]:(~subset(A,B)|(![X]:(~member(X,A)|member(X,B))))))&(![A]:(![B]:((?[X]:(member(X,A)&~member(X,B)))|subset(A,B))))),inference(shift_quantors,[status(thm)],[c312])).
% 31.44/31.61 fof(c314,plain,((![X254]:(![X255]:(~subset(X254,X255)|(![X256]:(~member(X256,X254)|member(X256,X255))))))&(![X257]:(![X258]:((?[X259]:(member(X259,X257)&~member(X259,X258)))|subset(X257,X258))))),inference(variable_rename,[status(thm)],[c313])).
% 31.44/31.61 fof(c316,plain,(![X254]:(![X255]:(![X256]:(![X257]:(![X258]:((~subset(X254,X255)|(~member(X256,X254)|member(X256,X255)))&((member(skolem0043(X257,X258),X257)&~member(skolem0043(X257,X258),X258))|subset(X257,X258)))))))),inference(shift_quantors,[status(thm)],[fof(c315,plain,((![X254]:(![X255]:(~subset(X254,X255)|(![X256]:(~member(X256,X254)|member(X256,X255))))))&(![X257]:(![X258]:((member(skolem0043(X257,X258),X257)&~member(skolem0043(X257,X258),X258))|subset(X257,X258))))),inference(skolemize,[status(esa)],[c314])).])).
% 31.44/31.61 fof(c317,plain,(![X254]:(![X255]:(![X256]:(![X257]:(![X258]:((~subset(X254,X255)|(~member(X256,X254)|member(X256,X255)))&((member(skolem0043(X257,X258),X257)|subset(X257,X258))&(~member(skolem0043(X257,X258),X258)|subset(X257,X258))))))))),inference(distribute,[status(thm)],[c316])).
% 31.44/31.61 cnf(c319,plain,member(skolem0043(X360,X361),X360)|subset(X360,X361),inference(split_conjunct,[status(thm)],[c317])).
% 31.44/31.61 cnf(c365,plain,subset(empty_set,X362),inference(resolution,[status(thm)],[c319, c281])).
% 31.44/31.61 fof(equal_set,axiom,(![A]:(![B]:(equal_set(A,B)<=>(subset(A,B)&subset(B,A))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', equal_set)).
% 31.44/31.61 fof(c304,plain,(![A]:(![B]:((~equal_set(A,B)|(subset(A,B)&subset(B,A)))&((~subset(A,B)|~subset(B,A))|equal_set(A,B))))),inference(fof_nnf,[status(thm)],[equal_set])).
% 31.44/31.61 fof(c305,plain,((![A]:(![B]:(~equal_set(A,B)|(subset(A,B)&subset(B,A)))))&(![A]:(![B]:((~subset(A,B)|~subset(B,A))|equal_set(A,B))))),inference(shift_quantors,[status(thm)],[c304])).
% 31.44/31.61 fof(c307,plain,(![X250]:(![X251]:(![X252]:(![X253]:((~equal_set(X250,X251)|(subset(X250,X251)&subset(X251,X250)))&((~subset(X252,X253)|~subset(X253,X252))|equal_set(X252,X253))))))),inference(shift_quantors,[status(thm)],[fof(c306,plain,((![X250]:(![X251]:(~equal_set(X250,X251)|(subset(X250,X251)&subset(X251,X250)))))&(![X252]:(![X253]:((~subset(X252,X253)|~subset(X253,X252))|equal_set(X252,X253))))),inference(variable_rename,[status(thm)],[c305])).])).
% 31.44/31.61 fof(c308,plain,(![X250]:(![X251]:(![X252]:(![X253]:(((~equal_set(X250,X251)|subset(X250,X251))&(~equal_set(X250,X251)|subset(X251,X250)))&((~subset(X252,X253)|~subset(X253,X252))|equal_set(X252,X253))))))),inference(distribute,[status(thm)],[c307])).
% 31.44/31.61 cnf(c311,plain,~subset(X419,X418)|~subset(X418,X419)|equal_set(X419,X418),inference(split_conjunct,[status(thm)],[c308])).
% 31.44/31.61 cnf(c407,plain,~subset(X429,empty_set)|equal_set(X429,empty_set),inference(resolution,[status(thm)],[c311, c365])).
% 31.44/31.61 cnf(c418,plain,equal_set(X880,empty_set)|member(skolem0043(X880,empty_set),X880),inference(resolution,[status(thm)],[c407, c319])).
% 31.44/31.61 fof(inverse_image2,axiom,(![F]:(![B]:(![X]:(member(X,inverse_image2(F,B))<=>(?[Y]:(member(Y,B)&apply(F,X,Y))))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+1.ax', inverse_image2)).
% 31.44/31.61 fof(c94,plain,(![F]:(![B]:(![X]:((~member(X,inverse_image2(F,B))|(?[Y]:(member(Y,B)&apply(F,X,Y))))&((![Y]:(~member(Y,B)|~apply(F,X,Y)))|member(X,inverse_image2(F,B))))))),inference(fof_nnf,[status(thm)],[inverse_image2])).
% 31.44/31.61 fof(c95,plain,((![F]:(![B]:(![X]:(~member(X,inverse_image2(F,B))|(?[Y]:(member(Y,B)&apply(F,X,Y)))))))&(![F]:(![B]:(![X]:((![Y]:(~member(Y,B)|~apply(F,X,Y)))|member(X,inverse_image2(F,B))))))),inference(shift_quantors,[status(thm)],[c94])).
% 31.44/31.61 fof(c96,plain,((![X69]:(![X70]:(![X71]:(~member(X71,inverse_image2(X69,X70))|(?[X72]:(member(X72,X70)&apply(X69,X71,X72)))))))&(![X73]:(![X74]:(![X75]:((![X76]:(~member(X76,X74)|~apply(X73,X75,X76)))|member(X75,inverse_image2(X73,X74))))))),inference(variable_rename,[status(thm)],[c95])).
% 31.44/31.61 fof(c98,plain,(![X69]:(![X70]:(![X71]:(![X73]:(![X74]:(![X75]:(![X76]:((~member(X71,inverse_image2(X69,X70))|(member(skolem0017(X69,X70,X71),X70)&apply(X69,X71,skolem0017(X69,X70,X71))))&((~member(X76,X74)|~apply(X73,X75,X76))|member(X75,inverse_image2(X73,X74))))))))))),inference(shift_quantors,[status(thm)],[fof(c97,plain,((![X69]:(![X70]:(![X71]:(~member(X71,inverse_image2(X69,X70))|(member(skolem0017(X69,X70,X71),X70)&apply(X69,X71,skolem0017(X69,X70,X71)))))))&(![X73]:(![X74]:(![X75]:((![X76]:(~member(X76,X74)|~apply(X73,X75,X76)))|member(X75,inverse_image2(X73,X74))))))),inference(skolemize,[status(esa)],[c96])).])).
% 31.44/31.61 fof(c99,plain,(![X69]:(![X70]:(![X71]:(![X73]:(![X74]:(![X75]:(![X76]:(((~member(X71,inverse_image2(X69,X70))|member(skolem0017(X69,X70,X71),X70))&(~member(X71,inverse_image2(X69,X70))|apply(X69,X71,skolem0017(X69,X70,X71))))&((~member(X76,X74)|~apply(X73,X75,X76))|member(X75,inverse_image2(X73,X74))))))))))),inference(distribute,[status(thm)],[c98])).
% 31.44/31.61 cnf(c100,plain,~member(X1218,inverse_image2(X1219,X1220))|member(skolem0017(X1219,X1220,X1218),X1220),inference(split_conjunct,[status(thm)],[c99])).
% 31.44/31.61 cnf(c1271,plain,member(skolem0017(X11059,X11060,skolem0043(inverse_image2(X11059,X11060),empty_set)),X11060)|equal_set(inverse_image2(X11059,X11060),empty_set),inference(resolution,[status(thm)],[c100, c418])).
% 31.44/31.61 cnf(c32055,plain,equal_set(inverse_image2(X11061,empty_set),empty_set),inference(resolution,[status(thm)],[c1271, c281])).
% 31.44/31.61 cnf(c32099,plain,$false,inference(resolution,[status(thm)],[c32055, c35])).
% 31.44/31.61 % SZS output end CNFRefutation
% 31.44/31.61
% 31.44/31.61 % Initial clauses : 168
% 31.44/31.61 % Processed clauses : 1369
% 31.44/31.61 % Factors computed : 200
% 31.44/31.61 % Resolvents computed: 31580
% 31.44/31.61 % Tautologies deleted: 4
% 31.44/31.61 % Forward subsumed : 3266
% 31.44/31.61 % Backward subsumed : 5
% 31.44/31.61 % -------- CPU Time ---------
% 31.44/31.61 % User time : 31.153 s
% 31.44/31.61 % System time : 0.091 s
% 31.44/31.61 % Total time : 31.244 s
%------------------------------------------------------------------------------