%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET988+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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:27 EDT 2024
% Result : Theorem 237.90s 238.13s
% Output : Refutation 237.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SET988+1 : TPTP v8.1.2. Released v3.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n011.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:01:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 237.90/238.13 % Version: 1.5
% 237.90/238.13 % SZS status Theorem
% 237.90/238.13 % SZS output start CNFRefutation
% 237.90/238.13 fof(t2_funct_1,conjecture,(![A]:(((![B]:(~(in(B,A)&(![C]:(![D]:ordered_pair(C,D)!=B)))))&(![B]:(![C]:(![D]:((in(ordered_pair(B,C),A)&in(ordered_pair(B,D),A))=>C=D)))))=>(relation(A)&function(A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t2_funct_1)).
% 237.90/238.13 fof(c30,negated_conjecture,(~(![A]:(((![B]:(~(in(B,A)&(![C]:(![D]:ordered_pair(C,D)!=B)))))&(![B]:(![C]:(![D]:((in(ordered_pair(B,C),A)&in(ordered_pair(B,D),A))=>C=D)))))=>(relation(A)&function(A))))),inference(assume_negation,[status(cth)],[t2_funct_1])).
% 237.90/238.13 fof(c31,negated_conjecture,(?[A]:(((![B]:(~in(B,A)|(?[C]:(?[D]:ordered_pair(C,D)=B))))&(![B]:(![C]:(![D]:((~in(ordered_pair(B,C),A)|~in(ordered_pair(B,D),A))|C=D)))))&(~relation(A)|~function(A)))),inference(fof_nnf,[status(thm)],[c30])).
% 237.90/238.13 fof(c32,negated_conjecture,(?[X18]:(((![X19]:(~in(X19,X18)|(?[X20]:(?[X21]:ordered_pair(X20,X21)=X19))))&(![X22]:(![X23]:(![X24]:((~in(ordered_pair(X22,X23),X18)|~in(ordered_pair(X22,X24),X18))|X23=X24)))))&(~relation(X18)|~function(X18)))),inference(variable_rename,[status(thm)],[c31])).
% 237.90/238.13 fof(c34,negated_conjecture,(![X19]:(![X22]:(![X23]:(![X24]:(((~in(X19,skolem0007)|ordered_pair(skolem0008(X19),skolem0009(X19))=X19)&((~in(ordered_pair(X22,X23),skolem0007)|~in(ordered_pair(X22,X24),skolem0007))|X23=X24))&(~relation(skolem0007)|~function(skolem0007))))))),inference(shift_quantors,[status(thm)],[fof(c33,negated_conjecture,(((![X19]:(~in(X19,skolem0007)|ordered_pair(skolem0008(X19),skolem0009(X19))=X19))&(![X22]:(![X23]:(![X24]:((~in(ordered_pair(X22,X23),skolem0007)|~in(ordered_pair(X22,X24),skolem0007))|X23=X24)))))&(~relation(skolem0007)|~function(skolem0007))),inference(skolemize,[status(esa)],[c32])).])).
% 237.90/238.13 cnf(c37,negated_conjecture,~relation(skolem0007)|~function(skolem0007),inference(split_conjunct,[status(thm)],[c34])).
% 237.90/238.13 fof(d1_funct_1,axiom,(![A]:(function(A)<=>(![B]:(![C]:(![D]:((in(ordered_pair(B,C),A)&in(ordered_pair(B,D),A))=>C=D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_funct_1)).
% 237.90/238.13 fof(c20,plain,(![A]:((~function(A)|(![B]:(![C]:(![D]:((~in(ordered_pair(B,C),A)|~in(ordered_pair(B,D),A))|C=D)))))&((?[B]:(?[C]:(?[D]:((in(ordered_pair(B,C),A)&in(ordered_pair(B,D),A))&C!=D))))|function(A)))),inference(fof_nnf,[status(thm)],[d1_funct_1])).
% 237.90/238.13 fof(c21,plain,((![A]:(~function(A)|(![B]:(![C]:(![D]:((~in(ordered_pair(B,C),A)|~in(ordered_pair(B,D),A))|C=D))))))&(![A]:((?[B]:(?[C]:(?[D]:((in(ordered_pair(B,C),A)&in(ordered_pair(B,D),A))&C!=D))))|function(A)))),inference(shift_quantors,[status(thm)],[c20])).
% 237.90/238.13 fof(c22,plain,((![X10]:(~function(X10)|(![X11]:(![X12]:(![X13]:((~in(ordered_pair(X11,X12),X10)|~in(ordered_pair(X11,X13),X10))|X12=X13))))))&(![X14]:((?[X15]:(?[X16]:(?[X17]:((in(ordered_pair(X15,X16),X14)&in(ordered_pair(X15,X17),X14))&X16!=X17))))|function(X14)))),inference(variable_rename,[status(thm)],[c21])).
% 237.90/238.13 fof(c24,plain,(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:((~function(X10)|((~in(ordered_pair(X11,X12),X10)|~in(ordered_pair(X11,X13),X10))|X12=X13))&(((in(ordered_pair(skolem0004(X14),skolem0005(X14)),X14)&in(ordered_pair(skolem0004(X14),skolem0006(X14)),X14))&skolem0005(X14)!=skolem0006(X14))|function(X14)))))))),inference(shift_quantors,[status(thm)],[fof(c23,plain,((![X10]:(~function(X10)|(![X11]:(![X12]:(![X13]:((~in(ordered_pair(X11,X12),X10)|~in(ordered_pair(X11,X13),X10))|X12=X13))))))&(![X14]:(((in(ordered_pair(skolem0004(X14),skolem0005(X14)),X14)&in(ordered_pair(skolem0004(X14),skolem0006(X14)),X14))&skolem0005(X14)!=skolem0006(X14))|function(X14)))),inference(skolemize,[status(esa)],[c22])).])).
% 237.90/238.13 fof(c25,plain,(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:((~function(X10)|((~in(ordered_pair(X11,X12),X10)|~in(ordered_pair(X11,X13),X10))|X12=X13))&(((in(ordered_pair(skolem0004(X14),skolem0005(X14)),X14)|function(X14))&(in(ordered_pair(skolem0004(X14),skolem0006(X14)),X14)|function(X14)))&(skolem0005(X14)!=skolem0006(X14)|function(X14))))))))),inference(distribute,[status(thm)],[c24])).
% 237.90/238.13 cnf(c29,plain,skolem0005(X175)!=skolem0006(X175)|function(X175),inference(split_conjunct,[status(thm)],[c25])).
% 237.90/238.13 cnf(c27,plain,in(ordered_pair(skolem0004(X166),skolem0005(X166)),X166)|function(X166),inference(split_conjunct,[status(thm)],[c25])).
% 237.90/238.13 cnf(c28,plain,in(ordered_pair(skolem0004(X173),skolem0006(X173)),X173)|function(X173),inference(split_conjunct,[status(thm)],[c25])).
% 237.90/238.13 cnf(c36,negated_conjecture,~in(ordered_pair(X183,X184),skolem0007)|~in(ordered_pair(X183,X185),skolem0007)|X184=X185,inference(split_conjunct,[status(thm)],[c34])).
% 237.90/238.13 cnf(c329,plain,~in(ordered_pair(skolem0004(skolem0007),X572),skolem0007)|X572=skolem0006(skolem0007)|function(skolem0007),inference(resolution,[status(thm)],[c36, c28])).
% 237.90/238.13 cnf(c2791,plain,skolem0005(skolem0007)=skolem0006(skolem0007)|function(skolem0007),inference(resolution,[status(thm)],[c329, c27])).
% 237.90/238.13 cnf(c86212,plain,function(skolem0007),inference(resolution,[status(thm)],[c2791, c29])).
% 237.90/238.13 cnf(c86307,plain,~relation(skolem0007),inference(resolution,[status(thm)],[c86212, c37])).
% 237.90/238.13 fof(d1_relat_1,axiom,(![A]:(relation(A)<=>(![B]:(~(in(B,A)&(![C]:(![D]:B!=ordered_pair(C,D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_relat_1)).
% 237.90/238.13 fof(c11,plain,(![A]:((~relation(A)|(![B]:(~in(B,A)|(?[C]:(?[D]:B=ordered_pair(C,D))))))&((?[B]:(in(B,A)&(![C]:(![D]:B!=ordered_pair(C,D)))))|relation(A)))),inference(fof_nnf,[status(thm)],[d1_relat_1])).
% 237.90/238.13 fof(c12,plain,((![A]:(~relation(A)|(![B]:(~in(B,A)|(?[C]:(?[D]:B=ordered_pair(C,D)))))))&(![A]:((?[B]:(in(B,A)&(![C]:(![D]:B!=ordered_pair(C,D)))))|relation(A)))),inference(shift_quantors,[status(thm)],[c11])).
% 237.90/238.13 fof(c13,plain,((![X2]:(~relation(X2)|(![X3]:(~in(X3,X2)|(?[X4]:(?[X5]:X3=ordered_pair(X4,X5)))))))&(![X6]:((?[X7]:(in(X7,X6)&(![X8]:(![X9]:X7!=ordered_pair(X8,X9)))))|relation(X6)))),inference(variable_rename,[status(thm)],[c12])).
% 237.90/238.13 fof(c15,plain,(![X2]:(![X3]:(![X6]:(![X8]:(![X9]:((~relation(X2)|(~in(X3,X2)|X3=ordered_pair(skolem0001(X2,X3),skolem0002(X2,X3))))&((in(skolem0003(X6),X6)&skolem0003(X6)!=ordered_pair(X8,X9))|relation(X6)))))))),inference(shift_quantors,[status(thm)],[fof(c14,plain,((![X2]:(~relation(X2)|(![X3]:(~in(X3,X2)|X3=ordered_pair(skolem0001(X2,X3),skolem0002(X2,X3))))))&(![X6]:((in(skolem0003(X6),X6)&(![X8]:(![X9]:skolem0003(X6)!=ordered_pair(X8,X9))))|relation(X6)))),inference(skolemize,[status(esa)],[c13])).])).
% 237.90/238.13 fof(c16,plain,(![X2]:(![X3]:(![X6]:(![X8]:(![X9]:((~relation(X2)|(~in(X3,X2)|X3=ordered_pair(skolem0001(X2,X3),skolem0002(X2,X3))))&((in(skolem0003(X6),X6)|relation(X6))&(skolem0003(X6)!=ordered_pair(X8,X9)|relation(X6))))))))),inference(distribute,[status(thm)],[c15])).
% 237.90/238.13 cnf(c19,plain,skolem0003(X151)!=ordered_pair(X150,X149)|relation(X151),inference(split_conjunct,[status(thm)],[c16])).
% 237.90/238.13 cnf(symmetry,axiom,X73!=X72|X72=X73,theory(equality)).
% 237.90/238.13 cnf(c18,plain,in(skolem0003(X147),X147)|relation(X147),inference(split_conjunct,[status(thm)],[c16])).
% 237.90/238.13 cnf(c35,negated_conjecture,~in(X180,skolem0007)|ordered_pair(skolem0008(X180),skolem0009(X180))=X180,inference(split_conjunct,[status(thm)],[c34])).
% 237.90/238.13 cnf(c306,plain,ordered_pair(skolem0008(skolem0003(skolem0007)),skolem0009(skolem0003(skolem0007)))=skolem0003(skolem0007)|relation(skolem0007),inference(resolution,[status(thm)],[c35, c18])).
% 237.90/238.13 cnf(c2310,plain,relation(skolem0007)|skolem0003(skolem0007)=ordered_pair(skolem0008(skolem0003(skolem0007)),skolem0009(skolem0003(skolem0007))),inference(resolution,[status(thm)],[c306, symmetry])).
% 237.90/238.13 cnf(c162118,plain,relation(skolem0007),inference(resolution,[status(thm)],[c2310, c19])).
% 237.90/238.13 cnf(c162237,plain,$false,inference(resolution,[status(thm)],[c162118, c86307])).
% 237.90/238.13 % SZS output end CNFRefutation
% 237.90/238.13
% 237.90/238.13 % Initial clauses : 64
% 237.90/238.13 % Processed clauses : 2984
% 237.90/238.13 % Factors computed : 14
% 237.90/238.13 % Resolvents computed: 162086
% 237.90/238.13 % Tautologies deleted: 31
% 237.90/238.13 % Forward subsumed : 5872
% 237.90/238.13 % Backward subsumed : 231
% 237.90/238.13 % -------- CPU Time ---------
% 237.90/238.13 % User time : 237.220 s
% 237.90/238.13 % System time : 0.512 s
% 237.90/238.13 % Total time : 237.732 s
%------------------------------------------------------------------------------