%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT020-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n010.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:48 AM UTC 2026 % Result : Unsatisfiable 0.12s 0.43s % Output : Refutation 0.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT020-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.07/0.35 % Computer : n010.cluster.edu % 0.07/0.35 % Model : x86_64 x86_64 % 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.35 % Memory : 8046.5625MB % 0.07/0.35 % OS : Linux 6.8.0-71-generic % 0.07/0.35 % CPULimit : 300 % 0.07/0.35 % WCLimit : 300 % 0.07/0.35 % DateTime : Mon Sep 7 12:01:26 UTC 2026 % 0.07/0.35 % CPUTime : % 0.12/0.43 % 0.12/0.43 SPASS V 3.9 % 0.12/0.43 SPASS beiseite: Proof found. % 0.12/0.43 % SZS status Theorem % 0.12/0.43 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.12/0.43 SPASS derived 225 clauses, backtracked 9 clauses, performed 2 splits and kept 117 clauses. % 0.12/0.43 SPASS allocated 75864 KBytes. % 0.12/0.43 SPASS spent 0:00:00.07 on the problem. % 0.12/0.43 0:00:00.03 for the input. % 0.12/0.43 0:00:00.00 for the FLOTTER CNF translation. % 0.12/0.43 0:00:00.00 for inferences. % 0.12/0.43 0:00:00.00 for the backtracking. % 0.12/0.43 0:00:00.01 for the reduction. % 0.12/0.43 % 0.12/0.43 % 0.12/0.43 Here is a proof with depth 5, length 47 : % 0.12/0.43 % SZS output start Refutation % 0.12/0.43 1[0:Inp] environment(u) || decreases(difference(disbanding_rate(first_movers,v),disbanding_rate(efficient_producers,v)))*+ subpopulations(first_movers,efficient_producers,u,v)* -> . % 0.12/0.43 2[0:Inp] environment(u) || in_environment(u,initial_FM_EP(u)) -> subpopulations(first_movers,efficient_producers,u,initial_FM_EP(u))*. % 0.12/0.43 3[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v)* -> greater_or_equal(v,initial_FM_EP(u)). % 0.12/0.43 4[0:Inp] environment(u) || greater_or_equal(v,w)* greater_or_equal(w,x)* greater(disbanding_rate(first_movers,x),disbanding_rate(efficient_producers,x))*r+ subpopulations(first_movers,efficient_producers,u,v)* -> decreases(difference(disbanding_rate(first_movers,w),disbanding_rate(efficient_producers,w)))* greater(disbanding_rate(first_movers,v),disbanding_rate(efficient_producers,v)). % 0.12/0.43 5[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v)* -> in_environment(u,v). % 0.12/0.43 6[0:Inp] environment(u) || -> greater_or_equal(initial_FM_EP(u),start_time(u))*. % 0.12/0.43 7[0:Inp] environment(u) || in_environment(u,v)* greater(v,w)*+ greater_or_equal(w,start_time(u))* -> in_environment(u,w). % 0.12/0.43 9[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 0.12/0.43 10[0:Inp] environment(u) || -> greater(disbanding_rate(first_movers,initial_FM_EP(u)),disbanding_rate(efficient_producers,initial_FM_EP(u)))*r. % 0.12/0.43 11[0:Inp] environment(u) || greater_or_equal(v,w)* greater_or_equal(w,x)* subpopulations(first_movers,efficient_producers,u,v)*+ subpopulations(first_movers,efficient_producers,u,x)* -> subpopulations(first_movers,efficient_producers,u,w)*. % 0.12/0.43 12[0:Inp] || -> environment(sk1)*. % 0.12/0.43 13[0:Inp] || -> subpopulations(first_movers,efficient_producers,sk1,sk2)*. % 0.12/0.43 14[0:Inp] || greater(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2))*r -> . % 0.12/0.43 18[0:Res:12.0,1.0] || decreases(difference(disbanding_rate(first_movers,u),disbanding_rate(efficient_producers,u)))* subpopulations(first_movers,efficient_producers,sk1,u) -> . % 0.12/0.43 19[0:Res:12.0,10.0] || -> greater(disbanding_rate(first_movers,initial_FM_EP(sk1)),disbanding_rate(efficient_producers,initial_FM_EP(sk1)))*r. % 0.12/0.43 20[0:Res:12.0,2.0] || in_environment(sk1,initial_FM_EP(sk1)) -> subpopulations(first_movers,efficient_producers,sk1,initial_FM_EP(sk1))*. % 0.12/0.43 21[0:Res:12.0,3.0] || subpopulations(first_movers,efficient_producers,sk1,u)* -> greater_or_equal(u,initial_FM_EP(sk1)). % 0.12/0.43 26[0:Res:13.0,3.1] environment(sk1) || -> greater_or_equal(sk2,initial_FM_EP(sk1))*. % 0.12/0.43 27[0:Res:13.0,5.1] environment(sk1) || -> in_environment(sk1,sk2)*. % 0.12/0.43 28[0:Res:13.0,11.2] environment(sk1) || subpopulations(first_movers,efficient_producers,sk1,u)* greater_or_equal(v,u)* greater_or_equal(sk2,v) -> subpopulations(first_movers,efficient_producers,sk1,v)*. % 0.12/0.43 29[0:Res:13.0,4.3] environment(sk1) || greater_or_equal(u,v)* greater_or_equal(sk2,u) greater(disbanding_rate(first_movers,v),disbanding_rate(efficient_producers,v))*r -> decreases(difference(disbanding_rate(first_movers,u),disbanding_rate(efficient_producers,u)))* greater(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2)). % 0.12/0.43 30[0:MRR:27.0,12.0] || -> in_environment(sk1,sk2)*. % 0.12/0.43 31[0:MRR:26.0,12.0] || -> greater_or_equal(sk2,initial_FM_EP(sk1))*. % 0.12/0.43 33[0:MRR:28.0,12.0] || greater_or_equal(u,v)* greater_or_equal(sk2,u) subpopulations(first_movers,efficient_producers,sk1,v)*+ -> subpopulations(first_movers,efficient_producers,sk1,u)*. % 0.12/0.43 35[0:MRR:29.0,29.5,12.0,14.0] || greater_or_equal(u,v)* greater_or_equal(sk2,u) greater(disbanding_rate(first_movers,v),disbanding_rate(efficient_producers,v))*r+ -> decreases(difference(disbanding_rate(first_movers,u),disbanding_rate(efficient_producers,u)))*. % 0.12/0.43 46[0:Res:2.2,3.1] environment(u) environment(u) || in_environment(u,initial_FM_EP(u)) -> greater_or_equal(initial_FM_EP(u),initial_FM_EP(u))*. % 0.12/0.43 48[0:Obv:46.0] environment(u) || in_environment(u,initial_FM_EP(u)) -> greater_or_equal(initial_FM_EP(u),initial_FM_EP(u))*. % 0.12/0.43 49[0:Res:31.0,9.0] || -> equal(initial_FM_EP(sk1),sk2) greater(sk2,initial_FM_EP(sk1))*r. % 0.12/0.43 54[1:Spt:49.0] || -> equal(initial_FM_EP(sk1),sk2)**. % 0.12/0.43 60[1:Rew:54.0,19.0] || -> greater(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2))*r. % 0.12/0.43 64[1:MRR:60.0,14.0] || -> . % 0.12/0.43 66[1:Spt:64.0,49.0,54.0] || equal(initial_FM_EP(sk1),sk2)** -> . % 0.12/0.43 67[1:Spt:64.0,49.1] || -> greater(sk2,initial_FM_EP(sk1))*r. % 0.12/0.43 79[1:Res:67.0,7.2] environment(u) || in_environment(u,sk2) greater_or_equal(initial_FM_EP(sk1),start_time(u))* -> in_environment(u,initial_FM_EP(sk1)). % 0.12/0.43 93[1:Res:6.1,79.2] environment(sk1) environment(sk1) || in_environment(sk1,sk2) -> in_environment(sk1,initial_FM_EP(sk1))*. % 0.12/0.43 94[1:Obv:93.0] environment(sk1) || in_environment(sk1,sk2) -> in_environment(sk1,initial_FM_EP(sk1))*. % 0.12/0.43 95[1:SSi:94.0,12.0] || in_environment(sk1,sk2) -> in_environment(sk1,initial_FM_EP(sk1))*. % 0.12/0.43 96[1:MRR:95.0,30.0] || -> in_environment(sk1,initial_FM_EP(sk1))*. % 0.12/0.43 97[1:MRR:20.0,96.0] || -> subpopulations(first_movers,efficient_producers,sk1,initial_FM_EP(sk1))*. % 0.12/0.43 112[1:Res:97.0,33.2] || greater_or_equal(u,initial_FM_EP(sk1)) greater_or_equal(sk2,u) -> subpopulations(first_movers,efficient_producers,sk1,u)*. % 0.12/0.43 265[0:Res:19.0,35.2] || greater_or_equal(u,initial_FM_EP(sk1)) greater_or_equal(sk2,u) -> decreases(difference(disbanding_rate(first_movers,u),disbanding_rate(efficient_producers,u)))*. % 0.12/0.43 273[0:Res:265.2,18.0] || greater_or_equal(u,initial_FM_EP(sk1)) greater_or_equal(sk2,u) subpopulations(first_movers,efficient_producers,sk1,u)* -> . % 0.12/0.43 276[0:MRR:273.0,21.1] || greater_or_equal(sk2,u) subpopulations(first_movers,efficient_producers,sk1,u)* -> . % 0.12/0.43 279[1:MRR:112.2,276.1] || greater_or_equal(u,initial_FM_EP(sk1))* greater_or_equal(sk2,u) -> . % 0.12/0.43 284[1:Res:48.2,279.0] environment(sk1) || in_environment(sk1,initial_FM_EP(sk1)) greater_or_equal(sk2,initial_FM_EP(sk1))* -> . % 0.12/0.43 288[1:SSi:284.0,12.0] || in_environment(sk1,initial_FM_EP(sk1)) greater_or_equal(sk2,initial_FM_EP(sk1))* -> . % 0.12/0.43 289[1:MRR:288.0,288.1,96.0,31.0] || -> . % 0.12/0.43 % SZS output end Refutation % 0.12/0.43 Formulae used in the proof : l3_22 mp_earliest_time_point_23 mp_earliest_time_point_24 mp_positive_function_difference_25 mp_time_point_occurs_26 mp_initial_time_27 mp_times_in_order_28 mp_greater_or_equal_30 a8_31 a10_32 prove_l2_33 prove_l2_34 prove_l2_35 % 0.12/0.43 %------------------------------------------------------------------------------