%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT026+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n001.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.21s 0.53s % Output : Refutation 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT026+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.03 % Command : run_spass %d %s % 0.09/0.35 % Computer : n001.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Mon Sep 7 12:16:07 UTC 2026 % 0.09/0.36 % CPUTime : % 0.21/0.53 % 0.21/0.53 SPASS V 3.9 % 0.21/0.53 SPASS beiseite: Proof found. % 0.21/0.53 % SZS status Theorem % 0.21/0.53 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.21/0.53 SPASS derived 96 clauses, backtracked 21 clauses, performed 2 splits and kept 102 clauses. % 0.21/0.53 SPASS allocated 97731 KBytes. % 0.21/0.53 SPASS spent 0:00:00.16 on the problem. % 0.21/0.53 0:00:00.06 for the input. % 0.21/0.53 0:00:00.05 for the FLOTTER CNF translation. % 0.21/0.53 0:00:00.00 for inferences. % 0.21/0.53 0:00:00.00 for the backtracking. % 0.21/0.53 0:00:00.01 for the reduction. % 0.21/0.53 % 0.21/0.53 % 0.21/0.53 Here is a proof with depth 4, length 65 : % 0.21/0.53 % SZS output start Refutation % 0.21/0.53 1[0:Inp] || -> environment(skc3)*. % 0.21/0.53 2[0:Inp] || -> in_environment(skc3,skc2)*. % 0.21/0.53 3[0:Inp] || -> greater(skc2,critical_point(skc3))*r. % 0.21/0.53 4[0:Inp] || selection_favors(efficient_producers,first_movers,skc2)* -> . % 0.21/0.53 5[0:Inp] || greater(u,v) -> greater_or_equal(u,v)*. % 0.21/0.53 7[0:Inp] environment(u) || -> greater_or_equal(critical_point(u),appear(efficient_producers,u))*. % 0.21/0.53 8[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 0.21/0.53 9[0:Inp] environment(u) || in_environment(u,v) -> subpopulation(first_movers,u,v)*. % 0.21/0.53 10[0:Inp] environment(u) || in_environment(u,v) -> subpopulation(efficient_producers,u,v)*. % 0.21/0.53 11[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.21/0.53 12[0:Inp] environment(u) || in_environment(u,v)*+ -> greater_or_equal(cardinality_at_time(first_movers,v),zero)*. % 0.21/0.53 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.21/0.53 15[0:Inp] environment(u) || greater(v,critical_point(u)) subpopulations(first_movers,efficient_producers,u,v)* -> greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v)). % 0.21/0.53 16[0:Inp] environment(u) || greater(growth_rate(v,w),growth_rate(x,w)) subpopulations(x,v,u,w)* -> selection_favors(v,x,w). % 0.21/0.53 17[0:Inp] environment(u) || in_environment(u,v) greater(cardinality_at_time(first_movers,v),zero) greater(cardinality_at_time(efficient_producers,v),zero) -> subpopulations(first_movers,efficient_producers,u,v)*. % 0.21/0.53 18[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.21/0.53 27[0:Res:1.0,10.0] || in_environment(skc3,u) -> subpopulation(efficient_producers,skc3,u)*. % 0.21/0.53 28[0:Res:1.0,7.0] || -> greater_or_equal(critical_point(skc3),appear(efficient_producers,skc3))*. % 0.21/0.53 29[0:Res:2.0,17.1] environment(skc3) || greater(cardinality_at_time(efficient_producers,skc2),zero) greater(cardinality_at_time(first_movers,skc2),zero) -> subpopulations(first_movers,efficient_producers,skc3,skc2)*. % 0.21/0.53 30[0:Res:2.0,14.1] environment(skc3) || greater_or_equal(skc2,appear(efficient_producers,skc3))* -> greater(cardinality_at_time(efficient_producers,skc2),zero). % 0.21/0.53 31[0:Res:2.0,12.1] environment(skc3) || -> greater_or_equal(cardinality_at_time(first_movers,skc2),zero)*. % 0.21/0.53 32[0:Res:2.0,9.1] environment(skc3) || -> subpopulation(first_movers,skc3,skc2)*. % 0.21/0.53 35[0:Res:18.5,4.0] environment(u) || equal(cardinality_at_time(first_movers,skc2),zero) greater(cardinality_at_time(efficient_producers,skc2),zero) subpopulation(first_movers,u,skc2) subpopulation(efficient_producers,u,skc2)* -> . % 0.21/0.53 36[0:MRR:32.0,1.0] || -> subpopulation(first_movers,skc3,skc2)*. % 0.21/0.53 38[0:MRR:31.0,1.0] || -> greater_or_equal(cardinality_at_time(first_movers,skc2),zero)*. % 0.21/0.53 39[0:MRR:30.0,1.0] || greater_or_equal(skc2,appear(efficient_producers,skc3))* -> greater(cardinality_at_time(efficient_producers,skc2),zero). % 0.21/0.53 40[0:MRR:29.0,1.0] || greater(cardinality_at_time(first_movers,skc2),zero) greater(cardinality_at_time(efficient_producers,skc2),zero) -> subpopulations(first_movers,efficient_producers,skc3,skc2)*. % 0.21/0.53 42[0:Res:38.0,8.0] || -> equal(cardinality_at_time(first_movers,skc2),zero) greater(cardinality_at_time(first_movers,skc2),zero)*l. % 0.21/0.53 44[0:Res:28.0,8.0] || -> equal(appear(efficient_producers,skc3),critical_point(skc3)) greater(critical_point(skc3),appear(efficient_producers,skc3))*r. % 0.21/0.53 45[0:Res:7.1,8.0] environment(u) || -> equal(appear(efficient_producers,u),critical_point(u)) greater(critical_point(u),appear(efficient_producers,u))*r. % 0.21/0.53 48[1:Spt:42.0] || -> equal(cardinality_at_time(first_movers,skc2),zero)**. % 0.21/0.53 51[1:Rew:48.0,35.1] environment(u) || equal(zero,zero) greater(cardinality_at_time(efficient_producers,skc2),zero) subpopulation(first_movers,u,skc2) subpopulation(efficient_producers,u,skc2)* -> . % 0.21/0.53 52[1:Obv:51.1] environment(u) || greater(cardinality_at_time(efficient_producers,skc2),zero) subpopulation(first_movers,u,skc2) subpopulation(efficient_producers,u,skc2)* -> . % 0.21/0.53 56[0:Res:5.1,39.0] || greater(skc2,appear(efficient_producers,skc3))*r -> greater(cardinality_at_time(efficient_producers,skc2),zero). % 0.21/0.53 64[2:Spt:44.0] || -> equal(appear(efficient_producers,skc3),critical_point(skc3))**. % 0.21/0.53 69[2:Rew:64.0,56.0] || greater(skc2,critical_point(skc3)) -> greater(cardinality_at_time(efficient_producers,skc2),zero)*l. % 0.21/0.53 70[2:MRR:69.0,3.0] || -> greater(cardinality_at_time(efficient_producers,skc2),zero)*l. % 0.21/0.53 72[2:MRR:52.1,70.0] environment(u) || subpopulation(first_movers,u,skc2) subpopulation(efficient_producers,u,skc2)* -> . % 0.21/0.53 78[2:Res:27.1,72.2] environment(skc3) || in_environment(skc3,skc2) subpopulation(first_movers,skc3,skc2)* -> . % 0.21/0.53 82[2:SSi:78.0,1.0] || in_environment(skc3,skc2) subpopulation(first_movers,skc3,skc2)* -> . % 0.21/0.53 83[2:MRR:82.0,82.1,2.0,36.0] || -> . % 0.21/0.53 86[2:Spt:83.0,44.0,64.0] || equal(appear(efficient_producers,skc3),critical_point(skc3))** -> . % 0.21/0.53 87[2:Spt:83.0,44.1] || -> greater(critical_point(skc3),appear(efficient_producers,skc3))*r. % 0.21/0.53 102[2:NCh:11.2,11.1,56.0,87.0] || greater(skc2,critical_point(skc3)) -> greater(cardinality_at_time(efficient_producers,skc2),zero)*l. % 0.21/0.53 104[0:NCh:11.2,11.1,56.0,45.2] environment(skc3) || greater(skc2,critical_point(skc3)) -> greater(cardinality_at_time(efficient_producers,skc2),zero) equal(appear(efficient_producers,skc3),critical_point(skc3))**. % 0.21/0.53 106[2:MRR:102.0,3.0] || -> greater(cardinality_at_time(efficient_producers,skc2),zero)*l. % 0.21/0.53 107[2:MRR:52.1,106.0] environment(u) || subpopulation(first_movers,u,skc2) subpopulation(efficient_producers,u,skc2)* -> . % 0.21/0.53 127[2:Res:27.1,107.2] environment(skc3) || in_environment(skc3,skc2) subpopulation(first_movers,skc3,skc2)* -> . % 0.21/0.53 131[2:SSi:127.0,1.0] || in_environment(skc3,skc2) subpopulation(first_movers,skc3,skc2)* -> . % 0.21/0.53 132[2:MRR:131.0,131.1,2.0,36.0] || -> . % 0.21/0.53 135[1:Spt:132.0,42.0,48.0] || equal(cardinality_at_time(first_movers,skc2),zero)** -> . % 0.21/0.53 136[1:Spt:132.0,42.1] || -> greater(cardinality_at_time(first_movers,skc2),zero)*l. % 0.21/0.53 138[1:MRR:40.0,136.0] || greater(cardinality_at_time(efficient_producers,skc2),zero) -> subpopulations(first_movers,efficient_producers,skc3,skc2)*. % 0.21/0.53 139[0:SSi:104.0,1.0] || greater(skc2,critical_point(skc3)) -> greater(cardinality_at_time(efficient_producers,skc2),zero) equal(appear(efficient_producers,skc3),critical_point(skc3))**. % 0.21/0.53 140[0:MRR:139.0,3.0] || -> greater(cardinality_at_time(efficient_producers,skc2),zero) equal(appear(efficient_producers,skc3),critical_point(skc3))**. % 0.21/0.53 143[0:Rew:140.1,56.0] || greater(skc2,critical_point(skc3)) -> greater(cardinality_at_time(efficient_producers,skc2),zero)*l. % 0.21/0.53 144[0:MRR:143.0,3.0] || -> greater(cardinality_at_time(efficient_producers,skc2),zero)*l. % 0.21/0.53 145[1:MRR:138.0,144.0] || -> subpopulations(first_movers,efficient_producers,skc3,skc2)*. % 0.21/0.53 151[1:Res:145.0,16.2] environment(skc3) || greater(growth_rate(efficient_producers,skc2),growth_rate(first_movers,skc2)) -> selection_favors(efficient_producers,first_movers,skc2)*. % 0.21/0.53 152[1:Res:145.0,15.2] environment(skc3) || greater(skc2,critical_point(skc3)) -> greater(growth_rate(efficient_producers,skc2),growth_rate(first_movers,skc2))*l. % 0.21/0.53 153[1:SSi:151.0,1.0] || greater(growth_rate(efficient_producers,skc2),growth_rate(first_movers,skc2)) -> selection_favors(efficient_producers,first_movers,skc2)*. % 0.21/0.53 154[1:MRR:153.1,4.0] || greater(growth_rate(efficient_producers,skc2),growth_rate(first_movers,skc2))*l -> . % 0.21/0.53 155[1:SSi:152.0,1.0] || greater(skc2,critical_point(skc3)) -> greater(growth_rate(efficient_producers,skc2),growth_rate(first_movers,skc2))*l. % 0.21/0.53 156[1:MRR:155.0,3.0] || -> greater(growth_rate(efficient_producers,skc2),growth_rate(first_movers,skc2))*l. % 0.21/0.53 157[1:MRR:156.0,154.0] || -> . % 0.21/0.54 % SZS output end Refutation % 0.21/0.54 Formulae used in the proof : prove_l8 mp_greater_or_equal mp_critical_point_after_EP mp_subpopulations mp_greater_transitivity mp_first_movers_exist t6 d1 mp1_high_growth_rates mp_non_empty_fm_and_ep mp2_favour_members % 0.21/0.54 %------------------------------------------------------------------------------