%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT031-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n018.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 : Satisfiable 0.31s 0.56s % Output : Saturation 0.31s % 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.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.09/0.36 % Computer : n018.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Mon Sep 7 12:23:22 UTC 2026 % 0.09/0.37 % CPUTime : % 0.31/0.56 % 0.31/0.56 SPASS V 3.9 % 0.31/0.56 SPASS beiseite: Completion found. % 0.31/0.56 % SZS status CounterSatisfiable % 0.31/0.56 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.31/0.56 SPASS derived 410 clauses, backtracked 0 clauses, performed 1 splits and kept 147 clauses. % 0.31/0.56 SPASS allocated 76199 KBytes. % 0.31/0.56 SPASS spent 0:00:00.19 on the problem. % 0.31/0.56 0:00:00.06 for the input. % 0.31/0.56 0:00:00.00 for the FLOTTER CNF translation. % 0.31/0.56 0:00:00.02 for inferences. % 0.31/0.56 0:00:00.00 for the backtracking. % 0.31/0.56 0:00:00.06 for the reduction. % 0.31/0.56 % 0.31/0.56 % 0.31/0.56 The saturated set of worked-off clauses is : % 0.31/0.56 % SZS output start Saturation % 0.31/0.56 7[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.31/0.56 369[0:Res:298.3,146.4] environment(u) environment(v) || in_environment(sk2,appear(first_movers,v)) greater(appear(an_organisation,sk2),appear(first_movers,v))+ greater(number_of_organizations(sk2,appear(first_movers,v)),zero)*l in_environment(u,appear(first_movers,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 370[0:Res:298.3,148.4] environment(u) environment(v) || in_environment(sk2,appear(an_organisation,v)) greater(appear(an_organisation,sk2),appear(an_organisation,v))+ greater(number_of_organizations(sk2,appear(an_organisation,v)),zero)*l in_environment(u,appear(an_organisation,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 589[0:Obv:586.1] environment(u) environment(v) || in_environment(sk2,appear(first_movers,v)) greater(appear(first_movers,sk2),appear(efficient_producers,e))+ greater(number_of_organizations(sk2,appear(first_movers,v)),zero)*l in_environment(u,appear(first_movers,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 579[0:Obv:575.1] environment(u) environment(v) || in_environment(sk2,appear(an_organisation,v)) greater(appear(first_movers,sk2),appear(efficient_producers,e))+ greater(number_of_organizations(sk2,appear(an_organisation,v)),zero)*l in_environment(u,appear(an_organisation,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 588[0:Obv:587.1] environment(u) environment(v) || in_environment(sk2,appear(first_movers,v)) equal(appear(first_movers,sk2),appear(efficient_producers,e)) greater(number_of_organizations(sk2,appear(first_movers,v)),zero)*l+ in_environment(u,appear(first_movers,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 351[0:Res:278.3,146.4] environment(u) environment(v) || in_environment(sk2,appear(first_movers,v)) greater(appear(first_movers,sk2),appear(first_movers,v))+ greater(number_of_organizations(sk2,appear(first_movers,v)),zero)*l in_environment(u,appear(first_movers,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 578[0:Obv:576.1] environment(u) environment(v) || in_environment(sk2,appear(an_organisation,v)) equal(appear(first_movers,sk2),appear(efficient_producers,e)) greater(number_of_organizations(sk2,appear(an_organisation,v)),zero)*l+ in_environment(u,appear(an_organisation,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 352[0:Res:278.3,148.4] environment(u) environment(v) || in_environment(sk2,appear(an_organisation,v)) greater(appear(first_movers,sk2),appear(an_organisation,v))+ greater(number_of_organizations(sk2,appear(an_organisation,v)),zero)*l in_environment(u,appear(an_organisation,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 552[0:Obv:545.0] environment(u) environment(v) || in_environment(sk2,appear(an_organisation,v)) greater(appear(an_organisation,sk2),appear(efficient_producers,e))+ greater(number_of_organizations(sk2,appear(an_organisation,v)),zero)*l in_environment(u,appear(an_organisation,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 557[0:NCh:7.2,7.1,350.2,22.0] environment(u) || in_environment(sk2,appear(first_movers,sk2)) greater(appear(first_movers,sk2),appear(efficient_producers,e))+ greater(number_of_organizations(sk2,appear(first_movers,sk2)),zero)*l in_environment(u,appear(first_movers,sk2))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 539[0:Obv:529.0] environment(u) environment(v) || in_environment(sk2,appear(first_movers,v)) greater(appear(an_organisation,sk2),appear(efficient_producers,e))+ greater(number_of_organizations(sk2,appear(first_movers,v)),zero)*l in_environment(u,appear(first_movers,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 537[0:SSi:528.0,13.0] environment(u) || in_environment(sk2,appear(first_movers,sk2)) greater(appear(an_organisation,sk2),appear(efficient_producers,e))+ greater(number_of_organizations(sk2,appear(first_movers,sk2)),zero)*l in_environment(u,appear(first_movers,sk2))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 368[0:Res:298.3,144.3] environment(u) || in_environment(sk2,appear(first_movers,sk2)) greater(appear(an_organisation,sk2),appear(first_movers,sk2))+ greater(number_of_organizations(sk2,appear(first_movers,sk2)),zero)*l in_environment(u,appear(first_movers,sk2))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 551[0:Obv:546.1] environment(u) || greater(appear(an_organisation,sk2),appear(efficient_producers,e)) greater(number_of_organizations(sk2,appear(an_organisation,u)),zero)*l in_environment(sk2,appear(an_organisation,u)) greater(appear(efficient_producers,sk2),appear(an_organisation,u)) -> . % 0.31/0.56 558[0:NCh:7.2,7.1,350.2,22.0] environment(u) || in_environment(sk2,appear(first_movers,sk2)) equal(appear(first_movers,sk2),appear(efficient_producers,e)) greater(number_of_organizations(sk2,appear(first_movers,sk2)),zero)*l+ in_environment(u,appear(first_movers,sk2))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 350[0:Res:278.3,144.3] environment(u) || in_environment(sk2,appear(first_movers,sk2)) greater(appear(first_movers,sk2),appear(first_movers,sk2))+ greater(number_of_organizations(sk2,appear(first_movers,sk2)),zero)*l in_environment(u,appear(first_movers,sk2))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 538[0:Obv:530.1] environment(u) || greater(appear(an_organisation,sk2),appear(efficient_producers,e)) greater(number_of_organizations(sk2,appear(first_movers,u)),zero)*l in_environment(sk2,appear(first_movers,u)) greater(appear(efficient_producers,sk2),appear(first_movers,u)) -> . % 0.31/0.56 451[0:Res:80.2,349.4] environment(u) environment(v) || greater(number_of_organizations(sk2,appear(an_organisation,v)),zero)+ in_environment(u,appear(an_organisation,v))* equal(appear(an_organisation,u),appear(efficient_producers,e)) -> equal(sk1(appear(an_organisation,v),sk2),efficient_producers)** equal(appear(first_movers,u),appear(an_organisation,u)). % 0.31/0.56 328[0:Res:214.3,148.4] environment(u) environment(v) || in_environment(sk2,appear(an_organisation,v)) equal(appear(an_organisation,sk2),appear(an_organisation,v)) greater(number_of_organizations(sk2,appear(an_organisation,v)),zero)*l+ in_environment(u,appear(an_organisation,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 310[0:Res:214.3,146.4] environment(u) environment(v) || in_environment(sk2,appear(first_movers,v)) equal(appear(first_movers,v),appear(an_organisation,sk2)) greater(number_of_organizations(sk2,appear(first_movers,v)),zero)*l+ in_environment(u,appear(first_movers,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 386[0:Res:80.2,225.4] environment(u) environment(v) || greater(number_of_organizations(sk2,appear(first_movers,u)),zero)+ in_environment(v,appear(first_movers,u))* equal(appear(an_organisation,v),appear(efficient_producers,e)) -> equal(sk1(appear(first_movers,u),sk2),efficient_producers)** equal(appear(first_movers,v),appear(an_organisation,v)). % 0.31/0.56 523[0:Obv:516.0] environment(u) environment(v) || in_environment(sk2,appear(an_organisation,v)) equal(appear(efficient_producers,e),appear(an_organisation,sk2)) greater(number_of_organizations(sk2,appear(an_organisation,v)),zero)*l+ in_environment(u,appear(an_organisation,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 487[0:Obv:477.0] environment(u) environment(v) || in_environment(sk2,appear(first_movers,v)) equal(appear(efficient_producers,e),appear(an_organisation,sk2)) greater(number_of_organizations(sk2,appear(first_movers,v)),zero)*l+ in_environment(u,appear(first_movers,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 510[0:Obv:503.1] environment(u) || in_environment(sk2,appear(an_organisation,u)) greater(appear(an_organisation,sk2),appear(efficient_producers,e)) greater(number_of_organizations(sk2,appear(an_organisation,u)),zero) -> greater(cardinality_at_time(efficient_producers,appear(an_organisation,u)),zero)*l. % 0.31/0.56 471[0:Obv:465.1] environment(u) || in_environment(sk2,appear(first_movers,u)) greater(appear(an_organisation,sk2),appear(efficient_producers,e)) greater(number_of_organizations(sk2,appear(first_movers,u)),zero) -> greater(cardinality_at_time(efficient_producers,appear(first_movers,u)),zero)*l. % 0.31/0.56 348[0:NCh:7.2,7.1,120.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.31/0.56 485[0:SSi:476.0,13.0] environment(u) || in_environment(sk2,appear(first_movers,sk2)) equal(appear(efficient_producers,e),appear(an_organisation,sk2)) greater(number_of_organizations(sk2,appear(first_movers,sk2)),zero)*l+ in_environment(u,appear(first_movers,sk2))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 522[0:Obv:517.1] environment(u) || equal(appear(efficient_producers,e),appear(an_organisation,sk2)) greater(number_of_organizations(sk2,appear(an_organisation,u)),zero)*l in_environment(sk2,appear(an_organisation,u)) greater(appear(efficient_producers,sk2),appear(an_organisation,u)) -> . % 0.31/0.56 486[0:Obv:478.1] environment(u) || equal(appear(efficient_producers,e),appear(an_organisation,sk2)) greater(number_of_organizations(sk2,appear(first_movers,u)),zero)*l in_environment(sk2,appear(first_movers,u)) greater(appear(efficient_producers,sk2),appear(first_movers,u)) -> . % 0.31/0.56 446[0:Obv:440.1] environment(u) || in_environment(sk2,appear(an_organisation,u)) equal(appear(efficient_producers,e),appear(an_organisation,sk2)) greater(number_of_organizations(sk2,appear(an_organisation,u)),zero) -> greater(cardinality_at_time(efficient_producers,appear(an_organisation,u)),zero)*l. % 0.31/0.56 515[1:Spt:410.0,410.2,410.3,410.5] environment(u) || in_environment(u,appear(first_movers,sk2))* equal(appear(an_organisation,u),appear(efficient_producers,e)) -> equal(appear(first_movers,u),appear(an_organisation,u)). % 0.31/0.56 507[0:Obv:497.1] environment(u) || in_environment(sk2,appear(an_organisation,u)) greater(appear(an_organisation,sk2),appear(efficient_producers,e)) greater(number_of_organizations(sk2,appear(an_organisation,u)),zero) -> subpopulation(efficient_producers,sk2,appear(an_organisation,u))*. % 0.31/0.56 426[0:Res:80.2,419.3] environment(u) || greater(number_of_organizations(sk2,appear(an_organisation,u)),zero) in_environment(sk2,appear(an_organisation,u)) greater(appear(an_organisation,sk2),appear(efficient_producers,e)) -> equal(sk1(appear(an_organisation,u),sk2),efficient_producers)**. % 0.31/0.56 405[0:Obv:400.1] environment(u) || in_environment(sk2,appear(first_movers,u)) equal(appear(efficient_producers,e),appear(an_organisation,sk2)) greater(number_of_organizations(sk2,appear(first_movers,u)),zero) -> greater(cardinality_at_time(efficient_producers,appear(first_movers,u)),zero)*l. % 0.31/0.56 468[0:Obv:459.1] environment(u) || in_environment(sk2,appear(first_movers,u)) greater(appear(an_organisation,sk2),appear(efficient_producers,e)) greater(number_of_organizations(sk2,appear(first_movers,u)),zero) -> subpopulation(efficient_producers,sk2,appear(first_movers,u))*. % 0.31/0.56 340[0:Res:80.2,224.3] environment(u) || greater(number_of_organizations(sk2,appear(first_movers,u)),zero) in_environment(sk2,appear(first_movers,u)) greater(appear(an_organisation,sk2),appear(efficient_producers,e)) -> equal(sk1(appear(first_movers,u),sk2),efficient_producers)**. % 0.31/0.56 349[0:NCh:7.2,7.1,120.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.31/0.56 323[0:Res:80.2,113.4] environment(u) environment(v) || greater(number_of_organizations(sk2,appear(an_organisation,v)),zero)+ in_environment(u,appear(an_organisation,v))* equal(appear(first_movers,u),appear(efficient_producers,e)) -> equal(sk1(appear(an_organisation,v),sk2),efficient_producers)**. % 0.31/0.56 156[0:Res:80.2,111.4] environment(u) environment(v) || greater(number_of_organizations(sk2,appear(first_movers,v)),zero)+ in_environment(u,appear(first_movers,v))* equal(appear(first_movers,u),appear(efficient_producers,e)) -> equal(sk1(appear(first_movers,v),sk2),efficient_producers)**. % 0.31/0.56 443[0:Obv:434.1] environment(u) || in_environment(sk2,appear(an_organisation,u)) equal(appear(efficient_producers,e),appear(an_organisation,sk2)) greater(number_of_organizations(sk2,appear(an_organisation,u)),zero) -> subpopulation(efficient_producers,sk2,appear(an_organisation,u))*. % 0.31/0.56 147[0:NCh:7.2,7.1,4.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.31/0.56 422[0:Res:80.2,418.3] environment(u) || greater(number_of_organizations(sk2,appear(an_organisation,u)),zero) in_environment(sk2,appear(an_organisation,u)) equal(appear(efficient_producers,e),appear(an_organisation,sk2)) -> equal(sk1(appear(an_organisation,u),sk2),efficient_producers)**. % 0.31/0.56 419[0:SSi:414.0,13.0] environment(u) || in_environment(sk2,appear(an_organisation,u)) greater(appear(an_organisation,sk2),appear(efficient_producers,e)) greater(cardinality_at_time(first_movers,appear(an_organisation,u)),zero)*l -> . % 0.31/0.56 418[0:SSi:415.0,13.0] environment(u) || in_environment(sk2,appear(an_organisation,u)) equal(appear(efficient_producers,e),appear(an_organisation,sk2)) greater(cardinality_at_time(first_movers,appear(an_organisation,u)),zero)*l -> . % 0.31/0.56 112[0:NCh:7.2,7.1,5.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.31/0.56 308[0:Obv:305.0] environment(u) || in_environment(u,appear(first_movers,sk2))* greater(appear(an_organisation,u),appear(efficient_producers,e))+ greater(cardinality_at_time(first_movers,appear(first_movers,sk2)),zero)*l -> equal(appear(first_movers,u),appear(an_organisation,u)). % 0.31/0.56 329[0:Res:78.2,148.4] environment(u) environment(v) || equal(first_movers,efficient_producers) greater(number_of_organizations(sk2,appear(an_organisation,v)),zero)*l+ in_environment(u,appear(an_organisation,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.56 193[0:Res:78.2,146.4] environment(u) environment(v) || equal(first_movers,efficient_producers) greater(number_of_organizations(sk2,appear(first_movers,v)),zero)*l+ in_environment(u,appear(first_movers,v))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.57 380[0:Obv:371.0] || greater(appear(an_organisation,sk2),u) greater(number_of_organizations(sk2,u),zero)*l in_environment(sk2,u) greater(appear(efficient_producers,sk2),u) -> . % 0.31/0.57 226[0:Obv:221.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.31/0.57 362[0:Obv:353.0] || greater(appear(first_movers,sk2),u) greater(number_of_organizations(sk2,u),zero)*l in_environment(sk2,u) greater(appear(efficient_producers,sk2),u) -> . % 0.31/0.57 402[0:Obv:394.1] environment(u) || in_environment(sk2,appear(first_movers,u)) equal(appear(efficient_producers,e),appear(an_organisation,sk2)) greater(number_of_organizations(sk2,appear(first_movers,u)),zero) -> subpopulation(efficient_producers,sk2,appear(first_movers,u))*. % 0.31/0.57 256[0:Res:80.2,223.3] environment(u) || greater(number_of_organizations(sk2,appear(first_movers,u)),zero) in_environment(sk2,appear(first_movers,u)) equal(appear(efficient_producers,e),appear(an_organisation,sk2)) -> equal(sk1(appear(first_movers,u),sk2),efficient_producers)**. % 0.31/0.57 248[0:Res:80.2,109.3] environment(u) || greater(number_of_organizations(sk2,appear(first_movers,sk2)),zero)+ in_environment(u,appear(first_movers,sk2))* equal(appear(first_movers,u),appear(efficient_producers,e)) -> equal(sk1(appear(first_movers,sk2),sk2),efficient_producers)**. % 0.31/0.57 225[0:Obv:222.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.31/0.57 260[0:Res:80.2,119.3] environment(u) || greater(number_of_organizations(sk2,v),zero)+ in_environment(u,v)* equal(appear(an_organisation,u),v)* -> equal(sk1(v,sk2),efficient_producers)** equal(appear(first_movers,u),appear(an_organisation,u))**. % 0.31/0.57 244[0:Res:80.2,118.2] environment(u) || greater(number_of_organizations(sk2,appear(an_organisation,u)),zero)+ in_environment(u,appear(an_organisation,u))* -> equal(sk1(appear(an_organisation,u),sk2),efficient_producers)** equal(appear(first_movers,u),appear(an_organisation,u)). % 0.31/0.57 298[0:Obv:293.0] || in_environment(sk2,u) greater(appear(an_organisation,sk2),u) greater(number_of_organizations(sk2,u),zero) -> greater(cardinality_at_time(efficient_producers,u),zero)*l. % 0.31/0.57 278[0:Obv:273.0] || in_environment(sk2,u) greater(appear(first_movers,sk2),u) greater(number_of_organizations(sk2,u),zero) -> greater(cardinality_at_time(efficient_producers,u),zero)*l. % 0.31/0.57 120[0:Obv:106.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.31/0.57 224[0:SSi:219.0,13.0] environment(u) || in_environment(sk2,appear(first_movers,u)) greater(appear(an_organisation,sk2),appear(efficient_producers,e)) greater(cardinality_at_time(first_movers,appear(first_movers,u)),zero)*l -> . % 0.31/0.57 252[0:Res:78.2,144.3] environment(u) || equal(first_movers,efficient_producers) greater(number_of_organizations(sk2,appear(first_movers,sk2)),zero)*l+ in_environment(u,appear(first_movers,sk2))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.57 336[0:SSi:327.1,13.0] environment(u) || greater(number_of_organizations(sk2,appear(an_organisation,sk2)),zero)*l+ in_environment(u,appear(an_organisation,sk2))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) -> . % 0.31/0.57 148[0:NCh:7.2,7.1,4.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.31/0.57 143[0:NCh:7.2,7.1,4.2,22.0] environment(u) || in_environment(u,appear(first_movers,sk2))* greater(appear(efficient_producers,u),appear(efficient_producers,e))+ greater(cardinality_at_time(efficient_producers,appear(first_movers,sk2)),zero)*l -> . % 0.31/0.57 113[0:NCh:7.2,7.1,5.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.31/0.57 141[0:NCh:7.2,7.0,4.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.31/0.57 318[0:Obv:311.0] || equal(appear(an_organisation,sk2),u) greater(number_of_organizations(sk2,u),zero)*l in_environment(sk2,u) greater(appear(efficient_producers,sk2),u) -> . % 0.31/0.57 214[0:Obv:209.0] || in_environment(sk2,u) equal(appear(an_organisation,sk2),u) greater(number_of_organizations(sk2,u),zero) -> greater(cardinality_at_time(efficient_producers,u),zero)*l. % 0.31/0.57 108[0:NCh:7.2,7.1,5.2,22.0] environment(u) || in_environment(u,appear(first_movers,sk2))* greater(appear(first_movers,u),appear(efficient_producers,e))+ greater(cardinality_at_time(first_movers,appear(first_movers,sk2)),zero)*l -> . % 0.31/0.57 295[0:Obv:287.0] || in_environment(sk2,u) greater(appear(an_organisation,sk2),u) greater(number_of_organizations(sk2,u),zero) -> subpopulation(efficient_producers,sk2,u)*. % 0.31/0.57 197[0:Res:80.2,117.2] || greater(number_of_organizations(sk2,u),zero) in_environment(sk2,u) greater(appear(an_organisation,sk2),u) -> equal(sk1(u,sk2),efficient_producers)**. % 0.31/0.57 275[0:Obv:268.0] || in_environment(sk2,u) greater(appear(first_movers,sk2),u) greater(number_of_organizations(sk2,u),zero) -> subpopulation(efficient_producers,sk2,u)*. % 0.31/0.57 157[0:Res:80.2,16.1] || greater(number_of_organizations(sk2,u),zero) in_environment(sk2,u) greater(appear(first_movers,sk2),u) -> equal(sk1(u,sk2),efficient_producers)**. % 0.31/0.57 119[0:Obv:107.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.31/0.57 223[0:SSi:220.0,13.0] environment(u) || in_environment(sk2,appear(first_movers,u)) equal(appear(efficient_producers,e),appear(an_organisation,sk2)) greater(cardinality_at_time(first_movers,appear(first_movers,u)),zero)*l -> . % 0.31/0.57 151[0:Res:78.2,17.1] || equal(first_movers,efficient_producers) greater(number_of_organizations(sk2,u),zero)*l in_environment(sk2,u) greater(appear(efficient_producers,sk2),u) -> . % 0.31/0.57 144[0:NCh:7.2,7.1,4.2,22.0] environment(u) || in_environment(u,appear(first_movers,sk2))* equal(appear(efficient_producers,u),appear(efficient_producers,e)) greater(cardinality_at_time(efficient_producers,appear(first_movers,sk2)),zero)*l+ -> . % 0.31/0.57 109[0:NCh:7.2,7.1,5.2,22.0] environment(u) || in_environment(u,appear(first_movers,sk2))* equal(appear(first_movers,u),appear(efficient_producers,e)) greater(cardinality_at_time(first_movers,appear(first_movers,sk2)),zero)*l+ -> . % 0.31/0.57 118[0:Obv:103.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.31/0.57 236[0:Res:1.1,101.1] environment(u) environment(e) || -> equal(sk1(appear(an_organisation,u),e),efficient_producers) greater(cardinality_at_time(first_movers,appear(an_organisation,u)),zero)*l. % 0.31/0.57 241[0:MRR:235.2,115.0] environment(e) || -> equal(sk1(appear(an_organisation,sk2),e),efficient_producers)**. % 0.31/0.57 101[0:Obv:92.2] environment(u) || greater(number_of_organizations(u,v),zero)+ -> equal(sk1(v,u),efficient_producers)** greater(cardinality_at_time(first_movers,v),zero)*l. % 0.31/0.57 139[0:NCh:7.2,7.0,4.2,31.0] environment(e) || in_environment(e,u) greater(appear(an_organisation,sk2),u) greater(cardinality_at_time(efficient_producers,u),zero)*l -> . % 0.31/0.57 145[0:NCh:7.2,7.1,4.2,12.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.31/0.57 228[0:Res:1.1,132.2] environment(u) environment(e) || equal(first_movers,efficient_producers) -> greater(cardinality_at_time(efficient_producers,appear(an_organisation,u)),zero)*l. % 0.31/0.57 227[0:Res:21.0,132.2] environment(e) || equal(first_movers,efficient_producers) -> greater(cardinality_at_time(efficient_producers,appear(an_organisation,sk2)),zero)*l. % 0.31/0.57 132[0:Obv:122.2] environment(u) || equal(first_movers,efficient_producers) greater(number_of_organizations(u,v),zero)*l+ -> greater(cardinality_at_time(efficient_producers,v),zero)*l. % 0.31/0.57 142[0:NCh:7.2,7.0,4.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.31/0.57 110[0:NCh:7.2,7.1,5.2,12.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.31/0.57 211[0:Obv:205.0] || in_environment(sk2,u) equal(appear(an_organisation,sk2),u) greater(number_of_organizations(sk2,u),zero) -> subpopulation(efficient_producers,sk2,u)*. % 0.31/0.58 158[0:Res:80.2,116.2] || greater(number_of_organizations(sk2,u),zero) in_environment(sk2,u) equal(appear(an_organisation,sk2),u) -> equal(sk1(u,sk2),efficient_producers)**. % 0.31/0.58 117[0:SSi:104.0,13.0] || in_environment(sk2,u) greater(appear(an_organisation,sk2),u) greater(cardinality_at_time(first_movers,u),zero)*l -> . % 0.31/0.58 191[0:MRR:188.1,14.0] || greater(number_of_organizations(sk2,appear(an_organisation,sk2)),zero)*l greater(appear(efficient_producers,sk2),appear(an_organisation,sk2)) -> . % 0.31/0.58 146[0:NCh:7.2,7.1,4.2,12.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.31/0.58 183[0:Obv:178.0] || greater(number_of_organizations(sk2,appear(an_organisation,sk2)),zero) -> greater(cardinality_at_time(efficient_producers,appear(an_organisation,sk2)),zero)*l. % 0.31/0.58 180[0:Obv:175.0] || greater(number_of_organizations(sk2,appear(an_organisation,sk2)),zero) -> subpopulation(efficient_producers,sk2,appear(an_organisation,sk2))*. % 0.31/0.58 155[0:Res:80.2,115.0] || greater(number_of_organizations(sk2,appear(an_organisation,sk2)),zero) -> equal(sk1(appear(an_organisation,sk2),sk2),efficient_producers)**. % 0.31/0.58 80[0:SSi:79.0,13.0] || greater(number_of_organizations(sk2,u),zero) -> equal(sk1(u,sk2),efficient_producers) greater(cardinality_at_time(first_movers,u),zero)*l. % 0.31/0.58 111[0:NCh:7.2,7.1,5.2,12.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.31/0.58 17[0:Res:13.0,4.0] || in_environment(sk2,u) greater(cardinality_at_time(efficient_producers,u),zero)*l greater(appear(efficient_producers,sk2),u) -> . % 0.31/0.58 16[0:Res:13.0,5.0] || in_environment(sk2,u) greater(cardinality_at_time(first_movers,u),zero)*l greater(appear(first_movers,sk2),u) -> . % 0.31/0.58 138[0:Res:54.1,4.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.31/0.58 78[0:SSi:77.0,13.0] || equal(first_movers,efficient_producers) greater(number_of_organizations(sk2,u),zero) -> greater(cardinality_at_time(efficient_producers,u),zero)*l. % 0.31/0.58 137[0:Res:12.1,4.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.31/0.58 140[0:NCh:7.2,7.0,4.2,31.0] environment(e) || in_environment(e,u) equal(appear(an_organisation,sk2),u) greater(cardinality_at_time(efficient_producers,u),zero)*l -> . % 0.31/0.58 99[0:Obv:91.2] environment(u) || greater(number_of_organizations(u,v),zero) -> equal(sk1(v,u),efficient_producers) subpopulation(first_movers,u,v)*. % 0.31/0.58 135[0:Res:22.0,4.2] environment(e) || in_environment(e,appear(first_movers,sk2)) greater(cardinality_at_time(efficient_producers,appear(first_movers,sk2)),zero)*l -> . % 0.31/0.58 136[0:Res:31.0,4.2] environment(e) || in_environment(e,appear(an_organisation,sk2)) greater(cardinality_at_time(efficient_producers,appear(an_organisation,sk2)),zero)*l -> . % 0.31/0.58 4[0:Inp] environment(u) || in_environment(u,v)* greater(appear(efficient_producers,u),v)*+ greater(cardinality_at_time(efficient_producers,v),zero)*l -> . % 0.31/0.58 130[0:Obv:121.2] environment(u) || equal(first_movers,efficient_producers) greater(number_of_organizations(u,v),zero) -> subpopulation(efficient_producers,u,v)*. % 0.31/0.58 90[0:EqF:61.2,61.3] environment(u) || greater(number_of_organizations(u,v),zero) equal(first_movers,efficient_producers) -> equal(sk1(v,u),efficient_producers)**. % 0.31/0.58 116[0:SSi:105.0,13.0] || in_environment(sk2,u) equal(appear(an_organisation,sk2),u) greater(cardinality_at_time(first_movers,u),zero)*l -> . % 0.31/0.58 115[0:MRR:114.0,14.0] || greater(cardinality_at_time(first_movers,appear(an_organisation,sk2)),zero)*l -> . % 0.31/0.58 5[0:Inp] environment(u) || in_environment(u,v)* greater(appear(first_movers,u),v)*+ greater(cardinality_at_time(first_movers,v),zero)*l -> . % 0.31/0.58 61[0:MRR:60.2,3.2] environment(u) || greater(number_of_organizations(u,v),zero) -> equal(sk1(v,u),first_movers)** equal(sk1(v,u),efficient_producers). % 0.31/0.58 18[0:Res:13.0,3.0] || greater(number_of_organizations(sk2,u),zero) -> greater(cardinality_at_time(sk1(u,sk2),u),zero)*l. % 0.31/0.58 19[0:Res:13.0,11.0] || greater(cardinality_at_time(u,v),zero) subpopulation(u,sk2,v)* -> equal(u,first_movers) equal(u,efficient_producers). % 0.31/0.58 66[0:Obv:64.0] || greater(number_of_organizations(sk2,u),zero) -> equal(sk1(u,sk2),efficient_producers) subpopulation(first_movers,sk2,u)*. % 0.31/0.58 3[0:Inp] environment(u) || greater(number_of_organizations(u,v),zero) -> greater(cardinality_at_time(sk1(v,u),v),zero)*l. % 0.31/0.58 72[0:Obv:69.0] || equal(first_movers,efficient_producers) greater(number_of_organizations(sk2,u),zero) -> subpopulation(efficient_producers,sk2,u)*. % 0.31/0.58 62[0:EqF:59.1,59.2] || greater(number_of_organizations(sk2,u),zero) equal(first_movers,efficient_producers) -> equal(sk1(u,sk2),efficient_producers)**. % 0.31/0.58 59[0:MRR:58.1,18.1] || greater(number_of_organizations(sk2,u),zero) -> equal(sk1(u,sk2),first_movers)** equal(sk1(u,sk2),efficient_producers). % 0.31/0.58 54[0:Obv:46.2] environment(u) || -> greater(appear(efficient_producers,e),appear(an_organisation,u))*. % 0.31/0.58 11[0:Inp] environment(u) || greater(cardinality_at_time(v,w),zero) subpopulation(v,u,w)* -> equal(v,first_movers) equal(v,efficient_producers). % 0.31/0.58 34[0:Res:6.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.31/0.58 27[0:Res:8.2,15.0] || greater_or_equal(appear(an_organisation,sk2),appear(first_movers,sk2))* -> greater(appear(an_organisation,sk2),appear(first_movers,sk2)). % 0.31/0.58 20[0:Res:13.0,2.0] || greater(number_of_organizations(sk2,u),zero) -> subpopulation(sk1(u,sk2),sk2,u)*. % 0.31/0.58 2[0:Inp] environment(u) || greater(number_of_organizations(u,v),zero) -> subpopulation(sk1(v,u),u,v)*. % 0.31/0.58 8[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 0.31/0.58 12[0:Inp] environment(u) || -> greater(appear(efficient_producers,e),appear(first_movers,u))*r. % 0.31/0.58 1[0:Inp] environment(u) || -> greater(number_of_organizations(e,appear(an_organisation,u)),zero)*l. % 0.31/0.58 31[0:OCh:7.1,7.0,28.0,22.0] || -> greater(appear(efficient_producers,e),appear(an_organisation,sk2))*l. % 0.31/0.58 9[0:Inp] || greater(u,v) -> greater_or_equal(u,v)*. % 0.31/0.58 28[0:MRR:26.0,23.0] || -> greater(appear(first_movers,sk2),appear(an_organisation,sk2))*l. % 0.31/0.58 22[0:Res:13.0,12.0] || -> greater(appear(efficient_producers,e),appear(first_movers,sk2))*r. % 0.31/0.58 21[0:Res:13.0,1.0] || -> greater(number_of_organizations(e,appear(an_organisation,sk2)),zero)*l. % 0.31/0.58 6[0:Inp] environment(u) || -> greater_or_equal(appear(first_movers,u),appear(an_organisation,u))*. % 0.31/0.58 15[0:Inp] || equal(appear(first_movers,sk2),appear(an_organisation,sk2))** -> . % 0.31/0.58 10[0:Inp] || equal(u,v) -> greater_or_equal(u,v)*. % 0.31/0.58 23[0:Res:13.0,6.0] || -> greater_or_equal(appear(first_movers,sk2),appear(an_organisation,sk2))*. % 0.31/0.58 14[0:Inp] || -> in_environment(sk2,appear(an_organisation,sk2))*. % 0.31/0.58 13[0:Inp] || -> environment(sk2)*. % 0.31/0.58 % SZS output end Saturation %------------------------------------------------------------------------------