%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT038+1 : TPTP v9.3.0. Bugfixed v9.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n020.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 : CounterSatisfiable 0.31s 0.57s % Output : Saturation 0.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT038+1 : TPTP v9.3.0. Bugfixed v9.3.0. % 0.00/0.03 % Command : run_spass %d %s % 0.11/0.36 % Computer : n020.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Mon Sep 7 12:49:13 UTC 2026 % 0.11/0.36 % CPUTime : % 0.31/0.57 % 0.31/0.57 SPASS V 3.9 % 0.31/0.57 SPASS beiseite: Completion found. % 0.31/0.57 % SZS status CounterSatisfiable % 0.31/0.57 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.31/0.57 SPASS derived 304 clauses, backtracked 0 clauses, performed 0 splits and kept 128 clauses. % 0.31/0.57 SPASS allocated 97961 KBytes. % 0.31/0.57 SPASS spent 0:00:00.21 on the problem. % 0.31/0.57 0:00:00.06 for the input. % 0.31/0.57 0:00:00.05 for the FLOTTER CNF translation. % 0.31/0.57 0:00:00.01 for inferences. % 0.31/0.57 0:00:00.00 for the backtracking. % 0.31/0.57 0:00:00.04 for the reduction. % 0.31/0.57 % 0.31/0.57 % 0.31/0.57 The saturated set of worked-off clauses is : % 0.31/0.57 % SZS output start Saturation % 0.31/0.57 9[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.31/0.57 193[0:NCh:9.2,9.1,79.3,10.2] stable(u) environment(u) environment(v) stable(w) environment(w) || greater(appear(first_movers,v),skf3(w))*+ in_environment(u,appear(efficient_producers,w))* -> in_environment(u,appear(efficient_producers,v))*. % 0.31/0.57 425[0:Obv:416.2] stable(u) environment(u) stable(v) environment(v) || greater(appear(first_movers,v),skf3(skc1))*l+ in_environment(u,appear(first_movers,skc1))* equal(w,skf3(v))* -> in_environment(u,w)*. % 0.31/0.57 195[0:NCh:9.2,9.1,79.3,54.2] stable(u) environment(u) environment(v) stable(w) environment(w) || greater(appear(first_movers,v),skf3(w))*+ in_environment(u,appear(first_movers,w))* -> in_environment(u,appear(efficient_producers,v))*. % 0.31/0.57 424[0:Obv:415.2] stable(u) environment(u) stable(v) environment(v) || greater(appear(first_movers,v),skf3(skc1))+ in_environment(u,appear(first_movers,skc1))* -> in_environment(u,skf2(skf3(v)))*. % 0.31/0.57 337[0:NCh:9.2,9.1,77.2,54.2] stable(u) environment(u) stable(v) environment(v) || greater(appear(first_movers,skc1),skf3(v))+ in_environment(u,appear(first_movers,v))* -> in_environment(u,appear(efficient_producers,skc1))*. % 0.31/0.57 204[0:NCh:9.2,9.0,87.4,18.0] stable(u) environment(u) stable(v) environment(v) || greater(appear(first_movers,skc1),skf3(v))+ in_environment(u,appear(efficient_producers,v))* -> in_environment(u,appear(efficient_producers,skc1))*. % 0.31/0.57 329[0:NCh:9.2,9.1,81.2,54.2] stable(u) environment(u) stable(v) environment(v) || greater(skf3(w),skf3(v))*+ in_environment(u,appear(first_movers,v))* -> in_environment(u,skf2(skf3(w)))*. % 0.31/0.57 208[0:NCh:9.2,9.0,87.4,45.0] stable(u) environment(u) stable(v) environment(v) || greater(skf3(w),skf3(v))*+ in_environment(u,appear(efficient_producers,v))* -> in_environment(u,skf2(skf3(w)))*. % 0.31/0.57 423[0:Obv:408.2] stable(u) environment(u) stable(v) environment(v) || greater(appear(first_movers,u),skf3(skc1))+ in_environment(v,appear(first_movers,skc1))* -> in_environment(v,skf3(u))*. % 0.31/0.57 399[0:Obv:390.2] stable(u) environment(u) stable(v) environment(v) || equal(appear(first_movers,v),skf3(skc1))**+ in_environment(u,appear(first_movers,skc1))* equal(w,skf3(v))* -> in_environment(u,w)*. % 0.31/0.57 214[0:NCh:9.2,9.1,34.1,10.2] environment(u) stable(v) environment(v) || greater(appear(first_movers,u),skf3(v))*+ in_environment(skc1,appear(efficient_producers,v))* -> in_environment(skc1,appear(efficient_producers,u))*. % 0.31/0.57 216[0:NCh:9.2,9.1,34.1,54.2] environment(u) stable(v) environment(v) || greater(appear(first_movers,u),skf3(v))*+ in_environment(skc1,appear(first_movers,v))* -> in_environment(skc1,appear(efficient_producers,u))*. % 0.31/0.57 194[0:NCh:9.2,9.1,79.3,10.2] stable(u) environment(u) environment(v) stable(w) environment(w) || equal(appear(first_movers,v),skf3(w))*+ in_environment(u,appear(efficient_producers,w))* -> in_environment(u,appear(efficient_producers,v))*. % 0.31/0.57 191[0:NCh:9.2,9.1,79.3,26.0] stable(u) environment(u) environment(v) || greater(appear(first_movers,v),skf3(skc1)) in_environment(u,appear(first_movers,skc1)) -> in_environment(u,appear(efficient_producers,v))*. % 0.31/0.57 398[0:Obv:389.2] stable(u) environment(u) stable(v) environment(v) || equal(appear(first_movers,v),skf3(skc1))+ in_environment(u,appear(first_movers,skc1))* -> in_environment(u,skf2(skf3(v)))*. % 0.31/0.57 338[0:NCh:9.2,9.1,77.2,54.2] stable(u) environment(u) stable(v) environment(v) || equal(appear(first_movers,skc1),skf3(v))+ in_environment(u,appear(first_movers,v))* -> in_environment(u,appear(efficient_producers,skc1))*. % 0.31/0.57 330[0:NCh:9.2,9.1,81.2,54.2] stable(u) environment(u) stable(v) environment(v) || equal(skf3(w),skf3(v))*+ in_environment(u,appear(first_movers,v))* -> in_environment(u,skf2(skf3(w)))*. % 0.31/0.57 196[0:NCh:9.2,9.1,79.3,54.2] stable(u) environment(u) environment(v) stable(w) environment(w) || equal(appear(first_movers,v),skf3(w))*+ in_environment(u,appear(first_movers,w))* -> in_environment(u,appear(efficient_producers,v))*. % 0.31/0.57 397[0:Obv:382.2] stable(u) environment(u) stable(v) environment(v) || equal(appear(first_movers,u),skf3(skc1))+ in_environment(v,appear(first_movers,skc1))* -> in_environment(v,skf3(u))*. % 0.31/0.57 302[0:NCh:9.2,9.0,83.2,45.0] stable(u) environment(u) || greater(skf3(v),skf3(skc1))+ in_environment(u,appear(efficient_producers,skc1))* -> in_environment(u,skf2(skf3(v)))*. % 0.31/0.57 295[0:NCh:9.2,9.0,85.2,45.0] stable(u) environment(u) || greater(skf3(v),skf3(skc1))+ in_environment(u,appear(first_movers,skc1))* -> in_environment(u,skf2(skf3(v)))*. % 0.31/0.57 117[0:NCh:9.2,9.1,47.0,10.2] stable(u) environment(u) || greater(skf3(v),skf3(u))*+ in_environment(skc1,appear(efficient_producers,u))* -> in_environment(skc1,skf2(skf3(v)))*. % 0.31/0.57 189[0:NCh:9.2,9.1,79.3,21.0] stable(u) environment(u) environment(v) || greater(appear(first_movers,v),skf3(skc1))+ in_environment(u,appear(efficient_producers,skc1))* -> in_environment(u,appear(efficient_producers,v))*. % 0.31/0.57 119[0:NCh:9.2,9.1,47.0,54.2] stable(u) environment(u) || greater(skf3(v),skf3(u))*+ in_environment(skc1,appear(first_movers,u))* -> in_environment(skc1,skf2(skf3(v)))*. % 0.31/0.57 380[0:Obv:366.1] stable(u) environment(u) stable(v) environment(v) || equal(appear(efficient_producers,v),skf3(u))*+ equal(w,skf3(v))* -> in_environment(u,w)*. % 0.31/0.57 379[0:Obv:367.1] stable(u) environment(u) stable(v) environment(v) || equal(appear(first_movers,v),skf3(u))*+ equal(w,skf3(v))* -> in_environment(u,w)*. % 0.31/0.57 215[0:NCh:9.2,9.1,34.1,10.2] environment(u) stable(v) environment(v) || equal(appear(first_movers,u),skf3(v))*+ in_environment(skc1,appear(efficient_producers,v))* -> in_environment(skc1,appear(efficient_producers,u))*. % 0.31/0.57 89[0:NCh:9.2,9.1,12.2,54.2] stable(u) environment(u) stable(v) environment(v) || greater(w,skf3(v))*+ in_environment(u,appear(first_movers,v))* -> in_environment(u,w)*. % 0.31/0.57 217[0:NCh:9.2,9.1,34.1,54.2] environment(u) stable(v) environment(v) || equal(appear(first_movers,u),skf3(v))*+ in_environment(skc1,appear(first_movers,v))* -> in_environment(skc1,appear(efficient_producers,u))*. % 0.31/0.57 192[0:NCh:9.2,9.1,79.3,26.0] stable(u) environment(u) environment(v) || equal(appear(first_movers,v),skf3(skc1)) in_environment(u,appear(first_movers,skc1)) -> in_environment(u,appear(efficient_producers,v))*. % 0.31/0.57 378[0:Obv:365.1] stable(u) environment(u) stable(v) environment(v) || equal(appear(efficient_producers,v),skf3(u)) -> in_environment(u,skf2(skf3(v)))*. % 0.31/0.57 377[0:Obv:368.1] stable(u) environment(u) stable(v) environment(v) || equal(appear(first_movers,v),skf3(u)) -> in_environment(u,skf2(skf3(v)))*. % 0.31/0.57 205[0:NCh:9.2,9.0,87.4,18.0] stable(u) environment(u) stable(v) environment(v) || equal(appear(first_movers,skc1),skf3(v))+ in_environment(u,appear(efficient_producers,v))* -> in_environment(u,appear(efficient_producers,skc1))*. % 0.31/0.57 376[0:Obv:351.1] stable(u) environment(u) stable(v) environment(v) || equal(appear(first_movers,u),skf3(v)) -> in_environment(v,skf3(u))*. % 0.31/0.57 375[0:Obv:352.1] stable(u) environment(u) stable(v) environment(v) || equal(appear(efficient_producers,u),skf3(v)) -> in_environment(v,skf3(u))*. % 0.31/0.57 374[0:Obv:360.1] stable(u) environment(u) || equal(appear(efficient_producers,skc1),skf3(u))*+ equal(v,skf3(skc1)) -> in_environment(u,v)*. % 0.31/0.57 373[0:Obv:363.1] stable(u) environment(u) || equal(appear(first_movers,skc1),skf3(u))*+ equal(v,skf3(skc1)) -> in_environment(u,v)*. % 0.31/0.57 209[0:NCh:9.2,9.0,87.4,45.0] stable(u) environment(u) stable(v) environment(v) || equal(skf3(w),skf3(v))*+ in_environment(u,appear(efficient_producers,v))* -> in_environment(u,skf2(skf3(w)))*. % 0.31/0.57 372[0:Obv:359.1] stable(u) environment(u) || equal(appear(efficient_producers,skc1),skf3(u)) -> in_environment(u,skf2(skf3(skc1)))*. % 0.31/0.57 371[0:Obv:362.1] stable(u) environment(u) || equal(appear(first_movers,skc1),skf3(u)) -> in_environment(u,skf2(skf3(skc1)))*. % 0.31/0.57 370[0:Obv:361.1] stable(u) environment(u) || equal(appear(efficient_producers,skc1),skf3(u)) -> in_environment(u,skf3(skc1))*. % 0.31/0.57 369[0:Obv:364.1] stable(u) environment(u) || equal(appear(first_movers,skc1),skf3(u)) -> in_environment(u,skf3(skc1))*. % 0.31/0.57 190[0:NCh:9.2,9.1,79.3,21.0] stable(u) environment(u) environment(v) || equal(appear(first_movers,v),skf3(skc1))+ in_environment(u,appear(efficient_producers,skc1))* -> in_environment(u,appear(efficient_producers,v))*. % 0.31/0.57 350[0:Obv:346.3] stable(u) environment(u) || equal(v,skf3(u)) -> in_environment(u,v)*. % 0.31/0.57 90[0:NCh:9.2,9.1,12.2,54.2] stable(u) environment(u) stable(v) environment(v) || equal(w,skf3(v))* in_environment(u,appear(first_movers,v))*+ -> in_environment(u,w)*. % 0.31/0.57 160[0:Res:43.1,68.3] stable(u) environment(u) || greater(appear(first_movers,u),skf3(skc1))*l+ equal(v,skf3(u))* -> in_environment(skc1,v)*. % 0.31/0.57 150[0:Res:43.1,53.3] stable(u) environment(u) || greater(appear(efficient_producers,u),skf3(skc1))*l+ equal(v,skf3(u))* -> in_environment(skc1,v)*. % 0.31/0.57 77[0:NCh:9.2,9.0,12.2,18.0] stable(u) environment(u) || greater(appear(first_movers,skc1),v)*+ in_environment(u,v)* -> in_environment(u,appear(efficient_producers,skc1))*. % 0.31/0.57 81[0:NCh:9.2,9.0,12.2,45.0] stable(u) environment(u) || greater(skf3(v),w)*+ in_environment(u,w)* -> in_environment(u,skf2(skf3(v)))*. % 0.31/0.57 303[0:NCh:9.2,9.0,83.2,45.0] stable(u) environment(u) || equal(skf3(v),skf3(skc1))+ in_environment(u,appear(efficient_producers,skc1))* -> in_environment(u,skf2(skf3(v)))*. % 0.31/0.57 296[0:NCh:9.2,9.0,85.2,45.0] stable(u) environment(u) || equal(skf3(v),skf3(skc1))+ in_environment(u,appear(first_movers,skc1))* -> in_environment(u,skf2(skf3(v)))*. % 0.31/0.57 297[0:Res:45.0,83.2] stable(u) environment(u) || in_environment(u,appear(efficient_producers,skc1))* -> in_environment(u,skf2(skf3(skc1))). % 0.31/0.57 83[0:NCh:9.2,9.1,12.2,21.0] stable(u) environment(u) || greater(v,skf3(skc1))+ in_environment(u,appear(efficient_producers,skc1))* -> in_environment(u,v)*. % 0.31/0.57 85[0:NCh:9.2,9.1,12.2,26.0] stable(u) environment(u) || greater(v,skf3(skc1))+ in_environment(u,appear(first_movers,skc1))* -> in_environment(u,v)*. % 0.31/0.57 67[0:NCh:9.2,9.1,54.2,22.0] stable(u) environment(u) || greater(v,skf3(u))*+ in_environment(skc1,appear(first_movers,u))* -> in_environment(skc1,v)*. % 0.31/0.57 282[0:Obv:278.3] stable(u) environment(u) || -> in_environment(u,skf2(skf3(u)))*. % 0.31/0.57 246[0:Obv:234.2] stable(u) environment(u) stable(v) environment(v) || in_environment(u,appear(first_movers,v))* -> in_environment(u,skf2(skf3(v))). % 0.31/0.57 52[0:NCh:9.2,9.1,10.2,22.0] stable(u) environment(u) || greater(v,skf3(u))*+ in_environment(skc1,appear(efficient_producers,u))* -> in_environment(skc1,v)*. % 0.31/0.57 118[0:NCh:9.2,9.1,47.0,10.2] stable(u) environment(u) || equal(skf3(v),skf3(u))*+ in_environment(skc1,appear(efficient_producers,u))* -> in_environment(skc1,skf2(skf3(v)))*. % 0.31/0.57 120[0:NCh:9.2,9.1,47.0,54.2] stable(u) environment(u) || equal(skf3(v),skf3(u))*+ in_environment(skc1,appear(first_movers,u))* -> in_environment(skc1,skf2(skf3(v)))*. % 0.31/0.57 219[0:MRR:212.2,20.0] environment(u) || greater(appear(first_movers,u),skf3(skc1)) -> in_environment(skc1,appear(efficient_producers,u))*. % 0.31/0.57 245[0:SSi:244.3,244.2,2.0,1.0,2.0,1.0] stable(u) environment(u) || in_environment(u,appear(first_movers,skc1))* -> in_environment(u,skf2(skf3(skc1))). % 0.31/0.57 203[0:Res:45.0,87.4] stable(u) environment(u) stable(v) environment(v) || in_environment(u,appear(efficient_producers,v))* -> in_environment(u,skf2(skf3(v))). % 0.31/0.57 218[0:MRR:213.2,20.0] environment(u) || equal(appear(first_movers,u),skf3(skc1)) -> in_environment(skc1,appear(efficient_producers,u))*. % 0.31/0.57 34[0:NCh:9.2,9.0,22.0,6.1] environment(u) || greater(appear(first_movers,u),v)*+ in_environment(skc1,v)* -> in_environment(skc1,appear(efficient_producers,u))*. % 0.31/0.57 145[0:Res:43.1,112.2] stable(u) environment(u) || greater(appear(first_movers,u),skf3(skc1)) -> in_environment(skc1,skf2(skf3(u)))*. % 0.31/0.57 135[0:Res:43.1,111.2] stable(u) environment(u) || greater(appear(efficient_producers,u),skf3(skc1)) -> in_environment(skc1,skf2(skf3(u)))*. % 0.31/0.57 87[0:NCh:9.2,9.1,12.2,10.2] stable(u) environment(u) stable(v) environment(v) || greater(w,skf3(v))*+ in_environment(u,appear(efficient_producers,v))* -> in_environment(u,w)*. % 0.31/0.57 202[0:Obv:198.3] stable(u) environment(u) || -> in_environment(u,skf3(u))*. % 0.31/0.57 75[0:Res:54.2,12.2] stable(u) environment(u) stable(v) environment(v) || in_environment(v,appear(first_movers,u))* -> in_environment(v,skf3(u)). % 0.31/0.57 63[0:Res:43.1,60.2] stable(u) environment(u) || greater(appear(first_movers,u),skf3(skc1)) -> in_environment(skc1,skf3(u))*. % 0.31/0.57 56[0:Res:43.1,49.2] stable(u) environment(u) || greater(appear(efficient_producers,u),skf3(skc1)) -> in_environment(skc1,skf3(u))*. % 0.31/0.57 79[0:NCh:9.2,9.0,12.2,6.1] stable(u) environment(u) environment(v) || greater(appear(first_movers,v),w)*+ in_environment(u,w)* -> in_environment(u,appear(efficient_producers,v))*. % 0.31/0.57 161[0:Res:42.1,68.3] stable(u) environment(u) || equal(appear(first_movers,u),skf3(skc1))**+ equal(v,skf3(u))* -> in_environment(skc1,v)*. % 0.31/0.57 151[0:Res:42.1,53.3] stable(u) environment(u) || equal(appear(efficient_producers,u),skf3(skc1))**+ equal(v,skf3(u))* -> in_environment(skc1,v)*. % 0.31/0.57 78[0:NCh:9.2,9.0,12.2,18.0] stable(u) environment(u) || equal(appear(first_movers,skc1),v)*+ in_environment(u,v)* -> in_environment(u,appear(efficient_producers,skc1))*. % 0.31/0.57 82[0:NCh:9.2,9.0,12.2,45.0] stable(u) environment(u) || equal(skf3(v),w)*+ in_environment(u,w)* -> in_environment(u,skf2(skf3(v)))*. % 0.31/0.57 88[0:NCh:9.2,9.1,12.2,10.2] stable(u) environment(u) stable(v) environment(v) || equal(w,skf3(v))* in_environment(u,appear(efficient_producers,v))*+ -> in_environment(u,w)*. % 0.31/0.57 84[0:NCh:9.2,9.1,12.2,21.0] stable(u) environment(u) || equal(v,skf3(skc1)) in_environment(u,appear(efficient_producers,skc1))*+ -> in_environment(u,v)*. % 0.31/0.57 86[0:NCh:9.2,9.1,12.2,26.0] stable(u) environment(u) || equal(v,skf3(skc1)) in_environment(u,appear(first_movers,skc1))*+ -> in_environment(u,v)*. % 0.31/0.57 68[0:NCh:9.2,9.1,54.2,22.0] stable(u) environment(u) || equal(v,skf3(u))* in_environment(skc1,appear(first_movers,u))*+ -> in_environment(skc1,v)*. % 0.31/0.57 53[0:NCh:9.2,9.1,10.2,22.0] stable(u) environment(u) || equal(v,skf3(u))* in_environment(skc1,appear(efficient_producers,u))*+ -> in_environment(skc1,v)*. % 0.31/0.57 80[0:NCh:9.2,9.0,12.2,6.1] stable(u) environment(u) environment(v) || equal(appear(first_movers,v),w)*+ in_environment(u,w)* -> in_environment(u,appear(efficient_producers,v))*. % 0.31/0.57 146[0:Res:42.1,112.2] stable(u) environment(u) || equal(appear(first_movers,u),skf3(skc1)) -> in_environment(skc1,skf2(skf3(u)))*. % 0.31/0.57 136[0:Res:42.1,111.2] stable(u) environment(u) || equal(appear(efficient_producers,u),skf3(skc1)) -> in_environment(skc1,skf2(skf3(u)))*. % 0.31/0.57 112[0:Res:54.2,47.0] stable(u) environment(u) || in_environment(skc1,appear(first_movers,u))* -> in_environment(skc1,skf2(skf3(u))). % 0.31/0.57 111[0:Res:10.2,47.0] stable(u) environment(u) || in_environment(skc1,appear(efficient_producers,u))* -> in_environment(skc1,skf2(skf3(u))). % 0.31/0.57 74[0:Res:10.2,12.2] stable(u) environment(u) stable(v) environment(v) || in_environment(v,appear(efficient_producers,u))* -> in_environment(v,skf3(u)). % 0.31/0.57 123[0:MRR:115.1,20.0] || greater(skf3(u),skf3(skc1)) -> in_environment(skc1,skf2(skf3(u)))*. % 0.31/0.57 122[0:MRR:114.1,41.0] || equal(skf3(u),skf3(skc1)) -> in_environment(skc1,skf2(skf3(u)))*. % 0.31/0.57 121[0:MRR:109.0,41.0] || -> in_environment(skc1,skf2(skf3(skc1)))*. % 0.31/0.57 47[0:NCh:9.2,9.0,45.0,22.0] || greater(skf3(u),v)*+ in_environment(skc1,v)* -> in_environment(skc1,skf2(skf3(u)))*. % 0.31/0.57 73[0:Res:6.1,12.2] environment(u) stable(v) environment(v) || in_environment(v,appear(first_movers,u)) -> in_environment(v,appear(efficient_producers,u))*. % 0.31/0.57 71[0:Res:18.0,12.2] stable(u) environment(u) || in_environment(u,appear(first_movers,skc1)) -> in_environment(u,appear(efficient_producers,skc1))*. % 0.31/0.57 76[0:Res:45.0,12.2] stable(u) environment(u) || in_environment(u,skf3(v)) -> in_environment(u,skf2(skf3(v)))*. % 0.31/0.57 72[0:Res:26.0,12.2] stable(u) environment(u) || in_environment(u,appear(first_movers,skc1))* -> in_environment(u,skf3(skc1)). % 0.31/0.57 70[0:Res:21.0,12.2] stable(u) environment(u) || in_environment(u,appear(efficient_producers,skc1))* -> in_environment(u,skf3(skc1)). % 0.31/0.57 12[0:Inp] stable(u) environment(u) || greater(v,w)*+ in_environment(u,w)* -> in_environment(u,v)*. % 0.31/0.59 35[0:NCh:9.2,9.0,22.0,6.1] environment(u) || equal(appear(first_movers,u),v)*+ in_environment(skc1,v)* -> in_environment(skc1,appear(efficient_producers,u))*. % 0.31/0.59 64[0:Res:42.1,60.2] stable(u) environment(u) || equal(appear(first_movers,u),skf3(skc1)) -> in_environment(skc1,skf3(u))*. % 0.31/0.59 57[0:Res:42.1,49.2] stable(u) environment(u) || equal(appear(efficient_producers,u),skf3(skc1)) -> in_environment(skc1,skf3(u))*. % 0.31/0.59 54[0:Obv:51.1] stable(u) environment(u) || -> greater(skf3(u),appear(first_movers,u))*r. % 0.31/0.59 11[0:Inp] || greater(u,appear(first_movers,skc1)) in_environment(skc1,u) equal(cardinality_at_time(first_movers,u),zero)** -> . % 0.31/0.59 60[0:Obv:59.0] stable(u) environment(u) || in_environment(skc1,appear(first_movers,u))* -> in_environment(skc1,skf3(u)). % 0.31/0.59 49[0:Res:10.2,22.0] stable(u) environment(u) || in_environment(skc1,appear(efficient_producers,u))* -> in_environment(skc1,skf3(u)). % 0.31/0.59 48[0:NCh:9.2,9.0,45.0,22.0] || equal(skf3(u),v)*+ in_environment(skc1,v)* -> in_environment(skc1,skf2(skf3(u)))*. % 0.31/0.59 31[0:Res:6.1,22.0] environment(u) || in_environment(skc1,appear(first_movers,u)) -> in_environment(skc1,appear(efficient_producers,u))*. % 0.31/0.59 10[0:Inp] stable(u) environment(u) || -> greater(skf3(u),appear(efficient_producers,u))*r. % 0.31/0.59 43[0:MRR:36.1,41.0] || greater(u,skf3(skc1)) -> in_environment(skc1,u)*. % 0.31/0.59 46[0:Res:45.0,22.0] || in_environment(skc1,skf3(u)) -> in_environment(skc1,skf2(skf3(u)))*. % 0.31/0.59 45[0:SSi:44.0,3.0] || -> greater(skf2(skf3(u)),skf3(u))*l. % 0.31/0.59 42[0:MRR:37.1,41.0] || equal(u,skf3(skc1)) -> in_environment(skc1,u)*. % 0.31/0.59 8[0:Inp] finite_set(u) || contracts_from(v,u)* -> greater(skf2(v),v). % 0.31/0.59 41[0:MRR:29.0,20.0] || -> in_environment(skc1,appear(efficient_producers,skc1))*. % 0.31/0.59 40[0:MRR:30.0,20.0] || -> in_environment(skc1,skf3(skc1))*. % 0.31/0.59 22[0:MRR:13.0,1.0] || greater(u,v)*+ in_environment(skc1,v)* -> in_environment(skc1,u)*. % 0.31/0.59 26[0:OCh:9.1,9.0,18.0,21.0] || -> greater(skf3(skc1),appear(first_movers,skc1))*r. % 0.31/0.59 6[0:Inp] environment(u) || -> greater(appear(efficient_producers,u),appear(first_movers,u))*l. % 0.31/0.59 18[0:Res:1.0,6.0] || -> greater(appear(efficient_producers,skc1),appear(first_movers,skc1))*l. % 0.31/0.59 7[0:Inp] stable(u) environment(u) || -> in_environment(u,appear(first_movers,u))*. % 0.31/0.59 21[0:MRR:14.0,1.0] || -> greater(skf3(skc1),appear(efficient_producers,skc1))*r. % 0.31/0.59 20[0:MRR:15.0,1.0] || -> in_environment(skc1,appear(first_movers,skc1))*. % 0.31/0.59 5[0:Inp] || -> equal(cardinality_at_time(s,skf2(u)),zero)**. % 0.31/0.59 4[0:Inp] || -> contracts_from(skf3(u),first_movers)*. % 0.31/0.59 1[0:Inp] || -> environment(skc1)*. % 0.31/0.59 2[0:Inp] || -> stable(skc1)*. % 0.31/0.59 3[0:Inp] || -> finite_set(first_movers)*. % 0.31/0.59 % SZS output end Saturation %------------------------------------------------------------------------------