%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR005+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:44:19 AM UTC 2026
% Result : Theorem 93.48s 13.59s
% Output : Refutation 93.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 52
% Syntax : Number of formulae : 305 ( 70 unt; 27 def)
% Number of atoms : 834 ( 134 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 873 ( 344 ~; 381 |; 104 &)
% ( 36 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 39 ( 37 usr; 21 prp; 0-4 aty)
% Number of functors : 15 ( 15 usr; 9 con; 0-3 aty)
% Number of variables : 304 ( 0 sgn 279 !; 25 ?)
% 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/Axioms/CSR001+0.ax',stoppedin_defn) ).
fof(f3,axiom,
! [X0,X1,X2,X3,X4] :
( ( happens(X0,X1)
& initiates(X0,X2,X1)
& less(n0,X4)
& trajectory(X2,X1,X3,X4)
& ~ stoppedIn(X1,X2,plus(X1,X4)) )
=> holdsAt(X3,plus(X1,X4)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax',change_holding) ).
fof(f5,axiom,
! [X0,X1] :
( ( holdsAt(X0,X1)
& ~ releasedAt(X0,plus(X1,n1))
& ~ ? [X2] :
( happens(X2,X1)
& terminates(X2,X0,X1) ) )
=> holdsAt(X0,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax',keep_holding) ).
fof(f8,axiom,
! [X0,X1] :
( ( ~ releasedAt(X0,X1)
& ~ ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) )
=> ~ releasedAt(X0,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax',keep_not_released) ).
fof(f9,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& initiates(X0,X2,X1) )
=> holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax',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/sandbox2/benchmark/Axioms/CSR001+0.ax',happens_not_released) ).
fof(f13,axiom,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = overflow
& X1 = waterLevel(X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+1.ax',initiates_all_defn) ).
fof(f16,axiom,
! [X0,X1] :
( happens(X0,X1)
<=> ( ( X0 = tapOn
& X1 = n0 )
| ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+1.ax',happens_all_defn) ).
fof(f17,axiom,
! [X0,X1,X2,X3] :
( ( holdsAt(waterLevel(X0),X1)
& X2 = plus(X0,X3) )
=> trajectory(filling,X1,waterLevel(X2),X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+1.ax',change_of_waterLevel) ).
fof(f18,axiom,
! [X0,X1,X2] :
( ( holdsAt(waterLevel(X1),X0)
& holdsAt(waterLevel(X2),X0) )
=> X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+1.ax',same_waterLevel) ).
fof(f21,axiom,
overflow != tapOn,
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+1.ax',overflow_not_tapOn) ).
fof(f27,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',plus0_1) ).
fof(f28,axiom,
plus(n0,n2) = n2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',plus0_2) ).
fof(f30,axiom,
plus(n1,n1) = n2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',plus1_1) ).
fof(f31,axiom,
plus(n1,n2) = n3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',plus1_2) ).
fof(f36,axiom,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_plus) ).
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(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(f50,axiom,
~ holdsAt(filling,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_filling_0) ).
fof(f55,axiom,
~ releasedAt(filling,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',filling_3_l1) ).
fof(f56,conjecture,
holdsAt(filling,n3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',filling_3) ).
fof(f57,negated_conjecture,
~ holdsAt(filling,n3),
inference(negated_conjecture,[status(cth)],[f56]) ).
fof(f58,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) )
| ? [X4] :
( holdsAt(waterLevel(X4),X2)
& X0 = overflow
& waterLevel(X4) = X1 ) ) ),
inference(rectify,[],[f13]) ).
fof(f59,plain,
~ holdsAt(filling,n3),
inference(flattening,[],[f57]) ).
fof(f61,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(f64,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,[],[f61]) ).
fof(f65,plain,
! [X0,X1,X2,X3,X4] :
( holdsAt(X3,plus(X1,X4))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1)
| ~ less(n0,X4)
| ~ trajectory(X2,X1,X3,X4)
| stoppedIn(X1,X2,plus(X1,X4)) ),
inference(ennf_transformation,[],[f3]) ).
fof(f66,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,[],[f65]) ).
fof(f67,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ? [X2] :
( happens(X2,X1)
& terminates(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f68,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ? [X2] :
( happens(X2,X1)
& terminates(X2,X0,X1) ) ),
inference(flattening,[],[f67]) ).
fof(f73,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f74,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(flattening,[],[f73]) ).
fof(f75,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f76,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(flattening,[],[f75]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(flattening,[],[f81]) ).
fof(f83,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(ennf_transformation,[],[f17]) ).
fof(f84,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(flattening,[],[f83]) ).
fof(f85,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f86,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(flattening,[],[f85]) ).
fof(f87,plain,
! [X0] : ~ less(X0,n0),
inference(ennf_transformation,[],[f38]) ).
fof(f88,definition,
! [X0,X2,X1] :
( ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) )
| ~ sP0(X0,X2,X1) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f89,plain,
! [X0,X1,X2] :
( sP0(X0,X2,X1)
| ~ stoppedIn(X0,X1,X2) ),
inference(definition_folding,[],[f64,f88]) ).
fof(f90,definition,
! [X2,X0,X1] :
( sP1(X2,X0,X1)
<=> ? [X4] :
( holdsAt(waterLevel(X4),X2)
& X0 = overflow
& waterLevel(X4) = X1 ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f91,definition,
! [X2,X0,X1] :
( sP2(X2,X0,X1)
<=> ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f92,definition,
! [X0,X1] :
( sP3(X0,X1)
<=> ( X0 = overflow
& X1 = spilling ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f93,definition,
! [X0,X1,X2] :
( sP4(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| sP3(X0,X1)
| sP2(X2,X0,X1)
| sP1(X2,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f94,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> sP4(X0,X1,X2) ),
inference(definition_folding,[],[f58,f93,f92,f91,f90]) ).
fof(f98,definition,
! [X1,X0] :
( sP7(X1,X0)
<=> ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow ) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f99,definition,
! [X0,X1] :
( sP8(X0,X1)
<=> ( ( X0 = tapOn
& X1 = n0 )
| sP7(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f100,plain,
! [X0,X1] :
( happens(X0,X1)
<=> sP8(X0,X1) ),
inference(definition_folding,[],[f16,f99,f98]) ).
fof(f101,plain,
! [X0,X2,X1] :
( ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) )
| ~ sP0(X0,X2,X1) ),
inference(nnf_transformation,[],[f88]) ).
fof(f102,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X1)
& terminates(X3,X2,X4) )
| ~ sP0(X0,X1,X2) ),
inference(rectify,[],[f101]) ).
fof(f103,plain,
! [X0,X1,X2] :
( ( happens(sK9(X0,X1,X2),sK10(X0,X1,X2))
& less(X0,sK10(X0,X1,X2))
& less(sK10(X0,X1,X2),X1)
& terminates(sK9(X0,X1,X2),X2,sK10(X0,X1,X2)) )
| ~ sP0(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10]),skolemize(X3,sK9(X0,X1,X2)),skolemize(X4,sK10(X0,X1,X2))],[f102]) ).
fof(f104,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ( happens(sK11(X0,X1),X1)
& terminates(sK11(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X2,sK11(X0,X1))],[f68]) ).
fof(f107,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ( happens(sK14(X0,X1),X1)
& releases(sK14(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X2,sK14(X0,X1))],[f74]) ).
fof(f108,plain,
! [X0,X1,X2] :
( ( sP4(X0,X1,X2)
| ( ( tapOn != X0
| filling != X1 )
& ~ sP3(X0,X1)
& ~ sP2(X2,X0,X1)
& ~ sP1(X2,X0,X1) ) )
& ( ( X0 = tapOn
& X1 = filling )
| sP3(X0,X1)
| sP2(X2,X0,X1)
| sP1(X2,X0,X1)
| ~ sP4(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f93]) ).
fof(f109,plain,
! [X0,X1,X2] :
( ( sP4(X0,X1,X2)
| ( ( tapOn != X0
| filling != X1 )
& ~ sP3(X0,X1)
& ~ sP2(X2,X0,X1)
& ~ sP1(X2,X0,X1) ) )
& ( ( X0 = tapOn
& X1 = filling )
| sP3(X0,X1)
| sP2(X2,X0,X1)
| sP1(X2,X0,X1)
| ~ sP4(X0,X1,X2) ) ),
inference(flattening,[],[f108]) ).
fof(f118,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ~ sP4(X0,X1,X2) )
& ( sP4(X0,X1,X2)
| ~ initiates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f94]) ).
fof(f127,plain,
! [X0,X1] :
( ( sP8(X0,X1)
| ( ( tapOn != X0
| n0 != X1 )
& ~ sP7(X1,X0) ) )
& ( ( X0 = tapOn
& X1 = n0 )
| sP7(X1,X0)
| ~ sP8(X0,X1) ) ),
inference(nnf_transformation,[],[f99]) ).
fof(f128,plain,
! [X0,X1] :
( ( sP8(X0,X1)
| ( ( tapOn != X0
| n0 != X1 )
& ~ sP7(X1,X0) ) )
& ( ( X0 = tapOn
& X1 = n0 )
| sP7(X1,X0)
| ~ sP8(X0,X1) ) ),
inference(flattening,[],[f127]) ).
fof(f129,plain,
! [X1,X0] :
( ( sP7(X1,X0)
| ~ holdsAt(waterLevel(n3),X1)
| ~ holdsAt(filling,X1)
| overflow != X0 )
& ( ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow )
| ~ sP7(X1,X0) ) ),
inference(nnf_transformation,[],[f98]) ).
fof(f130,plain,
! [X1,X0] :
( ( sP7(X1,X0)
| ~ holdsAt(waterLevel(n3),X1)
| ~ holdsAt(filling,X1)
| overflow != X0 )
& ( ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow )
| ~ sP7(X1,X0) ) ),
inference(flattening,[],[f129]) ).
fof(f131,plain,
! [X0,X1] :
( ( sP7(X0,X1)
| ~ holdsAt(waterLevel(n3),X0)
| ~ holdsAt(filling,X0)
| overflow != X1 )
& ( ( holdsAt(waterLevel(n3),X0)
& holdsAt(filling,X0)
& overflow = X1 )
| ~ sP7(X0,X1) ) ),
inference(rectify,[],[f130]) ).
fof(f132,plain,
! [X0,X1] :
( ( happens(X0,X1)
| ~ sP8(X0,X1) )
& ( sP8(X0,X1)
| ~ happens(X0,X1) ) ),
inference(nnf_transformation,[],[f100]) ).
fof(f134,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(f135,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,[],[f134]) ).
fof(f136,plain,
! [X0] :
( ( less(X0,n1)
| ~ less_or_equal(X0,n0) )
& ( less_or_equal(X0,n0)
| ~ less(X0,n1) ) ),
inference(nnf_transformation,[],[f39]) ).
fof(f137,plain,
! [X0] :
( ( less(X0,n2)
| ~ less_or_equal(X0,n1) )
& ( less_or_equal(X0,n1)
| ~ less(X0,n2) ) ),
inference(nnf_transformation,[],[f40]) ).
fof(f145,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(nnf_transformation,[],[f48]) ).
fof(f146,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(flattening,[],[f145]) ).
fof(f148,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| less(sK10(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f103]) ).
fof(f149,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| less(X0,sK10(X0,X1,X2)) ),
inference(cnf_transformation,[],[f103]) ).
fof(f150,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| happens(sK9(X0,X1,X2),sK10(X0,X1,X2)) ),
inference(cnf_transformation,[],[f103]) ).
fof(f151,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| sP0(X0,X2,X1) ),
inference(cnf_transformation,[],[f89]) ).
fof(f152,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,[],[f66]) ).
fof(f154,plain,
! [X0,X1] :
( ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1))
| releasedAt(X0,plus(X1,n1))
| happens(sK11(X0,X1),X1) ),
inference(cnf_transformation,[],[f104]) ).
fof(f160,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| happens(sK14(X0,X1),X1) ),
inference(cnf_transformation,[],[f107]) ).
fof(f161,plain,
! [X2,X0,X1] :
( ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1))
| ~ initiates(X0,X2,X1) ),
inference(cnf_transformation,[],[f76]) ).
fof(f165,plain,
! [X2,X0,X1] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(cnf_transformation,[],[f82]) ).
fof(f171,plain,
! [X2,X0,X1] :
( sP4(X0,X1,X2)
| tapOn != X0
| filling != X1 ),
inference(cnf_transformation,[],[f109]) ).
fof(f184,plain,
! [X2,X0,X1] :
( ~ sP4(X0,X1,X2)
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f118]) ).
fof(f197,plain,
! [X0,X1] :
( ~ sP8(X0,X1)
| sP7(X1,X0)
| n0 = X1 ),
inference(cnf_transformation,[],[f128]) ).
fof(f198,plain,
! [X0,X1] :
( ~ sP8(X0,X1)
| sP7(X1,X0)
| tapOn = X0 ),
inference(cnf_transformation,[],[f128]) ).
fof(f200,plain,
! [X0,X1] :
( sP8(X0,X1)
| tapOn != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f128]) ).
fof(f201,plain,
! [X0,X1] :
( ~ sP7(X0,X1)
| overflow = X1 ),
inference(cnf_transformation,[],[f131]) ).
fof(f203,plain,
! [X0,X1] :
( ~ sP7(X0,X1)
| holdsAt(waterLevel(n3),X0) ),
inference(cnf_transformation,[],[f131]) ).
fof(f205,plain,
! [X0,X1] :
( sP8(X0,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[],[f132]) ).
fof(f206,plain,
! [X0,X1] :
( ~ sP8(X0,X1)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f132]) ).
fof(f207,plain,
! [X2,X3,X0,X1] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(cnf_transformation,[],[f84]) ).
fof(f208,plain,
! [X2,X0,X1] :
( ~ holdsAt(waterLevel(X2),X0)
| ~ holdsAt(waterLevel(X1),X0)
| X1 = X2 ),
inference(cnf_transformation,[],[f86]) ).
fof(f211,plain,
tapOn != overflow,
inference(cnf_transformation,[],[f21]) ).
fof(f218,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f27]) ).
fof(f219,plain,
n2 = plus(n0,n2),
inference(cnf_transformation,[],[f28]) ).
fof(f221,plain,
n2 = plus(n1,n1),
inference(cnf_transformation,[],[f30]) ).
fof(f222,plain,
n3 = plus(n1,n2),
inference(cnf_transformation,[],[f31]) ).
fof(f227,plain,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[],[f36]) ).
fof(f228,plain,
! [X0,X1] :
( ~ less_or_equal(X0,X1)
| X0 = X1
| less(X0,X1) ),
inference(cnf_transformation,[],[f135]) ).
fof(f229,plain,
! [X0,X1] :
( less_or_equal(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f135]) ).
fof(f230,plain,
! [X0,X1] :
( less_or_equal(X0,X1)
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f135]) ).
fof(f231,plain,
! [X0] : ~ less(X0,n0),
inference(cnf_transformation,[],[f87]) ).
fof(f232,plain,
! [X0] :
( less_or_equal(X0,n0)
| ~ less(X0,n1) ),
inference(cnf_transformation,[],[f136]) ).
fof(f233,plain,
! [X0] :
( ~ less_or_equal(X0,n0)
| less(X0,n1) ),
inference(cnf_transformation,[],[f136]) ).
fof(f234,plain,
! [X0] :
( less_or_equal(X0,n1)
| ~ less(X0,n2) ),
inference(cnf_transformation,[],[f137]) ).
fof(f235,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| less(X0,n2) ),
inference(cnf_transformation,[],[f137]) ).
fof(f251,plain,
! [X0,X1] :
( ~ less(X0,X1)
| ~ less(X1,X0) ),
inference(cnf_transformation,[],[f146]) ).
fof(f253,plain,
holdsAt(waterLevel(n0),n0),
inference(cnf_transformation,[],[f49]) ).
fof(f254,plain,
~ holdsAt(filling,n0),
inference(cnf_transformation,[],[f50]) ).
fof(f259,plain,
~ releasedAt(filling,n3),
inference(cnf_transformation,[],[f55]) ).
fof(f260,plain,
~ holdsAt(filling,n3),
inference(cnf_transformation,[],[f59]) ).
fof(f261,plain,
! [X2,X1] :
( sP4(tapOn,X1,X2)
| filling != X1 ),
inference(equality_resolution,[],[f171]) ).
fof(f262,plain,
! [X2] : sP4(tapOn,filling,X2),
inference(equality_resolution,[],[f261]) ).
fof(f275,plain,
! [X1] :
( sP8(tapOn,X1)
| n0 != X1 ),
inference(equality_resolution,[],[f200]) ).
fof(f276,plain,
sP8(tapOn,n0),
inference(equality_resolution,[],[f275]) ).
fof(f278,plain,
! [X3,X0,X1] :
( ~ holdsAt(waterLevel(X0),X1)
| trajectory(filling,X1,waterLevel(plus(X0,X3)),X3) ),
inference(equality_resolution,[],[f207]) ).
fof(f280,plain,
! [X1] : less_or_equal(X1,X1),
inference(equality_resolution,[],[f229]) ).
fof(f283,plain,
n1 = plus(n1,n0),
inference(forward_demodulation,[],[f218,f227]) ).
fof(f286,plain,
happens(tapOn,n0),
inference(resolution,[],[f206,f276]) ).
fof(f289,plain,
less(n0,n1),
inference(resolution,[],[f233,f280]) ).
fof(f296,plain,
! [X0] : initiates(tapOn,filling,X0),
inference(resolution,[],[f184,f262]) ).
fof(f303,plain,
! [X0] :
( holdsAt(X0,plus(n0,n1))
| ~ initiates(tapOn,X0,n0) ),
inference(resolution,[],[f161,f286]) ).
fof(f304,plain,
! [X0] :
( holdsAt(X0,plus(n1,n0))
| ~ initiates(tapOn,X0,n0) ),
inference(forward_demodulation,[],[f303,f227]) ).
fof(f305,plain,
! [X0] :
( ~ initiates(tapOn,X0,n0)
| holdsAt(X0,n1) ),
inference(forward_demodulation,[],[f304,f283]) ).
fof(f307,plain,
less(n1,n2),
inference(resolution,[],[f235,f280]) ).
fof(f308,plain,
! [X0] :
( ~ less(X0,n1)
| less(X0,n2) ),
inference(resolution,[],[f235,f230]) ).
fof(f352,plain,
~ less(n2,n1),
inference(resolution,[],[f251,f307]) ).
fof(f406,plain,
! [X2,X0,X1] :
( ~ initiates(X2,X1,X0)
| ~ happens(X2,X0)
| ~ releasedAt(X1,plus(n1,X0)) ),
inference(superposition,[],[f165,f227]) ).
fof(f411,plain,
! [X0] :
( n0 = X0
| less(X0,n0)
| ~ less(X0,n1) ),
inference(resolution,[],[f228,f232]) ).
fof(f412,plain,
! [X0] :
( ~ less(X0,n2)
| less(X0,n1)
| n1 = X0 ),
inference(resolution,[],[f228,f234]) ).
fof(f416,plain,
! [X0] :
( ~ less(X0,n1)
| n0 = X0 ),
inference(global_subsumption,[],[f411,f231]) ).
fof(f465,plain,
less(n0,n2),
inference(resolution,[],[f308,f289]) ).
fof(f599,plain,
! [X0] :
( ~ happens(tapOn,X0)
| ~ releasedAt(filling,plus(n1,X0)) ),
inference(resolution,[],[f406,f296]) ).
fof(f615,plain,
! [X0] :
( ~ releasedAt(X0,n2)
| releasedAt(X0,n1)
| happens(sK14(X0,n1),n1) ),
inference(superposition,[],[f160,f221]) ).
fof(f920,definition,
( spl18_35
<=> n0 = n2 ),
introduced(definition,[new_symbols(definition,[spl18_35])],[avatar_definition]) ).
fof(f922,plain,
( n0 = n2
| ~ spl18_35 ),
inference(avatar_component_clause,[],[f920]) ).
fof(f1497,plain,
! [X0] :
( ~ less(X0,n2)
| n0 = X0
| n1 = X0 ),
inference(global_subsumption,[],[f416,f412]) ).
fof(f2055,plain,
( ~ less(n0,n1)
| ~ spl18_35 ),
inference(superposition,[],[f352,f922]) ).
fof(f2120,plain,
( $false
| ~ spl18_35 ),
inference(global_subsumption,[],[f2055,f289]) ).
fof(f2121,plain,
~ spl18_35,
inference(avatar_contradiction_clause,[],[f2120]) ).
fof(f5073,plain,
holdsAt(filling,n1),
inference(resolution,[],[f305,f296]) ).
fof(f5142,plain,
( holdsAt(filling,plus(n1,n1))
| releasedAt(filling,plus(n1,n1))
| happens(sK11(filling,n1),n1) ),
inference(resolution,[],[f5073,f154]) ).
fof(f5143,plain,
( holdsAt(filling,n2)
| releasedAt(filling,plus(n1,n1))
| happens(sK11(filling,n1),n1) ),
inference(forward_demodulation,[],[f5142,f221]) ).
fof(f5147,plain,
( releasedAt(filling,n2)
| holdsAt(filling,n2)
| happens(sK11(filling,n1),n1) ),
inference(forward_demodulation,[],[f5143,f221]) ).
fof(f5154,definition,
( spl18_79
<=> releasedAt(filling,n1) ),
introduced(definition,[new_symbols(definition,[spl18_79])],[avatar_definition]) ).
fof(f5164,definition,
( spl18_81
<=> happens(sK11(filling,n1),n1) ),
introduced(definition,[new_symbols(definition,[spl18_81])],[avatar_definition]) ).
fof(f5166,plain,
( happens(sK11(filling,n1),n1)
| ~ spl18_81 ),
inference(avatar_component_clause,[],[f5164]) ).
fof(f5168,definition,
( spl18_82
<=> holdsAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl18_82])],[avatar_definition]) ).
fof(f5170,plain,
( holdsAt(filling,n2)
| ~ spl18_82 ),
inference(avatar_component_clause,[],[f5168]) ).
fof(f5172,definition,
( spl18_83
<=> releasedAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl18_83])],[avatar_definition]) ).
fof(f5174,plain,
( releasedAt(filling,n2)
| ~ spl18_83 ),
inference(avatar_component_clause,[],[f5172]) ).
fof(f5175,plain,
( spl18_81
| spl18_82
| spl18_83 ),
inference(avatar_split_clause,[],[f5147,f5172,f5168,f5164]) ).
fof(f5383,plain,
( holdsAt(filling,plus(n2,n1))
| releasedAt(filling,plus(n2,n1))
| happens(sK11(filling,n2),n2)
| ~ spl18_82 ),
inference(resolution,[],[f5170,f154]) ).
fof(f5384,plain,
( holdsAt(filling,plus(n1,n2))
| releasedAt(filling,plus(n2,n1))
| happens(sK11(filling,n2),n2)
| ~ spl18_82 ),
inference(forward_demodulation,[],[f5383,f227]) ).
fof(f5386,plain,
( holdsAt(filling,n3)
| releasedAt(filling,plus(n2,n1))
| happens(sK11(filling,n2),n2)
| ~ spl18_82 ),
inference(forward_demodulation,[],[f5384,f222]) ).
fof(f5388,plain,
( releasedAt(filling,plus(n1,n2))
| holdsAt(filling,n3)
| happens(sK11(filling,n2),n2)
| ~ spl18_82 ),
inference(forward_demodulation,[],[f5386,f227]) ).
fof(f5390,plain,
( releasedAt(filling,n3)
| holdsAt(filling,n3)
| happens(sK11(filling,n2),n2)
| ~ spl18_82 ),
inference(forward_demodulation,[],[f5388,f222]) ).
fof(f5392,plain,
( happens(sK11(filling,n2),n2)
| ~ spl18_82 ),
inference(global_subsumption,[],[f5390,f259,f260]) ).
fof(f6343,plain,
~ releasedAt(filling,plus(n1,n0)),
inference(resolution,[],[f599,f286]) ).
fof(f6344,plain,
~ releasedAt(filling,n1),
inference(forward_demodulation,[],[f6343,f283]) ).
fof(f6953,plain,
! [X0,X1] :
( sP7(X0,X1)
| n0 = X0
| ~ happens(X1,X0) ),
inference(resolution,[],[f197,f205]) ).
fof(f6955,plain,
! [X0,X1] :
( sP7(X0,X1)
| tapOn = X1
| ~ happens(X1,X0) ),
inference(resolution,[],[f198,f205]) ).
fof(f7012,plain,
! [X0,X1] :
( ~ happens(X1,X0)
| n0 = X0
| holdsAt(waterLevel(n3),X0) ),
inference(resolution,[],[f6953,f203]) ).
fof(f7014,plain,
! [X0,X1] :
( ~ happens(X1,X0)
| n0 = X0
| overflow = X1 ),
inference(resolution,[],[f6953,f201]) ).
fof(f7016,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| tapOn = X0
| holdsAt(waterLevel(n3),X1) ),
inference(resolution,[],[f6955,f203]) ).
fof(f8449,plain,
( n0 = n2
| overflow = sK11(filling,n2)
| ~ spl18_82 ),
inference(resolution,[],[f7014,f5392]) ).
fof(f8464,definition,
( spl18_176
<=> n0 = n1 ),
introduced(definition,[new_symbols(definition,[spl18_176])],[avatar_definition]) ).
fof(f8466,plain,
( n0 = n1
| ~ spl18_176 ),
inference(avatar_component_clause,[],[f8464]) ).
fof(f8472,definition,
( spl18_177
<=> overflow = sK11(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl18_177])],[avatar_definition]) ).
fof(f8474,plain,
( overflow = sK11(filling,n2)
| ~ spl18_177 ),
inference(avatar_component_clause,[],[f8472]) ).
fof(f8475,plain,
( spl18_177
| spl18_35
| ~ spl18_82 ),
inference(avatar_split_clause,[],[f8449,f5168,f920,f8472]) ).
fof(f8545,plain,
( happens(overflow,n2)
| ~ spl18_82
| ~ spl18_177 ),
inference(superposition,[],[f5392,f8474]) ).
fof(f10900,plain,
( releasedAt(filling,n1)
| happens(sK14(filling,n1),n1)
| ~ spl18_83 ),
inference(resolution,[],[f5174,f615]) ).
fof(f10908,definition,
( spl18_221
<=> happens(sK14(filling,n1),n1) ),
introduced(definition,[new_symbols(definition,[spl18_221])],[avatar_definition]) ).
fof(f10910,plain,
( happens(sK14(filling,n1),n1)
| ~ spl18_221 ),
inference(avatar_component_clause,[],[f10908]) ).
fof(f10911,plain,
( spl18_221
| spl18_79
| ~ spl18_83 ),
inference(avatar_split_clause,[],[f10900,f5172,f5154,f10908]) ).
fof(f14088,plain,
( ~ holdsAt(filling,n1)
| ~ spl18_176 ),
inference(superposition,[],[f254,f8466]) ).
fof(f14195,plain,
( $false
| ~ spl18_176 ),
inference(global_subsumption,[],[f14088,f5073]) ).
fof(f14196,plain,
~ spl18_176,
inference(avatar_contradiction_clause,[],[f14195]) ).
fof(f16482,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(n0,X0)),X0),
inference(resolution,[],[f278,f253]) ).
fof(f16486,plain,
trajectory(filling,n0,waterLevel(n2),n2),
inference(superposition,[],[f16482,f219]) ).
fof(f16489,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(X0,n0)),X0),
inference(superposition,[],[f16482,f227]) ).
fof(f16502,plain,
! [X0] :
( ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,n2)
| holdsAt(waterLevel(n2),plus(n0,n2))
| stoppedIn(n0,filling,plus(n0,n2)) ),
inference(resolution,[],[f152,f16486]) ).
fof(f16503,plain,
! [X0] :
( holdsAt(waterLevel(n2),n2)
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,n2)
| stoppedIn(n0,filling,plus(n0,n2)) ),
inference(forward_demodulation,[],[f16502,f219]) ).
fof(f16509,definition,
( spl18_245
<=> ! [X0] :
( ~ happens(X0,n0)
| ~ initiates(X0,filling,n0) ) ),
introduced(definition,[new_symbols(definition,[spl18_245])],[avatar_definition]) ).
fof(f16510,plain,
( ! [X0] :
( ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) )
| ~ spl18_245 ),
inference(avatar_component_clause,[],[f16509]) ).
fof(f16512,plain,
! [X0] :
( stoppedIn(n0,filling,n2)
| holdsAt(waterLevel(n2),n2)
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,n2) ),
inference(forward_demodulation,[],[f16503,f219]) ).
fof(f16514,plain,
! [X0] :
( stoppedIn(n0,filling,n2)
| holdsAt(waterLevel(n2),n2)
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0) ),
inference(global_subsumption,[],[f16512,f465]) ).
fof(f16517,definition,
( spl18_246
<=> holdsAt(waterLevel(n2),n2) ),
introduced(definition,[new_symbols(definition,[spl18_246])],[avatar_definition]) ).
fof(f16519,plain,
( holdsAt(waterLevel(n2),n2)
| ~ spl18_246 ),
inference(avatar_component_clause,[],[f16517]) ).
fof(f16521,definition,
( spl18_247
<=> stoppedIn(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl18_247])],[avatar_definition]) ).
fof(f16523,plain,
( stoppedIn(n0,filling,n2)
| ~ spl18_247 ),
inference(avatar_component_clause,[],[f16521]) ).
fof(f16524,plain,
( spl18_245
| spl18_246
| spl18_247 ),
inference(avatar_split_clause,[],[f16514,f16521,f16517,f16509]) ).
fof(f16538,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n2)
| n2 = X0 )
| ~ spl18_246 ),
inference(resolution,[],[f16519,f208]) ).
fof(f16616,definition,
( spl18_260
<=> holdsAt(waterLevel(n3),n2) ),
introduced(definition,[new_symbols(definition,[spl18_260])],[avatar_definition]) ).
fof(f16618,plain,
( holdsAt(waterLevel(n3),n2)
| ~ spl18_260 ),
inference(avatar_component_clause,[],[f16616]) ).
fof(f16803,definition,
( spl18_279
<=> happens(overflow,n2) ),
introduced(definition,[new_symbols(definition,[spl18_279])],[avatar_definition]) ).
fof(f16804,plain,
( happens(overflow,n2)
| ~ spl18_279 ),
inference(avatar_component_clause,[],[f16803]) ).
fof(f16966,plain,
trajectory(filling,n0,waterLevel(n1),n1),
inference(superposition,[],[f16489,f283]) ).
fof(f17527,plain,
! [X0] :
( ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,n1)
| holdsAt(waterLevel(n1),plus(n0,n1))
| stoppedIn(n0,filling,plus(n0,n1)) ),
inference(resolution,[],[f16966,f152]) ).
fof(f17528,plain,
! [X0] :
( holdsAt(waterLevel(n1),plus(n1,n0))
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,n1)
| stoppedIn(n0,filling,plus(n0,n1)) ),
inference(forward_demodulation,[],[f17527,f227]) ).
fof(f17529,plain,
! [X0] :
( holdsAt(waterLevel(n1),n1)
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,n1)
| stoppedIn(n0,filling,plus(n0,n1)) ),
inference(forward_demodulation,[],[f17528,f283]) ).
fof(f17530,plain,
! [X0] :
( stoppedIn(n0,filling,plus(n1,n0))
| holdsAt(waterLevel(n1),n1)
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,n1) ),
inference(forward_demodulation,[],[f17529,f227]) ).
fof(f17531,plain,
! [X0] :
( stoppedIn(n0,filling,n1)
| holdsAt(waterLevel(n1),n1)
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,n1) ),
inference(forward_demodulation,[],[f17530,f283]) ).
fof(f17532,plain,
! [X0] :
( stoppedIn(n0,filling,n1)
| holdsAt(waterLevel(n1),n1)
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0) ),
inference(global_subsumption,[],[f17531,f289]) ).
fof(f17534,definition,
( spl18_301
<=> holdsAt(waterLevel(n1),n1) ),
introduced(definition,[new_symbols(definition,[spl18_301])],[avatar_definition]) ).
fof(f17536,plain,
( holdsAt(waterLevel(n1),n1)
| ~ spl18_301 ),
inference(avatar_component_clause,[],[f17534]) ).
fof(f17538,definition,
( spl18_302
<=> stoppedIn(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl18_302])],[avatar_definition]) ).
fof(f17540,plain,
( stoppedIn(n0,filling,n1)
| ~ spl18_302 ),
inference(avatar_component_clause,[],[f17538]) ).
fof(f17541,plain,
( spl18_245
| spl18_301
| spl18_302 ),
inference(avatar_split_clause,[],[f17532,f17538,f17534,f16509]) ).
fof(f17598,plain,
( sP0(n0,n1,filling)
| ~ spl18_302 ),
inference(resolution,[],[f17540,f151]) ).
fof(f17601,plain,
( less(n0,sK10(n0,n1,filling))
| ~ spl18_302 ),
inference(resolution,[],[f17598,f149]) ).
fof(f17602,plain,
( less(sK10(n0,n1,filling),n1)
| ~ spl18_302 ),
inference(resolution,[],[f17598,f148]) ).
fof(f17795,plain,
( n0 = sK10(n0,n1,filling)
| ~ spl18_302 ),
inference(resolution,[],[f17602,f416]) ).
fof(f17860,definition,
( spl18_325
<=> holdsAt(waterLevel(n3),n1) ),
introduced(definition,[new_symbols(definition,[spl18_325])],[avatar_definition]) ).
fof(f17862,plain,
( holdsAt(waterLevel(n3),n1)
| ~ spl18_325 ),
inference(avatar_component_clause,[],[f17860]) ).
fof(f19636,plain,
( less(n0,n0)
| ~ spl18_302 ),
inference(superposition,[],[f17601,f17795]) ).
fof(f19645,plain,
( $false
| ~ spl18_302 ),
inference(resolution,[],[f19636,f231]) ).
fof(f19649,plain,
~ spl18_302,
inference(avatar_contradiction_clause,[],[f19645]) ).
fof(f19764,plain,
( ~ happens(tapOn,n0)
| ~ spl18_245 ),
inference(resolution,[],[f16510,f296]) ).
fof(f19765,plain,
( $false
| ~ spl18_245 ),
inference(global_subsumption,[],[f19764,f286]) ).
fof(f19766,plain,
~ spl18_245,
inference(avatar_contradiction_clause,[],[f19765]) ).
fof(f19776,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n1)
| n1 = X0 )
| ~ spl18_301 ),
inference(resolution,[],[f17536,f208]) ).
fof(f20578,plain,
( n3 = n2
| ~ spl18_246
| ~ spl18_260 ),
inference(resolution,[],[f16538,f16618]) ).
fof(f20661,plain,
( sP0(n0,n2,filling)
| ~ spl18_247 ),
inference(resolution,[],[f16523,f151]) ).
fof(f20684,plain,
( happens(sK9(n0,n2,filling),sK10(n0,n2,filling))
| ~ spl18_247 ),
inference(resolution,[],[f20661,f150]) ).
fof(f20685,plain,
( less(n0,sK10(n0,n2,filling))
| ~ spl18_247 ),
inference(resolution,[],[f20661,f149]) ).
fof(f20686,plain,
( less(sK10(n0,n2,filling),n2)
| ~ spl18_247 ),
inference(resolution,[],[f20661,f148]) ).
fof(f20746,plain,
( n0 = sK10(n0,n2,filling)
| n1 = sK10(n0,n2,filling)
| ~ spl18_247 ),
inference(resolution,[],[f20686,f1497]) ).
fof(f20751,definition,
( spl18_511
<=> n1 = sK10(n0,n2,filling) ),
introduced(definition,[new_symbols(definition,[spl18_511])],[avatar_definition]) ).
fof(f20753,plain,
( n1 = sK10(n0,n2,filling)
| ~ spl18_511 ),
inference(avatar_component_clause,[],[f20751]) ).
fof(f20760,definition,
( spl18_513
<=> n0 = sK10(n0,n2,filling) ),
introduced(definition,[new_symbols(definition,[spl18_513])],[avatar_definition]) ).
fof(f20762,plain,
( n0 = sK10(n0,n2,filling)
| ~ spl18_513 ),
inference(avatar_component_clause,[],[f20760]) ).
fof(f20763,plain,
( spl18_511
| spl18_513
| ~ spl18_247 ),
inference(avatar_split_clause,[],[f20746,f16521,f20760,f20751]) ).
fof(f22782,definition,
( spl18_612
<=> n3 = n2 ),
introduced(definition,[new_symbols(definition,[spl18_612])],[avatar_definition]) ).
fof(f22784,plain,
( n3 = n2
| ~ spl18_612 ),
inference(avatar_component_clause,[],[f22782]) ).
fof(f27648,definition,
( spl18_822
<=> n1 = n3 ),
introduced(definition,[new_symbols(definition,[spl18_822])],[avatar_definition]) ).
fof(f27650,plain,
( n1 = n3
| ~ spl18_822 ),
inference(avatar_component_clause,[],[f27648]) ).
fof(f29985,plain,
( n0 = sK10(n0,n2,filling)
| holdsAt(waterLevel(n3),sK10(n0,n2,filling))
| ~ spl18_247 ),
inference(resolution,[],[f20684,f7012]) ).
fof(f30005,plain,
( n0 = n1
| holdsAt(waterLevel(n3),sK10(n0,n2,filling))
| ~ spl18_247
| ~ spl18_511 ),
inference(forward_demodulation,[],[f29985,f20753]) ).
fof(f30012,plain,
( holdsAt(waterLevel(n3),n1)
| n0 = n1
| ~ spl18_247
| ~ spl18_511 ),
inference(forward_demodulation,[],[f30005,f20753]) ).
fof(f30016,plain,
( spl18_176
| spl18_325
| ~ spl18_247
| ~ spl18_511 ),
inference(avatar_split_clause,[],[f30012,f20751,f16521,f17860,f8464]) ).
fof(f30161,plain,
( less(n0,n0)
| ~ spl18_247
| ~ spl18_513 ),
inference(superposition,[],[f20685,f20762]) ).
fof(f30227,plain,
( $false
| ~ spl18_247
| ~ spl18_513 ),
inference(resolution,[],[f30161,f231]) ).
fof(f30231,plain,
( ~ spl18_247
| ~ spl18_513 ),
inference(avatar_contradiction_clause,[],[f30227]) ).
fof(f30242,plain,
( spl18_612
| ~ spl18_246
| ~ spl18_260 ),
inference(avatar_split_clause,[],[f20578,f16616,f16517,f22782]) ).
fof(f30249,plain,
( spl18_279
| ~ spl18_82
| ~ spl18_177 ),
inference(avatar_split_clause,[],[f8545,f8472,f5168,f16803]) ).
fof(f30787,plain,
( n0 = n1
| holdsAt(waterLevel(n3),n1)
| ~ spl18_221 ),
inference(resolution,[],[f10910,f7012]) ).
fof(f30804,plain,
( spl18_325
| spl18_176
| ~ spl18_221 ),
inference(avatar_split_clause,[],[f30787,f10908,f8464,f17860]) ).
fof(f30809,plain,
~ spl18_79,
inference(avatar_split_clause,[],[f6344,f5154]) ).
fof(f30911,plain,
( n0 = n1
| holdsAt(waterLevel(n3),n1)
| ~ spl18_81 ),
inference(resolution,[],[f5166,f7012]) ).
fof(f30928,plain,
( spl18_325
| spl18_176
| ~ spl18_81 ),
inference(avatar_split_clause,[],[f30911,f5164,f8464,f17860]) ).
fof(f31113,plain,
( n1 = n3
| ~ spl18_301
| ~ spl18_325 ),
inference(resolution,[],[f17862,f19776]) ).
fof(f31130,plain,
( spl18_822
| ~ spl18_301
| ~ spl18_325 ),
inference(avatar_split_clause,[],[f31113,f17860,f17534,f27648]) ).
fof(f31179,plain,
( ~ holdsAt(filling,n1)
| ~ spl18_822 ),
inference(superposition,[],[f260,f27650]) ).
fof(f31394,plain,
( $false
| ~ spl18_822 ),
inference(global_subsumption,[],[f31179,f5073]) ).
fof(f31395,plain,
~ spl18_822,
inference(avatar_contradiction_clause,[],[f31394]) ).
fof(f31461,plain,
( tapOn = overflow
| holdsAt(waterLevel(n3),n2)
| ~ spl18_279 ),
inference(resolution,[],[f16804,f7016]) ).
fof(f31464,plain,
( holdsAt(waterLevel(n3),n2)
| ~ spl18_279 ),
inference(global_subsumption,[],[f31461,f211]) ).
fof(f31470,plain,
( spl18_260
| ~ spl18_279 ),
inference(avatar_split_clause,[],[f31464,f16803,f16616]) ).
fof(f31588,plain,
( holdsAt(filling,n3)
| ~ spl18_82
| ~ spl18_612 ),
inference(superposition,[],[f5170,f22784]) ).
fof(f31703,plain,
( $false
| ~ spl18_82
| ~ spl18_612 ),
inference(global_subsumption,[],[f31588,f260]) ).
fof(f31704,plain,
( ~ spl18_82
| ~ spl18_612 ),
inference(avatar_contradiction_clause,[],[f31703]) ).
cnf(s750,plain,
~ spl18_35,
inference(sat_conversion,[],[f2121]) ).
cnf(s981,plain,
( spl18_81
| spl18_82
| spl18_83 ),
inference(sat_conversion,[],[f5175]) ).
cnf(s1849,plain,
( spl18_35
| ~ spl18_82
| spl18_177 ),
inference(sat_conversion,[],[f8475]) ).
cnf(s2027,plain,
( spl18_79
| ~ spl18_83
| spl18_221 ),
inference(sat_conversion,[],[f10911]) ).
cnf(s2333,plain,
~ spl18_176,
inference(sat_conversion,[],[f14196]) ).
cnf(s2419,plain,
( spl18_245
| spl18_246
| spl18_247 ),
inference(sat_conversion,[],[f16524]) ).
cnf(s2880,plain,
( spl18_245
| spl18_301
| spl18_302 ),
inference(sat_conversion,[],[f17541]) ).
cnf(s3733,plain,
~ spl18_302,
inference(sat_conversion,[],[f19649]) ).
cnf(s3790,plain,
~ spl18_245,
inference(sat_conversion,[],[f19766]) ).
cnf(s4161,plain,
( ~ spl18_247
| spl18_511
| spl18_513 ),
inference(sat_conversion,[],[f20763]) ).
cnf(s6860,plain,
( spl18_176
| ~ spl18_247
| spl18_325
| ~ spl18_511 ),
inference(sat_conversion,[],[f30016]) ).
cnf(s6901,plain,
( ~ spl18_247
| ~ spl18_513 ),
inference(sat_conversion,[],[f30231]) ).
cnf(s6904,plain,
( ~ spl18_246
| ~ spl18_260
| spl18_612 ),
inference(sat_conversion,[],[f30242]) ).
cnf(s6919,plain,
( ~ spl18_82
| ~ spl18_177
| spl18_279 ),
inference(sat_conversion,[],[f30249]) ).
cnf(s7074,plain,
( spl18_176
| ~ spl18_221
| spl18_325 ),
inference(sat_conversion,[],[f30804]) ).
cnf(s7083,plain,
~ spl18_79,
inference(sat_conversion,[],[f30809]) ).
cnf(s7100,plain,
( ~ spl18_81
| spl18_176
| spl18_325 ),
inference(sat_conversion,[],[f30928]) ).
cnf(s7177,plain,
( ~ spl18_301
| ~ spl18_325
| spl18_822 ),
inference(sat_conversion,[],[f31130]) ).
cnf(s7293,plain,
~ spl18_822,
inference(sat_conversion,[],[f31395]) ).
cnf(s7360,plain,
( spl18_260
| ~ spl18_279 ),
inference(sat_conversion,[],[f31470]) ).
cnf(s7427,plain,
( ~ spl18_82
| ~ spl18_612 ),
inference(sat_conversion,[],[f31704]) ).
cnf(s7449,plain,
( ~ spl18_301
| ~ spl18_325 ),
inference(rat,[],[s7177,s7293]) ).
cnf(s7501,plain,
spl18_301,
inference(rat,[],[s2880,s3733,s3790]) ).
cnf(s7502,plain,
~ spl18_325,
inference(rat,[],[s7449,s7501]) ).
cnf(s7516,plain,
( spl18_246
| spl18_247 ),
inference(rat,[],[s2419,s3790]) ).
cnf(s7519,plain,
~ spl18_81,
inference(rat,[],[s7100,s7502,s2333]) ).
cnf(s7520,plain,
~ spl18_221,
inference(rat,[],[s7074,s7502,s2333]) ).
cnf(s7532,plain,
~ spl18_83,
inference(rat,[],[s2027,s7520,s7083]) ).
cnf(s7587,plain,
spl18_82,
inference(rat,[],[s981,s7532,s7519]) ).
cnf(s7588,plain,
~ spl18_612,
inference(rat,[],[s7427,s7587]) ).
cnf(s7599,plain,
spl18_177,
inference(rat,[],[s1849,s7587,s750]) ).
cnf(s7602,plain,
spl18_279,
inference(rat,[],[s6919,s7587,s7599]) ).
cnf(s7607,plain,
spl18_260,
inference(rat,[],[s7360,s7602]) ).
cnf(s7610,plain,
~ spl18_246,
inference(rat,[],[s6904,s7588,s7607]) ).
cnf(s7613,plain,
spl18_247,
inference(rat,[],[s7516,s7610]) ).
cnf(s7615,plain,
~ spl18_513,
inference(rat,[],[s6901,s7613]) ).
cnf(s7616,plain,
~ spl18_511,
inference(rat,[],[s6860,s2333,s7502,s7613]) ).
cnf(s7617,plain,
$false,
inference(rat,[],[s4161,s7615,s7616,s7613]) ).
fof(f31705,plain,
$false,
inference(avatar_sat_refutation,[],[s7617]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR005+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.24/0.27 % Computer : n002.cluster.edu
% 0.24/0.27 % Model : x86_64 x86_64
% 0.24/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.24/0.27 % Memory : 8046.5625MB
% 0.24/0.27 % OS : Linux 6.8.0-71-generic
% 0.24/0.27 % CPULimit : 300
% 0.24/0.27 % WCLimit : 300
% 0.24/0.27 % DateTime : Mon Sep 28 22:07:52 UTC 2026
% 0.24/0.28 % CPUTime :
% 0.24/0.28 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.24/0.32 Running first-order model finding
% 0.24/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.91/3.71 % (827229)Will run a generic schedule for satisfiability detection.
% 23.91/3.71 % (827237)dis+10_1_sil=32000:sp=arity:random_seed=2413080021:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 23.91/3.71 % (827235)% WARNING: option uhcvi not known.
% 23.91/3.71 % (827238)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2333398425:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 23.91/3.71 % (827234)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2934423862_2999 on theBenchmark for (2999ds/0Mi)
% 23.91/3.71 % (827236)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3897397379:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 23.91/3.71 % (827239)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1321027183:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 23.91/3.71 % (827235)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4109412519:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 23.91/3.71 % (827240)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3231011049:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 23.91/3.71 % Detected minimum model sizes of [3]
% 23.91/3.71 % Detected maximum model sizes of [max]
% 23.91/3.71 % TRYING [3]
% 23.91/3.71 % TRYING [4]
% 23.91/3.71 % (827237)Instruction limit reached!
% 23.91/3.71 % (827237)------------------------------
% 23.91/3.71 % (827237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.91/3.71 % (827237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.91/3.71 % (827237)CaDiCaL version: 2.1.3
% 23.91/3.71 % (827237)Termination reason: Instruction limit
% 23.91/3.71 % (827237)Termination phase: Saturation
% 23.91/3.71 % (827237)Time elapsed: 0.057 s
% 23.91/3.71 % (827237)Peak memory usage: 12 MB
% 23.91/3.71 % (827237)Instructions burned: 104 (million)
% 23.91/3.71 % TRYING [5]
% 23.91/3.71 % (827248)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3748193246:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 23.91/3.71 % Detected minimum model sizes of [3]
% 23.91/3.71 % Detected maximum model sizes of [max]
% 23.91/3.71 % TRYING [3]
% 23.91/3.71 % TRYING [4]
% 23.91/3.71 % TRYING [5]
% 23.91/3.71 % (827238)Instruction limit reached!
% 23.91/3.71 % (827238)------------------------------
% 23.91/3.71 % (827238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.91/3.71 % (827238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.91/3.71 % (827238)CaDiCaL version: 2.1.3
% 23.91/3.71 % (827238)Termination reason: Instruction limit
% 23.91/3.71 % (827238)Termination phase: Saturation
% 23.91/3.71 % (827238)Time elapsed: 0.119 s
% 23.91/3.71 % (827238)Peak memory usage: 13 MB
% 23.91/3.71 % (827238)Instructions burned: 116 (million)
% 23.91/3.71 % TRYING [6]
% 23.91/3.71 % (827239)Instruction limit reached!
% 23.91/3.71 % (827239)------------------------------
% 23.91/3.71 % (827239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.91/3.71 % (827239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.91/3.71 % (827239)CaDiCaL version: 2.1.3
% 23.91/3.71 % (827239)Termination reason: Instruction limit
% 23.91/3.71 % (827239)Termination phase: Saturation
% 23.91/3.71 % (827239)Time elapsed: 0.135 s
% 23.91/3.71 % (827239)Peak memory usage: 13 MB
% 23.91/3.71 % (827239)Instructions burned: 131 (million)
% 23.91/3.71 % (827250)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=613606150:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 23.91/3.71 % (827240)Instruction limit reached!
% 23.91/3.71 % (827240)------------------------------
% 23.91/3.71 % (827240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.91/3.71 % (827240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.91/3.71 % (827240)CaDiCaL version: 2.1.3
% 23.91/3.71 % (827240)Termination reason: Instruction limit
% 23.91/3.71 % (827240)Termination phase: Saturation
% 23.91/3.71 % (827240)Time elapsed: 0.151 s
% 23.91/3.71 % (827240)Peak memory usage: 12 MB
% 23.91/3.71 % (827240)Instructions burned: 160 (million)
% 23.91/3.71 % TRYING [6]
% 23.91/3.71 % (827251)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1556535469:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 23.91/3.71 % (827253)ott-21_1_sil=16000:fs=off:random_seed=3714908266:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 23.91/3.71 % (827250)Instruction limit reached!
% 23.91/3.71 % (827250)------------------------------
% 75.03/10.90 % (827250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.03/10.90 % (827250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.03/10.90 % (827250)CaDiCaL version: 2.1.3
% 75.03/10.90 % (827250)Termination reason: Instruction limit
% 75.03/10.90 % (827250)Termination phase: Saturation
% 75.03/10.90 % (827250)Time elapsed: 0.142 s
% 75.03/10.90 % (827250)Peak memory usage: 13 MB
% 75.03/10.90 % (827250)Instructions burned: 131 (million)
% 75.03/10.90 % TRYING [7]
% 75.03/10.90 % TRYING [7]
% 75.03/10.90 % (827256)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2892882587:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 75.03/10.90 % (827248)Instruction limit reached!
% 75.03/10.90 % (827248)------------------------------
% 75.03/10.90 % (827248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.03/10.90 % (827248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.03/10.90 % (827248)CaDiCaL version: 2.1.3
% 75.03/10.90 % (827248)Termination reason: Instruction limit
% 75.03/10.90 % (827248)Termination phase: Finite model building constraint generation
% 75.03/10.90 % (827248)Time elapsed: 0.291 s
% 75.03/10.90 % (827248)Peak memory usage: 28 MB
% 75.03/10.90 % (827248)Instructions burned: 716 (million)
% 75.03/10.90 % (827253)Instruction limit reached!
% 75.03/10.90 % (827253)------------------------------
% 75.03/10.90 % (827253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.03/10.90 % (827253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.03/10.90 % (827253)CaDiCaL version: 2.1.3
% 75.03/10.90 % (827253)Termination reason: Instruction limit
% 75.03/10.90 % (827253)Termination phase: Saturation
% 75.03/10.90 % (827253)Time elapsed: 0.172 s
% 75.03/10.90 % (827253)Peak memory usage: 12 MB
% 75.03/10.90 % (827253)Instructions burned: 180 (million)
% 75.03/10.90 % (827259)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3017551150:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 75.03/10.90 % (827258)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2206180619:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 75.03/10.90 % Detected minimum model sizes of [3]
% 75.03/10.90 % Detected maximum model sizes of [max]
% 75.03/10.90 % TRYING [3]
% 75.03/10.90 % TRYING [4]
% 75.03/10.90 % TRYING [5]
% 75.03/10.90 % TRYING [8]
% 75.03/10.90 % TRYING [6]
% 75.03/10.90 % (827251)Instruction limit reached!
% 75.03/10.90 % (827251)------------------------------
% 75.03/10.90 % (827251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.03/10.90 % (827251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.03/10.90 % (827251)CaDiCaL version: 2.1.3
% 75.03/10.90 % (827251)Termination reason: Instruction limit
% 75.03/10.90 % (827251)Termination phase: Saturation
% 75.03/10.90 % (827251)Time elapsed: 0.618 s
% 75.03/10.90 % (827251)Peak memory usage: 15 MB
% 75.03/10.90 % (827251)Instructions burned: 685 (million)
% 75.03/10.90 % (827264)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=245235625:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 75.03/10.90 % (827256)Instruction limit reached!
% 75.03/10.90 % (827256)------------------------------
% 75.03/10.90 % (827256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.03/10.90 % (827256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.03/10.90 % (827256)CaDiCaL version: 2.1.3
% 75.03/10.90 % (827256)Termination reason: Instruction limit
% 75.03/10.90 % (827256)Termination phase: Saturation
% 75.03/10.90 % (827256)Time elapsed: 0.505 s
% 75.03/10.90 % (827256)Peak memory usage: 13 MB
% 75.03/10.90 % (827256)Instructions burned: 477 (million)
% 75.03/10.90 % (827266)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2086008467:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 75.03/10.90 % (827259)Instruction limit reached!
% 75.03/10.90 % (827259)------------------------------
% 75.03/10.90 % (827259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 75.03/10.90 % (827259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.03/10.90 % (827259)CaDiCaL version: 2.1.3
% 75.03/10.90 % (827259)Termination reason: Instruction limit
% 75.03/10.90 % (827259)Termination phase: Saturation
% 75.03/10.90 % (827259)Time elapsed: 0.583 s
% 75.03/10.90 % (827259)Peak memory usage: 18 MB
% 75.03/10.90 % (827259)Instructions burned: 1181 (million)
% 75.03/10.90 % (827258)Instruction limit reached!
% 75.03/10.90 % (827258)------------------------------
% 75.03/10.90 % (827258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.48/13.59 % (827258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.48/13.59 % (827258)CaDiCaL version: 2.1.3
% 93.48/13.59 % (827258)Termination reason: Instruction limit
% 93.48/13.59 % (827258)Termination phase: Finite model building SAT solving
% 93.48/13.59 % (827258)Time elapsed: 0.614 s
% 93.48/13.59 % (827258)Peak memory usage: 26 MB
% 93.48/13.59 % (827258)Instructions burned: 866 (million)
% 93.48/13.59 % (827268)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3835789649:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 93.48/13.59 % (827270)fmb+10_1_sil=64000:random_seed=26113790:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 93.48/13.59 % Detected minimum model sizes of [3]
% 93.48/13.59 % Detected maximum model sizes of [max]
% 93.48/13.59 % TRYING [3]
% 93.48/13.59 % TRYING [4]
% 93.48/13.59 % TRYING [14]
% 93.48/13.59 % TRYING [5]
% 93.48/13.59 % TRYING [9]
% 93.48/13.59 % TRYING [6]
% 93.48/13.59 % TRYING [7]
% 93.48/13.59 % (827266)Instruction limit reached!
% 93.48/13.59 % (827266)------------------------------
% 93.48/13.59 % (827266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.48/13.59 % (827266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.48/13.59 % (827266)CaDiCaL version: 2.1.3
% 93.48/13.59 % (827266)Termination reason: Instruction limit
% 93.48/13.59 % (827266)Termination phase: Saturation
% 93.48/13.59 % (827266)Time elapsed: 0.509 s
% 93.48/13.59 % (827266)Peak memory usage: 14 MB
% 93.48/13.59 % (827266)Instructions burned: 693 (million)
% 93.48/13.59 % (827274)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2587324272:i=9515:nm=5_2985 on theBenchmark for (2985ds/9515Mi)
% 93.48/13.59 % Detected minimum model sizes of [3]
% 93.48/13.59 % Detected maximum model sizes of [max]
% 93.48/13.59 % TRYING [20]
% 93.48/13.59 % (827264)Instruction limit reached!
% 93.48/13.59 % (827264)------------------------------
% 93.48/13.59 % (827264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.48/13.59 % (827264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.48/13.59 % (827264)CaDiCaL version: 2.1.3
% 93.48/13.59 % (827264)Termination reason: Instruction limit
% 93.48/13.59 % (827264)Termination phase: Finite model building constraint generation
% 93.48/13.59 % (827264)Time elapsed: 0.691 s
% 93.48/13.59 % (827264)Peak memory usage: 79 MB
% 93.48/13.59 % (827264)Instructions burned: 889 (million)
% 93.48/13.59 % (827276)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2993673097:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 93.48/13.59 % Detected minimum model sizes of [3]
% 93.48/13.59 % Detected maximum model sizes of [max]
% 93.48/13.59 % TRYING [8]
% 93.48/13.59 % TRYING [8]
% 93.48/13.59 % (827268)Instruction limit reached!
% 93.48/13.59 % (827268)------------------------------
% 93.48/13.59 % (827268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.48/13.59 % (827268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.48/13.59 % (827268)CaDiCaL version: 2.1.3
% 93.48/13.59 % (827268)Termination reason: Instruction limit
% 93.48/13.59 % (827268)Termination phase: Saturation
% 93.48/13.59 % (827268)Time elapsed: 0.822 s
% 93.48/13.59 % (827268)Peak memory usage: 19 MB
% 93.48/13.59 % (827268)Instructions burned: 879 (million)
% 93.48/13.59 % (827278)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1537537801:i=5131_2981 on theBenchmark for (2981ds/5131Mi)
% 93.48/13.59 % TRYING [10]
% 93.48/13.59 % TRYING [9]
% 93.48/13.59 % (827276)Instruction limit reached!
% 93.48/13.59 % (827276)------------------------------
% 93.48/13.59 % (827276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.48/13.59 % (827276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.48/13.59 % (827276)CaDiCaL version: 2.1.3
% 93.48/13.59 % (827276)Termination reason: Instruction limit
% 93.48/13.59 % (827276)Termination phase: Finite model building constraint generation
% 93.48/13.59 % (827276)Time elapsed: 0.655 s
% 93.48/13.59 % (827276)Peak memory usage: 53 MB
% 93.48/13.59 % (827276)Instructions burned: 921 (million)
% 93.48/13.59 % (827280)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=297900885:i=1472:ins=7:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/1472Mi)
% 93.48/13.59 % TRYING [9]
% 93.48/13.59 % TRYING [10]
% 93.48/13.59 % (827280)Instruction limit reached!
% 93.48/13.59 % (827280)------------------------------
% 93.48/13.59 % (827280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.48/13.59 % (827280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.48/13.59 % (827280)CaDiCaL version: 2.1.3
% 93.48/13.59 % (827280)Termination reason: Instruction limit
% 93.48/13.59 % (827280)Termination phase: Saturation
% 93.48/13.59 % (827280)Time elapsed: 1.095 s
% 93.48/13.59 % (827280)Peak memory usage: 26 MB
% 93.48/13.59 % (827280)Instructions burned: 1472 (million)
% 93.48/13.59 % (827283)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3898918210:i=6324_2966 on theBenchmark for (2966ds/6324Mi)
% 93.48/13.59 % TRYING [11]
% 93.48/13.59 % Detected minimum model sizes of [3]
% 93.48/13.59 % Detected maximum model sizes of [max]
% 93.48/13.59 % TRYING [77]
% 93.48/13.59 % TRYING [11]
% 93.48/13.59 % TRYING [12]
% 93.48/13.59 % (827278)Instruction limit reached!
% 93.48/13.59 % (827278)------------------------------
% 93.48/13.59 % (827278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.48/13.59 % (827278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.48/13.59 % (827278)CaDiCaL version: 2.1.3
% 93.48/13.59 % (827278)Termination reason: Instruction limit
% 93.48/13.59 % (827278)Termination phase: Saturation
% 93.48/13.59 % (827278)Time elapsed: 4.417 s
% 93.48/13.59 % (827278)Peak memory usage: 24 MB
% 93.48/13.59 % (827278)Instructions burned: 5132 (million)
% 93.48/13.59 % (827287)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=908219482:fmbsr=2.30978:i=2174_2936 on theBenchmark for (2936ds/2174Mi)
% 93.48/13.59 % Detected minimum model sizes of [3]
% 93.48/13.59 % Detected maximum model sizes of [max]
% 93.48/13.59 % TRYING [16]
% 93.48/13.59 % TRYING [12]
% 93.48/13.59 % (827287)Instruction limit reached!
% 93.48/13.59 % (827287)------------------------------
% 93.48/13.59 % (827287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.48/13.59 % (827287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.48/13.59 % (827287)CaDiCaL version: 2.1.3
% 93.48/13.59 % (827287)Termination reason: Instruction limit
% 93.48/13.59 % (827287)Termination phase: Finite model building constraint generation
% 93.48/13.59 % (827287)Time elapsed: 1.515 s
% 93.48/13.59 % (827287)Peak memory usage: 134 MB
% 93.48/13.59 % (827287)Instructions burned: 2175 (million)
% 93.48/13.59 % (827289)ott-2_1_sil=16000:newcnf=on:random_seed=1174243275:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2921 on theBenchmark for (2921ds/869Mi)
% 93.48/13.59 % (827283)Instruction limit reached!
% 93.48/13.59 % (827283)------------------------------
% 93.48/13.59 % (827283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.48/13.59 % (827283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.48/13.59 % (827283)CaDiCaL version: 2.1.3
% 93.48/13.59 % (827283)Termination reason: Instruction limit
% 93.48/13.59 % (827283)Termination phase: Finite model building constraint generation
% 93.48/13.59 % (827283)Time elapsed: 4.622 s
% 93.48/13.59 % (827283)Peak memory usage: 516 MB
% 93.48/13.59 % (827283)Instructions burned: 6324 (million)
% 93.48/13.59 % (827291)ott+10_1_sil=32000:tgt=ground:random_seed=132912114:i=5114:av=off_2918 on theBenchmark for (2918ds/5114Mi)
% 93.48/13.59 % (827274)Instruction limit reached!
% 93.48/13.59 % (827274)------------------------------
% 93.48/13.59 % (827274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.48/13.59 % (827274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.48/13.59 % (827274)CaDiCaL version: 2.1.3
% 93.48/13.59 % (827274)Termination reason: Instruction limit
% 93.48/13.59 % (827274)Termination phase: Finite model building constraint generation
% 93.48/13.59 % (827274)Time elapsed: 6.717 s
% 93.48/13.59 % (827274)Peak memory usage: 611 MB
% 93.48/13.59 % (827274)Instructions burned: 9515 (million)
% 93.48/13.59 % (827293)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3307310231:i=54282_2916 on theBenchmark for (2916ds/54282Mi)
% 93.48/13.59 % Detected minimum model sizes of [3]
% 93.48/13.59 % Detected maximum model sizes of [max]
% 93.48/13.59 % TRYING [3]
% 93.48/13.59 % TRYING [4]
% 93.48/13.59 % TRYING [5]
% 93.48/13.59 % TRYING [6]
% 93.48/13.59 % TRYING [7]
% 93.48/13.59 % (827289)Instruction limit reached!
% 93.48/13.59 % (827289)------------------------------
% 93.48/13.59 % (827289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.48/13.59 % (827289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.48/13.59 % (827289)CaDiCaL version: 2.1.3
% 93.48/13.59 % (827289)Termination reason: Instruction limit
% 93.48/13.59 % (827289)Termination phase: Saturation
% 93.48/13.59 % (827289)Time elapsed: 0.658 s
% 93.48/13.59 % (827289)Peak memory usage: 15 MB
% 93.48/13.59 % (827289)Instructions burned: 870 (million)
% 93.48/13.59 % (827295)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=123142233:i=3512:aac=none_2914 on theBenchmark for (2914ds/3512Mi)
% 93.48/13.59 % TRYING [8]
% 93.48/13.59 % TRYING [9]
% 93.48/13.59 % TRYING [13]
% 93.48/13.59 % TRYING [10]
% 93.48/13.59 % (827270)Instruction limit reached!
% 93.48/13.59 % (827270)------------------------------
% 93.48/13.59 % (827270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.48/13.59 % (827270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.48/13.59 % (827270)CaDiCaL version: 2.1.3
% 93.48/13.59 % (827270)Termination reason: Instruction limit
% 93.48/13.59 % (827270)Termination phase: Finite model building SAT solving
% 93.48/13.59 % (827270)Time elapsed: 9.513 s
% 93.48/13.59 % (827270)Peak memory usage: 232 MB
% 93.48/13.59 % (827270)Instructions burned: 22063 (million)
% 93.48/13.59 % (827299)dis+21_1_sil=32000:sas=cadical:random_seed=3166685742:i=3773:amm=off_2893 on theBenchmark for (2893ds/3773Mi)
% 93.48/13.59 % TRYING [11]
% 93.48/13.59 % (827295)Instruction limit reached!
% 93.48/13.59 % (827295)------------------------------
% 93.48/13.59 % (827295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.48/13.59 % (827295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.48/13.59 % (827295)CaDiCaL version: 2.1.3
% 93.48/13.59 % (827295)Termination reason: Instruction limit
% 93.48/13.59 % (827295)Termination phase: Saturation
% 93.48/13.59 % (827295)Time elapsed: 3.145 s
% 93.48/13.59 % (827295)Peak memory usage: 26 MB
% 93.48/13.59 % (827295)Instructions burned: 3513 (million)
% 93.48/13.59 % (827303)ott+11_1_sil=16000:gs=on:random_seed=2970288832:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2882 on theBenchmark for (2882ds/2251Mi)
% 93.48/13.59 % (827299)Instruction limit reached!
% 93.48/13.59 % (827299)------------------------------
% 93.48/13.59 % (827299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.48/13.59 % (827299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.48/13.59 % (827299)CaDiCaL version: 2.1.3
% 93.48/13.59 % (827299)Termination reason: Instruction limit
% 93.48/13.59 % (827299)Termination phase: Saturation
% 93.48/13.59 % (827299)Time elapsed: 1.655 s
% 93.48/13.59 % (827299)Peak memory usage: 25 MB
% 93.48/13.59 % (827299)Instructions burned: 3773 (million)
% 93.48/13.59 % (827309)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1429321155:fmbsr=1.6:i=67534_2877 on theBenchmark for (2877ds/67534Mi)
% 93.48/13.59 % Detected minimum model sizes of [3]
% 93.48/13.59 % Detected maximum model sizes of [max]
% 93.48/13.59 % TRYING [7]
% 93.48/13.59 % (827291)Instruction limit reached!
% 93.48/13.59 % (827291)------------------------------
% 93.48/13.59 % (827291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.48/13.59 % (827291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.48/13.59 % (827291)CaDiCaL version: 2.1.3
% 93.48/13.59 % (827291)Termination reason: Instruction limit
% 93.48/13.59 % (827291)Termination phase: Saturation
% 93.48/13.59 % (827291)Time elapsed: 4.170 s
% 93.48/13.59 % (827291)Peak memory usage: 23 MB
% 93.48/13.59 % (827291)Instructions burned: 5115 (million)
% 93.48/13.59 % (827311)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3433482821:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2876 on theBenchmark for (2876ds/4591Mi)
% 93.48/13.59 % TRYING [8]
% 93.48/13.59 % (827303) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-827229-827303"...
% 93.48/13.59 % TRYING [12]
% 93.48/13.59 % (827303)...printing done.
% 93.48/13.59 % (827303)Refutation found. Thanks to Tanya!
% 93.48/13.59 % SZS status Theorem for theBenchmark
% 93.48/13.59 % SZS output start Proof for theBenchmark
% See solution above
% 93.48/13.59 % (827303)------------------------------
% 93.48/13.59 % (827303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.48/13.59 % (827303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.48/13.59 % (827303)CaDiCaL version: 2.1.3
% 93.48/13.59 % (827303)Termination reason: Refutation
% 93.48/13.59 % (827303)Time elapsed: 1.411 s
% 93.48/13.59 % (827303)Peak memory usage: 28 MB
% 93.48/13.59 % (827303)Instructions burned: 1938 (million)
% 93.48/13.59 % (827229)Success in time 13.257 s
% 93.48/13.59 % Vampire exiting
%------------------------------------------------------------------------------