%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR007+1 : 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 : n008.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 51.64s 7.69s
% Output : Refutation 52.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 46
% Syntax : Number of formulae : 303 ( 66 unt; 18 def)
% Number of atoms : 840 ( 120 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 893 ( 356 ~; 448 |; 51 &)
% ( 28 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 19 prp; 0-4 aty)
% Number of functors : 17 ( 17 usr; 9 con; 0-3 aty)
% Number of variables : 337 ( 0 sgn 316 !; 21 ?)
% 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(f6,axiom,
! [X0,X1] :
( ( ~ holdsAt(X0,X1)
& ~ releasedAt(X0,plus(X1,n1))
& ~ ? [X2] :
( happens(X2,X1)
& initiates(X2,X0,X1) ) )
=> ~ holdsAt(X0,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax',keep_not_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(f10,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& terminates(X0,X2,X1) )
=> ~ holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax',happens_terminates_not_holds) ).
fof(f12,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& ( initiates(X0,X2,X1)
| terminates(X0,X2,X1) ) )
=> ~ releasedAt(X2,plus(X1,n1)) ),
file('/export/starexec/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(f15,axiom,
! [X0,X1,X2] :
( releases(X0,X1,X2)
<=> ? [X3] :
( X0 = tapOn
& X1 = waterLevel(X3) ) ),
file('/export/starexec/sandbox2/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/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(f22,axiom,
! [X0] : filling != waterLevel(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+1.ax',filling_not_waterLevel) ).
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(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(f41,axiom,
! [X0] :
( less(X0,n3)
<=> less_or_equal(X0,n2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less3) ).
fof(f48,axiom,
! [X0,X1] :
( less(X0,X1)
<=> ( ~ less(X1,X0)
& X1 != X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_property) ).
fof(f49,axiom,
holdsAt(waterLevel(n0),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',waterLevel_0) ).
fof(f50,axiom,
~ holdsAt(filling,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_filling_0) ).
fof(f53,axiom,
~ releasedAt(filling,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_released_filling_0) ).
fof(f55,conjecture,
~ holdsAt(waterLevel(n3),n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',waterlevel_not_3) ).
fof(f56,negated_conjecture,
~ ~ holdsAt(waterLevel(n3),n2),
inference(negated_conjecture,[status(cth)],[f55]) ).
fof(f57,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) )
| ? [X4] :
( holdsAt(waterLevel(X4),X2)
& X0 = overflow
& waterLevel(X4) = X1 ) ) ),
inference(rectify,[],[f13]) ).
fof(f58,plain,
holdsAt(waterLevel(n3),n2),
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(f68,plain,
! [X0,X1] :
( ~ holdsAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ? [X2] :
( happens(X2,X1)
& initiates(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f6]) ).
fof(f69,plain,
! [X0,X1] :
( ~ holdsAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ? [X2] :
( happens(X2,X1)
& initiates(X2,X0,X1) ) ),
inference(flattening,[],[f68]) ).
fof(f72,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f73,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(flattening,[],[f72]) ).
fof(f74,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f75,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(flattening,[],[f74]) ).
fof(f76,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(flattening,[],[f76]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(flattening,[],[f80]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(ennf_transformation,[],[f17]) ).
fof(f83,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(flattening,[],[f82]) ).
fof(f84,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f85,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(flattening,[],[f84]) ).
fof(f86,plain,
! [X0] : ~ less(X0,n0),
inference(ennf_transformation,[],[f38]) ).
fof(f87,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| terminates(sK0(X0,X1,X2),X1,sK1(X0,X1,X2)) ),
inference(cnf_transformation,[],[f63]) ).
fof(f88,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| less(sK1(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f63]) ).
fof(f90,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| happens(sK0(X0,X1,X2),sK1(X0,X1,X2)) ),
inference(cnf_transformation,[],[f63]) ).
fof(f91,plain,
! [X2,X3,X0,X1,X4] :
( stoppedIn(X1,X2,plus(X1,X4))
| ~ trajectory(X2,X1,X3,X4)
| ~ less(n0,X4)
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X3,plus(X1,X4)) ),
inference(cnf_transformation,[],[f65]) ).
fof(f93,plain,
! [X0,X1] :
( happens(sK2(X0,X1),X1)
| releasedAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f67]) ).
fof(f94,plain,
! [X0,X1] :
( initiates(sK3(X0,X1),X0,X1)
| releasedAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| ~ holdsAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f69]) ).
fof(f95,plain,
! [X0,X1] :
( happens(sK3(X0,X1),X1)
| releasedAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| ~ holdsAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f69]) ).
fof(f98,plain,
! [X0,X1] :
( releases(sK5(X0,X1),X0,X1)
| releasedAt(X0,X1)
| ~ releasedAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f73]) ).
fof(f100,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f75]) ).
fof(f101,plain,
! [X2,X0,X1] :
( ~ terminates(X0,X2,X1)
| ~ happens(X0,X1)
| ~ holdsAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f77]) ).
fof(f104,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| ~ releasedAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f81]) ).
fof(f122,plain,
! [X2,X0,X1] :
( filling != X1
| tapOn != X0
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f57]) ).
fof(f131,plain,
! [X2,X0,X1] :
( waterLevel(sK9(X0,X1)) = X1
| ~ releases(X0,X1,X2) ),
inference(cnf_transformation,[],[f15]) ).
fof(f134,plain,
! [X0,X1] :
( n0 != X1
| tapOn != X0
| happens(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
fof(f135,plain,
! [X0,X1] :
( holdsAt(waterLevel(n3),X1)
| n0 = X1
| ~ happens(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
fof(f139,plain,
! [X0,X1] :
( overflow = X0
| n0 = X1
| ~ happens(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
fof(f142,plain,
! [X2,X3,X0,X1] :
( plus(X0,X3) != X2
| ~ holdsAt(waterLevel(X0),X1)
| trajectory(filling,X1,waterLevel(X2),X3) ),
inference(cnf_transformation,[],[f83]) ).
fof(f143,plain,
! [X2,X0,X1] :
( ~ holdsAt(waterLevel(X2),X0)
| ~ holdsAt(waterLevel(X1),X0)
| X1 = X2 ),
inference(cnf_transformation,[],[f85]) ).
fof(f147,plain,
! [X0] : filling != waterLevel(X0),
inference(cnf_transformation,[],[f22]) ).
fof(f153,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f27]) ).
fof(f154,plain,
n2 = plus(n0,n2),
inference(cnf_transformation,[],[f28]) ).
fof(f156,plain,
n2 = plus(n1,n1),
inference(cnf_transformation,[],[f30]) ).
fof(f162,plain,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[],[f36]) ).
fof(f163,plain,
! [X0,X1] :
( X0 = X1
| less(X0,X1)
| ~ less_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f164,plain,
! [X0,X1] :
( X0 != X1
| less_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f166,plain,
! [X0] : ~ less(X0,n0),
inference(cnf_transformation,[],[f86]) ).
fof(f167,plain,
! [X0] :
( ~ less_or_equal(X0,n0)
| less(X0,n1) ),
inference(cnf_transformation,[],[f39]) ).
fof(f168,plain,
! [X0] :
( less_or_equal(X0,n0)
| ~ less(X0,n1) ),
inference(cnf_transformation,[],[f39]) ).
fof(f169,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| less(X0,n2) ),
inference(cnf_transformation,[],[f40]) ).
fof(f170,plain,
! [X0] :
( less_or_equal(X0,n1)
| ~ less(X0,n2) ),
inference(cnf_transformation,[],[f40]) ).
fof(f171,plain,
! [X0] :
( ~ less_or_equal(X0,n2)
| less(X0,n3) ),
inference(cnf_transformation,[],[f41]) ).
fof(f185,plain,
! [X0,X1] :
( X0 != X1
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f186,plain,
! [X0,X1] :
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f187,plain,
! [X0,X1] :
( less(X1,X0)
| less(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f48]) ).
fof(f188,plain,
holdsAt(waterLevel(n0),n0),
inference(cnf_transformation,[],[f49]) ).
fof(f189,plain,
~ holdsAt(filling,n0),
inference(cnf_transformation,[],[f50]) ).
fof(f192,plain,
~ releasedAt(filling,n0),
inference(cnf_transformation,[],[f53]) ).
fof(f194,plain,
holdsAt(waterLevel(n3),n2),
inference(cnf_transformation,[],[f58]) ).
fof(f197,plain,
! [X2,X0] :
( tapOn != X0
| initiates(X0,filling,X2) ),
inference(equality_resolution,[],[f122]) ).
fof(f198,plain,
! [X2] : initiates(tapOn,filling,X2),
inference(equality_resolution,[],[f197]) ).
fof(f210,plain,
! [X0] :
( tapOn != X0
| happens(X0,n0) ),
inference(equality_resolution,[],[f134]) ).
fof(f211,plain,
happens(tapOn,n0),
inference(equality_resolution,[],[f210]) ).
fof(f212,plain,
! [X3,X0,X1] :
( ~ holdsAt(waterLevel(X0),X1)
| trajectory(filling,X1,waterLevel(plus(X0,X3)),X3) ),
inference(equality_resolution,[],[f142]) ).
fof(f214,plain,
! [X1] : less_or_equal(X1,X1),
inference(equality_resolution,[],[f164]) ).
fof(f215,plain,
! [X1] : ~ less(X1,X1),
inference(equality_resolution,[],[f185]) ).
fof(f216,plain,
! [X2,X0,X1] :
( ~ happens(sK0(X0,X1,X2),sK1(X0,X1,X2))
| stoppedIn(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f90]) ).
fof(f218,plain,
! [X2,X0,X1] :
( less(sK1(X0,X1,X2),X2)
| stoppedIn(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f88]) ).
fof(f219,plain,
! [X2,X0,X1] :
( ~ terminates(sK0(X0,X1,X2),X1,sK1(X0,X1,X2))
| stoppedIn(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f87]) ).
fof(f220,plain,
! [X2,X3,X0,X1,X4] :
( ~ initiates(X0,X2,X1)
| trajectory(X2,X1,X3,X4)
| ~ less(n0,X4)
| ~ stoppedIn(X1,X2,plus(X1,X4))
| happens(X0,X1)
| ~ holdsAt(X3,plus(X1,X4)) ),
inference(consistent_polarity_flipping,[],[f91]) ).
fof(f221,plain,
! [X0,X1] :
( ~ happens(sK2(X0,X1),X1)
| ~ releasedAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| ~ holdsAt(X0,plus(X1,n1)) ),
inference(consistent_polarity_flipping,[],[f93]) ).
fof(f223,plain,
! [X0,X1] :
( ~ happens(sK3(X0,X1),X1)
| ~ releasedAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1)) ),
inference(consistent_polarity_flipping,[],[f95]) ).
fof(f224,plain,
! [X0,X1] :
( initiates(sK3(X0,X1),X0,X1)
| ~ releasedAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1)) ),
inference(consistent_polarity_flipping,[],[f94]) ).
fof(f228,plain,
! [X0,X1] :
( ~ releases(sK5(X0,X1),X0,X1)
| ~ releasedAt(X0,X1)
| releasedAt(X0,plus(X1,n1)) ),
inference(consistent_polarity_flipping,[],[f98]) ).
fof(f229,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| happens(X0,X1)
| ~ holdsAt(X2,plus(X1,n1)) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f230,plain,
! [X2,X0,X1] :
( terminates(X0,X2,X1)
| holdsAt(X2,plus(X1,n1))
| happens(X0,X1) ),
inference(consistent_polarity_flipping,[],[f101]) ).
fof(f232,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| happens(X0,X1)
| releasedAt(X2,plus(X1,n1)) ),
inference(consistent_polarity_flipping,[],[f104]) ).
fof(f249,plain,
! [X2,X0,X1] :
( releases(X0,X1,X2)
| waterLevel(sK9(X0,X1)) = X1 ),
inference(consistent_polarity_flipping,[],[f131]) ).
fof(f252,plain,
! [X0,X1] :
( happens(X0,X1)
| n0 = X1
| overflow = X0 ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f256,plain,
! [X0,X1] :
( ~ holdsAt(waterLevel(n3),X1)
| n0 = X1
| happens(X0,X1) ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f257,plain,
~ happens(tapOn,n0),
inference(consistent_polarity_flipping,[],[f211]) ).
fof(f258,plain,
! [X3,X0,X1] :
( ~ trajectory(filling,X1,waterLevel(plus(X0,X3)),X3)
| holdsAt(waterLevel(X0),X1) ),
inference(consistent_polarity_flipping,[],[f212]) ).
fof(f259,plain,
! [X2,X0,X1] :
( holdsAt(waterLevel(X2),X0)
| holdsAt(waterLevel(X1),X0)
| X1 = X2 ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f261,plain,
! [X1] : ~ less_or_equal(X1,X1),
inference(consistent_polarity_flipping,[],[f214]) ).
fof(f262,plain,
! [X0,X1] :
( less_or_equal(X0,X1)
| less(X0,X1)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f263,plain,
! [X0] :
( ~ less_or_equal(X0,n0)
| ~ less(X0,n1) ),
inference(consistent_polarity_flipping,[],[f168]) ).
fof(f264,plain,
! [X0] :
( less_or_equal(X0,n0)
| less(X0,n1) ),
inference(consistent_polarity_flipping,[],[f167]) ).
fof(f265,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| ~ less(X0,n2) ),
inference(consistent_polarity_flipping,[],[f170]) ).
fof(f266,plain,
! [X0] :
( less_or_equal(X0,n1)
| less(X0,n2) ),
inference(consistent_polarity_flipping,[],[f169]) ).
fof(f268,plain,
! [X0] :
( less_or_equal(X0,n2)
| less(X0,n3) ),
inference(consistent_polarity_flipping,[],[f171]) ).
fof(f281,plain,
~ holdsAt(waterLevel(n0),n0),
inference(consistent_polarity_flipping,[],[f188]) ).
fof(f282,plain,
holdsAt(filling,n0),
inference(consistent_polarity_flipping,[],[f189]) ).
fof(f285,plain,
releasedAt(filling,n0),
inference(consistent_polarity_flipping,[],[f192]) ).
fof(f287,plain,
~ holdsAt(waterLevel(n3),n2),
inference(consistent_polarity_flipping,[],[f194]) ).
fof(f289,plain,
less(n0,n1),
inference(resolution,[],[f264,f261]) ).
fof(f292,plain,
less(n1,n2),
inference(resolution,[],[f266,f261]) ).
fof(f296,plain,
less(n2,n3),
inference(resolution,[],[f268,f261]) ).
fof(f298,plain,
~ less(n2,n1),
inference(resolution,[],[f292,f186]) ).
fof(f322,plain,
n1 = plus(n1,n0),
inference(superposition,[],[f162,f153]) ).
fof(f336,plain,
! [X0] :
( less(n0,X0)
| n0 = X0 ),
inference(resolution,[],[f187,f166]) ).
fof(f355,plain,
! [X0] :
( less(X0,n0)
| n0 = X0
| ~ less(X0,n1) ),
inference(resolution,[],[f262,f263]) ).
fof(f356,plain,
! [X0] :
( ~ less(X0,n2)
| n1 = X0
| less(X0,n1) ),
inference(resolution,[],[f262,f265]) ).
fof(f364,plain,
! [X0] :
( ~ less(X0,n1)
| n0 = X0 ),
inference(forward_subsumption_resolution,[],[f355,f166]) ).
fof(f387,definition,
( spl10_2
<=> holdsAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl10_2])],[avatar_definition]) ).
fof(f389,plain,
( holdsAt(filling,n2)
| ~ spl10_2 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f397,plain,
! [X2,X0,X1] :
( holdsAt(waterLevel(X1),X0)
| happens(X2,X0)
| n0 = X0
| n3 = X1 ),
inference(resolution,[],[f259,f256]) ).
fof(f401,plain,
! [X0] :
( holdsAt(waterLevel(X0),n2)
| n3 = X0 ),
inference(resolution,[],[f259,f287]) ).
fof(f409,plain,
! [X0] :
( ~ holdsAt(filling,plus(X0,n1))
| happens(tapOn,X0) ),
inference(resolution,[],[f229,f198]) ).
fof(f429,plain,
! [X0] :
( releasedAt(filling,plus(X0,n1))
| happens(tapOn,X0) ),
inference(resolution,[],[f232,f198]) ).
fof(f440,plain,
! [X0] :
( ~ trajectory(filling,X0,waterLevel(n1),n1)
| holdsAt(waterLevel(n0),X0) ),
inference(superposition,[],[f258,f153]) ).
fof(f442,plain,
! [X0] :
( ~ trajectory(filling,X0,waterLevel(n2),n2)
| holdsAt(waterLevel(n0),X0) ),
inference(superposition,[],[f258,f154]) ).
fof(f458,plain,
! [X2,X0,X1] :
( stoppedIn(X0,X1,X2)
| holdsAt(X1,plus(sK1(X0,X1,X2),n1))
| happens(sK0(X0,X1,X2),sK1(X0,X1,X2)) ),
inference(resolution,[],[f219,f230]) ).
fof(f461,plain,
! [X2,X0,X1] :
( stoppedIn(X0,X1,X2)
| holdsAt(X1,plus(sK1(X0,X1,X2),n1)) ),
inference(forward_subsumption_resolution,[],[f458,f216]) ).
fof(f463,plain,
! [X2,X0,X1] :
( holdsAt(X1,plus(n1,sK1(X0,X1,X2)))
| stoppedIn(X0,X1,X2) ),
inference(forward_demodulation,[],[f461,f162]) ).
fof(f465,plain,
! [X0,X1] :
( releasedAt(X0,plus(X1,n1))
| ~ releasedAt(X0,X1)
| waterLevel(sK9(sK5(X0,X1),X0)) = X0 ),
inference(resolution,[],[f228,f249]) ).
fof(f478,plain,
! [X0,X1] :
( ~ holdsAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| ~ releasedAt(X0,plus(X1,n1))
| n0 = X1
| overflow = sK2(X0,X1) ),
inference(resolution,[],[f221,f252]) ).
fof(f489,definition,
( spl10_3
<=> n1 = n3 ),
introduced(definition,[new_symbols(definition,[spl10_3])],[avatar_definition]) ).
fof(f490,plain,
( n1 != n3
| spl10_3 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f491,plain,
( n1 = n3
| ~ spl10_3 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f526,plain,
( less(n2,n1)
| ~ spl10_3 ),
inference(superposition,[],[f296,f491]) ).
fof(f535,plain,
( $false
| ~ spl10_3 ),
inference(forward_subsumption_resolution,[],[f526,f298]) ).
fof(f536,plain,
~ spl10_3,
inference(avatar_contradiction_clause,[],[f535]) ).
fof(f578,definition,
( spl10_9
<=> n0 = n2 ),
introduced(definition,[new_symbols(definition,[spl10_9])],[avatar_definition]) ).
fof(f579,plain,
( n0 != n2
| spl10_9 ),
inference(avatar_component_clause,[],[f578]) ).
fof(f580,plain,
( n0 = n2
| ~ spl10_9 ),
inference(avatar_component_clause,[],[f578]) ).
fof(f606,plain,
! [X2,X0,X1] :
( ~ less(n0,X2)
| trajectory(filling,X0,X1,X2)
| ~ stoppedIn(X0,filling,plus(X0,X2))
| happens(tapOn,X0)
| ~ holdsAt(X1,plus(X0,X2)) ),
inference(resolution,[],[f220,f198]) ).
fof(f608,plain,
! [X2,X3,X0,X1] :
( trajectory(X0,X1,X2,X3)
| ~ less(n0,X3)
| ~ stoppedIn(X1,X0,plus(X1,X3))
| happens(sK3(X0,X1),X1)
| ~ holdsAt(X2,plus(X1,X3))
| ~ releasedAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1)) ),
inference(resolution,[],[f220,f224]) ).
fof(f609,plain,
! [X2,X3,X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| ~ less(n0,X3)
| ~ stoppedIn(X1,X0,plus(X1,X3))
| ~ holdsAt(X2,plus(X1,X3))
| trajectory(X0,X1,X2,X3)
| ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1)) ),
inference(forward_subsumption_resolution,[],[f608,f223]) ).
fof(f650,plain,
( less(n1,n0)
| ~ spl10_9 ),
inference(superposition,[],[f292,f580]) ).
fof(f668,plain,
( $false
| ~ spl10_9 ),
inference(forward_subsumption_resolution,[],[f650,f166]) ).
fof(f669,plain,
~ spl10_9,
inference(avatar_contradiction_clause,[],[f668]) ).
fof(f678,plain,
! [X0,X1] :
( stoppedIn(X0,X1,n1)
| n0 = sK1(X0,X1,n1) ),
inference(resolution,[],[f364,f218]) ).
fof(f746,plain,
( ~ holdsAt(filling,n1)
| happens(tapOn,n0) ),
inference(superposition,[],[f409,f153]) ).
fof(f753,plain,
~ holdsAt(filling,n1),
inference(forward_subsumption_resolution,[],[f746,f257]) ).
fof(f772,plain,
( releasedAt(filling,n1)
| happens(tapOn,n0) ),
inference(superposition,[],[f429,f153]) ).
fof(f775,definition,
( spl10_19
<=> releasedAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl10_19])],[avatar_definition]) ).
fof(f776,plain,
( ~ releasedAt(filling,n2)
| spl10_19 ),
inference(avatar_component_clause,[],[f775]) ).
fof(f777,plain,
( releasedAt(filling,n2)
| ~ spl10_19 ),
inference(avatar_component_clause,[],[f775]) ).
fof(f779,plain,
releasedAt(filling,n1),
inference(forward_subsumption_resolution,[],[f772,f257]) ).
fof(f785,plain,
! [X0,X1] :
( less(sK1(X0,X1,n2),n1)
| n1 = sK1(X0,X1,n2)
| stoppedIn(X0,X1,n2) ),
inference(resolution,[],[f356,f218]) ).
fof(f968,definition,
( spl10_30
<=> holdsAt(filling,n1) ),
introduced(definition,[new_symbols(definition,[spl10_30])],[avatar_definition]) ).
fof(f969,plain,
( ~ holdsAt(filling,n1)
| spl10_30 ),
inference(avatar_component_clause,[],[f968]) ).
fof(f995,definition,
( spl10_31
<=> releasedAt(filling,n1) ),
introduced(definition,[new_symbols(definition,[spl10_31])],[avatar_definition]) ).
fof(f997,plain,
( releasedAt(filling,n1)
| ~ spl10_31 ),
inference(avatar_component_clause,[],[f995]) ).
fof(f1388,definition,
( spl10_52
<=> n0 = n1 ),
introduced(definition,[new_symbols(definition,[spl10_52])],[avatar_definition]) ).
fof(f1389,plain,
( n0 != n1
| spl10_52 ),
inference(avatar_component_clause,[],[f1388]) ).
fof(f1390,plain,
( n0 = n1
| ~ spl10_52 ),
inference(avatar_component_clause,[],[f1388]) ).
fof(f1424,plain,
! [X0] :
( releasedAt(X0,n2)
| ~ releasedAt(X0,n1)
| waterLevel(sK9(sK5(X0,n1),X0)) = X0 ),
inference(superposition,[],[f465,f156]) ).
fof(f1457,definition,
( spl10_57
<=> ! [X0] : happens(X0,n1) ),
introduced(definition,[new_symbols(definition,[spl10_57])],[avatar_definition]) ).
fof(f1458,plain,
( ! [X0] : happens(X0,n1)
| ~ spl10_57 ),
inference(avatar_component_clause,[],[f1457]) ).
fof(f1659,plain,
! [X0] :
( ~ holdsAt(X0,n2)
| holdsAt(X0,n1)
| ~ releasedAt(X0,n2)
| n0 = n1
| overflow = sK2(X0,n1) ),
inference(superposition,[],[f478,f156]) ).
fof(f1661,definition,
( spl10_59
<=> ! [X0] :
( ~ holdsAt(X0,n2)
| overflow = sK2(X0,n1)
| ~ releasedAt(X0,n2)
| holdsAt(X0,n1) ) ),
introduced(definition,[new_symbols(definition,[spl10_59])],[avatar_definition]) ).
fof(f1662,plain,
( ! [X0] :
( ~ releasedAt(X0,n2)
| overflow = sK2(X0,n1)
| ~ holdsAt(X0,n2)
| holdsAt(X0,n1) )
| ~ spl10_59 ),
inference(avatar_component_clause,[],[f1661]) ).
fof(f1663,plain,
( spl10_52
| spl10_59 ),
inference(avatar_split_clause,[],[f1659,f1661,f1388]) ).
fof(f1809,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,filling,plus(X0,X2))
| trajectory(filling,X0,X1,X2)
| happens(tapOn,X0)
| ~ holdsAt(X1,plus(X0,X2))
| n0 = X2 ),
inference(resolution,[],[f606,f336]) ).
fof(f2114,plain,
! [X2,X3,X0,X1] :
( ~ stoppedIn(X1,X2,plus(X1,X0))
| ~ less(n0,X0)
| ~ holdsAt(X3,plus(X1,X0))
| trajectory(X2,X1,X3,X0)
| ~ holdsAt(X2,X1)
| holdsAt(X2,plus(X1,n1))
| ~ releasedAt(X2,X1)
| waterLevel(sK9(sK5(X2,X1),X2)) = X2 ),
inference(resolution,[],[f609,f465]) ).
fof(f2174,definition,
( spl10_108
<=> ! [X0] :
( ~ holdsAt(X0,n2)
| trajectory(filling,n0,X0,n2) ) ),
introduced(definition,[new_symbols(definition,[spl10_108])],[avatar_definition]) ).
fof(f2175,plain,
( ! [X0] :
( trajectory(filling,n0,X0,n2)
| ~ holdsAt(X0,n2) )
| ~ spl10_108 ),
inference(avatar_component_clause,[],[f2174]) ).
fof(f2177,definition,
( spl10_109
<=> stoppedIn(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl10_109])],[avatar_definition]) ).
fof(f2179,plain,
( ~ stoppedIn(n0,filling,n2)
| spl10_109 ),
inference(avatar_component_clause,[],[f2177]) ).
fof(f2210,definition,
( spl10_113
<=> n0 = sK1(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl10_113])],[avatar_definition]) ).
fof(f2212,plain,
( n0 = sK1(n0,filling,n2)
| ~ spl10_113 ),
inference(avatar_component_clause,[],[f2210]) ).
fof(f2232,plain,
( ~ holdsAt(waterLevel(n2),n2)
| holdsAt(waterLevel(n0),n0)
| ~ spl10_108 ),
inference(resolution,[],[f2175,f442]) ).
fof(f2246,plain,
( ~ holdsAt(waterLevel(n2),n2)
| ~ spl10_108 ),
inference(forward_subsumption_resolution,[],[f2232,f281]) ).
fof(f2287,plain,
( n3 = n2
| ~ spl10_108 ),
inference(resolution,[],[f2246,f401]) ).
fof(f2332,plain,
~ spl10_30,
inference(avatar_split_clause,[],[f753,f968]) ).
fof(f2333,plain,
spl10_31,
inference(avatar_split_clause,[],[f779,f995]) ).
fof(f2349,plain,
( less(n1,n1)
| ~ spl10_52 ),
inference(superposition,[],[f289,f1390]) ).
fof(f2374,plain,
( $false
| ~ spl10_52 ),
inference(forward_subsumption_resolution,[],[f2349,f215]) ).
fof(f2375,plain,
~ spl10_52,
inference(avatar_contradiction_clause,[],[f2374]) ).
fof(f2726,definition,
( spl10_132
<=> n3 = n2 ),
introduced(definition,[new_symbols(definition,[spl10_132])],[avatar_definition]) ).
fof(f2728,plain,
( n3 = n2
| ~ spl10_132 ),
inference(avatar_component_clause,[],[f2726]) ).
fof(f4703,plain,
! [X0,X1] :
( stoppedIn(X0,X1,n2)
| n1 = sK1(X0,X1,n2)
| n0 = sK1(X0,X1,n2) ),
inference(resolution,[],[f785,f364]) ).
fof(f4850,plain,
( overflow = sK2(filling,n1)
| ~ holdsAt(filling,n2)
| holdsAt(filling,n1)
| ~ spl10_19
| ~ spl10_59 ),
inference(resolution,[],[f777,f1662]) ).
fof(f4853,plain,
( overflow = sK2(filling,n1)
| holdsAt(filling,n1)
| ~ spl10_2
| ~ spl10_19
| ~ spl10_59 ),
inference(forward_subsumption_resolution,[],[f4850,f389]) ).
fof(f4854,plain,
( overflow = sK2(filling,n1)
| ~ spl10_2
| ~ spl10_19
| spl10_30
| ~ spl10_59 ),
inference(forward_subsumption_resolution,[],[f4853,f969]) ).
fof(f4888,plain,
( ~ happens(overflow,n1)
| ~ releasedAt(filling,plus(n1,n1))
| holdsAt(filling,n1)
| ~ holdsAt(filling,plus(n1,n1))
| ~ spl10_2
| ~ spl10_19
| spl10_30
| ~ spl10_59 ),
inference(superposition,[],[f221,f4854]) ).
fof(f4889,plain,
( ~ releasedAt(filling,plus(n1,n1))
| holdsAt(filling,n1)
| ~ holdsAt(filling,plus(n1,n1))
| ~ spl10_2
| ~ spl10_19
| spl10_30
| ~ spl10_57
| ~ spl10_59 ),
inference(forward_subsumption_resolution,[],[f4888,f1458]) ).
fof(f4890,plain,
( ~ releasedAt(filling,plus(n1,n1))
| ~ holdsAt(filling,plus(n1,n1))
| ~ spl10_2
| ~ spl10_19
| spl10_30
| ~ spl10_57
| ~ spl10_59 ),
inference(forward_subsumption_resolution,[],[f4889,f969]) ).
fof(f4891,plain,
( ~ releasedAt(filling,n2)
| ~ holdsAt(filling,plus(n1,n1))
| ~ spl10_2
| ~ spl10_19
| spl10_30
| ~ spl10_57
| ~ spl10_59 ),
inference(forward_demodulation,[],[f4890,f156]) ).
fof(f4892,plain,
( ~ holdsAt(filling,plus(n1,n1))
| ~ spl10_2
| ~ spl10_19
| spl10_30
| ~ spl10_57
| ~ spl10_59 ),
inference(forward_subsumption_resolution,[],[f4891,f777]) ).
fof(f4893,plain,
( ~ holdsAt(filling,n2)
| ~ spl10_2
| ~ spl10_19
| spl10_30
| ~ spl10_57
| ~ spl10_59 ),
inference(forward_demodulation,[],[f4892,f156]) ).
fof(f4894,plain,
( $false
| ~ spl10_2
| ~ spl10_19
| spl10_30
| ~ spl10_57
| ~ spl10_59 ),
inference(forward_subsumption_resolution,[],[f4893,f389]) ).
fof(f4895,plain,
( ~ spl10_2
| ~ spl10_19
| spl10_30
| ~ spl10_57
| ~ spl10_59 ),
inference(avatar_contradiction_clause,[],[f4894]) ).
fof(f4907,plain,
( ~ releasedAt(filling,n1)
| filling = waterLevel(sK9(sK5(filling,n1),filling))
| spl10_19 ),
inference(resolution,[],[f776,f1424]) ).
fof(f4909,plain,
( filling = waterLevel(sK9(sK5(filling,n1),filling))
| spl10_19
| ~ spl10_31 ),
inference(forward_subsumption_resolution,[],[f4907,f997]) ).
fof(f4910,plain,
( $false
| spl10_19
| ~ spl10_31 ),
inference(forward_subsumption_resolution,[],[f4909,f147]) ).
fof(f4911,plain,
( spl10_19
| ~ spl10_31 ),
inference(avatar_contradiction_clause,[],[f4910]) ).
fof(f6671,definition,
( spl10_290
<=> ! [X0] :
( trajectory(filling,n0,X0,n1)
| ~ holdsAt(X0,n1) ) ),
introduced(definition,[new_symbols(definition,[spl10_290])],[avatar_definition]) ).
fof(f6672,plain,
( ! [X0] :
( trajectory(filling,n0,X0,n1)
| ~ holdsAt(X0,n1) )
| ~ spl10_290 ),
inference(avatar_component_clause,[],[f6671]) ).
fof(f6674,definition,
( spl10_291
<=> stoppedIn(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl10_291])],[avatar_definition]) ).
fof(f6675,plain,
( stoppedIn(n0,filling,n1)
| ~ spl10_291 ),
inference(avatar_component_clause,[],[f6674]) ).
fof(f6676,plain,
( ~ stoppedIn(n0,filling,n1)
| spl10_291 ),
inference(avatar_component_clause,[],[f6674]) ).
fof(f7334,plain,
! [X0] :
( ~ stoppedIn(n0,filling,n2)
| trajectory(filling,n0,X0,n2)
| happens(tapOn,n0)
| ~ holdsAt(X0,n2)
| n0 = n2 ),
inference(superposition,[],[f1809,f154]) ).
fof(f10526,plain,
! [X0,X1] :
( ~ stoppedIn(n0,X0,n1)
| ~ less(n0,n1)
| ~ holdsAt(X1,n1)
| trajectory(X0,n0,X1,n1)
| ~ holdsAt(X0,n0)
| holdsAt(X0,n1)
| ~ releasedAt(X0,n0)
| waterLevel(sK9(sK5(X0,n0),X0)) = X0 ),
inference(superposition,[],[f2114,f153]) ).
fof(f10546,plain,
! [X0,X1] :
( ~ stoppedIn(n0,X0,n1)
| ~ holdsAt(X1,n1)
| trajectory(X0,n0,X1,n1)
| ~ holdsAt(X0,n0)
| holdsAt(X0,n1)
| ~ releasedAt(X0,n0)
| waterLevel(sK9(sK5(X0,n0),X0)) = X0 ),
inference(forward_subsumption_resolution,[],[f10526,f289]) ).
fof(f13680,plain,
( n0 = sK1(n0,filling,n1)
| spl10_291 ),
inference(resolution,[],[f6676,f678]) ).
fof(f13690,definition,
( spl10_437
<=> n0 = sK1(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl10_437])],[avatar_definition]) ).
fof(f13692,plain,
( n0 = sK1(n0,filling,n1)
| ~ spl10_437 ),
inference(avatar_component_clause,[],[f13690]) ).
fof(f13704,plain,
( spl10_437
| spl10_291 ),
inference(avatar_split_clause,[],[f13680,f6674,f13690]) ).
fof(f16912,plain,
( spl10_132
| ~ spl10_108 ),
inference(avatar_split_clause,[],[f2287,f2174,f2726]) ).
fof(f16918,plain,
! [X0] :
( ~ stoppedIn(n0,filling,n2)
| trajectory(filling,n0,X0,n2)
| ~ holdsAt(X0,n2)
| n0 = n2 ),
inference(forward_subsumption_resolution,[],[f7334,f257]) ).
fof(f16919,plain,
( ! [X0] :
( ~ stoppedIn(n0,filling,n2)
| trajectory(filling,n0,X0,n2)
| ~ holdsAt(X0,n2) )
| spl10_9 ),
inference(forward_subsumption_resolution,[],[f16918,f579]) ).
fof(f16920,plain,
( spl10_108
| ~ spl10_109
| spl10_9 ),
inference(avatar_split_clause,[],[f16919,f578,f2177,f2174]) ).
fof(f16937,plain,
( less(n3,n3)
| ~ spl10_132 ),
inference(superposition,[],[f296,f2728]) ).
fof(f17172,plain,
( $false
| ~ spl10_132 ),
inference(forward_subsumption_resolution,[],[f16937,f215]) ).
fof(f17173,plain,
~ spl10_132,
inference(avatar_contradiction_clause,[],[f17172]) ).
fof(f21222,plain,
( n1 = sK1(n0,filling,n2)
| n0 = sK1(n0,filling,n2)
| spl10_109 ),
inference(resolution,[],[f4703,f2179]) ).
fof(f21224,definition,
( spl10_584
<=> n1 = sK1(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl10_584])],[avatar_definition]) ).
fof(f21226,plain,
( n1 = sK1(n0,filling,n2)
| ~ spl10_584 ),
inference(avatar_component_clause,[],[f21224]) ).
fof(f21227,plain,
( spl10_113
| spl10_584
| spl10_109 ),
inference(avatar_split_clause,[],[f21222,f2177,f21224,f2210]) ).
fof(f21260,plain,
( holdsAt(filling,plus(n1,n0))
| stoppedIn(n0,filling,n2)
| ~ spl10_113 ),
inference(superposition,[],[f463,f2212]) ).
fof(f21266,plain,
( holdsAt(filling,plus(n1,n0))
| spl10_109
| ~ spl10_113 ),
inference(forward_subsumption_resolution,[],[f21260,f2179]) ).
fof(f21282,plain,
( holdsAt(filling,n1)
| spl10_109
| ~ spl10_113 ),
inference(forward_demodulation,[],[f21266,f322]) ).
fof(f21292,plain,
( $false
| spl10_30
| spl10_109
| ~ spl10_113 ),
inference(forward_subsumption_resolution,[],[f21282,f969]) ).
fof(f21293,plain,
( spl10_30
| spl10_109
| ~ spl10_113 ),
inference(avatar_contradiction_clause,[],[f21292]) ).
fof(f21325,plain,
( holdsAt(filling,plus(n1,n1))
| stoppedIn(n0,filling,n2)
| ~ spl10_584 ),
inference(superposition,[],[f463,f21226]) ).
fof(f21331,plain,
( holdsAt(filling,plus(n1,n1))
| spl10_109
| ~ spl10_584 ),
inference(forward_subsumption_resolution,[],[f21325,f2179]) ).
fof(f21338,plain,
( holdsAt(filling,n2)
| spl10_109
| ~ spl10_584 ),
inference(forward_demodulation,[],[f21331,f156]) ).
fof(f24214,definition,
( spl10_640
<=> holdsAt(waterLevel(n1),n1) ),
introduced(definition,[new_symbols(definition,[spl10_640])],[avatar_definition]) ).
fof(f24215,plain,
( ~ holdsAt(waterLevel(n1),n1)
| spl10_640 ),
inference(avatar_component_clause,[],[f24214]) ).
fof(f45134,plain,
( spl10_2
| spl10_109
| ~ spl10_584 ),
inference(avatar_split_clause,[],[f21338,f21224,f2177,f387]) ).
fof(f130881,plain,
( holdsAt(filling,plus(n1,n0))
| stoppedIn(n0,filling,n1)
| ~ spl10_437 ),
inference(superposition,[],[f463,f13692]) ).
fof(f131014,plain,
( holdsAt(filling,n1)
| stoppedIn(n0,filling,n1)
| ~ spl10_437 ),
inference(forward_demodulation,[],[f130881,f322]) ).
fof(f131070,plain,
( stoppedIn(n0,filling,n1)
| spl10_30
| ~ spl10_437 ),
inference(forward_subsumption_resolution,[],[f131014,f969]) ).
fof(f131092,plain,
( spl10_291
| spl10_30
| ~ spl10_437 ),
inference(avatar_split_clause,[],[f131070,f13690,f968,f6674]) ).
fof(f131131,plain,
( ! [X0] :
( ~ holdsAt(X0,n1)
| trajectory(filling,n0,X0,n1)
| ~ holdsAt(filling,n0)
| holdsAt(filling,n1)
| ~ releasedAt(filling,n0)
| filling = waterLevel(sK9(sK5(filling,n0),filling)) )
| ~ spl10_291 ),
inference(resolution,[],[f6675,f10546]) ).
fof(f131137,plain,
( ! [X0] :
( ~ holdsAt(X0,n1)
| trajectory(filling,n0,X0,n1)
| holdsAt(filling,n1)
| ~ releasedAt(filling,n0)
| filling = waterLevel(sK9(sK5(filling,n0),filling)) )
| ~ spl10_291 ),
inference(forward_subsumption_resolution,[],[f131131,f282]) ).
fof(f131140,plain,
( ! [X0] :
( ~ holdsAt(X0,n1)
| trajectory(filling,n0,X0,n1)
| ~ releasedAt(filling,n0)
| filling = waterLevel(sK9(sK5(filling,n0),filling)) )
| spl10_30
| ~ spl10_291 ),
inference(forward_subsumption_resolution,[],[f131137,f969]) ).
fof(f131143,plain,
( ! [X0] :
( ~ holdsAt(X0,n1)
| trajectory(filling,n0,X0,n1)
| filling = waterLevel(sK9(sK5(filling,n0),filling)) )
| spl10_30
| ~ spl10_291 ),
inference(forward_subsumption_resolution,[],[f131140,f285]) ).
fof(f131150,plain,
( ! [X0] :
( ~ holdsAt(X0,n1)
| trajectory(filling,n0,X0,n1) )
| spl10_30
| ~ spl10_291 ),
inference(forward_subsumption_resolution,[],[f131143,f147]) ).
fof(f131151,plain,
( spl10_290
| spl10_30
| ~ spl10_291 ),
inference(avatar_split_clause,[],[f131150,f6674,f968,f6671]) ).
fof(f131153,plain,
( ~ holdsAt(waterLevel(n1),n1)
| holdsAt(waterLevel(n0),n0)
| ~ spl10_290 ),
inference(resolution,[],[f6672,f440]) ).
fof(f131192,plain,
( ~ holdsAt(waterLevel(n1),n1)
| ~ spl10_290 ),
inference(forward_subsumption_resolution,[],[f131153,f281]) ).
fof(f131204,plain,
( ~ spl10_640
| ~ spl10_290 ),
inference(avatar_split_clause,[],[f131192,f6671,f24214]) ).
fof(f131328,plain,
( ! [X0] :
( happens(X0,n1)
| n0 = n1
| n1 = n3 )
| spl10_640 ),
inference(resolution,[],[f24215,f397]) ).
fof(f131393,plain,
( ! [X0] :
( happens(X0,n1)
| n1 = n3 )
| spl10_52
| spl10_640 ),
inference(forward_subsumption_resolution,[],[f131328,f1389]) ).
fof(f131430,plain,
( ! [X0] : happens(X0,n1)
| spl10_3
| spl10_52
| spl10_640 ),
inference(forward_subsumption_resolution,[],[f131393,f490]) ).
fof(f131436,plain,
( spl10_57
| spl10_3
| spl10_52
| spl10_640 ),
inference(avatar_split_clause,[],[f131430,f24214,f1388,f489,f1457]) ).
cnf(s5,plain,
~ spl10_3,
inference(sat_conversion,[],[f536]) ).
cnf(s13,plain,
~ spl10_9,
inference(sat_conversion,[],[f669]) ).
cnf(s74,plain,
( spl10_52
| spl10_59 ),
inference(sat_conversion,[],[f1663]) ).
cnf(s141,plain,
~ spl10_30,
inference(sat_conversion,[],[f2332]) ).
cnf(s142,plain,
spl10_31,
inference(sat_conversion,[],[f2333]) ).
cnf(s146,plain,
~ spl10_52,
inference(sat_conversion,[],[f2375]) ).
cnf(s278,plain,
( ~ spl10_2
| ~ spl10_19
| spl10_30
| ~ spl10_57
| ~ spl10_59 ),
inference(sat_conversion,[],[f4895]) ).
cnf(s285,plain,
( spl10_19
| ~ spl10_31 ),
inference(sat_conversion,[],[f4911]) ).
cnf(s944,plain,
( spl10_291
| spl10_437 ),
inference(sat_conversion,[],[f13704]) ).
cnf(s1228,plain,
( ~ spl10_108
| spl10_132 ),
inference(sat_conversion,[],[f16912]) ).
cnf(s1230,plain,
( spl10_9
| spl10_108
| ~ spl10_109 ),
inference(sat_conversion,[],[f16920]) ).
cnf(s1237,plain,
~ spl10_132,
inference(sat_conversion,[],[f17173]) ).
cnf(s1420,plain,
( spl10_109
| spl10_113
| spl10_584 ),
inference(sat_conversion,[],[f21227]) ).
cnf(s1425,plain,
( spl10_30
| spl10_109
| ~ spl10_113 ),
inference(sat_conversion,[],[f21293]) ).
cnf(s2398,plain,
( spl10_2
| spl10_109
| ~ spl10_584 ),
inference(sat_conversion,[],[f45134]) ).
cnf(s4478,plain,
( spl10_30
| spl10_291
| ~ spl10_437 ),
inference(sat_conversion,[],[f131092]) ).
cnf(s4490,plain,
( spl10_30
| spl10_290
| ~ spl10_291 ),
inference(sat_conversion,[],[f131151]) ).
cnf(s4503,plain,
( ~ spl10_290
| ~ spl10_640 ),
inference(sat_conversion,[],[f131204]) ).
cnf(s4525,plain,
( spl10_3
| spl10_52
| spl10_57
| spl10_640 ),
inference(sat_conversion,[],[f131436]) ).
cnf(s4573,plain,
~ spl10_108,
inference(rat,[],[s1228,s1237]) ).
cnf(s4790,plain,
spl10_19,
inference(rat,[],[s285,s142]) ).
cnf(s4802,plain,
spl10_59,
inference(rat,[],[s74,s146]) ).
cnf(s4816,plain,
~ spl10_109,
inference(rat,[],[s1230,s4573,s13]) ).
cnf(s4817,plain,
~ spl10_113,
inference(rat,[],[s1425,s141,s4816]) ).
cnf(s4819,plain,
spl10_584,
inference(rat,[],[s1420,s4816,s4817]) ).
cnf(s4823,plain,
spl10_2,
inference(rat,[],[s2398,s4816,s4819]) ).
cnf(s4910,plain,
~ spl10_57,
inference(rat,[],[s278,s4802,s141,s4790,s4823]) ).
cnf(s5111,plain,
spl10_640,
inference(rat,[],[s4525,s4910,s146,s5]) ).
cnf(s5112,plain,
~ spl10_290,
inference(rat,[],[s4503,s5111]) ).
cnf(s5113,plain,
~ spl10_291,
inference(rat,[],[s4490,s141,s5112]) ).
cnf(s5114,plain,
~ spl10_437,
inference(rat,[],[s4478,s141,s5113]) ).
cnf(s5115,plain,
$false,
inference(rat,[],[s944,s5114,s5113]) ).
fof(f131439,plain,
$false,
inference(avatar_sat_refutation,[],[s5115]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR007+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n008.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 22:06:09 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 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
% 15.30/2.40 % (2709028)Will run a generic schedule for satisfiability detection.
% 15.30/2.40 % (2709036)dis+10_1_sil=32000:sp=arity:random_seed=1730717627:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.30/2.40 % (2709034)% WARNING: option uhcvi not known.
% 15.30/2.40 % (2709035)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1936437809:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.30/2.40 % (2709033)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=997542964_2999 on theBenchmark for (2999ds/0Mi)
% 15.30/2.40 % (2709034)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2190425043:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.30/2.40 % (2709037)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3197628270:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.30/2.40 % (2709039)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2870695833:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.30/2.40 % Detected minimum model sizes of [3]
% 15.30/2.40 % Detected maximum model sizes of [max]
% 15.30/2.40 % TRYING [3]
% 15.30/2.40 % (2709038)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3327426658:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.30/2.40 % TRYING [4]
% 15.30/2.40 % (2709036)Instruction limit reached!
% 15.30/2.40 % (2709036)------------------------------
% 15.30/2.40 % (2709036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.30/2.40 % (2709036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.30/2.40 % (2709036)CaDiCaL version: 2.1.3
% 15.30/2.40 % (2709036)Termination reason: Instruction limit
% 15.30/2.40 % (2709036)Termination phase: Saturation
% 15.30/2.40 % (2709036)Time elapsed: 0.034 s
% 15.30/2.40 % (2709036)Peak memory usage: 12 MB
% 15.30/2.40 % (2709036)Instructions burned: 105 (million)
% 15.30/2.40 % TRYING [5]
% 15.30/2.40 % (2709062)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2684537628:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.30/2.40 % Detected minimum model sizes of [3]
% 15.30/2.40 % Detected maximum model sizes of [max]
% 15.30/2.40 % TRYING [3]
% 15.30/2.40 % TRYING [4]
% 15.30/2.40 % TRYING [5]
% 15.30/2.40 % TRYING [6]
% 15.30/2.40 % (2709037)Instruction limit reached!
% 15.30/2.40 % (2709037)------------------------------
% 15.30/2.40 % (2709037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.30/2.40 % (2709037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.30/2.40 % (2709037)CaDiCaL version: 2.1.3
% 15.30/2.40 % (2709037)Termination reason: Instruction limit
% 15.30/2.40 % (2709037)Termination phase: Saturation
% 15.30/2.40 % (2709037)Time elapsed: 0.077 s
% 15.30/2.40 % (2709037)Peak memory usage: 13 MB
% 15.30/2.40 % (2709037)Instructions burned: 117 (million)
% 15.30/2.40 % TRYING [6]
% 15.30/2.40 % (2709039)Instruction limit reached!
% 15.30/2.40 % (2709039)------------------------------
% 15.30/2.40 % (2709039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.30/2.40 % (2709039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.30/2.40 % (2709039)CaDiCaL version: 2.1.3
% 15.30/2.40 % (2709039)Termination reason: Instruction limit
% 15.30/2.40 % (2709039)Termination phase: Saturation
% 15.30/2.40 % (2709039)Time elapsed: 0.091 s
% 15.30/2.40 % (2709039)Peak memory usage: 13 MB
% 15.30/2.40 % (2709039)Instructions burned: 161 (million)
% 15.30/2.40 % (2709038)Instruction limit reached!
% 15.30/2.40 % (2709038)------------------------------
% 15.30/2.40 % (2709038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.30/2.40 % (2709038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.30/2.40 % (2709038)CaDiCaL version: 2.1.3
% 15.30/2.40 % (2709038)Termination reason: Instruction limit
% 15.30/2.40 % (2709038)Termination phase: Saturation
% 15.30/2.40 % (2709038)Time elapsed: 0.089 s
% 15.30/2.40 % (2709038)Peak memory usage: 13 MB
% 15.30/2.40 % (2709038)Instructions burned: 132 (million)
% 15.30/2.40 % (2709082)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1462704768:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.30/2.40 % (2709094)ott-21_1_sil=16000:fs=off:random_seed=2180223228:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.30/2.40 % (2709093)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=1932214140:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.30/2.40 % TRYING [7]
% 15.30/2.40 % TRYING [7]
% 35.00/5.21 % (2709082)Instruction limit reached!
% 35.00/5.21 % (2709082)------------------------------
% 35.00/5.21 % (2709082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.00/5.21 % (2709082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.00/5.21 % (2709082)CaDiCaL version: 2.1.3
% 35.00/5.21 % (2709082)Termination reason: Instruction limit
% 35.00/5.21 % (2709082)Termination phase: Saturation
% 35.00/5.21 % (2709082)Time elapsed: 0.088 s
% 35.00/5.21 % (2709082)Peak memory usage: 13 MB
% 35.00/5.21 % (2709082)Instructions burned: 132 (million)
% 35.00/5.21 % (2709062)Instruction limit reached!
% 35.00/5.21 % (2709062)------------------------------
% 35.00/5.21 % (2709062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.00/5.21 % (2709062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.00/5.21 % (2709062)CaDiCaL version: 2.1.3
% 35.00/5.21 % (2709062)Termination reason: Instruction limit
% 35.00/5.21 % (2709062)Termination phase: Finite model building constraint generation
% 35.00/5.21 % (2709062)Time elapsed: 0.149 s
% 35.00/5.21 % (2709062)Peak memory usage: 27 MB
% 35.00/5.21 % (2709062)Instructions burned: 715 (million)
% 35.00/5.21 % (2709128)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2284164726:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 35.00/5.21 % Detected minimum model sizes of [3]
% 35.00/5.21 % Detected maximum model sizes of [max]
% 35.00/5.21 % TRYING [3]
% 35.00/5.21 % (2709127)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3210605718:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 35.00/5.21 % (2709094)Instruction limit reached!
% 35.00/5.21 % (2709094)------------------------------
% 35.00/5.21 % (2709094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.00/5.21 % (2709094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.00/5.21 % (2709094)CaDiCaL version: 2.1.3
% 35.00/5.21 % (2709094)Termination reason: Instruction limit
% 35.00/5.21 % (2709094)Termination phase: Saturation
% 35.00/5.21 % (2709094)Time elapsed: 0.095 s
% 35.00/5.21 % (2709094)Peak memory usage: 12 MB
% 35.00/5.21 % (2709094)Instructions burned: 182 (million)
% 35.00/5.21 % TRYING [4]
% 35.00/5.21 % (2709139)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4134783041:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 35.00/5.21 % TRYING [5]
% 35.00/5.21 % TRYING [8]
% 35.00/5.21 % TRYING [6]
% 35.00/5.21 % (2709128)Instruction limit reached!
% 35.00/5.21 % (2709128)------------------------------
% 35.00/5.21 % (2709128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.00/5.21 % (2709128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.00/5.21 % (2709128)CaDiCaL version: 2.1.3
% 35.00/5.21 % (2709128)Termination reason: Instruction limit
% 35.00/5.21 % (2709128)Termination phase: Finite model building SAT solving
% 35.00/5.21 % (2709128)Time elapsed: 0.185 s
% 35.00/5.21 % (2709128)Peak memory usage: 25 MB
% 35.00/5.21 % (2709128)Instructions burned: 871 (million)
% 35.00/5.21 % (2709181)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2341068924:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 35.00/5.21 % (2709093)Instruction limit reached!
% 35.00/5.21 % (2709093)------------------------------
% 35.00/5.21 % (2709093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.00/5.21 % (2709093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.00/5.21 % (2709093)CaDiCaL version: 2.1.3
% 35.00/5.21 % (2709093)Termination reason: Instruction limit
% 35.00/5.21 % (2709093)Termination phase: Saturation
% 35.00/5.21 % (2709093)Time elapsed: 0.359 s
% 35.00/5.21 % (2709093)Peak memory usage: 14 MB
% 35.00/5.21 % (2709093)Instructions burned: 685 (million)
% 35.00/5.21 % TRYING [14]
% 35.00/5.21 % (2709207)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=3120526509:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 35.00/5.21 % (2709127)Instruction limit reached!
% 35.00/5.21 % (2709127)------------------------------
% 35.00/5.21 % (2709127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.00/5.21 % (2709127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.00/5.21 % (2709127)CaDiCaL version: 2.1.3
% 35.00/5.21 % (2709127)Termination reason: Instruction limit
% 35.00/5.21 % (2709127)Termination phase: Saturation
% 35.00/5.21 % (2709127)Time elapsed: 0.361 s
% 35.00/5.21 % (2709127)Peak memory usage: 13 MB
% 35.00/5.21 % (2709127)Instructions burned: 477 (million)
% 51.64/7.69 % (2709209)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2318786240:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 51.64/7.69 % TRYING [9]
% 51.64/7.69 % (2709181)Instruction limit reached!
% 51.64/7.69 % (2709181)------------------------------
% 51.64/7.69 % (2709181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.64/7.69 % (2709181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.64/7.69 % (2709181)CaDiCaL version: 2.1.3
% 51.64/7.69 % (2709181)Termination reason: Instruction limit
% 51.64/7.69 % (2709181)Termination phase: Finite model building constraint generation
% 51.64/7.69 % (2709181)Time elapsed: 0.335 s
% 51.64/7.69 % (2709181)Peak memory usage: 79 MB
% 51.64/7.69 % (2709181)Instructions burned: 893 (million)
% 51.64/7.69 % (2709220)fmb+10_1_sil=64000:random_seed=1013692739:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 51.64/7.69 % Detected minimum model sizes of [3]
% 51.64/7.69 % Detected maximum model sizes of [max]
% 51.64/7.69 % TRYING [3]
% 51.64/7.69 % TRYING [4]
% 51.64/7.69 % TRYING [5]
% 51.64/7.69 % TRYING [6]
% 51.64/7.69 % TRYING [7]
% 51.64/7.69 % (2709207)Instruction limit reached!
% 51.64/7.69 % (2709207)------------------------------
% 51.64/7.69 % (2709207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.64/7.69 % (2709207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.64/7.69 % (2709207)CaDiCaL version: 2.1.3
% 51.64/7.69 % (2709207)Termination reason: Instruction limit
% 51.64/7.69 % (2709207)Termination phase: Saturation
% 51.64/7.69 % (2709207)Time elapsed: 0.442 s
% 51.64/7.69 % (2709207)Peak memory usage: 16 MB
% 51.64/7.69 % (2709207)Instructions burned: 694 (million)
% 51.64/7.69 % (2709288)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3007280945:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 51.64/7.69 % Detected minimum model sizes of [3]
% 51.64/7.69 % Detected maximum model sizes of [max]
% 51.64/7.69 % TRYING [20]
% 51.64/7.69 % (2709139)Instruction limit reached!
% 51.64/7.69 % (2709139)------------------------------
% 51.64/7.69 % (2709139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.64/7.69 % (2709139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.64/7.69 % (2709139)CaDiCaL version: 2.1.3
% 51.64/7.69 % (2709139)Termination reason: Instruction limit
% 51.64/7.69 % (2709139)Termination phase: Saturation
% 51.64/7.69 % (2709139)Time elapsed: 0.823 s
% 51.64/7.69 % (2709139)Peak memory usage: 19 MB
% 51.64/7.69 % (2709139)Instructions burned: 1179 (million)
% 51.64/7.69 % (2709320)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1318678418:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 51.64/7.69 % Detected minimum model sizes of [3]
% 51.64/7.69 % Detected maximum model sizes of [max]
% 51.64/7.69 % TRYING [8]
% 51.64/7.69 % TRYING [10]
% 51.64/7.69 % TRYING [8]
% 51.64/7.69 % (2709209)Instruction limit reached!
% 51.64/7.69 % (2709209)------------------------------
% 51.64/7.69 % (2709209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.64/7.69 % (2709209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.64/7.69 % (2709209)CaDiCaL version: 2.1.3
% 51.64/7.69 % (2709209)Termination reason: Instruction limit
% 51.64/7.69 % (2709209)Termination phase: Saturation
% 51.64/7.69 % (2709209)Time elapsed: 0.567 s
% 51.64/7.69 % (2709209)Peak memory usage: 18 MB
% 51.64/7.69 % (2709209)Instructions burned: 880 (million)
% 51.64/7.69 % (2709331)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1398184171:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 51.64/7.69 % TRYING [9]
% 51.64/7.69 % (2709320)Instruction limit reached!
% 51.64/7.69 % (2709320)------------------------------
% 51.64/7.69 % (2709320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.64/7.69 % (2709320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.64/7.69 % (2709320)CaDiCaL version: 2.1.3
% 51.64/7.69 % (2709320)Termination reason: Instruction limit
% 51.64/7.69 % (2709320)Termination phase: Finite model building constraint generation
% 51.64/7.69 % (2709320)Time elapsed: 0.346 s
% 51.64/7.69 % (2709320)Peak memory usage: 53 MB
% 51.64/7.69 % (2709320)Instructions burned: 923 (million)
% 51.64/7.69 % TRYING [9]
% 51.64/7.69 % (2709380)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3496797763:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 51.64/7.69 % TRYING [11]
% 51.64/7.69 % TRYING [10]
% 51.64/7.69 % (2709380)Instruction limit reached!
% 51.64/7.69 % (2709380)------------------------------
% 51.64/7.69 % (2709380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.64/7.69 % (2709380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.64/7.69 % (2709380)CaDiCaL version: 2.1.3
% 51.64/7.69 % (2709380)Termination reason: Instruction limit
% 51.64/7.69 % (2709380)Termination phase: Saturation
% 51.64/7.69 % (2709380)Time elapsed: 0.680 s
% 51.64/7.69 % (2709380)Peak memory usage: 16 MB
% 51.64/7.69 % (2709380)Instructions burned: 1472 (million)
% 51.64/7.69 % (2709382)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4276847857:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 51.64/7.69 % Detected minimum model sizes of [3]
% 51.64/7.69 % Detected maximum model sizes of [max]
% 51.64/7.69 % TRYING [77]
% 51.64/7.69 % TRYING [12]
% 51.64/7.69 % TRYING [11]
% 51.64/7.69 % (2709331)Instruction limit reached!
% 51.64/7.69 % (2709331)------------------------------
% 51.64/7.69 % (2709331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.64/7.69 % (2709331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.64/7.69 % (2709331)CaDiCaL version: 2.1.3
% 51.64/7.69 % (2709331)Termination reason: Instruction limit
% 51.64/7.69 % (2709331)Termination phase: Saturation
% 51.64/7.69 % (2709331)Time elapsed: 2.776 s
% 51.64/7.69 % (2709331)Peak memory usage: 24 MB
% 51.64/7.69 % (2709331)Instructions burned: 5133 (million)
% 51.64/7.69 % (2709384)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4250281948:fmbsr=2.30978:i=2174_2959 on theBenchmark for (2959ds/2174Mi)
% 51.64/7.69 % Detected minimum model sizes of [3]
% 51.64/7.69 % Detected maximum model sizes of [max]
% 51.64/7.69 % TRYING [16]
% 51.64/7.69 % (2709288)Instruction limit reached!
% 51.64/7.69 % (2709288)------------------------------
% 51.64/7.69 % (2709288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.64/7.69 % (2709288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.64/7.69 % (2709288)CaDiCaL version: 2.1.3
% 51.64/7.69 % (2709288)Termination reason: Instruction limit
% 51.64/7.69 % (2709288)Termination phase: Finite model building constraint generation
% 51.64/7.69 % (2709288)Time elapsed: 3.403 s
% 51.64/7.69 % (2709288)Peak memory usage: 611 MB
% 51.64/7.69 % (2709288)Instructions burned: 9515 (million)
% 51.64/7.69 % (2709386)ott-2_1_sil=16000:newcnf=on:random_seed=426773690:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi)
% 51.64/7.69 % (2709382)Instruction limit reached!
% 51.64/7.69 % (2709382)------------------------------
% 51.64/7.69 % (2709382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.64/7.69 % (2709382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.64/7.69 % (2709382)CaDiCaL version: 2.1.3
% 51.64/7.69 % (2709382)Termination reason: Instruction limit
% 51.64/7.69 % (2709382)Termination phase: Finite model building constraint generation
% 51.64/7.69 % (2709382)Time elapsed: 2.379 s
% 51.64/7.69 % (2709382)Peak memory usage: 516 MB
% 51.64/7.69 % (2709382)Instructions burned: 6325 (million)
% 51.64/7.69 % TRYING [12]
% 51.64/7.69 % (2709388)ott+10_1_sil=32000:tgt=ground:random_seed=3787702113:i=5114:av=off_2953 on theBenchmark for (2953ds/5114Mi)
% 51.64/7.69 % TRYING [13]
% 51.64/7.69 % (2709384)Instruction limit reached!
% 51.64/7.69 % (2709384)------------------------------
% 51.64/7.69 % (2709384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.64/7.69 % (2709384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.64/7.69 % (2709384)CaDiCaL version: 2.1.3
% 51.64/7.69 % (2709384)Termination reason: Instruction limit
% 51.64/7.69 % (2709384)Termination phase: Finite model building constraint generation
% 51.64/7.69 % (2709384)Time elapsed: 0.739 s
% 51.64/7.69 % (2709384)Peak memory usage: 134 MB
% 51.64/7.69 % (2709384)Instructions burned: 2176 (million)
% 51.64/7.69 % (2709390)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1698767893:i=54282_2952 on theBenchmark for (2952ds/54282Mi)
% 51.64/7.69 % Detected minimum model sizes of [3]
% 51.64/7.69 % Detected maximum model sizes of [max]
% 51.64/7.69 % TRYING [3]
% 51.64/7.69 % TRYING [4]
% 51.64/7.69 % TRYING [5]
% 51.64/7.69 % TRYING [6]
% 51.64/7.69 % TRYING [7]
% 51.64/7.69 % (2709386)Instruction limit reached!
% 51.64/7.69 % (2709386)------------------------------
% 51.64/7.69 % (2709386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.64/7.69 % (2709386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.64/7.69 % (2709386)CaDiCaL version: 2.1.3
% 51.64/7.69 % (2709386)Termination reason: Instruction limit
% 51.64/7.69 % (2709386)Termination phase: Saturation
% 51.64/7.69 % (2709386)Time elapsed: 0.455 s
% 51.64/7.69 % (2709386)Peak memory usage: 15 MB
% 51.64/7.69 % (2709386)Instructions burned: 870 (million)
% 51.64/7.69 % (2709392)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=436072532:i=3512:aac=none_2950 on theBenchmark for (2950ds/3512Mi)
% 51.64/7.69 % TRYING [8]
% 51.64/7.69 % TRYING [9]
% 51.64/7.69 % TRYING [10]
% 51.64/7.69 % (2709220)Instruction limit reached!
% 51.64/7.69 % (2709220)------------------------------
% 51.64/7.69 % (2709220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.64/7.69 % (2709220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.64/7.69 % (2709220)CaDiCaL version: 2.1.3
% 51.64/7.69 % (2709220)Termination reason: Instruction limit
% 51.64/7.69 % (2709220)Termination phase: Finite model building SAT solving
% 51.64/7.69 % (2709220)Time elapsed: 5.404 s
% 51.64/7.69 % (2709220)Peak memory usage: 233 MB
% 51.64/7.69 % (2709220)Instructions burned: 22063 (million)
% 51.64/7.69 % (2709394)dis+21_1_sil=32000:sas=cadical:random_seed=2286439262:i=3773:amm=off_2937 on theBenchmark for (2937ds/3773Mi)
% 51.64/7.69 % TRYING [11]
% 51.64/7.69 % (2709392)Instruction limit reached!
% 51.64/7.69 % (2709392)------------------------------
% 51.64/7.69 % (2709392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.64/7.69 % (2709392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.64/7.69 % (2709392)CaDiCaL version: 2.1.3
% 51.64/7.69 % (2709392)Termination reason: Instruction limit
% 51.64/7.69 % (2709392)Termination phase: Saturation
% 51.64/7.69 % (2709392)Time elapsed: 1.843 s
% 51.64/7.69 % (2709392)Peak memory usage: 27 MB
% 51.64/7.69 % (2709392)Instructions burned: 3512 (million)
% 51.64/7.69 % (2709396)ott+11_1_sil=16000:gs=on:random_seed=2866867388:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2931 on theBenchmark for (2931ds/2251Mi)
% 51.64/7.69 % TRYING [14]
% 51.64/7.69 % (2709388)Instruction limit reached!
% 51.64/7.69 % (2709388)------------------------------
% 51.64/7.69 % (2709388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.64/7.69 % (2709388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.64/7.69 % (2709388)CaDiCaL version: 2.1.3
% 51.64/7.69 % (2709388)Termination reason: Instruction limit
% 51.64/7.69 % (2709388)Termination phase: Saturation
% 51.64/7.69 % (2709388)Time elapsed: 2.690 s
% 51.64/7.69 % (2709388)Peak memory usage: 27 MB
% 51.64/7.69 % (2709388)Instructions burned: 5114 (million)
% 51.64/7.69 % (2709399)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4203277317:fmbsr=1.6:i=67534_2926 on theBenchmark for (2926ds/67534Mi)
% 51.64/7.69 % Detected minimum model sizes of [3]
% 51.64/7.69 % Detected maximum model sizes of [max]
% 51.64/7.69 % TRYING [7]
% 51.64/7.69 % (2709394)Instruction limit reached!
% 51.64/7.69 % (2709394)------------------------------
% 51.64/7.69 % (2709394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.64/7.69 % (2709394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.64/7.69 % (2709394)CaDiCaL version: 2.1.3
% 51.64/7.69 % (2709394)Termination reason: Instruction limit
% 51.64/7.69 % (2709394)Termination phase: Saturation
% 51.64/7.69 % (2709394)Time elapsed: 1.137 s
% 51.64/7.69 % (2709394)Peak memory usage: 26 MB
% 51.64/7.69 % (2709394)Instructions burned: 3775 (million)
% 51.64/7.69 % (2709401)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3930688973:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2926 on theBenchmark for (2926ds/4591Mi)
% 51.64/7.69 % (2709034) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2709028-2709034"...
% 51.64/7.69 % (2709034)...printing done.
% 51.64/7.69 % (2709034)Refutation found. Thanks to Tanya!
% 51.64/7.69 % SZS status Theorem for theBenchmark
% 51.64/7.69 % SZS output start Proof for theBenchmark
% See solution above
% 52.70/7.70 % (2709034)------------------------------
% 52.70/7.70 % (2709034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.70/7.70 % (2709034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.70/7.70 % (2709034)CaDiCaL version: 2.1.3
% 52.70/7.70 % (2709034)Termination reason: Refutation
% 52.70/7.70 % (2709034)Time elapsed: 7.362 s
% 52.70/7.70 % (2709034)Peak memory usage: 44 MB
% 52.70/7.70 % (2709034)Instructions burned: 13473 (million)
% 52.70/7.70 % (2709028)Success in time 7.459 s
% 52.70/7.70 % Vampire exiting
%------------------------------------------------------------------------------