%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU267+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:59 EDT 2024
% Result : Theorem 0.84s 1.02s
% Output : Refutation 0.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : SEU267+1 : TPTP v8.1.2. Released v3.3.0.
% 0.09/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n014.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % 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 11:15:38 EDT 2024
% 0.15/0.37 % CPUTime :
% 0.84/1.02 % Version: 1.5
% 0.84/1.02 % SZS status Theorem
% 0.84/1.02 % SZS output start CNFRefutation
% 0.84/1.02 fof(t7_mcart_1,conjecture,(![A]:(![B]:(pair_first(ordered_pair(A,B))=A&pair_second(ordered_pair(A,B))=B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t7_mcart_1)).
% 0.84/1.02 fof(c24,negated_conjecture,(~(![A]:(![B]:(pair_first(ordered_pair(A,B))=A&pair_second(ordered_pair(A,B))=B)))),inference(assume_negation,[status(cth)],[t7_mcart_1])).
% 0.84/1.02 fof(c25,negated_conjecture,(?[A]:(?[B]:(pair_first(ordered_pair(A,B))!=A|pair_second(ordered_pair(A,B))!=B))),inference(fof_nnf,[status(thm)],[c24])).
% 0.84/1.02 fof(c26,negated_conjecture,((?[A]:(?[B]:pair_first(ordered_pair(A,B))!=A))|(?[A]:(?[B]:pair_second(ordered_pair(A,B))!=B))),inference(shift_quantors,[status(thm)],[c25])).
% 0.84/1.02 fof(c27,negated_conjecture,((?[X20]:(?[X21]:pair_first(ordered_pair(X20,X21))!=X20))|(?[X22]:(?[X23]:pair_second(ordered_pair(X22,X23))!=X23))),inference(variable_rename,[status(thm)],[c26])).
% 0.84/1.02 fof(c28,negated_conjecture,(pair_first(ordered_pair(skolem0005,skolem0006))!=skolem0005|pair_second(ordered_pair(skolem0007,skolem0008))!=skolem0008),inference(skolemize,[status(esa)],[c27])).
% 0.84/1.02 cnf(c29,negated_conjecture,pair_first(ordered_pair(skolem0005,skolem0006))!=skolem0005|pair_second(ordered_pair(skolem0007,skolem0008))!=skolem0008,inference(split_conjunct,[status(thm)],[c28])).
% 0.84/1.02 cnf(reflexivity,axiom,X41=X41,theory(equality)).
% 0.84/1.02 fof(d2_mcart_1,axiom,(![A]:((?[B]:(?[C]:A=ordered_pair(B,C)))=>(![B]:(B=pair_second(A)<=>(![C]:(![D]:(A=ordered_pair(C,D)=>B=D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d2_mcart_1)).
% 0.84/1.02 fof(c6,plain,(![A]:((![B]:(![C]:A!=ordered_pair(B,C)))|(![B]:((B!=pair_second(A)|(![C]:(![D]:(A!=ordered_pair(C,D)|B=D))))&((?[C]:(?[D]:(A=ordered_pair(C,D)&B!=D)))|B=pair_second(A)))))),inference(fof_nnf,[status(thm)],[d2_mcart_1])).
% 0.84/1.02 fof(c7,plain,(![A]:((![B]:(![C]:A!=ordered_pair(B,C)))|((![B]:(B!=pair_second(A)|(![C]:(![D]:(A!=ordered_pair(C,D)|B=D)))))&(![B]:((?[C]:(?[D]:(A=ordered_pair(C,D)&B!=D)))|B=pair_second(A)))))),inference(shift_quantors,[status(thm)],[c6])).
% 0.84/1.02 fof(c8,plain,(![X2]:((![X3]:(![X4]:X2!=ordered_pair(X3,X4)))|((![X5]:(X5!=pair_second(X2)|(![X6]:(![X7]:(X2!=ordered_pair(X6,X7)|X5=X7)))))&(![X8]:((?[X9]:(?[X10]:(X2=ordered_pair(X9,X10)&X8!=X10)))|X8=pair_second(X2)))))),inference(variable_rename,[status(thm)],[c7])).
% 0.84/1.02 fof(c10,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(X2!=ordered_pair(X3,X4)|((X5!=pair_second(X2)|(X2!=ordered_pair(X6,X7)|X5=X7))&((X2=ordered_pair(skolem0001(X2,X8),skolem0002(X2,X8))&X8!=skolem0002(X2,X8))|X8=pair_second(X2))))))))))),inference(shift_quantors,[status(thm)],[fof(c9,plain,(![X2]:((![X3]:(![X4]:X2!=ordered_pair(X3,X4)))|((![X5]:(X5!=pair_second(X2)|(![X6]:(![X7]:(X2!=ordered_pair(X6,X7)|X5=X7)))))&(![X8]:((X2=ordered_pair(skolem0001(X2,X8),skolem0002(X2,X8))&X8!=skolem0002(X2,X8))|X8=pair_second(X2)))))),inference(skolemize,[status(esa)],[c8])).])).
% 0.84/1.02 fof(c11,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:((X2!=ordered_pair(X3,X4)|(X5!=pair_second(X2)|(X2!=ordered_pair(X6,X7)|X5=X7)))&((X2!=ordered_pair(X3,X4)|(X2=ordered_pair(skolem0001(X2,X8),skolem0002(X2,X8))|X8=pair_second(X2)))&(X2!=ordered_pair(X3,X4)|(X8!=skolem0002(X2,X8)|X8=pair_second(X2)))))))))))),inference(distribute,[status(thm)],[c10])).
% 0.84/1.02 cnf(c12,plain,X95!=ordered_pair(X92,X93)|X94!=pair_second(X95)|X95!=ordered_pair(X90,X91)|X94=X91,inference(split_conjunct,[status(thm)],[c11])).
% 0.84/1.02 cnf(c125,plain,X222!=ordered_pair(X221,X223)|X220!=pair_second(X222)|X220=X223,inference(factor,[status(thm)],[c12])).
% 0.84/1.02 cnf(c586,plain,X224!=pair_second(ordered_pair(X225,X226))|X224=X226,inference(resolution,[status(thm)],[c125, reflexivity])).
% 0.84/1.02 cnf(c591,plain,pair_second(ordered_pair(X227,X228))=X228,inference(resolution,[status(thm)],[c586, reflexivity])).
% 0.84/1.02 cnf(c610,plain,pair_first(ordered_pair(skolem0005,skolem0006))!=skolem0005,inference(resolution,[status(thm)],[c591, c29])).
% 0.84/1.02 fof(d1_mcart_1,axiom,(![A]:((?[B]:(?[C]:A=ordered_pair(B,C)))=>(![B]:(B=pair_first(A)<=>(![C]:(![D]:(A=ordered_pair(C,D)=>B=C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_mcart_1)).
% 0.84/1.02 fof(c15,plain,(![A]:((![B]:(![C]:A!=ordered_pair(B,C)))|(![B]:((B!=pair_first(A)|(![C]:(![D]:(A!=ordered_pair(C,D)|B=C))))&((?[C]:(?[D]:(A=ordered_pair(C,D)&B!=C)))|B=pair_first(A)))))),inference(fof_nnf,[status(thm)],[d1_mcart_1])).
% 0.84/1.02 fof(c16,plain,(![A]:((![B]:(![C]:A!=ordered_pair(B,C)))|((![B]:(B!=pair_first(A)|(![C]:((![D]:A!=ordered_pair(C,D))|B=C))))&(![B]:((?[C]:((?[D]:A=ordered_pair(C,D))&B!=C))|B=pair_first(A)))))),inference(shift_quantors,[status(thm)],[c15])).
% 0.84/1.02 fof(c17,plain,(![X11]:((![X12]:(![X13]:X11!=ordered_pair(X12,X13)))|((![X14]:(X14!=pair_first(X11)|(![X15]:((![X16]:X11!=ordered_pair(X15,X16))|X14=X15))))&(![X17]:((?[X18]:((?[X19]:X11=ordered_pair(X18,X19))&X17!=X18))|X17=pair_first(X11)))))),inference(variable_rename,[status(thm)],[c16])).
% 0.84/1.02 fof(c19,plain,(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(X11!=ordered_pair(X12,X13)|((X14!=pair_first(X11)|(X11!=ordered_pair(X15,X16)|X14=X15))&((X11=ordered_pair(skolem0003(X11,X17),skolem0004(X11,X17))&X17!=skolem0003(X11,X17))|X17=pair_first(X11))))))))))),inference(shift_quantors,[status(thm)],[fof(c18,plain,(![X11]:((![X12]:(![X13]:X11!=ordered_pair(X12,X13)))|((![X14]:(X14!=pair_first(X11)|(![X15]:((![X16]:X11!=ordered_pair(X15,X16))|X14=X15))))&(![X17]:((X11=ordered_pair(skolem0003(X11,X17),skolem0004(X11,X17))&X17!=skolem0003(X11,X17))|X17=pair_first(X11)))))),inference(skolemize,[status(esa)],[c17])).])).
% 0.84/1.02 fof(c20,plain,(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:((X11!=ordered_pair(X12,X13)|(X14!=pair_first(X11)|(X11!=ordered_pair(X15,X16)|X14=X15)))&((X11!=ordered_pair(X12,X13)|(X11=ordered_pair(skolem0003(X11,X17),skolem0004(X11,X17))|X17=pair_first(X11)))&(X11!=ordered_pair(X12,X13)|(X17!=skolem0003(X11,X17)|X17=pair_first(X11)))))))))))),inference(distribute,[status(thm)],[c19])).
% 0.84/1.02 cnf(c21,plain,X113!=ordered_pair(X115,X114)|X117!=pair_first(X113)|X113!=ordered_pair(X118,X116)|X117=X118,inference(split_conjunct,[status(thm)],[c20])).
% 0.84/1.02 cnf(c164,plain,X338!=ordered_pair(X336,X337)|X339!=pair_first(X338)|X339=X336,inference(factor,[status(thm)],[c21])).
% 0.84/1.02 cnf(c1208,plain,X376!=pair_first(ordered_pair(X377,X378))|X376=X377,inference(resolution,[status(thm)],[c164, reflexivity])).
% 0.84/1.02 cnf(c1239,plain,pair_first(ordered_pair(X380,X379))=X380,inference(resolution,[status(thm)],[c1208, reflexivity])).
% 0.84/1.02 cnf(c1253,plain,$false,inference(resolution,[status(thm)],[c1239, c610])).
% 0.84/1.02 % SZS output end CNFRefutation
% 0.84/1.02
% 0.84/1.02 % Initial clauses : 32
% 0.84/1.02 % Processed clauses : 156
% 0.84/1.02 % Factors computed : 6
% 0.84/1.02 % Resolvents computed: 1240
% 0.84/1.02 % Tautologies deleted: 4
% 0.84/1.02 % Forward subsumed : 146
% 0.84/1.02 % Backward subsumed : 4
% 0.84/1.02 % -------- CPU Time ---------
% 0.84/1.02 % User time : 0.623 s
% 0.84/1.02 % System time : 0.026 s
% 0.84/1.02 % Total time : 0.649 s
%------------------------------------------------------------------------------