%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT037-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n008.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:53 AM UTC 2026 % Result : Unsatisfiable 0.46s 0.79s % Output : Refutation 0.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : MGT037-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.06 % Command : run_spass %d %s % 0.15/0.41 % Computer : n008.cluster.edu % 0.15/0.41 % Model : x86_64 x86_64 % 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.41 % Memory : 8046.5625MB % 0.15/0.41 % OS : Linux 6.8.0-71-generic % 0.15/0.41 % CPULimit : 300 % 0.15/0.41 % WCLimit : 300 % 0.15/0.41 % DateTime : Mon Sep 7 12:44:38 UTC 2026 % 0.15/0.41 % CPUTime : % 0.46/0.79 % 0.46/0.79 SPASS V 3.9 % 0.46/0.79 SPASS beiseite: Proof found. % 0.46/0.79 % SZS status Theorem % 0.46/0.79 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.46/0.79 SPASS derived 607 clauses, backtracked 30 clauses, performed 5 splits and kept 281 clauses. % 0.46/0.79 SPASS allocated 76598 KBytes. % 0.46/0.79 SPASS spent 0:00:00.36 on the problem. % 0.46/0.79 0:00:00.09 for the input. % 0.46/0.79 0:00:00.00 for the FLOTTER CNF translation. % 0.46/0.79 0:00:00.04 for inferences. % 0.46/0.79 0:00:00.00 for the backtracking. % 0.46/0.79 0:00:00.16 for the reduction. % 0.46/0.79 % 0.46/0.79 % 0.46/0.79 Here is a proof with depth 14, length 181 : % 0.46/0.79 % SZS output start Refutation % 0.46/0.79 2[0:Inp] environment(u) || greater_or_equal(v,appear(efficient_producers,u)) equal(cardinality_at_time(efficient_producers,v),zero) -> in_environment(u,sk1(v,u))*. % 0.46/0.79 4[0:Inp] environment(u) || greater_or_equal(v,appear(efficient_producers,u)) equal(cardinality_at_time(efficient_producers,v),zero) -> greater(zero,growth_rate(efficient_producers,sk1(v,u)))*. % 0.46/0.79 5[0:Inp] environment(u) || in_environment(u,v) greater(appear(an_organisation,u),v)* -> equal(number_of_organizations(u,v),zero). % 0.46/0.79 6[0:Inp] environment(u) || in_environment(u,v) -> decreases(number_of_organizations(u,v)) subpopulation(sk2(v,u),u,v)*. % 0.46/0.79 7[0:Inp] environment(u) || in_environment(u,v) -> decreases(number_of_organizations(u,v)) greater(cardinality_at_time(sk2(v,u),v),zero)*. % 0.46/0.79 8[0:Inp] environment(u) || in_environment(u,v) greater(zero,growth_rate(sk2(v,u),v))* -> decreases(number_of_organizations(u,v)). % 0.46/0.79 9[0:Inp] environment(u) || in_environment(u,v) equal(number_of_organizations(u,v),zero) subpopulation(w,u,v)* -> equal(cardinality_at_time(w,v),zero). % 0.46/0.79 10[0:Inp] environment(u) || in_environment(u,v) -> subpopulation(first_movers,u,v)*. % 0.46/0.79 11[0:Inp] environment(u) || in_environment(u,v) -> subpopulation(efficient_producers,u,v)*. % 0.46/0.79 12[0:Inp] || greater(zero,growth_rate(u,v))* equal(cardinality_at_time(u,v),zero) -> . % 0.46/0.79 13[0:Inp] environment(u) || in_environment(u,v)*+ -> greater(cardinality_at_time(efficient_producers,v),zero)* equal(cardinality_at_time(efficient_producers,v),zero). % 0.46/0.79 14[0:Inp] decreases(u) constant(u) || -> . % 0.46/0.79 15[0:Inp] environment(u) || in_environment(u,v) -> greater_or_equal(v,appear(an_organisation,u)) greater(appear(an_organisation,u),v)*. % 0.46/0.79 16[0:Inp] environment(u) || in_environment(u,v) greater(equilibrium(u),v) greater(number_of_organizations(u,v),zero)* -> decreases(resources(u,v)). % 0.46/0.79 17[0:Inp] environment(u) || in_environment(u,v) greater(number_of_organizations(u,v),zero)* -> constant(resources(u,v)) greater(equilibrium(u),v). % 0.46/0.79 18[0:Inp] environment(u) || in_environment(u,v) greater_or_equal(v,appear(an_organisation,u)) -> greater(number_of_organizations(u,v),zero)*. % 0.46/0.79 19[0:Inp] environment(u) || decreases(number_of_organizations(u,v)) decreases(resources(u,v))* in_environment(u,v) -> . % 0.46/0.79 20[0:Inp] environment(u) || constant(resources(u,v))* in_environment(u,v) -> constant(number_of_organizations(u,v)). % 0.46/0.79 21[0:Inp] environment(u) || in_environment(u,v)* greater(zero,growth_rate(w,v))*+ greater(resilience(w),resilience(x))* -> greater(zero,growth_rate(x,v))*. % 0.46/0.79 22[0:Inp] || -> greater(resilience(efficient_producers),resilience(first_movers))*. % 0.46/0.79 23[0:Inp] environment(u) || greater(cardinality_at_time(v,w),zero)*+ subpopulation(v,u,w)* -> equal(v,first_movers) equal(v,efficient_producers). % 0.46/0.79 24[0:Inp] || -> environment(sk3)*. % 0.46/0.79 25[0:Inp] || -> in_environment(sk3,sk4)*. % 0.46/0.79 26[0:Inp] || -> greater_or_equal(sk4,appear(efficient_producers,sk3))*. % 0.46/0.79 27[0:Inp] || greater(cardinality_at_time(efficient_producers,sk4),zero)* -> . % 0.46/0.79 28[0:Res:24.0,21.0] || in_environment(sk3,u) greater(zero,growth_rate(v,u))*+ greater(resilience(v),resilience(w))* -> greater(zero,growth_rate(w,u))*. % 0.46/0.79 29[0:Res:24.0,9.0] || in_environment(sk3,u) equal(number_of_organizations(sk3,u),zero) subpopulation(v,sk3,u)* -> equal(cardinality_at_time(v,u),zero). % 0.46/0.79 30[0:Res:24.0,16.0] || in_environment(sk3,u) greater(equilibrium(sk3),u) greater(number_of_organizations(sk3,u),zero)* -> decreases(resources(sk3,u)). % 0.46/0.79 31[0:Res:24.0,4.0] || greater_or_equal(u,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,u),zero) -> greater(zero,growth_rate(efficient_producers,sk1(u,sk3)))*. % 0.46/0.79 33[0:Res:24.0,17.0] || in_environment(sk3,u) greater(number_of_organizations(sk3,u),zero)* -> constant(resources(sk3,u)) greater(equilibrium(sk3),u). % 0.46/0.79 34[0:Res:24.0,23.0] || greater(cardinality_at_time(u,v),zero)* subpopulation(u,sk3,v) -> equal(u,first_movers) equal(u,efficient_producers). % 0.46/0.79 36[0:Res:24.0,2.0] || greater_or_equal(u,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,u),zero) -> in_environment(sk3,sk1(u,sk3))*. % 0.46/0.79 37[0:Res:24.0,8.0] || in_environment(sk3,u) greater(zero,growth_rate(sk2(u,sk3),u))* -> decreases(number_of_organizations(sk3,u)). % 0.46/0.79 38[0:Res:24.0,5.0] || in_environment(sk3,u) greater(appear(an_organisation,sk3),u)* -> equal(number_of_organizations(sk3,u),zero). % 0.46/0.79 39[0:Res:24.0,7.0] || in_environment(sk3,u) -> decreases(number_of_organizations(sk3,u)) greater(cardinality_at_time(sk2(u,sk3),u),zero)*. % 0.46/0.79 40[0:Res:24.0,18.0] || greater_or_equal(u,appear(an_organisation,sk3)) in_environment(sk3,u) -> greater(number_of_organizations(sk3,u),zero)*. % 0.46/0.79 41[0:Res:24.0,6.0] || in_environment(sk3,u) -> decreases(number_of_organizations(sk3,u)) subpopulation(sk2(u,sk3),sk3,u)*. % 0.46/0.79 43[0:Res:24.0,15.0] || in_environment(sk3,u) -> greater_or_equal(u,appear(an_organisation,sk3)) greater(appear(an_organisation,sk3),u)*. % 0.46/0.79 44[0:Res:24.0,19.0] || decreases(number_of_organizations(sk3,u)) decreases(resources(sk3,u))* in_environment(sk3,u) -> . % 0.46/0.79 45[0:Res:24.0,20.0] || constant(resources(sk3,u))* in_environment(sk3,u) -> constant(number_of_organizations(sk3,u)). % 0.46/0.79 46[0:Res:24.0,10.0] || in_environment(sk3,u) -> subpopulation(first_movers,sk3,u)*. % 0.46/0.79 47[0:Res:24.0,11.0] || in_environment(sk3,u) -> subpopulation(efficient_producers,sk3,u)*. % 0.46/0.79 57[0:Res:25.0,13.1] environment(sk3) || -> equal(cardinality_at_time(efficient_producers,sk4),zero) greater(cardinality_at_time(efficient_producers,sk4),zero)*. % 0.46/0.79 67[0:MRR:57.0,57.2,24.0,27.0] || -> equal(cardinality_at_time(efficient_producers,sk4),zero)**. % 0.46/0.79 68[0:Rew:67.0,27.0] || greater(zero,zero)* -> . % 0.46/0.79 111[0:Res:43.2,38.1] || in_environment(sk3,u) in_environment(sk3,u) -> greater_or_equal(u,appear(an_organisation,sk3))* equal(number_of_organizations(sk3,u),zero). % 0.46/0.79 112[0:Obv:111.0] || in_environment(sk3,u) -> greater_or_equal(u,appear(an_organisation,sk3))* equal(number_of_organizations(sk3,u),zero). % 0.46/0.79 129[0:Res:39.2,34.0] || in_environment(sk3,u) subpopulation(sk2(u,sk3),sk3,u)* -> decreases(number_of_organizations(sk3,u)) equal(sk2(u,sk3),first_movers) equal(sk2(u,sk3),efficient_producers). % 0.46/0.79 130[0:MRR:129.1,41.2] || in_environment(sk3,u) -> decreases(number_of_organizations(sk3,u))* equal(sk2(u,sk3),first_movers) equal(sk2(u,sk3),efficient_producers). % 0.46/0.79 134[0:Res:40.2,33.1] || greater_or_equal(u,appear(an_organisation,sk3))* in_environment(sk3,u) in_environment(sk3,u) -> constant(resources(sk3,u)) greater(equilibrium(sk3),u). % 0.46/0.79 135[0:Obv:134.1] || greater_or_equal(u,appear(an_organisation,sk3))* in_environment(sk3,u) -> constant(resources(sk3,u)) greater(equilibrium(sk3),u). % 0.46/0.79 137[0:Res:112.1,135.0] || in_environment(sk3,u) in_environment(sk3,u) -> equal(number_of_organizations(sk3,u),zero) constant(resources(sk3,u))* greater(equilibrium(sk3),u). % 0.46/0.79 138[0:Obv:137.0] || in_environment(sk3,u) -> equal(number_of_organizations(sk3,u),zero) constant(resources(sk3,u))* greater(equilibrium(sk3),u). % 0.46/0.79 142[0:Res:15.3,5.2] environment(u) environment(u) || in_environment(u,v) in_environment(u,v) -> greater_or_equal(v,appear(an_organisation,u))* equal(number_of_organizations(u,v),zero). % 0.46/0.79 145[0:Obv:142.2] environment(u) || in_environment(u,v) -> greater_or_equal(v,appear(an_organisation,u))* equal(number_of_organizations(u,v),zero). % 0.46/0.79 147[0:Res:138.2,45.0] || in_environment(sk3,u) in_environment(sk3,u) -> equal(number_of_organizations(sk3,u),zero) greater(equilibrium(sk3),u) constant(number_of_organizations(sk3,u))*. % 0.46/0.79 149[0:Obv:147.0] || in_environment(sk3,u) -> equal(number_of_organizations(sk3,u),zero) greater(equilibrium(sk3),u) constant(number_of_organizations(sk3,u))*. % 0.46/0.79 151[0:EmS:14.0,14.1,130.1,149.3] || in_environment(sk3,u) in_environment(sk3,u) -> equal(sk2(u,sk3),first_movers) equal(sk2(u,sk3),efficient_producers) greater(equilibrium(sk3),u)* equal(number_of_organizations(sk3,u),zero). % 0.46/0.79 153[0:Obv:151.0] || in_environment(sk3,u) -> equal(sk2(u,sk3),first_movers) equal(sk2(u,sk3),efficient_producers) greater(equilibrium(sk3),u)* equal(number_of_organizations(sk3,u),zero). % 0.46/0.79 159[0:Res:31.2,12.0] || greater_or_equal(u,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,u),zero) equal(cardinality_at_time(efficient_producers,sk1(u,sk3)),zero)** -> . % 0.46/0.79 161[0:Res:40.2,30.2] || greater_or_equal(u,appear(an_organisation,sk3))* in_environment(sk3,u) in_environment(sk3,u) greater(equilibrium(sk3),u) -> decreases(resources(sk3,u)). % 0.46/0.79 163[0:Obv:161.1] || greater_or_equal(u,appear(an_organisation,sk3))* in_environment(sk3,u) greater(equilibrium(sk3),u) -> decreases(resources(sk3,u)). % 0.46/0.79 165[0:Res:112.1,163.0] || in_environment(sk3,u) in_environment(sk3,u) greater(equilibrium(sk3),u) -> equal(number_of_organizations(sk3,u),zero) decreases(resources(sk3,u))*. % 0.46/0.79 167[0:Obv:165.0] || in_environment(sk3,u) greater(equilibrium(sk3),u) -> equal(number_of_organizations(sk3,u),zero) decreases(resources(sk3,u))*. % 0.46/0.79 172[0:Res:167.3,44.1] || in_environment(sk3,u) greater(equilibrium(sk3),u) decreases(number_of_organizations(sk3,u))* in_environment(sk3,u) -> equal(number_of_organizations(sk3,u),zero). % 0.46/0.79 174[0:Obv:172.0] || greater(equilibrium(sk3),u) decreases(number_of_organizations(sk3,u))* in_environment(sk3,u) -> equal(number_of_organizations(sk3,u),zero). % 0.46/0.79 177[0:Res:130.1,174.1] || in_environment(sk3,u) greater(equilibrium(sk3),u)* in_environment(sk3,u) -> equal(sk2(u,sk3),first_movers) equal(sk2(u,sk3),efficient_producers) equal(number_of_organizations(sk3,u),zero). % 0.46/0.79 178[0:Obv:177.0] || greater(equilibrium(sk3),u)* in_environment(sk3,u) -> equal(sk2(u,sk3),first_movers) equal(sk2(u,sk3),efficient_producers) equal(number_of_organizations(sk3,u),zero). % 0.46/0.79 179[0:MRR:178.0,153.3] || in_environment(sk3,u) -> equal(sk2(u,sk3),first_movers)** equal(sk2(u,sk3),efficient_producers) equal(number_of_organizations(sk3,u),zero). % 0.46/0.79 187[0:SpL:179.1,37.1] || in_environment(sk3,u) in_environment(sk3,u) greater(zero,growth_rate(first_movers,u))* -> equal(sk2(u,sk3),efficient_producers) equal(number_of_organizations(sk3,u),zero) decreases(number_of_organizations(sk3,u)). % 0.46/0.79 191[0:Obv:187.0] || in_environment(sk3,u) greater(zero,growth_rate(first_movers,u))* -> equal(sk2(u,sk3),efficient_producers) equal(number_of_organizations(sk3,u),zero) decreases(number_of_organizations(sk3,u)). % 0.46/0.79 213[0:Res:47.1,29.2] || in_environment(sk3,u) in_environment(sk3,u) equal(number_of_organizations(sk3,u),zero)** -> equal(cardinality_at_time(efficient_producers,u),zero). % 0.46/0.79 214[0:Res:46.1,29.2] || in_environment(sk3,u) in_environment(sk3,u) equal(number_of_organizations(sk3,u),zero)** -> equal(cardinality_at_time(first_movers,u),zero). % 0.46/0.79 215[0:Res:41.2,29.2] || in_environment(sk3,u) in_environment(sk3,u) equal(number_of_organizations(sk3,u),zero) -> decreases(number_of_organizations(sk3,u)) equal(cardinality_at_time(sk2(u,sk3),u),zero)**. % 0.46/0.79 219[0:Obv:213.0] || in_environment(sk3,u) equal(number_of_organizations(sk3,u),zero)** -> equal(cardinality_at_time(efficient_producers,u),zero). % 0.46/0.79 220[0:Obv:214.0] || in_environment(sk3,u) equal(number_of_organizations(sk3,u),zero)** -> equal(cardinality_at_time(first_movers,u),zero). % 0.46/0.79 223[0:Obv:215.0] || in_environment(sk3,u) equal(number_of_organizations(sk3,u),zero) -> decreases(number_of_organizations(sk3,u)) equal(cardinality_at_time(sk2(u,sk3),u),zero)**. % 0.46/0.79 235[0:Res:7.3,23.1] environment(u) environment(v) || in_environment(u,w) subpopulation(sk2(w,u),v,w)* -> decreases(number_of_organizations(u,w)) equal(sk2(w,u),first_movers) equal(sk2(w,u),efficient_producers). % 0.46/0.79 237[0:SpR:223.3,39.2] || in_environment(sk3,u) equal(number_of_organizations(sk3,u),zero) in_environment(sk3,u) -> decreases(number_of_organizations(sk3,u))* decreases(number_of_organizations(sk3,u))* greater(zero,zero). % 0.46/0.79 244[0:Obv:237.3] || equal(number_of_organizations(sk3,u),zero) in_environment(sk3,u) -> decreases(number_of_organizations(sk3,u))* greater(zero,zero). % 0.46/0.79 245[0:MRR:244.3,68.0] || equal(number_of_organizations(sk3,u),zero) in_environment(sk3,u) -> decreases(number_of_organizations(sk3,u))*. % 0.46/0.79 250[0:Res:31.2,28.1] || greater_or_equal(u,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,u),zero) in_environment(sk3,sk1(u,sk3)) greater(resilience(efficient_producers),resilience(v)) -> greater(zero,growth_rate(v,sk1(u,sk3)))*. % 0.46/0.79 251[0:MRR:250.2,36.2] || greater_or_equal(u,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,u),zero) greater(resilience(efficient_producers),resilience(v)) -> greater(zero,growth_rate(v,sk1(u,sk3)))*. % 0.46/0.79 254[0:Res:18.3,17.2] environment(u) environment(u) || in_environment(u,v) greater_or_equal(v,appear(an_organisation,u))* in_environment(u,v) -> constant(resources(u,v)) greater(equilibrium(u),v). % 0.46/0.79 256[0:Obv:254.2] environment(u) || greater_or_equal(v,appear(an_organisation,u))* in_environment(u,v) -> constant(resources(u,v)) greater(equilibrium(u),v). % 0.46/0.79 258[0:Res:145.2,256.1] environment(u) environment(u) || in_environment(u,v) in_environment(u,v) -> equal(number_of_organizations(u,v),zero) constant(resources(u,v))* greater(equilibrium(u),v). % 0.46/0.79 260[0:Obv:258.2] environment(u) || in_environment(u,v) -> equal(number_of_organizations(u,v),zero) constant(resources(u,v))* greater(equilibrium(u),v). % 0.46/0.79 265[0:Res:260.3,20.1] environment(u) environment(u) || in_environment(u,v) in_environment(u,v) -> equal(number_of_organizations(u,v),zero) greater(equilibrium(u),v) constant(number_of_organizations(u,v))*. % 0.46/0.79 267[0:Obv:265.2] environment(u) || in_environment(u,v) -> equal(number_of_organizations(u,v),zero) greater(equilibrium(u),v) constant(number_of_organizations(u,v))*. % 0.46/0.79 277[0:Res:18.3,16.3] environment(u) environment(u) || in_environment(u,v) greater_or_equal(v,appear(an_organisation,u))* in_environment(u,v) greater(equilibrium(u),v) -> decreases(resources(u,v)). % 0.46/0.79 279[0:Obv:277.2] environment(u) || greater_or_equal(v,appear(an_organisation,u))* in_environment(u,v) greater(equilibrium(u),v) -> decreases(resources(u,v)). % 0.46/0.79 281[0:Res:145.2,279.1] environment(u) environment(u) || in_environment(u,v) in_environment(u,v) greater(equilibrium(u),v) -> equal(number_of_organizations(u,v),zero) decreases(resources(u,v))*. % 0.46/0.79 283[0:Obv:281.2] environment(u) || in_environment(u,v) greater(equilibrium(u),v) -> equal(number_of_organizations(u,v),zero) decreases(resources(u,v))*. % 0.46/0.79 289[0:Res:283.4,19.2] environment(u) environment(u) || in_environment(u,v) greater(equilibrium(u),v) decreases(number_of_organizations(u,v))* in_environment(u,v) -> equal(number_of_organizations(u,v),zero). % 0.46/0.79 291[0:Obv:289.2] environment(u) || greater(equilibrium(u),v) decreases(number_of_organizations(u,v))* in_environment(u,v) -> equal(number_of_organizations(u,v),zero). % 0.46/0.79 299[0:Res:6.3,9.3] environment(u) environment(u) || in_environment(u,v) in_environment(u,v) equal(number_of_organizations(u,v),zero) -> decreases(number_of_organizations(u,v)) equal(cardinality_at_time(sk2(v,u),v),zero)**. % 0.46/0.79 305[0:Obv:299.2] environment(u) || in_environment(u,v) equal(number_of_organizations(u,v),zero) -> decreases(number_of_organizations(u,v)) equal(cardinality_at_time(sk2(v,u),v),zero)**. % 0.46/0.79 322[0:SpR:305.4,7.3] environment(u) environment(u) || in_environment(u,v) equal(number_of_organizations(u,v),zero) in_environment(u,v) -> decreases(number_of_organizations(u,v))* decreases(number_of_organizations(u,v))* greater(zero,zero). % 0.46/0.79 329[0:Obv:322.5] environment(u) || equal(number_of_organizations(u,v),zero) in_environment(u,v) -> decreases(number_of_organizations(u,v))* greater(zero,zero). % 0.46/0.79 330[0:MRR:329.4,68.0] environment(u) || equal(number_of_organizations(u,v),zero) in_environment(u,v) -> decreases(number_of_organizations(u,v))*. % 0.46/0.79 356[0:Res:251.3,12.0] || greater_or_equal(u,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,u),zero) greater(resilience(efficient_producers),resilience(v)) equal(cardinality_at_time(v,sk1(u,sk3)),zero)** -> . % 0.46/0.79 359[0:Res:251.3,28.1] || greater_or_equal(u,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,u),zero) greater(resilience(efficient_producers),resilience(v))* in_environment(sk3,sk1(u,sk3)) greater(resilience(v),resilience(w))* -> greater(zero,growth_rate(w,sk1(u,sk3)))*. % 0.46/0.79 364[0:MRR:359.3,36.2] || greater_or_equal(u,appear(efficient_producers,sk3))+ equal(cardinality_at_time(efficient_producers,u),zero) greater(resilience(efficient_producers),resilience(v))* greater(resilience(v),resilience(w))* -> greater(zero,growth_rate(w,sk1(u,sk3)))*. % 0.46/0.79 369[0:Res:6.3,235.3] environment(u) environment(u) environment(u) || in_environment(u,v) in_environment(u,v) -> decreases(number_of_organizations(u,v))* decreases(number_of_organizations(u,v))* equal(sk2(v,u),first_movers) equal(sk2(v,u),efficient_producers). % 0.46/0.79 372[0:Obv:369.5] environment(u) || in_environment(u,v) -> decreases(number_of_organizations(u,v))* equal(sk2(v,u),first_movers) equal(sk2(v,u),efficient_producers). % 0.46/0.79 375[0:EmS:14.0,14.1,372.2,267.4] environment(u) environment(u) || in_environment(u,v) in_environment(u,v) -> equal(sk2(v,u),first_movers) equal(sk2(v,u),efficient_producers) greater(equilibrium(u),v)* equal(number_of_organizations(u,v),zero). % 0.46/0.79 379[0:Res:372.2,291.2] environment(u) environment(u) || in_environment(u,v) greater(equilibrium(u),v)* in_environment(u,v) -> equal(sk2(v,u),first_movers) equal(sk2(v,u),efficient_producers) equal(number_of_organizations(u,v),zero). % 0.46/0.79 382[0:Obv:375.2] environment(u) || in_environment(u,v) -> equal(sk2(v,u),first_movers) equal(sk2(v,u),efficient_producers) greater(equilibrium(u),v)* equal(number_of_organizations(u,v),zero). % 0.46/0.79 383[0:Obv:379.2] environment(u) || greater(equilibrium(u),v)* in_environment(u,v) -> equal(sk2(v,u),first_movers) equal(sk2(v,u),efficient_producers) equal(number_of_organizations(u,v),zero). % 0.46/0.79 384[0:MRR:383.1,382.4] environment(u) || in_environment(u,v) -> equal(sk2(v,u),first_movers)** equal(sk2(v,u),efficient_producers) equal(number_of_organizations(u,v),zero). % 0.46/0.79 395[0:SpL:384.2,8.2] environment(u) environment(u) || in_environment(u,v) in_environment(u,v) greater(zero,growth_rate(first_movers,v))* -> equal(sk2(v,u),efficient_producers) equal(number_of_organizations(u,v),zero) decreases(number_of_organizations(u,v))*. % 0.46/0.79 402[0:Obv:395.2] environment(u) || in_environment(u,v) greater(zero,growth_rate(first_movers,v))* -> equal(sk2(v,u),efficient_producers) equal(number_of_organizations(u,v),zero) decreases(number_of_organizations(u,v))*. % 0.46/0.79 403[0:MRR:402.4,330.1] environment(u) || in_environment(u,v) greater(zero,growth_rate(first_movers,v))*+ -> equal(sk2(v,u),efficient_producers) decreases(number_of_organizations(u,v))*. % 0.46/0.79 485[0:EmS:14.0,14.1,403.4,149.3] environment(sk3) || in_environment(sk3,u) greater(zero,growth_rate(first_movers,u))* in_environment(sk3,u) -> equal(sk2(u,sk3),efficient_producers) greater(equilibrium(sk3),u) equal(number_of_organizations(sk3,u),zero). % 0.46/0.79 486[0:Res:251.3,403.2] environment(u) || greater_or_equal(v,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,v),zero) greater(resilience(efficient_producers),resilience(first_movers)) in_environment(u,sk1(v,sk3)) -> equal(sk2(sk1(v,sk3),u),efficient_producers) decreases(number_of_organizations(u,sk1(v,sk3)))*. % 0.46/0.79 487[0:Obv:485.1] environment(sk3) || greater(zero,growth_rate(first_movers,u))* in_environment(sk3,u) -> equal(sk2(u,sk3),efficient_producers) greater(equilibrium(sk3),u) equal(number_of_organizations(sk3,u),zero). % 0.46/0.79 488[0:SSi:487.0,24.0] || greater(zero,growth_rate(first_movers,u))* in_environment(sk3,u) -> equal(sk2(u,sk3),efficient_producers) greater(equilibrium(sk3),u) equal(number_of_organizations(sk3,u),zero). % 0.46/0.79 490[0:MRR:486.3,22.0] environment(u) || greater_or_equal(v,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,v),zero) in_environment(u,sk1(v,sk3)) -> equal(sk2(sk1(v,sk3),u),efficient_producers) decreases(number_of_organizations(u,sk1(v,sk3)))*. % 0.46/0.79 499[0:Res:251.3,488.0] || greater_or_equal(u,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,u),zero) greater(resilience(efficient_producers),resilience(first_movers)) in_environment(sk3,sk1(u,sk3)) -> equal(sk2(sk1(u,sk3),sk3),efficient_producers) greater(equilibrium(sk3),sk1(u,sk3))* equal(number_of_organizations(sk3,sk1(u,sk3)),zero). % 0.46/0.79 500[0:MRR:499.2,499.3,22.0,36.2] || greater_or_equal(u,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,u),zero) -> equal(sk2(sk1(u,sk3),sk3),efficient_producers) greater(equilibrium(sk3),sk1(u,sk3))* equal(number_of_organizations(sk3,sk1(u,sk3)),zero). % 0.46/0.79 610[0:Res:26.0,364.0] || equal(cardinality_at_time(efficient_producers,sk4),zero) greater(resilience(efficient_producers),resilience(u))* greater(resilience(u),resilience(v))* -> greater(zero,growth_rate(v,sk1(sk4,sk3)))*. % 0.46/0.79 611[0:Rew:67.0,610.0] || equal(zero,zero) greater(resilience(efficient_producers),resilience(u))* greater(resilience(u),resilience(v))* -> greater(zero,growth_rate(v,sk1(sk4,sk3)))*. % 0.46/0.79 612[0:Obv:611.0] || greater(resilience(efficient_producers),resilience(u))*+ greater(resilience(u),resilience(v))* -> greater(zero,growth_rate(v,sk1(sk4,sk3)))*. % 0.46/0.79 613[0:Res:22.0,612.0] || greater(resilience(first_movers),resilience(u)) -> greater(zero,growth_rate(u,sk1(sk4,sk3)))*. % 0.46/0.79 619[0:Res:613.1,191.1] || greater(resilience(first_movers),resilience(first_movers)) in_environment(sk3,sk1(sk4,sk3)) -> equal(sk2(sk1(sk4,sk3),sk3),efficient_producers) equal(number_of_organizations(sk3,sk1(sk4,sk3)),zero) decreases(number_of_organizations(sk3,sk1(sk4,sk3)))*. % 0.46/0.79 623[0:MRR:619.3,245.0] || greater(resilience(first_movers),resilience(first_movers)) in_environment(sk3,sk1(sk4,sk3)) -> equal(sk2(sk1(sk4,sk3),sk3),efficient_producers) decreases(number_of_organizations(sk3,sk1(sk4,sk3)))*. % 0.46/0.79 643[1:Spt:623.2] || -> equal(sk2(sk1(sk4,sk3),sk3),efficient_producers)**. % 0.46/0.79 646[1:SpR:643.0,39.2] || in_environment(sk3,sk1(sk4,sk3)) -> decreases(number_of_organizations(sk3,sk1(sk4,sk3))) greater(cardinality_at_time(efficient_producers,sk1(sk4,sk3)),zero)*. % 0.46/0.79 652[1:SpL:643.0,37.1] || in_environment(sk3,sk1(sk4,sk3)) greater(zero,growth_rate(efficient_producers,sk1(sk4,sk3)))* -> decreases(number_of_organizations(sk3,sk1(sk4,sk3))). % 0.46/0.79 683[2:Spt:646.1] || -> decreases(number_of_organizations(sk3,sk1(sk4,sk3)))*. % 0.46/0.79 685[2:EmS:14.0,14.1,683.0,149.3] || in_environment(sk3,sk1(sk4,sk3)) -> greater(equilibrium(sk3),sk1(sk4,sk3))* equal(number_of_organizations(sk3,sk1(sk4,sk3)),zero). % 0.46/0.79 686[2:Res:683.0,174.1] || greater(equilibrium(sk3),sk1(sk4,sk3))* in_environment(sk3,sk1(sk4,sk3)) -> equal(number_of_organizations(sk3,sk1(sk4,sk3)),zero). % 0.46/0.79 688[2:MRR:686.0,685.1] || in_environment(sk3,sk1(sk4,sk3)) -> equal(number_of_organizations(sk3,sk1(sk4,sk3)),zero)**. % 0.46/0.79 699[2:SpL:688.1,219.1] || in_environment(sk3,sk1(sk4,sk3)) in_environment(sk3,sk1(sk4,sk3)) equal(zero,zero) -> equal(cardinality_at_time(efficient_producers,sk1(sk4,sk3)),zero)**. % 0.46/0.79 704[2:Obv:699.2] || in_environment(sk3,sk1(sk4,sk3)) -> equal(cardinality_at_time(efficient_producers,sk1(sk4,sk3)),zero)**. % 0.46/0.79 721[2:SpL:704.1,159.2] || in_environment(sk3,sk1(sk4,sk3))* greater_or_equal(sk4,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,sk4),zero) equal(zero,zero) -> . % 0.46/0.79 727[2:Obv:721.3] || in_environment(sk3,sk1(sk4,sk3))* greater_or_equal(sk4,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,sk4),zero) -> . % 0.46/0.79 728[2:Rew:67.0,727.2] || in_environment(sk3,sk1(sk4,sk3))* greater_or_equal(sk4,appear(efficient_producers,sk3)) equal(zero,zero) -> . % 0.46/0.79 729[2:Obv:728.2] || in_environment(sk3,sk1(sk4,sk3))* greater_or_equal(sk4,appear(efficient_producers,sk3)) -> . % 0.46/0.79 730[2:MRR:729.1,26.0] || in_environment(sk3,sk1(sk4,sk3))* -> . % 0.46/0.79 735[2:Res:2.3,730.0] environment(sk3) || greater_or_equal(sk4,appear(efficient_producers,sk3))* equal(cardinality_at_time(efficient_producers,sk4),zero) -> . % 0.46/0.79 739[2:Rew:67.0,735.2] environment(sk3) || greater_or_equal(sk4,appear(efficient_producers,sk3))* equal(zero,zero) -> . % 0.46/0.79 740[2:Obv:739.2] environment(sk3) || greater_or_equal(sk4,appear(efficient_producers,sk3))* -> . % 0.46/0.79 741[2:SSi:740.0,24.0] || greater_or_equal(sk4,appear(efficient_producers,sk3))* -> . % 0.46/0.79 742[2:MRR:741.0,26.0] || -> . % 0.46/0.79 743[2:Spt:742.0,646.1,683.0] || decreases(number_of_organizations(sk3,sk1(sk4,sk3)))* -> . % 0.56/0.82 744[2:Spt:742.0,646.0,646.2] || in_environment(sk3,sk1(sk4,sk3)) -> greater(cardinality_at_time(efficient_producers,sk1(sk4,sk3)),zero)*. % 0.56/0.82 746[2:MRR:652.2,743.0] || in_environment(sk3,sk1(sk4,sk3)) greater(zero,growth_rate(efficient_producers,sk1(sk4,sk3)))* -> . % 0.56/0.82 751[2:Res:31.2,746.1] || greater_or_equal(sk4,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,sk4),zero) in_environment(sk3,sk1(sk4,sk3))* -> . % 0.56/0.82 756[2:Rew:67.0,751.1] || greater_or_equal(sk4,appear(efficient_producers,sk3)) equal(zero,zero) in_environment(sk3,sk1(sk4,sk3))* -> . % 0.56/0.82 757[2:Obv:756.1] || greater_or_equal(sk4,appear(efficient_producers,sk3)) in_environment(sk3,sk1(sk4,sk3))* -> . % 0.56/0.82 758[2:MRR:757.0,26.0] || in_environment(sk3,sk1(sk4,sk3))* -> . % 0.56/0.82 762[2:Res:2.3,758.0] environment(sk3) || greater_or_equal(sk4,appear(efficient_producers,sk3))* equal(cardinality_at_time(efficient_producers,sk4),zero) -> . % 0.56/0.82 766[2:Rew:67.0,762.2] environment(sk3) || greater_or_equal(sk4,appear(efficient_producers,sk3))* equal(zero,zero) -> . % 0.56/0.82 767[2:Obv:766.2] environment(sk3) || greater_or_equal(sk4,appear(efficient_producers,sk3))* -> . % 0.56/0.82 768[2:SSi:767.0,24.0] || greater_or_equal(sk4,appear(efficient_producers,sk3))* -> . % 0.56/0.82 769[2:MRR:768.0,26.0] || -> . % 0.56/0.82 770[1:Spt:769.0,623.2,643.0] || equal(sk2(sk1(sk4,sk3),sk3),efficient_producers)** -> . % 0.56/0.82 771[1:Spt:769.0,623.0,623.1,623.3] || greater(resilience(first_movers),resilience(first_movers)) in_environment(sk3,sk1(sk4,sk3)) -> decreases(number_of_organizations(sk3,sk1(sk4,sk3)))*. % 0.56/0.82 962[0:Res:490.5,174.1] environment(sk3) || greater_or_equal(u,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,u),zero) in_environment(sk3,sk1(u,sk3)) greater(equilibrium(sk3),sk1(u,sk3))* in_environment(sk3,sk1(u,sk3)) -> equal(sk2(sk1(u,sk3),sk3),efficient_producers) equal(number_of_organizations(sk3,sk1(u,sk3)),zero). % 0.56/0.82 965[0:Obv:962.3] environment(sk3) || greater_or_equal(u,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,u),zero) greater(equilibrium(sk3),sk1(u,sk3))* in_environment(sk3,sk1(u,sk3)) -> equal(sk2(sk1(u,sk3),sk3),efficient_producers) equal(number_of_organizations(sk3,sk1(u,sk3)),zero). % 0.56/0.82 966[0:SSi:965.0,24.0] || greater_or_equal(u,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,u),zero) greater(equilibrium(sk3),sk1(u,sk3))* in_environment(sk3,sk1(u,sk3)) -> equal(sk2(sk1(u,sk3),sk3),efficient_producers) equal(number_of_organizations(sk3,sk1(u,sk3)),zero). % 0.56/0.82 967[0:MRR:966.3,36.2] || greater_or_equal(u,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,u),zero) greater(equilibrium(sk3),sk1(u,sk3))* -> equal(sk2(sk1(u,sk3),sk3),efficient_producers) equal(number_of_organizations(sk3,sk1(u,sk3)),zero). % 0.56/0.82 968[0:MRR:967.2,500.3] || greater_or_equal(u,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,u),zero) -> equal(sk2(sk1(u,sk3),sk3),efficient_producers)** equal(number_of_organizations(sk3,sk1(u,sk3)),zero). % 0.56/0.82 1003[1:SpL:968.2,770.0] || greater_or_equal(sk4,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,sk4),zero) equal(efficient_producers,efficient_producers) -> equal(number_of_organizations(sk3,sk1(sk4,sk3)),zero)**. % 0.56/0.82 1007[1:Obv:1003.2] || greater_or_equal(sk4,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,sk4),zero) -> equal(number_of_organizations(sk3,sk1(sk4,sk3)),zero)**. % 0.56/0.82 1008[1:Rew:67.0,1007.1] || greater_or_equal(sk4,appear(efficient_producers,sk3)) equal(zero,zero) -> equal(number_of_organizations(sk3,sk1(sk4,sk3)),zero)**. % 0.56/0.82 1009[1:Obv:1008.1] || greater_or_equal(sk4,appear(efficient_producers,sk3)) -> equal(number_of_organizations(sk3,sk1(sk4,sk3)),zero)**. % 0.56/0.82 1010[1:MRR:1009.0,26.0] || -> equal(number_of_organizations(sk3,sk1(sk4,sk3)),zero)**. % 0.56/0.82 1025[1:SpL:1010.0,220.1] || in_environment(sk3,sk1(sk4,sk3)) equal(zero,zero) -> equal(cardinality_at_time(first_movers,sk1(sk4,sk3)),zero)**. % 0.56/0.82 1031[1:Obv:1025.1] || in_environment(sk3,sk1(sk4,sk3)) -> equal(cardinality_at_time(first_movers,sk1(sk4,sk3)),zero)**. % 0.56/0.82 1040[1:SpL:1031.1,356.3] || in_environment(sk3,sk1(sk4,sk3)) greater_or_equal(sk4,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,sk4),zero) greater(resilience(efficient_producers),resilience(first_movers))* equal(zero,zero) -> . % 0.56/0.82 1044[1:Obv:1040.4] || in_environment(sk3,sk1(sk4,sk3)) greater_or_equal(sk4,appear(efficient_producers,sk3)) equal(cardinality_at_time(efficient_producers,sk4),zero) greater(resilience(efficient_producers),resilience(first_movers))* -> . % 0.56/0.82 1045[1:Rew:67.0,1044.2] || in_environment(sk3,sk1(sk4,sk3)) greater_or_equal(sk4,appear(efficient_producers,sk3)) equal(zero,zero) greater(resilience(efficient_producers),resilience(first_movers))* -> . % 0.56/0.82 1046[1:Obv:1045.2] || in_environment(sk3,sk1(sk4,sk3)) greater_or_equal(sk4,appear(efficient_producers,sk3)) greater(resilience(efficient_producers),resilience(first_movers))* -> . % 0.56/0.82 1047[1:MRR:1046.1,1046.2,26.0,22.0] || in_environment(sk3,sk1(sk4,sk3))* -> . % 0.56/0.82 1052[1:Res:2.3,1047.0] environment(sk3) || greater_or_equal(sk4,appear(efficient_producers,sk3))* equal(cardinality_at_time(efficient_producers,sk4),zero) -> . % 0.56/0.82 1056[1:Rew:67.0,1052.2] environment(sk3) || greater_or_equal(sk4,appear(efficient_producers,sk3))* equal(zero,zero) -> . % 0.56/0.82 1057[1:Obv:1056.2] environment(sk3) || greater_or_equal(sk4,appear(efficient_producers,sk3))* -> . % 0.56/0.82 1058[1:SSi:1057.0,24.0] || greater_or_equal(sk4,appear(efficient_producers,sk3))* -> . % 0.56/0.82 1059[1:MRR:1058.0,26.0] || -> . % 0.56/0.82 % SZS output end Refutation % 0.56/0.82 Formulae used in the proof : mp_previous_negative_growth_29 mp_previous_negative_growth_31 mp_start_of_organizations_32 mp_non_decreasing_33 mp_non_decreasing_34 mp_non_decreasing_35 mp_no_members_36 mp_subpopulations_37 mp_subpopulations_38 mp_empty_not_decreasing_39 mp_efficient_producers_exist_40 mp_constant_not_decrease_41 mp_environment_inequality_42 a3_43 a3_44 a1_45 a6_46 a6_47 a12_48 a2_49 a9_50 prove_t6_51 prove_t6_52 prove_t6_53 prove_t6_54 % 0.56/0.82 %------------------------------------------------------------------------------