%------------------------------------------------------------------------------
% File : Vampire-SAT---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 SAT
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:24:21 PM UTC 2026
% Result : Theorem 19.38s 5.22s
% Output : Refutation 19.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 39
% Syntax : Number of formulae : 318 ( 24 unt; 28 def)
% Number of atoms : 1202 ( 232 equ)
% Maximal formula atoms : 38 ( 3 avg)
% Number of connectives : 1387 ( 503 ~; 649 |; 177 &)
% ( 32 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 36 ( 34 usr; 29 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 8 con; 0-2 aty)
% Number of variables : 199 ( 0 sgn 153 !; 46 ?)
% 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(f9,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddZero) ).
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(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(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(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(f47,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(f48,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(f52,plain,
! [X0] :
( aInteger0(smndt0(X0))
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f61,plain,
! [X0] :
( ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f70,plain,
! [X0] :
( ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f71,plain,
! [X0] :
( ( sdtasdt0(smndt0(sz10),X0) = smndt0(X0)
& smndt0(X0) = sdtasdt0(X0,smndt0(sz10)) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f74,plain,
! [X0] :
( ! [X1] :
( aDivisorOf0(X1,X0)
<=> ( aInteger0(X1)
& X1 != sz00
& ? [X2] :
( aInteger0(X2)
& sdtasdt0(X1,X2) = X0 ) ) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f87,plain,
! [X0] :
( ( ? [X1] :
( aDivisorOf0(X1,X0)
& isPrime0(X1) )
<=> ( X0 != sz10
& X0 != smndt0(sz10) ) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f110,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,[],[f47]) ).
fof(f111,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,[],[f110]) ).
fof(f112,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,[],[f48]) ).
fof(f113,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,[],[f112]) ).
fof(f114,plain,
aInteger0(sz00),
inference(cnf_transformation,[],[f2]) ).
fof(f115,plain,
aInteger0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f116,plain,
! [X0] :
( aInteger0(smndt0(X0))
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f52]) ).
fof(f122,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,sz00) = X0 ),
inference(cnf_transformation,[],[f61]) ).
fof(f131,plain,
! [X0] :
( ~ aInteger0(X0)
| sz00 = sdtasdt0(sz00,X0) ),
inference(cnf_transformation,[],[f70]) ).
fof(f133,plain,
! [X0] :
( ~ aInteger0(X0)
| smndt0(X0) = sdtasdt0(X0,smndt0(sz10)) ),
inference(cnf_transformation,[],[f71]) ).
fof(f139,plain,
! [X0,X1] :
( ~ aInteger0(X0)
| sz00 != X1
| ~ aDivisorOf0(X1,X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f140,plain,
! [X0,X1] :
( ~ aDivisorOf0(X1,X0)
| aInteger0(X1)
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f148,plain,
! [X0] :
( ~ aInteger0(X0)
| smndt0(sz10) = X0
| sz10 = X0
| isPrime0(sK1(X0)) ),
inference(cnf_transformation,[],[f87]) ).
fof(f149,plain,
! [X0] :
( aDivisorOf0(sK1(X0),X0)
| smndt0(sz10) = X0
| sz10 = X0
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f87]) ).
fof(f150,plain,
! [X0,X1] :
( ~ aInteger0(X0)
| sz10 != X0
| ~ isPrime0(X1)
| ~ aDivisorOf0(X1,X0) ),
inference(cnf_transformation,[],[f87]) ).
fof(f151,plain,
! [X0,X1] :
( ~ aInteger0(X0)
| smndt0(sz10) != X0
| ~ isPrime0(X1)
| ~ aDivisorOf0(X1,X0) ),
inference(cnf_transformation,[],[f87]) ).
fof(f222,plain,
! [X2,X0] :
( ~ aElementOf0(X0,xS)
| ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,sK14(X0)))
| sdtpldt0(X2,smndt0(sz00)) = sdtasdt0(sK14(X0),sK15(X0,X2)) ),
inference(cnf_transformation,[],[f111]) ).
fof(f223,plain,
! [X2,X0] :
( ~ aElementOf0(X0,xS)
| ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,sK14(X0)))
| aInteger0(sK15(X0,X2)) ),
inference(cnf_transformation,[],[f111]) ).
fof(f229,plain,
! [X0,X6,X5] :
( ~ aDivisorOf0(X5,sdtpldt0(X6,smndt0(sz00)))
| ~ aInteger0(X6)
| aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(sz00,X5))
| ~ isPrime0(X5)
| sz00 = X5
| ~ aInteger0(X5)
| aElementOf0(X0,xS) ),
inference(cnf_transformation,[],[f111]) ).
fof(f236,plain,
! [X0,X5] :
( szAzrzSzezqlpdtcmdtrp0(sz00,X5) != X0
| ~ isPrime0(X5)
| sz00 = X5
| ~ aInteger0(X5)
| aElementOf0(X0,xS) ),
inference(cnf_transformation,[],[f111]) ).
fof(f237,plain,
! [X0] :
( ~ aElementOf0(X0,xS)
| szAzrzSzezqlpdtcmdtrp0(sz00,sK14(X0)) = X0 ),
inference(cnf_transformation,[],[f111]) ).
fof(f239,plain,
! [X0] :
( ~ aElementOf0(X0,xS)
| isPrime0(sK14(X0)) ),
inference(cnf_transformation,[],[f111]) ).
fof(f240,plain,
! [X0] :
( ~ aElementOf0(X0,xS)
| sz00 != sK14(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f241,plain,
! [X0] :
( ~ aElementOf0(X0,xS)
| aInteger0(sK14(X0)) ),
inference(cnf_transformation,[],[f111]) ).
fof(f242,plain,
xS = cS2043,
inference(cnf_transformation,[],[f111]) ).
fof(f244,plain,
aInteger0(xn),
inference(cnf_transformation,[],[f43]) ).
fof(f247,plain,
! [X2,X1,X5] :
( ~ aElementOf0(xn,X5)
| ~ aElementOf0(X5,xS)
| ~ isPrime0(X1)
| sdtasdt0(X1,X2) != xn
| ~ aInteger0(X2)
| sz00 = X1
| ~ aInteger0(X1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f248,plain,
! [X2,X1] :
( isPrime0(sK17)
| ~ isPrime0(X1)
| sdtasdt0(X1,X2) != xn
| ~ aInteger0(X2)
| sz00 = X1
| ~ aInteger0(X1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f249,plain,
! [X2,X1] :
( aDivisorOf0(sK17,xn)
| ~ isPrime0(X1)
| sdtasdt0(X1,X2) != xn
| ~ aInteger0(X2)
| sz00 = X1
| ~ aInteger0(X1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f255,plain,
( xn = sdtasdt0(sK17,sK19)
| aElementOf0(sK18,xS) ),
inference(cnf_transformation,[],[f113]) ).
fof(f256,plain,
( aInteger0(sK19)
| aElementOf0(sK18,xS) ),
inference(cnf_transformation,[],[f113]) ).
fof(f257,plain,
( xn = sdtasdt0(sK17,sK19)
| aElementOf0(xn,sK18) ),
inference(cnf_transformation,[],[f113]) ).
fof(f258,plain,
( aInteger0(sK19)
| aElementOf0(xn,sK18) ),
inference(cnf_transformation,[],[f113]) ).
fof(f269,plain,
( aInteger0(sK17)
| aElementOf0(xn,sK18) ),
inference(cnf_transformation,[],[f113]) ).
fof(f270,plain,
( aInteger0(sK17)
| aElementOf0(sK18,xS) ),
inference(cnf_transformation,[],[f113]) ).
fof(f271,plain,
( sz00 != sK17
| aElementOf0(xn,sK18) ),
inference(cnf_transformation,[],[f113]) ).
fof(f272,plain,
( sz00 != sK17
| aElementOf0(sK18,xS) ),
inference(cnf_transformation,[],[f113]) ).
fof(f275,plain,
( isPrime0(sK17)
| aElementOf0(xn,sK18) ),
inference(cnf_transformation,[],[f113]) ).
fof(f276,plain,
( isPrime0(sK17)
| aElementOf0(sK18,xS) ),
inference(cnf_transformation,[],[f113]) ).
fof(f285,plain,
! [X0] :
( ~ aElementOf0(X0,cS2043)
| aInteger0(sK14(X0)) ),
inference(definition_unfolding,[],[f241,f242]) ).
fof(f286,plain,
! [X0] :
( ~ aElementOf0(X0,cS2043)
| sz00 != sK14(X0) ),
inference(definition_unfolding,[],[f240,f242]) ).
fof(f287,plain,
! [X0] :
( ~ aElementOf0(X0,cS2043)
| isPrime0(sK14(X0)) ),
inference(definition_unfolding,[],[f239,f242]) ).
fof(f289,plain,
! [X0] :
( ~ aElementOf0(X0,cS2043)
| szAzrzSzezqlpdtcmdtrp0(sz00,sK14(X0)) = X0 ),
inference(definition_unfolding,[],[f237,f242]) ).
fof(f290,plain,
! [X0,X5] :
( szAzrzSzezqlpdtcmdtrp0(sz00,X5) != X0
| ~ isPrime0(X5)
| sz00 = X5
| ~ aInteger0(X5)
| aElementOf0(X0,cS2043) ),
inference(definition_unfolding,[],[f236,f242]) ).
fof(f297,plain,
! [X0,X6,X5] :
( ~ aDivisorOf0(X5,sdtpldt0(X6,smndt0(sz00)))
| ~ aInteger0(X6)
| aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(sz00,X5))
| ~ isPrime0(X5)
| sz00 = X5
| ~ aInteger0(X5)
| aElementOf0(X0,cS2043) ),
inference(definition_unfolding,[],[f229,f242]) ).
fof(f303,plain,
! [X2,X0] :
( ~ aElementOf0(X0,cS2043)
| ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,sK14(X0)))
| aInteger0(sK15(X0,X2)) ),
inference(definition_unfolding,[],[f223,f242]) ).
fof(f304,plain,
! [X2,X0] :
( ~ aElementOf0(X0,cS2043)
| ~ aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,sK14(X0)))
| sdtpldt0(X2,smndt0(sz00)) = sdtasdt0(sK14(X0),sK15(X0,X2)) ),
inference(definition_unfolding,[],[f222,f242]) ).
fof(f315,plain,
( isPrime0(sK17)
| aElementOf0(sK18,cS2043) ),
inference(definition_unfolding,[],[f276,f242]) ).
fof(f317,plain,
( sz00 != sK17
| aElementOf0(sK18,cS2043) ),
inference(definition_unfolding,[],[f272,f242]) ).
fof(f318,plain,
( aInteger0(sK17)
| aElementOf0(sK18,cS2043) ),
inference(definition_unfolding,[],[f270,f242]) ).
fof(f323,plain,
( aInteger0(sK19)
| aElementOf0(sK18,cS2043) ),
inference(definition_unfolding,[],[f256,f242]) ).
fof(f324,plain,
( xn = sdtasdt0(sK17,sK19)
| aElementOf0(sK18,cS2043) ),
inference(definition_unfolding,[],[f255,f242]) ).
fof(f328,plain,
! [X2,X1,X5] :
( ~ aElementOf0(xn,X5)
| ~ aElementOf0(X5,cS2043)
| ~ isPrime0(X1)
| sdtasdt0(X1,X2) != xn
| ~ aInteger0(X2)
| sz00 = X1
| ~ aInteger0(X1) ),
inference(definition_unfolding,[],[f247,f242]) ).
fof(f329,plain,
! [X0] :
( ~ aDivisorOf0(sz00,X0)
| ~ aInteger0(X0) ),
inference(equality_resolution,[],[f139]) ).
fof(f331,plain,
! [X1] :
( ~ aInteger0(smndt0(sz10))
| ~ isPrime0(X1)
| ~ aDivisorOf0(X1,smndt0(sz10)) ),
inference(equality_resolution,[],[f151]) ).
fof(f332,plain,
! [X1] :
( ~ aInteger0(sz10)
| ~ isPrime0(X1)
| ~ aDivisorOf0(X1,sz10) ),
inference(equality_resolution,[],[f150]) ).
fof(f361,plain,
! [X5] :
( ~ isPrime0(X5)
| sz00 = X5
| ~ aInteger0(X5)
| aElementOf0(szAzrzSzezqlpdtcmdtrp0(sz00,X5),cS2043) ),
inference(equality_resolution,[],[f290]) ).
fof(f362,plain,
! [X1] :
( ~ aInteger0(smndt0(sz10))
| isPrime0(X1)
| ~ aDivisorOf0(X1,smndt0(sz10)) ),
inference(consistent_polarity_flipping,[],[f331]) ).
fof(f363,plain,
! [X1] :
( ~ aInteger0(sz10)
| isPrime0(X1)
| ~ aDivisorOf0(X1,sz10) ),
inference(consistent_polarity_flipping,[],[f332]) ).
fof(f364,plain,
! [X0] :
( ~ isPrime0(sK1(X0))
| smndt0(sz10) = X0
| sz10 = X0
| ~ aInteger0(X0) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f430,plain,
! [X0] :
( aInteger0(sK14(X0))
| aElementOf0(X0,cS2043) ),
inference(consistent_polarity_flipping,[],[f285]) ).
fof(f431,plain,
! [X0] :
( sz00 != sK14(X0)
| aElementOf0(X0,cS2043) ),
inference(consistent_polarity_flipping,[],[f286]) ).
fof(f432,plain,
! [X0] :
( ~ isPrime0(sK14(X0))
| aElementOf0(X0,cS2043) ),
inference(consistent_polarity_flipping,[],[f287]) ).
fof(f434,plain,
! [X0] :
( aElementOf0(X0,cS2043)
| szAzrzSzezqlpdtcmdtrp0(sz00,sK14(X0)) = X0 ),
inference(consistent_polarity_flipping,[],[f289]) ).
fof(f435,plain,
! [X5] :
( ~ aElementOf0(szAzrzSzezqlpdtcmdtrp0(sz00,X5),cS2043)
| sz00 = X5
| ~ aInteger0(X5)
| isPrime0(X5) ),
inference(consistent_polarity_flipping,[],[f361]) ).
fof(f442,plain,
! [X0,X6,X5] :
( ~ aDivisorOf0(X5,sdtpldt0(X6,smndt0(sz00)))
| ~ aInteger0(X6)
| ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(sz00,X5))
| isPrime0(X5)
| sz00 = X5
| ~ aInteger0(X5)
| ~ aElementOf0(X0,cS2043) ),
inference(consistent_polarity_flipping,[],[f297]) ).
fof(f448,plain,
! [X2,X0] :
( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,sK14(X0)))
| aElementOf0(X0,cS2043)
| aInteger0(sK15(X0,X2)) ),
inference(consistent_polarity_flipping,[],[f303]) ).
fof(f449,plain,
! [X2,X0] :
( aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(sz00,sK14(X0)))
| aElementOf0(X0,cS2043)
| sdtpldt0(X2,smndt0(sz00)) = sdtasdt0(sK14(X0),sK15(X0,X2)) ),
inference(consistent_polarity_flipping,[],[f304]) ).
fof(f460,plain,
( ~ isPrime0(sK17)
| ~ aElementOf0(sK18,cS2043) ),
inference(consistent_polarity_flipping,[],[f315]) ).
fof(f461,plain,
( ~ isPrime0(sK17)
| ~ aElementOf0(xn,sK18) ),
inference(consistent_polarity_flipping,[],[f275]) ).
fof(f464,plain,
( sz00 != sK17
| ~ aElementOf0(sK18,cS2043) ),
inference(consistent_polarity_flipping,[],[f317]) ).
fof(f465,plain,
( sz00 != sK17
| ~ aElementOf0(xn,sK18) ),
inference(consistent_polarity_flipping,[],[f271]) ).
fof(f466,plain,
( aInteger0(sK17)
| ~ aElementOf0(sK18,cS2043) ),
inference(consistent_polarity_flipping,[],[f318]) ).
fof(f467,plain,
( aInteger0(sK17)
| ~ aElementOf0(xn,sK18) ),
inference(consistent_polarity_flipping,[],[f269]) ).
fof(f478,plain,
( aInteger0(sK19)
| ~ aElementOf0(xn,sK18) ),
inference(consistent_polarity_flipping,[],[f258]) ).
fof(f479,plain,
( xn = sdtasdt0(sK17,sK19)
| ~ aElementOf0(xn,sK18) ),
inference(consistent_polarity_flipping,[],[f257]) ).
fof(f480,plain,
( aInteger0(sK19)
| ~ aElementOf0(sK18,cS2043) ),
inference(consistent_polarity_flipping,[],[f323]) ).
fof(f481,plain,
( xn = sdtasdt0(sK17,sK19)
| ~ aElementOf0(sK18,cS2043) ),
inference(consistent_polarity_flipping,[],[f324]) ).
fof(f487,plain,
! [X2,X1] :
( aDivisorOf0(sK17,xn)
| isPrime0(X1)
| sdtasdt0(X1,X2) != xn
| ~ aInteger0(X2)
| sz00 = X1
| ~ aInteger0(X1) ),
inference(consistent_polarity_flipping,[],[f249]) ).
fof(f488,plain,
! [X2,X1] :
( ~ isPrime0(sK17)
| isPrime0(X1)
| sdtasdt0(X1,X2) != xn
| ~ aInteger0(X2)
| sz00 = X1
| ~ aInteger0(X1) ),
inference(consistent_polarity_flipping,[],[f248]) ).
fof(f489,plain,
! [X2,X1,X5] :
( aElementOf0(xn,X5)
| aElementOf0(X5,cS2043)
| isPrime0(X1)
| sdtasdt0(X1,X2) != xn
| ~ aInteger0(X2)
| sz00 = X1
| ~ aInteger0(X1) ),
inference(consistent_polarity_flipping,[],[f328]) ).
fof(f493,definition,
( spl20_1
<=> ! [X2,X1] :
( isPrime0(X1)
| ~ aInteger0(X1)
| sz00 = X1
| ~ aInteger0(X2)
| sdtasdt0(X1,X2) != xn ) ),
introduced(definition,[new_symbols(definition,[spl20_1])],[avatar_definition]) ).
fof(f494,plain,
( ! [X2,X1] :
( sdtasdt0(X1,X2) != xn
| ~ aInteger0(X1)
| sz00 = X1
| ~ aInteger0(X2)
| isPrime0(X1) )
| ~ spl20_1 ),
inference(avatar_component_clause,[],[f493]) ).
fof(f496,definition,
( spl20_2
<=> xn = sdtasdt0(sK17,sK19) ),
introduced(definition,[new_symbols(definition,[spl20_2])],[avatar_definition]) ).
fof(f498,plain,
( xn = sdtasdt0(sK17,sK19)
| ~ spl20_2 ),
inference(avatar_component_clause,[],[f496]) ).
fof(f501,definition,
( spl20_3
<=> aInteger0(sK19) ),
introduced(definition,[new_symbols(definition,[spl20_3])],[avatar_definition]) ).
fof(f503,plain,
( aInteger0(sK19)
| ~ spl20_3 ),
inference(avatar_component_clause,[],[f501]) ).
fof(f506,definition,
( spl20_4
<=> ! [X5] :
( aElementOf0(xn,X5)
| aElementOf0(X5,cS2043) ) ),
introduced(definition,[new_symbols(definition,[spl20_4])],[avatar_definition]) ).
fof(f507,plain,
( ! [X5] :
( aElementOf0(xn,X5)
| aElementOf0(X5,cS2043) )
| ~ spl20_4 ),
inference(avatar_component_clause,[],[f506]) ).
fof(f508,plain,
( spl20_1
| spl20_4 ),
inference(avatar_split_clause,[],[f489,f506,f493]) ).
fof(f510,definition,
( spl20_5
<=> isPrime0(sK17) ),
introduced(definition,[new_symbols(definition,[spl20_5])],[avatar_definition]) ).
fof(f512,plain,
( ~ isPrime0(sK17)
| spl20_5 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f513,plain,
( spl20_1
| ~ spl20_5 ),
inference(avatar_split_clause,[],[f488,f510,f493]) ).
fof(f515,definition,
( spl20_6
<=> aDivisorOf0(sK17,xn) ),
introduced(definition,[new_symbols(definition,[spl20_6])],[avatar_definition]) ).
fof(f517,plain,
( aDivisorOf0(sK17,xn)
| ~ spl20_6 ),
inference(avatar_component_clause,[],[f515]) ).
fof(f518,plain,
( spl20_1
| spl20_6 ),
inference(avatar_split_clause,[],[f487,f515,f493]) ).
fof(f520,definition,
( spl20_7
<=> sz00 = sK17 ),
introduced(definition,[new_symbols(definition,[spl20_7])],[avatar_definition]) ).
fof(f522,plain,
( sz00 != sK17
| spl20_7 ),
inference(avatar_component_clause,[],[f520]) ).
fof(f525,definition,
( spl20_8
<=> aInteger0(sK17) ),
introduced(definition,[new_symbols(definition,[spl20_8])],[avatar_definition]) ).
fof(f537,definition,
( spl20_10
<=> aElementOf0(sK18,cS2043) ),
introduced(definition,[new_symbols(definition,[spl20_10])],[avatar_definition]) ).
fof(f539,plain,
( ~ aElementOf0(sK18,cS2043)
| spl20_10 ),
inference(avatar_component_clause,[],[f537]) ).
fof(f540,plain,
( ~ spl20_10
| spl20_2 ),
inference(avatar_split_clause,[],[f481,f496,f537]) ).
fof(f541,plain,
( ~ spl20_10
| spl20_3 ),
inference(avatar_split_clause,[],[f480,f501,f537]) ).
fof(f543,definition,
( spl20_11
<=> aElementOf0(xn,sK18) ),
introduced(definition,[new_symbols(definition,[spl20_11])],[avatar_definition]) ).
fof(f545,plain,
( ~ aElementOf0(xn,sK18)
| spl20_11 ),
inference(avatar_component_clause,[],[f543]) ).
fof(f546,plain,
( ~ spl20_11
| spl20_2 ),
inference(avatar_split_clause,[],[f479,f496,f543]) ).
fof(f547,plain,
( ~ spl20_11
| spl20_3 ),
inference(avatar_split_clause,[],[f478,f501,f543]) ).
fof(f549,definition,
( spl20_12
<=> ! [X1] :
( isPrime0(X1)
| ~ aDivisorOf0(X1,xn) ) ),
introduced(definition,[new_symbols(definition,[spl20_12])],[avatar_definition]) ).
fof(f550,plain,
( ! [X1] :
( ~ aDivisorOf0(X1,xn)
| isPrime0(X1) )
| ~ spl20_12 ),
inference(avatar_component_clause,[],[f549]) ).
fof(f561,plain,
( ~ spl20_11
| spl20_8 ),
inference(avatar_split_clause,[],[f467,f525,f543]) ).
fof(f562,plain,
( ~ spl20_10
| spl20_8 ),
inference(avatar_split_clause,[],[f466,f525,f537]) ).
fof(f563,plain,
( ~ spl20_11
| ~ spl20_7 ),
inference(avatar_split_clause,[],[f465,f520,f543]) ).
fof(f564,plain,
( ~ spl20_10
| ~ spl20_7 ),
inference(avatar_split_clause,[],[f464,f520,f537]) ).
fof(f567,plain,
( ~ spl20_11
| ~ spl20_5 ),
inference(avatar_split_clause,[],[f461,f510,f543]) ).
fof(f568,plain,
( ~ spl20_10
| ~ spl20_5 ),
inference(avatar_split_clause,[],[f460,f510,f537]) ).
fof(f577,definition,
( spl20_13
<=> ! [X0] : ~ aElementOf0(X0,cS2043) ),
introduced(definition,[new_symbols(definition,[spl20_13])],[avatar_definition]) ).
fof(f578,plain,
( ! [X0] : ~ aElementOf0(X0,cS2043)
| ~ spl20_13 ),
inference(avatar_component_clause,[],[f577]) ).
fof(f608,definition,
( spl20_21
<=> ! [X6,X5] :
( ~ aDivisorOf0(X5,sdtpldt0(X6,smndt0(sz00)))
| ~ aInteger0(X5)
| sz00 = X5
| isPrime0(X5)
| ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(sz00,X5))
| ~ aInteger0(X6) ) ),
introduced(definition,[new_symbols(definition,[spl20_21])],[avatar_definition]) ).
fof(f609,plain,
( ! [X6,X5] :
( ~ aDivisorOf0(X5,sdtpldt0(X6,smndt0(sz00)))
| ~ aInteger0(X5)
| sz00 = X5
| isPrime0(X5)
| ~ aElementOf0(X6,szAzrzSzezqlpdtcmdtrp0(sz00,X5))
| ~ aInteger0(X6) )
| ~ spl20_21 ),
inference(avatar_component_clause,[],[f608]) ).
fof(f610,plain,
( spl20_13
| spl20_21 ),
inference(avatar_split_clause,[],[f442,f608,f577]) ).
fof(f616,definition,
( spl20_23
<=> ! [X1] :
( isPrime0(X1)
| ~ aDivisorOf0(X1,sz10) ) ),
introduced(definition,[new_symbols(definition,[spl20_23])],[avatar_definition]) ).
fof(f617,plain,
( ! [X1] :
( ~ aDivisorOf0(X1,sz10)
| isPrime0(X1) )
| ~ spl20_23 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f619,definition,
( spl20_24
<=> aInteger0(sz10) ),
introduced(definition,[new_symbols(definition,[spl20_24])],[avatar_definition]) ).
fof(f620,plain,
( aInteger0(sz10)
| ~ spl20_24 ),
inference(avatar_component_clause,[],[f619]) ).
fof(f622,plain,
( spl20_23
| ~ spl20_24 ),
inference(avatar_split_clause,[],[f363,f619,f616]) ).
fof(f624,definition,
( spl20_25
<=> ! [X1] :
( isPrime0(X1)
| ~ aDivisorOf0(X1,smndt0(sz10)) ) ),
introduced(definition,[new_symbols(definition,[spl20_25])],[avatar_definition]) ).
fof(f625,plain,
( ! [X1] :
( ~ aDivisorOf0(X1,smndt0(sz10))
| isPrime0(X1) )
| ~ spl20_25 ),
inference(avatar_component_clause,[],[f624]) ).
fof(f627,definition,
( spl20_26
<=> aInteger0(smndt0(sz10)) ),
introduced(definition,[new_symbols(definition,[spl20_26])],[avatar_definition]) ).
fof(f628,plain,
( aInteger0(smndt0(sz10))
| ~ spl20_26 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f629,plain,
( ~ aInteger0(smndt0(sz10))
| spl20_26 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f630,plain,
( spl20_25
| ~ spl20_26 ),
inference(avatar_split_clause,[],[f362,f627,f624]) ).
fof(f631,plain,
spl20_24,
inference(avatar_split_clause,[],[f115,f619]) ).
fof(f636,plain,
( ! [X5] : aElementOf0(xn,X5)
| ~ spl20_4
| ~ spl20_13 ),
inference(backward_subsumption_resolution,[],[f507,f578]) ).
fof(f637,plain,
( $false
| ~ spl20_4
| ~ spl20_13 ),
inference(resolution,[],[f636,f578]) ).
fof(f638,plain,
( ~ spl20_4
| ~ spl20_13 ),
inference(avatar_contradiction_clause,[],[f637]) ).
fof(f639,plain,
( isPrime0(sK17)
| ~ spl20_6
| ~ spl20_12 ),
inference(resolution,[],[f550,f517]) ).
fof(f642,plain,
( xn != xn
| ~ aInteger0(sK17)
| sz00 = sK17
| ~ aInteger0(sK19)
| isPrime0(sK17)
| ~ spl20_1
| ~ spl20_2 ),
inference(superposition,[],[f494,f498]) ).
fof(f643,plain,
( ~ aInteger0(sK17)
| sz00 = sK17
| ~ aInteger0(sK19)
| isPrime0(sK17)
| ~ spl20_1
| ~ spl20_2 ),
inference(trivial_inequality_removal,[],[f642]) ).
fof(f649,plain,
( ~ aInteger0(sK17)
| ~ aInteger0(sK19)
| isPrime0(sK17)
| ~ spl20_1
| ~ spl20_2
| spl20_7 ),
inference(forward_subsumption_resolution,[],[f643,f522]) ).
fof(f650,plain,
( ~ aInteger0(sK17)
| isPrime0(sK17)
| ~ spl20_1
| ~ spl20_2
| ~ spl20_3
| spl20_7 ),
inference(forward_subsumption_resolution,[],[f649,f503]) ).
fof(f651,plain,
( ~ aInteger0(sK17)
| ~ spl20_1
| ~ spl20_2
| ~ spl20_3
| spl20_5
| spl20_7 ),
inference(forward_subsumption_resolution,[],[f650,f512]) ).
fof(f652,plain,
( ~ spl20_8
| ~ spl20_1
| ~ spl20_2
| ~ spl20_3
| spl20_5
| spl20_7 ),
inference(avatar_split_clause,[],[f651,f520,f510,f501,f496,f493,f525]) ).
fof(f653,plain,
( ~ aInteger0(sz10)
| spl20_26 ),
inference(resolution,[],[f116,f629]) ).
fof(f654,plain,
( $false
| ~ spl20_24
| spl20_26 ),
inference(forward_subsumption_resolution,[],[f653,f620]) ).
fof(f655,plain,
( ~ spl20_24
| spl20_26 ),
inference(avatar_contradiction_clause,[],[f654]) ).
fof(f670,plain,
xn = sdtpldt0(xn,sz00),
inference(resolution,[],[f122,f244]) ).
fof(f706,plain,
( sz00 = sdtasdt0(sz00,smndt0(sz10))
| ~ spl20_26 ),
inference(resolution,[],[f131,f628]) ).
fof(f819,plain,
smndt0(sz00) = sdtasdt0(sz00,smndt0(sz10)),
inference(resolution,[],[f133,f114]) ).
fof(f1091,plain,
! [X0] :
( smndt0(sz10) = X0
| sz10 = X0
| ~ aInteger0(X0)
| aInteger0(sK1(X0))
| ~ aInteger0(X0) ),
inference(resolution,[],[f149,f140]) ).
fof(f1095,plain,
! [X0] :
( ~ aInteger0(X0)
| sz10 = X0
| smndt0(sz10) = X0
| aInteger0(sK1(X0)) ),
inference(duplicate_literal_removal,[],[f1091]) ).
fof(f1101,definition,
( spl20_35
<=> sz10 = xn ),
introduced(definition,[new_symbols(definition,[spl20_35])],[avatar_definition]) ).
fof(f1102,plain,
( sz10 != xn
| spl20_35 ),
inference(avatar_component_clause,[],[f1101]) ).
fof(f1103,plain,
( sz10 = xn
| ~ spl20_35 ),
inference(avatar_component_clause,[],[f1101]) ).
fof(f1105,definition,
( spl20_36
<=> smndt0(sz10) = xn ),
introduced(definition,[new_symbols(definition,[spl20_36])],[avatar_definition]) ).
fof(f1106,plain,
( smndt0(sz10) != xn
| spl20_36 ),
inference(avatar_component_clause,[],[f1105]) ).
fof(f1107,plain,
( smndt0(sz10) = xn
| ~ spl20_36 ),
inference(avatar_component_clause,[],[f1105]) ).
fof(f1182,plain,
( ! [X0] :
( sz00 = X0
| ~ aInteger0(X0)
| isPrime0(X0)
| aElementOf0(xn,szAzrzSzezqlpdtcmdtrp0(sz00,X0)) )
| ~ spl20_4 ),
inference(resolution,[],[f435,f507]) ).
fof(f1226,plain,
( spl20_5
| ~ spl20_6
| ~ spl20_12 ),
inference(avatar_split_clause,[],[f639,f549,f515,f510]) ).
fof(f1234,plain,
( sK18 = szAzrzSzezqlpdtcmdtrp0(sz00,sK14(sK18))
| spl20_10 ),
inference(resolution,[],[f539,f434]) ).
fof(f1235,plain,
( ! [X0] :
( ~ aDivisorOf0(X0,xn)
| isPrime0(X0) )
| ~ spl20_23
| ~ spl20_35 ),
inference(superposition,[],[f617,f1103]) ).
fof(f1244,plain,
( spl20_12
| ~ spl20_23
| ~ spl20_35 ),
inference(avatar_split_clause,[],[f1235,f1101,f616,f549]) ).
fof(f1743,plain,
( ! [X0] :
( ~ aInteger0(sK1(sdtpldt0(X0,smndt0(sz00))))
| sz00 = sK1(sdtpldt0(X0,smndt0(sz00)))
| isPrime0(sK1(sdtpldt0(X0,smndt0(sz00))))
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(sdtpldt0(X0,smndt0(sz00)))))
| ~ aInteger0(X0)
| smndt0(sz10) = sdtpldt0(X0,smndt0(sz00))
| sz10 = sdtpldt0(X0,smndt0(sz00))
| ~ aInteger0(sdtpldt0(X0,smndt0(sz00))) )
| ~ spl20_21 ),
inference(resolution,[],[f609,f149]) ).
fof(f1746,plain,
( ! [X0] :
( ~ aInteger0(sK1(sdtpldt0(X0,smndt0(sz00))))
| sz00 = sK1(sdtpldt0(X0,smndt0(sz00)))
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(sdtpldt0(X0,smndt0(sz00)))))
| ~ aInteger0(X0)
| smndt0(sz10) = sdtpldt0(X0,smndt0(sz00))
| sz10 = sdtpldt0(X0,smndt0(sz00))
| ~ aInteger0(sdtpldt0(X0,smndt0(sz00))) )
| ~ spl20_21 ),
inference(forward_subsumption_resolution,[],[f1743,f364]) ).
fof(f1999,plain,
( ! [X0] :
( aElementOf0(X0,sK18)
| aElementOf0(sK18,cS2043)
| sdtpldt0(X0,smndt0(sz00)) = sdtasdt0(sK14(sK18),sK15(sK18,X0)) )
| spl20_10 ),
inference(superposition,[],[f449,f1234]) ).
fof(f2001,plain,
( ! [X0] :
( aElementOf0(X0,sK18)
| aElementOf0(sK18,cS2043)
| aInteger0(sK15(sK18,X0)) )
| spl20_10 ),
inference(superposition,[],[f448,f1234]) ).
fof(f2021,definition,
( spl20_51
<=> isPrime0(sK14(sK18)) ),
introduced(definition,[new_symbols(definition,[spl20_51])],[avatar_definition]) ).
fof(f2022,plain,
( ~ isPrime0(sK14(sK18))
| spl20_51 ),
inference(avatar_component_clause,[],[f2021]) ).
fof(f2023,plain,
( isPrime0(sK14(sK18))
| ~ spl20_51 ),
inference(avatar_component_clause,[],[f2021]) ).
fof(f2025,definition,
( spl20_52
<=> sz00 = sK14(sK18) ),
introduced(definition,[new_symbols(definition,[spl20_52])],[avatar_definition]) ).
fof(f2026,plain,
( sz00 != sK14(sK18)
| spl20_52 ),
inference(avatar_component_clause,[],[f2025]) ).
fof(f2027,plain,
( sz00 = sK14(sK18)
| ~ spl20_52 ),
inference(avatar_component_clause,[],[f2025]) ).
fof(f2029,definition,
( spl20_53
<=> aInteger0(sK14(sK18)) ),
introduced(definition,[new_symbols(definition,[spl20_53])],[avatar_definition]) ).
fof(f2030,plain,
( aInteger0(sK14(sK18))
| ~ spl20_53 ),
inference(avatar_component_clause,[],[f2029]) ).
fof(f2031,plain,
( ~ aInteger0(sK14(sK18))
| spl20_53 ),
inference(avatar_component_clause,[],[f2029]) ).
fof(f2055,plain,
( ! [X0] :
( aInteger0(sK15(sK18,X0))
| aElementOf0(X0,sK18) )
| spl20_10 ),
inference(forward_subsumption_resolution,[],[f2001,f539]) ).
fof(f2057,plain,
( ! [X0] :
( aElementOf0(X0,sK18)
| sdtpldt0(X0,smndt0(sz00)) = sdtasdt0(sK14(sK18),sK15(sK18,X0)) )
| spl20_10 ),
inference(forward_subsumption_resolution,[],[f1999,f539]) ).
fof(f2223,plain,
( aElementOf0(sK18,cS2043)
| spl20_53 ),
inference(resolution,[],[f2031,f430]) ).
fof(f2224,plain,
( $false
| spl20_10
| spl20_53 ),
inference(forward_subsumption_resolution,[],[f2223,f539]) ).
fof(f2225,plain,
( spl20_10
| spl20_53 ),
inference(avatar_contradiction_clause,[],[f2224]) ).
fof(f2227,plain,
( aElementOf0(sK18,cS2043)
| ~ spl20_51 ),
inference(resolution,[],[f2023,f432]) ).
fof(f2228,plain,
( $false
| spl20_10
| ~ spl20_51 ),
inference(forward_subsumption_resolution,[],[f2227,f539]) ).
fof(f2229,plain,
( spl20_10
| ~ spl20_51 ),
inference(avatar_contradiction_clause,[],[f2228]) ).
fof(f2294,plain,
( ! [X0] :
( ~ aDivisorOf0(X0,xn)
| isPrime0(X0) )
| ~ spl20_25
| ~ spl20_36 ),
inference(superposition,[],[f625,f1107]) ).
fof(f2396,plain,
( sz00 != sz00
| aElementOf0(sK18,cS2043)
| ~ spl20_52 ),
inference(superposition,[],[f431,f2027]) ).
fof(f2407,plain,
( aElementOf0(sK18,cS2043)
| ~ spl20_52 ),
inference(trivial_inequality_removal,[],[f2396]) ).
fof(f2418,plain,
( $false
| spl20_10
| ~ spl20_52 ),
inference(forward_subsumption_resolution,[],[f2407,f539]) ).
fof(f2419,plain,
( spl20_10
| ~ spl20_52 ),
inference(avatar_contradiction_clause,[],[f2418]) ).
fof(f14467,definition,
( spl20_408
<=> aInteger0(sK15(sK18,xn)) ),
introduced(definition,[new_symbols(definition,[spl20_408])],[avatar_definition]) ).
fof(f14468,plain,
( ~ aInteger0(sK15(sK18,xn))
| spl20_408 ),
inference(avatar_component_clause,[],[f14467]) ).
fof(f14469,plain,
( aInteger0(sK15(sK18,xn))
| ~ spl20_408 ),
inference(avatar_component_clause,[],[f14467]) ).
fof(f14821,definition,
( spl20_454
<=> sz00 = sK1(xn) ),
introduced(definition,[new_symbols(definition,[spl20_454])],[avatar_definition]) ).
fof(f14822,plain,
( sz00 != sK1(xn)
| spl20_454 ),
inference(avatar_component_clause,[],[f14821]) ).
fof(f14823,plain,
( sz00 = sK1(xn)
| ~ spl20_454 ),
inference(avatar_component_clause,[],[f14821]) ).
fof(f14825,definition,
( spl20_455
<=> isPrime0(sK1(xn)) ),
introduced(definition,[new_symbols(definition,[spl20_455])],[avatar_definition]) ).
fof(f14826,plain,
( ~ isPrime0(sK1(xn))
| spl20_455 ),
inference(avatar_component_clause,[],[f14825]) ).
fof(f14827,plain,
( isPrime0(sK1(xn))
| ~ spl20_455 ),
inference(avatar_component_clause,[],[f14825]) ).
fof(f33572,plain,
( smndt0(sz10) = xn
| sz10 = xn
| ~ aInteger0(xn)
| ~ spl20_455 ),
inference(resolution,[],[f14827,f364]) ).
fof(f49335,plain,
( aDivisorOf0(sz00,xn)
| smndt0(sz10) = xn
| sz10 = xn
| ~ aInteger0(xn)
| ~ spl20_454 ),
inference(superposition,[],[f149,f14823]) ).
fof(f65378,plain,
( aElementOf0(xn,sK18)
| spl20_10
| spl20_408 ),
inference(resolution,[],[f14468,f2055]) ).
fof(f65379,plain,
( $false
| spl20_10
| spl20_11
| spl20_408 ),
inference(forward_subsumption_resolution,[],[f65378,f545]) ).
fof(f65380,plain,
( spl20_10
| spl20_11
| spl20_408 ),
inference(avatar_contradiction_clause,[],[f65379]) ).
fof(f111888,definition,
( spl20_3331
<=> xn = sdtasdt0(sK14(sK18),sK15(sK18,xn)) ),
introduced(definition,[new_symbols(definition,[spl20_3331])],[avatar_definition]) ).
fof(f111889,plain,
( xn != sdtasdt0(sK14(sK18),sK15(sK18,xn))
| spl20_3331 ),
inference(avatar_component_clause,[],[f111888]) ).
fof(f111890,plain,
( xn = sdtasdt0(sK14(sK18),sK15(sK18,xn))
| ~ spl20_3331 ),
inference(avatar_component_clause,[],[f111888]) ).
fof(f111904,plain,
( xn != xn
| ~ aInteger0(sK14(sK18))
| sz00 = sK14(sK18)
| ~ aInteger0(sK15(sK18,xn))
| isPrime0(sK14(sK18))
| ~ spl20_1
| ~ spl20_3331 ),
inference(superposition,[],[f494,f111890]) ).
fof(f111907,plain,
( ~ aInteger0(sK14(sK18))
| sz00 = sK14(sK18)
| ~ aInteger0(sK15(sK18,xn))
| isPrime0(sK14(sK18))
| ~ spl20_1
| ~ spl20_3331 ),
inference(trivial_inequality_removal,[],[f111904]) ).
fof(f111910,plain,
( sz00 = sK14(sK18)
| ~ aInteger0(sK15(sK18,xn))
| isPrime0(sK14(sK18))
| ~ spl20_1
| ~ spl20_53
| ~ spl20_3331 ),
inference(forward_subsumption_resolution,[],[f111907,f2030]) ).
fof(f111916,plain,
( ~ aInteger0(sK15(sK18,xn))
| isPrime0(sK14(sK18))
| ~ spl20_1
| spl20_52
| ~ spl20_53
| ~ spl20_3331 ),
inference(forward_subsumption_resolution,[],[f111910,f2026]) ).
fof(f111922,plain,
( isPrime0(sK14(sK18))
| ~ spl20_1
| spl20_52
| ~ spl20_53
| ~ spl20_408
| ~ spl20_3331 ),
inference(forward_subsumption_resolution,[],[f111916,f14469]) ).
fof(f111929,plain,
( $false
| ~ spl20_1
| spl20_51
| spl20_52
| ~ spl20_53
| ~ spl20_408
| ~ spl20_3331 ),
inference(forward_subsumption_resolution,[],[f111922,f2022]) ).
fof(f111930,plain,
( ~ spl20_1
| spl20_51
| spl20_52
| ~ spl20_53
| ~ spl20_408
| ~ spl20_3331 ),
inference(avatar_contradiction_clause,[],[f111929]) ).
fof(f112253,plain,
( smndt0(sz10) = xn
| sz10 = xn
| ~ spl20_455 ),
inference(forward_subsumption_resolution,[],[f33572,f244]) ).
fof(f113079,plain,
( spl20_35
| spl20_36
| ~ spl20_455 ),
inference(avatar_split_clause,[],[f112253,f14825,f1105,f1101]) ).
fof(f113336,plain,
( spl20_12
| ~ spl20_25
| ~ spl20_36 ),
inference(avatar_split_clause,[],[f2294,f1105,f624,f549]) ).
fof(f115882,definition,
( spl20_3559
<=> ! [X0] :
( aElementOf0(xn,szAzrzSzezqlpdtcmdtrp0(sz00,X0))
| isPrime0(X0)
| ~ aInteger0(X0)
| sz00 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl20_3559])],[avatar_definition]) ).
fof(f115883,plain,
( ! [X0] :
( aElementOf0(xn,szAzrzSzezqlpdtcmdtrp0(sz00,X0))
| isPrime0(X0)
| ~ aInteger0(X0)
| sz00 = X0 )
| ~ spl20_3559 ),
inference(avatar_component_clause,[],[f115882]) ).
fof(f116117,plain,
( spl20_3559
| ~ spl20_4 ),
inference(avatar_split_clause,[],[f1182,f506,f115882]) ).
fof(f116465,plain,
( sz00 = smndt0(sz00)
| ~ spl20_26 ),
inference(forward_demodulation,[],[f819,f706]) ).
fof(f117288,plain,
( sz10 = xn
| smndt0(sz10) = xn
| aInteger0(sK1(xn)) ),
inference(resolution,[],[f1095,f244]) ).
fof(f117492,plain,
( smndt0(sz10) = xn
| aInteger0(sK1(xn))
| spl20_35 ),
inference(forward_subsumption_resolution,[],[f117288,f1102]) ).
fof(f117628,plain,
( aInteger0(sK1(xn))
| spl20_35
| spl20_36 ),
inference(forward_subsumption_resolution,[],[f117492,f1106]) ).
fof(f121549,plain,
( smndt0(sz10) = xn
| sz10 = xn
| ~ aInteger0(xn)
| ~ spl20_454 ),
inference(forward_subsumption_resolution,[],[f49335,f329]) ).
fof(f121580,plain,
( sz10 = xn
| ~ aInteger0(xn)
| spl20_36
| ~ spl20_454 ),
inference(forward_subsumption_resolution,[],[f121549,f1106]) ).
fof(f121611,plain,
( ~ aInteger0(xn)
| spl20_35
| spl20_36
| ~ spl20_454 ),
inference(forward_subsumption_resolution,[],[f121580,f1102]) ).
fof(f121618,plain,
( $false
| spl20_35
| spl20_36
| ~ spl20_454 ),
inference(forward_subsumption_resolution,[],[f121611,f244]) ).
fof(f121619,plain,
( spl20_35
| spl20_36
| ~ spl20_454 ),
inference(avatar_contradiction_clause,[],[f121618]) ).
fof(f121878,plain,
( ! [X0] :
( sz00 = sK1(sdtpldt0(X0,smndt0(sz00)))
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(sdtpldt0(X0,smndt0(sz00)))))
| ~ aInteger0(X0)
| smndt0(sz10) = sdtpldt0(X0,smndt0(sz00))
| sz10 = sdtpldt0(X0,smndt0(sz00))
| ~ aInteger0(sdtpldt0(X0,smndt0(sz00))) )
| ~ spl20_21 ),
inference(forward_subsumption_resolution,[],[f1746,f1095]) ).
fof(f121879,plain,
( ! [X0] :
( sz00 = sK1(sdtpldt0(X0,sz00))
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(sdtpldt0(X0,smndt0(sz00)))))
| ~ aInteger0(X0)
| smndt0(sz10) = sdtpldt0(X0,smndt0(sz00))
| sz10 = sdtpldt0(X0,smndt0(sz00))
| ~ aInteger0(sdtpldt0(X0,smndt0(sz00))) )
| ~ spl20_21
| ~ spl20_26 ),
inference(forward_demodulation,[],[f121878,f116465]) ).
fof(f121880,plain,
( ! [X0] :
( ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(sdtpldt0(X0,sz00))))
| sz00 = sK1(sdtpldt0(X0,sz00))
| ~ aInteger0(X0)
| smndt0(sz10) = sdtpldt0(X0,smndt0(sz00))
| sz10 = sdtpldt0(X0,smndt0(sz00))
| ~ aInteger0(sdtpldt0(X0,smndt0(sz00))) )
| ~ spl20_21
| ~ spl20_26 ),
inference(forward_demodulation,[],[f121879,f116465]) ).
fof(f121881,plain,
( ! [X0] :
( sdtpldt0(X0,sz00) = smndt0(sz10)
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(sdtpldt0(X0,sz00))))
| sz00 = sK1(sdtpldt0(X0,sz00))
| ~ aInteger0(X0)
| sz10 = sdtpldt0(X0,smndt0(sz00))
| ~ aInteger0(sdtpldt0(X0,smndt0(sz00))) )
| ~ spl20_21
| ~ spl20_26 ),
inference(forward_demodulation,[],[f121880,f116465]) ).
fof(f121882,plain,
( ! [X0] :
( sz10 = sdtpldt0(X0,sz00)
| sdtpldt0(X0,sz00) = smndt0(sz10)
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(sdtpldt0(X0,sz00))))
| sz00 = sK1(sdtpldt0(X0,sz00))
| ~ aInteger0(X0)
| ~ aInteger0(sdtpldt0(X0,smndt0(sz00))) )
| ~ spl20_21
| ~ spl20_26 ),
inference(forward_demodulation,[],[f121881,f116465]) ).
fof(f121883,plain,
( ! [X0] :
( ~ aInteger0(sdtpldt0(X0,sz00))
| sz10 = sdtpldt0(X0,sz00)
| sdtpldt0(X0,sz00) = smndt0(sz10)
| ~ aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(sdtpldt0(X0,sz00))))
| sz00 = sK1(sdtpldt0(X0,sz00))
| ~ aInteger0(X0) )
| ~ spl20_21
| ~ spl20_26 ),
inference(forward_demodulation,[],[f121882,f116465]) ).
fof(f121887,plain,
( ~ aInteger0(xn)
| sz10 = xn
| smndt0(sz10) = xn
| ~ aElementOf0(xn,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(xn)))
| sz00 = sK1(xn)
| ~ aInteger0(xn)
| ~ spl20_21
| ~ spl20_26 ),
inference(superposition,[],[f121883,f670]) ).
fof(f121896,plain,
( ~ aInteger0(xn)
| sz10 = xn
| smndt0(sz10) = xn
| ~ aElementOf0(xn,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(xn)))
| sz00 = sK1(xn)
| ~ spl20_21
| ~ spl20_26 ),
inference(duplicate_literal_removal,[],[f121887]) ).
fof(f121902,plain,
( sz10 = xn
| smndt0(sz10) = xn
| ~ aElementOf0(xn,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(xn)))
| sz00 = sK1(xn)
| ~ spl20_21
| ~ spl20_26 ),
inference(forward_subsumption_resolution,[],[f121896,f244]) ).
fof(f121908,plain,
( smndt0(sz10) = xn
| ~ aElementOf0(xn,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(xn)))
| sz00 = sK1(xn)
| ~ spl20_21
| ~ spl20_26
| spl20_35 ),
inference(forward_subsumption_resolution,[],[f121902,f1102]) ).
fof(f121921,plain,
( ~ aElementOf0(xn,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(xn)))
| sz00 = sK1(xn)
| ~ spl20_21
| ~ spl20_26
| spl20_35
| spl20_36 ),
inference(forward_subsumption_resolution,[],[f121908,f1106]) ).
fof(f121924,definition,
( spl20_3828
<=> aElementOf0(xn,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(xn))) ),
introduced(definition,[new_symbols(definition,[spl20_3828])],[avatar_definition]) ).
fof(f121926,plain,
( ~ aElementOf0(xn,szAzrzSzezqlpdtcmdtrp0(sz00,sK1(xn)))
| spl20_3828 ),
inference(avatar_component_clause,[],[f121924]) ).
fof(f121927,plain,
( spl20_454
| ~ spl20_3828
| ~ spl20_21
| ~ spl20_26
| spl20_35
| spl20_36 ),
inference(avatar_split_clause,[],[f121921,f1105,f1101,f627,f608,f121924,f14821]) ).
fof(f142712,plain,
( isPrime0(sK1(xn))
| ~ aInteger0(sK1(xn))
| sz00 = sK1(xn)
| ~ spl20_3559
| spl20_3828 ),
inference(resolution,[],[f115883,f121926]) ).
fof(f142721,plain,
( ~ aInteger0(sK1(xn))
| sz00 = sK1(xn)
| spl20_455
| ~ spl20_3559
| spl20_3828 ),
inference(forward_subsumption_resolution,[],[f142712,f14826]) ).
fof(f142723,plain,
( sz00 = sK1(xn)
| spl20_35
| spl20_36
| spl20_455
| ~ spl20_3559
| spl20_3828 ),
inference(forward_subsumption_resolution,[],[f142721,f117628]) ).
fof(f142724,plain,
( $false
| spl20_35
| spl20_36
| spl20_454
| spl20_455
| ~ spl20_3559
| spl20_3828 ),
inference(forward_subsumption_resolution,[],[f142723,f14822]) ).
fof(f142725,plain,
( spl20_35
| spl20_36
| spl20_454
| spl20_455
| ~ spl20_3559
| spl20_3828 ),
inference(avatar_contradiction_clause,[],[f142724]) ).
fof(f169949,plain,
( ! [X0] :
( aElementOf0(X0,sK18)
| sdtpldt0(X0,sz00) = sdtasdt0(sK14(sK18),sK15(sK18,X0)) )
| spl20_10
| ~ spl20_26 ),
inference(forward_demodulation,[],[f2057,f116465]) ).
fof(f169987,plain,
( sdtpldt0(xn,sz00) = sdtasdt0(sK14(sK18),sK15(sK18,xn))
| spl20_10
| spl20_11
| ~ spl20_26 ),
inference(resolution,[],[f169949,f545]) ).
fof(f170013,plain,
( xn = sdtasdt0(sK14(sK18),sK15(sK18,xn))
| spl20_10
| spl20_11
| ~ spl20_26 ),
inference(forward_demodulation,[],[f169987,f670]) ).
fof(f170017,plain,
( $false
| spl20_10
| spl20_11
| ~ spl20_26
| spl20_3331 ),
inference(forward_subsumption_resolution,[],[f170013,f111889]) ).
fof(f170018,plain,
( spl20_10
| spl20_11
| ~ spl20_26
| spl20_3331 ),
inference(avatar_contradiction_clause,[],[f170017]) ).
cnf(s3,plain,
( spl20_1
| spl20_4 ),
inference(sat_conversion,[],[f508]) ).
cnf(s4,plain,
( spl20_1
| ~ spl20_5 ),
inference(sat_conversion,[],[f513]) ).
cnf(s5,plain,
( spl20_1
| spl20_6 ),
inference(sat_conversion,[],[f518]) ).
cnf(s11,plain,
( spl20_2
| ~ spl20_10 ),
inference(sat_conversion,[],[f540]) ).
cnf(s12,plain,
( spl20_3
| ~ spl20_10 ),
inference(sat_conversion,[],[f541]) ).
cnf(s13,plain,
( spl20_2
| ~ spl20_11 ),
inference(sat_conversion,[],[f546]) ).
cnf(s14,plain,
( spl20_3
| ~ spl20_11 ),
inference(sat_conversion,[],[f547]) ).
cnf(s25,plain,
( spl20_8
| ~ spl20_11 ),
inference(sat_conversion,[],[f561]) ).
cnf(s26,plain,
( spl20_8
| ~ spl20_10 ),
inference(sat_conversion,[],[f562]) ).
cnf(s27,plain,
( ~ spl20_7
| ~ spl20_11 ),
inference(sat_conversion,[],[f563]) ).
cnf(s28,plain,
( ~ spl20_7
| ~ spl20_10 ),
inference(sat_conversion,[],[f564]) ).
cnf(s31,plain,
( ~ spl20_5
| ~ spl20_11 ),
inference(sat_conversion,[],[f567]) ).
cnf(s32,plain,
( ~ spl20_5
| ~ spl20_10 ),
inference(sat_conversion,[],[f568]) ).
cnf(s47,plain,
( spl20_13
| spl20_21 ),
inference(sat_conversion,[],[f610]) ).
cnf(s49,plain,
( spl20_23
| ~ spl20_24 ),
inference(sat_conversion,[],[f622]) ).
cnf(s50,plain,
( spl20_25
| ~ spl20_26 ),
inference(sat_conversion,[],[f630]) ).
cnf(s51,plain,
spl20_24,
inference(sat_conversion,[],[f631]) ).
cnf(s54,plain,
( ~ spl20_4
| ~ spl20_13 ),
inference(sat_conversion,[],[f638]) ).
cnf(s57,plain,
( ~ spl20_1
| ~ spl20_2
| ~ spl20_3
| spl20_5
| spl20_7
| ~ spl20_8 ),
inference(sat_conversion,[],[f652]) ).
cnf(s58,plain,
( ~ spl20_24
| spl20_26 ),
inference(sat_conversion,[],[f655]) ).
cnf(s71,plain,
( spl20_5
| ~ spl20_6
| ~ spl20_12 ),
inference(sat_conversion,[],[f1226]) ).
cnf(s79,plain,
( spl20_12
| ~ spl20_23
| ~ spl20_35 ),
inference(sat_conversion,[],[f1244]) ).
cnf(s132,plain,
( spl20_10
| spl20_53 ),
inference(sat_conversion,[],[f2225]) ).
cnf(s133,plain,
( spl20_10
| ~ spl20_51 ),
inference(sat_conversion,[],[f2229]) ).
cnf(s138,plain,
( spl20_10
| ~ spl20_52 ),
inference(sat_conversion,[],[f2419]) ).
cnf(s3633,plain,
( spl20_10
| spl20_11
| spl20_408 ),
inference(sat_conversion,[],[f65380]) ).
cnf(s5115,plain,
( ~ spl20_1
| spl20_51
| spl20_52
| ~ spl20_53
| ~ spl20_408
| ~ spl20_3331 ),
inference(sat_conversion,[],[f111930]) ).
cnf(s5295,plain,
( spl20_35
| spl20_36
| ~ spl20_455 ),
inference(sat_conversion,[],[f113079]) ).
cnf(s5343,plain,
( spl20_12
| ~ spl20_25
| ~ spl20_36 ),
inference(sat_conversion,[],[f113336]) ).
cnf(s5613,plain,
( ~ spl20_4
| spl20_3559 ),
inference(sat_conversion,[],[f116117]) ).
cnf(s6099,plain,
( spl20_35
| spl20_36
| ~ spl20_454 ),
inference(sat_conversion,[],[f121619]) ).
cnf(s6150,plain,
( ~ spl20_21
| ~ spl20_26
| spl20_35
| spl20_36
| spl20_454
| ~ spl20_3828 ),
inference(sat_conversion,[],[f121927]) ).
cnf(s7519,plain,
( spl20_35
| spl20_36
| spl20_454
| spl20_455
| ~ spl20_3559
| spl20_3828 ),
inference(sat_conversion,[],[f142725]) ).
cnf(s8921,plain,
( spl20_10
| spl20_11
| ~ spl20_26
| spl20_3331 ),
inference(sat_conversion,[],[f170018]) ).
cnf(s8923,plain,
spl20_26,
inference(rat,[],[s58,s51]) ).
cnf(s8925,plain,
spl20_25,
inference(rat,[],[s50,s8923]) ).
cnf(s8926,plain,
spl20_23,
inference(rat,[],[s49,s51]) ).
cnf(s8927,plain,
spl20_1,
inference(rat,[],[s7519,s6150,s5295,s6099,s47,s79,s5343,s54,s5613,s71,s3,s4,s5,s8923,s8926,s8925]) ).
cnf(s8928,plain,
( spl20_11
| spl20_10 ),
inference(rat,[],[s5115,s132,s133,s138,s3633,s8921,s8923,s8927]) ).
cnf(s8929,plain,
spl20_2,
inference(rat,[],[s8928,s11,s13]) ).
cnf(s8930,plain,
~ spl20_11,
inference(rat,[],[s57,s14,s25,s27,s31,s8927,s8929]) ).
cnf(s8931,plain,
spl20_10,
inference(rat,[],[s8928,s8930]) ).
cnf(s8933,plain,
~ spl20_5,
inference(rat,[],[s32,s8931]) ).
cnf(s8935,plain,
~ spl20_7,
inference(rat,[],[s28,s8931]) ).
cnf(s8936,plain,
spl20_8,
inference(rat,[],[s26,s8931]) ).
cnf(s8938,plain,
spl20_3,
inference(rat,[],[s12,s8931]) ).
cnf(s8943,plain,
$false,
inference(rat,[],[s57,s8936,s8938,s8929,s8927,s8933,s8935]) ).
fof(f170022,plain,
$false,
inference(avatar_sat_refutation,[],[s8943]) ).
%------------------------------------------------------------------------------
%----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 SAT
% 0.11/0.38 % Computer : n008.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 19:58:24 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.75/2.55 % (1565441)Will run a generic schedule for satisfiability detection.
% 14.75/2.55 % (1565452)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3561807870:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.75/2.55 % (1565447)% WARNING: option uhcvi not known.
% 14.75/2.55 % (1565448)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=741097152:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.75/2.55 % (1565446)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1196409413_2999 on theBenchmark for (2999ds/0Mi)
% 14.75/2.55 % (1565447)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4013359082:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.75/2.55 % (1565449)dis+10_1_sil=32000:sp=arity:random_seed=1865629935:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.75/2.55 % (1565450)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=196568290:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.75/2.55 % (1565451)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=592910459:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.75/2.55 % TRYING [1]
% 14.75/2.55 % TRYING [2]
% 14.75/2.55 % TRYING [3]
% 14.75/2.55 % TRYING [4]
% 14.75/2.55 % (1565452)Instruction limit reached!
% 14.75/2.55 % (1565452)------------------------------
% 14.75/2.55 % (1565452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.75/2.55 % (1565452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.75/2.55 % (1565452)CaDiCaL version: 2.1.3
% 14.75/2.55 % (1565452)Termination reason: Instruction limit
% 14.75/2.55 % (1565452)Termination phase: Saturation
% 14.75/2.55 % (1565452)Time elapsed: 0.056 s
% 14.75/2.55 % (1565452)Peak memory usage: 14 MB
% 14.75/2.55 % (1565452)Instructions burned: 161 (million)
% 14.75/2.55 % (1565460)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3239015316:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.75/2.55 % TRYING [1]
% 14.75/2.55 % (1565449)Instruction limit reached!
% 14.75/2.55 % (1565449)------------------------------
% 14.75/2.55 % (1565449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.75/2.55 % (1565449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.75/2.55 % (1565449)CaDiCaL version: 2.1.3
% 14.75/2.55 % (1565449)Termination reason: Instruction limit
% 14.75/2.55 % (1565449)Termination phase: Saturation
% 14.75/2.55 % (1565449)Time elapsed: 0.067 s
% 14.75/2.55 % (1565449)Peak memory usage: 13 MB
% 14.75/2.55 % (1565449)Instructions burned: 103 (million)
% 14.75/2.55 % TRYING [2]
% 14.75/2.55 % TRYING [3]
% 14.75/2.55 % (1565450)Instruction limit reached!
% 14.75/2.55 % (1565450)------------------------------
% 14.75/2.55 % (1565450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.75/2.55 % (1565450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.75/2.55 % (1565450)CaDiCaL version: 2.1.3
% 14.75/2.55 % (1565450)Termination reason: Instruction limit
% 14.75/2.55 % (1565450)Termination phase: Saturation
% 14.75/2.55 % (1565450)Time elapsed: 0.071 s
% 14.75/2.55 % (1565450)Peak memory usage: 13 MB
% 14.75/2.55 % (1565450)Instructions burned: 117 (million)
% 14.75/2.55 % (1565451)Instruction limit reached!
% 14.75/2.55 % (1565451)------------------------------
% 14.75/2.55 % (1565451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.75/2.55 % (1565451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.75/2.55 % (1565451)CaDiCaL version: 2.1.3
% 14.75/2.55 % (1565451)Termination reason: Instruction limit
% 14.75/2.55 % (1565451)Termination phase: Saturation
% 14.75/2.55 % (1565451)Time elapsed: 0.074 s
% 14.75/2.55 % (1565451)Peak memory usage: 13 MB
% 14.75/2.55 % (1565451)Instructions burned: 131 (million)
% 14.75/2.55 % TRYING [4]
% 14.75/2.55 % (1565462)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4131802901:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.75/2.55 % TRYING [5]
% 14.75/2.55 % (1565463)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3667209676:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.75/2.55 % (1565464)ott-21_1_sil=16000:fs=off:random_seed=1315104812:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.75/2.55 % TRYING [5]
% 14.75/2.55 % (1565462)Instruction limit reached!
% 14.75/2.55 % (1565462)------------------------------
% 14.75/2.55 % (1565462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565462)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565462)Termination reason: Instruction limit
% 19.38/5.22 % (1565462)Termination phase: Saturation
% 19.38/5.22 % (1565462)Time elapsed: 0.075 s
% 19.38/5.22 % (1565462)Peak memory usage: 13 MB
% 19.38/5.22 % (1565462)Instructions burned: 132 (million)
% 19.38/5.22 % (1565468)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3222447930:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 19.38/5.22 % TRYING [6]
% 19.38/5.22 % (1565464)Instruction limit reached!
% 19.38/5.22 % (1565464)------------------------------
% 19.38/5.22 % (1565464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565464)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565464)Termination reason: Instruction limit
% 19.38/5.22 % (1565464)Termination phase: Saturation
% 19.38/5.22 % (1565464)Time elapsed: 0.092 s
% 19.38/5.22 % (1565464)Peak memory usage: 13 MB
% 19.38/5.22 % (1565464)Instructions burned: 180 (million)
% 19.38/5.22 % (1565470)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3292949165:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 19.38/5.22 % (1565460)Instruction limit reached!
% 19.38/5.22 % (1565460)------------------------------
% 19.38/5.22 % (1565460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565460)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565460)Termination reason: Instruction limit
% 19.38/5.22 % (1565460)Termination phase: Finite model building constraint generation
% 19.38/5.22 % (1565460)Time elapsed: 0.151 s
% 19.38/5.22 % (1565460)Peak memory usage: 27 MB
% 19.38/5.22 % (1565460)Instructions burned: 715 (million)
% 19.38/5.22 % TRYING [1]
% 19.38/5.22 % TRYING [2]
% 19.38/5.22 % (1565472)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1994743227:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 19.38/5.22 % TRYING [6]
% 19.38/5.22 % TRYING [3]
% 19.38/5.22 % TRYING [4]
% 19.38/5.22 % (1565463)Instruction limit reached!
% 19.38/5.22 % (1565463)------------------------------
% 19.38/5.22 % (1565463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565463)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565463)Termination reason: Instruction limit
% 19.38/5.22 % (1565463)Termination phase: Saturation
% 19.38/5.22 % (1565463)Time elapsed: 0.324 s
% 19.38/5.22 % (1565463)Peak memory usage: 16 MB
% 19.38/5.22 % (1565463)Instructions burned: 685 (million)
% 19.38/5.22 % (1565474)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4052814907:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 19.38/5.22 % TRYING [5]
% 19.38/5.22 % (1565468)Instruction limit reached!
% 19.38/5.22 % (1565468)------------------------------
% 19.38/5.22 % (1565468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565468)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565468)Termination reason: Instruction limit
% 19.38/5.22 % (1565468)Termination phase: Saturation
% 19.38/5.22 % (1565468)Time elapsed: 0.328 s
% 19.38/5.22 % (1565468)Peak memory usage: 14 MB
% 19.38/5.22 % (1565468)Instructions burned: 478 (million)
% 19.38/5.22 % (1565476)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2654378732:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 19.38/5.22 % (1565470)Instruction limit reached!
% 19.38/5.22 % (1565470)------------------------------
% 19.38/5.22 % (1565470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565470)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565470)Termination reason: Instruction limit
% 19.38/5.22 % (1565470)Termination phase: Finite model building SAT solving
% 19.38/5.22 % (1565470)Time elapsed: 0.346 s
% 19.38/5.22 % (1565470)Peak memory usage: 25 MB
% 19.38/5.22 % (1565470)Instructions burned: 865 (million)
% 19.38/5.22 % (1565472)Instruction limit reached!
% 19.38/5.22 % (1565472)------------------------------
% 19.38/5.22 % (1565472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565472)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565472)Termination reason: Instruction limit
% 19.38/5.22 % (1565472)Termination phase: Saturation
% 19.38/5.22 % (1565472)Time elapsed: 0.341 s
% 19.38/5.22 % (1565472)Peak memory usage: 22 MB
% 19.38/5.22 % (1565472)Instructions burned: 1182 (million)
% 19.38/5.22 % (1565478)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=422443691:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 19.38/5.22 % (1565479)fmb+10_1_sil=64000:random_seed=2281604494:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 19.38/5.22 % TRYING [1]
% 19.38/5.22 % TRYING [2]
% 19.38/5.22 % TRYING [3]
% 19.38/5.22 % TRYING [4]
% 19.38/5.22 % TRYING [7]
% 19.38/5.22 % TRYING [5]
% 19.38/5.22 % TRYING [14]
% 19.38/5.22 % (1565474)Instruction limit reached!
% 19.38/5.22 % (1565474)------------------------------
% 19.38/5.22 % (1565474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565474)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565474)Termination reason: Instruction limit
% 19.38/5.22 % (1565474)Termination phase: Finite model building constraint generation
% 19.38/5.22 % (1565474)Time elapsed: 0.365 s
% 19.38/5.22 % (1565474)Peak memory usage: 87 MB
% 19.38/5.22 % (1565474)Instructions burned: 891 (million)
% 19.38/5.22 % TRYING [6]
% 19.38/5.22 % (1565483)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2754014213:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 19.38/5.22 % TRYING [20]
% 19.38/5.22 % (1565476)Instruction limit reached!
% 19.38/5.22 % (1565476)------------------------------
% 19.38/5.22 % (1565476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565476)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565476)Termination reason: Instruction limit
% 19.38/5.22 % (1565476)Termination phase: Saturation
% 19.38/5.22 % (1565476)Time elapsed: 0.373 s
% 19.38/5.22 % (1565476)Peak memory usage: 23 MB
% 19.38/5.22 % (1565476)Instructions burned: 692 (million)
% 19.38/5.22 % (1565485)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1257241672:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 19.38/5.22 % TRYING [8]
% 19.38/5.22 % (1565478)Instruction limit reached!
% 19.38/5.22 % (1565478)------------------------------
% 19.38/5.22 % (1565478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565478)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565478)Termination reason: Instruction limit
% 19.38/5.22 % (1565478)Termination phase: Saturation
% 19.38/5.22 % (1565478)Time elapsed: 0.508 s
% 19.38/5.22 % (1565478)Peak memory usage: 19 MB
% 19.38/5.22 % (1565478)Instructions burned: 880 (million)
% 19.38/5.22 % (1565487)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=889752091:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 19.38/5.22 % TRYING [7]
% 19.38/5.22 % (1565485)Instruction limit reached!
% 19.38/5.22 % (1565485)------------------------------
% 19.38/5.22 % (1565485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565485)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565485)Termination reason: Instruction limit
% 19.38/5.22 % (1565485)Termination phase: Finite model building constraint generation
% 19.38/5.22 % (1565485)Time elapsed: 0.346 s
% 19.38/5.22 % (1565485)Peak memory usage: 73 MB
% 19.38/5.22 % (1565485)Instructions burned: 922 (million)
% 19.38/5.22 % (1565489)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3550241973:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 19.38/5.22 % (1565489)Instruction limit reached!
% 19.38/5.22 % (1565489)------------------------------
% 19.38/5.22 % (1565489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565489)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565489)Termination reason: Instruction limit
% 19.38/5.22 % (1565489)Termination phase: Saturation
% 19.38/5.22 % (1565489)Time elapsed: 0.769 s
% 19.38/5.22 % (1565489)Peak memory usage: 34 MB
% 19.38/5.22 % (1565489)Instructions burned: 1473 (million)
% 19.38/5.22 % (1565491)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2820700010:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 19.38/5.22 % TRYING [77]
% 19.38/5.22 % TRYING [8]
% 19.38/5.22 % TRYING [8]
% 19.38/5.22 % (1565487)Instruction limit reached!
% 19.38/5.22 % (1565487)------------------------------
% 19.38/5.22 % (1565487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565487)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565487)Termination reason: Instruction limit
% 19.38/5.22 % (1565487)Termination phase: Saturation
% 19.38/5.22 % (1565487)Time elapsed: 2.652 s
% 19.38/5.22 % (1565487)Peak memory usage: 36 MB
% 19.38/5.22 % (1565487)Instructions burned: 5132 (million)
% 19.38/5.22 % (1565493)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=85384339:fmbsr=2.30978:i=2174_2962 on theBenchmark for (2962ds/2174Mi)
% 19.38/5.22 % TRYING [16]
% 19.38/5.22 % (1565483)Instruction limit reached!
% 19.38/5.22 % (1565483)------------------------------
% 19.38/5.22 % (1565483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565483)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565483)Termination reason: Instruction limit
% 19.38/5.22 % (1565483)Termination phase: Finite model building constraint generation
% 19.38/5.22 % (1565483)Time elapsed: 3.347 s
% 19.38/5.22 % (1565483)Peak memory usage: 570 MB
% 19.38/5.22 % (1565483)Instructions burned: 9518 (million)
% 19.38/5.22 % (1565495)ott-2_1_sil=16000:newcnf=on:random_seed=3370032290:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 19.38/5.22 % (1565491)Instruction limit reached!
% 19.38/5.22 % (1565491)------------------------------
% 19.38/5.22 % (1565491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565491)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565491)Termination reason: Instruction limit
% 19.38/5.22 % (1565491)Termination phase: Finite model building constraint generation
% 19.38/5.22 % (1565491)Time elapsed: 2.237 s
% 19.38/5.22 % (1565491)Peak memory usage: 444 MB
% 19.38/5.22 % (1565491)Instructions burned: 6326 (million)
% 19.38/5.22 % (1565497)ott+10_1_sil=32000:tgt=ground:random_seed=1397234005:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 19.38/5.22 % (1565493)Instruction limit reached!
% 19.38/5.22 % (1565493)------------------------------
% 19.38/5.22 % (1565493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565493)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565493)Termination reason: Instruction limit
% 19.38/5.22 % (1565493)Termination phase: Finite model building constraint generation
% 19.38/5.22 % (1565493)Time elapsed: 0.765 s
% 19.38/5.22 % (1565493)Peak memory usage: 137 MB
% 19.38/5.22 % (1565493)Instructions burned: 2184 (million)
% 19.38/5.22 % (1565499)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3042658922:i=54282_2954 on theBenchmark for (2954ds/54282Mi)
% 19.38/5.22 % TRYING [1]
% 19.38/5.22 % TRYING [2]
% 19.38/5.22 % TRYING [3]
% 19.38/5.22 % TRYING [4]
% 19.38/5.22 % TRYING [5]
% 19.38/5.22 % (1565447) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1565441-1565447"...
% 19.38/5.22 % (1565447)...printing done.
% 19.38/5.22 % (1565447)Refutation found. Thanks to Tanya!
% 19.38/5.22 % SZS status Theorem for theBenchmark
% 19.38/5.22 % SZS output start Proof for theBenchmark
% See solution above
% 19.38/5.22 % (1565447)------------------------------
% 19.38/5.22 % (1565447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.38/5.22 % (1565447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/5.22 % (1565447)CaDiCaL version: 2.1.3
% 19.38/5.22 % (1565447)Termination reason: Refutation
% 19.38/5.22 % (1565447)Time elapsed: 4.734 s
% 19.38/5.22 % (1565447)Peak memory usage: 74 MB
% 19.38/5.22 % (1565447)Instructions burned: 8385 (million)
% 19.38/5.22 % (1565441)Success in time 4.801 s
% 19.38/5.22 % Vampire exiting
%------------------------------------------------------------------------------