%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : MGT038-10 : TPTP v9.3.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n004.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:16:07 AM UTC 2026 % Result : Satisfiable 0.13s 0.44s % Output : Saturation 0.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT038-10 : TPTP v9.3.0. Released v7.5.0. % 0.00/0.04 % Command : metis --show proof --show saturation %s % 0.10/0.35 % Computer : n004.cluster.edu % 0.10/0.35 % Model : x86_64 x86_64 % 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.35 % Memory : 8046.5625MB % 0.10/0.35 % OS : Linux 6.8.0-71-generic % 0.10/0.35 % CPULimit : 300 % 0.10/0.35 % WCLimit : 300 % 0.10/0.35 % DateTime : Mon Sep 7 12:45:45 UTC 2026 % 0.10/0.35 % CPUTime : % 0.10/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.13/0.44 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.13/0.44 % 0.13/0.44 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.13/0.44 |- ifeq2 $A $A $B $C = $B % 0.13/0.44 |- ifeq $A $A $B $C = $B % 0.13/0.44 |- finite_set first_movers = true % 0.13/0.44 |- ifeq (environment $A) true % 0.13/0.44 (ifeq (stable $A) true (in_environment $A (appear first_movers $A)) % 0.13/0.44 true) true = true % 0.13/0.44 |- ifeq (finite_set $A) true % 0.13/0.44 (ifeq (contracts_from $B $A) true (greater (sk1 $B $A) $B) true) % 0.13/0.44 true = true % 0.13/0.44 |- ifeq2 (finite_set $A) true (ifeq2 (contracts_from $B $A) true zero zero) % 0.13/0.44 zero = zero % 0.13/0.44 |- ifeq (greater $C $B) true % 0.13/0.44 (ifeq (in_environment $A $B) true % 0.13/0.44 (ifeq (environment $A) true % 0.13/0.44 (ifeq (stable $A) true (in_environment $A $C) true) true) true) % 0.13/0.44 true = true % 0.13/0.44 |- ifeq (greater $B $C) true % 0.13/0.44 (ifeq (greater $A $B) true (greater $A $C) true) true = true % 0.13/0.44 |- ifeq (environment $A) true % 0.13/0.44 (ifeq (stable $A) true % 0.13/0.44 (greater (sk2 $A) (appear efficient_producers $A)) true) true = % 0.13/0.44 true % 0.13/0.44 |- ifeq (environment $A) true % 0.13/0.44 (ifeq (stable $A) true (contracts_from (sk2 $A) first_movers) true) % 0.13/0.44 true = true % 0.13/0.44 |- ifeq (environment $A) true % 0.13/0.44 (greater (appear efficient_producers e) (appear first_movers $A)) % 0.13/0.44 true = true % 0.13/0.44 |- environment sk3 = true % 0.13/0.44 |- stable sk3 = true % 0.13/0.44 |- ~(tuple (cardinality_at_time first_movers to) (in_environment sk3 $A) % 0.13/0.44 (greater $A (appear first_movers sk3)) = tuple zero true true) % 0.13/0.44 |- greater (appear efficient_producers e) (appear first_movers sk3) = true % 0.13/0.44 |- contracts_from (sk2 sk3) first_movers = true % 0.13/0.44 |- in_environment sk3 (appear first_movers sk3) = true % 0.13/0.44 |- greater (sk2 sk3) (appear efficient_producers sk3) = true % 0.13/0.44 |- greater (sk1 (sk2 sk3) first_movers) (sk2 sk3) = true % 0.13/0.44 |- ifeq (contracts_from $_11 first_movers) true % 0.13/0.44 (greater (sk1 $_11 first_movers) $_11) true = true % 0.13/0.44 |- cardinality_at_time s t2 = zero % 0.13/0.44 |- ifeq2 (contracts_from $_14 first_movers) true zero zero = zero % 0.13/0.44 |- ~(tuple (cardinality_at_time first_movers to) true true = % 0.13/0.44 tuple zero true true) % 0.13/0.44 |- ~(tuple (cardinality_at_time first_movers to) true % 0.13/0.44 (greater (appear first_movers sk3) (appear first_movers sk3)) = % 0.13/0.44 tuple zero true true) % 0.13/0.44 |- ifeq (greater $_20 (appear first_movers sk3)) true % 0.13/0.44 (ifeq (greater (appear efficient_producers e) $_20) true true true) % 0.13/0.44 true = true % 0.13/0.44 |- ifeq (greater $_20 (sk2 sk3)) true % 0.13/0.44 (ifeq (greater (sk1 (sk2 sk3) first_movers) $_20) true true true) % 0.13/0.44 true = true % 0.13/0.44 |- ifeq (greater $_20 (appear efficient_producers sk3)) true % 0.13/0.44 (ifeq (greater (sk2 sk3) $_20) true true true) true = true % 0.13/0.44 |- ifeq (greater (appear first_movers sk3) $_21) true % 0.13/0.44 (greater (appear efficient_producers e) $_21) true = true % 0.13/0.44 |- ifeq (greater (sk2 sk3) $_21) true % 0.13/0.44 (greater (sk1 (sk2 sk3) first_movers) $_21) true = true % 0.13/0.44 |- ifeq (greater (appear efficient_producers sk3) $_21) true % 0.13/0.44 (greater (sk2 sk3) $_21) true = true % 0.13/0.44 |- ifeq (greater $_19 (appear efficient_producers e)) true % 0.13/0.44 (greater $_19 (appear first_movers sk3)) true = true % 0.13/0.44 |- ifeq (greater $_19 (sk1 (sk2 sk3) first_movers)) true % 0.13/0.44 (greater $_19 (sk2 sk3)) true = true % 0.13/0.44 |- ifeq (greater $_19 (sk2 sk3)) true % 0.13/0.44 (greater $_19 (appear efficient_producers sk3)) true = true % 0.13/0.44 |- ifeq % 0.13/0.44 (greater (appear efficient_producers sk3) % 0.13/0.44 (appear efficient_producers sk3)) true true true = true % 0.13/0.44 |- ifeq (greater (sk2 sk3) (sk2 sk3)) true true true = true % 0.13/0.45 |- greater (sk1 (sk2 sk3) first_movers) (appear efficient_producers sk3) = % 0.13/0.45 true % 0.13/0.45 |- ifeq (greater $A (sk1 (sk2 sk3) first_movers)) true % 0.13/0.45 (greater $A (appear efficient_producers sk3)) true = true % 0.13/0.45 |- ifeq (greater (appear efficient_producers sk3) $C) true % 0.13/0.45 (greater (sk1 (sk2 sk3) first_movers) $C) true = true % 0.13/0.45 |- ifeq (greater $B (appear efficient_producers sk3)) true % 0.13/0.45 (ifeq (greater (sk1 (sk2 sk3) first_movers) $B) true true true) true = % 0.13/0.45 true % 0.13/0.45 |- ifeq (greater (appear first_movers sk3) (appear first_movers sk3)) true % 0.13/0.45 true true = true % 0.13/0.45 |- ifeq % 0.13/0.45 (greater (appear efficient_producers e) % 0.13/0.45 (appear efficient_producers e)) true true true = true % 0.13/0.45 |- ifeq (greater (sk1 (sk2 sk3) first_movers) (sk1 (sk2 sk3) first_movers)) % 0.13/0.45 true true true = true % 0.13/0.45 |- ifeq (greater (sk2 sk3) (sk1 (sk2 sk3) first_movers)) true true true = % 0.13/0.45 true % 0.13/0.45 |- ifeq (greater (appear efficient_producers sk3) (sk2 sk3)) true true % 0.13/0.45 true = true % 0.13/0.45 |- ifeq (greater $_36 $_35) true % 0.13/0.45 (ifeq (in_environment sk3 $_35) true (in_environment sk3 $_36) true) % 0.13/0.45 true = true % 0.13/0.45 |- ifeq (greater (appear first_movers $_34) $_35) true % 0.13/0.45 (ifeq (in_environment $_34 $_35) true true true) true = true % 0.13/0.45 |- ifeq (greater $_36 (appear first_movers sk3)) true % 0.13/0.45 (in_environment sk3 $_36) true = true % 0.13/0.45 |- ifeq (in_environment $_34 (appear first_movers sk3)) true % 0.13/0.45 (ifeq (environment $_34) true % 0.13/0.45 (ifeq (stable $_34) true % 0.13/0.45 (in_environment $_34 (appear efficient_producers e)) true) true) % 0.13/0.45 true = true % 0.13/0.45 |- ifeq (in_environment $_34 (appear efficient_producers sk3)) true % 0.13/0.45 (ifeq (environment $_34) true % 0.13/0.45 (ifeq (stable $_34) true % 0.13/0.45 (in_environment $_34 (sk1 (sk2 sk3) first_movers)) true) true) % 0.13/0.45 true = true % 0.13/0.45 |- ifeq (in_environment $_34 (sk2 sk3)) true % 0.13/0.45 (ifeq (environment $_34) true % 0.13/0.45 (ifeq (stable $_34) true % 0.13/0.45 (in_environment $_34 (sk1 (sk2 sk3) first_movers)) true) true) % 0.13/0.45 true = true % 0.13/0.45 |- ifeq (in_environment $_34 (appear efficient_producers sk3)) true % 0.13/0.45 (ifeq (environment $_34) true % 0.13/0.45 (ifeq (stable $_34) true (in_environment $_34 (sk2 sk3)) true) % 0.13/0.45 true) true = true % 0.13/0.45 |- in_environment sk3 (appear efficient_producers e) = true % 0.13/0.45 |- ifeq (greater $C (appear efficient_producers e)) true % 0.13/0.45 (in_environment sk3 $C) true = true % 0.13/0.45 |- ifeq (greater (appear efficient_producers e) $B) true % 0.13/0.45 (ifeq (in_environment sk3 $B) true true true) true = true % 0.13/0.45 |- ifeq (greater (appear first_movers sk3) (appear efficient_producers e)) % 0.13/0.45 true true true = true % 0.13/0.45 |- ifeq (in_environment sk3 (appear efficient_producers sk3)) true % 0.13/0.45 (in_environment sk3 (sk2 sk3)) true = true % 0.13/0.45 |- ifeq (in_environment sk3 (sk2 sk3)) true % 0.13/0.45 (in_environment sk3 (sk1 (sk2 sk3) first_movers)) true = true % 0.13/0.45 |- ifeq (in_environment sk3 (appear efficient_producers sk3)) true % 0.13/0.45 (in_environment sk3 (sk1 (sk2 sk3) first_movers)) true = true % 0.13/0.45 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.13/0.45 %------------------------------------------------------------------------------