%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU294+3 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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 1.79s 1.98s
% Output : Refutation 1.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SEU294+3 : TPTP v8.1.2. Released v3.2.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n008.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 12:02:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 1.79/1.98 % Version: 1.5
% 1.79/1.98 % SZS status Theorem
% 1.79/1.98 % SZS output start CNFRefutation
% 1.79/1.98 fof(t13_finset_1,conjecture,(![A]:(![B]:((subset(A,B)&finite(B))=>finite(A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t13_finset_1)).
% 1.79/1.98 fof(c46,negated_conjecture,(~(![A]:(![B]:((subset(A,B)&finite(B))=>finite(A))))),inference(assume_negation,[status(cth)],[t13_finset_1])).
% 1.79/1.98 fof(c47,negated_conjecture,(?[A]:(?[B]:((subset(A,B)&finite(B))&~finite(A)))),inference(fof_nnf,[status(thm)],[c46])).
% 1.79/1.98 fof(c48,negated_conjecture,(?[A]:((?[B]:(subset(A,B)&finite(B)))&~finite(A))),inference(shift_quantors,[status(thm)],[c47])).
% 1.79/1.98 fof(c49,negated_conjecture,(?[X21]:((?[X22]:(subset(X21,X22)&finite(X22)))&~finite(X21))),inference(variable_rename,[status(thm)],[c48])).
% 1.79/1.98 fof(c50,negated_conjecture,((subset(skolem0001,skolem0002)&finite(skolem0002))&~finite(skolem0001)),inference(skolemize,[status(esa)],[c49])).
% 1.79/1.98 cnf(c53,negated_conjecture,~finite(skolem0001),inference(split_conjunct,[status(thm)],[c50])).
% 1.79/1.98 cnf(c52,negated_conjecture,finite(skolem0002),inference(split_conjunct,[status(thm)],[c50])).
% 1.79/1.98 fof(cc2_finset_1,axiom,(![A]:(finite(A)=>(![B]:(element(B,powerset(A))=>finite(B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc2_finset_1)).
% 1.79/1.98 fof(c248,plain,(![A]:(~finite(A)|(![B]:(~element(B,powerset(A))|finite(B))))),inference(fof_nnf,[status(thm)],[cc2_finset_1])).
% 1.79/1.98 fof(c250,plain,(![X60]:(![X61]:(~finite(X60)|(~element(X61,powerset(X60))|finite(X61))))),inference(shift_quantors,[status(thm)],[fof(c249,plain,(![X60]:(~finite(X60)|(![X61]:(~element(X61,powerset(X60))|finite(X61))))),inference(variable_rename,[status(thm)],[c248])).])).
% 1.79/1.98 cnf(c251,plain,~finite(X218)|~element(X219,powerset(X218))|finite(X219),inference(split_conjunct,[status(thm)],[c250])).
% 1.79/1.98 cnf(c51,negated_conjecture,subset(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c50])).
% 1.79/1.98 fof(t3_subset,axiom,(![A]:(![B]:(element(A,powerset(B))<=>subset(A,B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t3_subset)).
% 1.79/1.98 fof(c34,plain,(![A]:(![B]:((~element(A,powerset(B))|subset(A,B))&(~subset(A,B)|element(A,powerset(B)))))),inference(fof_nnf,[status(thm)],[t3_subset])).
% 1.79/1.98 fof(c35,plain,((![A]:(![B]:(~element(A,powerset(B))|subset(A,B))))&(![A]:(![B]:(~subset(A,B)|element(A,powerset(B)))))),inference(shift_quantors,[status(thm)],[c34])).
% 1.79/1.98 fof(c37,plain,(![X13]:(![X14]:(![X15]:(![X16]:((~element(X13,powerset(X14))|subset(X13,X14))&(~subset(X15,X16)|element(X15,powerset(X16)))))))),inference(shift_quantors,[status(thm)],[fof(c36,plain,((![X13]:(![X14]:(~element(X13,powerset(X14))|subset(X13,X14))))&(![X15]:(![X16]:(~subset(X15,X16)|element(X15,powerset(X16)))))),inference(variable_rename,[status(thm)],[c35])).])).
% 1.79/1.98 cnf(c39,plain,~subset(X162,X161)|element(X162,powerset(X161)),inference(split_conjunct,[status(thm)],[c37])).
% 1.79/1.98 cnf(c373,plain,element(skolem0001,powerset(skolem0002)),inference(resolution,[status(thm)],[c39, c51])).
% 1.79/1.98 cnf(c1679,plain,~finite(skolem0002)|finite(skolem0001),inference(resolution,[status(thm)],[c373, c251])).
% 1.79/1.98 cnf(c3676,plain,finite(skolem0001),inference(resolution,[status(thm)],[c1679, c52])).
% 1.79/1.98 cnf(c3680,plain,$false,inference(resolution,[status(thm)],[c3676, c53])).
% 1.79/1.98 % SZS output end CNFRefutation
% 1.79/1.98
% 1.79/1.98 % Initial clauses : 162
% 1.79/1.98 % Processed clauses : 674
% 1.79/1.98 % Factors computed : 4
% 1.79/1.98 % Resolvents computed: 3395
% 1.79/1.98 % Tautologies deleted: 25
% 1.79/1.98 % Forward subsumed : 616
% 1.79/1.98 % Backward subsumed : 22
% 1.79/1.98 % -------- CPU Time ---------
% 1.79/1.98 % User time : 1.591 s
% 1.79/1.98 % System time : 0.017 s
% 1.79/1.98 % Total time : 1.608 s
%------------------------------------------------------------------------------