%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU094+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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:33 EDT 2024
% Result : Theorem 204.88s 205.12s
% Output : Refutation 204.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SEU094+1 : TPTP v8.1.2. Released v3.2.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n011.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 11:41:23 EDT 2024
% 0.15/0.36 % CPUTime :
% 204.88/205.12 % Version: 1.5
% 204.88/205.12 % SZS status Theorem
% 204.88/205.12 % SZS output start CNFRefutation
% 204.88/205.12 fof(t25_finset_1,conjecture,(![A]:((finite(A)&(![B]:(in(B,A)=>finite(B))))<=>finite(union(A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t25_finset_1)).
% 204.88/205.12 fof(c47,negated_conjecture,(~(![A]:((finite(A)&(![B]:(in(B,A)=>finite(B))))<=>finite(union(A))))),inference(assume_negation,[status(cth)],[t25_finset_1])).
% 204.88/205.12 fof(c48,negated_conjecture,(?[A]:(((~finite(A)|(?[B]:(in(B,A)&~finite(B))))|~finite(union(A)))&((finite(A)&(![B]:(~in(B,A)|finite(B))))|finite(union(A))))),inference(fof_nnf,[status(thm)],[c47])).
% 204.88/205.12 fof(c49,negated_conjecture,(?[X21]:(((~finite(X21)|(?[X22]:(in(X22,X21)&~finite(X22))))|~finite(union(X21)))&((finite(X21)&(![X23]:(~in(X23,X21)|finite(X23))))|finite(union(X21))))),inference(variable_rename,[status(thm)],[c48])).
% 204.88/205.12 fof(c51,negated_conjecture,(![X23]:(((~finite(skolem0001)|(in(skolem0002,skolem0001)&~finite(skolem0002)))|~finite(union(skolem0001)))&((finite(skolem0001)&(~in(X23,skolem0001)|finite(X23)))|finite(union(skolem0001))))),inference(shift_quantors,[status(thm)],[fof(c50,negated_conjecture,(((~finite(skolem0001)|(in(skolem0002,skolem0001)&~finite(skolem0002)))|~finite(union(skolem0001)))&((finite(skolem0001)&(![X23]:(~in(X23,skolem0001)|finite(X23))))|finite(union(skolem0001)))),inference(skolemize,[status(esa)],[c49])).])).
% 204.88/205.12 fof(c52,negated_conjecture,(![X23]:((((~finite(skolem0001)|in(skolem0002,skolem0001))|~finite(union(skolem0001)))&((~finite(skolem0001)|~finite(skolem0002))|~finite(union(skolem0001))))&((finite(skolem0001)|finite(union(skolem0001)))&((~in(X23,skolem0001)|finite(X23))|finite(union(skolem0001)))))),inference(distribute,[status(thm)],[c51])).
% 204.88/205.12 cnf(c55,negated_conjecture,finite(skolem0001)|finite(union(skolem0001)),inference(split_conjunct,[status(thm)],[c52])).
% 204.88/205.12 fof(t24_finset_1,axiom,(![A]:(finite(A)<=>finite(powerset(A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t24_finset_1)).
% 204.88/205.12 fof(c57,plain,(![A]:((~finite(A)|finite(powerset(A)))&(~finite(powerset(A))|finite(A)))),inference(fof_nnf,[status(thm)],[t24_finset_1])).
% 204.88/205.12 fof(c58,plain,((![A]:(~finite(A)|finite(powerset(A))))&(![A]:(~finite(powerset(A))|finite(A)))),inference(shift_quantors,[status(thm)],[c57])).
% 204.88/205.12 fof(c60,plain,(![X24]:(![X25]:((~finite(X24)|finite(powerset(X24)))&(~finite(powerset(X25))|finite(X25))))),inference(shift_quantors,[status(thm)],[fof(c59,plain,((![X24]:(~finite(X24)|finite(powerset(X24))))&(![X25]:(~finite(powerset(X25))|finite(X25)))),inference(variable_rename,[status(thm)],[c58])).])).
% 204.88/205.12 cnf(c61,plain,~finite(X192)|finite(powerset(X192)),inference(split_conjunct,[status(thm)],[c60])).
% 204.88/205.12 cnf(c444,plain,finite(powerset(union(skolem0001)))|finite(skolem0001),inference(resolution,[status(thm)],[c61, c55])).
% 204.88/205.12 fof(t13_finset_1,axiom,(![A]:(![B]:((subset(A,B)&finite(B))=>finite(A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t13_finset_1)).
% 204.88/205.12 fof(c66,plain,(![A]:(![B]:((~subset(A,B)|~finite(B))|finite(A)))),inference(fof_nnf,[status(thm)],[t13_finset_1])).
% 204.88/205.12 fof(c67,plain,(![A]:((![B]:(~subset(A,B)|~finite(B)))|finite(A))),inference(shift_quantors,[status(thm)],[c66])).
% 204.88/205.12 fof(c69,plain,(![X28]:(![X29]:((~subset(X28,X29)|~finite(X29))|finite(X28)))),inference(shift_quantors,[status(thm)],[fof(c68,plain,(![X28]:((![X29]:(~subset(X28,X29)|~finite(X29)))|finite(X28))),inference(variable_rename,[status(thm)],[c67])).])).
% 204.88/205.12 cnf(c70,plain,~subset(X212,X211)|~finite(X211)|finite(X212),inference(split_conjunct,[status(thm)],[c69])).
% 204.88/205.12 fof(t100_zfmisc_1,axiom,(![A]:subset(A,powerset(union(A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t100_zfmisc_1)).
% 204.88/205.12 fof(c71,plain,(![X30]:subset(X30,powerset(union(X30)))),inference(variable_rename,[status(thm)],[t100_zfmisc_1])).
% 204.88/205.12 cnf(c72,plain,subset(X213,powerset(union(X213))),inference(split_conjunct,[status(thm)],[c71])).
% 204.88/205.12 cnf(c527,plain,~finite(powerset(union(X365)))|finite(X365),inference(resolution,[status(thm)],[c72, c70])).
% 204.88/205.12 cnf(c2255,plain,finite(skolem0001),inference(resolution,[status(thm)],[c527, c444])).
% 204.88/205.12 cnf(c54,negated_conjecture,~finite(skolem0001)|~finite(skolem0002)|~finite(union(skolem0001)),inference(split_conjunct,[status(thm)],[c52])).
% 204.88/205.12 fof(l22_finset_1,axiom,(![A]:((finite(A)&(![B]:(in(B,A)=>finite(B))))=>finite(union(A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l22_finset_1)).
% 204.88/205.12 fof(c223,plain,(![A]:((~finite(A)|(?[B]:(in(B,A)&~finite(B))))|finite(union(A)))),inference(fof_nnf,[status(thm)],[l22_finset_1])).
% 204.88/205.12 fof(c224,plain,(![X61]:((~finite(X61)|(?[X62]:(in(X62,X61)&~finite(X62))))|finite(union(X61)))),inference(variable_rename,[status(thm)],[c223])).
% 204.88/205.12 fof(c225,plain,(![X61]:((~finite(X61)|(in(skolem0028(X61),X61)&~finite(skolem0028(X61))))|finite(union(X61)))),inference(skolemize,[status(esa)],[c224])).
% 204.88/205.12 fof(c226,plain,(![X61]:(((~finite(X61)|in(skolem0028(X61),X61))|finite(union(X61)))&((~finite(X61)|~finite(skolem0028(X61)))|finite(union(X61))))),inference(distribute,[status(thm)],[c225])).
% 204.88/205.12 cnf(c228,plain,~finite(X236)|~finite(skolem0028(X236))|finite(union(X236)),inference(split_conjunct,[status(thm)],[c226])).
% 204.88/205.12 cnf(c56,negated_conjecture,~in(X189,skolem0001)|finite(X189)|finite(union(skolem0001)),inference(split_conjunct,[status(thm)],[c52])).
% 204.88/205.12 cnf(c227,plain,~finite(X229)|in(skolem0028(X229),X229)|finite(union(X229)),inference(split_conjunct,[status(thm)],[c226])).
% 204.88/205.12 cnf(c807,plain,in(skolem0028(skolem0001),skolem0001)|finite(union(skolem0001)),inference(resolution,[status(thm)],[c227, c55])).
% 204.88/205.12 cnf(c4555,plain,finite(union(skolem0001))|finite(skolem0028(skolem0001)),inference(resolution,[status(thm)],[c807, c56])).
% 204.88/205.12 cnf(c115971,plain,finite(union(skolem0001))|~finite(skolem0001),inference(resolution,[status(thm)],[c4555, c228])).
% 204.88/205.12 cnf(c115987,plain,finite(union(skolem0001)),inference(resolution,[status(thm)],[c115971, c2255])).
% 204.88/205.12 cnf(c116008,plain,~finite(skolem0001)|~finite(skolem0002),inference(resolution,[status(thm)],[c115987, c54])).
% 204.88/205.12 fof(t92_zfmisc_1,axiom,(![A]:(![B]:(in(A,B)=>subset(A,union(B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t92_zfmisc_1)).
% 204.88/205.12 fof(c20,plain,(![A]:(![B]:(~in(A,B)|subset(A,union(B))))),inference(fof_nnf,[status(thm)],[t92_zfmisc_1])).
% 204.88/205.12 fof(c21,plain,(![X2]:(![X3]:(~in(X2,X3)|subset(X2,union(X3))))),inference(variable_rename,[status(thm)],[c20])).
% 204.88/205.12 cnf(c22,plain,~in(X153,X154)|subset(X153,union(X154)),inference(split_conjunct,[status(thm)],[c21])).
% 204.88/205.12 cnf(c53,negated_conjecture,~finite(skolem0001)|in(skolem0002,skolem0001)|~finite(union(skolem0001)),inference(split_conjunct,[status(thm)],[c52])).
% 204.88/205.12 cnf(c116013,plain,~finite(skolem0001)|in(skolem0002,skolem0001),inference(resolution,[status(thm)],[c115987, c53])).
% 204.88/205.12 cnf(c116061,plain,in(skolem0002,skolem0001),inference(resolution,[status(thm)],[c116013, c2255])).
% 204.88/205.12 cnf(c116082,plain,subset(skolem0002,union(skolem0001)),inference(resolution,[status(thm)],[c116061, c22])).
% 204.88/205.12 cnf(c116168,plain,~finite(union(skolem0001))|finite(skolem0002),inference(resolution,[status(thm)],[c116082, c70])).
% 204.88/205.12 cnf(c117266,plain,finite(skolem0002),inference(resolution,[status(thm)],[c116168, c115987])).
% 204.88/205.12 cnf(c117274,plain,~finite(skolem0001),inference(resolution,[status(thm)],[c117266, c116008])).
% 204.88/205.12 cnf(c117291,plain,$false,inference(resolution,[status(thm)],[c117274, c2255])).
% 204.88/205.12 % SZS output end CNFRefutation
% 204.88/205.12
% 204.88/205.12 % Initial clauses : 174
% 204.88/205.12 % Processed clauses : 4202
% 204.88/205.12 % Factors computed : 13
% 204.88/205.12 % Resolvents computed: 116979
% 204.88/205.12 % Tautologies deleted: 46
% 204.88/205.12 % Forward subsumed : 9442
% 204.88/205.12 % Backward subsumed : 289
% 204.88/205.12 % -------- CPU Time ---------
% 204.88/205.12 % User time : 204.504 s
% 204.88/205.12 % System time : 0.200 s
% 204.88/205.12 % Total time : 204.704 s
%------------------------------------------------------------------------------