%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR002+2 : 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 : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:44:18 AM UTC 2026
% Result : Theorem 3.19s 0.79s
% Output : Refutation 3.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 54
% Syntax : Number of formulae : 326 ( 80 unt; 22 def)
% Number of atoms : 872 ( 174 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 924 ( 378 ~; 403 |; 100 &)
% ( 34 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 34 ( 32 usr; 21 prp; 0-4 aty)
% Number of functors : 16 ( 16 usr; 10 con; 0-3 aty)
% Number of variables : 309 ( 0 sgn 290 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( stoppedIn(X0,X1,X2)
<=> ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) ) ),
file('/export/starexec/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(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/sandbox/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/sandbox/benchmark/Axioms/CSR001+0.ax',keep_not_released) ).
fof(f9,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& initiates(X0,X2,X1) )
=> holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_holds) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& terminates(X0,X2,X1) )
=> ~ holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_terminates_not_holds) ).
fof(f12,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& ( initiates(X0,X2,X1)
| terminates(X0,X2,X1) ) )
=> ~ releasedAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_not_released) ).
fof(f13,axiom,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = overflow
& X1 = waterLevel(X3) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',initiates_all_defn) ).
fof(f14,axiom,
! [X0,X1,X2] :
( terminates(X0,X1,X2)
<=> ( ( X0 = tapOff
& X1 = filling )
| ( X0 = overflow
& X1 = filling ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',terminates_all_defn) ).
fof(f16,axiom,
! [X0,X1] :
( happens(X0,X1)
<=> ( ( X0 = tapOn
& X1 = n0 )
| ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow ) ) ),
file('/export/starexec/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(f19,axiom,
tapOff != tapOn,
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',tapOff_not_tapOn) ).
fof(f21,axiom,
overflow != tapOn,
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',overflow_not_tapOn) ).
fof(f27,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus0_1) ).
fof(f29,axiom,
plus(n0,n3) = n3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus0_3) ).
fof(f30,axiom,
plus(n1,n1) = n2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus1_1) ).
fof(f31,axiom,
plus(n1,n2) = n3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus1_2) ).
fof(f32,axiom,
plus(n1,n3) = n4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus1_3) ).
fof(f33,axiom,
plus(n2,n2) = n4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus2_2) ).
fof(f36,axiom,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_of_plus) ).
fof(f37,axiom,
! [X0,X1] :
( less_or_equal(X0,X1)
<=> ( less(X0,X1)
| X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_or_equal) ).
fof(f38,axiom,
~ ? [X0] : less(X0,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less0) ).
fof(f39,axiom,
! [X0] :
( less(X0,n1)
<=> less_or_equal(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less1) ).
fof(f40,axiom,
! [X0] :
( less(X0,n2)
<=> less_or_equal(X0,n1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less2) ).
fof(f41,axiom,
! [X0] :
( less(X0,n3)
<=> less_or_equal(X0,n2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less3) ).
fof(f42,axiom,
! [X0] :
( less(X0,n4)
<=> less_or_equal(X0,n3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less4) ).
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(f50,axiom,
~ holdsAt(filling,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_filling_0) ).
fof(f55,axiom,
holdsAt(waterLevel(n3),n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',waterLevel_3) ).
fof(f56,conjecture,
~ holdsAt(filling,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_filling_4) ).
fof(f57,negated_conjecture,
~ ~ holdsAt(filling,n4),
inference(negated_conjecture,[status(cth)],[f56]) ).
fof(f58,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) )
| ? [X4] :
( holdsAt(waterLevel(X4),X2)
& X0 = overflow
& waterLevel(X4) = X1 ) ) ),
inference(rectify,[],[f13]) ).
fof(f59,plain,
holdsAt(filling,n4),
inference(flattening,[],[f57]) ).
fof(f61,plain,
! [X0,X1,X2] :
( stoppedIn(X0,X1,X2)
=> ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) ) ),
inference(unused_predicate_definition_removal,[],[f1]) ).
fof(f64,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) )
| ~ stoppedIn(X0,X1,X2) ),
inference(ennf_transformation,[],[f61]) ).
fof(f65,plain,
! [X0,X1,X2,X3,X4] :
( holdsAt(X3,plus(X1,X4))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1)
| ~ less(n0,X4)
| ~ trajectory(X2,X1,X3,X4)
| stoppedIn(X1,X2,plus(X1,X4)) ),
inference(ennf_transformation,[],[f3]) ).
fof(f66,plain,
! [X0,X1,X2,X3,X4] :
( holdsAt(X3,plus(X1,X4))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1)
| ~ less(n0,X4)
| ~ trajectory(X2,X1,X3,X4)
| stoppedIn(X1,X2,plus(X1,X4)) ),
inference(flattening,[],[f65]) ).
fof(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(ennf_transformation,[],[f6]) ).
fof(f70,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,[],[f69]) ).
fof(f73,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f74,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(flattening,[],[f73]) ).
fof(f75,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f76,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(flattening,[],[f75]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f78,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(flattening,[],[f77]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(flattening,[],[f81]) ).
fof(f83,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(ennf_transformation,[],[f17]) ).
fof(f84,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(flattening,[],[f83]) ).
fof(f85,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f86,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(flattening,[],[f85]) ).
fof(f87,plain,
! [X0] : ~ less(X0,n0),
inference(ennf_transformation,[],[f38]) ).
fof(f88,definition,
! [X2,X0,X1] :
( sP0(X2,X0,X1)
<=> ? [X4] :
( holdsAt(waterLevel(X4),X2)
& X0 = overflow
& waterLevel(X4) = X1 ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f89,definition,
! [X2,X0,X1] :
( sP1(X2,X0,X1)
<=> ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f90,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| sP1(X2,X0,X1)
| sP0(X2,X0,X1) ) ),
inference(definition_folding,[],[f58,f89,f88]) ).
fof(f91,plain,
! [X0,X1,X2] :
( ( happens(sK2(X0,X1,X2),sK3(X0,X1,X2))
& less(X0,sK3(X0,X1,X2))
& less(sK3(X0,X1,X2),X2)
& terminates(sK2(X0,X1,X2),X1,sK3(X0,X1,X2)) )
| ~ stoppedIn(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X3,sK2(X0,X1,X2)),skolemize(X4,sK3(X0,X1,X2))],[f64]) ).
fof(f93,plain,
! [X0,X1] :
( ~ holdsAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ( happens(sK5(X0,X1),X1)
& initiates(sK5(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X2,sK5(X0,X1))],[f70]) ).
fof(f95,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ( happens(sK7(X0,X1),X1)
& releases(sK7(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f74]) ).
fof(f102,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ( ( tapOn != X0
| filling != X1 )
& ( overflow != X0
| spilling != X1 )
& ~ sP1(X2,X0,X1)
& ~ sP0(X2,X0,X1) ) )
& ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| sP1(X2,X0,X1)
| sP0(X2,X0,X1)
| ~ initiates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f90]) ).
fof(f103,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ( ( tapOn != X0
| filling != X1 )
& ( overflow != X0
| spilling != X1 )
& ~ sP1(X2,X0,X1)
& ~ sP0(X2,X0,X1) ) )
& ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| sP1(X2,X0,X1)
| sP0(X2,X0,X1)
| ~ initiates(X0,X1,X2) ) ),
inference(flattening,[],[f102]) ).
fof(f104,plain,
! [X0,X1,X2] :
( ( terminates(X0,X1,X2)
| ( ( tapOff != X0
| filling != X1 )
& ( overflow != X0
| filling != X1 ) ) )
& ( ( X0 = tapOff
& X1 = filling )
| ( X0 = overflow
& X1 = filling )
| ~ terminates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f14]) ).
fof(f105,plain,
! [X0,X1,X2] :
( ( terminates(X0,X1,X2)
| ( ( tapOff != X0
| filling != X1 )
& ( overflow != X0
| filling != X1 ) ) )
& ( ( X0 = tapOff
& X1 = filling )
| ( X0 = overflow
& X1 = filling )
| ~ terminates(X0,X1,X2) ) ),
inference(flattening,[],[f104]) ).
fof(f109,plain,
! [X0,X1] :
( ( happens(X0,X1)
| ( ( tapOn != X0
| n0 != X1 )
& ( ~ holdsAt(waterLevel(n3),X1)
| ~ holdsAt(filling,X1)
| overflow != X0 ) ) )
& ( ( X0 = tapOn
& X1 = n0 )
| ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow )
| ~ happens(X0,X1) ) ),
inference(nnf_transformation,[],[f16]) ).
fof(f110,plain,
! [X0,X1] :
( ( happens(X0,X1)
| ( ( tapOn != X0
| n0 != X1 )
& ( ~ holdsAt(waterLevel(n3),X1)
| ~ holdsAt(filling,X1)
| overflow != X0 ) ) )
& ( ( X0 = tapOn
& X1 = n0 )
| ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow )
| ~ happens(X0,X1) ) ),
inference(flattening,[],[f109]) ).
fof(f112,plain,
! [X0,X1] :
( ( less_or_equal(X0,X1)
| ( ~ less(X0,X1)
& X0 != X1 ) )
& ( less(X0,X1)
| X0 = X1
| ~ less_or_equal(X0,X1) ) ),
inference(nnf_transformation,[],[f37]) ).
fof(f113,plain,
! [X0,X1] :
( ( less_or_equal(X0,X1)
| ( ~ less(X0,X1)
& X0 != X1 ) )
& ( less(X0,X1)
| X0 = X1
| ~ less_or_equal(X0,X1) ) ),
inference(flattening,[],[f112]) ).
fof(f114,plain,
! [X0] :
( ( less(X0,n1)
| ~ less_or_equal(X0,n0) )
& ( less_or_equal(X0,n0)
| ~ less(X0,n1) ) ),
inference(nnf_transformation,[],[f39]) ).
fof(f115,plain,
! [X0] :
( ( less(X0,n2)
| ~ less_or_equal(X0,n1) )
& ( less_or_equal(X0,n1)
| ~ less(X0,n2) ) ),
inference(nnf_transformation,[],[f40]) ).
fof(f116,plain,
! [X0] :
( ( less(X0,n3)
| ~ less_or_equal(X0,n2) )
& ( less_or_equal(X0,n2)
| ~ less(X0,n3) ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f117,plain,
! [X0] :
( ( less(X0,n4)
| ~ less_or_equal(X0,n3) )
& ( less_or_equal(X0,n3)
| ~ less(X0,n4) ) ),
inference(nnf_transformation,[],[f42]) ).
fof(f123,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(nnf_transformation,[],[f48]) ).
fof(f124,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(flattening,[],[f123]) ).
fof(f125,plain,
! [X2,X0,X1] :
( terminates(sK2(X0,X1,X2),X1,sK3(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f91]) ).
fof(f126,plain,
! [X2,X0,X1] :
( less(sK3(X0,X1,X2),X2)
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f91]) ).
fof(f128,plain,
! [X2,X0,X1] :
( happens(sK2(X0,X1,X2),sK3(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f91]) ).
fof(f129,plain,
! [X2,X3,X0,X1,X4] :
( ~ trajectory(X2,X1,X3,X4)
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1)
| ~ less(n0,X4)
| holdsAt(X3,plus(X1,X4))
| stoppedIn(X1,X2,plus(X1,X4)) ),
inference(cnf_transformation,[],[f66]) ).
fof(f133,plain,
! [X0,X1] :
( ~ holdsAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| happens(sK5(X0,X1),X1) ),
inference(cnf_transformation,[],[f93]) ).
fof(f137,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| happens(sK7(X0,X1),X1) ),
inference(cnf_transformation,[],[f95]) ).
fof(f138,plain,
! [X2,X0,X1] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(cnf_transformation,[],[f76]) ).
fof(f139,plain,
! [X2,X0,X1] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(cnf_transformation,[],[f78]) ).
fof(f141,plain,
! [X2,X0,X1] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(cnf_transformation,[],[f82]) ).
fof(f142,plain,
! [X2,X0,X1] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(cnf_transformation,[],[f82]) ).
fof(f158,plain,
! [X2,X0,X1] :
( initiates(X0,X1,X2)
| tapOn != X0
| filling != X1 ),
inference(cnf_transformation,[],[f103]) ).
fof(f162,plain,
! [X2,X0,X1] :
( ~ terminates(X0,X1,X2)
| overflow = X0
| tapOff = X0 ),
inference(cnf_transformation,[],[f105]) ).
fof(f163,plain,
! [X2,X0,X1] :
( terminates(X0,X1,X2)
| overflow != X0
| filling != X1 ),
inference(cnf_transformation,[],[f105]) ).
fof(f169,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| holdsAt(filling,X1)
| n0 = X1 ),
inference(cnf_transformation,[],[f110]) ).
fof(f170,plain,
! [X0,X1] :
( holdsAt(waterLevel(n3),X1)
| n0 = X1
| ~ happens(X0,X1) ),
inference(cnf_transformation,[],[f110]) ).
fof(f171,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| overflow = X0
| tapOn = X0 ),
inference(cnf_transformation,[],[f110]) ).
fof(f172,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| holdsAt(filling,X1)
| tapOn = X0 ),
inference(cnf_transformation,[],[f110]) ).
fof(f174,plain,
! [X0,X1] :
( happens(X0,X1)
| ~ holdsAt(waterLevel(n3),X1)
| ~ holdsAt(filling,X1)
| overflow != X0 ),
inference(cnf_transformation,[],[f110]) ).
fof(f175,plain,
! [X0,X1] :
( happens(X0,X1)
| tapOn != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f110]) ).
fof(f176,plain,
! [X2,X3,X0,X1] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(cnf_transformation,[],[f84]) ).
fof(f177,plain,
! [X2,X0,X1] :
( ~ holdsAt(waterLevel(X2),X0)
| ~ holdsAt(waterLevel(X1),X0)
| X1 = X2 ),
inference(cnf_transformation,[],[f86]) ).
fof(f178,plain,
tapOn != tapOff,
inference(cnf_transformation,[],[f19]) ).
fof(f180,plain,
tapOn != overflow,
inference(cnf_transformation,[],[f21]) ).
fof(f187,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f27]) ).
fof(f189,plain,
n3 = plus(n0,n3),
inference(cnf_transformation,[],[f29]) ).
fof(f190,plain,
n2 = plus(n1,n1),
inference(cnf_transformation,[],[f30]) ).
fof(f191,plain,
n3 = plus(n1,n2),
inference(cnf_transformation,[],[f31]) ).
fof(f192,plain,
plus(n1,n3) = n4,
inference(cnf_transformation,[],[f32]) ).
fof(f193,plain,
n4 = plus(n2,n2),
inference(cnf_transformation,[],[f33]) ).
fof(f196,plain,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[],[f36]) ).
fof(f197,plain,
! [X0,X1] :
( ~ less_or_equal(X0,X1)
| X0 = X1
| less(X0,X1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f198,plain,
! [X0,X1] :
( less_or_equal(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f113]) ).
fof(f199,plain,
! [X0,X1] :
( ~ less(X0,X1)
| less_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f200,plain,
! [X0] : ~ less(X0,n0),
inference(cnf_transformation,[],[f87]) ).
fof(f201,plain,
! [X0] :
( ~ less(X0,n1)
| less_or_equal(X0,n0) ),
inference(cnf_transformation,[],[f114]) ).
fof(f202,plain,
! [X0] :
( ~ less_or_equal(X0,n0)
| less(X0,n1) ),
inference(cnf_transformation,[],[f114]) ).
fof(f204,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| less(X0,n2) ),
inference(cnf_transformation,[],[f115]) ).
fof(f206,plain,
! [X0] :
( ~ less_or_equal(X0,n2)
| less(X0,n3) ),
inference(cnf_transformation,[],[f116]) ).
fof(f208,plain,
! [X0] :
( ~ less_or_equal(X0,n3)
| less(X0,n4) ),
inference(cnf_transformation,[],[f117]) ).
fof(f219,plain,
! [X0,X1] :
( X0 != X1
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f124]) ).
fof(f220,plain,
! [X0,X1] :
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f124]) ).
fof(f222,plain,
holdsAt(waterLevel(n0),n0),
inference(cnf_transformation,[],[f49]) ).
fof(f223,plain,
~ holdsAt(filling,n0),
inference(cnf_transformation,[],[f50]) ).
fof(f228,plain,
holdsAt(waterLevel(n3),n3),
inference(cnf_transformation,[],[f55]) ).
fof(f229,plain,
holdsAt(filling,n4),
inference(cnf_transformation,[],[f59]) ).
fof(f234,plain,
! [X2,X1] :
( initiates(tapOn,X1,X2)
| filling != X1 ),
inference(equality_resolution,[],[f158]) ).
fof(f235,plain,
! [X2] : initiates(tapOn,filling,X2),
inference(equality_resolution,[],[f234]) ).
fof(f240,plain,
! [X2,X1] :
( terminates(overflow,X1,X2)
| filling != X1 ),
inference(equality_resolution,[],[f163]) ).
fof(f241,plain,
! [X2] : terminates(overflow,filling,X2),
inference(equality_resolution,[],[f240]) ).
fof(f244,plain,
! [X1] :
( happens(tapOn,X1)
| n0 != X1 ),
inference(equality_resolution,[],[f175]) ).
fof(f245,plain,
happens(tapOn,n0),
inference(equality_resolution,[],[f244]) ).
fof(f246,plain,
! [X1] :
( ~ holdsAt(waterLevel(n3),X1)
| happens(overflow,X1)
| ~ holdsAt(filling,X1) ),
inference(equality_resolution,[],[f174]) ).
fof(f247,plain,
! [X3,X0,X1] :
( ~ holdsAt(waterLevel(X0),X1)
| trajectory(filling,X1,waterLevel(plus(X0,X3)),X3) ),
inference(equality_resolution,[],[f176]) ).
fof(f249,plain,
! [X1] : less_or_equal(X1,X1),
inference(equality_resolution,[],[f198]) ).
fof(f250,plain,
! [X1] : ~ less(X1,X1),
inference(equality_resolution,[],[f219]) ).
fof(f253,plain,
holdsAt(filling,plus(n1,n3)),
inference(superposition,[],[f229,f192]) ).
fof(f255,plain,
plus(n1,n3) = plus(n2,n2),
inference(superposition,[],[f192,f193]) ).
fof(f257,plain,
less(n0,n1),
inference(resolution,[],[f202,f249]) ).
fof(f260,plain,
less(n1,n2),
inference(resolution,[],[f204,f249]) ).
fof(f264,plain,
less(n2,n3),
inference(resolution,[],[f206,f249]) ).
fof(f267,plain,
less_or_equal(n2,n3),
inference(resolution,[],[f264,f199]) ).
fof(f271,plain,
less(n3,n4),
inference(resolution,[],[f208,f249]) ).
fof(f272,plain,
less(n2,n4),
inference(resolution,[],[f208,f267]) ).
fof(f273,plain,
less(n2,plus(n2,n2)),
inference(forward_demodulation,[],[f272,f193]) ).
fof(f274,plain,
less(n3,plus(n2,n2)),
inference(forward_demodulation,[],[f271,f193]) ).
fof(f275,plain,
less(n2,plus(n1,n3)),
inference(forward_demodulation,[],[f273,f255]) ).
fof(f276,plain,
less(n3,plus(n1,n3)),
inference(forward_demodulation,[],[f274,f255]) ).
fof(f308,plain,
~ less(n2,n1),
inference(resolution,[],[f220,f260]) ).
fof(f403,plain,
! [X0,X1] :
( less_or_equal(sK3(X0,X1,n1),n0)
| ~ stoppedIn(X0,X1,n1) ),
inference(resolution,[],[f126,f201]) ).
fof(f442,plain,
( happens(overflow,n3)
| ~ holdsAt(filling,n3) ),
inference(resolution,[],[f246,f228]) ).
fof(f444,plain,
! [X0,X1] :
( happens(overflow,X0)
| ~ holdsAt(filling,X0)
| n0 = X0
| ~ happens(X1,X0) ),
inference(resolution,[],[f246,f170]) ).
fof(f445,plain,
! [X0,X1] :
( ~ happens(X1,X0)
| n0 = X0
| happens(overflow,X0) ),
inference(forward_subsumption_resolution,[],[f444,f169]) ).
fof(f448,definition,
( spl11_1
<=> holdsAt(filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_1])],[avatar_definition]) ).
fof(f450,plain,
( ~ holdsAt(filling,n3)
| spl11_1 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f452,definition,
( spl11_2
<=> happens(overflow,n3) ),
introduced(definition,[new_symbols(definition,[spl11_2])],[avatar_definition]) ).
fof(f453,plain,
( ~ happens(overflow,n3)
| spl11_2 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f455,plain,
( ~ spl11_1
| spl11_2 ),
inference(avatar_split_clause,[],[f442,f452,f448]) ).
fof(f467,plain,
! [X2,X0,X1] :
( ~ holdsAt(waterLevel(X0),X1)
| n3 = X0
| n0 = X1
| ~ happens(X2,X1) ),
inference(resolution,[],[f177,f170]) ).
fof(f476,plain,
! [X2,X0,X1] :
( holdsAt(X1,plus(n1,X0))
| ~ happens(X2,X0)
| ~ initiates(X2,X1,X0) ),
inference(superposition,[],[f138,f196]) ).
fof(f485,plain,
! [X2,X0,X1] :
( ~ holdsAt(X1,plus(n1,X0))
| ~ happens(X2,X0)
| ~ terminates(X2,X1,X0) ),
inference(superposition,[],[f139,f196]) ).
fof(f496,plain,
! [X2,X0,X1] :
( ~ releasedAt(X1,plus(n1,X0))
| ~ happens(X2,X0)
| ~ terminates(X2,X1,X0) ),
inference(superposition,[],[f141,f196]) ).
fof(f504,plain,
! [X0,X1] :
( ~ initiates(X1,X0,n0)
| ~ happens(X1,n0)
| ~ releasedAt(X0,n1) ),
inference(superposition,[],[f142,f187]) ).
fof(f509,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(n0,X0)),X0),
inference(resolution,[],[f247,f222]) ).
fof(f519,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| overflow = sK2(X0,X1,X2)
| tapOn = sK2(X0,X1,X2) ),
inference(resolution,[],[f128,f171]) ).
fof(f535,plain,
! [X0,X1] :
( ~ releasedAt(X1,plus(n1,X0))
| releasedAt(X1,X0)
| happens(sK7(X1,X0),X0) ),
inference(superposition,[],[f137,f196]) ).
fof(f537,plain,
! [X0] :
( ~ releasedAt(X0,n2)
| releasedAt(X0,n1)
| happens(sK7(X0,n1),n1) ),
inference(superposition,[],[f137,f190]) ).
fof(f538,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| overflow = sK2(X0,X1,X2)
| tapOff = sK2(X0,X1,X2) ),
inference(resolution,[],[f125,f162]) ).
fof(f563,plain,
! [X0,X1] :
( ~ holdsAt(X1,plus(n1,X0))
| holdsAt(X1,X0)
| releasedAt(X1,plus(n1,X0))
| happens(sK5(X1,X0),X0) ),
inference(superposition,[],[f133,f196]) ).
fof(f715,definition,
( spl11_14
<=> n0 = n3 ),
introduced(definition,[new_symbols(definition,[spl11_14])],[avatar_definition]) ).
fof(f716,plain,
( n0 != n3
| spl11_14 ),
inference(avatar_component_clause,[],[f715]) ).
fof(f717,plain,
( n0 = n3
| ~ spl11_14 ),
inference(avatar_component_clause,[],[f715]) ).
fof(f755,plain,
trajectory(filling,n0,waterLevel(n1),n1),
inference(superposition,[],[f509,f187]) ).
fof(f764,definition,
( spl11_16
<=> ! [X0] :
( ~ happens(X0,n0)
| ~ initiates(X0,filling,n0) ) ),
introduced(definition,[new_symbols(definition,[spl11_16])],[avatar_definition]) ).
fof(f765,plain,
( ! [X0] :
( ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) )
| ~ spl11_16 ),
inference(avatar_component_clause,[],[f764]) ).
fof(f920,plain,
! [X0,X1] :
( ~ stoppedIn(X0,X1,n1)
| n0 = sK3(X0,X1,n1)
| less(sK3(X0,X1,n1),n0) ),
inference(resolution,[],[f403,f197]) ).
fof(f921,plain,
! [X0,X1] :
( ~ stoppedIn(X0,X1,n1)
| n0 = sK3(X0,X1,n1) ),
inference(forward_subsumption_resolution,[],[f920,f200]) ).
fof(f1012,definition,
( spl11_29
<=> releasedAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl11_29])],[avatar_definition]) ).
fof(f1013,plain,
( releasedAt(filling,n2)
| ~ spl11_29 ),
inference(avatar_component_clause,[],[f1012]) ).
fof(f1014,plain,
( ~ releasedAt(filling,n2)
| spl11_29 ),
inference(avatar_component_clause,[],[f1012]) ).
fof(f1018,plain,
( ~ happens(tapOn,n0)
| ~ releasedAt(filling,n1) ),
inference(resolution,[],[f504,f235]) ).
fof(f1022,plain,
~ releasedAt(filling,n1),
inference(forward_subsumption_resolution,[],[f1018,f245]) ).
fof(f1096,plain,
! [X0,X1] :
( ~ initiates(X1,X0,n2)
| ~ happens(X1,n2)
| holdsAt(X0,n3) ),
inference(superposition,[],[f476,f191]) ).
fof(f1102,plain,
! [X0] :
( ~ terminates(X0,filling,n3)
| ~ happens(X0,n3) ),
inference(resolution,[],[f485,f253]) ).
fof(f1116,plain,
~ happens(overflow,n3),
inference(resolution,[],[f1102,f241]) ).
fof(f1117,plain,
~ spl11_2,
inference(avatar_split_clause,[],[f1116,f452]) ).
fof(f1121,plain,
! [X0,X1] :
( ~ terminates(X1,X0,n2)
| ~ happens(X1,n2)
| ~ releasedAt(X0,n3) ),
inference(superposition,[],[f496,f191]) ).
fof(f1186,plain,
! [X0] :
( ~ releasedAt(X0,n3)
| releasedAt(X0,n2)
| happens(sK7(X0,n2),n2) ),
inference(superposition,[],[f535,f191]) ).
fof(f1246,definition,
( spl11_30
<=> ! [X0] : ~ happens(X0,n1) ),
introduced(definition,[new_symbols(definition,[spl11_30])],[avatar_definition]) ).
fof(f1247,plain,
( ! [X0] : ~ happens(X0,n1)
| ~ spl11_30 ),
inference(avatar_component_clause,[],[f1246]) ).
fof(f1249,definition,
( spl11_31
<=> n0 = n1 ),
introduced(definition,[new_symbols(definition,[spl11_31])],[avatar_definition]) ).
fof(f1251,plain,
( n0 = n1
| ~ spl11_31 ),
inference(avatar_component_clause,[],[f1249]) ).
fof(f1291,definition,
( spl11_38
<=> n0 = n2 ),
introduced(definition,[new_symbols(definition,[spl11_38])],[avatar_definition]) ).
fof(f1292,plain,
( n0 != n2
| spl11_38 ),
inference(avatar_component_clause,[],[f1291]) ).
fof(f1293,plain,
( n0 = n2
| ~ spl11_38 ),
inference(avatar_component_clause,[],[f1291]) ).
fof(f1436,plain,
! [X0] :
( ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,n1)
| holdsAt(waterLevel(n1),plus(n0,n1))
| stoppedIn(n0,filling,plus(n0,n1)) ),
inference(resolution,[],[f755,f129]) ).
fof(f1437,plain,
! [X0] :
( ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| holdsAt(waterLevel(n1),plus(n0,n1))
| stoppedIn(n0,filling,plus(n0,n1)) ),
inference(forward_subsumption_resolution,[],[f1436,f257]) ).
fof(f1438,plain,
! [X0] :
( holdsAt(waterLevel(n1),n1)
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| stoppedIn(n0,filling,plus(n0,n1)) ),
inference(forward_demodulation,[],[f1437,f187]) ).
fof(f1439,plain,
! [X0] :
( stoppedIn(n0,filling,n1)
| holdsAt(waterLevel(n1),n1)
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0) ),
inference(forward_demodulation,[],[f1438,f187]) ).
fof(f1441,definition,
( spl11_47
<=> holdsAt(waterLevel(n1),n1) ),
introduced(definition,[new_symbols(definition,[spl11_47])],[avatar_definition]) ).
fof(f1443,plain,
( holdsAt(waterLevel(n1),n1)
| ~ spl11_47 ),
inference(avatar_component_clause,[],[f1441]) ).
fof(f1445,definition,
( spl11_48
<=> stoppedIn(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl11_48])],[avatar_definition]) ).
fof(f1447,plain,
( stoppedIn(n0,filling,n1)
| ~ spl11_48 ),
inference(avatar_component_clause,[],[f1445]) ).
fof(f1448,plain,
( spl11_16
| spl11_47
| spl11_48 ),
inference(avatar_split_clause,[],[f1439,f1445,f1441,f764]) ).
fof(f1566,definition,
( spl11_56
<=> happens(overflow,n2) ),
introduced(definition,[new_symbols(definition,[spl11_56])],[avatar_definition]) ).
fof(f1567,plain,
( ~ happens(overflow,n2)
| spl11_56 ),
inference(avatar_component_clause,[],[f1566]) ).
fof(f1568,plain,
( happens(overflow,n2)
| ~ spl11_56 ),
inference(avatar_component_clause,[],[f1566]) ).
fof(f1668,plain,
( holdsAt(filling,n3)
| releasedAt(filling,plus(n1,n3))
| happens(sK5(filling,n3),n3) ),
inference(resolution,[],[f563,f253]) ).
fof(f1685,plain,
( releasedAt(filling,plus(n1,n3))
| happens(sK5(filling,n3),n3)
| spl11_1 ),
inference(forward_subsumption_resolution,[],[f1668,f450]) ).
fof(f1687,definition,
( spl11_63
<=> happens(sK5(filling,n3),n3) ),
introduced(definition,[new_symbols(definition,[spl11_63])],[avatar_definition]) ).
fof(f1689,plain,
( happens(sK5(filling,n3),n3)
| ~ spl11_63 ),
inference(avatar_component_clause,[],[f1687]) ).
fof(f1691,definition,
( spl11_64
<=> releasedAt(filling,plus(n1,n3)) ),
introduced(definition,[new_symbols(definition,[spl11_64])],[avatar_definition]) ).
fof(f1693,plain,
( releasedAt(filling,plus(n1,n3))
| ~ spl11_64 ),
inference(avatar_component_clause,[],[f1691]) ).
fof(f1694,plain,
( spl11_63
| spl11_64
| spl11_1 ),
inference(avatar_split_clause,[],[f1685,f448,f1691,f1687]) ).
fof(f1703,plain,
( n0 = n3
| happens(overflow,n3)
| ~ spl11_63 ),
inference(resolution,[],[f1689,f445]) ).
fof(f1708,plain,
( n0 = n3
| spl11_2
| ~ spl11_63 ),
inference(forward_subsumption_resolution,[],[f1703,f453]) ).
fof(f1722,plain,
( spl11_14
| spl11_2
| ~ spl11_63 ),
inference(avatar_split_clause,[],[f1708,f1687,f452,f715]) ).
fof(f1733,plain,
( releasedAt(filling,n3)
| happens(sK7(filling,n3),n3)
| ~ spl11_64 ),
inference(resolution,[],[f1693,f535]) ).
fof(f1737,definition,
( spl11_67
<=> happens(sK7(filling,n3),n3) ),
introduced(definition,[new_symbols(definition,[spl11_67])],[avatar_definition]) ).
fof(f1739,plain,
( happens(sK7(filling,n3),n3)
| ~ spl11_67 ),
inference(avatar_component_clause,[],[f1737]) ).
fof(f1741,definition,
( spl11_68
<=> releasedAt(filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_68])],[avatar_definition]) ).
fof(f1743,plain,
( releasedAt(filling,n3)
| ~ spl11_68 ),
inference(avatar_component_clause,[],[f1741]) ).
fof(f1744,plain,
( spl11_67
| spl11_68
| ~ spl11_64 ),
inference(avatar_split_clause,[],[f1733,f1691,f1741,f1737]) ).
fof(f1794,plain,
( less(n2,plus(n1,n0))
| ~ spl11_14 ),
inference(superposition,[],[f275,f717]) ).
fof(f1898,plain,
( less(n2,plus(n0,n1))
| ~ spl11_14 ),
inference(forward_demodulation,[],[f1794,f196]) ).
fof(f1937,plain,
( less(n2,n1)
| ~ spl11_14 ),
inference(forward_demodulation,[],[f1898,f187]) ).
fof(f1951,plain,
( $false
| ~ spl11_14 ),
inference(forward_subsumption_resolution,[],[f1937,f308]) ).
fof(f1952,plain,
~ spl11_14,
inference(avatar_contradiction_clause,[],[f1951]) ).
fof(f2074,plain,
( n0 = n3
| happens(overflow,n3)
| ~ spl11_67 ),
inference(resolution,[],[f1739,f445]) ).
fof(f2079,plain,
( happens(overflow,n3)
| spl11_14
| ~ spl11_67 ),
inference(forward_subsumption_resolution,[],[f2074,f716]) ).
fof(f2093,plain,
( $false
| spl11_2
| spl11_14
| ~ spl11_67 ),
inference(forward_subsumption_resolution,[],[f2079,f453]) ).
fof(f2094,plain,
( spl11_2
| spl11_14
| ~ spl11_67 ),
inference(avatar_contradiction_clause,[],[f2093]) ).
fof(f2392,plain,
( ~ happens(tapOn,n0)
| ~ spl11_16 ),
inference(resolution,[],[f765,f235]) ).
fof(f2394,plain,
( $false
| ~ spl11_16 ),
inference(forward_subsumption_resolution,[],[f2392,f245]) ).
fof(f2395,plain,
~ spl11_16,
inference(avatar_contradiction_clause,[],[f2394]) ).
fof(f2423,plain,
( ! [X0] :
( n1 = n3
| n0 = n1
| ~ happens(X0,n1) )
| ~ spl11_47 ),
inference(resolution,[],[f1443,f467]) ).
fof(f2437,definition,
( spl11_84
<=> n1 = n3 ),
introduced(definition,[new_symbols(definition,[spl11_84])],[avatar_definition]) ).
fof(f2439,plain,
( n1 = n3
| ~ spl11_84 ),
inference(avatar_component_clause,[],[f2437]) ).
fof(f2440,plain,
( spl11_30
| spl11_31
| spl11_84
| ~ spl11_47 ),
inference(avatar_split_clause,[],[f2423,f1441,f2437,f1249,f1246]) ).
fof(f2554,plain,
( overflow = sK2(n0,filling,n1)
| tapOff = sK2(n0,filling,n1)
| ~ spl11_48 ),
inference(resolution,[],[f1447,f538]) ).
fof(f2556,plain,
( overflow = sK2(n0,filling,n1)
| tapOn = sK2(n0,filling,n1)
| ~ spl11_48 ),
inference(resolution,[],[f1447,f519]) ).
fof(f2559,definition,
( spl11_92
<=> tapOn = sK2(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl11_92])],[avatar_definition]) ).
fof(f2561,plain,
( tapOn = sK2(n0,filling,n1)
| ~ spl11_92 ),
inference(avatar_component_clause,[],[f2559]) ).
fof(f2563,definition,
( spl11_93
<=> overflow = sK2(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl11_93])],[avatar_definition]) ).
fof(f2565,plain,
( overflow = sK2(n0,filling,n1)
| ~ spl11_93 ),
inference(avatar_component_clause,[],[f2563]) ).
fof(f2566,plain,
( spl11_92
| spl11_93
| ~ spl11_48 ),
inference(avatar_split_clause,[],[f2556,f1445,f2563,f2559]) ).
fof(f2568,definition,
( spl11_94
<=> n0 = sK3(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl11_94])],[avatar_definition]) ).
fof(f2569,plain,
( n0 != sK3(n0,filling,n1)
| spl11_94 ),
inference(avatar_component_clause,[],[f2568]) ).
fof(f2570,plain,
( n0 = sK3(n0,filling,n1)
| ~ spl11_94 ),
inference(avatar_component_clause,[],[f2568]) ).
fof(f2573,definition,
( spl11_95
<=> tapOff = sK2(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl11_95])],[avatar_definition]) ).
fof(f2575,plain,
( tapOff = sK2(n0,filling,n1)
| ~ spl11_95 ),
inference(avatar_component_clause,[],[f2573]) ).
fof(f2576,plain,
( spl11_95
| spl11_93
| ~ spl11_48 ),
inference(avatar_split_clause,[],[f2554,f1445,f2563,f2573]) ).
fof(f3337,plain,
( less(n3,plus(n0,n3))
| ~ spl11_31 ),
inference(superposition,[],[f276,f1251]) ).
fof(f3477,plain,
( less(n3,n3)
| ~ spl11_31 ),
inference(forward_demodulation,[],[f3337,f189]) ).
fof(f3485,plain,
( $false
| ~ spl11_31 ),
inference(forward_subsumption_resolution,[],[f3477,f250]) ).
fof(f3486,plain,
~ spl11_31,
inference(avatar_contradiction_clause,[],[f3485]) ).
fof(f3552,plain,
( less(n2,plus(n1,n1))
| ~ spl11_84 ),
inference(superposition,[],[f275,f2439]) ).
fof(f3677,plain,
( less(n2,n2)
| ~ spl11_84 ),
inference(forward_demodulation,[],[f3552,f190]) ).
fof(f3691,plain,
( $false
| ~ spl11_84 ),
inference(forward_subsumption_resolution,[],[f3677,f250]) ).
fof(f3692,plain,
~ spl11_84,
inference(avatar_contradiction_clause,[],[f3691]) ).
fof(f4134,plain,
( happens(overflow,sK3(n0,filling,n1))
| ~ stoppedIn(n0,filling,n1)
| ~ spl11_93 ),
inference(superposition,[],[f128,f2565]) ).
fof(f4135,plain,
( happens(overflow,sK3(n0,filling,n1))
| ~ spl11_48
| ~ spl11_93 ),
inference(forward_subsumption_resolution,[],[f4134,f1447]) ).
fof(f4140,plain,
( holdsAt(filling,sK3(n0,filling,n1))
| tapOn = overflow
| ~ spl11_48
| ~ spl11_93 ),
inference(resolution,[],[f4135,f172]) ).
fof(f4173,plain,
( holdsAt(filling,sK3(n0,filling,n1))
| ~ spl11_48
| ~ spl11_93 ),
inference(forward_subsumption_resolution,[],[f4140,f180]) ).
fof(f4340,plain,
( ~ happens(tapOn,n2)
| holdsAt(filling,n3) ),
inference(resolution,[],[f1096,f235]) ).
fof(f4348,plain,
( ~ happens(overflow,n2)
| ~ releasedAt(filling,n3) ),
inference(resolution,[],[f1121,f241]) ).
fof(f4746,plain,
( releasedAt(filling,n2)
| happens(sK7(filling,n2),n2)
| ~ spl11_68 ),
inference(resolution,[],[f1186,f1743]) ).
fof(f4753,plain,
( releasedAt(filling,n1)
| happens(sK7(filling,n1),n1)
| ~ spl11_29 ),
inference(resolution,[],[f1013,f537]) ).
fof(f4754,plain,
( happens(sK7(filling,n1),n1)
| ~ spl11_29 ),
inference(forward_subsumption_resolution,[],[f4753,f1022]) ).
fof(f4755,plain,
( $false
| ~ spl11_29
| ~ spl11_30 ),
inference(forward_subsumption_resolution,[],[f4754,f1247]) ).
fof(f4756,plain,
( ~ spl11_29
| ~ spl11_30 ),
inference(avatar_contradiction_clause,[],[f4755]) ).
fof(f4773,plain,
( ~ happens(tapOn,n2)
| spl11_1 ),
inference(forward_subsumption_resolution,[],[f4340,f450]) ).
fof(f4802,plain,
( ~ happens(tapOn,n0)
| spl11_1
| ~ spl11_38 ),
inference(forward_demodulation,[],[f4773,f1293]) ).
fof(f4833,plain,
( $false
| spl11_1
| ~ spl11_38 ),
inference(forward_subsumption_resolution,[],[f4802,f245]) ).
fof(f4834,plain,
( spl11_1
| ~ spl11_38 ),
inference(avatar_contradiction_clause,[],[f4833]) ).
fof(f4861,plain,
( tapOn = tapOff
| ~ spl11_92
| ~ spl11_95 ),
inference(forward_demodulation,[],[f2575,f2561]) ).
fof(f4871,plain,
( $false
| ~ spl11_92
| ~ spl11_95 ),
inference(forward_subsumption_resolution,[],[f4861,f178]) ).
fof(f4872,plain,
( ~ spl11_92
| ~ spl11_95 ),
inference(avatar_contradiction_clause,[],[f4871]) ).
fof(f4924,plain,
( happens(sK7(filling,n2),n2)
| spl11_29
| ~ spl11_68 ),
inference(forward_subsumption_resolution,[],[f4746,f1014]) ).
fof(f5008,plain,
( n0 = n2
| happens(overflow,n2)
| spl11_29
| ~ spl11_68 ),
inference(resolution,[],[f4924,f445]) ).
fof(f5040,plain,
( happens(overflow,n2)
| spl11_29
| spl11_38
| ~ spl11_68 ),
inference(forward_subsumption_resolution,[],[f5008,f1292]) ).
fof(f5042,plain,
( $false
| spl11_29
| spl11_38
| spl11_56
| ~ spl11_68 ),
inference(forward_subsumption_resolution,[],[f5040,f1567]) ).
fof(f5043,plain,
( spl11_29
| spl11_38
| spl11_56
| ~ spl11_68 ),
inference(avatar_contradiction_clause,[],[f5042]) ).
fof(f5045,plain,
( ~ releasedAt(filling,n3)
| ~ spl11_56 ),
inference(forward_subsumption_resolution,[],[f4348,f1568]) ).
fof(f5047,plain,
( $false
| ~ spl11_56
| ~ spl11_68 ),
inference(forward_subsumption_resolution,[],[f5045,f1743]) ).
fof(f5048,plain,
( ~ spl11_56
| ~ spl11_68 ),
inference(avatar_contradiction_clause,[],[f5047]) ).
fof(f5049,plain,
( holdsAt(filling,n0)
| ~ spl11_48
| ~ spl11_93
| ~ spl11_94 ),
inference(forward_demodulation,[],[f4173,f2570]) ).
fof(f5058,plain,
( $false
| ~ spl11_48
| ~ spl11_93
| ~ spl11_94 ),
inference(forward_subsumption_resolution,[],[f5049,f223]) ).
fof(f5059,plain,
( ~ spl11_48
| ~ spl11_93
| ~ spl11_94 ),
inference(avatar_contradiction_clause,[],[f5058]) ).
fof(f5122,plain,
( n0 = sK3(n0,filling,n1)
| ~ spl11_48 ),
inference(resolution,[],[f1447,f921]) ).
fof(f5127,plain,
( $false
| ~ spl11_48
| spl11_94 ),
inference(forward_subsumption_resolution,[],[f5122,f2569]) ).
fof(f5128,plain,
( ~ spl11_48
| spl11_94 ),
inference(avatar_contradiction_clause,[],[f5127]) ).
cnf(s1,plain,
( ~ spl11_1
| spl11_2 ),
inference(sat_conversion,[],[f455]) ).
cnf(s19,plain,
~ spl11_2,
inference(sat_conversion,[],[f1117]) ).
cnf(s31,plain,
( spl11_16
| spl11_47
| spl11_48 ),
inference(sat_conversion,[],[f1448]) ).
cnf(s57,plain,
( spl11_1
| spl11_63
| spl11_64 ),
inference(sat_conversion,[],[f1694]) ).
cnf(s61,plain,
( spl11_2
| spl11_14
| ~ spl11_63 ),
inference(sat_conversion,[],[f1722]) ).
cnf(s64,plain,
( ~ spl11_64
| spl11_67
| spl11_68 ),
inference(sat_conversion,[],[f1744]) ).
cnf(s73,plain,
~ spl11_14,
inference(sat_conversion,[],[f1952]) ).
cnf(s77,plain,
( spl11_2
| spl11_14
| ~ spl11_67 ),
inference(sat_conversion,[],[f2094]) ).
cnf(s97,plain,
~ spl11_16,
inference(sat_conversion,[],[f2395]) ).
cnf(s99,plain,
( spl11_30
| spl11_31
| ~ spl11_47
| spl11_84 ),
inference(sat_conversion,[],[f2440]) ).
cnf(s109,plain,
( ~ spl11_48
| spl11_92
| spl11_93 ),
inference(sat_conversion,[],[f2566]) ).
cnf(s111,plain,
( ~ spl11_48
| spl11_93
| spl11_95 ),
inference(sat_conversion,[],[f2576]) ).
cnf(s129,plain,
~ spl11_31,
inference(sat_conversion,[],[f3486]) ).
cnf(s142,plain,
~ spl11_84,
inference(sat_conversion,[],[f3692]) ).
cnf(s179,plain,
( ~ spl11_29
| ~ spl11_30 ),
inference(sat_conversion,[],[f4756]) ).
cnf(s181,plain,
( spl11_1
| ~ spl11_38 ),
inference(sat_conversion,[],[f4834]) ).
cnf(s184,plain,
( ~ spl11_92
| ~ spl11_95 ),
inference(sat_conversion,[],[f4872]) ).
cnf(s201,plain,
( spl11_29
| spl11_38
| spl11_56
| ~ spl11_68 ),
inference(sat_conversion,[],[f5043]) ).
cnf(s202,plain,
( ~ spl11_56
| ~ spl11_68 ),
inference(sat_conversion,[],[f5048]) ).
cnf(s203,plain,
( ~ spl11_48
| ~ spl11_93
| ~ spl11_94 ),
inference(sat_conversion,[],[f5059]) ).
cnf(s212,plain,
( ~ spl11_48
| spl11_94 ),
inference(sat_conversion,[],[f5128]) ).
cnf(s214,plain,
( spl11_30
| ~ spl11_47 ),
inference(rat,[],[s99,s142,s129]) ).
cnf(s217,plain,
( spl11_2
| ~ spl11_63 ),
inference(rat,[],[s61,s73]) ).
cnf(s224,plain,
( spl11_47
| spl11_48 ),
inference(rat,[],[s31,s97]) ).
cnf(s228,plain,
~ spl11_67,
inference(rat,[],[s77,s73,s19]) ).
cnf(s229,plain,
~ spl11_63,
inference(rat,[],[s217,s19]) ).
cnf(s233,plain,
~ spl11_1,
inference(rat,[],[s1,s19]) ).
cnf(s235,plain,
~ spl11_38,
inference(rat,[],[s181,s233]) ).
cnf(s236,plain,
spl11_64,
inference(rat,[],[s57,s229,s233]) ).
cnf(s237,plain,
spl11_68,
inference(rat,[],[s64,s228,s236]) ).
cnf(s238,plain,
~ spl11_56,
inference(rat,[],[s202,s237]) ).
cnf(s239,plain,
spl11_29,
inference(rat,[],[s201,s237,s235,s238]) ).
cnf(s240,plain,
~ spl11_30,
inference(rat,[],[s179,s239]) ).
cnf(s242,plain,
~ spl11_47,
inference(rat,[],[s214,s240]) ).
cnf(s243,plain,
spl11_48,
inference(rat,[],[s224,s242]) ).
cnf(s244,plain,
spl11_94,
inference(rat,[],[s212,s243]) ).
cnf(s245,plain,
~ spl11_93,
inference(rat,[],[s203,s244,s243]) ).
cnf(s246,plain,
spl11_92,
inference(rat,[],[s109,s245,s243]) ).
cnf(s248,plain,
spl11_95,
inference(rat,[],[s111,s243,s245]) ).
cnf(s249,plain,
$false,
inference(rat,[],[s184,s248,s246]) ).
fof(f5129,plain,
$false,
inference(avatar_sat_refutation,[],[s249]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR002+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n001.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 22:11:04 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.24 Running first-order model finding
% 0.09/0.24 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
% 3.19/0.79 % (803478)Will run a generic schedule for satisfiability detection.
% 3.19/0.79 % (803483)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2640493131_2999 on theBenchmark for (2999ds/0Mi)
% 3.19/0.79 % (803484)% WARNING: option uhcvi not known.
% 3.19/0.79 % Detected minimum model sizes of [3]
% 3.19/0.79 % Detected maximum model sizes of [max]
% 3.19/0.79 % TRYING [3]
% 3.19/0.79 % (803484)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4230174931:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.19/0.79 % (803485)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4052038024:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.19/0.79 % (803486)dis+10_1_sil=32000:sp=arity:random_seed=4192222339:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.19/0.79 % (803487)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3911264425:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.19/0.79 % TRYING [4]
% 3.19/0.79 % (803488)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1292547002:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.19/0.79 % (803489)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=881245098:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.19/0.79 % TRYING [5]
% 3.19/0.79 % TRYING [6]
% 3.19/0.79 % (803486)Instruction limit reached!
% 3.19/0.79 % (803486)------------------------------
% 3.19/0.79 % (803486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.79 % (803486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.79 % (803486)CaDiCaL version: 2.1.3
% 3.19/0.79 % (803486)Termination reason: Instruction limit
% 3.19/0.79 % (803486)Termination phase: Saturation
% 3.19/0.79 % (803486)Time elapsed: 0.065 s
% 3.19/0.79 % (803486)Peak memory usage: 12 MB
% 3.19/0.79 % (803486)Instructions burned: 104 (million)
% 3.19/0.79 % TRYING [7]
% 3.19/0.79 % (803487)Instruction limit reached!
% 3.19/0.79 % (803487)------------------------------
% 3.19/0.79 % (803487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.79 % (803487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.79 % (803487)CaDiCaL version: 2.1.3
% 3.19/0.79 % (803487)Termination reason: Instruction limit
% 3.19/0.79 % (803487)Termination phase: Saturation
% 3.19/0.79 % (803487)Time elapsed: 0.077 s
% 3.19/0.79 % (803487)Peak memory usage: 13 MB
% 3.19/0.79 % (803487)Instructions burned: 116 (million)
% 3.19/0.79 % (803489)Instruction limit reached!
% 3.19/0.79 % (803489)------------------------------
% 3.19/0.79 % (803489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.79 % (803489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.79 % (803489)CaDiCaL version: 2.1.3
% 3.19/0.79 % (803489)Termination reason: Instruction limit
% 3.19/0.79 % (803489)Termination phase: Saturation
% 3.19/0.79 % (803489)Time elapsed: 0.078 s
% 3.19/0.79 % (803489)Peak memory usage: 12 MB
% 3.19/0.79 % (803489)Instructions burned: 160 (million)
% 3.19/0.79 % (803488)Instruction limit reached!
% 3.19/0.79 % (803488)------------------------------
% 3.19/0.79 % (803488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.79 % (803488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.79 % (803488)CaDiCaL version: 2.1.3
% 3.19/0.79 % (803488)Termination reason: Instruction limit
% 3.19/0.79 % (803488)Termination phase: Saturation
% 3.19/0.79 % (803488)Time elapsed: 0.083 s
% 3.19/0.79 % (803488)Peak memory usage: 13 MB
% 3.19/0.79 % (803488)Instructions burned: 134 (million)
% 3.19/0.79 % (803497)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3447834617:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.19/0.79 % Detected minimum model sizes of [3]
% 3.19/0.79 % Detected maximum model sizes of [max]
% 3.19/0.79 % TRYING [3]
% 3.19/0.79 % (803498)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=544020714:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 3.19/0.79 % (803499)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=4056662703:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 3.19/0.79 % TRYING [4]
% 3.19/0.79 % (803501)ott-21_1_sil=16000:fs=off:random_seed=3437699428:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 3.19/0.79 % TRYING [5]
% 3.19/0.79 % TRYING [8]
% 3.19/0.79 % TRYING [6]
% 3.19/0.79 % (803498)Instruction limit reached!
% 3.19/0.79 % (803498)------------------------------
% 3.19/0.79 % (803498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.79 % (803498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.79 % (803498)CaDiCaL version: 2.1.3
% 3.19/0.79 % (803498)Termination reason: Instruction limit
% 3.19/0.79 % (803498)Termination phase: Saturation
% 3.19/0.79 % (803498)Time elapsed: 0.085 s
% 3.19/0.79 % (803498)Peak memory usage: 13 MB
% 3.19/0.79 % (803498)Instructions burned: 131 (million)
% 3.19/0.79 % (803501)Instruction limit reached!
% 3.19/0.79 % (803501)------------------------------
% 3.19/0.79 % (803501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.79 % (803501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.79 % (803501)CaDiCaL version: 2.1.3
% 3.19/0.79 % (803501)Termination reason: Instruction limit
% 3.19/0.79 % (803501)Termination phase: Saturation
% 3.19/0.79 % (803501)Time elapsed: 0.094 s
% 3.19/0.79 % (803501)Peak memory usage: 12 MB
% 3.19/0.79 % (803501)Instructions burned: 180 (million)
% 3.19/0.79 % (803505)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3065531595:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 3.19/0.79 % (803506)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3404076045:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 3.19/0.79 % Detected minimum model sizes of [3]
% 3.19/0.79 % Detected maximum model sizes of [max]
% 3.19/0.79 % TRYING [3]
% 3.19/0.79 % TRYING [4]
% 3.19/0.79 % TRYING [5]
% 3.19/0.79 % TRYING [9]
% 3.19/0.79 % TRYING [7]
% 3.19/0.79 % (803497)Instruction limit reached!
% 3.19/0.79 % (803497)------------------------------
% 3.19/0.79 % (803497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.79 % (803497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.79 % (803497)CaDiCaL version: 2.1.3
% 3.19/0.79 % (803497)Termination reason: Instruction limit
% 3.19/0.79 % (803497)Termination phase: Finite model building constraint generation
% 3.19/0.79 % (803497)Time elapsed: 0.269 s
% 3.19/0.79 % (803497)Peak memory usage: 28 MB
% 3.19/0.79 % (803497)Instructions burned: 716 (million)
% 3.19/0.79 % (803509)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2852234571:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 3.19/0.79 % TRYING [6]
% 3.19/0.79 % (803499)Instruction limit reached!
% 3.19/0.79 % (803499)------------------------------
% 3.19/0.79 % (803499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.79 % (803499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.79 % (803499)CaDiCaL version: 2.1.3
% 3.19/0.79 % (803499)Termination reason: Instruction limit
% 3.19/0.79 % (803499)Termination phase: Saturation
% 3.19/0.79 % (803499)Time elapsed: 0.362 s
% 3.19/0.79 % (803499)Peak memory usage: 14 MB
% 3.19/0.79 % (803499)Instructions burned: 685 (million)
% 3.19/0.79 % (803511)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2122626009:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 3.19/0.79 % (803509) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-803478-803509"...
% 3.19/0.79 % (803505)Instruction limit reached!
% 3.19/0.79 % (803505)------------------------------
% 3.19/0.79 % (803505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.79 % (803505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.79 % (803505)CaDiCaL version: 2.1.3
% 3.19/0.79 % (803505)Termination reason: Instruction limit
% 3.19/0.79 % (803505)Termination phase: Saturation
% 3.19/0.79 % (803505)Time elapsed: 0.298 s
% 3.19/0.79 % (803505)Peak memory usage: 13 MB
% 3.19/0.79 % (803505)Instructions burned: 478 (million)
% 3.19/0.79 % (803509)...printing done.
% 3.19/0.79 % (803509)Refutation found. Thanks to Tanya!
% 3.19/0.79 % SZS status Theorem for theBenchmark
% 3.19/0.79 % SZS output start Proof for theBenchmark
% See solution above
% 3.19/0.79 % (803509)------------------------------
% 3.19/0.79 % (803509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.19/0.79 % (803509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.19/0.79 % (803509)CaDiCaL version: 2.1.3
% 3.19/0.79 % (803509)Termination reason: Refutation
% 3.19/0.79 % (803509)Time elapsed: 0.122 s
% 3.19/0.79 % (803509)Peak memory usage: 14 MB
% 3.19/0.79 % (803509)Instructions burned: 198 (million)
% 3.19/0.79 % (803478)Success in time 0.542 s
% 3.19/0.79 % Vampire exiting
%------------------------------------------------------------------------------