%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT031+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n011.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:50 AM UTC 2026 % Result : CounterSatisfiable 0.33s 0.58s % Output : Saturation 0.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT031+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.04 % Command : run_spass %d %s % 0.09/0.35 % Computer : n011.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Mon Sep 7 12:20:15 UTC 2026 % 0.09/0.36 % CPUTime : % 0.33/0.58 % 0.33/0.58 SPASS V 3.9 % 0.33/0.58 SPASS beiseite: Completion found. % 0.33/0.58 % SZS status CounterSatisfiable % 0.33/0.58 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.33/0.58 SPASS derived 269 clauses, backtracked 0 clauses, performed 1 splits and kept 125 clauses. % 0.33/0.58 SPASS allocated 98001 KBytes. % 0.33/0.58 SPASS spent 0:00:00.21 on the problem. % 0.33/0.58 0:00:00.06 for the input. % 0.33/0.58 0:00:00.05 for the FLOTTER CNF translation. % 0.33/0.58 0:00:00.01 for inferences. % 0.33/0.58 0:00:00.00 for the backtracking. % 0.33/0.58 0:00:00.04 for the reduction. % 0.33/0.58 % 0.33/0.58 % 0.33/0.58 The saturated set of worked-off clauses is : % 0.33/0.58 % SZS output start Saturation % 0.33/0.58 10[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.33/0.58 289[0:Res:178.3,131.4] environment(u) environment(v) || greater(number_of_organizations(skc1,appear(first_movers,v)),zero)*l+ in_environment(skc1,appear(first_movers,v)) greater(appear(an_organisation,skc1),appear(first_movers,v)) in_environment(u,appear(first_movers,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 290[0:Res:178.3,133.4] environment(u) environment(v) || greater(number_of_organizations(skc1,appear(an_organisation,v)),zero)*l+ in_environment(skc1,appear(an_organisation,v)) greater(appear(an_organisation,skc1),appear(an_organisation,v)) in_environment(u,appear(an_organisation,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 271[0:Res:179.3,131.4] environment(u) environment(v) || greater(number_of_organizations(skc1,appear(first_movers,v)),zero)*l+ in_environment(skc1,appear(first_movers,v)) greater(appear(first_movers,skc1),appear(first_movers,v)) in_environment(u,appear(first_movers,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 272[0:Res:179.3,133.4] environment(u) environment(v) || greater(number_of_organizations(skc1,appear(an_organisation,v)),zero)*l+ in_environment(skc1,appear(an_organisation,v)) greater(appear(first_movers,skc1),appear(an_organisation,v)) in_environment(u,appear(an_organisation,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 404[0:Obv:397.0] environment(u) environment(v) || greater(number_of_organizations(skc1,appear(an_organisation,v)),zero)*l+ in_environment(skc1,appear(an_organisation,v)) greater(appear(an_organisation,skc1),appear(efficient_producers,e)) in_environment(u,appear(an_organisation,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 390[0:Obv:380.0] environment(u) environment(v) || greater(number_of_organizations(skc1,appear(first_movers,v)),zero)*l+ in_environment(skc1,appear(first_movers,v)) greater(appear(an_organisation,skc1),appear(efficient_producers,e)) in_environment(u,appear(first_movers,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 388[0:SSi:379.0,1.0] environment(u) || greater(number_of_organizations(skc1,appear(first_movers,skc1)),zero)*l+ in_environment(skc1,appear(first_movers,skc1)) greater(appear(an_organisation,skc1),appear(efficient_producers,e)) in_environment(u,appear(first_movers,skc1))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 288[0:Res:178.3,129.3] environment(u) || greater(number_of_organizations(skc1,appear(first_movers,skc1)),zero)*l+ in_environment(skc1,appear(first_movers,skc1)) greater(appear(an_organisation,skc1),appear(first_movers,skc1)) in_environment(u,appear(first_movers,skc1))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 346[0:Res:162.1,269.4] environment(u) environment(v) || greater(number_of_organizations(skc1,appear(an_organisation,v)),zero)+ in_environment(u,appear(an_organisation,v))* equal(appear(an_organisation,u),appear(efficient_producers,e)) -> greater(cardinality_at_time(efficient_producers,appear(an_organisation,v)),zero)*l equal(appear(first_movers,u),appear(an_organisation,u)). % 0.33/0.58 270[0:Res:179.3,129.3] environment(u) || greater(number_of_organizations(skc1,appear(first_movers,skc1)),zero)*l+ in_environment(skc1,appear(first_movers,skc1)) greater(appear(first_movers,skc1),appear(first_movers,skc1)) in_environment(u,appear(first_movers,skc1))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 403[0:Obv:398.2] environment(u) || greater(number_of_organizations(skc1,appear(an_organisation,u)),zero)*l greater(appear(an_organisation,skc1),appear(efficient_producers,e)) in_environment(skc1,appear(an_organisation,u)) greater(appear(efficient_producers,skc1),appear(an_organisation,u)) -> . % 0.33/0.58 389[0:Obv:381.2] environment(u) || greater(number_of_organizations(skc1,appear(first_movers,u)),zero)*l greater(appear(an_organisation,skc1),appear(efficient_producers,e)) in_environment(skc1,appear(first_movers,u)) greater(appear(efficient_producers,skc1),appear(first_movers,u)) -> . % 0.33/0.58 242[0:Res:180.3,133.4] environment(u) environment(v) || greater(number_of_organizations(skc1,appear(an_organisation,v)),zero)*l+ in_environment(skc1,appear(an_organisation,v)) equal(appear(an_organisation,skc1),appear(an_organisation,v)) in_environment(u,appear(an_organisation,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 332[0:Res:162.1,213.4] environment(u) environment(v) || greater(number_of_organizations(skc1,appear(first_movers,u)),zero)+ in_environment(v,appear(first_movers,u))* equal(appear(an_organisation,v),appear(efficient_producers,e)) -> greater(cardinality_at_time(efficient_producers,appear(first_movers,u)),zero)*l equal(appear(first_movers,v),appear(an_organisation,v)). % 0.33/0.58 220[0:Res:180.3,131.4] environment(u) environment(v) || greater(number_of_organizations(skc1,appear(first_movers,v)),zero)*l+ in_environment(skc1,appear(first_movers,v)) equal(appear(first_movers,v),appear(an_organisation,skc1)) in_environment(u,appear(first_movers,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 374[0:Obv:367.0] environment(u) environment(v) || greater(number_of_organizations(skc1,appear(an_organisation,v)),zero)*l+ in_environment(skc1,appear(an_organisation,v)) equal(appear(efficient_producers,e),appear(an_organisation,skc1)) in_environment(u,appear(an_organisation,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 361[0:Obv:351.0] environment(u) environment(v) || greater(number_of_organizations(skc1,appear(first_movers,v)),zero)*l+ in_environment(skc1,appear(first_movers,v)) equal(appear(efficient_producers,e),appear(an_organisation,skc1)) in_environment(u,appear(first_movers,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 340[0:Res:162.1,329.3] environment(u) || greater(number_of_organizations(skc1,appear(an_organisation,u)),zero) in_environment(skc1,appear(an_organisation,u)) greater(appear(an_organisation,skc1),appear(efficient_producers,e)) -> greater(cardinality_at_time(efficient_producers,appear(an_organisation,u)),zero)*l. % 0.33/0.58 396[1:Spt:320.0,320.2,320.3,320.5] environment(u) || in_environment(u,appear(first_movers,skc1))* equal(appear(an_organisation,u),appear(efficient_producers,e)) -> equal(appear(first_movers,u),appear(an_organisation,u)). % 0.33/0.58 260[0:Res:162.1,212.3] environment(u) || greater(number_of_organizations(skc1,appear(first_movers,u)),zero) in_environment(skc1,appear(first_movers,u)) greater(appear(an_organisation,skc1),appear(efficient_producers,e)) -> greater(cardinality_at_time(efficient_producers,appear(first_movers,u)),zero)*l. % 0.33/0.58 237[0:Res:162.1,99.4] environment(u) environment(v) || greater(number_of_organizations(skc1,appear(an_organisation,v)),zero)+ in_environment(u,appear(an_organisation,v))* equal(appear(first_movers,u),appear(efficient_producers,e)) -> greater(cardinality_at_time(efficient_producers,appear(an_organisation,v)),zero)*l. % 0.33/0.58 176[0:Res:162.1,97.4] environment(u) environment(v) || greater(number_of_organizations(skc1,appear(first_movers,v)),zero)+ in_environment(u,appear(first_movers,v))* equal(appear(first_movers,u),appear(efficient_producers,e)) -> greater(cardinality_at_time(efficient_producers,appear(first_movers,v)),zero)*l. % 0.33/0.58 359[0:SSi:350.0,1.0] environment(u) || greater(number_of_organizations(skc1,appear(first_movers,skc1)),zero)*l+ in_environment(skc1,appear(first_movers,skc1)) equal(appear(efficient_producers,e),appear(an_organisation,skc1)) in_environment(u,appear(first_movers,skc1))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 268[0:NCh:10.2,10.1,106.2,54.1] environment(u) environment(v) || in_environment(u,appear(an_organisation,v))* greater(appear(an_organisation,u),appear(efficient_producers,e))+ greater(cardinality_at_time(first_movers,appear(an_organisation,v)),zero)*l -> equal(appear(first_movers,u),appear(an_organisation,u)). % 0.33/0.58 373[0:Obv:368.2] environment(u) || greater(number_of_organizations(skc1,appear(an_organisation,u)),zero)*l equal(appear(efficient_producers,e),appear(an_organisation,skc1)) in_environment(skc1,appear(an_organisation,u)) greater(appear(efficient_producers,skc1),appear(an_organisation,u)) -> . % 0.33/0.58 360[0:Obv:352.2] environment(u) || greater(number_of_organizations(skc1,appear(first_movers,u)),zero)*l equal(appear(efficient_producers,e),appear(an_organisation,skc1)) in_environment(skc1,appear(first_movers,u)) greater(appear(efficient_producers,skc1),appear(first_movers,u)) -> . % 0.33/0.58 336[0:Res:162.1,328.3] environment(u) || greater(number_of_organizations(skc1,appear(an_organisation,u)),zero) in_environment(skc1,appear(an_organisation,u)) equal(appear(efficient_producers,e),appear(an_organisation,skc1)) -> greater(cardinality_at_time(efficient_producers,appear(an_organisation,u)),zero)*l. % 0.33/0.58 215[0:Res:162.1,211.3] environment(u) || greater(number_of_organizations(skc1,appear(first_movers,u)),zero) in_environment(skc1,appear(first_movers,u)) equal(appear(efficient_producers,e),appear(an_organisation,skc1)) -> greater(cardinality_at_time(efficient_producers,appear(first_movers,u)),zero)*l. % 0.33/0.58 259[0:Obv:256.0] environment(u) || in_environment(u,appear(first_movers,skc1))* greater(appear(an_organisation,u),appear(efficient_producers,e))+ greater(cardinality_at_time(first_movers,appear(first_movers,skc1)),zero)*l -> equal(appear(first_movers,u),appear(an_organisation,u)). % 0.33/0.58 177[0:Res:162.1,95.3] environment(u) || greater(number_of_organizations(skc1,appear(first_movers,skc1)),zero)+ in_environment(u,appear(first_movers,skc1))* equal(appear(first_movers,u),appear(efficient_producers,e)) -> greater(cardinality_at_time(efficient_producers,appear(first_movers,skc1)),zero)*l. % 0.33/0.58 233[0:Res:162.1,105.3] environment(u) || greater(number_of_organizations(skc1,v),zero)+ in_environment(u,v)* equal(appear(an_organisation,u),v)* -> greater(cardinality_at_time(efficient_producers,v),zero)*l equal(appear(first_movers,u),appear(an_organisation,u))**. % 0.33/0.58 175[0:Res:162.1,104.2] environment(u) || greater(number_of_organizations(skc1,appear(an_organisation,u)),zero)+ in_environment(u,appear(an_organisation,u))* -> greater(cardinality_at_time(efficient_producers,appear(an_organisation,u)),zero)*l equal(appear(first_movers,u),appear(an_organisation,u)). % 0.33/0.58 269[0:NCh:10.2,10.1,106.2,54.1] environment(u) environment(v) || in_environment(u,appear(an_organisation,v))* equal(appear(an_organisation,u),appear(efficient_producers,e)) greater(cardinality_at_time(first_movers,appear(an_organisation,v)),zero)*l+ -> equal(appear(first_movers,u),appear(an_organisation,u)). % 0.33/0.58 214[0:Obv:209.0] environment(u) environment(v) || in_environment(v,appear(first_movers,u))* greater(appear(an_organisation,v),appear(efficient_producers,e))+ greater(cardinality_at_time(first_movers,appear(first_movers,u)),zero)*l -> equal(appear(first_movers,v),appear(an_organisation,v)). % 0.33/0.58 316[0:Obv:306.2] environment(u) || greater(number_of_organizations(skc1,v),zero) greater(number_of_organizations(u,v),zero) -> greater(cardinality_at_time(first_movers,v),zero) subpopulation(efficient_producers,u,v)*. % 0.33/0.58 132[0:NCh:10.2,10.1,13.2,54.1] environment(u) environment(v) || in_environment(u,appear(an_organisation,v))* greater(appear(efficient_producers,u),appear(efficient_producers,e))+ greater(cardinality_at_time(efficient_producers,appear(an_organisation,v)),zero)*l -> . % 0.33/0.58 329[0:SSi:324.0,1.0] environment(u) || in_environment(skc1,appear(an_organisation,u)) greater(appear(an_organisation,skc1),appear(efficient_producers,e)) greater(cardinality_at_time(first_movers,appear(an_organisation,u)),zero)*l -> . % 0.33/0.58 328[0:SSi:325.0,1.0] environment(u) || in_environment(skc1,appear(an_organisation,u)) equal(appear(efficient_producers,e),appear(an_organisation,skc1)) greater(cardinality_at_time(first_movers,appear(an_organisation,u)),zero)*l -> . % 0.33/0.58 213[0:Obv:210.0] environment(u) environment(v) || in_environment(v,appear(first_movers,u))* equal(appear(an_organisation,v),appear(efficient_producers,e)) greater(cardinality_at_time(first_movers,appear(first_movers,u)),zero)*l+ -> equal(appear(first_movers,v),appear(an_organisation,v)). % 0.33/0.58 98[0:NCh:10.2,10.1,14.2,54.1] environment(u) environment(v) || in_environment(u,appear(an_organisation,v))* greater(appear(first_movers,u),appear(efficient_producers,e))+ greater(cardinality_at_time(first_movers,appear(an_organisation,v)),zero)*l -> . % 0.33/0.58 243[0:Res:109.2,133.4] environment(u) environment(v) || equal(first_movers,efficient_producers) greater(number_of_organizations(skc1,appear(an_organisation,v)),zero)*l+ in_environment(u,appear(an_organisation,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 166[0:Res:109.2,131.4] environment(u) environment(v) || equal(first_movers,efficient_producers) greater(number_of_organizations(skc1,appear(first_movers,v)),zero)*l+ in_environment(u,appear(first_movers,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 117[0:SpR:61.2,18.1] environment(u) || greater(number_of_organizations(u,v),zero) greater(number_of_organizations(skc1,v),zero) -> equal(skf1(v,u),efficient_producers)** greater(cardinality_at_time(first_movers,v),zero). % 0.33/0.58 300[0:Obv:291.1] || greater(number_of_organizations(skc1,u),zero)*l greater(appear(an_organisation,skc1),u) in_environment(skc1,u) greater(appear(efficient_producers,skc1),u) -> . % 0.33/0.58 282[0:Obv:273.1] || greater(number_of_organizations(skc1,u),zero)*l greater(appear(first_movers,skc1),u) in_environment(skc1,u) greater(appear(efficient_producers,skc1),u) -> . % 0.33/0.58 178[0:Res:162.1,103.2] || greater(number_of_organizations(skc1,u),zero) in_environment(skc1,u) greater(appear(an_organisation,skc1),u) -> greater(cardinality_at_time(efficient_producers,u),zero)*l. % 0.33/0.58 179[0:Res:162.1,16.1] || greater(number_of_organizations(skc1,u),zero) in_environment(skc1,u) greater(appear(first_movers,skc1),u) -> greater(cardinality_at_time(efficient_producers,u),zero)*l. % 0.33/0.58 106[0:Obv:92.0] environment(u) || in_environment(u,v)* greater(appear(an_organisation,u),v)*+ greater(cardinality_at_time(first_movers,v),zero)*l -> equal(appear(first_movers,u),appear(an_organisation,u))**. % 0.33/0.58 212[0:SSi:207.0,1.0] environment(u) || in_environment(skc1,appear(first_movers,u)) greater(appear(an_organisation,skc1),appear(efficient_producers,e)) greater(cardinality_at_time(first_movers,appear(first_movers,u)),zero)*l -> . % 0.33/0.58 128[0:NCh:10.2,10.1,13.2,22.0] environment(u) || in_environment(u,appear(first_movers,skc1))* greater(appear(efficient_producers,u),appear(efficient_producers,e))+ greater(cardinality_at_time(efficient_producers,appear(first_movers,skc1)),zero)*l -> . % 0.33/0.58 170[0:Res:109.2,129.3] environment(u) || equal(first_movers,efficient_producers) greater(number_of_organizations(skc1,appear(first_movers,skc1)),zero)*l+ in_environment(u,appear(first_movers,skc1))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 250[0:SSi:241.1,1.0] environment(u) || greater(number_of_organizations(skc1,appear(an_organisation,skc1)),zero)*l+ in_environment(u,appear(an_organisation,skc1))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.33/0.58 94[0:NCh:10.2,10.1,14.2,22.0] environment(u) || in_environment(u,appear(first_movers,skc1))* greater(appear(first_movers,u),appear(efficient_producers,e))+ greater(cardinality_at_time(first_movers,appear(first_movers,skc1)),zero)*l -> . % 0.33/0.58 133[0:NCh:10.2,10.1,13.2,54.1] environment(u) environment(v) || in_environment(u,appear(an_organisation,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) greater(cardinality_at_time(efficient_producers,appear(an_organisation,v)),zero)*l+ -> . % 0.33/0.58 99[0:NCh:10.2,10.1,14.2,54.1] environment(u) environment(v) || in_environment(u,appear(an_organisation,v))* equal(appear(first_movers,u),appear(efficient_producers,e)) greater(cardinality_at_time(first_movers,appear(an_organisation,v)),zero)*l+ -> . % 0.33/0.58 126[0:NCh:10.2,10.0,13.2,54.1] environment(e) environment(u) || in_environment(e,v) greater(appear(an_organisation,u),v)* greater(cardinality_at_time(efficient_producers,v),zero)*l -> . % 0.33/0.58 228[0:Obv:221.1] || greater(number_of_organizations(skc1,u),zero)*l equal(appear(an_organisation,skc1),u) in_environment(skc1,u) greater(appear(efficient_producers,skc1),u) -> . % 0.33/0.58 130[0:NCh:10.2,10.1,13.2,9.1] environment(u) environment(v) || in_environment(u,appear(first_movers,v))* greater(appear(efficient_producers,u),appear(efficient_producers,e))+ greater(cardinality_at_time(efficient_producers,appear(first_movers,v)),zero)*l -> . % 0.33/0.58 105[0:Obv:93.0] environment(u) || in_environment(u,v)* equal(appear(an_organisation,u),v)* greater(cardinality_at_time(first_movers,v),zero)*l+ -> equal(appear(first_movers,u),appear(an_organisation,u))**. % 0.33/0.58 180[0:Res:162.1,102.2] || greater(number_of_organizations(skc1,u),zero) in_environment(skc1,u) equal(appear(an_organisation,skc1),u) -> greater(cardinality_at_time(efficient_producers,u),zero)*l. % 0.33/0.58 211[0:SSi:208.0,1.0] environment(u) || in_environment(skc1,appear(first_movers,u)) equal(appear(efficient_producers,e),appear(an_organisation,skc1)) greater(cardinality_at_time(first_movers,appear(first_movers,u)),zero)*l -> . % 0.33/0.58 205[0:MRR:202.1,2.0] || greater(number_of_organizations(skc1,appear(an_organisation,skc1)),zero)*l greater(appear(efficient_producers,skc1),appear(an_organisation,skc1)) -> . % 0.33/0.58 96[0:NCh:10.2,10.1,14.2,9.1] environment(u) environment(v) || in_environment(u,appear(first_movers,v))* greater(appear(first_movers,u),appear(efficient_producers,e))+ greater(cardinality_at_time(first_movers,appear(first_movers,v)),zero)*l -> . % 0.33/0.58 174[0:Res:162.1,101.0] || greater(number_of_organizations(skc1,appear(an_organisation,skc1)),zero) -> greater(cardinality_at_time(efficient_producers,appear(an_organisation,skc1)),zero)*l. % 0.33/0.58 162[0:Obv:158.0] || greater(number_of_organizations(skc1,u),zero) -> greater(cardinality_at_time(first_movers,u),zero)*l greater(cardinality_at_time(efficient_producers,u),zero). % 0.33/0.58 147[0:Res:109.2,17.1] || equal(first_movers,efficient_producers) greater(number_of_organizations(skc1,u),zero)*l in_environment(skc1,u) greater(appear(efficient_producers,skc1),u) -> . % 0.33/0.58 129[0:NCh:10.2,10.1,13.2,22.0] environment(u) || in_environment(u,appear(first_movers,skc1))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) greater(cardinality_at_time(efficient_producers,appear(first_movers,skc1)),zero)*l+ -> . % 0.33/0.58 131[0:NCh:10.2,10.1,13.2,9.1] environment(u) environment(v) || in_environment(u,appear(first_movers,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) greater(cardinality_at_time(efficient_producers,appear(first_movers,v)),zero)*l+ -> . % 0.33/0.58 95[0:NCh:10.2,10.1,14.2,22.0] environment(u) || in_environment(u,appear(first_movers,skc1))* equal(appear(first_movers,u),appear(efficient_producers,e)) greater(cardinality_at_time(first_movers,appear(first_movers,skc1)),zero)*l+ -> . % 0.33/0.58 104[0:Obv:89.0] environment(u) || in_environment(u,appear(an_organisation,u))* greater(cardinality_at_time(first_movers,appear(an_organisation,u)),zero)*l+ -> equal(appear(first_movers,u),appear(an_organisation,u)). % 0.33/0.58 124[0:NCh:10.2,10.0,13.2,31.0] environment(e) || in_environment(e,u) greater(appear(an_organisation,skc1),u) greater(cardinality_at_time(efficient_producers,u),zero)*l -> . % 0.33/0.58 127[0:NCh:10.2,10.0,13.2,54.1] environment(e) environment(u) || in_environment(e,v) equal(appear(an_organisation,u),v)* greater(cardinality_at_time(efficient_producers,v),zero)*l -> . % 0.33/0.58 97[0:NCh:10.2,10.1,14.2,9.1] environment(u) environment(v) || in_environment(u,appear(first_movers,v))* equal(appear(first_movers,u),appear(efficient_producers,e)) greater(cardinality_at_time(first_movers,appear(first_movers,v)),zero)*l+ -> . % 0.33/0.58 159[0:Obv:154.0] || greater(number_of_organizations(skc1,u),zero) -> greater(cardinality_at_time(first_movers,u),zero) subpopulation(efficient_producers,skc1,u)*. % 0.33/0.58 110[0:Obv:108.0] || greater(number_of_organizations(skc1,u),zero) -> equal(skf1(u,skc1),efficient_producers)** greater(cardinality_at_time(first_movers,u),zero). % 0.33/0.58 103[0:SSi:90.0,1.0] || in_environment(skc1,u) greater(appear(an_organisation,skc1),u) greater(cardinality_at_time(first_movers,u),zero)*l -> . % 0.33/0.58 17[0:Res:1.0,13.0] || in_environment(skc1,u) greater(cardinality_at_time(efficient_producers,u),zero)*l greater(appear(efficient_producers,skc1),u) -> . % 0.33/0.58 16[0:Res:1.0,14.0] || in_environment(skc1,u) greater(cardinality_at_time(first_movers,u),zero)*l greater(appear(first_movers,skc1),u) -> . % 0.33/0.58 123[0:Res:54.1,13.2] environment(u) environment(e) || in_environment(e,appear(an_organisation,u)) greater(cardinality_at_time(efficient_producers,appear(an_organisation,u)),zero)*l -> . % 0.33/0.58 109[0:Obv:107.0] || equal(first_movers,efficient_producers) greater(number_of_organizations(skc1,u),zero) -> greater(cardinality_at_time(efficient_producers,u),zero)*l. % 0.33/0.58 125[0:NCh:10.2,10.0,13.2,31.0] environment(e) || in_environment(e,u) equal(appear(an_organisation,skc1),u) greater(cardinality_at_time(efficient_producers,u),zero)*l -> . % 0.33/0.58 119[0:Obv:112.2] environment(u) || greater(number_of_organizations(u,v),zero) -> equal(skf1(v,u),efficient_producers) subpopulation(first_movers,u,v)*. % 0.33/0.58 122[0:Res:9.1,13.2] environment(u) environment(e) || in_environment(e,appear(first_movers,u)) greater(cardinality_at_time(efficient_producers,appear(first_movers,u)),zero)*l -> . % 0.33/0.58 142[0:Obv:134.2] environment(u) || equal(first_movers,efficient_producers) greater(number_of_organizations(u,v),zero) -> subpopulation(efficient_producers,u,v)*. % 0.33/0.58 111[0:EqF:61.2,61.3] environment(u) || greater(number_of_organizations(u,v),zero) equal(first_movers,efficient_producers) -> equal(skf1(v,u),efficient_producers)**. % 0.33/0.58 120[0:Res:22.0,13.2] environment(e) || in_environment(e,appear(first_movers,skc1)) greater(cardinality_at_time(efficient_producers,appear(first_movers,skc1)),zero)*l -> . % 0.33/0.58 121[0:Res:31.0,13.2] environment(e) || in_environment(e,appear(an_organisation,skc1)) greater(cardinality_at_time(efficient_producers,appear(an_organisation,skc1)),zero)*l -> . % 0.33/0.58 13[0:Inp] environment(u) || in_environment(u,v)* greater(appear(efficient_producers,u),v)*+ greater(cardinality_at_time(efficient_producers,v),zero)*l -> . % 0.33/0.58 61[0:MRR:60.2,12.2] environment(u) || greater(number_of_organizations(u,v),zero) -> equal(skf1(v,u),first_movers)** equal(skf1(v,u),efficient_producers). % 0.33/0.58 18[0:Res:1.0,12.0] || greater(number_of_organizations(skc1,u),zero) -> greater(cardinality_at_time(skf1(u,v),u),zero)*l. % 0.33/0.58 102[0:SSi:91.0,1.0] || in_environment(skc1,u) equal(appear(an_organisation,skc1),u) greater(cardinality_at_time(first_movers,u),zero)*l -> . % 0.33/0.58 101[0:MRR:100.0,2.0] || greater(cardinality_at_time(first_movers,appear(an_organisation,skc1)),zero)*l -> . % 0.33/0.58 14[0:Inp] environment(u) || in_environment(u,v)* greater(appear(first_movers,u),v)*+ greater(cardinality_at_time(first_movers,v),zero)*l -> . % 0.33/0.58 19[0:Res:1.0,15.0] || greater(cardinality_at_time(u,v),zero) subpopulation(u,skc1,v)* -> equal(u,first_movers) equal(u,efficient_producers). % 0.33/0.58 76[0:Res:6.1,12.1] environment(u) environment(e) || -> greater(cardinality_at_time(skf1(appear(an_organisation,u),v),appear(an_organisation,u)),zero)*l. % 0.33/0.58 66[0:Obv:64.0] || greater(number_of_organizations(skc1,u),zero) -> equal(skf1(u,skc1),efficient_producers) subpopulation(first_movers,skc1,u)*. % 0.33/0.58 75[0:Res:21.0,12.1] environment(e) || -> greater(cardinality_at_time(skf1(appear(an_organisation,skc1),u),appear(an_organisation,skc1)),zero)*l. % 0.33/0.58 12[0:Inp] environment(u) || greater(number_of_organizations(u,v),zero)*l+ -> greater(cardinality_at_time(skf1(v,w),v),zero)*l. % 0.33/0.58 72[0:Obv:69.0] || equal(first_movers,efficient_producers) greater(number_of_organizations(skc1,u),zero) -> subpopulation(efficient_producers,skc1,u)*. % 0.33/0.58 62[0:EqF:59.1,59.2] || greater(number_of_organizations(skc1,u),zero) equal(first_movers,efficient_producers) -> equal(skf1(u,skc1),efficient_producers)**. % 0.33/0.58 59[0:MRR:58.1,18.1] || greater(number_of_organizations(skc1,u),zero) -> equal(skf1(u,skc1),first_movers)** equal(skf1(u,skc1),efficient_producers). % 0.33/0.58 54[0:Obv:46.2] environment(u) || -> greater(appear(efficient_producers,e),appear(an_organisation,u))*. % 0.33/0.59 15[0:Inp] environment(u) || greater(cardinality_at_time(v,w),zero) subpopulation(v,u,w)* -> equal(v,first_movers) equal(v,efficient_producers). % 0.33/0.59 34[0:Res:7.1,8.0] environment(u) || -> equal(appear(first_movers,u),appear(an_organisation,u)) greater(appear(first_movers,u),appear(an_organisation,u))*l. % 0.33/0.59 27[0:Res:8.2,5.0] || greater_or_equal(appear(an_organisation,skc1),appear(first_movers,skc1))* -> greater(appear(an_organisation,skc1),appear(first_movers,skc1)). % 0.33/0.59 20[0:Res:1.0,11.0] || greater(number_of_organizations(skc1,u),zero) -> subpopulation(skf1(u,skc1),skc1,u)*. % 0.33/0.59 11[0:Inp] environment(u) || greater(number_of_organizations(u,v),zero) -> subpopulation(skf1(v,u),u,v)*. % 0.33/0.59 8[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 0.33/0.59 9[0:Inp] environment(u) || -> greater(appear(efficient_producers,e),appear(first_movers,u))*r. % 0.33/0.59 6[0:Inp] environment(u) || -> greater(number_of_organizations(e,appear(an_organisation,u)),zero)*l. % 0.33/0.59 31[0:OCh:10.1,10.0,28.0,22.0] || -> greater(appear(efficient_producers,e),appear(an_organisation,skc1))*l. % 0.33/0.59 3[0:Inp] || greater(u,v) -> greater_or_equal(u,v)*. % 0.33/0.59 28[0:MRR:26.0,23.0] || -> greater(appear(first_movers,skc1),appear(an_organisation,skc1))*l. % 0.33/0.59 22[0:Res:1.0,9.0] || -> greater(appear(efficient_producers,e),appear(first_movers,skc1))*r. % 0.33/0.59 21[0:Res:1.0,6.0] || -> greater(number_of_organizations(e,appear(an_organisation,skc1)),zero)*l. % 0.33/0.59 7[0:Inp] environment(u) || -> greater_or_equal(appear(first_movers,u),appear(an_organisation,u))*. % 0.33/0.59 5[0:Inp] || equal(appear(first_movers,skc1),appear(an_organisation,skc1))** -> . % 0.33/0.59 4[0:Inp] || equal(u,v) -> greater_or_equal(u,v)*. % 0.33/0.59 23[0:Res:1.0,7.0] || -> greater_or_equal(appear(first_movers,skc1),appear(an_organisation,skc1))*. % 0.33/0.59 2[0:Inp] || -> in_environment(skc1,appear(an_organisation,skc1))*. % 0.33/0.59 1[0:Inp] || -> environment(skc1)*. % 0.33/0.59 % SZS output end Saturation %------------------------------------------------------------------------------