%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR001+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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 09:44:18 AM UTC 2026
% Result : Theorem 5.63s 1.07s
% Output : Refutation 5.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 38
% Syntax : Number of formulae : 269 ( 50 unt; 16 def)
% Number of atoms : 855 ( 155 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 923 ( 337 ~; 463 |; 92 &)
% ( 25 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 15 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 10 con; 0-3 aty)
% Number of variables : 281 ( 0 sgn 263 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0,X1] :
( ( holdsAt(X0,X1)
& ~ releasedAt(X0,plus(X1,n1))
& ~ ? [X2] :
( happens(X2,X1)
& terminates(X2,X0,X1) ) )
=> holdsAt(X0,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',keep_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/Axioms/CSR001+0.ax',keep_not_released) ).
fof(f9,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& initiates(X0,X2,X1) )
=> holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_holds) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& terminates(X0,X2,X1) )
=> ~ holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_terminates_not_holds) ).
fof(f11,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& releases(X0,X2,X1) )
=> releasedAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_releases) ).
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/Axioms/CSR001+0.ax',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/Axioms/CSR001+1.ax',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/Axioms/CSR001+1.ax',terminates_all_defn) ).
fof(f15,axiom,
! [X0,X1,X2] :
( releases(X0,X1,X2)
<=> ? [X3] :
( X0 = tapOn
& X1 = waterLevel(X3) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',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/Axioms/CSR001+1.ax',happens_all_defn) ).
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(f38,axiom,
~ ? [X0] : less(X0,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less0) ).
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(f52,axiom,
! [X0] : ~ releasedAt(waterLevel(X0),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_released_waterLevel_0) ).
fof(f55,axiom,
holdsAt(waterLevel(n3),n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',waterLevel_3) ).
fof(f56,conjecture,
holdsAt(waterLevel(n3),n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',waterLevel_4) ).
fof(f57,negated_conjecture,
~ holdsAt(waterLevel(n3),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(waterLevel(n3),n4),
inference(flattening,[],[f57]) ).
fof(f67,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ? [X2] :
( happens(X2,X1)
& terminates(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f68,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ? [X2] :
( happens(X2,X1)
& terminates(X2,X0,X1) ) ),
inference(flattening,[],[f67]) ).
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(f75,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f76,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(flattening,[],[f75]) ).
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(f79,plain,
! [X0,X1,X2] :
( releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ releases(X0,X2,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f80,plain,
! [X0,X1,X2] :
( releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ releases(X0,X2,X1) ),
inference(flattening,[],[f79]) ).
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(f87,plain,
! [X0] : ~ less(X0,n0),
inference(ennf_transformation,[],[f38]) ).
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(f92,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ( happens(sK4(X0,X1),X1)
& terminates(sK4(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X2,sK4(X0,X1))],[f68]) ).
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(f99,plain,
! [X2,X0,X1] :
( ( sP0(X2,X0,X1)
| ! [X4] :
( ~ holdsAt(waterLevel(X4),X2)
| overflow != X0
| waterLevel(X4) != X1 ) )
& ( ? [X4] :
( holdsAt(waterLevel(X4),X2)
& X0 = overflow
& waterLevel(X4) = X1 )
| ~ sP0(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f88]) ).
fof(f100,plain,
! [X0,X1,X2] :
( ( sP0(X0,X1,X2)
| ! [X3] :
( ~ holdsAt(waterLevel(X3),X0)
| overflow != X1
| waterLevel(X3) != X2 ) )
& ( ? [X4] :
( holdsAt(waterLevel(X4),X0)
& overflow = X1
& waterLevel(X4) = X2 )
| ~ sP0(X0,X1,X2) ) ),
inference(rectify,[],[f99]) ).
fof(f101,plain,
! [X0,X1,X2] :
( ( sP0(X0,X1,X2)
| ! [X3] :
( ~ holdsAt(waterLevel(X3),X0)
| overflow != X1
| waterLevel(X3) != X2 ) )
& ( ( holdsAt(waterLevel(sK9(X0,X1,X2)),X0)
& overflow = X1
& waterLevel(sK9(X0,X1,X2)) = X2 )
| ~ sP0(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X4,sK9(X0,X1,X2))],[f100]) ).
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(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(f131,plain,
! [X0,X1] :
( releasedAt(X0,plus(X1,n1))
| happens(sK4(X0,X1),X1)
| ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f92]) ).
fof(f137,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| happens(sK7(X0,X1),X1) ),
inference(cnf_transformation,[],[f95]) ).
fof(f138,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f76]) ).
fof(f139,plain,
! [X2,X0,X1] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(cnf_transformation,[],[f78]) ).
fof(f140,plain,
! [X2,X0,X1] :
( ~ releases(X0,X2,X1)
| ~ happens(X0,X1)
| releasedAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f80]) ).
fof(f142,plain,
! [X2,X0,X1] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(cnf_transformation,[],[f82]) ).
fof(f150,plain,
! [X2,X3,X0,X1] :
( sP0(X0,X1,X2)
| ~ holdsAt(waterLevel(X3),X0)
| overflow != X1
| waterLevel(X3) != X2 ),
inference(cnf_transformation,[],[f101]) ).
fof(f155,plain,
! [X2,X0,X1] :
( ~ sP0(X2,X0,X1)
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f103]) ).
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(f167,plain,
! [X2,X3,X0,X1] :
( releases(X0,X1,X2)
| tapOn != X0
| waterLevel(X3) != X1 ),
inference(cnf_transformation,[],[f108]) ).
fof(f169,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| holdsAt(filling,X1)
| n0 = X1 ),
inference(cnf_transformation,[],[f110]) ).
fof(f170,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| holdsAt(waterLevel(n3),X1)
| n0 = 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(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(f200,plain,
! [X0] : ~ less(X0,n0),
inference(cnf_transformation,[],[f87]) ).
fof(f204,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| less(X0,n2) ),
inference(cnf_transformation,[],[f115]) ).
fof(f206,plain,
! [X0] :
( ~ less_or_equal(X0,n2)
| less(X0,n3) ),
inference(cnf_transformation,[],[f116]) ).
fof(f225,plain,
! [X0] : ~ releasedAt(waterLevel(X0),n0),
inference(cnf_transformation,[],[f52]) ).
fof(f228,plain,
holdsAt(waterLevel(n3),n3),
inference(cnf_transformation,[],[f55]) ).
fof(f229,plain,
~ holdsAt(waterLevel(n3),n4),
inference(cnf_transformation,[],[f59]) ).
fof(f232,plain,
! [X2,X3,X0] :
( sP0(X0,overflow,X2)
| ~ holdsAt(waterLevel(X3),X0)
| waterLevel(X3) != X2 ),
inference(equality_resolution,[],[f150]) ).
fof(f233,plain,
! [X3,X0] :
( sP0(X0,overflow,waterLevel(X3))
| ~ holdsAt(waterLevel(X3),X0) ),
inference(equality_resolution,[],[f232]) ).
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(f242,plain,
! [X2,X3,X1] :
( releases(tapOn,X1,X2)
| waterLevel(X3) != X1 ),
inference(equality_resolution,[],[f167]) ).
fof(f243,plain,
! [X2,X3] : releases(tapOn,waterLevel(X3),X2),
inference(equality_resolution,[],[f242]) ).
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(f351,plain,
! [X0,X1] :
( ~ initiates(X1,X0,n0)
| ~ happens(X1,n0)
| ~ releasedAt(X0,n1) ),
inference(superposition,[],[f142,f187]) ).
fof(f355,plain,
! [X0,X1] :
( ~ initiates(X1,X0,n1)
| ~ happens(X1,n1)
| ~ releasedAt(X0,n2) ),
inference(superposition,[],[f142,f190]) ).
fof(f357,plain,
! [X0,X1] :
( ~ terminates(X1,X0,n1)
| ~ happens(X1,n1)
| ~ holdsAt(X0,n2) ),
inference(superposition,[],[f139,f190]) ).
fof(f416,plain,
less(n1,n2),
inference(resolution,[],[f204,f249]) ).
fof(f454,plain,
less(n2,n3),
inference(resolution,[],[f206,f249]) ).
fof(f2356,plain,
! [X2,X0,X1] :
( ~ releasedAt(X1,plus(n1,X0))
| ~ happens(X2,X0)
| ~ initiates(X2,X1,X0) ),
inference(superposition,[],[f142,f196]) ).
fof(f2406,plain,
( ~ happens(overflow,n1)
| ~ holdsAt(filling,n2) ),
inference(resolution,[],[f357,f241]) ).
fof(f13262,plain,
( happens(overflow,n3)
| ~ holdsAt(filling,n3) ),
inference(resolution,[],[f246,f228]) ).
fof(f13862,plain,
! [X0,X1] :
( initiates(overflow,waterLevel(X0),X1)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(resolution,[],[f155,f233]) ).
fof(f13873,plain,
! [X0] :
( holdsAt(filling,plus(X0,n1))
| ~ happens(tapOn,X0) ),
inference(resolution,[],[f138,f235]) ).
fof(f13878,plain,
! [X0,X1] :
( holdsAt(waterLevel(X1),plus(X0,n1))
| ~ happens(overflow,X0)
| ~ holdsAt(waterLevel(X1),X0) ),
inference(resolution,[],[f138,f13862]) ).
fof(f13883,definition,
( spl11_142
<=> holdsAt(filling,n1) ),
introduced(definition,[new_symbols(definition,[spl11_142])],[avatar_definition]) ).
fof(f13884,plain,
( holdsAt(filling,n1)
| ~ spl11_142 ),
inference(avatar_component_clause,[],[f13883]) ).
fof(f13885,plain,
( ~ holdsAt(filling,n1)
| spl11_142 ),
inference(avatar_component_clause,[],[f13883]) ).
fof(f13918,plain,
( holdsAt(filling,n1)
| ~ happens(tapOn,n0) ),
inference(superposition,[],[f13873,f187]) ).
fof(f13920,plain,
( ~ happens(tapOn,n0)
| spl11_142 ),
inference(forward_subsumption_resolution,[],[f13918,f13885]) ).
fof(f13921,plain,
( $false
| spl11_142 ),
inference(forward_subsumption_resolution,[],[f13920,f245]) ).
fof(f13922,plain,
spl11_142,
inference(avatar_contradiction_clause,[],[f13921]) ).
fof(f13993,definition,
( spl11_151
<=> happens(overflow,n3) ),
introduced(definition,[new_symbols(definition,[spl11_151])],[avatar_definition]) ).
fof(f13994,plain,
( happens(overflow,n3)
| ~ spl11_151 ),
inference(avatar_component_clause,[],[f13993]) ).
fof(f13998,definition,
( spl11_152
<=> holdsAt(filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_152])],[avatar_definition]) ).
fof(f14000,plain,
( ~ holdsAt(filling,n3)
| spl11_152 ),
inference(avatar_component_clause,[],[f13998]) ).
fof(f14001,plain,
( ~ spl11_152
| spl11_151 ),
inference(avatar_split_clause,[],[f13262,f13993,f13998]) ).
fof(f14038,plain,
( ~ happens(tapOn,n0)
| ~ releasedAt(filling,n1) ),
inference(resolution,[],[f351,f235]) ).
fof(f14044,plain,
~ releasedAt(filling,n1),
inference(forward_subsumption_resolution,[],[f14038,f245]) ).
fof(f14065,plain,
! [X0,X1] :
( ~ initiates(X1,X0,n2)
| ~ happens(X1,n2)
| ~ releasedAt(X0,n3) ),
inference(superposition,[],[f2356,f191]) ).
fof(f14077,plain,
! [X0,X1] :
( releasedAt(waterLevel(X1),plus(X0,n1))
| ~ happens(tapOn,X0) ),
inference(resolution,[],[f140,f243]) ).
fof(f14138,plain,
! [X0] :
( releasedAt(waterLevel(X0),n1)
| ~ happens(tapOn,n0) ),
inference(superposition,[],[f14077,f187]) ).
fof(f14140,plain,
! [X0] : releasedAt(waterLevel(X0),n1),
inference(forward_subsumption_resolution,[],[f14138,f245]) ).
fof(f16236,plain,
! [X0] :
( ~ happens(overflow,n1)
| ~ releasedAt(waterLevel(X0),n2)
| ~ holdsAt(waterLevel(X0),n1) ),
inference(resolution,[],[f355,f13862]) ).
fof(f16255,plain,
! [X0] :
( ~ happens(overflow,n2)
| ~ releasedAt(waterLevel(X0),n3)
| ~ holdsAt(waterLevel(X0),n2) ),
inference(resolution,[],[f14065,f13862]) ).
fof(f16389,definition,
( spl11_172
<=> holdsAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl11_172])],[avatar_definition]) ).
fof(f16390,plain,
( holdsAt(filling,n2)
| ~ spl11_172 ),
inference(avatar_component_clause,[],[f16389]) ).
fof(f16391,plain,
( ~ holdsAt(filling,n2)
| spl11_172 ),
inference(avatar_component_clause,[],[f16389]) ).
fof(f16393,definition,
( spl11_173
<=> happens(overflow,n1) ),
introduced(definition,[new_symbols(definition,[spl11_173])],[avatar_definition]) ).
fof(f16395,plain,
( ~ happens(overflow,n1)
| spl11_173 ),
inference(avatar_component_clause,[],[f16393]) ).
fof(f16396,plain,
( ~ spl11_172
| ~ spl11_173 ),
inference(avatar_split_clause,[],[f2406,f16393,f16389]) ).
fof(f16399,definition,
( spl11_174
<=> happens(overflow,n2) ),
introduced(definition,[new_symbols(definition,[spl11_174])],[avatar_definition]) ).
fof(f16401,plain,
( ~ happens(overflow,n2)
| spl11_174 ),
inference(avatar_component_clause,[],[f16399]) ).
fof(f16418,plain,
! [X0,X1] :
( ~ releasedAt(X1,plus(n1,X0))
| releasedAt(X1,X0)
| happens(sK7(X1,X0),X0) ),
inference(superposition,[],[f137,f196]) ).
fof(f16421,plain,
! [X0] :
( happens(sK7(X0,n1),n1)
| releasedAt(X0,n1)
| ~ releasedAt(X0,n2) ),
inference(superposition,[],[f137,f190]) ).
fof(f16880,definition,
( spl11_178
<=> n0 = n1 ),
introduced(definition,[new_symbols(definition,[spl11_178])],[avatar_definition]) ).
fof(f16881,plain,
( n0 != n1
| spl11_178 ),
inference(avatar_component_clause,[],[f16880]) ).
fof(f16882,plain,
( n0 = n1
| ~ spl11_178 ),
inference(avatar_component_clause,[],[f16880]) ).
fof(f16884,definition,
( spl11_179
<=> holdsAt(waterLevel(n3),n1) ),
introduced(definition,[new_symbols(definition,[spl11_179])],[avatar_definition]) ).
fof(f16885,plain,
( ~ holdsAt(waterLevel(n3),n1)
| spl11_179 ),
inference(avatar_component_clause,[],[f16884]) ).
fof(f16886,plain,
( holdsAt(waterLevel(n3),n1)
| ~ spl11_179 ),
inference(avatar_component_clause,[],[f16884]) ).
fof(f16897,plain,
( ! [X0] : ~ releasedAt(waterLevel(X0),n1)
| ~ spl11_178 ),
inference(superposition,[],[f225,f16882]) ).
fof(f16948,plain,
( $false
| ~ spl11_178 ),
inference(forward_subsumption_resolution,[],[f16897,f14140]) ).
fof(f16949,plain,
~ spl11_178,
inference(avatar_contradiction_clause,[],[f16948]) ).
fof(f16955,plain,
( happens(overflow,n1)
| ~ holdsAt(filling,n1)
| ~ spl11_179 ),
inference(resolution,[],[f16886,f246]) ).
fof(f16957,plain,
( ~ holdsAt(filling,n1)
| spl11_173
| ~ spl11_179 ),
inference(forward_subsumption_resolution,[],[f16955,f16395]) ).
fof(f16958,plain,
( $false
| ~ spl11_142
| spl11_173
| ~ spl11_179 ),
inference(forward_subsumption_resolution,[],[f16957,f13884]) ).
fof(f16959,plain,
( ~ spl11_142
| spl11_173
| ~ spl11_179 ),
inference(avatar_contradiction_clause,[],[f16958]) ).
fof(f16998,definition,
( spl11_181
<=> releasedAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl11_181])],[avatar_definition]) ).
fof(f16999,plain,
( releasedAt(filling,n2)
| ~ spl11_181 ),
inference(avatar_component_clause,[],[f16998]) ).
fof(f17000,plain,
( ~ releasedAt(filling,n2)
| spl11_181 ),
inference(avatar_component_clause,[],[f16998]) ).
fof(f17730,definition,
( spl11_194
<=> n0 = n2 ),
introduced(definition,[new_symbols(definition,[spl11_194])],[avatar_definition]) ).
fof(f17731,plain,
( n0 != n2
| spl11_194 ),
inference(avatar_component_clause,[],[f17730]) ).
fof(f17732,plain,
( n0 = n2
| ~ spl11_194 ),
inference(avatar_component_clause,[],[f17730]) ).
fof(f17734,definition,
( spl11_195
<=> holdsAt(waterLevel(n3),n2) ),
introduced(definition,[new_symbols(definition,[spl11_195])],[avatar_definition]) ).
fof(f17735,plain,
( ~ holdsAt(waterLevel(n3),n2)
| spl11_195 ),
inference(avatar_component_clause,[],[f17734]) ).
fof(f17736,plain,
( holdsAt(waterLevel(n3),n2)
| ~ spl11_195 ),
inference(avatar_component_clause,[],[f17734]) ).
fof(f17744,plain,
( less(n1,n0)
| ~ spl11_194 ),
inference(superposition,[],[f416,f17732]) ).
fof(f17846,plain,
( $false
| ~ spl11_194 ),
inference(forward_subsumption_resolution,[],[f17744,f200]) ).
fof(f17847,plain,
~ spl11_194,
inference(avatar_contradiction_clause,[],[f17846]) ).
fof(f17852,plain,
( happens(overflow,n2)
| ~ holdsAt(filling,n2)
| ~ spl11_195 ),
inference(resolution,[],[f17736,f246]) ).
fof(f17856,plain,
( ~ holdsAt(filling,n2)
| spl11_174
| ~ spl11_195 ),
inference(forward_subsumption_resolution,[],[f17852,f16401]) ).
fof(f17857,plain,
( $false
| ~ spl11_172
| spl11_174
| ~ spl11_195 ),
inference(forward_subsumption_resolution,[],[f17856,f16390]) ).
fof(f17858,plain,
( ~ spl11_172
| spl11_174
| ~ spl11_195 ),
inference(avatar_contradiction_clause,[],[f17857]) ).
fof(f17877,definition,
( spl11_197
<=> n0 = n3 ),
introduced(definition,[new_symbols(definition,[spl11_197])],[avatar_definition]) ).
fof(f17878,plain,
( n0 != n3
| spl11_197 ),
inference(avatar_component_clause,[],[f17877]) ).
fof(f17879,plain,
( n0 = n3
| ~ spl11_197 ),
inference(avatar_component_clause,[],[f17877]) ).
fof(f17890,plain,
( less(n2,n0)
| ~ spl11_197 ),
inference(superposition,[],[f454,f17879]) ).
fof(f17994,plain,
( $false
| ~ spl11_197 ),
inference(forward_subsumption_resolution,[],[f17890,f200]) ).
fof(f17995,plain,
~ spl11_197,
inference(avatar_contradiction_clause,[],[f17994]) ).
fof(f18207,plain,
! [X0] :
( happens(sK7(X0,n3),n3)
| releasedAt(X0,n3)
| ~ releasedAt(X0,n4) ),
inference(superposition,[],[f16418,f192]) ).
fof(f18208,plain,
! [X0] :
( happens(sK7(X0,n2),n2)
| releasedAt(X0,n2)
| ~ releasedAt(X0,n3) ),
inference(superposition,[],[f16418,f191]) ).
fof(f18316,plain,
! [X0] :
( releasedAt(X0,n3)
| ~ releasedAt(X0,n4)
| holdsAt(filling,n3)
| n0 = n3 ),
inference(resolution,[],[f18207,f169]) ).
fof(f18322,plain,
( ! [X0] :
( releasedAt(X0,n3)
| ~ releasedAt(X0,n4)
| n0 = n3 )
| spl11_152 ),
inference(forward_subsumption_resolution,[],[f18316,f14000]) ).
fof(f18324,plain,
( ! [X0] :
( ~ releasedAt(X0,n4)
| releasedAt(X0,n3) )
| spl11_152
| spl11_197 ),
inference(forward_subsumption_resolution,[],[f18322,f17878]) ).
fof(f18329,plain,
! [X0] :
( releasedAt(X0,n2)
| ~ releasedAt(X0,n3)
| holdsAt(filling,n2)
| n0 = n2 ),
inference(resolution,[],[f18208,f169]) ).
fof(f18330,plain,
! [X0] :
( releasedAt(X0,n2)
| ~ releasedAt(X0,n3)
| holdsAt(waterLevel(n3),n2)
| n0 = n2 ),
inference(resolution,[],[f18208,f170]) ).
fof(f18352,plain,
! [X0,X1] :
( holdsAt(waterLevel(X1),plus(n1,X0))
| ~ happens(overflow,X0)
| ~ holdsAt(waterLevel(X1),X0) ),
inference(superposition,[],[f13878,f196]) ).
fof(f21515,plain,
! [X0,X1] :
( releasedAt(X1,plus(n1,X0))
| happens(sK4(X1,X0),X0)
| ~ holdsAt(X1,X0)
| holdsAt(X1,plus(n1,X0)) ),
inference(superposition,[],[f131,f196]) ).
fof(f21518,plain,
! [X0] :
( happens(sK4(X0,n1),n1)
| releasedAt(X0,n2)
| ~ holdsAt(X0,n1)
| holdsAt(X0,n2) ),
inference(superposition,[],[f131,f190]) ).
fof(f22141,plain,
( ! [X0] :
( releasedAt(X0,n2)
| ~ releasedAt(X0,n3)
| holdsAt(waterLevel(n3),n2) )
| spl11_194 ),
inference(forward_subsumption_resolution,[],[f18330,f17731]) ).
fof(f22149,plain,
( ! [X0] :
( releasedAt(X0,n2)
| ~ releasedAt(X0,n3)
| holdsAt(filling,n2) )
| spl11_194 ),
inference(forward_subsumption_resolution,[],[f18329,f17731]) ).
fof(f22604,plain,
! [X0] :
( releasedAt(X0,n2)
| ~ holdsAt(X0,n1)
| holdsAt(X0,n2)
| holdsAt(waterLevel(n3),n1)
| n0 = n1 ),
inference(resolution,[],[f21518,f170]) ).
fof(f22623,plain,
( ! [X0] :
( releasedAt(X0,n2)
| ~ holdsAt(X0,n1)
| holdsAt(X0,n2)
| holdsAt(waterLevel(n3),n1) )
| spl11_178 ),
inference(forward_subsumption_resolution,[],[f22604,f16881]) ).
fof(f22642,plain,
( ! [X0] :
( ~ holdsAt(X0,n1)
| releasedAt(X0,n2)
| holdsAt(X0,n2) )
| spl11_178
| spl11_179 ),
inference(forward_subsumption_resolution,[],[f22623,f16885]) ).
fof(f22643,plain,
( releasedAt(filling,n2)
| holdsAt(filling,n2)
| ~ spl11_142
| spl11_178
| spl11_179 ),
inference(resolution,[],[f22642,f13884]) ).
fof(f22651,plain,
( holdsAt(filling,n2)
| ~ spl11_142
| spl11_178
| spl11_179
| spl11_181 ),
inference(forward_subsumption_resolution,[],[f22643,f17000]) ).
fof(f22652,plain,
( $false
| ~ spl11_142
| spl11_172
| spl11_178
| spl11_179
| spl11_181 ),
inference(forward_subsumption_resolution,[],[f22651,f16391]) ).
fof(f22653,plain,
( ~ spl11_142
| spl11_172
| spl11_178
| spl11_179
| spl11_181 ),
inference(avatar_contradiction_clause,[],[f22652]) ).
fof(f22658,plain,
( ! [X0] :
( ~ releasedAt(X0,n3)
| releasedAt(X0,n2) )
| spl11_172
| spl11_194 ),
inference(forward_subsumption_resolution,[],[f22149,f16391]) ).
fof(f22774,plain,
! [X0] :
( releasedAt(X0,n1)
| ~ releasedAt(X0,n2)
| holdsAt(waterLevel(n3),n1)
| n0 = n1 ),
inference(resolution,[],[f16421,f170]) ).
fof(f22780,plain,
( ! [X0] :
( releasedAt(X0,n1)
| ~ releasedAt(X0,n2)
| n0 = n1 )
| spl11_179 ),
inference(forward_subsumption_resolution,[],[f22774,f16885]) ).
fof(f22782,plain,
( ! [X0] :
( ~ releasedAt(X0,n2)
| releasedAt(X0,n1) )
| spl11_178
| spl11_179 ),
inference(forward_subsumption_resolution,[],[f22780,f16881]) ).
fof(f22783,plain,
( releasedAt(filling,n1)
| spl11_178
| spl11_179
| ~ spl11_181 ),
inference(resolution,[],[f22782,f16999]) ).
fof(f22787,plain,
( $false
| spl11_178
| spl11_179
| ~ spl11_181 ),
inference(forward_subsumption_resolution,[],[f22783,f14044]) ).
fof(f22788,plain,
( spl11_178
| spl11_179
| ~ spl11_181 ),
inference(avatar_contradiction_clause,[],[f22787]) ).
fof(f22797,definition,
( spl11_260
<=> ! [X0] :
( ~ releasedAt(waterLevel(X0),n2)
| ~ holdsAt(waterLevel(X0),n1) ) ),
introduced(definition,[new_symbols(definition,[spl11_260])],[avatar_definition]) ).
fof(f22798,plain,
( ! [X0] :
( ~ releasedAt(waterLevel(X0),n2)
| ~ holdsAt(waterLevel(X0),n1) )
| ~ spl11_260 ),
inference(avatar_component_clause,[],[f22797]) ).
fof(f22799,plain,
( spl11_260
| ~ spl11_173 ),
inference(avatar_split_clause,[],[f16236,f16393,f22797]) ).
fof(f24180,plain,
! [X0] :
( holdsAt(waterLevel(X0),n4)
| ~ happens(overflow,n3)
| ~ holdsAt(waterLevel(X0),n3) ),
inference(superposition,[],[f18352,f192]) ).
fof(f26364,plain,
! [X0] :
( happens(sK4(X0,n3),n3)
| releasedAt(X0,n4)
| ~ holdsAt(X0,n3)
| holdsAt(X0,n4) ),
inference(superposition,[],[f21515,f192]) ).
fof(f26365,plain,
! [X0] :
( happens(sK4(X0,n2),n2)
| releasedAt(X0,n3)
| ~ holdsAt(X0,n2)
| holdsAt(X0,n3) ),
inference(superposition,[],[f21515,f191]) ).
fof(f26510,plain,
! [X0] :
( releasedAt(X0,n4)
| ~ holdsAt(X0,n3)
| holdsAt(X0,n4)
| holdsAt(filling,n3)
| n0 = n3 ),
inference(resolution,[],[f26364,f169]) ).
fof(f26517,plain,
( ! [X0] :
( releasedAt(X0,n4)
| ~ holdsAt(X0,n3)
| holdsAt(X0,n4)
| n0 = n3 )
| spl11_152 ),
inference(forward_subsumption_resolution,[],[f26510,f14000]) ).
fof(f26519,plain,
( ! [X0] :
( ~ holdsAt(X0,n3)
| releasedAt(X0,n4)
| holdsAt(X0,n4) )
| spl11_152
| spl11_197 ),
inference(forward_subsumption_resolution,[],[f26517,f17878]) ).
fof(f26530,plain,
( releasedAt(waterLevel(n3),n4)
| holdsAt(waterLevel(n3),n4)
| spl11_152
| spl11_197 ),
inference(resolution,[],[f26519,f228]) ).
fof(f26539,plain,
( releasedAt(waterLevel(n3),n4)
| spl11_152
| spl11_197 ),
inference(forward_subsumption_resolution,[],[f26530,f229]) ).
fof(f26546,plain,
( releasedAt(waterLevel(n3),n3)
| spl11_152
| spl11_197 ),
inference(resolution,[],[f26539,f18324]) ).
fof(f26547,plain,
( releasedAt(waterLevel(n3),n2)
| spl11_152
| spl11_172
| spl11_194
| spl11_197 ),
inference(resolution,[],[f26546,f22658]) ).
fof(f26551,plain,
( ~ holdsAt(waterLevel(n3),n1)
| spl11_152
| spl11_172
| spl11_194
| spl11_197
| ~ spl11_260 ),
inference(resolution,[],[f26547,f22798]) ).
fof(f26556,plain,
( $false
| spl11_152
| spl11_172
| ~ spl11_179
| spl11_194
| spl11_197
| ~ spl11_260 ),
inference(forward_subsumption_resolution,[],[f26551,f16886]) ).
fof(f26557,plain,
( spl11_152
| spl11_172
| ~ spl11_179
| spl11_194
| spl11_197
| ~ spl11_260 ),
inference(avatar_contradiction_clause,[],[f26556]) ).
fof(f26559,plain,
( ! [X0] :
( releasedAt(X0,n3)
| ~ releasedAt(X0,n4)
| holdsAt(filling,n3) )
| spl11_197 ),
inference(forward_subsumption_resolution,[],[f18316,f17878]) ).
fof(f26566,plain,
( ! [X0] :
( releasedAt(X0,n4)
| ~ holdsAt(X0,n3)
| holdsAt(X0,n4)
| holdsAt(filling,n3) )
| spl11_197 ),
inference(forward_subsumption_resolution,[],[f26510,f17878]) ).
fof(f26647,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n3)
| holdsAt(waterLevel(X0),n4) )
| ~ spl11_151 ),
inference(forward_subsumption_resolution,[],[f24180,f13994]) ).
fof(f26651,plain,
( holdsAt(waterLevel(n3),n4)
| ~ spl11_151 ),
inference(resolution,[],[f26647,f228]) ).
fof(f26668,plain,
( $false
| ~ spl11_151 ),
inference(forward_subsumption_resolution,[],[f26651,f229]) ).
fof(f26669,plain,
~ spl11_151,
inference(avatar_contradiction_clause,[],[f26668]) ).
fof(f26737,definition,
( spl11_317
<=> ! [X0] :
( ~ releasedAt(waterLevel(X0),n3)
| ~ holdsAt(waterLevel(X0),n2) ) ),
introduced(definition,[new_symbols(definition,[spl11_317])],[avatar_definition]) ).
fof(f26738,plain,
( ! [X0] :
( ~ releasedAt(waterLevel(X0),n3)
| ~ holdsAt(waterLevel(X0),n2) )
| ~ spl11_317 ),
inference(avatar_component_clause,[],[f26737]) ).
fof(f26739,plain,
( spl11_317
| ~ spl11_174 ),
inference(avatar_split_clause,[],[f16255,f16399,f26737]) ).
fof(f26782,plain,
( ! [X0] :
( ~ holdsAt(X0,n3)
| releasedAt(X0,n4)
| holdsAt(X0,n4) )
| spl11_152
| spl11_197 ),
inference(forward_subsumption_resolution,[],[f26566,f14000]) ).
fof(f26792,plain,
( releasedAt(waterLevel(n3),n4)
| holdsAt(waterLevel(n3),n4)
| spl11_152
| spl11_197 ),
inference(resolution,[],[f26782,f228]) ).
fof(f26810,plain,
( releasedAt(waterLevel(n3),n4)
| spl11_152
| spl11_197 ),
inference(forward_subsumption_resolution,[],[f26792,f229]) ).
fof(f26836,plain,
( ! [X0] :
( ~ releasedAt(X0,n4)
| releasedAt(X0,n3) )
| spl11_152
| spl11_197 ),
inference(forward_subsumption_resolution,[],[f26559,f14000]) ).
fof(f26863,plain,
( releasedAt(waterLevel(n3),n3)
| spl11_152
| spl11_197 ),
inference(resolution,[],[f26836,f26810]) ).
fof(f26864,plain,
( ~ holdsAt(waterLevel(n3),n2)
| spl11_152
| spl11_197
| ~ spl11_317 ),
inference(resolution,[],[f26863,f26738]) ).
fof(f26871,plain,
( ~ spl11_195
| spl11_152
| spl11_197
| ~ spl11_317 ),
inference(avatar_split_clause,[],[f26864,f26737,f17877,f13998,f17734]) ).
fof(f26960,plain,
( ! [X0] :
( ~ releasedAt(X0,n3)
| releasedAt(X0,n2) )
| spl11_194
| spl11_195 ),
inference(forward_subsumption_resolution,[],[f22141,f17735]) ).
fof(f27020,plain,
! [X0] :
( releasedAt(X0,n3)
| ~ holdsAt(X0,n2)
| holdsAt(X0,n3)
| holdsAt(waterLevel(n3),n2)
| n0 = n2 ),
inference(resolution,[],[f26365,f170]) ).
fof(f27025,plain,
( ! [X0] :
( releasedAt(X0,n3)
| ~ holdsAt(X0,n2)
| holdsAt(X0,n3)
| n0 = n2 )
| spl11_195 ),
inference(forward_subsumption_resolution,[],[f27020,f17735]) ).
fof(f27027,plain,
( ! [X0] :
( ~ holdsAt(X0,n2)
| releasedAt(X0,n3)
| holdsAt(X0,n3) )
| spl11_194
| spl11_195 ),
inference(forward_subsumption_resolution,[],[f27025,f17731]) ).
fof(f27060,plain,
( releasedAt(filling,n3)
| holdsAt(filling,n3)
| ~ spl11_172
| spl11_194
| spl11_195 ),
inference(resolution,[],[f27027,f16390]) ).
fof(f27075,plain,
( releasedAt(filling,n3)
| spl11_152
| ~ spl11_172
| spl11_194
| spl11_195 ),
inference(forward_subsumption_resolution,[],[f27060,f14000]) ).
fof(f27076,plain,
( releasedAt(filling,n2)
| spl11_152
| ~ spl11_172
| spl11_194
| spl11_195 ),
inference(resolution,[],[f27075,f26960]) ).
fof(f27081,plain,
( $false
| spl11_152
| ~ spl11_172
| spl11_181
| spl11_194
| spl11_195 ),
inference(forward_subsumption_resolution,[],[f27076,f17000]) ).
fof(f27082,plain,
( spl11_152
| ~ spl11_172
| spl11_181
| spl11_194
| spl11_195 ),
inference(avatar_contradiction_clause,[],[f27081]) ).
cnf(s5194,plain,
spl11_142,
inference(sat_conversion,[],[f13922]) ).
cnf(s5257,plain,
( spl11_151
| ~ spl11_152 ),
inference(sat_conversion,[],[f14001]) ).
cnf(s5694,plain,
( ~ spl11_172
| ~ spl11_173 ),
inference(sat_conversion,[],[f16396]) ).
cnf(s5888,plain,
~ spl11_178,
inference(sat_conversion,[],[f16949]) ).
cnf(s5904,plain,
( ~ spl11_142
| spl11_173
| ~ spl11_179 ),
inference(sat_conversion,[],[f16959]) ).
cnf(s6231,plain,
~ spl11_194,
inference(sat_conversion,[],[f17847]) ).
cnf(s6247,plain,
( ~ spl11_172
| spl11_174
| ~ spl11_195 ),
inference(sat_conversion,[],[f17858]) ).
cnf(s6290,plain,
~ spl11_197,
inference(sat_conversion,[],[f17995]) ).
cnf(s7913,plain,
( ~ spl11_142
| spl11_172
| spl11_178
| spl11_179
| spl11_181 ),
inference(sat_conversion,[],[f22653]) ).
cnf(s8033,plain,
( spl11_178
| spl11_179
| ~ spl11_181 ),
inference(sat_conversion,[],[f22788]) ).
cnf(s8061,plain,
( ~ spl11_173
| spl11_260 ),
inference(sat_conversion,[],[f22799]) ).
cnf(s9400,plain,
( spl11_152
| spl11_172
| ~ spl11_179
| spl11_194
| spl11_197
| ~ spl11_260 ),
inference(sat_conversion,[],[f26557]) ).
cnf(s9461,plain,
~ spl11_151,
inference(sat_conversion,[],[f26669]) ).
cnf(s9548,plain,
( ~ spl11_174
| spl11_317 ),
inference(sat_conversion,[],[f26739]) ).
cnf(s9666,plain,
( spl11_152
| ~ spl11_195
| spl11_197
| ~ spl11_317 ),
inference(sat_conversion,[],[f26871]) ).
cnf(s9762,plain,
( spl11_152
| ~ spl11_172
| spl11_181
| spl11_194
| spl11_195 ),
inference(sat_conversion,[],[f27082]) ).
cnf(s9772,plain,
~ spl11_152,
inference(rat,[],[s5257,s9461]) ).
cnf(s9824,plain,
( spl11_179
| spl11_172 ),
inference(rat,[],[s7913,s8033,s5888,s5194]) ).
cnf(s9825,plain,
( ~ spl11_179
| spl11_172 ),
inference(rat,[],[s8061,s5904,s9400,s6290,s6231,s9772,s5194]) ).
cnf(s9826,plain,
spl11_172,
inference(rat,[],[s9825,s9824]) ).
cnf(s9827,plain,
~ spl11_173,
inference(rat,[],[s5694,s9826]) ).
cnf(s9828,plain,
~ spl11_179,
inference(rat,[],[s5904,s5194,s9827]) ).
cnf(s9829,plain,
~ spl11_181,
inference(rat,[],[s8033,s5888,s9828]) ).
cnf(s9834,plain,
spl11_195,
inference(rat,[],[s9762,s9826,s6231,s9772,s9829]) ).
cnf(s9835,plain,
~ spl11_317,
inference(rat,[],[s9666,s9772,s6290,s9834]) ).
cnf(s9837,plain,
spl11_174,
inference(rat,[],[s6247,s9826,s9834]) ).
cnf(s9838,plain,
$false,
inference(rat,[],[s9548,s9835,s9837]) ).
fof(f27083,plain,
$false,
inference(avatar_sat_refutation,[],[s9838]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR001+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n011.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 22:05:02 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.63/1.07 % (3834505)Will run a generic schedule for satisfiability detection.
% 5.63/1.07 % (3834513)dis+10_1_sil=32000:sp=arity:random_seed=2342049168:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.63/1.07 % (3834511)% WARNING: option uhcvi not known.
% 5.63/1.07 % (3834510)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=462586723_2999 on theBenchmark for (2999ds/0Mi)
% 5.63/1.07 % (3834511)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=259380707:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.63/1.07 % (3834512)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3210294062:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.63/1.07 % (3834514)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3239073951:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.63/1.07 % (3834515)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2778007680:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.63/1.07 % (3834516)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2160071510:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.63/1.07 % Detected minimum model sizes of [3]
% 5.63/1.07 % Detected maximum model sizes of [max]
% 5.63/1.07 % TRYING [3]
% 5.63/1.07 % TRYING [4]
% 5.63/1.07 % (3834513)Instruction limit reached!
% 5.63/1.07 % (3834513)------------------------------
% 5.63/1.07 % (3834513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.07 % (3834513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.07 % (3834513)CaDiCaL version: 2.1.3
% 5.63/1.07 % (3834513)Termination reason: Instruction limit
% 5.63/1.07 % (3834513)Termination phase: Saturation
% 5.63/1.07 % (3834513)Time elapsed: 0.035 s
% 5.63/1.07 % (3834513)Peak memory usage: 12 MB
% 5.63/1.07 % (3834513)Instructions burned: 104 (million)
% 5.63/1.07 % TRYING [5]
% 5.63/1.07 % (3834524)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=865183175:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.63/1.07 % Detected minimum model sizes of [3]
% 5.63/1.07 % Detected maximum model sizes of [max]
% 5.63/1.07 % TRYING [3]
% 5.63/1.07 % TRYING [4]
% 5.63/1.07 % TRYING [5]
% 5.63/1.07 % TRYING [6]
% 5.63/1.07 % (3834516)Instruction limit reached!
% 5.63/1.07 % (3834516)------------------------------
% 5.63/1.07 % (3834516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.07 % (3834516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.07 % (3834516)CaDiCaL version: 2.1.3
% 5.63/1.07 % (3834516)Termination reason: Instruction limit
% 5.63/1.07 % (3834516)Termination phase: Saturation
% 5.63/1.07 % (3834516)Time elapsed: 0.076 s
% 5.63/1.07 % (3834516)Peak memory usage: 12 MB
% 5.63/1.07 % (3834516)Instructions burned: 159 (million)
% 5.63/1.07 % (3834514)Instruction limit reached!
% 5.63/1.07 % (3834514)------------------------------
% 5.63/1.07 % (3834514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.07 % (3834514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.07 % (3834514)CaDiCaL version: 2.1.3
% 5.63/1.07 % (3834514)Termination reason: Instruction limit
% 5.63/1.07 % (3834514)Termination phase: Saturation
% 5.63/1.07 % (3834514)Time elapsed: 0.077 s
% 5.63/1.07 % (3834514)Peak memory usage: 13 MB
% 5.63/1.07 % (3834514)Instructions burned: 116 (million)
% 5.63/1.07 % (3834515)Instruction limit reached!
% 5.63/1.07 % (3834515)------------------------------
% 5.63/1.07 % (3834515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.07 % (3834515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.07 % (3834515)CaDiCaL version: 2.1.3
% 5.63/1.07 % (3834515)Termination reason: Instruction limit
% 5.63/1.07 % (3834515)Termination phase: Saturation
% 5.63/1.07 % (3834515)Time elapsed: 0.081 s
% 5.63/1.07 % (3834515)Peak memory usage: 13 MB
% 5.63/1.07 % (3834515)Instructions burned: 131 (million)
% 5.63/1.07 % TRYING [6]
% 5.63/1.07 % (3834526)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=50334314:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 5.63/1.07 % (3834527)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=415024209:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.63/1.07 % (3834528)ott-21_1_sil=16000:fs=off:random_seed=2026850907:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.63/1.07 % TRYING [7]
% 5.63/1.07 % TRYING [7]
% 5.63/1.07 % (3834526)Instruction limit reached!
% 5.63/1.07 % (3834526)------------------------------
% 5.63/1.07 % (3834526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.07 % (3834526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.07 % (3834526)CaDiCaL version: 2.1.3
% 5.63/1.07 % (3834526)Termination reason: Instruction limit
% 5.63/1.07 % (3834526)Termination phase: Saturation
% 5.63/1.07 % (3834526)Time elapsed: 0.082 s
% 5.63/1.07 % (3834526)Peak memory usage: 13 MB
% 5.63/1.07 % (3834526)Instructions burned: 132 (million)
% 5.63/1.07 % (3834524)Instruction limit reached!
% 5.63/1.07 % (3834524)------------------------------
% 5.63/1.07 % (3834524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.07 % (3834524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.07 % (3834524)CaDiCaL version: 2.1.3
% 5.63/1.07 % (3834524)Termination reason: Instruction limit
% 5.63/1.07 % (3834524)Termination phase: Finite model building constraint generation
% 5.63/1.07 % (3834524)Time elapsed: 0.143 s
% 5.63/1.07 % (3834524)Peak memory usage: 28 MB
% 5.63/1.07 % (3834524)Instructions burned: 718 (million)
% 5.63/1.07 % (3834533)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1432290499:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 5.63/1.07 % (3834528)Instruction limit reached!
% 5.63/1.07 % (3834528)------------------------------
% 5.63/1.07 % (3834528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.07 % (3834528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.07 % (3834528)CaDiCaL version: 2.1.3
% 5.63/1.07 % (3834528)Termination reason: Instruction limit
% 5.63/1.07 % (3834528)Termination phase: Saturation
% 5.63/1.07 % (3834528)Time elapsed: 0.094 s
% 5.63/1.07 % (3834528)Peak memory usage: 13 MB
% 5.63/1.07 % (3834528)Instructions burned: 180 (million)
% 5.63/1.07 % Detected minimum model sizes of [3]
% 5.63/1.07 % Detected maximum model sizes of [max]
% 5.63/1.07 % TRYING [3]
% 5.63/1.07 % (3834532)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=531920459:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 5.63/1.07 % TRYING [4]
% 5.63/1.07 % (3834535)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1488098296:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 5.63/1.07 % TRYING [5]
% 5.63/1.07 % TRYING [6]
% 5.63/1.07 % TRYING [8]
% 5.63/1.07 % (3834533)Instruction limit reached!
% 5.63/1.07 % (3834533)------------------------------
% 5.63/1.07 % (3834533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.07 % (3834533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.07 % (3834533)CaDiCaL version: 2.1.3
% 5.63/1.07 % (3834533)Termination reason: Instruction limit
% 5.63/1.07 % (3834533)Termination phase: Finite model building SAT solving
% 5.63/1.07 % (3834533)Time elapsed: 0.177 s
% 5.63/1.07 % (3834533)Peak memory usage: 26 MB
% 5.63/1.07 % (3834533)Instructions burned: 870 (million)
% 5.63/1.07 % (3834538)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=596419621:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 5.63/1.07 % TRYING [14]
% 5.63/1.07 % (3834527)Instruction limit reached!
% 5.63/1.07 % (3834527)------------------------------
% 5.63/1.07 % (3834527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.07 % (3834527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.07 % (3834527)CaDiCaL version: 2.1.3
% 5.63/1.07 % (3834527)Termination reason: Instruction limit
% 5.63/1.07 % (3834527)Termination phase: Saturation
% 5.63/1.07 % (3834527)Time elapsed: 0.361 s
% 5.63/1.07 % (3834527)Peak memory usage: 14 MB
% 5.63/1.07 % (3834527)Instructions burned: 685 (million)
% 5.63/1.07 % (3834540)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=3240303648: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)
% 5.63/1.07 % (3834532)Instruction limit reached!
% 5.63/1.07 % (3834532)------------------------------
% 5.63/1.07 % (3834532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.07 % (3834532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.07 % (3834532)CaDiCaL version: 2.1.3
% 5.63/1.07 % (3834532)Termination reason: Instruction limit
% 5.63/1.07 % (3834532)Termination phase: Saturation
% 5.63/1.07 % (3834532)Time elapsed: 0.300 s
% 5.63/1.07 % (3834532)Peak memory usage: 14 MB
% 5.63/1.07 % (3834532)Instructions burned: 477 (million)
% 5.63/1.07 % (3834542)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1564156077:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 5.63/1.07 % TRYING [9]
% 5.63/1.07 % (3834538)Instruction limit reached!
% 5.63/1.07 % (3834538)------------------------------
% 5.63/1.07 % (3834538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.07 % (3834538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.07 % (3834538)CaDiCaL version: 2.1.3
% 5.63/1.07 % (3834538)Termination reason: Instruction limit
% 5.63/1.07 % (3834538)Termination phase: Finite model building constraint generation
% 5.63/1.07 % (3834538)Time elapsed: 0.188 s
% 5.63/1.07 % (3834538)Peak memory usage: 80 MB
% 5.63/1.07 % (3834538)Instructions burned: 893 (million)
% 5.63/1.07 % (3834544)fmb+10_1_sil=64000:random_seed=1061966524:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 5.63/1.07 % Detected minimum model sizes of [3]
% 5.63/1.07 % Detected maximum model sizes of [max]
% 5.63/1.07 % TRYING [3]
% 5.63/1.07 % TRYING [4]
% 5.63/1.07 % TRYING [5]
% 5.63/1.07 % TRYING [6]
% 5.63/1.07 % TRYING [7]
% 5.63/1.07 % (3834512) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3834505-3834512"...
% 5.63/1.07 % (3834512)...printing done.
% 5.63/1.07 % (3834512)Refutation found. Thanks to Tanya!
% 5.63/1.07 % SZS status Theorem for theBenchmark
% 5.63/1.07 % SZS output start Proof for theBenchmark
% See solution above
% 5.63/1.08 % (3834512)------------------------------
% 5.63/1.08 % (3834512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.63/1.08 % (3834512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.63/1.08 % (3834512)CaDiCaL version: 2.1.3
% 5.63/1.08 % (3834512)Termination reason: Refutation
% 5.63/1.08 % (3834512)Time elapsed: 0.786 s
% 5.63/1.08 % (3834512)Peak memory usage: 30 MB
% 5.63/1.08 % (3834512)Instructions burned: 1315 (million)
% 5.63/1.08 % (3834505)Success in time 0.843 s
% 5.63/1.08 % Vampire exiting
%------------------------------------------------------------------------------