%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM453+6 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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:24:22 PM UTC 2026
% Result : Theorem 114.57s 26.68s
% Output : Refutation 114.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 37
% Syntax : Number of formulae : 292 ( 54 unt; 20 def)
% Number of atoms : 1066 ( 219 equ)
% Maximal formula atoms : 38 ( 3 avg)
% Number of connectives : 1128 ( 354 ~; 481 |; 226 &)
% ( 36 <=>; 31 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 21 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 8 con; 0-2 aty)
% Number of variables : 198 ( 0 sgn 162 !; 36 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aInteger0(sz00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIntZero) ).
fof(f3,axiom,
aInteger0(sz10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIntOne) ).
fof(f4,axiom,
! [X0] :
( aInteger0(X0)
=> aInteger0(smndt0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIntNeg) ).
fof(f5,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1) )
=> aInteger0(sdtpldt0(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIntPlus) ).
fof(f6,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1) )
=> aInteger0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIntMult) ).
fof(f7,axiom,
! [X0,X1,X2] :
( ( aInteger0(X0)
& aInteger0(X1)
& aInteger0(X2) )
=> sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddAsso) ).
fof(f8,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1) )
=> sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddComm) ).
fof(f9,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddZero) ).
fof(f10,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtpldt0(X0,smndt0(X0)) = sz00
& sz00 = sdtpldt0(smndt0(X0),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddNeg) ).
fof(f15,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulZero) ).
fof(f17,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1) )
=> ( sdtasdt0(X0,X1) = sz00
=> ( X0 = sz00
| X1 = sz00 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mZeroDiv) ).
fof(f18,axiom,
! [X0] :
( aInteger0(X0)
=> ! [X1] :
( aDivisorOf0(X1,X0)
<=> ( aInteger0(X1)
& X1 != sz00
& ? [X2] :
( aInteger0(X2)
& sdtasdt0(X1,X2) = X0 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDivisor) ).
fof(f42,axiom,
( aSet0(xS)
& ! [X0] :
( ( aElementOf0(X0,xS)
=> ? [X1] :
( aInteger0(X1)
& X1 != sz00
& isPrime0(X1)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X1))
& ! [X2] :
( ( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,X1))
=> ( aInteger0(X2)
& ? [X3] :
( aInteger0(X3)
& sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(sz00)) )
& aDivisorOf0(X1,sdtpldt0(X2,smndt0(sz00)))
& sdteqdtlpzmzozddtrp0(X2,sz00,X1) ) )
& ( ( aInteger0(X2)
& ( ? [X3] :
( aInteger0(X3)
& sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(sz00)) )
| aDivisorOf0(X1,sdtpldt0(X2,smndt0(sz00)))
| sdteqdtlpzmzozddtrp0(X2,sz00,X1) ) )
=> aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,X1)) ) )
& szAzrzSzezqlpdtcmdtrp0(sz00,X1) = X0 ) )
& ( ? [X1] :
( aInteger0(X1)
& X1 != sz00
& isPrime0(X1)
& ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X1))
& ! [X2] :
( ( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,X1))
=> ( aInteger0(X2)
& ? [X3] :
( aInteger0(X3)
& sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(sz00)) )
& aDivisorOf0(X1,sdtpldt0(X2,smndt0(sz00)))
& sdteqdtlpzmzozddtrp0(X2,sz00,X1) ) )
& ( ( aInteger0(X2)
& ( ? [X3] :
( aInteger0(X3)
& sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(sz00)) )
| aDivisorOf0(X1,sdtpldt0(X2,smndt0(sz00)))
| sdteqdtlpzmzozddtrp0(X2,sz00,X1) ) )
=> aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,X1)) ) ) )
=> szAzrzSzezqlpdtcmdtrp0(sz00,X1) = X0 ) )
=> aElementOf0(X0,xS) ) )
& xS = cS2043 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2046) ).
fof(f43,axiom,
( aSet0(sbsmnsldt0(xS))
& ! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
<=> ( aInteger0(X0)
& ? [X1] :
( aElementOf0(X1,xS)
& aElementOf0(X0,X1) ) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [X0] :
( aElementOf0(X0,stldt0(sbsmnsldt0(xS)))
<=> ( aInteger0(X0)
& ~ aElementOf0(X0,sbsmnsldt0(xS)) ) )
& ! [X0] :
( aElementOf0(X0,stldt0(sbsmnsldt0(xS)))
<=> ( X0 = sz10
| X0 = smndt0(sz10) ) )
& stldt0(sbsmnsldt0(xS)) = cS2076 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2079) ).
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/sandbox/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/sandbox/benchmark/theBenchmark.p',m__2232) ).
fof(f48,conjecture,
( sdtpldt0(sz10,xp) != sz10
& sdtpldt0(sz10,smndt0(xp)) != sz10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f49,negated_conjecture,
~ ( sdtpldt0(sz10,xp) != sz10
& sdtpldt0(sz10,smndt0(xp)) != sz10 ),
inference(negated_conjecture,[status(cth)],[f48]) ).
fof(f51,plain,
( aSet0(xS)
& ! [X0] :
( ( aElementOf0(X0,xS)
=> ? [X1] :
( aInteger0(X1)
& X1 != sz00
& isPrime0(X1)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X1))
& ! [X2] :
( ( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,X1))
=> ( aInteger0(X2)
& ? [X3] :
( aInteger0(X3)
& sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(sz00)) )
& aDivisorOf0(X1,sdtpldt0(X2,smndt0(sz00)))
& sdteqdtlpzmzozddtrp0(X2,sz00,X1) ) )
& ( ( aInteger0(X2)
& ( ? [X4] :
( aInteger0(X4)
& sdtpldt0(X2,smndt0(sz00)) = sdtasdt0(X1,X4) )
| aDivisorOf0(X1,sdtpldt0(X2,smndt0(sz00)))
| sdteqdtlpzmzozddtrp0(X2,sz00,X1) ) )
=> aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,X1)) ) )
& szAzrzSzezqlpdtcmdtrp0(sz00,X1) = X0 ) )
& ( ? [X5] :
( aInteger0(X5)
& sz00 != X5
& isPrime0(X5)
& ( ( aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X5))
& ! [X6] :
( ( aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(sz00,X5))
=> ( aInteger0(X6)
& ? [X7] :
( aInteger0(X7)
& sdtasdt0(X5,X7) = sdtpldt0(X6,smndt0(sz00)) )
& aDivisorOf0(X5,sdtpldt0(X6,smndt0(sz00)))
& sdteqdtlpzmzozddtrp0(X6,sz00,X5) ) )
& ( ( aInteger0(X6)
& ( ? [X8] :
( aInteger0(X8)
& sdtpldt0(X6,smndt0(sz00)) = sdtasdt0(X5,X8) )
| aDivisorOf0(X5,sdtpldt0(X6,smndt0(sz00)))
| sdteqdtlpzmzozddtrp0(X6,sz00,X5) ) )
=> aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(sz00,X5)) ) ) )
=> szAzrzSzezqlpdtcmdtrp0(sz00,X5) = X0 ) )
=> aElementOf0(X0,xS) ) )
& xS = cS2043 ),
inference(rectify,[],[f42]) ).
fof(f52,plain,
( aSet0(sbsmnsldt0(xS))
& ! [X0] :
( aElementOf0(X0,sbsmnsldt0(xS))
<=> ( aInteger0(X0)
& ? [X1] :
( aElementOf0(X1,xS)
& aElementOf0(X0,X1) ) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [X2] :
( aElementOf0(X2,stldt0(sbsmnsldt0(xS)))
<=> ( aInteger0(X2)
& ~ aElementOf0(X2,sbsmnsldt0(xS)) ) )
& ! [X3] :
( aElementOf0(X3,stldt0(sbsmnsldt0(xS)))
<=> ( sz10 = X3
| smndt0(sz10) = X3 ) )
& stldt0(sbsmnsldt0(xS)) = cS2076 ),
inference(rectify,[],[f43]) ).
fof(f54,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(f55,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(f57,plain,
! [X0] :
( aInteger0(smndt0(X0))
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f58,plain,
! [X0,X1] :
( aInteger0(sdtpldt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f59,plain,
! [X0,X1] :
( aInteger0(sdtpldt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f58]) ).
fof(f60,plain,
! [X0,X1] :
( aInteger0(sdtasdt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f6]) ).
fof(f61,plain,
! [X0,X1] :
( aInteger0(sdtasdt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f60]) ).
fof(f62,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f63,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(flattening,[],[f62]) ).
fof(f64,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f65,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f64]) ).
fof(f66,plain,
! [X0] :
( ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f67,plain,
! [X0] :
( ( sdtpldt0(X0,smndt0(X0)) = sz00
& sz00 = sdtpldt0(smndt0(X0),X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f75,plain,
! [X0] :
( ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f77,plain,
! [X0,X1] :
( X0 = sz00
| X1 = sz00
| sz00 != sdtasdt0(X0,X1)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f78,plain,
! [X0,X1] :
( X0 = sz00
| X1 = sz00
| sz00 != sdtasdt0(X0,X1)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f77]) ).
fof(f79,plain,
! [X0] :
( ! [X1] :
( aDivisorOf0(X1,X0)
<=> ( aInteger0(X1)
& X1 != sz00
& ? [X2] :
( aInteger0(X2)
& sdtasdt0(X1,X2) = X0 ) ) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f119,plain,
( aSet0(xS)
& ! [X0] :
( ( ? [X1] :
( aInteger0(X1)
& X1 != sz00
& isPrime0(X1)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X1))
& ! [X2] :
( ( ( aInteger0(X2)
& ? [X3] :
( aInteger0(X3)
& sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(sz00)) )
& aDivisorOf0(X1,sdtpldt0(X2,smndt0(sz00)))
& sdteqdtlpzmzozddtrp0(X2,sz00,X1) )
| ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,X1)) )
& ( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,X1))
| ~ aInteger0(X2)
| ( ! [X4] :
( ~ aInteger0(X4)
| sdtpldt0(X2,smndt0(sz00)) != sdtasdt0(X1,X4) )
& ~ aDivisorOf0(X1,sdtpldt0(X2,smndt0(sz00)))
& ~ sdteqdtlpzmzozddtrp0(X2,sz00,X1) ) ) )
& szAzrzSzezqlpdtcmdtrp0(sz00,X1) = X0 )
| ~ aElementOf0(X0,xS) )
& ( aElementOf0(X0,xS)
| ! [X5] :
( ~ aInteger0(X5)
| sz00 = X5
| ~ isPrime0(X5)
| ( szAzrzSzezqlpdtcmdtrp0(sz00,X5) != X0
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X5))
& ! [X6] :
( ( ( aInteger0(X6)
& ? [X7] :
( aInteger0(X7)
& sdtasdt0(X5,X7) = sdtpldt0(X6,smndt0(sz00)) )
& aDivisorOf0(X5,sdtpldt0(X6,smndt0(sz00)))
& sdteqdtlpzmzozddtrp0(X6,sz00,X5) )
| ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(sz00,X5)) )
& ( aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(sz00,X5))
| ~ aInteger0(X6)
| ( ! [X8] :
( ~ aInteger0(X8)
| sdtpldt0(X6,smndt0(sz00)) != sdtasdt0(X5,X8) )
& ~ aDivisorOf0(X5,sdtpldt0(X6,smndt0(sz00)))
& ~ sdteqdtlpzmzozddtrp0(X6,sz00,X5) ) ) ) ) ) ) )
& xS = cS2043 ),
inference(ennf_transformation,[],[f51]) ).
fof(f120,plain,
( aSet0(xS)
& ! [X0] :
( ( ? [X1] :
( aInteger0(X1)
& X1 != sz00
& isPrime0(X1)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X1))
& ! [X2] :
( ( ( aInteger0(X2)
& ? [X3] :
( aInteger0(X3)
& sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(sz00)) )
& aDivisorOf0(X1,sdtpldt0(X2,smndt0(sz00)))
& sdteqdtlpzmzozddtrp0(X2,sz00,X1) )
| ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,X1)) )
& ( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,X1))
| ~ aInteger0(X2)
| ( ! [X4] :
( ~ aInteger0(X4)
| sdtpldt0(X2,smndt0(sz00)) != sdtasdt0(X1,X4) )
& ~ aDivisorOf0(X1,sdtpldt0(X2,smndt0(sz00)))
& ~ sdteqdtlpzmzozddtrp0(X2,sz00,X1) ) ) )
& szAzrzSzezqlpdtcmdtrp0(sz00,X1) = X0 )
| ~ aElementOf0(X0,xS) )
& ( aElementOf0(X0,xS)
| ! [X5] :
( ~ aInteger0(X5)
| sz00 = X5
| ~ isPrime0(X5)
| ( szAzrzSzezqlpdtcmdtrp0(sz00,X5) != X0
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X5))
& ! [X6] :
( ( ( aInteger0(X6)
& ? [X7] :
( aInteger0(X7)
& sdtasdt0(X5,X7) = sdtpldt0(X6,smndt0(sz00)) )
& aDivisorOf0(X5,sdtpldt0(X6,smndt0(sz00)))
& sdteqdtlpzmzozddtrp0(X6,sz00,X5) )
| ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(sz00,X5)) )
& ( aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(sz00,X5))
| ~ aInteger0(X6)
| ( ! [X8] :
( ~ aInteger0(X8)
| sdtpldt0(X6,smndt0(sz00)) != sdtasdt0(X5,X8) )
& ~ aDivisorOf0(X5,sdtpldt0(X6,smndt0(sz00)))
& ~ sdteqdtlpzmzozddtrp0(X6,sz00,X5) ) ) ) ) ) ) )
& xS = cS2043 ),
inference(flattening,[],[f119]) ).
fof(f123,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,[],[f54]) ).
fof(f124,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,[],[f123]) ).
fof(f125,plain,
( sz10 = sdtpldt0(sz10,xp)
| sz10 = sdtpldt0(sz10,smndt0(xp)) ),
inference(ennf_transformation,[],[f49]) ).
fof(f126,plain,
aInteger0(sz00),
inference(cnf_transformation,[],[f2]) ).
fof(f127,plain,
aInteger0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f128,plain,
! [X0] :
( ~ aInteger0(X0)
| aInteger0(smndt0(X0)) ),
inference(cnf_transformation,[],[f57]) ).
fof(f129,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| aInteger0(sdtpldt0(X0,X1)) ),
inference(cnf_transformation,[],[f59]) ).
fof(f130,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| aInteger0(sdtasdt0(X0,X1)) ),
inference(cnf_transformation,[],[f61]) ).
fof(f131,plain,
! [X2,X0,X1] :
( ~ aInteger0(X2)
| ~ aInteger0(X1)
| ~ aInteger0(X0)
| sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2) ),
inference(cnf_transformation,[],[f63]) ).
fof(f132,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ),
inference(cnf_transformation,[],[f65]) ).
fof(f133,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(sz00,X0) = X0 ),
inference(cnf_transformation,[],[f66]) ).
fof(f134,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,sz00) = X0 ),
inference(cnf_transformation,[],[f66]) ).
fof(f135,plain,
! [X0] :
( ~ aInteger0(X0)
| sz00 = sdtpldt0(smndt0(X0),X0) ),
inference(cnf_transformation,[],[f67]) ).
fof(f136,plain,
! [X0] :
( ~ aInteger0(X0)
| sz00 = sdtpldt0(X0,smndt0(X0)) ),
inference(cnf_transformation,[],[f67]) ).
fof(f144,plain,
! [X0] :
( ~ aInteger0(X0)
| sz00 = sdtasdt0(X0,sz00) ),
inference(cnf_transformation,[],[f75]) ).
fof(f147,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| sz00 != sdtasdt0(X0,X1)
| sz00 = X1
| sz00 = X0 ),
inference(cnf_transformation,[],[f78]) ).
fof(f148,plain,
! [X2,X0,X1] :
( ~ aInteger0(X0)
| sdtasdt0(X1,X2) != X0
| ~ aInteger0(X2)
| sz00 = X1
| ~ aInteger0(X1)
| aDivisorOf0(X1,X0) ),
inference(cnf_transformation,[],[f79]) ).
fof(f149,plain,
! [X0,X1] :
( ~ aInteger0(X0)
| sdtasdt0(X1,sK0(X0,X1)) = X0
| ~ aDivisorOf0(X1,X0) ),
inference(cnf_transformation,[],[f79]) ).
fof(f150,plain,
! [X0,X1] :
( ~ aInteger0(X0)
| aInteger0(sK0(X0,X1))
| ~ aDivisorOf0(X1,X0) ),
inference(cnf_transformation,[],[f79]) ).
fof(f151,plain,
! [X0,X1] :
( ~ aInteger0(X0)
| sz00 != X1
| ~ aDivisorOf0(X1,X0) ),
inference(cnf_transformation,[],[f79]) ).
fof(f256,plain,
xS = cS2043,
inference(cnf_transformation,[],[f120]) ).
fof(f263,plain,
! [X2] :
( aInteger0(X2)
| ~ aElementOf0(X2,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[],[f52]) ).
fof(f266,plain,
! [X3] :
( smndt0(sz10) != X3
| aElementOf0(X3,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[],[f52]) ).
fof(f268,plain,
stldt0(sbsmnsldt0(xS)) = cS2076,
inference(cnf_transformation,[],[f52]) ).
fof(f324,plain,
! [X0] :
( ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| aInteger0(X0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f335,plain,
sz00 != xp,
inference(cnf_transformation,[],[f124]) ).
fof(f336,plain,
aInteger0(xp),
inference(cnf_transformation,[],[f124]) ).
fof(f337,plain,
sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)) = sdtasdt0(xp,sK28),
inference(cnf_transformation,[],[f55]) ).
fof(f338,plain,
aInteger0(sK28),
inference(cnf_transformation,[],[f55]) ).
fof(f339,plain,
sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)) = sdtasdt0(xp,sK27),
inference(cnf_transformation,[],[f55]) ).
fof(f344,plain,
aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp)),
inference(cnf_transformation,[],[f55]) ).
fof(f346,plain,
aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))),
inference(cnf_transformation,[],[f55]) ).
fof(f347,plain,
( sz10 = sdtpldt0(sz10,smndt0(xp))
| sz10 = sdtpldt0(sz10,xp) ),
inference(cnf_transformation,[],[f125]) ).
fof(f374,plain,
cS2076 = stldt0(sbsmnsldt0(cS2043)),
inference(definition_unfolding,[],[f268,f256]) ).
fof(f376,plain,
! [X3] :
( smndt0(sz10) != X3
| aElementOf0(X3,stldt0(sbsmnsldt0(cS2043))) ),
inference(definition_unfolding,[],[f266,f256]) ).
fof(f379,plain,
! [X2] :
( aInteger0(X2)
| ~ aElementOf0(X2,stldt0(sbsmnsldt0(cS2043))) ),
inference(definition_unfolding,[],[f263,f256]) ).
fof(f440,plain,
! [X0] :
( ~ aInteger0(X0)
| ~ aDivisorOf0(sz00,X0) ),
inference(equality_resolution,[],[f151]) ).
fof(f441,plain,
! [X2,X1] :
( ~ aInteger0(sdtasdt0(X1,X2))
| ~ aInteger0(X2)
| sz00 = X1
| ~ aInteger0(X1)
| aDivisorOf0(X1,sdtasdt0(X1,X2)) ),
inference(equality_resolution,[],[f148]) ).
fof(f474,plain,
aElementOf0(smndt0(sz10),stldt0(sbsmnsldt0(cS2043))),
inference(equality_resolution,[],[f376]) ).
fof(f475,plain,
~ aInteger0(sz00),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f476,plain,
~ aInteger0(sz10),
inference(consistent_polarity_flipping,[],[f127]) ).
fof(f477,plain,
! [X0] :
( ~ aInteger0(smndt0(X0))
| aInteger0(X0) ),
inference(consistent_polarity_flipping,[],[f128]) ).
fof(f478,plain,
! [X0,X1] :
( ~ aInteger0(sdtpldt0(X0,X1))
| aInteger0(X0)
| aInteger0(X1) ),
inference(consistent_polarity_flipping,[],[f129]) ).
fof(f479,plain,
! [X0,X1] :
( ~ aInteger0(sdtasdt0(X0,X1))
| aInteger0(X0)
| aInteger0(X1) ),
inference(consistent_polarity_flipping,[],[f130]) ).
fof(f480,plain,
! [X2,X0,X1] :
( aInteger0(X2)
| aInteger0(X1)
| aInteger0(X0)
| sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2) ),
inference(consistent_polarity_flipping,[],[f131]) ).
fof(f481,plain,
! [X0,X1] :
( aInteger0(X1)
| aInteger0(X0)
| sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ),
inference(consistent_polarity_flipping,[],[f132]) ).
fof(f482,plain,
! [X0] :
( aInteger0(X0)
| sdtpldt0(X0,sz00) = X0 ),
inference(consistent_polarity_flipping,[],[f134]) ).
fof(f483,plain,
! [X0] :
( aInteger0(X0)
| sdtpldt0(sz00,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f133]) ).
fof(f484,plain,
! [X0] :
( aInteger0(X0)
| sz00 = sdtpldt0(X0,smndt0(X0)) ),
inference(consistent_polarity_flipping,[],[f136]) ).
fof(f485,plain,
! [X0] :
( aInteger0(X0)
| sz00 = sdtpldt0(smndt0(X0),X0) ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f492,plain,
! [X0] :
( aInteger0(X0)
| sz00 = sdtasdt0(X0,sz00) ),
inference(consistent_polarity_flipping,[],[f144]) ).
fof(f496,plain,
! [X0,X1] :
( sz00 != sdtasdt0(X0,X1)
| aInteger0(X0)
| aInteger0(X1)
| sz00 = X1
| sz00 = X0 ),
inference(consistent_polarity_flipping,[],[f147]) ).
fof(f498,plain,
! [X0] :
( ~ aDivisorOf0(sz00,X0)
| aInteger0(X0) ),
inference(consistent_polarity_flipping,[],[f440]) ).
fof(f499,plain,
! [X0,X1] :
( ~ aDivisorOf0(X1,X0)
| ~ aInteger0(sK0(X0,X1))
| aInteger0(X0) ),
inference(consistent_polarity_flipping,[],[f150]) ).
fof(f500,plain,
! [X0,X1] :
( ~ aDivisorOf0(X1,X0)
| sdtasdt0(X1,sK0(X0,X1)) = X0
| aInteger0(X0) ),
inference(consistent_polarity_flipping,[],[f149]) ).
fof(f501,plain,
! [X2,X1] :
( aInteger0(sdtasdt0(X1,X2))
| aInteger0(X2)
| sz00 = X1
| aInteger0(X1)
| aDivisorOf0(X1,sdtasdt0(X1,X2)) ),
inference(consistent_polarity_flipping,[],[f441]) ).
fof(f601,plain,
~ aElementOf0(smndt0(sz10),stldt0(sbsmnsldt0(cS2043))),
inference(consistent_polarity_flipping,[],[f474]) ).
fof(f604,plain,
! [X2] :
( ~ aInteger0(X2)
| aElementOf0(X2,stldt0(sbsmnsldt0(cS2043))) ),
inference(consistent_polarity_flipping,[],[f379]) ).
fof(f653,plain,
~ aInteger0(xp),
inference(consistent_polarity_flipping,[],[f336]) ).
fof(f661,plain,
! [X0] :
( aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))
| ~ aInteger0(X0) ),
inference(consistent_polarity_flipping,[],[f324]) ).
fof(f670,plain,
~ aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp)),
inference(consistent_polarity_flipping,[],[f344]) ).
fof(f673,plain,
~ aInteger0(sK28),
inference(consistent_polarity_flipping,[],[f338]) ).
fof(f675,definition,
( spl29_1
<=> sz10 = sdtpldt0(sz10,xp) ),
introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).
fof(f677,plain,
( sz10 = sdtpldt0(sz10,xp)
| ~ spl29_1 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f679,definition,
( spl29_2
<=> sz10 = sdtpldt0(sz10,smndt0(xp)) ),
introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).
fof(f681,plain,
( sz10 = sdtpldt0(sz10,smndt0(xp))
| ~ spl29_2 ),
inference(avatar_component_clause,[],[f679]) ).
fof(f682,plain,
( spl29_1
| spl29_2 ),
inference(avatar_split_clause,[],[f347,f679,f675]) ).
fof(f726,definition,
( spl29_14
<=> aInteger0(sz10) ),
introduced(definition,[new_symbols(definition,[spl29_14])],[avatar_definition]) ).
fof(f727,plain,
( ~ aInteger0(sz10)
| spl29_14 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f734,definition,
( spl29_16
<=> aInteger0(smndt0(sz10)) ),
introduced(definition,[new_symbols(definition,[spl29_16])],[avatar_definition]) ).
fof(f735,plain,
( ~ aInteger0(smndt0(sz10))
| spl29_16 ),
inference(avatar_component_clause,[],[f734]) ).
fof(f736,plain,
( aInteger0(smndt0(sz10))
| ~ spl29_16 ),
inference(avatar_component_clause,[],[f734]) ).
fof(f738,plain,
~ spl29_14,
inference(avatar_split_clause,[],[f476,f726]) ).
fof(f744,plain,
~ aElementOf0(smndt0(sz10),cS2076),
inference(forward_demodulation,[],[f601,f374]) ).
fof(f748,plain,
! [X2] :
( ~ aInteger0(X2)
| aElementOf0(X2,cS2076) ),
inference(forward_demodulation,[],[f604,f374]) ).
fof(f752,plain,
~ aInteger0(sdtpldt0(sz10,xp)),
inference(resolution,[],[f670,f661]) ).
fof(f755,plain,
sz00 = sdtpldt0(sz00,sz00),
inference(resolution,[],[f482,f475]) ).
fof(f759,plain,
xp = sdtpldt0(xp,sz00),
inference(resolution,[],[f482,f653]) ).
fof(f768,plain,
xp = sdtpldt0(sz00,xp),
inference(resolution,[],[f483,f653]) ).
fof(f795,plain,
sz00 = sdtasdt0(xp,sz00),
inference(resolution,[],[f492,f653]) ).
fof(f852,plain,
( sz00 = sdtpldt0(sz10,smndt0(sz10))
| spl29_14 ),
inference(resolution,[],[f484,f727]) ).
fof(f857,plain,
sz00 = sdtpldt0(xp,smndt0(xp)),
inference(resolution,[],[f484,f653]) ).
fof(f865,plain,
( sz00 = sdtpldt0(smndt0(sz10),sz10)
| spl29_14 ),
inference(resolution,[],[f485,f727]) ).
fof(f970,plain,
aDivisorOf0(xp,sdtasdt0(xp,sK28)),
inference(superposition,[],[f346,f337]) ).
fof(f971,plain,
( ~ aInteger0(sdtasdt0(xp,sK28))
| aInteger0(sdtpldt0(sz10,xp))
| aInteger0(smndt0(sz10)) ),
inference(superposition,[],[f478,f337]) ).
fof(f972,plain,
( ~ aInteger0(sdtasdt0(xp,sK28))
| aInteger0(smndt0(sz10)) ),
inference(forward_subsumption_resolution,[],[f971,f752]) ).
fof(f974,definition,
( spl29_21
<=> aInteger0(sdtasdt0(xp,sK28)) ),
introduced(definition,[new_symbols(definition,[spl29_21])],[avatar_definition]) ).
fof(f976,plain,
( ~ aInteger0(sdtasdt0(xp,sK28))
| spl29_21 ),
inference(avatar_component_clause,[],[f974]) ).
fof(f977,plain,
( spl29_16
| ~ spl29_21 ),
inference(avatar_split_clause,[],[f972,f974,f734]) ).
fof(f985,plain,
( sdtasdt0(xp,sK27) = sdtpldt0(sz10,smndt0(sz10))
| ~ spl29_2 ),
inference(forward_demodulation,[],[f339,f681]) ).
fof(f996,plain,
( ~ aInteger0(sdtasdt0(xp,sK27))
| aInteger0(sz10)
| aInteger0(smndt0(sz10))
| ~ spl29_2 ),
inference(superposition,[],[f478,f985]) ).
fof(f997,plain,
( ~ aInteger0(sdtasdt0(xp,sK27))
| aInteger0(smndt0(sz10))
| ~ spl29_2
| spl29_14 ),
inference(forward_subsumption_resolution,[],[f996,f727]) ).
fof(f999,definition,
( spl29_22
<=> aInteger0(sdtasdt0(xp,sK27)) ),
introduced(definition,[new_symbols(definition,[spl29_22])],[avatar_definition]) ).
fof(f1001,plain,
( ~ aInteger0(sdtasdt0(xp,sK27))
| spl29_22 ),
inference(avatar_component_clause,[],[f999]) ).
fof(f1002,plain,
( spl29_16
| ~ spl29_22
| ~ spl29_2
| spl29_14 ),
inference(avatar_split_clause,[],[f997,f726,f679,f999,f734]) ).
fof(f1060,plain,
( ! [X0] :
( aInteger0(X0)
| sdtpldt0(X0,sz10) = sdtpldt0(sz10,X0) )
| spl29_14 ),
inference(resolution,[],[f481,f727]) ).
fof(f1216,definition,
( spl29_23
<=> sdtasdt0(xp,sK28) = sdtasdt0(xp,sK0(sdtasdt0(xp,sK28),xp)) ),
introduced(definition,[new_symbols(definition,[spl29_23])],[avatar_definition]) ).
fof(f1218,plain,
( sdtasdt0(xp,sK28) = sdtasdt0(xp,sK0(sdtasdt0(xp,sK28),xp))
| ~ spl29_23 ),
inference(avatar_component_clause,[],[f1216]) ).
fof(f1222,plain,
( aElementOf0(smndt0(sz10),cS2076)
| ~ spl29_16 ),
inference(resolution,[],[f736,f748]) ).
fof(f1223,plain,
( $false
| ~ spl29_16 ),
inference(forward_subsumption_resolution,[],[f1222,f744]) ).
fof(f1224,plain,
~ spl29_16,
inference(avatar_contradiction_clause,[],[f1223]) ).
fof(f1269,plain,
( sdtasdt0(xp,sK28) = sdtpldt0(sz10,smndt0(sz10))
| ~ spl29_1 ),
inference(superposition,[],[f337,f677]) ).
fof(f1432,definition,
( spl29_33
<=> aInteger0(sK0(sdtasdt0(xp,sK28),xp)) ),
introduced(definition,[new_symbols(definition,[spl29_33])],[avatar_definition]) ).
fof(f1434,plain,
( ~ aInteger0(sK0(sdtasdt0(xp,sK28),xp))
| spl29_33 ),
inference(avatar_component_clause,[],[f1432]) ).
fof(f1511,definition,
( spl29_35
<=> sz00 = sdtasdt0(xp,sK27) ),
introduced(definition,[new_symbols(definition,[spl29_35])],[avatar_definition]) ).
fof(f1513,plain,
( sz00 = sdtasdt0(xp,sK27)
| ~ spl29_35 ),
inference(avatar_component_clause,[],[f1511]) ).
fof(f1525,definition,
( spl29_38
<=> sz00 = sdtasdt0(xp,sK28) ),
introduced(definition,[new_symbols(definition,[spl29_38])],[avatar_definition]) ).
fof(f1526,plain,
( sz00 = sdtasdt0(xp,sK28)
| ~ spl29_38 ),
inference(avatar_component_clause,[],[f1525]) ).
fof(f1632,plain,
! [X2,X1] :
( aDivisorOf0(X1,sdtasdt0(X1,X2))
| sz00 = X1
| aInteger0(X1)
| aInteger0(X2) ),
inference(forward_subsumption_resolution,[],[f501,f479]) ).
fof(f1735,definition,
( spl29_59
<=> sz00 = sK28 ),
introduced(definition,[new_symbols(definition,[spl29_59])],[avatar_definition]) ).
fof(f1737,plain,
( sz00 = sK28
| ~ spl29_59 ),
inference(avatar_component_clause,[],[f1735]) ).
fof(f1792,definition,
( spl29_70
<=> sz00 = sK0(sdtasdt0(xp,sK28),xp) ),
introduced(definition,[new_symbols(definition,[spl29_70])],[avatar_definition]) ).
fof(f1794,plain,
( sz00 = sK0(sdtasdt0(xp,sK28),xp)
| ~ spl29_70 ),
inference(avatar_component_clause,[],[f1792]) ).
fof(f1797,definition,
( spl29_71
<=> aDivisorOf0(sK0(sdtasdt0(xp,sK28),xp),sz00) ),
introduced(definition,[new_symbols(definition,[spl29_71])],[avatar_definition]) ).
fof(f1798,plain,
( ~ aDivisorOf0(sK0(sdtasdt0(xp,sK28),xp),sz00)
| spl29_71 ),
inference(avatar_component_clause,[],[f1797]) ).
fof(f1799,plain,
( aDivisorOf0(sK0(sdtasdt0(xp,sK28),xp),sz00)
| ~ spl29_71 ),
inference(avatar_component_clause,[],[f1797]) ).
fof(f1969,plain,
( ! [X0,X1] :
( aInteger0(X0)
| aInteger0(X1)
| sdtpldt0(X1,sdtpldt0(sz10,X0)) = sdtpldt0(sdtpldt0(X1,sz10),X0) )
| spl29_14 ),
inference(resolution,[],[f480,f727]) ).
fof(f1997,plain,
! [X0,X1] :
( aInteger0(X0)
| aInteger0(X1)
| sdtpldt0(xp,sdtpldt0(X1,X0)) = sdtpldt0(sdtpldt0(xp,X1),X0) ),
inference(resolution,[],[f480,f653]) ).
fof(f2146,plain,
( sz00 != sz00
| aInteger0(xp)
| aInteger0(sK28)
| sz00 = sK28
| sz00 = xp
| ~ spl29_38 ),
inference(superposition,[],[f496,f1526]) ).
fof(f2148,plain,
( aInteger0(xp)
| aInteger0(sK28)
| sz00 = sK28
| sz00 = xp
| ~ spl29_38 ),
inference(trivial_inequality_removal,[],[f2146]) ).
fof(f2149,plain,
( aInteger0(sK28)
| sz00 = sK28
| sz00 = xp
| ~ spl29_38 ),
inference(forward_subsumption_resolution,[],[f2148,f653]) ).
fof(f2151,plain,
( sz00 = sK28
| sz00 = xp
| ~ spl29_38 ),
inference(forward_subsumption_resolution,[],[f2149,f673]) ).
fof(f2153,plain,
( sz00 = sK28
| ~ spl29_38 ),
inference(forward_subsumption_resolution,[],[f2151,f335]) ).
fof(f2155,plain,
( spl29_59
| ~ spl29_38 ),
inference(avatar_split_clause,[],[f2153,f1525,f1735]) ).
fof(f3291,definition,
( spl29_121
<=> sz00 = sK0(sz00,xp) ),
introduced(definition,[new_symbols(definition,[spl29_121])],[avatar_definition]) ).
fof(f3293,plain,
( sz00 = sK0(sz00,xp)
| ~ spl29_121 ),
inference(avatar_component_clause,[],[f3291]) ).
fof(f4009,plain,
( sdtasdt0(xp,sK28) = sdtasdt0(xp,sK0(sdtasdt0(xp,sK28),xp))
| aInteger0(sdtasdt0(xp,sK28)) ),
inference(resolution,[],[f970,f500]) ).
fof(f4010,plain,
( ~ aInteger0(sK0(sdtasdt0(xp,sK28),xp))
| aInteger0(sdtasdt0(xp,sK28)) ),
inference(resolution,[],[f970,f499]) ).
fof(f4012,plain,
( sdtasdt0(xp,sK28) = sdtasdt0(xp,sK0(sdtasdt0(xp,sK28),xp))
| spl29_21 ),
inference(forward_subsumption_resolution,[],[f4009,f976]) ).
fof(f4013,plain,
( spl29_23
| spl29_21 ),
inference(avatar_split_clause,[],[f4012,f974,f1216]) ).
fof(f4080,plain,
( ~ aInteger0(sK0(sdtasdt0(xp,sK28),xp))
| spl29_21 ),
inference(forward_subsumption_resolution,[],[f4010,f976]) ).
fof(f4081,plain,
( ~ spl29_33
| spl29_21 ),
inference(avatar_split_clause,[],[f4080,f974,f1432]) ).
fof(f4262,plain,
( sz00 = sdtasdt0(xp,sK27)
| ~ spl29_2
| spl29_14 ),
inference(superposition,[],[f985,f852]) ).
fof(f4411,plain,
( spl29_35
| ~ spl29_2
| spl29_14 ),
inference(avatar_split_clause,[],[f4262,f726,f679,f1511]) ).
fof(f7954,definition,
( spl29_275
<=> aInteger0(smndt0(xp)) ),
introduced(definition,[new_symbols(definition,[spl29_275])],[avatar_definition]) ).
fof(f7955,plain,
( ~ aInteger0(smndt0(xp))
| spl29_275 ),
inference(avatar_component_clause,[],[f7954]) ).
fof(f7956,plain,
( aInteger0(smndt0(xp))
| ~ spl29_275 ),
inference(avatar_component_clause,[],[f7954]) ).
fof(f7968,plain,
( aInteger0(xp)
| ~ spl29_275 ),
inference(resolution,[],[f7956,f477]) ).
fof(f7970,plain,
( $false
| ~ spl29_275 ),
inference(forward_subsumption_resolution,[],[f7968,f653]) ).
fof(f7971,plain,
~ spl29_275,
inference(avatar_contradiction_clause,[],[f7970]) ).
fof(f8013,plain,
( sdtpldt0(sz10,smndt0(xp)) = sdtpldt0(smndt0(xp),sz10)
| spl29_14
| spl29_275 ),
inference(resolution,[],[f7955,f1060]) ).
fof(f8023,plain,
( sz10 = sdtpldt0(smndt0(xp),sz10)
| ~ spl29_2
| spl29_14
| spl29_275 ),
inference(forward_demodulation,[],[f8013,f681]) ).
fof(f8539,plain,
( sdtasdt0(xp,sK28) = sdtasdt0(xp,sz00)
| ~ spl29_23
| ~ spl29_70 ),
inference(forward_demodulation,[],[f1218,f1794]) ).
fof(f8605,plain,
( sz00 != sdtasdt0(xp,sK28)
| aInteger0(xp)
| aInteger0(sK0(sdtasdt0(xp,sK28),xp))
| sz00 = sK0(sdtasdt0(xp,sK28),xp)
| sz00 = xp
| ~ spl29_23 ),
inference(superposition,[],[f496,f1218]) ).
fof(f8607,plain,
( sz00 != sdtasdt0(xp,sK28)
| aInteger0(sK0(sdtasdt0(xp,sK28),xp))
| sz00 = sK0(sdtasdt0(xp,sK28),xp)
| sz00 = xp
| ~ spl29_23 ),
inference(forward_subsumption_resolution,[],[f8605,f653]) ).
fof(f8611,plain,
( sz00 != sdtasdt0(xp,sK28)
| sz00 = sK0(sdtasdt0(xp,sK28),xp)
| sz00 = xp
| ~ spl29_23
| spl29_33 ),
inference(forward_subsumption_resolution,[],[f8607,f1434]) ).
fof(f8615,plain,
( sz00 != sdtasdt0(xp,sK28)
| sz00 = sK0(sdtasdt0(xp,sK28),xp)
| ~ spl29_23
| spl29_33 ),
inference(forward_subsumption_resolution,[],[f8611,f335]) ).
fof(f8618,plain,
( spl29_70
| ~ spl29_38
| ~ spl29_23
| spl29_33 ),
inference(avatar_split_clause,[],[f8615,f1432,f1216,f1525,f1792]) ).
fof(f14788,plain,
( ! [X0] :
( aInteger0(X0)
| sdtpldt0(xp,sdtpldt0(X0,sdtasdt0(xp,sK27))) = sdtpldt0(sdtpldt0(xp,X0),sdtasdt0(xp,sK27)) )
| spl29_22 ),
inference(resolution,[],[f1997,f1001]) ).
fof(f14875,plain,
( ! [X0] :
( aInteger0(X0)
| sdtpldt0(xp,sdtpldt0(X0,sz00)) = sdtpldt0(sdtpldt0(xp,X0),sz00) )
| spl29_22
| ~ spl29_35 ),
inference(forward_demodulation,[],[f14788,f1513]) ).
fof(f17075,plain,
( ! [X0] :
( aInteger0(X0)
| sdtpldt0(X0,sdtpldt0(sz10,smndt0(sz10))) = sdtpldt0(sdtpldt0(X0,sz10),smndt0(sz10)) )
| spl29_14
| spl29_16 ),
inference(resolution,[],[f1969,f735]) ).
fof(f17119,plain,
( ! [X0] :
( aInteger0(X0)
| sdtpldt0(smndt0(sz10),sdtpldt0(sz10,X0)) = sdtpldt0(sdtpldt0(smndt0(sz10),sz10),X0) )
| spl29_14
| spl29_16 ),
inference(resolution,[],[f1969,f735]) ).
fof(f17165,plain,
( ! [X0] :
( aInteger0(X0)
| sdtpldt0(sz00,X0) = sdtpldt0(smndt0(sz10),sdtpldt0(sz10,X0)) )
| spl29_14
| spl29_16 ),
inference(forward_demodulation,[],[f17119,f865]) ).
fof(f17173,plain,
( ! [X0] :
( sdtpldt0(X0,sdtasdt0(xp,sK27)) = sdtpldt0(sdtpldt0(X0,sz10),smndt0(sz10))
| aInteger0(X0) )
| ~ spl29_2
| spl29_14
| spl29_16 ),
inference(forward_demodulation,[],[f17075,f985]) ).
fof(f17183,plain,
( ! [X0] :
( aInteger0(X0)
| sdtpldt0(X0,sz00) = sdtpldt0(sdtpldt0(X0,sz10),smndt0(sz10)) )
| ~ spl29_2
| spl29_14
| spl29_16
| ~ spl29_35 ),
inference(forward_demodulation,[],[f17173,f1513]) ).
fof(f59069,plain,
( aDivisorOf0(sK0(sz00,xp),sz00)
| ~ spl29_38
| ~ spl29_71 ),
inference(forward_demodulation,[],[f1799,f1526]) ).
fof(f59070,plain,
( aDivisorOf0(sz00,sz00)
| ~ spl29_38
| ~ spl29_71
| ~ spl29_121 ),
inference(forward_demodulation,[],[f59069,f3293]) ).
fof(f59073,plain,
( ~ aDivisorOf0(sK0(sz00,xp),sz00)
| ~ spl29_38
| spl29_71 ),
inference(forward_demodulation,[],[f1798,f1526]) ).
fof(f59074,plain,
( ~ aDivisorOf0(sz00,sz00)
| ~ spl29_38
| spl29_71
| ~ spl29_121 ),
inference(forward_demodulation,[],[f59073,f3293]) ).
fof(f83130,plain,
( sdtpldt0(smndt0(xp),sz00) = sdtpldt0(sdtpldt0(smndt0(xp),sz10),smndt0(sz10))
| ~ spl29_2
| spl29_14
| spl29_16
| ~ spl29_35
| spl29_275 ),
inference(resolution,[],[f17183,f7955]) ).
fof(f83249,plain,
( sdtpldt0(sz10,smndt0(sz10)) = sdtpldt0(smndt0(xp),sz00)
| ~ spl29_2
| spl29_14
| spl29_16
| ~ spl29_35
| spl29_275 ),
inference(forward_demodulation,[],[f83130,f8023]) ).
fof(f83282,plain,
( sdtasdt0(xp,sK27) = sdtpldt0(smndt0(xp),sz00)
| ~ spl29_2
| spl29_14
| spl29_16
| ~ spl29_35
| spl29_275 ),
inference(forward_demodulation,[],[f83249,f985]) ).
fof(f83311,plain,
( sz00 = sdtpldt0(smndt0(xp),sz00)
| ~ spl29_2
| spl29_14
| spl29_16
| ~ spl29_35
| spl29_275 ),
inference(forward_demodulation,[],[f83282,f1513]) ).
fof(f86722,plain,
( sdtpldt0(xp,sdtpldt0(smndt0(xp),sz00)) = sdtpldt0(sdtpldt0(xp,smndt0(xp)),sz00)
| spl29_22
| ~ spl29_35
| spl29_275 ),
inference(resolution,[],[f14875,f7955]) ).
fof(f86841,plain,
( sdtpldt0(sz00,sz00) = sdtpldt0(xp,sdtpldt0(smndt0(xp),sz00))
| spl29_22
| ~ spl29_35
| spl29_275 ),
inference(forward_demodulation,[],[f86722,f857]) ).
fof(f86871,plain,
( sdtpldt0(sz00,sz00) = sdtpldt0(xp,sz00)
| ~ spl29_2
| spl29_14
| spl29_16
| spl29_22
| ~ spl29_35
| spl29_275 ),
inference(forward_demodulation,[],[f86841,f83311]) ).
fof(f86894,plain,
( xp = sdtpldt0(sz00,sz00)
| ~ spl29_2
| spl29_14
| spl29_16
| spl29_22
| ~ spl29_35
| spl29_275 ),
inference(forward_demodulation,[],[f86871,f759]) ).
fof(f86897,plain,
( sz00 = xp
| ~ spl29_2
| spl29_14
| spl29_16
| spl29_22
| ~ spl29_35
| spl29_275 ),
inference(forward_demodulation,[],[f86894,f755]) ).
fof(f86898,plain,
( $false
| ~ spl29_2
| spl29_14
| spl29_16
| spl29_22
| ~ spl29_35
| spl29_275 ),
inference(forward_subsumption_resolution,[],[f86897,f335]) ).
fof(f86899,plain,
( ~ spl29_2
| spl29_14
| spl29_16
| spl29_22
| ~ spl29_35
| spl29_275 ),
inference(avatar_contradiction_clause,[],[f86898]) ).
fof(f86900,plain,
( sz00 = sdtasdt0(xp,sK28)
| ~ spl29_1
| spl29_14 ),
inference(forward_demodulation,[],[f1269,f852]) ).
fof(f86970,definition,
( spl29_973
<=> aDivisorOf0(xp,sz00) ),
introduced(definition,[new_symbols(definition,[spl29_973])],[avatar_definition]) ).
fof(f86972,plain,
( aDivisorOf0(xp,sz00)
| ~ spl29_973 ),
inference(avatar_component_clause,[],[f86970]) ).
fof(f87446,definition,
( spl29_984
<=> sz00 = sdtasdt0(xp,sz00) ),
introduced(definition,[new_symbols(definition,[spl29_984])],[avatar_definition]) ).
fof(f87448,plain,
( sz00 = sdtasdt0(xp,sz00)
| ~ spl29_984 ),
inference(avatar_component_clause,[],[f87446]) ).
fof(f88457,plain,
( spl29_38
| ~ spl29_1
| spl29_14 ),
inference(avatar_split_clause,[],[f86900,f726,f675,f1525]) ).
fof(f89826,plain,
spl29_984,
inference(avatar_split_clause,[],[f795,f87446]) ).
fof(f92074,plain,
( aDivisorOf0(xp,sz00)
| sz00 = xp
| aInteger0(xp)
| aInteger0(sz00)
| ~ spl29_984 ),
inference(superposition,[],[f1632,f87448]) ).
fof(f92076,plain,
( aDivisorOf0(xp,sz00)
| aInteger0(xp)
| aInteger0(sz00)
| ~ spl29_984 ),
inference(forward_subsumption_resolution,[],[f92074,f335]) ).
fof(f92078,plain,
( aDivisorOf0(xp,sz00)
| aInteger0(sz00)
| ~ spl29_984 ),
inference(forward_subsumption_resolution,[],[f92076,f653]) ).
fof(f92080,plain,
( aDivisorOf0(xp,sz00)
| ~ spl29_984 ),
inference(forward_subsumption_resolution,[],[f92078,f475]) ).
fof(f92082,plain,
( spl29_973
| ~ spl29_984 ),
inference(avatar_split_clause,[],[f92080,f87446,f86970]) ).
fof(f119040,plain,
( sz00 = sK0(sdtasdt0(xp,sz00),xp)
| ~ spl29_23
| ~ spl29_70 ),
inference(forward_demodulation,[],[f1794,f8539]) ).
fof(f119041,plain,
( sz00 = sK0(sz00,xp)
| ~ spl29_23
| ~ spl29_70
| ~ spl29_984 ),
inference(forward_demodulation,[],[f119040,f87448]) ).
fof(f287296,definition,
( spl29_1737
<=> aInteger0(sdtpldt0(sK28,xp)) ),
introduced(definition,[new_symbols(definition,[spl29_1737])],[avatar_definition]) ).
fof(f287297,plain,
( ~ aInteger0(sdtpldt0(sK28,xp))
| spl29_1737 ),
inference(avatar_component_clause,[],[f287296]) ).
fof(f287298,plain,
( aInteger0(sdtpldt0(sK28,xp))
| ~ spl29_1737 ),
inference(avatar_component_clause,[],[f287296]) ).
fof(f287300,definition,
( spl29_1738
<=> sz00 = sdtpldt0(sK28,xp) ),
introduced(definition,[new_symbols(definition,[spl29_1738])],[avatar_definition]) ).
fof(f287301,plain,
( sz00 != sdtpldt0(sK28,xp)
| spl29_1738 ),
inference(avatar_component_clause,[],[f287300]) ).
fof(f287302,plain,
( sz00 = sdtpldt0(sK28,xp)
| ~ spl29_1738 ),
inference(avatar_component_clause,[],[f287300]) ).
fof(f287304,definition,
( spl29_1739
<=> aDivisorOf0(sdtpldt0(sK28,xp),sz00) ),
introduced(definition,[new_symbols(definition,[spl29_1739])],[avatar_definition]) ).
fof(f287305,plain,
( ~ aDivisorOf0(sdtpldt0(sK28,xp),sz00)
| spl29_1739 ),
inference(avatar_component_clause,[],[f287304]) ).
fof(f287306,plain,
( aDivisorOf0(sdtpldt0(sK28,xp),sz00)
| ~ spl29_1739 ),
inference(avatar_component_clause,[],[f287304]) ).
fof(f287558,plain,
( aInteger0(sK28)
| aInteger0(xp)
| ~ spl29_1737 ),
inference(resolution,[],[f287298,f478]) ).
fof(f287560,plain,
( aInteger0(xp)
| ~ spl29_1737 ),
inference(forward_subsumption_resolution,[],[f287558,f673]) ).
fof(f287561,plain,
( $false
| ~ spl29_1737 ),
inference(forward_subsumption_resolution,[],[f287560,f653]) ).
fof(f287562,plain,
~ spl29_1737,
inference(avatar_contradiction_clause,[],[f287561]) ).
fof(f290142,plain,
( aDivisorOf0(sz00,sz00)
| ~ spl29_1738
| ~ spl29_1739 ),
inference(forward_demodulation,[],[f287306,f287302]) ).
fof(f290143,plain,
( $false
| ~ spl29_38
| spl29_71
| ~ spl29_121
| ~ spl29_1738
| ~ spl29_1739 ),
inference(forward_subsumption_resolution,[],[f290142,f59074]) ).
fof(f290144,plain,
( ~ spl29_38
| spl29_71
| ~ spl29_121
| ~ spl29_1738
| ~ spl29_1739 ),
inference(avatar_contradiction_clause,[],[f290143]) ).
fof(f290169,plain,
( spl29_121
| ~ spl29_23
| ~ spl29_70
| ~ spl29_984 ),
inference(avatar_split_clause,[],[f119041,f87446,f1792,f1216,f3291]) ).
fof(f290259,plain,
( aInteger0(sz00)
| ~ spl29_38
| ~ spl29_71
| ~ spl29_121 ),
inference(resolution,[],[f59070,f498]) ).
fof(f290265,plain,
( $false
| ~ spl29_38
| ~ spl29_71
| ~ spl29_121 ),
inference(forward_subsumption_resolution,[],[f290259,f475]) ).
fof(f290266,plain,
( ~ spl29_38
| ~ spl29_71
| ~ spl29_121 ),
inference(avatar_contradiction_clause,[],[f290265]) ).
fof(f548608,plain,
( sz00 != sdtpldt0(sz00,xp)
| ~ spl29_59
| spl29_1738 ),
inference(superposition,[],[f287301,f1737]) ).
fof(f851352,plain,
( sdtpldt0(sz00,sdtpldt0(sK28,xp)) = sdtpldt0(smndt0(sz10),sdtpldt0(sz10,sdtpldt0(sK28,xp)))
| spl29_14
| spl29_16
| spl29_1737 ),
inference(resolution,[],[f17165,f287297]) ).
fof(f851602,plain,
( sdtpldt0(sz00,sdtpldt0(sz00,xp)) = sdtpldt0(smndt0(sz10),sdtpldt0(sz10,sdtpldt0(sz00,xp)))
| spl29_14
| spl29_16
| ~ spl29_59
| spl29_1737 ),
inference(forward_demodulation,[],[f851352,f1737]) ).
fof(f851690,plain,
( sdtpldt0(sz00,xp) = sdtpldt0(smndt0(sz10),sdtpldt0(sz10,xp))
| spl29_14
| spl29_16
| ~ spl29_59
| spl29_1737 ),
inference(forward_demodulation,[],[f851602,f768]) ).
fof(f851776,plain,
( sdtpldt0(sz00,xp) = sdtpldt0(smndt0(sz10),sz10)
| ~ spl29_1
| spl29_14
| spl29_16
| ~ spl29_59
| spl29_1737 ),
inference(forward_demodulation,[],[f851690,f677]) ).
fof(f851814,plain,
( sz00 = sdtpldt0(sz00,xp)
| ~ spl29_1
| spl29_14
| spl29_16
| ~ spl29_59
| spl29_1737 ),
inference(forward_demodulation,[],[f851776,f865]) ).
fof(f851844,plain,
( $false
| ~ spl29_1
| spl29_14
| spl29_16
| ~ spl29_59
| spl29_1737
| spl29_1738 ),
inference(forward_subsumption_resolution,[],[f851814,f548608]) ).
fof(f851845,plain,
( ~ spl29_1
| spl29_14
| spl29_16
| ~ spl29_59
| spl29_1737
| spl29_1738 ),
inference(avatar_contradiction_clause,[],[f851844]) ).
fof(f851861,plain,
( ~ aDivisorOf0(sdtpldt0(sz00,xp),sz00)
| ~ spl29_59
| spl29_1739 ),
inference(forward_demodulation,[],[f287305,f1737]) ).
fof(f852200,plain,
( ~ aDivisorOf0(xp,sz00)
| ~ spl29_59
| spl29_1739 ),
inference(forward_demodulation,[],[f851861,f768]) ).
fof(f852309,plain,
( $false
| ~ spl29_59
| ~ spl29_973
| spl29_1739 ),
inference(forward_subsumption_resolution,[],[f852200,f86972]) ).
fof(f852310,plain,
( ~ spl29_59
| ~ spl29_973
| spl29_1739 ),
inference(avatar_contradiction_clause,[],[f852309]) ).
cnf(s1,plain,
( spl29_1
| spl29_2 ),
inference(sat_conversion,[],[f682]) ).
cnf(s13,plain,
~ spl29_14,
inference(sat_conversion,[],[f738]) ).
cnf(s16,plain,
( spl29_16
| ~ spl29_21 ),
inference(sat_conversion,[],[f977]) ).
cnf(s17,plain,
( ~ spl29_2
| spl29_14
| spl29_16
| ~ spl29_22 ),
inference(sat_conversion,[],[f1002]) ).
cnf(s19,plain,
~ spl29_16,
inference(sat_conversion,[],[f1224]) ).
cnf(s104,plain,
( ~ spl29_38
| spl29_59 ),
inference(sat_conversion,[],[f2155]) ).
cnf(s213,plain,
( spl29_21
| spl29_23 ),
inference(sat_conversion,[],[f4013]) ).
cnf(s216,plain,
( spl29_21
| ~ spl29_33 ),
inference(sat_conversion,[],[f4081]) ).
cnf(s244,plain,
( ~ spl29_2
| spl29_14
| spl29_35 ),
inference(sat_conversion,[],[f4411]) ).
cnf(s443,plain,
~ spl29_275,
inference(sat_conversion,[],[f7971]) ).
cnf(s464,plain,
( ~ spl29_23
| spl29_33
| ~ spl29_38
| spl29_70 ),
inference(sat_conversion,[],[f8618]) ).
cnf(s1143,plain,
( ~ spl29_2
| spl29_14
| spl29_16
| spl29_22
| ~ spl29_35
| spl29_275 ),
inference(sat_conversion,[],[f86899]) ).
cnf(s1274,plain,
( ~ spl29_1
| spl29_14
| spl29_38 ),
inference(sat_conversion,[],[f88457]) ).
cnf(s1319,plain,
spl29_984,
inference(sat_conversion,[],[f89826]) ).
cnf(s1390,plain,
( spl29_973
| ~ spl29_984 ),
inference(sat_conversion,[],[f92082]) ).
cnf(s2842,plain,
~ spl29_1737,
inference(sat_conversion,[],[f287562]) ).
cnf(s2846,plain,
( ~ spl29_38
| spl29_71
| ~ spl29_121
| ~ spl29_1738
| ~ spl29_1739 ),
inference(sat_conversion,[],[f290144]) ).
cnf(s2867,plain,
( ~ spl29_23
| ~ spl29_70
| spl29_121
| ~ spl29_984 ),
inference(sat_conversion,[],[f290169]) ).
cnf(s2879,plain,
( ~ spl29_38
| ~ spl29_71
| ~ spl29_121 ),
inference(sat_conversion,[],[f290266]) ).
cnf(s4504,plain,
( ~ spl29_1
| spl29_14
| spl29_16
| ~ spl29_59
| spl29_1737
| spl29_1738 ),
inference(sat_conversion,[],[f851845]) ).
cnf(s4529,plain,
( ~ spl29_59
| ~ spl29_973
| spl29_1739 ),
inference(sat_conversion,[],[f852310]) ).
cnf(s4562,plain,
spl29_973,
inference(rat,[],[s1390,s1319]) ).
cnf(s4640,plain,
( ~ spl29_2
| spl29_14
| ~ spl29_22 ),
inference(rat,[],[s17,s19]) ).
cnf(s4641,plain,
~ spl29_21,
inference(rat,[],[s16,s19]) ).
cnf(s4642,plain,
~ spl29_33,
inference(rat,[],[s216,s4641]) ).
cnf(s4643,plain,
spl29_23,
inference(rat,[],[s213,s4641]) ).
cnf(s4684,plain,
~ spl29_2,
inference(rat,[],[s1143,s4640,s244,s19,s13,s443]) ).
cnf(s4686,plain,
spl29_1,
inference(rat,[],[s1,s4684]) ).
cnf(s4698,plain,
spl29_38,
inference(rat,[],[s1274,s13,s4686]) ).
cnf(s4723,plain,
spl29_59,
inference(rat,[],[s104,s4698]) ).
cnf(s4724,plain,
spl29_70,
inference(rat,[],[s464,s4643,s4642,s4698]) ).
cnf(s4740,plain,
spl29_1739,
inference(rat,[],[s4529,s4562,s4723]) ).
cnf(s4745,plain,
spl29_1738,
inference(rat,[],[s4504,s4686,s2842,s13,s19,s4723]) ).
cnf(s4747,plain,
spl29_121,
inference(rat,[],[s2867,s1319,s4643,s4724]) ).
cnf(s4760,plain,
~ spl29_71,
inference(rat,[],[s2879,s4698,s4747]) ).
cnf(s4761,plain,
$false,
inference(rat,[],[s2846,s4740,s4745,s4698,s4747,s4760]) ).
fof(f852335,plain,
$false,
inference(avatar_sat_refutation,[],[s4761]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM453+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.37 % Computer : n013.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 19:59:21 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.40 Running first-order model finding
% 0.09/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 26.82/4.27 % (516542)Will run a generic schedule for satisfiability detection.
% 26.82/4.27 % (516550)dis+10_1_sil=32000:sp=arity:random_seed=825811986:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 26.82/4.27 % (516548)% WARNING: option uhcvi not known.
% 26.82/4.27 % (516547)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2663057872_2999 on theBenchmark for (2999ds/0Mi)
% 26.82/4.27 % (516548)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3105549287:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 26.82/4.27 % (516549)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3954068016:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 26.82/4.27 % (516551)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=196258289:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 26.82/4.27 % (516553)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=656714649:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 26.82/4.27 % (516552)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3003243187:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 26.82/4.27 % TRYING [1]
% 26.82/4.27 % TRYING [2]
% 26.82/4.27 % TRYING [3]
% 26.82/4.27 % (516550)Instruction limit reached!
% 26.82/4.27 % (516550)------------------------------
% 26.82/4.27 % (516550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.82/4.27 % (516550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.82/4.27 % (516550)CaDiCaL version: 2.1.3
% 26.82/4.27 % (516550)Termination reason: Instruction limit
% 26.82/4.27 % (516550)Termination phase: Saturation
% 26.82/4.27 % (516550)Time elapsed: 0.036 s
% 26.82/4.27 % (516550)Peak memory usage: 13 MB
% 26.82/4.27 % (516550)Instructions burned: 105 (million)
% 26.82/4.27 % (516561)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4133916195:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 26.82/4.27 % TRYING [1]
% 26.82/4.27 % TRYING [4]
% 26.82/4.27 % TRYING [2]
% 26.82/4.27 % TRYING [3]
% 26.82/4.27 % TRYING [4]
% 26.82/4.27 % (516551)Instruction limit reached!
% 26.82/4.27 % (516551)------------------------------
% 26.82/4.27 % (516551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.82/4.27 % (516551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.82/4.27 % (516551)CaDiCaL version: 2.1.3
% 26.82/4.27 % (516551)Termination reason: Instruction limit
% 26.82/4.27 % (516551)Termination phase: Saturation
% 26.82/4.27 % (516551)Time elapsed: 0.070 s
% 26.82/4.27 % (516551)Peak memory usage: 13 MB
% 26.82/4.27 % (516551)Instructions burned: 117 (million)
% 26.82/4.27 % (516552)Instruction limit reached!
% 26.82/4.27 % (516552)------------------------------
% 26.82/4.27 % (516552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.82/4.27 % (516552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.82/4.27 % (516552)CaDiCaL version: 2.1.3
% 26.82/4.27 % (516552)Termination reason: Instruction limit
% 26.82/4.27 % (516552)Termination phase: Saturation
% 26.82/4.27 % (516552)Time elapsed: 0.072 s
% 26.82/4.27 % (516552)Peak memory usage: 14 MB
% 26.82/4.27 % (516552)Instructions burned: 131 (million)
% 26.82/4.27 % (516563)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3646033621:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 26.82/4.27 % (516564)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2576415376:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 26.82/4.27 % TRYING [5]
% 26.82/4.27 % (516553)Instruction limit reached!
% 26.82/4.27 % (516553)------------------------------
% 26.82/4.27 % (516553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.82/4.27 % (516553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.82/4.27 % (516553)CaDiCaL version: 2.1.3
% 26.82/4.27 % (516553)Termination reason: Instruction limit
% 26.82/4.27 % (516553)Termination phase: Saturation
% 26.82/4.27 % (516553)Time elapsed: 0.099 s
% 26.82/4.27 % (516553)Peak memory usage: 14 MB
% 26.82/4.27 % (516553)Instructions burned: 159 (million)
% 26.82/4.27 % TRYING [5]
% 26.82/4.27 % (516567)ott-21_1_sil=16000:fs=off:random_seed=4121563994:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 26.82/4.27 % (516563)Instruction limit reached!
% 26.82/4.27 % (516563)------------------------------
% 26.82/4.27 % (516563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.82/4.27 % (516563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.90/7.04 % (516563)CaDiCaL version: 2.1.3
% 46.90/7.04 % (516563)Termination reason: Instruction limit
% 46.90/7.04 % (516563)Termination phase: Saturation
% 46.90/7.04 % (516563)Time elapsed: 0.079 s
% 46.90/7.04 % (516563)Peak memory usage: 13 MB
% 46.90/7.04 % (516563)Instructions burned: 132 (million)
% 46.90/7.04 % (516569)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1752591094:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 46.90/7.04 % TRYING [6]
% 46.90/7.04 % (516561)Instruction limit reached!
% 46.90/7.04 % (516561)------------------------------
% 46.90/7.04 % (516561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.90/7.04 % (516561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.90/7.04 % (516561)CaDiCaL version: 2.1.3
% 46.90/7.04 % (516561)Termination reason: Instruction limit
% 46.90/7.04 % (516561)Termination phase: Finite model building constraint generation
% 46.90/7.04 % (516561)Time elapsed: 0.159 s
% 46.90/7.04 % (516561)Peak memory usage: 33 MB
% 46.90/7.04 % (516561)Instructions burned: 719 (million)
% 46.90/7.04 % (516571)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=974837646:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 46.90/7.04 % (516567)Instruction limit reached!
% 46.90/7.04 % (516567)------------------------------
% 46.90/7.04 % (516567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.90/7.04 % (516567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.90/7.04 % (516567)CaDiCaL version: 2.1.3
% 46.90/7.04 % (516567)Termination reason: Instruction limit
% 46.90/7.04 % (516567)Termination phase: Saturation
% 46.90/7.04 % (516567)Time elapsed: 0.091 s
% 46.90/7.04 % (516567)Peak memory usage: 13 MB
% 46.90/7.04 % (516567)Instructions burned: 180 (million)
% 46.90/7.04 % TRYING [1]
% 46.90/7.04 % TRYING [2]
% 46.90/7.04 % TRYING [3]
% 46.90/7.04 % (516573)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1142529868:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 46.90/7.04 % TRYING [4]
% 46.90/7.04 % TRYING [6]
% 46.90/7.04 % (516571)Instruction limit reached!
% 46.90/7.04 % (516571)------------------------------
% 46.90/7.04 % (516571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.90/7.04 % (516571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.90/7.04 % (516571)CaDiCaL version: 2.1.3
% 46.90/7.04 % (516571)Termination reason: Instruction limit
% 46.90/7.04 % (516571)Termination phase: Finite model building SAT solving
% 46.90/7.04 % (516571)Time elapsed: 0.182 s
% 46.90/7.04 % (516571)Peak memory usage: 22 MB
% 46.90/7.04 % (516571)Instructions burned: 866 (million)
% 46.90/7.04 % (516575)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2583906379:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 46.90/7.04 % (516564)Instruction limit reached!
% 46.90/7.04 % (516564)------------------------------
% 46.90/7.04 % (516564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.90/7.04 % (516564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.90/7.04 % (516564)CaDiCaL version: 2.1.3
% 46.90/7.04 % (516564)Termination reason: Instruction limit
% 46.90/7.04 % (516564)Termination phase: Saturation
% 46.90/7.04 % (516564)Time elapsed: 0.363 s
% 46.90/7.04 % (516564)Peak memory usage: 20 MB
% 46.90/7.04 % (516564)Instructions burned: 685 (million)
% 46.90/7.04 % (516577)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1901161570:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 46.90/7.04 % (516569)Instruction limit reached!
% 46.90/7.04 % (516569)------------------------------
% 46.90/7.04 % (516569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.90/7.04 % (516569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.90/7.04 % (516569)CaDiCaL version: 2.1.3
% 46.90/7.04 % (516569)Termination reason: Instruction limit
% 46.90/7.04 % (516569)Termination phase: Saturation
% 46.90/7.04 % (516569)Time elapsed: 0.338 s
% 46.90/7.04 % (516569)Peak memory usage: 15 MB
% 46.90/7.04 % (516569)Instructions burned: 478 (million)
% 46.90/7.04 % (516579)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2025737436:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 46.90/7.04 % TRYING [14]
% 46.90/7.04 % (516575)Instruction limit reached!
% 46.90/7.04 % (516575)------------------------------
% 46.90/7.04 % (516575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.62/14.01 % (516575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.62/14.01 % (516575)CaDiCaL version: 2.1.3
% 95.62/14.01 % (516575)Termination reason: Instruction limit
% 95.62/14.01 % (516575)Termination phase: Finite model building constraint generation
% 95.62/14.01 % (516575)Time elapsed: 0.214 s
% 95.62/14.01 % (516575)Peak memory usage: 89 MB
% 95.62/14.01 % (516575)Instructions burned: 892 (million)
% 95.62/14.01 % (516581)fmb+10_1_sil=64000:random_seed=731685372:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 95.62/14.01 % TRYING [1]
% 95.62/14.01 % TRYING [2]
% 95.62/14.01 % TRYING [3]
% 95.62/14.01 % TRYING [4]
% 95.62/14.01 % TRYING [5]
% 95.62/14.01 % TRYING [7]
% 95.62/14.01 % (516577)Instruction limit reached!
% 95.62/14.01 % (516577)------------------------------
% 95.62/14.01 % (516577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.62/14.01 % (516577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.62/14.01 % (516577)CaDiCaL version: 2.1.3
% 95.62/14.01 % (516577)Termination reason: Instruction limit
% 95.62/14.01 % (516577)Termination phase: Saturation
% 95.62/14.01 % (516577)Time elapsed: 0.395 s
% 95.62/14.01 % (516577)Peak memory usage: 25 MB
% 95.62/14.01 % (516577)Instructions burned: 692 (million)
% 95.62/14.01 % (516583)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1328756874:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 95.62/14.01 % (516573)Instruction limit reached!
% 95.62/14.01 % (516573)------------------------------
% 95.62/14.01 % (516573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.62/14.01 % (516573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.62/14.01 % (516573)CaDiCaL version: 2.1.3
% 95.62/14.01 % (516573)Termination reason: Instruction limit
% 95.62/14.01 % (516573)Termination phase: Saturation
% 95.62/14.01 % (516573)Time elapsed: 0.660 s
% 95.62/14.01 % (516573)Peak memory usage: 25 MB
% 95.62/14.01 % (516573)Instructions burned: 1180 (million)
% 95.62/14.01 % TRYING [20]
% 95.62/14.01 % (516585)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=309576035:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 95.62/14.01 % TRYING [8]
% 95.62/14.01 % TRYING [6]
% 95.62/14.01 % (516579)Instruction limit reached!
% 95.62/14.01 % (516579)------------------------------
% 95.62/14.01 % (516579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.62/14.01 % (516579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.62/14.01 % (516579)CaDiCaL version: 2.1.3
% 95.62/14.01 % (516579)Termination reason: Instruction limit
% 95.62/14.01 % (516579)Termination phase: Saturation
% 95.62/14.01 % (516579)Time elapsed: 0.496 s
% 95.62/14.01 % (516579)Peak memory usage: 20 MB
% 95.62/14.01 % (516579)Instructions burned: 880 (million)
% 95.62/14.01 % (516587)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2121557784:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 95.62/14.01 % (516585)Instruction limit reached!
% 95.62/14.01 % (516585)------------------------------
% 95.62/14.01 % (516585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.62/14.01 % (516585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.62/14.01 % (516585)CaDiCaL version: 2.1.3
% 95.62/14.01 % (516585)Termination reason: Instruction limit
% 95.62/14.01 % (516585)Termination phase: Finite model building constraint generation
% 95.62/14.01 % (516585)Time elapsed: 0.341 s
% 95.62/14.01 % (516585)Peak memory usage: 80 MB
% 95.62/14.01 % (516585)Instructions burned: 921 (million)
% 95.62/14.01 % (516589)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3290933619:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 95.62/14.01 % TRYING [7]
% 95.62/14.01 % (516589)Instruction limit reached!
% 95.62/14.01 % (516589)------------------------------
% 95.62/14.01 % (516589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.62/14.01 % (516589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.62/14.01 % (516589)CaDiCaL version: 2.1.3
% 95.62/14.01 % (516589)Termination reason: Instruction limit
% 95.62/14.01 % (516589)Termination phase: Saturation
% 95.62/14.01 % (516589)Time elapsed: 0.763 s
% 95.62/14.01 % (516589)Peak memory usage: 29 MB
% 95.62/14.01 % (516589)Instructions burned: 1474 (million)
% 95.62/14.01 % (516591)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1895477999:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 95.62/14.01 % TRYING [77]
% 95.62/14.01 % TRYING [8]
% 95.62/14.01 % TRYING [8]
% 95.62/14.01 % (516587)Instruction limit reached!
% 95.62/14.01 % (516587)------------------------------
% 95.62/14.01 % (516587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.57/26.68 % (516587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.57/26.68 % (516587)CaDiCaL version: 2.1.3
% 114.57/26.68 % (516587)Termination reason: Instruction limit
% 114.57/26.68 % (516587)Termination phase: Saturation
% 114.57/26.68 % (516587)Time elapsed: 2.751 s
% 114.57/26.68 % (516587)Peak memory usage: 37 MB
% 114.57/26.68 % (516587)Instructions burned: 5132 (million)
% 114.57/26.68 % (516593)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=330510875:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 114.57/26.68 % TRYING [16]
% 114.57/26.68 % (516583)Instruction limit reached!
% 114.57/26.68 % (516583)------------------------------
% 114.57/26.68 % (516583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.57/26.68 % (516583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.57/26.68 % (516583)CaDiCaL version: 2.1.3
% 114.57/26.68 % (516583)Termination reason: Instruction limit
% 114.57/26.68 % (516583)Termination phase: Finite model building constraint generation
% 114.57/26.68 % (516583)Time elapsed: 3.220 s
% 114.57/26.68 % (516583)Peak memory usage: 520 MB
% 114.57/26.68 % (516583)Instructions burned: 9518 (million)
% 114.57/26.68 % (516595)ott-2_1_sil=16000:newcnf=on:random_seed=881225026:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 114.57/26.68 % (516591)Instruction limit reached!
% 114.57/26.68 % (516591)------------------------------
% 114.57/26.68 % (516591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.57/26.68 % (516591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.57/26.68 % (516591)CaDiCaL version: 2.1.3
% 114.57/26.68 % (516591)Termination reason: Instruction limit
% 114.57/26.68 % (516591)Termination phase: Finite model building constraint generation
% 114.57/26.68 % (516591)Time elapsed: 2.273 s
% 114.57/26.68 % (516591)Peak memory usage: 450 MB
% 114.57/26.68 % (516591)Instructions burned: 6327 (million)
% 114.57/26.68 % (516597)ott+10_1_sil=32000:tgt=ground:random_seed=220088146:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 114.57/26.68 % (516593)Instruction limit reached!
% 114.57/26.68 % (516593)------------------------------
% 114.57/26.68 % (516593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.57/26.68 % (516593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.57/26.68 % (516593)CaDiCaL version: 2.1.3
% 114.57/26.68 % (516593)Termination reason: Instruction limit
% 114.57/26.68 % (516593)Termination phase: Finite model building constraint generation
% 114.57/26.68 % (516593)Time elapsed: 0.771 s
% 114.57/26.68 % (516593)Peak memory usage: 137 MB
% 114.57/26.68 % (516593)Instructions burned: 2176 (million)
% 114.57/26.68 % (516599)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3991842651:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 114.57/26.68 % TRYING [1]
% 114.57/26.68 % TRYING [2]
% 114.57/26.68 % TRYING [3]
% 114.57/26.68 % TRYING [4]
% 114.57/26.68 % (516595)Instruction limit reached!
% 114.57/26.68 % (516595)------------------------------
% 114.57/26.68 % (516595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.57/26.68 % (516595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.57/26.68 % (516595)CaDiCaL version: 2.1.3
% 114.57/26.68 % (516595)Termination reason: Instruction limit
% 114.57/26.68 % (516595)Termination phase: Saturation
% 114.57/26.68 % (516595)Time elapsed: 0.499 s
% 114.57/26.68 % (516595)Peak memory usage: 20 MB
% 114.57/26.68 % (516595)Instructions burned: 870 (million)
% 114.57/26.68 % (516601)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=108917837:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi)
% 114.57/26.68 % TRYING [5]
% 114.57/26.68 % TRYING [6]
% 114.57/26.68 % TRYING [7]
% 114.57/26.68 % (516581)Instruction limit reached!
% 114.57/26.68 % (516581)------------------------------
% 114.57/26.68 % (516581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.57/26.68 % (516581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.57/26.68 % (516581)CaDiCaL version: 2.1.3
% 114.57/26.68 % (516581)Termination reason: Instruction limit
% 114.57/26.68 % (516581)Termination phase: Finite model building SAT solving
% 114.57/26.68 % (516581)Time elapsed: 5.024 s
% 114.57/26.68 % (516581)Peak memory usage: 154 MB
% 114.57/26.68 % (516581)Instructions burned: 22062 (million)
% 114.57/26.68 % (516603)dis+21_1_sil=32000:sas=cadical:random_seed=1747813879:i=3773:amm=off_2942 on theBenchmark for (2942ds/3773Mi)
% 114.57/26.68 % (516601)Instruction limit reached!
% 114.57/26.68 % (516601)------------------------------
% 114.57/26.68 % (516601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.57/26.68 % (516601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.57/26.68 % (516601)CaDiCaL version: 2.1.3
% 114.57/26.68 % (516601)Termination reason: Instruction limit
% 114.57/26.68 % (516601)Termination phase: Saturation
% 114.57/26.68 % (516601)Time elapsed: 1.865 s
% 114.57/26.68 % (516601)Peak memory usage: 34 MB
% 114.57/26.68 % (516601)Instructions burned: 3512 (million)
% 114.57/26.68 % (516605)ott+11_1_sil=16000:gs=on:random_seed=1094921269:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2933 on theBenchmark for (2933ds/2251Mi)
% 114.57/26.68 % (516603)Instruction limit reached!
% 114.57/26.68 % (516603)------------------------------
% 114.57/26.68 % (516603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.57/26.68 % (516603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.57/26.68 % (516603)CaDiCaL version: 2.1.3
% 114.57/26.68 % (516603)Termination reason: Instruction limit
% 114.57/26.68 % (516603)Termination phase: Saturation
% 114.57/26.68 % (516603)Time elapsed: 1.110 s
% 114.57/26.68 % (516603)Peak memory usage: 42 MB
% 114.57/26.68 % (516603)Instructions burned: 3776 (million)
% 114.57/26.68 % (516607)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2198442129:fmbsr=1.6:i=67534_2931 on theBenchmark for (2931ds/67534Mi)
% 114.57/26.68 % TRYING [7]
% 114.57/26.68 % (516597)Instruction limit reached!
% 114.57/26.68 % (516597)------------------------------
% 114.57/26.68 % (516597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.57/26.68 % (516597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.57/26.68 % (516597)CaDiCaL version: 2.1.3
% 114.57/26.68 % (516597)Termination reason: Instruction limit
% 114.57/26.68 % (516597)Termination phase: Saturation
% 114.57/26.68 % (516597)Time elapsed: 2.847 s
% 114.57/26.68 % (516597)Peak memory usage: 64 MB
% 114.57/26.68 % (516597)Instructions burned: 5115 (million)
% 114.57/26.68 % (516609)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=151973610:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2926 on theBenchmark for (2926ds/4591Mi)
% 114.57/26.68 % (516605)Instruction limit reached!
% 114.57/26.68 % (516605)------------------------------
% 114.57/26.68 % (516605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.57/26.68 % (516605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.57/26.68 % (516605)CaDiCaL version: 2.1.3
% 114.57/26.68 % (516605)Termination reason: Instruction limit
% 114.57/26.68 % (516605)Termination phase: Saturation
% 114.57/26.68 % (516605)Time elapsed: 0.979 s
% 114.57/26.68 % (516605)Peak memory usage: 18 MB
% 114.57/26.68 % (516605)Instructions burned: 2253 (million)
% 114.57/26.68 % TRYING [8]
% 114.57/26.68 % (516611)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2894093366:i=29340_2923 on theBenchmark for (2923ds/29340Mi)
% 114.57/26.68 % TRYING [8]
% 114.57/26.68 % (516609)Instruction limit reached!
% 114.57/26.68 % (516609)------------------------------
% 114.57/26.68 % (516609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.57/26.68 % (516609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.57/26.68 % (516609)CaDiCaL version: 2.1.3
% 114.57/26.68 % (516609)Termination reason: Instruction limit
% 114.57/26.68 % (516609)Termination phase: Saturation
% 114.57/26.68 % (516609)Time elapsed: 1.751 s
% 114.57/26.68 % (516609)Peak memory usage: 35 MB
% 114.57/26.68 % (516609)Instructions burned: 4591 (million)
% 114.57/26.68 % (516613)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3752073086:i=5211_2909 on theBenchmark for (2909ds/5211Mi)
% 114.57/26.68 % (516613)Instruction limit reached!
% 114.57/26.68 % (516613)------------------------------
% 114.57/26.68 % (516613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.57/26.68 % (516613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.57/26.68 % (516613)CaDiCaL version: 2.1.3
% 114.57/26.68 % (516613)Termination reason: Instruction limit
% 114.57/26.68 % (516613)Termination phase: Saturation
% 114.57/26.68 % (516613)Time elapsed: 2.514 s
% 114.57/26.68 % (516613)Peak memory usage: 41 MB
% 114.57/26.68 % (516613)Instructions burned: 5211 (million)
% 114.57/26.68 % (516615)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1819926658:i=5497:nm=2_2883 on theBenchmark for (2883ds/5497Mi)
% 114.57/26.68 % TRYING [17]
% 114.57/26.68 % TRYING [9]
% 114.57/26.68 % (516615)Instruction limit reached!
% 114.57/26.68 % (516615)------------------------------
% 114.57/26.68 % (516615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.57/26.68 % (516615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.57/26.68 % (516615)CaDiCaL version: 2.1.3
% 114.57/26.68 % (516615)Termination reason: Instruction limit
% 114.57/26.68 % (516615)Termination phase: Finite model building constraint generation
% 114.57/26.68 % (516615)Time elapsed: 1.927 s
% 114.57/26.68 % (516615)Peak memory usage: 346 MB
% 114.57/26.68 % (516615)Instructions burned: 5498 (million)
% 114.57/26.68 % (516617)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1303541893:fmbsr=2:i=46332_2863 on theBenchmark for (2863ds/46332Mi)
% 114.57/26.68 % TRYING [15]
% 114.57/26.68 % TRYING [9]
% 114.57/26.68 % (516611)Instruction limit reached!
% 114.57/26.68 % (516611)------------------------------
% 114.57/26.68 % (516611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.57/26.68 % (516611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.57/26.68 % (516611)CaDiCaL version: 2.1.3
% 114.57/26.68 % (516611)Termination reason: Instruction limit
% 114.57/26.68 % (516611)Termination phase: Saturation
% 114.57/26.68 % (516611)Time elapsed: 13.592 s
% 114.57/26.68 % (516611)Peak memory usage: 240 MB
% 114.57/26.68 % (516611)Instructions burned: 29341 (million)
% 114.57/26.68 % (516619)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1521871682:i=14071_2787 on theBenchmark for (2787ds/14071Mi)
% 114.57/26.68 % TRYING [12]
% 114.57/26.68 % TRYING [10]
% 114.57/26.68 % TRYING [9]
% 114.57/26.68 % (516607)Instruction limit reached!
% 114.57/26.68 % (516607)------------------------------
% 114.57/26.68 % (516607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.57/26.68 % (516607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.57/26.68 % (516607)CaDiCaL version: 2.1.3
% 114.57/26.68 % (516607)Termination reason: Instruction limit
% 114.57/26.68 % (516607)Termination phase: Finite model building SAT solving
% 114.57/26.68 % (516607)Time elapsed: 18.420 s
% 114.57/26.68 % (516607)Peak memory usage: 394 MB
% 114.57/26.68 % (516607)Instructions burned: 67536 (million)
% 114.57/26.68 % (516622)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2224534248:i=22565:add=on:rawr=on_2747 on theBenchmark for (2747ds/22565Mi)
% 114.57/26.68 % (516548) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-516542-516548"...
% 114.57/26.68 % (516548)...printing done.
% 114.57/26.68 % (516548)Refutation found. Thanks to Tanya!
% 114.57/26.68 % SZS status Theorem for theBenchmark
% 114.57/26.68 % SZS output start Proof for theBenchmark
% See solution above
% 114.57/26.68 % (516548)------------------------------
% 114.57/26.68 % (516548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 114.57/26.68 % (516548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.57/26.68 % (516548)CaDiCaL version: 2.1.3
% 114.57/26.68 % (516548)Termination reason: Refutation
% 114.57/26.68 % (516548)Time elapsed: 25.873 s
% 114.57/26.68 % (516548)Peak memory usage: 315 MB
% 114.57/26.68 % (516548)Instructions burned: 48909 (million)
% 114.57/26.68 % (516542)Success in time 26.263 s
% 114.57/26.68 % Vampire exiting
%------------------------------------------------------------------------------