%------------------------------------------------------------------------------
% File : Refute---2015
% Problem : MGT037+2 : TPTP v6.4.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : isabelle tptp_refute %d %s
% Computer : n075.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.75MB
% OS : Linux 3.10.0-327.10.1.el7.x86_64
% CPULimit : 300s
% DateTime : Tue Apr 12 17:35:07 EDT 2016
% Result : CounterSatisfiable 87.64s
% Output : Assurance 0s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT037+2 : TPTP v6.4.0. Released v2.0.0.
% 0.00/0.04 % Command : isabelle tptp_refute %d %s
% 0.02/0.24 % Computer : n075.star.cs.uiowa.edu
% 0.02/0.24 % Model : x86_64 x86_64
% 0.02/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.02/0.24 % Memory : 32218.75MB
% 0.02/0.24 % OS : Linux 3.10.0-327.10.1.el7.x86_64
% 0.02/0.24 % CPULimit : 300
% 0.02/0.24 % DateTime : Mon Apr 11 00:30:24 CDT 2016
% 0.02/0.24 % CPUTime :
% 6.30/5.87 > val it = (): unit
% 6.50/6.09 Trying to find a model that refutes: (bnd_environment E & bnd_in_environment E T) &
% 6.50/6.09 bnd_greater_or_equal T (bnd_appear bnd_efficient_producers E) -->
% 6.50/6.09 bnd_greater (bnd_cardinality_at_time bnd_efficient_producers T) bnd_zero
% 7.30/6.81 Unfolded term: [| ALL E S1 S2 T.
% 7.30/6.81 ((bnd_environment E & bnd_in_environment E T) &
% 7.30/6.81 ~ bnd_greater bnd_zero (bnd_growth_rate S1 T)) &
% 7.30/6.81 bnd_greater (bnd_resilience S2) (bnd_resilience S1) -->
% 7.30/6.81 ~ bnd_greater bnd_zero (bnd_growth_rate S2 T);
% 7.30/6.81 ALL E X T.
% 7.30/6.81 (bnd_environment E & bnd_subpopulation X E T) &
% 7.30/6.81 bnd_greater (bnd_cardinality_at_time X T) bnd_zero -->
% 7.30/6.81 X = bnd_efficient_producers | X = bnd_first_movers;
% 7.30/6.81 ALL E T.
% 7.30/6.81 bnd_environment E & bnd_in_environment E T -->
% 7.30/6.81 (bnd_decreases (bnd_resources E T) -->
% 7.30/6.81 ~ bnd_decreases (bnd_number_of_organizations E T)) &
% 7.30/6.81 (bnd_constant (bnd_resources E T) -->
% 7.30/6.81 bnd_constant (bnd_number_of_organizations E T));
% 7.30/6.81 ALL E T.
% 7.30/6.81 (bnd_environment E & bnd_in_environment E T) &
% 7.30/6.81 bnd_greater (bnd_number_of_organizations E T) bnd_zero -->
% 7.30/6.81 (bnd_greater (bnd_equilibrium E) T -->
% 7.30/6.81 bnd_decreases (bnd_resources E T)) &
% 7.30/6.81 (~ bnd_greater (bnd_equilibrium E) T -->
% 7.30/6.81 bnd_constant (bnd_resources E T));
% 7.30/6.81 bnd_greater (bnd_resilience bnd_efficient_producers)
% 7.30/6.81 (bnd_resilience bnd_first_movers);
% 7.30/6.81 ALL E T.
% 7.30/6.81 (bnd_environment E & bnd_in_environment E T) &
% 7.30/6.81 bnd_greater_or_equal T (bnd_appear bnd_an_organisation E) -->
% 7.30/6.81 bnd_greater (bnd_number_of_organizations E T) bnd_zero;
% 7.30/6.81 ALL E T.
% 7.30/6.81 bnd_environment E & bnd_in_environment E T -->
% 7.30/6.81 ~ bnd_greater_or_equal T (bnd_appear bnd_an_organisation E) |
% 7.30/6.81 bnd_greater (bnd_appear bnd_an_organisation E) T;
% 7.30/6.81 ALL X. bnd_constant X --> ~ bnd_decreases X;
% 7.30/6.81 ALL E T.
% 7.30/6.81 bnd_environment E & bnd_in_environment E T -->
% 7.30/6.81 bnd_cardinality_at_time bnd_efficient_producers T = bnd_zero |
% 7.30/6.81 bnd_greater (bnd_cardinality_at_time bnd_efficient_producers T)
% 7.30/6.81 bnd_zero;
% 7.30/6.81 ALL S T.
% 7.30/6.81 bnd_cardinality_at_time S T = bnd_zero -->
% 7.30/6.81 ~ bnd_greater bnd_zero (bnd_growth_rate S T);
% 7.30/6.81 ALL E T.
% 7.30/6.81 bnd_environment E & bnd_in_environment E T -->
% 7.30/6.81 bnd_subpopulation bnd_first_movers E T &
% 7.30/6.81 bnd_subpopulation bnd_efficient_producers E T;
% 7.30/6.81 ALL E T X.
% 7.30/6.81 ((bnd_environment E & bnd_in_environment E T) &
% 7.30/6.81 bnd_number_of_organizations E T = bnd_zero) &
% 7.30/6.81 bnd_subpopulation X E T -->
% 7.30/6.81 bnd_cardinality_at_time X T = bnd_zero;
% 7.30/6.81 ALL E T.
% 7.30/6.81 (bnd_environment E & bnd_in_environment E T) &
% 7.30/6.81 ~ bnd_decreases (bnd_number_of_organizations E T) -->
% 7.30/6.81 (EX X. (bnd_subpopulation X E T &
% 7.30/6.81 bnd_greater (bnd_cardinality_at_time X T) bnd_zero) &
% 7.30/6.81 ~ bnd_greater bnd_zero (bnd_growth_rate X T));
% 7.30/6.81 ALL E T.
% 7.30/6.81 (bnd_environment E & bnd_in_environment E T) &
% 7.30/6.81 bnd_greater (bnd_appear bnd_an_organisation E) T -->
% 7.30/6.81 bnd_number_of_organizations E T = bnd_zero;
% 7.30/6.81 ALL E T.
% 7.30/6.81 (bnd_environment E &
% 7.30/6.81 bnd_greater_or_equal T (bnd_appear bnd_efficient_producers E)) &
% 7.30/6.81 bnd_cardinality_at_time bnd_efficient_producers T = bnd_zero -->
% 7.30/6.81 (EX To.
% 7.30/6.81 ((bnd_greater To (bnd_appear bnd_efficient_producers E) &
% 7.30/6.81 bnd_in_environment E To) &
% 7.30/6.81 bnd_greater T To) &
% 7.30/6.81 bnd_greater bnd_zero
% 7.30/6.81 (bnd_growth_rate bnd_efficient_producers To)) |]
% 7.30/6.81 ==> (bnd_environment E & bnd_in_environment E T) &
% 7.30/6.81 bnd_greater_or_equal T (bnd_appear bnd_efficient_producers E) -->
% 7.30/6.81 bnd_greater (bnd_cardinality_at_time bnd_efficient_producers T) bnd_zero
% 7.30/6.81 Adding axioms...
% 7.30/6.82 Typedef.type_definition_def
% 10.81/10.38 ...done.
% 10.81/10.38 Ground types: ?'b, TPTP_Interpret.ind
% 10.81/10.38 Translating term (sizes: 1, 1) ...
% 13.11/12.61 Invoking SAT solver...
% 13.11/12.61 No model exists.
% 13.11/12.61 Translating term (sizes: 2, 1) ...
% 16.02/15.57 Invoking SAT solver...
% 16.02/15.57 No model exists.
% 16.02/15.57 Translating term (sizes: 1, 2) ...
% 26.23/25.78 Invoking SAT solver...
% 26.73/26.28 No model exists.
% 26.73/26.28 Translating term (sizes: 3, 1) ...
% 32.05/31.58 Invoking SAT solver...
% 32.05/31.58 No model exists.
% 32.05/31.58 Translating term (sizes: 2, 2) ...
% 50.00/49.49 Invoking SAT solver...
% 50.48/49.99 No model exists.
% 50.48/49.99 Translating term (sizes: 1, 3) ...
% 82.01/81.31 Invoking SAT solver...
% 87.64/86.94 Model found:
% 87.64/86.94 Size of types: ?'b: 1, TPTP_Interpret.ind: 3
% 87.64/86.94 T: ??.TPTP_Interpret.ind0
% 87.64/86.94 E: ??.TPTP_Interpret.ind2
% 87.64/86.94 bnd_an_organisation: ??.TPTP_Interpret.ind1
% 87.64/86.94 bnd_appear: {(??.TPTP_Interpret.ind0,
% 87.64/86.94 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 87.64/86.94 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.94 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind0)}),
% 87.64/86.94 (??.TPTP_Interpret.ind1,
% 87.64/86.94 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 87.64/86.94 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.94 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind1)}),
% 87.64/86.94 (??.TPTP_Interpret.ind2,
% 87.64/86.94 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 87.64/86.94 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.94 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind0)})}
% 87.64/86.94 bnd_greater_or_equal: {(??.TPTP_Interpret.ind0,
% 87.64/86.94 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False),
% 87.64/86.94 (??.TPTP_Interpret.ind2, False)}),
% 87.64/86.94 (??.TPTP_Interpret.ind1,
% 87.64/86.94 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 87.64/86.94 (??.TPTP_Interpret.ind2, False)}),
% 87.64/86.94 (??.TPTP_Interpret.ind2,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 87.64/86.95 (??.TPTP_Interpret.ind2, False)})}
% 87.64/86.95 bnd_equilibrium: {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind0)}
% 87.64/86.95 bnd_constant: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False),
% 87.64/86.95 (??.TPTP_Interpret.ind2, False)}
% 87.64/86.95 bnd_number_of_organizations: {(??.TPTP_Interpret.ind0,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind0)}),
% 87.64/86.95 (??.TPTP_Interpret.ind1,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind0)}),
% 87.64/86.95 (??.TPTP_Interpret.ind2,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind1),
% 87.64/86.95 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind1)})}
% 87.64/86.95 bnd_resources: {(??.TPTP_Interpret.ind0,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind0)}),
% 87.64/86.95 (??.TPTP_Interpret.ind1,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind0)}),
% 87.64/86.95 (??.TPTP_Interpret.ind2,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind2),
% 87.64/86.95 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind2)})}
% 87.64/86.95 bnd_decreases: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True),
% 87.64/86.95 (??.TPTP_Interpret.ind2, False)}
% 87.64/86.95 bnd_first_movers: ??.TPTP_Interpret.ind2
% 87.64/86.95 bnd_efficient_producers: ??.TPTP_Interpret.ind0
% 87.64/86.95 bnd_cardinality_at_time: {(??.TPTP_Interpret.ind0,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind2)}),
% 87.64/86.95 (??.TPTP_Interpret.ind1,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind1)}),
% 87.64/86.95 (??.TPTP_Interpret.ind2,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind1)})}
% 87.64/86.95 bnd_subpopulation: {(??.TPTP_Interpret.ind0,
% 87.64/86.95 {(??.TPTP_Interpret.ind0,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 87.64/86.95 (??.TPTP_Interpret.ind2, True)}),
% 87.64/86.95 (??.TPTP_Interpret.ind1,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 87.64/86.95 (??.TPTP_Interpret.ind2, True)}),
% 87.64/86.95 (??.TPTP_Interpret.ind2,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 87.64/86.95 (??.TPTP_Interpret.ind2, True)})}),
% 87.64/86.95 (??.TPTP_Interpret.ind1,
% 87.64/86.95 {(??.TPTP_Interpret.ind0,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 87.64/86.95 (??.TPTP_Interpret.ind2, True)}),
% 87.64/86.95 (??.TPTP_Interpret.ind1,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 87.64/86.95 (??.TPTP_Interpret.ind2, True)}),
% 87.64/86.95 (??.TPTP_Interpret.ind2,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 87.64/86.95 (??.TPTP_Interpret.ind2, True)})}),
% 87.64/86.95 (??.TPTP_Interpret.ind2,
% 87.64/86.95 {(??.TPTP_Interpret.ind0,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 87.64/86.95 (??.TPTP_Interpret.ind2, True)}),
% 87.64/86.95 (??.TPTP_Interpret.ind1,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 87.64/86.95 (??.TPTP_Interpret.ind2, True)}),
% 87.64/86.95 (??.TPTP_Interpret.ind2,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 87.64/86.95 (??.TPTP_Interpret.ind2, True)})})}
% 87.64/86.95 bnd_resilience: {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind2)}
% 87.64/86.95 bnd_growth_rate: {(??.TPTP_Interpret.ind0,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind2)}),
% 87.64/86.95 (??.TPTP_Interpret.ind1,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind2)}),
% 87.64/86.95 (??.TPTP_Interpret.ind2,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind1, ??.TPTP_Interpret.ind0),
% 87.64/86.95 (??.TPTP_Interpret.ind2, ??.TPTP_Interpret.ind2)})}
% 87.64/86.95 bnd_zero: ??.TPTP_Interpret.ind0
% 87.64/86.95 bnd_greater: {(??.TPTP_Interpret.ind0,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 87.64/86.95 (??.TPTP_Interpret.ind2, True)}),
% 87.64/86.95 (??.TPTP_Interpret.ind1,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 87.64/86.95 (??.TPTP_Interpret.ind2, False)}),
% 87.64/86.95 (??.TPTP_Interpret.ind2,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False),
% 87.64/86.95 (??.TPTP_Interpret.ind2, False)})}
% 87.64/86.95 bnd_in_environment: {(??.TPTP_Interpret.ind0,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 87.64/86.95 (??.TPTP_Interpret.ind2, False)}),
% 87.64/86.95 (??.TPTP_Interpret.ind1,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 87.64/86.95 (??.TPTP_Interpret.ind2, False)}),
% 87.64/86.95 (??.TPTP_Interpret.ind2,
% 87.64/86.95 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False),
% 87.64/86.95 (??.TPTP_Interpret.ind2, True)})}
% 87.64/86.95 bnd_environment: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 87.64/86.95 (??.TPTP_Interpret.ind2, True)}
% 87.64/86.95
% 87.64/86.95 % SZS status CounterSatisfiable
%------------------------------------------------------------------------------