%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : CSR310_1 : TPTP v9.0.0. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Apr 10 02:50:26 AM UTC 2025
% Result : Theorem 21.21s 7.11s
% Output : CNFRefutation 21.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 22
% Syntax : Number of formulae : 211 ( 74 unt; 0 typ; 0 def)
% Number of atoms : 535 ( 88 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 544 ( 220 ~; 274 |; 34 &)
% ( 5 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 825 ( 31 atm; 159 fun; 475 num; 160 var)
% Number of types : 5 ( 3 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 13 ( 10 usr; 1 prp; 0-4 aty)
% Number of functors : 37 ( 30 usr; 22 con; 0-3 aty)
% Number of variables : 235 ( 226 !; 9 ?; 235 :)
% Comments :
%------------------------------------------------------------------------------
%$ trajectory > antitrajectory > terminates > stoppedIn > startedIn > releases > initiates > releasedAt > holdsAt > happens > #nlpp > waterLevel > at_time > tapOn > tapOff > spilling > overflow > filling > #skF_11 > #skF_3 > #skF_2 > #skF_4 > #skF_9 > #skF_1 > #skF_7 > #skF_6 > #skF_10 > #skF_8 > #skF_5
%Foreground sorts:
tff(fluent,type,
fluent: $tType ).
tff(time,type,
time: $tType ).
tff(event,type,
event: $tType ).
%Background operators:
tff('#skE_7',type,
'#skE_7': $int ).
tff('#skE_11',type,
'#skE_11': $int ).
tff('#skE_12',type,
'#skE_12': $int ).
tff('#skE_2',type,
'#skE_2': $int ).
tff('#skE_1',type,
'#skE_1': $int ).
tff('#skE_6',type,
'#skE_6': $int ).
tff('#skE_10',type,
'#skE_10': $int ).
tff('#skE_5',type,
'#skE_5': $int ).
tff('#skE_8',type,
'#skE_8': $int ).
tff('#skE_4',type,
'#skE_4': $int ).
tff('#skE_3',type,
'#skE_3': $int ).
tff('#skE_9',type,
'#skE_9': $int ).
%Foreground operators:
tff(tapOff,type,
tapOff: event ).
tff('#skF_11',type,
'#skF_11': ( event * fluent * $int ) > $int ).
tff('#skF_3',type,
'#skF_3': ( $int * fluent * $int ) > event ).
tff(waterLevel,type,
waterLevel: $int > fluent ).
tff(initiates,type,
initiates: ( event * fluent * time ) > $o ).
tff(releasedAt,type,
releasedAt: ( fluent * time ) > $o ).
tff('#skF_2',type,
'#skF_2': ( $int * fluent * $int ) > $int ).
tff('#skF_4',type,
'#skF_4': ( $int * fluent * $int ) > $int ).
tff(releases,type,
releases: ( event * fluent * time ) > $o ).
tff(terminates,type,
terminates: ( event * fluent * time ) > $o ).
tff('#skF_9',type,
'#skF_9': ( event * fluent * $int ) > $int ).
tff(startedIn,type,
startedIn: ( time * fluent * time ) > $o ).
tff('#skF_1',type,
'#skF_1': ( $int * fluent * $int ) > event ).
tff(at_time,type,
at_time: $int > time ).
tff(stoppedIn,type,
stoppedIn: ( time * fluent * time ) > $o ).
tff('#skF_7',type,
'#skF_7': ( fluent * $int ) > event ).
tff(spilling,type,
spilling: fluent ).
tff(holdsAt,type,
holdsAt: ( fluent * time ) > $o ).
tff(overflow,type,
overflow: event ).
tff(trajectory,type,
trajectory: ( fluent * time * fluent * $int ) > $o ).
tff('#skF_6',type,
'#skF_6': ( fluent * $int ) > event ).
tff('#skF_10',type,
'#skF_10': ( event * fluent * $int ) > $int ).
tff(tapOn,type,
tapOn: event ).
tff('#skF_8',type,
'#skF_8': ( fluent * $int ) > event ).
tff(filling,type,
filling: fluent ).
tff('#skF_5',type,
'#skF_5': ( fluent * $int ) > event ).
tff(happens,type,
happens: ( event * time ) > $o ).
tff(antitrajectory,type,
antitrajectory: ( fluent * time * fluent * $int ) > $o ).
tff(f_309,axiom,
~ holdsAt(filling,at_time(0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_filling_0) ).
tff(f_306,axiom,
! [Event: event,Timea: $int] :
( happens(Event,at_time(Timea))
<=> ( ( ( Event = tapOn )
& ( Timea = 0 ) )
| ( holdsAt(waterLevel(3),at_time(Timea))
& holdsAt(filling,at_time(Timea))
& ( Event = overflow ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',happens_all_defn) ).
tff(f_262,axiom,
! [Event: event,Fluent: fluent,Timea: $int] :
( initiates(Event,Fluent,at_time(Timea))
<=> ( ( ( Event = tapOn )
& ( Fluent = filling ) )
| ( ( Event = overflow )
& ( Fluent = spilling ) )
| ? [Heighta: $int] :
( holdsAt(waterLevel(Heighta),at_time(Timea))
& ( Event = tapOff )
& ( Fluent = waterLevel(Heighta) ) )
| ? [Heighta: $int] :
( holdsAt(waterLevel(Heighta),at_time(Timea))
& ( Event = overflow )
& ( Fluent = waterLevel(Heighta) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001_1.ax',initiates_all_defn) ).
tff(f_162,axiom,
! [Event: event,Timea: $int,Fluent: fluent] :
( ( happens(Event,at_time(Timea))
& initiates(Event,Fluent,at_time(Timea)) )
=> holdsAt(Fluent,at_time($sum(Timea,1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001_0.ax',happens_holds) ).
tff(f_132,axiom,
! [Fluent: fluent,Timea: $int] :
( ( ~ holdsAt(Fluent,at_time(Timea))
& ~ releasedAt(Fluent,at_time($sum(Timea,1)))
& ~ ? [Event: event] :
( happens(Event,at_time(Timea))
& initiates(Event,Fluent,at_time(Timea)) ) )
=> ~ holdsAt(Fluent,at_time($sum(Timea,1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001_0.ax',keep_not_holding) ).
tff(f_184,axiom,
! [Event: event,Timea: $int,Fluent: fluent] :
( ( happens(Event,at_time(Timea))
& ( initiates(Event,Fluent,at_time(Timea))
| terminates(Event,Fluent,at_time(Timea)) ) )
=> ~ releasedAt(Fluent,at_time($sum(Timea,1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001_0.ax',happens_not_released) ).
tff(f_224,axiom,
tapOn != overflow,
file('/export/starexec/sandbox/benchmark/Axioms/CSR001_1.ax',tapOn_overflow) ).
tff(f_307,axiom,
holdsAt(waterLevel(0),at_time(0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',waterLevel_0) ).
tff(f_286,axiom,
! [Height1a: $int,Timea: $int,Height2a: $int,Offseta: $int] :
( ( holdsAt(waterLevel(Height1a),at_time(Timea))
& ( Height2a = $sum(Height1a,Offseta) ) )
=> trajectory(filling,at_time(Timea),waterLevel(Height2a),Offseta) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001_1.ax',change_of_waterLevel) ).
tff(f_91,axiom,
! [Event: event,Timea: $int,Fluent: fluent,Fluent2: fluent,Offseta: $int] :
( ( happens(Event,at_time(Timea))
& initiates(Event,Fluent,at_time(Timea))
& $less(0,Offseta)
& trajectory(Fluent,at_time(Timea),Fluent2,Offseta)
& ~ stoppedIn(at_time(Timea),Fluent,at_time($sum(Timea,Offseta))) )
=> holdsAt(Fluent2,at_time($sum(Timea,Offseta))) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001_0.ax',change_holding) ).
tff(f_67,axiom,
! [Time1a: $int,Fluent: fluent,Time2a: $int] :
( stoppedIn(at_time(Time1a),Fluent,at_time(Time2a))
<=> ? [Event: event,Timea: $int] :
( happens(Event,at_time(Timea))
& $less(Time1a,Timea)
& $less(Timea,Time2a)
& terminates(Event,Fluent,at_time(Timea)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001_0.ax',stoppedin_defn) ).
tff(f_324,negated_conjecture,
~ ( holdsAt(filling,at_time(3))
=> ( holdsAt(waterLevel(3),at_time(3))
| holdsAt(filling,at_time(4)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',waterLevel_filling) ).
tff(f_311,axiom,
~ holdsAt(spilling,at_time(0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_spilling_0) ).
tff(f_156,axiom,
! [Fluent: fluent,Timea: $int] :
( ( ~ releasedAt(Fluent,at_time(Timea))
& ~ ? [Event: event] :
( happens(Event,at_time(Timea))
& releases(Event,Fluent,at_time(Timea)) ) )
=> ~ releasedAt(Fluent,at_time($sum(Timea,1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001_0.ax',keep_not_released) ).
tff(f_318,axiom,
~ releasedAt(spilling,at_time(0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_released_spilling_0) ).
tff(f_272,axiom,
! [Event: event,Fluent: fluent,Timea: $int] :
( terminates(Event,Fluent,at_time(Timea))
<=> ( ( ( Event = tapOff )
& ( Fluent = filling ) )
| ( ( Event = overflow )
& ( Fluent = filling ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001_1.ax',terminates_all_defn) ).
tff(f_169,axiom,
! [Event: event,Timea: $int,Fluent: fluent] :
( ( happens(Event,at_time(Timea))
& terminates(Event,Fluent,at_time(Timea)) )
=> ~ holdsAt(Fluent,at_time($sum(Timea,1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001_0.ax',happens_terminates_not_holds) ).
tff(f_117,axiom,
! [Fluent: fluent,Timea: $int] :
( ( holdsAt(Fluent,at_time(Timea))
& ~ releasedAt(Fluent,at_time($sum(Timea,1)))
& ~ ? [Event: event] :
( happens(Event,at_time(Timea))
& terminates(Event,Fluent,at_time(Timea)) ) )
=> holdsAt(Fluent,at_time($sum(Timea,1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001_0.ax',keep_holding) ).
tff(f_229,axiom,
! [Xa: $int] : ( filling != waterLevel(Xa) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001_1.ax',filling_not_waterLevel) ).
tff(f_280,axiom,
! [Event: event,Fluent: fluent,Timea: $int] :
( releases(Event,Fluent,at_time(Timea))
<=> ? [Heighta: $int] :
( ( Event = tapOn )
& ( Fluent = waterLevel(Heighta) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001_1.ax',releases_all_defn) ).
tff(f_175,axiom,
! [Event: event,Timea: $int,Fluent: fluent] :
( ( happens(Event,at_time(Timea))
& releases(Event,Fluent,at_time(Timea)) )
=> releasedAt(Fluent,at_time($sum(Timea,1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001_0.ax',happens_releases) ).
tff(f_144,axiom,
! [Fluent: fluent,Timea: $int] :
( ( releasedAt(Fluent,at_time(Timea))
& ~ ? [Event: event] :
( happens(Event,at_time(Timea))
& ( initiates(Event,Fluent,at_time(Timea))
| terminates(Event,Fluent,at_time(Timea)) ) ) )
=> releasedAt(Fluent,at_time($sum(Timea,1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001_0.ax',keep_released) ).
tff(c_202,plain,
~ holdsAt(filling,at_time(0)),
inference(cnfTransformation,[status(thm)],[f_309]) ).
tff(c_204,plain,
happens(tapOn,at_time(0)),
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_226,plain,
! [Time_59a: $int] : initiates(tapOn,filling,at_time(Time_59a)),
inference(cnfTransformation,[status(thm)],[f_262]) ).
tff(c_911,plain,
! [Fluent_232: fluent,Time_234a: $int,Event_235: event] :
( holdsAt(Fluent_232,at_time($sum(1,Time_234a)))
| ~ initiates(Event_235,Fluent_232,at_time(Time_234a))
| ~ happens(Event_235,at_time(Time_234a)) ),
inference(cnfTransformation,[status(thm)],[f_162]) ).
tff(c_932,plain,
! [Time_59a: $int] :
( holdsAt(filling,at_time($sum(1,Time_59a)))
| ~ happens(tapOn,at_time(Time_59a)) ),
inference(resolution,[status(thm)],[c_226,c_911]) ).
tff(c_2202,plain,
! [Fluent_523: fluent,Time_524a: $int] :
( happens('#skF_6'(Fluent_523,Time_524a),at_time(Time_524a))
| ~ holdsAt(Fluent_523,at_time($sum(1,Time_524a)))
| releasedAt(Fluent_523,at_time($sum(1,Time_524a)))
| holdsAt(Fluent_523,at_time(Time_524a)) ),
inference(cnfTransformation,[status(thm)],[f_132]) ).
tff(c_973,plain,
! [Event_243: event,Fluent_244: fluent,Time_245a: $int] :
( ~ initiates(Event_243,Fluent_244,at_time(Time_245a))
| ~ releasedAt(Fluent_244,at_time($sum(1,Time_245a)))
| ~ happens(Event_243,at_time(Time_245a)) ),
inference(cnfTransformation,[status(thm)],[f_184]) ).
tff(c_994,plain,
! [Time_59a: $int] :
( ~ releasedAt(filling,at_time($sum(1,Time_59a)))
| ~ happens(tapOn,at_time(Time_59a)) ),
inference(resolution,[status(thm)],[c_226,c_973]) ).
tff(c_2286,plain,
! [Time_59a: $int,Time_524a: $int] :
( ~ happens(tapOn,at_time(Time_59a))
| happens('#skF_6'(filling,Time_524a),at_time(Time_524a))
| ~ holdsAt(filling,at_time($sum(1,Time_524a)))
| ( $sum(1,Time_59a) != $sum(1,Time_524a) )
| holdsAt(filling,at_time(Time_524a)) ),
inference(resolution,[status(thm)],[c_2202,c_994]) ).
tff(c_3128,plain,
! [Time_731a: $int] :
( ~ happens(tapOn,at_time(Time_731a))
| happens('#skF_6'(filling,Time_731a),at_time(Time_731a))
| ~ holdsAt(filling,at_time($sum(1,Time_731a)))
| holdsAt(filling,at_time(Time_731a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2286]) ).
tff(c_3133,plain,
! [Time_731a: $int,Time_59a: $int] :
( ~ happens(tapOn,at_time(Time_731a))
| happens('#skF_6'(filling,Time_731a),at_time(Time_731a))
| holdsAt(filling,at_time(Time_731a))
| ( $sum(1,Time_731a) != $sum(1,Time_59a) )
| ~ happens(tapOn,at_time(Time_59a)) ),
inference(resolution,[status(thm)],[c_932,c_3128]) ).
tff(c_3141,plain,
! [Time_733a: $int] :
( happens('#skF_6'(filling,Time_733a),at_time(Time_733a))
| holdsAt(filling,at_time(Time_733a))
| ~ happens(tapOn,at_time(Time_733a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_3133]) ).
tff(c_3157,plain,
( happens('#skF_6'(filling,0),at_time(0))
| ~ happens(tapOn,at_time(0)) ),
inference(resolution,[status(thm)],[c_3141,c_202]) ).
tff(c_3173,plain,
happens('#skF_6'(filling,0),at_time(0)),
inference(demodulation,[status(thm),theory(equality)],[c_204,c_3157]) ).
tff(c_208,plain,
! [Event_82: event,Time_83a: $int] :
( ( tapOn = Event_82 )
| holdsAt(filling,at_time(Time_83a))
| ~ happens(Event_82,at_time(Time_83a)) ),
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_3181,plain,
( ( tapOn = '#skF_6'(filling,0) )
| holdsAt(filling,at_time(0)) ),
inference(resolution,[status(thm)],[c_3173,c_208]) ).
tff(c_3198,plain,
tapOn = '#skF_6'(filling,0),
inference(negUnitSimplification,[status(thm)],[c_202,c_3181]) ).
tff(c_50,plain,
tapOn != overflow,
inference(cnfTransformation,[status(thm)],[f_224]) ).
tff(c_3464,plain,
overflow != '#skF_6'(filling,0),
inference(demodulation,[status(thm),theory(equality)],[c_3198,c_50]) ).
tff(c_203,plain,
holdsAt(waterLevel(0),at_time(0)),
inference(cnfTransformation,[status(thm)],[f_307]) ).
tff(c_3461,plain,
! [Time_59a: $int] : initiates('#skF_6'(filling,0),filling,at_time(Time_59a)),
inference(demodulation,[status(thm),theory(equality)],[c_3198,c_226]) ).
tff(c_216,plain,
! [Time_76a: $int,Height1_75a: $int,Offset_78a: $int] :
( trajectory(filling,at_time(Time_76a),waterLevel($sum(Height1_75a,Offset_78a)),Offset_78a)
| ~ holdsAt(waterLevel(Height1_75a),at_time(Time_76a)) ),
inference(cnfTransformation,[status(thm)],[f_286]) ).
tff(c_2811,plain,
! [Time_644a: $int,Fluent_642: fluent,Event_646: event,Fluent2_645: fluent,Offset_647a: $int] :
( holdsAt(Fluent2_645,at_time($sum(Offset_647a,Time_644a)))
| stoppedIn(at_time(Time_644a),Fluent_642,at_time($sum(Offset_647a,Time_644a)))
| ~ trajectory(Fluent_642,at_time(Time_644a),Fluent2_645,Offset_647a)
| ~ initiates(Event_646,Fluent_642,at_time(Time_644a))
| ~ happens(Event_646,at_time(Time_644a))
| ~ $less(0,Offset_647a) ),
inference(cnfTransformation,[status(thm)],[f_91]) ).
tff(c_2820,plain,
! [Height1_75a: $int,Offset_78a: $int,Time_76a: $int,Event_646: event] :
( holdsAt(waterLevel($sum(Height1_75a,Offset_78a)),at_time($sum(Offset_78a,Time_76a)))
| stoppedIn(at_time(Time_76a),filling,at_time($sum(Offset_78a,Time_76a)))
| ~ initiates(Event_646,filling,at_time(Time_76a))
| ~ happens(Event_646,at_time(Time_76a))
| ~ $less(0,Offset_78a)
| ~ holdsAt(waterLevel(Height1_75a),at_time(Time_76a)) ),
inference(resolution,[status(thm)],[c_216,c_2811]) ).
tff(c_8119,plain,
! [Offset_1772a: $int,Height1_1770a: $int,Time_1771a: $int,Event_1768: event] :
( holdsAt(waterLevel($sum(Offset_1772a,Height1_1770a)),at_time($sum(Time_1771a,Offset_1772a)))
| stoppedIn(at_time(Time_1771a),filling,at_time($sum(Time_1771a,Offset_1772a)))
| ~ initiates(Event_1768,filling,at_time(Time_1771a))
| ~ happens(Event_1768,at_time(Time_1771a))
| ~ $less(0,Offset_1772a)
| ~ holdsAt(waterLevel(Height1_1770a),at_time(Time_1771a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2820]) ).
tff(c_8138,plain,
! [Offset_1772a: $int,Height1_1770a: $int,Time_59a: $int] :
( holdsAt(waterLevel($sum(Offset_1772a,Height1_1770a)),at_time($sum(Time_59a,Offset_1772a)))
| stoppedIn(at_time(Time_59a),filling,at_time($sum(Time_59a,Offset_1772a)))
| ~ happens('#skF_6'(filling,0),at_time(Time_59a))
| ~ $less(0,Offset_1772a)
| ~ holdsAt(waterLevel(Height1_1770a),at_time(Time_59a)) ),
inference(resolution,[status(thm)],[c_3461,c_8119]) ).
tff(c_24292,plain,
! [Height1_8088a: $int,Offset_8086a: $int,Time_8089a: $int] :
( holdsAt(waterLevel($sum(Height1_8088a,Offset_8086a)),at_time($sum(Offset_8086a,Time_8089a)))
| stoppedIn(at_time(Time_8089a),filling,at_time($sum(Offset_8086a,Time_8089a)))
| ~ happens('#skF_6'(filling,0),at_time(Time_8089a))
| ~ $less(0,Offset_8086a)
| ~ holdsAt(waterLevel(Height1_8088a),at_time(Time_8089a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_8138]) ).
tff(c_335,plain,
! [Time1_1a: $int,Fluent_2: fluent,Time2_3a: $int] :
( $less(Time1_1a,'#skF_2'(Time1_1a,Fluent_2,Time2_3a))
| ~ stoppedIn(at_time(Time1_1a),Fluent_2,at_time(Time2_3a)) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_24306,plain,
! [Time_8089a: $int,Offset_8086a: $int,Height1_8088a: $int] :
( $less(Time_8089a,'#skF_2'(Time_8089a,filling,$sum(Offset_8086a,Time_8089a)))
| holdsAt(waterLevel($sum(Height1_8088a,Offset_8086a)),at_time($sum(Offset_8086a,Time_8089a)))
| ~ happens('#skF_6'(filling,0),at_time(Time_8089a))
| ~ $less(0,Offset_8086a)
| ~ holdsAt(waterLevel(Height1_8088a),at_time(Time_8089a)) ),
inference(resolution,[status(thm)],[c_24292,c_335]) ).
tff(c_24476,plain,
! [Time_8168a: $int,Offset_8167a: $int,Height1_8166a: $int] :
( $less(Time_8168a,'#skF_2'(Time_8168a,filling,$sum(Time_8168a,Offset_8167a)))
| holdsAt(waterLevel($sum(Offset_8167a,Height1_8166a)),at_time($sum(Time_8168a,Offset_8167a)))
| ~ happens('#skF_6'(filling,0),at_time(Time_8168a))
| ~ $less(0,Offset_8167a)
| ~ holdsAt(waterLevel(Height1_8166a),at_time(Time_8168a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_24306]) ).
tff(c_24498,plain,
! [Offset_8167a: $int] :
( $less(0,'#skF_2'(0,filling,$sum(0,Offset_8167a)))
| holdsAt(waterLevel($sum(Offset_8167a,0)),at_time($sum(0,Offset_8167a)))
| ~ happens('#skF_6'(filling,0),at_time(0))
| ~ $less(0,Offset_8167a) ),
inference(resolution,[status(thm)],[c_203,c_24476]) ).
tff(c_24513,plain,
! [Offset_8167a: $int] :
( $less(0,'#skF_2'(0,filling,$sum(0,Offset_8167a)))
| holdsAt(waterLevel($sum(Offset_8167a,0)),at_time($sum(0,Offset_8167a)))
| ~ $less(0,Offset_8167a) ),
inference(demodulation,[status(thm),theory(equality)],[c_3173,c_24498]) ).
tff(c_24516,plain,
! [Offset_8172a: $int] :
( $less(0,'#skF_2'(0,filling,Offset_8172a))
| holdsAt(waterLevel(Offset_8172a),at_time(Offset_8172a))
| ~ $less(0,Offset_8172a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_24513]) ).
tff(c_196,plain,
~ holdsAt(waterLevel(3),at_time(3)),
inference(cnfTransformation,[status(thm)],[f_324]) ).
tff(c_24815,plain,
( $less(0,'#skF_2'(0,filling,3))
| ~ $less(0,3) ),
inference(resolution,[status(thm)],[c_24516,c_196]) ).
tff(c_24817,plain,
$less(0,'#skF_2'(0,filling,3)),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_24815]) ).
tff(c_24821,plain,
'#skF_2'(0,filling,3) = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_24817]) ).
tff(c_8141,plain,
! [Height1_1770a: $int,Offset_1772a: $int,Time_59a: $int] :
( holdsAt(waterLevel($sum(Height1_1770a,Offset_1772a)),at_time($sum(Offset_1772a,Time_59a)))
| stoppedIn(at_time(Time_59a),filling,at_time($sum(Offset_1772a,Time_59a)))
| ~ happens('#skF_6'(filling,0),at_time(Time_59a))
| ~ $less(0,Offset_1772a)
| ~ holdsAt(waterLevel(Height1_1770a),at_time(Time_59a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_8138]) ).
tff(c_337,plain,
! [Time1_1a: $int,Fluent_2: fluent,Time2_3a: $int] :
( terminates('#skF_1'(Time1_1a,Fluent_2,Time2_3a),Fluent_2,at_time('#skF_2'(Time1_1a,Fluent_2,Time2_3a)))
| ~ stoppedIn(at_time(Time1_1a),Fluent_2,at_time(Time2_3a)) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_24833,plain,
( terminates('#skF_1'(0,filling,3),filling,at_time('#skE_7'))
| ~ stoppedIn(at_time(0),filling,at_time(3)) ),
inference(superposition,[status(thm),theory(equality)],[c_24821,c_337]) ).
tff(c_24840,plain,
~ stoppedIn(at_time(0),filling,at_time(3)),
inference(splitLeft,[status(thm)],[c_24833]) ).
tff(c_24843,plain,
! [Height1_1770a: $int,Offset_1772a: $int] :
( holdsAt(waterLevel($sum(Height1_1770a,Offset_1772a)),at_time($sum(Offset_1772a,0)))
| ( $sum(Offset_1772a,0) != 3 )
| ~ happens('#skF_6'(filling,0),at_time(0))
| ~ $less(0,Offset_1772a)
| ~ holdsAt(waterLevel(Height1_1770a),at_time(0)) ),
inference(resolution,[status(thm)],[c_8141,c_24840]) ).
tff(c_24860,plain,
! [Height1_1770a: $int,Offset_1772a: $int] :
( holdsAt(waterLevel($sum(Height1_1770a,Offset_1772a)),at_time($sum(Offset_1772a,0)))
| ( $sum(Offset_1772a,0) != 3 )
| ~ $less(0,Offset_1772a)
| ~ holdsAt(waterLevel(Height1_1770a),at_time(0)) ),
inference(demodulation,[status(thm),theory(equality)],[c_3173,c_24843]) ).
tff(c_24862,plain,
! [Height1_1770a: $int] :
( holdsAt(waterLevel($sum(3,Height1_1770a)),at_time(3))
| ~ $less(0,3)
| ~ holdsAt(waterLevel(Height1_1770a),at_time(0)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_24860]) ).
tff(c_24880,plain,
! [Height1_8215a: $int] :
( holdsAt(waterLevel($sum(3,Height1_8215a)),at_time(3))
| ~ holdsAt(waterLevel(Height1_8215a),at_time(0)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_24862]) ).
tff(c_24889,plain,
holdsAt(waterLevel($sum(3,0)),at_time(3)),
inference(resolution,[status(thm)],[c_203,c_24880]) ).
tff(c_24891,plain,
holdsAt(waterLevel(3),at_time(3)),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_24889]) ).
tff(c_24892,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_196,c_24891]) ).
tff(c_24898,plain,
stoppedIn(at_time(0),filling,at_time(3)),
inference(splitRight,[status(thm)],[c_24833]) ).
tff(c_334,plain,
! [Time1_1a: $int,Fluent_2: fluent,Time2_3a: $int] :
( happens('#skF_1'(Time1_1a,Fluent_2,Time2_3a),at_time('#skF_2'(Time1_1a,Fluent_2,Time2_3a)))
| ~ stoppedIn(at_time(Time1_1a),Fluent_2,at_time(Time2_3a)) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_24901,plain,
happens('#skF_1'(0,filling,3),at_time('#skF_2'(0,filling,3))),
inference(resolution,[status(thm)],[c_24898,c_334]) ).
tff(c_24913,plain,
happens('#skF_1'(0,filling,3),at_time('#skE_7')),
inference(demodulation,[status(thm),theory(equality)],[c_24821,c_24901]) ).
tff(c_24921,plain,
happens('#skF_1'(0,filling,3),at_time('#skE_7')),
inference(demodulation,[status(thm),theory(equality)],[c_24821,c_24901]) ).
tff(c_211,plain,
! [Event_82: event,Time_83a: $int] :
( ( overflow = Event_82 )
| ~ happens(Event_82,at_time(Time_83a))
| ( Time_83a = 0 ) ),
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_24951,plain,
( ( overflow = '#skF_1'(0,filling,3) )
| ( '#skE_7' = 0 ) ),
inference(resolution,[status(thm)],[c_24921,c_211]) ).
tff(c_24953,plain,
'#skE_7' = 0,
inference(splitLeft,[status(thm)],[c_24951]) ).
tff(c_24818,plain,
'#skF_2'(0,filling,3) = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_24817]) ).
tff(c_24822,plain,
$less(0,'#skE_7'),
inference(demodulation,[status(thm),theory(equality)],[c_24818,c_24817]) ).
tff(c_24961,plain,
$less(0,0),
inference(demodulation,[status(thm),theory(equality)],[c_24953,c_24822]) ).
tff(c_24966,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_24961]) ).
tff(c_24969,plain,
overflow = '#skF_1'(0,filling,3),
inference(splitRight,[status(thm)],[c_24951]) ).
tff(c_227,plain,
! [Time_59a: $int] : initiates(overflow,spilling,at_time(Time_59a)),
inference(cnfTransformation,[status(thm)],[f_262]) ).
tff(c_935,plain,
! [Time_59a: $int] :
( holdsAt(spilling,at_time($sum(1,Time_59a)))
| ~ happens(overflow,at_time(Time_59a)) ),
inference(resolution,[status(thm)],[c_227,c_911]) ).
tff(c_997,plain,
! [Time_59a: $int] :
( ~ releasedAt(spilling,at_time($sum(1,Time_59a)))
| ~ happens(overflow,at_time(Time_59a)) ),
inference(resolution,[status(thm)],[c_227,c_973]) ).
tff(c_2281,plain,
! [Time_59a: $int,Time_524a: $int] :
( ~ happens(overflow,at_time(Time_59a))
| happens('#skF_6'(spilling,Time_524a),at_time(Time_524a))
| ~ holdsAt(spilling,at_time($sum(1,Time_524a)))
| ( $sum(1,Time_59a) != $sum(1,Time_524a) )
| holdsAt(spilling,at_time(Time_524a)) ),
inference(resolution,[status(thm)],[c_2202,c_997]) ).
tff(c_2870,plain,
! [Time_679a: $int] :
( ~ happens(overflow,at_time(Time_679a))
| happens('#skF_6'(spilling,Time_679a),at_time(Time_679a))
| ~ holdsAt(spilling,at_time($sum(1,Time_679a)))
| holdsAt(spilling,at_time(Time_679a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2281]) ).
tff(c_2873,plain,
! [Time_679a: $int,Time_59a: $int] :
( ~ happens(overflow,at_time(Time_679a))
| happens('#skF_6'(spilling,Time_679a),at_time(Time_679a))
| holdsAt(spilling,at_time(Time_679a))
| ( $sum(1,Time_679a) != $sum(1,Time_59a) )
| ~ happens(overflow,at_time(Time_59a)) ),
inference(resolution,[status(thm)],[c_935,c_2870]) ).
tff(c_2876,plain,
! [Time_59a: $int] :
( happens('#skF_6'(spilling,Time_59a),at_time(Time_59a))
| holdsAt(spilling,at_time(Time_59a))
| ~ happens(overflow,at_time(Time_59a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2873]) ).
tff(c_201,plain,
~ holdsAt(spilling,at_time(0)),
inference(cnfTransformation,[status(thm)],[f_311]) ).
tff(c_292,plain,
! [Fluent_38: fluent,Time_39a: $int] :
( happens('#skF_8'(Fluent_38,Time_39a),at_time(Time_39a))
| ~ releasedAt(Fluent_38,at_time($sum(1,Time_39a)))
| releasedAt(Fluent_38,at_time(Time_39a)) ),
inference(cnfTransformation,[status(thm)],[f_156]) ).
tff(c_2266,plain,
! [Fluent_523: fluent,Time_39a: $int,Time_524a: $int] :
( happens('#skF_8'(Fluent_523,Time_39a),at_time(Time_39a))
| releasedAt(Fluent_523,at_time(Time_39a))
| happens('#skF_6'(Fluent_523,Time_524a),at_time(Time_524a))
| ~ holdsAt(Fluent_523,at_time($sum(1,Time_524a)))
| ( $sum(1,Time_524a) != $sum(1,Time_39a) )
| holdsAt(Fluent_523,at_time(Time_524a)) ),
inference(resolution,[status(thm)],[c_2202,c_292]) ).
tff(c_3699,plain,
! [Fluent_825: fluent,Time_826a: $int] :
( happens('#skF_8'(Fluent_825,Time_826a),at_time(Time_826a))
| releasedAt(Fluent_825,at_time(Time_826a))
| happens('#skF_6'(Fluent_825,Time_826a),at_time(Time_826a))
| ~ holdsAt(Fluent_825,at_time($sum(1,Time_826a)))
| holdsAt(Fluent_825,at_time(Time_826a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2266]) ).
tff(c_198,plain,
~ releasedAt(spilling,at_time(0)),
inference(cnfTransformation,[status(thm)],[f_318]) ).
tff(c_3736,plain,
( happens('#skF_8'(spilling,0),at_time(0))
| happens('#skF_6'(spilling,0),at_time(0))
| ~ holdsAt(spilling,at_time($sum(1,0)))
| holdsAt(spilling,at_time(0)) ),
inference(resolution,[status(thm)],[c_3699,c_198]) ).
tff(c_3773,plain,
( happens('#skF_8'(spilling,0),at_time(0))
| happens('#skF_6'(spilling,0),at_time(0))
| ~ holdsAt(spilling,at_time($sum(1,0))) ),
inference(negUnitSimplification,[status(thm)],[c_201,c_3736]) ).
tff(c_3775,plain,
( happens('#skF_8'(spilling,0),at_time(0))
| happens('#skF_6'(spilling,0),at_time(0))
| ~ holdsAt(spilling,at_time(1)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_3773]) ).
tff(c_4266,plain,
~ holdsAt(spilling,at_time(1)),
inference(splitLeft,[status(thm)],[c_3775]) ).
tff(c_4274,plain,
( happens('#skF_6'(spilling,1),at_time(1))
| ~ happens(overflow,at_time(1)) ),
inference(resolution,[status(thm)],[c_2876,c_4266]) ).
tff(c_4280,plain,
~ happens(overflow,at_time(1)),
inference(splitLeft,[status(thm)],[c_4274]) ).
tff(c_25591,plain,
~ happens('#skF_1'(0,filling,3),at_time(1)),
inference(demodulation,[status(thm),theory(equality)],[c_24969,c_4280]) ).
tff(c_25686,plain,
'#skE_7' != 1,
inference(resolution,[status(thm)],[c_24913,c_25591]) ).
tff(c_195,plain,
holdsAt(filling,at_time(3)),
inference(cnfTransformation,[status(thm)],[f_324]) ).
tff(c_221,plain,
! [Time_68a: $int] : terminates(overflow,filling,at_time(Time_68a)),
inference(cnfTransformation,[status(thm)],[f_272]) ).
tff(c_808,plain,
! [Fluent_214: fluent,Time_216a: $int,Event_217: event] :
( ~ holdsAt(Fluent_214,at_time($sum(1,Time_216a)))
| ~ terminates(Event_217,Fluent_214,at_time(Time_216a))
| ~ happens(Event_217,at_time(Time_216a)) ),
inference(cnfTransformation,[status(thm)],[f_169]) ).
tff(c_823,plain,
! [Time_221a: $int] :
( ~ holdsAt(filling,at_time($sum(1,Time_221a)))
| ~ happens(overflow,at_time(Time_221a)) ),
inference(resolution,[status(thm)],[c_221,c_808]) ).
tff(c_827,plain,
! [Time_221a: $int] :
( ( $sum(1,Time_221a) != 3 )
| ~ happens(overflow,at_time(Time_221a)) ),
inference(resolution,[status(thm)],[c_195,c_823]) ).
tff(c_830,plain,
~ happens(overflow,at_time(2)),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_827]) ).
tff(c_25651,plain,
~ happens('#skF_1'(0,filling,3),at_time(2)),
inference(demodulation,[status(thm),theory(equality)],[c_24969,c_830]) ).
tff(c_25676,plain,
'#skE_7' != 2,
inference(resolution,[status(thm)],[c_24913,c_25651]) ).
tff(c_336,plain,
! [Time1_1a: $int,Fluent_2: fluent,Time2_3a: $int] :
( $less('#skF_2'(Time1_1a,Fluent_2,Time2_3a),Time2_3a)
| ~ stoppedIn(at_time(Time1_1a),Fluent_2,at_time(Time2_3a)) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_24907,plain,
$less('#skF_2'(0,filling,3),3),
inference(resolution,[status(thm)],[c_24898,c_336]) ).
tff(c_24918,plain,
$less('#skE_7',3),
inference(demodulation,[status(thm),theory(equality)],[c_24821,c_24907]) ).
tff(c_25687,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_25686,c_25676,c_24918,c_24822]) ).
tff(c_25691,plain,
happens(overflow,at_time(1)),
inference(splitRight,[status(thm)],[c_4274]) ).
tff(c_207,plain,
! [Time_83a: $int,Event_82: event] :
( holdsAt(waterLevel(3),at_time(Time_83a))
| ~ happens(Event_82,at_time(Time_83a))
| ( Time_83a = 0 ) ),
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_25824,plain,
( holdsAt(waterLevel(3),at_time(1))
| ( 1 = 0 ) ),
inference(resolution,[status(thm)],[c_25691,c_207]) ).
tff(c_25826,plain,
holdsAt(waterLevel(3),at_time(1)),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_25824]) ).
tff(c_229,plain,
! [Height_65a: $int,Time_59a: $int] :
( ~ holdsAt(waterLevel(Height_65a),at_time(Time_59a))
| initiates(overflow,waterLevel(Height_65a),at_time(Time_59a)) ),
inference(cnfTransformation,[status(thm)],[f_262]) ).
tff(c_929,plain,
! [Height_65a: $int,Time_59a: $int] :
( holdsAt(waterLevel(Height_65a),at_time($sum(1,Time_59a)))
| ~ happens(overflow,at_time(Time_59a))
| ~ holdsAt(waterLevel(Height_65a),at_time(Time_59a)) ),
inference(resolution,[status(thm)],[c_229,c_911]) ).
tff(c_25936,plain,
( holdsAt(waterLevel(3),at_time($sum(1,1)))
| ~ happens(overflow,at_time(1)) ),
inference(resolution,[status(thm)],[c_25826,c_929]) ).
tff(c_25966,plain,
holdsAt(waterLevel(3),at_time($sum(1,1))),
inference(demodulation,[status(thm),theory(equality)],[c_25691,c_25936]) ).
tff(c_25968,plain,
holdsAt(waterLevel(3),at_time(2)),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_25966]) ).
tff(c_205,plain,
! [Time_83a: $int] :
( ~ holdsAt(filling,at_time(Time_83a))
| ~ holdsAt(waterLevel(3),at_time(Time_83a))
| happens(overflow,at_time(Time_83a)) ),
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_26006,plain,
( ~ holdsAt(filling,at_time(2))
| happens(overflow,at_time(2)) ),
inference(resolution,[status(thm)],[c_25968,c_205]) ).
tff(c_26022,plain,
~ holdsAt(filling,at_time(2)),
inference(negUnitSimplification,[status(thm)],[c_830,c_26006]) ).
tff(c_209,plain,
! [Time_83a: $int,Event_82: event] :
( holdsAt(filling,at_time(Time_83a))
| ~ happens(Event_82,at_time(Time_83a))
| ( Time_83a = 0 ) ),
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_25827,plain,
( holdsAt(filling,at_time(1))
| ( 1 = 0 ) ),
inference(resolution,[status(thm)],[c_25691,c_209]) ).
tff(c_25829,plain,
holdsAt(filling,at_time(1)),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_25827]) ).
tff(c_2085,plain,
! [Fluent_506: fluent,Time_507a: $int] :
( happens('#skF_5'(Fluent_506,Time_507a),at_time(Time_507a))
| holdsAt(Fluent_506,at_time($sum(1,Time_507a)))
| releasedAt(Fluent_506,at_time($sum(1,Time_507a)))
| ~ holdsAt(Fluent_506,at_time(Time_507a)) ),
inference(cnfTransformation,[status(thm)],[f_117]) ).
tff(c_1007,plain,
! [Event_254: event,Fluent_255: fluent,Time_256a: $int] :
( ~ terminates(Event_254,Fluent_255,at_time(Time_256a))
| ~ releasedAt(Fluent_255,at_time($sum(1,Time_256a)))
| ~ happens(Event_254,at_time(Time_256a)) ),
inference(cnfTransformation,[status(thm)],[f_184]) ).
tff(c_1016,plain,
! [Time_68a: $int] :
( ~ releasedAt(filling,at_time($sum(1,Time_68a)))
| ~ happens(overflow,at_time(Time_68a)) ),
inference(resolution,[status(thm)],[c_221,c_1007]) ).
tff(c_2161,plain,
! [Time_68a: $int,Time_507a: $int] :
( ~ happens(overflow,at_time(Time_68a))
| happens('#skF_5'(filling,Time_507a),at_time(Time_507a))
| holdsAt(filling,at_time($sum(1,Time_507a)))
| ( $sum(1,Time_68a) != $sum(1,Time_507a) )
| ~ holdsAt(filling,at_time(Time_507a)) ),
inference(resolution,[status(thm)],[c_2085,c_1016]) ).
tff(c_2165,plain,
! [Time_507a: $int] :
( ~ happens(overflow,at_time(Time_507a))
| happens('#skF_5'(filling,Time_507a),at_time(Time_507a))
| holdsAt(filling,at_time($sum(1,Time_507a)))
| ~ holdsAt(filling,at_time(Time_507a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2161]) ).
tff(c_25834,plain,
( ~ happens(overflow,at_time(1))
| happens('#skF_5'(filling,1),at_time(1))
| holdsAt(filling,at_time($sum(1,1))) ),
inference(resolution,[status(thm)],[c_25829,c_2165]) ).
tff(c_25847,plain,
( happens('#skF_5'(filling,1),at_time(1))
| holdsAt(filling,at_time($sum(1,1))) ),
inference(demodulation,[status(thm),theory(equality)],[c_25691,c_25834]) ).
tff(c_25849,plain,
( happens('#skF_5'(filling,1),at_time(1))
| holdsAt(filling,at_time(2)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_25847]) ).
tff(c_28236,plain,
happens('#skF_5'(filling,1),at_time(1)),
inference(negUnitSimplification,[status(thm)],[c_26022,c_25849]) ).
tff(c_28267,plain,
( ( overflow = '#skF_5'(filling,1) )
| ( 1 = 0 ) ),
inference(resolution,[status(thm)],[c_28236,c_211]) ).
tff(c_28269,plain,
overflow = '#skF_5'(filling,1),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_28267]) ).
tff(c_28504,plain,
! [Height_65a: $int,Time_59a: $int] :
( ~ holdsAt(waterLevel(Height_65a),at_time(Time_59a))
| initiates('#skF_5'(filling,1),waterLevel(Height_65a),at_time(Time_59a)) ),
inference(demodulation,[status(thm),theory(equality)],[c_28269,c_229]) ).
tff(c_3137,plain,
! [Time_731a: $int] :
( ~ happens(tapOn,at_time(Time_731a))
| happens('#skF_6'(filling,Time_731a),at_time(Time_731a))
| ( $sum(1,Time_731a) != 3 )
| holdsAt(filling,at_time(Time_731a)) ),
inference(resolution,[status(thm)],[c_195,c_3128]) ).
tff(c_3140,plain,
( ~ happens(tapOn,at_time(2))
| happens('#skF_6'(filling,2),at_time(2))
| holdsAt(filling,at_time(2)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_3137]) ).
tff(c_3663,plain,
( ~ happens('#skF_6'(filling,0),at_time(2))
| happens('#skF_6'(filling,2),at_time(2))
| holdsAt(filling,at_time(2)) ),
inference(demodulation,[status(thm),theory(equality)],[c_3198,c_3140]) ).
tff(c_3665,plain,
~ happens('#skF_6'(filling,0),at_time(2)),
inference(splitLeft,[status(thm)],[c_3663]) ).
tff(c_268,plain,
! [X_53a: $int] : ( waterLevel(X_53a) != filling ),
inference(cnfTransformation,[status(thm)],[f_229]) ).
tff(c_2658,plain,
! [Fluent_616: fluent,Time_617a: $int] :
( terminates('#skF_5'(Fluent_616,Time_617a),Fluent_616,at_time(Time_617a))
| holdsAt(Fluent_616,at_time($sum(1,Time_617a)))
| releasedAt(Fluent_616,at_time($sum(1,Time_617a)))
| ~ holdsAt(Fluent_616,at_time(Time_617a)) ),
inference(cnfTransformation,[status(thm)],[f_117]) ).
tff(c_225,plain,
! [Fluent_67: fluent,Event_66: event,Time_68a: $int] :
( ( filling = Fluent_67 )
| ~ terminates(Event_66,Fluent_67,at_time(Time_68a)) ),
inference(cnfTransformation,[status(thm)],[f_272]) ).
tff(c_2689,plain,
! [Fluent_626: fluent,Time_628a: $int] :
( ( filling = Fluent_626 )
| holdsAt(Fluent_626,at_time($sum(1,Time_628a)))
| releasedAt(Fluent_626,at_time($sum(1,Time_628a)))
| ~ holdsAt(Fluent_626,at_time(Time_628a)) ),
inference(resolution,[status(thm)],[c_2658,c_225]) ).
tff(c_1425,plain,
! [Fluent_315: fluent,Time_316a: $int] :
( releases('#skF_8'(Fluent_315,Time_316a),Fluent_315,at_time(Time_316a))
| ~ releasedAt(Fluent_315,at_time($sum(1,Time_316a)))
| releasedAt(Fluent_315,at_time(Time_316a)) ),
inference(cnfTransformation,[status(thm)],[f_156]) ).
tff(c_217,plain,
! [Event_69: event,Fluent_70: fluent,Time_71a: $int] :
( ( tapOn = Event_69 )
| ~ releases(Event_69,Fluent_70,at_time(Time_71a)) ),
inference(cnfTransformation,[status(thm)],[f_280]) ).
tff(c_1445,plain,
! [Fluent_315: fluent,Time_316a: $int] :
( ( tapOn = '#skF_8'(Fluent_315,Time_316a) )
| ~ releasedAt(Fluent_315,at_time($sum(1,Time_316a)))
| releasedAt(Fluent_315,at_time(Time_316a)) ),
inference(resolution,[status(thm)],[c_1425,c_217]) ).
tff(c_2750,plain,
! [Fluent_626: fluent,Time_316a: $int,Time_628a: $int] :
( ( tapOn = '#skF_8'(Fluent_626,Time_316a) )
| releasedAt(Fluent_626,at_time(Time_316a))
| ( filling = Fluent_626 )
| holdsAt(Fluent_626,at_time($sum(1,Time_628a)))
| ( $sum(1,Time_628a) != $sum(1,Time_316a) )
| ~ holdsAt(Fluent_626,at_time(Time_628a)) ),
inference(resolution,[status(thm)],[c_2689,c_1445]) ).
tff(c_2754,plain,
! [Fluent_626: fluent,Time_316a: $int] :
( ( tapOn = '#skF_8'(Fluent_626,Time_316a) )
| releasedAt(Fluent_626,at_time(Time_316a))
| ( filling = Fluent_626 )
| holdsAt(Fluent_626,at_time($sum(1,Time_316a)))
| ~ holdsAt(Fluent_626,at_time(Time_316a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2750]) ).
tff(c_3419,plain,
! [Fluent_626: fluent,Time_316a: $int] :
( ( '#skF_8'(Fluent_626,Time_316a) = '#skF_6'(filling,0) )
| releasedAt(Fluent_626,at_time(Time_316a))
| ( filling = Fluent_626 )
| holdsAt(Fluent_626,at_time($sum(1,Time_316a)))
| ~ holdsAt(Fluent_626,at_time(Time_316a)) ),
inference(demodulation,[status(thm),theory(equality)],[c_3198,c_2754]) ).
tff(c_219,plain,
! [Height_74a: $int,Time_71a: $int] : releases(tapOn,waterLevel(Height_74a),at_time(Time_71a)),
inference(cnfTransformation,[status(thm)],[f_280]) ).
tff(c_1039,plain,
! [Fluent_268: fluent,Time_270a: $int,Event_271: event] :
( releasedAt(Fluent_268,at_time($sum(1,Time_270a)))
| ~ releases(Event_271,Fluent_268,at_time(Time_270a))
| ~ happens(Event_271,at_time(Time_270a)) ),
inference(cnfTransformation,[status(thm)],[f_175]) ).
tff(c_1045,plain,
! [Height_74a: $int,Time_71a: $int] :
( releasedAt(waterLevel(Height_74a),at_time($sum(1,Time_71a)))
| ~ happens(tapOn,at_time(Time_71a)) ),
inference(resolution,[status(thm)],[c_219,c_1039]) ).
tff(c_3440,plain,
! [Height_74a: $int,Time_71a: $int] :
( releasedAt(waterLevel(Height_74a),at_time($sum(1,Time_71a)))
| ~ happens('#skF_6'(filling,0),at_time(Time_71a)) ),
inference(demodulation,[status(thm),theory(equality)],[c_3198,c_1045]) ).
tff(c_1357,plain,
! [Fluent_302: fluent,Time_303a: $int] :
( happens('#skF_7'(Fluent_302,Time_303a),at_time(Time_303a))
| releasedAt(Fluent_302,at_time($sum(1,Time_303a)))
| ~ releasedAt(Fluent_302,at_time(Time_303a)) ),
inference(cnfTransformation,[status(thm)],[f_144]) ).
tff(c_1360,plain,
! [Height_74a: $int,Time_71a: $int] :
( happens('#skF_7'(waterLevel(Height_74a),$sum(1,Time_71a)),at_time($sum(1,Time_71a)))
| releasedAt(waterLevel(Height_74a),at_time($sum(1,$sum(1,Time_71a))))
| ~ happens(tapOn,at_time(Time_71a)) ),
inference(resolution,[status(thm)],[c_1045,c_1357]) ).
tff(c_1363,plain,
! [Height_74a: $int,Time_71a: $int] :
( happens('#skF_7'(waterLevel(Height_74a),$sum(1,Time_71a)),at_time($sum(1,Time_71a)))
| releasedAt(waterLevel(Height_74a),at_time($sum(2,Time_71a)))
| ~ happens(tapOn,at_time(Time_71a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1360]) ).
tff(c_34958,plain,
! [Height_10346a: $int,Time_10347a: $int] :
( happens('#skF_7'(waterLevel(Height_10346a),$sum(1,Time_10347a)),at_time($sum(1,Time_10347a)))
| releasedAt(waterLevel(Height_10346a),at_time($sum(2,Time_10347a)))
| ~ happens('#skF_6'(filling,0),at_time(Time_10347a)) ),
inference(demodulation,[status(thm),theory(equality)],[c_3198,c_1363]) ).
tff(c_991,plain,
! [Height_65a: $int,Time_59a: $int] :
( ~ releasedAt(waterLevel(Height_65a),at_time($sum(1,Time_59a)))
| ~ happens(overflow,at_time(Time_59a))
| ~ holdsAt(waterLevel(Height_65a),at_time(Time_59a)) ),
inference(resolution,[status(thm)],[c_229,c_973]) ).
tff(c_28481,plain,
! [Height_65a: $int,Time_59a: $int] :
( ~ releasedAt(waterLevel(Height_65a),at_time($sum(1,Time_59a)))
| ~ happens('#skF_5'(filling,1),at_time(Time_59a))
| ~ holdsAt(waterLevel(Height_65a),at_time(Time_59a)) ),
inference(demodulation,[status(thm),theory(equality)],[c_28269,c_991]) ).
tff(c_35023,plain,
! [Time_59a: $int,Height_10346a: $int,Time_10347a: $int] :
( ~ happens('#skF_5'(filling,1),at_time(Time_59a))
| ~ holdsAt(waterLevel(Height_10346a),at_time(Time_59a))
| happens('#skF_7'(waterLevel(Height_10346a),$sum(1,Time_10347a)),at_time($sum(1,Time_10347a)))
| ( $sum(2,Time_10347a) != $sum(1,Time_59a) )
| ~ happens('#skF_6'(filling,0),at_time(Time_10347a)) ),
inference(resolution,[status(thm)],[c_34958,c_28481]) ).
tff(c_35025,plain,
! [Time_59a: $int,Height_10346a: $int] :
( ~ happens('#skF_5'(filling,1),at_time(Time_59a))
| ~ holdsAt(waterLevel(Height_10346a),at_time(Time_59a))
| happens('#skF_7'(waterLevel(Height_10346a),$sum(1,$sum($uminus(1),Time_59a))),at_time($sum(1,$sum($uminus(1),Time_59a))))
| ~ happens('#skF_6'(filling,0),at_time($sum($uminus(1),Time_59a))) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_35023]) ).
tff(c_35471,plain,
! [Time_10535a: $int,Height_10536a: $int] :
( ~ happens('#skF_5'(filling,1),at_time(Time_10535a))
| ~ holdsAt(waterLevel(Height_10536a),at_time(Time_10535a))
| happens('#skF_7'(waterLevel(Height_10536a),Time_10535a),at_time(Time_10535a))
| ~ happens('#skF_6'(filling,0),at_time($sum($uminus(1),Time_10535a))) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_35025]) ).
tff(c_35483,plain,
( ~ happens('#skF_5'(filling,1),at_time(1))
| happens('#skF_7'(waterLevel(3),1),at_time(1))
| ~ happens('#skF_6'(filling,0),at_time($sum($uminus(1),1))) ),
inference(resolution,[status(thm)],[c_25826,c_35471]) ).
tff(c_35497,plain,
( happens('#skF_7'(waterLevel(3),1),at_time(1))
| ~ happens('#skF_6'(filling,0),at_time($sum($uminus(1),1))) ),
inference(demodulation,[status(thm),theory(equality)],[c_28236,c_35483]) ).
tff(c_35499,plain,
( happens('#skF_7'(waterLevel(3),1),at_time(1))
| ~ happens('#skF_6'(filling,0),at_time(0)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_35497]) ).
tff(c_35504,plain,
happens('#skF_7'(waterLevel(3),1),at_time(1)),
inference(demodulation,[status(thm),theory(equality)],[c_3173,c_35499]) ).
tff(c_28506,plain,
! [Event_82: event,Time_83a: $int] :
( ( Event_82 = '#skF_5'(filling,1) )
| ~ happens(Event_82,at_time(Time_83a))
| ( Time_83a = 0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_28269,c_211]) ).
tff(c_35521,plain,
( ( '#skF_7'(waterLevel(3),1) = '#skF_5'(filling,1) )
| ( 1 = 0 ) ),
inference(resolution,[status(thm)],[c_35504,c_28506]) ).
tff(c_35523,plain,
'#skF_7'(waterLevel(3),1) = '#skF_5'(filling,1),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_35521]) ).
tff(c_2317,plain,
! [Fluent_538: fluent,Time_539a: $int] :
( terminates('#skF_7'(Fluent_538,Time_539a),Fluent_538,at_time(Time_539a))
| initiates('#skF_7'(Fluent_538,Time_539a),Fluent_538,at_time(Time_539a))
| releasedAt(Fluent_538,at_time($sum(1,Time_539a)))
| ~ releasedAt(Fluent_538,at_time(Time_539a)) ),
inference(cnfTransformation,[status(thm)],[f_144]) ).
tff(c_2346,plain,
! [Fluent_538: fluent,Time_539a: $int] :
( ( filling = Fluent_538 )
| initiates('#skF_7'(Fluent_538,Time_539a),Fluent_538,at_time(Time_539a))
| releasedAt(Fluent_538,at_time($sum(1,Time_539a)))
| ~ releasedAt(Fluent_538,at_time(Time_539a)) ),
inference(resolution,[status(thm)],[c_2317,c_225]) ).
tff(c_35550,plain,
( ( waterLevel(3) = filling )
| initiates('#skF_5'(filling,1),waterLevel(3),at_time(1))
| releasedAt(waterLevel(3),at_time($sum(1,1)))
| ~ releasedAt(waterLevel(3),at_time(1)) ),
inference(superposition,[status(thm),theory(equality)],[c_35523,c_2346]) ).
tff(c_35572,plain,
( initiates('#skF_5'(filling,1),waterLevel(3),at_time(1))
| releasedAt(waterLevel(3),at_time($sum(1,1)))
| ~ releasedAt(waterLevel(3),at_time(1)) ),
inference(negUnitSimplification,[status(thm)],[c_268,c_35550]) ).
tff(c_35574,plain,
( initiates('#skF_5'(filling,1),waterLevel(3),at_time(1))
| releasedAt(waterLevel(3),at_time(2))
| ~ releasedAt(waterLevel(3),at_time(1)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_35572]) ).
tff(c_35585,plain,
~ releasedAt(waterLevel(3),at_time(1)),
inference(splitLeft,[status(thm)],[c_35574]) ).
tff(c_35933,plain,
! [Time_71a: $int] :
( ( $sum(1,Time_71a) != 1 )
| ~ happens('#skF_6'(filling,0),at_time(Time_71a)) ),
inference(resolution,[status(thm)],[c_3440,c_35585]) ).
tff(c_35936,plain,
~ happens('#skF_6'(filling,0),at_time(0)),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_35933]) ).
tff(c_35968,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3173,c_35936]) ).
tff(c_35971,plain,
( releasedAt(waterLevel(3),at_time(2))
| initiates('#skF_5'(filling,1),waterLevel(3),at_time(1)) ),
inference(splitRight,[status(thm)],[c_35574]) ).
tff(c_36159,plain,
initiates('#skF_5'(filling,1),waterLevel(3),at_time(1)),
inference(splitLeft,[status(thm)],[c_35971]) ).
tff(c_272,plain,
! [Event_50: event,Fluent_52: fluent,Time_51a: $int] :
( ~ initiates(Event_50,Fluent_52,at_time(Time_51a))
| ~ releasedAt(Fluent_52,at_time($sum(1,Time_51a)))
| ~ happens(Event_50,at_time(Time_51a)) ),
inference(cnfTransformation,[status(thm)],[f_184]) ).
tff(c_36218,plain,
( ~ releasedAt(waterLevel(3),at_time($sum(1,1)))
| ~ happens('#skF_5'(filling,1),at_time(1)) ),
inference(resolution,[status(thm)],[c_36159,c_272]) ).
tff(c_36298,plain,
~ releasedAt(waterLevel(3),at_time($sum(1,1))),
inference(demodulation,[status(thm),theory(equality)],[c_28236,c_36218]) ).
tff(c_36300,plain,
~ releasedAt(waterLevel(3),at_time(2)),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_36298]) ).
tff(c_36334,plain,
( ( '#skF_8'(waterLevel(3),2) = '#skF_6'(filling,0) )
| ( waterLevel(3) = filling )
| holdsAt(waterLevel(3),at_time($sum(1,2)))
| ~ holdsAt(waterLevel(3),at_time(2)) ),
inference(resolution,[status(thm)],[c_3419,c_36300]) ).
tff(c_36458,plain,
( ( '#skF_8'(waterLevel(3),2) = '#skF_6'(filling,0) )
| ( waterLevel(3) = filling )
| holdsAt(waterLevel(3),at_time($sum(1,2))) ),
inference(demodulation,[status(thm),theory(equality)],[c_25968,c_36334]) ).
tff(c_36460,plain,
( ( '#skF_8'(waterLevel(3),2) = '#skF_6'(filling,0) )
| holdsAt(waterLevel(3),at_time($sum(1,2))) ),
inference(negUnitSimplification,[status(thm)],[c_268,c_36458]) ).
tff(c_36462,plain,
( ( '#skF_8'(waterLevel(3),2) = '#skF_6'(filling,0) )
| holdsAt(waterLevel(3),at_time(3)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_36460]) ).
tff(c_36798,plain,
'#skF_8'(waterLevel(3),2) = '#skF_6'(filling,0),
inference(negUnitSimplification,[status(thm)],[c_196,c_36462]) ).
tff(c_2759,plain,
! [Fluent_626: fluent,Time_39a: $int,Time_628a: $int] :
( happens('#skF_8'(Fluent_626,Time_39a),at_time(Time_39a))
| releasedAt(Fluent_626,at_time(Time_39a))
| ( filling = Fluent_626 )
| holdsAt(Fluent_626,at_time($sum(1,Time_628a)))
| ( $sum(1,Time_628a) != $sum(1,Time_39a) )
| ~ holdsAt(Fluent_626,at_time(Time_628a)) ),
inference(resolution,[status(thm)],[c_2689,c_292]) ).
tff(c_2763,plain,
! [Fluent_626: fluent,Time_39a: $int] :
( happens('#skF_8'(Fluent_626,Time_39a),at_time(Time_39a))
| releasedAt(Fluent_626,at_time(Time_39a))
| ( filling = Fluent_626 )
| holdsAt(Fluent_626,at_time($sum(1,Time_39a)))
| ~ holdsAt(Fluent_626,at_time(Time_39a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2759]) ).
tff(c_36337,plain,
( happens('#skF_8'(waterLevel(3),2),at_time(2))
| ( waterLevel(3) = filling )
| holdsAt(waterLevel(3),at_time($sum(1,2)))
| ~ holdsAt(waterLevel(3),at_time(2)) ),
inference(resolution,[status(thm)],[c_2763,c_36300]) ).
tff(c_36466,plain,
( happens('#skF_8'(waterLevel(3),2),at_time(2))
| ( waterLevel(3) = filling )
| holdsAt(waterLevel(3),at_time($sum(1,2))) ),
inference(demodulation,[status(thm),theory(equality)],[c_25968,c_36337]) ).
tff(c_36468,plain,
( happens('#skF_8'(waterLevel(3),2),at_time(2))
| holdsAt(waterLevel(3),at_time($sum(1,2))) ),
inference(negUnitSimplification,[status(thm)],[c_268,c_36466]) ).
tff(c_36470,plain,
( happens('#skF_8'(waterLevel(3),2),at_time(2))
| holdsAt(waterLevel(3),at_time(3)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_36468]) ).
tff(c_36813,plain,
( happens('#skF_6'(filling,0),at_time(2))
| holdsAt(waterLevel(3),at_time(3)) ),
inference(demodulation,[status(thm),theory(equality)],[c_36798,c_36470]) ).
tff(c_36814,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_196,c_3665,c_36813]) ).
tff(c_36818,plain,
~ initiates('#skF_5'(filling,1),waterLevel(3),at_time(1)),
inference(splitRight,[status(thm)],[c_35971]) ).
tff(c_36997,plain,
~ holdsAt(waterLevel(3),at_time(1)),
inference(resolution,[status(thm)],[c_28504,c_36818]) ).
tff(c_37001,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_25826,c_36997]) ).
tff(c_37005,plain,
happens('#skF_6'(filling,0),at_time(2)),
inference(splitRight,[status(thm)],[c_3663]) ).
tff(c_37012,plain,
( ( overflow = '#skF_6'(filling,0) )
| ( 2 = 0 ) ),
inference(resolution,[status(thm)],[c_37005,c_211]) ).
tff(c_37021,plain,
2 = 0,
inference(negUnitSimplification,[status(thm)],[c_3464,c_37012]) ).
tff(c_37024,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_37021]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CSR310_1 : TPTP v9.0.0. Released v9.1.0.
% 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n005.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Apr 9 20:10:57 EDT 2025
% 0.13/0.34 % CPUTime :
% 21.21/7.11 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.21/7.13
% 21.21/7.13 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------