%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET767+4 : TPTP v8.1.2. Released v2.2.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:40:03 EDT 2024
% Result : Theorem 2.67s 2.85s
% Output : Refutation 2.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SET767+4 : TPTP v8.1.2. Released v2.2.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n010.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 18:15:53 EDT 2024
% 0.14/0.35 % CPUTime :
% 2.67/2.85 % Version: 1.5
% 2.67/2.85 % SZS status Theorem
% 2.67/2.85 % SZS output start CNFRefutation
% 2.67/2.85 fof(thIII03,conjecture,(![E]:(![R]:(![A]:(equivalence(R,E)=>subset(equivalence_class(A,E,R),E))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thIII03)).
% 2.67/2.85 fof(c17,negated_conjecture,(~(![E]:(![R]:(![A]:(equivalence(R,E)=>subset(equivalence_class(A,E,R),E)))))),inference(assume_negation,[status(cth)],[thIII03])).
% 2.67/2.85 fof(c18,negated_conjecture,(?[E]:(?[R]:(?[A]:(equivalence(R,E)&~subset(equivalence_class(A,E,R),E))))),inference(fof_nnf,[status(thm)],[c17])).
% 2.67/2.85 fof(c19,negated_conjecture,(?[E]:(?[R]:(equivalence(R,E)&(?[A]:~subset(equivalence_class(A,E,R),E))))),inference(shift_quantors,[status(thm)],[c18])).
% 2.67/2.85 fof(c20,negated_conjecture,(?[X2]:(?[X3]:(equivalence(X3,X2)&(?[X4]:~subset(equivalence_class(X4,X2,X3),X2))))),inference(variable_rename,[status(thm)],[c19])).
% 2.67/2.85 fof(c21,negated_conjecture,(equivalence(skolem0002,skolem0001)&~subset(equivalence_class(skolem0003,skolem0001,skolem0002),skolem0001)),inference(skolemize,[status(esa)],[c20])).
% 2.67/2.85 cnf(c23,negated_conjecture,~subset(equivalence_class(skolem0003,skolem0001,skolem0002),skolem0001),inference(split_conjunct,[status(thm)],[c21])).
% 2.67/2.85 fof(subset,axiom,(![A]:(![B]:(subset(A,B)<=>(![X]:(member(X,A)=>member(X,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/SET006+0.ax', subset)).
% 2.67/2.85 fof(c222,plain,(![A]:(![B]:((~subset(A,B)|(![X]:(~member(X,A)|member(X,B))))&((?[X]:(member(X,A)&~member(X,B)))|subset(A,B))))),inference(fof_nnf,[status(thm)],[subset])).
% 2.67/2.85 fof(c223,plain,((![A]:(![B]:(~subset(A,B)|(![X]:(~member(X,A)|member(X,B))))))&(![A]:(![B]:((?[X]:(member(X,A)&~member(X,B)))|subset(A,B))))),inference(shift_quantors,[status(thm)],[c222])).
% 2.67/2.85 fof(c224,plain,((![X112]:(![X113]:(~subset(X112,X113)|(![X114]:(~member(X114,X112)|member(X114,X113))))))&(![X115]:(![X116]:((?[X117]:(member(X117,X115)&~member(X117,X116)))|subset(X115,X116))))),inference(variable_rename,[status(thm)],[c223])).
% 2.67/2.85 fof(c226,plain,(![X112]:(![X113]:(![X114]:(![X115]:(![X116]:((~subset(X112,X113)|(~member(X114,X112)|member(X114,X113)))&((member(skolem0023(X115,X116),X115)&~member(skolem0023(X115,X116),X116))|subset(X115,X116)))))))),inference(shift_quantors,[status(thm)],[fof(c225,plain,((![X112]:(![X113]:(~subset(X112,X113)|(![X114]:(~member(X114,X112)|member(X114,X113))))))&(![X115]:(![X116]:((member(skolem0023(X115,X116),X115)&~member(skolem0023(X115,X116),X116))|subset(X115,X116))))),inference(skolemize,[status(esa)],[c224])).])).
% 2.67/2.85 fof(c227,plain,(![X112]:(![X113]:(![X114]:(![X115]:(![X116]:((~subset(X112,X113)|(~member(X114,X112)|member(X114,X113)))&((member(skolem0023(X115,X116),X115)|subset(X115,X116))&(~member(skolem0023(X115,X116),X116)|subset(X115,X116))))))))),inference(distribute,[status(thm)],[c226])).
% 2.67/2.85 cnf(c230,plain,~member(skolem0023(X228,X227),X227)|subset(X228,X227),inference(split_conjunct,[status(thm)],[c227])).
% 2.67/2.85 cnf(c229,plain,member(skolem0023(X216,X215),X216)|subset(X216,X215),inference(split_conjunct,[status(thm)],[c227])).
% 2.67/2.85 fof(equivalence_class,axiom,(![R]:(![E]:(![A]:(![X]:(member(X,equivalence_class(A,E,R))<=>(member(X,E)&apply(R,A,X))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SET006+2.ax', equivalence_class)).
% 2.67/2.85 fof(c44,plain,(![R]:(![E]:(![A]:(![X]:((~member(X,equivalence_class(A,E,R))|(member(X,E)&apply(R,A,X)))&((~member(X,E)|~apply(R,A,X))|member(X,equivalence_class(A,E,R)))))))),inference(fof_nnf,[status(thm)],[equivalence_class])).
% 2.67/2.85 fof(c45,plain,((![R]:(![E]:(![A]:(![X]:(~member(X,equivalence_class(A,E,R))|(member(X,E)&apply(R,A,X)))))))&(![R]:(![E]:(![A]:(![X]:((~member(X,E)|~apply(R,A,X))|member(X,equivalence_class(A,E,R)))))))),inference(shift_quantors,[status(thm)],[c44])).
% 2.67/2.85 fof(c47,plain,(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:((~member(X20,equivalence_class(X19,X18,X17))|(member(X20,X18)&apply(X17,X19,X20)))&((~member(X24,X22)|~apply(X21,X23,X24))|member(X24,equivalence_class(X23,X22,X21)))))))))))),inference(shift_quantors,[status(thm)],[fof(c46,plain,((![X17]:(![X18]:(![X19]:(![X20]:(~member(X20,equivalence_class(X19,X18,X17))|(member(X20,X18)&apply(X17,X19,X20)))))))&(![X21]:(![X22]:(![X23]:(![X24]:((~member(X24,X22)|~apply(X21,X23,X24))|member(X24,equivalence_class(X23,X22,X21)))))))),inference(variable_rename,[status(thm)],[c45])).])).
% 2.67/2.85 fof(c48,plain,(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(((~member(X20,equivalence_class(X19,X18,X17))|member(X20,X18))&(~member(X20,equivalence_class(X19,X18,X17))|apply(X17,X19,X20)))&((~member(X24,X22)|~apply(X21,X23,X24))|member(X24,equivalence_class(X23,X22,X21)))))))))))),inference(distribute,[status(thm)],[c47])).
% 2.67/2.85 cnf(c49,plain,~member(X246,equivalence_class(X248,X245,X247))|member(X246,X245),inference(split_conjunct,[status(thm)],[c48])).
% 2.67/2.85 cnf(c317,plain,member(skolem0023(equivalence_class(X1810,X1809,X1807),X1808),X1809)|subset(equivalence_class(X1810,X1809,X1807),X1808),inference(resolution,[status(thm)],[c49, c229])).
% 2.67/2.85 cnf(c7250,plain,subset(equivalence_class(X1812,X1813,X1811),X1813),inference(resolution,[status(thm)],[c317, c230])).
% 2.67/2.85 cnf(c7260,plain,$false,inference(resolution,[status(thm)],[c7250, c23])).
% 2.67/2.85 % SZS output end CNFRefutation
% 2.67/2.85
% 2.67/2.85 % Initial clauses : 146
% 2.67/2.85 % Processed clauses : 413
% 2.67/2.85 % Factors computed : 24
% 2.67/2.85 % Resolvents computed: 7007
% 2.67/2.85 % Tautologies deleted: 2
% 2.67/2.85 % Forward subsumed : 486
% 2.67/2.85 % Backward subsumed : 4
% 2.67/2.85 % -------- CPU Time ---------
% 2.67/2.85 % User time : 2.434 s
% 2.67/2.85 % System time : 0.034 s
% 2.67/2.85 % Total time : 2.468 s
%------------------------------------------------------------------------------