%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR008+1 : 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 : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:44:19 AM UTC 2026
% Result : Theorem 1.45s 0.59s
% Output : Refutation 1.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 30
% Syntax : Number of formulae : 184 ( 45 unt; 13 def)
% Number of atoms : 435 ( 68 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 435 ( 184 ~; 194 |; 31 &)
% ( 22 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 14 prp; 0-4 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-3 aty)
% Number of variables : 175 ( 0 sgn 164 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( stoppedIn(X0,X1,X2)
<=> ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',stoppedin_defn) ).
fof(f3,axiom,
! [X0,X1,X2,X3,X4] :
( ( happens(X0,X1)
& initiates(X0,X2,X1)
& less(n0,X4)
& trajectory(X2,X1,X3,X4)
& ~ stoppedIn(X1,X2,plus(X1,X4)) )
=> holdsAt(X3,plus(X1,X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',change_holding) ).
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(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(f17,axiom,
! [X0,X1,X2,X3] :
( ( holdsAt(waterLevel(X0),X1)
& X2 = plus(X0,X3) )
=> trajectory(filling,X1,waterLevel(X2),X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',change_of_waterLevel) ).
fof(f18,axiom,
! [X0,X1,X2] :
( ( holdsAt(waterLevel(X1),X0)
& holdsAt(waterLevel(X2),X0) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',same_waterLevel) ).
fof(f27,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus0_1) ).
fof(f28,axiom,
plus(n0,n2) = n2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus0_2) ).
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(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(f48,axiom,
! [X0,X1] :
( less(X0,X1)
<=> ( ~ less(X1,X0)
& X1 != X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_property) ).
fof(f49,axiom,
holdsAt(waterLevel(n0),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',waterLevel_0) ).
fof(f55,conjecture,
holdsAt(waterLevel(n2),n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',waterLevel_2) ).
fof(f56,negated_conjecture,
~ holdsAt(waterLevel(n2),n2),
inference(negated_conjecture,[status(cth)],[f55]) ).
fof(f57,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(f58,plain,
~ holdsAt(waterLevel(n2),n2),
inference(flattening,[],[f56]) ).
fof(f60,plain,
! [X0,X1,X2] :
( stoppedIn(X0,X1,X2)
=> ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) ) ),
inference(unused_predicate_definition_removal,[],[f1]) ).
fof(f63,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) )
| ~ stoppedIn(X0,X1,X2) ),
inference(ennf_transformation,[],[f60]) ).
fof(f64,plain,
! [X0,X1,X2,X3,X4] :
( holdsAt(X3,plus(X1,X4))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1)
| ~ less(n0,X4)
| ~ trajectory(X2,X1,X3,X4)
| stoppedIn(X1,X2,plus(X1,X4)) ),
inference(ennf_transformation,[],[f3]) ).
fof(f65,plain,
! [X0,X1,X2,X3,X4] :
( holdsAt(X3,plus(X1,X4))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1)
| ~ less(n0,X4)
| ~ trajectory(X2,X1,X3,X4)
| stoppedIn(X1,X2,plus(X1,X4)) ),
inference(flattening,[],[f64]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(ennf_transformation,[],[f17]) ).
fof(f83,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(flattening,[],[f82]) ).
fof(f84,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f85,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(flattening,[],[f84]) ).
fof(f86,plain,
! [X0] : ~ less(X0,n0),
inference(ennf_transformation,[],[f38]) ).
fof(f88,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| less(sK1(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f63]) ).
fof(f89,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| less(X0,sK1(X0,X1,X2)) ),
inference(cnf_transformation,[],[f63]) ).
fof(f90,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| happens(sK0(X0,X1,X2),sK1(X0,X1,X2)) ),
inference(cnf_transformation,[],[f63]) ).
fof(f91,plain,
! [X2,X3,X0,X1,X4] :
( stoppedIn(X1,X2,plus(X1,X4))
| ~ trajectory(X2,X1,X3,X4)
| ~ less(n0,X4)
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X3,plus(X1,X4)) ),
inference(cnf_transformation,[],[f65]) ).
fof(f122,plain,
! [X2,X0,X1] :
( filling != X1
| tapOn != X0
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f57]) ).
fof(f134,plain,
! [X0,X1] :
( n0 != X1
| tapOn != X0
| happens(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
fof(f135,plain,
! [X0,X1] :
( holdsAt(waterLevel(n3),X1)
| n0 = X1
| ~ happens(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
fof(f142,plain,
! [X2,X3,X0,X1] :
( plus(X0,X3) != X2
| ~ holdsAt(waterLevel(X0),X1)
| trajectory(filling,X1,waterLevel(X2),X3) ),
inference(cnf_transformation,[],[f83]) ).
fof(f143,plain,
! [X2,X0,X1] :
( ~ holdsAt(waterLevel(X2),X0)
| ~ holdsAt(waterLevel(X1),X0)
| X1 = X2 ),
inference(cnf_transformation,[],[f85]) ).
fof(f153,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f27]) ).
fof(f154,plain,
n2 = plus(n0,n2),
inference(cnf_transformation,[],[f28]) ).
fof(f162,plain,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[],[f36]) ).
fof(f163,plain,
! [X0,X1] :
( X0 = X1
| less(X0,X1)
| ~ less_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f164,plain,
! [X0,X1] :
( X0 != X1
| less_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f165,plain,
! [X0,X1] :
( ~ less(X0,X1)
| less_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f166,plain,
! [X0] : ~ less(X0,n0),
inference(cnf_transformation,[],[f86]) ).
fof(f167,plain,
! [X0] :
( ~ less_or_equal(X0,n0)
| less(X0,n1) ),
inference(cnf_transformation,[],[f39]) ).
fof(f168,plain,
! [X0] :
( less_or_equal(X0,n0)
| ~ less(X0,n1) ),
inference(cnf_transformation,[],[f39]) ).
fof(f169,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| less(X0,n2) ),
inference(cnf_transformation,[],[f40]) ).
fof(f170,plain,
! [X0] :
( less_or_equal(X0,n1)
| ~ less(X0,n2) ),
inference(cnf_transformation,[],[f40]) ).
fof(f171,plain,
! [X0] :
( ~ less_or_equal(X0,n2)
| less(X0,n3) ),
inference(cnf_transformation,[],[f41]) ).
fof(f186,plain,
! [X0,X1] :
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f188,plain,
holdsAt(waterLevel(n0),n0),
inference(cnf_transformation,[],[f49]) ).
fof(f194,plain,
~ holdsAt(waterLevel(n2),n2),
inference(cnf_transformation,[],[f58]) ).
fof(f197,plain,
! [X2,X0] :
( tapOn != X0
| initiates(X0,filling,X2) ),
inference(equality_resolution,[],[f122]) ).
fof(f198,plain,
! [X2] : initiates(tapOn,filling,X2),
inference(equality_resolution,[],[f197]) ).
fof(f210,plain,
! [X0] :
( tapOn != X0
| happens(X0,n0) ),
inference(equality_resolution,[],[f134]) ).
fof(f211,plain,
happens(tapOn,n0),
inference(equality_resolution,[],[f210]) ).
fof(f212,plain,
! [X3,X0,X1] :
( ~ holdsAt(waterLevel(X0),X1)
| trajectory(filling,X1,waterLevel(plus(X0,X3)),X3) ),
inference(equality_resolution,[],[f142]) ).
fof(f214,plain,
! [X1] : less_or_equal(X1,X1),
inference(equality_resolution,[],[f164]) ).
fof(f216,plain,
! [X2,X3,X0,X1,X4] :
( ~ happens(X0,X1)
| trajectory(X2,X1,X3,X4)
| ~ less(n0,X4)
| ~ initiates(X0,X2,X1)
| stoppedIn(X1,X2,plus(X1,X4))
| ~ holdsAt(X3,plus(X1,X4)) ),
inference(consistent_polarity_flipping,[],[f91]) ).
fof(f255,plain,
! [X0,X1] :
( ~ holdsAt(waterLevel(n3),X1)
| n0 = X1
| ~ happens(X0,X1) ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f256,plain,
! [X3,X0,X1] :
( ~ trajectory(filling,X1,waterLevel(plus(X0,X3)),X3)
| holdsAt(waterLevel(X0),X1) ),
inference(consistent_polarity_flipping,[],[f212]) ).
fof(f257,plain,
! [X2,X0,X1] :
( holdsAt(waterLevel(X2),X0)
| holdsAt(waterLevel(X1),X0)
| X1 = X2 ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f258,plain,
! [X0,X1] :
( ~ less_or_equal(X0,X1)
| ~ less(X0,X1) ),
inference(consistent_polarity_flipping,[],[f165]) ).
fof(f259,plain,
! [X1] : ~ less_or_equal(X1,X1),
inference(consistent_polarity_flipping,[],[f214]) ).
fof(f260,plain,
! [X0,X1] :
( less_or_equal(X0,X1)
| less(X0,X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f261,plain,
! [X0] :
( ~ less_or_equal(X0,n0)
| ~ less(X0,n1) ),
inference(consistent_polarity_flipping,[],[f168]) ).
fof(f262,plain,
! [X0] :
( less_or_equal(X0,n0)
| less(X0,n1) ),
inference(consistent_polarity_flipping,[],[f167]) ).
fof(f263,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| ~ less(X0,n2) ),
inference(consistent_polarity_flipping,[],[f170]) ).
fof(f264,plain,
! [X0] :
( less_or_equal(X0,n1)
| less(X0,n2) ),
inference(consistent_polarity_flipping,[],[f169]) ).
fof(f266,plain,
! [X0] :
( less_or_equal(X0,n2)
| less(X0,n3) ),
inference(consistent_polarity_flipping,[],[f171]) ).
fof(f279,plain,
~ holdsAt(waterLevel(n0),n0),
inference(consistent_polarity_flipping,[],[f188]) ).
fof(f285,plain,
holdsAt(waterLevel(n2),n2),
inference(consistent_polarity_flipping,[],[f194]) ).
fof(f287,plain,
less(n0,n1),
inference(resolution,[],[f262,f259]) ).
fof(f290,plain,
less(n1,n2),
inference(resolution,[],[f264,f259]) ).
fof(f291,plain,
! [X0] :
( less(X0,n2)
| ~ less(X0,n1) ),
inference(resolution,[],[f264,f258]) ).
fof(f293,plain,
~ less(n2,n1),
inference(resolution,[],[f290,f186]) ).
fof(f295,plain,
less(n2,n3),
inference(resolution,[],[f266,f259]) ).
fof(f321,plain,
n1 = plus(n1,n0),
inference(superposition,[],[f162,f153]) ).
fof(f359,plain,
! [X0] :
( less(X0,n0)
| n0 = X0
| ~ less(X0,n1) ),
inference(resolution,[],[f260,f261]) ).
fof(f360,plain,
! [X0] :
( ~ less(X0,n2)
| n1 = X0
| less(X0,n1) ),
inference(resolution,[],[f260,f263]) ).
fof(f368,plain,
! [X0] :
( ~ less(X0,n1)
| n0 = X0 ),
inference(forward_subsumption_resolution,[],[f359,f166]) ).
fof(f385,definition,
( spl10_1
<=> n1 = n3 ),
introduced(definition,[new_symbols(definition,[spl10_1])],[avatar_definition]) ).
fof(f387,plain,
( n1 = n3
| ~ spl10_1 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f489,plain,
! [X0] :
( ~ trajectory(filling,X0,waterLevel(n1),n1)
| holdsAt(waterLevel(n0),X0) ),
inference(superposition,[],[f256,f153]) ).
fof(f491,plain,
! [X0] :
( ~ trajectory(filling,X0,waterLevel(n2),n2)
| holdsAt(waterLevel(n0),X0) ),
inference(superposition,[],[f256,f154]) ).
fof(f653,plain,
! [X2,X0,X1] :
( ~ initiates(tapOn,X0,n0)
| ~ less(n0,X2)
| trajectory(X0,n0,X1,X2)
| stoppedIn(n0,X0,plus(n0,X2))
| ~ holdsAt(X1,plus(n0,X2)) ),
inference(resolution,[],[f216,f211]) ).
fof(f1458,plain,
! [X0,X1] :
( ~ holdsAt(X1,plus(n0,X0))
| trajectory(filling,n0,X1,X0)
| stoppedIn(n0,filling,plus(n0,X0))
| ~ less(n0,X0) ),
inference(resolution,[],[f653,f198]) ).
fof(f1657,definition,
( spl10_77
<=> ! [X0] :
( n3 = X0
| holdsAt(waterLevel(X0),n1) ) ),
introduced(definition,[new_symbols(definition,[spl10_77])],[avatar_definition]) ).
fof(f1658,plain,
( ! [X0] :
( holdsAt(waterLevel(X0),n1)
| n3 = X0 )
| ~ spl10_77 ),
inference(avatar_component_clause,[],[f1657]) ).
fof(f1661,definition,
( spl10_78
<=> n0 = n1 ),
introduced(definition,[new_symbols(definition,[spl10_78])],[avatar_definition]) ).
fof(f2858,plain,
! [X0] :
( ~ holdsAt(X0,n2)
| trajectory(filling,n0,X0,n2)
| stoppedIn(n0,filling,n2)
| ~ less(n0,n2) ),
inference(superposition,[],[f1458,f154]) ).
fof(f2859,plain,
! [X0,X1] :
( ~ holdsAt(X1,plus(X0,n0))
| trajectory(filling,n0,X1,X0)
| stoppedIn(n0,filling,plus(X0,n0))
| ~ less(n0,X0) ),
inference(superposition,[],[f1458,f162]) ).
fof(f2862,definition,
( spl10_131
<=> less(n0,n2) ),
introduced(definition,[new_symbols(definition,[spl10_131])],[avatar_definition]) ).
fof(f2864,plain,
( ~ less(n0,n2)
| spl10_131 ),
inference(avatar_component_clause,[],[f2862]) ).
fof(f2866,definition,
( spl10_132
<=> stoppedIn(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl10_132])],[avatar_definition]) ).
fof(f2868,plain,
( stoppedIn(n0,filling,n2)
| ~ spl10_132 ),
inference(avatar_component_clause,[],[f2866]) ).
fof(f2870,definition,
( spl10_133
<=> ! [X0] :
( ~ holdsAt(X0,n2)
| trajectory(filling,n0,X0,n2) ) ),
introduced(definition,[new_symbols(definition,[spl10_133])],[avatar_definition]) ).
fof(f2871,plain,
( ! [X0] :
( trajectory(filling,n0,X0,n2)
| ~ holdsAt(X0,n2) )
| ~ spl10_133 ),
inference(avatar_component_clause,[],[f2870]) ).
fof(f2872,plain,
( ~ spl10_131
| spl10_132
| spl10_133 ),
inference(avatar_split_clause,[],[f2858,f2870,f2866,f2862]) ).
fof(f2884,definition,
( spl10_136
<=> stoppedIn(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl10_136])],[avatar_definition]) ).
fof(f2886,plain,
( stoppedIn(n0,filling,n1)
| ~ spl10_136 ),
inference(avatar_component_clause,[],[f2884]) ).
fof(f2888,definition,
( spl10_137
<=> ! [X0] :
( ~ holdsAt(X0,n1)
| trajectory(filling,n0,X0,n1) ) ),
introduced(definition,[new_symbols(definition,[spl10_137])],[avatar_definition]) ).
fof(f2889,plain,
( ! [X0] :
( trajectory(filling,n0,X0,n1)
| ~ holdsAt(X0,n1) )
| ~ spl10_137 ),
inference(avatar_component_clause,[],[f2888]) ).
fof(f2962,plain,
( ~ less(n0,n1)
| spl10_131 ),
inference(resolution,[],[f2864,f291]) ).
fof(f2963,plain,
( $false
| spl10_131 ),
inference(forward_subsumption_resolution,[],[f2962,f287]) ).
fof(f2964,plain,
spl10_131,
inference(avatar_contradiction_clause,[],[f2963]) ).
fof(f3297,plain,
( happens(sK0(n0,filling,n2),sK1(n0,filling,n2))
| ~ spl10_132 ),
inference(resolution,[],[f2868,f90]) ).
fof(f3298,plain,
( less(n0,sK1(n0,filling,n2))
| ~ spl10_132 ),
inference(resolution,[],[f2868,f89]) ).
fof(f3299,plain,
( less(sK1(n0,filling,n2),n2)
| ~ spl10_132 ),
inference(resolution,[],[f2868,f88]) ).
fof(f3354,plain,
( less(n0,sK1(n0,filling,n1))
| ~ spl10_136 ),
inference(resolution,[],[f2886,f89]) ).
fof(f3355,plain,
( less(sK1(n0,filling,n1),n1)
| ~ spl10_136 ),
inference(resolution,[],[f2886,f88]) ).
fof(f3798,definition,
( spl10_158
<=> less(sK1(n0,filling,n2),n1) ),
introduced(definition,[new_symbols(definition,[spl10_158])],[avatar_definition]) ).
fof(f3800,plain,
( less(sK1(n0,filling,n2),n1)
| ~ spl10_158 ),
inference(avatar_component_clause,[],[f3798]) ).
fof(f3802,definition,
( spl10_159
<=> n1 = sK1(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl10_159])],[avatar_definition]) ).
fof(f3804,plain,
( n1 = sK1(n0,filling,n2)
| ~ spl10_159 ),
inference(avatar_component_clause,[],[f3802]) ).
fof(f3808,plain,
( ~ holdsAt(waterLevel(n2),n2)
| holdsAt(waterLevel(n0),n0)
| ~ spl10_133 ),
inference(resolution,[],[f2871,f491]) ).
fof(f3831,plain,
( holdsAt(waterLevel(n0),n0)
| ~ spl10_133 ),
inference(forward_subsumption_resolution,[],[f3808,f285]) ).
fof(f3841,plain,
( $false
| ~ spl10_133 ),
inference(forward_subsumption_resolution,[],[f3831,f279]) ).
fof(f3842,plain,
~ spl10_133,
inference(avatar_contradiction_clause,[],[f3841]) ).
fof(f3850,plain,
( n1 = sK1(n0,filling,n2)
| less(sK1(n0,filling,n2),n1)
| ~ spl10_132 ),
inference(resolution,[],[f3299,f360]) ).
fof(f3853,plain,
( spl10_158
| spl10_159
| ~ spl10_132 ),
inference(avatar_split_clause,[],[f3850,f2866,f3802,f3798]) ).
fof(f5081,plain,
( n0 = sK1(n0,filling,n1)
| ~ spl10_136 ),
inference(resolution,[],[f3355,f368]) ).
fof(f5251,plain,
! [X0] :
( ~ holdsAt(X0,n1)
| trajectory(filling,n0,X0,n1)
| stoppedIn(n0,filling,n1)
| ~ less(n0,n1) ),
inference(superposition,[],[f2859,f321]) ).
fof(f5277,plain,
( n0 = sK1(n0,filling,n2)
| ~ spl10_158 ),
inference(resolution,[],[f3800,f368]) ).
fof(f5482,plain,
! [X0] :
( ~ holdsAt(X0,n1)
| trajectory(filling,n0,X0,n1)
| stoppedIn(n0,filling,n1) ),
inference(forward_subsumption_resolution,[],[f5251,f287]) ).
fof(f5484,plain,
( spl10_136
| spl10_137 ),
inference(avatar_split_clause,[],[f5482,f2888,f2884]) ).
fof(f5489,plain,
( ~ holdsAt(waterLevel(n1),n1)
| holdsAt(waterLevel(n0),n0)
| ~ spl10_137 ),
inference(resolution,[],[f2889,f489]) ).
fof(f5506,definition,
( spl10_224
<=> holdsAt(waterLevel(n3),n1) ),
introduced(definition,[new_symbols(definition,[spl10_224])],[avatar_definition]) ).
fof(f5507,plain,
( holdsAt(waterLevel(n3),n1)
| ~ spl10_224 ),
inference(avatar_component_clause,[],[f5506]) ).
fof(f5508,plain,
( ~ holdsAt(waterLevel(n3),n1)
| spl10_224 ),
inference(avatar_component_clause,[],[f5506]) ).
fof(f5510,plain,
( ~ holdsAt(waterLevel(n1),n1)
| ~ spl10_137 ),
inference(forward_subsumption_resolution,[],[f5489,f279]) ).
fof(f5982,plain,
( n1 = n3
| ~ spl10_77
| ~ spl10_137 ),
inference(resolution,[],[f5510,f1658]) ).
fof(f6009,plain,
( spl10_1
| ~ spl10_77
| ~ spl10_137 ),
inference(avatar_split_clause,[],[f5982,f2888,f1657,f385]) ).
fof(f6035,plain,
( less(n2,n1)
| ~ spl10_1 ),
inference(superposition,[],[f295,f387]) ).
fof(f6105,plain,
( $false
| ~ spl10_1 ),
inference(forward_subsumption_resolution,[],[f6035,f293]) ).
fof(f6106,plain,
~ spl10_1,
inference(avatar_contradiction_clause,[],[f6105]) ).
fof(f6246,plain,
( ! [X0] :
( holdsAt(waterLevel(X0),n1)
| n3 = X0 )
| spl10_224 ),
inference(resolution,[],[f5508,f257]) ).
fof(f6265,plain,
( spl10_77
| spl10_224 ),
inference(avatar_split_clause,[],[f6246,f5506,f1657]) ).
fof(f6555,plain,
( less(n0,n0)
| ~ spl10_136 ),
inference(superposition,[],[f3354,f5081]) ).
fof(f6556,plain,
( $false
| ~ spl10_136 ),
inference(forward_subsumption_resolution,[],[f6555,f166]) ).
fof(f6557,plain,
~ spl10_136,
inference(avatar_contradiction_clause,[],[f6556]) ).
fof(f6596,plain,
( ! [X0] :
( n0 = n1
| ~ happens(X0,n1) )
| ~ spl10_224 ),
inference(resolution,[],[f5507,f255]) ).
fof(f6599,definition,
( spl10_245
<=> ! [X0] : ~ happens(X0,n1) ),
introduced(definition,[new_symbols(definition,[spl10_245])],[avatar_definition]) ).
fof(f6600,plain,
( ! [X0] : ~ happens(X0,n1)
| ~ spl10_245 ),
inference(avatar_component_clause,[],[f6599]) ).
fof(f6601,plain,
( spl10_245
| spl10_78
| ~ spl10_224 ),
inference(avatar_split_clause,[],[f6596,f5506,f1661,f6599]) ).
fof(f6671,definition,
( spl10_246
<=> n0 = sK1(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl10_246])],[avatar_definition]) ).
fof(f6672,plain,
( n0 != sK1(n0,filling,n2)
| spl10_246 ),
inference(avatar_component_clause,[],[f6671]) ).
fof(f6673,plain,
( n0 = sK1(n0,filling,n2)
| ~ spl10_246 ),
inference(avatar_component_clause,[],[f6671]) ).
fof(f6684,plain,
( spl10_246
| ~ spl10_158 ),
inference(avatar_split_clause,[],[f5277,f3798,f6671]) ).
fof(f6749,plain,
( less(n0,n0)
| ~ spl10_132
| ~ spl10_246 ),
inference(superposition,[],[f3298,f6673]) ).
fof(f6758,plain,
( $false
| ~ spl10_132
| ~ spl10_246 ),
inference(forward_subsumption_resolution,[],[f6749,f166]) ).
fof(f6759,plain,
( ~ spl10_132
| ~ spl10_246 ),
inference(avatar_contradiction_clause,[],[f6758]) ).
fof(f6823,plain,
( n0 != n1
| ~ spl10_159
| spl10_246 ),
inference(forward_demodulation,[],[f6672,f3804]) ).
fof(f6824,plain,
( ~ spl10_78
| ~ spl10_159
| spl10_246 ),
inference(avatar_split_clause,[],[f6823,f6671,f3802,f1661]) ).
fof(f7100,plain,
( happens(sK0(n0,filling,n2),n1)
| ~ spl10_132
| ~ spl10_159 ),
inference(forward_demodulation,[],[f3297,f3804]) ).
fof(f7101,plain,
( $false
| ~ spl10_132
| ~ spl10_159
| ~ spl10_245 ),
inference(forward_subsumption_resolution,[],[f7100,f6600]) ).
fof(f7102,plain,
( ~ spl10_132
| ~ spl10_159
| ~ spl10_245 ),
inference(avatar_contradiction_clause,[],[f7101]) ).
cnf(s363,plain,
( ~ spl10_131
| spl10_132
| spl10_133 ),
inference(sat_conversion,[],[f2872]) ).
cnf(s379,plain,
spl10_131,
inference(sat_conversion,[],[f2964]) ).
cnf(s460,plain,
~ spl10_133,
inference(sat_conversion,[],[f3842]) ).
cnf(s462,plain,
( ~ spl10_132
| spl10_158
| spl10_159 ),
inference(sat_conversion,[],[f3853]) ).
cnf(s547,plain,
( spl10_136
| spl10_137 ),
inference(sat_conversion,[],[f5484]) ).
cnf(s621,plain,
( spl10_1
| ~ spl10_77
| ~ spl10_137 ),
inference(sat_conversion,[],[f6009]) ).
cnf(s627,plain,
~ spl10_1,
inference(sat_conversion,[],[f6106]) ).
cnf(s641,plain,
( spl10_77
| spl10_224 ),
inference(sat_conversion,[],[f6265]) ).
cnf(s673,plain,
~ spl10_136,
inference(sat_conversion,[],[f6557]) ).
cnf(s689,plain,
( spl10_78
| ~ spl10_224
| spl10_245 ),
inference(sat_conversion,[],[f6601]) ).
cnf(s692,plain,
( ~ spl10_158
| spl10_246 ),
inference(sat_conversion,[],[f6684]) ).
cnf(s697,plain,
( ~ spl10_132
| ~ spl10_246 ),
inference(sat_conversion,[],[f6759]) ).
cnf(s703,plain,
( ~ spl10_78
| ~ spl10_159
| spl10_246 ),
inference(sat_conversion,[],[f6824]) ).
cnf(s708,plain,
( ~ spl10_132
| ~ spl10_159
| ~ spl10_245 ),
inference(sat_conversion,[],[f7102]) ).
cnf(s712,plain,
( ~ spl10_77
| ~ spl10_137 ),
inference(rat,[],[s621,s627]) ).
cnf(s722,plain,
spl10_137,
inference(rat,[],[s547,s673]) ).
cnf(s724,plain,
~ spl10_77,
inference(rat,[],[s712,s722]) ).
cnf(s725,plain,
spl10_224,
inference(rat,[],[s641,s724]) ).
cnf(s746,plain,
spl10_132,
inference(rat,[],[s363,s460,s379]) ).
cnf(s747,plain,
~ spl10_246,
inference(rat,[],[s697,s746]) ).
cnf(s749,plain,
~ spl10_158,
inference(rat,[],[s692,s747]) ).
cnf(s750,plain,
spl10_159,
inference(rat,[],[s462,s746,s749]) ).
cnf(s751,plain,
~ spl10_245,
inference(rat,[],[s708,s746,s750]) ).
cnf(s752,plain,
~ spl10_78,
inference(rat,[],[s703,s747,s750]) ).
cnf(s753,plain,
$false,
inference(rat,[],[s689,s725,s751,s752]) ).
fof(f7103,plain,
$false,
inference(avatar_sat_refutation,[],[s753]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR008+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.23 % Computer : n008.cluster.edu
% 0.11/0.23 % Model : x86_64 x86_64
% 0.11/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.23 % Memory : 8046.5625MB
% 0.11/0.23 % OS : Linux 6.8.0-71-generic
% 0.11/0.23 % CPULimit : 300
% 0.11/0.23 % WCLimit : 300
% 0.11/0.23 % DateTime : Mon Sep 28 22:06:10 UTC 2026
% 0.11/0.24 % CPUTime :
% 0.11/0.24 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.28 Running first-order model finding
% 0.11/0.28 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
% 1.45/0.59 % (2709188)Will run a generic schedule for satisfiability detection.
% 1.45/0.59 % (2709195)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1528210113:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.45/0.59 % (2709193)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2097330007_2999 on theBenchmark for (2999ds/0Mi)
% 1.45/0.59 % (2709194)% WARNING: option uhcvi not known.
% 1.45/0.59 % Detected minimum model sizes of [3]
% 1.45/0.59 % Detected maximum model sizes of [max]
% 1.45/0.59 % TRYING [3]
% 1.45/0.59 % (2709196)dis+10_1_sil=32000:sp=arity:random_seed=612647976:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.45/0.59 % (2709194)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=577712361:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.45/0.59 % (2709197)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=231001580:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.45/0.59 % (2709198)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3219622568:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.45/0.59 % (2709199)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2025618456:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.45/0.59 % TRYING [4]
% 1.45/0.59 % TRYING [5]
% 1.45/0.59 % (2709196)Instruction limit reached!
% 1.45/0.59 % (2709196)------------------------------
% 1.45/0.59 % (2709196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.45/0.59 % (2709196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.45/0.59 % (2709196)CaDiCaL version: 2.1.3
% 1.45/0.59 % (2709196)Termination reason: Instruction limit
% 1.45/0.59 % (2709196)Termination phase: Saturation
% 1.45/0.59 % (2709196)Time elapsed: 0.109 s
% 1.45/0.59 % (2709196)Peak memory usage: 12 MB
% 1.45/0.59 % (2709196)Instructions burned: 103 (million)
% 1.45/0.59 % TRYING [6]
% 1.45/0.59 % (2709197)Instruction limit reached!
% 1.45/0.59 % (2709197)------------------------------
% 1.45/0.59 % (2709197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.45/0.59 % (2709197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.45/0.59 % (2709197)CaDiCaL version: 2.1.3
% 1.45/0.59 % (2709197)Termination reason: Instruction limit
% 1.45/0.59 % (2709197)Termination phase: Saturation
% 1.45/0.59 % (2709197)Time elapsed: 0.125 s
% 1.45/0.59 % (2709197)Peak memory usage: 13 MB
% 1.45/0.59 % (2709197)Instructions burned: 116 (million)
% 1.45/0.59 % (2709198)Instruction limit reached!
% 1.45/0.59 % (2709198)------------------------------
% 1.45/0.59 % (2709198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.45/0.59 % (2709198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.45/0.59 % (2709198)CaDiCaL version: 2.1.3
% 1.45/0.59 % (2709198)Termination reason: Instruction limit
% 1.45/0.59 % (2709198)Termination phase: Saturation
% 1.45/0.59 % (2709198)Time elapsed: 0.135 s
% 1.45/0.59 % (2709198)Peak memory usage: 13 MB
% 1.45/0.59 % (2709198)Instructions burned: 131 (million)
% 1.45/0.59 % (2709210)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3052064415:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 1.45/0.59 % (2709199)Instruction limit reached!
% 1.45/0.59 % (2709199)------------------------------
% 1.45/0.59 % (2709199)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.45/0.59 % (2709199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.45/0.59 % (2709199)CaDiCaL version: 2.1.3
% 1.45/0.59 % (2709199)Termination reason: Instruction limit
% 1.45/0.59 % (2709199)Termination phase: Saturation
% 1.45/0.59 % (2709199)Time elapsed: 0.150 s
% 1.45/0.59 % (2709199)Peak memory usage: 12 MB
% 1.45/0.59 % (2709199)Instructions burned: 159 (million)
% 1.45/0.59 % Detected minimum model sizes of [3]
% 1.45/0.59 % Detected maximum model sizes of [max]
% 1.45/0.59 % TRYING [3]
% 1.45/0.59 % (2709211)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2284721392:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.45/0.59 % (2709212)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=3124277591:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.45/0.59 % (2709215)ott-21_1_sil=16000:fs=off:random_seed=3845561064:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.45/0.59 % TRYING [4]
% 1.45/0.59 % TRYING [5]
% 1.45/0.59 % (2709194) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2709188-2709194"...
% 1.45/0.59 % (2709194)...printing done.
% 1.45/0.59 % (2709194)Refutation found. Thanks to Tanya!
% 1.45/0.59 % SZS status Theorem for theBenchmark
% 1.45/0.59 % SZS output start Proof for theBenchmark
% See solution above
% 1.45/0.59 % (2709194)------------------------------
% 1.45/0.59 % (2709194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.45/0.59 % (2709194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.45/0.59 % (2709194)CaDiCaL version: 2.1.3
% 1.45/0.59 % (2709194)Termination reason: Refutation
% 1.45/0.59 % (2709194)Time elapsed: 0.251 s
% 1.45/0.59 % (2709194)Peak memory usage: 15 MB
% 1.45/0.59 % (2709194)Instructions burned: 269 (million)
% 1.45/0.59 % (2709188)Success in time 0.297 s
% 1.45/0.59 % Vampire exiting
%------------------------------------------------------------------------------