%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MED008+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n003.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 : Sun Jul 17 21:55:53 EDT 2022 % Result : Theorem 1.05s 1.22s % Output : Refutation 1.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : MED008+1 : TPTP v8.1.0. Released v3.2.0. % 0.10/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n003.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jul 5 01:56:40 EDT 2022 % 0.13/0.34 % CPUTime : % 1.05/1.22 % 1.05/1.22 SPASS V 3.9 % 1.05/1.22 SPASS beiseite: Proof found. % 1.05/1.22 % SZS status Theorem % 1.05/1.22 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.05/1.22 SPASS derived 2946 clauses, backtracked 478 clauses, performed 8 splits and kept 2293 clauses. % 1.05/1.22 SPASS allocated 100045 KBytes. % 1.05/1.22 SPASS spent 0:00:00.87 on the problem. % 1.05/1.22 0:00:00.04 for the input. % 1.05/1.22 0:00:00.06 for the FLOTTER CNF translation. % 1.05/1.22 0:00:00.03 for inferences. % 1.05/1.22 0:00:00.01 for the backtracking. % 1.05/1.22 0:00:00.70 for the reduction. % 1.05/1.22 % 1.05/1.22 % 1.05/1.22 Here is a proof with depth 6, length 162 : % 1.05/1.22 % SZS output start Refutation % 1.05/1.22 1[0:Inp] || -> s1(n0)*. % 1.05/1.22 2[0:Inp] || bcapacitysn(n0)* -> . % 1.05/1.22 3[0:Inp] || qilt27(n0)* -> . % 1.05/1.22 4[0:Inp] || gt(u,u)* -> . % 1.05/1.22 9[0:Inp] || -> conditionnormo(u)* gt(n0,u). % 1.05/1.22 13[0:Inp] || gt(u,skf26(u))*r -> . % 1.05/1.22 16[0:Inp] || gt(u,skf32(u))*r -> . % 1.05/1.22 22[0:Inp] || gt(u,skf36(u))*r -> . % 1.05/1.22 23[0:Inp] SkP8(u) || -> bcapacitysn(u)*. % 1.05/1.22 24[0:Inp] SkP8(u) || -> qilt27(u)*. % 1.05/1.22 25[0:Inp] SkP9(u) || -> bcapacitysn(u)*. % 1.05/1.22 26[0:Inp] SkP10(u) || -> bcapacityne(u)*. % 1.05/1.22 30[0:Inp] drugi(u) || -> s3(u)*. % 1.05/1.22 31[0:Inp] || gt(u,skf38(u))*r -> . % 1.05/1.22 32[0:Inp] || gt(u,skf37(u))*r -> . % 1.05/1.22 33[0:Inp] || gt(u,skf39(u))*r -> . % 1.05/1.22 39[0:Inp] || -> bcapacitysn(u) bcapacityex(u)* bcapacityne(u). % 1.05/1.22 40[0:Inp] bcapacityex(u) bcapacityne(u) || -> . % 1.05/1.22 42[0:Inp] bcapacitysn(u) bcapacityex(u) || -> . % 1.05/1.22 45[0:Inp] conditionnormo(u) conditionhyper(u) || -> . % 1.05/1.22 48[0:Inp] || bsecretioni(skf26(u))* -> SkP1(u). % 1.05/1.22 50[0:Inp] || bsecretioni(skf32(u))* -> SkP4(u). % 1.05/1.22 57[0:Inp] s3(u) s1(u) || -> . % 1.05/1.22 59[0:Inp] || conditionnormo(skf36(u))* -> SkP7(u). % 1.05/1.22 61[0:Inp] SkP11(u) bcapacityex(u) || -> . % 1.05/1.22 62[0:Inp] || bsecretioni(skf39(u))* -> SkP11(u). % 1.05/1.22 63[0:Inp] s1(u) || -> drugbg(u)* qilt27(u). % 1.05/1.22 64[0:Inp] || -> releaselg(u) uptakelg(u)* gt(v,u)*. % 1.05/1.22 68[0:Inp] SkP8(u) || -> bsecretioni(v)* gt(u,v)*. % 1.05/1.22 69[0:Inp] SkP10(u) || -> bsecretioni(v)* gt(u,v)*. % 1.05/1.22 71[0:Inp] SkP11(u) || -> drugsu(v)* gt(u,v)*. % 1.05/1.22 73[0:Inp] uptakelg(u) releaselg(u) || -> gt(v,u)*. % 1.05/1.22 74[0:Inp] SkP8(u) || gt(u,v)*+ -> conditionhyper(v)*. % 1.05/1.22 75[0:Inp] SkP9(u) releaselg(v) || -> gt(u,v)*. % 1.05/1.22 76[0:Inp] SkP9(u) || gt(u,v)* -> conditionhyper(v)*. % 1.05/1.22 77[0:Inp] SkP10(u) || gt(u,v)*+ -> conditionhyper(v)*. % 1.05/1.22 81[0:Inp] || uptakelg(skf37(u))*+ -> drugi(v)* gt(u,v)*. % 1.05/1.22 82[0:Inp] || uptakepg(skf38(u))*+ -> drugi(v)* gt(u,v)*. % 1.05/1.22 85[0:Inp] || gt(u,v)* gt(v,w)* -> gt(u,w)*. % 1.05/1.22 87[0:Inp] SkP7(u) || -> SkP10(u)* SkP9(u) SkP8(u) bcapacityex(u). % 1.05/1.22 92[0:Inp] SkP7(u) || -> SkP10(u)* SkP9(u) SkP8(u) uptakelg(v)* gt(u,v)*. % 1.05/1.22 93[0:Inp] SkP7(u) || -> SkP10(u)* SkP9(u) SkP8(u) uptakepg(v)* gt(u,v)*. % 1.05/1.22 94[0:Inp] SkP10(u) releaselg(v) || -> uptakepg(w)* gt(u,w)* gt(u,v)*. % 1.05/1.22 96[0:Inp] SkP7(u) || gt(u,v)* -> conditionhyper(v)* SkP8(u) SkP9(u) SkP10(u)*. % 1.05/1.22 104[0:MRR:96.3,96.4,96.5,74.0,76.0,77.0] SkP7(u) || gt(u,v)*+ -> conditionhyper(v)*. % 1.05/1.22 109[0:Res:1.0,63.0] || -> qilt27(n0) drugbg(n0)*. % 1.05/1.22 112[0:Res:1.0,57.0] s3(n0) || -> . % 1.05/1.22 115[0:Res:24.1,3.0] SkP8(n0) || -> . % 1.05/1.22 116[0:Res:39.2,2.0] || -> bcapacityex(n0)* bcapacityne(n0). % 1.05/1.22 118[0:Res:25.1,2.0] SkP9(n0) || -> . % 1.05/1.22 119[0:Res:9.0,4.0] || -> conditionnormo(n0)*. % 1.05/1.22 124[0:Res:9.0,33.0] || -> conditionnormo(skf39(n0))*. % 1.05/1.22 125[0:Res:9.0,32.0] || -> conditionnormo(skf37(n0))*. % 1.05/1.22 126[0:Res:9.0,31.0] || -> conditionnormo(skf38(n0))*. % 1.05/1.22 127[0:Res:9.0,22.0] || -> conditionnormo(skf36(n0))*. % 1.05/1.22 132[0:Res:9.0,16.0] || -> conditionnormo(skf32(n0))*. % 1.05/1.22 134[0:Res:9.0,13.0] || -> conditionnormo(skf26(n0))*. % 1.05/1.22 142[0:MRR:109.0,3.0] || -> drugbg(n0)*. % 1.05/1.22 277[0:SoR:112.0,30.1] drugi(n0) || -> . % 1.05/1.22 286[0:Res:127.0,59.0] || -> SkP7(n0)*. % 1.05/1.22 329[0:Res:9.0,59.0] || -> gt(n0,skf36(u))*r SkP7(u). % 1.05/1.22 365[0:NCh:85.2,85.1,329.0,4.0] || gt(skf36(u),n0)*l -> SkP7(u). % 1.05/1.22 366[0:NCh:85.2,85.1,329.0,22.0] || gt(u,n0) -> SkP7(u)*. % 1.05/1.22 376[0:Res:64.2,365.0] || -> releaselg(n0) uptakelg(n0) SkP7(u)*. % 1.05/1.22 381[0:NCh:85.2,85.1,64.2,4.0] || gt(u,v)*+ -> releaselg(u) uptakelg(u)*. % 1.05/1.22 387[0:NCh:85.2,85.1,64.2,32.0] || gt(u,v)* -> releaselg(skf37(u)) uptakelg(skf37(u))*. % 1.05/1.22 406[1:Spt:376.2] || -> SkP7(u)*. % 1.05/1.22 408[1:MRR:104.0,406.0] || gt(u,v)*+ -> conditionhyper(v)*. % 1.05/1.22 410[1:MRR:92.0,406.0] || -> SkP10(u)* SkP9(u) SkP8(u) uptakelg(v)* gt(u,v)*. % 1.05/1.22 421[1:EmS:45.0,45.1,125.0,408.1] || gt(u,skf37(n0))* -> . % 1.05/1.22 434[1:EmS:45.0,45.1,119.0,408.1] || gt(u,n0)* -> . % 1.05/1.22 435[1:Res:64.2,408.0] || -> releaselg(u) uptakelg(u) conditionhyper(u)*. % 1.05/1.22 452[1:EmS:45.0,45.1,125.0,435.2] || -> uptakelg(skf37(n0))* releaselg(skf37(n0)). % 1.05/1.22 532[1:Res:69.2,408.0] SkP10(u) || -> bsecretioni(v) conditionhyper(v)*. % 1.05/1.22 565[1:Res:68.2,408.0] SkP8(u) || -> bsecretioni(v) conditionhyper(v)*. % 1.05/1.22 669[0:Res:73.2,4.0] uptakelg(u) releaselg(u) || -> . % 1.05/1.22 775[0:Res:75.2,32.0] SkP9(u) releaselg(skf37(u)) || -> . % 1.05/1.22 827[0:SoR:277.0,82.1] || uptakepg(skf38(u))* -> gt(u,n0). % 1.05/1.22 830[1:MRR:827.1,434.0] || uptakepg(skf38(u))* -> . % 1.05/1.22 832[0:SoR:277.0,81.1] || uptakelg(skf37(u))* -> gt(u,n0). % 1.05/1.22 837[1:MRR:832.1,434.0] || uptakelg(skf37(u))* -> . % 1.05/1.22 838[1:MRR:452.0,837.0] || -> releaselg(skf37(n0))*. % 1.05/1.22 839[1:MRR:387.2,837.0] || gt(u,v)*+ -> releaselg(skf37(u))*. % 1.05/1.22 1125[1:EmS:669.0,669.1,410.3,838.0] || -> SkP10(u)* SkP9(u) SkP8(u) gt(u,skf37(n0))*. % 1.05/1.22 1178[1:MRR:1125.3,421.0] || -> SkP10(u)* SkP9(u) SkP8(u). % 1.05/1.22 1181[1:EmS:532.0,1178.0] || -> bsecretioni(u) conditionhyper(u)* SkP8(v) SkP9(v)*. % 1.05/1.22 1182[1:MRR:1181.2,565.0] || -> bsecretioni(u) conditionhyper(u)* SkP9(v)*. % 1.05/1.22 1183[2:Spt:1182.2] || -> SkP9(u)*. % 1.05/1.22 1184[2:UnC:1183.0,118.0] || -> . % 1.05/1.22 1185[2:Spt:1184.0,1182.0,1182.1] || -> bsecretioni(u) conditionhyper(u)*. % 1.05/1.22 1540[0:Res:94.4,32.0] SkP10(u) releaselg(skf37(u)) || -> uptakepg(v)* gt(u,v)*. % 1.05/1.22 1833[1:Res:75.2,839.0] SkP9(u) releaselg(v) || -> releaselg(skf37(u))*. % 1.05/1.22 1872[1:MRR:1833.2,775.1] SkP9(u) releaselg(v) || -> . % 1.05/1.22 1949[0:Res:64.2,381.0] || -> releaselg(u) uptakelg(u)* releaselg(v) uptakelg(v)*. % 1.05/1.22 1980[0:Con:1949.2] || -> releaselg(u) uptakelg(u)*. % 1.05/1.22 1990[1:Res:1980.1,837.0] || -> releaselg(skf37(u))*. % 1.05/1.22 1991[1:MRR:1540.1,1990.0] SkP10(u) || -> uptakepg(v)* gt(u,v)*. % 1.05/1.22 1994[1:EmS:1872.1,1990.0] SkP9(u) || -> . % 1.05/1.22 1995[1:MRR:1178.1,1994.0] || -> SkP10(u)* SkP8(u). % 1.05/1.22 2001[1:Res:1991.2,408.0] SkP10(u) || -> uptakepg(v) conditionhyper(v)*. % 1.05/1.22 2051[1:EmS:2001.0,1995.0] || -> uptakepg(u) conditionhyper(u)* SkP8(v)*. % 1.05/1.22 2052[3:Spt:2051.0,2051.1] || -> uptakepg(u) conditionhyper(u)*. % 1.05/1.22 2072[3:EmS:45.0,45.1,126.0,2052.1] || -> uptakepg(skf38(n0))*. % 1.05/1.22 2089[3:MRR:2072.0,830.0] || -> . % 1.05/1.22 2090[3:Spt:2089.0,2051.2] || -> SkP8(u)*. % 1.05/1.22 2091[3:UnC:2090.0,115.0] || -> . % 1.05/1.22 2092[1:Spt:2091.0,376.0,376.1] || -> releaselg(n0) uptakelg(n0)*. % 1.05/1.22 2287[0:EmS:45.0,45.1,125.0,104.2] SkP7(u) || gt(u,skf37(n0))* -> . % 1.05/1.22 2288[0:EmS:45.0,45.1,126.0,104.2] SkP7(u) || gt(u,skf38(n0))* -> . % 1.05/1.22 2300[0:EmS:45.0,45.1,119.0,104.2] SkP7(u) || gt(u,n0)* -> . % 1.05/1.22 2309[0:Res:68.2,104.1] SkP8(u) SkP7(u) || -> bsecretioni(v) conditionhyper(v)*. % 1.05/1.22 2334[0:MRR:2300.0,366.1] || gt(u,n0)* -> . % 1.05/1.22 2335[0:MRR:827.1,2334.0] || uptakepg(skf38(u))* -> . % 1.05/1.22 2336[0:MRR:832.1,2334.0] || uptakelg(skf37(u))* -> . % 1.05/1.22 2341[0:Res:1980.1,2336.0] || -> releaselg(skf37(u))*. % 1.05/1.22 2343[0:MRR:775.1,2341.0] SkP9(u) || -> . % 1.05/1.22 2344[0:MRR:1540.1,2341.0] SkP10(u) || -> uptakepg(v)* gt(u,v)*. % 1.05/1.22 2347[0:MRR:87.2,2343.0] SkP7(u) || -> SkP10(u)* SkP8(u) bcapacityex(u). % 1.05/1.22 2348[0:MRR:92.2,2343.0] SkP7(u) || -> SkP10(u)* SkP8(u) uptakelg(v)* gt(u,v)*. % 1.05/1.22 2349[0:MRR:93.2,2343.0] SkP7(u) || -> SkP10(u)* SkP8(u) uptakepg(v)* gt(u,v)*. % 1.05/1.22 2350[0:MRR:2349.1,2344.0] SkP7(u) || -> SkP8(u)* uptakepg(v)* gt(u,v)*. % 1.05/1.22 2355[0:Res:71.2,2334.0] SkP11(u) || -> drugsu(n0)*. % 1.05/1.22 2356[0:Res:68.2,2334.0] SkP8(u) || -> bsecretioni(n0)*. % 1.05/1.22 2357[0:Res:69.2,2334.0] SkP10(u) || -> bsecretioni(n0)*. % 1.05/1.22 2412[0:Res:69.2,77.1] SkP10(u) SkP10(u) || -> bsecretioni(v) conditionhyper(v)*. % 1.05/1.22 2436[0:Obv:2412.0] SkP10(u) || -> bsecretioni(v) conditionhyper(v)*. % 1.05/1.22 2438[0:EmS:2357.0,2347.1] SkP7(u) || -> bsecretioni(n0) bcapacityex(u) SkP8(u)*. % 1.05/1.22 2439[0:MRR:2438.3,2356.0] SkP7(u) || -> bsecretioni(n0)* bcapacityex(u)*. % 1.05/1.22 2440[2:Spt:2439.0,2439.2] SkP7(u) || -> bcapacityex(u)*. % 1.05/1.22 2441[2:EmS:42.0,42.1,23.1,2440.1] SkP8(u) SkP7(u) || -> . % 1.05/1.22 2444[2:MRR:2350.1,2441.0] SkP7(u) || -> uptakepg(v)* gt(u,v)*. % 1.05/1.22 2448[2:Res:2444.1,2335.0] SkP7(u) || -> gt(u,skf38(v))*. % 1.05/1.22 2502[2:MRR:2288.1,2448.1] SkP7(u) || -> . % 1.05/1.22 2503[2:UnC:2502.0,286.0] || -> . % 1.05/1.22 2506[2:Spt:2503.0,2439.1] || -> bsecretioni(n0)*. % 1.05/1.22 2507[0:EmS:2436.0,2347.1] SkP7(u) || -> bsecretioni(v) conditionhyper(v)* bcapacityex(u) SkP8(u)*. % 1.05/1.22 2508[0:MRR:2507.4,2309.0] SkP7(u) || -> bsecretioni(v) conditionhyper(v)* bcapacityex(u)*. % 1.06/1.23 2509[3:Spt:2508.1,2508.2] || -> bsecretioni(u) conditionhyper(u)*. % 1.06/1.23 2524[3:EmS:45.0,45.1,124.0,2509.1] || -> bsecretioni(skf39(n0))*. % 1.06/1.23 2532[3:EmS:45.0,45.1,132.0,2509.1] || -> bsecretioni(skf32(n0))*. % 1.06/1.23 2534[3:EmS:45.0,45.1,134.0,2509.1] || -> bsecretioni(skf26(n0))*. % 1.06/1.23 2607[3:Res:2524.0,62.0] || -> SkP11(n0)*. % 1.06/1.23 2615[0:Res:2350.3,104.1] SkP7(u) SkP7(u) || -> SkP8(u)* uptakepg(v) conditionhyper(v)*. % 1.06/1.23 2667[0:Obv:2615.0] SkP7(u) || -> SkP8(u)* uptakepg(v) conditionhyper(v)*. % 1.06/1.23 2674[3:EmS:2355.0,2607.0] || -> drugsu(n0)*. % 1.06/1.23 2675[3:EmS:61.0,61.1,2607.0,116.0] || -> bcapacityne(n0)*. % 1.06/1.23 2680[0:EmS:669.0,669.1,2348.3,2341.0] SkP7(u) || -> SkP10(u)* SkP8(u) gt(u,skf37(v))*. % 1.06/1.23 2827[3:Res:2532.0,50.0] || -> SkP4(n0)*. % 1.06/1.23 2910[3:Res:2534.0,48.0] || -> SkP1(n0)*. % 1.06/1.23 3202[4:Spt:2667.2,2667.3] || -> uptakepg(u) conditionhyper(u)*. % 1.06/1.23 3223[4:EmS:45.0,45.1,126.0,3202.1] || -> uptakepg(skf38(n0))*. % 1.06/1.23 3240[4:MRR:3223.0,2335.0] || -> . % 1.06/1.23 3241[4:Spt:3240.0,2667.0,2667.1] SkP7(u) || -> SkP8(u)*. % 1.06/1.23 3242[4:SoR:115.0,3241.1] SkP7(n0) || -> . % 1.06/1.23 3243[4:SSi:3242.0,1.0,142.0,119.0,286.0,2506.0,2607.0,2674.0,2675.0,2827.0,2910.0] || -> . % 1.06/1.23 3244[3:Spt:3243.0,2508.0,2508.3] SkP7(u) || -> bcapacityex(u)*. % 1.06/1.23 3245[3:EmS:42.0,42.1,23.1,3244.1] SkP8(u) SkP7(u) || -> . % 1.06/1.23 3246[3:EmS:40.0,40.1,3244.1,26.1] SkP7(u) SkP10(u) || -> . % 1.06/1.23 3254[3:MRR:2680.2,3245.0] SkP7(u) || -> SkP10(u)* gt(u,skf37(v))*. % 1.06/1.23 3307[3:MRR:3254.1,3246.1] SkP7(u) || -> gt(u,skf37(v))*. % 1.06/1.23 3308[3:MRR:2287.1,3307.1] SkP7(u) || -> . % 1.06/1.23 3309[3:UnC:3308.0,286.0] || -> . % 1.06/1.23 % SZS output end Refutation % 1.06/1.23 Formulae used in the proof : unsuccessfuls1_qige27 irreflexivity_gt sn_cure_1 xorcondition3 ne_cure normo insulincomp insulin_completion su_completion xorcapacity1 xorcapacity2 xorcapacity4 xorstep6 step2 uptake_completion liver_glucose transitivity_gt % 1.06/1.23 %------------------------------------------------------------------------------