%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT020+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n029.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:47 AM UTC 2026 % Result : Theorem 0.22s 0.55s % Output : Refutation 0.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT020+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.03 % Command : run_spass %d %s % 0.09/0.35 % Computer : n029.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Mon Sep 7 12:02:11 UTC 2026 % 0.09/0.35 % CPUTime : % 0.22/0.55 % 0.22/0.55 SPASS V 3.9 % 0.22/0.55 SPASS beiseite: Proof found. % 0.22/0.55 % SZS status Theorem % 0.22/0.55 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.22/0.55 SPASS derived 225 clauses, backtracked 9 clauses, performed 2 splits and kept 117 clauses. % 0.22/0.55 SPASS allocated 97837 KBytes. % 0.22/0.55 SPASS spent 0:00:00.18 on the problem. % 0.22/0.55 0:00:00.06 for the input. % 0.22/0.55 0:00:00.05 for the FLOTTER CNF translation. % 0.22/0.55 0:00:00.01 for inferences. % 0.22/0.55 0:00:00.00 for the backtracking. % 0.22/0.55 0:00:00.02 for the reduction. % 0.22/0.55 % 0.22/0.55 % 0.22/0.55 Here is a proof with depth 5, length 47 : % 0.22/0.55 % SZS output start Refutation % 0.22/0.55 1[0:Inp] || -> environment(skc3)*. % 0.22/0.55 2[0:Inp] || -> subpopulations(first_movers,efficient_producers,skc3,skc2)*. % 0.22/0.55 3[0:Inp] || greater(disbanding_rate(first_movers,skc2),disbanding_rate(efficient_producers,skc2))*r -> . % 0.22/0.55 4[0:Inp] environment(u) || -> greater_or_equal(initial_FM_EP(u),start_time(u))*. % 0.22/0.55 5[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 0.22/0.55 7[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v)* -> in_environment(u,v). % 0.22/0.55 8[0:Inp] environment(u) || -> greater(disbanding_rate(first_movers,initial_FM_EP(u)),disbanding_rate(efficient_producers,initial_FM_EP(u)))*r. % 0.22/0.55 9[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v)* -> greater_or_equal(v,initial_FM_EP(u)). % 0.22/0.55 10[0:Inp] environment(u) || in_environment(u,initial_FM_EP(u)) -> subpopulations(first_movers,efficient_producers,u,initial_FM_EP(u))*. % 0.22/0.55 11[0:Inp] environment(u) || decreases(difference(disbanding_rate(first_movers,v),disbanding_rate(efficient_producers,v)))*+ subpopulations(first_movers,efficient_producers,u,v)* -> . % 0.22/0.55 12[0:Inp] environment(u) || greater(v,w)*+ in_environment(u,v)* greater_or_equal(w,start_time(u))* -> in_environment(u,w). % 0.22/0.55 13[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.22/0.55 14[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.22/0.55 18[0:Res:1.0,11.0] || decreases(difference(disbanding_rate(first_movers,u),disbanding_rate(efficient_producers,u)))* subpopulations(first_movers,efficient_producers,skc3,u) -> . % 0.22/0.55 19[0:Res:1.0,8.0] || -> greater(disbanding_rate(first_movers,initial_FM_EP(skc3)),disbanding_rate(efficient_producers,initial_FM_EP(skc3)))*r. % 0.22/0.55 20[0:Res:1.0,10.0] || in_environment(skc3,initial_FM_EP(skc3)) -> subpopulations(first_movers,efficient_producers,skc3,initial_FM_EP(skc3))*. % 0.22/0.55 21[0:Res:1.0,9.0] || subpopulations(first_movers,efficient_producers,skc3,u)* -> greater_or_equal(u,initial_FM_EP(skc3)). % 0.22/0.55 26[0:Res:2.0,9.1] environment(skc3) || -> greater_or_equal(skc2,initial_FM_EP(skc3))*. % 0.22/0.55 27[0:Res:2.0,7.1] environment(skc3) || -> in_environment(skc3,skc2)*. % 0.22/0.55 28[0:Res:2.0,13.2] environment(skc3) || subpopulations(first_movers,efficient_producers,skc3,u)* greater_or_equal(v,u)* greater_or_equal(skc2,v) -> subpopulations(first_movers,efficient_producers,skc3,v)*. % 0.22/0.55 29[0:Res:2.0,14.4] environment(skc3) || greater_or_equal(u,v)* greater(disbanding_rate(first_movers,v),disbanding_rate(efficient_producers,v))*r greater_or_equal(skc2,u) -> decreases(difference(disbanding_rate(first_movers,u),disbanding_rate(efficient_producers,u)))* greater(disbanding_rate(first_movers,skc2),disbanding_rate(efficient_producers,skc2)). % 0.22/0.55 30[0:MRR:27.0,1.0] || -> in_environment(skc3,skc2)*. % 0.22/0.55 31[0:MRR:26.0,1.0] || -> greater_or_equal(skc2,initial_FM_EP(skc3))*. % 0.22/0.55 33[0:MRR:28.0,1.0] || greater_or_equal(u,v)* greater_or_equal(skc2,u) subpopulations(first_movers,efficient_producers,skc3,v)*+ -> subpopulations(first_movers,efficient_producers,skc3,u)*. % 0.22/0.55 35[0:MRR:29.0,29.5,1.0,3.0] || greater_or_equal(u,v)* greater_or_equal(skc2,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.22/0.55 46[0:Res:10.2,9.1] environment(u) environment(u) || in_environment(u,initial_FM_EP(u)) -> greater_or_equal(initial_FM_EP(u),initial_FM_EP(u))*. % 0.22/0.55 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.22/0.55 49[0:Res:31.0,5.0] || -> equal(initial_FM_EP(skc3),skc2) greater(skc2,initial_FM_EP(skc3))*r. % 0.22/0.55 54[1:Spt:49.0] || -> equal(initial_FM_EP(skc3),skc2)**. % 0.22/0.55 60[1:Rew:54.0,19.0] || -> greater(disbanding_rate(first_movers,skc2),disbanding_rate(efficient_producers,skc2))*r. % 0.22/0.55 64[1:MRR:60.0,3.0] || -> . % 0.22/0.55 66[1:Spt:64.0,49.0,54.0] || equal(initial_FM_EP(skc3),skc2)** -> . % 0.22/0.55 67[1:Spt:64.0,49.1] || -> greater(skc2,initial_FM_EP(skc3))*r. % 0.22/0.55 79[1:Res:67.0,12.1] environment(u) || in_environment(u,skc2) greater_or_equal(initial_FM_EP(skc3),start_time(u))* -> in_environment(u,initial_FM_EP(skc3)). % 0.22/0.55 93[1:Res:4.1,79.2] environment(skc3) environment(skc3) || in_environment(skc3,skc2) -> in_environment(skc3,initial_FM_EP(skc3))*. % 0.22/0.55 94[1:Obv:93.0] environment(skc3) || in_environment(skc3,skc2) -> in_environment(skc3,initial_FM_EP(skc3))*. % 0.22/0.55 95[1:SSi:94.0,1.0] || in_environment(skc3,skc2) -> in_environment(skc3,initial_FM_EP(skc3))*. % 0.22/0.55 96[1:MRR:95.0,30.0] || -> in_environment(skc3,initial_FM_EP(skc3))*. % 0.22/0.55 97[1:MRR:20.0,96.0] || -> subpopulations(first_movers,efficient_producers,skc3,initial_FM_EP(skc3))*. % 0.22/0.55 112[1:Res:97.0,33.2] || greater_or_equal(u,initial_FM_EP(skc3)) greater_or_equal(skc2,u) -> subpopulations(first_movers,efficient_producers,skc3,u)*. % 0.22/0.55 265[0:Res:19.0,35.2] || greater_or_equal(u,initial_FM_EP(skc3)) greater_or_equal(skc2,u) -> decreases(difference(disbanding_rate(first_movers,u),disbanding_rate(efficient_producers,u)))*. % 0.22/0.55 273[0:Res:265.2,18.0] || greater_or_equal(u,initial_FM_EP(skc3)) greater_or_equal(skc2,u) subpopulations(first_movers,efficient_producers,skc3,u)* -> . % 0.22/0.55 276[0:MRR:273.0,21.1] || greater_or_equal(skc2,u) subpopulations(first_movers,efficient_producers,skc3,u)* -> . % 0.22/0.55 279[1:MRR:112.2,276.1] || greater_or_equal(u,initial_FM_EP(skc3))* greater_or_equal(skc2,u) -> . % 0.22/0.55 284[1:Res:48.2,279.0] environment(skc3) || in_environment(skc3,initial_FM_EP(skc3)) greater_or_equal(skc2,initial_FM_EP(skc3))* -> . % 0.22/0.55 288[1:SSi:284.0,1.0] || in_environment(skc3,initial_FM_EP(skc3)) greater_or_equal(skc2,initial_FM_EP(skc3))* -> . % 0.22/0.55 289[1:MRR:288.0,288.1,96.0,31.0] || -> . % 0.22/0.55 % SZS output end Refutation % 0.22/0.55 Formulae used in the proof : prove_l2 mp_initial_time mp_greater_or_equal mp_time_point_occurs a8 mp_earliest_time_point l3 mp_times_in_order a10 mp_positive_function_difference % 0.22/0.55 %------------------------------------------------------------------------------