%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT039-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n006.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 : Unsatisfiable 0.22s 0.49s % Output : Refutation 0.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT039-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : run_spass %d %s % 0.07/0.35 % Computer : n006.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:54:46 UTC 2026 % 0.07/0.35 % CPUTime : % 0.22/0.49 % 0.22/0.49 SPASS V 3.9 % 0.22/0.49 SPASS beiseite: Proof found. % 0.22/0.49 % SZS status Theorem % 0.22/0.49 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.22/0.49 SPASS derived 108 clauses, backtracked 0 clauses, performed 0 splits and kept 89 clauses. % 0.22/0.49 SPASS allocated 75787 KBytes. % 0.22/0.49 SPASS spent 0:00:00.12 on the problem. % 0.22/0.49 0:00:00.06 for the input. % 0.22/0.49 0:00:00.00 for the FLOTTER CNF translation. % 0.22/0.49 0:00:00.00 for inferences. % 0.22/0.49 0:00:00.00 for the backtracking. % 0.22/0.49 0:00:00.01 for the reduction. % 0.22/0.49 % 0.22/0.49 % 0.22/0.49 Here is a proof with depth 8, length 59 : % 0.22/0.49 % SZS output start Refutation % 0.22/0.49 1[0:Inp] observational_period(u) || propagation_strategy(first_movers) propagation_strategy(efficient_producers) -> environment(sk1(u)) selection_favors(efficient_producers,first_movers,u)*. % 0.22/0.49 2[0:Inp] observational_period(u) || propagation_strategy(first_movers) propagation_strategy(efficient_producers) -> in_environment(u,sk1(u))* selection_favors(efficient_producers,first_movers,u)*. % 0.22/0.49 3[0:Inp] observational_period(u) || propagation_strategy(first_movers) propagation_strategy(efficient_producers) selection_favors(efficient_producers,first_movers,end_time(sk1(u)))* -> selection_favors(efficient_producers,first_movers,u). % 0.22/0.49 4[0:Inp] environment(u) slow_change(v) observational_period(v) || in_environment(v,u) -> in_environment(u,sk2(u,v))*. % 0.22/0.49 5[0:Inp] environment(u) slow_change(v) observational_period(v) || in_environment(v,u) -> greater(sk2(u,v),critical_point(u))*l. % 0.22/0.49 6[0:Inp] || -> propagation_strategy(first_movers)*. % 0.22/0.49 7[0:Inp] || -> propagation_strategy(efficient_producers)*. % 0.22/0.49 8[0:Inp] environment(u) || greater_or_equal(v,start_time(u))*+ greater_or_equal(end_time(u),v)* -> in_environment(u,v). % 0.22/0.49 9[0:Inp] environment(u) || in_environment(u,v) -> greater_or_equal(end_time(u),v)*. % 0.22/0.49 10[0:Inp] environment(u) || -> greater_or_equal(critical_point(u),start_time(u))*. % 0.22/0.49 11[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.22/0.49 12[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 0.22/0.49 13[0:Inp] || greater(u,v) -> greater_or_equal(u,v)*. % 0.22/0.49 14[0:Inp] || equal(u,v) -> greater_or_equal(u,v)*. % 0.22/0.49 16[0:Inp] environment(u) || in_environment(u,v)* greater(v,critical_point(u))+ -> selection_favors(efficient_producers,first_movers,v)*. % 0.22/0.49 17[0:Inp] || -> observational_period(sk3)*. % 0.22/0.49 18[0:Inp] || -> slow_change(sk3)*. % 0.22/0.49 19[0:Inp] || selection_favors(efficient_producers,first_movers,sk3)* -> . % 0.22/0.49 20[0:MRR:1.1,1.2,6.0,7.0] observational_period(u) || -> environment(sk1(u)) selection_favors(efficient_producers,first_movers,u)*. % 0.22/0.49 21[0:MRR:2.1,2.2,6.0,7.0] observational_period(u) || -> in_environment(u,sk1(u))* selection_favors(efficient_producers,first_movers,u)*. % 0.22/0.49 22[0:MRR:3.1,3.2,6.0,7.0] observational_period(u) || selection_favors(efficient_producers,first_movers,end_time(sk1(u)))* -> selection_favors(efficient_producers,first_movers,u). % 0.22/0.49 24[0:Res:18.0,4.1] observational_period(sk3) environment(u) || in_environment(sk3,u) -> in_environment(u,sk2(u,sk3))*. % 0.22/0.49 25[0:Res:17.0,5.0] slow_change(sk3) environment(u) || in_environment(sk3,u) -> greater(sk2(u,sk3),critical_point(u))*l. % 0.22/0.49 30[0:Res:22.2,19.0] observational_period(sk3) || selection_favors(efficient_producers,first_movers,end_time(sk1(sk3)))* -> . % 0.22/0.49 31[0:Res:21.2,19.0] observational_period(sk3) || -> in_environment(sk3,sk1(sk3))*. % 0.22/0.49 32[0:Res:20.2,19.0] observational_period(sk3) || -> environment(sk1(sk3))*. % 0.22/0.49 34[0:MRR:32.0,17.0] || -> environment(sk1(sk3))*. % 0.22/0.49 35[0:MRR:31.0,17.0] || -> in_environment(sk3,sk1(sk3))*. % 0.22/0.49 36[0:MRR:30.0,17.0] || selection_favors(efficient_producers,first_movers,end_time(sk1(sk3)))* -> . % 0.22/0.49 37[0:MRR:24.0,17.0] environment(u) || in_environment(sk3,u) -> in_environment(u,sk2(u,sk3))*. % 0.22/0.49 38[0:MRR:25.0,18.0] environment(u) || in_environment(sk3,u) -> greater(sk2(u,sk3),critical_point(u))*l. % 0.22/0.49 45[0:Res:9.2,12.0] environment(u) || in_environment(u,v)* -> equal(end_time(u),v) greater(end_time(u),v). % 0.22/0.49 46[0:Res:10.1,12.0] environment(u) || -> equal(start_time(u),critical_point(u)) greater(critical_point(u),start_time(u))*r. % 0.22/0.49 48[0:Res:14.1,8.1] environment(u) || equal(v,start_time(u)) greater_or_equal(end_time(u),v)* -> in_environment(u,v). % 0.22/0.49 49[0:Res:9.2,8.1] environment(u) environment(v) || in_environment(u,start_time(v)) greater_or_equal(end_time(v),end_time(u))* -> in_environment(v,end_time(u)). % 0.22/0.49 55[0:Res:13.1,48.2] environment(u) || greater(end_time(u),v) equal(v,start_time(u)) -> in_environment(u,v)*. % 0.22/0.49 73[0:Res:37.2,45.1] environment(u) environment(u) || in_environment(sk3,u) -> equal(sk2(u,sk3),end_time(u)) greater(end_time(u),sk2(u,sk3))*r. % 0.22/0.49 77[0:Obv:73.0] environment(u) || in_environment(sk3,u) -> equal(sk2(u,sk3),end_time(u)) greater(end_time(u),sk2(u,sk3))*r. % 0.22/0.49 97[0:Res:14.1,49.3] environment(u) environment(v) || equal(end_time(v),end_time(u))+ in_environment(u,start_time(v))* -> in_environment(v,end_time(u))*. % 0.22/0.49 101[0:EqR:97.2] environment(u) environment(u) || in_environment(u,start_time(u))* -> in_environment(u,end_time(u)). % 0.22/0.49 102[0:Obv:101.0] environment(u) || in_environment(u,start_time(u))* -> in_environment(u,end_time(u)). % 0.22/0.49 104[0:Res:55.3,102.1] environment(u) environment(u) || greater(end_time(u),start_time(u)) equal(start_time(u),start_time(u)) -> in_environment(u,end_time(u))*. % 0.22/0.49 107[0:Obv:104.3] environment(u) || greater(end_time(u),start_time(u)) -> in_environment(u,end_time(u))*. % 0.22/0.49 121[0:OCh:11.1,11.0,77.3,38.2] environment(u) environment(u) || in_environment(sk3,u) in_environment(sk3,u) -> equal(sk2(u,sk3),end_time(u))** greater(end_time(u),critical_point(u)). % 0.22/0.49 123[0:Obv:121.2] environment(u) || in_environment(sk3,u) -> equal(sk2(u,sk3),end_time(u))** greater(end_time(u),critical_point(u)). % 0.22/0.49 126[0:SpR:123.2,38.2] environment(u) environment(u) || in_environment(sk3,u)* in_environment(sk3,u)* -> greater(end_time(u),critical_point(u)) greater(end_time(u),critical_point(u)). % 0.22/0.49 136[0:Obv:126.4] environment(u) || in_environment(sk3,u)* -> greater(end_time(u),critical_point(u)). % 0.22/0.49 140[0:Res:35.0,136.1] environment(sk1(sk3)) || -> greater(end_time(sk1(sk3)),critical_point(sk1(sk3)))*r. % 0.22/0.49 150[0:SSi:140.0,34.0] || -> greater(end_time(sk1(sk3)),critical_point(sk1(sk3)))*r. % 0.22/0.49 156[0:Res:150.0,16.2] environment(sk1(sk3)) || in_environment(sk1(sk3),end_time(sk1(sk3))) -> selection_favors(efficient_producers,first_movers,end_time(sk1(sk3)))*. % 0.22/0.49 159[0:SSi:156.0,34.0] || in_environment(sk1(sk3),end_time(sk1(sk3))) -> selection_favors(efficient_producers,first_movers,end_time(sk1(sk3)))*. % 0.22/0.49 160[0:MRR:159.1,36.0] || in_environment(sk1(sk3),end_time(sk1(sk3)))* -> . % 0.22/0.49 166[0:Res:107.2,160.0] environment(sk1(sk3)) || greater(end_time(sk1(sk3)),start_time(sk1(sk3)))*r -> . % 0.22/0.49 169[0:SSi:166.0,34.0] || greater(end_time(sk1(sk3)),start_time(sk1(sk3)))*r -> . % 0.22/0.49 172[0:NCh:11.2,11.1,169.0,46.2] environment(sk1(sk3)) || greater(end_time(sk1(sk3)),critical_point(sk1(sk3))) -> equal(start_time(sk1(sk3)),critical_point(sk1(sk3)))**. % 0.22/0.49 175[0:SSi:172.0,34.0] || greater(end_time(sk1(sk3)),critical_point(sk1(sk3))) -> equal(start_time(sk1(sk3)),critical_point(sk1(sk3)))**. % 0.22/0.49 176[0:MRR:175.0,150.0] || -> equal(start_time(sk1(sk3)),critical_point(sk1(sk3)))**. % 0.22/0.49 178[0:Rew:176.0,169.0] || greater(end_time(sk1(sk3)),critical_point(sk1(sk3)))*r -> . % 0.22/0.49 179[0:MRR:178.0,150.0] || -> . % 0.22/0.49 % SZS output end Refutation % 0.22/0.49 Formulae used in the proof : mp3_favoured_trategy_20 mp3_favoured_trategy_21 mp3_favoured_trategy_22 mp4_critical_point_23 mp4_critical_point_24 mp_organizational_sets1_25 mp_organizational_sets2_26 mp_time_in_environment_27 mp_environment_end_point_28 mp_time_of_critical_point_29 mp_greater_transitivity_30 mp_greater_or_equal_31 mp_greater_or_equal_32 mp_greater_or_equal_33 l8_35 prove_t8_36 prove_t8_37 prove_t8_38 % 0.22/0.49 %------------------------------------------------------------------------------