%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : CSR020+1 : TPTP v8.1.0. Bugfixed v3.1.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n028.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:14 EDT 2022 % Result : Theorem 0.60s 0.78s % Output : Refutation 0.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : CSR020+1 : TPTP v8.1.0. Bugfixed v3.1.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.33 % Computer : n028.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Fri Jun 10 01:36:18 EDT 2022 % 0.13/0.34 % CPUTime : % 0.60/0.78 % 0.60/0.78 SPASS V 3.9 % 0.60/0.78 SPASS beiseite: Proof found. % 0.60/0.78 % SZS status Theorem % 0.60/0.78 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.60/0.78 SPASS derived 7634 clauses, backtracked 24 clauses, performed 15 splits and kept 796 clauses. % 0.60/0.78 SPASS allocated 88926 KBytes. % 0.60/0.78 SPASS spent 0:00:00.40 on the problem. % 0.60/0.78 0:00:00.04 for the input. % 0.60/0.78 0:00:00.09 for the FLOTTER CNF translation. % 0.60/0.78 0:00:00.06 for inferences. % 0.60/0.78 0:00:00.00 for the backtracking. % 0.60/0.78 0:00:00.19 for the reduction. % 0.60/0.78 % 0.60/0.78 % 0.60/0.78 Here is a proof with depth 8, length 103 : % 0.60/0.78 % SZS output start Refutation % 0.60/0.78 1[0:Inp] || -> holdsAt(spinning,n2)*. % 0.60/0.78 2[0:Inp] || less(u,n0)* -> . % 0.60/0.78 5[0:Inp] || holdsAt(spinning,n0)* -> . % 0.60/0.78 6[0:Inp] || releasedAt(u,v)* -> . % 0.60/0.78 7[0:Inp] || equal(pull,push)** -> . % 0.60/0.78 9[0:Inp] || equal(spinning,forwards)** -> . % 0.60/0.78 10[0:Inp] || equal(spinning,backwards)** -> . % 0.60/0.78 12[0:Inp] || -> equal(plus(n0,n1),n1)**. % 0.60/0.78 15[0:Inp] || -> equal(plus(n1,n1),n2)**. % 0.60/0.78 23[0:Inp] || less(u,v)* -> less_or_equal(u,v). % 0.60/0.78 24[0:Inp] || equal(u,v) -> less_or_equal(u,v)*. % 0.60/0.78 26[0:Inp] || less_or_equal(u,n0) -> less(u,n1)*. % 0.60/0.78 28[0:Inp] || less_or_equal(u,n1) -> less(u,n2)*. % 0.60/0.78 45[0:Inp] || SkP7(u,v)* -> equal(v,push). % 0.60/0.78 46[0:Inp] || SkP7(u,v)* -> equal(u,n0). % 0.60/0.78 47[0:Inp] || SkP8(u,v)* -> equal(v,pull). % 0.60/0.78 48[0:Inp] || SkP8(u,v)* -> equal(u,n1). % 0.60/0.78 49[0:Inp] || less(u,v)*+ less(v,u)* -> . % 0.60/0.78 50[0:Inp] || less(u,v)* equal(v,u) -> . % 0.60/0.78 51[0:Inp] || SkP0(u,v,w)* -> equal(w,push). % 0.60/0.78 52[0:Inp] || SkP0(u,v,w)* -> equal(v,forwards). % 0.60/0.78 53[0:Inp] || SkP1(u,v,w)* -> equal(w,pull). % 0.60/0.78 54[0:Inp] || SkP1(u,v,w)* -> equal(v,backwards). % 0.60/0.78 67[0:Inp] || -> less(u,v)* equal(v,u) less(v,u)*. % 0.60/0.78 89[0:Inp] || happens(u,v) -> SkP8(v,u)* SkP7(v,u) equal(v,n2). % 0.60/0.78 108[0:Inp] || initiates(u,v,w) -> equal(u,pull) SkP0(w,v,u) SkP1(w,v,u)*. % 0.60/0.78 110[0:Inp] || initiates(u,v,w) -> happens(push,w) SkP1(w,v,u)* SkP0(w,v,u). % 0.60/0.78 114[0:Inp] || happens(u,v) -> equal(u,push) equal(u,pull) SkP7(v,u) SkP8(v,u)*. % 0.60/0.78 116[0:Inp] || holdsAt(u,plus(v,n1)) -> happens(skf13(v,w),v)* holdsAt(u,v) releasedAt(u,plus(v,n1))*. % 0.60/0.78 117[0:Inp] || holdsAt(u,plus(v,n1)) -> initiates(skf13(v,u),u,v)* holdsAt(u,v) releasedAt(u,plus(v,n1)). % 0.60/0.78 127[0:MRR:114.3,114.4,45.0,47.0] || happens(u,v)* -> equal(u,pull) equal(u,push). % 0.60/0.78 128[0:MRR:108.3,53.0] || initiates(u,v,w) -> equal(u,pull) SkP0(w,v,u)*. % 0.60/0.78 129[0:MRR:116.3,6.0] || holdsAt(u,plus(v,n1))*+ -> holdsAt(u,v) happens(skf13(v,w),v)*. % 0.60/0.78 131[0:MRR:117.3,6.0] || holdsAt(u,plus(v,n1)) -> holdsAt(u,v) initiates(skf13(v,u),u,v)*. % 0.60/0.78 187[0:Res:28.1,50.0] || less_or_equal(u,n1)* equal(n2,u) -> . % 0.60/0.78 188[0:Res:26.1,50.0] || less_or_equal(u,n0)* equal(n1,u) -> . % 0.60/0.78 196[0:Res:28.1,49.0] || less_or_equal(u,n1) less(n2,u)* -> . % 0.60/0.78 345[0:Res:67.0,2.0] || -> equal(n0,u) less(n0,u)*. % 0.60/0.78 399[0:Res:345.1,23.0] || -> equal(n0,u) less_or_equal(n0,u)*. % 0.60/0.78 406[0:MRR:399.0,24.0] || -> less_or_equal(n0,u)*. % 0.60/0.78 414[0:Res:406.0,187.0] || equal(n2,n0)** -> . % 0.60/0.78 415[0:Res:406.0,188.0] || equal(n1,n0)** -> . % 0.60/0.78 441[0:Res:28.1,196.1] || less_or_equal(n2,n1)* less_or_equal(n2,n1)* -> . % 0.60/0.78 445[0:Obv:441.0] || less_or_equal(n2,n1)* -> . % 0.60/0.78 447[0:Res:24.1,445.0] || equal(n2,n1)** -> . % 0.60/0.78 682[0:Res:128.2,52.0] || initiates(u,v,w)* -> equal(u,pull) equal(v,forwards). % 0.60/0.78 691[0:Res:89.1,47.0] || happens(u,v) -> SkP7(v,u)* equal(v,n2) equal(u,pull). % 0.60/0.78 692[0:Res:89.1,48.0] || happens(u,v) -> SkP7(v,u)* equal(v,n2) equal(v,n1). % 0.60/0.78 709[0:SpL:15.0,129.0] || holdsAt(u,n2)*+ -> holdsAt(u,n1) happens(skf13(n1,v),n1)*. % 0.60/0.78 710[0:SpL:12.0,129.0] || holdsAt(u,n1)*+ -> holdsAt(u,n0) happens(skf13(n0,v),n0)*. % 0.60/0.78 1455[0:Res:110.2,54.0] || initiates(u,v,w) -> happens(push,w) SkP0(w,v,u)* equal(v,backwards). % 0.60/0.78 5663[1:Spt:709.0,709.1] || holdsAt(u,n2)* -> holdsAt(u,n1). % 0.60/0.78 5664[1:Res:1.0,5663.0] || -> holdsAt(spinning,n1)*. % 0.60/0.78 5868[2:Spt:710.0,710.1] || holdsAt(u,n1)* -> holdsAt(u,n0). % 0.60/0.78 5869[2:Res:5664.0,5868.0] || -> holdsAt(spinning,n0)*. % 0.60/0.78 5870[2:MRR:5869.0,5.0] || -> . % 0.60/0.78 5871[2:Spt:5870.0,710.2] || -> happens(skf13(n0,u),n0)*. % 0.60/0.78 5872[2:Res:5871.0,127.0] || -> equal(skf13(n0,u),pull)** equal(skf13(n0,u),push). % 0.60/0.78 5875[2:SpR:5872.0,5871.0] || -> equal(skf13(n0,u),push)** happens(pull,n0). % 0.60/0.78 5878[3:Spt:5875.0] || -> equal(skf13(n0,u),push)**. % 0.60/0.78 5880[3:SpR:5878.0,131.2] || holdsAt(u,plus(n0,n1))* -> holdsAt(u,n0) initiates(push,u,n0). % 0.60/0.78 5882[3:Rew:12.0,5880.0] || holdsAt(u,n1) -> holdsAt(u,n0) initiates(push,u,n0)*. % 0.60/0.78 6012[3:Res:5882.2,682.0] || holdsAt(u,n1)* -> holdsAt(u,n0) equal(pull,push) equal(u,forwards). % 0.60/0.78 6016[3:MRR:6012.2,7.0] || holdsAt(u,n1)* -> holdsAt(u,n0) equal(u,forwards). % 0.60/0.78 6019[3:Res:5664.0,6016.0] || -> holdsAt(spinning,n0)* equal(spinning,forwards). % 0.60/0.78 6020[3:MRR:6019.0,6019.1,5.0,9.0] || -> . % 0.60/0.78 6021[3:Spt:6020.0,5875.1] || -> happens(pull,n0)*. % 0.60/0.78 6722[0:Res:691.1,46.0] || happens(u,v)* -> equal(v,n2) equal(u,pull) equal(v,n0). % 0.60/0.78 7000[0:Res:692.1,45.0] || happens(u,v)* -> equal(v,n2) equal(v,n1) equal(u,push). % 0.60/0.78 7937[3:Res:6021.0,7000.0] || -> equal(n2,n0) equal(n1,n0) equal(pull,push)**. % 0.60/0.78 7939[3:MRR:7937.0,7937.1,7937.2,414.0,415.0,7.0] || -> . % 0.60/0.78 7942[1:Spt:7939.0,709.2] || -> happens(skf13(n1,u),n1)*. % 0.60/0.78 7944[1:Res:7942.0,6722.0] || -> equal(n2,n1) equal(skf13(n1,u),pull)** equal(n1,n0). % 0.60/0.78 7946[1:MRR:7944.0,7944.2,447.0,415.0] || -> equal(skf13(n1,u),pull)**. % 0.60/0.78 7951[2:Spt:710.0,710.1] || holdsAt(u,n1)* -> holdsAt(u,n0). % 0.60/0.78 7952[1:SpR:7946.0,131.2] || holdsAt(u,plus(n1,n1))* -> holdsAt(u,n1) initiates(pull,u,n1). % 0.60/0.78 7954[1:Rew:15.0,7952.0] || holdsAt(u,n2) -> holdsAt(u,n1) initiates(pull,u,n1)*. % 0.60/0.78 8143[0:Res:1455.2,51.0] || initiates(u,v,w)* -> happens(push,w) equal(v,backwards) equal(u,push). % 0.60/0.78 8344[1:Res:7954.2,8143.0] || holdsAt(u,n2)* -> holdsAt(u,n1) happens(push,n1)* equal(u,backwards) equal(pull,push). % 0.60/0.78 8345[1:MRR:8344.4,7.0] || holdsAt(u,n2)*+ -> holdsAt(u,n1) happens(push,n1)* equal(u,backwards). % 0.60/0.78 8346[3:Spt:8345.0,8345.1,8345.3] || holdsAt(u,n2)* -> holdsAt(u,n1) equal(u,backwards). % 0.60/0.78 8347[3:Res:1.0,8346.0] || -> holdsAt(spinning,n1)* equal(spinning,backwards). % 0.60/0.78 8348[3:MRR:8347.1,10.0] || -> holdsAt(spinning,n1)*. % 0.60/0.78 8350[3:Res:8348.0,7951.0] || -> holdsAt(spinning,n0)*. % 0.60/0.78 8351[3:MRR:8350.0,5.0] || -> . % 0.60/0.78 8353[3:Spt:8351.0,8345.2] || -> happens(push,n1)*. % 0.60/0.78 8356[3:Res:8353.0,6722.0] || -> equal(n2,n1) equal(pull,push)** equal(n1,n0). % 0.60/0.78 8358[3:MRR:8356.0,8356.1,8356.2,447.0,7.0,415.0] || -> . % 0.60/0.78 8359[2:Spt:8358.0,710.2] || -> happens(skf13(n0,u),n0)*. % 0.60/0.78 8361[2:Res:8359.0,7000.0] || -> equal(n2,n0) equal(n1,n0) equal(skf13(n0,u),push)**. % 0.60/0.78 8364[2:MRR:8361.0,8361.1,414.0,415.0] || -> equal(skf13(n0,u),push)**. % 0.60/0.78 8379[2:SpR:8364.0,131.2] || holdsAt(u,plus(n0,n1))* -> holdsAt(u,n0) initiates(push,u,n0). % 0.60/0.78 8381[2:Rew:12.0,8379.0] || holdsAt(u,n1) -> holdsAt(u,n0) initiates(push,u,n0)*. % 0.60/0.78 8384[2:Res:8381.2,682.0] || holdsAt(u,n1)* -> holdsAt(u,n0) equal(pull,push) equal(u,forwards). % 0.60/0.78 8388[2:MRR:8384.2,7.0] || holdsAt(u,n1)* -> holdsAt(u,n0) equal(u,forwards). % 0.60/0.78 8399[3:Spt:8345.0,8345.1,8345.3] || holdsAt(u,n2)* -> holdsAt(u,n1) equal(u,backwards). % 0.60/0.78 8400[3:Res:1.0,8399.0] || -> holdsAt(spinning,n1)* equal(spinning,backwards). % 0.60/0.78 8401[3:MRR:8400.1,10.0] || -> holdsAt(spinning,n1)*. % 0.60/0.78 8404[3:Res:8401.0,8388.0] || -> holdsAt(spinning,n0)* equal(spinning,forwards). % 0.60/0.78 8405[3:MRR:8404.0,8404.1,5.0,9.0] || -> . % 0.60/0.78 8410[3:Spt:8405.0,8345.2] || -> happens(push,n1)*. % 0.60/0.78 8414[3:Res:8410.0,6722.0] || -> equal(n2,n1) equal(pull,push)** equal(n1,n0). % 0.60/0.78 8416[3:MRR:8414.0,8414.1,8414.2,447.0,7.0,415.0] || -> . % 0.60/0.78 % SZS output end Refutation % 0.60/0.78 Formulae used in the proof : not_spinning_2 less0 not_splinning_0 not_releasedAt push_not_pull forwards_not_spinning spinning_not_backwards plus0_1 plus1_1 less_or_equal less1 less2 happens_all_defn less_property initiates_all_defn keep_not_holding % 0.60/0.78 %------------------------------------------------------------------------------