%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET347+4 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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:31 EDT 2024
% Result : Theorem 1.70s 1.89s
% Output : Refutation 1.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SET347+4 : TPTP v8.1.2. Released v2.2.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n018.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 19:27:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 1.70/1.89 % Version: 1.5
% 1.70/1.89 % SZS status Theorem
% 1.70/1.89 % SZS output start CNFRefutation
% 1.70/1.89 fof(thI38,conjecture,equal_set(sum(empty_set),empty_set),file('/export/starexec/sandbox/benchmark/theBenchmark.p', thI38)).
% 1.70/1.89 fof(c11,negated_conjecture,(~equal_set(sum(empty_set),empty_set)),inference(assume_negation,[status(cth)],[thI38])).
% 1.70/1.89 fof(c12,negated_conjecture,~equal_set(sum(empty_set),empty_set),inference(fof_simplification,[status(thm)],[c11])).
% 1.70/1.89 cnf(c13,negated_conjecture,~equal_set(sum(empty_set),empty_set),inference(split_conjunct,[status(thm)],[c12])).
% 1.70/1.89 fof(empty_set,axiom,(![X]:(~member(X,empty_set))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', empty_set)).
% 1.70/1.89 fof(c55,plain,(![X]:~member(X,empty_set)),inference(fof_simplification,[status(thm)],[empty_set])).
% 1.70/1.89 fof(c56,plain,(![X30]:~member(X30,empty_set)),inference(variable_rename,[status(thm)],[c55])).
% 1.70/1.89 cnf(c57,plain,~member(X58,empty_set),inference(split_conjunct,[status(thm)],[c56])).
% 1.70/1.89 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)).
% 1.70/1.89 fof(c88,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])).
% 1.70/1.89 fof(c89,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)],[c88])).
% 1.70/1.89 fof(c90,plain,((![X51]:(![X52]:(~subset(X51,X52)|(![X53]:(~member(X53,X51)|member(X53,X52))))))&(![X54]:(![X55]:((?[X56]:(member(X56,X54)&~member(X56,X55)))|subset(X54,X55))))),inference(variable_rename,[status(thm)],[c89])).
% 1.70/1.89 fof(c92,plain,(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:((~subset(X51,X52)|(~member(X53,X51)|member(X53,X52)))&((member(skolem0003(X54,X55),X54)&~member(skolem0003(X54,X55),X55))|subset(X54,X55)))))))),inference(shift_quantors,[status(thm)],[fof(c91,plain,((![X51]:(![X52]:(~subset(X51,X52)|(![X53]:(~member(X53,X51)|member(X53,X52))))))&(![X54]:(![X55]:((member(skolem0003(X54,X55),X54)&~member(skolem0003(X54,X55),X55))|subset(X54,X55))))),inference(skolemize,[status(esa)],[c90])).])).
% 1.70/1.89 fof(c93,plain,(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:((~subset(X51,X52)|(~member(X53,X51)|member(X53,X52)))&((member(skolem0003(X54,X55),X54)|subset(X54,X55))&(~member(skolem0003(X54,X55),X55)|subset(X54,X55))))))))),inference(distribute,[status(thm)],[c92])).
% 1.70/1.89 cnf(c95,plain,member(skolem0003(X145,X144),X145)|subset(X145,X144),inference(split_conjunct,[status(thm)],[c93])).
% 1.70/1.89 cnf(c135,plain,subset(empty_set,X146),inference(resolution,[status(thm)],[c95, c57])).
% 1.70/1.89 fof(equal_set,axiom,(![A]:(![B]:(equal_set(A,B)<=>(subset(A,B)&subset(B,A))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', equal_set)).
% 1.70/1.89 fof(c80,plain,(![A]:(![B]:((~equal_set(A,B)|(subset(A,B)&subset(B,A)))&((~subset(A,B)|~subset(B,A))|equal_set(A,B))))),inference(fof_nnf,[status(thm)],[equal_set])).
% 1.70/1.89 fof(c81,plain,((![A]:(![B]:(~equal_set(A,B)|(subset(A,B)&subset(B,A)))))&(![A]:(![B]:((~subset(A,B)|~subset(B,A))|equal_set(A,B))))),inference(shift_quantors,[status(thm)],[c80])).
% 1.70/1.89 fof(c83,plain,(![X47]:(![X48]:(![X49]:(![X50]:((~equal_set(X47,X48)|(subset(X47,X48)&subset(X48,X47)))&((~subset(X49,X50)|~subset(X50,X49))|equal_set(X49,X50))))))),inference(shift_quantors,[status(thm)],[fof(c82,plain,((![X47]:(![X48]:(~equal_set(X47,X48)|(subset(X47,X48)&subset(X48,X47)))))&(![X49]:(![X50]:((~subset(X49,X50)|~subset(X50,X49))|equal_set(X49,X50))))),inference(variable_rename,[status(thm)],[c81])).])).
% 1.70/1.89 fof(c84,plain,(![X47]:(![X48]:(![X49]:(![X50]:(((~equal_set(X47,X48)|subset(X47,X48))&(~equal_set(X47,X48)|subset(X48,X47)))&((~subset(X49,X50)|~subset(X50,X49))|equal_set(X49,X50))))))),inference(distribute,[status(thm)],[c83])).
% 1.70/1.89 cnf(c87,plain,~subset(X172,X173)|~subset(X173,X172)|equal_set(X172,X173),inference(split_conjunct,[status(thm)],[c84])).
% 1.70/1.89 cnf(c163,plain,~subset(X183,empty_set)|equal_set(X183,empty_set),inference(resolution,[status(thm)],[c87, c135])).
% 1.70/1.89 fof(sum,axiom,(![X]:(![A]:(member(X,sum(A))<=>(?[Y]:(member(Y,A)&member(X,Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', sum)).
% 1.70/1.89 fof(c23,plain,(![X]:(![A]:((~member(X,sum(A))|(?[Y]:(member(Y,A)&member(X,Y))))&((![Y]:(~member(Y,A)|~member(X,Y)))|member(X,sum(A)))))),inference(fof_nnf,[status(thm)],[sum])).
% 1.70/1.89 fof(c24,plain,((![X]:(![A]:(~member(X,sum(A))|(?[Y]:(member(Y,A)&member(X,Y))))))&(![X]:(![A]:((![Y]:(~member(Y,A)|~member(X,Y)))|member(X,sum(A)))))),inference(shift_quantors,[status(thm)],[c23])).
% 1.70/1.89 fof(c25,plain,((![X8]:(![X9]:(~member(X8,sum(X9))|(?[X10]:(member(X10,X9)&member(X8,X10))))))&(![X11]:(![X12]:((![X13]:(~member(X13,X12)|~member(X11,X13)))|member(X11,sum(X12)))))),inference(variable_rename,[status(thm)],[c24])).
% 1.70/1.89 fof(c27,plain,(![X8]:(![X9]:(![X11]:(![X12]:(![X13]:((~member(X8,sum(X9))|(member(skolem0002(X8,X9),X9)&member(X8,skolem0002(X8,X9))))&((~member(X13,X12)|~member(X11,X13))|member(X11,sum(X12))))))))),inference(shift_quantors,[status(thm)],[fof(c26,plain,((![X8]:(![X9]:(~member(X8,sum(X9))|(member(skolem0002(X8,X9),X9)&member(X8,skolem0002(X8,X9))))))&(![X11]:(![X12]:((![X13]:(~member(X13,X12)|~member(X11,X13)))|member(X11,sum(X12)))))),inference(skolemize,[status(esa)],[c25])).])).
% 1.70/1.89 fof(c28,plain,(![X8]:(![X9]:(![X11]:(![X12]:(![X13]:(((~member(X8,sum(X9))|member(skolem0002(X8,X9),X9))&(~member(X8,sum(X9))|member(X8,skolem0002(X8,X9))))&((~member(X13,X12)|~member(X11,X13))|member(X11,sum(X12))))))))),inference(distribute,[status(thm)],[c27])).
% 1.70/1.89 cnf(c29,plain,~member(X235,sum(X236))|member(skolem0002(X235,X236),X236),inference(split_conjunct,[status(thm)],[c28])).
% 1.70/1.89 cnf(c263,plain,member(skolem0002(skolem0003(sum(X1358),X1357),X1358),X1358)|subset(sum(X1358),X1357),inference(resolution,[status(thm)],[c29, c95])).
% 1.70/1.89 cnf(c3561,plain,subset(sum(empty_set),X1359),inference(resolution,[status(thm)],[c263, c57])).
% 1.70/1.89 cnf(c3582,plain,equal_set(sum(empty_set),empty_set),inference(resolution,[status(thm)],[c3561, c163])).
% 1.70/1.89 cnf(c3587,plain,$false,inference(resolution,[status(thm)],[c3582, c13])).
% 1.70/1.89 % SZS output end CNFRefutation
% 1.70/1.89
% 1.70/1.89 % Initial clauses : 44
% 1.70/1.89 % Processed clauses : 299
% 1.70/1.89 % Factors computed : 16
% 1.70/1.89 % Resolvents computed: 3475
% 1.70/1.89 % Tautologies deleted: 2
% 1.70/1.89 % Forward subsumed : 397
% 1.70/1.89 % Backward subsumed : 2
% 1.70/1.89 % -------- CPU Time ---------
% 1.70/1.89 % User time : 1.504 s
% 1.70/1.89 % System time : 0.020 s
% 1.70/1.89 % Total time : 1.524 s
%------------------------------------------------------------------------------