%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : CSR308_1 : TPTP v9.0.0. Released v9.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n023.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 : Tue Apr 1 01:53:41 AM UTC 2025 % Result : Theorem 18.98s 3.22s % Output : Proof 21.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : CSR308_1 : TPTP v9.0.0. Released v9.1.0. % 0.07/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.35 % Computer : n023.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Mon Mar 31 16:20:24 EDT 2025 % 0.13/0.35 % CPUTime : % 0.63/0.62 ________ _____ % 0.63/0.62 ___ __ \_________(_)________________________________ % 0.63/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.63/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.63/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.63/0.62 % 0.63/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.63/0.62 (2023-06-19) % 0.63/0.62 % 0.63/0.62 (c) Philipp Rümmer, 2009-2023 % 0.63/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.63/0.62 Amanda Stjerna. % 0.63/0.62 Free software under BSD-3-Clause. % 0.63/0.62 % 0.63/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.63/0.62 % 0.63/0.62 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.63/0.63 Running up to 7 provers in parallel. % 0.69/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.69/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.69/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.69/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.69/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.69/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.69/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.83/1.28 Prover 1: Preprocessing ... % 3.83/1.29 Prover 4: Preprocessing ... % 4.41/1.32 Prover 5: Preprocessing ... % 4.41/1.32 Prover 2: Preprocessing ... % 4.41/1.32 Prover 6: Preprocessing ... % 4.41/1.32 Prover 3: Preprocessing ... % 4.41/1.32 Prover 0: Preprocessing ... % 8.31/1.90 Prover 6: Proving ... % 8.90/1.91 Prover 3: Constructing countermodel ... % 8.90/1.91 Prover 1: Constructing countermodel ... % 8.90/1.95 Prover 5: Proving ... % 9.46/1.98 Prover 4: Constructing countermodel ... % 9.46/2.02 Prover 2: Proving ... % 9.46/2.05 Prover 0: Proving ... % 18.98/3.22 Prover 5: proved (2577ms) % 18.98/3.22 % 18.98/3.22 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 18.98/3.22 % 18.98/3.22 Prover 3: stopped % 18.98/3.23 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 18.98/3.23 Prover 6: stopped % 18.98/3.24 Prover 2: stopped % 18.98/3.24 Prover 0: stopped % 18.98/3.25 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 18.98/3.25 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 18.98/3.25 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 18.98/3.25 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 18.98/3.26 Prover 7: Preprocessing ... % 19.64/3.30 Prover 11: Preprocessing ... % 19.83/3.31 Prover 8: Preprocessing ... % 19.83/3.31 Prover 10: Preprocessing ... % 19.83/3.31 Prover 13: Preprocessing ... % 19.94/3.37 Prover 4: Found proof (size 274) % 19.94/3.38 Prover 4: proved (2731ms) % 19.94/3.39 Prover 13: stopped % 19.94/3.39 Prover 7: Warning: ignoring some quantifiers % 19.94/3.40 Prover 1: stopped % 19.94/3.40 Prover 10: Warning: ignoring some quantifiers % 19.94/3.40 Prover 7: Constructing countermodel ... % 19.94/3.40 Prover 10: Constructing countermodel ... % 19.94/3.41 Prover 7: stopped % 19.94/3.41 Prover 10: stopped % 19.94/3.42 Prover 8: Warning: ignoring some quantifiers % 19.94/3.42 Prover 8: Constructing countermodel ... % 20.69/3.43 Prover 8: stopped % 20.69/3.46 Prover 11: Constructing countermodel ... % 20.69/3.46 Prover 11: stopped % 20.69/3.46 % 20.69/3.46 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 20.69/3.46 % 20.69/3.48 % SZS output start Proof for theBenchmark % 20.69/3.48 Assumptions after simplification: % 20.69/3.48 --------------------------------- % 20.69/3.48 % 20.69/3.48 (filling_not_spilling) % 20.69/3.49 ~ (filling = spilling) & fluent(filling) & fluent(spilling) % 20.69/3.49 % 20.69/3.49 (filling_not_waterLevel) % 21.05/3.50 fluent(filling) & ! [v0: int] : ~ (waterLevel(v0) = filling) % 21.05/3.50 % 21.05/3.50 (filling_times) % 21.05/3.50 fluent(filling) & ? [v0: int] : ? [v1: time] : ? [v2: time] : ? [v3: int] % 21.05/3.50 : ? [v4: int] : ( ~ (v4 = 0) & ~ (v3 = 0) & ~ (v0 = 0) & % 21.05/3.50 releasedAt(filling, v2) = v3 & holdsAt(filling, v2) = v4 & holdsAt(filling, % 21.05/3.50 v1) = 0 & at_time($sum(v0, 1)) = v1 & at_time(v0) = v2 & time(v2) & % 21.05/3.50 time(v1)) % 21.05/3.50 % 21.05/3.50 (happens_all_defn) % 21.05/3.50 event(overflow) & event(tapOn) & fluent(filling) & ? [v0: fluent] : % 21.05/3.50 (waterLevel(3) = v0 & fluent(v0) & ! [v1: int] : ! [v2: time] : ! [v3: int] % 21.05/3.50 : (v3 = 0 | ~ (at_time(v1) = v2) | ~ (happens(overflow, v2) = v3) | ? % 21.05/3.50 [v4: any] : ? [v5: any] : (holdsAt(v0, v2) = v4 & holdsAt(filling, v2) = % 21.05/3.50 v5 & ( ~ (v5 = 0) | ~ (v4 = 0)))) & ! [v1: event] : ! [v2: int] : ! % 21.05/3.50 [v3: time] : (v2 = 0 | v1 = overflow | ~ (at_time(v2) = v3) | ~ % 21.05/3.50 (happens(v1, v3) = 0) | ~ event(v1)) & ! [v1: event] : ! [v2: int] : ! % 21.05/3.51 [v3: time] : (v2 = 0 | ~ (at_time(v2) = v3) | ~ (happens(v1, v3) = 0) | ~ % 21.05/3.51 event(v1) | (holdsAt(v0, v3) = 0 & holdsAt(filling, v3) = 0)) & ! [v1: % 21.05/3.51 event] : ! [v2: int] : ! [v3: time] : (v1 = overflow | v1 = tapOn | ~ % 21.05/3.51 (at_time(v2) = v3) | ~ (happens(v1, v3) = 0) | ~ event(v1)) & ! [v1: % 21.05/3.51 event] : ! [v2: int] : ! [v3: time] : (v1 = tapOn | ~ (at_time(v2) = % 21.05/3.51 v3) | ~ (happens(v1, v3) = 0) | ~ event(v1) | (holdsAt(v0, v3) = 0 & % 21.05/3.51 holdsAt(filling, v3) = 0)) & ! [v1: time] : ! [v2: int] : (v2 = 0 | ~ % 21.05/3.51 (at_time(0) = v1) | ~ (happens(tapOn, v1) = v2))) % 21.05/3.51 % 21.05/3.51 (initiates_all_defn) % 21.05/3.51 event(overflow) & event(tapOff) & event(tapOn) & fluent(filling) & % 21.05/3.51 fluent(spilling) & ! [v0: fluent] : ! [v1: int] : ! [v2: time] : ! [v3: % 21.05/3.51 int] : ! [v4: int] : (v3 = 0 | ~ (waterLevel(v4) = v0) | ~ % 21.05/3.51 (initiates(overflow, v0, v2) = v3) | ~ (at_time(v1) = v2) | ~ fluent(v0) | % 21.05/3.51 ? [v5: int] : ( ~ (v5 = 0) & holdsAt(v0, v2) = v5)) & ! [v0: fluent] : ! % 21.05/3.51 [v1: int] : ! [v2: time] : ! [v3: int] : ! [v4: int] : (v3 = 0 | ~ % 21.05/3.51 (waterLevel(v4) = v0) | ~ (initiates(tapOff, v0, v2) = v3) | ~ % 21.05/3.51 (at_time(v1) = v2) | ~ fluent(v0) | ? [v5: int] : ( ~ (v5 = 0) & % 21.05/3.51 holdsAt(v0, v2) = v5)) & ! [v0: event] : ! [v1: fluent] : ! [v2: int] : % 21.05/3.51 ! [v3: time] : (v1 = filling | v1 = spilling | ~ (initiates(v0, v1, v3) = 0) % 21.05/3.51 | ~ (at_time(v2) = v3) | ~ event(v0) | ~ fluent(v1) | ? [v4: int] : ? % 21.05/3.51 [v5: fluent] : ? [v6: int] : ((v6 = 0 & v5 = v1 & v0 = overflow & % 21.05/3.51 waterLevel(v4) = v1 & holdsAt(v1, v3) = 0) | (v6 = 0 & v5 = v1 & v0 = % 21.05/3.51 tapOff & waterLevel(v4) = v1 & holdsAt(v1, v3) = 0))) & ! [v0: event] : % 21.05/3.51 ! [v1: fluent] : ! [v2: int] : ! [v3: time] : (v1 = filling | v0 = overflow % 21.05/3.51 | ~ (initiates(v0, v1, v3) = 0) | ~ (at_time(v2) = v3) | ~ event(v0) | ~ % 21.05/3.51 fluent(v1) | ? [v4: int] : (v0 = tapOff & waterLevel(v4) = v1 & holdsAt(v1, % 21.05/3.51 v3) = 0)) & ! [v0: event] : ! [v1: fluent] : ! [v2: int] : ! [v3: % 21.05/3.51 time] : (v1 = spilling | v0 = tapOn | ~ (initiates(v0, v1, v3) = 0) | ~ % 21.05/3.51 (at_time(v2) = v3) | ~ event(v0) | ~ fluent(v1) | ? [v4: int] : ? [v5: % 21.05/3.51 fluent] : ? [v6: int] : ((v6 = 0 & v5 = v1 & v0 = overflow & % 21.05/3.51 waterLevel(v4) = v1 & holdsAt(v1, v3) = 0) | (v6 = 0 & v5 = v1 & v0 = % 21.05/3.51 tapOff & waterLevel(v4) = v1 & holdsAt(v1, v3) = 0))) & ! [v0: event] : % 21.05/3.51 ! [v1: fluent] : ! [v2: int] : ! [v3: time] : (v0 = overflow | v0 = tapOn | % 21.05/3.51 ~ (initiates(v0, v1, v3) = 0) | ~ (at_time(v2) = v3) | ~ event(v0) | ~ % 21.05/3.51 fluent(v1) | ? [v4: int] : (v0 = tapOff & waterLevel(v4) = v1 & holdsAt(v1, % 21.05/3.51 v3) = 0)) & ! [v0: int] : ! [v1: time] : ! [v2: int] : (v2 = 0 | ~ % 21.05/3.51 (initiates(overflow, spilling, v1) = v2) | ~ (at_time(v0) = v1)) & ! [v0: % 21.05/3.51 int] : ! [v1: time] : ! [v2: int] : (v2 = 0 | ~ (initiates(tapOn, % 21.05/3.51 filling, v1) = v2) | ~ (at_time(v0) = v1)) % 21.05/3.51 % 21.05/3.51 (keep_holding) % 21.05/3.51 ! [v0: fluent] : ! [v1: int] : ! [v2: time] : ! [v3: int] : (v3 = 0 | ~ % 21.05/3.52 (releasedAt(v0, v2) = v3) | ~ (at_time($sum(v1, 1)) = v2) | ~ fluent(v0) | % 21.05/3.52 ? [v4: time] : ? [v5: any] : ? [v6: any] : ? [v7: event] : ? [v8: int] % 21.05/3.52 : ? [v9: int] : (holdsAt(v0, v4) = v5 & holdsAt(v0, v2) = v6 & at_time(v1) % 21.05/3.52 = v4 & event(v7) & time(v4) & ( ~ (v5 = 0) | v6 = 0 | (v9 = 0 & v8 = 0 & % 21.05/3.52 happens(v7, v4) = 0 & terminates(v7, v0, v4) = 0)))) & ! [v0: fluent] % 21.05/3.52 : ! [v1: int] : ! [v2: time] : ! [v3: int] : (v3 = 0 | ~ (holdsAt(v0, v2) % 21.05/3.52 = v3) | ~ (at_time($sum(v1, 1)) = v2) | ~ fluent(v0) | ? [v4: time] : % 21.05/3.52 ? [v5: any] : ? [v6: any] : ? [v7: event] : ? [v8: int] : ? [v9: int] : % 21.05/3.52 (releasedAt(v0, v2) = v6 & holdsAt(v0, v4) = v5 & at_time(v1) = v4 & % 21.05/3.52 event(v7) & time(v4) & ( ~ (v5 = 0) | v6 = 0 | (v9 = 0 & v8 = 0 & % 21.05/3.52 happens(v7, v4) = 0 & terminates(v7, v0, v4) = 0)))) & ! [v0: fluent] % 21.05/3.52 : ! [v1: int] : ! [v2: time] : ( ~ (holdsAt(v0, v2) = 0) | ~ (at_time(v1) = % 21.05/3.52 v2) | ~ fluent(v0) | ? [v3: time] : ? [v4: any] : ? [v5: any] : ? % 21.05/3.52 [v6: event] : ? [v7: int] : ? [v8: int] : (event(v6) & ((v8 = 0 & v7 = 0 & % 21.05/3.52 happens(v6, v2) = 0 & terminates(v6, v0, v2) = 0) | (releasedAt(v0, % 21.05/3.52 v3) = v4 & holdsAt(v0, v3) = v5 & at_time($sum(v1, 1)) = v3 & % 21.05/3.52 time(v3) & (v5 = 0 | v4 = 0))))) % 21.05/3.52 % 21.05/3.52 (keep_not_holding) % 21.05/3.52 ! [v0: fluent] : ! [v1: int] : ! [v2: time] : ! [v3: int] : (v3 = 0 | ~ % 21.05/3.52 (releasedAt(v0, v2) = v3) | ~ (at_time($sum(v1, 1)) = v2) | ~ fluent(v0) | % 21.05/3.52 ? [v4: time] : ? [v5: any] : ? [v6: any] : ? [v7: event] : ? [v8: int] % 21.05/3.52 : ? [v9: int] : (holdsAt(v0, v4) = v5 & holdsAt(v0, v2) = v6 & at_time(v1) % 21.05/3.52 = v4 & event(v7) & time(v4) & ( ~ (v6 = 0) | v5 = 0 | (v9 = 0 & v8 = 0 & % 21.05/3.52 initiates(v7, v0, v4) = 0 & happens(v7, v4) = 0)))) & ! [v0: fluent] % 21.05/3.52 : ! [v1: int] : ! [v2: time] : ! [v3: int] : (v3 = 0 | ~ (holdsAt(v0, v2) % 21.05/3.52 = v3) | ~ (at_time(v1) = v2) | ~ fluent(v0) | ? [v4: time] : ? [v5: % 21.05/3.52 any] : ? [v6: any] : ? [v7: event] : ? [v8: int] : ? [v9: int] : % 21.05/3.52 (event(v7) & ((v9 = 0 & v8 = 0 & initiates(v7, v0, v2) = 0 & happens(v7, v2) % 21.05/3.52 = 0) | (releasedAt(v0, v4) = v5 & holdsAt(v0, v4) = v6 & % 21.05/3.52 at_time($sum(v1, 1)) = v4 & time(v4) & ( ~ (v6 = 0) | v5 = 0))))) & ! % 21.05/3.52 [v0: fluent] : ! [v1: int] : ! [v2: time] : ( ~ (holdsAt(v0, v2) = 0) | ~ % 21.05/3.52 (at_time($sum(v1, 1)) = v2) | ~ fluent(v0) | ? [v3: time] : ? [v4: any] : % 21.05/3.52 ? [v5: any] : ? [v6: event] : ? [v7: int] : ? [v8: int] : % 21.05/3.52 (releasedAt(v0, v2) = v5 & holdsAt(v0, v3) = v4 & at_time(v1) = v3 & % 21.05/3.52 event(v6) & time(v3) & (v5 = 0 | v4 = 0 | (v8 = 0 & v7 = 0 & initiates(v6, % 21.05/3.52 v0, v3) = 0 & happens(v6, v3) = 0)))) % 21.05/3.52 % 21.05/3.52 (keep_not_released) % 21.05/3.52 ! [v0: fluent] : ! [v1: int] : ! [v2: time] : ! [v3: int] : (v3 = 0 | ~ % 21.05/3.52 (releasedAt(v0, v2) = v3) | ~ (at_time(v1) = v2) | ~ fluent(v0) | ? [v4: % 21.05/3.52 time] : ? [v5: int] : ? [v6: event] : ? [v7: int] : ? [v8: int] : % 21.05/3.52 (event(v6) & ((v8 = 0 & v7 = 0 & releases(v6, v0, v2) = 0 & happens(v6, v2) % 21.05/3.52 = 0) | ( ~ (v5 = 0) & releasedAt(v0, v4) = v5 & at_time($sum(v1, 1)) = % 21.05/3.52 v4 & time(v4))))) & ! [v0: fluent] : ! [v1: int] : ! [v2: time] : ( % 21.05/3.52 ~ (releasedAt(v0, v2) = 0) | ~ (at_time($sum(v1, 1)) = v2) | ~ fluent(v0) % 21.05/3.52 | ? [v3: time] : ? [v4: any] : ? [v5: event] : ? [v6: int] : ? [v7: % 21.05/3.52 int] : (releasedAt(v0, v3) = v4 & at_time(v1) = v3 & event(v5) & time(v3) % 21.05/3.52 & (v4 = 0 | (v7 = 0 & v6 = 0 & releases(v5, v0, v3) = 0 & happens(v5, v3) % 21.05/3.52 = 0)))) % 21.05/3.52 % 21.05/3.52 (keep_released) % 21.05/3.52 ! [v0: fluent] : ! [v1: int] : ! [v2: time] : ! [v3: int] : (v3 = 0 | ~ % 21.05/3.52 (releasedAt(v0, v2) = v3) | ~ (at_time($sum(v1, 1)) = v2) | ~ fluent(v0) | % 21.05/3.52 ? [v4: time] : ? [v5: any] : ? [v6: event] : ? [v7: int] : ? [v8: any] % 21.05/3.52 : ? [v9: any] : (releasedAt(v0, v4) = v5 & at_time(v1) = v4 & event(v6) & % 21.05/3.52 time(v4) & ( ~ (v5 = 0) | (v7 = 0 & initiates(v6, v0, v4) = v8 & % 21.05/3.52 happens(v6, v4) = 0 & terminates(v6, v0, v4) = v9 & (v9 = 0 | v8 = % 21.05/3.52 0))))) & ! [v0: fluent] : ! [v1: int] : ! [v2: time] : ( ~ % 21.05/3.52 (releasedAt(v0, v2) = 0) | ~ (at_time(v1) = v2) | ~ fluent(v0) | ? [v3: % 21.05/3.52 time] : ? [v4: int] : ? [v5: event] : ? [v6: int] : ? [v7: any] : ? % 21.05/3.52 [v8: any] : (event(v5) & ((v6 = 0 & initiates(v5, v0, v2) = v7 & happens(v5, % 21.05/3.52 v2) = 0 & terminates(v5, v0, v2) = v8 & (v8 = 0 | v7 = 0)) | (v4 = 0 % 21.05/3.52 & releasedAt(v0, v3) = 0 & at_time($sum(v1, 1)) = v3 & time(v3))))) % 21.05/3.52 % 21.05/3.52 (releases_all_defn) % 21.05/3.52 event(tapOn) & ! [v0: fluent] : ! [v1: int] : ! [v2: time] : ! [v3: int] : % 21.05/3.52 ! [v4: int] : (v3 = 0 | ~ (waterLevel(v4) = v0) | ~ (releases(tapOn, v0, % 21.05/3.52 v2) = v3) | ~ (at_time(v1) = v2) | ~ fluent(v0)) & ! [v0: event] : ! % 21.05/3.52 [v1: fluent] : ! [v2: int] : ! [v3: time] : ( ~ (releases(v0, v1, v3) = 0) | % 21.05/3.52 ~ (at_time(v2) = v3) | ~ event(v0) | ~ fluent(v1) | ? [v4: int] : (v0 = % 21.05/3.52 tapOn & waterLevel(v4) = v1)) % 21.05/3.52 % 21.05/3.52 (tapOn_overflow) % 21.05/3.52 ~ (overflow = tapOn) & event(overflow) & event(tapOn) % 21.05/3.52 % 21.05/3.52 (function-axioms) % 21.05/3.53 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: int] : ! % 21.05/3.53 [v3: fluent] : ! [v4: time] : ! [v5: fluent] : (v1 = v0 | ~ % 21.05/3.53 (antitrajectory(v5, v4, v3, v2) = v1) | ~ (antitrajectory(v5, v4, v3, v2) = % 21.05/3.53 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 21.05/3.53 int] : ! [v3: fluent] : ! [v4: time] : ! [v5: fluent] : (v1 = v0 | ~ % 21.05/3.53 (trajectory(v5, v4, v3, v2) = v1) | ~ (trajectory(v5, v4, v3, v2) = v0)) & % 21.05/3.53 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: time] : ! % 21.05/3.53 [v3: fluent] : ! [v4: event] : (v1 = v0 | ~ (releases(v4, v3, v2) = v1) | ~ % 21.05/3.53 (releases(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 21.05/3.53 MultipleValueBool] : ! [v2: time] : ! [v3: fluent] : ! [v4: time] : (v1 = % 21.05/3.53 v0 | ~ (startedIn(v4, v3, v2) = v1) | ~ (startedIn(v4, v3, v2) = v0)) & ! % 21.05/3.53 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: time] : ! [v3: % 21.05/3.53 fluent] : ! [v4: event] : (v1 = v0 | ~ (initiates(v4, v3, v2) = v1) | ~ % 21.05/3.53 (initiates(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 21.05/3.53 MultipleValueBool] : ! [v2: time] : ! [v3: fluent] : ! [v4: time] : (v1 = % 21.05/3.53 v0 | ~ (stoppedIn(v4, v3, v2) = v1) | ~ (stoppedIn(v4, v3, v2) = v0)) & ! % 21.05/3.53 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: time] : ! [v3: % 21.05/3.53 fluent] : ! [v4: event] : (v1 = v0 | ~ (terminates(v4, v3, v2) = v1) | ~ % 21.05/3.53 (terminates(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 21.05/3.53 MultipleValueBool] : ! [v2: time] : ! [v3: fluent] : (v1 = v0 | ~ % 21.05/3.53 (releasedAt(v3, v2) = v1) | ~ (releasedAt(v3, v2) = v0)) & ! [v0: % 21.05/3.53 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: time] : ! [v3: % 21.05/3.53 fluent] : (v1 = v0 | ~ (holdsAt(v3, v2) = v1) | ~ (holdsAt(v3, v2) = v0)) % 21.05/3.53 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: time] : ! % 21.05/3.53 [v3: event] : (v1 = v0 | ~ (happens(v3, v2) = v1) | ~ (happens(v3, v2) = % 21.05/3.53 v0)) & ! [v0: fluent] : ! [v1: fluent] : ! [v2: int] : (v1 = v0 | ~ % 21.05/3.53 (waterLevel(v2) = v1) | ~ (waterLevel(v2) = v0)) & ! [v0: time] : ! [v1: % 21.05/3.53 time] : ! [v2: int] : (v1 = v0 | ~ (at_time(v2) = v1) | ~ (at_time(v2) = % 21.05/3.53 v0)) % 21.05/3.53 % 21.05/3.53 Further assumptions not needed in the proof: % 21.05/3.53 -------------------------------------------- % 21.05/3.53 antitrajectory, change_holding, change_of_waterLevel, distinct_waterLevels, % 21.05/3.53 happens_holds, happens_not_released, happens_releases, % 21.05/3.53 happens_terminates_not_holds, not_filling_0, not_released_filling_0, % 21.05/3.53 not_released_spilling_0, not_released_waterLevel_0, not_spilling_0, % 21.05/3.53 same_waterLevel, spilling_not_waterLevel, startedin_defn, stoppedin_defn, % 21.05/3.53 tapOff_overflow, tapOn_tapOff, terminates_all_defn, waterLevel_0 % 21.05/3.53 % 21.05/3.53 Those formulas are unsatisfiable: % 21.05/3.53 --------------------------------- % 21.05/3.53 % 21.05/3.53 Begin of proof % 21.05/3.53 | % 21.05/3.53 | ALPHA: (keep_holding) implies: % 21.05/3.53 | (1) ! [v0: fluent] : ! [v1: int] : ! [v2: time] : ! [v3: int] : (v3 = 0 % 21.05/3.53 | | ~ (holdsAt(v0, v2) = v3) | ~ (at_time($sum(v1, 1)) = v2) | ~ % 21.05/3.53 | fluent(v0) | ? [v4: time] : ? [v5: any] : ? [v6: any] : ? [v7: % 21.05/3.53 | event] : ? [v8: int] : ? [v9: int] : (releasedAt(v0, v2) = v6 & % 21.05/3.53 | holdsAt(v0, v4) = v5 & at_time(v1) = v4 & event(v7) & time(v4) & ( % 21.05/3.53 | ~ (v5 = 0) | v6 = 0 | (v9 = 0 & v8 = 0 & happens(v7, v4) = 0 & % 21.05/3.53 | terminates(v7, v0, v4) = 0)))) % 21.05/3.53 | (2) ! [v0: fluent] : ! [v1: int] : ! [v2: time] : ! [v3: int] : (v3 = 0 % 21.05/3.53 | | ~ (releasedAt(v0, v2) = v3) | ~ (at_time($sum(v1, 1)) = v2) | ~ % 21.05/3.53 | fluent(v0) | ? [v4: time] : ? [v5: any] : ? [v6: any] : ? [v7: % 21.05/3.53 | event] : ? [v8: int] : ? [v9: int] : (holdsAt(v0, v4) = v5 & % 21.05/3.53 | holdsAt(v0, v2) = v6 & at_time(v1) = v4 & event(v7) & time(v4) & ( % 21.05/3.53 | ~ (v5 = 0) | v6 = 0 | (v9 = 0 & v8 = 0 & happens(v7, v4) = 0 & % 21.05/3.53 | terminates(v7, v0, v4) = 0)))) % 21.05/3.53 | % 21.05/3.53 | ALPHA: (keep_not_holding) implies: % 21.05/3.53 | (3) ! [v0: fluent] : ! [v1: int] : ! [v2: time] : ( ~ (holdsAt(v0, v2) = % 21.05/3.53 | 0) | ~ (at_time($sum(v1, 1)) = v2) | ~ fluent(v0) | ? [v3: time] % 21.05/3.53 | : ? [v4: any] : ? [v5: any] : ? [v6: event] : ? [v7: int] : ? % 21.05/3.53 | [v8: int] : (releasedAt(v0, v2) = v5 & holdsAt(v0, v3) = v4 & % 21.05/3.53 | at_time(v1) = v3 & event(v6) & time(v3) & (v5 = 0 | v4 = 0 | (v8 = % 21.05/3.53 | 0 & v7 = 0 & initiates(v6, v0, v3) = 0 & happens(v6, v3) = % 21.05/3.53 | 0)))) % 21.05/3.54 | (4) ! [v0: fluent] : ! [v1: int] : ! [v2: time] : ! [v3: int] : (v3 = 0 % 21.05/3.54 | | ~ (holdsAt(v0, v2) = v3) | ~ (at_time(v1) = v2) | ~ fluent(v0) | % 21.05/3.54 | ? [v4: time] : ? [v5: any] : ? [v6: any] : ? [v7: event] : ? % 21.05/3.54 | [v8: int] : ? [v9: int] : (event(v7) & ((v9 = 0 & v8 = 0 & % 21.05/3.54 | initiates(v7, v0, v2) = 0 & happens(v7, v2) = 0) | % 21.05/3.54 | (releasedAt(v0, v4) = v5 & holdsAt(v0, v4) = v6 & % 21.05/3.54 | at_time($sum(v1, 1)) = v4 & time(v4) & ( ~ (v6 = 0) | v5 = % 21.05/3.54 | 0))))) % 21.05/3.54 | (5) ! [v0: fluent] : ! [v1: int] : ! [v2: time] : ! [v3: int] : (v3 = 0 % 21.05/3.54 | | ~ (releasedAt(v0, v2) = v3) | ~ (at_time($sum(v1, 1)) = v2) | ~ % 21.05/3.54 | fluent(v0) | ? [v4: time] : ? [v5: any] : ? [v6: any] : ? [v7: % 21.05/3.54 | event] : ? [v8: int] : ? [v9: int] : (holdsAt(v0, v4) = v5 & % 21.05/3.54 | holdsAt(v0, v2) = v6 & at_time(v1) = v4 & event(v7) & time(v4) & ( % 21.05/3.54 | ~ (v6 = 0) | v5 = 0 | (v9 = 0 & v8 = 0 & initiates(v7, v0, v4) = % 21.05/3.54 | 0 & happens(v7, v4) = 0)))) % 21.05/3.54 | % 21.05/3.54 | ALPHA: (keep_released) implies: % 21.05/3.54 | (6) ! [v0: fluent] : ! [v1: int] : ! [v2: time] : ! [v3: int] : (v3 = 0 % 21.05/3.54 | | ~ (releasedAt(v0, v2) = v3) | ~ (at_time($sum(v1, 1)) = v2) | ~ % 21.05/3.54 | fluent(v0) | ? [v4: time] : ? [v5: any] : ? [v6: event] : ? [v7: % 21.05/3.54 | int] : ? [v8: any] : ? [v9: any] : (releasedAt(v0, v4) = v5 & % 21.05/3.54 | at_time(v1) = v4 & event(v6) & time(v4) & ( ~ (v5 = 0) | (v7 = 0 & % 21.05/3.54 | initiates(v6, v0, v4) = v8 & happens(v6, v4) = 0 & % 21.05/3.54 | terminates(v6, v0, v4) = v9 & (v9 = 0 | v8 = 0))))) % 21.05/3.54 | % 21.05/3.54 | ALPHA: (keep_not_released) implies: % 21.05/3.54 | (7) ! [v0: fluent] : ! [v1: int] : ! [v2: time] : ! [v3: int] : (v3 = 0 % 21.05/3.54 | | ~ (releasedAt(v0, v2) = v3) | ~ (at_time(v1) = v2) | ~ % 21.05/3.54 | fluent(v0) | ? [v4: time] : ? [v5: int] : ? [v6: event] : ? [v7: % 21.05/3.54 | int] : ? [v8: int] : (event(v6) & ((v8 = 0 & v7 = 0 & releases(v6, % 21.05/3.54 | v0, v2) = 0 & happens(v6, v2) = 0) | ( ~ (v5 = 0) & % 21.05/3.54 | releasedAt(v0, v4) = v5 & at_time($sum(v1, 1)) = v4 & % 21.05/3.54 | time(v4))))) % 21.05/3.54 | % 21.05/3.54 | ALPHA: (tapOn_overflow) implies: % 21.05/3.54 | (8) ~ (overflow = tapOn) % 21.05/3.54 | % 21.05/3.54 | ALPHA: (filling_not_waterLevel) implies: % 21.05/3.54 | (9) ! [v0: int] : ~ (waterLevel(v0) = filling) % 21.05/3.54 | % 21.05/3.54 | ALPHA: (filling_not_spilling) implies: % 21.05/3.54 | (10) ~ (filling = spilling) % 21.05/3.54 | % 21.05/3.54 | ALPHA: (initiates_all_defn) implies: % 21.05/3.54 | (11) ! [v0: event] : ! [v1: fluent] : ! [v2: int] : ! [v3: time] : (v1 % 21.05/3.54 | = spilling | v0 = tapOn | ~ (initiates(v0, v1, v3) = 0) | ~ % 21.05/3.54 | (at_time(v2) = v3) | ~ event(v0) | ~ fluent(v1) | ? [v4: int] : % 21.05/3.54 | ? [v5: fluent] : ? [v6: int] : ((v6 = 0 & v5 = v1 & v0 = overflow & % 21.05/3.54 | waterLevel(v4) = v1 & holdsAt(v1, v3) = 0) | (v6 = 0 & v5 = v1 & % 21.05/3.54 | v0 = tapOff & waterLevel(v4) = v1 & holdsAt(v1, v3) = 0))) % 21.05/3.54 | % 21.05/3.54 | ALPHA: (releases_all_defn) implies: % 21.05/3.54 | (12) ! [v0: event] : ! [v1: fluent] : ! [v2: int] : ! [v3: time] : ( ~ % 21.05/3.54 | (releases(v0, v1, v3) = 0) | ~ (at_time(v2) = v3) | ~ event(v0) | % 21.05/3.54 | ~ fluent(v1) | ? [v4: int] : (v0 = tapOn & waterLevel(v4) = v1)) % 21.05/3.54 | % 21.05/3.54 | ALPHA: (happens_all_defn) implies: % 21.05/3.54 | (13) ? [v0: fluent] : (waterLevel(3) = v0 & fluent(v0) & ! [v1: int] : ! % 21.05/3.54 | [v2: time] : ! [v3: int] : (v3 = 0 | ~ (at_time(v1) = v2) | ~ % 21.05/3.54 | (happens(overflow, v2) = v3) | ? [v4: any] : ? [v5: any] : % 21.05/3.54 | (holdsAt(v0, v2) = v4 & holdsAt(filling, v2) = v5 & ( ~ (v5 = 0) | % 21.05/3.54 | ~ (v4 = 0)))) & ! [v1: event] : ! [v2: int] : ! [v3: time] % 21.05/3.54 | : (v2 = 0 | v1 = overflow | ~ (at_time(v2) = v3) | ~ (happens(v1, % 21.05/3.54 | v3) = 0) | ~ event(v1)) & ! [v1: event] : ! [v2: int] : ! % 21.05/3.54 | [v3: time] : (v2 = 0 | ~ (at_time(v2) = v3) | ~ (happens(v1, v3) = % 21.05/3.54 | 0) | ~ event(v1) | (holdsAt(v0, v3) = 0 & holdsAt(filling, v3) % 21.05/3.54 | = 0)) & ! [v1: event] : ! [v2: int] : ! [v3: time] : (v1 = % 21.05/3.54 | overflow | v1 = tapOn | ~ (at_time(v2) = v3) | ~ (happens(v1, % 21.05/3.54 | v3) = 0) | ~ event(v1)) & ! [v1: event] : ! [v2: int] : ! % 21.05/3.54 | [v3: time] : (v1 = tapOn | ~ (at_time(v2) = v3) | ~ (happens(v1, % 21.05/3.54 | v3) = 0) | ~ event(v1) | (holdsAt(v0, v3) = 0 & % 21.05/3.54 | holdsAt(filling, v3) = 0)) & ! [v1: time] : ! [v2: int] : (v2 % 21.05/3.54 | = 0 | ~ (at_time(0) = v1) | ~ (happens(tapOn, v1) = v2))) % 21.05/3.54 | % 21.05/3.54 | ALPHA: (filling_times) implies: % 21.05/3.55 | (14) fluent(filling) % 21.05/3.55 | (15) ? [v0: int] : ? [v1: time] : ? [v2: time] : ? [v3: int] : ? [v4: % 21.05/3.55 | int] : ( ~ (v4 = 0) & ~ (v3 = 0) & ~ (v0 = 0) & % 21.05/3.55 | releasedAt(filling, v2) = v3 & holdsAt(filling, v2) = v4 & % 21.05/3.55 | holdsAt(filling, v1) = 0 & at_time($sum(v0, 1)) = v1 & at_time(v0) = % 21.05/3.55 | v2 & time(v2) & time(v1)) % 21.05/3.55 | % 21.05/3.55 | ALPHA: (function-axioms) implies: % 21.05/3.55 | (16) ! [v0: time] : ! [v1: time] : ! [v2: int] : (v1 = v0 | ~ % 21.05/3.55 | (at_time(v2) = v1) | ~ (at_time(v2) = v0)) % 21.05/3.55 | (17) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 21.05/3.55 | time] : ! [v3: fluent] : (v1 = v0 | ~ (holdsAt(v3, v2) = v1) | ~ % 21.05/3.55 | (holdsAt(v3, v2) = v0)) % 21.05/3.55 | (18) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 21.05/3.55 | time] : ! [v3: fluent] : (v1 = v0 | ~ (releasedAt(v3, v2) = v1) | % 21.05/3.55 | ~ (releasedAt(v3, v2) = v0)) % 21.05/3.55 | % 21.05/3.55 | DELTA: instantiating (15) with fresh symbols all_43_0, all_43_1, all_43_2, % 21.05/3.55 | all_43_3, all_43_4 gives: % 21.05/3.55 | (19) ~ (all_43_0 = 0) & ~ (all_43_1 = 0) & ~ (all_43_4 = 0) & % 21.05/3.55 | releasedAt(filling, all_43_2) = all_43_1 & holdsAt(filling, all_43_2) % 21.05/3.55 | = all_43_0 & holdsAt(filling, all_43_3) = 0 & at_time($sum(all_43_4, % 21.05/3.55 | 1)) = all_43_3 & at_time(all_43_4) = all_43_2 & time(all_43_2) & % 21.05/3.55 | time(all_43_3) % 21.05/3.55 | % 21.05/3.55 | ALPHA: (19) implies: % 21.05/3.55 | (20) ~ (all_43_4 = 0) % 21.05/3.55 | (21) ~ (all_43_1 = 0) % 21.05/3.55 | (22) ~ (all_43_0 = 0) % 21.05/3.55 | (23) at_time(all_43_4) = all_43_2 % 21.05/3.55 | (24) at_time($sum(all_43_4, 1)) = all_43_3 % 21.05/3.55 | (25) holdsAt(filling, all_43_3) = 0 % 21.05/3.55 | (26) holdsAt(filling, all_43_2) = all_43_0 % 21.05/3.55 | (27) releasedAt(filling, all_43_2) = all_43_1 % 21.05/3.55 | % 21.05/3.55 | DELTA: instantiating (13) with fresh symbol all_45_0 gives: % 21.05/3.55 | (28) waterLevel(3) = all_45_0 & fluent(all_45_0) & ! [v0: int] : ! [v1: % 21.05/3.55 | time] : ! [v2: int] : (v2 = 0 | ~ (at_time(v0) = v1) | ~ % 21.05/3.55 | (happens(overflow, v1) = v2) | ? [v3: any] : ? [v4: any] : % 21.05/3.55 | (holdsAt(all_45_0, v1) = v3 & holdsAt(filling, v1) = v4 & ( ~ (v4 = % 21.05/3.55 | 0) | ~ (v3 = 0)))) & ! [v0: event] : ! [v1: int] : ! [v2: % 21.05/3.55 | time] : (v1 = 0 | v0 = overflow | ~ (at_time(v1) = v2) | ~ % 21.05/3.55 | (happens(v0, v2) = 0) | ~ event(v0)) & ! [v0: event] : ! [v1: % 21.05/3.55 | int] : ! [v2: time] : (v1 = 0 | ~ (at_time(v1) = v2) | ~ % 21.05/3.55 | (happens(v0, v2) = 0) | ~ event(v0) | (holdsAt(all_45_0, v2) = 0 & % 21.05/3.55 | holdsAt(filling, v2) = 0)) & ! [v0: event] : ! [v1: int] : ! % 21.05/3.55 | [v2: time] : (v0 = overflow | v0 = tapOn | ~ (at_time(v1) = v2) | ~ % 21.05/3.55 | (happens(v0, v2) = 0) | ~ event(v0)) & ! [v0: event] : ! [v1: % 21.05/3.55 | int] : ! [v2: time] : (v0 = tapOn | ~ (at_time(v1) = v2) | ~ % 21.05/3.55 | (happens(v0, v2) = 0) | ~ event(v0) | (holdsAt(all_45_0, v2) = 0 & % 21.05/3.55 | holdsAt(filling, v2) = 0)) & ! [v0: time] : ! [v1: int] : (v1 = % 21.05/3.55 | 0 | ~ (at_time(0) = v0) | ~ (happens(tapOn, v0) = v1)) % 21.05/3.55 | % 21.05/3.55 | ALPHA: (28) implies: % 21.05/3.55 | (29) ! [v0: event] : ! [v1: int] : ! [v2: time] : (v0 = tapOn | ~ % 21.05/3.55 | (at_time(v1) = v2) | ~ (happens(v0, v2) = 0) | ~ event(v0) | % 21.05/3.55 | (holdsAt(all_45_0, v2) = 0 & holdsAt(filling, v2) = 0)) % 21.05/3.55 | (30) ! [v0: event] : ! [v1: int] : ! [v2: time] : (v0 = overflow | v0 = % 21.05/3.55 | tapOn | ~ (at_time(v1) = v2) | ~ (happens(v0, v2) = 0) | ~ % 21.05/3.55 | event(v0)) % 21.05/3.55 | (31) ! [v0: event] : ! [v1: int] : ! [v2: time] : (v1 = 0 | v0 = % 21.05/3.55 | overflow | ~ (at_time(v1) = v2) | ~ (happens(v0, v2) = 0) | ~ % 21.05/3.55 | event(v0)) % 21.05/3.55 | % 21.05/3.56 | GROUND_INST: instantiating (3) with filling, all_43_4, all_43_3, simplifying % 21.05/3.56 | with (14), (24), (25) gives: % 21.05/3.56 | (32) ? [v0: time] : ? [v1: any] : ? [v2: any] : ? [v3: event] : ? [v4: % 21.05/3.56 | int] : ? [v5: int] : (releasedAt(filling, all_43_3) = v2 & % 21.05/3.56 | holdsAt(filling, v0) = v1 & at_time(all_43_4) = v0 & event(v3) & % 21.05/3.56 | time(v0) & (v2 = 0 | v1 = 0 | (v5 = 0 & v4 = 0 & initiates(v3, % 21.05/3.56 | filling, v0) = 0 & happens(v3, v0) = 0))) % 21.05/3.56 | % 21.05/3.56 | GROUND_INST: instantiating (1) with filling, $sum(all_43_4, -1), all_43_2, % 21.05/3.56 | all_43_0, simplifying with (14), (23), (26) gives: % 21.05/3.56 | (33) all_43_0 = 0 | ? [v0: time] : ? [v1: any] : ? [v2: any] : ? [v3: % 21.05/3.56 | event] : ? [v4: int] : ? [v5: int] : (releasedAt(filling, % 21.05/3.56 | all_43_2) = v2 & holdsAt(filling, v0) = v1 & % 21.05/3.56 | at_time($sum(all_43_4, -1)) = v0 & event(v3) & time(v0) & ( ~ (v1 = % 21.05/3.56 | 0) | v2 = 0 | (v5 = 0 & v4 = 0 & happens(v3, v0) = 0 & % 21.05/3.56 | terminates(v3, filling, v0) = 0))) % 21.05/3.56 | % 21.05/3.56 | GROUND_INST: instantiating (4) with filling, all_43_4, all_43_2, all_43_0, % 21.05/3.56 | simplifying with (14), (23), (26) gives: % 21.05/3.56 | (34) all_43_0 = 0 | ? [v0: time] : ? [v1: any] : ? [v2: any] : ? [v3: % 21.05/3.56 | event] : ? [v4: int] : ? [v5: int] : (event(v3) & ((v5 = 0 & v4 = % 21.05/3.56 | 0 & initiates(v3, filling, all_43_2) = 0 & happens(v3, all_43_2) % 21.05/3.56 | = 0) | (releasedAt(filling, v0) = v1 & holdsAt(filling, v0) = v2 % 21.05/3.56 | & at_time($sum(all_43_4, 1)) = v0 & time(v0) & ( ~ (v2 = 0) | v1 % 21.05/3.56 | = 0)))) % 21.05/3.56 | % 21.05/3.56 | GROUND_INST: instantiating (5) with filling, $sum(all_43_4, -1), all_43_2, % 21.05/3.56 | all_43_1, simplifying with (14), (23), (27) gives: % 21.05/3.56 | (35) all_43_1 = 0 | ? [v0: time] : ? [v1: any] : ? [v2: any] : ? [v3: % 21.05/3.56 | event] : ? [v4: int] : ? [v5: int] : (holdsAt(filling, v0) = v1 & % 21.05/3.56 | holdsAt(filling, all_43_2) = v2 & at_time($sum(all_43_4, -1)) = v0 & % 21.05/3.56 | event(v3) & time(v0) & ( ~ (v2 = 0) | v1 = 0 | (v5 = 0 & v4 = 0 & % 21.05/3.56 | initiates(v3, filling, v0) = 0 & happens(v3, v0) = 0))) % 21.05/3.56 | % 21.05/3.56 | GROUND_INST: instantiating (2) with filling, $sum(all_43_4, -1), all_43_2, % 21.05/3.56 | all_43_1, simplifying with (14), (23), (27) gives: % 21.05/3.56 | (36) all_43_1 = 0 | ? [v0: time] : ? [v1: any] : ? [v2: any] : ? [v3: % 21.05/3.56 | event] : ? [v4: int] : ? [v5: int] : (holdsAt(filling, v0) = v1 & % 21.05/3.56 | holdsAt(filling, all_43_2) = v2 & at_time($sum(all_43_4, -1)) = v0 & % 21.05/3.56 | event(v3) & time(v0) & ( ~ (v1 = 0) | v2 = 0 | (v5 = 0 & v4 = 0 & % 21.05/3.56 | happens(v3, v0) = 0 & terminates(v3, filling, v0) = 0))) % 21.05/3.56 | % 21.05/3.56 | GROUND_INST: instantiating (7) with filling, all_43_4, all_43_2, all_43_1, % 21.05/3.56 | simplifying with (14), (23), (27) gives: % 21.05/3.56 | (37) all_43_1 = 0 | ? [v0: time] : ? [v1: int] : ? [v2: event] : ? [v3: % 21.05/3.56 | int] : ? [v4: int] : (event(v2) & ((v4 = 0 & v3 = 0 & releases(v2, % 21.05/3.56 | filling, all_43_2) = 0 & happens(v2, all_43_2) = 0) | ( ~ (v1 % 21.05/3.56 | = 0) & releasedAt(filling, v0) = v1 & at_time($sum(all_43_4, % 21.05/3.56 | 1)) = v0 & time(v0)))) % 21.05/3.56 | % 21.05/3.56 | DELTA: instantiating (32) with fresh symbols all_65_0, all_65_1, all_65_2, % 21.05/3.56 | all_65_3, all_65_4, all_65_5 gives: % 21.05/3.56 | (38) releasedAt(filling, all_43_3) = all_65_3 & holdsAt(filling, all_65_5) % 21.05/3.56 | = all_65_4 & at_time(all_43_4) = all_65_5 & event(all_65_2) & % 21.05/3.56 | time(all_65_5) & (all_65_3 = 0 | all_65_4 = 0 | (all_65_0 = 0 & % 21.05/3.56 | all_65_1 = 0 & initiates(all_65_2, filling, all_65_5) = 0 & % 21.05/3.56 | happens(all_65_2, all_65_5) = 0)) % 21.05/3.56 | % 21.05/3.56 | ALPHA: (38) implies: % 21.05/3.56 | (39) event(all_65_2) % 21.05/3.56 | (40) at_time(all_43_4) = all_65_5 % 21.05/3.56 | (41) holdsAt(filling, all_65_5) = all_65_4 % 21.05/3.56 | (42) releasedAt(filling, all_43_3) = all_65_3 % 21.05/3.56 | (43) all_65_3 = 0 | all_65_4 = 0 | (all_65_0 = 0 & all_65_1 = 0 & % 21.05/3.56 | initiates(all_65_2, filling, all_65_5) = 0 & happens(all_65_2, % 21.05/3.56 | all_65_5) = 0) % 21.05/3.56 | % 21.05/3.56 | BETA: splitting (35) gives: % 21.05/3.56 | % 21.05/3.56 | Case 1: % 21.05/3.56 | | % 21.05/3.56 | | (44) all_43_1 = 0 % 21.05/3.56 | | % 21.05/3.56 | | REDUCE: (21), (44) imply: % 21.05/3.56 | | (45) $false % 21.05/3.56 | | % 21.05/3.56 | | CLOSE: (45) is inconsistent. % 21.05/3.56 | | % 21.05/3.56 | Case 2: % 21.05/3.56 | | % 21.05/3.56 | | (46) ? [v0: time] : ? [v1: any] : ? [v2: any] : ? [v3: event] : ? % 21.05/3.56 | | [v4: int] : ? [v5: int] : (holdsAt(filling, v0) = v1 & % 21.05/3.56 | | holdsAt(filling, all_43_2) = v2 & at_time($sum(all_43_4, -1)) = v0 % 21.05/3.56 | | & event(v3) & time(v0) & ( ~ (v2 = 0) | v1 = 0 | (v5 = 0 & v4 = 0 % 21.05/3.56 | | & initiates(v3, filling, v0) = 0 & happens(v3, v0) = 0))) % 21.05/3.56 | | % 21.05/3.56 | | DELTA: instantiating (46) with fresh symbols all_83_0, all_83_1, all_83_2, % 21.05/3.56 | | all_83_3, all_83_4, all_83_5 gives: % 21.05/3.57 | | (47) holdsAt(filling, all_83_5) = all_83_4 & holdsAt(filling, all_43_2) = % 21.05/3.57 | | all_83_3 & at_time($sum(all_43_4, -1)) = all_83_5 & event(all_83_2) % 21.05/3.57 | | & time(all_83_5) & ( ~ (all_83_3 = 0) | all_83_4 = 0 | (all_83_0 = 0 % 21.05/3.57 | | & all_83_1 = 0 & initiates(all_83_2, filling, all_83_5) = 0 & % 21.05/3.57 | | happens(all_83_2, all_83_5) = 0)) % 21.05/3.57 | | % 21.05/3.57 | | ALPHA: (47) implies: % 21.05/3.57 | | (48) holdsAt(filling, all_43_2) = all_83_3 % 21.05/3.57 | | % 21.05/3.57 | | BETA: splitting (37) gives: % 21.05/3.57 | | % 21.05/3.57 | | Case 1: % 21.05/3.57 | | | % 21.05/3.57 | | | (49) all_43_1 = 0 % 21.05/3.57 | | | % 21.05/3.57 | | | REDUCE: (21), (49) imply: % 21.05/3.57 | | | (50) $false % 21.05/3.57 | | | % 21.05/3.57 | | | CLOSE: (50) is inconsistent. % 21.05/3.57 | | | % 21.05/3.57 | | Case 2: % 21.05/3.57 | | | % 21.05/3.57 | | | (51) ? [v0: time] : ? [v1: int] : ? [v2: event] : ? [v3: int] : ? % 21.05/3.57 | | | [v4: int] : (event(v2) & ((v4 = 0 & v3 = 0 & releases(v2, filling, % 21.05/3.57 | | | all_43_2) = 0 & happens(v2, all_43_2) = 0) | ( ~ (v1 = 0) % 21.05/3.57 | | | & releasedAt(filling, v0) = v1 & at_time($sum(all_43_4, 1)) % 21.05/3.57 | | | = v0 & time(v0)))) % 21.05/3.57 | | | % 21.05/3.57 | | | DELTA: instantiating (51) with fresh symbols all_88_0, all_88_1, all_88_2, % 21.05/3.57 | | | all_88_3, all_88_4 gives: % 21.05/3.57 | | | (52) event(all_88_2) & ((all_88_0 = 0 & all_88_1 = 0 & % 21.05/3.57 | | | releases(all_88_2, filling, all_43_2) = 0 & happens(all_88_2, % 21.05/3.57 | | | all_43_2) = 0) | ( ~ (all_88_3 = 0) & releasedAt(filling, % 21.05/3.57 | | | all_88_4) = all_88_3 & at_time($sum(all_43_4, 1)) = all_88_4 % 21.05/3.57 | | | & time(all_88_4))) % 21.05/3.57 | | | % 21.05/3.57 | | | ALPHA: (52) implies: % 21.05/3.57 | | | (53) event(all_88_2) % 21.05/3.57 | | | (54) (all_88_0 = 0 & all_88_1 = 0 & releases(all_88_2, filling, % 21.05/3.57 | | | all_43_2) = 0 & happens(all_88_2, all_43_2) = 0) | ( ~ % 21.05/3.57 | | | (all_88_3 = 0) & releasedAt(filling, all_88_4) = all_88_3 & % 21.05/3.57 | | | at_time($sum(all_43_4, 1)) = all_88_4 & time(all_88_4)) % 21.05/3.57 | | | % 21.05/3.57 | | | BETA: splitting (36) gives: % 21.05/3.57 | | | % 21.05/3.57 | | | Case 1: % 21.05/3.57 | | | | % 21.05/3.57 | | | | (55) all_43_1 = 0 % 21.05/3.57 | | | | % 21.05/3.57 | | | | REDUCE: (21), (55) imply: % 21.05/3.57 | | | | (56) $false % 21.05/3.57 | | | | % 21.05/3.57 | | | | CLOSE: (56) is inconsistent. % 21.05/3.57 | | | | % 21.05/3.57 | | | Case 2: % 21.05/3.57 | | | | % 21.05/3.57 | | | | (57) ? [v0: time] : ? [v1: any] : ? [v2: any] : ? [v3: event] : % 21.05/3.57 | | | | ? [v4: int] : ? [v5: int] : (holdsAt(filling, v0) = v1 & % 21.05/3.57 | | | | holdsAt(filling, all_43_2) = v2 & at_time($sum(all_43_4, -1)) % 21.05/3.57 | | | | = v0 & event(v3) & time(v0) & ( ~ (v1 = 0) | v2 = 0 | (v5 = 0 % 21.05/3.57 | | | | & v4 = 0 & happens(v3, v0) = 0 & terminates(v3, filling, % 21.05/3.57 | | | | v0) = 0))) % 21.05/3.57 | | | | % 21.05/3.57 | | | | DELTA: instantiating (57) with fresh symbols all_118_0, all_118_1, % 21.05/3.57 | | | | all_118_2, all_118_3, all_118_4, all_118_5 gives: % 21.05/3.57 | | | | (58) holdsAt(filling, all_118_5) = all_118_4 & holdsAt(filling, % 21.05/3.57 | | | | all_43_2) = all_118_3 & at_time($sum(all_43_4, -1)) = % 21.05/3.57 | | | | all_118_5 & event(all_118_2) & time(all_118_5) & ( ~ (all_118_4 % 21.05/3.57 | | | | = 0) | all_118_3 = 0 | (all_118_0 = 0 & all_118_1 = 0 & % 21.05/3.57 | | | | happens(all_118_2, all_118_5) = 0 & terminates(all_118_2, % 21.05/3.57 | | | | filling, all_118_5) = 0)) % 21.05/3.57 | | | | % 21.05/3.57 | | | | ALPHA: (58) implies: % 21.05/3.57 | | | | (59) holdsAt(filling, all_43_2) = all_118_3 % 21.05/3.57 | | | | % 21.05/3.57 | | | | BETA: splitting (34) gives: % 21.05/3.57 | | | | % 21.05/3.57 | | | | Case 1: % 21.05/3.57 | | | | | % 21.05/3.57 | | | | | (60) all_43_0 = 0 % 21.05/3.57 | | | | | % 21.05/3.57 | | | | | REDUCE: (22), (60) imply: % 21.05/3.57 | | | | | (61) $false % 21.05/3.57 | | | | | % 21.05/3.57 | | | | | CLOSE: (61) is inconsistent. % 21.05/3.57 | | | | | % 21.05/3.57 | | | | Case 2: % 21.05/3.57 | | | | | % 21.05/3.57 | | | | | (62) ? [v0: time] : ? [v1: any] : ? [v2: any] : ? [v3: event] : % 21.05/3.57 | | | | | ? [v4: int] : ? [v5: int] : (event(v3) & ((v5 = 0 & v4 = 0 & % 21.05/3.57 | | | | | initiates(v3, filling, all_43_2) = 0 & happens(v3, % 21.05/3.57 | | | | | all_43_2) = 0) | (releasedAt(filling, v0) = v1 & % 21.05/3.57 | | | | | holdsAt(filling, v0) = v2 & at_time($sum(all_43_4, 1)) = % 21.05/3.57 | | | | | v0 & time(v0) & ( ~ (v2 = 0) | v1 = 0)))) % 21.05/3.57 | | | | | % 21.05/3.57 | | | | | DELTA: instantiating (62) with fresh symbols all_128_0, all_128_1, % 21.05/3.57 | | | | | all_128_2, all_128_3, all_128_4, all_128_5 gives: % 21.42/3.57 | | | | | (63) event(all_128_2) & ((all_128_0 = 0 & all_128_1 = 0 & % 21.42/3.57 | | | | | initiates(all_128_2, filling, all_43_2) = 0 & % 21.42/3.57 | | | | | happens(all_128_2, all_43_2) = 0) | (releasedAt(filling, % 21.42/3.57 | | | | | all_128_5) = all_128_4 & holdsAt(filling, all_128_5) = % 21.42/3.57 | | | | | all_128_3 & at_time($sum(all_43_4, 1)) = all_128_5 & % 21.42/3.57 | | | | | time(all_128_5) & ( ~ (all_128_3 = 0) | all_128_4 = 0))) % 21.42/3.57 | | | | | % 21.42/3.57 | | | | | ALPHA: (63) implies: % 21.42/3.57 | | | | | (64) event(all_128_2) % 21.42/3.57 | | | | | (65) (all_128_0 = 0 & all_128_1 = 0 & initiates(all_128_2, filling, % 21.42/3.57 | | | | | all_43_2) = 0 & happens(all_128_2, all_43_2) = 0) | % 21.42/3.57 | | | | | (releasedAt(filling, all_128_5) = all_128_4 & holdsAt(filling, % 21.42/3.57 | | | | | all_128_5) = all_128_3 & at_time($sum(all_43_4, 1)) = % 21.42/3.57 | | | | | all_128_5 & time(all_128_5) & ( ~ (all_128_3 = 0) | % 21.42/3.57 | | | | | all_128_4 = 0)) % 21.42/3.57 | | | | | % 21.42/3.57 | | | | | BETA: splitting (33) gives: % 21.42/3.57 | | | | | % 21.42/3.57 | | | | | Case 1: % 21.42/3.57 | | | | | | % 21.42/3.57 | | | | | | (66) all_43_0 = 0 % 21.42/3.57 | | | | | | % 21.42/3.57 | | | | | | REDUCE: (22), (66) imply: % 21.42/3.57 | | | | | | (67) $false % 21.42/3.57 | | | | | | % 21.42/3.57 | | | | | | CLOSE: (67) is inconsistent. % 21.42/3.57 | | | | | | % 21.42/3.57 | | | | | Case 2: % 21.42/3.57 | | | | | | % 21.42/3.57 | | | | | | % 21.42/3.57 | | | | | | GROUND_INST: instantiating (16) with all_43_2, all_65_5, all_43_4, % 21.42/3.57 | | | | | | simplifying with (23), (40) gives: % 21.42/3.57 | | | | | | (68) all_65_5 = all_43_2 % 21.42/3.57 | | | | | | % 21.42/3.57 | | | | | | GROUND_INST: instantiating (17) with all_43_0, all_118_3, all_43_2, % 21.42/3.57 | | | | | | filling, simplifying with (26), (59) gives: % 21.42/3.57 | | | | | | (69) all_118_3 = all_43_0 % 21.42/3.57 | | | | | | % 21.42/3.57 | | | | | | GROUND_INST: instantiating (17) with all_83_3, all_118_3, all_43_2, % 21.42/3.57 | | | | | | filling, simplifying with (48), (59) gives: % 21.42/3.57 | | | | | | (70) all_118_3 = all_83_3 % 21.42/3.57 | | | | | | % 21.42/3.57 | | | | | | COMBINE_EQS: (69), (70) imply: % 21.42/3.57 | | | | | | (71) all_83_3 = all_43_0 % 21.42/3.57 | | | | | | % 21.42/3.57 | | | | | | REDUCE: (41), (68) imply: % 21.42/3.57 | | | | | | (72) holdsAt(filling, all_43_2) = all_65_4 % 21.42/3.57 | | | | | | % 21.42/3.57 | | | | | | GROUND_INST: instantiating (17) with all_43_0, all_65_4, all_43_2, % 21.42/3.57 | | | | | | filling, simplifying with (26), (72) gives: % 21.42/3.57 | | | | | | (73) all_65_4 = all_43_0 % 21.42/3.57 | | | | | | % 21.42/3.57 | | | | | | GROUND_INST: instantiating (6) with filling, all_43_4, all_43_3, % 21.42/3.57 | | | | | | all_65_3, simplifying with (14), (24), (42) gives: % 21.42/3.57 | | | | | | (74) all_65_3 = 0 | ? [v0: time] : ? [v1: any] : ? [v2: event] % 21.42/3.57 | | | | | | : ? [v3: int] : ? [v4: any] : ? [v5: any] : % 21.42/3.57 | | | | | | (releasedAt(filling, v0) = v1 & at_time(all_43_4) = v0 & % 21.42/3.57 | | | | | | event(v2) & time(v0) & ( ~ (v1 = 0) | (v3 = 0 & % 21.42/3.57 | | | | | | initiates(v2, filling, v0) = v4 & happens(v2, v0) = 0 % 21.42/3.57 | | | | | | & terminates(v2, filling, v0) = v5 & (v5 = 0 | v4 = % 21.42/3.57 | | | | | | 0)))) % 21.42/3.57 | | | | | | % 21.42/3.57 | | | | | | GROUND_INST: instantiating (5) with filling, all_43_4, all_43_3, % 21.42/3.57 | | | | | | all_65_3, simplifying with (14), (24), (42) gives: % 21.42/3.57 | | | | | | (75) all_65_3 = 0 | ? [v0: time] : ? [v1: any] : ? [v2: any] : % 21.42/3.57 | | | | | | ? [v3: event] : ? [v4: int] : ? [v5: int] : % 21.42/3.57 | | | | | | (holdsAt(filling, v0) = v1 & holdsAt(filling, all_43_3) = v2 % 21.42/3.57 | | | | | | & at_time(all_43_4) = v0 & event(v3) & time(v0) & ( ~ (v2 % 21.42/3.57 | | | | | | = 0) | v1 = 0 | (v5 = 0 & v4 = 0 & initiates(v3, % 21.42/3.57 | | | | | | filling, v0) = 0 & happens(v3, v0) = 0))) % 21.42/3.58 | | | | | | % 21.42/3.58 | | | | | | GROUND_INST: instantiating (2) with filling, all_43_4, all_43_3, % 21.42/3.58 | | | | | | all_65_3, simplifying with (14), (24), (42) gives: % 21.42/3.58 | | | | | | (76) all_65_3 = 0 | ? [v0: time] : ? [v1: any] : ? [v2: any] : % 21.42/3.58 | | | | | | ? [v3: event] : ? [v4: int] : ? [v5: int] : % 21.42/3.58 | | | | | | (holdsAt(filling, v0) = v1 & holdsAt(filling, all_43_3) = v2 % 21.42/3.58 | | | | | | & at_time(all_43_4) = v0 & event(v3) & time(v0) & ( ~ (v1 % 21.42/3.58 | | | | | | = 0) | v2 = 0 | (v5 = 0 & v4 = 0 & happens(v3, v0) = 0 % 21.42/3.58 | | | | | | & terminates(v3, filling, v0) = 0))) % 21.42/3.58 | | | | | | % 21.42/3.58 | | | | | | BETA: splitting (43) gives: % 21.42/3.58 | | | | | | % 21.42/3.58 | | | | | | Case 1: % 21.42/3.58 | | | | | | | % 21.42/3.58 | | | | | | | (77) all_65_3 = 0 % 21.42/3.58 | | | | | | | % 21.42/3.58 | | | | | | | REDUCE: (42), (77) imply: % 21.42/3.58 | | | | | | | (78) releasedAt(filling, all_43_3) = 0 % 21.42/3.58 | | | | | | | % 21.42/3.58 | | | | | | | BETA: splitting (54) gives: % 21.42/3.58 | | | | | | | % 21.42/3.58 | | | | | | | Case 1: % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | (79) all_88_0 = 0 & all_88_1 = 0 & releases(all_88_2, % 21.42/3.58 | | | | | | | | filling, all_43_2) = 0 & happens(all_88_2, all_43_2) = % 21.42/3.58 | | | | | | | | 0 % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | ALPHA: (79) implies: % 21.42/3.58 | | | | | | | | (80) happens(all_88_2, all_43_2) = 0 % 21.42/3.58 | | | | | | | | (81) releases(all_88_2, filling, all_43_2) = 0 % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | GROUND_INST: instantiating (31) with all_88_2, all_43_4, % 21.42/3.58 | | | | | | | | all_43_2, simplifying with (23), (53), (80) gives: % 21.42/3.58 | | | | | | | | (82) all_88_2 = overflow | all_43_4 = 0 % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | GROUND_INST: instantiating (12) with all_88_2, filling, % 21.42/3.58 | | | | | | | | all_43_4, all_43_2, simplifying with (14), (23), % 21.42/3.58 | | | | | | | | (53), (81) gives: % 21.42/3.58 | | | | | | | | (83) ? [v0: int] : (all_88_2 = tapOn & waterLevel(v0) = % 21.42/3.58 | | | | | | | | filling) % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | DELTA: instantiating (83) with fresh symbol all_245_0 gives: % 21.42/3.58 | | | | | | | | (84) all_88_2 = tapOn & waterLevel(all_245_0) = filling % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | ALPHA: (84) implies: % 21.42/3.58 | | | | | | | | (85) all_88_2 = tapOn % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | BETA: splitting (82) gives: % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | Case 1: % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | (86) all_88_2 = overflow % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | COMBINE_EQS: (85), (86) imply: % 21.42/3.58 | | | | | | | | | (87) overflow = tapOn % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | REDUCE: (8), (87) imply: % 21.42/3.58 | | | | | | | | | (88) $false % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | CLOSE: (88) is inconsistent. % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | Case 2: % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | (89) all_43_4 = 0 % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | REDUCE: (20), (89) imply: % 21.42/3.58 | | | | | | | | | (90) $false % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | CLOSE: (90) is inconsistent. % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | End of split % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | Case 2: % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | (91) ~ (all_88_3 = 0) & releasedAt(filling, all_88_4) = % 21.42/3.58 | | | | | | | | all_88_3 & at_time($sum(all_43_4, 1)) = all_88_4 & % 21.42/3.58 | | | | | | | | time(all_88_4) % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | ALPHA: (91) implies: % 21.42/3.58 | | | | | | | | (92) ~ (all_88_3 = 0) % 21.42/3.58 | | | | | | | | (93) at_time($sum(all_43_4, 1)) = all_88_4 % 21.42/3.58 | | | | | | | | (94) releasedAt(filling, all_88_4) = all_88_3 % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | GROUND_INST: instantiating (16) with all_43_3, all_88_4, % 21.42/3.58 | | | | | | | | $sum(all_43_4, 1), simplifying with (24), (93) % 21.42/3.58 | | | | | | | | gives: % 21.42/3.58 | | | | | | | | (95) all_88_4 = all_43_3 % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | REDUCE: (94), (95) imply: % 21.42/3.58 | | | | | | | | (96) releasedAt(filling, all_43_3) = all_88_3 % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | GROUND_INST: instantiating (18) with 0, all_88_3, all_43_3, % 21.42/3.58 | | | | | | | | filling, simplifying with (78), (96) gives: % 21.42/3.58 | | | | | | | | (97) all_88_3 = 0 % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | REDUCE: (92), (97) imply: % 21.42/3.58 | | | | | | | | (98) $false % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | CLOSE: (98) is inconsistent. % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | End of split % 21.42/3.58 | | | | | | | % 21.42/3.58 | | | | | | Case 2: % 21.42/3.58 | | | | | | | % 21.42/3.58 | | | | | | | (99) ~ (all_65_3 = 0) % 21.42/3.58 | | | | | | | (100) all_65_4 = 0 | (all_65_0 = 0 & all_65_1 = 0 & % 21.42/3.58 | | | | | | | initiates(all_65_2, filling, all_65_5) = 0 & % 21.42/3.58 | | | | | | | happens(all_65_2, all_65_5) = 0) % 21.42/3.58 | | | | | | | % 21.42/3.58 | | | | | | | BETA: splitting (65) gives: % 21.42/3.58 | | | | | | | % 21.42/3.58 | | | | | | | Case 1: % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | (101) all_128_0 = 0 & all_128_1 = 0 & initiates(all_128_2, % 21.42/3.58 | | | | | | | | filling, all_43_2) = 0 & happens(all_128_2, all_43_2) % 21.42/3.58 | | | | | | | | = 0 % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | ALPHA: (101) implies: % 21.42/3.58 | | | | | | | | (102) happens(all_128_2, all_43_2) = 0 % 21.42/3.58 | | | | | | | | (103) initiates(all_128_2, filling, all_43_2) = 0 % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | BETA: splitting (100) gives: % 21.42/3.58 | | | | | | | | % 21.42/3.58 | | | | | | | | Case 1: % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | (104) all_65_4 = 0 % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | COMBINE_EQS: (73), (104) imply: % 21.42/3.58 | | | | | | | | | (105) all_43_0 = 0 % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | SIMP: (105) implies: % 21.42/3.58 | | | | | | | | | (106) all_43_0 = 0 % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | REDUCE: (22), (106) imply: % 21.42/3.58 | | | | | | | | | (107) $false % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | CLOSE: (107) is inconsistent. % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | Case 2: % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | (108) ~ (all_65_4 = 0) % 21.42/3.58 | | | | | | | | | (109) all_65_0 = 0 & all_65_1 = 0 & initiates(all_65_2, % 21.42/3.58 | | | | | | | | | filling, all_65_5) = 0 & happens(all_65_2, % 21.42/3.58 | | | | | | | | | all_65_5) = 0 % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | ALPHA: (109) implies: % 21.42/3.58 | | | | | | | | | (110) happens(all_65_2, all_65_5) = 0 % 21.42/3.58 | | | | | | | | | (111) initiates(all_65_2, filling, all_65_5) = 0 % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | REDUCE: (68), (111) imply: % 21.42/3.58 | | | | | | | | | (112) initiates(all_65_2, filling, all_43_2) = 0 % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | REDUCE: (68), (110) imply: % 21.42/3.58 | | | | | | | | | (113) happens(all_65_2, all_43_2) = 0 % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | BETA: splitting (76) gives: % 21.42/3.58 | | | | | | | | | % 21.42/3.58 | | | | | | | | | Case 1: % 21.42/3.58 | | | | | | | | | | % 21.42/3.58 | | | | | | | | | | (114) all_65_3 = 0 % 21.42/3.58 | | | | | | | | | | % 21.42/3.58 | | | | | | | | | | REDUCE: (99), (114) imply: % 21.42/3.58 | | | | | | | | | | (115) $false % 21.42/3.58 | | | | | | | | | | % 21.42/3.58 | | | | | | | | | | CLOSE: (115) is inconsistent. % 21.42/3.58 | | | | | | | | | | % 21.42/3.58 | | | | | | | | | Case 2: % 21.42/3.58 | | | | | | | | | | % 21.42/3.58 | | | | | | | | | | (116) ? [v0: time] : ? [v1: any] : ? [v2: any] : ? % 21.42/3.58 | | | | | | | | | | [v3: event] : ? [v4: int] : ? [v5: int] : % 21.42/3.58 | | | | | | | | | | (holdsAt(filling, v0) = v1 & holdsAt(filling, % 21.42/3.58 | | | | | | | | | | all_43_3) = v2 & at_time(all_43_4) = v0 & % 21.42/3.58 | | | | | | | | | | event(v3) & time(v0) & ( ~ (v1 = 0) | v2 = 0 | % 21.42/3.58 | | | | | | | | | | (v5 = 0 & v4 = 0 & happens(v3, v0) = 0 & % 21.42/3.58 | | | | | | | | | | terminates(v3, filling, v0) = 0))) % 21.42/3.58 | | | | | | | | | | % 21.42/3.58 | | | | | | | | | | DELTA: instantiating (116) with fresh symbols all_247_0, % 21.42/3.58 | | | | | | | | | | all_247_1, all_247_2, all_247_3, all_247_4, all_247_5 % 21.42/3.58 | | | | | | | | | | gives: % 21.42/3.58 | | | | | | | | | | (117) holdsAt(filling, all_247_5) = all_247_4 & % 21.42/3.58 | | | | | | | | | | holdsAt(filling, all_43_3) = all_247_3 & % 21.42/3.58 | | | | | | | | | | at_time(all_43_4) = all_247_5 & event(all_247_2) & % 21.42/3.58 | | | | | | | | | | time(all_247_5) & ( ~ (all_247_4 = 0) | all_247_3 = % 21.42/3.58 | | | | | | | | | | 0 | (all_247_0 = 0 & all_247_1 = 0 & % 21.42/3.58 | | | | | | | | | | happens(all_247_2, all_247_5) = 0 & % 21.42/3.58 | | | | | | | | | | terminates(all_247_2, filling, all_247_5) = 0)) % 21.42/3.58 | | | | | | | | | | % 21.42/3.58 | | | | | | | | | | ALPHA: (117) implies: % 21.42/3.58 | | | | | | | | | | (118) at_time(all_43_4) = all_247_5 % 21.42/3.58 | | | | | | | | | | (119) holdsAt(filling, all_43_3) = all_247_3 % 21.42/3.58 | | | | | | | | | | (120) holdsAt(filling, all_247_5) = all_247_4 % 21.42/3.58 | | | | | | | | | | % 21.42/3.58 | | | | | | | | | | BETA: splitting (74) gives: % 21.42/3.58 | | | | | | | | | | % 21.42/3.58 | | | | | | | | | | Case 1: % 21.42/3.58 | | | | | | | | | | | % 21.42/3.58 | | | | | | | | | | | (121) all_65_3 = 0 % 21.42/3.58 | | | | | | | | | | | % 21.42/3.58 | | | | | | | | | | | REDUCE: (99), (121) imply: % 21.42/3.58 | | | | | | | | | | | (122) $false % 21.42/3.58 | | | | | | | | | | | % 21.42/3.58 | | | | | | | | | | | CLOSE: (122) is inconsistent. % 21.42/3.58 | | | | | | | | | | | % 21.42/3.58 | | | | | | | | | | Case 2: % 21.42/3.58 | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | (123) ? [v0: time] : ? [v1: any] : ? [v2: event] : ? % 21.42/3.59 | | | | | | | | | | | [v3: int] : ? [v4: any] : ? [v5: any] : % 21.42/3.59 | | | | | | | | | | | (releasedAt(filling, v0) = v1 & at_time(all_43_4) % 21.42/3.59 | | | | | | | | | | | = v0 & event(v2) & time(v0) & ( ~ (v1 = 0) | (v3 % 21.42/3.59 | | | | | | | | | | | = 0 & initiates(v2, filling, v0) = v4 & % 21.42/3.59 | | | | | | | | | | | happens(v2, v0) = 0 & terminates(v2, % 21.42/3.59 | | | | | | | | | | | filling, v0) = v5 & (v5 = 0 | v4 = 0)))) % 21.42/3.59 | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | DELTA: instantiating (123) with fresh symbols all_252_0, % 21.42/3.59 | | | | | | | | | | | all_252_1, all_252_2, all_252_3, all_252_4, % 21.42/3.59 | | | | | | | | | | | all_252_5 gives: % 21.42/3.59 | | | | | | | | | | | (124) releasedAt(filling, all_252_5) = all_252_4 & % 21.42/3.59 | | | | | | | | | | | at_time(all_43_4) = all_252_5 & event(all_252_3) & % 21.42/3.59 | | | | | | | | | | | time(all_252_5) & ( ~ (all_252_4 = 0) | (all_252_2 % 21.42/3.59 | | | | | | | | | | | = 0 & initiates(all_252_3, filling, all_252_5) % 21.42/3.59 | | | | | | | | | | | = all_252_1 & happens(all_252_3, all_252_5) = % 21.42/3.59 | | | | | | | | | | | 0 & terminates(all_252_3, filling, all_252_5) % 21.42/3.59 | | | | | | | | | | | = all_252_0 & (all_252_0 = 0 | all_252_1 = % 21.42/3.59 | | | | | | | | | | | 0))) % 21.42/3.59 | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | ALPHA: (124) implies: % 21.42/3.59 | | | | | | | | | | | (125) at_time(all_43_4) = all_252_5 % 21.42/3.59 | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | BETA: splitting (75) gives: % 21.42/3.59 | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | Case 1: % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | (126) all_65_3 = 0 % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | REDUCE: (99), (126) imply: % 21.42/3.59 | | | | | | | | | | | | (127) $false % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | CLOSE: (127) is inconsistent. % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | Case 2: % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | (128) ? [v0: time] : ? [v1: any] : ? [v2: any] : ? % 21.42/3.59 | | | | | | | | | | | | [v3: event] : ? [v4: int] : ? [v5: int] : % 21.42/3.59 | | | | | | | | | | | | (holdsAt(filling, v0) = v1 & holdsAt(filling, % 21.42/3.59 | | | | | | | | | | | | all_43_3) = v2 & at_time(all_43_4) = v0 & % 21.42/3.59 | | | | | | | | | | | | event(v3) & time(v0) & ( ~ (v2 = 0) | v1 = 0 | % 21.42/3.59 | | | | | | | | | | | | (v5 = 0 & v4 = 0 & initiates(v3, filling, v0) % 21.42/3.59 | | | | | | | | | | | | = 0 & happens(v3, v0) = 0))) % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | DELTA: instantiating (128) with fresh symbols all_257_0, % 21.42/3.59 | | | | | | | | | | | | all_257_1, all_257_2, all_257_3, all_257_4, % 21.42/3.59 | | | | | | | | | | | | all_257_5 gives: % 21.42/3.59 | | | | | | | | | | | | (129) holdsAt(filling, all_257_5) = all_257_4 & % 21.42/3.59 | | | | | | | | | | | | holdsAt(filling, all_43_3) = all_257_3 & % 21.42/3.59 | | | | | | | | | | | | at_time(all_43_4) = all_257_5 & event(all_257_2) & % 21.42/3.59 | | | | | | | | | | | | time(all_257_5) & ( ~ (all_257_3 = 0) | all_257_4 % 21.42/3.59 | | | | | | | | | | | | = 0 | (all_257_0 = 0 & all_257_1 = 0 & % 21.42/3.59 | | | | | | | | | | | | initiates(all_257_2, filling, all_257_5) = 0 & % 21.42/3.59 | | | | | | | | | | | | happens(all_257_2, all_257_5) = 0)) % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | ALPHA: (129) implies: % 21.42/3.59 | | | | | | | | | | | | (130) event(all_257_2) % 21.42/3.59 | | | | | | | | | | | | (131) at_time(all_43_4) = all_257_5 % 21.42/3.59 | | | | | | | | | | | | (132) holdsAt(filling, all_43_3) = all_257_3 % 21.42/3.59 | | | | | | | | | | | | (133) holdsAt(filling, all_257_5) = all_257_4 % 21.42/3.59 | | | | | | | | | | | | (134) ~ (all_257_3 = 0) | all_257_4 = 0 | (all_257_0 = % 21.42/3.59 | | | | | | | | | | | | 0 & all_257_1 = 0 & initiates(all_257_2, % 21.42/3.59 | | | | | | | | | | | | filling, all_257_5) = 0 & happens(all_257_2, % 21.42/3.59 | | | | | | | | | | | | all_257_5) = 0) % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_43_2, all_252_5, % 21.42/3.59 | | | | | | | | | | | | all_43_4, simplifying with (23), (125) gives: % 21.42/3.59 | | | | | | | | | | | | (135) all_252_5 = all_43_2 % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_252_5, all_257_5, % 21.42/3.59 | | | | | | | | | | | | all_43_4, simplifying with (125), (131) gives: % 21.42/3.59 | | | | | | | | | | | | (136) all_257_5 = all_252_5 % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | GROUND_INST: instantiating (16) with all_247_5, all_257_5, % 21.42/3.59 | | | | | | | | | | | | all_43_4, simplifying with (118), (131) gives: % 21.42/3.59 | | | | | | | | | | | | (137) all_257_5 = all_247_5 % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | GROUND_INST: instantiating (17) with 0, all_257_3, all_43_3, % 21.42/3.59 | | | | | | | | | | | | filling, simplifying with (25), (132) gives: % 21.42/3.59 | | | | | | | | | | | | (138) all_257_3 = 0 % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | GROUND_INST: instantiating (17) with all_247_3, all_257_3, % 21.42/3.59 | | | | | | | | | | | | all_43_3, filling, simplifying with (119), (132) % 21.42/3.59 | | | | | | | | | | | | gives: % 21.42/3.59 | | | | | | | | | | | | (139) all_257_3 = all_247_3 % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | COMBINE_EQS: (138), (139) imply: % 21.42/3.59 | | | | | | | | | | | | (140) all_247_3 = 0 % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | COMBINE_EQS: (136), (137) imply: % 21.42/3.59 | | | | | | | | | | | | (141) all_252_5 = all_247_5 % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | SIMP: (141) implies: % 21.42/3.59 | | | | | | | | | | | | (142) all_252_5 = all_247_5 % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | COMBINE_EQS: (135), (142) imply: % 21.42/3.59 | | | | | | | | | | | | (143) all_247_5 = all_43_2 % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | COMBINE_EQS: (137), (143) imply: % 21.42/3.59 | | | | | | | | | | | | (144) all_257_5 = all_43_2 % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | REDUCE: (133), (144) imply: % 21.42/3.59 | | | | | | | | | | | | (145) holdsAt(filling, all_43_2) = all_257_4 % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | REDUCE: (120), (143) imply: % 21.42/3.59 | | | | | | | | | | | | (146) holdsAt(filling, all_43_2) = all_247_4 % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | GROUND_INST: instantiating (17) with all_43_0, all_257_4, % 21.42/3.59 | | | | | | | | | | | | all_43_2, filling, simplifying with (26), (145) % 21.42/3.59 | | | | | | | | | | | | gives: % 21.42/3.59 | | | | | | | | | | | | (147) all_257_4 = all_43_0 % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | GROUND_INST: instantiating (17) with all_247_4, all_257_4, % 21.42/3.59 | | | | | | | | | | | | all_43_2, filling, simplifying with (145), (146) % 21.42/3.59 | | | | | | | | | | | | gives: % 21.42/3.59 | | | | | | | | | | | | (148) all_257_4 = all_247_4 % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | COMBINE_EQS: (147), (148) imply: % 21.42/3.59 | | | | | | | | | | | | (149) all_247_4 = all_43_0 % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | BETA: splitting (134) gives: % 21.42/3.59 | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | Case 1: % 21.42/3.59 | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | (150) ~ (all_257_3 = 0) % 21.42/3.59 | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | REDUCE: (138), (150) imply: % 21.42/3.59 | | | | | | | | | | | | | (151) $false % 21.42/3.59 | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | CLOSE: (151) is inconsistent. % 21.42/3.59 | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | Case 2: % 21.42/3.59 | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | (152) all_257_4 = 0 | (all_257_0 = 0 & all_257_1 = 0 & % 21.42/3.59 | | | | | | | | | | | | | initiates(all_257_2, filling, all_257_5) = 0 & % 21.42/3.59 | | | | | | | | | | | | | happens(all_257_2, all_257_5) = 0) % 21.42/3.59 | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | BETA: splitting (152) gives: % 21.42/3.59 | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | Case 1: % 21.42/3.59 | | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | | (153) all_257_4 = 0 % 21.42/3.59 | | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | | COMBINE_EQS: (147), (153) imply: % 21.42/3.59 | | | | | | | | | | | | | | (154) all_43_0 = 0 % 21.42/3.59 | | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | | REDUCE: (22), (154) imply: % 21.42/3.59 | | | | | | | | | | | | | | (155) $false % 21.42/3.59 | | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | | CLOSE: (155) is inconsistent. % 21.42/3.59 | | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | Case 2: % 21.42/3.59 | | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | | (156) all_257_0 = 0 & all_257_1 = 0 & % 21.42/3.59 | | | | | | | | | | | | | | initiates(all_257_2, filling, all_257_5) = 0 & % 21.42/3.59 | | | | | | | | | | | | | | happens(all_257_2, all_257_5) = 0 % 21.42/3.59 | | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | | ALPHA: (156) implies: % 21.42/3.59 | | | | | | | | | | | | | | (157) happens(all_257_2, all_257_5) = 0 % 21.42/3.59 | | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | | REDUCE: (144), (157) imply: % 21.42/3.59 | | | | | | | | | | | | | | (158) happens(all_257_2, all_43_2) = 0 % 21.42/3.59 | | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | | GROUND_INST: instantiating (31) with all_65_2, all_43_4, % 21.42/3.59 | | | | | | | | | | | | | | all_43_2, simplifying with (23), (39), (113) % 21.42/3.59 | | | | | | | | | | | | | | gives: % 21.42/3.59 | | | | | | | | | | | | | | (159) all_65_2 = overflow | all_43_4 = 0 % 21.42/3.59 | | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | | GROUND_INST: instantiating (31) with all_128_2, all_43_4, % 21.42/3.59 | | | | | | | | | | | | | | all_43_2, simplifying with (23), (64), (102) % 21.42/3.59 | | | | | | | | | | | | | | gives: % 21.42/3.59 | | | | | | | | | | | | | | (160) all_128_2 = overflow | all_43_4 = 0 % 21.42/3.59 | | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | | GROUND_INST: instantiating (30) with all_128_2, all_43_4, % 21.42/3.59 | | | | | | | | | | | | | | all_43_2, simplifying with (23), (64), (102) % 21.42/3.59 | | | | | | | | | | | | | | gives: % 21.42/3.59 | | | | | | | | | | | | | | (161) all_128_2 = overflow | all_128_2 = tapOn % 21.42/3.59 | | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | | GROUND_INST: instantiating (29) with all_128_2, all_43_4, % 21.42/3.59 | | | | | | | | | | | | | | all_43_2, simplifying with (23), (64), (102) % 21.42/3.59 | | | | | | | | | | | | | | gives: % 21.42/3.59 | | | | | | | | | | | | | | (162) all_128_2 = tapOn | (holdsAt(all_45_0, all_43_2) = % 21.42/3.59 | | | | | | | | | | | | | | 0 & holdsAt(filling, all_43_2) = 0) % 21.42/3.59 | | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | | GROUND_INST: instantiating (31) with all_257_2, all_43_4, % 21.42/3.59 | | | | | | | | | | | | | | all_43_2, simplifying with (23), (130), (158) % 21.42/3.59 | | | | | | | | | | | | | | gives: % 21.42/3.59 | | | | | | | | | | | | | | (163) all_257_2 = overflow | all_43_4 = 0 % 21.42/3.59 | | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | | GROUND_INST: instantiating (29) with all_257_2, all_43_4, % 21.42/3.59 | | | | | | | | | | | | | | all_43_2, simplifying with (23), (130), (158) % 21.42/3.59 | | | | | | | | | | | | | | gives: % 21.42/3.59 | | | | | | | | | | | | | | (164) all_257_2 = tapOn | (holdsAt(all_45_0, all_43_2) = % 21.42/3.59 | | | | | | | | | | | | | | 0 & holdsAt(filling, all_43_2) = 0) % 21.42/3.59 | | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | | GROUND_INST: instantiating (11) with all_65_2, filling, % 21.42/3.59 | | | | | | | | | | | | | | all_43_4, all_43_2, simplifying with (14), (23), % 21.42/3.59 | | | | | | | | | | | | | | (39), (112) gives: % 21.42/3.59 | | | | | | | | | | | | | | (165) all_65_2 = tapOn | filling = spilling | ? [v0: % 21.42/3.59 | | | | | | | | | | | | | | int] : ? [v1: fluent] : ? [v2: int] : ((v2 = 0 % 21.42/3.59 | | | | | | | | | | | | | | & v1 = filling & all_65_2 = overflow & % 21.42/3.59 | | | | | | | | | | | | | | waterLevel(v0) = filling & holdsAt(filling, % 21.42/3.59 | | | | | | | | | | | | | | all_43_2) = 0) | (v2 = 0 & v1 = filling & % 21.42/3.59 | | | | | | | | | | | | | | all_65_2 = tapOff & waterLevel(v0) = filling & % 21.42/3.59 | | | | | | | | | | | | | | holdsAt(filling, all_43_2) = 0)) % 21.42/3.59 | | | | | | | | | | | | | | % 21.42/3.59 | | | | | | | | | | | | | | GROUND_INST: instantiating (11) with all_128_2, filling, % 21.42/3.59 | | | | | | | | | | | | | | all_43_4, all_43_2, simplifying with (14), (23), % 21.42/3.59 | | | | | | | | | | | | | | (64), (103) gives: % 21.42/3.60 | | | | | | | | | | | | | | (166) all_128_2 = tapOn | filling = spilling | ? [v0: % 21.42/3.60 | | | | | | | | | | | | | | int] : ? [v1: fluent] : ? [v2: int] : ((v2 = 0 % 21.42/3.60 | | | | | | | | | | | | | | & v1 = filling & all_128_2 = overflow & % 21.42/3.60 | | | | | | | | | | | | | | waterLevel(v0) = filling & holdsAt(filling, % 21.42/3.60 | | | | | | | | | | | | | | all_43_2) = 0) | (v2 = 0 & v1 = filling & % 21.42/3.60 | | | | | | | | | | | | | | all_128_2 = tapOff & waterLevel(v0) = filling % 21.42/3.60 | | | | | | | | | | | | | | & holdsAt(filling, all_43_2) = 0)) % 21.42/3.60 | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | BETA: splitting (164) gives: % 21.42/3.60 | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | Case 1: % 21.42/3.60 | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | (167) all_257_2 = tapOn % 21.42/3.60 | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | BETA: splitting (162) gives: % 21.42/3.60 | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | Case 1: % 21.42/3.60 | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | (168) all_128_2 = tapOn % 21.42/3.60 | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | REF_CLOSE: (8), (20), (160), (168) are inconsistent by % 21.42/3.60 | | | | | | | | | | | | | | | | sub-proof #2. % 21.42/3.60 | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | Case 2: % 21.42/3.60 | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | (169) ~ (all_128_2 = tapOn) % 21.42/3.60 | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | REF_CLOSE: (8), (20), (160), (161), (163), (167), (169) are % 21.42/3.60 | | | | | | | | | | | | | | | | inconsistent by sub-proof #1. % 21.42/3.60 | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | End of split % 21.42/3.60 | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | Case 2: % 21.42/3.60 | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | (170) ~ (all_257_2 = tapOn) % 21.42/3.60 | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | BETA: splitting (163) gives: % 21.42/3.60 | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | Case 1: % 21.42/3.60 | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | (171) all_257_2 = overflow % 21.42/3.60 | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | BETA: splitting (160) gives: % 21.42/3.60 | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | Case 1: % 21.42/3.60 | | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | | (172) all_128_2 = overflow % 21.42/3.60 | | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | | BETA: splitting (159) gives: % 21.42/3.60 | | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | | Case 1: % 21.42/3.60 | | | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | | | (173) all_65_2 = overflow % 21.42/3.60 | | | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | | | BETA: splitting (166) gives: % 21.42/3.60 | | | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | | | Case 1: % 21.42/3.60 | | | | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | | | | (174) filling = spilling % 21.42/3.60 | | | | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | | | | REDUCE: (10), (174) imply: % 21.42/3.60 | | | | | | | | | | | | | | | | | | | (175) $false % 21.42/3.60 | | | | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | | | | CLOSE: (175) is inconsistent. % 21.42/3.60 | | | | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | | | Case 2: % 21.42/3.60 | | | | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | | | | (176) all_128_2 = tapOn | ? [v0: int] : ? [v1: fluent] % 21.42/3.60 | | | | | | | | | | | | | | | | | | | : ? [v2: int] : ((v2 = 0 & v1 = filling & % 21.42/3.60 | | | | | | | | | | | | | | | | | | | all_128_2 = overflow & waterLevel(v0) = % 21.42/3.60 | | | | | | | | | | | | | | | | | | | filling & holdsAt(filling, all_43_2) = 0) | % 21.42/3.60 | | | | | | | | | | | | | | | | | | | (v2 = 0 & v1 = filling & all_128_2 = tapOff & % 21.42/3.60 | | | | | | | | | | | | | | | | | | | waterLevel(v0) = filling & holdsAt(filling, % 21.42/3.60 | | | | | | | | | | | | | | | | | | | all_43_2) = 0)) % 21.42/3.60 | | | | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | | | | BETA: splitting (176) gives: % 21.42/3.60 | | | | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | | | | Case 1: % 21.42/3.60 | | | | | | | | | | | | | | | | | | | | % 21.42/3.60 | | | | | | | | | | | | | | | | | | | | (177) all_128_2 = tapOn % 21.42/3.60 | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | REF_CLOSE: (8), (20), (160), (177) are inconsistent by % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | sub-proof #2. % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | Case 2: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | (178) ~ (all_128_2 = tapOn) % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | BETA: splitting (165) gives: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | Case 1: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | (179) filling = spilling % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | REDUCE: (10), (179) imply: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | (180) $false % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | CLOSE: (180) is inconsistent. % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | Case 2: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | (181) all_65_2 = tapOn | ? [v0: int] : ? [v1: fluent] % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | : ? [v2: int] : ((v2 = 0 & v1 = filling & % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | all_65_2 = overflow & waterLevel(v0) = filling % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | & holdsAt(filling, all_43_2) = 0) | (v2 = 0 & % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | v1 = filling & all_65_2 = tapOff & % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | waterLevel(v0) = filling & holdsAt(filling, % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | all_43_2) = 0)) % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | BETA: splitting (181) gives: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | Case 1: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | (182) all_65_2 = tapOn % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (173), (182) imply: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | (183) overflow = tapOn % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (171), (183) imply: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | (184) all_257_2 = tapOn % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | REF_CLOSE: (8), (20), (160), (161), (163), (178), (184) are % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | inconsistent by sub-proof #1. % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | Case 2: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | (185) ? [v0: int] : ? [v1: fluent] : ? [v2: int] : % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | ((v2 = 0 & v1 = filling & all_65_2 = overflow & % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | waterLevel(v0) = filling & holdsAt(filling, % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | all_43_2) = 0) | (v2 = 0 & v1 = filling & % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | all_65_2 = tapOff & waterLevel(v0) = filling & % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | holdsAt(filling, all_43_2) = 0)) % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (185) with fresh symbols all_336_0, % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | all_336_1, all_336_2 gives: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | (186) (all_336_0 = 0 & all_336_1 = filling & all_65_2 = % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | overflow & waterLevel(all_336_2) = filling & % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | holdsAt(filling, all_43_2) = 0) | (all_336_0 = 0 % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | & all_336_1 = filling & all_65_2 = tapOff & % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | waterLevel(all_336_2) = filling & % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | holdsAt(filling, all_43_2) = 0) % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (186) gives: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | Case 1: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | (187) all_336_0 = 0 & all_336_1 = filling & all_65_2 = % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | overflow & waterLevel(all_336_2) = filling & % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | holdsAt(filling, all_43_2) = 0 % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (187) implies: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | (188) waterLevel(all_336_2) = filling % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (9) with all_336_2, simplifying with % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | (188) gives: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | (189) $false % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (189) is inconsistent. % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | Case 2: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | (190) all_336_0 = 0 & all_336_1 = filling & all_65_2 = % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | tapOff & waterLevel(all_336_2) = filling & % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | holdsAt(filling, all_43_2) = 0 % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (190) implies: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | (191) waterLevel(all_336_2) = filling % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (9) with all_336_2, simplifying with % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | (191) gives: % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | (192) $false % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (192) is inconsistent. % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | End of split % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | End of split % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | End of split % 21.55/3.60 | | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | | End of split % 21.55/3.60 | | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | End of split % 21.55/3.60 | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | Case 2: % 21.55/3.60 | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | (193) all_43_4 = 0 % 21.55/3.60 | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | REDUCE: (20), (193) imply: % 21.55/3.60 | | | | | | | | | | | | | | | | | | (194) $false % 21.55/3.60 | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | | CLOSE: (194) is inconsistent. % 21.55/3.60 | | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | End of split % 21.55/3.60 | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | Case 2: % 21.55/3.60 | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | (195) all_43_4 = 0 % 21.55/3.60 | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | REDUCE: (20), (195) imply: % 21.55/3.60 | | | | | | | | | | | | | | | | | (196) $false % 21.55/3.60 | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | | CLOSE: (196) is inconsistent. % 21.55/3.60 | | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | End of split % 21.55/3.60 | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | Case 2: % 21.55/3.60 | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | (197) all_43_4 = 0 % 21.55/3.60 | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | REDUCE: (20), (197) imply: % 21.55/3.60 | | | | | | | | | | | | | | | | (198) $false % 21.55/3.60 | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | | CLOSE: (198) is inconsistent. % 21.55/3.60 | | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | | End of split % 21.55/3.60 | | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | | End of split % 21.55/3.60 | | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | | End of split % 21.55/3.60 | | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | | End of split % 21.55/3.60 | | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | | End of split % 21.55/3.60 | | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | End of split % 21.55/3.60 | | | | | | | | | | % 21.55/3.60 | | | | | | | | | End of split % 21.55/3.60 | | | | | | | | | % 21.55/3.60 | | | | | | | | End of split % 21.55/3.60 | | | | | | | | % 21.55/3.60 | | | | | | | Case 2: % 21.55/3.60 | | | | | | | | % 21.55/3.60 | | | | | | | | (199) releasedAt(filling, all_128_5) = all_128_4 & % 21.55/3.60 | | | | | | | | holdsAt(filling, all_128_5) = all_128_3 & % 21.55/3.60 | | | | | | | | at_time($sum(all_43_4, 1)) = all_128_5 & % 21.55/3.60 | | | | | | | | time(all_128_5) & ( ~ (all_128_3 = 0) | all_128_4 = 0) % 21.55/3.60 | | | | | | | | % 21.55/3.60 | | | | | | | | ALPHA: (199) implies: % 21.55/3.60 | | | | | | | | (200) at_time($sum(all_43_4, 1)) = all_128_5 % 21.55/3.60 | | | | | | | | (201) holdsAt(filling, all_128_5) = all_128_3 % 21.55/3.60 | | | | | | | | (202) releasedAt(filling, all_128_5) = all_128_4 % 21.55/3.60 | | | | | | | | (203) ~ (all_128_3 = 0) | all_128_4 = 0 % 21.55/3.60 | | | | | | | | % 21.55/3.60 | | | | | | | | BETA: splitting (76) gives: % 21.55/3.60 | | | | | | | | % 21.55/3.60 | | | | | | | | Case 1: % 21.55/3.60 | | | | | | | | | % 21.55/3.60 | | | | | | | | | (204) all_65_3 = 0 % 21.55/3.60 | | | | | | | | | % 21.55/3.60 | | | | | | | | | REDUCE: (99), (204) imply: % 21.55/3.60 | | | | | | | | | (205) $false % 21.55/3.60 | | | | | | | | | % 21.55/3.60 | | | | | | | | | CLOSE: (205) is inconsistent. % 21.55/3.60 | | | | | | | | | % 21.55/3.60 | | | | | | | | Case 2: % 21.55/3.60 | | | | | | | | | % 21.55/3.60 | | | | | | | | | (206) ? [v0: time] : ? [v1: any] : ? [v2: any] : ? [v3: % 21.55/3.60 | | | | | | | | | event] : ? [v4: int] : ? [v5: int] : % 21.55/3.60 | | | | | | | | | (holdsAt(filling, v0) = v1 & holdsAt(filling, % 21.55/3.60 | | | | | | | | | all_43_3) = v2 & at_time(all_43_4) = v0 & % 21.55/3.60 | | | | | | | | | event(v3) & time(v0) & ( ~ (v1 = 0) | v2 = 0 | (v5 % 21.55/3.60 | | | | | | | | | = 0 & v4 = 0 & happens(v3, v0) = 0 & % 21.55/3.60 | | | | | | | | | terminates(v3, filling, v0) = 0))) % 21.55/3.60 | | | | | | | | | % 21.55/3.60 | | | | | | | | | DELTA: instantiating (206) with fresh symbols all_248_0, % 21.55/3.60 | | | | | | | | | all_248_1, all_248_2, all_248_3, all_248_4, all_248_5 % 21.55/3.60 | | | | | | | | | gives: % 21.55/3.60 | | | | | | | | | (207) holdsAt(filling, all_248_5) = all_248_4 & % 21.55/3.60 | | | | | | | | | holdsAt(filling, all_43_3) = all_248_3 & % 21.55/3.60 | | | | | | | | | at_time(all_43_4) = all_248_5 & event(all_248_2) & % 21.55/3.60 | | | | | | | | | time(all_248_5) & ( ~ (all_248_4 = 0) | all_248_3 = 0 % 21.55/3.60 | | | | | | | | | | (all_248_0 = 0 & all_248_1 = 0 & % 21.55/3.60 | | | | | | | | | happens(all_248_2, all_248_5) = 0 & % 21.55/3.60 | | | | | | | | | terminates(all_248_2, filling, all_248_5) = 0)) % 21.55/3.60 | | | | | | | | | % 21.55/3.60 | | | | | | | | | ALPHA: (207) implies: % 21.55/3.60 | | | | | | | | | (208) holdsAt(filling, all_43_3) = all_248_3 % 21.55/3.60 | | | | | | | | | % 21.55/3.60 | | | | | | | | | BETA: splitting (75) gives: % 21.55/3.60 | | | | | | | | | % 21.55/3.60 | | | | | | | | | Case 1: % 21.55/3.60 | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | (209) all_65_3 = 0 % 21.55/3.60 | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | REDUCE: (99), (209) imply: % 21.55/3.60 | | | | | | | | | | (210) $false % 21.55/3.60 | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | CLOSE: (210) is inconsistent. % 21.55/3.60 | | | | | | | | | | % 21.55/3.60 | | | | | | | | | Case 2: % 21.55/3.60 | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | (211) ? [v0: time] : ? [v1: any] : ? [v2: any] : ? % 21.55/3.60 | | | | | | | | | | [v3: event] : ? [v4: int] : ? [v5: int] : % 21.55/3.60 | | | | | | | | | | (holdsAt(filling, v0) = v1 & holdsAt(filling, % 21.55/3.60 | | | | | | | | | | all_43_3) = v2 & at_time(all_43_4) = v0 & % 21.55/3.60 | | | | | | | | | | event(v3) & time(v0) & ( ~ (v2 = 0) | v1 = 0 | % 21.55/3.60 | | | | | | | | | | (v5 = 0 & v4 = 0 & initiates(v3, filling, v0) = % 21.55/3.60 | | | | | | | | | | 0 & happens(v3, v0) = 0))) % 21.55/3.60 | | | | | | | | | | % 21.55/3.60 | | | | | | | | | | DELTA: instantiating (211) with fresh symbols all_258_0, % 21.55/3.60 | | | | | | | | | | all_258_1, all_258_2, all_258_3, all_258_4, all_258_5 % 21.55/3.60 | | | | | | | | | | gives: % 21.55/3.61 | | | | | | | | | | (212) holdsAt(filling, all_258_5) = all_258_4 & % 21.55/3.61 | | | | | | | | | | holdsAt(filling, all_43_3) = all_258_3 & % 21.55/3.61 | | | | | | | | | | at_time(all_43_4) = all_258_5 & event(all_258_2) & % 21.55/3.61 | | | | | | | | | | time(all_258_5) & ( ~ (all_258_3 = 0) | all_258_4 = % 21.55/3.61 | | | | | | | | | | 0 | (all_258_0 = 0 & all_258_1 = 0 & % 21.55/3.61 | | | | | | | | | | initiates(all_258_2, filling, all_258_5) = 0 & % 21.55/3.61 | | | | | | | | | | happens(all_258_2, all_258_5) = 0)) % 21.55/3.61 | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | ALPHA: (212) implies: % 21.55/3.61 | | | | | | | | | | (213) holdsAt(filling, all_43_3) = all_258_3 % 21.55/3.61 | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | GROUND_INST: instantiating (16) with all_43_3, all_128_5, % 21.55/3.61 | | | | | | | | | | $sum(all_43_4, 1), simplifying with (24), (200) % 21.55/3.61 | | | | | | | | | | gives: % 21.55/3.61 | | | | | | | | | | (214) all_128_5 = all_43_3 % 21.55/3.61 | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | GROUND_INST: instantiating (17) with 0, all_258_3, all_43_3, % 21.55/3.61 | | | | | | | | | | filling, simplifying with (25), (213) gives: % 21.55/3.61 | | | | | | | | | | (215) all_258_3 = 0 % 21.55/3.61 | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | GROUND_INST: instantiating (17) with all_248_3, all_258_3, % 21.55/3.61 | | | | | | | | | | all_43_3, filling, simplifying with (208), (213) % 21.55/3.61 | | | | | | | | | | gives: % 21.55/3.61 | | | | | | | | | | (216) all_258_3 = all_248_3 % 21.55/3.61 | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | COMBINE_EQS: (215), (216) imply: % 21.55/3.61 | | | | | | | | | | (217) all_248_3 = 0 % 21.55/3.61 | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | REDUCE: (202), (214) imply: % 21.55/3.61 | | | | | | | | | | (218) releasedAt(filling, all_43_3) = all_128_4 % 21.55/3.61 | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | REDUCE: (201), (214) imply: % 21.55/3.61 | | | | | | | | | | (219) holdsAt(filling, all_43_3) = all_128_3 % 21.55/3.61 | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | GROUND_INST: instantiating (17) with 0, all_128_3, all_43_3, % 21.55/3.61 | | | | | | | | | | filling, simplifying with (25), (219) gives: % 21.55/3.61 | | | | | | | | | | (220) all_128_3 = 0 % 21.55/3.61 | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | GROUND_INST: instantiating (18) with all_65_3, all_128_4, % 21.55/3.61 | | | | | | | | | | all_43_3, filling, simplifying with (42), (218) % 21.55/3.61 | | | | | | | | | | gives: % 21.55/3.61 | | | | | | | | | | (221) all_128_4 = all_65_3 % 21.55/3.61 | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | BETA: splitting (203) gives: % 21.55/3.61 | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | Case 1: % 21.55/3.61 | | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | | (222) ~ (all_128_3 = 0) % 21.55/3.61 | | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | | REDUCE: (220), (222) imply: % 21.55/3.61 | | | | | | | | | | | (223) $false % 21.55/3.61 | | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | | CLOSE: (223) is inconsistent. % 21.55/3.61 | | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | Case 2: % 21.55/3.61 | | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | | (224) all_128_4 = 0 % 21.55/3.61 | | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | | COMBINE_EQS: (221), (224) imply: % 21.55/3.61 | | | | | | | | | | | (225) all_65_3 = 0 % 21.55/3.61 | | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | | SIMP: (225) implies: % 21.55/3.61 | | | | | | | | | | | (226) all_65_3 = 0 % 21.55/3.61 | | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | | REDUCE: (99), (226) imply: % 21.55/3.61 | | | | | | | | | | | (227) $false % 21.55/3.61 | | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | | CLOSE: (227) is inconsistent. % 21.55/3.61 | | | | | | | | | | | % 21.55/3.61 | | | | | | | | | | End of split % 21.55/3.61 | | | | | | | | | | % 21.55/3.61 | | | | | | | | | End of split % 21.55/3.61 | | | | | | | | | % 21.55/3.61 | | | | | | | | End of split % 21.55/3.61 | | | | | | | | % 21.55/3.61 | | | | | | | End of split % 21.55/3.61 | | | | | | | % 21.55/3.61 | | | | | | End of split % 21.55/3.61 | | | | | | % 21.55/3.61 | | | | | End of split % 21.55/3.61 | | | | | % 21.55/3.61 | | | | End of split % 21.55/3.61 | | | | % 21.55/3.61 | | | End of split % 21.55/3.61 | | | % 21.55/3.61 | | End of split % 21.55/3.61 | | % 21.55/3.61 | End of split % 21.55/3.61 | % 21.55/3.61 End of proof % 21.55/3.61 % 21.55/3.61 Sub-proof #1 shows that the following formulas are inconsistent: % 21.55/3.61 ---------------------------------------------------------------- % 21.55/3.61 (1) ~ (overflow = tapOn) % 21.55/3.61 (2) all_128_2 = overflow | all_128_2 = tapOn % 21.55/3.61 (3) all_257_2 = overflow | all_43_4 = 0 % 21.55/3.61 (4) ~ (all_43_4 = 0) % 21.55/3.61 (5) all_128_2 = overflow | all_43_4 = 0 % 21.55/3.61 (6) all_257_2 = tapOn % 21.55/3.61 (7) ~ (all_128_2 = tapOn) % 21.55/3.61 % 21.55/3.61 Begin of proof % 21.55/3.61 | % 21.55/3.61 | BETA: splitting (2) gives: % 21.55/3.61 | % 21.55/3.61 | Case 1: % 21.55/3.61 | | % 21.55/3.61 | | (8) all_128_2 = overflow % 21.55/3.61 | | % 21.55/3.61 | | BETA: splitting (3) gives: % 21.55/3.61 | | % 21.55/3.61 | | Case 1: % 21.55/3.61 | | | % 21.55/3.61 | | | (9) all_257_2 = overflow % 21.55/3.61 | | | % 21.55/3.61 | | | COMBINE_EQS: (6), (9) imply: % 21.55/3.61 | | | (10) overflow = tapOn % 21.55/3.61 | | | % 21.55/3.61 | | | SIMP: (10) implies: % 21.55/3.61 | | | (11) overflow = tapOn % 21.55/3.61 | | | % 21.55/3.61 | | | COMBINE_EQS: (8), (11) imply: % 21.55/3.61 | | | (12) all_128_2 = tapOn % 21.55/3.61 | | | % 21.55/3.61 | | | REF_CLOSE: (1), (4), (5), (12) are inconsistent by sub-proof #2. % 21.55/3.61 | | | % 21.55/3.61 | | Case 2: % 21.55/3.61 | | | % 21.55/3.61 | | | (13) all_43_4 = 0 % 21.55/3.61 | | | % 21.55/3.61 | | | REDUCE: (4), (13) imply: % 21.55/3.61 | | | (14) $false % 21.55/3.61 | | | % 21.55/3.61 | | | CLOSE: (14) is inconsistent. % 21.55/3.61 | | | % 21.55/3.61 | | End of split % 21.55/3.61 | | % 21.55/3.61 | Case 2: % 21.55/3.61 | | % 21.55/3.61 | | (15) all_128_2 = tapOn % 21.55/3.61 | | % 21.55/3.61 | | REF_CLOSE: (1), (4), (5), (15) are inconsistent by sub-proof #2. % 21.55/3.61 | | % 21.55/3.61 | End of split % 21.55/3.61 | % 21.55/3.61 End of proof % 21.55/3.61 % 21.55/3.61 Sub-proof #2 shows that the following formulas are inconsistent: % 21.55/3.61 ---------------------------------------------------------------- % 21.55/3.61 (1) all_128_2 = overflow | all_43_4 = 0 % 21.55/3.61 (2) all_128_2 = tapOn % 21.55/3.61 (3) ~ (overflow = tapOn) % 21.55/3.61 (4) ~ (all_43_4 = 0) % 21.55/3.61 % 21.55/3.61 Begin of proof % 21.55/3.61 | % 21.55/3.61 | BETA: splitting (1) gives: % 21.55/3.61 | % 21.55/3.61 | Case 1: % 21.55/3.61 | | % 21.55/3.61 | | (5) all_128_2 = overflow % 21.55/3.61 | | % 21.55/3.61 | | COMBINE_EQS: (2), (5) imply: % 21.55/3.61 | | (6) overflow = tapOn % 21.55/3.61 | | % 21.55/3.61 | | REDUCE: (3), (6) imply: % 21.55/3.61 | | (7) $false % 21.55/3.61 | | % 21.55/3.61 | | CLOSE: (7) is inconsistent. % 21.55/3.61 | | % 21.55/3.61 | Case 2: % 21.55/3.61 | | % 21.55/3.61 | | (8) all_43_4 = 0 % 21.55/3.61 | | % 21.55/3.61 | | REDUCE: (4), (8) imply: % 21.55/3.61 | | (9) $false % 21.55/3.61 | | % 21.55/3.61 | | CLOSE: (9) is inconsistent. % 21.55/3.61 | | % 21.55/3.61 | End of split % 21.55/3.61 | % 21.55/3.61 End of proof % 21.55/3.61 % SZS output end Proof for theBenchmark % 21.55/3.61 % 21.55/3.61 2992ms %------------------------------------------------------------------------------