%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU294+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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.02s 1.22s
% Output : Refutation 1.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SEU294+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n010.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 11:52:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 1.02/1.22 % Version: 1.5
% 1.02/1.22 % SZS status Theorem
% 1.02/1.22 % SZS output start CNFRefutation
% 1.02/1.22 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.02/1.22 fof(c41,negated_conjecture,(~(![A]:(![B]:((subset(A,B)&finite(B))=>finite(A))))),inference(assume_negation,[status(cth)],[t13_finset_1])).
% 1.02/1.22 fof(c42,negated_conjecture,(?[A]:(?[B]:((subset(A,B)&finite(B))&~finite(A)))),inference(fof_nnf,[status(thm)],[c41])).
% 1.02/1.22 fof(c43,negated_conjecture,(?[A]:((?[B]:(subset(A,B)&finite(B)))&~finite(A))),inference(shift_quantors,[status(thm)],[c42])).
% 1.02/1.22 fof(c44,negated_conjecture,(?[X21]:((?[X22]:(subset(X21,X22)&finite(X22)))&~finite(X21))),inference(variable_rename,[status(thm)],[c43])).
% 1.02/1.22 fof(c45,negated_conjecture,((subset(skolem0001,skolem0002)&finite(skolem0002))&~finite(skolem0001)),inference(skolemize,[status(esa)],[c44])).
% 1.02/1.22 cnf(c48,negated_conjecture,~finite(skolem0001),inference(split_conjunct,[status(thm)],[c45])).
% 1.02/1.22 cnf(c47,negated_conjecture,finite(skolem0002),inference(split_conjunct,[status(thm)],[c45])).
% 1.02/1.22 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.02/1.22 fof(c194,plain,(![A]:(~finite(A)|(![B]:(~element(B,powerset(A))|finite(B))))),inference(fof_nnf,[status(thm)],[cc2_finset_1])).
% 1.02/1.22 fof(c196,plain,(![X52]:(![X53]:(~finite(X52)|(~element(X53,powerset(X52))|finite(X53))))),inference(shift_quantors,[status(thm)],[fof(c195,plain,(![X52]:(~finite(X52)|(![X53]:(~element(X53,powerset(X52))|finite(X53))))),inference(variable_rename,[status(thm)],[c194])).])).
% 1.02/1.22 cnf(c197,plain,~finite(X194)|~element(X195,powerset(X194))|finite(X195),inference(split_conjunct,[status(thm)],[c196])).
% 1.02/1.22 cnf(c46,negated_conjecture,subset(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c45])).
% 1.02/1.22 fof(t3_subset,axiom,(![A]:(![B]:(element(A,powerset(B))<=>subset(A,B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t3_subset)).
% 1.02/1.22 fof(c29,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.02/1.22 fof(c30,plain,((![A]:(![B]:(~element(A,powerset(B))|subset(A,B))))&(![A]:(![B]:(~subset(A,B)|element(A,powerset(B)))))),inference(shift_quantors,[status(thm)],[c29])).
% 1.02/1.22 fof(c32,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(c31,plain,((![X13]:(![X14]:(~element(X13,powerset(X14))|subset(X13,X14))))&(![X15]:(![X16]:(~subset(X15,X16)|element(X15,powerset(X16)))))),inference(variable_rename,[status(thm)],[c30])).])).
% 1.02/1.22 cnf(c34,plain,~subset(X143,X144)|element(X143,powerset(X144)),inference(split_conjunct,[status(thm)],[c32])).
% 1.02/1.22 cnf(c303,plain,element(skolem0001,powerset(skolem0002)),inference(resolution,[status(thm)],[c34, c46])).
% 1.02/1.22 cnf(c1096,plain,~finite(skolem0002)|finite(skolem0001),inference(resolution,[status(thm)],[c303, c197])).
% 1.02/1.22 cnf(c2486,plain,finite(skolem0001),inference(resolution,[status(thm)],[c1096, c47])).
% 1.02/1.22 cnf(c2489,plain,$false,inference(resolution,[status(thm)],[c2486, c48])).
% 1.02/1.22 % SZS output end CNFRefutation
% 1.02/1.22
% 1.02/1.22 % Initial clauses : 127
% 1.02/1.22 % Processed clauses : 401
% 1.02/1.22 % Factors computed : 4
% 1.02/1.22 % Resolvents computed: 2256
% 1.02/1.22 % Tautologies deleted: 19
% 1.02/1.22 % Forward subsumed : 398
% 1.02/1.22 % Backward subsumed : 24
% 1.02/1.22 % -------- CPU Time ---------
% 1.02/1.22 % User time : 0.848 s
% 1.02/1.22 % System time : 0.016 s
% 1.02/1.22 % Total time : 0.864 s
%------------------------------------------------------------------------------