%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM451+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 : n019.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:14 PM UTC 2026
% Result : Theorem 11.28s 2.53s
% Output : Refutation 12.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 38
% Syntax : Number of formulae : 287 ( 47 unt; 21 def)
% Number of atoms : 1376 ( 329 equ)
% Maximal formula atoms : 38 ( 4 avg)
% Number of connectives : 1731 ( 642 ~; 632 |; 394 &)
% ( 30 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 27 ( 25 usr; 17 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 8 con; 0-2 aty)
% Number of variables : 267 ( 0 sgn 220 !; 47 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
aInteger0(sz10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mIntOne) ).
fof(f5,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1) )
=> aInteger0(sdtpldt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mIntPlus) ).
fof(f6,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1) )
=> aInteger0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',mAddAsso) ).
fof(f8,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1) )
=> sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mAddComm) ).
fof(f9,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mAddZero) ).
fof(f10,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtpldt0(X0,smndt0(X0)) = sz00
& sz00 = sdtpldt0(smndt0(X0),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mAddNeg) ).
fof(f12,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1) )
=> sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulComm) ).
fof(f13,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtasdt0(X0,sz10) = X0
& X0 = sdtasdt0(sz10,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulOne) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( aInteger0(X0)
& aInteger0(X1)
& aInteger0(X2) )
=> ( sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(sdtpldt0(X0,X1),X2) = sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDistrib) ).
fof(f15,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulZero) ).
fof(f16,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtasdt0(smndt0(sz10),X0) = smndt0(X0)
& smndt0(X0) = sdtasdt0(X0,smndt0(sz10)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulMinOne) ).
fof(f17,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1) )
=> ( sdtasdt0(X0,X1) = sz00
=> ( X0 = sz00
| X1 = sz00 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mZeroDiv) ).
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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',m__2171) ).
fof(f47,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(f48,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)],[f47]) ).
fof(f55,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(f56,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(f58,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(f60,plain,
! [X0,X1] :
( aInteger0(sdtpldt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f61,plain,
! [X0,X1] :
( aInteger0(sdtpldt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f60]) ).
fof(f62,plain,
! [X0,X1] :
( aInteger0(sdtasdt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f6]) ).
fof(f63,plain,
! [X0,X1] :
( aInteger0(sdtasdt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f62]) ).
fof(f64,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(f65,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(flattening,[],[f64]) ).
fof(f66,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f67,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f66]) ).
fof(f68,plain,
! [X0] :
( ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f69,plain,
! [X0] :
( ( sdtpldt0(X0,smndt0(X0)) = sz00
& sz00 = sdtpldt0(smndt0(X0),X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f72,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f12]) ).
fof(f73,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f72]) ).
fof(f74,plain,
! [X0] :
( ( sdtasdt0(X0,sz10) = X0
& X0 = sdtasdt0(sz10,X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f75,plain,
! [X0,X1,X2] :
( ( sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(sdtpldt0(X0,X1),X2) = sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f76,plain,
! [X0,X1,X2] :
( ( sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(sdtpldt0(X0,X1),X2) = sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(flattening,[],[f75]) ).
fof(f77,plain,
! [X0] :
( ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f78,plain,
! [X0] :
( ( sdtasdt0(smndt0(sz10),X0) = smndt0(X0)
& smndt0(X0) = sdtasdt0(X0,smndt0(sz10)) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f79,plain,
! [X0,X1] :
( X0 = sz00
| X1 = sz00
| sz00 != sdtasdt0(X0,X1)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f80,plain,
! [X0,X1] :
( X0 = sz00
| X1 = sz00
| sz00 != sdtasdt0(X0,X1)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f79]) ).
fof(f115,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,[],[f55]) ).
fof(f116,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,[],[f115]) ).
fof(f119,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,[],[f58]) ).
fof(f120,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,[],[f119]) ).
fof(f121,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,[],[f48]) ).
fof(f131,definition,
! [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) ) ) )
| ~ sP6(X5) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f132,definition,
! [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) ) ) )
| ~ sP7(X1) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f133,plain,
( aSet0(xS)
& ! [X0] :
( ( ? [X1] :
( aInteger0(X1)
& X1 != sz00
& isPrime0(X1)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X1))
& sP7(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))
& sP6(X5) ) ) ) )
& xS = cS2043 ),
inference(definition_folding,[],[f116,f132,f131]) ).
fof(f189,plain,
( aSet0(xS)
& ! [X0] :
( ( ? [X1] :
( aInteger0(X1)
& X1 != sz00
& isPrime0(X1)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X1))
& sP7(X1)
& szAzrzSzezqlpdtcmdtrp0(sz00,X1) = X0 )
| ~ aElementOf0(X0,xS) )
& ( aElementOf0(X0,xS)
| ! [X2] :
( ~ aInteger0(X2)
| sz00 = X2
| ~ isPrime0(X2)
| ( szAzrzSzezqlpdtcmdtrp0(sz00,X2) != X0
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X2))
& sP6(X2) ) ) ) )
& xS = cS2043 ),
inference(rectify,[],[f133]) ).
fof(f190,plain,
( aSet0(xS)
& ! [X0] :
( ( ( aInteger0(sK27(X0))
& sz00 != sK27(X0)
& isPrime0(sK27(X0))
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,sK27(X0)))
& sP7(sK27(X0))
& szAzrzSzezqlpdtcmdtrp0(sz00,sK27(X0)) = X0 )
| ~ aElementOf0(X0,xS) )
& ( aElementOf0(X0,xS)
| ! [X2] :
( ~ aInteger0(X2)
| sz00 = X2
| ~ isPrime0(X2)
| ( szAzrzSzezqlpdtcmdtrp0(sz00,X2) != X0
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X2))
& sP6(X2) ) ) ) )
& xS = cS2043 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27]),skolemize(X1,sK27(X0))],[f189]) ).
fof(f191,plain,
( aSet0(sbsmnsldt0(xS))
& ! [X0] :
( ( aElementOf0(X0,sbsmnsldt0(xS))
| ~ aInteger0(X0)
| ! [X1] :
( ~ aElementOf0(X1,xS)
| ~ aElementOf0(X0,X1) ) )
& ( ( aInteger0(X0)
& ? [X1] :
( aElementOf0(X1,xS)
& aElementOf0(X0,X1) ) )
| ~ aElementOf0(X0,sbsmnsldt0(xS)) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [X2] :
( ( aElementOf0(X2,stldt0(sbsmnsldt0(xS)))
| ~ aInteger0(X2)
| aElementOf0(X2,sbsmnsldt0(xS)) )
& ( ( aInteger0(X2)
& ~ aElementOf0(X2,sbsmnsldt0(xS)) )
| ~ aElementOf0(X2,stldt0(sbsmnsldt0(xS))) ) )
& ! [X3] :
( ( aElementOf0(X3,stldt0(sbsmnsldt0(xS)))
| ( sz10 != X3
& smndt0(sz10) != X3 ) )
& ( sz10 = X3
| smndt0(sz10) = X3
| ~ aElementOf0(X3,stldt0(sbsmnsldt0(xS))) ) )
& stldt0(sbsmnsldt0(xS)) = cS2076 ),
inference(nnf_transformation,[],[f56]) ).
fof(f192,plain,
( aSet0(sbsmnsldt0(xS))
& ! [X0] :
( ( aElementOf0(X0,sbsmnsldt0(xS))
| ~ aInteger0(X0)
| ! [X1] :
( ~ aElementOf0(X1,xS)
| ~ aElementOf0(X0,X1) ) )
& ( ( aInteger0(X0)
& ? [X1] :
( aElementOf0(X1,xS)
& aElementOf0(X0,X1) ) )
| ~ aElementOf0(X0,sbsmnsldt0(xS)) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [X2] :
( ( aElementOf0(X2,stldt0(sbsmnsldt0(xS)))
| ~ aInteger0(X2)
| aElementOf0(X2,sbsmnsldt0(xS)) )
& ( ( aInteger0(X2)
& ~ aElementOf0(X2,sbsmnsldt0(xS)) )
| ~ aElementOf0(X2,stldt0(sbsmnsldt0(xS))) ) )
& ! [X3] :
( ( aElementOf0(X3,stldt0(sbsmnsldt0(xS)))
| ( sz10 != X3
& smndt0(sz10) != X3 ) )
& ( sz10 = X3
| smndt0(sz10) = X3
| ~ aElementOf0(X3,stldt0(sbsmnsldt0(xS))) ) )
& stldt0(sbsmnsldt0(xS)) = cS2076 ),
inference(flattening,[],[f191]) ).
fof(f193,plain,
( aSet0(sbsmnsldt0(xS))
& ! [X0] :
( ( aElementOf0(X0,sbsmnsldt0(xS))
| ~ aInteger0(X0)
| ! [X1] :
( ~ aElementOf0(X1,xS)
| ~ aElementOf0(X0,X1) ) )
& ( ( aInteger0(X0)
& ? [X2] :
( aElementOf0(X2,xS)
& aElementOf0(X0,X2) ) )
| ~ aElementOf0(X0,sbsmnsldt0(xS)) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [X3] :
( ( aElementOf0(X3,stldt0(sbsmnsldt0(xS)))
| ~ aInteger0(X3)
| aElementOf0(X3,sbsmnsldt0(xS)) )
& ( ( aInteger0(X3)
& ~ aElementOf0(X3,sbsmnsldt0(xS)) )
| ~ aElementOf0(X3,stldt0(sbsmnsldt0(xS))) ) )
& ! [X4] :
( ( aElementOf0(X4,stldt0(sbsmnsldt0(xS)))
| ( sz10 != X4
& smndt0(sz10) != X4 ) )
& ( sz10 = X4
| smndt0(sz10) = X4
| ~ aElementOf0(X4,stldt0(sbsmnsldt0(xS))) ) )
& stldt0(sbsmnsldt0(xS)) = cS2076 ),
inference(rectify,[],[f192]) ).
fof(f194,plain,
( aSet0(sbsmnsldt0(xS))
& ! [X0] :
( ( aElementOf0(X0,sbsmnsldt0(xS))
| ~ aInteger0(X0)
| ! [X1] :
( ~ aElementOf0(X1,xS)
| ~ aElementOf0(X0,X1) ) )
& ( ( aInteger0(X0)
& aElementOf0(sK28(X0),xS)
& aElementOf0(X0,sK28(X0)) )
| ~ aElementOf0(X0,sbsmnsldt0(xS)) ) )
& aSet0(stldt0(sbsmnsldt0(xS)))
& ! [X3] :
( ( aElementOf0(X3,stldt0(sbsmnsldt0(xS)))
| ~ aInteger0(X3)
| aElementOf0(X3,sbsmnsldt0(xS)) )
& ( ( aInteger0(X3)
& ~ aElementOf0(X3,sbsmnsldt0(xS)) )
| ~ aElementOf0(X3,stldt0(sbsmnsldt0(xS))) ) )
& ! [X4] :
( ( aElementOf0(X4,stldt0(sbsmnsldt0(xS)))
| ( sz10 != X4
& smndt0(sz10) != X4 ) )
& ( sz10 = X4
| smndt0(sz10) = X4
| ~ aElementOf0(X4,stldt0(sbsmnsldt0(xS))) ) )
& stldt0(sbsmnsldt0(xS)) = cS2076 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(X2,sK28(X0))],[f193]) ).
fof(f205,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,[],[f120]) ).
fof(f206,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,[],[f205]) ).
fof(f207,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,[],[f206]) ).
fof(f208,plain,
( aInteger0(xp)
& xp != sz00
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp))
& ! [X0] :
( ( ( aInteger0(X0)
& aInteger0(sK35(X0))
& sdtpldt0(X0,smndt0(sz10)) = sdtasdt0(xp,sK35(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(sK36(X3),xS)
& aElementOf0(X3,sK36(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,[sK35,sK36]),skolemize(X1,sK35(X0)),skolemize(X5,sK36(X3))],[f207]) ).
fof(f210,plain,
aInteger0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f212,plain,
! [X0,X1] :
( aInteger0(sdtpldt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(cnf_transformation,[],[f61]) ).
fof(f213,plain,
! [X0,X1] :
( aInteger0(sdtasdt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(cnf_transformation,[],[f63]) ).
fof(f214,plain,
! [X2,X0,X1] :
( ~ aInteger0(X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2) ),
inference(cnf_transformation,[],[f65]) ).
fof(f215,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ),
inference(cnf_transformation,[],[f67]) ).
fof(f216,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(sz00,X0) = X0 ),
inference(cnf_transformation,[],[f68]) ).
fof(f217,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,sz00) = X0 ),
inference(cnf_transformation,[],[f68]) ).
fof(f218,plain,
! [X0] :
( ~ aInteger0(X0)
| sz00 = sdtpldt0(smndt0(X0),X0) ),
inference(cnf_transformation,[],[f69]) ).
fof(f221,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
inference(cnf_transformation,[],[f73]) ).
fof(f222,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(sz10,X0) = X0 ),
inference(cnf_transformation,[],[f74]) ).
fof(f223,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(X0,sz10) = X0 ),
inference(cnf_transformation,[],[f74]) ).
fof(f225,plain,
! [X2,X0,X1] :
( ~ aInteger0(X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)) ),
inference(cnf_transformation,[],[f76]) ).
fof(f226,plain,
! [X0] :
( ~ aInteger0(X0)
| sz00 = sdtasdt0(sz00,X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f229,plain,
! [X0] :
( ~ aInteger0(X0)
| smndt0(X0) = sdtasdt0(smndt0(sz10),X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f230,plain,
! [X0,X1] :
( sz00 != sdtasdt0(X0,X1)
| sz00 = X1
| sz00 = X0
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(cnf_transformation,[],[f80]) ).
fof(f333,plain,
xS = cS2043,
inference(cnf_transformation,[],[f190]) ).
fof(f344,plain,
stldt0(sbsmnsldt0(xS)) = cS2076,
inference(cnf_transformation,[],[f194]) ).
fof(f346,plain,
! [X4] :
( aElementOf0(X4,stldt0(sbsmnsldt0(xS)))
| smndt0(sz10) != X4 ),
inference(cnf_transformation,[],[f194]) ).
fof(f407,plain,
! [X6] :
( aInteger0(X6)
| ~ aElementOf0(X6,stldt0(sbsmnsldt0(xS))) ),
inference(cnf_transformation,[],[f208]) ).
fof(f423,plain,
sz00 != xp,
inference(cnf_transformation,[],[f208]) ).
fof(f424,plain,
aInteger0(xp),
inference(cnf_transformation,[],[f208]) ).
fof(f432,plain,
! [X0,X1] :
( ~ aInteger0(X0)
| ~ aInteger0(X1)
| sdtasdt0(xp,X1) != sdtpldt0(X0,smndt0(sz10))
| sz10 = X0
| smndt0(sz10) = X0 ),
inference(cnf_transformation,[],[f121]) ).
fof(f453,plain,
! [X4] :
( aElementOf0(X4,stldt0(sbsmnsldt0(cS2043)))
| smndt0(sz10) != X4 ),
inference(definition_unfolding,[],[f346,f333]) ).
fof(f455,plain,
cS2076 = stldt0(sbsmnsldt0(cS2043)),
inference(definition_unfolding,[],[f344,f333]) ).
fof(f493,plain,
! [X6] :
( ~ aElementOf0(X6,stldt0(sbsmnsldt0(cS2043)))
| aInteger0(X6) ),
inference(definition_unfolding,[],[f407,f333]) ).
fof(f514,plain,
aElementOf0(smndt0(sz10),stldt0(sbsmnsldt0(cS2043))),
inference(equality_resolution,[],[f453]) ).
fof(f515,definition,
! [X1] : sF37(X1) = sdtasdt0(xp,X1),
introduced(definition,[new_symbols(definition,[sF37])],[function_definition]) ).
fof(f516,plain,
! [X1] : sdtasdt0(xp,X1) = sF37(X1),
inference(reorient_equations,[],[f515]) ).
fof(f517,definition,
sF38 = smndt0(sz10),
introduced(definition,[new_symbols(definition,[sF38])],[function_definition]) ).
fof(f518,plain,
smndt0(sz10) = sF38,
inference(reorient_equations,[],[f517]) ).
fof(f519,definition,
! [X0] : sF39(X0) = sdtpldt0(X0,sF38),
introduced(definition,[new_symbols(definition,[sF39])],[function_definition]) ).
fof(f520,plain,
! [X0] : sdtpldt0(X0,sF38) = sF39(X0),
inference(reorient_equations,[],[f519]) ).
fof(f521,plain,
! [X0,X1] :
( sF37(X1) != sF39(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X0)
| sz10 = X0
| sF38 = X0 ),
inference(definition_folding,[],[f432,f518,f520,f518,f516]) ).
fof(f531,plain,
aElementOf0(smndt0(sz10),cS2076),
inference(forward_demodulation,[],[f514,f455]) ).
fof(f554,definition,
( spl41_6
<=> aInteger0(sz10) ),
introduced(definition,[new_symbols(definition,[spl41_6])],[avatar_definition]) ).
fof(f555,plain,
( aInteger0(sz10)
| ~ spl41_6 ),
inference(avatar_component_clause,[],[f554]) ).
fof(f561,plain,
spl41_6,
inference(avatar_split_clause,[],[f210,f554]) ).
fof(f563,plain,
aElementOf0(sF38,cS2076),
inference(forward_demodulation,[],[f531,f518]) ).
fof(f584,plain,
xp = sdtasdt0(sz10,xp),
inference(resolution,[],[f222,f424]) ).
fof(f594,plain,
xp = sdtasdt0(xp,sz10),
inference(resolution,[],[f223,f424]) ).
fof(f595,plain,
xp = sF37(sz10),
inference(forward_demodulation,[],[f594,f516]) ).
fof(f597,plain,
! [X0] :
( xp != sF39(X0)
| ~ aInteger0(sz10)
| ~ aInteger0(X0)
| sz10 = X0
| sF38 = X0 ),
inference(superposition,[],[f521,f595]) ).
fof(f598,plain,
( ! [X0] :
( xp != sF39(X0)
| ~ aInteger0(X0)
| sz10 = X0
| sF38 = X0 )
| ~ spl41_6 ),
inference(forward_subsumption_resolution,[],[f597,f555]) ).
fof(f606,plain,
xp = sdtpldt0(xp,sz00),
inference(resolution,[],[f217,f424]) ).
fof(f610,plain,
! [X0] :
( ~ aElementOf0(X0,cS2076)
| aInteger0(X0) ),
inference(superposition,[],[f493,f455]) ).
fof(f626,plain,
( sz10 = sdtpldt0(sz00,sz10)
| ~ spl41_6 ),
inference(resolution,[],[f555,f216]) ).
fof(f632,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,xp) = sdtpldt0(xp,X0) ),
inference(resolution,[],[f215,f424]) ).
fof(f633,plain,
( ! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,sz10) = sdtpldt0(sz10,X0) )
| ~ spl41_6 ),
inference(resolution,[],[f215,f555]) ).
fof(f634,plain,
( sdtpldt0(xp,sz10) = sdtpldt0(sz10,xp)
| ~ spl41_6 ),
inference(resolution,[],[f633,f424]) ).
fof(f645,plain,
! [X0] :
( aInteger0(sF39(X0))
| ~ aInteger0(X0)
| ~ aInteger0(sF38) ),
inference(superposition,[],[f212,f520]) ).
fof(f651,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| sdtasdt0(X0,sdtpldt0(X1,xp)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,xp)) ),
inference(resolution,[],[f225,f424]) ).
fof(f707,plain,
! [X0] :
( sz00 != sF37(X0)
| sz00 = X0
| sz00 = xp
| ~ aInteger0(xp)
| ~ aInteger0(X0) ),
inference(superposition,[],[f230,f516]) ).
fof(f711,plain,
! [X0] :
( sz00 != sF37(X0)
| sz00 = X0
| ~ aInteger0(xp)
| ~ aInteger0(X0) ),
inference(forward_subsumption_resolution,[],[f707,f423]) ).
fof(f712,plain,
! [X0] :
( sz00 != sF37(X0)
| sz00 = X0
| ~ aInteger0(X0) ),
inference(forward_subsumption_resolution,[],[f711,f424]) ).
fof(f725,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(xp,X0) = sdtasdt0(X0,xp) ),
inference(resolution,[],[f221,f424]) ).
fof(f729,plain,
! [X0] :
( ~ aInteger0(X0)
| sF37(X0) = sdtasdt0(X0,xp) ),
inference(forward_demodulation,[],[f725,f516]) ).
fof(f751,plain,
sz00 = sdtasdt0(sz00,xp),
inference(resolution,[],[f226,f424]) ).
fof(f755,plain,
smndt0(xp) = sdtasdt0(smndt0(sz10),xp),
inference(resolution,[],[f229,f424]) ).
fof(f762,plain,
smndt0(xp) = sdtasdt0(sF38,xp),
inference(forward_demodulation,[],[f755,f518]) ).
fof(f764,plain,
( sz00 != smndt0(xp)
| sz00 = xp
| sz00 = sF38
| ~ aInteger0(sF38)
| ~ aInteger0(xp) ),
inference(superposition,[],[f230,f762]) ).
fof(f767,plain,
( ! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(X0,sdtpldt0(sz10,xp)) = sdtpldt0(sdtasdt0(X0,sz10),sdtasdt0(X0,xp)) )
| ~ spl41_6 ),
inference(resolution,[],[f651,f555]) ).
fof(f771,plain,
( sdtasdt0(xp,sdtpldt0(sz10,xp)) = sdtpldt0(sdtasdt0(xp,sz10),sdtasdt0(xp,xp))
| ~ spl41_6 ),
inference(resolution,[],[f767,f424]) ).
fof(f777,plain,
( sdtasdt0(xp,sdtpldt0(sz10,xp)) = sdtpldt0(sdtasdt0(xp,sz10),sF37(xp))
| ~ spl41_6 ),
inference(forward_demodulation,[],[f771,f516]) ).
fof(f780,plain,
( sdtasdt0(xp,sdtpldt0(sz10,xp)) = sdtpldt0(sF37(sz10),sF37(xp))
| ~ spl41_6 ),
inference(forward_demodulation,[],[f777,f516]) ).
fof(f781,plain,
( sdtasdt0(xp,sdtpldt0(sz10,xp)) = sdtpldt0(xp,sF37(xp))
| ~ spl41_6 ),
inference(forward_demodulation,[],[f780,f595]) ).
fof(f782,plain,
( sdtpldt0(xp,sF37(xp)) = sF37(sdtpldt0(sz10,xp))
| ~ spl41_6 ),
inference(forward_demodulation,[],[f781,f516]) ).
fof(f788,definition,
( spl41_13
<=> aInteger0(sdtpldt0(sz10,xp)) ),
introduced(definition,[new_symbols(definition,[spl41_13])],[avatar_definition]) ).
fof(f789,plain,
( aInteger0(sdtpldt0(sz10,xp))
| ~ spl41_13 ),
inference(avatar_component_clause,[],[f788]) ).
fof(f790,plain,
( ~ aInteger0(sdtpldt0(sz10,xp))
| spl41_13 ),
inference(avatar_component_clause,[],[f788]) ).
fof(f812,plain,
( ~ aInteger0(sz10)
| ~ aInteger0(xp)
| spl41_13 ),
inference(resolution,[],[f790,f212]) ).
fof(f813,plain,
( ~ aInteger0(xp)
| ~ spl41_6
| spl41_13 ),
inference(forward_subsumption_resolution,[],[f812,f555]) ).
fof(f814,plain,
( $false
| ~ spl41_6
| spl41_13 ),
inference(forward_subsumption_resolution,[],[f813,f424]) ).
fof(f815,plain,
( ~ spl41_6
| spl41_13 ),
inference(avatar_contradiction_clause,[],[f814]) ).
fof(f840,plain,
aInteger0(sF38),
inference(resolution,[],[f610,f563]) ).
fof(f846,definition,
( spl41_19
<=> aInteger0(sF38) ),
introduced(definition,[new_symbols(definition,[spl41_19])],[avatar_definition]) ).
fof(f847,plain,
( aInteger0(sF38)
| ~ spl41_19 ),
inference(avatar_component_clause,[],[f846]) ).
fof(f850,definition,
( spl41_20
<=> ! [X0] :
( aInteger0(sF39(X0))
| ~ aInteger0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl41_20])],[avatar_definition]) ).
fof(f851,plain,
( ! [X0] :
( aInteger0(sF39(X0))
| ~ aInteger0(X0) )
| ~ spl41_20 ),
inference(avatar_component_clause,[],[f850]) ).
fof(f852,plain,
( ~ spl41_19
| spl41_20 ),
inference(avatar_split_clause,[],[f645,f850,f846]) ).
fof(f853,plain,
( sz00 != smndt0(xp)
| sz00 = sF38
| ~ aInteger0(sF38)
| ~ aInteger0(xp) ),
inference(forward_subsumption_resolution,[],[f764,f423]) ).
fof(f856,plain,
spl41_19,
inference(avatar_split_clause,[],[f840,f846]) ).
fof(f858,plain,
( sz00 != smndt0(xp)
| sz00 = sF38
| ~ aInteger0(sF38) ),
inference(forward_subsumption_resolution,[],[f853,f424]) ).
fof(f860,definition,
( spl41_21
<=> sz00 = sF38 ),
introduced(definition,[new_symbols(definition,[spl41_21])],[avatar_definition]) ).
fof(f862,plain,
( sz00 = sF38
| ~ spl41_21 ),
inference(avatar_component_clause,[],[f860]) ).
fof(f874,definition,
( spl41_24
<=> sz00 = smndt0(xp) ),
introduced(definition,[new_symbols(definition,[spl41_24])],[avatar_definition]) ).
fof(f876,plain,
( sz00 != smndt0(xp)
| spl41_24 ),
inference(avatar_component_clause,[],[f874]) ).
fof(f877,plain,
( ~ spl41_19
| spl41_21
| ~ spl41_24 ),
inference(avatar_split_clause,[],[f858,f874,f860,f846]) ).
fof(f888,plain,
( sdtpldt0(sF38,sz10) = sdtpldt0(sz10,sF38)
| ~ spl41_6
| ~ spl41_19 ),
inference(resolution,[],[f847,f633]) ).
fof(f893,plain,
( sdtasdt0(sF38,xp) = sF37(sF38)
| ~ spl41_19 ),
inference(resolution,[],[f847,f729]) ).
fof(f896,plain,
( smndt0(xp) = sF37(sF38)
| ~ spl41_19 ),
inference(forward_demodulation,[],[f893,f762]) ).
fof(f899,plain,
( sdtpldt0(sF38,sz10) = sF39(sz10)
| ~ spl41_6
| ~ spl41_19 ),
inference(forward_demodulation,[],[f888,f520]) ).
fof(f914,plain,
( ! [X0] :
( sF39(X0) != smndt0(xp)
| ~ aInteger0(sF38)
| ~ aInteger0(X0)
| sz10 = X0
| sF38 = X0 )
| ~ spl41_19 ),
inference(superposition,[],[f521,f896]) ).
fof(f915,plain,
( ! [X0] :
( sF39(X0) != smndt0(xp)
| ~ aInteger0(X0)
| sz10 = X0
| sF38 = X0 )
| ~ spl41_19 ),
inference(forward_subsumption_resolution,[],[f914,f847]) ).
fof(f960,definition,
( spl41_29
<=> sz00 = sz10 ),
introduced(definition,[new_symbols(definition,[spl41_29])],[avatar_definition]) ).
fof(f961,plain,
( sz00 != sz10
| spl41_29 ),
inference(avatar_component_clause,[],[f960]) ).
fof(f962,plain,
( sz00 = sz10
| ~ spl41_29 ),
inference(avatar_component_clause,[],[f960]) ).
fof(f1150,plain,
( xp = sdtasdt0(sz00,xp)
| ~ spl41_29 ),
inference(superposition,[],[f584,f962]) ).
fof(f1186,plain,
( sz00 = xp
| ~ spl41_29 ),
inference(forward_demodulation,[],[f1150,f751]) ).
fof(f1199,plain,
( $false
| ~ spl41_29 ),
inference(forward_subsumption_resolution,[],[f1186,f423]) ).
fof(f1200,plain,
~ spl41_29,
inference(avatar_contradiction_clause,[],[f1199]) ).
fof(f1288,plain,
( ! [X0,X1] :
( ~ aInteger0(X0)
| ~ aInteger0(X1)
| sdtpldt0(X0,sdtpldt0(X1,sF38)) = sdtpldt0(sdtpldt0(X0,X1),sF38) )
| ~ spl41_19 ),
inference(resolution,[],[f214,f847]) ).
fof(f1289,plain,
( ! [X0,X1] :
( sF39(sdtpldt0(X0,X1)) = sdtpldt0(X0,sdtpldt0(X1,sF38))
| ~ aInteger0(X0)
| ~ aInteger0(X1) )
| ~ spl41_19 ),
inference(forward_demodulation,[],[f1288,f520]) ).
fof(f1290,plain,
( ! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| sF39(sdtpldt0(X0,X1)) = sdtpldt0(X0,sF39(X1)) )
| ~ spl41_19 ),
inference(forward_demodulation,[],[f1289,f520]) ).
fof(f1291,plain,
( ! [X0] :
( ~ aInteger0(X0)
| sF39(sdtpldt0(X0,sz10)) = sdtpldt0(X0,sF39(sz10)) )
| ~ spl41_6
| ~ spl41_19 ),
inference(resolution,[],[f1290,f555]) ).
fof(f1296,plain,
( ! [X0] :
( ~ aInteger0(X0)
| sF39(sdtpldt0(X0,xp)) = sdtpldt0(X0,sF39(xp)) )
| ~ spl41_19 ),
inference(resolution,[],[f1290,f424]) ).
fof(f1297,plain,
( ! [X0] :
( ~ aInteger0(X0)
| sF39(sdtpldt0(X0,sF38)) = sdtpldt0(X0,sF39(sF38)) )
| ~ spl41_19 ),
inference(resolution,[],[f1290,f847]) ).
fof(f1298,plain,
( ! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,sF39(sF38)) = sF39(sF39(X0)) )
| ~ spl41_19 ),
inference(forward_demodulation,[],[f1297,f520]) ).
fof(f1304,plain,
( sF39(sdtpldt0(xp,sz10)) = sdtpldt0(xp,sF39(sz10))
| ~ spl41_6
| ~ spl41_19 ),
inference(resolution,[],[f1291,f424]) ).
fof(f1307,plain,
( sF39(sdtpldt0(sz10,xp)) = sdtpldt0(xp,sF39(sz10))
| ~ spl41_6
| ~ spl41_19 ),
inference(forward_demodulation,[],[f1304,f634]) ).
fof(f1311,plain,
( sF39(sdtpldt0(sz10,xp)) = sdtpldt0(sz10,sF39(xp))
| ~ spl41_6
| ~ spl41_19 ),
inference(resolution,[],[f1296,f555]) ).
fof(f1322,plain,
( sdtpldt0(xp,sF39(sz10)) = sdtpldt0(sz10,sF39(xp))
| ~ spl41_6
| ~ spl41_19 ),
inference(forward_demodulation,[],[f1311,f1307]) ).
fof(f1483,plain,
( xp != sdtpldt0(xp,sF39(sz10))
| ~ aInteger0(sdtpldt0(sz10,xp))
| sz10 = sdtpldt0(sz10,xp)
| sF38 = sdtpldt0(sz10,xp)
| ~ spl41_6
| ~ spl41_19 ),
inference(superposition,[],[f598,f1307]) ).
fof(f1508,plain,
( xp != sdtpldt0(xp,sF39(sz10))
| sz10 = sdtpldt0(sz10,xp)
| sF38 = sdtpldt0(sz10,xp)
| ~ spl41_6
| ~ spl41_13
| ~ spl41_19 ),
inference(forward_subsumption_resolution,[],[f1483,f789]) ).
fof(f1527,plain,
( xp != sdtpldt0(sz10,sF39(xp))
| sz10 = sdtpldt0(sz10,xp)
| sF38 = sdtpldt0(sz10,xp)
| ~ spl41_6
| ~ spl41_13
| ~ spl41_19 ),
inference(forward_demodulation,[],[f1508,f1322]) ).
fof(f1553,definition,
( spl41_70
<=> sF38 = sdtpldt0(sz10,xp) ),
introduced(definition,[new_symbols(definition,[spl41_70])],[avatar_definition]) ).
fof(f1555,plain,
( sF38 = sdtpldt0(sz10,xp)
| ~ spl41_70 ),
inference(avatar_component_clause,[],[f1553]) ).
fof(f1557,definition,
( spl41_71
<=> sz10 = sdtpldt0(sz10,xp) ),
introduced(definition,[new_symbols(definition,[spl41_71])],[avatar_definition]) ).
fof(f1559,plain,
( sz10 = sdtpldt0(sz10,xp)
| ~ spl41_71 ),
inference(avatar_component_clause,[],[f1557]) ).
fof(f1569,definition,
( spl41_73
<=> xp = sdtpldt0(sz10,sF39(xp)) ),
introduced(definition,[new_symbols(definition,[spl41_73])],[avatar_definition]) ).
fof(f1570,plain,
( xp = sdtpldt0(sz10,sF39(xp))
| ~ spl41_73 ),
inference(avatar_component_clause,[],[f1569]) ).
fof(f1571,plain,
( xp != sdtpldt0(sz10,sF39(xp))
| spl41_73 ),
inference(avatar_component_clause,[],[f1569]) ).
fof(f1581,plain,
( spl41_70
| spl41_71
| ~ spl41_73
| ~ spl41_6
| ~ spl41_13
| ~ spl41_19 ),
inference(avatar_split_clause,[],[f1527,f846,f788,f554,f1569,f1557,f1553]) ).
fof(f1943,definition,
( spl41_84
<=> sz10 = sF39(sz10) ),
introduced(definition,[new_symbols(definition,[spl41_84])],[avatar_definition]) ).
fof(f1945,plain,
( sz10 = sF39(sz10)
| ~ spl41_84 ),
inference(avatar_component_clause,[],[f1943]) ).
fof(f2340,plain,
( sdtpldt0(sz00,sz10) = sF39(sz10)
| ~ spl41_6
| ~ spl41_19
| ~ spl41_21 ),
inference(superposition,[],[f899,f862]) ).
fof(f2372,plain,
( sz10 = sF39(sz10)
| ~ spl41_6
| ~ spl41_19
| ~ spl41_21 ),
inference(forward_demodulation,[],[f2340,f626]) ).
fof(f2382,plain,
( spl41_84
| ~ spl41_6
| ~ spl41_19
| ~ spl41_21 ),
inference(avatar_split_clause,[],[f2372,f860,f846,f554,f1943]) ).
fof(f3267,plain,
( sz00 = sdtpldt0(smndt0(sz10),sz10)
| ~ spl41_6 ),
inference(resolution,[],[f218,f555]) ).
fof(f3281,plain,
( sz00 = sdtpldt0(sF38,sz10)
| ~ spl41_6 ),
inference(forward_demodulation,[],[f3267,f518]) ).
fof(f3284,plain,
( sz00 = sF39(sz10)
| ~ spl41_6
| ~ spl41_19 ),
inference(forward_demodulation,[],[f3281,f899]) ).
fof(f3287,plain,
( sz00 = sz10
| ~ spl41_6
| ~ spl41_19
| ~ spl41_84 ),
inference(forward_demodulation,[],[f3284,f1945]) ).
fof(f3290,plain,
( $false
| ~ spl41_6
| ~ spl41_19
| spl41_29
| ~ spl41_84 ),
inference(forward_subsumption_resolution,[],[f3287,f961]) ).
fof(f3291,plain,
( ~ spl41_6
| ~ spl41_19
| spl41_29
| ~ spl41_84 ),
inference(avatar_contradiction_clause,[],[f3290]) ).
fof(f3469,plain,
( sdtpldt0(xp,sz00) = sdtpldt0(sz10,sF39(xp))
| ~ spl41_6
| ~ spl41_19 ),
inference(superposition,[],[f1322,f3284]) ).
fof(f3490,plain,
( xp = sdtpldt0(sz10,sF39(xp))
| ~ spl41_6
| ~ spl41_19 ),
inference(forward_demodulation,[],[f3469,f606]) ).
fof(f3498,plain,
( $false
| ~ spl41_6
| ~ spl41_19
| spl41_73 ),
inference(forward_subsumption_resolution,[],[f3490,f1571]) ).
fof(f3499,plain,
( ~ spl41_6
| ~ spl41_19
| spl41_73 ),
inference(avatar_contradiction_clause,[],[f3498]) ).
fof(f3556,plain,
( sF39(sF38) = sdtpldt0(xp,sF39(sz10))
| ~ spl41_6
| ~ spl41_19
| ~ spl41_70 ),
inference(superposition,[],[f1307,f1555]) ).
fof(f3561,plain,
( sF39(sF38) = sdtpldt0(sz10,sF39(xp))
| ~ spl41_6
| ~ spl41_19
| ~ spl41_70 ),
inference(forward_demodulation,[],[f3556,f1322]) ).
fof(f3564,plain,
( xp = sF39(sF38)
| ~ spl41_6
| ~ spl41_19
| ~ spl41_70
| ~ spl41_73 ),
inference(forward_demodulation,[],[f3561,f1570]) ).
fof(f3884,plain,
( sF39(sz10) = sdtpldt0(xp,sF39(sz10))
| ~ spl41_6
| ~ spl41_19
| ~ spl41_71 ),
inference(superposition,[],[f1307,f1559]) ).
fof(f3888,plain,
( sF39(sz10) = sdtpldt0(sz10,sF39(xp))
| ~ spl41_6
| ~ spl41_19
| ~ spl41_71 ),
inference(forward_demodulation,[],[f3884,f1322]) ).
fof(f3893,plain,
( xp = sF39(sz10)
| ~ spl41_6
| ~ spl41_19
| ~ spl41_71
| ~ spl41_73 ),
inference(forward_demodulation,[],[f3888,f1570]) ).
fof(f3895,plain,
( sz00 = xp
| ~ spl41_6
| ~ spl41_19
| ~ spl41_71
| ~ spl41_73 ),
inference(forward_demodulation,[],[f3893,f3284]) ).
fof(f3897,plain,
( $false
| ~ spl41_6
| ~ spl41_19
| ~ spl41_71
| ~ spl41_73 ),
inference(forward_subsumption_resolution,[],[f3895,f423]) ).
fof(f3898,plain,
( ~ spl41_6
| ~ spl41_19
| ~ spl41_71
| ~ spl41_73 ),
inference(avatar_contradiction_clause,[],[f3897]) ).
fof(f4238,plain,
( sdtpldt0(xp,sF37(xp)) = sF37(sF38)
| ~ spl41_6
| ~ spl41_70 ),
inference(superposition,[],[f782,f1555]) ).
fof(f4250,plain,
( smndt0(xp) = sdtpldt0(xp,sF37(xp))
| ~ spl41_6
| ~ spl41_19
| ~ spl41_70 ),
inference(forward_demodulation,[],[f4238,f896]) ).
fof(f5164,plain,
! [X0] :
( aInteger0(sF37(X0))
| ~ aInteger0(xp)
| ~ aInteger0(X0) ),
inference(superposition,[],[f213,f516]) ).
fof(f5176,plain,
! [X0] :
( aInteger0(sF37(X0))
| ~ aInteger0(X0) ),
inference(forward_subsumption_resolution,[],[f5164,f424]) ).
fof(f5759,definition,
( spl41_153
<=> sz00 = sF37(xp) ),
introduced(definition,[new_symbols(definition,[spl41_153])],[avatar_definition]) ).
fof(f5760,plain,
( sz00 != sF37(xp)
| spl41_153 ),
inference(avatar_component_clause,[],[f5759]) ).
fof(f5761,plain,
( sz00 = sF37(xp)
| ~ spl41_153 ),
inference(avatar_component_clause,[],[f5759]) ).
fof(f5763,definition,
( spl41_154
<=> aInteger0(sF37(xp)) ),
introduced(definition,[new_symbols(definition,[spl41_154])],[avatar_definition]) ).
fof(f5764,plain,
( aInteger0(sF37(xp))
| ~ spl41_154 ),
inference(avatar_component_clause,[],[f5763]) ).
fof(f5765,plain,
( ~ aInteger0(sF37(xp))
| spl41_154 ),
inference(avatar_component_clause,[],[f5763]) ).
fof(f5808,plain,
( ~ aInteger0(xp)
| spl41_154 ),
inference(resolution,[],[f5765,f5176]) ).
fof(f5809,plain,
( $false
| spl41_154 ),
inference(forward_subsumption_resolution,[],[f5808,f424]) ).
fof(f5810,plain,
spl41_154,
inference(avatar_contradiction_clause,[],[f5809]) ).
fof(f5825,plain,
( sz00 != sz00
| sz00 = xp
| ~ aInteger0(xp)
| ~ spl41_153 ),
inference(superposition,[],[f712,f5761]) ).
fof(f5830,plain,
( sz00 = xp
| ~ aInteger0(xp)
| ~ spl41_153 ),
inference(trivial_inequality_removal,[],[f5825]) ).
fof(f5831,plain,
( ~ aInteger0(xp)
| ~ spl41_153 ),
inference(forward_subsumption_resolution,[],[f5830,f423]) ).
fof(f5841,plain,
( $false
| ~ spl41_153 ),
inference(forward_subsumption_resolution,[],[f5831,f424]) ).
fof(f5842,plain,
~ spl41_153,
inference(avatar_contradiction_clause,[],[f5841]) ).
fof(f6006,plain,
( sF37(xp) = sdtpldt0(sF37(xp),sz00)
| ~ spl41_154 ),
inference(resolution,[],[f5764,f217]) ).
fof(f6018,plain,
( sdtpldt0(xp,sF37(xp)) = sdtpldt0(sF37(xp),xp)
| ~ spl41_154 ),
inference(resolution,[],[f5764,f632]) ).
fof(f6019,plain,
( sdtpldt0(sF37(xp),sz10) = sdtpldt0(sz10,sF37(xp))
| ~ spl41_6
| ~ spl41_154 ),
inference(resolution,[],[f5764,f633]) ).
fof(f6032,plain,
( ! [X0] :
( ~ aInteger0(X0)
| sF39(sdtpldt0(X0,sF37(xp))) = sdtpldt0(X0,sF39(sF37(xp))) )
| ~ spl41_19
| ~ spl41_154 ),
inference(resolution,[],[f5764,f1290]) ).
fof(f6033,plain,
( sF39(sdtpldt0(sF37(xp),sz10)) = sdtpldt0(sF37(xp),sF39(sz10))
| ~ spl41_6
| ~ spl41_19
| ~ spl41_154 ),
inference(resolution,[],[f5764,f1291]) ).
fof(f6035,plain,
( sdtpldt0(sF37(xp),sF39(sF38)) = sF39(sF39(sF37(xp)))
| ~ spl41_19
| ~ spl41_154 ),
inference(resolution,[],[f5764,f1298]) ).
fof(f6057,plain,
( sdtpldt0(sF37(xp),xp) = sF39(sF39(sF37(xp)))
| ~ spl41_6
| ~ spl41_19
| ~ spl41_70
| ~ spl41_73
| ~ spl41_154 ),
inference(forward_demodulation,[],[f6035,f3564]) ).
fof(f6058,plain,
( sdtpldt0(sF37(xp),sz00) = sF39(sdtpldt0(sF37(xp),sz10))
| ~ spl41_6
| ~ spl41_19
| ~ spl41_154 ),
inference(forward_demodulation,[],[f6033,f3284]) ).
fof(f6063,plain,
( smndt0(xp) = sdtpldt0(sF37(xp),xp)
| ~ spl41_6
| ~ spl41_19
| ~ spl41_70
| ~ spl41_154 ),
inference(forward_demodulation,[],[f6018,f4250]) ).
fof(f6070,plain,
( sdtpldt0(sF37(xp),sz00) = sF39(sdtpldt0(sz10,sF37(xp)))
| ~ spl41_6
| ~ spl41_19
| ~ spl41_154 ),
inference(forward_demodulation,[],[f6058,f6019]) ).
fof(f6076,plain,
( sF37(xp) = sF39(sdtpldt0(sz10,sF37(xp)))
| ~ spl41_6
| ~ spl41_19
| ~ spl41_154 ),
inference(forward_demodulation,[],[f6070,f6006]) ).
fof(f6217,plain,
( sF39(sdtpldt0(sz10,sF37(xp))) = sdtpldt0(sz10,sF39(sF37(xp)))
| ~ spl41_6
| ~ spl41_19
| ~ spl41_154 ),
inference(resolution,[],[f6032,f555]) ).
fof(f6238,plain,
( sF37(xp) = sdtpldt0(sz10,sF39(sF37(xp)))
| ~ spl41_6
| ~ spl41_19
| ~ spl41_154 ),
inference(forward_demodulation,[],[f6217,f6076]) ).
fof(f10078,plain,
( smndt0(xp) != sdtpldt0(sF37(xp),xp)
| ~ aInteger0(sF39(sF37(xp)))
| sz10 = sF39(sF37(xp))
| sF38 = sF39(sF37(xp))
| ~ spl41_6
| ~ spl41_19
| ~ spl41_70
| ~ spl41_73
| ~ spl41_154 ),
inference(superposition,[],[f915,f6057]) ).
fof(f10083,plain,
( ~ aInteger0(sF39(sF37(xp)))
| sz10 = sF39(sF37(xp))
| sF38 = sF39(sF37(xp))
| ~ spl41_6
| ~ spl41_19
| ~ spl41_70
| ~ spl41_73
| ~ spl41_154 ),
inference(forward_subsumption_resolution,[],[f10078,f6063]) ).
fof(f10102,definition,
( spl41_216
<=> aInteger0(sF39(sF37(xp))) ),
introduced(definition,[new_symbols(definition,[spl41_216])],[avatar_definition]) ).
fof(f10104,plain,
( ~ aInteger0(sF39(sF37(xp)))
| spl41_216 ),
inference(avatar_component_clause,[],[f10102]) ).
fof(f10116,definition,
( spl41_219
<=> sF38 = sF39(sF37(xp)) ),
introduced(definition,[new_symbols(definition,[spl41_219])],[avatar_definition]) ).
fof(f10118,plain,
( sF38 = sF39(sF37(xp))
| ~ spl41_219 ),
inference(avatar_component_clause,[],[f10116]) ).
fof(f10120,definition,
( spl41_220
<=> sz10 = sF39(sF37(xp)) ),
introduced(definition,[new_symbols(definition,[spl41_220])],[avatar_definition]) ).
fof(f10122,plain,
( sz10 = sF39(sF37(xp))
| ~ spl41_220 ),
inference(avatar_component_clause,[],[f10120]) ).
fof(f10123,plain,
( spl41_219
| spl41_220
| ~ spl41_216
| ~ spl41_6
| ~ spl41_19
| ~ spl41_70
| ~ spl41_73
| ~ spl41_154 ),
inference(avatar_split_clause,[],[f10083,f5763,f1569,f1553,f846,f554,f10102,f10120,f10116]) ).
fof(f10142,plain,
( ~ aInteger0(sF37(xp))
| ~ spl41_20
| spl41_216 ),
inference(resolution,[],[f10104,f851]) ).
fof(f10143,plain,
( $false
| ~ spl41_20
| ~ spl41_154
| spl41_216 ),
inference(forward_subsumption_resolution,[],[f10142,f5764]) ).
fof(f10144,plain,
( ~ spl41_20
| ~ spl41_154
| spl41_216 ),
inference(avatar_contradiction_clause,[],[f10143]) ).
fof(f10148,plain,
( sF37(xp) = sdtpldt0(sz10,sF38)
| ~ spl41_6
| ~ spl41_19
| ~ spl41_154
| ~ spl41_219 ),
inference(superposition,[],[f6238,f10118]) ).
fof(f10172,plain,
( sF37(xp) = sF39(sz10)
| ~ spl41_6
| ~ spl41_19
| ~ spl41_154
| ~ spl41_219 ),
inference(forward_demodulation,[],[f10148,f520]) ).
fof(f10198,plain,
( sz00 = sF37(xp)
| ~ spl41_6
| ~ spl41_19
| ~ spl41_154
| ~ spl41_219 ),
inference(forward_demodulation,[],[f10172,f3284]) ).
fof(f10201,plain,
( $false
| ~ spl41_6
| ~ spl41_19
| spl41_153
| ~ spl41_154
| ~ spl41_219 ),
inference(forward_subsumption_resolution,[],[f10198,f5760]) ).
fof(f10202,plain,
( ~ spl41_6
| ~ spl41_19
| spl41_153
| ~ spl41_154
| ~ spl41_219 ),
inference(avatar_contradiction_clause,[],[f10201]) ).
fof(f10207,plain,
( sF39(sz10) = sdtpldt0(sF37(xp),xp)
| ~ spl41_6
| ~ spl41_19
| ~ spl41_70
| ~ spl41_73
| ~ spl41_154
| ~ spl41_220 ),
inference(superposition,[],[f6057,f10122]) ).
fof(f10233,plain,
( smndt0(xp) = sF39(sz10)
| ~ spl41_6
| ~ spl41_19
| ~ spl41_70
| ~ spl41_73
| ~ spl41_154
| ~ spl41_220 ),
inference(forward_demodulation,[],[f10207,f6063]) ).
fof(f10238,plain,
( sz00 = smndt0(xp)
| ~ spl41_6
| ~ spl41_19
| ~ spl41_70
| ~ spl41_73
| ~ spl41_154
| ~ spl41_220 ),
inference(forward_demodulation,[],[f10233,f3284]) ).
fof(f10243,plain,
( $false
| ~ spl41_6
| ~ spl41_19
| spl41_24
| ~ spl41_70
| ~ spl41_73
| ~ spl41_154
| ~ spl41_220 ),
inference(forward_subsumption_resolution,[],[f10238,f876]) ).
fof(f10244,plain,
( ~ spl41_6
| ~ spl41_19
| spl41_24
| ~ spl41_70
| ~ spl41_73
| ~ spl41_154
| ~ spl41_220 ),
inference(avatar_contradiction_clause,[],[f10243]) ).
cnf(s5,plain,
spl41_6,
inference(sat_conversion,[],[f561]) ).
cnf(s14,plain,
( ~ spl41_6
| spl41_13 ),
inference(sat_conversion,[],[f815]) ).
cnf(s16,plain,
( ~ spl41_19
| spl41_20 ),
inference(sat_conversion,[],[f852]) ).
cnf(s17,plain,
spl41_19,
inference(sat_conversion,[],[f856]) ).
cnf(s21,plain,
( ~ spl41_19
| spl41_21
| ~ spl41_24 ),
inference(sat_conversion,[],[f877]) ).
cnf(s44,plain,
~ spl41_29,
inference(sat_conversion,[],[f1200]) ).
cnf(s86,plain,
( ~ spl41_6
| ~ spl41_13
| ~ spl41_19
| spl41_70
| spl41_71
| ~ spl41_73 ),
inference(sat_conversion,[],[f1581]) ).
cnf(s151,plain,
( ~ spl41_6
| ~ spl41_19
| ~ spl41_21
| spl41_84 ),
inference(sat_conversion,[],[f2382]) ).
cnf(s178,plain,
( ~ spl41_6
| ~ spl41_19
| spl41_29
| ~ spl41_84 ),
inference(sat_conversion,[],[f3291]) ).
cnf(s184,plain,
( ~ spl41_6
| ~ spl41_19
| spl41_73 ),
inference(sat_conversion,[],[f3499]) ).
cnf(s221,plain,
( ~ spl41_6
| ~ spl41_19
| ~ spl41_71
| ~ spl41_73 ),
inference(sat_conversion,[],[f3898]) ).
cnf(s331,plain,
spl41_154,
inference(sat_conversion,[],[f5810]) ).
cnf(s332,plain,
~ spl41_153,
inference(sat_conversion,[],[f5842]) ).
cnf(s466,plain,
( ~ spl41_6
| ~ spl41_19
| ~ spl41_70
| ~ spl41_73
| ~ spl41_154
| ~ spl41_216
| spl41_219
| spl41_220 ),
inference(sat_conversion,[],[f10123]) ).
cnf(s479,plain,
( ~ spl41_20
| ~ spl41_154
| spl41_216 ),
inference(sat_conversion,[],[f10144]) ).
cnf(s484,plain,
( ~ spl41_6
| ~ spl41_19
| spl41_153
| ~ spl41_154
| ~ spl41_219 ),
inference(sat_conversion,[],[f10202]) ).
cnf(s491,plain,
( ~ spl41_6
| ~ spl41_19
| spl41_24
| ~ spl41_70
| ~ spl41_73
| ~ spl41_154
| ~ spl41_220 ),
inference(sat_conversion,[],[f10244]) ).
cnf(s508,plain,
spl41_20,
inference(rat,[],[s16,s17]) ).
cnf(s509,plain,
spl41_216,
inference(rat,[],[s479,s331,s508]) ).
cnf(s510,plain,
~ spl41_219,
inference(rat,[],[s484,s17,s331,s332,s5]) ).
cnf(s512,plain,
spl41_73,
inference(rat,[],[s184,s17,s5]) ).
cnf(s513,plain,
~ spl41_84,
inference(rat,[],[s178,s17,s44,s5]) ).
cnf(s514,plain,
~ spl41_21,
inference(rat,[],[s151,s513,s17,s5]) ).
cnf(s517,plain,
spl41_13,
inference(rat,[],[s14,s5]) ).
cnf(s519,plain,
~ spl41_71,
inference(rat,[],[s221,s5,s17,s512]) ).
cnf(s523,plain,
~ spl41_24,
inference(rat,[],[s21,s17,s514]) ).
cnf(s526,plain,
spl41_70,
inference(rat,[],[s86,s512,s519,s5,s17,s517]) ).
cnf(s543,plain,
spl41_220,
inference(rat,[],[s466,s512,s510,s509,s331,s5,s17,s526]) ).
cnf(s547,plain,
$false,
inference(rat,[],[s491,s523,s331,s512,s5,s17,s543,s526]) ).
fof(f10245,plain,
$false,
inference(avatar_sat_refutation,[],[s547]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM451+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.09/0.36 % Computer : n019.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 19:59:03 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 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
% 11.28/2.53 % (3372303)Detected formulas, will run a generic FOF schedule.
% 11.28/2.53 % (3372311)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3793750140:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.28/2.53 % (3372311)Instruction limit reached!
% 11.28/2.53 % (3372311)------------------------------
% 11.28/2.53 % (3372311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.28/2.53 % (3372311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.28/2.53 % (3372311)CaDiCaL version: 2.1.3
% 11.28/2.53 % (3372311)Termination reason: Instruction limit
% 11.28/2.53 % (3372311)Termination phase: Saturation
% 11.28/2.53 % (3372311)Time elapsed: 0.039 s
% 11.28/2.53 % (3372311)Peak memory usage: 90 MB
% 11.28/2.53 % (3372311)Instructions burned: 110 (million)
% 11.28/2.53 % (3372312)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=13717717:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.28/2.53 % (3372308)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=560381642:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.28/2.53 % (3372310)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=3159336808:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.28/2.53 % (3372314)dis-21_1_sil=8000:lcm=predicate:random_seed=4043301540: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)
% 11.28/2.53 % (3372309)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=2229988536:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.28/2.53 % (3372313)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3441005969:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.28/2.53 % (3372312)Instruction limit reached!
% 11.28/2.53 % (3372312)------------------------------
% 11.28/2.53 % (3372312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.28/2.53 % (3372312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.28/2.53 % (3372312)CaDiCaL version: 2.1.3
% 11.28/2.53 % (3372312)Termination reason: Instruction limit
% 11.28/2.53 % (3372312)Termination phase: Saturation
% 11.28/2.53 % (3372312)Time elapsed: 0.072 s
% 11.28/2.53 % (3372312)Peak memory usage: 88 MB
% 11.28/2.53 % (3372312)Instructions burned: 120 (million)
% 11.28/2.53 % (3372314)Instruction limit reached!
% 11.28/2.53 % (3372314)------------------------------
% 11.28/2.53 % (3372314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.28/2.53 % (3372314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.28/2.53 % (3372314)CaDiCaL version: 2.1.3
% 11.28/2.53 % (3372314)Termination reason: Instruction limit
% 11.28/2.53 % (3372314)Termination phase: Saturation
% 11.28/2.53 % (3372314)Time elapsed: 0.074 s
% 11.28/2.53 % (3372314)Peak memory usage: 89 MB
% 11.28/2.53 % (3372314)Instructions burned: 130 (million)
% 11.28/2.53 % (3372313)Instruction limit reached!
% 11.28/2.53 % (3372313)------------------------------
% 11.28/2.53 % (3372313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.28/2.53 % (3372313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.28/2.53 % (3372313)CaDiCaL version: 2.1.3
% 11.28/2.53 % (3372313)Termination reason: Instruction limit
% 11.28/2.53 % (3372313)Termination phase: Saturation
% 11.28/2.53 % (3372313)Time elapsed: 0.093 s
% 11.28/2.53 % (3372313)Peak memory usage: 90 MB
% 11.28/2.53 % (3372313)Instructions burned: 139 (million)
% 11.28/2.53 % (3372322)lrs+10_1_sil=8000:sp=occurrence:random_seed=1495907599:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 11.28/2.53 % (3372322)Instruction limit reached!
% 11.28/2.53 % (3372322)------------------------------
% 11.28/2.53 % (3372322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.28/2.53 % (3372322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.28/2.53 % (3372322)CaDiCaL version: 2.1.3
% 11.28/2.53 % (3372322)Termination reason: Instruction limit
% 11.28/2.53 % (3372322)Termination phase: Saturation
% 11.28/2.53 % (3372322)Time elapsed: 0.088 s
% 11.28/2.53 % (3372322)Peak memory usage: 92 MB
% 11.28/2.53 % (3372322)Instructions burned: 286 (million)
% 11.28/2.53 % (3372324)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4007629956:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 11.28/2.53 % (3372323)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3861430023:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 11.28/2.53 % (3372325)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3562797865:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 11.28/2.53 % (3372323)Instruction limit reached!
% 11.28/2.53 % (3372323)------------------------------
% 11.28/2.53 % (3372323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.28/2.53 % (3372323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.28/2.53 % (3372323)CaDiCaL version: 2.1.3
% 11.28/2.53 % (3372323)Termination reason: Instruction limit
% 11.28/2.53 % (3372323)Termination phase: Saturation
% 11.28/2.53 % (3372323)Time elapsed: 0.084 s
% 11.28/2.53 % (3372323)Peak memory usage: 91 MB
% 11.28/2.53 % (3372323)Instructions burned: 158 (million)
% 11.28/2.53 % (3372327)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=861320669:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 11.28/2.53 % (3372325)Instruction limit reached!
% 11.28/2.53 % (3372325)------------------------------
% 11.28/2.53 % (3372325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.28/2.53 % (3372325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.28/2.53 % (3372325)CaDiCaL version: 2.1.3
% 11.28/2.53 % (3372325)Termination reason: Instruction limit
% 11.28/2.53 % (3372325)Termination phase: Saturation
% 11.28/2.53 % (3372325)Time elapsed: 0.123 s
% 11.28/2.53 % (3372325)Peak memory usage: 96 MB
% 11.28/2.53 % (3372325)Instructions burned: 249 (million)
% 11.28/2.53 % (3372327)Instruction limit reached!
% 11.28/2.53 % (3372327)------------------------------
% 11.28/2.53 % (3372327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.28/2.53 % (3372327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.28/2.53 % (3372327)CaDiCaL version: 2.1.3
% 11.28/2.53 % (3372327)Termination reason: Instruction limit
% 11.28/2.53 % (3372327)Termination phase: Saturation
% 11.28/2.53 % (3372327)Time elapsed: 0.098 s
% 11.28/2.53 % (3372327)Peak memory usage: 90 MB
% 11.28/2.53 % (3372327)Instructions burned: 294 (million)
% 11.28/2.53 % (3372324)Instruction limit reached!
% 11.28/2.53 % (3372324)------------------------------
% 11.28/2.53 % (3372324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.28/2.53 % (3372324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.28/2.53 % (3372324)CaDiCaL version: 2.1.3
% 11.28/2.53 % (3372324)Termination reason: Instruction limit
% 11.28/2.53 % (3372324)Termination phase: Saturation
% 11.28/2.53 % (3372324)Time elapsed: 0.203 s
% 11.28/2.53 % (3372324)Peak memory usage: 92 MB
% 11.28/2.53 % (3372324)Instructions burned: 325 (million)
% 11.28/2.53 % (3372331)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3844092551:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 11.28/2.53 % (3372333)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3229657095:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 11.28/2.53 % (3372334)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1451413590:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 11.28/2.53 % (3372334)Instruction limit reached!
% 11.28/2.53 % (3372334)------------------------------
% 11.28/2.53 % (3372334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.28/2.53 % (3372334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.28/2.53 % (3372334)CaDiCaL version: 2.1.3
% 11.28/2.53 % (3372334)Termination reason: Instruction limit
% 11.28/2.53 % (3372334)Termination phase: Saturation
% 11.28/2.53 % (3372334)Time elapsed: 0.034 s
% 11.28/2.53 % (3372334)Peak memory usage: 89 MB
% 11.28/2.53 % (3372334)Instructions burned: 127 (million)
% 11.28/2.53 % (3372335)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4024079163:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 11.28/2.53 % (3372333)Instruction limit reached!
% 11.28/2.53 % (3372333)------------------------------
% 11.28/2.53 % (3372333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.28/2.53 % (3372333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.28/2.53 % (3372333)CaDiCaL version: 2.1.3
% 11.28/2.53 % (3372333)Termination reason: Instruction limit
% 11.28/2.53 % (3372333)Termination phase: Saturation
% 11.28/2.53 % (3372333)Time elapsed: 0.074 s
% 11.28/2.53 % (3372333)Peak memory usage: 90 MB
% 11.28/2.53 % (3372333)Instructions burned: 114 (million)
% 11.28/2.53 % (3372335)Instruction limit reached!
% 11.28/2.53 % (3372335)------------------------------
% 11.28/2.53 % (3372335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.28/2.53 % (3372335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.28/2.53 % (3372335)CaDiCaL version: 2.1.3
% 11.28/2.53 % (3372335)Termination reason: Instruction limit
% 11.28/2.53 % (3372335)Termination phase: Saturation
% 11.28/2.53 % (3372335)Time elapsed: 0.062 s
% 11.28/2.53 % (3372335)Peak memory usage: 89 MB
% 11.28/2.53 % (3372335)Instructions burned: 114 (million)
% 11.28/2.53 % (3372339)lrs+10_1_sil=8000:sp=occurrence:random_seed=1694657323:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 11.28/2.53 % (3372341)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2287102675:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 11.28/2.53 % (3372342)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3991418173:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 11.28/2.53 % (3372339)Instruction limit reached!
% 11.28/2.53 % (3372339)------------------------------
% 11.28/2.53 % (3372339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.28/2.53 % (3372339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.28/2.53 % (3372339)CaDiCaL version: 2.1.3
% 11.28/2.53 % (3372339)Termination reason: Instruction limit
% 11.28/2.53 % (3372339)Termination phase: Saturation
% 11.28/2.53 % (3372339)Time elapsed: 0.263 s
% 11.28/2.53 % (3372339)Peak memory usage: 97 MB
% 11.28/2.53 % (3372339)Instructions burned: 909 (million)
% 11.28/2.53 % (3372341)Instruction limit reached!
% 11.28/2.53 % (3372341)------------------------------
% 11.28/2.53 % (3372341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.28/2.53 % (3372341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.28/2.53 % (3372341)CaDiCaL version: 2.1.3
% 11.28/2.53 % (3372341)Termination reason: Instruction limit
% 11.28/2.53 % (3372341)Termination phase: Saturation
% 11.28/2.53 % (3372341)Time elapsed: 0.274 s
% 11.28/2.53 % (3372341)Peak memory usage: 92 MB
% 11.28/2.53 % (3372341)Instructions burned: 438 (million)
% 11.28/2.53 % (3372346)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1269514800:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 11.28/2.53 % (3372346)Instruction limit reached!
% 11.28/2.53 % (3372346)------------------------------
% 11.28/2.53 % (3372346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.28/2.53 % (3372346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.28/2.53 % (3372346)CaDiCaL version: 2.1.3
% 11.28/2.53 % (3372346)Termination reason: Instruction limit
% 11.28/2.53 % (3372346)Termination phase: Saturation
% 11.28/2.53 % (3372346)Time elapsed: 0.038 s
% 11.28/2.53 % (3372346)Peak memory usage: 93 MB
% 11.28/2.53 % (3372346)Instructions burned: 139 (million)
% 11.28/2.53 % (3372347)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1520575920:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 11.28/2.53 % (3372308)First to succeed.
% 11.28/2.53 % (3372349)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2293003613:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 11.28/2.53 % (3372308)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3372303"
% 11.28/2.53 % (3372308)Refutation found. Thanks to Tanya!
% 11.28/2.53 % SZS status Theorem for theBenchmark
% 11.28/2.53 % SZS output start Proof for theBenchmark
% See solution above
% 12.49/2.73 % (3372308)------------------------------
% 12.49/2.73 % (3372308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.73 % (3372308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.73 % (3372308)CaDiCaL version: 2.1.3
% 12.49/2.73 % (3372308)Termination reason: Refutation
% 12.49/2.73 % (3372308)Time elapsed: 1.249 s
% 12.49/2.73 % (3372308)Peak memory usage: 138 MB
% 12.49/2.73 % (3372308)Instructions burned: 1899 (million)
% 12.49/2.73 % (3372308)------------------------------
% 12.49/2.73 % (3372308)------------------------------
% 12.49/2.73 % (3372303)Success in time 1.681 s
% 12.49/2.73 % Vampire exiting
%------------------------------------------------------------------------------