%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : MGT019+2 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n017.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:15:20 AM UTC 2026 % Result : CounterSatisfiable 0.12s 0.37s % Output : Saturation 0.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT019+2 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.03 % Command : metis --show proof --show saturation %s % 0.08/0.35 % Computer : n017.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 11:53:54 UTC 2026 % 0.08/0.35 % CPUTime : % 0.12/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.12/0.37 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.12/0.37 % 0.12/0.37 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.12/0.37 |- ~greater (disbanding_rate first_movers skolemFOFtoCNF_T) % 0.12/0.37 (disbanding_rate efficient_producers skolemFOFtoCNF_T) % 0.12/0.37 |- environment skolemFOFtoCNF_E % 0.12/0.37 |- subpopulations first_movers efficient_producers skolemFOFtoCNF_E % 0.12/0.37 skolemFOFtoCNF_T % 0.12/0.37 |- ~greater (disbanding_rate first_movers $T) % 0.12/0.37 (disbanding_rate efficient_producers $T) \/ % 0.12/0.37 ~greater_or_equal (founding_rate efficient_producers $T) % 0.12/0.37 (founding_rate first_movers $T) \/ % 0.12/0.37 greater (growth_rate efficient_producers $T) % 0.12/0.37 (growth_rate first_movers $T) % 0.12/0.37 |- ~greater_or_equal $X $Y \/ $X = $Y \/ greater $X $Y % 0.12/0.37 |- ~environment $E \/ ~stable $E \/ % 0.12/0.37 in_environment $E (skolemFOFtoCNF_To $E) % 0.12/0.37 |- ~environment $E \/ ~greater_or_equal $T (skolemFOFtoCNF_To $E) \/ % 0.12/0.37 ~stable $E \/ ~subpopulations first_movers efficient_producers $E $T \/ % 0.12/0.37 greater_or_equal (founding_rate efficient_producers $T) % 0.12/0.37 (founding_rate first_movers $T) % 0.12/0.37 |- environment skolemFOFtoCNF_E_1 % 0.12/0.37 |- stable skolemFOFtoCNF_E_1 % 0.12/0.37 |- ~greater (growth_rate efficient_producers (skolemFOFtoCNF_T_1 $To)) % 0.12/0.37 (growth_rate first_movers (skolemFOFtoCNF_T_1 $To)) \/ % 0.12/0.37 ~in_environment skolemFOFtoCNF_E_1 $To % 0.12/0.37 |- ~in_environment skolemFOFtoCNF_E_1 $To \/ % 0.12/0.37 greater_or_equal (skolemFOFtoCNF_T_1 $To) $To % 0.12/0.37 |- ~in_environment skolemFOFtoCNF_E_1 $To \/ % 0.12/0.37 subpopulations first_movers efficient_producers skolemFOFtoCNF_E_1 % 0.12/0.37 (skolemFOFtoCNF_T_1 $To) % 0.12/0.37 |- in_environment skolemFOFtoCNF_E_1 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1) % 0.12/0.37 |- subpopulations first_movers efficient_producers skolemFOFtoCNF_E_1 % 0.12/0.37 (skolemFOFtoCNF_T_1 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1)) % 0.12/0.37 |- greater_or_equal % 0.12/0.37 (skolemFOFtoCNF_T_1 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1)) % 0.12/0.37 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1) % 0.12/0.37 |- skolemFOFtoCNF_T_1 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1) = % 0.12/0.37 skolemFOFtoCNF_To skolemFOFtoCNF_E_1 \/ % 0.12/0.37 greater (skolemFOFtoCNF_T_1 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1)) % 0.12/0.37 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1) % 0.12/0.37 |- ~greater_or_equal skolemFOFtoCNF_T % 0.12/0.37 (skolemFOFtoCNF_To skolemFOFtoCNF_E) \/ ~stable skolemFOFtoCNF_E \/ % 0.12/0.37 greater_or_equal (founding_rate efficient_producers skolemFOFtoCNF_T) % 0.12/0.37 (founding_rate first_movers skolemFOFtoCNF_T) % 0.12/0.37 |- greater_or_equal % 0.12/0.37 (founding_rate efficient_producers % 0.12/0.37 (skolemFOFtoCNF_T_1 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1))) % 0.12/0.37 (founding_rate first_movers % 0.12/0.37 (skolemFOFtoCNF_T_1 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1))) % 0.12/0.37 |- founding_rate efficient_producers % 0.12/0.37 (skolemFOFtoCNF_T_1 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1)) = % 0.12/0.37 founding_rate first_movers % 0.12/0.37 (skolemFOFtoCNF_T_1 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1)) \/ % 0.12/0.37 greater % 0.12/0.37 (founding_rate efficient_producers % 0.12/0.37 (skolemFOFtoCNF_T_1 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1))) % 0.12/0.37 (founding_rate first_movers % 0.12/0.37 (skolemFOFtoCNF_T_1 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1))) % 0.12/0.37 |- ~greater % 0.12/0.37 (disbanding_rate first_movers % 0.12/0.37 (skolemFOFtoCNF_T_1 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1))) % 0.12/0.37 (disbanding_rate efficient_producers % 0.12/0.37 (skolemFOFtoCNF_T_1 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1))) \/ % 0.12/0.37 greater % 0.12/0.37 (growth_rate efficient_producers % 0.12/0.37 (skolemFOFtoCNF_T_1 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1))) % 0.12/0.37 (growth_rate first_movers % 0.12/0.37 (skolemFOFtoCNF_T_1 (skolemFOFtoCNF_To skolemFOFtoCNF_E_1))) % 0.12/0.37 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.12/0.37 %------------------------------------------------------------------------------