%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU153+1 : TPTP v8.1.2. Released v3.3.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:40:41 EDT 2024
% Result : Theorem 2.21s 2.41s
% Output : Refutation 2.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SEU153+1 : TPTP v8.1.2. Released v3.3.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n029.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 10:59:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 2.21/2.41 % Version: 1.5
% 2.21/2.41 % SZS status Theorem
% 2.21/2.41 % SZS output start CNFRefutation
% 2.21/2.41 fof(antisymmetry_r2_hidden,axiom,(![A]:(![B]:(in(A,B)=>(~in(B,A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', antisymmetry_r2_hidden)).
% 2.21/2.41 fof(c66,plain,(![A]:(![B]:(in(A,B)=>~in(B,A)))),inference(fof_simplification,[status(thm)],[antisymmetry_r2_hidden])).
% 2.21/2.41 fof(c67,plain,(![A]:(![B]:(~in(A,B)|~in(B,A)))),inference(fof_nnf,[status(thm)],[c66])).
% 2.21/2.41 fof(c68,plain,(![X35]:(![X36]:(~in(X35,X36)|~in(X36,X35)))),inference(variable_rename,[status(thm)],[c67])).
% 2.21/2.41 cnf(c69,plain,~in(X50,X49)|~in(X49,X50),inference(split_conjunct,[status(thm)],[c68])).
% 2.21/2.41 cnf(c78,plain,~in(X55,X55),inference(factor,[status(thm)],[c69])).
% 2.21/2.41 fof(d3_xboole_0,axiom,(![A]:(![B]:(![C]:(C=set_intersection2(A,B)<=>(![D]:(in(D,C)<=>(in(D,A)&in(D,B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d3_xboole_0)).
% 2.21/2.41 fof(c34,plain,(![A]:(![B]:(![C]:((C!=set_intersection2(A,B)|(![D]:((~in(D,C)|(in(D,A)&in(D,B)))&((~in(D,A)|~in(D,B))|in(D,C)))))&((?[D]:((~in(D,C)|(~in(D,A)|~in(D,B)))&(in(D,C)|(in(D,A)&in(D,B)))))|C=set_intersection2(A,B)))))),inference(fof_nnf,[status(thm)],[d3_xboole_0])).
% 2.21/2.41 fof(c35,plain,((![A]:(![B]:(![C]:(C!=set_intersection2(A,B)|((![D]:(~in(D,C)|(in(D,A)&in(D,B))))&(![D]:((~in(D,A)|~in(D,B))|in(D,C))))))))&(![A]:(![B]:(![C]:((?[D]:((~in(D,C)|(~in(D,A)|~in(D,B)))&(in(D,C)|(in(D,A)&in(D,B)))))|C=set_intersection2(A,B)))))),inference(shift_quantors,[status(thm)],[c34])).
% 2.21/2.41 fof(c36,plain,((![X13]:(![X14]:(![X15]:(X15!=set_intersection2(X13,X14)|((![X16]:(~in(X16,X15)|(in(X16,X13)&in(X16,X14))))&(![X17]:((~in(X17,X13)|~in(X17,X14))|in(X17,X15))))))))&(![X18]:(![X19]:(![X20]:((?[X21]:((~in(X21,X20)|(~in(X21,X18)|~in(X21,X19)))&(in(X21,X20)|(in(X21,X18)&in(X21,X19)))))|X20=set_intersection2(X18,X19)))))),inference(variable_rename,[status(thm)],[c35])).
% 2.21/2.41 fof(c38,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:((X15!=set_intersection2(X13,X14)|((~in(X16,X15)|(in(X16,X13)&in(X16,X14)))&((~in(X17,X13)|~in(X17,X14))|in(X17,X15))))&(((~in(skolem0005(X18,X19,X20),X20)|(~in(skolem0005(X18,X19,X20),X18)|~in(skolem0005(X18,X19,X20),X19)))&(in(skolem0005(X18,X19,X20),X20)|(in(skolem0005(X18,X19,X20),X18)&in(skolem0005(X18,X19,X20),X19))))|X20=set_intersection2(X18,X19))))))))))),inference(shift_quantors,[status(thm)],[fof(c37,plain,((![X13]:(![X14]:(![X15]:(X15!=set_intersection2(X13,X14)|((![X16]:(~in(X16,X15)|(in(X16,X13)&in(X16,X14))))&(![X17]:((~in(X17,X13)|~in(X17,X14))|in(X17,X15))))))))&(![X18]:(![X19]:(![X20]:(((~in(skolem0005(X18,X19,X20),X20)|(~in(skolem0005(X18,X19,X20),X18)|~in(skolem0005(X18,X19,X20),X19)))&(in(skolem0005(X18,X19,X20),X20)|(in(skolem0005(X18,X19,X20),X18)&in(skolem0005(X18,X19,X20),X19))))|X20=set_intersection2(X18,X19)))))),inference(skolemize,[status(esa)],[c36])).])).
% 2.21/2.41 fof(c39,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:((((X15!=set_intersection2(X13,X14)|(~in(X16,X15)|in(X16,X13)))&(X15!=set_intersection2(X13,X14)|(~in(X16,X15)|in(X16,X14))))&(X15!=set_intersection2(X13,X14)|((~in(X17,X13)|~in(X17,X14))|in(X17,X15))))&(((~in(skolem0005(X18,X19,X20),X20)|(~in(skolem0005(X18,X19,X20),X18)|~in(skolem0005(X18,X19,X20),X19)))|X20=set_intersection2(X18,X19))&(((in(skolem0005(X18,X19,X20),X20)|in(skolem0005(X18,X19,X20),X18))|X20=set_intersection2(X18,X19))&((in(skolem0005(X18,X19,X20),X20)|in(skolem0005(X18,X19,X20),X19))|X20=set_intersection2(X18,X19))))))))))))),inference(distribute,[status(thm)],[c38])).
% 2.21/2.41 cnf(c41,plain,X103!=set_intersection2(X104,X102)|~in(X105,X103)|in(X105,X102),inference(split_conjunct,[status(thm)],[c39])).
% 2.21/2.41 cnf(reflexivity,axiom,X37=X37,theory(equality)).
% 2.21/2.41 fof(d1_xboole_0,axiom,(![A]:(A=empty_set<=>(![B]:(~in(B,A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_xboole_0)).
% 2.21/2.41 fof(c46,plain,(![A]:(A=empty_set<=>(![B]:~in(B,A)))),inference(fof_simplification,[status(thm)],[d1_xboole_0])).
% 2.21/2.41 fof(c47,plain,(![A]:((A!=empty_set|(![B]:~in(B,A)))&((?[B]:in(B,A))|A=empty_set))),inference(fof_nnf,[status(thm)],[c46])).
% 2.21/2.41 fof(c48,plain,((![A]:(A!=empty_set|(![B]:~in(B,A))))&(![A]:((?[B]:in(B,A))|A=empty_set))),inference(shift_quantors,[status(thm)],[c47])).
% 2.21/2.41 fof(c49,plain,((![X22]:(X22!=empty_set|(![X23]:~in(X23,X22))))&(![X24]:((?[X25]:in(X25,X24))|X24=empty_set))),inference(variable_rename,[status(thm)],[c48])).
% 2.21/2.41 fof(c51,plain,(![X22]:(![X23]:(![X24]:((X22!=empty_set|~in(X23,X22))&(in(skolem0006(X24),X24)|X24=empty_set))))),inference(shift_quantors,[status(thm)],[fof(c50,plain,((![X22]:(X22!=empty_set|(![X23]:~in(X23,X22))))&(![X24]:(in(skolem0006(X24),X24)|X24=empty_set))),inference(skolemize,[status(esa)],[c49])).])).
% 2.21/2.41 cnf(c52,plain,X63!=empty_set|~in(X62,X63),inference(split_conjunct,[status(thm)],[c51])).
% 2.21/2.41 cnf(c44,plain,in(skolem0005(X140,X138,X139),X139)|in(skolem0005(X140,X138,X139),X140)|X139=set_intersection2(X140,X138),inference(split_conjunct,[status(thm)],[c39])).
% 2.21/2.41 cnf(c177,plain,in(skolem0005(X457,X456,X457),X457)|X457=set_intersection2(X457,X456),inference(factor,[status(thm)],[c44])).
% 2.21/2.41 cnf(c2304,plain,X458=set_intersection2(X458,X459)|X458!=empty_set,inference(resolution,[status(thm)],[c177, c52])).
% 2.21/2.41 cnf(c2347,plain,empty_set=set_intersection2(empty_set,X460),inference(resolution,[status(thm)],[c2304, reflexivity])).
% 2.21/2.41 cnf(c2376,plain,~in(X480,empty_set)|in(X480,X479),inference(resolution,[status(thm)],[c2347, c41])).
% 2.21/2.41 fof(l25_zfmisc_1,conjecture,(![A]:(![B]:(~(disjoint(singleton(A),B)&in(A,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', l25_zfmisc_1)).
% 2.21/2.41 fof(c15,negated_conjecture,(~(![A]:(![B]:(~(disjoint(singleton(A),B)&in(A,B)))))),inference(assume_negation,[status(cth)],[l25_zfmisc_1])).
% 2.21/2.41 fof(c16,negated_conjecture,(?[A]:(?[B]:(disjoint(singleton(A),B)&in(A,B)))),inference(fof_nnf,[status(thm)],[c15])).
% 2.21/2.41 fof(c17,negated_conjecture,(?[X6]:(?[X7]:(disjoint(singleton(X6),X7)&in(X6,X7)))),inference(variable_rename,[status(thm)],[c16])).
% 2.21/2.41 fof(c18,negated_conjecture,(disjoint(singleton(skolem0003),skolem0004)&in(skolem0003,skolem0004)),inference(skolemize,[status(esa)],[c17])).
% 2.21/2.41 cnf(c20,negated_conjecture,in(skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c18])).
% 2.21/2.41 fof(d1_tarski,axiom,(![A]:(![B]:(B=singleton(A)<=>(![C]:(in(C,B)<=>C=A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_tarski)).
% 2.21/2.41 fof(c54,plain,(![A]:(![B]:((B!=singleton(A)|(![C]:((~in(C,B)|C=A)&(C!=A|in(C,B)))))&((?[C]:((~in(C,B)|C!=A)&(in(C,B)|C=A)))|B=singleton(A))))),inference(fof_nnf,[status(thm)],[d1_tarski])).
% 2.21/2.41 fof(c55,plain,((![A]:(![B]:(B!=singleton(A)|((![C]:(~in(C,B)|C=A))&(![C]:(C!=A|in(C,B)))))))&(![A]:(![B]:((?[C]:((~in(C,B)|C!=A)&(in(C,B)|C=A)))|B=singleton(A))))),inference(shift_quantors,[status(thm)],[c54])).
% 2.21/2.41 fof(c56,plain,((![X26]:(![X27]:(X27!=singleton(X26)|((![X28]:(~in(X28,X27)|X28=X26))&(![X29]:(X29!=X26|in(X29,X27)))))))&(![X30]:(![X31]:((?[X32]:((~in(X32,X31)|X32!=X30)&(in(X32,X31)|X32=X30)))|X31=singleton(X30))))),inference(variable_rename,[status(thm)],[c55])).
% 2.21/2.41 fof(c58,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:((X27!=singleton(X26)|((~in(X28,X27)|X28=X26)&(X29!=X26|in(X29,X27))))&(((~in(skolem0007(X30,X31),X31)|skolem0007(X30,X31)!=X30)&(in(skolem0007(X30,X31),X31)|skolem0007(X30,X31)=X30))|X31=singleton(X30))))))))),inference(shift_quantors,[status(thm)],[fof(c57,plain,((![X26]:(![X27]:(X27!=singleton(X26)|((![X28]:(~in(X28,X27)|X28=X26))&(![X29]:(X29!=X26|in(X29,X27)))))))&(![X30]:(![X31]:(((~in(skolem0007(X30,X31),X31)|skolem0007(X30,X31)!=X30)&(in(skolem0007(X30,X31),X31)|skolem0007(X30,X31)=X30))|X31=singleton(X30))))),inference(skolemize,[status(esa)],[c56])).])).
% 2.21/2.41 fof(c59,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(((X27!=singleton(X26)|(~in(X28,X27)|X28=X26))&(X27!=singleton(X26)|(X29!=X26|in(X29,X27))))&(((~in(skolem0007(X30,X31),X31)|skolem0007(X30,X31)!=X30)|X31=singleton(X30))&((in(skolem0007(X30,X31),X31)|skolem0007(X30,X31)=X30)|X31=singleton(X30)))))))))),inference(distribute,[status(thm)],[c58])).
% 2.21/2.41 cnf(c61,plain,X155!=singleton(X156)|X157!=X156|in(X157,X155),inference(split_conjunct,[status(thm)],[c59])).
% 2.21/2.41 cnf(c284,plain,X159!=X158|in(X159,singleton(X158)),inference(resolution,[status(thm)],[c61, reflexivity])).
% 2.21/2.41 cnf(c298,plain,in(X160,singleton(X160)),inference(resolution,[status(thm)],[c284, reflexivity])).
% 2.21/2.41 cnf(c42,plain,X113!=set_intersection2(X114,X112)|~in(X115,X114)|~in(X115,X112)|in(X115,X113),inference(split_conjunct,[status(thm)],[c39])).
% 2.21/2.41 cnf(symmetry,axiom,X39!=X38|X38=X39,theory(equality)).
% 2.21/2.41 fof(symmetry_r1_xboole_0,axiom,(![A]:(![B]:(disjoint(A,B)=>disjoint(B,A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', symmetry_r1_xboole_0)).
% 2.21/2.41 fof(c5,plain,(![A]:(![B]:(~disjoint(A,B)|disjoint(B,A)))),inference(fof_nnf,[status(thm)],[symmetry_r1_xboole_0])).
% 2.21/2.41 fof(c6,plain,(![X2]:(![X3]:(~disjoint(X2,X3)|disjoint(X3,X2)))),inference(variable_rename,[status(thm)],[c5])).
% 2.21/2.41 cnf(c7,plain,~disjoint(X48,X47)|disjoint(X47,X48),inference(split_conjunct,[status(thm)],[c6])).
% 2.21/2.41 cnf(c19,negated_conjecture,disjoint(singleton(skolem0003),skolem0004),inference(split_conjunct,[status(thm)],[c18])).
% 2.21/2.41 cnf(c77,plain,disjoint(skolem0004,singleton(skolem0003)),inference(resolution,[status(thm)],[c19, c7])).
% 2.21/2.41 fof(d7_xboole_0,axiom,(![A]:(![B]:(disjoint(A,B)<=>set_intersection2(A,B)=empty_set))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d7_xboole_0)).
% 2.21/2.41 fof(c28,plain,(![A]:(![B]:((~disjoint(A,B)|set_intersection2(A,B)=empty_set)&(set_intersection2(A,B)!=empty_set|disjoint(A,B))))),inference(fof_nnf,[status(thm)],[d7_xboole_0])).
% 2.21/2.41 fof(c29,plain,((![A]:(![B]:(~disjoint(A,B)|set_intersection2(A,B)=empty_set)))&(![A]:(![B]:(set_intersection2(A,B)!=empty_set|disjoint(A,B))))),inference(shift_quantors,[status(thm)],[c28])).
% 2.21/2.41 fof(c31,plain,(![X9]:(![X10]:(![X11]:(![X12]:((~disjoint(X9,X10)|set_intersection2(X9,X10)=empty_set)&(set_intersection2(X11,X12)!=empty_set|disjoint(X11,X12))))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,((![X9]:(![X10]:(~disjoint(X9,X10)|set_intersection2(X9,X10)=empty_set)))&(![X11]:(![X12]:(set_intersection2(X11,X12)!=empty_set|disjoint(X11,X12))))),inference(variable_rename,[status(thm)],[c29])).])).
% 2.21/2.41 cnf(c32,plain,~disjoint(X82,X83)|set_intersection2(X82,X83)=empty_set,inference(split_conjunct,[status(thm)],[c31])).
% 2.21/2.41 cnf(c115,plain,set_intersection2(skolem0004,singleton(skolem0003))=empty_set,inference(resolution,[status(thm)],[c32, c77])).
% 2.21/2.41 cnf(c204,plain,empty_set=set_intersection2(skolem0004,singleton(skolem0003)),inference(resolution,[status(thm)],[c115, symmetry])).
% 2.21/2.41 cnf(c242,plain,~in(X954,skolem0004)|~in(X954,singleton(skolem0003))|in(X954,empty_set),inference(resolution,[status(thm)],[c204, c42])).
% 2.21/2.41 cnf(c6233,plain,~in(skolem0003,skolem0004)|in(skolem0003,empty_set),inference(resolution,[status(thm)],[c242, c298])).
% 2.21/2.41 cnf(c6251,plain,in(skolem0003,empty_set),inference(resolution,[status(thm)],[c6233, c20])).
% 2.21/2.41 cnf(c6259,plain,in(skolem0003,X957),inference(resolution,[status(thm)],[c6251, c2376])).
% 2.21/2.41 cnf(c6288,plain,$false,inference(resolution,[status(thm)],[c6259, c78])).
% 2.21/2.41 % SZS output end CNFRefutation
% 2.21/2.41
% 2.21/2.41 % Initial clauses : 34
% 2.21/2.41 % Processed clauses : 381
% 2.21/2.41 % Factors computed : 30
% 2.21/2.41 % Resolvents computed: 6231
% 2.21/2.41 % Tautologies deleted: 15
% 2.21/2.41 % Forward subsumed : 384
% 2.21/2.41 % Backward subsumed : 35
% 2.21/2.41 % -------- CPU Time ---------
% 2.21/2.41 % User time : 2.027 s
% 2.21/2.41 % System time : 0.020 s
% 2.21/2.41 % Total time : 2.047 s
%------------------------------------------------------------------------------