%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET762+4 : TPTP v8.1.2. Bugfixed v2.2.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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 40.83s 41.04s
% Output : Refutation 40.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET762+4 : TPTP v8.1.2. Bugfixed v2.2.1.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n026.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 18:42:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 40.83/41.04 % Version: 1.5
% 40.83/41.04 % SZS status Theorem
% 40.83/41.04 % SZS output start CNFRefutation
% 40.83/41.04 fof(thIIa12,conjecture,(![F]:(![A]:(![B]:(maps(F,A,B)=>equal_set(image2(F,empty_set),empty_set))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thIIa12)).
% 40.83/41.04 fof(c29,negated_conjecture,(~(![F]:(![A]:(![B]:(maps(F,A,B)=>equal_set(image2(F,empty_set),empty_set)))))),inference(assume_negation,[status(cth)],[thIIa12])).
% 40.83/41.04 fof(c30,negated_conjecture,(?[F]:(?[A]:(?[B]:(maps(F,A,B)&~equal_set(image2(F,empty_set),empty_set))))),inference(fof_nnf,[status(thm)],[c29])).
% 40.83/41.04 fof(c31,negated_conjecture,(?[F]:((?[A]:(?[B]:maps(F,A,B)))&~equal_set(image2(F,empty_set),empty_set))),inference(shift_quantors,[status(thm)],[c30])).
% 40.83/41.04 fof(c32,negated_conjecture,(?[X2]:((?[X3]:(?[X4]:maps(X2,X3,X4)))&~equal_set(image2(X2,empty_set),empty_set))),inference(variable_rename,[status(thm)],[c31])).
% 40.83/41.04 fof(c33,negated_conjecture,(maps(skolem0001,skolem0002,skolem0003)&~equal_set(image2(skolem0001,empty_set),empty_set)),inference(skolemize,[status(esa)],[c32])).
% 40.83/41.04 cnf(c35,negated_conjecture,~equal_set(image2(skolem0001,empty_set),empty_set),inference(split_conjunct,[status(thm)],[c33])).
% 40.83/41.04 fof(empty_set,axiom,(![X]:(~member(X,empty_set))),file('/export/starexec/sandbox2/benchmark/Axioms/SET006+0.ax', empty_set)).
% 40.83/41.04 fof(c279,plain,(![X]:~member(X,empty_set)),inference(fof_simplification,[status(thm)],[empty_set])).
% 40.83/41.04 fof(c280,plain,(![X233]:~member(X233,empty_set)),inference(variable_rename,[status(thm)],[c279])).
% 40.83/41.04 cnf(c281,plain,~member(X261,empty_set),inference(split_conjunct,[status(thm)],[c280])).
% 40.83/41.04 fof(subset,axiom,(![A]:(![B]:(subset(A,B)<=>(![X]:(member(X,A)=>member(X,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/SET006+0.ax', subset)).
% 40.83/41.04 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])).
% 40.83/41.04 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])).
% 40.83/41.04 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])).
% 40.83/41.04 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])).])).
% 40.83/41.04 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])).
% 40.83/41.04 cnf(c319,plain,member(skolem0043(X360,X361),X360)|subset(X360,X361),inference(split_conjunct,[status(thm)],[c317])).
% 40.83/41.04 cnf(c365,plain,subset(empty_set,X362),inference(resolution,[status(thm)],[c319, c281])).
% 40.83/41.04 fof(equal_set,axiom,(![A]:(![B]:(equal_set(A,B)<=>(subset(A,B)&subset(B,A))))),file('/export/starexec/sandbox2/benchmark/Axioms/SET006+0.ax', equal_set)).
% 40.83/41.04 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])).
% 40.83/41.04 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])).
% 40.83/41.04 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])).])).
% 40.83/41.04 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])).
% 40.83/41.04 cnf(c311,plain,~subset(X418,X419)|~subset(X419,X418)|equal_set(X418,X419),inference(split_conjunct,[status(thm)],[c308])).
% 40.83/41.04 cnf(c407,plain,~subset(X429,empty_set)|equal_set(X429,empty_set),inference(resolution,[status(thm)],[c311, c365])).
% 40.83/41.04 cnf(c418,plain,equal_set(X880,empty_set)|member(skolem0043(X880,empty_set),X880),inference(resolution,[status(thm)],[c407, c319])).
% 40.83/41.04 fof(image2,axiom,(![F]:(![A]:(![Y]:(member(Y,image2(F,A))<=>(?[X]:(member(X,A)&apply(F,X,Y))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SET006+1.ax', image2)).
% 40.83/41.04 fof(c113,plain,(![F]:(![A]:(![Y]:((~member(Y,image2(F,A))|(?[X]:(member(X,A)&apply(F,X,Y))))&((![X]:(~member(X,A)|~apply(F,X,Y)))|member(Y,image2(F,A))))))),inference(fof_nnf,[status(thm)],[image2])).
% 40.83/41.04 fof(c114,plain,((![F]:(![A]:(![Y]:(~member(Y,image2(F,A))|(?[X]:(member(X,A)&apply(F,X,Y)))))))&(![F]:(![A]:(![Y]:((![X]:(~member(X,A)|~apply(F,X,Y)))|member(Y,image2(F,A))))))),inference(shift_quantors,[status(thm)],[c113])).
% 40.83/41.04 fof(c115,plain,((![X87]:(![X88]:(![X89]:(~member(X89,image2(X87,X88))|(?[X90]:(member(X90,X88)&apply(X87,X90,X89)))))))&(![X91]:(![X92]:(![X93]:((![X94]:(~member(X94,X92)|~apply(X91,X94,X93)))|member(X93,image2(X91,X92))))))),inference(variable_rename,[status(thm)],[c114])).
% 40.83/41.04 fof(c117,plain,(![X87]:(![X88]:(![X89]:(![X91]:(![X92]:(![X93]:(![X94]:((~member(X89,image2(X87,X88))|(member(skolem0019(X87,X88,X89),X88)&apply(X87,skolem0019(X87,X88,X89),X89)))&((~member(X94,X92)|~apply(X91,X94,X93))|member(X93,image2(X91,X92))))))))))),inference(shift_quantors,[status(thm)],[fof(c116,plain,((![X87]:(![X88]:(![X89]:(~member(X89,image2(X87,X88))|(member(skolem0019(X87,X88,X89),X88)&apply(X87,skolem0019(X87,X88,X89),X89))))))&(![X91]:(![X92]:(![X93]:((![X94]:(~member(X94,X92)|~apply(X91,X94,X93)))|member(X93,image2(X91,X92))))))),inference(skolemize,[status(esa)],[c115])).])).
% 40.83/41.04 fof(c118,plain,(![X87]:(![X88]:(![X89]:(![X91]:(![X92]:(![X93]:(![X94]:(((~member(X89,image2(X87,X88))|member(skolem0019(X87,X88,X89),X88))&(~member(X89,image2(X87,X88))|apply(X87,skolem0019(X87,X88,X89),X89)))&((~member(X94,X92)|~apply(X91,X94,X93))|member(X93,image2(X91,X92))))))))))),inference(distribute,[status(thm)],[c117])).
% 40.83/41.04 cnf(c119,plain,~member(X1319,image2(X1320,X1321))|member(skolem0019(X1320,X1321,X1319),X1321),inference(split_conjunct,[status(thm)],[c118])).
% 40.83/41.04 cnf(c1351,plain,member(skolem0019(X12345,X12344,skolem0043(image2(X12345,X12344),empty_set)),X12344)|equal_set(image2(X12345,X12344),empty_set),inference(resolution,[status(thm)],[c119, c418])).
% 40.83/41.04 cnf(c39663,plain,equal_set(image2(X12346,empty_set),empty_set),inference(resolution,[status(thm)],[c1351, c281])).
% 40.83/41.04 cnf(c39684,plain,$false,inference(resolution,[status(thm)],[c39663, c35])).
% 40.83/41.04 % SZS output end CNFRefutation
% 40.83/41.04
% 40.83/41.04 % Initial clauses : 168
% 40.83/41.04 % Processed clauses : 1485
% 40.83/41.04 % Factors computed : 200
% 40.83/41.04 % Resolvents computed: 39165
% 40.83/41.04 % Tautologies deleted: 4
% 40.83/41.04 % Forward subsumed : 3630
% 40.83/41.04 % Backward subsumed : 9
% 40.83/41.04 % -------- CPU Time ---------
% 40.83/41.04 % User time : 40.604 s
% 40.83/41.04 % System time : 0.094 s
% 40.83/41.04 % Total time : 40.698 s
%------------------------------------------------------------------------------