%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM510+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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:36 PM UTC 2026
% Result : Theorem 4.31s 1.15s
% Output : Refutation 4.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 38
% Syntax : Number of formulae : 228 ( 47 unt; 17 def)
% Number of atoms : 803 ( 199 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 1002 ( 427 ~; 428 |; 101 &)
% ( 23 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 18 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 157 ( 0 sgn 144 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsC) ).
fof(f3,axiom,
( aNaturalNumber0(sz10)
& sz10 != sz00 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsC_01) ).
fof(f4,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> aNaturalNumber0(sdtpldt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsB) ).
fof(f5,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> aNaturalNumber0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsB_02) ).
fof(f8,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_AddZero) ).
fof(f11,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( sdtasdt0(X0,sz10) = X0
& X0 = sdtasdt0(sz10,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_MulUnit) ).
fof(f12,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_MulZero) ).
fof(f15,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( X0 != sz00
=> ! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( sdtasdt0(X0,X1) = sdtasdt0(X0,X2)
| sdtasdt0(X1,X0) = sdtasdt0(X2,X0) )
=> X1 = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulCanc) ).
fof(f18,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( sdtlseqdt0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& sdtpldt0(X0,X2) = X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefLE) ).
fof(f20,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> sdtlseqdt0(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLERefl) ).
fof(f22,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X1,X2) )
=> sdtlseqdt0(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLETran) ).
fof(f25,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( X0 != sz00
& X1 != X2
& sdtlseqdt0(X1,X2) )
=> ( sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
& sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
& sdtlseqdt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMonMul) ).
fof(f27,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( X0 != sz00
=> sdtlseqdt0(X1,sdtasdt0(X1,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMonMul2) ).
fof(f31,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( ( X0 != sz00
& doDivides0(X0,X1) )
=> ! [X2] :
( X2 = sdtsldt0(X1,X0)
<=> ( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefQuot) ).
fof(f39,axiom,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm)
& aNaturalNumber0(xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1837) ).
fof(f42,axiom,
~ ( ? [X0] :
( aNaturalNumber0(X0)
& sdtpldt0(xp,X0) = xn )
| sdtlseqdt0(xp,xn) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1870) ).
fof(f45,axiom,
( aNaturalNumber0(xk)
& sdtasdt0(xn,xm) = sdtasdt0(xp,xk)
& xk = sdtsldt0(sdtasdt0(xn,xm),xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2306) ).
fof(f46,axiom,
~ ( xk = sz00
| xk = sz10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2315) ).
fof(f48,axiom,
( aNaturalNumber0(xr)
& ? [X0] :
( aNaturalNumber0(X0)
& xk = sdtasdt0(xr,X0) )
& doDivides0(xr,xk)
& xr != sz00
& xr != sz10
& ! [X0] :
( ( aNaturalNumber0(X0)
& ( ? [X1] :
( aNaturalNumber0(X1)
& xr = sdtasdt0(X0,X1) )
| doDivides0(X0,xr) ) )
=> ( X0 = sz10
| X0 = xr ) )
& isPrime0(xr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2342) ).
fof(f52,axiom,
( ? [X0] :
( aNaturalNumber0(X0)
& xn = sdtasdt0(xr,X0) )
& doDivides0(xr,xn) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2487) ).
fof(f53,conjecture,
( ~ ( aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& sdtsldt0(xn,xr) = xn )
& ( ( aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr)) )
=> ( ? [X0] :
( aNaturalNumber0(X0)
& sdtpldt0(sdtsldt0(xn,xr),X0) = xn )
| sdtlseqdt0(sdtsldt0(xn,xr),xn) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f54,negated_conjecture,
~ ( ~ ( aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& sdtsldt0(xn,xr) = xn )
& ( ( aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr)) )
=> ( ? [X0] :
( aNaturalNumber0(X0)
& sdtpldt0(sdtsldt0(xn,xr),X0) = xn )
| sdtlseqdt0(sdtsldt0(xn,xr),xn) ) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f58,plain,
( aNaturalNumber0(xr)
& ? [X0] :
( aNaturalNumber0(X0)
& xk = sdtasdt0(xr,X0) )
& doDivides0(xr,xk)
& xr != sz00
& xr != sz10
& ! [X1] :
( ( aNaturalNumber0(X1)
& ( ? [X2] :
( aNaturalNumber0(X2)
& sdtasdt0(X1,X2) = xr )
| doDivides0(X1,xr) ) )
=> ( sz10 = X1
| xr = X1 ) )
& isPrime0(xr) ),
inference(rectify,[],[f48]) ).
fof(f62,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f4]) ).
fof(f63,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f62]) ).
fof(f64,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f65,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f64]) ).
fof(f70,plain,
! [X0] :
( ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) )
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f75,plain,
! [X0] :
( ( sdtasdt0(X0,sz10) = X0
& X0 = sdtasdt0(sz10,X0) )
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f76,plain,
! [X0] :
( ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) )
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f81,plain,
! [X0] :
( ! [X1,X2] :
( X1 = X2
| ( sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
& sdtasdt0(X1,X0) != sdtasdt0(X2,X0) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) )
| sz00 = X0
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f82,plain,
! [X0] :
( ! [X1,X2] :
( X1 = X2
| ( sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
& sdtasdt0(X1,X0) != sdtasdt0(X2,X0) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) )
| sz00 = X0
| ~ aNaturalNumber0(X0) ),
inference(flattening,[],[f81]) ).
fof(f87,plain,
! [X0,X1] :
( ( sdtlseqdt0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& sdtpldt0(X0,X2) = X1 ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f88,plain,
! [X0,X1] :
( ( sdtlseqdt0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& sdtpldt0(X0,X2) = X1 ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f87]) ).
fof(f91,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f94,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(ennf_transformation,[],[f22]) ).
fof(f95,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(flattening,[],[f94]) ).
fof(f100,plain,
! [X0,X1,X2] :
( ( sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
& sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
& sdtlseqdt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0)) )
| sz00 = X0
| X1 = X2
| ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(ennf_transformation,[],[f25]) ).
fof(f101,plain,
! [X0,X1,X2] :
( ( sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
& sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
& sdtlseqdt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0)) )
| sz00 = X0
| X1 = X2
| ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(flattening,[],[f100]) ).
fof(f104,plain,
! [X0,X1] :
( sdtlseqdt0(X1,sdtasdt0(X1,X0))
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f27]) ).
fof(f105,plain,
! [X0,X1] :
( sdtlseqdt0(X1,sdtasdt0(X1,X0))
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f104]) ).
fof(f112,plain,
! [X0,X1] :
( ! [X2] :
( X2 = sdtsldt0(X1,X0)
<=> ( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f31]) ).
fof(f113,plain,
! [X0,X1] :
( ! [X2] :
( X2 = sdtsldt0(X1,X0)
<=> ( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f112]) ).
fof(f132,plain,
( ! [X0] :
( ~ aNaturalNumber0(X0)
| xn != sdtpldt0(xp,X0) )
& ~ sdtlseqdt0(xp,xn) ),
inference(ennf_transformation,[],[f42]) ).
fof(f134,plain,
( sz00 != xk
& sz10 != xk ),
inference(ennf_transformation,[],[f46]) ).
fof(f135,plain,
( aNaturalNumber0(xr)
& ? [X0] :
( aNaturalNumber0(X0)
& xk = sdtasdt0(xr,X0) )
& doDivides0(xr,xk)
& xr != sz00
& xr != sz10
& ! [X1] :
( sz10 = X1
| xr = X1
| ~ aNaturalNumber0(X1)
| ( ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtasdt0(X1,X2) != xr )
& ~ doDivides0(X1,xr) ) )
& isPrime0(xr) ),
inference(ennf_transformation,[],[f58]) ).
fof(f136,plain,
( aNaturalNumber0(xr)
& ? [X0] :
( aNaturalNumber0(X0)
& xk = sdtasdt0(xr,X0) )
& doDivides0(xr,xk)
& xr != sz00
& xr != sz10
& ! [X1] :
( sz10 = X1
| xr = X1
| ~ aNaturalNumber0(X1)
| ( ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtasdt0(X1,X2) != xr )
& ~ doDivides0(X1,xr) ) )
& isPrime0(xr) ),
inference(flattening,[],[f135]) ).
fof(f137,plain,
( ( aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& sdtsldt0(xn,xr) = xn )
| ( ! [X0] :
( ~ aNaturalNumber0(X0)
| xn != sdtpldt0(sdtsldt0(xn,xr),X0) )
& ~ sdtlseqdt0(sdtsldt0(xn,xr),xn)
& aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr)) ) ),
inference(ennf_transformation,[],[f54]) ).
fof(f138,plain,
( ( aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& sdtsldt0(xn,xr) = xn )
| ( ! [X0] :
( ~ aNaturalNumber0(X0)
| xn != sdtpldt0(sdtsldt0(xn,xr),X0) )
& ~ sdtlseqdt0(sdtsldt0(xn,xr),xn)
& aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr)) ) ),
inference(flattening,[],[f137]) ).
fof(f139,plain,
aNaturalNumber0(sz00),
inference(cnf_transformation,[],[f2]) ).
fof(f141,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f142,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f63]) ).
fof(f143,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f65]) ).
fof(f146,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtpldt0(sz00,X0) = X0 ),
inference(cnf_transformation,[],[f70]) ).
fof(f150,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(sz10,X0) = X0 ),
inference(cnf_transformation,[],[f75]) ).
fof(f152,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = sdtasdt0(sz00,X0) ),
inference(cnf_transformation,[],[f76]) ).
fof(f158,plain,
! [X2,X0,X1] :
( sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
| sz00 = X0
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| X1 = X2 ),
inference(cnf_transformation,[],[f82]) ).
fof(f159,plain,
! [X2,X0,X1] :
( sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
| sz00 = X0
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| X1 = X2 ),
inference(cnf_transformation,[],[f82]) ).
fof(f165,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f88]) ).
fof(f169,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtlseqdt0(X0,X0) ),
inference(cnf_transformation,[],[f91]) ).
fof(f171,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(X0,X2) ),
inference(cnf_transformation,[],[f95]) ).
fof(f178,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X2)
| X1 = X2
| sz00 = X0
| sdtlseqdt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0)) ),
inference(cnf_transformation,[],[f101]) ).
fof(f183,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sz00 = X0
| sdtlseqdt0(X1,sdtasdt0(X1,X0)) ),
inference(cnf_transformation,[],[f105]) ).
fof(f188,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| sdtasdt0(X0,X2) = X1
| sdtsldt0(X1,X0) != X2 ),
inference(cnf_transformation,[],[f113]) ).
fof(f206,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[],[f39]) ).
fof(f207,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[],[f39]) ).
fof(f250,plain,
~ sdtlseqdt0(xp,xn),
inference(cnf_transformation,[],[f132]) ).
fof(f262,plain,
sdtasdt0(xn,xm) = sdtasdt0(xp,xk),
inference(cnf_transformation,[],[f45]) ).
fof(f263,plain,
aNaturalNumber0(xk),
inference(cnf_transformation,[],[f45]) ).
fof(f265,plain,
sz00 != xk,
inference(cnf_transformation,[],[f134]) ).
fof(f273,plain,
sz10 != xr,
inference(cnf_transformation,[],[f136]) ).
fof(f274,plain,
sz00 != xr,
inference(cnf_transformation,[],[f136]) ).
fof(f276,plain,
aNaturalNumber0(xr),
inference(cnf_transformation,[],[f136]) ).
fof(f295,plain,
xn = sdtasdt0(xr,sK19),
inference(cnf_transformation,[],[f52]) ).
fof(f296,plain,
aNaturalNumber0(sK19),
inference(cnf_transformation,[],[f52]) ).
fof(f297,plain,
doDivides0(xr,xn),
inference(cnf_transformation,[],[f52]) ).
fof(f301,plain,
( ~ sdtlseqdt0(sdtsldt0(xn,xr),xn)
| xn = sdtsldt0(xn,xr) ),
inference(cnf_transformation,[],[f138]) ).
fof(f306,plain,
aNaturalNumber0(sdtsldt0(xn,xr)),
inference(cnf_transformation,[],[f138]) ).
fof(f310,plain,
! [X2,X0] :
( ~ aNaturalNumber0(sdtpldt0(X0,X2))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X0,sdtpldt0(X0,X2)) ),
inference(equality_resolution,[],[f165]) ).
fof(f318,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| sdtasdt0(X0,sdtsldt0(X1,X0)) = X1 ),
inference(equality_resolution,[],[f188]) ).
fof(f323,plain,
! [X2,X0] :
( ~ aNaturalNumber0(sdtpldt0(X0,X2))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X0,sdtpldt0(X0,X2)) ),
inference(consistent_polarity_flipping,[],[f310]) ).
fof(f329,plain,
! [X0] :
( ~ sdtlseqdt0(X0,X0)
| ~ aNaturalNumber0(X0) ),
inference(consistent_polarity_flipping,[],[f169]) ).
fof(f331,plain,
! [X2,X0,X1] :
( ~ sdtlseqdt0(X0,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtlseqdt0(X1,X2)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X2) ),
inference(consistent_polarity_flipping,[],[f171]) ).
fof(f341,plain,
! [X2,X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtlseqdt0(X1,X2)
| X1 = X2
| sz00 = X0
| ~ aNaturalNumber0(X2) ),
inference(consistent_polarity_flipping,[],[f178]) ).
fof(f343,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X1,sdtasdt0(X1,X0))
| ~ aNaturalNumber0(X0)
| sz00 = X0
| ~ aNaturalNumber0(X1) ),
inference(consistent_polarity_flipping,[],[f183]) ).
fof(f350,plain,
! [X0,X1] :
( doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| sz00 = X0
| sdtasdt0(X0,sdtsldt0(X1,X0)) = X1 ),
inference(consistent_polarity_flipping,[],[f318]) ).
fof(f382,plain,
sdtlseqdt0(xp,xn),
inference(consistent_polarity_flipping,[],[f250]) ).
fof(f395,plain,
~ doDivides0(xr,xn),
inference(consistent_polarity_flipping,[],[f297]) ).
fof(f398,plain,
( sdtlseqdt0(sdtsldt0(xn,xr),xn)
| xn = sdtsldt0(xn,xr) ),
inference(consistent_polarity_flipping,[],[f301]) ).
fof(f401,definition,
( spl20_1
<=> aNaturalNumber0(sdtsldt0(xn,xr)) ),
introduced(definition,[new_symbols(definition,[spl20_1])],[avatar_definition]) ).
fof(f403,plain,
( aNaturalNumber0(sdtsldt0(xn,xr))
| ~ spl20_1 ),
inference(avatar_component_clause,[],[f401]) ).
fof(f409,definition,
( spl20_3
<=> xn = sdtasdt0(xr,sdtsldt0(xn,xr)) ),
introduced(definition,[new_symbols(definition,[spl20_3])],[avatar_definition]) ).
fof(f411,plain,
( xn = sdtasdt0(xr,sdtsldt0(xn,xr))
| ~ spl20_3 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f414,definition,
( spl20_4
<=> xn = sdtsldt0(xn,xr) ),
introduced(definition,[new_symbols(definition,[spl20_4])],[avatar_definition]) ).
fof(f416,plain,
( xn = sdtsldt0(xn,xr)
| ~ spl20_4 ),
inference(avatar_component_clause,[],[f414]) ).
fof(f419,definition,
( spl20_5
<=> sdtlseqdt0(sdtsldt0(xn,xr),xn) ),
introduced(definition,[new_symbols(definition,[spl20_5])],[avatar_definition]) ).
fof(f421,plain,
( sdtlseqdt0(sdtsldt0(xn,xr),xn)
| ~ spl20_5 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f422,plain,
( spl20_4
| spl20_5 ),
inference(avatar_split_clause,[],[f398,f419,f414]) ).
fof(f427,plain,
spl20_1,
inference(avatar_split_clause,[],[f306,f401]) ).
fof(f458,definition,
( spl20_11
<=> doDivides0(xr,xn) ),
introduced(definition,[new_symbols(definition,[spl20_11])],[avatar_definition]) ).
fof(f460,plain,
( ~ doDivides0(xr,xn)
| spl20_11 ),
inference(avatar_component_clause,[],[f458]) ).
fof(f469,definition,
( spl20_13
<=> aNaturalNumber0(sz10) ),
introduced(definition,[new_symbols(definition,[spl20_13])],[avatar_definition]) ).
fof(f470,plain,
( aNaturalNumber0(sz10)
| ~ spl20_13 ),
inference(avatar_component_clause,[],[f469]) ).
fof(f478,definition,
( spl20_15
<=> aNaturalNumber0(sz00) ),
introduced(definition,[new_symbols(definition,[spl20_15])],[avatar_definition]) ).
fof(f479,plain,
( aNaturalNumber0(sz00)
| ~ spl20_15 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f482,plain,
spl20_13,
inference(avatar_split_clause,[],[f141,f469]) ).
fof(f483,plain,
spl20_15,
inference(avatar_split_clause,[],[f139,f478]) ).
fof(f485,plain,
( xn = sdtasdt0(xr,xn)
| ~ spl20_3
| ~ spl20_4 ),
inference(forward_demodulation,[],[f411,f416]) ).
fof(f486,plain,
~ spl20_11,
inference(avatar_split_clause,[],[f395,f458]) ).
fof(f527,plain,
( sdtsldt0(xn,xr) = sdtasdt0(sz10,sdtsldt0(xn,xr))
| ~ spl20_1 ),
inference(resolution,[],[f150,f403]) ).
fof(f532,plain,
xr = sdtasdt0(sz10,xr),
inference(resolution,[],[f150,f276]) ).
fof(f542,plain,
sK19 = sdtasdt0(sz10,sK19),
inference(resolution,[],[f150,f296]) ).
fof(f543,plain,
( xn = sdtasdt0(sz10,xn)
| ~ spl20_1
| ~ spl20_4 ),
inference(forward_demodulation,[],[f527,f416]) ).
fof(f567,plain,
sz00 = sdtasdt0(sz00,xm),
inference(resolution,[],[f152,f207]) ).
fof(f623,plain,
( aNaturalNumber0(xn)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sK19) ),
inference(superposition,[],[f143,f295]) ).
fof(f752,plain,
( ~ sdtlseqdt0(xp,sdtasdt0(xn,xm))
| ~ aNaturalNumber0(xk)
| sz00 = xk
| ~ aNaturalNumber0(xp) ),
inference(superposition,[],[f343,f262]) ).
fof(f763,plain,
( ~ sdtlseqdt0(xp,sdtasdt0(xn,xm))
| sz00 = xk
| ~ aNaturalNumber0(xp) ),
inference(forward_subsumption_resolution,[],[f752,f263]) ).
fof(f771,plain,
( ~ sdtlseqdt0(xp,sdtasdt0(xn,xm))
| ~ aNaturalNumber0(xp) ),
inference(forward_subsumption_resolution,[],[f763,f265]) ).
fof(f807,definition,
( spl20_23
<=> sz00 = xn ),
introduced(definition,[new_symbols(definition,[spl20_23])],[avatar_definition]) ).
fof(f809,plain,
( sz00 = xn
| ~ spl20_23 ),
inference(avatar_component_clause,[],[f807]) ).
fof(f811,plain,
~ sdtlseqdt0(xp,sdtasdt0(xn,xm)),
inference(forward_subsumption_resolution,[],[f771,f206]) ).
fof(f817,definition,
( spl20_25
<=> sdtlseqdt0(xp,sdtasdt0(xn,xm)) ),
introduced(definition,[new_symbols(definition,[spl20_25])],[avatar_definition]) ).
fof(f819,plain,
( ~ sdtlseqdt0(xp,sdtasdt0(xn,xm))
| spl20_25 ),
inference(avatar_component_clause,[],[f817]) ).
fof(f826,plain,
~ spl20_25,
inference(avatar_split_clause,[],[f811,f817]) ).
fof(f864,plain,
! [X2,X0] :
( ~ sdtlseqdt0(X0,sdtpldt0(X0,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f323,f142]) ).
fof(f1168,definition,
( spl20_44
<=> xn = sdtasdt0(xn,xm) ),
introduced(definition,[new_symbols(definition,[spl20_44])],[avatar_definition]) ).
fof(f1169,plain,
( xn = sdtasdt0(xn,xm)
| ~ spl20_44 ),
inference(avatar_component_clause,[],[f1168]) ).
fof(f1415,plain,
( ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xn)
| sz00 = xr
| xn = sdtasdt0(xr,sdtsldt0(xn,xr))
| spl20_11 ),
inference(resolution,[],[f350,f460]) ).
fof(f1427,plain,
( ~ aNaturalNumber0(xn)
| sz00 = xr
| xn = sdtasdt0(xr,sdtsldt0(xn,xr))
| spl20_11 ),
inference(forward_subsumption_resolution,[],[f1415,f276]) ).
fof(f1927,plain,
( aNaturalNumber0(xn)
| ~ aNaturalNumber0(sK19) ),
inference(forward_subsumption_resolution,[],[f623,f276]) ).
fof(f1930,definition,
( spl20_70
<=> aNaturalNumber0(xn) ),
introduced(definition,[new_symbols(definition,[spl20_70])],[avatar_definition]) ).
fof(f1931,plain,
( aNaturalNumber0(xn)
| ~ spl20_70 ),
inference(avatar_component_clause,[],[f1930]) ).
fof(f1963,plain,
( ~ aNaturalNumber0(xn)
| xn = sdtasdt0(xr,sdtsldt0(xn,xr))
| spl20_11 ),
inference(forward_subsumption_resolution,[],[f1427,f274]) ).
fof(f1974,plain,
aNaturalNumber0(xn),
inference(forward_subsumption_resolution,[],[f1927,f296]) ).
fof(f1987,plain,
( spl20_3
| ~ spl20_70
| spl20_11 ),
inference(avatar_split_clause,[],[f1963,f458,f1930,f409]) ).
fof(f1993,plain,
spl20_70,
inference(avatar_split_clause,[],[f1974,f1930]) ).
fof(f1996,plain,
( xn = sdtpldt0(sz00,xn)
| ~ spl20_70 ),
inference(resolution,[],[f1931,f146]) ).
fof(f2007,plain,
( ! [X0] :
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| sdtlseqdt0(X0,xn)
| sdtlseqdt0(sdtsldt0(xn,xr),X0)
| ~ aNaturalNumber0(xn) )
| ~ spl20_5 ),
inference(resolution,[],[f421,f331]) ).
fof(f2012,plain,
( ! [X0] :
( ~ aNaturalNumber0(X0)
| sdtlseqdt0(X0,xn)
| sdtlseqdt0(sdtsldt0(xn,xr),X0)
| ~ aNaturalNumber0(xn) )
| ~ spl20_1
| ~ spl20_5 ),
inference(forward_subsumption_resolution,[],[f2007,f403]) ).
fof(f2015,plain,
( ! [X0] :
( sdtlseqdt0(sdtsldt0(xn,xr),X0)
| sdtlseqdt0(X0,xn)
| ~ aNaturalNumber0(X0) )
| ~ spl20_1
| ~ spl20_5
| ~ spl20_70 ),
inference(forward_subsumption_resolution,[],[f2012,f1931]) ).
fof(f2034,plain,
( ! [X0] :
( xn != sdtasdt0(xr,X0)
| sz00 = xr
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xr)
| sdtsldt0(xn,xr) = X0 )
| ~ spl20_3 ),
inference(superposition,[],[f159,f411]) ).
fof(f2040,plain,
( ! [X0] :
( xn != sdtasdt0(xr,X0)
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xr)
| sdtsldt0(xn,xr) = X0 )
| ~ spl20_3 ),
inference(forward_subsumption_resolution,[],[f2034,f274]) ).
fof(f2045,plain,
( ! [X0] :
( xn != sdtasdt0(xr,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xr)
| sdtsldt0(xn,xr) = X0 )
| ~ spl20_1
| ~ spl20_3 ),
inference(forward_subsumption_resolution,[],[f2040,f403]) ).
fof(f2050,definition,
( spl20_82
<=> sz00 = sdtsldt0(xn,xr) ),
introduced(definition,[new_symbols(definition,[spl20_82])],[avatar_definition]) ).
fof(f2052,plain,
( sz00 = sdtsldt0(xn,xr)
| ~ spl20_82 ),
inference(avatar_component_clause,[],[f2050]) ).
fof(f2054,plain,
( ! [X0] :
( xn != sdtasdt0(xr,X0)
| ~ aNaturalNumber0(X0)
| sdtsldt0(xn,xr) = X0 )
| ~ spl20_1
| ~ spl20_3 ),
inference(forward_subsumption_resolution,[],[f2045,f276]) ).
fof(f2176,plain,
( ~ sdtlseqdt0(sz00,xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sz00)
| ~ spl20_70 ),
inference(superposition,[],[f864,f1996]) ).
fof(f2177,plain,
( ~ sdtlseqdt0(sz00,xn)
| ~ aNaturalNumber0(sz00)
| ~ spl20_70 ),
inference(forward_subsumption_resolution,[],[f2176,f1931]) ).
fof(f2186,plain,
( ~ sdtlseqdt0(sz00,xn)
| ~ spl20_15
| ~ spl20_70 ),
inference(forward_subsumption_resolution,[],[f2177,f479]) ).
fof(f2300,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(X0,sdtsldt0(xn,xr)),xn)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| sdtlseqdt0(X0,xr)
| xr = X0
| sz00 = sdtsldt0(xn,xr)
| ~ aNaturalNumber0(xr) )
| ~ spl20_3 ),
inference(superposition,[],[f341,f411]) ).
fof(f2309,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(X0,sdtsldt0(xn,xr)),xn)
| ~ aNaturalNumber0(X0)
| sdtlseqdt0(X0,xr)
| xr = X0
| sz00 = sdtsldt0(xn,xr)
| ~ aNaturalNumber0(xr) )
| ~ spl20_1
| ~ spl20_3 ),
inference(forward_subsumption_resolution,[],[f2300,f403]) ).
fof(f2325,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(X0,sdtsldt0(xn,xr)),xn)
| ~ aNaturalNumber0(X0)
| sdtlseqdt0(X0,xr)
| xr = X0
| sz00 = sdtsldt0(xn,xr) )
| ~ spl20_1
| ~ spl20_3 ),
inference(forward_subsumption_resolution,[],[f2309,f276]) ).
fof(f2338,definition,
( spl20_84
<=> ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(X0,sK19),xn)
| xr = X0
| sdtlseqdt0(X0,xr)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl20_84])],[avatar_definition]) ).
fof(f2339,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(X0,sK19),xn)
| xr = X0
| sdtlseqdt0(X0,xr)
| ~ aNaturalNumber0(X0) )
| ~ spl20_84 ),
inference(avatar_component_clause,[],[f2338]) ).
fof(f2354,definition,
( spl20_88
<=> ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(X0,sdtsldt0(xn,xr)),xn)
| xr = X0
| sdtlseqdt0(X0,xr)
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl20_88])],[avatar_definition]) ).
fof(f2355,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(X0,sdtsldt0(xn,xr)),xn)
| xr = X0
| sdtlseqdt0(X0,xr)
| ~ aNaturalNumber0(X0) )
| ~ spl20_88 ),
inference(avatar_component_clause,[],[f2354]) ).
fof(f2356,plain,
( spl20_82
| spl20_88
| ~ spl20_1
| ~ spl20_3 ),
inference(avatar_split_clause,[],[f2325,f409,f401,f2354,f2050]) ).
fof(f2393,plain,
( sdtlseqdt0(sz00,xn)
| ~ spl20_5
| ~ spl20_82 ),
inference(superposition,[],[f421,f2052]) ).
fof(f2397,plain,
( $false
| ~ spl20_5
| ~ spl20_15
| ~ spl20_70
| ~ spl20_82 ),
inference(forward_subsumption_resolution,[],[f2393,f2186]) ).
fof(f2398,plain,
( ~ spl20_5
| ~ spl20_15
| ~ spl20_70
| ~ spl20_82 ),
inference(avatar_contradiction_clause,[],[f2397]) ).
fof(f2573,definition,
( spl20_100
<=> ! [X0] :
( xn != sdtasdt0(X0,xn)
| xr = X0
| ~ aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl20_100])],[avatar_definition]) ).
fof(f2574,plain,
( ! [X0] :
( xn != sdtasdt0(X0,xn)
| xr = X0
| ~ aNaturalNumber0(X0) )
| ~ spl20_100 ),
inference(avatar_component_clause,[],[f2573]) ).
fof(f4537,plain,
( xn != xn
| sz10 = xr
| ~ aNaturalNumber0(sz10)
| ~ spl20_1
| ~ spl20_4
| ~ spl20_100 ),
inference(superposition,[],[f2574,f543]) ).
fof(f4538,plain,
( sz10 = xr
| ~ aNaturalNumber0(sz10)
| ~ spl20_1
| ~ spl20_4
| ~ spl20_100 ),
inference(trivial_inequality_removal,[],[f4537]) ).
fof(f4539,plain,
( ~ aNaturalNumber0(sz10)
| ~ spl20_1
| ~ spl20_4
| ~ spl20_100 ),
inference(forward_subsumption_resolution,[],[f4538,f273]) ).
fof(f4540,plain,
( $false
| ~ spl20_1
| ~ spl20_4
| ~ spl20_13
| ~ spl20_100 ),
inference(forward_subsumption_resolution,[],[f4539,f470]) ).
fof(f4541,plain,
( ~ spl20_1
| ~ spl20_4
| ~ spl20_13
| ~ spl20_100 ),
inference(avatar_contradiction_clause,[],[f4540]) ).
fof(f5049,plain,
( sdtlseqdt0(sdtsldt0(xn,xr),xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| ~ spl20_1
| ~ spl20_5
| ~ spl20_70 ),
inference(resolution,[],[f2015,f329]) ).
fof(f5175,plain,
( xn != xn
| ~ aNaturalNumber0(sK19)
| sdtsldt0(xn,xr) = sK19
| ~ spl20_1
| ~ spl20_3 ),
inference(superposition,[],[f2054,f295]) ).
fof(f5176,plain,
( ~ aNaturalNumber0(sK19)
| sdtsldt0(xn,xr) = sK19
| ~ spl20_1
| ~ spl20_3 ),
inference(trivial_inequality_removal,[],[f5175]) ).
fof(f5177,plain,
( sdtsldt0(xn,xr) = sK19
| ~ spl20_1
| ~ spl20_3 ),
inference(forward_subsumption_resolution,[],[f5176,f296]) ).
fof(f5461,definition,
( spl20_164
<=> sdtlseqdt0(sz10,xr) ),
introduced(definition,[new_symbols(definition,[spl20_164])],[avatar_definition]) ).
fof(f5481,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(X0,sK19),xn)
| xr = X0
| sdtlseqdt0(X0,xr)
| ~ aNaturalNumber0(X0) )
| ~ spl20_1
| ~ spl20_3
| ~ spl20_88 ),
inference(forward_demodulation,[],[f2355,f5177]) ).
fof(f5482,plain,
( spl20_84
| ~ spl20_1
| ~ spl20_3
| ~ spl20_88 ),
inference(avatar_split_clause,[],[f5481,f2354,f409,f401,f2338]) ).
fof(f8290,plain,
( ~ sdtlseqdt0(sz10,xr)
| ~ aNaturalNumber0(xr)
| sz00 = xr
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[],[f343,f532]) ).
fof(f8293,plain,
( ~ sdtlseqdt0(sz10,xr)
| sz00 = xr
| ~ aNaturalNumber0(sz10) ),
inference(forward_subsumption_resolution,[],[f8290,f276]) ).
fof(f8303,plain,
( ~ sdtlseqdt0(sz10,xr)
| ~ aNaturalNumber0(sz10) ),
inference(forward_subsumption_resolution,[],[f8293,f274]) ).
fof(f8312,plain,
( ~ sdtlseqdt0(sz10,xr)
| ~ spl20_13 ),
inference(forward_subsumption_resolution,[],[f8303,f470]) ).
fof(f8321,plain,
( ~ spl20_164
| ~ spl20_13 ),
inference(avatar_split_clause,[],[f8312,f469,f5461]) ).
fof(f22903,plain,
( ! [X0] :
( xn != sdtasdt0(X0,xn)
| sz00 = xn
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xn)
| xr = X0 )
| ~ spl20_3
| ~ spl20_4 ),
inference(superposition,[],[f158,f485]) ).
fof(f22922,plain,
( ! [X0] :
( xn != sdtasdt0(X0,xn)
| sz00 = xn
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xn)
| xr = X0 )
| ~ spl20_3
| ~ spl20_4 ),
inference(forward_subsumption_resolution,[],[f22903,f276]) ).
fof(f22930,plain,
( ! [X0] :
( xn != sdtasdt0(X0,xn)
| sz00 = xn
| ~ aNaturalNumber0(X0)
| xr = X0 )
| ~ spl20_3
| ~ spl20_4
| ~ spl20_70 ),
inference(forward_subsumption_resolution,[],[f22922,f1931]) ).
fof(f22938,plain,
( spl20_23
| spl20_100
| ~ spl20_3
| ~ spl20_4
| ~ spl20_70 ),
inference(avatar_split_clause,[],[f22930,f1930,f414,f409,f2573,f807]) ).
fof(f23138,plain,
( xn = sdtasdt0(xn,xm)
| ~ spl20_23 ),
inference(superposition,[],[f567,f809]) ).
fof(f23236,plain,
( spl20_44
| ~ spl20_23 ),
inference(avatar_split_clause,[],[f23138,f807,f1168]) ).
fof(f23572,plain,
( sdtlseqdt0(sdtsldt0(xn,xr),xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr))
| ~ spl20_1
| ~ spl20_5
| ~ spl20_70 ),
inference(duplicate_literal_removal,[],[f5049]) ).
fof(f23641,plain,
( sdtlseqdt0(sdtsldt0(xn,xr),xn)
| ~ spl20_1
| ~ spl20_5
| ~ spl20_70 ),
inference(forward_subsumption_resolution,[],[f23572,f403]) ).
fof(f24319,definition,
( spl20_1273
<=> sdtlseqdt0(sK19,xn) ),
introduced(definition,[new_symbols(definition,[spl20_1273])],[avatar_definition]) ).
fof(f24455,plain,
( sdtlseqdt0(sK19,xn)
| ~ spl20_1
| ~ spl20_3
| ~ spl20_5
| ~ spl20_70 ),
inference(forward_demodulation,[],[f23641,f5177]) ).
fof(f24820,plain,
( spl20_1273
| ~ spl20_1
| ~ spl20_3
| ~ spl20_5
| ~ spl20_70 ),
inference(avatar_split_clause,[],[f24455,f1930,f419,f409,f401,f24319]) ).
fof(f25919,plain,
( ~ sdtlseqdt0(xp,xn)
| spl20_25
| ~ spl20_44 ),
inference(superposition,[],[f819,f1169]) ).
fof(f25953,plain,
( $false
| spl20_25
| ~ spl20_44 ),
inference(forward_subsumption_resolution,[],[f25919,f382]) ).
fof(f25954,plain,
( spl20_25
| ~ spl20_44 ),
inference(avatar_contradiction_clause,[],[f25953]) ).
fof(f28156,plain,
( ~ sdtlseqdt0(sK19,xn)
| sz10 = xr
| sdtlseqdt0(sz10,xr)
| ~ aNaturalNumber0(sz10)
| ~ spl20_84 ),
inference(superposition,[],[f2339,f542]) ).
fof(f28157,plain,
( ~ sdtlseqdt0(sK19,xn)
| sdtlseqdt0(sz10,xr)
| ~ aNaturalNumber0(sz10)
| ~ spl20_84 ),
inference(forward_subsumption_resolution,[],[f28156,f273]) ).
fof(f28160,plain,
( ~ sdtlseqdt0(sK19,xn)
| sdtlseqdt0(sz10,xr)
| ~ spl20_13
| ~ spl20_84 ),
inference(forward_subsumption_resolution,[],[f28157,f470]) ).
fof(f28161,plain,
( spl20_164
| ~ spl20_1273
| ~ spl20_13
| ~ spl20_84 ),
inference(avatar_split_clause,[],[f28160,f2338,f469,f24319,f5461]) ).
cnf(s4,plain,
( spl20_4
| spl20_5 ),
inference(sat_conversion,[],[f422]) ).
cnf(s9,plain,
spl20_1,
inference(sat_conversion,[],[f427]) ).
cnf(s24,plain,
spl20_13,
inference(sat_conversion,[],[f482]) ).
cnf(s25,plain,
spl20_15,
inference(sat_conversion,[],[f483]) ).
cnf(s26,plain,
~ spl20_11,
inference(sat_conversion,[],[f486]) ).
cnf(s34,plain,
~ spl20_25,
inference(sat_conversion,[],[f826]) ).
cnf(s101,plain,
( spl20_3
| spl20_11
| ~ spl20_70 ),
inference(sat_conversion,[],[f1987]) ).
cnf(s104,plain,
spl20_70,
inference(sat_conversion,[],[f1993]) ).
cnf(s112,plain,
( ~ spl20_1
| ~ spl20_3
| spl20_82
| spl20_88 ),
inference(sat_conversion,[],[f2356]) ).
cnf(s120,plain,
( ~ spl20_5
| ~ spl20_15
| ~ spl20_70
| ~ spl20_82 ),
inference(sat_conversion,[],[f2398]) ).
cnf(s390,plain,
( ~ spl20_1
| ~ spl20_4
| ~ spl20_13
| ~ spl20_100 ),
inference(sat_conversion,[],[f4541]) ).
cnf(s470,plain,
( ~ spl20_1
| ~ spl20_3
| spl20_84
| ~ spl20_88 ),
inference(sat_conversion,[],[f5482]) ).
cnf(s575,plain,
( ~ spl20_13
| ~ spl20_164 ),
inference(sat_conversion,[],[f8321]) ).
cnf(s2000,plain,
( ~ spl20_3
| ~ spl20_4
| spl20_23
| ~ spl20_70
| spl20_100 ),
inference(sat_conversion,[],[f22938]) ).
cnf(s2022,plain,
( ~ spl20_23
| spl20_44 ),
inference(sat_conversion,[],[f23236]) ).
cnf(s2424,plain,
( ~ spl20_1
| ~ spl20_3
| ~ spl20_5
| ~ spl20_70
| spl20_1273 ),
inference(sat_conversion,[],[f24820]) ).
cnf(s2666,plain,
( spl20_25
| ~ spl20_44 ),
inference(sat_conversion,[],[f25954]) ).
cnf(s3038,plain,
( ~ spl20_13
| ~ spl20_84
| spl20_164
| ~ spl20_1273 ),
inference(sat_conversion,[],[f28161]) ).
cnf(s3061,plain,
( spl20_3
| spl20_11 ),
inference(rat,[],[s101,s104]) ).
cnf(s3108,plain,
~ spl20_44,
inference(rat,[],[s2666,s34]) ).
cnf(s3111,plain,
~ spl20_23,
inference(rat,[],[s2022,s3108]) ).
cnf(s3126,plain,
spl20_3,
inference(rat,[],[s3061,s26]) ).
cnf(s3188,plain,
~ spl20_164,
inference(rat,[],[s575,s24]) ).
cnf(s3208,plain,
~ spl20_4,
inference(rat,[],[s390,s2000,s24,s9,s3111,s104,s3126]) ).
cnf(s3210,plain,
spl20_5,
inference(rat,[],[s4,s3208]) ).
cnf(s3213,plain,
~ spl20_82,
inference(rat,[],[s120,s25,s104,s3210]) ).
cnf(s3217,plain,
spl20_1273,
inference(rat,[],[s2424,s9,s104,s3126,s3210]) ).
cnf(s3233,plain,
spl20_88,
inference(rat,[],[s112,s9,s3126,s3213]) ).
cnf(s3248,plain,
~ spl20_84,
inference(rat,[],[s3038,s3188,s24,s3217]) ).
cnf(s3250,plain,
$false,
inference(rat,[],[s470,s9,s3126,s3233,s3248]) ).
fof(f28162,plain,
$false,
inference(avatar_sat_refutation,[],[s3250]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM510+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.36 % Computer : n011.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 20:16:01 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 Running first-order model finding
% 0.11/0.39 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.31/1.15 % (2733579)Will run a generic schedule for satisfiability detection.
% 4.31/1.15 % (2733586)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=590431787:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.31/1.15 % (2733585)% WARNING: option uhcvi not known.
% 4.31/1.15 % (2733584)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3173746794_2999 on theBenchmark for (2999ds/0Mi)
% 4.31/1.15 % (2733585)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1065144694:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.31/1.15 % (2733587)dis+10_1_sil=32000:sp=arity:random_seed=1459703738:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.31/1.15 % (2733588)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2603474142:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.31/1.15 % (2733590)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2036997766:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.31/1.15 % (2733589)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2424769497:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.31/1.15 % Detected minimum model sizes of [4]
% 4.31/1.15 % Detected maximum model sizes of [max]
% 4.31/1.15 % TRYING [4]
% 4.31/1.15 % TRYING [5]
% 4.31/1.15 % (2733587)Instruction limit reached!
% 4.31/1.15 % (2733587)------------------------------
% 4.31/1.15 % (2733587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.31/1.15 % (2733587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.15 % (2733587)CaDiCaL version: 2.1.3
% 4.31/1.15 % (2733587)Termination reason: Instruction limit
% 4.31/1.15 % (2733587)Termination phase: Saturation
% 4.31/1.15 % (2733587)Time elapsed: 0.061 s
% 4.31/1.15 % (2733587)Peak memory usage: 13 MB
% 4.31/1.15 % (2733587)Instructions burned: 103 (million)
% 4.31/1.15 % (2733588)Instruction limit reached!
% 4.31/1.15 % (2733588)------------------------------
% 4.31/1.15 % (2733588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.31/1.15 % (2733588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.15 % (2733588)CaDiCaL version: 2.1.3
% 4.31/1.15 % (2733588)Termination reason: Instruction limit
% 4.31/1.15 % (2733588)Termination phase: Saturation
% 4.31/1.15 % (2733588)Time elapsed: 0.062 s
% 4.31/1.15 % (2733588)Peak memory usage: 13 MB
% 4.31/1.15 % (2733588)Instructions burned: 116 (million)
% 4.31/1.15 % (2733589)Instruction limit reached!
% 4.31/1.15 % (2733589)------------------------------
% 4.31/1.15 % (2733589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.31/1.15 % (2733589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.15 % (2733589)CaDiCaL version: 2.1.3
% 4.31/1.15 % (2733589)Termination reason: Instruction limit
% 4.31/1.15 % (2733589)Termination phase: Saturation
% 4.31/1.15 % (2733589)Time elapsed: 0.070 s
% 4.31/1.15 % (2733589)Peak memory usage: 13 MB
% 4.31/1.15 % (2733589)Instructions burned: 132 (million)
% 4.31/1.15 % (2733598)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=111474668:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 4.31/1.15 % (2733599)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2628569646:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 4.31/1.15 % Detected minimum model sizes of [4]
% 4.31/1.15 % Detected maximum model sizes of [max]
% 4.31/1.15 % TRYING [4]
% 4.31/1.15 % (2733600)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=2510210242:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 4.31/1.15 % (2733590)Instruction limit reached!
% 4.31/1.15 % (2733590)------------------------------
% 4.31/1.15 % (2733590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.31/1.15 % (2733590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.15 % (2733590)CaDiCaL version: 2.1.3
% 4.31/1.15 % (2733590)Termination reason: Instruction limit
% 4.31/1.15 % (2733590)Termination phase: Saturation
% 4.31/1.15 % (2733590)Time elapsed: 0.097 s
% 4.31/1.15 % (2733590)Peak memory usage: 15 MB
% 4.31/1.15 % (2733590)Instructions burned: 159 (million)
% 4.31/1.15 % (2733604)ott-21_1_sil=16000:fs=off:random_seed=2263430054:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.31/1.15 % TRYING [5]
% 4.31/1.15 % TRYING [6]
% 4.31/1.15 % (2733599)Instruction limit reached!
% 4.31/1.15 % (2733599)------------------------------
% 4.31/1.15 % (2733599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.31/1.15 % (2733599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.15 % (2733599)CaDiCaL version: 2.1.3
% 4.31/1.15 % (2733599)Termination reason: Instruction limit
% 4.31/1.15 % (2733599)Termination phase: Saturation
% 4.31/1.15 % (2733599)Time elapsed: 0.060 s
% 4.31/1.15 % (2733599)Peak memory usage: 12 MB
% 4.31/1.15 % (2733599)Instructions burned: 131 (million)
% 4.31/1.15 % (2733606)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=716972603:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 4.31/1.15 % (2733604)Instruction limit reached!
% 4.31/1.15 % (2733604)------------------------------
% 4.31/1.15 % (2733604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.31/1.15 % (2733604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.15 % (2733604)CaDiCaL version: 2.1.3
% 4.31/1.15 % (2733604)Termination reason: Instruction limit
% 4.31/1.15 % (2733604)Termination phase: Saturation
% 4.31/1.15 % (2733604)Time elapsed: 0.092 s
% 4.31/1.15 % (2733604)Peak memory usage: 13 MB
% 4.31/1.15 % (2733604)Instructions burned: 181 (million)
% 4.31/1.15 % TRYING [6]
% 4.31/1.15 % (2733608)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3303822231:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 4.31/1.15 % Detected minimum model sizes of [4]
% 4.31/1.15 % Detected maximum model sizes of [max]
% 4.31/1.15 % TRYING [4]
% 4.31/1.15 % (2733598)Instruction limit reached!
% 4.31/1.15 % (2733598)------------------------------
% 4.31/1.15 % (2733598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.31/1.15 % (2733598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.15 % (2733598)CaDiCaL version: 2.1.3
% 4.31/1.15 % (2733598)Termination reason: Instruction limit
% 4.31/1.15 % (2733598)Termination phase: Finite model building constraint generation
% 4.31/1.15 % (2733598)Time elapsed: 0.255 s
% 4.31/1.15 % (2733598)Peak memory usage: 32 MB
% 4.31/1.15 % (2733598)Instructions burned: 714 (million)
% 4.31/1.15 % TRYING [7]
% 4.31/1.15 % TRYING [5]
% 4.31/1.15 % (2733610)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2891206102:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 4.31/1.15 % (2733600)Instruction limit reached!
% 4.31/1.15 % (2733600)------------------------------
% 4.31/1.15 % (2733600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.31/1.15 % (2733600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.15 % (2733600)CaDiCaL version: 2.1.3
% 4.31/1.15 % (2733600)Termination reason: Instruction limit
% 4.31/1.15 % (2733600)Termination phase: Saturation
% 4.31/1.15 % (2733600)Time elapsed: 0.371 s
% 4.31/1.15 % (2733600)Peak memory usage: 17 MB
% 4.31/1.15 % (2733600)Instructions burned: 685 (million)
% 4.31/1.15 % (2733612)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2513729335:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 4.31/1.15 % (2733606)Instruction limit reached!
% 4.31/1.15 % (2733606)------------------------------
% 4.31/1.15 % (2733606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.31/1.15 % (2733606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.15 % (2733606)CaDiCaL version: 2.1.3
% 4.31/1.15 % (2733606)Termination reason: Instruction limit
% 4.31/1.15 % (2733606)Termination phase: Saturation
% 4.31/1.15 % (2733606)Time elapsed: 0.317 s
% 4.31/1.15 % (2733606)Peak memory usage: 14 MB
% 4.31/1.15 % (2733606)Instructions burned: 477 (million)
% 4.31/1.15 % (2733614)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=3660190701: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)
% 4.31/1.15 % (2733608)Instruction limit reached!
% 4.31/1.15 % (2733608)------------------------------
% 4.31/1.15 % (2733608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.31/1.15 % (2733608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.15 % (2733608)CaDiCaL version: 2.1.3
% 4.31/1.15 % (2733608)Termination reason: Instruction limit
% 4.31/1.15 % (2733608)Termination phase: Finite model building SAT solving
% 4.31/1.15 % (2733608)Time elapsed: 0.356 s
% 4.31/1.15 % (2733608)Peak memory usage: 24 MB
% 4.31/1.15 % (2733608)Instructions burned: 867 (million)
% 4.31/1.15 % (2733616)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1537118740:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 4.31/1.15 % TRYING [14]
% 4.31/1.15 % (2733585) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2733579-2733585"...
% 4.31/1.15 % (2733585)...printing done.
% 4.31/1.15 % (2733585)Refutation found. Thanks to Tanya!
% 4.31/1.15 % SZS status Theorem for theBenchmark
% 4.31/1.15 % SZS output start Proof for theBenchmark
% See solution above
% 4.31/1.15 % (2733585)------------------------------
% 4.31/1.15 % (2733585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.31/1.15 % (2733585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.15 % (2733585)CaDiCaL version: 2.1.3
% 4.31/1.15 % (2733585)Termination reason: Refutation
% 4.31/1.15 % (2733585)Time elapsed: 0.693 s
% 4.31/1.15 % (2733585)Peak memory usage: 23 MB
% 4.31/1.15 % (2733585)Instructions burned: 1230 (million)
% 4.31/1.15 % (2733579)Success in time 0.751 s
% 4.31/1.15 % Vampire exiting
%------------------------------------------------------------------------------