%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR011+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:44:20 AM UTC 2026
% Result : Theorem 47.42s 8.06s
% Output : Refutation 47.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 66
% Syntax : Number of formulae : 402 ( 82 unt; 38 def)
% Number of atoms : 1103 ( 202 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 1169 ( 468 ~; 513 |; 128 &)
% ( 51 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 50 ( 48 usr; 30 prp; 0-4 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-3 aty)
% Number of variables : 403 ( 0 sgn 375 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( stoppedIn(X0,X1,X2)
<=> ? [X3,X4] :
( happens(X3,X4)
& less(X0,X4)
& less(X4,X2)
& terminates(X3,X1,X4) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',stoppedin_defn) ).
fof(f3,axiom,
! [X0,X1,X2,X3,X4] :
( ( happens(X0,X1)
& initiates(X0,X2,X1)
& less(n0,X4)
& trajectory(X2,X1,X3,X4)
& ~ stoppedIn(X1,X2,plus(X1,X4)) )
=> holdsAt(X3,plus(X1,X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',change_holding) ).
fof(f6,axiom,
! [X0,X1] :
( ( ~ holdsAt(X0,X1)
& ~ releasedAt(X0,plus(X1,n1))
& ~ ? [X2] :
( happens(X2,X1)
& initiates(X2,X0,X1) ) )
=> ~ holdsAt(X0,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',keep_not_holding) ).
fof(f8,axiom,
! [X0,X1] :
( ( ~ releasedAt(X0,X1)
& ~ ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) )
=> ~ releasedAt(X0,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',keep_not_released) ).
fof(f9,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& initiates(X0,X2,X1) )
=> holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_holds) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& terminates(X0,X2,X1) )
=> ~ holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_terminates_not_holds) ).
fof(f12,axiom,
! [X0,X1,X2] :
( ( happens(X0,X1)
& ( initiates(X0,X2,X1)
| terminates(X0,X2,X1) ) )
=> ~ releasedAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_not_released) ).
fof(f13,axiom,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ( X0 = tapOn
& X1 = filling )
| ( X0 = overflow
& X1 = spilling )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = tapOff
& X1 = waterLevel(X3) )
| ? [X3] :
( holdsAt(waterLevel(X3),X2)
& X0 = overflow
& X1 = waterLevel(X3) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',initiates_all_defn) ).
fof(f14,axiom,
! [X0,X1,X2] :
( terminates(X0,X1,X2)
<=> ( ( X0 = tapOff
& X1 = filling )
| ( X0 = overflow
& X1 = filling ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',terminates_all_defn) ).
fof(f15,axiom,
! [X0,X1,X2] :
( releases(X0,X1,X2)
<=> ? [X3] :
( X0 = tapOn
& X1 = waterLevel(X3) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',releases_all_defn) ).
fof(f16,axiom,
! [X0,X1] :
( happens(X0,X1)
<=> ( ( X0 = tapOn
& X1 = n0 )
| ( holdsAt(waterLevel(n3),X1)
& holdsAt(filling,X1)
& X0 = overflow ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',happens_all_defn) ).
fof(f17,axiom,
! [X0,X1,X2,X3] :
( ( holdsAt(waterLevel(X0),X1)
& X2 = plus(X0,X3) )
=> trajectory(filling,X1,waterLevel(X2),X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',change_of_waterLevel) ).
fof(f18,axiom,
! [X0,X1,X2] :
( ( holdsAt(waterLevel(X1),X0)
& holdsAt(waterLevel(X2),X0) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',same_waterLevel) ).
fof(f21,axiom,
overflow != tapOn,
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',overflow_not_tapOn) ).
fof(f27,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus0_1) ).
fof(f28,axiom,
plus(n0,n2) = n2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus0_2) ).
fof(f30,axiom,
plus(n1,n1) = n2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus1_1) ).
fof(f31,axiom,
plus(n1,n2) = n3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus1_2) ).
fof(f36,axiom,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_of_plus) ).
fof(f37,axiom,
! [X0,X1] :
( less_or_equal(X0,X1)
<=> ( less(X0,X1)
| X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_or_equal) ).
fof(f38,axiom,
~ ? [X0] : less(X0,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less0) ).
fof(f39,axiom,
! [X0] :
( less(X0,n1)
<=> less_or_equal(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less1) ).
fof(f40,axiom,
! [X0] :
( less(X0,n2)
<=> less_or_equal(X0,n1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less2) ).
fof(f41,axiom,
! [X0] :
( less(X0,n3)
<=> less_or_equal(X0,n2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less3) ).
fof(f48,axiom,
! [X0,X1] :
( less(X0,X1)
<=> ( ~ less(X1,X0)
& X1 != X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_property) ).
fof(f49,axiom,
holdsAt(waterLevel(n0),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',waterLevel_0) ).
fof(f50,axiom,
~ holdsAt(filling,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_filling_0) ).
fof(f55,conjecture,
~ stoppedIn(n0,filling,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_stopped_filling_0_3) ).
fof(f56,negated_conjecture,
~ ~ stoppedIn(n0,filling,n3),
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,
stoppedIn(n0,filling,n3),
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(f68,plain,
! [X0,X1] :
( ~ holdsAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ? [X2] :
( happens(X2,X1)
& initiates(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f6]) ).
fof(f69,plain,
! [X0,X1] :
( ~ holdsAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ? [X2] :
( happens(X2,X1)
& initiates(X2,X0,X1) ) ),
inference(flattening,[],[f68]) ).
fof(f72,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f73,plain,
! [X0,X1] :
( ~ releasedAt(X0,plus(X1,n1))
| releasedAt(X0,X1)
| ? [X2] :
( happens(X2,X1)
& releases(X2,X0,X1) ) ),
inference(flattening,[],[f72]) ).
fof(f74,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f75,plain,
! [X0,X1,X2] :
( holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(flattening,[],[f74]) ).
fof(f76,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(flattening,[],[f76]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ( ~ initiates(X0,X2,X1)
& ~ terminates(X0,X2,X1) ) ),
inference(flattening,[],[f80]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(ennf_transformation,[],[f17]) ).
fof(f83,plain,
! [X0,X1,X2,X3] :
( trajectory(filling,X1,waterLevel(X2),X3)
| ~ holdsAt(waterLevel(X0),X1)
| plus(X0,X3) != X2 ),
inference(flattening,[],[f82]) ).
fof(f84,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f85,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(waterLevel(X2),X0) ),
inference(flattening,[],[f84]) ).
fof(f86,plain,
! [X0] : ~ less(X0,n0),
inference(ennf_transformation,[],[f38]) ).
fof(f87,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(f104,plain,
! [X0,X1] :
( ~ holdsAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| ( happens(sK12(X0,X1),X1)
& initiates(sK12(X0,X1),X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f69]) ).
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(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(f155,plain,
! [X0,X1] :
( ~ holdsAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| happens(sK12(X0,X1),X1) ),
inference(cnf_transformation,[],[f104]) ).
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(f161,plain,
! [X2,X0,X1] :
( ~ holdsAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ terminates(X0,X2,X1) ),
inference(cnf_transformation,[],[f77]) ).
fof(f164,plain,
! [X2,X0,X1] :
( ~ releasedAt(X2,plus(X1,n1))
| ~ happens(X0,X1)
| ~ initiates(X0,X2,X1) ),
inference(cnf_transformation,[],[f81]) ).
fof(f170,plain,
! [X2,X0,X1] :
( sP4(X0,X1,X2)
| tapOn != X0
| filling != X1 ),
inference(cnf_transformation,[],[f108]) ).
fof(f183,plain,
! [X2,X0,X1] :
( ~ sP4(X0,X1,X2)
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f117]) ).
fof(f186,plain,
! [X0,X1] :
( sP6(X0,X1)
| ~ sP5(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f190,plain,
! [X0,X1] :
( sP5(X0,X1)
| overflow != X0
| filling != X1 ),
inference(cnf_transformation,[],[f121]) ).
fof(f192,plain,
! [X2,X0,X1] :
( ~ sP6(X0,X1)
| terminates(X0,X1,X2) ),
inference(cnf_transformation,[],[f122]) ).
fof(f194,plain,
! [X2,X0,X1] :
( ~ releases(X0,X1,X2)
| tapOn = X0 ),
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(f210,plain,
tapOn != overflow,
inference(cnf_transformation,[],[f21]) ).
fof(f217,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f27]) ).
fof(f218,plain,
n2 = plus(n0,n2),
inference(cnf_transformation,[],[f28]) ).
fof(f220,plain,
n2 = plus(n1,n1),
inference(cnf_transformation,[],[f30]) ).
fof(f221,plain,
n3 = plus(n1,n2),
inference(cnf_transformation,[],[f31]) ).
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(f253,plain,
~ holdsAt(filling,n0),
inference(cnf_transformation,[],[f50]) ).
fof(f258,plain,
stoppedIn(n0,filling,n3),
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(f269,plain,
! [X1] :
( sP5(overflow,X1)
| filling != X1 ),
inference(equality_resolution,[],[f190]) ).
fof(f270,plain,
sP5(overflow,filling),
inference(equality_resolution,[],[f269]) ).
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(f294,plain,
sP0(n0,n3,filling),
inference(resolution,[],[f150,f258]) ).
fof(f298,plain,
! [X0] : initiates(tapOn,filling,X0),
inference(resolution,[],[f183,f260]) ).
fof(f303,plain,
less(n1,n2),
inference(resolution,[],[f234,f278]) ).
fof(f304,plain,
! [X0] :
( ~ less(X0,n1)
| less(X0,n2) ),
inference(resolution,[],[f234,f229]) ).
fof(f305,plain,
! [X0] :
( holdsAt(X0,plus(n0,n1))
| ~ initiates(tapOn,X0,n0) ),
inference(resolution,[],[f160,f284]) ).
fof(f306,plain,
! [X0] :
( holdsAt(X0,plus(n1,n0))
| ~ initiates(tapOn,X0,n0) ),
inference(forward_demodulation,[],[f305,f226]) ).
fof(f307,plain,
! [X0] :
( ~ initiates(tapOn,X0,n0)
| holdsAt(X0,n1) ),
inference(forward_demodulation,[],[f306,f281]) ).
fof(f320,plain,
! [X0] :
( ~ releasedAt(X0,n2)
| releasedAt(X0,n1)
| happens(sK14(X0,n1),n1) ),
inference(superposition,[],[f159,f220]) ).
fof(f321,plain,
! [X0] :
( ~ releasedAt(X0,n2)
| releasedAt(X0,n1)
| releases(sK14(X0,n1),X0,n1) ),
inference(superposition,[],[f158,f220]) ).
fof(f423,plain,
~ less(n2,n1),
inference(resolution,[],[f250,f303]) ).
fof(f425,plain,
~ less(n3,n2),
inference(resolution,[],[f250,f289]) ).
fof(f439,plain,
! [X0,X1] :
( ~ holdsAt(X1,plus(n1,X0))
| holdsAt(X1,X0)
| releasedAt(X1,plus(n1,X0))
| happens(sK12(X1,X0),X0) ),
inference(superposition,[],[f155,f226]) ).
fof(f441,plain,
! [X0,X1] :
( ~ releasedAt(X1,plus(n1,X0))
| releasedAt(X1,X0)
| happens(sK14(X1,X0),X0) ),
inference(superposition,[],[f159,f226]) ).
fof(f442,plain,
! [X2,X0,X1] :
( ~ terminates(X2,X1,X0)
| ~ happens(X2,X0)
| ~ holdsAt(X1,plus(n1,X0)) ),
inference(superposition,[],[f161,f226]) ).
fof(f444,plain,
! [X2,X0,X1] :
( ~ initiates(X2,X1,X0)
| ~ happens(X2,X0)
| ~ releasedAt(X1,plus(n1,X0)) ),
inference(superposition,[],[f164,f226]) ).
fof(f447,plain,
! [X0] :
( n0 = X0
| less(X0,n0)
| ~ less(X0,n1) ),
inference(resolution,[],[f227,f231]) ).
fof(f448,plain,
! [X0] :
( ~ less(X0,n2)
| less(X0,n1)
| n1 = X0 ),
inference(resolution,[],[f227,f233]) ).
fof(f450,plain,
! [X0] :
( less(X0,n2)
| n2 = X0
| ~ less(X0,n3) ),
inference(resolution,[],[f227,f235]) ).
fof(f454,plain,
! [X0] :
( ~ less(X0,n1)
| n0 = X0 ),
inference(global_subsumption,[],[f447,f230]) ).
fof(f471,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(n0,X0)),X0),
inference(resolution,[],[f276,f252]) ).
fof(f491,plain,
less(n0,n2),
inference(resolution,[],[f304,f287]) ).
fof(f571,plain,
! [X0,X1] :
( ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,X1)
| holdsAt(waterLevel(plus(n0,X1)),plus(n0,X1))
| stoppedIn(n0,filling,plus(n0,X1)) ),
inference(resolution,[],[f471,f151]) ).
fof(f576,plain,
! [X0] : trajectory(filling,n0,waterLevel(plus(X0,n0)),X0),
inference(superposition,[],[f471,f226]) ).
fof(f578,definition,
( spl18_23
<=> ! [X1] :
( ~ less(n0,X1)
| stoppedIn(n0,filling,plus(n0,X1))
| holdsAt(waterLevel(plus(n0,X1)),plus(n0,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl18_23])],[avatar_definition]) ).
fof(f579,plain,
( ! [X1] :
( holdsAt(waterLevel(plus(n0,X1)),plus(n0,X1))
| stoppedIn(n0,filling,plus(n0,X1))
| ~ less(n0,X1) )
| ~ spl18_23 ),
inference(avatar_component_clause,[],[f578]) ).
fof(f581,definition,
( spl18_24
<=> ! [X0] :
( ~ happens(X0,n0)
| ~ initiates(X0,filling,n0) ) ),
introduced(definition,[new_symbols(definition,[spl18_24])],[avatar_definition]) ).
fof(f582,plain,
( ! [X0] :
( ~ initiates(X0,filling,n0)
| ~ happens(X0,n0) )
| ~ spl18_24 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f583,plain,
( spl18_23
| spl18_24 ),
inference(avatar_split_clause,[],[f571,f581,f578]) ).
fof(f931,plain,
! [X0] :
( ~ happens(tapOn,X0)
| ~ releasedAt(filling,plus(n1,X0)) ),
inference(resolution,[],[f444,f298]) ).
fof(f936,plain,
! [X0] :
( ~ releasedAt(X0,n3)
| releasedAt(X0,n2)
| happens(sK14(X0,n2),n2) ),
inference(superposition,[],[f441,f221]) ).
fof(f968,definition,
( spl18_44
<=> stoppedIn(n0,filling,n2) ),
introduced(definition,[new_symbols(definition,[spl18_44])],[avatar_definition]) ).
fof(f970,plain,
( stoppedIn(n0,filling,n2)
| ~ spl18_44 ),
inference(avatar_component_clause,[],[f968]) ).
fof(f975,plain,
! [X0] :
( ~ holdsAt(X0,n3)
| holdsAt(X0,n2)
| releasedAt(X0,n3)
| happens(sK12(X0,n2),n2) ),
inference(superposition,[],[f439,f221]) ).
fof(f978,plain,
( sP0(n0,n2,filling)
| ~ spl18_44 ),
inference(resolution,[],[f970,f150]) ).
fof(f1096,plain,
! [X0,X1] :
( ~ happens(X0,n0)
| ~ initiates(X0,filling,n0)
| ~ less(n0,X1)
| holdsAt(waterLevel(plus(X1,n0)),plus(n0,X1))
| stoppedIn(n0,filling,plus(n0,X1)) ),
inference(resolution,[],[f576,f151]) ).
fof(f1102,definition,
( spl18_55
<=> ! [X1] :
( ~ less(n0,X1)
| stoppedIn(n0,filling,plus(n0,X1))
| holdsAt(waterLevel(plus(X1,n0)),plus(n0,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl18_55])],[avatar_definition]) ).
fof(f1103,plain,
( ! [X1] :
( holdsAt(waterLevel(plus(X1,n0)),plus(n0,X1))
| stoppedIn(n0,filling,plus(n0,X1))
| ~ less(n0,X1) )
| ~ spl18_55 ),
inference(avatar_component_clause,[],[f1102]) ).
fof(f1104,plain,
( spl18_55
| spl18_24 ),
inference(avatar_split_clause,[],[f1096,f581,f1102]) ).
fof(f1261,definition,
( spl18_73
<=> n0 = n2 ),
introduced(definition,[new_symbols(definition,[spl18_73])],[avatar_definition]) ).
fof(f1263,plain,
( n0 = n2
| ~ spl18_73 ),
inference(avatar_component_clause,[],[f1261]) ).
fof(f1423,plain,
( ~ less(n0,n1)
| ~ spl18_73 ),
inference(superposition,[],[f423,f1263]) ).
fof(f1472,plain,
( $false
| ~ spl18_73 ),
inference(global_subsumption,[],[f1423,f287]) ).
fof(f1473,plain,
~ spl18_73,
inference(avatar_contradiction_clause,[],[f1472]) ).
fof(f1497,definition,
( spl18_79
<=> n0 = n1 ),
introduced(definition,[new_symbols(definition,[spl18_79])],[avatar_definition]) ).
fof(f1499,plain,
( n0 = n1
| ~ spl18_79 ),
inference(avatar_component_clause,[],[f1497]) ).
fof(f1550,plain,
( ~ holdsAt(filling,n1)
| ~ spl18_79 ),
inference(superposition,[],[f253,f1499]) ).
fof(f2049,plain,
( ! [X0] :
( holdsAt(waterLevel(plus(X0,n0)),plus(X0,n0))
| stoppedIn(n0,filling,plus(X0,n0))
| ~ less(n0,X0) )
| ~ spl18_23 ),
inference(superposition,[],[f579,f226]) ).
fof(f2072,definition,
( spl18_97
<=> stoppedIn(n0,filling,n1) ),
introduced(definition,[new_symbols(definition,[spl18_97])],[avatar_definition]) ).
fof(f2074,plain,
( stoppedIn(n0,filling,n1)
| ~ spl18_97 ),
inference(avatar_component_clause,[],[f2072]) ).
fof(f2107,plain,
( ~ happens(tapOn,n0)
| ~ spl18_24 ),
inference(resolution,[],[f582,f298]) ).
fof(f2108,plain,
( $false
| ~ spl18_24 ),
inference(global_subsumption,[],[f2107,f284]) ).
fof(f2109,plain,
~ spl18_24,
inference(avatar_contradiction_clause,[],[f2108]) ).
fof(f2263,plain,
( sP0(n0,n1,filling)
| ~ spl18_97 ),
inference(resolution,[],[f2074,f150]) ).
fof(f2506,plain,
! [X2,X0,X1] :
( ~ sP5(X0,X1)
| terminates(X0,X1,X2) ),
inference(resolution,[],[f186,f192]) ).
fof(f2706,plain,
! [X0] :
( ~ less(X0,n2)
| n0 = X0
| n1 = X0 ),
inference(global_subsumption,[],[f454,f448]) ).
fof(f2808,plain,
! [X0] : terminates(overflow,filling,X0),
inference(resolution,[],[f2506,f270]) ).
fof(f2836,plain,
! [X0] :
( ~ happens(overflow,X0)
| ~ holdsAt(filling,plus(n1,X0)) ),
inference(resolution,[],[f2808,f442]) ).
fof(f2916,plain,
holdsAt(filling,n1),
inference(resolution,[],[f307,f298]) ).
fof(f2980,definition,
( spl18_122
<=> releasedAt(filling,n1) ),
introduced(definition,[new_symbols(definition,[spl18_122])],[avatar_definition]) ).
fof(f2994,definition,
( spl18_125
<=> holdsAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl18_125])],[avatar_definition]) ).
fof(f2998,definition,
( spl18_126
<=> releasedAt(filling,n2) ),
introduced(definition,[new_symbols(definition,[spl18_126])],[avatar_definition]) ).
fof(f3000,plain,
( releasedAt(filling,n2)
| ~ spl18_126 ),
inference(avatar_component_clause,[],[f2998]) ).
fof(f3122,plain,
( ! [X0,X1] :
( ~ holdsAt(waterLevel(X1),plus(n0,X0))
| ~ less(n0,X0)
| stoppedIn(n0,filling,plus(n0,X0))
| plus(X0,n0) = X1 )
| ~ spl18_55 ),
inference(resolution,[],[f1103,f207]) ).
fof(f3221,plain,
( ! [X0,X1] :
( ~ holdsAt(waterLevel(X1),plus(X0,n0))
| ~ less(n0,X0)
| stoppedIn(n0,filling,plus(X0,n0))
| plus(X0,n0) = X1 )
| ~ spl18_23 ),
inference(resolution,[],[f2049,f207]) ).
fof(f3646,plain,
~ releasedAt(filling,plus(n1,n0)),
inference(resolution,[],[f931,f284]) ).
fof(f3647,plain,
~ releasedAt(filling,n1),
inference(forward_demodulation,[],[f3646,f281]) ).
fof(f3649,plain,
! [X0] :
( ~ less(X0,n3)
| n1 = X0
| n2 = X0
| n0 = X0 ),
inference(resolution,[],[f2706,f450]) ).
fof(f5910,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n2)
| ~ less(n0,n2)
| stoppedIn(n0,filling,n2)
| plus(n2,n0) = X0 )
| ~ spl18_55 ),
inference(superposition,[],[f3122,f218]) ).
fof(f5972,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n1)
| ~ less(n0,n1)
| stoppedIn(n0,filling,n1)
| n1 = X0 )
| ~ spl18_23 ),
inference(superposition,[],[f3221,f281]) ).
fof(f8773,definition,
( spl18_200
<=> holdsAt(filling,n3) ),
introduced(definition,[new_symbols(definition,[spl18_200])],[avatar_definition]) ).
fof(f8775,plain,
( holdsAt(filling,n3)
| ~ spl18_200 ),
inference(avatar_component_clause,[],[f8773]) ).
fof(f8777,definition,
( spl18_201
<=> releasedAt(filling,n3) ),
introduced(definition,[new_symbols(definition,[spl18_201])],[avatar_definition]) ).
fof(f8779,plain,
( releasedAt(filling,n3)
| ~ spl18_201 ),
inference(avatar_component_clause,[],[f8777]) ).
fof(f9748,plain,
( releasedAt(filling,n2)
| happens(sK14(filling,n2),n2)
| ~ spl18_201 ),
inference(resolution,[],[f8779,f936]) ).
fof(f9754,definition,
( spl18_209
<=> happens(sK14(filling,n2),n2) ),
introduced(definition,[new_symbols(definition,[spl18_209])],[avatar_definition]) ).
fof(f9756,plain,
( happens(sK14(filling,n2),n2)
| ~ spl18_209 ),
inference(avatar_component_clause,[],[f9754]) ).
fof(f9757,plain,
( spl18_209
| spl18_126
| ~ spl18_201 ),
inference(avatar_split_clause,[],[f9748,f8777,f2998,f9754]) ).
fof(f9785,plain,
( releasedAt(filling,n1)
| releases(sK14(filling,n1),filling,n1)
| ~ spl18_126 ),
inference(resolution,[],[f3000,f321]) ).
fof(f9786,plain,
( releasedAt(filling,n1)
| happens(sK14(filling,n1),n1)
| ~ spl18_126 ),
inference(resolution,[],[f3000,f320]) ).
fof(f9795,definition,
( spl18_214
<=> happens(sK14(filling,n1),n1) ),
introduced(definition,[new_symbols(definition,[spl18_214])],[avatar_definition]) ).
fof(f9797,plain,
( happens(sK14(filling,n1),n1)
| ~ spl18_214 ),
inference(avatar_component_clause,[],[f9795]) ).
fof(f9798,plain,
( spl18_214
| spl18_122
| ~ spl18_126 ),
inference(avatar_split_clause,[],[f9786,f2998,f2980,f9795]) ).
fof(f9800,definition,
( spl18_215
<=> releases(sK14(filling,n1),filling,n1) ),
introduced(definition,[new_symbols(definition,[spl18_215])],[avatar_definition]) ).
fof(f9802,plain,
( releases(sK14(filling,n1),filling,n1)
| ~ spl18_215 ),
inference(avatar_component_clause,[],[f9800]) ).
fof(f9803,plain,
( spl18_215
| spl18_122
| ~ spl18_126 ),
inference(avatar_split_clause,[],[f9785,f2998,f2980,f9800]) ).
fof(f9839,plain,
( holdsAt(filling,n2)
| releasedAt(filling,n3)
| happens(sK12(filling,n2),n2)
| ~ spl18_200 ),
inference(resolution,[],[f8775,f975]) ).
fof(f11873,plain,
! [X0,X1] :
( sP7(X0,X1)
| n0 = X0
| ~ happens(X1,X0) ),
inference(resolution,[],[f196,f204]) ).
fof(f12263,plain,
! [X0,X1] :
( ~ happens(X1,X0)
| n0 = X0
| holdsAt(waterLevel(n3),X0) ),
inference(resolution,[],[f11873,f202]) ).
fof(f12264,plain,
! [X0,X1] :
( ~ happens(X1,X0)
| n0 = X0
| holdsAt(filling,X0) ),
inference(resolution,[],[f11873,f201]) ).
fof(f12265,plain,
! [X0,X1] :
( ~ happens(X1,X0)
| n0 = X0
| overflow = X1 ),
inference(resolution,[],[f11873,f200]) ).
fof(f14026,definition,
( spl18_253
<=> n0 = n3 ),
introduced(definition,[new_symbols(definition,[spl18_253])],[avatar_definition]) ).
fof(f14028,plain,
( n0 = n3
| ~ spl18_253 ),
inference(avatar_component_clause,[],[f14026]) ).
fof(f14070,plain,
( ~ less(n0,n2)
| ~ spl18_253 ),
inference(superposition,[],[f425,f14028]) ).
fof(f14208,plain,
( $false
| ~ spl18_253 ),
inference(global_subsumption,[],[f14070,f491]) ).
fof(f14209,plain,
~ spl18_253,
inference(avatar_contradiction_clause,[],[f14208]) ).
fof(f17565,definition,
( spl18_277
<=> happens(sK12(filling,n2),n2) ),
introduced(definition,[new_symbols(definition,[spl18_277])],[avatar_definition]) ).
fof(f17567,plain,
( happens(sK12(filling,n2),n2)
| ~ spl18_277 ),
inference(avatar_component_clause,[],[f17565]) ).
fof(f17568,plain,
( spl18_277
| spl18_201
| spl18_125
| ~ spl18_200 ),
inference(avatar_split_clause,[],[f9839,f8773,f2994,f8777,f17565]) ).
fof(f18335,plain,
~ spl18_122,
inference(avatar_split_clause,[],[f3647,f2980]) ).
fof(f18596,plain,
( n0 = n1
| overflow = sK14(filling,n1)
| ~ spl18_214 ),
inference(resolution,[],[f9797,f12265]) ).
fof(f18603,definition,
( spl18_286
<=> overflow = sK14(filling,n1) ),
introduced(definition,[new_symbols(definition,[spl18_286])],[avatar_definition]) ).
fof(f18605,plain,
( overflow = sK14(filling,n1)
| ~ spl18_286 ),
inference(avatar_component_clause,[],[f18603]) ).
fof(f18606,plain,
( spl18_286
| spl18_79
| ~ spl18_214 ),
inference(avatar_split_clause,[],[f18596,f9795,f1497,f18603]) ).
fof(f19478,plain,
( n0 = n2
| holdsAt(filling,n2)
| ~ spl18_209 ),
inference(resolution,[],[f9756,f12264]) ).
fof(f19483,plain,
( spl18_125
| spl18_73
| ~ spl18_209 ),
inference(avatar_split_clause,[],[f19478,f9754,f1261,f2994]) ).
fof(f19520,plain,
( n0 = n2
| holdsAt(filling,n2)
| ~ spl18_277 ),
inference(resolution,[],[f17567,f12264]) ).
fof(f19525,plain,
( spl18_125
| spl18_73
| ~ spl18_277 ),
inference(avatar_split_clause,[],[f19520,f17565,f1261,f2994]) ).
fof(f22498,plain,
( tapOn = sK14(filling,n1)
| ~ spl18_215 ),
inference(resolution,[],[f9802,f194]) ).
fof(f22500,plain,
( tapOn = overflow
| ~ spl18_215
| ~ spl18_286 ),
inference(forward_demodulation,[],[f22498,f18605]) ).
fof(f22504,plain,
( $false
| ~ spl18_215
| ~ spl18_286 ),
inference(global_subsumption,[],[f22500,f210]) ).
fof(f22505,plain,
( ~ spl18_215
| ~ spl18_286 ),
inference(avatar_contradiction_clause,[],[f22504]) ).
fof(f24766,plain,
less(sK10(n0,n3,filling),n3),
inference(resolution,[],[f147,f294]) ).
fof(f24767,plain,
( less(sK10(n0,n2,filling),n2)
| ~ spl18_44 ),
inference(resolution,[],[f147,f978]) ).
fof(f24768,plain,
( less(sK10(n0,n1,filling),n1)
| ~ spl18_97 ),
inference(resolution,[],[f147,f2263]) ).
fof(f24782,plain,
( n1 = sK10(n0,n3,filling)
| n2 = sK10(n0,n3,filling)
| n0 = sK10(n0,n3,filling) ),
inference(resolution,[],[f24766,f3649]) ).
fof(f24786,definition,
( spl18_533
<=> n2 = sK10(n0,n3,filling) ),
introduced(definition,[new_symbols(definition,[spl18_533])],[avatar_definition]) ).
fof(f24788,plain,
( n2 = sK10(n0,n3,filling)
| ~ spl18_533 ),
inference(avatar_component_clause,[],[f24786]) ).
fof(f24790,definition,
( spl18_534
<=> n1 = sK10(n0,n3,filling) ),
introduced(definition,[new_symbols(definition,[spl18_534])],[avatar_definition]) ).
fof(f24792,plain,
( n1 = sK10(n0,n3,filling)
| ~ spl18_534 ),
inference(avatar_component_clause,[],[f24790]) ).
fof(f24799,definition,
( spl18_536
<=> n0 = sK10(n0,n3,filling) ),
introduced(definition,[new_symbols(definition,[spl18_536])],[avatar_definition]) ).
fof(f24801,plain,
( n0 = sK10(n0,n3,filling)
| ~ spl18_536 ),
inference(avatar_component_clause,[],[f24799]) ).
fof(f24802,plain,
( spl18_536
| spl18_533
| spl18_534 ),
inference(avatar_split_clause,[],[f24782,f24790,f24786,f24799]) ).
fof(f24859,plain,
( n0 = sK10(n0,n2,filling)
| n1 = sK10(n0,n2,filling)
| ~ spl18_44 ),
inference(resolution,[],[f24767,f2706]) ).
fof(f24867,definition,
( spl18_539
<=> n1 = sK10(n0,n2,filling) ),
introduced(definition,[new_symbols(definition,[spl18_539])],[avatar_definition]) ).
fof(f24869,plain,
( n1 = sK10(n0,n2,filling)
| ~ spl18_539 ),
inference(avatar_component_clause,[],[f24867]) ).
fof(f24880,definition,
( spl18_542
<=> n0 = sK10(n0,n2,filling) ),
introduced(definition,[new_symbols(definition,[spl18_542])],[avatar_definition]) ).
fof(f24882,plain,
( n0 = sK10(n0,n2,filling)
| ~ spl18_542 ),
inference(avatar_component_clause,[],[f24880]) ).
fof(f24883,plain,
( spl18_539
| spl18_542
| ~ spl18_44 ),
inference(avatar_split_clause,[],[f24859,f968,f24880,f24867]) ).
fof(f24894,plain,
( ! [X0] :
( plus(n0,n2) = X0
| ~ holdsAt(waterLevel(X0),n2)
| ~ less(n0,n2)
| stoppedIn(n0,filling,n2) )
| ~ spl18_55 ),
inference(forward_demodulation,[],[f5910,f226]) ).
fof(f24924,definition,
( spl18_544
<=> ! [X0] :
( ~ holdsAt(waterLevel(X0),n2)
| n2 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl18_544])],[avatar_definition]) ).
fof(f24925,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n2)
| n2 = X0 )
| ~ spl18_544 ),
inference(avatar_component_clause,[],[f24924]) ).
fof(f24933,plain,
( ! [X0] :
( n2 = X0
| ~ holdsAt(waterLevel(X0),n2)
| ~ less(n0,n2)
| stoppedIn(n0,filling,n2) )
| ~ spl18_55 ),
inference(forward_demodulation,[],[f24894,f218]) ).
fof(f24974,plain,
( ! [X0] :
( n2 = X0
| ~ holdsAt(waterLevel(X0),n2)
| stoppedIn(n0,filling,n2) )
| ~ spl18_55 ),
inference(global_subsumption,[],[f24933,f491]) ).
fof(f25008,plain,
( spl18_44
| spl18_544
| ~ spl18_55 ),
inference(avatar_split_clause,[],[f24974,f1102,f24924,f968]) ).
fof(f25371,plain,
( n0 = sK10(n0,n1,filling)
| ~ spl18_97 ),
inference(resolution,[],[f24768,f454]) ).
fof(f26020,plain,
less(n0,sK10(n0,n3,filling)),
inference(resolution,[],[f148,f294]) ).
fof(f26021,plain,
( less(n0,sK10(n0,n1,filling))
| ~ spl18_97 ),
inference(resolution,[],[f148,f2263]) ).
fof(f26022,plain,
( less(n0,sK10(n0,n2,filling))
| ~ spl18_44 ),
inference(resolution,[],[f148,f978]) ).
fof(f26033,plain,
( less(n0,n0)
| ~ spl18_97 ),
inference(forward_demodulation,[],[f26021,f25371]) ).
fof(f26036,plain,
( $false
| ~ spl18_97 ),
inference(resolution,[],[f26033,f230]) ).
fof(f26040,plain,
~ spl18_97,
inference(avatar_contradiction_clause,[],[f26036]) ).
fof(f26052,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n1)
| stoppedIn(n0,filling,n1)
| n1 = X0 )
| ~ spl18_23 ),
inference(global_subsumption,[],[f5972,f287]) ).
fof(f26101,definition,
( spl18_621
<=> ! [X0] :
( ~ holdsAt(waterLevel(X0),n1)
| n1 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl18_621])],[avatar_definition]) ).
fof(f26102,plain,
( ! [X0] :
( ~ holdsAt(waterLevel(X0),n1)
| n1 = X0 )
| ~ spl18_621 ),
inference(avatar_component_clause,[],[f26101]) ).
fof(f26103,plain,
( spl18_97
| spl18_621
| ~ spl18_23 ),
inference(avatar_split_clause,[],[f26052,f578,f26101,f2072]) ).
fof(f27238,definition,
( spl18_699
<=> holdsAt(waterLevel(n3),n1) ),
introduced(definition,[new_symbols(definition,[spl18_699])],[avatar_definition]) ).
fof(f27240,plain,
( holdsAt(waterLevel(n3),n1)
| ~ spl18_699 ),
inference(avatar_component_clause,[],[f27238]) ).
fof(f27310,plain,
( n1 = n3
| ~ spl18_621
| ~ spl18_699 ),
inference(resolution,[],[f27240,f26102]) ).
fof(f27339,plain,
( less(n2,n1)
| ~ spl18_621
| ~ spl18_699 ),
inference(superposition,[],[f289,f27310]) ).
fof(f27530,plain,
( $false
| ~ spl18_621
| ~ spl18_699 ),
inference(global_subsumption,[],[f27339,f423]) ).
fof(f27531,plain,
( ~ spl18_621
| ~ spl18_699 ),
inference(avatar_contradiction_clause,[],[f27530]) ).
fof(f27598,definition,
( spl18_713
<=> holdsAt(waterLevel(n3),n2) ),
introduced(definition,[new_symbols(definition,[spl18_713])],[avatar_definition]) ).
fof(f27600,plain,
( holdsAt(waterLevel(n3),n2)
| ~ spl18_713 ),
inference(avatar_component_clause,[],[f27598]) ).
fof(f27611,plain,
( n3 = n2
| ~ spl18_544
| ~ spl18_713 ),
inference(resolution,[],[f27600,f24925]) ).
fof(f27615,plain,
( sP7(n2,overflow)
| ~ holdsAt(filling,n2)
| ~ spl18_713 ),
inference(resolution,[],[f27600,f275]) ).
fof(f27627,definition,
( spl18_714
<=> sP7(n2,overflow) ),
introduced(definition,[new_symbols(definition,[spl18_714])],[avatar_definition]) ).
fof(f27629,plain,
( sP7(n2,overflow)
| ~ spl18_714 ),
inference(avatar_component_clause,[],[f27627]) ).
fof(f27630,plain,
( ~ spl18_125
| spl18_714
| ~ spl18_713 ),
inference(avatar_split_clause,[],[f27615,f27598,f27627,f2994]) ).
fof(f27940,plain,
( sP8(overflow,n2)
| ~ spl18_714 ),
inference(resolution,[],[f27629,f198]) ).
fof(f29030,definition,
( spl18_777
<=> n3 = n2 ),
introduced(definition,[new_symbols(definition,[spl18_777])],[avatar_definition]) ).
fof(f29032,plain,
( n3 = n2
| ~ spl18_777 ),
inference(avatar_component_clause,[],[f29030]) ).
fof(f30061,plain,
( happens(overflow,n2)
| ~ spl18_714 ),
inference(resolution,[],[f27940,f205]) ).
fof(f30078,plain,
( ~ holdsAt(filling,plus(n1,n2))
| ~ spl18_714 ),
inference(resolution,[],[f30061,f2836]) ).
fof(f30103,plain,
( ~ holdsAt(filling,n3)
| ~ spl18_714 ),
inference(forward_demodulation,[],[f30078,f221]) ).
fof(f31900,plain,
happens(sK9(n0,n3,filling),sK10(n0,n3,filling)),
inference(resolution,[],[f149,f294]) ).
fof(f31901,plain,
( happens(sK9(n0,n2,filling),sK10(n0,n2,filling))
| ~ spl18_44 ),
inference(resolution,[],[f149,f978]) ).
fof(f31909,plain,
( happens(sK9(n0,n2,filling),n1)
| ~ spl18_44
| ~ spl18_539 ),
inference(forward_demodulation,[],[f31901,f24869]) ).
fof(f31910,plain,
( happens(sK9(n0,n3,filling),n1)
| ~ spl18_534 ),
inference(forward_demodulation,[],[f31900,f24792]) ).
fof(f31919,plain,
( n0 = n1
| holdsAt(waterLevel(n3),n1)
| ~ spl18_534 ),
inference(resolution,[],[f31910,f12263]) ).
fof(f31936,plain,
( spl18_699
| spl18_79
| ~ spl18_534 ),
inference(avatar_split_clause,[],[f31919,f24790,f1497,f27238]) ).
fof(f31942,plain,
( happens(sK9(n0,n3,filling),n2)
| ~ spl18_533 ),
inference(forward_demodulation,[],[f31900,f24788]) ).
fof(f31999,plain,
( n0 = n2
| holdsAt(waterLevel(n3),n2)
| ~ spl18_533 ),
inference(resolution,[],[f31942,f12263]) ).
fof(f32000,plain,
( n0 = n2
| holdsAt(filling,n2)
| ~ spl18_533 ),
inference(resolution,[],[f31942,f12264]) ).
fof(f32008,plain,
( spl18_713
| spl18_73
| ~ spl18_533 ),
inference(avatar_split_clause,[],[f31999,f24786,f1261,f27598]) ).
fof(f32019,plain,
( less(n0,n0)
| ~ spl18_536 ),
inference(forward_demodulation,[],[f26020,f24801]) ).
fof(f32036,plain,
( $false
| ~ spl18_536 ),
inference(resolution,[],[f32019,f230]) ).
fof(f32040,plain,
~ spl18_536,
inference(avatar_contradiction_clause,[],[f32036]) ).
fof(f32061,plain,
( $false
| ~ spl18_79 ),
inference(global_subsumption,[],[f1550,f2916]) ).
fof(f32062,plain,
~ spl18_79,
inference(avatar_contradiction_clause,[],[f32061]) ).
fof(f32228,plain,
( holdsAt(filling,n2)
| ~ spl18_714 ),
inference(resolution,[],[f27629,f201]) ).
fof(f32723,plain,
( n0 = n1
| holdsAt(waterLevel(n3),n1)
| ~ spl18_44
| ~ spl18_539 ),
inference(resolution,[],[f31909,f12263]) ).
fof(f32740,plain,
( spl18_699
| spl18_79
| ~ spl18_44
| ~ spl18_539 ),
inference(avatar_split_clause,[],[f32723,f24867,f968,f1497,f27238]) ).
fof(f32747,plain,
( less(n0,n0)
| ~ spl18_44
| ~ spl18_542 ),
inference(forward_demodulation,[],[f26022,f24882]) ).
fof(f32776,plain,
( $false
| ~ spl18_44
| ~ spl18_542 ),
inference(resolution,[],[f32747,f230]) ).
fof(f32780,plain,
( ~ spl18_44
| ~ spl18_542 ),
inference(avatar_contradiction_clause,[],[f32776]) ).
fof(f32782,plain,
( spl18_777
| ~ spl18_544
| ~ spl18_713 ),
inference(avatar_split_clause,[],[f27611,f27598,f24924,f29030]) ).
fof(f32811,plain,
( n0 = n3
| holdsAt(filling,n2)
| ~ spl18_533
| ~ spl18_777 ),
inference(forward_demodulation,[],[f32000,f29032]) ).
fof(f32814,plain,
( holdsAt(filling,n3)
| ~ spl18_714
| ~ spl18_777 ),
inference(forward_demodulation,[],[f32228,f29032]) ).
fof(f32831,plain,
( holdsAt(filling,n3)
| n0 = n3
| ~ spl18_533
| ~ spl18_777 ),
inference(forward_demodulation,[],[f32811,f29032]) ).
fof(f32836,plain,
( $false
| ~ spl18_714
| ~ spl18_777 ),
inference(global_subsumption,[],[f32814,f30103]) ).
fof(f32837,plain,
( ~ spl18_714
| ~ spl18_777 ),
inference(avatar_contradiction_clause,[],[f32836]) ).
fof(f32850,plain,
( spl18_253
| spl18_200
| ~ spl18_533
| ~ spl18_777 ),
inference(avatar_split_clause,[],[f32831,f29030,f24786,f8773,f14026]) ).
cnf(s238,plain,
( spl18_23
| spl18_24 ),
inference(sat_conversion,[],[f583]) ).
cnf(s464,plain,
( spl18_24
| spl18_55 ),
inference(sat_conversion,[],[f1104]) ).
cnf(s600,plain,
~ spl18_73,
inference(sat_conversion,[],[f1473]) ).
cnf(s854,plain,
~ spl18_24,
inference(sat_conversion,[],[f2109]) ).
cnf(s1551,plain,
( spl18_126
| ~ spl18_201
| spl18_209 ),
inference(sat_conversion,[],[f9757]) ).
cnf(s1565,plain,
( spl18_122
| ~ spl18_126
| spl18_214 ),
inference(sat_conversion,[],[f9798]) ).
cnf(s1567,plain,
( spl18_122
| ~ spl18_126
| spl18_215 ),
inference(sat_conversion,[],[f9803]) ).
cnf(s1849,plain,
~ spl18_253,
inference(sat_conversion,[],[f14209]) ).
cnf(s2104,plain,
( spl18_125
| ~ spl18_200
| spl18_201
| spl18_277 ),
inference(sat_conversion,[],[f17568]) ).
cnf(s2141,plain,
~ spl18_122,
inference(sat_conversion,[],[f18335]) ).
cnf(s2155,plain,
( spl18_79
| ~ spl18_214
| spl18_286 ),
inference(sat_conversion,[],[f18606]) ).
cnf(s2179,plain,
( spl18_73
| spl18_125
| ~ spl18_209 ),
inference(sat_conversion,[],[f19483]) ).
cnf(s2191,plain,
( spl18_73
| spl18_125
| ~ spl18_277 ),
inference(sat_conversion,[],[f19525]) ).
cnf(s2675,plain,
( ~ spl18_215
| ~ spl18_286 ),
inference(sat_conversion,[],[f22505]) ).
cnf(s3549,plain,
( spl18_533
| spl18_534
| spl18_536 ),
inference(sat_conversion,[],[f24802]) ).
cnf(s3568,plain,
( ~ spl18_44
| spl18_539
| spl18_542 ),
inference(sat_conversion,[],[f24883]) ).
cnf(s3613,plain,
( spl18_44
| ~ spl18_55
| spl18_544 ),
inference(sat_conversion,[],[f25008]) ).
cnf(s4014,plain,
~ spl18_97,
inference(sat_conversion,[],[f26040]) ).
cnf(s4034,plain,
( ~ spl18_23
| spl18_97
| spl18_621 ),
inference(sat_conversion,[],[f26103]) ).
cnf(s4636,plain,
( ~ spl18_621
| ~ spl18_699 ),
inference(sat_conversion,[],[f27531]) ).
cnf(s4677,plain,
( ~ spl18_125
| ~ spl18_713
| spl18_714 ),
inference(sat_conversion,[],[f27630]) ).
cnf(s6083,plain,
( spl18_79
| ~ spl18_534
| spl18_699 ),
inference(sat_conversion,[],[f31936]) ).
cnf(s6119,plain,
( spl18_73
| ~ spl18_533
| spl18_713 ),
inference(sat_conversion,[],[f32008]) ).
cnf(s6133,plain,
~ spl18_536,
inference(sat_conversion,[],[f32040]) ).
cnf(s6156,plain,
~ spl18_79,
inference(sat_conversion,[],[f32062]) ).
cnf(s6463,plain,
( ~ spl18_44
| spl18_79
| ~ spl18_539
| spl18_699 ),
inference(sat_conversion,[],[f32740]) ).
cnf(s6509,plain,
( ~ spl18_44
| ~ spl18_542 ),
inference(sat_conversion,[],[f32780]) ).
cnf(s6529,plain,
( ~ spl18_544
| ~ spl18_713
| spl18_777 ),
inference(sat_conversion,[],[f32782]) ).
cnf(s6649,plain,
( ~ spl18_714
| ~ spl18_777 ),
inference(sat_conversion,[],[f32837]) ).
cnf(s6660,plain,
( spl18_200
| spl18_253
| ~ spl18_533
| ~ spl18_777 ),
inference(sat_conversion,[],[f32850]) ).
cnf(s6671,plain,
( ~ spl18_534
| spl18_699 ),
inference(rat,[],[s6083,s6156]) ).
cnf(s6702,plain,
( spl18_533
| spl18_534 ),
inference(rat,[],[s3549,s6133]) ).
cnf(s6718,plain,
( ~ spl18_214
| spl18_286 ),
inference(rat,[],[s2155,s6156]) ).
cnf(s6733,plain,
( ~ spl18_126
| spl18_215 ),
inference(rat,[],[s1567,s2141]) ).
cnf(s6734,plain,
( ~ spl18_126
| spl18_214 ),
inference(rat,[],[s1565,s2141]) ).
cnf(s6768,plain,
spl18_55,
inference(rat,[],[s464,s854]) ).
cnf(s6779,plain,
spl18_23,
inference(rat,[],[s238,s854]) ).
cnf(s6780,plain,
spl18_621,
inference(rat,[],[s4034,s4014,s6779]) ).
cnf(s6783,plain,
~ spl18_699,
inference(rat,[],[s4636,s6780]) ).
cnf(s6784,plain,
~ spl18_534,
inference(rat,[],[s6671,s6783]) ).
cnf(s6787,plain,
spl18_533,
inference(rat,[],[s6702,s6784]) ).
cnf(s6793,plain,
spl18_713,
inference(rat,[],[s6119,s600,s6787]) ).
cnf(s6796,plain,
~ spl18_44,
inference(rat,[],[s3568,s6463,s6509,s6156,s6783]) ).
cnf(s6799,plain,
spl18_544,
inference(rat,[],[s3613,s6768,s6796]) ).
cnf(s6803,plain,
spl18_777,
inference(rat,[],[s6529,s6793,s6799]) ).
cnf(s6809,plain,
~ spl18_714,
inference(rat,[],[s6649,s6803]) ).
cnf(s6810,plain,
spl18_200,
inference(rat,[],[s6660,s6787,s1849,s6803]) ).
cnf(s6813,plain,
~ spl18_125,
inference(rat,[],[s4677,s6793,s6809]) ).
cnf(s6814,plain,
~ spl18_277,
inference(rat,[],[s2191,s600,s6813]) ).
cnf(s6815,plain,
~ spl18_209,
inference(rat,[],[s2179,s600,s6813]) ).
cnf(s6817,plain,
spl18_201,
inference(rat,[],[s2104,s6814,s6810,s6813]) ).
cnf(s6819,plain,
spl18_126,
inference(rat,[],[s1551,s6815,s6817]) ).
cnf(s6821,plain,
spl18_215,
inference(rat,[],[s6733,s6819]) ).
cnf(s6822,plain,
spl18_214,
inference(rat,[],[s6734,s6819]) ).
cnf(s6824,plain,
~ spl18_286,
inference(rat,[],[s2675,s6821]) ).
cnf(s6825,plain,
$false,
inference(rat,[],[s6718,s6824,s6822]) ).
fof(f32859,plain,
$false,
inference(avatar_sat_refutation,[],[s6825]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR011+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.18 % Computer : n014.cluster.edu
% 0.11/0.18 % Model : x86_64 x86_64
% 0.11/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.18 % Memory : 8046.5625MB
% 0.11/0.18 % OS : Linux 6.8.0-71-generic
% 0.11/0.18 % CPULimit : 300
% 0.11/0.18 % WCLimit : 300
% 0.11/0.18 % DateTime : Mon Sep 28 22:05:46 UTC 2026
% 0.11/0.18 % CPUTime :
% 0.11/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.21 Running first-order model finding
% 0.11/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.78/2.33 % (2236563)Will run a generic schedule for satisfiability detection.
% 14.78/2.33 % (2236574)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2122181929:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.78/2.33 % (2236569)% WARNING: option uhcvi not known.
% 14.78/2.33 % (2236568)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2424612672_2999 on theBenchmark for (2999ds/0Mi)
% 14.78/2.33 % (2236570)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2891260825:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.78/2.33 % (2236571)dis+10_1_sil=32000:sp=arity:random_seed=73651739:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.78/2.33 % (2236572)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3261370363:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.78/2.33 % (2236569)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4004320193:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.78/2.33 % (2236573)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3943246859:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.78/2.33 % Detected minimum model sizes of [3]
% 14.78/2.33 % Detected maximum model sizes of [max]
% 14.78/2.33 % TRYING [3]
% 14.78/2.33 % TRYING [4]
% 14.78/2.33 % TRYING [5]
% 14.78/2.33 % (2236574)Instruction limit reached!
% 14.78/2.33 % (2236574)------------------------------
% 14.78/2.33 % (2236574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.78/2.33 % (2236574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.78/2.33 % (2236574)CaDiCaL version: 2.1.3
% 14.78/2.33 % (2236574)Termination reason: Instruction limit
% 14.78/2.33 % (2236574)Termination phase: Saturation
% 14.78/2.33 % (2236574)Time elapsed: 0.050 s
% 14.78/2.33 % (2236574)Peak memory usage: 13 MB
% 14.78/2.33 % (2236574)Instructions burned: 159 (million)
% 14.78/2.33 % (2236582)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2052515098:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.78/2.33 % (2236571)Instruction limit reached!
% 14.78/2.33 % (2236571)------------------------------
% 14.78/2.33 % (2236571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.78/2.33 % (2236571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.78/2.33 % (2236571)CaDiCaL version: 2.1.3
% 14.78/2.33 % (2236571)Termination reason: Instruction limit
% 14.78/2.33 % (2236571)Termination phase: Saturation
% 14.78/2.33 % (2236571)Time elapsed: 0.065 s
% 14.78/2.33 % (2236571)Peak memory usage: 12 MB
% 14.78/2.33 % (2236571)Instructions burned: 103 (million)
% 14.78/2.33 % Detected minimum model sizes of [3]
% 14.78/2.33 % Detected maximum model sizes of [max]
% 14.78/2.33 % TRYING [3]
% 14.78/2.33 % TRYING [6]
% 14.78/2.33 % (2236572)Instruction limit reached!
% 14.78/2.33 % (2236572)------------------------------
% 14.78/2.33 % (2236572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.78/2.33 % (2236572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.78/2.33 % (2236572)CaDiCaL version: 2.1.3
% 14.78/2.33 % (2236572)Termination reason: Instruction limit
% 14.78/2.33 % (2236572)Termination phase: Saturation
% 14.78/2.33 % (2236572)Time elapsed: 0.075 s
% 14.78/2.33 % (2236572)Peak memory usage: 13 MB
% 14.78/2.33 % (2236572)Instructions burned: 117 (million)
% 14.78/2.33 % TRYING [4]
% 14.78/2.33 % (2236573)Instruction limit reached!
% 14.78/2.33 % (2236573)------------------------------
% 14.78/2.33 % (2236573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.78/2.33 % (2236573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.78/2.33 % (2236573)CaDiCaL version: 2.1.3
% 14.78/2.33 % (2236573)Termination reason: Instruction limit
% 14.78/2.33 % (2236573)Termination phase: Saturation
% 14.78/2.33 % (2236573)Time elapsed: 0.084 s
% 14.78/2.33 % (2236584)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2020328057:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.78/2.33 % (2236573)Peak memory usage: 13 MB
% 14.78/2.33 % (2236573)Instructions burned: 132 (million)
% 14.78/2.33 % (2236585)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=2525039205:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.78/2.33 % TRYING [5]
% 14.78/2.33 % (2236587)ott-21_1_sil=16000:fs=off:random_seed=3502213998:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.78/2.33 % TRYING [6]
% 14.78/2.33 % TRYING [7]
% 14.78/2.33 % (2236584)Instruction limit reached!
% 32.53/4.91 % (2236584)------------------------------
% 32.53/4.91 % (2236584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.53/4.91 % (2236584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.53/4.91 % (2236584)CaDiCaL version: 2.1.3
% 32.53/4.91 % (2236584)Termination reason: Instruction limit
% 32.53/4.91 % (2236584)Termination phase: Saturation
% 32.53/4.91 % (2236584)Time elapsed: 0.090 s
% 32.53/4.91 % (2236584)Peak memory usage: 13 MB
% 32.53/4.91 % (2236584)Instructions burned: 132 (million)
% 32.53/4.91 % (2236587)Instruction limit reached!
% 32.53/4.91 % (2236587)------------------------------
% 32.53/4.91 % (2236587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.53/4.91 % (2236587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.53/4.91 % (2236587)CaDiCaL version: 2.1.3
% 32.53/4.91 % (2236587)Termination reason: Instruction limit
% 32.53/4.91 % (2236587)Termination phase: Saturation
% 32.53/4.91 % (2236587)Time elapsed: 0.086 s
% 32.53/4.91 % (2236587)Peak memory usage: 12 MB
% 32.53/4.91 % (2236587)Instructions burned: 182 (million)
% 32.53/4.91 % (2236590)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2234551107:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 32.53/4.91 % (2236591)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1097329097:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 32.53/4.91 % Detected minimum model sizes of [3]
% 32.53/4.91 % Detected maximum model sizes of [max]
% 32.53/4.91 % TRYING [3]
% 32.53/4.91 % TRYING [4]
% 32.53/4.91 % (2236585)Instruction limit reached!
% 32.53/4.91 % (2236585)------------------------------
% 32.53/4.91 % (2236585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.53/4.91 % (2236585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.53/4.91 % (2236585)CaDiCaL version: 2.1.3
% 32.53/4.91 % (2236585)Termination reason: Instruction limit
% 32.53/4.91 % (2236585)Termination phase: Saturation
% 32.53/4.91 % (2236585)Time elapsed: 0.182 s
% 32.53/4.91 % (2236585)Peak memory usage: 14 MB
% 32.53/4.91 % (2236585)Instructions burned: 689 (million)
% 32.53/4.91 % (2236594)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=913885689:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 32.53/4.91 % TRYING [5]
% 32.53/4.91 % TRYING [7]
% 32.53/4.91 % TRYING [8]
% 32.53/4.91 % (2236582)Instruction limit reached!
% 32.53/4.91 % (2236582)------------------------------
% 32.53/4.91 % (2236582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.53/4.91 % (2236582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.53/4.91 % (2236582)CaDiCaL version: 2.1.3
% 32.53/4.91 % (2236582)Termination reason: Instruction limit
% 32.53/4.91 % (2236582)Termination phase: Finite model building constraint generation
% 32.53/4.91 % (2236582)Time elapsed: 0.267 s
% 32.53/4.91 % (2236582)Peak memory usage: 28 MB
% 32.53/4.91 % (2236582)Instructions burned: 714 (million)
% 32.53/4.91 % (2236596)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=7208636:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 32.53/4.91 % TRYING [6]
% 32.53/4.91 % TRYING [14]
% 32.53/4.91 % (2236590)Instruction limit reached!
% 32.53/4.91 % (2236590)------------------------------
% 32.53/4.91 % (2236590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.53/4.91 % (2236590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.53/4.91 % (2236590)CaDiCaL version: 2.1.3
% 32.53/4.91 % (2236590)Termination reason: Instruction limit
% 32.53/4.91 % (2236590)Termination phase: Saturation
% 32.53/4.91 % (2236590)Time elapsed: 0.296 s
% 32.53/4.91 % (2236590)Peak memory usage: 13 MB
% 32.53/4.91 % (2236590)Instructions burned: 477 (million)
% 32.53/4.91 % (2236598)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=3067274942:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 32.53/4.91 % (2236591)Instruction limit reached!
% 32.53/4.91 % (2236591)------------------------------
% 32.53/4.91 % (2236591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.53/4.91 % (2236591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.53/4.91 % (2236591)CaDiCaL version: 2.1.3
% 32.53/4.91 % (2236591)Termination reason: Instruction limit
% 32.53/4.91 % (2236591)Termination phase: Finite model building SAT solving
% 32.53/4.91 % (2236591)Time elapsed: 0.336 s
% 32.53/4.91 % (2236591)Peak memory usage: 26 MB
% 32.53/4.91 % (2236591)Instructions burned: 866 (million)
% 47.42/8.06 % TRYING [9]
% 47.42/8.06 % (2236600)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3970316175:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 47.42/8.06 % (2236594)Instruction limit reached!
% 47.42/8.06 % (2236594)------------------------------
% 47.42/8.06 % (2236594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.42/8.06 % (2236594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.42/8.06 % (2236594)CaDiCaL version: 2.1.3
% 47.42/8.06 % (2236594)Termination reason: Instruction limit
% 47.42/8.06 % (2236594)Termination phase: Saturation
% 47.42/8.06 % (2236594)Time elapsed: 0.374 s
% 47.42/8.06 % (2236594)Peak memory usage: 20 MB
% 47.42/8.06 % (2236594)Instructions burned: 1181 (million)
% 47.42/8.06 % (2236602)fmb+10_1_sil=64000:random_seed=3169855628:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 47.42/8.06 % Detected minimum model sizes of [3]
% 47.42/8.06 % Detected maximum model sizes of [max]
% 47.42/8.06 % TRYING [3]
% 47.42/8.06 % TRYING [4]
% 47.42/8.06 % (2236596)Instruction limit reached!
% 47.42/8.06 % (2236596)------------------------------
% 47.42/8.06 % (2236596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.42/8.06 % (2236596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.42/8.06 % (2236596)CaDiCaL version: 2.1.3
% 47.42/8.06 % (2236596)Termination reason: Instruction limit
% 47.42/8.06 % (2236596)Termination phase: Finite model building constraint generation
% 47.42/8.06 % (2236596)Time elapsed: 0.335 s
% 47.42/8.06 % (2236596)Peak memory usage: 79 MB
% 47.42/8.06 % (2236596)Instructions burned: 890 (million)
% 47.42/8.06 % TRYING [5]
% 47.42/8.06 % (2236604)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3804145814:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 47.42/8.06 % Detected minimum model sizes of [3]
% 47.42/8.06 % Detected maximum model sizes of [max]
% 47.42/8.06 % TRYING [20]
% 47.42/8.06 % TRYING [6]
% 47.42/8.06 % TRYING [7]
% 47.42/8.06 % (2236598)Instruction limit reached!
% 47.42/8.06 % (2236598)------------------------------
% 47.42/8.06 % (2236598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.42/8.06 % (2236598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.42/8.06 % (2236598)CaDiCaL version: 2.1.3
% 47.42/8.06 % (2236598)Termination reason: Instruction limit
% 47.42/8.06 % (2236598)Termination phase: Saturation
% 47.42/8.06 % (2236598)Time elapsed: 0.381 s
% 47.42/8.06 % (2236598)Peak memory usage: 16 MB
% 47.42/8.06 % (2236598)Instructions burned: 692 (million)
% 47.42/8.06 % (2236606)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2078667591:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 47.42/8.06 % Detected minimum model sizes of [3]
% 47.42/8.06 % Detected maximum model sizes of [max]
% 47.42/8.06 % TRYING [8]
% 47.42/8.06 % TRYING [10]
% 47.42/8.06 % TRYING [8]
% 47.42/8.06 % (2236600)Instruction limit reached!
% 47.42/8.06 % (2236600)------------------------------
% 47.42/8.06 % (2236600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.42/8.06 % (2236600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.42/8.06 % (2236600)CaDiCaL version: 2.1.3
% 47.42/8.06 % (2236600)Termination reason: Instruction limit
% 47.42/8.06 % (2236600)Termination phase: Saturation
% 47.42/8.06 % (2236600)Time elapsed: 0.505 s
% 47.42/8.06 % (2236600)Peak memory usage: 19 MB
% 47.42/8.06 % (2236600)Instructions burned: 880 (million)
% 47.42/8.06 % (2236608)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1836386656:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 47.42/8.06 % TRYING [9]
% 47.42/8.06 % (2236606)Instruction limit reached!
% 47.42/8.06 % (2236606)------------------------------
% 47.42/8.06 % (2236606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.42/8.06 % (2236606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.42/8.06 % (2236606)CaDiCaL version: 2.1.3
% 47.42/8.06 % (2236606)Termination reason: Instruction limit
% 47.42/8.06 % (2236606)Termination phase: Finite model building constraint generation
% 47.42/8.06 % (2236606)Time elapsed: 0.353 s
% 47.42/8.06 % (2236606)Peak memory usage: 53 MB
% 47.42/8.06 % (2236606)Instructions burned: 923 (million)
% 47.42/8.06 % (2236610)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3629085881:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 47.42/8.06 % TRYING [9]
% 47.42/8.06 % TRYING [11]
% 47.42/8.06 % TRYING [10]
% 47.42/8.06 % (2236610)Instruction limit reached!
% 47.42/8.06 % (2236610)------------------------------
% 47.42/8.06 % (2236610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.42/8.06 % (2236610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.42/8.06 % (2236610)CaDiCaL version: 2.1.3
% 47.42/8.06 % (2236610)Termination reason: Instruction limit
% 47.42/8.06 % (2236610)Termination phase: Saturation
% 47.42/8.06 % (2236610)Time elapsed: 0.785 s
% 47.42/8.06 % (2236610)Peak memory usage: 24 MB
% 47.42/8.06 % (2236610)Instructions burned: 1472 (million)
% 47.42/8.06 % (2236612)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1142437395:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 47.42/8.06 % Detected minimum model sizes of [3]
% 47.42/8.06 % Detected maximum model sizes of [max]
% 47.42/8.06 % TRYING [77]
% 47.42/8.06 % TRYING [11]
% 47.42/8.06 % TRYING [12]
% 47.42/8.06 % (2236608)Instruction limit reached!
% 47.42/8.06 % (2236608)------------------------------
% 47.42/8.06 % (2236608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.42/8.06 % (2236608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.42/8.06 % (2236608)CaDiCaL version: 2.1.3
% 47.42/8.06 % (2236608)Termination reason: Instruction limit
% 47.42/8.06 % (2236608)Termination phase: Saturation
% 47.42/8.06 % (2236608)Time elapsed: 2.683 s
% 47.42/8.06 % (2236608)Peak memory usage: 22 MB
% 47.42/8.06 % (2236608)Instructions burned: 5131 (million)
% 47.42/8.06 % (2236614)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4152252806:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 47.42/8.06 % Detected minimum model sizes of [3]
% 47.42/8.06 % Detected maximum model sizes of [max]
% 47.42/8.06 % TRYING [16]
% 47.42/8.06 % (2236604)Instruction limit reached!
% 47.42/8.06 % (2236604)------------------------------
% 47.42/8.06 % (2236604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.42/8.06 % (2236604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.42/8.06 % (2236604)CaDiCaL version: 2.1.3
% 47.42/8.06 % (2236604)Termination reason: Instruction limit
% 47.42/8.06 % (2236604)Termination phase: Finite model building constraint generation
% 47.42/8.06 % (2236604)Time elapsed: 3.400 s
% 47.42/8.06 % (2236604)Peak memory usage: 611 MB
% 47.42/8.06 % (2236604)Instructions burned: 9515 (million)
% 47.42/8.06 % (2236616)ott-2_1_sil=16000:newcnf=on:random_seed=359804969:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 47.42/8.06 % TRYING [12]
% 47.42/8.06 % (2236612)Instruction limit reached!
% 47.42/8.06 % (2236612)------------------------------
% 47.42/8.06 % (2236612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.42/8.06 % (2236612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.42/8.06 % (2236612)CaDiCaL version: 2.1.3
% 47.42/8.06 % (2236612)Termination reason: Instruction limit
% 47.42/8.06 % (2236612)Termination phase: Finite model building constraint generation
% 47.42/8.06 % (2236612)Time elapsed: 2.355 s
% 47.42/8.06 % (2236612)Peak memory usage: 516 MB
% 47.42/8.06 % (2236612)Instructions burned: 6325 (million)
% 47.42/8.06 % (2236618)ott+10_1_sil=32000:tgt=ground:random_seed=586144699:i=5114:av=off_2954 on theBenchmark for (2954ds/5114Mi)
% 47.42/8.06 % (2236614)Instruction limit reached!
% 47.42/8.06 % (2236614)------------------------------
% 47.42/8.06 % (2236614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.42/8.06 % (2236614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.42/8.06 % (2236614)CaDiCaL version: 2.1.3
% 47.42/8.06 % (2236614)Termination reason: Instruction limit
% 47.42/8.06 % (2236614)Termination phase: Finite model building constraint generation
% 47.42/8.06 % (2236614)Time elapsed: 0.738 s
% 47.42/8.06 % (2236614)Peak memory usage: 134 MB
% 47.42/8.06 % (2236614)Instructions burned: 2176 (million)
% 47.42/8.06 % (2236620)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1255020782:i=54282_2954 on theBenchmark for (2954ds/54282Mi)
% 47.42/8.06 % Detected minimum model sizes of [3]
% 47.42/8.06 % Detected maximum model sizes of [max]
% 47.42/8.06 % TRYING [3]
% 47.42/8.06 % TRYING [4]
% 47.42/8.06 % TRYING [5]
% 47.42/8.06 % TRYING [6]
% 47.42/8.06 % (2236616)Instruction limit reached!
% 47.42/8.06 % (2236616)------------------------------
% 47.42/8.06 % (2236616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.42/8.06 % (2236616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.42/8.06 % (2236616)CaDiCaL version: 2.1.3
% 47.42/8.06 % (2236616)Termination reason: Instruction limit
% 47.42/8.06 % (2236616)Termination phase: Saturation
% 47.42/8.06 % (2236616)Time elapsed: 0.447 s
% 47.42/8.06 % (2236616)Peak memory usage: 15 MB
% 47.42/8.06 % (2236616)Instructions burned: 869 (million)
% 47.42/8.06 % (2236622)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3514844636:i=3512:aac=none_2953 on theBenchmark for (2953ds/3512Mi)
% 47.42/8.06 % TRYING [7]
% 47.42/8.06 % TRYING [8]
% 47.42/8.06 % TRYING [13]
% 47.42/8.06 % TRYING [9]
% 47.42/8.06 % TRYING [10]
% 47.42/8.06 % (2236602)Instruction limit reached!
% 47.42/8.06 % (2236602)------------------------------
% 47.42/8.06 % (2236602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.42/8.06 % (2236602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.42/8.06 % (2236602)CaDiCaL version: 2.1.3
% 47.42/8.06 % (2236602)Termination reason: Instruction limit
% 47.42/8.06 % (2236602)Termination phase: Finite model building SAT solving
% 47.42/8.06 % (2236602)Time elapsed: 5.432 s
% 47.42/8.06 % (2236602)Peak memory usage: 232 MB
% 47.42/8.06 % (2236602)Instructions burned: 22063 (million)
% 47.42/8.06 % (2236624)dis+21_1_sil=32000:sas=cadical:random_seed=3826055034:i=3773:amm=off_2938 on theBenchmark for (2938ds/3773Mi)
% 47.42/8.06 % TRYING [11]
% 47.42/8.06 % (2236622)Instruction limit reached!
% 47.42/8.06 % (2236622)------------------------------
% 47.42/8.06 % (2236622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.42/8.06 % (2236622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.42/8.06 % (2236622)CaDiCaL version: 2.1.3
% 47.42/8.06 % (2236622)Termination reason: Instruction limit
% 47.42/8.06 % (2236622)Termination phase: Saturation
% 47.42/8.06 % (2236622)Time elapsed: 1.916 s
% 47.42/8.06 % (2236622)Peak memory usage: 25 MB
% 47.42/8.06 % (2236622)Instructions burned: 3512 (million)
% 47.42/8.06 % (2236626)ott+11_1_sil=16000:gs=on:random_seed=1326670987:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2933 on theBenchmark for (2933ds/2251Mi)
% 47.42/8.06 % (2236618)Instruction limit reached!
% 47.42/8.06 % (2236618)------------------------------
% 47.42/8.06 % (2236618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.42/8.06 % (2236618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.42/8.06 % (2236618)CaDiCaL version: 2.1.3
% 47.42/8.06 % (2236618)Termination reason: Instruction limit
% 47.42/8.06 % (2236618)Termination phase: Saturation
% 47.42/8.06 % (2236618)Time elapsed: 2.626 s
% 47.42/8.06 % (2236618)Peak memory usage: 25 MB
% 47.42/8.06 % (2236618)Instructions burned: 5115 (million)
% 47.42/8.06 % (2236628)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3607786144:fmbsr=1.6:i=67534_2928 on theBenchmark for (2928ds/67534Mi)
% 47.42/8.06 % Detected minimum model sizes of [3]
% 47.42/8.06 % Detected maximum model sizes of [max]
% 47.42/8.06 % TRYING [7]
% 47.42/8.06 % (2236624)Instruction limit reached!
% 47.42/8.06 % (2236624)------------------------------
% 47.42/8.06 % (2236624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.42/8.06 % (2236624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.42/8.06 % (2236624)CaDiCaL version: 2.1.3
% 47.42/8.06 % (2236624)Termination reason: Instruction limit
% 47.42/8.06 % (2236624)Termination phase: Saturation
% 47.42/8.06 % (2236624)Time elapsed: 1.107 s
% 47.42/8.06 % (2236624)Peak memory usage: 26 MB
% 47.42/8.06 % (2236624)Instructions burned: 3774 (million)
% 47.42/8.06 % (2236630)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4056270695:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2927 on theBenchmark for (2927ds/4591Mi)
% 47.42/8.06 % TRYING [12]
% 47.42/8.06 % (2236626) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2236563-2236626"...
% 47.42/8.06 % (2236626)...printing done.
% 47.42/8.06 % (2236626)Refutation found. Thanks to Tanya!
% 47.42/8.06 % SZS status Theorem for theBenchmark
% 47.42/8.06 % SZS output start Proof for theBenchmark
% See solution above
% 47.42/8.06 % (2236626)------------------------------
% 47.42/8.06 % (2236626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.42/8.06 % (2236626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.42/8.06 % (2236626)CaDiCaL version: 2.1.3
% 47.42/8.06 % (2236626)Termination reason: Refutation
% 47.42/8.06 % (2236626)Time elapsed: 1.120 s
% 47.42/8.06 % (2236626)Peak memory usage: 27 MB
% 47.42/8.06 % (2236626)Instructions burned: 1749 (million)
% 47.42/8.06 % (2236563)Success in time 7.84 s
% 47.42/8.06 % Vampire exiting
%------------------------------------------------------------------------------