%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET914+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n022.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:21 EDT 2024
% Result : Theorem 8.21s 8.39s
% Output : Refutation 8.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : SET914+1 : TPTP v8.1.2. Released v3.2.0.
% 0.09/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n022.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Wed May 8 19:02:08 EDT 2024
% 0.15/0.37 % CPUTime :
% 8.21/8.39 % Version: 1.5
% 8.21/8.39 % SZS status Theorem
% 8.21/8.39 % SZS output start CNFRefutation
% 8.21/8.39 fof(t55_zfmisc_1,conjecture,(![A]:(![B]:(![C]:(~(disjoint(unordered_pair(A,B),C)&in(A,C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t55_zfmisc_1)).
% 8.21/8.39 fof(c5,negated_conjecture,(~(![A]:(![B]:(![C]:(~(disjoint(unordered_pair(A,B),C)&in(A,C))))))),inference(assume_negation,[status(cth)],[t55_zfmisc_1])).
% 8.21/8.39 fof(c6,negated_conjecture,(?[A]:(?[B]:(?[C]:(disjoint(unordered_pair(A,B),C)&in(A,C))))),inference(fof_nnf,[status(thm)],[c5])).
% 8.21/8.39 fof(c7,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(disjoint(unordered_pair(X2,X3),X4)&in(X2,X4))))),inference(variable_rename,[status(thm)],[c6])).
% 8.21/8.39 fof(c8,negated_conjecture,(disjoint(unordered_pair(skolem0001,skolem0002),skolem0003)&in(skolem0001,skolem0003)),inference(skolemize,[status(esa)],[c7])).
% 8.21/8.39 cnf(c9,negated_conjecture,disjoint(unordered_pair(skolem0001,skolem0002),skolem0003),inference(split_conjunct,[status(thm)],[c8])).
% 8.21/8.39 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)).
% 8.21/8.39 fof(c25,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])).
% 8.21/8.39 fof(c26,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)],[c25])).
% 8.21/8.39 fof(c28,plain,(![X10]:(![X11]:(![X12]:(![X13]:((~disjoint(X10,X11)|set_intersection2(X10,X11)=empty_set)&(set_intersection2(X12,X13)!=empty_set|disjoint(X12,X13))))))),inference(shift_quantors,[status(thm)],[fof(c27,plain,((![X10]:(![X11]:(~disjoint(X10,X11)|set_intersection2(X10,X11)=empty_set)))&(![X12]:(![X13]:(set_intersection2(X12,X13)!=empty_set|disjoint(X12,X13))))),inference(variable_rename,[status(thm)],[c26])).])).
% 8.21/8.39 cnf(c29,plain,~disjoint(X92,X93)|set_intersection2(X92,X93)=empty_set,inference(split_conjunct,[status(thm)],[c28])).
% 8.21/8.39 cnf(c126,plain,set_intersection2(unordered_pair(skolem0001,skolem0002),skolem0003)=empty_set,inference(resolution,[status(thm)],[c29, c9])).
% 8.21/8.39 fof(d1_xboole_0,axiom,(![A]:(A=empty_set<=>(![B]:(~in(B,A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_xboole_0)).
% 8.21/8.39 fof(c55,plain,(![A]:(A=empty_set<=>(![B]:~in(B,A)))),inference(fof_simplification,[status(thm)],[d1_xboole_0])).
% 8.21/8.39 fof(c56,plain,(![A]:((A!=empty_set|(![B]:~in(B,A)))&((?[B]:in(B,A))|A=empty_set))),inference(fof_nnf,[status(thm)],[c55])).
% 8.21/8.39 fof(c57,plain,((![A]:(A!=empty_set|(![B]:~in(B,A))))&(![A]:((?[B]:in(B,A))|A=empty_set))),inference(shift_quantors,[status(thm)],[c56])).
% 8.21/8.39 fof(c58,plain,((![X32]:(X32!=empty_set|(![X33]:~in(X33,X32))))&(![X34]:((?[X35]:in(X35,X34))|X34=empty_set))),inference(variable_rename,[status(thm)],[c57])).
% 8.21/8.39 fof(c60,plain,(![X32]:(![X33]:(![X34]:((X32!=empty_set|~in(X33,X32))&(in(skolem0008(X34),X34)|X34=empty_set))))),inference(shift_quantors,[status(thm)],[fof(c59,plain,((![X32]:(X32!=empty_set|(![X33]:~in(X33,X32))))&(![X34]:(in(skolem0008(X34),X34)|X34=empty_set))),inference(skolemize,[status(esa)],[c58])).])).
% 8.21/8.39 cnf(c61,plain,X64!=empty_set|~in(X65,X64),inference(split_conjunct,[status(thm)],[c60])).
% 8.21/8.39 cnf(c10,negated_conjecture,in(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c8])).
% 8.21/8.39 cnf(reflexivity,axiom,X42=X42,theory(equality)).
% 8.21/8.39 fof(d2_tarski,axiom,(![A]:(![B]:(![C]:(C=unordered_pair(A,B)<=>(![D]:(in(D,C)<=>(D=A|D=B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d2_tarski)).
% 8.21/8.39 fof(c43,plain,(![A]:(![B]:(![C]:((C!=unordered_pair(A,B)|(![D]:((~in(D,C)|(D=A|D=B))&((D!=A&D!=B)|in(D,C)))))&((?[D]:((~in(D,C)|(D!=A&D!=B))&(in(D,C)|(D=A|D=B))))|C=unordered_pair(A,B)))))),inference(fof_nnf,[status(thm)],[d2_tarski])).
% 8.21/8.39 fof(c44,plain,((![A]:(![B]:(![C]:(C!=unordered_pair(A,B)|((![D]:(~in(D,C)|(D=A|D=B)))&(![D]:((D!=A&D!=B)|in(D,C))))))))&(![A]:(![B]:(![C]:((?[D]:((~in(D,C)|(D!=A&D!=B))&(in(D,C)|(D=A|D=B))))|C=unordered_pair(A,B)))))),inference(shift_quantors,[status(thm)],[c43])).
% 8.21/8.39 fof(c45,plain,((![X23]:(![X24]:(![X25]:(X25!=unordered_pair(X23,X24)|((![X26]:(~in(X26,X25)|(X26=X23|X26=X24)))&(![X27]:((X27!=X23&X27!=X24)|in(X27,X25))))))))&(![X28]:(![X29]:(![X30]:((?[X31]:((~in(X31,X30)|(X31!=X28&X31!=X29))&(in(X31,X30)|(X31=X28|X31=X29))))|X30=unordered_pair(X28,X29)))))),inference(variable_rename,[status(thm)],[c44])).
% 8.21/8.39 fof(c47,plain,(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:((X25!=unordered_pair(X23,X24)|((~in(X26,X25)|(X26=X23|X26=X24))&((X27!=X23&X27!=X24)|in(X27,X25))))&(((~in(skolem0007(X28,X29,X30),X30)|(skolem0007(X28,X29,X30)!=X28&skolem0007(X28,X29,X30)!=X29))&(in(skolem0007(X28,X29,X30),X30)|(skolem0007(X28,X29,X30)=X28|skolem0007(X28,X29,X30)=X29)))|X30=unordered_pair(X28,X29))))))))))),inference(shift_quantors,[status(thm)],[fof(c46,plain,((![X23]:(![X24]:(![X25]:(X25!=unordered_pair(X23,X24)|((![X26]:(~in(X26,X25)|(X26=X23|X26=X24)))&(![X27]:((X27!=X23&X27!=X24)|in(X27,X25))))))))&(![X28]:(![X29]:(![X30]:(((~in(skolem0007(X28,X29,X30),X30)|(skolem0007(X28,X29,X30)!=X28&skolem0007(X28,X29,X30)!=X29))&(in(skolem0007(X28,X29,X30),X30)|(skolem0007(X28,X29,X30)=X28|skolem0007(X28,X29,X30)=X29)))|X30=unordered_pair(X28,X29)))))),inference(skolemize,[status(esa)],[c45])).])).
% 8.21/8.39 fof(c48,plain,(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(((X25!=unordered_pair(X23,X24)|(~in(X26,X25)|(X26=X23|X26=X24)))&((X25!=unordered_pair(X23,X24)|(X27!=X23|in(X27,X25)))&(X25!=unordered_pair(X23,X24)|(X27!=X24|in(X27,X25)))))&((((~in(skolem0007(X28,X29,X30),X30)|skolem0007(X28,X29,X30)!=X28)|X30=unordered_pair(X28,X29))&((~in(skolem0007(X28,X29,X30),X30)|skolem0007(X28,X29,X30)!=X29)|X30=unordered_pair(X28,X29)))&((in(skolem0007(X28,X29,X30),X30)|(skolem0007(X28,X29,X30)=X28|skolem0007(X28,X29,X30)=X29))|X30=unordered_pair(X28,X29)))))))))))),inference(distribute,[status(thm)],[c47])).
% 8.21/8.39 cnf(c50,plain,X170!=unordered_pair(X169,X171)|X168!=X169|in(X168,X170),inference(split_conjunct,[status(thm)],[c48])).
% 8.21/8.39 cnf(c272,plain,X196!=X197|in(X196,unordered_pair(X197,X195)),inference(resolution,[status(thm)],[c50, reflexivity])).
% 8.21/8.39 cnf(c312,plain,in(X201,unordered_pair(X201,X202)),inference(resolution,[status(thm)],[c272, reflexivity])).
% 8.21/8.39 fof(commutativity_k3_xboole_0,axiom,(![A]:(![B]:set_intersection2(A,B)=set_intersection2(B,A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', commutativity_k3_xboole_0)).
% 8.21/8.39 fof(c63,plain,(![X36]:(![X37]:set_intersection2(X36,X37)=set_intersection2(X37,X36))),inference(variable_rename,[status(thm)],[commutativity_k3_xboole_0])).
% 8.21/8.39 cnf(c64,plain,set_intersection2(X80,X79)=set_intersection2(X79,X80),inference(split_conjunct,[status(thm)],[c63])).
% 8.21/8.39 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)).
% 8.21/8.39 fof(c31,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])).
% 8.21/8.39 fof(c32,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)],[c31])).
% 8.21/8.39 fof(c33,plain,((![X14]:(![X15]:(![X16]:(X16!=set_intersection2(X14,X15)|((![X17]:(~in(X17,X16)|(in(X17,X14)&in(X17,X15))))&(![X18]:((~in(X18,X14)|~in(X18,X15))|in(X18,X16))))))))&(![X19]:(![X20]:(![X21]:((?[X22]:((~in(X22,X21)|(~in(X22,X19)|~in(X22,X20)))&(in(X22,X21)|(in(X22,X19)&in(X22,X20)))))|X21=set_intersection2(X19,X20)))))),inference(variable_rename,[status(thm)],[c32])).
% 8.21/8.39 fof(c35,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:((X16!=set_intersection2(X14,X15)|((~in(X17,X16)|(in(X17,X14)&in(X17,X15)))&((~in(X18,X14)|~in(X18,X15))|in(X18,X16))))&(((~in(skolem0006(X19,X20,X21),X21)|(~in(skolem0006(X19,X20,X21),X19)|~in(skolem0006(X19,X20,X21),X20)))&(in(skolem0006(X19,X20,X21),X21)|(in(skolem0006(X19,X20,X21),X19)&in(skolem0006(X19,X20,X21),X20))))|X21=set_intersection2(X19,X20))))))))))),inference(shift_quantors,[status(thm)],[fof(c34,plain,((![X14]:(![X15]:(![X16]:(X16!=set_intersection2(X14,X15)|((![X17]:(~in(X17,X16)|(in(X17,X14)&in(X17,X15))))&(![X18]:((~in(X18,X14)|~in(X18,X15))|in(X18,X16))))))))&(![X19]:(![X20]:(![X21]:(((~in(skolem0006(X19,X20,X21),X21)|(~in(skolem0006(X19,X20,X21),X19)|~in(skolem0006(X19,X20,X21),X20)))&(in(skolem0006(X19,X20,X21),X21)|(in(skolem0006(X19,X20,X21),X19)&in(skolem0006(X19,X20,X21),X20))))|X21=set_intersection2(X19,X20)))))),inference(skolemize,[status(esa)],[c33])).])).
% 8.21/8.39 fof(c36,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:((((X16!=set_intersection2(X14,X15)|(~in(X17,X16)|in(X17,X14)))&(X16!=set_intersection2(X14,X15)|(~in(X17,X16)|in(X17,X15))))&(X16!=set_intersection2(X14,X15)|((~in(X18,X14)|~in(X18,X15))|in(X18,X16))))&(((~in(skolem0006(X19,X20,X21),X21)|(~in(skolem0006(X19,X20,X21),X19)|~in(skolem0006(X19,X20,X21),X20)))|X21=set_intersection2(X19,X20))&(((in(skolem0006(X19,X20,X21),X21)|in(skolem0006(X19,X20,X21),X19))|X21=set_intersection2(X19,X20))&((in(skolem0006(X19,X20,X21),X21)|in(skolem0006(X19,X20,X21),X20))|X21=set_intersection2(X19,X20))))))))))))),inference(distribute,[status(thm)],[c35])).
% 8.21/8.39 cnf(c39,plain,X129!=set_intersection2(X130,X131)|~in(X128,X130)|~in(X128,X131)|in(X128,X129),inference(split_conjunct,[status(thm)],[c36])).
% 8.21/8.39 cnf(c169,plain,~in(X626,X625)|~in(X626,X624)|in(X626,set_intersection2(X624,X625)),inference(resolution,[status(thm)],[c39, c64])).
% 8.21/8.39 cnf(c2341,plain,~in(X2474,X2475)|in(X2474,set_intersection2(unordered_pair(X2474,X2473),X2475)),inference(resolution,[status(thm)],[c169, c312])).
% 8.21/8.39 cnf(c19939,plain,in(skolem0001,set_intersection2(unordered_pair(skolem0001,X2496),skolem0003)),inference(resolution,[status(thm)],[c2341, c10])).
% 8.21/8.39 cnf(c20180,plain,set_intersection2(unordered_pair(skolem0001,X2535),skolem0003)!=empty_set,inference(resolution,[status(thm)],[c19939, c61])).
% 8.21/8.39 cnf(c20632,plain,$false,inference(resolution,[status(thm)],[c20180, c126])).
% 8.21/8.39 % SZS output end CNFRefutation
% 8.21/8.39
% 8.21/8.39 % Initial clauses : 34
% 8.21/8.39 % Processed clauses : 551
% 8.21/8.39 % Factors computed : 60
% 8.21/8.39 % Resolvents computed: 20502
% 8.21/8.39 % Tautologies deleted: 19
% 8.21/8.39 % Forward subsumed : 892
% 8.21/8.39 % Backward subsumed : 31
% 8.21/8.39 % -------- CPU Time ---------
% 8.21/8.39 % User time : 7.952 s
% 8.21/8.39 % System time : 0.059 s
% 8.21/8.39 % Total time : 8.011 s
%------------------------------------------------------------------------------