%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : MGT033-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n028.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 : Satisfiable 0.13s 0.41s % Output : Saturation 0.13s % 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.4.0. % 0.00/0.04 % Command : metis --show proof --show saturation %s % 0.09/0.35 % Computer : n028.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:26:31 UTC 2026 % 0.09/0.35 % CPUTime : % 0.09/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.13/0.41 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.13/0.41 % 0.13/0.41 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.13/0.41 |- ~(cardinality_at_time $D $C = zero) \/ ~environment $A \/ % 0.13/0.41 ~greater (cardinality_at_time $B $C) zero \/ ~subpopulation $B $A $C \/ % 0.13/0.41 ~subpopulation $D $A $C \/ selection_favors $B $D $C % 0.13/0.41 |- ~environment $A \/ ~greater (appear $C $A) $B \/ % 0.13/0.41 ~in_environment $A $B \/ cardinality_at_time $C $B = zero % 0.13/0.41 |- ~environment $A \/ ~greater (number_of_organizations $A $B) zero \/ % 0.13/0.41 subpopulation (sk1 $B $A) $A $B % 0.13/0.41 |- ~environment $A \/ ~greater (number_of_organizations $A $B) zero \/ % 0.13/0.41 greater (cardinality_at_time (sk1 $B $A) $B) zero % 0.13/0.41 |- ~(cardinality_at_time $A t = zero) \/ % 0.13/0.41 ~greater (cardinality_at_time $A $B) zero % 0.13/0.41 |- ~environment $A \/ ~greater (number_of_organizations $A $B) zero \/ % 0.13/0.41 in_environment $A $B % 0.13/0.41 |- ~environment $A \/ ~greater_or_equal $C $D \/ ~greater_or_equal $D $B \/ % 0.13/0.41 ~in_environment $A $B \/ ~in_environment $A $C \/ in_environment $A $D % 0.13/0.41 |- ~environment $A \/ in_environment $A (start_time $A) % 0.13/0.41 |- ~environment $A \/ % 0.13/0.41 greater_or_equal (appear first_movers $A) (start_time $A) % 0.13/0.41 |- ~environment $A \/ ~in_environment $A $B \/ % 0.13/0.41 subpopulation first_movers $A $B % 0.13/0.41 |- ~environment $A \/ ~in_environment $A $B \/ % 0.13/0.41 subpopulation efficient_producers $A $B % 0.13/0.41 |- ~environment $A \/ ~in_environment $A (appear first_movers $A) \/ % 0.13/0.41 in_environment $A (appear an_organisation $A) % 0.13/0.41 |- ~environment $A \/ ~greater_or_equal $B (appear an_organisation $A) \/ % 0.13/0.41 ~in_environment $A $B \/ greater (number_of_organizations $A $B) zero % 0.13/0.41 |- ~environment $A \/ ~greater (cardinality_at_time $B $C) zero \/ % 0.13/0.41 ~subpopulation $B $A $C \/ $B = efficient_producers \/ $B = first_movers % 0.13/0.41 |- ~environment $A \/ ~in_environment $A (appear an_organisation $A) \/ % 0.13/0.41 appear an_organisation $A = appear first_movers $A % 0.13/0.41 |- ~(cardinality_at_time $D $C = zero) \/ ~environment $A \/ % 0.13/0.41 ~greater zero zero \/ ~subpopulation $D $A $C \/ % 0.13/0.41 selection_favors $D $D $C % 0.13/0.41 |- ~environment $A \/ ~greater_or_equal $C $D \/ ~greater_or_equal $D $C \/ % 0.13/0.41 ~in_environment $A $C \/ in_environment $A $D % 0.13/0.41 |- environment sk2 % 0.13/0.41 |- in_environment sk2 sk3 % 0.13/0.41 |- greater_or_equal sk3 (appear an_organisation sk2) % 0.13/0.41 |- greater (appear efficient_producers sk2) sk3 % 0.13/0.41 |- ~selection_favors first_movers efficient_producers sk3 % 0.13/0.41 |- in_environment sk2 (start_time sk2) % 0.13/0.41 |- greater_or_equal (appear an_organisation sk2) (start_time sk2) % 0.13/0.41 |- subpopulation first_movers sk2 sk3 % 0.13/0.41 |- subpopulation first_movers sk2 (start_time sk2) % 0.13/0.41 |- subpopulation efficient_producers sk2 sk3 % 0.13/0.41 |- subpopulation efficient_producers sk2 (start_time sk2) % 0.13/0.41 |- cardinality_at_time efficient_producers sk3 = zero % 0.13/0.41 |- ~environment $_21 \/ % 0.13/0.41 ~greater_or_equal (start_time sk2) (appear an_organisation sk2) \/ % 0.13/0.41 ~in_environment $_21 (start_time sk2) \/ % 0.13/0.41 in_environment $_21 (appear an_organisation sk2) % 0.13/0.41 |- ~greater_or_equal $_23 sk3 \/ ~greater_or_equal sk3 $_23 \/ % 0.13/0.41 in_environment sk2 $_23 % 0.13/0.41 |- ~greater_or_equal $_23 (start_time sk2) \/ % 0.13/0.41 ~greater_or_equal (start_time sk2) $_23 \/ in_environment sk2 $_23 % 0.13/0.41 |- ~(cardinality_at_time efficient_producers (start_time sk2) = zero) \/ % 0.13/0.41 ~greater zero zero \/ % 0.13/0.41 selection_favors efficient_producers efficient_producers % 0.13/0.41 (start_time sk2) % 0.13/0.41 |- ~(cardinality_at_time first_movers (start_time sk2) = zero) \/ % 0.13/0.41 ~greater zero zero \/ % 0.13/0.41 selection_favors first_movers first_movers (start_time sk2) % 0.13/0.41 |- ~environment $_34 \/ ~greater_or_equal (start_time sk2) $_35 \/ % 0.13/0.41 ~in_environment $_34 $_35 \/ % 0.13/0.41 ~in_environment $_34 (appear an_organisation sk2) \/ % 0.13/0.41 in_environment $_34 (start_time sk2) % 0.13/0.41 |- ~environment $_34 \/ % 0.13/0.41 ~greater_or_equal $_36 (appear an_organisation sk2) \/ % 0.13/0.41 ~in_environment $_34 $_36 \/ ~in_environment $_34 (start_time sk2) \/ % 0.13/0.41 in_environment $_34 (appear an_organisation sk2) % 0.13/0.41 |- ~greater_or_equal $_36 $_37 \/ ~greater_or_equal $_37 sk3 \/ % 0.13/0.41 ~in_environment sk2 $_36 \/ in_environment sk2 $_37 % 0.13/0.41 |- ~greater_or_equal $_36 $_37 \/ % 0.13/0.41 ~greater_or_equal $_37 (start_time sk2) \/ ~in_environment sk2 $_36 \/ % 0.13/0.41 in_environment sk2 $_37 % 0.13/0.41 |- ~greater_or_equal $_37 $_35 \/ ~greater_or_equal sk3 $_37 \/ % 0.13/0.41 ~in_environment sk2 $_35 \/ in_environment sk2 $_37 % 0.13/0.41 |- ~greater_or_equal $_37 $_35 \/ % 0.13/0.41 ~greater_or_equal (start_time sk2) $_37 \/ ~in_environment sk2 $_35 \/ % 0.13/0.41 in_environment sk2 $_37 % 0.13/0.41 |- ~greater_or_equal $_39 sk3 \/ ~greater_or_equal (start_time sk2) $_39 \/ % 0.13/0.41 in_environment sk2 $_39 % 0.13/0.41 |- ~greater_or_equal $_42 (start_time sk2) \/ ~greater_or_equal sk3 $_42 \/ % 0.13/0.41 in_environment sk2 $_42 % 0.13/0.41 |- ~greater_or_equal $D $B \/ % 0.13/0.41 ~greater_or_equal (appear an_organisation sk2) $D \/ % 0.13/0.41 ~in_environment sk2 $B \/ in_environment sk2 $D % 0.13/0.41 |- ~greater_or_equal $C $D \/ % 0.13/0.41 ~greater_or_equal $D (appear an_organisation sk2) \/ % 0.13/0.41 ~in_environment sk2 $C \/ in_environment sk2 $D % 0.13/0.41 |- ~greater_or_equal $D (appear an_organisation sk2) \/ % 0.13/0.41 ~greater_or_equal (appear an_organisation sk2) $D \/ % 0.13/0.41 in_environment sk2 $D % 0.13/0.41 |- subpopulation efficient_producers sk2 (appear an_organisation sk2) % 0.13/0.41 |- subpopulation first_movers sk2 (appear an_organisation sk2) % 0.13/0.41 |- in_environment sk2 (appear an_organisation sk2) % 0.13/0.41 |- ~greater_or_equal $_37 (appear an_organisation sk2) \/ % 0.13/0.41 ~greater_or_equal sk3 $_37 \/ in_environment sk2 $_37 % 0.13/0.41 |- ~greater_or_equal $_37 sk3 \/ % 0.13/0.41 ~greater_or_equal (appear an_organisation sk2) $_37 \/ % 0.13/0.41 in_environment sk2 $_37 % 0.13/0.41 |- appear an_organisation sk2 = appear first_movers sk2 % 0.13/0.41 |- ~greater (appear an_organisation sk2) $B \/ ~in_environment sk2 $B \/ % 0.13/0.41 cardinality_at_time first_movers $B = zero % 0.13/0.41 |- ~(cardinality_at_time efficient_producers (appear an_organisation sk2) = % 0.13/0.41 zero) \/ ~greater zero zero \/ % 0.13/0.41 selection_favors efficient_producers efficient_producers % 0.13/0.41 (appear an_organisation sk2) % 0.13/0.41 |- ~(cardinality_at_time first_movers (appear an_organisation sk2) = % 0.13/0.41 zero) \/ ~greater zero zero \/ % 0.13/0.41 selection_favors first_movers first_movers (appear an_organisation sk2) % 0.13/0.41 |- greater (number_of_organizations sk2 sk3) zero % 0.13/0.41 |- greater zero zero % 0.13/0.41 |- ~(cardinality_at_time efficient_producers t = zero) % 0.13/0.41 |- ~greater_or_equal $_48 (start_time sk2) \/ % 0.13/0.41 ~greater_or_equal (appear an_organisation sk2) $_48 \/ % 0.13/0.41 in_environment sk2 $_48 % 0.13/0.41 |- ~greater_or_equal $_51 (appear an_organisation sk2) \/ % 0.13/0.41 ~greater_or_equal (start_time sk2) $_51 \/ in_environment sk2 $_51 % 0.13/0.41 |- ~environment $_34 \/ % 0.13/0.41 ~greater_or_equal (start_time sk2) (appear an_organisation sk2) \/ % 0.13/0.41 ~in_environment $_34 (appear an_organisation sk2) \/ % 0.13/0.41 in_environment $_34 (start_time sk2) % 0.13/0.41 |- ~environment $_60 \/ ~in_environment $_60 sk3 \/ % 0.13/0.41 ~in_environment $_60 (start_time sk2) \/ % 0.13/0.41 in_environment $_60 (appear an_organisation sk2) % 0.13/0.41 |- ~greater (cardinality_at_time $_67 sk3) zero \/ % 0.13/0.41 ~subpopulation $_67 sk2 sk3 \/ % 0.13/0.41 selection_favors $_67 efficient_producers sk3 % 0.13/0.41 |- ~(cardinality_at_time $_69 sk3 = zero) \/ ~environment $_66 \/ % 0.13/0.41 ~subpopulation $_69 $_66 sk3 \/ % 0.13/0.41 ~subpopulation efficient_producers $_66 sk3 \/ % 0.13/0.41 selection_favors efficient_producers $_69 sk3 % 0.13/0.41 |- ~(cardinality_at_time $_74 sk3 = zero) \/ ~subpopulation $_74 sk2 sk3 \/ % 0.13/0.41 selection_favors efficient_producers $_74 sk3 % 0.13/0.41 |- selection_favors efficient_producers efficient_producers sk3 % 0.13/0.41 |- ~(cardinality_at_time first_movers sk3 = zero) \/ % 0.13/0.41 selection_favors efficient_producers first_movers sk3 % 0.13/0.41 |- sk1 sk3 sk2 = efficient_producers % 0.13/0.41 |- ~(cardinality_at_time first_movers sk3 = zero) \/ % 0.13/0.41 selection_favors first_movers first_movers sk3 % 0.13/0.41 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.13/0.41 %------------------------------------------------------------------------------