%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : CSR009+1 : TPTP v8.1.0. Bugfixed v3.1.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n032.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:12 EDT 2022 % Result : Theorem 16.75s 16.99s % Output : Refutation 16.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : CSR009+1 : TPTP v8.1.0. Bugfixed v3.1.0. % 0.00/0.11 % Command : run_spass %d %s % 0.11/0.31 % Computer : n032.cluster.edu % 0.11/0.31 % Model : x86_64 x86_64 % 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.31 % Memory : 8042.1875MB % 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.31 % CPULimit : 300 % 0.11/0.31 % WCLimit : 600 % 0.11/0.31 % DateTime : Fri Jun 10 16:49:24 EDT 2022 % 0.11/0.31 % CPUTime : % 16.75/16.99 % 16.75/16.99 SPASS V 3.9 % 16.75/16.99 SPASS beiseite: Proof found. % 16.75/16.99 % SZS status Theorem % 16.75/16.99 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 16.75/16.99 SPASS derived 25851 clauses, backtracked 2024 clauses, performed 86 splits and kept 8341 clauses. % 16.75/16.99 SPASS allocated 106740 KBytes. % 16.75/16.99 SPASS spent 0:0:16.64 on the problem. % 16.75/16.99 0:00:00.03 for the input. % 16.75/16.99 0:00:00.05 for the FLOTTER CNF translation. % 16.75/16.99 0:00:00.49 for inferences. % 16.75/16.99 0:00:00.31 for the backtracking. % 16.75/16.99 0:0:15.61 for the reduction. % 16.75/16.99 % 16.75/16.99 % 16.75/16.99 Here is a proof with depth 17, length 629 : % 16.75/16.99 % SZS output start Refutation % 16.75/16.99 1[0:Inp] || holdsAt(filling,n2)* -> . % 16.75/16.99 2[0:Inp] || less(u,n0)* -> . % 16.75/16.99 3[0:Inp] || -> holdsAt(waterLevel(n0),n0)*. % 16.75/16.99 4[0:Inp] || holdsAt(filling,n0)* -> . % 16.75/16.99 6[0:Inp] || releasedAt(filling,n0)* -> . % 16.75/16.99 8[0:Inp] || equal(tapOff,tapOn)** -> . % 16.75/16.99 10[0:Inp] || equal(overflow,tapOn)** -> . % 16.75/16.99 11[0:Inp] || equal(spilling,filling)** -> . % 16.75/16.99 13[0:Inp] || -> equal(plus(n0,n1),n1)**. % 16.75/16.99 16[0:Inp] || -> equal(plus(n1,n1),n2)**. % 16.75/16.99 17[0:Inp] || -> equal(plus(n1,n2),n3)**. % 16.75/16.99 18[0:Inp] || -> equal(plus(n1,n3),n4)**. % 16.75/16.99 22[0:Inp] || releasedAt(waterLevel(u),n0)* -> . % 16.75/16.99 23[0:Inp] || equal(waterLevel(u),filling)** -> . % 16.75/16.99 25[0:Inp] || -> equal(plus(u,v),plus(v,u))*. % 16.75/16.99 26[0:Inp] || less(u,v)* -> less_or_equal(u,v). % 16.75/16.99 27[0:Inp] || equal(u,v) -> less_or_equal(u,v)*. % 16.75/16.99 28[0:Inp] || less(u,n1)* -> less_or_equal(u,n0). % 16.75/16.99 29[0:Inp] || less_or_equal(u,n0) -> less(u,n1)*. % 16.75/16.99 30[0:Inp] || less(u,n2)* -> less_or_equal(u,n1). % 16.75/16.99 31[0:Inp] || less_or_equal(u,n1) -> less(u,n2)*. % 16.75/16.99 32[0:Inp] || less(u,n3)* -> less_or_equal(u,n2). % 16.75/16.99 33[0:Inp] || less_or_equal(u,n2) -> less(u,n3)*. % 16.75/16.99 34[0:Inp] || less(u,n4)* -> less_or_equal(u,n3). % 16.75/16.99 35[0:Inp] || less_or_equal(u,n3) -> less(u,n4)*. % 16.75/16.99 36[0:Inp] || less(u,n5)* -> less_or_equal(u,n4). % 16.75/16.99 37[0:Inp] || less_or_equal(u,n4) -> less(u,n5)*. % 16.75/16.99 38[0:Inp] || less(u,n6)* -> less_or_equal(u,n5). % 16.75/16.99 39[0:Inp] || less_or_equal(u,n5) -> less(u,n6)*. % 16.75/16.99 40[0:Inp] || less(u,n7)* -> less_or_equal(u,n6). % 16.75/16.99 41[0:Inp] || less_or_equal(u,n6) -> less(u,n7)*. % 16.75/16.99 42[0:Inp] || less(u,n8)* -> less_or_equal(u,n7). % 16.75/16.99 43[0:Inp] || less_or_equal(u,n7) -> less(u,n8)*. % 16.75/16.99 44[0:Inp] || less(u,n9)* -> less_or_equal(u,n8). % 16.75/16.99 45[0:Inp] || less_or_equal(u,n8) -> less(u,n9)*. % 16.75/16.99 48[0:Inp] || less(u,v)*+ less(v,u)* -> . % 16.75/16.99 49[0:Inp] || less(u,v)* equal(v,u) -> . % 16.75/16.99 50[0:Inp] || SkP0(u,v) -> initiates(v,u,w)*. % 16.75/16.99 52[0:Inp] || terminates(u,v,w)* -> equal(v,filling). % 16.75/16.99 53[0:Inp] || releases(u,v,w)* -> equal(u,tapOn). % 16.75/16.99 54[0:Inp] || -> less(u,v)* equal(v,u) less(v,u)*. % 16.75/16.99 56[0:Inp] || equal(waterLevel(u),waterLevel(v))* -> equal(u,v). % 16.75/16.99 57[0:Inp] || equal(u,v) -> equal(waterLevel(u),waterLevel(v))*. % 16.75/16.99 58[0:Inp] || less_or_equal(u,v) -> equal(u,v) less(u,v)*. % 16.75/16.99 59[0:Inp] || releases(u,v,w)* -> equal(waterLevel(skf21(v)),v). % 16.75/16.99 60[0:Inp] || happens(u,v)* -> equal(v,n0) equal(u,overflow). % 16.75/16.99 61[0:Inp] || happens(u,v)* -> equal(v,n0) holdsAt(filling,v). % 16.75/16.99 63[0:Inp] || happens(u,v)* -> equal(u,tapOn) holdsAt(filling,v). % 16.75/16.99 64[0:Inp] || stoppedIn(u,v,w)*+ -> less(skf11(u,w,x),w)*. % 16.75/16.99 65[0:Inp] || stoppedIn(u,v,w)*+ -> less(u,skf11(u,x,y))*. % 16.75/16.99 68[0:Inp] || equal(u,tapOn) equal(v,filling) -> SkP0(v,u)*. % 16.75/16.99 70[0:Inp] || SkP1(u,v,w)*+ -> equal(waterLevel(skf20(u,x)),u)**. % 16.75/16.99 72[0:Inp] || happens(u,v)*+ -> equal(v,n0) holdsAt(waterLevel(n3),v)*. % 16.75/16.99 74[0:Inp] || equal(u,n0) equal(v,tapOn) -> happens(v,u)*. % 16.75/16.99 75[0:Inp] || equal(u,spilling) equal(v,overflow) -> initiates(v,u,w)*. % 16.75/16.99 77[0:Inp] || equal(u,filling) equal(v,overflow) -> terminates(v,u,w)*. % 16.75/16.99 78[0:Inp] || equal(u,tapOn) equal(v,waterLevel(w))*+ -> releases(u,v,x)*. % 16.75/16.99 79[0:Inp] || holdsAt(waterLevel(u),v) -> trajectory(filling,v,waterLevel(plus(u,w)),w)*. % 16.75/16.99 80[0:Inp] || holdsAt(waterLevel(u),v)*+ holdsAt(waterLevel(w),v)* -> equal(w,u)*. % 16.75/16.99 83[0:Inp] || releasedAt(u,v)+ -> releasedAt(u,plus(v,n1))* happens(skf17(v,w),v)*. % 16.75/16.99 84[0:Inp] || releasedAt(u,plus(v,n1))*+ -> releasedAt(u,v) happens(skf18(v,w),v)*. % 16.75/16.99 85[0:Inp] || happens(u,v) initiates(u,w,v)*+ -> holdsAt(w,plus(v,n1))*. % 16.75/16.99 86[0:Inp] || happens(u,v) releases(u,w,v)*+ -> releasedAt(w,plus(v,n1))*. % 16.75/16.99 89[0:Inp] || releasedAt(u,plus(v,n1)) -> releasedAt(u,v) releases(skf18(v,u),u,v)*. % 16.75/16.99 90[0:Inp] || happens(u,v) holdsAt(w,plus(v,n1))*+ terminates(u,w,v)* -> . % 16.75/16.99 91[0:Inp] || happens(u,v) releasedAt(w,plus(v,n1))*+ initiates(u,w,v)* -> . % 16.75/16.99 92[0:Inp] || happens(u,v) releasedAt(w,plus(v,n1))*+ terminates(u,w,v)* -> . % 16.75/16.99 94[0:Inp] || equal(u,overflow) holdsAt(filling,v) holdsAt(waterLevel(n3),v)*+ -> happens(u,v)*. % 16.75/16.99 95[0:Inp] || equal(u,overflow) equal(v,waterLevel(w))*+ holdsAt(waterLevel(w),x)* -> initiates(u,v,x)*. % 16.75/16.99 96[0:Inp] || equal(u,tapOff) equal(v,waterLevel(w))*+ holdsAt(waterLevel(w),x)* -> SkP1(v,u,x)*. % 16.75/16.99 97[0:Inp] || holdsAt(u,v)+ -> holdsAt(u,plus(v,n1)) releasedAt(u,plus(v,n1))* happens(skf15(v,w),v)*. % 16.75/16.99 98[0:Inp] || holdsAt(u,plus(v,n1))+ -> holdsAt(u,v) releasedAt(u,plus(v,n1))* happens(skf16(v,w),v)*. % 16.75/16.99 99[0:Inp] || holdsAt(u,plus(v,n1)) -> holdsAt(u,v) releasedAt(u,plus(v,n1)) initiates(skf16(v,u),u,v)*. % 16.75/16.99 100[0:Inp] || holdsAt(u,v) -> holdsAt(u,plus(v,n1)) releasedAt(u,plus(v,n1)) terminates(skf15(v,u),u,v)*. % 16.75/16.99 103[0:Inp] || releasedAt(u,v) -> releasedAt(u,plus(v,n1)) terminates(skf17(v,u),u,v) initiates(skf17(v,u),u,v)*. % 16.75/16.99 105[0:Inp] || less(u,v)* less(v,w)* happens(x,v) terminates(x,y,v)*+ -> stoppedIn(u,y,w)*. % 16.75/16.99 107[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))*. % 16.75/16.99 109[0:Res:61.1,1.0] || happens(u,n2)* -> equal(n2,n0). % 16.75/16.99 113[0:Res:98.2,1.0] || holdsAt(filling,plus(n2,n1)) -> happens(skf16(n2,u),n2)* releasedAt(filling,plus(n2,n1)). % 16.75/16.99 114[0:Rew:17.0,113.2,25.0,113.2,17.0,113.0,25.0,113.0] || holdsAt(filling,n3) -> releasedAt(filling,n3) happens(skf16(n2,u),n2)*. % 16.75/16.99 148[0:Res:43.1,26.0] || less_or_equal(u,n7) -> less_or_equal(u,n8)*. % 16.75/16.99 149[0:Res:41.1,26.0] || less_or_equal(u,n6) -> less_or_equal(u,n7)*. % 16.75/16.99 150[0:Res:39.1,26.0] || less_or_equal(u,n5) -> less_or_equal(u,n6)*. % 16.75/16.99 151[0:Res:37.1,26.0] || less_or_equal(u,n4) -> less_or_equal(u,n5)*. % 16.75/16.99 152[0:Res:35.1,26.0] || less_or_equal(u,n3) -> less_or_equal(u,n4)*. % 16.75/16.99 153[0:Res:33.1,26.0] || less_or_equal(u,n2) -> less_or_equal(u,n3)*. % 16.75/16.99 154[0:Res:31.1,26.0] || less_or_equal(u,n1) -> less_or_equal(u,n2)*. % 16.75/16.99 155[0:Res:29.1,26.0] || less_or_equal(u,n0) -> less_or_equal(u,n1)*. % 16.75/16.99 161[0:Res:35.1,49.0] || less_or_equal(u,n3)* equal(n4,u) -> . % 16.75/16.99 162[0:Res:33.1,49.0] || less_or_equal(u,n2)* equal(n3,u) -> . % 16.75/16.99 163[0:Res:31.1,49.0] || less_or_equal(u,n1)* equal(n2,u) -> . % 16.75/16.99 164[0:Res:29.1,49.0] || less_or_equal(u,n0)* equal(n1,u) -> . % 16.75/16.99 165[0:Res:45.1,48.0] || less_or_equal(u,n8) less(n9,u)* -> . % 16.75/16.99 166[0:Res:43.1,48.0] || less_or_equal(u,n7) less(n8,u)* -> . % 16.75/16.99 167[0:Res:41.1,48.0] || less_or_equal(u,n6) less(n7,u)* -> . % 16.75/16.99 168[0:Res:39.1,48.0] || less_or_equal(u,n5) less(n6,u)* -> . % 16.75/16.99 169[0:Res:37.1,48.0] || less_or_equal(u,n4) less(n5,u)* -> . % 16.75/16.99 170[0:Res:35.1,48.0] || less_or_equal(u,n3) less(n4,u)* -> . % 16.75/16.99 171[0:Res:33.1,48.0] || less_or_equal(u,n2) less(n3,u)* -> . % 16.75/16.99 172[0:Res:31.1,48.0] || less_or_equal(u,n1) less(n2,u)* -> . % 16.75/16.99 191[0:Res:45.1,165.1] || less_or_equal(n9,n8)* less_or_equal(n9,n8)* -> . % 16.75/16.99 200[0:Obv:191.0] || less_or_equal(n9,n8)* -> . % 16.75/16.99 201[0:Res:148.1,200.0] || less_or_equal(n9,n7)* -> . % 16.75/16.99 203[0:Res:149.1,201.0] || less_or_equal(n9,n6)* -> . % 16.75/16.99 205[0:Res:150.1,203.0] || less_or_equal(n9,n5)* -> . % 16.75/16.99 207[0:Res:151.1,205.0] || less_or_equal(n9,n4)* -> . % 16.75/16.99 209[0:Res:152.1,207.0] || less_or_equal(n9,n3)* -> . % 16.75/16.99 211[0:Res:153.1,209.0] || less_or_equal(n9,n2)* -> . % 16.75/16.99 213[0:Res:154.1,211.0] || less_or_equal(n9,n1)* -> . % 16.75/16.99 233[0:Res:155.1,213.0] || less_or_equal(n9,n0)* -> . % 16.75/16.99 234[0:Res:27.1,213.0] || equal(n9,n1)** -> . % 16.75/16.99 242[0:Res:43.1,166.1] || less_or_equal(n8,n7)* less_or_equal(n8,n7)* -> . % 16.75/16.99 250[0:Obv:242.0] || less_or_equal(n8,n7)* -> . % 16.75/16.99 251[0:Res:149.1,250.0] || less_or_equal(n8,n6)* -> . % 16.75/16.99 253[0:Res:150.1,251.0] || less_or_equal(n8,n5)* -> . % 16.75/16.99 256[0:Res:54.0,2.0] || -> equal(n0,u) less(n0,u)*. % 16.75/16.99 257[0:Res:54.0,44.0] || -> equal(n9,u) less(n9,u)* less_or_equal(u,n8). % 16.75/16.99 258[0:Res:54.0,42.0] || -> equal(n8,u) less(n8,u)* less_or_equal(u,n7). % 16.75/16.99 259[0:Res:54.0,40.0] || -> equal(n7,u) less(n7,u)* less_or_equal(u,n6). % 16.75/16.99 260[0:Res:54.0,38.0] || -> equal(n6,u) less(n6,u)* less_or_equal(u,n5). % 16.75/16.99 261[0:Res:54.0,36.0] || -> equal(n5,u) less(n5,u)* less_or_equal(u,n4). % 16.75/16.99 262[0:Res:54.0,34.0] || -> equal(n4,u) less(n4,u)* less_or_equal(u,n3). % 16.75/16.99 263[0:Res:54.0,32.0] || -> equal(n3,u) less(n3,u)* less_or_equal(u,n2). % 16.75/16.99 264[0:Res:54.0,30.0] || -> equal(n2,u) less(n2,u)* less_or_equal(u,n1). % 16.75/16.99 265[0:Res:54.0,28.0] || -> equal(n1,u) less(n1,u)* less_or_equal(u,n0). % 16.75/16.99 268[0:Res:54.0,26.0] || -> equal(u,v) less(u,v)* less_or_equal(v,u). % 16.75/16.99 287[0:Res:151.1,253.0] || less_or_equal(n8,n4)* -> . % 16.75/16.99 289[0:Res:152.1,287.0] || less_or_equal(n8,n3)* -> . % 16.75/16.99 291[0:Res:153.1,289.0] || less_or_equal(n8,n2)* -> . % 16.75/16.99 293[0:Res:154.1,291.0] || less_or_equal(n8,n1)* -> . % 16.75/16.99 295[0:Res:155.1,293.0] || less_or_equal(n8,n0)* -> . % 16.75/16.99 296[0:Res:27.1,293.0] || equal(n8,n1)** -> . % 16.75/16.99 310[0:Res:256.1,26.0] || -> equal(n0,u) less_or_equal(n0,u)*. % 16.75/16.99 313[0:MRR:310.0,27.0] || -> less_or_equal(n0,u)*. % 16.75/16.99 319[0:Res:313.0,161.0] || equal(n4,n0)** -> . % 16.75/16.99 320[0:Res:313.0,162.0] || equal(n3,n0)** -> . % 16.75/16.99 321[0:Res:313.0,163.0] || equal(n2,n0)** -> . % 16.75/16.99 322[0:Res:313.0,164.0] || equal(n1,n0)** -> . % 16.75/16.99 323[0:MRR:109.1,321.0] || happens(u,n2)* -> . % 16.75/16.99 324[0:MRR:114.2,323.0] || holdsAt(filling,n3) -> releasedAt(filling,n3)*. % 16.75/16.99 328[0:Res:41.1,167.1] || less_or_equal(n7,n6)* less_or_equal(n7,n6)* -> . % 16.75/16.99 337[0:Obv:328.0] || less_or_equal(n7,n6)* -> . % 16.75/16.99 338[0:Res:150.1,337.0] || less_or_equal(n7,n5)* -> . % 16.75/16.99 340[0:Res:58.2,2.0] || less_or_equal(u,n0)* -> equal(u,n0). % 16.75/16.99 349[0:Res:58.2,28.0] || less_or_equal(u,n1)* -> equal(u,n1) less_or_equal(u,n0). % 16.75/16.99 350[0:Res:58.2,48.0] || less_or_equal(u,v) less(v,u)* -> equal(u,v). % 16.75/16.99 356[0:MRR:350.2,49.1] || less_or_equal(u,v) less(v,u)* -> . % 16.75/16.99 360[0:Res:151.1,338.0] || less_or_equal(n7,n4)* -> . % 16.75/16.99 362[0:Res:152.1,360.0] || less_or_equal(n7,n3)* -> . % 16.75/16.99 364[0:Res:153.1,362.0] || less_or_equal(n7,n2)* -> . % 16.75/16.99 366[0:Res:154.1,364.0] || less_or_equal(n7,n1)* -> . % 16.75/16.99 368[0:Res:155.1,366.0] || less_or_equal(n7,n0)* -> . % 16.75/16.99 369[0:Res:27.1,366.0] || equal(n7,n1)** -> . % 16.75/16.99 378[0:Res:39.1,168.1] || less_or_equal(n6,n5)* less_or_equal(n6,n5)* -> . % 16.75/16.99 387[0:Obv:378.0] || less_or_equal(n6,n5)* -> . % 16.75/16.99 389[0:Res:151.1,387.0] || less_or_equal(n6,n4)* -> . % 16.75/16.99 391[0:Res:152.1,389.0] || less_or_equal(n6,n3)* -> . % 16.75/16.99 401[0:Res:153.1,391.0] || less_or_equal(n6,n2)* -> . % 16.75/16.99 403[0:Res:154.1,401.0] || less_or_equal(n6,n1)* -> . % 16.75/16.99 405[0:Res:155.1,403.0] || less_or_equal(n6,n0)* -> . % 16.75/16.99 406[0:Res:27.1,403.0] || equal(n6,n1)** -> . % 16.75/16.99 412[0:Res:37.1,169.1] || less_or_equal(n5,n4)* less_or_equal(n5,n4)* -> . % 16.75/16.99 420[0:Obv:412.0] || less_or_equal(n5,n4)* -> . % 16.75/16.99 422[0:Res:152.1,420.0] || less_or_equal(n5,n3)* -> . % 16.75/16.99 424[0:Res:153.1,422.0] || less_or_equal(n5,n2)* -> . % 16.75/16.99 426[0:Res:154.1,424.0] || less_or_equal(n5,n1)* -> . % 16.75/16.99 428[0:Res:155.1,426.0] || less_or_equal(n5,n0)* -> . % 16.75/16.99 429[0:Res:27.1,426.0] || equal(n5,n1)** -> . % 16.75/16.99 436[0:Res:35.1,170.1] || less_or_equal(n4,n3)* less_or_equal(n4,n3)* -> . % 16.75/16.99 443[0:Obv:436.0] || less_or_equal(n4,n3)* -> . % 16.75/16.99 445[0:Res:153.1,443.0] || less_or_equal(n4,n2)* -> . % 16.75/16.99 447[0:Res:154.1,445.0] || less_or_equal(n4,n1)* -> . % 16.75/16.99 449[0:Res:155.1,447.0] || less_or_equal(n4,n0)* -> . % 16.75/16.99 450[0:Res:27.1,447.0] || equal(n4,n1)** -> . % 16.75/16.99 458[0:Res:33.1,171.1] || less_or_equal(n3,n2)* less_or_equal(n3,n2)* -> . % 16.75/16.99 464[0:Obv:458.0] || less_or_equal(n3,n2)* -> . % 16.75/16.99 468[0:Res:154.1,464.0] || less_or_equal(n3,n1)* -> . % 16.75/16.99 471[0:Res:27.1,468.0] || equal(n3,n1)** -> . % 16.75/16.99 482[0:Res:31.1,172.1] || less_or_equal(n2,n1)* less_or_equal(n2,n1)* -> . % 16.75/16.99 484[0:Res:58.2,172.1] || less_or_equal(n2,u)* less_or_equal(u,n1)* -> equal(n2,u). % 16.75/16.99 487[0:Obv:482.0] || less_or_equal(n2,n1)* -> . % 16.75/16.99 488[0:MRR:484.2,163.1] || less_or_equal(n2,u)*+ less_or_equal(u,n1)* -> . % 16.75/16.99 489[0:Res:155.1,487.0] || less_or_equal(n2,n0)* -> . % 16.75/16.99 490[0:Res:27.1,487.0] || equal(n2,n1)** -> . % 16.75/16.99 518[0:SpR:13.0,79.1] || holdsAt(waterLevel(n0),u) -> trajectory(filling,u,waterLevel(n1),n1)*. % 16.75/16.99 543[0:EqR:78.1] || equal(u,tapOn) -> releases(u,waterLevel(v),w)*. % 16.75/16.99 563[0:SpL:16.0,84.0] || releasedAt(u,n2)*+ -> releasedAt(u,n1) happens(skf18(n1,v),n1)*. % 16.75/16.99 564[0:SpL:13.0,84.0] || releasedAt(u,n1)*+ -> releasedAt(u,n0) happens(skf18(n0,v),n0)*. % 16.75/16.99 565[0:SpL:25.0,84.0] || releasedAt(u,plus(n1,v))*+ -> releasedAt(u,v) happens(skf18(v,w),v)*. % 16.75/16.99 647[0:Res:75.2,85.1] || equal(u,spilling)+ equal(v,overflow) happens(v,w)* -> holdsAt(u,plus(w,n1))*. % 16.75/16.99 648[0:Res:50.1,85.1] || SkP0(u,v)*+ happens(v,w)* -> holdsAt(u,plus(w,n1))*. % 16.75/16.99 706[0:SpL:16.0,92.1] || happens(u,n1) releasedAt(v,n2) terminates(u,v,n1)* -> . % 16.75/16.99 717[0:SpL:16.0,90.1] || happens(u,n1) holdsAt(v,n2) terminates(u,v,n1)* -> . % 16.75/16.99 727[0:SpL:16.0,91.1] || happens(u,n1) releasedAt(v,n2) initiates(u,v,n1)* -> . % 16.75/16.99 728[0:SpL:13.0,91.1] || happens(u,n0) releasedAt(v,n1) initiates(u,v,n0)* -> . % 16.75/16.99 740[0:Res:89.2,53.0] || releasedAt(u,plus(v,n1))* -> releasedAt(u,v) equal(skf18(v,u),tapOn). % 16.75/16.99 742[0:Rew:740.2,89.2] || releasedAt(u,plus(v,n1))* -> releasedAt(u,v) releases(tapOn,u,v). % 16.75/16.99 752[0:SpL:13.0,742.0] || releasedAt(u,n1) -> releasedAt(u,n0) releases(tapOn,u,n0)*. % 16.75/16.99 753[0:SpL:25.0,742.0] || releasedAt(u,plus(n1,v))* -> releasedAt(u,v) releases(tapOn,u,v). % 16.75/16.99 825[0:SpL:57.1,94.2] || equal(u,n3) equal(v,overflow) holdsAt(filling,w) holdsAt(waterLevel(u),w)*+ -> happens(v,w)*. % 16.75/16.99 834[0:EqR:96.1] || equal(u,tapOff) holdsAt(waterLevel(v),w) -> SkP1(waterLevel(v),u,w)*. % 16.75/16.99 843[0:EqR:95.1] || equal(u,overflow) holdsAt(waterLevel(v),w) -> initiates(u,waterLevel(v),w)*. % 16.75/16.99 852[0:Res:3.0,97.0] || -> holdsAt(waterLevel(n0),plus(n0,n1)) releasedAt(waterLevel(n0),plus(n0,n1))* happens(skf15(n0,u),n0)*. % 16.75/16.99 854[0:Rew:13.0,852.1,13.0,852.0] || -> holdsAt(waterLevel(n0),n1) releasedAt(waterLevel(n0),n1) happens(skf15(n0,u),n0)*. % 16.75/16.99 868[0:Res:58.2,356.1] || less_or_equal(u,v)*+ less_or_equal(v,u)* -> equal(u,v). % 16.75/16.99 873[0:SpL:13.0,98.0] || holdsAt(u,n1) -> holdsAt(u,n0) releasedAt(u,plus(n0,n1))* happens(skf16(n0,v),n0)*. % 16.75/16.99 874[0:SpL:25.0,98.0] || holdsAt(u,plus(n1,v))+ -> holdsAt(u,v) releasedAt(u,plus(v,n1))* happens(skf16(v,w),v)*. % 16.75/16.99 877[0:Rew:13.0,873.2] || holdsAt(u,n1)+ -> holdsAt(u,n0) releasedAt(u,n1)* happens(skf16(n0,v),n0)*. % 16.75/16.99 887[0:Res:257.1,28.0] || -> equal(n9,n1) less_or_equal(n1,n8) less_or_equal(n9,n0)*. % 16.75/16.99 900[0:MRR:887.0,887.2,234.0,233.0] || -> less_or_equal(n1,n8)*. % 16.75/16.99 907[0:Res:100.3,52.0] || holdsAt(u,v) -> holdsAt(u,plus(v,n1)) releasedAt(u,plus(v,n1))* equal(u,filling). % 16.75/16.99 996[0:Res:258.1,28.0] || -> equal(n8,n1) less_or_equal(n1,n7) less_or_equal(n8,n0)*. % 16.75/16.99 1008[0:MRR:996.0,996.2,296.0,295.0] || -> less_or_equal(n1,n7)*. % 16.75/16.99 1010[0:Res:103.3,85.1] || releasedAt(u,v) happens(skf17(v,u),v) -> releasedAt(u,plus(v,n1)) terminates(skf17(v,u),u,v)* holdsAt(u,plus(v,n1)). % 16.75/16.99 1011[0:MRR:1010.1,83.2] || releasedAt(u,v) -> releasedAt(u,plus(v,n1)) terminates(skf17(v,u),u,v)* holdsAt(u,plus(v,n1)). % 16.75/16.99 1186[0:Res:259.1,28.0] || -> equal(n7,n1) less_or_equal(n1,n6) less_or_equal(n7,n0)*. % 16.75/16.99 1197[0:MRR:1186.0,1186.2,369.0,368.0] || -> less_or_equal(n1,n6)*. % 16.75/16.99 1204[0:Res:77.2,105.3] || equal(u,filling)+ equal(v,overflow) less(w,x)* less(x,y)* happens(v,x)* -> stoppedIn(w,u,y)*. % 16.75/16.99 1205[0:Res:100.3,105.3] || holdsAt(u,v) less(w,v)* less(v,x)* happens(skf15(v,u),v)* -> holdsAt(u,plus(v,n1)) releasedAt(u,plus(v,n1)) stoppedIn(w,u,x)*. % 16.75/16.99 1208[0:MRR:1205.3,97.3] || holdsAt(u,v)+ less(w,v)* less(v,x)* -> holdsAt(u,plus(v,n1)) releasedAt(u,plus(v,n1))* stoppedIn(w,u,x)*. % 16.75/16.99 1439[0:Res:260.1,28.0] || -> equal(n6,n1) less_or_equal(n1,n5) less_or_equal(n6,n0)*. % 16.75/16.99 1449[0:MRR:1439.0,1439.2,406.0,405.0] || -> less_or_equal(n1,n5)*. % 16.75/16.99 1552[0:Res:261.1,28.0] || -> equal(n5,n1) less_or_equal(n1,n4) less_or_equal(n5,n0)*. % 16.75/16.99 1561[0:MRR:1552.0,1552.2,429.0,428.0] || -> less_or_equal(n1,n4)*. % 16.75/16.99 1591[0:Res:262.1,28.0] || -> equal(n4,n1) less_or_equal(n1,n3) less_or_equal(n4,n0)*. % 16.75/16.99 1599[0:MRR:1591.0,1591.2,450.0,449.0] || -> less_or_equal(n1,n3)*. % 16.75/16.99 1640[0:Res:263.1,26.0] || -> equal(n3,u) less_or_equal(u,n2)* less_or_equal(n3,u)*. % 16.75/16.99 1645[0:MRR:1640.0,27.0] || -> less_or_equal(u,n2)* less_or_equal(n3,u)*. % 16.75/16.99 1739[0:Res:264.1,26.0] || -> equal(n2,u) less_or_equal(u,n1)* less_or_equal(n2,u)*. % 16.75/16.99 1743[0:MRR:1739.0,27.0] || -> less_or_equal(u,n1)* less_or_equal(n2,u)*. % 16.75/16.99 1884[0:Res:265.1,26.0] || -> equal(n1,u) less_or_equal(u,n0)* less_or_equal(n1,u)*. % 16.75/16.99 1887[0:MRR:1884.0,27.0] || -> less_or_equal(u,n0)* less_or_equal(n1,u)*. % 16.75/16.99 1991[0:Res:543.1,59.0] || equal(u,tapOn)* -> equal(waterLevel(skf21(waterLevel(v))),waterLevel(v))**. % 16.75/16.99 1993[0:Res:543.1,86.1] || equal(u,tapOn)+ happens(u,v)* -> releasedAt(waterLevel(w),plus(v,n1))*. % 16.75/16.99 1994[0:AED:8.0,1991.0] || -> equal(waterLevel(skf21(waterLevel(u))),waterLevel(u))**. % 16.75/16.99 2179[0:Res:268.1,26.0] || -> equal(u,v) less_or_equal(v,u)* less_or_equal(u,v)*. % 16.75/16.99 2190[0:MRR:2179.0,27.0] || -> less_or_equal(u,v)* less_or_equal(v,u)*. % 16.75/16.99 2191[0:Fac:2190.0,2190.1] || -> less_or_equal(u,u)*. % 16.75/16.99 4659[0:SpL:1994.0,56.0] || equal(waterLevel(u),waterLevel(v))*+ -> equal(skf21(waterLevel(u)),v)*. % 16.75/16.99 4820[0:Res:1743.0,349.0] || -> less_or_equal(n2,u)* equal(u,n1) less_or_equal(u,n0)*. % 16.75/16.99 5261[0:Res:4820.2,340.0] || -> less_or_equal(n2,u)* equal(u,n1) equal(u,n0). % 16.75/16.99 5335[0:Res:5261.0,488.0] || less_or_equal(u,n1)* -> equal(u,n1) equal(u,n0). % 16.75/16.99 5454[0:Res:518.1,107.3] || holdsAt(waterLevel(n0),u)+ happens(v,u) less(n0,n1) initiates(v,filling,u)* -> holdsAt(waterLevel(n1),plus(u,n1)) stoppedIn(u,filling,plus(u,n1))*. % 16.75/16.99 5462[0:Res:752.2,59.0] || releasedAt(u,n1) -> releasedAt(u,n0) equal(waterLevel(skf21(u)),u)**. % 16.75/16.99 5478[0:EqR:4659.0] || -> equal(skf21(waterLevel(u)),u)**. % 16.75/16.99 5533[0:Res:1645.0,868.0] || less_or_equal(n2,u) -> less_or_equal(n3,u)* equal(u,n2). % 16.75/16.99 5712[1:Spt:563.0,563.1] || releasedAt(u,n2)* -> releasedAt(u,n1). % 16.75/16.99 5993[2:Spt:564.0,564.1] || releasedAt(u,n1)* -> releasedAt(u,n0). % 16.75/16.99 6114[0:Res:5533.1,868.0] || less_or_equal(n2,u)*+ less_or_equal(u,n3)* -> equal(u,n2) equal(n3,u). % 16.75/16.99 6220[0:Res:854.2,63.0] || -> holdsAt(waterLevel(n0),n1) releasedAt(waterLevel(n0),n1)* equal(skf15(n0,u),tapOn)** holdsAt(filling,n0). % 16.75/16.99 6222[0:MRR:6220.3,4.0] || -> holdsAt(waterLevel(n0),n1) releasedAt(waterLevel(n0),n1)* equal(skf15(n0,u),tapOn)**. % 16.75/16.99 6223[0:Rew:6222.2,854.2] || -> holdsAt(waterLevel(n0),n1) releasedAt(waterLevel(n0),n1)* happens(tapOn,n0). % 16.75/16.99 6247[0:Res:77.2,706.2] || equal(u,filling)+ equal(v,overflow) happens(v,n1)* releasedAt(u,n2)* -> . % 16.75/16.99 6649[0:Res:77.2,717.2] || equal(u,filling)+ equal(v,overflow) happens(v,n1)* holdsAt(u,n2)* -> . % 16.75/16.99 6877[0:Res:75.2,727.2] || equal(u,spilling)+ equal(v,overflow) happens(v,n1)* releasedAt(u,n2)* -> . % 16.75/16.99 6906[0:Res:50.1,728.2] || SkP0(u,v)* happens(v,n0) releasedAt(u,n1) -> . % 16.75/16.99 6927[0:Res:68.2,6906.0] || equal(u,tapOn)+ equal(v,filling) happens(u,n0)* releasedAt(v,n1)* -> . % 16.75/16.99 6997[0:Res:68.2,648.0] || equal(u,tapOn)+ equal(v,filling) happens(u,w)* -> holdsAt(v,plus(w,n1))*. % 16.75/16.99 7010[0:SpL:17.0,753.0] || releasedAt(u,n3) -> releasedAt(u,n2) releases(tapOn,u,n2)*. % 16.75/16.99 7019[0:Res:7010.2,59.0] || releasedAt(u,n3) -> releasedAt(u,n2) equal(waterLevel(skf21(u)),u)**. % 16.75/16.99 7103[0:SpL:7019.2,23.0] || releasedAt(u,n3)* equal(u,filling) -> releasedAt(u,n2). % 16.75/16.99 7144[0:Res:834.2,70.0] || equal(u,tapOff)* holdsAt(waterLevel(v),w)* -> equal(waterLevel(skf20(waterLevel(v),x)),waterLevel(v))**. % 16.75/16.99 7148[0:AED:8.0,7144.0] || holdsAt(waterLevel(u),v)*+ -> equal(waterLevel(skf20(waterLevel(u),w)),waterLevel(u))**. % 16.75/16.99 7177[0:Res:324.1,7103.0] || holdsAt(filling,n3) equal(filling,filling) -> releasedAt(filling,n2)*. % 16.75/16.99 7179[0:Obv:7177.1] || holdsAt(filling,n3) -> releasedAt(filling,n2)*. % 16.75/16.99 7183[1:Res:7179.1,5712.0] || holdsAt(filling,n3) -> releasedAt(filling,n1)*. % 16.75/16.99 7196[0:SpR:57.1,843.2] || equal(u,v)* equal(w,overflow) holdsAt(waterLevel(u),x)*+ -> initiates(w,waterLevel(v),x)*. % 16.75/16.99 7200[0:Res:843.2,85.1] || equal(u,overflow) holdsAt(waterLevel(v),w)+ happens(u,w)* -> holdsAt(waterLevel(v),plus(w,n1))*. % 16.75/16.99 7203[0:Res:843.2,727.2] || equal(u,overflow) holdsAt(waterLevel(v),n1) happens(u,n1)* releasedAt(waterLevel(v),n2)* -> . % 16.75/16.99 7225[0:SpL:18.0,565.0] || releasedAt(u,n4)*+ -> releasedAt(u,n3) happens(skf18(n3,v),n3)*. % 16.75/16.99 7226[0:SpL:17.0,565.0] || releasedAt(u,n3)* -> releasedAt(u,n2) happens(skf18(n2,v),n2)*. % 16.75/16.99 7230[0:MRR:7226.2,323.0] || releasedAt(u,n3)* -> releasedAt(u,n2). % 16.75/16.99 7400[0:EqR:647.0] || equal(u,overflow)+ happens(u,v)* -> holdsAt(spilling,plus(v,n1))*. % 16.75/16.99 7486[0:SpR:25.0,907.2] || holdsAt(u,v) -> holdsAt(u,plus(v,n1)) releasedAt(u,plus(n1,v))* equal(u,filling). % 16.75/16.99 7492[0:Res:907.2,84.0] || holdsAt(u,v)+ -> holdsAt(u,plus(v,n1))* equal(u,filling) releasedAt(u,v) happens(skf18(v,w),v)*. % 16.75/16.99 8726[0:EqR:7400.0] || happens(overflow,u) -> holdsAt(spilling,plus(u,n1))*. % 16.75/16.99 8727[0:SpR:16.0,8726.1] || happens(overflow,n1)* -> holdsAt(spilling,n2). % 16.75/16.99 8857[0:SpL:18.0,874.0] || holdsAt(u,n4) -> holdsAt(u,n3) releasedAt(u,plus(n3,n1))* happens(skf16(n3,v),n3)*. % 16.75/16.99 8858[0:SpL:17.0,874.0] || holdsAt(u,n3) -> holdsAt(u,n2) releasedAt(u,plus(n2,n1))* happens(skf16(n2,v),n2)*. % 16.75/16.99 8865[0:Rew:18.0,8857.2,25.0,8857.2] || holdsAt(u,n4)+ -> holdsAt(u,n3) releasedAt(u,n4)* happens(skf16(n3,v),n3)*. % 16.75/16.99 8866[0:Rew:17.0,8858.2,25.0,8858.2] || holdsAt(u,n3) -> holdsAt(u,n2) releasedAt(u,n3)* happens(skf16(n2,v),n2)*. % 16.75/16.99 8867[0:MRR:8866.3,323.0] || holdsAt(u,n3) -> holdsAt(u,n2) releasedAt(u,n3)*. % 16.75/16.99 8871[0:Res:8867.2,7230.0] || holdsAt(u,n3) -> holdsAt(u,n2) releasedAt(u,n2)*. % 16.75/16.99 8921[0:Res:1011.2,52.0] || releasedAt(u,v) -> releasedAt(u,plus(v,n1))* holdsAt(u,plus(v,n1)) equal(u,filling). % 16.75/16.99 9461[0:EqR:1993.0] || happens(tapOn,u) -> releasedAt(waterLevel(v),plus(u,n1))*. % 16.75/16.99 9463[0:SpR:13.0,9461.1] || happens(tapOn,n0) -> releasedAt(waterLevel(u),n1)*. % 16.75/16.99 9472[0:Res:9461.1,84.0] || happens(tapOn,u)+ -> releasedAt(waterLevel(v),u)* happens(skf18(u,w),u)*. % 16.75/16.99 9491[0:EqR:1204.0] || equal(u,overflow)+ less(v,w)* less(w,x)* happens(u,w)* -> stoppedIn(v,filling,x)*. % 16.75/16.99 9494[0:Res:9463.1,83.0] || happens(tapOn,n0) -> releasedAt(waterLevel(u),plus(n1,n1))* happens(skf17(n1,v),n1)*. % 16.75/16.99 9495[2:Res:9463.1,5993.0] || happens(tapOn,n0) -> releasedAt(waterLevel(u),n0)*. % 16.75/16.99 9496[2:MRR:9495.1,22.0] || happens(tapOn,n0)* -> . % 16.75/16.99 9499[2:Res:74.2,9496.0] || equal(n0,n0) equal(tapOn,tapOn)* -> . % 16.75/16.99 9500[2:Obv:9499.1] || -> . % 16.75/16.99 9501[2:Spt:9500.0,564.2] || -> happens(skf18(n0,u),n0)*. % 16.75/16.99 9502[0:MRR:6223.2,9463.0] || -> holdsAt(waterLevel(n0),n1) releasedAt(waterLevel(n0),n1)*. % 16.75/16.99 9508[0:Rew:16.0,9494.1] || happens(tapOn,n0) -> releasedAt(waterLevel(u),n2)* happens(skf17(n1,v),n1)*. % 16.75/16.99 9516[2:Res:9501.0,63.0] || -> equal(skf18(n0,u),tapOn)** holdsAt(filling,n0). % 16.75/16.99 9518[2:MRR:9516.1,4.0] || -> equal(skf18(n0,u),tapOn)**. % 16.75/16.99 9519[2:Rew:9518.0,9501.0] || -> happens(tapOn,n0)*. % 16.75/16.99 9520[2:MRR:9463.0,9519.0] || -> releasedAt(waterLevel(u),n1)*. % 16.75/16.99 9521[2:MRR:9508.0,9519.0] || -> releasedAt(waterLevel(u),n2)* happens(skf17(n1,v),n1)*. % 16.75/16.99 9559[3:Spt:9521.0] || -> releasedAt(waterLevel(u),n2)*. % 16.75/16.99 9560[3:MRR:7203.3,9559.0] || equal(u,overflow) holdsAt(waterLevel(v),n1)*+ happens(u,n1)* -> . % 16.75/16.99 9576[4:Spt:877.0,877.1,877.2] || holdsAt(u,n1) -> holdsAt(u,n0) releasedAt(u,n1)*. % 16.75/16.99 9930[0:SpL:5462.2,23.0] || releasedAt(u,n1)* equal(u,filling) -> releasedAt(u,n0). % 16.75/16.99 9933[0:SpL:5462.2,7148.0] || releasedAt(u,n1) holdsAt(u,v)* -> releasedAt(u,n0) equal(waterLevel(skf20(waterLevel(skf21(u)),w)),waterLevel(skf21(u)))**. % 16.75/16.99 9953[0:Rew:5462.2,9933.3] || releasedAt(u,n1)+ holdsAt(u,v)* -> releasedAt(u,n0) equal(waterLevel(skf20(u,w)),u)**. % 16.75/16.99 9982[4:Res:9576.2,9930.0] || holdsAt(u,n1) equal(u,filling) -> holdsAt(u,n0) releasedAt(u,n0)*. % 16.75/16.99 10010[1:Res:7183.1,9930.0] || holdsAt(filling,n3) equal(filling,filling) -> releasedAt(filling,n0)*. % 16.75/16.99 10012[1:Obv:10010.1] || holdsAt(filling,n3) -> releasedAt(filling,n0)*. % 16.75/16.99 10013[1:MRR:10012.1,6.0] || holdsAt(filling,n3)* -> . % 16.75/16.99 10378[0:Res:74.2,9472.0] || equal(u,n0) equal(tapOn,tapOn) -> releasedAt(waterLevel(v),u)* happens(skf18(u,w),u)*. % 16.75/16.99 10381[0:Obv:10378.1] || equal(u,n0)+ -> releasedAt(waterLevel(v),u)* happens(skf18(u,w),u)*. % 16.75/16.99 10382[0:EqR:10381.0] || -> releasedAt(waterLevel(u),n0)* happens(skf18(n0,v),n0)*. % 16.75/16.99 10416[4:Res:9982.3,6.0] || holdsAt(filling,n1)* equal(filling,filling) -> holdsAt(filling,n0). % 16.75/16.99 10421[4:Obv:10416.1] || holdsAt(filling,n1)* -> holdsAt(filling,n0). % 16.75/16.99 10422[4:MRR:10421.1,4.0] || holdsAt(filling,n1)* -> . % 16.75/16.99 10873[0:EqR:6247.0] || equal(u,overflow) happens(u,n1)* releasedAt(filling,n2) -> . % 16.75/16.99 10951[0:EqR:6877.0] || equal(u,overflow) happens(u,n1)* releasedAt(spilling,n2) -> . % 16.75/16.99 11620[0:EqR:6997.0] || equal(u,filling) happens(tapOn,v) -> holdsAt(u,plus(v,n1))*. % 16.75/16.99 11622[0:SpR:13.0,11620.2] || equal(u,filling) happens(tapOn,n0)* -> holdsAt(u,n1)*. % 16.75/16.99 11639[2:MRR:11622.1,9519.0] || equal(u,filling) -> holdsAt(u,n1)*. % 16.75/16.99 11643[4:Res:11639.1,10422.0] || equal(filling,filling)* -> . % 16.75/16.99 11645[2:Res:11639.1,97.0] || equal(u,filling) -> holdsAt(u,plus(n1,n1)) releasedAt(u,plus(n1,n1))* happens(skf15(n1,v),n1)*. % 16.75/16.99 11655[4:Obv:11643.0] || -> . % 16.75/16.99 11656[2:Rew:16.0,11645.2,16.0,11645.1] || equal(u,filling)+ -> holdsAt(u,n2) releasedAt(u,n2)* happens(skf15(n1,v),n1)*. % 16.75/16.99 11658[4:Spt:11655.0,877.3] || -> happens(skf16(n0,u),n0)*. % 16.75/16.99 11819[0:SpR:18.0,7486.2] || holdsAt(u,n3) -> holdsAt(u,plus(n3,n1))* releasedAt(u,n4) equal(u,filling). % 16.75/16.99 11820[0:SpR:17.0,7486.2] || holdsAt(u,n2) -> holdsAt(u,plus(n2,n1))* releasedAt(u,n3) equal(u,filling). % 16.75/16.99 11839[0:Rew:18.0,11819.1,25.0,11819.1] || holdsAt(u,n3) -> holdsAt(u,n4) releasedAt(u,n4)* equal(u,filling). % 16.75/16.99 11840[0:Rew:17.0,11820.1,25.0,11820.1] || holdsAt(u,n2) -> holdsAt(u,n3) releasedAt(u,n3)* equal(u,filling). % 16.75/16.99 11992[0:SpR:16.0,8921.1] || releasedAt(u,n1) -> releasedAt(u,n2) holdsAt(u,plus(n1,n1))* equal(u,filling). % 16.75/16.99 12011[0:Rew:16.0,11992.2] || releasedAt(u,n1) -> releasedAt(u,n2)* holdsAt(u,n2) equal(u,filling). % 16.75/16.99 12144[0:Res:11840.2,7230.0] || holdsAt(u,n2) -> holdsAt(u,n3) equal(u,filling) releasedAt(u,n2)*. % 16.75/16.99 12480[5:Spt:11656.0,11656.1,11656.2] || equal(u,filling) -> holdsAt(u,n2) releasedAt(u,n2)*. % 16.75/16.99 12484[5:Res:12480.2,5712.0] || equal(u,filling) -> holdsAt(u,n2) releasedAt(u,n1)*. % 16.75/16.99 12494[5:Res:12484.2,9930.0] || equal(u,filling) equal(u,filling) -> holdsAt(u,n2) releasedAt(u,n0)*. % 16.75/16.99 12496[5:Obv:12494.0] || equal(u,filling) -> holdsAt(u,n2) releasedAt(u,n0)*. % 16.75/16.99 12508[5:Res:12496.2,6.0] || equal(filling,filling) -> holdsAt(filling,n2)*. % 16.75/16.99 12513[5:Obv:12508.0] || -> holdsAt(filling,n2)*. % 16.75/16.99 12514[5:MRR:12513.0,1.0] || -> . % 16.75/16.99 12517[5:Spt:12514.0,11656.3] || -> happens(skf15(n1,u),n1)*. % 16.75/16.99 12519[5:Res:12517.0,72.0] || -> equal(n1,n0) holdsAt(waterLevel(n3),n1)*. % 16.75/16.99 12523[5:Res:12517.0,61.0] || -> equal(n1,n0) holdsAt(filling,n1)*. % 16.75/16.99 12527[5:MRR:12523.0,322.0] || -> holdsAt(filling,n1)*. % 16.75/16.99 12528[5:MRR:12519.0,322.0] || -> holdsAt(waterLevel(n3),n1)*. % 16.75/16.99 12628[5:Res:12528.0,9560.1] || equal(u,overflow) happens(u,n1)* -> . % 16.75/16.99 12631[5:Res:12528.0,825.3] || equal(n3,n3) equal(u,overflow) holdsAt(filling,n1) -> happens(u,n1)*. % 16.75/16.99 12635[5:Obv:12631.0] || equal(u,overflow) holdsAt(filling,n1) -> happens(u,n1)*. % 16.75/16.99 12636[5:MRR:12635.1,12527.0] || equal(u,overflow) -> happens(u,n1)*. % 16.75/16.99 12637[5:MRR:12636.1,12628.1] || equal(u,overflow)* -> . % 16.75/16.99 12638[5:UnC:12637.0,5478.0] || -> . % 16.75/16.99 12641[3:Spt:12638.0,9521.1] || -> happens(skf17(n1,u),n1)*. % 16.75/16.99 12644[3:Res:12641.0,72.0] || -> equal(n1,n0) holdsAt(waterLevel(n3),n1)*. % 16.75/16.99 12645[3:Res:12641.0,60.0] || -> equal(n1,n0) equal(skf17(n1,u),overflow)**. % 16.75/16.99 12648[3:Res:12641.0,61.0] || -> equal(n1,n0) holdsAt(filling,n1)*. % 16.75/16.99 12649[3:MRR:12648.0,322.0] || -> holdsAt(filling,n1)*. % 16.75/16.99 12650[3:MRR:12644.0,322.0] || -> holdsAt(waterLevel(n3),n1)*. % 16.75/16.99 12651[3:MRR:12645.0,322.0] || -> equal(skf17(n1,u),overflow)**. % 16.75/16.99 12652[3:Rew:12651.0,12641.0] || -> happens(overflow,n1)*. % 16.75/16.99 12657[3:MRR:8727.0,12652.0] || -> holdsAt(spilling,n2)*. % 16.75/16.99 12661[3:Res:12649.0,1208.0] || less(u,n1) less(n1,v) -> holdsAt(filling,plus(n1,n1)) releasedAt(filling,plus(n1,n1))* stoppedIn(u,filling,v)*. % 16.75/16.99 12665[3:Rew:16.0,12661.3,16.0,12661.2] || less(u,n1) less(n1,v) -> holdsAt(filling,n2) releasedAt(filling,n2) stoppedIn(u,filling,v)*. % 16.75/16.99 12666[3:MRR:12665.2,1.0] || less(u,n1) less(n1,v) -> releasedAt(filling,n2) stoppedIn(u,filling,v)*. % 16.75/16.99 12678[4:Spt:877.0,877.1,877.2] || holdsAt(u,n1) -> holdsAt(u,n0) releasedAt(u,n1)*. % 16.75/16.99 12684[4:Res:12678.2,9930.0] || holdsAt(u,n1) equal(u,filling) -> holdsAt(u,n0) releasedAt(u,n0)*. % 16.75/16.99 12686[4:MRR:12684.0,11639.1] || equal(u,filling) -> holdsAt(u,n0) releasedAt(u,n0)*. % 16.75/16.99 12698[3:Res:12650.0,94.2] || equal(u,overflow) holdsAt(filling,n1) -> happens(u,n1)*. % 16.75/16.99 12700[3:Res:12650.0,7148.0] || -> equal(waterLevel(skf20(waterLevel(n3),u)),waterLevel(n3))**. % 16.75/16.99 12701[3:Res:12650.0,80.0] || holdsAt(waterLevel(u),n1)* -> equal(u,n3). % 16.75/16.99 12702[3:Res:12650.0,7200.1] || equal(u,overflow) happens(u,n1)* -> holdsAt(waterLevel(n3),plus(n1,n1))*. % 16.75/16.99 12704[3:Res:12650.0,7196.2] || equal(n3,u) equal(v,overflow) -> initiates(v,waterLevel(u),n1)*. % 16.75/16.99 12707[3:MRR:12698.1,12649.0] || equal(u,overflow) -> happens(u,n1)*. % 16.75/16.99 12708[3:MRR:6247.2,12707.1] || equal(u,filling) equal(v,overflow)* releasedAt(u,n2)* -> . % 16.75/16.99 12709[3:MRR:6649.2,12707.1] || equal(u,filling) equal(v,overflow)* holdsAt(u,n2)* -> . % 16.75/16.99 12711[3:MRR:10951.1,12707.1] || equal(u,overflow)* releasedAt(spilling,n2)* -> . % 16.75/16.99 12712[3:MRR:10873.1,12707.1] || equal(u,overflow)* releasedAt(filling,n2)* -> . % 16.75/16.99 12713[3:MRR:7203.2,12707.1] || equal(u,overflow)* holdsAt(waterLevel(v),n1) releasedAt(waterLevel(v),n2)* -> . % 16.75/16.99 12714[3:AED:8.0,12711.0] || releasedAt(spilling,n2)* -> . % 16.75/16.99 12716[3:AED:8.0,12712.0] || releasedAt(filling,n2)* -> . % 16.75/16.99 12718[3:MRR:12666.2,12716.0] || less(u,n1) less(n1,v) -> stoppedIn(u,filling,v)*. % 16.75/16.99 12719[3:AED:8.0,12708.1] || equal(u,filling) releasedAt(u,n2)* -> . % 16.75/16.99 12721[3:AED:8.0,12709.1] || equal(u,filling) holdsAt(u,n2)* -> . % 16.75/16.99 12724[3:Rew:16.0,12702.2] || equal(u,overflow) happens(u,n1)* -> holdsAt(waterLevel(n3),n2)*. % 16.75/16.99 12725[3:MRR:12724.1,12707.1] || equal(u,overflow)*+ -> holdsAt(waterLevel(n3),n2)*. % 16.75/16.99 12726[3:AED:8.0,12713.0] || holdsAt(waterLevel(u),n1) releasedAt(waterLevel(u),n2)* -> . % 16.75/16.99 12730[3:Res:12144.3,12714.0] || holdsAt(spilling,n2) -> holdsAt(spilling,n3)* equal(spilling,filling). % 16.75/16.99 12734[3:MRR:12730.0,12730.2,12657.0,11.0] || -> holdsAt(spilling,n3)*. % 16.75/16.99 12746[3:Res:8871.2,12719.1] || holdsAt(u,n3)* equal(u,filling) -> holdsAt(u,n2). % 16.75/16.99 12748[3:MRR:12746.2,12721.1] || holdsAt(u,n3)* equal(u,filling) -> . % 16.75/16.99 12795[3:SpR:12700.0,5478.0] || -> equal(skf20(waterLevel(n3),u),skf21(waterLevel(n3)))**. % 16.75/16.99 12869[3:Rew:5478.0,12795.0] || -> equal(skf20(waterLevel(n3),u),n3)**. % 16.75/16.99 12933[3:EqR:12725.0] || -> holdsAt(waterLevel(n3),n2)*. % 16.75/16.99 12937[3:Res:12933.0,97.0] || -> holdsAt(waterLevel(n3),plus(n2,n1)) releasedAt(waterLevel(n3),plus(n2,n1))* happens(skf15(n2,u),n2)*. % 16.75/16.99 12950[3:Rew:17.0,12937.1,25.0,12937.1,17.0,12937.0,25.0,12937.0] || -> holdsAt(waterLevel(n3),n3) releasedAt(waterLevel(n3),n3) happens(skf15(n2,u),n2)*. % 16.75/16.99 12951[3:MRR:12950.2,323.0] || -> holdsAt(waterLevel(n3),n3) releasedAt(waterLevel(n3),n3)*. % 16.75/16.99 12966[3:Res:12144.3,12726.1] || holdsAt(waterLevel(u),n2) holdsAt(waterLevel(u),n1) -> holdsAt(waterLevel(u),n3)* equal(waterLevel(u),filling). % 16.75/16.99 12967[3:Res:12011.1,12726.1] || releasedAt(waterLevel(u),n1)* holdsAt(waterLevel(u),n1) -> holdsAt(waterLevel(u),n2) equal(waterLevel(u),filling). % 16.75/16.99 12972[3:MRR:12966.3,23.0] || holdsAt(waterLevel(u),n2) holdsAt(waterLevel(u),n1) -> holdsAt(waterLevel(u),n3)*. % 16.75/16.99 12973[3:MRR:12967.0,12967.3,9520.0,23.0] || holdsAt(waterLevel(u),n1) -> holdsAt(waterLevel(u),n2)*. % 16.75/16.99 12974[3:MRR:12972.0,12973.1] || holdsAt(waterLevel(u),n1) -> holdsAt(waterLevel(u),n3)*. % 16.75/16.99 13018[3:SpL:5462.2,12701.0] || releasedAt(u,n1)* holdsAt(u,n1) -> releasedAt(u,n0) equal(skf21(u),n3). % 16.75/16.99 13158[3:SpR:57.1,12974.1] || equal(u,v)* holdsAt(waterLevel(u),n1)*+ -> holdsAt(waterLevel(v),n3)*. % 16.75/16.99 13179[4:Res:12686.2,6.0] || equal(filling,filling) -> holdsAt(filling,n0)*. % 16.75/16.99 13184[4:Obv:13179.0] || -> holdsAt(filling,n0)*. % 16.75/16.99 13185[4:MRR:13184.0,4.0] || -> . % 16.75/16.99 13189[4:Spt:13185.0,877.3] || -> happens(skf16(n0,u),n0)*. % 16.75/16.99 13195[4:Res:13189.0,63.0] || -> equal(skf16(n0,u),tapOn)** holdsAt(filling,n0). % 16.75/16.99 13199[4:MRR:13195.1,4.0] || -> equal(skf16(n0,u),tapOn)**. % 16.75/16.99 13208[4:SpR:13199.0,99.3] || holdsAt(u,plus(n0,n1)) -> holdsAt(u,n0) releasedAt(u,plus(n0,n1))* initiates(tapOn,u,n0). % 16.75/16.99 13210[4:Rew:13.0,13208.2,13.0,13208.0] || holdsAt(u,n1) -> holdsAt(u,n0) releasedAt(u,n1) initiates(tapOn,u,n0)*. % 16.75/16.99 13215[5:Spt:12951.0] || -> holdsAt(waterLevel(n3),n3)*. % 16.75/16.99 13219[5:Res:13215.0,97.0] || -> holdsAt(waterLevel(n3),plus(n3,n1)) releasedAt(waterLevel(n3),plus(n3,n1))* happens(skf15(n3,u),n3)*. % 16.75/16.99 13233[5:Rew:18.0,13219.1,25.0,13219.1,18.0,13219.0,25.0,13219.0] || -> holdsAt(waterLevel(n3),n4) releasedAt(waterLevel(n3),n4) happens(skf15(n3,u),n3)*. % 16.75/16.99 13235[6:Spt:7225.0,7225.1] || releasedAt(u,n4)* -> releasedAt(u,n3). % 16.75/16.99 13236[6:Res:11839.2,13235.0] || holdsAt(u,n3) -> holdsAt(u,n4) equal(u,filling) releasedAt(u,n3)*. % 16.75/16.99 13237[6:MRR:13236.2,12748.1] || holdsAt(u,n3) -> holdsAt(u,n4) releasedAt(u,n3)*. % 16.75/16.99 13296[7:Spt:8865.0,8865.1,8865.2] || holdsAt(u,n4) -> holdsAt(u,n3) releasedAt(u,n4)*. % 16.75/16.99 13300[7:Res:13296.2,13235.0] || holdsAt(u,n4) -> holdsAt(u,n3) releasedAt(u,n3)*. % 16.75/16.99 13350[6:Res:13237.2,7230.0] || holdsAt(u,n3) -> holdsAt(u,n4) releasedAt(u,n2)*. % 16.75/16.99 13357[7:Res:13300.2,7230.0] || holdsAt(u,n4) -> holdsAt(u,n3) releasedAt(u,n2)*. % 16.75/16.99 13391[6:Res:13350.2,12714.0] || holdsAt(spilling,n3) -> holdsAt(spilling,n4)*. % 16.75/16.99 13394[6:MRR:13391.0,12734.0] || -> holdsAt(spilling,n4)*. % 16.75/16.99 13439[7:Res:13357.2,12716.0] || holdsAt(filling,n4)* -> holdsAt(filling,n3). % 16.75/16.99 13441[7:MRR:13439.1,10013.0] || holdsAt(filling,n4)* -> . % 16.75/16.99 13591[0:EqR:9491.0] || less(u,v)*+ less(v,w)* happens(overflow,v)* -> stoppedIn(u,filling,w)*. % 16.75/16.99 13652[3:Res:12718.2,65.0] || less(u,n1)+ less(n1,v)* -> less(u,skf11(u,w,x))*. % 16.75/16.99 13723[6:Res:13394.0,7492.0] || -> holdsAt(spilling,plus(n4,n1)) equal(spilling,filling) releasedAt(spilling,n4) happens(skf18(n4,u),n4)*. % 16.75/16.99 13727[6:Rew:25.0,13723.0] || -> holdsAt(spilling,plus(n1,n4)) equal(spilling,filling) releasedAt(spilling,n4) happens(skf18(n4,u),n4)*. % 16.75/16.99 13728[6:MRR:13727.1,11.0] || -> holdsAt(spilling,plus(n1,n4)) releasedAt(spilling,n4) happens(skf18(n4,u),n4)*. % 16.75/16.99 13779[8:Spt:13233.0] || -> holdsAt(waterLevel(n3),n4)*. % 16.75/16.99 13780[8:SpR:57.1,13779.0] || equal(n3,u) -> holdsAt(waterLevel(u),n4)*. % 16.75/16.99 13806[8:SpR:5462.2,13780.1] || releasedAt(u,n1)* equal(skf21(u),n3) -> releasedAt(u,n0) holdsAt(u,n4). % 16.75/16.99 13862[9:Spt:13728.2] || -> happens(skf18(n4,u),n4)*. % 16.75/16.99 13866[9:Res:13862.0,60.0] || -> equal(n4,n0) equal(skf18(n4,u),overflow)**. % 16.75/16.99 13868[9:Res:13862.0,63.0] || -> equal(skf18(n4,u),tapOn)** holdsAt(filling,n4). % 16.75/16.99 13871[9:MRR:13866.0,319.0] || -> equal(skf18(n4,u),overflow)**. % 16.75/16.99 13873[9:Rew:13871.0,13868.0] || -> equal(overflow,tapOn) holdsAt(filling,n4)*. % 16.75/16.99 13874[9:MRR:13873.0,13873.1,10.0,13441.0] || -> . % 16.75/16.99 13875[9:Spt:13874.0,13728.0,13728.1] || -> holdsAt(spilling,plus(n1,n4))* releasedAt(spilling,n4). % 16.75/16.99 13908[3:Res:12704.2,727.2] || equal(n3,u) equal(v,overflow) happens(v,n1)* releasedAt(waterLevel(u),n2)* -> . % 16.75/16.99 13912[3:MRR:13908.2,12707.1] || equal(n3,u) equal(v,overflow)* releasedAt(waterLevel(u),n2)*+ -> . % 16.75/16.99 13919[3:SpL:5462.2,13912.2] || releasedAt(u,n1) equal(skf21(u),n3) equal(v,overflow)* releasedAt(u,n2)* -> releasedAt(u,n0). % 16.75/16.99 13933[3:AED:8.0,13919.2] || releasedAt(u,n1) equal(skf21(u),n3) releasedAt(u,n2)* -> releasedAt(u,n0). % 16.75/16.99 13934[3:MRR:13933.0,5712.1] || equal(skf21(u),n3) releasedAt(u,n2)* -> releasedAt(u,n0). % 16.75/16.99 14041[3:Res:12650.0,13158.1] || equal(n3,u) -> holdsAt(waterLevel(u),n3)*. % 16.75/16.99 14821[3:Res:256.1,13652.0] || less(n1,u)* -> equal(n1,n0) less(n0,skf11(n0,v,w))*. % 16.75/16.99 14829[3:MRR:14821.1,322.0] || less(n1,u)*+ -> less(n0,skf11(n0,v,w))*. % 16.75/16.99 14830[3:Res:45.1,14829.0] || less_or_equal(n1,n8) -> less(n0,skf11(n0,u,v))*. % 16.75/16.99 14844[3:MRR:14830.0,900.0] || -> less(n0,skf11(n0,u,v))*. % 16.75/16.99 14889[3:Res:14844.0,356.1] || less_or_equal(skf11(n0,u,v),n0)* -> . % 16.75/16.99 14894[3:Res:1887.0,14889.0] || -> less_or_equal(n1,skf11(n0,u,v))*. % 16.75/16.99 14898[3:Res:14894.0,868.0] || less_or_equal(skf11(n0,u,v),n1)* -> equal(skf11(n0,u,v),n1). % 16.75/16.99 17141[0:EqR:6927.0] || equal(u,filling) happens(tapOn,n0)* releasedAt(u,n1)* -> . % 16.75/16.99 18846[0:Res:29.1,13591.0] || less_or_equal(u,n0) less(n1,v) happens(overflow,n1) -> stoppedIn(u,filling,v)*. % 16.75/16.99 18854[0:Res:256.1,13591.0] || less(u,v)*+ happens(overflow,u)* -> equal(n0,u) stoppedIn(n0,filling,v)*. % 16.75/16.99 18864[3:MRR:18846.2,12652.0] || less_or_equal(u,n0) less(n1,v) -> stoppedIn(u,filling,v)*. % 16.75/16.99 18867[3:Res:18864.2,64.0] || less_or_equal(u,n0) less(n1,v) -> less(skf11(u,v,w),v)*. % 16.75/16.99 18877[3:Res:18867.2,30.0] || less_or_equal(u,n0) less(n1,n2) -> less_or_equal(skf11(u,n2,v),n1)*. % 16.75/16.99 19006[3:Res:18877.2,14898.0] || less_or_equal(n0,n0) less(n1,n2) -> equal(skf11(n0,n2,u),n1)**. % 16.75/16.99 19007[3:MRR:19006.0,2191.0] || less(n1,n2) -> equal(skf11(n0,n2,u),n1)**. % 16.75/16.99 19038[3:SpR:19007.1,14844.0] || less(n1,n2)* -> less(n0,n1). % 16.75/16.99 19097[3:Res:31.1,19038.0] || less_or_equal(n1,n1) -> less(n0,n1)*. % 16.75/16.99 19101[3:MRR:19097.0,2191.0] || -> less(n0,n1)*. % 16.75/16.99 19103[3:MRR:5454.2,19101.0] || holdsAt(waterLevel(n0),u)+ happens(v,u) initiates(v,filling,u)* -> holdsAt(waterLevel(n1),plus(u,n1)) stoppedIn(u,filling,plus(u,n1))*. % 16.75/16.99 19222[3:Res:3.0,19103.0] || happens(u,n0) initiates(u,filling,n0)* -> holdsAt(waterLevel(n1),plus(n0,n1)) stoppedIn(n0,filling,plus(n0,n1))*. % 16.75/16.99 19254[3:Rew:13.0,19222.3,13.0,19222.2] || happens(u,n0) initiates(u,filling,n0)* -> holdsAt(waterLevel(n1),n1) stoppedIn(n0,filling,n1). % 16.75/16.99 19944[0:Res:45.1,18854.0] || less_or_equal(u,n8)+ happens(overflow,u)* -> equal(n0,u) stoppedIn(n0,filling,n9)*. % 16.75/16.99 19945[0:Res:43.1,18854.0] || less_or_equal(u,n7)+ happens(overflow,u)* -> equal(n0,u) stoppedIn(n0,filling,n8)*. % 16.75/16.99 19946[0:Res:41.1,18854.0] || less_or_equal(u,n6)+ happens(overflow,u)* -> equal(n0,u) stoppedIn(n0,filling,n7)*. % 16.75/16.99 19947[0:Res:39.1,18854.0] || less_or_equal(u,n5)+ happens(overflow,u)* -> equal(n0,u) stoppedIn(n0,filling,n6)*. % 16.75/16.99 19948[0:Res:37.1,18854.0] || less_or_equal(u,n4)+ happens(overflow,u)* -> equal(n0,u) stoppedIn(n0,filling,n5)*. % 16.75/16.99 19949[0:Res:35.1,18854.0] || less_or_equal(u,n3)+ happens(overflow,u)* -> equal(n0,u) stoppedIn(n0,filling,n4)*. % 16.75/16.99 19967[0:Res:265.1,18854.0] || happens(overflow,n1) -> equal(n1,u) less_or_equal(u,n0) equal(n1,n0) stoppedIn(n0,filling,u)*. % 16.75/16.99 23880[10:Spt:19944.0,19944.1,19944.2] || less_or_equal(u,n8) happens(overflow,u)* -> equal(n0,u). % 16.75/16.99 23881[10:Res:12707.1,23880.1] || equal(overflow,overflow) less_or_equal(n1,n8)* -> equal(n1,n0). % 16.75/16.99 23895[10:Obv:23881.0] || less_or_equal(n1,n8)* -> equal(n1,n0). % 16.75/16.99 23896[10:MRR:23895.0,23895.1,900.0,322.0] || -> . % 16.75/16.99 23927[10:Spt:23896.0,19944.3] || -> stoppedIn(n0,filling,n9)*. % 16.75/16.99 23985[11:Spt:19945.0,19945.1,19945.2] || less_or_equal(u,n7) happens(overflow,u)* -> equal(n0,u). % 16.75/16.99 23986[11:Res:12707.1,23985.1] || equal(overflow,overflow) less_or_equal(n1,n7)* -> equal(n1,n0). % 16.75/16.99 24000[11:Obv:23986.0] || less_or_equal(n1,n7)* -> equal(n1,n0). % 16.75/16.99 24001[11:MRR:24000.0,24000.1,1008.0,322.0] || -> . % 16.75/16.99 24030[11:Spt:24001.0,19945.3] || -> stoppedIn(n0,filling,n8)*. % 16.75/16.99 24215[12:Spt:19946.0,19946.1,19946.2] || less_or_equal(u,n6) happens(overflow,u)* -> equal(n0,u). % 16.75/16.99 24216[12:Res:12707.1,24215.1] || equal(overflow,overflow) less_or_equal(n1,n6)* -> equal(n1,n0). % 16.75/16.99 24230[12:Obv:24216.0] || less_or_equal(n1,n6)* -> equal(n1,n0). % 16.75/16.99 24231[12:MRR:24230.0,24230.1,1197.0,322.0] || -> . % 16.75/16.99 24260[12:Spt:24231.0,19946.3] || -> stoppedIn(n0,filling,n7)*. % 16.75/16.99 24345[13:Spt:19947.0,19947.1,19947.2] || less_or_equal(u,n5) happens(overflow,u)* -> equal(n0,u). % 16.75/16.99 24346[13:Res:12707.1,24345.1] || equal(overflow,overflow) less_or_equal(n1,n5)* -> equal(n1,n0). % 16.75/16.99 24360[13:Obv:24346.0] || less_or_equal(n1,n5)* -> equal(n1,n0). % 16.75/16.99 24361[13:MRR:24360.0,24360.1,1449.0,322.0] || -> . % 16.75/16.99 24390[13:Spt:24361.0,19947.3] || -> stoppedIn(n0,filling,n6)*. % 16.75/16.99 24447[14:Spt:19948.0,19948.1,19948.2] || less_or_equal(u,n4) happens(overflow,u)* -> equal(n0,u). % 16.75/16.99 24448[14:Res:12707.1,24447.1] || equal(overflow,overflow) less_or_equal(n1,n4)* -> equal(n1,n0). % 16.75/16.99 24462[14:Obv:24448.0] || less_or_equal(n1,n4)* -> equal(n1,n0). % 16.75/16.99 24463[14:MRR:24462.0,24462.1,1561.0,322.0] || -> . % 16.75/16.99 24492[14:Spt:24463.0,19948.3] || -> stoppedIn(n0,filling,n5)*. % 16.75/16.99 24537[15:Spt:19949.0,19949.1,19949.2] || less_or_equal(u,n3) happens(overflow,u)* -> equal(n0,u). % 16.75/16.99 24538[15:Res:12707.1,24537.1] || equal(overflow,overflow) less_or_equal(n1,n3)* -> equal(n1,n0). % 16.75/16.99 24552[15:Obv:24538.0] || less_or_equal(n1,n3)* -> equal(n1,n0). % 16.75/16.99 24553[15:MRR:24552.0,24552.1,1599.0,322.0] || -> . % 16.75/16.99 24582[15:Spt:24553.0,19949.3] || -> stoppedIn(n0,filling,n4)*. % 16.75/16.99 26946[16:Spt:19254.3] || -> stoppedIn(n0,filling,n1)*. % 16.75/16.99 26949[16:Res:26946.0,64.0] || -> less(skf11(n0,n1,u),n1)*. % 16.75/16.99 26980[16:Res:26949.0,356.1] || less_or_equal(n1,skf11(n0,n1,u))* -> . % 16.75/16.99 26993[16:MRR:26980.0,14894.0] || -> . % 16.75/16.99 26996[16:Spt:26993.0,19254.3,26946.0] || stoppedIn(n0,filling,n1)* -> . % 16.75/16.99 26997[16:Spt:26993.0,19254.0,19254.1,19254.2] || happens(u,n0) initiates(u,filling,n0)* -> holdsAt(waterLevel(n1),n1). % 16.75/16.99 27002[16:Res:13210.3,26997.1] || holdsAt(filling,n1) happens(tapOn,n0) -> holdsAt(filling,n0) releasedAt(filling,n1) holdsAt(waterLevel(n1),n1)*. % 16.75/16.99 27003[16:MRR:27002.0,27002.1,27002.2,12649.0,9519.0,4.0] || -> releasedAt(filling,n1) holdsAt(waterLevel(n1),n1)*. % 16.75/16.99 27126[17:Spt:27003.1] || -> holdsAt(waterLevel(n1),n1)*. % 16.75/16.99 27174[17:Res:27126.0,12701.0] || -> equal(n3,n1)**. % 16.75/16.99 27175[17:MRR:27174.0,471.0] || -> . % 16.75/16.99 27201[17:Spt:27175.0,27003.1,27126.0] || holdsAt(waterLevel(n1),n1)* -> . % 16.75/16.99 27202[17:Spt:27175.0,27003.0] || -> releasedAt(filling,n1)*. % 16.75/16.99 27214[17:Res:27202.0,13806.0] || equal(skf21(filling),n3) -> releasedAt(filling,n0)* holdsAt(filling,n4). % 16.75/16.99 27219[17:Res:27202.0,13018.0] || holdsAt(filling,n1) -> releasedAt(filling,n0)* equal(skf21(filling),n3). % 16.75/16.99 27233[17:MRR:27214.1,27214.2,6.0,13441.0] || equal(skf21(filling),n3)** -> . % 16.75/16.99 27234[17:MRR:27219.0,27219.1,12649.0,6.0] || -> equal(skf21(filling),n3)**. % 16.75/16.99 27235[17:MRR:27234.0,27233.0] || -> . % 16.75/16.99 27242[8:Spt:27235.0,13233.0,13779.0] || holdsAt(waterLevel(n3),n4)* -> . % 16.75/16.99 27243[8:Spt:27235.0,13233.1,13233.2] || -> releasedAt(waterLevel(n3),n4) happens(skf15(n3,u),n3)*. % 16.75/16.99 27289[9:Spt:27243.1] || -> happens(skf15(n3,u),n3)*. % 16.75/16.99 27292[9:Res:27289.0,60.0] || -> equal(n3,n0) equal(skf15(n3,u),overflow)**. % 16.75/16.99 27294[9:Res:27289.0,63.0] || -> equal(skf15(n3,u),tapOn)** holdsAt(filling,n3). % 16.75/16.99 27298[9:MRR:27292.0,320.0] || -> equal(skf15(n3,u),overflow)**. % 16.75/16.99 27301[9:Rew:27298.0,27294.0] || -> equal(overflow,tapOn) holdsAt(filling,n3)*. % 16.75/16.99 27302[9:MRR:27301.0,27301.1,10.0,10013.0] || -> . % 16.75/16.99 27304[9:Spt:27302.0,27243.0] || -> releasedAt(waterLevel(n3),n4)*. % 16.75/16.99 27313[9:Res:27304.0,13235.0] || -> releasedAt(waterLevel(n3),n3)*. % 16.75/16.99 27331[9:Res:27313.0,7230.0] || -> releasedAt(waterLevel(n3),n2)*. % 16.75/16.99 27346[9:Res:27331.0,13934.1] || equal(skf21(waterLevel(n3)),n3) -> releasedAt(waterLevel(n3),n0)*. % 16.75/16.99 27363[9:Rew:5478.0,27346.0] || equal(n3,n3) -> releasedAt(waterLevel(n3),n0)*. % 16.75/16.99 27364[9:Obv:27363.0] || -> releasedAt(waterLevel(n3),n0)*. % 16.75/16.99 27365[9:MRR:27364.0,22.0] || -> . % 16.75/16.99 27372[7:Spt:27365.0,8865.3] || -> happens(skf16(n3,u),n3)*. % 16.75/16.99 27394[7:Res:27372.0,60.0] || -> equal(n3,n0) equal(skf16(n3,u),overflow)**. % 16.75/16.99 27396[7:Res:27372.0,63.0] || -> equal(skf16(n3,u),tapOn)** holdsAt(filling,n3). % 16.75/16.99 27399[7:MRR:27394.0,320.0] || -> equal(skf16(n3,u),overflow)**. % 16.75/16.99 27451[7:Rew:27399.0,27396.0] || -> equal(overflow,tapOn) holdsAt(filling,n3)*. % 16.75/16.99 27452[7:MRR:27451.0,27451.1,10.0,10013.0] || -> . % 16.75/16.99 27453[6:Spt:27452.0,7225.2] || -> happens(skf18(n3,u),n3)*. % 16.75/16.99 27463[6:Res:27453.0,60.0] || -> equal(n3,n0) equal(skf18(n3,u),overflow)**. % 16.75/16.99 27465[6:Res:27453.0,63.0] || -> equal(skf18(n3,u),tapOn)** holdsAt(filling,n3). % 16.75/16.99 27468[6:MRR:27463.0,320.0] || -> equal(skf18(n3,u),overflow)**. % 16.75/16.99 27526[6:Rew:27468.0,27465.0] || -> equal(overflow,tapOn) holdsAt(filling,n3)*. % 16.75/16.99 27527[6:MRR:27526.0,27526.1,10.0,10013.0] || -> . % 16.75/16.99 27529[5:Spt:27527.0,12951.0,13215.0] || holdsAt(waterLevel(n3),n3)* -> . % 16.75/16.99 27530[5:Spt:27527.0,12951.1] || -> releasedAt(waterLevel(n3),n3)*. % 16.75/16.99 27557[5:SpL:57.1,27529.0] || equal(u,n3) holdsAt(waterLevel(u),n3)* -> . % 16.75/16.99 27564[5:MRR:27557.1,14041.1] || equal(u,n3)* -> . % 16.75/16.99 27565[5:UnC:27564.0,12869.0] || -> . % 16.75/16.99 27566[1:Spt:27565.0,563.2] || -> happens(skf18(n1,u),n1)*. % 16.75/16.99 27567[0:MRR:10382.0,22.0] || -> happens(skf18(n0,u),n0)*. % 16.75/16.99 27591[0:MRR:19967.3,322.0] || happens(overflow,n1) -> equal(n1,u) less_or_equal(u,n0) stoppedIn(n0,filling,u)*. % 16.75/16.99 27730[1:Res:27566.0,72.0] || -> equal(n1,n0) holdsAt(waterLevel(n3),n1)*. % 16.75/16.99 27731[1:Res:27566.0,60.0] || -> equal(n1,n0) equal(skf18(n1,u),overflow)**. % 16.75/16.99 27734[1:Res:27566.0,61.0] || -> equal(n1,n0) holdsAt(filling,n1)*. % 16.75/16.99 27735[1:MRR:27734.0,322.0] || -> holdsAt(filling,n1)*. % 16.75/16.99 27739[1:MRR:27730.0,322.0] || -> holdsAt(waterLevel(n3),n1)*. % 16.75/16.99 27740[1:MRR:27731.0,322.0] || -> equal(skf18(n1,u),overflow)**. % 16.75/16.99 27741[1:Rew:27740.0,27566.0] || -> happens(overflow,n1)*. % 16.75/16.99 27752[1:MRR:27591.0,27741.0] || -> equal(n1,u) less_or_equal(u,n0) stoppedIn(n0,filling,u)*. % 16.75/16.99 27810[1:Res:27739.0,94.2] || equal(u,overflow) holdsAt(filling,n1) -> happens(u,n1)*. % 16.75/16.99 27814[1:Res:27739.0,80.0] || holdsAt(waterLevel(u),n1)* -> equal(u,n3). % 16.75/16.99 27827[1:MRR:27810.1,27735.0] || equal(u,overflow) -> happens(u,n1)*. % 16.75/16.99 27833[1:MRR:7203.2,27827.1] || equal(u,overflow)* holdsAt(waterLevel(v),n1) releasedAt(waterLevel(v),n2)* -> . % 16.75/16.99 27845[1:AED:8.0,27833.0] || holdsAt(waterLevel(u),n1) releasedAt(waterLevel(u),n2)* -> . % 16.75/16.99 27861[2:Spt:9502.0] || -> holdsAt(waterLevel(n0),n1)*. % 16.75/16.99 27951[0:Res:27567.0,63.0] || -> equal(skf18(n0,u),tapOn)** holdsAt(filling,n0). % 16.75/16.99 27953[0:MRR:27951.1,4.0] || -> equal(skf18(n0,u),tapOn)**. % 16.75/16.99 27954[0:Rew:27953.0,27567.0] || -> happens(tapOn,n0)*. % 16.75/16.99 27956[0:MRR:11622.1,27954.0] || equal(u,filling) -> holdsAt(u,n1)*. % 16.75/16.99 27959[0:MRR:17141.1,27954.0] || equal(u,filling) releasedAt(u,n1)* -> . % 16.75/16.99 27960[0:MRR:9508.0,27954.0] || -> releasedAt(waterLevel(u),n2)* happens(skf17(n1,v),n1)*. % 16.75/16.99 28487[1:SpL:57.1,27845.1] || equal(u,v)* holdsAt(waterLevel(u),n1)*+ releasedAt(waterLevel(v),n2)* -> . % 16.75/16.99 28557[2:Res:27861.0,27814.0] || -> equal(n3,n0)**. % 16.75/16.99 28558[2:MRR:28557.0,320.0] || -> . % 16.75/16.99 28559[2:Spt:28558.0,9502.0,27861.0] || holdsAt(waterLevel(n0),n1)* -> . % 16.75/16.99 28560[2:Spt:28558.0,9502.1] || -> releasedAt(waterLevel(n0),n1)*. % 16.75/16.99 28781[3:Spt:877.0,877.1,877.2] || holdsAt(u,n1) -> holdsAt(u,n0) releasedAt(u,n1)*. % 16.75/16.99 28788[3:Res:28781.2,27959.1] || holdsAt(u,n1)* equal(u,filling) -> holdsAt(u,n0). % 16.75/16.99 28792[3:MRR:28788.0,27956.1] || equal(u,filling) -> holdsAt(u,n0)*. % 16.75/16.99 28801[3:Res:28792.1,4.0] || equal(filling,filling)* -> . % 16.75/16.99 28838[3:Obv:28801.0] || -> . % 16.75/16.99 28843[3:Spt:28838.0,877.3] || -> happens(skf16(n0,u),n0)*. % 16.75/16.99 28850[3:Res:28843.0,63.0] || -> equal(skf16(n0,u),tapOn)** holdsAt(filling,n0). % 16.75/16.99 28855[3:MRR:28850.1,4.0] || -> equal(skf16(n0,u),tapOn)**. % 16.75/16.99 28874[4:Spt:27960.0] || -> releasedAt(waterLevel(u),n2)*. % 16.75/16.99 28876[4:MRR:28487.2,28874.0] || equal(u,v)* holdsAt(waterLevel(u),n1)* -> . % 16.75/16.99 28878[4:AED:8.0,28876.0] || holdsAt(waterLevel(u),n1)* -> . % 16.75/16.99 28879[4:UnC:28878.0,27739.0] || -> . % 16.75/16.99 28880[4:Spt:28879.0,27960.1] || -> happens(skf17(n1,u),n1)*. % 16.75/16.99 29350[1:Res:27752.2,65.0] || -> equal(n1,u) less_or_equal(u,n0)* less(n0,skf11(n0,v,w))*. % 16.75/16.99 29351[1:Res:27752.2,64.0] || -> equal(n1,u) less_or_equal(u,n0) less(skf11(n0,u,v),u)*. % 16.75/16.99 29467[0:Res:3.0,5454.0] || happens(u,n0) less(n0,n1) initiates(u,filling,n0)* -> holdsAt(waterLevel(n1),plus(n0,n1)) stoppedIn(n0,filling,plus(n0,n1))*. % 16.75/16.99 29487[0:Rew:13.0,29467.4,13.0,29467.3] || happens(u,n0) less(n0,n1) initiates(u,filling,n0)* -> holdsAt(waterLevel(n1),n1) stoppedIn(n0,filling,n1). % 16.75/16.99 30326[5:Spt:29350.0,29350.1] || -> equal(n1,u) less_or_equal(u,n0)*. % 16.75/16.99 30359[5:Res:30326.1,6114.0] || less_or_equal(n0,n3)* -> equal(n2,n1) equal(n2,n0) equal(n3,n0). % 16.75/16.99 30630[5:MRR:30359.0,30359.1,30359.2,30359.3,313.0,490.0,321.0,320.0] || -> . % 16.75/16.99 30773[5:Spt:30630.0,29350.2] || -> less(n0,skf11(n0,u,v))*. % 16.75/16.99 30831[5:Res:30773.0,49.0] || equal(skf11(n0,u,v),n0)** -> . % 16.75/16.99 30833[5:Res:30773.0,356.1] || less_or_equal(skf11(n0,u,v),n0)* -> . % 16.75/16.99 30865[5:Res:1887.0,30833.0] || -> less_or_equal(n1,skf11(n0,u,v))*. % 16.75/16.99 31411[1:Res:29351.2,30.0] || -> equal(n2,n1) less_or_equal(n2,n0) less_or_equal(skf11(n0,n2,u),n1)*. % 16.75/16.99 31444[1:MRR:31411.0,31411.1,490.0,489.0] || -> less_or_equal(skf11(n0,n2,u),n1)*. % 16.75/16.99 31552[1:Res:31444.0,5335.0] || -> equal(skf11(n0,n2,u),n1)** equal(skf11(n0,n2,u),n0). % 16.75/16.99 31563[5:MRR:31552.1,30831.0] || -> equal(skf11(n0,n2,u),n1)**. % 16.75/16.99 31606[5:SpR:31563.0,30773.0] || -> less(n0,n1)*. % 16.75/16.99 31643[5:MRR:29487.1,31606.0] || happens(u,n0) initiates(u,filling,n0)* -> holdsAt(waterLevel(n1),n1) stoppedIn(n0,filling,n1). % 16.75/16.99 32245[6:Spt:31643.3] || -> stoppedIn(n0,filling,n1)*. % 16.75/16.99 32249[6:Res:32245.0,64.0] || -> less(skf11(n0,n1,u),n1)*. % 16.75/16.99 32259[6:Res:32249.0,356.1] || less_or_equal(n1,skf11(n0,n1,u))* -> . % 16.75/16.99 32272[6:MRR:32259.0,30865.0] || -> . % 16.75/16.99 32275[6:Spt:32272.0,31643.3,32245.0] || stoppedIn(n0,filling,n1)* -> . % 16.75/16.99 32276[6:Spt:32272.0,31643.0,31643.1,31643.2] || happens(u,n0) initiates(u,filling,n0)* -> holdsAt(waterLevel(n1),n1). % 16.75/16.99 32279[6:Res:99.3,32276.1] || holdsAt(filling,plus(n0,n1)) happens(skf16(n0,filling),n0)* -> holdsAt(filling,n0) releasedAt(filling,plus(n0,n1)) holdsAt(waterLevel(n1),n1). % 16.75/16.99 32281[6:Rew:13.0,32279.3,28855.0,32279.1,13.0,32279.0] || holdsAt(filling,n1) happens(tapOn,n0) -> holdsAt(filling,n0) releasedAt(filling,n1) holdsAt(waterLevel(n1),n1)*. % 16.75/16.99 32282[6:MRR:32281.0,32281.1,32281.2,27735.0,27954.0,4.0] || -> releasedAt(filling,n1) holdsAt(waterLevel(n1),n1)*. % 16.75/16.99 32305[7:Spt:32282.1] || -> holdsAt(waterLevel(n1),n1)*. % 16.75/16.99 32347[7:Res:32305.0,27814.0] || -> equal(n3,n1)**. % 16.75/16.99 32348[7:MRR:32347.0,471.0] || -> . % 16.75/16.99 32368[7:Spt:32348.0,32282.1,32305.0] || holdsAt(waterLevel(n1),n1)* -> . % 16.75/16.99 32369[7:Spt:32348.0,32282.0] || -> releasedAt(filling,n1)*. % 16.75/16.99 32378[7:Res:32369.0,9953.0] || holdsAt(filling,u)* -> releasedAt(filling,n0) equal(waterLevel(skf20(filling,v)),filling)**. % 16.75/16.99 32387[7:MRR:32378.1,32378.2,6.0,23.0] || holdsAt(filling,u)* -> . % 16.75/16.99 32388[7:UnC:32387.0,27735.0] || -> . % 16.75/16.99 % SZS output end Refutation % 16.75/16.99 Formulae used in the proof : filling_2 less0 waterLevel_0 not_filling_0 not_released_filling_0 tapOff_not_tapOn overflow_not_tapOn filling_not_spilling plus0_1 plus1_1 plus1_2 plus1_3 not_released_waterLevel_0 filling_not_waterLevel symmetry_of_plus less_or_equal less1 less2 less3 less4 less5 less6 less7 less8 less9 less_property initiates_all_defn terminates_all_defn releases_all_defn distinct_waterLevels happens_all_defn stoppedin_defn change_of_waterLevel same_waterLevel keep_released keep_not_released happens_holds happens_releases happens_terminates_not_holds happens_not_released keep_holding keep_not_holding change_holding % 17.13/17.31 %------------------------------------------------------------------------------