%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : CSR004+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:15:04 AM UTC 2026
% Result : Theorem 0.38s 0.65s
% Output : Proof 0.38s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(stoppedin_defn,axiom,
! [Time1,Fluent,Time2] :
( stoppedIn(Time1,Fluent,Time2)
<=> ? [Event,Time] :
( terminates(Event,Fluent,Time)
& less(Time,Time2)
& less(Time1,Time)
& happens(Event,Time) ) ),
file('CSR001+0.ax',stoppedin_defn) ).
fof(startedin_defn,axiom,
! [Time1,Time2,Fluent] :
( startedIn(Time1,Fluent,Time2)
<=> ? [Event,Time] :
( initiates(Event,Fluent,Time)
& less(Time,Time2)
& less(Time1,Time)
& happens(Event,Time) ) ),
file('CSR001+0.ax',startedin_defn) ).
fof(change_holding,axiom,
! [Event,Time,Fluent,Fluent2,Offset] :
( ( ~ stoppedIn(Time,Fluent,plus(Time,Offset))
& trajectory(Fluent,Time,Fluent2,Offset)
& less(n0,Offset)
& initiates(Event,Fluent,Time)
& happens(Event,Time) )
=> holdsAt(Fluent2,plus(Time,Offset)) ),
file('CSR001+0.ax',change_holding) ).
fof(antitrajectory,axiom,
! [Event,Time1,Fluent1,Time2,Fluent2] :
( ( ~ startedIn(Time1,Fluent1,plus(Time1,Time2))
& antitrajectory(Fluent1,Time1,Fluent2,Time2)
& less(n0,Time2)
& terminates(Event,Fluent1,Time1)
& happens(Event,Time1) )
=> holdsAt(Fluent2,plus(Time1,Time2)) ),
file('CSR001+0.ax',antitrajectory) ).
fof(keep_holding,axiom,
! [Fluent,Time] :
( ( ~ ? [Event] :
( terminates(Event,Fluent,Time)
& happens(Event,Time) )
& ~ releasedAt(Fluent,plus(Time,n1))
& holdsAt(Fluent,Time) )
=> holdsAt(Fluent,plus(Time,n1)) ),
file('CSR001+0.ax',keep_holding) ).
fof(keep_not_holding,axiom,
! [Fluent,Time] :
( ( ~ ? [Event] :
( initiates(Event,Fluent,Time)
& happens(Event,Time) )
& ~ releasedAt(Fluent,plus(Time,n1))
& ~ holdsAt(Fluent,Time) )
=> ~ holdsAt(Fluent,plus(Time,n1)) ),
file('CSR001+0.ax',keep_not_holding) ).
fof(keep_released,axiom,
! [Fluent,Time] :
( ( ~ ? [Event] :
( ( terminates(Event,Fluent,Time)
| initiates(Event,Fluent,Time) )
& happens(Event,Time) )
& releasedAt(Fluent,Time) )
=> releasedAt(Fluent,plus(Time,n1)) ),
file('CSR001+0.ax',keep_released) ).
fof(keep_not_released,axiom,
! [Fluent,Time] :
( ( ~ ? [Event] :
( releases(Event,Fluent,Time)
& happens(Event,Time) )
& ~ releasedAt(Fluent,Time) )
=> ~ releasedAt(Fluent,plus(Time,n1)) ),
file('CSR001+0.ax',keep_not_released) ).
fof(happens_holds,axiom,
! [Event,Time,Fluent] :
( ( initiates(Event,Fluent,Time)
& happens(Event,Time) )
=> holdsAt(Fluent,plus(Time,n1)) ),
file('CSR001+0.ax',happens_holds) ).
fof(happens_terminates_not_holds,axiom,
! [Event,Time,Fluent] :
( ( terminates(Event,Fluent,Time)
& happens(Event,Time) )
=> ~ holdsAt(Fluent,plus(Time,n1)) ),
file('CSR001+0.ax',happens_terminates_not_holds) ).
fof(happens_releases,axiom,
! [Event,Time,Fluent] :
( ( releases(Event,Fluent,Time)
& happens(Event,Time) )
=> releasedAt(Fluent,plus(Time,n1)) ),
file('CSR001+0.ax',happens_releases) ).
fof(happens_not_released,axiom,
! [Event,Time,Fluent] :
( ( ( terminates(Event,Fluent,Time)
| initiates(Event,Fluent,Time) )
& happens(Event,Time) )
=> ~ releasedAt(Fluent,plus(Time,n1)) ),
file('CSR001+0.ax',happens_not_released) ).
fof(initiates_all_defn,axiom,
! [Event,Fluent,Time] :
( initiates(Event,Fluent,Time)
<=> ( ? [Height] :
( Fluent = waterLevel(Height)
& Event = overflow
& holdsAt(waterLevel(Height),Time) )
| ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOff
& holdsAt(waterLevel(Height),Time) )
| ( Fluent = spilling
& Event = overflow )
| ( Fluent = filling
& Event = tapOn ) ) ),
file('CSR001+1.ax',initiates_all_defn) ).
fof(terminates_all_defn,axiom,
! [Event,Fluent,Time] :
( terminates(Event,Fluent,Time)
<=> ( ( Fluent = filling
& Event = overflow )
| ( Fluent = filling
& Event = tapOff ) ) ),
file('CSR001+1.ax',terminates_all_defn) ).
fof(releases_all_defn,axiom,
! [Event,Fluent,Time] :
( releases(Event,Fluent,Time)
<=> ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOn ) ),
file('CSR001+1.ax',releases_all_defn) ).
fof(happens_all_defn,axiom,
! [Event,Time] :
( happens(Event,Time)
<=> ( ( Event = overflow
& holdsAt(filling,Time)
& holdsAt(waterLevel(n3),Time) )
| ( Time = n0
& Event = tapOn ) ) ),
file('CSR001+1.ax',happens_all_defn) ).
fof(change_of_waterLevel,axiom,
! [Height1,Time,Height2,Offset] :
( ( Height2 = plus(Height1,Offset)
& holdsAt(waterLevel(Height1),Time) )
=> trajectory(filling,Time,waterLevel(Height2),Offset) ),
file('CSR001+1.ax',change_of_waterLevel) ).
fof(same_waterLevel,axiom,
! [Time,Height1,Height2] :
( ( holdsAt(waterLevel(Height2),Time)
& holdsAt(waterLevel(Height1),Time) )
=> Height1 = Height2 ),
file('CSR001+1.ax',same_waterLevel) ).
fof(tapOff_not_tapOn,axiom,
tapOff != tapOn,
file('CSR001+1.ax',tapOff_not_tapOn) ).
fof(tapOff_not_overflow,axiom,
tapOff != overflow,
file('CSR001+1.ax',tapOff_not_overflow) ).
fof(overflow_not_tapOn,axiom,
overflow != tapOn,
file('CSR001+1.ax',overflow_not_tapOn) ).
fof(filling_not_waterLevel,axiom,
! [X] : filling != waterLevel(X),
file('CSR001+1.ax',filling_not_waterLevel) ).
fof(spilling_not_waterLevel,axiom,
! [X] : spilling != waterLevel(X),
file('CSR001+1.ax',spilling_not_waterLevel) ).
fof(filling_not_spilling,axiom,
filling != spilling,
file('CSR001+1.ax',filling_not_spilling) ).
fof(distinct_waterLevels,axiom,
! [X,Y] :
( waterLevel(X) = waterLevel(Y)
<=> X = Y ),
file('CSR001+1.ax',distinct_waterLevels) ).
fof(plus0_0,axiom,
plus(n0,n0) = n0,
file('theBenchmark.p',plus0_0) ).
fof(plus0_1,axiom,
plus(n0,n1) = n1,
file('theBenchmark.p',plus0_1) ).
fof(plus0_2,axiom,
plus(n0,n2) = n2,
file('theBenchmark.p',plus0_2) ).
fof(plus0_3,axiom,
plus(n0,n3) = n3,
file('theBenchmark.p',plus0_3) ).
fof(plus1_1,axiom,
plus(n1,n1) = n2,
file('theBenchmark.p',plus1_1) ).
fof(plus1_2,axiom,
plus(n1,n2) = n3,
file('theBenchmark.p',plus1_2) ).
fof(plus1_3,axiom,
plus(n1,n3) = n4,
file('theBenchmark.p',plus1_3) ).
fof(plus2_2,axiom,
plus(n2,n2) = n4,
file('theBenchmark.p',plus2_2) ).
fof(plus2_3,axiom,
plus(n2,n3) = n5,
file('theBenchmark.p',plus2_3) ).
fof(plus3_3,axiom,
plus(n3,n3) = n6,
file('theBenchmark.p',plus3_3) ).
fof(symmetry_of_plus,axiom,
! [X,Y] : plus(X,Y) = plus(Y,X),
file('theBenchmark.p',symmetry_of_plus) ).
fof(less_or_equal,axiom,
! [X,Y] :
( less_or_equal(X,Y)
<=> ( X = Y
| less(X,Y) ) ),
file('theBenchmark.p',less_or_equal) ).
fof(less0,axiom,
~ ? [X] : less(X,n0),
file('theBenchmark.p',less0) ).
fof(less1,axiom,
! [X] :
( less(X,n1)
<=> less_or_equal(X,n0) ),
file('theBenchmark.p',less1) ).
fof(less2,axiom,
! [X] :
( less(X,n2)
<=> less_or_equal(X,n1) ),
file('theBenchmark.p',less2) ).
fof(less3,axiom,
! [X] :
( less(X,n3)
<=> less_or_equal(X,n2) ),
file('theBenchmark.p',less3) ).
fof(less4,axiom,
! [X] :
( less(X,n4)
<=> less_or_equal(X,n3) ),
file('theBenchmark.p',less4) ).
fof(less5,axiom,
! [X] :
( less(X,n5)
<=> less_or_equal(X,n4) ),
file('theBenchmark.p',less5) ).
fof(less6,axiom,
! [X] :
( less(X,n6)
<=> less_or_equal(X,n5) ),
file('theBenchmark.p',less6) ).
fof(less7,axiom,
! [X] :
( less(X,n7)
<=> less_or_equal(X,n6) ),
file('theBenchmark.p',less7) ).
fof(less8,axiom,
! [X] :
( less(X,n8)
<=> less_or_equal(X,n7) ),
file('theBenchmark.p',less8) ).
fof(less9,axiom,
! [X] :
( less(X,n9)
<=> less_or_equal(X,n8) ),
file('theBenchmark.p',less9) ).
fof(less_property,axiom,
! [X,Y] :
( less(X,Y)
<=> ( Y != X
& ~ less(Y,X) ) ),
file('theBenchmark.p',less_property) ).
fof(waterLevel_0,hypothesis,
holdsAt(waterLevel(n0),n0),
file('theBenchmark.p',waterLevel_0) ).
fof(not_filling_0,hypothesis,
~ holdsAt(filling,n0),
file('theBenchmark.p',not_filling_0) ).
fof(not_spilling_0,hypothesis,
~ holdsAt(spilling,n0),
file('theBenchmark.p',not_spilling_0) ).
fof(not_released_waterLevel_0,hypothesis,
! [Height] : ~ releasedAt(waterLevel(Height),n0),
file('theBenchmark.p',not_released_waterLevel_0) ).
fof(not_released_filling_0,hypothesis,
~ releasedAt(filling,n0),
file('theBenchmark.p',not_released_filling_0) ).
fof(not_released_spilling_0,hypothesis,
~ releasedAt(spilling,n0),
file('theBenchmark.p',not_released_spilling_0) ).
fof(waterLevel_3,lemma,
holdsAt(waterLevel(n3),n3),
file('theBenchmark.p',waterLevel_3) ).
fof(filling_3,lemma,
holdsAt(filling,n3),
file('theBenchmark.p',filling_3) ).
fof(overflow_3,conjecture,
happens(overflow,n3),
file('theBenchmark.p',overflow_3) ).
fof(f_1_1,plain,
! [Time1,Fluent,Time2] :
( ( stoppedIn(Time1,Fluent,Time2)
| ! [Event,Time] :
( ~ terminates(Event,Fluent,Time)
| ~ less(Time,Time2)
| ~ less(Time1,Time)
| ~ happens(Event,Time) ) )
& ( ? [Event,Time] :
( terminates(Event,Fluent,Time)
& less(Time,Time2)
& less(Time1,Time)
& happens(Event,Time) )
| ~ stoppedIn(Time1,Fluent,Time2) ) ),
inference(fof_nnf,[status(thm)],[stoppedin_defn]) ).
fof(f_1_2,plain,
! [U_6,U_5,U_4] :
( ( stoppedIn(U_6,U_5,U_4)
| ! [U_3,U_2] :
( ~ terminates(U_3,U_5,U_2)
| ~ less(U_2,U_4)
| ~ less(U_6,U_2)
| ~ happens(U_3,U_2) ) )
& ( ? [U_1,U_0] :
( terminates(U_1,U_5,U_0)
& less(U_0,U_4)
& less(U_6,U_0)
& happens(U_1,U_0) )
| ~ stoppedIn(U_6,U_5,U_4) ) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
( ! [U_12,U_10,U_8] :
( stoppedIn(U_12,U_10,U_8)
| ! [U_3,U_2] :
( ~ terminates(U_3,U_10,U_2)
| ~ less(U_2,U_8)
| ~ less(U_12,U_2)
| ~ happens(U_3,U_2) ) )
& ! [U_11,U_9,U_7] :
( ? [U_1,U_0] :
( terminates(U_1,U_9,U_0)
& less(U_0,U_7)
& less(U_11,U_0)
& happens(U_1,U_0) )
| ~ stoppedIn(U_11,U_9,U_7) ) ),
inference(miniscope,[status(thm)],[f_1_2]) ).
fof(f_1_4,plain,
( ! [U_12,U_10,U_8] :
( stoppedIn(U_12,U_10,U_8)
| ! [U_3,U_2] :
( ~ terminates(U_3,U_10,U_2)
| ~ less(U_2,U_8)
| ~ less(U_12,U_2)
| ~ happens(U_3,U_2) ) )
& ! [U_11,U_9,U_7] :
( ? [U_0] :
( terminates(sK1(U_11,U_9,U_7),U_9,U_0)
& less(U_0,U_7)
& less(U_11,U_0)
& happens(sK1(U_11,U_9,U_7),U_0) )
| ~ stoppedIn(U_11,U_9,U_7) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_1,sK1(U_11,U_9,U_7))],[f_1_3]) ).
fof(f_1_5,plain,
( ! [U_12,U_10,U_8] :
( stoppedIn(U_12,U_10,U_8)
| ! [U_3,U_2] :
( ~ terminates(U_3,U_10,U_2)
| ~ less(U_2,U_8)
| ~ less(U_12,U_2)
| ~ happens(U_3,U_2) ) )
& ! [U_11,U_9,U_7] :
( ( terminates(sK1(U_11,U_9,U_7),U_9,sK2(U_11,U_9,U_7))
& less(sK2(U_11,U_9,U_7),U_7)
& less(U_11,sK2(U_11,U_9,U_7))
& happens(sK1(U_11,U_9,U_7),sK2(U_11,U_9,U_7)) )
| ~ stoppedIn(U_11,U_9,U_7) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_0,sK2(U_11,U_9,U_7))],[f_1_4]) ).
cnf(f_1_6,plain,
( happens(sK1(U_11,U_9,U_7),sK2(U_11,U_9,U_7))
| ~ stoppedIn(U_11,U_9,U_7) ),
inference(clausify,[status(thm)],[f_1_5]) ).
cnf(f_1_7,plain,
( less(U_11,sK2(U_11,U_9,U_7))
| ~ stoppedIn(U_11,U_9,U_7) ),
inference(clausify,[status(thm)],[f_1_5]) ).
cnf(f_1_8,plain,
( less(sK2(U_11,U_9,U_7),U_7)
| ~ stoppedIn(U_11,U_9,U_7) ),
inference(clausify,[status(thm)],[f_1_5]) ).
cnf(f_1_9,plain,
( terminates(sK1(U_11,U_9,U_7),U_9,sK2(U_11,U_9,U_7))
| ~ stoppedIn(U_11,U_9,U_7) ),
inference(clausify,[status(thm)],[f_1_5]) ).
cnf(f_1_10,plain,
( stoppedIn(U_12,U_10,U_8)
| ~ terminates(U_3,U_10,U_2)
| ~ less(U_2,U_8)
| ~ less(U_12,U_2)
| ~ happens(U_3,U_2) ),
inference(clausify,[status(thm)],[f_1_5]) ).
fof(f_2_1,plain,
! [Time1,Time2,Fluent] :
( ( startedIn(Time1,Fluent,Time2)
| ! [Event,Time] :
( ~ initiates(Event,Fluent,Time)
| ~ less(Time,Time2)
| ~ less(Time1,Time)
| ~ happens(Event,Time) ) )
& ( ? [Event,Time] :
( initiates(Event,Fluent,Time)
& less(Time,Time2)
& less(Time1,Time)
& happens(Event,Time) )
| ~ startedIn(Time1,Fluent,Time2) ) ),
inference(fof_nnf,[status(thm)],[startedin_defn]) ).
fof(f_2_2,plain,
! [U_19,U_18,U_17] :
( ( startedIn(U_19,U_17,U_18)
| ! [U_16,U_15] :
( ~ initiates(U_16,U_17,U_15)
| ~ less(U_15,U_18)
| ~ less(U_19,U_15)
| ~ happens(U_16,U_15) ) )
& ( ? [U_14,U_13] :
( initiates(U_14,U_17,U_13)
& less(U_13,U_18)
& less(U_19,U_13)
& happens(U_14,U_13) )
| ~ startedIn(U_19,U_17,U_18) ) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
( ! [U_25,U_23,U_21] :
( startedIn(U_25,U_21,U_23)
| ! [U_16,U_15] :
( ~ initiates(U_16,U_21,U_15)
| ~ less(U_15,U_23)
| ~ less(U_25,U_15)
| ~ happens(U_16,U_15) ) )
& ! [U_24,U_22,U_20] :
( ? [U_14,U_13] :
( initiates(U_14,U_20,U_13)
& less(U_13,U_22)
& less(U_24,U_13)
& happens(U_14,U_13) )
| ~ startedIn(U_24,U_20,U_22) ) ),
inference(miniscope,[status(thm)],[f_2_2]) ).
fof(f_2_4,plain,
( ! [U_25,U_23,U_21] :
( startedIn(U_25,U_21,U_23)
| ! [U_16,U_15] :
( ~ initiates(U_16,U_21,U_15)
| ~ less(U_15,U_23)
| ~ less(U_25,U_15)
| ~ happens(U_16,U_15) ) )
& ! [U_24,U_22,U_20] :
( ? [U_13] :
( initiates(sK3(U_24,U_22,U_20),U_20,U_13)
& less(U_13,U_22)
& less(U_24,U_13)
& happens(sK3(U_24,U_22,U_20),U_13) )
| ~ startedIn(U_24,U_20,U_22) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_14,sK3(U_24,U_22,U_20))],[f_2_3]) ).
fof(f_2_5,plain,
( ! [U_25,U_23,U_21] :
( startedIn(U_25,U_21,U_23)
| ! [U_16,U_15] :
( ~ initiates(U_16,U_21,U_15)
| ~ less(U_15,U_23)
| ~ less(U_25,U_15)
| ~ happens(U_16,U_15) ) )
& ! [U_24,U_22,U_20] :
( ( initiates(sK3(U_24,U_22,U_20),U_20,sK4(U_24,U_22,U_20))
& less(sK4(U_24,U_22,U_20),U_22)
& less(U_24,sK4(U_24,U_22,U_20))
& happens(sK3(U_24,U_22,U_20),sK4(U_24,U_22,U_20)) )
| ~ startedIn(U_24,U_20,U_22) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_13,sK4(U_24,U_22,U_20))],[f_2_4]) ).
cnf(f_2_6,plain,
( happens(sK3(U_24,U_22,U_20),sK4(U_24,U_22,U_20))
| ~ startedIn(U_24,U_20,U_22) ),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_7,plain,
( less(U_24,sK4(U_24,U_22,U_20))
| ~ startedIn(U_24,U_20,U_22) ),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_8,plain,
( less(sK4(U_24,U_22,U_20),U_22)
| ~ startedIn(U_24,U_20,U_22) ),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_9,plain,
( initiates(sK3(U_24,U_22,U_20),U_20,sK4(U_24,U_22,U_20))
| ~ startedIn(U_24,U_20,U_22) ),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_10,plain,
( startedIn(U_25,U_21,U_23)
| ~ initiates(U_16,U_21,U_15)
| ~ less(U_15,U_23)
| ~ less(U_25,U_15)
| ~ happens(U_16,U_15) ),
inference(clausify,[status(thm)],[f_2_5]) ).
fof(f_3_1,plain,
! [Event,Time,Fluent,Fluent2,Offset] :
( holdsAt(Fluent2,plus(Time,Offset))
| stoppedIn(Time,Fluent,plus(Time,Offset))
| ~ trajectory(Fluent,Time,Fluent2,Offset)
| ~ less(n0,Offset)
| ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(fof_nnf,[status(thm)],[change_holding]) ).
fof(f_3_2,plain,
! [U_30,U_29,U_28,U_27,U_26] :
( holdsAt(U_27,plus(U_29,U_26))
| stoppedIn(U_29,U_28,plus(U_29,U_26))
| ~ trajectory(U_28,U_29,U_27,U_26)
| ~ less(n0,U_26)
| ~ initiates(U_30,U_28,U_29)
| ~ happens(U_30,U_29) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
cnf(f_3_3,plain,
( holdsAt(U_27,plus(U_29,U_26))
| stoppedIn(U_29,U_28,plus(U_29,U_26))
| ~ trajectory(U_28,U_29,U_27,U_26)
| ~ less(n0,U_26)
| ~ initiates(U_30,U_28,U_29)
| ~ happens(U_30,U_29) ),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
! [Event,Time1,Fluent1,Time2,Fluent2] :
( holdsAt(Fluent2,plus(Time1,Time2))
| startedIn(Time1,Fluent1,plus(Time1,Time2))
| ~ antitrajectory(Fluent1,Time1,Fluent2,Time2)
| ~ less(n0,Time2)
| ~ terminates(Event,Fluent1,Time1)
| ~ happens(Event,Time1) ),
inference(fof_nnf,[status(thm)],[antitrajectory]) ).
fof(f_4_2,plain,
! [U_35,U_34,U_33,U_32,U_31] :
( holdsAt(U_31,plus(U_34,U_32))
| startedIn(U_34,U_33,plus(U_34,U_32))
| ~ antitrajectory(U_33,U_34,U_31,U_32)
| ~ less(n0,U_32)
| ~ terminates(U_35,U_33,U_34)
| ~ happens(U_35,U_34) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
cnf(f_4_3,plain,
( holdsAt(U_31,plus(U_34,U_32))
| startedIn(U_34,U_33,plus(U_34,U_32))
| ~ antitrajectory(U_33,U_34,U_31,U_32)
| ~ less(n0,U_32)
| ~ terminates(U_35,U_33,U_34)
| ~ happens(U_35,U_34) ),
inference(clausify,[status(thm)],[f_4_2]) ).
fof(f_5_1,plain,
! [Fluent,Time] :
( holdsAt(Fluent,plus(Time,n1))
| ? [Event] :
( terminates(Event,Fluent,Time)
& happens(Event,Time) )
| releasedAt(Fluent,plus(Time,n1))
| ~ holdsAt(Fluent,Time) ),
inference(fof_nnf,[status(thm)],[keep_holding]) ).
fof(f_5_2,plain,
! [U_38,U_37] :
( holdsAt(U_38,plus(U_37,n1))
| ? [U_36] :
( terminates(U_36,U_38,U_37)
& happens(U_36,U_37) )
| releasedAt(U_38,plus(U_37,n1))
| ~ holdsAt(U_38,U_37) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
! [U_38,U_37] :
( holdsAt(U_38,plus(U_37,n1))
| ( terminates(sK5(U_38,U_37),U_38,U_37)
& happens(sK5(U_38,U_37),U_37) )
| releasedAt(U_38,plus(U_37,n1))
| ~ holdsAt(U_38,U_37) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_36,sK5(U_38,U_37))],[f_5_2]) ).
cnf(f_5_4,plain,
( happens(sK5(U_38,U_37),U_37)
| releasedAt(U_38,plus(U_37,n1))
| ~ holdsAt(U_38,U_37)
| holdsAt(U_38,plus(U_37,n1)) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(f_5_5,plain,
( terminates(sK5(U_38,U_37),U_38,U_37)
| releasedAt(U_38,plus(U_37,n1))
| ~ holdsAt(U_38,U_37)
| holdsAt(U_38,plus(U_37,n1)) ),
inference(clausify,[status(thm)],[f_5_3]) ).
fof(f_6_1,plain,
! [Fluent,Time] :
( ~ holdsAt(Fluent,plus(Time,n1))
| ? [Event] :
( initiates(Event,Fluent,Time)
& happens(Event,Time) )
| releasedAt(Fluent,plus(Time,n1))
| holdsAt(Fluent,Time) ),
inference(fof_nnf,[status(thm)],[keep_not_holding]) ).
fof(f_6_2,plain,
! [U_41,U_40] :
( ~ holdsAt(U_41,plus(U_40,n1))
| ? [U_39] :
( initiates(U_39,U_41,U_40)
& happens(U_39,U_40) )
| releasedAt(U_41,plus(U_40,n1))
| holdsAt(U_41,U_40) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
! [U_41,U_40] :
( ~ holdsAt(U_41,plus(U_40,n1))
| ( initiates(sK6(U_41,U_40),U_41,U_40)
& happens(sK6(U_41,U_40),U_40) )
| releasedAt(U_41,plus(U_40,n1))
| holdsAt(U_41,U_40) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_39,sK6(U_41,U_40))],[f_6_2]) ).
cnf(f_6_4,plain,
( happens(sK6(U_41,U_40),U_40)
| releasedAt(U_41,plus(U_40,n1))
| holdsAt(U_41,U_40)
| ~ holdsAt(U_41,plus(U_40,n1)) ),
inference(clausify,[status(thm)],[f_6_3]) ).
cnf(f_6_5,plain,
( initiates(sK6(U_41,U_40),U_41,U_40)
| releasedAt(U_41,plus(U_40,n1))
| holdsAt(U_41,U_40)
| ~ holdsAt(U_41,plus(U_40,n1)) ),
inference(clausify,[status(thm)],[f_6_3]) ).
fof(f_7_1,plain,
! [Fluent,Time] :
( releasedAt(Fluent,plus(Time,n1))
| ? [Event] :
( ( terminates(Event,Fluent,Time)
| initiates(Event,Fluent,Time) )
& happens(Event,Time) )
| ~ releasedAt(Fluent,Time) ),
inference(fof_nnf,[status(thm)],[keep_released]) ).
fof(f_7_2,plain,
! [U_44,U_43] :
( releasedAt(U_44,plus(U_43,n1))
| ? [U_42] :
( ( terminates(U_42,U_44,U_43)
| initiates(U_42,U_44,U_43) )
& happens(U_42,U_43) )
| ~ releasedAt(U_44,U_43) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
! [U_44,U_43] :
( releasedAt(U_44,plus(U_43,n1))
| ( ( terminates(sK7(U_44,U_43),U_44,U_43)
| initiates(sK7(U_44,U_43),U_44,U_43) )
& happens(sK7(U_44,U_43),U_43) )
| ~ releasedAt(U_44,U_43) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_42,sK7(U_44,U_43))],[f_7_2]) ).
cnf(f_7_4,plain,
( happens(sK7(U_44,U_43),U_43)
| ~ releasedAt(U_44,U_43)
| releasedAt(U_44,plus(U_43,n1)) ),
inference(clausify,[status(thm)],[f_7_3]) ).
cnf(f_7_5,plain,
( terminates(sK7(U_44,U_43),U_44,U_43)
| initiates(sK7(U_44,U_43),U_44,U_43)
| ~ releasedAt(U_44,U_43)
| releasedAt(U_44,plus(U_43,n1)) ),
inference(clausify,[status(thm)],[f_7_3]) ).
fof(f_8_1,plain,
! [Fluent,Time] :
( ~ releasedAt(Fluent,plus(Time,n1))
| ? [Event] :
( releases(Event,Fluent,Time)
& happens(Event,Time) )
| releasedAt(Fluent,Time) ),
inference(fof_nnf,[status(thm)],[keep_not_released]) ).
fof(f_8_2,plain,
! [U_47,U_46] :
( ~ releasedAt(U_47,plus(U_46,n1))
| ? [U_45] :
( releases(U_45,U_47,U_46)
& happens(U_45,U_46) )
| releasedAt(U_47,U_46) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
! [U_47,U_46] :
( ~ releasedAt(U_47,plus(U_46,n1))
| ( releases(sK8(U_47,U_46),U_47,U_46)
& happens(sK8(U_47,U_46),U_46) )
| releasedAt(U_47,U_46) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_45,sK8(U_47,U_46))],[f_8_2]) ).
cnf(f_8_4,plain,
( happens(sK8(U_47,U_46),U_46)
| releasedAt(U_47,U_46)
| ~ releasedAt(U_47,plus(U_46,n1)) ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_5,plain,
( releases(sK8(U_47,U_46),U_47,U_46)
| releasedAt(U_47,U_46)
| ~ releasedAt(U_47,plus(U_46,n1)) ),
inference(clausify,[status(thm)],[f_8_3]) ).
fof(f_9_1,plain,
! [Event,Time,Fluent] :
( holdsAt(Fluent,plus(Time,n1))
| ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(fof_nnf,[status(thm)],[happens_holds]) ).
fof(f_9_2,plain,
! [U_50,U_49,U_48] :
( holdsAt(U_48,plus(U_49,n1))
| ~ initiates(U_50,U_48,U_49)
| ~ happens(U_50,U_49) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
cnf(f_9_3,plain,
( holdsAt(U_48,plus(U_49,n1))
| ~ initiates(U_50,U_48,U_49)
| ~ happens(U_50,U_49) ),
inference(clausify,[status(thm)],[f_9_2]) ).
fof(f_10_1,plain,
! [Event,Time,Fluent] :
( ~ holdsAt(Fluent,plus(Time,n1))
| ~ terminates(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(fof_nnf,[status(thm)],[happens_terminates_not_holds]) ).
fof(f_10_2,plain,
! [U_53,U_52,U_51] :
( ~ holdsAt(U_51,plus(U_52,n1))
| ~ terminates(U_53,U_51,U_52)
| ~ happens(U_53,U_52) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
cnf(f_10_3,plain,
( ~ holdsAt(U_51,plus(U_52,n1))
| ~ terminates(U_53,U_51,U_52)
| ~ happens(U_53,U_52) ),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,plain,
! [Event,Time,Fluent] :
( releasedAt(Fluent,plus(Time,n1))
| ~ releases(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(fof_nnf,[status(thm)],[happens_releases]) ).
fof(f_11_2,plain,
! [U_56,U_55,U_54] :
( releasedAt(U_54,plus(U_55,n1))
| ~ releases(U_56,U_54,U_55)
| ~ happens(U_56,U_55) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
cnf(f_11_3,plain,
( releasedAt(U_54,plus(U_55,n1))
| ~ releases(U_56,U_54,U_55)
| ~ happens(U_56,U_55) ),
inference(clausify,[status(thm)],[f_11_2]) ).
fof(f_12_1,plain,
! [Event,Time,Fluent] :
( ~ releasedAt(Fluent,plus(Time,n1))
| ( ~ terminates(Event,Fluent,Time)
& ~ initiates(Event,Fluent,Time) )
| ~ happens(Event,Time) ),
inference(fof_nnf,[status(thm)],[happens_not_released]) ).
fof(f_12_2,plain,
! [U_59,U_58,U_57] :
( ~ releasedAt(U_57,plus(U_58,n1))
| ( ~ terminates(U_59,U_57,U_58)
& ~ initiates(U_59,U_57,U_58) )
| ~ happens(U_59,U_58) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
cnf(f_12_3,plain,
( ~ initiates(U_59,U_57,U_58)
| ~ happens(U_59,U_58)
| ~ releasedAt(U_57,plus(U_58,n1)) ),
inference(clausify,[status(thm)],[f_12_2]) ).
cnf(f_12_4,plain,
( ~ terminates(U_59,U_57,U_58)
| ~ happens(U_59,U_58)
| ~ releasedAt(U_57,plus(U_58,n1)) ),
inference(clausify,[status(thm)],[f_12_2]) ).
fof(f_13_1,plain,
! [Event,Fluent,Time] :
( ( initiates(Event,Fluent,Time)
| ( ! [Height] :
( Fluent != waterLevel(Height)
| Event != overflow
| ~ holdsAt(waterLevel(Height),Time) )
& ! [Height] :
( Fluent != waterLevel(Height)
| Event != tapOff
| ~ holdsAt(waterLevel(Height),Time) )
& ( Fluent != spilling
| Event != overflow )
& ( Fluent != filling
| Event != tapOn ) ) )
& ( ? [Height] :
( Fluent = waterLevel(Height)
& Event = overflow
& holdsAt(waterLevel(Height),Time) )
| ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOff
& holdsAt(waterLevel(Height),Time) )
| ( Fluent = spilling
& Event = overflow )
| ( Fluent = filling
& Event = tapOn )
| ~ initiates(Event,Fluent,Time) ) ),
inference(fof_nnf,[status(thm)],[initiates_all_defn]) ).
fof(f_13_2,plain,
! [U_66,U_65,U_64] :
( ( initiates(U_66,U_65,U_64)
| ( ! [U_63] :
( U_65 != waterLevel(U_63)
| U_66 != overflow
| ~ holdsAt(waterLevel(U_63),U_64) )
& ! [U_62] :
( U_65 != waterLevel(U_62)
| U_66 != tapOff
| ~ holdsAt(waterLevel(U_62),U_64) )
& ( U_65 != spilling
| U_66 != overflow )
& ( U_65 != filling
| U_66 != tapOn ) ) )
& ( ? [U_61] :
( U_65 = waterLevel(U_61)
& U_66 = overflow
& holdsAt(waterLevel(U_61),U_64) )
| ? [U_60] :
( U_65 = waterLevel(U_60)
& U_66 = tapOff
& holdsAt(waterLevel(U_60),U_64) )
| ( U_65 = spilling
& U_66 = overflow )
| ( U_65 = filling
& U_66 = tapOn )
| ~ initiates(U_66,U_65,U_64) ) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
( ! [U_72,U_70,U_68] :
( initiates(U_72,U_70,U_68)
| ( ( ! [U_63] :
( U_70 != waterLevel(U_63)
| ~ holdsAt(waterLevel(U_63),U_68) )
| U_72 != overflow )
& ( ! [U_62] :
( U_70 != waterLevel(U_62)
| ~ holdsAt(waterLevel(U_62),U_68) )
| U_72 != tapOff )
& ( U_70 != spilling
| U_72 != overflow )
& ( U_70 != filling
| U_72 != tapOn ) ) )
& ! [U_71,U_69,U_67] :
( ( ? [U_61] :
( U_69 = waterLevel(U_61)
& holdsAt(waterLevel(U_61),U_67) )
& U_71 = overflow )
| ( ? [U_60] :
( U_69 = waterLevel(U_60)
& holdsAt(waterLevel(U_60),U_67) )
& U_71 = tapOff )
| ( U_69 = spilling
& U_71 = overflow )
| ( U_69 = filling
& U_71 = tapOn )
| ~ initiates(U_71,U_69,U_67) ) ),
inference(miniscope,[status(thm)],[f_13_2]) ).
fof(f_13_4,plain,
( ! [U_72,U_70,U_68] :
( initiates(U_72,U_70,U_68)
| ( ( ! [U_63] :
( U_70 != waterLevel(U_63)
| ~ holdsAt(waterLevel(U_63),U_68) )
| U_72 != overflow )
& ( ! [U_62] :
( U_70 != waterLevel(U_62)
| ~ holdsAt(waterLevel(U_62),U_68) )
| U_72 != tapOff )
& ( U_70 != spilling
| U_72 != overflow )
& ( U_70 != filling
| U_72 != tapOn ) ) )
& ! [U_71,U_69,U_67] :
( ( ? [U_61] :
( U_69 = waterLevel(U_61)
& holdsAt(waterLevel(U_61),U_67) )
& U_71 = overflow )
| ( U_69 = waterLevel(sK9(U_71,U_69,U_67))
& holdsAt(waterLevel(sK9(U_71,U_69,U_67)),U_67)
& U_71 = tapOff )
| ( U_69 = spilling
& U_71 = overflow )
| ( U_69 = filling
& U_71 = tapOn )
| ~ initiates(U_71,U_69,U_67) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_60,sK9(U_71,U_69,U_67))],[f_13_3]) ).
fof(f_13_5,plain,
( ! [U_72,U_70,U_68] :
( initiates(U_72,U_70,U_68)
| ( ( ! [U_63] :
( U_70 != waterLevel(U_63)
| ~ holdsAt(waterLevel(U_63),U_68) )
| U_72 != overflow )
& ( ! [U_62] :
( U_70 != waterLevel(U_62)
| ~ holdsAt(waterLevel(U_62),U_68) )
| U_72 != tapOff )
& ( U_70 != spilling
| U_72 != overflow )
& ( U_70 != filling
| U_72 != tapOn ) ) )
& ! [U_71,U_69,U_67] :
( ( U_69 = waterLevel(sK10(U_71,U_69,U_67))
& holdsAt(waterLevel(sK10(U_71,U_69,U_67)),U_67)
& U_71 = overflow )
| ( U_69 = waterLevel(sK9(U_71,U_69,U_67))
& holdsAt(waterLevel(sK9(U_71,U_69,U_67)),U_67)
& U_71 = tapOff )
| ( U_69 = spilling
& U_71 = overflow )
| ( U_69 = filling
& U_71 = tapOn )
| ~ initiates(U_71,U_69,U_67) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_61,sK10(U_71,U_69,U_67))],[f_13_4]) ).
cnf(f_13_6,plain,
( U_71 = overflow
| U_71 = overflow
| U_71 = tapOff
| U_71 = tapOn
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_7,plain,
( U_69 = spilling
| U_71 = overflow
| U_71 = tapOff
| U_71 = tapOn
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_8,plain,
( holdsAt(waterLevel(sK9(U_71,U_69,U_67)),U_67)
| U_71 = tapOn
| U_71 = overflow
| U_71 = overflow
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_9,plain,
( U_69 = waterLevel(sK9(U_71,U_69,U_67))
| U_71 = tapOn
| U_71 = overflow
| U_71 = overflow
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_10,plain,
( holdsAt(waterLevel(sK9(U_71,U_69,U_67)),U_67)
| U_71 = tapOn
| U_69 = spilling
| U_71 = overflow
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_11,plain,
( U_69 = waterLevel(sK9(U_71,U_69,U_67))
| U_71 = tapOn
| U_69 = spilling
| U_71 = overflow
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_12,plain,
( holdsAt(waterLevel(sK10(U_71,U_69,U_67)),U_67)
| U_71 = overflow
| U_71 = tapOff
| U_71 = tapOn
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_13,plain,
( U_69 = waterLevel(sK10(U_71,U_69,U_67))
| U_71 = overflow
| U_71 = tapOff
| U_71 = tapOn
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_14,plain,
( holdsAt(waterLevel(sK10(U_71,U_69,U_67)),U_67)
| U_69 = spilling
| U_71 = tapOff
| U_71 = tapOn
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_15,plain,
( U_69 = waterLevel(sK10(U_71,U_69,U_67))
| U_69 = spilling
| U_71 = tapOff
| U_71 = tapOn
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_16,plain,
( holdsAt(waterLevel(sK10(U_71,U_69,U_67)),U_67)
| U_71 = overflow
| holdsAt(waterLevel(sK9(U_71,U_69,U_67)),U_67)
| U_71 = tapOn
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_17,plain,
( U_69 = waterLevel(sK10(U_71,U_69,U_67))
| U_71 = overflow
| holdsAt(waterLevel(sK9(U_71,U_69,U_67)),U_67)
| U_71 = tapOn
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_18,plain,
( holdsAt(waterLevel(sK10(U_71,U_69,U_67)),U_67)
| U_71 = overflow
| U_69 = waterLevel(sK9(U_71,U_69,U_67))
| U_71 = tapOn
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_19,plain,
( U_69 = waterLevel(sK10(U_71,U_69,U_67))
| U_71 = overflow
| U_69 = waterLevel(sK9(U_71,U_69,U_67))
| U_71 = tapOn
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_20,plain,
( holdsAt(waterLevel(sK10(U_71,U_69,U_67)),U_67)
| U_69 = spilling
| holdsAt(waterLevel(sK9(U_71,U_69,U_67)),U_67)
| U_71 = tapOn
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_21,plain,
( U_69 = waterLevel(sK10(U_71,U_69,U_67))
| U_69 = spilling
| holdsAt(waterLevel(sK9(U_71,U_69,U_67)),U_67)
| U_71 = tapOn
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_22,plain,
( holdsAt(waterLevel(sK10(U_71,U_69,U_67)),U_67)
| U_69 = spilling
| U_69 = waterLevel(sK9(U_71,U_69,U_67))
| U_71 = tapOn
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_23,plain,
( U_69 = waterLevel(sK10(U_71,U_69,U_67))
| U_69 = spilling
| U_69 = waterLevel(sK9(U_71,U_69,U_67))
| U_71 = tapOn
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_24,plain,
( U_71 = overflow
| U_71 = overflow
| U_71 = tapOff
| U_69 = filling
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_25,plain,
( U_69 = spilling
| U_71 = overflow
| U_71 = tapOff
| U_69 = filling
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_26,plain,
( holdsAt(waterLevel(sK9(U_71,U_69,U_67)),U_67)
| U_69 = filling
| U_71 = overflow
| U_71 = overflow
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_27,plain,
( U_69 = waterLevel(sK9(U_71,U_69,U_67))
| U_69 = filling
| U_71 = overflow
| U_71 = overflow
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_28,plain,
( holdsAt(waterLevel(sK9(U_71,U_69,U_67)),U_67)
| U_69 = filling
| U_69 = spilling
| U_71 = overflow
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_29,plain,
( U_69 = waterLevel(sK9(U_71,U_69,U_67))
| U_69 = filling
| U_69 = spilling
| U_71 = overflow
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_30,plain,
( holdsAt(waterLevel(sK10(U_71,U_69,U_67)),U_67)
| U_71 = overflow
| U_71 = tapOff
| U_69 = filling
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_31,plain,
( U_69 = waterLevel(sK10(U_71,U_69,U_67))
| U_71 = overflow
| U_71 = tapOff
| U_69 = filling
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_32,plain,
( holdsAt(waterLevel(sK10(U_71,U_69,U_67)),U_67)
| U_69 = spilling
| U_71 = tapOff
| U_69 = filling
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_33,plain,
( U_69 = waterLevel(sK10(U_71,U_69,U_67))
| U_69 = spilling
| U_71 = tapOff
| U_69 = filling
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_34,plain,
( holdsAt(waterLevel(sK10(U_71,U_69,U_67)),U_67)
| U_71 = overflow
| holdsAt(waterLevel(sK9(U_71,U_69,U_67)),U_67)
| U_69 = filling
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_35,plain,
( U_69 = waterLevel(sK10(U_71,U_69,U_67))
| U_71 = overflow
| holdsAt(waterLevel(sK9(U_71,U_69,U_67)),U_67)
| U_69 = filling
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_36,plain,
( holdsAt(waterLevel(sK10(U_71,U_69,U_67)),U_67)
| U_71 = overflow
| U_69 = waterLevel(sK9(U_71,U_69,U_67))
| U_69 = filling
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_37,plain,
( U_69 = waterLevel(sK10(U_71,U_69,U_67))
| U_71 = overflow
| U_69 = waterLevel(sK9(U_71,U_69,U_67))
| U_69 = filling
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_38,plain,
( holdsAt(waterLevel(sK10(U_71,U_69,U_67)),U_67)
| U_69 = spilling
| holdsAt(waterLevel(sK9(U_71,U_69,U_67)),U_67)
| U_69 = filling
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_39,plain,
( U_69 = waterLevel(sK10(U_71,U_69,U_67))
| U_69 = spilling
| holdsAt(waterLevel(sK9(U_71,U_69,U_67)),U_67)
| U_69 = filling
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_40,plain,
( holdsAt(waterLevel(sK10(U_71,U_69,U_67)),U_67)
| U_69 = spilling
| U_69 = waterLevel(sK9(U_71,U_69,U_67))
| U_69 = filling
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_41,plain,
( U_69 = waterLevel(sK10(U_71,U_69,U_67))
| U_69 = spilling
| U_69 = waterLevel(sK9(U_71,U_69,U_67))
| U_69 = filling
| ~ initiates(U_71,U_69,U_67) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_42,plain,
( U_70 != filling
| U_72 != tapOn
| initiates(U_72,U_70,U_68) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_43,plain,
( U_70 != spilling
| U_72 != overflow
| initiates(U_72,U_70,U_68) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_44,plain,
( U_70 != waterLevel(U_62)
| ~ holdsAt(waterLevel(U_62),U_68)
| U_72 != tapOff
| initiates(U_72,U_70,U_68) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_45,plain,
( U_70 != waterLevel(U_63)
| ~ holdsAt(waterLevel(U_63),U_68)
| U_72 != overflow
| initiates(U_72,U_70,U_68) ),
inference(clausify,[status(thm)],[f_13_5]) ).
fof(f_14_1,plain,
! [Event,Fluent,Time] :
( ( terminates(Event,Fluent,Time)
| ( ( Fluent != filling
| Event != overflow )
& ( Fluent != filling
| Event != tapOff ) ) )
& ( ( Fluent = filling
& Event = overflow )
| ( Fluent = filling
& Event = tapOff )
| ~ terminates(Event,Fluent,Time) ) ),
inference(fof_nnf,[status(thm)],[terminates_all_defn]) ).
fof(f_14_2,plain,
! [U_75,U_74,U_73] :
( ( terminates(U_75,U_74,U_73)
| ( ( U_74 != filling
| U_75 != overflow )
& ( U_74 != filling
| U_75 != tapOff ) ) )
& ( ( U_74 = filling
& U_75 = overflow )
| ( U_74 = filling
& U_75 = tapOff )
| ~ terminates(U_75,U_74,U_73) ) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
fof(f_14_3,plain,
( ! [U_81,U_79] :
( ! [U_77] : terminates(U_81,U_79,U_77)
| ( ( U_79 != filling
| U_81 != overflow )
& ( U_79 != filling
| U_81 != tapOff ) ) )
& ! [U_80,U_78] :
( ! [U_76] : ~ terminates(U_80,U_78,U_76)
| ( U_78 = filling
& U_80 = overflow )
| ( U_78 = filling
& U_80 = tapOff ) ) ),
inference(miniscope,[status(thm)],[f_14_2]) ).
cnf(f_14_4,plain,
( U_80 = overflow
| U_80 = tapOff
| ~ terminates(U_80,U_78,U_76) ),
inference(clausify,[status(thm)],[f_14_3]) ).
cnf(f_14_5,plain,
( U_78 = filling
| U_80 = tapOff
| ~ terminates(U_80,U_78,U_76) ),
inference(clausify,[status(thm)],[f_14_3]) ).
cnf(f_14_6,plain,
( U_80 = overflow
| U_78 = filling
| ~ terminates(U_80,U_78,U_76) ),
inference(clausify,[status(thm)],[f_14_3]) ).
cnf(f_14_7,plain,
( U_78 = filling
| U_78 = filling
| ~ terminates(U_80,U_78,U_76) ),
inference(clausify,[status(thm)],[f_14_3]) ).
cnf(f_14_8,plain,
( U_79 != filling
| U_81 != tapOff
| terminates(U_81,U_79,U_77) ),
inference(clausify,[status(thm)],[f_14_3]) ).
cnf(f_14_9,plain,
( U_79 != filling
| U_81 != overflow
| terminates(U_81,U_79,U_77) ),
inference(clausify,[status(thm)],[f_14_3]) ).
fof(f_15_1,plain,
! [Event,Fluent,Time] :
( ( releases(Event,Fluent,Time)
| ! [Height] :
( Fluent != waterLevel(Height)
| Event != tapOn ) )
& ( ? [Height] :
( Fluent = waterLevel(Height)
& Event = tapOn )
| ~ releases(Event,Fluent,Time) ) ),
inference(fof_nnf,[status(thm)],[releases_all_defn]) ).
fof(f_15_2,plain,
! [U_86,U_85,U_84] :
( ( releases(U_86,U_85,U_84)
| ! [U_83] :
( U_85 != waterLevel(U_83)
| U_86 != tapOn ) )
& ( ? [U_82] :
( U_85 = waterLevel(U_82)
& U_86 = tapOn )
| ~ releases(U_86,U_85,U_84) ) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
fof(f_15_3,plain,
( ! [U_92,U_90] :
( ! [U_88] : releases(U_92,U_90,U_88)
| ! [U_83] : U_90 != waterLevel(U_83)
| U_92 != tapOn )
& ! [U_91,U_89] :
( ! [U_87] : ~ releases(U_91,U_89,U_87)
| ( ? [U_82] : U_89 = waterLevel(U_82)
& U_91 = tapOn ) ) ),
inference(miniscope,[status(thm)],[f_15_2]) ).
fof(f_15_4,plain,
( ! [U_92,U_90] :
( ! [U_88] : releases(U_92,U_90,U_88)
| ! [U_83] : U_90 != waterLevel(U_83)
| U_92 != tapOn )
& ! [U_91,U_89] :
( ! [U_87] : ~ releases(U_91,U_89,U_87)
| ( U_89 = waterLevel(sK11(U_91,U_89))
& U_91 = tapOn ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_82,sK11(U_91,U_89))],[f_15_3]) ).
cnf(f_15_5,plain,
( U_91 = tapOn
| ~ releases(U_91,U_89,U_87) ),
inference(clausify,[status(thm)],[f_15_4]) ).
cnf(f_15_6,plain,
( U_89 = waterLevel(sK11(U_91,U_89))
| ~ releases(U_91,U_89,U_87) ),
inference(clausify,[status(thm)],[f_15_4]) ).
cnf(f_15_7,plain,
( releases(U_92,U_90,U_88)
| U_90 != waterLevel(U_83)
| U_92 != tapOn ),
inference(clausify,[status(thm)],[f_15_4]) ).
fof(f_16_1,plain,
! [Event,Time] :
( ( happens(Event,Time)
| ( ( Event != overflow
| ~ holdsAt(filling,Time)
| ~ holdsAt(waterLevel(n3),Time) )
& ( Time != n0
| Event != tapOn ) ) )
& ( ( Event = overflow
& holdsAt(filling,Time)
& holdsAt(waterLevel(n3),Time) )
| ( Time = n0
& Event = tapOn )
| ~ happens(Event,Time) ) ),
inference(fof_nnf,[status(thm)],[happens_all_defn]) ).
fof(f_16_2,plain,
! [U_94,U_93] :
( ( happens(U_94,U_93)
| ( ( U_94 != overflow
| ~ holdsAt(filling,U_93)
| ~ holdsAt(waterLevel(n3),U_93) )
& ( U_93 != n0
| U_94 != tapOn ) ) )
& ( ( U_94 = overflow
& holdsAt(filling,U_93)
& holdsAt(waterLevel(n3),U_93) )
| ( U_93 = n0
& U_94 = tapOn )
| ~ happens(U_94,U_93) ) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
( ! [U_98,U_96] :
( happens(U_98,U_96)
| ( ( U_98 != overflow
| ~ holdsAt(filling,U_96)
| ~ holdsAt(waterLevel(n3),U_96) )
& ( U_96 != n0
| U_98 != tapOn ) ) )
& ! [U_97,U_95] :
( ( U_97 = overflow
& holdsAt(filling,U_95)
& holdsAt(waterLevel(n3),U_95) )
| ( U_95 = n0
& U_97 = tapOn )
| ~ happens(U_97,U_95) ) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
cnf(f_16_4,plain,
( holdsAt(waterLevel(n3),U_95)
| U_97 = tapOn
| ~ happens(U_97,U_95) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_5,plain,
( holdsAt(filling,U_95)
| U_97 = tapOn
| ~ happens(U_97,U_95) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_6,plain,
( U_97 = overflow
| U_97 = tapOn
| ~ happens(U_97,U_95) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_7,plain,
( holdsAt(waterLevel(n3),U_95)
| U_95 = n0
| ~ happens(U_97,U_95) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_8,plain,
( holdsAt(filling,U_95)
| U_95 = n0
| ~ happens(U_97,U_95) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_9,plain,
( U_97 = overflow
| U_95 = n0
| ~ happens(U_97,U_95) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_10,plain,
( U_96 != n0
| U_98 != tapOn
| happens(U_98,U_96) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_11,plain,
( U_98 != overflow
| ~ holdsAt(filling,U_96)
| ~ holdsAt(waterLevel(n3),U_96)
| happens(U_98,U_96) ),
inference(clausify,[status(thm)],[f_16_3]) ).
fof(f_17_1,plain,
! [Height1,Time,Height2,Offset] :
( trajectory(filling,Time,waterLevel(Height2),Offset)
| Height2 != plus(Height1,Offset)
| ~ holdsAt(waterLevel(Height1),Time) ),
inference(fof_nnf,[status(thm)],[change_of_waterLevel]) ).
fof(f_17_2,plain,
! [U_102,U_101,U_100,U_99] :
( trajectory(filling,U_101,waterLevel(U_100),U_99)
| U_100 != plus(U_102,U_99)
| ~ holdsAt(waterLevel(U_102),U_101) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
cnf(f_17_3,plain,
( trajectory(filling,U_101,waterLevel(U_100),U_99)
| U_100 != plus(U_102,U_99)
| ~ holdsAt(waterLevel(U_102),U_101) ),
inference(clausify,[status(thm)],[f_17_2]) ).
fof(f_18_1,plain,
! [Time,Height1,Height2] :
( Height1 = Height2
| ~ holdsAt(waterLevel(Height2),Time)
| ~ holdsAt(waterLevel(Height1),Time) ),
inference(fof_nnf,[status(thm)],[same_waterLevel]) ).
fof(f_18_2,plain,
! [U_105,U_104,U_103] :
( U_104 = U_103
| ~ holdsAt(waterLevel(U_103),U_105)
| ~ holdsAt(waterLevel(U_104),U_105) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
cnf(f_18_3,plain,
( U_104 = U_103
| ~ holdsAt(waterLevel(U_103),U_105)
| ~ holdsAt(waterLevel(U_104),U_105) ),
inference(clausify,[status(thm)],[f_18_2]) ).
fof(f_19_1,plain,
tapOff != tapOn,
inference(fof_nnf,[status(thm)],[tapOff_not_tapOn]) ).
cnf(f_19_2,plain,
tapOff != tapOn,
inference(clausify,[status(thm)],[f_19_1]) ).
fof(f_20_1,plain,
tapOff != overflow,
inference(fof_nnf,[status(thm)],[tapOff_not_overflow]) ).
cnf(f_20_2,plain,
tapOff != overflow,
inference(clausify,[status(thm)],[f_20_1]) ).
fof(f_21_1,plain,
overflow != tapOn,
inference(fof_nnf,[status(thm)],[overflow_not_tapOn]) ).
cnf(f_21_2,plain,
overflow != tapOn,
inference(clausify,[status(thm)],[f_21_1]) ).
fof(f_22_1,plain,
! [X] : filling != waterLevel(X),
inference(fof_nnf,[status(thm)],[filling_not_waterLevel]) ).
fof(f_22_2,plain,
! [U_106] : filling != waterLevel(U_106),
inference(variable_rename,[status(thm)],[f_22_1]) ).
cnf(f_22_3,plain,
filling != waterLevel(U_106),
inference(clausify,[status(thm)],[f_22_2]) ).
fof(f_23_1,plain,
! [X] : spilling != waterLevel(X),
inference(fof_nnf,[status(thm)],[spilling_not_waterLevel]) ).
fof(f_23_2,plain,
! [U_107] : spilling != waterLevel(U_107),
inference(variable_rename,[status(thm)],[f_23_1]) ).
cnf(f_23_3,plain,
spilling != waterLevel(U_107),
inference(clausify,[status(thm)],[f_23_2]) ).
fof(f_24_1,plain,
filling != spilling,
inference(fof_nnf,[status(thm)],[filling_not_spilling]) ).
cnf(f_24_2,plain,
filling != spilling,
inference(clausify,[status(thm)],[f_24_1]) ).
fof(f_25_1,plain,
! [X,Y] :
( ( waterLevel(X) = waterLevel(Y)
| X != Y )
& ( X = Y
| waterLevel(X) != waterLevel(Y) ) ),
inference(fof_nnf,[status(thm)],[distinct_waterLevels]) ).
fof(f_25_2,plain,
! [U_109,U_108] :
( ( waterLevel(U_109) = waterLevel(U_108)
| U_109 != U_108 )
& ( U_109 = U_108
| waterLevel(U_109) != waterLevel(U_108) ) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
fof(f_25_3,plain,
( ! [U_113,U_111] :
( waterLevel(U_113) = waterLevel(U_111)
| U_113 != U_111 )
& ! [U_112,U_110] :
( U_112 = U_110
| waterLevel(U_112) != waterLevel(U_110) ) ),
inference(miniscope,[status(thm)],[f_25_2]) ).
cnf(f_25_4,plain,
( U_112 = U_110
| waterLevel(U_112) != waterLevel(U_110) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_5,plain,
( waterLevel(U_113) = waterLevel(U_111)
| U_113 != U_111 ),
inference(clausify,[status(thm)],[f_25_3]) ).
fof(f_26_1,plain,
plus(n0,n0) = n0,
inference(fof_nnf,[status(thm)],[plus0_0]) ).
cnf(f_26_2,plain,
plus(n0,n0) = n0,
inference(clausify,[status(thm)],[f_26_1]) ).
fof(f_27_1,plain,
plus(n0,n1) = n1,
inference(fof_nnf,[status(thm)],[plus0_1]) ).
cnf(f_27_2,plain,
plus(n0,n1) = n1,
inference(clausify,[status(thm)],[f_27_1]) ).
fof(f_28_1,plain,
plus(n0,n2) = n2,
inference(fof_nnf,[status(thm)],[plus0_2]) ).
cnf(f_28_2,plain,
plus(n0,n2) = n2,
inference(clausify,[status(thm)],[f_28_1]) ).
fof(f_29_1,plain,
plus(n0,n3) = n3,
inference(fof_nnf,[status(thm)],[plus0_3]) ).
cnf(f_29_2,plain,
plus(n0,n3) = n3,
inference(clausify,[status(thm)],[f_29_1]) ).
fof(f_30_1,plain,
plus(n1,n1) = n2,
inference(fof_nnf,[status(thm)],[plus1_1]) ).
cnf(f_30_2,plain,
plus(n1,n1) = n2,
inference(clausify,[status(thm)],[f_30_1]) ).
fof(f_31_1,plain,
plus(n1,n2) = n3,
inference(fof_nnf,[status(thm)],[plus1_2]) ).
cnf(f_31_2,plain,
plus(n1,n2) = n3,
inference(clausify,[status(thm)],[f_31_1]) ).
fof(f_32_1,plain,
plus(n1,n3) = n4,
inference(fof_nnf,[status(thm)],[plus1_3]) ).
cnf(f_32_2,plain,
plus(n1,n3) = n4,
inference(clausify,[status(thm)],[f_32_1]) ).
fof(f_33_1,plain,
plus(n2,n2) = n4,
inference(fof_nnf,[status(thm)],[plus2_2]) ).
cnf(f_33_2,plain,
plus(n2,n2) = n4,
inference(clausify,[status(thm)],[f_33_1]) ).
fof(f_34_1,plain,
plus(n2,n3) = n5,
inference(fof_nnf,[status(thm)],[plus2_3]) ).
cnf(f_34_2,plain,
plus(n2,n3) = n5,
inference(clausify,[status(thm)],[f_34_1]) ).
fof(f_35_1,plain,
plus(n3,n3) = n6,
inference(fof_nnf,[status(thm)],[plus3_3]) ).
cnf(f_35_2,plain,
plus(n3,n3) = n6,
inference(clausify,[status(thm)],[f_35_1]) ).
fof(f_36_1,plain,
! [X,Y] : plus(X,Y) = plus(Y,X),
inference(fof_nnf,[status(thm)],[symmetry_of_plus]) ).
fof(f_36_2,plain,
! [U_115,U_114] : plus(U_115,U_114) = plus(U_114,U_115),
inference(variable_rename,[status(thm)],[f_36_1]) ).
cnf(f_36_3,plain,
plus(U_115,U_114) = plus(U_114,U_115),
inference(clausify,[status(thm)],[f_36_2]) ).
fof(f_37_1,plain,
! [X,Y] :
( ( less_or_equal(X,Y)
| ( X != Y
& ~ less(X,Y) ) )
& ( X = Y
| less(X,Y)
| ~ less_or_equal(X,Y) ) ),
inference(fof_nnf,[status(thm)],[less_or_equal]) ).
fof(f_37_2,plain,
! [U_117,U_116] :
( ( less_or_equal(U_117,U_116)
| ( U_117 != U_116
& ~ less(U_117,U_116) ) )
& ( U_117 = U_116
| less(U_117,U_116)
| ~ less_or_equal(U_117,U_116) ) ),
inference(variable_rename,[status(thm)],[f_37_1]) ).
fof(f_37_3,plain,
( ! [U_121,U_119] :
( less_or_equal(U_121,U_119)
| ( U_121 != U_119
& ~ less(U_121,U_119) ) )
& ! [U_120,U_118] :
( U_120 = U_118
| less(U_120,U_118)
| ~ less_or_equal(U_120,U_118) ) ),
inference(miniscope,[status(thm)],[f_37_2]) ).
cnf(f_37_4,plain,
( U_120 = U_118
| less(U_120,U_118)
| ~ less_or_equal(U_120,U_118) ),
inference(clausify,[status(thm)],[f_37_3]) ).
cnf(f_37_5,plain,
( ~ less(U_121,U_119)
| less_or_equal(U_121,U_119) ),
inference(clausify,[status(thm)],[f_37_3]) ).
cnf(f_37_6,plain,
( U_121 != U_119
| less_or_equal(U_121,U_119) ),
inference(clausify,[status(thm)],[f_37_3]) ).
fof(f_38_1,plain,
! [X] : ~ less(X,n0),
inference(fof_nnf,[status(thm)],[less0]) ).
fof(f_38_2,plain,
! [U_122] : ~ less(U_122,n0),
inference(variable_rename,[status(thm)],[f_38_1]) ).
cnf(f_38_3,plain,
~ less(U_122,n0),
inference(clausify,[status(thm)],[f_38_2]) ).
fof(f_39_1,plain,
! [X] :
( ( less(X,n1)
| ~ less_or_equal(X,n0) )
& ( less_or_equal(X,n0)
| ~ less(X,n1) ) ),
inference(fof_nnf,[status(thm)],[less1]) ).
fof(f_39_2,plain,
! [U_123] :
( ( less(U_123,n1)
| ~ less_or_equal(U_123,n0) )
& ( less_or_equal(U_123,n0)
| ~ less(U_123,n1) ) ),
inference(variable_rename,[status(thm)],[f_39_1]) ).
fof(f_39_3,plain,
( ! [U_125] :
( less(U_125,n1)
| ~ less_or_equal(U_125,n0) )
& ! [U_124] :
( less_or_equal(U_124,n0)
| ~ less(U_124,n1) ) ),
inference(miniscope,[status(thm)],[f_39_2]) ).
cnf(f_39_4,plain,
( less_or_equal(U_124,n0)
| ~ less(U_124,n1) ),
inference(clausify,[status(thm)],[f_39_3]) ).
cnf(f_39_5,plain,
( less(U_125,n1)
| ~ less_or_equal(U_125,n0) ),
inference(clausify,[status(thm)],[f_39_3]) ).
fof(f_40_1,plain,
! [X] :
( ( less(X,n2)
| ~ less_or_equal(X,n1) )
& ( less_or_equal(X,n1)
| ~ less(X,n2) ) ),
inference(fof_nnf,[status(thm)],[less2]) ).
fof(f_40_2,plain,
! [U_126] :
( ( less(U_126,n2)
| ~ less_or_equal(U_126,n1) )
& ( less_or_equal(U_126,n1)
| ~ less(U_126,n2) ) ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
fof(f_40_3,plain,
( ! [U_128] :
( less(U_128,n2)
| ~ less_or_equal(U_128,n1) )
& ! [U_127] :
( less_or_equal(U_127,n1)
| ~ less(U_127,n2) ) ),
inference(miniscope,[status(thm)],[f_40_2]) ).
cnf(f_40_4,plain,
( less_or_equal(U_127,n1)
| ~ less(U_127,n2) ),
inference(clausify,[status(thm)],[f_40_3]) ).
cnf(f_40_5,plain,
( less(U_128,n2)
| ~ less_or_equal(U_128,n1) ),
inference(clausify,[status(thm)],[f_40_3]) ).
fof(f_41_1,plain,
! [X] :
( ( less(X,n3)
| ~ less_or_equal(X,n2) )
& ( less_or_equal(X,n2)
| ~ less(X,n3) ) ),
inference(fof_nnf,[status(thm)],[less3]) ).
fof(f_41_2,plain,
! [U_129] :
( ( less(U_129,n3)
| ~ less_or_equal(U_129,n2) )
& ( less_or_equal(U_129,n2)
| ~ less(U_129,n3) ) ),
inference(variable_rename,[status(thm)],[f_41_1]) ).
fof(f_41_3,plain,
( ! [U_131] :
( less(U_131,n3)
| ~ less_or_equal(U_131,n2) )
& ! [U_130] :
( less_or_equal(U_130,n2)
| ~ less(U_130,n3) ) ),
inference(miniscope,[status(thm)],[f_41_2]) ).
cnf(f_41_4,plain,
( less_or_equal(U_130,n2)
| ~ less(U_130,n3) ),
inference(clausify,[status(thm)],[f_41_3]) ).
cnf(f_41_5,plain,
( less(U_131,n3)
| ~ less_or_equal(U_131,n2) ),
inference(clausify,[status(thm)],[f_41_3]) ).
fof(f_42_1,plain,
! [X] :
( ( less(X,n4)
| ~ less_or_equal(X,n3) )
& ( less_or_equal(X,n3)
| ~ less(X,n4) ) ),
inference(fof_nnf,[status(thm)],[less4]) ).
fof(f_42_2,plain,
! [U_132] :
( ( less(U_132,n4)
| ~ less_or_equal(U_132,n3) )
& ( less_or_equal(U_132,n3)
| ~ less(U_132,n4) ) ),
inference(variable_rename,[status(thm)],[f_42_1]) ).
fof(f_42_3,plain,
( ! [U_134] :
( less(U_134,n4)
| ~ less_or_equal(U_134,n3) )
& ! [U_133] :
( less_or_equal(U_133,n3)
| ~ less(U_133,n4) ) ),
inference(miniscope,[status(thm)],[f_42_2]) ).
cnf(f_42_4,plain,
( less_or_equal(U_133,n3)
| ~ less(U_133,n4) ),
inference(clausify,[status(thm)],[f_42_3]) ).
cnf(f_42_5,plain,
( less(U_134,n4)
| ~ less_or_equal(U_134,n3) ),
inference(clausify,[status(thm)],[f_42_3]) ).
fof(f_43_1,plain,
! [X] :
( ( less(X,n5)
| ~ less_or_equal(X,n4) )
& ( less_or_equal(X,n4)
| ~ less(X,n5) ) ),
inference(fof_nnf,[status(thm)],[less5]) ).
fof(f_43_2,plain,
! [U_135] :
( ( less(U_135,n5)
| ~ less_or_equal(U_135,n4) )
& ( less_or_equal(U_135,n4)
| ~ less(U_135,n5) ) ),
inference(variable_rename,[status(thm)],[f_43_1]) ).
fof(f_43_3,plain,
( ! [U_137] :
( less(U_137,n5)
| ~ less_or_equal(U_137,n4) )
& ! [U_136] :
( less_or_equal(U_136,n4)
| ~ less(U_136,n5) ) ),
inference(miniscope,[status(thm)],[f_43_2]) ).
cnf(f_43_4,plain,
( less_or_equal(U_136,n4)
| ~ less(U_136,n5) ),
inference(clausify,[status(thm)],[f_43_3]) ).
cnf(f_43_5,plain,
( less(U_137,n5)
| ~ less_or_equal(U_137,n4) ),
inference(clausify,[status(thm)],[f_43_3]) ).
fof(f_44_1,plain,
! [X] :
( ( less(X,n6)
| ~ less_or_equal(X,n5) )
& ( less_or_equal(X,n5)
| ~ less(X,n6) ) ),
inference(fof_nnf,[status(thm)],[less6]) ).
fof(f_44_2,plain,
! [U_138] :
( ( less(U_138,n6)
| ~ less_or_equal(U_138,n5) )
& ( less_or_equal(U_138,n5)
| ~ less(U_138,n6) ) ),
inference(variable_rename,[status(thm)],[f_44_1]) ).
fof(f_44_3,plain,
( ! [U_140] :
( less(U_140,n6)
| ~ less_or_equal(U_140,n5) )
& ! [U_139] :
( less_or_equal(U_139,n5)
| ~ less(U_139,n6) ) ),
inference(miniscope,[status(thm)],[f_44_2]) ).
cnf(f_44_4,plain,
( less_or_equal(U_139,n5)
| ~ less(U_139,n6) ),
inference(clausify,[status(thm)],[f_44_3]) ).
cnf(f_44_5,plain,
( less(U_140,n6)
| ~ less_or_equal(U_140,n5) ),
inference(clausify,[status(thm)],[f_44_3]) ).
fof(f_45_1,plain,
! [X] :
( ( less(X,n7)
| ~ less_or_equal(X,n6) )
& ( less_or_equal(X,n6)
| ~ less(X,n7) ) ),
inference(fof_nnf,[status(thm)],[less7]) ).
fof(f_45_2,plain,
! [U_141] :
( ( less(U_141,n7)
| ~ less_or_equal(U_141,n6) )
& ( less_or_equal(U_141,n6)
| ~ less(U_141,n7) ) ),
inference(variable_rename,[status(thm)],[f_45_1]) ).
fof(f_45_3,plain,
( ! [U_143] :
( less(U_143,n7)
| ~ less_or_equal(U_143,n6) )
& ! [U_142] :
( less_or_equal(U_142,n6)
| ~ less(U_142,n7) ) ),
inference(miniscope,[status(thm)],[f_45_2]) ).
cnf(f_45_4,plain,
( less_or_equal(U_142,n6)
| ~ less(U_142,n7) ),
inference(clausify,[status(thm)],[f_45_3]) ).
cnf(f_45_5,plain,
( less(U_143,n7)
| ~ less_or_equal(U_143,n6) ),
inference(clausify,[status(thm)],[f_45_3]) ).
fof(f_46_1,plain,
! [X] :
( ( less(X,n8)
| ~ less_or_equal(X,n7) )
& ( less_or_equal(X,n7)
| ~ less(X,n8) ) ),
inference(fof_nnf,[status(thm)],[less8]) ).
fof(f_46_2,plain,
! [U_144] :
( ( less(U_144,n8)
| ~ less_or_equal(U_144,n7) )
& ( less_or_equal(U_144,n7)
| ~ less(U_144,n8) ) ),
inference(variable_rename,[status(thm)],[f_46_1]) ).
fof(f_46_3,plain,
( ! [U_146] :
( less(U_146,n8)
| ~ less_or_equal(U_146,n7) )
& ! [U_145] :
( less_or_equal(U_145,n7)
| ~ less(U_145,n8) ) ),
inference(miniscope,[status(thm)],[f_46_2]) ).
cnf(f_46_4,plain,
( less_or_equal(U_145,n7)
| ~ less(U_145,n8) ),
inference(clausify,[status(thm)],[f_46_3]) ).
cnf(f_46_5,plain,
( less(U_146,n8)
| ~ less_or_equal(U_146,n7) ),
inference(clausify,[status(thm)],[f_46_3]) ).
fof(f_47_1,plain,
! [X] :
( ( less(X,n9)
| ~ less_or_equal(X,n8) )
& ( less_or_equal(X,n8)
| ~ less(X,n9) ) ),
inference(fof_nnf,[status(thm)],[less9]) ).
fof(f_47_2,plain,
! [U_147] :
( ( less(U_147,n9)
| ~ less_or_equal(U_147,n8) )
& ( less_or_equal(U_147,n8)
| ~ less(U_147,n9) ) ),
inference(variable_rename,[status(thm)],[f_47_1]) ).
fof(f_47_3,plain,
( ! [U_149] :
( less(U_149,n9)
| ~ less_or_equal(U_149,n8) )
& ! [U_148] :
( less_or_equal(U_148,n8)
| ~ less(U_148,n9) ) ),
inference(miniscope,[status(thm)],[f_47_2]) ).
cnf(f_47_4,plain,
( less_or_equal(U_148,n8)
| ~ less(U_148,n9) ),
inference(clausify,[status(thm)],[f_47_3]) ).
cnf(f_47_5,plain,
( less(U_149,n9)
| ~ less_or_equal(U_149,n8) ),
inference(clausify,[status(thm)],[f_47_3]) ).
fof(f_48_1,plain,
! [X,Y] :
( ( less(X,Y)
| Y = X
| less(Y,X) )
& ( ( Y != X
& ~ less(Y,X) )
| ~ less(X,Y) ) ),
inference(fof_nnf,[status(thm)],[less_property]) ).
fof(f_48_2,plain,
! [U_151,U_150] :
( ( less(U_151,U_150)
| U_150 = U_151
| less(U_150,U_151) )
& ( ( U_150 != U_151
& ~ less(U_150,U_151) )
| ~ less(U_151,U_150) ) ),
inference(variable_rename,[status(thm)],[f_48_1]) ).
fof(f_48_3,plain,
( ! [U_155,U_153] :
( less(U_155,U_153)
| U_153 = U_155
| less(U_153,U_155) )
& ! [U_154,U_152] :
( ( U_152 != U_154
& ~ less(U_152,U_154) )
| ~ less(U_154,U_152) ) ),
inference(miniscope,[status(thm)],[f_48_2]) ).
cnf(f_48_4,plain,
( ~ less(U_152,U_154)
| ~ less(U_154,U_152) ),
inference(clausify,[status(thm)],[f_48_3]) ).
cnf(f_48_5,plain,
( U_152 != U_154
| ~ less(U_154,U_152) ),
inference(clausify,[status(thm)],[f_48_3]) ).
cnf(f_48_6,plain,
( less(U_155,U_153)
| U_153 = U_155
| less(U_153,U_155) ),
inference(clausify,[status(thm)],[f_48_3]) ).
fof(f_49_1,plain,
holdsAt(waterLevel(n0),n0),
inference(fof_nnf,[status(thm)],[waterLevel_0]) ).
cnf(f_49_2,plain,
holdsAt(waterLevel(n0),n0),
inference(clausify,[status(thm)],[f_49_1]) ).
fof(f_50_1,plain,
~ holdsAt(filling,n0),
inference(fof_nnf,[status(thm)],[not_filling_0]) ).
cnf(f_50_2,plain,
~ holdsAt(filling,n0),
inference(clausify,[status(thm)],[f_50_1]) ).
fof(f_51_1,plain,
~ holdsAt(spilling,n0),
inference(fof_nnf,[status(thm)],[not_spilling_0]) ).
cnf(f_51_2,plain,
~ holdsAt(spilling,n0),
inference(clausify,[status(thm)],[f_51_1]) ).
fof(f_52_1,plain,
! [Height] : ~ releasedAt(waterLevel(Height),n0),
inference(fof_nnf,[status(thm)],[not_released_waterLevel_0]) ).
fof(f_52_2,plain,
! [U_156] : ~ releasedAt(waterLevel(U_156),n0),
inference(variable_rename,[status(thm)],[f_52_1]) ).
cnf(f_52_3,plain,
~ releasedAt(waterLevel(U_156),n0),
inference(clausify,[status(thm)],[f_52_2]) ).
fof(f_53_1,plain,
~ releasedAt(filling,n0),
inference(fof_nnf,[status(thm)],[not_released_filling_0]) ).
cnf(f_53_2,plain,
~ releasedAt(filling,n0),
inference(clausify,[status(thm)],[f_53_1]) ).
fof(f_54_1,plain,
~ releasedAt(spilling,n0),
inference(fof_nnf,[status(thm)],[not_released_spilling_0]) ).
cnf(f_54_2,plain,
~ releasedAt(spilling,n0),
inference(clausify,[status(thm)],[f_54_1]) ).
fof(f_55_1,plain,
holdsAt(waterLevel(n3),n3),
inference(fof_nnf,[status(thm)],[waterLevel_3]) ).
cnf(f_55_2,plain,
holdsAt(waterLevel(n3),n3),
inference(clausify,[status(thm)],[f_55_1]) ).
fof(f_56_1,plain,
holdsAt(filling,n3),
inference(fof_nnf,[status(thm)],[filling_3]) ).
cnf(f_56_2,plain,
holdsAt(filling,n3),
inference(clausify,[status(thm)],[f_56_1]) ).
fof(f_57_1,negated_conjecture,
~ happens(overflow,n3),
inference(negate,[status(cth)],[overflow_3]) ).
fof(f_57_2,negated_conjecture,
~ happens(overflow,n3),
inference(definitional_conversion,[status(esa)],[f_57_1]) ).
cnf(f_57_3,negated_conjecture,
~ happens(overflow,n3),
inference(clausify,[status(thm)],[f_57_2]) ).
cnf(f_13_6_simplified,plain,
( U_71 = overflow
| U_71 = tapOff
| U_71 = tapOn
| ~ initiates(U_71,U_69,U_67) ),
inference(simplify_clause,[status(thm)],[f_13_6]) ).
cnf(f_13_8_simplified,plain,
( holdsAt(waterLevel(sK9(U_71,U_69,U_67)),U_67)
| U_71 = tapOn
| U_71 = overflow
| ~ initiates(U_71,U_69,U_67) ),
inference(simplify_clause,[status(thm)],[f_13_8]) ).
cnf(f_13_9_simplified,plain,
( U_69 = waterLevel(sK9(U_71,U_69,U_67))
| U_71 = tapOn
| U_71 = overflow
| ~ initiates(U_71,U_69,U_67) ),
inference(simplify_clause,[status(thm)],[f_13_9]) ).
cnf(f_13_24_simplified,plain,
( U_71 = overflow
| U_71 = tapOff
| U_69 = filling
| ~ initiates(U_71,U_69,U_67) ),
inference(simplify_clause,[status(thm)],[f_13_24]) ).
cnf(f_13_26_simplified,plain,
( holdsAt(waterLevel(sK9(U_71,U_69,U_67)),U_67)
| U_69 = filling
| U_71 = overflow
| ~ initiates(U_71,U_69,U_67) ),
inference(simplify_clause,[status(thm)],[f_13_26]) ).
cnf(f_13_27_simplified,plain,
( U_69 = waterLevel(sK9(U_71,U_69,U_67))
| U_69 = filling
| U_71 = overflow
| ~ initiates(U_71,U_69,U_67) ),
inference(simplify_clause,[status(thm)],[f_13_27]) ).
cnf(f_14_7_simplified,plain,
( U_78 = filling
| ~ terminates(U_80,U_78,U_76) ),
inference(simplify_clause,[status(thm)],[f_14_7]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( plus(Eq_x_0,Eq_x_1) = plus(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( waterLevel(Eq_x_0) = waterLevel(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( sK1(Eq_x_0,Eq_x_1,Eq_x_2) = sK1(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( sK2(Eq_x_0,Eq_x_1,Eq_x_2) = sK2(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( sK3(Eq_x_0,Eq_x_1,Eq_x_2) = sK3(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( sK4(Eq_x_0,Eq_x_1,Eq_x_2) = sK4(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( sK5(Eq_x_0,Eq_x_1) = sK5(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( sK6(Eq_x_0,Eq_x_1) = sK6(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( sK7(Eq_x_0,Eq_x_1) = sK7(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( sK8(Eq_x_0,Eq_x_1) = sK8(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( sK9(Eq_x_0,Eq_x_1,Eq_x_2) = sK9(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_15,axiom,
( sK10(Eq_x_0,Eq_x_1,Eq_x_2) = sK10(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,axiom,
( sK11(Eq_x_0,Eq_x_1) = sK11(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_17,axiom,
( stoppedIn(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ stoppedIn(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_18,axiom,
( happens(Eq_y_0,Eq_y_1)
| ~ happens(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_19,axiom,
( less(Eq_y_0,Eq_y_1)
| ~ less(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_20,axiom,
( terminates(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ terminates(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_21,axiom,
( startedIn(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ startedIn(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_22,axiom,
( initiates(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ initiates(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_23,axiom,
( trajectory(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ trajectory(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_24,axiom,
( holdsAt(Eq_y_0,Eq_y_1)
| ~ holdsAt(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_25,axiom,
( antitrajectory(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ antitrajectory(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_26,axiom,
( releasedAt(Eq_y_0,Eq_y_1)
| ~ releasedAt(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_27,axiom,
( releases(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ releases(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_28,axiom,
( less_or_equal(Eq_y_0,Eq_y_1)
| ~ less_or_equal(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR004+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 15:38:06 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.38/0.65 % SZS status Theorem for theBenchmark
% 0.38/0.65 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------