%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : CSR005+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n010.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 : Fri Sep 25 01:09:52 PM UTC 2026
% Result : Theorem 244.90s 58.55s
% Output : CNFRefutation 244.90s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f249ERROR: Could not build tree for root c_694802ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( stoppedIn(X0,X1,X2)
<=> ? [X3,X4] :
( terminates(X3,X1,X4)
& less(X4,X2)
& less(X0,X4)
& happens(X3,X4) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',stoppedin_defn) ).
fof(f3,axiom,
! [X0,X1,X2,X3,X4] :
( ( ~ stoppedIn(X1,X2,plus(X1,X4))
& trajectory(X2,X1,X3,X4)
& less(n0,X4)
& initiates(X0,X2,X1)
& happens(X0,X1) )
=> holdsAt(X3,plus(X1,X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',change_holding) ).
fof(f5,axiom,
! [X0,X1] :
( ( ~ ? [X2] :
( terminates(X2,X0,X1)
& happens(X2,X1) )
& ~ releasedAt(X0,plus(X1,n1))
& holdsAt(X0,X1) )
=> holdsAt(X0,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',keep_holding) ).
fof(f6,axiom,
! [X0,X1] :
( ( ~ ? [X2] :
( initiates(X2,X0,X1)
& happens(X2,X1) )
& ~ releasedAt(X0,plus(X1,n1))
& ~ holdsAt(X0,X1) )
=> ~ holdsAt(X0,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',keep_not_holding) ).
fof(f7,axiom,
! [X0,X1] :
( ( ~ ? [X2] :
( ( terminates(X2,X0,X1)
| initiates(X2,X0,X1) )
& happens(X2,X1) )
& releasedAt(X0,X1) )
=> releasedAt(X0,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',keep_released) ).
fof(f8,axiom,
! [X0,X1] :
( ( ~ ? [X2] :
( releases(X2,X0,X1)
& happens(X2,X1) )
& ~ releasedAt(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] :
( ( initiates(X0,X2,X1)
& happens(X0,X1) )
=> holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_holds) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( terminates(X0,X2,X1)
& happens(X0,X1) )
=> ~ holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_terminates_not_holds) ).
fof(f11,axiom,
! [X0,X1,X2] :
( ( releases(X0,X2,X1)
& happens(X0,X1) )
=> releasedAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_releases) ).
fof(f12,axiom,
! [X0,X1,X2] :
( ( ( terminates(X0,X2,X1)
| initiates(X0,X2,X1) )
& happens(X0,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)
<=> ( ? [X3] :
( X1 = waterLevel(X3)
& X0 = overflow
& holdsAt(waterLevel(X3),X2) )
| ? [X3] :
( X1 = waterLevel(X3)
& X0 = tapOff
& holdsAt(waterLevel(X3),X2) )
| ( X1 = spilling
& X0 = overflow )
| ( X1 = filling
& X0 = tapOn ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',initiates_all_defn) ).
fof(f14,axiom,
! [X0,X1,X2] :
( terminates(X0,X1,X2)
<=> ( ( X1 = filling
& X0 = overflow )
| ( X1 = filling
& X0 = tapOff ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',terminates_all_defn) ).
fof(f15,axiom,
! [X0,X1,X2] :
( releases(X0,X1,X2)
<=> ? [X3] :
( X1 = waterLevel(X3)
& X0 = tapOn ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',releases_all_defn) ).
fof(f16,axiom,
! [X0,X1] :
( happens(X0,X1)
<=> ( ( X0 = overflow
& holdsAt(filling,X1)
& holdsAt(waterLevel(n3),X1) )
| ( X1 = n0
& X0 = tapOn ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',happens_all_defn) ).
fof(f17,axiom,
! [X0,X1,X2,X3] :
( ( X2 = plus(X0,X3)
& holdsAt(waterLevel(X0),X1) )
=> 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(X2),X0)
& holdsAt(waterLevel(X1),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(f22,axiom,
! [X0] : filling != waterLevel(X0),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+1.ax',filling_not_waterLevel) ).
fof(f26,axiom,
plus(n0,n0) = n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus0_0) ).
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(f32,axiom,
plus(n1,n3) = n4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus1_3) ).
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)
<=> ( X0 = X1
| less(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_or_equal) ).
fof(f38,axiom,
~ ? [X0] : less(X0,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less0) ).
fof(f39,axiom,
! [X0] :
( less(X0,n1)
<=> less_or_equal(X0,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less1) ).
fof(f40,axiom,
! [X0] :
( less(X0,n2)
<=> less_or_equal(X0,n1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less2) ).
fof(f41,axiom,
! [X0] :
( less(X0,n3)
<=> less_or_equal(X0,n2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less3) ).
fof(f42,axiom,
! [X0] :
( less(X0,n4)
<=> less_or_equal(X0,n3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less4) ).
fof(f48,axiom,
! [X0,X1] :
( less(X0,X1)
<=> ( X1 != X0
& ~ less(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,
holdsAt(filling,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',filling_3) ).
fof(f56,negated_conjecture,
~ holdsAt(filling,n3),
inference(negated_conjecture,[status(cth)],[f55]) ).
fof(f57,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( ? [X4] :
( waterLevel(X4) = X1
& X0 = overflow
& holdsAt(waterLevel(X4),X2) )
| ? [X3] :
( X1 = waterLevel(X3)
& X0 = tapOff
& holdsAt(waterLevel(X3),X2) )
| ( X1 = spilling
& X0 = overflow )
| ( X1 = filling
& X0 = tapOn ) ) ),
inference(rectify,[],[f13]) ).
fof(f58,plain,
~ holdsAt(filling,n3),
inference(flattening,[],[f56]) ).
fof(f60,plain,
! [X0,X1,X2] :
( stoppedIn(X0,X1,X2)
=> ? [X3,X4] :
( terminates(X3,X1,X4)
& less(X4,X2)
& less(X0,X4)
& happens(X3,X4) ) ),
inference(unused_predicate_definition_removal,[],[f1]) ).
fof(f63,plain,
! [X0,X1,X2] :
( ~ stoppedIn(X0,X1,X2)
| ? [X3,X4] :
( terminates(X3,X1,X4)
& less(X4,X2)
& less(X0,X4)
& happens(X3,X4) ) ),
inference(ennf_transformation,[],[f60]) ).
fof(f64,plain,
! [X0,X1,X2,X3,X4] :
( stoppedIn(X1,X2,plus(X1,X4))
| ~ trajectory(X2,X1,X3,X4)
| ~ less(n0,X4)
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X3,plus(X1,X4)) ),
inference(ennf_transformation,[],[f3]) ).
fof(f65,plain,
! [X0,X1,X2,X3,X4] :
( stoppedIn(X1,X2,plus(X1,X4))
| ~ trajectory(X2,X1,X3,X4)
| ~ less(n0,X4)
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X3,plus(X1,X4)) ),
inference(flattening,[],[f64]) ).
fof(f66,plain,
! [X0,X1] :
( ? [X2] :
( terminates(X2,X0,X1)
& happens(X2,X1) )
| releasedAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1)) ),
inference(ennf_transformation,[],[f5]) ).
fof(f67,plain,
! [X0,X1] :
( ? [X2] :
( terminates(X2,X0,X1)
& happens(X2,X1) )
| releasedAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1)) ),
inference(flattening,[],[f66]) ).
fof(f68,plain,
! [X0,X1] :
( ? [X2] :
( initiates(X2,X0,X1)
& happens(X2,X1) )
| releasedAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| ~ holdsAt(X0,plus(X1,n1)) ),
inference(ennf_transformation,[],[f6]) ).
fof(f69,plain,
! [X0,X1] :
( ? [X2] :
( initiates(X2,X0,X1)
& happens(X2,X1) )
| releasedAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| ~ holdsAt(X0,plus(X1,n1)) ),
inference(flattening,[],[f68]) ).
fof(f70,plain,
! [X0,X1] :
( ? [X2] :
( ( terminates(X2,X0,X1)
| initiates(X2,X0,X1) )
& happens(X2,X1) )
| ~ releasedAt(X0,X1)
| releasedAt(X0,plus(X1,n1)) ),
inference(ennf_transformation,[],[f7]) ).
fof(f71,plain,
! [X0,X1] :
( ? [X2] :
( ( terminates(X2,X0,X1)
| initiates(X2,X0,X1) )
& happens(X2,X1) )
| ~ releasedAt(X0,X1)
| releasedAt(X0,plus(X1,n1)) ),
inference(flattening,[],[f70]) ).
fof(f72,plain,
! [X0,X1] :
( ? [X2] :
( releases(X2,X0,X1)
& happens(X2,X1) )
| releasedAt(X0,X1)
| ~ releasedAt(X0,plus(X1,n1)) ),
inference(ennf_transformation,[],[f8]) ).
fof(f73,plain,
! [X0,X1] :
( ? [X2] :
( releases(X2,X0,X1)
& happens(X2,X1) )
| releasedAt(X0,X1)
| ~ releasedAt(X0,plus(X1,n1)) ),
inference(flattening,[],[f72]) ).
fof(f74,plain,
! [X0,X1,X2] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(ennf_transformation,[],[f9]) ).
fof(f75,plain,
! [X0,X1,X2] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(flattening,[],[f74]) ).
fof(f76,plain,
! [X0,X1,X2] :
( ~ terminates(X0,X2,X1)
| ~ happens(X0,X1)
| ~ holdsAt(X2,plus(X1,n1)) ),
inference(ennf_transformation,[],[f10]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ~ terminates(X0,X2,X1)
| ~ happens(X0,X1)
| ~ holdsAt(X2,plus(X1,n1)) ),
inference(flattening,[],[f76]) ).
fof(f78,plain,
! [X0,X1,X2] :
( ~ releases(X0,X2,X1)
| ~ happens(X0,X1)
| releasedAt(X2,plus(X1,n1)) ),
inference(ennf_transformation,[],[f11]) ).
fof(f79,plain,
! [X0,X1,X2] :
( ~ releases(X0,X2,X1)
| ~ happens(X0,X1)
| releasedAt(X2,plus(X1,n1)) ),
inference(flattening,[],[f78]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ( ~ terminates(X0,X2,X1)
& ~ initiates(X0,X2,X1) )
| ~ happens(X0,X1)
| ~ releasedAt(X2,plus(X1,n1)) ),
inference(ennf_transformation,[],[f12]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ( ~ terminates(X0,X2,X1)
& ~ initiates(X0,X2,X1) )
| ~ happens(X0,X1)
| ~ releasedAt(X2,plus(X1,n1)) ),
inference(flattening,[],[f80]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( plus(X0,X3) != X2
| ~ holdsAt(waterLevel(X0),X1)
| trajectory(filling,X1,waterLevel(X2),X3) ),
inference(ennf_transformation,[],[f17]) ).
fof(f83,plain,
! [X0,X1,X2,X3] :
( plus(X0,X3) != X2
| ~ holdsAt(waterLevel(X0),X1)
| trajectory(filling,X1,waterLevel(X2),X3) ),
inference(flattening,[],[f82]) ).
fof(f84,plain,
! [X0,X1,X2] :
( ~ holdsAt(waterLevel(X2),X0)
| ~ holdsAt(waterLevel(X1),X0)
| X1 = X2 ),
inference(ennf_transformation,[],[f18]) ).
fof(f85,plain,
! [X0,X1,X2] :
( ~ holdsAt(waterLevel(X2),X0)
| ~ holdsAt(waterLevel(X1),X0)
| X1 = X2 ),
inference(flattening,[],[f84]) ).
fof(f86,plain,
! [X0] : ~ less(X0,n0),
inference(ennf_transformation,[],[f38]) ).
fof(f90,plain,
! [X0,X1,X2] :
( ~ stoppedIn(X0,X1,X2)
| ( terminates(sK2(X0,X1,X2),X1,sK3(X0,X1,X2))
& less(sK3(X0,X1,X2),X2)
& less(X0,sK3(X0,X1,X2))
& happens(sK2(X0,X1,X2),sK3(X0,X1,X2)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X3,sK2(X0,X1,X2)),skolemize(X4,sK3(X0,X1,X2))],[f63]) ).
fof(f91,plain,
! [X0,X1] :
( ( terminates(sK4(X0,X1),X0,X1)
& happens(sK4(X0,X1),X1) )
| releasedAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X2,sK4(X0,X1))],[f67]) ).
fof(f92,plain,
! [X0,X1] :
( ( initiates(sK5(X0,X1),X0,X1)
& happens(sK5(X0,X1),X1) )
| releasedAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| ~ holdsAt(X0,plus(X1,n1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X2,sK5(X0,X1))],[f69]) ).
fof(f93,plain,
! [X0,X1] :
( ( ( terminates(sK6(X0,X1),X0,X1)
| initiates(sK6(X0,X1),X0,X1) )
& happens(sK6(X0,X1),X1) )
| ~ releasedAt(X0,X1)
| releasedAt(X0,plus(X1,n1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X2,sK6(X0,X1))],[f71]) ).
fof(f94,plain,
! [X0,X1] :
( ( releases(sK7(X0,X1),X0,X1)
& happens(sK7(X0,X1),X1) )
| releasedAt(X0,X1)
| ~ releasedAt(X0,plus(X1,n1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f73]) ).
fof(f101,plain,
! [X0,X1,X2] :
( ( ~ initiates(X0,X1,X2)
| sP0(X2,X0,X1)
| sP1(X2,X0,X1)
| ( X1 = spilling
& X0 = overflow )
| ( X1 = filling
& X0 = tapOn ) )
& ( ( ~ sP0(X2,X0,X1)
& ~ sP1(X2,X0,X1)
& ( spilling != X1
| overflow != X0 )
& ( filling != X1
| tapOn != X0 ) )
| initiates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f89]) ).
fof(f102,plain,
! [X0,X1,X2] :
( ( ~ initiates(X0,X1,X2)
| sP0(X2,X0,X1)
| sP1(X2,X0,X1)
| ( X1 = spilling
& X0 = overflow )
| ( X1 = filling
& X0 = tapOn ) )
& ( ( ~ sP0(X2,X0,X1)
& ~ sP1(X2,X0,X1)
& ( spilling != X1
| overflow != X0 )
& ( filling != X1
| tapOn != X0 ) )
| initiates(X0,X1,X2) ) ),
inference(flattening,[],[f101]) ).
fof(f103,plain,
! [X0,X1,X2] :
( ( ~ terminates(X0,X1,X2)
| ( X1 = filling
& X0 = overflow )
| ( X1 = filling
& X0 = tapOff ) )
& ( ( ( filling != X1
| overflow != X0 )
& ( filling != X1
| tapOff != X0 ) )
| terminates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f14]) ).
fof(f104,plain,
! [X0,X1,X2] :
( ( ~ terminates(X0,X1,X2)
| ( X1 = filling
& X0 = overflow )
| ( X1 = filling
& X0 = tapOff ) )
& ( ( ( filling != X1
| overflow != X0 )
& ( filling != X1
| tapOff != X0 ) )
| terminates(X0,X1,X2) ) ),
inference(flattening,[],[f103]) ).
fof(f105,plain,
! [X0,X1,X2] :
( ( ~ releases(X0,X1,X2)
| ? [X3] :
( X1 = waterLevel(X3)
& X0 = tapOn ) )
& ( ! [X3] :
( waterLevel(X3) != X1
| tapOn != X0 )
| releases(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f15]) ).
fof(f106,plain,
! [X0,X1,X2] :
( ( ~ releases(X0,X1,X2)
| ? [X4] :
( waterLevel(X4) = X1
& X0 = tapOn ) )
& ( ! [X3] :
( waterLevel(X3) != X1
| tapOn != X0 )
| releases(X0,X1,X2) ) ),
inference(rectify,[],[f105]) ).
fof(f107,plain,
! [X0,X1,X2] :
( ( ~ releases(X0,X1,X2)
| ( waterLevel(sK10(X0,X1)) = X1
& X0 = tapOn ) )
& ( ! [X3] :
( waterLevel(X3) != X1
| tapOn != X0 )
| releases(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X4,sK10(X0,X1))],[f106]) ).
fof(f108,plain,
! [X0,X1] :
( ( ~ happens(X0,X1)
| ( X0 = overflow
& holdsAt(filling,X1)
& holdsAt(waterLevel(n3),X1) )
| ( X1 = n0
& X0 = tapOn ) )
& ( ( ( overflow != X0
| ~ holdsAt(filling,X1)
| ~ holdsAt(waterLevel(n3),X1) )
& ( n0 != X1
| tapOn != X0 ) )
| happens(X0,X1) ) ),
inference(nnf_transformation,[],[f16]) ).
fof(f109,plain,
! [X0,X1] :
( ( ~ happens(X0,X1)
| ( X0 = overflow
& holdsAt(filling,X1)
& holdsAt(waterLevel(n3),X1) )
| ( X1 = n0
& X0 = tapOn ) )
& ( ( ( overflow != X0
| ~ holdsAt(filling,X1)
| ~ holdsAt(waterLevel(n3),X1) )
& ( n0 != X1
| tapOn != X0 ) )
| happens(X0,X1) ) ),
inference(flattening,[],[f108]) ).
fof(f111,plain,
! [X0,X1] :
( ( ~ less_or_equal(X0,X1)
| X0 = X1
| less(X0,X1) )
& ( ( X0 != X1
& ~ less(X0,X1) )
| less_or_equal(X0,X1) ) ),
inference(nnf_transformation,[],[f37]) ).
fof(f112,plain,
! [X0,X1] :
( ( ~ less_or_equal(X0,X1)
| X0 = X1
| less(X0,X1) )
& ( ( X0 != X1
& ~ less(X0,X1) )
| less_or_equal(X0,X1) ) ),
inference(flattening,[],[f111]) ).
fof(f113,plain,
! [X0] :
( ( ~ less(X0,n1)
| less_or_equal(X0,n0) )
& ( ~ less_or_equal(X0,n0)
| less(X0,n1) ) ),
inference(nnf_transformation,[],[f39]) ).
fof(f114,plain,
! [X0] :
( ( ~ less(X0,n2)
| less_or_equal(X0,n1) )
& ( ~ less_or_equal(X0,n1)
| less(X0,n2) ) ),
inference(nnf_transformation,[],[f40]) ).
fof(f115,plain,
! [X0] :
( ( ~ less(X0,n3)
| less_or_equal(X0,n2) )
& ( ~ less_or_equal(X0,n2)
| less(X0,n3) ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f116,plain,
! [X0] :
( ( ~ less(X0,n4)
| less_or_equal(X0,n3) )
& ( ~ less_or_equal(X0,n3)
| less(X0,n4) ) ),
inference(nnf_transformation,[],[f42]) ).
fof(f122,plain,
! [X0,X1] :
( ( ~ less(X0,X1)
| ( X1 != X0
& ~ less(X1,X0) ) )
& ( X0 = X1
| less(X1,X0)
| less(X0,X1) ) ),
inference(nnf_transformation,[],[f48]) ).
fof(f123,plain,
! [X0,X1] :
( ( ~ less(X0,X1)
| ( X1 != X0
& ~ less(X1,X0) ) )
& ( X0 = X1
| less(X1,X0)
| less(X0,X1) ) ),
inference(flattening,[],[f122]) ).
fof(f124,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| terminates(sK2(X0,X1,X2),X1,sK3(X0,X1,X2)) ),
inference(cnf_transformation,[],[f90]) ).
fof(f125,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| less(sK3(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f90]) ).
fof(f126,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| less(X0,sK3(X0,X1,X2)) ),
inference(cnf_transformation,[],[f90]) ).
fof(f127,plain,
! [X2,X0,X1] :
( ~ stoppedIn(X0,X1,X2)
| happens(sK2(X0,X1,X2),sK3(X0,X1,X2)) ),
inference(cnf_transformation,[],[f90]) ).
fof(f128,plain,
! [X2,X3,X0,X1,X4] :
( stoppedIn(X1,X2,plus(X1,X4))
| ~ trajectory(X2,X1,X3,X4)
| ~ less(n0,X4)
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X3,plus(X1,X4)) ),
inference(cnf_transformation,[],[f65]) ).
fof(f129,plain,
! [X0,X1] :
( terminates(sK4(X0,X1),X0,X1)
| releasedAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f91]) ).
fof(f130,plain,
! [X0,X1] :
( happens(sK4(X0,X1),X1)
| releasedAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| holdsAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f91]) ).
fof(f131,plain,
! [X0,X1] :
( initiates(sK5(X0,X1),X0,X1)
| releasedAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| ~ holdsAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f92]) ).
fof(f132,plain,
! [X0,X1] :
( happens(sK5(X0,X1),X1)
| releasedAt(X0,plus(X1,n1))
| holdsAt(X0,X1)
| ~ holdsAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f92]) ).
fof(f133,plain,
! [X0,X1] :
( terminates(sK6(X0,X1),X0,X1)
| initiates(sK6(X0,X1),X0,X1)
| ~ releasedAt(X0,X1)
| releasedAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f93]) ).
fof(f134,plain,
! [X0,X1] :
( happens(sK6(X0,X1),X1)
| ~ releasedAt(X0,X1)
| releasedAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f93]) ).
fof(f135,plain,
! [X0,X1] :
( releases(sK7(X0,X1),X0,X1)
| releasedAt(X0,X1)
| ~ releasedAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f94]) ).
fof(f136,plain,
! [X0,X1] :
( happens(sK7(X0,X1),X1)
| releasedAt(X0,X1)
| ~ releasedAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f94]) ).
fof(f137,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f75]) ).
fof(f138,plain,
! [X2,X0,X1] :
( ~ terminates(X0,X2,X1)
| ~ happens(X0,X1)
| ~ holdsAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f77]) ).
fof(f139,plain,
! [X2,X0,X1] :
( ~ releases(X0,X2,X1)
| ~ happens(X0,X1)
| releasedAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f140,plain,
! [X2,X0,X1] :
( ~ terminates(X0,X2,X1)
| ~ happens(X0,X1)
| ~ releasedAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f81]) ).
fof(f141,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| ~ releasedAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f81]) ).
fof(f154,plain,
! [X2,X0,X1] :
( ~ sP0(X2,X0,X1)
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f102]) ).
fof(f156,plain,
! [X2,X0,X1] :
( spilling != X1
| overflow != X0
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f102]) ).
fof(f157,plain,
! [X2,X0,X1] :
( filling != X1
| tapOn != X0
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f102]) ).
fof(f161,plain,
! [X2,X0,X1] :
( ~ terminates(X0,X1,X2)
| overflow = X0
| tapOff = X0 ),
inference(cnf_transformation,[],[f104]) ).
fof(f162,plain,
! [X2,X0,X1] :
( filling != X1
| overflow != X0
| terminates(X0,X1,X2) ),
inference(cnf_transformation,[],[f104]) ).
fof(f163,plain,
! [X2,X0,X1] :
( filling != X1
| tapOff != X0
| terminates(X0,X1,X2) ),
inference(cnf_transformation,[],[f104]) ).
fof(f164,plain,
! [X2,X0,X1] :
( ~ releases(X0,X1,X2)
| waterLevel(sK10(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f107]) ).
fof(f166,plain,
! [X2,X3,X0,X1] :
( waterLevel(X3) != X1
| tapOn != X0
| releases(X0,X1,X2) ),
inference(cnf_transformation,[],[f107]) ).
fof(f168,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| holdsAt(filling,X1)
| n0 = X1 ),
inference(cnf_transformation,[],[f109]) ).
fof(f169,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| holdsAt(waterLevel(n3),X1)
| n0 = X1 ),
inference(cnf_transformation,[],[f109]) ).
fof(f170,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| overflow = X0
| tapOn = X0 ),
inference(cnf_transformation,[],[f109]) ).
fof(f172,plain,
! [X0,X1] :
( ~ happens(X0,X1)
| holdsAt(waterLevel(n3),X1)
| tapOn = X0 ),
inference(cnf_transformation,[],[f109]) ).
fof(f173,plain,
! [X0,X1] :
( overflow != X0
| ~ holdsAt(filling,X1)
| ~ holdsAt(waterLevel(n3),X1)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f109]) ).
fof(f174,plain,
! [X0,X1] :
( n0 != X1
| tapOn != X0
| happens(X0,X1) ),
inference(cnf_transformation,[],[f109]) ).
fof(f175,plain,
! [X2,X3,X0,X1] :
( plus(X0,X3) != X2
| ~ holdsAt(waterLevel(X0),X1)
| trajectory(filling,X1,waterLevel(X2),X3) ),
inference(cnf_transformation,[],[f83]) ).
fof(f176,plain,
! [X2,X0,X1] :
( ~ holdsAt(waterLevel(X2),X0)
| ~ holdsAt(waterLevel(X1),X0)
| X1 = X2 ),
inference(cnf_transformation,[],[f85]) ).
fof(f179,plain,
tapOn != overflow,
inference(cnf_transformation,[],[f21]) ).
fof(f180,plain,
! [X0] : filling != waterLevel(X0),
inference(cnf_transformation,[],[f22]) ).
fof(f185,plain,
n0 = plus(n0,n0),
inference(cnf_transformation,[],[f26]) ).
fof(f186,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f27]) ).
fof(f187,plain,
n2 = plus(n0,n2),
inference(cnf_transformation,[],[f28]) ).
fof(f189,plain,
n2 = plus(n1,n1),
inference(cnf_transformation,[],[f30]) ).
fof(f190,plain,
n3 = plus(n1,n2),
inference(cnf_transformation,[],[f31]) ).
fof(f191,plain,
plus(n1,n3) = n4,
inference(cnf_transformation,[],[f32]) ).
fof(f195,plain,
! [X0,X1] : plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[],[f36]) ).
fof(f196,plain,
! [X0,X1] :
( ~ less_or_equal(X0,X1)
| X0 = X1
| less(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f197,plain,
! [X0,X1] :
( X0 != X1
| less_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f198,plain,
! [X0,X1] :
( ~ less(X0,X1)
| less_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f199,plain,
! [X0] : ~ less(X0,n0),
inference(cnf_transformation,[],[f86]) ).
fof(f200,plain,
! [X0] :
( ~ less(X0,n1)
| less_or_equal(X0,n0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f201,plain,
! [X0] :
( ~ less_or_equal(X0,n0)
| less(X0,n1) ),
inference(cnf_transformation,[],[f113]) ).
fof(f202,plain,
! [X0] :
( ~ less(X0,n2)
| less_or_equal(X0,n1) ),
inference(cnf_transformation,[],[f114]) ).
fof(f203,plain,
! [X0] :
( ~ less_or_equal(X0,n1)
| less(X0,n2) ),
inference(cnf_transformation,[],[f114]) ).
fof(f204,plain,
! [X0] :
( ~ less(X0,n3)
| less_or_equal(X0,n2) ),
inference(cnf_transformation,[],[f115]) ).
fof(f205,plain,
! [X0] :
( ~ less_or_equal(X0,n2)
| less(X0,n3) ),
inference(cnf_transformation,[],[f115]) ).
fof(f206,plain,
! [X0] :
( ~ less(X0,n4)
| less_or_equal(X0,n3) ),
inference(cnf_transformation,[],[f116]) ).
fof(f207,plain,
! [X0] :
( ~ less_or_equal(X0,n3)
| less(X0,n4) ),
inference(cnf_transformation,[],[f116]) ).
fof(f218,plain,
! [X0,X1] :
( ~ less(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f123]) ).
fof(f219,plain,
! [X0,X1] :
( ~ less(X0,X1)
| ~ less(X1,X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f220,plain,
! [X0,X1] :
( X0 = X1
| less(X1,X0)
| less(X0,X1) ),
inference(cnf_transformation,[],[f123]) ).
fof(f221,plain,
holdsAt(waterLevel(n0),n0),
inference(cnf_transformation,[],[f49]) ).
fof(f222,plain,
~ holdsAt(filling,n0),
inference(cnf_transformation,[],[f50]) ).
fof(f227,plain,
~ holdsAt(filling,n3),
inference(cnf_transformation,[],[f58]) ).
fof(f232,plain,
! [X2,X1] :
( filling != X1
| initiates(tapOn,X1,X2) ),
inference(equality_resolution,[],[f157]) ).
fof(f233,plain,
! [X2] : initiates(tapOn,filling,X2),
inference(equality_resolution,[],[f232]) ).
fof(f234,plain,
! [X2,X1] :
( spilling != X1
| initiates(overflow,X1,X2) ),
inference(equality_resolution,[],[f156]) ).
fof(f235,plain,
! [X2] : initiates(overflow,spilling,X2),
inference(equality_resolution,[],[f234]) ).
fof(f236,plain,
! [X2,X1] :
( filling != X1
| terminates(tapOff,X1,X2) ),
inference(equality_resolution,[],[f163]) ).
fof(f237,plain,
! [X2] : terminates(tapOff,filling,X2),
inference(equality_resolution,[],[f236]) ).
fof(f238,plain,
! [X2,X1] :
( filling != X1
| terminates(overflow,X1,X2) ),
inference(equality_resolution,[],[f162]) ).
fof(f239,plain,
! [X2] : terminates(overflow,filling,X2),
inference(equality_resolution,[],[f238]) ).
fof(f240,plain,
! [X2,X3,X1] :
( waterLevel(X3) != X1
| releases(tapOn,X1,X2) ),
inference(equality_resolution,[],[f166]) ).
fof(f241,plain,
! [X2,X3] : releases(tapOn,waterLevel(X3),X2),
inference(equality_resolution,[],[f240]) ).
fof(f242,plain,
! [X1] :
( n0 != X1
| happens(tapOn,X1) ),
inference(equality_resolution,[],[f174]) ).
fof(f243,plain,
happens(tapOn,n0),
inference(equality_resolution,[],[f242]) ).
fof(f244,plain,
! [X1] :
( ~ holdsAt(filling,X1)
| ~ holdsAt(waterLevel(n3),X1)
| happens(overflow,X1) ),
inference(equality_resolution,[],[f173]) ).
fof(f245,plain,
! [X3,X0,X1] :
( ~ holdsAt(waterLevel(X0),X1)
| trajectory(filling,X1,waterLevel(plus(X0,X3)),X3) ),
inference(equality_resolution,[],[f175]) ).
fof(f247,plain,
! [X1] : less_or_equal(X1,X1),
inference(equality_resolution,[],[f197]) ).
fof(f248,plain,
! [X1] : ~ less(X1,X1),
inference(equality_resolution,[],[f218]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i,X2: $i] :
( happens(sK2(X0,X1,X2),sK3(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] :
( less(X0,sK3(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i] :
( less(sK3(X0,X1,X2),X2)
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f125]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i,X2: $i] :
( terminates(sK2(X0,X1,X2),X1,sK3(X0,X1,X2))
| ~ stoppedIn(X0,X1,X2) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( holdsAt(X2,plus(X1,X3))
| stoppedIn(X1,X0,plus(X1,X3))
| ~ less(n0,X3)
| ~ happens(X4,X1)
| ~ initiates(X4,X0,X1)
| ~ trajectory(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(X1,n1))
| holdsAt(X0,plus(X1,n1))
| happens(sK4(X0,X1),X1)
| ~ holdsAt(X0,X1) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(X1,n1))
| holdsAt(X0,plus(X1,n1))
| terminates(sK4(X0,X1),X0,X1)
| ~ holdsAt(X0,X1) ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i] :
( holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| happens(sK5(X0,X1),X1)
| ~ holdsAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f132]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i] :
( holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| initiates(sK5(X0,X1),X0,X1)
| ~ holdsAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(X1,n1))
| happens(sK6(X0,X1),X1)
| ~ releasedAt(X0,X1) ),
inference(cnf_transformation,[],[f134]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(X1,n1))
| initiates(sK6(X0,X1),X0,X1)
| terminates(sK6(X0,X1),X0,X1)
| ~ releasedAt(X0,X1) ),
inference(cnf_transformation,[],[f133]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,X1)
| happens(sK7(X0,X1),X1)
| ~ releasedAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f136]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,X1)
| releases(sK7(X0,X1),X0,X1)
| ~ releasedAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f135]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i] :
( holdsAt(X1,plus(X2,n1))
| ~ happens(X0,X2)
| ~ initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f137]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ happens(X2,X1)
| ~ terminates(X2,X0,X1)
| ~ holdsAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f138]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i] :
( releasedAt(X1,plus(X2,n1))
| ~ happens(X0,X2)
| ~ releases(X0,X1,X2) ),
inference(cnf_transformation,[],[f139]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ happens(X2,X1)
| ~ initiates(X2,X0,X1)
| ~ releasedAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f141]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ happens(X2,X1)
| ~ terminates(X2,X0,X1)
| ~ releasedAt(X0,plus(X1,n1)) ),
inference(cnf_transformation,[],[f140]) ).
tcf(c_75,plain,
! [X0: $i] : initiates(tapOn,filling,X0),
inference(cnf_transformation,[],[f233]) ).
tcf(c_76,plain,
! [X0: $i] : initiates(overflow,spilling,X0),
inference(cnf_transformation,[],[f235]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i,X2: $i] :
( initiates(X1,X2,X0)
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f154]) ).
tcf(c_83,plain,
! [X0: $i] : terminates(tapOff,filling,X0),
inference(cnf_transformation,[],[f237]) ).
tcf(c_84,plain,
! [X0: $i] : terminates(overflow,filling,X0),
inference(cnf_transformation,[],[f239]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = overflow )
| ( X0 = tapOff )
| ~ terminates(X0,X1,X2) ),
inference(cnf_transformation,[],[f161]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = filling )
| ~ terminates(X0,X1,X2) ),
inference(cnf_transformation,[],[f249]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i] : releases(tapOn,waterLevel(X0),X1),
inference(cnf_transformation,[],[f241]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( waterLevel(sK10(X0,X1)) = X1 )
| ~ releases(X0,X1,X2) ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_92,plain,
happens(tapOn,n0),
inference(cnf_transformation,[],[f243]) ).
tcf(c_93,plain,
! [X0: $i] :
( happens(overflow,X0)
| ~ holdsAt(filling,X0)
| ~ holdsAt(waterLevel(n3),X0) ),
inference(cnf_transformation,[],[f244]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i] :
( holdsAt(waterLevel(n3),X1)
| ( X0 = tapOn )
| ~ happens(X0,X1) ),
inference(cnf_transformation,[],[f172]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i] :
( ( X0 = tapOn )
| ( X0 = overflow )
| ~ happens(X0,X1) ),
inference(cnf_transformation,[],[f170]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i] :
( holdsAt(waterLevel(n3),X1)
| ( X1 = n0 )
| ~ happens(X0,X1) ),
inference(cnf_transformation,[],[f169]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i] :
( holdsAt(filling,X1)
| ( X1 = n0 )
| ~ happens(X0,X1) ),
inference(cnf_transformation,[],[f168]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i,X2: $i] :
( trajectory(filling,X1,waterLevel(plus(X0,X2)),X2)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(cnf_transformation,[],[f245]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = X2 )
| ~ holdsAt(waterLevel(X2),X1)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(cnf_transformation,[],[f176]) ).
tcf(c_104,plain,
overflow != tapOn,
inference(cnf_transformation,[],[f179]) ).
tcf(c_105,plain,
! [X0: $i] : waterLevel(X0) != filling,
inference(cnf_transformation,[],[f180]) ).
tcf(c_109,plain,
plus(n0,n0) = n0,
inference(cnf_transformation,[],[f185]) ).
tcf(c_110,plain,
plus(n0,n1) = n1,
inference(cnf_transformation,[],[f186]) ).
tcf(c_111,plain,
plus(n0,n2) = n2,
inference(cnf_transformation,[],[f187]) ).
tcf(c_113,plain,
plus(n1,n1) = n2,
inference(cnf_transformation,[],[f189]) ).
tcf(c_114,plain,
plus(n1,n2) = n3,
inference(cnf_transformation,[],[f190]) ).
tcf(c_115,plain,
plus(n1,n3) = n4,
inference(cnf_transformation,[],[f191]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i] : plus(X0,X1) = plus(X1,X0),
inference(cnf_transformation,[],[f195]) ).
tcf(c_120,plain,
! [X0: $i,X1: $i] :
( less_or_equal(X0,X1)
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f198]) ).
tcf(c_121,plain,
! [X0: $i] : less_or_equal(X0,X0),
inference(cnf_transformation,[],[f247]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i] :
( less(X0,X1)
| ( X0 = X1 )
| ~ less_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f196]) ).
tcf(c_123,plain,
! [X0: $i] : ~ less(X0,n0),
inference(cnf_transformation,[],[f199]) ).
tcf(c_124,plain,
! [X0: $i] :
( less(X0,n1)
| ~ less_or_equal(X0,n0) ),
inference(cnf_transformation,[],[f201]) ).
tcf(c_125,plain,
! [X0: $i] :
( less_or_equal(X0,n0)
| ~ less(X0,n1) ),
inference(cnf_transformation,[],[f200]) ).
tcf(c_126,plain,
! [X0: $i] :
( less(X0,n2)
| ~ less_or_equal(X0,n1) ),
inference(cnf_transformation,[],[f203]) ).
tcf(c_127,plain,
! [X0: $i] :
( less_or_equal(X0,n1)
| ~ less(X0,n2) ),
inference(cnf_transformation,[],[f202]) ).
tcf(c_128,plain,
! [X0: $i] :
( less(X0,n3)
| ~ less_or_equal(X0,n2) ),
inference(cnf_transformation,[],[f205]) ).
tcf(c_129,plain,
! [X0: $i] :
( less_or_equal(X0,n2)
| ~ less(X0,n3) ),
inference(cnf_transformation,[],[f204]) ).
tcf(c_130,plain,
! [X0: $i] :
( less(X0,n4)
| ~ less_or_equal(X0,n3) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_131,plain,
! [X0: $i] :
( less_or_equal(X0,n3)
| ~ less(X0,n4) ),
inference(cnf_transformation,[],[f206]) ).
tcf(c_142,plain,
! [X0: $i,X1: $i] :
( less(X1,X0)
| less(X0,X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f220]) ).
tcf(c_143,plain,
! [X0: $i,X1: $i] :
( ~ less(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_144,plain,
! [X0: $i] : ~ less(X0,X0),
inference(cnf_transformation,[],[f248]) ).
tcf(c_145,plain,
holdsAt(waterLevel(n0),n0),
inference(cnf_transformation,[],[f221]) ).
tcf(c_146,plain,
~ holdsAt(filling,n0),
inference(cnf_transformation,[],[f222]) ).
tcf(c_151,negated_conjecture,
~ holdsAt(filling,n3),
inference(cnf_transformation,[],[f227]) ).
tcf(c_152,plain,
less_or_equal(n1,n1),
inference(instantiation,[status(thm)],[c_121]) ).
tcf(c_153,plain,
~ less(n1,n1),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_177,plain,
( less(n1,n2)
| ~ less_or_equal(n1,n1) ),
inference(instantiation,[status(thm)],[c_126]) ).
tcf(c_186,plain,
( less(n1,n1)
| ( n1 = n1 ) ),
inference(instantiation,[status(thm)],[c_142]) ).
tcf(c_198,plain,
( happens(overflow,n1)
| ~ holdsAt(filling,n1)
| ~ holdsAt(waterLevel(n3),n1) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_232,plain,
! [X0: $i] :
( less(X0,n1)
| ~ less_or_equal(X0,n0) ),
inference(prop_impl_just,[status(thm)],[c_124]) ).
tcf(c_234,plain,
! [X0: $i] :
( ~ less(X0,n2)
| less_or_equal(X0,n1) ),
inference(prop_impl_just,[status(thm)],[c_127]) ).
tcf(c_235,plain,
! [X0: $i] :
( less_or_equal(X0,n1)
| ~ less(X0,n2) ),
inference(renaming,[status(thm)],[c_234]) ).
tcf(c_238,plain,
! [X0: $i] :
( ~ less(X0,n3)
| less_or_equal(X0,n2) ),
inference(prop_impl_just,[status(thm)],[c_129]) ).
tcf(c_239,plain,
! [X0: $i] :
( less_or_equal(X0,n2)
| ~ less(X0,n3) ),
inference(renaming,[status(thm)],[c_238]) ).
tcf(c_240,plain,
! [X0: $i] :
( less(X0,n3)
| ~ less_or_equal(X0,n2) ),
inference(prop_impl_just,[status(thm)],[c_128]) ).
tcf(c_242,plain,
! [X0: $i] :
( ~ less(X0,n4)
| less_or_equal(X0,n3) ),
inference(prop_impl_just,[status(thm)],[c_131]) ).
tcf(c_243,plain,
! [X0: $i] :
( less_or_equal(X0,n3)
| ~ less(X0,n4) ),
inference(renaming,[status(thm)],[c_242]) ).
tcf(c_244,plain,
! [X0: $i] :
( less(X0,n4)
| ~ less_or_equal(X0,n3) ),
inference(prop_impl_just,[status(thm)],[c_130]) ).
tcf(c_276,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( waterLevel(sK10(X0,X1)) = X1 )
| ~ releases(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_91]) ).
tcf(c_282,plain,
! [X0: $i,X1: $i,X2: $i] :
( trajectory(filling,X1,waterLevel(plus(X0,X2)),X2)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(prop_impl_just,[status(thm)],[c_100]) ).
tcf(c_304,plain,
! [X0: $i,X1: $i] :
( less_or_equal(X0,X1)
| ~ less(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_120]) ).
tcf(c_1018,plain,
plus(n1,n0) = n1,
inference(demodulation,[status(thm)],[c_110,c_119]) ).
tcf(c_1315,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( holdsAt(X5,plus(X1,X6))
| stoppedIn(X1,X0,plus(X1,X6))
| ~ less(n0,X6)
| ~ happens(X7,X1)
| ~ holdsAt(waterLevel(X3),X2)
| ~ initiates(X7,X0,X1)
| ( X4 != X6 )
| ( X1 != X2 )
| ( X0 != filling )
| ( waterLevel(plus(X3,X4)) != X5 ) ),
inference(resolution_lifted,[status(thm)],[c_53,c_282]) ).
tcf(c_1316,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( stoppedIn(X1,filling,plus(X1,X3))
| holdsAt(waterLevel(plus(X0,X3)),plus(X1,X3))
| ~ less(n0,X3)
| ~ happens(X2,X1)
| ~ initiates(X2,filling,X1)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(unflattening,[status(thm)],[c_1315]) ).
tcf(c_1342,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( releasedAt(X0,X1)
| ( waterLevel(sK10(X2,X3)) = X3 )
| ~ releasedAt(X0,plus(X1,n1))
| ( X1 != X4 )
| ( X0 != X3 )
| ( sK7(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_61,c_276]) ).
tcf(c_1343,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,X1)
| ( waterLevel(sK10(sK7(X0,X1),X0)) = X0 )
| ~ releasedAt(X0,plus(X1,n1)) ),
inference(unflattening,[status(thm)],[c_1342]) ).
tcf(c_1376,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( releasedAt(X2,plus(X3,n1))
| ~ happens(X0,X3)
| ( X3 != X4 )
| ( X0 != tapOn )
| ( waterLevel(X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_64,c_89]) ).
tcf(c_1377,plain,
! [X0: $i,X1: $i] :
( releasedAt(waterLevel(X1),plus(X0,n1))
| ~ happens(tapOn,X0) ),
inference(unflattening,[status(thm)],[c_1376]) ).
tcf(c_1803,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ happens(X3,X1)
| ~ holdsAt(X0,plus(X1,n1))
| ( X3 != overflow )
| ( X1 != X2 )
| ( X0 != filling ) ),
inference(resolution_lifted,[status(thm)],[c_63,c_84]) ).
tcf(c_1804,plain,
! [X0: $i] :
( ~ happens(overflow,X0)
| ~ holdsAt(filling,plus(X0,n1)) ),
inference(unflattening,[status(thm)],[c_1803]) ).
tcf(c_2248,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( holdsAt(X0,X1)
| releasedAt(X0,plus(X1,n1))
| stoppedIn(X3,filling,plus(X3,X5))
| holdsAt(waterLevel(plus(X4,X5)),plus(X3,X5))
| ~ less(n0,X5)
| ~ happens(X2,X3)
| ~ holdsAt(waterLevel(X4),X3)
| ~ holdsAt(X0,plus(X1,n1))
| ( X1 != X3 )
| ( X0 != filling )
| ( sK5(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_1316]) ).
tcf(c_2249,plain,
! [X0: $i,X1: $i,X2: $i] :
( holdsAt(filling,X0)
| releasedAt(filling,plus(X0,n1))
| stoppedIn(X0,filling,plus(X0,X2))
| holdsAt(waterLevel(plus(X1,X2)),plus(X0,X2))
| ~ less(n0,X2)
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(filling,plus(X0,n1))
| ~ happens(sK5(filling,X0),X0) ),
inference(unflattening,[status(thm)],[c_2248]) ).
tcf(c_2267,plain,
! [X0: $i,X1: $i,X2: $i] :
( holdsAt(filling,X0)
| releasedAt(filling,plus(X0,n1))
| stoppedIn(X0,filling,plus(X0,X2))
| holdsAt(waterLevel(plus(X1,X2)),plus(X0,X2))
| ~ less(n0,X2)
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(filling,plus(X0,n1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2249,c_56]) ).
tcf(c_2490,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ happens(X3,X1)
| ~ releasedAt(X0,plus(X1,n1))
| ( X3 != tapOn )
| ( X1 != X2 )
| ( X0 != filling ) ),
inference(resolution_lifted,[status(thm)],[c_65,c_75]) ).
tcf(c_2491,plain,
! [X0: $i] :
( ~ happens(tapOn,X0)
| ~ releasedAt(filling,plus(X0,n1)) ),
inference(unflattening,[status(thm)],[c_2490]) ).
tcf(c_2753,plain,
! [X0: $i,X1: $i,X2: $i] :
( less(X1,n3)
| ~ less(X0,X2)
| ( X2 != n2 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_304,c_240]) ).
tcf(c_2754,plain,
! [X0: $i] :
( less(X0,n3)
| ~ less(X0,n2) ),
inference(unflattening,[status(thm)],[c_2753]) ).
tcf(c_2755,plain,
( less(n1,n3)
| ~ less(n1,n2) ),
inference(instantiation,[status(thm)],[c_2754]) ).
tcf(c_2774,plain,
! [X0: $i,X1: $i,X2: $i] :
( less(X1,n4)
| ~ less(X0,X2)
| ( X2 != n3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_304,c_244]) ).
tcf(c_2775,plain,
! [X0: $i] :
( less(X0,n4)
| ~ less(X0,n3) ),
inference(unflattening,[status(thm)],[c_2774]) ).
tcf(c_2776,plain,
( less(n1,n4)
| ~ less(n1,n3) ),
inference(instantiation,[status(thm)],[c_2775]) ).
tcf(c_2947,plain,
! [X0: $i,X1: $i] :
( less(X0,n1)
| ~ less(X1,n2)
| ( n0 != n1 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_232,c_235]) ).
tcf(c_2948,plain,
! [X0: $i] :
( less(X0,n1)
| ~ less(X0,n2)
| ( n0 != n1 ) ),
inference(unflattening,[status(thm)],[c_2947]) ).
tcf(c_2949,plain,
( less(n1,n1)
| ~ less(n1,n2)
| ( n0 != n1 ) ),
inference(instantiation,[status(thm)],[c_2948]) ).
tcf(c_2965,plain,
! [X0: $i,X1: $i] :
( less(X0,n1)
| ~ less(X1,n3)
| ( n0 != n2 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_232,c_239]) ).
tcf(c_2966,plain,
! [X0: $i] :
( less(X0,n1)
| ~ less(X0,n3)
| ( n0 != n2 ) ),
inference(unflattening,[status(thm)],[c_2965]) ).
tcf(c_2967,plain,
( less(n1,n1)
| ~ less(n1,n3)
| ( n0 != n2 ) ),
inference(instantiation,[status(thm)],[c_2966]) ).
tcf(c_2983,plain,
! [X0: $i,X1: $i] :
( less(X0,n1)
| ~ less(X1,n4)
| ( n0 != n3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_232,c_243]) ).
tcf(c_2984,plain,
! [X0: $i] :
( less(X0,n1)
| ~ less(X0,n4)
| ( n0 != n3 ) ),
inference(unflattening,[status(thm)],[c_2983]) ).
tcf(c_2985,plain,
( less(n1,n1)
| ~ less(n1,n4)
| ( n0 != n3 ) ),
inference(instantiation,[status(thm)],[c_2984]) ).
tcf(c_3234,plain,
! [X0: $i,X1: $i] :
( less(X0,n3)
| ~ less(X1,n4)
| ( n3 != n2 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_240,c_243]) ).
tcf(c_3235,plain,
! [X0: $i] :
( less(X0,n3)
| ~ less(X0,n4)
| ( n3 != n2 ) ),
inference(unflattening,[status(thm)],[c_3234]) ).
tcf(c_4063,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( holdsAt(waterLevel(n3),X3)
| releasedAt(X0,plus(X1,n1))
| holdsAt(X0,plus(X1,n1))
| ( X3 = n0 )
| ~ holdsAt(X0,X1)
| ( X1 != X3 )
| ( sK4(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_97,c_54]) ).
tcf(c_4064,plain,
! [X0: $i,X1: $i] :
( holdsAt(waterLevel(n3),X1)
| releasedAt(X0,plus(X1,n1))
| holdsAt(X0,plus(X1,n1))
| ( X1 = n0 )
| ~ holdsAt(X0,X1) ),
inference(unflattening,[status(thm)],[c_4063]) ).
tcf(c_4363,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( releasedAt(X0,X1)
| holdsAt(waterLevel(n3),X3)
| ( X3 = n0 )
| ~ releasedAt(X0,plus(X1,n1))
| ( X1 != X3 )
| ( sK7(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_97,c_60]) ).
tcf(c_4364,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,X1)
| holdsAt(waterLevel(n3),X1)
| ( X1 = n0 )
| ~ releasedAt(X0,plus(X1,n1)) ),
inference(unflattening,[status(thm)],[c_4363]) ).
tcf(c_5381,plain,
! [X0: $i,X1: $i] :
( releasedAt(waterLevel(X1),plus(X0,n1))
| ~ happens(tapOn,X0) ),
inference(prop_impl_just,[status(thm)],[c_1377]) ).
tcf(c_9975,negated_conjecture,
~ holdsAt(filling,n3),
inference(demodulation,[status(thm)],[c_151]) ).
tcf(c_9976,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_9978,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_9981,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( less(X0,X2)
| ~ less(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_9984,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( holdsAt(X0,X2)
| ~ holdsAt(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_9985,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( initiates(X0,X2,X4)
| ~ initiates(X1,X3,X4)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_9987,plain,
! [X0: $i,X1: $i] :
( ( waterLevel(X0) = waterLevel(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_9991,plain,
! [X0: $i,X1: $i,X2: $i] :
( less_or_equal(X2,X0)
| ~ less_or_equal(X2,X1)
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_11914,plain,
! [X0: $i] :
( ( filling = filling )
| ~ terminates(tapOff,filling,X0) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_12009,plain,
( holdsAt(filling,n0)
| ( n0 = n0 )
| ~ happens(tapOn,n0) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_12014,plain,
! [X0: $i] :
( holdsAt(X0,plus(n0,n1))
| ~ happens(tapOn,n0)
| ~ initiates(tapOn,X0,n0) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_12020,plain,
! [X0: $i,X1: $i] :
( releasedAt(waterLevel(X1),plus(n1,X0))
| ~ happens(tapOn,X0) ),
inference(superposition,[status(thm)],[c_119,c_5381]) ).
tcf(c_12071,plain,
~ less(n3,n3),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_12073,plain,
~ less(n4,n4),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_12074,plain,
( less(n4,n4)
| ~ less_or_equal(n4,n3) ),
inference(instantiation,[status(thm)],[c_130]) ).
tcf(c_12389,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| happens(sK6(X0,n1),n1)
| ~ releasedAt(X0,n1) ),
inference(superposition,[status(thm)],[c_113,c_58]) ).
tcf(c_12390,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(n1,X1))
| happens(sK6(X0,X1),X1)
| ~ releasedAt(X0,X1) ),
inference(superposition,[status(thm)],[c_119,c_58]) ).
tcf(c_12445,plain,
! [X0: $i] :
( releasedAt(X0,n1)
| happens(sK7(X0,n1),n1)
| ~ releasedAt(X0,n2) ),
inference(superposition,[status(thm)],[c_113,c_60]) ).
tcf(c_12446,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,X1)
| happens(sK7(X0,X1),X1)
| ~ releasedAt(X0,plus(n1,X1)) ),
inference(superposition,[status(thm)],[c_119,c_60]) ).
tcf(c_12501,plain,
! [X0: $i] :
( releasedAt(waterLevel(X0),n1)
| ~ happens(tapOn,n0) ),
inference(superposition,[status(thm)],[c_1018,c_12020]) ).
tcf(c_12503,plain,
! [X0: $i] : releasedAt(waterLevel(X0),n1),
inference(forward_subsumption_resolution,[status(thm)],[c_12501,c_92]) ).
tcf(c_12517,plain,
! [X0: $i] :
( holdsAt(filling,plus(X0,n1))
| ~ happens(tapOn,X0) ),
inference(superposition,[status(thm)],[c_75,c_62]) ).
tcf(c_12562,plain,
! [X0: $i,X1: $i] :
( ~ holdsAt(X1,n2)
| ~ happens(X0,n1)
| ~ terminates(X0,X1,n1) ),
inference(superposition,[status(thm)],[c_113,c_63]) ).
tcf(c_12638,plain,
! [X0: $i] :
( holdsAt(filling,plus(n1,X0))
| ~ happens(tapOn,X0) ),
inference(superposition,[status(thm)],[c_119,c_12517]) ).
tcf(c_12640,plain,
! [X0: $i,X1: $i] :
( ~ happens(tapOn,X1)
| ~ happens(X0,X1)
| ~ terminates(X0,filling,X1) ),
inference(superposition,[status(thm)],[c_12517,c_63]) ).
tcf(c_12723,plain,
! [X0: $i,X1: $i,X2: $i] :
( happens(sK6(X1,X2),X2)
| ~ releasedAt(X1,X2)
| ~ happens(X0,X2)
| ~ initiates(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_58,c_65]) ).
tcf(c_12726,plain,
! [X0: $i,X1: $i] :
( ~ releasedAt(X1,n2)
| ~ happens(X0,n1)
| ~ initiates(X0,X1,n1) ),
inference(superposition,[status(thm)],[c_113,c_65]) ).
tcf(c_12727,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ happens(X2,X1)
| ~ initiates(X2,X0,X1)
| ~ releasedAt(X0,plus(n1,X1)) ),
inference(superposition,[status(thm)],[c_119,c_65]) ).
tcf(c_12829,plain,
( holdsAt(filling,n1)
| ~ happens(tapOn,n0) ),
inference(superposition,[status(thm)],[c_1018,c_12638]) ).
tcf(c_12831,plain,
holdsAt(filling,n1),
inference(forward_subsumption_resolution,[status(thm)],[c_12829,c_92]) ).
tcf(c_12863,plain,
! [X0: $i] :
( ~ happens(tapOn,n0)
| ~ initiates(tapOn,X0,n0)
| ~ releasedAt(X0,plus(n0,n1)) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_12908,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(X0,plus(n1,n1))
| happens(sK4(X0,n1),n1)
| ~ holdsAt(X0,n1) ),
inference(superposition,[status(thm)],[c_113,c_54]) ).
tcf(c_12909,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(n1,X1))
| holdsAt(X0,plus(X1,n1))
| happens(sK4(X0,X1),X1)
| ~ holdsAt(X0,X1) ),
inference(superposition,[status(thm)],[c_119,c_54]) ).
tcf(c_12920,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(X0,n2)
| happens(sK4(X0,n1),n1)
| ~ holdsAt(X0,n1) ),
inference(light_normalisation,[status(thm)],[c_12908,c_113]) ).
tcf(c_12985,plain,
! [X0: $i,X1: $i,X2: $i] :
( less(X0,X2)
| ~ less(X1,n3)
| ( X2 != n3 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_9981]) ).
tcf(c_12986,plain,
( less(n1,n1)
| ~ less(n1,n3)
| ( n1 != n3 )
| ( n1 != n1 ) ),
inference(instantiation,[status(thm)],[c_12985]) ).
tcf(c_13354,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(X1,n1))
| initiates(sK6(X0,X1),X0,X1)
| ( X0 = filling )
| ~ releasedAt(X0,X1) ),
inference(superposition,[status(thm)],[c_59,c_88]) ).
tcf(c_13355,plain,
! [X0: $i] :
( releasedAt(filling,plus(X0,n1))
| initiates(sK6(filling,X0),filling,X0)
| ~ releasedAt(filling,X0)
| ~ happens(tapOn,X0)
| ~ happens(sK6(filling,X0),X0) ),
inference(superposition,[status(thm)],[c_59,c_12640]) ).
tcf(c_13574,plain,
! [X0: $i] :
( less_or_equal(n4,n3)
| ~ less_or_equal(n4,X0)
| ( n3 != X0 ) ),
inference(instantiation,[status(thm)],[c_9991]) ).
tcf(c_13734,plain,
( holdsAt(filling,plus(n0,n1))
| ~ happens(tapOn,n0)
| ~ initiates(tapOn,filling,n0) ),
inference(instantiation,[status(thm)],[c_12014]) ).
tcf(c_13735,plain,
initiates(tapOn,filling,n0),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_13864,plain,
! [X0: $i] :
( ~ happens(sK6(filling,X0),X0)
| ~ happens(tapOn,X0)
| ~ releasedAt(filling,X0)
| initiates(sK6(filling,X0),filling,X0) ),
inference(global_subsumption_just,[status(thm)],[c_13355,c_2491,c_13355]) ).
tcf(c_13865,plain,
! [X0: $i] :
( initiates(sK6(filling,X0),filling,X0)
| ~ releasedAt(filling,X0)
| ~ happens(tapOn,X0)
| ~ happens(sK6(filling,X0),X0) ),
inference(renaming,[status(thm)],[c_13864]) ).
tcf(c_14446,plain,
! [X0: $i,X1: $i] :
( ( filling = X0 )
| ( filling != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_9978]) ).
tcf(c_15003,plain,
! [X0: $i,X1: $i] :
( less(X0,n3)
| ~ less(X1,n3)
| ( n3 != n3 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_12985]) ).
tcf(c_15004,plain,
n3 = n3,
inference(instantiation,[status(thm)],[c_9976]) ).
tcf(c_21641,plain,
( ~ happens(tapOn,n0)
| ~ initiates(tapOn,filling,n0)
| ~ releasedAt(filling,plus(n0,n1)) ),
inference(instantiation,[status(thm)],[c_12863]) ).
tcf(c_21851,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(waterLevel(n3),n1)
| ( n0 = n1 )
| ~ releasedAt(X0,n1) ),
inference(superposition,[status(thm)],[c_12389,c_97]) ).
tcf(c_21930,plain,
( holdsAt(filling,n0)
| releasedAt(filling,plus(n0,n1))
| initiates(sK5(filling,n0),filling,n0)
| ~ holdsAt(filling,plus(n0,n1)) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_21931,plain,
( holdsAt(filling,n0)
| releasedAt(filling,plus(n0,n1))
| happens(sK5(filling,n0),n0)
| ~ holdsAt(filling,plus(n0,n1)) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_22199,plain,
! [X0: $i] :
( releasedAt(X0,n3)
| happens(sK6(X0,n2),n2)
| ~ releasedAt(X0,n2) ),
inference(superposition,[status(thm)],[c_114,c_12390]) ).
tcf(c_22200,plain,
! [X0: $i] :
( releasedAt(X0,n4)
| happens(sK6(X0,n3),n3)
| ~ releasedAt(X0,n3) ),
inference(superposition,[status(thm)],[c_115,c_12390]) ).
tcf(c_22298,plain,
! [X0: $i] :
( less_or_equal(n4,X0)
| ~ less(n4,X0) ),
inference(instantiation,[status(thm)],[c_120]) ).
tcf(c_22416,plain,
! [X0: $i] :
( releasedAt(X0,n3)
| holdsAt(waterLevel(n3),n2)
| ( n0 = n2 )
| ~ releasedAt(X0,n2) ),
inference(superposition,[status(thm)],[c_22199,c_97]) ).
tcf(c_22420,plain,
! [X0: $i] :
( holdsAt(filling,n2)
| releasedAt(X0,n3)
| ( n0 = n2 )
| ~ releasedAt(X0,n2) ),
inference(superposition,[status(thm)],[c_22199,c_98]) ).
tcf(c_22586,plain,
! [X0: $i] :
( holdsAt(filling,n3)
| releasedAt(X0,n4)
| ( n0 = n3 )
| ~ releasedAt(X0,n3) ),
inference(superposition,[status(thm)],[c_22200,c_98]) ).
tcf(c_22588,plain,
! [X0: $i] :
( releasedAt(X0,n4)
| ( n0 = n3 )
| ~ releasedAt(X0,n3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_22586,c_9975]) ).
tcf(c_22715,plain,
! [X0: $i] :
( releasedAt(X0,n4)
| ~ releasedAt(X0,n3) ),
inference(global_subsumption_just,[status(thm)],[c_22588,c_152,c_153,c_177,c_2755,c_2776,c_2985,c_22588]) ).
tcf(c_23321,plain,
! [X0: $i] :
( releasedAt(X0,n1)
| holdsAt(waterLevel(n3),n1)
| ( n0 = n1 )
| ~ releasedAt(X0,n2) ),
inference(superposition,[status(thm)],[c_12445,c_97]) ).
tcf(c_23362,plain,
! [X0: $i] :
( ( filling = X0 )
| ( filling != filling )
| ( X0 != filling ) ),
inference(instantiation,[status(thm)],[c_14446]) ).
tcf(c_23584,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| happens(sK7(X0,n2),n2)
| ~ releasedAt(X0,n3) ),
inference(superposition,[status(thm)],[c_114,c_12446]) ).
tcf(c_23585,plain,
! [X0: $i] :
( releasedAt(X0,n3)
| happens(sK7(X0,n3),n3)
| ~ releasedAt(X0,n4) ),
inference(superposition,[status(thm)],[c_115,c_12446]) ).
tcf(c_24171,plain,
! [X0: $i] :
( less(n3,n3)
| ~ less(X0,n3)
| ( n3 != n3 )
| ( n3 != X0 ) ),
inference(instantiation,[status(thm)],[c_15003]) ).
tcf(c_24204,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(waterLevel(n3),n2)
| ( n0 = n2 )
| ~ releasedAt(X0,n3) ),
inference(superposition,[status(thm)],[c_23584,c_97]) ).
tcf(c_24208,plain,
! [X0: $i] :
( holdsAt(filling,n2)
| releasedAt(X0,n2)
| ( n0 = n2 )
| ~ releasedAt(X0,n3) ),
inference(superposition,[status(thm)],[c_23584,c_98]) ).
tcf(c_24248,plain,
! [X0: $i,X1: $i] :
( ( n3 = X0 )
| ( n3 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_9978]) ).
tcf(c_24595,plain,
! [X0: $i] :
( holdsAt(filling,n3)
| releasedAt(X0,n3)
| ( n0 = n3 )
| ~ releasedAt(X0,n4) ),
inference(superposition,[status(thm)],[c_23585,c_98]) ).
tcf(c_24597,plain,
! [X0: $i] :
( releasedAt(X0,n3)
| ( n0 = n3 )
| ~ releasedAt(X0,n4) ),
inference(forward_subsumption_resolution,[status(thm)],[c_24595,c_9975]) ).
tcf(c_24649,plain,
! [X0: $i] :
( releasedAt(X0,n3)
| ~ releasedAt(X0,n4) ),
inference(global_subsumption_just,[status(thm)],[c_24597,c_152,c_153,c_177,c_2755,c_2776,c_2985,c_24597]) ).
tcf(c_24730,plain,
! [X0: $i] :
( releasedAt(X0,plus(n1,n1))
| initiates(sK6(X0,n1),X0,n1)
| ~ releasedAt(X0,n1)
| ~ holdsAt(X0,n2)
| ~ happens(sK6(X0,n1),n1) ),
inference(superposition,[status(thm)],[c_59,c_12562]) ).
tcf(c_24732,plain,
( ~ holdsAt(filling,n2)
| ~ happens(overflow,n1) ),
inference(superposition,[status(thm)],[c_84,c_12562]) ).
tcf(c_24738,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| initiates(sK6(X0,n1),X0,n1)
| ~ releasedAt(X0,n1)
| ~ holdsAt(X0,n2)
| ~ happens(sK6(X0,n1),n1) ),
inference(light_normalisation,[status(thm)],[c_24730,c_113]) ).
tcf(c_24825,plain,
( ~ releasedAt(spilling,n2)
| ~ happens(overflow,n1) ),
inference(superposition,[status(thm)],[c_76,c_12726]) ).
tcf(c_28388,plain,
! [X0: $i] :
( happens(sK6(filling,X0),X0)
| ~ releasedAt(filling,X0)
| ~ happens(tapOn,X0) ),
inference(superposition,[status(thm)],[c_75,c_12723]) ).
tcf(c_28808,plain,
! [X0: $i] :
( initiates(sK6(filling,X0),filling,X0)
| ~ releasedAt(filling,X0)
| ~ happens(tapOn,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_13865,c_28388]) ).
tcf(c_29038,plain,
! [X0: $i] :
( holdsAt(filling,n2)
| releasedAt(X0,n3)
| ~ releasedAt(X0,n2) ),
inference(global_subsumption_just,[status(thm)],[c_22420,c_152,c_153,c_177,c_2755,c_2967,c_22420]) ).
tcf(c_29053,plain,
! [X0: $i] :
( holdsAt(filling,n2)
| releasedAt(X0,n2)
| ~ releasedAt(X0,n3) ),
inference(global_subsumption_just,[status(thm)],[c_24208,c_152,c_153,c_177,c_2755,c_2967,c_24208]) ).
tcf(c_30138,plain,
! [X0: $i,X1: $i] :
( ~ releasedAt(X1,n1)
| ~ happens(X0,n0)
| ~ initiates(X0,X1,n0) ),
inference(superposition,[status(thm)],[c_1018,c_12727]) ).
tcf(c_30350,plain,
! [X0: $i] :
( holdsAt(X0,n0)
| releasedAt(X0,plus(n0,n1))
| ~ releasedAt(X0,n1)
| ~ holdsAt(X0,plus(n0,n1))
| ~ happens(sK5(X0,n0),n0) ),
inference(superposition,[status(thm)],[c_57,c_30138]) ).
tcf(c_30351,plain,
( ~ releasedAt(filling,n1)
| ~ happens(tapOn,n0) ),
inference(superposition,[status(thm)],[c_75,c_30138]) ).
tcf(c_30356,plain,
~ releasedAt(filling,n1),
inference(forward_subsumption_resolution,[status(thm)],[c_30351,c_92]) ).
tcf(c_30674,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(X0,n2)
| holdsAt(waterLevel(n3),n1)
| ( n0 = n1 )
| ~ holdsAt(X0,n1) ),
inference(superposition,[status(thm)],[c_12920,c_97]) ).
tcf(c_31041,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(waterLevel(n3),n1)
| ~ releasedAt(X0,n1) ),
inference(global_subsumption_just,[status(thm)],[c_21851,c_152,c_153,c_177,c_2949,c_21851]) ).
tcf(c_31055,plain,
! [X0: $i] :
( holdsAt(filling,n2)
| releasedAt(X0,n3)
| holdsAt(waterLevel(n3),n1)
| ~ releasedAt(X0,n1) ),
inference(superposition,[status(thm)],[c_31041,c_29038]) ).
tcf(c_31060,plain,
! [X0: $i] :
( happens(overflow,n1)
| releasedAt(X0,n2)
| ~ holdsAt(filling,n1)
| ~ releasedAt(X0,n1) ),
inference(superposition,[status(thm)],[c_31041,c_93]) ).
tcf(c_31065,plain,
! [X0: $i] :
( happens(overflow,n1)
| releasedAt(X0,n2)
| ~ releasedAt(X0,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_31060,c_12831]) ).
tcf(c_31527,plain,
! [X0: $i] :
( releasedAt(X0,n1)
| holdsAt(waterLevel(n3),n1)
| ~ releasedAt(X0,n2) ),
inference(global_subsumption_just,[status(thm)],[c_23321,c_152,c_153,c_177,c_2949,c_23321]) ).
tcf(c_31641,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(waterLevel(n3),n2)
| ~ releasedAt(X0,n3) ),
inference(global_subsumption_just,[status(thm)],[c_24204,c_152,c_153,c_177,c_2755,c_2967,c_24204]) ).
tcf(c_31662,plain,
! [X0: $i] :
( happens(overflow,n2)
| releasedAt(X0,n2)
| ~ holdsAt(filling,n2)
| ~ releasedAt(X0,n3) ),
inference(superposition,[status(thm)],[c_31641,c_93]) ).
tcf(c_32431,plain,
! [X0: $i] :
( happens(overflow,n2)
| releasedAt(X0,n2)
| ~ releasedAt(X0,n3) ),
inference(global_subsumption_just,[status(thm)],[c_31662,c_29053,c_31662]) ).
tcf(c_32675,plain,
! [X0: $i] :
( holdsAt(filling,n2)
| releasedAt(X0,n4)
| holdsAt(waterLevel(n3),n1)
| ~ releasedAt(X0,n1) ),
inference(superposition,[status(thm)],[c_31055,c_22715]) ).
tcf(c_43666,plain,
! [X0: $i] :
( holdsAt(X0,plus(n0,n1))
| ~ happens(sK5(filling,n0),n0)
| ~ initiates(sK5(filling,n0),X0,n0) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_43669,plain,
! [X0: $i] :
( ~ happens(sK5(filling,n0),n0)
| ~ releasedAt(X0,plus(n0,n1))
| ~ initiates(sK5(filling,n0),X0,n0) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_54868,plain,
! [X0: $i] :
( releasedAt(X0,n1)
| ( waterLevel(sK10(sK7(X0,n1),X0)) = X0 )
| ~ releasedAt(X0,n2) ),
inference(superposition,[status(thm)],[c_113,c_1343]) ).
tcf(c_62843,plain,
! [X0: $i] :
( ( n3 = X0 )
| ( n3 != n3 )
| ( X0 != n3 ) ),
inference(instantiation,[status(thm)],[c_24248]) ).
tcf(c_63354,plain,
! [X0: $i] :
( holdsAt(X0,n0)
| releasedAt(X0,plus(n0,n1))
| happens(sK5(X0,n0),n0)
| ~ holdsAt(X0,plus(n0,n1)) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_80740,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(X0,n2)
| holdsAt(waterLevel(n3),n1)
| ~ holdsAt(X0,n1) ),
inference(global_subsumption_just,[status(thm)],[c_30674,c_152,c_153,c_177,c_2949,c_30674]) ).
tcf(c_80758,plain,
! [X0: $i] :
( releasedAt(X0,n1)
| holdsAt(X0,n2)
| holdsAt(waterLevel(n3),n1)
| ~ holdsAt(X0,n1) ),
inference(superposition,[status(thm)],[c_80740,c_31527]) ).
tcf(c_80789,plain,
! [X0: $i] :
( happens(overflow,n1)
| releasedAt(X0,n2)
| holdsAt(X0,n2)
| ~ holdsAt(filling,n1)
| ~ holdsAt(X0,n1) ),
inference(superposition,[status(thm)],[c_80740,c_93]) ).
tcf(c_80830,plain,
! [X0: $i] :
( happens(overflow,n1)
| releasedAt(X0,n2)
| holdsAt(X0,n2)
| ~ holdsAt(X0,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_80789,c_12831]) ).
tcf(c_81985,plain,
( releasedAt(filling,n2)
| holdsAt(filling,n2)
| happens(overflow,n1) ),
inference(superposition,[status(thm)],[c_12831,c_80830]) ).
tcf(c_83148,plain,
( releasedAt(filling,n1)
| holdsAt(filling,n2)
| happens(overflow,n1)
| ( waterLevel(sK10(sK7(filling,n1),filling)) = filling ) ),
inference(superposition,[status(thm)],[c_81985,c_54868]) ).
tcf(c_83187,plain,
( holdsAt(filling,n2)
| happens(overflow,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_83148,c_30356,c_105]) ).
tcf(c_83195,plain,
( holdsAt(filling,n2)
| holdsAt(waterLevel(n3),n1)
| ( overflow = tapOn ) ),
inference(superposition,[status(thm)],[c_83187,c_94]) ).
tcf(c_83215,plain,
( holdsAt(filling,n2)
| ~ releasedAt(spilling,n2) ),
inference(superposition,[status(thm)],[c_83187,c_24825]) ).
tcf(c_83236,plain,
( holdsAt(filling,n2)
| holdsAt(waterLevel(n3),n1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_83195,c_104]) ).
tcf(c_85749,plain,
! [X0: $i,X1: $i,X2: $i] :
( holdsAt(X1,plus(X2,n1))
| happens(sK4(X1,X2),X2)
| ~ holdsAt(X1,X2)
| ~ happens(X0,X2)
| ~ terminates(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_54,c_66]) ).
tcf(c_86093,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(X1,n1))
| initiates(sK6(X0,X1),X0,X1)
| ( sK6(X0,X1) = overflow )
| ( sK6(X0,X1) = tapOff )
| ~ releasedAt(X0,X1) ),
inference(superposition,[status(thm)],[c_59,c_85]) ).
tcf(c_125666,plain,
! [X0: $i] :
( releasedAt(X0,n3)
| holdsAt(X0,plus(n2,n1))
| happens(sK4(X0,n2),n2)
| ~ holdsAt(X0,n2) ),
inference(superposition,[status(thm)],[c_114,c_12909]) ).
tcf(c_125875,plain,
! [X0: $i] :
( releasedAt(X0,n3)
| holdsAt(X0,n3)
| happens(sK4(X0,n2),n2)
| ~ holdsAt(X0,n2) ),
inference(demodulation,[status(thm)],[c_125666,c_114,c_119]) ).
tcf(c_125888,plain,
! [X0: $i] :
( releasedAt(X0,n3)
| holdsAt(X0,n3)
| holdsAt(waterLevel(n3),n2)
| ( n0 = n2 )
| ~ holdsAt(X0,n2) ),
inference(superposition,[status(thm)],[c_125875,c_97]) ).
tcf(c_147378,plain,
! [X0: $i,X1: $i,X2: $i] :
( holdsAt(X0,X1)
| ~ holdsAt(filling,X2)
| ( X1 != X2 )
| ( X0 != filling ) ),
inference(instantiation,[status(thm)],[c_9984]) ).
tcf(c_147611,plain,
! [X0: $i,X1: $i] :
( holdsAt(filling,X0)
| ~ holdsAt(filling,X1)
| ( filling != filling )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_147378]) ).
tcf(c_148454,plain,
! [X0: $i] :
( holdsAt(filling,n0)
| ~ holdsAt(filling,X0)
| ( filling != filling )
| ( n0 != X0 ) ),
inference(instantiation,[status(thm)],[c_147611]) ).
tcf(c_160824,plain,
sK5(filling,n0) = sK5(filling,n0),
inference(instantiation,[status(thm)],[c_9976]) ).
tcf(c_165942,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(X1,n1))
| holdsAt(X0,plus(X1,n1))
| ( X0 = filling )
| ~ releasedAt(X0,X1)
| ~ happens(sK6(X0,X1),X1) ),
inference(superposition,[status(thm)],[c_13354,c_62]) ).
tcf(c_181311,plain,
! [X0: $i,X1: $i,X2: $i] :
( happens(sK4(X1,X2),X2)
| ~ holdsAt(X1,X2)
| ~ happens(X0,X2)
| ~ terminates(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_85749,c_63]) ).
tcf(c_181328,plain,
! [X0: $i] :
( happens(sK4(filling,X0),X0)
| ~ holdsAt(filling,X0)
| ~ happens(overflow,X0) ),
inference(superposition,[status(thm)],[c_84,c_181311]) ).
tcf(c_182002,plain,
! [X0: $i] :
( holdsAt(waterLevel(n3),X0)
| ( X0 = n0 )
| ~ holdsAt(filling,X0)
| ~ happens(overflow,X0) ),
inference(superposition,[status(thm)],[c_181328,c_97]) ).
tcf(c_199447,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(X1,n1))
| holdsAt(X0,plus(X1,n1))
| ( sK6(X0,X1) = overflow )
| ( sK6(X0,X1) = tapOff )
| ~ releasedAt(X0,X1)
| ~ happens(sK6(X0,X1),X1) ),
inference(superposition,[status(thm)],[c_86093,c_62]) ).
tcf(c_201124,plain,
! [X0: $i] :
( releasedAt(X0,n1)
| happens(sK7(X0,n1),n1)
| ~ releasedAt(X0,n2) ),
inference(superposition,[status(thm)],[c_113,c_60]) ).
tcf(c_201125,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,X1)
| happens(sK7(X0,X1),X1)
| ~ releasedAt(X0,plus(n1,X1)) ),
inference(superposition,[status(thm)],[c_119,c_60]) ).
tcf(c_201144,plain,
! [X0: $i] :
( holdsAt(filling,plus(X0,n1))
| ~ happens(tapOn,X0) ),
inference(superposition,[status(thm)],[c_75,c_62]) ).
tcf(c_201298,plain,
! [X0: $i,X1: $i] :
( ~ happens(tapOn,X1)
| ~ happens(X0,X1)
| ~ terminates(X0,filling,X1) ),
inference(superposition,[status(thm)],[c_201144,c_63]) ).
tcf(c_201334,plain,
! [X0: $i,X1: $i] :
( ~ releasedAt(X1,n2)
| ~ happens(X0,n1)
| ~ initiates(X0,X1,n1) ),
inference(superposition,[status(thm)],[c_113,c_65]) ).
tcf(c_201620,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(n1,X1))
| holdsAt(X0,plus(X1,n1))
| happens(sK4(X0,X1),X1)
| ~ holdsAt(X0,X1) ),
inference(superposition,[status(thm)],[c_119,c_54]) ).
tcf(c_202024,plain,
! [X0: $i] :
( releasedAt(filling,plus(X0,n1))
| initiates(sK6(filling,X0),filling,X0)
| ~ releasedAt(filling,X0)
| ~ happens(tapOn,X0)
| ~ happens(sK6(filling,X0),X0) ),
inference(superposition,[status(thm)],[c_59,c_201298]) ).
tcf(c_202329,plain,
! [X0: $i] :
( ~ happens(tapOn,X0)
| ~ releasedAt(filling,X0)
| initiates(sK6(filling,X0),filling,X0) ),
inference(global_subsumption_just,[status(thm)],[c_202024,c_28808]) ).
tcf(c_202330,plain,
! [X0: $i] :
( initiates(sK6(filling,X0),filling,X0)
| ~ releasedAt(filling,X0)
| ~ happens(tapOn,X0) ),
inference(renaming,[status(thm)],[c_202329]) ).
tcf(c_208821,plain,
! [X0: $i] :
( releasedAt(X0,n1)
| holdsAt(waterLevel(n3),n1)
| ( n0 = n1 )
| ~ releasedAt(X0,n2) ),
inference(superposition,[status(thm)],[c_201124,c_97]) ).
tcf(c_209373,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| happens(sK7(X0,n2),n2)
| ~ releasedAt(X0,n3) ),
inference(superposition,[status(thm)],[c_114,c_201125]) ).
tcf(c_210123,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(waterLevel(n3),n2)
| ( n0 = n2 )
| ~ releasedAt(X0,n3) ),
inference(superposition,[status(thm)],[c_209373,c_97]) ).
tcf(c_212511,plain,
! [X0: $i,X1: $i] :
( holdsAt(X0,X1)
| ( X1 != n0 )
| ( X0 != waterLevel(n0) ) ),
inference(resolution,[status(thm)],[c_9984,c_145]) ).
tcf(c_213420,plain,
! [X0: $i] :
( holdsAt(waterLevel(n0),X0)
| ( X0 != n0 ) ),
inference(resolution,[status(thm)],[c_212511,c_9976]) ).
tcf(c_213790,plain,
holdsAt(waterLevel(n0),plus(n0,n0)),
inference(resolution,[status(thm)],[c_213420,c_109]) ).
tcf(c_213861,plain,
! [X0: $i] :
( ( n0 = X0 )
| ~ holdsAt(waterLevel(X0),plus(n0,n0)) ),
inference(resolution,[status(thm)],[c_213790,c_101]) ).
tcf(c_213863,plain,
! [X0: $i,X1: $i] :
( holdsAt(X0,X1)
| ( X1 != plus(n0,n0) )
| ( X0 != waterLevel(n0) ) ),
inference(resolution,[status(thm)],[c_213790,c_9984]) ).
tcf(c_214946,plain,
! [X0: $i] :
( holdsAt(X0,plus(n0,n0))
| ( X0 != waterLevel(n0) ) ),
inference(resolution,[status(thm)],[c_213863,c_9976]) ).
tcf(c_220073,plain,
( ~ releasedAt(filling,n2)
| ~ releasedAt(filling,n1)
| ~ happens(tapOn,n1)
| ~ happens(sK6(filling,n1),n1) ),
inference(superposition,[status(thm)],[c_202330,c_201334]) ).
tcf(c_220155,plain,
~ releasedAt(filling,n1),
inference(global_subsumption_just,[status(thm)],[c_220073,c_30356]) ).
tcf(c_229735,plain,
! [X0: $i] :
( releasedAt(X0,n1)
| holdsAt(waterLevel(n3),n1)
| ~ releasedAt(X0,n2) ),
inference(global_subsumption_just,[status(thm)],[c_208821,c_152,c_153,c_177,c_2949,c_23321]) ).
tcf(c_230052,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(waterLevel(n3),n2)
| ~ releasedAt(X0,n3) ),
inference(global_subsumption_just,[status(thm)],[c_210123,c_31641]) ).
tcf(c_230066,plain,
! [X0: $i] :
( releasedAt(X0,n1)
| holdsAt(waterLevel(n3),n2)
| holdsAt(waterLevel(n3),n1)
| ~ releasedAt(X0,n3) ),
inference(superposition,[status(thm)],[c_230052,c_229735]) ).
tcf(c_231121,plain,
! [X0: $i,X1: $i] :
( initiates(X0,X1,n0)
| ~ initiates(sK5(filling,n0),filling,n0)
| ( X1 != filling )
| ( X0 != sK5(filling,n0) ) ),
inference(instantiation,[status(thm)],[c_9985]) ).
tcf(c_254625,plain,
! [X0: $i] :
( holdsAt(waterLevel(X0),plus(n0,n0))
| ( X0 != n0 ) ),
inference(resolution,[status(thm)],[c_9987,c_214946]) ).
tcf(c_255114,plain,
! [X0: $i] :
( releasedAt(X0,n3)
| holdsAt(X0,plus(n2,n1))
| happens(sK4(X0,n2),n2)
| ~ holdsAt(X0,n2) ),
inference(superposition,[status(thm)],[c_114,c_201620]) ).
tcf(c_255423,plain,
! [X0: $i] :
( releasedAt(X0,n3)
| holdsAt(X0,n3)
| happens(sK4(X0,n2),n2)
| ~ holdsAt(X0,n2) ),
inference(demodulation,[status(thm)],[c_255114,c_114,c_119]) ).
tcf(c_255436,plain,
! [X0: $i] :
( releasedAt(X0,n3)
| holdsAt(X0,n3)
| holdsAt(waterLevel(n3),n2)
| ( n0 = n2 )
| ~ holdsAt(X0,n2) ),
inference(superposition,[status(thm)],[c_255423,c_97]) ).
tcf(c_255727,plain,
! [X0: $i] :
( releasedAt(X0,n3)
| holdsAt(X0,n3)
| holdsAt(waterLevel(n3),n2)
| ~ holdsAt(X0,n2) ),
inference(global_subsumption_just,[status(thm)],[c_255436,c_152,c_153,c_177,c_2755,c_2967,c_125888]) ).
tcf(c_256808,plain,
! [X0: $i,X1: $i] :
( less_or_equal(X1,X0)
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_9991,c_121]) ).
tcf(c_261823,plain,
! [X0: $i] :
( ( n0 = X0 )
| ( X0 != n0 ) ),
inference(resolution,[status(thm)],[c_254625,c_213861]) ).
tcf(c_300323,plain,
! [X0: $i] :
( initiates(sK5(filling,n0),X0,n0)
| ~ initiates(sK5(filling,n0),filling,n0)
| ( X0 != filling )
| ( sK5(filling,n0) != sK5(filling,n0) ) ),
inference(instantiation,[status(thm)],[c_231121]) ).
tcf(c_344210,plain,
less_or_equal(n4,plus(n1,n3)),
inference(resolution,[status(thm)],[c_256808,c_115]) ).
tcf(c_363743,plain,
! [X0: $i] :
( less_or_equal(n4,X0)
| ( X0 != plus(n1,n3) ) ),
inference(resolution,[status(thm)],[c_344210,c_9991]) ).
tcf(c_370002,plain,
! [X0: $i,X1: $i] :
( holdsAt(filling,n0)
| ~ holdsAt(X1,X0)
| ( filling != X1 )
| ( n0 != X0 ) ),
inference(instantiation,[status(thm)],[c_9984]) ).
tcf(c_384258,plain,
! [X0: $i] :
( holdsAt(filling,n0)
| ~ holdsAt(X0,n0)
| ( filling != X0 )
| ( n0 != n0 ) ),
inference(instantiation,[status(thm)],[c_370002]) ).
tcf(c_454285,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,X1)
| holdsAt(X0,plus(X1,n1))
| happens(sK7(X0,X1),X1)
| happens(sK4(X0,X1),X1)
| ~ holdsAt(X0,X1) ),
inference(superposition,[status(thm)],[c_54,c_60]) ).
tcf(c_454298,plain,
! [X0: $i] :
( holdsAt(filling,plus(X0,n1))
| ~ happens(tapOn,X0) ),
inference(superposition,[status(thm)],[c_75,c_62]) ).
tcf(c_454334,plain,
! [X0: $i,X1: $i,X2: $i] :
( holdsAt(X1,plus(X2,n1))
| happens(sK4(X1,X2),X2)
| ~ holdsAt(X1,X2)
| ~ happens(X0,X2)
| ~ terminates(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_54,c_66]) ).
tcf(c_454465,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(X1,n1))
| initiates(sK6(X0,X1),X0,X1)
| ( sK6(X0,X1) = overflow )
| ( sK6(X0,X1) = tapOff )
| ~ releasedAt(X0,X1) ),
inference(superposition,[status(thm)],[c_59,c_85]) ).
tcf(c_454486,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(X1,n1))
| holdsAt(X0,plus(X1,n1))
| ( X0 = filling )
| ~ holdsAt(X0,X1) ),
inference(superposition,[status(thm)],[c_55,c_88]) ).
tcf(c_454487,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(X1,n1))
| initiates(sK6(X0,X1),X0,X1)
| ( X0 = filling )
| ~ releasedAt(X0,X1) ),
inference(superposition,[status(thm)],[c_59,c_88]) ).
tcf(c_454556,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sK2(X0,X1,X2) = tapOn )
| ( sK2(X0,X1,X2) = overflow )
| ~ stoppedIn(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_49,c_96]) ).
tcf(c_454661,plain,
! [X0: $i,X1: $i] :
( ~ releasedAt(X1,n2)
| ~ happens(X0,n1)
| ~ initiates(X0,X1,n1) ),
inference(superposition,[status(thm)],[c_113,c_65]) ).
tcf(c_454662,plain,
! [X0: $i,X1: $i] :
( ~ holdsAt(X1,n2)
| ~ happens(X0,n1)
| ~ terminates(X0,X1,n1) ),
inference(superposition,[status(thm)],[c_113,c_63]) ).
tcf(c_454700,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ happens(X2,X1)
| ~ initiates(X2,X0,X1)
| ~ releasedAt(X0,plus(n1,X1)) ),
inference(superposition,[status(thm)],[c_119,c_65]) ).
tcf(c_454701,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ happens(X2,X1)
| ~ terminates(X2,X0,X1)
| ~ holdsAt(X0,plus(n1,X1)) ),
inference(superposition,[status(thm)],[c_119,c_63]) ).
tcf(c_454755,plain,
less(n0,n1),
inference(superposition,[status(thm)],[c_121,c_124]) ).
tcf(c_454760,plain,
! [X0: $i,X1: $i] :
( less_or_equal(sK3(X0,X1,n1),n0)
| ~ stoppedIn(X0,X1,n1) ),
inference(superposition,[status(thm)],[c_51,c_125]) ).
tcf(c_454769,plain,
less_or_equal(n0,n1),
inference(superposition,[status(thm)],[c_454755,c_120]) ).
tcf(c_454775,plain,
! [X0: $i,X1: $i] :
( less_or_equal(sK3(X0,X1,n2),n1)
| ~ stoppedIn(X0,X1,n2) ),
inference(superposition,[status(thm)],[c_51,c_127]) ).
tcf(c_454793,plain,
less(n0,n2),
inference(superposition,[status(thm)],[c_454769,c_126]) ).
tcf(c_454905,plain,
! [X0: $i] :
( less_or_equal(X0,n0)
| less(n1,X0)
| ( X0 = n1 ) ),
inference(superposition,[status(thm)],[c_142,c_125]) ).
tcf(c_455019,plain,
! [X0: $i,X1: $i] :
( releasedAt(waterLevel(X1),plus(n1,X0))
| ~ happens(tapOn,X0) ),
inference(superposition,[status(thm)],[c_119,c_5381]) ).
tcf(c_455052,plain,
! [X0: $i,X1: $i,X2: $i] :
( holdsAt(filling,X0)
| releasedAt(filling,plus(X0,n1))
| stoppedIn(X0,filling,plus(X0,X2))
| holdsAt(waterLevel(plus(X1,X2)),plus(X0,X2))
| ~ less(n0,X2)
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(filling,plus(X0,n1))
| ~ happens(sK5(filling,X0),X0) ),
inference(superposition,[status(thm)],[c_57,c_1316]) ).
tcf(c_455053,plain,
! [X0: $i,X1: $i,X2: $i] :
( stoppedIn(X1,filling,plus(X1,X2))
| holdsAt(waterLevel(plus(X0,X2)),plus(X1,X2))
| ~ less(n0,X2)
| ~ happens(tapOn,X1)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(superposition,[status(thm)],[c_75,c_1316]) ).
tcf(c_455181,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,X1)
| holdsAt(waterLevel(n3),X1)
| holdsAt(X0,plus(X1,n1))
| happens(sK4(X0,X1),X1)
| ( X1 = n0 )
| ~ holdsAt(X0,X1) ),
inference(superposition,[status(thm)],[c_454285,c_97]) ).
tcf(c_455220,plain,
! [X0: $i] :
( holdsAt(filling,plus(n1,X0))
| ~ happens(tapOn,X0) ),
inference(superposition,[status(thm)],[c_119,c_454298]) ).
tcf(c_455222,plain,
! [X0: $i,X1: $i] :
( ~ happens(tapOn,X1)
| ~ happens(X0,X1)
| ~ terminates(X0,filling,X1) ),
inference(superposition,[status(thm)],[c_454298,c_63]) ).
tcf(c_455339,plain,
! [X0: $i,X1: $i,X2: $i] :
( happens(sK4(X1,X2),X2)
| ~ holdsAt(X1,X2)
| ~ happens(X0,X2)
| ~ terminates(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_454334,c_63]) ).
tcf(c_455356,plain,
! [X0: $i] :
( happens(sK4(filling,X0),X0)
| ~ holdsAt(filling,X0)
| ~ happens(overflow,X0) ),
inference(superposition,[status(thm)],[c_84,c_455339]) ).
tcf(c_455908,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(X1,n1))
| holdsAt(X0,plus(X1,n1))
| ( sK6(X0,X1) = overflow )
| ( sK6(X0,X1) = tapOff )
| ~ releasedAt(X0,X1)
| ~ happens(sK6(X0,X1),X1) ),
inference(superposition,[status(thm)],[c_454465,c_62]) ).
tcf(c_455975,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(X0,plus(n1,n1))
| ( X0 = filling )
| ~ holdsAt(X0,n1) ),
inference(superposition,[status(thm)],[c_113,c_454486]) ).
tcf(c_455983,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(X0,n2)
| ( X0 = filling )
| ~ holdsAt(X0,n1) ),
inference(light_normalisation,[status(thm)],[c_455975,c_113]) ).
tcf(c_456036,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(X1,n1))
| holdsAt(X0,plus(X1,n1))
| ( X0 = filling )
| ~ releasedAt(X0,X1)
| ~ happens(sK6(X0,X1),X1) ),
inference(superposition,[status(thm)],[c_454487,c_62]) ).
tcf(c_456978,plain,
! [X0: $i] :
( releasedAt(X0,plus(n1,n1))
| initiates(sK6(X0,n1),X0,n1)
| ~ releasedAt(X0,n1)
| ~ holdsAt(X0,n2)
| ~ happens(sK6(X0,n1),n1) ),
inference(superposition,[status(thm)],[c_59,c_454662]) ).
tcf(c_456984,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| initiates(sK6(X0,n1),X0,n1)
| ~ releasedAt(X0,n1)
| ~ holdsAt(X0,n2)
| ~ happens(sK6(X0,n1),n1) ),
inference(light_normalisation,[status(thm)],[c_456978,c_113]) ).
tcf(c_457467,plain,
! [X0: $i,X1: $i] :
( ~ releasedAt(X1,n1)
| ~ happens(X0,n0)
| ~ initiates(X0,X1,n0) ),
inference(superposition,[status(thm)],[c_1018,c_454700]) ).
tcf(c_457733,plain,
! [X0: $i,X1: $i] :
( ~ holdsAt(X1,n1)
| ~ happens(X0,n0)
| ~ terminates(X0,X1,n0) ),
inference(superposition,[status(thm)],[c_1018,c_454701]) ).
tcf(c_458247,plain,
! [X0: $i,X1: $i] :
( less(sK3(X0,X1,n1),n0)
| ( sK3(X0,X1,n1) = n0 )
| ~ stoppedIn(X0,X1,n1) ),
inference(superposition,[status(thm)],[c_454760,c_122]) ).
tcf(c_458251,plain,
! [X0: $i,X1: $i] :
( ( sK3(X0,X1,n1) = n0 )
| ~ stoppedIn(X0,X1,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_458247,c_123]) ).
tcf(c_458258,plain,
! [X0: $i,X1: $i] :
( less(sK3(X0,X1,n2),n1)
| ( sK3(X0,X1,n2) = n1 )
| ~ stoppedIn(X0,X1,n2) ),
inference(superposition,[status(thm)],[c_454775,c_122]) ).
tcf(c_458556,plain,
! [X0: $i] :
( less(n1,X0)
| less(X0,n0)
| ( X0 = n1 )
| ( X0 = n0 ) ),
inference(superposition,[status(thm)],[c_454905,c_122]) ).
tcf(c_458561,plain,
! [X0: $i] :
( less(n1,X0)
| ( X0 = n1 )
| ( X0 = n0 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_458556,c_123]) ).
tcf(c_458940,plain,
! [X0: $i] :
( releasedAt(waterLevel(X0),n1)
| ~ happens(tapOn,n0) ),
inference(superposition,[status(thm)],[c_1018,c_455019]) ).
tcf(c_458949,plain,
! [X0: $i] : releasedAt(waterLevel(X0),n1),
inference(forward_subsumption_resolution,[status(thm)],[c_458940,c_92]) ).
tcf(c_459069,plain,
! [X0: $i,X1: $i,X2: $i] :
( holdsAt(filling,X0)
| releasedAt(filling,plus(X0,n1))
| stoppedIn(X0,filling,plus(X0,X2))
| holdsAt(waterLevel(plus(X1,X2)),plus(X0,X2))
| ~ less(n0,X2)
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(filling,plus(X0,n1)) ),
inference(global_subsumption_just,[status(thm)],[c_455052,c_2267]) ).
tcf(c_459105,plain,
! [X0: $i,X1: $i,X2: $i] :
( holdsAt(filling,X0)
| releasedAt(filling,plus(X0,n1))
| stoppedIn(X0,filling,plus(X0,X2))
| holdsAt(waterLevel(plus(X2,X1)),plus(X0,X2))
| ~ less(n0,X2)
| ~ holdsAt(waterLevel(X1),X0)
| ~ holdsAt(filling,plus(X0,n1)) ),
inference(superposition,[status(thm)],[c_119,c_459069]) ).
tcf(c_459496,plain,
! [X0: $i,X1: $i,X2: $i] :
( stoppedIn(X1,filling,plus(X2,X1))
| holdsAt(waterLevel(plus(X0,X2)),plus(X1,X2))
| ~ less(n0,X2)
| ~ happens(tapOn,X1)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(superposition,[status(thm)],[c_119,c_455053]) ).
tcf(c_459513,plain,
! [X0: $i] :
( stoppedIn(n0,filling,plus(n0,n2))
| holdsAt(waterLevel(plus(X0,n2)),n2)
| ~ less(n0,n2)
| ~ happens(tapOn,n0)
| ~ holdsAt(waterLevel(X0),n0) ),
inference(superposition,[status(thm)],[c_111,c_455053]) ).
tcf(c_459555,plain,
! [X0: $i] :
( stoppedIn(n0,filling,n2)
| holdsAt(waterLevel(plus(X0,n2)),n2)
| ~ less(n0,n2)
| ~ happens(tapOn,n0)
| ~ holdsAt(waterLevel(X0),n0) ),
inference(light_normalisation,[status(thm)],[c_459513,c_111]) ).
tcf(c_459556,plain,
! [X0: $i] :
( stoppedIn(n0,filling,n2)
| holdsAt(waterLevel(plus(X0,n2)),n2)
| ~ holdsAt(waterLevel(X0),n0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_459555,c_454793,c_92]) ).
tcf(c_460480,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,X1)
| holdsAt(waterLevel(n3),X1)
| holdsAt(X0,plus(X1,n1))
| ~ holdsAt(X0,X1)
| ( X1 = n0 ) ),
inference(global_subsumption_just,[status(thm)],[c_455181,c_4064,c_4364]) ).
tcf(c_460481,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,X1)
| holdsAt(waterLevel(n3),X1)
| holdsAt(X0,plus(X1,n1))
| ( X1 = n0 )
| ~ holdsAt(X0,X1) ),
inference(renaming,[status(thm)],[c_460480]) ).
tcf(c_460494,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,X1)
| holdsAt(waterLevel(n3),X1)
| holdsAt(X0,plus(n1,X1))
| ( X1 = n0 )
| ~ holdsAt(X0,X1) ),
inference(superposition,[status(thm)],[c_119,c_460481]) ).
tcf(c_460647,plain,
( holdsAt(filling,n1)
| ~ happens(tapOn,n0) ),
inference(superposition,[status(thm)],[c_1018,c_455220]) ).
tcf(c_460653,plain,
holdsAt(filling,n1),
inference(forward_subsumption_resolution,[status(thm)],[c_460647,c_92]) ).
tcf(c_460665,plain,
! [X0: $i,X1: $i] :
( ~ stoppedIn(X0,filling,X1)
| ~ happens(tapOn,sK3(X0,filling,X1))
| ~ happens(sK2(X0,filling,X1),sK3(X0,filling,X1)) ),
inference(superposition,[status(thm)],[c_52,c_455222]) ).
tcf(c_461200,plain,
! [X0: $i] :
( holdsAt(waterLevel(n3),X0)
| ( X0 = n0 )
| ~ holdsAt(filling,X0)
| ~ happens(overflow,X0) ),
inference(superposition,[status(thm)],[c_455356,c_97]) ).
tcf(c_465009,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(X1,n1))
| holdsAt(X0,plus(X1,n1))
| ( sK6(X0,X1) = overflow )
| ( sK6(X0,X1) = tapOff )
| ~ releasedAt(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_455908,c_58,c_199447]) ).
tcf(c_465022,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(X0,plus(n1,n1))
| ( sK6(X0,n1) = overflow )
| ( sK6(X0,n1) = tapOff )
| ~ releasedAt(X0,n1) ),
inference(superposition,[status(thm)],[c_113,c_465009]) ).
tcf(c_465035,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(X0,n2)
| ( sK6(X0,n1) = overflow )
| ( sK6(X0,n1) = tapOff )
| ~ releasedAt(X0,n1) ),
inference(light_normalisation,[status(thm)],[c_465022,c_113]) ).
tcf(c_465383,plain,
! [X0: $i,X1: $i] :
( releasedAt(X0,plus(X1,n1))
| holdsAt(X0,plus(X1,n1))
| ( X0 = filling )
| ~ releasedAt(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_456036,c_58,c_165942]) ).
tcf(c_465394,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(X0,plus(n1,n1))
| ( X0 = filling )
| ~ releasedAt(X0,n1) ),
inference(superposition,[status(thm)],[c_113,c_465383]) ).
tcf(c_465407,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(X0,n2)
| ( X0 = filling )
| ~ releasedAt(X0,n1) ),
inference(light_normalisation,[status(thm)],[c_465394,c_113]) ).
tcf(c_468935,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| initiates(sK6(X0,n1),X0,n1)
| ~ releasedAt(X0,n1) ),
inference(global_subsumption_just,[status(thm)],[c_456984,c_92,c_146,c_83,c_11914,c_12009,c_12389,c_13734,c_13735,c_21641,c_21931,c_21930,c_23362,c_24738,c_30350,c_43666,c_43669,c_63354,c_160824,c_300323,c_384258,c_465407]) ).
tcf(c_468953,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(X0,plus(n1,n1))
| ~ releasedAt(X0,n1)
| ~ happens(sK6(X0,n1),n1) ),
inference(superposition,[status(thm)],[c_468935,c_62]) ).
tcf(c_468959,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(X0,n2)
| ~ releasedAt(X0,n1)
| ~ happens(sK6(X0,n1),n1) ),
inference(light_normalisation,[status(thm)],[c_468953,c_113]) ).
tcf(c_469880,plain,
( ~ releasedAt(filling,n1)
| ~ happens(tapOn,n0) ),
inference(superposition,[status(thm)],[c_75,c_457467]) ).
tcf(c_469888,plain,
~ releasedAt(filling,n1),
inference(forward_subsumption_resolution,[status(thm)],[c_469880,c_92]) ).
tcf(c_470344,plain,
( ~ holdsAt(filling,n1)
| ~ happens(overflow,n0) ),
inference(superposition,[status(thm)],[c_84,c_457733]) ).
tcf(c_470345,plain,
~ happens(overflow,n0),
inference(forward_subsumption_resolution,[status(thm)],[c_470344,c_460653]) ).
tcf(c_471900,plain,
! [X0: $i,X1: $i] :
( ( sK3(X0,X1,n2) = n1 )
| ~ stoppedIn(X0,X1,n2)
| ~ less(n1,sK3(X0,X1,n2)) ),
inference(superposition,[status(thm)],[c_458258,c_143]) ).
tcf(c_474376,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( holdsAt(filling,X1)
| releasedAt(filling,plus(X1,n1))
| stoppedIn(X1,filling,plus(X1,X2))
| ( plus(X2,X3) = X0 )
| ~ less(n0,X2)
| ~ holdsAt(waterLevel(X3),X1)
| ~ holdsAt(filling,plus(X1,n1))
| ~ holdsAt(waterLevel(X0),plus(X1,X2)) ),
inference(superposition,[status(thm)],[c_459105,c_101]) ).
tcf(c_477064,plain,
! [X0: $i,X1: $i,X2: $i] :
( stoppedIn(X1,filling,plus(X2,X1))
| holdsAt(waterLevel(plus(X0,X2)),plus(X2,X1))
| ~ less(n0,X2)
| ~ happens(tapOn,X1)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(superposition,[status(thm)],[c_119,c_459496]) ).
tcf(c_478618,plain,
( holdsAt(waterLevel(n2),n2)
| stoppedIn(n0,filling,n2)
| ~ holdsAt(waterLevel(n0),n0) ),
inference(superposition,[status(thm)],[c_111,c_459556]) ).
tcf(c_478639,plain,
( holdsAt(waterLevel(n2),n2)
| stoppedIn(n0,filling,n2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_478618,c_145]) ).
tcf(c_482295,plain,
! [X0: $i,X1: $i] :
( ~ stoppedIn(X0,filling,X1)
| ~ happens(tapOn,sK3(X0,filling,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_460665,c_49]) ).
tcf(c_486925,plain,
! [X0: $i] :
( holdsAt(waterLevel(n3),X0)
| ~ happens(overflow,X0)
| ~ holdsAt(filling,X0) ),
inference(global_subsumption_just,[status(thm)],[c_461200,c_146,c_83,c_11914,c_148454,c_182002,c_261823]) ).
tcf(c_486926,plain,
! [X0: $i] :
( holdsAt(waterLevel(n3),X0)
| ~ holdsAt(filling,X0)
| ~ happens(overflow,X0) ),
inference(renaming,[status(thm)],[c_486925]) ).
tcf(c_495909,plain,
! [X0: $i] :
( ( X0 = plus(n1,n3) )
| ( X0 != n4 ) ),
inference(resolution,[status(thm)],[c_9978,c_115]) ).
tcf(c_499657,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(X0,n2)
| ~ releasedAt(X0,n1) ),
inference(global_subsumption_just,[status(thm)],[c_465035,c_12389,c_468959]) ).
tcf(c_499668,plain,
! [X0: $i] :
( releasedAt(waterLevel(X0),n2)
| holdsAt(waterLevel(X0),n2) ),
inference(superposition,[status(thm)],[c_458949,c_499657]) ).
tcf(c_499689,plain,
( releasedAt(waterLevel(n1),n2)
| holdsAt(waterLevel(n1),n2) ),
inference(instantiation,[status(thm)],[c_499668]) ).
tcf(c_509493,plain,
! [X0: $i,X1: $i] :
( ( sK3(X0,X1,n2) = n1 )
| ( sK3(X0,X1,n2) = n0 )
| ~ stoppedIn(X0,X1,n2) ),
inference(superposition,[status(thm)],[c_458561,c_471900]) ).
tcf(c_516250,plain,
! [X0: $i,X1: $i] :
( holdsAt(filling,n0)
| releasedAt(filling,plus(n0,n1))
| stoppedIn(n0,filling,plus(n0,n2))
| ( plus(n2,X1) = X0 )
| ~ less(n0,n2)
| ~ holdsAt(waterLevel(X1),n0)
| ~ holdsAt(waterLevel(X0),n2)
| ~ holdsAt(filling,plus(n0,n1)) ),
inference(superposition,[status(thm)],[c_111,c_474376]) ).
tcf(c_516294,plain,
! [X0: $i,X1: $i] :
( holdsAt(filling,n0)
| stoppedIn(n0,filling,n2)
| releasedAt(filling,plus(n0,n1))
| ( plus(n2,X1) = X0 )
| ~ less(n0,n2)
| ~ holdsAt(waterLevel(X1),n0)
| ~ holdsAt(waterLevel(X0),n2)
| ~ holdsAt(filling,plus(n0,n1)) ),
inference(light_normalisation,[status(thm)],[c_516250,c_111]) ).
tcf(c_516295,plain,
! [X0: $i,X1: $i] :
( stoppedIn(n0,filling,n2)
| releasedAt(filling,plus(n0,n1))
| ( plus(n2,X1) = X0 )
| ~ holdsAt(waterLevel(X1),n0)
| ~ holdsAt(waterLevel(X0),n2)
| ~ holdsAt(filling,plus(n0,n1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_516294,c_146,c_454793]) ).
tcf(c_522980,plain,
! [X0: $i] :
( stoppedIn(n0,filling,plus(n1,n0))
| holdsAt(waterLevel(plus(X0,n1)),n1)
| ~ less(n0,n1)
| ~ happens(tapOn,n0)
| ~ holdsAt(waterLevel(X0),n0) ),
inference(superposition,[status(thm)],[c_1018,c_477064]) ).
tcf(c_523020,plain,
! [X0: $i] :
( stoppedIn(n0,filling,n1)
| holdsAt(waterLevel(plus(X0,n1)),n1)
| ~ less(n0,n1)
| ~ happens(tapOn,n0)
| ~ holdsAt(waterLevel(X0),n0) ),
inference(light_normalisation,[status(thm)],[c_522980,c_1018]) ).
tcf(c_523021,plain,
! [X0: $i] :
( stoppedIn(n0,filling,n1)
| holdsAt(waterLevel(plus(X0,n1)),n1)
| ~ holdsAt(waterLevel(X0),n0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_523020,c_454755,c_92]) ).
tcf(c_542058,plain,
! [X0: $i] :
( less(n4,X0)
| less(X0,n4)
| ( X0 = plus(n1,n3) ) ),
inference(resolution,[status(thm)],[c_495909,c_142]) ).
tcf(c_545823,plain,
! [X0: $i] :
( stoppedIn(n0,filling,n1)
| holdsAt(waterLevel(plus(n1,X0)),n1)
| ~ holdsAt(waterLevel(X0),n0) ),
inference(superposition,[status(thm)],[c_119,c_523021]) ).
tcf(c_545840,plain,
! [X0: $i,X1: $i] :
( stoppedIn(n0,filling,n1)
| ( plus(X0,n1) = X1 )
| ~ holdsAt(waterLevel(X1),n1)
| ~ holdsAt(waterLevel(X0),n0) ),
inference(superposition,[status(thm)],[c_523021,c_101]) ).
tcf(c_549299,plain,
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,n1)
| ~ holdsAt(waterLevel(n0),n0) ),
inference(superposition,[status(thm)],[c_1018,c_545823]) ).
tcf(c_549328,plain,
( holdsAt(waterLevel(n1),n1)
| stoppedIn(n0,filling,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_549299,c_145]) ).
tcf(c_549592,plain,
( holdsAt(waterLevel(n1),n1)
| ( sK3(n0,filling,n1) = n0 ) ),
inference(superposition,[status(thm)],[c_549328,c_458251]) ).
tcf(c_549750,plain,
( releasedAt(waterLevel(n1),n2)
| holdsAt(waterLevel(n1),n2)
| ( waterLevel(n1) = filling )
| ( sK3(n0,filling,n1) = n0 ) ),
inference(superposition,[status(thm)],[c_549592,c_455983]) ).
tcf(c_549793,plain,
( releasedAt(waterLevel(n1),n2)
| holdsAt(waterLevel(n1),n2)
| ( sK3(n0,filling,n1) = n0 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_549750,c_105]) ).
tcf(c_681538,plain,
! [X0: $i] :
( stoppedIn(n0,filling,n1)
| ( plus(n0,n1) = X0 )
| ~ holdsAt(waterLevel(X0),n1) ),
inference(superposition,[status(thm)],[c_145,c_545840]) ).
tcf(c_681625,plain,
! [X0: $i] :
( stoppedIn(n0,filling,n1)
| ( X0 = n1 )
| ~ holdsAt(waterLevel(X0),n1) ),
inference(demodulation,[status(thm)],[c_681538,c_119,c_1018]) ).
fof(f87,definition,
! [X2,X0,X1] :
( sP0(X2,X0,X1)
<=> ? [X4] :
( waterLevel(X4) = X1
& X0 = overflow
& holdsAt(waterLevel(X4),X2) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f88,definition,
! [X2,X0,X1] :
( sP1(X2,X0,X1)
<=> ? [X3] :
( X1 = waterLevel(X3)
& X0 = tapOff
& holdsAt(waterLevel(X3),X2) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f89,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ( sP0(X2,X0,X1)
| sP1(X2,X0,X1)
| ( X1 = spilling
& X0 = overflow )
| ( X1 = filling
& X0 = tapOn ) ) ),
inference(definition_folding,[],[f57,f88,f87]) ).
fof(f98,plain,
! [X2,X0,X1] :
( ( ~ sP0(X2,X0,X1)
| ? [X4] :
( waterLevel(X4) = X1
& X0 = overflow
& holdsAt(waterLevel(X4),X2) ) )
& ( ! [X4] :
( waterLevel(X4) != X1
| overflow != X0
| ~ holdsAt(waterLevel(X4),X2) )
| sP0(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f87]) ).
fof(f99,plain,
! [X0,X1,X2] :
( ( ~ sP0(X0,X1,X2)
| ? [X4] :
( waterLevel(X4) = X2
& overflow = X1
& holdsAt(waterLevel(X4),X0) ) )
& ( ! [X3] :
( waterLevel(X3) != X2
| overflow != X1
| ~ holdsAt(waterLevel(X3),X0) )
| sP0(X0,X1,X2) ) ),
inference(rectify,[],[f98]) ).
fof(f100,plain,
! [X0,X1,X2] :
( ( ~ sP0(X0,X1,X2)
| ( waterLevel(sK9(X0,X1,X2)) = X2
& overflow = X1
& holdsAt(waterLevel(sK9(X0,X1,X2)),X0) ) )
& ( ! [X3] :
( waterLevel(X3) != X2
| overflow != X1
| ~ holdsAt(waterLevel(X3),X0) )
| sP0(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X4,sK9(X0,X1,X2))],[f99]) ).
fof(f149,plain,
! [X2,X3,X0,X1] :
( waterLevel(X3) != X2
| overflow != X1
| ~ holdsAt(waterLevel(X3),X0)
| sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f100]) ).
fof(f230,plain,
! [X2,X3,X0] :
( waterLevel(X3) != X2
| ~ holdsAt(waterLevel(X3),X0)
| sP0(X0,overflow,X2) ),
inference(equality_resolution,[],[f149]) ).
fof(f231,plain,
! [X3,X0] :
( ~ holdsAt(waterLevel(X3),X0)
| sP0(X0,overflow,waterLevel(X3)) ),
inference(equality_resolution,[],[f230]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i] :
( sP0(X1,overflow,waterLevel(X0))
| ~ holdsAt(waterLevel(X0),X1) ),
inference(cnf_transformation,[],[f231]) ).
tcf(c_11932,plain,
! [X0: $i,X1: $i] :
( initiates(overflow,waterLevel(X0),X1)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(superposition,[status(thm)],[c_71,c_78]) ).
tcf(c_13113,plain,
! [X0: $i,X1: $i] :
( holdsAt(waterLevel(X0),plus(X1,n1))
| ~ happens(overflow,X1)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(superposition,[status(thm)],[c_11932,c_62]) ).
tcf(c_24826,plain,
! [X0: $i] :
( ~ happens(overflow,n1)
| ~ releasedAt(waterLevel(X0),n2)
| ~ holdsAt(waterLevel(X0),n1) ),
inference(superposition,[status(thm)],[c_11932,c_12726]) ).
tcf(c_30825,plain,
! [X0: $i] :
( holdsAt(waterLevel(X0),n2)
| ~ happens(overflow,n1)
| ~ holdsAt(waterLevel(X0),n1) ),
inference(superposition,[status(thm)],[c_113,c_13113]) ).
tcf(c_31053,plain,
! [X0: $i] :
( holdsAt(waterLevel(n3),n1)
| ~ happens(overflow,n1)
| ~ releasedAt(waterLevel(X0),n1)
| ~ holdsAt(waterLevel(X0),n1) ),
inference(superposition,[status(thm)],[c_31041,c_24826]) ).
tcf(c_31061,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(waterLevel(n3),n2)
| ~ happens(overflow,n1)
| ~ releasedAt(X0,n1) ),
inference(superposition,[status(thm)],[c_31041,c_30825]) ).
tcf(c_31099,plain,
! [X0: $i] :
( holdsAt(waterLevel(n3),n1)
| ~ happens(overflow,n1)
| ~ holdsAt(waterLevel(X0),n1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_31053,c_12503]) ).
tcf(c_32870,plain,
! [X0: $i] :
( holdsAt(filling,n2)
| releasedAt(X0,n4)
| holdsAt(waterLevel(n3),n2)
| ~ happens(overflow,n1)
| ~ releasedAt(X0,n1) ),
inference(superposition,[status(thm)],[c_32675,c_30825]) ).
tcf(c_33025,plain,
! [X0: $i] :
( ~ releasedAt(X0,n1)
| holdsAt(waterLevel(n3),n2)
| releasedAt(X0,n4) ),
inference(global_subsumption_just,[status(thm)],[c_32870,c_152,c_153,c_177,c_2755,c_2967,c_22416,c_22715,c_31065,c_31061]) ).
tcf(c_33026,plain,
! [X0: $i] :
( releasedAt(X0,n4)
| holdsAt(waterLevel(n3),n2)
| ~ releasedAt(X0,n1) ),
inference(renaming,[status(thm)],[c_33025]) ).
tcf(c_33038,plain,
! [X0: $i] :
( releasedAt(X0,n3)
| holdsAt(waterLevel(n3),n2)
| ~ releasedAt(X0,n1) ),
inference(superposition,[status(thm)],[c_33026,c_24649]) ).
tcf(c_33161,plain,
! [X0: $i] :
( happens(overflow,n2)
| releasedAt(X0,n2)
| holdsAt(waterLevel(n3),n2)
| ~ releasedAt(X0,n1) ),
inference(superposition,[status(thm)],[c_33038,c_32431]) ).
tcf(c_33167,plain,
! [X0: $i] :
( happens(overflow,n2)
| releasedAt(X0,n3)
| ~ holdsAt(filling,n2)
| ~ releasedAt(X0,n1) ),
inference(superposition,[status(thm)],[c_33038,c_93]) ).
tcf(c_33275,plain,
! [X0: $i] :
( ~ releasedAt(X0,n1)
| holdsAt(waterLevel(n3),n2)
| releasedAt(X0,n2) ),
inference(global_subsumption_just,[status(thm)],[c_33161,c_31065,c_31061]) ).
tcf(c_33276,plain,
! [X0: $i] :
( releasedAt(X0,n2)
| holdsAt(waterLevel(n3),n2)
| ~ releasedAt(X0,n1) ),
inference(renaming,[status(thm)],[c_33275]) ).
tcf(c_84035,plain,
( holdsAt(filling,n2)
| holdsAt(waterLevel(n3),n2)
| ~ happens(overflow,n1) ),
inference(superposition,[status(thm)],[c_83236,c_30825]) ).
tcf(c_97068,plain,
( holdsAt(filling,n2)
| holdsAt(waterLevel(n3),n2)
| ~ releasedAt(spilling,n1) ),
inference(superposition,[status(thm)],[c_33276,c_83215]) ).
tcf(c_97177,plain,
( holdsAt(filling,n2)
| holdsAt(waterLevel(n3),n2) ),
inference(global_subsumption_just,[status(thm)],[c_97068,c_83187,c_84035]) ).
tcf(c_104230,plain,
! [X0: $i] :
( happens(overflow,n2)
| releasedAt(X0,n3)
| holdsAt(X0,n2)
| holdsAt(waterLevel(n3),n1)
| ~ holdsAt(filling,n2)
| ~ holdsAt(X0,n1) ),
inference(superposition,[status(thm)],[c_80758,c_33167]) ).
tcf(c_108019,plain,
! [X0: $i] :
( happens(overflow,n2)
| releasedAt(X0,n3)
| holdsAt(X0,n2)
| holdsAt(waterLevel(n3),n1)
| ~ holdsAt(X0,n1) ),
inference(global_subsumption_just,[status(thm)],[c_104230,c_33167,c_80758,c_83236]) ).
tcf(c_108062,plain,
! [X0: $i] :
( happens(overflow,n2)
| releasedAt(X0,n4)
| holdsAt(X0,n2)
| holdsAt(waterLevel(n3),n1)
| ~ holdsAt(X0,n1) ),
inference(superposition,[status(thm)],[c_108019,c_22715]) ).
tcf(c_109115,plain,
! [X0: $i] :
( happens(overflow,n2)
| releasedAt(X0,n4)
| holdsAt(X0,n2)
| holdsAt(waterLevel(n3),n1)
| ~ happens(overflow,n1)
| ~ holdsAt(X0,n1) ),
inference(superposition,[status(thm)],[c_108062,c_31099]) ).
tcf(c_110781,plain,
( ~ happens(overflow,n1)
| holdsAt(waterLevel(n3),n1) ),
inference(global_subsumption_just,[status(thm)],[c_109115,c_24732,c_83236]) ).
tcf(c_110782,plain,
( holdsAt(waterLevel(n3),n1)
| ~ happens(overflow,n1) ),
inference(renaming,[status(thm)],[c_110781]) ).
tcf(c_110828,plain,
( holdsAt(waterLevel(n3),n2)
| ~ happens(overflow,n1) ),
inference(superposition,[status(thm)],[c_110782,c_30825]) ).
tcf(c_235621,plain,
! [X0: $i] :
( releasedAt(X0,n1)
| holdsAt(waterLevel(n3),n2)
| ~ releasedAt(X0,n3) ),
inference(global_subsumption_just,[status(thm)],[c_230066,c_152,c_153,c_177,c_198,c_2949,c_12831,c_23321,c_31641,c_110828]) ).
tcf(c_255757,plain,
! [X0: $i] :
( releasedAt(X0,n1)
| holdsAt(X0,n3)
| holdsAt(waterLevel(n3),n2)
| ~ holdsAt(X0,n2) ),
inference(superposition,[status(thm)],[c_255727,c_235621]) ).
tcf(c_256432,plain,
( holdsAt(filling,n3)
| holdsAt(waterLevel(n3),n2)
| ~ holdsAt(filling,n2) ),
inference(superposition,[status(thm)],[c_255757,c_220155]) ).
tcf(c_256492,plain,
( holdsAt(waterLevel(n3),n2)
| ~ holdsAt(filling,n2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_256432,c_9975]) ).
tcf(c_256818,plain,
holdsAt(waterLevel(n3),n2),
inference(global_subsumption_just,[status(thm)],[c_256492,c_97177,c_256492]) ).
tcf(c_256828,plain,
! [X0: $i] :
( ( X0 = n3 )
| ~ holdsAt(waterLevel(X0),n2) ),
inference(superposition,[status(thm)],[c_256818,c_101]) ).
tcf(c_256876,plain,
( ( n1 = n3 )
| ~ holdsAt(waterLevel(n1),n2) ),
inference(instantiation,[status(thm)],[c_256828]) ).
tcf(c_454414,plain,
! [X0: $i,X1: $i] :
( initiates(overflow,waterLevel(X0),X1)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(superposition,[status(thm)],[c_71,c_78]) ).
tcf(c_455710,plain,
! [X0: $i,X1: $i] :
( holdsAt(waterLevel(X0),plus(X1,n1))
| ~ happens(overflow,X1)
| ~ holdsAt(waterLevel(X0),X1) ),
inference(superposition,[status(thm)],[c_454414,c_62]) ).
tcf(c_456959,plain,
! [X0: $i] :
( ~ happens(overflow,n1)
| ~ releasedAt(waterLevel(X0),n2)
| ~ holdsAt(waterLevel(X0),n1) ),
inference(superposition,[status(thm)],[c_454414,c_454661]) ).
tcf(c_464415,plain,
! [X0: $i] :
( holdsAt(waterLevel(X0),n2)
| ~ happens(overflow,n1)
| ~ holdsAt(waterLevel(X0),n1) ),
inference(superposition,[status(thm)],[c_113,c_455710]) ).
tcf(c_464426,plain,
! [X0: $i] :
( happens(overflow,plus(X0,n1))
| ~ happens(overflow,X0)
| ~ holdsAt(waterLevel(n3),X0)
| ~ holdsAt(filling,plus(X0,n1)) ),
inference(superposition,[status(thm)],[c_455710,c_93]) ).
tcf(c_496793,plain,
( holdsAt(waterLevel(n3),n2)
| ~ holdsAt(filling,n1)
| ~ happens(overflow,n1) ),
inference(superposition,[status(thm)],[c_486926,c_464415]) ).
tcf(c_496806,plain,
( holdsAt(waterLevel(n3),n2)
| ~ happens(overflow,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_496793,c_460653]) ).
tcf(c_496999,plain,
holdsAt(waterLevel(n3),n2),
inference(global_subsumption_just,[status(thm)],[c_496806,c_97177,c_256492]) ).
tcf(c_497009,plain,
! [X0: $i] :
( ( X0 = n3 )
| ~ holdsAt(waterLevel(X0),n2) ),
inference(superposition,[status(thm)],[c_496999,c_101]) ).
tcf(c_497166,plain,
! [X0: $i] :
( ~ holdsAt(filling,plus(X0,n1))
| ~ happens(overflow,X0) ),
inference(global_subsumption_just,[status(thm)],[c_464426,c_1804]) ).
tcf(c_497167,plain,
! [X0: $i] :
( ~ happens(overflow,X0)
| ~ holdsAt(filling,plus(X0,n1)) ),
inference(renaming,[status(thm)],[c_497166]) ).
tcf(c_497176,plain,
( releasedAt(filling,n1)
| holdsAt(waterLevel(n3),n1)
| ( n0 = n1 )
| ~ holdsAt(filling,n1)
| ~ happens(overflow,n1) ),
inference(superposition,[status(thm)],[c_460494,c_497167]) ).
tcf(c_497184,plain,
( holdsAt(waterLevel(n3),n1)
| ( n0 = n1 )
| ~ happens(overflow,n1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_497176,c_469888,c_460653]) ).
tcf(c_497221,plain,
! [X0: $i] :
( stoppedIn(n0,filling,n2)
| ( plus(X0,n2) = n3 )
| ~ holdsAt(waterLevel(X0),n0) ),
inference(superposition,[status(thm)],[c_459556,c_497009]) ).
tcf(c_518941,plain,
( holdsAt(waterLevel(n3),n1)
| ~ happens(overflow,n1) ),
inference(global_subsumption_just,[status(thm)],[c_497184,c_110782]) ).
tcf(c_543377,plain,
( stoppedIn(n0,filling,n2)
| ( plus(n0,n2) = n3 ) ),
inference(superposition,[status(thm)],[c_145,c_497221]) ).
tcf(c_543378,plain,
( stoppedIn(n0,filling,n2)
| ( n3 = n2 ) ),
inference(light_normalisation,[status(thm)],[c_543377,c_111]) ).
tcf(c_551120,plain,
releasedAt(waterLevel(n1),n2),
inference(global_subsumption_just,[status(thm)],[c_549793,c_152,c_153,c_177,c_186,c_2755,c_12986,c_256876,c_499689]) ).
tcf(c_551122,plain,
( ~ happens(overflow,n1)
| ~ holdsAt(waterLevel(n1),n1) ),
inference(superposition,[status(thm)],[c_551120,c_456959]) ).
tcf(c_609311,plain,
! [X0: $i] :
( stoppedIn(n0,filling,n2)
| ~ holdsAt(waterLevel(X0),n2) ),
inference(global_subsumption_just,[status(thm)],[c_516295,c_3235,c_12071,c_12073,c_12074,c_13574,c_15004,c_22298,c_24171,c_62843,c_256828,c_363743,c_542058,c_543378]) ).
tcf(c_609317,plain,
stoppedIn(n0,filling,n2),
inference(backward_subsumption_resolution,[status(thm)],[c_478639,c_609311]) ).
tcf(c_609351,plain,
( ( sK2(n0,filling,n2) = tapOn )
| ( sK2(n0,filling,n2) = overflow ) ),
inference(superposition,[status(thm)],[c_609317,c_454556]) ).
tcf(c_610382,plain,
( happens(tapOn,sK3(n0,filling,n2))
| ( sK2(n0,filling,n2) = overflow )
| ~ stoppedIn(n0,filling,n2) ),
inference(superposition,[status(thm)],[c_609351,c_49]) ).
tcf(c_610386,plain,
( happens(tapOn,sK3(n0,filling,n2))
| ( sK2(n0,filling,n2) = overflow ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_610382,c_609317]) ).
tcf(c_610413,plain,
( ( sK2(n0,filling,n2) = overflow )
| ~ stoppedIn(n0,filling,n2) ),
inference(superposition,[status(thm)],[c_610386,c_482295]) ).
tcf(c_610415,plain,
sK2(n0,filling,n2) = overflow,
inference(forward_subsumption_resolution,[status(thm)],[c_610413,c_609317]) ).
tcf(c_610724,plain,
( happens(overflow,sK3(n0,filling,n2))
| ~ stoppedIn(n0,filling,n2) ),
inference(superposition,[status(thm)],[c_610415,c_49]) ).
tcf(c_610725,plain,
happens(overflow,sK3(n0,filling,n2)),
inference(forward_subsumption_resolution,[status(thm)],[c_610724,c_609317]) ).
tcf(c_681653,plain,
( stoppedIn(n0,filling,n1)
| ( n1 = n3 )
| ~ happens(overflow,n1) ),
inference(superposition,[status(thm)],[c_518941,c_681625]) ).
tcf(c_681809,plain,
( stoppedIn(n0,filling,n1)
| ~ happens(overflow,n1) ),
inference(global_subsumption_just,[status(thm)],[c_681653,c_152,c_153,c_177,c_186,c_2755,c_12986,c_681653]) ).
tcf(c_692662,plain,
( ( sK3(n0,filling,n2) = n1 )
| ( sK3(n0,filling,n2) = n0 ) ),
inference(superposition,[status(thm)],[c_609317,c_509493]) ).
tcf(c_693519,plain,
( happens(overflow,n0)
| ( sK3(n0,filling,n2) = n1 ) ),
inference(superposition,[status(thm)],[c_692662,c_610725]) ).
tcf(c_693520,plain,
sK3(n0,filling,n2) = n1,
inference(forward_subsumption_resolution,[status(thm)],[c_693519,c_470345]) ).
tcf(c_693531,plain,
happens(overflow,n1),
inference(demodulation,[status(thm)],[c_610725,c_693520]) ).
tcf(c_693532,plain,
stoppedIn(n0,filling,n1),
inference(backward_subsumption_resolution,[status(thm)],[c_681809,c_693531]) ).
tcf(c_693538,plain,
~ holdsAt(waterLevel(n1),n1),
inference(backward_subsumption_resolution,[status(thm)],[c_551122,c_693531]) ).
tcf(c_693565,plain,
sK3(n0,filling,n1) = n0,
inference(backward_subsumption_resolution,[status(thm)],[c_549592,c_693538]) ).
tcf(c_694759,plain,
( less(n0,n0)
| ~ stoppedIn(n0,filling,n1) ),
inference(superposition,[status(thm)],[c_693565,c_50]) ).
tcf(c_694802,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_694759,c_123,c_693532]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR005+1 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.17/20.66 % Computer : n010.cluster.edu
% 0.17/20.66 % Model : x86_64 x86_64
% 0.17/20.66 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/20.66 % Memory : 8046.5625MB
% 0.17/20.66 % OS : Linux 6.8.0-71-generic
% 0.17/20.66 % CPULimit : 300
% 0.17/20.66 % WCLimit : 300
% 0.17/20.66 % DateTime : Fri Sep 25 08:06:50 UTC 2026
% 0.17/20.67 % CPUTime :
% 0.17/20.67 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.22/20.73 Running first-order theorem proving
% 0.22/20.73 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.22/20.75
% 0.22/20.75 % ======== iProver multi-core TPTP/SMT =========
% 0.22/20.75
% 0.22/20.75 % Detected problem language: tptp
% 0.22/20.77 % Proving...
% 244.90/58.55 % SZS status Started for theBenchmark.p
% 244.90/58.55 % SZS status Theorem for theBenchmark.p
% 244.90/58.55
% 244.90/58.55 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 244.90/58.55
% 244.90/58.55 % ------ iProver source info
% 244.90/58.55
% 244.90/58.55 % git: date: 2026-07-19 20:42:38 +0200
% 244.90/58.55 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 244.90/58.55 % git: non_committed_changes: false
% 244.90/58.55
% 244.90/58.55 % ------ Parsing...
% 244.90/58.55 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 244.90/58.55
% 244.90/58.55 % ------ Preprocessing... sup_sim: 2 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sup_sim: 0 sf_s rm: 3 0s sf_e pe_s pe_e %
% 244.90/58.55
% 244.90/58.55 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 244.90/58.55
% 244.90/58.55 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 244.90/58.55 % ------ Proving...
% 244.90/58.55 % ------ Problem Properties
% 244.90/58.55
% 244.90/58.55 %
% 244.90/58.55 % clauses 99
% 244.90/58.55 % conjectures 1
% 244.90/58.55 % EPR 53
% 244.90/58.55 % Horn 76
% 244.90/58.55 % unary 33
% 244.90/58.55 % binary 37
% 244.90/58.55 % lits 208
% 244.90/58.55 % lits eq 48
% 244.90/58.55 % fd_pure 0
% 244.90/58.55 % fd_pseudo 0
% 244.90/58.55 % fd_cond 14
% 244.90/58.55 % fd_pseudo_cond 4
% 244.90/58.55 % AC symbols 0
% 244.90/58.55
% 244.90/58.55 % ------ Schedule dynamic 5 is on
% 244.90/58.55
% 244.90/58.55 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 244.90/58.55
% 244.90/58.55
% 244.90/58.55 % ------
% 244.90/58.55 % Current options:
% 244.90/58.55 % ------
% 244.90/58.55
% 244.90/58.55
% 244.90/58.55 %
% 244.90/58.55
% 244.90/58.55 % ------ Proving...
% 244.90/58.55 % Proof_search_loop: time out after: 10156 full_loop iterations
% 244.90/58.55
% 244.90/58.55 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 244.90/58.55
% 244.90/58.55
% 244.90/58.55 % ------
% 244.90/58.55 % Current options:
% 244.90/58.55 % ------
% 244.90/58.55
% 244.90/58.55
% 244.90/58.55 %
% 244.90/58.55
% 244.90/58.55 % ------ Proving...
% 244.90/58.55 % Proof_search_loop: time out after: 12737 full_loop iterations
% 244.90/58.55
% 244.90/58.55 % ------ Option_1: Negative Selections Time Limit: 35.
% 244.90/58.55
% 244.90/58.55
% 244.90/58.55 % ------
% 244.90/58.55 % Current options:
% 244.90/58.55 % ------
% 244.90/58.55
% 244.90/58.55
% 244.90/58.55 %
% 244.90/58.55
% 244.90/58.55 % ------ Proving...
% 244.90/58.55 %
% 244.90/58.55
% 244.90/58.55 % SZS status Theorem for theBenchmark.p
% 244.90/58.55
% 244.90/58.55 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 244.90/58.57
% 244.90/58.57
%------------------------------------------------------------------------------