%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR004+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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:18 AM UTC 2026
% Result : Theorem 194.57s 27.90s
% Output : Refutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 54
% Syntax : Number of formulae : 400 ( 68 unt; 25 def)
% Number of atoms : 1174 ( 212 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 1260 ( 486 ~; 631 |; 97 &)
% ( 36 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 24 prp; 0-4 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-3 aty)
% Number of variables : 388 ( 0 sgn 366 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( stoppedIn(X0,X1,X2)
<=> ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',stoppedin_defn) ).
fof(f3,axiom,
! [X0,X1,X2,X3,X4] :
( ( happens(X0,X1)
& initiates(X0,X2,X1)
& less(n0,X4)
& trajectory(X2,X1,X3,X4)
& ~ stoppedIn(X1,X2,plus(X1,X4)) )
=> holdsAt(X3,plus(X1,X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',change_holding) ).
fof(f5,axiom,
! [X0,X1] :
( ( holdsAt(X0,X1)
& ~ releasedAt(X0,plus(X1,n1))
& ~ ? [X2] :
( happens(X2,X1)
& terminates(X2,X0,X1) ) )
=> holdsAt(X0,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',keep_holding) ).
fof(f8,axiom,
! [X0,X1] :
( ( ~ releasedAt(X0,X1)
& ~ ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) )
=> ~ releasedAt(X0,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',keep_not_released) ).
fof(f9,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& initiates(X0,X2,X1) )
=> holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_holds) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& terminates(X0,X2,X1) )
=> ~ holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_terminates_not_holds) ).
fof(f11,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& releases(X0,X2,X1) )
=> releasedAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_releases) ).
fof(f12,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& ( initiates(X0,X2,X1)
| terminates(X0,X2,X1) ) )
=> ~ releasedAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_not_released) ).
fof(f13,axiom,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = overflow
& X1 = waterLevel(X3) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',initiates_all_defn) ).
fof(f15,axiom,
! [X0,X1,X2] :
( releases(X0,X1,X2)
<=> ? [X3] :
( X0 = tapOn
& X1 = waterLevel(X3) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',releases_all_defn) ).
fof(f16,axiom,
! [X0,X1] :
( happens(X0,X1)
<=> ( ( X0 = tapOn
& X1 = n0 )
| ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',happens_all_defn) ).
fof(f17,axiom,
! [X0,X1,X2,X3] :
( ( holdsAt(waterLevel(X0),X1)
& X2 = plus(X0,X3) )
=> trajectory(filling,X1,waterLevel(X2),X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',change_of_waterLevel) ).
fof(f18,axiom,
! [X0,X1,X2] :
( ( holdsAt(waterLevel(X1),X0)
& holdsAt(waterLevel(X2),X0) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',same_waterLevel) ).
fof(f21,axiom,
overflow != tapOn,
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',overflow_not_tapOn) ).
fof(f27,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus0_1) ).
fof(f28,axiom,
plus(n0,n2) = n2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus0_2) ).
fof(f29,axiom,
plus(n0,n3) = n3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus0_3) ).
fof(f30,axiom,
plus(n1,n1) = n2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus1_1) ).
fof(f31,axiom,
plus(n1,n2) = n3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus1_2) ).
fof(f36,axiom,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_of_plus) ).
fof(f37,axiom,
! [X0,X1] :
( less_or_equal(X0,X1)
<=> ( less(X0,X1)
| X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_or_equal) ).
fof(f38,axiom,
~ ? [X0] : less(X0,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less0) ).
fof(f39,axiom,
! [X0] :
( less(X0,n1)
<=> less_or_equal(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less1) ).
fof(f40,axiom,
! [X0] :
( less(X0,n2)
<=> less_or_equal(X0,n1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less2) ).
fof(f41,axiom,
! [X0] :
( less(X0,n3)
<=> less_or_equal(X0,n2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less3) ).
fof(f48,axiom,
! [X0,X1] :
( less(X0,X1)
<=> ( ~ less(X1,X0)
& X1 != X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_property) ).
fof(f49,axiom,
holdsAt(waterLevel(n0),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',waterLevel_0) ).
fof(f52,axiom,
! [X0] : ~ releasedAt(waterLevel(X0),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_released_waterLevel_0) ).
fof(f55,conjecture,
happens(overflow,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',overflow_3) ).
fof(f56,negated_conjecture,
~ happens(overflow,n3),
inference(negated_conjecture,[status(cth)],[f55]) ).
fof(f57,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) )
| ? [X4] :
( holdsAt(waterLevel(X4),X2)
& X0 = overflow
& waterLevel(X4) = X1 ) ) ),
inference(rectify,[],[f13]) ).
fof(f58,plain,
~ happens(overflow,n3),
inference(flattening,[],[f56]) ).
fof(f60,plain,
! [X0,X1,X2] :
( stoppedIn(X0,X1,X2)
=> ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) ) ),
inference(unused_predicate_definition_removal,[],[f1]) ).
fof(f63,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) )
| ~ stoppedIn(X0,X1,X2) ),
inference(ennf_transformation,[],[f60]) ).
fof(f64,plain,
! [X0,X1,X2,X3,X4] :
( holdsAt(X3,plus(X1,X4))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1)
| ~ less(n0,X4)
| ~ trajectory(X2,X1,X3,X4)
| stoppedIn(X1,X2,plus(X1,X4)) ),
inference(ennf_transformation,[],[f3]) ).
fof(f65,plain,
! [X0,X1,X2,X3,X4] :
( holdsAt(X3,plus(X1,X4))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1)
| ~ less(n0,X4)
| ~ trajectory(X2,X1,X3,X4)
| stoppedIn(X1,X2,plus(X1,X4)) ),
inference(flattening,[],[f64]) ).
fof(f66,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ? [X2] :
( happens(X2,X1)
& terminates(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f67,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ? [X2] :
( happens(X2,X1)
& terminates(X2,X0,X1) ) ),
inference(flattening,[],[f66]) ).
fof(f72,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f73,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(flattening,[],[f72]) ).
fof(f74,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f75,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(flattening,[],[f74]) ).
fof(f76,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(flattening,[],[f76]) ).
fof(f78,plain,
! [X0,X1,X2] :
( releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ releases(X0,X2,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f79,plain,
! [X0,X1,X2] :
( releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ releases(X0,X2,X1) ),
inference(flattening,[],[f78]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(flattening,[],[f80]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(ennf_transformation,[],[f17]) ).
fof(f83,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(flattening,[],[f82]) ).
fof(f84,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f85,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(flattening,[],[f84]) ).
fof(f86,plain,
! [X0] : ~ less(X0,n0),
inference(ennf_transformation,[],[f38]) ).
fof(f87,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,[],[f57,f88,f87]) ).
fof(f90,plain,
! [X0,X1,X2] :
( ( happens(sK2(X0,X1,X2),sK3(X0,X1,X2))
& less(X0,sK3(X0,X1,X2))
& less(sK3(X0,X1,X2),X2)
& terminates(sK2(X0,X1,X2),X1,sK3(X0,X1,X2)) )
| ~ stoppedIn(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X3,sK2(X0,X1,X2)),skolemize(X4,sK3(X0,X1,X2))],[f63]) ).
fof(f91,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ( happens(sK4(X0,X1),X1)
& terminates(sK4(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X2,sK4(X0,X1))],[f67]) ).
fof(f94,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))],[f73]) ).
fof(f101,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(f102,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,[],[f101]) ).
fof(f105,plain,
! [X0,X1,X2] :
( ( releases(X0,X1,X2)
| ! [X3] :
( tapOn != X0
| waterLevel(X3) != X1 ) )
& ( ? [X3] :
( X0 = tapOn
& X1 = waterLevel(X3) )
| ~ releases(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f15]) ).
fof(f106,plain,
! [X0,X1,X2] :
( ( releases(X0,X1,X2)
| ! [X3] :
( tapOn != X0
| waterLevel(X3) != X1 ) )
& ( ? [X4] :
( X0 = tapOn
& waterLevel(X4) = X1 )
| ~ releases(X0,X1,X2) ) ),
inference(rectify,[],[f105]) ).
fof(f107,plain,
! [X0,X1,X2] :
( ( releases(X0,X1,X2)
| ! [X3] :
( tapOn != X0
| waterLevel(X3) != X1 ) )
& ( ( X0 = tapOn
& waterLevel(sK10(X0,X1)) = X1 )
| ~ releases(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X4,sK10(X0,X1))],[f106]) ).
fof(f108,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(f109,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,[],[f108]) ).
fof(f111,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(f112,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,[],[f111]) ).
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] :
( ( less(X0,n2)
| ~ less_or_equal(X0,n1) )
& ( less_or_equal(X0,n1)
| ~ less(X0,n2) ) ),
inference(nnf_transformation,[],[f40]) ).
fof(f115,plain,
! [X0] :
( ( less(X0,n3)
| ~ less_or_equal(X0,n2) )
& ( less_or_equal(X0,n2)
| ~ less(X0,n3) ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f122,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(nnf_transformation,[],[f48]) ).
fof(f123,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(flattening,[],[f122]) ).
fof(f124,plain,
! [X2,X0,X1] :
( terminates(sK2(X0,X1,X2),X1,sK3(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f90]) ).
fof(f125,plain,
! [X2,X0,X1] :
( less(sK3(X0,X1,X2),X2)
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f90]) ).
fof(f127,plain,
! [X2,X0,X1] :
( happens(sK2(X0,X1,X2),sK3(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f90]) ).
fof(f128,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,[],[f65]) ).
fof(f130,plain,
! [X0,X1] :
( releasedAt(X0,plus(X1,n1))
| happens(sK4(X0,X1),X1)
| ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f91]) ).
fof(f135,plain,
! [X0,X1] :
( releases(sK7(X0,X1),X0,X1)
| releasedAt(X0,X1)
| ~ releasedAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f94]) ).
fof(f136,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| happens(sK7(X0,X1),X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f137,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f75]) ).
fof(f138,plain,
! [X2,X0,X1] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(cnf_transformation,[],[f77]) ).
fof(f139,plain,
! [X2,X0,X1] :
( ~ releases(X0,X2,X1)
| ~ happens(X0,X1)
| releasedAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f141,plain,
! [X2,X0,X1] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(cnf_transformation,[],[f81]) ).
fof(f157,plain,
! [X2,X0,X1] :
( initiates(X0,X1,X2)
| tapOn != X0
| filling != X1 ),
inference(cnf_transformation,[],[f102]) ).
fof(f165,plain,
! [X2,X0,X1] :
( ~ releases(X0,X1,X2)
| tapOn = X0 ),
inference(cnf_transformation,[],[f107]) ).
fof(f166,plain,
! [X2,X3,X0,X1] :
( releases(X0,X1,X2)
| tapOn != X0
| waterLevel(X3) != X1 ),
inference(cnf_transformation,[],[f107]) ).
fof(f167,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| overflow = X0
| n0 = X1 ),
inference(cnf_transformation,[],[f109]) ).
fof(f169,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| holdsAt(waterLevel(n3),X1)
| n0 = X1 ),
inference(cnf_transformation,[],[f109]) ).
fof(f173,plain,
! [X0,X1] :
( happens(X0,X1)
| ~ holdsAt(waterLevel(n3),X1)
| ~ holdsAt(filling,X1)
| overflow != X0 ),
inference(cnf_transformation,[],[f109]) ).
fof(f174,plain,
! [X0,X1] :
( happens(X0,X1)
| tapOn != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f109]) ).
fof(f175,plain,
! [X2,X3,X0,X1] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(cnf_transformation,[],[f83]) ).
fof(f176,plain,
! [X2,X0,X1] :
( ~ holdsAt(waterLevel(X2),X0)
| ~ holdsAt(waterLevel(X1),X0)
| X1 = X2 ),
inference(cnf_transformation,[],[f85]) ).
fof(f179,plain,
tapOn != overflow,
inference(cnf_transformation,[],[f21]) ).
fof(f186,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f27]) ).
fof(f187,plain,
n2 = plus(n0,n2),
inference(cnf_transformation,[],[f28]) ).
fof(f188,plain,
n3 = plus(n0,n3),
inference(cnf_transformation,[],[f29]) ).
fof(f189,plain,
n2 = plus(n1,n1),
inference(cnf_transformation,[],[f30]) ).
fof(f190,plain,
n3 = plus(n1,n2),
inference(cnf_transformation,[],[f31]) ).
fof(f195,plain,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[],[f36]) ).
fof(f196,plain,
! [X0,X1] :
( ~ less_or_equal(X0,X1)
| X0 = X1
| less(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f197,plain,
! [X0,X1] :
( less_or_equal(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f112]) ).
fof(f198,plain,
! [X0,X1] :
( ~ less(X0,X1)
| less_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f199,plain,
! [X0] : ~ less(X0,n0),
inference(cnf_transformation,[],[f86]) ).
fof(f200,plain,
! [X0] :
( ~ less(X0,n1)
| less_or_equal(X0,n0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f201,plain,
! [X0] :
( ~ less_or_equal(X0,n0)
| less(X0,n1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f202,plain,
! [X0] :
( ~ less(X0,n2)
| less_or_equal(X0,n1) ),
inference(cnf_transformation,[],[f114]) ).
fof(f203,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| less(X0,n2) ),
inference(cnf_transformation,[],[f114]) ).
fof(f204,plain,
! [X0] :
( ~ less(X0,n3)
| less_or_equal(X0,n2) ),
inference(cnf_transformation,[],[f115]) ).
fof(f205,plain,
! [X0] :
( ~ less_or_equal(X0,n2)
| less(X0,n3) ),
inference(cnf_transformation,[],[f115]) ).
fof(f218,plain,
! [X0,X1] :
( X0 != X1
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f123]) ).
fof(f219,plain,
! [X0,X1] :
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f123]) ).
fof(f220,plain,
! [X0,X1] :
( less(X1,X0)
| less(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f123]) ).
fof(f221,plain,
holdsAt(waterLevel(n0),n0),
inference(cnf_transformation,[],[f49]) ).
fof(f224,plain,
! [X0] : ~ releasedAt(waterLevel(X0),n0),
inference(cnf_transformation,[],[f52]) ).
fof(f227,plain,
~ happens(overflow,n3),
inference(cnf_transformation,[],[f58]) ).
fof(f232,plain,
! [X2,X1] :
( initiates(tapOn,X1,X2)
| filling != X1 ),
inference(equality_resolution,[],[f157]) ).
fof(f233,plain,
! [X2] : initiates(tapOn,filling,X2),
inference(equality_resolution,[],[f232]) ).
fof(f240,plain,
! [X2,X3,X1] :
( releases(tapOn,X1,X2)
| waterLevel(X3) != X1 ),
inference(equality_resolution,[],[f166]) ).
fof(f241,plain,
! [X2,X3] : releases(tapOn,waterLevel(X3),X2),
inference(equality_resolution,[],[f240]) ).
fof(f242,plain,
! [X1] :
( happens(tapOn,X1)
| n0 != X1 ),
inference(equality_resolution,[],[f174]) ).
fof(f243,plain,
happens(tapOn,n0),
inference(equality_resolution,[],[f242]) ).
fof(f244,plain,
! [X1] :
( ~ holdsAt(waterLevel(n3),X1)
| happens(overflow,X1)
| ~ holdsAt(filling,X1) ),
inference(equality_resolution,[],[f173]) ).
fof(f245,plain,
! [X3,X0,X1] :
( trajectory(filling,X1,waterLevel(plus(X0,X3)),X3)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(equality_resolution,[],[f175]) ).
fof(f247,plain,
! [X1] : less_or_equal(X1,X1),
inference(equality_resolution,[],[f197]) ).
fof(f248,plain,
! [X1] : ~ less(X1,X1),
inference(equality_resolution,[],[f218]) ).
fof(f323,plain,
! [X0,X1] :
( ~ initiates(X1,X0,n0)
| ~ happens(X1,n0)
| ~ releasedAt(X0,n1) ),
inference(superposition,[],[f141,f186]) ).
fof(f358,plain,
less(n0,n1),
inference(resolution,[],[f201,f247]) ).
fof(f367,plain,
less_or_equal(n0,n1),
inference(resolution,[],[f358,f198]) ).
fof(f388,plain,
less(n1,n2),
inference(resolution,[],[f203,f247]) ).
fof(f389,plain,
less(n0,n2),
inference(resolution,[],[f203,f367]) ).
fof(f401,plain,
~ less(n2,n1),
inference(resolution,[],[f388,f219]) ).
fof(f403,plain,
less_or_equal(n0,n2),
inference(resolution,[],[f389,f198]) ).
fof(f426,plain,
less(n2,n3),
inference(resolution,[],[f205,f247]) ).
fof(f427,plain,
less(n0,n3),
inference(resolution,[],[f205,f403]) ).
fof(f5215,plain,
! [X0] :
( less_or_equal(X0,n0)
| n1 = X0
| less(n1,X0) ),
inference(resolution,[],[f220,f200]) ).
fof(f5217,plain,
! [X0] :
( less_or_equal(X0,n1)
| n2 = X0
| less(n2,X0) ),
inference(resolution,[],[f220,f202]) ).
fof(f5405,plain,
! [X0] :
( n1 = X0
| less(n1,X0)
| n0 = X0
| less(X0,n0) ),
inference(resolution,[],[f5215,f196]) ).
fof(f5406,plain,
! [X0] :
( less(n1,X0)
| n1 = X0
| n0 = X0 ),
inference(forward_subsumption_resolution,[],[f5405,f199]) ).
fof(f6734,plain,
! [X0] :
( less(n2,X0)
| less(X0,n1)
| n1 = X0
| n2 = X0 ),
inference(resolution,[],[f5217,f196]) ).
fof(f8626,plain,
! [X0] :
( ~ less(X0,n1)
| n0 = X0
| n1 = X0 ),
inference(resolution,[],[f5406,f219]) ).
fof(f11067,plain,
! [X0,X1] :
( less_or_equal(sK3(X0,X1,n1),n0)
| ~ stoppedIn(X0,X1,n1) ),
inference(resolution,[],[f125,f200]) ).
fof(f11071,plain,
! [X0,X1] :
( less_or_equal(sK3(X0,X1,n3),n2)
| ~ stoppedIn(X0,X1,n3) ),
inference(resolution,[],[f125,f204]) ).
fof(f11075,plain,
! [X0,X1] :
( less_or_equal(sK3(X0,X1,n2),n1)
| ~ stoppedIn(X0,X1,n2) ),
inference(resolution,[],[f125,f202]) ).
fof(f13788,definition,
( spl11_133
<=> holdsAt(filling,n1) ),
introduced(definition,[new_symbols(definition,[spl11_133])],[avatar_definition]) ).
fof(f13789,plain,
( holdsAt(filling,n1)
| ~ spl11_133 ),
inference(avatar_component_clause,[],[f13788]) ).
fof(f13790,plain,
( ~ holdsAt(filling,n1)
| spl11_133 ),
inference(avatar_component_clause,[],[f13788]) ).
fof(f13824,plain,
! [X0] :
( holdsAt(filling,plus(X0,n1))
| ~ happens(tapOn,X0) ),
inference(resolution,[],[f137,f233]) ).
fof(f13836,plain,
! [X0,X1] :
( ~ terminates(X1,filling,X0)
| ~ happens(X1,X0)
| ~ happens(tapOn,X0) ),
inference(resolution,[],[f13824,f138]) ).
fof(f13840,plain,
( holdsAt(filling,n1)
| ~ happens(tapOn,n0) ),
inference(superposition,[],[f13824,f186]) ).
fof(f13842,plain,
( ~ happens(tapOn,n0)
| spl11_133 ),
inference(forward_subsumption_resolution,[],[f13840,f13790]) ).
fof(f13843,plain,
( $false
| spl11_133 ),
inference(forward_subsumption_resolution,[],[f13842,f243]) ).
fof(f13844,plain,
spl11_133,
inference(avatar_contradiction_clause,[],[f13843]) ).
fof(f13902,plain,
( ~ happens(tapOn,n0)
| ~ releasedAt(filling,n1) ),
inference(resolution,[],[f323,f233]) ).
fof(f13908,plain,
~ releasedAt(filling,n1),
inference(forward_subsumption_resolution,[],[f13902,f243]) ).
fof(f13948,plain,
! [X0,X1] :
( releasedAt(waterLevel(X1),plus(X0,n1))
| ~ happens(tapOn,X0) ),
inference(resolution,[],[f139,f241]) ).
fof(f13980,plain,
! [X0] :
( releasedAt(waterLevel(X0),n1)
| ~ happens(tapOn,n0) ),
inference(superposition,[],[f13948,f186]) ).
fof(f13982,plain,
! [X0] : releasedAt(waterLevel(X0),n1),
inference(forward_subsumption_resolution,[],[f13980,f243]) ).
fof(f14039,plain,
! [X0] :
( trajectory(filling,X0,waterLevel(n1),n1)
| ~ holdsAt(waterLevel(n0),X0) ),
inference(superposition,[],[f245,f186]) ).
fof(f14040,plain,
! [X0] :
( trajectory(filling,X0,waterLevel(n3),n3)
| ~ holdsAt(waterLevel(n0),X0) ),
inference(superposition,[],[f245,f188]) ).
fof(f14041,plain,
! [X0] :
( trajectory(filling,X0,waterLevel(n2),n2)
| ~ holdsAt(waterLevel(n0),X0) ),
inference(superposition,[],[f245,f187]) ).
fof(f14200,plain,
! [X0] :
( less(n2,X0)
| n1 = X0
| n2 = X0
| n0 = X0
| n1 = X0 ),
inference(resolution,[],[f6734,f8626]) ).
fof(f14253,plain,
! [X0] :
( less(n2,X0)
| n1 = X0
| n2 = X0
| n0 = X0 ),
inference(duplicate_literal_removal,[],[f14200]) ).
fof(f15722,plain,
! [X0] :
( ~ less(X0,n2)
| n2 = X0
| n0 = X0
| n1 = X0 ),
inference(resolution,[],[f14253,f219]) ).
fof(f16134,definition,
( spl11_159
<=> holdsAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl11_159])],[avatar_definition]) ).
fof(f16135,plain,
( holdsAt(filling,n2)
| ~ spl11_159 ),
inference(avatar_component_clause,[],[f16134]) ).
fof(f16136,plain,
( ~ holdsAt(filling,n2)
| spl11_159 ),
inference(avatar_component_clause,[],[f16134]) ).
fof(f16144,definition,
( spl11_161
<=> holdsAt(filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_161])],[avatar_definition]) ).
fof(f16145,plain,
( holdsAt(filling,n3)
| ~ spl11_161 ),
inference(avatar_component_clause,[],[f16144]) ).
fof(f16146,plain,
( ~ holdsAt(filling,n3)
| spl11_161 ),
inference(avatar_component_clause,[],[f16144]) ).
fof(f16405,definition,
( spl11_166
<=> n0 = n1 ),
introduced(definition,[new_symbols(definition,[spl11_166])],[avatar_definition]) ).
fof(f16406,plain,
( n0 != n1
| spl11_166 ),
inference(avatar_component_clause,[],[f16405]) ).
fof(f16407,plain,
( n0 = n1
| ~ spl11_166 ),
inference(avatar_component_clause,[],[f16405]) ).
fof(f16409,definition,
( spl11_167
<=> holdsAt(waterLevel(n3),n1) ),
introduced(definition,[new_symbols(definition,[spl11_167])],[avatar_definition]) ).
fof(f16410,plain,
( ~ holdsAt(waterLevel(n3),n1)
| spl11_167 ),
inference(avatar_component_clause,[],[f16409]) ).
fof(f16411,plain,
( holdsAt(waterLevel(n3),n1)
| ~ spl11_167 ),
inference(avatar_component_clause,[],[f16409]) ).
fof(f16422,plain,
( ! [X0] : ~ releasedAt(waterLevel(X0),n1)
| ~ spl11_166 ),
inference(superposition,[],[f224,f16407]) ).
fof(f16472,plain,
( $false
| ~ spl11_166 ),
inference(forward_subsumption_resolution,[],[f16422,f13982]) ).
fof(f16473,plain,
~ spl11_166,
inference(avatar_contradiction_clause,[],[f16472]) ).
fof(f16555,plain,
! [X0,X1] :
( ~ releasedAt(X1,plus(n1,X0))
| releasedAt(X1,X0)
| happens(sK7(X1,X0),X0) ),
inference(superposition,[],[f136,f195]) ).
fof(f16558,plain,
! [X0] :
( happens(sK7(X0,n1),n1)
| releasedAt(X0,n1)
| ~ releasedAt(X0,n2) ),
inference(superposition,[],[f136,f189]) ).
fof(f16801,definition,
( spl11_181
<=> releasedAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl11_181])],[avatar_definition]) ).
fof(f16802,plain,
( releasedAt(filling,n2)
| ~ spl11_181 ),
inference(avatar_component_clause,[],[f16801]) ).
fof(f16803,plain,
( ~ releasedAt(filling,n2)
| spl11_181 ),
inference(avatar_component_clause,[],[f16801]) ).
fof(f16805,definition,
( spl11_182
<=> happens(tapOn,n1) ),
introduced(definition,[new_symbols(definition,[spl11_182])],[avatar_definition]) ).
fof(f16806,plain,
( happens(tapOn,n1)
| ~ spl11_182 ),
inference(avatar_component_clause,[],[f16805]) ).
fof(f16807,plain,
( ~ happens(tapOn,n1)
| spl11_182 ),
inference(avatar_component_clause,[],[f16805]) ).
fof(f17201,definition,
( spl11_189
<=> n0 = n2 ),
introduced(definition,[new_symbols(definition,[spl11_189])],[avatar_definition]) ).
fof(f17202,plain,
( n0 != n2
| spl11_189 ),
inference(avatar_component_clause,[],[f17201]) ).
fof(f17203,plain,
( n0 = n2
| ~ spl11_189 ),
inference(avatar_component_clause,[],[f17201]) ).
fof(f17206,definition,
( spl11_190
<=> holdsAt(waterLevel(n3),n2) ),
introduced(definition,[new_symbols(definition,[spl11_190])],[avatar_definition]) ).
fof(f17207,plain,
( ~ holdsAt(waterLevel(n3),n2)
| spl11_190 ),
inference(avatar_component_clause,[],[f17206]) ).
fof(f17208,plain,
( holdsAt(waterLevel(n3),n2)
| ~ spl11_190 ),
inference(avatar_component_clause,[],[f17206]) ).
fof(f17216,plain,
( less(n1,n0)
| ~ spl11_189 ),
inference(superposition,[],[f388,f17203]) ).
fof(f17317,plain,
( $false
| ~ spl11_189 ),
inference(forward_subsumption_resolution,[],[f17216,f199]) ).
fof(f17318,plain,
~ spl11_189,
inference(avatar_contradiction_clause,[],[f17317]) ).
fof(f17335,definition,
( spl11_191
<=> releasedAt(filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_191])],[avatar_definition]) ).
fof(f17336,plain,
( releasedAt(filling,n3)
| ~ spl11_191 ),
inference(avatar_component_clause,[],[f17335]) ).
fof(f17337,plain,
( ~ releasedAt(filling,n3)
| spl11_191 ),
inference(avatar_component_clause,[],[f17335]) ).
fof(f17369,definition,
( spl11_196
<=> holdsAt(waterLevel(n3),n3) ),
introduced(definition,[new_symbols(definition,[spl11_196])],[avatar_definition]) ).
fof(f17370,plain,
( ~ holdsAt(waterLevel(n3),n3)
| spl11_196 ),
inference(avatar_component_clause,[],[f17369]) ).
fof(f17371,plain,
( holdsAt(waterLevel(n3),n3)
| ~ spl11_196 ),
inference(avatar_component_clause,[],[f17369]) ).
fof(f17486,plain,
( happens(overflow,n3)
| ~ holdsAt(filling,n3)
| ~ spl11_196 ),
inference(resolution,[],[f17371,f244]) ).
fof(f17490,plain,
( ~ holdsAt(filling,n3)
| ~ spl11_196 ),
inference(forward_subsumption_resolution,[],[f17486,f227]) ).
fof(f17491,plain,
( $false
| ~ spl11_161
| ~ spl11_196 ),
inference(forward_subsumption_resolution,[],[f17490,f16145]) ).
fof(f17492,plain,
( ~ spl11_161
| ~ spl11_196 ),
inference(avatar_contradiction_clause,[],[f17491]) ).
fof(f17528,plain,
! [X0] :
( happens(sK7(X0,n2),n2)
| releasedAt(X0,n2)
| ~ releasedAt(X0,n3) ),
inference(superposition,[],[f16555,f190]) ).
fof(f17631,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| tapOn = sK7(X0,X1) ),
inference(resolution,[],[f135,f165]) ).
fof(f17705,plain,
! [X0] :
( ~ releasedAt(X0,n2)
| releasedAt(X0,n1)
| tapOn = sK7(X0,n1) ),
inference(superposition,[],[f17631,f189]) ).
fof(f17897,plain,
! [X0,X1] :
( releasedAt(X1,plus(n1,X0))
| happens(sK4(X1,X0),X0)
| ~ holdsAt(X1,X0)
| holdsAt(X1,plus(n1,X0)) ),
inference(superposition,[],[f130,f195]) ).
fof(f17900,plain,
! [X0] :
( happens(sK4(X0,n1),n1)
| releasedAt(X0,n2)
| ~ holdsAt(X0,n1)
| holdsAt(X0,n2) ),
inference(superposition,[],[f130,f189]) ).
fof(f18044,plain,
( tapOn = overflow
| n0 = n1
| ~ spl11_182 ),
inference(resolution,[],[f16806,f167]) ).
fof(f18051,plain,
( n0 = n1
| ~ spl11_182 ),
inference(forward_subsumption_resolution,[],[f18044,f179]) ).
fof(f18054,plain,
( $false
| spl11_166
| ~ spl11_182 ),
inference(forward_subsumption_resolution,[],[f18051,f16406]) ).
fof(f18055,plain,
( spl11_166
| ~ spl11_182 ),
inference(avatar_contradiction_clause,[],[f18054]) ).
fof(f18086,plain,
! [X0] :
( releasedAt(X0,n2)
| ~ holdsAt(X0,n1)
| holdsAt(X0,n2)
| holdsAt(waterLevel(n3),n1)
| n0 = n1 ),
inference(resolution,[],[f17900,f169]) ).
fof(f18109,definition,
( spl11_218
<=> ! [X0] :
( ~ releasedAt(X0,n3)
| releasedAt(X0,n2) ) ),
introduced(definition,[new_symbols(definition,[spl11_218])],[avatar_definition]) ).
fof(f18110,plain,
( ! [X0] :
( ~ releasedAt(X0,n3)
| releasedAt(X0,n2) )
| ~ spl11_218 ),
inference(avatar_component_clause,[],[f18109]) ).
fof(f18347,plain,
( ! [X0] :
( releasedAt(X0,n2)
| ~ holdsAt(X0,n1)
| holdsAt(X0,n2)
| holdsAt(waterLevel(n3),n1) )
| spl11_166 ),
inference(forward_subsumption_resolution,[],[f18086,f16406]) ).
fof(f18436,plain,
! [X0] :
( ~ releasedAt(X0,n2)
| releasedAt(X0,n1)
| tapOn = sK7(X0,n1) ),
inference(global_subsumption,[],[f17705]) ).
fof(f18440,plain,
( releasedAt(filling,n1)
| tapOn = sK7(filling,n1)
| ~ spl11_181 ),
inference(resolution,[],[f18436,f16802]) ).
fof(f18442,plain,
( tapOn = sK7(filling,n1)
| ~ spl11_181 ),
inference(forward_subsumption_resolution,[],[f18440,f13908]) ).
fof(f18443,plain,
( happens(tapOn,n1)
| releasedAt(filling,n1)
| ~ releasedAt(filling,n2)
| ~ spl11_181 ),
inference(superposition,[],[f16558,f18442]) ).
fof(f18446,plain,
( releasedAt(filling,n1)
| ~ releasedAt(filling,n2)
| ~ spl11_181
| spl11_182 ),
inference(forward_subsumption_resolution,[],[f18443,f16807]) ).
fof(f18448,plain,
( ~ releasedAt(filling,n2)
| ~ spl11_181
| spl11_182 ),
inference(forward_subsumption_resolution,[],[f18446,f13908]) ).
fof(f18450,plain,
( $false
| ~ spl11_181
| spl11_182 ),
inference(forward_subsumption_resolution,[],[f18448,f16802]) ).
fof(f18451,plain,
( ~ spl11_181
| spl11_182 ),
inference(avatar_contradiction_clause,[],[f18450]) ).
fof(f18530,plain,
! [X0] :
( releasedAt(X0,n2)
| ~ releasedAt(X0,n3)
| holdsAt(waterLevel(n3),n2)
| n0 = n2 ),
inference(resolution,[],[f17528,f169]) ).
fof(f18535,plain,
( ! [X0] :
( releasedAt(X0,n2)
| ~ releasedAt(X0,n3)
| n0 = n2 )
| spl11_190 ),
inference(forward_subsumption_resolution,[],[f18530,f17207]) ).
fof(f18537,plain,
( ! [X0] :
( releasedAt(X0,n2)
| ~ releasedAt(X0,n3) )
| spl11_189
| spl11_190 ),
inference(forward_subsumption_resolution,[],[f18535,f17202]) ).
fof(f18538,plain,
( spl11_218
| spl11_189
| spl11_190 ),
inference(avatar_split_clause,[],[f18537,f17206,f17201,f18109]) ).
fof(f18550,plain,
( releasedAt(filling,n2)
| ~ spl11_191
| ~ spl11_218 ),
inference(resolution,[],[f18110,f17336]) ).
fof(f18553,plain,
( $false
| spl11_181
| ~ spl11_191
| ~ spl11_218 ),
inference(forward_subsumption_resolution,[],[f18550,f16803]) ).
fof(f18554,plain,
( spl11_181
| ~ spl11_191
| ~ spl11_218 ),
inference(avatar_contradiction_clause,[],[f18553]) ).
fof(f18642,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n2)
| n3 = X0 )
| ~ spl11_190 ),
inference(resolution,[],[f17208,f176]) ).
fof(f18870,plain,
( ! [X0] :
( ~ holdsAt(X0,n1)
| releasedAt(X0,n2)
| holdsAt(X0,n2) )
| spl11_166
| spl11_167 ),
inference(forward_subsumption_resolution,[],[f18347,f16410]) ).
fof(f18871,plain,
( releasedAt(filling,n2)
| holdsAt(filling,n2)
| ~ spl11_133
| spl11_166
| spl11_167 ),
inference(resolution,[],[f18870,f13789]) ).
fof(f18875,plain,
( holdsAt(filling,n2)
| ~ spl11_133
| spl11_166
| spl11_167
| spl11_181 ),
inference(forward_subsumption_resolution,[],[f18871,f16803]) ).
fof(f18876,plain,
( $false
| ~ spl11_133
| spl11_159
| spl11_166
| spl11_167
| spl11_181 ),
inference(forward_subsumption_resolution,[],[f18875,f16136]) ).
fof(f18877,plain,
( ~ spl11_133
| spl11_159
| spl11_166
| spl11_167
| spl11_181 ),
inference(avatar_contradiction_clause,[],[f18876]) ).
fof(f18903,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n1)
| n3 = X0 )
| ~ spl11_167 ),
inference(resolution,[],[f16411,f176]) ).
fof(f24228,plain,
! [X0] :
( happens(sK4(X0,n2),n2)
| releasedAt(X0,n3)
| ~ holdsAt(X0,n2)
| holdsAt(X0,n3) ),
inference(superposition,[],[f17897,f190]) ).
fof(f24442,plain,
! [X0] :
( releasedAt(X0,n3)
| ~ holdsAt(X0,n2)
| holdsAt(X0,n3)
| holdsAt(waterLevel(n3),n2)
| n0 = n2 ),
inference(resolution,[],[f24228,f169]) ).
fof(f49567,plain,
! [X2,X0,X1] :
( holdsAt(waterLevel(n3),sK3(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2)
| n0 = sK3(X0,X1,X2) ),
inference(resolution,[],[f127,f169]) ).
fof(f49882,plain,
! [X0,X1] :
( ~ stoppedIn(X0,X1,n3)
| n2 = sK3(X0,X1,n3)
| less(sK3(X0,X1,n3),n2) ),
inference(resolution,[],[f11071,f196]) ).
fof(f49906,plain,
! [X0,X1] :
( ~ stoppedIn(X0,X1,n2)
| n1 = sK3(X0,X1,n2)
| less(sK3(X0,X1,n2),n1) ),
inference(resolution,[],[f11075,f196]) ).
fof(f52497,plain,
! [X0,X1] :
( ~ stoppedIn(X0,filling,X1)
| ~ happens(sK2(X0,filling,X1),sK3(X0,filling,X1))
| ~ happens(tapOn,sK3(X0,filling,X1)) ),
inference(resolution,[],[f124,f13836]) ).
fof(f52518,plain,
! [X0,X1] :
( ~ happens(tapOn,sK3(X0,filling,X1))
| ~ stoppedIn(X0,filling,X1) ),
inference(forward_subsumption_resolution,[],[f52497,f127]) ).
fof(f77780,definition,
( spl11_743
<=> n3 = n2 ),
introduced(definition,[new_symbols(definition,[spl11_743])],[avatar_definition]) ).
fof(f77781,plain,
( n3 != n2
| spl11_743 ),
inference(avatar_component_clause,[],[f77780]) ).
fof(f77782,plain,
( n3 = n2
| ~ spl11_743 ),
inference(avatar_component_clause,[],[f77780]) ).
fof(f77795,plain,
( less(n3,n3)
| ~ spl11_743 ),
inference(superposition,[],[f426,f77782]) ).
fof(f77981,plain,
( $false
| ~ spl11_743 ),
inference(forward_subsumption_resolution,[],[f77795,f248]) ).
fof(f77982,plain,
~ spl11_743,
inference(avatar_contradiction_clause,[],[f77981]) ).
fof(f79043,plain,
! [X0,X1] :
( ~ stoppedIn(X0,X1,n1)
| n0 = sK3(X0,X1,n1)
| less(sK3(X0,X1,n1),n0) ),
inference(resolution,[],[f11067,f196]) ).
fof(f79044,plain,
! [X0,X1] :
( ~ stoppedIn(X0,X1,n1)
| n0 = sK3(X0,X1,n1) ),
inference(forward_subsumption_resolution,[],[f79043,f199]) ).
fof(f80981,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| ~ initiates(X0,filling,X1)
| ~ less(n0,n1)
| holdsAt(waterLevel(n1),plus(X1,n1))
| stoppedIn(X1,filling,plus(X1,n1))
| ~ holdsAt(waterLevel(n0),X1) ),
inference(resolution,[],[f128,f14039]) ).
fof(f80988,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| ~ initiates(X0,filling,X1)
| ~ less(n0,n3)
| holdsAt(waterLevel(n3),plus(X1,n3))
| stoppedIn(X1,filling,plus(X1,n3))
| ~ holdsAt(waterLevel(n0),X1) ),
inference(resolution,[],[f128,f14040]) ).
fof(f80994,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| ~ initiates(X0,filling,X1)
| ~ less(n0,n2)
| holdsAt(waterLevel(n2),plus(X1,n2))
| stoppedIn(X1,filling,plus(X1,n2))
| ~ holdsAt(waterLevel(n0),X1) ),
inference(resolution,[],[f128,f14041]) ).
fof(f81001,plain,
! [X0,X1] :
( ~ holdsAt(waterLevel(n0),X1)
| ~ initiates(X0,filling,X1)
| holdsAt(waterLevel(n2),plus(X1,n2))
| stoppedIn(X1,filling,plus(X1,n2))
| ~ happens(X0,X1) ),
inference(forward_subsumption_resolution,[],[f80994,f389]) ).
fof(f81008,plain,
! [X0,X1] :
( ~ holdsAt(waterLevel(n0),X1)
| ~ initiates(X0,filling,X1)
| holdsAt(waterLevel(n1),plus(X1,n1))
| stoppedIn(X1,filling,plus(X1,n1))
| ~ happens(X0,X1) ),
inference(forward_subsumption_resolution,[],[f80981,f358]) ).
fof(f90745,plain,
! [X0,X1] :
( ~ holdsAt(waterLevel(n0),X1)
| ~ initiates(X0,filling,X1)
| holdsAt(waterLevel(n3),plus(X1,n3))
| stoppedIn(X1,filling,plus(X1,n3))
| ~ happens(X0,X1) ),
inference(forward_subsumption_resolution,[],[f80988,f427]) ).
fof(f118819,definition,
( spl11_959
<=> ! [X0] :
( ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ) ),
introduced(definition,[new_symbols(definition,[spl11_959])],[avatar_definition]) ).
fof(f118820,plain,
( ! [X0] :
( ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) )
| ~ spl11_959 ),
inference(avatar_component_clause,[],[f118819]) ).
fof(f118822,definition,
( spl11_960
<=> holdsAt(waterLevel(n2),n2) ),
introduced(definition,[new_symbols(definition,[spl11_960])],[avatar_definition]) ).
fof(f118823,plain,
( ~ holdsAt(waterLevel(n2),n2)
| spl11_960 ),
inference(avatar_component_clause,[],[f118822]) ).
fof(f118824,plain,
( holdsAt(waterLevel(n2),n2)
| ~ spl11_960 ),
inference(avatar_component_clause,[],[f118822]) ).
fof(f118826,plain,
( ~ happens(tapOn,n0)
| ~ spl11_959 ),
inference(resolution,[],[f118820,f233]) ).
fof(f118830,plain,
( $false
| ~ spl11_959 ),
inference(forward_subsumption_resolution,[],[f118826,f243]) ).
fof(f118831,plain,
~ spl11_959,
inference(avatar_contradiction_clause,[],[f118830]) ).
fof(f118838,plain,
( n3 = n2
| ~ spl11_190
| ~ spl11_960 ),
inference(resolution,[],[f118824,f18642]) ).
fof(f118879,plain,
( $false
| ~ spl11_190
| spl11_743
| ~ spl11_960 ),
inference(forward_subsumption_resolution,[],[f118838,f77781]) ).
fof(f118880,plain,
( ~ spl11_190
| spl11_743
| ~ spl11_960 ),
inference(avatar_contradiction_clause,[],[f118879]) ).
fof(f121555,plain,
! [X0] :
( ~ initiates(X0,filling,n0)
| holdsAt(waterLevel(n2),plus(n0,n2))
| stoppedIn(n0,filling,plus(n0,n2))
| ~ happens(X0,n0) ),
inference(resolution,[],[f81001,f221]) ).
fof(f121588,plain,
! [X0] :
( holdsAt(waterLevel(n2),n2)
| ~ initiates(X0,filling,n0)
| stoppedIn(n0,filling,plus(n0,n2))
| ~ happens(X0,n0) ),
inference(forward_demodulation,[],[f121555,f187]) ).
fof(f121601,plain,
( ! [X0] :
( ~ initiates(X0,filling,n0)
| stoppedIn(n0,filling,plus(n0,n2))
| ~ happens(X0,n0) )
| spl11_960 ),
inference(forward_subsumption_resolution,[],[f121588,f118823]) ).
fof(f121606,plain,
( ! [X0] :
( stoppedIn(n0,filling,n2)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) )
| spl11_960 ),
inference(forward_demodulation,[],[f121601,f187]) ).
fof(f121661,plain,
! [X0,X1] :
( less(sK3(X0,X1,n2),n1)
| n1 = sK3(X0,X1,n2)
| ~ stoppedIn(X0,X1,n2) ),
inference(global_subsumption,[],[f49906]) ).
fof(f121756,definition,
( spl11_980
<=> stoppedIn(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl11_980])],[avatar_definition]) ).
fof(f121758,plain,
( stoppedIn(n0,filling,n2)
| ~ spl11_980 ),
inference(avatar_component_clause,[],[f121756]) ).
fof(f121759,plain,
( spl11_959
| spl11_980
| spl11_960 ),
inference(avatar_split_clause,[],[f121606,f118822,f121756,f118819]) ).
fof(f121781,definition,
( spl11_981
<=> n0 = sK3(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl11_981])],[avatar_definition]) ).
fof(f121782,plain,
( n0 != sK3(n0,filling,n2)
| spl11_981 ),
inference(avatar_component_clause,[],[f121781]) ).
fof(f121783,plain,
( n0 = sK3(n0,filling,n2)
| ~ spl11_981 ),
inference(avatar_component_clause,[],[f121781]) ).
fof(f121789,plain,
( ~ happens(tapOn,n0)
| ~ stoppedIn(n0,filling,n2)
| ~ spl11_981 ),
inference(superposition,[],[f52518,f121783]) ).
fof(f121865,plain,
( ~ stoppedIn(n0,filling,n2)
| ~ spl11_981 ),
inference(forward_subsumption_resolution,[],[f121789,f243]) ).
fof(f121873,plain,
( $false
| ~ spl11_980
| ~ spl11_981 ),
inference(forward_subsumption_resolution,[],[f121865,f121758]) ).
fof(f121874,plain,
( ~ spl11_980
| ~ spl11_981 ),
inference(avatar_contradiction_clause,[],[f121873]) ).
fof(f124491,plain,
! [X0] :
( ~ initiates(X0,filling,n0)
| holdsAt(waterLevel(n1),plus(n0,n1))
| stoppedIn(n0,filling,plus(n0,n1))
| ~ happens(X0,n0) ),
inference(resolution,[],[f81008,f221]) ).
fof(f124526,plain,
! [X0] :
( holdsAt(waterLevel(n1),n1)
| ~ initiates(X0,filling,n0)
| stoppedIn(n0,filling,plus(n0,n1))
| ~ happens(X0,n0) ),
inference(forward_demodulation,[],[f124491,f186]) ).
fof(f124540,plain,
! [X0] :
( stoppedIn(n0,filling,n1)
| holdsAt(waterLevel(n1),n1)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ),
inference(forward_demodulation,[],[f124526,f186]) ).
fof(f125031,definition,
( spl11_1008
<=> holdsAt(waterLevel(n1),n1) ),
introduced(definition,[new_symbols(definition,[spl11_1008])],[avatar_definition]) ).
fof(f125032,plain,
( ~ holdsAt(waterLevel(n1),n1)
| spl11_1008 ),
inference(avatar_component_clause,[],[f125031]) ).
fof(f125033,plain,
( holdsAt(waterLevel(n1),n1)
| ~ spl11_1008 ),
inference(avatar_component_clause,[],[f125031]) ).
fof(f125035,plain,
( n1 = n3
| ~ spl11_167
| ~ spl11_1008 ),
inference(resolution,[],[f125033,f18903]) ).
fof(f125570,plain,
( less(n2,n1)
| ~ spl11_167
| ~ spl11_1008 ),
inference(superposition,[],[f426,f125035]) ).
fof(f125922,plain,
( $false
| ~ spl11_167
| ~ spl11_1008 ),
inference(forward_subsumption_resolution,[],[f125570,f401]) ).
fof(f125923,plain,
( ~ spl11_167
| ~ spl11_1008 ),
inference(avatar_contradiction_clause,[],[f125922]) ).
fof(f125965,plain,
! [X0,X1] :
( ~ stoppedIn(X0,X1,n1)
| n0 = sK3(X0,X1,n1) ),
inference(global_subsumption,[],[f79044]) ).
fof(f126920,plain,
( ! [X0] :
( stoppedIn(n0,filling,n1)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) )
| spl11_1008 ),
inference(forward_subsumption_resolution,[],[f124540,f125032]) ).
fof(f126922,definition,
( spl11_1019
<=> stoppedIn(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl11_1019])],[avatar_definition]) ).
fof(f126924,plain,
( stoppedIn(n0,filling,n1)
| ~ spl11_1019 ),
inference(avatar_component_clause,[],[f126922]) ).
fof(f126925,plain,
( spl11_959
| spl11_1019
| spl11_1008 ),
inference(avatar_split_clause,[],[f126920,f125031,f126922,f118819]) ).
fof(f126926,plain,
( n0 = sK3(n0,filling,n1)
| ~ spl11_1019 ),
inference(resolution,[],[f126924,f125965]) ).
fof(f126931,plain,
( ~ happens(tapOn,n0)
| ~ stoppedIn(n0,filling,n1)
| ~ spl11_1019 ),
inference(superposition,[],[f52518,f126926]) ).
fof(f127008,plain,
( ~ stoppedIn(n0,filling,n1)
| ~ spl11_1019 ),
inference(forward_subsumption_resolution,[],[f126931,f243]) ).
fof(f127016,plain,
( $false
| ~ spl11_1019 ),
inference(forward_subsumption_resolution,[],[f127008,f126924]) ).
fof(f127017,plain,
~ spl11_1019,
inference(avatar_contradiction_clause,[],[f127016]) ).
fof(f127018,plain,
( ! [X0] :
( releasedAt(X0,n3)
| ~ holdsAt(X0,n2)
| holdsAt(X0,n3)
| holdsAt(waterLevel(n3),n2) )
| spl11_189 ),
inference(forward_subsumption_resolution,[],[f24442,f17202]) ).
fof(f135747,plain,
! [X0,X1] :
( n1 = sK3(X0,X1,n2)
| ~ stoppedIn(X0,X1,n2)
| n0 = sK3(X0,X1,n2)
| n1 = sK3(X0,X1,n2) ),
inference(resolution,[],[f121661,f8626]) ).
fof(f135764,plain,
! [X0,X1] :
( ~ stoppedIn(X0,X1,n2)
| n1 = sK3(X0,X1,n2)
| n0 = sK3(X0,X1,n2) ),
inference(duplicate_literal_removal,[],[f135747]) ).
fof(f136167,plain,
( n1 = sK3(n0,filling,n2)
| n0 = sK3(n0,filling,n2)
| ~ spl11_980 ),
inference(resolution,[],[f135764,f121758]) ).
fof(f136168,plain,
( n1 = sK3(n0,filling,n2)
| ~ spl11_980
| spl11_981 ),
inference(forward_subsumption_resolution,[],[f136167,f121782]) ).
fof(f136219,plain,
( holdsAt(waterLevel(n3),n1)
| ~ stoppedIn(n0,filling,n2)
| n0 = n1
| ~ spl11_980
| spl11_981 ),
inference(superposition,[],[f49567,f136168]) ).
fof(f136238,plain,
( ~ stoppedIn(n0,filling,n2)
| n0 = n1
| spl11_167
| ~ spl11_980
| spl11_981 ),
inference(forward_subsumption_resolution,[],[f136219,f16410]) ).
fof(f136252,plain,
( n0 = n1
| spl11_167
| ~ spl11_980
| spl11_981 ),
inference(forward_subsumption_resolution,[],[f136238,f121758]) ).
fof(f136262,plain,
( $false
| spl11_166
| spl11_167
| ~ spl11_980
| spl11_981 ),
inference(forward_subsumption_resolution,[],[f136252,f16406]) ).
fof(f136263,plain,
( spl11_166
| spl11_167
| ~ spl11_980
| spl11_981 ),
inference(avatar_contradiction_clause,[],[f136262]) ).
fof(f162857,plain,
! [X0] :
( ~ initiates(X0,filling,n0)
| holdsAt(waterLevel(n3),plus(n0,n3))
| stoppedIn(n0,filling,plus(n0,n3))
| ~ happens(X0,n0) ),
inference(resolution,[],[f90745,f221]) ).
fof(f162892,plain,
! [X0] :
( holdsAt(waterLevel(n3),n3)
| ~ initiates(X0,filling,n0)
| stoppedIn(n0,filling,plus(n0,n3))
| ~ happens(X0,n0) ),
inference(forward_demodulation,[],[f162857,f188]) ).
fof(f162943,plain,
( ! [X0] :
( ~ initiates(X0,filling,n0)
| stoppedIn(n0,filling,plus(n0,n3))
| ~ happens(X0,n0) )
| spl11_196 ),
inference(forward_subsumption_resolution,[],[f162892,f17370]) ).
fof(f162947,plain,
( ! [X0] :
( stoppedIn(n0,filling,n3)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) )
| spl11_196 ),
inference(forward_demodulation,[],[f162943,f188]) ).
fof(f163114,plain,
! [X0,X1] :
( less(sK3(X0,X1,n3),n2)
| n2 = sK3(X0,X1,n3)
| ~ stoppedIn(X0,X1,n3) ),
inference(global_subsumption,[],[f49882]) ).
fof(f163116,definition,
( spl11_1161
<=> stoppedIn(n0,filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_1161])],[avatar_definition]) ).
fof(f163118,plain,
( stoppedIn(n0,filling,n3)
| ~ spl11_1161 ),
inference(avatar_component_clause,[],[f163116]) ).
fof(f163119,plain,
( spl11_959
| spl11_1161
| spl11_196 ),
inference(avatar_split_clause,[],[f162947,f17369,f163116,f118819]) ).
fof(f163126,definition,
( spl11_1162
<=> n0 = sK3(n0,filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_1162])],[avatar_definition]) ).
fof(f163127,plain,
( n0 != sK3(n0,filling,n3)
| spl11_1162 ),
inference(avatar_component_clause,[],[f163126]) ).
fof(f163128,plain,
( n0 = sK3(n0,filling,n3)
| ~ spl11_1162 ),
inference(avatar_component_clause,[],[f163126]) ).
fof(f163136,plain,
( ~ happens(tapOn,n0)
| ~ stoppedIn(n0,filling,n3)
| ~ spl11_1162 ),
inference(superposition,[],[f52518,f163128]) ).
fof(f163190,plain,
( ~ stoppedIn(n0,filling,n3)
| ~ spl11_1162 ),
inference(forward_subsumption_resolution,[],[f163136,f243]) ).
fof(f163198,plain,
( $false
| ~ spl11_1161
| ~ spl11_1162 ),
inference(forward_subsumption_resolution,[],[f163190,f163118]) ).
fof(f163199,plain,
( ~ spl11_1161
| ~ spl11_1162 ),
inference(avatar_contradiction_clause,[],[f163198]) ).
fof(f163385,plain,
! [X0,X1] :
( n2 = sK3(X0,X1,n3)
| ~ stoppedIn(X0,X1,n3)
| n2 = sK3(X0,X1,n3)
| n0 = sK3(X0,X1,n3)
| n1 = sK3(X0,X1,n3) ),
inference(resolution,[],[f163114,f15722]) ).
fof(f163388,plain,
! [X0,X1] :
( ~ stoppedIn(X0,X1,n3)
| n2 = sK3(X0,X1,n3)
| n0 = sK3(X0,X1,n3)
| n1 = sK3(X0,X1,n3) ),
inference(duplicate_literal_removal,[],[f163385]) ).
fof(f165143,plain,
( n2 = sK3(n0,filling,n3)
| n0 = sK3(n0,filling,n3)
| n1 = sK3(n0,filling,n3)
| ~ spl11_1161 ),
inference(resolution,[],[f163388,f163118]) ).
fof(f165144,plain,
( n2 = sK3(n0,filling,n3)
| n1 = sK3(n0,filling,n3)
| ~ spl11_1161
| spl11_1162 ),
inference(forward_subsumption_resolution,[],[f165143,f163127]) ).
fof(f165146,definition,
( spl11_1183
<=> n1 = sK3(n0,filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_1183])],[avatar_definition]) ).
fof(f165148,plain,
( n1 = sK3(n0,filling,n3)
| ~ spl11_1183 ),
inference(avatar_component_clause,[],[f165146]) ).
fof(f165150,definition,
( spl11_1184
<=> n2 = sK3(n0,filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_1184])],[avatar_definition]) ).
fof(f165152,plain,
( n2 = sK3(n0,filling,n3)
| ~ spl11_1184 ),
inference(avatar_component_clause,[],[f165150]) ).
fof(f165153,plain,
( spl11_1183
| spl11_1184
| ~ spl11_1161
| spl11_1162 ),
inference(avatar_split_clause,[],[f165144,f163126,f163116,f165150,f165146]) ).
fof(f165218,plain,
( holdsAt(waterLevel(n3),n1)
| ~ stoppedIn(n0,filling,n3)
| n0 = n1
| ~ spl11_1183 ),
inference(superposition,[],[f49567,f165148]) ).
fof(f165247,plain,
( ~ stoppedIn(n0,filling,n3)
| n0 = n1
| spl11_167
| ~ spl11_1183 ),
inference(forward_subsumption_resolution,[],[f165218,f16410]) ).
fof(f165276,plain,
( n0 = n1
| spl11_167
| ~ spl11_1161
| ~ spl11_1183 ),
inference(forward_subsumption_resolution,[],[f165247,f163118]) ).
fof(f165296,plain,
( $false
| spl11_166
| spl11_167
| ~ spl11_1161
| ~ spl11_1183 ),
inference(forward_subsumption_resolution,[],[f165276,f16406]) ).
fof(f165297,plain,
( spl11_166
| spl11_167
| ~ spl11_1161
| ~ spl11_1183 ),
inference(avatar_contradiction_clause,[],[f165296]) ).
fof(f165365,plain,
( holdsAt(waterLevel(n3),n2)
| ~ stoppedIn(n0,filling,n3)
| n0 = n2
| ~ spl11_1184 ),
inference(superposition,[],[f49567,f165152]) ).
fof(f165394,plain,
( ~ stoppedIn(n0,filling,n3)
| n0 = n2
| spl11_190
| ~ spl11_1184 ),
inference(forward_subsumption_resolution,[],[f165365,f17207]) ).
fof(f165423,plain,
( n0 = n2
| spl11_190
| ~ spl11_1161
| ~ spl11_1184 ),
inference(forward_subsumption_resolution,[],[f165394,f163118]) ).
fof(f165443,plain,
( $false
| spl11_189
| spl11_190
| ~ spl11_1161
| ~ spl11_1184 ),
inference(forward_subsumption_resolution,[],[f165423,f17202]) ).
fof(f165444,plain,
( spl11_189
| spl11_190
| ~ spl11_1161
| ~ spl11_1184 ),
inference(avatar_contradiction_clause,[],[f165443]) ).
fof(f165561,plain,
( ! [X0] :
( ~ holdsAt(X0,n2)
| releasedAt(X0,n3)
| holdsAt(X0,n3) )
| spl11_189
| spl11_190 ),
inference(forward_subsumption_resolution,[],[f127018,f17207]) ).
fof(f166985,plain,
( releasedAt(filling,n3)
| holdsAt(filling,n3)
| ~ spl11_159
| spl11_189
| spl11_190 ),
inference(resolution,[],[f165561,f16135]) ).
fof(f166992,plain,
( holdsAt(filling,n3)
| ~ spl11_159
| spl11_189
| spl11_190
| spl11_191 ),
inference(forward_subsumption_resolution,[],[f166985,f17337]) ).
fof(f166993,plain,
( $false
| ~ spl11_159
| spl11_161
| spl11_189
| spl11_190
| spl11_191 ),
inference(forward_subsumption_resolution,[],[f166992,f16146]) ).
fof(f166994,plain,
( ~ spl11_159
| spl11_161
| spl11_189
| spl11_190
| spl11_191 ),
inference(avatar_contradiction_clause,[],[f166993]) ).
cnf(s5194,plain,
spl11_133,
inference(sat_conversion,[],[f13844]) ).
cnf(s5740,plain,
~ spl11_166,
inference(sat_conversion,[],[f16473]) ).
cnf(s6127,plain,
~ spl11_189,
inference(sat_conversion,[],[f17318]) ).
cnf(s6219,plain,
( ~ spl11_161
| ~ spl11_196 ),
inference(sat_conversion,[],[f17492]) ).
cnf(s6597,plain,
( spl11_166
| ~ spl11_182 ),
inference(sat_conversion,[],[f18055]) ).
cnf(s6930,plain,
( ~ spl11_181
| spl11_182 ),
inference(sat_conversion,[],[f18451]) ).
cnf(s7002,plain,
( spl11_189
| spl11_190
| spl11_218 ),
inference(sat_conversion,[],[f18538]) ).
cnf(s7024,plain,
( spl11_181
| ~ spl11_191
| ~ spl11_218 ),
inference(sat_conversion,[],[f18554]) ).
cnf(s7204,plain,
( ~ spl11_133
| spl11_159
| spl11_166
| spl11_167
| spl11_181 ),
inference(sat_conversion,[],[f18877]) ).
cnf(s22067,plain,
~ spl11_743,
inference(sat_conversion,[],[f77982]) ).
cnf(s30772,plain,
~ spl11_959,
inference(sat_conversion,[],[f118831]) ).
cnf(s30778,plain,
( ~ spl11_190
| spl11_743
| ~ spl11_960 ),
inference(sat_conversion,[],[f118880]) ).
cnf(s31499,plain,
( spl11_959
| spl11_960
| spl11_980 ),
inference(sat_conversion,[],[f121759]) ).
cnf(s31532,plain,
( ~ spl11_980
| ~ spl11_981 ),
inference(sat_conversion,[],[f121874]) ).
cnf(s32595,plain,
( ~ spl11_167
| ~ spl11_1008 ),
inference(sat_conversion,[],[f125923]) ).
cnf(s32992,plain,
( spl11_959
| spl11_1008
| spl11_1019 ),
inference(sat_conversion,[],[f126925]) ).
cnf(s33013,plain,
~ spl11_1019,
inference(sat_conversion,[],[f127017]) ).
cnf(s36606,plain,
( spl11_166
| spl11_167
| ~ spl11_980
| spl11_981 ),
inference(sat_conversion,[],[f136263]) ).
cnf(s45654,plain,
( spl11_196
| spl11_959
| spl11_1161 ),
inference(sat_conversion,[],[f163119]) ).
cnf(s45668,plain,
( ~ spl11_1161
| ~ spl11_1162 ),
inference(sat_conversion,[],[f163199]) ).
cnf(s46143,plain,
( ~ spl11_1161
| spl11_1162
| spl11_1183
| spl11_1184 ),
inference(sat_conversion,[],[f165153]) ).
cnf(s46166,plain,
( spl11_166
| spl11_167
| ~ spl11_1161
| ~ spl11_1183 ),
inference(sat_conversion,[],[f165297]) ).
cnf(s46198,plain,
( spl11_189
| spl11_190
| ~ spl11_1161
| ~ spl11_1184 ),
inference(sat_conversion,[],[f165444]) ).
cnf(s46811,plain,
( ~ spl11_159
| spl11_161
| spl11_189
| spl11_190
| spl11_191 ),
inference(sat_conversion,[],[f166994]) ).
cnf(s46825,plain,
( spl11_959
| spl11_1008 ),
inference(rat,[],[s32992,s33013]) ).
cnf(s46832,plain,
spl11_1008,
inference(rat,[],[s46825,s30772]) ).
cnf(s46834,plain,
~ spl11_167,
inference(rat,[],[s32595,s46832]) ).
cnf(s46872,plain,
( ~ spl11_133
| spl11_159
| spl11_166
| spl11_181 ),
inference(rat,[],[s7204,s46834]) ).
cnf(s46964,plain,
~ spl11_182,
inference(rat,[],[s6597,s5740]) ).
cnf(s46969,plain,
~ spl11_181,
inference(rat,[],[s6930,s46964]) ).
cnf(s46980,plain,
spl11_159,
inference(rat,[],[s46872,s46969,s5740,s5194]) ).
cnf(s47012,plain,
( spl11_190
| spl11_161 ),
inference(rat,[],[s7024,s46811,s7002,s46969,s6127,s46980]) ).
cnf(s47013,plain,
~ spl11_980,
inference(rat,[],[s36606,s31532,s46834,s5740]) ).
cnf(s47014,plain,
spl11_960,
inference(rat,[],[s31499,s30772,s47013]) ).
cnf(s47018,plain,
~ spl11_190,
inference(rat,[],[s30778,s22067,s47014]) ).
cnf(s47034,plain,
spl11_161,
inference(rat,[],[s47012,s47018]) ).
cnf(s47046,plain,
~ spl11_196,
inference(rat,[],[s6219,s47034]) ).
cnf(s47050,plain,
spl11_1161,
inference(rat,[],[s45654,s30772,s47046]) ).
cnf(s47059,plain,
~ spl11_1162,
inference(rat,[],[s45668,s47050]) ).
cnf(s47060,plain,
~ spl11_1183,
inference(rat,[],[s46166,s5740,s46834,s47050]) ).
cnf(s47061,plain,
~ spl11_1184,
inference(rat,[],[s46198,s47018,s6127,s47050]) ).
cnf(s47066,plain,
$false,
inference(rat,[],[s46143,s47061,s47050,s47060,s47059]) ).
fof(f166995,plain,
$false,
inference(avatar_sat_refutation,[],[s47066]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR004+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 22:04:49 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.12 Running first-order model finding
% 0.09/0.12 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.12/1.39 % (3839465)Will run a generic schedule for satisfiability detection.
% 8.12/1.39 % (3839478)% WARNING: option uhcvi not known.
% 8.12/1.39 % (3839478)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4264645281:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.12/1.39 % (3839482)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3382462477:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.12/1.39 % (3839480)dis+10_1_sil=32000:sp=arity:random_seed=3751271680:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.12/1.39 % (3839481)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3093402326:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.12/1.39 % (3839477)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2783659006_2999 on theBenchmark for (2999ds/0Mi)
% 8.12/1.39 % (3839479)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4117043267:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.12/1.39 % (3839483)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=892397447:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.12/1.39 % Detected minimum model sizes of [3]
% 8.12/1.39 % Detected maximum model sizes of [max]
% 8.12/1.39 % TRYING [3]
% 8.12/1.39 % TRYING [4]
% 8.12/1.39 % TRYING [5]
% 8.12/1.39 % (3839480)Instruction limit reached!
% 8.12/1.39 % (3839480)------------------------------
% 8.12/1.39 % (3839480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.12/1.39 % (3839480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.12/1.39 % (3839480)CaDiCaL version: 2.1.3
% 8.12/1.39 % (3839480)Termination reason: Instruction limit
% 8.12/1.39 % (3839480)Termination phase: Saturation
% 8.12/1.39 % (3839480)Time elapsed: 0.039 s
% 8.12/1.39 % (3839480)Peak memory usage: 12 MB
% 8.12/1.39 % (3839480)Instructions burned: 104 (million)
% 8.12/1.39 % TRYING [6]
% 8.12/1.39 % (3839481)Instruction limit reached!
% 8.12/1.39 % (3839481)------------------------------
% 8.12/1.39 % (3839481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.12/1.39 % (3839481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.12/1.39 % (3839481)CaDiCaL version: 2.1.3
% 8.12/1.39 % (3839481)Termination reason: Instruction limit
% 8.12/1.39 % (3839481)Termination phase: Saturation
% 8.12/1.39 % (3839481)Time elapsed: 0.040 s
% 8.12/1.39 % (3839481)Peak memory usage: 13 MB
% 8.12/1.39 % (3839481)Instructions burned: 117 (million)
% 8.12/1.39 % (3839482)Instruction limit reached!
% 8.12/1.39 % (3839482)------------------------------
% 8.12/1.39 % (3839482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.12/1.39 % (3839482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.12/1.39 % (3839482)CaDiCaL version: 2.1.3
% 8.12/1.39 % (3839482)Termination reason: Instruction limit
% 8.12/1.39 % (3839482)Termination phase: Saturation
% 8.12/1.39 % (3839482)Time elapsed: 0.043 s
% 8.12/1.39 % (3839482)Peak memory usage: 12 MB
% 8.12/1.39 % (3839482)Instructions burned: 132 (million)
% 8.12/1.39 % (3839509)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1653481417:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 8.12/1.39 % (3839483)Instruction limit reached!
% 8.12/1.39 % (3839483)------------------------------
% 8.12/1.39 % (3839483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.12/1.39 % (3839483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.12/1.39 % (3839483)CaDiCaL version: 2.1.3
% 8.12/1.39 % (3839483)Termination reason: Instruction limit
% 8.12/1.39 % (3839483)Termination phase: Saturation
% 8.12/1.39 % (3839483)Time elapsed: 0.052 s
% 8.12/1.39 % (3839483)Peak memory usage: 13 MB
% 8.12/1.39 % (3839483)Instructions burned: 161 (million)
% 8.12/1.39 % (3839510)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1779802833:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 8.12/1.39 % (3839511)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=138500532:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 8.12/1.39 % Detected minimum model sizes of [3]
% 8.12/1.39 % Detected maximum model sizes of [max]
% 8.12/1.39 % TRYING [3]
% 8.12/1.39 % TRYING [4]
% 8.12/1.39 % (3839517)ott-21_1_sil=16000:fs=off:random_seed=1376902190:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 8.12/1.39 % TRYING [5]
% 8.12/1.39 % TRYING [7]
% 8.12/1.39 % (3839510)Instruction limit reached!
% 18.36/2.85 % (3839510)------------------------------
% 18.36/2.85 % (3839510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.36/2.85 % (3839510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.36/2.85 % (3839510)CaDiCaL version: 2.1.3
% 18.36/2.85 % (3839510)Termination reason: Instruction limit
% 18.36/2.85 % (3839510)Termination phase: Saturation
% 18.36/2.85 % (3839510)Time elapsed: 0.056 s
% 18.36/2.85 % (3839510)Peak memory usage: 13 MB
% 18.36/2.85 % (3839510)Instructions burned: 133 (million)
% 18.36/2.85 % TRYING [6]
% 18.36/2.85 % (3839541)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3451513276:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 18.36/2.85 % (3839517)Instruction limit reached!
% 18.36/2.85 % (3839517)------------------------------
% 18.36/2.85 % (3839517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.36/2.85 % (3839517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.36/2.85 % (3839517)CaDiCaL version: 2.1.3
% 18.36/2.85 % (3839517)Termination reason: Instruction limit
% 18.36/2.85 % (3839517)Termination phase: Saturation
% 18.36/2.85 % (3839517)Time elapsed: 0.059 s
% 18.36/2.85 % (3839517)Peak memory usage: 13 MB
% 18.36/2.85 % (3839517)Instructions burned: 180 (million)
% 18.36/2.85 % (3839543)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3804980230:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 18.36/2.85 % Detected minimum model sizes of [3]
% 18.36/2.85 % Detected maximum model sizes of [max]
% 18.36/2.85 % TRYING [3]
% 18.36/2.85 % TRYING [4]
% 18.36/2.85 % TRYING [5]
% 18.36/2.85 % TRYING [8]
% 18.36/2.85 % TRYING [7]
% 18.36/2.85 % (3839509)Instruction limit reached!
% 18.36/2.85 % (3839509)------------------------------
% 18.36/2.85 % (3839509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.36/2.85 % (3839509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.36/2.85 % (3839509)CaDiCaL version: 2.1.3
% 18.36/2.85 % (3839509)Termination reason: Instruction limit
% 18.36/2.85 % (3839509)Termination phase: Finite model building constraint generation
% 18.36/2.85 % (3839509)Time elapsed: 0.157 s
% 18.36/2.85 % (3839509)Peak memory usage: 27 MB
% 18.36/2.85 % (3839509)Instructions burned: 716 (million)
% 18.36/2.85 % (3839548)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3906662370:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 18.36/2.85 % (3839511)Instruction limit reached!
% 18.36/2.85 % (3839511)------------------------------
% 18.36/2.85 % (3839511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.36/2.85 % (3839511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.36/2.85 % (3839511)CaDiCaL version: 2.1.3
% 18.36/2.85 % (3839511)Termination reason: Instruction limit
% 18.36/2.85 % (3839511)Termination phase: Saturation
% 18.36/2.85 % (3839511)Time elapsed: 0.179 s
% 18.36/2.85 % (3839511)Peak memory usage: 14 MB
% 18.36/2.85 % (3839511)Instructions burned: 688 (million)
% 18.36/2.85 % TRYING [6]
% 18.36/2.85 % (3839557)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1383307508:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 18.36/2.85 % (3839541)Instruction limit reached!
% 18.36/2.85 % (3839541)------------------------------
% 18.36/2.85 % (3839541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.36/2.85 % (3839541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.36/2.85 % (3839541)CaDiCaL version: 2.1.3
% 18.36/2.85 % (3839541)Termination reason: Instruction limit
% 18.36/2.85 % (3839541)Termination phase: Saturation
% 18.36/2.85 % (3839541)Time elapsed: 0.158 s
% 18.36/2.85 % (3839541)Peak memory usage: 13 MB
% 18.36/2.85 % (3839541)Instructions burned: 479 (million)
% 18.36/2.85 % (3839577)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=137689162:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 18.36/2.85 % TRYING [14]
% 18.36/2.85 % (3839543)Instruction limit reached!
% 18.36/2.85 % (3839543)------------------------------
% 18.36/2.85 % (3839543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.36/2.85 % (3839543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.36/2.85 % (3839543)CaDiCaL version: 2.1.3
% 18.36/2.85 % (3839543)Termination reason: Instruction limit
% 18.36/2.85 % (3839543)Termination phase: Finite model building SAT solving
% 18.36/2.85 % (3839543)Time elapsed: 0.183 s
% 18.36/2.85 % (3839543)Peak memory usage: 25 MB
% 18.36/2.85 % (3839543)Instructions burned: 869 (million)
% 44.08/6.41 % TRYING [9]
% 44.08/6.41 % (3839595)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1347442156:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 44.08/6.41 % (3839557)Instruction limit reached!
% 44.08/6.41 % (3839557)------------------------------
% 44.08/6.41 % (3839557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.08/6.41 % (3839557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.08/6.41 % (3839557)CaDiCaL version: 2.1.3
% 44.08/6.41 % (3839557)Termination reason: Instruction limit
% 44.08/6.41 % (3839557)Termination phase: Finite model building constraint generation
% 44.08/6.41 % (3839557)Time elapsed: 0.189 s
% 44.08/6.41 % (3839557)Peak memory usage: 79 MB
% 44.08/6.41 % (3839557)Instructions burned: 892 (million)
% 44.08/6.41 % (3839632)fmb+10_1_sil=64000:random_seed=2324295889:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 44.08/6.41 % Detected minimum model sizes of [3]
% 44.08/6.41 % Detected maximum model sizes of [max]
% 44.08/6.41 % TRYING [3]
% 44.08/6.41 % TRYING [4]
% 44.08/6.41 % TRYING [5]
% 44.08/6.41 % (3839577)Instruction limit reached!
% 44.08/6.41 % (3839577)------------------------------
% 44.08/6.41 % (3839577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.08/6.41 % (3839577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.08/6.41 % (3839577)CaDiCaL version: 2.1.3
% 44.08/6.41 % (3839577)Termination reason: Instruction limit
% 44.08/6.41 % (3839577)Termination phase: Saturation
% 44.08/6.41 % (3839577)Time elapsed: 0.204 s
% 44.08/6.41 % (3839577)Peak memory usage: 17 MB
% 44.08/6.41 % (3839577)Instructions burned: 692 (million)
% 44.08/6.41 % (3839651)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1278497098:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 44.08/6.41 % Detected minimum model sizes of [3]
% 44.08/6.41 % Detected maximum model sizes of [max]
% 44.08/6.41 % TRYING [20]
% 44.08/6.41 % TRYING [6]
% 44.08/6.41 % TRYING [10]
% 44.08/6.41 % (3839548)Instruction limit reached!
% 44.08/6.41 % (3839548)------------------------------
% 44.08/6.41 % (3839548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.08/6.41 % (3839548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.08/6.41 % (3839548)CaDiCaL version: 2.1.3
% 44.08/6.41 % (3839548)Termination reason: Instruction limit
% 44.08/6.41 % (3839548)Termination phase: Saturation
% 44.08/6.41 % (3839548)Time elapsed: 0.354 s
% 44.08/6.41 % (3839548)Peak memory usage: 19 MB
% 44.08/6.41 % (3839548)Instructions burned: 1179 (million)
% 44.08/6.41 % (3839662)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3271458708:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 44.08/6.41 % Detected minimum model sizes of [3]
% 44.08/6.41 % Detected maximum model sizes of [max]
% 44.08/6.41 % TRYING [8]
% 44.08/6.41 % (3839595)Instruction limit reached!
% 44.08/6.41 % (3839595)------------------------------
% 44.08/6.41 % (3839595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.08/6.41 % (3839595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.08/6.41 % (3839595)CaDiCaL version: 2.1.3
% 44.08/6.41 % (3839595)Termination reason: Instruction limit
% 44.08/6.41 % (3839595)Termination phase: Saturation
% 44.08/6.41 % (3839595)Time elapsed: 0.278 s
% 44.08/6.41 % (3839595)Peak memory usage: 18 MB
% 44.08/6.41 % (3839595)Instructions burned: 882 (million)
% 44.08/6.41 % TRYING [7]
% 44.08/6.41 % (3839664)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1341965412:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 44.08/6.41 % TRYING [9]
% 44.08/6.41 % (3839662)Instruction limit reached!
% 44.08/6.41 % (3839662)------------------------------
% 44.08/6.41 % (3839662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.08/6.41 % (3839662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.08/6.41 % (3839662)CaDiCaL version: 2.1.3
% 44.08/6.41 % (3839662)Termination reason: Instruction limit
% 44.08/6.41 % (3839662)Termination phase: Finite model building constraint generation
% 44.08/6.41 % (3839662)Time elapsed: 0.195 s
% 44.08/6.41 % (3839662)Peak memory usage: 53 MB
% 44.08/6.41 % (3839662)Instructions burned: 924 (million)
% 44.08/6.41 % (3839713)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3343399199:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi)
% 44.08/6.41 % TRYING [8]
% 44.08/6.41 % TRYING [11]
% 44.08/6.41 % TRYING [9]
% 44.08/6.41 % (3839713)Instruction limit reached!
% 44.08/6.41 % (3839713)------------------------------
% 44.08/6.41 % (3839713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 174.58/24.93 % (3839713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.58/24.93 % (3839713)CaDiCaL version: 2.1.3
% 174.58/24.93 % (3839713)Termination reason: Instruction limit
% 174.58/24.93 % (3839713)Termination phase: Saturation
% 174.58/24.93 % (3839713)Time elapsed: 0.438 s
% 174.58/24.93 % (3839713)Peak memory usage: 26 MB
% 174.58/24.93 % (3839713)Instructions burned: 1475 (million)
% 174.58/24.93 % (3839715)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3363286207:i=6324_2987 on theBenchmark for (2987ds/6324Mi)
% 174.58/24.93 % Detected minimum model sizes of [3]
% 174.58/24.93 % Detected maximum model sizes of [max]
% 174.58/24.93 % TRYING [77]
% 174.58/24.93 % TRYING [12]
% 174.58/24.93 % TRYING [10]
% 174.58/24.93 % (3839664)Instruction limit reached!
% 174.58/24.93 % (3839664)------------------------------
% 174.58/24.93 % (3839664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 174.58/24.93 % (3839664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.58/24.93 % (3839664)CaDiCaL version: 2.1.3
% 174.58/24.93 % (3839664)Termination reason: Instruction limit
% 174.58/24.93 % (3839664)Termination phase: Saturation
% 174.58/24.93 % (3839664)Time elapsed: 1.457 s
% 174.58/24.93 % (3839664)Peak memory usage: 24 MB
% 174.58/24.93 % (3839664)Instructions burned: 5131 (million)
% 174.58/24.93 % (3839717)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3528980921:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 174.58/24.93 % Detected minimum model sizes of [3]
% 174.58/24.93 % Detected maximum model sizes of [max]
% 174.58/24.93 % TRYING [16]
% 174.58/24.93 % (3839651)Instruction limit reached!
% 174.58/24.93 % (3839651)------------------------------
% 174.58/24.93 % (3839651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 174.58/24.93 % (3839651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.58/24.93 % (3839651)CaDiCaL version: 2.1.3
% 174.58/24.93 % (3839651)Termination reason: Instruction limit
% 174.58/24.93 % (3839651)Termination phase: Finite model building constraint generation
% 174.58/24.93 % (3839651)Time elapsed: 1.882 s
% 174.58/24.93 % (3839651)Peak memory usage: 611 MB
% 174.58/24.93 % (3839651)Instructions burned: 9516 (million)
% 174.58/24.93 % (3839719)ott-2_1_sil=16000:newcnf=on:random_seed=456081162:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2975 on theBenchmark for (2975ds/869Mi)
% 174.58/24.93 % (3839717)Instruction limit reached!
% 174.58/24.93 % (3839717)------------------------------
% 174.58/24.93 % (3839717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 174.58/24.93 % (3839717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.58/24.93 % (3839717)CaDiCaL version: 2.1.3
% 174.58/24.93 % (3839717)Termination reason: Instruction limit
% 174.58/24.93 % (3839717)Termination phase: Finite model building constraint generation
% 174.58/24.93 % (3839717)Time elapsed: 0.409 s
% 174.58/24.93 % (3839717)Peak memory usage: 134 MB
% 174.58/24.93 % (3839717)Instructions burned: 2179 (million)
% 174.58/24.93 % (3839721)ott+10_1_sil=32000:tgt=ground:random_seed=2097729423:i=5114:av=off_2974 on theBenchmark for (2974ds/5114Mi)
% 174.58/24.93 % (3839715)Instruction limit reached!
% 174.58/24.93 % (3839715)------------------------------
% 174.58/24.93 % (3839715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 174.58/24.93 % (3839715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.58/24.93 % (3839715)CaDiCaL version: 2.1.3
% 174.58/24.93 % (3839715)Termination reason: Instruction limit
% 174.58/24.93 % (3839715)Termination phase: Finite model building constraint generation
% 174.58/24.93 % (3839715)Time elapsed: 1.311 s
% 174.58/24.93 % (3839715)Peak memory usage: 516 MB
% 174.58/24.93 % (3839715)Instructions burned: 6327 (million)
% 174.58/24.93 % (3839723)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1434293973:i=54282_2973 on theBenchmark for (2973ds/54282Mi)
% 174.58/24.93 % Detected minimum model sizes of [3]
% 174.58/24.93 % Detected maximum model sizes of [max]
% 174.58/24.93 % TRYING [3]
% 174.58/24.93 % TRYING [4]
% 174.58/24.93 % TRYING [5]
% 174.58/24.93 % TRYING [6]
% 174.58/24.93 % TRYING [7]
% 174.58/24.93 % (3839719)Instruction limit reached!
% 174.58/24.93 % (3839719)------------------------------
% 174.58/24.93 % (3839719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 174.58/24.93 % (3839719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.58/24.93 % (3839719)CaDiCaL version: 2.1.3
% 174.58/24.93 % (3839719)Termination reason: Instruction limit
% 174.58/24.93 % (3839719)Termination phase: Saturation
% 174.58/24.93 % (3839719)Time elapsed: 0.239 s
% 174.58/24.93 % (3839719)Peak memory usage: 15 MB
% 174.58/24.93 % (3839719)Instructions burned: 872 (million)
% 194.57/27.90 % (3839725)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3077907158:i=3512:aac=none_2972 on theBenchmark for (2972ds/3512Mi)
% 194.57/27.90 % TRYING [8]
% 194.57/27.90 % TRYING [11]
% 194.57/27.90 % TRYING [9]
% 194.57/27.90 % TRYING [13]
% 194.57/27.90 % TRYING [10]
% 194.57/27.90 % TRYING [11]
% 194.57/27.90 % (3839725)Instruction limit reached!
% 194.57/27.90 % (3839725)------------------------------
% 194.57/27.90 % (3839725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 194.57/27.90 % (3839725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.57/27.90 % (3839725)CaDiCaL version: 2.1.3
% 194.57/27.90 % (3839725)Termination reason: Instruction limit
% 194.57/27.90 % (3839725)Termination phase: Saturation
% 194.57/27.90 % (3839725)Time elapsed: 1.039 s
% 194.57/27.90 % (3839725)Peak memory usage: 26 MB
% 194.57/27.90 % (3839725)Instructions burned: 3515 (million)
% 194.57/27.90 % (3839727)dis+21_1_sil=32000:sas=cadical:random_seed=4025435593:i=3773:amm=off_2962 on theBenchmark for (2962ds/3773Mi)
% 194.57/27.90 % (3839721)Instruction limit reached!
% 194.57/27.90 % (3839721)------------------------------
% 194.57/27.90 % (3839721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 194.57/27.90 % (3839721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.57/27.90 % (3839721)CaDiCaL version: 2.1.3
% 194.57/27.90 % (3839721)Termination reason: Instruction limit
% 194.57/27.90 % (3839721)Termination phase: Saturation
% 194.57/27.90 % (3839721)Time elapsed: 1.401 s
% 194.57/27.90 % (3839721)Peak memory usage: 23 MB
% 194.57/27.90 % (3839721)Instructions burned: 5114 (million)
% 194.57/27.90 % (3839729)ott+11_1_sil=16000:gs=on:random_seed=1010665688:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2960 on theBenchmark for (2960ds/2251Mi)
% 194.57/27.90 % TRYING [12]
% 194.57/27.90 % TRYING [12]
% 194.57/27.90 % (3839729)Instruction limit reached!
% 194.57/27.90 % (3839729)------------------------------
% 194.57/27.90 % (3839729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 194.57/27.90 % (3839729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.57/27.90 % (3839729)CaDiCaL version: 2.1.3
% 194.57/27.90 % (3839729)Termination reason: Instruction limit
% 194.57/27.90 % (3839729)Termination phase: Saturation
% 194.57/27.90 % (3839729)Time elapsed: 0.799 s
% 194.57/27.90 % (3839729)Peak memory usage: 29 MB
% 194.57/27.90 % (3839729)Instructions burned: 2251 (million)
% 194.57/27.90 % (3839731)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=281715236:fmbsr=1.6:i=67534_2952 on theBenchmark for (2952ds/67534Mi)
% 194.57/27.90 % Detected minimum model sizes of [3]
% 194.57/27.90 % Detected maximum model sizes of [max]
% 194.57/27.90 % TRYING [7]
% 194.57/27.90 % (3839727)Instruction limit reached!
% 194.57/27.90 % (3839727)------------------------------
% 194.57/27.90 % (3839727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 194.57/27.90 % (3839727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.57/27.90 % (3839727)CaDiCaL version: 2.1.3
% 194.57/27.90 % (3839727)Termination reason: Instruction limit
% 194.57/27.90 % (3839727)Termination phase: Saturation
% 194.57/27.90 % (3839727)Time elapsed: 1.117 s
% 194.57/27.90 % (3839727)Peak memory usage: 25 MB
% 194.57/27.90 % (3839727)Instructions burned: 3775 (million)
% 194.57/27.90 % (3839733)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3543829880:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2950 on theBenchmark for (2950ds/4591Mi)
% 194.57/27.90 % TRYING [8]
% 194.57/27.90 % TRYING [13]
% 194.57/27.90 % TRYING [9]
% 194.57/27.90 % (3839733)Instruction limit reached!
% 194.57/27.90 % (3839733)------------------------------
% 194.57/27.90 % (3839733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 194.57/27.90 % (3839733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.57/27.90 % (3839733)CaDiCaL version: 2.1.3
% 194.57/27.90 % (3839733)Termination reason: Instruction limit
% 194.57/27.90 % (3839733)Termination phase: Saturation
% 194.57/27.90 % (3839733)Time elapsed: 1.347 s
% 194.57/27.90 % (3839733)Peak memory usage: 46 MB
% 194.57/27.90 % (3839733)Instructions burned: 4594 (million)
% 194.57/27.90 % (3839632)Instruction limit reached!
% 194.57/27.90 % (3839632)------------------------------
% 194.57/27.90 % (3839632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 194.57/27.90 % (3839632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.57/27.90 % (3839632)CaDiCaL version: 2.1.3
% 194.57/27.90 % (3839632)Termination reason: Instruction limit
% 194.57/27.90 % (3839632)Termination phase: Finite model building SAT solving
% 194.57/27.90 % (3839632)Time elapsed: 5.804 s
% 194.57/27.90 % (3839632)Peak memory usage: 232 MB
% 194.57/27.90 % (3839632)Instructions burned: 22061 (million)
% 194.57/27.90 % (3839735)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2983016450:i=29340_2937 on theBenchmark for (2937ds/29340Mi)
% 194.57/27.90 % (3839737)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4155378856:i=5211_2937 on theBenchmark for (2937ds/5211Mi)
% 194.57/27.90 % (3839737)Instruction limit reached!
% 194.57/27.90 % (3839737)------------------------------
% 194.57/27.90 % (3839737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 194.57/27.90 % (3839737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.57/27.90 % (3839737)CaDiCaL version: 2.1.3
% 194.57/27.90 % (3839737)Termination reason: Instruction limit
% 194.57/27.90 % (3839737)Termination phase: Saturation
% 194.57/27.90 % (3839737)Time elapsed: 1.408 s
% 194.57/27.90 % (3839737)Peak memory usage: 37 MB
% 194.57/27.90 % (3839737)Instructions burned: 5213 (million)
% 194.57/27.90 % (3839739)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=777726175:i=5497:nm=2_2922 on theBenchmark for (2922ds/5497Mi)
% 194.57/27.90 % Detected minimum model sizes of [3]
% 194.57/27.90 % Detected maximum model sizes of [max]
% 194.57/27.90 % TRYING [17]
% 194.57/27.90 % (3839739)Instruction limit reached!
% 194.57/27.90 % (3839739)------------------------------
% 194.57/27.90 % (3839739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 194.57/27.90 % (3839739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.57/27.90 % (3839739)CaDiCaL version: 2.1.3
% 194.57/27.90 % (3839739)Termination reason: Instruction limit
% 194.57/27.90 % (3839739)Termination phase: Finite model building constraint generation
% 194.57/27.90 % (3839739)Time elapsed: 1.215 s
% 194.57/27.90 % (3839739)Peak memory usage: 464 MB
% 194.57/27.90 % (3839739)Instructions burned: 5499 (million)
% 194.57/27.90 % (3839741)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2578360322:fmbsr=2:i=46332_2910 on theBenchmark for (2910ds/46332Mi)
% 194.57/27.90 % Detected minimum model sizes of [3]
% 194.57/27.90 % Detected maximum model sizes of [max]
% 194.57/27.90 % TRYING [15]
% 194.57/27.90 % TRYING [14]
% 194.57/27.90 % (3839735)Instruction limit reached!
% 194.57/27.90 % (3839735)------------------------------
% 194.57/27.90 % (3839735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 194.57/27.90 % (3839735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.57/27.90 % (3839735)CaDiCaL version: 2.1.3
% 194.57/27.90 % (3839735)Termination reason: Instruction limit
% 194.57/27.90 % (3839735)Termination phase: Saturation
% 194.57/27.90 % (3839735)Time elapsed: 7.564 s
% 194.57/27.90 % (3839735)Peak memory usage: 117 MB
% 194.57/27.90 % (3839735)Instructions burned: 29343 (million)
% 194.57/27.90 % (3839761)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2738142989:i=14071_2861 on theBenchmark for (2861ds/14071Mi)
% 194.57/27.90 % Detected minimum model sizes of [3]
% 194.57/27.90 % Detected maximum model sizes of [max]
% 194.57/27.90 % TRYING [12]
% 194.57/27.90 % TRYING [13]
% 194.57/27.90 % TRYING [14]
% 194.57/27.90 % (3839761)Instruction limit reached!
% 194.57/27.90 % (3839761)------------------------------
% 194.57/27.90 % (3839761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 194.57/27.90 % (3839761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.57/27.90 % (3839761)CaDiCaL version: 2.1.3
% 194.57/27.90 % (3839761)Termination reason: Instruction limit
% 194.57/27.90 % (3839761)Termination phase: Finite model building SAT solving
% 194.57/27.90 % (3839761)Time elapsed: 6.889 s
% 194.57/27.90 % (3839761)Peak memory usage: 554 MB
% 194.57/27.90 % (3839761)Instructions burned: 14072 (million)
% 194.57/27.90 % (3840076)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2662016810:i=22565:add=on:rawr=on_2791 on theBenchmark for (2791ds/22565Mi)
% 194.57/27.90 % (3839723)Instruction limit reached!
% 194.57/27.90 % (3839723)------------------------------
% 194.57/27.90 % (3839723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 194.57/27.90 % (3839723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.57/27.90 % (3839723)CaDiCaL version: 2.1.3
% 194.57/27.90 % (3839723)Termination reason: Instruction limit
% 194.57/27.90 % (3839723)Termination phase: Finite model building SAT solving
% 194.57/27.90 % (3839723)Time elapsed: 19.619 s
% 194.57/27.90 % (3839723)Peak memory usage: 632 MB
% 194.57/27.90 % (3839723)Instructions burned: 54282 (million)
% 194.57/27.90 % (3840197)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1376063606:i=8173:av=off_2776 on theBenchmark for (2776ds/8173Mi)
% 194.57/27.90 % (3840197)Instruction limit reached!
% 194.57/27.90 % (3840197)------------------------------
% 194.57/27.90 % (3840197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 194.57/27.90 % (3840197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.57/27.90 % (3840197)CaDiCaL version: 2.1.3
% 194.57/27.90 % (3840197)Termination reason: Instruction limit
% 194.57/27.90 % (3840197)Termination phase: Saturation
% 194.57/27.90 % (3840197)Time elapsed: 2.472 s
% 194.57/27.90 % (3840197)Peak memory usage: 38 MB
% 194.57/27.90 % (3840197)Instructions burned: 8175 (million)
% 194.57/27.90 % (3840237)dis+10_16:1_sil=16000:random_seed=1990607123:i=9155:fsr=off_2751 on theBenchmark for (2751ds/9155Mi)
% 194.57/27.90 % (3840237)Instruction limit reached!
% 194.57/27.90 % (3840237)------------------------------
% 194.57/27.90 % (3840237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 194.57/27.90 % (3840237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.57/27.90 % (3840237)CaDiCaL version: 2.1.3
% 194.57/27.90 % (3840237)Termination reason: Instruction limit
% 194.57/27.90 % (3840237)Termination phase: Saturation
% 194.57/27.90 % (3840237)Time elapsed: 2.563 s
% 194.57/27.90 % (3840237)Peak memory usage: 40 MB
% 194.57/27.90 % (3840237)Instructions burned: 9158 (million)
% 194.57/27.90 % (3840239)ott-3_8_sil=64000:random_seed=2893571404:i=20139:bs=on_2726 on theBenchmark for (2726ds/20139Mi)
% 194.57/27.90 % (3839731)Instruction limit reached!
% 194.57/27.90 % (3839731)------------------------------
% 194.57/27.90 % (3839731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 194.57/27.90 % (3839731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.57/27.90 % (3839731)CaDiCaL version: 2.1.3
% 194.57/27.90 % (3839731)Termination reason: Instruction limit
% 194.57/27.90 % (3839731)Termination phase: Finite model building SAT solving
% 194.57/27.90 % (3839731)Time elapsed: 22.707 s
% 194.57/27.90 % (3839731)Peak memory usage: 84 MB
% 194.57/27.90 % (3839731)Instructions burned: 67537 (million)
% 194.57/27.90 % (3840241)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4151549212:fmbsr=2:i=32576_2725 on theBenchmark for (2725ds/32576Mi)
% 194.57/27.90 % Detected minimum model sizes of [3]
% 194.57/27.90 % Detected maximum model sizes of [max]
% 194.57/27.90 % TRYING [9]
% 194.57/27.90 % (3840076) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3839465-3840076"...
% 194.57/27.90 % (3840076)...printing done.
% 194.57/27.90 % (3840076)Refutation found. Thanks to Tanya!
% 194.57/27.90 % SZS status Theorem for theBenchmark
% 194.57/27.90 % SZS output start Proof for theBenchmark
% See solution above
% 0.09/27.90 % (3840076)------------------------------
% 0.09/27.90 % (3840076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.09/27.90 % (3840076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.09/27.90 % (3840076)CaDiCaL version: 2.1.3
% 0.09/27.90 % (3840076)Termination reason: Refutation
% 0.09/27.90 % (3840076)Time elapsed: 6.795 s
% 0.09/27.90 % (3840076)Peak memory usage: 107 MB
% 0.09/27.90 % (3840076)Instructions burned: 14684 (million)
% 0.09/27.90 % (3839465)Success in time 27.765 s
% 0.09/27.90 % Vampire exiting
%------------------------------------------------------------------------------