%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : MGT033+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n003.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:44 AM UTC 2026 % Result : CounterSatisfiable 0.11s 0.43s % Output : Saturation 0.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT033+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.04 % Command : metis --show proof --show saturation %s % 0.11/0.36 % Computer : n003.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Mon Sep 7 12:24:38 UTC 2026 % 0.11/0.36 % CPUTime : % 0.11/0.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.11/0.43 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.11/0.43 % 0.11/0.43 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.11/0.43 |- ~(cardinality_at_time $S2 $T = zero) \/ ~environment $E \/ % 0.11/0.43 ~greater (cardinality_at_time $S1 $T) zero \/ % 0.11/0.43 ~subpopulation $S1 $E $T \/ ~subpopulation $S2 $E $T \/ % 0.11/0.43 selection_favors $S1 $S2 $T % 0.11/0.43 |- ~environment $E \/ ~greater (appear $X $E) $T \/ % 0.11/0.43 ~in_environment $E $T \/ cardinality_at_time $X $T = zero % 0.11/0.43 |- ~environment $E \/ ~greater (number_of_organizations $E $T) zero \/ % 0.11/0.43 greater (cardinality_at_time (skolemFOFtoCNF_X $E $T) $T) zero % 0.11/0.43 |- ~environment $E \/ ~greater (number_of_organizations $E $T) zero \/ % 0.11/0.43 subpopulation (skolemFOFtoCNF_X $E $T) $E $T % 0.11/0.43 |- ~(cardinality_at_time $X t = zero) \/ % 0.11/0.43 ~greater (cardinality_at_time $X $T) zero % 0.11/0.43 |- ~environment $E \/ ~greater (number_of_organizations $E $T) zero \/ % 0.11/0.43 in_environment $E $T % 0.11/0.43 |- ~environment $E \/ ~greater_or_equal $T $T1 \/ % 0.11/0.43 ~greater_or_equal $T2 $T \/ ~in_environment $E $T1 \/ % 0.11/0.43 ~in_environment $E $T2 \/ in_environment $E $T % 0.11/0.43 |- ~environment $E \/ in_environment $E (start_time $E) % 0.11/0.43 |- ~environment $E \/ % 0.11/0.43 greater_or_equal (appear first_movers $E) (start_time $E) % 0.11/0.43 |- ~environment $E \/ ~in_environment $E $T \/ % 0.11/0.43 subpopulation efficient_producers $E $T % 0.11/0.43 |- ~environment $E \/ ~in_environment $E $T \/ % 0.11/0.43 subpopulation first_movers $E $T % 0.11/0.43 |- ~environment $E \/ ~in_environment $E (appear first_movers $E) \/ % 0.11/0.43 in_environment $E (appear an_organisation $E) % 0.11/0.43 |- ~environment $E \/ ~greater_or_equal $T (appear an_organisation $E) \/ % 0.11/0.43 ~in_environment $E $T \/ greater (number_of_organizations $E $T) zero % 0.11/0.43 |- ~environment $E \/ ~greater (cardinality_at_time $X $T) zero \/ % 0.11/0.43 ~subpopulation $X $E $T \/ $X = efficient_producers \/ $X = first_movers % 0.11/0.43 |- ~environment $E \/ ~in_environment $E (appear an_organisation $E) \/ % 0.11/0.43 appear an_organisation $E = appear first_movers $E % 0.11/0.43 |- ~(cardinality_at_time $S2 $T = zero) \/ ~environment $E \/ % 0.11/0.43 ~greater zero zero \/ ~subpopulation $S2 $E $T \/ % 0.11/0.43 selection_favors $S2 $S2 $T % 0.11/0.43 |- ~environment $E \/ ~greater_or_equal $T $T2 \/ % 0.11/0.43 ~greater_or_equal $T2 $T \/ ~in_environment $E $T2 \/ % 0.11/0.43 in_environment $E $T % 0.11/0.43 |- ~selection_favors first_movers efficient_producers skolemFOFtoCNF_T % 0.11/0.43 |- environment skolemFOFtoCNF_E % 0.11/0.43 |- greater (appear efficient_producers skolemFOFtoCNF_E) skolemFOFtoCNF_T % 0.11/0.43 |- greater_or_equal skolemFOFtoCNF_T % 0.11/0.43 (appear an_organisation skolemFOFtoCNF_E) % 0.11/0.43 |- in_environment skolemFOFtoCNF_E skolemFOFtoCNF_T % 0.11/0.43 |- in_environment skolemFOFtoCNF_E (start_time skolemFOFtoCNF_E) % 0.11/0.43 |- greater_or_equal (appear an_organisation skolemFOFtoCNF_E) % 0.11/0.43 (start_time skolemFOFtoCNF_E) % 0.11/0.43 |- subpopulation efficient_producers skolemFOFtoCNF_E skolemFOFtoCNF_T % 0.11/0.43 |- subpopulation efficient_producers skolemFOFtoCNF_E % 0.11/0.43 (start_time skolemFOFtoCNF_E) % 0.11/0.43 |- subpopulation first_movers skolemFOFtoCNF_E skolemFOFtoCNF_T % 0.11/0.43 |- subpopulation first_movers skolemFOFtoCNF_E % 0.11/0.43 (start_time skolemFOFtoCNF_E) % 0.11/0.43 |- cardinality_at_time efficient_producers skolemFOFtoCNF_T = zero % 0.11/0.43 |- ~greater_or_equal $_22 skolemFOFtoCNF_T \/ % 0.11/0.43 ~greater_or_equal skolemFOFtoCNF_T $_22 \/ % 0.11/0.43 in_environment skolemFOFtoCNF_E $_22 % 0.11/0.43 |- ~greater_or_equal $_22 (start_time skolemFOFtoCNF_E) \/ % 0.11/0.43 ~greater_or_equal (start_time skolemFOFtoCNF_E) $_22 \/ % 0.11/0.43 in_environment skolemFOFtoCNF_E $_22 % 0.11/0.43 |- ~(cardinality_at_time efficient_producers % 0.11/0.43 (start_time skolemFOFtoCNF_E) = zero) \/ ~greater zero zero \/ % 0.11/0.43 selection_favors efficient_producers efficient_producers % 0.11/0.43 (start_time skolemFOFtoCNF_E) % 0.11/0.43 |- ~(cardinality_at_time first_movers (start_time skolemFOFtoCNF_E) = % 0.11/0.43 zero) \/ ~greater zero zero \/ % 0.11/0.43 selection_favors first_movers first_movers (start_time skolemFOFtoCNF_E) % 0.11/0.43 |- ~environment $_34 \/ % 0.11/0.43 ~greater_or_equal $_37 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.11/0.43 ~in_environment $_34 $_37 \/ % 0.11/0.43 ~in_environment $_34 (start_time skolemFOFtoCNF_E) \/ % 0.11/0.43 in_environment $_34 (appear an_organisation skolemFOFtoCNF_E) % 0.11/0.43 |- ~environment $_34 \/ % 0.11/0.43 ~greater_or_equal (start_time skolemFOFtoCNF_E) $_36 \/ % 0.11/0.43 ~in_environment $_34 $_36 \/ % 0.11/0.43 ~in_environment $_34 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.11/0.43 in_environment $_34 (start_time skolemFOFtoCNF_E) % 0.11/0.43 |- ~greater_or_equal $_35 skolemFOFtoCNF_T \/ % 0.11/0.43 ~greater_or_equal $_37 $_35 \/ ~in_environment skolemFOFtoCNF_E $_37 \/ % 0.11/0.43 in_environment skolemFOFtoCNF_E $_35 % 0.11/0.43 |- ~greater_or_equal $_35 (start_time skolemFOFtoCNF_E) \/ % 0.11/0.43 ~greater_or_equal $_37 $_35 \/ ~in_environment skolemFOFtoCNF_E $_37 \/ % 0.11/0.43 in_environment skolemFOFtoCNF_E $_35 % 0.11/0.43 |- ~greater_or_equal $_35 $_36 \/ % 0.11/0.43 ~greater_or_equal skolemFOFtoCNF_T $_35 \/ % 0.11/0.43 ~in_environment skolemFOFtoCNF_E $_36 \/ % 0.11/0.43 in_environment skolemFOFtoCNF_E $_35 % 0.11/0.43 |- ~greater_or_equal $_35 $_36 \/ % 0.11/0.43 ~greater_or_equal (start_time skolemFOFtoCNF_E) $_35 \/ % 0.11/0.43 ~in_environment skolemFOFtoCNF_E $_36 \/ % 0.11/0.43 in_environment skolemFOFtoCNF_E $_35 % 0.11/0.43 |- ~greater_or_equal $_40 skolemFOFtoCNF_T \/ % 0.11/0.43 ~greater_or_equal (start_time skolemFOFtoCNF_E) $_40 \/ % 0.11/0.43 in_environment skolemFOFtoCNF_E $_40 % 0.11/0.43 |- ~greater_or_equal $_43 (start_time skolemFOFtoCNF_E) \/ % 0.11/0.43 ~greater_or_equal skolemFOFtoCNF_T $_43 \/ % 0.11/0.43 in_environment skolemFOFtoCNF_E $_43 % 0.11/0.43 |- ~greater_or_equal $T $T1 \/ % 0.11/0.43 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) $T \/ % 0.11/0.43 ~in_environment skolemFOFtoCNF_E $T1 \/ % 0.11/0.43 in_environment skolemFOFtoCNF_E $T % 0.11/0.43 |- ~greater_or_equal $T (appear an_organisation skolemFOFtoCNF_E) \/ % 0.11/0.43 ~greater_or_equal $T2 $T \/ ~in_environment skolemFOFtoCNF_E $T2 \/ % 0.11/0.43 in_environment skolemFOFtoCNF_E $T % 0.11/0.43 |- ~greater_or_equal $T (appear an_organisation skolemFOFtoCNF_E) \/ % 0.11/0.43 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) $T \/ % 0.11/0.43 in_environment skolemFOFtoCNF_E $T % 0.11/0.43 |- subpopulation first_movers skolemFOFtoCNF_E % 0.11/0.43 (appear an_organisation skolemFOFtoCNF_E) % 0.11/0.43 |- subpopulation efficient_producers skolemFOFtoCNF_E % 0.11/0.43 (appear an_organisation skolemFOFtoCNF_E) % 0.11/0.43 |- in_environment skolemFOFtoCNF_E % 0.11/0.43 (appear an_organisation skolemFOFtoCNF_E) % 0.11/0.43 |- ~greater_or_equal $_35 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.11/0.43 ~greater_or_equal skolemFOFtoCNF_T $_35 \/ % 0.11/0.43 in_environment skolemFOFtoCNF_E $_35 % 0.11/0.43 |- ~greater_or_equal $_35 skolemFOFtoCNF_T \/ % 0.11/0.43 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) $_35 \/ % 0.11/0.43 in_environment skolemFOFtoCNF_E $_35 % 0.11/0.43 |- ~greater_or_equal $_35 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.11/0.43 ~greater_or_equal (start_time skolemFOFtoCNF_E) $_35 \/ % 0.11/0.43 in_environment skolemFOFtoCNF_E $_35 % 0.11/0.43 |- appear an_organisation skolemFOFtoCNF_E = % 0.11/0.43 appear first_movers skolemFOFtoCNF_E % 0.11/0.43 |- ~(cardinality_at_time first_movers % 0.11/0.43 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.11/0.43 ~greater zero zero \/ % 0.11/0.43 selection_favors first_movers first_movers % 0.11/0.43 (appear an_organisation skolemFOFtoCNF_E) % 0.11/0.43 |- greater (number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T) zero % 0.11/0.43 |- ~greater (appear an_organisation skolemFOFtoCNF_E) $T \/ % 0.11/0.43 ~in_environment skolemFOFtoCNF_E $T \/ % 0.11/0.43 cardinality_at_time first_movers $T = zero % 0.11/0.43 |- ~(cardinality_at_time efficient_producers % 0.11/0.43 (appear an_organisation skolemFOFtoCNF_E) = zero) \/ % 0.11/0.43 ~greater zero zero \/ % 0.11/0.43 selection_favors efficient_producers efficient_producers % 0.11/0.43 (appear an_organisation skolemFOFtoCNF_E) % 0.11/0.43 |- greater zero zero % 0.11/0.43 |- ~(cardinality_at_time efficient_producers t = zero) % 0.11/0.43 |- ~greater_or_equal $_51 (start_time skolemFOFtoCNF_E) \/ % 0.11/0.43 ~greater_or_equal (appear an_organisation skolemFOFtoCNF_E) $_51 \/ % 0.11/0.43 in_environment skolemFOFtoCNF_E $_51 % 0.11/0.44 |- ~environment $_34 \/ % 0.11/0.44 ~greater_or_equal (start_time skolemFOFtoCNF_E) % 0.11/0.44 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.11/0.44 ~in_environment $_34 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.11/0.44 in_environment $_34 (start_time skolemFOFtoCNF_E) % 0.11/0.44 |- ~environment $_34 \/ % 0.11/0.44 ~greater_or_equal (start_time skolemFOFtoCNF_E) % 0.11/0.44 (appear an_organisation skolemFOFtoCNF_E) \/ % 0.11/0.44 ~in_environment $_34 (start_time skolemFOFtoCNF_E) \/ % 0.11/0.44 in_environment $_34 (appear an_organisation skolemFOFtoCNF_E) % 0.11/0.44 |- ~environment $_63 \/ ~in_environment $_63 skolemFOFtoCNF_T \/ % 0.11/0.44 ~in_environment $_63 (start_time skolemFOFtoCNF_E) \/ % 0.11/0.44 in_environment $_63 (appear an_organisation skolemFOFtoCNF_E) % 0.11/0.44 |- ~greater (cardinality_at_time $_67 skolemFOFtoCNF_T) zero \/ % 0.11/0.44 ~subpopulation $_67 skolemFOFtoCNF_E skolemFOFtoCNF_T \/ % 0.11/0.44 selection_favors $_67 efficient_producers skolemFOFtoCNF_T % 0.11/0.44 |- ~(cardinality_at_time $_68 skolemFOFtoCNF_T = zero) \/ % 0.11/0.44 ~environment $_66 \/ ~subpopulation $_68 $_66 skolemFOFtoCNF_T \/ % 0.11/0.44 ~subpopulation efficient_producers $_66 skolemFOFtoCNF_T \/ % 0.11/0.44 selection_favors efficient_producers $_68 skolemFOFtoCNF_T % 0.11/0.44 |- ~(cardinality_at_time $_74 skolemFOFtoCNF_T = zero) \/ % 0.11/0.44 ~subpopulation $_74 skolemFOFtoCNF_E skolemFOFtoCNF_T \/ % 0.11/0.44 selection_favors efficient_producers $_74 skolemFOFtoCNF_T % 0.11/0.44 |- selection_favors efficient_producers efficient_producers % 0.11/0.44 skolemFOFtoCNF_T % 0.11/0.44 |- ~(cardinality_at_time first_movers skolemFOFtoCNF_T = zero) \/ % 0.11/0.44 selection_favors efficient_producers first_movers skolemFOFtoCNF_T % 0.11/0.44 |- skolemFOFtoCNF_X skolemFOFtoCNF_E skolemFOFtoCNF_T = efficient_producers % 0.11/0.44 |- ~(cardinality_at_time first_movers skolemFOFtoCNF_T = zero) \/ % 0.11/0.44 selection_favors first_movers first_movers skolemFOFtoCNF_T % 0.11/0.44 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.11/0.44 %------------------------------------------------------------------------------