%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET704+4 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:59 EDT 2024
% Result : Theorem 111.48s 111.72s
% Output : Refutation 111.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SET704+4 : TPTP v8.1.2. Released v2.2.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n029.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:00:23 EDT 2024
% 0.15/0.36 % CPUTime :
% 111.48/111.72 % Version: 1.5
% 111.48/111.72 % SZS status Theorem
% 111.48/111.72 % SZS output start CNFRefutation
% 111.48/111.72 fof(thI42,conjecture,(![A]:(![X]:(member(X,A)=>subset(product(A),X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', thI42)).
% 111.48/111.72 fof(c11,negated_conjecture,(~(![A]:(![X]:(member(X,A)=>subset(product(A),X))))),inference(assume_negation,[status(cth)],[thI42])).
% 111.48/111.72 fof(c12,negated_conjecture,(?[A]:(?[X]:(member(X,A)&~subset(product(A),X)))),inference(fof_nnf,[status(thm)],[c11])).
% 111.48/111.72 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(member(X3,X2)&~subset(product(X2),X3)))),inference(variable_rename,[status(thm)],[c12])).
% 111.48/111.72 fof(c14,negated_conjecture,(member(skolem0002,skolem0001)&~subset(product(skolem0001),skolem0002)),inference(skolemize,[status(esa)],[c13])).
% 111.48/111.72 cnf(c16,negated_conjecture,~subset(product(skolem0001),skolem0002),inference(split_conjunct,[status(thm)],[c14])).
% 111.48/111.72 fof(subset,axiom,(![A]:(![B]:(subset(A,B)<=>(![X]:(member(X,A)=>member(X,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', subset)).
% 111.48/111.72 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])).
% 111.48/111.72 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])).
% 111.48/111.72 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])).
% 111.48/111.72 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])).])).
% 111.48/111.72 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])).
% 111.48/111.72 cnf(c99,plain,~member(skolem0005(X164,X165),X165)|subset(X164,X165),inference(split_conjunct,[status(thm)],[c96])).
% 111.48/111.72 cnf(c15,negated_conjecture,member(skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 111.48/111.72 fof(product,axiom,(![X]:(![A]:(member(X,product(A))<=>(![Y]:(member(Y,A)=>member(X,Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', product)).
% 111.48/111.72 fof(c17,plain,(![X]:(![A]:((~member(X,product(A))|(![Y]:(~member(Y,A)|member(X,Y))))&((?[Y]:(member(Y,A)&~member(X,Y)))|member(X,product(A)))))),inference(fof_nnf,[status(thm)],[product])).
% 111.48/111.72 fof(c18,plain,((![X]:(![A]:(~member(X,product(A))|(![Y]:(~member(Y,A)|member(X,Y))))))&(![X]:(![A]:((?[Y]:(member(Y,A)&~member(X,Y)))|member(X,product(A)))))),inference(shift_quantors,[status(thm)],[c17])).
% 111.48/111.72 fof(c19,plain,((![X4]:(![X5]:(~member(X4,product(X5))|(![X6]:(~member(X6,X5)|member(X4,X6))))))&(![X7]:(![X8]:((?[X9]:(member(X9,X8)&~member(X7,X9)))|member(X7,product(X8)))))),inference(variable_rename,[status(thm)],[c18])).
% 111.48/111.72 fof(c21,plain,(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:((~member(X4,product(X5))|(~member(X6,X5)|member(X4,X6)))&((member(skolem0003(X7,X8),X8)&~member(X7,skolem0003(X7,X8)))|member(X7,product(X8))))))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,((![X4]:(![X5]:(~member(X4,product(X5))|(![X6]:(~member(X6,X5)|member(X4,X6))))))&(![X7]:(![X8]:((member(skolem0003(X7,X8),X8)&~member(X7,skolem0003(X7,X8)))|member(X7,product(X8)))))),inference(skolemize,[status(esa)],[c19])).])).
% 111.48/111.72 fof(c22,plain,(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:((~member(X4,product(X5))|(~member(X6,X5)|member(X4,X6)))&((member(skolem0003(X7,X8),X8)|member(X7,product(X8)))&(~member(X7,skolem0003(X7,X8))|member(X7,product(X8)))))))))),inference(distribute,[status(thm)],[c21])).
% 111.48/111.72 cnf(c23,plain,~member(X206,product(X207))|~member(X205,X207)|member(X206,X205),inference(split_conjunct,[status(thm)],[c22])).
% 111.48/111.72 cnf(c98,plain,member(skolem0005(X152,X153),X152)|subset(X152,X153),inference(split_conjunct,[status(thm)],[c96])).
% 111.48/111.72 cnf(c151,plain,member(skolem0005(product(skolem0001),skolem0002),product(skolem0001)),inference(resolution,[status(thm)],[c98, c16])).
% 111.48/111.72 cnf(c1273,plain,~member(X10144,skolem0001)|member(skolem0005(product(skolem0001),skolem0002),X10144),inference(resolution,[status(thm)],[c151, c23])).
% 111.48/111.72 cnf(c128393,plain,member(skolem0005(product(skolem0001),skolem0002),skolem0002),inference(resolution,[status(thm)],[c1273, c15])).
% 111.48/111.72 cnf(c128495,plain,subset(product(skolem0001),skolem0002),inference(resolution,[status(thm)],[c128393, c99])).
% 111.48/111.72 cnf(c128559,plain,$false,inference(resolution,[status(thm)],[c128495, c16])).
% 111.48/111.72 % SZS output end CNFRefutation
% 111.48/111.72
% 111.48/111.72 % Initial clauses : 45
% 111.48/111.72 % Processed clauses : 1394
% 111.48/111.72 % Factors computed : 59
% 111.48/111.72 % Resolvents computed: 128413
% 111.48/111.72 % Tautologies deleted: 65
% 111.48/111.72 % Forward subsumed : 3949
% 111.48/111.72 % Backward subsumed : 11
% 111.48/111.72 % -------- CPU Time ---------
% 111.48/111.72 % User time : 111.067 s
% 111.48/111.72 % System time : 0.256 s
% 111.48/111.72 % Total time : 111.323 s
%------------------------------------------------------------------------------