%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET696+4 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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 75.18s 75.34s
% Output : Refutation 75.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET696+4 : TPTP v8.1.2. Released v2.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n009.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 18:22:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 75.18/75.34 % Version: 1.5
% 75.18/75.34 % SZS status Theorem
% 75.18/75.34 % SZS output start CNFRefutation
% 75.18/75.34 fof(thI28,conjecture,(![A]:(![E]:(subset(A,E)=>equal_set(intersection(difference(E,A),A),empty_set)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', thI28)).
% 75.18/75.34 fof(c11,negated_conjecture,(~(![A]:(![E]:(subset(A,E)=>equal_set(intersection(difference(E,A),A),empty_set))))),inference(assume_negation,[status(cth)],[thI28])).
% 75.18/75.34 fof(c12,negated_conjecture,(?[A]:(?[E]:(subset(A,E)&~equal_set(intersection(difference(E,A),A),empty_set)))),inference(fof_nnf,[status(thm)],[c11])).
% 75.18/75.34 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(subset(X2,X3)&~equal_set(intersection(difference(X3,X2),X2),empty_set)))),inference(variable_rename,[status(thm)],[c12])).
% 75.18/75.34 fof(c14,negated_conjecture,(subset(skolem0001,skolem0002)&~equal_set(intersection(difference(skolem0002,skolem0001),skolem0001),empty_set)),inference(skolemize,[status(esa)],[c13])).
% 75.18/75.34 cnf(c16,negated_conjecture,~equal_set(intersection(difference(skolem0002,skolem0001),skolem0001),empty_set),inference(split_conjunct,[status(thm)],[c14])).
% 75.18/75.34 fof(empty_set,axiom,(![X]:(~member(X,empty_set))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', empty_set)).
% 75.18/75.34 fof(c58,plain,(![X]:~member(X,empty_set)),inference(fof_simplification,[status(thm)],[empty_set])).
% 75.18/75.34 fof(c59,plain,(![X32]:~member(X32,empty_set)),inference(variable_rename,[status(thm)],[c58])).
% 75.18/75.34 cnf(c60,plain,~member(X60,empty_set),inference(split_conjunct,[status(thm)],[c59])).
% 75.18/75.34 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)).
% 75.18/75.34 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])).
% 75.18/75.34 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])).
% 75.18/75.34 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])).
% 75.18/75.34 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])).])).
% 75.18/75.34 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])).
% 75.18/75.34 cnf(c98,plain,member(skolem0005(X151,X150),X151)|subset(X151,X150),inference(split_conjunct,[status(thm)],[c96])).
% 75.18/75.34 cnf(c142,plain,subset(empty_set,X152),inference(resolution,[status(thm)],[c98, c60])).
% 75.18/75.34 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)).
% 75.18/75.34 fof(c83,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])).
% 75.18/75.34 fof(c84,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)],[c83])).
% 75.18/75.34 fof(c86,plain,(![X49]:(![X50]:(![X51]:(![X52]:((~equal_set(X49,X50)|(subset(X49,X50)&subset(X50,X49)))&((~subset(X51,X52)|~subset(X52,X51))|equal_set(X51,X52))))))),inference(shift_quantors,[status(thm)],[fof(c85,plain,((![X49]:(![X50]:(~equal_set(X49,X50)|(subset(X49,X50)&subset(X50,X49)))))&(![X51]:(![X52]:((~subset(X51,X52)|~subset(X52,X51))|equal_set(X51,X52))))),inference(variable_rename,[status(thm)],[c84])).])).
% 75.18/75.34 fof(c87,plain,(![X49]:(![X50]:(![X51]:(![X52]:(((~equal_set(X49,X50)|subset(X49,X50))&(~equal_set(X49,X50)|subset(X50,X49)))&((~subset(X51,X52)|~subset(X52,X51))|equal_set(X51,X52))))))),inference(distribute,[status(thm)],[c86])).
% 75.18/75.34 cnf(c90,plain,~subset(X180,X181)|~subset(X181,X180)|equal_set(X180,X181),inference(split_conjunct,[status(thm)],[c87])).
% 75.18/75.34 cnf(c180,plain,~subset(X191,empty_set)|equal_set(X191,empty_set),inference(resolution,[status(thm)],[c90, c142])).
% 75.18/75.34 fof(intersection,axiom,(![X]:(![A]:(![B]:(member(X,intersection(A,B))<=>(member(X,A)&member(X,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', intersection)).
% 75.18/75.34 fof(c69,plain,(![X]:(![A]:(![B]:((~member(X,intersection(A,B))|(member(X,A)&member(X,B)))&((~member(X,A)|~member(X,B))|member(X,intersection(A,B))))))),inference(fof_nnf,[status(thm)],[intersection])).
% 75.18/75.34 fof(c70,plain,((![X]:(![A]:(![B]:(~member(X,intersection(A,B))|(member(X,A)&member(X,B))))))&(![X]:(![A]:(![B]:((~member(X,A)|~member(X,B))|member(X,intersection(A,B))))))),inference(shift_quantors,[status(thm)],[c69])).
% 75.18/75.34 fof(c72,plain,(![X39]:(![X40]:(![X41]:(![X42]:(![X43]:(![X44]:((~member(X39,intersection(X40,X41))|(member(X39,X40)&member(X39,X41)))&((~member(X42,X43)|~member(X42,X44))|member(X42,intersection(X43,X44)))))))))),inference(shift_quantors,[status(thm)],[fof(c71,plain,((![X39]:(![X40]:(![X41]:(~member(X39,intersection(X40,X41))|(member(X39,X40)&member(X39,X41))))))&(![X42]:(![X43]:(![X44]:((~member(X42,X43)|~member(X42,X44))|member(X42,intersection(X43,X44))))))),inference(variable_rename,[status(thm)],[c70])).])).
% 75.18/75.34 fof(c73,plain,(![X39]:(![X40]:(![X41]:(![X42]:(![X43]:(![X44]:(((~member(X39,intersection(X40,X41))|member(X39,X40))&(~member(X39,intersection(X40,X41))|member(X39,X41)))&((~member(X42,X43)|~member(X42,X44))|member(X42,intersection(X43,X44)))))))))),inference(distribute,[status(thm)],[c72])).
% 75.18/75.34 cnf(c75,plain,~member(X145,intersection(X143,X144))|member(X145,X144),inference(split_conjunct,[status(thm)],[c73])).
% 75.18/75.34 cnf(c141,plain,subset(intersection(X514,X515),X516)|member(skolem0005(intersection(X514,X515),X516),X515),inference(resolution,[status(thm)],[c98, c75])).
% 75.18/75.34 fof(difference,axiom,(![B]:(![A]:(![E]:(member(B,difference(E,A))<=>(member(B,E)&(~member(B,A))))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax', difference)).
% 75.18/75.34 fof(c49,plain,(![B]:(![A]:(![E]:(member(B,difference(E,A))<=>(member(B,E)&~member(B,A)))))),inference(fof_simplification,[status(thm)],[difference])).
% 75.18/75.34 fof(c50,plain,(![B]:(![A]:(![E]:((~member(B,difference(E,A))|(member(B,E)&~member(B,A)))&((~member(B,E)|member(B,A))|member(B,difference(E,A))))))),inference(fof_nnf,[status(thm)],[c49])).
% 75.18/75.34 fof(c51,plain,((![B]:(![A]:(![E]:(~member(B,difference(E,A))|(member(B,E)&~member(B,A))))))&(![B]:(![A]:(![E]:((~member(B,E)|member(B,A))|member(B,difference(E,A))))))),inference(shift_quantors,[status(thm)],[c50])).
% 75.18/75.34 fof(c53,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:((~member(X26,difference(X28,X27))|(member(X26,X28)&~member(X26,X27)))&((~member(X29,X31)|member(X29,X30))|member(X29,difference(X31,X30)))))))))),inference(shift_quantors,[status(thm)],[fof(c52,plain,((![X26]:(![X27]:(![X28]:(~member(X26,difference(X28,X27))|(member(X26,X28)&~member(X26,X27))))))&(![X29]:(![X30]:(![X31]:((~member(X29,X31)|member(X29,X30))|member(X29,difference(X31,X30))))))),inference(variable_rename,[status(thm)],[c51])).])).
% 75.18/75.34 fof(c54,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(((~member(X26,difference(X28,X27))|member(X26,X28))&(~member(X26,difference(X28,X27))|~member(X26,X27)))&((~member(X29,X31)|member(X29,X30))|member(X29,difference(X31,X30)))))))))),inference(distribute,[status(thm)],[c53])).
% 75.18/75.34 cnf(c56,plain,~member(X110,difference(X108,X109))|~member(X110,X109),inference(split_conjunct,[status(thm)],[c54])).
% 75.18/75.34 cnf(c74,plain,~member(X142,intersection(X140,X141))|member(X142,X140),inference(split_conjunct,[status(thm)],[c73])).
% 75.18/75.34 cnf(c146,plain,subset(intersection(X553,X554),X555)|member(skolem0005(intersection(X553,X554),X555),X553),inference(resolution,[status(thm)],[c98, c74])).
% 75.18/75.34 cnf(c1102,plain,subset(intersection(difference(X8835,X8832),X8833),X8834)|~member(skolem0005(intersection(difference(X8835,X8832),X8833),X8834),X8832),inference(resolution,[status(thm)],[c146, c56])).
% 75.18/75.34 cnf(c91701,plain,subset(intersection(difference(X8840,X8841),X8841),X8839),inference(resolution,[status(thm)],[c1102, c141])).
% 75.18/75.34 cnf(c91904,plain,equal_set(intersection(difference(X8845,X8844),X8844),empty_set),inference(resolution,[status(thm)],[c91701, c180])).
% 75.18/75.34 cnf(c91925,plain,$false,inference(resolution,[status(thm)],[c91904, c16])).
% 75.18/75.34 % SZS output end CNFRefutation
% 75.18/75.34
% 75.18/75.34 % Initial clauses : 45
% 75.18/75.34 % Processed clauses : 1149
% 75.18/75.34 % Factors computed : 53
% 75.18/75.34 % Resolvents computed: 91773
% 75.18/75.34 % Tautologies deleted: 59
% 75.18/75.34 % Forward subsumed : 3404
% 75.18/75.34 % Backward subsumed : 11
% 75.18/75.34 % -------- CPU Time ---------
% 75.18/75.34 % User time : 74.790 s
% 75.18/75.34 % System time : 0.201 s
% 75.18/75.34 % Total time : 74.991 s
%------------------------------------------------------------------------------