%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU294+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:41:02 EDT 2024
% Result : Theorem 197.50s 197.80s
% Output : Refutation 197.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : SEU294+2 : TPTP v8.1.2. Released v3.3.0.
% 0.09/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.16/0.37 % Computer : n029.cluster.edu
% 0.16/0.37 % Model : x86_64 x86_64
% 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.37 % Memory : 8042.1875MB
% 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.37 % CPULimit : 300
% 0.16/0.37 % WCLimit : 300
% 0.16/0.37 % DateTime : Wed May 8 12:08:38 EDT 2024
% 0.16/0.37 % CPUTime :
% 197.50/197.80 % Version: 1.5
% 197.50/197.80 % SZS status Theorem
% 197.50/197.80 % SZS output start CNFRefutation
% 197.50/197.80 fof(t13_finset_1,conjecture,(![A]:(![B]:((subset(A,B)&finite(B))=>finite(A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t13_finset_1)).
% 197.50/197.80 fof(c724,negated_conjecture,(~(![A]:(![B]:((subset(A,B)&finite(B))=>finite(A))))),inference(assume_negation,[status(cth)],[t13_finset_1])).
% 197.50/197.80 fof(c725,negated_conjecture,(?[A]:(?[B]:((subset(A,B)&finite(B))&~finite(A)))),inference(fof_nnf,[status(thm)],[c724])).
% 197.50/197.80 fof(c726,negated_conjecture,(?[A]:((?[B]:(subset(A,B)&finite(B)))&~finite(A))),inference(shift_quantors,[status(thm)],[c725])).
% 197.50/197.80 fof(c727,negated_conjecture,(?[X387]:((?[X388]:(subset(X387,X388)&finite(X388)))&~finite(X387))),inference(variable_rename,[status(thm)],[c726])).
% 197.50/197.80 fof(c728,negated_conjecture,((subset(skolem0028,skolem0029)&finite(skolem0029))&~finite(skolem0028)),inference(skolemize,[status(esa)],[c727])).
% 197.50/197.80 cnf(c731,negated_conjecture,~finite(skolem0028),inference(split_conjunct,[status(thm)],[c728])).
% 197.50/197.80 cnf(c730,negated_conjecture,finite(skolem0029),inference(split_conjunct,[status(thm)],[c728])).
% 197.50/197.80 cnf(c729,negated_conjecture,subset(skolem0028,skolem0029),inference(split_conjunct,[status(thm)],[c728])).
% 197.50/197.80 fof(t3_subset,axiom,(![A]:(![B]:(element(A,powerset(B))<=>subset(A,B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t3_subset)).
% 197.50/197.80 fof(c402,plain,(![A]:(![B]:((~element(A,powerset(B))|subset(A,B))&(~subset(A,B)|element(A,powerset(B)))))),inference(fof_nnf,[status(thm)],[t3_subset])).
% 197.50/197.80 fof(c403,plain,((![A]:(![B]:(~element(A,powerset(B))|subset(A,B))))&(![A]:(![B]:(~subset(A,B)|element(A,powerset(B)))))),inference(shift_quantors,[status(thm)],[c402])).
% 197.50/197.80 fof(c405,plain,(![X190]:(![X191]:(![X192]:(![X193]:((~element(X190,powerset(X191))|subset(X190,X191))&(~subset(X192,X193)|element(X192,powerset(X193)))))))),inference(shift_quantors,[status(thm)],[fof(c404,plain,((![X190]:(![X191]:(~element(X190,powerset(X191))|subset(X190,X191))))&(![X192]:(![X193]:(~subset(X192,X193)|element(X192,powerset(X193)))))),inference(variable_rename,[status(thm)],[c403])).])).
% 197.50/197.80 cnf(c407,plain,~subset(X2231,X2232)|element(X2231,powerset(X2232)),inference(split_conjunct,[status(thm)],[c405])).
% 197.50/197.80 cnf(c7790,plain,element(skolem0028,powerset(skolem0029)),inference(resolution,[status(thm)],[c407, c729])).
% 197.50/197.80 fof(cc2_finset_1,axiom,(![A]:(finite(A)=>(![B]:(element(B,powerset(A))=>finite(B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', cc2_finset_1)).
% 197.50/197.80 fof(c2739,plain,(![A]:(~finite(A)|(![B]:(~element(B,powerset(A))|finite(B))))),inference(fof_nnf,[status(thm)],[cc2_finset_1])).
% 197.50/197.80 fof(c2741,plain,(![X1314]:(![X1315]:(~finite(X1314)|(~element(X1315,powerset(X1314))|finite(X1315))))),inference(shift_quantors,[status(thm)],[fof(c2740,plain,(![X1314]:(~finite(X1314)|(![X1315]:(~element(X1315,powerset(X1314))|finite(X1315))))),inference(variable_rename,[status(thm)],[c2739])).])).
% 197.50/197.80 cnf(c2742,plain,~finite(X7538)|~element(X7537,powerset(X7538))|finite(X7537),inference(split_conjunct,[status(thm)],[c2741])).
% 197.50/197.80 cnf(c119408,plain,~finite(skolem0029)|finite(skolem0028),inference(resolution,[status(thm)],[c2742, c7790])).
% 197.50/197.80 cnf(c173362,plain,finite(skolem0028),inference(resolution,[status(thm)],[c119408, c730])).
% 197.50/197.80 cnf(c173365,plain,$false,inference(resolution,[status(thm)],[c173362, c731])).
% 197.50/197.80 % SZS output end CNFRefutation
% 197.50/197.80
% 197.50/197.80 % Initial clauses : 1560
% 197.50/197.80 % Processed clauses : 5160
% 197.50/197.80 % Factors computed : 233
% 197.50/197.80 % Resolvents computed: 170351
% 197.50/197.80 % Tautologies deleted: 51
% 197.50/197.80 % Forward subsumed : 3829
% 197.50/197.80 % Backward subsumed : 287
% 197.50/197.80 % -------- CPU Time ---------
% 197.50/197.80 % User time : 197.015 s
% 197.50/197.80 % System time : 0.341 s
% 197.50/197.80 % Total time : 197.356 s
%------------------------------------------------------------------------------