%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU119+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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:34 EDT 2024
% Result : Theorem 48.45s 48.62s
% Output : Refutation 48.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU119+2 : TPTP v8.1.2. Released v3.3.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n010.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 12:10:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 48.45/48.62 % Version: 1.5
% 48.45/48.62 % SZS status Theorem
% 48.45/48.62 % SZS output start CNFRefutation
% 48.45/48.62 fof(antisymmetry_r2_hidden,axiom,(![A]:(![B]:(in(A,B)=>(~in(B,A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', antisymmetry_r2_hidden)).
% 48.45/48.62 fof(c62,plain,(![A]:(![B]:(in(A,B)=>~in(B,A)))),inference(fof_simplification,[status(thm)],[antisymmetry_r2_hidden])).
% 48.45/48.62 fof(c63,plain,(![A]:(![B]:(~in(A,B)|~in(B,A)))),inference(fof_nnf,[status(thm)],[c62])).
% 48.45/48.62 fof(c64,plain,(![X32]:(![X33]:(~in(X32,X33)|~in(X33,X32)))),inference(variable_rename,[status(thm)],[c63])).
% 48.45/48.62 cnf(c65,plain,~in(X46,X47)|~in(X47,X46),inference(split_conjunct,[status(thm)],[c64])).
% 48.45/48.62 cnf(c73,plain,~in(X48,X48),inference(factor,[status(thm)],[c65])).
% 48.45/48.62 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/sandbox2/benchmark/theBenchmark.p', d3_xboole_0)).
% 48.45/48.62 fof(c40,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])).
% 48.45/48.62 fof(c41,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)],[c40])).
% 48.45/48.62 fof(c42,plain,((![X17]:(![X18]:(![X19]:(X19!=set_intersection2(X17,X18)|((![X20]:(~in(X20,X19)|(in(X20,X17)&in(X20,X18))))&(![X21]:((~in(X21,X17)|~in(X21,X18))|in(X21,X19))))))))&(![X22]:(![X23]:(![X24]:((?[X25]:((~in(X25,X24)|(~in(X25,X22)|~in(X25,X23)))&(in(X25,X24)|(in(X25,X22)&in(X25,X23)))))|X24=set_intersection2(X22,X23)))))),inference(variable_rename,[status(thm)],[c41])).
% 48.45/48.62 fof(c44,plain,(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:((X19!=set_intersection2(X17,X18)|((~in(X20,X19)|(in(X20,X17)&in(X20,X18)))&((~in(X21,X17)|~in(X21,X18))|in(X21,X19))))&(((~in(skolem0008(X22,X23,X24),X24)|(~in(skolem0008(X22,X23,X24),X22)|~in(skolem0008(X22,X23,X24),X23)))&(in(skolem0008(X22,X23,X24),X24)|(in(skolem0008(X22,X23,X24),X22)&in(skolem0008(X22,X23,X24),X23))))|X24=set_intersection2(X22,X23))))))))))),inference(shift_quantors,[status(thm)],[fof(c43,plain,((![X17]:(![X18]:(![X19]:(X19!=set_intersection2(X17,X18)|((![X20]:(~in(X20,X19)|(in(X20,X17)&in(X20,X18))))&(![X21]:((~in(X21,X17)|~in(X21,X18))|in(X21,X19))))))))&(![X22]:(![X23]:(![X24]:(((~in(skolem0008(X22,X23,X24),X24)|(~in(skolem0008(X22,X23,X24),X22)|~in(skolem0008(X22,X23,X24),X23)))&(in(skolem0008(X22,X23,X24),X24)|(in(skolem0008(X22,X23,X24),X22)&in(skolem0008(X22,X23,X24),X23))))|X24=set_intersection2(X22,X23)))))),inference(skolemize,[status(esa)],[c42])).])).
% 48.45/48.62 fof(c45,plain,(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:((((X19!=set_intersection2(X17,X18)|(~in(X20,X19)|in(X20,X17)))&(X19!=set_intersection2(X17,X18)|(~in(X20,X19)|in(X20,X18))))&(X19!=set_intersection2(X17,X18)|((~in(X21,X17)|~in(X21,X18))|in(X21,X19))))&(((~in(skolem0008(X22,X23,X24),X24)|(~in(skolem0008(X22,X23,X24),X22)|~in(skolem0008(X22,X23,X24),X23)))|X24=set_intersection2(X22,X23))&(((in(skolem0008(X22,X23,X24),X24)|in(skolem0008(X22,X23,X24),X22))|X24=set_intersection2(X22,X23))&((in(skolem0008(X22,X23,X24),X24)|in(skolem0008(X22,X23,X24),X23))|X24=set_intersection2(X22,X23))))))))))))),inference(distribute,[status(thm)],[c44])).
% 48.45/48.62 cnf(c46,plain,X109!=set_intersection2(X110,X107)|~in(X108,X109)|in(X108,X110),inference(split_conjunct,[status(thm)],[c45])).
% 48.45/48.62 cnf(transitivity,axiom,X43!=X41|X41!=X42|X43=X42,theory(equality)).
% 48.45/48.62 cnf(symmetry,axiom,X36!=X35|X35=X36,theory(equality)).
% 48.45/48.62 fof(d7_xboole_0,axiom,(![A]:(![B]:(disjoint(A,B)<=>set_intersection2(A,B)=empty_set))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d7_xboole_0)).
% 48.45/48.62 fof(c34,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])).
% 48.45/48.62 fof(c35,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)],[c34])).
% 48.45/48.62 fof(c37,plain,(![X13]:(![X14]:(![X15]:(![X16]:((~disjoint(X13,X14)|set_intersection2(X13,X14)=empty_set)&(set_intersection2(X15,X16)!=empty_set|disjoint(X15,X16))))))),inference(shift_quantors,[status(thm)],[fof(c36,plain,((![X13]:(![X14]:(~disjoint(X13,X14)|set_intersection2(X13,X14)=empty_set)))&(![X15]:(![X16]:(set_intersection2(X15,X16)!=empty_set|disjoint(X15,X16))))),inference(variable_rename,[status(thm)],[c35])).])).
% 48.45/48.62 cnf(c38,plain,~disjoint(X92,X91)|set_intersection2(X92,X91)=empty_set,inference(split_conjunct,[status(thm)],[c37])).
% 48.45/48.62 fof(symmetry_r1_xboole_0,axiom,(![A]:(![B]:(disjoint(A,B)=>disjoint(B,A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', symmetry_r1_xboole_0)).
% 48.45/48.62 fof(c18,plain,(![A]:(![B]:(~disjoint(A,B)|disjoint(B,A)))),inference(fof_nnf,[status(thm)],[symmetry_r1_xboole_0])).
% 48.45/48.62 fof(c19,plain,(![X8]:(![X9]:(~disjoint(X8,X9)|disjoint(X9,X8)))),inference(variable_rename,[status(thm)],[c18])).
% 48.45/48.62 cnf(c20,plain,~disjoint(X45,X44)|disjoint(X44,X45),inference(split_conjunct,[status(thm)],[c19])).
% 48.45/48.62 cnf(reflexivity,axiom,X34=X34,theory(equality)).
% 48.45/48.62 fof(d1_xboole_0,axiom,(![A]:(A=empty_set<=>(![B]:(~in(B,A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_xboole_0)).
% 48.45/48.62 fof(c52,plain,(![A]:(A=empty_set<=>(![B]:~in(B,A)))),inference(fof_simplification,[status(thm)],[d1_xboole_0])).
% 48.45/48.62 fof(c53,plain,(![A]:((A!=empty_set|(![B]:~in(B,A)))&((?[B]:in(B,A))|A=empty_set))),inference(fof_nnf,[status(thm)],[c52])).
% 48.45/48.62 fof(c54,plain,((![A]:(A!=empty_set|(![B]:~in(B,A))))&(![A]:((?[B]:in(B,A))|A=empty_set))),inference(shift_quantors,[status(thm)],[c53])).
% 48.45/48.62 fof(c55,plain,((![X26]:(X26!=empty_set|(![X27]:~in(X27,X26))))&(![X28]:((?[X29]:in(X29,X28))|X28=empty_set))),inference(variable_rename,[status(thm)],[c54])).
% 48.45/48.62 fof(c57,plain,(![X26]:(![X27]:(![X28]:((X26!=empty_set|~in(X27,X26))&(in(skolem0009(X28),X28)|X28=empty_set))))),inference(shift_quantors,[status(thm)],[fof(c56,plain,((![X26]:(X26!=empty_set|(![X27]:~in(X27,X26))))&(![X28]:(in(skolem0009(X28),X28)|X28=empty_set))),inference(skolemize,[status(esa)],[c55])).])).
% 48.45/48.62 cnf(c58,plain,X57!=empty_set|~in(X56,X57),inference(split_conjunct,[status(thm)],[c57])).
% 48.45/48.62 cnf(c166,plain,~in(X127,set_intersection2(X126,X128))|in(X127,X126),inference(resolution,[status(thm)],[c46, reflexivity])).
% 48.45/48.62 cnf(c59,plain,in(skolem0009(X75),X75)|X75=empty_set,inference(split_conjunct,[status(thm)],[c57])).
% 48.45/48.62 cnf(c39,plain,set_intersection2(X93,X94)!=empty_set|disjoint(X93,X94),inference(split_conjunct,[status(thm)],[c37])).
% 48.45/48.62 cnf(c117,plain,disjoint(X305,X304)|in(skolem0009(set_intersection2(X305,X304)),set_intersection2(X305,X304)),inference(resolution,[status(thm)],[c39, c59])).
% 48.45/48.62 cnf(c799,plain,disjoint(X308,X309)|in(skolem0009(set_intersection2(X308,X309)),X308),inference(resolution,[status(thm)],[c117, c166])).
% 48.45/48.62 cnf(c810,plain,disjoint(X310,X311)|X310!=empty_set,inference(resolution,[status(thm)],[c799, c58])).
% 48.45/48.62 cnf(c819,plain,disjoint(empty_set,X312),inference(resolution,[status(thm)],[c810, reflexivity])).
% 48.45/48.62 cnf(c825,plain,disjoint(X315,empty_set),inference(resolution,[status(thm)],[c819, c20])).
% 48.45/48.62 cnf(c842,plain,set_intersection2(X333,empty_set)=empty_set,inference(resolution,[status(thm)],[c825, c38])).
% 48.45/48.62 cnf(c937,plain,empty_set=set_intersection2(X348,empty_set),inference(resolution,[status(thm)],[c842, symmetry])).
% 48.45/48.62 cnf(c1057,plain,X867!=empty_set|X867=set_intersection2(X866,empty_set),inference(resolution,[status(thm)],[c937, transitivity])).
% 48.45/48.62 fof(t3_xboole_0,conjecture,(![A]:(![B]:((~((~disjoint(A,B))&(![C]:(~(in(C,A)&in(C,B))))))&(~((?[C]:(in(C,A)&in(C,B)))&disjoint(A,B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t3_xboole_0)).
% 48.45/48.62 fof(c4,negated_conjecture,(~(![A]:(![B]:((~((~disjoint(A,B))&(![C]:(~(in(C,A)&in(C,B))))))&(~((?[C]:(in(C,A)&in(C,B)))&disjoint(A,B))))))),inference(assume_negation,[status(cth)],[t3_xboole_0])).
% 48.45/48.62 fof(c5,negated_conjecture,(~(![A]:(![B]:((~(~disjoint(A,B)&(![C]:(~(in(C,A)&in(C,B))))))&(~((?[C]:(in(C,A)&in(C,B)))&disjoint(A,B))))))),inference(fof_simplification,[status(thm)],[c4])).
% 48.45/48.62 fof(c6,negated_conjecture,(?[A]:(?[B]:((~disjoint(A,B)&(![C]:(~in(C,A)|~in(C,B))))|((?[C]:(in(C,A)&in(C,B)))&disjoint(A,B))))),inference(fof_nnf,[status(thm)],[c5])).
% 48.45/48.62 fof(c7,negated_conjecture,((?[A]:(?[B]:(~disjoint(A,B)&(![C]:(~in(C,A)|~in(C,B))))))|(?[A]:(?[B]:((?[C]:(in(C,A)&in(C,B)))&disjoint(A,B))))),inference(shift_quantors,[status(thm)],[c6])).
% 48.45/48.62 fof(c8,negated_conjecture,((?[X2]:(?[X3]:(~disjoint(X2,X3)&(![X4]:(~in(X4,X2)|~in(X4,X3))))))|(?[X5]:(?[X6]:((?[X7]:(in(X7,X5)&in(X7,X6)))&disjoint(X5,X6))))),inference(variable_rename,[status(thm)],[c7])).
% 48.45/48.62 fof(c10,negated_conjecture,(![X4]:((~disjoint(skolem0001,skolem0002)&(~in(X4,skolem0001)|~in(X4,skolem0002)))|((in(skolem0005,skolem0003)&in(skolem0005,skolem0004))&disjoint(skolem0003,skolem0004)))),inference(shift_quantors,[status(thm)],[fof(c9,negated_conjecture,((~disjoint(skolem0001,skolem0002)&(![X4]:(~in(X4,skolem0001)|~in(X4,skolem0002))))|((in(skolem0005,skolem0003)&in(skolem0005,skolem0004))&disjoint(skolem0003,skolem0004))),inference(skolemize,[status(esa)],[c8])).])).
% 48.45/48.62 fof(c11,negated_conjecture,(![X4]:((((~disjoint(skolem0001,skolem0002)|in(skolem0005,skolem0003))&(~disjoint(skolem0001,skolem0002)|in(skolem0005,skolem0004)))&(~disjoint(skolem0001,skolem0002)|disjoint(skolem0003,skolem0004)))&((((~in(X4,skolem0001)|~in(X4,skolem0002))|in(skolem0005,skolem0003))&((~in(X4,skolem0001)|~in(X4,skolem0002))|in(skolem0005,skolem0004)))&((~in(X4,skolem0001)|~in(X4,skolem0002))|disjoint(skolem0003,skolem0004))))),inference(distribute,[status(thm)],[c10])).
% 48.45/48.62 cnf(c14,negated_conjecture,~disjoint(skolem0001,skolem0002)|disjoint(skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c11])).
% 48.45/48.62 fof(commutativity_k3_xboole_0,axiom,(![A]:(![B]:set_intersection2(A,B)=set_intersection2(B,A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', commutativity_k3_xboole_0)).
% 48.45/48.62 fof(c60,plain,(![X30]:(![X31]:set_intersection2(X30,X31)=set_intersection2(X31,X30))),inference(variable_rename,[status(thm)],[commutativity_k3_xboole_0])).
% 48.45/48.62 cnf(c61,plain,set_intersection2(X67,X68)=set_intersection2(X68,X67),inference(split_conjunct,[status(thm)],[c60])).
% 48.45/48.62 cnf(c164,plain,~in(X124,set_intersection2(X123,X125))|in(X124,X125),inference(resolution,[status(thm)],[c46, c61])).
% 48.45/48.62 cnf(c801,plain,disjoint(X636,X637)|in(skolem0009(set_intersection2(X636,X637)),X637),inference(resolution,[status(thm)],[c117, c164])).
% 48.45/48.62 cnf(c17,negated_conjecture,~in(X106,skolem0001)|~in(X106,skolem0002)|disjoint(skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c11])).
% 48.45/48.62 cnf(c811,plain,disjoint(skolem0002,X5579)|~in(skolem0009(set_intersection2(skolem0002,X5579)),skolem0001)|disjoint(skolem0003,skolem0004),inference(resolution,[status(thm)],[c799, c17])).
% 48.45/48.62 cnf(c49067,plain,disjoint(skolem0002,skolem0001)|disjoint(skolem0003,skolem0004),inference(resolution,[status(thm)],[c811, c801])).
% 48.45/48.62 cnf(c49068,plain,disjoint(skolem0003,skolem0004)|disjoint(skolem0001,skolem0002),inference(resolution,[status(thm)],[c49067, c20])).
% 48.45/48.62 cnf(c49078,plain,disjoint(skolem0003,skolem0004),inference(resolution,[status(thm)],[c49068, c14])).
% 48.45/48.62 cnf(c49083,plain,disjoint(skolem0004,skolem0003),inference(resolution,[status(thm)],[c49078, c20])).
% 48.45/48.62 cnf(c49087,plain,set_intersection2(skolem0004,skolem0003)=empty_set,inference(resolution,[status(thm)],[c49083, c38])).
% 48.45/48.62 cnf(c49383,plain,set_intersection2(skolem0004,skolem0003)=set_intersection2(X6005,empty_set),inference(resolution,[status(thm)],[c49087, c1057])).
% 48.45/48.62 cnf(c54593,plain,~in(X6185,set_intersection2(skolem0004,skolem0003))|in(X6185,X6184),inference(resolution,[status(thm)],[c49383, c46])).
% 48.45/48.62 cnf(c12,negated_conjecture,~disjoint(skolem0001,skolem0002)|in(skolem0005,skolem0003),inference(split_conjunct,[status(thm)],[c11])).
% 48.45/48.62 cnf(c15,negated_conjecture,~in(X95,skolem0001)|~in(X95,skolem0002)|in(skolem0005,skolem0003),inference(split_conjunct,[status(thm)],[c11])).
% 48.45/48.62 cnf(c816,plain,disjoint(skolem0002,X5591)|~in(skolem0009(set_intersection2(skolem0002,X5591)),skolem0001)|in(skolem0005,skolem0003),inference(resolution,[status(thm)],[c799, c15])).
% 48.45/48.62 cnf(c49436,plain,disjoint(skolem0002,skolem0001)|in(skolem0005,skolem0003),inference(resolution,[status(thm)],[c816, c801])).
% 48.45/48.62 cnf(c49942,plain,in(skolem0005,skolem0003)|disjoint(skolem0001,skolem0002),inference(resolution,[status(thm)],[c49436, c20])).
% 48.45/48.62 cnf(c50127,plain,in(skolem0005,skolem0003),inference(resolution,[status(thm)],[c49942, c12])).
% 48.45/48.62 cnf(c48,plain,X136!=set_intersection2(X137,X135)|~in(X134,X137)|~in(X134,X135)|in(X134,X136),inference(split_conjunct,[status(thm)],[c45])).
% 48.45/48.62 cnf(c188,plain,~in(X643,X644)|~in(X643,X642)|in(X643,set_intersection2(X642,X644)),inference(resolution,[status(thm)],[c48, c61])).
% 48.45/48.62 cnf(c13,negated_conjecture,~disjoint(skolem0001,skolem0002)|in(skolem0005,skolem0004),inference(split_conjunct,[status(thm)],[c11])).
% 48.45/48.62 cnf(c16,negated_conjecture,~in(X100,skolem0001)|~in(X100,skolem0002)|in(skolem0005,skolem0004),inference(split_conjunct,[status(thm)],[c11])).
% 48.45/48.62 cnf(c814,plain,disjoint(skolem0002,X5583)|~in(skolem0009(set_intersection2(skolem0002,X5583)),skolem0001)|in(skolem0005,skolem0004),inference(resolution,[status(thm)],[c799, c16])).
% 48.45/48.62 cnf(c49275,plain,disjoint(skolem0002,skolem0001)|in(skolem0005,skolem0004),inference(resolution,[status(thm)],[c814, c801])).
% 48.45/48.62 cnf(c49905,plain,in(skolem0005,skolem0004)|disjoint(skolem0001,skolem0002),inference(resolution,[status(thm)],[c49275, c20])).
% 48.45/48.62 cnf(c49989,plain,in(skolem0005,skolem0004),inference(resolution,[status(thm)],[c49905, c13])).
% 48.45/48.62 cnf(c49994,plain,~in(skolem0005,X6601)|in(skolem0005,set_intersection2(skolem0004,X6601)),inference(resolution,[status(thm)],[c49989, c188])).
% 48.45/48.62 cnf(c62322,plain,in(skolem0005,set_intersection2(skolem0004,skolem0003)),inference(resolution,[status(thm)],[c49994, c50127])).
% 48.45/48.62 cnf(c62342,plain,in(skolem0005,X6602),inference(resolution,[status(thm)],[c62322, c54593])).
% 48.45/48.62 cnf(c62464,plain,$false,inference(resolution,[status(thm)],[c62342, c73])).
% 48.45/48.62 % SZS output end CNFRefutation
% 48.45/48.62
% 48.45/48.62 % Initial clauses : 32
% 48.45/48.62 % Processed clauses : 1104
% 48.45/48.62 % Factors computed : 79
% 48.45/48.62 % Resolvents computed: 62321
% 48.45/48.62 % Tautologies deleted: 28
% 48.45/48.62 % Forward subsumed : 3044
% 48.45/48.62 % Backward subsumed : 139
% 48.45/48.62 % -------- CPU Time ---------
% 48.45/48.62 % User time : 48.127 s
% 48.45/48.62 % System time : 0.142 s
% 48.45/48.62 % Total time : 48.269 s
%------------------------------------------------------------------------------