%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT024-1 : TPTP v9.3.0. Released v2.4.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 : 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.21s 0.47s % Output : Refutation 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT024-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.08/0.35 % Computer : n003.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Mon Sep 7 12:10:09 UTC 2026 % 0.08/0.35 % CPUTime : % 0.21/0.47 % 0.21/0.47 SPASS V 3.9 % 0.21/0.47 SPASS beiseite: Proof found. % 0.21/0.47 % SZS status Theorem % 0.21/0.47 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.21/0.47 SPASS derived 48 clauses, backtracked 27 clauses, performed 3 splits and kept 84 clauses. % 0.21/0.47 SPASS allocated 75676 KBytes. % 0.21/0.47 SPASS spent 0:00:00.11 on the problem. % 0.21/0.47 0:00:00.06 for the input. % 0.21/0.47 0:00:00.00 for the FLOTTER CNF translation. % 0.21/0.47 0:00:00.00 for inferences. % 0.21/0.47 0:00:00.00 for the backtracking. % 0.21/0.47 0:00:00.00 for the reduction. % 0.21/0.47 % 0.21/0.47 % 0.21/0.47 Here is a proof with depth 3, length 76 : % 0.21/0.47 % SZS output start Refutation % 0.21/0.47 1[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v)* -> in_environment(u,v). % 0.21/0.47 2[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v) -> greater(number_of_organizations(u,v),zero)*. % 0.21/0.47 3[0:Inp] environment(u) || greater_or_equal(v,equilibrium(u)) greater(equilibrium(u),v)* -> . % 0.21/0.47 5[0:Inp] environment(u) || in_environment(u,v) greater(number_of_organizations(u,v),zero)* -> constant(resources(u,v)) greater(equilibrium(u),v). % 0.21/0.47 7[0:Inp] environment(u) || constant(resources(u,v))* in_environment(u,v) -> constant(number_of_organizations(u,v)). % 0.21/0.47 9[0:Inp] environment(u) || constant(number_of_organizations(u,v)) subpopulations(first_movers,efficient_producers,u,v)* -> greater(zero,growth_rate(first_movers,v)) greater(growth_rate(first_movers,v),zero)* equal(growth_rate(first_movers,v),zero). % 0.21/0.47 10[0:Inp] environment(u) || constant(number_of_organizations(u,v)) subpopulations(first_movers,efficient_producers,u,v)* -> greater(zero,growth_rate(efficient_producers,v)) greater(growth_rate(efficient_producers,v),zero)* equal(growth_rate(first_movers,v),zero). % 0.21/0.47 12[0:Inp] environment(u) || constant(number_of_organizations(u,v)) subpopulations(first_movers,efficient_producers,u,v)* -> greater(growth_rate(efficient_producers,v),zero)* greater(growth_rate(first_movers,v),zero) equal(growth_rate(efficient_producers,v),zero). % 0.21/0.47 13[0:Inp] environment(u) || constant(number_of_organizations(u,v)) subpopulations(first_movers,efficient_producers,u,v)* -> greater(zero,growth_rate(first_movers,v)) greater(growth_rate(first_movers,v),zero)* equal(growth_rate(efficient_producers,v),zero). % 0.21/0.47 14[0:Inp] environment(u) || constant(number_of_organizations(u,v)) subpopulations(first_movers,efficient_producers,u,v)* -> greater(zero,growth_rate(efficient_producers,v)) greater(growth_rate(efficient_producers,v),zero)* equal(growth_rate(efficient_producers,v),zero). % 0.21/0.47 15[0:Inp] environment(u) || constant(number_of_organizations(u,v)) subpopulations(first_movers,efficient_producers,u,v)* -> greater(zero,growth_rate(first_movers,v)) greater(zero,growth_rate(efficient_producers,v))* equal(growth_rate(efficient_producers,v),zero). % 0.21/0.47 16[0:Inp] || -> environment(sk1)*. % 0.21/0.47 17[0:Inp] || -> subpopulations(first_movers,efficient_producers,sk1,sk2)*. % 0.21/0.47 18[0:Inp] || -> greater_or_equal(sk2,equilibrium(sk1))*. % 0.21/0.47 19[0:Inp] || equal(growth_rate(efficient_producers,sk2),zero)** equal(growth_rate(first_movers,sk2),zero) -> . % 0.21/0.47 20[0:Inp] || greater(zero,growth_rate(efficient_producers,sk2)) greater(growth_rate(first_movers,sk2),zero)* -> . % 0.21/0.47 21[0:Inp] || greater(zero,growth_rate(first_movers,sk2)) greater(growth_rate(efficient_producers,sk2),zero)* -> . % 0.21/0.47 31[0:Res:16.0,5.0] || in_environment(sk1,u) greater(number_of_organizations(sk1,u),zero)* -> constant(resources(sk1,u)) greater(equilibrium(sk1),u). % 0.21/0.47 33[0:Res:16.0,7.0] || constant(resources(sk1,u))* in_environment(sk1,u) -> constant(number_of_organizations(sk1,u)). % 0.21/0.47 37[0:Res:18.0,3.1] environment(sk1) || greater(equilibrium(sk1),sk2)* -> . % 0.21/0.47 38[0:Res:17.0,15.1] environment(sk1) || constant(number_of_organizations(sk1,sk2)) -> equal(growth_rate(efficient_producers,sk2),zero) greater(zero,growth_rate(efficient_producers,sk2))* greater(zero,growth_rate(first_movers,sk2)). % 0.21/0.47 39[0:Res:17.0,14.1] environment(sk1) || constant(number_of_organizations(sk1,sk2)) -> equal(growth_rate(efficient_producers,sk2),zero) greater(zero,growth_rate(efficient_producers,sk2)) greater(growth_rate(efficient_producers,sk2),zero)*. % 0.21/0.47 40[0:Res:17.0,13.1] environment(sk1) || constant(number_of_organizations(sk1,sk2)) -> equal(growth_rate(efficient_producers,sk2),zero) greater(growth_rate(first_movers,sk2),zero)* greater(zero,growth_rate(first_movers,sk2)). % 0.21/0.47 41[0:Res:17.0,12.1] environment(sk1) || constant(number_of_organizations(sk1,sk2)) -> equal(growth_rate(efficient_producers,sk2),zero) greater(growth_rate(first_movers,sk2),zero) greater(growth_rate(efficient_producers,sk2),zero)*. % 0.21/0.47 43[0:Res:17.0,10.1] environment(sk1) || constant(number_of_organizations(sk1,sk2)) -> equal(growth_rate(first_movers,sk2),zero) greater(zero,growth_rate(efficient_producers,sk2)) greater(growth_rate(efficient_producers,sk2),zero)*. % 0.21/0.47 44[0:Res:17.0,9.1] environment(sk1) || constant(number_of_organizations(sk1,sk2)) -> equal(growth_rate(first_movers,sk2),zero) greater(growth_rate(first_movers,sk2),zero)* greater(zero,growth_rate(first_movers,sk2)). % 0.21/0.47 46[0:Res:17.0,2.1] environment(sk1) || -> greater(number_of_organizations(sk1,sk2),zero)*. % 0.21/0.47 47[0:Res:17.0,1.1] environment(sk1) || -> in_environment(sk1,sk2)*. % 0.21/0.47 48[0:MRR:47.0,16.0] || -> in_environment(sk1,sk2)*. % 0.21/0.47 49[0:MRR:37.0,16.0] || greater(equilibrium(sk1),sk2)* -> . % 0.21/0.47 50[0:MRR:46.0,16.0] || -> greater(number_of_organizations(sk1,sk2),zero)*. % 0.21/0.47 52[0:MRR:44.0,16.0] || constant(number_of_organizations(sk1,sk2)) -> greater(zero,growth_rate(first_movers,sk2)) greater(growth_rate(first_movers,sk2),zero)* equal(growth_rate(first_movers,sk2),zero). % 0.21/0.47 53[0:MRR:43.0,16.0] || constant(number_of_organizations(sk1,sk2)) -> greater(zero,growth_rate(efficient_producers,sk2)) greater(growth_rate(efficient_producers,sk2),zero)* equal(growth_rate(first_movers,sk2),zero). % 0.21/0.47 55[0:MRR:41.0,16.0] || constant(number_of_organizations(sk1,sk2)) -> greater(growth_rate(efficient_producers,sk2),zero)* greater(growth_rate(first_movers,sk2),zero) equal(growth_rate(efficient_producers,sk2),zero). % 0.21/0.47 56[0:MRR:40.0,16.0] || constant(number_of_organizations(sk1,sk2)) -> greater(zero,growth_rate(first_movers,sk2)) greater(growth_rate(first_movers,sk2),zero)* equal(growth_rate(efficient_producers,sk2),zero). % 0.21/0.47 57[0:MRR:39.0,16.0] || constant(number_of_organizations(sk1,sk2)) -> greater(zero,growth_rate(efficient_producers,sk2)) greater(growth_rate(efficient_producers,sk2),zero)* equal(growth_rate(efficient_producers,sk2),zero). % 0.21/0.47 58[0:MRR:38.0,16.0] || constant(number_of_organizations(sk1,sk2)) -> greater(zero,growth_rate(first_movers,sk2)) greater(zero,growth_rate(efficient_producers,sk2))* equal(growth_rate(efficient_producers,sk2),zero). % 0.21/0.47 59[1:Spt:55.3] || -> equal(growth_rate(efficient_producers,sk2),zero)**. % 0.21/0.47 61[1:Rew:59.0,53.2] || constant(number_of_organizations(sk1,sk2)) -> greater(zero,growth_rate(efficient_producers,sk2))* greater(zero,zero) equal(growth_rate(first_movers,sk2),zero). % 0.21/0.47 62[1:Rew:59.0,21.1] || greater(zero,growth_rate(first_movers,sk2))* greater(zero,zero) -> . % 0.21/0.47 64[1:Rew:59.0,20.0] || greater(zero,zero) greater(growth_rate(first_movers,sk2),zero)* -> . % 0.21/0.47 65[1:Rew:59.0,19.0] || equal(zero,zero) equal(growth_rate(first_movers,sk2),zero)** -> . % 0.21/0.47 66[1:Obv:65.0] || equal(growth_rate(first_movers,sk2),zero)** -> . % 0.21/0.47 67[1:MRR:52.3,66.0] || constant(number_of_organizations(sk1,sk2)) -> greater(zero,growth_rate(first_movers,sk2)) greater(growth_rate(first_movers,sk2),zero)*. % 0.21/0.47 69[1:Rew:59.0,61.1] || constant(number_of_organizations(sk1,sk2))* -> greater(zero,zero) greater(zero,zero) equal(growth_rate(first_movers,sk2),zero). % 0.21/0.47 70[1:Obv:69.1] || constant(number_of_organizations(sk1,sk2))* -> greater(zero,zero) equal(growth_rate(first_movers,sk2),zero). % 0.21/0.47 71[1:MRR:70.2,66.0] || constant(number_of_organizations(sk1,sk2))* -> greater(zero,zero). % 0.21/0.47 74[2:Spt:62.1] || greater(zero,zero)* -> . % 0.21/0.47 75[2:MRR:71.1,74.0] || constant(number_of_organizations(sk1,sk2))* -> . % 0.21/0.47 77[0:Res:50.0,31.1] || in_environment(sk1,sk2) -> constant(resources(sk1,sk2))* greater(equilibrium(sk1),sk2). % 0.21/0.47 80[0:MRR:77.0,77.2,48.0,49.0] || -> constant(resources(sk1,sk2))*. % 0.21/0.47 82[0:Res:80.0,33.0] || in_environment(sk1,sk2) -> constant(number_of_organizations(sk1,sk2))*. % 0.21/0.47 83[0:Res:80.0,7.1] environment(sk1) || in_environment(sk1,sk2) -> constant(number_of_organizations(sk1,sk2))*. % 0.21/0.47 85[0:SSi:83.0,16.0] || in_environment(sk1,sk2) -> constant(number_of_organizations(sk1,sk2))*. % 0.21/0.48 86[2:MRR:85.0,85.1,48.0,75.0] || -> . % 0.21/0.48 87[2:Spt:86.0,62.1,74.0] || -> greater(zero,zero)*. % 0.21/0.48 88[2:Spt:86.0,62.0] || greater(zero,growth_rate(first_movers,sk2))* -> . % 0.21/0.48 89[0:MRR:82.0,48.0] || -> constant(number_of_organizations(sk1,sk2))*. % 0.21/0.48 90[2:MRR:64.0,87.0] || greater(growth_rate(first_movers,sk2),zero)* -> . % 0.21/0.48 91[2:MRR:67.0,67.1,67.2,89.0,88.0,90.0] || -> . % 0.21/0.48 92[1:Spt:91.0,55.3,59.0] || equal(growth_rate(efficient_producers,sk2),zero)** -> . % 0.21/0.48 93[1:Spt:91.0,55.0,55.1,55.2] || constant(number_of_organizations(sk1,sk2)) -> greater(growth_rate(efficient_producers,sk2),zero)* greater(growth_rate(first_movers,sk2),zero). % 0.21/0.48 94[1:MRR:93.0,89.0] || -> greater(growth_rate(efficient_producers,sk2),zero)* greater(growth_rate(first_movers,sk2),zero). % 0.21/0.48 98[1:MRR:56.0,56.3,89.0,92.0] || -> greater(zero,growth_rate(first_movers,sk2)) greater(growth_rate(first_movers,sk2),zero)*. % 0.21/0.48 99[1:MRR:57.0,57.3,89.0,92.0] || -> greater(zero,growth_rate(efficient_producers,sk2)) greater(growth_rate(efficient_producers,sk2),zero)*. % 0.21/0.48 100[1:MRR:58.0,58.3,89.0,92.0] || -> greater(zero,growth_rate(first_movers,sk2)) greater(zero,growth_rate(efficient_producers,sk2))*. % 0.21/0.48 101[2:Spt:20.0] || greater(zero,growth_rate(efficient_producers,sk2))* -> . % 0.21/0.48 102[2:MRR:99.0,101.0] || -> greater(growth_rate(efficient_producers,sk2),zero)*. % 0.21/0.48 103[2:MRR:100.1,101.0] || -> greater(zero,growth_rate(first_movers,sk2))*. % 0.21/0.48 104[2:MRR:21.1,102.0] || greater(zero,growth_rate(first_movers,sk2))* -> . % 0.21/0.48 105[2:MRR:104.0,103.0] || -> . % 0.21/0.48 106[2:Spt:105.0,20.0,101.0] || -> greater(zero,growth_rate(efficient_producers,sk2))*. % 0.21/0.48 107[2:Spt:105.0,20.1] || greater(growth_rate(first_movers,sk2),zero)* -> . % 0.21/0.48 108[2:MRR:94.1,107.0] || -> greater(growth_rate(efficient_producers,sk2),zero)*. % 0.21/0.48 109[2:MRR:98.1,107.0] || -> greater(zero,growth_rate(first_movers,sk2))*. % 0.21/0.48 110[2:MRR:21.0,21.1,109.0,108.0] || -> . % 0.21/0.48 % SZS output end Refutation % 0.21/0.48 Formulae used in the proof : mp_time_point_occur_24 mp_positive_number_of_organizations_25 mp_equilibrium_26 a3_28 a6_30 l7_32 l7_33 l7_35 l7_36 l7_37 l7_38 prove_l6_39 prove_l6_40 prove_l6_41 prove_l6_42 prove_l6_43 prove_l6_44 % 0.21/0.48 %------------------------------------------------------------------------------