%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT025+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:19:49 AM UTC 2026 % Result : Theorem 0.41s 0.68s % Output : Refutation 0.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : MGT025+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.06 % Command : run_spass %d %s % 0.17/0.42 % Computer : n016.cluster.edu % 0.17/0.42 % Model : x86_64 x86_64 % 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.42 % Memory : 8046.5625MB % 0.17/0.42 % OS : Linux 6.8.0-71-generic % 0.17/0.42 % CPULimit : 300 % 0.17/0.42 % WCLimit : 300 % 0.17/0.42 % DateTime : Mon Sep 7 12:14:17 UTC 2026 % 0.17/0.43 % CPUTime : % 0.41/0.68 % 0.41/0.68 SPASS V 3.9 % 0.41/0.68 SPASS beiseite: Proof found. % 0.41/0.68 % SZS status Theorem % 0.41/0.68 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.41/0.68 SPASS derived 177 clauses, backtracked 79 clauses, performed 7 splits and kept 171 clauses. % 0.41/0.68 SPASS allocated 97840 KBytes. % 0.41/0.68 SPASS spent 0:00:00.25 on the problem. % 0.41/0.68 0:00:00.08 for the input. % 0.41/0.68 0:00:00.07 for the FLOTTER CNF translation. % 0.41/0.68 0:00:00.01 for inferences. % 0.41/0.68 0:00:00.00 for the backtracking. % 0.41/0.68 0:00:00.03 for the reduction. % 0.41/0.68 % 0.41/0.68 % 0.41/0.68 Here is a proof with depth 11, length 125 : % 0.41/0.68 % SZS output start Refutation % 0.41/0.68 1[0:Inp] || -> environment(skc3)*. % 0.41/0.68 2[0:Inp] || -> constant(number_of_organizations(skc3,skc2))*. % 0.41/0.68 3[0:Inp] || -> subpopulations(first_movers,efficient_producers,skc3,skc2)*. % 0.41/0.68 4[0:Inp] || SkP0(u,v)* -> constant(v). % 0.41/0.68 5[0:Inp] || SkP0(u,v)* -> constant(u). % 0.41/0.68 6[0:Inp] || SkP1(u,v)* -> increases(v). % 0.41/0.68 7[0:Inp] || SkP1(u,v)* -> decreases(u). % 0.41/0.68 8[0:Inp] environment(u) || in_environment(u,v) -> subpopulation(first_movers,u,v)*. % 0.41/0.68 9[0:Inp] environment(u) || in_environment(u,v) -> subpopulation(efficient_producers,u,v)*. % 0.41/0.68 10[0:Inp] || greater(zero,growth_rate(first_movers,skc2)) greater(growth_rate(efficient_producers,skc2),zero)* -> . % 0.41/0.68 11[0:Inp] || greater(zero,growth_rate(efficient_producers,skc2)) greater(growth_rate(first_movers,skc2),zero)* -> . % 0.41/0.68 12[0:Inp] || equal(growth_rate(efficient_producers,skc2),zero) equal(growth_rate(first_movers,skc2),zero)** -> . % 0.41/0.68 13[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v)* -> in_environment(u,v). % 0.41/0.68 14[0:Inp] || constant(sum__dfg(u,v))* -> decreases(u) SkP1(v,u) SkP0(v,u). % 0.41/0.68 15[0:Inp] || constant(sum__dfg(u,v))* -> increases(v) SkP1(v,u) SkP0(v,u). % 0.41/0.68 16[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v)*+ -> greater(cardinality_at_time(first_movers,v),zero)*. % 0.41/0.68 17[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v)*+ -> greater(cardinality_at_time(efficient_producers,v),zero)*. % 0.41/0.68 20[0:Inp] environment(u) || equal(v,efficient_producers) subpopulation(v,u,w)*+ -> equal(number_of_organizations(u,w),sum__dfg(cardinality_at_time(first_movers,w),cardinality_at_time(efficient_producers,w)))*. % 0.41/0.68 22[0:Inp] environment(u) || decreases(cardinality_at_time(v,w)) in_environment(u,w) greater(cardinality_at_time(v,w),zero)*+ subpopulation(v,u,w)* -> greater(zero,growth_rate(v,w)). % 0.41/0.68 23[0:Inp] environment(u) || increases(cardinality_at_time(v,w)) in_environment(u,w) greater(cardinality_at_time(v,w),zero)+ subpopulation(v,u,w)* -> greater(growth_rate(v,w),zero)*. % 0.41/0.68 24[0:Inp] environment(u) || constant(cardinality_at_time(v,w)) in_environment(u,w) greater(cardinality_at_time(v,w),zero)*+ subpopulation(v,u,w)* -> equal(growth_rate(v,w),zero). % 0.41/0.68 29[0:Res:1.0,20.0] || equal(u,efficient_producers) subpopulation(u,skc3,v)*+ -> equal(sum__dfg(cardinality_at_time(first_movers,v),cardinality_at_time(efficient_producers,v)),number_of_organizations(skc3,v))**. % 0.41/0.68 36[0:Res:1.0,9.0] || in_environment(skc3,u) -> subpopulation(efficient_producers,skc3,u)*. % 0.41/0.68 37[0:Res:3.0,16.1] environment(skc3) || -> greater(cardinality_at_time(first_movers,skc2),zero)*. % 0.41/0.68 38[0:Res:3.0,17.1] environment(skc3) || -> greater(cardinality_at_time(efficient_producers,skc2),zero)*. % 0.41/0.68 39[0:Res:3.0,13.1] environment(skc3) || -> in_environment(skc3,skc2)*. % 0.41/0.68 40[0:MRR:39.0,1.0] || -> in_environment(skc3,skc2)*. % 0.41/0.68 41[0:MRR:37.0,1.0] || -> greater(cardinality_at_time(first_movers,skc2),zero)*. % 0.41/0.68 42[0:MRR:38.0,1.0] || -> greater(cardinality_at_time(efficient_producers,skc2),zero)*. % 0.41/0.68 54[0:Res:36.1,29.1] || in_environment(skc3,u) equal(efficient_producers,efficient_producers) -> equal(sum__dfg(cardinality_at_time(first_movers,u),cardinality_at_time(efficient_producers,u)),number_of_organizations(skc3,u))**. % 0.41/0.68 58[0:Obv:54.1] || in_environment(skc3,u) -> equal(sum__dfg(cardinality_at_time(first_movers,u),cardinality_at_time(efficient_producers,u)),number_of_organizations(skc3,u))**. % 0.41/0.68 79[0:Res:9.2,20.2] environment(u) environment(u) || in_environment(u,v) equal(efficient_producers,efficient_producers) -> equal(number_of_organizations(u,v),sum__dfg(cardinality_at_time(first_movers,v),cardinality_at_time(efficient_producers,v)))*. % 0.41/0.68 83[0:Obv:79.3] environment(u) || in_environment(u,v) -> equal(number_of_organizations(u,v),sum__dfg(cardinality_at_time(first_movers,v),cardinality_at_time(efficient_producers,v)))*. % 0.41/0.68 86[0:SpR:83.2,58.1] environment(u) || in_environment(u,v) in_environment(skc3,v) -> equal(number_of_organizations(u,v),number_of_organizations(skc3,v))*. % 0.41/0.68 93[0:SpR:86.3,2.0] environment(u) || in_environment(u,skc2) in_environment(skc3,skc2) -> constant(number_of_organizations(u,skc2))*. % 0.41/0.68 97[0:MRR:93.2,40.0] environment(u) || in_environment(u,skc2) -> constant(number_of_organizations(u,skc2))*. % 0.41/0.68 111[0:SpR:83.2,97.2] environment(u) environment(u) || in_environment(u,skc2)* in_environment(u,skc2)* -> constant(sum__dfg(cardinality_at_time(first_movers,skc2),cardinality_at_time(efficient_producers,skc2)))*. % 0.41/0.68 112[0:Obv:111.2] environment(u) || in_environment(u,skc2)*+ -> constant(sum__dfg(cardinality_at_time(first_movers,skc2),cardinality_at_time(efficient_producers,skc2)))*. % 0.41/0.68 115[0:Res:40.0,112.1] environment(skc3) || -> constant(sum__dfg(cardinality_at_time(first_movers,skc2),cardinality_at_time(efficient_producers,skc2)))*. % 0.41/0.68 116[0:SSi:115.0,1.0] || -> constant(sum__dfg(cardinality_at_time(first_movers,skc2),cardinality_at_time(efficient_producers,skc2)))*. % 0.41/0.68 119[0:Res:116.0,14.0] || -> decreases(cardinality_at_time(first_movers,skc2)) SkP1(cardinality_at_time(efficient_producers,skc2),cardinality_at_time(first_movers,skc2))* SkP0(cardinality_at_time(efficient_producers,skc2),cardinality_at_time(first_movers,skc2)). % 0.41/0.68 120[0:Res:116.0,15.0] || -> increases(cardinality_at_time(efficient_producers,skc2)) SkP1(cardinality_at_time(efficient_producers,skc2),cardinality_at_time(first_movers,skc2))* SkP0(cardinality_at_time(efficient_producers,skc2),cardinality_at_time(first_movers,skc2)). % 0.41/0.68 121[0:Res:119.1,6.0] || -> decreases(cardinality_at_time(first_movers,skc2)) SkP0(cardinality_at_time(efficient_producers,skc2),cardinality_at_time(first_movers,skc2))* increases(cardinality_at_time(first_movers,skc2)). % 0.41/0.68 122[0:Res:119.1,7.0] || -> decreases(cardinality_at_time(first_movers,skc2)) SkP0(cardinality_at_time(efficient_producers,skc2),cardinality_at_time(first_movers,skc2))* decreases(cardinality_at_time(efficient_producers,skc2)). % 0.41/0.68 129[1:Spt:121.0] || -> decreases(cardinality_at_time(first_movers,skc2))*. % 0.41/0.68 130[0:Res:120.1,6.0] || -> increases(cardinality_at_time(efficient_producers,skc2)) SkP0(cardinality_at_time(efficient_producers,skc2),cardinality_at_time(first_movers,skc2))* increases(cardinality_at_time(first_movers,skc2)). % 0.41/0.68 131[0:Res:120.1,7.0] || -> increases(cardinality_at_time(efficient_producers,skc2)) SkP0(cardinality_at_time(efficient_producers,skc2),cardinality_at_time(first_movers,skc2))* decreases(cardinality_at_time(efficient_producers,skc2)). % 0.41/0.68 132[2:Spt:130.0] || -> increases(cardinality_at_time(efficient_producers,skc2))*. % 0.41/0.68 169[0:Res:42.0,23.3] environment(u) || increases(cardinality_at_time(efficient_producers,skc2)) in_environment(u,skc2) subpopulation(efficient_producers,u,skc2)* -> greater(growth_rate(efficient_producers,skc2),zero)*. % 0.41/0.68 170[0:Res:41.0,23.3] environment(u) || increases(cardinality_at_time(first_movers,skc2)) in_environment(u,skc2) subpopulation(first_movers,u,skc2)* -> greater(growth_rate(first_movers,skc2),zero)*. % 0.41/0.68 173[0:MRR:170.3,8.2] environment(u) || increases(cardinality_at_time(first_movers,skc2))+ in_environment(u,skc2)* -> greater(growth_rate(first_movers,skc2),zero)*. % 0.41/0.68 174[2:MRR:169.1,169.3,132.0,9.2] environment(u) || in_environment(u,skc2)*+ -> greater(growth_rate(efficient_producers,skc2),zero)*. % 0.41/0.68 177[2:Res:40.0,174.1] environment(skc3) || -> greater(growth_rate(efficient_producers,skc2),zero)*. % 0.41/0.68 178[2:SSi:177.0,1.0] || -> greater(growth_rate(efficient_producers,skc2),zero)*. % 0.41/0.68 179[2:MRR:10.1,178.0] || greater(zero,growth_rate(first_movers,skc2))* -> . % 0.41/0.68 180[0:Res:42.0,24.3] environment(u) || constant(cardinality_at_time(efficient_producers,skc2)) in_environment(u,skc2) subpopulation(efficient_producers,u,skc2)* -> equal(growth_rate(efficient_producers,skc2),zero). % 0.41/0.68 181[0:Res:41.0,24.3] environment(u) || constant(cardinality_at_time(first_movers,skc2)) in_environment(u,skc2) subpopulation(first_movers,u,skc2)* -> equal(growth_rate(first_movers,skc2),zero). % 0.45/0.70 184[0:MRR:181.3,8.2] environment(u) || constant(cardinality_at_time(first_movers,skc2))*+ in_environment(u,skc2)* -> equal(growth_rate(first_movers,skc2),zero). % 0.45/0.70 185[0:MRR:180.3,9.2] environment(u) || constant(cardinality_at_time(efficient_producers,skc2))*+ in_environment(u,skc2)* -> equal(growth_rate(efficient_producers,skc2),zero). % 0.45/0.70 190[0:Res:42.0,22.3] environment(u) || decreases(cardinality_at_time(efficient_producers,skc2)) in_environment(u,skc2) subpopulation(efficient_producers,u,skc2)* -> greater(zero,growth_rate(efficient_producers,skc2))*. % 0.45/0.70 191[0:Res:41.0,22.3] environment(u) || decreases(cardinality_at_time(first_movers,skc2)) in_environment(u,skc2) subpopulation(first_movers,u,skc2)* -> greater(zero,growth_rate(first_movers,skc2))*. % 0.45/0.70 194[2:MRR:191.1,191.3,191.4,129.0,8.2,179.0] environment(u) || in_environment(u,skc2)* -> . % 0.45/0.70 197[2:Res:40.0,194.1] environment(skc3) || -> . % 0.45/0.70 198[2:SSi:197.0,1.0] || -> . % 0.45/0.70 199[2:Spt:198.0,130.0,132.0] || increases(cardinality_at_time(efficient_producers,skc2))* -> . % 0.45/0.70 200[2:Spt:198.0,130.1,130.2] || -> SkP0(cardinality_at_time(efficient_producers,skc2),cardinality_at_time(first_movers,skc2))* increases(cardinality_at_time(first_movers,skc2)). % 0.45/0.70 201[2:MRR:131.0,199.0] || -> SkP0(cardinality_at_time(efficient_producers,skc2),cardinality_at_time(first_movers,skc2))* decreases(cardinality_at_time(efficient_producers,skc2)). % 0.45/0.70 203[0:MRR:190.3,9.2] environment(u) || decreases(cardinality_at_time(efficient_producers,skc2)) in_environment(u,skc2)* -> greater(zero,growth_rate(efficient_producers,skc2))*. % 0.45/0.70 205[3:Spt:200.0] || -> SkP0(cardinality_at_time(efficient_producers,skc2),cardinality_at_time(first_movers,skc2))*. % 0.45/0.70 206[3:Res:205.0,4.0] || -> constant(cardinality_at_time(first_movers,skc2))*. % 0.45/0.70 207[3:Res:205.0,5.0] || -> constant(cardinality_at_time(efficient_producers,skc2))*. % 0.45/0.70 208[3:MRR:184.1,206.0] environment(u) || in_environment(u,skc2)*+ -> equal(growth_rate(first_movers,skc2),zero)**. % 0.45/0.70 209[3:MRR:185.1,207.0] environment(u) || in_environment(u,skc2)* -> equal(growth_rate(efficient_producers,skc2),zero)**. % 0.45/0.70 227[3:Res:40.0,208.1] environment(skc3) || -> equal(growth_rate(first_movers,skc2),zero)**. % 0.45/0.70 228[3:SSi:227.0,1.0] || -> equal(growth_rate(first_movers,skc2),zero)**. % 0.45/0.70 229[3:Rew:228.0,12.1] || equal(growth_rate(efficient_producers,skc2),zero)** equal(zero,zero) -> . % 0.45/0.70 232[3:Obv:229.1] || equal(growth_rate(efficient_producers,skc2),zero)** -> . % 0.45/0.70 233[3:MRR:209.2,232.0] environment(u) || in_environment(u,skc2)* -> . % 0.45/0.70 237[3:Res:40.0,233.1] environment(skc3) || -> . % 0.45/0.70 238[3:SSi:237.0,1.0] || -> . % 0.45/0.70 239[3:Spt:238.0,200.0,205.0] || SkP0(cardinality_at_time(efficient_producers,skc2),cardinality_at_time(first_movers,skc2))* -> . % 0.45/0.70 240[3:Spt:238.0,200.1] || -> increases(cardinality_at_time(first_movers,skc2))*. % 0.45/0.70 241[3:MRR:201.0,239.0] || -> decreases(cardinality_at_time(efficient_producers,skc2))*. % 0.45/0.70 243[3:MRR:173.1,240.0] environment(u) || in_environment(u,skc2)* -> greater(growth_rate(first_movers,skc2),zero)*. % 0.45/0.70 244[3:MRR:203.1,241.0] environment(u) || in_environment(u,skc2)* -> greater(zero,growth_rate(efficient_producers,skc2))*. % 0.45/0.70 259[4:Spt:11.0] || greater(zero,growth_rate(efficient_producers,skc2))* -> . % 0.45/0.70 260[4:MRR:244.2,259.0] environment(u) || in_environment(u,skc2)* -> . % 0.45/0.70 261[4:Res:40.0,260.1] environment(skc3) || -> . % 0.45/0.70 262[4:SSi:261.0,1.0] || -> . % 0.45/0.70 263[4:Spt:262.0,11.0,259.0] || -> greater(zero,growth_rate(efficient_producers,skc2))*. % 0.45/0.70 264[4:Spt:262.0,11.1] || greater(growth_rate(first_movers,skc2),zero)* -> . % 0.45/0.70 265[4:MRR:243.2,264.0] environment(u) || in_environment(u,skc2)* -> . % 0.45/0.70 266[4:Res:40.0,265.1] environment(skc3) || -> . % 0.45/0.70 267[4:SSi:266.0,1.0] || -> . % 0.45/0.70 268[1:Spt:267.0,121.0,129.0] || decreases(cardinality_at_time(first_movers,skc2))* -> . % 0.45/0.70 269[1:Spt:267.0,121.1,121.2] || -> SkP0(cardinality_at_time(efficient_producers,skc2),cardinality_at_time(first_movers,skc2))* increases(cardinality_at_time(first_movers,skc2)). % 0.45/0.70 270[1:MRR:122.0,268.0] || -> SkP0(cardinality_at_time(efficient_producers,skc2),cardinality_at_time(first_movers,skc2))* decreases(cardinality_at_time(efficient_producers,skc2)). % 0.45/0.70 272[2:Spt:269.0] || -> SkP0(cardinality_at_time(efficient_producers,skc2),cardinality_at_time(first_movers,skc2))*. % 0.45/0.70 273[2:Res:272.0,4.0] || -> constant(cardinality_at_time(first_movers,skc2))*. % 0.45/0.70 274[2:Res:272.0,5.0] || -> constant(cardinality_at_time(efficient_producers,skc2))*. % 0.45/0.70 275[2:MRR:184.1,273.0] environment(u) || in_environment(u,skc2)* -> equal(growth_rate(first_movers,skc2),zero)**. % 0.45/0.70 276[2:MRR:185.1,274.0] environment(u) || in_environment(u,skc2)* -> equal(growth_rate(efficient_producers,skc2),zero)**. % 0.45/0.70 292[3:Spt:12.0] || equal(growth_rate(efficient_producers,skc2),zero)** -> . % 0.45/0.70 293[3:MRR:276.2,292.0] environment(u) || in_environment(u,skc2)* -> . % 0.45/0.70 294[3:Res:40.0,293.1] environment(skc3) || -> . % 0.45/0.70 295[3:SSi:294.0,1.0] || -> . % 0.45/0.70 296[3:Spt:295.0,12.0,292.0] || -> equal(growth_rate(efficient_producers,skc2),zero)**. % 0.45/0.70 297[3:Spt:295.0,12.1] || equal(growth_rate(first_movers,skc2),zero)** -> . % 0.45/0.70 300[3:MRR:275.2,297.0] environment(u) || in_environment(u,skc2)* -> . % 0.45/0.70 302[3:Res:40.0,300.1] environment(skc3) || -> . % 0.45/0.70 303[3:SSi:302.0,1.0] || -> . % 0.45/0.70 304[2:Spt:303.0,269.0,272.0] || SkP0(cardinality_at_time(efficient_producers,skc2),cardinality_at_time(first_movers,skc2))* -> . % 0.45/0.70 305[2:Spt:303.0,269.1] || -> increases(cardinality_at_time(first_movers,skc2))*. % 0.45/0.70 306[2:MRR:270.0,304.0] || -> decreases(cardinality_at_time(efficient_producers,skc2))*. % 0.45/0.70 308[2:MRR:173.1,305.0] environment(u) || in_environment(u,skc2)* -> greater(growth_rate(first_movers,skc2),zero)*. % 0.45/0.70 309[2:MRR:203.1,306.0] environment(u) || in_environment(u,skc2)* -> greater(zero,growth_rate(efficient_producers,skc2))*. % 0.45/0.70 324[3:Spt:11.0] || greater(zero,growth_rate(efficient_producers,skc2))* -> . % 0.45/0.70 325[3:MRR:309.2,324.0] environment(u) || in_environment(u,skc2)* -> . % 0.45/0.70 326[3:Res:40.0,325.1] environment(skc3) || -> . % 0.45/0.70 327[3:SSi:326.0,1.0] || -> . % 0.45/0.70 328[3:Spt:327.0,11.0,324.0] || -> greater(zero,growth_rate(efficient_producers,skc2))*. % 0.45/0.70 329[3:Spt:327.0,11.1] || greater(growth_rate(first_movers,skc2),zero)* -> . % 0.45/0.70 330[3:MRR:308.2,329.0] environment(u) || in_environment(u,skc2)* -> . % 0.45/0.70 331[3:Res:40.0,330.1] environment(skc3) || -> . % 0.45/0.70 332[3:SSi:331.0,1.0] || -> . % 0.45/0.70 % SZS output end Refutation % 0.45/0.70 Formulae used in the proof : prove_l7 mp_abc_sum_increase mp_subpopulations mp_time_point_occur mp_non_zero_producers mp_only_members mp_growth_rate % 0.45/0.70 %------------------------------------------------------------------------------