%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT038-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n028.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:19:53 AM UTC 2026 % Result : Satisfiable 0.57s 0.82s % Output : Saturation 0.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT038-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.10/0.37 % Computer : n028.cluster.edu % 0.10/0.37 % Model : x86_64 x86_64 % 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.37 % Memory : 8046.5625MB % 0.10/0.37 % OS : Linux 6.8.0-71-generic % 0.10/0.37 % CPULimit : 300 % 0.10/0.37 % WCLimit : 300 % 0.10/0.37 % DateTime : Mon Sep 7 12:51:17 UTC 2026 % 0.10/0.37 % CPUTime : % 0.57/0.82 % 0.57/0.82 SPASS V 3.9 % 0.57/0.82 SPASS beiseite: Completion found. % 0.57/0.82 % SZS status CounterSatisfiable % 0.57/0.82 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.57/0.82 SPASS derived 366 clauses, backtracked 0 clauses, performed 0 splits and kept 232 clauses. % 0.57/0.82 SPASS allocated 76347 KBytes. % 0.57/0.82 SPASS spent 0:00:00.44 on the problem. % 0.57/0.82 0:00:00.06 for the input. % 0.57/0.82 0:00:00.00 for the FLOTTER CNF translation. % 0.57/0.82 0:00:00.04 for inferences. % 0.57/0.82 0:00:00.00 for the backtracking. % 0.57/0.82 0:00:00.28 for the reduction. % 0.57/0.82 % 0.57/0.82 % 0.57/0.82 The saturated set of worked-off clauses is : % 0.57/0.82 % SZS output start Saturation % 0.57/0.82 6[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.57/0.82 394[0:NCh:6.2,6.0,356.8,3.2] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) finite_set(x1) || greater(x2,sk2(v))* in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(sk1(sk1(sk1(x2,x1),z),y),x),w)+ contracts_from(sk1(sk1(sk1(x2,x1),z),y),x) contracts_from(sk1(sk1(x2,x1),z),y) contracts_from(sk1(x2,x1),z) contracts_from(x2,x1) -> in_environment(u,sk1(sk1(sk1(sk1(sk1(x2,x1),z),y),x),w))*. % 0.57/0.82 384[0:Res:3.2,347.7] finite_set(u) stable(v) environment(v) environment(w) finite_set(x) finite_set(y) finite_set(z) finite_set(x1) || contracts_from(appear(efficient_producers,e),u) in_environment(v,appear(first_movers,w))* contracts_from(sk1(sk1(sk1(sk1(appear(efficient_producers,e),u),x1),z),y),x)+ contracts_from(sk1(sk1(sk1(appear(efficient_producers,e),u),x1),z),y) contracts_from(sk1(sk1(appear(efficient_producers,e),u),x1),z) contracts_from(sk1(appear(efficient_producers,e),u),x1) -> in_environment(v,sk1(sk1(sk1(sk1(sk1(appear(efficient_producers,e),u),x1),z),y),x))*. % 0.57/0.82 385[0:NCh:6.2,6.0,347.7,3.2] stable(u) environment(u) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) finite_set(x1) || greater(x2,appear(efficient_producers,e)) in_environment(u,appear(first_movers,v))* contracts_from(sk1(sk1(sk1(sk1(x2,x1),z),y),x),w)+ contracts_from(sk1(sk1(sk1(x2,x1),z),y),x) contracts_from(sk1(sk1(x2,x1),z),y) contracts_from(sk1(x2,x1),z) contracts_from(x2,x1) -> in_environment(u,sk1(sk1(sk1(sk1(sk1(x2,x1),z),y),x),w))*. % 0.57/0.82 392[0:NCh:6.2,6.0,356.8,9.1] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) environment(x1) || greater(appear(first_movers,x1),sk2(v))*+ in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(sk1(sk1(appear(efficient_producers,e),z),y),x),w) contracts_from(sk1(sk1(appear(efficient_producers,e),z),y),x) contracts_from(sk1(appear(efficient_producers,e),z),y) contracts_from(appear(efficient_producers,e),z) -> in_environment(u,sk1(sk1(sk1(sk1(appear(efficient_producers,e),z),y),x),w))*. % 0.57/0.82 389[0:Res:3.2,356.8] finite_set(u) stable(v) environment(v) stable(w) environment(w) finite_set(x) finite_set(y) finite_set(z) finite_set(x1) || contracts_from(sk2(w),u) in_environment(v,appear(efficient_producers,w)) contracts_from(sk1(sk1(sk1(sk1(sk2(w),u),x1),z),y),x) contracts_from(sk1(sk1(sk1(sk2(w),u),x1),z),y) contracts_from(sk1(sk1(sk2(w),u),x1),z) contracts_from(sk1(sk2(w),u),x1) -> in_environment(v,sk1(sk1(sk1(sk1(sk1(sk2(w),u),x1),z),y),x))*. % 0.57/0.82 395[0:NCh:6.2,6.0,356.8,3.2] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) finite_set(x1) || equal(x2,sk2(v))* in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(sk1(sk1(sk1(x2,x1),z),y),x),w)+ contracts_from(sk1(sk1(sk1(x2,x1),z),y),x) contracts_from(sk1(sk1(x2,x1),z),y) contracts_from(sk1(x2,x1),z) contracts_from(x2,x1) -> in_environment(u,sk1(sk1(sk1(sk1(sk1(x2,x1),z),y),x),w))*. % 0.57/0.82 390[0:NCh:6.2,6.0,356.8,19.0] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) || greater(appear(first_movers,sk3),sk2(v))+ in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(sk1(sk1(appear(efficient_producers,e),z),y),x),w) contracts_from(sk1(sk1(appear(efficient_producers,e),z),y),x) contracts_from(sk1(appear(efficient_producers,e),z),y) contracts_from(appear(efficient_producers,e),z) -> in_environment(u,sk1(sk1(sk1(sk1(appear(efficient_producers,e),z),y),x),w))*. % 0.57/0.82 381[0:NCh:6.2,6.0,343.6,3.2] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) || greater(x1,sk2(u))* in_environment(sk3,appear(efficient_producers,u))* contracts_from(sk1(sk1(sk1(sk1(x1,z),y),x),w),v)+ contracts_from(sk1(sk1(sk1(x1,z),y),x),w) contracts_from(sk1(sk1(x1,z),y),x) contracts_from(sk1(x1,z),y) contracts_from(x1,z) -> in_environment(sk3,sk1(sk1(sk1(sk1(sk1(x1,z),y),x),w),v))*. % 0.57/0.82 386[0:NCh:6.2,6.0,347.7,3.2] stable(u) environment(u) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) finite_set(x1) || equal(x2,appear(efficient_producers,e)) in_environment(u,appear(first_movers,v))* contracts_from(sk1(sk1(sk1(sk1(x2,x1),z),y),x),w)+ contracts_from(sk1(sk1(sk1(x2,x1),z),y),x) contracts_from(sk1(sk1(x2,x1),z),y) contracts_from(sk1(x2,x1),z) contracts_from(x2,x1) -> in_environment(u,sk1(sk1(sk1(sk1(sk1(x2,x1),z),y),x),w))*. % 0.57/0.82 393[0:NCh:6.2,6.0,356.8,9.1] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) environment(x1) || equal(appear(first_movers,x1),sk2(v))* in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(sk1(sk1(appear(efficient_producers,e),z),y),x),w)+ contracts_from(sk1(sk1(appear(efficient_producers,e),z),y),x) contracts_from(sk1(appear(efficient_producers,e),z),y) contracts_from(appear(efficient_producers,e),z) -> in_environment(u,sk1(sk1(sk1(sk1(appear(efficient_producers,e),z),y),x),w))*. % 0.57/0.82 371[0:Res:3.2,334.5] finite_set(u) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) || contracts_from(appear(efficient_producers,e),u) in_environment(sk3,appear(first_movers,v))* contracts_from(sk1(sk1(sk1(sk1(appear(efficient_producers,e),u),z),y),x),w)+ contracts_from(sk1(sk1(sk1(appear(efficient_producers,e),u),z),y),x) contracts_from(sk1(sk1(appear(efficient_producers,e),u),z),y) contracts_from(sk1(appear(efficient_producers,e),u),z) -> in_environment(sk3,sk1(sk1(sk1(sk1(sk1(appear(efficient_producers,e),u),z),y),x),w))*. % 0.57/0.82 372[0:NCh:6.2,6.0,334.5,3.2] environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) || greater(x1,appear(efficient_producers,e)) in_environment(sk3,appear(first_movers,u))* contracts_from(sk1(sk1(sk1(sk1(x1,z),y),x),w),v)+ contracts_from(sk1(sk1(sk1(x1,z),y),x),w) contracts_from(sk1(sk1(x1,z),y),x) contracts_from(sk1(x1,z),y) contracts_from(x1,z) -> in_environment(sk3,sk1(sk1(sk1(sk1(sk1(x1,z),y),x),w),v))*. % 0.57/0.82 379[0:NCh:6.2,6.0,343.6,9.1] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) environment(z) || greater(appear(first_movers,z),sk2(u))*+ in_environment(sk3,appear(efficient_producers,u))* contracts_from(sk1(sk1(sk1(appear(efficient_producers,e),y),x),w),v) contracts_from(sk1(sk1(appear(efficient_producers,e),y),x),w) contracts_from(sk1(appear(efficient_producers,e),y),x) contracts_from(appear(efficient_producers,e),y) -> in_environment(sk3,sk1(sk1(sk1(sk1(appear(efficient_producers,e),y),x),w),v))*. % 0.57/0.82 376[0:Res:3.2,343.6] finite_set(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) || contracts_from(sk2(v),u) in_environment(sk3,appear(efficient_producers,v)) contracts_from(sk1(sk1(sk1(sk1(sk2(v),u),z),y),x),w) contracts_from(sk1(sk1(sk1(sk2(v),u),z),y),x) contracts_from(sk1(sk1(sk2(v),u),z),y) contracts_from(sk1(sk2(v),u),z) -> in_environment(sk3,sk1(sk1(sk1(sk1(sk1(sk2(v),u),z),y),x),w))*. % 0.57/0.82 391[0:NCh:6.2,6.0,356.8,19.0] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) || equal(appear(first_movers,sk3),sk2(v)) in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(sk1(sk1(appear(efficient_producers,e),z),y),x),w)+ contracts_from(sk1(sk1(appear(efficient_producers,e),z),y),x) contracts_from(sk1(appear(efficient_producers,e),z),y) contracts_from(appear(efficient_producers,e),z) -> in_environment(u,sk1(sk1(sk1(sk1(appear(efficient_producers,e),z),y),x),w))*. % 0.57/0.82 382[0:NCh:6.2,6.0,343.6,3.2] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) || equal(x1,sk2(u))* in_environment(sk3,appear(efficient_producers,u))* contracts_from(sk1(sk1(sk1(sk1(x1,z),y),x),w),v)+ contracts_from(sk1(sk1(sk1(x1,z),y),x),w) contracts_from(sk1(sk1(x1,z),y),x) contracts_from(sk1(x1,z),y) contracts_from(x1,z) -> in_environment(sk3,sk1(sk1(sk1(sk1(sk1(x1,z),y),x),w),v))*. % 0.57/0.82 377[0:NCh:6.2,6.0,343.6,19.0] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) || greater(appear(first_movers,sk3),sk2(u))+ in_environment(sk3,appear(efficient_producers,u))* contracts_from(sk1(sk1(sk1(appear(efficient_producers,e),y),x),w),v) contracts_from(sk1(sk1(appear(efficient_producers,e),y),x),w) contracts_from(sk1(appear(efficient_producers,e),y),x) contracts_from(appear(efficient_producers,e),y) -> in_environment(sk3,sk1(sk1(sk1(sk1(appear(efficient_producers,e),y),x),w),v))*. % 0.57/0.82 373[0:NCh:6.2,6.0,334.5,3.2] environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) || equal(x1,appear(efficient_producers,e)) in_environment(sk3,appear(first_movers,u))* contracts_from(sk1(sk1(sk1(sk1(x1,z),y),x),w),v)+ contracts_from(sk1(sk1(sk1(x1,z),y),x),w) contracts_from(sk1(sk1(x1,z),y),x) contracts_from(sk1(x1,z),y) contracts_from(x1,z) -> in_environment(sk3,sk1(sk1(sk1(sk1(sk1(x1,z),y),x),w),v))*. % 0.57/0.82 380[0:NCh:6.2,6.0,343.6,9.1] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) environment(z) || equal(appear(first_movers,z),sk2(u))* in_environment(sk3,appear(efficient_producers,u))* contracts_from(sk1(sk1(sk1(appear(efficient_producers,e),y),x),w),v)+ contracts_from(sk1(sk1(appear(efficient_producers,e),y),x),w) contracts_from(sk1(appear(efficient_producers,e),y),x) contracts_from(appear(efficient_producers,e),y) -> in_environment(sk3,sk1(sk1(sk1(sk1(appear(efficient_producers,e),y),x),w),v))*. % 0.57/0.82 387[0:NCh:6.2,6.1,347.7,7.2] stable(u) environment(u) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) stable(e) environment(e) || greater(x1,sk2(e)) in_environment(u,appear(first_movers,v))* contracts_from(sk1(sk1(sk1(x1,z),y),x),w) contracts_from(sk1(sk1(x1,z),y),x) contracts_from(sk1(x1,z),y) contracts_from(x1,z) -> in_environment(u,sk1(sk1(sk1(sk1(x1,z),y),x),w))*. % 0.57/0.82 378[0:NCh:6.2,6.0,343.6,19.0] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) || equal(appear(first_movers,sk3),sk2(u)) in_environment(sk3,appear(efficient_producers,u))* contracts_from(sk1(sk1(sk1(appear(efficient_producers,e),y),x),w),v)+ contracts_from(sk1(sk1(appear(efficient_producers,e),y),x),w) contracts_from(sk1(appear(efficient_producers,e),y),x) contracts_from(appear(efficient_producers,e),y) -> in_environment(sk3,sk1(sk1(sk1(sk1(appear(efficient_producers,e),y),x),w),v))*. % 0.57/0.82 356[0:NCh:6.2,6.0,307.7,3.2] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) || greater(x1,sk2(v))*+ in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(sk1(sk1(x1,z),y),x),w) contracts_from(sk1(sk1(x1,z),y),x) contracts_from(sk1(x1,z),y) contracts_from(x1,z) -> in_environment(u,sk1(sk1(sk1(sk1(x1,z),y),x),w))*. % 0.57/0.82 388[0:NCh:6.2,6.1,347.7,7.2] stable(u) environment(u) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) stable(e) environment(e) || equal(x1,sk2(e)) in_environment(u,appear(first_movers,v))* contracts_from(sk1(sk1(sk1(x1,z),y),x),w) contracts_from(sk1(sk1(x1,z),y),x) contracts_from(sk1(x1,z),y) contracts_from(x1,z) -> in_environment(u,sk1(sk1(sk1(sk1(x1,z),y),x),w))*. % 0.57/0.82 383[0:Res:7.2,347.7] stable(e) environment(e) stable(u) environment(u) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) || in_environment(u,appear(first_movers,v))* contracts_from(sk1(sk1(sk1(sk2(e),z),y),x),w) contracts_from(sk1(sk1(sk2(e),z),y),x) contracts_from(sk1(sk2(e),z),y) contracts_from(sk2(e),z) -> in_environment(u,sk1(sk1(sk1(sk1(sk2(e),z),y),x),w))*. % 0.57/0.82 347[0:NCh:6.2,6.0,274.6,3.2] stable(u) environment(u) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) || greater(x1,appear(efficient_producers,e))+ in_environment(u,appear(first_movers,v))* contracts_from(sk1(sk1(sk1(x1,z),y),x),w) contracts_from(sk1(sk1(x1,z),y),x) contracts_from(sk1(x1,z),y) contracts_from(x1,z) -> in_environment(u,sk1(sk1(sk1(sk1(x1,z),y),x),w))*. % 0.57/0.82 354[0:NCh:6.2,6.0,307.7,9.1] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) environment(z) || greater(appear(first_movers,z),sk2(v))*+ in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(sk1(appear(efficient_producers,e),y),x),w) contracts_from(sk1(appear(efficient_producers,e),y),x) contracts_from(appear(efficient_producers,e),y) -> in_environment(u,sk1(sk1(sk1(appear(efficient_producers,e),y),x),w))*. % 0.57/0.82 374[0:NCh:6.2,6.1,334.5,7.2] environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) stable(e) environment(e) || greater(z,sk2(e)) in_environment(sk3,appear(first_movers,u))* contracts_from(sk1(sk1(sk1(z,y),x),w),v) contracts_from(sk1(sk1(z,y),x),w) contracts_from(sk1(z,y),x) contracts_from(z,y) -> in_environment(sk3,sk1(sk1(sk1(sk1(z,y),x),w),v))*. % 0.57/0.82 346[0:Res:3.2,274.6] finite_set(u) stable(v) environment(v) environment(w) finite_set(x) finite_set(y) finite_set(z) || contracts_from(appear(efficient_producers,e),u) in_environment(v,appear(first_movers,w))* contracts_from(sk1(sk1(sk1(appear(efficient_producers,e),u),z),y),x)+ contracts_from(sk1(sk1(appear(efficient_producers,e),u),z),y) contracts_from(sk1(appear(efficient_producers,e),u),z) -> in_environment(v,sk1(sk1(sk1(sk1(appear(efficient_producers,e),u),z),y),x))*. % 0.57/0.82 357[0:NCh:6.2,6.0,307.7,3.2] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) || equal(x1,sk2(v))* in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(sk1(sk1(x1,z),y),x),w)+ contracts_from(sk1(sk1(x1,z),y),x) contracts_from(sk1(x1,z),y) contracts_from(x1,z) -> in_environment(u,sk1(sk1(sk1(sk1(x1,z),y),x),w))*. % 0.57/0.82 351[0:Res:3.2,307.7] finite_set(u) stable(v) environment(v) stable(w) environment(w) finite_set(x) finite_set(y) finite_set(z) || contracts_from(sk2(w),u) in_environment(v,appear(efficient_producers,w)) contracts_from(sk1(sk1(sk1(sk2(w),u),z),y),x) contracts_from(sk1(sk1(sk2(w),u),z),y) contracts_from(sk1(sk2(w),u),z) -> in_environment(v,sk1(sk1(sk1(sk1(sk2(w),u),z),y),x))*. % 0.57/0.82 352[0:NCh:6.2,6.0,307.7,19.0] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) || greater(appear(first_movers,sk3),sk2(v))+ in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(sk1(appear(efficient_producers,e),y),x),w) contracts_from(sk1(appear(efficient_producers,e),y),x) contracts_from(appear(efficient_producers,e),y) -> in_environment(u,sk1(sk1(sk1(appear(efficient_producers,e),y),x),w))*. % 0.57/0.82 343[0:NCh:6.2,6.0,267.5,3.2] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) || greater(z,sk2(u))*+ in_environment(sk3,appear(efficient_producers,u))* contracts_from(sk1(sk1(sk1(z,y),x),w),v) contracts_from(sk1(sk1(z,y),x),w) contracts_from(sk1(z,y),x) contracts_from(z,y) -> in_environment(sk3,sk1(sk1(sk1(sk1(z,y),x),w),v))*. % 0.57/0.82 348[0:NCh:6.2,6.0,274.6,3.2] stable(u) environment(u) environment(v) finite_set(w) finite_set(x) finite_set(y) finite_set(z) || equal(x1,appear(efficient_producers,e)) in_environment(u,appear(first_movers,v))* contracts_from(sk1(sk1(sk1(x1,z),y),x),w)+ contracts_from(sk1(sk1(x1,z),y),x) contracts_from(sk1(x1,z),y) contracts_from(x1,z) -> in_environment(u,sk1(sk1(sk1(sk1(x1,z),y),x),w))*. % 0.57/0.82 375[0:NCh:6.2,6.1,334.5,7.2] environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) stable(e) environment(e) || equal(z,sk2(e)) in_environment(sk3,appear(first_movers,u))* contracts_from(sk1(sk1(sk1(z,y),x),w),v) contracts_from(sk1(sk1(z,y),x),w) contracts_from(sk1(z,y),x) contracts_from(z,y) -> in_environment(sk3,sk1(sk1(sk1(sk1(z,y),x),w),v))*. % 0.57/0.82 355[0:NCh:6.2,6.0,307.7,9.1] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) environment(z) || equal(appear(first_movers,z),sk2(v))* in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(sk1(appear(efficient_producers,e),y),x),w)+ contracts_from(sk1(appear(efficient_producers,e),y),x) contracts_from(appear(efficient_producers,e),y) -> in_environment(u,sk1(sk1(sk1(appear(efficient_producers,e),y),x),w))*. % 0.57/0.82 370[0:Res:7.2,334.5] stable(e) environment(e) environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) || in_environment(sk3,appear(first_movers,u))* contracts_from(sk1(sk1(sk1(sk2(e),y),x),w),v) contracts_from(sk1(sk1(sk2(e),y),x),w) contracts_from(sk1(sk2(e),y),x) contracts_from(sk2(e),y) -> in_environment(sk3,sk1(sk1(sk1(sk1(sk2(e),y),x),w),v))*. % 0.57/0.82 334[0:NCh:6.2,6.0,257.4,3.2] environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) || greater(z,appear(efficient_producers,e))+ in_environment(sk3,appear(first_movers,u))* contracts_from(sk1(sk1(sk1(z,y),x),w),v) contracts_from(sk1(sk1(z,y),x),w) contracts_from(sk1(z,y),x) contracts_from(z,y) -> in_environment(sk3,sk1(sk1(sk1(sk1(z,y),x),w),v))*. % 0.57/0.82 364[0:NCh:6.2,6.1,322.6,24.0] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) environment(y) || greater(appear(first_movers,y),sk2(sk3))*l+ in_environment(u,appear(efficient_producers,sk3)) contracts_from(sk1(sk1(appear(efficient_producers,e),x),w),v) contracts_from(sk1(appear(efficient_producers,e),x),w) contracts_from(appear(efficient_producers,e),x) -> in_environment(u,sk1(sk1(sk1(appear(efficient_producers,e),x),w),v))*. % 0.57/0.82 333[0:Res:3.2,257.4] finite_set(u) environment(v) finite_set(w) finite_set(x) finite_set(y) || contracts_from(appear(efficient_producers,e),u) in_environment(sk3,appear(first_movers,v))* contracts_from(sk1(sk1(sk1(appear(efficient_producers,e),u),y),x),w)+ contracts_from(sk1(sk1(appear(efficient_producers,e),u),y),x) contracts_from(sk1(appear(efficient_producers,e),u),y) -> in_environment(sk3,sk1(sk1(sk1(sk1(appear(efficient_producers,e),u),y),x),w))*. % 0.57/0.82 324[0:NCh:6.2,6.0,245.5,3.2] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) || greater(z,x1)* in_environment(u,x1)* contracts_from(sk1(sk1(sk1(z,y),x),w),v)+ contracts_from(sk1(sk1(z,y),x),w) contracts_from(sk1(z,y),x) contracts_from(z,y) -> in_environment(u,sk1(sk1(sk1(sk1(z,y),x),w),v))*. % 0.57/0.82 353[0:NCh:6.2,6.0,307.7,19.0] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) || equal(appear(first_movers,sk3),sk2(v)) in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(sk1(appear(efficient_producers,e),y),x),w)+ contracts_from(sk1(appear(efficient_producers,e),y),x) contracts_from(appear(efficient_producers,e),y) -> in_environment(u,sk1(sk1(sk1(appear(efficient_producers,e),y),x),w))*. % 0.57/0.82 344[0:NCh:6.2,6.0,267.5,3.2] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) || equal(z,sk2(u))* in_environment(sk3,appear(efficient_producers,u))* contracts_from(sk1(sk1(sk1(z,y),x),w),v)+ contracts_from(sk1(sk1(z,y),x),w) contracts_from(sk1(z,y),x) contracts_from(z,y) -> in_environment(sk3,sk1(sk1(sk1(sk1(z,y),x),w),v))*. % 0.57/0.82 338[0:Res:3.2,267.5] finite_set(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) || contracts_from(sk2(v),u) in_environment(sk3,appear(efficient_producers,v)) contracts_from(sk1(sk1(sk1(sk2(v),u),y),x),w) contracts_from(sk1(sk1(sk2(v),u),y),x) contracts_from(sk1(sk2(v),u),y) -> in_environment(sk3,sk1(sk1(sk1(sk1(sk2(v),u),y),x),w))*. % 0.57/0.82 365[0:NCh:6.2,6.1,322.6,24.0] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) environment(y) || equal(appear(first_movers,y),sk2(sk3))** in_environment(u,appear(efficient_producers,sk3)) contracts_from(sk1(sk1(appear(efficient_producers,e),x),w),v)+ contracts_from(sk1(appear(efficient_producers,e),x),w) contracts_from(appear(efficient_producers,e),x) -> in_environment(u,sk1(sk1(sk1(appear(efficient_producers,e),x),w),v))*. % 0.57/0.82 322[0:NCh:6.2,6.0,245.5,9.1] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) environment(y) || greater(appear(first_movers,y),z)*+ in_environment(u,z)* contracts_from(sk1(sk1(appear(efficient_producers,e),x),w),v) contracts_from(sk1(appear(efficient_producers,e),x),w) contracts_from(appear(efficient_producers,e),x) -> in_environment(u,sk1(sk1(sk1(appear(efficient_producers,e),x),w),v))*. % 0.57/0.82 358[0:NCh:6.2,6.1,320.5,24.0] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) || greater(appear(first_movers,sk3),sk2(sk3)) in_environment(u,appear(efficient_producers,sk3)) contracts_from(sk1(sk1(appear(efficient_producers,e),x),w),v) contracts_from(sk1(appear(efficient_producers,e),x),w) contracts_from(appear(efficient_producers,e),x) -> in_environment(u,sk1(sk1(sk1(appear(efficient_producers,e),x),w),v))*. % 0.57/0.82 349[0:NCh:6.2,6.1,274.6,7.2] stable(u) environment(u) environment(v) finite_set(w) finite_set(x) finite_set(y) stable(e) environment(e) || greater(z,sk2(e)) in_environment(u,appear(first_movers,v))* contracts_from(sk1(sk1(z,y),x),w) contracts_from(sk1(z,y),x) contracts_from(z,y) -> in_environment(u,sk1(sk1(sk1(z,y),x),w))*. % 0.57/0.82 335[0:NCh:6.2,6.0,257.4,3.2] environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) || equal(z,appear(efficient_producers,e)) in_environment(sk3,appear(first_movers,u))* contracts_from(sk1(sk1(sk1(z,y),x),w),v)+ contracts_from(sk1(sk1(z,y),x),w) contracts_from(sk1(z,y),x) contracts_from(z,y) -> in_environment(sk3,sk1(sk1(sk1(sk1(z,y),x),w),v))*. % 0.57/0.82 359[0:NCh:6.2,6.1,320.5,24.0] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) || equal(appear(first_movers,sk3),sk2(sk3)) in_environment(u,appear(efficient_producers,sk3)) contracts_from(sk1(sk1(appear(efficient_producers,e),x),w),v) contracts_from(sk1(appear(efficient_producers,e),x),w) contracts_from(appear(efficient_producers,e),x) -> in_environment(u,sk1(sk1(sk1(appear(efficient_producers,e),x),w),v))*. % 0.57/0.82 325[0:NCh:6.2,6.0,245.5,3.2] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) finite_set(y) || equal(z,x1)* in_environment(u,x1)* contracts_from(sk1(sk1(sk1(z,y),x),w),v)+ contracts_from(sk1(sk1(z,y),x),w) contracts_from(sk1(z,y),x) contracts_from(z,y) -> in_environment(u,sk1(sk1(sk1(sk1(z,y),x),w),v))*. % 0.57/0.82 320[0:NCh:6.2,6.0,245.5,19.0] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) || greater(appear(first_movers,sk3),y)*+ in_environment(u,y)* contracts_from(sk1(sk1(appear(efficient_producers,e),x),w),v) contracts_from(sk1(appear(efficient_producers,e),x),w) contracts_from(appear(efficient_producers,e),x) -> in_environment(u,sk1(sk1(sk1(appear(efficient_producers,e),x),w),v))*. % 0.57/0.82 287[0:NCh:6.2,6.0,201.4,3.2] finite_set(u) finite_set(v) finite_set(w) finite_set(x) || contracts_from(sk1(sk1(sk1(y,x),w),v),u)+ greater(y,z)* in_environment(sk3,z)* contracts_from(sk1(sk1(y,x),w),v) contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(sk3,sk1(sk1(sk1(sk1(y,x),w),v),u))*. % 0.57/0.82 307[0:NCh:6.2,6.0,234.6,3.2] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) || greater(z,sk2(v))*+ in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(sk1(z,y),x),w) contracts_from(sk1(z,y),x) contracts_from(z,y) -> in_environment(u,sk1(sk1(sk1(z,y),x),w))*. % 0.57/0.82 350[0:NCh:6.2,6.1,274.6,7.2] stable(u) environment(u) environment(v) finite_set(w) finite_set(x) finite_set(y) stable(e) environment(e) || equal(z,sk2(e)) in_environment(u,appear(first_movers,v))* contracts_from(sk1(sk1(z,y),x),w) contracts_from(sk1(z,y),x) contracts_from(z,y) -> in_environment(u,sk1(sk1(sk1(z,y),x),w))*. % 0.57/0.82 323[0:NCh:6.2,6.0,245.5,9.1] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) environment(y) || equal(appear(first_movers,y),z)* in_environment(u,z)* contracts_from(sk1(sk1(appear(efficient_producers,e),x),w),v)+ contracts_from(sk1(appear(efficient_producers,e),x),w) contracts_from(appear(efficient_producers,e),x) -> in_environment(u,sk1(sk1(sk1(appear(efficient_producers,e),x),w),v))*. % 0.57/0.82 345[0:Res:7.2,274.6] stable(e) environment(e) stable(u) environment(u) environment(v) finite_set(w) finite_set(x) finite_set(y) || in_environment(u,appear(first_movers,v))* contracts_from(sk1(sk1(sk2(e),y),x),w) contracts_from(sk1(sk2(e),y),x) contracts_from(sk2(e),y) -> in_environment(u,sk1(sk1(sk1(sk2(e),y),x),w))*. % 0.57/0.82 274[0:NCh:6.2,6.0,218.5,3.2] stable(u) environment(u) environment(v) finite_set(w) finite_set(x) finite_set(y) || greater(z,appear(efficient_producers,e))+ in_environment(u,appear(first_movers,v))* contracts_from(sk1(sk1(z,y),x),w) contracts_from(sk1(z,y),x) contracts_from(z,y) -> in_environment(u,sk1(sk1(sk1(z,y),x),w))*. % 0.57/0.82 305[0:NCh:6.2,6.0,234.6,9.1] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) environment(y) || greater(appear(first_movers,y),sk2(v))*+ in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(appear(efficient_producers,e),x),w) contracts_from(appear(efficient_producers,e),x) -> in_environment(u,sk1(sk1(appear(efficient_producers,e),x),w))*. % 0.57/0.82 336[0:NCh:6.2,6.1,257.4,7.2] environment(u) finite_set(v) finite_set(w) finite_set(x) stable(e) environment(e) || greater(y,sk2(e)) in_environment(sk3,appear(first_movers,u))* contracts_from(sk1(sk1(y,x),w),v) contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(sk3,sk1(sk1(sk1(y,x),w),v))*. % 0.57/0.82 319[0:Res:3.2,245.5] finite_set(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) || contracts_from(z,u) in_environment(v,z) contracts_from(sk1(sk1(sk1(z,u),y),x),w) contracts_from(sk1(sk1(z,u),y),x) contracts_from(sk1(z,u),y) -> in_environment(v,sk1(sk1(sk1(sk1(z,u),y),x),w))*. % 0.57/0.82 321[0:NCh:6.2,6.0,245.5,19.0] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) || equal(appear(first_movers,sk3),y)* in_environment(u,y)* contracts_from(sk1(sk1(appear(efficient_producers,e),x),w),v)+ contracts_from(sk1(appear(efficient_producers,e),x),w) contracts_from(appear(efficient_producers,e),x) -> in_environment(u,sk1(sk1(sk1(appear(efficient_producers,e),x),w),v))*. % 0.57/0.82 288[0:NCh:6.2,6.0,201.4,3.2] finite_set(u) finite_set(v) finite_set(w) finite_set(x) || contracts_from(sk1(sk1(sk1(y,x),w),v),u)+ equal(y,z)* in_environment(sk3,z)* contracts_from(sk1(sk1(y,x),w),v) contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(sk3,sk1(sk1(sk1(sk1(y,x),w),v),u))*. % 0.57/0.82 308[0:NCh:6.2,6.0,234.6,3.2] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) finite_set(y) || equal(z,sk2(v))* in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(sk1(z,y),x),w)+ contracts_from(sk1(z,y),x) contracts_from(z,y) -> in_environment(u,sk1(sk1(sk1(z,y),x),w))*. % 0.57/0.82 273[0:Res:3.2,218.5] finite_set(u) stable(v) environment(v) environment(w) finite_set(x) finite_set(y) || contracts_from(appear(efficient_producers,e),u) in_environment(v,appear(first_movers,w))* contracts_from(sk1(sk1(appear(efficient_producers,e),u),y),x)+ contracts_from(sk1(appear(efficient_producers,e),u),y) -> in_environment(v,sk1(sk1(sk1(appear(efficient_producers,e),u),y),x))*. % 0.57/0.82 300[0:NCh:6.2,6.1,241.4,7.2] stable(u) environment(u) finite_set(v) finite_set(w) stable(x) environment(x) || greater(appear(first_movers,sk3),sk2(x))+ in_environment(u,appear(efficient_producers,x))* contracts_from(sk1(appear(efficient_producers,e),w),v) contracts_from(appear(efficient_producers,e),w) -> in_environment(u,sk1(sk1(appear(efficient_producers,e),w),v))*. % 0.57/0.82 302[0:Res:3.2,234.6] finite_set(u) stable(v) environment(v) stable(w) environment(w) finite_set(x) finite_set(y) || contracts_from(sk2(w),u) in_environment(v,appear(efficient_producers,w)) contracts_from(sk1(sk1(sk2(w),u),y),x) contracts_from(sk1(sk2(w),u),y) -> in_environment(v,sk1(sk1(sk1(sk2(w),u),y),x))*. % 0.57/0.82 326[0:NCh:6.2,6.1,245.5,24.0] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) || greater(y,sk2(sk3)) in_environment(u,appear(efficient_producers,sk3)) contracts_from(sk1(sk1(y,x),w),v) contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(u,sk1(sk1(sk1(y,x),w),v))*. % 0.57/0.82 267[0:NCh:6.2,6.0,186.4,3.2] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) || greater(y,sk2(u))*+ in_environment(sk3,appear(efficient_producers,u))* contracts_from(sk1(sk1(y,x),w),v) contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(sk3,sk1(sk1(sk1(y,x),w),v))*. % 0.57/0.82 275[0:NCh:6.2,6.0,218.5,3.2] stable(u) environment(u) environment(v) finite_set(w) finite_set(x) finite_set(y) || equal(z,appear(efficient_producers,e)) in_environment(u,appear(first_movers,v))* contracts_from(sk1(sk1(z,y),x),w)+ contracts_from(sk1(z,y),x) contracts_from(z,y) -> in_environment(u,sk1(sk1(sk1(z,y),x),w))*. % 0.57/0.82 306[0:NCh:6.2,6.0,234.6,9.1] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) environment(y) || equal(appear(first_movers,y),sk2(v))* in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(appear(efficient_producers,e),x),w)+ contracts_from(appear(efficient_producers,e),x) -> in_environment(u,sk1(sk1(appear(efficient_producers,e),x),w))*. % 0.57/0.82 337[0:NCh:6.2,6.1,257.4,7.2] environment(u) finite_set(v) finite_set(w) finite_set(x) stable(e) environment(e) || equal(y,sk2(e)) in_environment(sk3,appear(first_movers,u))* contracts_from(sk1(sk1(y,x),w),v) contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(sk3,sk1(sk1(sk1(y,x),w),v))*. % 0.57/0.82 332[0:Res:7.2,257.4] stable(e) environment(e) environment(u) finite_set(v) finite_set(w) finite_set(x) || in_environment(sk3,appear(first_movers,u))* contracts_from(sk1(sk1(sk2(e),x),w),v) contracts_from(sk1(sk2(e),x),w) contracts_from(sk2(e),x) -> in_environment(sk3,sk1(sk1(sk1(sk2(e),x),w),v))*. % 0.57/0.82 257[0:NCh:6.2,6.0,176.3,3.2] environment(u) finite_set(v) finite_set(w) finite_set(x) || greater(y,appear(efficient_producers,e))+ in_environment(sk3,appear(first_movers,u))* contracts_from(sk1(sk1(y,x),w),v) contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(sk3,sk1(sk1(sk1(y,x),w),v))*. % 0.57/0.82 316[0:Res:19.0,245.5] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) || in_environment(u,appear(first_movers,sk3)) contracts_from(sk1(sk1(appear(efficient_producers,e),x),w),v) contracts_from(sk1(appear(efficient_producers,e),x),w) contracts_from(appear(efficient_producers,e),x) -> in_environment(u,sk1(sk1(sk1(appear(efficient_producers,e),x),w),v))*. % 0.57/0.82 309[0:NCh:6.2,6.1,243.5,24.0] stable(u) environment(u) finite_set(v) finite_set(w) environment(x) || greater(appear(first_movers,x),sk2(sk3))*l+ in_environment(u,appear(efficient_producers,sk3)) contracts_from(sk1(appear(efficient_producers,e),w),v) contracts_from(appear(efficient_producers,e),w) -> in_environment(u,sk1(sk1(appear(efficient_producers,e),w),v))*. % 0.57/0.82 282[0:Res:3.2,201.4] finite_set(u) finite_set(v) finite_set(w) finite_set(x) || contracts_from(y,u) contracts_from(sk1(sk1(sk1(y,u),x),w),v) in_environment(sk3,y) contracts_from(sk1(sk1(y,u),x),w) contracts_from(sk1(y,u),x) -> in_environment(sk3,sk1(sk1(sk1(sk1(y,u),x),w),v))*. % 0.57/0.82 276[0:NCh:6.2,6.1,218.5,7.2] stable(u) environment(u) environment(v) finite_set(w) finite_set(x) stable(e) environment(e) || greater(y,sk2(e)) in_environment(u,appear(first_movers,v))* contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(u,sk1(sk1(y,x),w))*. % 0.57/0.82 327[0:NCh:6.2,6.1,245.5,24.0] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) || equal(y,sk2(sk3)) in_environment(u,appear(efficient_producers,sk3)) contracts_from(sk1(sk1(y,x),w),v) contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(u,sk1(sk1(sk1(y,x),w),v))*. % 0.57/0.82 315[0:Res:24.0,245.5] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) || in_environment(u,appear(efficient_producers,sk3)) contracts_from(sk1(sk1(sk2(sk3),x),w),v) contracts_from(sk1(sk2(sk3),x),w) contracts_from(sk2(sk3),x) -> in_environment(u,sk1(sk1(sk1(sk2(sk3),x),w),v))*. % 0.57/0.82 245[0:NCh:6.2,6.0,165.4,3.2] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) || greater(y,z)*+ in_environment(u,z)* contracts_from(sk1(sk1(y,x),w),v) contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(u,sk1(sk1(sk1(y,x),w),v))*. % 0.57/0.82 301[0:NCh:6.2,6.1,241.4,7.2] stable(u) environment(u) finite_set(v) finite_set(w) stable(x) environment(x) || equal(appear(first_movers,sk3),sk2(x)) in_environment(u,appear(efficient_producers,x))* contracts_from(sk1(appear(efficient_producers,e),w),v)+ contracts_from(appear(efficient_producers,e),w) -> in_environment(u,sk1(sk1(appear(efficient_producers,e),w),v))*. % 0.57/0.82 268[0:NCh:6.2,6.0,186.4,3.2] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) || equal(y,sk2(u))* in_environment(sk3,appear(efficient_producers,u))* contracts_from(sk1(sk1(y,x),w),v)+ contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(sk3,sk1(sk1(sk1(y,x),w),v))*. % 0.57/0.82 296[0:NCh:6.2,6.1,241.4,24.0] stable(u) environment(u) finite_set(v) finite_set(w) || greater(appear(first_movers,sk3),sk2(sk3)) in_environment(u,appear(efficient_producers,sk3)) contracts_from(sk1(appear(efficient_producers,e),w),v) contracts_from(appear(efficient_producers,e),w) -> in_environment(u,sk1(sk1(appear(efficient_producers,e),w),v))*. % 0.57/0.82 310[0:NCh:6.2,6.1,243.5,24.0] stable(u) environment(u) finite_set(v) finite_set(w) environment(x) || equal(appear(first_movers,x),sk2(sk3))** in_environment(u,appear(efficient_producers,sk3)) contracts_from(sk1(appear(efficient_producers,e),w),v)+ contracts_from(appear(efficient_producers,e),w) -> in_environment(u,sk1(sk1(appear(efficient_producers,e),w),v))*. % 0.57/0.82 243[0:NCh:6.2,6.0,165.4,9.1] stable(u) environment(u) finite_set(v) finite_set(w) environment(x) || greater(appear(first_movers,x),y)*+ in_environment(u,y)* contracts_from(sk1(appear(efficient_producers,e),w),v) contracts_from(appear(efficient_producers,e),w) -> in_environment(u,sk1(sk1(appear(efficient_producers,e),w),v))*. % 0.57/0.82 262[0:Res:3.2,186.4] finite_set(u) stable(v) environment(v) finite_set(w) finite_set(x) || contracts_from(sk2(v),u) in_environment(sk3,appear(efficient_producers,v)) contracts_from(sk1(sk1(sk2(v),u),x),w) contracts_from(sk1(sk2(v),u),x) -> in_environment(sk3,sk1(sk1(sk1(sk2(v),u),x),w))*. % 0.57/0.82 289[0:NCh:6.2,6.1,201.4,24.0] finite_set(u) finite_set(v) finite_set(w) || contracts_from(sk1(sk1(x,w),v),u) greater(x,sk2(sk3)) in_environment(sk3,appear(efficient_producers,sk3)) contracts_from(sk1(x,w),v) contracts_from(x,w) -> in_environment(sk3,sk1(sk1(sk1(x,w),v),u))*. % 0.57/0.82 258[0:NCh:6.2,6.0,176.3,3.2] environment(u) finite_set(v) finite_set(w) finite_set(x) || equal(y,appear(efficient_producers,e)) in_environment(sk3,appear(first_movers,u))* contracts_from(sk1(sk1(y,x),w),v)+ contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(sk3,sk1(sk1(sk1(y,x),w),v))*. % 0.57/0.82 234[0:NCh:6.2,6.0,154.5,3.2] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) || greater(y,sk2(v))*+ in_environment(u,appear(efficient_producers,v))* contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(u,sk1(sk1(y,x),w))*. % 0.57/0.82 246[0:NCh:6.2,6.0,165.4,3.2] stable(u) environment(u) finite_set(v) finite_set(w) finite_set(x) || equal(y,z)* in_environment(u,z)* contracts_from(sk1(sk1(y,x),w),v)+ contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(u,sk1(sk1(sk1(y,x),w),v))*. % 0.57/0.82 297[0:NCh:6.2,6.1,241.4,24.0] stable(u) environment(u) finite_set(v) finite_set(w) || equal(appear(first_movers,sk3),sk2(sk3)) in_environment(u,appear(efficient_producers,sk3)) contracts_from(sk1(appear(efficient_producers,e),w),v) contracts_from(appear(efficient_producers,e),w) -> in_environment(u,sk1(sk1(appear(efficient_producers,e),w),v))*. % 0.57/0.82 290[0:NCh:6.2,6.1,201.4,24.0] finite_set(u) finite_set(v) finite_set(w) || contracts_from(sk1(sk1(x,w),v),u) equal(x,sk2(sk3)) in_environment(sk3,appear(efficient_producers,sk3)) contracts_from(sk1(x,w),v) contracts_from(x,w) -> in_environment(sk3,sk1(sk1(sk1(x,w),v),u))*. % 0.57/0.82 278[0:Res:24.0,201.4] finite_set(u) finite_set(v) finite_set(w) || contracts_from(sk1(sk1(sk2(sk3),w),v),u) in_environment(sk3,appear(efficient_producers,sk3)) contracts_from(sk1(sk2(sk3),w),v) contracts_from(sk2(sk3),w) -> in_environment(sk3,sk1(sk1(sk1(sk2(sk3),w),v),u))*. % 0.57/0.82 295[0:MRR:279.4,23.0] finite_set(u) finite_set(v) finite_set(w) || contracts_from(sk1(sk1(appear(efficient_producers,e),w),v),u) contracts_from(sk1(appear(efficient_producers,e),w),v) contracts_from(appear(efficient_producers,e),w) -> in_environment(sk3,sk1(sk1(sk1(appear(efficient_producers,e),w),v),u))*. % 0.57/0.82 241[0:NCh:6.2,6.0,165.4,19.0] stable(u) environment(u) finite_set(v) finite_set(w) || greater(appear(first_movers,sk3),x)*+ in_environment(u,x)* contracts_from(sk1(appear(efficient_producers,e),w),v) contracts_from(appear(efficient_producers,e),w) -> in_environment(u,sk1(sk1(appear(efficient_producers,e),w),v))*. % 0.57/0.82 201[0:NCh:6.2,6.0,130.3,3.2] finite_set(u) finite_set(v) finite_set(w) || contracts_from(sk1(sk1(x,w),v),u) greater(x,y)*+ in_environment(sk3,y)* contracts_from(sk1(x,w),v) contracts_from(x,w) -> in_environment(sk3,sk1(sk1(sk1(x,w),v),u))*. % 0.57/0.82 272[0:Res:7.2,218.5] stable(e) environment(e) stable(u) environment(u) environment(v) finite_set(w) finite_set(x) || in_environment(u,appear(first_movers,v))* contracts_from(sk1(sk2(e),x),w) contracts_from(sk2(e),x) -> in_environment(u,sk1(sk1(sk2(e),x),w))*. % 0.57/0.82 218[0:NCh:6.2,6.0,143.4,3.2] stable(u) environment(u) environment(v) finite_set(w) finite_set(x) || greater(y,appear(efficient_producers,e))+ in_environment(u,appear(first_movers,v))* contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(u,sk1(sk1(y,x),w))*. % 0.57/0.82 227[0:NCh:6.2,6.1,163.4,7.2] stable(u) environment(u) finite_set(v) environment(w) stable(x) environment(x) || greater(appear(first_movers,w),sk2(x))*+ in_environment(u,appear(efficient_producers,x))* contracts_from(appear(efficient_producers,e),v) -> in_environment(u,sk1(appear(efficient_producers,e),v))*. % 0.57/0.82 244[0:NCh:6.2,6.0,165.4,9.1] stable(u) environment(u) finite_set(v) finite_set(w) environment(x) || equal(appear(first_movers,x),y)* in_environment(u,y)* contracts_from(sk1(appear(efficient_producers,e),w),v)+ contracts_from(appear(efficient_producers,e),w) -> in_environment(u,sk1(sk1(appear(efficient_producers,e),w),v))*. % 0.57/0.82 259[0:NCh:6.2,6.1,176.3,7.2] environment(u) finite_set(v) finite_set(w) stable(e) environment(e) || greater(x,sk2(e)) in_environment(sk3,appear(first_movers,u))* contracts_from(sk1(x,w),v) contracts_from(x,w) -> in_environment(sk3,sk1(sk1(x,w),v))*. % 0.57/0.82 240[0:Res:3.2,165.4] finite_set(u) stable(v) environment(v) finite_set(w) finite_set(x) || contracts_from(y,u) in_environment(v,y) contracts_from(sk1(sk1(y,u),x),w) contracts_from(sk1(y,u),x) -> in_environment(v,sk1(sk1(sk1(y,u),x),w))*. % 0.57/0.82 271[0:Obv:270.1] stable(u) environment(u) stable(e) environment(e) finite_set(v) finite_set(w) || equal(x,sk2(e)) contracts_from(sk1(x,w),v) contracts_from(x,w) -> in_environment(u,sk1(sk1(x,w),v))*. % 0.57/0.82 235[0:NCh:6.2,6.0,154.5,3.2] stable(u) environment(u) stable(v) environment(v) finite_set(w) finite_set(x) || equal(y,sk2(v))* in_environment(u,appear(efficient_producers,v))*+ contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(u,sk1(sk1(y,x),w))*. % 0.57/0.82 214[0:NCh:6.2,6.1,161.3,7.2] stable(u) environment(u) finite_set(v) stable(w) environment(w) || greater(appear(first_movers,sk3),sk2(w))+ in_environment(u,appear(efficient_producers,w))* contracts_from(appear(efficient_producers,e),v) -> in_environment(u,sk1(appear(efficient_producers,e),v))*. % 0.57/0.82 247[0:NCh:6.2,6.1,165.4,24.0] stable(u) environment(u) finite_set(v) finite_set(w) || greater(x,sk2(sk3)) in_environment(u,appear(efficient_producers,sk3)) contracts_from(sk1(x,w),v) contracts_from(x,w) -> in_environment(u,sk1(sk1(x,w),v))*. % 0.57/0.82 186[0:NCh:6.2,6.0,109.3,3.2] stable(u) environment(u) finite_set(v) finite_set(w) || greater(x,sk2(u))*+ in_environment(sk3,appear(efficient_producers,u))* contracts_from(sk1(x,w),v) contracts_from(x,w) -> in_environment(sk3,sk1(sk1(x,w),v))*. % 0.57/0.82 242[0:NCh:6.2,6.0,165.4,19.0] stable(u) environment(u) finite_set(v) finite_set(w) || equal(appear(first_movers,sk3),x)* in_environment(u,x)* contracts_from(sk1(appear(efficient_producers,e),w),v)+ contracts_from(appear(efficient_producers,e),w) -> in_environment(u,sk1(sk1(appear(efficient_producers,e),w),v))*. % 0.57/0.82 202[0:NCh:6.2,6.0,130.3,3.2] finite_set(u) finite_set(v) finite_set(w) || contracts_from(sk1(sk1(x,w),v),u)+ equal(x,y)* in_environment(sk3,y)* contracts_from(sk1(x,w),v) contracts_from(x,w) -> in_environment(sk3,sk1(sk1(sk1(x,w),v),u))*. % 0.57/0.82 229[0:Res:3.2,154.5] finite_set(u) stable(v) environment(v) stable(w) environment(w) finite_set(x) || contracts_from(sk2(w),u) in_environment(v,appear(efficient_producers,w)) contracts_from(sk1(sk2(w),u),x) -> in_environment(v,sk1(sk1(sk2(w),u),x))*. % 0.57/0.82 219[0:NCh:6.2,6.0,143.4,3.2] stable(u) environment(u) environment(v) finite_set(w) finite_set(x) || equal(y,appear(efficient_producers,e))+ in_environment(u,appear(first_movers,v))* contracts_from(sk1(y,x),w) contracts_from(y,x) -> in_environment(u,sk1(sk1(y,x),w))*. % 0.57/0.82 228[0:NCh:6.2,6.1,163.4,7.2] stable(u) environment(u) finite_set(v) environment(w) stable(x) environment(x) || equal(appear(first_movers,w),sk2(x))*+ in_environment(u,appear(efficient_producers,x))* contracts_from(appear(efficient_producers,e),v) -> in_environment(u,sk1(appear(efficient_producers,e),v))*. % 0.57/0.82 255[0:Res:7.2,176.3] stable(e) environment(e) environment(u) finite_set(v) finite_set(w) || in_environment(sk3,appear(first_movers,u))* contracts_from(sk1(sk2(e),w),v) contracts_from(sk2(e),w) -> in_environment(sk3,sk1(sk1(sk2(e),w),v))*. % 0.57/0.82 176[0:NCh:6.2,6.0,100.2,3.2] environment(u) finite_set(v) finite_set(w) || greater(x,appear(efficient_producers,e))+ in_environment(sk3,appear(first_movers,u))* contracts_from(sk1(x,w),v) contracts_from(x,w) -> in_environment(sk3,sk1(sk1(x,w),v))*. % 0.57/0.82 217[0:Res:3.2,143.4] finite_set(u) stable(v) environment(v) environment(w) finite_set(x) || contracts_from(appear(efficient_producers,e),u) in_environment(v,appear(first_movers,w))* contracts_from(sk1(appear(efficient_producers,e),u),x)+ -> in_environment(v,sk1(sk1(appear(efficient_producers,e),u),x))*. % 0.57/0.82 220[0:NCh:6.2,6.1,143.4,7.2] stable(u) environment(u) environment(v) finite_set(w) stable(e) environment(e) || greater(x,sk2(e)) in_environment(u,appear(first_movers,v))* contracts_from(x,w) -> in_environment(u,sk1(x,w))*. % 0.57/0.82 223[0:NCh:6.2,6.1,163.4,24.0] stable(u) environment(u) finite_set(v) environment(w) || greater(appear(first_movers,w),sk2(sk3))*l+ in_environment(u,appear(efficient_producers,sk3)) contracts_from(appear(efficient_producers,e),v) -> in_environment(u,sk1(appear(efficient_producers,e),v))*. % 0.57/0.82 237[0:Res:19.0,165.4] stable(u) environment(u) finite_set(v) finite_set(w) || in_environment(u,appear(first_movers,sk3)) contracts_from(sk1(appear(efficient_producers,e),w),v) contracts_from(appear(efficient_producers,e),w) -> in_environment(u,sk1(sk1(appear(efficient_producers,e),w),v))*. % 0.57/0.82 196[0:Res:3.2,130.3] finite_set(u) finite_set(v) finite_set(w) || contracts_from(x,u) contracts_from(sk1(sk1(x,u),w),v) in_environment(sk3,x) contracts_from(sk1(x,u),w) -> in_environment(sk3,sk1(sk1(sk1(x,u),w),v))*. % 0.57/0.82 215[0:NCh:6.2,6.1,161.3,7.2] stable(u) environment(u) finite_set(v) stable(w) environment(w) || equal(appear(first_movers,sk3),sk2(w))+ in_environment(u,appear(efficient_producers,w))* contracts_from(appear(efficient_producers,e),v) -> in_environment(u,sk1(appear(efficient_producers,e),v))*. % 0.57/0.82 248[0:NCh:6.2,6.1,165.4,24.0] stable(u) environment(u) finite_set(v) finite_set(w) || equal(x,sk2(sk3)) in_environment(u,appear(efficient_producers,sk3)) contracts_from(sk1(x,w),v) contracts_from(x,w) -> in_environment(u,sk1(sk1(x,w),v))*. % 0.57/0.82 253[0:Res:43.0,187.5] stable(e) environment(e) finite_set(u) finite_set(v) || equal(w,sk2(e)) contracts_from(sk1(w,v),u) contracts_from(w,v) -> in_environment(sk3,sk1(sk1(w,v),u))*. % 0.57/0.82 187[0:NCh:6.2,6.0,109.3,3.2] stable(u) environment(u) finite_set(v) finite_set(w) || equal(x,sk2(u))* in_environment(sk3,appear(efficient_producers,u))*+ contracts_from(sk1(x,w),v) contracts_from(x,w) -> in_environment(sk3,sk1(sk1(x,w),v))*. % 0.57/0.82 236[0:Res:24.0,165.4] stable(u) environment(u) finite_set(v) finite_set(w) || in_environment(u,appear(efficient_producers,sk3)) contracts_from(sk1(sk2(sk3),w),v) contracts_from(sk2(sk3),w) -> in_environment(u,sk1(sk1(sk2(sk3),w),v))*. % 0.57/0.82 165[0:NCh:6.2,6.0,63.3,3.2] stable(u) environment(u) finite_set(v) finite_set(w) || greater(x,y)*+ in_environment(u,y)* contracts_from(sk1(x,w),v) contracts_from(x,w) -> in_environment(u,sk1(sk1(x,w),v))*. % 0.57/0.82 154[0:NCh:6.2,6.0,69.4,3.2] stable(u) environment(u) stable(v) environment(v) finite_set(w) || greater(x,sk2(v))*+ in_environment(u,appear(efficient_producers,v))* contracts_from(x,w) -> in_environment(u,sk1(x,w))*. % 0.57/0.82 210[0:NCh:6.2,6.1,161.3,24.0] stable(u) environment(u) finite_set(v) || greater(appear(first_movers,sk3),sk2(sk3)) in_environment(u,appear(efficient_producers,sk3)) contracts_from(appear(efficient_producers,e),v) -> in_environment(u,sk1(appear(efficient_producers,e),v))*. % 0.57/0.82 203[0:NCh:6.2,6.1,130.3,24.0] finite_set(u) finite_set(v) || contracts_from(sk1(w,v),u) greater(w,sk2(sk3)) in_environment(sk3,appear(efficient_producers,sk3)) contracts_from(w,v) -> in_environment(sk3,sk1(sk1(w,v),u))*. % 0.57/0.82 224[0:NCh:6.2,6.1,163.4,24.0] stable(u) environment(u) finite_set(v) environment(w) || equal(appear(first_movers,w),sk2(sk3))**+ in_environment(u,appear(efficient_producers,sk3)) contracts_from(appear(efficient_producers,e),v) -> in_environment(u,sk1(appear(efficient_producers,e),v))*. % 0.57/0.82 163[0:NCh:6.2,6.0,63.3,9.1] stable(u) environment(u) finite_set(v) environment(w) || greater(appear(first_movers,w),x)*+ in_environment(u,x)* contracts_from(appear(efficient_producers,e),v) -> in_environment(u,sk1(appear(efficient_producers,e),v))*. % 0.57/0.82 181[0:Res:3.2,109.3] finite_set(u) stable(v) environment(v) finite_set(w) || contracts_from(sk2(v),u) in_environment(sk3,appear(efficient_producers,v)) contracts_from(sk1(sk2(v),u),w) -> in_environment(sk3,sk1(sk1(sk2(v),u),w))*. % 0.57/0.82 177[0:NCh:6.2,6.0,100.2,3.2] environment(u) finite_set(v) finite_set(w) || equal(x,appear(efficient_producers,e))+ in_environment(sk3,appear(first_movers,u))* contracts_from(sk1(x,w),v) contracts_from(x,w) -> in_environment(sk3,sk1(sk1(x,w),v))*. % 0.57/0.82 216[0:Res:7.2,143.4] stable(e) environment(e) stable(u) environment(u) environment(v) finite_set(w) || in_environment(u,appear(first_movers,v))* contracts_from(sk2(e),w) -> in_environment(u,sk1(sk2(e),w))*. % 0.57/0.82 143[0:NCh:6.2,6.0,67.3,3.2] stable(u) environment(u) environment(v) finite_set(w) || greater(x,appear(efficient_producers,e))+ in_environment(u,appear(first_movers,v))* contracts_from(x,w) -> in_environment(u,sk1(x,w))*. % 0.57/0.82 166[0:NCh:6.2,6.0,63.3,3.2] stable(u) environment(u) finite_set(v) finite_set(w) || equal(x,y)* in_environment(u,y)* contracts_from(sk1(x,w),v)+ contracts_from(x,w) -> in_environment(u,sk1(sk1(x,w),v))*. % 0.57/0.82 178[0:NCh:6.2,6.1,100.2,7.2] environment(u) finite_set(v) stable(e) environment(e) || greater(w,sk2(e)) in_environment(sk3,appear(first_movers,u))* contracts_from(w,v) -> in_environment(sk3,sk1(w,v))*. % 0.57/0.82 211[0:NCh:6.2,6.1,161.3,24.0] stable(u) environment(u) finite_set(v) || equal(appear(first_movers,sk3),sk2(sk3)) in_environment(u,appear(efficient_producers,sk3)) contracts_from(appear(efficient_producers,e),v) -> in_environment(u,sk1(appear(efficient_producers,e),v))*. % 0.57/0.82 204[0:NCh:6.2,6.1,130.3,24.0] finite_set(u) finite_set(v) || contracts_from(sk1(w,v),u) equal(w,sk2(sk3)) in_environment(sk3,appear(efficient_producers,sk3)) contracts_from(w,v) -> in_environment(sk3,sk1(sk1(w,v),u))*. % 0.57/0.82 192[0:Res:24.0,130.3] finite_set(u) finite_set(v) || contracts_from(sk1(sk2(sk3),v),u) in_environment(sk3,appear(efficient_producers,sk3)) contracts_from(sk2(sk3),v) -> in_environment(sk3,sk1(sk1(sk2(sk3),v),u))*. % 0.57/0.82 161[0:NCh:6.2,6.0,63.3,19.0] stable(u) environment(u) finite_set(v) || greater(appear(first_movers,sk3),w)*+ in_environment(u,w)* contracts_from(appear(efficient_producers,e),v) -> in_environment(u,sk1(appear(efficient_producers,e),v))*. % 0.57/0.82 209[0:MRR:193.3,23.0] finite_set(u) finite_set(v) || contracts_from(sk1(appear(efficient_producers,e),v),u) contracts_from(appear(efficient_producers,e),v) -> in_environment(sk3,sk1(sk1(appear(efficient_producers,e),v),u))*. % 0.57/0.82 130[0:NCh:6.2,6.0,51.2,3.2] finite_set(u) finite_set(v) || contracts_from(sk1(w,v),u) greater(w,x)*+ in_environment(sk3,x)* contracts_from(w,v) -> in_environment(sk3,sk1(sk1(w,v),u))*. % 0.57/0.82 191[0:Obv:190.1] stable(u) environment(u) stable(e) environment(e) finite_set(v) || equal(w,sk2(e)) contracts_from(w,v) -> in_environment(u,sk1(w,v))*. % 0.57/0.82 155[0:NCh:6.2,6.0,69.4,3.2] stable(u) environment(u) stable(v) environment(v) finite_set(w) || equal(x,sk2(v))* in_environment(u,appear(efficient_producers,v))*+ contracts_from(x,w) -> in_environment(u,sk1(x,w))*. % 0.57/0.82 164[0:NCh:6.2,6.0,63.3,9.1] stable(u) environment(u) finite_set(v) environment(w) || equal(appear(first_movers,w),x)*+ in_environment(u,x)* contracts_from(appear(efficient_producers,e),v) -> in_environment(u,sk1(appear(efficient_producers,e),v))*. % 0.57/0.82 119[0:NCh:6.2,6.0,65.2,3.2] stable(u) environment(u) finite_set(v) || greater(w,sk2(sk3)) in_environment(u,appear(efficient_producers,sk3)) contracts_from(w,v) -> in_environment(u,sk1(w,v))*. % 0.57/0.82 109[0:NCh:6.2,6.0,48.2,3.2] stable(u) environment(u) finite_set(v) || greater(w,sk2(u))*+ in_environment(sk3,appear(efficient_producers,u))* contracts_from(w,v) -> in_environment(sk3,sk1(w,v))*. % 0.57/0.82 145[0:NCh:6.2,6.1,67.3,7.2] stable(u) environment(u) environment(v) stable(e) environment(e) || greater(w,sk2(e)) in_environment(u,appear(first_movers,v))* -> in_environment(u,w)*. % 0.57/0.82 160[0:Res:3.2,63.3] finite_set(u) stable(v) environment(v) finite_set(w) || contracts_from(x,u) in_environment(v,x) contracts_from(sk1(x,u),w) -> in_environment(v,sk1(sk1(x,u),w))*. % 0.57/0.82 144[0:NCh:6.2,6.0,67.3,3.2] stable(u) environment(u) environment(v) finite_set(w) || equal(x,appear(efficient_producers,e))+ in_environment(u,appear(first_movers,v))* contracts_from(x,w) -> in_environment(u,sk1(x,w))*. % 0.57/0.82 149[0:Res:3.2,69.4] finite_set(u) stable(v) environment(v) stable(w) environment(w) || contracts_from(sk2(w),u) in_environment(v,appear(efficient_producers,w)) -> in_environment(v,sk1(sk2(w),u))*. % 0.57/0.82 174[0:Res:7.2,100.2] stable(e) environment(e) environment(u) finite_set(v) || in_environment(sk3,appear(first_movers,u))* contracts_from(sk2(e),v) -> in_environment(sk3,sk1(sk2(e),v))*. % 0.57/0.82 100[0:NCh:6.2,6.0,41.1,3.2] environment(u) finite_set(v) || greater(w,appear(efficient_producers,e))+ in_environment(sk3,appear(first_movers,u))* contracts_from(w,v) -> in_environment(sk3,sk1(w,v))*. % 0.57/0.82 131[0:NCh:6.2,6.0,51.2,3.2] finite_set(u) finite_set(v) || contracts_from(sk1(w,v),u)+ equal(w,x)* in_environment(sk3,x)* contracts_from(w,v) -> in_environment(sk3,sk1(sk1(w,v),u))*. % 0.57/0.82 162[0:NCh:6.2,6.0,63.3,19.0] stable(u) environment(u) finite_set(v) || equal(appear(first_movers,sk3),w)*+ in_environment(u,w)* contracts_from(appear(efficient_producers,e),v) -> in_environment(u,sk1(appear(efficient_producers,e),v))*. % 0.57/0.82 157[0:Res:19.0,63.3] stable(u) environment(u) finite_set(v) || in_environment(u,appear(first_movers,sk3)) contracts_from(appear(efficient_producers,e),v) -> in_environment(u,sk1(appear(efficient_producers,e),v))*. % 0.57/0.82 63[0:NCh:6.2,6.0,5.2,3.2] stable(u) environment(u) finite_set(v) || greater(w,x)*+ in_environment(u,x)* contracts_from(w,v) -> in_environment(u,sk1(w,v))*. % 0.57/0.82 142[0:Res:3.2,67.3] finite_set(u) stable(v) environment(v) environment(w) || contracts_from(appear(efficient_producers,e),u)+ in_environment(v,appear(first_movers,w))* -> in_environment(v,sk1(appear(efficient_producers,e),u))*. % 0.57/0.82 120[0:NCh:6.2,6.0,65.2,3.2] stable(u) environment(u) finite_set(v) || equal(w,sk2(sk3)) in_environment(u,appear(efficient_producers,sk3)) contracts_from(w,v) -> in_environment(u,sk1(w,v))*. % 0.57/0.82 69[0:NCh:6.2,6.1,5.2,7.2] stable(u) environment(u) stable(v) environment(v) || greater(w,sk2(v))*+ in_environment(u,appear(efficient_producers,v))* -> in_environment(u,w)*. % 0.57/0.82 147[0:Res:43.0,110.4] stable(e) environment(e) finite_set(u) || equal(v,sk2(e)) contracts_from(v,u) -> in_environment(sk3,sk1(v,u))*. % 0.57/0.82 110[0:NCh:6.2,6.0,48.2,3.2] stable(u) environment(u) finite_set(v) || equal(w,sk2(u))* in_environment(sk3,appear(efficient_producers,u))*+ contracts_from(w,v) -> in_environment(sk3,sk1(w,v))*. % 0.57/0.82 78[0:NCh:6.2,6.0,39.0,3.2] finite_set(u) || greater(v,sk2(sk3)) in_environment(sk3,appear(efficient_producers,sk3)) contracts_from(v,u) -> in_environment(sk3,sk1(v,u))*. % 0.57/0.82 102[0:NCh:6.2,6.1,41.1,7.2] environment(u) stable(e) environment(e) || greater(v,sk2(e)) in_environment(sk3,appear(first_movers,u))* -> in_environment(sk3,v)*. % 0.57/0.82 67[0:NCh:6.2,6.1,5.2,9.1] stable(u) environment(u) environment(v) || greater(w,appear(efficient_producers,e))*+ in_environment(u,appear(first_movers,v))* -> in_environment(u,w)*. % 0.57/0.82 125[0:Res:3.2,51.2] finite_set(u) finite_set(v) || contracts_from(w,u) contracts_from(sk1(w,u),v) in_environment(sk3,w) -> in_environment(sk3,sk1(sk1(w,u),v))*. % 0.57/0.82 101[0:NCh:6.2,6.0,41.1,3.2] environment(u) finite_set(v) || equal(w,appear(efficient_producers,e))+ in_environment(sk3,appear(first_movers,u))* contracts_from(w,v) -> in_environment(sk3,sk1(w,v))*. % 0.57/0.82 104[0:Res:3.2,48.2] finite_set(u) stable(v) environment(v) || contracts_from(sk2(v),u) in_environment(sk3,appear(efficient_producers,v)) -> in_environment(sk3,sk1(sk2(v),u))*. % 0.57/0.82 114[0:Res:3.2,65.2] finite_set(u) stable(v) environment(v) || contracts_from(sk2(sk3),u) in_environment(v,appear(efficient_producers,sk3)) -> in_environment(v,sk1(sk2(sk3),u))*. % 0.57/0.82 64[0:NCh:6.2,6.0,5.2,3.2] stable(u) environment(u) finite_set(v) || equal(w,x)*+ in_environment(u,x)* contracts_from(w,v) -> in_environment(u,sk1(w,v))*. % 0.57/0.82 138[0:MRR:122.2,23.0] finite_set(u) || contracts_from(appear(efficient_producers,e),u) -> in_environment(sk3,sk1(appear(efficient_producers,e),u))*. % 0.57/0.82 51[0:NCh:6.2,6.0,3.2,25.0] finite_set(u) || contracts_from(v,u) greater(v,w)*+ in_environment(sk3,w)* -> in_environment(sk3,sk1(v,u))*. % 0.57/0.82 65[0:NCh:6.2,6.1,5.2,24.0] stable(u) environment(u) || greater(v,sk2(sk3))+ in_environment(u,appear(efficient_producers,sk3))* -> in_environment(u,v)*. % 0.57/0.82 113[0:Obv:112.1] stable(u) environment(u) stable(e) environment(e) || equal(v,sk2(e)) -> in_environment(u,v)*. % 0.57/0.82 70[0:NCh:6.2,6.1,5.2,7.2] stable(u) environment(u) stable(v) environment(v) || equal(w,sk2(v))* in_environment(u,appear(efficient_producers,v))*+ -> in_environment(u,w)*. % 0.57/0.82 48[0:NCh:6.2,6.1,7.2,25.0] stable(u) environment(u) || greater(v,sk2(u))*+ in_environment(sk3,appear(efficient_producers,u))* -> in_environment(sk3,v)*. % 0.57/0.82 79[0:NCh:6.2,6.0,39.0,3.2] finite_set(u) || equal(v,sk2(sk3)) in_environment(sk3,appear(efficient_producers,sk3)) contracts_from(v,u) -> in_environment(sk3,sk1(v,u))*. % 0.57/0.82 41[0:NCh:6.2,6.1,25.0,9.1] environment(u) || greater(v,appear(efficient_producers,e))*+ in_environment(sk3,appear(first_movers,u))* -> in_environment(sk3,v)*. % 0.57/0.82 68[0:NCh:6.2,6.1,5.2,9.1] stable(u) environment(u) environment(v) || equal(w,appear(efficient_producers,e))*+ in_environment(u,appear(first_movers,v))* -> in_environment(u,w)*. % 0.57/0.82 58[0:Res:3.2,5.2] finite_set(u) stable(v) environment(v) || contracts_from(w,u) in_environment(v,w) -> in_environment(v,sk1(w,u))*. % 0.57/0.82 96[0:EqR:91.2] stable(u) environment(u) || in_environment(sk3,sk2(u)) -> in_environment(sk3,sk1(sk2(u),first_movers))*. % 0.57/0.82 91[0:SSi:89.2,1.0] stable(u) environment(u) || equal(sk2(u),v)*+ in_environment(sk3,v)* -> in_environment(sk3,sk1(sk2(u),first_movers))*. % 0.57/0.82 95[0:Obv:94.1] stable(e) environment(e) stable(u) environment(u) || -> in_environment(u,sk2(e))*. % 0.57/0.82 57[0:Res:7.2,5.2] stable(u) environment(u) stable(v) environment(v) || in_environment(v,appear(efficient_producers,u))* -> in_environment(v,sk2(u)). % 0.57/0.82 92[0:EqR:90.0] || in_environment(sk3,sk2(sk3)) -> in_environment(sk3,sk1(sk2(sk3),first_movers))*. % 0.57/0.82 90[0:SSi:88.0,1.0] || equal(sk2(sk3),u)+ in_environment(sk3,u)* -> in_environment(sk3,sk1(sk2(sk3),first_movers))*. % 0.57/0.82 52[0:NCh:6.2,6.0,3.2,25.0] finite_set(u) || contracts_from(v,u)+ equal(v,w)* in_environment(sk3,w)* -> in_environment(sk3,sk1(v,u))*. % 0.57/0.82 85[0:Obv:83.2] stable(u) environment(u) || -> in_environment(u,appear(efficient_producers,e))*. % 0.57/0.82 66[0:NCh:6.2,6.1,5.2,24.0] stable(u) environment(u) || equal(v,sk2(sk3)) in_environment(u,appear(efficient_producers,sk3))*+ -> in_environment(u,v)*. % 0.57/0.82 80[0:Res:43.0,49.3] stable(e) environment(e) || equal(u,sk2(e)) -> in_environment(sk3,u)*. % 0.57/0.82 49[0:NCh:6.2,6.1,7.2,25.0] stable(u) environment(u) || equal(v,sk2(u))* in_environment(sk3,appear(efficient_producers,u))*+ -> in_environment(sk3,v)*. % 0.57/0.82 73[0:Res:3.2,39.0] finite_set(u) || contracts_from(sk2(sk3),u) in_environment(sk3,appear(efficient_producers,sk3)) -> in_environment(sk3,sk1(sk2(sk3),u))*. % 0.57/0.82 47[0:OCh:6.1,6.0,7.2,9.1] stable(e) environment(e) environment(u) || -> greater(sk2(e),appear(first_movers,u))*r. % 0.57/0.82 39[0:NCh:6.2,6.1,25.0,24.0] || greater(u,sk2(sk3))+ in_environment(sk3,appear(efficient_producers,sk3))* -> in_environment(sk3,u)*. % 0.57/0.82 42[0:NCh:6.2,6.1,25.0,9.1] environment(u) || equal(v,appear(efficient_producers,e))*+ in_environment(sk3,appear(first_movers,u))* -> in_environment(sk3,v)*. % 0.57/0.82 54[0:Res:24.0,5.2] stable(u) environment(u) || in_environment(u,appear(efficient_producers,sk3))* -> in_environment(u,sk2(sk3)). % 0.57/0.84 5[0:Inp] stable(u) environment(u) || greater(v,w)*+ in_environment(u,w)* -> in_environment(u,v)*. % 0.57/0.84 46[0:OCh:6.1,6.0,7.2,19.0] stable(e) environment(e) || -> greater(sk2(e),appear(first_movers,sk3))*r. % 0.57/0.84 50[0:Res:3.2,25.0] finite_set(u) || contracts_from(v,u) in_environment(sk3,v) -> in_environment(sk3,sk1(v,u))*. % 0.57/0.84 53[0:Res:43.0,45.2] stable(e) environment(e) || -> in_environment(sk3,sk2(e))*. % 0.57/0.84 45[0:Res:7.2,25.0] stable(u) environment(u) || in_environment(sk3,appear(efficient_producers,u))* -> in_environment(sk3,sk2(u)). % 0.57/0.84 3[0:Inp] finite_set(u) || contracts_from(v,u) -> greater(sk1(v,u),v)*l. % 0.57/0.84 40[0:NCh:6.2,6.1,25.0,24.0] || equal(u,sk2(sk3)) in_environment(sk3,appear(efficient_producers,sk3))*+ -> in_environment(sk3,u)*. % 0.57/0.84 32[0:Res:24.0,25.0] || in_environment(sk3,appear(efficient_producers,sk3))* -> in_environment(sk3,sk2(sk3)). % 0.57/0.84 44[0:MRR:27.0,43.0] || equal(cardinality_at_time(first_movers,to),zero)** -> . % 0.57/0.84 43[0:MRR:33.0,23.0] || -> in_environment(sk3,appear(efficient_producers,e))*. % 0.57/0.84 7[0:Inp] stable(u) environment(u) || -> greater(sk2(u),appear(efficient_producers,u))*r. % 0.57/0.84 25[0:MRR:13.0,10.0] || greater(u,v)*+ in_environment(sk3,v)* -> in_environment(sk3,u)*. % 0.57/0.84 9[0:Inp] environment(u) || -> greater(appear(efficient_producers,e),appear(first_movers,u))*. % 0.57/0.84 30[0:SSi:28.0,1.0] || -> equal(cardinality_at_time(s,t2),zero)**. % 0.57/0.84 19[0:Res:10.0,9.0] || -> greater(appear(efficient_producers,e),appear(first_movers,sk3))*l. % 0.57/0.84 2[0:Inp] stable(u) environment(u) || -> in_environment(u,appear(first_movers,u))*. % 0.57/0.84 24[0:MRR:14.0,10.0] || -> greater(sk2(sk3),appear(efficient_producers,sk3))*r. % 0.57/0.84 23[0:MRR:15.0,10.0] || -> in_environment(sk3,appear(first_movers,sk3))*. % 0.57/0.84 8[0:Inp] stable(u) environment(u) || -> contracts_from(sk2(u),first_movers)*. % 0.57/0.84 22[0:MRR:16.0,10.0] || -> contracts_from(sk2(sk3),first_movers)*. % 0.57/0.84 10[0:Inp] || -> environment(sk3)*. % 0.57/0.84 11[0:Inp] || -> stable(sk3)*. % 0.57/0.84 1[0:Inp] || -> finite_set(first_movers)*. % 0.57/0.84 % SZS output end Saturation %------------------------------------------------------------------------------