%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR002+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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 09:41:55 AM UTC 2026
% Result : Theorem 1.66s 0.81s
% Output : Refutation 2.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 35
% Syntax : Number of formulae : 204 ( 48 unt; 12 def)
% Number of atoms : 594 ( 149 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 653 ( 263 ~; 274 |; 88 &)
% ( 24 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 11 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 10 con; 0-2 aty)
% Number of variables : 199 ( 0 sgn 184 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [X0,X1] :
( ( ~ holdsAt(X0,X1)
& ~ releasedAt(X0,plus(X1,n1))
& ~ ? [X2] :
( happens(X2,X1)
& initiates(X2,X0,X1) ) )
=> ~ holdsAt(X0,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',keep_not_holding) ).
fof(f8,axiom,
! [X0,X1] :
( ( ~ releasedAt(X0,X1)
& ~ ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) )
=> ~ releasedAt(X0,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',keep_not_released) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& terminates(X0,X2,X1) )
=> ~ holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',happens_terminates_not_holds) ).
fof(f12,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& ( initiates(X0,X2,X1)
| terminates(X0,X2,X1) ) )
=> ~ releasedAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',happens_not_released) ).
fof(f13,axiom,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = overflow
& X1 = waterLevel(X3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',initiates_all_defn) ).
fof(f14,axiom,
! [X0,X1,X2] :
( terminates(X0,X1,X2)
<=> ( ( X0 = tapOff
& X1 = filling )
| ( X0 = overflow
& X1 = filling ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',terminates_all_defn) ).
fof(f15,axiom,
! [X0,X1,X2] :
( releases(X0,X1,X2)
<=> ? [X3] :
( X0 = tapOn
& X1 = waterLevel(X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',releases_all_defn) ).
fof(f16,axiom,
! [X0,X1] :
( happens(X0,X1)
<=> ( ( X0 = tapOn
& X1 = n0 )
| ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',happens_all_defn) ).
fof(f21,axiom,
overflow != tapOn,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',overflow_not_tapOn) ).
fof(f22,axiom,
! [X0] : filling != waterLevel(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',filling_not_waterLevel) ).
fof(f27,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus0_1) ).
fof(f30,axiom,
plus(n1,n1) = n2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus1_1) ).
fof(f31,axiom,
plus(n1,n2) = n3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus1_2) ).
fof(f32,axiom,
plus(n1,n3) = n4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus1_3) ).
fof(f36,axiom,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_of_plus) ).
fof(f37,axiom,
! [X0,X1] :
( less_or_equal(X0,X1)
<=> ( less(X0,X1)
| X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_or_equal) ).
fof(f39,axiom,
! [X0] :
( less(X0,n1)
<=> less_or_equal(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less1) ).
fof(f40,axiom,
! [X0] :
( less(X0,n2)
<=> less_or_equal(X0,n1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less2) ).
fof(f41,axiom,
! [X0] :
( less(X0,n3)
<=> less_or_equal(X0,n2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less3) ).
fof(f42,axiom,
! [X0] :
( less(X0,n4)
<=> less_or_equal(X0,n3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less4) ).
fof(f48,axiom,
! [X0,X1] :
( less(X0,X1)
<=> ( ~ less(X1,X0)
& X1 != X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_property) ).
fof(f55,axiom,
holdsAt(waterLevel(n3),n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',waterLevel_3) ).
fof(f56,conjecture,
~ holdsAt(filling,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_filling_4) ).
fof(f57,negated_conjecture,
~ ~ holdsAt(filling,n4),
inference(negated_conjecture,[status(cth)],[f56]) ).
fof(f58,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) )
| ? [X4] :
( holdsAt(waterLevel(X4),X2)
& X0 = overflow
& waterLevel(X4) = X1 ) ) ),
inference(rectify,[],[f13]) ).
fof(f59,plain,
holdsAt(filling,n4),
inference(flattening,[],[f57]) ).
fof(f69,plain,
! [X0,X1] :
( ~ holdsAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ? [X2] :
( happens(X2,X1)
& initiates(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f6]) ).
fof(f70,plain,
! [X0,X1] :
( ~ holdsAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ? [X2] :
( happens(X2,X1)
& initiates(X2,X0,X1) ) ),
inference(flattening,[],[f69]) ).
fof(f73,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f74,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(flattening,[],[f73]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f78,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(flattening,[],[f77]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(flattening,[],[f81]) ).
fof(f88,definition,
! [X2,X0,X1] :
( sP0(X2,X0,X1)
<=> ? [X4] :
( holdsAt(waterLevel(X4),X2)
& X0 = overflow
& waterLevel(X4) = X1 ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f89,definition,
! [X2,X0,X1] :
( sP1(X2,X0,X1)
<=> ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f90,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| sP1(X2,X0,X1)
| sP0(X2,X0,X1) ) ),
inference(definition_folding,[],[f58,f89,f88]) ).
fof(f93,plain,
! [X0,X1] :
( ~ holdsAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ( happens(sK5(X0,X1),X1)
& initiates(sK5(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X2,sK5(X0,X1))],[f70]) ).
fof(f95,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ( happens(sK7(X0,X1),X1)
& releases(sK7(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f74]) ).
fof(f102,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ( ( tapOn != X0
| filling != X1 )
& ( overflow != X0
| spilling != X1 )
& ~ sP1(X2,X0,X1)
& ~ sP0(X2,X0,X1) ) )
& ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| sP1(X2,X0,X1)
| sP0(X2,X0,X1)
| ~ initiates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f90]) ).
fof(f103,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ( ( tapOn != X0
| filling != X1 )
& ( overflow != X0
| spilling != X1 )
& ~ sP1(X2,X0,X1)
& ~ sP0(X2,X0,X1) ) )
& ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| sP1(X2,X0,X1)
| sP0(X2,X0,X1)
| ~ initiates(X0,X1,X2) ) ),
inference(flattening,[],[f102]) ).
fof(f104,plain,
! [X0,X1,X2] :
( ( terminates(X0,X1,X2)
| ( ( tapOff != X0
| filling != X1 )
& ( overflow != X0
| filling != X1 ) ) )
& ( ( X0 = tapOff
& X1 = filling )
| ( X0 = overflow
& X1 = filling )
| ~ terminates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f14]) ).
fof(f105,plain,
! [X0,X1,X2] :
( ( terminates(X0,X1,X2)
| ( ( tapOff != X0
| filling != X1 )
& ( overflow != X0
| filling != X1 ) ) )
& ( ( X0 = tapOff
& X1 = filling )
| ( X0 = overflow
& X1 = filling )
| ~ terminates(X0,X1,X2) ) ),
inference(flattening,[],[f104]) ).
fof(f106,plain,
! [X0,X1,X2] :
( ( releases(X0,X1,X2)
| ! [X3] :
( tapOn != X0
| waterLevel(X3) != X1 ) )
& ( ? [X3] :
( X0 = tapOn
& X1 = waterLevel(X3) )
| ~ releases(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f15]) ).
fof(f107,plain,
! [X0,X1,X2] :
( ( releases(X0,X1,X2)
| ! [X3] :
( tapOn != X0
| waterLevel(X3) != X1 ) )
& ( ? [X4] :
( X0 = tapOn
& waterLevel(X4) = X1 )
| ~ releases(X0,X1,X2) ) ),
inference(rectify,[],[f106]) ).
fof(f108,plain,
! [X0,X1,X2] :
( ( releases(X0,X1,X2)
| ! [X3] :
( tapOn != X0
| waterLevel(X3) != X1 ) )
& ( ( X0 = tapOn
& waterLevel(sK10(X0,X1)) = X1 )
| ~ releases(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X4,sK10(X0,X1))],[f107]) ).
fof(f109,plain,
! [X0,X1] :
( ( happens(X0,X1)
| ( ( tapOn != X0
| n0 != X1 )
& ( ~ holdsAt(waterLevel(n3),X1)
| ~ holdsAt(filling,X1)
| overflow != X0 ) ) )
& ( ( X0 = tapOn
& X1 = n0 )
| ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow )
| ~ happens(X0,X1) ) ),
inference(nnf_transformation,[],[f16]) ).
fof(f110,plain,
! [X0,X1] :
( ( happens(X0,X1)
| ( ( tapOn != X0
| n0 != X1 )
& ( ~ holdsAt(waterLevel(n3),X1)
| ~ holdsAt(filling,X1)
| overflow != X0 ) ) )
& ( ( X0 = tapOn
& X1 = n0 )
| ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow )
| ~ happens(X0,X1) ) ),
inference(flattening,[],[f109]) ).
fof(f112,plain,
! [X0,X1] :
( ( less_or_equal(X0,X1)
| ( ~ less(X0,X1)
& X0 != X1 ) )
& ( less(X0,X1)
| X0 = X1
| ~ less_or_equal(X0,X1) ) ),
inference(nnf_transformation,[],[f37]) ).
fof(f113,plain,
! [X0,X1] :
( ( less_or_equal(X0,X1)
| ( ~ less(X0,X1)
& X0 != X1 ) )
& ( less(X0,X1)
| X0 = X1
| ~ less_or_equal(X0,X1) ) ),
inference(flattening,[],[f112]) ).
fof(f114,plain,
! [X0] :
( ( less(X0,n1)
| ~ less_or_equal(X0,n0) )
& ( less_or_equal(X0,n0)
| ~ less(X0,n1) ) ),
inference(nnf_transformation,[],[f39]) ).
fof(f115,plain,
! [X0] :
( ( less(X0,n2)
| ~ less_or_equal(X0,n1) )
& ( less_or_equal(X0,n1)
| ~ less(X0,n2) ) ),
inference(nnf_transformation,[],[f40]) ).
fof(f116,plain,
! [X0] :
( ( less(X0,n3)
| ~ less_or_equal(X0,n2) )
& ( less_or_equal(X0,n2)
| ~ less(X0,n3) ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f117,plain,
! [X0] :
( ( less(X0,n4)
| ~ less_or_equal(X0,n3) )
& ( less_or_equal(X0,n3)
| ~ less(X0,n4) ) ),
inference(nnf_transformation,[],[f42]) ).
fof(f123,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(nnf_transformation,[],[f48]) ).
fof(f124,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(flattening,[],[f123]) ).
fof(f133,plain,
! [X0,X1] :
( releasedAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| ~ holdsAt(X0,plus(X1,n1))
| happens(sK5(X0,X1),X1) ),
inference(cnf_transformation,[],[f93]) ).
fof(f136,plain,
! [X0,X1] :
( releases(sK7(X0,X1),X0,X1)
| releasedAt(X0,X1)
| ~ releasedAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f95]) ).
fof(f137,plain,
! [X0,X1] :
( releasedAt(X0,X1)
| ~ releasedAt(X0,plus(X1,n1))
| happens(sK7(X0,X1),X1) ),
inference(cnf_transformation,[],[f95]) ).
fof(f139,plain,
! [X2,X0,X1] :
( ~ happens(X0,X1)
| ~ holdsAt(X2,plus(X1,n1))
| ~ terminates(X0,X2,X1) ),
inference(cnf_transformation,[],[f78]) ).
fof(f142,plain,
! [X2,X0,X1] :
( ~ happens(X0,X1)
| ~ releasedAt(X2,plus(X1,n1))
| ~ initiates(X0,X2,X1) ),
inference(cnf_transformation,[],[f82]) ).
fof(f158,plain,
! [X2,X0,X1] :
( initiates(X0,X1,X2)
| tapOn != X0
| filling != X1 ),
inference(cnf_transformation,[],[f103]) ).
fof(f163,plain,
! [X2,X0,X1] :
( terminates(X0,X1,X2)
| overflow != X0
| filling != X1 ),
inference(cnf_transformation,[],[f105]) ).
fof(f165,plain,
! [X2,X0,X1] :
( ~ releases(X0,X1,X2)
| waterLevel(sK10(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f108]) ).
fof(f166,plain,
! [X2,X0,X1] :
( ~ releases(X0,X1,X2)
| tapOn = X0 ),
inference(cnf_transformation,[],[f108]) ).
fof(f168,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| overflow = X0
| n0 = X1 ),
inference(cnf_transformation,[],[f110]) ).
fof(f169,plain,
! [X0,X1] :
( holdsAt(filling,X1)
| n0 = X1
| ~ happens(X0,X1) ),
inference(cnf_transformation,[],[f110]) ).
fof(f174,plain,
! [X0,X1] :
( happens(X0,X1)
| ~ holdsAt(waterLevel(n3),X1)
| ~ holdsAt(filling,X1)
| overflow != X0 ),
inference(cnf_transformation,[],[f110]) ).
fof(f175,plain,
! [X0,X1] :
( happens(X0,X1)
| tapOn != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f110]) ).
fof(f180,plain,
tapOn != overflow,
inference(cnf_transformation,[],[f21]) ).
fof(f181,plain,
! [X0] : filling != waterLevel(X0),
inference(cnf_transformation,[],[f22]) ).
fof(f187,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f27]) ).
fof(f190,plain,
n2 = plus(n1,n1),
inference(cnf_transformation,[],[f30]) ).
fof(f191,plain,
n3 = plus(n1,n2),
inference(cnf_transformation,[],[f31]) ).
fof(f192,plain,
plus(n1,n3) = n4,
inference(cnf_transformation,[],[f32]) ).
fof(f196,plain,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[],[f36]) ).
fof(f198,plain,
! [X0,X1] :
( less_or_equal(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f113]) ).
fof(f199,plain,
! [X0,X1] :
( less_or_equal(X0,X1)
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f202,plain,
! [X0] :
( less(X0,n1)
| ~ less_or_equal(X0,n0) ),
inference(cnf_transformation,[],[f114]) ).
fof(f204,plain,
! [X0] :
( less(X0,n2)
| ~ less_or_equal(X0,n1) ),
inference(cnf_transformation,[],[f115]) ).
fof(f206,plain,
! [X0] :
( ~ less_or_equal(X0,n2)
| less(X0,n3) ),
inference(cnf_transformation,[],[f116]) ).
fof(f208,plain,
! [X0] :
( less(X0,n4)
| ~ less_or_equal(X0,n3) ),
inference(cnf_transformation,[],[f117]) ).
fof(f219,plain,
! [X0,X1] :
( X0 != X1
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f124]) ).
fof(f220,plain,
! [X0,X1] :
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f124]) ).
fof(f228,plain,
holdsAt(waterLevel(n3),n3),
inference(cnf_transformation,[],[f55]) ).
fof(f229,plain,
holdsAt(filling,n4),
inference(cnf_transformation,[],[f59]) ).
fof(f234,plain,
! [X2,X1] :
( initiates(tapOn,X1,X2)
| filling != X1 ),
inference(equality_resolution,[],[f158]) ).
fof(f235,plain,
! [X2] : initiates(tapOn,filling,X2),
inference(equality_resolution,[],[f234]) ).
fof(f240,plain,
! [X2,X1] :
( terminates(overflow,X1,X2)
| filling != X1 ),
inference(equality_resolution,[],[f163]) ).
fof(f241,plain,
! [X2] : terminates(overflow,filling,X2),
inference(equality_resolution,[],[f240]) ).
fof(f244,plain,
! [X1] :
( happens(tapOn,X1)
| n0 != X1 ),
inference(equality_resolution,[],[f175]) ).
fof(f245,plain,
happens(tapOn,n0),
inference(equality_resolution,[],[f244]) ).
fof(f246,plain,
! [X1] :
( ~ holdsAt(waterLevel(n3),X1)
| happens(overflow,X1)
| ~ holdsAt(filling,X1) ),
inference(equality_resolution,[],[f174]) ).
fof(f249,plain,
! [X1] : less_or_equal(X1,X1),
inference(equality_resolution,[],[f198]) ).
fof(f250,plain,
! [X1] : ~ less(X1,X1),
inference(equality_resolution,[],[f219]) ).
fof(f270,plain,
( happens(overflow,n3)
| ~ holdsAt(filling,n3) ),
inference(resolution,[],[f246,f228]) ).
fof(f276,definition,
( spl11_1
<=> holdsAt(filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_1])],[avatar_definition]) ).
fof(f278,plain,
( ~ holdsAt(filling,n3)
| spl11_1 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f280,definition,
( spl11_2
<=> happens(overflow,n3) ),
introduced(definition,[new_symbols(definition,[spl11_2])],[avatar_definition]) ).
fof(f282,plain,
( happens(overflow,n3)
| ~ spl11_2 ),
inference(avatar_component_clause,[],[f280]) ).
fof(f283,plain,
( ~ spl11_1
| spl11_2 ),
inference(avatar_split_clause,[],[f270,f280,f276]) ).
fof(f285,plain,
( ! [X0] :
( n0 = n3
| ~ happens(X0,n3) )
| spl11_1 ),
inference(resolution,[],[f278,f169]) ).
fof(f287,definition,
( spl11_3
<=> ! [X0] : ~ happens(X0,n3) ),
introduced(definition,[new_symbols(definition,[spl11_3])],[avatar_definition]) ).
fof(f288,plain,
( ! [X0] : ~ happens(X0,n3)
| ~ spl11_3 ),
inference(avatar_component_clause,[],[f287]) ).
fof(f290,definition,
( spl11_4
<=> n0 = n3 ),
introduced(definition,[new_symbols(definition,[spl11_4])],[avatar_definition]) ).
fof(f292,plain,
( n0 = n3
| ~ spl11_4 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f293,plain,
( spl11_3
| spl11_4
| spl11_1 ),
inference(avatar_split_clause,[],[f285,f276,f290,f287]) ).
fof(f314,plain,
~ less_or_equal(n2,n1),
inference(resolution,[],[f204,f250]) ).
fof(f317,plain,
~ less(n2,n1),
inference(resolution,[],[f314,f199]) ).
fof(f319,plain,
~ less_or_equal(n2,n0),
inference(resolution,[],[f317,f202]) ).
fof(f327,plain,
less(n2,n3),
inference(resolution,[],[f206,f249]) ).
fof(f346,plain,
! [X0] :
( ~ less_or_equal(X0,n3)
| ~ less(n4,X0) ),
inference(resolution,[],[f220,f208]) ).
fof(f367,plain,
n1 = plus(n1,n0),
inference(superposition,[],[f196,f187]) ).
fof(f372,plain,
! [X0,X1] :
( releasedAt(X1,plus(n1,X0))
| holdsAt(X1,X0)
| ~ holdsAt(X1,plus(n1,X0))
| happens(sK5(X1,X0),X0) ),
inference(superposition,[],[f133,f196]) ).
fof(f575,plain,
! [X0] :
( ~ releasedAt(X0,plus(n0,n1))
| ~ initiates(tapOn,X0,n0) ),
inference(resolution,[],[f142,f245]) ).
fof(f576,plain,
! [X0] :
( ~ releasedAt(X0,n1)
| ~ initiates(tapOn,X0,n0) ),
inference(forward_demodulation,[],[f575,f187]) ).
fof(f619,definition,
( spl11_32
<=> releasedAt(filling,n1) ),
introduced(definition,[new_symbols(definition,[spl11_32])],[avatar_definition]) ).
fof(f620,plain,
( releasedAt(filling,n1)
| ~ spl11_32 ),
inference(avatar_component_clause,[],[f619]) ).
fof(f621,plain,
( ~ releasedAt(filling,n1)
| spl11_32 ),
inference(avatar_component_clause,[],[f619]) ).
fof(f642,definition,
( spl11_36
<=> releasedAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl11_36])],[avatar_definition]) ).
fof(f643,plain,
( releasedAt(filling,n2)
| ~ spl11_36 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f644,plain,
( ~ releasedAt(filling,n2)
| spl11_36 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f663,definition,
( spl11_39
<=> happens(sK7(filling,n2),n2) ),
introduced(definition,[new_symbols(definition,[spl11_39])],[avatar_definition]) ).
fof(f665,plain,
( happens(sK7(filling,n2),n2)
| ~ spl11_39 ),
inference(avatar_component_clause,[],[f663]) ).
fof(f667,definition,
( spl11_40
<=> releasedAt(filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_40])],[avatar_definition]) ).
fof(f668,plain,
( releasedAt(filling,n3)
| ~ spl11_40 ),
inference(avatar_component_clause,[],[f667]) ).
fof(f669,plain,
( ~ releasedAt(filling,n3)
| spl11_40 ),
inference(avatar_component_clause,[],[f667]) ).
fof(f671,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| waterLevel(sK10(sK7(X0,X1),X0)) = X0 ),
inference(resolution,[],[f136,f165]) ).
fof(f672,plain,
! [X0,X1] :
( tapOn = sK7(X0,X1)
| ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1) ),
inference(resolution,[],[f136,f166]) ).
fof(f678,plain,
( ~ releasedAt(filling,plus(n3,n1))
| happens(sK7(filling,n3),n3)
| spl11_40 ),
inference(resolution,[],[f669,f137]) ).
fof(f679,plain,
( ~ releasedAt(filling,plus(n3,n1))
| ~ spl11_3
| spl11_40 ),
inference(forward_subsumption_resolution,[],[f678,f288]) ).
fof(f680,plain,
( ~ releasedAt(filling,plus(n1,n3))
| ~ spl11_3
| spl11_40 ),
inference(forward_demodulation,[],[f679,f196]) ).
fof(f681,plain,
( ~ releasedAt(filling,n4)
| ~ spl11_3
| spl11_40 ),
inference(forward_demodulation,[],[f680,f192]) ).
fof(f847,plain,
! [X0] :
( ~ less(X0,n3)
| ~ less(n4,X0) ),
inference(resolution,[],[f346,f199]) ).
fof(f939,definition,
( spl11_56
<=> n0 = n2 ),
introduced(definition,[new_symbols(definition,[spl11_56])],[avatar_definition]) ).
fof(f940,plain,
( n0 != n2
| spl11_56 ),
inference(avatar_component_clause,[],[f939]) ).
fof(f941,plain,
( n0 = n2
| ~ spl11_56 ),
inference(avatar_component_clause,[],[f939]) ).
fof(f1246,plain,
( ~ initiates(tapOn,filling,n0)
| ~ spl11_32 ),
inference(resolution,[],[f620,f576]) ).
fof(f1249,plain,
( $false
| ~ spl11_32 ),
inference(forward_subsumption_resolution,[],[f1246,f235]) ).
fof(f1250,plain,
~ spl11_32,
inference(avatar_contradiction_clause,[],[f1249]) ).
fof(f1377,plain,
! [X0] :
( ~ releasedAt(X0,n2)
| releasedAt(X0,n1)
| waterLevel(sK10(sK7(X0,n1),X0)) = X0 ),
inference(superposition,[],[f671,f190]) ).
fof(f1396,plain,
! [X0] :
( releasedAt(X0,n4)
| holdsAt(X0,n3)
| ~ holdsAt(X0,n4)
| happens(sK5(X0,n3),n3) ),
inference(superposition,[],[f372,f192]) ).
fof(f1400,plain,
( ! [X0] :
( releasedAt(X0,n4)
| holdsAt(X0,n3)
| ~ holdsAt(X0,n4) )
| ~ spl11_3 ),
inference(forward_subsumption_resolution,[],[f1396,f288]) ).
fof(f1759,plain,
~ less(n4,n2),
inference(resolution,[],[f847,f327]) ).
fof(f1761,plain,
~ less_or_equal(n4,n1),
inference(resolution,[],[f1759,f204]) ).
fof(f1846,definition,
( spl11_98
<=> n1 = n4 ),
introduced(definition,[new_symbols(definition,[spl11_98])],[avatar_definition]) ).
fof(f1848,plain,
( n1 = n4
| ~ spl11_98 ),
inference(avatar_component_clause,[],[f1846]) ).
fof(f1870,plain,
( holdsAt(filling,n3)
| ~ holdsAt(filling,n4)
| ~ spl11_3
| spl11_40 ),
inference(resolution,[],[f1400,f681]) ).
fof(f1873,plain,
( ~ holdsAt(filling,n4)
| spl11_1
| ~ spl11_3
| spl11_40 ),
inference(forward_subsumption_resolution,[],[f1870,f278]) ).
fof(f1883,plain,
( $false
| spl11_1
| ~ spl11_3
| spl11_40 ),
inference(forward_subsumption_resolution,[],[f1873,f229]) ).
fof(f1884,plain,
( spl11_1
| ~ spl11_3
| spl11_40 ),
inference(avatar_contradiction_clause,[],[f1883]) ).
fof(f1959,plain,
( n4 = plus(n1,n0)
| ~ spl11_4 ),
inference(superposition,[],[f192,f292]) ).
fof(f2021,plain,
( n1 = n4
| ~ spl11_4 ),
inference(forward_demodulation,[],[f1959,f367]) ).
fof(f2024,plain,
( spl11_98
| ~ spl11_4 ),
inference(avatar_split_clause,[],[f2021,f290,f1846]) ).
fof(f3107,plain,
( ~ less_or_equal(n1,n1)
| ~ spl11_98 ),
inference(superposition,[],[f1761,f1848]) ).
fof(f3121,plain,
( $false
| ~ spl11_98 ),
inference(forward_subsumption_resolution,[],[f3107,f249]) ).
fof(f3122,plain,
~ spl11_98,
inference(avatar_contradiction_clause,[],[f3121]) ).
fof(f3555,plain,
( happens(tapOn,n2)
| ~ releasedAt(filling,plus(n2,n1))
| releasedAt(filling,n2)
| ~ spl11_39 ),
inference(superposition,[],[f665,f672]) ).
fof(f3556,plain,
( happens(tapOn,n2)
| ~ releasedAt(filling,plus(n2,n1))
| spl11_36
| ~ spl11_39 ),
inference(forward_subsumption_resolution,[],[f3555,f644]) ).
fof(f3588,plain,
( ~ releasedAt(filling,plus(n1,n2))
| happens(tapOn,n2)
| spl11_36
| ~ spl11_39 ),
inference(forward_demodulation,[],[f3556,f196]) ).
fof(f3594,plain,
( ~ releasedAt(filling,n3)
| happens(tapOn,n2)
| spl11_36
| ~ spl11_39 ),
inference(forward_demodulation,[],[f3588,f191]) ).
fof(f3595,plain,
( happens(tapOn,n2)
| spl11_36
| ~ spl11_39
| ~ spl11_40 ),
inference(forward_subsumption_resolution,[],[f3594,f668]) ).
fof(f3597,plain,
( releasedAt(filling,n1)
| filling = waterLevel(sK10(sK7(filling,n1),filling))
| ~ spl11_36 ),
inference(resolution,[],[f643,f1377]) ).
fof(f3600,plain,
( filling = waterLevel(sK10(sK7(filling,n1),filling))
| spl11_32
| ~ spl11_36 ),
inference(forward_subsumption_resolution,[],[f3597,f621]) ).
fof(f3602,plain,
( $false
| spl11_32
| ~ spl11_36 ),
inference(forward_subsumption_resolution,[],[f3600,f181]) ).
fof(f3603,plain,
( spl11_32
| ~ spl11_36 ),
inference(avatar_contradiction_clause,[],[f3602]) ).
fof(f3609,plain,
( ~ releasedAt(filling,plus(n2,n1))
| happens(sK7(filling,n2),n2)
| spl11_36 ),
inference(resolution,[],[f644,f137]) ).
fof(f3610,plain,
( ~ releasedAt(filling,plus(n1,n2))
| happens(sK7(filling,n2),n2)
| spl11_36 ),
inference(forward_demodulation,[],[f3609,f196]) ).
fof(f3611,plain,
( ~ releasedAt(filling,n3)
| happens(sK7(filling,n2),n2)
| spl11_36 ),
inference(forward_demodulation,[],[f3610,f191]) ).
fof(f3612,plain,
( happens(sK7(filling,n2),n2)
| spl11_36
| ~ spl11_40 ),
inference(forward_subsumption_resolution,[],[f3611,f668]) ).
fof(f3613,plain,
( spl11_39
| spl11_36
| ~ spl11_40 ),
inference(avatar_split_clause,[],[f3612,f667,f642,f663]) ).
fof(f3625,plain,
( ~ less_or_equal(n0,n0)
| ~ spl11_56 ),
inference(superposition,[],[f319,f941]) ).
fof(f3670,plain,
( $false
| ~ spl11_56 ),
inference(forward_subsumption_resolution,[],[f3625,f249]) ).
fof(f3671,plain,
~ spl11_56,
inference(avatar_contradiction_clause,[],[f3670]) ).
fof(f3878,plain,
( tapOn = overflow
| n0 = n2
| spl11_36
| ~ spl11_39
| ~ spl11_40 ),
inference(resolution,[],[f3595,f168]) ).
fof(f3888,plain,
( n0 = n2
| spl11_36
| ~ spl11_39
| ~ spl11_40 ),
inference(forward_subsumption_resolution,[],[f3878,f180]) ).
fof(f3896,plain,
( $false
| spl11_36
| ~ spl11_39
| ~ spl11_40
| spl11_56 ),
inference(forward_subsumption_resolution,[],[f3888,f940]) ).
fof(f3897,plain,
( spl11_36
| ~ spl11_39
| ~ spl11_40
| spl11_56 ),
inference(avatar_contradiction_clause,[],[f3896]) ).
fof(f3937,plain,
( ! [X0] :
( ~ holdsAt(X0,plus(n3,n1))
| ~ terminates(overflow,X0,n3) )
| ~ spl11_2 ),
inference(resolution,[],[f282,f139]) ).
fof(f3952,plain,
( ! [X0] :
( ~ holdsAt(X0,plus(n1,n3))
| ~ terminates(overflow,X0,n3) )
| ~ spl11_2 ),
inference(forward_demodulation,[],[f3937,f196]) ).
fof(f3957,plain,
( ! [X0] :
( ~ terminates(overflow,X0,n3)
| ~ holdsAt(X0,n4) )
| ~ spl11_2 ),
inference(forward_demodulation,[],[f3952,f192]) ).
fof(f3981,plain,
( ~ holdsAt(filling,n4)
| ~ spl11_2 ),
inference(resolution,[],[f3957,f241]) ).
fof(f3982,plain,
( $false
| ~ spl11_2 ),
inference(forward_subsumption_resolution,[],[f3981,f229]) ).
fof(f3983,plain,
~ spl11_2,
inference(avatar_contradiction_clause,[],[f3982]) ).
cnf(s1,plain,
( ~ spl11_1
| spl11_2 ),
inference(sat_conversion,[],[f283]) ).
cnf(s2,plain,
( spl11_1
| spl11_3
| spl11_4 ),
inference(sat_conversion,[],[f293]) ).
cnf(s82,plain,
~ spl11_32,
inference(sat_conversion,[],[f1250]) ).
cnf(s153,plain,
( spl11_1
| ~ spl11_3
| spl11_40 ),
inference(sat_conversion,[],[f1884]) ).
cnf(s170,plain,
( ~ spl11_4
| spl11_98 ),
inference(sat_conversion,[],[f2024]) ).
cnf(s317,plain,
~ spl11_98,
inference(sat_conversion,[],[f3122]) ).
cnf(s369,plain,
( spl11_32
| ~ spl11_36 ),
inference(sat_conversion,[],[f3603]) ).
cnf(s370,plain,
( spl11_36
| spl11_39
| ~ spl11_40 ),
inference(sat_conversion,[],[f3613]) ).
cnf(s375,plain,
~ spl11_56,
inference(sat_conversion,[],[f3671]) ).
cnf(s410,plain,
( spl11_36
| ~ spl11_39
| ~ spl11_40
| spl11_56 ),
inference(sat_conversion,[],[f3897]) ).
cnf(s422,plain,
~ spl11_2,
inference(sat_conversion,[],[f3983]) ).
cnf(s439,plain,
~ spl11_4,
inference(rat,[],[s170,s317]) ).
cnf(s476,plain,
~ spl11_36,
inference(rat,[],[s369,s82]) ).
cnf(s503,plain,
( spl11_1
| spl11_3 ),
inference(rat,[],[s2,s439]) ).
cnf(s504,plain,
~ spl11_1,
inference(rat,[],[s1,s422]) ).
cnf(s505,plain,
spl11_3,
inference(rat,[],[s503,s504]) ).
cnf(s507,plain,
spl11_40,
inference(rat,[],[s153,s504,s505]) ).
cnf(s509,plain,
~ spl11_39,
inference(rat,[],[s410,s375,s476,s507]) ).
cnf(s510,plain,
$false,
inference(rat,[],[s370,s476,s507,s509]) ).
fof(f3984,plain,
$false,
inference(avatar_sat_refutation,[],[s510]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR002+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n014.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 22:05:00 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.66/0.81 % (2234196)Detected formulas, will run a generic FOF schedule.
% 1.66/0.81 % (2234218)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2560369071:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 1.66/0.81 % (2234212)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=250891864:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 1.66/0.81 % (2234217)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2525703172:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 1.66/0.81 % (2234216)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=166523492:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 1.66/0.81 % (2234213)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=3502687338:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 1.66/0.81 % (2234219)dis-21_1_sil=8000:lcm=predicate:random_seed=1916489388: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)
% 1.66/0.81 % (2234214)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=3600490335:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 1.66/0.81 % (2234216)Refutation not found, incomplete strategy
% 1.66/0.81 % (2234216)------------------------------
% 1.66/0.81 % (2234216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.66/0.81 % (2234216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.66/0.81 % (2234216)CaDiCaL version: 2.1.3
% 1.66/0.81 % (2234216)Termination reason: Refutation not found, incomplete strategy
% 1.66/0.81 % (2234216)Time elapsed: 0.002 s
% 1.66/0.81 % (2234216)Peak memory usage: 88 MB
% 1.66/0.81 % (2234216)Instructions burned: 1 (million)
% 1.66/0.81 % (2234217)Refutation not found, incomplete strategy
% 1.66/0.81 % (2234217)------------------------------
% 1.66/0.81 % (2234217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.66/0.81 % (2234217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.66/0.81 % (2234217)CaDiCaL version: 2.1.3
% 1.66/0.81 % (2234217)Termination reason: Refutation not found, incomplete strategy
% 1.66/0.81 % (2234217)Time elapsed: 0.007 s
% 1.66/0.81 % (2234217)Peak memory usage: 88 MB
% 1.66/0.81 % (2234217)Instructions burned: 11 (million)
% 1.66/0.81 % (2234218)First to succeed.
% 1.66/0.81 % (2234218)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2234196"
% 1.66/0.81 % (2234219)Instruction limit reached!
% 1.66/0.81 % (2234219)------------------------------
% 1.66/0.81 % (2234219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.66/0.81 % (2234219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.66/0.81 % (2234219)CaDiCaL version: 2.1.3
% 1.66/0.81 % (2234219)Termination reason: Instruction limit
% 1.66/0.81 % (2234219)Termination phase: Saturation
% 1.66/0.81 % (2234219)Time elapsed: 0.088 s
% 1.66/0.81 % (2234219)Peak memory usage: 89 MB
% 1.66/0.81 % (2234219)Instructions burned: 129 (million)
% 1.66/0.81 % (2234218)Refutation found. Thanks to Tanya!
% 1.66/0.81 % SZS status Theorem for theBenchmark
% 1.66/0.81 % SZS output start Proof for theBenchmark
% See solution above
% 2.84/1.01 % (2234218)------------------------------
% 2.84/1.01 % (2234218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.84/1.01 % (2234218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.84/1.01 % (2234218)CaDiCaL version: 2.1.3
% 2.84/1.01 % (2234218)Termination reason: Refutation
% 2.84/1.01 % (2234218)Time elapsed: 0.040 s
% 2.84/1.01 % (2234218)Peak memory usage: 91 MB
% 2.84/1.01 % (2234218)Instructions burned: 99 (million)
% 2.84/1.01 % (2234218)------------------------------
% 2.84/1.01 % (2234218)------------------------------
% 2.84/1.01 % (2234196)Success in time 0.35 s
% 2.84/1.01 % Vampire exiting
%------------------------------------------------------------------------------