%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM455+6 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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 : Tue Sep 29 12:15:16 PM UTC 2026
% Result : Theorem 1.85s 1.12s
% Output : Refutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 20
% Syntax : Number of formulae : 96 ( 27 unt; 12 def)
% Number of atoms : 448 ( 61 equ)
% Maximal formula atoms : 33 ( 4 avg)
% Number of connectives : 512 ( 160 ~; 135 |; 193 &)
% ( 16 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 9 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 7 con; 0-2 aty)
% Number of variables : 80 ( 0 sgn 56 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
aInteger0(sz10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mIntOne) ).
fof(f4,axiom,
! [X0] :
( aInteger0(X0)
=> aInteger0(smndt0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mIntNeg) ).
fof(f5,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1) )
=> aInteger0(sdtpldt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mIntPlus) ).
fof(f46,axiom,
( aInteger0(xp)
& xp != sz00
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ! [X0] :
( ( aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
=> ( aInteger0(X0)
& ? [X1] :
( aInteger0(X1)
& sdtasdt0(xp,X1) = sdtpldt0(X0,smndt0(sz10)) )
& aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(X0,sz10,xp) ) )
& ( ( aInteger0(X0)
& ( ? [X1] :
( aInteger0(X1)
& sdtasdt0(xp,X1) = sdtpldt0(X0,smndt0(sz10)) )
| aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
| sdteqdtlpzmzozddtrp0(X0,sz10,xp) ) )
=> aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ) )
& aSet0(sbsmnsldt0(xS))
& ! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
<=> ( aInteger0(X0)
& ? [X1] :
( aElementOf0(X1,xS)
& aElementOf0(X0,X1) ) ) )
& ! [X0] :
( aElementOf0(X0,stldt0(sbsmnsldt0(xS)))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,sbsmnsldt0(xS)) ) )
& ! [X0] :
( aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
=> aElementOf0(X0,stldt0(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2171) ).
fof(f47,axiom,
( ? [X0] :
( aInteger0(X0)
& sdtasdt0(xp,X0) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)) )
& aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
& aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ? [X0] :
( aInteger0(X0)
& sdtasdt0(xp,X0) = sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)) )
& aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp)
& aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2232) ).
fof(f48,axiom,
( sdtpldt0(sz10,xp) != sz10
& sdtpldt0(sz10,smndt0(xp)) != sz10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2258) ).
fof(f49,axiom,
( sdtpldt0(sz10,xp) != smndt0(sz10)
| sdtpldt0(sz10,smndt0(xp)) != smndt0(sz10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2286) ).
fof(f50,conjecture,
? [X0] :
( ( ( aInteger0(X0)
& ( ? [X1] :
( aInteger0(X1)
& sdtasdt0(xp,X1) = sdtpldt0(X0,smndt0(sz10)) )
| aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
| sdteqdtlpzmzozddtrp0(X0,sz10,xp) ) )
| aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ~ ( ( X0 = sz10
| X0 = smndt0(sz10) )
& aElementOf0(X0,cS2200) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f51,negated_conjecture,
~ ? [X0] :
( ( ( aInteger0(X0)
& ( ? [X1] :
( aInteger0(X1)
& sdtasdt0(xp,X1) = sdtpldt0(X0,smndt0(sz10)) )
| aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
| sdteqdtlpzmzozddtrp0(X0,sz10,xp) ) )
| aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ~ ( ( X0 = sz10
| X0 = smndt0(sz10) )
& aElementOf0(X0,cS2200) ) ),
inference(negated_conjecture,[status(cth)],[f50]) ).
fof(f55,plain,
( aInteger0(xp)
& xp != sz00
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ! [X0] :
( ( aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
=> ( aInteger0(X0)
& ? [X1] :
( aInteger0(X1)
& sdtasdt0(xp,X1) = sdtpldt0(X0,smndt0(sz10)) )
& aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(X0,sz10,xp) ) )
& ( ( aInteger0(X0)
& ( ? [X2] :
( aInteger0(X2)
& sdtpldt0(X0,smndt0(sz10)) = sdtasdt0(xp,X2) )
| aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
| sdteqdtlpzmzozddtrp0(X0,sz10,xp) ) )
=> aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ) )
& aSet0(sbsmnsldt0(xS))
& ! [X3] :
( aElementOf0(X3,sbsmnsldt0(xS))
<=> ( aInteger0(X3)
& ? [X4] :
( aElementOf0(X4,xS)
& aElementOf0(X3,X4) ) ) )
& ! [X5] :
( aElementOf0(X5,stldt0(sbsmnsldt0(xS)))
<=> ( aInteger0(X5)
& ~ aElementOf0(X5,sbsmnsldt0(xS)) ) )
& ! [X6] :
( aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
=> aElementOf0(X6,stldt0(sbsmnsldt0(xS))) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ),
inference(rectify,[],[f46]) ).
fof(f56,plain,
( ? [X0] :
( aInteger0(X0)
& sdtasdt0(xp,X0) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)) )
& aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
& aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ? [X1] :
( aInteger0(X1)
& sdtasdt0(xp,X1) = sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)) )
& aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp)
& aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ),
inference(rectify,[],[f47]) ).
fof(f67,plain,
( aInteger0(xp)
& xp != sz00
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ! [X0] :
( ( ( aInteger0(X0)
& ? [X1] :
( aInteger0(X1)
& sdtasdt0(xp,X1) = sdtpldt0(X0,smndt0(sz10)) )
& aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(X0,sz10,xp) )
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aInteger0(X0)
| ( ! [X2] :
( ~ aInteger0(X2)
| sdtpldt0(X0,smndt0(sz10)) != sdtasdt0(xp,X2) )
& ~ aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
& ~ sdteqdtlpzmzozddtrp0(X0,sz10,xp) ) ) )
& aSet0(sbsmnsldt0(xS))
& ! [X3] :
( aElementOf0(X3,sbsmnsldt0(xS))
<=> ( aInteger0(X3)
& ? [X4] :
( aElementOf0(X4,xS)
& aElementOf0(X3,X4) ) ) )
& ! [X5] :
( aElementOf0(X5,stldt0(sbsmnsldt0(xS)))
<=> ( aInteger0(X5)
& ~ aElementOf0(X5,sbsmnsldt0(xS)) ) )
& ! [X6] :
( aElementOf0(X6,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ),
inference(ennf_transformation,[],[f55]) ).
fof(f68,plain,
( aInteger0(xp)
& xp != sz00
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ! [X0] :
( ( ( aInteger0(X0)
& ? [X1] :
( aInteger0(X1)
& sdtasdt0(xp,X1) = sdtpldt0(X0,smndt0(sz10)) )
& aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(X0,sz10,xp) )
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aInteger0(X0)
| ( ! [X2] :
( ~ aInteger0(X2)
| sdtpldt0(X0,smndt0(sz10)) != sdtasdt0(xp,X2) )
& ~ aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
& ~ sdteqdtlpzmzozddtrp0(X0,sz10,xp) ) ) )
& aSet0(sbsmnsldt0(xS))
& ! [X3] :
( aElementOf0(X3,sbsmnsldt0(xS))
<=> ( aInteger0(X3)
& ? [X4] :
( aElementOf0(X4,xS)
& aElementOf0(X3,X4) ) ) )
& ! [X5] :
( aElementOf0(X5,stldt0(sbsmnsldt0(xS)))
<=> ( aInteger0(X5)
& ~ aElementOf0(X5,sbsmnsldt0(xS)) ) )
& ! [X6] :
( aElementOf0(X6,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ),
inference(flattening,[],[f67]) ).
fof(f69,plain,
! [X0] :
( ( ( ~ aInteger0(X0)
| ( ! [X1] :
( ~ aInteger0(X1)
| sdtasdt0(xp,X1) != sdtpldt0(X0,smndt0(sz10)) )
& ~ aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
& ~ sdteqdtlpzmzozddtrp0(X0,sz10,xp) ) )
& ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
| ( ( X0 = sz10
| X0 = smndt0(sz10) )
& aElementOf0(X0,cS2200) ) ),
inference(ennf_transformation,[],[f51]) ).
fof(f74,plain,
! [X0] :
( aInteger0(smndt0(X0))
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f90,plain,
! [X0,X1] :
( aInteger0(sdtpldt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f91,plain,
! [X0,X1] :
( aInteger0(sdtpldt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f90]) ).
fof(f149,plain,
( aInteger0(xp)
& xp != sz00
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ! [X0] :
( ( ( aInteger0(X0)
& ? [X1] :
( aInteger0(X1)
& sdtasdt0(xp,X1) = sdtpldt0(X0,smndt0(sz10)) )
& aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(X0,sz10,xp) )
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aInteger0(X0)
| ( ! [X2] :
( ~ aInteger0(X2)
| sdtpldt0(X0,smndt0(sz10)) != sdtasdt0(xp,X2) )
& ~ aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
& ~ sdteqdtlpzmzozddtrp0(X0,sz10,xp) ) ) )
& aSet0(sbsmnsldt0(xS))
& ! [X3] :
( ( aElementOf0(X3,sbsmnsldt0(xS))
| ~ aInteger0(X3)
| ! [X4] :
( ~ aElementOf0(X4,xS)
| ~ aElementOf0(X3,X4) ) )
& ( ( aInteger0(X3)
& ? [X4] :
( aElementOf0(X4,xS)
& aElementOf0(X3,X4) ) )
| ~ aElementOf0(X3,sbsmnsldt0(xS)) ) )
& ! [X5] :
( ( aElementOf0(X5,stldt0(sbsmnsldt0(xS)))
| ~ aInteger0(X5)
| aElementOf0(X5,sbsmnsldt0(xS)) )
& ( ( aInteger0(X5)
& ~ aElementOf0(X5,sbsmnsldt0(xS)) )
| ~ aElementOf0(X5,stldt0(sbsmnsldt0(xS))) ) )
& ! [X6] :
( aElementOf0(X6,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ),
inference(nnf_transformation,[],[f68]) ).
fof(f150,plain,
( aInteger0(xp)
& xp != sz00
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ! [X0] :
( ( ( aInteger0(X0)
& ? [X1] :
( aInteger0(X1)
& sdtasdt0(xp,X1) = sdtpldt0(X0,smndt0(sz10)) )
& aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(X0,sz10,xp) )
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aInteger0(X0)
| ( ! [X2] :
( ~ aInteger0(X2)
| sdtpldt0(X0,smndt0(sz10)) != sdtasdt0(xp,X2) )
& ~ aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
& ~ sdteqdtlpzmzozddtrp0(X0,sz10,xp) ) ) )
& aSet0(sbsmnsldt0(xS))
& ! [X3] :
( ( aElementOf0(X3,sbsmnsldt0(xS))
| ~ aInteger0(X3)
| ! [X4] :
( ~ aElementOf0(X4,xS)
| ~ aElementOf0(X3,X4) ) )
& ( ( aInteger0(X3)
& ? [X4] :
( aElementOf0(X4,xS)
& aElementOf0(X3,X4) ) )
| ~ aElementOf0(X3,sbsmnsldt0(xS)) ) )
& ! [X5] :
( ( aElementOf0(X5,stldt0(sbsmnsldt0(xS)))
| ~ aInteger0(X5)
| aElementOf0(X5,sbsmnsldt0(xS)) )
& ( ( aInteger0(X5)
& ~ aElementOf0(X5,sbsmnsldt0(xS)) )
| ~ aElementOf0(X5,stldt0(sbsmnsldt0(xS))) ) )
& ! [X6] :
( aElementOf0(X6,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ),
inference(flattening,[],[f149]) ).
fof(f151,plain,
( aInteger0(xp)
& xp != sz00
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ! [X0] :
( ( ( aInteger0(X0)
& ? [X1] :
( aInteger0(X1)
& sdtasdt0(xp,X1) = sdtpldt0(X0,smndt0(sz10)) )
& aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(X0,sz10,xp) )
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aInteger0(X0)
| ( ! [X2] :
( ~ aInteger0(X2)
| sdtpldt0(X0,smndt0(sz10)) != sdtasdt0(xp,X2) )
& ~ aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
& ~ sdteqdtlpzmzozddtrp0(X0,sz10,xp) ) ) )
& aSet0(sbsmnsldt0(xS))
& ! [X3] :
( ( aElementOf0(X3,sbsmnsldt0(xS))
| ~ aInteger0(X3)
| ! [X4] :
( ~ aElementOf0(X4,xS)
| ~ aElementOf0(X3,X4) ) )
& ( ( aInteger0(X3)
& ? [X5] :
( aElementOf0(X5,xS)
& aElementOf0(X3,X5) ) )
| ~ aElementOf0(X3,sbsmnsldt0(xS)) ) )
& ! [X6] :
( ( aElementOf0(X6,stldt0(sbsmnsldt0(xS)))
| ~ aInteger0(X6)
| aElementOf0(X6,sbsmnsldt0(xS)) )
& ( ( aInteger0(X6)
& ~ aElementOf0(X6,sbsmnsldt0(xS)) )
| ~ aElementOf0(X6,stldt0(sbsmnsldt0(xS))) ) )
& ! [X7] :
( aElementOf0(X7,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ),
inference(rectify,[],[f150]) ).
fof(f152,plain,
( aInteger0(xp)
& xp != sz00
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ! [X0] :
( ( ( aInteger0(X0)
& aInteger0(sK16(X0))
& sdtpldt0(X0,smndt0(sz10)) = sdtasdt0(xp,sK16(X0))
& aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(X0,sz10,xp) )
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& ( aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aInteger0(X0)
| ( ! [X2] :
( ~ aInteger0(X2)
| sdtpldt0(X0,smndt0(sz10)) != sdtasdt0(xp,X2) )
& ~ aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10)))
& ~ sdteqdtlpzmzozddtrp0(X0,sz10,xp) ) ) )
& aSet0(sbsmnsldt0(xS))
& ! [X3] :
( ( aElementOf0(X3,sbsmnsldt0(xS))
| ~ aInteger0(X3)
| ! [X4] :
( ~ aElementOf0(X4,xS)
| ~ aElementOf0(X3,X4) ) )
& ( ( aInteger0(X3)
& aElementOf0(sK17(X3),xS)
& aElementOf0(X3,sK17(X3)) )
| ~ aElementOf0(X3,sbsmnsldt0(xS)) ) )
& ! [X6] :
( ( aElementOf0(X6,stldt0(sbsmnsldt0(xS)))
| ~ aInteger0(X6)
| aElementOf0(X6,sbsmnsldt0(xS)) )
& ( ( aInteger0(X6)
& ~ aElementOf0(X6,sbsmnsldt0(xS)) )
| ~ aElementOf0(X6,stldt0(sbsmnsldt0(xS))) ) )
& ! [X7] :
( aElementOf0(X7,stldt0(sbsmnsldt0(xS)))
| ~ aElementOf0(X7,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) )
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17]),skolemize(X1,sK16(X0)),skolemize(X5,sK17(X3))],[f151]) ).
fof(f153,plain,
( aInteger0(sK18)
& sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)) = sdtasdt0(xp,sK18)
& aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp)
& aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& aInteger0(sK19)
& sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)) = sdtasdt0(xp,sK19)
& aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))
& sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp)
& aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19]),skolemize(X0,sK18),skolemize(X1,sK19)],[f56]) ).
fof(f295,plain,
aInteger0(xp),
inference(cnf_transformation,[],[f152]) ).
fof(f297,plain,
sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp),
inference(cnf_transformation,[],[f153]) ).
fof(f302,plain,
sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp),
inference(cnf_transformation,[],[f153]) ).
fof(f306,plain,
sz10 != sdtpldt0(sz10,smndt0(xp)),
inference(cnf_transformation,[],[f48]) ).
fof(f307,plain,
sz10 != sdtpldt0(sz10,xp),
inference(cnf_transformation,[],[f48]) ).
fof(f308,plain,
( smndt0(sz10) != sdtpldt0(sz10,xp)
| smndt0(sz10) != sdtpldt0(sz10,smndt0(xp)) ),
inference(cnf_transformation,[],[f49]) ).
fof(f312,plain,
! [X0] :
( ~ sdteqdtlpzmzozddtrp0(X0,sz10,xp)
| ~ aInteger0(X0)
| sz10 = X0
| smndt0(sz10) = X0 ),
inference(cnf_transformation,[],[f69]) ).
fof(f327,plain,
! [X0] :
( aInteger0(smndt0(X0))
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f339,plain,
! [X0,X1] :
( aInteger0(sdtpldt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(cnf_transformation,[],[f91]) ).
fof(f361,plain,
aInteger0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f475,definition,
~ sP39(sz10),
introduced(definition,[new_symbols(definition,[sP39])],[inequality_splitting_name_introduction]) ).
fof(f476,plain,
sP39(sdtpldt0(sz10,xp)),
inference(inequality_splitting,[],[f307,f475]) ).
fof(f477,definition,
~ sP40(sz10),
introduced(definition,[new_symbols(definition,[sP40])],[inequality_splitting_name_introduction]) ).
fof(f478,plain,
sP40(sdtpldt0(sz10,smndt0(xp))),
inference(inequality_splitting,[],[f306,f477]) ).
fof(f479,definition,
~ sP41(smndt0(sz10)),
introduced(definition,[new_symbols(definition,[sP41])],[inequality_splitting_name_introduction]) ).
fof(f480,definition,
~ sP42(smndt0(sz10)),
introduced(definition,[new_symbols(definition,[sP42])],[inequality_splitting_name_introduction]) ).
fof(f481,plain,
( sP41(sdtpldt0(sz10,xp))
| sP42(sdtpldt0(sz10,smndt0(xp))) ),
inference(inequality_splitting,[],[f308,f480,f479]) ).
fof(f512,definition,
( spl52_1
<=> sP42(sdtpldt0(sz10,smndt0(xp))) ),
introduced(definition,[new_symbols(definition,[spl52_1])],[avatar_definition]) ).
fof(f514,plain,
( sP42(sdtpldt0(sz10,smndt0(xp)))
| ~ spl52_1 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f516,definition,
( spl52_2
<=> sP41(sdtpldt0(sz10,xp)) ),
introduced(definition,[new_symbols(definition,[spl52_2])],[avatar_definition]) ).
fof(f518,plain,
( sP41(sdtpldt0(sz10,xp))
| ~ spl52_2 ),
inference(avatar_component_clause,[],[f516]) ).
fof(f519,plain,
( spl52_1
| spl52_2 ),
inference(avatar_split_clause,[],[f481,f516,f512]) ).
fof(f1072,plain,
( ~ aInteger0(sdtpldt0(sz10,xp))
| sz10 = sdtpldt0(sz10,xp)
| smndt0(sz10) = sdtpldt0(sz10,xp) ),
inference(resolution,[],[f302,f312]) ).
fof(f1083,definition,
( spl52_55
<=> aInteger0(sdtpldt0(sz10,xp)) ),
introduced(definition,[new_symbols(definition,[spl52_55])],[avatar_definition]) ).
fof(f1085,plain,
( ~ aInteger0(sdtpldt0(sz10,xp))
| spl52_55 ),
inference(avatar_component_clause,[],[f1083]) ).
fof(f1088,definition,
( spl52_56
<=> smndt0(sz10) = sdtpldt0(sz10,xp) ),
introduced(definition,[new_symbols(definition,[spl52_56])],[avatar_definition]) ).
fof(f1090,plain,
( smndt0(sz10) = sdtpldt0(sz10,xp)
| ~ spl52_56 ),
inference(avatar_component_clause,[],[f1088]) ).
fof(f1092,definition,
( spl52_57
<=> sz10 = sdtpldt0(sz10,xp) ),
introduced(definition,[new_symbols(definition,[spl52_57])],[avatar_definition]) ).
fof(f1094,plain,
( sz10 = sdtpldt0(sz10,xp)
| ~ spl52_57 ),
inference(avatar_component_clause,[],[f1092]) ).
fof(f1095,plain,
( spl52_56
| spl52_57
| ~ spl52_55 ),
inference(avatar_split_clause,[],[f1072,f1083,f1092,f1088]) ).
fof(f1102,plain,
( ~ aInteger0(sz10)
| ~ aInteger0(xp)
| spl52_55 ),
inference(resolution,[],[f1085,f339]) ).
fof(f1103,plain,
( ~ aInteger0(xp)
| spl52_55 ),
inference(forward_subsumption_resolution,[],[f1102,f361]) ).
fof(f1104,plain,
( $false
| spl52_55 ),
inference(forward_subsumption_resolution,[],[f1103,f295]) ).
fof(f1105,plain,
spl52_55,
inference(avatar_contradiction_clause,[],[f1104]) ).
fof(f1161,plain,
( sP41(smndt0(sz10))
| ~ spl52_2
| ~ spl52_56 ),
inference(superposition,[],[f518,f1090]) ).
fof(f1170,plain,
( $false
| ~ spl52_2
| ~ spl52_56 ),
inference(forward_subsumption_resolution,[],[f1161,f479]) ).
fof(f1171,plain,
( ~ spl52_2
| ~ spl52_56 ),
inference(avatar_contradiction_clause,[],[f1170]) ).
fof(f1244,plain,
( sP39(sz10)
| ~ spl52_57 ),
inference(superposition,[],[f476,f1094]) ).
fof(f1252,plain,
( $false
| ~ spl52_57 ),
inference(forward_subsumption_resolution,[],[f1244,f475]) ).
fof(f1253,plain,
~ spl52_57,
inference(avatar_contradiction_clause,[],[f1252]) ).
fof(f1312,plain,
( ~ aInteger0(sdtpldt0(sz10,smndt0(xp)))
| sz10 = sdtpldt0(sz10,smndt0(xp))
| smndt0(sz10) = sdtpldt0(sz10,smndt0(xp)) ),
inference(resolution,[],[f297,f312]) ).
fof(f1323,definition,
( spl52_69
<=> aInteger0(sdtpldt0(sz10,smndt0(xp))) ),
introduced(definition,[new_symbols(definition,[spl52_69])],[avatar_definition]) ).
fof(f1325,plain,
( ~ aInteger0(sdtpldt0(sz10,smndt0(xp)))
| spl52_69 ),
inference(avatar_component_clause,[],[f1323]) ).
fof(f1328,definition,
( spl52_70
<=> smndt0(sz10) = sdtpldt0(sz10,smndt0(xp)) ),
introduced(definition,[new_symbols(definition,[spl52_70])],[avatar_definition]) ).
fof(f1330,plain,
( smndt0(sz10) = sdtpldt0(sz10,smndt0(xp))
| ~ spl52_70 ),
inference(avatar_component_clause,[],[f1328]) ).
fof(f1332,definition,
( spl52_71
<=> sz10 = sdtpldt0(sz10,smndt0(xp)) ),
introduced(definition,[new_symbols(definition,[spl52_71])],[avatar_definition]) ).
fof(f1334,plain,
( sz10 = sdtpldt0(sz10,smndt0(xp))
| ~ spl52_71 ),
inference(avatar_component_clause,[],[f1332]) ).
fof(f1335,plain,
( spl52_70
| spl52_71
| ~ spl52_69 ),
inference(avatar_split_clause,[],[f1312,f1323,f1332,f1328]) ).
fof(f1349,plain,
( ~ aInteger0(sz10)
| ~ aInteger0(smndt0(xp))
| spl52_69 ),
inference(resolution,[],[f1325,f339]) ).
fof(f1350,plain,
( ~ aInteger0(smndt0(xp))
| spl52_69 ),
inference(forward_subsumption_resolution,[],[f1349,f361]) ).
fof(f1439,plain,
( ~ aInteger0(xp)
| spl52_69 ),
inference(resolution,[],[f1350,f327]) ).
fof(f1440,plain,
( $false
| spl52_69 ),
inference(forward_subsumption_resolution,[],[f1439,f295]) ).
fof(f1441,plain,
spl52_69,
inference(avatar_contradiction_clause,[],[f1440]) ).
fof(f1703,plain,
( sP42(smndt0(sz10))
| ~ spl52_1
| ~ spl52_70 ),
inference(superposition,[],[f514,f1330]) ).
fof(f1723,plain,
( $false
| ~ spl52_1
| ~ spl52_70 ),
inference(forward_subsumption_resolution,[],[f1703,f480]) ).
fof(f1724,plain,
( ~ spl52_1
| ~ spl52_70 ),
inference(avatar_contradiction_clause,[],[f1723]) ).
fof(f1792,plain,
( sP40(sz10)
| ~ spl52_71 ),
inference(superposition,[],[f478,f1334]) ).
fof(f1813,plain,
( $false
| ~ spl52_71 ),
inference(forward_subsumption_resolution,[],[f1792,f477]) ).
fof(f1814,plain,
~ spl52_71,
inference(avatar_contradiction_clause,[],[f1813]) ).
cnf(s1,plain,
( spl52_1
| spl52_2 ),
inference(sat_conversion,[],[f519]) ).
cnf(s41,plain,
( ~ spl52_55
| spl52_56
| spl52_57 ),
inference(sat_conversion,[],[f1095]) ).
cnf(s42,plain,
spl52_55,
inference(sat_conversion,[],[f1105]) ).
cnf(s43,plain,
( ~ spl52_2
| ~ spl52_56 ),
inference(sat_conversion,[],[f1171]) ).
cnf(s48,plain,
~ spl52_57,
inference(sat_conversion,[],[f1253]) ).
cnf(s50,plain,
( ~ spl52_69
| spl52_70
| spl52_71 ),
inference(sat_conversion,[],[f1335]) ).
cnf(s58,plain,
spl52_69,
inference(sat_conversion,[],[f1441]) ).
cnf(s68,plain,
( ~ spl52_1
| ~ spl52_70 ),
inference(sat_conversion,[],[f1724]) ).
cnf(s72,plain,
~ spl52_71,
inference(sat_conversion,[],[f1814]) ).
cnf(s78,plain,
spl52_70,
inference(rat,[],[s50,s72,s58]) ).
cnf(s79,plain,
~ spl52_1,
inference(rat,[],[s68,s78]) ).
cnf(s81,plain,
spl52_56,
inference(rat,[],[s41,s48,s42]) ).
cnf(s82,plain,
~ spl52_2,
inference(rat,[],[s43,s81]) ).
cnf(s96,plain,
$false,
inference(rat,[],[s1,s82,s79]) ).
fof(f1830,plain,
$false,
inference(avatar_sat_refutation,[],[s96]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM455+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.36 % Computer : n016.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 20:04:02 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 Running first-order theorem proving
% 0.11/0.39 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.85/1.12 % (2957402)Detected formulas, will run a generic FOF schedule.
% 1.85/1.12 % (2957410)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2960914194:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 1.85/1.12 % (2957410)First to succeed.
% 1.85/1.12 % (2957410)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2957402"
% 1.85/1.12 % (2957408)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1805096981:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 1.85/1.12 % (2957407)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3276244261:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 1.85/1.12 % (2957412)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3628701363:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 1.85/1.12 % (2957409)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1161197763:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 1.85/1.12 % (2957411)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2194098017:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 1.85/1.12 % (2957413)dis-21_1_sil=8000:lcm=predicate:random_seed=1731382718:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 1.85/1.12 % (2957412)Also succeeded, but the first one will report.
% 1.85/1.12 % (2957413)Also succeeded, but the first one will report.
% 1.85/1.12 % (2957411)Also succeeded, but the first one will report.
% 1.85/1.12 % (2957410)Refutation found. Thanks to Tanya!
% 1.85/1.12 % SZS status Theorem for theBenchmark
% 1.85/1.12 % SZS output start Proof for theBenchmark
% See solution above
% 0.15/1.31 % (2957410)------------------------------
% 0.15/1.31 % (2957410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.15/1.31 % (2957410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/1.31 % (2957410)CaDiCaL version: 2.1.3
% 0.15/1.31 % (2957410)Termination reason: Refutation
% 0.15/1.31 % (2957410)Time elapsed: 0.021 s
% 0.15/1.31 % (2957410)Peak memory usage: 90 MB
% 0.15/1.31 % (2957410)Instructions burned: 53 (million)
% 0.15/1.31 % (2957410)------------------------------
% 0.15/1.31 % (2957410)------------------------------
% 0.15/1.31 % (2957402)Success in time 0.289 s
% 0.15/1.31 % Vampire exiting
%------------------------------------------------------------------------------