%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT027+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.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 : Theorem 0.64s 0.95s % Output : Refutation 0.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : MGT027+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.06 % Command : run_spass %d %s % 0.16/0.43 % Computer : n019.cluster.edu % 0.16/0.43 % Model : x86_64 x86_64 % 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.43 % Memory : 8046.5625MB % 0.16/0.43 % OS : Linux 6.8.0-71-generic % 0.16/0.43 % CPULimit : 300 % 0.16/0.44 % WCLimit : 300 % 0.16/0.44 % DateTime : Mon Sep 7 12:13:22 UTC 2026 % 0.16/0.44 % CPUTime : % 0.64/0.95 % 0.64/0.95 SPASS V 3.9 % 0.64/0.95 SPASS beiseite: Proof found. % 0.64/0.95 % SZS status Theorem % 0.64/0.95 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.64/0.95 SPASS derived 650 clauses, backtracked 91 clauses, performed 7 splits and kept 443 clauses. % 0.64/0.95 SPASS allocated 98466 KBytes. % 0.64/0.95 SPASS spent 0:00:00.50 on the problem. % 0.64/0.95 0:00:00.09 for the input. % 0.64/0.95 0:00:00.07 for the FLOTTER CNF translation. % 0.64/0.95 0:00:00.03 for inferences. % 0.64/0.95 0:00:00.00 for the backtracking. % 0.64/0.95 0:00:00.23 for the reduction. % 0.64/0.95 % 0.64/0.95 % 0.64/0.95 Here is a proof with depth 9, length 112 : % 0.64/0.95 % SZS output start Refutation % 0.64/0.95 1[0:Inp] || -> environment(skc1)*. % 0.64/0.95 2[0:Inp] || -> stable(skc1)*. % 0.64/0.95 3[0:Inp] || -> greater(cardinality_at_time(first_movers,skf2(u)),zero)*l. % 0.64/0.95 4[0:Inp] || greater(u,v) -> greater_or_equal(u,v)*. % 0.64/0.95 6[0:Inp] || contracts_from(u,first_movers)* greater(u,appear(efficient_producers,skc1))*+ -> . % 0.64/0.95 7[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 0.64/0.95 8[0:Inp] stable(u) environment(u) || -> in_environment(u,appear(efficient_producers,u))*. % 0.64/0.95 9[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.64/0.95 10[0:Inp] stable(u) environment(u) || -> greater(skf4(u),appear(efficient_producers,u))*r. % 0.64/0.95 11[0:Inp] stable(u) environment(u) || in_environment(u,v)*+ -> contracts_from(v,first_movers) greater_or_equal(skf2(v),v)*. % 0.64/0.95 12[0:Inp] stable(u) environment(u) || greater(v,w)*+ in_environment(u,w)* -> in_environment(u,v)*. % 0.64/0.95 13[0:Inp] environment(u) || in_environment(u,v) greater_or_equal(v,appear(efficient_producers,u))* -> greater(cardinality_at_time(efficient_producers,v),zero). % 0.64/0.95 14[0:Inp] stable(u) environment(u) || in_environment(u,v)* greater(zero,growth_rate(first_movers,skf2(v)))*r+ -> contracts_from(v,first_movers). % 0.64/0.95 15[0:Inp] stable(u) environment(u) || greater_or_equal(v,skf4(u)) subpopulations(first_movers,efficient_producers,u,v)* -> greater(zero,growth_rate(first_movers,v)). % 0.64/0.95 16[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)*. % 0.64/0.95 19[0:Res:2.0,12.1] environment(skc1) || in_environment(skc1,u)* greater(v,u)* -> in_environment(skc1,v)*. % 0.64/0.95 20[0:Res:2.0,10.1] environment(skc1) || -> greater(skf4(skc1),appear(efficient_producers,skc1))*r. % 0.64/0.95 22[0:Res:2.0,8.1] environment(skc1) || -> in_environment(skc1,appear(efficient_producers,skc1))*. % 0.64/0.95 25[0:Res:1.0,14.0] stable(skc1) || greater(zero,growth_rate(first_movers,skf2(u)))*r in_environment(skc1,u) -> contracts_from(u,first_movers). % 0.64/0.95 31[0:MRR:22.0,1.0] || -> in_environment(skc1,appear(efficient_producers,skc1))*. % 0.64/0.95 32[0:MRR:20.0,1.0] || -> greater(skf4(skc1),appear(efficient_producers,skc1))*r. % 0.64/0.95 34[0:MRR:19.0,1.0] || greater(u,v)*+ in_environment(skc1,v)* -> in_environment(skc1,u)*. % 0.64/0.95 35[0:MRR:25.0,2.0] || in_environment(skc1,u) greater(zero,growth_rate(first_movers,skf2(u)))*r -> contracts_from(u,first_movers). % 0.64/0.95 37[0:Res:32.0,6.0] || contracts_from(skf4(skc1),first_movers)* -> . % 0.64/0.95 41[0:NCh:9.2,9.1,6.1,32.0] || contracts_from(u,first_movers)* greater(u,skf4(skc1)) -> . % 0.64/0.95 42[0:NCh:9.2,9.1,6.1,32.0] || contracts_from(u,first_movers)* equal(u,skf4(skc1)) -> . % 0.64/0.95 46[0:Res:32.0,34.0] || in_environment(skc1,appear(efficient_producers,skc1))* -> in_environment(skc1,skf4(skc1)). % 0.64/0.95 50[0:NCh:9.2,9.1,34.0,32.0] || greater(u,skf4(skc1)) in_environment(skc1,appear(efficient_producers,skc1))* -> in_environment(skc1,u)*. % 0.64/0.95 51[0:NCh:9.2,9.1,34.0,32.0] || equal(u,skf4(skc1)) in_environment(skc1,appear(efficient_producers,skc1))* -> in_environment(skc1,u)*. % 0.64/0.95 52[0:MRR:46.0,31.0] || -> in_environment(skc1,skf4(skc1))*. % 0.64/0.95 53[0:MRR:51.1,31.0] || equal(u,skf4(skc1)) -> in_environment(skc1,u)*. % 0.64/0.95 54[0:MRR:50.1,31.0] || greater(u,skf4(skc1)) -> in_environment(skc1,u)*. % 0.64/0.95 69[0:Res:54.1,11.2] stable(skc1) environment(skc1) || greater(u,skf4(skc1)) -> contracts_from(u,first_movers) greater_or_equal(skf2(u),u)*. % 0.64/0.95 70[0:Res:53.1,11.2] stable(skc1) environment(skc1) || equal(u,skf4(skc1)) -> contracts_from(u,first_movers) greater_or_equal(skf2(u),u)*. % 0.64/0.95 71[0:Res:52.0,11.2] stable(skc1) environment(skc1) || -> contracts_from(skf4(skc1),first_movers) greater_or_equal(skf2(skf4(skc1)),skf4(skc1))*. % 0.64/0.95 74[0:SSi:71.1,71.0,2.0,1.0,2.0,1.0] || -> contracts_from(skf4(skc1),first_movers) greater_or_equal(skf2(skf4(skc1)),skf4(skc1))*. % 0.64/0.95 75[0:MRR:74.0,37.0] || -> greater_or_equal(skf2(skf4(skc1)),skf4(skc1))*. % 0.64/0.95 76[0:SSi:70.1,70.0,2.0,1.0,2.0,1.0] || equal(u,skf4(skc1)) -> contracts_from(u,first_movers) greater_or_equal(skf2(u),u)*. % 0.64/0.95 77[0:MRR:76.1,42.0] || equal(u,skf4(skc1)) -> greater_or_equal(skf2(u),u)*. % 0.64/0.95 79[0:SSi:69.1,69.0,2.0,1.0,2.0,1.0] || greater(u,skf4(skc1)) -> contracts_from(u,first_movers) greater_or_equal(skf2(u),u)*. % 0.64/0.95 80[0:MRR:79.1,41.0] || greater(u,skf4(skc1)) -> greater_or_equal(skf2(u),u)*. % 0.64/0.95 84[0:Res:75.0,7.0] || -> equal(skf2(skf4(skc1)),skf4(skc1)) greater(skf2(skf4(skc1)),skf4(skc1))*l. % 0.64/0.95 85[0:Res:77.1,7.0] || equal(u,skf4(skc1))*+ -> equal(skf2(u),u) greater(skf2(u),u)*l. % 0.64/0.95 87[0:Res:80.1,7.0] || greater(u,skf4(skc1))*+ -> equal(skf2(u),u) greater(skf2(u),u)*l. % 0.64/0.95 104[0:Res:84.1,34.0] || in_environment(skc1,skf4(skc1)) -> equal(skf2(skf4(skc1)),skf4(skc1)) in_environment(skc1,skf2(skf4(skc1)))*. % 0.64/0.95 110[0:MRR:104.0,104.1,52.0,53.0] || -> in_environment(skc1,skf2(skf4(skc1)))*. % 0.64/0.95 111[0:Res:110.0,11.2] stable(skc1) environment(skc1) || -> contracts_from(skf2(skf4(skc1)),first_movers) greater_or_equal(skf2(skf2(skf4(skc1))),skf2(skf4(skc1)))*. % 0.64/0.95 112[0:SSi:111.1,111.0,2.0,1.0,2.0,1.0] || -> contracts_from(skf2(skf4(skc1)),first_movers) greater_or_equal(skf2(skf2(skf4(skc1))),skf2(skf4(skc1)))*. % 0.64/0.95 113[0:Res:4.1,13.2] environment(u) || greater(v,appear(efficient_producers,u))*+ in_environment(u,v)* -> greater(cardinality_at_time(efficient_producers,v),zero)*l. % 0.64/0.95 153[0:Res:16.4,15.3] environment(u) stable(u) environment(u) || in_environment(u,v) greater(cardinality_at_time(first_movers,v),zero) greater(cardinality_at_time(efficient_producers,v),zero) greater_or_equal(v,skf4(u))* -> greater(zero,growth_rate(first_movers,v)). % 0.64/0.95 154[0:Obv:153.0] stable(u) environment(u) || in_environment(u,v) greater(cardinality_at_time(first_movers,v),zero) greater(cardinality_at_time(efficient_producers,v),zero) greater_or_equal(v,skf4(u))* -> greater(zero,growth_rate(first_movers,v)). % 0.64/0.95 250[0:NCh:9.2,9.1,113.1,32.0] environment(skc1) || greater(u,skf4(skc1)) in_environment(skc1,u) -> greater(cardinality_at_time(efficient_producers,u),zero)*l. % 0.64/0.95 251[0:NCh:9.2,9.1,113.1,32.0] environment(skc1) || equal(u,skf4(skc1)) in_environment(skc1,u) -> greater(cardinality_at_time(efficient_producers,u),zero)*l. % 0.64/0.95 252[0:NCh:9.2,9.1,113.1,10.2] environment(u) stable(u) environment(u) || greater(v,skf4(u)) in_environment(u,v)* -> greater(cardinality_at_time(efficient_producers,v),zero)*l. % 0.64/0.95 256[0:SSi:251.0,2.0,1.0] || equal(u,skf4(skc1)) in_environment(skc1,u) -> greater(cardinality_at_time(efficient_producers,u),zero)*l. % 0.64/0.95 257[0:MRR:256.1,53.1] || equal(u,skf4(skc1)) -> greater(cardinality_at_time(efficient_producers,u),zero)*l. % 0.64/0.95 260[0:SSi:250.0,2.0,1.0] || greater(u,skf4(skc1)) in_environment(skc1,u) -> greater(cardinality_at_time(efficient_producers,u),zero)*l. % 0.64/0.95 261[0:MRR:260.1,54.1] || greater(u,skf4(skc1)) -> greater(cardinality_at_time(efficient_producers,u),zero)*l. % 0.64/0.95 264[0:Obv:252.0] stable(u) environment(u) || greater(v,skf4(u))+ in_environment(u,v)* -> greater(cardinality_at_time(efficient_producers,v),zero)*l. % 0.64/0.95 350[0:Res:75.0,154.5] stable(skc1) environment(skc1) || in_environment(skc1,skf2(skf4(skc1))) greater(cardinality_at_time(first_movers,skf2(skf4(skc1))),zero) greater(cardinality_at_time(efficient_producers,skf2(skf4(skc1))),zero) -> greater(zero,growth_rate(first_movers,skf2(skf4(skc1))))*r. % 0.64/0.95 354[0:SSi:350.1,350.0,2.0,1.0,2.0,1.0] || in_environment(skc1,skf2(skf4(skc1))) greater(cardinality_at_time(first_movers,skf2(skf4(skc1))),zero) greater(cardinality_at_time(efficient_producers,skf2(skf4(skc1))),zero) -> greater(zero,growth_rate(first_movers,skf2(skf4(skc1))))*r. % 0.64/0.95 355[0:MRR:354.0,354.1,110.0,3.0] || greater(cardinality_at_time(efficient_producers,skf2(skf4(skc1))),zero) -> greater(zero,growth_rate(first_movers,skf2(skf4(skc1))))*r. % 0.64/0.95 502[0:Res:84.1,87.0] || -> equal(skf2(skf4(skc1)),skf4(skc1)) equal(skf2(skf2(skf4(skc1))),skf2(skf4(skc1))) greater(skf2(skf2(skf4(skc1))),skf2(skf4(skc1)))*l. % 0.64/0.97 519[0:MRR:502.0,85.0] || -> equal(skf2(skf2(skf4(skc1))),skf2(skf4(skc1))) greater(skf2(skf2(skf4(skc1))),skf2(skf4(skc1)))*l. % 0.64/0.97 521[0:Res:519.1,34.0] || in_environment(skc1,skf2(skf4(skc1))) -> equal(skf2(skf2(skf4(skc1))),skf2(skf4(skc1))) in_environment(skc1,skf2(skf2(skf4(skc1))))*. % 0.64/0.97 527[0:NCh:9.2,9.0,519.1,6.1] || contracts_from(skf2(skf2(skf4(skc1))),first_movers)* greater(skf2(skf4(skc1)),appear(efficient_producers,skc1)) -> equal(skf2(skf2(skf4(skc1))),skf2(skf4(skc1))). % 0.64/0.97 543[0:MRR:521.0,110.0] || -> equal(skf2(skf2(skf4(skc1))),skf2(skf4(skc1))) in_environment(skc1,skf2(skf2(skf4(skc1))))*. % 0.64/0.97 546[1:Spt:543.0] || -> equal(skf2(skf2(skf4(skc1))),skf2(skf4(skc1)))**. % 0.64/0.97 547[1:Rew:546.0,112.1] || -> contracts_from(skf2(skf4(skc1)),first_movers) greater_or_equal(skf2(skf4(skc1)),skf2(skf4(skc1)))*. % 0.64/0.97 556[1:SpL:546.0,35.1] || in_environment(skc1,skf2(skf4(skc1))) greater(zero,growth_rate(first_movers,skf2(skf4(skc1))))*r -> contracts_from(skf2(skf4(skc1)),first_movers). % 0.64/0.97 558[1:MRR:556.0,110.0] || greater(zero,growth_rate(first_movers,skf2(skf4(skc1))))*r -> contracts_from(skf2(skf4(skc1)),first_movers). % 0.64/0.97 564[2:Spt:547.0] || -> contracts_from(skf2(skf4(skc1)),first_movers)*. % 0.64/0.97 565[2:Res:564.0,41.0] || greater(skf2(skf4(skc1)),skf4(skc1))*l -> . % 0.64/0.97 566[2:Res:564.0,42.0] || equal(skf2(skf4(skc1)),skf4(skc1))** -> . % 0.64/0.97 567[2:MRR:84.0,566.0] || -> greater(skf2(skf4(skc1)),skf4(skc1))*l. % 0.64/0.97 573[2:MRR:565.0,567.0] || -> . % 0.64/0.97 574[2:Spt:573.0,547.0,564.0] || contracts_from(skf2(skf4(skc1)),first_movers)* -> . % 0.64/0.97 575[2:Spt:573.0,547.1] || -> greater_or_equal(skf2(skf4(skc1)),skf2(skf4(skc1)))*. % 0.64/0.97 576[2:MRR:558.1,574.0] || greater(zero,growth_rate(first_movers,skf2(skf4(skc1))))*r -> . % 0.64/0.97 577[2:MRR:355.1,576.0] || greater(cardinality_at_time(efficient_producers,skf2(skf4(skc1))),zero)*l -> . % 0.64/0.97 581[2:Res:257.1,577.0] || equal(skf2(skf4(skc1)),skf4(skc1))** -> . % 0.64/0.97 583[2:NCh:9.2,9.0,577.0,261.1] || equal(zero,zero) greater(skf2(skf4(skc1)),skf4(skc1))*l -> . % 0.64/0.97 586[2:MRR:84.0,581.0] || -> greater(skf2(skf4(skc1)),skf4(skc1))*l. % 0.64/0.97 593[2:Obv:583.0] || greater(skf2(skf4(skc1)),skf4(skc1))*l -> . % 0.64/0.97 594[2:MRR:593.0,586.0] || -> . % 0.64/0.97 596[1:Spt:594.0,543.0,546.0] || equal(skf2(skf2(skf4(skc1))),skf2(skf4(skc1)))** -> . % 0.64/0.97 597[1:Spt:594.0,543.1] || -> in_environment(skc1,skf2(skf2(skf4(skc1))))*. % 0.64/0.97 601[1:MRR:527.2,596.0] || contracts_from(skf2(skf2(skf4(skc1))),first_movers)* greater(skf2(skf4(skc1)),appear(efficient_producers,skc1)) -> . % 0.64/0.97 616[1:Res:597.0,11.2] stable(skc1) environment(skc1) || -> contracts_from(skf2(skf2(skf4(skc1))),first_movers) greater_or_equal(skf2(skf2(skf2(skf4(skc1)))),skf2(skf2(skf4(skc1))))*. % 0.64/0.97 617[1:SSi:616.1,616.0,2.0,1.0,2.0,1.0] || -> contracts_from(skf2(skf2(skf4(skc1))),first_movers) greater_or_equal(skf2(skf2(skf2(skf4(skc1)))),skf2(skf2(skf4(skc1))))*. % 0.64/0.97 643[2:Spt:617.0] || -> contracts_from(skf2(skf2(skf4(skc1))),first_movers)*. % 0.64/0.97 645[2:MRR:601.0,643.0] || greater(skf2(skf4(skc1)),appear(efficient_producers,skc1))*r -> . % 0.64/0.97 656[2:NCh:9.2,9.1,645.0,32.0] || equal(skf2(skf4(skc1)),skf4(skc1))** -> . % 0.64/0.97 657[2:NCh:9.2,9.1,645.0,10.2] stable(skc1) environment(skc1) || greater(skf2(skf4(skc1)),skf4(skc1))*l -> . % 0.64/0.97 659[2:MRR:84.0,656.0] || -> greater(skf2(skf4(skc1)),skf4(skc1))*l. % 0.64/0.97 668[2:SSi:657.1,657.0,2.0,1.0,2.0,1.0] || greater(skf2(skf4(skc1)),skf4(skc1))*l -> . % 0.64/0.97 669[2:MRR:668.0,659.0] || -> . % 0.64/0.97 670[2:Spt:669.0,617.0,643.0] || contracts_from(skf2(skf2(skf4(skc1))),first_movers)* -> . % 0.64/0.97 671[2:Spt:669.0,617.1] || -> greater_or_equal(skf2(skf2(skf2(skf4(skc1)))),skf2(skf2(skf4(skc1))))*. % 0.64/0.97 684[3:Spt:84.0] || -> equal(skf2(skf4(skc1)),skf4(skc1))**. % 0.64/0.97 696[3:Rew:684.0,596.0] || equal(skf2(skf4(skc1)),skf4(skc1))** -> . % 0.64/0.97 717[3:Rew:684.0,696.0] || equal(skf4(skc1),skf4(skc1))* -> . % 0.64/0.97 718[3:Obv:717.0] || -> . % 0.64/0.97 730[3:Spt:718.0,84.0,684.0] || equal(skf2(skf4(skc1)),skf4(skc1))** -> . % 0.64/0.97 731[3:Spt:718.0,84.1] || -> greater(skf2(skf4(skc1)),skf4(skc1))*l. % 0.64/0.97 769[3:Res:731.0,264.2] stable(skc1) environment(skc1) || in_environment(skc1,skf2(skf4(skc1))) -> greater(cardinality_at_time(efficient_producers,skf2(skf4(skc1))),zero)*l. % 0.64/0.97 786[3:SSi:769.1,769.0,2.0,1.0,2.0,1.0] || in_environment(skc1,skf2(skf4(skc1))) -> greater(cardinality_at_time(efficient_producers,skf2(skf4(skc1))),zero)*l. % 0.64/0.97 787[3:MRR:786.0,110.0] || -> greater(cardinality_at_time(efficient_producers,skf2(skf4(skc1))),zero)*l. % 0.64/0.97 788[3:MRR:355.0,787.0] || -> greater(zero,growth_rate(first_movers,skf2(skf4(skc1))))*r. % 0.64/0.97 828[3:NCh:9.2,9.1,788.0,35.1] || in_environment(skc1,skf4(skc1)) equal(zero,zero) -> contracts_from(skf4(skc1),first_movers)*. % 0.64/0.97 842[3:Obv:828.1] || in_environment(skc1,skf4(skc1)) -> contracts_from(skf4(skc1),first_movers)*. % 0.64/0.97 843[3:MRR:842.0,842.1,52.0,37.0] || -> . % 0.64/0.97 % SZS output end Refutation % 0.64/0.97 Formulae used in the proof : prove_l9 mp_contracts_from l10 mp_EP_in_stable_environments mp_long_stable_environments mp_greater_or_equal mp_greater_transitivity t6 mp_non_empty_fm_and_ep % 0.64/0.97 %------------------------------------------------------------------------------