%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : MGT037+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n017.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 : Theorem 0.23s 0.48s
% Output : Refutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 24
% Syntax : Number of clauses : 102 ( 13 unt; 50 nHn; 102 RR)
% Number of literals : 369 ( 0 equ; 207 neg)
% Maximal clause size : 6 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
environment(skc3),
file('MGT037+1.p',unknown),
[] ).
cnf(2,axiom,
in_environment(skc3,skc2),
file('MGT037+1.p',unknown),
[] ).
cnf(3,axiom,
greater_or_equal(skc2,appear(efficient_producers,skc3)),
file('MGT037+1.p',unknown),
[] ).
cnf(4,axiom,
greater(resilience(efficient_producers),resilience(first_movers)),
file('MGT037+1.p',unknown),
[] ).
cnf(5,axiom,
~ greater(cardinality_at_time(efficient_producers,skc2),zero),
file('MGT037+1.p',unknown),
[] ).
cnf(6,axiom,
( ~ decreases(u)
| ~ constant(u) ),
file('MGT037+1.p',unknown),
[] ).
cnf(7,axiom,
greater(zero,growth_rate(efficient_producers,skf2(u,v))),
file('MGT037+1.p',unknown),
[] ).
cnf(9,axiom,
( ~ environment(u)
| ~ in_environment(u,v)
| subpopulation(efficient_producers,u,v) ),
file('MGT037+1.p',unknown),
[] ).
cnf(10,axiom,
( ~ greater(zero,growth_rate(u,v))
| ~ equal(cardinality_at_time(u,v),zero) ),
file('MGT037+1.p',unknown),
[] ).
cnf(11,axiom,
( ~ environment(u)
| ~ constant(resources(u,v))
| ~ in_environment(u,v)
| constant(number_of_organizations(u,v)) ),
file('MGT037+1.p',unknown),
[] ).
cnf(12,axiom,
( ~ environment(u)
| ~ in_environment(u,v)
| decreases(number_of_organizations(u,v))
| subpopulation(skf3(v,u),u,v) ),
file('MGT037+1.p',unknown),
[] ).
cnf(13,axiom,
( ~ environment(u)
| ~ in_environment(u,v)
| equal(cardinality_at_time(efficient_producers,v),zero)
| greater(cardinality_at_time(efficient_producers,v),zero) ),
file('MGT037+1.p',unknown),
[] ).
cnf(14,axiom,
( ~ environment(u)
| ~ in_environment(u,v)
| greater_or_equal(v,appear(an_organisation,u))
| greater(appear(an_organisation,u),v) ),
file('MGT037+1.p',unknown),
[] ).
cnf(15,axiom,
( ~ environment(u)
| ~ decreases(resources(u,v))
| ~ decreases(number_of_organizations(u,v))
| ~ in_environment(u,v) ),
file('MGT037+1.p',unknown),
[] ).
cnf(16,axiom,
( ~ environment(u)
| ~ in_environment(u,v)
| ~ greater(appear(an_organisation,u),v)
| equal(number_of_organizations(u,v),zero) ),
file('MGT037+1.p',unknown),
[] ).
cnf(17,axiom,
( ~ environment(u)
| ~ in_environment(u,v)
| decreases(number_of_organizations(u,v))
| greater(cardinality_at_time(skf3(v,w),v),zero) ),
file('MGT037+1.p',unknown),
[] ).
cnf(18,axiom,
( ~ environment(u)
| ~ in_environment(u,v)
| ~ greater_or_equal(v,appear(an_organisation,u))
| greater(number_of_organizations(u,v),zero) ),
file('MGT037+1.p',unknown),
[] ).
cnf(19,axiom,
( ~ environment(u)
| ~ in_environment(u,v)
| ~ greater(zero,growth_rate(skf3(v,w),v))
| decreases(number_of_organizations(u,v)) ),
file('MGT037+1.p',unknown),
[] ).
cnf(20,axiom,
( ~ environment(u)
| ~ greater(cardinality_at_time(v,w),zero)
| ~ subpopulation(v,u,w)
| equal(v,first_movers)
| equal(v,efficient_producers) ),
file('MGT037+1.p',unknown),
[] ).
cnf(22,axiom,
( ~ environment(u)
| ~ greater_or_equal(v,appear(efficient_producers,u))
| ~ equal(cardinality_at_time(efficient_producers,v),zero)
| in_environment(u,skf2(v,u)) ),
file('MGT037+1.p',unknown),
[] ).
cnf(23,axiom,
( ~ environment(u)
| ~ in_environment(u,v)
| ~ greater(number_of_organizations(u,v),zero)
| constant(resources(u,v))
| greater(equilibrium(u),v) ),
file('MGT037+1.p',unknown),
[] ).
cnf(24,axiom,
( ~ environment(u)
| ~ in_environment(u,v)
| ~ greater(equilibrium(u),v)
| ~ greater(number_of_organizations(u,v),zero)
| decreases(resources(u,v)) ),
file('MGT037+1.p',unknown),
[] ).
cnf(26,axiom,
( ~ environment(u)
| ~ in_environment(u,v)
| ~ equal(number_of_organizations(u,v),zero)
| ~ subpopulation(w,u,v)
| equal(cardinality_at_time(w,v),zero) ),
file('MGT037+1.p',unknown),
[] ).
cnf(27,axiom,
( ~ environment(u)
| ~ in_environment(u,v)
| ~ greater(zero,growth_rate(w,v))
| ~ greater(resilience(w),resilience(x))
| greater(zero,growth_rate(x,v)) ),
file('MGT037+1.p',unknown),
[] ).
cnf(28,plain,
( ~ in_environment(skc3,u)
| ~ greater(zero,growth_rate(v,u))
| ~ greater(resilience(v),resilience(w))
| greater(zero,growth_rate(w,u)) ),
inference(res,[status(thm),theory(equality)],[1,27]),
[iquote('0:Res:1.0,27.0')] ).
cnf(29,plain,
( ~ in_environment(skc3,u)
| ~ equal(number_of_organizations(skc3,u),zero)
| ~ subpopulation(v,skc3,u)
| equal(cardinality_at_time(v,u),zero) ),
inference(res,[status(thm),theory(equality)],[1,26]),
[iquote('0:Res:1.0,26.0')] ).
cnf(31,plain,
( ~ in_environment(skc3,u)
| ~ greater(equilibrium(skc3),u)
| ~ greater(number_of_organizations(skc3,u),zero)
| decreases(resources(skc3,u)) ),
inference(res,[status(thm),theory(equality)],[1,24]),
[iquote('0:Res:1.0,24.0')] ).
cnf(32,plain,
( ~ in_environment(skc3,u)
| ~ greater(number_of_organizations(skc3,u),zero)
| constant(resources(skc3,u))
| greater(equilibrium(skc3),u) ),
inference(res,[status(thm),theory(equality)],[1,23]),
[iquote('0:Res:1.0,23.0')] ).
cnf(33,plain,
( ~ greater_or_equal(u,appear(efficient_producers,skc3))
| ~ equal(cardinality_at_time(efficient_producers,u),zero)
| in_environment(skc3,skf2(u,skc3)) ),
inference(res,[status(thm),theory(equality)],[1,22]),
[iquote('0:Res:1.0,22.0')] ).
cnf(35,plain,
( ~ greater(cardinality_at_time(u,v),zero)
| ~ subpopulation(u,skc3,v)
| equal(u,first_movers)
| equal(u,efficient_producers) ),
inference(res,[status(thm),theory(equality)],[1,20]),
[iquote('0:Res:1.0,20.0')] ).
cnf(36,plain,
( ~ in_environment(skc3,u)
| ~ greater(zero,growth_rate(skf3(u,v),u))
| decreases(number_of_organizations(skc3,u)) ),
inference(res,[status(thm),theory(equality)],[1,19]),
[iquote('0:Res:1.0,19.0')] ).
cnf(37,plain,
( ~ in_environment(skc3,u)
| ~ greater(appear(an_organisation,skc3),u)
| equal(number_of_organizations(skc3,u),zero) ),
inference(res,[status(thm),theory(equality)],[1,16]),
[iquote('0:Res:1.0,16.0')] ).
cnf(38,plain,
( ~ in_environment(skc3,u)
| decreases(number_of_organizations(skc3,u))
| greater(cardinality_at_time(skf3(u,v),u),zero) ),
inference(res,[status(thm),theory(equality)],[1,17]),
[iquote('0:Res:1.0,17.0')] ).
cnf(39,plain,
( ~ greater_or_equal(u,appear(an_organisation,skc3))
| ~ in_environment(skc3,u)
| greater(number_of_organizations(skc3,u),zero) ),
inference(res,[status(thm),theory(equality)],[1,18]),
[iquote('0:Res:1.0,18.0')] ).
cnf(40,plain,
( ~ in_environment(skc3,u)
| decreases(number_of_organizations(skc3,u))
| subpopulation(skf3(u,skc3),skc3,u) ),
inference(res,[status(thm),theory(equality)],[1,12]),
[iquote('0:Res:1.0,12.0')] ).
cnf(42,plain,
( ~ in_environment(skc3,u)
| greater_or_equal(u,appear(an_organisation,skc3))
| greater(appear(an_organisation,skc3),u) ),
inference(res,[status(thm),theory(equality)],[1,14]),
[iquote('0:Res:1.0,14.0')] ).
cnf(43,plain,
( ~ decreases(resources(skc3,u))
| ~ decreases(number_of_organizations(skc3,u))
| ~ in_environment(skc3,u) ),
inference(res,[status(thm),theory(equality)],[1,15]),
[iquote('0:Res:1.0,15.0')] ).
cnf(44,plain,
( ~ constant(resources(skc3,u))
| ~ in_environment(skc3,u)
| constant(number_of_organizations(skc3,u)) ),
inference(res,[status(thm),theory(equality)],[1,11]),
[iquote('0:Res:1.0,11.0')] ).
cnf(46,plain,
( ~ in_environment(skc3,u)
| subpopulation(efficient_producers,skc3,u) ),
inference(res,[status(thm),theory(equality)],[1,9]),
[iquote('0:Res:1.0,9.0')] ).
cnf(55,plain,
( ~ environment(skc3)
| greater(cardinality_at_time(efficient_producers,skc2),zero)
| equal(cardinality_at_time(efficient_producers,skc2),zero) ),
inference(res,[status(thm),theory(equality)],[2,13]),
[iquote('0:Res:2.0,13.1')] ).
cnf(66,plain,
equal(cardinality_at_time(efficient_producers,skc2),zero),
inference(mrr,[status(thm)],[55,1,5]),
[iquote('0:MRR:55.0,55.1,1.0,5.0')] ).
cnf(67,plain,
~ greater(zero,zero),
inference(rew,[status(thm),theory(equality)],[66,5]),
[iquote('0:Rew:66.0,5.0')] ).
cnf(106,plain,
~ equal(cardinality_at_time(efficient_producers,skf2(u,v)),zero),
inference(res,[status(thm),theory(equality)],[7,10]),
[iquote('0:Res:7.0,10.0')] ).
cnf(111,plain,
( ~ in_environment(skc3,u)
| ~ in_environment(skc3,u)
| greater_or_equal(u,appear(an_organisation,skc3))
| equal(number_of_organizations(skc3,u),zero) ),
inference(res,[status(thm),theory(equality)],[42,37]),
[iquote('0:Res:42.2,37.1')] ).
cnf(112,plain,
( ~ in_environment(skc3,u)
| greater_or_equal(u,appear(an_organisation,skc3))
| equal(number_of_organizations(skc3,u),zero) ),
inference(obv,[status(thm),theory(equality)],[111]),
[iquote('0:Obv:111.0')] ).
cnf(130,plain,
( ~ in_environment(skc3,u)
| ~ subpopulation(skf3(u,v),skc3,u)
| decreases(number_of_organizations(skc3,u))
| equal(skf3(u,v),first_movers)
| equal(skf3(u,v),efficient_producers) ),
inference(res,[status(thm),theory(equality)],[38,35]),
[iquote('0:Res:38.2,35.0')] ).
cnf(134,plain,
( ~ greater_or_equal(u,appear(an_organisation,skc3))
| ~ in_environment(skc3,u)
| ~ in_environment(skc3,u)
| constant(resources(skc3,u))
| greater(equilibrium(skc3),u) ),
inference(res,[status(thm),theory(equality)],[39,32]),
[iquote('0:Res:39.2,32.1')] ).
cnf(135,plain,
( ~ greater_or_equal(u,appear(an_organisation,skc3))
| ~ in_environment(skc3,u)
| constant(resources(skc3,u))
| greater(equilibrium(skc3),u) ),
inference(obv,[status(thm),theory(equality)],[134]),
[iquote('0:Obv:134.1')] ).
cnf(143,plain,
( ~ in_environment(skc3,u)
| ~ in_environment(skc3,u)
| equal(number_of_organizations(skc3,u),zero)
| constant(resources(skc3,u))
| greater(equilibrium(skc3),u) ),
inference(res,[status(thm),theory(equality)],[112,135]),
[iquote('0:Res:112.1,135.0')] ).
cnf(145,plain,
( ~ in_environment(skc3,u)
| equal(number_of_organizations(skc3,u),zero)
| constant(resources(skc3,u))
| greater(equilibrium(skc3),u) ),
inference(obv,[status(thm),theory(equality)],[143]),
[iquote('0:Obv:143.0')] ).
cnf(149,plain,
( ~ in_environment(skc3,u)
| ~ in_environment(skc3,u)
| equal(number_of_organizations(skc3,u),zero)
| greater(equilibrium(skc3),u)
| constant(number_of_organizations(skc3,u)) ),
inference(res,[status(thm),theory(equality)],[145,44]),
[iquote('0:Res:145.2,44.0')] ).
cnf(151,plain,
( ~ in_environment(skc3,u)
| equal(number_of_organizations(skc3,u),zero)
| greater(equilibrium(skc3),u)
| constant(number_of_organizations(skc3,u)) ),
inference(obv,[status(thm),theory(equality)],[149]),
[iquote('0:Obv:149.0')] ).
cnf(164,plain,
( ~ greater_or_equal(u,appear(an_organisation,skc3))
| ~ in_environment(skc3,u)
| ~ in_environment(skc3,u)
| ~ greater(equilibrium(skc3),u)
| decreases(resources(skc3,u)) ),
inference(res,[status(thm),theory(equality)],[39,31]),
[iquote('0:Res:39.2,31.2')] ).
cnf(166,plain,
( ~ greater_or_equal(u,appear(an_organisation,skc3))
| ~ in_environment(skc3,u)
| ~ greater(equilibrium(skc3),u)
| decreases(resources(skc3,u)) ),
inference(obv,[status(thm),theory(equality)],[164]),
[iquote('0:Obv:164.1')] ).
cnf(168,plain,
( ~ environment(skc3)
| ~ in_environment(skc3,u)
| ~ greater(zero,growth_rate(skf3(u,v),u))
| ~ in_environment(skc3,u)
| greater(equilibrium(skc3),u)
| equal(number_of_organizations(skc3,u),zero) ),
inference(ems,[status(thm)],[6,19,151]),
[iquote('0:EmS:6.0,6.1,19.3,151.3')] ).
cnf(169,plain,
( ~ environment(skc3)
| ~ greater(zero,growth_rate(skf3(u,v),u))
| ~ in_environment(skc3,u)
| greater(equilibrium(skc3),u)
| equal(number_of_organizations(skc3,u),zero) ),
inference(obv,[status(thm),theory(equality)],[168]),
[iquote('0:Obv:168.1')] ).
cnf(170,plain,
( ~ greater(zero,growth_rate(skf3(u,v),u))
| ~ in_environment(skc3,u)
| greater(equilibrium(skc3),u)
| equal(number_of_organizations(skc3,u),zero) ),
inference(ssi,[status(thm)],[169,1]),
[iquote('0:SSi:169.0,1.0')] ).
cnf(171,plain,
( ~ in_environment(skc3,u)
| ~ in_environment(skc3,u)
| ~ greater(equilibrium(skc3),u)
| equal(number_of_organizations(skc3,u),zero)
| decreases(resources(skc3,u)) ),
inference(res,[status(thm),theory(equality)],[112,166]),
[iquote('0:Res:112.1,166.0')] ).
cnf(173,plain,
( ~ in_environment(skc3,u)
| ~ greater(equilibrium(skc3),u)
| equal(number_of_organizations(skc3,u),zero)
| decreases(resources(skc3,u)) ),
inference(obv,[status(thm),theory(equality)],[171]),
[iquote('0:Obv:171.0')] ).
cnf(178,plain,
( ~ in_environment(skc3,u)
| ~ greater(equilibrium(skc3),u)
| ~ decreases(number_of_organizations(skc3,u))
| ~ in_environment(skc3,u)
| equal(number_of_organizations(skc3,u),zero) ),
inference(res,[status(thm),theory(equality)],[173,43]),
[iquote('0:Res:173.3,43.0')] ).
cnf(180,plain,
( ~ greater(equilibrium(skc3),u)
| ~ decreases(number_of_organizations(skc3,u))
| ~ in_environment(skc3,u)
| equal(number_of_organizations(skc3,u),zero) ),
inference(obv,[status(thm),theory(equality)],[178]),
[iquote('0:Obv:178.0')] ).
cnf(185,plain,
( ~ in_environment(skc3,u)
| ~ in_environment(skc3,u)
| ~ equal(number_of_organizations(skc3,u),zero)
| equal(cardinality_at_time(efficient_producers,u),zero) ),
inference(res,[status(thm),theory(equality)],[46,29]),
[iquote('0:Res:46.1,29.2')] ).
cnf(187,plain,
( ~ in_environment(skc3,u)
| ~ in_environment(skc3,u)
| ~ equal(number_of_organizations(skc3,u),zero)
| decreases(number_of_organizations(skc3,u))
| equal(cardinality_at_time(skf3(u,skc3),u),zero) ),
inference(res,[status(thm),theory(equality)],[40,29]),
[iquote('0:Res:40.2,29.2')] ).
cnf(191,plain,
( ~ in_environment(skc3,u)
| ~ equal(number_of_organizations(skc3,u),zero)
| equal(cardinality_at_time(efficient_producers,u),zero) ),
inference(obv,[status(thm),theory(equality)],[185]),
[iquote('0:Obv:185.0')] ).
cnf(195,plain,
( ~ in_environment(skc3,u)
| ~ equal(number_of_organizations(skc3,u),zero)
| decreases(number_of_organizations(skc3,u))
| equal(cardinality_at_time(skf3(u,skc3),u),zero) ),
inference(obv,[status(thm),theory(equality)],[187]),
[iquote('0:Obv:187.0')] ).
cnf(216,plain,
( ~ in_environment(skc3,u)
| ~ equal(number_of_organizations(skc3,u),zero)
| ~ in_environment(skc3,u)
| decreases(number_of_organizations(skc3,u))
| decreases(number_of_organizations(skc3,u))
| greater(zero,zero) ),
inference(spr,[status(thm),theory(equality)],[195,38]),
[iquote('0:SpR:195.3,38.2')] ).
cnf(220,plain,
( ~ equal(number_of_organizations(skc3,u),zero)
| ~ in_environment(skc3,u)
| decreases(number_of_organizations(skc3,u))
| greater(zero,zero) ),
inference(obv,[status(thm),theory(equality)],[216]),
[iquote('0:Obv:216.3')] ).
cnf(221,plain,
( ~ equal(number_of_organizations(skc3,u),zero)
| ~ in_environment(skc3,u)
| decreases(number_of_organizations(skc3,u)) ),
inference(mrr,[status(thm)],[220,67]),
[iquote('0:MRR:220.3,67.0')] ).
cnf(225,plain,
( ~ in_environment(skc3,skf2(u,v))
| ~ greater(resilience(efficient_producers),resilience(w))
| greater(zero,growth_rate(w,skf2(u,v))) ),
inference(res,[status(thm),theory(equality)],[7,28]),
[iquote('0:Res:7.0,28.1')] ).
cnf(233,plain,
( ~ in_environment(skc3,skf2(u,v))
| ~ greater(resilience(efficient_producers),resilience(skf3(skf2(u,v),w)))
| ~ in_environment(skc3,skf2(u,v))
| decreases(number_of_organizations(skc3,skf2(u,v))) ),
inference(res,[status(thm),theory(equality)],[225,36]),
[iquote('0:Res:225.2,36.1')] ).
cnf(236,plain,
( ~ greater(resilience(efficient_producers),resilience(skf3(skf2(u,v),w)))
| ~ in_environment(skc3,skf2(u,v))
| decreases(number_of_organizations(skc3,skf2(u,v))) ),
inference(obv,[status(thm),theory(equality)],[233]),
[iquote('0:Obv:233.0')] ).
cnf(383,plain,
( ~ in_environment(skc3,u)
| ~ in_environment(skc3,u)
| decreases(number_of_organizations(skc3,u))
| decreases(number_of_organizations(skc3,u))
| equal(skf3(u,skc3),first_movers)
| equal(skf3(u,skc3),efficient_producers) ),
inference(res,[status(thm),theory(equality)],[40,130]),
[iquote('0:Res:40.2,130.1')] ).
cnf(385,plain,
( ~ in_environment(skc3,u)
| decreases(number_of_organizations(skc3,u))
| equal(skf3(u,skc3),first_movers)
| equal(skf3(u,skc3),efficient_producers) ),
inference(obv,[status(thm),theory(equality)],[383]),
[iquote('0:Obv:383.2')] ).
cnf(388,plain,
( ~ in_environment(skc3,u)
| ~ in_environment(skc3,u)
| equal(skf3(u,skc3),first_movers)
| equal(skf3(u,skc3),efficient_producers)
| greater(equilibrium(skc3),u)
| equal(number_of_organizations(skc3,u),zero) ),
inference(ems,[status(thm)],[6,385,151]),
[iquote('0:EmS:6.0,6.1,385.1,151.3')] ).
cnf(390,plain,
( ~ in_environment(skc3,u)
| ~ greater(equilibrium(skc3),u)
| ~ in_environment(skc3,u)
| equal(skf3(u,skc3),first_movers)
| equal(skf3(u,skc3),efficient_producers)
| equal(number_of_organizations(skc3,u),zero) ),
inference(res,[status(thm),theory(equality)],[385,180]),
[iquote('0:Res:385.1,180.1')] ).
cnf(392,plain,
( ~ in_environment(skc3,u)
| equal(skf3(u,skc3),first_movers)
| equal(skf3(u,skc3),efficient_producers)
| greater(equilibrium(skc3),u)
| equal(number_of_organizations(skc3,u),zero) ),
inference(obv,[status(thm),theory(equality)],[388]),
[iquote('0:Obv:388.0')] ).
cnf(393,plain,
( ~ greater(equilibrium(skc3),u)
| ~ in_environment(skc3,u)
| equal(skf3(u,skc3),first_movers)
| equal(skf3(u,skc3),efficient_producers)
| equal(number_of_organizations(skc3,u),zero) ),
inference(obv,[status(thm),theory(equality)],[390]),
[iquote('0:Obv:390.0')] ).
cnf(394,plain,
( ~ in_environment(skc3,u)
| equal(skf3(u,skc3),first_movers)
| equal(skf3(u,skc3),efficient_producers)
| equal(number_of_organizations(skc3,u),zero) ),
inference(mrr,[status(thm)],[393,392]),
[iquote('0:MRR:393.0,392.3')] ).
cnf(411,plain,
( ~ in_environment(skc3,skf2(u,v))
| ~ greater(resilience(efficient_producers),resilience(first_movers))
| ~ in_environment(skc3,skf2(u,v))
| equal(skf3(skf2(u,v),skc3),efficient_producers)
| equal(number_of_organizations(skc3,skf2(u,v)),zero)
| decreases(number_of_organizations(skc3,skf2(u,v))) ),
inference(spl,[status(thm),theory(equality)],[394,236]),
[iquote('0:SpL:394.1,236.0')] ).
cnf(424,plain,
( ~ greater(resilience(efficient_producers),resilience(first_movers))
| ~ in_environment(skc3,skf2(u,v))
| equal(skf3(skf2(u,v),skc3),efficient_producers)
| equal(number_of_organizations(skc3,skf2(u,v)),zero)
| decreases(number_of_organizations(skc3,skf2(u,v))) ),
inference(obv,[status(thm),theory(equality)],[411]),
[iquote('0:Obv:411.0')] ).
cnf(425,plain,
( ~ in_environment(skc3,skf2(u,v))
| equal(skf3(skf2(u,v),skc3),efficient_producers)
| decreases(number_of_organizations(skc3,skf2(u,v))) ),
inference(mrr,[status(thm)],[424,4,221]),
[iquote('0:MRR:424.0,424.3,4.0,221.0')] ).
cnf(540,plain,
( ~ in_environment(skc3,skf2(u,v))
| ~ in_environment(skc3,skf2(u,v))
| equal(skf3(skf2(u,v),skc3),efficient_producers)
| greater(equilibrium(skc3),skf2(u,v))
| equal(number_of_organizations(skc3,skf2(u,v)),zero) ),
inference(ems,[status(thm)],[6,425,151]),
[iquote('0:EmS:6.0,6.1,425.2,151.3')] ).
cnf(541,plain,
( ~ in_environment(skc3,skf2(u,v))
| ~ greater(equilibrium(skc3),skf2(u,v))
| ~ in_environment(skc3,skf2(u,v))
| equal(skf3(skf2(u,v),skc3),efficient_producers)
| equal(number_of_organizations(skc3,skf2(u,v)),zero) ),
inference(res,[status(thm),theory(equality)],[425,180]),
[iquote('0:Res:425.2,180.1')] ).
cnf(543,plain,
( ~ in_environment(skc3,skf2(u,v))
| equal(skf3(skf2(u,v),skc3),efficient_producers)
| greater(equilibrium(skc3),skf2(u,v))
| equal(number_of_organizations(skc3,skf2(u,v)),zero) ),
inference(obv,[status(thm),theory(equality)],[540]),
[iquote('0:Obv:540.0')] ).
cnf(544,plain,
( ~ greater(equilibrium(skc3),skf2(u,v))
| ~ in_environment(skc3,skf2(u,v))
| equal(skf3(skf2(u,v),skc3),efficient_producers)
| equal(number_of_organizations(skc3,skf2(u,v)),zero) ),
inference(obv,[status(thm),theory(equality)],[541]),
[iquote('0:Obv:541.0')] ).
cnf(545,plain,
( ~ in_environment(skc3,skf2(u,v))
| equal(skf3(skf2(u,v),skc3),efficient_producers)
| equal(number_of_organizations(skc3,skf2(u,v)),zero) ),
inference(mrr,[status(thm)],[544,543]),
[iquote('0:MRR:544.0,543.2')] ).
cnf(557,plain,
( ~ in_environment(skc3,skf2(u,v))
| ~ greater(zero,growth_rate(efficient_producers,skf2(u,v)))
| ~ in_environment(skc3,skf2(u,v))
| equal(number_of_organizations(skc3,skf2(u,v)),zero)
| greater(equilibrium(skc3),skf2(u,v))
| equal(number_of_organizations(skc3,skf2(u,v)),zero) ),
inference(spl,[status(thm),theory(equality)],[545,170]),
[iquote('0:SpL:545.1,170.0')] ).
cnf(558,plain,
( ~ in_environment(skc3,skf2(u,v))
| ~ in_environment(skc3,skf2(u,v))
| ~ greater(zero,growth_rate(efficient_producers,skf2(u,v)))
| equal(number_of_organizations(skc3,skf2(u,v)),zero)
| decreases(number_of_organizations(skc3,skf2(u,v))) ),
inference(spl,[status(thm),theory(equality)],[545,36]),
[iquote('0:SpL:545.1,36.1')] ).
cnf(572,plain,
( ~ in_environment(skc3,skf2(u,v))
| ~ greater(zero,growth_rate(efficient_producers,skf2(u,v)))
| equal(number_of_organizations(skc3,skf2(u,v)),zero)
| decreases(number_of_organizations(skc3,skf2(u,v))) ),
inference(obv,[status(thm),theory(equality)],[558]),
[iquote('0:Obv:558.0')] ).
cnf(573,plain,
( ~ in_environment(skc3,skf2(u,v))
| decreases(number_of_organizations(skc3,skf2(u,v))) ),
inference(mrr,[status(thm)],[572,7,221]),
[iquote('0:MRR:572.1,572.2,7.0,221.0')] ).
cnf(578,plain,
( ~ greater(zero,growth_rate(efficient_producers,skf2(u,v)))
| ~ in_environment(skc3,skf2(u,v))
| greater(equilibrium(skc3),skf2(u,v))
| equal(number_of_organizations(skc3,skf2(u,v)),zero) ),
inference(obv,[status(thm),theory(equality)],[557]),
[iquote('0:Obv:557.3')] ).
cnf(579,plain,
( ~ in_environment(skc3,skf2(u,v))
| greater(equilibrium(skc3),skf2(u,v))
| equal(number_of_organizations(skc3,skf2(u,v)),zero) ),
inference(mrr,[status(thm)],[578,7]),
[iquote('0:MRR:578.0,7.0')] ).
cnf(585,plain,
( ~ in_environment(skc3,skf2(u,v))
| ~ greater(equilibrium(skc3),skf2(u,v))
| ~ in_environment(skc3,skf2(u,v))
| equal(number_of_organizations(skc3,skf2(u,v)),zero) ),
inference(res,[status(thm),theory(equality)],[573,180]),
[iquote('0:Res:573.1,180.1')] ).
cnf(588,plain,
( ~ greater(equilibrium(skc3),skf2(u,v))
| ~ in_environment(skc3,skf2(u,v))
| equal(number_of_organizations(skc3,skf2(u,v)),zero) ),
inference(obv,[status(thm),theory(equality)],[585]),
[iquote('0:Obv:585.0')] ).
cnf(589,plain,
( ~ in_environment(skc3,skf2(u,v))
| equal(number_of_organizations(skc3,skf2(u,v)),zero) ),
inference(mrr,[status(thm)],[588,579]),
[iquote('0:MRR:588.0,579.1')] ).
cnf(606,plain,
( ~ in_environment(skc3,skf2(u,v))
| ~ in_environment(skc3,skf2(u,v))
| ~ equal(zero,zero)
| equal(cardinality_at_time(efficient_producers,skf2(u,v)),zero) ),
inference(spl,[status(thm),theory(equality)],[589,191]),
[iquote('0:SpL:589.1,191.1')] ).
cnf(612,plain,
( ~ in_environment(skc3,skf2(u,v))
| equal(cardinality_at_time(efficient_producers,skf2(u,v)),zero) ),
inference(obv,[status(thm),theory(equality)],[606]),
[iquote('0:Obv:606.2')] ).
cnf(613,plain,
~ in_environment(skc3,skf2(u,v)),
inference(mrr,[status(thm)],[612,106]),
[iquote('0:MRR:612.1,106.0')] ).
cnf(614,plain,
( ~ greater_or_equal(u,appear(efficient_producers,skc3))
| ~ equal(cardinality_at_time(efficient_producers,u),zero) ),
inference(mrr,[status(thm)],[33,613]),
[iquote('0:MRR:33.2,613.0')] ).
cnf(626,plain,
~ equal(cardinality_at_time(efficient_producers,skc2),zero),
inference(res,[status(thm),theory(equality)],[3,614]),
[iquote('0:Res:3.0,614.0')] ).
cnf(627,plain,
~ equal(zero,zero),
inference(rew,[status(thm),theory(equality)],[66,626]),
[iquote('0:Rew:66.0,626.0')] ).
cnf(628,plain,
$false,
inference(obv,[status(thm),theory(equality)],[627]),
[iquote('0:Obv:627.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT037+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : run_spass %d %s
% 0.09/0.36 % Computer : n017.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 7 12:38:09 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.23/0.48
% 0.23/0.48 SPASS V 3.9
% 0.23/0.48 SPASS beiseite: Proof found.
% 0.23/0.48 % SZS status Theorem
% 0.23/0.48 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.23/0.48 SPASS derived 372 clauses, backtracked 6 clauses, performed 2 splits and kept 199 clauses.
% 0.23/0.48 SPASS allocated 98225 KBytes.
% 0.23/0.48 SPASS spent 0:00:00.12 on the problem.
% 0.23/0.48 0:00:00.03 for the input.
% 0.23/0.48 0:00:00.02 for the FLOTTER CNF translation.
% 0.23/0.48 0:00:00.01 for inferences.
% 0.23/0.48 0:00:00.00 for the backtracking.
% 0.23/0.48 0:00:00.03 for the reduction.
% 0.23/0.48
% 0.23/0.48
% 0.23/0.48 Here is a proof with depth 10, length 102 :
% 0.23/0.48 % SZS output start Refutation
% See solution above
% 0.23/0.49 Formulae used in the proof : prove_t6 a2 mp_constant_not_decrease mp_previous_negative_growth mp_efficient_producers_exist mp_subpopulations mp_empty_not_decreasing a6 mp_non_decreasing mp_environment_inequality mp_start_of_organizations a1 a9 a3 mp_no_members a12
% 0.23/0.49
%------------------------------------------------------------------------------