%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM449+6 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:24:30 PM UTC 2026
% Result : Theorem 1.44s 1.77s
% Output : CNFRefutation 1.44s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f110ERROR: Could not build tree for root c_34370ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aInteger0(sz00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIntZero) ).
fof(f15,axiom,
! [X0] :
( aInteger0(X0)
=> ( sz00 = sdtasdt0(sz00,X0)
& sdtasdt0(X0,sz00) = sz00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulZero) ).
fof(f40,axiom,
! [X0] :
( ( ! [X1] :
( aElementOf0(X1,X0)
=> ( isClosed0(X1)
& aSubsetOf0(X1,cS1395) ) )
& isFinite0(X0)
& aSet0(X0) )
=> isClosed0(sbsmnsldt0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mUnionSClosed) ).
fof(f41,axiom,
! [X0,X1] :
( ( X1 != sz00
& aInteger0(X1)
& aInteger0(X0) )
=> ( isClosed0(szAzrzSzezqlpdtcmdtrp0(X0,X1))
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),cS1395) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mArSeqClosed) ).
fof(f44,axiom,
isFinite0(xS),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2117) ).
fof(f45,conjecture,
( ( ! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
<=> ( ? [X1] :
( aElementOf0(X0,X1)
& aElementOf0(X1,xS) )
& aInteger0(X0) ) )
& aSet0(sbsmnsldt0(xS)) )
=> ( isClosed0(sbsmnsldt0(xS))
| ( ! [X0] :
( aElementOf0(X0,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(X0,sbsmnsldt0(xS))
& aInteger0(X0) ) )
=> ( isOpen0(stldt0(sbsmnsldt0(xS)))
| ! [X0] :
( aElementOf0(X0,stldt0(sbsmnsldt0(xS)))
=> ? [X1] :
( ( ( ! [X2] :
( ( ( ( sdteqdtlpzmzozddtrp0(X2,X0,X1)
| aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0)))
| ? [X3] :
( sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0))
& aInteger0(X3) ) )
& aInteger0(X2) )
=> aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)) )
& ( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
=> ( sdteqdtlpzmzozddtrp0(X2,X0,X1)
& aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0)))
& ? [X3] :
( sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0))
& aInteger0(X3) )
& aInteger0(X2) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(X0,X1)) )
=> ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),stldt0(sbsmnsldt0(xS)))
| ! [X2] :
( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
=> aElementOf0(X2,stldt0(sbsmnsldt0(xS))) ) ) )
& X1 != sz00
& aInteger0(X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f46,negated_conjecture,
~ ( ( ! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
<=> ( ? [X1] :
( aElementOf0(X0,X1)
& aElementOf0(X1,xS) )
& aInteger0(X0) ) )
& aSet0(sbsmnsldt0(xS)) )
=> ( isClosed0(sbsmnsldt0(xS))
| ( ! [X0] :
( aElementOf0(X0,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(X0,sbsmnsldt0(xS))
& aInteger0(X0) ) )
=> ( isOpen0(stldt0(sbsmnsldt0(xS)))
| ! [X0] :
( aElementOf0(X0,stldt0(sbsmnsldt0(xS)))
=> ? [X1] :
( ( ( ! [X2] :
( ( ( ( sdteqdtlpzmzozddtrp0(X2,X0,X1)
| aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0)))
| ? [X3] :
( sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0))
& aInteger0(X3) ) )
& aInteger0(X2) )
=> aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)) )
& ( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
=> ( sdteqdtlpzmzozddtrp0(X2,X0,X1)
& aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0)))
& ? [X3] :
( sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0))
& aInteger0(X3) )
& aInteger0(X2) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(X0,X1)) )
=> ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),stldt0(sbsmnsldt0(xS)))
| ! [X2] :
( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
=> aElementOf0(X2,stldt0(sbsmnsldt0(xS))) ) ) )
& X1 != sz00
& aInteger0(X1) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f45]) ).
fof(f49,plain,
~ ( ( ! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
<=> ( ? [X1] :
( aElementOf0(X0,X1)
& aElementOf0(X1,xS) )
& aInteger0(X0) ) )
& aSet0(sbsmnsldt0(xS)) )
=> ( isClosed0(sbsmnsldt0(xS))
| ( ! [X2] :
( aElementOf0(X2,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(X2,sbsmnsldt0(xS))
& aInteger0(X2) ) )
=> ( isOpen0(stldt0(sbsmnsldt0(xS)))
| ! [X3] :
( aElementOf0(X3,stldt0(sbsmnsldt0(xS)))
=> ? [X4] :
( ( ( ! [X5] :
( ( ( ( sdteqdtlpzmzozddtrp0(X5,X3,X4)
| aDivisorOf0(X4,sdtpldt0(X5,smndt0(X3)))
| ? [X7] :
( sdtpldt0(X5,smndt0(X3)) = sdtasdt0(X4,X7)
& aInteger0(X7) ) )
& aInteger0(X5) )
=> aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(X3,X4)) )
& ( aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(X3,X4))
=> ( sdteqdtlpzmzozddtrp0(X5,X3,X4)
& aDivisorOf0(X4,sdtpldt0(X5,smndt0(X3)))
& ? [X6] :
( sdtasdt0(X4,X6) = sdtpldt0(X5,smndt0(X3))
& aInteger0(X6) )
& aInteger0(X5) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(X3,X4)) )
=> ( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X3,X4),stldt0(sbsmnsldt0(xS)))
| ! [X8] :
( aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(X3,X4))
=> aElementOf0(X8,stldt0(sbsmnsldt0(xS))) ) ) )
& sz00 != X4
& aInteger0(X4) ) ) ) ) ) ),
inference(rectify,[],[f46]) ).
fof(f58,plain,
( ! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
<=> ( ? [X1] :
( aElementOf0(X0,X1)
& aElementOf0(X1,xS) )
& aInteger0(X0) ) )
& aSet0(sbsmnsldt0(xS))
& ~ isClosed0(sbsmnsldt0(xS))
& ! [X2] :
( aElementOf0(X2,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(X2,sbsmnsldt0(xS))
& aInteger0(X2) ) )
& ~ isOpen0(stldt0(sbsmnsldt0(xS)))
& ? [X3] :
( aElementOf0(X3,stldt0(sbsmnsldt0(xS)))
& ! [X4] :
( ( ! [X5] :
( ( ( ~ sdteqdtlpzmzozddtrp0(X5,X3,X4)
& ~ aDivisorOf0(X4,sdtpldt0(X5,smndt0(X3)))
& ! [X7] :
( sdtpldt0(X5,smndt0(X3)) != sdtasdt0(X4,X7)
| ~ aInteger0(X7) ) )
| ~ aInteger0(X5)
| aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(X3,X4)) )
& ( ~ aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(X3,X4))
| ( sdteqdtlpzmzozddtrp0(X5,X3,X4)
& aDivisorOf0(X4,sdtpldt0(X5,smndt0(X3)))
& ? [X6] :
( sdtasdt0(X4,X6) = sdtpldt0(X5,smndt0(X3))
& aInteger0(X6) )
& aInteger0(X5) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(X3,X4))
& ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X3,X4),stldt0(sbsmnsldt0(xS)))
& ? [X8] :
( aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(X3,X4))
& ~ aElementOf0(X8,stldt0(sbsmnsldt0(xS))) ) )
| sz00 = X4
| ~ aInteger0(X4) ) ) ),
inference(ennf_transformation,[],[f49]) ).
fof(f59,plain,
( ! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
<=> ( ? [X1] :
( aElementOf0(X0,X1)
& aElementOf0(X1,xS) )
& aInteger0(X0) ) )
& aSet0(sbsmnsldt0(xS))
& ~ isClosed0(sbsmnsldt0(xS))
& ! [X2] :
( aElementOf0(X2,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(X2,sbsmnsldt0(xS))
& aInteger0(X2) ) )
& ~ isOpen0(stldt0(sbsmnsldt0(xS)))
& ? [X3] :
( aElementOf0(X3,stldt0(sbsmnsldt0(xS)))
& ! [X4] :
( ( ! [X5] :
( ( ( ~ sdteqdtlpzmzozddtrp0(X5,X3,X4)
& ~ aDivisorOf0(X4,sdtpldt0(X5,smndt0(X3)))
& ! [X7] :
( sdtpldt0(X5,smndt0(X3)) != sdtasdt0(X4,X7)
| ~ aInteger0(X7) ) )
| ~ aInteger0(X5)
| aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(X3,X4)) )
& ( ~ aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(X3,X4))
| ( sdteqdtlpzmzozddtrp0(X5,X3,X4)
& aDivisorOf0(X4,sdtpldt0(X5,smndt0(X3)))
& ? [X6] :
( sdtasdt0(X4,X6) = sdtpldt0(X5,smndt0(X3))
& aInteger0(X6) )
& aInteger0(X5) ) ) )
& aSet0(szAzrzSzezqlpdtcmdtrp0(X3,X4))
& ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X3,X4),stldt0(sbsmnsldt0(xS)))
& ? [X8] :
( aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(X3,X4))
& ~ aElementOf0(X8,stldt0(sbsmnsldt0(xS))) ) )
| sz00 = X4
| ~ aInteger0(X4) ) ) ),
inference(flattening,[],[f58]) ).
fof(f62,plain,
! [X0] :
( ~ aInteger0(X0)
| ( sz00 = sdtasdt0(sz00,X0)
& sdtasdt0(X0,sz00) = sz00 ) ),
inference(ennf_transformation,[],[f15]) ).
fof(f93,plain,
! [X0,X1] :
( sz00 = X1
| ~ aInteger0(X1)
| ~ aInteger0(X0)
| ( isClosed0(szAzrzSzezqlpdtcmdtrp0(X0,X1))
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),cS1395) ) ),
inference(ennf_transformation,[],[f41]) ).
fof(f94,plain,
! [X0,X1] :
( sz00 = X1
| ~ aInteger0(X1)
| ~ aInteger0(X0)
| ( isClosed0(szAzrzSzezqlpdtcmdtrp0(X0,X1))
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),cS1395) ) ),
inference(flattening,[],[f93]) ).
fof(f106,plain,
! [X0] :
( ? [X1] :
( aElementOf0(X1,X0)
& ( ~ isClosed0(X1)
| ~ aSubsetOf0(X1,cS1395) ) )
| ~ isFinite0(X0)
| ~ aSet0(X0)
| isClosed0(sbsmnsldt0(X0)) ),
inference(ennf_transformation,[],[f40]) ).
fof(f107,plain,
! [X0] :
( ? [X1] :
( aElementOf0(X1,X0)
& ( ~ isClosed0(X1)
| ~ aSubsetOf0(X1,cS1395) ) )
| ~ isFinite0(X0)
| ~ aSet0(X0)
| isClosed0(sbsmnsldt0(X0)) ),
inference(flattening,[],[f106]) ).
fof(f122,plain,
( xS = cS2043
& ! [X0] :
( ( ! [X2] :
( ( sP0(X2)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X2))
& szAzrzSzezqlpdtcmdtrp0(sz00,X2) != X0 )
| ~ isPrime0(X2)
| sz00 = X2
| ~ aInteger0(X2) )
| aElementOf0(X0,xS) )
& ( ~ aElementOf0(X0,xS)
| ? [X1] :
( szAzrzSzezqlpdtcmdtrp0(sz00,X1) = X0
& sP1(X1)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X1))
& isPrime0(X1)
& X1 != sz00
& aInteger0(X1) ) ) )
& aSet0(xS) ),
inference(rectify,[],[f110]) ).
fof(f123,plain,
( xS = cS2043
& ! [X0] :
( ( ! [X2] :
( ( sP0(X2)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X2))
& szAzrzSzezqlpdtcmdtrp0(sz00,X2) != X0 )
| ~ isPrime0(X2)
| sz00 = X2
| ~ aInteger0(X2) )
| aElementOf0(X0,xS) )
& ( ~ aElementOf0(X0,xS)
| ( szAzrzSzezqlpdtcmdtrp0(sz00,sK7(X0)) = X0
& sP1(sK7(X0))
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,sK7(X0)))
& isPrime0(sK7(X0))
& sz00 != sK7(X0)
& aInteger0(sK7(X0)) ) ) )
& aSet0(xS) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X1,sK7(X0))],[f122]) ).
fof(f131,plain,
( ! [X0] :
( ( ~ aElementOf0(X0,sbsmnsldt0(xS))
| ( ? [X1] :
( aElementOf0(X0,X1)
& aElementOf0(X1,xS) )
& aInteger0(X0) ) )
& ( ! [X1] :
( ~ aElementOf0(X0,X1)
| ~ aElementOf0(X1,xS) )
| ~ aInteger0(X0)
| aElementOf0(X0,sbsmnsldt0(xS)) ) )
& aSet0(sbsmnsldt0(xS))
& ~ isClosed0(sbsmnsldt0(xS))
& ! [X2] :
( ( ~ aElementOf0(X2,stldt0(sbsmnsldt0(xS)))
| ( ~ aElementOf0(X2,sbsmnsldt0(xS))
& aInteger0(X2) ) )
& ( aElementOf0(X2,sbsmnsldt0(xS))
| ~ aInteger0(X2)
| aElementOf0(X2,stldt0(sbsmnsldt0(xS))) ) )
& ~ isOpen0(stldt0(sbsmnsldt0(xS)))
& ? [X3] :
( aElementOf0(X3,stldt0(sbsmnsldt0(xS)))
& ! [X4] :
( ( sP2(X3,X4)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X3,X4))
& ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X3,X4),stldt0(sbsmnsldt0(xS)))
& ? [X8] :
( aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(X3,X4))
& ~ aElementOf0(X8,stldt0(sbsmnsldt0(xS))) ) )
| sz00 = X4
| ~ aInteger0(X4) ) ) ),
inference(nnf_transformation,[],[f112]) ).
fof(f132,plain,
( ! [X0] :
( ( ~ aElementOf0(X0,sbsmnsldt0(xS))
| ( ? [X1] :
( aElementOf0(X0,X1)
& aElementOf0(X1,xS) )
& aInteger0(X0) ) )
& ( ! [X1] :
( ~ aElementOf0(X0,X1)
| ~ aElementOf0(X1,xS) )
| ~ aInteger0(X0)
| aElementOf0(X0,sbsmnsldt0(xS)) ) )
& aSet0(sbsmnsldt0(xS))
& ~ isClosed0(sbsmnsldt0(xS))
& ! [X2] :
( ( ~ aElementOf0(X2,stldt0(sbsmnsldt0(xS)))
| ( ~ aElementOf0(X2,sbsmnsldt0(xS))
& aInteger0(X2) ) )
& ( aElementOf0(X2,sbsmnsldt0(xS))
| ~ aInteger0(X2)
| aElementOf0(X2,stldt0(sbsmnsldt0(xS))) ) )
& ~ isOpen0(stldt0(sbsmnsldt0(xS)))
& ? [X3] :
( aElementOf0(X3,stldt0(sbsmnsldt0(xS)))
& ! [X4] :
( ( sP2(X3,X4)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X3,X4))
& ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X3,X4),stldt0(sbsmnsldt0(xS)))
& ? [X8] :
( aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(X3,X4))
& ~ aElementOf0(X8,stldt0(sbsmnsldt0(xS))) ) )
| sz00 = X4
| ~ aInteger0(X4) ) ) ),
inference(flattening,[],[f131]) ).
fof(f133,plain,
( ! [X4] :
( ( ~ aElementOf0(X4,sbsmnsldt0(xS))
| ( ? [X6] :
( aElementOf0(X4,X6)
& aElementOf0(X6,xS) )
& aInteger0(X4) ) )
& ( ! [X5] :
( ~ aElementOf0(X4,X5)
| ~ aElementOf0(X5,xS) )
| ~ aInteger0(X4)
| aElementOf0(X4,sbsmnsldt0(xS)) ) )
& aSet0(sbsmnsldt0(xS))
& ~ isClosed0(sbsmnsldt0(xS))
& ! [X3] :
( ( ~ aElementOf0(X3,stldt0(sbsmnsldt0(xS)))
| ( ~ aElementOf0(X3,sbsmnsldt0(xS))
& aInteger0(X3) ) )
& ( aElementOf0(X3,sbsmnsldt0(xS))
| ~ aInteger0(X3)
| aElementOf0(X3,stldt0(sbsmnsldt0(xS))) ) )
& ~ isOpen0(stldt0(sbsmnsldt0(xS)))
& ? [X0] :
( aElementOf0(X0,stldt0(sbsmnsldt0(xS)))
& ! [X1] :
( ( sP2(X0,X1)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X0,X1))
& ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),stldt0(sbsmnsldt0(xS)))
& ? [X2] :
( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
& ~ aElementOf0(X2,stldt0(sbsmnsldt0(xS))) ) )
| sz00 = X1
| ~ aInteger0(X1) ) ) ),
inference(rectify,[],[f132]) ).
fof(f134,plain,
( ! [X4] :
( ( ~ aElementOf0(X4,sbsmnsldt0(xS))
| ( aElementOf0(X4,sK12(X4))
& aElementOf0(sK12(X4),xS)
& aInteger0(X4) ) )
& ( ! [X5] :
( ~ aElementOf0(X4,X5)
| ~ aElementOf0(X5,xS) )
| ~ aInteger0(X4)
| aElementOf0(X4,sbsmnsldt0(xS)) ) )
& aSet0(sbsmnsldt0(xS))
& ~ isClosed0(sbsmnsldt0(xS))
& ! [X3] :
( ( ~ aElementOf0(X3,stldt0(sbsmnsldt0(xS)))
| ( ~ aElementOf0(X3,sbsmnsldt0(xS))
& aInteger0(X3) ) )
& ( aElementOf0(X3,sbsmnsldt0(xS))
| ~ aInteger0(X3)
| aElementOf0(X3,stldt0(sbsmnsldt0(xS))) ) )
& ~ isOpen0(stldt0(sbsmnsldt0(xS)))
& aElementOf0(sK10,stldt0(sbsmnsldt0(xS)))
& ! [X1] :
( ( sP2(sK10,X1)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sK10,X1))
& ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sK10,X1),stldt0(sbsmnsldt0(xS)))
& aElementOf0(sK11(X1),szAzrzSzezqlpdtcmdtrp0(sK10,X1))
& ~ aElementOf0(sK11(X1),stldt0(sbsmnsldt0(xS))) )
| sz00 = X1
| ~ aInteger0(X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12]),skolemize(X0,sK10),skolemize(X2,sK11(X1)),skolemize(X6,sK12(X4))],[f133]) ).
fof(f168,plain,
! [X0] :
( ( aElementOf0(sK25(X0),X0)
& ( ~ isClosed0(sK25(X0))
| ~ aSubsetOf0(sK25(X0),cS1395) ) )
| ~ isFinite0(X0)
| ~ aSet0(X0)
| isClosed0(sbsmnsldt0(X0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(X1,sK25(X0))],[f107]) ).
fof(f185,plain,
xS = cS2043,
inference(cnf_transformation,[],[f123]) ).
fof(f189,plain,
! [X0] :
( ~ aElementOf0(X0,xS)
| szAzrzSzezqlpdtcmdtrp0(sz00,sK7(X0)) = X0 ),
inference(cnf_transformation,[],[f123]) ).
fof(f193,plain,
! [X0] :
( ~ aElementOf0(X0,xS)
| sz00 != sK7(X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f194,plain,
! [X0] :
( ~ aElementOf0(X0,xS)
| aInteger0(sK7(X0)) ),
inference(cnf_transformation,[],[f123]) ).
fof(f195,plain,
aSet0(xS),
inference(cnf_transformation,[],[f123]) ).
fof(f209,plain,
isFinite0(xS),
inference(cnf_transformation,[],[f44]) ).
fof(f223,plain,
~ isClosed0(sbsmnsldt0(xS)),
inference(cnf_transformation,[],[f134]) ).
fof(f229,plain,
! [X1] :
( sP2(sK10,X1)
| sz00 = X1
| ~ aInteger0(X1) ),
inference(cnf_transformation,[],[f134]) ).
fof(f232,plain,
! [X1] :
( aElementOf0(sK11(X1),szAzrzSzezqlpdtcmdtrp0(sK10,X1))
| sz00 = X1
| ~ aInteger0(X1) ),
inference(cnf_transformation,[],[f134]) ).
fof(f236,plain,
! [X0] :
( ~ aInteger0(X0)
| sz00 = sdtasdt0(X0,sz00) ),
inference(cnf_transformation,[],[f62]) ).
fof(f237,plain,
aInteger0(sz00),
inference(cnf_transformation,[],[f2]) ).
fof(f271,plain,
! [X0,X1] :
( sz00 = X1
| ~ aInteger0(X1)
| ~ aInteger0(X0)
| isClosed0(szAzrzSzezqlpdtcmdtrp0(X0,X1)) ),
inference(cnf_transformation,[],[f94]) ).
fof(f272,plain,
! [X0,X1] :
( sz00 = X1
| ~ aInteger0(X1)
| ~ aInteger0(X0)
| aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),cS1395) ),
inference(cnf_transformation,[],[f94]) ).
fof(f314,plain,
! [X0] :
( aElementOf0(sK25(X0),X0)
| ~ isFinite0(X0)
| ~ aSet0(X0)
| isClosed0(sbsmnsldt0(X0)) ),
inference(cnf_transformation,[],[f168]) ).
fof(f315,plain,
! [X0] :
( ~ isClosed0(sK25(X0))
| ~ aSubsetOf0(sK25(X0),cS1395)
| ~ isFinite0(X0)
| ~ aSet0(X0)
| isClosed0(sbsmnsldt0(X0)) ),
inference(cnf_transformation,[],[f168]) ).
fof(f316,plain,
aSet0(cS2043),
inference(definition_unfolding,[],[f195,f185]) ).
fof(f317,plain,
! [X0] :
( ~ aElementOf0(X0,cS2043)
| aInteger0(sK7(X0)) ),
inference(definition_unfolding,[],[f194,f185]) ).
fof(f318,plain,
! [X0] :
( ~ aElementOf0(X0,cS2043)
| sz00 != sK7(X0) ),
inference(definition_unfolding,[],[f193,f185]) ).
fof(f322,plain,
! [X0] :
( ~ aElementOf0(X0,cS2043)
| szAzrzSzezqlpdtcmdtrp0(sz00,sK7(X0)) = X0 ),
inference(definition_unfolding,[],[f189,f185]) ).
fof(f339,plain,
isFinite0(cS2043),
inference(definition_unfolding,[],[f209,f185]) ).
fof(f347,plain,
~ isClosed0(sbsmnsldt0(cS2043)),
inference(definition_unfolding,[],[f223,f185]) ).
tcf(c_65,plain,
aSet0(cS2043),
inference(cnf_transformation,[],[f316]) ).
tcf(c_66,plain,
! [X0: $i] :
( aInteger0(sK7(X0))
| ~ aElementOf0(X0,cS2043) ),
inference(cnf_transformation,[],[f317]) ).
tcf(c_67,plain,
! [X0: $i] :
( ~ aElementOf0(X0,cS2043)
| ( sK7(X0) != sz00 ) ),
inference(cnf_transformation,[],[f318]) ).
tcf(c_71,plain,
! [X0: $i] :
( ( szAzrzSzezqlpdtcmdtrp0(sz00,sK7(X0)) = X0 )
| ~ aElementOf0(X0,cS2043) ),
inference(cnf_transformation,[],[f322]) ).
tcf(c_88,plain,
isFinite0(cS2043),
inference(cnf_transformation,[],[f339]) ).
tcf(c_98,negated_conjecture,
! [X0: $i] :
( aElementOf0(sK11(X0),szAzrzSzezqlpdtcmdtrp0(sK10,X0))
| ( X0 = sz00 )
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f232]) ).
tcf(c_101,negated_conjecture,
! [X0: $i] :
( sP2(sK10,X0)
| ( X0 = sz00 )
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f229]) ).
tcf(c_107,negated_conjecture,
~ isClosed0(sbsmnsldt0(cS2043)),
inference(cnf_transformation,[],[f347]) ).
tcf(c_114,plain,
! [X0: $i] :
( ( sdtasdt0(X0,sz00) = sz00 )
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f236]) ).
tcf(c_116,plain,
aInteger0(sz00),
inference(cnf_transformation,[],[f237]) ).
tcf(c_150,plain,
! [X0: $i,X1: $i] :
( aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X1,X0),cS1395)
| ( X0 = sz00 )
| ~ aInteger0(X1)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f272]) ).
tcf(c_151,plain,
! [X0: $i,X1: $i] :
( isClosed0(szAzrzSzezqlpdtcmdtrp0(X1,X0))
| ( X0 = sz00 )
| ~ aInteger0(X1)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f271]) ).
tcf(c_193,plain,
! [X0: $i] :
( isClosed0(sbsmnsldt0(X0))
| ~ isFinite0(X0)
| ~ aSet0(X0)
| ~ isClosed0(sK25(X0))
| ~ aSubsetOf0(sK25(X0),cS1395) ),
inference(cnf_transformation,[],[f315]) ).
tcf(c_194,plain,
! [X0: $i] :
( isClosed0(sbsmnsldt0(X0))
| aElementOf0(sK25(X0),X0)
| ~ isFinite0(X0)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f314]) ).
tcf(c_2213,plain,
! [X0: $i] :
( isClosed0(sbsmnsldt0(X0))
| aElementOf0(sK25(X0),X0)
| ~ aSet0(X0)
| ( X0 != cS2043 ) ),
inference(resolution_lifted,[status(thm)],[c_88,c_194]) ).
tcf(c_2214,plain,
( isClosed0(sbsmnsldt0(cS2043))
| aElementOf0(sK25(cS2043),cS2043)
| ~ aSet0(cS2043) ),
inference(unflattening,[status(thm)],[c_2213]) ).
tcf(c_2215,plain,
aElementOf0(sK25(cS2043),cS2043),
inference(global_subsumption_just,[status(thm)],[c_2214,c_65,c_107,c_2214]) ).
tcf(c_2220,plain,
! [X0: $i] :
( isClosed0(sbsmnsldt0(X0))
| ~ aSet0(X0)
| ~ isClosed0(sK25(X0))
| ~ aSubsetOf0(sK25(X0),cS1395)
| ( X0 != cS2043 ) ),
inference(resolution_lifted,[status(thm)],[c_88,c_193]) ).
tcf(c_2221,plain,
( isClosed0(sbsmnsldt0(cS2043))
| ~ aSet0(cS2043)
| ~ isClosed0(sK25(cS2043))
| ~ aSubsetOf0(sK25(cS2043),cS1395) ),
inference(unflattening,[status(thm)],[c_2220]) ).
tcf(c_2222,plain,
( ~ isClosed0(sK25(cS2043))
| ~ aSubsetOf0(sK25(cS2043),cS1395) ),
inference(global_subsumption_just,[status(thm)],[c_2221,c_65,c_107,c_2221]) ).
tcf(c_11554,plain,
aInteger0(sK7(sK25(cS2043))),
inference(superposition,[status(thm)],[c_2215,c_66]) ).
tcf(c_15276,plain,
szAzrzSzezqlpdtcmdtrp0(sz00,sK7(sK25(cS2043))) = sK25(cS2043),
inference(superposition,[status(thm)],[c_2215,c_71]) ).
tcf(c_33602,plain,
( aSubsetOf0(sK25(cS2043),cS1395)
| ( sK7(sK25(cS2043)) = sz00 )
| ~ aInteger0(sz00)
| ~ aInteger0(sK7(sK25(cS2043))) ),
inference(superposition,[status(thm)],[c_15276,c_150]) ).
tcf(c_33604,plain,
( isClosed0(sK25(cS2043))
| ( sK7(sK25(cS2043)) = sz00 )
| ~ aInteger0(sz00)
| ~ aInteger0(sK7(sK25(cS2043))) ),
inference(superposition,[status(thm)],[c_15276,c_151]) ).
tcf(c_33618,plain,
( isClosed0(sK25(cS2043))
| ( sK7(sK25(cS2043)) = sz00 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_33604,c_116,c_11554]) ).
tcf(c_33624,plain,
( aSubsetOf0(sK25(cS2043),cS1395)
| ( sK7(sK25(cS2043)) = sz00 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_33602,c_116,c_11554]) ).
fof(f111,definition,
! [X3,X4] :
( ~ sP2(X3,X4)
| ! [X5] :
( ( ( ~ sdteqdtlpzmzozddtrp0(X5,X3,X4)
& ~ aDivisorOf0(X4,sdtpldt0(X5,smndt0(X3)))
& ! [X7] :
( sdtpldt0(X5,smndt0(X3)) != sdtasdt0(X4,X7)
| ~ aInteger0(X7) ) )
| ~ aInteger0(X5)
| aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(X3,X4)) )
& ( ~ aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(X3,X4))
| ( sdteqdtlpzmzozddtrp0(X5,X3,X4)
& aDivisorOf0(X4,sdtpldt0(X5,smndt0(X3)))
& ? [X6] :
( sdtasdt0(X4,X6) = sdtpldt0(X5,smndt0(X3))
& aInteger0(X6) )
& aInteger0(X5) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f112,plain,
( ! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
<=> ( ? [X1] :
( aElementOf0(X0,X1)
& aElementOf0(X1,xS) )
& aInteger0(X0) ) )
& aSet0(sbsmnsldt0(xS))
& ~ isClosed0(sbsmnsldt0(xS))
& ! [X2] :
( aElementOf0(X2,stldt0(sbsmnsldt0(xS)))
<=> ( ~ aElementOf0(X2,sbsmnsldt0(xS))
& aInteger0(X2) ) )
& ~ isOpen0(stldt0(sbsmnsldt0(xS)))
& ? [X3] :
( aElementOf0(X3,stldt0(sbsmnsldt0(xS)))
& ! [X4] :
( ( sP2(X3,X4)
& aSet0(szAzrzSzezqlpdtcmdtrp0(X3,X4))
& ~ aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X3,X4),stldt0(sbsmnsldt0(xS)))
& ? [X8] :
( aElementOf0(X8,szAzrzSzezqlpdtcmdtrp0(X3,X4))
& ~ aElementOf0(X8,stldt0(sbsmnsldt0(xS))) ) )
| sz00 = X4
| ~ aInteger0(X4) ) ) ),
inference(definition_folding,[],[f59,f111]) ).
fof(f128,plain,
! [X3,X4] :
( ~ sP2(X3,X4)
| ! [X5] :
( ( ( ~ sdteqdtlpzmzozddtrp0(X5,X3,X4)
& ~ aDivisorOf0(X4,sdtpldt0(X5,smndt0(X3)))
& ! [X7] :
( sdtpldt0(X5,smndt0(X3)) != sdtasdt0(X4,X7)
| ~ aInteger0(X7) ) )
| ~ aInteger0(X5)
| aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(X3,X4)) )
& ( ~ aElementOf0(X5,szAzrzSzezqlpdtcmdtrp0(X3,X4))
| ( sdteqdtlpzmzozddtrp0(X5,X3,X4)
& aDivisorOf0(X4,sdtpldt0(X5,smndt0(X3)))
& ? [X6] :
( sdtasdt0(X4,X6) = sdtpldt0(X5,smndt0(X3))
& aInteger0(X6) )
& aInteger0(X5) ) ) ) ),
inference(nnf_transformation,[],[f111]) ).
fof(f129,plain,
! [X0,X1] :
( ~ sP2(X0,X1)
| ! [X2] :
( ( ( ~ sdteqdtlpzmzozddtrp0(X2,X0,X1)
& ~ aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0)))
& ! [X4] :
( sdtpldt0(X2,smndt0(X0)) != sdtasdt0(X1,X4)
| ~ aInteger0(X4) ) )
| ~ aInteger0(X2)
| aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)) )
& ( ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
| ( sdteqdtlpzmzozddtrp0(X2,X0,X1)
& aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0)))
& ? [X3] :
( sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0))
& aInteger0(X3) )
& aInteger0(X2) ) ) ) ),
inference(rectify,[],[f128]) ).
fof(f130,plain,
! [X0,X1] :
( ~ sP2(X0,X1)
| ! [X2] :
( ( ( ~ sdteqdtlpzmzozddtrp0(X2,X0,X1)
& ~ aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0)))
& ! [X4] :
( sdtpldt0(X2,smndt0(X0)) != sdtasdt0(X1,X4)
| ~ aInteger0(X4) ) )
| ~ aInteger0(X2)
| aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)) )
& ( ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
| ( sdteqdtlpzmzozddtrp0(X2,X0,X1)
& aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0)))
& sdtpldt0(X2,smndt0(X0)) = sdtasdt0(X1,sK9(X0,X1,X2))
& aInteger0(sK9(X0,X1,X2))
& aInteger0(X2) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X3,sK9(X0,X1,X2))],[f129]) ).
fof(f216,plain,
! [X2,X0,X1] :
( ~ sP2(X0,X1)
| ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
| aInteger0(sK9(X0,X1,X2)) ),
inference(cnf_transformation,[],[f130]) ).
fof(f217,plain,
! [X2,X0,X1] :
( ~ sP2(X0,X1)
| ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))
| aInteger0(X2) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i,X2: $i] :
( aInteger0(X0)
| ~ sP2(X1,X2)
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(X1,X2)) ),
inference(cnf_transformation,[],[f217]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i,X2: $i] :
( aInteger0(sK9(X1,X2,X0))
| ~ sP2(X1,X2)
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(X1,X2)) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_2603,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( aInteger0(sK9(X0,X1,X3))
| ( X2 = sz00 )
| ~ aInteger0(X2)
| ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X0,X1))
| ( X1 != X2 )
| ( X0 != sK10 ) ),
inference(resolution_lifted,[status(thm)],[c_90,c_101]) ).
tcf(c_2604,plain,
! [X0: $i,X1: $i] :
( aInteger0(sK9(sK10,X1,X0))
| ( X1 = sz00 )
| ~ aInteger0(X1)
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sK10,X1)) ),
inference(unflattening,[status(thm)],[c_2603]) ).
tcf(c_2618,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( aInteger0(X3)
| ( X2 = sz00 )
| ~ aInteger0(X2)
| ~ aElementOf0(X3,szAzrzSzezqlpdtcmdtrp0(X0,X1))
| ( X1 != X2 )
| ( X0 != sK10 ) ),
inference(resolution_lifted,[status(thm)],[c_89,c_101]) ).
tcf(c_2619,plain,
! [X0: $i,X1: $i] :
( aInteger0(X0)
| ( X1 = sz00 )
| ~ aInteger0(X1)
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sK10,X1)) ),
inference(unflattening,[status(thm)],[c_2618]) ).
tcf(c_11359,plain,
! [X0: $i] :
( aInteger0(sK11(X0))
| ( X0 = sz00 )
| ~ aInteger0(X0) ),
inference(superposition,[status(thm)],[c_98,c_2619]) ).
tcf(c_11395,plain,
! [X0: $i] :
( aInteger0(sK9(sK10,X0,sK11(X0)))
| ( X0 = sz00 )
| ~ aInteger0(X0) ),
inference(superposition,[status(thm)],[c_98,c_2604]) ).
tcf(c_11779,plain,
! [X0: $i] :
( ( X0 = sz00 )
| ( sdtasdt0(sK9(sK10,X0,sK11(X0)),sz00) = sz00 )
| ~ aInteger0(X0) ),
inference(superposition,[status(thm)],[c_11395,c_114]) ).
tcf(c_11861,plain,
! [X0: $i] :
( ( X0 = sz00 )
| ( sK11(X0) = sz00 )
| ( sdtasdt0(sK9(sK10,sK11(X0),sK11(sK11(X0))),sz00) = sz00 )
| ~ aInteger0(X0) ),
inference(superposition,[status(thm)],[c_11359,c_11779]) ).
tcf(c_12037,plain,
( ( sK7(sK25(cS2043)) = sz00 )
| ( sK11(sK7(sK25(cS2043))) = sz00 )
| ( sdtasdt0(sK9(sK10,sK11(sK7(sK25(cS2043))),sK11(sK11(sK7(sK25(cS2043))))),sz00) = sz00 ) ),
inference(superposition,[status(thm)],[c_11554,c_11861]) ).
tcf(c_34357,plain,
sK7(sK25(cS2043)) = sz00,
inference(global_subsumption_just,[status(thm)],[c_12037,c_2222,c_33618,c_33624]) ).
tcf(c_34368,plain,
~ aElementOf0(sK25(cS2043),cS2043),
inference(superposition,[status(thm)],[c_34357,c_67]) ).
tcf(c_34370,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_34368,c_2215]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM449+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.37 % Computer : n015.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8046.5625MB
% 0.13/0.37 % OS : Linux 6.8.0-71-generic
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Thu Sep 24 04:05:40 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.41 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.43
% 0.13/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.43
% 0.13/0.43 % Detected problem language: tptp
% 0.13/0.44 % Proving...
% 1.44/1.77 % SZS status Started for theBenchmark.p
% 1.44/1.77 % SZS status Theorem for theBenchmark.p
% 1.44/1.77
% 1.44/1.77 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.44/1.77
% 1.44/1.77 % ------ iProver source info
% 1.44/1.77
% 1.44/1.77 % git: date: 2026-07-19 20:42:38 +0200
% 1.44/1.77 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.44/1.77 % git: non_committed_changes: false
% 1.44/1.77
% 1.44/1.77 % ------ Parsing...
% 1.44/1.77 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 1.44/1.77
% 1.44/1.77 % ------ Preprocessing... sup_sim: 11 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sup_sim: 0 sf_s rm: 4 0s sf_e pe_s pe_e %
% 1.44/1.77
% 1.44/1.77 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 1.44/1.77
% 1.44/1.77 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 1.44/1.77 % ------ Proving...
% 1.44/1.77 % ------ Problem Properties
% 1.44/1.77
% 1.44/1.77 %
% 1.44/1.77 % clauses 140
% 1.44/1.77 % conjectures 8
% 1.44/1.77 % EPR 23
% 1.44/1.77 % Horn 91
% 1.44/1.77 % unary 12
% 1.44/1.77 % binary 32
% 1.44/1.77 % lits 472
% 1.44/1.77 % lits eq 78
% 1.44/1.77 % fd_pure 0
% 1.44/1.77 % fd_pseudo 0
% 1.44/1.77 % fd_cond 34
% 1.44/1.77 % fd_pseudo_cond 7
% 1.44/1.77 % AC symbols 0
% 1.44/1.77
% 1.44/1.77 % ------ Schedule dynamic 5 is on
% 1.44/1.77
% 1.44/1.77 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 1.44/1.77
% 1.44/1.77
% 1.44/1.77 % ------
% 1.44/1.77 % Current options:
% 1.44/1.77 % ------
% 1.44/1.77
% 1.44/1.77
% 1.44/1.77 %
% 1.44/1.77
% 1.44/1.77 % ------ Proving...
% 1.44/1.77 %
% 1.44/1.77
% 1.44/1.77 % SZS status Theorem for theBenchmark.p
% 1.44/1.77
% 1.44/1.77 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.44/1.78
% 1.44/1.78
%------------------------------------------------------------------------------