%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET900+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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:19 EDT 2024
% Result : Theorem 0.38s 0.57s
% Output : Refutation 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SET900+1 : TPTP v8.1.2. Released v3.2.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n024.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:31:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.38/0.57 % Version: 1.5
% 0.38/0.57 % SZS status Theorem
% 0.38/0.57 % SZS output start CNFRefutation
% 0.38/0.57 fof(t41_zfmisc_1,conjecture,(![A]:(![B]:(~((A!=singleton(B)&A!=empty_set)&(![C]:(~(in(C,A)&C!=B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t41_zfmisc_1)).
% 0.38/0.57 fof(c9,negated_conjecture,(~(![A]:(![B]:(~((A!=singleton(B)&A!=empty_set)&(![C]:(~(in(C,A)&C!=B)))))))),inference(assume_negation,[status(cth)],[t41_zfmisc_1])).
% 0.38/0.57 fof(c10,negated_conjecture,(?[A]:(?[B]:((A!=singleton(B)&A!=empty_set)&(![C]:(~in(C,A)|C=B))))),inference(fof_nnf,[status(thm)],[c9])).
% 0.38/0.57 fof(c11,negated_conjecture,(?[X5]:(?[X6]:((X5!=singleton(X6)&X5!=empty_set)&(![X7]:(~in(X7,X5)|X7=X6))))),inference(variable_rename,[status(thm)],[c10])).
% 0.38/0.57 fof(c13,negated_conjecture,(![X7]:((skolem0002!=singleton(skolem0003)&skolem0002!=empty_set)&(~in(X7,skolem0002)|X7=skolem0003))),inference(shift_quantors,[status(thm)],[fof(c12,negated_conjecture,((skolem0002!=singleton(skolem0003)&skolem0002!=empty_set)&(![X7]:(~in(X7,skolem0002)|X7=skolem0003))),inference(skolemize,[status(esa)],[c11])).])).
% 0.38/0.57 cnf(c15,negated_conjecture,skolem0002!=empty_set,inference(split_conjunct,[status(thm)],[c13])).
% 0.38/0.57 cnf(c14,negated_conjecture,skolem0002!=singleton(skolem0003),inference(split_conjunct,[status(thm)],[c13])).
% 0.38/0.57 cnf(c16,negated_conjecture,~in(X28,skolem0002)|X28=skolem0003,inference(split_conjunct,[status(thm)],[c13])).
% 0.38/0.57 fof(l45_zfmisc_1,axiom,(![A]:(![B]:(~((A!=singleton(B)&A!=empty_set)&(![C]:(~(in(C,A)&C!=B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', l45_zfmisc_1)).
% 0.38/0.57 fof(c3,plain,(![A]:(![B]:((A=singleton(B)|A=empty_set)|(?[C]:(in(C,A)&C!=B))))),inference(fof_nnf,[status(thm)],[l45_zfmisc_1])).
% 0.38/0.57 fof(c4,plain,(![X2]:(![X3]:((X2=singleton(X3)|X2=empty_set)|(?[X4]:(in(X4,X2)&X4!=X3))))),inference(variable_rename,[status(thm)],[c3])).
% 0.38/0.57 fof(c5,plain,(![X2]:(![X3]:((X2=singleton(X3)|X2=empty_set)|(in(skolem0001(X2,X3),X2)&skolem0001(X2,X3)!=X3)))),inference(skolemize,[status(esa)],[c4])).
% 0.38/0.57 fof(c6,plain,(![X2]:(![X3]:(((X2=singleton(X3)|X2=empty_set)|in(skolem0001(X2,X3),X2))&((X2=singleton(X3)|X2=empty_set)|skolem0001(X2,X3)!=X3)))),inference(distribute,[status(thm)],[c5])).
% 0.38/0.57 cnf(c7,plain,X36=singleton(X37)|X36=empty_set|in(skolem0001(X36,X37),X36),inference(split_conjunct,[status(thm)],[c6])).
% 0.38/0.57 cnf(c36,plain,skolem0002=empty_set|in(skolem0001(skolem0002,skolem0003),skolem0002),inference(resolution,[status(thm)],[c7, c14])).
% 0.38/0.57 cnf(c51,plain,in(skolem0001(skolem0002,skolem0003),skolem0002),inference(resolution,[status(thm)],[c36, c15])).
% 0.38/0.57 cnf(c57,plain,skolem0001(skolem0002,skolem0003)=skolem0003,inference(resolution,[status(thm)],[c51, c16])).
% 0.38/0.57 cnf(c8,plain,X38=singleton(X39)|X38=empty_set|skolem0001(X38,X39)!=X39,inference(split_conjunct,[status(thm)],[c6])).
% 0.38/0.57 cnf(c63,plain,skolem0002=singleton(skolem0003)|skolem0002=empty_set,inference(resolution,[status(thm)],[c8, c57])).
% 0.38/0.57 cnf(c79,plain,skolem0002=empty_set,inference(resolution,[status(thm)],[c63, c14])).
% 0.38/0.57 cnf(c104,plain,$false,inference(resolution,[status(thm)],[c79, c15])).
% 0.38/0.57 % SZS output end CNFRefutation
% 0.38/0.57
% 0.38/0.57 % Initial clauses : 15
% 0.38/0.57 % Processed clauses : 29
% 0.38/0.57 % Factors computed : 2
% 0.38/0.57 % Resolvents computed: 75
% 0.38/0.57 % Tautologies deleted: 3
% 0.38/0.57 % Forward subsumed : 5
% 0.38/0.57 % Backward subsumed : 2
% 0.38/0.57 % -------- CPU Time ---------
% 0.38/0.57 % User time : 0.199 s
% 0.38/0.57 % System time : 0.010 s
% 0.38/0.57 % Total time : 0.209 s
%------------------------------------------------------------------------------