%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR009+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:57 AM UTC 2026
% Result : Theorem 7.29s 1.93s
% Output : Refutation 8.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 38
% Syntax : Number of formulae : 228 ( 45 unt; 14 def)
% Number of atoms : 694 ( 148 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 763 ( 297 ~; 333 |; 99 &)
% ( 25 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 13 prp; 0-4 aty)
% Number of functors : 15 ( 15 usr; 9 con; 0-3 aty)
% Number of variables : 275 ( 0 sgn 256 !; 19 ?)
% 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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',happens_holds) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& terminates(X0,X2,X1) )
=> ~ holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',happens_terminates_not_holds) ).
fof(f12,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& ( initiates(X0,X2,X1)
| terminates(X0,X2,X1) ) )
=> ~ releasedAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',same_waterLevel) ).
fof(f19,axiom,
tapOff != tapOn,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tapOff_not_tapOn) ).
fof(f21,axiom,
overflow != tapOn,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',overflow_not_tapOn) ).
fof(f27,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',plus0_1) ).
fof(f30,axiom,
plus(n1,n1) = n2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',plus1_1) ).
fof(f37,axiom,
! [X0,X1] :
( less_or_equal(X0,X1)
<=> ( less(X0,X1)
| X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_or_equal) ).
fof(f38,axiom,
~ ? [X0] : less(X0,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less0) ).
fof(f39,axiom,
! [X0] :
( less(X0,n1)
<=> less_or_equal(X0,n0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less1) ).
fof(f40,axiom,
! [X0] :
( less(X0,n2)
<=> less_or_equal(X0,n1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less2) ).
fof(f41,axiom,
! [X0] :
( less(X0,n3)
<=> less_or_equal(X0,n2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less3) ).
fof(f48,axiom,
! [X0,X1] :
( less(X0,X1)
<=> ( ~ less(X1,X0)
& X1 != X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_property) ).
fof(f49,axiom,
holdsAt(waterLevel(n0),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',waterLevel_0) ).
fof(f55,conjecture,
holdsAt(filling,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',filling_2) ).
fof(f56,negated_conjecture,
~ holdsAt(filling,n2),
inference(negated_conjecture,[status(cth)],[f55]) ).
fof(f57,plain,
~ holdsAt(filling,n2),
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(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] : ~ less(X0,n0),
inference(ennf_transformation,[],[f38]) ).
fof(f64,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f65,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(flattening,[],[f64]) ).
fof(f66,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(f67,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(flattening,[],[f66]) ).
fof(f68,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f69,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(flattening,[],[f68]) ).
fof(f74,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(f75,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,[],[f74]) ).
fof(f78,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f79,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(flattening,[],[f78]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(flattening,[],[f80]) ).
fof(f82,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(f83,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,[],[f82]) ).
fof(f84,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(f85,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(ennf_transformation,[],[f17]) ).
fof(f86,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(flattening,[],[f85]) ).
fof(f87,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(f88,definition,
! [X2,X0,X1] :
( sP1(X2,X0,X1)
<=> ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f89,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| sP1(X2,X0,X1)
| sP0(X2,X0,X1) ) ),
inference(definition_folding,[],[f58,f88,f87]) ).
fof(f97,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ( ( tapOn != X0
| filling != X1 )
& ( overflow != X0
| spilling != X1 )
& ~ sP1(X2,X0,X1)
& ~ sP0(X2,X0,X1) ) )
& ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| sP1(X2,X0,X1)
| sP0(X2,X0,X1)
| ~ initiates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f89]) ).
fof(f98,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ( ( tapOn != X0
| filling != X1 )
& ( overflow != X0
| spilling != X1 )
& ~ sP1(X2,X0,X1)
& ~ sP0(X2,X0,X1) ) )
& ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| sP1(X2,X0,X1)
| sP0(X2,X0,X1)
| ~ initiates(X0,X1,X2) ) ),
inference(flattening,[],[f97]) ).
fof(f99,plain,
! [X0] :
( ( less(X0,n3)
| ~ less_or_equal(X0,n2) )
& ( less_or_equal(X0,n2)
| ~ less(X0,n3) ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f100,plain,
! [X0] :
( ( less(X0,n2)
| ~ less_or_equal(X0,n1) )
& ( less_or_equal(X0,n1)
| ~ less(X0,n2) ) ),
inference(nnf_transformation,[],[f40]) ).
fof(f101,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(nnf_transformation,[],[f48]) ).
fof(f102,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(flattening,[],[f101]) ).
fof(f103,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(f104,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,[],[f103]) ).
fof(f108,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(f109,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,[],[f108]) ).
fof(f113,plain,
! [X0] :
( ( less(X0,n1)
| ~ less_or_equal(X0,n0) )
& ( less_or_equal(X0,n0)
| ~ less(X0,n1) ) ),
inference(nnf_transformation,[],[f39]) ).
fof(f114,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(f115,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,[],[f114]) ).
fof(f118,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ( happens(sK7(X0,X1),X1)
& releases(sK7(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f79]) ).
fof(f119,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ( happens(sK8(X0,X1),X1)
& terminates(sK8(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X2,sK8(X0,X1))],[f83]) ).
fof(f120,plain,
! [X0,X1,X2] :
( ( happens(sK9(X0,X1,X2),sK10(X0,X1,X2))
& less(X0,sK10(X0,X1,X2))
& less(sK10(X0,X1,X2),X2)
& terminates(sK9(X0,X1,X2),X1,sK10(X0,X1,X2)) )
| ~ stoppedIn(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10]),skolemize(X3,sK9(X0,X1,X2)),skolemize(X4,sK10(X0,X1,X2))],[f84]) ).
fof(f122,plain,
holdsAt(waterLevel(n0),n0),
inference(cnf_transformation,[],[f49]) ).
fof(f128,plain,
~ holdsAt(filling,n2),
inference(cnf_transformation,[],[f57]) ).
fof(f129,plain,
! [X0] : ~ less(X0,n0),
inference(cnf_transformation,[],[f63]) ).
fof(f133,plain,
! [X2,X0,X1] :
( ~ holdsAt(waterLevel(X2),X0)
| ~ holdsAt(waterLevel(X1),X0)
| X1 = X2 ),
inference(cnf_transformation,[],[f65]) ).
fof(f152,plain,
! [X2,X0,X1] :
( initiates(X0,X1,X2)
| tapOn != X0
| filling != X1 ),
inference(cnf_transformation,[],[f98]) ).
fof(f154,plain,
! [X0] :
( ~ less_or_equal(X0,n2)
| less(X0,n3) ),
inference(cnf_transformation,[],[f99]) ).
fof(f156,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| less(X0,n2) ),
inference(cnf_transformation,[],[f100]) ).
fof(f160,plain,
n2 = plus(n1,n1),
inference(cnf_transformation,[],[f30]) ).
fof(f162,plain,
! [X0,X1] :
( X0 != X1
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f102]) ).
fof(f163,plain,
! [X0,X1] :
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f102]) ).
fof(f166,plain,
tapOn != overflow,
inference(cnf_transformation,[],[f21]) ).
fof(f167,plain,
tapOn != tapOff,
inference(cnf_transformation,[],[f19]) ).
fof(f170,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| holdsAt(waterLevel(n3),X1)
| n0 = X1 ),
inference(cnf_transformation,[],[f104]) ).
fof(f171,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| overflow = X0
| tapOn = X0 ),
inference(cnf_transformation,[],[f104]) ).
fof(f175,plain,
! [X0,X1] :
( happens(X0,X1)
| tapOn != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f104]) ).
fof(f183,plain,
! [X2,X0,X1] :
( ~ terminates(X0,X1,X2)
| overflow = X0
| tapOff = X0 ),
inference(cnf_transformation,[],[f109]) ).
fof(f184,plain,
! [X2,X0,X1] :
( terminates(X0,X1,X2)
| overflow != X0
| filling != X1 ),
inference(cnf_transformation,[],[f109]) ).
fof(f187,plain,
! [X2,X0,X1] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(cnf_transformation,[],[f67]) ).
fof(f188,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f69]) ).
fof(f193,plain,
! [X2,X3,X0,X1,X4] :
( ~ trajectory(X2,X1,X3,X4)
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1)
| ~ less(n0,X4)
| holdsAt(X3,plus(X1,X4))
| stoppedIn(X1,X2,plus(X1,X4)) ),
inference(cnf_transformation,[],[f75]) ).
fof(f199,plain,
! [X0] :
( ~ less(X0,n1)
| less_or_equal(X0,n0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f200,plain,
! [X0] :
( ~ less_or_equal(X0,n0)
| less(X0,n1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f201,plain,
! [X0,X1] :
( ~ less_or_equal(X0,X1)
| X0 = X1
| less(X0,X1) ),
inference(cnf_transformation,[],[f115]) ).
fof(f202,plain,
! [X0,X1] :
( less_or_equal(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f115]) ).
fof(f204,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f27]) ).
fof(f211,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| happens(sK7(X0,X1),X1) ),
inference(cnf_transformation,[],[f118]) ).
fof(f212,plain,
! [X2,X0,X1] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(cnf_transformation,[],[f81]) ).
fof(f214,plain,
! [X0,X1] :
( releasedAt(X0,plus(X1,n1))
| happens(sK8(X0,X1),X1)
| ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f119]) ).
fof(f215,plain,
! [X2,X0,X1] :
( terminates(sK9(X0,X1,X2),X1,sK10(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f120]) ).
fof(f216,plain,
! [X2,X0,X1] :
( less(sK10(X0,X1,X2),X2)
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f120]) ).
fof(f218,plain,
! [X2,X0,X1] :
( happens(sK9(X0,X1,X2),sK10(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f120]) ).
fof(f219,plain,
! [X2,X3,X0,X1] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(cnf_transformation,[],[f86]) ).
fof(f227,plain,
! [X2,X1] :
( initiates(tapOn,X1,X2)
| filling != X1 ),
inference(equality_resolution,[],[f152]) ).
fof(f228,plain,
! [X2] : initiates(tapOn,filling,X2),
inference(equality_resolution,[],[f227]) ).
fof(f231,plain,
! [X1] : ~ less(X1,X1),
inference(equality_resolution,[],[f162]) ).
fof(f232,plain,
! [X1] :
( happens(tapOn,X1)
| n0 != X1 ),
inference(equality_resolution,[],[f175]) ).
fof(f233,plain,
happens(tapOn,n0),
inference(equality_resolution,[],[f232]) ).
fof(f239,plain,
! [X2,X1] :
( terminates(overflow,X1,X2)
| filling != X1 ),
inference(equality_resolution,[],[f184]) ).
fof(f240,plain,
! [X2] : terminates(overflow,filling,X2),
inference(equality_resolution,[],[f239]) ).
fof(f241,plain,
! [X1] : less_or_equal(X1,X1),
inference(equality_resolution,[],[f202]) ).
fof(f242,plain,
! [X3,X0,X1] :
( trajectory(filling,X1,waterLevel(plus(X0,X3)),X3)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(equality_resolution,[],[f219]) ).
fof(f245,plain,
less(n2,n3),
inference(resolution,[],[f154,f241]) ).
fof(f247,plain,
less(n1,n2),
inference(resolution,[],[f156,f241]) ).
fof(f250,plain,
~ less(n2,n1),
inference(resolution,[],[f247,f163]) ).
fof(f254,plain,
less(n0,n1),
inference(resolution,[],[f200,f241]) ).
fof(f370,plain,
! [X0,X1] :
( less_or_equal(sK10(X0,X1,n1),n0)
| ~ stoppedIn(X0,X1,n1) ),
inference(resolution,[],[f216,f199]) ).
fof(f412,plain,
! [X0,X1] :
( ~ initiates(X1,X0,n0)
| ~ happens(X1,n0)
| ~ releasedAt(X0,n1) ),
inference(superposition,[],[f187,f204]) ).
fof(f416,plain,
! [X0] :
( holdsAt(filling,plus(X0,n1))
| ~ happens(tapOn,X0) ),
inference(resolution,[],[f188,f228]) ).
fof(f427,plain,
! [X0,X1] :
( ~ terminates(X1,X0,n0)
| ~ happens(X1,n0)
| ~ holdsAt(X0,n1) ),
inference(superposition,[],[f212,f204]) ).
fof(f463,plain,
! [X0] :
( happens(sK7(X0,n1),n1)
| releasedAt(X0,n1)
| ~ releasedAt(X0,n2) ),
inference(superposition,[],[f211,f160]) ).
fof(f469,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| overflow = sK9(X0,X1,X2)
| tapOn = sK9(X0,X1,X2) ),
inference(resolution,[],[f218,f171]) ).
fof(f478,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| overflow = sK9(X0,X1,X2)
| tapOff = sK9(X0,X1,X2) ),
inference(resolution,[],[f215,f183]) ).
fof(f522,plain,
! [X0] :
( happens(sK8(X0,n1),n1)
| releasedAt(X0,n2)
| ~ holdsAt(X0,n1)
| holdsAt(X0,n2) ),
inference(superposition,[],[f214,f160]) ).
fof(f549,plain,
! [X2,X3,X0,X1] :
( ~ holdsAt(waterLevel(X3),X1)
| ~ initiates(X0,filling,X1)
| ~ less(n0,X2)
| holdsAt(waterLevel(plus(X3,X2)),plus(X1,X2))
| stoppedIn(X1,filling,plus(X1,X2))
| ~ happens(X0,X1) ),
inference(resolution,[],[f193,f242]) ).
fof(f625,plain,
( holdsAt(filling,n1)
| ~ happens(tapOn,n0) ),
inference(superposition,[],[f416,f204]) ).
fof(f628,plain,
holdsAt(filling,n1),
inference(forward_subsumption_resolution,[],[f625,f233]) ).
fof(f645,definition,
( spl11_5
<=> happens(overflow,n0) ),
introduced(definition,[new_symbols(definition,[spl11_5])],[avatar_definition]) ).
fof(f646,plain,
( happens(overflow,n0)
| ~ spl11_5 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f647,plain,
( ~ happens(overflow,n0)
| spl11_5 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f735,plain,
! [X0,X1] :
( ~ stoppedIn(X0,X1,n1)
| n0 = sK10(X0,X1,n1)
| less(sK10(X0,X1,n1),n0) ),
inference(resolution,[],[f370,f201]) ).
fof(f736,plain,
! [X0,X1] :
( ~ stoppedIn(X0,X1,n1)
| n0 = sK10(X0,X1,n1) ),
inference(forward_subsumption_resolution,[],[f735,f129]) ).
fof(f821,definition,
( spl11_15
<=> releasedAt(filling,n1) ),
introduced(definition,[new_symbols(definition,[spl11_15])],[avatar_definition]) ).
fof(f822,plain,
( releasedAt(filling,n1)
| ~ spl11_15 ),
inference(avatar_component_clause,[],[f821]) ).
fof(f823,plain,
( ~ releasedAt(filling,n1)
| spl11_15 ),
inference(avatar_component_clause,[],[f821]) ).
fof(f835,definition,
( spl11_17
<=> releasedAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl11_17])],[avatar_definition]) ).
fof(f836,plain,
( releasedAt(filling,n2)
| ~ spl11_17 ),
inference(avatar_component_clause,[],[f835]) ).
fof(f837,plain,
( ~ releasedAt(filling,n2)
| spl11_17 ),
inference(avatar_component_clause,[],[f835]) ).
fof(f844,plain,
( ~ happens(tapOn,n0)
| ~ releasedAt(filling,n1) ),
inference(resolution,[],[f412,f228]) ).
fof(f876,plain,
( ~ happens(overflow,n0)
| ~ holdsAt(filling,n1) ),
inference(resolution,[],[f427,f240]) ).
fof(f1087,definition,
( spl11_23
<=> n0 = n1 ),
introduced(definition,[new_symbols(definition,[spl11_23])],[avatar_definition]) ).
fof(f1088,plain,
( n0 != n1
| spl11_23 ),
inference(avatar_component_clause,[],[f1087]) ).
fof(f1089,plain,
( n0 = n1
| ~ spl11_23 ),
inference(avatar_component_clause,[],[f1087]) ).
fof(f1095,definition,
( spl11_25
<=> holdsAt(waterLevel(n3),n1) ),
introduced(definition,[new_symbols(definition,[spl11_25])],[avatar_definition]) ).
fof(f1096,plain,
( ~ holdsAt(waterLevel(n3),n1)
| spl11_25 ),
inference(avatar_component_clause,[],[f1095]) ).
fof(f1097,plain,
( holdsAt(waterLevel(n3),n1)
| ~ spl11_25 ),
inference(avatar_component_clause,[],[f1095]) ).
fof(f1123,plain,
( less(n0,n0)
| ~ spl11_23 ),
inference(superposition,[],[f254,f1089]) ).
fof(f1173,plain,
( $false
| ~ spl11_23 ),
inference(forward_subsumption_resolution,[],[f1123,f231]) ).
fof(f1174,plain,
~ spl11_23,
inference(avatar_contradiction_clause,[],[f1173]) ).
fof(f1185,plain,
! [X0] :
( releasedAt(X0,n1)
| ~ releasedAt(X0,n2)
| holdsAt(waterLevel(n3),n1)
| n0 = n1 ),
inference(resolution,[],[f463,f170]) ).
fof(f1287,plain,
( ! [X0] :
( releasedAt(X0,n1)
| ~ releasedAt(X0,n2)
| n0 = n1 )
| spl11_25 ),
inference(forward_subsumption_resolution,[],[f1185,f1096]) ).
fof(f1289,plain,
( ! [X0] :
( ~ releasedAt(X0,n2)
| releasedAt(X0,n1) )
| spl11_23
| spl11_25 ),
inference(forward_subsumption_resolution,[],[f1287,f1088]) ).
fof(f1467,plain,
! [X0] :
( releasedAt(X0,n2)
| ~ holdsAt(X0,n1)
| holdsAt(X0,n2)
| holdsAt(waterLevel(n3),n1)
| n0 = n1 ),
inference(resolution,[],[f522,f170]) ).
fof(f1473,plain,
( ! [X0] :
( releasedAt(X0,n2)
| ~ holdsAt(X0,n1)
| holdsAt(X0,n2)
| n0 = n1 )
| spl11_25 ),
inference(forward_subsumption_resolution,[],[f1467,f1096]) ).
fof(f1475,plain,
( ! [X0] :
( ~ holdsAt(X0,n1)
| releasedAt(X0,n2)
| holdsAt(X0,n2) )
| spl11_23
| spl11_25 ),
inference(forward_subsumption_resolution,[],[f1473,f1088]) ).
fof(f1478,plain,
( releasedAt(filling,n2)
| holdsAt(filling,n2)
| spl11_23
| spl11_25 ),
inference(resolution,[],[f1475,f628]) ).
fof(f1479,plain,
( holdsAt(filling,n2)
| spl11_17
| spl11_23
| spl11_25 ),
inference(forward_subsumption_resolution,[],[f1478,f837]) ).
fof(f1480,plain,
( $false
| spl11_17
| spl11_23
| spl11_25 ),
inference(forward_subsumption_resolution,[],[f1479,f128]) ).
fof(f1481,plain,
( spl11_17
| spl11_23
| spl11_25 ),
inference(avatar_contradiction_clause,[],[f1480]) ).
fof(f1489,plain,
( releasedAt(filling,n1)
| ~ spl11_17
| spl11_23
| spl11_25 ),
inference(resolution,[],[f836,f1289]) ).
fof(f1490,plain,
( $false
| spl11_15
| ~ spl11_17
| spl11_23
| spl11_25 ),
inference(forward_subsumption_resolution,[],[f1489,f823]) ).
fof(f1491,plain,
( spl11_15
| ~ spl11_17
| spl11_23
| spl11_25 ),
inference(avatar_contradiction_clause,[],[f1490]) ).
fof(f1492,plain,
~ releasedAt(filling,n1),
inference(forward_subsumption_resolution,[],[f844,f233]) ).
fof(f1493,plain,
( $false
| ~ spl11_15 ),
inference(forward_subsumption_resolution,[],[f1492,f822]) ).
fof(f1494,plain,
~ spl11_15,
inference(avatar_contradiction_clause,[],[f1493]) ).
fof(f1554,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n1)
| n3 = X0 )
| ~ spl11_25 ),
inference(resolution,[],[f1097,f133]) ).
fof(f2071,plain,
! [X0,X1] :
( ~ initiates(X0,filling,n0)
| ~ less(n0,X1)
| holdsAt(waterLevel(plus(n0,X1)),plus(n0,X1))
| stoppedIn(n0,filling,plus(n0,X1))
| ~ happens(X0,n0) ),
inference(resolution,[],[f549,f122]) ).
fof(f2093,definition,
( spl11_30
<=> ! [X1] :
( ~ less(n0,X1)
| stoppedIn(n0,filling,plus(n0,X1))
| holdsAt(waterLevel(plus(n0,X1)),plus(n0,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl11_30])],[avatar_definition]) ).
fof(f2094,plain,
( ! [X1] :
( holdsAt(waterLevel(plus(n0,X1)),plus(n0,X1))
| stoppedIn(n0,filling,plus(n0,X1))
| ~ less(n0,X1) )
| ~ spl11_30 ),
inference(avatar_component_clause,[],[f2093]) ).
fof(f2096,definition,
( spl11_31
<=> ! [X0] :
( ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ) ),
introduced(definition,[new_symbols(definition,[spl11_31])],[avatar_definition]) ).
fof(f2097,plain,
( ! [X0] :
( ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) )
| ~ spl11_31 ),
inference(avatar_component_clause,[],[f2096]) ).
fof(f2098,plain,
( spl11_30
| spl11_31 ),
inference(avatar_split_clause,[],[f2071,f2096,f2093]) ).
fof(f4497,plain,
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,n1)
| ~ less(n0,n1)
| ~ spl11_30 ),
inference(superposition,[],[f2094,f204]) ).
fof(f4503,plain,
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,n1)
| ~ spl11_30 ),
inference(forward_subsumption_resolution,[],[f4497,f254]) ).
fof(f4517,definition,
( spl11_72
<=> stoppedIn(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl11_72])],[avatar_definition]) ).
fof(f4519,plain,
( stoppedIn(n0,filling,n1)
| ~ spl11_72 ),
inference(avatar_component_clause,[],[f4517]) ).
fof(f4521,definition,
( spl11_73
<=> holdsAt(waterLevel(n1),n1) ),
introduced(definition,[new_symbols(definition,[spl11_73])],[avatar_definition]) ).
fof(f4523,plain,
( holdsAt(waterLevel(n1),n1)
| ~ spl11_73 ),
inference(avatar_component_clause,[],[f4521]) ).
fof(f4544,plain,
( ~ happens(tapOn,n0)
| ~ spl11_31 ),
inference(resolution,[],[f2097,f228]) ).
fof(f4548,plain,
( $false
| ~ spl11_31 ),
inference(forward_subsumption_resolution,[],[f4544,f233]) ).
fof(f4549,plain,
~ spl11_31,
inference(avatar_contradiction_clause,[],[f4548]) ).
fof(f4557,plain,
( spl11_72
| spl11_73
| ~ spl11_30 ),
inference(avatar_split_clause,[],[f4503,f2093,f4521,f4517]) ).
fof(f4697,plain,
( n0 = sK10(n0,filling,n1)
| ~ spl11_72 ),
inference(resolution,[],[f4519,f736]) ).
fof(f4700,plain,
( overflow = sK9(n0,filling,n1)
| tapOn = sK9(n0,filling,n1)
| ~ spl11_72 ),
inference(resolution,[],[f4519,f469]) ).
fof(f4703,definition,
( spl11_86
<=> tapOn = sK9(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl11_86])],[avatar_definition]) ).
fof(f4705,plain,
( tapOn = sK9(n0,filling,n1)
| ~ spl11_86 ),
inference(avatar_component_clause,[],[f4703]) ).
fof(f4707,definition,
( spl11_87
<=> overflow = sK9(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl11_87])],[avatar_definition]) ).
fof(f4709,plain,
( overflow = sK9(n0,filling,n1)
| ~ spl11_87 ),
inference(avatar_component_clause,[],[f4707]) ).
fof(f4710,plain,
( spl11_86
| spl11_87
| ~ spl11_72 ),
inference(avatar_split_clause,[],[f4700,f4517,f4707,f4703]) ).
fof(f4712,definition,
( spl11_88
<=> n0 = sK10(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl11_88])],[avatar_definition]) ).
fof(f4714,plain,
( n0 = sK10(n0,filling,n1)
| ~ spl11_88 ),
inference(avatar_component_clause,[],[f4712]) ).
fof(f4721,plain,
( spl11_88
| ~ spl11_72 ),
inference(avatar_split_clause,[],[f4697,f4517,f4712]) ).
fof(f4759,plain,
( n1 = n3
| ~ spl11_25
| ~ spl11_73 ),
inference(resolution,[],[f4523,f1554]) ).
fof(f4802,plain,
( overflow = sK9(n0,filling,n1)
| tapOff = sK9(n0,filling,n1)
| ~ spl11_72 ),
inference(resolution,[],[f4519,f478]) ).
fof(f4882,plain,
( happens(overflow,sK10(n0,filling,n1))
| ~ stoppedIn(n0,filling,n1)
| ~ spl11_87 ),
inference(superposition,[],[f218,f4709]) ).
fof(f4883,plain,
( happens(overflow,sK10(n0,filling,n1))
| ~ spl11_72
| ~ spl11_87 ),
inference(forward_subsumption_resolution,[],[f4882,f4519]) ).
fof(f4884,plain,
( happens(overflow,n0)
| ~ spl11_72
| ~ spl11_87
| ~ spl11_88 ),
inference(forward_demodulation,[],[f4883,f4714]) ).
fof(f4885,plain,
( $false
| spl11_5
| ~ spl11_72
| ~ spl11_87
| ~ spl11_88 ),
inference(forward_subsumption_resolution,[],[f4884,f647]) ).
fof(f4886,plain,
( spl11_5
| ~ spl11_72
| ~ spl11_87
| ~ spl11_88 ),
inference(avatar_contradiction_clause,[],[f4885]) ).
fof(f4888,plain,
( ~ holdsAt(filling,n1)
| ~ spl11_5 ),
inference(forward_subsumption_resolution,[],[f876,f646]) ).
fof(f4892,plain,
( $false
| ~ spl11_5 ),
inference(forward_subsumption_resolution,[],[f4888,f628]) ).
fof(f4893,plain,
~ spl11_5,
inference(avatar_contradiction_clause,[],[f4892]) ).
fof(f4900,plain,
( tapOn = overflow
| tapOff = sK9(n0,filling,n1)
| ~ spl11_72
| ~ spl11_86 ),
inference(forward_demodulation,[],[f4802,f4705]) ).
fof(f4903,plain,
( tapOff = sK9(n0,filling,n1)
| ~ spl11_72
| ~ spl11_86 ),
inference(forward_subsumption_resolution,[],[f4900,f166]) ).
fof(f4904,plain,
( tapOn = tapOff
| ~ spl11_72
| ~ spl11_86 ),
inference(forward_demodulation,[],[f4903,f4705]) ).
fof(f4905,plain,
( $false
| ~ spl11_72
| ~ spl11_86 ),
inference(forward_subsumption_resolution,[],[f4904,f167]) ).
fof(f4906,plain,
( ~ spl11_72
| ~ spl11_86 ),
inference(avatar_contradiction_clause,[],[f4905]) ).
fof(f4947,plain,
( less(n2,n1)
| ~ spl11_25
| ~ spl11_73 ),
inference(superposition,[],[f245,f4759]) ).
fof(f5056,plain,
( $false
| ~ spl11_25
| ~ spl11_73 ),
inference(forward_subsumption_resolution,[],[f4947,f250]) ).
fof(f5057,plain,
( ~ spl11_25
| ~ spl11_73 ),
inference(avatar_contradiction_clause,[],[f5056]) ).
cnf(s28,plain,
~ spl11_23,
inference(sat_conversion,[],[f1174]) ).
cnf(s36,plain,
( spl11_17
| spl11_23
| spl11_25 ),
inference(sat_conversion,[],[f1481]) ).
cnf(s37,plain,
( spl11_15
| ~ spl11_17
| spl11_23
| spl11_25 ),
inference(sat_conversion,[],[f1491]) ).
cnf(s38,plain,
~ spl11_15,
inference(sat_conversion,[],[f1494]) ).
cnf(s43,plain,
( spl11_30
| spl11_31 ),
inference(sat_conversion,[],[f2098]) ).
cnf(s104,plain,
~ spl11_31,
inference(sat_conversion,[],[f4549]) ).
cnf(s107,plain,
( ~ spl11_30
| spl11_72
| spl11_73 ),
inference(sat_conversion,[],[f4557]) ).
cnf(s116,plain,
( ~ spl11_72
| spl11_86
| spl11_87 ),
inference(sat_conversion,[],[f4710]) ).
cnf(s119,plain,
( ~ spl11_72
| spl11_88 ),
inference(sat_conversion,[],[f4721]) ).
cnf(s124,plain,
( spl11_5
| ~ spl11_72
| ~ spl11_87
| ~ spl11_88 ),
inference(sat_conversion,[],[f4886]) ).
cnf(s125,plain,
~ spl11_5,
inference(sat_conversion,[],[f4893]) ).
cnf(s128,plain,
( ~ spl11_72
| ~ spl11_86 ),
inference(sat_conversion,[],[f4906]) ).
cnf(s136,plain,
( ~ spl11_25
| ~ spl11_73 ),
inference(sat_conversion,[],[f5057]) ).
cnf(s137,plain,
( ~ spl11_72
| ~ spl11_87
| ~ spl11_88 ),
inference(rat,[],[s124,s125]) ).
cnf(s144,plain,
spl11_30,
inference(rat,[],[s43,s104]) ).
cnf(s145,plain,
( ~ spl11_17
| spl11_23
| spl11_25 ),
inference(rat,[],[s37,s38]) ).
cnf(s149,plain,
spl11_25,
inference(rat,[],[s36,s145,s28]) ).
cnf(s150,plain,
~ spl11_73,
inference(rat,[],[s136,s149]) ).
cnf(s155,plain,
spl11_72,
inference(rat,[],[s107,s144,s150]) ).
cnf(s160,plain,
~ spl11_86,
inference(rat,[],[s128,s155]) ).
cnf(s161,plain,
spl11_88,
inference(rat,[],[s119,s155]) ).
cnf(s162,plain,
spl11_87,
inference(rat,[],[s116,s160,s155]) ).
cnf(s163,plain,
$false,
inference(rat,[],[s137,s161,s155,s162]) ).
fof(f5062,plain,
$false,
inference(avatar_sat_refutation,[],[s163]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR009+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n016.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 22:10:19 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.29/1.93 % (4088691)Detected formulas, will run a generic FOF schedule.
% 7.29/1.93 % (4088715)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=3235222747:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 7.29/1.93 % (4088718)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2047001078:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 7.29/1.93 % (4088718)Refutation not found, incomplete strategy
% 7.29/1.93 % (4088718)------------------------------
% 7.29/1.93 % (4088718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.93 % (4088718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.93 % (4088718)CaDiCaL version: 2.1.3
% 7.29/1.93 % (4088718)Termination reason: Refutation not found, incomplete strategy
% 7.29/1.93 % (4088718)Time elapsed: 0.006 s
% 7.29/1.93 % (4088718)Peak memory usage: 88 MB
% 7.29/1.93 % (4088718)Instructions burned: 7 (million)
% 7.29/1.93 % (4088714)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=4128724270:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 7.29/1.93 % (4088717)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3657467699:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 7.29/1.93 % (4088717)Refutation not found, incomplete strategy
% 7.29/1.93 % (4088717)------------------------------
% 7.29/1.93 % (4088717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.93 % (4088717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.93 % (4088717)CaDiCaL version: 2.1.3
% 7.29/1.93 % (4088717)Termination reason: Refutation not found, incomplete strategy
% 7.29/1.93 % (4088717)Time elapsed: 0.002 s
% 7.29/1.93 % (4088717)Peak memory usage: 88 MB
% 7.29/1.93 % (4088717)Instructions burned: 1 (million)
% 7.29/1.93 % (4088716)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=3935454002:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 7.29/1.93 % (4088720)dis-21_1_sil=8000:lcm=predicate:random_seed=3450390185: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)
% 7.29/1.93 % (4088719)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1393045678:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 7.29/1.93 % (4088720)Instruction limit reached!
% 7.29/1.93 % (4088720)------------------------------
% 7.29/1.93 % (4088720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.93 % (4088720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.93 % (4088720)CaDiCaL version: 2.1.3
% 7.29/1.93 % (4088720)Termination reason: Instruction limit
% 7.29/1.93 % (4088720)Termination phase: Saturation
% 7.29/1.93 % (4088720)Time elapsed: 0.120 s
% 7.29/1.93 % (4088720)Peak memory usage: 89 MB
% 7.29/1.93 % (4088720)Instructions burned: 130 (million)
% 7.29/1.93 % (4088719)Instruction limit reached!
% 7.29/1.93 % (4088719)------------------------------
% 7.29/1.93 % (4088719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.93 % (4088719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.93 % (4088719)CaDiCaL version: 2.1.3
% 7.29/1.93 % (4088719)Termination reason: Instruction limit
% 7.29/1.93 % (4088719)Termination phase: Saturation
% 7.29/1.93 % (4088719)Time elapsed: 0.158 s
% 7.29/1.93 % (4088719)Peak memory usage: 90 MB
% 7.29/1.93 % (4088719)Instructions burned: 139 (million)
% 7.29/1.93 % (4088718)------------------------------
% 7.29/1.93 % (4088718)------------------------------
% 7.29/1.93 % (4088732)lrs+10_1_sil=8000:sp=occurrence:random_seed=3728816352:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 7.29/1.93 % (4088717)------------------------------
% 7.29/1.93 % (4088717)------------------------------
% 7.29/1.93 % (4088733)lrs+10_1_sil=32000:urr=on:br=off:random_seed=506079189:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 7.29/1.93 % (4088733)Refutation not found, incomplete strategy
% 7.29/1.93 % (4088733)------------------------------
% 7.29/1.93 % (4088733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.93 % (4088733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.93 % (4088733)CaDiCaL version: 2.1.3
% 7.29/1.93 % (4088733)Termination reason: Refutation not found, incomplete strategy
% 7.29/1.93 % (4088733)Time elapsed: 0.002 s
% 7.29/1.93 % (4088733)Peak memory usage: 88 MB
% 7.29/1.93 % (4088733)Instructions burned: 1 (million)
% 7.29/1.93 % (4088732)First to succeed.
% 7.29/1.93 % (4088715)Also succeeded, but the first one will report.
% 7.29/1.93 % (4088732)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4088691"
% 7.29/1.93 % (4088737)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1300124646:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 7.29/1.93 % (4088741)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=866219153:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 7.29/1.93 % (4088733)------------------------------
% 7.29/1.93 % (4088733)------------------------------
% 7.29/1.93 % (4088737)Instruction limit reached!
% 7.29/1.93 % (4088737)------------------------------
% 7.29/1.93 % (4088737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.93 % (4088737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.93 % (4088737)CaDiCaL version: 2.1.3
% 7.29/1.93 % (4088737)Termination reason: Instruction limit
% 7.29/1.93 % (4088737)Termination phase: Saturation
% 7.29/1.93 % (4088737)Time elapsed: 0.266 s
% 7.29/1.93 % (4088737)Peak memory usage: 90 MB
% 7.29/1.93 % (4088737)Instructions burned: 325 (million)
% 7.29/1.93 % (4088716)Refutation not found, incomplete strategy
% 7.29/1.93 % (4088716)------------------------------
% 7.29/1.93 % (4088716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.93 % (4088716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.93 % (4088741)Instruction limit reached!
% 7.29/1.93 % (4088741)------------------------------
% 7.29/1.93 % (4088741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.29/1.93 % (4088716)CaDiCaL version: 2.1.3
% 7.29/1.93 % (4088741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.93 % (4088716)Termination reason: Refutation not found, incomplete strategy
% 7.29/1.93 % (4088716)Time elapsed: 0.827 s
% 7.29/1.93 % (4088716)Peak memory usage: 128 MB
% 7.29/1.93 % (4088741)CaDiCaL version: 2.1.3
% 7.29/1.93 % (4088716)Instructions burned: 899 (million)
% 7.29/1.93 % (4088741)Termination reason: Instruction limit
% 7.29/1.93 % (4088741)Termination phase: Saturation
% 7.29/1.93 % (4088741)Time elapsed: 0.235 s
% 7.29/1.93 % (4088741)Peak memory usage: 91 MB
% 7.29/1.93 % (4088741)Instructions burned: 248 (million)
% 7.29/1.93 % (4088732)Refutation found. Thanks to Tanya!
% 7.29/1.93 % SZS status Theorem for theBenchmark
% 7.29/1.93 % SZS output start Proof for theBenchmark
% See solution above
% 8.79/2.13 % (4088732)------------------------------
% 8.79/2.13 % (4088732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.79/2.13 % (4088732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.79/2.13 % (4088732)CaDiCaL version: 2.1.3
% 8.79/2.13 % (4088732)Termination reason: Refutation
% 8.79/2.13 % (4088732)Time elapsed: 0.172 s
% 8.79/2.13 % (4088732)Peak memory usage: 91 MB
% 8.79/2.13 % (4088732)Instructions burned: 173 (million)
% 8.79/2.13 % (4088732)------------------------------
% 8.79/2.13 % (4088732)------------------------------
% 8.79/2.13 % (4088691)Success in time 1.154 s
% 8.79/2.13 % Vampire exiting
%------------------------------------------------------------------------------