%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT027-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.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.57s 0.89s % Output : Refutation 0.67s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT027-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.10/0.35 % Computer : n019.cluster.edu % 0.10/0.35 % Model : x86_64 x86_64 % 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.35 % Memory : 8046.5625MB % 0.10/0.35 % OS : Linux 6.8.0-71-generic % 0.10/0.35 % CPULimit : 300 % 0.10/0.35 % WCLimit : 300 % 0.10/0.35 % DateTime : Mon Sep 7 12:14:07 UTC 2026 % 0.10/0.35 % CPUTime : % 0.57/0.89 % 0.57/0.89 SPASS V 3.9 % 0.57/0.89 SPASS beiseite: Proof found. % 0.57/0.89 % SZS status Theorem % 0.57/0.89 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.57/0.89 SPASS derived 641 clauses, backtracked 0 clauses, performed 4 splits and kept 477 clauses. % 0.57/0.89 SPASS allocated 76712 KBytes. % 0.57/0.89 SPASS spent 0:00:00.53 on the problem. % 0.57/0.89 0:00:00.06 for the input. % 0.57/0.89 0:00:00.00 for the FLOTTER CNF translation. % 0.57/0.89 0:00:00.03 for inferences. % 0.57/0.89 0:00:00.00 for the backtracking. % 0.57/0.89 0:00:00.40 for the reduction. % 0.57/0.89 % 0.57/0.89 % 0.57/0.89 Here is a proof with depth 4, length 59 : % 0.57/0.89 % SZS output start Refutation % 0.57/0.89 1[0:Inp] stable(u) environment(u) || in_environment(u,v) -> contracts_from(v,first_movers) greater(cardinality_at_time(first_movers,sk1(v,u)),zero)*l. % 0.57/0.89 2[0:Inp] stable(u) environment(u) || in_environment(u,v) -> contracts_from(v,first_movers) greater_or_equal(sk1(v,u),v)*. % 0.57/0.89 3[0:Inp] stable(u) environment(u) || in_environment(u,v) greater(zero,growth_rate(first_movers,sk1(v,u)))*r -> contracts_from(v,first_movers). % 0.57/0.89 4[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.57/0.89 5[0:Inp] stable(u) environment(u) || greater(v,w)*+ in_environment(u,w)* -> in_environment(u,v)*. % 0.57/0.89 6[0:Inp] stable(u) environment(u) || -> in_environment(u,appear(efficient_producers,u))*. % 0.57/0.89 7[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.57/0.89 8[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 0.57/0.89 9[0:Inp] || greater(u,v) -> greater_or_equal(u,v)*. % 0.57/0.89 11[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.57/0.89 12[0:Inp] stable(u) environment(u) || -> greater(sk2(u),appear(efficient_producers,u))*r. % 0.57/0.89 13[0:Inp] stable(u) environment(u) || greater_or_equal(v,sk2(u)) subpopulations(first_movers,efficient_producers,u,v)* -> greater(zero,growth_rate(first_movers,v)). % 0.57/0.89 14[0:Inp] || -> environment(sk3)*. % 0.57/0.89 15[0:Inp] || -> stable(sk3)*. % 0.57/0.89 16[0:Inp] || contracts_from(u,first_movers)* greater(u,appear(efficient_producers,sk3))*+ -> . % 0.57/0.89 20[0:Res:15.0,5.1] environment(sk3) || in_environment(sk3,u)* greater(v,u)* -> in_environment(sk3,v)*. % 0.57/0.89 21[0:Res:15.0,2.1] environment(sk3) || in_environment(sk3,u) -> greater_or_equal(sk1(u,sk3),u)* contracts_from(u,first_movers). % 0.57/0.89 22[0:Res:15.0,12.1] environment(sk3) || -> greater(sk2(sk3),appear(efficient_producers,sk3))*r. % 0.57/0.89 23[0:Res:15.0,6.1] environment(sk3) || -> in_environment(sk3,appear(efficient_producers,sk3))*. % 0.57/0.89 26[0:Res:14.0,3.0] stable(sk3) || in_environment(sk3,u) greater(zero,growth_rate(first_movers,sk1(u,sk3)))*r -> contracts_from(u,first_movers). % 0.57/0.89 27[0:Res:14.0,1.0] stable(sk3) || in_environment(sk3,u) -> greater(cardinality_at_time(first_movers,sk1(u,sk3)),zero)*l contracts_from(u,first_movers). % 0.57/0.89 33[0:MRR:23.0,14.0] || -> in_environment(sk3,appear(efficient_producers,sk3))*. % 0.57/0.89 34[0:MRR:22.0,14.0] || -> greater(sk2(sk3),appear(efficient_producers,sk3))*r. % 0.57/0.89 35[0:MRR:21.0,14.0] || in_environment(sk3,u) -> contracts_from(u,first_movers) greater_or_equal(sk1(u,sk3),u)*. % 0.57/0.89 36[0:MRR:20.0,14.0] || greater(u,v)*+ in_environment(sk3,v)* -> in_environment(sk3,u)*. % 0.57/0.89 37[0:MRR:27.0,15.0] || in_environment(sk3,u) -> contracts_from(u,first_movers) greater(cardinality_at_time(first_movers,sk1(u,sk3)),zero)*l. % 0.57/0.89 38[0:MRR:26.0,15.0] || in_environment(sk3,u) greater(zero,growth_rate(first_movers,sk1(u,sk3)))*r -> contracts_from(u,first_movers). % 0.57/0.89 40[0:Res:34.0,16.1] || contracts_from(sk2(sk3),first_movers)* -> . % 0.57/0.89 45[0:Res:35.2,8.0] || in_environment(sk3,u) -> contracts_from(u,first_movers) equal(sk1(u,sk3),u) greater(sk1(u,sk3),u)*l. % 0.57/0.89 46[0:Res:34.0,36.0] || in_environment(sk3,appear(efficient_producers,sk3))* -> in_environment(sk3,sk2(sk3)). % 0.57/0.89 48[0:NCh:7.2,7.1,36.0,34.0] || equal(u,sk2(sk3)) in_environment(sk3,appear(efficient_producers,sk3))* -> in_environment(sk3,u)*. % 0.57/0.89 49[0:MRR:46.0,33.0] || -> in_environment(sk3,sk2(sk3))*. % 0.57/0.89 50[0:MRR:48.1,33.0] || equal(u,sk2(sk3)) -> in_environment(sk3,u)*. % 0.57/0.89 63[0:Res:2.4,8.0] stable(u) environment(u) || in_environment(u,v) -> contracts_from(v,first_movers) equal(sk1(v,u),v) greater(sk1(v,u),v)*l. % 0.57/0.89 82[0:NCh:7.2,7.1,5.2,12.2] stable(u) environment(u) stable(v) environment(v) || equal(w,sk2(v))* in_environment(u,appear(efficient_producers,v))*+ -> in_environment(u,w)*. % 0.57/0.89 98[0:Res:9.1,11.2] environment(u) || greater(v,appear(efficient_producers,u))*+ in_environment(u,v)* -> greater(cardinality_at_time(efficient_producers,v),zero)*l. % 0.57/0.89 144[0:Res:4.4,13.3] environment(u) stable(u) environment(u) || in_environment(u,v) greater(cardinality_at_time(efficient_producers,v),zero) greater(cardinality_at_time(first_movers,v),zero) greater_or_equal(v,sk2(u))* -> greater(zero,growth_rate(first_movers,v)). % 0.57/0.89 146[0:Obv:144.0] stable(u) environment(u) || in_environment(u,v) greater(cardinality_at_time(efficient_producers,v),zero) greater(cardinality_at_time(first_movers,v),zero) greater_or_equal(v,sk2(u))* -> greater(zero,growth_rate(first_movers,v)). % 0.57/0.89 199[0:Res:6.2,82.5] stable(u) environment(u) stable(u) environment(u) stable(u) environment(u) || equal(v,sk2(u)) -> in_environment(u,v)*. % 0.57/0.89 203[0:Obv:199.3] stable(u) environment(u) || equal(v,sk2(u)) -> in_environment(u,v)*. % 0.57/0.89 249[0:NCh:7.2,7.1,98.1,12.2] environment(u) stable(u) environment(u) || greater(v,sk2(u)) in_environment(u,v)* -> greater(cardinality_at_time(efficient_producers,v),zero)*l. % 0.57/0.89 250[0:NCh:7.2,7.1,98.1,12.2] environment(u) stable(u) environment(u) || equal(v,sk2(u)) in_environment(u,v)* -> greater(cardinality_at_time(efficient_producers,v),zero)*l. % 0.57/0.89 259[0:Obv:250.0] stable(u) environment(u) || equal(v,sk2(u)) in_environment(u,v)* -> greater(cardinality_at_time(efficient_producers,v),zero)*l. % 0.57/0.89 260[0:MRR:259.3,203.3] stable(u) environment(u) || equal(v,sk2(u))*+ -> greater(cardinality_at_time(efficient_producers,v),zero)*l. % 0.57/0.89 261[0:Obv:249.0] stable(u) environment(u) || greater(v,sk2(u))+ in_environment(u,v)* -> greater(cardinality_at_time(efficient_producers,v),zero)*l. % 0.57/0.89 275[0:Res:63.5,36.0] stable(u) environment(u) || in_environment(u,v) in_environment(sk3,v) -> contracts_from(v,first_movers) equal(sk1(v,u),v) in_environment(sk3,sk1(v,u))*. % 0.57/0.89 495[0:Res:35.2,146.5] stable(u) environment(u) || in_environment(sk3,sk2(u)) in_environment(u,sk1(sk2(u),sk3))* greater(cardinality_at_time(efficient_producers,sk1(sk2(u),sk3)),zero) greater(cardinality_at_time(first_movers,sk1(sk2(u),sk3)),zero) -> contracts_from(sk2(u),first_movers) greater(zero,growth_rate(first_movers,sk1(sk2(u),sk3)))*r. % 0.57/0.89 499[0:MRR:495.5,495.7,37.2,38.1] stable(u) environment(u) || in_environment(sk3,sk2(u)) in_environment(u,sk1(sk2(u),sk3))* greater(cardinality_at_time(efficient_producers,sk1(sk2(u),sk3)),zero)*l -> contracts_from(sk2(u),first_movers). % 0.57/0.89 810[0:Res:45.3,261.2] stable(u) environment(u) || in_environment(sk3,sk2(u)) in_environment(u,sk1(sk2(u),sk3))* -> contracts_from(sk2(u),first_movers) equal(sk1(sk2(u),sk3),sk2(u)) greater(cardinality_at_time(efficient_producers,sk1(sk2(u),sk3)),zero)*l. % 0.57/0.89 834[0:MRR:810.5,260.2] stable(u) environment(u) || in_environment(sk3,sk2(u)) in_environment(u,sk1(sk2(u),sk3))* -> contracts_from(sk2(u),first_movers) greater(cardinality_at_time(efficient_producers,sk1(sk2(u),sk3)),zero)*l. % 0.57/0.89 835[0:MRR:834.5,499.4] stable(u) environment(u) || in_environment(sk3,sk2(u)) in_environment(u,sk1(sk2(u),sk3))* -> contracts_from(sk2(u),first_movers). % 0.57/0.89 839[0:Res:50.1,835.3] stable(sk3) environment(sk3) || equal(sk1(sk2(sk3),sk3),sk2(sk3))** in_environment(sk3,sk2(sk3)) -> contracts_from(sk2(sk3),first_movers). % 0.57/0.89 841[0:Res:275.6,835.3] stable(sk3) environment(sk3) stable(sk3) environment(sk3) || in_environment(sk3,sk2(sk3)) in_environment(sk3,sk2(sk3)) in_environment(sk3,sk2(sk3)) -> contracts_from(sk2(sk3),first_movers) equal(sk1(sk2(sk3),sk3),sk2(sk3))** contracts_from(sk2(sk3),first_movers). % 0.57/0.89 844[0:SSi:839.1,839.0,15.0,14.0,15.0,14.0] || equal(sk1(sk2(sk3),sk3),sk2(sk3))** in_environment(sk3,sk2(sk3)) -> contracts_from(sk2(sk3),first_movers). % 0.57/0.89 845[0:MRR:844.1,844.2,49.0,40.0] || equal(sk1(sk2(sk3),sk3),sk2(sk3))** -> . % 0.57/0.89 856[0:Obv:841.7] stable(sk3) environment(sk3) || in_environment(sk3,sk2(sk3)) -> equal(sk1(sk2(sk3),sk3),sk2(sk3))** contracts_from(sk2(sk3),first_movers). % 0.67/0.91 857[0:SSi:856.1,856.0,15.0,14.0,15.0,14.0] || in_environment(sk3,sk2(sk3)) -> equal(sk1(sk2(sk3),sk3),sk2(sk3))** contracts_from(sk2(sk3),first_movers). % 0.67/0.91 858[0:MRR:857.0,857.2,49.0,40.0] || -> equal(sk1(sk2(sk3),sk3),sk2(sk3))**. % 0.67/0.91 859[0:MRR:858.0,845.0] || -> . % 0.67/0.91 % SZS output end Refutation % 0.67/0.91 Formulae used in the proof : mp_contracts_from_24 mp_contracts_from_25 mp_contracts_from_26 mp_non_empty_fm_and_ep_27 mp_long_stable_environments_28 mp_EP_in_stable_environments_29 mp_greater_transitivity_30 mp_greater_or_equal_31 mp_greater_or_equal_32 t6_34 l10_35 l10_36 prove_l9_37 prove_l9_38 prove_l9_39 % 0.67/0.91 %------------------------------------------------------------------------------