%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LAT382+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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.65s 0.86s
% Output : Refutation 0.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : LAT382+1 : TPTP v8.1.2. Released v4.0.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n004.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 12:17:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.65/0.86 % Version: 1.5
% 0.65/0.86 % SZS status Theorem
% 0.65/0.86 % SZS output start CNFRefutation
% 0.65/0.86 fof(m__,conjecture,xu=xv,file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 0.65/0.86 fof(c10,negated_conjecture,(~xu=xv),inference(assume_negation,[status(cth)],[m__])).
% 0.65/0.86 fof(c11,negated_conjecture,xu!=xv,inference(fof_simplification,[status(thm)],[c10])).
% 0.65/0.86 cnf(c12,negated_conjecture,xu!=xv,inference(split_conjunct,[status(thm)],[c11])).
% 0.65/0.86 cnf(symmetry,axiom,X48!=X47|X47=X48,theory(equality)).
% 0.65/0.86 fof(m__773,plain,aSet0(xT),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__773)).
% 0.65/0.86 cnf(c16,plain,aSet0(xT),inference(split_conjunct,[status(thm)],[m__773])).
% 0.65/0.86 fof(mEOfElem,axiom,(![W0]:(aSet0(W0)=>(![W1]:(aElementOf0(W1,W0)=>aElement0(W1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mEOfElem)).
% 0.65/0.86 fof(c91,plain,(![W0]:(~aSet0(W0)|(![W1]:(~aElementOf0(W1,W0)|aElement0(W1))))),inference(fof_nnf,[status(thm)],[mEOfElem])).
% 0.65/0.86 fof(c93,plain,(![X44]:(![X45]:(~aSet0(X44)|(~aElementOf0(X45,X44)|aElement0(X45))))),inference(shift_quantors,[status(thm)],[fof(c92,plain,(![X44]:(~aSet0(X44)|(![X45]:(~aElementOf0(X45,X44)|aElement0(X45))))),inference(variable_rename,[status(thm)],[c91])).])).
% 0.65/0.86 cnf(c94,plain,~aSet0(X75)|~aElementOf0(X74,X75)|aElement0(X74),inference(split_conjunct,[status(thm)],[c93])).
% 0.65/0.86 fof(m__773_01,plain,aSubsetOf0(xS,xT),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__773_01)).
% 0.65/0.86 cnf(c15,plain,aSubsetOf0(xS,xT),inference(split_conjunct,[status(thm)],[m__773_01])).
% 0.65/0.86 fof(m__792,plain,(aInfimumOfIn0(xu,xS,xT)&aInfimumOfIn0(xv,xS,xT)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__792)).
% 0.65/0.86 cnf(c14,plain,aInfimumOfIn0(xv,xS,xT),inference(split_conjunct,[status(thm)],[m__792])).
% 0.65/0.86 fof(mDefInf,plain,(![W0]:(aSet0(W0)=>(![W1]:(aSubsetOf0(W1,W0)=>(![W2]:(aInfimumOfIn0(W2,W1,W0)<=>((aElementOf0(W2,W0)&aLowerBoundOfIn0(W2,W1,W0))&(![W3]:(aLowerBoundOfIn0(W3,W1,W0)=>sdtlseqdt0(W3,W2)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mDefInf)).
% 0.65/0.86 fof(c32,plain,(![W0]:(~aSet0(W0)|(![W1]:(~aSubsetOf0(W1,W0)|(![W2]:((~aInfimumOfIn0(W2,W1,W0)|((aElementOf0(W2,W0)&aLowerBoundOfIn0(W2,W1,W0))&(![W3]:(~aLowerBoundOfIn0(W3,W1,W0)|sdtlseqdt0(W3,W2)))))&(((~aElementOf0(W2,W0)|~aLowerBoundOfIn0(W2,W1,W0))|(?[W3]:(aLowerBoundOfIn0(W3,W1,W0)&~sdtlseqdt0(W3,W2))))|aInfimumOfIn0(W2,W1,W0)))))))),inference(fof_nnf,[status(thm)],[mDefInf])).
% 0.65/0.86 fof(c33,plain,(![W0]:(~aSet0(W0)|(![W1]:(~aSubsetOf0(W1,W0)|((![W2]:(~aInfimumOfIn0(W2,W1,W0)|((aElementOf0(W2,W0)&aLowerBoundOfIn0(W2,W1,W0))&(![W3]:(~aLowerBoundOfIn0(W3,W1,W0)|sdtlseqdt0(W3,W2))))))&(![W2]:(((~aElementOf0(W2,W0)|~aLowerBoundOfIn0(W2,W1,W0))|(?[W3]:(aLowerBoundOfIn0(W3,W1,W0)&~sdtlseqdt0(W3,W2))))|aInfimumOfIn0(W2,W1,W0)))))))),inference(shift_quantors,[status(thm)],[c32])).
% 0.65/0.86 fof(c34,plain,(![X12]:(~aSet0(X12)|(![X13]:(~aSubsetOf0(X13,X12)|((![X14]:(~aInfimumOfIn0(X14,X13,X12)|((aElementOf0(X14,X12)&aLowerBoundOfIn0(X14,X13,X12))&(![X15]:(~aLowerBoundOfIn0(X15,X13,X12)|sdtlseqdt0(X15,X14))))))&(![X16]:(((~aElementOf0(X16,X12)|~aLowerBoundOfIn0(X16,X13,X12))|(?[X17]:(aLowerBoundOfIn0(X17,X13,X12)&~sdtlseqdt0(X17,X16))))|aInfimumOfIn0(X16,X13,X12)))))))),inference(variable_rename,[status(thm)],[c33])).
% 0.65/0.86 fof(c36,plain,(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(~aSet0(X12)|(~aSubsetOf0(X13,X12)|((~aInfimumOfIn0(X14,X13,X12)|((aElementOf0(X14,X12)&aLowerBoundOfIn0(X14,X13,X12))&(~aLowerBoundOfIn0(X15,X13,X12)|sdtlseqdt0(X15,X14))))&(((~aElementOf0(X16,X12)|~aLowerBoundOfIn0(X16,X13,X12))|(aLowerBoundOfIn0(skolem0002(X12,X13,X16),X13,X12)&~sdtlseqdt0(skolem0002(X12,X13,X16),X16)))|aInfimumOfIn0(X16,X13,X12)))))))))),inference(shift_quantors,[status(thm)],[fof(c35,plain,(![X12]:(~aSet0(X12)|(![X13]:(~aSubsetOf0(X13,X12)|((![X14]:(~aInfimumOfIn0(X14,X13,X12)|((aElementOf0(X14,X12)&aLowerBoundOfIn0(X14,X13,X12))&(![X15]:(~aLowerBoundOfIn0(X15,X13,X12)|sdtlseqdt0(X15,X14))))))&(![X16]:(((~aElementOf0(X16,X12)|~aLowerBoundOfIn0(X16,X13,X12))|(aLowerBoundOfIn0(skolem0002(X12,X13,X16),X13,X12)&~sdtlseqdt0(skolem0002(X12,X13,X16),X16)))|aInfimumOfIn0(X16,X13,X12)))))))),inference(skolemize,[status(esa)],[c34])).])).
% 0.65/0.86 fof(c37,plain,(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:((((~aSet0(X12)|(~aSubsetOf0(X13,X12)|(~aInfimumOfIn0(X14,X13,X12)|aElementOf0(X14,X12))))&(~aSet0(X12)|(~aSubsetOf0(X13,X12)|(~aInfimumOfIn0(X14,X13,X12)|aLowerBoundOfIn0(X14,X13,X12)))))&(~aSet0(X12)|(~aSubsetOf0(X13,X12)|(~aInfimumOfIn0(X14,X13,X12)|(~aLowerBoundOfIn0(X15,X13,X12)|sdtlseqdt0(X15,X14))))))&((~aSet0(X12)|(~aSubsetOf0(X13,X12)|(((~aElementOf0(X16,X12)|~aLowerBoundOfIn0(X16,X13,X12))|aLowerBoundOfIn0(skolem0002(X12,X13,X16),X13,X12))|aInfimumOfIn0(X16,X13,X12))))&(~aSet0(X12)|(~aSubsetOf0(X13,X12)|(((~aElementOf0(X16,X12)|~aLowerBoundOfIn0(X16,X13,X12))|~sdtlseqdt0(skolem0002(X12,X13,X16),X16))|aInfimumOfIn0(X16,X13,X12))))))))))),inference(distribute,[status(thm)],[c36])).
% 0.65/0.86 cnf(c38,plain,~aSet0(X101)|~aSubsetOf0(X102,X101)|~aInfimumOfIn0(X100,X102,X101)|aElementOf0(X100,X101),inference(split_conjunct,[status(thm)],[c37])).
% 0.65/0.86 cnf(c127,plain,~aSet0(xT)|~aSubsetOf0(xS,xT)|aElementOf0(xv,xT),inference(resolution,[status(thm)],[c38, c14])).
% 0.65/0.86 cnf(c157,plain,~aSet0(xT)|aElementOf0(xv,xT),inference(resolution,[status(thm)],[c127, c15])).
% 0.65/0.86 cnf(c158,plain,aElementOf0(xv,xT),inference(resolution,[status(thm)],[c157, c16])).
% 0.65/0.86 cnf(c161,plain,~aSet0(xT)|aElement0(xv),inference(resolution,[status(thm)],[c158, c94])).
% 0.65/0.86 cnf(c163,plain,aElement0(xv),inference(resolution,[status(thm)],[c161, c16])).
% 0.65/0.86 cnf(c13,plain,aInfimumOfIn0(xu,xS,xT),inference(split_conjunct,[status(thm)],[m__792])).
% 0.65/0.86 cnf(c126,plain,~aSet0(xT)|~aSubsetOf0(xS,xT)|aElementOf0(xu,xT),inference(resolution,[status(thm)],[c38, c13])).
% 0.65/0.86 cnf(c128,plain,~aSet0(xT)|aElementOf0(xu,xT),inference(resolution,[status(thm)],[c126, c15])).
% 0.65/0.86 cnf(c129,plain,aElementOf0(xu,xT),inference(resolution,[status(thm)],[c128, c16])).
% 0.65/0.86 cnf(c132,plain,~aSet0(xT)|aElement0(xu),inference(resolution,[status(thm)],[c129, c94])).
% 0.65/0.86 cnf(c136,plain,aElement0(xu),inference(resolution,[status(thm)],[c132, c16])).
% 0.65/0.86 fof(mASymm,axiom,(![W0]:(![W1]:((aElement0(W0)&aElement0(W1))=>((sdtlseqdt0(W0,W1)&sdtlseqdt0(W1,W0))=>W0=W1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mASymm)).
% 0.65/0.86 fof(c66,plain,(![W0]:(![W1]:((~aElement0(W0)|~aElement0(W1))|((~sdtlseqdt0(W0,W1)|~sdtlseqdt0(W1,W0))|W0=W1)))),inference(fof_nnf,[status(thm)],[mASymm])).
% 0.65/0.86 fof(c67,plain,(![X33]:(![X34]:((~aElement0(X33)|~aElement0(X34))|((~sdtlseqdt0(X33,X34)|~sdtlseqdt0(X34,X33))|X33=X34)))),inference(variable_rename,[status(thm)],[c66])).
% 0.65/0.86 cnf(c68,plain,~aElement0(X213)|~aElement0(X212)|~sdtlseqdt0(X213,X212)|~sdtlseqdt0(X212,X213)|X213=X212,inference(split_conjunct,[status(thm)],[c67])).
% 0.65/0.86 cnf(c40,plain,~aSet0(X168)|~aSubsetOf0(X170,X168)|~aInfimumOfIn0(X167,X170,X168)|~aLowerBoundOfIn0(X169,X170,X168)|sdtlseqdt0(X169,X167),inference(split_conjunct,[status(thm)],[c37])).
% 0.65/0.86 cnf(c39,plain,~aSet0(X161)|~aSubsetOf0(X162,X161)|~aInfimumOfIn0(X160,X162,X161)|aLowerBoundOfIn0(X160,X162,X161),inference(split_conjunct,[status(thm)],[c37])).
% 0.65/0.86 cnf(c171,plain,~aSet0(xT)|~aSubsetOf0(xS,xT)|aLowerBoundOfIn0(xu,xS,xT),inference(resolution,[status(thm)],[c39, c13])).
% 0.65/0.86 cnf(c264,plain,~aSet0(xT)|aLowerBoundOfIn0(xu,xS,xT),inference(resolution,[status(thm)],[c171, c15])).
% 0.65/0.86 cnf(c265,plain,aLowerBoundOfIn0(xu,xS,xT),inference(resolution,[status(thm)],[c264, c16])).
% 0.65/0.86 cnf(c266,plain,~aSet0(xT)|~aSubsetOf0(xS,xT)|~aInfimumOfIn0(X295,xS,xT)|sdtlseqdt0(xu,X295),inference(resolution,[status(thm)],[c265, c40])).
% 0.65/0.86 cnf(c496,plain,~aSet0(xT)|~aSubsetOf0(xS,xT)|sdtlseqdt0(xu,xv),inference(resolution,[status(thm)],[c266, c14])).
% 0.65/0.86 cnf(c497,plain,~aSet0(xT)|sdtlseqdt0(xu,xv),inference(resolution,[status(thm)],[c496, c15])).
% 0.65/0.86 cnf(c502,plain,sdtlseqdt0(xu,xv),inference(resolution,[status(thm)],[c497, c16])).
% 0.65/0.86 cnf(c504,plain,~aElement0(xv)|~aElement0(xu)|~sdtlseqdt0(xv,xu)|xv=xu,inference(resolution,[status(thm)],[c502, c68])).
% 0.65/0.86 cnf(c172,plain,~aSet0(xT)|~aSubsetOf0(xS,xT)|aLowerBoundOfIn0(xv,xS,xT),inference(resolution,[status(thm)],[c39, c14])).
% 0.65/0.86 cnf(c271,plain,~aSet0(xT)|aLowerBoundOfIn0(xv,xS,xT),inference(resolution,[status(thm)],[c172, c15])).
% 0.65/0.86 cnf(c272,plain,aLowerBoundOfIn0(xv,xS,xT),inference(resolution,[status(thm)],[c271, c16])).
% 0.65/0.86 cnf(c273,plain,~aSet0(xT)|~aSubsetOf0(xS,xT)|~aInfimumOfIn0(X302,xS,xT)|sdtlseqdt0(xv,X302),inference(resolution,[status(thm)],[c272, c40])).
% 0.65/0.86 cnf(c511,plain,~aSet0(xT)|~aSubsetOf0(xS,xT)|sdtlseqdt0(xv,xu),inference(resolution,[status(thm)],[c273, c13])).
% 0.65/0.86 cnf(c513,plain,~aSet0(xT)|sdtlseqdt0(xv,xu),inference(resolution,[status(thm)],[c511, c15])).
% 0.65/0.86 cnf(c516,plain,sdtlseqdt0(xv,xu),inference(resolution,[status(thm)],[c513, c16])).
% 0.65/0.86 cnf(c519,plain,~aElement0(xv)|~aElement0(xu)|xv=xu,inference(resolution,[status(thm)],[c516, c504])).
% 0.65/0.86 cnf(c522,plain,~aElement0(xv)|xv=xu,inference(resolution,[status(thm)],[c519, c136])).
% 0.65/0.86 cnf(c523,plain,xv=xu,inference(resolution,[status(thm)],[c522, c163])).
% 0.65/0.86 cnf(c529,plain,xu=xv,inference(resolution,[status(thm)],[c523, symmetry])).
% 0.65/0.86 cnf(c544,plain,$false,inference(resolution,[status(thm)],[c529, c12])).
% 0.65/0.86 % SZS output end CNFRefutation
% 0.65/0.86
% 0.65/0.86 % Initial clauses : 50
% 0.65/0.86 % Processed clauses : 205
% 0.65/0.86 % Factors computed : 11
% 0.65/0.86 % Resolvents computed: 443
% 0.65/0.86 % Tautologies deleted: 16
% 0.65/0.86 % Forward subsumed : 100
% 0.65/0.86 % Backward subsumed : 45
% 0.65/0.86 % -------- CPU Time ---------
% 0.65/0.86 % User time : 0.466 s
% 0.65/0.86 % System time : 0.023 s
% 0.65/0.86 % Total time : 0.489 s
%------------------------------------------------------------------------------