%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR013+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 : n026.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:20 AM UTC 2026
% Result : Theorem 67.62s 9.99s
% Output : Refutation 67.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 35
% Syntax : Number of formulae : 241 ( 55 unt; 11 def)
% Number of atoms : 600 ( 141 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 589 ( 230 ~; 294 |; 37 &)
% ( 22 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 12 prp; 0-4 aty)
% Number of functors : 16 ( 16 usr; 10 con; 0-3 aty)
% Number of variables : 331 ( 0 sgn 316 !; 15 ?)
% 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(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(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(f20,axiom,
tapOff != overflow,
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',tapOff_not_overflow) ).
fof(f22,axiom,
! [X0] : filling != waterLevel(X0),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',filling_not_waterLevel) ).
fof(f25,axiom,
! [X0,X1] :
( waterLevel(X0) = waterLevel(X1)
<=> X0 = X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',distinct_waterLevels) ).
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(f30,axiom,
plus(n1,n1) = n2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus1_1) ).
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(f55,conjecture,
~ ? [X0] :
( happens(X0,n2)
& terminates(X0,filling,n2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nothing_terminates_filling_2) ).
fof(f56,negated_conjecture,
~ ~ ? [X0] :
( happens(X0,n2)
& terminates(X0,filling,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,
? [X0] :
( happens(X0,n2)
& terminates(X0,filling,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(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(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(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(f105,plain,
! [X2,X3,X0,X1] :
( waterLevel(X3) != X1
| tapOff != X0
| ~ holdsAt(waterLevel(X3),X2)
| sP8(X3,X2,X1,X0) ),
inference(cnf_transformation,[],[f57]) ).
fof(f106,plain,
! [X2,X3,X0,X1] :
( waterLevel(X3) = X1
| ~ sP8(X3,X2,X1,X0) ),
inference(cnf_transformation,[],[f57]) ).
fof(f120,plain,
! [X2,X0,X1] :
( sP8(sK7(X0,X1,X2),X2,X1,X0)
| overflow = X0
| filling = X1
| ~ initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f57]) ).
fof(f122,plain,
! [X2,X0,X1] :
( filling != X1
| tapOn != X0
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f57]) ).
fof(f124,plain,
! [X2,X3,X0,X1] :
( ~ sP8(X3,X2,X1,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(f133,plain,
! [X2,X3,X0,X1] :
( waterLevel(X3) != X1
| tapOn != X0
| 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(f137,plain,
! [X0,X1] :
( holdsAt(filling,X1)
| 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(f145,plain,
overflow != tapOff,
inference(cnf_transformation,[],[f20]) ).
fof(f147,plain,
! [X0] : filling != waterLevel(X0),
inference(cnf_transformation,[],[f22]) ).
fof(f151,plain,
! [X0,X1] :
( waterLevel(X0) != waterLevel(X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f25]) ).
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(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] :
( X0 = X1
| less(X1,X0)
| less(X0,X1) ),
inference(cnf_transformation,[],[f48]) ).
fof(f188,plain,
holdsAt(waterLevel(n0),n0),
inference(cnf_transformation,[],[f49]) ).
fof(f195,plain,
happens(sK10,n2),
inference(cnf_transformation,[],[f58]) ).
fof(f198,plain,
! [X2,X0] :
( tapOn != X0
| initiates(X0,filling,X2) ),
inference(equality_resolution,[],[f122]) ).
fof(f199,plain,
! [X2] : initiates(tapOn,filling,X2),
inference(equality_resolution,[],[f198]) ).
fof(f202,plain,
! [X2,X3,X0] :
( tapOff != X0
| ~ holdsAt(waterLevel(X3),X2)
| sP8(X3,X2,waterLevel(X3),X0) ),
inference(equality_resolution,[],[f105]) ).
fof(f203,plain,
! [X2,X3] :
( ~ holdsAt(waterLevel(X3),X2)
| sP8(X3,X2,waterLevel(X3),tapOff) ),
inference(equality_resolution,[],[f202]) ).
fof(f208,plain,
! [X2,X3,X0] :
( tapOn != X0
| releases(X0,waterLevel(X3),X2) ),
inference(equality_resolution,[],[f133]) ).
fof(f209,plain,
! [X2,X3] : releases(tapOn,waterLevel(X3),X2),
inference(equality_resolution,[],[f208]) ).
fof(f211,plain,
! [X0] :
( tapOn != X0
| happens(X0,n0) ),
inference(equality_resolution,[],[f134]) ).
fof(f212,plain,
happens(tapOn,n0),
inference(equality_resolution,[],[f211]) ).
fof(f213,plain,
! [X3,X0,X1] :
( ~ holdsAt(waterLevel(X0),X1)
| trajectory(filling,X1,waterLevel(plus(X0,X3)),X3) ),
inference(equality_resolution,[],[f142]) ).
fof(f215,plain,
! [X1] : less_or_equal(X1,X1),
inference(equality_resolution,[],[f164]) ).
fof(f216,plain,
! [X1] : ~ less(X1,X1),
inference(equality_resolution,[],[f185]) ).
fof(f217,plain,
! [X2,X0,X1] :
( happens(sK0(X0,X1,X2),sK1(X0,X1,X2))
| stoppedIn(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f90]) ).
fof(f219,plain,
! [X2,X0,X1] :
( ~ less(sK1(X0,X1,X2),X2)
| stoppedIn(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f88]) ).
fof(f220,plain,
! [X2,X0,X1] :
( ~ terminates(sK0(X0,X1,X2),X1,sK1(X0,X1,X2))
| stoppedIn(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f87]) ).
fof(f221,plain,
! [X2,X3,X0,X1,X4] :
( ~ happens(X0,X1)
| trajectory(X2,X1,X3,X4)
| less(n0,X4)
| ~ initiates(X0,X2,X1)
| ~ stoppedIn(X1,X2,plus(X1,X4))
| ~ holdsAt(X3,plus(X1,X4)) ),
inference(consistent_polarity_flipping,[],[f91]) ).
fof(f228,plain,
! [X2,X0,X1] :
( ~ happens(X0,X1)
| ~ initiates(X0,X2,X1)
| ~ holdsAt(X2,plus(X1,n1)) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f229,plain,
! [X2,X0,X1] :
( ~ happens(X0,X1)
| terminates(X0,X2,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(consistent_polarity_flipping,[],[f101]) ).
fof(f232,plain,
! [X2,X3,X0,X1] :
( sP8(X3,X2,X1,X0)
| initiates(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f124]) ).
fof(f234,plain,
! [X2,X0,X1] :
( ~ sP8(sK7(X0,X1,X2),X2,X1,X0)
| overflow = X0
| filling = X1
| ~ initiates(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f120]) ).
fof(f248,plain,
! [X2,X3,X0,X1] :
( sP8(X3,X2,X1,X0)
| waterLevel(X3) = X1 ),
inference(consistent_polarity_flipping,[],[f106]) ).
fof(f249,plain,
! [X2,X3] :
( ~ sP8(X3,X2,waterLevel(X3),tapOff)
| holdsAt(waterLevel(X3),X2) ),
inference(consistent_polarity_flipping,[],[f203]) ).
fof(f256,plain,
! [X2,X3] : ~ releases(tapOn,waterLevel(X3),X2),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f258,plain,
! [X2,X0,X1] :
( releases(X0,X1,X2)
| waterLevel(sK9(X0,X1)) = X1 ),
inference(consistent_polarity_flipping,[],[f131]) ).
fof(f261,plain,
! [X0,X1] :
( ~ holdsAt(filling,X1)
| n0 = X1
| ~ happens(X0,X1) ),
inference(consistent_polarity_flipping,[],[f137]) ).
fof(f263,plain,
! [X0,X1] :
( ~ holdsAt(waterLevel(n3),X1)
| n0 = X1
| ~ happens(X0,X1) ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f264,plain,
! [X3,X0,X1] :
( ~ trajectory(filling,X1,waterLevel(plus(X0,X3)),X3)
| holdsAt(waterLevel(X0),X1) ),
inference(consistent_polarity_flipping,[],[f213]) ).
fof(f265,plain,
! [X2,X0,X1] :
( holdsAt(waterLevel(X2),X0)
| holdsAt(waterLevel(X1),X0)
| X1 = X2 ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f267,plain,
! [X1] : ~ less_or_equal(X1,X1),
inference(consistent_polarity_flipping,[],[f215]) ).
fof(f268,plain,
! [X0,X1] :
( ~ less(X0,X1)
| X0 = X1
| less_or_equal(X0,X1) ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f269,plain,
! [X0] : less(X0,n0),
inference(consistent_polarity_flipping,[],[f166]) ).
fof(f270,plain,
! [X0] :
( ~ less_or_equal(X0,n0)
| less(X0,n1) ),
inference(consistent_polarity_flipping,[],[f168]) ).
fof(f272,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| less(X0,n2) ),
inference(consistent_polarity_flipping,[],[f170]) ).
fof(f273,plain,
! [X0] :
( ~ less(X0,n2)
| less_or_equal(X0,n1) ),
inference(consistent_polarity_flipping,[],[f169]) ).
fof(f275,plain,
! [X0] :
( ~ less(X0,n3)
| less_or_equal(X0,n2) ),
inference(consistent_polarity_flipping,[],[f171]) ).
fof(f288,plain,
! [X0,X1] :
( ~ less(X0,X1)
| ~ less(X1,X0)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f187]) ).
fof(f289,plain,
! [X0,X1] :
( less(X1,X0)
| less(X0,X1) ),
inference(consistent_polarity_flipping,[],[f186]) ).
fof(f290,plain,
! [X1] : less(X1,X1),
inference(consistent_polarity_flipping,[],[f216]) ).
fof(f291,plain,
~ holdsAt(waterLevel(n0),n0),
inference(consistent_polarity_flipping,[],[f188]) ).
fof(f297,plain,
less_or_equal(n3,n2),
inference(resolution,[],[f275,f290]) ).
fof(f327,plain,
n1 = plus(n1,n0),
inference(superposition,[],[f162,f153]) ).
fof(f357,definition,
( spl11_2
<=> n0 = n2 ),
introduced(definition,[new_symbols(definition,[spl11_2])],[avatar_definition]) ).
fof(f358,plain,
( n0 != n2
| spl11_2 ),
inference(avatar_component_clause,[],[f357]) ).
fof(f359,plain,
( n0 = n2
| ~ spl11_2 ),
inference(avatar_component_clause,[],[f357]) ).
fof(f375,plain,
( ! [X0] :
( ~ less(X0,n0)
| less_or_equal(X0,n1) )
| ~ spl11_2 ),
inference(superposition,[],[f273,f359]) ).
fof(f381,plain,
( ! [X0] : less_or_equal(X0,n1)
| ~ spl11_2 ),
inference(forward_subsumption_resolution,[],[f375,f269]) ).
fof(f387,plain,
! [X0] :
( less_or_equal(X0,n0)
| n0 = X0 ),
inference(resolution,[],[f268,f269]) ).
fof(f389,plain,
! [X0,X1] :
( less_or_equal(X0,X1)
| X0 = X1
| less(X1,X0) ),
inference(resolution,[],[f268,f289]) ).
fof(f400,plain,
! [X0,X1] :
( initiates(tapOff,waterLevel(X0),X1)
| holdsAt(waterLevel(X0),X1) ),
inference(resolution,[],[f249,f232]) ).
fof(f408,plain,
! [X0] : waterLevel(X0) = waterLevel(sK9(tapOn,waterLevel(X0))),
inference(resolution,[],[f258,f256]) ).
fof(f414,plain,
! [X0] :
( holdsAt(waterLevel(X0),n0)
| n0 = X0 ),
inference(resolution,[],[f265,f291]) ).
fof(f431,plain,
! [X0] :
( ~ initiates(tapOn,X0,n0)
| ~ holdsAt(X0,plus(n0,n1)) ),
inference(resolution,[],[f228,f212]) ).
fof(f432,plain,
! [X0] :
( ~ initiates(tapOn,X0,n0)
| ~ holdsAt(X0,n1) ),
inference(forward_demodulation,[],[f431,f153]) ).
fof(f440,plain,
( $false
| ~ spl11_2 ),
inference(resolution,[],[f381,f267]) ).
fof(f442,plain,
~ spl11_2,
inference(avatar_contradiction_clause,[],[f440]) ).
fof(f491,plain,
! [X0] :
( ~ trajectory(filling,X0,waterLevel(n2),n2)
| holdsAt(waterLevel(n0),X0) ),
inference(superposition,[],[f264,f154]) ).
fof(f508,plain,
! [X2,X3,X0,X1] :
( stoppedIn(X0,X1,X2)
| terminates(sK0(X0,X1,X2),X3,sK1(X0,X1,X2))
| holdsAt(X3,plus(sK1(X0,X1,X2),n1)) ),
inference(resolution,[],[f217,f229]) ).
fof(f513,plain,
! [X2,X3,X0,X1] :
( terminates(sK0(X0,X1,X2),X3,sK1(X0,X1,X2))
| stoppedIn(X0,X1,X2)
| holdsAt(X3,plus(n1,sK1(X0,X1,X2))) ),
inference(forward_demodulation,[],[f508,f162]) ).
fof(f573,definition,
( spl11_11
<=> holdsAt(filling,n1) ),
introduced(definition,[new_symbols(definition,[spl11_11])],[avatar_definition]) ).
fof(f574,plain,
( ~ holdsAt(filling,n1)
| spl11_11 ),
inference(avatar_component_clause,[],[f573]) ).
fof(f588,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X1,X2)
| filling = X1
| overflow = X0
| waterLevel(sK7(X0,X1,X2)) = X1 ),
inference(resolution,[],[f234,f248]) ).
fof(f734,plain,
! [X2,X0,X1] :
( ~ initiates(tapOn,X0,n0)
| less(n0,X2)
| trajectory(X0,n0,X1,X2)
| ~ stoppedIn(n0,X0,plus(n0,X2))
| ~ holdsAt(X1,plus(n0,X2)) ),
inference(resolution,[],[f221,f212]) ).
fof(f979,plain,
! [X0] :
( less(X0,n1)
| n0 = X0 ),
inference(resolution,[],[f387,f270]) ).
fof(f995,plain,
~ holdsAt(filling,n1),
inference(resolution,[],[f432,f199]) ).
fof(f1000,plain,
! [X0,X1] :
( waterLevel(X0) != waterLevel(X1)
| sK9(tapOn,waterLevel(X0)) = X1 ),
inference(superposition,[],[f151,f408]) ).
fof(f1009,plain,
! [X0] :
( holdsAt(waterLevel(X0),n0)
| n0 = sK9(tapOn,waterLevel(X0)) ),
inference(superposition,[],[f414,f408]) ).
fof(f1013,plain,
! [X0] :
( less(n1,X0)
| less(X0,n2)
| n1 = X0 ),
inference(resolution,[],[f389,f272]) ).
fof(f1110,definition,
( spl11_57
<=> ! [X1] : ~ happens(X1,n2) ),
introduced(definition,[new_symbols(definition,[spl11_57])],[avatar_definition]) ).
fof(f1111,plain,
( ! [X1] : ~ happens(X1,n2)
| ~ spl11_57 ),
inference(avatar_component_clause,[],[f1110]) ).
fof(f1256,plain,
~ spl11_11,
inference(avatar_split_clause,[],[f995,f573]) ).
fof(f1289,plain,
( $false
| ~ spl11_57 ),
inference(backward_subsumption_resolution,[],[f195,f1111]) ).
fof(f1291,plain,
~ spl11_57,
inference(avatar_contradiction_clause,[],[f1289]) ).
fof(f1334,plain,
! [X0,X1] :
( filling = waterLevel(X0)
| overflow = tapOff
| waterLevel(X0) = waterLevel(sK7(tapOff,waterLevel(X0),X1))
| holdsAt(waterLevel(X0),X1) ),
inference(resolution,[],[f588,f400]) ).
fof(f1335,plain,
! [X0,X1] :
( filling = waterLevel(X0)
| waterLevel(X0) = waterLevel(sK7(tapOff,waterLevel(X0),X1))
| holdsAt(waterLevel(X0),X1) ),
inference(forward_subsumption_resolution,[],[f1334,f145]) ).
fof(f1336,plain,
! [X0,X1] :
( holdsAt(waterLevel(X0),X1)
| waterLevel(X0) = waterLevel(sK7(tapOff,waterLevel(X0),X1)) ),
inference(forward_subsumption_resolution,[],[f1335,f147]) ).
fof(f1397,plain,
! [X2,X0,X1] :
( stoppedIn(X0,X1,X2)
| holdsAt(X1,plus(n1,sK1(X0,X1,X2)))
| stoppedIn(X0,X1,X2) ),
inference(resolution,[],[f513,f220]) ).
fof(f1398,plain,
! [X2,X0,X1] :
( holdsAt(X1,plus(n1,sK1(X0,X1,X2)))
| stoppedIn(X0,X1,X2) ),
inference(duplicate_literal_removal,[],[f1397]) ).
fof(f1420,plain,
! [X0,X1] :
( ~ stoppedIn(n0,filling,plus(n0,X0))
| trajectory(filling,n0,X1,X0)
| less(n0,X0)
| ~ holdsAt(X1,plus(n0,X0)) ),
inference(resolution,[],[f734,f199]) ).
fof(f1755,definition,
( spl11_74
<=> less(n0,n2) ),
introduced(definition,[new_symbols(definition,[spl11_74])],[avatar_definition]) ).
fof(f1756,plain,
( ~ less(n0,n2)
| spl11_74 ),
inference(avatar_component_clause,[],[f1755]) ).
fof(f1757,plain,
( less(n0,n2)
| ~ spl11_74 ),
inference(avatar_component_clause,[],[f1755]) ).
fof(f1822,plain,
( ~ less(n2,n0)
| n0 = n2
| ~ spl11_74 ),
inference(resolution,[],[f1757,f288]) ).
fof(f1825,plain,
( n0 = n2
| ~ spl11_74 ),
inference(forward_subsumption_resolution,[],[f1822,f269]) ).
fof(f1828,plain,
( $false
| spl11_2
| ~ spl11_74 ),
inference(forward_subsumption_resolution,[],[f1825,f358]) ).
fof(f1829,plain,
( spl11_2
| ~ spl11_74 ),
inference(avatar_contradiction_clause,[],[f1828]) ).
fof(f2009,definition,
( spl11_101
<=> n3 = n2 ),
introduced(definition,[new_symbols(definition,[spl11_101])],[avatar_definition]) ).
fof(f2011,plain,
( n3 = n2
| ~ spl11_101 ),
inference(avatar_component_clause,[],[f2009]) ).
fof(f2823,plain,
! [X0] :
( ~ less(n1,X0)
| n0 = X0
| n1 = X0 ),
inference(resolution,[],[f979,f288]) ).
fof(f3019,plain,
! [X0,X1] :
( less(n1,sK1(X0,X1,n2))
| n1 = sK1(X0,X1,n2)
| stoppedIn(X0,X1,n2) ),
inference(resolution,[],[f1013,f219]) ).
fof(f3272,plain,
n0 = sK9(tapOn,waterLevel(n0)),
inference(resolution,[],[f1009,f291]) ).
fof(f3381,plain,
! [X0] : sK9(tapOn,waterLevel(X0)) = X0,
inference(equality_resolution,[],[f1000]) ).
fof(f3412,plain,
! [X2,X0,X1] :
( ~ happens(X2,plus(n1,sK1(X0,filling,X1)))
| n0 = plus(n1,sK1(X0,filling,X1))
| stoppedIn(X0,filling,X1) ),
inference(resolution,[],[f1398,f261]) ).
fof(f3472,plain,
waterLevel(n0) = waterLevel(sK7(tapOff,waterLevel(n0),n0)),
inference(resolution,[],[f1336,f291]) ).
fof(f4059,plain,
! [X0] :
( ~ stoppedIn(n0,filling,n2)
| trajectory(filling,n0,X0,n2)
| less(n0,n2)
| ~ holdsAt(X0,n2) ),
inference(superposition,[],[f1420,f154]) ).
fof(f4062,plain,
( ! [X0] :
( ~ stoppedIn(n0,filling,n2)
| trajectory(filling,n0,X0,n2)
| ~ holdsAt(X0,n2) )
| spl11_74 ),
inference(forward_subsumption_resolution,[],[f4059,f1756]) ).
fof(f4077,definition,
( spl11_250
<=> ! [X0] :
( trajectory(filling,n0,X0,n2)
| ~ holdsAt(X0,n2) ) ),
introduced(definition,[new_symbols(definition,[spl11_250])],[avatar_definition]) ).
fof(f4078,plain,
( ! [X0] :
( trajectory(filling,n0,X0,n2)
| ~ holdsAt(X0,n2) )
| ~ spl11_250 ),
inference(avatar_component_clause,[],[f4077]) ).
fof(f4080,definition,
( spl11_251
<=> stoppedIn(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl11_251])],[avatar_definition]) ).
fof(f4082,plain,
( ~ stoppedIn(n0,filling,n2)
| spl11_251 ),
inference(avatar_component_clause,[],[f4080]) ).
fof(f4083,plain,
( spl11_250
| ~ spl11_251
| spl11_74 ),
inference(avatar_split_clause,[],[f4062,f1755,f4080,f4077]) ).
fof(f4101,definition,
( spl11_255
<=> n0 = sK1(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl11_255])],[avatar_definition]) ).
fof(f4102,plain,
( n0 != sK1(n0,filling,n2)
| spl11_255 ),
inference(avatar_component_clause,[],[f4101]) ).
fof(f4103,plain,
( n0 = sK1(n0,filling,n2)
| ~ spl11_255 ),
inference(avatar_component_clause,[],[f4101]) ).
fof(f4378,plain,
( ~ holdsAt(waterLevel(n2),n2)
| holdsAt(waterLevel(n0),n0)
| ~ spl11_250 ),
inference(resolution,[],[f4078,f491]) ).
fof(f4392,plain,
( ~ holdsAt(waterLevel(n2),n2)
| ~ spl11_250 ),
inference(forward_subsumption_resolution,[],[f4378,f291]) ).
fof(f4406,plain,
( ! [X0] :
( holdsAt(waterLevel(X0),n2)
| n2 = X0 )
| ~ spl11_250 ),
inference(resolution,[],[f4392,f265]) ).
fof(f4705,definition,
( spl11_277
<=> ! [X0] :
( holdsAt(waterLevel(X0),n2)
| n2 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl11_277])],[avatar_definition]) ).
fof(f4706,plain,
( ! [X0] :
( holdsAt(waterLevel(X0),n2)
| n2 = X0 )
| ~ spl11_277 ),
inference(avatar_component_clause,[],[f4705]) ).
fof(f4899,plain,
( spl11_277
| ~ spl11_250 ),
inference(avatar_split_clause,[],[f4406,f4077,f4705]) ).
fof(f5147,plain,
( ! [X0] :
( n3 = n2
| n0 = n2
| ~ happens(X0,n2) )
| ~ spl11_277 ),
inference(resolution,[],[f4706,f263]) ).
fof(f5166,plain,
( ! [X0] :
( n3 = n2
| ~ happens(X0,n2) )
| spl11_2
| ~ spl11_277 ),
inference(forward_subsumption_resolution,[],[f5147,f358]) ).
fof(f5174,plain,
( spl11_57
| spl11_101
| spl11_2
| ~ spl11_277 ),
inference(avatar_split_clause,[],[f5166,f4705,f357,f2009,f1110]) ).
fof(f9910,plain,
( less_or_equal(n3,n3)
| ~ spl11_101 ),
inference(superposition,[],[f297,f2011]) ).
fof(f10007,plain,
( $false
| ~ spl11_101 ),
inference(forward_subsumption_resolution,[],[f9910,f267]) ).
fof(f10008,plain,
~ spl11_101,
inference(avatar_contradiction_clause,[],[f10007]) ).
fof(f13266,plain,
sK9(tapOn,waterLevel(n0)) = sK7(tapOff,waterLevel(n0),n0),
inference(superposition,[],[f3381,f3472]) ).
fof(f13359,plain,
n0 = sK7(tapOff,waterLevel(n0),n0),
inference(forward_demodulation,[],[f13266,f3272]) ).
fof(f18093,plain,
! [X0,X1] :
( n1 = sK1(X0,X1,n2)
| stoppedIn(X0,X1,n2)
| n0 = sK1(X0,X1,n2)
| n1 = sK1(X0,X1,n2) ),
inference(resolution,[],[f3019,f2823]) ).
fof(f18100,plain,
! [X0,X1] :
( stoppedIn(X0,X1,n2)
| n1 = sK1(X0,X1,n2)
| n0 = sK1(X0,X1,n2) ),
inference(duplicate_literal_removal,[],[f18093]) ).
fof(f29558,plain,
( holdsAt(filling,plus(n1,n0))
| stoppedIn(n0,filling,n2)
| ~ spl11_255 ),
inference(superposition,[],[f1398,f4103]) ).
fof(f29573,plain,
( holdsAt(filling,plus(n1,n0))
| spl11_251
| ~ spl11_255 ),
inference(forward_subsumption_resolution,[],[f29558,f4082]) ).
fof(f29605,plain,
( holdsAt(filling,n1)
| spl11_251
| ~ spl11_255 ),
inference(forward_demodulation,[],[f29573,f327]) ).
fof(f29628,plain,
( $false
| spl11_11
| spl11_251
| ~ spl11_255 ),
inference(forward_subsumption_resolution,[],[f29605,f574]) ).
fof(f29629,plain,
( spl11_11
| spl11_251
| ~ spl11_255 ),
inference(avatar_contradiction_clause,[],[f29628]) ).
fof(f123425,definition,
( spl11_1536
<=> n0 = sK7(tapOff,waterLevel(n0),n0) ),
introduced(definition,[new_symbols(definition,[spl11_1536])],[avatar_definition]) ).
fof(f123427,plain,
( n0 = sK7(tapOff,waterLevel(n0),n0)
| ~ spl11_1536 ),
inference(avatar_component_clause,[],[f123425]) ).
fof(f125561,definition,
( spl11_1620
<=> n0 = plus(n1,plus(n1,sK7(tapOff,waterLevel(n0),n0))) ),
introduced(definition,[new_symbols(definition,[spl11_1620])],[avatar_definition]) ).
fof(f125562,plain,
( n0 != plus(n1,plus(n1,sK7(tapOff,waterLevel(n0),n0)))
| spl11_1620 ),
inference(avatar_component_clause,[],[f125561]) ).
fof(f125563,plain,
( n0 = plus(n1,plus(n1,sK7(tapOff,waterLevel(n0),n0)))
| ~ spl11_1620 ),
inference(avatar_component_clause,[],[f125561]) ).
fof(f135992,plain,
spl11_1536,
inference(avatar_split_clause,[],[f13359,f123425]) ).
fof(f136664,plain,
( n0 = plus(n1,plus(n1,n0))
| ~ spl11_1536
| ~ spl11_1620 ),
inference(forward_demodulation,[],[f125563,f123427]) ).
fof(f136898,plain,
( n0 = plus(n1,n1)
| ~ spl11_1536
| ~ spl11_1620 ),
inference(forward_demodulation,[],[f136664,f327]) ).
fof(f138265,plain,
( n0 = n2
| ~ spl11_1536
| ~ spl11_1620 ),
inference(superposition,[],[f136898,f156]) ).
fof(f138921,plain,
( $false
| spl11_2
| ~ spl11_1536
| ~ spl11_1620 ),
inference(forward_subsumption_resolution,[],[f138265,f358]) ).
fof(f138922,plain,
( spl11_2
| ~ spl11_1536
| ~ spl11_1620 ),
inference(avatar_contradiction_clause,[],[f138921]) ).
fof(f139214,plain,
( n0 != plus(n1,plus(n1,n0))
| ~ spl11_1536
| spl11_1620 ),
inference(forward_demodulation,[],[f125562,f123427]) ).
fof(f139218,plain,
( n0 != plus(n1,n1)
| ~ spl11_1536
| spl11_1620 ),
inference(forward_demodulation,[],[f139214,f327]) ).
fof(f146366,plain,
( n1 = sK1(n0,filling,n2)
| n0 = sK1(n0,filling,n2)
| spl11_251 ),
inference(resolution,[],[f18100,f4082]) ).
fof(f146372,plain,
( n1 = sK1(n0,filling,n2)
| spl11_251
| spl11_255 ),
inference(forward_subsumption_resolution,[],[f146366,f4102]) ).
fof(f146461,plain,
( ! [X0] :
( ~ happens(X0,plus(n1,n1))
| n0 = plus(n1,n1)
| stoppedIn(n0,filling,n2) )
| spl11_251
| spl11_255 ),
inference(superposition,[],[f3412,f146372]) ).
fof(f146544,plain,
( ! [X0] :
( ~ happens(X0,plus(n1,n1))
| stoppedIn(n0,filling,n2) )
| spl11_251
| spl11_255
| ~ spl11_1536
| spl11_1620 ),
inference(forward_subsumption_resolution,[],[f146461,f139218]) ).
fof(f146641,plain,
( ! [X0] : ~ happens(X0,plus(n1,n1))
| spl11_251
| spl11_255
| ~ spl11_1536
| spl11_1620 ),
inference(forward_subsumption_resolution,[],[f146544,f4082]) ).
fof(f146710,plain,
( ! [X0] : ~ happens(X0,n2)
| spl11_251
| spl11_255
| ~ spl11_1536
| spl11_1620 ),
inference(forward_demodulation,[],[f146641,f156]) ).
fof(f146742,plain,
( spl11_57
| spl11_251
| spl11_255
| ~ spl11_1536
| spl11_1620 ),
inference(avatar_split_clause,[],[f146710,f125561,f123425,f4101,f4080,f1110]) ).
cnf(s3,plain,
~ spl11_2,
inference(sat_conversion,[],[f442]) ).
cnf(s59,plain,
~ spl11_11,
inference(sat_conversion,[],[f1256]) ).
cnf(s65,plain,
~ spl11_57,
inference(sat_conversion,[],[f1291]) ).
cnf(s105,plain,
( spl11_2
| ~ spl11_74 ),
inference(sat_conversion,[],[f1829]) ).
cnf(s316,plain,
( spl11_74
| spl11_250
| ~ spl11_251 ),
inference(sat_conversion,[],[f4083]) ).
cnf(s366,plain,
( ~ spl11_250
| spl11_277 ),
inference(sat_conversion,[],[f4899]) ).
cnf(s385,plain,
( spl11_2
| spl11_57
| spl11_101
| ~ spl11_277 ),
inference(sat_conversion,[],[f5174]) ).
cnf(s674,plain,
~ spl11_101,
inference(sat_conversion,[],[f10008]) ).
cnf(s1840,plain,
( spl11_11
| spl11_251
| ~ spl11_255 ),
inference(sat_conversion,[],[f29629]) ).
cnf(s4547,plain,
spl11_1536,
inference(sat_conversion,[],[f135992]) ).
cnf(s4628,plain,
( spl11_2
| ~ spl11_1536
| ~ spl11_1620 ),
inference(sat_conversion,[],[f138922]) ).
cnf(s4915,plain,
( spl11_57
| spl11_251
| spl11_255
| ~ spl11_1536
| spl11_1620 ),
inference(sat_conversion,[],[f146742]) ).
cnf(s5057,plain,
( spl11_2
| spl11_57
| ~ spl11_277 ),
inference(rat,[],[s385,s674]) ).
cnf(s5174,plain,
~ spl11_1620,
inference(rat,[],[s4628,s4547,s3]) ).
cnf(s5178,plain,
~ spl11_277,
inference(rat,[],[s5057,s65,s3]) ).
cnf(s5180,plain,
~ spl11_74,
inference(rat,[],[s105,s3]) ).
cnf(s5185,plain,
~ spl11_250,
inference(rat,[],[s366,s5178]) ).
cnf(s5205,plain,
~ spl11_251,
inference(rat,[],[s316,s5180,s5185]) ).
cnf(s5209,plain,
spl11_255,
inference(rat,[],[s4915,s5174,s4547,s65,s5205]) ).
cnf(s5214,plain,
$false,
inference(rat,[],[s1840,s59,s5209,s5205]) ).
fof(f146752,plain,
$false,
inference(avatar_sat_refutation,[],[s5214]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR013+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.19 % Computer : n026.cluster.edu
% 0.11/0.19 % Model : x86_64 x86_64
% 0.11/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.19 % Memory : 8046.5625MB
% 0.11/0.19 % OS : Linux 6.8.0-71-generic
% 0.11/0.19 % CPULimit : 300
% 0.11/0.19 % WCLimit : 300
% 0.11/0.19 % DateTime : Mon Sep 28 22:08:42 UTC 2026
% 0.11/0.19 % CPUTime :
% 0.11/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.22 Running first-order model finding
% 0.11/0.22 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
% 16.60/2.64 % (140291)Will run a generic schedule for satisfiability detection.
% 16.60/2.64 % (140304)dis+10_1_sil=32000:sp=arity:random_seed=2961895109:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.60/2.64 % (140302)% WARNING: option uhcvi not known.
% 16.60/2.64 % (140307)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2847227357:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.60/2.64 % (140301)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=378831012_2999 on theBenchmark for (2999ds/0Mi)
% 16.60/2.64 % (140302)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1233316110:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.60/2.64 % (140306)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3144685115:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.60/2.64 % Detected minimum model sizes of [3]
% 16.60/2.64 % Detected maximum model sizes of [max]
% 16.60/2.64 % TRYING [3]
% 16.60/2.64 % (140305)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3505016957:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.60/2.64 % TRYING [4]
% 16.60/2.64 % (140303)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2758118242:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.60/2.64 % (140304)Instruction limit reached!
% 16.60/2.64 % (140304)------------------------------
% 16.60/2.64 % (140304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.60/2.64 % (140304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.60/2.64 % (140304)CaDiCaL version: 2.1.3
% 16.60/2.64 % (140304)Termination reason: Instruction limit
% 16.60/2.64 % (140304)Termination phase: Saturation
% 16.60/2.64 % (140304)Time elapsed: 0.034 s
% 16.60/2.64 % (140304)Peak memory usage: 12 MB
% 16.60/2.64 % (140304)Instructions burned: 104 (million)
% 16.60/2.64 % TRYING [5]
% 16.60/2.64 % (140319)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2969234704:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.60/2.64 % Detected minimum model sizes of [3]
% 16.60/2.64 % Detected maximum model sizes of [max]
% 16.60/2.64 % TRYING [3]
% 16.60/2.64 % TRYING [4]
% 16.60/2.64 % TRYING [5]
% 16.60/2.64 % TRYING [6]
% 16.60/2.64 % TRYING [6]
% 16.60/2.64 % (140307)Instruction limit reached!
% 16.60/2.64 % (140307)------------------------------
% 16.60/2.64 % (140307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.60/2.64 % (140307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.60/2.64 % (140307)CaDiCaL version: 2.1.3
% 16.60/2.64 % (140307)Termination reason: Instruction limit
% 16.60/2.64 % (140307)Termination phase: Saturation
% 16.60/2.64 % (140307)Time elapsed: 0.091 s
% 16.60/2.64 % (140307)Peak memory usage: 13 MB
% 16.60/2.64 % (140307)Instructions burned: 159 (million)
% 16.60/2.64 % (140306)Instruction limit reached!
% 16.60/2.64 % (140306)------------------------------
% 16.60/2.64 % (140306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.60/2.64 % (140306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.60/2.64 % (140306)CaDiCaL version: 2.1.3
% 16.60/2.64 % (140306)Termination reason: Instruction limit
% 16.60/2.64 % (140306)Termination phase: Saturation
% 16.60/2.64 % (140306)Time elapsed: 0.108 s
% 16.60/2.64 % (140306)Peak memory usage: 12 MB
% 16.60/2.64 % (140306)Instructions burned: 131 (million)
% 16.60/2.64 % (140321)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2690491525:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.60/2.64 % (140305)Instruction limit reached!
% 16.60/2.64 % (140305)------------------------------
% 16.60/2.64 % (140305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.60/2.64 % (140305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.60/2.64 % (140305)CaDiCaL version: 2.1.3
% 16.60/2.64 % (140305)Termination reason: Instruction limit
% 16.60/2.64 % (140305)Termination phase: Saturation
% 16.60/2.64 % (140305)Time elapsed: 0.109 s
% 16.60/2.64 % (140305)Peak memory usage: 12 MB
% 16.60/2.64 % (140305)Instructions burned: 116 (million)
% 16.60/2.64 % (140323)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=2479187931:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.60/2.64 % (140324)ott-21_1_sil=16000:fs=off:random_seed=4249608007:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.60/2.64 % TRYING [7]
% 16.60/2.64 % TRYING [7]
% 16.60/2.64 % (140319)Instruction limit reached!
% 16.60/2.64 % (140319)------------------------------
% 44.96/6.63 % (140319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.96/6.63 % (140319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.96/6.63 % (140319)CaDiCaL version: 2.1.3
% 44.96/6.63 % (140319)Termination reason: Instruction limit
% 44.96/6.63 % (140319)Termination phase: Finite model building constraint generation
% 44.96/6.63 % (140319)Time elapsed: 0.144 s
% 44.96/6.63 % (140319)Peak memory usage: 28 MB
% 44.96/6.63 % (140319)Instructions burned: 717 (million)
% 44.96/6.63 % (140321)Instruction limit reached!
% 44.96/6.63 % (140321)------------------------------
% 44.96/6.63 % (140321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.96/6.63 % (140321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.96/6.63 % (140321)CaDiCaL version: 2.1.3
% 44.96/6.63 % (140321)Termination reason: Instruction limit
% 44.96/6.63 % (140321)Termination phase: Saturation
% 44.96/6.63 % (140321)Time elapsed: 0.087 s
% 44.96/6.63 % (140321)Peak memory usage: 12 MB
% 44.96/6.63 % (140321)Instructions burned: 131 (million)
% 44.96/6.63 % (140327)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=951320059:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 44.96/6.63 % (140328)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1027445117:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 44.96/6.63 % (140324)Instruction limit reached!
% 44.96/6.63 % (140324)------------------------------
% 44.96/6.63 % (140324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.96/6.63 % (140324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.96/6.63 % (140324)CaDiCaL version: 2.1.3
% 44.96/6.63 % (140324)Termination reason: Instruction limit
% 44.96/6.63 % (140324)Termination phase: Saturation
% 44.96/6.63 % (140324)Time elapsed: 0.094 s
% 44.96/6.63 % (140324)Peak memory usage: 13 MB
% 44.96/6.63 % (140324)Instructions burned: 182 (million)
% 44.96/6.63 % Detected minimum model sizes of [3]
% 44.96/6.63 % Detected maximum model sizes of [max]
% 44.96/6.63 % TRYING [3]
% 44.96/6.63 % (140331)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4279092933:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 44.96/6.63 % TRYING [4]
% 44.96/6.63 % TRYING [5]
% 44.96/6.63 % TRYING [8]
% 44.96/6.63 % TRYING [6]
% 44.96/6.63 % (140328)Instruction limit reached!
% 44.96/6.63 % (140328)------------------------------
% 44.96/6.63 % (140328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.96/6.63 % (140328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.96/6.63 % (140328)CaDiCaL version: 2.1.3
% 44.96/6.63 % (140328)Termination reason: Instruction limit
% 44.96/6.63 % (140328)Termination phase: Finite model building SAT solving
% 44.96/6.63 % (140328)Time elapsed: 0.188 s
% 44.96/6.63 % (140328)Peak memory usage: 25 MB
% 44.96/6.63 % (140328)Instructions burned: 868 (million)
% 44.96/6.63 % (140333)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2179187209:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 44.96/6.63 % (140323)Instruction limit reached!
% 44.96/6.63 % (140323)------------------------------
% 44.96/6.63 % (140323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.96/6.63 % (140323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.96/6.63 % (140323)CaDiCaL version: 2.1.3
% 44.96/6.63 % (140323)Termination reason: Instruction limit
% 44.96/6.63 % (140323)Termination phase: Saturation
% 44.96/6.63 % (140323)Time elapsed: 0.348 s
% 44.96/6.63 % (140323)Peak memory usage: 14 MB
% 44.96/6.63 % (140323)Instructions burned: 686 (million)
% 44.96/6.63 % (140335)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=3119002503: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)
% 44.96/6.63 % TRYING [14]
% 44.96/6.63 % (140327)Instruction limit reached!
% 44.96/6.63 % (140327)------------------------------
% 44.96/6.63 % (140327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.96/6.63 % (140327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.96/6.63 % (140327)CaDiCaL version: 2.1.3
% 44.96/6.63 % (140327)Termination reason: Instruction limit
% 44.96/6.63 % (140327)Termination phase: Saturation
% 44.96/6.63 % (140327)Time elapsed: 0.312 s
% 44.96/6.63 % (140327)Peak memory usage: 13 MB
% 44.96/6.63 % (140327)Instructions burned: 478 (million)
% 44.96/6.63 % TRYING [9]
% 44.96/6.63 % (140337)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=271683338:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 61.64/9.15 % (140333)Instruction limit reached!
% 61.64/9.15 % (140333)------------------------------
% 61.64/9.15 % (140333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.64/9.15 % (140333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.64/9.15 % (140333)CaDiCaL version: 2.1.3
% 61.64/9.15 % (140333)Termination reason: Instruction limit
% 61.64/9.15 % (140333)Termination phase: Finite model building constraint generation
% 61.64/9.15 % (140333)Time elapsed: 0.193 s
% 61.64/9.15 % (140333)Peak memory usage: 79 MB
% 61.64/9.15 % (140333)Instructions burned: 890 (million)
% 61.64/9.15 % (140347)fmb+10_1_sil=64000:random_seed=3298873068:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 61.64/9.15 % Detected minimum model sizes of [3]
% 61.64/9.15 % Detected maximum model sizes of [max]
% 61.64/9.15 % TRYING [3]
% 61.64/9.15 % TRYING [4]
% 61.64/9.15 % TRYING [5]
% 61.64/9.15 % TRYING [6]
% 61.64/9.15 % TRYING [7]
% 61.64/9.15 % (140335)Instruction limit reached!
% 61.64/9.15 % (140335)------------------------------
% 61.64/9.15 % (140335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.64/9.15 % (140335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.64/9.15 % (140335)CaDiCaL version: 2.1.3
% 61.64/9.15 % (140335)Termination reason: Instruction limit
% 61.64/9.15 % (140335)Termination phase: Saturation
% 61.64/9.15 % (140335)Time elapsed: 0.539 s
% 61.64/9.15 % (140335)Peak memory usage: 16 MB
% 61.64/9.15 % (140335)Instructions burned: 692 (million)
% 61.64/9.15 % (140357)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=653608181:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 61.64/9.15 % Detected minimum model sizes of [3]
% 61.64/9.15 % Detected maximum model sizes of [max]
% 61.64/9.15 % TRYING [20]
% 61.64/9.15 % (140331)Instruction limit reached!
% 61.64/9.15 % (140331)------------------------------
% 61.64/9.15 % (140331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.64/9.15 % (140331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.64/9.15 % (140331)CaDiCaL version: 2.1.3
% 61.64/9.15 % (140331)Termination reason: Instruction limit
% 61.64/9.15 % (140331)Termination phase: Saturation
% 61.64/9.15 % (140331)Time elapsed: 0.864 s
% 61.64/9.15 % (140331)Peak memory usage: 20 MB
% 61.64/9.15 % (140331)Instructions burned: 1179 (million)
% 61.64/9.15 % (140359)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2131617837:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 61.64/9.15 % Detected minimum model sizes of [3]
% 61.64/9.15 % Detected maximum model sizes of [max]
% 61.64/9.15 % TRYING [8]
% 61.64/9.15 % TRYING [8]
% 61.64/9.15 % TRYING [10]
% 61.64/9.15 % (140337)Instruction limit reached!
% 61.64/9.15 % (140337)------------------------------
% 61.64/9.15 % (140337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.64/9.15 % (140337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.64/9.15 % (140337)CaDiCaL version: 2.1.3
% 61.64/9.15 % (140337)Termination reason: Instruction limit
% 61.64/9.15 % (140337)Termination phase: Saturation
% 61.64/9.15 % (140337)Time elapsed: 0.772 s
% 61.64/9.15 % (140337)Peak memory usage: 18 MB
% 61.64/9.15 % (140337)Instructions burned: 882 (million)
% 61.64/9.15 % (140364)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2034960609:i=5131_2986 on theBenchmark for (2986ds/5131Mi)
% 61.64/9.15 % TRYING [9]
% 61.64/9.15 % (140359)Instruction limit reached!
% 61.64/9.15 % (140359)------------------------------
% 61.64/9.15 % (140359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.64/9.15 % (140359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.64/9.15 % (140359)CaDiCaL version: 2.1.3
% 61.64/9.15 % (140359)Termination reason: Instruction limit
% 61.64/9.15 % (140359)Termination phase: Finite model building constraint generation
% 61.64/9.15 % (140359)Time elapsed: 0.406 s
% 61.64/9.15 % (140359)Peak memory usage: 52 MB
% 61.64/9.15 % (140359)Instructions burned: 923 (million)
% 61.64/9.15 % (140367)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4150270996:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi)
% 61.64/9.15 % TRYING [9]
% 61.64/9.15 % TRYING [11]
% 61.64/9.15 % TRYING [10]
% 61.64/9.15 % (140367)Instruction limit reached!
% 61.64/9.15 % (140367)------------------------------
% 61.64/9.15 % (140367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 61.64/9.15 % (140367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.64/9.15 % (140367)CaDiCaL version: 2.1.3
% 67.62/9.99 % (140367)Termination reason: Instruction limit
% 67.62/9.99 % (140367)Termination phase: Saturation
% 67.62/9.99 % (140367)Time elapsed: 0.793 s
% 67.62/9.99 % (140367)Peak memory usage: 27 MB
% 67.62/9.99 % (140367)Instructions burned: 1473 (million)
% 67.62/9.99 % (140521)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4097232213:i=6324_2975 on theBenchmark for (2975ds/6324Mi)
% 67.62/9.99 % Detected minimum model sizes of [3]
% 67.62/9.99 % Detected maximum model sizes of [max]
% 67.62/9.99 % TRYING [77]
% 67.62/9.99 % TRYING [12]
% 67.62/9.99 % TRYING [11]
% 67.62/9.99 % (140364)Instruction limit reached!
% 67.62/9.99 % (140364)------------------------------
% 67.62/9.99 % (140364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.62/9.99 % (140364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.62/9.99 % (140364)CaDiCaL version: 2.1.3
% 67.62/9.99 % (140364)Termination reason: Instruction limit
% 67.62/9.99 % (140364)Termination phase: Saturation
% 67.62/9.99 % (140364)Time elapsed: 2.767 s
% 67.62/9.99 % (140364)Peak memory usage: 24 MB
% 67.62/9.99 % (140364)Instructions burned: 5133 (million)
% 67.62/9.99 % (140523)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4190131425:fmbsr=2.30978:i=2174_2958 on theBenchmark for (2958ds/2174Mi)
% 67.62/9.99 % Detected minimum model sizes of [3]
% 67.62/9.99 % Detected maximum model sizes of [max]
% 67.62/9.99 % TRYING [16]
% 67.62/9.99 % (140357)Instruction limit reached!
% 67.62/9.99 % (140357)------------------------------
% 67.62/9.99 % (140357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.62/9.99 % (140357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.62/9.99 % (140357)CaDiCaL version: 2.1.3
% 67.62/9.99 % (140357)Termination reason: Instruction limit
% 67.62/9.99 % (140357)Termination phase: Finite model building constraint generation
% 67.62/9.99 % (140357)Time elapsed: 3.506 s
% 67.62/9.99 % (140357)Peak memory usage: 611 MB
% 67.62/9.99 % (140357)Instructions burned: 9516 (million)
% 67.62/9.99 % (140525)ott-2_1_sil=16000:newcnf=on:random_seed=1412802347:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2953 on theBenchmark for (2953ds/869Mi)
% 67.62/9.99 % (140521)Instruction limit reached!
% 67.62/9.99 % (140521)------------------------------
% 67.62/9.99 % (140521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.62/9.99 % (140521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.62/9.99 % (140521)CaDiCaL version: 2.1.3
% 67.62/9.99 % (140521)Termination reason: Instruction limit
% 67.62/9.99 % (140521)Termination phase: Finite model building constraint generation
% 67.62/9.99 % (140521)Time elapsed: 2.363 s
% 67.62/9.99 % (140521)Peak memory usage: 515 MB
% 67.62/9.99 % (140521)Instructions burned: 6326 (million)
% 67.62/9.99 % TRYING [12]
% 67.62/9.99 % (140527)ott+10_1_sil=32000:tgt=ground:random_seed=2778503395:i=5114:av=off_2951 on theBenchmark for (2951ds/5114Mi)
% 67.62/9.99 % (140523)Instruction limit reached!
% 67.62/9.99 % (140523)------------------------------
% 67.62/9.99 % (140523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.62/9.99 % (140523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.62/9.99 % (140523)CaDiCaL version: 2.1.3
% 67.62/9.99 % (140523)Termination reason: Instruction limit
% 67.62/9.99 % (140523)Termination phase: Finite model building constraint generation
% 67.62/9.99 % (140523)Time elapsed: 0.742 s
% 67.62/9.99 % (140523)Peak memory usage: 134 MB
% 67.62/9.99 % (140523)Instructions burned: 2177 (million)
% 67.62/9.99 % (140529)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=336675203:i=54282_2950 on theBenchmark for (2950ds/54282Mi)
% 67.62/9.99 % Detected minimum model sizes of [3]
% 67.62/9.99 % Detected maximum model sizes of [max]
% 67.62/9.99 % TRYING [3]
% 67.62/9.99 % TRYING [4]
% 67.62/9.99 % TRYING [13]
% 67.62/9.99 % TRYING [5]
% 67.62/9.99 % TRYING [6]
% 67.62/9.99 % TRYING [7]
% 67.62/9.99 % (140525)Instruction limit reached!
% 67.62/9.99 % (140525)------------------------------
% 67.62/9.99 % (140525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.62/9.99 % (140525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.62/9.99 % (140525)CaDiCaL version: 2.1.3
% 67.62/9.99 % (140525)Termination reason: Instruction limit
% 67.62/9.99 % (140525)Termination phase: Saturation
% 67.62/9.99 % (140525)Time elapsed: 0.458 s
% 67.62/9.99 % (140525)Peak memory usage: 15 MB
% 67.62/9.99 % (140525)Instructions burned: 870 (million)
% 67.62/9.99 % (140531)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=714075518:i=3512:aac=none_2948 on theBenchmark for (2948ds/3512Mi)
% 67.62/9.99 % TRYING [8]
% 67.62/9.99 % TRYING [9]
% 67.62/9.99 % TRYING [10]
% 67.62/9.99 % (140347)Instruction limit reached!
% 67.62/9.99 % (140347)------------------------------
% 67.62/9.99 % (140347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.62/9.99 % (140347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.62/9.99 % (140347)CaDiCaL version: 2.1.3
% 67.62/9.99 % (140347)Termination reason: Instruction limit
% 67.62/9.99 % (140347)Termination phase: Finite model building SAT solving
% 67.62/9.99 % (140347)Time elapsed: 5.707 s
% 67.62/9.99 % (140347)Peak memory usage: 232 MB
% 67.62/9.99 % (140347)Instructions burned: 22065 (million)
% 67.62/9.99 % (140533)dis+21_1_sil=32000:sas=cadical:random_seed=626018637:i=3773:amm=off_2935 on theBenchmark for (2935ds/3773Mi)
% 67.62/9.99 % TRYING [11]
% 67.62/9.99 % (140531)Instruction limit reached!
% 67.62/9.99 % (140531)------------------------------
% 67.62/9.99 % (140531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.62/9.99 % (140531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.62/9.99 % (140531)CaDiCaL version: 2.1.3
% 67.62/9.99 % (140531)Termination reason: Instruction limit
% 67.62/9.99 % (140531)Termination phase: Saturation
% 67.62/9.99 % (140531)Time elapsed: 1.936 s
% 67.62/9.99 % (140531)Peak memory usage: 28 MB
% 67.62/9.99 % (140531)Instructions burned: 3514 (million)
% 67.62/9.99 % (140535)ott+11_1_sil=16000:gs=on:random_seed=2040729667:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2928 on theBenchmark for (2928ds/2251Mi)
% 67.62/9.99 % TRYING [14]
% 67.62/9.99 % (140527)Instruction limit reached!
% 67.62/9.99 % (140527)------------------------------
% 67.62/9.99 % (140527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.62/9.99 % (140527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.62/9.99 % (140527)CaDiCaL version: 2.1.3
% 67.62/9.99 % (140527)Termination reason: Instruction limit
% 67.62/9.99 % (140527)Termination phase: Saturation
% 67.62/9.99 % (140527)Time elapsed: 2.661 s
% 67.62/9.99 % (140527)Peak memory usage: 25 MB
% 67.62/9.99 % (140527)Instructions burned: 5115 (million)
% 67.62/9.99 % (140537)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2445322972:fmbsr=1.6:i=67534_2924 on theBenchmark for (2924ds/67534Mi)
% 67.62/9.99 % Detected minimum model sizes of [3]
% 67.62/9.99 % Detected maximum model sizes of [max]
% 67.62/9.99 % TRYING [7]
% 67.62/9.99 % (140533)Instruction limit reached!
% 67.62/9.99 % (140533)------------------------------
% 67.62/9.99 % (140533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.62/9.99 % (140533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.62/9.99 % (140533)CaDiCaL version: 2.1.3
% 67.62/9.99 % (140533)Termination reason: Instruction limit
% 67.62/9.99 % (140533)Termination phase: Saturation
% 67.62/9.99 % (140533)Time elapsed: 1.145 s
% 67.62/9.99 % (140533)Peak memory usage: 26 MB
% 67.62/9.99 % (140533)Instructions burned: 3776 (million)
% 67.62/9.99 % (140539)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3805298029:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2924 on theBenchmark for (2924ds/4591Mi)
% 67.62/9.99 % TRYING [12]
% 67.62/9.99 % TRYING [8]
% 67.62/9.99 % (140535)Instruction limit reached!
% 67.62/9.99 % (140535)------------------------------
% 67.62/9.99 % (140535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.62/9.99 % (140535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.62/9.99 % (140535)CaDiCaL version: 2.1.3
% 67.62/9.99 % (140535)Termination reason: Instruction limit
% 67.62/9.99 % (140535)Termination phase: Saturation
% 67.62/9.99 % (140535)Time elapsed: 1.415 s
% 67.62/9.99 % (140535)Peak memory usage: 27 MB
% 67.62/9.99 % (140535)Instructions burned: 2252 (million)
% 67.62/9.99 % (140541)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2378187445:i=29340_2914 on theBenchmark for (2914ds/29340Mi)
% 67.62/9.99 % (140539)Instruction limit reached!
% 67.62/9.99 % (140539)------------------------------
% 67.62/9.99 % (140539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.62/9.99 % (140539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.62/9.99 % (140539)CaDiCaL version: 2.1.3
% 67.62/9.99 % (140539)Termination reason: Instruction limit
% 67.62/9.99 % (140539)Termination phase: Saturation
% 67.62/9.99 % (140539)Time elapsed: 1.303 s
% 67.62/9.99 % (140539)Peak memory usage: 48 MB
% 67.62/9.99 % (140539)Instructions burned: 4594 (million)
% 67.62/9.99 % (140543)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2755551865:i=5211_2910 on theBenchmark for (2910ds/5211Mi)
% 67.62/9.99 % TRYING [9]
% 67.62/9.99 % TRYING [13]
% 67.62/9.99 % (140302) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-140291-140302"...
% 67.62/9.99 % (140302)...printing done.
% 67.62/9.99 % (140302)Refutation found. Thanks to Tanya!
% 67.62/9.99 % SZS status Theorem for theBenchmark
% 67.62/9.99 % SZS output start Proof for theBenchmark
% See solution above
% 67.62/9.99 % (140302)------------------------------
% 67.62/9.99 % (140302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.62/9.99 % (140302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.62/9.99 % (140302)CaDiCaL version: 2.1.3
% 67.62/9.99 % (140302)Termination reason: Refutation
% 67.62/9.99 % (140302)Time elapsed: 9.650 s
% 67.62/9.99 % (140302)Peak memory usage: 48 MB
% 67.62/9.99 % (140302)Instructions burned: 17945 (million)
% 67.62/9.99 % (140291)Success in time 9.76 s
% 67.62/9.99 % Vampire exiting
%------------------------------------------------------------------------------