%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT026-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n010.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 : Unsatisfiable 0.22s 0.47s % Output : Refutation 0.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT026-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.07/0.34 % Computer : n010.cluster.edu % 0.07/0.34 % Model : x86_64 x86_64 % 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.34 % Memory : 8046.5625MB % 0.07/0.34 % OS : Linux 6.8.0-71-generic % 0.07/0.34 % CPULimit : 300 % 0.07/0.34 % WCLimit : 300 % 0.07/0.34 % DateTime : Mon Sep 7 12:12:26 UTC 2026 % 0.07/0.34 % CPUTime : % 0.22/0.47 % 0.22/0.47 SPASS V 3.9 % 0.22/0.47 SPASS beiseite: Proof found. % 0.22/0.47 % SZS status Theorem % 0.22/0.47 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.22/0.47 SPASS derived 119 clauses, backtracked 21 clauses, performed 2 splits and kept 124 clauses. % 0.22/0.47 SPASS allocated 75794 KBytes. % 0.22/0.47 SPASS spent 0:00:00.12 on the problem. % 0.22/0.47 0:00:00.06 for the input. % 0.22/0.47 0:00:00.00 for the FLOTTER CNF translation. % 0.22/0.47 0:00:00.00 for inferences. % 0.22/0.47 0:00:00.00 for the backtracking. % 0.22/0.47 0:00:00.02 for the reduction. % 0.22/0.47 % 0.22/0.47 % 0.22/0.47 Here is a proof with depth 4, length 66 : % 0.22/0.47 % SZS output start Refutation % 0.22/0.47 1[0:Inp] environment(u) || greater(growth_rate(v,w),growth_rate(x,w)) subpopulations(x,v,u,w)* -> selection_favors(v,x,w). % 0.22/0.47 2[0:Inp] environment(u) || equal(cardinality_at_time(v,w),zero) greater(cardinality_at_time(x,w),zero)+ subpopulation(v,u,w)* subpopulation(x,u,w)* -> selection_favors(x,v,w)*. % 0.22/0.47 3[0:Inp] environment(u) || in_environment(u,v) greater(cardinality_at_time(efficient_producers,v),zero) greater(cardinality_at_time(first_movers,v),zero) -> subpopulations(first_movers,efficient_producers,u,v)*. % 0.22/0.47 4[0:Inp] environment(u) || in_environment(u,v)*+ -> greater_or_equal(cardinality_at_time(first_movers,v),zero)*. % 0.22/0.47 5[0:Inp] environment(u) || in_environment(u,v) -> subpopulation(first_movers,u,v)*. % 0.22/0.47 6[0:Inp] environment(u) || in_environment(u,v) -> subpopulation(efficient_producers,u,v)*. % 0.22/0.47 7[0:Inp] environment(u) || -> greater_or_equal(critical_point(u),appear(efficient_producers,u))*. % 0.22/0.47 8[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.22/0.47 9[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 0.22/0.47 10[0:Inp] || greater(u,v) -> greater_or_equal(u,v)*. % 0.22/0.47 13[0:Inp] environment(u) || greater(v,w)*+ equal(w,critical_point(u))* subpopulations(first_movers,efficient_producers,u,v)* -> greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v)). % 0.22/0.47 14[0:Inp] environment(u) || in_environment(u,v) greater_or_equal(v,appear(efficient_producers,u))* -> greater(cardinality_at_time(efficient_producers,v),zero). % 0.22/0.47 15[0:Inp] || -> environment(sk1)*. % 0.22/0.47 16[0:Inp] || -> in_environment(sk1,sk2)*. % 0.22/0.47 17[0:Inp] || -> greater(sk2,critical_point(sk1))*r. % 0.22/0.47 18[0:Inp] || selection_favors(efficient_producers,first_movers,sk2)* -> . % 0.22/0.47 27[0:Res:15.0,6.0] || in_environment(sk1,u) -> subpopulation(efficient_producers,sk1,u)*. % 0.22/0.47 28[0:Res:15.0,7.0] || -> greater_or_equal(critical_point(sk1),appear(efficient_producers,sk1))*. % 0.22/0.47 29[0:Res:16.0,3.1] environment(sk1) || greater(cardinality_at_time(first_movers,sk2),zero) greater(cardinality_at_time(efficient_producers,sk2),zero) -> subpopulations(first_movers,efficient_producers,sk1,sk2)*. % 0.22/0.47 30[0:Res:16.0,14.1] environment(sk1) || greater_or_equal(sk2,appear(efficient_producers,sk1))* -> greater(cardinality_at_time(efficient_producers,sk2),zero). % 0.22/0.47 31[0:Res:16.0,4.1] environment(sk1) || -> greater_or_equal(cardinality_at_time(first_movers,sk2),zero)*. % 0.22/0.47 32[0:Res:16.0,5.1] environment(sk1) || -> subpopulation(first_movers,sk1,sk2)*. % 0.22/0.47 35[0:Res:2.5,18.0] environment(u) || equal(cardinality_at_time(first_movers,sk2),zero) greater(cardinality_at_time(efficient_producers,sk2),zero) subpopulation(first_movers,u,sk2) subpopulation(efficient_producers,u,sk2)* -> . % 0.22/0.47 36[0:MRR:32.0,15.0] || -> subpopulation(first_movers,sk1,sk2)*. % 0.22/0.47 38[0:MRR:31.0,15.0] || -> greater_or_equal(cardinality_at_time(first_movers,sk2),zero)*. % 0.22/0.47 39[0:MRR:30.0,15.0] || greater_or_equal(sk2,appear(efficient_producers,sk1))* -> greater(cardinality_at_time(efficient_producers,sk2),zero). % 0.22/0.47 40[0:MRR:29.0,15.0] || greater(cardinality_at_time(efficient_producers,sk2),zero) greater(cardinality_at_time(first_movers,sk2),zero) -> subpopulations(first_movers,efficient_producers,sk1,sk2)*. % 0.22/0.47 42[0:Res:38.0,9.0] || -> equal(cardinality_at_time(first_movers,sk2),zero) greater(cardinality_at_time(first_movers,sk2),zero)*l. % 0.22/0.47 44[0:Res:28.0,9.0] || -> equal(appear(efficient_producers,sk1),critical_point(sk1)) greater(critical_point(sk1),appear(efficient_producers,sk1))*r. % 0.22/0.47 45[0:Res:7.1,9.0] environment(u) || -> equal(appear(efficient_producers,u),critical_point(u)) greater(critical_point(u),appear(efficient_producers,u))*r. % 0.22/0.47 48[1:Spt:42.0] || -> equal(cardinality_at_time(first_movers,sk2),zero)**. % 0.22/0.47 51[1:Rew:48.0,35.1] environment(u) || equal(zero,zero) greater(cardinality_at_time(efficient_producers,sk2),zero) subpopulation(first_movers,u,sk2) subpopulation(efficient_producers,u,sk2)* -> . % 0.22/0.47 52[1:Obv:51.1] environment(u) || greater(cardinality_at_time(efficient_producers,sk2),zero) subpopulation(first_movers,u,sk2) subpopulation(efficient_producers,u,sk2)* -> . % 0.22/0.47 56[0:Res:10.1,39.0] || greater(sk2,appear(efficient_producers,sk1))*r -> greater(cardinality_at_time(efficient_producers,sk2),zero). % 0.22/0.47 58[2:Spt:44.0] || -> equal(appear(efficient_producers,sk1),critical_point(sk1))**. % 0.22/0.47 63[2:Rew:58.0,56.0] || greater(sk2,critical_point(sk1)) -> greater(cardinality_at_time(efficient_producers,sk2),zero)*l. % 0.22/0.47 64[2:MRR:63.0,17.0] || -> greater(cardinality_at_time(efficient_producers,sk2),zero)*l. % 0.22/0.47 66[2:MRR:52.1,64.0] environment(u) || subpopulation(first_movers,u,sk2) subpopulation(efficient_producers,u,sk2)* -> . % 0.22/0.47 76[2:Res:27.1,66.2] environment(sk1) || in_environment(sk1,sk2) subpopulation(first_movers,sk1,sk2)* -> . % 0.22/0.47 80[2:SSi:76.0,15.0] || in_environment(sk1,sk2) subpopulation(first_movers,sk1,sk2)* -> . % 0.22/0.47 81[2:MRR:80.0,80.1,16.0,36.0] || -> . % 0.22/0.47 84[2:Spt:81.0,44.0,58.0] || equal(appear(efficient_producers,sk1),critical_point(sk1))** -> . % 0.22/0.47 85[2:Spt:81.0,44.1] || -> greater(critical_point(sk1),appear(efficient_producers,sk1))*r. % 0.22/0.47 98[2:NCh:8.2,8.1,56.0,85.0] || greater(sk2,critical_point(sk1)) -> greater(cardinality_at_time(efficient_producers,sk2),zero)*l. % 0.22/0.47 100[0:NCh:8.2,8.1,56.0,45.2] environment(sk1) || greater(sk2,critical_point(sk1)) -> greater(cardinality_at_time(efficient_producers,sk2),zero) equal(appear(efficient_producers,sk1),critical_point(sk1))**. % 0.22/0.47 102[2:MRR:98.0,17.0] || -> greater(cardinality_at_time(efficient_producers,sk2),zero)*l. % 0.22/0.47 103[2:MRR:52.1,102.0] environment(u) || subpopulation(first_movers,u,sk2) subpopulation(efficient_producers,u,sk2)* -> . % 0.22/0.47 123[2:Res:27.1,103.2] environment(sk1) || in_environment(sk1,sk2) subpopulation(first_movers,sk1,sk2)* -> . % 0.22/0.47 127[2:SSi:123.0,15.0] || in_environment(sk1,sk2) subpopulation(first_movers,sk1,sk2)* -> . % 0.22/0.47 128[2:MRR:127.0,127.1,16.0,36.0] || -> . % 0.22/0.47 131[1:Spt:128.0,42.0,48.0] || equal(cardinality_at_time(first_movers,sk2),zero)** -> . % 0.22/0.47 132[1:Spt:128.0,42.1] || -> greater(cardinality_at_time(first_movers,sk2),zero)*l. % 0.22/0.47 134[1:MRR:40.1,132.0] || greater(cardinality_at_time(efficient_producers,sk2),zero) -> subpopulations(first_movers,efficient_producers,sk1,sk2)*. % 0.22/0.47 135[0:SSi:100.0,15.0] || greater(sk2,critical_point(sk1)) -> greater(cardinality_at_time(efficient_producers,sk2),zero) equal(appear(efficient_producers,sk1),critical_point(sk1))**. % 0.22/0.47 136[0:MRR:135.0,17.0] || -> greater(cardinality_at_time(efficient_producers,sk2),zero) equal(appear(efficient_producers,sk1),critical_point(sk1))**. % 0.22/0.47 139[0:Rew:136.1,56.0] || greater(sk2,critical_point(sk1)) -> greater(cardinality_at_time(efficient_producers,sk2),zero)*l. % 0.22/0.47 140[0:MRR:139.0,17.0] || -> greater(cardinality_at_time(efficient_producers,sk2),zero)*l. % 0.22/0.47 141[1:MRR:134.0,140.0] || -> subpopulations(first_movers,efficient_producers,sk1,sk2)*. % 0.22/0.47 147[1:Res:141.0,1.2] environment(sk1) || greater(growth_rate(efficient_producers,sk2),growth_rate(first_movers,sk2)) -> selection_favors(efficient_producers,first_movers,sk2)*. % 0.22/0.47 148[1:SSi:147.0,15.0] || greater(growth_rate(efficient_producers,sk2),growth_rate(first_movers,sk2)) -> selection_favors(efficient_producers,first_movers,sk2)*. % 0.22/0.47 149[1:MRR:148.1,18.0] || greater(growth_rate(efficient_producers,sk2),growth_rate(first_movers,sk2))*l -> . % 0.22/0.47 150[0:Res:17.0,13.1] environment(u) || equal(critical_point(sk1),critical_point(u)) subpopulations(first_movers,efficient_producers,u,sk2)* -> greater(growth_rate(efficient_producers,sk2),growth_rate(first_movers,sk2)). % 0.22/0.47 168[1:MRR:150.3,149.0] environment(u) || equal(critical_point(sk1),critical_point(u)) subpopulations(first_movers,efficient_producers,u,sk2)* -> . % 0.22/0.47 178[1:Res:141.0,168.2] environment(sk1) || equal(critical_point(sk1),critical_point(sk1))* -> . % 0.22/0.47 179[1:Obv:178.1] environment(sk1) || -> . % 0.22/0.47 180[1:SSi:179.0,15.0] || -> . % 0.22/0.48 % SZS output end Refutation % 0.22/0.48 Formulae used in the proof : mp1_high_growth_rates_28 mp2_favour_members_29 mp_non_empty_fm_and_ep_30 mp_first_movers_exist_31 mp_subpopulations_32 mp_subpopulations_33 mp_critical_point_after_EP_34 mp_greater_transitivity_35 mp_greater_or_equal_36 mp_greater_or_equal_37 d1_40 t6_41 prove_l8_42 prove_l8_43 prove_l8_44 prove_l8_45 % 0.22/0.48 %------------------------------------------------------------------------------