%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM447+5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.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:13 PM UTC 2026
% Result : Theorem 9.90s 3.91s
% Output : Refutation 22.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 50
% Syntax : Number of formulae : 421 ( 34 unt; 30 def)
% Number of atoms : 1999 ( 391 equ)
% Maximal formula atoms : 38 ( 4 avg)
% Number of connectives : 2661 (1083 ~;1156 |; 344 &)
% ( 40 <=>; 38 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 38 ( 36 usr; 29 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 8 con; 0-3 aty)
% Number of variables : 465 ( 0 sgn 398 !; 67 ?)
% 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(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(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(f11,axiom,
! [X0,X1,X2] :
( ( aInteger0(X0)
& aInteger0(X1)
& aInteger0(X2) )
=> sdtasdt0(X0,sdtasdt0(X1,X2)) = sdtasdt0(sdtasdt0(X0,X1),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulAsso) ).
fof(f15,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',mMulMinOne) ).
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(f19,axiom,
! [X0,X1,X2] :
( ( aInteger0(X0)
& aInteger0(X1)
& aInteger0(X2)
& X2 != sz00 )
=> ( sdteqdtlpzmzozddtrp0(X0,X1,X2)
<=> aDivisorOf0(X2,sdtpldt0(X0,smndt0(X1))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mEquMod) ).
fof(f21,axiom,
! [X0,X1,X2] :
( ( aInteger0(X0)
& aInteger0(X1)
& aInteger0(X2)
& X2 != sz00 )
=> ( sdteqdtlpzmzozddtrp0(X0,X1,X2)
=> sdteqdtlpzmzozddtrp0(X1,X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mEquModSym) ).
fof(f23,axiom,
! [X0,X1,X2,X3] :
( ( aInteger0(X0)
& aInteger0(X1)
& aInteger0(X2)
& X2 != sz00
& aInteger0(X3)
& X3 != sz00 )
=> ( sdteqdtlpzmzozddtrp0(X0,X1,sdtasdt0(X2,X3))
=> ( sdteqdtlpzmzozddtrp0(X0,X1,X2)
& sdteqdtlpzmzozddtrp0(X0,X1,X3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mEquModMul) ).
fof(f25,axiom,
! [X0] :
( aInteger0(X0)
=> ( ? [X1] :
( aDivisorOf0(X1,X0)
& isPrime0(X1) )
<=> ( X0 != sz10
& X0 != smndt0(sz10) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mPrimeDivisor) ).
fof(f34,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1)
& X1 != sz00 )
=> ! [X2] :
( X2 = szAzrzSzezqlpdtcmdtrp0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aInteger0(X3)
& sdteqdtlpzmzozddtrp0(X3,X0,X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mArSeq) ).
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,
aInteger0(xn),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2106) ).
fof(f44,conjecture,
( ( ( ? [X0] :
( aElementOf0(X0,xS)
& aElementOf0(xn,X0) )
& aElementOf0(xn,sbsmnsldt0(xS)) )
=> ? [X0] :
( ( ( aInteger0(X0)
& X0 != sz00
& ? [X1] :
( aInteger0(X1)
& sdtasdt0(X0,X1) = xn ) )
| aDivisorOf0(X0,xn) )
& isPrime0(X0) ) )
& ( ? [X0] :
( aInteger0(X0)
& X0 != sz00
& ? [X1] :
( aInteger0(X1)
& sdtasdt0(X0,X1) = xn )
& aDivisorOf0(X0,xn)
& isPrime0(X0) )
=> ( ? [X0] :
( aElementOf0(X0,xS)
& aElementOf0(xn,X0) )
| aElementOf0(xn,sbsmnsldt0(xS)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f45,negated_conjecture,
~ ( ( ( ? [X0] :
( aElementOf0(X0,xS)
& aElementOf0(xn,X0) )
& aElementOf0(xn,sbsmnsldt0(xS)) )
=> ? [X0] :
( ( ( aInteger0(X0)
& X0 != sz00
& ? [X1] :
( aInteger0(X1)
& sdtasdt0(X0,X1) = xn ) )
| aDivisorOf0(X0,xn) )
& isPrime0(X0) ) )
& ( ? [X0] :
( aInteger0(X0)
& X0 != sz00
& ? [X1] :
( aInteger0(X1)
& sdtasdt0(X0,X1) = xn )
& aDivisorOf0(X0,xn)
& isPrime0(X0) )
=> ( ? [X0] :
( aElementOf0(X0,xS)
& aElementOf0(xn,X0) )
| aElementOf0(xn,sbsmnsldt0(xS)) ) ) ),
inference(negated_conjecture,[status(cth)],[f44]) ).
fof(f46,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(f47,plain,
~ ( ( ( ? [X0] :
( aElementOf0(X0,xS)
& aElementOf0(xn,X0) )
& aElementOf0(xn,sbsmnsldt0(xS)) )
=> ? [X1] :
( ( ( aInteger0(X1)
& sz00 != X1
& ? [X2] :
( aInteger0(X2)
& sdtasdt0(X1,X2) = xn ) )
| aDivisorOf0(X1,xn) )
& isPrime0(X1) ) )
& ( ? [X3] :
( aInteger0(X3)
& sz00 != X3
& ? [X4] :
( aInteger0(X4)
& xn = sdtasdt0(X3,X4) )
& aDivisorOf0(X3,xn)
& isPrime0(X3) )
=> ( ? [X5] :
( aElementOf0(X5,xS)
& aElementOf0(xn,X5) )
| aElementOf0(xn,sbsmnsldt0(xS)) ) ) ),
inference(rectify,[],[f45]) ).
fof(f55,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,[],[f46]) ).
fof(f56,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,[],[f55]) ).
fof(f57,plain,
( ( ! [X1] :
( ( ( ~ aInteger0(X1)
| sz00 = X1
| ! [X2] :
( ~ aInteger0(X2)
| sdtasdt0(X1,X2) != xn ) )
& ~ aDivisorOf0(X1,xn) )
| ~ isPrime0(X1) )
& ? [X0] :
( aElementOf0(X0,xS)
& aElementOf0(xn,X0) )
& aElementOf0(xn,sbsmnsldt0(xS)) )
| ( ! [X5] :
( ~ aElementOf0(X5,xS)
| ~ aElementOf0(xn,X5) )
& ~ aElementOf0(xn,sbsmnsldt0(xS))
& ? [X3] :
( aInteger0(X3)
& sz00 != X3
& ? [X4] :
( aInteger0(X4)
& xn = sdtasdt0(X3,X4) )
& aDivisorOf0(X3,xn)
& isPrime0(X3) ) ) ),
inference(ennf_transformation,[],[f47]) ).
fof(f58,plain,
( ( ! [X1] :
( ( ( ~ aInteger0(X1)
| sz00 = X1
| ! [X2] :
( ~ aInteger0(X2)
| sdtasdt0(X1,X2) != xn ) )
& ~ aDivisorOf0(X1,xn) )
| ~ isPrime0(X1) )
& ? [X0] :
( aElementOf0(X0,xS)
& aElementOf0(xn,X0) )
& aElementOf0(xn,sbsmnsldt0(xS)) )
| ( ! [X5] :
( ~ aElementOf0(X5,xS)
| ~ aElementOf0(xn,X5) )
& ~ aElementOf0(xn,sbsmnsldt0(xS))
& ? [X3] :
( aInteger0(X3)
& sz00 != X3
& ? [X4] :
( aInteger0(X4)
& xn = sdtasdt0(X3,X4) )
& aDivisorOf0(X3,xn)
& isPrime0(X3) ) ) ),
inference(flattening,[],[f57]) ).
fof(f59,plain,
! [X0] :
( ( ? [X1] :
( aDivisorOf0(X1,X0)
& isPrime0(X1) )
<=> ( X0 != sz10
& X0 != smndt0(sz10) ) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f60,plain,
! [X0,X1,X2] :
( ( sdteqdtlpzmzozddtrp0(X0,X1,X2)
<=> aDivisorOf0(X2,sdtpldt0(X0,smndt0(X1))) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| sz00 = X2 ),
inference(ennf_transformation,[],[f19]) ).
fof(f61,plain,
! [X0,X1,X2] :
( ( sdteqdtlpzmzozddtrp0(X0,X1,X2)
<=> aDivisorOf0(X2,sdtpldt0(X0,smndt0(X1))) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| sz00 = X2 ),
inference(flattening,[],[f60]) ).
fof(f62,plain,
! [X0] :
( ! [X1] :
( aDivisorOf0(X1,X0)
<=> ( aInteger0(X1)
& X1 != sz00
& ? [X2] :
( aInteger0(X2)
& sdtasdt0(X1,X2) = X0 ) ) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f63,plain,
! [X0] :
( ( sdtasdt0(smndt0(sz10),X0) = smndt0(X0)
& smndt0(X0) = sdtasdt0(X0,smndt0(sz10)) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f64,plain,
! [X0] :
( ( sdtpldt0(X0,smndt0(X0)) = sz00
& sz00 = sdtpldt0(smndt0(X0),X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f65,plain,
! [X0] :
( aInteger0(smndt0(X0))
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f66,plain,
! [X0,X1] :
( ! [X2] :
( X2 = szAzrzSzezqlpdtcmdtrp0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aInteger0(X3)
& sdteqdtlpzmzozddtrp0(X3,X0,X1) ) ) ) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 ),
inference(ennf_transformation,[],[f34]) ).
fof(f67,plain,
! [X0,X1] :
( ! [X2] :
( X2 = szAzrzSzezqlpdtcmdtrp0(X0,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aInteger0(X3)
& sdteqdtlpzmzozddtrp0(X3,X0,X1) ) ) ) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 ),
inference(flattening,[],[f66]) ).
fof(f68,plain,
! [X0,X1,X2,X3] :
( ( sdteqdtlpzmzozddtrp0(X0,X1,X2)
& sdteqdtlpzmzozddtrp0(X0,X1,X3) )
| ~ sdteqdtlpzmzozddtrp0(X0,X1,sdtasdt0(X2,X3))
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| sz00 = X2
| ~ aInteger0(X3)
| sz00 = X3 ),
inference(ennf_transformation,[],[f23]) ).
fof(f69,plain,
! [X0,X1,X2,X3] :
( ( sdteqdtlpzmzozddtrp0(X0,X1,X2)
& sdteqdtlpzmzozddtrp0(X0,X1,X3) )
| ~ sdteqdtlpzmzozddtrp0(X0,X1,sdtasdt0(X2,X3))
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| sz00 = X2
| ~ aInteger0(X3)
| sz00 = X3 ),
inference(flattening,[],[f68]) ).
fof(f72,plain,
! [X0,X1,X2] :
( sdteqdtlpzmzozddtrp0(X1,X0,X2)
| ~ sdteqdtlpzmzozddtrp0(X0,X1,X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| sz00 = X2 ),
inference(ennf_transformation,[],[f21]) ).
fof(f73,plain,
! [X0,X1,X2] :
( sdteqdtlpzmzozddtrp0(X1,X0,X2)
| ~ sdteqdtlpzmzozddtrp0(X0,X1,X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| sz00 = X2 ),
inference(flattening,[],[f72]) ).
fof(f78,plain,
! [X0] :
( ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f81,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(f82,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(flattening,[],[f81]) ).
fof(f85,plain,
! [X0,X1] :
( X0 = sz00
| X1 = sz00
| sz00 != sdtasdt0(X0,X1)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f86,plain,
! [X0,X1] :
( X0 = sz00
| X1 = sz00
| sz00 != sdtasdt0(X0,X1)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f85]) ).
fof(f87,plain,
! [X0] :
( ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f91,plain,
! [X0,X1,X2] :
( sdtasdt0(X0,sdtasdt0(X1,X2)) = sdtasdt0(sdtasdt0(X0,X1),X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(ennf_transformation,[],[f11]) ).
fof(f92,plain,
! [X0,X1,X2] :
( sdtasdt0(X0,sdtasdt0(X1,X2)) = sdtasdt0(sdtasdt0(X0,X1),X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(flattening,[],[f91]) ).
fof(f93,plain,
! [X0,X1] :
( aInteger0(sdtasdt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f6]) ).
fof(f94,plain,
! [X0,X1] :
( aInteger0(sdtasdt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f93]) ).
fof(f113,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) ) ) )
| ~ sP0(X5) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f114,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) ) ) )
| ~ sP1(X1) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f115,plain,
( aSet0(xS)
& ! [X0] :
( ( ? [X1] :
( aInteger0(X1)
& X1 != sz00
& isPrime0(X1)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X1))
& sP1(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))
& sP0(X5) ) ) ) )
& xS = cS2043 ),
inference(definition_folding,[],[f56,f114,f113]) ).
fof(f116,definition,
( ( ! [X5] :
( ~ aElementOf0(X5,xS)
| ~ aElementOf0(xn,X5) )
& ~ aElementOf0(xn,sbsmnsldt0(xS))
& ? [X3] :
( aInteger0(X3)
& sz00 != X3
& ? [X4] :
( aInteger0(X4)
& xn = sdtasdt0(X3,X4) )
& aDivisorOf0(X3,xn)
& isPrime0(X3) ) )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f117,plain,
( ( ! [X1] :
( ( ( ~ aInteger0(X1)
| sz00 = X1
| ! [X2] :
( ~ aInteger0(X2)
| sdtasdt0(X1,X2) != xn ) )
& ~ aDivisorOf0(X1,xn) )
| ~ isPrime0(X1) )
& ? [X0] :
( aElementOf0(X0,xS)
& aElementOf0(xn,X0) )
& aElementOf0(xn,sbsmnsldt0(xS)) )
| sP2 ),
inference(definition_folding,[],[f58,f116]) ).
fof(f133,plain,
( aSet0(xS)
& ! [X0] :
( ( ? [X1] :
( aInteger0(X1)
& X1 != sz00
& isPrime0(X1)
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X1))
& sP1(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))
& sP0(X2) ) ) ) )
& xS = cS2043 ),
inference(rectify,[],[f115]) ).
fof(f134,plain,
( aSet0(xS)
& ! [X0] :
( ( ( aInteger0(sK11(X0))
& sz00 != sK11(X0)
& isPrime0(sK11(X0))
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,sK11(X0)))
& sP1(sK11(X0))
& szAzrzSzezqlpdtcmdtrp0(sz00,sK11(X0)) = X0 )
| ~ aElementOf0(X0,xS) )
& ( aElementOf0(X0,xS)
| ! [X2] :
( ~ aInteger0(X2)
| sz00 = X2
| ~ isPrime0(X2)
| ( szAzrzSzezqlpdtcmdtrp0(sz00,X2) != X0
& aSet0(szAzrzSzezqlpdtcmdtrp0(sz00,X2))
& sP0(X2) ) ) ) )
& xS = cS2043 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X1,sK11(X0))],[f133]) ).
fof(f135,plain,
( ( ! [X5] :
( ~ aElementOf0(X5,xS)
| ~ aElementOf0(xn,X5) )
& ~ aElementOf0(xn,sbsmnsldt0(xS))
& ? [X3] :
( aInteger0(X3)
& sz00 != X3
& ? [X4] :
( aInteger0(X4)
& xn = sdtasdt0(X3,X4) )
& aDivisorOf0(X3,xn)
& isPrime0(X3) ) )
| ~ sP2 ),
inference(nnf_transformation,[],[f116]) ).
fof(f136,plain,
( ( ! [X0] :
( ~ aElementOf0(X0,xS)
| ~ aElementOf0(xn,X0) )
& ~ aElementOf0(xn,sbsmnsldt0(xS))
& ? [X1] :
( aInteger0(X1)
& sz00 != X1
& ? [X2] :
( aInteger0(X2)
& sdtasdt0(X1,X2) = xn )
& aDivisorOf0(X1,xn)
& isPrime0(X1) ) )
| ~ sP2 ),
inference(rectify,[],[f135]) ).
fof(f137,plain,
( ( ! [X0] :
( ~ aElementOf0(X0,xS)
| ~ aElementOf0(xn,X0) )
& ~ aElementOf0(xn,sbsmnsldt0(xS))
& aInteger0(sK12)
& sz00 != sK12
& aInteger0(sK13)
& xn = sdtasdt0(sK12,sK13)
& aDivisorOf0(sK12,xn)
& isPrime0(sK12) )
| ~ sP2 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13]),skolemize(X1,sK12),skolemize(X2,sK13)],[f136]) ).
fof(f138,plain,
( ( ! [X0] :
( ( ( ~ aInteger0(X0)
| sz00 = X0
| ! [X1] :
( ~ aInteger0(X1)
| sdtasdt0(X0,X1) != xn ) )
& ~ aDivisorOf0(X0,xn) )
| ~ isPrime0(X0) )
& ? [X2] :
( aElementOf0(X2,xS)
& aElementOf0(xn,X2) )
& aElementOf0(xn,sbsmnsldt0(xS)) )
| sP2 ),
inference(rectify,[],[f117]) ).
fof(f139,plain,
( ( ! [X0] :
( ( ( ~ aInteger0(X0)
| sz00 = X0
| ! [X1] :
( ~ aInteger0(X1)
| sdtasdt0(X0,X1) != xn ) )
& ~ aDivisorOf0(X0,xn) )
| ~ isPrime0(X0) )
& aElementOf0(sK14,xS)
& aElementOf0(xn,sK14)
& aElementOf0(xn,sbsmnsldt0(xS)) )
| sP2 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X2,sK14)],[f138]) ).
fof(f140,plain,
! [X0] :
( ( ( ? [X1] :
( aDivisorOf0(X1,X0)
& isPrime0(X1) )
| sz10 = X0
| smndt0(sz10) = X0 )
& ( ( X0 != sz10
& X0 != smndt0(sz10) )
| ! [X1] :
( ~ aDivisorOf0(X1,X0)
| ~ isPrime0(X1) ) ) )
| ~ aInteger0(X0) ),
inference(nnf_transformation,[],[f59]) ).
fof(f141,plain,
! [X0] :
( ( ( ? [X1] :
( aDivisorOf0(X1,X0)
& isPrime0(X1) )
| sz10 = X0
| smndt0(sz10) = X0 )
& ( ( X0 != sz10
& X0 != smndt0(sz10) )
| ! [X1] :
( ~ aDivisorOf0(X1,X0)
| ~ isPrime0(X1) ) ) )
| ~ aInteger0(X0) ),
inference(flattening,[],[f140]) ).
fof(f142,plain,
! [X0] :
( ( ( ? [X1] :
( aDivisorOf0(X1,X0)
& isPrime0(X1) )
| sz10 = X0
| smndt0(sz10) = X0 )
& ( ( X0 != sz10
& X0 != smndt0(sz10) )
| ! [X2] :
( ~ aDivisorOf0(X2,X0)
| ~ isPrime0(X2) ) ) )
| ~ aInteger0(X0) ),
inference(rectify,[],[f141]) ).
fof(f143,plain,
! [X0] :
( ( ( ( aDivisorOf0(sK15(X0),X0)
& isPrime0(sK15(X0)) )
| sz10 = X0
| smndt0(sz10) = X0 )
& ( ( X0 != sz10
& X0 != smndt0(sz10) )
| ! [X2] :
( ~ aDivisorOf0(X2,X0)
| ~ isPrime0(X2) ) ) )
| ~ aInteger0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X1,sK15(X0))],[f142]) ).
fof(f144,plain,
! [X0,X1,X2] :
( ( ( sdteqdtlpzmzozddtrp0(X0,X1,X2)
| ~ aDivisorOf0(X2,sdtpldt0(X0,smndt0(X1))) )
& ( aDivisorOf0(X2,sdtpldt0(X0,smndt0(X1)))
| ~ sdteqdtlpzmzozddtrp0(X0,X1,X2) ) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| sz00 = X2 ),
inference(nnf_transformation,[],[f61]) ).
fof(f145,plain,
! [X0] :
( ! [X1] :
( ( aDivisorOf0(X1,X0)
| ~ aInteger0(X1)
| sz00 = X1
| ! [X2] :
( ~ aInteger0(X2)
| sdtasdt0(X1,X2) != X0 ) )
& ( ( aInteger0(X1)
& X1 != sz00
& ? [X2] :
( aInteger0(X2)
& sdtasdt0(X1,X2) = X0 ) )
| ~ aDivisorOf0(X1,X0) ) )
| ~ aInteger0(X0) ),
inference(nnf_transformation,[],[f62]) ).
fof(f146,plain,
! [X0] :
( ! [X1] :
( ( aDivisorOf0(X1,X0)
| ~ aInteger0(X1)
| sz00 = X1
| ! [X2] :
( ~ aInteger0(X2)
| sdtasdt0(X1,X2) != X0 ) )
& ( ( aInteger0(X1)
& X1 != sz00
& ? [X2] :
( aInteger0(X2)
& sdtasdt0(X1,X2) = X0 ) )
| ~ aDivisorOf0(X1,X0) ) )
| ~ aInteger0(X0) ),
inference(flattening,[],[f145]) ).
fof(f147,plain,
! [X0] :
( ! [X1] :
( ( aDivisorOf0(X1,X0)
| ~ aInteger0(X1)
| sz00 = X1
| ! [X2] :
( ~ aInteger0(X2)
| sdtasdt0(X1,X2) != X0 ) )
& ( ( aInteger0(X1)
& X1 != sz00
& ? [X3] :
( aInteger0(X3)
& sdtasdt0(X1,X3) = X0 ) )
| ~ aDivisorOf0(X1,X0) ) )
| ~ aInteger0(X0) ),
inference(rectify,[],[f146]) ).
fof(f148,plain,
! [X0] :
( ! [X1] :
( ( aDivisorOf0(X1,X0)
| ~ aInteger0(X1)
| sz00 = X1
| ! [X2] :
( ~ aInteger0(X2)
| sdtasdt0(X1,X2) != X0 ) )
& ( ( aInteger0(X1)
& X1 != sz00
& aInteger0(sK16(X0,X1))
& sdtasdt0(X1,sK16(X0,X1)) = X0 )
| ~ aDivisorOf0(X1,X0) ) )
| ~ aInteger0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X3,sK16(X0,X1))],[f147]) ).
fof(f149,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = szAzrzSzezqlpdtcmdtrp0(X0,X1)
| ~ aSet0(X2)
| ? [X3] :
( ( ~ aInteger0(X3)
| ~ sdteqdtlpzmzozddtrp0(X3,X0,X1)
| ~ aElementOf0(X3,X2) )
& ( ( aInteger0(X3)
& sdteqdtlpzmzozddtrp0(X3,X0,X1) )
| aElementOf0(X3,X2) ) ) )
& ( ( aSet0(X2)
& ! [X3] :
( ( aElementOf0(X3,X2)
| ~ aInteger0(X3)
| ~ sdteqdtlpzmzozddtrp0(X3,X0,X1) )
& ( ( aInteger0(X3)
& sdteqdtlpzmzozddtrp0(X3,X0,X1) )
| ~ aElementOf0(X3,X2) ) ) )
| szAzrzSzezqlpdtcmdtrp0(X0,X1) != X2 ) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 ),
inference(nnf_transformation,[],[f67]) ).
fof(f150,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = szAzrzSzezqlpdtcmdtrp0(X0,X1)
| ~ aSet0(X2)
| ? [X3] :
( ( ~ aInteger0(X3)
| ~ sdteqdtlpzmzozddtrp0(X3,X0,X1)
| ~ aElementOf0(X3,X2) )
& ( ( aInteger0(X3)
& sdteqdtlpzmzozddtrp0(X3,X0,X1) )
| aElementOf0(X3,X2) ) ) )
& ( ( aSet0(X2)
& ! [X3] :
( ( aElementOf0(X3,X2)
| ~ aInteger0(X3)
| ~ sdteqdtlpzmzozddtrp0(X3,X0,X1) )
& ( ( aInteger0(X3)
& sdteqdtlpzmzozddtrp0(X3,X0,X1) )
| ~ aElementOf0(X3,X2) ) ) )
| szAzrzSzezqlpdtcmdtrp0(X0,X1) != X2 ) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 ),
inference(flattening,[],[f149]) ).
fof(f151,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = szAzrzSzezqlpdtcmdtrp0(X0,X1)
| ~ aSet0(X2)
| ? [X3] :
( ( ~ aInteger0(X3)
| ~ sdteqdtlpzmzozddtrp0(X3,X0,X1)
| ~ aElementOf0(X3,X2) )
& ( ( aInteger0(X3)
& sdteqdtlpzmzozddtrp0(X3,X0,X1) )
| aElementOf0(X3,X2) ) ) )
& ( ( aSet0(X2)
& ! [X4] :
( ( aElementOf0(X4,X2)
| ~ aInteger0(X4)
| ~ sdteqdtlpzmzozddtrp0(X4,X0,X1) )
& ( ( aInteger0(X4)
& sdteqdtlpzmzozddtrp0(X4,X0,X1) )
| ~ aElementOf0(X4,X2) ) ) )
| szAzrzSzezqlpdtcmdtrp0(X0,X1) != X2 ) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 ),
inference(rectify,[],[f150]) ).
fof(f152,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = szAzrzSzezqlpdtcmdtrp0(X0,X1)
| ~ aSet0(X2)
| ( ( ~ aInteger0(sK17(X0,X1,X2))
| ~ sdteqdtlpzmzozddtrp0(sK17(X0,X1,X2),X0,X1)
| ~ aElementOf0(sK17(X0,X1,X2),X2) )
& ( ( aInteger0(sK17(X0,X1,X2))
& sdteqdtlpzmzozddtrp0(sK17(X0,X1,X2),X0,X1) )
| aElementOf0(sK17(X0,X1,X2),X2) ) ) )
& ( ( aSet0(X2)
& ! [X4] :
( ( aElementOf0(X4,X2)
| ~ aInteger0(X4)
| ~ sdteqdtlpzmzozddtrp0(X4,X0,X1) )
& ( ( aInteger0(X4)
& sdteqdtlpzmzozddtrp0(X4,X0,X1) )
| ~ aElementOf0(X4,X2) ) ) )
| szAzrzSzezqlpdtcmdtrp0(X0,X1) != X2 ) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(X3,sK17(X0,X1,X2))],[f151]) ).
fof(f201,plain,
xS = cS2043,
inference(cnf_transformation,[],[f134]) ).
fof(f204,plain,
! [X2,X0] :
( aElementOf0(X0,xS)
| ~ aInteger0(X2)
| sz00 = X2
| ~ isPrime0(X2)
| szAzrzSzezqlpdtcmdtrp0(sz00,X2) != X0 ),
inference(cnf_transformation,[],[f134]) ).
fof(f205,plain,
! [X0] :
( szAzrzSzezqlpdtcmdtrp0(sz00,sK11(X0)) = X0
| ~ aElementOf0(X0,xS) ),
inference(cnf_transformation,[],[f134]) ).
fof(f208,plain,
! [X0] :
( isPrime0(sK11(X0))
| ~ aElementOf0(X0,xS) ),
inference(cnf_transformation,[],[f134]) ).
fof(f209,plain,
! [X0] :
( sz00 != sK11(X0)
| ~ aElementOf0(X0,xS) ),
inference(cnf_transformation,[],[f134]) ).
fof(f210,plain,
! [X0] :
( aInteger0(sK11(X0))
| ~ aElementOf0(X0,xS) ),
inference(cnf_transformation,[],[f134]) ).
fof(f212,plain,
aInteger0(xn),
inference(cnf_transformation,[],[f43]) ).
fof(f213,plain,
( isPrime0(sK12)
| ~ sP2 ),
inference(cnf_transformation,[],[f137]) ).
fof(f215,plain,
( xn = sdtasdt0(sK12,sK13)
| ~ sP2 ),
inference(cnf_transformation,[],[f137]) ).
fof(f216,plain,
( aInteger0(sK13)
| ~ sP2 ),
inference(cnf_transformation,[],[f137]) ).
fof(f217,plain,
( sz00 != sK12
| ~ sP2 ),
inference(cnf_transformation,[],[f137]) ).
fof(f218,plain,
( aInteger0(sK12)
| ~ sP2 ),
inference(cnf_transformation,[],[f137]) ).
fof(f220,plain,
! [X0] :
( ~ aElementOf0(X0,xS)
| ~ aElementOf0(xn,X0)
| ~ sP2 ),
inference(cnf_transformation,[],[f137]) ).
fof(f222,plain,
( aElementOf0(xn,sK14)
| sP2 ),
inference(cnf_transformation,[],[f139]) ).
fof(f223,plain,
( aElementOf0(sK14,xS)
| sP2 ),
inference(cnf_transformation,[],[f139]) ).
fof(f224,plain,
! [X0] :
( ~ aDivisorOf0(X0,xn)
| ~ isPrime0(X0)
| sP2 ),
inference(cnf_transformation,[],[f139]) ).
fof(f226,plain,
aInteger0(sz00),
inference(cnf_transformation,[],[f2]) ).
fof(f227,plain,
! [X2,X0] :
( smndt0(sz10) != X0
| ~ aDivisorOf0(X2,X0)
| ~ isPrime0(X2)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f228,plain,
! [X2,X0] :
( sz10 != X0
| ~ aDivisorOf0(X2,X0)
| ~ isPrime0(X2)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f229,plain,
! [X0] :
( smndt0(sz10) = X0
| sz10 = X0
| isPrime0(sK15(X0))
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f230,plain,
! [X0] :
( aDivisorOf0(sK15(X0),X0)
| sz10 = X0
| smndt0(sz10) = X0
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f231,plain,
! [X2,X0,X1] :
( aDivisorOf0(X2,sdtpldt0(X0,smndt0(X1)))
| ~ sdteqdtlpzmzozddtrp0(X0,X1,X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| sz00 = X2 ),
inference(cnf_transformation,[],[f144]) ).
fof(f232,plain,
! [X2,X0,X1] :
( ~ aDivisorOf0(X2,sdtpldt0(X0,smndt0(X1)))
| sdteqdtlpzmzozddtrp0(X0,X1,X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| sz00 = X2 ),
inference(cnf_transformation,[],[f144]) ).
fof(f236,plain,
! [X0,X1] :
( ~ aDivisorOf0(X1,X0)
| aInteger0(X1)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f148]) ).
fof(f237,plain,
! [X2,X0,X1] :
( aDivisorOf0(X1,X0)
| ~ aInteger0(X1)
| sz00 = X1
| ~ aInteger0(X2)
| sdtasdt0(X1,X2) != X0
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f148]) ).
fof(f238,plain,
! [X0] :
( smndt0(X0) = sdtasdt0(X0,smndt0(sz10))
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f63]) ).
fof(f240,plain,
! [X0] :
( sz00 = sdtpldt0(smndt0(X0),X0)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f64]) ).
fof(f241,plain,
! [X0] :
( sz00 = sdtpldt0(X0,smndt0(X0))
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f64]) ).
fof(f242,plain,
! [X0] :
( aInteger0(smndt0(X0))
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f65]) ).
fof(f243,plain,
! [X2,X0,X1,X4] :
( sdteqdtlpzmzozddtrp0(X4,X0,X1)
| ~ aElementOf0(X4,X2)
| szAzrzSzezqlpdtcmdtrp0(X0,X1) != X2
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 ),
inference(cnf_transformation,[],[f152]) ).
fof(f244,plain,
! [X2,X0,X1,X4] :
( aInteger0(X4)
| ~ aElementOf0(X4,X2)
| szAzrzSzezqlpdtcmdtrp0(X0,X1) != X2
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 ),
inference(cnf_transformation,[],[f152]) ).
fof(f245,plain,
! [X2,X0,X1,X4] :
( aElementOf0(X4,X2)
| ~ aInteger0(X4)
| ~ sdteqdtlpzmzozddtrp0(X4,X0,X1)
| szAzrzSzezqlpdtcmdtrp0(X0,X1) != X2
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 ),
inference(cnf_transformation,[],[f152]) ).
fof(f251,plain,
! [X2,X3,X0,X1] :
( ~ sdteqdtlpzmzozddtrp0(X0,X1,sdtasdt0(X2,X3))
| sdteqdtlpzmzozddtrp0(X0,X1,X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| sz00 = X2
| ~ aInteger0(X3)
| sz00 = X3 ),
inference(cnf_transformation,[],[f69]) ).
fof(f253,plain,
! [X2,X0,X1] :
( sdteqdtlpzmzozddtrp0(X1,X0,X2)
| ~ sdteqdtlpzmzozddtrp0(X0,X1,X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2)
| sz00 = X2 ),
inference(cnf_transformation,[],[f73]) ).
fof(f257,plain,
! [X0] :
( sdtpldt0(sz00,X0) = X0
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f258,plain,
! [X0] :
( sdtpldt0(X0,sz00) = X0
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f260,plain,
! [X2,X0,X1] :
( sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(cnf_transformation,[],[f82]) ).
fof(f262,plain,
! [X0,X1] :
( sz00 != sdtasdt0(X0,X1)
| sz00 = X1
| sz00 = X0
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(cnf_transformation,[],[f86]) ).
fof(f264,plain,
! [X0] :
( sz00 = sdtasdt0(X0,sz00)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f87]) ).
fof(f268,plain,
! [X2,X0,X1] :
( sdtasdt0(X0,sdtasdt0(X1,X2)) = sdtasdt0(sdtasdt0(X0,X1),X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(cnf_transformation,[],[f92]) ).
fof(f269,plain,
! [X0,X1] :
( aInteger0(sdtasdt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f327,plain,
aInteger0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f333,plain,
! [X0] :
( ~ aElementOf0(X0,cS2043)
| aInteger0(sK11(X0)) ),
inference(definition_unfolding,[],[f210,f201]) ).
fof(f334,plain,
! [X0] :
( sz00 != sK11(X0)
| ~ aElementOf0(X0,cS2043) ),
inference(definition_unfolding,[],[f209,f201]) ).
fof(f335,plain,
! [X0] :
( ~ aElementOf0(X0,cS2043)
| isPrime0(sK11(X0)) ),
inference(definition_unfolding,[],[f208,f201]) ).
fof(f338,plain,
! [X0] :
( szAzrzSzezqlpdtcmdtrp0(sz00,sK11(X0)) = X0
| ~ aElementOf0(X0,cS2043) ),
inference(definition_unfolding,[],[f205,f201]) ).
fof(f339,plain,
! [X2,X0] :
( aElementOf0(X0,cS2043)
| ~ aInteger0(X2)
| sz00 = X2
| ~ isPrime0(X2)
| szAzrzSzezqlpdtcmdtrp0(sz00,X2) != X0 ),
inference(definition_unfolding,[],[f204,f201]) ).
fof(f342,plain,
! [X0] :
( ~ aElementOf0(X0,cS2043)
| ~ aElementOf0(xn,X0)
| ~ sP2 ),
inference(definition_unfolding,[],[f220,f201]) ).
fof(f344,plain,
( aElementOf0(sK14,cS2043)
| sP2 ),
inference(definition_unfolding,[],[f223,f201]) ).
fof(f346,plain,
! [X2] :
( aElementOf0(szAzrzSzezqlpdtcmdtrp0(sz00,X2),cS2043)
| ~ aInteger0(X2)
| sz00 = X2
| ~ isPrime0(X2) ),
inference(equality_resolution,[],[f339]) ).
fof(f347,plain,
! [X2] :
( ~ aDivisorOf0(X2,sz10)
| ~ isPrime0(X2)
| ~ aInteger0(sz10) ),
inference(equality_resolution,[],[f228]) ).
fof(f348,plain,
! [X2] :
( ~ aDivisorOf0(X2,smndt0(sz10))
| ~ isPrime0(X2)
| ~ aInteger0(smndt0(sz10)) ),
inference(equality_resolution,[],[f227]) ).
fof(f349,plain,
! [X2,X1] :
( aDivisorOf0(X1,sdtasdt0(X1,X2))
| ~ aInteger0(X1)
| sz00 = X1
| ~ aInteger0(X2)
| ~ aInteger0(sdtasdt0(X1,X2)) ),
inference(equality_resolution,[],[f237]) ).
fof(f352,plain,
! [X0,X1,X4] :
( aElementOf0(X4,szAzrzSzezqlpdtcmdtrp0(X0,X1))
| ~ aInteger0(X4)
| ~ sdteqdtlpzmzozddtrp0(X4,X0,X1)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 ),
inference(equality_resolution,[],[f245]) ).
fof(f353,plain,
! [X0,X1,X4] :
( ~ aElementOf0(X4,szAzrzSzezqlpdtcmdtrp0(X0,X1))
| aInteger0(X4)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 ),
inference(equality_resolution,[],[f244]) ).
fof(f354,plain,
! [X0,X1,X4] :
( ~ aElementOf0(X4,szAzrzSzezqlpdtcmdtrp0(X0,X1))
| sdteqdtlpzmzozddtrp0(X4,X0,X1)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 ),
inference(equality_resolution,[],[f243]) ).
fof(f362,plain,
! [X2,X1] :
( aDivisorOf0(X1,sdtasdt0(X1,X2))
| ~ aInteger0(X1)
| sz00 = X1
| ~ aInteger0(X2) ),
inference(forward_subsumption_resolution,[],[f349,f269]) ).
fof(f364,definition,
( spl29_1
<=> aInteger0(smndt0(sz10)) ),
introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).
fof(f365,plain,
( aInteger0(smndt0(sz10))
| ~ spl29_1 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f366,plain,
( ~ aInteger0(smndt0(sz10))
| spl29_1 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f368,definition,
( spl29_2
<=> ! [X2] :
( ~ aDivisorOf0(X2,smndt0(sz10))
| ~ isPrime0(X2) ) ),
introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).
fof(f369,plain,
( ! [X2] :
( ~ aDivisorOf0(X2,smndt0(sz10))
| ~ isPrime0(X2) )
| ~ spl29_2 ),
inference(avatar_component_clause,[],[f368]) ).
fof(f370,plain,
( ~ spl29_1
| spl29_2 ),
inference(avatar_split_clause,[],[f348,f368,f364]) ).
fof(f371,plain,
! [X2] :
( ~ aDivisorOf0(X2,sz10)
| ~ isPrime0(X2) ),
inference(forward_subsumption_resolution,[],[f347,f327]) ).
fof(f373,definition,
( spl29_3
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl29_3])],[avatar_definition]) ).
fof(f382,definition,
( spl29_5
<=> aElementOf0(xn,sK14) ),
introduced(definition,[new_symbols(definition,[spl29_5])],[avatar_definition]) ).
fof(f384,plain,
( aElementOf0(xn,sK14)
| ~ spl29_5 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f385,plain,
( spl29_3
| spl29_5 ),
inference(avatar_split_clause,[],[f222,f382,f373]) ).
fof(f387,definition,
( spl29_6
<=> aElementOf0(sK14,cS2043) ),
introduced(definition,[new_symbols(definition,[spl29_6])],[avatar_definition]) ).
fof(f389,plain,
( aElementOf0(sK14,cS2043)
| ~ spl29_6 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f390,plain,
( spl29_3
| spl29_6 ),
inference(avatar_split_clause,[],[f344,f387,f373]) ).
fof(f392,definition,
( spl29_7
<=> ! [X0] :
( ~ aDivisorOf0(X0,xn)
| ~ isPrime0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl29_7])],[avatar_definition]) ).
fof(f393,plain,
( ! [X0] :
( ~ aDivisorOf0(X0,xn)
| ~ isPrime0(X0) )
| ~ spl29_7 ),
inference(avatar_component_clause,[],[f392]) ).
fof(f394,plain,
( spl29_3
| spl29_7 ),
inference(avatar_split_clause,[],[f224,f392,f373]) ).
fof(f400,definition,
( spl29_9
<=> isPrime0(sK12) ),
introduced(definition,[new_symbols(definition,[spl29_9])],[avatar_definition]) ).
fof(f402,plain,
( isPrime0(sK12)
| ~ spl29_9 ),
inference(avatar_component_clause,[],[f400]) ).
fof(f403,plain,
( ~ spl29_3
| spl29_9 ),
inference(avatar_split_clause,[],[f213,f400,f373]) ).
fof(f410,definition,
( spl29_11
<=> xn = sdtasdt0(sK12,sK13) ),
introduced(definition,[new_symbols(definition,[spl29_11])],[avatar_definition]) ).
fof(f412,plain,
( xn = sdtasdt0(sK12,sK13)
| ~ spl29_11 ),
inference(avatar_component_clause,[],[f410]) ).
fof(f413,plain,
( ~ spl29_3
| spl29_11 ),
inference(avatar_split_clause,[],[f215,f410,f373]) ).
fof(f415,definition,
( spl29_12
<=> aInteger0(sK13) ),
introduced(definition,[new_symbols(definition,[spl29_12])],[avatar_definition]) ).
fof(f417,plain,
( aInteger0(sK13)
| ~ spl29_12 ),
inference(avatar_component_clause,[],[f415]) ).
fof(f418,plain,
( ~ spl29_3
| spl29_12 ),
inference(avatar_split_clause,[],[f216,f415,f373]) ).
fof(f420,definition,
( spl29_13
<=> sz00 = sK12 ),
introduced(definition,[new_symbols(definition,[spl29_13])],[avatar_definition]) ).
fof(f422,plain,
( sz00 != sK12
| spl29_13 ),
inference(avatar_component_clause,[],[f420]) ).
fof(f423,plain,
( ~ spl29_3
| ~ spl29_13 ),
inference(avatar_split_clause,[],[f217,f420,f373]) ).
fof(f425,definition,
( spl29_14
<=> aInteger0(sK12) ),
introduced(definition,[new_symbols(definition,[spl29_14])],[avatar_definition]) ).
fof(f427,plain,
( aInteger0(sK12)
| ~ spl29_14 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f428,plain,
( ~ spl29_3
| spl29_14 ),
inference(avatar_split_clause,[],[f218,f425,f373]) ).
fof(f431,definition,
( spl29_15
<=> ! [X0] :
( ~ aElementOf0(X0,cS2043)
| ~ aElementOf0(xn,X0) ) ),
introduced(definition,[new_symbols(definition,[spl29_15])],[avatar_definition]) ).
fof(f432,plain,
( ! [X0] :
( ~ aElementOf0(xn,X0)
| ~ aElementOf0(X0,cS2043) )
| ~ spl29_15 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f433,plain,
( ~ spl29_3
| spl29_15 ),
inference(avatar_split_clause,[],[f342,f431,f373]) ).
fof(f474,plain,
! [X0] :
( aDivisorOf0(X0,sz00)
| ~ aInteger0(X0)
| sz00 = X0
| ~ aInteger0(sz00)
| ~ aInteger0(X0) ),
inference(superposition,[],[f362,f264]) ).
fof(f477,plain,
! [X0] :
( aDivisorOf0(X0,sz00)
| ~ aInteger0(X0)
| sz00 = X0
| ~ aInteger0(sz00) ),
inference(duplicate_literal_removal,[],[f474]) ).
fof(f484,plain,
! [X0] :
( aDivisorOf0(X0,sz00)
| ~ aInteger0(X0)
| sz00 = X0 ),
inference(forward_subsumption_resolution,[],[f477,f226]) ).
fof(f486,definition,
( spl29_19
<=> ! [X0] :
( ~ isPrime0(X0)
| sz00 = X0
| ~ aInteger0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl29_19])],[avatar_definition]) ).
fof(f487,plain,
( ! [X0] :
( sz00 = X0
| ~ isPrime0(X0)
| ~ aInteger0(X0) )
| ~ spl29_19 ),
inference(avatar_component_clause,[],[f486]) ).
fof(f489,definition,
( spl29_20
<=> sz00 = xn ),
introduced(definition,[new_symbols(definition,[spl29_20])],[avatar_definition]) ).
fof(f490,plain,
( sz00 = xn
| ~ spl29_20 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f491,plain,
( sz00 != xn
| spl29_20 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f560,definition,
( spl29_21
<=> sz00 = sz10 ),
introduced(definition,[new_symbols(definition,[spl29_21])],[avatar_definition]) ).
fof(f561,plain,
( sz00 != sz10
| spl29_21 ),
inference(avatar_component_clause,[],[f560]) ).
fof(f562,plain,
( sz00 = sz10
| ~ spl29_21 ),
inference(avatar_component_clause,[],[f560]) ).
fof(f621,plain,
( sz00 = smndt0(sz00)
| ~ aInteger0(smndt0(sz00))
| ~ aInteger0(sz00) ),
inference(superposition,[],[f258,f240]) ).
fof(f644,plain,
( ~ aInteger0(sz10)
| spl29_1 ),
inference(resolution,[],[f242,f366]) ).
fof(f646,plain,
( $false
| spl29_1 ),
inference(forward_subsumption_resolution,[],[f644,f327]) ).
fof(f647,plain,
spl29_1,
inference(avatar_contradiction_clause,[],[f646]) ).
fof(f651,plain,
( sz00 = smndt0(sz00)
| ~ aInteger0(sz00) ),
inference(forward_subsumption_resolution,[],[f621,f242]) ).
fof(f654,definition,
( spl29_23
<=> sz00 = smndt0(sz00) ),
introduced(definition,[new_symbols(definition,[spl29_23])],[avatar_definition]) ).
fof(f655,plain,
( sz00 = smndt0(sz00)
| ~ spl29_23 ),
inference(avatar_component_clause,[],[f654]) ).
fof(f662,plain,
sz00 = smndt0(sz00),
inference(forward_subsumption_resolution,[],[f651,f226]) ).
fof(f664,plain,
spl29_23,
inference(avatar_split_clause,[],[f662,f654]) ).
fof(f679,definition,
( spl29_27
<=> sz00 = smndt0(sz10) ),
introduced(definition,[new_symbols(definition,[spl29_27])],[avatar_definition]) ).
fof(f681,plain,
( sz00 = smndt0(sz10)
| ~ spl29_27 ),
inference(avatar_component_clause,[],[f679]) ).
fof(f702,plain,
! [X0,X1] :
( sdtpldt0(sz00,X1) = sdtpldt0(smndt0(X0),sdtpldt0(X0,X1))
| ~ aInteger0(smndt0(X0))
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X0) ),
inference(superposition,[],[f260,f240]) ).
fof(f713,plain,
! [X0,X1] :
( sdtpldt0(sz00,X1) = sdtpldt0(smndt0(X0),sdtpldt0(X0,X1))
| ~ aInteger0(smndt0(X0))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(duplicate_literal_removal,[],[f702]) ).
fof(f724,plain,
! [X0,X1] :
( sdtpldt0(sz00,X1) = sdtpldt0(smndt0(X0),sdtpldt0(X0,X1))
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(forward_subsumption_resolution,[],[f713,f242]) ).
fof(f804,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| sdteqdtlpzmzozddtrp0(X1,sz00,sK11(X0))
| ~ aInteger0(sz00)
| ~ aInteger0(sK11(X0))
| sz00 = sK11(X0)
| ~ aElementOf0(X0,cS2043) ),
inference(superposition,[],[f354,f338]) ).
fof(f805,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| sdteqdtlpzmzozddtrp0(X1,sz00,sK11(X0))
| ~ aInteger0(sz00)
| sz00 = sK11(X0)
| ~ aElementOf0(X0,cS2043) ),
inference(forward_subsumption_resolution,[],[f804,f333]) ).
fof(f806,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| sdteqdtlpzmzozddtrp0(X1,sz00,sK11(X0))
| ~ aInteger0(sz00)
| ~ aElementOf0(X0,cS2043) ),
inference(forward_subsumption_resolution,[],[f805,f334]) ).
fof(f807,plain,
! [X0,X1] :
( sdteqdtlpzmzozddtrp0(X1,sz00,sK11(X0))
| ~ aElementOf0(X1,X0)
| ~ aElementOf0(X0,cS2043) ),
inference(forward_subsumption_resolution,[],[f806,f226]) ).
fof(f906,plain,
! [X2,X0,X1] :
( aDivisorOf0(sdtasdt0(X0,X1),sdtasdt0(X0,sdtasdt0(X1,X2)))
| ~ aInteger0(sdtasdt0(X0,X1))
| sz00 = sdtasdt0(X0,X1)
| ~ aInteger0(X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(superposition,[],[f362,f268]) ).
fof(f913,plain,
! [X2,X0,X1] :
( aDivisorOf0(sdtasdt0(X0,X1),sdtasdt0(X0,sdtasdt0(X1,X2)))
| ~ aInteger0(sdtasdt0(X0,X1))
| sz00 = sdtasdt0(X0,X1)
| ~ aInteger0(X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(duplicate_literal_removal,[],[f906]) ).
fof(f934,plain,
! [X2,X0,X1] :
( aDivisorOf0(sdtasdt0(X0,X1),sdtasdt0(X0,sdtasdt0(X1,X2)))
| sz00 = sdtasdt0(X0,X1)
| ~ aInteger0(X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(forward_subsumption_resolution,[],[f913,f269]) ).
fof(f971,plain,
! [X0,X1] :
( aDivisorOf0(X1,smndt0(X0))
| ~ sdteqdtlpzmzozddtrp0(sz00,X0,X1)
| ~ aInteger0(sz00)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1
| ~ aInteger0(smndt0(X0)) ),
inference(superposition,[],[f231,f257]) ).
fof(f986,plain,
! [X0,X1] :
( aDivisorOf0(X1,smndt0(X0))
| ~ sdteqdtlpzmzozddtrp0(sz00,X0,X1)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1
| ~ aInteger0(smndt0(X0)) ),
inference(forward_subsumption_resolution,[],[f971,f226]) ).
fof(f988,plain,
! [X0,X1] :
( ~ sdteqdtlpzmzozddtrp0(sz00,X0,X1)
| aDivisorOf0(X1,smndt0(X0))
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 ),
inference(forward_subsumption_resolution,[],[f986,f242]) ).
fof(f998,plain,
! [X0] :
( sz00 != smndt0(X0)
| sz00 = smndt0(sz10)
| sz00 = X0
| ~ aInteger0(X0)
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(X0) ),
inference(superposition,[],[f262,f238]) ).
fof(f1008,plain,
! [X0,X1] :
( smndt0(sdtasdt0(X0,X1)) = sdtasdt0(X0,sdtasdt0(X1,smndt0(sz10)))
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(sdtasdt0(X0,X1)) ),
inference(superposition,[],[f268,f238]) ).
fof(f1017,plain,
! [X0] :
( sz00 != smndt0(X0)
| sz00 = smndt0(sz10)
| sz00 = X0
| ~ aInteger0(X0)
| ~ aInteger0(smndt0(sz10)) ),
inference(duplicate_literal_removal,[],[f998]) ).
fof(f1024,plain,
( ! [X0,X1] :
( smndt0(sdtasdt0(X0,X1)) = sdtasdt0(X0,sdtasdt0(X1,smndt0(sz10)))
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(sdtasdt0(X0,X1)) )
| ~ spl29_1 ),
inference(forward_subsumption_resolution,[],[f1008,f365]) ).
fof(f1029,plain,
( ! [X0] :
( sz00 != smndt0(X0)
| sz00 = smndt0(sz10)
| sz00 = X0
| ~ aInteger0(X0) )
| ~ spl29_1 ),
inference(forward_subsumption_resolution,[],[f1017,f365]) ).
fof(f1035,plain,
( ! [X0,X1] :
( smndt0(sdtasdt0(X0,X1)) = sdtasdt0(X0,sdtasdt0(X1,smndt0(sz10)))
| ~ aInteger0(X0)
| ~ aInteger0(X1) )
| ~ spl29_1 ),
inference(forward_subsumption_resolution,[],[f1024,f269]) ).
fof(f1041,definition,
( spl29_32
<=> ! [X0] :
( sz00 != smndt0(X0)
| ~ aInteger0(X0)
| sz00 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl29_32])],[avatar_definition]) ).
fof(f1042,plain,
( ! [X0] :
( sz00 != smndt0(X0)
| ~ aInteger0(X0)
| sz00 = X0 )
| ~ spl29_32 ),
inference(avatar_component_clause,[],[f1041]) ).
fof(f1043,plain,
( spl29_27
| spl29_32
| ~ spl29_1 ),
inference(avatar_split_clause,[],[f1029,f364,f1041,f679]) ).
fof(f1054,plain,
( sz00 = sdtpldt0(sz00,sz10)
| ~ aInteger0(sz10)
| ~ spl29_27 ),
inference(superposition,[],[f240,f681]) ).
fof(f1057,plain,
( sz00 = sdtpldt0(sz00,sz10)
| ~ spl29_27 ),
inference(forward_subsumption_resolution,[],[f1054,f327]) ).
fof(f1131,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| aInteger0(X1)
| ~ aInteger0(sz00)
| ~ aInteger0(sK11(X0))
| sz00 = sK11(X0)
| ~ aElementOf0(X0,cS2043) ),
inference(superposition,[],[f353,f338]) ).
fof(f1135,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| aInteger0(X1)
| ~ aInteger0(sz00)
| sz00 = sK11(X0)
| ~ aElementOf0(X0,cS2043) ),
inference(forward_subsumption_resolution,[],[f1131,f333]) ).
fof(f1143,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| aInteger0(X1)
| ~ aInteger0(sz00)
| ~ aElementOf0(X0,cS2043) ),
inference(forward_subsumption_resolution,[],[f1135,f334]) ).
fof(f1144,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| aInteger0(X1)
| ~ aElementOf0(X0,cS2043) ),
inference(forward_subsumption_resolution,[],[f1143,f226]) ).
fof(f1218,plain,
( sz10 = xn
| smndt0(sz10) = xn
| ~ aInteger0(xn)
| ~ isPrime0(sK15(xn))
| ~ spl29_7 ),
inference(resolution,[],[f230,f393]) ).
fof(f1221,plain,
( sz10 = xn
| smndt0(sz10) = xn
| ~ aInteger0(xn)
| ~ spl29_7 ),
inference(forward_subsumption_resolution,[],[f1218,f229]) ).
fof(f1224,plain,
( sz10 = xn
| smndt0(sz10) = xn
| ~ spl29_7 ),
inference(forward_subsumption_resolution,[],[f1221,f212]) ).
fof(f1475,plain,
( sz00 = sz10
| ~ aInteger0(sz10)
| ~ spl29_27 ),
inference(superposition,[],[f1057,f257]) ).
fof(f1483,plain,
( ~ aInteger0(sz10)
| spl29_21
| ~ spl29_27 ),
inference(forward_subsumption_resolution,[],[f1475,f561]) ).
fof(f1487,plain,
( $false
| spl29_21
| ~ spl29_27 ),
inference(forward_subsumption_resolution,[],[f1483,f327]) ).
fof(f1488,plain,
( spl29_21
| ~ spl29_27 ),
inference(avatar_contradiction_clause,[],[f1487]) ).
fof(f1666,plain,
! [X0,X1] :
( ~ sdteqdtlpzmzozddtrp0(X0,sz00,X1)
| ~ aInteger0(X0)
| ~ aInteger0(sz00)
| ~ aInteger0(X1)
| sz00 = X1
| aDivisorOf0(X1,smndt0(X0))
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 ),
inference(resolution,[],[f253,f988]) ).
fof(f1667,plain,
! [X0,X1] :
( ~ sdteqdtlpzmzozddtrp0(X0,sz00,X1)
| ~ aInteger0(X0)
| ~ aInteger0(sz00)
| ~ aInteger0(X1)
| sz00 = X1
| aDivisorOf0(X1,smndt0(X0)) ),
inference(duplicate_literal_removal,[],[f1666]) ).
fof(f1668,plain,
! [X0,X1] :
( ~ sdteqdtlpzmzozddtrp0(X0,sz00,X1)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1
| aDivisorOf0(X1,smndt0(X0)) ),
inference(forward_subsumption_resolution,[],[f1667,f226]) ).
fof(f1860,plain,
( ! [X0,X1] :
( sdtasdt0(X1,smndt0(X0)) = smndt0(sdtasdt0(X1,X0))
| ~ aInteger0(X1)
| ~ aInteger0(X0)
| ~ aInteger0(X0) )
| ~ spl29_1 ),
inference(superposition,[],[f1035,f238]) ).
fof(f1912,plain,
( ! [X0,X1] :
( sdtasdt0(X1,smndt0(X0)) = smndt0(sdtasdt0(X1,X0))
| ~ aInteger0(X1)
| ~ aInteger0(X0) )
| ~ spl29_1 ),
inference(duplicate_literal_removal,[],[f1860]) ).
fof(f2235,plain,
! [X0,X1] :
( ~ aDivisorOf0(X1,smndt0(X0))
| sdteqdtlpzmzozddtrp0(sz00,X0,X1)
| ~ aInteger0(sz00)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1
| ~ aInteger0(smndt0(X0)) ),
inference(superposition,[],[f232,f257]) ).
fof(f2236,plain,
! [X0,X1] :
( ~ aDivisorOf0(X0,sz00)
| sdteqdtlpzmzozddtrp0(smndt0(smndt0(X1)),X1,X0)
| ~ aInteger0(smndt0(smndt0(X1)))
| ~ aInteger0(X1)
| ~ aInteger0(X0)
| sz00 = X0
| ~ aInteger0(smndt0(X1)) ),
inference(superposition,[],[f232,f240]) ).
fof(f2252,plain,
! [X0,X1] :
( sdteqdtlpzmzozddtrp0(smndt0(smndt0(X1)),X1,X0)
| ~ aInteger0(smndt0(smndt0(X1)))
| ~ aInteger0(X1)
| ~ aInteger0(X0)
| sz00 = X0
| ~ aInteger0(smndt0(X1)) ),
inference(forward_subsumption_resolution,[],[f2236,f484]) ).
fof(f2253,plain,
! [X0,X1] :
( ~ aDivisorOf0(X1,smndt0(X0))
| sdteqdtlpzmzozddtrp0(sz00,X0,X1)
| ~ aInteger0(sz00)
| ~ aInteger0(X0)
| sz00 = X1
| ~ aInteger0(smndt0(X0)) ),
inference(forward_subsumption_resolution,[],[f2235,f236]) ).
fof(f2267,plain,
! [X0,X1] :
( sdteqdtlpzmzozddtrp0(smndt0(smndt0(X1)),X1,X0)
| ~ aInteger0(X1)
| ~ aInteger0(X0)
| sz00 = X0
| ~ aInteger0(smndt0(X1)) ),
inference(forward_subsumption_resolution,[],[f2252,f242]) ).
fof(f2268,plain,
! [X0,X1] :
( ~ aDivisorOf0(X1,smndt0(X0))
| sdteqdtlpzmzozddtrp0(sz00,X0,X1)
| ~ aInteger0(X0)
| sz00 = X1
| ~ aInteger0(smndt0(X0)) ),
inference(forward_subsumption_resolution,[],[f2253,f226]) ).
fof(f2276,plain,
! [X0,X1] :
( sdteqdtlpzmzozddtrp0(smndt0(smndt0(X1)),X1,X0)
| ~ aInteger0(X1)
| ~ aInteger0(X0)
| sz00 = X0 ),
inference(forward_subsumption_resolution,[],[f2267,f242]) ).
fof(f2277,plain,
! [X0,X1] :
( sdteqdtlpzmzozddtrp0(sz00,X0,X1)
| ~ aDivisorOf0(X1,smndt0(X0))
| ~ aInteger0(X0)
| sz00 = X1 ),
inference(forward_subsumption_resolution,[],[f2268,f242]) ).
fof(f2607,definition,
( spl29_47
<=> smndt0(sz10) = xn ),
introduced(definition,[new_symbols(definition,[spl29_47])],[avatar_definition]) ).
fof(f2608,plain,
( smndt0(sz10) != xn
| spl29_47 ),
inference(avatar_component_clause,[],[f2607]) ).
fof(f2609,plain,
( smndt0(sz10) = xn
| ~ spl29_47 ),
inference(avatar_component_clause,[],[f2607]) ).
fof(f2611,definition,
( spl29_48
<=> sz10 = xn ),
introduced(definition,[new_symbols(definition,[spl29_48])],[avatar_definition]) ).
fof(f2613,plain,
( sz10 = xn
| ~ spl29_48 ),
inference(avatar_component_clause,[],[f2611]) ).
fof(f2614,plain,
( spl29_47
| spl29_48
| ~ spl29_7 ),
inference(avatar_split_clause,[],[f1224,f392,f2611,f2607]) ).
fof(f2631,plain,
( sz00 = sdtpldt0(xn,sz10)
| ~ aInteger0(sz10)
| ~ spl29_47 ),
inference(superposition,[],[f240,f2609]) ).
fof(f2645,plain,
( sz00 = sdtpldt0(xn,sz10)
| ~ spl29_47 ),
inference(forward_subsumption_resolution,[],[f2631,f327]) ).
fof(f2666,plain,
( sdtpldt0(sz00,sz10) = sdtpldt0(smndt0(xn),sz00)
| ~ aInteger0(xn)
| ~ aInteger0(sz10)
| ~ spl29_47 ),
inference(superposition,[],[f724,f2645]) ).
fof(f2667,plain,
( sdtpldt0(sz00,sz10) = sdtpldt0(smndt0(xn),sz00)
| ~ aInteger0(sz10)
| ~ spl29_47 ),
inference(forward_subsumption_resolution,[],[f2666,f212]) ).
fof(f2668,plain,
( sdtpldt0(sz00,sz10) = sdtpldt0(smndt0(xn),sz00)
| ~ spl29_47 ),
inference(forward_subsumption_resolution,[],[f2667,f327]) ).
fof(f2737,plain,
( sdtpldt0(sz00,sz10) = smndt0(xn)
| ~ aInteger0(smndt0(xn))
| ~ spl29_47 ),
inference(superposition,[],[f2668,f258]) ).
fof(f2743,plain,
( sdtpldt0(sz00,sz10) = smndt0(xn)
| ~ aInteger0(smndt0(xn))
| ~ spl29_47 ),
inference(superposition,[],[f258,f2668]) ).
fof(f2755,definition,
( spl29_49
<=> aInteger0(smndt0(xn)) ),
introduced(definition,[new_symbols(definition,[spl29_49])],[avatar_definition]) ).
fof(f2757,plain,
( ~ aInteger0(smndt0(xn))
| spl29_49 ),
inference(avatar_component_clause,[],[f2755]) ).
fof(f2759,definition,
( spl29_50
<=> sdtpldt0(sz00,sz10) = smndt0(xn) ),
introduced(definition,[new_symbols(definition,[spl29_50])],[avatar_definition]) ).
fof(f2761,plain,
( sdtpldt0(sz00,sz10) = smndt0(xn)
| ~ spl29_50 ),
inference(avatar_component_clause,[],[f2759]) ).
fof(f2762,plain,
( ~ spl29_49
| spl29_50
| ~ spl29_47 ),
inference(avatar_split_clause,[],[f2743,f2607,f2759,f2755]) ).
fof(f2772,plain,
( ~ spl29_49
| spl29_50
| ~ spl29_47 ),
inference(avatar_split_clause,[],[f2737,f2607,f2759,f2755]) ).
fof(f2794,plain,
( ~ aInteger0(xn)
| spl29_49 ),
inference(resolution,[],[f2757,f242]) ).
fof(f2795,plain,
( $false
| spl29_49 ),
inference(forward_subsumption_resolution,[],[f2794,f212]) ).
fof(f2796,plain,
spl29_49,
inference(avatar_contradiction_clause,[],[f2795]) ).
fof(f2801,plain,
( aElementOf0(sz10,sK14)
| ~ spl29_5
| ~ spl29_48 ),
inference(superposition,[],[f384,f2613]) ).
fof(f3828,plain,
( sz10 = smndt0(xn)
| ~ aInteger0(sz10)
| ~ spl29_50 ),
inference(superposition,[],[f257,f2761]) ).
fof(f3835,plain,
( sz10 = smndt0(xn)
| ~ spl29_50 ),
inference(forward_subsumption_resolution,[],[f3828,f327]) ).
fof(f3971,plain,
( sz00 != smndt0(sz10)
| ~ spl29_20
| spl29_47 ),
inference(forward_demodulation,[],[f2608,f490]) ).
fof(f4061,plain,
( ~ aElementOf0(sK14,cS2043)
| ~ spl29_5
| ~ spl29_15 ),
inference(resolution,[],[f432,f384]) ).
fof(f4065,plain,
( $false
| ~ spl29_5
| ~ spl29_6
| ~ spl29_15 ),
inference(forward_subsumption_resolution,[],[f4061,f389]) ).
fof(f4066,plain,
( ~ spl29_5
| ~ spl29_6
| ~ spl29_15 ),
inference(avatar_contradiction_clause,[],[f4065]) ).
fof(f4080,plain,
( smndt0(xn) = sdtasdt0(sK12,smndt0(sK13))
| ~ aInteger0(sK12)
| ~ aInteger0(sK13)
| ~ spl29_1
| ~ spl29_11 ),
inference(superposition,[],[f1912,f412]) ).
fof(f4085,plain,
( smndt0(xn) = sdtasdt0(sK12,smndt0(sK13))
| ~ aInteger0(sK13)
| ~ spl29_1
| ~ spl29_11
| ~ spl29_14 ),
inference(forward_subsumption_resolution,[],[f4080,f427]) ).
fof(f4095,plain,
( smndt0(xn) = sdtasdt0(sK12,smndt0(sK13))
| ~ spl29_1
| ~ spl29_11
| ~ spl29_12
| ~ spl29_14 ),
inference(forward_subsumption_resolution,[],[f4085,f417]) ).
fof(f4105,plain,
( sz10 = sdtasdt0(sK12,smndt0(sK13))
| ~ spl29_1
| ~ spl29_11
| ~ spl29_12
| ~ spl29_14
| ~ spl29_50 ),
inference(forward_demodulation,[],[f4095,f3835]) ).
fof(f4107,definition,
( spl29_64
<=> sz00 = sK13 ),
introduced(definition,[new_symbols(definition,[spl29_64])],[avatar_definition]) ).
fof(f4108,plain,
( sz00 != sK13
| spl29_64 ),
inference(avatar_component_clause,[],[f4107]) ).
fof(f4109,plain,
( sz00 = sK13
| ~ spl29_64 ),
inference(avatar_component_clause,[],[f4107]) ).
fof(f4132,plain,
( xn = sdtasdt0(sK12,sz00)
| ~ spl29_11
| ~ spl29_64 ),
inference(superposition,[],[f412,f4109]) ).
fof(f4142,plain,
( sz00 = xn
| ~ aInteger0(sK12)
| ~ spl29_11
| ~ spl29_64 ),
inference(superposition,[],[f4132,f264]) ).
fof(f4169,plain,
( ~ aInteger0(sK12)
| ~ spl29_11
| spl29_20
| ~ spl29_64 ),
inference(forward_subsumption_resolution,[],[f4142,f491]) ).
fof(f4182,plain,
( $false
| ~ spl29_11
| ~ spl29_14
| spl29_20
| ~ spl29_64 ),
inference(forward_subsumption_resolution,[],[f4169,f427]) ).
fof(f4183,plain,
( ~ spl29_11
| ~ spl29_14
| spl29_20
| ~ spl29_64 ),
inference(avatar_contradiction_clause,[],[f4182]) ).
fof(f4259,definition,
( spl29_69
<=> sz00 = smndt0(sK12) ),
introduced(definition,[new_symbols(definition,[spl29_69])],[avatar_definition]) ).
fof(f4260,plain,
( sz00 != smndt0(sK12)
| spl29_69 ),
inference(avatar_component_clause,[],[f4259]) ).
fof(f4261,plain,
( sz00 = smndt0(sK12)
| ~ spl29_69 ),
inference(avatar_component_clause,[],[f4259]) ).
fof(f4422,definition,
( spl29_80
<=> aDivisorOf0(sK12,sz10) ),
introduced(definition,[new_symbols(definition,[spl29_80])],[avatar_definition]) ).
fof(f4424,plain,
( aDivisorOf0(sK12,sz10)
| ~ spl29_80 ),
inference(avatar_component_clause,[],[f4422]) ).
fof(f4722,plain,
( aDivisorOf0(sK12,sz10)
| ~ aInteger0(sK12)
| sz00 = sK12
| ~ aInteger0(smndt0(sK13))
| ~ spl29_1
| ~ spl29_11
| ~ spl29_12
| ~ spl29_14
| ~ spl29_50 ),
inference(superposition,[],[f362,f4105]) ).
fof(f4730,plain,
( aDivisorOf0(sK12,sz10)
| sz00 = sK12
| ~ aInteger0(smndt0(sK13))
| ~ spl29_1
| ~ spl29_11
| ~ spl29_12
| ~ spl29_14
| ~ spl29_50 ),
inference(forward_subsumption_resolution,[],[f4722,f427]) ).
fof(f4737,definition,
( spl29_96
<=> aInteger0(smndt0(sK13)) ),
introduced(definition,[new_symbols(definition,[spl29_96])],[avatar_definition]) ).
fof(f4739,plain,
( ~ aInteger0(smndt0(sK13))
| spl29_96 ),
inference(avatar_component_clause,[],[f4737]) ).
fof(f4758,plain,
( aDivisorOf0(sK12,sz10)
| ~ aInteger0(smndt0(sK13))
| ~ spl29_1
| ~ spl29_11
| ~ spl29_12
| spl29_13
| ~ spl29_14
| ~ spl29_50 ),
inference(forward_subsumption_resolution,[],[f4730,f422]) ).
fof(f4779,plain,
( ~ spl29_96
| spl29_80
| ~ spl29_1
| ~ spl29_11
| ~ spl29_12
| spl29_13
| ~ spl29_14
| ~ spl29_50 ),
inference(avatar_split_clause,[],[f4758,f2759,f425,f420,f415,f410,f364,f4422,f4737]) ).
fof(f4780,plain,
( ~ aInteger0(sK13)
| spl29_96 ),
inference(resolution,[],[f4739,f242]) ).
fof(f4781,plain,
( $false
| ~ spl29_12
| spl29_96 ),
inference(forward_subsumption_resolution,[],[f4780,f417]) ).
fof(f4782,plain,
( ~ spl29_12
| spl29_96 ),
inference(avatar_contradiction_clause,[],[f4781]) ).
fof(f4783,plain,
( ~ isPrime0(sK12)
| ~ spl29_80 ),
inference(resolution,[],[f4424,f371]) ).
fof(f4785,plain,
( $false
| ~ spl29_9
| ~ spl29_80 ),
inference(forward_subsumption_resolution,[],[f4783,f402]) ).
fof(f4786,plain,
( ~ spl29_9
| ~ spl29_80 ),
inference(avatar_contradiction_clause,[],[f4785]) ).
fof(f7108,plain,
! [X0,X1] :
( ~ aInteger0(X0)
| ~ aInteger0(sK11(X1))
| sz00 = sK11(X1)
| aDivisorOf0(sK11(X1),smndt0(X0))
| ~ aElementOf0(X0,X1)
| ~ aElementOf0(X1,cS2043) ),
inference(resolution,[],[f1668,f807]) ).
fof(f7117,plain,
! [X0,X1] :
( ~ aInteger0(sK11(X1))
| sz00 = sK11(X1)
| aDivisorOf0(sK11(X1),smndt0(X0))
| ~ aElementOf0(X0,X1)
| ~ aElementOf0(X1,cS2043) ),
inference(forward_subsumption_resolution,[],[f7108,f1144]) ).
fof(f7119,plain,
! [X0,X1] :
( sz00 = sK11(X1)
| aDivisorOf0(sK11(X1),smndt0(X0))
| ~ aElementOf0(X0,X1)
| ~ aElementOf0(X1,cS2043) ),
inference(forward_subsumption_resolution,[],[f7117,f333]) ).
fof(f7120,plain,
! [X0,X1] :
( aDivisorOf0(sK11(X1),smndt0(X0))
| ~ aElementOf0(X0,X1)
| ~ aElementOf0(X1,cS2043) ),
inference(forward_subsumption_resolution,[],[f7119,f334]) ).
fof(f7121,plain,
( ! [X0] :
( ~ aElementOf0(sz10,X0)
| ~ aElementOf0(X0,cS2043)
| ~ isPrime0(sK11(X0)) )
| ~ spl29_2 ),
inference(resolution,[],[f7120,f369]) ).
fof(f7130,plain,
( ! [X0] :
( aDivisorOf0(sK11(X0),sz10)
| ~ aElementOf0(xn,X0)
| ~ aElementOf0(X0,cS2043) )
| ~ spl29_50 ),
inference(superposition,[],[f7120,f3835]) ).
fof(f7133,plain,
( ! [X0] :
( ~ aElementOf0(sz10,X0)
| ~ aElementOf0(X0,cS2043) )
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f7121,f335]) ).
fof(f7226,plain,
! [X2,X0,X1] :
( sdteqdtlpzmzozddtrp0(sz00,X0,X1)
| ~ aInteger0(sz00)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1
| ~ aInteger0(X2)
| sz00 = X2
| ~ aDivisorOf0(sdtasdt0(X1,X2),smndt0(X0))
| ~ aInteger0(X0)
| sz00 = sdtasdt0(X1,X2) ),
inference(resolution,[],[f251,f2277]) ).
fof(f7260,plain,
! [X2,X0,X1] :
( sdteqdtlpzmzozddtrp0(sz00,X0,X1)
| ~ aInteger0(sz00)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1
| ~ aInteger0(X2)
| sz00 = X2
| ~ aDivisorOf0(sdtasdt0(X1,X2),smndt0(X0))
| sz00 = sdtasdt0(X1,X2) ),
inference(duplicate_literal_removal,[],[f7226]) ).
fof(f7270,plain,
! [X2,X0,X1] :
( sdteqdtlpzmzozddtrp0(sz00,X0,X1)
| ~ aInteger0(sz00)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1
| ~ aInteger0(X2)
| sz00 = X2
| ~ aDivisorOf0(sdtasdt0(X1,X2),smndt0(X0)) ),
inference(forward_subsumption_resolution,[],[f7260,f262]) ).
fof(f7275,plain,
! [X2,X0,X1] :
( ~ aDivisorOf0(sdtasdt0(X1,X2),smndt0(X0))
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1
| ~ aInteger0(X2)
| sz00 = X2
| sdteqdtlpzmzozddtrp0(sz00,X0,X1) ),
inference(forward_subsumption_resolution,[],[f7270,f226]) ).
fof(f8310,plain,
( ! [X0] :
( aDivisorOf0(xn,sdtasdt0(sK12,sdtasdt0(sK13,X0)))
| sz00 = xn
| ~ aInteger0(X0)
| ~ aInteger0(sK12)
| ~ aInteger0(sK13) )
| ~ spl29_11 ),
inference(superposition,[],[f934,f412]) ).
fof(f9900,plain,
( ! [X0] :
( ~ aDivisorOf0(xn,smndt0(X0))
| ~ aInteger0(X0)
| ~ aInteger0(sK12)
| sz00 = sK12
| ~ aInteger0(sK13)
| sz00 = sK13
| sdteqdtlpzmzozddtrp0(sz00,X0,sK12) )
| ~ spl29_11 ),
inference(superposition,[],[f7275,f412]) ).
fof(f12614,plain,
( ! [X0] :
( sdteqdtlpzmzozddtrp0(smndt0(sz00),sz00,X0)
| ~ aInteger0(sz00)
| ~ aInteger0(X0)
| sz00 = X0 )
| ~ spl29_23 ),
inference(superposition,[],[f2276,f655]) ).
fof(f12633,plain,
( ! [X0] :
( sdteqdtlpzmzozddtrp0(smndt0(sz00),sz00,X0)
| ~ aInteger0(X0)
| sz00 = X0 )
| ~ spl29_23 ),
inference(forward_subsumption_resolution,[],[f12614,f226]) ).
fof(f12641,plain,
( ! [X0] :
( sdteqdtlpzmzozddtrp0(sz00,sz00,X0)
| ~ aInteger0(X0)
| sz00 = X0 )
| ~ spl29_23 ),
inference(forward_demodulation,[],[f12633,f655]) ).
fof(f17050,plain,
( ! [X0] :
( ~ aElementOf0(xn,X0)
| ~ aElementOf0(X0,cS2043)
| ~ isPrime0(sK11(X0)) )
| ~ spl29_50 ),
inference(resolution,[],[f7130,f371]) ).
fof(f17055,plain,
( ! [X0] :
( ~ aElementOf0(xn,X0)
| ~ aElementOf0(X0,cS2043) )
| ~ spl29_50 ),
inference(forward_subsumption_resolution,[],[f17050,f335]) ).
fof(f17056,plain,
( spl29_15
| ~ spl29_50 ),
inference(avatar_split_clause,[],[f17055,f2759,f431]) ).
fof(f17243,plain,
( ~ aElementOf0(sK14,cS2043)
| ~ spl29_2
| ~ spl29_5
| ~ spl29_48 ),
inference(resolution,[],[f2801,f7133]) ).
fof(f17245,plain,
( $false
| ~ spl29_2
| ~ spl29_5
| ~ spl29_6
| ~ spl29_48 ),
inference(forward_subsumption_resolution,[],[f17243,f389]) ).
fof(f17246,plain,
( ~ spl29_2
| ~ spl29_5
| ~ spl29_6
| ~ spl29_48 ),
inference(avatar_contradiction_clause,[],[f17245]) ).
fof(f17268,plain,
( smndt0(xn) = sdtasdt0(sK12,smndt0(sK13))
| ~ spl29_1
| ~ spl29_11
| ~ spl29_12
| ~ spl29_14 ),
inference(forward_subsumption_resolution,[],[f4085,f417]) ).
fof(f17285,plain,
( ! [X0] :
( aDivisorOf0(xn,sdtasdt0(sK12,sdtasdt0(sK13,X0)))
| ~ aInteger0(X0)
| ~ aInteger0(sK12)
| ~ aInteger0(sK13) )
| ~ spl29_11
| spl29_20 ),
inference(forward_subsumption_resolution,[],[f8310,f491]) ).
fof(f17300,plain,
( ! [X0] :
( ~ aDivisorOf0(xn,smndt0(X0))
| ~ aInteger0(X0)
| sz00 = sK12
| ~ aInteger0(sK13)
| sz00 = sK13
| sdteqdtlpzmzozddtrp0(sz00,X0,sK12) )
| ~ spl29_11
| ~ spl29_14 ),
inference(forward_subsumption_resolution,[],[f9900,f427]) ).
fof(f17320,plain,
( ! [X0] :
( aDivisorOf0(xn,sdtasdt0(sK12,sdtasdt0(sK13,X0)))
| ~ aInteger0(X0)
| ~ aInteger0(sK13) )
| ~ spl29_11
| ~ spl29_14
| spl29_20 ),
inference(forward_subsumption_resolution,[],[f17285,f427]) ).
fof(f17344,plain,
( ! [X0] :
( ~ aDivisorOf0(xn,smndt0(X0))
| ~ aInteger0(X0)
| ~ aInteger0(sK13)
| sz00 = sK13
| sdteqdtlpzmzozddtrp0(sz00,X0,sK12) )
| ~ spl29_11
| spl29_13
| ~ spl29_14 ),
inference(forward_subsumption_resolution,[],[f17300,f422]) ).
fof(f17353,plain,
( ! [X0] :
( aDivisorOf0(xn,sdtasdt0(sK12,sdtasdt0(sK13,X0)))
| ~ aInteger0(X0) )
| ~ spl29_11
| ~ spl29_12
| ~ spl29_14
| spl29_20 ),
inference(forward_subsumption_resolution,[],[f17320,f417]) ).
fof(f17358,plain,
( ! [X0] :
( ~ aDivisorOf0(xn,smndt0(X0))
| ~ aInteger0(X0)
| sz00 = sK13
| sdteqdtlpzmzozddtrp0(sz00,X0,sK12) )
| ~ spl29_11
| ~ spl29_12
| spl29_13
| ~ spl29_14 ),
inference(forward_subsumption_resolution,[],[f17344,f417]) ).
fof(f17363,plain,
( ! [X0] :
( sdteqdtlpzmzozddtrp0(sz00,X0,sK12)
| ~ aInteger0(X0)
| ~ aDivisorOf0(xn,smndt0(X0)) )
| ~ spl29_11
| ~ spl29_12
| spl29_13
| ~ spl29_14
| spl29_64 ),
inference(forward_subsumption_resolution,[],[f17358,f4108]) ).
fof(f17371,plain,
( ! [X0,X1] :
( ~ aElementOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),cS2043)
| ~ aInteger0(xn)
| ~ sdteqdtlpzmzozddtrp0(xn,X0,X1)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 )
| ~ spl29_15 ),
inference(resolution,[],[f432,f352]) ).
fof(f17372,plain,
( ! [X0,X1] :
( ~ aElementOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),cS2043)
| ~ sdteqdtlpzmzozddtrp0(xn,X0,X1)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sz00 = X1 )
| ~ spl29_15 ),
inference(forward_subsumption_resolution,[],[f17371,f212]) ).
fof(f17515,definition,
( spl29_226
<=> aDivisorOf0(xn,smndt0(xn)) ),
introduced(definition,[new_symbols(definition,[spl29_226])],[avatar_definition]) ).
fof(f17517,plain,
( aDivisorOf0(xn,smndt0(xn))
| ~ spl29_226 ),
inference(avatar_component_clause,[],[f17515]) ).
fof(f17910,plain,
( aDivisorOf0(xn,sdtasdt0(sK12,smndt0(sK13)))
| ~ aInteger0(smndt0(sz10))
| ~ aInteger0(sK13)
| ~ spl29_11
| ~ spl29_12
| ~ spl29_14
| spl29_20 ),
inference(superposition,[],[f17353,f238]) ).
fof(f17938,plain,
( aDivisorOf0(xn,sdtasdt0(sK12,smndt0(sK13)))
| ~ aInteger0(sK13)
| ~ spl29_1
| ~ spl29_11
| ~ spl29_12
| ~ spl29_14
| spl29_20 ),
inference(forward_subsumption_resolution,[],[f17910,f365]) ).
fof(f17947,plain,
( aDivisorOf0(xn,sdtasdt0(sK12,smndt0(sK13)))
| ~ spl29_1
| ~ spl29_11
| ~ spl29_12
| ~ spl29_14
| spl29_20 ),
inference(forward_subsumption_resolution,[],[f17938,f417]) ).
fof(f17961,plain,
( aDivisorOf0(xn,smndt0(xn))
| ~ spl29_1
| ~ spl29_11
| ~ spl29_12
| ~ spl29_14
| spl29_20 ),
inference(forward_demodulation,[],[f17947,f17268]) ).
fof(f17966,plain,
( spl29_226
| ~ spl29_1
| ~ spl29_11
| ~ spl29_12
| ~ spl29_14
| spl29_20 ),
inference(avatar_split_clause,[],[f17961,f489,f425,f415,f410,f364,f17515]) ).
fof(f18501,plain,
( ! [X0] :
( ~ sdteqdtlpzmzozddtrp0(xn,sz00,X0)
| ~ aInteger0(sz00)
| ~ aInteger0(X0)
| sz00 = X0
| ~ aInteger0(X0)
| sz00 = X0
| ~ isPrime0(X0) )
| ~ spl29_15 ),
inference(resolution,[],[f17372,f346]) ).
fof(f18506,plain,
( ! [X0] :
( ~ sdteqdtlpzmzozddtrp0(xn,sz00,X0)
| ~ aInteger0(sz00)
| ~ aInteger0(X0)
| sz00 = X0
| ~ isPrime0(X0) )
| ~ spl29_15 ),
inference(duplicate_literal_removal,[],[f18501]) ).
fof(f18509,plain,
( ! [X0] :
( ~ sdteqdtlpzmzozddtrp0(xn,sz00,X0)
| ~ aInteger0(X0)
| sz00 = X0
| ~ isPrime0(X0) )
| ~ spl29_15 ),
inference(forward_subsumption_resolution,[],[f18506,f226]) ).
fof(f18882,plain,
( ! [X0] :
( ~ aInteger0(X0)
| sz00 = X0
| ~ isPrime0(X0)
| ~ sdteqdtlpzmzozddtrp0(sz00,xn,X0)
| ~ aInteger0(sz00)
| ~ aInteger0(xn)
| ~ aInteger0(X0)
| sz00 = X0 )
| ~ spl29_15 ),
inference(resolution,[],[f18509,f253]) ).
fof(f18887,plain,
( ! [X0] :
( ~ aInteger0(X0)
| sz00 = X0
| ~ isPrime0(X0)
| ~ sdteqdtlpzmzozddtrp0(sz00,xn,X0)
| ~ aInteger0(sz00)
| ~ aInteger0(xn) )
| ~ spl29_15 ),
inference(duplicate_literal_removal,[],[f18882]) ).
fof(f18890,plain,
( ! [X0] :
( ~ aInteger0(X0)
| sz00 = X0
| ~ isPrime0(X0)
| ~ sdteqdtlpzmzozddtrp0(sz00,xn,X0)
| ~ aInteger0(xn) )
| ~ spl29_15 ),
inference(forward_subsumption_resolution,[],[f18887,f226]) ).
fof(f18893,plain,
( ! [X0] :
( ~ sdteqdtlpzmzozddtrp0(sz00,xn,X0)
| sz00 = X0
| ~ isPrime0(X0)
| ~ aInteger0(X0) )
| ~ spl29_15 ),
inference(forward_subsumption_resolution,[],[f18890,f212]) ).
fof(f19069,plain,
( sz00 != sz00
| ~ aInteger0(sK12)
| sz00 = sK12
| ~ spl29_32
| ~ spl29_69 ),
inference(superposition,[],[f1042,f4261]) ).
fof(f19094,plain,
( ~ aInteger0(sK12)
| sz00 = sK12
| ~ spl29_32
| ~ spl29_69 ),
inference(trivial_inequality_removal,[],[f19069]) ).
fof(f19112,plain,
( sz00 = sK12
| ~ spl29_14
| ~ spl29_32
| ~ spl29_69 ),
inference(forward_subsumption_resolution,[],[f19094,f427]) ).
fof(f19132,plain,
( $false
| spl29_13
| ~ spl29_14
| ~ spl29_32
| ~ spl29_69 ),
inference(forward_subsumption_resolution,[],[f19112,f422]) ).
fof(f19133,plain,
( spl29_13
| ~ spl29_14
| ~ spl29_32
| ~ spl29_69 ),
inference(avatar_contradiction_clause,[],[f19132]) ).
fof(f19935,plain,
( sz00 = sK12
| ~ isPrime0(sK12)
| ~ aInteger0(sK12)
| ~ aInteger0(xn)
| ~ aDivisorOf0(xn,smndt0(xn))
| ~ spl29_11
| ~ spl29_12
| spl29_13
| ~ spl29_14
| ~ spl29_15
| spl29_64 ),
inference(resolution,[],[f18893,f17363]) ).
fof(f19946,plain,
( ~ isPrime0(sK12)
| ~ aInteger0(sK12)
| ~ aInteger0(xn)
| ~ aDivisorOf0(xn,smndt0(xn))
| ~ spl29_11
| ~ spl29_12
| spl29_13
| ~ spl29_14
| ~ spl29_15
| spl29_64 ),
inference(forward_subsumption_resolution,[],[f19935,f422]) ).
fof(f19949,plain,
( ~ aInteger0(sK12)
| ~ aInteger0(xn)
| ~ aDivisorOf0(xn,smndt0(xn))
| ~ spl29_9
| ~ spl29_11
| ~ spl29_12
| spl29_13
| ~ spl29_14
| ~ spl29_15
| spl29_64 ),
inference(forward_subsumption_resolution,[],[f19946,f402]) ).
fof(f19950,plain,
( ~ aInteger0(xn)
| ~ aDivisorOf0(xn,smndt0(xn))
| ~ spl29_9
| ~ spl29_11
| ~ spl29_12
| spl29_13
| ~ spl29_14
| ~ spl29_15
| spl29_64 ),
inference(forward_subsumption_resolution,[],[f19949,f427]) ).
fof(f19951,plain,
( ~ aDivisorOf0(xn,smndt0(xn))
| ~ spl29_9
| ~ spl29_11
| ~ spl29_12
| spl29_13
| ~ spl29_14
| ~ spl29_15
| spl29_64 ),
inference(forward_subsumption_resolution,[],[f19950,f212]) ).
fof(f19952,plain,
( $false
| ~ spl29_9
| ~ spl29_11
| ~ spl29_12
| spl29_13
| ~ spl29_14
| ~ spl29_15
| spl29_64
| ~ spl29_226 ),
inference(forward_subsumption_resolution,[],[f19951,f17517]) ).
fof(f19953,plain,
( ~ spl29_9
| ~ spl29_11
| ~ spl29_12
| spl29_13
| ~ spl29_14
| ~ spl29_15
| spl29_64
| ~ spl29_226 ),
inference(avatar_contradiction_clause,[],[f19952]) ).
fof(f20349,plain,
( ! [X0] :
( ~ sdteqdtlpzmzozddtrp0(sz00,sz00,X0)
| sz00 = X0
| ~ isPrime0(X0)
| ~ aInteger0(X0) )
| ~ spl29_15
| ~ spl29_20 ),
inference(superposition,[],[f18893,f490]) ).
fof(f20352,plain,
( ! [X0] :
( sz00 = X0
| ~ isPrime0(X0)
| ~ aInteger0(X0) )
| ~ spl29_15
| ~ spl29_20
| ~ spl29_23 ),
inference(forward_subsumption_resolution,[],[f20349,f12641]) ).
fof(f20454,plain,
( spl29_19
| ~ spl29_15
| ~ spl29_20
| ~ spl29_23 ),
inference(avatar_split_clause,[],[f20352,f654,f489,f431,f486]) ).
fof(f20521,plain,
( ! [X0,X1] :
( sdtpldt0(X0,X1) = X1
| ~ aInteger0(X1)
| ~ isPrime0(X0)
| ~ aInteger0(X0) )
| ~ spl29_19 ),
inference(superposition,[],[f257,f487]) ).
fof(f20788,plain,
( ! [X0] :
( sz00 = smndt0(X0)
| ~ aInteger0(X0)
| ~ aInteger0(smndt0(X0))
| ~ isPrime0(X0)
| ~ aInteger0(X0) )
| ~ spl29_19 ),
inference(superposition,[],[f241,f20521]) ).
fof(f20849,plain,
( ! [X0] :
( sz00 = smndt0(X0)
| ~ aInteger0(X0)
| ~ aInteger0(smndt0(X0))
| ~ isPrime0(X0) )
| ~ spl29_19 ),
inference(duplicate_literal_removal,[],[f20788]) ).
fof(f20912,plain,
( ! [X0] :
( sz00 = smndt0(X0)
| ~ aInteger0(X0)
| ~ isPrime0(X0) )
| ~ spl29_19 ),
inference(forward_subsumption_resolution,[],[f20849,f242]) ).
fof(f21030,plain,
( sz00 != sz00
| ~ aInteger0(sK12)
| ~ isPrime0(sK12)
| ~ spl29_19
| spl29_69 ),
inference(superposition,[],[f4260,f20912]) ).
fof(f21038,plain,
( ~ aInteger0(sK12)
| ~ isPrime0(sK12)
| ~ spl29_19
| spl29_69 ),
inference(trivial_inequality_removal,[],[f21030]) ).
fof(f21079,plain,
( ~ isPrime0(sK12)
| ~ spl29_14
| ~ spl29_19
| spl29_69 ),
inference(forward_subsumption_resolution,[],[f21038,f427]) ).
fof(f21107,plain,
( $false
| ~ spl29_9
| ~ spl29_14
| ~ spl29_19
| spl29_69 ),
inference(forward_subsumption_resolution,[],[f21079,f402]) ).
fof(f21108,plain,
( ~ spl29_9
| ~ spl29_14
| ~ spl29_19
| spl29_69 ),
inference(avatar_contradiction_clause,[],[f21107]) ).
fof(f21199,plain,
( sz00 != smndt0(sz00)
| ~ spl29_20
| ~ spl29_21
| spl29_47 ),
inference(forward_demodulation,[],[f3971,f562]) ).
fof(f21243,plain,
( $false
| ~ spl29_20
| ~ spl29_21
| ~ spl29_23
| spl29_47 ),
inference(forward_subsumption_resolution,[],[f21199,f655]) ).
fof(f21244,plain,
( ~ spl29_20
| ~ spl29_21
| ~ spl29_23
| spl29_47 ),
inference(avatar_contradiction_clause,[],[f21243]) ).
cnf(s1,plain,
( ~ spl29_1
| spl29_2 ),
inference(sat_conversion,[],[f370]) ).
cnf(s3,plain,
( spl29_3
| spl29_5 ),
inference(sat_conversion,[],[f385]) ).
cnf(s4,plain,
( spl29_3
| spl29_6 ),
inference(sat_conversion,[],[f390]) ).
cnf(s5,plain,
( spl29_3
| spl29_7 ),
inference(sat_conversion,[],[f394]) ).
cnf(s7,plain,
( ~ spl29_3
| spl29_9 ),
inference(sat_conversion,[],[f403]) ).
cnf(s9,plain,
( ~ spl29_3
| spl29_11 ),
inference(sat_conversion,[],[f413]) ).
cnf(s10,plain,
( ~ spl29_3
| spl29_12 ),
inference(sat_conversion,[],[f418]) ).
cnf(s11,plain,
( ~ spl29_3
| ~ spl29_13 ),
inference(sat_conversion,[],[f423]) ).
cnf(s12,plain,
( ~ spl29_3
| spl29_14 ),
inference(sat_conversion,[],[f428]) ).
cnf(s14,plain,
( ~ spl29_3
| spl29_15 ),
inference(sat_conversion,[],[f433]) ).
cnf(s19,plain,
spl29_1,
inference(sat_conversion,[],[f647]) ).
cnf(s22,plain,
spl29_23,
inference(sat_conversion,[],[f664]) ).
cnf(s33,plain,
( ~ spl29_1
| spl29_27
| spl29_32 ),
inference(sat_conversion,[],[f1043]) ).
cnf(s42,plain,
( spl29_21
| ~ spl29_27 ),
inference(sat_conversion,[],[f1488]) ).
cnf(s54,plain,
( ~ spl29_7
| spl29_47
| spl29_48 ),
inference(sat_conversion,[],[f2614]) ).
cnf(s56,plain,
( ~ spl29_47
| ~ spl29_49
| spl29_50 ),
inference(sat_conversion,[],[f2762]) ).
cnf(s58,plain,
( ~ spl29_47
| ~ spl29_49
| spl29_50 ),
inference(sat_conversion,[],[f2772]) ).
cnf(s67,plain,
spl29_49,
inference(sat_conversion,[],[f2796]) ).
cnf(s90,plain,
( ~ spl29_5
| ~ spl29_6
| ~ spl29_15 ),
inference(sat_conversion,[],[f4066]) ).
cnf(s97,plain,
( ~ spl29_11
| ~ spl29_14
| spl29_20
| ~ spl29_64 ),
inference(sat_conversion,[],[f4183]) ).
cnf(s131,plain,
( ~ spl29_1
| ~ spl29_11
| ~ spl29_12
| spl29_13
| ~ spl29_14
| ~ spl29_50
| spl29_80
| ~ spl29_96 ),
inference(sat_conversion,[],[f4779]) ).
cnf(s132,plain,
( ~ spl29_12
| spl29_96 ),
inference(sat_conversion,[],[f4782]) ).
cnf(s133,plain,
( ~ spl29_9
| ~ spl29_80 ),
inference(sat_conversion,[],[f4786]) ).
cnf(s278,plain,
( spl29_15
| ~ spl29_50 ),
inference(sat_conversion,[],[f17056]) ).
cnf(s304,plain,
( ~ spl29_2
| ~ spl29_5
| ~ spl29_6
| ~ spl29_48 ),
inference(sat_conversion,[],[f17246]) ).
cnf(s352,plain,
( ~ spl29_1
| ~ spl29_11
| ~ spl29_12
| ~ spl29_14
| spl29_20
| spl29_226 ),
inference(sat_conversion,[],[f17966]) ).
cnf(s373,plain,
( spl29_13
| ~ spl29_14
| ~ spl29_32
| ~ spl29_69 ),
inference(sat_conversion,[],[f19133]) ).
cnf(s416,plain,
( ~ spl29_9
| ~ spl29_11
| ~ spl29_12
| spl29_13
| ~ spl29_14
| ~ spl29_15
| spl29_64
| ~ spl29_226 ),
inference(sat_conversion,[],[f19953]) ).
cnf(s474,plain,
( ~ spl29_15
| spl29_19
| ~ spl29_20
| ~ spl29_23 ),
inference(sat_conversion,[],[f20454]) ).
cnf(s483,plain,
( ~ spl29_9
| ~ spl29_14
| ~ spl29_19
| spl29_69 ),
inference(sat_conversion,[],[f21108]) ).
cnf(s494,plain,
( ~ spl29_20
| ~ spl29_21
| ~ spl29_23
| spl29_47 ),
inference(sat_conversion,[],[f21244]) ).
cnf(s513,plain,
( ~ spl29_47
| spl29_50 ),
inference(rat,[],[s58,s67]) ).
cnf(s515,plain,
( ~ spl29_47
| spl29_50 ),
inference(rat,[],[s56,s67]) ).
cnf(s520,plain,
spl29_2,
inference(rat,[],[s1,s19]) ).
cnf(s521,plain,
spl29_3,
inference(rat,[],[s515,s278,s54,s90,s304,s3,s4,s5,s520]) ).
cnf(s522,plain,
spl29_15,
inference(rat,[],[s14,s521]) ).
cnf(s524,plain,
spl29_14,
inference(rat,[],[s12,s521]) ).
cnf(s525,plain,
~ spl29_13,
inference(rat,[],[s11,s521]) ).
cnf(s526,plain,
spl29_12,
inference(rat,[],[s10,s521]) ).
cnf(s527,plain,
spl29_11,
inference(rat,[],[s9,s521]) ).
cnf(s529,plain,
spl29_9,
inference(rat,[],[s7,s521]) ).
cnf(s536,plain,
spl29_96,
inference(rat,[],[s132,s526]) ).
cnf(s558,plain,
~ spl29_80,
inference(rat,[],[s133,s529]) ).
cnf(s562,plain,
~ spl29_50,
inference(rat,[],[s131,s536,s527,s526,s524,s525,s19,s558]) ).
cnf(s577,plain,
~ spl29_47,
inference(rat,[],[s513,s562]) ).
cnf(s578,plain,
spl29_20,
inference(rat,[],[s416,s352,s97,s526,s525,s524,s522,s527,s529,s19]) ).
cnf(s579,plain,
~ spl29_21,
inference(rat,[],[s494,s577,s22,s578]) ).
cnf(s587,plain,
spl29_19,
inference(rat,[],[s474,s22,s522,s578]) ).
cnf(s595,plain,
~ spl29_27,
inference(rat,[],[s42,s579]) ).
cnf(s601,plain,
spl29_69,
inference(rat,[],[s483,s529,s524,s587]) ).
cnf(s608,plain,
spl29_32,
inference(rat,[],[s33,s19,s595]) ).
cnf(s614,plain,
$false,
inference(rat,[],[s373,s525,s524,s608,s601]) ).
fof(f21297,plain,
$false,
inference(avatar_sat_refutation,[],[s614]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM447+5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.36 % Computer : n002.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Sun Sep 27 20:00:36 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.40 Running first-order theorem proving
% 0.15/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.67/2.74 % (3841221)Detected formulas, will run a generic FOF schedule.
% 12.67/2.74 % (3841379)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=3243634876:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.67/2.74 % (3841378)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=2953816463:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.67/2.74 % (3841380)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=2069507227:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.67/2.74 % (3841381)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=238771328:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.67/2.74 % (3841382)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1869033858:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.67/2.74 % (3841383)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2001283023:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.67/2.74 % (3841384)dis-21_1_sil=8000:lcm=predicate:random_seed=1667946216: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)
% 12.67/2.74 % (3841381)Instruction limit reached!
% 12.67/2.74 % (3841381)------------------------------
% 12.67/2.74 % (3841381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.67/2.74 % (3841381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.67/2.74 % (3841381)CaDiCaL version: 2.1.3
% 12.67/2.74 % (3841381)Termination reason: Instruction limit
% 12.67/2.74 % (3841381)Termination phase: Saturation
% 12.67/2.74 % (3841381)Time elapsed: 0.069 s
% 12.67/2.74 % (3841381)Peak memory usage: 89 MB
% 12.67/2.74 % (3841381)Instructions burned: 110 (million)
% 12.67/2.74 % (3841382)Instruction limit reached!
% 12.67/2.74 % (3841382)------------------------------
% 12.67/2.74 % (3841382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.67/2.74 % (3841382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.67/2.74 % (3841382)CaDiCaL version: 2.1.3
% 12.67/2.74 % (3841382)Termination reason: Instruction limit
% 12.67/2.74 % (3841382)Termination phase: Saturation
% 12.67/2.74 % (3841382)Time elapsed: 0.070 s
% 12.67/2.74 % (3841382)Peak memory usage: 88 MB
% 12.67/2.74 % (3841382)Instructions burned: 120 (million)
% 12.67/2.74 % (3841384)Instruction limit reached!
% 12.67/2.74 % (3841384)------------------------------
% 12.67/2.74 % (3841384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.67/2.74 % (3841384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.67/2.74 % (3841384)CaDiCaL version: 2.1.3
% 12.67/2.74 % (3841384)Termination reason: Instruction limit
% 12.67/2.74 % (3841384)Termination phase: Saturation
% 12.67/2.74 % (3841384)Time elapsed: 0.080 s
% 12.67/2.74 % (3841384)Peak memory usage: 89 MB
% 12.67/2.74 % (3841384)Instructions burned: 130 (million)
% 12.67/2.74 % (3841383)Instruction limit reached!
% 12.67/2.74 % (3841383)------------------------------
% 12.67/2.74 % (3841383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.67/2.74 % (3841383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.67/2.74 % (3841383)CaDiCaL version: 2.1.3
% 12.67/2.74 % (3841383)Termination reason: Instruction limit
% 12.67/2.74 % (3841383)Termination phase: Saturation
% 12.67/2.74 % (3841383)Time elapsed: 0.093 s
% 12.67/2.74 % (3841383)Peak memory usage: 90 MB
% 12.67/2.74 % (3841383)Instructions burned: 139 (million)
% 12.67/2.74 % (3841393)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3252940814:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.67/2.74 % (3841392)lrs+10_1_sil=8000:sp=occurrence:random_seed=3550024815:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.67/2.74 % (3841394)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1172910675:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 12.67/2.74 % (3841395)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=3006082659:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 12.67/2.74 % (3841393)Instruction limit reached!
% 17.43/3.37 % (3841393)------------------------------
% 17.43/3.37 % (3841393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.43/3.37 % (3841393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.43/3.37 % (3841393)CaDiCaL version: 2.1.3
% 17.43/3.37 % (3841393)Termination reason: Instruction limit
% 17.43/3.37 % (3841393)Termination phase: Saturation
% 17.43/3.37 % (3841393)Time elapsed: 0.077 s
% 17.43/3.37 % (3841393)Peak memory usage: 92 MB
% 17.43/3.37 % (3841393)Instructions burned: 159 (million)
% 17.43/3.37 % (3841395)Instruction limit reached!
% 17.43/3.37 % (3841395)------------------------------
% 17.43/3.37 % (3841395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.43/3.37 % (3841395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.43/3.37 % (3841395)CaDiCaL version: 2.1.3
% 17.43/3.37 % (3841395)Termination reason: Instruction limit
% 17.43/3.37 % (3841395)Termination phase: Saturation
% 17.43/3.37 % (3841395)Time elapsed: 0.125 s
% 17.43/3.37 % (3841395)Peak memory usage: 94 MB
% 17.43/3.37 % (3841395)Instructions burned: 249 (million)
% 17.43/3.37 % (3841392)Instruction limit reached!
% 17.43/3.37 % (3841392)------------------------------
% 17.43/3.37 % (3841392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.43/3.37 % (3841392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.43/3.37 % (3841392)CaDiCaL version: 2.1.3
% 17.43/3.37 % (3841392)Termination reason: Instruction limit
% 17.43/3.37 % (3841392)Termination phase: Saturation
% 17.43/3.37 % (3841392)Time elapsed: 0.177 s
% 17.43/3.37 % (3841392)Peak memory usage: 92 MB
% 17.43/3.37 % (3841392)Instructions burned: 286 (million)
% 17.43/3.37 % (3841400)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=505685674:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 17.43/3.37 % (3841394)Instruction limit reached!
% 17.43/3.37 % (3841394)------------------------------
% 17.43/3.37 % (3841394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.43/3.37 % (3841394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.43/3.37 % (3841394)CaDiCaL version: 2.1.3
% 17.43/3.37 % (3841394)Termination reason: Instruction limit
% 17.43/3.37 % (3841394)Termination phase: Saturation
% 17.43/3.37 % (3841394)Time elapsed: 0.207 s
% 17.43/3.37 % (3841394)Peak memory usage: 93 MB
% 17.43/3.37 % (3841394)Instructions burned: 326 (million)
% 17.43/3.37 % (3841400)Instruction limit reached!
% 17.43/3.37 % (3841400)------------------------------
% 17.43/3.37 % (3841400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.43/3.37 % (3841400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.43/3.37 % (3841400)CaDiCaL version: 2.1.3
% 17.43/3.37 % (3841400)Termination reason: Instruction limit
% 17.43/3.37 % (3841400)Termination phase: Saturation
% 17.43/3.37 % (3841400)Time elapsed: 0.091 s
% 17.43/3.37 % (3841400)Peak memory usage: 90 MB
% 17.43/3.37 % (3841400)Instructions burned: 294 (million)
% 17.43/3.37 % (3841401)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1231522944:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 17.43/3.37 % (3841402)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3450555306:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 17.43/3.37 % (3841404)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2628864803:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 17.43/3.37 % (3841402)Instruction limit reached!
% 17.43/3.37 % (3841402)------------------------------
% 17.43/3.37 % (3841402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.43/3.37 % (3841402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.43/3.37 % (3841402)CaDiCaL version: 2.1.3
% 17.43/3.37 % (3841402)Termination reason: Instruction limit
% 17.43/3.37 % (3841402)Termination phase: Saturation
% 17.43/3.37 % (3841402)Time elapsed: 0.074 s
% 17.43/3.37 % (3841402)Peak memory usage: 90 MB
% 17.43/3.37 % (3841402)Instructions burned: 113 (million)
% 17.43/3.37 % (3841405)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1605406601:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 17.43/3.37 % (3841404)Instruction limit reached!
% 17.43/3.37 % (3841404)------------------------------
% 17.43/3.37 % (3841404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.43/3.37 % (3841404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/3.91 % (3841404)CaDiCaL version: 2.1.3
% 9.90/3.91 % (3841404)Termination reason: Instruction limit
% 9.90/3.91 % (3841404)Termination phase: Saturation
% 9.90/3.91 % (3841404)Time elapsed: 0.064 s
% 9.90/3.91 % (3841404)Peak memory usage: 89 MB
% 9.90/3.91 % (3841404)Instructions burned: 127 (million)
% 9.90/3.91 % (3841405)Instruction limit reached!
% 9.90/3.91 % (3841405)------------------------------
% 9.90/3.91 % (3841405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/3.91 % (3841405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/3.91 % (3841405)CaDiCaL version: 2.1.3
% 9.90/3.91 % (3841405)Termination reason: Instruction limit
% 9.90/3.91 % (3841405)Termination phase: Saturation
% 9.90/3.91 % (3841405)Time elapsed: 0.033 s
% 9.90/3.91 % (3841405)Peak memory usage: 89 MB
% 9.90/3.91 % (3841405)Instructions burned: 115 (million)
% 9.90/3.91 % (3841412)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3835316733:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 9.90/3.91 % (3841409)lrs+10_1_sil=8000:sp=occurrence:random_seed=1961301025:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 9.90/3.91 % (3841411)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3777376708:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 9.90/3.91 % (3841411)Instruction limit reached!
% 9.90/3.91 % (3841411)------------------------------
% 9.90/3.91 % (3841411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/3.91 % (3841411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/3.91 % (3841411)CaDiCaL version: 2.1.3
% 9.90/3.91 % (3841411)Termination reason: Instruction limit
% 9.90/3.91 % (3841411)Termination phase: Saturation
% 9.90/3.91 % (3841411)Time elapsed: 0.270 s
% 9.90/3.91 % (3841411)Peak memory usage: 92 MB
% 9.90/3.91 % (3841411)Instructions burned: 438 (million)
% 9.90/3.91 % (3841416)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=455866762:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 9.90/3.91 % (3841409)Instruction limit reached!
% 9.90/3.91 % (3841409)------------------------------
% 9.90/3.91 % (3841409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/3.91 % (3841409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/3.91 % (3841409)CaDiCaL version: 2.1.3
% 9.90/3.91 % (3841409)Termination reason: Instruction limit
% 9.90/3.91 % (3841409)Termination phase: Saturation
% 9.90/3.91 % (3841409)Time elapsed: 0.514 s
% 9.90/3.91 % (3841409)Peak memory usage: 99 MB
% 9.90/3.91 % (3841409)Instructions burned: 909 (million)
% 9.90/3.91 % (3841416)Instruction limit reached!
% 9.90/3.91 % (3841416)------------------------------
% 9.90/3.91 % (3841416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/3.91 % (3841416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/3.91 % (3841416)CaDiCaL version: 2.1.3
% 9.90/3.91 % (3841416)Termination reason: Instruction limit
% 9.90/3.91 % (3841416)Termination phase: Saturation
% 9.90/3.91 % (3841416)Time elapsed: 0.065 s
% 9.90/3.91 % (3841416)Peak memory usage: 91 MB
% 9.90/3.91 % (3841416)Instructions burned: 134 (million)
% 9.90/3.91 % (3841418)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3597026904:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 9.90/3.91 % (3841419)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3923948126:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 9.90/3.91 % (3841401)Instruction limit reached!
% 9.90/3.91 % (3841401)------------------------------
% 9.90/3.91 % (3841401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/3.91 % (3841401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/3.91 % (3841401)CaDiCaL version: 2.1.3
% 9.90/3.91 % (3841401)Termination reason: Instruction limit
% 9.90/3.91 % (3841401)Termination phase: Saturation
% 9.90/3.91 % (3841401)Time elapsed: 1.050 s
% 9.90/3.91 % (3841401)Peak memory usage: 143 MB
% 9.90/3.91 % (3841401)Instructions burned: 2352 (million)
% 9.90/3.91 % (3841422)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1102828588:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi)
% 9.90/3.91 % (3841422)Instruction limit reached!
% 9.90/3.91 % (3841422)------------------------------
% 9.90/3.91 % (3841422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/3.91 % (3841422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/3.91 % (3841422)CaDiCaL version: 2.1.3
% 9.90/3.91 % (3841422)Termination reason: Instruction limit
% 9.90/3.91 % (3841422)Termination phase: Saturation
% 9.90/3.91 % (3841422)Time elapsed: 0.038 s
% 9.90/3.91 % (3841422)Peak memory usage: 91 MB
% 9.90/3.91 % (3841422)Instructions burned: 127 (million)
% 9.90/3.91 % (3841418)Instruction limit reached!
% 9.90/3.91 % (3841418)------------------------------
% 9.90/3.91 % (3841418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/3.91 % (3841418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/3.91 % (3841418)CaDiCaL version: 2.1.3
% 9.90/3.91 % (3841418)Termination reason: Instruction limit
% 9.90/3.91 % (3841418)Termination phase: Saturation
% 9.90/3.91 % (3841418)Time elapsed: 0.373 s
% 9.90/3.91 % (3841418)Peak memory usage: 95 MB
% 9.90/3.91 % (3841418)Instructions burned: 593 (million)
% 9.90/3.91 % (3841424)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3404924295:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi)
% 9.90/3.91 % (3841424)Instruction limit reached!
% 9.90/3.91 % (3841424)------------------------------
% 9.90/3.91 % (3841424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/3.91 % (3841424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/3.91 % (3841424)CaDiCaL version: 2.1.3
% 9.90/3.91 % (3841424)Termination reason: Instruction limit
% 9.90/3.91 % (3841424)Termination phase: Saturation
% 9.90/3.91 % (3841424)Time elapsed: 0.044 s
% 9.90/3.91 % (3841424)Peak memory usage: 91 MB
% 9.90/3.91 % (3841424)Instructions burned: 137 (million)
% 9.90/3.91 % (3841425)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2112385210:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi)
% 9.90/3.91 % (3841427)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2269427265:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2979 on theBenchmark for (2979ds/431Mi)
% 9.90/3.91 % (3841425)Instruction limit reached!
% 9.90/3.91 % (3841425)------------------------------
% 9.90/3.91 % (3841425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/3.91 % (3841425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/3.91 % (3841425)CaDiCaL version: 2.1.3
% 9.90/3.91 % (3841425)Termination reason: Instruction limit
% 9.90/3.91 % (3841425)Termination phase: Saturation
% 9.90/3.91 % (3841425)Time elapsed: 0.082 s
% 9.90/3.91 % (3841425)Peak memory usage: 92 MB
% 9.90/3.91 % (3841425)Instructions burned: 141 (million)
% 9.90/3.91 % (3841427)Instruction limit reached!
% 9.90/3.91 % (3841427)------------------------------
% 9.90/3.91 % (3841427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/3.91 % (3841427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/3.91 % (3841427)CaDiCaL version: 2.1.3
% 9.90/3.91 % (3841427)Termination reason: Instruction limit
% 9.90/3.91 % (3841427)Termination phase: Saturation
% 9.90/3.91 % (3841427)Time elapsed: 0.128 s
% 9.90/3.91 % (3841427)Peak memory usage: 93 MB
% 9.90/3.91 % (3841427)Instructions burned: 434 (million)
% 9.90/3.91 % (3841430)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=4076007938:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi)
% 9.90/3.91 % (3841431)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2404113788:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2976 on theBenchmark for (2976ds/150Mi)
% 9.90/3.91 % (3841431)Instruction limit reached!
% 9.90/3.91 % (3841431)------------------------------
% 9.90/3.91 % (3841431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.90/3.91 % (3841431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.90/3.91 % (3841431)CaDiCaL version: 2.1.3
% 9.90/3.91 % (3841431)Termination reason: Instruction limit
% 9.90/3.91 % (3841431)Termination phase: Saturation
% 9.90/3.91 % (3841431)Time elapsed: 0.046 s
% 9.90/3.91 % (3841431)Peak memory usage: 92 MB
% 9.90/3.91 % (3841431)Instructions burned: 152 (million)
% 9.90/3.91 % (3841434)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3983873527:i=14155:bd=all_2974 on theBenchmark for (2974ds/14155Mi)
% 9.90/3.91 % (3841412)First to succeed.
% 9.90/3.91 % (3841412)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3841221"
% 9.90/3.91 % (3841412)Refutation found. Thanks to Tanya!
% 9.90/3.91 % SZS status Theorem for theBenchmark
% 9.90/3.91 % SZS output start Proof for theBenchmark
% See solution above
% 22.20/4.11 % (3841412)------------------------------
% 22.20/4.11 % (3841412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.20/4.11 % (3841412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.20/4.11 % (3841412)CaDiCaL version: 2.1.3
% 22.20/4.11 % (3841412)Termination reason: Refutation
% 22.20/4.11 % (3841412)Time elapsed: 1.824 s
% 22.20/4.11 % (3841412)Peak memory usage: 147 MB
% 22.20/4.11 % (3841412)Instructions burned: 3222 (million)
% 22.20/4.11 % (3841412)------------------------------
% 22.20/4.11 % (3841412)------------------------------
% 22.20/4.11 % (3841221)Success in time 3.062 s
% 22.20/4.11 % Vampire exiting
%------------------------------------------------------------------------------