%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT025-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n028.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.22s 0.53s % Output : Refutation 0.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT025-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.11/0.37 % Computer : n028.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Mon Sep 7 12:13:02 UTC 2026 % 0.11/0.37 % CPUTime : % 0.22/0.53 % 0.22/0.53 SPASS V 3.9 % 0.22/0.53 SPASS beiseite: Proof found. % 0.22/0.53 % SZS status Theorem % 0.22/0.53 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.22/0.53 SPASS derived 256 clauses, backtracked 118 clauses, performed 10 splits and kept 259 clauses. % 0.22/0.53 SPASS allocated 75944 KBytes. % 0.22/0.53 SPASS spent 0:00:00.15 on the problem. % 0.22/0.53 0:00:00.06 for the input. % 0.22/0.53 0:00:00.00 for the FLOTTER CNF translation. % 0.22/0.53 0:00:00.01 for inferences. % 0.22/0.53 0:00:00.00 for the backtracking. % 0.22/0.53 0:00:00.04 for the reduction. % 0.22/0.53 % 0.22/0.53 % 0.22/0.53 Here is a proof with depth 9, length 169 : % 0.22/0.53 % SZS output start Refutation % 0.22/0.53 3[0:Inp] environment(u) || equal(v,first_movers) subpopulation(v,u,w)*+ -> equal(number_of_organizations(u,w),sum__dfg(cardinality_at_time(first_movers,w),cardinality_at_time(efficient_producers,w)))*. % 0.22/0.53 4[0:Inp] environment(u) || in_environment(u,v) -> subpopulation(first_movers,u,v)*. % 0.22/0.53 5[0:Inp] environment(u) || in_environment(u,v) -> subpopulation(efficient_producers,u,v)*. % 0.22/0.53 6[0:Inp] constant(u) || equal(u,sum__dfg(v,w))* -> decreases(v) increases(v) constant(v). % 0.22/0.53 7[0:Inp] constant(u) || equal(u,sum__dfg(v,w))* -> increases(w) increases(v) constant(v). % 0.22/0.53 8[0:Inp] constant(u) || equal(u,sum__dfg(v,w))* -> decreases(v) decreases(w) constant(v). % 0.22/0.53 9[0:Inp] constant(u) || equal(u,sum__dfg(v,w))* -> increases(w) decreases(w) constant(v). % 0.22/0.53 10[0:Inp] constant(u) || equal(u,sum__dfg(v,w))* -> decreases(v) increases(v) constant(w). % 0.22/0.53 11[0:Inp] constant(u) || equal(u,sum__dfg(v,w))* -> increases(w) increases(v) constant(w). % 0.22/0.53 12[0:Inp] constant(u) || equal(u,sum__dfg(v,w))* -> decreases(v) decreases(w) constant(w). % 0.22/0.53 13[0:Inp] constant(u) || equal(u,sum__dfg(v,w))* -> increases(w) decreases(w) constant(w). % 0.22/0.53 14[0:Inp] environment(u) || constant(cardinality_at_time(v,w)) in_environment(u,w) greater(cardinality_at_time(v,w),zero)*+ subpopulation(v,u,w)* -> equal(growth_rate(v,w),zero). % 0.22/0.53 15[0:Inp] environment(u) || increases(cardinality_at_time(v,w)) in_environment(u,w) greater(cardinality_at_time(v,w),zero)+ subpopulation(v,u,w)* -> greater(growth_rate(v,w),zero)*. % 0.22/0.53 16[0:Inp] environment(u) || decreases(cardinality_at_time(v,w)) in_environment(u,w) greater(cardinality_at_time(v,w),zero)*+ subpopulation(v,u,w)* -> greater(zero,growth_rate(v,w)). % 0.22/0.53 17[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v)*+ -> greater(cardinality_at_time(first_movers,v),zero)*. % 0.22/0.53 18[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v)*+ -> greater(cardinality_at_time(efficient_producers,v),zero)*. % 0.22/0.53 19[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v)* -> in_environment(u,v). % 0.22/0.53 21[0:Inp] || -> environment(sk1)*. % 0.22/0.53 22[0:Inp] || -> subpopulations(first_movers,efficient_producers,sk1,sk2)*. % 0.22/0.53 23[0:Inp] || -> constant(number_of_organizations(sk1,sk2))*. % 0.22/0.53 24[0:Inp] || equal(growth_rate(efficient_producers,sk2),zero)** equal(growth_rate(first_movers,sk2),zero) -> . % 0.22/0.53 25[0:Inp] || greater(zero,growth_rate(efficient_producers,sk2)) greater(growth_rate(first_movers,sk2),zero)* -> . % 0.22/0.53 26[0:Inp] || greater(zero,growth_rate(first_movers,sk2)) greater(growth_rate(efficient_producers,sk2),zero)* -> . % 0.22/0.53 28[0:Res:21.0,15.0] || increases(cardinality_at_time(u,v)) in_environment(sk1,v) greater(cardinality_at_time(u,v),zero) subpopulation(u,sk1,v) -> greater(growth_rate(u,v),zero)*. % 0.22/0.53 31[0:Res:21.0,3.0] || equal(u,first_movers) subpopulation(u,sk1,v)*+ -> equal(sum__dfg(cardinality_at_time(first_movers,v),cardinality_at_time(efficient_producers,v)),number_of_organizations(sk1,v))**. % 0.22/0.53 37[0:Res:21.0,4.0] || in_environment(sk1,u) -> subpopulation(first_movers,sk1,u)*. % 0.22/0.53 47[0:Res:22.0,17.1] environment(sk1) || -> greater(cardinality_at_time(first_movers,sk2),zero)*. % 0.22/0.53 48[0:Res:22.0,18.1] environment(sk1) || -> greater(cardinality_at_time(efficient_producers,sk2),zero)*. % 0.22/0.53 49[0:Res:22.0,19.1] environment(sk1) || -> in_environment(sk1,sk2)*. % 0.22/0.53 50[0:MRR:49.0,21.0] || -> in_environment(sk1,sk2)*. % 0.22/0.53 51[0:MRR:47.0,21.0] || -> greater(cardinality_at_time(first_movers,sk2),zero)*. % 0.22/0.53 52[0:MRR:48.0,21.0] || -> greater(cardinality_at_time(efficient_producers,sk2),zero)*. % 0.22/0.53 60[0:EqR:13.1] constant(sum__dfg(u,v)) || -> increases(v)* decreases(v) constant(v). % 0.22/0.53 61[0:EqR:6.1] constant(sum__dfg(u,v)) || -> decreases(u) increases(u)* constant(u). % 0.22/0.53 62[0:EqR:10.1] constant(sum__dfg(u,v)) || -> decreases(u) increases(u)* constant(v)*. % 0.22/0.53 63[0:EqR:9.1] constant(sum__dfg(u,v)) || -> increases(v)* decreases(v) constant(u)*. % 0.22/0.53 64[0:EqR:12.1] constant(sum__dfg(u,v)) || -> decreases(u)* decreases(v)* constant(v). % 0.22/0.53 65[0:EqR:11.1] constant(sum__dfg(u,v)) || -> increases(v)* increases(u)* constant(v). % 0.22/0.53 66[0:EqR:8.1] constant(sum__dfg(u,v)) || -> decreases(u)* decreases(v)* constant(u). % 0.22/0.53 67[0:EqR:7.1] constant(sum__dfg(u,v)) || -> increases(v)* increases(u)* constant(u). % 0.22/0.53 78[0:Res:37.1,31.1] || in_environment(sk1,u) equal(first_movers,first_movers) -> equal(sum__dfg(cardinality_at_time(first_movers,u),cardinality_at_time(efficient_producers,u)),number_of_organizations(sk1,u))**. % 0.22/0.53 80[0:Obv:78.1] || in_environment(sk1,u) -> equal(sum__dfg(cardinality_at_time(first_movers,u),cardinality_at_time(efficient_producers,u)),number_of_organizations(sk1,u))**. % 0.22/0.53 112[0:Res:4.2,3.2] environment(u) environment(u) || in_environment(u,v) equal(first_movers,first_movers) -> equal(number_of_organizations(u,v),sum__dfg(cardinality_at_time(first_movers,v),cardinality_at_time(efficient_producers,v)))*. % 0.22/0.53 114[0:Obv:112.3] environment(u) || in_environment(u,v) -> equal(number_of_organizations(u,v),sum__dfg(cardinality_at_time(first_movers,v),cardinality_at_time(efficient_producers,v)))*. % 0.22/0.53 118[0:SpR:114.2,80.1] environment(u) || in_environment(u,v) in_environment(sk1,v) -> equal(number_of_organizations(u,v),number_of_organizations(sk1,v))*. % 0.22/0.53 139[0:SpR:118.3,23.0] environment(u) || in_environment(u,sk2) in_environment(sk1,sk2) -> constant(number_of_organizations(u,sk2))*. % 0.22/0.53 143[0:MRR:139.2,50.0] environment(u) || in_environment(u,sk2) -> constant(number_of_organizations(u,sk2))*. % 0.22/0.53 150[0:SpR:114.2,143.2] environment(u) environment(u) || in_environment(u,sk2)* in_environment(u,sk2)* -> constant(sum__dfg(cardinality_at_time(first_movers,sk2),cardinality_at_time(efficient_producers,sk2)))*. % 0.22/0.53 151[0:Obv:150.2] environment(u) || in_environment(u,sk2)*+ -> constant(sum__dfg(cardinality_at_time(first_movers,sk2),cardinality_at_time(efficient_producers,sk2)))*. % 0.22/0.53 162[0:Res:50.0,151.1] environment(sk1) || -> constant(sum__dfg(cardinality_at_time(first_movers,sk2),cardinality_at_time(efficient_producers,sk2)))*. % 0.22/0.53 163[0:SSi:162.0,21.0] || -> constant(sum__dfg(cardinality_at_time(first_movers,sk2),cardinality_at_time(efficient_producers,sk2)))*. % 0.22/0.53 171[0:SoR:67.0,163.0] || -> increases(cardinality_at_time(efficient_producers,sk2))* increases(cardinality_at_time(first_movers,sk2)) constant(cardinality_at_time(first_movers,sk2)). % 0.22/0.53 172[0:SoR:66.0,163.0] || -> decreases(cardinality_at_time(first_movers,sk2)) decreases(cardinality_at_time(efficient_producers,sk2))* constant(cardinality_at_time(first_movers,sk2)). % 0.22/0.53 173[0:SoR:65.0,163.0] || -> increases(cardinality_at_time(efficient_producers,sk2))* increases(cardinality_at_time(first_movers,sk2)) constant(cardinality_at_time(efficient_producers,sk2)). % 0.22/0.53 174[0:SoR:64.0,163.0] || -> decreases(cardinality_at_time(first_movers,sk2)) decreases(cardinality_at_time(efficient_producers,sk2))* constant(cardinality_at_time(efficient_producers,sk2)). % 0.22/0.53 175[0:SoR:63.0,163.0] || -> increases(cardinality_at_time(efficient_producers,sk2))* decreases(cardinality_at_time(efficient_producers,sk2)) constant(cardinality_at_time(first_movers,sk2)). % 0.22/0.53 176[0:SoR:62.0,163.0] || -> decreases(cardinality_at_time(first_movers,sk2)) increases(cardinality_at_time(first_movers,sk2))* constant(cardinality_at_time(efficient_producers,sk2)). % 0.22/0.53 177[0:SoR:61.0,163.0] || -> decreases(cardinality_at_time(first_movers,sk2)) increases(cardinality_at_time(first_movers,sk2))* constant(cardinality_at_time(first_movers,sk2)). % 0.22/0.53 178[0:SoR:60.0,163.0] || -> increases(cardinality_at_time(efficient_producers,sk2))* decreases(cardinality_at_time(efficient_producers,sk2)) constant(cardinality_at_time(efficient_producers,sk2)). % 0.22/0.53 181[1:Spt:171.0] || -> increases(cardinality_at_time(efficient_producers,sk2))*. % 0.22/0.53 182[2:Spt:172.0] || -> decreases(cardinality_at_time(first_movers,sk2))*. % 0.22/0.53 225[0:Res:52.0,15.3] environment(u) || increases(cardinality_at_time(efficient_producers,sk2)) in_environment(u,sk2) subpopulation(efficient_producers,u,sk2)* -> greater(growth_rate(efficient_producers,sk2),zero)*. % 0.22/0.53 226[0:Res:51.0,15.3] environment(u) || increases(cardinality_at_time(first_movers,sk2)) in_environment(u,sk2) subpopulation(first_movers,u,sk2)* -> greater(growth_rate(first_movers,sk2),zero)*. % 0.22/0.53 229[0:MRR:226.3,4.2] environment(u) || increases(cardinality_at_time(first_movers,sk2))+ in_environment(u,sk2)* -> greater(growth_rate(first_movers,sk2),zero)*. % 0.22/0.53 230[1:MRR:225.1,225.3,181.0,5.2] environment(u) || in_environment(u,sk2)*+ -> greater(growth_rate(efficient_producers,sk2),zero)*. % 0.22/0.53 233[1:Res:50.0,230.1] environment(sk1) || -> greater(growth_rate(efficient_producers,sk2),zero)*. % 0.22/0.53 234[1:SSi:233.0,21.0] || -> greater(growth_rate(efficient_producers,sk2),zero)*. % 0.22/0.53 235[1:MRR:26.1,234.0] || greater(zero,growth_rate(first_movers,sk2))* -> . % 0.22/0.53 240[0:Res:52.0,14.3] environment(u) || constant(cardinality_at_time(efficient_producers,sk2)) in_environment(u,sk2) subpopulation(efficient_producers,u,sk2)* -> equal(growth_rate(efficient_producers,sk2),zero). % 0.22/0.53 241[0:Res:51.0,14.3] environment(u) || constant(cardinality_at_time(first_movers,sk2)) in_environment(u,sk2) subpopulation(first_movers,u,sk2)* -> equal(growth_rate(first_movers,sk2),zero). % 0.22/0.53 244[0:MRR:241.3,4.2] environment(u) || constant(cardinality_at_time(first_movers,sk2))*+ in_environment(u,sk2)* -> equal(growth_rate(first_movers,sk2),zero). % 0.22/0.53 245[0:MRR:240.3,5.2] environment(u) || constant(cardinality_at_time(efficient_producers,sk2))*+ in_environment(u,sk2)* -> equal(growth_rate(efficient_producers,sk2),zero). % 0.22/0.53 250[0:Res:52.0,16.3] environment(u) || decreases(cardinality_at_time(efficient_producers,sk2)) in_environment(u,sk2) subpopulation(efficient_producers,u,sk2)* -> greater(zero,growth_rate(efficient_producers,sk2))*. % 0.22/0.53 251[0:Res:51.0,16.3] environment(u) || decreases(cardinality_at_time(first_movers,sk2)) in_environment(u,sk2) subpopulation(first_movers,u,sk2)* -> greater(zero,growth_rate(first_movers,sk2))*. % 0.22/0.53 254[2:MRR:251.1,251.3,251.4,182.0,4.2,235.0] environment(u) || in_environment(u,sk2)* -> . % 0.22/0.53 257[2:Res:50.0,254.1] environment(sk1) || -> . % 0.22/0.53 258[2:SSi:257.0,21.0] || -> . % 0.22/0.53 259[2:Spt:258.0,172.0,182.0] || decreases(cardinality_at_time(first_movers,sk2))* -> . % 0.22/0.53 260[2:Spt:258.0,172.1,172.2] || -> decreases(cardinality_at_time(efficient_producers,sk2))* constant(cardinality_at_time(first_movers,sk2)). % 0.22/0.53 261[2:MRR:174.0,259.0] || -> decreases(cardinality_at_time(efficient_producers,sk2))* constant(cardinality_at_time(efficient_producers,sk2)). % 0.22/0.53 262[2:MRR:176.0,259.0] || -> increases(cardinality_at_time(first_movers,sk2))* constant(cardinality_at_time(efficient_producers,sk2)). % 0.22/0.53 263[2:MRR:177.0,259.0] || -> increases(cardinality_at_time(first_movers,sk2))* constant(cardinality_at_time(first_movers,sk2)). % 0.22/0.53 264[0:MRR:250.3,5.2] environment(u) || decreases(cardinality_at_time(efficient_producers,sk2)) in_environment(u,sk2)* -> greater(zero,growth_rate(efficient_producers,sk2))*. % 0.22/0.53 269[3:Spt:260.0] || -> decreases(cardinality_at_time(efficient_producers,sk2))*. % 0.22/0.53 270[3:MRR:264.1,269.0] environment(u) || in_environment(u,sk2)*+ -> greater(zero,growth_rate(efficient_producers,sk2))*. % 0.22/0.53 271[4:Spt:262.0] || -> increases(cardinality_at_time(first_movers,sk2))*. % 0.22/0.53 285[0:Res:28.4,25.1] || increases(cardinality_at_time(first_movers,sk2)) in_environment(sk1,sk2) greater(cardinality_at_time(first_movers,sk2),zero)* subpopulation(first_movers,sk1,sk2) greater(zero,growth_rate(efficient_producers,sk2)) -> . % 0.22/0.53 286[4:MRR:285.0,285.1,285.2,271.0,50.0,51.0] || subpopulation(first_movers,sk1,sk2) greater(zero,growth_rate(efficient_producers,sk2))* -> . % 0.22/0.53 287[3:Res:50.0,270.1] environment(sk1) || -> greater(zero,growth_rate(efficient_producers,sk2))*. % 0.22/0.53 288[3:SSi:287.0,21.0] || -> greater(zero,growth_rate(efficient_producers,sk2))*. % 0.22/0.53 290[4:MRR:286.1,288.0] || subpopulation(first_movers,sk1,sk2)* -> . % 0.22/0.53 292[4:Res:37.1,290.0] || in_environment(sk1,sk2)* -> . % 0.22/0.53 294[4:MRR:292.0,50.0] || -> . % 0.22/0.53 295[4:Spt:294.0,262.0,271.0] || increases(cardinality_at_time(first_movers,sk2))* -> . % 0.22/0.53 296[4:Spt:294.0,262.1] || -> constant(cardinality_at_time(efficient_producers,sk2))*. % 0.22/0.53 297[4:MRR:263.0,295.0] || -> constant(cardinality_at_time(first_movers,sk2))*. % 0.22/0.53 298[4:MRR:244.1,297.0] environment(u) || in_environment(u,sk2)*+ -> equal(growth_rate(first_movers,sk2),zero)**. % 0.22/0.53 299[4:MRR:245.1,296.0] environment(u) || in_environment(u,sk2)* -> equal(growth_rate(efficient_producers,sk2),zero)**. % 0.22/0.53 317[4:Res:50.0,298.1] environment(sk1) || -> equal(growth_rate(first_movers,sk2),zero)**. % 0.22/0.53 318[4:SSi:317.0,21.0] || -> equal(growth_rate(first_movers,sk2),zero)**. % 0.22/0.53 319[4:Rew:318.0,24.1] || equal(growth_rate(efficient_producers,sk2),zero)** equal(zero,zero) -> . % 0.22/0.53 322[4:Obv:319.1] || equal(growth_rate(efficient_producers,sk2),zero)** -> . % 0.22/0.53 323[4:MRR:299.2,322.0] environment(u) || in_environment(u,sk2)* -> . % 0.22/0.53 326[4:Res:50.0,323.1] environment(sk1) || -> . % 0.22/0.53 327[4:SSi:326.0,21.0] || -> . % 0.22/0.53 328[3:Spt:327.0,260.0,269.0] || decreases(cardinality_at_time(efficient_producers,sk2))* -> . % 0.22/0.53 329[3:Spt:327.0,260.1] || -> constant(cardinality_at_time(first_movers,sk2))*. % 0.22/0.53 330[3:MRR:261.0,328.0] || -> constant(cardinality_at_time(efficient_producers,sk2))*. % 0.22/0.53 331[3:MRR:244.1,329.0] environment(u) || in_environment(u,sk2)* -> equal(growth_rate(first_movers,sk2),zero)**. % 0.22/0.53 333[3:MRR:245.1,330.0] environment(u) || in_environment(u,sk2)* -> equal(growth_rate(efficient_producers,sk2),zero)**. % 0.22/0.53 334[0:MRR:285.1,285.2,50.0,51.0] || increases(cardinality_at_time(first_movers,sk2)) subpopulation(first_movers,sk1,sk2) greater(zero,growth_rate(efficient_producers,sk2))* -> . % 0.22/0.53 347[4:Spt:24.0] || equal(growth_rate(efficient_producers,sk2),zero)** -> . % 0.22/0.53 348[4:MRR:333.2,347.0] environment(u) || in_environment(u,sk2)* -> . % 0.22/0.53 349[4:Res:50.0,348.1] environment(sk1) || -> . % 0.22/0.53 350[4:SSi:349.0,21.0] || -> . % 0.22/0.53 351[4:Spt:350.0,24.0,347.0] || -> equal(growth_rate(efficient_producers,sk2),zero)**. % 0.22/0.53 352[4:Spt:350.0,24.1] || equal(growth_rate(first_movers,sk2),zero)** -> . % 0.22/0.53 357[4:MRR:331.2,352.0] environment(u) || in_environment(u,sk2)* -> . % 0.22/0.53 362[4:Res:50.0,357.1] environment(sk1) || -> . % 0.22/0.53 363[4:SSi:362.0,21.0] || -> . % 0.22/0.53 364[1:Spt:363.0,171.0,181.0] || increases(cardinality_at_time(efficient_producers,sk2))* -> . % 0.22/0.53 365[1:Spt:363.0,171.1,171.2] || -> increases(cardinality_at_time(first_movers,sk2))* constant(cardinality_at_time(first_movers,sk2)). % 0.22/0.53 366[1:MRR:173.0,364.0] || -> increases(cardinality_at_time(first_movers,sk2))* constant(cardinality_at_time(efficient_producers,sk2)). % 0.22/0.53 367[1:MRR:175.0,364.0] || -> decreases(cardinality_at_time(efficient_producers,sk2))* constant(cardinality_at_time(first_movers,sk2)). % 0.22/0.53 368[1:MRR:178.0,364.0] || -> decreases(cardinality_at_time(efficient_producers,sk2))* constant(cardinality_at_time(efficient_producers,sk2)). % 0.22/0.53 370[2:Spt:365.0] || -> increases(cardinality_at_time(first_movers,sk2))*. % 0.22/0.53 371[2:MRR:334.0,370.0] || subpopulation(first_movers,sk1,sk2) greater(zero,growth_rate(efficient_producers,sk2))* -> . % 0.22/0.53 372[2:MRR:229.1,370.0] environment(u) || in_environment(u,sk2)* -> greater(growth_rate(first_movers,sk2),zero)*. % 0.22/0.53 377[3:Spt:25.0] || greater(zero,growth_rate(efficient_producers,sk2))* -> . % 0.22/0.53 378[3:MRR:264.3,377.0] environment(u) || decreases(cardinality_at_time(efficient_producers,sk2))* in_environment(u,sk2)* -> . % 0.22/0.53 379[4:Spt:367.0] || -> decreases(cardinality_at_time(efficient_producers,sk2))*. % 0.22/0.53 380[4:MRR:378.1,379.0] environment(u) || in_environment(u,sk2)* -> . % 0.22/0.53 381[4:Res:50.0,380.1] environment(sk1) || -> . % 0.22/0.53 382[4:SSi:381.0,21.0] || -> . % 0.22/0.53 383[4:Spt:382.0,367.0,379.0] || decreases(cardinality_at_time(efficient_producers,sk2))* -> . % 0.22/0.53 384[4:Spt:382.0,367.1] || -> constant(cardinality_at_time(first_movers,sk2))*. % 0.22/0.53 385[4:MRR:368.0,383.0] || -> constant(cardinality_at_time(efficient_producers,sk2))*. % 0.22/0.53 386[4:MRR:244.1,384.0] environment(u) || in_environment(u,sk2)* -> equal(growth_rate(first_movers,sk2),zero)**. % 0.22/0.53 387[4:Rew:386.2,372.2] environment(u) || in_environment(u,sk2)* -> greater(zero,zero)*. % 0.22/0.53 388[4:MRR:245.1,385.0] environment(u) || in_environment(u,sk2)* -> equal(growth_rate(efficient_producers,sk2),zero)**. % 0.22/0.54 390[5:Spt:24.0] || equal(growth_rate(efficient_producers,sk2),zero)** -> . % 0.22/0.54 391[5:MRR:388.2,390.0] environment(u) || in_environment(u,sk2)* -> . % 0.22/0.54 392[5:Res:50.0,391.1] environment(sk1) || -> . % 0.22/0.54 393[5:SSi:392.0,21.0] || -> . % 0.22/0.54 394[5:Spt:393.0,24.0,390.0] || -> equal(growth_rate(efficient_producers,sk2),zero)**. % 0.22/0.54 395[5:Spt:393.0,24.1] || equal(growth_rate(first_movers,sk2),zero)** -> . % 0.22/0.54 396[5:Rew:394.0,377.0] || greater(zero,zero)* -> . % 0.22/0.54 398[5:MRR:387.2,396.0] environment(u) || in_environment(u,sk2)* -> . % 0.22/0.54 401[5:Res:50.0,398.1] environment(sk1) || -> . % 0.22/0.54 402[5:SSi:401.0,21.0] || -> . % 0.22/0.54 403[3:Spt:402.0,25.0,377.0] || -> greater(zero,growth_rate(efficient_producers,sk2))*. % 0.22/0.54 404[3:Spt:402.0,25.1] || greater(growth_rate(first_movers,sk2),zero)* -> . % 0.22/0.54 405[3:MRR:371.1,403.0] || subpopulation(first_movers,sk1,sk2)* -> . % 0.22/0.54 408[3:Res:37.1,405.0] || in_environment(sk1,sk2)* -> . % 0.22/0.54 410[3:MRR:408.0,50.0] || -> . % 0.22/0.54 411[2:Spt:410.0,365.0,370.0] || increases(cardinality_at_time(first_movers,sk2))* -> . % 0.22/0.54 412[2:Spt:410.0,365.1] || -> constant(cardinality_at_time(first_movers,sk2))*. % 0.22/0.54 413[2:MRR:366.0,411.0] || -> constant(cardinality_at_time(efficient_producers,sk2))*. % 0.22/0.54 414[2:MRR:244.1,412.0] environment(u) || in_environment(u,sk2)* -> equal(growth_rate(first_movers,sk2),zero)**. % 0.22/0.54 415[2:MRR:245.1,413.0] environment(u) || in_environment(u,sk2)* -> equal(growth_rate(efficient_producers,sk2),zero)**. % 0.22/0.54 435[3:Spt:24.0] || equal(growth_rate(efficient_producers,sk2),zero)** -> . % 0.22/0.54 436[3:MRR:415.2,435.0] environment(u) || in_environment(u,sk2)* -> . % 0.22/0.54 437[3:Res:50.0,436.1] environment(sk1) || -> . % 0.22/0.54 438[3:SSi:437.0,21.0] || -> . % 0.22/0.54 439[3:Spt:438.0,24.0,435.0] || -> equal(growth_rate(efficient_producers,sk2),zero)**. % 0.22/0.54 440[3:Spt:438.0,24.1] || equal(growth_rate(first_movers,sk2),zero)** -> . % 0.22/0.54 443[3:MRR:414.2,440.0] environment(u) || in_environment(u,sk2)* -> . % 0.22/0.54 446[3:Res:50.0,443.1] environment(sk1) || -> . % 0.22/0.54 447[3:SSi:446.0,21.0] || -> . % 0.22/0.54 % SZS output end Refutation % 0.22/0.54 Formulae used in the proof : mp_only_members_29 mp_subpopulations_30 mp_subpopulations_31 mp_abc_sum_increase_32 mp_abc_sum_increase_33 mp_abc_sum_increase_34 mp_abc_sum_increase_35 mp_abc_sum_increase_36 mp_abc_sum_increase_37 mp_abc_sum_increase_38 mp_abc_sum_increase_39 mp_growth_rate_40 mp_growth_rate_41 mp_growth_rate_42 mp_non_zero_producers_43 mp_non_zero_producers_44 mp_time_point_occur_45 prove_l7_47 prove_l7_48 prove_l7_49 prove_l7_50 prove_l7_51 prove_l7_52 % 0.22/0.54 %------------------------------------------------------------------------------