%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET095+4 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:39:11 EDT 2024
% Result : Theorem 9.34s 9.56s
% Output : Refutation 9.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SET095+4 : TPTP v8.1.2. Released v2.2.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n005.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 19:20:08 EDT 2024
% 0.15/0.36 % CPUTime :
% 9.34/9.56 % Version: 1.5
% 9.34/9.56 % SZS status Theorem
% 9.34/9.56 % SZS output start CNFRefutation
% 9.34/9.56 fof(thI44,conjecture,(![A]:(![X]:(member(X,A)=>subset(singleton(X),A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thI44)).
% 9.34/9.56 fof(c11,negated_conjecture,(~(![A]:(![X]:(member(X,A)=>subset(singleton(X),A))))),inference(assume_negation,[status(cth)],[thI44])).
% 9.34/9.56 fof(c12,negated_conjecture,(?[A]:(?[X]:(member(X,A)&~subset(singleton(X),A)))),inference(fof_nnf,[status(thm)],[c11])).
% 9.34/9.56 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(member(X3,X2)&~subset(singleton(X3),X2)))),inference(variable_rename,[status(thm)],[c12])).
% 9.34/9.56 fof(c14,negated_conjecture,(member(skolem0002,skolem0001)&~subset(singleton(skolem0002),skolem0001)),inference(skolemize,[status(esa)],[c13])).
% 9.34/9.56 cnf(c16,negated_conjecture,~subset(singleton(skolem0002),skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 9.34/9.56 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)).
% 9.34/9.56 fof(c91,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])).
% 9.41/9.56 fof(c92,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)],[c91])).
% 9.41/9.56 fof(c93,plain,((![X53]:(![X54]:(~subset(X53,X54)|(![X55]:(~member(X55,X53)|member(X55,X54))))))&(![X56]:(![X57]:((?[X58]:(member(X58,X56)&~member(X58,X57)))|subset(X56,X57))))),inference(variable_rename,[status(thm)],[c92])).
% 9.41/9.56 fof(c95,plain,(![X53]:(![X54]:(![X55]:(![X56]:(![X57]:((~subset(X53,X54)|(~member(X55,X53)|member(X55,X54)))&((member(skolem0005(X56,X57),X56)&~member(skolem0005(X56,X57),X57))|subset(X56,X57)))))))),inference(shift_quantors,[status(thm)],[fof(c94,plain,((![X53]:(![X54]:(~subset(X53,X54)|(![X55]:(~member(X55,X53)|member(X55,X54))))))&(![X56]:(![X57]:((member(skolem0005(X56,X57),X56)&~member(skolem0005(X56,X57),X57))|subset(X56,X57))))),inference(skolemize,[status(esa)],[c93])).])).
% 9.41/9.56 fof(c96,plain,(![X53]:(![X54]:(![X55]:(![X56]:(![X57]:((~subset(X53,X54)|(~member(X55,X53)|member(X55,X54)))&((member(skolem0005(X56,X57),X56)|subset(X56,X57))&(~member(skolem0005(X56,X57),X57)|subset(X56,X57))))))))),inference(distribute,[status(thm)],[c95])).
% 9.41/9.56 cnf(c99,plain,~member(skolem0005(X165,X164),X164)|subset(X165,X164),inference(split_conjunct,[status(thm)],[c96])).
% 9.41/9.56 cnf(reflexivity,axiom,X59=X59,theory(equality)).
% 9.41/9.56 cnf(c15,negated_conjecture,member(skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 9.41/9.56 cnf(c9,axiom,X186!=X188|X187!=X189|~member(X186,X187)|member(X188,X189),theory(equality)).
% 9.41/9.56 cnf(c200,plain,skolem0002!=X871|skolem0001!=X872|member(X871,X872),inference(resolution,[status(thm)],[c9, c15])).
% 9.41/9.56 cnf(c2007,plain,skolem0002!=X873|member(X873,skolem0001),inference(resolution,[status(thm)],[c200, reflexivity])).
% 9.41/9.56 cnf(symmetry,axiom,X61!=X62|X62=X61,theory(equality)).
% 9.41/9.56 fof(singleton,axiom,(![X]:(![A]:(member(X,singleton(A))<=>X=A))),file('/export/starexec/sandbox2/benchmark/Axioms/SET006+0.ax', singleton)).
% 9.41/9.56 fof(c43,plain,(![X]:(![A]:((~member(X,singleton(A))|X=A)&(X!=A|member(X,singleton(A)))))),inference(fof_nnf,[status(thm)],[singleton])).
% 9.41/9.56 fof(c44,plain,((![X]:(![A]:(~member(X,singleton(A))|X=A)))&(![X]:(![A]:(X!=A|member(X,singleton(A)))))),inference(shift_quantors,[status(thm)],[c43])).
% 9.41/9.56 fof(c46,plain,(![X22]:(![X23]:(![X24]:(![X25]:((~member(X22,singleton(X23))|X22=X23)&(X24!=X25|member(X24,singleton(X25)))))))),inference(shift_quantors,[status(thm)],[fof(c45,plain,((![X22]:(![X23]:(~member(X22,singleton(X23))|X22=X23)))&(![X24]:(![X25]:(X24!=X25|member(X24,singleton(X25)))))),inference(variable_rename,[status(thm)],[c44])).])).
% 9.41/9.56 cnf(c47,plain,~member(X78,singleton(X77))|X78=X77,inference(split_conjunct,[status(thm)],[c46])).
% 9.41/9.56 cnf(c98,plain,member(skolem0005(X153,X152),X153)|subset(X153,X152),inference(split_conjunct,[status(thm)],[c96])).
% 9.41/9.56 cnf(c146,plain,subset(singleton(X537),X536)|skolem0005(singleton(X537),X536)=X537,inference(resolution,[status(thm)],[c98, c47])).
% 9.41/9.56 cnf(c1147,plain,skolem0005(singleton(skolem0002),skolem0001)=skolem0002,inference(resolution,[status(thm)],[c146, c16])).
% 9.41/9.56 cnf(c1878,plain,skolem0002=skolem0005(singleton(skolem0002),skolem0001),inference(resolution,[status(thm)],[c1147, symmetry])).
% 9.41/9.56 cnf(c7741,plain,member(skolem0005(singleton(skolem0002),skolem0001),skolem0001),inference(resolution,[status(thm)],[c1878, c2007])).
% 9.41/9.56 cnf(c24205,plain,subset(singleton(skolem0002),skolem0001),inference(resolution,[status(thm)],[c7741, c99])).
% 9.41/9.56 cnf(c24230,plain,$false,inference(resolution,[status(thm)],[c24205, c16])).
% 9.41/9.56 % SZS output end CNFRefutation
% 9.41/9.56
% 9.41/9.56 % Initial clauses : 45
% 9.41/9.56 % Processed clauses : 565
% 9.41/9.56 % Factors computed : 27
% 9.41/9.56 % Resolvents computed: 24106
% 9.41/9.56 % Tautologies deleted: 30
% 9.41/9.56 % Forward subsumed : 1147
% 9.41/9.56 % Backward subsumed : 3
% 9.41/9.56 % -------- CPU Time ---------
% 9.41/9.56 % User time : 9.142 s
% 9.41/9.56 % System time : 0.050 s
% 9.41/9.56 % Total time : 9.192 s
%------------------------------------------------------------------------------