%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : CSR014+1 : TPTP v8.1.0. Bugfixed v3.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n022.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 : 600s % DateTime : Fri Jul 15 02:50:13 EDT 2022 % Result : Theorem 21.98s 6.32s % Output : Proof 27.81s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : CSR014+1 : TPTP v8.1.0. Bugfixed v3.1.0. % 0.07/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.11/0.33 % Computer : n022.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Fri Jun 10 01:32:19 EDT 2022 % 0.11/0.33 % CPUTime : % 0.18/0.56 ____ _ % 0.18/0.56 ___ / __ \_____(_)___ ________ __________ % 0.18/0.56 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.18/0.56 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.18/0.56 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.18/0.56 % 0.18/0.56 A Theorem Prover for First-Order Logic % 0.18/0.56 (ePrincess v.1.0) % 0.18/0.56 % 0.18/0.56 (c) Philipp Rümmer, 2009-2015 % 0.18/0.56 (c) Peter Backeman, 2014-2015 % 0.18/0.56 (contributions by Angelo Brillout, Peter Baumgartner) % 0.18/0.56 Free software under GNU Lesser General Public License (LGPL). % 0.18/0.56 Bug reports to peter@backeman.se % 0.18/0.56 % 0.18/0.56 For more information, visit http://user.uu.se/~petba168/breu/ % 0.18/0.56 % 0.18/0.56 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.64/0.61 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.85/0.97 Prover 0: Preprocessing ... % 3.16/1.39 Prover 0: Warning: ignoring some quantifiers % 3.39/1.41 Prover 0: Constructing countermodel ... % 20.22/5.90 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 20.51/5.99 Prover 1: Preprocessing ... % 21.33/6.15 Prover 1: Constructing countermodel ... % 21.98/6.31 Prover 1: proved (408ms) % 21.98/6.32 Prover 0: stopped % 21.98/6.32 % 21.98/6.32 No countermodel exists, formula is valid % 21.98/6.32 % SZS status Theorem for theBenchmark % 21.98/6.32 % 21.98/6.32 Generating proof ... found it (size 387) % 26.96/7.49 % 26.96/7.49 % SZS output start Proof for theBenchmark % 26.96/7.49 Assumed formulas after preprocessing and simplification: % 26.96/7.49 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ( ~ (v5 = 0) & ~ (v4 = 0) & ~ (v3 = 0) & ~ (v2 = 0) & ~ (tapOff = overflow) & ~ (tapOff = tapOn) & ~ (spilling = filling) & ~ (overflow = tapOn) & waterLevel(n3) = v0 & waterLevel(n0) = v1 & releasedAt(spilling, n0) = v5 & releasedAt(filling, n3) = 0 & releasedAt(filling, n0) = v4 & plus(n2, n2) = n4 & plus(n2, n3) = n5 & plus(n3, n3) = n6 & plus(n1, n2) = n3 & plus(n1, n3) = n4 & plus(n1, n1) = n2 & plus(n0, n2) = n2 & plus(n0, n3) = n3 & plus(n0, n1) = n1 & plus(n0, n0) = n0 & holdsAt(v1, n0) = 0 & holdsAt(spilling, n0) = v3 & holdsAt(filling, n0) = v2 & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v13 = 0 | v12 = 0 | ~ (plus(v7, v10) = v11) | ~ (holdsAt(v9, v11) = v13) | ~ (stoppedIn(v7, v8, v11) = v12) | ~ (happens(v6, v7) = 0) | ? [v14] : ? [v15] : ? [v16] : (trajectory(v8, v7, v9, v10) = v16 & initiates(v6, v8, v7) = v14 & less(n0, v10) = v15 & ( ~ (v16 = 0) | ~ (v15 = 0) | ~ (v14 = 0)))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v13 = 0 | v12 = 0 | ~ (plus(v7, v9) = v11) | ~ (holdsAt(v10, v11) = v13) | ~ (startedIn(v7, v8, v11) = v12) | ~ (happens(v6, v7) = 0) | ? [v14] : ? [v15] : ? [v16] : (antitrajectory(v8, v7, v10, v9) = v16 & less(n0, v9) = v15 & terminates(v6, v8, v7) = v14 & ( ~ (v16 = 0) | ~ (v15 = 0) | ~ (v14 = 0)))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v12 = 0 | ~ (waterLevel(v8) = v11) | ~ (waterLevel(v6) = v10) | ~ (holdsAt(v10, v7) = 0) | ~ (trajectory(filling, v7, v11, v9) = v12) | ? [v13] : ( ~ (v13 = v8) & plus(v6, v9) = v13)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = 0 | ~ (startedIn(v6, v8, v7) = v9) | ~ (initiates(v10, v8, v11) = 0) | ? [v12] : ? [v13] : ? [v14] : (happens(v10, v11) = v12 & less(v11, v7) = v14 & less(v6, v11) = v13 & ( ~ (v14 = 0) | ~ (v13 = 0) | ~ (v12 = 0)))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = 0 | ~ (stoppedIn(v6, v7, v8) = v9) | ~ (terminates(v10, v7, v11) = 0) | ? [v12] : ? [v13] : ? [v14] : (happens(v10, v11) = v12 & less(v11, v8) = v14 & less(v6, v11) = v13 & ( ~ (v14 = 0) | ~ (v13 = 0) | ~ (v12 = 0)))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v7 = v6 | ~ (antitrajectory(v11, v10, v9, v8) = v7) | ~ (antitrajectory(v11, v10, v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v7 = v6 | ~ (trajectory(v11, v10, v9, v8) = v7) | ~ (trajectory(v11, v10, v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | ~ (releasedAt(v8, v9) = v10) | ~ (plus(v7, n1) = v9) | ~ (happens(v6, v7) = 0) | ? [v11] : ( ~ (v11 = 0) & releases(v6, v8, v7) = v11)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | ~ (plus(v7, n1) = v9) | ~ (holdsAt(v8, v9) = v10) | ~ (happens(v6, v7) = 0) | ? [v11] : ( ~ (v11 = 0) & initiates(v6, v8, v7) = v11)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v8 = v7 | ~ (waterLevel(v8) = v10) | ~ (waterLevel(v7) = v9) | ~ (holdsAt(v10, v6) = 0) | ~ (holdsAt(v9, v6) = 0)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v7 = v6 | ~ (releases(v10, v9, v8) = v7) | ~ (releases(v10, v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v7 = v6 | ~ (startedIn(v10, v9, v8) = v7) | ~ (startedIn(v10, v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v7 = v6 | ~ (initiates(v10, v9, v8) = v7) | ~ (initiates(v10, v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v7 = v6 | ~ (stoppedIn(v10, v9, v8) = v7) | ~ (stoppedIn(v10, v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v7 = v6 | ~ (terminates(v10, v9, v8) = v7) | ~ (terminates(v10, v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | ~ (releasedAt(v6, v8) = v9) | ~ (plus(v7, n1) = v8) | ? [v10] : ? [v11] : ? [v12] : ? [v13] : ((v11 = 0 & initiates(v10, v6, v7) = v12 & happens(v10, v7) = 0 & terminates(v10, v6, v7) = v13 & (v13 = 0 | v12 = 0)) | ( ~ (v10 = 0) & releasedAt(v6, v7) = v10))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | ~ (releasedAt(v6, v8) = v9) | ~ (plus(v7, n1) = v8) | ? [v10] : ? [v11] : ? [v12] : ((v12 = 0 & v11 = 0 & initiates(v10, v6, v7) = 0 & happens(v10, v7) = 0) | (holdsAt(v6, v8) = v11 & holdsAt(v6, v7) = v10 & ( ~ (v11 = 0) | v10 = 0)))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | ~ (releasedAt(v6, v8) = v9) | ~ (plus(v7, n1) = v8) | ? [v10] : ? [v11] : ? [v12] : ((v12 = 0 & v11 = 0 & happens(v10, v7) = 0 & terminates(v10, v6, v7) = 0) | (holdsAt(v6, v8) = v11 & holdsAt(v6, v7) = v10 & ( ~ (v10 = 0) | v11 = 0)))) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (waterLevel(v9) = v6) | ~ (releases(tapOn, v6, v7) = v8)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (waterLevel(v9) = v6) | ~ (holdsAt(v6, v7) = 0) | ~ (initiates(tapOff, v6, v7) = v8)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (waterLevel(v9) = v6) | ~ (holdsAt(v6, v7) = 0) | ~ (initiates(overflow, v6, v7) = v8)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (less_or_equal(v9, v8) = v7) | ~ (less_or_equal(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (releasedAt(v9, v8) = v7) | ~ (releasedAt(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (plus(v9, v8) = v7) | ~ (plus(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (holdsAt(v9, v8) = v7) | ~ (holdsAt(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (happens(v9, v8) = v7) | ~ (happens(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (less(v9, v8) = v7) | ~ (less(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ (releasedAt(v8, v9) = 0) | ~ (plus(v7, n1) = v9) | ~ (happens(v6, v7) = 0) | ? [v10] : ? [v11] : ( ~ (v11 = 0) & ~ (v10 = 0) & initiates(v6, v8, v7) = v10 & terminates(v6, v8, v7) = v11)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ (plus(v7, n1) = v9) | ~ (holdsAt(v8, v9) = 0) | ~ (happens(v6, v7) = 0) | ? [v10] : ( ~ (v10 = 0) & terminates(v6, v8, v7) = v10)) & ! [v6] : ! [v7] : ! [v8] : (v8 = v7 | ~ (waterLevel(v6) = v8) | ~ (waterLevel(v6) = v7)) & ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | v7 = v6 | ~ (less(v6, v7) = v8) | less(v7, v6) = 0) & ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | ~ (less_or_equal(v6, v7) = v8) | ? [v9] : ( ~ (v9 = 0) & less(v6, v7) = v9)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (waterLevel(v8) = v7) | ~ (waterLevel(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (waterLevel(v7) = v8) | ~ (waterLevel(v6) = v8)) & ! [v6] : ! [v7] : ! [v8] : (v7 = spilling | v7 = filling | ~ (initiates(v6, v7, v8) = 0) | ? [v9] : ? [v10] : ? [v11] : ((v11 = 0 & v10 = v7 & v6 = tapOff & waterLevel(v9) = v7 & holdsAt(v7, v8) = 0) | (v11 = 0 & v10 = v7 & v6 = overflow & waterLevel(v9) = v7 & holdsAt(v7, v8) = 0))) & ! [v6] : ! [v7] : ! [v8] : (v7 = spilling | v6 = tapOn | ~ (initiates(v6, v7, v8) = 0) | ? [v9] : ? [v10] : ? [v11] : ((v11 = 0 & v10 = v7 & v6 = tapOff & waterLevel(v9) = v7 & holdsAt(v7, v8) = 0) | (v11 = 0 & v10 = v7 & v6 = overflow & waterLevel(v9) = v7 & holdsAt(v7, v8) = 0))) & ! [v6] : ! [v7] : ! [v8] : (v7 = filling | v6 = overflow | ~ (initiates(v6, v7, v8) = 0) | ? [v9] : (v6 = tapOff & waterLevel(v9) = v7 & holdsAt(v7, v8) = 0)) & ! [v6] : ! [v7] : ! [v8] : (v7 = filling | ~ (terminates(v6, v7, v8) = 0)) & ! [v6] : ! [v7] : ! [v8] : (v6 = tapOff | v6 = overflow | ~ (terminates(v6, v7, v8) = 0)) & ! [v6] : ! [v7] : ! [v8] : (v6 = overflow | v6 = tapOn | ~ (initiates(v6, v7, v8) = 0) | ? [v9] : (v6 = tapOff & waterLevel(v9) = v7 & holdsAt(v7, v8) = 0)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (releases(v6, v7, v8) = 0) | ? [v9] : (v6 = tapOn & waterLevel(v9) = v7)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (releasedAt(v6, v8) = 0) | ~ (plus(v7, n1) = v8) | ? [v9] : ? [v10] : ? [v11] : ((v11 = 0 & v10 = 0 & releases(v9, v6, v7) = 0 & happens(v9, v7) = 0) | (v9 = 0 & releasedAt(v6, v7) = 0))) & ! [v6] : ! [v7] : ! [v8] : ( ~ (plus(v6, v7) = v8) | plus(v7, v6) = v8) & ! [v6] : ! [v7] : ! [v8] : ( ~ (startedIn(v6, v8, v7) = 0) | ? [v9] : ? [v10] : (initiates(v9, v8, v10) = 0 & happens(v9, v10) = 0 & less(v10, v7) = 0 & less(v6, v10) = 0)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (stoppedIn(v6, v7, v8) = 0) | ? [v9] : ? [v10] : (happens(v9, v10) = 0 & less(v10, v8) = 0 & less(v6, v10) = 0 & terminates(v9, v7, v10) = 0)) & ! [v6] : ! [v7] : (v7 = v6 | ~ (less_or_equal(v6, v7) = 0) | less(v6, v7) = 0) & ! [v6] : ! [v7] : (v7 = n0 | v6 = overflow | ~ (happens(v6, v7) = 0)) & ! [v6] : ! [v7] : (v7 = n0 | ~ (happens(v6, v7) = 0) | (holdsAt(v0, v7) = 0 & holdsAt(filling, v7) = 0)) & ! [v6] : ! [v7] : (v7 = 0 | ~ (less_or_equal(v6, v6) = v7)) & ! [v6] : ! [v7] : (v7 = 0 | ~ (less_or_equal(v6, n8) = v7) | ? [v8] : ( ~ (v8 = 0) & less(v6, n9) = v8)) & ! [v6] : ! [v7] : (v7 = 0 | ~ (less_or_equal(v6, n7) = v7) | ? [v8] : ( ~ (v8 = 0) & less(v6, n8) = v8)) & ! [v6] : ! [v7] : (v7 = 0 | ~ (less_or_equal(v6, n6) = v7) | ? [v8] : ( ~ (v8 = 0) & less(v6, n7) = v8)) & ! [v6] : ! [v7] : (v7 = 0 | ~ (less_or_equal(v6, n5) = v7) | ? [v8] : ( ~ (v8 = 0) & less(v6, n6) = v8)) & ! [v6] : ! [v7] : (v7 = 0 | ~ (less_or_equal(v6, n4) = v7) | ? [v8] : ( ~ (v8 = 0) & less(v6, n5) = v8)) & ! [v6] : ! [v7] : (v7 = 0 | ~ (less_or_equal(v6, n2) = v7) | ? [v8] : ( ~ (v8 = 0) & less(v6, n3) = v8)) & ! [v6] : ! [v7] : (v7 = 0 | ~ (less_or_equal(v6, n3) = v7) | ? [v8] : ( ~ (v8 = 0) & less(v6, n4) = v8)) & ! [v6] : ! [v7] : (v7 = 0 | ~ (less_or_equal(v6, n1) = v7) | ? [v8] : ( ~ (v8 = 0) & less(v6, n2) = v8)) & ! [v6] : ! [v7] : (v7 = 0 | ~ (less_or_equal(v6, n0) = v7) | ? [v8] : ( ~ (v8 = 0) & less(v6, n1) = v8)) & ! [v6] : ! [v7] : (v7 = 0 | ~ (initiates(overflow, spilling, v6) = v7)) & ! [v6] : ! [v7] : (v7 = 0 | ~ (initiates(tapOn, filling, v6) = v7)) & ! [v6] : ! [v7] : (v7 = 0 | ~ (happens(overflow, v6) = v7) | ? [v8] : ? [v9] : (holdsAt(v0, v6) = v8 & holdsAt(filling, v6) = v9 & ( ~ (v9 = 0) | ~ (v8 = 0)))) & ! [v6] : ! [v7] : (v7 = 0 | ~ (terminates(tapOff, filling, v6) = v7)) & ! [v6] : ! [v7] : (v7 = 0 | ~ (terminates(overflow, filling, v6) = v7)) & ! [v6] : ! [v7] : (v6 = overflow | v6 = tapOn | ~ (happens(v6, v7) = 0)) & ! [v6] : ! [v7] : (v6 = tapOn | ~ (happens(v6, v7) = 0) | (holdsAt(v0, v7) = 0 & holdsAt(filling, v7) = 0)) & ! [v6] : ! [v7] : ( ~ (waterLevel(v6) = v7) | ? [v8] : ( ~ (v8 = 0) & releasedAt(v7, n0) = v8)) & ! [v6] : ! [v7] : ( ~ (less(v6, v7) = 0) | ? [v8] : ( ~ (v8 = 0) & less(v7, v6) = v8)) & ! [v6] : (v6 = 0 | ~ (happens(tapOn, n0) = v6)) & ! [v6] : ( ~ (less_or_equal(v6, n8) = 0) | less(v6, n9) = 0) & ! [v6] : ( ~ (less_or_equal(v6, n7) = 0) | less(v6, n8) = 0) & ! [v6] : ( ~ (less_or_equal(v6, n6) = 0) | less(v6, n7) = 0) & ! [v6] : ( ~ (less_or_equal(v6, n5) = 0) | less(v6, n6) = 0) & ! [v6] : ( ~ (less_or_equal(v6, n4) = 0) | less(v6, n5) = 0) & ! [v6] : ( ~ (less_or_equal(v6, n2) = 0) | less(v6, n3) = 0) & ! [v6] : ( ~ (less_or_equal(v6, n3) = 0) | less(v6, n4) = 0) & ! [v6] : ( ~ (less_or_equal(v6, n1) = 0) | less(v6, n2) = 0) & ! [v6] : ( ~ (less_or_equal(v6, n0) = 0) | less(v6, n1) = 0) & ! [v6] : ~ (waterLevel(v6) = spilling) & ! [v6] : ~ (waterLevel(v6) = filling) & ! [v6] : ~ (less(v6, v6) = 0) & ! [v6] : ~ (less(v6, n0) = 0)) % 27.34/7.55 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5 yields: % 27.34/7.55 | (1) ~ (all_0_0_0 = 0) & ~ (all_0_1_1 = 0) & ~ (all_0_2_2 = 0) & ~ (all_0_3_3 = 0) & ~ (tapOff = overflow) & ~ (tapOff = tapOn) & ~ (spilling = filling) & ~ (overflow = tapOn) & waterLevel(n3) = all_0_5_5 & waterLevel(n0) = all_0_4_4 & releasedAt(spilling, n0) = all_0_0_0 & releasedAt(filling, n3) = 0 & releasedAt(filling, n0) = all_0_1_1 & plus(n2, n2) = n4 & plus(n2, n3) = n5 & plus(n3, n3) = n6 & plus(n1, n2) = n3 & plus(n1, n3) = n4 & plus(n1, n1) = n2 & plus(n0, n2) = n2 & plus(n0, n3) = n3 & plus(n0, n1) = n1 & plus(n0, n0) = n0 & holdsAt(all_0_4_4, n0) = 0 & holdsAt(spilling, n0) = all_0_2_2 & holdsAt(filling, n0) = all_0_3_3 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v6 = 0 | ~ (plus(v1, v4) = v5) | ~ (holdsAt(v3, v5) = v7) | ~ (stoppedIn(v1, v2, v5) = v6) | ~ (happens(v0, v1) = 0) | ? [v8] : ? [v9] : ? [v10] : (trajectory(v2, v1, v3, v4) = v10 & initiates(v0, v2, v1) = v8 & less(n0, v4) = v9 & ( ~ (v10 = 0) | ~ (v9 = 0) | ~ (v8 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v6 = 0 | ~ (plus(v1, v3) = v5) | ~ (holdsAt(v4, v5) = v7) | ~ (startedIn(v1, v2, v5) = v6) | ~ (happens(v0, v1) = 0) | ? [v8] : ? [v9] : ? [v10] : (antitrajectory(v2, v1, v4, v3) = v10 & less(n0, v3) = v9 & terminates(v0, v2, v1) = v8 & ( ~ (v10 = 0) | ~ (v9 = 0) | ~ (v8 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (waterLevel(v2) = v5) | ~ (waterLevel(v0) = v4) | ~ (holdsAt(v4, v1) = 0) | ~ (trajectory(filling, v1, v5, v3) = v6) | ? [v7] : ( ~ (v7 = v2) & plus(v0, v3) = v7)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = 0 | ~ (startedIn(v0, v2, v1) = v3) | ~ (initiates(v4, v2, v5) = 0) | ? [v6] : ? [v7] : ? [v8] : (happens(v4, v5) = v6 & less(v5, v1) = v8 & less(v0, v5) = v7 & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = 0 | ~ (stoppedIn(v0, v1, v2) = v3) | ~ (terminates(v4, v1, v5) = 0) | ? [v6] : ? [v7] : ? [v8] : (happens(v4, v5) = v6 & less(v5, v2) = v8 & less(v0, v5) = v7 & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v1 = v0 | ~ (antitrajectory(v5, v4, v3, v2) = v1) | ~ (antitrajectory(v5, v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v1 = v0 | ~ (trajectory(v5, v4, v3, v2) = v1) | ~ (trajectory(v5, v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (releasedAt(v2, v3) = v4) | ~ (plus(v1, n1) = v3) | ~ (happens(v0, v1) = 0) | ? [v5] : ( ~ (v5 = 0) & releases(v0, v2, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (plus(v1, n1) = v3) | ~ (holdsAt(v2, v3) = v4) | ~ (happens(v0, v1) = 0) | ? [v5] : ( ~ (v5 = 0) & initiates(v0, v2, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (waterLevel(v2) = v4) | ~ (waterLevel(v1) = v3) | ~ (holdsAt(v4, v0) = 0) | ~ (holdsAt(v3, v0) = 0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (releases(v4, v3, v2) = v1) | ~ (releases(v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (startedIn(v4, v3, v2) = v1) | ~ (startedIn(v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (initiates(v4, v3, v2) = v1) | ~ (initiates(v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (stoppedIn(v4, v3, v2) = v1) | ~ (stoppedIn(v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (terminates(v4, v3, v2) = v1) | ~ (terminates(v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (releasedAt(v0, v2) = v3) | ~ (plus(v1, n1) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ((v5 = 0 & initiates(v4, v0, v1) = v6 & happens(v4, v1) = 0 & terminates(v4, v0, v1) = v7 & (v7 = 0 | v6 = 0)) | ( ~ (v4 = 0) & releasedAt(v0, v1) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (releasedAt(v0, v2) = v3) | ~ (plus(v1, n1) = v2) | ? [v4] : ? [v5] : ? [v6] : ((v6 = 0 & v5 = 0 & initiates(v4, v0, v1) = 0 & happens(v4, v1) = 0) | (holdsAt(v0, v2) = v5 & holdsAt(v0, v1) = v4 & ( ~ (v5 = 0) | v4 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (releasedAt(v0, v2) = v3) | ~ (plus(v1, n1) = v2) | ? [v4] : ? [v5] : ? [v6] : ((v6 = 0 & v5 = 0 & happens(v4, v1) = 0 & terminates(v4, v0, v1) = 0) | (holdsAt(v0, v2) = v5 & holdsAt(v0, v1) = v4 & ( ~ (v4 = 0) | v5 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (waterLevel(v3) = v0) | ~ (releases(tapOn, v0, v1) = v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (waterLevel(v3) = v0) | ~ (holdsAt(v0, v1) = 0) | ~ (initiates(tapOff, v0, v1) = v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (waterLevel(v3) = v0) | ~ (holdsAt(v0, v1) = 0) | ~ (initiates(overflow, v0, v1) = v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (less_or_equal(v3, v2) = v1) | ~ (less_or_equal(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (releasedAt(v3, v2) = v1) | ~ (releasedAt(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (plus(v3, v2) = v1) | ~ (plus(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (holdsAt(v3, v2) = v1) | ~ (holdsAt(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (happens(v3, v2) = v1) | ~ (happens(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (less(v3, v2) = v1) | ~ (less(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (releasedAt(v2, v3) = 0) | ~ (plus(v1, n1) = v3) | ~ (happens(v0, v1) = 0) | ? [v4] : ? [v5] : ( ~ (v5 = 0) & ~ (v4 = 0) & initiates(v0, v2, v1) = v4 & terminates(v0, v2, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (plus(v1, n1) = v3) | ~ (holdsAt(v2, v3) = 0) | ~ (happens(v0, v1) = 0) | ? [v4] : ( ~ (v4 = 0) & terminates(v0, v2, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (waterLevel(v0) = v2) | ~ (waterLevel(v0) = v1)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | v1 = v0 | ~ (less(v0, v1) = v2) | less(v1, v0) = 0) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (less_or_equal(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & less(v0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (waterLevel(v2) = v1) | ~ (waterLevel(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (waterLevel(v1) = v2) | ~ (waterLevel(v0) = v2)) & ! [v0] : ! [v1] : ! [v2] : (v1 = spilling | v1 = filling | ~ (initiates(v0, v1, v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v5 = 0 & v4 = v1 & v0 = tapOff & waterLevel(v3) = v1 & holdsAt(v1, v2) = 0) | (v5 = 0 & v4 = v1 & v0 = overflow & waterLevel(v3) = v1 & holdsAt(v1, v2) = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = spilling | v0 = tapOn | ~ (initiates(v0, v1, v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v5 = 0 & v4 = v1 & v0 = tapOff & waterLevel(v3) = v1 & holdsAt(v1, v2) = 0) | (v5 = 0 & v4 = v1 & v0 = overflow & waterLevel(v3) = v1 & holdsAt(v1, v2) = 0))) & ! [v0] : ! [v1] : ! [v2] : (v1 = filling | v0 = overflow | ~ (initiates(v0, v1, v2) = 0) | ? [v3] : (v0 = tapOff & waterLevel(v3) = v1 & holdsAt(v1, v2) = 0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = filling | ~ (terminates(v0, v1, v2) = 0)) & ! [v0] : ! [v1] : ! [v2] : (v0 = tapOff | v0 = overflow | ~ (terminates(v0, v1, v2) = 0)) & ! [v0] : ! [v1] : ! [v2] : (v0 = overflow | v0 = tapOn | ~ (initiates(v0, v1, v2) = 0) | ? [v3] : (v0 = tapOff & waterLevel(v3) = v1 & holdsAt(v1, v2) = 0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (releases(v0, v1, v2) = 0) | ? [v3] : (v0 = tapOn & waterLevel(v3) = v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (releasedAt(v0, v2) = 0) | ~ (plus(v1, n1) = v2) | ? [v3] : ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & releases(v3, v0, v1) = 0 & happens(v3, v1) = 0) | (v3 = 0 & releasedAt(v0, v1) = 0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (plus(v0, v1) = v2) | plus(v1, v0) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (startedIn(v0, v2, v1) = 0) | ? [v3] : ? [v4] : (initiates(v3, v2, v4) = 0 & happens(v3, v4) = 0 & less(v4, v1) = 0 & less(v0, v4) = 0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (stoppedIn(v0, v1, v2) = 0) | ? [v3] : ? [v4] : (happens(v3, v4) = 0 & less(v4, v2) = 0 & less(v0, v4) = 0 & terminates(v3, v1, v4) = 0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (less_or_equal(v0, v1) = 0) | less(v0, v1) = 0) & ! [v0] : ! [v1] : (v1 = n0 | v0 = overflow | ~ (happens(v0, v1) = 0)) & ! [v0] : ! [v1] : (v1 = n0 | ~ (happens(v0, v1) = 0) | (holdsAt(all_0_5_5, v1) = 0 & holdsAt(filling, v1) = 0)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, v0) = v1)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n8) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n9) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n7) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n8) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n6) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n7) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n5) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n6) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n4) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n5) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n2) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n3) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n3) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n4) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n1) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n2) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n0) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n1) = v2)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (initiates(overflow, spilling, v0) = v1)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (initiates(tapOn, filling, v0) = v1)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (happens(overflow, v0) = v1) | ? [v2] : ? [v3] : (holdsAt(all_0_5_5, v0) = v2 & holdsAt(filling, v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) & ! [v0] : ! [v1] : (v1 = 0 | ~ (terminates(tapOff, filling, v0) = v1)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (terminates(overflow, filling, v0) = v1)) & ! [v0] : ! [v1] : (v0 = overflow | v0 = tapOn | ~ (happens(v0, v1) = 0)) & ! [v0] : ! [v1] : (v0 = tapOn | ~ (happens(v0, v1) = 0) | (holdsAt(all_0_5_5, v1) = 0 & holdsAt(filling, v1) = 0)) & ! [v0] : ! [v1] : ( ~ (waterLevel(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & releasedAt(v1, n0) = v2)) & ! [v0] : ! [v1] : ( ~ (less(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & less(v1, v0) = v2)) & ! [v0] : (v0 = 0 | ~ (happens(tapOn, n0) = v0)) & ! [v0] : ( ~ (less_or_equal(v0, n8) = 0) | less(v0, n9) = 0) & ! [v0] : ( ~ (less_or_equal(v0, n7) = 0) | less(v0, n8) = 0) & ! [v0] : ( ~ (less_or_equal(v0, n6) = 0) | less(v0, n7) = 0) & ! [v0] : ( ~ (less_or_equal(v0, n5) = 0) | less(v0, n6) = 0) & ! [v0] : ( ~ (less_or_equal(v0, n4) = 0) | less(v0, n5) = 0) & ! [v0] : ( ~ (less_or_equal(v0, n2) = 0) | less(v0, n3) = 0) & ! [v0] : ( ~ (less_or_equal(v0, n3) = 0) | less(v0, n4) = 0) & ! [v0] : ( ~ (less_or_equal(v0, n1) = 0) | less(v0, n2) = 0) & ! [v0] : ( ~ (less_or_equal(v0, n0) = 0) | less(v0, n1) = 0) & ! [v0] : ~ (waterLevel(v0) = spilling) & ! [v0] : ~ (waterLevel(v0) = filling) & ! [v0] : ~ (less(v0, v0) = 0) & ! [v0] : ~ (less(v0, n0) = 0) % 27.34/7.57 | % 27.34/7.57 | Applying alpha-rule on (1) yields: % 27.34/7.57 | (2) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (holdsAt(v3, v2) = v1) | ~ (holdsAt(v3, v2) = v0)) % 27.34/7.57 | (3) plus(n0, n0) = n0 % 27.34/7.57 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (terminates(v4, v3, v2) = v1) | ~ (terminates(v4, v3, v2) = v0)) % 27.34/7.57 | (5) ~ (all_0_2_2 = 0) % 27.34/7.57 | (6) ! [v0] : ( ~ (less_or_equal(v0, n2) = 0) | less(v0, n3) = 0) % 27.34/7.57 | (7) plus(n0, n3) = n3 % 27.34/7.57 | (8) releasedAt(filling, n0) = all_0_1_1 % 27.34/7.57 | (9) ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n0) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n1) = v2)) % 27.34/7.57 | (10) ! [v0] : ! [v1] : ! [v2] : (v1 = spilling | v0 = tapOn | ~ (initiates(v0, v1, v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v5 = 0 & v4 = v1 & v0 = tapOff & waterLevel(v3) = v1 & holdsAt(v1, v2) = 0) | (v5 = 0 & v4 = v1 & v0 = overflow & waterLevel(v3) = v1 & holdsAt(v1, v2) = 0))) % 27.34/7.57 | (11) ! [v0] : ! [v1] : (v1 = 0 | ~ (initiates(tapOn, filling, v0) = v1)) % 27.34/7.57 | (12) ! [v0] : ! [v1] : ! [v2] : (v0 = tapOff | v0 = overflow | ~ (terminates(v0, v1, v2) = 0)) % 27.34/7.57 | (13) ! [v0] : ! [v1] : ! [v2] : ( ~ (plus(v0, v1) = v2) | plus(v1, v0) = v2) % 27.34/7.57 | (14) ! [v0] : ( ~ (less_or_equal(v0, n8) = 0) | less(v0, n9) = 0) % 27.34/7.57 | (15) ! [v0] : (v0 = 0 | ~ (happens(tapOn, n0) = v0)) % 27.34/7.57 | (16) ! [v0] : ! [v1] : ( ~ (less(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & less(v1, v0) = v2)) % 27.34/7.57 | (17) ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n5) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n6) = v2)) % 27.34/7.57 | (18) ! [v0] : ( ~ (less_or_equal(v0, n7) = 0) | less(v0, n8) = 0) % 27.34/7.57 | (19) plus(n1, n3) = n4 % 27.34/7.57 | (20) ! [v0] : ~ (waterLevel(v0) = filling) % 27.34/7.57 | (21) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (less_or_equal(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & less(v0, v1) = v3)) % 27.34/7.57 | (22) ! [v0] : ! [v1] : ! [v2] : ( ~ (startedIn(v0, v2, v1) = 0) | ? [v3] : ? [v4] : (initiates(v3, v2, v4) = 0 & happens(v3, v4) = 0 & less(v4, v1) = 0 & less(v0, v4) = 0)) % 27.34/7.57 | (23) ! [v0] : ! [v1] : ! [v2] : (v0 = overflow | v0 = tapOn | ~ (initiates(v0, v1, v2) = 0) | ? [v3] : (v0 = tapOff & waterLevel(v3) = v1 & holdsAt(v1, v2) = 0)) % 27.34/7.57 | (24) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (initiates(v4, v3, v2) = v1) | ~ (initiates(v4, v3, v2) = v0)) % 27.34/7.57 | (25) plus(n1, n2) = n3 % 27.34/7.57 | (26) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (less(v3, v2) = v1) | ~ (less(v3, v2) = v0)) % 27.34/7.57 | (27) plus(n2, n3) = n5 % 27.34/7.57 | (28) ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n6) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n7) = v2)) % 27.34/7.57 | (29) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v1 = v0 | ~ (antitrajectory(v5, v4, v3, v2) = v1) | ~ (antitrajectory(v5, v4, v3, v2) = v0)) % 27.34/7.57 | (30) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (releasedAt(v0, v2) = v3) | ~ (plus(v1, n1) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ((v5 = 0 & initiates(v4, v0, v1) = v6 & happens(v4, v1) = 0 & terminates(v4, v0, v1) = v7 & (v7 = 0 | v6 = 0)) | ( ~ (v4 = 0) & releasedAt(v0, v1) = v4))) % 27.34/7.57 | (31) holdsAt(spilling, n0) = all_0_2_2 % 27.34/7.57 | (32) ! [v0] : ! [v1] : (v1 = 0 | ~ (terminates(overflow, filling, v0) = v1)) % 27.34/7.57 | (33) ! [v0] : ! [v1] : (v1 = n0 | v0 = overflow | ~ (happens(v0, v1) = 0)) % 27.34/7.58 | (34) plus(n0, n2) = n2 % 27.34/7.58 | (35) ! [v0] : ! [v1] : (v1 = n0 | ~ (happens(v0, v1) = 0) | (holdsAt(all_0_5_5, v1) = 0 & holdsAt(filling, v1) = 0)) % 27.34/7.58 | (36) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (waterLevel(v1) = v2) | ~ (waterLevel(v0) = v2)) % 27.34/7.58 | (37) ~ (spilling = filling) % 27.34/7.58 | (38) ! [v0] : ! [v1] : (v1 = v0 | ~ (less_or_equal(v0, v1) = 0) | less(v0, v1) = 0) % 27.34/7.58 | (39) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (releasedAt(v0, v2) = v3) | ~ (plus(v1, n1) = v2) | ? [v4] : ? [v5] : ? [v6] : ((v6 = 0 & v5 = 0 & initiates(v4, v0, v1) = 0 & happens(v4, v1) = 0) | (holdsAt(v0, v2) = v5 & holdsAt(v0, v1) = v4 & ( ~ (v5 = 0) | v4 = 0)))) % 27.34/7.58 | (40) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (releases(v4, v3, v2) = v1) | ~ (releases(v4, v3, v2) = v0)) % 27.34/7.58 | (41) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (plus(v1, n1) = v3) | ~ (holdsAt(v2, v3) = v4) | ~ (happens(v0, v1) = 0) | ? [v5] : ( ~ (v5 = 0) & initiates(v0, v2, v1) = v5)) % 27.34/7.58 | (42) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v1 = v0 | ~ (trajectory(v5, v4, v3, v2) = v1) | ~ (trajectory(v5, v4, v3, v2) = v0)) % 27.34/7.58 | (43) ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n2) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n3) = v2)) % 27.34/7.58 | (44) ! [v0] : ! [v1] : (v0 = overflow | v0 = tapOn | ~ (happens(v0, v1) = 0)) % 27.34/7.58 | (45) ! [v0] : ! [v1] : ! [v2] : ( ~ (releases(v0, v1, v2) = 0) | ? [v3] : (v0 = tapOn & waterLevel(v3) = v1)) % 27.34/7.58 | (46) ! [v0] : ( ~ (less_or_equal(v0, n1) = 0) | less(v0, n2) = 0) % 27.34/7.58 | (47) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (waterLevel(v2) = v4) | ~ (waterLevel(v1) = v3) | ~ (holdsAt(v4, v0) = 0) | ~ (holdsAt(v3, v0) = 0)) % 27.34/7.58 | (48) waterLevel(n0) = all_0_4_4 % 27.34/7.58 | (49) ~ (overflow = tapOn) % 27.34/7.58 | (50) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = 0 | ~ (startedIn(v0, v2, v1) = v3) | ~ (initiates(v4, v2, v5) = 0) | ? [v6] : ? [v7] : ? [v8] : (happens(v4, v5) = v6 & less(v5, v1) = v8 & less(v0, v5) = v7 & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0)))) % 27.34/7.58 | (51) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (releasedAt(v2, v3) = v4) | ~ (plus(v1, n1) = v3) | ~ (happens(v0, v1) = 0) | ? [v5] : ( ~ (v5 = 0) & releases(v0, v2, v1) = v5)) % 27.34/7.58 | (52) ! [v0] : ~ (less(v0, n0) = 0) % 27.34/7.58 | (53) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | v1 = v0 | ~ (less(v0, v1) = v2) | less(v1, v0) = 0) % 27.34/7.58 | (54) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (startedIn(v4, v3, v2) = v1) | ~ (startedIn(v4, v3, v2) = v0)) % 27.34/7.58 | (55) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (plus(v3, v2) = v1) | ~ (plus(v3, v2) = v0)) % 27.34/7.58 | (56) ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n1) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n2) = v2)) % 27.34/7.58 | (57) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v3 = 0 | ~ (stoppedIn(v0, v1, v2) = v3) | ~ (terminates(v4, v1, v5) = 0) | ? [v6] : ? [v7] : ? [v8] : (happens(v4, v5) = v6 & less(v5, v2) = v8 & less(v0, v5) = v7 & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0)))) % 27.34/7.58 | (58) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v6 = 0 | ~ (plus(v1, v3) = v5) | ~ (holdsAt(v4, v5) = v7) | ~ (startedIn(v1, v2, v5) = v6) | ~ (happens(v0, v1) = 0) | ? [v8] : ? [v9] : ? [v10] : (antitrajectory(v2, v1, v4, v3) = v10 & less(n0, v3) = v9 & terminates(v0, v2, v1) = v8 & ( ~ (v10 = 0) | ~ (v9 = 0) | ~ (v8 = 0)))) % 27.34/7.58 | (59) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (stoppedIn(v4, v3, v2) = v1) | ~ (stoppedIn(v4, v3, v2) = v0)) % 27.34/7.58 | (60) waterLevel(n3) = all_0_5_5 % 27.34/7.58 | (61) ! [v0] : ! [v1] : ! [v2] : (v1 = filling | v0 = overflow | ~ (initiates(v0, v1, v2) = 0) | ? [v3] : (v0 = tapOff & waterLevel(v3) = v1 & holdsAt(v1, v2) = 0)) % 27.34/7.58 | (62) ~ (all_0_3_3 = 0) % 27.34/7.58 | (63) releasedAt(spilling, n0) = all_0_0_0 % 27.34/7.58 | (64) ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n4) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n5) = v2)) % 27.34/7.58 | (65) ! [v0] : ~ (less(v0, v0) = 0) % 27.34/7.58 | (66) ! [v0] : ! [v1] : ( ~ (waterLevel(v0) = v1) | ? [v2] : ( ~ (v2 = 0) & releasedAt(v1, n0) = v2)) % 27.34/7.58 | (67) ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, v0) = v1)) % 27.34/7.58 | (68) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (waterLevel(v2) = v5) | ~ (waterLevel(v0) = v4) | ~ (holdsAt(v4, v1) = 0) | ~ (trajectory(filling, v1, v5, v3) = v6) | ? [v7] : ( ~ (v7 = v2) & plus(v0, v3) = v7)) % 27.34/7.58 | (69) ~ (all_0_1_1 = 0) % 27.34/7.58 | (70) ! [v0] : ! [v1] : ! [v2] : ( ~ (releasedAt(v0, v2) = 0) | ~ (plus(v1, n1) = v2) | ? [v3] : ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & releases(v3, v0, v1) = 0 & happens(v3, v1) = 0) | (v3 = 0 & releasedAt(v0, v1) = 0))) % 27.34/7.58 | (71) ~ (all_0_0_0 = 0) % 27.34/7.59 | (72) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (waterLevel(v2) = v1) | ~ (waterLevel(v2) = v0)) % 27.34/7.59 | (73) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | v6 = 0 | ~ (plus(v1, v4) = v5) | ~ (holdsAt(v3, v5) = v7) | ~ (stoppedIn(v1, v2, v5) = v6) | ~ (happens(v0, v1) = 0) | ? [v8] : ? [v9] : ? [v10] : (trajectory(v2, v1, v3, v4) = v10 & initiates(v0, v2, v1) = v8 & less(n0, v4) = v9 & ( ~ (v10 = 0) | ~ (v9 = 0) | ~ (v8 = 0)))) % 27.34/7.59 | (74) ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n7) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n8) = v2)) % 27.34/7.59 | (75) ! [v0] : ( ~ (less_or_equal(v0, n3) = 0) | less(v0, n4) = 0) % 27.34/7.59 | (76) plus(n2, n2) = n4 % 27.34/7.59 | (77) ! [v0] : ! [v1] : ! [v2] : (v1 = filling | ~ (terminates(v0, v1, v2) = 0)) % 27.34/7.59 | (78) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (releasedAt(v0, v2) = v3) | ~ (plus(v1, n1) = v2) | ? [v4] : ? [v5] : ? [v6] : ((v6 = 0 & v5 = 0 & happens(v4, v1) = 0 & terminates(v4, v0, v1) = 0) | (holdsAt(v0, v2) = v5 & holdsAt(v0, v1) = v4 & ( ~ (v4 = 0) | v5 = 0)))) % 27.34/7.59 | (79) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (plus(v1, n1) = v3) | ~ (holdsAt(v2, v3) = 0) | ~ (happens(v0, v1) = 0) | ? [v4] : ( ~ (v4 = 0) & terminates(v0, v2, v1) = v4)) % 27.34/7.59 | (80) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (waterLevel(v3) = v0) | ~ (holdsAt(v0, v1) = 0) | ~ (initiates(tapOff, v0, v1) = v2)) % 27.34/7.59 | (81) ! [v0] : ( ~ (less_or_equal(v0, n4) = 0) | less(v0, n5) = 0) % 27.34/7.59 | (82) ! [v0] : ! [v1] : (v1 = 0 | ~ (terminates(tapOff, filling, v0) = v1)) % 27.34/7.59 | (83) ! [v0] : ! [v1] : (v1 = 0 | ~ (happens(overflow, v0) = v1) | ? [v2] : ? [v3] : (holdsAt(all_0_5_5, v0) = v2 & holdsAt(filling, v0) = v3 & ( ~ (v3 = 0) | ~ (v2 = 0)))) % 27.34/7.59 | (84) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (waterLevel(v3) = v0) | ~ (holdsAt(v0, v1) = 0) | ~ (initiates(overflow, v0, v1) = v2)) % 27.34/7.59 | (85) holdsAt(filling, n0) = all_0_3_3 % 27.34/7.59 | (86) ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n8) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n9) = v2)) % 27.34/7.59 | (87) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (less_or_equal(v3, v2) = v1) | ~ (less_or_equal(v3, v2) = v0)) % 27.34/7.59 | (88) plus(n0, n1) = n1 % 27.34/7.59 | (89) ! [v0] : ! [v1] : ! [v2] : ( ~ (stoppedIn(v0, v1, v2) = 0) | ? [v3] : ? [v4] : (happens(v3, v4) = 0 & less(v4, v2) = 0 & less(v0, v4) = 0 & terminates(v3, v1, v4) = 0)) % 27.34/7.59 | (90) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (releasedAt(v2, v3) = 0) | ~ (plus(v1, n1) = v3) | ~ (happens(v0, v1) = 0) | ? [v4] : ? [v5] : ( ~ (v5 = 0) & ~ (v4 = 0) & initiates(v0, v2, v1) = v4 & terminates(v0, v2, v1) = v5)) % 27.34/7.59 | (91) ~ (tapOff = tapOn) % 27.34/7.59 | (92) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (releasedAt(v3, v2) = v1) | ~ (releasedAt(v3, v2) = v0)) % 27.34/7.59 | (93) ! [v0] : ! [v1] : ! [v2] : (v1 = spilling | v1 = filling | ~ (initiates(v0, v1, v2) = 0) | ? [v3] : ? [v4] : ? [v5] : ((v5 = 0 & v4 = v1 & v0 = tapOff & waterLevel(v3) = v1 & holdsAt(v1, v2) = 0) | (v5 = 0 & v4 = v1 & v0 = overflow & waterLevel(v3) = v1 & holdsAt(v1, v2) = 0))) % 27.34/7.59 | (94) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (waterLevel(v0) = v2) | ~ (waterLevel(v0) = v1)) % 27.34/7.59 | (95) ! [v0] : ! [v1] : (v1 = 0 | ~ (initiates(overflow, spilling, v0) = v1)) % 27.34/7.59 | (96) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (happens(v3, v2) = v1) | ~ (happens(v3, v2) = v0)) % 27.34/7.59 | (97) plus(n1, n1) = n2 % 27.34/7.59 | (98) ! [v0] : ( ~ (less_or_equal(v0, n5) = 0) | less(v0, n6) = 0) % 27.34/7.59 | (99) ! [v0] : ~ (waterLevel(v0) = spilling) % 27.34/7.59 | (100) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (waterLevel(v3) = v0) | ~ (releases(tapOn, v0, v1) = v2)) % 27.34/7.59 | (101) ! [v0] : ! [v1] : (v1 = 0 | ~ (less_or_equal(v0, n3) = v1) | ? [v2] : ( ~ (v2 = 0) & less(v0, n4) = v2)) % 27.34/7.59 | (102) plus(n3, n3) = n6 % 27.34/7.59 | (103) ! [v0] : ( ~ (less_or_equal(v0, n0) = 0) | less(v0, n1) = 0) % 27.34/7.59 | (104) holdsAt(all_0_4_4, n0) = 0 % 27.34/7.59 | (105) ~ (tapOff = overflow) % 27.34/7.59 | (106) ! [v0] : ! [v1] : (v0 = tapOn | ~ (happens(v0, v1) = 0) | (holdsAt(all_0_5_5, v1) = 0 & holdsAt(filling, v1) = 0)) % 27.34/7.59 | (107) ! [v0] : ( ~ (less_or_equal(v0, n6) = 0) | less(v0, n7) = 0) % 27.34/7.59 | (108) releasedAt(filling, n3) = 0 % 27.34/7.59 | % 27.34/7.59 | Instantiating formula (92) with filling, n0, all_0_1_1, 0 and discharging atoms releasedAt(filling, n0) = all_0_1_1, yields: % 27.34/7.59 | (109) all_0_1_1 = 0 | ~ (releasedAt(filling, n0) = 0) % 27.34/7.59 | % 27.34/7.60 | Instantiating formula (55) with n3, n3, n5, n4 yields: % 27.34/7.60 | (110) n5 = n4 | ~ (plus(n3, n3) = n5) | ~ (plus(n3, n3) = n4) % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (55) with n3, n3, n6, n5 and discharging atoms plus(n3, n3) = n6, yields: % 27.34/7.60 | (111) n6 = n5 | ~ (plus(n3, n3) = n5) % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (55) with n1, n1, n3, n4 yields: % 27.34/7.60 | (112) n4 = n3 | ~ (plus(n1, n1) = n4) | ~ (plus(n1, n1) = n3) % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (55) with n1, n3, n4, n5 and discharging atoms plus(n1, n3) = n4, yields: % 27.34/7.60 | (113) n5 = n4 | ~ (plus(n1, n3) = n5) % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (55) with n1, n1, n4, n6 yields: % 27.34/7.60 | (114) n6 = n4 | ~ (plus(n1, n1) = n6) | ~ (plus(n1, n1) = n4) % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (55) with n1, n3, n4, n3 and discharging atoms plus(n1, n3) = n4, yields: % 27.34/7.60 | (115) n4 = n3 | ~ (plus(n1, n3) = n3) % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (55) with n1, n1, n1, n3 yields: % 27.34/7.60 | (116) n3 = n1 | ~ (plus(n1, n1) = n3) | ~ (plus(n1, n1) = n1) % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (55) with n1, n1, n2, n4 and discharging atoms plus(n1, n1) = n2, yields: % 27.34/7.60 | (117) n4 = n2 | ~ (plus(n1, n1) = n4) % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (55) with n0, n0, n0, n4 and discharging atoms plus(n0, n0) = n0, yields: % 27.34/7.60 | (118) n4 = n0 | ~ (plus(n0, n0) = n4) % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (55) with n0, n2, n2, n3 and discharging atoms plus(n0, n2) = n2, yields: % 27.34/7.60 | (119) n2 = n3 | ~ (plus(n0, n2) = n3) % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (55) with n0, n3, n3, n5 and discharging atoms plus(n0, n3) = n3, yields: % 27.34/7.60 | (120) n5 = n3 | ~ (plus(n0, n3) = n5) % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (55) with n0, n0, n0, n6 and discharging atoms plus(n0, n0) = n0, yields: % 27.34/7.60 | (121) n6 = n0 | ~ (plus(n0, n0) = n6) % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (55) with n0, n3, n3, n4 and discharging atoms plus(n0, n3) = n3, yields: % 27.34/7.60 | (122) n4 = n3 | ~ (plus(n0, n3) = n4) % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (55) with n0, n0, n0, n2 and discharging atoms plus(n0, n0) = n0, yields: % 27.34/7.60 | (123) n2 = n0 | ~ (plus(n0, n0) = n2) % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (66) with all_0_5_5, n3 and discharging atoms waterLevel(n3) = all_0_5_5, yields: % 27.34/7.60 | (124) ? [v0] : ( ~ (v0 = 0) & releasedAt(all_0_5_5, n0) = v0) % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (66) with all_0_4_4, n0 and discharging atoms waterLevel(n0) = all_0_4_4, yields: % 27.34/7.60 | (125) ? [v0] : ( ~ (v0 = 0) & releasedAt(all_0_4_4, n0) = v0) % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (13) with n5, n3, n2 and discharging atoms plus(n2, n3) = n5, yields: % 27.34/7.60 | (126) plus(n3, n2) = n5 % 27.34/7.60 | % 27.34/7.60 | Instantiating formula (70) with n3, n1, filling and discharging atoms releasedAt(filling, n3) = 0, yields: % 27.81/7.60 | (127) ~ (plus(n1, n1) = n3) | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & releases(v0, filling, n1) = 0 & happens(v0, n1) = 0) | (v0 = 0 & releasedAt(filling, n1) = 0)) % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (13) with n3, n2, n1 and discharging atoms plus(n1, n2) = n3, yields: % 27.81/7.60 | (128) plus(n2, n1) = n3 % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (13) with n4, n3, n1 and discharging atoms plus(n1, n3) = n4, yields: % 27.81/7.60 | (129) plus(n3, n1) = n4 % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (13) with n2, n2, n0 and discharging atoms plus(n0, n2) = n2, yields: % 27.81/7.60 | (130) plus(n2, n0) = n2 % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (70) with n1, n0, filling and discharging atoms plus(n0, n1) = n1, yields: % 27.81/7.60 | (131) ~ (releasedAt(filling, n1) = 0) | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & releases(v0, filling, n0) = 0 & happens(v0, n0) = 0) | (v0 = 0 & releasedAt(filling, n0) = 0)) % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (13) with n3, n3, n0 and discharging atoms plus(n0, n3) = n3, yields: % 27.81/7.60 | (132) plus(n3, n0) = n3 % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (30) with all_0_0_0, n0, n0, spilling and discharging atoms releasedAt(spilling, n0) = all_0_0_0, yields: % 27.81/7.60 | (133) all_0_0_0 = 0 | ~ (plus(n0, n1) = n0) | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v1 = 0 & initiates(v0, spilling, n0) = v2 & happens(v0, n0) = 0 & terminates(v0, spilling, n0) = v3 & (v3 = 0 | v2 = 0)) | ( ~ (v0 = 0) & releasedAt(spilling, n0) = v0)) % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (39) with all_0_0_0, n0, n0, spilling and discharging atoms releasedAt(spilling, n0) = all_0_0_0, yields: % 27.81/7.60 | (134) all_0_0_0 = 0 | ~ (plus(n0, n1) = n0) | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & initiates(v0, spilling, n0) = 0 & happens(v0, n0) = 0) | (holdsAt(spilling, n0) = v1 & holdsAt(spilling, n0) = v0 & ( ~ (v1 = 0) | v0 = 0))) % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (78) with all_0_0_0, n0, n0, spilling and discharging atoms releasedAt(spilling, n0) = all_0_0_0, yields: % 27.81/7.60 | (135) all_0_0_0 = 0 | ~ (plus(n0, n1) = n0) | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & happens(v0, n0) = 0 & terminates(v0, spilling, n0) = 0) | (holdsAt(spilling, n0) = v1 & holdsAt(spilling, n0) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (30) with all_0_1_1, n0, n0, filling and discharging atoms releasedAt(filling, n0) = all_0_1_1, yields: % 27.81/7.60 | (136) all_0_1_1 = 0 | ~ (plus(n0, n1) = n0) | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v1 = 0 & initiates(v0, filling, n0) = v2 & happens(v0, n0) = 0 & terminates(v0, filling, n0) = v3 & (v3 = 0 | v2 = 0)) | ( ~ (v0 = 0) & releasedAt(filling, n0) = v0)) % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (39) with all_0_1_1, n0, n0, filling and discharging atoms releasedAt(filling, n0) = all_0_1_1, yields: % 27.81/7.60 | (137) all_0_1_1 = 0 | ~ (plus(n0, n1) = n0) | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & initiates(v0, filling, n0) = 0 & happens(v0, n0) = 0) | (holdsAt(filling, n0) = v1 & holdsAt(filling, n0) = v0 & ( ~ (v1 = 0) | v0 = 0))) % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (78) with all_0_1_1, n0, n0, filling and discharging atoms releasedAt(filling, n0) = all_0_1_1, yields: % 27.81/7.60 | (138) all_0_1_1 = 0 | ~ (plus(n0, n1) = n0) | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & happens(v0, n0) = 0 & terminates(v0, filling, n0) = 0) | (holdsAt(filling, n0) = v1 & holdsAt(filling, n0) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (13) with n1, n1, n0 and discharging atoms plus(n0, n1) = n1, yields: % 27.81/7.60 | (139) plus(n1, n0) = n1 % 27.81/7.60 | % 27.81/7.60 | Instantiating (125) with all_17_0_6 yields: % 27.81/7.60 | (140) ~ (all_17_0_6 = 0) & releasedAt(all_0_4_4, n0) = all_17_0_6 % 27.81/7.60 | % 27.81/7.60 | Applying alpha-rule on (140) yields: % 27.81/7.60 | (141) ~ (all_17_0_6 = 0) % 27.81/7.60 | (142) releasedAt(all_0_4_4, n0) = all_17_0_6 % 27.81/7.60 | % 27.81/7.60 | Instantiating (124) with all_19_0_7 yields: % 27.81/7.60 | (143) ~ (all_19_0_7 = 0) & releasedAt(all_0_5_5, n0) = all_19_0_7 % 27.81/7.60 | % 27.81/7.60 | Applying alpha-rule on (143) yields: % 27.81/7.60 | (144) ~ (all_19_0_7 = 0) % 27.81/7.60 | (145) releasedAt(all_0_5_5, n0) = all_19_0_7 % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (55) with n1, n2, n5, n1 yields: % 27.81/7.60 | (146) n5 = n1 | ~ (plus(n1, n2) = n5) | ~ (plus(n1, n2) = n1) % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (55) with n3, n1, n4, n3 and discharging atoms plus(n3, n1) = n4, yields: % 27.81/7.60 | (147) n4 = n3 | ~ (plus(n3, n1) = n3) % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (55) with n3, n0, n3, n5 and discharging atoms plus(n3, n0) = n3, yields: % 27.81/7.60 | (148) n5 = n3 | ~ (plus(n3, n0) = n5) % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (30) with all_17_0_6, n0, n0, all_0_4_4 and discharging atoms releasedAt(all_0_4_4, n0) = all_17_0_6, yields: % 27.81/7.60 | (149) all_17_0_6 = 0 | ~ (plus(n0, n1) = n0) | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v1 = 0 & initiates(v0, all_0_4_4, n0) = v2 & happens(v0, n0) = 0 & terminates(v0, all_0_4_4, n0) = v3 & (v3 = 0 | v2 = 0)) | ( ~ (v0 = 0) & releasedAt(all_0_4_4, n0) = v0)) % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (39) with all_17_0_6, n0, n0, all_0_4_4 and discharging atoms releasedAt(all_0_4_4, n0) = all_17_0_6, yields: % 27.81/7.60 | (150) all_17_0_6 = 0 | ~ (plus(n0, n1) = n0) | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & initiates(v0, all_0_4_4, n0) = 0 & happens(v0, n0) = 0) | (holdsAt(all_0_4_4, n0) = v1 & holdsAt(all_0_4_4, n0) = v0 & ( ~ (v1 = 0) | v0 = 0))) % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (78) with all_17_0_6, n0, n0, all_0_4_4 and discharging atoms releasedAt(all_0_4_4, n0) = all_17_0_6, yields: % 27.81/7.60 | (151) all_17_0_6 = 0 | ~ (plus(n0, n1) = n0) | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & happens(v0, n0) = 0 & terminates(v0, all_0_4_4, n0) = 0) | (holdsAt(all_0_4_4, n0) = v1 & holdsAt(all_0_4_4, n0) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (30) with all_19_0_7, n0, n0, all_0_5_5 and discharging atoms releasedAt(all_0_5_5, n0) = all_19_0_7, yields: % 27.81/7.60 | (152) all_19_0_7 = 0 | ~ (plus(n0, n1) = n0) | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v1 = 0 & initiates(v0, all_0_5_5, n0) = v2 & happens(v0, n0) = 0 & terminates(v0, all_0_5_5, n0) = v3 & (v3 = 0 | v2 = 0)) | ( ~ (v0 = 0) & releasedAt(all_0_5_5, n0) = v0)) % 27.81/7.60 | % 27.81/7.60 | Instantiating formula (39) with all_19_0_7, n0, n0, all_0_5_5 and discharging atoms releasedAt(all_0_5_5, n0) = all_19_0_7, yields: % 27.81/7.60 | (153) all_19_0_7 = 0 | ~ (plus(n0, n1) = n0) | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & initiates(v0, all_0_5_5, n0) = 0 & happens(v0, n0) = 0) | (holdsAt(all_0_5_5, n0) = v1 & holdsAt(all_0_5_5, n0) = v0 & ( ~ (v1 = 0) | v0 = 0))) % 27.81/7.61 | % 27.81/7.61 | Instantiating formula (78) with all_19_0_7, n0, n0, all_0_5_5 and discharging atoms releasedAt(all_0_5_5, n0) = all_19_0_7, yields: % 27.81/7.61 | (154) all_19_0_7 = 0 | ~ (plus(n0, n1) = n0) | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & happens(v0, n0) = 0 & terminates(v0, all_0_5_5, n0) = 0) | (holdsAt(all_0_5_5, n0) = v1 & holdsAt(all_0_5_5, n0) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 27.81/7.61 | % 27.81/7.61 | Instantiating formula (70) with n3, n2, filling and discharging atoms releasedAt(filling, n3) = 0, plus(n2, n1) = n3, yields: % 27.81/7.61 | (155) ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & releases(v0, filling, n2) = 0 & happens(v0, n2) = 0) | (v0 = 0 & releasedAt(filling, n2) = 0)) % 27.81/7.61 | % 27.81/7.61 | Instantiating formula (30) with all_19_0_7, n0, n3, all_0_5_5 and discharging atoms releasedAt(all_0_5_5, n0) = all_19_0_7, yields: % 27.81/7.61 | (156) all_19_0_7 = 0 | ~ (plus(n3, n1) = n0) | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v1 = 0 & initiates(v0, all_0_5_5, n3) = v2 & happens(v0, n3) = 0 & terminates(v0, all_0_5_5, n3) = v3 & (v3 = 0 | v2 = 0)) | ( ~ (v0 = 0) & releasedAt(all_0_5_5, n3) = v0)) % 27.81/7.61 | % 27.81/7.61 | Instantiating (155) with all_26_0_8, all_26_1_9, all_26_2_10 yields: % 27.81/7.61 | (157) (all_26_0_8 = 0 & all_26_1_9 = 0 & releases(all_26_2_10, filling, n2) = 0 & happens(all_26_2_10, n2) = 0) | (all_26_2_10 = 0 & releasedAt(filling, n2) = 0) % 27.81/7.61 | % 27.81/7.61 +-Applying beta-rule and splitting (121), into two cases. % 27.81/7.61 |-Branch one: % 27.81/7.61 | (158) ~ (plus(n0, n0) = n6) % 27.81/7.61 | % 27.81/7.61 | Using (3) and (158) yields: % 27.81/7.61 | (159) ~ (n6 = n0) % 27.81/7.61 | % 27.81/7.61 +-Applying beta-rule and splitting (123), into two cases. % 27.81/7.61 |-Branch one: % 27.81/7.61 | (160) ~ (plus(n0, n0) = n2) % 27.81/7.61 | % 27.81/7.61 | Using (130) and (160) yields: % 27.81/7.61 | (161) ~ (n2 = n0) % 27.81/7.61 | % 27.81/7.61 +-Applying beta-rule and splitting (109), into two cases. % 27.81/7.61 |-Branch one: % 27.81/7.61 | (162) ~ (releasedAt(filling, n0) = 0) % 27.81/7.61 | % 27.81/7.61 +-Applying beta-rule and splitting (119), into two cases. % 27.81/7.61 |-Branch one: % 27.81/7.61 | (163) ~ (plus(n0, n2) = n3) % 27.81/7.61 | % 27.81/7.61 | Using (25) and (163) yields: % 27.81/7.61 | (164) ~ (n1 = n0) % 27.81/7.61 | % 27.81/7.61 +-Applying beta-rule and splitting (131), into two cases. % 27.81/7.61 |-Branch one: % 27.81/7.61 | (165) ~ (releasedAt(filling, n1) = 0) % 27.81/7.61 | % 27.81/7.61 +-Applying beta-rule and splitting (157), into two cases. % 27.81/7.61 |-Branch one: % 27.81/7.61 | (166) all_26_0_8 = 0 & all_26_1_9 = 0 & releases(all_26_2_10, filling, n2) = 0 & happens(all_26_2_10, n2) = 0 % 27.81/7.61 | % 27.81/7.61 | Applying alpha-rule on (166) yields: % 27.81/7.61 | (167) all_26_0_8 = 0 % 27.81/7.61 | (168) all_26_1_9 = 0 % 27.81/7.61 | (169) releases(all_26_2_10, filling, n2) = 0 % 27.81/7.61 | (170) happens(all_26_2_10, n2) = 0 % 27.81/7.61 | % 27.81/7.61 | Instantiating formula (33) with n2, all_26_2_10 and discharging atoms happens(all_26_2_10, n2) = 0, yields: % 27.81/7.61 | (171) all_26_2_10 = overflow | n2 = n0 % 27.81/7.61 | % 27.81/7.61 | Instantiating formula (45) with n2, filling, all_26_2_10 and discharging atoms releases(all_26_2_10, filling, n2) = 0, yields: % 27.81/7.61 | (172) ? [v0] : (all_26_2_10 = tapOn & waterLevel(v0) = filling) % 27.81/7.61 | % 27.81/7.61 | Instantiating formula (35) with n2, all_26_2_10 and discharging atoms happens(all_26_2_10, n2) = 0, yields: % 27.81/7.61 | (173) n2 = n0 | (holdsAt(all_0_5_5, n2) = 0 & holdsAt(filling, n2) = 0) % 27.81/7.61 | % 27.81/7.61 | Instantiating (172) with all_306_0_13 yields: % 27.81/7.61 | (174) all_26_2_10 = tapOn & waterLevel(all_306_0_13) = filling % 27.81/7.61 | % 27.81/7.61 | Applying alpha-rule on (174) yields: % 27.81/7.61 | (175) all_26_2_10 = tapOn % 27.81/7.61 | (176) waterLevel(all_306_0_13) = filling % 27.81/7.61 | % 27.81/7.61 +-Applying beta-rule and splitting (173), into two cases. % 27.81/7.61 |-Branch one: % 27.81/7.61 | (177) n2 = n0 % 27.81/7.61 | % 27.81/7.61 | Equations (177) can reduce 161 to: % 27.81/7.61 | (178) $false % 27.81/7.61 | % 27.81/7.61 |-The branch is then unsatisfiable % 27.81/7.61 |-Branch two: % 27.81/7.61 | (161) ~ (n2 = n0) % 27.81/7.61 | (180) holdsAt(all_0_5_5, n2) = 0 & holdsAt(filling, n2) = 0 % 27.81/7.61 | % 27.81/7.61 +-Applying beta-rule and splitting (171), into two cases. % 27.81/7.61 |-Branch one: % 27.81/7.61 | (177) n2 = n0 % 27.81/7.61 | % 27.81/7.61 | Equations (177) can reduce 161 to: % 27.81/7.61 | (178) $false % 27.81/7.61 | % 27.81/7.61 |-The branch is then unsatisfiable % 27.81/7.61 |-Branch two: % 27.81/7.61 | (161) ~ (n2 = n0) % 27.81/7.61 | (184) all_26_2_10 = overflow % 27.81/7.61 | % 27.81/7.61 | Combining equations (184,175) yields a new equation: % 27.81/7.61 | (185) overflow = tapOn % 27.81/7.61 | % 27.81/7.61 | Simplifying 185 yields: % 27.81/7.61 | (186) overflow = tapOn % 27.81/7.61 | % 27.81/7.61 | Equations (186) can reduce 49 to: % 27.81/7.61 | (178) $false % 27.81/7.61 | % 27.81/7.61 |-The branch is then unsatisfiable % 27.81/7.61 |-Branch two: % 27.81/7.61 | (188) all_26_2_10 = 0 & releasedAt(filling, n2) = 0 % 27.81/7.61 | % 27.81/7.61 | Applying alpha-rule on (188) yields: % 27.81/7.61 | (189) all_26_2_10 = 0 % 27.81/7.61 | (190) releasedAt(filling, n2) = 0 % 27.81/7.61 | % 27.81/7.61 | Instantiating formula (70) with n2, n1, filling and discharging atoms releasedAt(filling, n2) = 0, plus(n1, n1) = n2, yields: % 27.81/7.61 | (191) ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & releases(v0, filling, n1) = 0 & happens(v0, n1) = 0) | (v0 = 0 & releasedAt(filling, n1) = 0)) % 27.81/7.61 | % 27.81/7.61 | Instantiating (191) with all_304_0_14, all_304_1_15, all_304_2_16 yields: % 27.81/7.61 | (192) (all_304_0_14 = 0 & all_304_1_15 = 0 & releases(all_304_2_16, filling, n1) = 0 & happens(all_304_2_16, n1) = 0) | (all_304_2_16 = 0 & releasedAt(filling, n1) = 0) % 27.81/7.61 | % 27.81/7.61 +-Applying beta-rule and splitting (192), into two cases. % 27.81/7.61 |-Branch one: % 27.81/7.61 | (193) all_304_0_14 = 0 & all_304_1_15 = 0 & releases(all_304_2_16, filling, n1) = 0 & happens(all_304_2_16, n1) = 0 % 27.81/7.61 | % 27.81/7.61 | Applying alpha-rule on (193) yields: % 27.81/7.61 | (194) all_304_0_14 = 0 % 27.81/7.61 | (195) all_304_1_15 = 0 % 27.81/7.61 | (196) releases(all_304_2_16, filling, n1) = 0 % 27.81/7.61 | (197) happens(all_304_2_16, n1) = 0 % 27.81/7.61 | % 27.81/7.61 | Instantiating formula (33) with n1, all_304_2_16 and discharging atoms happens(all_304_2_16, n1) = 0, yields: % 27.81/7.61 | (198) all_304_2_16 = overflow | n1 = n0 % 27.81/7.61 | % 27.81/7.61 | Instantiating formula (45) with n1, filling, all_304_2_16 and discharging atoms releases(all_304_2_16, filling, n1) = 0, yields: % 27.81/7.61 | (199) ? [v0] : (all_304_2_16 = tapOn & waterLevel(v0) = filling) % 27.81/7.61 | % 27.81/7.61 | Instantiating formula (35) with n1, all_304_2_16 and discharging atoms happens(all_304_2_16, n1) = 0, yields: % 27.81/7.61 | (200) n1 = n0 | (holdsAt(all_0_5_5, n1) = 0 & holdsAt(filling, n1) = 0) % 27.81/7.61 | % 27.81/7.61 | Instantiating (199) with all_314_0_19 yields: % 27.81/7.61 | (201) all_304_2_16 = tapOn & waterLevel(all_314_0_19) = filling % 27.81/7.61 | % 27.81/7.61 | Applying alpha-rule on (201) yields: % 27.81/7.61 | (202) all_304_2_16 = tapOn % 27.81/7.61 | (203) waterLevel(all_314_0_19) = filling % 27.81/7.61 | % 27.81/7.61 +-Applying beta-rule and splitting (200), into two cases. % 27.81/7.61 |-Branch one: % 27.81/7.61 | (204) n1 = n0 % 27.81/7.61 | % 27.81/7.61 | Equations (204) can reduce 164 to: % 27.81/7.61 | (178) $false % 27.81/7.61 | % 27.81/7.61 |-The branch is then unsatisfiable % 27.81/7.61 |-Branch two: % 27.81/7.61 | (164) ~ (n1 = n0) % 27.81/7.61 | (207) holdsAt(all_0_5_5, n1) = 0 & holdsAt(filling, n1) = 0 % 27.81/7.61 | % 27.81/7.61 +-Applying beta-rule and splitting (198), into two cases. % 27.81/7.61 |-Branch one: % 27.81/7.61 | (204) n1 = n0 % 27.81/7.61 | % 27.81/7.61 | Equations (204) can reduce 164 to: % 27.81/7.61 | (178) $false % 27.81/7.61 | % 27.81/7.61 |-The branch is then unsatisfiable % 27.81/7.61 |-Branch two: % 27.81/7.61 | (164) ~ (n1 = n0) % 27.81/7.61 | (211) all_304_2_16 = overflow % 27.81/7.61 | % 27.81/7.61 | Combining equations (211,202) yields a new equation: % 27.81/7.61 | (185) overflow = tapOn % 27.81/7.61 | % 27.81/7.61 | Simplifying 185 yields: % 27.81/7.61 | (186) overflow = tapOn % 27.81/7.61 | % 27.81/7.61 | Equations (186) can reduce 49 to: % 27.81/7.61 | (178) $false % 27.81/7.61 | % 27.81/7.61 |-The branch is then unsatisfiable % 27.81/7.61 |-Branch two: % 27.81/7.61 | (215) all_304_2_16 = 0 & releasedAt(filling, n1) = 0 % 27.81/7.61 | % 27.81/7.61 | Applying alpha-rule on (215) yields: % 27.81/7.61 | (216) all_304_2_16 = 0 % 27.81/7.61 | (217) releasedAt(filling, n1) = 0 % 27.81/7.61 | % 27.81/7.61 | Using (217) and (165) yields: % 27.81/7.61 | (218) $false % 27.81/7.61 | % 27.81/7.61 |-The branch is then unsatisfiable % 27.81/7.61 |-Branch two: % 27.81/7.61 | (217) releasedAt(filling, n1) = 0 % 27.81/7.61 | (220) ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & releases(v0, filling, n0) = 0 & happens(v0, n0) = 0) | (v0 = 0 & releasedAt(filling, n0) = 0)) % 27.81/7.61 | % 27.81/7.61 | Instantiating (220) with all_196_0_20, all_196_1_21, all_196_2_22 yields: % 27.81/7.61 | (221) (all_196_0_20 = 0 & all_196_1_21 = 0 & releases(all_196_2_22, filling, n0) = 0 & happens(all_196_2_22, n0) = 0) | (all_196_2_22 = 0 & releasedAt(filling, n0) = 0) % 27.81/7.61 | % 27.81/7.61 +-Applying beta-rule and splitting (221), into two cases. % 27.81/7.61 |-Branch one: % 27.81/7.61 | (222) all_196_0_20 = 0 & all_196_1_21 = 0 & releases(all_196_2_22, filling, n0) = 0 & happens(all_196_2_22, n0) = 0 % 27.81/7.61 | % 27.81/7.61 | Applying alpha-rule on (222) yields: % 27.81/7.61 | (223) all_196_0_20 = 0 % 27.81/7.61 | (224) all_196_1_21 = 0 % 27.81/7.61 | (225) releases(all_196_2_22, filling, n0) = 0 % 27.81/7.61 | (226) happens(all_196_2_22, n0) = 0 % 27.81/7.61 | % 27.81/7.61 | Instantiating formula (45) with n0, filling, all_196_2_22 and discharging atoms releases(all_196_2_22, filling, n0) = 0, yields: % 27.81/7.61 | (227) ? [v0] : (all_196_2_22 = tapOn & waterLevel(v0) = filling) % 27.81/7.61 | % 27.81/7.62 | Instantiating (227) with all_208_0_25 yields: % 27.81/7.62 | (228) all_196_2_22 = tapOn & waterLevel(all_208_0_25) = filling % 27.81/7.62 | % 27.81/7.62 | Applying alpha-rule on (228) yields: % 27.81/7.62 | (229) all_196_2_22 = tapOn % 27.81/7.62 | (230) waterLevel(all_208_0_25) = filling % 27.81/7.62 | % 27.81/7.62 | Instantiating formula (20) with all_208_0_25 and discharging atoms waterLevel(all_208_0_25) = filling, yields: % 27.81/7.62 | (218) $false % 27.81/7.62 | % 27.81/7.62 |-The branch is then unsatisfiable % 27.81/7.62 |-Branch two: % 27.81/7.62 | (232) all_196_2_22 = 0 & releasedAt(filling, n0) = 0 % 27.81/7.62 | % 27.81/7.62 | Applying alpha-rule on (232) yields: % 27.81/7.62 | (233) all_196_2_22 = 0 % 27.81/7.62 | (234) releasedAt(filling, n0) = 0 % 27.81/7.62 | % 27.81/7.62 | Using (234) and (162) yields: % 27.81/7.62 | (218) $false % 27.81/7.62 | % 27.81/7.62 |-The branch is then unsatisfiable % 27.81/7.62 |-Branch two: % 27.81/7.62 | (236) plus(n0, n2) = n3 % 27.81/7.62 | (237) n2 = n3 % 27.81/7.62 | % 27.81/7.62 | From (237)(237) and (76) follows: % 27.81/7.62 | (238) plus(n3, n3) = n4 % 27.81/7.62 | % 27.81/7.62 | From (237) and (128) follows: % 27.81/7.62 | (239) plus(n3, n1) = n3 % 27.81/7.62 | % 27.81/7.62 | From (237) and (126) follows: % 27.81/7.62 | (240) plus(n3, n3) = n5 % 27.81/7.62 | % 27.81/7.62 | From (237) and (97) follows: % 27.81/7.62 | (241) plus(n1, n1) = n3 % 27.81/7.62 | % 27.81/7.62 | From (237) and (236) follows: % 27.81/7.62 | (7) plus(n0, n3) = n3 % 27.81/7.62 | % 27.81/7.62 +-Applying beta-rule and splitting (147), into two cases. % 27.81/7.62 |-Branch one: % 27.81/7.62 | (243) ~ (plus(n3, n1) = n3) % 27.81/7.62 | % 27.81/7.62 | Using (239) and (243) yields: % 27.81/7.62 | (218) $false % 27.81/7.62 | % 27.81/7.62 |-The branch is then unsatisfiable % 27.81/7.62 |-Branch two: % 27.81/7.62 | (239) plus(n3, n1) = n3 % 27.81/7.62 | (246) n4 = n3 % 27.81/7.62 | % 27.81/7.62 | From (246) and (238) follows: % 27.81/7.62 | (247) plus(n3, n3) = n3 % 27.81/7.62 | % 27.81/7.62 | From (246) and (19) follows: % 27.81/7.62 | (248) plus(n1, n3) = n3 % 27.81/7.62 | % 27.81/7.62 +-Applying beta-rule and splitting (110), into two cases. % 27.81/7.62 |-Branch one: % 27.81/7.62 | (249) ~ (plus(n3, n3) = n5) % 27.81/7.62 | % 27.81/7.62 | Using (240) and (249) yields: % 27.81/7.62 | (218) $false % 27.81/7.62 | % 27.81/7.62 |-The branch is then unsatisfiable % 27.81/7.62 |-Branch two: % 27.81/7.62 | (240) plus(n3, n3) = n5 % 27.81/7.62 | (252) n5 = n4 | ~ (plus(n3, n3) = n4) % 27.81/7.62 | % 27.81/7.62 +-Applying beta-rule and splitting (127), into two cases. % 27.81/7.62 |-Branch one: % 27.81/7.62 | (253) ~ (plus(n1, n1) = n3) % 27.81/7.62 | % 27.81/7.62 | Using (241) and (253) yields: % 27.81/7.62 | (218) $false % 27.81/7.62 | % 27.81/7.62 |-The branch is then unsatisfiable % 27.81/7.62 |-Branch two: % 27.81/7.62 | (241) plus(n1, n1) = n3 % 27.81/7.62 | (191) ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & releases(v0, filling, n1) = 0 & happens(v0, n1) = 0) | (v0 = 0 & releasedAt(filling, n1) = 0)) % 27.81/7.62 | % 27.81/7.62 | Instantiating (191) with all_101_0_26, all_101_1_27, all_101_2_28 yields: % 27.81/7.62 | (257) (all_101_0_26 = 0 & all_101_1_27 = 0 & releases(all_101_2_28, filling, n1) = 0 & happens(all_101_2_28, n1) = 0) | (all_101_2_28 = 0 & releasedAt(filling, n1) = 0) % 27.81/7.62 | % 27.81/7.62 +-Applying beta-rule and splitting (252), into two cases. % 27.81/7.62 |-Branch one: % 27.81/7.62 | (258) ~ (plus(n3, n3) = n4) % 27.81/7.62 | % 27.81/7.62 | From (246) and (258) follows: % 27.81/7.62 | (259) ~ (plus(n3, n3) = n3) % 27.81/7.62 | % 27.81/7.62 | Using (247) and (259) yields: % 27.81/7.62 | (218) $false % 27.81/7.62 | % 27.81/7.62 |-The branch is then unsatisfiable % 27.81/7.62 |-Branch two: % 27.81/7.62 | (238) plus(n3, n3) = n4 % 27.81/7.62 | (262) n5 = n4 % 27.81/7.62 | % 27.81/7.62 | Combining equations (246,262) yields a new equation: % 27.81/7.62 | (263) n5 = n3 % 27.81/7.62 | % 27.81/7.62 | From (246) and (238) follows: % 27.81/7.62 | (247) plus(n3, n3) = n3 % 27.81/7.62 | % 27.81/7.62 +-Applying beta-rule and splitting (111), into two cases. % 27.81/7.62 |-Branch one: % 27.81/7.62 | (249) ~ (plus(n3, n3) = n5) % 27.81/7.62 | % 27.81/7.62 | From (263) and (249) follows: % 27.81/7.62 | (259) ~ (plus(n3, n3) = n3) % 27.81/7.62 | % 27.81/7.62 | Using (247) and (259) yields: % 27.81/7.62 | (218) $false % 27.81/7.62 | % 27.81/7.62 |-The branch is then unsatisfiable % 27.81/7.62 |-Branch two: % 27.81/7.62 | (240) plus(n3, n3) = n5 % 27.81/7.62 | (269) n6 = n5 % 27.81/7.62 | % 27.81/7.62 | Combining equations (263,269) yields a new equation: % 27.81/7.62 | (270) n6 = n3 % 27.81/7.62 | % 27.81/7.62 | Equations (270) can reduce 159 to: % 27.81/7.62 | (271) ~ (n3 = n0) % 27.81/7.62 | % 27.81/7.62 +-Applying beta-rule and splitting (122), into two cases. % 27.81/7.62 |-Branch one: % 27.81/7.62 | (272) ~ (plus(n0, n3) = n4) % 27.81/7.62 | % 27.81/7.62 | From (246) and (272) follows: % 27.81/7.62 | (273) ~ (plus(n0, n3) = n3) % 27.81/7.62 | % 27.81/7.62 | Using (7) and (273) yields: % 27.81/7.62 | (218) $false % 27.81/7.62 | % 27.81/7.62 |-The branch is then unsatisfiable % 27.81/7.62 |-Branch two: % 27.81/7.62 | (275) plus(n0, n3) = n4 % 27.81/7.62 | (246) n4 = n3 % 27.81/7.62 | % 27.81/7.62 | From (246) and (275) follows: % 27.81/7.62 | (7) plus(n0, n3) = n3 % 27.81/7.62 | % 27.81/7.62 +-Applying beta-rule and splitting (120), into two cases. % 27.81/7.62 |-Branch one: % 27.81/7.62 | (278) ~ (plus(n0, n3) = n5) % 27.81/7.62 | % 27.81/7.62 | From (263) and (278) follows: % 27.81/7.62 | (273) ~ (plus(n0, n3) = n3) % 27.81/7.62 | % 27.81/7.62 | Using (7) and (273) yields: % 27.81/7.62 | (218) $false % 27.81/7.62 | % 27.81/7.62 |-The branch is then unsatisfiable % 27.81/7.62 |-Branch two: % 27.81/7.62 | (281) plus(n0, n3) = n5 % 27.81/7.62 | (263) n5 = n3 % 27.81/7.62 | % 27.81/7.62 +-Applying beta-rule and splitting (118), into two cases. % 27.81/7.62 |-Branch one: % 27.81/7.62 | (283) ~ (plus(n0, n0) = n4) % 27.81/7.62 | % 27.81/7.62 | From (246) and (283) follows: % 27.81/7.62 | (284) ~ (plus(n0, n0) = n3) % 27.81/7.62 | % 27.81/7.62 +-Applying beta-rule and splitting (115), into two cases. % 27.81/7.62 |-Branch one: % 27.81/7.62 | (285) ~ (plus(n1, n3) = n3) % 27.81/7.62 | % 27.81/7.62 | Using (248) and (285) yields: % 27.81/7.62 | (218) $false % 27.81/7.62 | % 27.81/7.62 |-The branch is then unsatisfiable % 27.81/7.62 |-Branch two: % 27.81/7.62 | (248) plus(n1, n3) = n3 % 27.81/7.62 | (246) n4 = n3 % 27.81/7.62 | % 27.81/7.62 +-Applying beta-rule and splitting (117), into two cases. % 27.81/7.62 |-Branch one: % 27.81/7.62 | (289) ~ (plus(n1, n1) = n4) % 27.81/7.62 | % 27.81/7.62 | From (246) and (289) follows: % 27.81/7.62 | (253) ~ (plus(n1, n1) = n3) % 27.81/7.62 | % 27.81/7.62 | Using (241) and (253) yields: % 27.81/7.62 | (218) $false % 27.81/7.62 | % 27.81/7.62 |-The branch is then unsatisfiable % 27.81/7.62 |-Branch two: % 27.81/7.62 | (292) plus(n1, n1) = n4 % 27.81/7.62 | (293) n4 = n2 % 27.81/7.62 | % 27.81/7.62 | Combining equations (246,293) yields a new equation: % 27.81/7.62 | (237) n2 = n3 % 27.81/7.62 | % 27.81/7.62 | Combining equations (237,293) yields a new equation: % 27.81/7.62 | (246) n4 = n3 % 27.81/7.62 | % 27.81/7.62 | From (246) and (292) follows: % 27.81/7.62 | (241) plus(n1, n1) = n3 % 27.81/7.62 | % 27.81/7.62 +-Applying beta-rule and splitting (113), into two cases. % 27.81/7.62 |-Branch one: % 27.81/7.62 | (297) ~ (plus(n1, n3) = n5) % 27.81/7.62 | % 27.81/7.62 | From (263) and (297) follows: % 27.81/7.62 | (285) ~ (plus(n1, n3) = n3) % 27.81/7.62 | % 27.81/7.62 | Using (248) and (285) yields: % 27.81/7.62 | (218) $false % 27.81/7.62 | % 27.81/7.62 |-The branch is then unsatisfiable % 27.81/7.62 |-Branch two: % 27.81/7.62 | (300) plus(n1, n3) = n5 % 27.81/7.62 | (262) n5 = n4 % 27.81/7.62 | % 27.81/7.62 | Combining equations (263,262) yields a new equation: % 27.81/7.62 | (246) n4 = n3 % 27.81/7.62 | % 27.81/7.62 +-Applying beta-rule and splitting (116), into two cases. % 27.81/7.62 |-Branch one: % 27.81/7.62 | (253) ~ (plus(n1, n1) = n3) % 27.81/7.62 | % 27.81/7.62 | Using (241) and (253) yields: % 27.81/7.62 | (218) $false % 27.81/7.62 | % 27.81/7.62 |-The branch is then unsatisfiable % 27.81/7.62 |-Branch two: % 27.81/7.62 | (241) plus(n1, n1) = n3 % 27.81/7.62 | (306) n3 = n1 | ~ (plus(n1, n1) = n1) % 27.81/7.62 | % 27.81/7.62 +-Applying beta-rule and splitting (112), into two cases. % 27.81/7.62 |-Branch one: % 27.81/7.62 | (289) ~ (plus(n1, n1) = n4) % 27.81/7.62 | % 27.81/7.62 | From (246) and (289) follows: % 27.81/7.62 | (253) ~ (plus(n1, n1) = n3) % 27.81/7.62 | % 27.81/7.62 | Using (241) and (253) yields: % 27.81/7.62 | (218) $false % 27.81/7.62 | % 27.81/7.62 |-The branch is then unsatisfiable % 27.81/7.62 |-Branch two: % 27.81/7.62 | (292) plus(n1, n1) = n4 % 27.81/7.62 | (311) n4 = n3 | ~ (plus(n1, n1) = n3) % 27.81/7.62 | % 27.81/7.62 | From (246) and (292) follows: % 27.81/7.62 | (241) plus(n1, n1) = n3 % 27.81/7.62 | % 27.81/7.62 +-Applying beta-rule and splitting (114), into two cases. % 27.81/7.62 |-Branch one: % 27.81/7.62 | (313) ~ (plus(n1, n1) = n6) % 27.81/7.62 | % 27.81/7.62 | From (270) and (313) follows: % 27.81/7.62 | (253) ~ (plus(n1, n1) = n3) % 27.81/7.62 | % 27.81/7.62 | Using (241) and (253) yields: % 27.81/7.62 | (218) $false % 27.81/7.62 | % 27.81/7.62 |-The branch is then unsatisfiable % 27.81/7.62 |-Branch two: % 27.81/7.62 | (316) plus(n1, n1) = n6 % 27.81/7.62 | (317) n6 = n4 | ~ (plus(n1, n1) = n4) % 27.81/7.63 | % 27.81/7.63 | From (270) and (316) follows: % 27.81/7.63 | (241) plus(n1, n1) = n3 % 27.81/7.63 | % 27.81/7.63 +-Applying beta-rule and splitting (131), into two cases. % 27.81/7.63 |-Branch one: % 27.81/7.63 | (165) ~ (releasedAt(filling, n1) = 0) % 27.81/7.63 | % 27.81/7.63 +-Applying beta-rule and splitting (257), into two cases. % 27.81/7.63 |-Branch one: % 27.81/7.63 | (320) all_101_0_26 = 0 & all_101_1_27 = 0 & releases(all_101_2_28, filling, n1) = 0 & happens(all_101_2_28, n1) = 0 % 27.81/7.63 | % 27.81/7.63 | Applying alpha-rule on (320) yields: % 27.81/7.63 | (321) all_101_0_26 = 0 % 27.81/7.63 | (322) all_101_1_27 = 0 % 27.81/7.63 | (323) releases(all_101_2_28, filling, n1) = 0 % 27.81/7.63 | (324) happens(all_101_2_28, n1) = 0 % 27.81/7.63 | % 27.81/7.63 | Instantiating formula (33) with n1, all_101_2_28 and discharging atoms happens(all_101_2_28, n1) = 0, yields: % 27.81/7.63 | (325) all_101_2_28 = overflow | n1 = n0 % 27.81/7.63 | % 27.81/7.63 +-Applying beta-rule and splitting (133), into two cases. % 27.81/7.63 |-Branch one: % 27.81/7.63 | (326) ~ (plus(n0, n1) = n0) % 27.81/7.63 | % 27.81/7.63 | Using (88) and (326) yields: % 27.81/7.63 | (164) ~ (n1 = n0) % 27.81/7.63 | % 27.81/7.63 +-Applying beta-rule and splitting (325), into two cases. % 27.81/7.63 |-Branch one: % 27.81/7.63 | (204) n1 = n0 % 27.81/7.63 | % 27.81/7.63 | Equations (204) can reduce 164 to: % 27.81/7.63 | (178) $false % 27.81/7.63 | % 27.81/7.63 |-The branch is then unsatisfiable % 27.81/7.63 |-Branch two: % 27.81/7.63 | (164) ~ (n1 = n0) % 27.81/7.63 | (331) all_101_2_28 = overflow % 27.81/7.63 | % 27.81/7.63 | From (331) and (323) follows: % 27.81/7.63 | (332) releases(overflow, filling, n1) = 0 % 27.81/7.63 | % 27.81/7.63 | Instantiating formula (45) with n1, filling, overflow and discharging atoms releases(overflow, filling, n1) = 0, yields: % 27.81/7.63 | (333) ? [v0] : (overflow = tapOn & waterLevel(v0) = filling) % 27.81/7.63 | % 27.81/7.63 | Instantiating (333) with all_275_0_34 yields: % 27.81/7.63 | (334) overflow = tapOn & waterLevel(all_275_0_34) = filling % 27.81/7.63 | % 27.81/7.63 | Applying alpha-rule on (334) yields: % 27.81/7.63 | (186) overflow = tapOn % 27.81/7.63 | (336) waterLevel(all_275_0_34) = filling % 27.81/7.63 | % 27.81/7.63 | Equations (186) can reduce 49 to: % 27.81/7.63 | (178) $false % 27.81/7.63 | % 27.81/7.63 |-The branch is then unsatisfiable % 27.81/7.63 |-Branch two: % 27.81/7.63 | (338) plus(n0, n1) = n0 % 27.81/7.63 | (339) all_0_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v1 = 0 & initiates(v0, spilling, n0) = v2 & happens(v0, n0) = 0 & terminates(v0, spilling, n0) = v3 & (v3 = 0 | v2 = 0)) | ( ~ (v0 = 0) & releasedAt(spilling, n0) = v0)) % 27.81/7.63 | % 27.81/7.63 +-Applying beta-rule and splitting (138), into two cases. % 27.81/7.63 |-Branch one: % 27.81/7.63 | (326) ~ (plus(n0, n1) = n0) % 27.81/7.63 | % 27.81/7.63 | Using (338) and (326) yields: % 27.81/7.63 | (218) $false % 27.81/7.63 | % 27.81/7.63 |-The branch is then unsatisfiable % 27.81/7.63 |-Branch two: % 27.81/7.63 | (338) plus(n0, n1) = n0 % 27.81/7.63 | (343) all_0_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & happens(v0, n0) = 0 & terminates(v0, filling, n0) = 0) | (holdsAt(filling, n0) = v1 & holdsAt(filling, n0) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 27.81/7.63 | % 27.81/7.63 +-Applying beta-rule and splitting (134), into two cases. % 27.81/7.63 |-Branch one: % 27.81/7.63 | (326) ~ (plus(n0, n1) = n0) % 27.81/7.63 | % 27.81/7.63 | Using (338) and (326) yields: % 27.81/7.63 | (218) $false % 27.81/7.63 | % 27.81/7.63 |-The branch is then unsatisfiable % 27.81/7.63 |-Branch two: % 27.81/7.63 | (338) plus(n0, n1) = n0 % 27.81/7.63 | (347) all_0_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & initiates(v0, spilling, n0) = 0 & happens(v0, n0) = 0) | (holdsAt(spilling, n0) = v1 & holdsAt(spilling, n0) = v0 & ( ~ (v1 = 0) | v0 = 0))) % 27.81/7.63 | % 27.81/7.63 +-Applying beta-rule and splitting (137), into two cases. % 27.81/7.63 |-Branch one: % 27.81/7.63 | (326) ~ (plus(n0, n1) = n0) % 27.81/7.63 | % 27.81/7.63 | Using (338) and (326) yields: % 27.81/7.63 | (218) $false % 27.81/7.63 | % 27.81/7.63 |-The branch is then unsatisfiable % 27.81/7.63 |-Branch two: % 27.81/7.63 | (338) plus(n0, n1) = n0 % 27.81/7.63 | (351) all_0_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & initiates(v0, filling, n0) = 0 & happens(v0, n0) = 0) | (holdsAt(filling, n0) = v1 & holdsAt(filling, n0) = v0 & ( ~ (v1 = 0) | v0 = 0))) % 27.81/7.63 | % 27.81/7.63 +-Applying beta-rule and splitting (136), into two cases. % 27.81/7.63 |-Branch one: % 27.81/7.63 | (326) ~ (plus(n0, n1) = n0) % 27.81/7.63 | % 27.81/7.63 | Using (338) and (326) yields: % 27.81/7.63 | (218) $false % 27.81/7.63 | % 27.81/7.63 |-The branch is then unsatisfiable % 27.81/7.63 |-Branch two: % 27.81/7.63 | (338) plus(n0, n1) = n0 % 27.81/7.63 | (355) all_0_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v1 = 0 & initiates(v0, filling, n0) = v2 & happens(v0, n0) = 0 & terminates(v0, filling, n0) = v3 & (v3 = 0 | v2 = 0)) | ( ~ (v0 = 0) & releasedAt(filling, n0) = v0)) % 27.81/7.63 | % 27.81/7.63 +-Applying beta-rule and splitting (135), into two cases. % 27.81/7.63 |-Branch one: % 27.81/7.63 | (326) ~ (plus(n0, n1) = n0) % 27.81/7.63 | % 27.81/7.63 | Using (338) and (326) yields: % 27.81/7.63 | (218) $false % 27.81/7.63 | % 27.81/7.63 |-The branch is then unsatisfiable % 27.81/7.63 |-Branch two: % 27.81/7.63 | (338) plus(n0, n1) = n0 % 27.81/7.63 | (359) all_0_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & happens(v0, n0) = 0 & terminates(v0, spilling, n0) = 0) | (holdsAt(spilling, n0) = v1 & holdsAt(spilling, n0) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 27.81/7.63 | % 27.81/7.63 +-Applying beta-rule and splitting (150), into two cases. % 27.81/7.63 |-Branch one: % 27.81/7.63 | (326) ~ (plus(n0, n1) = n0) % 27.81/7.63 | % 27.81/7.63 | Using (338) and (326) yields: % 27.81/7.63 | (218) $false % 27.81/7.63 | % 27.81/7.63 |-The branch is then unsatisfiable % 27.81/7.63 |-Branch two: % 27.81/7.63 | (338) plus(n0, n1) = n0 % 27.81/7.63 | (363) all_17_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & initiates(v0, all_0_4_4, n0) = 0 & happens(v0, n0) = 0) | (holdsAt(all_0_4_4, n0) = v1 & holdsAt(all_0_4_4, n0) = v0 & ( ~ (v1 = 0) | v0 = 0))) % 27.81/7.63 | % 27.81/7.63 +-Applying beta-rule and splitting (152), into two cases. % 27.81/7.63 |-Branch one: % 27.81/7.63 | (326) ~ (plus(n0, n1) = n0) % 27.81/7.63 | % 27.81/7.63 | Using (338) and (326) yields: % 27.81/7.63 | (218) $false % 27.81/7.63 | % 27.81/7.63 |-The branch is then unsatisfiable % 27.81/7.63 |-Branch two: % 27.81/7.63 | (338) plus(n0, n1) = n0 % 27.81/7.63 | (367) all_19_0_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v1 = 0 & initiates(v0, all_0_5_5, n0) = v2 & happens(v0, n0) = 0 & terminates(v0, all_0_5_5, n0) = v3 & (v3 = 0 | v2 = 0)) | ( ~ (v0 = 0) & releasedAt(all_0_5_5, n0) = v0)) % 27.81/7.63 | % 27.81/7.63 +-Applying beta-rule and splitting (151), into two cases. % 27.81/7.63 |-Branch one: % 27.81/7.63 | (326) ~ (plus(n0, n1) = n0) % 27.81/7.63 | % 27.81/7.63 | Using (338) and (326) yields: % 27.81/7.63 | (218) $false % 27.81/7.63 | % 27.81/7.63 |-The branch is then unsatisfiable % 27.81/7.63 |-Branch two: % 27.81/7.63 | (338) plus(n0, n1) = n0 % 27.81/7.63 | (371) all_17_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & happens(v0, n0) = 0 & terminates(v0, all_0_4_4, n0) = 0) | (holdsAt(all_0_4_4, n0) = v1 & holdsAt(all_0_4_4, n0) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 27.81/7.63 | % 27.81/7.63 +-Applying beta-rule and splitting (154), into two cases. % 27.81/7.63 |-Branch one: % 27.81/7.63 | (326) ~ (plus(n0, n1) = n0) % 27.81/7.63 | % 27.81/7.63 | Using (338) and (326) yields: % 27.81/7.63 | (218) $false % 27.81/7.63 | % 27.81/7.63 |-The branch is then unsatisfiable % 27.81/7.63 |-Branch two: % 27.81/7.63 | (338) plus(n0, n1) = n0 % 27.81/7.63 | (375) all_19_0_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & happens(v0, n0) = 0 & terminates(v0, all_0_5_5, n0) = 0) | (holdsAt(all_0_5_5, n0) = v1 & holdsAt(all_0_5_5, n0) = v0 & ( ~ (v0 = 0) | v1 = 0))) % 27.81/7.63 | % 27.81/7.63 +-Applying beta-rule and splitting (149), into two cases. % 27.81/7.63 |-Branch one: % 27.81/7.63 | (326) ~ (plus(n0, n1) = n0) % 27.81/7.63 | % 27.81/7.63 | Using (338) and (326) yields: % 27.81/7.63 | (218) $false % 27.81/7.63 | % 27.81/7.63 |-The branch is then unsatisfiable % 27.81/7.63 |-Branch two: % 27.81/7.63 | (338) plus(n0, n1) = n0 % 27.81/7.63 | (379) all_17_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v1 = 0 & initiates(v0, all_0_4_4, n0) = v2 & happens(v0, n0) = 0 & terminates(v0, all_0_4_4, n0) = v3 & (v3 = 0 | v2 = 0)) | ( ~ (v0 = 0) & releasedAt(all_0_4_4, n0) = v0)) % 27.81/7.63 | % 27.81/7.63 +-Applying beta-rule and splitting (153), into two cases. % 27.81/7.63 |-Branch one: % 27.81/7.63 | (326) ~ (plus(n0, n1) = n0) % 27.81/7.63 | % 27.81/7.63 | Using (338) and (326) yields: % 27.81/7.63 | (218) $false % 27.81/7.63 | % 27.81/7.63 |-The branch is then unsatisfiable % 27.81/7.63 |-Branch two: % 27.81/7.63 | (338) plus(n0, n1) = n0 % 27.81/7.63 | (383) all_19_0_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & initiates(v0, all_0_5_5, n0) = 0 & happens(v0, n0) = 0) | (holdsAt(all_0_5_5, n0) = v1 & holdsAt(all_0_5_5, n0) = v0 & ( ~ (v1 = 0) | v0 = 0))) % 27.81/7.63 | % 27.81/7.63 | Instantiating formula (55) with n0, n1, n0, n1 and discharging atoms plus(n0, n1) = n1, plus(n0, n1) = n0, yields: % 27.81/7.63 | (204) n1 = n0 % 27.81/7.63 | % 27.81/7.63 | From (204)(204) and (241) follows: % 27.81/7.63 | (385) plus(n0, n0) = n3 % 27.81/7.63 | % 27.81/7.63 | Using (385) and (284) yields: % 27.81/7.63 | (218) $false % 27.81/7.63 | % 27.81/7.63 |-The branch is then unsatisfiable % 27.81/7.63 |-Branch two: % 27.81/7.63 | (387) all_101_2_28 = 0 & releasedAt(filling, n1) = 0 % 27.81/7.63 | % 27.81/7.63 | Applying alpha-rule on (387) yields: % 27.81/7.63 | (388) all_101_2_28 = 0 % 27.81/7.63 | (217) releasedAt(filling, n1) = 0 % 27.81/7.63 | % 27.81/7.63 | Using (217) and (165) yields: % 27.81/7.63 | (218) $false % 27.81/7.63 | % 27.81/7.63 |-The branch is then unsatisfiable % 27.81/7.63 |-Branch two: % 27.81/7.63 | (217) releasedAt(filling, n1) = 0 % 27.81/7.63 | (220) ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & releases(v0, filling, n0) = 0 & happens(v0, n0) = 0) | (v0 = 0 & releasedAt(filling, n0) = 0)) % 27.81/7.64 | % 27.81/7.64 | Instantiating (220) with all_176_0_75, all_176_1_76, all_176_2_77 yields: % 27.81/7.64 | (393) (all_176_0_75 = 0 & all_176_1_76 = 0 & releases(all_176_2_77, filling, n0) = 0 & happens(all_176_2_77, n0) = 0) | (all_176_2_77 = 0 & releasedAt(filling, n0) = 0) % 27.81/7.64 | % 27.81/7.64 +-Applying beta-rule and splitting (393), into two cases. % 27.81/7.64 |-Branch one: % 27.81/7.64 | (394) all_176_0_75 = 0 & all_176_1_76 = 0 & releases(all_176_2_77, filling, n0) = 0 & happens(all_176_2_77, n0) = 0 % 27.81/7.64 | % 27.81/7.64 | Applying alpha-rule on (394) yields: % 27.81/7.64 | (395) all_176_0_75 = 0 % 27.81/7.64 | (396) all_176_1_76 = 0 % 27.81/7.64 | (397) releases(all_176_2_77, filling, n0) = 0 % 27.81/7.64 | (398) happens(all_176_2_77, n0) = 0 % 27.81/7.64 | % 27.81/7.64 | Instantiating formula (45) with n0, filling, all_176_2_77 and discharging atoms releases(all_176_2_77, filling, n0) = 0, yields: % 27.81/7.64 | (399) ? [v0] : (all_176_2_77 = tapOn & waterLevel(v0) = filling) % 27.81/7.64 | % 27.81/7.64 | Instantiating (399) with all_266_0_80 yields: % 27.81/7.64 | (400) all_176_2_77 = tapOn & waterLevel(all_266_0_80) = filling % 27.81/7.64 | % 27.81/7.64 | Applying alpha-rule on (400) yields: % 27.81/7.64 | (401) all_176_2_77 = tapOn % 27.81/7.64 | (402) waterLevel(all_266_0_80) = filling % 27.81/7.64 | % 27.81/7.64 | Instantiating formula (20) with all_266_0_80 and discharging atoms waterLevel(all_266_0_80) = filling, yields: % 27.81/7.64 | (218) $false % 27.81/7.64 | % 27.81/7.64 |-The branch is then unsatisfiable % 27.81/7.64 |-Branch two: % 27.81/7.64 | (404) all_176_2_77 = 0 & releasedAt(filling, n0) = 0 % 27.81/7.64 | % 27.81/7.64 | Applying alpha-rule on (404) yields: % 27.81/7.64 | (405) all_176_2_77 = 0 % 27.81/7.64 | (234) releasedAt(filling, n0) = 0 % 27.81/7.64 | % 27.81/7.64 | Using (234) and (162) yields: % 27.81/7.64 | (218) $false % 27.81/7.64 | % 27.81/7.64 |-The branch is then unsatisfiable % 27.81/7.64 |-Branch two: % 27.81/7.64 | (408) plus(n0, n0) = n4 % 27.81/7.64 | (409) n4 = n0 % 27.81/7.64 | % 27.81/7.64 | Combining equations (246,409) yields a new equation: % 27.81/7.64 | (410) n3 = n0 % 27.81/7.64 | % 27.81/7.64 | Simplifying 410 yields: % 27.81/7.64 | (411) n3 = n0 % 27.81/7.64 | % 27.81/7.64 | Equations (411) can reduce 271 to: % 27.81/7.64 | (178) $false % 27.81/7.64 | % 27.81/7.64 |-The branch is then unsatisfiable % 27.81/7.64 |-Branch two: % 27.81/7.64 | (234) releasedAt(filling, n0) = 0 % 27.81/7.64 | (414) all_0_1_1 = 0 % 27.81/7.64 | % 27.81/7.64 | Equations (414) can reduce 69 to: % 27.81/7.64 | (178) $false % 27.81/7.64 | % 27.81/7.64 |-The branch is then unsatisfiable % 27.81/7.64 |-Branch two: % 27.81/7.64 | (416) plus(n0, n0) = n2 % 27.81/7.64 | (177) n2 = n0 % 27.81/7.64 | % 27.81/7.64 | From (177) and (126) follows: % 27.81/7.64 | (418) plus(n3, n0) = n5 % 27.81/7.64 | % 27.81/7.64 | From (177) and (25) follows: % 27.81/7.64 | (419) plus(n1, n0) = n3 % 27.81/7.64 | % 27.81/7.64 +-Applying beta-rule and splitting (148), into two cases. % 27.81/7.64 |-Branch one: % 27.81/7.64 | (420) ~ (plus(n3, n0) = n5) % 27.81/7.64 | % 27.81/7.64 | Using (418) and (420) yields: % 27.81/7.64 | (218) $false % 27.81/7.64 | % 27.81/7.64 |-The branch is then unsatisfiable % 27.81/7.64 |-Branch two: % 27.81/7.64 | (418) plus(n3, n0) = n5 % 27.81/7.64 | (263) n5 = n3 % 27.81/7.64 | % 27.81/7.64 +-Applying beta-rule and splitting (146), into two cases. % 27.81/7.64 |-Branch one: % 27.81/7.64 | (424) ~ (plus(n1, n2) = n5) % 27.81/7.64 | % 27.81/7.64 | From (177)(263) and (424) follows: % 27.81/7.64 | (425) ~ (plus(n1, n0) = n3) % 27.81/7.64 | % 27.81/7.64 | Using (419) and (425) yields: % 27.81/7.64 | (218) $false % 27.81/7.64 | % 27.81/7.64 |-The branch is then unsatisfiable % 27.81/7.64 |-Branch two: % 27.81/7.64 | (427) plus(n1, n2) = n5 % 27.81/7.64 | (428) n5 = n1 | ~ (plus(n1, n2) = n1) % 27.81/7.64 | % 27.81/7.64 +-Applying beta-rule and splitting (428), into two cases. % 27.81/7.64 |-Branch one: % 27.81/7.64 | (429) ~ (plus(n1, n2) = n1) % 27.81/7.64 | % 27.81/7.64 | From (177) and (429) follows: % 27.81/7.64 | (430) ~ (plus(n1, n0) = n1) % 27.81/7.64 | % 27.81/7.64 | Using (139) and (430) yields: % 27.81/7.64 | (218) $false % 27.81/7.64 | % 27.81/7.64 |-The branch is then unsatisfiable % 27.81/7.64 |-Branch two: % 27.81/7.64 | (432) plus(n1, n2) = n1 % 27.81/7.64 | (433) n5 = n1 % 27.81/7.64 | % 27.81/7.64 | Combining equations (263,433) yields a new equation: % 27.81/7.64 | (434) n3 = n1 % 27.81/7.64 | % 27.81/7.64 | Simplifying 434 yields: % 27.81/7.64 | (435) n3 = n1 % 27.81/7.64 | % 27.81/7.64 | From (435)(435) and (102) follows: % 27.81/7.64 | (316) plus(n1, n1) = n6 % 27.81/7.64 | % 27.81/7.64 | From (435) and (19) follows: % 27.81/7.64 | (292) plus(n1, n1) = n4 % 27.81/7.64 | % 27.81/7.64 +-Applying beta-rule and splitting (117), into two cases. % 27.81/7.64 |-Branch one: % 27.81/7.64 | (289) ~ (plus(n1, n1) = n4) % 27.81/7.64 | % 27.81/7.64 | Using (292) and (289) yields: % 27.81/7.64 | (218) $false % 27.81/7.64 | % 27.81/7.64 |-The branch is then unsatisfiable % 27.81/7.64 |-Branch two: % 27.81/7.64 | (292) plus(n1, n1) = n4 % 27.81/7.64 | (293) n4 = n2 % 27.81/7.64 | % 27.81/7.64 | Combining equations (177,293) yields a new equation: % 27.81/7.64 | (409) n4 = n0 % 27.81/7.64 | % 27.81/7.64 | From (409) and (292) follows: % 27.81/7.64 | (443) plus(n1, n1) = n0 % 27.81/7.64 | % 27.81/7.64 +-Applying beta-rule and splitting (156), into two cases. % 27.81/7.64 |-Branch one: % 27.81/7.64 | (444) ~ (plus(n3, n1) = n0) % 27.81/7.64 | % 27.81/7.64 | From (435) and (444) follows: % 27.81/7.64 | (445) ~ (plus(n1, n1) = n0) % 27.81/7.64 | % 27.81/7.64 | Using (443) and (445) yields: % 27.81/7.64 | (218) $false % 27.81/7.64 | % 27.81/7.64 |-The branch is then unsatisfiable % 27.81/7.64 |-Branch two: % 27.81/7.64 | (447) plus(n3, n1) = n0 % 27.81/7.64 | (448) all_19_0_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v1 = 0 & initiates(v0, all_0_5_5, n3) = v2 & happens(v0, n3) = 0 & terminates(v0, all_0_5_5, n3) = v3 & (v3 = 0 | v2 = 0)) | ( ~ (v0 = 0) & releasedAt(all_0_5_5, n3) = v0)) % 27.81/7.64 | % 27.81/7.64 | From (435) and (447) follows: % 27.81/7.64 | (443) plus(n1, n1) = n0 % 27.81/7.64 | % 27.81/7.64 +-Applying beta-rule and splitting (114), into two cases. % 27.81/7.64 |-Branch one: % 27.81/7.64 | (313) ~ (plus(n1, n1) = n6) % 27.81/7.64 | % 27.81/7.64 | Using (316) and (313) yields: % 27.81/7.64 | (218) $false % 27.81/7.64 | % 27.81/7.64 |-The branch is then unsatisfiable % 27.81/7.64 |-Branch two: % 27.81/7.64 | (316) plus(n1, n1) = n6 % 27.81/7.64 | (317) n6 = n4 | ~ (plus(n1, n1) = n4) % 27.81/7.64 | % 27.81/7.64 +-Applying beta-rule and splitting (317), into two cases. % 27.81/7.64 |-Branch one: % 27.81/7.64 | (289) ~ (plus(n1, n1) = n4) % 27.81/7.64 | % 27.81/7.64 | From (409) and (289) follows: % 27.81/7.64 | (445) ~ (plus(n1, n1) = n0) % 27.81/7.64 | % 27.81/7.64 | Using (443) and (445) yields: % 27.81/7.64 | (218) $false % 27.81/7.64 | % 27.81/7.64 |-The branch is then unsatisfiable % 27.81/7.64 |-Branch two: % 27.81/7.64 | (292) plus(n1, n1) = n4 % 27.81/7.64 | (458) n6 = n4 % 27.81/7.64 | % 27.81/7.64 | Combining equations (409,458) yields a new equation: % 27.81/7.64 | (459) n6 = n0 % 27.81/7.64 | % 27.81/7.64 | Equations (459) can reduce 159 to: % 27.81/7.64 | (178) $false % 27.81/7.64 | % 27.81/7.64 |-The branch is then unsatisfiable % 27.81/7.64 |-Branch two: % 27.81/7.64 | (461) plus(n0, n0) = n6 % 27.81/7.64 | (459) n6 = n0 % 27.81/7.64 | % 27.81/7.64 +-Applying beta-rule and splitting (119), into two cases. % 27.81/7.64 |-Branch one: % 27.81/7.64 | (163) ~ (plus(n0, n2) = n3) % 27.81/7.64 | % 27.81/7.64 | Using (25) and (163) yields: % 27.81/7.64 | (164) ~ (n1 = n0) % 27.81/7.64 | % 27.81/7.64 +-Applying beta-rule and splitting (123), into two cases. % 27.81/7.64 |-Branch one: % 27.81/7.64 | (160) ~ (plus(n0, n0) = n2) % 27.81/7.64 | % 27.81/7.64 | Using (130) and (160) yields: % 27.81/7.64 | (161) ~ (n2 = n0) % 27.81/7.64 | % 27.81/7.64 +-Applying beta-rule and splitting (109), into two cases. % 27.81/7.64 |-Branch one: % 27.81/7.64 | (162) ~ (releasedAt(filling, n0) = 0) % 27.81/7.64 | % 27.81/7.64 +-Applying beta-rule and splitting (131), into two cases. % 27.81/7.64 |-Branch one: % 27.81/7.64 | (165) ~ (releasedAt(filling, n1) = 0) % 27.81/7.64 | % 27.81/7.64 +-Applying beta-rule and splitting (157), into two cases. % 27.81/7.64 |-Branch one: % 27.81/7.64 | (166) all_26_0_8 = 0 & all_26_1_9 = 0 & releases(all_26_2_10, filling, n2) = 0 & happens(all_26_2_10, n2) = 0 % 27.81/7.64 | % 27.81/7.64 | Applying alpha-rule on (166) yields: % 27.81/7.64 | (167) all_26_0_8 = 0 % 27.81/7.64 | (168) all_26_1_9 = 0 % 27.81/7.64 | (169) releases(all_26_2_10, filling, n2) = 0 % 27.81/7.65 | (170) happens(all_26_2_10, n2) = 0 % 27.81/7.65 | % 27.81/7.65 | Instantiating formula (33) with n2, all_26_2_10 and discharging atoms happens(all_26_2_10, n2) = 0, yields: % 27.81/7.65 | (171) all_26_2_10 = overflow | n2 = n0 % 27.81/7.65 | % 27.81/7.65 | Instantiating formula (45) with n2, filling, all_26_2_10 and discharging atoms releases(all_26_2_10, filling, n2) = 0, yields: % 27.81/7.65 | (172) ? [v0] : (all_26_2_10 = tapOn & waterLevel(v0) = filling) % 27.81/7.65 | % 27.81/7.65 | Instantiating formula (35) with n2, all_26_2_10 and discharging atoms happens(all_26_2_10, n2) = 0, yields: % 27.81/7.65 | (173) n2 = n0 | (holdsAt(all_0_5_5, n2) = 0 & holdsAt(filling, n2) = 0) % 27.81/7.65 | % 27.81/7.65 | Instantiating (172) with all_297_0_90 yields: % 27.81/7.65 | (477) all_26_2_10 = tapOn & waterLevel(all_297_0_90) = filling % 27.81/7.65 | % 27.81/7.65 | Applying alpha-rule on (477) yields: % 27.81/7.65 | (175) all_26_2_10 = tapOn % 27.81/7.65 | (479) waterLevel(all_297_0_90) = filling % 27.81/7.65 | % 27.81/7.65 +-Applying beta-rule and splitting (173), into two cases. % 27.81/7.65 |-Branch one: % 27.81/7.65 | (177) n2 = n0 % 27.81/7.65 | % 27.81/7.65 | Equations (177) can reduce 161 to: % 27.81/7.65 | (178) $false % 27.81/7.65 | % 27.81/7.65 |-The branch is then unsatisfiable % 27.81/7.65 |-Branch two: % 27.81/7.65 | (161) ~ (n2 = n0) % 27.81/7.65 | (180) holdsAt(all_0_5_5, n2) = 0 & holdsAt(filling, n2) = 0 % 27.81/7.65 | % 27.81/7.65 +-Applying beta-rule and splitting (171), into two cases. % 27.81/7.65 |-Branch one: % 27.81/7.65 | (177) n2 = n0 % 27.81/7.65 | % 27.81/7.65 | Equations (177) can reduce 161 to: % 27.81/7.65 | (178) $false % 27.81/7.65 | % 27.81/7.65 |-The branch is then unsatisfiable % 27.81/7.65 |-Branch two: % 27.81/7.65 | (161) ~ (n2 = n0) % 27.81/7.65 | (184) all_26_2_10 = overflow % 27.81/7.65 | % 27.81/7.65 | Combining equations (184,175) yields a new equation: % 27.81/7.65 | (185) overflow = tapOn % 27.81/7.65 | % 27.81/7.65 | Simplifying 185 yields: % 27.81/7.65 | (186) overflow = tapOn % 27.81/7.65 | % 27.81/7.65 | Equations (186) can reduce 49 to: % 27.81/7.65 | (178) $false % 27.81/7.65 | % 27.81/7.65 |-The branch is then unsatisfiable % 27.81/7.65 |-Branch two: % 27.81/7.65 | (188) all_26_2_10 = 0 & releasedAt(filling, n2) = 0 % 27.81/7.65 | % 27.81/7.65 | Applying alpha-rule on (188) yields: % 27.81/7.65 | (189) all_26_2_10 = 0 % 27.81/7.65 | (190) releasedAt(filling, n2) = 0 % 27.81/7.65 | % 27.81/7.65 | Instantiating formula (70) with n2, n1, filling and discharging atoms releasedAt(filling, n2) = 0, plus(n1, n1) = n2, yields: % 27.81/7.65 | (191) ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & releases(v0, filling, n1) = 0 & happens(v0, n1) = 0) | (v0 = 0 & releasedAt(filling, n1) = 0)) % 27.81/7.65 | % 27.81/7.65 | Instantiating (191) with all_295_0_91, all_295_1_92, all_295_2_93 yields: % 27.81/7.65 | (495) (all_295_0_91 = 0 & all_295_1_92 = 0 & releases(all_295_2_93, filling, n1) = 0 & happens(all_295_2_93, n1) = 0) | (all_295_2_93 = 0 & releasedAt(filling, n1) = 0) % 27.81/7.65 | % 27.81/7.65 +-Applying beta-rule and splitting (495), into two cases. % 27.81/7.65 |-Branch one: % 27.81/7.65 | (496) all_295_0_91 = 0 & all_295_1_92 = 0 & releases(all_295_2_93, filling, n1) = 0 & happens(all_295_2_93, n1) = 0 % 27.81/7.65 | % 27.81/7.65 | Applying alpha-rule on (496) yields: % 27.81/7.65 | (497) all_295_0_91 = 0 % 27.81/7.65 | (498) all_295_1_92 = 0 % 27.81/7.65 | (499) releases(all_295_2_93, filling, n1) = 0 % 27.81/7.65 | (500) happens(all_295_2_93, n1) = 0 % 27.81/7.65 | % 27.81/7.65 | Instantiating formula (33) with n1, all_295_2_93 and discharging atoms happens(all_295_2_93, n1) = 0, yields: % 27.81/7.65 | (501) all_295_2_93 = overflow | n1 = n0 % 27.81/7.65 | % 27.81/7.65 | Instantiating formula (45) with n1, filling, all_295_2_93 and discharging atoms releases(all_295_2_93, filling, n1) = 0, yields: % 27.81/7.65 | (502) ? [v0] : (all_295_2_93 = tapOn & waterLevel(v0) = filling) % 27.81/7.65 | % 27.81/7.65 | Instantiating formula (35) with n1, all_295_2_93 and discharging atoms happens(all_295_2_93, n1) = 0, yields: % 27.81/7.65 | (200) n1 = n0 | (holdsAt(all_0_5_5, n1) = 0 & holdsAt(filling, n1) = 0) % 27.81/7.65 | % 27.81/7.65 | Instantiating (502) with all_305_0_96 yields: % 27.81/7.65 | (504) all_295_2_93 = tapOn & waterLevel(all_305_0_96) = filling % 27.81/7.65 | % 27.81/7.65 | Applying alpha-rule on (504) yields: % 27.81/7.65 | (505) all_295_2_93 = tapOn % 27.81/7.65 | (506) waterLevel(all_305_0_96) = filling % 27.81/7.65 | % 27.81/7.65 +-Applying beta-rule and splitting (200), into two cases. % 27.81/7.65 |-Branch one: % 27.81/7.65 | (204) n1 = n0 % 27.81/7.65 | % 27.81/7.65 | Equations (204) can reduce 164 to: % 27.81/7.65 | (178) $false % 27.81/7.65 | % 27.81/7.65 |-The branch is then unsatisfiable % 27.81/7.65 |-Branch two: % 27.81/7.65 | (164) ~ (n1 = n0) % 27.81/7.65 | (207) holdsAt(all_0_5_5, n1) = 0 & holdsAt(filling, n1) = 0 % 27.81/7.65 | % 27.81/7.65 +-Applying beta-rule and splitting (501), into two cases. % 27.81/7.65 |-Branch one: % 27.81/7.65 | (204) n1 = n0 % 27.81/7.65 | % 27.81/7.65 | Equations (204) can reduce 164 to: % 27.81/7.65 | (178) $false % 27.81/7.65 | % 27.81/7.65 |-The branch is then unsatisfiable % 27.81/7.65 |-Branch two: % 27.81/7.65 | (164) ~ (n1 = n0) % 27.81/7.65 | (514) all_295_2_93 = overflow % 27.81/7.65 | % 27.81/7.65 | Combining equations (514,505) yields a new equation: % 27.81/7.65 | (185) overflow = tapOn % 27.81/7.65 | % 27.81/7.65 | Simplifying 185 yields: % 27.81/7.65 | (186) overflow = tapOn % 27.81/7.65 | % 27.81/7.65 | Equations (186) can reduce 49 to: % 27.81/7.65 | (178) $false % 27.81/7.65 | % 27.81/7.65 |-The branch is then unsatisfiable % 27.81/7.65 |-Branch two: % 27.81/7.65 | (518) all_295_2_93 = 0 & releasedAt(filling, n1) = 0 % 27.81/7.65 | % 27.81/7.65 | Applying alpha-rule on (518) yields: % 27.81/7.65 | (519) all_295_2_93 = 0 % 27.81/7.65 | (217) releasedAt(filling, n1) = 0 % 27.81/7.65 | % 27.81/7.65 | Using (217) and (165) yields: % 27.81/7.65 | (218) $false % 27.81/7.65 | % 27.81/7.65 |-The branch is then unsatisfiable % 27.81/7.65 |-Branch two: % 27.81/7.65 | (217) releasedAt(filling, n1) = 0 % 27.81/7.65 | (220) ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & releases(v0, filling, n0) = 0 & happens(v0, n0) = 0) | (v0 = 0 & releasedAt(filling, n0) = 0)) % 27.81/7.65 | % 27.81/7.65 | Instantiating (220) with all_188_0_97, all_188_1_98, all_188_2_99 yields: % 27.81/7.65 | (524) (all_188_0_97 = 0 & all_188_1_98 = 0 & releases(all_188_2_99, filling, n0) = 0 & happens(all_188_2_99, n0) = 0) | (all_188_2_99 = 0 & releasedAt(filling, n0) = 0) % 27.81/7.65 | % 27.81/7.65 +-Applying beta-rule and splitting (524), into two cases. % 27.81/7.65 |-Branch one: % 27.81/7.65 | (525) all_188_0_97 = 0 & all_188_1_98 = 0 & releases(all_188_2_99, filling, n0) = 0 & happens(all_188_2_99, n0) = 0 % 27.81/7.65 | % 27.81/7.65 | Applying alpha-rule on (525) yields: % 27.81/7.65 | (526) all_188_0_97 = 0 % 27.81/7.65 | (527) all_188_1_98 = 0 % 27.81/7.65 | (528) releases(all_188_2_99, filling, n0) = 0 % 27.81/7.65 | (529) happens(all_188_2_99, n0) = 0 % 27.81/7.65 | % 27.81/7.65 | Instantiating formula (45) with n0, filling, all_188_2_99 and discharging atoms releases(all_188_2_99, filling, n0) = 0, yields: % 27.81/7.65 | (530) ? [v0] : (all_188_2_99 = tapOn & waterLevel(v0) = filling) % 27.81/7.65 | % 27.81/7.65 | Instantiating (530) with all_303_0_111 yields: % 27.81/7.65 | (531) all_188_2_99 = tapOn & waterLevel(all_303_0_111) = filling % 27.81/7.65 | % 27.81/7.65 | Applying alpha-rule on (531) yields: % 27.81/7.65 | (532) all_188_2_99 = tapOn % 27.81/7.65 | (533) waterLevel(all_303_0_111) = filling % 27.81/7.65 | % 27.81/7.65 | Instantiating formula (20) with all_303_0_111 and discharging atoms waterLevel(all_303_0_111) = filling, yields: % 27.81/7.65 | (218) $false % 27.81/7.65 | % 27.81/7.65 |-The branch is then unsatisfiable % 27.81/7.65 |-Branch two: % 27.81/7.65 | (535) all_188_2_99 = 0 & releasedAt(filling, n0) = 0 % 27.81/7.65 | % 27.81/7.65 | Applying alpha-rule on (535) yields: % 27.81/7.65 | (536) all_188_2_99 = 0 % 27.81/7.65 | (234) releasedAt(filling, n0) = 0 % 27.81/7.65 | % 27.81/7.65 | Using (234) and (162) yields: % 27.81/7.65 | (218) $false % 27.81/7.65 | % 27.81/7.65 |-The branch is then unsatisfiable % 27.81/7.65 |-Branch two: % 27.81/7.65 | (234) releasedAt(filling, n0) = 0 % 27.81/7.65 | (414) all_0_1_1 = 0 % 27.81/7.65 | % 27.81/7.65 | Equations (414) can reduce 69 to: % 27.81/7.65 | (178) $false % 27.81/7.65 | % 27.81/7.65 |-The branch is then unsatisfiable % 27.81/7.65 |-Branch two: % 27.81/7.65 | (416) plus(n0, n0) = n2 % 27.81/7.65 | (177) n2 = n0 % 27.81/7.65 | % 27.81/7.65 +-Applying beta-rule and splitting (157), into two cases. % 27.81/7.65 |-Branch one: % 27.81/7.65 | (166) all_26_0_8 = 0 & all_26_1_9 = 0 & releases(all_26_2_10, filling, n2) = 0 & happens(all_26_2_10, n2) = 0 % 27.81/7.65 | % 27.81/7.65 | Applying alpha-rule on (166) yields: % 27.81/7.65 | (167) all_26_0_8 = 0 % 27.81/7.65 | (168) all_26_1_9 = 0 % 27.81/7.65 | (169) releases(all_26_2_10, filling, n2) = 0 % 27.81/7.65 | (170) happens(all_26_2_10, n2) = 0 % 27.81/7.65 | % 27.81/7.65 | From (177) and (169) follows: % 27.81/7.65 | (549) releases(all_26_2_10, filling, n0) = 0 % 27.81/7.65 | % 27.81/7.65 | Instantiating formula (45) with n0, filling, all_26_2_10 and discharging atoms releases(all_26_2_10, filling, n0) = 0, yields: % 27.81/7.65 | (172) ? [v0] : (all_26_2_10 = tapOn & waterLevel(v0) = filling) % 27.81/7.65 | % 27.81/7.65 | Instantiating (172) with all_312_0_200 yields: % 27.81/7.65 | (551) all_26_2_10 = tapOn & waterLevel(all_312_0_200) = filling % 27.81/7.65 | % 27.81/7.65 | Applying alpha-rule on (551) yields: % 27.81/7.65 | (175) all_26_2_10 = tapOn % 27.81/7.65 | (553) waterLevel(all_312_0_200) = filling % 27.81/7.65 | % 27.81/7.65 | Instantiating formula (20) with all_312_0_200 and discharging atoms waterLevel(all_312_0_200) = filling, yields: % 27.81/7.65 | (218) $false % 27.81/7.65 | % 27.81/7.65 |-The branch is then unsatisfiable % 27.81/7.65 |-Branch two: % 27.81/7.65 | (188) all_26_2_10 = 0 & releasedAt(filling, n2) = 0 % 27.81/7.65 | % 27.81/7.65 | Applying alpha-rule on (188) yields: % 27.81/7.65 | (189) all_26_2_10 = 0 % 27.81/7.65 | (190) releasedAt(filling, n2) = 0 % 27.81/7.65 | % 27.81/7.65 | From (177) and (190) follows: % 27.81/7.65 | (234) releasedAt(filling, n0) = 0 % 27.81/7.65 | % 27.81/7.65 +-Applying beta-rule and splitting (109), into two cases. % 27.81/7.65 |-Branch one: % 27.81/7.65 | (162) ~ (releasedAt(filling, n0) = 0) % 27.81/7.65 | % 27.81/7.65 | Using (234) and (162) yields: % 27.81/7.65 | (218) $false % 27.81/7.65 | % 27.81/7.65 |-The branch is then unsatisfiable % 27.81/7.65 |-Branch two: % 27.81/7.65 | (234) releasedAt(filling, n0) = 0 % 27.81/7.65 | (414) all_0_1_1 = 0 % 27.81/7.65 | % 27.81/7.65 | Equations (414) can reduce 69 to: % 27.81/7.65 | (178) $false % 27.81/7.65 | % 27.81/7.65 |-The branch is then unsatisfiable % 27.81/7.65 |-Branch two: % 27.81/7.65 | (236) plus(n0, n2) = n3 % 27.81/7.65 | (237) n2 = n3 % 27.81/7.65 | % 27.81/7.65 | From (237)(237) and (76) follows: % 27.81/7.65 | (238) plus(n3, n3) = n4 % 27.81/7.65 | % 27.81/7.65 | From (237) and (126) follows: % 27.81/7.65 | (240) plus(n3, n3) = n5 % 27.81/7.65 | % 27.81/7.65 | From (237) and (25) follows: % 27.81/7.65 | (248) plus(n1, n3) = n3 % 27.81/7.65 | % 27.81/7.65 +-Applying beta-rule and splitting (110), into two cases. % 27.81/7.65 |-Branch one: % 27.81/7.65 | (249) ~ (plus(n3, n3) = n5) % 27.81/7.65 | % 27.81/7.65 | Using (240) and (249) yields: % 27.81/7.65 | (218) $false % 27.81/7.65 | % 27.81/7.65 |-The branch is then unsatisfiable % 27.81/7.65 |-Branch two: % 27.81/7.65 | (240) plus(n3, n3) = n5 % 27.81/7.65 | (252) n5 = n4 | ~ (plus(n3, n3) = n4) % 27.81/7.65 | % 27.81/7.65 +-Applying beta-rule and splitting (252), into two cases. % 27.81/7.65 |-Branch one: % 27.81/7.65 | (258) ~ (plus(n3, n3) = n4) % 27.81/7.65 | % 27.81/7.65 | Using (238) and (258) yields: % 27.81/7.65 | (218) $false % 27.81/7.65 | % 27.81/7.65 |-The branch is then unsatisfiable % 27.81/7.65 |-Branch two: % 27.81/7.65 | (238) plus(n3, n3) = n4 % 27.81/7.65 | (262) n5 = n4 % 27.81/7.65 | % 27.81/7.65 | From (262) and (240) follows: % 27.81/7.65 | (238) plus(n3, n3) = n4 % 27.81/7.66 | % 27.81/7.66 +-Applying beta-rule and splitting (115), into two cases. % 27.81/7.66 |-Branch one: % 27.81/7.66 | (285) ~ (plus(n1, n3) = n3) % 27.81/7.66 | % 27.81/7.66 | Using (248) and (285) yields: % 27.81/7.66 | (218) $false % 27.81/7.66 | % 27.81/7.66 |-The branch is then unsatisfiable % 27.81/7.66 |-Branch two: % 27.81/7.66 | (248) plus(n1, n3) = n3 % 27.81/7.66 | (246) n4 = n3 % 27.81/7.66 | % 27.81/7.66 | Combining equations (246,262) yields a new equation: % 27.81/7.66 | (263) n5 = n3 % 27.81/7.66 | % 27.81/7.66 | From (246) and (238) follows: % 27.81/7.66 | (247) plus(n3, n3) = n3 % 27.81/7.66 | % 27.81/7.66 +-Applying beta-rule and splitting (111), into two cases. % 27.81/7.66 |-Branch one: % 27.81/7.66 | (249) ~ (plus(n3, n3) = n5) % 27.81/7.66 | % 27.81/7.66 | From (263) and (249) follows: % 27.81/7.66 | (259) ~ (plus(n3, n3) = n3) % 27.81/7.66 | % 27.81/7.66 | Using (247) and (259) yields: % 27.81/7.66 | (218) $false % 27.81/7.66 | % 27.81/7.66 |-The branch is then unsatisfiable % 27.81/7.66 |-Branch two: % 27.81/7.66 | (240) plus(n3, n3) = n5 % 27.81/7.66 | (269) n6 = n5 % 27.81/7.66 | % 27.81/7.66 | Combining equations (269,459) yields a new equation: % 27.81/7.66 | (589) n5 = n0 % 27.81/7.66 | % 27.81/7.66 | Simplifying 589 yields: % 27.81/7.66 | (590) n5 = n0 % 27.81/7.66 | % 27.81/7.66 | Combining equations (590,263) yields a new equation: % 27.81/7.66 | (411) n3 = n0 % 27.81/7.66 | % 27.81/7.66 | From (411) and (108) follows: % 27.81/7.66 | (234) releasedAt(filling, n0) = 0 % 27.81/7.66 | % 27.81/7.66 +-Applying beta-rule and splitting (109), into two cases. % 27.81/7.66 |-Branch one: % 27.81/7.66 | (162) ~ (releasedAt(filling, n0) = 0) % 27.81/7.66 | % 27.81/7.66 | Using (234) and (162) yields: % 27.81/7.66 | (218) $false % 27.81/7.66 | % 27.81/7.66 |-The branch is then unsatisfiable % 27.81/7.66 |-Branch two: % 27.81/7.66 | (234) releasedAt(filling, n0) = 0 % 27.81/7.66 | (414) all_0_1_1 = 0 % 27.81/7.66 | % 27.81/7.66 | Equations (414) can reduce 69 to: % 27.81/7.66 | (178) $false % 27.81/7.66 | % 27.81/7.66 |-The branch is then unsatisfiable % 27.81/7.66 % SZS output end Proof for theBenchmark % 27.81/7.66 % 27.81/7.66 7083ms %------------------------------------------------------------------------------