%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : CSR310_1 : TPTP v9.0.0. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n005.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Apr 1 01:53:46 AM UTC 2025 % Result : Theorem 5.20s 3.40s % Output : Refutation 5.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : CSR310_1 : TPTP v9.0.0. Released v9.1.0. % 0.06/0.13 % Command : spasst-tptp-script %s %d % 0.12/0.34 % Computer : n005.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Mon Mar 31 16:20:44 EDT 2025 % 0.12/0.34 % CPUTime : % 0.19/0.47 % Using integer theory % 5.20/3.40 % 5.20/3.40 % 5.20/3.40 % SZS status Theorem for /tmp/SPASST_17866_n005.cluster.edu % 5.20/3.40 % 5.20/3.40 SPASS V 2.2.22 in combination with yices. % 5.20/3.40 SPASS beiseite: Proof found by SPASS. % 5.20/3.40 Problem: /tmp/SPASST_17866_n005.cluster.edu % 5.20/3.40 SPASS derived 7062 clauses, backtracked 16 clauses and kept 2731 clauses. % 5.20/3.40 SPASS backtracked 4 times (0 times due to theory inconsistency). % 5.20/3.40 SPASS allocated 15235 KBytes. % 5.20/3.40 SPASS spent 0:00:02.23 on the problem. % 5.20/3.40 0:00:00.00 for the input. % 5.20/3.40 0:00:00.01 for the FLOTTER CNF translation. % 5.20/3.40 0:00:00.17 for inferences. % 5.20/3.40 0:00:00.01 for the backtracking. % 5.20/3.40 0:00:01.61 for the reduction. % 5.20/3.40 0:00:00.14 for interacting with the SMT procedure. % 5.20/3.40 % 5.20/3.40 % 5.20/3.40 % SZS output start CNFRefutation for /tmp/SPASST_17866_n005.cluster.edu % 5.20/3.40 % 5.20/3.40 % Here is a proof with depth 8, length 68 : % 5.20/3.40 1[0:Inp] || -> fluent(filling)*. % 5.20/3.40 3[0:Inp] || -> event(overflow)*. % 5.20/3.40 5[0:Inp] || -> event(tapOn)*. % 5.20/3.40 15[0:Inp] || -> event(skf18(U,V))*. % 5.20/3.40 18[0:Inp] || -> event(skf15(U,V))*. % 5.20/3.40 19[0:Inp] || -> holdsAt(filling,at_time(3))*. % 5.20/3.40 21[0:Inp] || releasedAt(filling,at_time(0))* -> . % 5.20/3.40 23[0:Inp] || holdsAt(filling,at_time(0))* -> . % 5.20/3.40 26[0:Inp] || equal(waterLevel(U),filling)** -> . % 5.20/3.40 29[0:Inp] || holdsAt(filling,at_time(4))* -> . % 5.20/3.40 33[0:Inp] || holdsAt(waterLevel(3),at_time(3))* -> . % 5.20/3.40 43[0:Inp] || event(U) happens(U,at_time(V))* -> equal(U,tapOn) equal(U,overflow). % 5.20/3.40 46[0:Inp] || event(U) happens(U,at_time(V))*+ -> equal(U,tapOn) holdsAt(filling,at_time(V))*. % 5.20/3.40 48[0:Inp] || event(U) fluent(V) releases(U,V,at_time(W))* -> equal(U,tapOn). % 5.20/3.40 51[0:Inp] || event(U) happens(U,at_time(V))*+ -> equal(V,0) holdsAt(waterLevel(3),at_time(V))*. % 5.20/3.40 56[0:Inp] || event(U) fluent(V) releases(U,V,at_time(W))* -> equal(waterLevel(skf21(V)),V). % 5.20/3.40 66[0:Inp] || fluent(U) releasedAt(U,at_time(V))* equal(V,plus(W,1))*+ -> releasedAt(U,at_time(W)) happens(skf18(U,W),at_time(W))*. % 5.20/3.40 70[0:Inp] || fluent(U) releasedAt(U,at_time(V))* equal(V,plus(W,1))*+ -> releasedAt(U,at_time(W)) releases(skf18(U,W),U,at_time(W))*. % 5.20/3.40 78[0:Inp] || fluent(U) holdsAt(U,at_time(V)) equal(W,plus(V,1))*+ equal(X,plus(V,1))* -> releasedAt(U,at_time(X))* holdsAt(U,at_time(W))* happens(skf15(U,V),at_time(V))*. % 5.20/3.40 98[0:ThA] || -> equal(plus(0,U),U)**. % 5.20/3.40 129[0:Res:19.0,78.3] || equal(U,plus(3,1)) equal(V,plus(3,1)) fluent(filling) -> holdsAt(filling,at_time(V))* happens(skf15(filling,3),at_time(3))* releasedAt(filling,at_time(U))*. % 5.20/3.40 142[0:Res:51.2,33.0] || event(U) happens(U,at_time(3))* -> equal(3,0). % 5.20/3.40 153[0:ArS:142.2] || event(U) happens(U,at_time(3))* -> . % 5.20/3.40 162[0:ArS:129.1] || equal(U,4) equal(V,4) fluent(filling) -> holdsAt(filling,at_time(V))* happens(skf15(filling,3),at_time(3))* releasedAt(filling,at_time(U))*. % 5.20/3.40 163[0:MRR:162.2,1.0] || equal(U,4) equal(V,4) -> holdsAt(filling,at_time(V))* happens(skf15(filling,3),at_time(3))* releasedAt(filling,at_time(U))*. % 5.20/3.40 186[0:Res:163.2,29.0] || equal(U,4) equal(4,4) -> happens(skf15(filling,3),at_time(3))* releasedAt(filling,at_time(U))*. % 5.20/3.40 188(e)[0:ArS:186.1] || equal(U,4) -> releasedAt(filling,at_time(U))* happens(skf15(filling,3),at_time(3))*. % 5.20/3.40 242[1:Spt:188.2] || -> happens(skf15(filling,3),at_time(3))*. % 5.20/3.40 243[1:Res:242.0,153.1] || event(skf15(filling,3))* -> . % 5.20/3.40 245(e)[1:MRR:243.0,18.0] || -> . % 5.20/3.40 247[1:Spt:245.0,188.2,242.0] || happens(skf15(filling,3),at_time(3))* -> . % 5.20/3.40 248[1:Spt:245.0,188.0,188.1] || equal(U,4) -> releasedAt(filling,at_time(U))*. % 5.20/3.40 777[0:EqR:66.2] || fluent(U) releasedAt(U,at_time(plus(V,1))) -> releasedAt(U,at_time(V)) happens(skf18(U,V),at_time(V))*. % 5.20/3.40 778[0:SpL:98.0,66.2] || fluent(U) releasedAt(U,at_time(V))*+ equal(V,1) -> releasedAt(U,at_time(0)) happens(skf18(U,0),at_time(0))*. % 5.20/3.40 1106[0:EqR:70.2] || fluent(U) releasedAt(U,at_time(plus(V,1))) -> releasedAt(U,at_time(V)) releases(skf18(U,V),U,at_time(V))*. % 5.20/3.40 1108[0:SpL:98.0,70.2] || fluent(U) releasedAt(U,at_time(V))*+ equal(V,1) -> releasedAt(U,at_time(0)) releases(skf18(U,0),U,at_time(0))*. % 5.20/3.40 3529[0:Res:777.3,43.1] || fluent(U) releasedAt(U,at_time(plus(V,1)))* event(skf18(U,V)) -> releasedAt(U,at_time(V)) equal(skf18(U,V),tapOn) equal(skf18(U,V),overflow). % 5.20/3.40 3539(e)[0:MRR:3529.2,15.0] || fluent(U) releasedAt(U,at_time(plus(V,1)))* -> releasedAt(U,at_time(V)) equal(skf18(U,V),tapOn) equal(skf18(U,V),overflow). % 5.20/3.40 3704[0:Res:1106.3,56.2] || fluent(U) releasedAt(U,at_time(plus(V,1)))* event(skf18(U,V)) fluent(U) -> releasedAt(U,at_time(V)) equal(waterLevel(skf21(U)),U). % 5.20/3.40 3705[0:Res:1106.3,48.2] || fluent(U) releasedAt(U,at_time(plus(V,1)))* event(skf18(U,V)) fluent(U) -> releasedAt(U,at_time(V)) equal(skf18(U,V),tapOn). % 5.20/3.40 3706[0:Obv:3705.0] || releasedAt(U,at_time(plus(V,1)))* event(skf18(U,V)) fluent(U) -> releasedAt(U,at_time(V)) equal(skf18(U,V),tapOn). % 5.20/3.40 3707[0:Rew:3539.4,3706.1] || releasedAt(U,at_time(plus(V,1)))* event(overflow) fluent(U) -> releasedAt(U,at_time(V)) equal(skf18(U,V),tapOn). % 5.20/3.40 3708[0:MRR:3707.1,3.0] || releasedAt(U,at_time(plus(V,1)))* fluent(U) -> releasedAt(U,at_time(V)) equal(skf18(U,V),tapOn). % 5.20/3.40 3716[0:Obv:3704.0] || releasedAt(U,at_time(plus(V,1)))* event(skf18(U,V)) fluent(U) -> releasedAt(U,at_time(V)) equal(waterLevel(skf21(U)),U). % 5.20/3.40 3717[0:Rew:3708.3,3716.1] || releasedAt(U,at_time(plus(V,1)))* event(tapOn) fluent(U) -> releasedAt(U,at_time(V)) equal(waterLevel(skf21(U)),U). % 5.20/3.40 3718[0:MRR:3717.1,5.0] || releasedAt(U,at_time(plus(V,1)))* fluent(U) -> releasedAt(U,at_time(V)) equal(waterLevel(skf21(U)),U). % 5.20/3.40 11856[1:Res:248.1,3718.0] || equal(plus(U,1),4) fluent(filling) -> releasedAt(filling,at_time(U))* equal(waterLevel(skf21(filling)),filling). % 5.20/3.40 11859[1:ArS:11856.0] || equal(U,3) fluent(filling) -> releasedAt(filling,at_time(U))* equal(waterLevel(skf21(filling)),filling). % 5.20/3.40 11860[1:MRR:11859.1,11859.3,1.0,26.0] || equal(U,3) -> releasedAt(filling,at_time(U))*. % 5.20/3.40 11878[1:Res:11860.1,3718.0] || equal(plus(U,1),3) fluent(filling) -> releasedAt(filling,at_time(U))* equal(waterLevel(skf21(filling)),filling). % 5.20/3.40 11898[1:ArS:11878.0] || equal(U,2) fluent(filling) -> releasedAt(filling,at_time(U))* equal(waterLevel(skf21(filling)),filling). % 5.20/3.40 11899[1:MRR:11898.1,11898.3,1.0,26.0] || equal(U,2) -> releasedAt(filling,at_time(U))*. % 5.20/3.40 11930[1:Res:11899.1,3718.0] || equal(plus(U,1),2) fluent(filling) -> releasedAt(filling,at_time(U))* equal(waterLevel(skf21(filling)),filling). % 5.20/3.40 11952[1:ArS:11930.0] || equal(U,1) fluent(filling) -> releasedAt(filling,at_time(U))* equal(waterLevel(skf21(filling)),filling). % 5.20/3.40 11953[1:MRR:11952.1,11952.3,1.0,26.0] || equal(U,1) -> releasedAt(filling,at_time(U))*. % 5.20/3.40 11980[1:Res:11953.1,1108.1] || equal(U,1)* fluent(filling) equal(U,1)* -> releasedAt(filling,at_time(0)) releases(skf18(filling,0),filling,at_time(0))*. % 5.20/3.40 11982[1:Res:11953.1,778.1] || equal(U,1)* fluent(filling) equal(U,1)* -> releasedAt(filling,at_time(0)) happens(skf18(filling,0),at_time(0))*. % 5.20/3.40 12006[1:Obv:11982.0] || fluent(filling) equal(U,1)* -> releasedAt(filling,at_time(0)) happens(skf18(filling,0),at_time(0))*. % 5.20/3.40 12007[1:AED:12006.1] || fluent(filling) -> releasedAt(filling,at_time(0)) happens(skf18(filling,0),at_time(0))*. % 5.20/3.40 12008[1:MRR:12007.0,12007.1,1.0,21.0] || -> happens(skf18(filling,0),at_time(0))*. % 5.20/3.40 12011[1:Obv:11980.0] || fluent(filling) equal(U,1)* -> releasedAt(filling,at_time(0)) releases(skf18(filling,0),filling,at_time(0))*. % 5.20/3.40 12012[1:AED:12011.1] || fluent(filling) -> releasedAt(filling,at_time(0)) releases(skf18(filling,0),filling,at_time(0))*. % 5.20/3.40 12013[1:MRR:12012.0,12012.1,1.0,21.0] || -> releases(skf18(filling,0),filling,at_time(0))*. % 5.20/3.40 12034[1:Res:12008.0,46.1] || event(skf18(filling,0)) -> equal(skf18(filling,0),tapOn) holdsAt(filling,at_time(0))*. % 5.20/3.40 12044[1:MRR:12034.0,12034.2,15.0,23.0] || -> equal(skf18(filling,0),tapOn)**. % 5.20/3.40 12046[1:Rew:12044.0,12013.0] || -> releases(tapOn,filling,at_time(0))*. % 5.20/3.40 12106[1:Res:12046.0,56.2] || event(tapOn) fluent(filling) -> equal(waterLevel(skf21(filling)),filling)**. % 5.20/3.40 12109(e)[1:MRR:12106.0,12106.1,12106.2,5.0,1.0,26.0] || -> . % 5.20/3.40 % 5.20/3.40 % SZS output end CNFRefutation for /tmp/SPASST_17866_n005.cluster.edu % 5.20/3.40 % 5.20/3.40 Formulae used in the proof : fof_spilling_decl fof_tapOff_decl fof_tapOn_tapOff fof_keep_not_holding fof_overflow_decl fof_keep_holding fof_not_released_spilling_0 fof_not_spilling_0 fof_spilling_not_waterLevel fof_stoppedin_defn fof_happens_all_defn fof_same_waterLevel fof_initiates_all_defn fof_keep_released fof_startedin_defn fof_happens_not_released % 5.40/3.51 % 5.40/3.52 SPASS+T ended %------------------------------------------------------------------------------