%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : RNG120+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:35:36 PM UTC 2026
% Result : Theorem 3.75s 1.19s
% Output : Refutation 4.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 13
% Syntax : Number of formulae : 74 ( 15 unt; 4 def)
% Number of atoms : 394 ( 63 equ)
% Maximal formula atoms : 28 ( 5 avg)
% Number of connectives : 468 ( 148 ~; 137 |; 149 &)
% ( 16 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 5 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 10 con; 0-2 aty)
% Number of variables : 149 ( 0 sgn 104 !; 45 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
aElement0(sz10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsC_01) ).
fof(f4,axiom,
! [X0] :
( aElement0(X0)
=> aElement0(smndt0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsU) ).
fof(f15,axiom,
! [X0] :
( aElement0(X0)
=> ( sdtasdt0(smndt0(sz10),X0) = smndt0(X0)
& smndt0(X0) = sdtasdt0(X0,smndt0(sz10)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulMnOne) ).
fof(f20,axiom,
! [X0] :
( aSet0(X0)
=> ! [X1] :
( aElementOf0(X1,X0)
=> aElement0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEOfElem) ).
fof(f24,axiom,
! [X0] :
( aIdeal0(X0)
<=> ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,X0)
=> ( ! [X2] :
( aElementOf0(X2,X0)
=> aElementOf0(sdtpldt0(X1,X2),X0) )
& ! [X2] :
( aElement0(X2)
=> aElementOf0(sdtasdt0(X2,X1),X0) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefIdeal) ).
fof(f42,axiom,
( aSet0(xI)
& ! [X0] :
( aElementOf0(X0,xI)
=> ( ! [X1] :
( aElementOf0(X1,xI)
=> aElementOf0(sdtpldt0(X0,X1),xI) )
& ! [X1] :
( aElement0(X1)
=> aElementOf0(sdtasdt0(X1,X0),xI) ) ) )
& aIdeal0(xI)
& ! [X0] :
( aElementOf0(X0,slsdtgt0(xa))
<=> ? [X1] :
( aElement0(X1)
& sdtasdt0(xa,X1) = X0 ) )
& ! [X0] :
( aElementOf0(X0,slsdtgt0(xb))
<=> ? [X1] :
( aElement0(X1)
& sdtasdt0(xb,X1) = X0 ) )
& ! [X0] :
( aElementOf0(X0,xI)
<=> ? [X1,X2] :
( aElementOf0(X1,slsdtgt0(xa))
& aElementOf0(X2,slsdtgt0(xb))
& sdtpldt0(X1,X2) = X0 ) )
& xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2174) ).
fof(f45,axiom,
( ? [X0,X1] :
( aElementOf0(X0,slsdtgt0(xa))
& aElementOf0(X1,slsdtgt0(xb))
& sdtpldt0(X0,X1) = xu )
& aElementOf0(xu,xI)
& xu != sz00
& ! [X0] :
( ( ( ? [X1,X2] :
( aElementOf0(X1,slsdtgt0(xa))
& aElementOf0(X2,slsdtgt0(xb))
& sdtpldt0(X1,X2) = X0 )
| aElementOf0(X0,xI) )
& X0 != sz00 )
=> ~ iLess0(sbrdtbr0(X0),sbrdtbr0(xu)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2273) ).
fof(f50,axiom,
( aElement0(xq)
& aElement0(xr)
& xb = sdtpldt0(sdtasdt0(xq,xu),xr)
& ( xr = sz00
| iLess0(sbrdtbr0(xr),sbrdtbr0(xu)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2666) ).
fof(f52,conjecture,
( ? [X0,X1] :
( aElementOf0(X0,slsdtgt0(xa))
& aElementOf0(X1,slsdtgt0(xb))
& sdtpldt0(X0,X1) = smndt0(sdtasdt0(xq,xu)) )
| aElementOf0(smndt0(sdtasdt0(xq,xu)),xI) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f53,negated_conjecture,
~ ( ? [X0,X1] :
( aElementOf0(X0,slsdtgt0(xa))
& aElementOf0(X1,slsdtgt0(xb))
& sdtpldt0(X0,X1) = smndt0(sdtasdt0(xq,xu)) )
| aElementOf0(smndt0(sdtasdt0(xq,xu)),xI) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f55,plain,
( aSet0(xI)
& ! [X0] :
( aElementOf0(X0,xI)
=> ( ! [X1] :
( aElementOf0(X1,xI)
=> aElementOf0(sdtpldt0(X0,X1),xI) )
& ! [X2] :
( aElement0(X2)
=> aElementOf0(sdtasdt0(X2,X0),xI) ) ) )
& aIdeal0(xI)
& ! [X3] :
( aElementOf0(X3,slsdtgt0(xa))
<=> ? [X4] :
( aElement0(X4)
& sdtasdt0(xa,X4) = X3 ) )
& ! [X5] :
( aElementOf0(X5,slsdtgt0(xb))
<=> ? [X6] :
( aElement0(X6)
& sdtasdt0(xb,X6) = X5 ) )
& ! [X7] :
( aElementOf0(X7,xI)
<=> ? [X8,X9] :
( aElementOf0(X8,slsdtgt0(xa))
& aElementOf0(X9,slsdtgt0(xb))
& sdtpldt0(X8,X9) = X7 ) )
& xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ),
inference(rectify,[],[f42]) ).
fof(f58,plain,
( ? [X0,X1] :
( aElementOf0(X0,slsdtgt0(xa))
& aElementOf0(X1,slsdtgt0(xb))
& sdtpldt0(X0,X1) = xu )
& aElementOf0(xu,xI)
& xu != sz00
& ! [X2] :
( ( ( ? [X3,X4] :
( aElementOf0(X3,slsdtgt0(xa))
& aElementOf0(X4,slsdtgt0(xb))
& sdtpldt0(X3,X4) = X2 )
| aElementOf0(X2,xI) )
& sz00 != X2 )
=> ~ iLess0(sbrdtbr0(X2),sbrdtbr0(xu)) ) ),
inference(rectify,[],[f45]) ).
fof(f63,plain,
! [X0] :
( aIdeal0(X0)
<=> ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,X0)
=> ( ! [X2] :
( aElementOf0(X2,X0)
=> aElementOf0(sdtpldt0(X1,X2),X0) )
& ! [X3] :
( aElement0(X3)
=> aElementOf0(sdtasdt0(X3,X1),X0) ) ) ) ) ),
inference(rectify,[],[f24]) ).
fof(f71,plain,
( aSet0(xI)
& ! [X0] :
( ( ! [X1] :
( aElementOf0(sdtpldt0(X0,X1),xI)
| ~ aElementOf0(X1,xI) )
& ! [X2] :
( aElementOf0(sdtasdt0(X2,X0),xI)
| ~ aElement0(X2) ) )
| ~ aElementOf0(X0,xI) )
& aIdeal0(xI)
& ! [X3] :
( aElementOf0(X3,slsdtgt0(xa))
<=> ? [X4] :
( aElement0(X4)
& sdtasdt0(xa,X4) = X3 ) )
& ! [X5] :
( aElementOf0(X5,slsdtgt0(xb))
<=> ? [X6] :
( aElement0(X6)
& sdtasdt0(xb,X6) = X5 ) )
& ! [X7] :
( aElementOf0(X7,xI)
<=> ? [X8,X9] :
( aElementOf0(X8,slsdtgt0(xa))
& aElementOf0(X9,slsdtgt0(xb))
& sdtpldt0(X8,X9) = X7 ) )
& xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ),
inference(ennf_transformation,[],[f55]) ).
fof(f72,plain,
( ? [X0,X1] :
( aElementOf0(X0,slsdtgt0(xa))
& aElementOf0(X1,slsdtgt0(xb))
& sdtpldt0(X0,X1) = xu )
& aElementOf0(xu,xI)
& xu != sz00
& ! [X2] :
( ~ iLess0(sbrdtbr0(X2),sbrdtbr0(xu))
| ( ! [X3,X4] :
( ~ aElementOf0(X3,slsdtgt0(xa))
| ~ aElementOf0(X4,slsdtgt0(xb))
| sdtpldt0(X3,X4) != X2 )
& ~ aElementOf0(X2,xI) )
| sz00 = X2 ) ),
inference(ennf_transformation,[],[f58]) ).
fof(f73,plain,
( ? [X0,X1] :
( aElementOf0(X0,slsdtgt0(xa))
& aElementOf0(X1,slsdtgt0(xb))
& sdtpldt0(X0,X1) = xu )
& aElementOf0(xu,xI)
& xu != sz00
& ! [X2] :
( ~ iLess0(sbrdtbr0(X2),sbrdtbr0(xu))
| ( ! [X3,X4] :
( ~ aElementOf0(X3,slsdtgt0(xa))
| ~ aElementOf0(X4,slsdtgt0(xb))
| sdtpldt0(X3,X4) != X2 )
& ~ aElementOf0(X2,xI) )
| sz00 = X2 ) ),
inference(flattening,[],[f72]) ).
fof(f76,plain,
( ! [X0,X1] :
( ~ aElementOf0(X0,slsdtgt0(xa))
| ~ aElementOf0(X1,slsdtgt0(xb))
| sdtpldt0(X0,X1) != smndt0(sdtasdt0(xq,xu)) )
& ~ aElementOf0(smndt0(sdtasdt0(xq,xu)),xI) ),
inference(ennf_transformation,[],[f53]) ).
fof(f103,plain,
! [X0] :
( aIdeal0(X0)
<=> ( aSet0(X0)
& ! [X1] :
( ( ! [X2] :
( aElementOf0(sdtpldt0(X1,X2),X0)
| ~ aElementOf0(X2,X0) )
& ! [X3] :
( aElementOf0(sdtasdt0(X3,X1),X0)
| ~ aElement0(X3) ) )
| ~ aElementOf0(X1,X0) ) ) ),
inference(ennf_transformation,[],[f63]) ).
fof(f113,plain,
! [X0] :
( ! [X1] :
( aElement0(X1)
| ~ aElementOf0(X1,X0) )
| ~ aSet0(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f123,plain,
! [X0] :
( ( sdtasdt0(smndt0(sz10),X0) = smndt0(X0)
& smndt0(X0) = sdtasdt0(X0,smndt0(sz10)) )
| ~ aElement0(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f124,plain,
! [X0] :
( aElement0(smndt0(X0))
| ~ aElement0(X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f140,plain,
( aSet0(xI)
& ! [X0] :
( ( ! [X1] :
( aElementOf0(sdtpldt0(X0,X1),xI)
| ~ aElementOf0(X1,xI) )
& ! [X2] :
( aElementOf0(sdtasdt0(X2,X0),xI)
| ~ aElement0(X2) ) )
| ~ aElementOf0(X0,xI) )
& aIdeal0(xI)
& ! [X3] :
( ( aElementOf0(X3,slsdtgt0(xa))
| ! [X4] :
( ~ aElement0(X4)
| sdtasdt0(xa,X4) != X3 ) )
& ( ? [X4] :
( aElement0(X4)
& sdtasdt0(xa,X4) = X3 )
| ~ aElementOf0(X3,slsdtgt0(xa)) ) )
& ! [X5] :
( ( aElementOf0(X5,slsdtgt0(xb))
| ! [X6] :
( ~ aElement0(X6)
| sdtasdt0(xb,X6) != X5 ) )
& ( ? [X6] :
( aElement0(X6)
& sdtasdt0(xb,X6) = X5 )
| ~ aElementOf0(X5,slsdtgt0(xb)) ) )
& ! [X7] :
( ( aElementOf0(X7,xI)
| ! [X8,X9] :
( ~ aElementOf0(X8,slsdtgt0(xa))
| ~ aElementOf0(X9,slsdtgt0(xb))
| sdtpldt0(X8,X9) != X7 ) )
& ( ? [X8,X9] :
( aElementOf0(X8,slsdtgt0(xa))
& aElementOf0(X9,slsdtgt0(xb))
& sdtpldt0(X8,X9) = X7 )
| ~ aElementOf0(X7,xI) ) )
& xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ),
inference(nnf_transformation,[],[f71]) ).
fof(f141,plain,
( aSet0(xI)
& ! [X0] :
( ( ! [X1] :
( aElementOf0(sdtpldt0(X0,X1),xI)
| ~ aElementOf0(X1,xI) )
& ! [X2] :
( aElementOf0(sdtasdt0(X2,X0),xI)
| ~ aElement0(X2) ) )
| ~ aElementOf0(X0,xI) )
& aIdeal0(xI)
& ! [X3] :
( ( aElementOf0(X3,slsdtgt0(xa))
| ! [X4] :
( ~ aElement0(X4)
| sdtasdt0(xa,X4) != X3 ) )
& ( ? [X5] :
( aElement0(X5)
& sdtasdt0(xa,X5) = X3 )
| ~ aElementOf0(X3,slsdtgt0(xa)) ) )
& ! [X6] :
( ( aElementOf0(X6,slsdtgt0(xb))
| ! [X7] :
( ~ aElement0(X7)
| sdtasdt0(xb,X7) != X6 ) )
& ( ? [X8] :
( aElement0(X8)
& sdtasdt0(xb,X8) = X6 )
| ~ aElementOf0(X6,slsdtgt0(xb)) ) )
& ! [X9] :
( ( aElementOf0(X9,xI)
| ! [X10,X11] :
( ~ aElementOf0(X10,slsdtgt0(xa))
| ~ aElementOf0(X11,slsdtgt0(xb))
| sdtpldt0(X10,X11) != X9 ) )
& ( ? [X12,X13] :
( aElementOf0(X12,slsdtgt0(xa))
& aElementOf0(X13,slsdtgt0(xb))
& sdtpldt0(X12,X13) = X9 )
| ~ aElementOf0(X9,xI) ) )
& xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ),
inference(rectify,[],[f140]) ).
fof(f142,plain,
( aSet0(xI)
& ! [X0] :
( ( ! [X1] :
( aElementOf0(sdtpldt0(X0,X1),xI)
| ~ aElementOf0(X1,xI) )
& ! [X2] :
( aElementOf0(sdtasdt0(X2,X0),xI)
| ~ aElement0(X2) ) )
| ~ aElementOf0(X0,xI) )
& aIdeal0(xI)
& ! [X3] :
( ( aElementOf0(X3,slsdtgt0(xa))
| ! [X4] :
( ~ aElement0(X4)
| sdtasdt0(xa,X4) != X3 ) )
& ( ( aElement0(sK8(X3))
& sdtasdt0(xa,sK8(X3)) = X3 )
| ~ aElementOf0(X3,slsdtgt0(xa)) ) )
& ! [X6] :
( ( aElementOf0(X6,slsdtgt0(xb))
| ! [X7] :
( ~ aElement0(X7)
| sdtasdt0(xb,X7) != X6 ) )
& ( ( aElement0(sK9(X6))
& sdtasdt0(xb,sK9(X6)) = X6 )
| ~ aElementOf0(X6,slsdtgt0(xb)) ) )
& ! [X9] :
( ( aElementOf0(X9,xI)
| ! [X10,X11] :
( ~ aElementOf0(X10,slsdtgt0(xa))
| ~ aElementOf0(X11,slsdtgt0(xb))
| sdtpldt0(X10,X11) != X9 ) )
& ( ( aElementOf0(sK10(X9),slsdtgt0(xa))
& aElementOf0(sK11(X9),slsdtgt0(xb))
& sdtpldt0(sK10(X9),sK11(X9)) = X9 )
| ~ aElementOf0(X9,xI) ) )
& xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10,sK11]),skolemize(X5,sK8(X3)),skolemize(X8,sK9(X6)),skolemize(X12,sK10(X9)),skolemize(X13,sK11(X9))],[f141]) ).
fof(f147,plain,
( aElementOf0(sK21,slsdtgt0(xa))
& aElementOf0(sK22,slsdtgt0(xb))
& xu = sdtpldt0(sK21,sK22)
& aElementOf0(xu,xI)
& xu != sz00
& ! [X2] :
( ~ iLess0(sbrdtbr0(X2),sbrdtbr0(xu))
| ( ! [X3,X4] :
( ~ aElementOf0(X3,slsdtgt0(xa))
| ~ aElementOf0(X4,slsdtgt0(xb))
| sdtpldt0(X3,X4) != X2 )
& ~ aElementOf0(X2,xI) )
| sz00 = X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21,sK22]),skolemize(X0,sK21),skolemize(X1,sK22)],[f73]) ).
fof(f161,plain,
! [X0] :
( ( aIdeal0(X0)
| ~ aSet0(X0)
| ? [X1] :
( ( ? [X2] :
( ~ aElementOf0(sdtpldt0(X1,X2),X0)
& aElementOf0(X2,X0) )
| ? [X3] :
( ~ aElementOf0(sdtasdt0(X3,X1),X0)
& aElement0(X3) ) )
& aElementOf0(X1,X0) ) )
& ( ( aSet0(X0)
& ! [X1] :
( ( ! [X2] :
( aElementOf0(sdtpldt0(X1,X2),X0)
| ~ aElementOf0(X2,X0) )
& ! [X3] :
( aElementOf0(sdtasdt0(X3,X1),X0)
| ~ aElement0(X3) ) )
| ~ aElementOf0(X1,X0) ) )
| ~ aIdeal0(X0) ) ),
inference(nnf_transformation,[],[f103]) ).
fof(f162,plain,
! [X0] :
( ( aIdeal0(X0)
| ~ aSet0(X0)
| ? [X1] :
( ( ? [X2] :
( ~ aElementOf0(sdtpldt0(X1,X2),X0)
& aElementOf0(X2,X0) )
| ? [X3] :
( ~ aElementOf0(sdtasdt0(X3,X1),X0)
& aElement0(X3) ) )
& aElementOf0(X1,X0) ) )
& ( ( aSet0(X0)
& ! [X1] :
( ( ! [X2] :
( aElementOf0(sdtpldt0(X1,X2),X0)
| ~ aElementOf0(X2,X0) )
& ! [X3] :
( aElementOf0(sdtasdt0(X3,X1),X0)
| ~ aElement0(X3) ) )
| ~ aElementOf0(X1,X0) ) )
| ~ aIdeal0(X0) ) ),
inference(flattening,[],[f161]) ).
fof(f163,plain,
! [X0] :
( ( aIdeal0(X0)
| ~ aSet0(X0)
| ? [X1] :
( ( ? [X2] :
( ~ aElementOf0(sdtpldt0(X1,X2),X0)
& aElementOf0(X2,X0) )
| ? [X3] :
( ~ aElementOf0(sdtasdt0(X3,X1),X0)
& aElement0(X3) ) )
& aElementOf0(X1,X0) ) )
& ( ( aSet0(X0)
& ! [X4] :
( ( ! [X5] :
( aElementOf0(sdtpldt0(X4,X5),X0)
| ~ aElementOf0(X5,X0) )
& ! [X6] :
( aElementOf0(sdtasdt0(X6,X4),X0)
| ~ aElement0(X6) ) )
| ~ aElementOf0(X4,X0) ) )
| ~ aIdeal0(X0) ) ),
inference(rectify,[],[f162]) ).
fof(f164,plain,
! [X0] :
( ( aIdeal0(X0)
| ~ aSet0(X0)
| ( ( ( ~ aElementOf0(sdtpldt0(sK34(X0),sK35(X0)),X0)
& aElementOf0(sK35(X0),X0) )
| ( ~ aElementOf0(sdtasdt0(sK36(X0),sK34(X0)),X0)
& aElement0(sK36(X0)) ) )
& aElementOf0(sK34(X0),X0) ) )
& ( ( aSet0(X0)
& ! [X4] :
( ( ! [X5] :
( aElementOf0(sdtpldt0(X4,X5),X0)
| ~ aElementOf0(X5,X0) )
& ! [X6] :
( aElementOf0(sdtasdt0(X6,X4),X0)
| ~ aElement0(X6) ) )
| ~ aElementOf0(X4,X0) ) )
| ~ aIdeal0(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34,sK35,sK36]),skolemize(X1,sK34(X0)),skolemize(X2,sK35(X0)),skolemize(X3,sK36(X0))],[f163]) ).
fof(f219,plain,
aIdeal0(xI),
inference(cnf_transformation,[],[f142]) ).
fof(f222,plain,
aSet0(xI),
inference(cnf_transformation,[],[f142]) ).
fof(f249,plain,
aElementOf0(xu,xI),
inference(cnf_transformation,[],[f147]) ).
fof(f270,plain,
aElement0(xq),
inference(cnf_transformation,[],[f50]) ).
fof(f272,plain,
~ aElementOf0(smndt0(sdtasdt0(xq,xu)),xI),
inference(cnf_transformation,[],[f76]) ).
fof(f309,plain,
! [X0,X6,X4] :
( aElementOf0(sdtasdt0(X6,X4),X0)
| ~ aElement0(X6)
| ~ aElementOf0(X4,X0)
| ~ aIdeal0(X0) ),
inference(cnf_transformation,[],[f164]) ).
fof(f347,plain,
! [X0,X1] :
( ~ aElementOf0(X1,X0)
| aElement0(X1)
| ~ aSet0(X0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f360,plain,
! [X0] :
( smndt0(X0) = sdtasdt0(smndt0(sz10),X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f361,plain,
! [X0] :
( aElement0(smndt0(X0))
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f364,plain,
aElement0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f411,plain,
( ~ aElementOf0(sdtasdt0(smndt0(sz10),sdtasdt0(xq,xu)),xI)
| ~ aElement0(sdtasdt0(xq,xu)) ),
inference(superposition,[],[f272,f360]) ).
fof(f413,definition,
( spl46_6
<=> aElement0(sdtasdt0(xq,xu)) ),
introduced(definition,[new_symbols(definition,[spl46_6])],[avatar_definition]) ).
fof(f415,plain,
( ~ aElement0(sdtasdt0(xq,xu))
| spl46_6 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f417,definition,
( spl46_7
<=> aElementOf0(sdtasdt0(smndt0(sz10),sdtasdt0(xq,xu)),xI) ),
introduced(definition,[new_symbols(definition,[spl46_7])],[avatar_definition]) ).
fof(f419,plain,
( ~ aElementOf0(sdtasdt0(smndt0(sz10),sdtasdt0(xq,xu)),xI)
| spl46_7 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f420,plain,
( ~ spl46_6
| ~ spl46_7 ),
inference(avatar_split_clause,[],[f411,f417,f413]) ).
fof(f492,plain,
( ~ aElement0(smndt0(sz10))
| ~ aElementOf0(sdtasdt0(xq,xu),xI)
| ~ aIdeal0(xI)
| spl46_7 ),
inference(resolution,[],[f419,f309]) ).
fof(f495,plain,
( ~ aElement0(smndt0(sz10))
| ~ aElementOf0(sdtasdt0(xq,xu),xI)
| spl46_7 ),
inference(forward_subsumption_resolution,[],[f492,f219]) ).
fof(f497,definition,
( spl46_17
<=> aElementOf0(sdtasdt0(xq,xu),xI) ),
introduced(definition,[new_symbols(definition,[spl46_17])],[avatar_definition]) ).
fof(f498,plain,
( aElementOf0(sdtasdt0(xq,xu),xI)
| ~ spl46_17 ),
inference(avatar_component_clause,[],[f497]) ).
fof(f499,plain,
( ~ aElementOf0(sdtasdt0(xq,xu),xI)
| spl46_17 ),
inference(avatar_component_clause,[],[f497]) ).
fof(f501,definition,
( spl46_18
<=> aElement0(smndt0(sz10)) ),
introduced(definition,[new_symbols(definition,[spl46_18])],[avatar_definition]) ).
fof(f503,plain,
( ~ aElement0(smndt0(sz10))
| spl46_18 ),
inference(avatar_component_clause,[],[f501]) ).
fof(f504,plain,
( ~ spl46_17
| ~ spl46_18
| spl46_7 ),
inference(avatar_split_clause,[],[f495,f417,f501,f497]) ).
fof(f505,plain,
( ~ aElement0(sz10)
| spl46_18 ),
inference(resolution,[],[f503,f361]) ).
fof(f506,plain,
( $false
| spl46_18 ),
inference(forward_subsumption_resolution,[],[f505,f364]) ).
fof(f507,plain,
spl46_18,
inference(avatar_contradiction_clause,[],[f506]) ).
fof(f509,plain,
( ~ aElement0(xq)
| ~ aElementOf0(xu,xI)
| ~ aIdeal0(xI)
| spl46_17 ),
inference(resolution,[],[f499,f309]) ).
fof(f512,plain,
( ~ aElementOf0(xu,xI)
| ~ aIdeal0(xI)
| spl46_17 ),
inference(forward_subsumption_resolution,[],[f509,f270]) ).
fof(f513,plain,
( ~ aIdeal0(xI)
| spl46_17 ),
inference(forward_subsumption_resolution,[],[f512,f249]) ).
fof(f514,plain,
( $false
| spl46_17 ),
inference(forward_subsumption_resolution,[],[f513,f219]) ).
fof(f515,plain,
spl46_17,
inference(avatar_contradiction_clause,[],[f514]) ).
fof(f516,plain,
( aElement0(sdtasdt0(xq,xu))
| ~ aSet0(xI)
| ~ spl46_17 ),
inference(resolution,[],[f498,f347]) ).
fof(f519,plain,
( ~ aSet0(xI)
| spl46_6
| ~ spl46_17 ),
inference(forward_subsumption_resolution,[],[f516,f415]) ).
fof(f520,plain,
( $false
| spl46_6
| ~ spl46_17 ),
inference(forward_subsumption_resolution,[],[f519,f222]) ).
fof(f521,plain,
( spl46_6
| ~ spl46_17 ),
inference(avatar_contradiction_clause,[],[f520]) ).
cnf(s5,plain,
( ~ spl46_6
| ~ spl46_7 ),
inference(sat_conversion,[],[f420]) ).
cnf(s13,plain,
( spl46_7
| ~ spl46_17
| ~ spl46_18 ),
inference(sat_conversion,[],[f504]) ).
cnf(s14,plain,
spl46_18,
inference(sat_conversion,[],[f507]) ).
cnf(s15,plain,
spl46_17,
inference(sat_conversion,[],[f515]) ).
cnf(s16,plain,
( spl46_6
| ~ spl46_17 ),
inference(sat_conversion,[],[f521]) ).
cnf(s17,plain,
spl46_6,
inference(rat,[],[s16,s15]) ).
cnf(s18,plain,
spl46_7,
inference(rat,[],[s13,s14,s15]) ).
cnf(s20,plain,
$false,
inference(rat,[],[s5,s18,s17]) ).
fof(f522,plain,
$false,
inference(avatar_sat_refutation,[],[s20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG120+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n019.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 23:21:04 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.41 Running first-order theorem proving
% 0.13/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.75/1.19 % (3519095)Detected formulas, will run a generic FOF schedule.
% 3.75/1.19 % (3519105)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2013965925:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.75/1.19 % (3519102)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3109111999:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.75/1.19 % (3519106)dis-21_1_sil=8000:lcm=predicate:random_seed=3499812249:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.75/1.19 % (3519101)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2054553384:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.75/1.19 % (3519104)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1421239418:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.75/1.19 % (3519103)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1919843199:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.75/1.19 % (3519100)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=869081984:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.75/1.19 % (3519105)Instruction limit reached!
% 3.75/1.19 % (3519105)------------------------------
% 3.75/1.19 % (3519105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/1.19 % (3519105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/1.19 % (3519105)CaDiCaL version: 2.1.3
% 3.75/1.19 % (3519105)Termination reason: Instruction limit
% 3.75/1.19 % (3519105)Termination phase: Saturation
% 3.75/1.19 % (3519105)Time elapsed: 0.051 s
% 3.75/1.19 % (3519105)Peak memory usage: 90 MB
% 3.75/1.19 % (3519105)Instructions burned: 142 (million)
% 3.75/1.19 % (3519106)Instruction limit reached!
% 3.75/1.19 % (3519106)------------------------------
% 3.75/1.19 % (3519106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/1.19 % (3519106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/1.19 % (3519106)CaDiCaL version: 2.1.3
% 3.75/1.19 % (3519106)Termination reason: Instruction limit
% 3.75/1.19 % (3519106)Termination phase: Saturation
% 3.75/1.19 % (3519106)Time elapsed: 0.060 s
% 3.75/1.19 % (3519106)Peak memory usage: 89 MB
% 3.75/1.19 % (3519106)Instructions burned: 129 (million)
% 3.75/1.19 % (3519103)Instruction limit reached!
% 3.75/1.19 % (3519103)------------------------------
% 3.75/1.19 % (3519103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/1.19 % (3519103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/1.19 % (3519103)CaDiCaL version: 2.1.3
% 3.75/1.19 % (3519103)Termination reason: Instruction limit
% 3.75/1.19 % (3519103)Termination phase: Saturation
% 3.75/1.19 % (3519103)Time elapsed: 0.066 s
% 3.75/1.19 % (3519103)Peak memory usage: 89 MB
% 3.75/1.19 % (3519103)Instructions burned: 109 (million)
% 3.75/1.19 % (3519104)Instruction limit reached!
% 3.75/1.19 % (3519104)------------------------------
% 3.75/1.19 % (3519104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/1.19 % (3519104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/1.19 % (3519104)CaDiCaL version: 2.1.3
% 3.75/1.19 % (3519104)Termination reason: Instruction limit
% 3.75/1.19 % (3519104)Termination phase: Saturation
% 3.75/1.19 % (3519104)Time elapsed: 0.070 s
% 3.75/1.19 % (3519104)Peak memory usage: 88 MB
% 3.75/1.19 % (3519104)Instructions burned: 119 (million)
% 3.75/1.19 % (3519114)lrs+10_1_sil=8000:sp=occurrence:random_seed=2145208072:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 3.75/1.19 % (3519115)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1946239876:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 3.75/1.19 % (3519114)Instruction limit reached!
% 3.75/1.19 % (3519114)------------------------------
% 3.75/1.19 % (3519114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/1.19 % (3519114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/1.19 % (3519114)CaDiCaL version: 2.1.3
% 3.75/1.19 % (3519114)Termination reason: Instruction limit
% 3.75/1.19 % (3519114)Termination phase: Saturation
% 3.75/1.19 % (3519114)Time elapsed: 0.101 s
% 3.75/1.19 % (3519114)Peak memory usage: 93 MB
% 3.75/1.19 % (3519114)Instructions burned: 287 (million)
% 3.75/1.19 % (3519117)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2541091056:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 3.75/1.19 % (3519116)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1421544379:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 3.75/1.19 % (3519115)Instruction limit reached!
% 3.75/1.19 % (3519115)------------------------------
% 3.75/1.19 % (3519115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/1.19 % (3519115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/1.19 % (3519115)CaDiCaL version: 2.1.3
% 3.75/1.19 % (3519115)Termination reason: Instruction limit
% 3.75/1.19 % (3519115)Termination phase: Saturation
% 3.75/1.19 % (3519115)Time elapsed: 0.081 s
% 3.75/1.19 % (3519115)Peak memory usage: 95 MB
% 3.75/1.19 % (3519115)Instructions burned: 157 (million)
% 3.75/1.19 % (3519121)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2383324389:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 3.75/1.19 % (3519121)First to succeed.
% 3.75/1.19 % (3519121)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3519095"
% 3.75/1.19 % (3519117)Instruction limit reached!
% 3.75/1.19 % (3519117)------------------------------
% 3.75/1.19 % (3519117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/1.19 % (3519117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/1.19 % (3519117)CaDiCaL version: 2.1.3
% 3.75/1.19 % (3519117)Termination reason: Instruction limit
% 3.75/1.19 % (3519117)Termination phase: Saturation
% 3.75/1.19 % (3519117)Time elapsed: 0.117 s
% 3.75/1.19 % (3519117)Peak memory usage: 95 MB
% 3.75/1.19 % (3519117)Instructions burned: 250 (million)
% 3.75/1.19 % (3519123)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3511874253:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 3.75/1.19 % (3519116)Instruction limit reached!
% 3.75/1.19 % (3519116)------------------------------
% 3.75/1.19 % (3519116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/1.19 % (3519116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/1.19 % (3519116)CaDiCaL version: 2.1.3
% 3.75/1.19 % (3519116)Termination reason: Instruction limit
% 3.75/1.19 % (3519116)Termination phase: Saturation
% 3.75/1.19 % (3519116)Time elapsed: 0.206 s
% 3.75/1.19 % (3519116)Peak memory usage: 93 MB
% 3.75/1.19 % (3519116)Instructions burned: 325 (million)
% 3.75/1.19 % (3519121)Refutation found. Thanks to Tanya!
% 3.75/1.19 % SZS status Theorem for theBenchmark
% 3.75/1.19 % SZS output start Proof for theBenchmark
% See solution above
% 4.49/1.39 % (3519121)------------------------------
% 4.49/1.39 % (3519121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.49/1.39 % (3519121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.49/1.39 % (3519121)CaDiCaL version: 2.1.3
% 4.49/1.39 % (3519121)Termination reason: Refutation
% 4.49/1.39 % (3519121)Time elapsed: 0.005 s
% 4.49/1.39 % (3519121)Peak memory usage: 89 MB
% 4.49/1.39 % (3519121)Instructions burned: 14 (million)
% 4.49/1.39 % (3519121)------------------------------
% 4.49/1.39 % (3519121)------------------------------
% 4.49/1.39 % (3519095)Success in time 0.582 s
% 4.49/1.39 % Vampire exiting
%------------------------------------------------------------------------------