%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT039+2 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n009.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:54 AM UTC 2026 % Result : Theorem 13.45s 13.74s % Output : Refutation 13.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT039+2 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.04 % Command : run_spass %d %s % 0.08/0.35 % Computer : n009.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:55:37 UTC 2026 % 0.08/0.35 % CPUTime : % 13.45/13.74 % 13.45/13.74 SPASS V 3.9 % 13.45/13.74 SPASS beiseite: Proof found. % 13.45/13.74 % SZS status Theorem % 13.45/13.74 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 13.45/13.74 SPASS derived 5009 clauses, backtracked 711 clauses, performed 64 splits and kept 3886 clauses. % 13.45/13.74 SPASS allocated 103880 KBytes. % 13.45/13.74 SPASS spent 0:0:13.37 on the problem. % 13.45/13.74 0:00:00.06 for the input. % 13.45/13.74 0:00:00.05 for the FLOTTER CNF translation. % 13.45/13.74 0:00:00.26 for inferences. % 13.45/13.74 0:00:00.16 for the backtracking. % 13.45/13.74 0:0:12.71 for the reduction. % 13.45/13.74 % 13.45/13.74 % 13.45/13.74 Here is a proof with depth 14, length 196 : % 13.45/13.74 % SZS output start Refutation % 13.45/13.74 1[0:Inp] || -> observational_period(skc1)*. % 13.45/13.74 2[0:Inp] || -> slow_change(skc1)*. % 13.45/13.74 3[0:Inp] || -> propagation_strategy(first_movers)*. % 13.45/13.74 4[0:Inp] || -> propagation_strategy(efficient_producers)*. % 13.45/13.74 5[0:Inp] || -> environment(skf2(u))*. % 13.45/13.74 6[0:Inp] || selection_favors(efficient_producers,first_movers,skc1)* -> . % 13.45/13.74 7[0:Inp] || greater(u,v) -> greater_or_equal(u,v)*. % 13.45/13.74 8[0:Inp] || equal(u,v) -> greater_or_equal(u,v)*. % 13.45/13.74 9[0:Inp] environment(u) || -> greater_or_equal(critical_point(u),start_time(u))*. % 13.45/13.74 10[0:Inp] environment(u) || -> greater_or_equal(critical_point(u),appear(efficient_producers,u))*. % 13.45/13.74 11[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 13.45/13.74 12[0:Inp] environment(u) || in_environment(u,v) -> greater_or_equal(end_time(u),v)*. % 13.45/13.74 13[0:Inp] environment(u) || in_environment(u,v) -> subpopulation(first_movers,u,v)*. % 13.45/13.74 14[0:Inp] environment(u) || in_environment(u,v) -> subpopulation(efficient_producers,u,v)*. % 13.45/13.74 15[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 13.45/13.74 16[0:Inp] environment(u) || in_environment(u,v)*+ -> greater_or_equal(cardinality_at_time(first_movers,v),zero)*. % 13.45/13.74 18[0:Inp] environment(u) || greater_or_equal(v,start_time(u))*+ greater_or_equal(end_time(u),v)* -> in_environment(u,v). % 13.45/13.74 20[0:Inp] observational_period(u) || propagation_strategy(efficient_producers) propagation_strategy(first_movers) -> in_environment(u,skf2(u))* selection_favors(efficient_producers,first_movers,u)*. % 13.45/13.74 21[0:Inp] environment(u) slow_change(v) observational_period(v) || in_environment(v,u)*+ -> in_environment(u,skf3(u))*. % 13.45/13.74 22[0:Inp] environment(u) slow_change(v) observational_period(v) || in_environment(v,u)* -> greater(skf3(u),critical_point(u)). % 13.45/13.74 23[0:Inp] environment(u) || in_environment(u,v) greater_or_equal(v,appear(efficient_producers,u))* -> greater(cardinality_at_time(efficient_producers,v),zero). % 13.45/13.74 24[0:Inp] observational_period(u) || selection_favors(efficient_producers,first_movers,end_time(skf2(u)))* propagation_strategy(efficient_producers) propagation_strategy(first_movers) -> selection_favors(efficient_producers,first_movers,u). % 13.45/13.74 25[0:Inp] environment(u) || greater(v,critical_point(u)) subpopulations(first_movers,efficient_producers,u,v)* -> greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v)). % 13.45/13.74 26[0:Inp] environment(u) || greater(growth_rate(v,w),growth_rate(x,w)) subpopulations(x,v,u,w)* -> selection_favors(v,x,w). % 13.45/13.74 27[0:Inp] environment(u) || in_environment(u,v) greater(cardinality_at_time(first_movers,v),zero) greater(cardinality_at_time(efficient_producers,v),zero) -> subpopulations(first_movers,efficient_producers,u,v)*. % 13.45/13.74 28[0:Inp] environment(u) || equal(cardinality_at_time(v,w),zero) greater(cardinality_at_time(x,w),zero)+ subpopulation(v,u,w)* subpopulation(x,u,w)* -> selection_favors(x,v,w)*. % 13.45/13.74 29[0:MRR:20.1,20.2,4.0,3.0] observational_period(u) || -> in_environment(u,skf2(u))* selection_favors(efficient_producers,first_movers,u)*. % 13.45/13.74 30[0:MRR:24.2,24.3,4.0,3.0] observational_period(u) || selection_favors(efficient_producers,first_movers,end_time(skf2(u)))* -> selection_favors(efficient_producers,first_movers,u). % 13.45/13.74 33[0:Res:1.0,22.0] slow_change(skc1) environment(u) || in_environment(skc1,u)* -> greater(skf3(u),critical_point(u)). % 13.45/13.74 37[0:Res:30.2,6.0] observational_period(skc1) || selection_favors(efficient_producers,first_movers,end_time(skf2(skc1)))* -> . % 13.45/13.74 38[0:Res:29.2,6.0] observational_period(skc1) || -> in_environment(skc1,skf2(skc1))*. % 13.45/13.74 41[0:MRR:38.0,1.0] || -> in_environment(skc1,skf2(skc1))*. % 13.45/13.74 42[0:MRR:37.0,1.0] || selection_favors(efficient_producers,first_movers,end_time(skf2(skc1)))* -> . % 13.45/13.74 44[0:MRR:33.0,2.0] environment(u) || in_environment(skc1,u)* -> greater(skf3(u),critical_point(u)). % 13.45/13.74 52[0:Res:12.2,11.0] environment(u) || in_environment(u,v)* -> equal(end_time(u),v) greater(end_time(u),v). % 13.45/13.74 53[0:Res:9.1,11.0] environment(u) || -> equal(start_time(u),critical_point(u)) greater(critical_point(u),start_time(u))*r. % 13.45/13.74 54[0:Res:10.1,11.0] environment(u) || -> equal(appear(efficient_producers,u),critical_point(u)) greater(critical_point(u),appear(efficient_producers,u))*r. % 13.45/13.74 57[0:Res:7.1,18.1] environment(u) || greater(v,start_time(u)) greater_or_equal(end_time(u),v)* -> in_environment(u,v). % 13.45/13.74 58[0:Res:8.1,18.1] environment(u) || equal(v,start_time(u)) greater_or_equal(end_time(u),v)* -> in_environment(u,v). % 13.45/13.74 59[0:Res:12.2,18.1] environment(u) environment(v) || in_environment(u,start_time(v)) greater_or_equal(end_time(v),end_time(u))* -> in_environment(v,end_time(u)). % 13.45/13.74 62[0:Res:41.0,21.3] environment(skf2(skc1)) slow_change(skc1) observational_period(skc1) || -> in_environment(skf2(skc1),skf3(skf2(skc1)))*. % 13.45/13.74 63[0:Res:29.1,21.3] observational_period(u) environment(skf2(u)) slow_change(u) observational_period(u) || -> selection_favors(efficient_producers,first_movers,u) in_environment(skf2(u),skf3(skf2(u)))*. % 13.45/13.74 65[0:SSi:62.2,62.1,62.0,2.0,1.0,2.0,1.0,5.0,2.0,1.0] || -> in_environment(skf2(skc1),skf3(skf2(skc1)))*. % 13.45/13.74 66[0:Obv:63.0] environment(skf2(u)) slow_change(u) observational_period(u) || -> selection_favors(efficient_producers,first_movers,u) in_environment(skf2(u),skf3(skf2(u)))*. % 13.45/13.74 67[0:SSi:66.0,5.0] slow_change(u) observational_period(u) || -> selection_favors(efficient_producers,first_movers,u) in_environment(skf2(u),skf3(skf2(u)))*. % 13.45/13.74 69[0:Res:65.0,16.1] environment(skf2(skc1)) || -> greater_or_equal(cardinality_at_time(first_movers,skf3(skf2(skc1))),zero)*. % 13.45/13.74 70[0:SSi:69.0,5.0,2.0,1.0] || -> greater_or_equal(cardinality_at_time(first_movers,skf3(skf2(skc1))),zero)*. % 13.45/13.74 71[0:Res:70.0,11.0] || -> equal(cardinality_at_time(first_movers,skf3(skf2(skc1))),zero) greater(cardinality_at_time(first_movers,skf3(skf2(skc1))),zero)*l. % 13.45/13.74 82[0:Res:7.1,58.2] environment(u) || greater(end_time(u),v) equal(v,start_time(u)) -> in_environment(u,v)*. % 13.45/13.74 88[0:Res:7.1,23.2] environment(u) || greater(v,appear(efficient_producers,u))*+ in_environment(u,v)* -> greater(cardinality_at_time(efficient_producers,v),zero)*l. % 13.45/13.74 93[0:Res:41.0,44.1] environment(skf2(skc1)) || -> greater(skf3(skf2(skc1)),critical_point(skf2(skc1)))*l. % 13.45/13.74 97[0:SSi:93.0,5.0,2.0,1.0] || -> greater(skf3(skf2(skc1)),critical_point(skf2(skc1)))*l. % 13.45/13.74 135[0:Res:65.0,52.1] environment(skf2(skc1)) || -> equal(skf3(skf2(skc1)),end_time(skf2(skc1))) greater(end_time(skf2(skc1)),skf3(skf2(skc1)))*r. % 13.45/13.74 137[0:SSi:135.0,5.0,2.0,1.0] || -> equal(skf3(skf2(skc1)),end_time(skf2(skc1))) greater(end_time(skf2(skc1)),skf3(skf2(skc1)))*r. % 13.45/13.74 140[1:Spt:137.0] || -> equal(skf3(skf2(skc1)),end_time(skf2(skc1)))**. % 13.45/13.74 141[1:Rew:140.0,65.0] || -> in_environment(skf2(skc1),end_time(skf2(skc1)))*. % 13.45/13.74 143[1:Rew:140.0,71.0] || -> equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero) greater(cardinality_at_time(first_movers,skf3(skf2(skc1))),zero)*l. % 13.45/13.74 144[1:Rew:140.0,97.0] || -> greater(end_time(skf2(skc1)),critical_point(skf2(skc1)))*r. % 13.45/13.74 147[1:Rew:140.0,143.1] || -> equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero) greater(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero)*l. % 13.45/13.74 158[0:Res:27.4,26.2] environment(u) environment(u) || in_environment(u,v)* greater(cardinality_at_time(first_movers,v),zero) greater(cardinality_at_time(efficient_producers,v),zero) greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v)) -> selection_favors(efficient_producers,first_movers,v)*. % 13.45/13.74 159[0:Res:27.4,25.2] environment(u) environment(u) || in_environment(u,v)* greater(cardinality_at_time(first_movers,v),zero) greater(cardinality_at_time(efficient_producers,v),zero)*l greater(v,critical_point(u)) -> greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v)). % 13.45/13.74 160[0:Obv:158.0] environment(u) || in_environment(u,v)* greater(cardinality_at_time(first_movers,v),zero) greater(cardinality_at_time(efficient_producers,v),zero) greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v))+ -> selection_favors(efficient_producers,first_movers,v)*. % 13.45/13.74 161[0:Obv:159.0] environment(u) || in_environment(u,v)* greater(cardinality_at_time(first_movers,v),zero)+ greater(cardinality_at_time(efficient_producers,v),zero)*l greater(v,critical_point(u)) -> greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v)). % 13.45/13.74 163[0:Res:8.1,57.2] environment(u) || equal(end_time(u),v) greater(v,start_time(u)) -> in_environment(u,v)*. % 13.45/13.74 171[0:Res:82.3,16.1] environment(u) environment(u) || greater(end_time(u),v)* equal(v,start_time(u))* -> greater_or_equal(cardinality_at_time(first_movers,v),zero)*. % 13.45/13.74 173[0:Obv:171.0] environment(u) || greater(end_time(u),v)*+ equal(v,start_time(u))* -> greater_or_equal(cardinality_at_time(first_movers,v),zero)*. % 13.45/13.74 179[0:Res:163.3,16.1] environment(u) environment(u) || equal(end_time(u),v) greater(v,start_time(u))* -> greater_or_equal(cardinality_at_time(first_movers,v),zero)*. % 13.45/13.74 181[0:Obv:179.0] environment(u) || equal(end_time(u),v) greater(v,start_time(u))*+ -> greater_or_equal(cardinality_at_time(first_movers,v),zero)*. % 13.45/13.74 192[0:Res:8.1,59.3] environment(u) environment(v) || equal(end_time(v),end_time(u))+ in_environment(u,start_time(v))* -> in_environment(v,end_time(u))*. % 13.45/13.74 196[0:EqR:192.2] environment(u) environment(u) || in_environment(u,start_time(u))* -> in_environment(u,end_time(u)). % 13.45/13.74 197[0:Obv:196.0] environment(u) || in_environment(u,start_time(u))* -> in_environment(u,end_time(u)). % 13.45/13.74 199[0:Res:82.3,197.1] environment(u) environment(u) || greater(end_time(u),start_time(u)) equal(start_time(u),start_time(u)) -> in_environment(u,end_time(u))*. % 13.45/13.74 202[0:Obv:199.3] environment(u) || greater(end_time(u),start_time(u)) -> in_environment(u,end_time(u))*. % 13.45/13.74 216[0:Res:202.2,16.1] environment(u) environment(u) || greater(end_time(u),start_time(u)) -> greater_or_equal(cardinality_at_time(first_movers,end_time(u)),zero)*. % 13.45/13.74 217[0:Obv:216.0] environment(u) || greater(end_time(u),start_time(u)) -> greater_or_equal(cardinality_at_time(first_movers,end_time(u)),zero)*. % 13.45/13.74 244[0:NCh:15.2,15.1,173.1,54.2] environment(u) environment(v) || greater(end_time(u),critical_point(v))+ equal(appear(efficient_producers,v),start_time(u))* -> greater_or_equal(cardinality_at_time(first_movers,appear(efficient_producers,v)),zero)* equal(appear(efficient_producers,v),critical_point(v)). % 13.45/13.74 253[0:NCh:15.2,15.1,88.1,54.2] environment(u) environment(u) || greater(v,critical_point(u)) in_environment(u,v)* -> greater(cardinality_at_time(efficient_producers,v),zero)*l equal(appear(efficient_producers,u),critical_point(u))**. % 13.45/13.74 257[0:Obv:253.0] environment(u) || greater(v,critical_point(u))+ in_environment(u,v)* -> greater(cardinality_at_time(efficient_producers,v),zero)*l equal(appear(efficient_producers,u),critical_point(u))**. % 13.45/13.74 262[1:NCh:15.2,15.0,181.2,147.1] environment(u) || equal(end_time(u),cardinality_at_time(first_movers,end_time(skf2(skc1))))*+ equal(start_time(u),zero)** -> greater_or_equal(cardinality_at_time(first_movers,cardinality_at_time(first_movers,end_time(skf2(skc1)))),zero)* equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero). % 13.45/13.74 263[0:NCh:15.2,15.1,181.2,53.2] environment(u) environment(u) || equal(end_time(u),v) greater(v,critical_point(u))* -> greater_or_equal(cardinality_at_time(first_movers,v),zero)* equal(start_time(u),critical_point(u))**. % 13.45/13.74 267[0:Obv:263.0] environment(u) || equal(end_time(u),v) greater(v,critical_point(u))*+ -> greater_or_equal(cardinality_at_time(first_movers,v),zero)* equal(start_time(u),critical_point(u))**. % 13.45/13.74 422[1:Res:147.1,161.2] environment(u) || in_environment(u,end_time(skf2(skc1)))* greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero)*l greater(end_time(skf2(skc1)),critical_point(u)) -> equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero) greater(growth_rate(efficient_producers,end_time(skf2(skc1))),growth_rate(first_movers,end_time(skf2(skc1)))). % 13.45/13.74 580[1:Res:144.0,257.1] environment(skf2(skc1)) || in_environment(skf2(skc1),end_time(skf2(skc1)))* -> greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero) equal(appear(efficient_producers,skf2(skc1)),critical_point(skf2(skc1))). % 13.45/13.74 607[1:SSi:580.0,5.0,2.0,1.0] || in_environment(skf2(skc1),end_time(skf2(skc1)))* -> greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero) equal(appear(efficient_producers,skf2(skc1)),critical_point(skf2(skc1))). % 13.45/13.74 608[1:MRR:607.0,141.0] || -> greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero)*l equal(appear(efficient_producers,skf2(skc1)),critical_point(skf2(skc1))). % 13.45/13.74 611[2:Spt:608.0] || -> greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero)*l. % 13.45/13.74 612[2:MRR:422.2,611.0] environment(u) || in_environment(u,end_time(skf2(skc1)))* greater(end_time(skf2(skc1)),critical_point(u)) -> equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero)** greater(growth_rate(efficient_producers,end_time(skf2(skc1))),growth_rate(first_movers,end_time(skf2(skc1)))). % 13.45/13.74 613[2:Res:611.0,28.2] environment(u) || equal(cardinality_at_time(v,end_time(skf2(skc1))),zero)+ subpopulation(v,u,end_time(skf2(skc1)))* subpopulation(efficient_producers,u,end_time(skf2(skc1)))* -> selection_favors(efficient_producers,v,end_time(skf2(skc1)))*. % 13.45/13.74 903[3:Spt:262.4] || -> equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero)**. % 13.45/13.74 917[3:SpL:903.0,613.1] environment(u) || equal(zero,zero) subpopulation(first_movers,u,end_time(skf2(skc1))) subpopulation(efficient_producers,u,end_time(skf2(skc1)))* -> selection_favors(efficient_producers,first_movers,end_time(skf2(skc1)))*. % 13.45/13.74 920[3:Obv:917.1] environment(u) || subpopulation(first_movers,u,end_time(skf2(skc1))) subpopulation(efficient_producers,u,end_time(skf2(skc1)))* -> selection_favors(efficient_producers,first_movers,end_time(skf2(skc1)))*. % 13.45/13.74 921[3:MRR:920.3,42.0] environment(u) || subpopulation(first_movers,u,end_time(skf2(skc1))) subpopulation(efficient_producers,u,end_time(skf2(skc1)))* -> . % 13.45/13.74 923[3:Res:14.2,921.2] environment(u) environment(u) || in_environment(u,end_time(skf2(skc1))) subpopulation(first_movers,u,end_time(skf2(skc1)))* -> . % 13.45/13.74 924[3:Obv:923.0] environment(u) || in_environment(u,end_time(skf2(skc1))) subpopulation(first_movers,u,end_time(skf2(skc1)))* -> . % 13.45/13.74 925[3:MRR:924.2,13.2] environment(u) || in_environment(u,end_time(skf2(skc1)))* -> . % 13.45/13.74 934[3:Res:141.0,925.1] environment(skf2(skc1)) || -> . % 13.45/13.74 937[3:SSi:934.0,5.0,2.0,1.0] || -> . % 13.45/13.74 953[3:Spt:937.0,262.4,903.0] || equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero)** -> . % 13.45/13.74 954[3:Spt:937.0,262.0,262.1,262.2,262.3] environment(u) || equal(end_time(u),cardinality_at_time(first_movers,end_time(skf2(skc1))))*+ equal(start_time(u),zero)** -> greater_or_equal(cardinality_at_time(first_movers,cardinality_at_time(first_movers,end_time(skf2(skc1)))),zero)*. % 13.45/13.74 955[3:MRR:147.0,953.0] || -> greater(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero)*l. % 13.45/13.74 966[3:MRR:612.3,953.0] environment(u) || in_environment(u,end_time(skf2(skc1)))* greater(end_time(skf2(skc1)),critical_point(u))+ -> greater(growth_rate(efficient_producers,end_time(skf2(skc1))),growth_rate(first_movers,end_time(skf2(skc1))))*l. % 13.45/13.74 2344[3:Res:144.0,966.2] environment(skf2(skc1)) || in_environment(skf2(skc1),end_time(skf2(skc1)))* -> greater(growth_rate(efficient_producers,end_time(skf2(skc1))),growth_rate(first_movers,end_time(skf2(skc1)))). % 13.45/13.74 2347[3:SSi:2344.0,5.0,2.0,1.0] || in_environment(skf2(skc1),end_time(skf2(skc1)))* -> greater(growth_rate(efficient_producers,end_time(skf2(skc1))),growth_rate(first_movers,end_time(skf2(skc1)))). % 13.45/13.74 2348[3:MRR:2347.0,141.0] || -> greater(growth_rate(efficient_producers,end_time(skf2(skc1))),growth_rate(first_movers,end_time(skf2(skc1))))*l. % 13.45/13.74 2350[3:Res:2348.0,160.4] environment(u) || in_environment(u,end_time(skf2(skc1)))* greater(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero) greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero) -> selection_favors(efficient_producers,first_movers,end_time(skf2(skc1)))*. % 13.45/13.74 2381[3:MRR:2350.2,2350.3,2350.4,955.0,611.0,42.0] environment(u) || in_environment(u,end_time(skf2(skc1)))* -> . % 13.45/13.74 2391[3:Res:141.0,2381.1] environment(skf2(skc1)) || -> . % 13.45/13.74 2398[3:SSi:2391.0,5.0,2.0,1.0] || -> . % 13.45/13.74 2426[2:Spt:2398.0,608.0,611.0] || greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero)*l -> . % 13.45/13.74 2427[2:Spt:2398.0,608.1] || -> equal(appear(efficient_producers,skf2(skc1)),critical_point(skf2(skc1)))**. % 13.45/13.74 2450[2:SpL:2427.0,88.1] environment(skf2(skc1)) || greater(u,critical_point(skf2(skc1))) in_environment(skf2(skc1),u)* -> greater(cardinality_at_time(efficient_producers,u),zero). % 13.45/13.74 2461[2:SSi:2450.0,5.0,2.0,1.0] || greater(u,critical_point(skf2(skc1))) in_environment(skf2(skc1),u)* -> greater(cardinality_at_time(efficient_producers,u),zero). % 13.45/13.74 2586[2:Res:67.3,2461.1] slow_change(skc1) observational_period(skc1) || greater(skf3(skf2(skc1)),critical_point(skf2(skc1))) -> selection_favors(efficient_producers,first_movers,skc1) greater(cardinality_at_time(efficient_producers,skf3(skf2(skc1))),zero)*l. % 13.45/13.74 2594[2:Rew:140.0,2586.4,140.0,2586.2] slow_change(skc1) observational_period(skc1) || greater(end_time(skf2(skc1)),critical_point(skf2(skc1))) -> selection_favors(efficient_producers,first_movers,skc1) greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero)*l. % 13.45/13.74 2595[2:SSi:2594.1,2594.0,2.0,1.0,2.0,1.0] || greater(end_time(skf2(skc1)),critical_point(skf2(skc1))) -> selection_favors(efficient_producers,first_movers,skc1) greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero)*l. % 13.45/13.74 2596[2:MRR:2595.0,2595.1,2595.2,144.0,6.0,2426.0] || -> . % 13.45/13.74 2610[1:Spt:2596.0,137.0,140.0] || equal(skf3(skf2(skc1)),end_time(skf2(skc1)))** -> . % 13.45/13.74 2611[1:Spt:2596.0,137.1] || -> greater(end_time(skf2(skc1)),skf3(skf2(skc1)))*r. % 13.45/13.74 2640[1:OCh:15.1,15.0,97.0,2611.0] || -> greater(end_time(skf2(skc1)),critical_point(skf2(skc1)))*r. % 13.45/13.74 2675[1:Res:2640.0,257.1] environment(skf2(skc1)) || in_environment(skf2(skc1),end_time(skf2(skc1)))* -> greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero) equal(appear(efficient_producers,skf2(skc1)),critical_point(skf2(skc1))). % 13.45/13.74 2676[1:Res:2640.0,267.2] environment(skf2(skc1)) || equal(end_time(skf2(skc1)),end_time(skf2(skc1))) -> greater_or_equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero)* equal(start_time(skf2(skc1)),critical_point(skf2(skc1))). % 13.45/13.74 2707[1:Obv:2676.1] environment(skf2(skc1)) || -> greater_or_equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero)* equal(start_time(skf2(skc1)),critical_point(skf2(skc1))). % 13.45/13.74 2708[1:SSi:2707.0,5.0,2.0,1.0] || -> greater_or_equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero)* equal(start_time(skf2(skc1)),critical_point(skf2(skc1))). % 13.45/13.74 2713[1:SSi:2675.0,5.0,2.0,1.0] || in_environment(skf2(skc1),end_time(skf2(skc1)))* -> greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero) equal(appear(efficient_producers,skf2(skc1)),critical_point(skf2(skc1))). % 13.45/13.74 2758[2:Spt:2708.0] || -> greater_or_equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero)*. % 13.45/13.74 2759[2:Res:2758.0,11.0] || -> equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero) greater(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero)*l. % 13.45/13.74 2801[2:Res:2759.1,161.2] environment(u) || in_environment(u,end_time(skf2(skc1)))* greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero)*l greater(end_time(skf2(skc1)),critical_point(u)) -> equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero) greater(growth_rate(efficient_producers,end_time(skf2(skc1))),growth_rate(first_movers,end_time(skf2(skc1)))). % 13.45/13.74 2830[2:NCh:15.2,15.0,2759.1,181.2] environment(u) || equal(end_time(u),cardinality_at_time(first_movers,end_time(skf2(skc1))))*+ equal(start_time(u),zero)** -> equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero) greater_or_equal(cardinality_at_time(first_movers,cardinality_at_time(first_movers,end_time(skf2(skc1)))),zero)*. % 13.45/13.74 2906[3:Spt:2713.1] || -> greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero)*l. % 13.45/13.74 2907[3:MRR:2801.2,2906.0] environment(u) || in_environment(u,end_time(skf2(skc1)))* greater(end_time(skf2(skc1)),critical_point(u)) -> equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero)** greater(growth_rate(efficient_producers,end_time(skf2(skc1))),growth_rate(first_movers,end_time(skf2(skc1)))). % 13.45/13.74 2908[3:Res:2906.0,28.2] environment(u) || equal(cardinality_at_time(v,end_time(skf2(skc1))),zero)+ subpopulation(v,u,end_time(skf2(skc1)))* subpopulation(efficient_producers,u,end_time(skf2(skc1)))* -> selection_favors(efficient_producers,v,end_time(skf2(skc1)))*. % 13.45/13.74 3198[4:Spt:2830.3] || -> equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero)**. % 13.45/13.74 3212[4:SpL:3198.0,2908.1] environment(u) || equal(zero,zero) subpopulation(first_movers,u,end_time(skf2(skc1))) subpopulation(efficient_producers,u,end_time(skf2(skc1)))* -> selection_favors(efficient_producers,first_movers,end_time(skf2(skc1)))*. % 13.45/13.74 3215[4:Obv:3212.1] environment(u) || subpopulation(first_movers,u,end_time(skf2(skc1))) subpopulation(efficient_producers,u,end_time(skf2(skc1)))* -> selection_favors(efficient_producers,first_movers,end_time(skf2(skc1)))*. % 13.45/13.74 3216[4:MRR:3215.3,42.0] environment(u) || subpopulation(first_movers,u,end_time(skf2(skc1))) subpopulation(efficient_producers,u,end_time(skf2(skc1)))* -> . % 13.45/13.74 3218[4:Res:14.2,3216.2] environment(u) environment(u) || in_environment(u,end_time(skf2(skc1))) subpopulation(first_movers,u,end_time(skf2(skc1)))* -> . % 13.45/13.74 3219[4:Obv:3218.0] environment(u) || in_environment(u,end_time(skf2(skc1))) subpopulation(first_movers,u,end_time(skf2(skc1)))* -> . % 13.45/13.74 3220[4:MRR:3219.2,13.2] environment(u) || in_environment(u,end_time(skf2(skc1)))* -> . % 13.45/13.74 3237[4:Res:202.2,3220.1] environment(skf2(skc1)) environment(skf2(skc1)) || greater(end_time(skf2(skc1)),start_time(skf2(skc1)))*r -> . % 13.45/13.74 3244[4:Obv:3237.0] environment(skf2(skc1)) || greater(end_time(skf2(skc1)),start_time(skf2(skc1)))*r -> . % 13.45/13.74 3245[4:SSi:3244.0,5.0,2.0,1.0] || greater(end_time(skf2(skc1)),start_time(skf2(skc1)))*r -> . % 13.45/13.74 3258[4:NCh:15.2,15.1,3245.0,53.2] environment(skf2(skc1)) || greater(end_time(skf2(skc1)),critical_point(skf2(skc1))) -> equal(start_time(skf2(skc1)),critical_point(skf2(skc1)))**. % 13.45/13.74 3261[4:SSi:3258.0,5.0,2.0,1.0] || greater(end_time(skf2(skc1)),critical_point(skf2(skc1))) -> equal(start_time(skf2(skc1)),critical_point(skf2(skc1)))**. % 13.45/13.74 3262[4:MRR:3261.0,2640.0] || -> equal(start_time(skf2(skc1)),critical_point(skf2(skc1)))**. % 13.45/13.74 3272[4:Rew:3262.0,3245.0] || greater(end_time(skf2(skc1)),critical_point(skf2(skc1)))*r -> . % 13.45/13.74 3367[4:MRR:3272.0,2640.0] || -> . % 13.45/13.74 3400[4:Spt:3367.0,2830.3,3198.0] || equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero)** -> . % 13.45/13.74 3401[4:Spt:3367.0,2830.0,2830.1,2830.2,2830.4] environment(u) || equal(end_time(u),cardinality_at_time(first_movers,end_time(skf2(skc1))))*+ equal(start_time(u),zero)** -> greater_or_equal(cardinality_at_time(first_movers,cardinality_at_time(first_movers,end_time(skf2(skc1)))),zero)*. % 13.45/13.74 3402[4:MRR:2759.0,3400.0] || -> greater(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero)*l. % 13.45/13.74 3413[4:MRR:2907.3,3400.0] environment(u) || in_environment(u,end_time(skf2(skc1)))* greater(end_time(skf2(skc1)),critical_point(u))+ -> greater(growth_rate(efficient_producers,end_time(skf2(skc1))),growth_rate(first_movers,end_time(skf2(skc1))))*l. % 13.45/13.74 4339[1:Res:2640.0,244.2] environment(skf2(skc1)) environment(skf2(skc1)) || equal(appear(efficient_producers,skf2(skc1)),start_time(skf2(skc1))) -> greater_or_equal(cardinality_at_time(first_movers,appear(efficient_producers,skf2(skc1))),zero)* equal(appear(efficient_producers,skf2(skc1)),critical_point(skf2(skc1))). % 13.45/13.74 4342[1:Obv:4339.0] environment(skf2(skc1)) || equal(appear(efficient_producers,skf2(skc1)),start_time(skf2(skc1))) -> greater_or_equal(cardinality_at_time(first_movers,appear(efficient_producers,skf2(skc1))),zero)* equal(appear(efficient_producers,skf2(skc1)),critical_point(skf2(skc1))). % 13.45/13.74 5244[4:Res:2640.0,3413.2] environment(skf2(skc1)) || in_environment(skf2(skc1),end_time(skf2(skc1)))* -> greater(growth_rate(efficient_producers,end_time(skf2(skc1))),growth_rate(first_movers,end_time(skf2(skc1)))). % 13.77/14.11 5247[4:SSi:5244.0,5.0,2.0,1.0] || in_environment(skf2(skc1),end_time(skf2(skc1)))* -> greater(growth_rate(efficient_producers,end_time(skf2(skc1))),growth_rate(first_movers,end_time(skf2(skc1)))). % 13.77/14.11 5338[1:SSi:4342.0,5.0,2.0,1.0] || equal(appear(efficient_producers,skf2(skc1)),start_time(skf2(skc1))) -> greater_or_equal(cardinality_at_time(first_movers,appear(efficient_producers,skf2(skc1))),zero)* equal(appear(efficient_producers,skf2(skc1)),critical_point(skf2(skc1))). % 13.77/14.11 5450[4:Res:202.2,5247.0] environment(skf2(skc1)) || greater(end_time(skf2(skc1)),start_time(skf2(skc1))) -> greater(growth_rate(efficient_producers,end_time(skf2(skc1))),growth_rate(first_movers,end_time(skf2(skc1))))*l. % 13.77/14.11 5455[4:SSi:5450.0,5.0,2.0,1.0] || greater(end_time(skf2(skc1)),start_time(skf2(skc1))) -> greater(growth_rate(efficient_producers,end_time(skf2(skc1))),growth_rate(first_movers,end_time(skf2(skc1))))*l. % 13.77/14.11 5650[4:Res:5455.1,160.4] environment(u) || greater(end_time(skf2(skc1)),start_time(skf2(skc1))) in_environment(u,end_time(skf2(skc1)))* greater(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero) greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero) -> selection_favors(efficient_producers,first_movers,end_time(skf2(skc1)))*. % 13.77/14.11 5683[4:MRR:5650.3,5650.4,5650.5,3402.0,2906.0,42.0] environment(u) || greater(end_time(skf2(skc1)),start_time(skf2(skc1))) in_environment(u,end_time(skf2(skc1)))* -> . % 13.77/14.11 5691[4:Res:202.2,5683.2] environment(skf2(skc1)) environment(skf2(skc1)) || greater(end_time(skf2(skc1)),start_time(skf2(skc1)))*r greater(end_time(skf2(skc1)),start_time(skf2(skc1)))*r -> . % 13.77/14.11 5697[4:Obv:5691.2] environment(skf2(skc1)) || greater(end_time(skf2(skc1)),start_time(skf2(skc1)))*r -> . % 13.77/14.11 5698[4:SSi:5697.0,5.0,2.0,1.0] || greater(end_time(skf2(skc1)),start_time(skf2(skc1)))*r -> . % 13.77/14.11 5713[4:NCh:15.2,15.1,5698.0,53.2] environment(skf2(skc1)) || greater(end_time(skf2(skc1)),critical_point(skf2(skc1))) -> equal(start_time(skf2(skc1)),critical_point(skf2(skc1)))**. % 13.77/14.11 5717[4:SSi:5713.0,5.0,2.0,1.0] || greater(end_time(skf2(skc1)),critical_point(skf2(skc1))) -> equal(start_time(skf2(skc1)),critical_point(skf2(skc1)))**. % 13.77/14.11 5720[4:MRR:5717.0,2640.0] || -> equal(start_time(skf2(skc1)),critical_point(skf2(skc1)))**. % 13.77/14.11 5726[4:Rew:5720.0,5698.0] || greater(end_time(skf2(skc1)),critical_point(skf2(skc1)))*r -> . % 13.77/14.11 5811[4:MRR:5726.0,2640.0] || -> . % 13.77/14.11 5823[3:Spt:5811.0,2713.1,2906.0] || greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero)*l -> . % 13.77/14.11 5824[3:Spt:5811.0,2713.0,2713.2] || in_environment(skf2(skc1),end_time(skf2(skc1)))* -> equal(appear(efficient_producers,skf2(skc1)),critical_point(skf2(skc1))). % 13.77/14.11 5834[3:Res:202.2,5824.0] environment(skf2(skc1)) || greater(end_time(skf2(skc1)),start_time(skf2(skc1))) -> equal(appear(efficient_producers,skf2(skc1)),critical_point(skf2(skc1)))**. % 13.77/14.11 5839[3:SSi:5834.0,5.0,2.0,1.0] || greater(end_time(skf2(skc1)),start_time(skf2(skc1))) -> equal(appear(efficient_producers,skf2(skc1)),critical_point(skf2(skc1)))**. % 13.77/14.11 6088[4:Spt:5338.2] || -> equal(appear(efficient_producers,skf2(skc1)),critical_point(skf2(skc1)))**. % 13.77/14.11 6100[4:SpL:6088.0,88.1] environment(skf2(skc1)) || greater(u,critical_point(skf2(skc1))) in_environment(skf2(skc1),u)* -> greater(cardinality_at_time(efficient_producers,u),zero). % 13.77/14.11 6116[4:SSi:6100.0,5.0,2.0,1.0] || greater(u,critical_point(skf2(skc1))) in_environment(skf2(skc1),u)* -> greater(cardinality_at_time(efficient_producers,u),zero). % 13.77/14.11 6209[4:Res:202.2,6116.1] environment(skf2(skc1)) || greater(end_time(skf2(skc1)),start_time(skf2(skc1))) greater(end_time(skf2(skc1)),critical_point(skf2(skc1))) -> greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero)*l. % 13.77/14.11 6218[4:SSi:6209.0,5.0,2.0,1.0] || greater(end_time(skf2(skc1)),start_time(skf2(skc1))) greater(end_time(skf2(skc1)),critical_point(skf2(skc1))) -> greater(cardinality_at_time(efficient_producers,end_time(skf2(skc1))),zero)*l. % 13.77/14.11 6219[4:MRR:6218.1,6218.2,2640.0,5823.0] || greater(end_time(skf2(skc1)),start_time(skf2(skc1)))*r -> . % 13.77/14.11 6235[4:NCh:15.2,15.1,6219.0,53.2] environment(skf2(skc1)) || greater(end_time(skf2(skc1)),critical_point(skf2(skc1))) -> equal(start_time(skf2(skc1)),critical_point(skf2(skc1)))**. % 13.77/14.11 6237[4:SSi:6235.0,5.0,2.0,1.0] || greater(end_time(skf2(skc1)),critical_point(skf2(skc1))) -> equal(start_time(skf2(skc1)),critical_point(skf2(skc1)))**. % 13.77/14.11 6238[4:MRR:6237.0,2640.0] || -> equal(start_time(skf2(skc1)),critical_point(skf2(skc1)))**. % 13.77/14.11 6243[4:Rew:6238.0,6219.0] || greater(end_time(skf2(skc1)),critical_point(skf2(skc1)))*r -> . % 13.77/14.11 6281[4:MRR:6243.0,2640.0] || -> . % 13.77/14.11 6296[4:Spt:6281.0,5338.2,6088.0] || equal(appear(efficient_producers,skf2(skc1)),critical_point(skf2(skc1)))** -> . % 13.77/14.11 6297[4:Spt:6281.0,5338.0,5338.1] || equal(appear(efficient_producers,skf2(skc1)),start_time(skf2(skc1))) -> greater_or_equal(cardinality_at_time(first_movers,appear(efficient_producers,skf2(skc1))),zero)*. % 13.77/14.11 6300[4:MRR:5839.1,6296.0] || greater(end_time(skf2(skc1)),start_time(skf2(skc1)))*r -> . % 13.77/14.11 6332[4:NCh:15.2,15.1,6300.0,53.2] environment(skf2(skc1)) || greater(end_time(skf2(skc1)),critical_point(skf2(skc1))) -> equal(start_time(skf2(skc1)),critical_point(skf2(skc1)))**. % 13.77/14.11 6335[4:SSi:6332.0,5.0,2.0,1.0] || greater(end_time(skf2(skc1)),critical_point(skf2(skc1))) -> equal(start_time(skf2(skc1)),critical_point(skf2(skc1)))**. % 13.77/14.11 6336[4:MRR:6335.0,2640.0] || -> equal(start_time(skf2(skc1)),critical_point(skf2(skc1)))**. % 13.77/14.11 6340[4:Rew:6336.0,6300.0] || greater(end_time(skf2(skc1)),critical_point(skf2(skc1)))*r -> . % 13.77/14.11 6367[4:MRR:6340.0,2640.0] || -> . % 13.77/14.11 6377[2:Spt:6367.0,2708.0,2758.0] || greater_or_equal(cardinality_at_time(first_movers,end_time(skf2(skc1))),zero)* -> . % 13.77/14.11 6378[2:Spt:6367.0,2708.1] || -> equal(start_time(skf2(skc1)),critical_point(skf2(skc1)))**. % 13.77/14.11 6454[2:Res:217.2,6377.0] environment(skf2(skc1)) || greater(end_time(skf2(skc1)),start_time(skf2(skc1)))*r -> . % 13.77/14.11 6458[2:Rew:6378.0,6454.1] environment(skf2(skc1)) || greater(end_time(skf2(skc1)),critical_point(skf2(skc1)))*r -> . % 13.77/14.11 6459[2:SSi:6458.0,5.0,2.0,1.0] || greater(end_time(skf2(skc1)),critical_point(skf2(skc1)))*r -> . % 13.77/14.11 6460[2:MRR:6459.0,2640.0] || -> . % 13.77/14.11 % SZS output end Refutation % 13.77/14.11 Formulae used in the proof : prove_t8 mp_organizational_sets1 mp_organizational_sets2 mp3_favoured_trategy mp_greater_or_equal mp_time_of_critical_point mp_critical_point_after_EP mp_environment_end_point mp_subpopulations mp_greater_transitivity mp_first_movers_exist mp_time_in_environment mp4_critical_point t6 d1 mp1_high_growth_rates mp_contains_FM_and_EP mp2_favour_members % 13.77/14.11 %------------------------------------------------------------------------------