%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET920+1 : TPTP v8.1.2. Released v3.2.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:22 EDT 2024
% Result : Theorem 1.04s 1.23s
% Output : Refutation 1.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : SET920+1 : TPTP v8.1.2. Released v3.2.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 19:00:07 EDT 2024
% 0.13/0.35 % CPUTime :
% 1.04/1.23 % Version: 1.5
% 1.04/1.23 % SZS status Theorem
% 1.04/1.23 % SZS output start CNFRefutation
% 1.04/1.23 fof(t63_zfmisc_1,conjecture,(![A]:(![B]:(![C]:(set_intersection2(unordered_pair(A,B),C)=unordered_pair(A,B)=>in(A,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t63_zfmisc_1)).
% 1.04/1.23 fof(c4,negated_conjecture,(~(![A]:(![B]:(![C]:(set_intersection2(unordered_pair(A,B),C)=unordered_pair(A,B)=>in(A,C)))))),inference(assume_negation,[status(cth)],[t63_zfmisc_1])).
% 1.04/1.23 fof(c5,negated_conjecture,(?[A]:(?[B]:(?[C]:(set_intersection2(unordered_pair(A,B),C)=unordered_pair(A,B)&~in(A,C))))),inference(fof_nnf,[status(thm)],[c4])).
% 1.04/1.23 fof(c6,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(set_intersection2(unordered_pair(X2,X3),X4)=unordered_pair(X2,X3)&~in(X2,X4))))),inference(variable_rename,[status(thm)],[c5])).
% 1.04/1.23 fof(c7,negated_conjecture,(set_intersection2(unordered_pair(skolem0001,skolem0002),skolem0003)=unordered_pair(skolem0001,skolem0002)&~in(skolem0001,skolem0003)),inference(skolemize,[status(esa)],[c6])).
% 1.04/1.23 cnf(c9,negated_conjecture,~in(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c7])).
% 1.04/1.23 cnf(reflexivity,axiom,X32=X32,theory(equality)).
% 1.04/1.23 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)).
% 1.04/1.23 fof(c32,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])).
% 1.04/1.23 fof(c33,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)],[c32])).
% 1.04/1.23 fof(c34,plain,((![X17]:(![X18]:(![X19]:(X19!=unordered_pair(X17,X18)|((![X20]:(~in(X20,X19)|(X20=X17|X20=X18)))&(![X21]:((X21!=X17&X21!=X18)|in(X21,X19))))))))&(![X22]:(![X23]:(![X24]:((?[X25]:((~in(X25,X24)|(X25!=X22&X25!=X23))&(in(X25,X24)|(X25=X22|X25=X23))))|X24=unordered_pair(X22,X23)))))),inference(variable_rename,[status(thm)],[c33])).
% 1.04/1.23 fof(c36,plain,(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:((X19!=unordered_pair(X17,X18)|((~in(X20,X19)|(X20=X17|X20=X18))&((X21!=X17&X21!=X18)|in(X21,X19))))&(((~in(skolem0007(X22,X23,X24),X24)|(skolem0007(X22,X23,X24)!=X22&skolem0007(X22,X23,X24)!=X23))&(in(skolem0007(X22,X23,X24),X24)|(skolem0007(X22,X23,X24)=X22|skolem0007(X22,X23,X24)=X23)))|X24=unordered_pair(X22,X23))))))))))),inference(shift_quantors,[status(thm)],[fof(c35,plain,((![X17]:(![X18]:(![X19]:(X19!=unordered_pair(X17,X18)|((![X20]:(~in(X20,X19)|(X20=X17|X20=X18)))&(![X21]:((X21!=X17&X21!=X18)|in(X21,X19))))))))&(![X22]:(![X23]:(![X24]:(((~in(skolem0007(X22,X23,X24),X24)|(skolem0007(X22,X23,X24)!=X22&skolem0007(X22,X23,X24)!=X23))&(in(skolem0007(X22,X23,X24),X24)|(skolem0007(X22,X23,X24)=X22|skolem0007(X22,X23,X24)=X23)))|X24=unordered_pair(X22,X23)))))),inference(skolemize,[status(esa)],[c34])).])).
% 1.04/1.23 fof(c37,plain,(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(((X19!=unordered_pair(X17,X18)|(~in(X20,X19)|(X20=X17|X20=X18)))&((X19!=unordered_pair(X17,X18)|(X21!=X17|in(X21,X19)))&(X19!=unordered_pair(X17,X18)|(X21!=X18|in(X21,X19)))))&((((~in(skolem0007(X22,X23,X24),X24)|skolem0007(X22,X23,X24)!=X22)|X24=unordered_pair(X22,X23))&((~in(skolem0007(X22,X23,X24),X24)|skolem0007(X22,X23,X24)!=X23)|X24=unordered_pair(X22,X23)))&((in(skolem0007(X22,X23,X24),X24)|(skolem0007(X22,X23,X24)=X22|skolem0007(X22,X23,X24)=X23))|X24=unordered_pair(X22,X23)))))))))))),inference(distribute,[status(thm)],[c36])).
% 1.04/1.23 cnf(c39,plain,X187!=unordered_pair(X188,X186)|X189!=X188|in(X189,X187),inference(split_conjunct,[status(thm)],[c37])).
% 1.04/1.23 cnf(c292,plain,X191!=X190|in(X191,unordered_pair(X190,X192)),inference(resolution,[status(thm)],[c39, reflexivity])).
% 1.04/1.23 cnf(c307,plain,in(X193,unordered_pair(X193,X194)),inference(resolution,[status(thm)],[c292, reflexivity])).
% 1.04/1.23 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)).
% 1.04/1.23 fof(c20,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])).
% 1.04/1.23 fof(c21,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)],[c20])).
% 1.04/1.23 fof(c22,plain,((![X8]:(![X9]:(![X10]:(X10!=set_intersection2(X8,X9)|((![X11]:(~in(X11,X10)|(in(X11,X8)&in(X11,X9))))&(![X12]:((~in(X12,X8)|~in(X12,X9))|in(X12,X10))))))))&(![X13]:(![X14]:(![X15]:((?[X16]:((~in(X16,X15)|(~in(X16,X13)|~in(X16,X14)))&(in(X16,X15)|(in(X16,X13)&in(X16,X14)))))|X15=set_intersection2(X13,X14)))))),inference(variable_rename,[status(thm)],[c21])).
% 1.04/1.23 fof(c24,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:((X10!=set_intersection2(X8,X9)|((~in(X11,X10)|(in(X11,X8)&in(X11,X9)))&((~in(X12,X8)|~in(X12,X9))|in(X12,X10))))&(((~in(skolem0006(X13,X14,X15),X15)|(~in(skolem0006(X13,X14,X15),X13)|~in(skolem0006(X13,X14,X15),X14)))&(in(skolem0006(X13,X14,X15),X15)|(in(skolem0006(X13,X14,X15),X13)&in(skolem0006(X13,X14,X15),X14))))|X15=set_intersection2(X13,X14))))))))))),inference(shift_quantors,[status(thm)],[fof(c23,plain,((![X8]:(![X9]:(![X10]:(X10!=set_intersection2(X8,X9)|((![X11]:(~in(X11,X10)|(in(X11,X8)&in(X11,X9))))&(![X12]:((~in(X12,X8)|~in(X12,X9))|in(X12,X10))))))))&(![X13]:(![X14]:(![X15]:(((~in(skolem0006(X13,X14,X15),X15)|(~in(skolem0006(X13,X14,X15),X13)|~in(skolem0006(X13,X14,X15),X14)))&(in(skolem0006(X13,X14,X15),X15)|(in(skolem0006(X13,X14,X15),X13)&in(skolem0006(X13,X14,X15),X14))))|X15=set_intersection2(X13,X14)))))),inference(skolemize,[status(esa)],[c22])).])).
% 1.04/1.23 fof(c25,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:((((X10!=set_intersection2(X8,X9)|(~in(X11,X10)|in(X11,X8)))&(X10!=set_intersection2(X8,X9)|(~in(X11,X10)|in(X11,X9))))&(X10!=set_intersection2(X8,X9)|((~in(X12,X8)|~in(X12,X9))|in(X12,X10))))&(((~in(skolem0006(X13,X14,X15),X15)|(~in(skolem0006(X13,X14,X15),X13)|~in(skolem0006(X13,X14,X15),X14)))|X15=set_intersection2(X13,X14))&(((in(skolem0006(X13,X14,X15),X15)|in(skolem0006(X13,X14,X15),X13))|X15=set_intersection2(X13,X14))&((in(skolem0006(X13,X14,X15),X15)|in(skolem0006(X13,X14,X15),X14))|X15=set_intersection2(X13,X14))))))))))))),inference(distribute,[status(thm)],[c24])).
% 1.04/1.23 cnf(c27,plain,X107!=set_intersection2(X105,X104)|~in(X106,X107)|in(X106,X104),inference(split_conjunct,[status(thm)],[c25])).
% 1.04/1.23 cnf(symmetry,axiom,X35!=X34|X34=X35,theory(equality)).
% 1.04/1.23 cnf(c8,negated_conjecture,set_intersection2(unordered_pair(skolem0001,skolem0002),skolem0003)=unordered_pair(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c7])).
% 1.04/1.23 cnf(c99,plain,unordered_pair(skolem0001,skolem0002)=set_intersection2(unordered_pair(skolem0001,skolem0002),skolem0003),inference(resolution,[status(thm)],[c8, symmetry])).
% 1.04/1.23 cnf(c1201,plain,~in(X763,unordered_pair(skolem0001,skolem0002))|in(X763,skolem0003),inference(resolution,[status(thm)],[c99, c27])).
% 1.04/1.23 cnf(c2239,plain,in(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1201, c307])).
% 1.04/1.23 cnf(c2251,plain,$false,inference(resolution,[status(thm)],[c2239, c9])).
% 1.04/1.23 % SZS output end CNFRefutation
% 1.04/1.23
% 1.04/1.23 % Initial clauses : 27
% 1.04/1.23 % Processed clauses : 176
% 1.04/1.23 % Factors computed : 12
% 1.04/1.23 % Resolvents computed: 2191
% 1.04/1.23 % Tautologies deleted: 8
% 1.04/1.23 % Forward subsumed : 191
% 1.04/1.23 % Backward subsumed : 1
% 1.04/1.23 % -------- CPU Time ---------
% 1.04/1.23 % User time : 0.854 s
% 1.04/1.23 % System time : 0.024 s
% 1.04/1.23 % Total time : 0.878 s
%------------------------------------------------------------------------------