%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LAT382+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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:30:11 EDT 2024
% Result : Theorem 0.59s 0.76s
% Output : Refutation 0.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : LAT382+3 : TPTP v8.1.2. Released v4.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.32 % Computer : n023.cluster.edu
% 0.13/0.32 % Model : x86_64 x86_64
% 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32 % Memory : 8042.1875MB
% 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32 % CPULimit : 300
% 0.13/0.32 % WCLimit : 300
% 0.13/0.32 % DateTime : Wed May 8 12:43:53 EDT 2024
% 0.13/0.32 % CPUTime :
% 0.59/0.76 % Version: 1.5
% 0.59/0.76 % SZS status Theorem
% 0.59/0.76 % SZS output start CNFRefutation
% 0.59/0.76 fof(m__,conjecture,xu=xv,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__)).
% 0.59/0.76 fof(c10,negated_conjecture,(~xu=xv),inference(assume_negation,[status(cth)],[m__])).
% 0.59/0.76 fof(c11,negated_conjecture,xu!=xv,inference(fof_simplification,[status(thm)],[c10])).
% 0.59/0.76 cnf(c12,negated_conjecture,xu!=xv,inference(split_conjunct,[status(thm)],[c11])).
% 0.59/0.76 cnf(symmetry,axiom,X55!=X54|X54=X55,theory(equality)).
% 0.59/0.76 fof(m__773,plain,aSet0(xT),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__773)).
% 0.59/0.76 cnf(c40,plain,aSet0(xT),inference(split_conjunct,[status(thm)],[m__773])).
% 0.59/0.76 fof(m__792,plain,(((((((((((aElementOf0(xu,xT)&aElementOf0(xu,xT))&(![W0]:(aElementOf0(W0,xS)=>sdtlseqdt0(xu,W0))))&aLowerBoundOfIn0(xu,xS,xT))&(![W0]:(((aElementOf0(W0,xT)&(![W1]:(aElementOf0(W1,xS)=>sdtlseqdt0(W0,W1))))|aLowerBoundOfIn0(W0,xS,xT))=>sdtlseqdt0(W0,xu))))&aInfimumOfIn0(xu,xS,xT))&aElementOf0(xv,xT))&aElementOf0(xv,xT))&(![W0]:(aElementOf0(W0,xS)=>sdtlseqdt0(xv,W0))))&aLowerBoundOfIn0(xv,xS,xT))&(![W0]:(((aElementOf0(W0,xT)&(![W1]:(aElementOf0(W1,xS)=>sdtlseqdt0(W0,W1))))|aLowerBoundOfIn0(W0,xS,xT))=>sdtlseqdt0(W0,xv))))&aInfimumOfIn0(xv,xS,xT)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__792)).
% 0.59/0.76 fof(c13,plain,((((((((((aElementOf0(xu,xT)&(![W0]:(aElementOf0(W0,xS)=>sdtlseqdt0(xu,W0))))&aLowerBoundOfIn0(xu,xS,xT))&(![W0]:(((aElementOf0(W0,xT)&(![W1]:(aElementOf0(W1,xS)=>sdtlseqdt0(W0,W1))))|aLowerBoundOfIn0(W0,xS,xT))=>sdtlseqdt0(W0,xu))))&aInfimumOfIn0(xu,xS,xT))&aElementOf0(xv,xT))&aElementOf0(xv,xT))&(![W0]:(aElementOf0(W0,xS)=>sdtlseqdt0(xv,W0))))&aLowerBoundOfIn0(xv,xS,xT))&(![W0]:(((aElementOf0(W0,xT)&(![W1]:(aElementOf0(W1,xS)=>sdtlseqdt0(W0,W1))))|aLowerBoundOfIn0(W0,xS,xT))=>sdtlseqdt0(W0,xv))))&aInfimumOfIn0(xv,xS,xT)),inference(fof_simplification,[status(thm)],[m__792])).
% 0.59/0.76 fof(c14,plain,((((((((((aElementOf0(xu,xT)&(![W0]:(~aElementOf0(W0,xS)|sdtlseqdt0(xu,W0))))&aLowerBoundOfIn0(xu,xS,xT))&(![W0]:(((~aElementOf0(W0,xT)|(?[W1]:(aElementOf0(W1,xS)&~sdtlseqdt0(W0,W1))))&~aLowerBoundOfIn0(W0,xS,xT))|sdtlseqdt0(W0,xu))))&aInfimumOfIn0(xu,xS,xT))&aElementOf0(xv,xT))&aElementOf0(xv,xT))&(![W0]:(~aElementOf0(W0,xS)|sdtlseqdt0(xv,W0))))&aLowerBoundOfIn0(xv,xS,xT))&(![W0]:(((~aElementOf0(W0,xT)|(?[W1]:(aElementOf0(W1,xS)&~sdtlseqdt0(W0,W1))))&~aLowerBoundOfIn0(W0,xS,xT))|sdtlseqdt0(W0,xv))))&aInfimumOfIn0(xv,xS,xT)),inference(fof_nnf,[status(thm)],[c13])).
% 0.59/0.76 fof(c15,plain,((((((((((aElementOf0(xu,xT)&(![X2]:(~aElementOf0(X2,xS)|sdtlseqdt0(xu,X2))))&aLowerBoundOfIn0(xu,xS,xT))&(![X3]:(((~aElementOf0(X3,xT)|(?[X4]:(aElementOf0(X4,xS)&~sdtlseqdt0(X3,X4))))&~aLowerBoundOfIn0(X3,xS,xT))|sdtlseqdt0(X3,xu))))&aInfimumOfIn0(xu,xS,xT))&aElementOf0(xv,xT))&aElementOf0(xv,xT))&(![X5]:(~aElementOf0(X5,xS)|sdtlseqdt0(xv,X5))))&aLowerBoundOfIn0(xv,xS,xT))&(![X6]:(((~aElementOf0(X6,xT)|(?[X7]:(aElementOf0(X7,xS)&~sdtlseqdt0(X6,X7))))&~aLowerBoundOfIn0(X6,xS,xT))|sdtlseqdt0(X6,xv))))&aInfimumOfIn0(xv,xS,xT)),inference(variable_rename,[status(thm)],[c14])).
% 0.59/0.76 fof(c17,plain,(![X2]:(![X3]:(![X5]:(![X6]:((((((((((aElementOf0(xu,xT)&(~aElementOf0(X2,xS)|sdtlseqdt0(xu,X2)))&aLowerBoundOfIn0(xu,xS,xT))&(((~aElementOf0(X3,xT)|(aElementOf0(skolem0001(X3),xS)&~sdtlseqdt0(X3,skolem0001(X3))))&~aLowerBoundOfIn0(X3,xS,xT))|sdtlseqdt0(X3,xu)))&aInfimumOfIn0(xu,xS,xT))&aElementOf0(xv,xT))&aElementOf0(xv,xT))&(~aElementOf0(X5,xS)|sdtlseqdt0(xv,X5)))&aLowerBoundOfIn0(xv,xS,xT))&(((~aElementOf0(X6,xT)|(aElementOf0(skolem0002(X6),xS)&~sdtlseqdt0(X6,skolem0002(X6))))&~aLowerBoundOfIn0(X6,xS,xT))|sdtlseqdt0(X6,xv)))&aInfimumOfIn0(xv,xS,xT)))))),inference(shift_quantors,[status(thm)],[fof(c16,plain,((((((((((aElementOf0(xu,xT)&(![X2]:(~aElementOf0(X2,xS)|sdtlseqdt0(xu,X2))))&aLowerBoundOfIn0(xu,xS,xT))&(![X3]:(((~aElementOf0(X3,xT)|(aElementOf0(skolem0001(X3),xS)&~sdtlseqdt0(X3,skolem0001(X3))))&~aLowerBoundOfIn0(X3,xS,xT))|sdtlseqdt0(X3,xu))))&aInfimumOfIn0(xu,xS,xT))&aElementOf0(xv,xT))&aElementOf0(xv,xT))&(![X5]:(~aElementOf0(X5,xS)|sdtlseqdt0(xv,X5))))&aLowerBoundOfIn0(xv,xS,xT))&(![X6]:(((~aElementOf0(X6,xT)|(aElementOf0(skolem0002(X6),xS)&~sdtlseqdt0(X6,skolem0002(X6))))&~aLowerBoundOfIn0(X6,xS,xT))|sdtlseqdt0(X6,xv))))&aInfimumOfIn0(xv,xS,xT)),inference(skolemize,[status(esa)],[c15])).])).
% 0.59/0.76 fof(c18,plain,(![X2]:(![X3]:(![X5]:(![X6]:((((((((((aElementOf0(xu,xT)&(~aElementOf0(X2,xS)|sdtlseqdt0(xu,X2)))&aLowerBoundOfIn0(xu,xS,xT))&((((~aElementOf0(X3,xT)|aElementOf0(skolem0001(X3),xS))|sdtlseqdt0(X3,xu))&((~aElementOf0(X3,xT)|~sdtlseqdt0(X3,skolem0001(X3)))|sdtlseqdt0(X3,xu)))&(~aLowerBoundOfIn0(X3,xS,xT)|sdtlseqdt0(X3,xu))))&aInfimumOfIn0(xu,xS,xT))&aElementOf0(xv,xT))&aElementOf0(xv,xT))&(~aElementOf0(X5,xS)|sdtlseqdt0(xv,X5)))&aLowerBoundOfIn0(xv,xS,xT))&((((~aElementOf0(X6,xT)|aElementOf0(skolem0002(X6),xS))|sdtlseqdt0(X6,xv))&((~aElementOf0(X6,xT)|~sdtlseqdt0(X6,skolem0002(X6)))|sdtlseqdt0(X6,xv)))&(~aLowerBoundOfIn0(X6,xS,xT)|sdtlseqdt0(X6,xv))))&aInfimumOfIn0(xv,xS,xT)))))),inference(distribute,[status(thm)],[c17])).
% 0.59/0.76 cnf(c26,plain,aElementOf0(xv,xT),inference(split_conjunct,[status(thm)],[c18])).
% 0.59/0.76 fof(mEOfElem,axiom,(![W0]:(aSet0(W0)=>(![W1]:(aElementOf0(W1,W0)=>aElement0(W1))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mEOfElem)).
% 0.59/0.76 fof(c115,plain,(![W0]:(~aSet0(W0)|(![W1]:(~aElementOf0(W1,W0)|aElement0(W1))))),inference(fof_nnf,[status(thm)],[mEOfElem])).
% 0.59/0.76 fof(c117,plain,(![X51]:(![X52]:(~aSet0(X51)|(~aElementOf0(X52,X51)|aElement0(X52))))),inference(shift_quantors,[status(thm)],[fof(c116,plain,(![X51]:(~aSet0(X51)|(![X52]:(~aElementOf0(X52,X51)|aElement0(X52))))),inference(variable_rename,[status(thm)],[c115])).])).
% 0.59/0.76 cnf(c118,plain,~aSet0(X89)|~aElementOf0(X88,X89)|aElement0(X88),inference(split_conjunct,[status(thm)],[c117])).
% 0.59/0.76 cnf(c136,plain,~aSet0(xT)|aElement0(xv),inference(resolution,[status(thm)],[c118, c26])).
% 0.59/0.76 cnf(c140,plain,aElement0(xv),inference(resolution,[status(thm)],[c136, c40])).
% 0.59/0.76 cnf(c19,plain,aElementOf0(xu,xT),inference(split_conjunct,[status(thm)],[c18])).
% 0.59/0.76 cnf(c135,plain,~aSet0(xT)|aElement0(xu),inference(resolution,[status(thm)],[c118, c19])).
% 0.59/0.76 cnf(c137,plain,aElement0(xu),inference(resolution,[status(thm)],[c135, c40])).
% 0.59/0.76 cnf(c29,plain,aLowerBoundOfIn0(xv,xS,xT),inference(split_conjunct,[status(thm)],[c18])).
% 0.59/0.76 cnf(c24,plain,~aLowerBoundOfIn0(X94,xS,xT)|sdtlseqdt0(X94,xu),inference(split_conjunct,[status(thm)],[c18])).
% 0.59/0.76 cnf(c143,plain,sdtlseqdt0(xv,xu),inference(resolution,[status(thm)],[c24, c29])).
% 0.59/0.76 cnf(c21,plain,aLowerBoundOfIn0(xu,xS,xT),inference(split_conjunct,[status(thm)],[c18])).
% 0.59/0.76 cnf(c32,plain,~aLowerBoundOfIn0(X101,xS,xT)|sdtlseqdt0(X101,xv),inference(split_conjunct,[status(thm)],[c18])).
% 0.59/0.76 cnf(c149,plain,sdtlseqdt0(xu,xv),inference(resolution,[status(thm)],[c32, c21])).
% 0.59/0.76 fof(mASymm,axiom,(![W0]:(![W1]:((aElement0(W0)&aElement0(W1))=>((sdtlseqdt0(W0,W1)&sdtlseqdt0(W1,W0))=>W0=W1)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mASymm)).
% 0.59/0.76 fof(c90,plain,(![W0]:(![W1]:((~aElement0(W0)|~aElement0(W1))|((~sdtlseqdt0(W0,W1)|~sdtlseqdt0(W1,W0))|W0=W1)))),inference(fof_nnf,[status(thm)],[mASymm])).
% 0.59/0.76 fof(c91,plain,(![X40]:(![X41]:((~aElement0(X40)|~aElement0(X41))|((~sdtlseqdt0(X40,X41)|~sdtlseqdt0(X41,X40))|X40=X41)))),inference(variable_rename,[status(thm)],[c90])).
% 0.59/0.76 cnf(c92,plain,~aElement0(X237)|~aElement0(X238)|~sdtlseqdt0(X237,X238)|~sdtlseqdt0(X238,X237)|X237=X238,inference(split_conjunct,[status(thm)],[c91])).
% 0.59/0.76 cnf(c329,plain,~aElement0(xv)|~aElement0(xu)|~sdtlseqdt0(xv,xu)|xv=xu,inference(resolution,[status(thm)],[c92, c149])).
% 0.59/0.76 cnf(c599,plain,~aElement0(xv)|~aElement0(xu)|xv=xu,inference(resolution,[status(thm)],[c329, c143])).
% 0.59/0.76 cnf(c600,plain,~aElement0(xv)|xv=xu,inference(resolution,[status(thm)],[c599, c137])).
% 0.59/0.76 cnf(c601,plain,xv=xu,inference(resolution,[status(thm)],[c600, c140])).
% 0.59/0.76 cnf(c610,plain,xu=xv,inference(resolution,[status(thm)],[c601, symmetry])).
% 0.59/0.76 cnf(c623,plain,$false,inference(resolution,[status(thm)],[c610, c12])).
% 0.59/0.76 % SZS output end CNFRefutation
% 0.59/0.76
% 0.59/0.76 % Initial clauses : 65
% 0.59/0.76 % Processed clauses : 196
% 0.59/0.76 % Factors computed : 11
% 0.59/0.76 % Resolvents computed: 497
% 0.59/0.76 % Tautologies deleted: 19
% 0.59/0.76 % Forward subsumed : 119
% 0.59/0.76 % Backward subsumed : 28
% 0.59/0.76 % -------- CPU Time ---------
% 0.59/0.76 % User time : 0.418 s
% 0.59/0.76 % System time : 0.017 s
% 0.59/0.76 % Total time : 0.435 s
%------------------------------------------------------------------------------