%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR005+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 : n013.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.58s 0.49s
% Output : Refutation 1.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 47
% Syntax : Number of formulae : 292 ( 60 unt; 21 def)
% Number of atoms : 719 ( 92 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 740 ( 313 ~; 341 |; 46 &)
% ( 31 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 22 prp; 0-4 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-3 aty)
% Number of variables : 282 ( 0 sgn 264 !; 18 ?)
% 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(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(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(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(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(f22,axiom,
! [X0] : filling != waterLevel(X0),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',filling_not_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(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(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(filling,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',filling_3) ).
fof(f56,negated_conjecture,
~ holdsAt(filling,n3),
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(filling,n3),
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(f66,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(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(flattening,[],[f66]) ).
fof(f72,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f73,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(flattening,[],[f72]) ).
fof(f74,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f75,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(flattening,[],[f74]) ).
fof(f76,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(flattening,[],[f76]) ).
fof(f80,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(f81,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(flattening,[],[f80]) ).
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(f87,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| terminates(sK0(X0,X1,X2),X1,sK1(X0,X1,X2)) ),
inference(cnf_transformation,[],[f63]) ).
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(f93,plain,
! [X0,X1] :
( happens(sK2(X0,X1),X1)
| releasedAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f67]) ).
fof(f98,plain,
! [X0,X1] :
( releases(sK5(X0,X1),X0,X1)
| releasedAt(X0,X1)
| ~ releasedAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f73]) ).
fof(f100,plain,
! [X2,X0,X1] :
( ~ happens(X0,X1)
| ~ initiates(X0,X2,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f75]) ).
fof(f101,plain,
! [X2,X0,X1] :
( ~ terminates(X0,X2,X1)
| ~ happens(X0,X1)
| ~ holdsAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f77]) ).
fof(f104,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| ~ releasedAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f81]) ).
fof(f122,plain,
! [X2,X0,X1] :
( filling != X1
| tapOn != X0
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f57]) ).
fof(f131,plain,
! [X2,X0,X1] :
( waterLevel(sK9(X0,X1)) = X1
| ~ releases(X0,X1,X2) ),
inference(cnf_transformation,[],[f15]) ).
fof(f134,plain,
! [X0,X1] :
( n0 != X1
| tapOn != X0
| happens(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
fof(f135,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| n0 = X1
| holdsAt(waterLevel(n3),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(X1),X0)
| ~ holdsAt(waterLevel(X2),X0)
| X1 = X2 ),
inference(cnf_transformation,[],[f85]) ).
fof(f147,plain,
! [X0] : filling != waterLevel(X0),
inference(cnf_transformation,[],[f22]) ).
fof(f153,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f27]) ).
fof(f154,plain,
n2 = plus(n0,n2),
inference(cnf_transformation,[],[f28]) ).
fof(f156,plain,
n2 = plus(n1,n1),
inference(cnf_transformation,[],[f30]) ).
fof(f157,plain,
n3 = plus(n1,n2),
inference(cnf_transformation,[],[f31]) ).
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(f185,plain,
! [X0,X1] :
( X0 != X1
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f188,plain,
holdsAt(waterLevel(n0),n0),
inference(cnf_transformation,[],[f49]) ).
fof(f194,plain,
~ holdsAt(filling,n3),
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(f215,plain,
! [X1] : ~ less(X1,X1),
inference(equality_resolution,[],[f185]) ).
fof(f216,plain,
! [X2,X0,X1] :
( happens(sK0(X0,X1,X2),sK1(X0,X1,X2))
| stoppedIn(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f90]) ).
fof(f217,plain,
! [X2,X0,X1] :
( ~ less(X0,sK1(X0,X1,X2))
| stoppedIn(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f89]) ).
fof(f218,plain,
! [X2,X0,X1] :
( ~ less(sK1(X0,X1,X2),X2)
| stoppedIn(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f88]) ).
fof(f219,plain,
! [X2,X0,X1] :
( ~ terminates(sK0(X0,X1,X2),X1,sK1(X0,X1,X2))
| stoppedIn(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f87]) ).
fof(f220,plain,
! [X2,X3,X0,X1,X4] :
( ~ trajectory(X2,X1,X3,X4)
| ~ stoppedIn(X1,X2,plus(X1,X4))
| less(n0,X4)
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X3,plus(X1,X4)) ),
inference(consistent_polarity_flipping,[],[f91]) ).
fof(f221,plain,
! [X0,X1] :
( ~ holdsAt(X0,X1)
| ~ releasedAt(X0,plus(X1,n1))
| happens(sK2(X0,X1),X1)
| holdsAt(X0,plus(X1,n1)) ),
inference(consistent_polarity_flipping,[],[f93]) ).
fof(f228,plain,
! [X0,X1] :
( ~ releases(sK5(X0,X1),X0,X1)
| ~ releasedAt(X0,X1)
| releasedAt(X0,plus(X1,n1)) ),
inference(consistent_polarity_flipping,[],[f98]) ).
fof(f229,plain,
! [X2,X0,X1] :
( ~ happens(X0,X1)
| terminates(X0,X2,X1)
| ~ holdsAt(X2,plus(X1,n1)) ),
inference(consistent_polarity_flipping,[],[f101]) ).
fof(f231,plain,
! [X2,X0,X1] :
( ~ happens(X0,X1)
| ~ initiates(X0,X2,X1)
| releasedAt(X2,plus(X1,n1)) ),
inference(consistent_polarity_flipping,[],[f104]) ).
fof(f258,plain,
! [X2,X0,X1] :
( releases(X0,X1,X2)
| waterLevel(sK9(X0,X1)) = X1 ),
inference(consistent_polarity_flipping,[],[f131]) ).
fof(f259,plain,
! [X0,X1] :
( less_or_equal(X0,X1)
| less(X0,X1) ),
inference(consistent_polarity_flipping,[],[f165]) ).
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(X0,n0),
inference(consistent_polarity_flipping,[],[f166]) ).
fof(f262,plain,
! [X0] :
( less_or_equal(X0,n0)
| less(X0,n1) ),
inference(consistent_polarity_flipping,[],[f168]) ).
fof(f263,plain,
! [X0] :
( ~ less_or_equal(X0,n0)
| ~ less(X0,n1) ),
inference(consistent_polarity_flipping,[],[f167]) ).
fof(f264,plain,
! [X0] :
( less_or_equal(X0,n1)
| less(X0,n2) ),
inference(consistent_polarity_flipping,[],[f170]) ).
fof(f265,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| ~ less(X0,n2) ),
inference(consistent_polarity_flipping,[],[f169]) ).
fof(f267,plain,
! [X0] :
( ~ less(X0,n3)
| ~ less_or_equal(X0,n2) ),
inference(consistent_polarity_flipping,[],[f171]) ).
fof(f282,plain,
! [X1] : less(X1,X1),
inference(consistent_polarity_flipping,[],[f215]) ).
fof(f287,plain,
~ less(n0,n1),
inference(resolution,[],[f263,f214]) ).
fof(f290,plain,
~ less(n1,n2),
inference(resolution,[],[f265,f214]) ).
fof(f291,plain,
! [X0] :
( ~ less(X0,n2)
| less(X0,n1) ),
inference(resolution,[],[f265,f259]) ).
fof(f292,plain,
~ less_or_equal(n3,n2),
inference(resolution,[],[f267,f282]) ).
fof(f324,plain,
n1 = plus(n1,n0),
inference(superposition,[],[f162,f153]) ).
fof(f360,plain,
! [X0] :
( ~ less(X0,n0)
| n0 = X0
| less(X0,n1) ),
inference(resolution,[],[f260,f262]) ).
fof(f361,plain,
! [X0] :
( less(X0,n2)
| n1 = X0
| ~ less(X0,n1) ),
inference(resolution,[],[f260,f264]) ).
fof(f369,plain,
! [X0] :
( less(X0,n1)
| n0 = X0 ),
inference(forward_subsumption_resolution,[],[f360,f261]) ).
fof(f436,definition,
( spl10_13
<=> n3 = n2 ),
introduced(definition,[new_symbols(definition,[spl10_13])],[avatar_definition]) ).
fof(f438,plain,
( n3 = n2
| ~ spl10_13 ),
inference(avatar_component_clause,[],[f436]) ).
fof(f460,plain,
! [X0] :
( ~ initiates(tapOn,X0,n0)
| holdsAt(X0,plus(n0,n1)) ),
inference(resolution,[],[f100,f211]) ).
fof(f461,plain,
! [X0] :
( ~ initiates(tapOn,X0,n0)
| holdsAt(X0,n1) ),
inference(forward_demodulation,[],[f460,f153]) ).
fof(f462,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(n0,X0)),X0),
inference(resolution,[],[f212,f188]) ).
fof(f467,plain,
! [X0] :
( ~ initiates(tapOn,X0,n0)
| releasedAt(X0,plus(n0,n1)) ),
inference(resolution,[],[f231,f211]) ).
fof(f468,plain,
! [X0] :
( ~ initiates(tapOn,X0,n0)
| releasedAt(X0,n1) ),
inference(forward_demodulation,[],[f467,f153]) ).
fof(f478,plain,
! [X2,X3,X0,X1] :
( stoppedIn(X0,X1,X2)
| terminates(sK0(X0,X1,X2),X3,sK1(X0,X1,X2))
| ~ holdsAt(X3,plus(sK1(X0,X1,X2),n1)) ),
inference(resolution,[],[f216,f229]) ).
fof(f485,plain,
! [X2,X3,X0,X1] :
( terminates(sK0(X0,X1,X2),X3,sK1(X0,X1,X2))
| stoppedIn(X0,X1,X2)
| ~ holdsAt(X3,plus(n1,sK1(X0,X1,X2))) ),
inference(forward_demodulation,[],[f478,f162]) ).
fof(f511,definition,
( spl10_18
<=> releasedAt(filling,n1) ),
introduced(definition,[new_symbols(definition,[spl10_18])],[avatar_definition]) ).
fof(f513,plain,
( releasedAt(filling,n1)
| ~ spl10_18 ),
inference(avatar_component_clause,[],[f511]) ).
fof(f517,plain,
! [X0,X1] :
( ~ releasedAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| waterLevel(sK9(sK5(X0,X1),X0)) = X0 ),
inference(resolution,[],[f228,f258]) ).
fof(f778,definition,
( spl10_48
<=> n1 = n3 ),
introduced(definition,[new_symbols(definition,[spl10_48])],[avatar_definition]) ).
fof(f780,plain,
( n1 = n3
| ~ spl10_48 ),
inference(avatar_component_clause,[],[f778]) ).
fof(f820,plain,
! [X0,X1] :
( stoppedIn(X0,X1,n1)
| n0 = sK1(X0,X1,n1) ),
inference(resolution,[],[f369,f218]) ).
fof(f829,plain,
holdsAt(filling,n1),
inference(resolution,[],[f461,f198]) ).
fof(f831,plain,
( ~ releasedAt(filling,plus(n1,n1))
| happens(sK2(filling,n1),n1)
| holdsAt(filling,plus(n1,n1)) ),
inference(resolution,[],[f829,f221]) ).
fof(f832,plain,
( ~ releasedAt(filling,n2)
| happens(sK2(filling,n1),n1)
| holdsAt(filling,plus(n1,n1)) ),
inference(forward_demodulation,[],[f831,f156]) ).
fof(f834,plain,
( holdsAt(filling,n2)
| ~ releasedAt(filling,n2)
| happens(sK2(filling,n1),n1) ),
inference(forward_demodulation,[],[f832,f156]) ).
fof(f837,definition,
( spl10_54
<=> happens(sK2(filling,n1),n1) ),
introduced(definition,[new_symbols(definition,[spl10_54])],[avatar_definition]) ).
fof(f839,plain,
( happens(sK2(filling,n1),n1)
| ~ spl10_54 ),
inference(avatar_component_clause,[],[f837]) ).
fof(f841,definition,
( spl10_55
<=> releasedAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl10_55])],[avatar_definition]) ).
fof(f842,plain,
( releasedAt(filling,n2)
| ~ spl10_55 ),
inference(avatar_component_clause,[],[f841]) ).
fof(f845,definition,
( spl10_56
<=> holdsAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl10_56])],[avatar_definition]) ).
fof(f847,plain,
( holdsAt(filling,n2)
| ~ spl10_56 ),
inference(avatar_component_clause,[],[f845]) ).
fof(f848,plain,
( spl10_54
| ~ spl10_55
| spl10_56 ),
inference(avatar_split_clause,[],[f834,f845,f841,f837]) ).
fof(f854,plain,
releasedAt(filling,n1),
inference(resolution,[],[f468,f198]) ).
fof(f855,plain,
spl10_18,
inference(avatar_split_clause,[],[f854,f511]) ).
fof(f874,plain,
trajectory(filling,n0,waterLevel(n1),n1),
inference(superposition,[],[f462,f153]) ).
fof(f877,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(X0,n0)),X0),
inference(superposition,[],[f462,f162]) ).
fof(f880,definition,
( spl10_60
<=> ! [X1] :
( ~ initiates(X1,filling,n0)
| ~ happens(X1,n0) ) ),
introduced(definition,[new_symbols(definition,[spl10_60])],[avatar_definition]) ).
fof(f881,plain,
( ! [X1] :
( ~ initiates(X1,filling,n0)
| ~ happens(X1,n0) )
| ~ spl10_60 ),
inference(avatar_component_clause,[],[f880]) ).
fof(f904,plain,
! [X0,X1] :
( ~ less(sK1(X0,X1,n2),n1)
| n1 = sK1(X0,X1,n2)
| stoppedIn(X0,X1,n2) ),
inference(resolution,[],[f361,f218]) ).
fof(f1071,plain,
( releasedAt(filling,plus(n1,n1))
| filling = waterLevel(sK9(sK5(filling,n1),filling))
| ~ spl10_18 ),
inference(resolution,[],[f517,f513]) ).
fof(f1072,plain,
( releasedAt(filling,plus(n1,n1))
| ~ spl10_18 ),
inference(forward_subsumption_resolution,[],[f1071,f147]) ).
fof(f1076,plain,
( releasedAt(filling,n2)
| ~ spl10_18 ),
inference(forward_demodulation,[],[f1072,f156]) ).
fof(f1092,plain,
( spl10_55
| ~ spl10_18 ),
inference(avatar_split_clause,[],[f1076,f511,f841]) ).
fof(f1222,plain,
( releasedAt(filling,plus(n2,n1))
| filling = waterLevel(sK9(sK5(filling,n2),filling))
| ~ spl10_55 ),
inference(resolution,[],[f842,f517]) ).
fof(f1227,plain,
( releasedAt(filling,plus(n2,n1))
| ~ spl10_55 ),
inference(forward_subsumption_resolution,[],[f1222,f147]) ).
fof(f1230,plain,
( releasedAt(filling,plus(n1,n2))
| ~ spl10_55 ),
inference(forward_demodulation,[],[f1227,f162]) ).
fof(f1236,definition,
( spl10_89
<=> releasedAt(filling,n3) ),
introduced(definition,[new_symbols(definition,[spl10_89])],[avatar_definition]) ).
fof(f1238,plain,
( releasedAt(filling,n3)
| ~ spl10_89 ),
inference(avatar_component_clause,[],[f1236]) ).
fof(f1245,plain,
( releasedAt(filling,n3)
| ~ spl10_55 ),
inference(forward_demodulation,[],[f1230,f157]) ).
fof(f1246,plain,
( spl10_89
| ~ spl10_55 ),
inference(avatar_split_clause,[],[f1245,f841,f1236]) ).
fof(f1305,plain,
! [X2,X0,X1] :
( stoppedIn(X0,X1,X2)
| ~ holdsAt(X1,plus(n1,sK1(X0,X1,X2)))
| stoppedIn(X0,X1,X2) ),
inference(resolution,[],[f485,f219]) ).
fof(f1306,plain,
! [X2,X0,X1] :
( ~ holdsAt(X1,plus(n1,sK1(X0,X1,X2)))
| stoppedIn(X0,X1,X2) ),
inference(duplicate_literal_removal,[],[f1305]) ).
fof(f1573,plain,
! [X0] :
( ~ stoppedIn(n0,filling,plus(n0,n1))
| less(n0,n1)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0)
| holdsAt(waterLevel(n1),plus(n0,n1)) ),
inference(resolution,[],[f874,f220]) ).
fof(f1574,plain,
! [X0] :
( ~ stoppedIn(n0,filling,plus(n0,n1))
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0)
| holdsAt(waterLevel(n1),plus(n0,n1)) ),
inference(forward_subsumption_resolution,[],[f1573,f287]) ).
fof(f1575,plain,
! [X0] :
( ~ stoppedIn(n0,filling,n1)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0)
| holdsAt(waterLevel(n1),plus(n0,n1)) ),
inference(forward_demodulation,[],[f1574,f153]) ).
fof(f1576,plain,
! [X0] :
( holdsAt(waterLevel(n1),n1)
| ~ stoppedIn(n0,filling,n1)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(forward_demodulation,[],[f1575,f153]) ).
fof(f1578,definition,
( spl10_114
<=> stoppedIn(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl10_114])],[avatar_definition]) ).
fof(f1580,plain,
( ~ stoppedIn(n0,filling,n1)
| spl10_114 ),
inference(avatar_component_clause,[],[f1578]) ).
fof(f1582,definition,
( spl10_115
<=> holdsAt(waterLevel(n1),n1) ),
introduced(definition,[new_symbols(definition,[spl10_115])],[avatar_definition]) ).
fof(f1584,plain,
( holdsAt(waterLevel(n1),n1)
| ~ spl10_115 ),
inference(avatar_component_clause,[],[f1582]) ).
fof(f1585,plain,
( spl10_60
| ~ spl10_114
| spl10_115 ),
inference(avatar_split_clause,[],[f1576,f1582,f1578,f880]) ).
fof(f1606,definition,
( spl10_119
<=> less(n0,n2) ),
introduced(definition,[new_symbols(definition,[spl10_119])],[avatar_definition]) ).
fof(f1607,plain,
( ~ less(n0,n2)
| spl10_119 ),
inference(avatar_component_clause,[],[f1606]) ).
fof(f1608,plain,
( less(n0,n2)
| ~ spl10_119 ),
inference(avatar_component_clause,[],[f1606]) ).
fof(f1610,definition,
( spl10_120
<=> stoppedIn(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl10_120])],[avatar_definition]) ).
fof(f1612,plain,
( ~ stoppedIn(n0,filling,n2)
| spl10_120 ),
inference(avatar_component_clause,[],[f1610]) ).
fof(f1614,definition,
( spl10_121
<=> holdsAt(waterLevel(n2),n2) ),
introduced(definition,[new_symbols(definition,[spl10_121])],[avatar_definition]) ).
fof(f1616,plain,
( holdsAt(waterLevel(n2),n2)
| ~ spl10_121 ),
inference(avatar_component_clause,[],[f1614]) ).
fof(f1769,plain,
( ~ happens(tapOn,n0)
| ~ spl10_60 ),
inference(resolution,[],[f881,f198]) ).
fof(f1773,plain,
( $false
| ~ spl10_60 ),
inference(forward_subsumption_resolution,[],[f1769,f211]) ).
fof(f1774,plain,
~ spl10_60,
inference(avatar_contradiction_clause,[],[f1773]) ).
fof(f1781,plain,
! [X0,X1] :
( ~ stoppedIn(n0,filling,plus(n0,X0))
| less(n0,X0)
| ~ initiates(X1,filling,n0)
| ~ happens(X1,n0)
| holdsAt(waterLevel(plus(X0,n0)),plus(n0,X0)) ),
inference(resolution,[],[f877,f220]) ).
fof(f1787,definition,
( spl10_129
<=> ! [X0] :
( ~ stoppedIn(n0,filling,plus(n0,X0))
| holdsAt(waterLevel(plus(X0,n0)),plus(n0,X0))
| less(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl10_129])],[avatar_definition]) ).
fof(f1788,plain,
( ! [X0] :
( ~ stoppedIn(n0,filling,plus(n0,X0))
| holdsAt(waterLevel(plus(X0,n0)),plus(n0,X0))
| less(n0,X0) )
| ~ spl10_129 ),
inference(avatar_component_clause,[],[f1787]) ).
fof(f1789,plain,
( spl10_60
| spl10_129 ),
inference(avatar_split_clause,[],[f1781,f1787,f880]) ).
fof(f2125,plain,
( n0 = sK1(n0,filling,n1)
| spl10_114 ),
inference(resolution,[],[f1580,f820]) ).
fof(f2135,definition,
( spl10_136
<=> n0 = sK1(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl10_136])],[avatar_definition]) ).
fof(f2137,plain,
( n0 = sK1(n0,filling,n1)
| ~ spl10_136 ),
inference(avatar_component_clause,[],[f2135]) ).
fof(f2149,plain,
( spl10_136
| spl10_114 ),
inference(avatar_split_clause,[],[f2125,f1578,f2135]) ).
fof(f2173,plain,
! [X0,X1] :
( stoppedIn(X0,X1,n2)
| n1 = sK1(X0,X1,n2)
| n0 = sK1(X0,X1,n2) ),
inference(resolution,[],[f904,f369]) ).
fof(f2226,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n1)
| n1 = X0 )
| ~ spl10_115 ),
inference(resolution,[],[f1584,f143]) ).
fof(f2358,definition,
( spl10_150
<=> holdsAt(waterLevel(n3),n2) ),
introduced(definition,[new_symbols(definition,[spl10_150])],[avatar_definition]) ).
fof(f2360,plain,
( holdsAt(waterLevel(n3),n2)
| ~ spl10_150 ),
inference(avatar_component_clause,[],[f2358]) ).
fof(f2403,definition,
( spl10_157
<=> n0 = sK1(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl10_157])],[avatar_definition]) ).
fof(f2405,plain,
( n0 = sK1(n0,filling,n2)
| ~ spl10_157 ),
inference(avatar_component_clause,[],[f2403]) ).
fof(f2447,plain,
( less(n0,n1)
| ~ spl10_119 ),
inference(resolution,[],[f1608,f291]) ).
fof(f2450,plain,
( $false
| ~ spl10_119 ),
inference(forward_subsumption_resolution,[],[f2447,f287]) ).
fof(f2451,plain,
~ spl10_119,
inference(avatar_contradiction_clause,[],[f2450]) ).
fof(f2468,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n2)
| n2 = X0 )
| ~ spl10_121 ),
inference(resolution,[],[f1616,f143]) ).
fof(f2575,plain,
( n0 = n1
| holdsAt(waterLevel(n3),n1)
| ~ spl10_54 ),
inference(resolution,[],[f839,f135]) ).
fof(f2599,definition,
( spl10_177
<=> n0 = n1 ),
introduced(definition,[new_symbols(definition,[spl10_177])],[avatar_definition]) ).
fof(f2601,plain,
( n0 = n1
| ~ spl10_177 ),
inference(avatar_component_clause,[],[f2599]) ).
fof(f2604,definition,
( spl10_178
<=> holdsAt(waterLevel(n3),n1) ),
introduced(definition,[new_symbols(definition,[spl10_178])],[avatar_definition]) ).
fof(f2606,plain,
( holdsAt(waterLevel(n3),n1)
| ~ spl10_178 ),
inference(avatar_component_clause,[],[f2604]) ).
fof(f2628,plain,
( ~ releasedAt(filling,plus(n2,n1))
| happens(sK2(filling,n2),n2)
| holdsAt(filling,plus(n2,n1))
| ~ spl10_56 ),
inference(resolution,[],[f847,f221]) ).
fof(f2629,plain,
( ~ releasedAt(filling,plus(n1,n2))
| happens(sK2(filling,n2),n2)
| holdsAt(filling,plus(n2,n1))
| ~ spl10_56 ),
inference(forward_demodulation,[],[f2628,f162]) ).
fof(f2631,plain,
( ~ releasedAt(filling,n3)
| happens(sK2(filling,n2),n2)
| holdsAt(filling,plus(n2,n1))
| ~ spl10_56 ),
inference(forward_demodulation,[],[f2629,f157]) ).
fof(f2633,plain,
( happens(sK2(filling,n2),n2)
| holdsAt(filling,plus(n2,n1))
| ~ spl10_56
| ~ spl10_89 ),
inference(forward_subsumption_resolution,[],[f2631,f1238]) ).
fof(f2635,plain,
( holdsAt(filling,plus(n1,n2))
| happens(sK2(filling,n2),n2)
| ~ spl10_56
| ~ spl10_89 ),
inference(forward_demodulation,[],[f2633,f162]) ).
fof(f2637,plain,
( holdsAt(filling,n3)
| happens(sK2(filling,n2),n2)
| ~ spl10_56
| ~ spl10_89 ),
inference(forward_demodulation,[],[f2635,f157]) ).
fof(f2639,plain,
( happens(sK2(filling,n2),n2)
| ~ spl10_56
| ~ spl10_89 ),
inference(forward_subsumption_resolution,[],[f2637,f194]) ).
fof(f2666,definition,
( spl10_181
<=> n0 = n2 ),
introduced(definition,[new_symbols(definition,[spl10_181])],[avatar_definition]) ).
fof(f2668,plain,
( n0 = n2
| ~ spl10_181 ),
inference(avatar_component_clause,[],[f2666]) ).
fof(f2678,plain,
( spl10_178
| spl10_177
| ~ spl10_54 ),
inference(avatar_split_clause,[],[f2575,f837,f2599,f2604]) ).
fof(f2688,plain,
( n2 = plus(n1,n2)
| ~ spl10_177 ),
inference(superposition,[],[f154,f2601]) ).
fof(f2747,plain,
( n3 = n2
| ~ spl10_177 ),
inference(forward_demodulation,[],[f2688,f157]) ).
fof(f2748,plain,
( spl10_13
| ~ spl10_177 ),
inference(avatar_split_clause,[],[f2747,f2599,f436]) ).
fof(f3278,plain,
( ~ less(n0,n0)
| stoppedIn(n0,filling,n1)
| ~ spl10_136 ),
inference(superposition,[],[f217,f2137]) ).
fof(f3317,plain,
( stoppedIn(n0,filling,n1)
| ~ spl10_136 ),
inference(forward_subsumption_resolution,[],[f3278,f261]) ).
fof(f3405,plain,
( spl10_114
| ~ spl10_136 ),
inference(avatar_split_clause,[],[f3317,f2135,f1578]) ).
fof(f5111,plain,
( n1 = sK1(n0,filling,n2)
| n0 = sK1(n0,filling,n2)
| spl10_120 ),
inference(resolution,[],[f2173,f1612]) ).
fof(f5113,definition,
( spl10_244
<=> n1 = sK1(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl10_244])],[avatar_definition]) ).
fof(f5115,plain,
( n1 = sK1(n0,filling,n2)
| ~ spl10_244 ),
inference(avatar_component_clause,[],[f5113]) ).
fof(f5116,plain,
( spl10_157
| spl10_244
| spl10_120 ),
inference(avatar_split_clause,[],[f5111,f1610,f5113,f2403]) ).
fof(f5145,plain,
( ~ stoppedIn(n0,filling,n2)
| holdsAt(waterLevel(plus(n2,n0)),n2)
| less(n0,n2)
| ~ spl10_129 ),
inference(superposition,[],[f1788,f154]) ).
fof(f5187,plain,
( ~ holdsAt(filling,plus(n1,n1))
| stoppedIn(n0,filling,n2)
| ~ spl10_244 ),
inference(superposition,[],[f1306,f5115]) ).
fof(f6700,plain,
( n1 = n3
| ~ spl10_115
| ~ spl10_178 ),
inference(resolution,[],[f2226,f2606]) ).
fof(f6716,plain,
( spl10_48
| ~ spl10_115
| ~ spl10_178 ),
inference(avatar_split_clause,[],[f6700,f2604,f1582,f778]) ).
fof(f6721,plain,
( ~ holdsAt(filling,n1)
| ~ spl10_48 ),
inference(superposition,[],[f194,f780]) ).
fof(f6837,plain,
( $false
| ~ spl10_48 ),
inference(forward_subsumption_resolution,[],[f6721,f829]) ).
fof(f6838,plain,
~ spl10_48,
inference(avatar_contradiction_clause,[],[f6837]) ).
fof(f6916,plain,
( ~ stoppedIn(n0,filling,n2)
| holdsAt(waterLevel(plus(n2,n0)),n2)
| spl10_119
| ~ spl10_129 ),
inference(forward_subsumption_resolution,[],[f5145,f1607]) ).
fof(f6917,plain,
( ~ holdsAt(filling,n2)
| stoppedIn(n0,filling,n2)
| ~ spl10_244 ),
inference(forward_demodulation,[],[f5187,f156]) ).
fof(f6985,plain,
( holdsAt(waterLevel(plus(n0,n2)),n2)
| ~ stoppedIn(n0,filling,n2)
| spl10_119
| ~ spl10_129 ),
inference(forward_demodulation,[],[f6916,f162]) ).
fof(f6986,plain,
( spl10_120
| ~ spl10_56
| ~ spl10_244 ),
inference(avatar_split_clause,[],[f6917,f5113,f845,f1610]) ).
fof(f7053,plain,
( holdsAt(waterLevel(n2),n2)
| ~ stoppedIn(n0,filling,n2)
| spl10_119
| ~ spl10_129 ),
inference(forward_demodulation,[],[f6985,f154]) ).
fof(f7104,plain,
( ~ spl10_120
| spl10_121
| spl10_119
| ~ spl10_129 ),
inference(avatar_split_clause,[],[f7053,f1787,f1606,f1614,f1610]) ).
fof(f7117,plain,
( n0 = n2
| holdsAt(waterLevel(n3),n2)
| ~ spl10_56
| ~ spl10_89 ),
inference(resolution,[],[f2639,f135]) ).
fof(f7136,plain,
( spl10_150
| spl10_181
| ~ spl10_56
| ~ spl10_89 ),
inference(avatar_split_clause,[],[f7117,f1236,f845,f2666,f2358]) ).
fof(f7434,plain,
( ~ less(n1,n0)
| ~ spl10_181 ),
inference(superposition,[],[f290,f2668]) ).
fof(f7550,plain,
( $false
| ~ spl10_181 ),
inference(forward_subsumption_resolution,[],[f7434,f261]) ).
fof(f7551,plain,
~ spl10_181,
inference(avatar_contradiction_clause,[],[f7550]) ).
fof(f7830,plain,
( n3 = n2
| ~ spl10_121
| ~ spl10_150 ),
inference(resolution,[],[f2468,f2360]) ).
fof(f7849,plain,
( spl10_13
| ~ spl10_121
| ~ spl10_150 ),
inference(avatar_split_clause,[],[f7830,f2358,f1614,f436]) ).
fof(f7857,plain,
( ~ less_or_equal(n3,n3)
| ~ spl10_13 ),
inference(superposition,[],[f292,f438]) ).
fof(f7978,plain,
( $false
| ~ spl10_13 ),
inference(forward_subsumption_resolution,[],[f7857,f214]) ).
fof(f7979,plain,
~ spl10_13,
inference(avatar_contradiction_clause,[],[f7978]) ).
fof(f8065,plain,
( ~ holdsAt(filling,plus(n1,n0))
| stoppedIn(n0,filling,n2)
| ~ spl10_157 ),
inference(superposition,[],[f1306,f2405]) ).
fof(f8100,plain,
( ~ holdsAt(filling,plus(n1,n0))
| spl10_120
| ~ spl10_157 ),
inference(forward_subsumption_resolution,[],[f8065,f1612]) ).
fof(f8159,plain,
( ~ holdsAt(filling,n1)
| spl10_120
| ~ spl10_157 ),
inference(forward_demodulation,[],[f8100,f324]) ).
fof(f8192,plain,
( $false
| spl10_120
| ~ spl10_157 ),
inference(forward_subsumption_resolution,[],[f8159,f829]) ).
fof(f8193,plain,
( spl10_120
| ~ spl10_157 ),
inference(avatar_contradiction_clause,[],[f8192]) ).
cnf(s31,plain,
( spl10_54
| ~ spl10_55
| spl10_56 ),
inference(sat_conversion,[],[f848]) ).
cnf(s33,plain,
spl10_18,
inference(sat_conversion,[],[f855]) ).
cnf(s49,plain,
( ~ spl10_18
| spl10_55 ),
inference(sat_conversion,[],[f1092]) ).
cnf(s63,plain,
( ~ spl10_55
| spl10_89 ),
inference(sat_conversion,[],[f1246]) ).
cnf(s88,plain,
( spl10_60
| ~ spl10_114
| spl10_115 ),
inference(sat_conversion,[],[f1585]) ).
cnf(s95,plain,
~ spl10_60,
inference(sat_conversion,[],[f1774]) ).
cnf(s97,plain,
( spl10_60
| spl10_129 ),
inference(sat_conversion,[],[f1789]) ).
cnf(s131,plain,
( spl10_114
| spl10_136 ),
inference(sat_conversion,[],[f2149]) ).
cnf(s150,plain,
~ spl10_119,
inference(sat_conversion,[],[f2451]) ).
cnf(s165,plain,
( ~ spl10_54
| spl10_177
| spl10_178 ),
inference(sat_conversion,[],[f2678]) ).
cnf(s176,plain,
( spl10_13
| ~ spl10_177 ),
inference(sat_conversion,[],[f2748]) ).
cnf(s236,plain,
( spl10_114
| ~ spl10_136 ),
inference(sat_conversion,[],[f3405]) ).
cnf(s350,plain,
( spl10_120
| spl10_157
| spl10_244 ),
inference(sat_conversion,[],[f5116]) ).
cnf(s378,plain,
( spl10_48
| ~ spl10_115
| ~ spl10_178 ),
inference(sat_conversion,[],[f6716]) ).
cnf(s383,plain,
~ spl10_48,
inference(sat_conversion,[],[f6838]) ).
cnf(s410,plain,
( ~ spl10_56
| spl10_120
| ~ spl10_244 ),
inference(sat_conversion,[],[f6986]) ).
cnf(s445,plain,
( spl10_119
| ~ spl10_120
| spl10_121
| ~ spl10_129 ),
inference(sat_conversion,[],[f7104]) ).
cnf(s458,plain,
( ~ spl10_56
| ~ spl10_89
| spl10_150
| spl10_181 ),
inference(sat_conversion,[],[f7136]) ).
cnf(s479,plain,
~ spl10_181,
inference(sat_conversion,[],[f7551]) ).
cnf(s507,plain,
( spl10_13
| ~ spl10_121
| ~ spl10_150 ),
inference(sat_conversion,[],[f7849]) ).
cnf(s512,plain,
~ spl10_13,
inference(sat_conversion,[],[f7979]) ).
cnf(s556,plain,
( spl10_120
| ~ spl10_157 ),
inference(sat_conversion,[],[f8193]) ).
cnf(s558,plain,
( ~ spl10_121
| ~ spl10_150 ),
inference(rat,[],[s507,s512]) ).
cnf(s566,plain,
( ~ spl10_56
| ~ spl10_89
| spl10_150 ),
inference(rat,[],[s458,s479]) ).
cnf(s570,plain,
( ~ spl10_115
| ~ spl10_178 ),
inference(rat,[],[s378,s383]) ).
cnf(s576,plain,
~ spl10_177,
inference(rat,[],[s176,s512]) ).
cnf(s578,plain,
( ~ spl10_54
| spl10_178 ),
inference(rat,[],[s165,s576]) ).
cnf(s586,plain,
spl10_129,
inference(rat,[],[s97,s95]) ).
cnf(s591,plain,
( ~ spl10_114
| spl10_115 ),
inference(rat,[],[s88,s95]) ).
cnf(s602,plain,
spl10_55,
inference(rat,[],[s49,s33]) ).
cnf(s603,plain,
spl10_89,
inference(rat,[],[s63,s602]) ).
cnf(s608,plain,
( spl10_54
| spl10_56 ),
inference(rat,[],[s31,s602]) ).
cnf(s611,plain,
~ spl10_56,
inference(rat,[],[s350,s410,s556,s445,s558,s566,s150,s586,s603]) ).
cnf(s613,plain,
spl10_54,
inference(rat,[],[s608,s611]) ).
cnf(s615,plain,
spl10_178,
inference(rat,[],[s578,s613]) ).
cnf(s617,plain,
~ spl10_115,
inference(rat,[],[s570,s615]) ).
cnf(s618,plain,
~ spl10_114,
inference(rat,[],[s591,s617]) ).
cnf(s619,plain,
~ spl10_136,
inference(rat,[],[s236,s618]) ).
cnf(s621,plain,
$false,
inference(rat,[],[s131,s619,s618]) ).
fof(f8202,plain,
$false,
inference(avatar_sat_refutation,[],[s621]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR005+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n013.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % 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:04:37 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 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.58/0.49 % (1636489)Will run a generic schedule for satisfiability detection.
% 1.58/0.49 % (1636499)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3663272497:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.58/0.49 % (1636495)% WARNING: option uhcvi not known.
% 1.58/0.49 % (1636497)dis+10_1_sil=32000:sp=arity:random_seed=838504308:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.58/0.49 % (1636494)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2347474998_2999 on theBenchmark for (2999ds/0Mi)
% 1.58/0.49 % (1636495)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4009822971:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.58/0.49 % (1636496)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3089138428:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.58/0.49 % (1636498)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3649261714:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.58/0.49 % (1636500)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1808228943:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.58/0.49 % Detected minimum model sizes of [3]
% 1.58/0.49 % Detected maximum model sizes of [max]
% 1.58/0.49 % TRYING [3]
% 1.58/0.49 % TRYING [4]
% 1.58/0.49 % TRYING [5]
% 1.58/0.49 % (1636499)Instruction limit reached!
% 1.58/0.49 % (1636499)------------------------------
% 1.58/0.49 % (1636499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.49 % (1636499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.49 % (1636499)CaDiCaL version: 2.1.3
% 1.58/0.49 % (1636499)Termination reason: Instruction limit
% 1.58/0.49 % (1636499)Termination phase: Saturation
% 1.58/0.49 % (1636499)Time elapsed: 0.046 s
% 1.58/0.49 % (1636499)Peak memory usage: 13 MB
% 1.58/0.49 % (1636499)Instructions burned: 131 (million)
% 1.58/0.49 % (1636508)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3248673980:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.58/0.49 % Detected minimum model sizes of [3]
% 1.58/0.49 % Detected maximum model sizes of [max]
% 1.58/0.49 % TRYING [3]
% 1.58/0.49 % TRYING [4]
% 1.58/0.49 % (1636497)Instruction limit reached!
% 1.58/0.49 % (1636497)------------------------------
% 1.58/0.49 % (1636497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.49 % (1636497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.49 % (1636497)CaDiCaL version: 2.1.3
% 1.58/0.49 % (1636497)Termination reason: Instruction limit
% 1.58/0.49 % (1636497)Termination phase: Saturation
% 1.58/0.49 % (1636497)Time elapsed: 0.070 s
% 1.58/0.49 % (1636497)Peak memory usage: 12 MB
% 1.58/0.49 % (1636497)Instructions burned: 104 (million)
% 1.58/0.49 % TRYING [5]
% 1.58/0.49 % TRYING [6]
% 1.58/0.49 % (1636498)Instruction limit reached!
% 1.58/0.49 % (1636498)------------------------------
% 1.58/0.49 % (1636498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.49 % (1636498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.49 % (1636498)CaDiCaL version: 2.1.3
% 1.58/0.49 % (1636498)Termination reason: Instruction limit
% 1.58/0.49 % (1636498)Termination phase: Saturation
% 1.58/0.49 % (1636498)Time elapsed: 0.078 s
% 1.58/0.49 % (1636498)Peak memory usage: 13 MB
% 1.58/0.49 % (1636498)Instructions burned: 117 (million)
% 1.58/0.49 % (1636500)Instruction limit reached!
% 1.58/0.49 % (1636500)------------------------------
% 1.58/0.49 % (1636500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.49 % (1636500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.49 % (1636500)CaDiCaL version: 2.1.3
% 1.58/0.49 % (1636500)Termination reason: Instruction limit
% 1.58/0.49 % (1636500)Termination phase: Saturation
% 1.58/0.49 % (1636500)Time elapsed: 0.085 s
% 1.58/0.49 % (1636500)Peak memory usage: 12 MB
% 1.58/0.49 % (1636500)Instructions burned: 159 (million)
% 1.58/0.49 % (1636510)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3855306625:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.58/0.49 % TRYING [6]
% 1.58/0.49 % (1636511)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=3140371050:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.58/0.49 % (1636512)ott-21_1_sil=16000:fs=off:random_seed=494228568:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.58/0.49 % TRYING [7]
% 1.58/0.49 % TRYING [7]
% 1.58/0.49 % (1636510)Instruction limit reached!
% 1.58/0.49 % (1636510)------------------------------
% 1.58/0.49 % (1636510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.49 % (1636510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.49 % (1636510)CaDiCaL version: 2.1.3
% 1.58/0.49 % (1636510)Termination reason: Instruction limit
% 1.58/0.49 % (1636510)Termination phase: Saturation
% 1.58/0.49 % (1636510)Time elapsed: 0.086 s
% 1.58/0.49 % (1636510)Peak memory usage: 13 MB
% 1.58/0.49 % (1636510)Instructions burned: 132 (million)
% 1.58/0.49 % (1636508)Instruction limit reached!
% 1.58/0.49 % (1636508)------------------------------
% 1.58/0.49 % (1636508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.49 % (1636508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.49 % (1636508)CaDiCaL version: 2.1.3
% 1.58/0.49 % (1636508)Termination reason: Instruction limit
% 1.58/0.49 % (1636508)Termination phase: Finite model building constraint generation
% 1.58/0.49 % (1636508)Time elapsed: 0.146 s
% 1.58/0.49 % (1636508)Peak memory usage: 28 MB
% 1.58/0.49 % (1636508)Instructions burned: 720 (million)
% 1.58/0.49 % (1636495) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1636489-1636495"...
% 1.58/0.49 % (1636516)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2933620253:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.58/0.49 % (1636512)Instruction limit reached!
% 1.58/0.49 % (1636512)------------------------------
% 1.58/0.49 % (1636512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.49 % (1636512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.49 % (1636512)CaDiCaL version: 2.1.3
% 1.58/0.49 % (1636512)Termination reason: Instruction limit
% 1.58/0.49 % (1636512)Termination phase: Saturation
% 1.58/0.49 % (1636512)Time elapsed: 0.096 s
% 1.58/0.49 % (1636512)Peak memory usage: 12 MB
% 1.58/0.49 % (1636512)Instructions burned: 182 (million)
% 1.58/0.49 % (1636495)...printing done.
% 1.58/0.49 % (1636495)Refutation found. Thanks to Tanya!
% 1.58/0.49 % SZS status Theorem for theBenchmark
% 1.58/0.49 % SZS output start Proof for theBenchmark
% See solution above
% 1.58/0.49 % (1636495)------------------------------
% 1.58/0.49 % (1636495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.58/0.49 % (1636495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.58/0.49 % (1636495)CaDiCaL version: 2.1.3
% 1.58/0.49 % (1636495)Termination reason: Refutation
% 1.58/0.49 % (1636495)Time elapsed: 0.202 s
% 1.58/0.49 % (1636495)Peak memory usage: 15 MB
% 1.58/0.49 % (1636495)Instructions burned: 316 (million)
% 1.58/0.49 % (1636489)Success in time 0.242 s
% 1.58/0.49 % Vampire exiting
%------------------------------------------------------------------------------