%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT039+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n009.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 : Theorem 0.23s 0.54s % Output : Refutation 0.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT039+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.04 % Command : run_spass %d %s % 0.08/0.35 % Computer : n009.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Mon Sep 7 12:53:37 UTC 2026 % 0.14/0.36 % CPUTime : % 0.23/0.54 % 0.23/0.54 SPASS V 3.9 % 0.23/0.54 SPASS beiseite: Proof found. % 0.23/0.54 % SZS status Theorem % 0.23/0.54 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.23/0.54 SPASS derived 125 clauses, backtracked 7 clauses, performed 1 splits and kept 117 clauses. % 0.23/0.54 SPASS allocated 97775 KBytes. % 0.23/0.54 SPASS spent 0:00:00.17 on the problem. % 0.23/0.54 0:00:00.06 for the input. % 0.23/0.54 0:00:00.05 for the FLOTTER CNF translation. % 0.23/0.54 0:00:00.00 for inferences. % 0.23/0.54 0:00:00.00 for the backtracking. % 0.23/0.54 0:00:00.02 for the reduction. % 0.23/0.54 % 0.23/0.54 % 0.23/0.54 Here is a proof with depth 8, length 56 : % 0.23/0.54 % SZS output start Refutation % 0.23/0.54 1[0:Inp] || -> observational_period(skc1)*. % 0.23/0.54 2[0:Inp] || -> slow_change(skc1)*. % 0.23/0.54 3[0:Inp] || -> propagation_strategy(first_movers)*. % 0.23/0.54 4[0:Inp] || -> propagation_strategy(efficient_producers)*. % 0.23/0.54 5[0:Inp] || -> environment(skf2(u))*. % 0.23/0.54 6[0:Inp] || selection_favors(efficient_producers,first_movers,skc1)* -> . % 0.23/0.54 7[0:Inp] || greater(u,v) -> greater_or_equal(u,v)*. % 0.23/0.54 8[0:Inp] || equal(u,v) -> greater_or_equal(u,v)*. % 0.23/0.54 9[0:Inp] environment(u) || -> greater_or_equal(critical_point(u),start_time(u))*. % 0.23/0.54 10[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 0.23/0.54 11[0:Inp] environment(u) || in_environment(u,v) -> greater_or_equal(end_time(u),v)*. % 0.23/0.54 12[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.23/0.54 13[0:Inp] environment(u) || greater_or_equal(v,start_time(u))*+ greater_or_equal(end_time(u),v)* -> in_environment(u,v). % 0.23/0.54 15[0:Inp] environment(u) || in_environment(u,v)* greater(v,critical_point(u))+ -> selection_favors(efficient_producers,first_movers,v)*. % 0.23/0.54 16[0:Inp] observational_period(u) || propagation_strategy(efficient_producers) propagation_strategy(first_movers) -> in_environment(u,skf2(u))* selection_favors(efficient_producers,first_movers,u)*. % 0.23/0.54 17[0:Inp] environment(u) slow_change(v) observational_period(v) || in_environment(v,u)*+ -> in_environment(u,skf3(u))*. % 0.23/0.54 18[0:Inp] environment(u) slow_change(v) observational_period(v) || in_environment(v,u)* -> greater(skf3(u),critical_point(u)). % 0.23/0.54 19[0:Inp] observational_period(u) || selection_favors(efficient_producers,first_movers,end_time(skf2(u)))* propagation_strategy(efficient_producers) propagation_strategy(first_movers) -> selection_favors(efficient_producers,first_movers,u). % 0.23/0.54 20[0:MRR:16.1,16.2,4.0,3.0] observational_period(u) || -> in_environment(u,skf2(u))* selection_favors(efficient_producers,first_movers,u)*. % 0.23/0.54 21[0:MRR:19.2,19.3,4.0,3.0] observational_period(u) || selection_favors(efficient_producers,first_movers,end_time(skf2(u)))* -> selection_favors(efficient_producers,first_movers,u). % 0.23/0.54 24[0:Res:1.0,18.0] slow_change(skc1) environment(u) || in_environment(skc1,u)* -> greater(skf3(u),critical_point(u)). % 0.23/0.54 28[0:Res:21.2,6.0] observational_period(skc1) || selection_favors(efficient_producers,first_movers,end_time(skf2(skc1)))* -> . % 0.23/0.54 29[0:Res:20.2,6.0] observational_period(skc1) || -> in_environment(skc1,skf2(skc1))*. % 0.23/0.54 31[0:MRR:29.0,1.0] || -> in_environment(skc1,skf2(skc1))*. % 0.23/0.54 32[0:MRR:28.0,1.0] || selection_favors(efficient_producers,first_movers,end_time(skf2(skc1)))* -> . % 0.23/0.54 34[0:MRR:24.0,2.0] environment(u) || in_environment(skc1,u)* -> greater(skf3(u),critical_point(u)). % 0.23/0.54 38[0:Res:11.2,10.0] environment(u) || in_environment(u,v)* -> equal(end_time(u),v) greater(end_time(u),v). % 0.23/0.54 39[0:Res:9.1,10.0] environment(u) || -> equal(start_time(u),critical_point(u)) greater(critical_point(u),start_time(u))*r. % 0.23/0.54 40[0:Res:7.1,13.1] environment(u) || greater(v,start_time(u)) greater_or_equal(end_time(u),v)* -> in_environment(u,v). % 0.23/0.54 48[0:Res:31.0,17.3] environment(skf2(skc1)) slow_change(skc1) observational_period(skc1) || -> in_environment(skf2(skc1),skf3(skf2(skc1)))*. % 0.23/0.54 52[0:SSi:48.2,48.1,48.0,2.0,1.0,2.0,1.0,5.0,2.0,1.0] || -> in_environment(skf2(skc1),skf3(skf2(skc1)))*. % 0.23/0.54 63[0:Res:31.0,34.1] environment(skf2(skc1)) || -> greater(skf3(skf2(skc1)),critical_point(skf2(skc1)))*l. % 0.23/0.54 67[0:SSi:63.0,5.0,2.0,1.0] || -> greater(skf3(skf2(skc1)),critical_point(skf2(skc1)))*l. % 0.23/0.54 68[0:Res:67.0,15.2] environment(skf2(skc1)) || in_environment(skf2(skc1),skf3(skf2(skc1))) -> selection_favors(efficient_producers,first_movers,skf3(skf2(skc1)))*. % 0.23/0.54 71[0:SSi:68.0,5.0,2.0,1.0] || in_environment(skf2(skc1),skf3(skf2(skc1))) -> selection_favors(efficient_producers,first_movers,skf3(skf2(skc1)))*. % 0.23/0.54 72[0:MRR:71.0,52.0] || -> selection_favors(efficient_producers,first_movers,skf3(skf2(skc1)))*. % 0.23/0.54 91[0:Res:52.0,38.1] environment(skf2(skc1)) || -> equal(skf3(skf2(skc1)),end_time(skf2(skc1))) greater(end_time(skf2(skc1)),skf3(skf2(skc1)))*r. % 0.23/0.54 93[0:SSi:91.0,5.0,2.0,1.0] || -> equal(skf3(skf2(skc1)),end_time(skf2(skc1))) greater(end_time(skf2(skc1)),skf3(skf2(skc1)))*r. % 0.23/0.54 102[1:Spt:93.0] || -> equal(skf3(skf2(skc1)),end_time(skf2(skc1)))**. % 0.23/0.54 105[1:Rew:102.0,72.0] || -> selection_favors(efficient_producers,first_movers,end_time(skf2(skc1)))*. % 0.23/0.54 108[1:MRR:105.0,32.0] || -> . % 0.23/0.54 109[1:Spt:108.0,93.0,102.0] || equal(skf3(skf2(skc1)),end_time(skf2(skc1)))** -> . % 0.23/0.54 110[1:Spt:108.0,93.1] || -> greater(end_time(skf2(skc1)),skf3(skf2(skc1)))*r. % 0.23/0.54 115[0:Res:8.1,40.2] environment(u) || equal(end_time(u),v) greater(v,start_time(u)) -> in_environment(u,v)*. % 0.23/0.54 120[1:OCh:12.1,12.0,67.0,110.0] || -> greater(end_time(skf2(skc1)),critical_point(skf2(skc1)))*r. % 0.23/0.54 123[1:Res:120.0,15.2] environment(skf2(skc1)) || in_environment(skf2(skc1),end_time(skf2(skc1))) -> selection_favors(efficient_producers,first_movers,end_time(skf2(skc1)))*. % 0.23/0.54 126[1:SSi:123.0,5.0,2.0,1.0] || in_environment(skf2(skc1),end_time(skf2(skc1))) -> selection_favors(efficient_producers,first_movers,end_time(skf2(skc1)))*. % 0.23/0.54 127[1:MRR:126.1,32.0] || in_environment(skf2(skc1),end_time(skf2(skc1)))* -> . % 0.23/0.54 167[1:Res:115.3,127.0] environment(skf2(skc1)) || equal(end_time(skf2(skc1)),end_time(skf2(skc1))) greater(end_time(skf2(skc1)),start_time(skf2(skc1)))*r -> . % 0.23/0.54 170[1:Obv:167.1] environment(skf2(skc1)) || greater(end_time(skf2(skc1)),start_time(skf2(skc1)))*r -> . % 0.23/0.54 171[1:SSi:170.0,5.0,2.0,1.0] || greater(end_time(skf2(skc1)),start_time(skf2(skc1)))*r -> . % 0.23/0.54 183[1:NCh:12.2,12.1,171.0,39.2] environment(skf2(skc1)) || greater(end_time(skf2(skc1)),critical_point(skf2(skc1))) -> equal(start_time(skf2(skc1)),critical_point(skf2(skc1)))**. % 0.23/0.54 186[1:SSi:183.0,5.0,2.0,1.0] || greater(end_time(skf2(skc1)),critical_point(skf2(skc1))) -> equal(start_time(skf2(skc1)),critical_point(skf2(skc1)))**. % 0.23/0.54 187[1:MRR:186.0,120.0] || -> equal(start_time(skf2(skc1)),critical_point(skf2(skc1)))**. % 0.23/0.54 190[1:Rew:187.0,171.0] || greater(end_time(skf2(skc1)),critical_point(skf2(skc1)))*r -> . % 0.23/0.54 193[1:MRR:190.0,120.0] || -> . % 0.23/0.54 % SZS output end Refutation % 0.23/0.54 Formulae used in the proof : prove_t8 mp_organizational_sets1 mp_organizational_sets2 mp3_favoured_trategy mp_greater_or_equal mp_time_of_critical_point mp_environment_end_point mp_greater_transitivity mp_time_in_environment l8 mp4_critical_point % 0.23/0.54 %------------------------------------------------------------------------------