%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR001+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 : n017.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:17 AM UTC 2026
% Result : Theorem 54.42s 14.05s
% Output : Refutation 54.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 77
% Syntax : Number of formulae : 496 ( 78 unt; 48 def)
% Number of atoms : 1379 ( 221 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 1464 ( 581 ~; 676 |; 137 &)
% ( 61 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 60 ( 58 usr; 40 prp; 0-4 aty)
% Number of functors : 18 ( 18 usr; 10 con; 0-3 aty)
% Number of variables : 429 ( 0 sgn 399 !; 30 ?)
% 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(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(f18,axiom,
! [X0,X1,X2] :
( ( holdsAt(waterLevel(X1),X0)
& holdsAt(waterLevel(X2),X0) )
=> X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+1.ax',same_waterLevel) ).
fof(f20,axiom,
tapOff != overflow,
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+1.ax',tapOff_not_overflow) ).
fof(f21,axiom,
overflow != tapOn,
file('/export/starexec/sandbox2/benchmark/Axioms/CSR001+1.ax',overflow_not_tapOn) ).
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(f55,conjecture,
holdsAt(waterLevel(n3),n4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',waterLevel_4) ).
fof(f56,negated_conjecture,
~ holdsAt(waterLevel(n3),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(waterLevel(n3),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(f78,plain,
! [X0,X1,X2] :
( releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ releases(X0,X2,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f79,plain,
! [X0,X1,X2] :
( releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ releases(X0,X2,X1) ),
inference(flattening,[],[f78]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(flattening,[],[f80]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(ennf_transformation,[],[f17]) ).
fof(f83,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(flattening,[],[f82]) ).
fof(f84,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f85,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(flattening,[],[f84]) ).
fof(f86,plain,
! [X0] : ~ less(X0,n0),
inference(ennf_transformation,[],[f38]) ).
fof(f87,definition,
! [X0,X2,X1] :
( ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) )
| ~ sP0(X0,X2,X1) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f88,plain,
! [X0,X1,X2] :
( sP0(X0,X2,X1)
| ~ stoppedIn(X0,X1,X2) ),
inference(definition_folding,[],[f63,f87]) ).
fof(f89,definition,
! [X2,X0,X1] :
( sP1(X2,X0,X1)
<=> ? [X4] :
( holdsAt(waterLevel(X4),X2)
& X0 = overflow
& waterLevel(X4) = X1 ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f90,definition,
! [X2,X0,X1] :
( sP2(X2,X0,X1)
<=> ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f91,definition,
! [X0,X1] :
( sP3(X0,X1)
<=> ( X0 = overflow
& X1 = spilling ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f92,definition,
! [X0,X1,X2] :
( sP4(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| sP3(X0,X1)
| sP2(X2,X0,X1)
| sP1(X2,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f93,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> sP4(X0,X1,X2) ),
inference(definition_folding,[],[f57,f92,f91,f90,f89]) ).
fof(f94,definition,
! [X0,X1] :
( sP5(X0,X1)
<=> ( X0 = overflow
& X1 = filling ) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f95,definition,
! [X0,X1] :
( sP6(X0,X1)
<=> ( ( X0 = tapOff
& X1 = filling )
| sP5(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f96,plain,
! [X0,X1,X2] :
( terminates(X0,X1,X2)
<=> sP6(X0,X1) ),
inference(definition_folding,[],[f14,f95,f94]) ).
fof(f97,definition,
! [X1,X0] :
( sP7(X1,X0)
<=> ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow ) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f98,definition,
! [X0,X1] :
( sP8(X0,X1)
<=> ( ( X0 = tapOn
& X1 = n0 )
| sP7(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f99,plain,
! [X0,X1] :
( happens(X0,X1)
<=> sP8(X0,X1) ),
inference(definition_folding,[],[f16,f98,f97]) ).
fof(f100,plain,
! [X0,X2,X1] :
( ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) )
| ~ sP0(X0,X2,X1) ),
inference(nnf_transformation,[],[f87]) ).
fof(f101,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X1)
& terminates(X3,X2,X4) )
| ~ sP0(X0,X1,X2) ),
inference(rectify,[],[f100]) ).
fof(f102,plain,
! [X0,X1,X2] :
( ( happens(sK9(X0,X1,X2),sK10(X0,X1,X2))
& less(X0,sK10(X0,X1,X2))
& less(sK10(X0,X1,X2),X1)
& terminates(sK9(X0,X1,X2),X2,sK10(X0,X1,X2)) )
| ~ sP0(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10]),skolemize(X3,sK9(X0,X1,X2)),skolemize(X4,sK10(X0,X1,X2))],[f101]) ).
fof(f103,plain,
! [X0,X1] :
( holdsAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ( happens(sK11(X0,X1),X1)
& terminates(sK11(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X2,sK11(X0,X1))],[f67]) ).
fof(f106,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ( happens(sK14(X0,X1),X1)
& releases(sK14(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X2,sK14(X0,X1))],[f73]) ).
fof(f107,plain,
! [X0,X1,X2] :
( ( sP4(X0,X1,X2)
| ( ( tapOn != X0
| filling != X1 )
& ~ sP3(X0,X1)
& ~ sP2(X2,X0,X1)
& ~ sP1(X2,X0,X1) ) )
& ( ( X0 = tapOn
& X1 = filling )
| sP3(X0,X1)
| sP2(X2,X0,X1)
| sP1(X2,X0,X1)
| ~ sP4(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f92]) ).
fof(f108,plain,
! [X0,X1,X2] :
( ( sP4(X0,X1,X2)
| ( ( tapOn != X0
| filling != X1 )
& ~ sP3(X0,X1)
& ~ sP2(X2,X0,X1)
& ~ sP1(X2,X0,X1) ) )
& ( ( X0 = tapOn
& X1 = filling )
| sP3(X0,X1)
| sP2(X2,X0,X1)
| sP1(X2,X0,X1)
| ~ sP4(X0,X1,X2) ) ),
inference(flattening,[],[f107]) ).
fof(f114,plain,
! [X2,X0,X1] :
( ( sP1(X2,X0,X1)
| ! [X4] :
( ~ holdsAt(waterLevel(X4),X2)
| overflow != X0
| waterLevel(X4) != X1 ) )
& ( ? [X4] :
( holdsAt(waterLevel(X4),X2)
& X0 = overflow
& waterLevel(X4) = X1 )
| ~ sP1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f89]) ).
fof(f115,plain,
! [X0,X1,X2] :
( ( sP1(X0,X1,X2)
| ! [X3] :
( ~ holdsAt(waterLevel(X3),X0)
| overflow != X1
| waterLevel(X3) != X2 ) )
& ( ? [X4] :
( holdsAt(waterLevel(X4),X0)
& overflow = X1
& waterLevel(X4) = X2 )
| ~ sP1(X0,X1,X2) ) ),
inference(rectify,[],[f114]) ).
fof(f116,plain,
! [X0,X1,X2] :
( ( sP1(X0,X1,X2)
| ! [X3] :
( ~ holdsAt(waterLevel(X3),X0)
| overflow != X1
| waterLevel(X3) != X2 ) )
& ( ( holdsAt(waterLevel(sK16(X0,X1,X2)),X0)
& overflow = X1
& waterLevel(sK16(X0,X1,X2)) = X2 )
| ~ sP1(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X4,sK16(X0,X1,X2))],[f115]) ).
fof(f117,plain,
! [X0,X1,X2] :
( ( initiates(X0,X1,X2)
| ~ sP4(X0,X1,X2) )
& ( sP4(X0,X1,X2)
| ~ initiates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f93]) ).
fof(f118,plain,
! [X0,X1] :
( ( sP6(X0,X1)
| ( ( tapOff != X0
| filling != X1 )
& ~ sP5(X0,X1) ) )
& ( ( X0 = tapOff
& X1 = filling )
| sP5(X0,X1)
| ~ sP6(X0,X1) ) ),
inference(nnf_transformation,[],[f95]) ).
fof(f119,plain,
! [X0,X1] :
( ( sP6(X0,X1)
| ( ( tapOff != X0
| filling != X1 )
& ~ sP5(X0,X1) ) )
& ( ( X0 = tapOff
& X1 = filling )
| sP5(X0,X1)
| ~ sP6(X0,X1) ) ),
inference(flattening,[],[f118]) ).
fof(f120,plain,
! [X0,X1] :
( ( sP5(X0,X1)
| overflow != X0
| filling != X1 )
& ( ( X0 = overflow
& X1 = filling )
| ~ sP5(X0,X1) ) ),
inference(nnf_transformation,[],[f94]) ).
fof(f121,plain,
! [X0,X1] :
( ( sP5(X0,X1)
| overflow != X0
| filling != X1 )
& ( ( X0 = overflow
& X1 = filling )
| ~ sP5(X0,X1) ) ),
inference(flattening,[],[f120]) ).
fof(f122,plain,
! [X0,X1,X2] :
( ( terminates(X0,X1,X2)
| ~ sP6(X0,X1) )
& ( sP6(X0,X1)
| ~ terminates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f96]) ).
fof(f123,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(f124,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,[],[f123]) ).
fof(f125,plain,
! [X0,X1,X2] :
( ( releases(X0,X1,X2)
| ! [X3] :
( tapOn != X0
| waterLevel(X3) != X1 ) )
& ( ( X0 = tapOn
& waterLevel(sK17(X0,X1)) = X1 )
| ~ releases(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(X4,sK17(X0,X1))],[f124]) ).
fof(f126,plain,
! [X0,X1] :
( ( sP8(X0,X1)
| ( ( tapOn != X0
| n0 != X1 )
& ~ sP7(X1,X0) ) )
& ( ( X0 = tapOn
& X1 = n0 )
| sP7(X1,X0)
| ~ sP8(X0,X1) ) ),
inference(nnf_transformation,[],[f98]) ).
fof(f127,plain,
! [X0,X1] :
( ( sP8(X0,X1)
| ( ( tapOn != X0
| n0 != X1 )
& ~ sP7(X1,X0) ) )
& ( ( X0 = tapOn
& X1 = n0 )
| sP7(X1,X0)
| ~ sP8(X0,X1) ) ),
inference(flattening,[],[f126]) ).
fof(f128,plain,
! [X1,X0] :
( ( sP7(X1,X0)
| ~ holdsAt(waterLevel(n3),X1)
| ~ holdsAt(filling,X1)
| overflow != X0 )
& ( ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow )
| ~ sP7(X1,X0) ) ),
inference(nnf_transformation,[],[f97]) ).
fof(f129,plain,
! [X1,X0] :
( ( sP7(X1,X0)
| ~ holdsAt(waterLevel(n3),X1)
| ~ holdsAt(filling,X1)
| overflow != X0 )
& ( ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow )
| ~ sP7(X1,X0) ) ),
inference(flattening,[],[f128]) ).
fof(f130,plain,
! [X0,X1] :
( ( sP7(X0,X1)
| ~ holdsAt(waterLevel(n3),X0)
| ~ holdsAt(filling,X0)
| overflow != X1 )
& ( ( holdsAt(waterLevel(n3),X0)
& holdsAt(filling,X0)
& overflow = X1 )
| ~ sP7(X0,X1) ) ),
inference(rectify,[],[f129]) ).
fof(f131,plain,
! [X0,X1] :
( ( happens(X0,X1)
| ~ sP8(X0,X1) )
& ( sP8(X0,X1)
| ~ happens(X0,X1) ) ),
inference(nnf_transformation,[],[f99]) ).
fof(f133,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(f134,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,[],[f133]) ).
fof(f135,plain,
! [X0] :
( ( less(X0,n1)
| ~ less_or_equal(X0,n0) )
& ( less_or_equal(X0,n0)
| ~ less(X0,n1) ) ),
inference(nnf_transformation,[],[f39]) ).
fof(f136,plain,
! [X0] :
( ( less(X0,n2)
| ~ less_or_equal(X0,n1) )
& ( less_or_equal(X0,n1)
| ~ less(X0,n2) ) ),
inference(nnf_transformation,[],[f40]) ).
fof(f137,plain,
! [X0] :
( ( less(X0,n3)
| ~ less_or_equal(X0,n2) )
& ( less_or_equal(X0,n2)
| ~ less(X0,n3) ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f144,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(nnf_transformation,[],[f48]) ).
fof(f145,plain,
! [X0,X1] :
( ( less(X0,X1)
| less(X1,X0)
| X0 = X1 )
& ( ( ~ less(X1,X0)
& X1 != X0 )
| ~ less(X0,X1) ) ),
inference(flattening,[],[f144]) ).
fof(f147,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| less(sK10(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f102]) ).
fof(f148,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| less(X0,sK10(X0,X1,X2)) ),
inference(cnf_transformation,[],[f102]) ).
fof(f149,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| happens(sK9(X0,X1,X2),sK10(X0,X1,X2)) ),
inference(cnf_transformation,[],[f102]) ).
fof(f150,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| sP0(X0,X2,X1) ),
inference(cnf_transformation,[],[f88]) ).
fof(f151,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(f152,plain,
! [X0,X1] :
( ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1))
| releasedAt(X0,plus(X1,n1))
| terminates(sK11(X0,X1),X0,X1) ),
inference(cnf_transformation,[],[f103]) ).
fof(f153,plain,
! [X0,X1] :
( ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1))
| releasedAt(X0,plus(X1,n1))
| happens(sK11(X0,X1),X1) ),
inference(cnf_transformation,[],[f103]) ).
fof(f158,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| releases(sK14(X0,X1),X0,X1) ),
inference(cnf_transformation,[],[f106]) ).
fof(f159,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| happens(sK14(X0,X1),X1) ),
inference(cnf_transformation,[],[f106]) ).
fof(f160,plain,
! [X2,X0,X1] :
( ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1))
| ~ initiates(X0,X2,X1) ),
inference(cnf_transformation,[],[f75]) ).
fof(f162,plain,
! [X2,X0,X1] :
( ~ happens(X0,X1)
| releasedAt(X2,plus(X1,n1))
| ~ releases(X0,X2,X1) ),
inference(cnf_transformation,[],[f79]) ).
fof(f164,plain,
! [X2,X0,X1] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(cnf_transformation,[],[f81]) ).
fof(f167,plain,
! [X2,X0,X1] :
( ~ sP1(X2,X0,X1)
| sP4(X0,X1,X2) ),
inference(cnf_transformation,[],[f108]) ).
fof(f170,plain,
! [X2,X0,X1] :
( sP4(X0,X1,X2)
| tapOn != X0
| filling != X1 ),
inference(cnf_transformation,[],[f108]) ).
fof(f181,plain,
! [X2,X3,X0,X1] :
( sP1(X0,X1,X2)
| ~ holdsAt(waterLevel(X3),X0)
| overflow != X1
| waterLevel(X3) != X2 ),
inference(cnf_transformation,[],[f116]) ).
fof(f183,plain,
! [X2,X0,X1] :
( ~ sP4(X0,X1,X2)
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f117]) ).
fof(f185,plain,
! [X0,X1] :
( ~ sP6(X0,X1)
| sP5(X0,X1)
| tapOff = X0 ),
inference(cnf_transformation,[],[f119]) ).
fof(f188,plain,
! [X0,X1] :
( ~ sP5(X0,X1)
| filling = X1 ),
inference(cnf_transformation,[],[f121]) ).
fof(f191,plain,
! [X2,X0,X1] :
( ~ terminates(X0,X1,X2)
| sP6(X0,X1) ),
inference(cnf_transformation,[],[f122]) ).
fof(f194,plain,
! [X2,X0,X1] :
( ~ releases(X0,X1,X2)
| tapOn = X0 ),
inference(cnf_transformation,[],[f125]) ).
fof(f195,plain,
! [X2,X3,X0,X1] :
( releases(X0,X1,X2)
| tapOn != X0
| waterLevel(X3) != X1 ),
inference(cnf_transformation,[],[f125]) ).
fof(f196,plain,
! [X0,X1] :
( ~ sP8(X0,X1)
| sP7(X1,X0)
| n0 = X1 ),
inference(cnf_transformation,[],[f127]) ).
fof(f198,plain,
! [X0,X1] :
( ~ sP7(X1,X0)
| sP8(X0,X1) ),
inference(cnf_transformation,[],[f127]) ).
fof(f199,plain,
! [X0,X1] :
( sP8(X0,X1)
| tapOn != X0
| n0 != X1 ),
inference(cnf_transformation,[],[f127]) ).
fof(f200,plain,
! [X0,X1] :
( ~ sP7(X0,X1)
| overflow = X1 ),
inference(cnf_transformation,[],[f130]) ).
fof(f201,plain,
! [X0,X1] :
( ~ sP7(X0,X1)
| holdsAt(filling,X0) ),
inference(cnf_transformation,[],[f130]) ).
fof(f202,plain,
! [X0,X1] :
( ~ sP7(X0,X1)
| holdsAt(waterLevel(n3),X0) ),
inference(cnf_transformation,[],[f130]) ).
fof(f203,plain,
! [X0,X1] :
( sP7(X0,X1)
| ~ holdsAt(waterLevel(n3),X0)
| ~ holdsAt(filling,X0)
| overflow != X1 ),
inference(cnf_transformation,[],[f130]) ).
fof(f204,plain,
! [X0,X1] :
( sP8(X0,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[],[f131]) ).
fof(f205,plain,
! [X0,X1] :
( ~ sP8(X0,X1)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f131]) ).
fof(f206,plain,
! [X2,X3,X0,X1] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(cnf_transformation,[],[f83]) ).
fof(f207,plain,
! [X2,X0,X1] :
( ~ holdsAt(waterLevel(X2),X0)
| ~ holdsAt(waterLevel(X1),X0)
| X1 = X2 ),
inference(cnf_transformation,[],[f85]) ).
fof(f209,plain,
overflow != tapOff,
inference(cnf_transformation,[],[f20]) ).
fof(f210,plain,
tapOn != overflow,
inference(cnf_transformation,[],[f21]) ).
fof(f217,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f27]) ).
fof(f219,plain,
n3 = plus(n0,n3),
inference(cnf_transformation,[],[f29]) ).
fof(f220,plain,
n2 = plus(n1,n1),
inference(cnf_transformation,[],[f30]) ).
fof(f221,plain,
n3 = plus(n1,n2),
inference(cnf_transformation,[],[f31]) ).
fof(f222,plain,
plus(n1,n3) = n4,
inference(cnf_transformation,[],[f32]) ).
fof(f226,plain,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[],[f36]) ).
fof(f227,plain,
! [X0,X1] :
( ~ less_or_equal(X0,X1)
| X0 = X1
| less(X0,X1) ),
inference(cnf_transformation,[],[f134]) ).
fof(f228,plain,
! [X0,X1] :
( less_or_equal(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f134]) ).
fof(f229,plain,
! [X0,X1] :
( less_or_equal(X0,X1)
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f134]) ).
fof(f230,plain,
! [X0] : ~ less(X0,n0),
inference(cnf_transformation,[],[f86]) ).
fof(f231,plain,
! [X0] :
( less_or_equal(X0,n0)
| ~ less(X0,n1) ),
inference(cnf_transformation,[],[f135]) ).
fof(f232,plain,
! [X0] :
( ~ less_or_equal(X0,n0)
| less(X0,n1) ),
inference(cnf_transformation,[],[f135]) ).
fof(f233,plain,
! [X0] :
( less_or_equal(X0,n1)
| ~ less(X0,n2) ),
inference(cnf_transformation,[],[f136]) ).
fof(f234,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| less(X0,n2) ),
inference(cnf_transformation,[],[f136]) ).
fof(f235,plain,
! [X0] :
( less_or_equal(X0,n2)
| ~ less(X0,n3) ),
inference(cnf_transformation,[],[f137]) ).
fof(f236,plain,
! [X0] :
( ~ less_or_equal(X0,n2)
| less(X0,n3) ),
inference(cnf_transformation,[],[f137]) ).
fof(f250,plain,
! [X0,X1] :
( ~ less(X0,X1)
| ~ less(X1,X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f252,plain,
holdsAt(waterLevel(n0),n0),
inference(cnf_transformation,[],[f49]) ).
fof(f258,plain,
~ holdsAt(waterLevel(n3),n4),
inference(cnf_transformation,[],[f58]) ).
fof(f259,plain,
! [X2,X1] :
( sP4(tapOn,X1,X2)
| filling != X1 ),
inference(equality_resolution,[],[f170]) ).
fof(f260,plain,
! [X2] : sP4(tapOn,filling,X2),
inference(equality_resolution,[],[f259]) ).
fof(f265,plain,
! [X2,X3,X0] :
( sP1(X0,overflow,X2)
| ~ holdsAt(waterLevel(X3),X0)
| waterLevel(X3) != X2 ),
inference(equality_resolution,[],[f181]) ).
fof(f266,plain,
! [X3,X0] :
( ~ holdsAt(waterLevel(X3),X0)
| sP1(X0,overflow,waterLevel(X3)) ),
inference(equality_resolution,[],[f265]) ).
fof(f271,plain,
! [X2,X3,X1] :
( releases(tapOn,X1,X2)
| waterLevel(X3) != X1 ),
inference(equality_resolution,[],[f195]) ).
fof(f272,plain,
! [X2,X3] : releases(tapOn,waterLevel(X3),X2),
inference(equality_resolution,[],[f271]) ).
fof(f273,plain,
! [X1] :
( sP8(tapOn,X1)
| n0 != X1 ),
inference(equality_resolution,[],[f199]) ).
fof(f274,plain,
sP8(tapOn,n0),
inference(equality_resolution,[],[f273]) ).
fof(f275,plain,
! [X0] :
( ~ holdsAt(waterLevel(n3),X0)
| sP7(X0,overflow)
| ~ holdsAt(filling,X0) ),
inference(equality_resolution,[],[f203]) ).
fof(f276,plain,
! [X3,X0,X1] :
( ~ holdsAt(waterLevel(X0),X1)
| trajectory(filling,X1,waterLevel(plus(X0,X3)),X3) ),
inference(equality_resolution,[],[f206]) ).
fof(f278,plain,
! [X1] : less_or_equal(X1,X1),
inference(equality_resolution,[],[f228]) ).
fof(f281,plain,
n1 = plus(n1,n0),
inference(forward_demodulation,[],[f217,f226]) ).
fof(f284,plain,
happens(tapOn,n0),
inference(resolution,[],[f205,f274]) ).
fof(f287,plain,
less(n0,n1),
inference(resolution,[],[f232,f278]) ).
fof(f289,plain,
less(n2,n3),
inference(resolution,[],[f236,f278]) ).
fof(f296,plain,
! [X0] :
( ~ less(X0,n2)
| less(X0,n3) ),
inference(resolution,[],[f229,f236]) ).
fof(f300,plain,
! [X0] : initiates(tapOn,filling,X0),
inference(resolution,[],[f183,f260]) ).
fof(f304,plain,
less(n1,n2),
inference(resolution,[],[f234,f278]) ).
fof(f305,plain,
! [X0] :
( ~ less(X0,n1)
| less(X0,n2) ),
inference(resolution,[],[f234,f229]) ).
fof(f307,plain,
! [X0] :
( holdsAt(X0,plus(n0,n1))
| ~ initiates(tapOn,X0,n0) ),
inference(resolution,[],[f160,f284]) ).
fof(f308,plain,
! [X0] :
( holdsAt(X0,plus(n1,n0))
| ~ initiates(tapOn,X0,n0) ),
inference(forward_demodulation,[],[f307,f226]) ).
fof(f309,plain,
! [X0] :
( ~ initiates(tapOn,X0,n0)
| holdsAt(X0,n1) ),
inference(forward_demodulation,[],[f308,f281]) ).
fof(f314,plain,
! [X0] :
( releasedAt(X0,plus(n0,n1))
| ~ releases(tapOn,X0,n0) ),
inference(resolution,[],[f162,f284]) ).
fof(f315,plain,
! [X0] :
( releasedAt(X0,plus(n1,n0))
| ~ releases(tapOn,X0,n0) ),
inference(forward_demodulation,[],[f314,f226]) ).
fof(f316,plain,
! [X0] :
( ~ releases(tapOn,X0,n0)
| releasedAt(X0,n1) ),
inference(forward_demodulation,[],[f315,f281]) ).
fof(f322,plain,
! [X0] :
( ~ releasedAt(X0,n2)
| releasedAt(X0,n1)
| happens(sK14(X0,n1),n1) ),
inference(superposition,[],[f159,f220]) ).
fof(f324,plain,
~ less(n2,n1),
inference(resolution,[],[f250,f304]) ).
fof(f326,plain,
~ less(n3,n2),
inference(resolution,[],[f250,f289]) ).
fof(f330,plain,
! [X0] :
( ~ releasedAt(X0,n2)
| releasedAt(X0,n1)
| releases(sK14(X0,n1),X0,n1) ),
inference(superposition,[],[f158,f220]) ).
fof(f439,plain,
! [X0,X1] :
( ~ releasedAt(X1,plus(n1,X0))
| releasedAt(X1,X0)
| releases(sK14(X1,X0),X1,X0) ),
inference(superposition,[],[f158,f226]) ).
fof(f440,plain,
! [X0,X1] :
( ~ releasedAt(X1,plus(n1,X0))
| releasedAt(X1,X0)
| happens(sK14(X1,X0),X0) ),
inference(superposition,[],[f159,f226]) ).
fof(f443,plain,
! [X2,X0,X1] :
( ~ initiates(X2,X1,X0)
| ~ happens(X2,X0)
| ~ releasedAt(X1,plus(n1,X0)) ),
inference(superposition,[],[f164,f226]) ).
fof(f446,plain,
! [X0] :
( n0 = X0
| less(X0,n0)
| ~ less(X0,n1) ),
inference(resolution,[],[f227,f231]) ).
fof(f447,plain,
! [X0] :
( ~ less(X0,n2)
| less(X0,n1)
| n1 = X0 ),
inference(resolution,[],[f227,f233]) ).
fof(f449,plain,
! [X0] :
( less(X0,n2)
| n2 = X0
| ~ less(X0,n3) ),
inference(resolution,[],[f227,f235]) ).
fof(f453,plain,
! [X0] :
( ~ less(X0,n1)
| n0 = X0 ),
inference(global_subsumption,[],[f446,f230]) ).
fof(f503,plain,
less(n0,n2),
inference(resolution,[],[f305,f287]) ).
fof(f504,plain,
less(n0,n3),
inference(resolution,[],[f503,f296]) ).
fof(f779,plain,
! [X0] :
( ~ happens(tapOn,X0)
| ~ releasedAt(filling,plus(n1,X0)) ),
inference(resolution,[],[f443,f300]) ).
fof(f784,plain,
! [X0] :
( ~ releasedAt(X0,n4)
| releasedAt(X0,n3)
| happens(sK14(X0,n3),n3) ),
inference(superposition,[],[f440,f222]) ).
fof(f785,plain,
! [X0] :
( ~ releasedAt(X0,n3)
| releasedAt(X0,n2)
| happens(sK14(X0,n2),n2) ),
inference(superposition,[],[f440,f221]) ).
fof(f844,plain,
! [X0] :
( ~ releasedAt(X0,n3)
| releasedAt(X0,n2)
| releases(sK14(X0,n2),X0,n2) ),
inference(superposition,[],[f439,f221]) ).
fof(f1155,definition,
( spl18_51
<=> n0 = n2 ),
introduced(definition,[new_symbols(definition,[spl18_51])],[avatar_definition]) ).
fof(f1157,plain,
( n0 = n2
| ~ spl18_51 ),
inference(avatar_component_clause,[],[f1155]) ).
fof(f1289,definition,
( spl18_60
<=> n0 = n1 ),
introduced(definition,[new_symbols(definition,[spl18_60])],[avatar_definition]) ).
fof(f1291,plain,
( n0 = n1
| ~ spl18_60 ),
inference(avatar_component_clause,[],[f1289]) ).
fof(f1317,plain,
( ! [X0] : ~ less(X0,n1)
| ~ spl18_60 ),
inference(superposition,[],[f230,f1291]) ).
fof(f1438,plain,
( $false
| ~ spl18_60 ),
inference(resolution,[],[f1317,f287]) ).
fof(f1442,plain,
~ spl18_60,
inference(avatar_contradiction_clause,[],[f1438]) ).
fof(f2234,plain,
! [X0] :
( ~ less(X0,n2)
| n0 = X0
| n1 = X0 ),
inference(global_subsumption,[],[f453,f447]) ).
fof(f2987,plain,
! [X0] :
( ~ less(X0,n3)
| n1 = X0
| n2 = X0
| n0 = X0 ),
inference(resolution,[],[f2234,f449]) ).
fof(f3443,plain,
holdsAt(filling,n1),
inference(resolution,[],[f309,f300]) ).
fof(f3484,plain,
( holdsAt(filling,plus(n1,n1))
| releasedAt(filling,plus(n1,n1))
| happens(sK11(filling,n1),n1) ),
inference(resolution,[],[f3443,f153]) ).
fof(f3485,plain,
( holdsAt(filling,n2)
| releasedAt(filling,plus(n1,n1))
| happens(sK11(filling,n1),n1) ),
inference(forward_demodulation,[],[f3484,f220]) ).
fof(f3489,plain,
( releasedAt(filling,n2)
| holdsAt(filling,n2)
| happens(sK11(filling,n1),n1) ),
inference(forward_demodulation,[],[f3485,f220]) ).
fof(f3496,definition,
( spl18_80
<=> releasedAt(filling,n1) ),
introduced(definition,[new_symbols(definition,[spl18_80])],[avatar_definition]) ).
fof(f3506,definition,
( spl18_82
<=> happens(sK11(filling,n1),n1) ),
introduced(definition,[new_symbols(definition,[spl18_82])],[avatar_definition]) ).
fof(f3508,plain,
( happens(sK11(filling,n1),n1)
| ~ spl18_82 ),
inference(avatar_component_clause,[],[f3506]) ).
fof(f3510,definition,
( spl18_83
<=> holdsAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl18_83])],[avatar_definition]) ).
fof(f3512,plain,
( holdsAt(filling,n2)
| ~ spl18_83 ),
inference(avatar_component_clause,[],[f3510]) ).
fof(f3514,definition,
( spl18_84
<=> releasedAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl18_84])],[avatar_definition]) ).
fof(f3516,plain,
( releasedAt(filling,n2)
| ~ spl18_84 ),
inference(avatar_component_clause,[],[f3514]) ).
fof(f3517,plain,
( spl18_82
| spl18_83
| spl18_84 ),
inference(avatar_split_clause,[],[f3489,f3514,f3510,f3506]) ).
fof(f3556,plain,
( holdsAt(filling,plus(n2,n1))
| releasedAt(filling,plus(n2,n1))
| happens(sK11(filling,n2),n2)
| ~ spl18_83 ),
inference(resolution,[],[f3512,f153]) ).
fof(f3557,plain,
( holdsAt(filling,plus(n1,n2))
| releasedAt(filling,plus(n2,n1))
| happens(sK11(filling,n2),n2)
| ~ spl18_83 ),
inference(forward_demodulation,[],[f3556,f226]) ).
fof(f3559,plain,
( holdsAt(filling,n3)
| releasedAt(filling,plus(n2,n1))
| happens(sK11(filling,n2),n2)
| ~ spl18_83 ),
inference(forward_demodulation,[],[f3557,f221]) ).
fof(f3561,plain,
( releasedAt(filling,plus(n1,n2))
| holdsAt(filling,n3)
| happens(sK11(filling,n2),n2)
| ~ spl18_83 ),
inference(forward_demodulation,[],[f3559,f226]) ).
fof(f3563,plain,
( releasedAt(filling,n3)
| holdsAt(filling,n3)
| happens(sK11(filling,n2),n2)
| ~ spl18_83 ),
inference(forward_demodulation,[],[f3561,f221]) ).
fof(f3566,definition,
( spl18_86
<=> happens(sK11(filling,n2),n2) ),
introduced(definition,[new_symbols(definition,[spl18_86])],[avatar_definition]) ).
fof(f3568,plain,
( happens(sK11(filling,n2),n2)
| ~ spl18_86 ),
inference(avatar_component_clause,[],[f3566]) ).
fof(f3570,definition,
( spl18_87
<=> holdsAt(filling,n3) ),
introduced(definition,[new_symbols(definition,[spl18_87])],[avatar_definition]) ).
fof(f3574,definition,
( spl18_88
<=> releasedAt(filling,n3) ),
introduced(definition,[new_symbols(definition,[spl18_88])],[avatar_definition]) ).
fof(f3576,plain,
( releasedAt(filling,n3)
| ~ spl18_88 ),
inference(avatar_component_clause,[],[f3574]) ).
fof(f3577,plain,
( spl18_86
| spl18_87
| spl18_88
| ~ spl18_83 ),
inference(avatar_split_clause,[],[f3563,f3510,f3574,f3570,f3566]) ).
fof(f4173,plain,
! [X0] : releasedAt(waterLevel(X0),n1),
inference(resolution,[],[f316,f272]) ).
fof(f4716,plain,
( ~ less(n0,n1)
| ~ spl18_51 ),
inference(superposition,[],[f324,f1157]) ).
fof(f4800,plain,
( $false
| ~ spl18_51 ),
inference(global_subsumption,[],[f4716,f287]) ).
fof(f4801,plain,
~ spl18_51,
inference(avatar_contradiction_clause,[],[f4800]) ).
fof(f6019,plain,
~ releasedAt(filling,plus(n1,n0)),
inference(resolution,[],[f779,f284]) ).
fof(f6020,plain,
~ releasedAt(filling,n1),
inference(forward_demodulation,[],[f6019,f281]) ).
fof(f8513,plain,
! [X0,X1] :
( sP7(X0,X1)
| n0 = X0
| ~ happens(X1,X0) ),
inference(resolution,[],[f196,f204]) ).
fof(f9600,plain,
! [X0,X1] :
( ~ happens(X1,X0)
| n0 = X0
| holdsAt(waterLevel(n3),X0) ),
inference(resolution,[],[f8513,f202]) ).
fof(f9601,plain,
! [X0,X1] :
( ~ happens(X1,X0)
| n0 = X0
| holdsAt(filling,X0) ),
inference(resolution,[],[f8513,f201]) ).
fof(f9602,plain,
! [X0,X1] :
( ~ happens(X1,X0)
| n0 = X0
| overflow = X1 ),
inference(resolution,[],[f8513,f200]) ).
fof(f10417,plain,
( releasedAt(filling,n1)
| releases(sK14(filling,n1),filling,n1)
| ~ spl18_84 ),
inference(resolution,[],[f3516,f330]) ).
fof(f10418,plain,
( releasedAt(filling,n1)
| happens(sK14(filling,n1),n1)
| ~ spl18_84 ),
inference(resolution,[],[f3516,f322]) ).
fof(f10426,definition,
( spl18_112
<=> happens(sK14(filling,n1),n1) ),
introduced(definition,[new_symbols(definition,[spl18_112])],[avatar_definition]) ).
fof(f10428,plain,
( happens(sK14(filling,n1),n1)
| ~ spl18_112 ),
inference(avatar_component_clause,[],[f10426]) ).
fof(f10429,plain,
( spl18_112
| spl18_80
| ~ spl18_84 ),
inference(avatar_split_clause,[],[f10418,f3514,f3496,f10426]) ).
fof(f10431,definition,
( spl18_113
<=> releases(sK14(filling,n1),filling,n1) ),
introduced(definition,[new_symbols(definition,[spl18_113])],[avatar_definition]) ).
fof(f10433,plain,
( releases(sK14(filling,n1),filling,n1)
| ~ spl18_113 ),
inference(avatar_component_clause,[],[f10431]) ).
fof(f10434,plain,
( spl18_113
| spl18_80
| ~ spl18_84 ),
inference(avatar_split_clause,[],[f10417,f3514,f3496,f10431]) ).
fof(f10617,plain,
( n0 = n1
| overflow = sK14(filling,n1)
| ~ spl18_112 ),
inference(resolution,[],[f10428,f9602]) ).
fof(f10628,definition,
( spl18_117
<=> overflow = sK14(filling,n1) ),
introduced(definition,[new_symbols(definition,[spl18_117])],[avatar_definition]) ).
fof(f10630,plain,
( overflow = sK14(filling,n1)
| ~ spl18_117 ),
inference(avatar_component_clause,[],[f10628]) ).
fof(f10631,plain,
( spl18_117
| spl18_60
| ~ spl18_112 ),
inference(avatar_split_clause,[],[f10617,f10426,f1289,f10628]) ).
fof(f10632,plain,
~ spl18_80,
inference(avatar_split_clause,[],[f6020,f3496]) ).
fof(f11136,plain,
( releasedAt(filling,n2)
| releases(sK14(filling,n2),filling,n2)
| ~ spl18_88 ),
inference(resolution,[],[f3576,f844]) ).
fof(f11137,plain,
( releasedAt(filling,n2)
| happens(sK14(filling,n2),n2)
| ~ spl18_88 ),
inference(resolution,[],[f3576,f785]) ).
fof(f11863,definition,
( spl18_122
<=> n0 = n3 ),
introduced(definition,[new_symbols(definition,[spl18_122])],[avatar_definition]) ).
fof(f11865,plain,
( n0 = n3
| ~ spl18_122 ),
inference(avatar_component_clause,[],[f11863]) ).
fof(f12408,plain,
( tapOn = sK14(filling,n1)
| ~ spl18_113 ),
inference(resolution,[],[f10433,f194]) ).
fof(f12410,plain,
( tapOn = overflow
| ~ spl18_113
| ~ spl18_117 ),
inference(forward_demodulation,[],[f12408,f10630]) ).
fof(f12414,plain,
( $false
| ~ spl18_113
| ~ spl18_117 ),
inference(global_subsumption,[],[f12410,f210]) ).
fof(f12415,plain,
( ~ spl18_113
| ~ spl18_117 ),
inference(avatar_contradiction_clause,[],[f12414]) ).
fof(f12418,definition,
( spl18_132
<=> happens(sK14(filling,n2),n2) ),
introduced(definition,[new_symbols(definition,[spl18_132])],[avatar_definition]) ).
fof(f12420,plain,
( happens(sK14(filling,n2),n2)
| ~ spl18_132 ),
inference(avatar_component_clause,[],[f12418]) ).
fof(f12421,plain,
( spl18_132
| spl18_84
| ~ spl18_88 ),
inference(avatar_split_clause,[],[f11137,f3574,f3514,f12418]) ).
fof(f12423,definition,
( spl18_133
<=> releases(sK14(filling,n2),filling,n2) ),
introduced(definition,[new_symbols(definition,[spl18_133])],[avatar_definition]) ).
fof(f12425,plain,
( releases(sK14(filling,n2),filling,n2)
| ~ spl18_133 ),
inference(avatar_component_clause,[],[f12423]) ).
fof(f12426,plain,
( spl18_133
| spl18_84
| ~ spl18_88 ),
inference(avatar_split_clause,[],[f11136,f3574,f3514,f12423]) ).
fof(f12833,plain,
( n0 = n2
| overflow = sK14(filling,n2)
| ~ spl18_132 ),
inference(resolution,[],[f12420,f9602]) ).
fof(f12844,definition,
( spl18_134
<=> overflow = sK14(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl18_134])],[avatar_definition]) ).
fof(f12846,plain,
( overflow = sK14(filling,n2)
| ~ spl18_134 ),
inference(avatar_component_clause,[],[f12844]) ).
fof(f12847,plain,
( spl18_134
| spl18_51
| ~ spl18_132 ),
inference(avatar_split_clause,[],[f12833,f12418,f1155,f12844]) ).
fof(f13749,plain,
( tapOn = sK14(filling,n2)
| ~ spl18_133 ),
inference(resolution,[],[f12425,f194]) ).
fof(f13751,plain,
( tapOn = overflow
| ~ spl18_133
| ~ spl18_134 ),
inference(forward_demodulation,[],[f13749,f12846]) ).
fof(f13755,plain,
( $false
| ~ spl18_133
| ~ spl18_134 ),
inference(global_subsumption,[],[f13751,f210]) ).
fof(f13756,plain,
( ~ spl18_133
| ~ spl18_134 ),
inference(avatar_contradiction_clause,[],[f13755]) ).
fof(f14030,plain,
( n0 = n2
| overflow = sK11(filling,n2)
| ~ spl18_86 ),
inference(resolution,[],[f3568,f9602]) ).
fof(f14041,definition,
( spl18_139
<=> overflow = sK11(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl18_139])],[avatar_definition]) ).
fof(f14043,plain,
( overflow = sK11(filling,n2)
| ~ spl18_139 ),
inference(avatar_component_clause,[],[f14041]) ).
fof(f14044,plain,
( spl18_139
| spl18_51
| ~ spl18_86 ),
inference(avatar_split_clause,[],[f14030,f3566,f1155,f14041]) ).
fof(f14153,plain,
( happens(overflow,n2)
| ~ spl18_86
| ~ spl18_139 ),
inference(superposition,[],[f3568,f14043]) ).
fof(f18184,plain,
( ~ less(n0,n2)
| ~ spl18_122 ),
inference(superposition,[],[f326,f11865]) ).
fof(f18318,plain,
( $false
| ~ spl18_122 ),
inference(global_subsumption,[],[f18184,f503]) ).
fof(f18319,plain,
~ spl18_122,
inference(avatar_contradiction_clause,[],[f18318]) ).
fof(f20572,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(n0,X0)),X0),
inference(resolution,[],[f276,f252]) ).
fof(f20595,plain,
trajectory(filling,n0,waterLevel(n3),n3),
inference(superposition,[],[f20572,f219]) ).
fof(f20597,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(X0,n0)),X0),
inference(superposition,[],[f20572,f226]) ).
fof(f20602,definition,
( spl18_192
<=> ! [X0] :
( ~ happens(X0,n0)
| ~ initiates(X0,filling,n0) ) ),
introduced(definition,[new_symbols(definition,[spl18_192])],[avatar_definition]) ).
fof(f20603,plain,
( ! [X0] :
( ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) )
| ~ spl18_192 ),
inference(avatar_component_clause,[],[f20602]) ).
fof(f20654,plain,
! [X0] :
( ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,n3)
| holdsAt(waterLevel(n3),plus(n0,n3))
| stoppedIn(n0,filling,plus(n0,n3)) ),
inference(resolution,[],[f20595,f151]) ).
fof(f20668,plain,
( ~ happens(tapOn,n0)
| ~ spl18_192 ),
inference(resolution,[],[f20603,f300]) ).
fof(f20669,plain,
( $false
| ~ spl18_192 ),
inference(global_subsumption,[],[f20668,f284]) ).
fof(f20670,plain,
~ spl18_192,
inference(avatar_contradiction_clause,[],[f20669]) ).
fof(f20673,plain,
! [X0] :
( holdsAt(waterLevel(n3),n3)
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,n3)
| stoppedIn(n0,filling,plus(n0,n3)) ),
inference(forward_demodulation,[],[f20654,f219]) ).
fof(f20674,plain,
! [X0] :
( stoppedIn(n0,filling,n3)
| holdsAt(waterLevel(n3),n3)
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,n3) ),
inference(forward_demodulation,[],[f20673,f219]) ).
fof(f20675,plain,
! [X0] :
( stoppedIn(n0,filling,n3)
| holdsAt(waterLevel(n3),n3)
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0) ),
inference(global_subsumption,[],[f20674,f504]) ).
fof(f20677,definition,
( spl18_195
<=> holdsAt(waterLevel(n3),n3) ),
introduced(definition,[new_symbols(definition,[spl18_195])],[avatar_definition]) ).
fof(f20679,plain,
( holdsAt(waterLevel(n3),n3)
| ~ spl18_195 ),
inference(avatar_component_clause,[],[f20677]) ).
fof(f20681,definition,
( spl18_196
<=> stoppedIn(n0,filling,n3) ),
introduced(definition,[new_symbols(definition,[spl18_196])],[avatar_definition]) ).
fof(f20683,plain,
( stoppedIn(n0,filling,n3)
| ~ spl18_196 ),
inference(avatar_component_clause,[],[f20681]) ).
fof(f20684,plain,
( spl18_192
| spl18_195
| spl18_196 ),
inference(avatar_split_clause,[],[f20675,f20681,f20677,f20602]) ).
fof(f20694,plain,
trajectory(filling,n0,waterLevel(n1),n1),
inference(superposition,[],[f20597,f281]) ).
fof(f20756,plain,
( sP0(n0,n3,filling)
| ~ spl18_196 ),
inference(resolution,[],[f20683,f150]) ).
fof(f20780,plain,
( happens(sK9(n0,n3,filling),sK10(n0,n3,filling))
| ~ spl18_196 ),
inference(resolution,[],[f20756,f149]) ).
fof(f20781,plain,
( less(n0,sK10(n0,n3,filling))
| ~ spl18_196 ),
inference(resolution,[],[f20756,f148]) ).
fof(f20782,plain,
( less(sK10(n0,n3,filling),n3)
| ~ spl18_196 ),
inference(resolution,[],[f20756,f147]) ).
fof(f20785,plain,
( n0 = n2
| holdsAt(waterLevel(n3),n2)
| ~ spl18_86 ),
inference(resolution,[],[f9600,f3568]) ).
fof(f20792,definition,
( spl18_198
<=> holdsAt(waterLevel(n3),n2) ),
introduced(definition,[new_symbols(definition,[spl18_198])],[avatar_definition]) ).
fof(f20794,plain,
( holdsAt(waterLevel(n3),n2)
| ~ spl18_198 ),
inference(avatar_component_clause,[],[f20792]) ).
fof(f20797,plain,
( spl18_198
| spl18_51
| ~ spl18_86 ),
inference(avatar_split_clause,[],[f20785,f3566,f1155,f20792]) ).
fof(f20799,plain,
( sP7(n2,overflow)
| ~ holdsAt(filling,n2)
| ~ spl18_198 ),
inference(resolution,[],[f20794,f275]) ).
fof(f20801,plain,
( sP1(n2,overflow,waterLevel(n3))
| ~ spl18_198 ),
inference(resolution,[],[f20794,f266]) ).
fof(f20821,definition,
( spl18_201
<=> holdsAt(waterLevel(n3),n1) ),
introduced(definition,[new_symbols(definition,[spl18_201])],[avatar_definition]) ).
fof(f20823,plain,
( holdsAt(waterLevel(n3),n1)
| ~ spl18_201 ),
inference(avatar_component_clause,[],[f20821]) ).
fof(f20832,definition,
( spl18_203
<=> sP7(n2,overflow) ),
introduced(definition,[new_symbols(definition,[spl18_203])],[avatar_definition]) ).
fof(f20834,plain,
( sP7(n2,overflow)
| ~ spl18_203 ),
inference(avatar_component_clause,[],[f20832]) ).
fof(f20835,plain,
( ~ spl18_83
| spl18_203
| ~ spl18_198 ),
inference(avatar_split_clause,[],[f20799,f20792,f20832,f3510]) ).
fof(f20847,definition,
( spl18_205
<=> releasedAt(waterLevel(n3),n3) ),
introduced(definition,[new_symbols(definition,[spl18_205])],[avatar_definition]) ).
fof(f20867,plain,
( sP8(overflow,n2)
| ~ spl18_203 ),
inference(resolution,[],[f20834,f198]) ).
fof(f20896,plain,
( happens(overflow,n2)
| ~ spl18_203 ),
inference(resolution,[],[f20867,f205]) ).
fof(f20930,definition,
( spl18_214
<=> releasedAt(waterLevel(n3),n4) ),
introduced(definition,[new_symbols(definition,[spl18_214])],[avatar_definition]) ).
fof(f20932,plain,
( releasedAt(waterLevel(n3),n4)
| ~ spl18_214 ),
inference(avatar_component_clause,[],[f20930]) ).
fof(f20978,plain,
( releasedAt(waterLevel(n3),n3)
| happens(sK14(waterLevel(n3),n3),n3)
| ~ spl18_214 ),
inference(resolution,[],[f20932,f784]) ).
fof(f21037,definition,
( spl18_223
<=> stoppedIn(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl18_223])],[avatar_definition]) ).
fof(f21039,plain,
( stoppedIn(n0,filling,n1)
| ~ spl18_223 ),
inference(avatar_component_clause,[],[f21037]) ).
fof(f21064,plain,
( sP4(overflow,waterLevel(n3),n2)
| ~ spl18_198 ),
inference(resolution,[],[f20801,f167]) ).
fof(f21112,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,[],[f20694,f151]) ).
fof(f21113,plain,
! [X0] :
( holdsAt(waterLevel(n1),plus(n1,n0))
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,n1)
| stoppedIn(n0,filling,plus(n0,n1)) ),
inference(forward_demodulation,[],[f21112,f226]) ).
fof(f21114,plain,
! [X0] :
( holdsAt(waterLevel(n1),n1)
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,n1)
| stoppedIn(n0,filling,plus(n0,n1)) ),
inference(forward_demodulation,[],[f21113,f281]) ).
fof(f21115,plain,
! [X0] :
( stoppedIn(n0,filling,plus(n1,n0))
| holdsAt(waterLevel(n1),n1)
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,n1) ),
inference(forward_demodulation,[],[f21114,f226]) ).
fof(f21116,plain,
! [X0] :
( stoppedIn(n0,filling,n1)
| holdsAt(waterLevel(n1),n1)
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,n1) ),
inference(forward_demodulation,[],[f21115,f281]) ).
fof(f21117,plain,
! [X0] :
( stoppedIn(n0,filling,n1)
| holdsAt(waterLevel(n1),n1)
| ~ happens(X0,n0)
| ~ initiates(X0,filling,n0) ),
inference(global_subsumption,[],[f21116,f287]) ).
fof(f21119,definition,
( spl18_225
<=> holdsAt(waterLevel(n1),n1) ),
introduced(definition,[new_symbols(definition,[spl18_225])],[avatar_definition]) ).
fof(f21121,plain,
( holdsAt(waterLevel(n1),n1)
| ~ spl18_225 ),
inference(avatar_component_clause,[],[f21119]) ).
fof(f21122,plain,
( spl18_192
| spl18_225
| spl18_223 ),
inference(avatar_split_clause,[],[f21117,f21037,f21119,f20602]) ).
fof(f21123,plain,
( sP0(n0,n1,filling)
| ~ spl18_223 ),
inference(resolution,[],[f21039,f150]) ).
fof(f21126,plain,
( less(n0,sK10(n0,n1,filling))
| ~ spl18_223 ),
inference(resolution,[],[f21123,f148]) ).
fof(f21127,plain,
( less(sK10(n0,n1,filling),n1)
| ~ spl18_223 ),
inference(resolution,[],[f21123,f147]) ).
fof(f21128,plain,
( initiates(overflow,waterLevel(n3),n2)
| ~ spl18_198 ),
inference(resolution,[],[f21064,f183]) ).
fof(f21170,plain,
( ~ happens(overflow,n2)
| ~ releasedAt(waterLevel(n3),plus(n1,n2))
| ~ spl18_198 ),
inference(resolution,[],[f21128,f443]) ).
fof(f21172,plain,
( ~ releasedAt(waterLevel(n3),n3)
| ~ happens(overflow,n2)
| ~ spl18_198 ),
inference(forward_demodulation,[],[f21170,f221]) ).
fof(f21175,definition,
( spl18_226
<=> happens(overflow,n2) ),
introduced(definition,[new_symbols(definition,[spl18_226])],[avatar_definition]) ).
fof(f21176,plain,
( happens(overflow,n2)
| ~ spl18_226 ),
inference(avatar_component_clause,[],[f21175]) ).
fof(f21178,plain,
( ~ spl18_226
| ~ spl18_205
| ~ spl18_198 ),
inference(avatar_split_clause,[],[f21172,f20792,f20847,f21175]) ).
fof(f21179,plain,
( sP7(n3,overflow)
| ~ holdsAt(filling,n3)
| ~ spl18_195 ),
inference(resolution,[],[f20679,f275]) ).
fof(f21181,plain,
( sP1(n3,overflow,waterLevel(n3))
| ~ spl18_195 ),
inference(resolution,[],[f20679,f266]) ).
fof(f21188,plain,
( holdsAt(waterLevel(n3),plus(n3,n1))
| releasedAt(waterLevel(n3),plus(n3,n1))
| terminates(sK11(waterLevel(n3),n3),waterLevel(n3),n3)
| ~ spl18_195 ),
inference(resolution,[],[f20679,f152]) ).
fof(f21189,plain,
( holdsAt(waterLevel(n3),plus(n3,n1))
| releasedAt(waterLevel(n3),plus(n3,n1))
| happens(sK11(waterLevel(n3),n3),n3)
| ~ spl18_195 ),
inference(resolution,[],[f20679,f153]) ).
fof(f21190,plain,
( holdsAt(waterLevel(n3),plus(n1,n3))
| releasedAt(waterLevel(n3),plus(n3,n1))
| happens(sK11(waterLevel(n3),n3),n3)
| ~ spl18_195 ),
inference(forward_demodulation,[],[f21189,f226]) ).
fof(f21191,plain,
( holdsAt(waterLevel(n3),plus(n1,n3))
| releasedAt(waterLevel(n3),plus(n3,n1))
| terminates(sK11(waterLevel(n3),n3),waterLevel(n3),n3)
| ~ spl18_195 ),
inference(forward_demodulation,[],[f21188,f226]) ).
fof(f21193,plain,
( holdsAt(waterLevel(n3),n4)
| releasedAt(waterLevel(n3),plus(n3,n1))
| happens(sK11(waterLevel(n3),n3),n3)
| ~ spl18_195 ),
inference(forward_demodulation,[],[f21190,f222]) ).
fof(f21194,plain,
( holdsAt(waterLevel(n3),n4)
| releasedAt(waterLevel(n3),plus(n3,n1))
| terminates(sK11(waterLevel(n3),n3),waterLevel(n3),n3)
| ~ spl18_195 ),
inference(forward_demodulation,[],[f21191,f222]) ).
fof(f21195,plain,
( releasedAt(waterLevel(n3),plus(n1,n3))
| holdsAt(waterLevel(n3),n4)
| happens(sK11(waterLevel(n3),n3),n3)
| ~ spl18_195 ),
inference(forward_demodulation,[],[f21193,f226]) ).
fof(f21196,plain,
( releasedAt(waterLevel(n3),plus(n1,n3))
| holdsAt(waterLevel(n3),n4)
| terminates(sK11(waterLevel(n3),n3),waterLevel(n3),n3)
| ~ spl18_195 ),
inference(forward_demodulation,[],[f21194,f226]) ).
fof(f21197,plain,
( releasedAt(waterLevel(n3),n4)
| holdsAt(waterLevel(n3),n4)
| happens(sK11(waterLevel(n3),n3),n3)
| ~ spl18_195 ),
inference(forward_demodulation,[],[f21195,f222]) ).
fof(f21198,plain,
( releasedAt(waterLevel(n3),n4)
| holdsAt(waterLevel(n3),n4)
| terminates(sK11(waterLevel(n3),n3),waterLevel(n3),n3)
| ~ spl18_195 ),
inference(forward_demodulation,[],[f21196,f222]) ).
fof(f21216,definition,
( spl18_230
<=> happens(sK14(waterLevel(n3),n3),n3) ),
introduced(definition,[new_symbols(definition,[spl18_230])],[avatar_definition]) ).
fof(f21218,plain,
( happens(sK14(waterLevel(n3),n3),n3)
| ~ spl18_230 ),
inference(avatar_component_clause,[],[f21216]) ).
fof(f21219,plain,
( spl18_230
| spl18_205
| ~ spl18_214 ),
inference(avatar_split_clause,[],[f20978,f20930,f20847,f21216]) ).
fof(f21230,plain,
( sP4(overflow,waterLevel(n3),n3)
| ~ spl18_195 ),
inference(resolution,[],[f21181,f167]) ).
fof(f21273,plain,
( initiates(overflow,waterLevel(n3),n3)
| ~ spl18_195 ),
inference(resolution,[],[f21230,f183]) ).
fof(f21326,plain,
( ~ happens(overflow,n3)
| ~ releasedAt(waterLevel(n3),plus(n1,n3))
| ~ spl18_195 ),
inference(resolution,[],[f21273,f443]) ).
fof(f21328,plain,
( ~ releasedAt(waterLevel(n3),n4)
| ~ happens(overflow,n3)
| ~ spl18_195 ),
inference(forward_demodulation,[],[f21326,f222]) ).
fof(f21330,definition,
( spl18_232
<=> happens(overflow,n3) ),
introduced(definition,[new_symbols(definition,[spl18_232])],[avatar_definition]) ).
fof(f21333,plain,
( ~ spl18_232
| ~ spl18_214
| ~ spl18_195 ),
inference(avatar_split_clause,[],[f21328,f20677,f20930,f21330]) ).
fof(f21834,plain,
( n1 = sK10(n0,n3,filling)
| n2 = sK10(n0,n3,filling)
| n0 = sK10(n0,n3,filling)
| ~ spl18_196 ),
inference(resolution,[],[f20782,f2987]) ).
fof(f21838,definition,
( spl18_266
<=> n2 = sK10(n0,n3,filling) ),
introduced(definition,[new_symbols(definition,[spl18_266])],[avatar_definition]) ).
fof(f21840,plain,
( n2 = sK10(n0,n3,filling)
| ~ spl18_266 ),
inference(avatar_component_clause,[],[f21838]) ).
fof(f21842,definition,
( spl18_267
<=> n1 = sK10(n0,n3,filling) ),
introduced(definition,[new_symbols(definition,[spl18_267])],[avatar_definition]) ).
fof(f21844,plain,
( n1 = sK10(n0,n3,filling)
| ~ spl18_267 ),
inference(avatar_component_clause,[],[f21842]) ).
fof(f21851,definition,
( spl18_269
<=> n0 = sK10(n0,n3,filling) ),
introduced(definition,[new_symbols(definition,[spl18_269])],[avatar_definition]) ).
fof(f21853,plain,
( n0 = sK10(n0,n3,filling)
| ~ spl18_269 ),
inference(avatar_component_clause,[],[f21851]) ).
fof(f21854,plain,
( spl18_269
| spl18_266
| spl18_267
| ~ spl18_196 ),
inference(avatar_split_clause,[],[f21834,f20681,f21842,f21838,f21851]) ).
fof(f21869,plain,
( n0 = sK10(n0,n1,filling)
| ~ spl18_223 ),
inference(resolution,[],[f21127,f453]) ).
fof(f22283,plain,
( less(n0,n0)
| ~ spl18_223 ),
inference(superposition,[],[f21126,f21869]) ).
fof(f22284,plain,
( $false
| ~ spl18_223 ),
inference(resolution,[],[f22283,f230]) ).
fof(f22288,plain,
~ spl18_223,
inference(avatar_contradiction_clause,[],[f22284]) ).
fof(f22330,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n1)
| n1 = X0 )
| ~ spl18_225 ),
inference(resolution,[],[f21121,f207]) ).
fof(f22770,plain,
( releasedAt(waterLevel(n3),n4)
| happens(sK11(waterLevel(n3),n3),n3)
| ~ spl18_195 ),
inference(global_subsumption,[],[f21197,f258]) ).
fof(f22771,plain,
( releasedAt(waterLevel(n3),n4)
| terminates(sK11(waterLevel(n3),n3),waterLevel(n3),n3)
| ~ spl18_195 ),
inference(global_subsumption,[],[f21198,f258]) ).
fof(f22773,definition,
( spl18_350
<=> happens(sK11(waterLevel(n3),n3),n3) ),
introduced(definition,[new_symbols(definition,[spl18_350])],[avatar_definition]) ).
fof(f22775,plain,
( happens(sK11(waterLevel(n3),n3),n3)
| ~ spl18_350 ),
inference(avatar_component_clause,[],[f22773]) ).
fof(f22776,plain,
( spl18_350
| spl18_214
| ~ spl18_195 ),
inference(avatar_split_clause,[],[f22770,f20677,f20930,f22773]) ).
fof(f22778,definition,
( spl18_351
<=> terminates(sK11(waterLevel(n3),n3),waterLevel(n3),n3) ),
introduced(definition,[new_symbols(definition,[spl18_351])],[avatar_definition]) ).
fof(f22780,plain,
( terminates(sK11(waterLevel(n3),n3),waterLevel(n3),n3)
| ~ spl18_351 ),
inference(avatar_component_clause,[],[f22778]) ).
fof(f22781,plain,
( spl18_351
| spl18_214
| ~ spl18_195 ),
inference(avatar_split_clause,[],[f22771,f20677,f20930,f22778]) ).
fof(f22877,plain,
( n0 = n3
| holdsAt(filling,n3)
| ~ spl18_230 ),
inference(resolution,[],[f21218,f9601]) ).
fof(f22893,plain,
( spl18_87
| spl18_122
| ~ spl18_230 ),
inference(avatar_split_clause,[],[f22877,f21216,f11863,f3570]) ).
fof(f22916,plain,
( n0 = n3
| overflow = sK11(waterLevel(n3),n3)
| ~ spl18_350 ),
inference(resolution,[],[f22775,f9602]) ).
fof(f22921,definition,
( spl18_359
<=> overflow = sK11(waterLevel(n3),n3) ),
introduced(definition,[new_symbols(definition,[spl18_359])],[avatar_definition]) ).
fof(f22923,plain,
( overflow = sK11(waterLevel(n3),n3)
| ~ spl18_359 ),
inference(avatar_component_clause,[],[f22921]) ).
fof(f22930,plain,
( spl18_359
| spl18_122
| ~ spl18_350 ),
inference(avatar_split_clause,[],[f22916,f22773,f11863,f22921]) ).
fof(f22939,definition,
( spl18_361
<=> sP7(n3,overflow) ),
introduced(definition,[new_symbols(definition,[spl18_361])],[avatar_definition]) ).
fof(f22941,plain,
( sP7(n3,overflow)
| ~ spl18_361 ),
inference(avatar_component_clause,[],[f22939]) ).
fof(f22942,plain,
( ~ spl18_87
| spl18_361
| ~ spl18_195 ),
inference(avatar_split_clause,[],[f21179,f20677,f22939,f3570]) ).
fof(f22946,plain,
( sP8(overflow,n3)
| ~ spl18_361 ),
inference(resolution,[],[f22941,f198]) ).
fof(f22949,plain,
( happens(overflow,n3)
| ~ spl18_361 ),
inference(resolution,[],[f22946,f205]) ).
fof(f22950,plain,
( spl18_232
| ~ spl18_361 ),
inference(avatar_split_clause,[],[f22949,f22939,f21330]) ).
fof(f22951,plain,
( sP6(sK11(waterLevel(n3),n3),waterLevel(n3))
| ~ spl18_351 ),
inference(resolution,[],[f22780,f191]) ).
fof(f22952,plain,
( sP6(overflow,waterLevel(n3))
| ~ spl18_351
| ~ spl18_359 ),
inference(forward_demodulation,[],[f22951,f22923]) ).
fof(f22993,plain,
( sP5(overflow,waterLevel(n3))
| overflow = tapOff
| ~ spl18_351
| ~ spl18_359 ),
inference(resolution,[],[f22952,f185]) ).
fof(f22997,definition,
( spl18_362
<=> filling = waterLevel(n3) ),
introduced(definition,[new_symbols(definition,[spl18_362])],[avatar_definition]) ).
fof(f22999,plain,
( filling = waterLevel(n3)
| ~ spl18_362 ),
inference(avatar_component_clause,[],[f22997]) ).
fof(f23001,definition,
( spl18_363
<=> sP5(overflow,waterLevel(n3)) ),
introduced(definition,[new_symbols(definition,[spl18_363])],[avatar_definition]) ).
fof(f23003,plain,
( sP5(overflow,waterLevel(n3))
| ~ spl18_363 ),
inference(avatar_component_clause,[],[f23001]) ).
fof(f23005,plain,
( sP5(overflow,waterLevel(n3))
| ~ spl18_351
| ~ spl18_359 ),
inference(global_subsumption,[],[f22993,f209]) ).
fof(f23006,plain,
( spl18_363
| ~ spl18_351
| ~ spl18_359 ),
inference(avatar_split_clause,[],[f23005,f22921,f22778,f23001]) ).
fof(f23021,plain,
( filling = waterLevel(n3)
| ~ spl18_363 ),
inference(resolution,[],[f23003,f188]) ).
fof(f23022,plain,
( spl18_362
| ~ spl18_363 ),
inference(avatar_split_clause,[],[f23021,f23001,f22997]) ).
fof(f23112,plain,
( releasedAt(filling,n1)
| ~ spl18_362 ),
inference(superposition,[],[f4173,f22999]) ).
fof(f23190,plain,
( $false
| ~ spl18_362 ),
inference(global_subsumption,[],[f23112,f6020]) ).
fof(f23191,plain,
~ spl18_362,
inference(avatar_contradiction_clause,[],[f23190]) ).
fof(f23227,plain,
( spl18_226
| ~ spl18_86
| ~ spl18_139 ),
inference(avatar_split_clause,[],[f14153,f14041,f3566,f21175]) ).
fof(f23229,plain,
( spl18_226
| ~ spl18_203 ),
inference(avatar_split_clause,[],[f20896,f20832,f21175]) ).
fof(f24202,plain,
( n0 = n1
| holdsAt(waterLevel(n3),n1)
| ~ spl18_82 ),
inference(resolution,[],[f3508,f9600]) ).
fof(f26749,plain,
( n1 = n3
| ~ spl18_201
| ~ spl18_225 ),
inference(resolution,[],[f22330,f20823]) ).
fof(f26799,plain,
( less(n2,n1)
| ~ spl18_201
| ~ spl18_225 ),
inference(superposition,[],[f289,f26749]) ).
fof(f27014,plain,
( $false
| ~ spl18_201
| ~ spl18_225 ),
inference(global_subsumption,[],[f26799,f324]) ).
fof(f27015,plain,
( ~ spl18_201
| ~ spl18_225 ),
inference(avatar_contradiction_clause,[],[f27014]) ).
fof(f27019,plain,
( spl18_201
| spl18_60
| ~ spl18_82 ),
inference(avatar_split_clause,[],[f24202,f3506,f1289,f20821]) ).
fof(f27172,plain,
( ! [X0] :
( holdsAt(X0,plus(n2,n1))
| ~ initiates(overflow,X0,n2) )
| ~ spl18_226 ),
inference(resolution,[],[f21176,f160]) ).
fof(f27185,plain,
( ! [X0] :
( holdsAt(X0,plus(n1,n2))
| ~ initiates(overflow,X0,n2) )
| ~ spl18_226 ),
inference(forward_demodulation,[],[f27172,f226]) ).
fof(f27188,plain,
( ! [X0] :
( ~ initiates(overflow,X0,n2)
| holdsAt(X0,n3) )
| ~ spl18_226 ),
inference(forward_demodulation,[],[f27185,f221]) ).
fof(f27212,plain,
( sP1(n2,overflow,waterLevel(n3))
| ~ spl18_198 ),
inference(resolution,[],[f20794,f266]) ).
fof(f27255,plain,
( sP4(overflow,waterLevel(n3),n2)
| ~ spl18_198 ),
inference(resolution,[],[f27212,f167]) ).
fof(f27268,plain,
( initiates(overflow,waterLevel(n3),n2)
| ~ spl18_198 ),
inference(resolution,[],[f27255,f183]) ).
fof(f28803,plain,
( holdsAt(waterLevel(n3),n3)
| ~ spl18_198
| ~ spl18_226 ),
inference(resolution,[],[f27188,f27268]) ).
fof(f28805,plain,
( spl18_195
| ~ spl18_198
| ~ spl18_226 ),
inference(avatar_split_clause,[],[f28803,f21175,f20792,f20677]) ).
fof(f34212,plain,
( n0 = sK10(n0,n3,filling)
| holdsAt(waterLevel(n3),sK10(n0,n3,filling))
| ~ spl18_196 ),
inference(resolution,[],[f20780,f9600]) ).
fof(f34232,plain,
( n0 = n2
| holdsAt(waterLevel(n3),sK10(n0,n3,filling))
| ~ spl18_196
| ~ spl18_266 ),
inference(forward_demodulation,[],[f34212,f21840]) ).
fof(f34240,plain,
( holdsAt(waterLevel(n3),n2)
| n0 = n2
| ~ spl18_196
| ~ spl18_266 ),
inference(forward_demodulation,[],[f34232,f21840]) ).
fof(f34245,plain,
( spl18_51
| spl18_198
| ~ spl18_196
| ~ spl18_266 ),
inference(avatar_split_clause,[],[f34240,f21838,f20681,f20792,f1155]) ).
fof(f34259,plain,
( n0 = n1
| holdsAt(waterLevel(n3),sK10(n0,n3,filling))
| ~ spl18_196
| ~ spl18_267 ),
inference(forward_demodulation,[],[f34212,f21844]) ).
fof(f34269,plain,
( holdsAt(waterLevel(n3),n1)
| n0 = n1
| ~ spl18_196
| ~ spl18_267 ),
inference(forward_demodulation,[],[f34259,f21844]) ).
fof(f34277,plain,
( spl18_60
| spl18_201
| ~ spl18_196
| ~ spl18_267 ),
inference(avatar_split_clause,[],[f34269,f21842,f20681,f20821,f1289]) ).
fof(f34368,plain,
( less(n0,n0)
| ~ spl18_196
| ~ spl18_269 ),
inference(superposition,[],[f20781,f21853]) ).
fof(f34378,plain,
( $false
| ~ spl18_196
| ~ spl18_269 ),
inference(resolution,[],[f34368,f230]) ).
fof(f34382,plain,
( ~ spl18_196
| ~ spl18_269 ),
inference(avatar_contradiction_clause,[],[f34378]) ).
cnf(s588,plain,
~ spl18_60,
inference(sat_conversion,[],[f1442]) ).
cnf(s910,plain,
( spl18_82
| spl18_83
| spl18_84 ),
inference(sat_conversion,[],[f3517]) ).
cnf(s920,plain,
( ~ spl18_83
| spl18_86
| spl18_87
| spl18_88 ),
inference(sat_conversion,[],[f3577]) ).
cnf(s1057,plain,
~ spl18_51,
inference(sat_conversion,[],[f4801]) ).
cnf(s1278,plain,
( spl18_80
| ~ spl18_84
| spl18_112 ),
inference(sat_conversion,[],[f10429]) ).
cnf(s1280,plain,
( spl18_80
| ~ spl18_84
| spl18_113 ),
inference(sat_conversion,[],[f10434]) ).
cnf(s1291,plain,
( spl18_60
| ~ spl18_112
| spl18_117 ),
inference(sat_conversion,[],[f10631]) ).
cnf(s1300,plain,
~ spl18_80,
inference(sat_conversion,[],[f10632]) ).
cnf(s1371,plain,
( ~ spl18_113
| ~ spl18_117 ),
inference(sat_conversion,[],[f12415]) ).
cnf(s1375,plain,
( spl18_84
| ~ spl18_88
| spl18_132 ),
inference(sat_conversion,[],[f12421]) ).
cnf(s1377,plain,
( spl18_84
| ~ spl18_88
| spl18_133 ),
inference(sat_conversion,[],[f12426]) ).
cnf(s1387,plain,
( spl18_51
| ~ spl18_132
| spl18_134 ),
inference(sat_conversion,[],[f12847]) ).
cnf(s1419,plain,
( ~ spl18_133
| ~ spl18_134 ),
inference(sat_conversion,[],[f13756]) ).
cnf(s1433,plain,
( spl18_51
| ~ spl18_86
| spl18_139 ),
inference(sat_conversion,[],[f14044]) ).
cnf(s1738,plain,
~ spl18_122,
inference(sat_conversion,[],[f18319]) ).
cnf(s1911,plain,
~ spl18_192,
inference(sat_conversion,[],[f20670]) ).
cnf(s1917,plain,
( spl18_192
| spl18_195
| spl18_196 ),
inference(sat_conversion,[],[f20684]) ).
cnf(s1959,plain,
( spl18_51
| ~ spl18_86
| spl18_198 ),
inference(sat_conversion,[],[f20797]) ).
cnf(s1973,plain,
( ~ spl18_83
| ~ spl18_198
| spl18_203 ),
inference(sat_conversion,[],[f20835]) ).
cnf(s2036,plain,
( spl18_192
| spl18_223
| spl18_225 ),
inference(sat_conversion,[],[f21122]) ).
cnf(s2049,plain,
( ~ spl18_198
| ~ spl18_205
| ~ spl18_226 ),
inference(sat_conversion,[],[f21178]) ).
cnf(s2063,plain,
( spl18_205
| ~ spl18_214
| spl18_230 ),
inference(sat_conversion,[],[f21219]) ).
cnf(s2092,plain,
( ~ spl18_195
| ~ spl18_214
| ~ spl18_232 ),
inference(sat_conversion,[],[f21333]) ).
cnf(s2289,plain,
( ~ spl18_196
| spl18_266
| spl18_267
| spl18_269 ),
inference(sat_conversion,[],[f21854]) ).
cnf(s2462,plain,
~ spl18_223,
inference(sat_conversion,[],[f22288]) ).
cnf(s2645,plain,
( ~ spl18_195
| spl18_214
| spl18_350 ),
inference(sat_conversion,[],[f22776]) ).
cnf(s2647,plain,
( ~ spl18_195
| spl18_214
| spl18_351 ),
inference(sat_conversion,[],[f22781]) ).
cnf(s2680,plain,
( spl18_87
| spl18_122
| ~ spl18_230 ),
inference(sat_conversion,[],[f22893]) ).
cnf(s2699,plain,
( spl18_122
| ~ spl18_350
| spl18_359 ),
inference(sat_conversion,[],[f22930]) ).
cnf(s2711,plain,
( ~ spl18_87
| ~ spl18_195
| spl18_361 ),
inference(sat_conversion,[],[f22942]) ).
cnf(s2715,plain,
( spl18_232
| ~ spl18_361 ),
inference(sat_conversion,[],[f22950]) ).
cnf(s2730,plain,
( ~ spl18_351
| ~ spl18_359
| spl18_363 ),
inference(sat_conversion,[],[f23006]) ).
cnf(s2733,plain,
( spl18_362
| ~ spl18_363 ),
inference(sat_conversion,[],[f23022]) ).
cnf(s2809,plain,
~ spl18_362,
inference(sat_conversion,[],[f23191]) ).
cnf(s2829,plain,
( ~ spl18_86
| ~ spl18_139
| spl18_226 ),
inference(sat_conversion,[],[f23227]) ).
cnf(s2833,plain,
( ~ spl18_203
| spl18_226 ),
inference(sat_conversion,[],[f23229]) ).
cnf(s4382,plain,
( ~ spl18_201
| ~ spl18_225 ),
inference(sat_conversion,[],[f27015]) ).
cnf(s4394,plain,
( spl18_60
| ~ spl18_82
| spl18_201 ),
inference(sat_conversion,[],[f27019]) ).
cnf(s5109,plain,
( spl18_195
| ~ spl18_198
| ~ spl18_226 ),
inference(sat_conversion,[],[f28805]) ).
cnf(s7251,plain,
( spl18_51
| ~ spl18_196
| spl18_198
| ~ spl18_266 ),
inference(sat_conversion,[],[f34245]) ).
cnf(s7261,plain,
( spl18_60
| ~ spl18_196
| spl18_201
| ~ spl18_267 ),
inference(sat_conversion,[],[f34277]) ).
cnf(s7291,plain,
( ~ spl18_196
| ~ spl18_269 ),
inference(sat_conversion,[],[f34382]) ).
cnf(s7362,plain,
~ spl18_363,
inference(rat,[],[s2733,s2809]) ).
cnf(s7363,plain,
( ~ spl18_351
| ~ spl18_359 ),
inference(rat,[],[s2730,s7362]) ).
cnf(s7373,plain,
( spl18_192
| spl18_225 ),
inference(rat,[],[s2036,s2462]) ).
cnf(s7378,plain,
spl18_225,
inference(rat,[],[s7373,s1911]) ).
cnf(s7380,plain,
~ spl18_201,
inference(rat,[],[s4382,s7378]) ).
cnf(s7407,plain,
( ~ spl18_84
| spl18_113 ),
inference(rat,[],[s1280,s1300]) ).
cnf(s7408,plain,
( ~ spl18_84
| spl18_112 ),
inference(rat,[],[s1278,s1300]) ).
cnf(s7436,plain,
~ spl18_82,
inference(rat,[],[s4394,s7380,s588]) ).
cnf(s7462,plain,
~ spl18_84,
inference(rat,[],[s1291,s1371,s7408,s7407,s588]) ).
cnf(s7463,plain,
spl18_83,
inference(rat,[],[s910,s7436,s7462]) ).
cnf(s7465,plain,
( spl18_214
| ~ spl18_195 ),
inference(rat,[],[s2699,s7363,s2645,s2647,s1738]) ).
cnf(s7466,plain,
( ~ spl18_232
| ~ spl18_195 ),
inference(rat,[],[s7465,s2092]) ).
cnf(s7467,plain,
( ~ spl18_87
| ~ spl18_195 ),
inference(rat,[],[s7466,s2715,s2711]) ).
cnf(s7470,plain,
~ spl18_88,
inference(rat,[],[s1387,s1419,s1375,s1377,s1057,s7462]) ).
cnf(s7473,plain,
~ spl18_195,
inference(rat,[],[s2829,s2049,s1433,s1959,s920,s2063,s2680,s7467,s7465,s1057,s7470,s7463,s1738]) ).
cnf(s7483,plain,
spl18_196,
inference(rat,[],[s1917,s1911,s7473]) ).
cnf(s7485,plain,
~ spl18_269,
inference(rat,[],[s7291,s7483]) ).
cnf(s7486,plain,
~ spl18_267,
inference(rat,[],[s7261,s588,s7380,s7483]) ).
cnf(s7487,plain,
spl18_266,
inference(rat,[],[s2289,s7485,s7486,s7483]) ).
cnf(s7489,plain,
spl18_198,
inference(rat,[],[s7251,s7483,s1057,s7487]) ).
cnf(s7491,plain,
spl18_203,
inference(rat,[],[s1973,s7463,s7489]) ).
cnf(s7492,plain,
~ spl18_226,
inference(rat,[],[s5109,s7473,s7489]) ).
cnf(s7494,plain,
$false,
inference(rat,[],[s2833,s7492,s7491]) ).
fof(f34383,plain,
$false,
inference(avatar_sat_refutation,[],[s7494]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR001+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.18 % Computer : n017.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 22:00:21 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 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
% 23.90/3.60 % (4084848)Will run a generic schedule for satisfiability detection.
% 23.90/3.60 % (4084861)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1655880221:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 23.90/3.60 % (4084857)% WARNING: option uhcvi not known.
% 23.90/3.60 % (4084857)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3374575788:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 23.90/3.60 % (4084858)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=695289653:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 23.90/3.60 % (4084859)dis+10_1_sil=32000:sp=arity:random_seed=1012082681:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 23.90/3.60 % (4084860)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=587685879:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 23.90/3.60 % (4084856)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1105276863_2999 on theBenchmark for (2999ds/0Mi)
% 23.90/3.60 % (4084862)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1461700768:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 23.90/3.60 % Detected minimum model sizes of [3]
% 23.90/3.60 % Detected maximum model sizes of [max]
% 23.90/3.60 % TRYING [3]
% 23.90/3.60 % TRYING [4]
% 23.90/3.60 % TRYING [5]
% 23.90/3.60 % (4084861)Instruction limit reached!
% 23.90/3.60 % (4084861)------------------------------
% 23.90/3.60 % (4084861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.90/3.60 % (4084861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.90/3.60 % (4084861)CaDiCaL version: 2.1.3
% 23.90/3.60 % (4084861)Termination reason: Instruction limit
% 23.90/3.60 % (4084861)Termination phase: Saturation
% 23.90/3.60 % (4084861)Time elapsed: 0.046 s
% 23.90/3.60 % (4084861)Peak memory usage: 13 MB
% 23.90/3.60 % (4084861)Instructions burned: 131 (million)
% 23.90/3.60 % (4084886)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1967417235:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 23.90/3.60 % Detected minimum model sizes of [3]
% 23.90/3.60 % Detected maximum model sizes of [max]
% 23.90/3.60 % TRYING [3]
% 23.90/3.60 % TRYING [4]
% 23.90/3.60 % (4084859)Instruction limit reached!
% 23.90/3.60 % (4084859)------------------------------
% 23.90/3.60 % (4084859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.90/3.60 % (4084859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.90/3.60 % (4084859)CaDiCaL version: 2.1.3
% 23.90/3.60 % (4084859)Termination reason: Instruction limit
% 23.90/3.60 % (4084859)Termination phase: Saturation
% 23.90/3.60 % (4084859)Time elapsed: 0.071 s
% 23.90/3.60 % (4084859)Peak memory usage: 12 MB
% 23.90/3.60 % (4084859)Instructions burned: 103 (million)
% 23.90/3.60 % TRYING [5]
% 23.90/3.60 % TRYING [6]
% 23.90/3.60 % (4084860)Instruction limit reached!
% 23.90/3.60 % (4084860)------------------------------
% 23.90/3.60 % (4084860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.90/3.60 % (4084860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.90/3.60 % (4084860)CaDiCaL version: 2.1.3
% 23.90/3.60 % (4084860)Termination reason: Instruction limit
% 23.90/3.60 % (4084860)Termination phase: Saturation
% 23.90/3.60 % (4084860)Time elapsed: 0.082 s
% 23.90/3.60 % (4084860)Peak memory usage: 13 MB
% 23.90/3.60 % (4084860)Instructions burned: 117 (million)
% 23.90/3.60 % (4084892)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2623692304:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 23.90/3.60 % TRYING [6]
% 23.90/3.60 % (4084896)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=51866103:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 23.90/3.60 % (4084862)Instruction limit reached!
% 23.90/3.60 % (4084862)------------------------------
% 23.90/3.60 % (4084862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.90/3.60 % (4084862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.90/3.60 % (4084862)CaDiCaL version: 2.1.3
% 23.90/3.60 % (4084862)Termination reason: Instruction limit
% 23.90/3.60 % (4084862)Termination phase: Saturation
% 23.90/3.60 % (4084862)Time elapsed: 0.115 s
% 23.90/3.60 % (4084862)Peak memory usage: 12 MB
% 23.90/3.60 % (4084862)Instructions burned: 160 (million)
% 23.90/3.60 % (4084908)ott-21_1_sil=16000:fs=off:random_seed=2524182643:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 23.90/3.60 % TRYING [7]
% 23.90/3.60 % TRYING [7]
% 23.90/3.60 % (4084892)Instruction limit reached!
% 59.50/8.79 % (4084892)------------------------------
% 59.50/8.79 % (4084892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.50/8.79 % (4084892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.50/8.79 % (4084892)CaDiCaL version: 2.1.3
% 59.50/8.79 % (4084892)Termination reason: Instruction limit
% 59.50/8.79 % (4084892)Termination phase: Saturation
% 59.50/8.79 % (4084892)Time elapsed: 0.093 s
% 59.50/8.79 % (4084892)Peak memory usage: 13 MB
% 59.50/8.79 % (4084892)Instructions burned: 131 (million)
% 59.50/8.79 % (4084886)Instruction limit reached!
% 59.50/8.79 % (4084886)------------------------------
% 59.50/8.79 % (4084886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.50/8.79 % (4084886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.50/8.79 % (4084886)CaDiCaL version: 2.1.3
% 59.50/8.79 % (4084886)Termination reason: Instruction limit
% 59.50/8.79 % (4084886)Termination phase: Finite model building constraint generation
% 59.50/8.79 % (4084886)Time elapsed: 0.161 s
% 59.50/8.79 % (4084886)Peak memory usage: 28 MB
% 59.50/8.79 % (4084886)Instructions burned: 715 (million)
% 59.50/8.79 % (4084927)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2206032185:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 59.50/8.79 % (4084935)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3532273402:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 59.50/8.79 % Detected minimum model sizes of [3]
% 59.50/8.79 % Detected maximum model sizes of [max]
% 59.50/8.79 % TRYING [3]
% 59.50/8.79 % TRYING [4]
% 59.50/8.79 % (4084908)Instruction limit reached!
% 59.50/8.79 % (4084908)------------------------------
% 59.50/8.79 % (4084908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.50/8.79 % (4084908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.50/8.79 % (4084908)CaDiCaL version: 2.1.3
% 59.50/8.79 % (4084908)Termination reason: Instruction limit
% 59.50/8.79 % (4084908)Termination phase: Saturation
% 59.50/8.79 % (4084908)Time elapsed: 0.154 s
% 59.50/8.79 % (4084908)Peak memory usage: 13 MB
% 59.50/8.79 % (4084908)Instructions burned: 180 (million)
% 59.50/8.79 % TRYING [5]
% 59.50/8.79 % (4084948)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3545769091:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 59.50/8.79 % TRYING [8]
% 59.50/8.79 % TRYING [6]
% 59.50/8.79 % (4084935)Instruction limit reached!
% 59.50/8.79 % (4084935)------------------------------
% 59.50/8.79 % (4084935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.50/8.79 % (4084935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.50/8.79 % (4084935)CaDiCaL version: 2.1.3
% 59.50/8.79 % (4084935)Termination reason: Instruction limit
% 59.50/8.79 % (4084935)Termination phase: Finite model building SAT solving
% 59.50/8.79 % (4084935)Time elapsed: 0.354 s
% 59.50/8.79 % (4084935)Peak memory usage: 25 MB
% 59.50/8.79 % (4084935)Instructions burned: 865 (million)
% 59.50/8.79 % (4084966)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=746241815:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 59.50/8.79 % (4084896)Instruction limit reached!
% 59.50/8.79 % (4084896)------------------------------
% 59.50/8.79 % (4084896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.50/8.79 % (4084896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.50/8.79 % (4084896)CaDiCaL version: 2.1.3
% 59.50/8.79 % (4084896)Termination reason: Instruction limit
% 59.50/8.79 % (4084896)Termination phase: Saturation
% 59.50/8.79 % (4084896)Time elapsed: 0.538 s
% 59.50/8.79 % (4084896)Peak memory usage: 14 MB
% 59.50/8.79 % (4084896)Instructions burned: 684 (million)
% 59.50/8.79 % (4084968)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=667641578:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 59.50/8.79 % (4084927)Instruction limit reached!
% 59.50/8.79 % (4084927)------------------------------
% 59.50/8.79 % (4084927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 59.50/8.79 % (4084927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.50/8.79 % (4084927)CaDiCaL version: 2.1.3
% 59.50/8.79 % (4084927)Termination reason: Instruction limit
% 59.50/8.79 % (4084927)Termination phase: Saturation
% 59.50/8.79 % (4084927)Time elapsed: 0.478 s
% 59.50/8.79 % (4084927)Peak memory usage: 13 MB
% 59.50/8.79 % (4084927)Instructions burned: 478 (million)
% 54.42/14.04 % TRYING [14]
% 54.42/14.04 % (4084970)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3581433755:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 54.42/14.04 % TRYING [9]
% 54.42/14.04 % (4084966)Instruction limit reached!
% 54.42/14.04 % (4084966)------------------------------
% 54.42/14.04 % (4084966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.42/14.04 % (4084966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.42/14.04 % (4084966)CaDiCaL version: 2.1.3
% 54.42/14.04 % (4084966)Termination reason: Instruction limit
% 54.42/14.04 % (4084966)Termination phase: Finite model building constraint generation
% 54.42/14.04 % (4084966)Time elapsed: 0.375 s
% 54.42/14.04 % (4084966)Peak memory usage: 79 MB
% 54.42/14.04 % (4084966)Instructions burned: 891 (million)
% 54.42/14.04 % (4084977)fmb+10_1_sil=64000:random_seed=4071042042:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 54.42/14.04 % Detected minimum model sizes of [3]
% 54.42/14.04 % Detected maximum model sizes of [max]
% 54.42/14.04 % TRYING [3]
% 54.42/14.04 % TRYING [4]
% 54.42/14.04 % TRYING [5]
% 54.42/14.04 % TRYING [6]
% 54.42/14.04 % (4084968)Instruction limit reached!
% 54.42/14.04 % (4084968)------------------------------
% 54.42/14.04 % (4084968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.42/14.04 % (4084968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.42/14.04 % (4084968)CaDiCaL version: 2.1.3
% 54.42/14.04 % (4084968)Termination reason: Instruction limit
% 54.42/14.04 % (4084968)Termination phase: Saturation
% 54.42/14.04 % (4084968)Time elapsed: 0.542 s
% 54.42/14.04 % (4084968)Peak memory usage: 16 MB
% 54.42/14.04 % (4084968)Instructions burned: 692 (million)
% 54.42/14.04 % (4084987)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1458515546:i=9515:nm=5_2987 on theBenchmark for (2987ds/9515Mi)
% 54.42/14.04 % Detected minimum model sizes of [3]
% 54.42/14.04 % Detected maximum model sizes of [max]
% 54.42/14.04 % TRYING [20]
% 54.42/14.04 % TRYING [7]
% 54.42/14.04 % (4084948)Instruction limit reached!
% 54.42/14.04 % (4084948)------------------------------
% 54.42/14.04 % (4084948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.42/14.04 % (4084948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.42/14.04 % (4084948)CaDiCaL version: 2.1.3
% 54.42/14.04 % (4084948)Termination reason: Instruction limit
% 54.42/14.04 % (4084948)Termination phase: Saturation
% 54.42/14.04 % (4084948)Time elapsed: 1.105 s
% 54.42/14.04 % (4084948)Peak memory usage: 18 MB
% 54.42/14.04 % (4084948)Instructions burned: 1180 (million)
% 54.42/14.04 % (4084994)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3970317292:fmbsr=1.7:i=920_2985 on theBenchmark for (2985ds/920Mi)
% 54.42/14.04 % Detected minimum model sizes of [3]
% 54.42/14.04 % Detected maximum model sizes of [max]
% 54.42/14.04 % TRYING [8]
% 54.42/14.04 % TRYING [8]
% 54.42/14.04 % (4084970)Instruction limit reached!
% 54.42/14.04 % (4084970)------------------------------
% 54.42/14.04 % (4084970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.42/14.04 % (4084970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.42/14.04 % (4084970)CaDiCaL version: 2.1.3
% 54.42/14.04 % (4084970)Termination reason: Instruction limit
% 54.42/14.04 % (4084970)Termination phase: Saturation
% 54.42/14.04 % (4084970)Time elapsed: 0.877 s
% 54.42/14.04 % (4084970)Peak memory usage: 19 MB
% 54.42/14.04 % (4084970)Instructions burned: 880 (million)
% 54.42/14.04 % (4085000)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3605667344:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 54.42/14.04 % TRYING [10]
% 54.42/14.04 % TRYING [9]
% 54.42/14.04 % (4084994)Instruction limit reached!
% 54.42/14.04 % (4084994)------------------------------
% 54.42/14.04 % (4084994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.42/14.04 % (4084994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.42/14.04 % (4084994)CaDiCaL version: 2.1.3
% 54.42/14.04 % (4084994)Termination reason: Instruction limit
% 54.42/14.04 % (4084994)Termination phase: Finite model building constraint generation
% 54.42/14.04 % (4084994)Time elapsed: 0.687 s
% 54.42/14.04 % (4084994)Peak memory usage: 52 MB
% 54.42/14.04 % (4084994)Instructions burned: 920 (million)
% 54.42/14.04 % TRYING [9]
% 54.42/14.04 % (4085004)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=585661948:i=1472:ins=7:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/1472Mi)
% 54.42/14.04 % TRYING [10]
% 54.42/14.04 % TRYING [11]
% 54.42/14.04 % (4085004)Instruction limit reached!
% 54.42/14.04 % (4085004)------------------------------
% 54.42/14.04 % (4085004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.42/14.04 % (4085004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.42/14.04 % (4085004)CaDiCaL version: 2.1.3
% 54.42/14.04 % (4085004)Termination reason: Instruction limit
% 54.42/14.04 % (4085004)Termination phase: Saturation
% 54.42/14.04 % (4085004)Time elapsed: 1.131 s
% 54.42/14.04 % (4085004)Peak memory usage: 26 MB
% 54.42/14.04 % (4085004)Instructions burned: 1472 (million)
% 54.42/14.04 % (4085008)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3265310839:i=6324_2966 on theBenchmark for (2966ds/6324Mi)
% 54.42/14.04 % Detected minimum model sizes of [3]
% 54.42/14.04 % Detected maximum model sizes of [max]
% 54.42/14.04 % TRYING [77]
% 54.42/14.04 % TRYING [11]
% 54.42/14.04 % TRYING [12]
% 54.42/14.04 % (4085000)Instruction limit reached!
% 54.42/14.04 % (4085000)------------------------------
% 54.42/14.04 % (4085000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.42/14.04 % (4085000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.42/14.04 % (4085000)CaDiCaL version: 2.1.3
% 54.42/14.04 % (4085000)Termination reason: Instruction limit
% 54.42/14.04 % (4085000)Termination phase: Saturation
% 54.42/14.04 % (4085000)Time elapsed: 4.533 s
% 54.42/14.04 % (4085000)Peak memory usage: 24 MB
% 54.42/14.04 % (4085000)Instructions burned: 5131 (million)
% 54.42/14.04 % (4085026)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1052083675:fmbsr=2.30978:i=2174_2937 on theBenchmark for (2937ds/2174Mi)
% 54.42/14.04 % Detected minimum model sizes of [3]
% 54.42/14.04 % Detected maximum model sizes of [max]
% 54.42/14.04 % TRYING [16]
% 54.42/14.04 % TRYING [12]
% 54.42/14.04 % (4085026)Instruction limit reached!
% 54.42/14.04 % (4085026)------------------------------
% 54.42/14.04 % (4085026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.42/14.04 % (4085026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.42/14.04 % (4085026)CaDiCaL version: 2.1.3
% 54.42/14.04 % (4085026)Termination reason: Instruction limit
% 54.42/14.04 % (4085026)Termination phase: Finite model building constraint generation
% 54.42/14.04 % (4085026)Time elapsed: 1.480 s
% 54.42/14.04 % (4085026)Peak memory usage: 134 MB
% 54.42/14.04 % (4085026)Instructions burned: 2176 (million)
% 54.42/14.04 % (4085030)ott-2_1_sil=16000:newcnf=on:random_seed=2111123667:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2922 on theBenchmark for (2922ds/869Mi)
% 54.42/14.04 % (4084987)Instruction limit reached!
% 54.42/14.04 % (4084987)------------------------------
% 54.42/14.04 % (4084987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.42/14.04 % (4084987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.42/14.04 % (4084987)CaDiCaL version: 2.1.3
% 54.42/14.04 % (4084987)Termination reason: Instruction limit
% 54.42/14.04 % (4084987)Termination phase: Finite model building constraint generation
% 54.42/14.04 % (4084987)Time elapsed: 6.721 s
% 54.42/14.04 % (4084987)Peak memory usage: 611 MB
% 54.42/14.04 % (4084987)Instructions burned: 9515 (million)
% 54.42/14.04 % (4085008)Instruction limit reached!
% 54.42/14.04 % (4085008)------------------------------
% 54.42/14.04 % (4085008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.42/14.04 % (4085008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.42/14.04 % (4085008)CaDiCaL version: 2.1.3
% 54.42/14.04 % (4085008)Termination reason: Instruction limit
% 54.42/14.04 % (4085008)Termination phase: Finite model building constraint generation
% 54.42/14.04 % (4085008)Time elapsed: 4.679 s
% 54.42/14.04 % (4085008)Peak memory usage: 516 MB
% 54.42/14.04 % (4085008)Instructions burned: 6324 (million)
% 54.42/14.04 % (4085032)ott+10_1_sil=32000:tgt=ground:random_seed=2237317435:i=5114:av=off_2918 on theBenchmark for (2918ds/5114Mi)
% 54.42/14.04 % (4085034)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=219089104:i=54282_2918 on theBenchmark for (2918ds/54282Mi)
% 54.42/14.04 % Detected minimum model sizes of [3]
% 54.42/14.04 % Detected maximum model sizes of [max]
% 54.42/14.04 % TRYING [3]
% 54.42/14.04 % TRYING [4]
% 54.42/14.04 % TRYING [5]
% 54.42/14.04 % TRYING [6]
% 54.42/14.04 % TRYING [7]
% 54.42/14.04 % (4085030)Instruction limit reached!
% 54.42/14.04 % (4085030)------------------------------
% 54.42/14.04 % (4085030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.42/14.04 % (4085030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.42/14.04 % (4085030)CaDiCaL version: 2.1.3
% 54.42/14.04 % (4085030)Termination reason: Instruction limit
% 54.42/14.04 % (4085030)Termination phase: Saturation
% 54.42/14.04 % (4085030)Time elapsed: 0.780 s
% 54.42/14.04 % (4085030)Peak memory usage: 15 MB
% 54.42/14.04 % (4085030)Instructions burned: 870 (million)
% 54.42/14.04 % (4085038)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3038693635:i=3512:aac=none_2914 on theBenchmark for (2914ds/3512Mi)
% 54.42/14.04 % TRYING [8]
% 54.42/14.04 % TRYING [9]
% 54.42/14.04 % TRYING [13]
% 54.42/14.04 % TRYING [10]
% 54.42/14.04 % (4084977)Instruction limit reached!
% 54.42/14.04 % (4084977)------------------------------
% 54.42/14.04 % (4084977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.42/14.04 % (4084977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.42/14.04 % (4084977)CaDiCaL version: 2.1.3
% 54.42/14.04 % (4084977)Termination reason: Instruction limit
% 54.42/14.04 % (4084977)Termination phase: Finite model building SAT solving
% 54.42/14.04 % (4084977)Time elapsed: 9.232 s
% 54.42/14.04 % (4084977)Peak memory usage: 232 MB
% 54.42/14.04 % (4084977)Instructions burned: 22064 (million)
% 54.42/14.04 % (4085042)dis+21_1_sil=32000:sas=cadical:random_seed=2346694233:i=3773:amm=off_2896 on theBenchmark for (2896ds/3773Mi)
% 54.42/14.04 % TRYING [11]
% 54.42/14.04 % (4085038)Instruction limit reached!
% 54.42/14.04 % (4085038)------------------------------
% 54.42/14.04 % (4085038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.42/14.05 % (4085038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.42/14.05 % (4085038)CaDiCaL version: 2.1.3
% 54.42/14.05 % (4085038)Termination reason: Instruction limit
% 54.42/14.05 % (4085038)Termination phase: Saturation
% 54.42/14.05 % (4085038)Time elapsed: 3.196 s
% 54.42/14.05 % (4085038)Peak memory usage: 26 MB
% 54.42/14.05 % (4085038)Instructions burned: 3513 (million)
% 54.42/14.05 % (4085044)ott+11_1_sil=16000:gs=on:random_seed=646310022:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2882 on theBenchmark for (2882ds/2251Mi)
% 54.42/14.05 % (4085042)Instruction limit reached!
% 54.42/14.05 % (4085042)------------------------------
% 54.42/14.05 % (4085042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.42/14.05 % (4085042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.42/14.05 % (4085042)CaDiCaL version: 2.1.3
% 54.42/14.05 % (4085042)Termination reason: Instruction limit
% 54.42/14.05 % (4085042)Termination phase: Saturation
% 54.42/14.05 % (4085042)Time elapsed: 1.875 s
% 54.42/14.05 % (4085042)Peak memory usage: 25 MB
% 54.42/14.05 % (4085042)Instructions burned: 3774 (million)
% 54.42/14.05 % (4085046)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4007140902:fmbsr=1.6:i=67534_2877 on theBenchmark for (2877ds/67534Mi)
% 54.42/14.05 % Detected minimum model sizes of [3]
% 54.42/14.05 % Detected maximum model sizes of [max]
% 54.42/14.05 % TRYING [7]
% 54.42/14.05 % (4085032)Instruction limit reached!
% 54.42/14.05 % (4085032)------------------------------
% 54.42/14.05 % (4085032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.42/14.05 % (4085032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.42/14.05 % (4085032)CaDiCaL version: 2.1.3
% 54.42/14.05 % (4085032)Termination reason: Instruction limit
% 54.42/14.05 % (4085032)Termination phase: Saturation
% 54.42/14.05 % (4085032)Time elapsed: 4.307 s
% 54.42/14.05 % (4085032)Peak memory usage: 23 MB
% 54.42/14.05 % (4085032)Instructions burned: 5114 (million)
% 54.42/14.05 % (4085048)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=360728922:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2875 on theBenchmark for (2875ds/4591Mi)
% 54.42/14.05 % TRYING [8]
% 54.42/14.05 % (4085044) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4084848-4085044"...
% 54.42/14.05 % (4085044)...printing done.
% 54.42/14.05 % (4085044)Refutation found. Thanks to Tanya!
% 54.42/14.05 % SZS status Theorem for theBenchmark
% 54.42/14.05 % SZS output start Proof for theBenchmark
% See solution above
% 54.42/14.06 % (4085044)------------------------------
% 54.42/14.06 % (4085044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.42/14.06 % (4085044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.42/14.06 % (4085044)CaDiCaL version: 2.1.3
% 54.42/14.06 % (4085044)Termination reason: Refutation
% 54.42/14.06 % (4085044)Time elapsed: 1.879 s
% 54.42/14.06 % (4085044)Peak memory usage: 28 MB
% 54.42/14.06 % (4085044)Instructions burned: 2044 (million)
% 54.42/14.06 % (4084848)Success in time 13.818 s
% 54.42/14.06 % Vampire exiting
%------------------------------------------------------------------------------