%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET616+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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:51 EDT 2024
% Result : Theorem 11.10s 11.29s
% Output : Refutation 11.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SET616+3 : TPTP v8.1.2. Released v2.2.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.35 % Computer : n028.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 19:29:23 EDT 2024
% 0.15/0.36 % CPUTime :
% 11.10/11.29 % Version: 1.5
% 11.10/11.29 % SZS status Theorem
% 11.10/11.29 % SZS output start CNFRefutation
% 11.10/11.29 fof(prove_th90,conjecture,(![B]:(![C]:(difference(B,C)=difference(C,B)=>B=C))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_th90)).
% 11.10/11.29 fof(c3,negated_conjecture,(~(![B]:(![C]:(difference(B,C)=difference(C,B)=>B=C)))),inference(assume_negation,[status(cth)],[prove_th90])).
% 11.10/11.29 fof(c4,negated_conjecture,(?[B]:(?[C]:(difference(B,C)=difference(C,B)&B!=C))),inference(fof_nnf,[status(thm)],[c3])).
% 11.10/11.29 fof(c5,negated_conjecture,(?[X2]:(?[X3]:(difference(X2,X3)=difference(X3,X2)&X2!=X3))),inference(variable_rename,[status(thm)],[c4])).
% 11.10/11.29 fof(c6,negated_conjecture,(difference(skolem0001,skolem0002)=difference(skolem0002,skolem0001)&skolem0001!=skolem0002),inference(skolemize,[status(esa)],[c5])).
% 11.10/11.29 cnf(c8,negated_conjecture,skolem0001!=skolem0002,inference(split_conjunct,[status(thm)],[c6])).
% 11.10/11.29 cnf(symmetry,axiom,X34!=X33|X33=X34,theory(equality)).
% 11.10/11.29 fof(equal_defn,axiom,(![B]:(![C]:(B=C<=>(subset(B,C)&subset(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', equal_defn)).
% 11.10/11.29 fof(c30,plain,(![B]:(![C]:((B!=C|(subset(B,C)&subset(C,B)))&((~subset(B,C)|~subset(C,B))|B=C)))),inference(fof_nnf,[status(thm)],[equal_defn])).
% 11.10/11.29 fof(c31,plain,((![B]:(![C]:(B!=C|(subset(B,C)&subset(C,B)))))&(![B]:(![C]:((~subset(B,C)|~subset(C,B))|B=C)))),inference(shift_quantors,[status(thm)],[c30])).
% 11.10/11.29 fof(c33,plain,(![X18]:(![X19]:(![X20]:(![X21]:((X18!=X19|(subset(X18,X19)&subset(X19,X18)))&((~subset(X20,X21)|~subset(X21,X20))|X20=X21)))))),inference(shift_quantors,[status(thm)],[fof(c32,plain,((![X18]:(![X19]:(X18!=X19|(subset(X18,X19)&subset(X19,X18)))))&(![X20]:(![X21]:((~subset(X20,X21)|~subset(X21,X20))|X20=X21)))),inference(variable_rename,[status(thm)],[c31])).])).
% 11.10/11.29 fof(c34,plain,(![X18]:(![X19]:(![X20]:(![X21]:(((X18!=X19|subset(X18,X19))&(X18!=X19|subset(X19,X18)))&((~subset(X20,X21)|~subset(X21,X20))|X20=X21)))))),inference(distribute,[status(thm)],[c33])).
% 11.10/11.29 cnf(c37,plain,~subset(X76,X77)|~subset(X77,X76)|X76=X77,inference(split_conjunct,[status(thm)],[c34])).
% 11.10/11.29 fof(subset_defn,axiom,(![B]:(![C]:(subset(B,C)<=>(![D]:(member(D,B)=>member(D,C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', subset_defn)).
% 11.10/11.29 fof(c11,plain,(![B]:(![C]:((~subset(B,C)|(![D]:(~member(D,B)|member(D,C))))&((?[D]:(member(D,B)&~member(D,C)))|subset(B,C))))),inference(fof_nnf,[status(thm)],[subset_defn])).
% 11.10/11.29 fof(c12,plain,((![B]:(![C]:(~subset(B,C)|(![D]:(~member(D,B)|member(D,C))))))&(![B]:(![C]:((?[D]:(member(D,B)&~member(D,C)))|subset(B,C))))),inference(shift_quantors,[status(thm)],[c11])).
% 11.10/11.29 fof(c13,plain,((![X5]:(![X6]:(~subset(X5,X6)|(![X7]:(~member(X7,X5)|member(X7,X6))))))&(![X8]:(![X9]:((?[X10]:(member(X10,X8)&~member(X10,X9)))|subset(X8,X9))))),inference(variable_rename,[status(thm)],[c12])).
% 11.10/11.29 fof(c15,plain,(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:((~subset(X5,X6)|(~member(X7,X5)|member(X7,X6)))&((member(skolem0003(X8,X9),X8)&~member(skolem0003(X8,X9),X9))|subset(X8,X9)))))))),inference(shift_quantors,[status(thm)],[fof(c14,plain,((![X5]:(![X6]:(~subset(X5,X6)|(![X7]:(~member(X7,X5)|member(X7,X6))))))&(![X8]:(![X9]:((member(skolem0003(X8,X9),X8)&~member(skolem0003(X8,X9),X9))|subset(X8,X9))))),inference(skolemize,[status(esa)],[c13])).])).
% 11.10/11.29 fof(c16,plain,(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:((~subset(X5,X6)|(~member(X7,X5)|member(X7,X6)))&((member(skolem0003(X8,X9),X8)|subset(X8,X9))&(~member(skolem0003(X8,X9),X9)|subset(X8,X9))))))))),inference(distribute,[status(thm)],[c15])).
% 11.10/11.29 cnf(c19,plain,~member(skolem0003(X55,X54),X54)|subset(X55,X54),inference(split_conjunct,[status(thm)],[c16])).
% 11.10/11.29 cnf(c18,plain,member(skolem0003(X53,X52),X53)|subset(X53,X52),inference(split_conjunct,[status(thm)],[c16])).
% 11.10/11.29 fof(difference_defn,axiom,(![B]:(![C]:(![D]:(member(D,difference(B,C))<=>(member(D,B)&(~member(D,C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', difference_defn)).
% 11.10/11.29 fof(c38,plain,(![B]:(![C]:(![D]:(member(D,difference(B,C))<=>(member(D,B)&~member(D,C)))))),inference(fof_simplification,[status(thm)],[difference_defn])).
% 11.10/11.29 fof(c39,plain,(![B]:(![C]:(![D]:((~member(D,difference(B,C))|(member(D,B)&~member(D,C)))&((~member(D,B)|member(D,C))|member(D,difference(B,C))))))),inference(fof_nnf,[status(thm)],[c38])).
% 11.10/11.29 fof(c40,plain,((![B]:(![C]:(![D]:(~member(D,difference(B,C))|(member(D,B)&~member(D,C))))))&(![B]:(![C]:(![D]:((~member(D,B)|member(D,C))|member(D,difference(B,C))))))),inference(shift_quantors,[status(thm)],[c39])).
% 11.10/11.29 fof(c42,plain,(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:((~member(X24,difference(X22,X23))|(member(X24,X22)&~member(X24,X23)))&((~member(X27,X25)|member(X27,X26))|member(X27,difference(X25,X26)))))))))),inference(shift_quantors,[status(thm)],[fof(c41,plain,((![X22]:(![X23]:(![X24]:(~member(X24,difference(X22,X23))|(member(X24,X22)&~member(X24,X23))))))&(![X25]:(![X26]:(![X27]:((~member(X27,X25)|member(X27,X26))|member(X27,difference(X25,X26))))))),inference(variable_rename,[status(thm)],[c40])).])).
% 11.10/11.29 fof(c43,plain,(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(((~member(X24,difference(X22,X23))|member(X24,X22))&(~member(X24,difference(X22,X23))|~member(X24,X23)))&((~member(X27,X25)|member(X27,X26))|member(X27,difference(X25,X26)))))))))),inference(distribute,[status(thm)],[c42])).
% 11.10/11.29 cnf(c45,plain,~member(X64,difference(X65,X66))|~member(X64,X66),inference(split_conjunct,[status(thm)],[c43])).
% 11.10/11.29 cnf(c63,plain,~member(skolem0003(difference(X154,X153),X155),X153)|subset(difference(X154,X153),X155),inference(resolution,[status(thm)],[c45, c18])).
% 11.10/11.29 cnf(c17,plain,~subset(X68,X69)|~member(X67,X68)|member(X67,X69),inference(split_conjunct,[status(thm)],[c16])).
% 11.10/11.29 cnf(c64,plain,~subset(X108,X110)|member(skolem0003(X108,X109),X110)|subset(X108,X109),inference(resolution,[status(thm)],[c17, c18])).
% 11.10/11.29 cnf(reflexivity,axiom,X31=X31,theory(equality)).
% 11.10/11.29 cnf(c7,negated_conjecture,difference(skolem0001,skolem0002)=difference(skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 11.10/11.29 cnf(c79,plain,difference(skolem0002,skolem0001)=difference(skolem0001,skolem0002),inference(resolution,[status(thm)],[c7, symmetry])).
% 11.10/11.29 cnf(c2,axiom,X78!=X81|X79!=X80|~subset(X78,X79)|subset(X81,X80),theory(equality)).
% 11.10/11.29 cnf(c44,plain,~member(X57,difference(X58,X59))|member(X57,X58),inference(split_conjunct,[status(thm)],[c43])).
% 11.10/11.29 cnf(c61,plain,member(skolem0003(difference(X132,X133),X134),X132)|subset(difference(X132,X133),X134),inference(resolution,[status(thm)],[c44, c18])).
% 11.10/11.29 cnf(c171,plain,subset(difference(X136,X135),X136),inference(resolution,[status(thm)],[c61, c19])).
% 11.10/11.29 cnf(c182,plain,difference(X144,X143)!=X145|X144!=X146|subset(X145,X146),inference(resolution,[status(thm)],[c171, c2])).
% 11.10/11.29 cnf(c190,plain,skolem0002!=X152|subset(difference(skolem0001,skolem0002),X152),inference(resolution,[status(thm)],[c182, c79])).
% 11.10/11.29 cnf(c202,plain,subset(difference(skolem0001,skolem0002),skolem0002),inference(resolution,[status(thm)],[c190, reflexivity])).
% 11.10/11.29 cnf(c211,plain,member(skolem0003(difference(skolem0001,skolem0002),X1712),skolem0002)|subset(difference(skolem0001,skolem0002),X1712),inference(resolution,[status(thm)],[c202, c64])).
% 11.10/11.29 cnf(c5948,plain,subset(difference(skolem0001,skolem0002),X1713),inference(resolution,[status(thm)],[c211, c63])).
% 11.10/11.29 cnf(c46,plain,~member(X107,X105)|member(X107,X106)|member(X107,difference(X105,X106)),inference(split_conjunct,[status(thm)],[c43])).
% 11.10/11.29 cnf(c122,plain,member(skolem0003(X782,X783),X784)|member(skolem0003(X782,X783),difference(X782,X784))|subset(X782,X783),inference(resolution,[status(thm)],[c46, c18])).
% 11.10/11.29 cnf(c1523,plain,member(skolem0003(X785,X786),difference(X785,X786))|subset(X785,X786),inference(resolution,[status(thm)],[c122, c19])).
% 11.10/11.29 cnf(c1552,plain,subset(X5257,X5256)|~subset(difference(X5257,X5256),X5255)|member(skolem0003(X5257,X5256),X5255),inference(resolution,[status(thm)],[c1523, c17])).
% 11.10/11.29 cnf(c22854,plain,subset(skolem0001,skolem0002)|member(skolem0003(skolem0001,skolem0002),X5264),inference(resolution,[status(thm)],[c1552, c5948])).
% 11.10/11.29 cnf(c22923,plain,subset(skolem0001,skolem0002),inference(resolution,[status(thm)],[c22854, c19])).
% 11.10/11.29 cnf(c23045,plain,~subset(skolem0002,skolem0001)|skolem0002=skolem0001,inference(resolution,[status(thm)],[c22923, c37])).
% 11.10/11.29 cnf(c203,plain,subset(difference(X156,X156),X157),inference(resolution,[status(thm)],[c63, c61])).
% 11.10/11.29 cnf(c204,plain,difference(X282,X282)!=X279|X280!=X281|subset(X279,X281),inference(resolution,[status(thm)],[c203, c2])).
% 11.10/11.29 cnf(transitivity,axiom,X38!=X36|X36!=X37|X38=X37,theory(equality)).
% 11.10/11.29 cnf(c74,plain,X177!=difference(skolem0001,skolem0002)|X177=difference(skolem0002,skolem0001),inference(resolution,[status(thm)],[c7, transitivity])).
% 11.10/11.29 cnf(c205,plain,~subset(X178,difference(X179,X179))|X178=difference(X179,X179),inference(resolution,[status(thm)],[c203, c37])).
% 11.10/11.29 cnf(c5972,plain,difference(skolem0001,skolem0002)=difference(X1714,X1714),inference(resolution,[status(thm)],[c5948, c205])).
% 11.10/11.29 cnf(c5991,plain,difference(X1719,X1719)=difference(skolem0001,skolem0002),inference(resolution,[status(thm)],[c5972, symmetry])).
% 11.10/11.29 cnf(c6068,plain,difference(X1728,X1728)=difference(skolem0002,skolem0001),inference(resolution,[status(thm)],[c5991, c74])).
% 11.10/11.29 cnf(c6119,plain,X1765!=X1766|subset(difference(skolem0002,skolem0001),X1766),inference(resolution,[status(thm)],[c6068, c204])).
% 11.10/11.29 cnf(c6350,plain,subset(difference(skolem0002,skolem0001),X1767),inference(resolution,[status(thm)],[c6119, reflexivity])).
% 11.10/11.29 cnf(c22871,plain,subset(skolem0002,skolem0001)|member(skolem0003(skolem0002,skolem0001),X5275),inference(resolution,[status(thm)],[c1552, c6350])).
% 11.10/11.29 cnf(c23292,plain,subset(skolem0002,skolem0001),inference(resolution,[status(thm)],[c22871, c19])).
% 11.10/11.29 cnf(c23308,plain,skolem0002=skolem0001,inference(resolution,[status(thm)],[c23292, c23045])).
% 11.10/11.29 cnf(c23346,plain,skolem0001=skolem0002,inference(resolution,[status(thm)],[c23308, symmetry])).
% 11.10/11.29 cnf(c23438,plain,$false,inference(resolution,[status(thm)],[c23346, c8])).
% 11.10/11.29 % SZS output end CNFRefutation
% 11.10/11.29
% 11.10/11.29 % Initial clauses : 24
% 11.10/11.29 % Processed clauses : 491
% 11.10/11.29 % Factors computed : 93
% 11.10/11.29 % Resolvents computed: 23330
% 11.10/11.29 % Tautologies deleted: 8
% 11.10/11.29 % Forward subsumed : 1718
% 11.10/11.29 % Backward subsumed : 131
% 11.10/11.29 % -------- CPU Time ---------
% 11.10/11.29 % User time : 10.859 s
% 11.10/11.29 % System time : 0.072 s
% 11.10/11.29 % Total time : 10.931 s
%------------------------------------------------------------------------------