%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : CSR013+1 : TPTP v8.1.0. Bugfixed v3.1.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Fri Jul 15 23:24:13 EDT 2022 % Result : Theorem 6.83s 7.00s % Output : Refutation 6.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : CSR013+1 : TPTP v8.1.0. Bugfixed v3.1.0. % 0.07/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n023.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Fri Jun 10 08:35:37 EDT 2022 % 0.14/0.34 % CPUTime : % 6.83/7.00 % 6.83/7.00 SPASS V 3.9 % 6.83/7.00 SPASS beiseite: Proof found. % 6.83/7.00 % SZS status Theorem % 6.83/7.00 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 6.83/7.00 SPASS derived 19549 clauses, backtracked 1410 clauses, performed 56 splits and kept 5495 clauses. % 6.83/7.00 SPASS allocated 100783 KBytes. % 6.83/7.00 SPASS spent 0:00:06.63 on the problem. % 6.83/7.00 0:00:00.04 for the input. % 6.83/7.00 0:00:00.07 for the FLOTTER CNF translation. % 6.83/7.00 0:00:00.30 for inferences. % 6.83/7.00 0:00:00.10 for the backtracking. % 6.83/7.00 0:00:06.03 for the reduction. % 6.83/7.00 % 6.83/7.00 % 6.83/7.00 Here is a proof with depth 16, length 531 : % 6.83/7.00 % SZS output start Refutation % 6.83/7.00 1[0:Inp] || -> happens(skc1,n2)*. % 6.83/7.00 2[0:Inp] || -> terminates(skc1,filling,n2)*. % 6.83/7.00 3[0:Inp] || less(u,n0)* -> . % 6.83/7.00 4[0:Inp] || -> holdsAt(waterLevel(n0),n0)*. % 6.83/7.00 5[0:Inp] || holdsAt(filling,n0)* -> . % 6.83/7.00 6[0:Inp] || holdsAt(spilling,n0)* -> . % 6.83/7.00 7[0:Inp] || releasedAt(filling,n0)* -> . % 6.83/7.00 8[0:Inp] || releasedAt(spilling,n0)* -> . % 6.83/7.00 9[0:Inp] || equal(tapOff,tapOn)** -> . % 6.83/7.00 11[0:Inp] || equal(overflow,tapOn)** -> . % 6.83/7.00 14[0:Inp] || -> equal(plus(n0,n1),n1)**. % 6.83/7.00 15[0:Inp] || -> equal(plus(n0,n2),n2)**. % 6.83/7.00 17[0:Inp] || -> equal(plus(n1,n1),n2)**. % 6.83/7.00 18[0:Inp] || -> equal(plus(n1,n2),n3)**. % 6.83/7.00 19[0:Inp] || -> equal(plus(n1,n3),n4)**. % 6.83/7.00 20[0:Inp] || -> equal(plus(n2,n2),n4)**. % 6.83/7.00 21[0:Inp] || -> equal(plus(n2,n3),n5)**. % 6.83/7.00 23[0:Inp] || releasedAt(waterLevel(u),n0)* -> . % 6.83/7.00 25[0:Inp] || equal(waterLevel(u),spilling)** -> . % 6.83/7.00 26[0:Inp] || -> equal(plus(u,v),plus(v,u))*. % 6.83/7.00 27[0:Inp] || less(u,v)* -> less_or_equal(u,v). % 6.83/7.00 28[0:Inp] || equal(u,v) -> less_or_equal(u,v)*. % 6.83/7.00 29[0:Inp] || less(u,n1)* -> less_or_equal(u,n0). % 6.83/7.00 30[0:Inp] || less_or_equal(u,n0) -> less(u,n1)*. % 6.83/7.00 31[0:Inp] || less(u,n2)* -> less_or_equal(u,n1). % 6.83/7.00 32[0:Inp] || less_or_equal(u,n1) -> less(u,n2)*. % 6.83/7.00 33[0:Inp] || less(u,n3)* -> less_or_equal(u,n2). % 6.83/7.00 34[0:Inp] || less_or_equal(u,n2) -> less(u,n3)*. % 6.83/7.00 35[0:Inp] || less(u,n4)* -> less_or_equal(u,n3). % 6.83/7.00 36[0:Inp] || less_or_equal(u,n3) -> less(u,n4)*. % 6.83/7.00 38[0:Inp] || less_or_equal(u,n4) -> less(u,n5)*. % 6.83/7.00 40[0:Inp] || less_or_equal(u,n5) -> less(u,n6)*. % 6.83/7.00 42[0:Inp] || less_or_equal(u,n6) -> less(u,n7)*. % 6.83/7.00 44[0:Inp] || less_or_equal(u,n7) -> less(u,n8)*. % 6.83/7.00 45[0:Inp] || less(u,n9)* -> less_or_equal(u,n8). % 6.83/7.00 46[0:Inp] || less_or_equal(u,n8) -> less(u,n9)*. % 6.83/7.00 48[0:Inp] || SkP0(u,v)* -> equal(u,filling). % 6.83/7.00 49[0:Inp] || less(u,v)*+ less(v,u)* -> . % 6.83/7.00 50[0:Inp] || less(u,v)* equal(v,u) -> . % 6.83/7.00 53[0:Inp] || terminates(u,v,w)* -> equal(v,filling). % 6.83/7.00 54[0:Inp] || releases(u,v,w)* -> equal(u,tapOn). % 6.83/7.00 55[0:Inp] || -> less(u,v)* equal(v,u) less(v,u)*. % 6.83/7.00 57[0:Inp] || equal(waterLevel(u),waterLevel(v))* -> equal(u,v). % 6.83/7.00 58[0:Inp] || equal(u,v) -> equal(waterLevel(u),waterLevel(v))*. % 6.83/7.00 59[0:Inp] || less_or_equal(u,v) -> equal(u,v) less(u,v)*. % 6.83/7.00 60[0:Inp] || releases(u,v,w)* -> equal(waterLevel(skf21(v)),v). % 6.83/7.00 61[0:Inp] || happens(u,v)* -> equal(v,n0) equal(u,overflow). % 6.83/7.00 62[0:Inp] || happens(u,v)* -> equal(v,n0) holdsAt(filling,v). % 6.83/7.00 63[0:Inp] || happens(u,v)* -> equal(u,tapOn) equal(u,overflow). % 6.83/7.00 64[0:Inp] || happens(u,v)* -> equal(u,tapOn) holdsAt(filling,v). % 6.83/7.00 65[0:Inp] || stoppedIn(u,v,w)*+ -> less(skf11(u,w,x),w)*. % 6.83/7.00 66[0:Inp] || stoppedIn(u,v,w)*+ -> less(u,skf11(u,x,y))*. % 6.83/7.00 70[0:Inp] || SkP1(u,v,w)* -> holdsAt(waterLevel(skf20(u,w)),w)*. % 6.83/7.00 71[0:Inp] || SkP1(u,v,w)*+ -> equal(waterLevel(skf20(u,x)),u)**. % 6.83/7.00 72[0:Inp] || terminates(u,v,w)* -> equal(u,overflow) equal(u,tapOff). % 6.83/7.00 73[0:Inp] || happens(u,v)*+ -> equal(v,n0) holdsAt(waterLevel(n3),v)*. % 6.83/7.00 74[0:Inp] || happens(u,v)*+ -> equal(u,tapOn) holdsAt(waterLevel(n3),v)*. % 6.83/7.00 76[0:Inp] || equal(u,spilling) equal(v,overflow) -> initiates(v,u,w)*. % 6.83/7.00 78[0:Inp] || equal(u,filling) equal(v,overflow) -> terminates(v,u,w)*. % 6.83/7.00 79[0:Inp] || equal(u,tapOn) equal(v,waterLevel(w))*+ -> releases(u,v,x)*. % 6.83/7.00 80[0:Inp] || holdsAt(waterLevel(u),v) -> trajectory(filling,v,waterLevel(plus(u,w)),w)*. % 6.83/7.00 81[0:Inp] || holdsAt(waterLevel(u),v)*+ holdsAt(waterLevel(w),v)* -> equal(w,u)*. % 6.83/7.00 82[0:Inp] || stoppedIn(u,v,w) -> happens(skf12(w,u,v),skf11(u,w,v))*. % 6.83/7.00 85[0:Inp] || releasedAt(u,plus(v,n1))*+ -> releasedAt(u,v) happens(skf18(v,w),v)*. % 6.83/7.00 86[0:Inp] || happens(u,v) initiates(u,w,v)*+ -> holdsAt(w,plus(v,n1))*. % 6.83/7.00 88[0:Inp] || stoppedIn(u,v,w) -> terminates(skf12(w,u,v),v,skf11(u,w,v))*. % 6.83/7.00 90[0:Inp] || releasedAt(u,plus(v,n1)) -> releasedAt(u,v) releases(skf18(v,u),u,v)*. % 6.83/7.00 91[0:Inp] || happens(u,v) holdsAt(w,plus(v,n1))*+ terminates(u,w,v)* -> . % 6.83/7.00 92[0:Inp] || happens(u,v) releasedAt(w,plus(v,n1))*+ initiates(u,w,v)* -> . % 6.83/7.00 93[0:Inp] || happens(u,v) releasedAt(w,plus(v,n1))*+ terminates(u,w,v)* -> . % 6.83/7.00 94[0:Inp] || initiates(u,v,w) -> SkP0(v,u) equal(u,overflow) SkP1(v,u,w)*. % 6.83/7.00 95[0:Inp] || equal(u,overflow) holdsAt(filling,v) holdsAt(waterLevel(n3),v)*+ -> happens(u,v)*. % 6.83/7.00 96[0:Inp] || equal(u,overflow) equal(v,waterLevel(w))*+ holdsAt(waterLevel(w),x)* -> initiates(u,v,x)*. % 6.83/7.00 97[0:Inp] || equal(u,tapOff) equal(v,waterLevel(w))*+ holdsAt(waterLevel(w),x)* -> SkP1(v,u,x)*. % 6.83/7.00 98[0:Inp] || holdsAt(u,v)+ -> holdsAt(u,plus(v,n1)) releasedAt(u,plus(v,n1))* happens(skf15(v,w),v)*. % 6.83/7.00 99[0:Inp] || holdsAt(u,plus(v,n1))+ -> holdsAt(u,v) releasedAt(u,plus(v,n1))* happens(skf16(v,w),v)*. % 6.83/7.00 100[0:Inp] || holdsAt(u,plus(v,n1)) -> holdsAt(u,v) releasedAt(u,plus(v,n1)) initiates(skf16(v,u),u,v)*. % 6.83/7.00 101[0:Inp] || holdsAt(u,v) -> holdsAt(u,plus(v,n1)) releasedAt(u,plus(v,n1)) terminates(skf15(v,u),u,v)*. % 6.83/7.00 106[0:Inp] || less(u,v)* less(v,w)* happens(x,v) terminates(x,y,v)*+ -> stoppedIn(u,y,w)*. % 6.83/7.00 108[0:Inp] || happens(u,v) less(n0,w) initiates(u,x,v)* trajectory(x,v,y,w)*+ -> holdsAt(y,plus(v,w)) stoppedIn(v,x,plus(v,w))*. % 6.83/7.00 109[0:Rew:71.1,70.1] || SkP1(u,v,w)* -> holdsAt(u,w). % 6.83/7.00 112[0:Res:1.0,91.0] || terminates(skc1,u,n2) holdsAt(u,plus(n2,n1))* -> . % 6.83/7.00 113[0:Res:1.0,86.0] || initiates(skc1,u,n2) -> holdsAt(u,plus(n2,n1))*. % 6.83/7.00 116[0:Res:1.0,74.0] || -> holdsAt(waterLevel(n3),n2)* equal(skc1,tapOn). % 6.83/7.00 119[0:Res:1.0,63.0] || -> equal(skc1,overflow)** equal(skc1,tapOn). % 6.83/7.00 120[0:Res:1.0,64.0] || -> holdsAt(filling,n2)* equal(skc1,tapOn). % 6.83/7.00 121[0:Res:1.0,108.1] || trajectory(u,n2,v,w)* initiates(skc1,u,n2) less(n0,w) -> holdsAt(v,plus(n2,w)) stoppedIn(n2,u,plus(n2,w))*. % 6.83/7.00 123[0:Res:1.0,92.1] || initiates(skc1,u,n2) releasedAt(u,plus(n2,n1))* -> . % 6.83/7.00 125[0:Res:2.0,93.0] || happens(skc1,n2) releasedAt(filling,plus(n2,n1))* -> . % 6.83/7.00 126[0:Res:2.0,72.0] || -> equal(skc1,tapOff)** equal(skc1,overflow). % 6.83/7.00 128[0:Res:2.0,106.1] || happens(skc1,n2) less(n2,u) less(v,n2) -> stoppedIn(v,filling,u)*. % 6.83/7.00 129[0:Res:2.0,91.1] || happens(skc1,n2) holdsAt(filling,plus(n2,n1))* -> . % 6.83/7.00 131[0:Rew:119.1,126.0] || -> equal(tapOff,tapOn) equal(skc1,overflow)**. % 6.83/7.00 132[0:MRR:131.0,9.0] || -> equal(skc1,overflow)**. % 6.83/7.00 133[0:Rew:132.0,1.0] || -> happens(overflow,n2)*. % 6.83/7.00 135[0:Rew:132.0,120.1] || -> holdsAt(filling,n2)* equal(overflow,tapOn). % 6.83/7.00 136[0:MRR:135.1,11.0] || -> holdsAt(filling,n2)*. % 6.83/7.00 137[0:Rew:132.0,116.1] || -> holdsAt(waterLevel(n3),n2)* equal(overflow,tapOn). % 6.83/7.00 138[0:MRR:137.1,11.0] || -> holdsAt(waterLevel(n3),n2)*. % 6.83/7.00 139[0:Rew:18.0,113.1,26.0,113.1,132.0,113.0] || initiates(overflow,u,n2)* -> holdsAt(u,n3). % 6.83/7.00 141[0:Rew:18.0,125.1,26.0,125.1,132.0,125.0] || happens(overflow,n2)* releasedAt(filling,n3) -> . % 6.83/7.00 142[0:MRR:141.0,133.0] || releasedAt(filling,n3)* -> . % 6.83/7.00 143[0:Rew:18.0,129.1,26.0,129.1,132.0,129.0] || happens(overflow,n2)* holdsAt(filling,n3) -> . % 6.83/7.00 144[0:MRR:143.0,133.0] || holdsAt(filling,n3)* -> . % 6.83/7.00 145[0:Rew:18.0,112.1,26.0,112.1,132.0,112.0] || holdsAt(u,n3) terminates(overflow,u,n2)* -> . % 6.84/7.00 146[0:Rew:18.0,123.1,26.0,123.1,132.0,123.0] || releasedAt(u,n3) initiates(overflow,u,n2)* -> . % 6.84/7.00 148[0:Rew:132.0,128.0] || happens(overflow,n2) less(n2,u) less(v,n2) -> stoppedIn(v,filling,u)*. % 6.84/7.00 149[0:MRR:148.0,133.0] || less(u,n2) less(n2,v) -> stoppedIn(u,filling,v)*. % 6.84/7.00 155[0:Rew:132.0,121.1] || less(n0,u) initiates(overflow,v,n2) trajectory(v,n2,w,u)*+ -> holdsAt(w,plus(n2,u)) stoppedIn(n2,v,plus(n2,u))*. % 6.84/7.00 189[0:Res:44.1,27.0] || less_or_equal(u,n7) -> less_or_equal(u,n8)*. % 6.84/7.00 190[0:Res:42.1,27.0] || less_or_equal(u,n6) -> less_or_equal(u,n7)*. % 6.84/7.00 191[0:Res:40.1,27.0] || less_or_equal(u,n5) -> less_or_equal(u,n6)*. % 6.84/7.00 192[0:Res:38.1,27.0] || less_or_equal(u,n4) -> less_or_equal(u,n5)*. % 6.84/7.00 193[0:Res:36.1,27.0] || less_or_equal(u,n3) -> less_or_equal(u,n4)*. % 6.84/7.00 194[0:Res:34.1,27.0] || less_or_equal(u,n2) -> less_or_equal(u,n3)*. % 6.84/7.00 195[0:Res:32.1,27.0] || less_or_equal(u,n1) -> less_or_equal(u,n2)*. % 6.84/7.00 196[0:Res:30.1,27.0] || less_or_equal(u,n0) -> less_or_equal(u,n1)*. % 6.84/7.00 201[0:Res:38.1,50.0] || less_or_equal(u,n4)* equal(n5,u) -> . % 6.84/7.00 203[0:Res:34.1,50.0] || less_or_equal(u,n2)* equal(n3,u) -> . % 6.84/7.00 204[0:Res:32.1,50.0] || less_or_equal(u,n1)* equal(n2,u) -> . % 6.84/7.00 205[0:Res:30.1,50.0] || less_or_equal(u,n0)* equal(n1,u) -> . % 6.84/7.00 206[0:Res:46.1,49.0] || less_or_equal(u,n8) less(n9,u)* -> . % 6.84/7.00 211[0:Res:36.1,49.0] || less_or_equal(u,n3) less(n4,u)* -> . % 6.84/7.00 212[0:Res:34.1,49.0] || less_or_equal(u,n2) less(n3,u)* -> . % 6.84/7.00 213[0:Res:32.1,49.0] || less_or_equal(u,n1) less(n2,u)* -> . % 6.84/7.00 223[0:Res:193.1,201.0] || less_or_equal(u,n3)* equal(n5,u) -> . % 6.84/7.00 228[0:Res:195.1,203.0] || less_or_equal(u,n1)* equal(n3,u) -> . % 6.84/7.00 233[0:Res:46.1,206.1] || less_or_equal(n9,n8)* less_or_equal(n9,n8)* -> . % 6.84/7.00 242[0:Obv:233.0] || less_or_equal(n9,n8)* -> . % 6.84/7.00 244[0:Res:189.1,242.0] || less_or_equal(n9,n7)* -> . % 6.84/7.00 246[0:Res:190.1,244.0] || less_or_equal(n9,n6)* -> . % 6.84/7.00 248[0:Res:191.1,246.0] || less_or_equal(n9,n5)* -> . % 6.84/7.00 250[0:Res:192.1,248.0] || less_or_equal(n9,n4)* -> . % 6.84/7.00 252[0:Res:193.1,250.0] || less_or_equal(n9,n3)* -> . % 6.84/7.00 274[0:Res:194.1,252.0] || less_or_equal(n9,n2)* -> . % 6.84/7.00 276[0:Res:195.1,274.0] || less_or_equal(n9,n1)* -> . % 6.84/7.00 277[0:Res:28.1,274.0] || equal(n9,n2)** -> . % 6.84/7.00 287[0:Res:55.0,3.0] || -> equal(n0,u) less(n0,u)*. % 6.84/7.00 288[0:Res:55.0,45.0] || -> equal(n9,u) less(n9,u)* less_or_equal(u,n8). % 6.84/7.00 293[0:Res:55.0,35.0] || -> equal(n4,u) less(n4,u)* less_or_equal(u,n3). % 6.84/7.00 294[0:Res:55.0,33.0] || -> equal(n3,u) less(n3,u)* less_or_equal(u,n2). % 6.84/7.00 295[0:Res:55.0,31.0] || -> equal(n2,u) less(n2,u)* less_or_equal(u,n1). % 6.84/7.00 296[0:Res:55.0,29.0] || -> equal(n1,u) less(n1,u)* less_or_equal(u,n0). % 6.84/7.00 328[0:Res:287.1,27.0] || -> equal(n0,u) less_or_equal(n0,u)*. % 6.84/7.00 330[0:MRR:328.0,28.0] || -> less_or_equal(n0,u)*. % 6.84/7.00 337[0:Res:330.0,203.0] || equal(n3,n0)** -> . % 6.84/7.00 338[0:Res:330.0,204.0] || equal(n2,n0)** -> . % 6.84/7.00 339[0:Res:330.0,205.0] || equal(n1,n0)** -> . % 6.84/7.00 371[0:Res:59.2,3.0] || less_or_equal(u,n0)* -> equal(u,n0). % 6.84/7.00 380[0:Res:59.2,29.0] || less_or_equal(u,n1)* -> equal(u,n1) less_or_equal(u,n0). % 6.84/7.00 381[0:Res:59.2,49.0] || less_or_equal(u,v) less(v,u)* -> equal(u,v). % 6.84/7.00 386[0:MRR:381.2,50.1] || less_or_equal(u,v) less(v,u)* -> . % 6.84/7.00 484[0:Res:36.1,211.1] || less_or_equal(n4,n3)* less_or_equal(n4,n3)* -> . % 6.84/7.00 491[0:Obv:484.0] || less_or_equal(n4,n3)* -> . % 6.84/7.00 493[0:Res:194.1,491.0] || less_or_equal(n4,n2)* -> . % 6.84/7.00 495[0:Res:195.1,493.0] || less_or_equal(n4,n1)* -> . % 6.84/7.00 496[0:Res:28.1,493.0] || equal(n4,n2)** -> . % 6.84/7.00 508[0:Res:34.1,212.1] || less_or_equal(n3,n2)* less_or_equal(n3,n2)* -> . % 6.84/7.00 514[0:Obv:508.0] || less_or_equal(n3,n2)* -> . % 6.84/7.00 518[0:Res:195.1,514.0] || less_or_equal(n3,n1)* -> . % 6.84/7.00 519[0:Res:28.1,514.0] || equal(n3,n2)** -> . % 6.84/7.00 520[0:Res:196.1,518.0] || less_or_equal(n3,n0)* -> . % 6.84/7.00 521[0:Res:28.1,518.0] || equal(n3,n1)** -> . % 6.84/7.00 523[0:Res:76.2,139.0] || equal(u,spilling) equal(overflow,overflow) -> holdsAt(u,n3)*. % 6.84/7.00 524[0:Obv:523.1] || equal(u,spilling) -> holdsAt(u,n3)*. % 6.84/7.00 533[0:Res:32.1,213.1] || less_or_equal(n2,n1)* less_or_equal(n2,n1)* -> . % 6.84/7.00 538[0:Obv:533.0] || less_or_equal(n2,n1)* -> . % 6.84/7.00 540[0:Res:196.1,538.0] || less_or_equal(n2,n0)* -> . % 6.84/7.00 541[0:Res:28.1,538.0] || equal(n2,n1)** -> . % 6.84/7.00 548[0:SpR:15.0,80.1] || holdsAt(waterLevel(n0),u) -> trajectory(filling,u,waterLevel(n2),n2)*. % 6.84/7.00 550[0:SpR:14.0,80.1] || holdsAt(waterLevel(n0),u) -> trajectory(filling,u,waterLevel(n1),n1)*. % 6.84/7.00 552[0:SpR:26.0,80.1] || holdsAt(waterLevel(u),v) -> trajectory(filling,v,waterLevel(plus(w,u)),w)*. % 6.84/7.00 574[0:Res:138.0,81.0] || holdsAt(waterLevel(u),n2)* -> equal(u,n3). % 6.84/7.00 585[0:EqR:79.1] || equal(u,tapOn) -> releases(u,waterLevel(v),w)*. % 6.84/7.00 599[0:Res:28.1,223.0] || equal(u,n3) equal(n5,u)* -> . % 6.84/7.00 606[0:SpL:17.0,85.0] || releasedAt(u,n2)*+ -> releasedAt(u,n1) happens(skf18(n1,v),n1)*. % 6.84/7.00 607[0:SpL:14.0,85.0] || releasedAt(u,n1)*+ -> releasedAt(u,n0) happens(skf18(n0,v),n0)*. % 6.84/7.00 608[0:SpL:26.0,85.0] || releasedAt(u,plus(n1,v))*+ -> releasedAt(u,v) happens(skf18(v,w),v)*. % 6.84/7.00 610[0:Res:196.1,228.0] || less_or_equal(u,n0)* equal(n3,u) -> . % 6.84/7.00 635[0:Res:76.2,86.1] || equal(u,spilling)+ equal(v,overflow) happens(v,w)* -> holdsAt(u,plus(w,n1))*. % 6.84/7.00 734[0:Res:82.1,63.0] || stoppedIn(u,v,w) -> equal(skf12(w,u,v),tapOn) equal(skf12(w,u,v),overflow)**. % 6.84/7.00 761[0:SpL:17.0,91.1] || happens(u,n1) holdsAt(v,n2) terminates(u,v,n1)* -> . % 6.84/7.00 781[0:Res:28.1,610.0] || equal(u,n0) equal(n3,u)* -> . % 6.84/7.00 785[0:Res:90.2,54.0] || releasedAt(u,plus(v,n1))* -> releasedAt(u,v) equal(skf18(v,u),tapOn). % 6.84/7.00 787[0:Rew:785.2,90.2] || releasedAt(u,plus(v,n1))* -> releasedAt(u,v) releases(tapOn,u,v). % 6.84/7.00 797[0:SpL:14.0,787.0] || releasedAt(u,n1) -> releasedAt(u,n0) releases(tapOn,u,n0)*. % 6.84/7.00 810[0:Res:94.3,109.0] || initiates(u,v,w)* -> SkP0(v,u) equal(u,overflow) holdsAt(v,w). % 6.84/7.00 819[0:Res:88.1,72.0] || stoppedIn(u,v,w) -> equal(skf12(w,u,v),overflow) equal(skf12(w,u,v),tapOff)**. % 6.84/7.00 821[0:Rew:734.1,819.2] || stoppedIn(u,v,w) -> equal(skf12(w,u,v),overflow)** equal(tapOff,tapOn). % 6.84/7.00 822[0:MRR:821.2,9.0] || stoppedIn(u,v,w) -> equal(skf12(w,u,v),overflow)**. % 6.84/7.00 823[0:Rew:822.1,82.1] || stoppedIn(u,v,w) -> happens(overflow,skf11(u,w,v))*. % 6.84/7.00 824[0:Rew:822.1,88.1] || stoppedIn(u,v,w) -> terminates(overflow,v,skf11(u,w,v))*. % 6.84/7.00 890[0:EqR:97.1] || equal(u,tapOff) holdsAt(waterLevel(v),w) -> SkP1(waterLevel(v),u,w)*. % 6.84/7.00 900[0:EqR:96.1] || equal(u,overflow) holdsAt(waterLevel(v),w) -> initiates(u,waterLevel(v),w)*. % 6.84/7.00 913[0:Res:4.0,98.0] || -> holdsAt(waterLevel(n0),plus(n0,n1)) releasedAt(waterLevel(n0),plus(n0,n1))* happens(skf15(n0,u),n0)*. % 6.84/7.00 918[0:Rew:14.0,913.1,14.0,913.0] || -> holdsAt(waterLevel(n0),n1) releasedAt(waterLevel(n0),n1) happens(skf15(n0,u),n0)*. % 6.84/7.00 932[0:SpL:17.0,99.0] || holdsAt(u,n2) -> holdsAt(u,n1) releasedAt(u,plus(n1,n1))* happens(skf16(n1,v),n1)*. % 6.84/7.00 933[0:SpL:14.0,99.0] || holdsAt(u,n1) -> holdsAt(u,n0) releasedAt(u,plus(n0,n1))* happens(skf16(n0,v),n0)*. % 6.84/7.00 934[0:SpL:26.0,99.0] || holdsAt(u,plus(n1,v))+ -> holdsAt(u,v) releasedAt(u,plus(v,n1))* happens(skf16(v,w),v)*. % 6.84/7.00 936[0:Rew:17.0,932.2] || holdsAt(u,n2)+ -> holdsAt(u,n1) releasedAt(u,n2)* happens(skf16(n1,v),n1)*. % 6.84/7.00 937[0:Rew:14.0,933.2] || holdsAt(u,n1)+ -> holdsAt(u,n0) releasedAt(u,n1)* happens(skf16(n0,v),n0)*. % 6.84/7.00 947[0:Res:101.3,53.0] || holdsAt(u,v) -> holdsAt(u,plus(v,n1)) releasedAt(u,plus(v,n1))* equal(u,filling). % 6.84/7.00 965[0:Res:59.2,386.1] || less_or_equal(u,v)*+ less_or_equal(v,u)* -> equal(u,v). % 6.84/7.00 977[0:Res:78.2,145.1] || equal(u,filling) equal(overflow,overflow) holdsAt(u,n3)* -> . % 6.84/7.00 978[0:Obv:977.1] || equal(u,filling) holdsAt(u,n3)* -> . % 6.84/7.00 979[0:Res:524.1,978.1] || equal(u,spilling)* equal(u,filling) -> . % 6.84/7.00 987[0:Res:76.2,146.1] || equal(u,spilling) equal(overflow,overflow) releasedAt(u,n3)* -> . % 6.84/7.00 989[0:Obv:987.1] || equal(u,spilling) releasedAt(u,n3)* -> . % 6.84/7.00 999[0:Res:288.1,31.0] || -> equal(n9,n2) less_or_equal(n2,n8) less_or_equal(n9,n1)*. % 6.84/7.00 1012[0:MRR:999.0,999.2,277.0,276.0] || -> less_or_equal(n2,n8)*. % 6.84/7.00 1030[0:Res:824.1,106.3] || stoppedIn(u,v,w) less(x,skf11(u,w,v))* less(skf11(u,w,v),y)* happens(overflow,skf11(u,w,v))* -> stoppedIn(x,v,y)*. % 6.84/7.00 1034[0:MRR:1030.3,823.1] || stoppedIn(u,v,w) less(x,skf11(u,w,v))*+ less(skf11(u,w,v),y)* -> stoppedIn(x,v,y)*. % 6.84/7.00 1421[0:Res:293.1,31.0] || -> equal(n4,n2) less_or_equal(n2,n3) less_or_equal(n4,n1)*. % 6.84/7.00 1429[0:MRR:1421.0,1421.2,496.0,495.0] || -> less_or_equal(n2,n3)*. % 6.84/7.00 1466[0:Res:294.1,29.0] || -> equal(n3,n1) less_or_equal(n1,n2) less_or_equal(n3,n0)*. % 6.84/7.00 1469[0:Res:294.1,27.0] || -> equal(n3,u) less_or_equal(u,n2)* less_or_equal(n3,u)*. % 6.84/7.00 1473[0:MRR:1466.0,1466.2,521.0,520.0] || -> less_or_equal(n1,n2)*. % 6.84/7.00 1474[0:MRR:1469.0,28.0] || -> less_or_equal(u,n2)* less_or_equal(n3,u)*. % 6.84/7.00 1517[0:Res:295.1,27.0] || -> equal(n2,u) less_or_equal(u,n1)* less_or_equal(n2,u)*. % 6.84/7.00 1521[0:MRR:1517.0,28.0] || -> less_or_equal(u,n1)* less_or_equal(n2,u)*. % 6.84/7.00 1677[0:Res:296.1,27.0] || -> equal(n1,u) less_or_equal(u,n0)* less_or_equal(n1,u)*. % 6.84/7.00 1680[0:MRR:1677.0,28.0] || -> less_or_equal(u,n0)* less_or_equal(n1,u)*. % 6.84/7.00 1810[0:Res:585.1,60.0] || equal(u,tapOn)* -> equal(waterLevel(skf21(waterLevel(v))),waterLevel(v))**. % 6.84/7.00 1814[0:AED:9.0,1810.0] || -> equal(waterLevel(skf21(waterLevel(u))),waterLevel(u))**. % 6.84/7.00 3327[0:SpL:1814.0,57.0] || equal(waterLevel(u),waterLevel(v))*+ -> equal(skf21(waterLevel(u)),v)*. % 6.84/7.00 4395[0:Res:1521.0,380.0] || -> less_or_equal(n2,u)* equal(u,n1) less_or_equal(u,n0)*. % 6.84/7.00 5593[0:Res:548.1,108.3] || holdsAt(waterLevel(n0),u) happens(v,u) less(n0,n2) initiates(v,filling,u)* -> holdsAt(waterLevel(n2),plus(u,n2)) stoppedIn(u,filling,plus(u,n2))*. % 6.84/7.00 5607[0:Res:797.2,60.0] || releasedAt(u,n1) -> releasedAt(u,n0) equal(waterLevel(skf21(u)),u)**. % 6.84/7.00 5620[0:EqR:3327.0] || -> equal(skf21(waterLevel(u)),u)**. % 6.84/7.00 5687[0:Res:1521.0,965.0] || less_or_equal(n1,u) -> less_or_equal(n2,u)* equal(u,n1). % 6.84/7.00 5754[0:Res:4395.0,965.0] || less_or_equal(u,n2)* -> equal(u,n1) less_or_equal(u,n0) equal(n2,u). % 6.84/7.00 6007[1:Spt:606.0,606.1] || releasedAt(u,n2)* -> releasedAt(u,n1). % 6.84/7.00 6272[2:Spt:607.0,607.1] || releasedAt(u,n1)* -> releasedAt(u,n0). % 6.84/7.00 6328[0:Res:5687.1,965.0] || less_or_equal(n1,u)*+ less_or_equal(u,n2)* -> equal(u,n1) equal(n2,u). % 6.84/7.00 6335[0:Res:149.2,66.0] || less(u,n2)+ less(n2,v)* -> less(u,skf11(u,w,x))*. % 6.84/7.00 6336[0:Res:149.2,65.0] || less(u,n2) less(n2,v) -> less(skf11(u,v,w),v)*. % 6.84/7.00 6360[0:Res:918.2,64.0] || -> holdsAt(waterLevel(n0),n1) releasedAt(waterLevel(n0),n1)* equal(skf15(n0,u),tapOn)** holdsAt(filling,n0). % 6.84/7.00 6362[0:MRR:6360.3,5.0] || -> holdsAt(waterLevel(n0),n1) releasedAt(waterLevel(n0),n1)* equal(skf15(n0,u),tapOn)**. % 6.84/7.00 6363[0:Rew:6362.2,918.2] || -> holdsAt(waterLevel(n0),n1) releasedAt(waterLevel(n0),n1)* happens(tapOn,n0). % 6.84/7.00 6367[2:Res:6363.1,6272.0] || -> holdsAt(waterLevel(n0),n1) happens(tapOn,n0) releasedAt(waterLevel(n0),n0)*. % 6.84/7.00 6368[2:MRR:6367.2,23.0] || -> holdsAt(waterLevel(n0),n1)* happens(tapOn,n0). % 6.84/7.00 6369[2:SpR:58.1,6368.0] || equal(n0,u) -> holdsAt(waterLevel(u),n1)* happens(tapOn,n0). % 6.84/7.00 6374[3:Spt:6369.0,6369.1] || equal(n0,u) -> holdsAt(waterLevel(u),n1)*. % 6.84/7.00 6378[3:Res:6374.1,81.0] || equal(n0,u)* holdsAt(waterLevel(v),n1)*+ -> equal(v,u)*. % 6.84/7.00 6858[0:Res:78.2,761.2] || equal(u,filling)+ equal(v,overflow) happens(v,n1)* holdsAt(u,n2)* -> . % 6.84/7.00 7004[2:Res:6362.1,6272.0] || -> holdsAt(waterLevel(n0),n1) equal(skf15(n0,u),tapOn)** releasedAt(waterLevel(n0),n0)*. % 6.84/7.00 7005[2:MRR:7004.2,23.0] || -> holdsAt(waterLevel(n0),n1)* equal(skf15(n0,u),tapOn)**. % 6.84/7.00 7007[4:Spt:7005.0] || -> holdsAt(waterLevel(n0),n1)*. % 6.84/7.00 7011[4:Res:7007.0,98.0] || -> holdsAt(waterLevel(n0),plus(n1,n1)) releasedAt(waterLevel(n0),plus(n1,n1))* happens(skf15(n1,u),n1)*. % 6.84/7.00 7015[4:Rew:17.0,7011.1,17.0,7011.0] || -> holdsAt(waterLevel(n0),n2) releasedAt(waterLevel(n0),n2) happens(skf15(n1,u),n1)*. % 6.84/7.00 7017[4:Res:7015.2,73.0] || -> holdsAt(waterLevel(n0),n2) releasedAt(waterLevel(n0),n2)* equal(n1,n0) holdsAt(waterLevel(n3),n1). % 6.84/7.00 7021[4:Res:7015.2,62.0] || -> holdsAt(waterLevel(n0),n2) releasedAt(waterLevel(n0),n2)* equal(n1,n0) holdsAt(filling,n1). % 6.84/7.00 7022[4:MRR:7021.2,339.0] || -> holdsAt(waterLevel(n0),n2) releasedAt(waterLevel(n0),n2)* holdsAt(filling,n1). % 6.84/7.00 7023[4:MRR:7017.2,339.0] || -> holdsAt(waterLevel(n0),n2) releasedAt(waterLevel(n0),n2)* holdsAt(waterLevel(n3),n1). % 6.84/7.00 7032[5:Spt:7022.0] || -> holdsAt(waterLevel(n0),n2)*. % 6.84/7.00 7035[5:Res:7032.0,574.0] || -> equal(n3,n0)**. % 6.84/7.00 7040[5:MRR:7035.0,337.0] || -> . % 6.84/7.00 7042[5:Spt:7040.0,7022.0,7032.0] || holdsAt(waterLevel(n0),n2)* -> . % 6.84/7.00 7043[5:Spt:7040.0,7022.1,7022.2] || -> releasedAt(waterLevel(n0),n2)* holdsAt(filling,n1). % 6.84/7.00 7045[5:MRR:7023.0,7042.0] || -> releasedAt(waterLevel(n0),n2)* holdsAt(waterLevel(n3),n1). % 6.84/7.00 7047[6:Spt:7043.0] || -> releasedAt(waterLevel(n0),n2)*. % 6.84/7.00 7051[6:Res:7047.0,6007.0] || -> releasedAt(waterLevel(n0),n1)*. % 6.84/7.00 7056[6:Res:7051.0,6272.0] || -> releasedAt(waterLevel(n0),n0)*. % 6.84/7.00 7057[6:MRR:7056.0,23.0] || -> . % 6.84/7.00 7059[6:Spt:7057.0,7043.0,7047.0] || releasedAt(waterLevel(n0),n2)* -> . % 6.84/7.00 7060[6:Spt:7057.0,7043.1] || -> holdsAt(filling,n1)*. % 6.84/7.00 7062[6:MRR:7045.0,7059.0] || -> holdsAt(waterLevel(n3),n1)*. % 6.84/7.00 7080[6:Res:7062.0,6378.1] || equal(n0,u) -> equal(n3,u)*. % 6.84/7.00 7084[6:MRR:7080.1,781.1] || equal(n0,u)* -> . % 6.84/7.00 7085[6:UnC:7084.0,5620.0] || -> . % 6.84/7.00 7094[4:Spt:7085.0,7005.0,7007.0] || holdsAt(waterLevel(n0),n1)* -> . % 6.84/7.00 7095[4:Spt:7085.0,7005.1] || -> equal(skf15(n0,u),tapOn)**. % 6.84/7.00 7102[4:SpL:58.1,7094.0] || equal(u,n0) holdsAt(waterLevel(u),n1)* -> . % 6.84/7.00 7107[4:MRR:7102.1,6374.1] || equal(u,n0)* -> . % 6.84/7.00 7108[4:UnC:7107.0,5620.0] || -> . % 6.84/7.00 7109[3:Spt:7108.0,6369.2] || -> happens(tapOn,n0)*. % 6.84/7.00 7689[0:SpR:21.0,552.1] || holdsAt(waterLevel(n3),u) -> trajectory(filling,u,waterLevel(n5),n2)*. % 6.84/7.00 8507[0:Res:890.2,71.0] || equal(u,tapOff)* holdsAt(waterLevel(v),w)* -> equal(waterLevel(skf20(waterLevel(v),x)),waterLevel(v))**. % 6.84/7.00 8511[0:AED:9.0,8507.0] || holdsAt(waterLevel(u),v)*+ -> equal(waterLevel(skf20(waterLevel(u),w)),waterLevel(u))**. % 6.84/7.00 8524[0:Res:138.0,8511.0] || -> equal(waterLevel(skf20(waterLevel(n3),u)),waterLevel(n3))**. % 6.84/7.00 8537[0:SpR:8524.0,5620.0] || -> equal(skf20(waterLevel(n3),u),skf21(waterLevel(n3)))**. % 6.84/7.00 8562[0:Rew:5620.0,8537.0] || -> equal(skf20(waterLevel(n3),u),n3)**. % 6.84/7.00 8589[0:Res:900.2,146.1] || equal(overflow,overflow) holdsAt(waterLevel(u),n2) releasedAt(waterLevel(u),n3)* -> . % 6.84/7.00 8590[0:Res:900.2,139.0] || equal(overflow,overflow) holdsAt(waterLevel(u),n2) -> holdsAt(waterLevel(u),n3)*. % 6.84/7.00 8597[0:Obv:8590.0] || holdsAt(waterLevel(u),n2) -> holdsAt(waterLevel(u),n3)*. % 6.84/7.00 8598[0:Obv:8589.0] || holdsAt(waterLevel(u),n2) releasedAt(waterLevel(u),n3)* -> . % 6.84/7.00 8656[0:SpR:58.1,8597.1] || equal(u,v)* holdsAt(waterLevel(u),n2)*+ -> holdsAt(waterLevel(v),n3)*. % 6.84/7.00 8663[0:Res:8597.1,81.0] || holdsAt(waterLevel(u),n2)*+ holdsAt(waterLevel(v),n3)* -> equal(v,u)*. % 6.84/7.00 8668[0:SpL:58.1,8598.1] || equal(u,v)* holdsAt(waterLevel(u),n2)*+ releasedAt(waterLevel(v),n3)* -> . % 6.84/7.00 8677[0:SpL:19.0,608.0] || releasedAt(u,n4)*+ -> releasedAt(u,n3) happens(skf18(n3,v),n3)*. % 6.84/7.00 8714[0:Res:138.0,8656.1] || equal(n3,u) -> holdsAt(waterLevel(u),n3)*. % 6.84/7.00 8743[0:Res:138.0,8663.0] || holdsAt(waterLevel(u),n3)* -> equal(u,n3). % 6.84/7.00 8750[4:Spt:936.0,936.1,936.2] || holdsAt(u,n2) -> holdsAt(u,n1) releasedAt(u,n2)*. % 6.84/7.00 8752[4:Res:8750.2,6007.0] || holdsAt(u,n2) -> holdsAt(u,n1) releasedAt(u,n1)*. % 6.84/7.00 8755[4:Res:8752.2,6272.0] || holdsAt(u,n2) -> holdsAt(u,n1) releasedAt(u,n0)*. % 6.84/7.00 8758[4:Res:8755.2,7.0] || holdsAt(filling,n2)* -> holdsAt(filling,n1). % 6.84/7.00 8759[4:Res:8755.2,23.0] || holdsAt(waterLevel(u),n2)* -> holdsAt(waterLevel(u),n1). % 6.84/7.00 8761[4:MRR:8758.0,136.0] || -> holdsAt(filling,n1)*. % 6.84/7.00 8771[4:Res:138.0,8759.0] || -> holdsAt(waterLevel(n3),n1)*. % 6.84/7.00 8775[4:Res:8771.0,95.2] || equal(u,overflow) holdsAt(filling,n1) -> happens(u,n1)*. % 6.84/7.00 8780[4:MRR:8775.1,8761.0] || equal(u,overflow) -> happens(u,n1)*. % 6.84/7.00 8782[4:MRR:6858.2,8780.1] || equal(u,filling) equal(v,overflow)* holdsAt(u,n2)* -> . % 6.84/7.00 8786[4:AED:9.0,8782.1] || equal(u,filling) holdsAt(u,n2)* -> . % 6.84/7.00 8817[4:Res:136.0,8786.1] || equal(filling,filling)* -> . % 6.84/7.00 8820[4:Obv:8817.0] || -> . % 6.84/7.00 8821[4:Spt:8820.0,936.3] || -> happens(skf16(n1,u),n1)*. % 6.84/7.00 8823[4:Res:8821.0,73.0] || -> equal(n1,n0) holdsAt(waterLevel(n3),n1)*. % 6.84/7.00 8827[4:Res:8821.0,62.0] || -> equal(n1,n0) holdsAt(filling,n1)*. % 6.84/7.00 8828[4:MRR:8827.0,339.0] || -> holdsAt(filling,n1)*. % 6.84/7.00 8829[4:MRR:8823.0,339.0] || -> holdsAt(waterLevel(n3),n1)*. % 6.84/7.00 8846[4:Res:8829.0,95.2] || equal(u,overflow) holdsAt(filling,n1) -> happens(u,n1)*. % 6.84/7.00 8851[4:MRR:8846.1,8828.0] || equal(u,overflow) -> happens(u,n1)*. % 6.84/7.00 8853[4:MRR:6858.2,8851.1] || equal(u,filling) equal(v,overflow)* holdsAt(u,n2)* -> . % 6.84/7.00 8857[4:AED:9.0,8853.1] || equal(u,filling) holdsAt(u,n2)* -> . % 6.84/7.00 8891[4:Res:136.0,8857.1] || equal(filling,filling)* -> . % 6.84/7.00 8894[4:Obv:8891.0] || -> . % 6.84/7.00 8895[2:Spt:8894.0,607.2] || -> happens(skf18(n0,u),n0)*. % 6.84/7.00 8902[2:Res:8895.0,64.0] || -> equal(skf18(n0,u),tapOn)** holdsAt(filling,n0). % 6.84/7.00 8904[2:MRR:8902.1,5.0] || -> equal(skf18(n0,u),tapOn)**. % 6.84/7.00 8905[2:Rew:8904.0,8895.0] || -> happens(tapOn,n0)*. % 6.84/7.00 8922[3:Spt:937.0,937.1,937.2] || holdsAt(u,n1) -> holdsAt(u,n0) releasedAt(u,n1)*. % 6.84/7.00 8932[4:Spt:936.0,936.1,936.2] || holdsAt(u,n2) -> holdsAt(u,n1) releasedAt(u,n2)*. % 6.84/7.00 8934[4:Res:8932.2,6007.0] || holdsAt(u,n2) -> holdsAt(u,n1) releasedAt(u,n1)*. % 6.84/7.00 8962[0:SpR:5607.2,8597.1] || releasedAt(u,n1) holdsAt(waterLevel(skf21(u)),n2)* -> releasedAt(u,n0) holdsAt(u,n3). % 6.84/7.00 8971[0:SpL:5607.2,25.0] || releasedAt(u,n1)* equal(u,spilling) -> releasedAt(u,n0). % 6.84/7.00 8980[0:SpL:5607.2,574.0] || releasedAt(u,n1)* holdsAt(u,n2) -> releasedAt(u,n0) equal(skf21(u),n3). % 6.84/7.00 8995[0:Rew:5607.2,8962.1] || releasedAt(u,n1)* holdsAt(u,n2) -> releasedAt(u,n0) holdsAt(u,n3). % 6.84/7.00 9058[0:EqR:635.0] || equal(u,overflow)+ happens(u,v)* -> holdsAt(spilling,plus(v,n1))*. % 6.84/7.00 9071[0:EqR:9058.0] || happens(overflow,u) -> holdsAt(spilling,plus(u,n1))*. % 6.84/7.00 9074[0:SpR:26.0,947.2] || holdsAt(u,v) -> holdsAt(u,plus(v,n1)) releasedAt(u,plus(n1,v))* equal(u,filling). % 6.84/7.00 9091[0:SpR:17.0,9071.1] || happens(overflow,n1)* -> holdsAt(spilling,n2). % 6.84/7.00 9467[0:Res:138.0,8668.1] || equal(n3,u) releasedAt(waterLevel(u),n3)* -> . % 6.84/7.00 9483[4:Res:8934.2,8995.0] || holdsAt(u,n2) holdsAt(u,n2) -> holdsAt(u,n1) releasedAt(u,n0)* holdsAt(u,n3). % 6.84/7.00 9484[3:Res:8922.2,8995.0] || holdsAt(u,n1) holdsAt(u,n2) -> holdsAt(u,n0) releasedAt(u,n0)* holdsAt(u,n3). % 6.84/7.00 9485[4:Obv:9483.0] || holdsAt(u,n2) -> holdsAt(u,n1) releasedAt(u,n0)* holdsAt(u,n3). % 6.84/7.00 9486[4:MRR:9484.0,9485.1] || holdsAt(u,n2) -> holdsAt(u,n0) releasedAt(u,n0)* holdsAt(u,n3). % 6.84/7.00 9497[4:Res:9486.2,7.0] || holdsAt(filling,n2) -> holdsAt(filling,n0) holdsAt(filling,n3)*. % 6.84/7.00 9500[4:MRR:9497.0,9497.1,9497.2,136.0,5.0,144.0] || -> . % 6.84/7.00 9502[4:Spt:9500.0,936.3] || -> happens(skf16(n1,u),n1)*. % 6.84/7.00 9504[4:Res:9502.0,73.0] || -> equal(n1,n0) holdsAt(waterLevel(n3),n1)*. % 6.84/7.00 9508[4:Res:9502.0,62.0] || -> equal(n1,n0) holdsAt(filling,n1)*. % 6.84/7.00 9509[4:MRR:9508.0,339.0] || -> holdsAt(filling,n1)*. % 6.84/7.00 9510[4:MRR:9504.0,339.0] || -> holdsAt(waterLevel(n3),n1)*. % 6.84/7.00 9534[4:Res:9510.0,95.2] || equal(u,overflow) holdsAt(filling,n1) -> happens(u,n1)*. % 6.84/7.00 9540[4:MRR:9534.1,9509.0] || equal(u,overflow) -> happens(u,n1)*. % 6.84/7.00 9542[4:MRR:6858.2,9540.1] || equal(u,filling) equal(v,overflow)* holdsAt(u,n2)* -> . % 6.84/7.00 9546[4:AED:9.0,9542.1] || equal(u,filling) holdsAt(u,n2)* -> . % 6.84/7.00 9601[4:Res:136.0,9546.1] || equal(filling,filling)* -> . % 6.84/7.00 9605[4:Obv:9601.0] || -> . % 6.84/7.00 9606[3:Spt:9605.0,937.3] || -> happens(skf16(n0,u),n0)*. % 6.84/7.00 9611[3:Res:9606.0,64.0] || -> equal(skf16(n0,u),tapOn)** holdsAt(filling,n0). % 6.84/7.00 9613[3:MRR:9611.1,5.0] || -> equal(skf16(n0,u),tapOn)**. % 6.84/7.00 9615[3:SpR:9613.0,100.3] || holdsAt(u,plus(n0,n1)) -> holdsAt(u,n0) releasedAt(u,plus(n0,n1))* initiates(tapOn,u,n0). % 6.84/7.00 9617[3:Rew:14.0,9615.2,14.0,9615.0] || holdsAt(u,n1) -> holdsAt(u,n0) releasedAt(u,n1) initiates(tapOn,u,n0)*. % 6.84/7.00 9618[4:Spt:936.0,936.1,936.2] || holdsAt(u,n2) -> holdsAt(u,n1) releasedAt(u,n2)*. % 6.84/7.00 9620[4:Res:9618.2,6007.0] || holdsAt(u,n2) -> holdsAt(u,n1) releasedAt(u,n1)*. % 6.84/7.00 9624[4:Res:9620.2,8995.0] || holdsAt(u,n2) holdsAt(u,n2) -> holdsAt(u,n1) releasedAt(u,n0)* holdsAt(u,n3). % 6.84/7.00 9626[4:Res:9620.2,8971.0] || holdsAt(u,n2) equal(u,spilling) -> holdsAt(u,n1) releasedAt(u,n0)*. % 6.84/7.00 9628[4:Obv:9624.0] || holdsAt(u,n2) -> holdsAt(u,n1) releasedAt(u,n0)* holdsAt(u,n3). % 6.84/7.00 9636[0:SpL:19.0,934.0] || holdsAt(u,n4) -> holdsAt(u,n3) releasedAt(u,plus(n3,n1))* happens(skf16(n3,v),n3)*. % 6.84/7.00 9637[0:SpL:18.0,934.0] || holdsAt(u,n3) -> holdsAt(u,n2) releasedAt(u,plus(n2,n1))* happens(skf16(n2,v),n2)*. % 6.84/7.00 9644[0:Rew:19.0,9636.2,26.0,9636.2] || holdsAt(u,n4)+ -> holdsAt(u,n3) releasedAt(u,n4)* happens(skf16(n3,v),n3)*. % 6.84/7.00 9645[0:Rew:18.0,9637.2,26.0,9637.2] || holdsAt(u,n3)+ -> holdsAt(u,n2) releasedAt(u,n3)* happens(skf16(n2,v),n2)*. % 6.84/7.00 9685[5:Spt:8677.0,8677.1] || releasedAt(u,n4)* -> releasedAt(u,n3). % 6.84/7.00 9721[4:Res:9628.2,7.0] || holdsAt(filling,n2) -> holdsAt(filling,n1) holdsAt(filling,n3)*. % 6.84/7.00 9724[4:MRR:9721.0,9721.2,136.0,144.0] || -> holdsAt(filling,n1)*. % 6.84/7.00 9745[3:Res:9617.3,810.0] || holdsAt(u,n1) -> holdsAt(u,n0) releasedAt(u,n1) SkP0(u,tapOn)* equal(overflow,tapOn) holdsAt(u,n0). % 6.84/7.00 9752[3:Obv:9745.1] || holdsAt(u,n1) -> releasedAt(u,n1) SkP0(u,tapOn)* equal(overflow,tapOn) holdsAt(u,n0). % 6.84/7.00 9753[3:MRR:9752.3,11.0] || holdsAt(u,n1) -> releasedAt(u,n1) SkP0(u,tapOn)* holdsAt(u,n0). % 6.84/7.00 9761[3:Res:9753.2,48.0] || holdsAt(u,n1) -> releasedAt(u,n1)* holdsAt(u,n0) equal(u,filling). % 6.84/7.00 9765[3:Res:9761.1,8971.0] || holdsAt(u,n1) equal(u,spilling) -> holdsAt(u,n0) equal(u,filling) releasedAt(u,n0)*. % 6.84/7.00 9766[3:MRR:9765.3,979.1] || holdsAt(u,n1) equal(u,spilling) -> holdsAt(u,n0) releasedAt(u,n0)*. % 6.84/7.00 9774[4:Res:9626.3,8.0] || holdsAt(spilling,n2)* equal(spilling,spilling) -> holdsAt(spilling,n1). % 6.84/7.00 9778[4:Obv:9774.1] || holdsAt(spilling,n2)* -> holdsAt(spilling,n1). % 6.84/7.00 9797[3:Res:9766.3,8.0] || holdsAt(spilling,n1)* equal(spilling,spilling) -> holdsAt(spilling,n0). % 6.84/7.00 9801[3:Obv:9797.1] || holdsAt(spilling,n1)* -> holdsAt(spilling,n0). % 6.84/7.00 9802[3:MRR:9801.1,6.0] || holdsAt(spilling,n1)* -> . % 6.84/7.00 9804[4:MRR:9778.1,9802.0] || holdsAt(spilling,n2)* -> . % 6.84/7.00 9805[4:MRR:9091.1,9804.0] || happens(overflow,n1)* -> . % 6.84/7.00 9819[0:Res:287.1,1034.1] || stoppedIn(u,v,w) less(skf11(u,w,v),x)* -> equal(skf11(u,w,v),n0) stoppedIn(n0,v,x). % 6.84/7.00 10051[0:Res:548.1,155.2] || holdsAt(waterLevel(n0),n2) less(n0,n2) initiates(overflow,filling,n2) -> holdsAt(waterLevel(n2),plus(n2,n2)) stoppedIn(n2,filling,plus(n2,n2))*. % 6.84/7.00 10052[0:Res:7689.1,155.2] || holdsAt(waterLevel(n3),n2) less(n0,n2) initiates(overflow,filling,n2) -> holdsAt(waterLevel(n5),plus(n2,n2)) stoppedIn(n2,filling,plus(n2,n2))*. % 6.84/7.00 10054[0:Res:550.1,155.2] || holdsAt(waterLevel(n0),n2) less(n0,n1) initiates(overflow,filling,n2) -> holdsAt(waterLevel(n1),plus(n2,n1)) stoppedIn(n2,filling,plus(n2,n1))*. % 6.84/7.00 10064[0:Rew:18.0,10054.4,26.0,10054.4,18.0,10054.3,26.0,10054.3] || holdsAt(waterLevel(n0),n2) less(n0,n1) initiates(overflow,filling,n2)* -> holdsAt(waterLevel(n1),n3) stoppedIn(n2,filling,n3). % 6.84/7.00 10066[0:Rew:20.0,10052.4,20.0,10052.3] || holdsAt(waterLevel(n3),n2) less(n0,n2) initiates(overflow,filling,n2)* -> holdsAt(waterLevel(n5),n4) stoppedIn(n2,filling,n4). % 6.84/7.00 10067[0:MRR:10066.0,138.0] || less(n0,n2) initiates(overflow,filling,n2)* -> holdsAt(waterLevel(n5),n4) stoppedIn(n2,filling,n4). % 6.84/7.00 10068[0:Rew:20.0,10051.4,20.0,10051.3] || holdsAt(waterLevel(n0),n2) less(n0,n2) initiates(overflow,filling,n2)* -> holdsAt(waterLevel(n2),n4) stoppedIn(n2,filling,n4). % 6.84/7.00 10247[0:Res:55.0,6335.0] || less(n2,u)*+ -> equal(n2,v) less(n2,v) less(v,skf11(v,w,x))*. % 6.84/7.00 10250[0:Res:287.1,6335.0] || less(n2,u)* -> equal(n2,n0) less(n0,skf11(n0,v,w))*. % 6.84/7.00 10258[0:Res:296.1,6335.0] || less(n2,u)* -> equal(n2,n1) less_or_equal(n2,n0) less(n1,skf11(n1,v,w))*. % 6.84/7.00 10259[0:MRR:10250.1,338.0] || less(n2,u)*+ -> less(n0,skf11(n0,v,w))*. % 6.84/7.00 10260[0:MRR:10258.1,10258.2,541.0,540.0] || less(n2,u)*+ -> less(n1,skf11(n1,v,w))*. % 6.84/7.00 10279[0:Res:46.1,10259.0] || less_or_equal(n2,n8) -> less(n0,skf11(n0,u,v))*. % 6.84/7.00 10293[0:MRR:10279.0,1012.0] || -> less(n0,skf11(n0,u,v))*. % 6.84/7.00 10297[0:Res:10293.0,386.1] || less_or_equal(skf11(n0,u,v),n0)* -> . % 6.84/7.00 10301[0:Res:1680.0,10297.0] || -> less_or_equal(n1,skf11(n0,u,v))*. % 6.84/7.00 10329[0:Res:10301.0,965.0] || less_or_equal(skf11(n0,u,v),n1)* -> equal(skf11(n0,u,v),n1). % 6.84/7.00 10332[0:Res:46.1,10260.0] || less_or_equal(n2,n8) -> less(n1,skf11(n1,u,v))*. % 6.84/7.00 10346[0:MRR:10332.0,1012.0] || -> less(n1,skf11(n1,u,v))*. % 6.84/7.00 10348[0:Res:10346.0,50.0] || equal(skf11(n1,u,v),n1)** -> . % 6.84/7.00 10349[0:Res:10346.0,27.0] || -> less_or_equal(n1,skf11(n1,u,v))*. % 6.84/7.00 10354[0:Res:10349.0,6328.0] || less_or_equal(skf11(n1,u,v),n2)* -> equal(skf11(n1,u,v),n1) equal(skf11(n1,u,v),n2). % 6.84/7.00 10356[0:MRR:10354.1,10348.0] || less_or_equal(skf11(n1,u,v),n2)* -> equal(skf11(n1,u,v),n2). % 6.84/7.00 10439[0:Res:6336.2,33.0] || less(u,n2) less(n2,n3) -> less_or_equal(skf11(u,n3,v),n2)*. % 6.84/7.00 10442[0:Res:6336.2,29.0] || less(u,n2) less(n2,n1) -> less_or_equal(skf11(u,n1,v),n0)*. % 6.84/7.00 10606[0:Res:10439.2,10356.0] || less(n1,n2) less(n2,n3) -> equal(skf11(n1,n3,u),n2)**. % 6.84/7.00 10684[0:Res:10442.2,371.0] || less(u,n2) less(n2,n1) -> equal(skf11(u,n1,v),n0)**. % 6.84/7.00 10776[0:SpR:10684.2,6336.2] || less(u,n2)* less(n2,n1)* less(u,n2)* less(n2,n1)* -> less(n0,n1). % 6.84/7.00 10798[0:Obv:10776.1] || less(u,n2)*+ less(n2,n1)* -> less(n0,n1). % 6.84/7.00 10805[0:Res:287.1,10798.0] || less(n2,n1)* -> equal(n2,n0) less(n0,n1). % 6.84/7.00 10816[0:MRR:10805.1,338.0] || less(n2,n1)* -> less(n0,n1). % 6.84/7.00 10821[0:Res:55.0,10816.0] || -> equal(n2,n1) less(n1,n2)* less(n0,n1). % 6.84/7.00 10824[0:MRR:10821.0,541.0] || -> less(n1,n2)* less(n0,n1). % 6.84/7.00 10825[6:Spt:10824.0] || -> less(n1,n2)*. % 6.84/7.00 10826[6:MRR:10606.0,10825.0] || less(n2,n3) -> equal(skf11(n1,n3,u),n2)**. % 6.84/7.00 11689[7:Spt:9645.0,9645.1,9645.2] || holdsAt(u,n3) -> holdsAt(u,n2) releasedAt(u,n3)*. % 6.84/7.00 11692[7:Res:11689.2,989.1] || holdsAt(u,n3)* equal(u,spilling) -> holdsAt(u,n2). % 6.84/7.00 11700[7:MRR:11692.0,524.1] || equal(u,spilling) -> holdsAt(u,n2)*. % 6.84/7.00 11721[7:Res:11700.1,9804.0] || equal(spilling,spilling)* -> . % 6.84/7.00 11722[7:Obv:11721.0] || -> . % 6.84/7.00 11725[7:Spt:11722.0,9645.3] || -> happens(skf16(n2,u),n2)*. % 6.84/7.00 11753[8:Spt:9644.0,9644.1,9644.2] || holdsAt(u,n4) -> holdsAt(u,n3) releasedAt(u,n4)*. % 6.84/7.00 11757[8:Res:11753.2,9685.0] || holdsAt(u,n4) -> holdsAt(u,n3) releasedAt(u,n3)*. % 6.84/7.00 11767[8:Res:11757.2,142.0] || holdsAt(filling,n4)* -> holdsAt(filling,n3). % 6.84/7.00 11777[8:MRR:11767.1,144.0] || holdsAt(filling,n4)* -> . % 6.84/7.00 11852[0:EqR:6858.0] || equal(u,overflow) happens(u,n1)* holdsAt(filling,n2) -> . % 6.84/7.00 11853[0:MRR:11852.2,136.0] || equal(u,overflow) happens(u,n1)* -> . % 6.84/7.00 12194[0:SpR:19.0,9074.2] || holdsAt(u,n3) -> holdsAt(u,plus(n3,n1))* releasedAt(u,n4) equal(u,filling). % 6.84/7.00 12214[0:Rew:19.0,12194.1,26.0,12194.1] || holdsAt(u,n3) -> holdsAt(u,n4) releasedAt(u,n4)* equal(u,filling). % 6.84/7.00 12215[0:MRR:12214.3,978.0] || holdsAt(u,n3) -> holdsAt(u,n4) releasedAt(u,n4)*. % 6.84/7.00 12226[5:Res:12215.2,9685.0] || holdsAt(u,n3) -> holdsAt(u,n4) releasedAt(u,n3)*. % 6.84/7.00 12241[5:Res:12226.2,8598.1] || holdsAt(waterLevel(u),n3) holdsAt(waterLevel(u),n2) -> holdsAt(waterLevel(u),n4)*. % 6.84/7.00 12242[5:Res:12226.2,9467.1] || holdsAt(waterLevel(u),n3) equal(n3,u) -> holdsAt(waterLevel(u),n4)*. % 6.84/7.00 12243[5:MRR:12242.0,8714.1] || equal(n3,u) -> holdsAt(waterLevel(u),n4)*. % 6.84/7.00 12244[5:MRR:12241.0,8597.1] || holdsAt(waterLevel(u),n2) -> holdsAt(waterLevel(u),n4)*. % 6.84/7.00 12251[5:SpR:5607.2,12243.1] || releasedAt(u,n1)* equal(skf21(u),n3) -> releasedAt(u,n0) holdsAt(u,n4). % 6.84/7.00 12256[5:Res:12243.1,81.0] || equal(n3,u)* holdsAt(waterLevel(v),n4)*+ -> equal(v,u)*. % 6.84/7.00 12274[5:Res:12244.1,81.0] || holdsAt(waterLevel(u),n2)*+ holdsAt(waterLevel(v),n4)* -> equal(v,u)*. % 6.84/7.00 12423[5:Res:138.0,12274.0] || holdsAt(waterLevel(u),n4)* -> equal(u,n3). % 6.84/7.00 14126[9:Spt:10064.3] || -> holdsAt(waterLevel(n1),n3)*. % 6.84/7.00 14140[9:Res:14126.0,8743.0] || -> equal(n3,n1)**. % 6.84/7.00 14145[9:MRR:14140.0,521.0] || -> . % 6.84/7.00 14151[9:Spt:14145.0,10064.3,14126.0] || holdsAt(waterLevel(n1),n3)* -> . % 6.84/7.00 14152[9:Spt:14145.0,10064.0,10064.1,10064.2,10064.4] || holdsAt(waterLevel(n0),n2) less(n0,n1) initiates(overflow,filling,n2)* -> stoppedIn(n2,filling,n3). % 6.84/7.00 14210[10:Spt:10068.3] || -> holdsAt(waterLevel(n2),n4)*. % 6.84/7.00 14228[10:Res:14210.0,12423.0] || -> equal(n3,n2)**. % 6.84/7.00 14229[10:MRR:14228.0,519.0] || -> . % 6.84/7.00 14235[10:Spt:14229.0,10068.3,14210.0] || holdsAt(waterLevel(n2),n4)* -> . % 6.84/7.00 14236[10:Spt:14229.0,10068.0,10068.1,10068.2,10068.4] || holdsAt(waterLevel(n0),n2) less(n0,n2) initiates(overflow,filling,n2)* -> stoppedIn(n2,filling,n4). % 6.84/7.00 14245[10:Res:12244.1,14235.0] || holdsAt(waterLevel(n2),n2)* -> . % 6.84/7.00 14417[6:SpL:10826.1,9819.1] || less(n2,n3) stoppedIn(n1,u,n3) less(n2,v) -> equal(skf11(n1,n3,u),n0)** stoppedIn(n0,u,v)*. % 6.84/7.00 14436[6:Rew:10826.1,14417.3] || less(n2,n3) stoppedIn(n1,u,n3)* less(n2,v) -> equal(n2,n0) stoppedIn(n0,u,v)*. % 6.84/7.00 14437[6:MRR:14436.3,338.0] || less(n2,n3) stoppedIn(n1,u,n3)* less(n2,v) -> stoppedIn(n0,u,v)*. % 6.84/7.00 18618[0:Res:46.1,10247.0] || less_or_equal(n2,n8) -> equal(n2,u) less(n2,u) less(u,skf11(u,v,w))*. % 6.84/7.00 18636[0:MRR:18618.0,1012.0] || -> equal(n2,u) less(n2,u) less(u,skf11(u,v,w))*. % 6.84/7.00 18648[0:Res:18636.2,212.1] || less_or_equal(skf11(n3,u,v),n2)* -> equal(n3,n2) less(n2,n3). % 6.84/7.00 18661[0:MRR:18648.1,519.0] || less_or_equal(skf11(n3,u,v),n2)* -> less(n2,n3). % 6.84/7.00 19348[0:Res:1474.0,18661.0] || -> less_or_equal(n3,skf11(n3,u,v))* less(n2,n3). % 6.84/7.00 19355[11:Spt:19348.1] || -> less(n2,n3)*. % 6.84/7.00 19394[11:MRR:14437.0,19355.0] || stoppedIn(n1,u,n3)*+ less(n2,v) -> stoppedIn(n0,u,v)*. % 6.84/7.00 20187[11:Res:149.2,19394.0] || less(n1,n2) less(n2,n3) less(n2,u) -> stoppedIn(n0,filling,u)*. % 6.84/7.00 20190[11:MRR:20187.0,20187.1,10825.0,19355.0] || less(n2,u) -> stoppedIn(n0,filling,u)*. % 6.84/7.00 20195[11:Res:20190.1,65.0] || less(n2,u) -> less(skf11(n0,u,v),u)*. % 6.84/7.00 20215[11:Res:20195.1,33.0] || less(n2,n3) -> less_or_equal(skf11(n0,n3,u),n2)*. % 6.84/7.00 20246[11:MRR:20215.0,19355.0] || -> less_or_equal(skf11(n0,n3,u),n2)*. % 6.84/7.00 20316[11:Res:20246.0,5754.0] || -> equal(skf11(n0,n3,u),n1) less_or_equal(skf11(n0,n3,u),n0)* equal(skf11(n0,n3,u),n2). % 6.84/7.00 20327[11:MRR:20316.1,10297.0] || -> equal(skf11(n0,n3,u),n1) equal(skf11(n0,n3,u),n2)**. % 6.84/7.00 21198[11:SpR:20327.1,10293.0] || -> equal(skf11(n0,n3,u),n1)** less(n0,n2). % 6.84/7.00 21268[12:Spt:21198.0] || -> equal(skf11(n0,n3,u),n1)**. % 6.84/7.00 21277[12:SpR:21268.0,823.1] || stoppedIn(n0,u,n3)* -> happens(overflow,n1). % 6.84/7.00 21357[12:MRR:21277.1,9805.0] || stoppedIn(n0,u,n3)* -> . % 6.84/7.00 21432[12:Res:20190.1,21357.0] || less(n2,n3)* -> . % 6.84/7.00 21433[12:MRR:21432.0,19355.0] || -> . % 6.84/7.00 21436[12:Spt:21433.0,21198.1] || -> less(n0,n2)*. % 6.84/7.00 21437[12:MRR:10067.0,21436.0] || initiates(overflow,filling,n2)* -> holdsAt(waterLevel(n5),n4) stoppedIn(n2,filling,n4). % 6.84/7.00 21445[12:MRR:5593.2,21436.0] || holdsAt(waterLevel(n0),u)+ happens(v,u) initiates(v,filling,u)* -> holdsAt(waterLevel(n2),plus(u,n2)) stoppedIn(u,filling,plus(u,n2))*. % 6.84/7.00 21462[12:Res:4.0,21445.0] || happens(u,n0) initiates(u,filling,n0)* -> holdsAt(waterLevel(n2),plus(n0,n2)) stoppedIn(n0,filling,plus(n0,n2))*. % 6.84/7.00 21491[12:Rew:15.0,21462.3,15.0,21462.2] || happens(u,n0) initiates(u,filling,n0)* -> holdsAt(waterLevel(n2),n2) stoppedIn(n0,filling,n2). % 6.84/7.00 21492[12:MRR:21491.2,14245.0] || happens(u,n0) initiates(u,filling,n0)* -> stoppedIn(n0,filling,n2). % 6.84/7.00 21689[13:Spt:21437.1] || -> holdsAt(waterLevel(n5),n4)*. % 6.84/7.00 21712[13:Res:21689.0,12256.1] || equal(n3,u) -> equal(n5,u)*. % 6.84/7.00 21725[13:MRR:21712.1,599.1] || equal(n3,u)* -> . % 6.84/7.00 21726[13:UnC:21725.0,8562.0] || -> . % 6.84/7.00 21735[13:Spt:21726.0,21437.1,21689.0] || holdsAt(waterLevel(n5),n4)* -> . % 6.84/7.00 21736[13:Spt:21726.0,21437.0,21437.2] || initiates(overflow,filling,n2)* -> stoppedIn(n2,filling,n4). % 6.84/7.00 22916[12:Res:9617.3,21492.1] || holdsAt(filling,n1) happens(tapOn,n0) -> holdsAt(filling,n0) releasedAt(filling,n1) stoppedIn(n0,filling,n2)*. % 6.84/7.00 22917[12:MRR:22916.0,22916.1,22916.2,9724.0,8905.0,5.0] || -> releasedAt(filling,n1) stoppedIn(n0,filling,n2)*. % 6.84/7.00 22919[14:Spt:22917.1] || -> stoppedIn(n0,filling,n2)*. % 6.84/7.00 22922[14:Res:22919.0,65.0] || -> less(skf11(n0,n2,u),n2)*. % 6.84/7.00 22925[14:Res:22922.0,31.0] || -> less_or_equal(skf11(n0,n2,u),n1)*. % 6.84/7.00 22954[14:Res:22925.0,10329.0] || -> equal(skf11(n0,n2,u),n1)**. % 6.84/7.00 23031[14:SpR:22954.0,823.1] || stoppedIn(n0,u,n2)* -> happens(overflow,n1). % 6.84/7.00 23107[14:MRR:23031.1,9805.0] || stoppedIn(n0,u,n2)* -> . % 6.84/7.00 23108[14:UnC:23107.0,22919.0] || -> . % 6.84/7.00 23124[14:Spt:23108.0,22917.1,22919.0] || stoppedIn(n0,filling,n2)* -> . % 6.84/7.00 23125[14:Spt:23108.0,22917.0] || -> releasedAt(filling,n1)*. % 6.84/7.00 23135[14:Res:23125.0,12251.0] || equal(skf21(filling),n3) -> releasedAt(filling,n0)* holdsAt(filling,n4). % 6.84/7.00 23139[14:Res:23125.0,8980.0] || holdsAt(filling,n2) -> releasedAt(filling,n0)* equal(skf21(filling),n3). % 6.84/7.00 23151[14:MRR:23135.1,23135.2,7.0,11777.0] || equal(skf21(filling),n3)** -> . % 6.84/7.00 23154[14:MRR:23139.0,23139.1,136.0,7.0] || -> equal(skf21(filling),n3)**. % 6.84/7.00 23155[14:MRR:23154.0,23151.0] || -> . % 6.84/7.00 23163[11:Spt:23155.0,19348.1,19355.0] || less(n2,n3)* -> . % 6.84/7.00 23164[11:Spt:23155.0,19348.0] || -> less_or_equal(n3,skf11(n3,u,v))*. % 6.84/7.00 23182[11:Res:59.2,23163.0] || less_or_equal(n2,n3)* -> equal(n3,n2). % 6.84/7.00 23187[11:MRR:23182.0,23182.1,1429.0,519.0] || -> . % 6.84/7.00 23188[8:Spt:23187.0,9644.3] || -> happens(skf16(n3,u),n3)*. % 6.84/7.00 23225[8:Res:23188.0,61.0] || -> equal(n3,n0) equal(skf16(n3,u),overflow)**. % 6.84/7.00 23227[8:Res:23188.0,64.0] || -> equal(skf16(n3,u),tapOn)** holdsAt(filling,n3). % 6.84/7.00 23230[8:MRR:23225.0,337.0] || -> equal(skf16(n3,u),overflow)**. % 6.84/7.00 23240[8:Rew:23230.0,23227.0] || -> equal(overflow,tapOn) holdsAt(filling,n3)*. % 6.84/7.00 23241[8:MRR:23240.0,23240.1,11.0,144.0] || -> . % 6.84/7.00 23243[6:Spt:23241.0,10824.0,10825.0] || less(n1,n2)* -> . % 6.84/7.00 23244[6:Spt:23241.0,10824.1] || -> less(n0,n1)*. % 6.84/7.00 23344[6:Res:59.2,23243.0] || less_or_equal(n1,n2)* -> equal(n2,n1). % 6.84/7.00 23349[6:MRR:23344.0,23344.1,1473.0,541.0] || -> . % 6.84/7.00 23350[5:Spt:23349.0,8677.2] || -> happens(skf18(n3,u),n3)*. % 6.84/7.00 23409[5:Res:23350.0,61.0] || -> equal(n3,n0) equal(skf18(n3,u),overflow)**. % 6.84/7.00 23411[5:Res:23350.0,64.0] || -> equal(skf18(n3,u),tapOn)** holdsAt(filling,n3). % 6.84/7.00 23414[5:MRR:23409.0,337.0] || -> equal(skf18(n3,u),overflow)**. % 6.84/7.00 23428[5:Rew:23414.0,23411.0] || -> equal(overflow,tapOn) holdsAt(filling,n3)*. % 6.84/7.00 23429[5:MRR:23428.0,23428.1,11.0,144.0] || -> . % 6.84/7.00 23431[4:Spt:23429.0,936.3] || -> happens(skf16(n1,u),n1)*. % 6.84/7.00 23449[4:Res:23431.0,61.0] || -> equal(n1,n0) equal(skf16(n1,u),overflow)**. % 6.84/7.00 23454[4:Res:23431.0,11853.1] || equal(skf16(n1,u),overflow)** -> . % 6.84/7.00 23463[4:MRR:23449.0,339.0] || -> equal(skf16(n1,u),overflow)**. % 6.84/7.00 23464[4:MRR:23463.0,23454.0] || -> . % 6.84/7.00 23481[1:Spt:23464.0,606.2] || -> happens(skf18(n1,u),n1)*. % 6.84/7.00 23523[1:Res:23481.0,61.0] || -> equal(n1,n0) equal(skf18(n1,u),overflow)**. % 6.84/7.00 23528[1:Res:23481.0,11853.1] || equal(skf18(n1,u),overflow)** -> . % 6.84/7.00 23532[1:MRR:23523.0,339.0] || -> equal(skf18(n1,u),overflow)**. % 6.97/7.14 23533[1:MRR:23532.0,23528.0] || -> . % 6.97/7.14 % SZS output end Refutation % 6.97/7.14 Formulae used in the proof : nothing_terminates_filling_2 less0 waterLevel_0 not_filling_0 not_spilling_0 not_released_filling_0 not_released_spilling_0 tapOff_not_tapOn overflow_not_tapOn plus0_1 plus0_2 plus1_1 plus1_2 plus1_3 plus2_2 plus2_3 not_released_waterLevel_0 spilling_not_waterLevel symmetry_of_plus less_or_equal less1 less2 less3 less4 less5 less6 less7 less8 less9 initiates_all_defn less_property terminates_all_defn releases_all_defn distinct_waterLevels happens_all_defn stoppedin_defn change_of_waterLevel same_waterLevel keep_not_released happens_holds happens_terminates_not_holds happens_not_released keep_holding keep_not_holding change_holding % 6.97/7.14 %------------------------------------------------------------------------------