↑ Up

Metis---2.4.CSA-Sat.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : MGT037+2 : TPTP v9.3.0. Released v2.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n014.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   : CounterSatisfiable 0.14s 0.40s
% Output   : Saturation 0.14s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : MGT037+2 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04  % Command  : metis --show proof --show saturation %s
% 0.09/0.36  % Computer : n014.cluster.edu
% 0.09/0.36  % Model    : x86_64 x86_64
% 0.09/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36  % Memory   : 8046.5625MB
% 0.09/0.36  % OS       : Linux 6.8.0-71-generic
% 0.09/0.36  % CPULimit : 300
% 0.09/0.36  % WCLimit  : 300
% 0.09/0.36  % DateTime : Mon Sep  7 12:44:26 UTC 2026
% 0.09/0.36  % CPUTime  : 
% 0.09/0.37  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.14/0.40  % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.40  
% 0.14/0.40  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.40  |- ~(cardinality_at_time efficient_producers $T = zero) \/
% 0.14/0.40     ~environment $E \/
% 0.14/0.40     ~greater_or_equal $T (appear efficient_producers $E) \/
% 0.14/0.40     greater $T (skolemFOFtoCNF_To $E $T)
% 0.14/0.40  |- ~(cardinality_at_time efficient_producers $T = zero) \/
% 0.14/0.40     ~environment $E \/
% 0.14/0.40     ~greater_or_equal $T (appear efficient_producers $E) \/
% 0.14/0.40     greater (skolemFOFtoCNF_To $E $T) (appear efficient_producers $E)
% 0.14/0.40  |- ~(cardinality_at_time efficient_producers $T = zero) \/
% 0.14/0.40     ~environment $E \/
% 0.14/0.40     ~greater_or_equal $T (appear efficient_producers $E) \/
% 0.14/0.40     greater zero (growth_rate efficient_producers (skolemFOFtoCNF_To $E $T))
% 0.14/0.40  |- ~(cardinality_at_time efficient_producers $T = zero) \/
% 0.14/0.40     ~environment $E \/
% 0.14/0.40     ~greater_or_equal $T (appear efficient_producers $E) \/
% 0.14/0.40     in_environment $E (skolemFOFtoCNF_To $E $T)
% 0.14/0.40  |- ~environment $E \/ ~greater (appear an_organisation $E) $T \/
% 0.14/0.40     ~in_environment $E $T \/ number_of_organizations $E $T = zero
% 0.14/0.40  |- ~environment $E \/
% 0.14/0.40     ~greater zero (growth_rate (skolemFOFtoCNF_X $E $T) $T) \/
% 0.14/0.40     ~in_environment $E $T \/ decreases (number_of_organizations $E $T)
% 0.14/0.40  |- ~environment $E \/ ~in_environment $E $T \/
% 0.14/0.40     decreases (number_of_organizations $E $T) \/
% 0.14/0.40     greater (cardinality_at_time (skolemFOFtoCNF_X $E $T) $T) zero
% 0.14/0.40  |- ~environment $E \/ ~in_environment $E $T \/
% 0.14/0.40     decreases (number_of_organizations $E $T) \/
% 0.14/0.40     subpopulation (skolemFOFtoCNF_X $E $T) $E $T
% 0.14/0.40  |- ~(number_of_organizations $E $T = zero) \/ ~environment $E \/
% 0.14/0.40     ~in_environment $E $T \/ ~subpopulation $X $E $T \/
% 0.14/0.40     cardinality_at_time $X $T = zero
% 0.14/0.40  |- ~environment $E \/ ~in_environment $E $T \/
% 0.14/0.40     subpopulation efficient_producers $E $T
% 0.14/0.40  |- ~environment $E \/ ~in_environment $E $T \/
% 0.14/0.40     subpopulation first_movers $E $T
% 0.14/0.40  |- ~(cardinality_at_time $S $T = zero) \/ ~greater zero (growth_rate $S $T)
% 0.14/0.40  |- ~environment $E \/ ~in_environment $E $T \/
% 0.14/0.40     cardinality_at_time efficient_producers $T = zero \/
% 0.14/0.40     greater (cardinality_at_time efficient_producers $T) zero
% 0.14/0.40  |- ~constant $X \/ ~decreases $X
% 0.14/0.40  |- ~environment $E \/ ~greater_or_equal $T (appear an_organisation $E) \/
% 0.14/0.40     ~in_environment $E $T \/ greater (appear an_organisation $E) $T
% 0.14/0.40  |- ~environment $E \/ ~greater_or_equal $T (appear an_organisation $E) \/
% 0.14/0.40     ~in_environment $E $T \/ greater (number_of_organizations $E $T) zero
% 0.14/0.40  |- greater (resilience efficient_producers) (resilience first_movers)
% 0.14/0.40  |- ~environment $E \/ ~greater (equilibrium $E) $T \/
% 0.14/0.40     ~greater (number_of_organizations $E $T) zero \/
% 0.14/0.40     ~in_environment $E $T \/ decreases (resources $E $T)
% 0.14/0.40  |- ~environment $E \/ ~greater (number_of_organizations $E $T) zero \/
% 0.14/0.40     ~in_environment $E $T \/ constant (resources $E $T) \/
% 0.14/0.40     greater (equilibrium $E) $T
% 0.14/0.40  |- ~constant (resources $E $T) \/ ~environment $E \/
% 0.14/0.40     ~in_environment $E $T \/ constant (number_of_organizations $E $T)
% 0.14/0.40  |- ~decreases (number_of_organizations $E $T) \/
% 0.14/0.40     ~decreases (resources $E $T) \/ ~environment $E \/ ~in_environment $E $T
% 0.14/0.40  |- ~environment $E \/ ~greater (cardinality_at_time $X $T) zero \/
% 0.14/0.40     ~subpopulation $X $E $T \/ $X = efficient_producers \/ $X = first_movers
% 0.14/0.40  |- ~environment $E \/ ~greater (resilience $S2) (resilience $S1) \/
% 0.14/0.40     ~greater zero (growth_rate $S2 $T) \/ ~in_environment $E $T \/
% 0.14/0.40     greater zero (growth_rate $S1 $T)
% 0.14/0.40  |- ~greater zero zero
% 0.14/0.40  |- environment skolemFOFtoCNF_E
% 0.14/0.40  |- greater_or_equal skolemFOFtoCNF_T
% 0.14/0.40       (appear efficient_producers skolemFOFtoCNF_E)
% 0.14/0.40  |- in_environment skolemFOFtoCNF_E skolemFOFtoCNF_T
% 0.14/0.40  |- subpopulation efficient_producers skolemFOFtoCNF_E skolemFOFtoCNF_T
% 0.14/0.40  |- subpopulation first_movers skolemFOFtoCNF_E skolemFOFtoCNF_T
% 0.14/0.40  |- decreases (number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T) \/
% 0.14/0.40     subpopulation (skolemFOFtoCNF_X skolemFOFtoCNF_E skolemFOFtoCNF_T)
% 0.14/0.40       skolemFOFtoCNF_E skolemFOFtoCNF_T
% 0.14/0.40  |- cardinality_at_time efficient_producers skolemFOFtoCNF_T = zero
% 0.14/0.40  |- decreases (number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T) \/
% 0.14/0.40     greater
% 0.14/0.40       (cardinality_at_time
% 0.14/0.40          (skolemFOFtoCNF_X skolemFOFtoCNF_E skolemFOFtoCNF_T)
% 0.14/0.40          skolemFOFtoCNF_T) zero
% 0.14/0.40  |- greater skolemFOFtoCNF_T
% 0.14/0.40       (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T)
% 0.14/0.40  |- in_environment skolemFOFtoCNF_E
% 0.14/0.40       (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T)
% 0.14/0.40  |- decreases
% 0.14/0.40       (number_of_organizations skolemFOFtoCNF_E
% 0.14/0.40          (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T)) \/
% 0.14/0.40     greater
% 0.14/0.40       (cardinality_at_time
% 0.14/0.40          (skolemFOFtoCNF_X skolemFOFtoCNF_E
% 0.14/0.40             (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T))
% 0.14/0.40          (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T)) zero
% 0.14/0.40  |- cardinality_at_time efficient_producers
% 0.14/0.40       (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T) = zero \/
% 0.14/0.40     greater
% 0.14/0.40       (cardinality_at_time efficient_producers
% 0.14/0.40          (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T)) zero
% 0.14/0.40  |- decreases
% 0.14/0.40       (number_of_organizations skolemFOFtoCNF_E
% 0.14/0.40          (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T)) \/
% 0.14/0.40     subpopulation
% 0.14/0.40       (skolemFOFtoCNF_X skolemFOFtoCNF_E
% 0.14/0.40          (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T))
% 0.14/0.40       skolemFOFtoCNF_E (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T)
% 0.14/0.40  |- subpopulation first_movers skolemFOFtoCNF_E
% 0.14/0.40       (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T)
% 0.14/0.40  |- subpopulation efficient_producers skolemFOFtoCNF_E
% 0.14/0.40       (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T)
% 0.14/0.40  |- greater (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T)
% 0.14/0.40       (appear efficient_producers skolemFOFtoCNF_E)
% 0.14/0.40  |- greater zero
% 0.14/0.40       (growth_rate efficient_producers
% 0.14/0.40          (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T))
% 0.14/0.40  |- ~(cardinality_at_time efficient_producers
% 0.14/0.40         (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T) = zero)
% 0.14/0.40  |- skolemFOFtoCNF_X skolemFOFtoCNF_E skolemFOFtoCNF_T =
% 0.14/0.40     efficient_producers \/
% 0.14/0.40     skolemFOFtoCNF_X skolemFOFtoCNF_E skolemFOFtoCNF_T = first_movers \/
% 0.14/0.40     decreases (number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T)
% 0.14/0.40  |- ~constant (number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T) \/
% 0.14/0.40     skolemFOFtoCNF_X skolemFOFtoCNF_E skolemFOFtoCNF_T =
% 0.14/0.40     efficient_producers \/
% 0.14/0.40     skolemFOFtoCNF_X skolemFOFtoCNF_E skolemFOFtoCNF_T = first_movers
% 0.14/0.40  |- ~(number_of_organizations skolemFOFtoCNF_E
% 0.14/0.40         (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T) = zero)
% 0.14/0.41  |- ~(number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T = zero) \/
% 0.14/0.41     cardinality_at_time first_movers skolemFOFtoCNF_T = zero
% 0.14/0.41  |- ~(number_of_organizations skolemFOFtoCNF_E skolemFOFtoCNF_T = zero) \/
% 0.14/0.41     cardinality_at_time (skolemFOFtoCNF_X skolemFOFtoCNF_E skolemFOFtoCNF_T)
% 0.14/0.41       skolemFOFtoCNF_T = zero \/ decreases zero
% 0.14/0.41  |- skolemFOFtoCNF_X skolemFOFtoCNF_E
% 0.14/0.41       (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T) =
% 0.14/0.41     efficient_producers \/
% 0.14/0.41     skolemFOFtoCNF_X skolemFOFtoCNF_E
% 0.14/0.41       (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T) =
% 0.14/0.41     first_movers \/
% 0.14/0.41     decreases
% 0.14/0.41       (number_of_organizations skolemFOFtoCNF_E
% 0.14/0.41          (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T))
% 0.14/0.41  |- ~constant
% 0.14/0.41        (number_of_organizations skolemFOFtoCNF_E
% 0.14/0.41           (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T)) \/
% 0.14/0.41     skolemFOFtoCNF_X skolemFOFtoCNF_E
% 0.14/0.41       (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T) =
% 0.14/0.41     efficient_producers \/
% 0.14/0.41     skolemFOFtoCNF_X skolemFOFtoCNF_E
% 0.14/0.41       (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T) = first_movers
% 0.14/0.41  |- ~environment $_45 \/
% 0.14/0.41     ~greater zero (growth_rate efficient_producers $_48) \/
% 0.14/0.41     ~in_environment $_45 $_48 \/
% 0.14/0.41     greater zero (growth_rate first_movers $_48)
% 0.14/0.41  |- greater zero
% 0.14/0.41       (growth_rate first_movers
% 0.14/0.41          (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T))
% 0.14/0.41  |- ~(cardinality_at_time first_movers
% 0.14/0.41         (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T) = zero)
% 0.14/0.41  |- ~greater (resilience efficient_producers) (resilience $_53) \/
% 0.14/0.41     greater zero
% 0.14/0.41       (growth_rate $_53
% 0.14/0.41          (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T))
% 0.14/0.41  |- ~greater (resilience first_movers) (resilience $_56) \/
% 0.14/0.41     greater zero
% 0.14/0.41       (growth_rate $_56
% 0.14/0.41          (skolemFOFtoCNF_To skolemFOFtoCNF_E skolemFOFtoCNF_T))
% 0.14/0.41  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.41  
%------------------------------------------------------------------------------