%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR004+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:41:56 AM UTC 2026
% Result : Theorem 9.20s 2.15s
% Output : Refutation 10.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 59
% Syntax : Number of formulae : 374 ( 72 unt; 31 def)
% Number of atoms : 1069 ( 210 equ)
% Maximal formula atoms : 18 ( 2 avg)
% Number of connectives : 1144 ( 449 ~; 525 |; 121 &)
% ( 42 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 43 ( 41 usr; 31 prp; 0-4 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-3 aty)
% Number of variables : 284 ( 0 sgn 262 !; 22 ?)
% 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/theBenchmark.p',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/theBenchmark.p',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/theBenchmark.p',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/theBenchmark.p',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/theBenchmark.p',happens_holds) ).
fof(f12,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& ( initiates(X0,X2,X1)
| terminates(X0,X2,X1) ) )
=> ~ releasedAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',happens_not_released) ).
fof(f13,axiom,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = overflow
& X1 = waterLevel(X3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',initiates_all_defn) ).
fof(f14,axiom,
! [X0,X1,X2] :
( terminates(X0,X1,X2)
<=> ( ( X0 = tapOff
& X1 = filling )
| ( X0 = overflow
& X1 = filling ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',terminates_all_defn) ).
fof(f16,axiom,
! [X0,X1] :
( happens(X0,X1)
<=> ( ( X0 = tapOn
& X1 = n0 )
| ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',happens_all_defn) ).
fof(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/theBenchmark.p',change_of_waterLevel) ).
fof(f18,axiom,
! [X0,X1,X2] :
( ( holdsAt(waterLevel(X1),X0)
& holdsAt(waterLevel(X2),X0) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',same_waterLevel) ).
fof(f20,axiom,
tapOff != overflow,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tapOff_not_overflow) ).
fof(f21,axiom,
overflow != tapOn,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',overflow_not_tapOn) ).
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(f29,axiom,
plus(n0,n3) = n3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus0_3) ).
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(f50,axiom,
~ holdsAt(filling,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_filling_0) ).
fof(f55,conjecture,
happens(overflow,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',overflow_3) ).
fof(f56,negated_conjecture,
~ happens(overflow,n3),
inference(negated_conjecture,[status(cth)],[f55]) ).
fof(f57,plain,
~ happens(overflow,n3),
inference(flattening,[],[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,
! [X0] : ~ less(X0,n0),
inference(ennf_transformation,[],[f38]) ).
fof(f60,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f61,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(flattening,[],[f60]) ).
fof(f62,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(ennf_transformation,[],[f17]) ).
fof(f63,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(flattening,[],[f62]) ).
fof(f64,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(f65,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(flattening,[],[f64]) ).
fof(f68,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f69,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(flattening,[],[f68]) ).
fof(f74,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(f75,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,[],[f74]) ).
fof(f76,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(f77,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,[],[f76]) ).
fof(f78,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f79,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(flattening,[],[f78]) ).
fof(f84,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(f85,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) )
| sP0(X2,X0,X1) ) ),
inference(definition_folding,[],[f58,f84]) ).
fof(f86,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(f87,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,[],[f86]) ).
fof(f88,plain,
! [X0] :
( ( less(X0,n1)
| ~ less_or_equal(X0,n0) )
& ( less_or_equal(X0,n0)
| ~ less(X0,n1) ) ),
inference(nnf_transformation,[],[f39]) ).
fof(f89,plain,
! [X0] :
( ( less(X0,n2)
| ~ less_or_equal(X0,n1) )
& ( less_or_equal(X0,n1)
| ~ less(X0,n2) ) ),
inference(nnf_transformation,[],[f40]) ).
fof(f90,plain,
! [X0] :
( ( less(X0,n3)
| ~ less_or_equal(X0,n2) )
& ( less_or_equal(X0,n2)
| ~ less(X0,n3) ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f97,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(nnf_transformation,[],[f48]) ).
fof(f98,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(flattening,[],[f97]) ).
fof(f99,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(f100,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,[],[f99]) ).
fof(f108,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ( ( tapOn != X0
| filling != X1 )
& ( overflow != X0
| spilling != X1 )
& ! [X3] :
( ~ holdsAt(waterLevel(X3),X2)
| tapOff != X0
| waterLevel(X3) != X1 )
& ~ sP0(X2,X0,X1) ) )
& ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) )
| sP0(X2,X0,X1)
| ~ initiates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f85]) ).
fof(f109,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ( ( tapOn != X0
| filling != X1 )
& ( overflow != X0
| spilling != X1 )
& ! [X3] :
( ~ holdsAt(waterLevel(X3),X2)
| tapOff != X0
| waterLevel(X3) != X1 )
& ~ sP0(X2,X0,X1) ) )
& ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) )
| sP0(X2,X0,X1)
| ~ initiates(X0,X1,X2) ) ),
inference(flattening,[],[f108]) ).
fof(f110,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ( ( tapOn != X0
| filling != X1 )
& ( overflow != X0
| spilling != X1 )
& ! [X3] :
( ~ holdsAt(waterLevel(X3),X2)
| tapOff != X0
| waterLevel(X3) != X1 )
& ~ sP0(X2,X0,X1) ) )
& ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ? [X4] :
( holdsAt(waterLevel(X4),X2)
& X0 = tapOff
& waterLevel(X4) = X1 )
| sP0(X2,X0,X1)
| ~ initiates(X0,X1,X2) ) ),
inference(rectify,[],[f109]) ).
fof(f111,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ( ( tapOn != X0
| filling != X1 )
& ( overflow != X0
| spilling != X1 )
& ! [X3] :
( ~ holdsAt(waterLevel(X3),X2)
| tapOff != X0
| waterLevel(X3) != X1 )
& ~ sP0(X2,X0,X1) ) )
& ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ( holdsAt(waterLevel(sK3(X0,X1,X2)),X2)
& X0 = tapOff
& waterLevel(sK3(X0,X1,X2)) = X1 )
| sP0(X2,X0,X1)
| ~ initiates(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X4,sK3(X0,X1,X2))],[f110]) ).
fof(f112,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(f113,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,[],[f112]) ).
fof(f114,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ( happens(sK4(X0,X1),X1)
& releases(sK4(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X2,sK4(X0,X1))],[f69]) ).
fof(f117,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ( happens(sK7(X0,X1),X1)
& terminates(sK7(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f75]) ).
fof(f121,plain,
! [X0,X1,X2] :
( ( stoppedIn(X0,X1,X2)
| ! [X3,X4] :
( ~ happens(X3,X4)
| ~ less(X0,X4)
| ~ less(X4,X2)
| ~ terminates(X3,X1,X4) ) )
& ( ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) )
| ~ stoppedIn(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f1]) ).
fof(f122,plain,
! [X0,X1,X2] :
( ( stoppedIn(X0,X1,X2)
| ! [X3,X4] :
( ~ happens(X3,X4)
| ~ less(X0,X4)
| ~ less(X4,X2)
| ~ terminates(X3,X1,X4) ) )
& ( ? [X5,X6] :
( happens(X5,X6)
& less(X0,X6)
& less(X6,X2)
& terminates(X5,X1,X6) )
| ~ stoppedIn(X0,X1,X2) ) ),
inference(rectify,[],[f121]) ).
fof(f123,plain,
! [X0,X1,X2] :
( ( stoppedIn(X0,X1,X2)
| ! [X3,X4] :
( ~ happens(X3,X4)
| ~ less(X0,X4)
| ~ less(X4,X2)
| ~ terminates(X3,X1,X4) ) )
& ( ( happens(sK10(X0,X1,X2),sK11(X0,X1,X2))
& less(X0,sK11(X0,X1,X2))
& less(sK11(X0,X1,X2),X2)
& terminates(sK10(X0,X1,X2),X1,sK11(X0,X1,X2)) )
| ~ stoppedIn(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11]),skolemize(X5,sK10(X0,X1,X2)),skolemize(X6,sK11(X0,X1,X2))],[f122]) ).
fof(f125,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f27]) ).
fof(f126,plain,
n2 = plus(n0,n2),
inference(cnf_transformation,[],[f28]) ).
fof(f127,plain,
n3 = plus(n0,n3),
inference(cnf_transformation,[],[f29]) ).
fof(f128,plain,
n2 = plus(n1,n1),
inference(cnf_transformation,[],[f30]) ).
fof(f129,plain,
n3 = plus(n1,n2),
inference(cnf_transformation,[],[f31]) ).
fof(f134,plain,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[],[f36]) ).
fof(f135,plain,
! [X0,X1] :
( ~ less_or_equal(X0,X1)
| X0 = X1
| less(X0,X1) ),
inference(cnf_transformation,[],[f87]) ).
fof(f136,plain,
! [X0,X1] :
( less_or_equal(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f87]) ).
fof(f137,plain,
! [X0,X1] :
( less_or_equal(X0,X1)
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f87]) ).
fof(f138,plain,
! [X0] : ~ less(X0,n0),
inference(cnf_transformation,[],[f59]) ).
fof(f139,plain,
! [X0] :
( less_or_equal(X0,n0)
| ~ less(X0,n1) ),
inference(cnf_transformation,[],[f88]) ).
fof(f140,plain,
! [X0] :
( ~ less_or_equal(X0,n0)
| less(X0,n1) ),
inference(cnf_transformation,[],[f88]) ).
fof(f141,plain,
! [X0] :
( less_or_equal(X0,n1)
| ~ less(X0,n2) ),
inference(cnf_transformation,[],[f89]) ).
fof(f142,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| less(X0,n2) ),
inference(cnf_transformation,[],[f89]) ).
fof(f143,plain,
! [X0] :
( less_or_equal(X0,n2)
| ~ less(X0,n3) ),
inference(cnf_transformation,[],[f90]) ).
fof(f144,plain,
! [X0] :
( ~ less_or_equal(X0,n2)
| less(X0,n3) ),
inference(cnf_transformation,[],[f90]) ).
fof(f157,plain,
! [X0,X1] :
( X0 != X1
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f98]) ).
fof(f159,plain,
! [X0,X1] :
( less(X0,X1)
| less(X1,X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f98]) ).
fof(f160,plain,
holdsAt(waterLevel(n0),n0),
inference(cnf_transformation,[],[f49]) ).
fof(f161,plain,
~ holdsAt(filling,n0),
inference(cnf_transformation,[],[f50]) ).
fof(f166,plain,
~ happens(overflow,n3),
inference(cnf_transformation,[],[f57]) ).
fof(f167,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| overflow = X0
| n0 = X1 ),
inference(cnf_transformation,[],[f100]) ).
fof(f169,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| holdsAt(waterLevel(n3),X1)
| n0 = X1 ),
inference(cnf_transformation,[],[f100]) ).
fof(f172,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| holdsAt(waterLevel(n3),X1)
| tapOn = X0 ),
inference(cnf_transformation,[],[f100]) ).
fof(f173,plain,
! [X0,X1] :
( happens(X0,X1)
| ~ holdsAt(waterLevel(n3),X1)
| ~ holdsAt(filling,X1)
| overflow != X0 ),
inference(cnf_transformation,[],[f100]) ).
fof(f174,plain,
! [X0,X1] :
( happens(X0,X1)
| tapOn != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f100]) ).
fof(f179,plain,
! [X2,X0,X1] :
( ~ holdsAt(waterLevel(X2),X0)
| ~ holdsAt(waterLevel(X1),X0)
| X1 = X2 ),
inference(cnf_transformation,[],[f61]) ).
fof(f180,plain,
! [X2,X3,X0,X1] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(cnf_transformation,[],[f63]) ).
fof(f203,plain,
! [X2,X0,X1] :
( initiates(X0,X1,X2)
| tapOn != X0
| filling != X1 ),
inference(cnf_transformation,[],[f111]) ).
fof(f208,plain,
! [X2,X0,X1] :
( ~ terminates(X0,X1,X2)
| overflow = X0
| tapOff = X0 ),
inference(cnf_transformation,[],[f113]) ).
fof(f212,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| ~ releasedAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f65]) ).
fof(f215,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| happens(sK4(X0,X1),X1) ),
inference(cnf_transformation,[],[f114]) ).
fof(f221,plain,
! [X0,X1] :
( ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1))
| releasedAt(X0,plus(X1,n1))
| happens(sK7(X0,X1),X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f222,plain,
tapOn != overflow,
inference(cnf_transformation,[],[f21]) ).
fof(f223,plain,
overflow != tapOff,
inference(cnf_transformation,[],[f20]) ).
fof(f225,plain,
! [X2,X3,X0,X1,X4] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X3,plus(X1,X4))
| ~ less(n0,X4)
| ~ trajectory(X2,X1,X3,X4)
| stoppedIn(X1,X2,plus(X1,X4)) ),
inference(cnf_transformation,[],[f77]) ).
fof(f226,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f234,plain,
! [X2,X0,X1] :
( terminates(sK10(X0,X1,X2),X1,sK11(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f123]) ).
fof(f235,plain,
! [X2,X0,X1] :
( less(sK11(X0,X1,X2),X2)
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f123]) ).
fof(f236,plain,
! [X2,X0,X1] :
( less(X0,sK11(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f123]) ).
fof(f237,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| happens(sK10(X0,X1,X2),sK11(X0,X1,X2)) ),
inference(cnf_transformation,[],[f123]) ).
fof(f239,plain,
! [X1] : less_or_equal(X1,X1),
inference(equality_resolution,[],[f136]) ).
fof(f240,plain,
! [X1] : ~ less(X1,X1),
inference(equality_resolution,[],[f157]) ).
fof(f241,plain,
! [X1] :
( happens(tapOn,X1)
| n0 != X1 ),
inference(equality_resolution,[],[f174]) ).
fof(f242,plain,
happens(tapOn,n0),
inference(equality_resolution,[],[f241]) ).
fof(f243,plain,
! [X1] :
( ~ holdsAt(waterLevel(n3),X1)
| happens(overflow,X1)
| ~ holdsAt(filling,X1) ),
inference(equality_resolution,[],[f173]) ).
fof(f245,plain,
! [X3,X0,X1] :
( ~ holdsAt(waterLevel(X0),X1)
| trajectory(filling,X1,waterLevel(plus(X0,X3)),X3) ),
inference(equality_resolution,[],[f180]) ).
fof(f250,plain,
! [X2,X1] :
( initiates(tapOn,X1,X2)
| filling != X1 ),
inference(equality_resolution,[],[f203]) ).
fof(f251,plain,
! [X2] : initiates(tapOn,filling,X2),
inference(equality_resolution,[],[f250]) ).
fof(f262,plain,
n1 = plus(n1,n0),
inference(forward_demodulation,[],[f125,f134]) ).
fof(f265,plain,
less(n2,n3),
inference(resolution,[],[f239,f144]) ).
fof(f268,plain,
! [X0] :
( ~ less(X0,n2)
| less(X0,n3) ),
inference(resolution,[],[f137,f144]) ).
fof(f270,plain,
less(n1,n2),
inference(resolution,[],[f142,f239]) ).
fof(f271,plain,
! [X0] :
( less(X0,n2)
| ~ less(X0,n1) ),
inference(resolution,[],[f142,f137]) ).
fof(f278,plain,
! [X0] :
( ~ less(X0,n2)
| n1 = X0
| less(X0,n1) ),
inference(resolution,[],[f141,f135]) ).
fof(f280,plain,
! [X0,X1] :
( ~ stoppedIn(X0,X1,n2)
| less(sK11(X0,X1,n2),n1)
| n1 = sK11(X0,X1,n2) ),
inference(resolution,[],[f278,f235]) ).
fof(f282,plain,
! [X0] :
( ~ less(X0,n3)
| n2 = X0
| less(X0,n2) ),
inference(resolution,[],[f143,f135]) ).
fof(f284,plain,
! [X0,X1] :
( ~ stoppedIn(X0,X1,n3)
| less(sK11(X0,X1,n3),n2)
| n2 = sK11(X0,X1,n3) ),
inference(resolution,[],[f282,f235]) ).
fof(f285,plain,
less(n0,n1),
inference(resolution,[],[f140,f239]) ).
fof(f318,plain,
! [X0] :
( ~ less(X0,n1)
| n0 = X0
| less(X0,n0) ),
inference(resolution,[],[f139,f135]) ).
fof(f319,plain,
! [X0] :
( ~ less(X0,n1)
| n0 = X0 ),
inference(forward_subsumption_resolution,[],[f318,f138]) ).
fof(f321,plain,
! [X0,X1] :
( ~ stoppedIn(X0,X1,n1)
| n0 = sK11(X0,X1,n1) ),
inference(resolution,[],[f319,f235]) ).
fof(f322,plain,
! [X0] :
( ~ releasedAt(X0,n2)
| releasedAt(X0,n1)
| happens(sK4(X0,n1),n1) ),
inference(superposition,[],[f215,f128]) ).
fof(f324,plain,
! [X0,X1] :
( ~ releasedAt(X1,plus(n1,X0))
| releasedAt(X1,X0)
| happens(sK4(X1,X0),X0) ),
inference(superposition,[],[f215,f134]) ).
fof(f332,plain,
! [X0] :
( less(n0,X0)
| n0 = X0 ),
inference(resolution,[],[f159,f138]) ).
fof(f341,plain,
~ less(n2,n1),
inference(resolution,[],[f271,f240]) ).
fof(f342,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(n0,X0)),X0),
inference(resolution,[],[f245,f160]) ).
fof(f343,plain,
trajectory(filling,n0,waterLevel(n2),n2),
inference(superposition,[],[f342,f126]) ).
fof(f344,plain,
trajectory(filling,n0,waterLevel(n3),n3),
inference(superposition,[],[f342,f127]) ).
fof(f347,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(X0,n0)),X0),
inference(superposition,[],[f342,f134]) ).
fof(f348,plain,
trajectory(filling,n0,waterLevel(n1),n1),
inference(superposition,[],[f347,f262]) ).
fof(f382,plain,
( n0 = n2
| less(n0,n3) ),
inference(resolution,[],[f332,f268]) ).
fof(f385,definition,
( spl12_5
<=> less(n0,n3) ),
introduced(definition,[new_symbols(definition,[spl12_5])],[avatar_definition]) ).
fof(f386,plain,
( less(n0,n3)
| ~ spl12_5 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f388,definition,
( spl12_6
<=> n0 = n2 ),
introduced(definition,[new_symbols(definition,[spl12_6])],[avatar_definition]) ).
fof(f389,plain,
( n0 = n2
| ~ spl12_6 ),
inference(avatar_component_clause,[],[f388]) ).
fof(f390,plain,
( spl12_5
| spl12_6 ),
inference(avatar_split_clause,[],[f382,f388,f385]) ).
fof(f409,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| tapOff = sK10(X0,X1,X2)
| overflow = sK10(X0,X1,X2) ),
inference(resolution,[],[f208,f234]) ).
fof(f413,plain,
! [X0] :
( ~ releasedAt(X0,n3)
| releasedAt(X0,n2)
| happens(sK4(X0,n2),n2) ),
inference(superposition,[],[f324,f129]) ).
fof(f557,definition,
( spl12_20
<=> holdsAt(waterLevel(n3),n1) ),
introduced(definition,[new_symbols(definition,[spl12_20])],[avatar_definition]) ).
fof(f558,plain,
( holdsAt(waterLevel(n3),n1)
| ~ spl12_20 ),
inference(avatar_component_clause,[],[f557]) ).
fof(f561,definition,
( spl12_21
<=> holdsAt(filling,n1) ),
introduced(definition,[new_symbols(definition,[spl12_21])],[avatar_definition]) ).
fof(f562,plain,
( holdsAt(filling,n1)
| ~ spl12_21 ),
inference(avatar_component_clause,[],[f561]) ).
fof(f569,definition,
( spl12_23
<=> n0 = n1 ),
introduced(definition,[new_symbols(definition,[spl12_23])],[avatar_definition]) ).
fof(f570,plain,
( n0 = n1
| ~ spl12_23 ),
inference(avatar_component_clause,[],[f569]) ).
fof(f634,plain,
( ~ holdsAt(filling,n1)
| ~ spl12_23 ),
inference(superposition,[],[f161,f570]) ).
fof(f662,plain,
( $false
| ~ spl12_21
| ~ spl12_23 ),
inference(forward_subsumption_resolution,[],[f634,f562]) ).
fof(f663,plain,
( ~ spl12_21
| ~ spl12_23 ),
inference(avatar_contradiction_clause,[],[f662]) ).
fof(f674,plain,
( holdsAt(filling,plus(n1,n1))
| releasedAt(filling,plus(n1,n1))
| happens(sK7(filling,n1),n1)
| ~ spl12_21 ),
inference(resolution,[],[f562,f221]) ).
fof(f675,plain,
( holdsAt(filling,n2)
| releasedAt(filling,plus(n1,n1))
| happens(sK7(filling,n1),n1)
| ~ spl12_21 ),
inference(forward_demodulation,[],[f674,f128]) ).
fof(f676,plain,
( releasedAt(filling,n2)
| holdsAt(filling,n2)
| happens(sK7(filling,n1),n1)
| ~ spl12_21 ),
inference(forward_demodulation,[],[f675,f128]) ).
fof(f678,definition,
( spl12_28
<=> happens(sK7(filling,n1),n1) ),
introduced(definition,[new_symbols(definition,[spl12_28])],[avatar_definition]) ).
fof(f679,plain,
( happens(sK7(filling,n1),n1)
| ~ spl12_28 ),
inference(avatar_component_clause,[],[f678]) ).
fof(f681,definition,
( spl12_29
<=> holdsAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl12_29])],[avatar_definition]) ).
fof(f682,plain,
( holdsAt(filling,n2)
| ~ spl12_29 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f684,definition,
( spl12_30
<=> releasedAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl12_30])],[avatar_definition]) ).
fof(f685,plain,
( releasedAt(filling,n2)
| ~ spl12_30 ),
inference(avatar_component_clause,[],[f684]) ).
fof(f686,plain,
( spl12_28
| spl12_29
| spl12_30
| ~ spl12_21 ),
inference(avatar_split_clause,[],[f676,f561,f684,f681,f678]) ).
fof(f700,plain,
( holdsAt(waterLevel(n3),n1)
| n0 = n1
| ~ spl12_28 ),
inference(resolution,[],[f679,f169]) ).
fof(f716,plain,
( spl12_23
| spl12_20
| ~ spl12_28 ),
inference(avatar_split_clause,[],[f700,f678,f557,f569]) ).
fof(f718,plain,
( releasedAt(filling,n1)
| happens(sK4(filling,n1),n1)
| ~ spl12_30 ),
inference(resolution,[],[f685,f322]) ).
fof(f722,definition,
( spl12_35
<=> happens(sK4(filling,n1),n1) ),
introduced(definition,[new_symbols(definition,[spl12_35])],[avatar_definition]) ).
fof(f723,plain,
( happens(sK4(filling,n1),n1)
| ~ spl12_35 ),
inference(avatar_component_clause,[],[f722]) ).
fof(f725,definition,
( spl12_36
<=> releasedAt(filling,n1) ),
introduced(definition,[new_symbols(definition,[spl12_36])],[avatar_definition]) ).
fof(f726,plain,
( releasedAt(filling,n1)
| ~ spl12_36 ),
inference(avatar_component_clause,[],[f725]) ).
fof(f727,plain,
( spl12_35
| spl12_36
| ~ spl12_30 ),
inference(avatar_split_clause,[],[f718,f684,f725,f722]) ).
fof(f733,definition,
( spl12_38
<=> releasedAt(filling,n3) ),
introduced(definition,[new_symbols(definition,[spl12_38])],[avatar_definition]) ).
fof(f734,plain,
( releasedAt(filling,n3)
| ~ spl12_38 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f750,definition,
( spl12_40
<=> holdsAt(waterLevel(n3),n2) ),
introduced(definition,[new_symbols(definition,[spl12_40])],[avatar_definition]) ).
fof(f751,plain,
( holdsAt(waterLevel(n3),n2)
| ~ spl12_40 ),
inference(avatar_component_clause,[],[f750]) ).
fof(f770,plain,
( less(n1,n0)
| ~ spl12_6 ),
inference(superposition,[],[f270,f389]) ).
fof(f792,plain,
( $false
| ~ spl12_6 ),
inference(forward_subsumption_resolution,[],[f770,f138]) ).
fof(f793,plain,
~ spl12_6,
inference(avatar_contradiction_clause,[],[f792]) ).
fof(f798,plain,
( releasedAt(filling,n2)
| happens(sK4(filling,n2),n2)
| ~ spl12_38 ),
inference(resolution,[],[f734,f413]) ).
fof(f811,plain,
( holdsAt(waterLevel(n3),n1)
| n0 = n1
| ~ spl12_35 ),
inference(resolution,[],[f723,f169]) ).
fof(f827,plain,
( spl12_23
| spl12_20
| ~ spl12_35 ),
inference(avatar_split_clause,[],[f811,f722,f557,f569]) ).
fof(f830,definition,
( spl12_46
<=> happens(sK4(filling,n2),n2) ),
introduced(definition,[new_symbols(definition,[spl12_46])],[avatar_definition]) ).
fof(f831,plain,
( happens(sK4(filling,n2),n2)
| ~ spl12_46 ),
inference(avatar_component_clause,[],[f830]) ).
fof(f832,plain,
( spl12_46
| spl12_30
| ~ spl12_38 ),
inference(avatar_split_clause,[],[f798,f733,f684,f830]) ).
fof(f835,plain,
( holdsAt(filling,plus(n2,n1))
| releasedAt(filling,plus(n2,n1))
| happens(sK7(filling,n2),n2)
| ~ spl12_29 ),
inference(resolution,[],[f682,f221]) ).
fof(f836,plain,
( holdsAt(filling,plus(n1,n2))
| releasedAt(filling,plus(n2,n1))
| happens(sK7(filling,n2),n2)
| ~ spl12_29 ),
inference(forward_demodulation,[],[f835,f134]) ).
fof(f837,plain,
( holdsAt(filling,n3)
| releasedAt(filling,plus(n2,n1))
| happens(sK7(filling,n2),n2)
| ~ spl12_29 ),
inference(forward_demodulation,[],[f836,f129]) ).
fof(f838,plain,
( releasedAt(filling,plus(n1,n2))
| holdsAt(filling,n3)
| happens(sK7(filling,n2),n2)
| ~ spl12_29 ),
inference(forward_demodulation,[],[f837,f134]) ).
fof(f839,plain,
( releasedAt(filling,n3)
| holdsAt(filling,n3)
| happens(sK7(filling,n2),n2)
| ~ spl12_29 ),
inference(forward_demodulation,[],[f838,f129]) ).
fof(f842,plain,
( holdsAt(waterLevel(n3),n2)
| n0 = n2
| ~ spl12_46 ),
inference(resolution,[],[f831,f169]) ).
fof(f858,plain,
( spl12_6
| spl12_40
| ~ spl12_46 ),
inference(avatar_split_clause,[],[f842,f830,f750,f388]) ).
fof(f862,definition,
( spl12_49
<=> happens(sK7(filling,n2),n2) ),
introduced(definition,[new_symbols(definition,[spl12_49])],[avatar_definition]) ).
fof(f863,plain,
( happens(sK7(filling,n2),n2)
| ~ spl12_49 ),
inference(avatar_component_clause,[],[f862]) ).
fof(f865,definition,
( spl12_50
<=> holdsAt(filling,n3) ),
introduced(definition,[new_symbols(definition,[spl12_50])],[avatar_definition]) ).
fof(f866,plain,
( holdsAt(filling,n3)
| ~ spl12_50 ),
inference(avatar_component_clause,[],[f865]) ).
fof(f867,plain,
( spl12_49
| spl12_50
| spl12_38
| ~ spl12_29 ),
inference(avatar_split_clause,[],[f839,f681,f733,f865,f862]) ).
fof(f1031,plain,
! [X0] :
( ~ happens(tapOn,X0)
| ~ releasedAt(filling,plus(X0,n1)) ),
inference(resolution,[],[f251,f212]) ).
fof(f1032,plain,
! [X2,X0,X1] :
( ~ happens(tapOn,X0)
| holdsAt(X1,plus(X0,X2))
| ~ less(n0,X2)
| ~ trajectory(filling,X0,X1,X2)
| stoppedIn(X0,filling,plus(X0,X2)) ),
inference(resolution,[],[f251,f225]) ).
fof(f1033,plain,
! [X0] :
( ~ happens(tapOn,X0)
| holdsAt(filling,plus(X0,n1)) ),
inference(resolution,[],[f251,f226]) ).
fof(f1034,plain,
! [X0,X1] :
( ~ trajectory(filling,n0,X0,X1)
| ~ less(n0,X1)
| holdsAt(X0,plus(n0,X1))
| stoppedIn(n0,filling,plus(n0,X1)) ),
inference(resolution,[],[f1032,f242]) ).
fof(f1038,plain,
( ~ less(n0,n1)
| holdsAt(waterLevel(n1),plus(n0,n1))
| stoppedIn(n0,filling,plus(n0,n1)) ),
inference(resolution,[],[f1034,f348]) ).
fof(f1039,plain,
( ~ less(n0,n3)
| holdsAt(waterLevel(n3),plus(n0,n3))
| stoppedIn(n0,filling,plus(n0,n3)) ),
inference(resolution,[],[f1034,f344]) ).
fof(f1040,plain,
( ~ less(n0,n2)
| holdsAt(waterLevel(n2),plus(n0,n2))
| stoppedIn(n0,filling,plus(n0,n2)) ),
inference(resolution,[],[f1034,f343]) ).
fof(f1041,plain,
( holdsAt(waterLevel(n2),n2)
| ~ less(n0,n2)
| stoppedIn(n0,filling,plus(n0,n2)) ),
inference(forward_demodulation,[],[f1040,f126]) ).
fof(f1042,plain,
( holdsAt(waterLevel(n3),plus(n0,n3))
| stoppedIn(n0,filling,plus(n0,n3))
| ~ spl12_5 ),
inference(forward_subsumption_resolution,[],[f1039,f386]) ).
fof(f1043,plain,
( holdsAt(waterLevel(n1),plus(n0,n1))
| stoppedIn(n0,filling,plus(n0,n1)) ),
inference(forward_subsumption_resolution,[],[f1038,f285]) ).
fof(f1044,plain,
( stoppedIn(n0,filling,n2)
| holdsAt(waterLevel(n2),n2)
| ~ less(n0,n2) ),
inference(forward_demodulation,[],[f1041,f126]) ).
fof(f1045,plain,
( holdsAt(waterLevel(n3),n3)
| stoppedIn(n0,filling,plus(n0,n3))
| ~ spl12_5 ),
inference(forward_demodulation,[],[f1042,f127]) ).
fof(f1046,plain,
( holdsAt(waterLevel(n1),plus(n1,n0))
| stoppedIn(n0,filling,plus(n0,n1)) ),
inference(forward_demodulation,[],[f1043,f134]) ).
fof(f1048,definition,
( spl12_53
<=> less(n0,n2) ),
introduced(definition,[new_symbols(definition,[spl12_53])],[avatar_definition]) ).
fof(f1049,plain,
( ~ less(n0,n2)
| spl12_53 ),
inference(avatar_component_clause,[],[f1048]) ).
fof(f1051,definition,
( spl12_54
<=> holdsAt(waterLevel(n2),n2) ),
introduced(definition,[new_symbols(definition,[spl12_54])],[avatar_definition]) ).
fof(f1052,plain,
( holdsAt(waterLevel(n2),n2)
| ~ spl12_54 ),
inference(avatar_component_clause,[],[f1051]) ).
fof(f1054,definition,
( spl12_55
<=> stoppedIn(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl12_55])],[avatar_definition]) ).
fof(f1055,plain,
( stoppedIn(n0,filling,n2)
| ~ spl12_55 ),
inference(avatar_component_clause,[],[f1054]) ).
fof(f1056,plain,
( ~ spl12_53
| spl12_54
| spl12_55 ),
inference(avatar_split_clause,[],[f1044,f1054,f1051,f1048]) ).
fof(f1057,plain,
( stoppedIn(n0,filling,n3)
| holdsAt(waterLevel(n3),n3)
| ~ spl12_5 ),
inference(forward_demodulation,[],[f1045,f127]) ).
fof(f1058,plain,
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,plus(n0,n1)) ),
inference(forward_demodulation,[],[f1046,f262]) ).
fof(f1060,definition,
( spl12_56
<=> holdsAt(waterLevel(n3),n3) ),
introduced(definition,[new_symbols(definition,[spl12_56])],[avatar_definition]) ).
fof(f1061,plain,
( holdsAt(waterLevel(n3),n3)
| ~ spl12_56 ),
inference(avatar_component_clause,[],[f1060]) ).
fof(f1063,definition,
( spl12_57
<=> stoppedIn(n0,filling,n3) ),
introduced(definition,[new_symbols(definition,[spl12_57])],[avatar_definition]) ).
fof(f1064,plain,
( stoppedIn(n0,filling,n3)
| ~ spl12_57 ),
inference(avatar_component_clause,[],[f1063]) ).
fof(f1065,plain,
( spl12_56
| spl12_57
| ~ spl12_5 ),
inference(avatar_split_clause,[],[f1057,f385,f1063,f1060]) ).
fof(f1066,plain,
( stoppedIn(n0,filling,plus(n1,n0))
| holdsAt(waterLevel(n1),n1) ),
inference(forward_demodulation,[],[f1058,f134]) ).
fof(f1067,plain,
( stoppedIn(n0,filling,n1)
| holdsAt(waterLevel(n1),n1) ),
inference(forward_demodulation,[],[f1066,f262]) ).
fof(f1069,definition,
( spl12_58
<=> holdsAt(waterLevel(n1),n1) ),
introduced(definition,[new_symbols(definition,[spl12_58])],[avatar_definition]) ).
fof(f1070,plain,
( holdsAt(waterLevel(n1),n1)
| ~ spl12_58 ),
inference(avatar_component_clause,[],[f1069]) ).
fof(f1072,definition,
( spl12_59
<=> stoppedIn(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl12_59])],[avatar_definition]) ).
fof(f1073,plain,
( stoppedIn(n0,filling,n1)
| ~ spl12_59 ),
inference(avatar_component_clause,[],[f1072]) ).
fof(f1074,plain,
( spl12_58
| spl12_59 ),
inference(avatar_split_clause,[],[f1067,f1072,f1069]) ).
fof(f1078,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n1)
| n1 = X0 )
| ~ spl12_58 ),
inference(resolution,[],[f1070,f179]) ).
fof(f1114,plain,
( happens(overflow,n3)
| ~ holdsAt(filling,n3)
| ~ spl12_56 ),
inference(resolution,[],[f1061,f243]) ).
fof(f1130,plain,
( ~ holdsAt(filling,n3)
| ~ spl12_56 ),
inference(forward_subsumption_resolution,[],[f1114,f166]) ).
fof(f1132,plain,
( $false
| ~ spl12_50
| ~ spl12_56 ),
inference(forward_subsumption_resolution,[],[f1130,f866]) ).
fof(f1133,plain,
( ~ spl12_50
| ~ spl12_56 ),
inference(avatar_contradiction_clause,[],[f1132]) ).
fof(f1149,plain,
( ~ less(n0,n1)
| spl12_53 ),
inference(resolution,[],[f1049,f271]) ).
fof(f1155,plain,
( $false
| spl12_53 ),
inference(forward_subsumption_resolution,[],[f1149,f285]) ).
fof(f1156,plain,
spl12_53,
inference(avatar_contradiction_clause,[],[f1155]) ).
fof(f1166,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n2)
| n2 = X0 )
| ~ spl12_54 ),
inference(resolution,[],[f1052,f179]) ).
fof(f1231,plain,
( less(sK11(n0,filling,n3),n2)
| n2 = sK11(n0,filling,n3)
| ~ spl12_57 ),
inference(resolution,[],[f1064,f284]) ).
fof(f1235,plain,
( tapOff = sK10(n0,filling,n3)
| overflow = sK10(n0,filling,n3)
| ~ spl12_57 ),
inference(resolution,[],[f1064,f409]) ).
fof(f1236,plain,
( happens(sK10(n0,filling,n3),sK11(n0,filling,n3))
| ~ spl12_57 ),
inference(resolution,[],[f1064,f237]) ).
fof(f1238,definition,
( spl12_81
<=> overflow = sK10(n0,filling,n3) ),
introduced(definition,[new_symbols(definition,[spl12_81])],[avatar_definition]) ).
fof(f1239,plain,
( overflow = sK10(n0,filling,n3)
| ~ spl12_81 ),
inference(avatar_component_clause,[],[f1238]) ).
fof(f1241,definition,
( spl12_82
<=> tapOff = sK10(n0,filling,n3) ),
introduced(definition,[new_symbols(definition,[spl12_82])],[avatar_definition]) ).
fof(f1242,plain,
( tapOff = sK10(n0,filling,n3)
| ~ spl12_82 ),
inference(avatar_component_clause,[],[f1241]) ).
fof(f1243,plain,
( spl12_81
| spl12_82
| ~ spl12_57 ),
inference(avatar_split_clause,[],[f1235,f1063,f1241,f1238]) ).
fof(f1245,definition,
( spl12_83
<=> n2 = sK11(n0,filling,n3) ),
introduced(definition,[new_symbols(definition,[spl12_83])],[avatar_definition]) ).
fof(f1246,plain,
( n2 = sK11(n0,filling,n3)
| ~ spl12_83 ),
inference(avatar_component_clause,[],[f1245]) ).
fof(f1248,definition,
( spl12_84
<=> less(sK11(n0,filling,n3),n2) ),
introduced(definition,[new_symbols(definition,[spl12_84])],[avatar_definition]) ).
fof(f1249,plain,
( less(sK11(n0,filling,n3),n2)
| ~ spl12_84 ),
inference(avatar_component_clause,[],[f1248]) ).
fof(f1250,plain,
( spl12_83
| spl12_84
| ~ spl12_57 ),
inference(avatar_split_clause,[],[f1231,f1063,f1248,f1245]) ).
fof(f1251,plain,
( n1 = sK11(n0,filling,n3)
| less(sK11(n0,filling,n3),n1)
| ~ spl12_84 ),
inference(resolution,[],[f1249,f278]) ).
fof(f1255,definition,
( spl12_85
<=> less(sK11(n0,filling,n3),n1) ),
introduced(definition,[new_symbols(definition,[spl12_85])],[avatar_definition]) ).
fof(f1256,plain,
( less(sK11(n0,filling,n3),n1)
| ~ spl12_85 ),
inference(avatar_component_clause,[],[f1255]) ).
fof(f1258,definition,
( spl12_86
<=> n1 = sK11(n0,filling,n3) ),
introduced(definition,[new_symbols(definition,[spl12_86])],[avatar_definition]) ).
fof(f1259,plain,
( n1 = sK11(n0,filling,n3)
| ~ spl12_86 ),
inference(avatar_component_clause,[],[f1258]) ).
fof(f1260,plain,
( spl12_85
| spl12_86
| ~ spl12_84 ),
inference(avatar_split_clause,[],[f1251,f1248,f1258,f1255]) ).
fof(f1262,plain,
( n0 = sK11(n0,filling,n3)
| ~ spl12_85 ),
inference(resolution,[],[f1256,f319]) ).
fof(f1268,plain,
( less(n0,n0)
| ~ stoppedIn(n0,filling,n3)
| ~ spl12_85 ),
inference(superposition,[],[f236,f1262]) ).
fof(f1269,plain,
( ~ stoppedIn(n0,filling,n3)
| ~ spl12_85 ),
inference(forward_subsumption_resolution,[],[f1268,f240]) ).
fof(f1271,plain,
( $false
| ~ spl12_57
| ~ spl12_85 ),
inference(forward_subsumption_resolution,[],[f1269,f1064]) ).
fof(f1272,plain,
( ~ spl12_57
| ~ spl12_85 ),
inference(avatar_contradiction_clause,[],[f1271]) ).
fof(f1410,plain,
( holdsAt(waterLevel(n3),sK11(n0,filling,n3))
| n0 = sK11(n0,filling,n3)
| ~ spl12_57 ),
inference(resolution,[],[f1236,f169]) ).
fof(f1428,plain,
( holdsAt(waterLevel(n3),n1)
| n0 = sK11(n0,filling,n3)
| ~ spl12_57
| ~ spl12_86 ),
inference(forward_demodulation,[],[f1410,f1259]) ).
fof(f1439,plain,
( n0 = n1
| holdsAt(waterLevel(n3),n1)
| ~ spl12_57
| ~ spl12_86 ),
inference(forward_demodulation,[],[f1428,f1259]) ).
fof(f1445,plain,
( spl12_20
| spl12_23
| ~ spl12_57
| ~ spl12_86 ),
inference(avatar_split_clause,[],[f1439,f1258,f1063,f569,f557]) ).
fof(f1502,plain,
( n3 = n2
| ~ spl12_40
| ~ spl12_54 ),
inference(resolution,[],[f751,f1166]) ).
fof(f1554,plain,
( less(sK11(n0,filling,n2),n1)
| n1 = sK11(n0,filling,n2)
| ~ spl12_55 ),
inference(resolution,[],[f1055,f280]) ).
fof(f1559,plain,
( happens(sK10(n0,filling,n2),sK11(n0,filling,n2))
| ~ spl12_55 ),
inference(resolution,[],[f1055,f237]) ).
fof(f1568,definition,
( spl12_103
<=> n1 = sK11(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl12_103])],[avatar_definition]) ).
fof(f1569,plain,
( n1 = sK11(n0,filling,n2)
| ~ spl12_103 ),
inference(avatar_component_clause,[],[f1568]) ).
fof(f1571,definition,
( spl12_104
<=> less(sK11(n0,filling,n2),n1) ),
introduced(definition,[new_symbols(definition,[spl12_104])],[avatar_definition]) ).
fof(f1572,plain,
( less(sK11(n0,filling,n2),n1)
| ~ spl12_104 ),
inference(avatar_component_clause,[],[f1571]) ).
fof(f1573,plain,
( spl12_103
| spl12_104
| ~ spl12_55 ),
inference(avatar_split_clause,[],[f1554,f1054,f1571,f1568]) ).
fof(f1581,plain,
( holdsAt(waterLevel(n3),sK11(n0,filling,n2))
| n0 = sK11(n0,filling,n2)
| ~ spl12_55 ),
inference(resolution,[],[f1559,f169]) ).
fof(f1597,plain,
( holdsAt(waterLevel(n3),n1)
| n0 = sK11(n0,filling,n2)
| ~ spl12_55
| ~ spl12_103 ),
inference(forward_demodulation,[],[f1581,f1569]) ).
fof(f1606,plain,
( n0 = n1
| holdsAt(waterLevel(n3),n1)
| ~ spl12_55
| ~ spl12_103 ),
inference(forward_demodulation,[],[f1597,f1569]) ).
fof(f1612,plain,
( spl12_20
| spl12_23
| ~ spl12_55
| ~ spl12_103 ),
inference(avatar_split_clause,[],[f1606,f1568,f1054,f569,f557]) ).
fof(f1629,plain,
( holdsAt(waterLevel(n3),n2)
| n0 = n2
| ~ spl12_49 ),
inference(resolution,[],[f863,f169]) ).
fof(f1647,plain,
( spl12_6
| spl12_40
| ~ spl12_49 ),
inference(avatar_split_clause,[],[f1629,f862,f750,f388]) ).
fof(f1694,plain,
( n0 = sK11(n0,filling,n2)
| ~ spl12_104 ),
inference(resolution,[],[f1572,f319]) ).
fof(f1700,plain,
( less(n0,n0)
| ~ stoppedIn(n0,filling,n2)
| ~ spl12_104 ),
inference(superposition,[],[f236,f1694]) ).
fof(f1701,plain,
( ~ stoppedIn(n0,filling,n2)
| ~ spl12_104 ),
inference(forward_subsumption_resolution,[],[f1700,f240]) ).
fof(f1704,plain,
( $false
| ~ spl12_55
| ~ spl12_104 ),
inference(forward_subsumption_resolution,[],[f1701,f1055]) ).
fof(f1705,plain,
( ~ spl12_55
| ~ spl12_104 ),
inference(avatar_contradiction_clause,[],[f1704]) ).
fof(f1731,plain,
( n1 = n3
| ~ spl12_20
| ~ spl12_58 ),
inference(resolution,[],[f558,f1078]) ).
fof(f1746,plain,
( less(n2,n1)
| ~ spl12_20
| ~ spl12_58 ),
inference(superposition,[],[f265,f1731]) ).
fof(f1780,plain,
( $false
| ~ spl12_20
| ~ spl12_58 ),
inference(forward_subsumption_resolution,[],[f1746,f341]) ).
fof(f1781,plain,
( ~ spl12_20
| ~ spl12_58 ),
inference(avatar_contradiction_clause,[],[f1780]) ).
fof(f1795,plain,
( n0 = sK11(n0,filling,n1)
| ~ spl12_59 ),
inference(resolution,[],[f1073,f321]) ).
fof(f1810,plain,
( less(n0,n0)
| ~ stoppedIn(n0,filling,n1)
| ~ spl12_59 ),
inference(superposition,[],[f236,f1795]) ).
fof(f1811,plain,
( ~ stoppedIn(n0,filling,n1)
| ~ spl12_59 ),
inference(forward_subsumption_resolution,[],[f1810,f240]) ).
fof(f1813,plain,
( $false
| ~ spl12_59 ),
inference(forward_subsumption_resolution,[],[f1811,f1073]) ).
fof(f1814,plain,
~ spl12_59,
inference(avatar_contradiction_clause,[],[f1813]) ).
fof(f1856,plain,
( less(n3,n3)
| ~ spl12_40
| ~ spl12_54 ),
inference(superposition,[],[f265,f1502]) ).
fof(f1877,plain,
( $false
| ~ spl12_40
| ~ spl12_54 ),
inference(forward_subsumption_resolution,[],[f1856,f240]) ).
fof(f1878,plain,
( ~ spl12_40
| ~ spl12_54 ),
inference(avatar_contradiction_clause,[],[f1877]) ).
fof(f1946,plain,
( happens(sK10(n0,filling,n3),sK11(n0,filling,n3))
| ~ spl12_57 ),
inference(resolution,[],[f1064,f237]) ).
fof(f1947,plain,
( happens(sK10(n0,filling,n3),n2)
| ~ spl12_57
| ~ spl12_83 ),
inference(forward_demodulation,[],[f1946,f1246]) ).
fof(f1949,plain,
( happens(overflow,n2)
| ~ spl12_57
| ~ spl12_81
| ~ spl12_83 ),
inference(forward_demodulation,[],[f1947,f1239]) ).
fof(f1953,plain,
( happens(tapOff,n2)
| ~ spl12_57
| ~ spl12_82
| ~ spl12_83 ),
inference(forward_demodulation,[],[f1947,f1242]) ).
fof(f2074,plain,
holdsAt(filling,plus(n0,n1)),
inference(resolution,[],[f1033,f242]) ).
fof(f2075,plain,
holdsAt(filling,plus(n1,n0)),
inference(forward_demodulation,[],[f2074,f134]) ).
fof(f2076,plain,
holdsAt(filling,n1),
inference(forward_demodulation,[],[f2075,f262]) ).
fof(f2077,plain,
spl12_21,
inference(avatar_split_clause,[],[f2076,f561]) ).
fof(f2201,plain,
( overflow = tapOff
| n0 = n2
| ~ spl12_57
| ~ spl12_82
| ~ spl12_83 ),
inference(resolution,[],[f1953,f167]) ).
fof(f2219,plain,
( n0 = n2
| ~ spl12_57
| ~ spl12_82
| ~ spl12_83 ),
inference(forward_subsumption_resolution,[],[f2201,f223]) ).
fof(f2225,plain,
( spl12_6
| ~ spl12_57
| ~ spl12_82
| ~ spl12_83 ),
inference(avatar_split_clause,[],[f2219,f1245,f1241,f1063,f388]) ).
fof(f2246,plain,
( holdsAt(waterLevel(n3),n2)
| tapOn = overflow
| ~ spl12_57
| ~ spl12_81
| ~ spl12_83 ),
inference(resolution,[],[f1949,f172]) ).
fof(f2253,plain,
( holdsAt(waterLevel(n3),n2)
| ~ spl12_57
| ~ spl12_81
| ~ spl12_83 ),
inference(forward_subsumption_resolution,[],[f2246,f222]) ).
fof(f2259,plain,
( spl12_40
| ~ spl12_57
| ~ spl12_81
| ~ spl12_83 ),
inference(avatar_split_clause,[],[f2253,f1245,f1238,f1063,f750]) ).
fof(f2519,plain,
~ releasedAt(filling,plus(n0,n1)),
inference(resolution,[],[f1031,f242]) ).
fof(f2520,plain,
~ releasedAt(filling,plus(n1,n0)),
inference(forward_demodulation,[],[f2519,f134]) ).
fof(f2521,plain,
~ releasedAt(filling,n1),
inference(forward_demodulation,[],[f2520,f262]) ).
fof(f2522,plain,
( $false
| ~ spl12_36 ),
inference(forward_subsumption_resolution,[],[f2521,f726]) ).
fof(f2523,plain,
~ spl12_36,
inference(avatar_contradiction_clause,[],[f2522]) ).
cnf(s4,plain,
( spl12_5
| spl12_6 ),
inference(sat_conversion,[],[f390]) ).
cnf(s32,plain,
( ~ spl12_21
| ~ spl12_23 ),
inference(sat_conversion,[],[f663]) ).
cnf(s33,plain,
( ~ spl12_21
| spl12_28
| spl12_29
| spl12_30 ),
inference(sat_conversion,[],[f686]) ).
cnf(s37,plain,
( spl12_20
| spl12_23
| ~ spl12_28 ),
inference(sat_conversion,[],[f716]) ).
cnf(s39,plain,
( ~ spl12_30
| spl12_35
| spl12_36 ),
inference(sat_conversion,[],[f727]) ).
cnf(s50,plain,
~ spl12_6,
inference(sat_conversion,[],[f793]) ).
cnf(s54,plain,
( spl12_20
| spl12_23
| ~ spl12_35 ),
inference(sat_conversion,[],[f827]) ).
cnf(s56,plain,
( spl12_30
| ~ spl12_38
| spl12_46 ),
inference(sat_conversion,[],[f832]) ).
cnf(s59,plain,
( spl12_6
| spl12_40
| ~ spl12_46 ),
inference(sat_conversion,[],[f858]) ).
cnf(s61,plain,
( ~ spl12_29
| spl12_38
| spl12_49
| spl12_50 ),
inference(sat_conversion,[],[f867]) ).
cnf(s65,plain,
( ~ spl12_53
| spl12_54
| spl12_55 ),
inference(sat_conversion,[],[f1056]) ).
cnf(s66,plain,
( ~ spl12_5
| spl12_56
| spl12_57 ),
inference(sat_conversion,[],[f1065]) ).
cnf(s67,plain,
( spl12_58
| spl12_59 ),
inference(sat_conversion,[],[f1074]) ).
cnf(s72,plain,
( ~ spl12_50
| ~ spl12_56 ),
inference(sat_conversion,[],[f1133]) ).
cnf(s75,plain,
spl12_53,
inference(sat_conversion,[],[f1156]) ).
cnf(s83,plain,
( ~ spl12_57
| spl12_81
| spl12_82 ),
inference(sat_conversion,[],[f1243]) ).
cnf(s84,plain,
( ~ spl12_57
| spl12_83
| spl12_84 ),
inference(sat_conversion,[],[f1250]) ).
cnf(s85,plain,
( ~ spl12_84
| spl12_85
| spl12_86 ),
inference(sat_conversion,[],[f1260]) ).
cnf(s86,plain,
( ~ spl12_57
| ~ spl12_85 ),
inference(sat_conversion,[],[f1272]) ).
cnf(s97,plain,
( spl12_20
| spl12_23
| ~ spl12_57
| ~ spl12_86 ),
inference(sat_conversion,[],[f1445]) ).
cnf(s110,plain,
( ~ spl12_55
| spl12_103
| spl12_104 ),
inference(sat_conversion,[],[f1573]) ).
cnf(s112,plain,
( spl12_20
| spl12_23
| ~ spl12_55
| ~ spl12_103 ),
inference(sat_conversion,[],[f1612]) ).
cnf(s116,plain,
( spl12_6
| spl12_40
| ~ spl12_49 ),
inference(sat_conversion,[],[f1647]) ).
cnf(s120,plain,
( ~ spl12_55
| ~ spl12_104 ),
inference(sat_conversion,[],[f1705]) ).
cnf(s129,plain,
( ~ spl12_20
| ~ spl12_58 ),
inference(sat_conversion,[],[f1781]) ).
cnf(s132,plain,
~ spl12_59,
inference(sat_conversion,[],[f1814]) ).
cnf(s142,plain,
( ~ spl12_40
| ~ spl12_54 ),
inference(sat_conversion,[],[f1878]) ).
cnf(s158,plain,
spl12_21,
inference(sat_conversion,[],[f2077]) ).
cnf(s182,plain,
( spl12_6
| ~ spl12_57
| ~ spl12_82
| ~ spl12_83 ),
inference(sat_conversion,[],[f2225]) ).
cnf(s185,plain,
( spl12_40
| ~ spl12_57
| ~ spl12_81
| ~ spl12_83 ),
inference(sat_conversion,[],[f2259]) ).
cnf(s220,plain,
~ spl12_36,
inference(sat_conversion,[],[f2523]) ).
cnf(s223,plain,
spl12_58,
inference(rat,[],[s67,s132]) ).
cnf(s224,plain,
~ spl12_20,
inference(rat,[],[s129,s223]) ).
cnf(s225,plain,
( spl12_54
| spl12_55 ),
inference(rat,[],[s65,s75]) ).
cnf(s226,plain,
( spl12_23
| ~ spl12_35 ),
inference(rat,[],[s54,s224]) ).
cnf(s231,plain,
( ~ spl12_30
| spl12_35 ),
inference(rat,[],[s39,s220]) ).
cnf(s232,plain,
( spl12_23
| ~ spl12_28 ),
inference(rat,[],[s37,s224]) ).
cnf(s234,plain,
( spl12_28
| spl12_29
| spl12_30 ),
inference(rat,[],[s33,s158]) ).
cnf(s235,plain,
~ spl12_23,
inference(rat,[],[s32,s158]) ).
cnf(s239,plain,
~ spl12_35,
inference(rat,[],[s226,s235]) ).
cnf(s240,plain,
~ spl12_28,
inference(rat,[],[s232,s235]) ).
cnf(s241,plain,
~ spl12_30,
inference(rat,[],[s231,s239]) ).
cnf(s242,plain,
spl12_29,
inference(rat,[],[s234,s241,s240]) ).
cnf(s246,plain,
spl12_5,
inference(rat,[],[s4,s50]) ).
cnf(s247,plain,
( ~ spl12_83
| ~ spl12_57
| spl12_40 ),
inference(rat,[],[s83,s182,s185,s50]) ).
cnf(s248,plain,
( spl12_40
| spl12_38 ),
inference(rat,[],[s247,s84,s85,s97,s86,s66,s72,s61,s116,s224,s235,s246,s242,s50]) ).
cnf(s249,plain,
( ~ spl12_55
| spl12_104 ),
inference(rat,[],[s112,s110,s235,s224]) ).
cnf(s250,plain,
~ spl12_55,
inference(rat,[],[s249,s120]) ).
cnf(s251,plain,
spl12_54,
inference(rat,[],[s225,s250]) ).
cnf(s253,plain,
~ spl12_40,
inference(rat,[],[s142,s251]) ).
cnf(s259,plain,
~ spl12_46,
inference(rat,[],[s59,s50,s253]) ).
cnf(s260,plain,
spl12_38,
inference(rat,[],[s248,s253]) ).
cnf(s261,plain,
$false,
inference(rat,[],[s56,s241,s259,s260]) ).
fof(f2524,plain,
$false,
inference(avatar_sat_refutation,[],[s261]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR004+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.19 % Computer : n018.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Mon Sep 28 22:07:25 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.22 Running first-order theorem proving
% 0.10/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.20/2.15 % (3844918)Detected formulas, will run a generic FOF schedule.
% 9.20/2.15 % (3844990)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=139989110:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.20/2.15 % (3844990)Refutation not found, incomplete strategy
% 9.20/2.15 % (3844990)------------------------------
% 9.20/2.15 % (3844990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.15 % (3844990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.15 % (3844990)CaDiCaL version: 2.1.3
% 9.20/2.15 % (3844990)Termination reason: Refutation not found, incomplete strategy
% 9.20/2.15 % (3844990)Time elapsed: 0.001 s
% 9.20/2.15 % (3844990)Peak memory usage: 88 MB
% 9.20/2.15 % (3844992)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3480223294:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.20/2.15 % (3844987)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3217397518:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.20/2.15 % (3844993)dis-21_1_sil=8000:lcm=predicate:random_seed=1456279672:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 9.20/2.15 % (3844991)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2756295432:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.20/2.15 % (3844989)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=4209140043:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.20/2.15 % (3844988)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3250077969:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.20/2.15 % (3844991)Refutation not found, incomplete strategy
% 9.20/2.15 % (3844991)------------------------------
% 9.20/2.15 % (3844991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.15 % (3844991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.15 % (3844991)CaDiCaL version: 2.1.3
% 9.20/2.15 % (3844991)Termination reason: Refutation not found, incomplete strategy
% 9.20/2.15 % (3844991)Time elapsed: 0.002 s
% 9.20/2.15 % (3844991)Peak memory usage: 88 MB
% 9.20/2.15 % (3844991)Instructions burned: 1 (million)
% 9.20/2.15 % (3844993)Instruction limit reached!
% 9.20/2.15 % (3844993)------------------------------
% 9.20/2.15 % (3844993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.15 % (3844993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.15 % (3844993)CaDiCaL version: 2.1.3
% 9.20/2.15 % (3844993)Termination reason: Instruction limit
% 9.20/2.15 % (3844993)Termination phase: Saturation
% 9.20/2.15 % (3844993)Time elapsed: 0.085 s
% 9.20/2.15 % (3844993)Peak memory usage: 89 MB
% 9.20/2.15 % (3844993)Instructions burned: 130 (million)
% 9.20/2.15 % (3844992)Instruction limit reached!
% 9.20/2.15 % (3844992)------------------------------
% 9.20/2.15 % (3844992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.15 % (3844992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.15 % (3844992)CaDiCaL version: 2.1.3
% 9.20/2.15 % (3844992)Termination reason: Instruction limit
% 9.20/2.15 % (3844992)Termination phase: Saturation
% 9.20/2.15 % (3844992)Time elapsed: 0.099 s
% 9.20/2.15 % (3844992)Peak memory usage: 90 MB
% 9.20/2.15 % (3844992)Instructions burned: 140 (million)
% 9.20/2.15 % (3844990)------------------------------
% 9.20/2.15 % (3844990)------------------------------
% 9.20/2.15 % (3845010)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3979031788:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 9.20/2.15 % (3845009)lrs+10_1_sil=8000:sp=occurrence:random_seed=1942827055:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 9.20/2.15 % (3845010)Refutation not found, incomplete strategy
% 9.20/2.15 % (3845010)------------------------------
% 9.20/2.15 % (3845010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.15 % (3845010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.15 % (3845010)CaDiCaL version: 2.1.3
% 9.20/2.15 % (3845010)Termination reason: Refutation not found, incomplete strategy
% 9.20/2.15 % (3845010)Time elapsed: 0.002 s
% 9.20/2.15 % (3845010)Peak memory usage: 88 MB
% 9.20/2.15 % (3845010)Instructions burned: 1 (million)
% 9.20/2.15 % (3844991)------------------------------
% 9.20/2.15 % (3844991)------------------------------
% 9.20/2.15 % (3845011)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2913915078:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 9.20/2.15 % (3845011)Instruction limit reached!
% 9.20/2.15 % (3845011)------------------------------
% 9.20/2.15 % (3845011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.15 % (3845011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.15 % (3845011)CaDiCaL version: 2.1.3
% 9.20/2.15 % (3845011)Termination reason: Instruction limit
% 9.20/2.15 % (3845011)Termination phase: Saturation
% 9.20/2.15 % (3845011)Time elapsed: 0.163 s
% 9.20/2.15 % (3845011)Peak memory usage: 90 MB
% 9.20/2.15 % (3845011)Instructions burned: 327 (million)
% 9.20/2.15 % (3845009)Instruction limit reached!
% 9.20/2.15 % (3845009)------------------------------
% 9.20/2.15 % (3845009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.15 % (3845009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.15 % (3845009)CaDiCaL version: 2.1.3
% 9.20/2.15 % (3845009)Termination reason: Instruction limit
% 9.20/2.15 % (3845009)Termination phase: Saturation
% 9.20/2.15 % (3845009)Time elapsed: 0.262 s
% 9.20/2.15 % (3845009)Peak memory usage: 90 MB
% 9.20/2.15 % (3845009)Instructions burned: 285 (million)
% 9.20/2.15 % (3845022)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3011607020:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 9.20/2.15 % (3845023)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3829727283:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 9.20/2.15 % (3845010)------------------------------
% 9.20/2.15 % (3845010)------------------------------
% 9.20/2.15 % (3845023)Instruction limit reached!
% 9.20/2.15 % (3845023)------------------------------
% 9.20/2.15 % (3845023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.15 % (3845023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.15 % (3845023)CaDiCaL version: 2.1.3
% 9.20/2.15 % (3845023)Termination reason: Instruction limit
% 9.20/2.15 % (3845023)Termination phase: Saturation
% 9.20/2.15 % (3845023)Time elapsed: 0.089 s
% 9.20/2.15 % (3845023)Peak memory usage: 89 MB
% 9.20/2.15 % (3845023)Instructions burned: 296 (million)
% 9.20/2.15 % (3845024)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3198454040:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 9.20/2.15 % (3845022)Instruction limit reached!
% 9.20/2.15 % (3845022)------------------------------
% 9.20/2.15 % (3845022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.15 % (3845022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.15 % (3845022)CaDiCaL version: 2.1.3
% 9.20/2.15 % (3845022)Termination reason: Instruction limit
% 9.20/2.15 % (3845022)Termination phase: Saturation
% 9.20/2.15 % (3845022)Time elapsed: 0.144 s
% 9.20/2.15 % (3845022)Peak memory usage: 91 MB
% 9.20/2.15 % (3845022)Instructions burned: 249 (million)
% 9.20/2.15 % (3844989)Refutation not found, incomplete strategy
% 9.20/2.15 % (3844989)------------------------------
% 9.20/2.15 % (3844989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.15 % (3844989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.15 % (3844989)CaDiCaL version: 2.1.3
% 9.20/2.15 % (3844989)Termination reason: Refutation not found, incomplete strategy
% 9.20/2.15 % (3844989)Time elapsed: 0.821 s
% 9.20/2.15 % (3844989)Peak memory usage: 127 MB
% 9.20/2.15 % (3844989)Instructions burned: 899 (million)
% 9.20/2.15 % (3845027)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1201298231:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 9.20/2.15 % (3845027)Refutation not found, incomplete strategy
% 9.20/2.15 % (3845027)------------------------------
% 9.20/2.15 % (3845027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.15 % (3845027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.15 % (3845027)CaDiCaL version: 2.1.3
% 9.20/2.15 % (3845027)Termination reason: Refutation not found, incomplete strategy
% 9.20/2.15 % (3845027)Time elapsed: 0.003 s
% 9.20/2.15 % (3845027)Peak memory usage: 89 MB
% 9.20/2.15 % (3845027)Instructions burned: 2 (million)
% 9.20/2.15 % (3845028)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=603781643:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 9.20/2.15 % (3845028)Instruction limit reached!
% 9.20/2.15 % (3845028)------------------------------
% 9.20/2.15 % (3845028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.15 % (3845028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.15 % (3845028)CaDiCaL version: 2.1.3
% 9.20/2.15 % (3845028)Termination reason: Instruction limit
% 9.20/2.15 % (3845028)Termination phase: Saturation
% 9.20/2.15 % (3845028)Time elapsed: 0.035 s
% 9.20/2.15 % (3845028)Peak memory usage: 89 MB
% 9.20/2.15 % (3845028)Instructions burned: 131 (million)
% 9.20/2.15 % (3845030)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1600116671:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 9.20/2.15 % (3845030)Refutation not found, incomplete strategy
% 9.20/2.15 % (3845030)------------------------------
% 9.20/2.15 % (3845030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.15 % (3845030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.15 % (3845030)CaDiCaL version: 2.1.3
% 9.20/2.15 % (3845030)Termination reason: Refutation not found, incomplete strategy
% 9.20/2.15 % (3845030)Time elapsed: 0.008 s
% 9.20/2.15 % (3845030)Peak memory usage: 88 MB
% 9.20/2.15 % (3845030)Instructions burned: 10 (million)
% 9.20/2.15 % (3844988)First to succeed.
% 9.20/2.15 % (3844988)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3844918"
% 9.20/2.15 % (3844989)------------------------------
% 9.20/2.15 % (3844989)------------------------------
% 9.20/2.15 % (3845034)lrs+10_1_sil=8000:sp=occurrence:random_seed=109370896:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 9.20/2.15 % (3844987)Also succeeded, but the first one will report.
% 9.20/2.15 % (3845027)------------------------------
% 9.20/2.15 % (3845027)------------------------------
% 9.20/2.15 % (3845030)------------------------------
% 9.20/2.15 % (3845030)------------------------------
% 9.20/2.15 % (3845039)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=89883016:i=437:sd=1:aac=none:ss=included_2987 on theBenchmark for (2987ds/437Mi)
% 9.20/2.15 % (3845039)Refutation not found, incomplete strategy
% 9.20/2.15 % (3845039)------------------------------
% 9.20/2.15 % (3845039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.20/2.15 % (3845039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.20/2.15 % (3845039)CaDiCaL version: 2.1.3
% 9.20/2.15 % (3845039)Termination reason: Refutation not found, incomplete strategy
% 9.20/2.15 % (3845039)Time elapsed: 0.002 s
% 9.20/2.15 % (3845039)Peak memory usage: 88 MB
% 9.20/2.15 % (3845039)Instructions burned: 1 (million)
% 9.20/2.15 % (3845061)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1934411733:i=5202:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/5202Mi)
% 9.20/2.15 % (3844988)Refutation found. Thanks to Tanya!
% 9.20/2.15 % SZS status Theorem for theBenchmark
% 9.20/2.15 % SZS output start Proof for theBenchmark
% See solution above
% 10.98/2.35 % (3844988)------------------------------
% 10.98/2.35 % (3844988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.98/2.35 % (3844988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.98/2.35 % (3844988)CaDiCaL version: 2.1.3
% 10.98/2.35 % (3844988)Termination reason: Refutation
% 10.98/2.35 % (3844988)Time elapsed: 1.031 s
% 10.98/2.35 % (3844988)Peak memory usage: 131 MB
% 10.98/2.35 % (3844988)Instructions burned: 1175 (million)
% 10.98/2.35 % (3844988)------------------------------
% 10.98/2.35 % (3844988)------------------------------
% 10.98/2.35 % (3844918)Success in time 1.469 s
% 10.98/2.35 % Vampire exiting
%------------------------------------------------------------------------------