%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR003+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n006.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 40.64s 6.13s
% Output : Refutation 41.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 56
% Syntax : Number of formulae : 440 ( 65 unt; 28 def)
% Number of atoms : 1361 ( 228 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 1491 ( 570 ~; 757 |; 115 &)
% ( 40 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 40 ( 38 usr; 27 prp; 0-4 aty)
% Number of functors : 18 ( 18 usr; 10 con; 0-3 aty)
% Number of variables : 435 ( 0 sgn 411 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( stoppedIn(X0,X1,X2)
<=> ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax',stoppedin_defn) ).
fof(f3,axiom,
! [X0,X1,X2,X3,X4] :
( ( happens(X0,X1)
& initiates(X0,X2,X1)
& less(n0,X4)
& trajectory(X2,X1,X3,X4)
& ~ stoppedIn(X1,X2,plus(X1,X4)) )
=> holdsAt(X3,plus(X1,X4)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax',change_holding) ).
fof(f5,axiom,
! [X0,X1] :
( ( holdsAt(X0,X1)
& ~ releasedAt(X0,plus(X1,n1))
& ~ ? [X2] :
( happens(X2,X1)
& terminates(X2,X0,X1) ) )
=> holdsAt(X0,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax',keep_holding) ).
fof(f8,axiom,
! [X0,X1] :
( ( ~ releasedAt(X0,X1)
& ~ ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) )
=> ~ releasedAt(X0,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax',keep_not_released) ).
fof(f9,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& initiates(X0,X2,X1) )
=> holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax',happens_holds) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& terminates(X0,X2,X1) )
=> ~ holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax',happens_terminates_not_holds) ).
fof(f11,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& releases(X0,X2,X1) )
=> releasedAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax',happens_releases) ).
fof(f12,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& ( initiates(X0,X2,X1)
| terminates(X0,X2,X1) ) )
=> ~ releasedAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+0.ax',happens_not_released) ).
fof(f13,axiom,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = overflow
& X1 = waterLevel(X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+1.ax',initiates_all_defn) ).
fof(f14,axiom,
! [X0,X1,X2] :
( terminates(X0,X1,X2)
<=> ( ( X0 = tapOff
& X1 = filling )
| ( X0 = overflow
& X1 = filling ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+1.ax',terminates_all_defn) ).
fof(f15,axiom,
! [X0,X1,X2] :
( releases(X0,X1,X2)
<=> ? [X3] :
( X0 = tapOn
& X1 = waterLevel(X3) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+1.ax',releases_all_defn) ).
fof(f16,axiom,
! [X0,X1] :
( happens(X0,X1)
<=> ( ( X0 = tapOn
& X1 = n0 )
| ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+1.ax',happens_all_defn) ).
fof(f17,axiom,
! [X0,X1,X2,X3] :
( ( holdsAt(waterLevel(X0),X1)
& X2 = plus(X0,X3) )
=> trajectory(filling,X1,waterLevel(X2),X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+1.ax',change_of_waterLevel) ).
fof(f27,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',plus0_1) ).
fof(f29,axiom,
plus(n0,n3) = n3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',plus0_3) ).
fof(f30,axiom,
plus(n1,n1) = n2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',plus1_1) ).
fof(f31,axiom,
plus(n1,n2) = n3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',plus1_2) ).
fof(f32,axiom,
plus(n1,n3) = n4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',plus1_3) ).
fof(f36,axiom,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_plus) ).
fof(f37,axiom,
! [X0,X1] :
( less_or_equal(X0,X1)
<=> ( less(X0,X1)
| X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_or_equal) ).
fof(f38,axiom,
~ ? [X0] : less(X0,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less0) ).
fof(f39,axiom,
! [X0] :
( less(X0,n1)
<=> less_or_equal(X0,n0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less1) ).
fof(f40,axiom,
! [X0] :
( less(X0,n2)
<=> less_or_equal(X0,n1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less2) ).
fof(f41,axiom,
! [X0] :
( less(X0,n3)
<=> less_or_equal(X0,n2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less3) ).
fof(f48,axiom,
! [X0,X1] :
( less(X0,X1)
<=> ( ~ less(X1,X0)
& X1 != X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_property) ).
fof(f49,axiom,
holdsAt(waterLevel(n0),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',waterLevel_0) ).
fof(f52,axiom,
! [X0] : ~ releasedAt(waterLevel(X0),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_released_waterLevel_0) ).
fof(f55,conjecture,
holdsAt(spilling,n4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',spilling_4) ).
fof(f56,negated_conjecture,
~ holdsAt(spilling,n4),
inference(negated_conjecture,[status(cth)],[f55]) ).
fof(f57,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) )
| ? [X4] :
( holdsAt(waterLevel(X4),X2)
& X0 = overflow
& waterLevel(X4) = X1 ) ) ),
inference(rectify,[],[f13]) ).
fof(f58,plain,
~ holdsAt(spilling,n4),
inference(flattening,[],[f56]) ).
fof(f60,plain,
! [X0,X1,X2] :
( stoppedIn(X0,X1,X2)
=> ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) ) ),
inference(unused_predicate_definition_removal,[],[f1]) ).
fof(f63,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) )
| ~ stoppedIn(X0,X1,X2) ),
inference(ennf_transformation,[],[f60]) ).
fof(f64,plain,
! [X0,X1,X2,X3,X4] :
( holdsAt(X3,plus(X1,X4))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1)
| ~ less(n0,X4)
| ~ trajectory(X2,X1,X3,X4)
| stoppedIn(X1,X2,plus(X1,X4)) ),
inference(ennf_transformation,[],[f3]) ).
fof(f65,plain,
! [X0,X1,X2,X3,X4] :
( holdsAt(X3,plus(X1,X4))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1)
| ~ less(n0,X4)
| ~ trajectory(X2,X1,X3,X4)
| stoppedIn(X1,X2,plus(X1,X4)) ),
inference(flattening,[],[f64]) ).
fof(f66,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ? [X2] :
( happens(X2,X1)
& terminates(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f67,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ? [X2] :
( happens(X2,X1)
& terminates(X2,X0,X1) ) ),
inference(flattening,[],[f66]) ).
fof(f72,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f73,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(flattening,[],[f72]) ).
fof(f74,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f75,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(flattening,[],[f74]) ).
fof(f76,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(flattening,[],[f76]) ).
fof(f78,plain,
! [X0,X1,X2] :
( releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ releases(X0,X2,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f79,plain,
! [X0,X1,X2] :
( releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ releases(X0,X2,X1) ),
inference(flattening,[],[f78]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(flattening,[],[f80]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(ennf_transformation,[],[f17]) ).
fof(f83,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(flattening,[],[f82]) ).
fof(f86,plain,
! [X0] : ~ less(X0,n0),
inference(ennf_transformation,[],[f38]) ).
fof(f87,definition,
! [X2,X0,X1] :
( sP0(X2,X0,X1)
<=> ? [X4] :
( holdsAt(waterLevel(X4),X2)
& X0 = overflow
& waterLevel(X4) = X1 ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f88,definition,
! [X2,X0,X1] :
( sP1(X2,X0,X1)
<=> ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f89,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| sP1(X2,X0,X1)
| sP0(X2,X0,X1) ) ),
inference(definition_folding,[],[f57,f88,f87]) ).
fof(f90,plain,
! [X0,X1,X2] :
( ( happens(sK2(X0,X1,X2),sK3(X0,X1,X2))
& less(X0,sK3(X0,X1,X2))
& less(sK3(X0,X1,X2),X2)
& terminates(sK2(X0,X1,X2),X1,sK3(X0,X1,X2)) )
| ~ stoppedIn(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X3,sK2(X0,X1,X2)),skolemize(X4,sK3(X0,X1,X2))],[f63]) ).
fof(f91,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ( happens(sK4(X0,X1),X1)
& terminates(sK4(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X2,sK4(X0,X1))],[f67]) ).
fof(f94,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ( happens(sK7(X0,X1),X1)
& releases(sK7(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f73]) ).
fof(f98,plain,
! [X2,X0,X1] :
( ( sP0(X2,X0,X1)
| ! [X4] :
( ~ holdsAt(waterLevel(X4),X2)
| overflow != X0
| waterLevel(X4) != X1 ) )
& ( ? [X4] :
( holdsAt(waterLevel(X4),X2)
& X0 = overflow
& waterLevel(X4) = X1 )
| ~ sP0(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f87]) ).
fof(f99,plain,
! [X0,X1,X2] :
( ( sP0(X0,X1,X2)
| ! [X3] :
( ~ holdsAt(waterLevel(X3),X0)
| overflow != X1
| waterLevel(X3) != X2 ) )
& ( ? [X4] :
( holdsAt(waterLevel(X4),X0)
& overflow = X1
& waterLevel(X4) = X2 )
| ~ sP0(X0,X1,X2) ) ),
inference(rectify,[],[f98]) ).
fof(f100,plain,
! [X0,X1,X2] :
( ( sP0(X0,X1,X2)
| ! [X3] :
( ~ holdsAt(waterLevel(X3),X0)
| overflow != X1
| waterLevel(X3) != X2 ) )
& ( ( holdsAt(waterLevel(sK9(X0,X1,X2)),X0)
& overflow = X1
& waterLevel(sK9(X0,X1,X2)) = X2 )
| ~ sP0(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X4,sK9(X0,X1,X2))],[f99]) ).
fof(f101,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ( ( tapOn != X0
| filling != X1 )
& ( overflow != X0
| spilling != X1 )
& ~ sP1(X2,X0,X1)
& ~ sP0(X2,X0,X1) ) )
& ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| sP1(X2,X0,X1)
| sP0(X2,X0,X1)
| ~ initiates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f89]) ).
fof(f102,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ( ( tapOn != X0
| filling != X1 )
& ( overflow != X0
| spilling != X1 )
& ~ sP1(X2,X0,X1)
& ~ sP0(X2,X0,X1) ) )
& ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| sP1(X2,X0,X1)
| sP0(X2,X0,X1)
| ~ initiates(X0,X1,X2) ) ),
inference(flattening,[],[f101]) ).
fof(f103,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(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(flattening,[],[f103]) ).
fof(f105,plain,
! [X0,X1,X2] :
( ( releases(X0,X1,X2)
| ! [X3] :
( tapOn != X0
| waterLevel(X3) != X1 ) )
& ( ? [X3] :
( X0 = tapOn
& X1 = waterLevel(X3) )
| ~ releases(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f15]) ).
fof(f106,plain,
! [X0,X1,X2] :
( ( releases(X0,X1,X2)
| ! [X3] :
( tapOn != X0
| waterLevel(X3) != X1 ) )
& ( ? [X4] :
( X0 = tapOn
& waterLevel(X4) = X1 )
| ~ releases(X0,X1,X2) ) ),
inference(rectify,[],[f105]) ).
fof(f107,plain,
! [X0,X1,X2] :
( ( releases(X0,X1,X2)
| ! [X3] :
( tapOn != X0
| waterLevel(X3) != X1 ) )
& ( ( X0 = tapOn
& waterLevel(sK10(X0,X1)) = X1 )
| ~ releases(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X4,sK10(X0,X1))],[f106]) ).
fof(f108,plain,
! [X0,X1] :
( ( happens(X0,X1)
| ( ( tapOn != X0
| n0 != X1 )
& ( ~ holdsAt(waterLevel(n3),X1)
| ~ holdsAt(filling,X1)
| overflow != X0 ) ) )
& ( ( X0 = tapOn
& X1 = n0 )
| ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow )
| ~ happens(X0,X1) ) ),
inference(nnf_transformation,[],[f16]) ).
fof(f109,plain,
! [X0,X1] :
( ( happens(X0,X1)
| ( ( tapOn != X0
| n0 != X1 )
& ( ~ holdsAt(waterLevel(n3),X1)
| ~ holdsAt(filling,X1)
| overflow != X0 ) ) )
& ( ( X0 = tapOn
& X1 = n0 )
| ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow )
| ~ happens(X0,X1) ) ),
inference(flattening,[],[f108]) ).
fof(f111,plain,
! [X0,X1] :
( ( less_or_equal(X0,X1)
| ( ~ less(X0,X1)
& X0 != X1 ) )
& ( less(X0,X1)
| X0 = X1
| ~ less_or_equal(X0,X1) ) ),
inference(nnf_transformation,[],[f37]) ).
fof(f112,plain,
! [X0,X1] :
( ( less_or_equal(X0,X1)
| ( ~ less(X0,X1)
& X0 != X1 ) )
& ( less(X0,X1)
| X0 = X1
| ~ less_or_equal(X0,X1) ) ),
inference(flattening,[],[f111]) ).
fof(f113,plain,
! [X0] :
( ( less(X0,n1)
| ~ less_or_equal(X0,n0) )
& ( less_or_equal(X0,n0)
| ~ less(X0,n1) ) ),
inference(nnf_transformation,[],[f39]) ).
fof(f114,plain,
! [X0] :
( ( less(X0,n2)
| ~ less_or_equal(X0,n1) )
& ( less_or_equal(X0,n1)
| ~ less(X0,n2) ) ),
inference(nnf_transformation,[],[f40]) ).
fof(f115,plain,
! [X0] :
( ( less(X0,n3)
| ~ less_or_equal(X0,n2) )
& ( less_or_equal(X0,n2)
| ~ less(X0,n3) ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f122,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(nnf_transformation,[],[f48]) ).
fof(f123,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(flattening,[],[f122]) ).
fof(f124,plain,
! [X2,X0,X1] :
( terminates(sK2(X0,X1,X2),X1,sK3(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f90]) ).
fof(f125,plain,
! [X2,X0,X1] :
( less(sK3(X0,X1,X2),X2)
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f90]) ).
fof(f127,plain,
! [X2,X0,X1] :
( happens(sK2(X0,X1,X2),sK3(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f90]) ).
fof(f128,plain,
! [X2,X3,X0,X1,X4] :
( ~ trajectory(X2,X1,X3,X4)
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1)
| ~ less(n0,X4)
| holdsAt(X3,plus(X1,X4))
| stoppedIn(X1,X2,plus(X1,X4)) ),
inference(cnf_transformation,[],[f65]) ).
fof(f130,plain,
! [X0,X1] :
( releasedAt(X0,plus(X1,n1))
| happens(sK4(X0,X1),X1)
| ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f91]) ).
fof(f135,plain,
! [X0,X1] :
( releases(sK7(X0,X1),X0,X1)
| releasedAt(X0,X1)
| ~ releasedAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f94]) ).
fof(f136,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| happens(sK7(X0,X1),X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f137,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f75]) ).
fof(f138,plain,
! [X2,X0,X1] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(cnf_transformation,[],[f77]) ).
fof(f139,plain,
! [X2,X0,X1] :
( ~ releases(X0,X2,X1)
| ~ happens(X0,X1)
| releasedAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f141,plain,
! [X2,X0,X1] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(cnf_transformation,[],[f81]) ).
fof(f149,plain,
! [X2,X3,X0,X1] :
( sP0(X0,X1,X2)
| ~ holdsAt(waterLevel(X3),X0)
| overflow != X1
| waterLevel(X3) != X2 ),
inference(cnf_transformation,[],[f100]) ).
fof(f154,plain,
! [X2,X0,X1] :
( ~ sP0(X2,X0,X1)
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f102]) ).
fof(f156,plain,
! [X2,X0,X1] :
( initiates(X0,X1,X2)
| overflow != X0
| spilling != X1 ),
inference(cnf_transformation,[],[f102]) ).
fof(f157,plain,
! [X2,X0,X1] :
( initiates(X0,X1,X2)
| tapOn != X0
| filling != X1 ),
inference(cnf_transformation,[],[f102]) ).
fof(f162,plain,
! [X2,X0,X1] :
( terminates(X0,X1,X2)
| overflow != X0
| filling != X1 ),
inference(cnf_transformation,[],[f104]) ).
fof(f165,plain,
! [X2,X0,X1] :
( ~ releases(X0,X1,X2)
| tapOn = X0 ),
inference(cnf_transformation,[],[f107]) ).
fof(f166,plain,
! [X2,X3,X0,X1] :
( releases(X0,X1,X2)
| tapOn != X0
| waterLevel(X3) != X1 ),
inference(cnf_transformation,[],[f107]) ).
fof(f168,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| holdsAt(filling,X1)
| n0 = X1 ),
inference(cnf_transformation,[],[f109]) ).
fof(f169,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| holdsAt(waterLevel(n3),X1)
| n0 = X1 ),
inference(cnf_transformation,[],[f109]) ).
fof(f173,plain,
! [X0,X1] :
( happens(X0,X1)
| ~ holdsAt(waterLevel(n3),X1)
| ~ holdsAt(filling,X1)
| overflow != X0 ),
inference(cnf_transformation,[],[f109]) ).
fof(f174,plain,
! [X0,X1] :
( happens(X0,X1)
| tapOn != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f109]) ).
fof(f175,plain,
! [X2,X3,X0,X1] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(cnf_transformation,[],[f83]) ).
fof(f186,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f27]) ).
fof(f188,plain,
n3 = plus(n0,n3),
inference(cnf_transformation,[],[f29]) ).
fof(f189,plain,
n2 = plus(n1,n1),
inference(cnf_transformation,[],[f30]) ).
fof(f190,plain,
n3 = plus(n1,n2),
inference(cnf_transformation,[],[f31]) ).
fof(f191,plain,
plus(n1,n3) = n4,
inference(cnf_transformation,[],[f32]) ).
fof(f195,plain,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[],[f36]) ).
fof(f196,plain,
! [X0,X1] :
( ~ less_or_equal(X0,X1)
| X0 = X1
| less(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f197,plain,
! [X0,X1] :
( less_or_equal(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f112]) ).
fof(f198,plain,
! [X0,X1] :
( ~ less(X0,X1)
| less_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f199,plain,
! [X0] : ~ less(X0,n0),
inference(cnf_transformation,[],[f86]) ).
fof(f200,plain,
! [X0] :
( ~ less(X0,n1)
| less_or_equal(X0,n0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f201,plain,
! [X0] :
( ~ less_or_equal(X0,n0)
| less(X0,n1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f202,plain,
! [X0] :
( ~ less(X0,n2)
| less_or_equal(X0,n1) ),
inference(cnf_transformation,[],[f114]) ).
fof(f203,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| less(X0,n2) ),
inference(cnf_transformation,[],[f114]) ).
fof(f204,plain,
! [X0] :
( ~ less(X0,n3)
| less_or_equal(X0,n2) ),
inference(cnf_transformation,[],[f115]) ).
fof(f205,plain,
! [X0] :
( ~ less_or_equal(X0,n2)
| less(X0,n3) ),
inference(cnf_transformation,[],[f115]) ).
fof(f219,plain,
! [X0,X1] :
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f123]) ).
fof(f220,plain,
! [X0,X1] :
( less(X1,X0)
| less(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f123]) ).
fof(f221,plain,
holdsAt(waterLevel(n0),n0),
inference(cnf_transformation,[],[f49]) ).
fof(f224,plain,
! [X0] : ~ releasedAt(waterLevel(X0),n0),
inference(cnf_transformation,[],[f52]) ).
fof(f227,plain,
~ holdsAt(spilling,n4),
inference(cnf_transformation,[],[f58]) ).
fof(f230,plain,
! [X2,X3,X0] :
( sP0(X0,overflow,X2)
| ~ holdsAt(waterLevel(X3),X0)
| waterLevel(X3) != X2 ),
inference(equality_resolution,[],[f149]) ).
fof(f231,plain,
! [X3,X0] :
( sP0(X0,overflow,waterLevel(X3))
| ~ holdsAt(waterLevel(X3),X0) ),
inference(equality_resolution,[],[f230]) ).
fof(f232,plain,
! [X2,X1] :
( initiates(tapOn,X1,X2)
| filling != X1 ),
inference(equality_resolution,[],[f157]) ).
fof(f233,plain,
! [X2] : initiates(tapOn,filling,X2),
inference(equality_resolution,[],[f232]) ).
fof(f234,plain,
! [X2,X1] :
( initiates(overflow,X1,X2)
| spilling != X1 ),
inference(equality_resolution,[],[f156]) ).
fof(f235,plain,
! [X2] : initiates(overflow,spilling,X2),
inference(equality_resolution,[],[f234]) ).
fof(f238,plain,
! [X2,X1] :
( terminates(overflow,X1,X2)
| filling != X1 ),
inference(equality_resolution,[],[f162]) ).
fof(f239,plain,
! [X2] : terminates(overflow,filling,X2),
inference(equality_resolution,[],[f238]) ).
fof(f240,plain,
! [X2,X3,X1] :
( releases(tapOn,X1,X2)
| waterLevel(X3) != X1 ),
inference(equality_resolution,[],[f166]) ).
fof(f241,plain,
! [X2,X3] : releases(tapOn,waterLevel(X3),X2),
inference(equality_resolution,[],[f240]) ).
fof(f242,plain,
! [X1] :
( happens(tapOn,X1)
| n0 != X1 ),
inference(equality_resolution,[],[f174]) ).
fof(f243,plain,
happens(tapOn,n0),
inference(equality_resolution,[],[f242]) ).
fof(f244,plain,
! [X1] :
( ~ holdsAt(waterLevel(n3),X1)
| happens(overflow,X1)
| ~ holdsAt(filling,X1) ),
inference(equality_resolution,[],[f173]) ).
fof(f245,plain,
! [X3,X0,X1] :
( trajectory(filling,X1,waterLevel(plus(X0,X3)),X3)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(equality_resolution,[],[f175]) ).
fof(f247,plain,
! [X1] : less_or_equal(X1,X1),
inference(equality_resolution,[],[f197]) ).
fof(f323,plain,
! [X0,X1] :
( ~ initiates(X1,X0,n0)
| ~ happens(X1,n0)
| ~ releasedAt(X0,n1) ),
inference(superposition,[],[f141,f186]) ).
fof(f327,plain,
! [X0,X1] :
( ~ initiates(X1,X0,n1)
| ~ happens(X1,n1)
| ~ releasedAt(X0,n2) ),
inference(superposition,[],[f141,f189]) ).
fof(f329,plain,
! [X0,X1] :
( ~ terminates(X1,X0,n1)
| ~ happens(X1,n1)
| ~ holdsAt(X0,n2) ),
inference(superposition,[],[f138,f189]) ).
fof(f358,plain,
less(n0,n1),
inference(resolution,[],[f201,f247]) ).
fof(f367,plain,
less_or_equal(n0,n1),
inference(resolution,[],[f358,f198]) ).
fof(f388,plain,
less(n1,n2),
inference(resolution,[],[f203,f247]) ).
fof(f389,plain,
less(n0,n2),
inference(resolution,[],[f203,f367]) ).
fof(f403,plain,
less_or_equal(n0,n2),
inference(resolution,[],[f389,f198]) ).
fof(f426,plain,
less(n2,n3),
inference(resolution,[],[f205,f247]) ).
fof(f427,plain,
less(n0,n3),
inference(resolution,[],[f205,f403]) ).
fof(f2344,plain,
! [X2,X0,X1] :
( ~ releasedAt(X1,plus(n1,X0))
| ~ happens(X2,X0)
| ~ initiates(X2,X1,X0) ),
inference(superposition,[],[f141,f195]) ).
fof(f2346,plain,
! [X2,X0,X1] :
( ~ holdsAt(X1,plus(n1,X0))
| ~ happens(X2,X0)
| ~ terminates(X2,X1,X0) ),
inference(superposition,[],[f138,f195]) ).
fof(f5233,plain,
! [X0] :
( less_or_equal(X0,n0)
| n1 = X0
| less(n1,X0) ),
inference(resolution,[],[f220,f200]) ).
fof(f5235,plain,
! [X0] :
( less_or_equal(X0,n1)
| n2 = X0
| less(n2,X0) ),
inference(resolution,[],[f220,f202]) ).
fof(f5423,plain,
! [X0] :
( n1 = X0
| less(n1,X0)
| n0 = X0
| less(X0,n0) ),
inference(resolution,[],[f5233,f196]) ).
fof(f5424,plain,
! [X0] :
( less(n1,X0)
| n1 = X0
| n0 = X0 ),
inference(forward_subsumption_resolution,[],[f5423,f199]) ).
fof(f6737,plain,
! [X0] :
( less(n2,X0)
| less(X0,n1)
| n1 = X0
| n2 = X0 ),
inference(resolution,[],[f5235,f196]) ).
fof(f8528,plain,
! [X0,X1] :
( less_or_equal(sK3(X0,X1,n3),n2)
| ~ stoppedIn(X0,X1,n3) ),
inference(resolution,[],[f125,f204]) ).
fof(f8663,plain,
! [X0] :
( ~ less(X0,n1)
| n0 = X0
| n1 = X0 ),
inference(resolution,[],[f5424,f219]) ).
fof(f13096,plain,
( ~ happens(overflow,n1)
| ~ holdsAt(filling,n2) ),
inference(resolution,[],[f329,f239]) ).
fof(f13107,plain,
! [X0,X1] :
( ~ terminates(X1,X0,n2)
| ~ happens(X1,n2)
| ~ holdsAt(X0,n3) ),
inference(superposition,[],[f2346,f190]) ).
fof(f13252,plain,
( ~ happens(overflow,n2)
| ~ holdsAt(filling,n3) ),
inference(resolution,[],[f13107,f239]) ).
fof(f13769,definition,
( spl11_133
<=> holdsAt(filling,n1) ),
introduced(definition,[new_symbols(definition,[spl11_133])],[avatar_definition]) ).
fof(f13770,plain,
( holdsAt(filling,n1)
| ~ spl11_133 ),
inference(avatar_component_clause,[],[f13769]) ).
fof(f13771,plain,
( ~ holdsAt(filling,n1)
| spl11_133 ),
inference(avatar_component_clause,[],[f13769]) ).
fof(f13785,plain,
! [X0,X1] :
( initiates(overflow,waterLevel(X0),X1)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(resolution,[],[f154,f231]) ).
fof(f13805,plain,
! [X0] :
( holdsAt(filling,plus(X0,n1))
| ~ happens(tapOn,X0) ),
inference(resolution,[],[f137,f233]) ).
fof(f13806,plain,
! [X0] :
( holdsAt(spilling,plus(X0,n1))
| ~ happens(overflow,X0) ),
inference(resolution,[],[f137,f235]) ).
fof(f13810,plain,
! [X0,X1] :
( holdsAt(waterLevel(X1),plus(X0,n1))
| ~ happens(overflow,X0)
| ~ holdsAt(waterLevel(X1),X0) ),
inference(resolution,[],[f137,f13785]) ).
fof(f13821,plain,
( ~ happens(tapOn,n0)
| ~ releasedAt(filling,n1) ),
inference(resolution,[],[f323,f233]) ).
fof(f13827,plain,
~ releasedAt(filling,n1),
inference(forward_subsumption_resolution,[],[f13821,f243]) ).
fof(f13848,plain,
! [X0,X1] :
( ~ initiates(X1,X0,n2)
| ~ happens(X1,n2)
| ~ releasedAt(X0,n3) ),
inference(superposition,[],[f2344,f190]) ).
fof(f13870,plain,
! [X0,X1] :
( ~ terminates(X1,filling,X0)
| ~ happens(X1,X0)
| ~ happens(tapOn,X0) ),
inference(resolution,[],[f13805,f138]) ).
fof(f13872,plain,
! [X0] :
( holdsAt(filling,plus(n1,X0))
| ~ happens(tapOn,X0) ),
inference(superposition,[],[f13805,f195]) ).
fof(f13874,plain,
( holdsAt(filling,n1)
| ~ happens(tapOn,n0) ),
inference(superposition,[],[f13805,f186]) ).
fof(f13876,plain,
( ~ happens(tapOn,n0)
| spl11_133 ),
inference(forward_subsumption_resolution,[],[f13874,f13771]) ).
fof(f13877,plain,
( $false
| spl11_133 ),
inference(forward_subsumption_resolution,[],[f13876,f243]) ).
fof(f13878,plain,
spl11_133,
inference(avatar_contradiction_clause,[],[f13877]) ).
fof(f13917,plain,
! [X0,X1] :
( releasedAt(waterLevel(X1),plus(X0,n1))
| ~ happens(tapOn,X0) ),
inference(resolution,[],[f139,f241]) ).
fof(f13949,plain,
! [X0] :
( releasedAt(waterLevel(X0),n1)
| ~ happens(tapOn,n0) ),
inference(superposition,[],[f13917,f186]) ).
fof(f13951,plain,
! [X0] : releasedAt(waterLevel(X0),n1),
inference(forward_subsumption_resolution,[],[f13949,f243]) ).
fof(f14009,plain,
! [X0] :
( trajectory(filling,X0,waterLevel(n3),n3)
| ~ holdsAt(waterLevel(n0),X0) ),
inference(superposition,[],[f245,f188]) ).
fof(f14169,plain,
! [X0] :
( less(n2,X0)
| n1 = X0
| n2 = X0
| n0 = X0
| n1 = X0 ),
inference(resolution,[],[f6737,f8663]) ).
fof(f14222,plain,
! [X0] :
( less(n2,X0)
| n1 = X0
| n2 = X0
| n0 = X0 ),
inference(duplicate_literal_removal,[],[f14169]) ).
fof(f15691,plain,
! [X0] :
( ~ less(X0,n2)
| n2 = X0
| n0 = X0
| n1 = X0 ),
inference(resolution,[],[f14222,f219]) ).
fof(f16042,plain,
( ~ happens(overflow,n1)
| ~ releasedAt(spilling,n2) ),
inference(resolution,[],[f327,f235]) ).
fof(f16044,plain,
! [X0] :
( ~ happens(overflow,n1)
| ~ releasedAt(waterLevel(X0),n2)
| ~ holdsAt(waterLevel(X0),n1) ),
inference(resolution,[],[f327,f13785]) ).
fof(f16077,plain,
( ~ happens(overflow,n2)
| ~ releasedAt(spilling,n3) ),
inference(resolution,[],[f13848,f235]) ).
fof(f16104,definition,
( spl11_159
<=> holdsAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl11_159])],[avatar_definition]) ).
fof(f16105,plain,
( holdsAt(filling,n2)
| ~ spl11_159 ),
inference(avatar_component_clause,[],[f16104]) ).
fof(f16106,plain,
( ~ holdsAt(filling,n2)
| spl11_159 ),
inference(avatar_component_clause,[],[f16104]) ).
fof(f16108,definition,
( spl11_160
<=> happens(overflow,n1) ),
introduced(definition,[new_symbols(definition,[spl11_160])],[avatar_definition]) ).
fof(f16109,plain,
( happens(overflow,n1)
| ~ spl11_160 ),
inference(avatar_component_clause,[],[f16108]) ).
fof(f16110,plain,
( ~ happens(overflow,n1)
| spl11_160 ),
inference(avatar_component_clause,[],[f16108]) ).
fof(f16111,plain,
( ~ spl11_159
| ~ spl11_160 ),
inference(avatar_split_clause,[],[f13096,f16108,f16104]) ).
fof(f16118,definition,
( spl11_162
<=> happens(overflow,n3) ),
introduced(definition,[new_symbols(definition,[spl11_162])],[avatar_definition]) ).
fof(f16120,plain,
( ~ happens(overflow,n3)
| spl11_162 ),
inference(avatar_component_clause,[],[f16118]) ).
fof(f16124,definition,
( spl11_163
<=> holdsAt(filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_163])],[avatar_definition]) ).
fof(f16125,plain,
( holdsAt(filling,n3)
| ~ spl11_163 ),
inference(avatar_component_clause,[],[f16124]) ).
fof(f16126,plain,
( ~ holdsAt(filling,n3)
| spl11_163 ),
inference(avatar_component_clause,[],[f16124]) ).
fof(f16128,definition,
( spl11_164
<=> happens(overflow,n2) ),
introduced(definition,[new_symbols(definition,[spl11_164])],[avatar_definition]) ).
fof(f16130,plain,
( ~ happens(overflow,n2)
| spl11_164 ),
inference(avatar_component_clause,[],[f16128]) ).
fof(f16131,plain,
( ~ spl11_163
| ~ spl11_164 ),
inference(avatar_split_clause,[],[f13252,f16128,f16124]) ).
fof(f16347,plain,
! [X0] :
( holdsAt(spilling,plus(n1,X0))
| ~ happens(overflow,X0) ),
inference(superposition,[],[f13806,f195]) ).
fof(f16350,plain,
( holdsAt(spilling,n2)
| ~ happens(overflow,n1) ),
inference(superposition,[],[f13806,f189]) ).
fof(f16386,definition,
( spl11_168
<=> n0 = n1 ),
introduced(definition,[new_symbols(definition,[spl11_168])],[avatar_definition]) ).
fof(f16387,plain,
( n0 != n1
| spl11_168 ),
inference(avatar_component_clause,[],[f16386]) ).
fof(f16388,plain,
( n0 = n1
| ~ spl11_168 ),
inference(avatar_component_clause,[],[f16386]) ).
fof(f16390,definition,
( spl11_169
<=> holdsAt(waterLevel(n3),n1) ),
introduced(definition,[new_symbols(definition,[spl11_169])],[avatar_definition]) ).
fof(f16391,plain,
( ~ holdsAt(waterLevel(n3),n1)
| spl11_169 ),
inference(avatar_component_clause,[],[f16390]) ).
fof(f16392,plain,
( holdsAt(waterLevel(n3),n1)
| ~ spl11_169 ),
inference(avatar_component_clause,[],[f16390]) ).
fof(f16403,plain,
( ! [X0] : ~ releasedAt(waterLevel(X0),n1)
| ~ spl11_168 ),
inference(superposition,[],[f224,f16388]) ).
fof(f16453,plain,
( $false
| ~ spl11_168 ),
inference(forward_subsumption_resolution,[],[f16403,f13951]) ).
fof(f16454,plain,
~ spl11_168,
inference(avatar_contradiction_clause,[],[f16453]) ).
fof(f16458,plain,
( happens(overflow,n1)
| ~ holdsAt(filling,n1)
| ~ spl11_169 ),
inference(resolution,[],[f16392,f244]) ).
fof(f16464,plain,
( happens(overflow,n1)
| ~ spl11_133
| ~ spl11_169 ),
inference(forward_subsumption_resolution,[],[f16458,f13770]) ).
fof(f16465,plain,
( spl11_160
| ~ spl11_133
| ~ spl11_169 ),
inference(avatar_split_clause,[],[f16464,f16390,f13769,f16108]) ).
fof(f16523,plain,
! [X0,X1] :
( ~ releasedAt(X1,plus(n1,X0))
| releasedAt(X1,X0)
| happens(sK7(X1,X0),X0) ),
inference(superposition,[],[f136,f195]) ).
fof(f16526,plain,
! [X0] :
( happens(sK7(X0,n1),n1)
| releasedAt(X0,n1)
| ~ releasedAt(X0,n2) ),
inference(superposition,[],[f136,f189]) ).
fof(f16864,plain,
( holdsAt(filling,n3)
| ~ happens(tapOn,n2) ),
inference(superposition,[],[f13872,f190]) ).
fof(f16885,plain,
( holdsAt(spilling,n4)
| ~ happens(overflow,n3) ),
inference(superposition,[],[f16347,f191]) ).
fof(f16886,plain,
( holdsAt(spilling,n3)
| ~ happens(overflow,n2) ),
inference(superposition,[],[f16347,f190]) ).
fof(f16938,definition,
( spl11_178
<=> releasedAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl11_178])],[avatar_definition]) ).
fof(f16939,plain,
( releasedAt(filling,n2)
| ~ spl11_178 ),
inference(avatar_component_clause,[],[f16938]) ).
fof(f16940,plain,
( ~ releasedAt(filling,n2)
| spl11_178 ),
inference(avatar_component_clause,[],[f16938]) ).
fof(f17380,definition,
( spl11_191
<=> n0 = n2 ),
introduced(definition,[new_symbols(definition,[spl11_191])],[avatar_definition]) ).
fof(f17381,plain,
( n0 != n2
| spl11_191 ),
inference(avatar_component_clause,[],[f17380]) ).
fof(f17382,plain,
( n0 = n2
| ~ spl11_191 ),
inference(avatar_component_clause,[],[f17380]) ).
fof(f17384,definition,
( spl11_192
<=> holdsAt(waterLevel(n3),n2) ),
introduced(definition,[new_symbols(definition,[spl11_192])],[avatar_definition]) ).
fof(f17385,plain,
( ~ holdsAt(waterLevel(n3),n2)
| spl11_192 ),
inference(avatar_component_clause,[],[f17384]) ).
fof(f17386,plain,
( holdsAt(waterLevel(n3),n2)
| ~ spl11_192 ),
inference(avatar_component_clause,[],[f17384]) ).
fof(f17394,plain,
( less(n1,n0)
| ~ spl11_191 ),
inference(superposition,[],[f388,f17382]) ).
fof(f17491,plain,
( $false
| ~ spl11_191 ),
inference(forward_subsumption_resolution,[],[f17394,f199]) ).
fof(f17492,plain,
~ spl11_191,
inference(avatar_contradiction_clause,[],[f17491]) ).
fof(f17497,plain,
( happens(overflow,n2)
| ~ holdsAt(filling,n2)
| ~ spl11_192 ),
inference(resolution,[],[f17386,f244]) ).
fof(f17501,plain,
( ~ holdsAt(filling,n2)
| spl11_164
| ~ spl11_192 ),
inference(forward_subsumption_resolution,[],[f17497,f16130]) ).
fof(f17502,plain,
( $false
| ~ spl11_159
| spl11_164
| ~ spl11_192 ),
inference(forward_subsumption_resolution,[],[f17501,f16105]) ).
fof(f17503,plain,
( ~ spl11_159
| spl11_164
| ~ spl11_192 ),
inference(avatar_contradiction_clause,[],[f17502]) ).
fof(f17509,definition,
( spl11_193
<=> releasedAt(filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_193])],[avatar_definition]) ).
fof(f17510,plain,
( releasedAt(filling,n3)
| ~ spl11_193 ),
inference(avatar_component_clause,[],[f17509]) ).
fof(f17511,plain,
( ~ releasedAt(filling,n3)
| spl11_193 ),
inference(avatar_component_clause,[],[f17509]) ).
fof(f17513,definition,
( spl11_194
<=> happens(tapOn,n2) ),
introduced(definition,[new_symbols(definition,[spl11_194])],[avatar_definition]) ).
fof(f17515,plain,
( ~ happens(tapOn,n2)
| spl11_194 ),
inference(avatar_component_clause,[],[f17513]) ).
fof(f17539,definition,
( spl11_197
<=> n0 = n3 ),
introduced(definition,[new_symbols(definition,[spl11_197])],[avatar_definition]) ).
fof(f17540,plain,
( n0 != n3
| spl11_197 ),
inference(avatar_component_clause,[],[f17539]) ).
fof(f17541,plain,
( n0 = n3
| ~ spl11_197 ),
inference(avatar_component_clause,[],[f17539]) ).
fof(f17543,definition,
( spl11_198
<=> holdsAt(waterLevel(n3),n3) ),
introduced(definition,[new_symbols(definition,[spl11_198])],[avatar_definition]) ).
fof(f17544,plain,
( ~ holdsAt(waterLevel(n3),n3)
| spl11_198 ),
inference(avatar_component_clause,[],[f17543]) ).
fof(f17545,plain,
( holdsAt(waterLevel(n3),n3)
| ~ spl11_198 ),
inference(avatar_component_clause,[],[f17543]) ).
fof(f17554,plain,
( less(n2,n0)
| ~ spl11_197 ),
inference(superposition,[],[f426,f17541]) ).
fof(f17651,plain,
( $false
| ~ spl11_197 ),
inference(forward_subsumption_resolution,[],[f17554,f199]) ).
fof(f17652,plain,
~ spl11_197,
inference(avatar_contradiction_clause,[],[f17651]) ).
fof(f17657,plain,
( happens(overflow,n3)
| ~ holdsAt(filling,n3)
| ~ spl11_198 ),
inference(resolution,[],[f17545,f244]) ).
fof(f17661,plain,
( ~ holdsAt(filling,n3)
| spl11_162
| ~ spl11_198 ),
inference(forward_subsumption_resolution,[],[f17657,f16120]) ).
fof(f17662,plain,
( $false
| spl11_162
| ~ spl11_163
| ~ spl11_198 ),
inference(forward_subsumption_resolution,[],[f17661,f16125]) ).
fof(f17663,plain,
( spl11_162
| ~ spl11_163
| ~ spl11_198 ),
inference(avatar_contradiction_clause,[],[f17662]) ).
fof(f17698,plain,
! [X0] :
( releasedAt(X0,n1)
| ~ releasedAt(X0,n2)
| holdsAt(waterLevel(n3),n1)
| n0 = n1 ),
inference(resolution,[],[f16526,f169]) ).
fof(f17703,plain,
( ! [X0] :
( releasedAt(X0,n1)
| ~ releasedAt(X0,n2)
| n0 = n1 )
| spl11_169 ),
inference(forward_subsumption_resolution,[],[f17698,f16391]) ).
fof(f17705,plain,
( ! [X0] :
( ~ releasedAt(X0,n2)
| releasedAt(X0,n1) )
| spl11_168
| spl11_169 ),
inference(forward_subsumption_resolution,[],[f17703,f16387]) ).
fof(f17720,plain,
( releasedAt(filling,n1)
| spl11_168
| spl11_169
| ~ spl11_178 ),
inference(resolution,[],[f17705,f16939]) ).
fof(f17721,plain,
( $false
| spl11_168
| spl11_169
| ~ spl11_178 ),
inference(forward_subsumption_resolution,[],[f17720,f13827]) ).
fof(f17722,plain,
( spl11_168
| spl11_169
| ~ spl11_178 ),
inference(avatar_contradiction_clause,[],[f17721]) ).
fof(f17748,plain,
! [X0] :
( happens(sK7(X0,n3),n3)
| releasedAt(X0,n3)
| ~ releasedAt(X0,n4) ),
inference(superposition,[],[f16523,f191]) ).
fof(f17749,plain,
! [X0] :
( happens(sK7(X0,n2),n2)
| releasedAt(X0,n2)
| ~ releasedAt(X0,n3) ),
inference(superposition,[],[f16523,f190]) ).
fof(f17769,plain,
! [X0] :
( holdsAt(waterLevel(X0),n2)
| ~ happens(overflow,n1)
| ~ holdsAt(waterLevel(X0),n1) ),
inference(superposition,[],[f13810,f189]) ).
fof(f17844,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| tapOn = sK7(X0,X1) ),
inference(resolution,[],[f135,f165]) ).
fof(f17915,plain,
! [X0,X1] :
( ~ releasedAt(X1,plus(n1,X0))
| releasedAt(X1,X0)
| tapOn = sK7(X1,X0) ),
inference(superposition,[],[f17844,f195]) ).
fof(f18298,definition,
( spl11_218
<=> ! [X0] :
( ~ releasedAt(X0,n3)
| releasedAt(X0,n2) ) ),
introduced(definition,[new_symbols(definition,[spl11_218])],[avatar_definition]) ).
fof(f18299,plain,
( ! [X0] :
( ~ releasedAt(X0,n3)
| releasedAt(X0,n2) )
| ~ spl11_218 ),
inference(avatar_component_clause,[],[f18298]) ).
fof(f18316,definition,
( spl11_219
<=> releasedAt(spilling,n2) ),
introduced(definition,[new_symbols(definition,[spl11_219])],[avatar_definition]) ).
fof(f18318,plain,
( ~ releasedAt(spilling,n2)
| spl11_219 ),
inference(avatar_component_clause,[],[f18316]) ).
fof(f18319,plain,
( ~ spl11_219
| ~ spl11_160 ),
inference(avatar_split_clause,[],[f16042,f16108,f18316]) ).
fof(f18329,definition,
( spl11_220
<=> ! [X0] :
( ~ releasedAt(X0,n4)
| releasedAt(X0,n3) ) ),
introduced(definition,[new_symbols(definition,[spl11_220])],[avatar_definition]) ).
fof(f18330,plain,
( ! [X0] :
( ~ releasedAt(X0,n4)
| releasedAt(X0,n3) )
| ~ spl11_220 ),
inference(avatar_component_clause,[],[f18329]) ).
fof(f20828,plain,
! [X0,X1] :
( releasedAt(X1,plus(n1,X0))
| happens(sK4(X1,X0),X0)
| ~ holdsAt(X1,X0)
| holdsAt(X1,plus(n1,X0)) ),
inference(superposition,[],[f130,f195]) ).
fof(f20831,plain,
! [X0] :
( happens(sK4(X0,n1),n1)
| releasedAt(X0,n2)
| ~ holdsAt(X0,n1)
| holdsAt(X0,n2) ),
inference(superposition,[],[f130,f189]) ).
fof(f21082,plain,
! [X0] :
( releasedAt(X0,n2)
| ~ holdsAt(X0,n1)
| holdsAt(X0,n2)
| holdsAt(waterLevel(n3),n1)
| n0 = n1 ),
inference(resolution,[],[f20831,f169]) ).
fof(f21087,plain,
( ! [X0] :
( releasedAt(X0,n2)
| ~ holdsAt(X0,n1)
| holdsAt(X0,n2)
| n0 = n1 )
| spl11_169 ),
inference(forward_subsumption_resolution,[],[f21082,f16391]) ).
fof(f21089,plain,
( ! [X0] :
( ~ holdsAt(X0,n1)
| releasedAt(X0,n2)
| holdsAt(X0,n2) )
| spl11_168
| spl11_169 ),
inference(forward_subsumption_resolution,[],[f21087,f16387]) ).
fof(f21090,plain,
( releasedAt(filling,n2)
| holdsAt(filling,n2)
| ~ spl11_133
| spl11_168
| spl11_169 ),
inference(resolution,[],[f21089,f13770]) ).
fof(f21093,plain,
( holdsAt(filling,n2)
| ~ spl11_133
| spl11_168
| spl11_169
| spl11_178 ),
inference(forward_subsumption_resolution,[],[f21090,f16940]) ).
fof(f21094,plain,
( $false
| ~ spl11_133
| spl11_159
| spl11_168
| spl11_169
| spl11_178 ),
inference(forward_subsumption_resolution,[],[f21093,f16106]) ).
fof(f21095,plain,
( ~ spl11_133
| spl11_159
| spl11_168
| spl11_169
| spl11_178 ),
inference(avatar_contradiction_clause,[],[f21094]) ).
fof(f22418,plain,
! [X0] :
( happens(sK4(X0,n3),n3)
| releasedAt(X0,n4)
| ~ holdsAt(X0,n3)
| holdsAt(X0,n4) ),
inference(superposition,[],[f20828,f191]) ).
fof(f22419,plain,
! [X0] :
( happens(sK4(X0,n2),n2)
| releasedAt(X0,n3)
| ~ holdsAt(X0,n2)
| holdsAt(X0,n3) ),
inference(superposition,[],[f20828,f190]) ).
fof(f22458,plain,
! [X0] :
( releasedAt(X0,n4)
| ~ holdsAt(X0,n3)
| holdsAt(X0,n4)
| holdsAt(filling,n3)
| n0 = n3 ),
inference(resolution,[],[f22418,f168]) ).
fof(f22484,plain,
( ! [X0] :
( releasedAt(X0,n4)
| ~ holdsAt(X0,n3)
| holdsAt(X0,n4)
| holdsAt(filling,n3) )
| spl11_197 ),
inference(forward_subsumption_resolution,[],[f22458,f17540]) ).
fof(f22568,plain,
! [X0] :
( releasedAt(X0,n3)
| ~ holdsAt(X0,n2)
| holdsAt(X0,n3)
| holdsAt(filling,n2)
| n0 = n2 ),
inference(resolution,[],[f22419,f168]) ).
fof(f22569,plain,
! [X0] :
( releasedAt(X0,n3)
| ~ holdsAt(X0,n2)
| holdsAt(X0,n3)
| holdsAt(waterLevel(n3),n2)
| n0 = n2 ),
inference(resolution,[],[f22419,f169]) ).
fof(f22734,plain,
( ! [X0] :
( releasedAt(X0,n3)
| ~ holdsAt(X0,n2)
| holdsAt(X0,n3)
| holdsAt(waterLevel(n3),n2) )
| spl11_191 ),
inference(forward_subsumption_resolution,[],[f22569,f17381]) ).
fof(f22781,plain,
( ! [X0] :
( releasedAt(X0,n3)
| ~ holdsAt(X0,n2)
| holdsAt(X0,n3)
| holdsAt(filling,n2) )
| spl11_191 ),
inference(forward_subsumption_resolution,[],[f22568,f17381]) ).
fof(f22794,definition,
( spl11_261
<=> ! [X0] :
( ~ releasedAt(waterLevel(X0),n2)
| ~ holdsAt(waterLevel(X0),n1) ) ),
introduced(definition,[new_symbols(definition,[spl11_261])],[avatar_definition]) ).
fof(f22795,plain,
( ! [X0] :
( ~ releasedAt(waterLevel(X0),n2)
| ~ holdsAt(waterLevel(X0),n1) )
| ~ spl11_261 ),
inference(avatar_component_clause,[],[f22794]) ).
fof(f22796,plain,
( spl11_261
| ~ spl11_160 ),
inference(avatar_split_clause,[],[f16044,f16108,f22794]) ).
fof(f22864,plain,
( holdsAt(spilling,n2)
| ~ spl11_160 ),
inference(forward_subsumption_resolution,[],[f16350,f16109]) ).
fof(f23217,plain,
( ! [X0] :
( ~ holdsAt(X0,n2)
| releasedAt(X0,n3)
| holdsAt(X0,n3) )
| spl11_159
| spl11_191 ),
inference(forward_subsumption_resolution,[],[f22781,f16106]) ).
fof(f23230,plain,
~ happens(overflow,n3),
inference(forward_subsumption_resolution,[],[f16885,f227]) ).
fof(f23235,plain,
~ spl11_162,
inference(avatar_split_clause,[],[f23230,f16118]) ).
fof(f23277,plain,
( releasedAt(spilling,n3)
| holdsAt(spilling,n3)
| spl11_159
| ~ spl11_160
| spl11_191 ),
inference(resolution,[],[f23217,f22864]) ).
fof(f23278,plain,
( releasedAt(waterLevel(n3),n3)
| holdsAt(waterLevel(n3),n3)
| spl11_159
| spl11_191
| ~ spl11_192 ),
inference(resolution,[],[f23217,f17386]) ).
fof(f23282,definition,
( spl11_276
<=> holdsAt(spilling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_276])],[avatar_definition]) ).
fof(f23283,plain,
( ~ holdsAt(spilling,n3)
| spl11_276 ),
inference(avatar_component_clause,[],[f23282]) ).
fof(f23284,plain,
( holdsAt(spilling,n3)
| ~ spl11_276 ),
inference(avatar_component_clause,[],[f23282]) ).
fof(f23286,definition,
( spl11_277
<=> releasedAt(spilling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_277])],[avatar_definition]) ).
fof(f23288,plain,
( releasedAt(spilling,n3)
| ~ spl11_277 ),
inference(avatar_component_clause,[],[f23286]) ).
fof(f23289,plain,
( spl11_276
| spl11_277
| spl11_159
| ~ spl11_160
| spl11_191 ),
inference(avatar_split_clause,[],[f23277,f17380,f16108,f16104,f23286,f23282]) ).
fof(f23423,plain,
! [X0] :
( releasedAt(X0,n3)
| ~ releasedAt(X0,n4)
| holdsAt(filling,n3)
| n0 = n3 ),
inference(resolution,[],[f17748,f168]) ).
fof(f23430,plain,
( ! [X0] :
( releasedAt(X0,n3)
| ~ releasedAt(X0,n4)
| n0 = n3 )
| spl11_163 ),
inference(forward_subsumption_resolution,[],[f23423,f16126]) ).
fof(f23432,plain,
( ! [X0] :
( releasedAt(X0,n3)
| ~ releasedAt(X0,n4) )
| spl11_163
| spl11_197 ),
inference(forward_subsumption_resolution,[],[f23430,f17540]) ).
fof(f23433,plain,
( spl11_220
| spl11_163
| spl11_197 ),
inference(avatar_split_clause,[],[f23432,f17539,f16124,f18329]) ).
fof(f23472,plain,
! [X0] :
( releasedAt(X0,n2)
| ~ releasedAt(X0,n3)
| holdsAt(filling,n2)
| n0 = n2 ),
inference(resolution,[],[f17749,f168]) ).
fof(f23480,plain,
( ! [X0] :
( releasedAt(X0,n2)
| ~ releasedAt(X0,n3)
| n0 = n2 )
| spl11_159 ),
inference(forward_subsumption_resolution,[],[f23472,f16106]) ).
fof(f23483,plain,
( ! [X0] :
( releasedAt(X0,n2)
| ~ releasedAt(X0,n3) )
| spl11_159
| spl11_191 ),
inference(forward_subsumption_resolution,[],[f23480,f17381]) ).
fof(f23504,plain,
( spl11_218
| spl11_159
| spl11_191 ),
inference(avatar_split_clause,[],[f23483,f17380,f16104,f18298]) ).
fof(f23562,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n1)
| holdsAt(waterLevel(X0),n2) )
| ~ spl11_160 ),
inference(forward_subsumption_resolution,[],[f17769,f16109]) ).
fof(f23566,plain,
( holdsAt(waterLevel(n3),n2)
| ~ spl11_160
| ~ spl11_169 ),
inference(resolution,[],[f23562,f16392]) ).
fof(f23669,plain,
( ! [X0] :
( ~ holdsAt(X0,n3)
| releasedAt(X0,n4)
| holdsAt(X0,n4) )
| spl11_163
| spl11_197 ),
inference(forward_subsumption_resolution,[],[f22484,f16126]) ).
fof(f23670,plain,
( releasedAt(spilling,n4)
| holdsAt(spilling,n4)
| spl11_163
| spl11_197
| ~ spl11_276 ),
inference(resolution,[],[f23669,f23284]) ).
fof(f23676,plain,
( releasedAt(spilling,n4)
| spl11_163
| spl11_197
| ~ spl11_276 ),
inference(forward_subsumption_resolution,[],[f23670,f227]) ).
fof(f23679,plain,
( releasedAt(spilling,n3)
| spl11_163
| spl11_197
| ~ spl11_220
| ~ spl11_276 ),
inference(resolution,[],[f23676,f18330]) ).
fof(f23680,plain,
( spl11_277
| spl11_163
| spl11_197
| ~ spl11_220
| ~ spl11_276 ),
inference(avatar_split_clause,[],[f23679,f23282,f18329,f17539,f16124,f23286]) ).
fof(f23712,plain,
( releasedAt(spilling,n2)
| ~ spl11_218
| ~ spl11_277 ),
inference(resolution,[],[f23288,f18299]) ).
fof(f23714,plain,
( $false
| ~ spl11_218
| spl11_219
| ~ spl11_277 ),
inference(forward_subsumption_resolution,[],[f23712,f18318]) ).
fof(f23715,plain,
( ~ spl11_218
| spl11_219
| ~ spl11_277 ),
inference(avatar_contradiction_clause,[],[f23714]) ).
fof(f23722,plain,
( releasedAt(waterLevel(n3),n3)
| spl11_159
| spl11_191
| ~ spl11_192
| spl11_198 ),
inference(forward_subsumption_resolution,[],[f23278,f17544]) ).
fof(f23726,plain,
( releasedAt(waterLevel(n3),n2)
| spl11_159
| spl11_191
| ~ spl11_192
| spl11_198
| ~ spl11_218 ),
inference(resolution,[],[f23722,f18299]) ).
fof(f23734,plain,
( ~ holdsAt(waterLevel(n3),n1)
| spl11_159
| spl11_191
| ~ spl11_192
| spl11_198
| ~ spl11_218
| ~ spl11_261 ),
inference(resolution,[],[f23726,f22795]) ).
fof(f23738,plain,
( $false
| spl11_159
| ~ spl11_169
| spl11_191
| ~ spl11_192
| spl11_198
| ~ spl11_218
| ~ spl11_261 ),
inference(forward_subsumption_resolution,[],[f23734,f16392]) ).
fof(f23739,plain,
( spl11_159
| ~ spl11_169
| spl11_191
| ~ spl11_192
| spl11_198
| ~ spl11_218
| ~ spl11_261 ),
inference(avatar_contradiction_clause,[],[f23738]) ).
fof(f23740,plain,
( $false
| ~ spl11_160
| ~ spl11_169
| spl11_192 ),
inference(forward_subsumption_resolution,[],[f23566,f17385]) ).
fof(f23741,plain,
( ~ spl11_160
| ~ spl11_169
| spl11_192 ),
inference(avatar_contradiction_clause,[],[f23740]) ).
fof(f23889,plain,
! [X0] :
( ~ releasedAt(X0,n3)
| releasedAt(X0,n2)
| tapOn = sK7(X0,n2) ),
inference(superposition,[],[f17915,f190]) ).
fof(f28715,plain,
! [X0,X1] :
( ~ stoppedIn(X0,X1,n3)
| n2 = sK3(X0,X1,n3)
| less(sK3(X0,X1,n3),n2) ),
inference(resolution,[],[f8528,f196]) ).
fof(f32935,plain,
! [X2,X0,X1] :
( holdsAt(filling,sK3(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2)
| n0 = sK3(X0,X1,X2) ),
inference(resolution,[],[f127,f168]) ).
fof(f32936,plain,
! [X2,X0,X1] :
( holdsAt(waterLevel(n3),sK3(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2)
| n0 = sK3(X0,X1,X2) ),
inference(resolution,[],[f127,f169]) ).
fof(f33439,plain,
! [X0,X1] :
( ~ stoppedIn(X0,filling,X1)
| ~ happens(sK2(X0,filling,X1),sK3(X0,filling,X1))
| ~ happens(tapOn,sK3(X0,filling,X1)) ),
inference(resolution,[],[f124,f13870]) ).
fof(f33451,plain,
! [X0,X1] :
( ~ happens(tapOn,sK3(X0,filling,X1))
| ~ stoppedIn(X0,filling,X1) ),
inference(forward_subsumption_resolution,[],[f33439,f127]) ).
fof(f42361,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| ~ initiates(X0,filling,X1)
| ~ less(n0,n3)
| holdsAt(waterLevel(n3),plus(X1,n3))
| stoppedIn(X1,filling,plus(X1,n3))
| ~ holdsAt(waterLevel(n0),X1) ),
inference(resolution,[],[f128,f14009]) ).
fof(f42378,plain,
! [X0,X1] :
( ~ holdsAt(waterLevel(n0),X1)
| ~ initiates(X0,filling,X1)
| holdsAt(waterLevel(n3),plus(X1,n3))
| stoppedIn(X1,filling,plus(X1,n3))
| ~ happens(X0,X1) ),
inference(forward_subsumption_resolution,[],[f42361,f427]) ).
fof(f51723,definition,
( spl11_550
<=> ! [X0] :
( ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) ) ),
introduced(definition,[new_symbols(definition,[spl11_550])],[avatar_definition]) ).
fof(f51724,plain,
( ! [X0] :
( ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) )
| ~ spl11_550 ),
inference(avatar_component_clause,[],[f51723]) ).
fof(f51803,plain,
( ~ happens(tapOn,n0)
| ~ spl11_550 ),
inference(resolution,[],[f51724,f233]) ).
fof(f51806,plain,
( $false
| ~ spl11_550 ),
inference(forward_subsumption_resolution,[],[f51803,f243]) ).
fof(f51807,plain,
~ spl11_550,
inference(avatar_contradiction_clause,[],[f51806]) ).
fof(f62163,plain,
! [X0] :
( ~ initiates(X0,filling,n0)
| holdsAt(waterLevel(n3),plus(n0,n3))
| stoppedIn(n0,filling,plus(n0,n3))
| ~ happens(X0,n0) ),
inference(resolution,[],[f42378,f221]) ).
fof(f62188,plain,
! [X0] :
( holdsAt(waterLevel(n3),n3)
| ~ initiates(X0,filling,n0)
| stoppedIn(n0,filling,plus(n0,n3))
| ~ happens(X0,n0) ),
inference(forward_demodulation,[],[f62163,f188]) ).
fof(f62198,plain,
! [X0,X1] :
( less(sK3(X0,X1,n3),n2)
| n2 = sK3(X0,X1,n3)
| ~ stoppedIn(X0,X1,n3) ),
inference(global_subsumption,[],[f28715]) ).
fof(f62261,plain,
( ! [X0] :
( ~ initiates(X0,filling,n0)
| stoppedIn(n0,filling,plus(n0,n3))
| ~ happens(X0,n0) )
| spl11_198 ),
inference(forward_subsumption_resolution,[],[f62188,f17544]) ).
fof(f62264,plain,
( ! [X0] :
( stoppedIn(n0,filling,n3)
| ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) )
| spl11_198 ),
inference(forward_demodulation,[],[f62261,f188]) ).
fof(f62467,definition,
( spl11_606
<=> stoppedIn(n0,filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_606])],[avatar_definition]) ).
fof(f62469,plain,
( stoppedIn(n0,filling,n3)
| ~ spl11_606 ),
inference(avatar_component_clause,[],[f62467]) ).
fof(f62470,plain,
( spl11_550
| spl11_606
| spl11_198 ),
inference(avatar_split_clause,[],[f62264,f17543,f62467,f51723]) ).
fof(f62783,definition,
( spl11_607
<=> n0 = sK3(n0,filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_607])],[avatar_definition]) ).
fof(f62784,plain,
( n0 != sK3(n0,filling,n3)
| spl11_607 ),
inference(avatar_component_clause,[],[f62783]) ).
fof(f62785,plain,
( n0 = sK3(n0,filling,n3)
| ~ spl11_607 ),
inference(avatar_component_clause,[],[f62783]) ).
fof(f62791,plain,
( ~ happens(tapOn,n0)
| ~ stoppedIn(n0,filling,n3)
| ~ spl11_607 ),
inference(superposition,[],[f33451,f62785]) ).
fof(f62826,plain,
( ~ stoppedIn(n0,filling,n3)
| ~ spl11_607 ),
inference(forward_subsumption_resolution,[],[f62791,f243]) ).
fof(f62831,plain,
( $false
| ~ spl11_606
| ~ spl11_607 ),
inference(forward_subsumption_resolution,[],[f62826,f62469]) ).
fof(f62832,plain,
( ~ spl11_606
| ~ spl11_607 ),
inference(avatar_contradiction_clause,[],[f62831]) ).
fof(f70659,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| n0 = sK3(X0,X1,X2)
| happens(overflow,sK3(X0,X1,X2))
| ~ holdsAt(filling,sK3(X0,X1,X2)) ),
inference(resolution,[],[f32936,f244]) ).
fof(f70687,plain,
! [X2,X0,X1] :
( happens(overflow,sK3(X0,X1,X2))
| n0 = sK3(X0,X1,X2)
| ~ stoppedIn(X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f70659,f32935]) ).
fof(f77226,plain,
! [X0,X1] :
( n2 = sK3(X0,X1,n3)
| ~ stoppedIn(X0,X1,n3)
| n2 = sK3(X0,X1,n3)
| n0 = sK3(X0,X1,n3)
| n1 = sK3(X0,X1,n3) ),
inference(resolution,[],[f62198,f15691]) ).
fof(f77229,plain,
! [X0,X1] :
( ~ stoppedIn(X0,X1,n3)
| n2 = sK3(X0,X1,n3)
| n0 = sK3(X0,X1,n3)
| n1 = sK3(X0,X1,n3) ),
inference(duplicate_literal_removal,[],[f77226]) ).
fof(f77423,plain,
( n2 = sK3(n0,filling,n3)
| n0 = sK3(n0,filling,n3)
| n1 = sK3(n0,filling,n3)
| ~ spl11_606 ),
inference(resolution,[],[f77229,f62469]) ).
fof(f77424,plain,
( n2 = sK3(n0,filling,n3)
| n1 = sK3(n0,filling,n3)
| ~ spl11_606
| spl11_607 ),
inference(forward_subsumption_resolution,[],[f77423,f62784]) ).
fof(f77426,definition,
( spl11_687
<=> n1 = sK3(n0,filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_687])],[avatar_definition]) ).
fof(f77428,plain,
( n1 = sK3(n0,filling,n3)
| ~ spl11_687 ),
inference(avatar_component_clause,[],[f77426]) ).
fof(f77430,definition,
( spl11_688
<=> n2 = sK3(n0,filling,n3) ),
introduced(definition,[new_symbols(definition,[spl11_688])],[avatar_definition]) ).
fof(f77432,plain,
( n2 = sK3(n0,filling,n3)
| ~ spl11_688 ),
inference(avatar_component_clause,[],[f77430]) ).
fof(f77433,plain,
( spl11_687
| spl11_688
| ~ spl11_606
| spl11_607 ),
inference(avatar_split_clause,[],[f77424,f62783,f62467,f77430,f77426]) ).
fof(f78389,plain,
( holdsAt(waterLevel(n3),n2)
| ~ stoppedIn(n0,filling,n3)
| n0 = n2
| ~ spl11_688 ),
inference(superposition,[],[f32936,f77432]) ).
fof(f78409,plain,
( ~ stoppedIn(n0,filling,n3)
| n0 = n2
| spl11_192
| ~ spl11_688 ),
inference(forward_subsumption_resolution,[],[f78389,f17385]) ).
fof(f78426,plain,
( n0 = n2
| spl11_192
| ~ spl11_606
| ~ spl11_688 ),
inference(forward_subsumption_resolution,[],[f78409,f62469]) ).
fof(f78441,plain,
( $false
| spl11_191
| spl11_192
| ~ spl11_606
| ~ spl11_688 ),
inference(forward_subsumption_resolution,[],[f78426,f17381]) ).
fof(f78442,plain,
( spl11_191
| spl11_192
| ~ spl11_606
| ~ spl11_688 ),
inference(avatar_contradiction_clause,[],[f78441]) ).
fof(f78597,plain,
( happens(overflow,n1)
| n0 = n1
| ~ stoppedIn(n0,filling,n3)
| ~ spl11_687 ),
inference(superposition,[],[f70687,f77428]) ).
fof(f78605,plain,
( n0 = n1
| ~ stoppedIn(n0,filling,n3)
| spl11_160
| ~ spl11_687 ),
inference(forward_subsumption_resolution,[],[f78597,f16110]) ).
fof(f78622,plain,
( ~ stoppedIn(n0,filling,n3)
| spl11_160
| spl11_168
| ~ spl11_687 ),
inference(forward_subsumption_resolution,[],[f78605,f16387]) ).
fof(f78634,plain,
( $false
| spl11_160
| spl11_168
| ~ spl11_606
| ~ spl11_687 ),
inference(forward_subsumption_resolution,[],[f78622,f62469]) ).
fof(f78635,plain,
( spl11_160
| spl11_168
| ~ spl11_606
| ~ spl11_687 ),
inference(avatar_contradiction_clause,[],[f78634]) ).
fof(f78672,plain,
( ~ happens(overflow,n2)
| spl11_276 ),
inference(forward_subsumption_resolution,[],[f16886,f23283]) ).
fof(f78740,plain,
( ~ spl11_164
| spl11_276 ),
inference(avatar_split_clause,[],[f78672,f23282,f16128]) ).
fof(f78769,plain,
( ~ spl11_277
| ~ spl11_164 ),
inference(avatar_split_clause,[],[f16077,f16128,f23286]) ).
fof(f80026,plain,
( ~ happens(tapOn,n2)
| spl11_163 ),
inference(forward_subsumption_resolution,[],[f16864,f16126]) ).
fof(f80035,plain,
( ~ spl11_194
| spl11_163 ),
inference(avatar_split_clause,[],[f80026,f16124,f17513]) ).
fof(f81398,plain,
( ! [X0] :
( ~ holdsAt(X0,n2)
| releasedAt(X0,n3)
| holdsAt(X0,n3) )
| spl11_191
| spl11_192 ),
inference(forward_subsumption_resolution,[],[f22734,f17385]) ).
fof(f81399,plain,
( releasedAt(filling,n3)
| holdsAt(filling,n3)
| ~ spl11_159
| spl11_191
| spl11_192 ),
inference(resolution,[],[f81398,f16105]) ).
fof(f81404,plain,
( holdsAt(filling,n3)
| ~ spl11_159
| spl11_191
| spl11_192
| spl11_193 ),
inference(forward_subsumption_resolution,[],[f81399,f17511]) ).
fof(f81405,plain,
( $false
| ~ spl11_159
| spl11_163
| spl11_191
| spl11_192
| spl11_193 ),
inference(forward_subsumption_resolution,[],[f81404,f16126]) ).
fof(f81406,plain,
( ~ spl11_159
| spl11_163
| spl11_191
| spl11_192
| spl11_193 ),
inference(avatar_contradiction_clause,[],[f81405]) ).
fof(f81423,plain,
! [X0] :
( ~ releasedAt(X0,n3)
| releasedAt(X0,n2)
| tapOn = sK7(X0,n2) ),
inference(global_subsumption,[],[f23889]) ).
fof(f81474,plain,
( releasedAt(filling,n2)
| tapOn = sK7(filling,n2)
| ~ spl11_193 ),
inference(resolution,[],[f81423,f17510]) ).
fof(f81475,plain,
( tapOn = sK7(filling,n2)
| spl11_178
| ~ spl11_193 ),
inference(forward_subsumption_resolution,[],[f81474,f16940]) ).
fof(f81494,plain,
( happens(tapOn,n2)
| releasedAt(filling,n2)
| ~ releasedAt(filling,n3)
| spl11_178
| ~ spl11_193 ),
inference(superposition,[],[f17749,f81475]) ).
fof(f81497,plain,
( releasedAt(filling,n2)
| ~ releasedAt(filling,n3)
| spl11_178
| ~ spl11_193
| spl11_194 ),
inference(forward_subsumption_resolution,[],[f81494,f17515]) ).
fof(f81499,plain,
( ~ releasedAt(filling,n3)
| spl11_178
| ~ spl11_193
| spl11_194 ),
inference(forward_subsumption_resolution,[],[f81497,f16940]) ).
fof(f81501,plain,
( $false
| spl11_178
| ~ spl11_193
| spl11_194 ),
inference(forward_subsumption_resolution,[],[f81499,f17510]) ).
fof(f81502,plain,
( spl11_178
| ~ spl11_193
| spl11_194 ),
inference(avatar_contradiction_clause,[],[f81501]) ).
cnf(s5189,plain,
spl11_133,
inference(sat_conversion,[],[f13878]) ).
cnf(s5563,plain,
( ~ spl11_159
| ~ spl11_160 ),
inference(sat_conversion,[],[f16111]) ).
cnf(s5573,plain,
( ~ spl11_163
| ~ spl11_164 ),
inference(sat_conversion,[],[f16131]) ).
cnf(s5692,plain,
~ spl11_168,
inference(sat_conversion,[],[f16454]) ).
cnf(s5713,plain,
( ~ spl11_133
| spl11_160
| ~ spl11_169 ),
inference(sat_conversion,[],[f16465]) ).
cnf(s6146,plain,
~ spl11_191,
inference(sat_conversion,[],[f17492]) ).
cnf(s6162,plain,
( ~ spl11_159
| spl11_164
| ~ spl11_192 ),
inference(sat_conversion,[],[f17503]) ).
cnf(s6219,plain,
~ spl11_197,
inference(sat_conversion,[],[f17652]) ).
cnf(s6237,plain,
( spl11_162
| ~ spl11_163
| ~ spl11_198 ),
inference(sat_conversion,[],[f17663]) ).
cnf(s6284,plain,
( spl11_168
| spl11_169
| ~ spl11_178 ),
inference(sat_conversion,[],[f17722]) ).
cnf(s6694,plain,
( ~ spl11_160
| ~ spl11_219 ),
inference(sat_conversion,[],[f18319]) ).
cnf(s7241,plain,
( ~ spl11_133
| spl11_159
| spl11_168
| spl11_169
| spl11_178 ),
inference(sat_conversion,[],[f21095]) ).
cnf(s8031,plain,
( ~ spl11_160
| spl11_261 ),
inference(sat_conversion,[],[f22796]) ).
cnf(s8261,plain,
~ spl11_162,
inference(sat_conversion,[],[f23235]) ).
cnf(s8299,plain,
( spl11_159
| ~ spl11_160
| spl11_191
| spl11_276
| spl11_277 ),
inference(sat_conversion,[],[f23289]) ).
cnf(s8365,plain,
( spl11_163
| spl11_197
| spl11_220 ),
inference(sat_conversion,[],[f23433]) ).
cnf(s8401,plain,
( spl11_159
| spl11_191
| spl11_218 ),
inference(sat_conversion,[],[f23504]) ).
cnf(s8482,plain,
( spl11_163
| spl11_197
| ~ spl11_220
| ~ spl11_276
| spl11_277 ),
inference(sat_conversion,[],[f23680]) ).
cnf(s8501,plain,
( ~ spl11_218
| spl11_219
| ~ spl11_277 ),
inference(sat_conversion,[],[f23715]) ).
cnf(s8527,plain,
( spl11_159
| ~ spl11_169
| spl11_191
| ~ spl11_192
| spl11_198
| ~ spl11_218
| ~ spl11_261 ),
inference(sat_conversion,[],[f23739]) ).
cnf(s8535,plain,
( ~ spl11_160
| ~ spl11_169
| spl11_192 ),
inference(sat_conversion,[],[f23741]) ).
cnf(s16424,plain,
~ spl11_550,
inference(sat_conversion,[],[f51807]) ).
cnf(s20491,plain,
( spl11_198
| spl11_550
| spl11_606 ),
inference(sat_conversion,[],[f62470]) ).
cnf(s20684,plain,
( ~ spl11_606
| ~ spl11_607 ),
inference(sat_conversion,[],[f62832]) ).
cnf(s24094,plain,
( ~ spl11_606
| spl11_607
| spl11_687
| spl11_688 ),
inference(sat_conversion,[],[f77433]) ).
cnf(s24548,plain,
( spl11_191
| spl11_192
| ~ spl11_606
| ~ spl11_688 ),
inference(sat_conversion,[],[f78442]) ).
cnf(s24625,plain,
( spl11_160
| spl11_168
| ~ spl11_606
| ~ spl11_687 ),
inference(sat_conversion,[],[f78635]) ).
cnf(s24808,plain,
( ~ spl11_164
| spl11_276 ),
inference(sat_conversion,[],[f78740]) ).
cnf(s24879,plain,
( ~ spl11_164
| ~ spl11_277 ),
inference(sat_conversion,[],[f78769]) ).
cnf(s25393,plain,
( spl11_163
| ~ spl11_194 ),
inference(sat_conversion,[],[f80035]) ).
cnf(s25702,plain,
( ~ spl11_159
| spl11_163
| spl11_191
| spl11_192
| spl11_193 ),
inference(sat_conversion,[],[f81406]) ).
cnf(s25786,plain,
( spl11_178
| ~ spl11_193
| spl11_194 ),
inference(sat_conversion,[],[f81502]) ).
cnf(s25799,plain,
( ~ spl11_163
| ~ spl11_198 ),
inference(rat,[],[s6237,s8261]) ).
cnf(s25844,plain,
( spl11_169
| spl11_159 ),
inference(rat,[],[s7241,s6284,s5692,s5189]) ).
cnf(s25845,plain,
spl11_159,
inference(rat,[],[s8482,s8365,s8299,s25799,s8501,s8527,s6694,s8031,s8535,s5713,s25844,s8401,s6219,s6146,s5189]) ).
cnf(s25846,plain,
~ spl11_160,
inference(rat,[],[s5563,s25845]) ).
cnf(s25847,plain,
~ spl11_169,
inference(rat,[],[s5713,s5189,s25846]) ).
cnf(s25860,plain,
~ spl11_178,
inference(rat,[],[s6284,s5692,s25847]) ).
cnf(s25866,plain,
spl11_163,
inference(rat,[],[s8482,s24808,s24879,s6162,s25702,s25786,s8365,s25393,s6219,s25845,s6146,s25860]) ).
cnf(s25868,plain,
~ spl11_198,
inference(rat,[],[s25799,s25866]) ).
cnf(s25869,plain,
~ spl11_164,
inference(rat,[],[s5573,s25866]) ).
cnf(s25870,plain,
spl11_606,
inference(rat,[],[s20491,s16424,s25868]) ).
cnf(s25877,plain,
~ spl11_192,
inference(rat,[],[s6162,s25845,s25869]) ).
cnf(s25878,plain,
~ spl11_607,
inference(rat,[],[s20684,s25870]) ).
cnf(s25879,plain,
~ spl11_687,
inference(rat,[],[s24625,s25846,s5692,s25870]) ).
cnf(s25880,plain,
~ spl11_688,
inference(rat,[],[s24548,s25870,s6146,s25877]) ).
cnf(s25892,plain,
$false,
inference(rat,[],[s24094,s25878,s25870,s25880,s25879]) ).
fof(f81504,plain,
$false,
inference(avatar_sat_refutation,[],[s25892]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR003+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.24 % Computer : n006.cluster.edu
% 0.09/0.24 % Model : x86_64 x86_64
% 0.09/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.24 % Memory : 8046.5625MB
% 0.09/0.24 % OS : Linux 6.8.0-71-generic
% 0.09/0.24 % CPULimit : 300
% 0.09/0.24 % WCLimit : 300
% 0.09/0.24 % DateTime : Mon Sep 28 22:04:55 UTC 2026
% 0.09/0.25 % CPUTime :
% 0.09/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.22/0.29 Running first-order model finding
% 0.22/0.29 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.84/2.97 % (264012)Will run a generic schedule for satisfiability detection.
% 16.84/2.97 % (264023)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2162844014:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.84/2.97 % (264018)% WARNING: option uhcvi not known.
% 16.84/2.97 % (264017)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3581392206_2999 on theBenchmark for (2999ds/0Mi)
% 16.84/2.97 % (264020)dis+10_1_sil=32000:sp=arity:random_seed=2690630261:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.84/2.97 % (264018)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3200697258:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.84/2.97 % (264019)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=210992155:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.84/2.97 % (264022)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3211578244:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.84/2.97 % (264021)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1944756843:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.84/2.97 % Detected minimum model sizes of [3]
% 16.84/2.97 % Detected maximum model sizes of [max]
% 16.84/2.97 % TRYING [3]
% 16.84/2.97 % TRYING [4]
% 16.84/2.97 % TRYING [5]
% 16.84/2.97 % (264023)Instruction limit reached!
% 16.84/2.97 % (264023)------------------------------
% 16.84/2.97 % (264023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.84/2.97 % (264023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.84/2.97 % (264023)CaDiCaL version: 2.1.3
% 16.84/2.97 % (264023)Termination reason: Instruction limit
% 16.84/2.97 % (264023)Termination phase: Saturation
% 16.84/2.97 % (264023)Time elapsed: 0.088 s
% 16.84/2.97 % (264023)Peak memory usage: 12 MB
% 16.84/2.97 % (264023)Instructions burned: 159 (million)
% 16.84/2.97 % (264020)Instruction limit reached!
% 16.84/2.97 % (264020)------------------------------
% 16.84/2.97 % (264020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.84/2.97 % (264020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.84/2.97 % (264020)CaDiCaL version: 2.1.3
% 16.84/2.97 % (264020)Termination reason: Instruction limit
% 16.84/2.97 % (264020)Termination phase: Saturation
% 16.84/2.97 % (264020)Time elapsed: 0.099 s
% 16.84/2.97 % (264020)Peak memory usage: 12 MB
% 16.84/2.97 % (264020)Instructions burned: 103 (million)
% 16.84/2.97 % (264031)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2835469417:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 16.84/2.97 % Detected minimum model sizes of [3]
% 16.84/2.97 % Detected maximum model sizes of [max]
% 16.84/2.97 % TRYING [3]
% 16.84/2.97 % TRYING [4]
% 16.84/2.97 % (264021)Instruction limit reached!
% 16.84/2.97 % (264021)------------------------------
% 16.84/2.97 % (264021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.84/2.97 % (264021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.84/2.97 % (264021)CaDiCaL version: 2.1.3
% 16.84/2.97 % (264021)Termination reason: Instruction limit
% 16.84/2.97 % (264021)Termination phase: Saturation
% 16.84/2.97 % (264021)Time elapsed: 0.120 s
% 16.84/2.97 % (264021)Peak memory usage: 13 MB
% 16.84/2.97 % (264021)Instructions burned: 116 (million)
% 16.84/2.97 % (264032)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=665580534:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.84/2.97 % (264022)Instruction limit reached!
% 16.84/2.97 % (264022)------------------------------
% 16.84/2.97 % (264022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.84/2.97 % (264022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.84/2.97 % (264022)CaDiCaL version: 2.1.3
% 16.84/2.97 % (264022)Termination reason: Instruction limit
% 16.84/2.97 % (264022)Termination phase: Saturation
% 16.84/2.97 % (264022)Time elapsed: 0.132 s
% 16.84/2.97 % (264022)Peak memory usage: 12 MB
% 16.84/2.97 % (264022)Instructions burned: 133 (million)
% 16.84/2.97 % TRYING [6]
% 16.84/2.97 % TRYING [5]
% 16.84/2.97 % (264034)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=714513902:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.84/2.97 % (264036)ott-21_1_sil=16000:fs=off:random_seed=332657454:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.84/2.97 % TRYING [6]
% 16.84/2.97 % (264032)Instruction limit reached!
% 16.84/2.97 % (264032)------------------------------
% 16.84/2.97 % (264032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.64/6.13 % (264032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.64/6.13 % (264032)CaDiCaL version: 2.1.3
% 40.64/6.13 % (264032)Termination reason: Instruction limit
% 40.64/6.13 % (264032)Termination phase: Saturation
% 40.64/6.13 % (264032)Time elapsed: 0.132 s
% 40.64/6.13 % (264032)Peak memory usage: 13 MB
% 40.64/6.13 % (264032)Instructions burned: 131 (million)
% 40.64/6.13 % TRYING [7]
% 40.64/6.13 % (264039)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2558876503:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 40.64/6.13 % (264036)Instruction limit reached!
% 40.64/6.13 % (264036)------------------------------
% 40.64/6.13 % (264036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.64/6.13 % (264036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.64/6.13 % (264036)CaDiCaL version: 2.1.3
% 40.64/6.13 % (264036)Termination reason: Instruction limit
% 40.64/6.13 % (264036)Termination phase: Saturation
% 40.64/6.13 % (264036)Time elapsed: 0.164 s
% 40.64/6.13 % (264036)Peak memory usage: 12 MB
% 40.64/6.13 % (264036)Instructions burned: 181 (million)
% 40.64/6.13 % TRYING [7]
% 40.64/6.13 % (264041)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=5195360:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 40.64/6.13 % (264031)Instruction limit reached!
% 40.64/6.13 % (264031)------------------------------
% 40.64/6.13 % (264031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.64/6.13 % (264031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.64/6.13 % (264031)CaDiCaL version: 2.1.3
% 40.64/6.13 % (264031)Termination reason: Instruction limit
% 40.64/6.13 % (264031)Termination phase: Finite model building constraint generation
% 40.64/6.13 % (264031)Time elapsed: 0.283 s
% 40.64/6.13 % (264031)Peak memory usage: 28 MB
% 40.64/6.13 % (264031)Instructions burned: 715 (million)
% 40.64/6.13 % Detected minimum model sizes of [3]
% 40.64/6.13 % Detected maximum model sizes of [max]
% 40.64/6.13 % TRYING [3]
% 40.64/6.13 % (264043)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1770694108:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 40.64/6.13 % TRYING [4]
% 40.64/6.13 % TRYING [5]
% 40.64/6.13 % TRYING [8]
% 40.64/6.13 % (264039)Instruction limit reached!
% 40.64/6.13 % (264039)------------------------------
% 40.64/6.13 % (264039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.64/6.13 % (264039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.64/6.13 % (264039)CaDiCaL version: 2.1.3
% 40.64/6.13 % (264039)Termination reason: Instruction limit
% 40.64/6.13 % (264039)Termination phase: Saturation
% 40.64/6.13 % (264039)Time elapsed: 0.315 s
% 40.64/6.13 % (264039)Peak memory usage: 13 MB
% 40.64/6.13 % (264039)Instructions burned: 477 (million)
% 40.64/6.13 % (264045)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1630139178:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 40.64/6.13 % TRYING [6]
% 40.64/6.13 % (264034)Instruction limit reached!
% 40.64/6.13 % (264034)------------------------------
% 40.64/6.13 % (264034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.64/6.13 % (264034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.64/6.13 % (264034)CaDiCaL version: 2.1.3
% 40.64/6.13 % (264034)Termination reason: Instruction limit
% 40.64/6.13 % (264034)Termination phase: Saturation
% 40.64/6.13 % (264034)Time elapsed: 0.575 s
% 40.64/6.13 % (264034)Peak memory usage: 14 MB
% 40.64/6.13 % (264034)Instructions burned: 684 (million)
% 40.64/6.13 % (264047)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=2768541741:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi)
% 40.64/6.13 % TRYING [14]
% 40.64/6.13 % (264041)Instruction limit reached!
% 40.64/6.13 % (264041)------------------------------
% 40.64/6.13 % (264041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.64/6.13 % (264041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.64/6.13 % (264041)CaDiCaL version: 2.1.3
% 40.64/6.13 % (264041)Termination reason: Instruction limit
% 40.64/6.13 % (264041)Termination phase: Finite model building SAT solving
% 40.64/6.13 % (264041)Time elapsed: 0.588 s
% 40.64/6.13 % (264041)Peak memory usage: 26 MB
% 40.64/6.13 % (264041)Instructions burned: 866 (million)
% 40.64/6.13 % (264049)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=210798302:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 40.64/6.13 % (264045)Instruction limit reached!
% 40.64/6.13 % (264045)------------------------------
% 40.64/6.13 % (264045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.64/6.13 % (264045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.64/6.13 % (264045)CaDiCaL version: 2.1.3
% 40.64/6.13 % (264045)Termination reason: Instruction limit
% 40.64/6.13 % (264045)Termination phase: Finite model building constraint generation
% 40.64/6.13 % (264045)Time elapsed: 0.397 s
% 40.64/6.13 % (264045)Peak memory usage: 79 MB
% 40.64/6.13 % (264045)Instructions burned: 891 (million)
% 40.64/6.13 % (264051)fmb+10_1_sil=64000:random_seed=432938008:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 40.64/6.13 % TRYING [9]
% 40.64/6.13 % Detected minimum model sizes of [3]
% 40.64/6.13 % Detected maximum model sizes of [max]
% 40.64/6.13 % TRYING [3]
% 40.64/6.13 % TRYING [4]
% 40.64/6.13 % TRYING [5]
% 40.64/6.13 % TRYING [6]
% 40.64/6.13 % (264047)Instruction limit reached!
% 40.64/6.13 % (264047)------------------------------
% 40.64/6.13 % (264047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.64/6.13 % (264047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.64/6.13 % (264047)CaDiCaL version: 2.1.3
% 40.64/6.13 % (264047)Termination reason: Instruction limit
% 40.64/6.13 % (264047)Termination phase: Saturation
% 40.64/6.13 % (264047)Time elapsed: 0.554 s
% 40.64/6.13 % (264047)Peak memory usage: 15 MB
% 40.64/6.13 % (264047)Instructions burned: 692 (million)
% 40.64/6.13 % (264053)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4212771984:i=9515:nm=5_2986 on theBenchmark for (2986ds/9515Mi)
% 40.64/6.13 % Detected minimum model sizes of [3]
% 40.64/6.13 % Detected maximum model sizes of [max]
% 40.64/6.13 % TRYING [20]
% 40.64/6.13 % (264043)Instruction limit reached!
% 40.64/6.13 % (264043)------------------------------
% 40.64/6.13 % (264043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.64/6.13 % (264043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.64/6.13 % (264043)CaDiCaL version: 2.1.3
% 40.64/6.13 % (264043)Termination reason: Instruction limit
% 40.64/6.13 % (264043)Termination phase: Saturation
% 40.64/6.13 % (264043)Time elapsed: 1.029 s
% 40.64/6.13 % (264043)Peak memory usage: 18 MB
% 40.64/6.13 % (264043)Instructions burned: 1180 (million)
% 40.64/6.13 % (264055)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=275622274:fmbsr=1.7:i=920_2985 on theBenchmark for (2985ds/920Mi)
% 40.64/6.13 % Detected minimum model sizes of [3]
% 40.64/6.13 % Detected maximum model sizes of [max]
% 40.64/6.13 % TRYING [8]
% 40.64/6.13 % TRYING [7]
% 40.64/6.13 % (264049)Instruction limit reached!
% 40.64/6.13 % (264049)------------------------------
% 40.64/6.13 % (264049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.64/6.13 % (264049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.64/6.13 % (264049)CaDiCaL version: 2.1.3
% 40.64/6.13 % (264049)Termination reason: Instruction limit
% 40.64/6.13 % (264049)Termination phase: Saturation
% 40.64/6.13 % (264049)Time elapsed: 0.734 s
% 40.64/6.13 % (264049)Peak memory usage: 19 MB
% 40.64/6.13 % (264049)Instructions burned: 879 (million)
% 40.64/6.13 % (264057)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=274266440:i=5131_2982 on theBenchmark for (2982ds/5131Mi)
% 40.64/6.13 % TRYING [9]
% 40.64/6.13 % (264055)Instruction limit reached!
% 40.64/6.13 % (264055)------------------------------
% 40.64/6.13 % (264055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.64/6.13 % (264055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.64/6.13 % (264055)CaDiCaL version: 2.1.3
% 40.64/6.13 % (264055)Termination reason: Instruction limit
% 40.64/6.13 % (264055)Termination phase: Finite model building constraint generation
% 40.64/6.13 % (264055)Time elapsed: 0.369 s
% 40.64/6.13 % (264055)Peak memory usage: 53 MB
% 40.64/6.13 % (264055)Instructions burned: 921 (million)
% 40.64/6.13 % (264059)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1541711131:i=1472:ins=7:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/1472Mi)
% 40.64/6.13 % TRYING [10]
% 40.64/6.13 % TRYING [8]
% 40.64/6.13 % (264059)Instruction limit reached!
% 40.64/6.13 % (264059)------------------------------
% 40.64/6.13 % (264059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.64/6.13 % (264059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.64/6.13 % (264059)CaDiCaL version: 2.1.3
% 40.64/6.13 % (264059)Termination reason: Instruction limit
% 40.64/6.13 % (264059)Termination phase: Saturation
% 40.64/6.13 % (264059)Time elapsed: 0.784 s
% 40.64/6.13 % (264059)Peak memory usage: 24 MB
% 40.64/6.13 % (264059)Instructions burned: 1474 (million)
% 40.64/6.13 % (264061)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2123714062:i=6324_2973 on theBenchmark for (2973ds/6324Mi)
% 40.64/6.13 % Detected minimum model sizes of [3]
% 40.64/6.13 % Detected maximum model sizes of [max]
% 40.64/6.13 % TRYING [77]
% 40.64/6.13 % TRYING [9]
% 40.64/6.13 % TRYING [11]
% 40.64/6.13 % TRYING [10]
% 40.64/6.13 % (264061)Instruction limit reached!
% 40.64/6.13 % (264061)------------------------------
% 40.64/6.13 % (264061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.64/6.13 % (264061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.64/6.13 % (264061)CaDiCaL version: 2.1.3
% 40.64/6.13 % (264061)Termination reason: Instruction limit
% 40.64/6.13 % (264061)Termination phase: Finite model building constraint generation
% 40.64/6.13 % (264061)Time elapsed: 2.514 s
% 40.64/6.13 % (264061)Peak memory usage: 516 MB
% 40.64/6.13 % (264061)Instructions burned: 6325 (million)
% 40.64/6.13 % (264065)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3732455764:fmbsr=2.30978:i=2174_2947 on theBenchmark for (2947ds/2174Mi)
% 40.64/6.13 % Detected minimum model sizes of [3]
% 40.64/6.13 % Detected maximum model sizes of [max]
% 40.64/6.13 % TRYING [16]
% 40.64/6.13 % (264019) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-264012-264019"...
% 40.64/6.13 % (264019)...printing done.
% 40.64/6.13 % (264019)Refutation found. Thanks to Tanya!
% 40.64/6.13 % SZS status Theorem for theBenchmark
% 40.64/6.13 % SZS output start Proof for theBenchmark
% See solution above
% 41.01/6.14 % (264019)------------------------------
% 41.01/6.14 % (264019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.01/6.14 % (264019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.01/6.14 % (264019)CaDiCaL version: 2.1.3
% 41.01/6.14 % (264019)Termination reason: Refutation
% 41.01/6.14 % (264019)Time elapsed: 5.707 s
% 41.01/6.14 % (264019)Peak memory usage: 60 MB
% 41.01/6.14 % (264019)Instructions burned: 5543 (million)
% 41.01/6.14 % (264012)Success in time 5.836 s
% 41.01/6.14 % Vampire exiting
%------------------------------------------------------------------------------