%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : MGT035-2 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n019.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 29 12:02:37 PM UTC 2026
% Result : Unsatisfiable 2.60s 0.92s
% Output : Refutation 2.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 82
% Syntax : Number of formulae : 508 ( 49 unt; 48 def)
% Number of atoms : 1459 ( 57 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1728 ( 777 ~; 903 |; 0 &)
% ( 48 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 61 ( 59 usr; 49 prp; 0-4 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-2 aty)
% Number of variables : 170 ( 0 sgn 170 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| in_environment(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_time_point_in_environment_36) ).
fof(f2,axiom,
! [X0,X1] :
( ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| greater(number_of_organizations(X0,X1),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_environment_not_empty_37) ).
fof(f4,axiom,
! [X2,X0,X1] :
( ~ environment(X0)
| ~ subpopulation(X1,X0,X2)
| X1 != efficient_producers
| number_of_organizations(X0,X2) = sum(cardinality_at_time(first_movers,X2),cardinality_at_time(efficient_producers,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_only_members_39) ).
fof(f5,plain,
! [X2,X0,X1] :
( ~ environment(X0)
| ~ subpopulation(X1,X0,X2)
| efficient_producers != X1
| number_of_organizations(X0,X2) = sum(cardinality_at_time(first_movers,X2),cardinality_at_time(efficient_producers,X2)) ),
inference(reorient_equations,[],[f4]) ).
fof(f8,axiom,
! [X0,X1] :
( ~ in_environment(X0,X1)
| ~ environment(X0)
| subpopulation(first_movers,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_FM_and_EP_organisational_41) ).
fof(f9,axiom,
! [X0,X1] :
( ~ in_environment(X0,X1)
| ~ environment(X0)
| subpopulation(efficient_producers,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_FM_and_EP_organisational_42) ).
fof(f10,axiom,
! [X2,X0,X1] :
( X0 != sum(X1,X2)
| ~ constant(X0)
| constant(X1)
| increases(X1)
| decreases(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_abc_sum_increase_43) ).
fof(f11,plain,
! [X2,X0,X1] :
( sum(X1,X2) != X0
| ~ constant(X0)
| constant(X1)
| increases(X1)
| decreases(X1) ),
inference(reorient_equations,[],[f10]) ).
fof(f12,axiom,
! [X2,X0,X1] :
( X0 != sum(X1,X2)
| ~ constant(X0)
| constant(X1)
| increases(X1)
| increases(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_abc_sum_increase_44) ).
fof(f13,plain,
! [X2,X0,X1] :
( sum(X1,X2) != X0
| ~ constant(X0)
| constant(X1)
| increases(X1)
| increases(X2) ),
inference(reorient_equations,[],[f12]) ).
fof(f14,axiom,
! [X2,X0,X1] :
( X0 != sum(X1,X2)
| ~ constant(X0)
| constant(X1)
| decreases(X2)
| decreases(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_abc_sum_increase_45) ).
fof(f15,plain,
! [X2,X0,X1] :
( sum(X1,X2) != X0
| ~ constant(X0)
| constant(X1)
| decreases(X2)
| decreases(X1) ),
inference(reorient_equations,[],[f14]) ).
fof(f16,axiom,
! [X2,X0,X1] :
( X0 != sum(X1,X2)
| ~ constant(X0)
| constant(X1)
| decreases(X2)
| increases(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_abc_sum_increase_46) ).
fof(f17,plain,
! [X2,X0,X1] :
( sum(X1,X2) != X0
| ~ constant(X0)
| constant(X1)
| decreases(X2)
| increases(X2) ),
inference(reorient_equations,[],[f16]) ).
fof(f22,axiom,
! [X2,X0,X1] :
( X0 != sum(X1,X2)
| ~ constant(X0)
| constant(X2)
| decreases(X2)
| decreases(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_abc_sum_increase_49) ).
fof(f23,plain,
! [X2,X0,X1] :
( sum(X1,X2) != X0
| ~ constant(X0)
| constant(X2)
| decreases(X2)
| decreases(X1) ),
inference(reorient_equations,[],[f22]) ).
fof(f26,axiom,
! [X2,X0,X1] :
( ~ environment(X0)
| ~ in_environment(X0,X1)
| ~ subpopulation(X2,X0,X1)
| ~ greater(cardinality_at_time(X2,X1),zero)
| ~ constant(cardinality_at_time(X2,X1))
| growth_rate(X2,X1) = zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_growth_rate_51) ).
fof(f27,plain,
! [X2,X0,X1] :
( ~ greater(cardinality_at_time(X2,X1),zero)
| ~ in_environment(X0,X1)
| ~ subpopulation(X2,X0,X1)
| ~ environment(X0)
| ~ constant(cardinality_at_time(X2,X1))
| zero = growth_rate(X2,X1) ),
inference(reorient_equations,[],[f26]) ).
fof(f28,axiom,
! [X2,X0,X1] :
( ~ greater(cardinality_at_time(X2,X1),zero)
| ~ in_environment(X0,X1)
| ~ subpopulation(X2,X0,X1)
| ~ environment(X0)
| ~ increases(cardinality_at_time(X2,X1))
| greater(growth_rate(X2,X1),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_growth_rate_52) ).
fof(f29,axiom,
! [X2,X0,X1] :
( ~ greater(cardinality_at_time(X2,X1),zero)
| ~ in_environment(X0,X1)
| ~ subpopulation(X2,X0,X1)
| ~ environment(X0)
| ~ decreases(cardinality_at_time(X2,X1))
| greater(zero,growth_rate(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_growth_rate_53) ).
fof(f30,axiom,
! [X0,X1] :
( ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| greater(cardinality_at_time(first_movers,X1),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_positive_number_of_organizations_54) ).
fof(f31,axiom,
! [X0,X1] :
( ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| greater(cardinality_at_time(efficient_producers,X1),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_positive_number_of_organizations_55) ).
fof(f32,axiom,
! [X0,X1] :
( ~ greater(X0,X1)
| X0 != X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp6_1_56) ).
fof(f33,axiom,
! [X0,X1] :
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp6_2_57) ).
fof(f34,axiom,
! [X2,X0,X1] :
( ~ greater(X1,X2)
| ~ greater(X0,X1)
| greater(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_transitivity_58) ).
fof(f35,axiom,
! [X2,X0,X1] :
( ~ in_environment(X0,X1)
| ~ in_environment(X0,X2)
| greater(X2,X1)
| X2 = X1
| greater(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_times_in_environment_59) ).
fof(f36,plain,
! [X2,X0,X1] :
( ~ in_environment(X0,X2)
| ~ in_environment(X0,X1)
| greater(X2,X1)
| X1 = X2
| greater(X1,X2) ),
inference(reorient_equations,[],[f35]) ).
fof(f37,axiom,
! [X0,X1] :
( ~ greater_or_equal(X0,X1)
| greater(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_60) ).
fof(f38,axiom,
! [X0,X1] :
( ~ greater(X0,X1)
| greater_or_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_61) ).
fof(f40,axiom,
! [X0,X1] :
( ~ greater_or_equal(X1,equilibrium(X0))
| ~ environment(X0)
| ~ greater(equilibrium(X0),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_equilibrium_63) ).
fof(f41,axiom,
! [X2,X3,X0,X1] :
( ~ greater_or_equal(growth_rate(X2,X3),zero)
| ~ subpopulations(X1,X2,X0,X3)
| ~ environment(X0)
| ~ greater(zero,growth_rate(X1,X3))
| outcompetes(X2,X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_64) ).
fof(f45,axiom,
! [X0,X1] :
( ~ greater(number_of_organizations(X0,X1),zero)
| ~ in_environment(X0,X1)
| ~ environment(X0)
| greater(equilibrium(X0),X1)
| constant(resources(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a4_68) ).
fof(f46,axiom,
! [X0] :
( ~ stable(X0)
| ~ environment(X0)
| in_environment(X0,sk1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a5_69) ).
fof(f47,axiom,
! [X0] :
( greater_or_equal(sk1(X0),equilibrium(X0))
| ~ stable(X0)
| ~ environment(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a5_70) ).
fof(f49,axiom,
! [X0,X1] :
( ~ constant(resources(X0,X1))
| ~ in_environment(X0,X1)
| ~ environment(X0)
| constant(number_of_organizations(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a7_72) ).
fof(f52,axiom,
! [X0] :
( ~ stable(X0)
| ~ environment(X0)
| in_environment(X0,sk2(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l1_74) ).
fof(f53,axiom,
! [X0,X1] :
( ~ subpopulations(first_movers,efficient_producers,X0,X1)
| ~ stable(X0)
| ~ environment(X0)
| ~ greater_or_equal(X1,sk2(X0))
| greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l1_75) ).
fof(f54,negated_conjecture,
environment(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_t4_76) ).
fof(f55,negated_conjecture,
stable(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_t4_77) ).
fof(f56,negated_conjecture,
! [X0] :
( subpopulations(first_movers,efficient_producers,sk3,sk4(X0))
| ~ in_environment(sk3,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_t4_78) ).
fof(f57,negated_conjecture,
! [X0] :
( greater_or_equal(sk4(X0),X0)
| ~ in_environment(sk3,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_t4_79) ).
fof(f58,negated_conjecture,
! [X0] :
( ~ outcompetes(efficient_producers,first_movers,sk4(X0))
| ~ in_environment(sk3,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_t4_80) ).
fof(f59,plain,
! [X2,X0] :
( ~ subpopulation(efficient_producers,X0,X2)
| ~ environment(X0)
| number_of_organizations(X0,X2) = sum(cardinality_at_time(first_movers,X2),cardinality_at_time(efficient_producers,X2)) ),
inference(equality_resolution,[],[f5]) ).
fof(f61,plain,
! [X2,X1] :
( ~ constant(sum(X1,X2))
| constant(X1)
| increases(X1)
| decreases(X1) ),
inference(equality_resolution,[],[f11]) ).
fof(f62,plain,
! [X2,X1] :
( ~ constant(sum(X1,X2))
| constant(X1)
| increases(X1)
| increases(X2) ),
inference(equality_resolution,[],[f13]) ).
fof(f63,plain,
! [X2,X1] :
( ~ constant(sum(X1,X2))
| constant(X1)
| decreases(X2)
| decreases(X1) ),
inference(equality_resolution,[],[f15]) ).
fof(f64,plain,
! [X2,X1] :
( ~ constant(sum(X1,X2))
| constant(X1)
| decreases(X2)
| increases(X2) ),
inference(equality_resolution,[],[f17]) ).
fof(f67,plain,
! [X2,X1] :
( ~ constant(sum(X1,X2))
| constant(X2)
| decreases(X2)
| decreases(X1) ),
inference(equality_resolution,[],[f23]) ).
fof(f69,plain,
! [X1] : ~ greater(X1,X1),
inference(equality_resolution,[],[f32]) ).
fof(f71,plain,
( ~ environment(sk3)
| in_environment(sk3,sk1(sk3)) ),
inference(resolution,[],[f46,f55]) ).
fof(f72,plain,
in_environment(sk3,sk1(sk3)),
inference(forward_subsumption_resolution,[],[f71,f54]) ).
fof(f73,plain,
( ~ environment(sk3)
| in_environment(sk3,sk2(sk3)) ),
inference(resolution,[],[f52,f55]) ).
fof(f74,plain,
in_environment(sk3,sk2(sk3)),
inference(forward_subsumption_resolution,[],[f73,f54]) ).
fof(f83,plain,
! [X0] :
( ~ in_environment(sk3,X0)
| sk4(X0) = X0
| greater(sk4(X0),X0) ),
inference(resolution,[],[f37,f57]) ).
fof(f85,plain,
! [X0] :
( ~ stable(X0)
| equilibrium(X0) = sk1(X0)
| greater(sk1(X0),equilibrium(X0))
| ~ environment(X0) ),
inference(resolution,[],[f37,f47]) ).
fof(f86,plain,
! [X0] :
( ~ environment(sk3)
| in_environment(sk3,sk4(X0))
| ~ in_environment(sk3,X0) ),
inference(resolution,[],[f1,f56]) ).
fof(f87,plain,
! [X0] :
( in_environment(sk3,sk4(X0))
| ~ in_environment(sk3,X0) ),
inference(forward_subsumption_resolution,[],[f86,f54]) ).
fof(f92,plain,
! [X0] :
( ~ in_environment(sk3,X0)
| ~ environment(sk3)
| subpopulation(efficient_producers,sk3,sk4(X0)) ),
inference(resolution,[],[f87,f9]) ).
fof(f95,plain,
! [X0] :
( ~ in_environment(sk3,X0)
| subpopulation(efficient_producers,sk3,sk4(X0)) ),
inference(forward_subsumption_resolution,[],[f92,f54]) ).
fof(f99,plain,
subpopulation(efficient_producers,sk3,sk4(sk1(sk3))),
inference(resolution,[],[f95,f72]) ).
fof(f100,plain,
subpopulation(efficient_producers,sk3,sk4(sk2(sk3))),
inference(resolution,[],[f95,f74]) ).
fof(f105,plain,
! [X0] :
( ~ environment(sk3)
| greater(number_of_organizations(sk3,sk4(X0)),zero)
| ~ in_environment(sk3,X0) ),
inference(resolution,[],[f2,f56]) ).
fof(f106,plain,
! [X0] :
( ~ in_environment(sk3,X0)
| greater(number_of_organizations(sk3,sk4(X0)),zero) ),
inference(forward_subsumption_resolution,[],[f105,f54]) ).
fof(f107,plain,
! [X0] :
( ~ environment(sk3)
| greater(cardinality_at_time(first_movers,sk4(X0)),zero)
| ~ in_environment(sk3,X0) ),
inference(resolution,[],[f30,f56]) ).
fof(f108,plain,
! [X0] :
( ~ in_environment(sk3,X0)
| greater(cardinality_at_time(first_movers,sk4(X0)),zero) ),
inference(forward_subsumption_resolution,[],[f107,f54]) ).
fof(f109,plain,
greater(number_of_organizations(sk3,sk4(sk1(sk3))),zero),
inference(resolution,[],[f106,f72]) ).
fof(f110,plain,
greater(number_of_organizations(sk3,sk4(sk2(sk3))),zero),
inference(resolution,[],[f106,f74]) ).
fof(f112,plain,
! [X0] :
( ~ environment(sk3)
| greater(cardinality_at_time(efficient_producers,sk4(X0)),zero)
| ~ in_environment(sk3,X0) ),
inference(resolution,[],[f31,f56]) ).
fof(f113,plain,
! [X0] :
( ~ in_environment(sk3,X0)
| greater(cardinality_at_time(efficient_producers,sk4(X0)),zero) ),
inference(forward_subsumption_resolution,[],[f112,f54]) ).
fof(f121,plain,
! [X0] :
( ~ in_environment(sk3,X0)
| greater(sk1(sk3),X0)
| sk1(sk3) = X0
| greater(X0,sk1(sk3)) ),
inference(resolution,[],[f36,f72]) ).
fof(f127,plain,
greater(cardinality_at_time(first_movers,sk4(sk1(sk3))),zero),
inference(resolution,[],[f108,f72]) ).
fof(f128,plain,
greater(cardinality_at_time(first_movers,sk4(sk2(sk3))),zero),
inference(resolution,[],[f108,f74]) ).
fof(f132,plain,
( ~ environment(sk3)
| number_of_organizations(sk3,sk4(sk1(sk3))) = sum(cardinality_at_time(first_movers,sk4(sk1(sk3))),cardinality_at_time(efficient_producers,sk4(sk1(sk3)))) ),
inference(resolution,[],[f59,f99]) ).
fof(f133,plain,
( ~ environment(sk3)
| number_of_organizations(sk3,sk4(sk2(sk3))) = sum(cardinality_at_time(first_movers,sk4(sk2(sk3))),cardinality_at_time(efficient_producers,sk4(sk2(sk3)))) ),
inference(resolution,[],[f59,f100]) ).
fof(f134,plain,
number_of_organizations(sk3,sk4(sk2(sk3))) = sum(cardinality_at_time(first_movers,sk4(sk2(sk3))),cardinality_at_time(efficient_producers,sk4(sk2(sk3)))),
inference(forward_subsumption_resolution,[],[f133,f54]) ).
fof(f135,plain,
number_of_organizations(sk3,sk4(sk1(sk3))) = sum(cardinality_at_time(first_movers,sk4(sk1(sk3))),cardinality_at_time(efficient_producers,sk4(sk1(sk3)))),
inference(forward_subsumption_resolution,[],[f132,f54]) ).
fof(f163,definition,
( spl0_2
<=> greater(equilibrium(sk3),sk4(sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f164,plain,
( greater(equilibrium(sk3),sk4(sk2(sk3)))
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f163]) ).
fof(f165,plain,
( ~ greater(equilibrium(sk3),sk4(sk2(sk3)))
| spl0_2 ),
inference(avatar_component_clause,[],[f163]) ).
fof(f167,definition,
( spl0_3
<=> in_environment(sk3,sk4(sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f168,plain,
( in_environment(sk3,sk4(sk2(sk3)))
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f167]) ).
fof(f169,plain,
( ~ in_environment(sk3,sk4(sk2(sk3)))
| spl0_3 ),
inference(avatar_component_clause,[],[f167]) ).
fof(f176,definition,
( spl0_5
<=> greater(equilibrium(sk3),sk4(sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f177,plain,
( greater(equilibrium(sk3),sk4(sk1(sk3)))
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f176]) ).
fof(f178,plain,
( ~ greater(equilibrium(sk3),sk4(sk1(sk3)))
| spl0_5 ),
inference(avatar_component_clause,[],[f176]) ).
fof(f180,definition,
( spl0_6
<=> in_environment(sk3,sk4(sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f181,plain,
( in_environment(sk3,sk4(sk1(sk3)))
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f182,plain,
( ~ in_environment(sk3,sk4(sk1(sk3)))
| spl0_6 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f184,plain,
( ~ in_environment(sk3,sk1(sk3))
| spl0_6 ),
inference(resolution,[],[f182,f87]) ).
fof(f185,plain,
( $false
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f184,f72]) ).
fof(f186,plain,
spl0_6,
inference(avatar_contradiction_clause,[],[f185]) ).
fof(f187,plain,
( ~ in_environment(sk3,sk4(sk1(sk3)))
| ~ environment(sk3)
| greater(equilibrium(sk3),sk4(sk1(sk3)))
| constant(resources(sk3,sk4(sk1(sk3)))) ),
inference(resolution,[],[f45,f109]) ).
fof(f188,plain,
( ~ in_environment(sk3,sk4(sk2(sk3)))
| ~ environment(sk3)
| greater(equilibrium(sk3),sk4(sk2(sk3)))
| constant(resources(sk3,sk4(sk2(sk3)))) ),
inference(resolution,[],[f45,f110]) ).
fof(f189,plain,
( ~ in_environment(sk3,sk4(sk2(sk3)))
| greater(equilibrium(sk3),sk4(sk2(sk3)))
| constant(resources(sk3,sk4(sk2(sk3)))) ),
inference(forward_subsumption_resolution,[],[f188,f54]) ).
fof(f190,plain,
( ~ environment(sk3)
| greater(equilibrium(sk3),sk4(sk1(sk3)))
| constant(resources(sk3,sk4(sk1(sk3))))
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f187,f181]) ).
fof(f191,plain,
( ~ in_environment(sk3,sk4(sk2(sk3)))
| constant(resources(sk3,sk4(sk2(sk3))))
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f189,f165]) ).
fof(f192,plain,
( greater(equilibrium(sk3),sk4(sk1(sk3)))
| constant(resources(sk3,sk4(sk1(sk3))))
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f190,f54]) ).
fof(f194,definition,
( spl0_7
<=> constant(resources(sk3,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f196,plain,
( constant(resources(sk3,sk4(sk2(sk3))))
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f194]) ).
fof(f197,plain,
( spl0_7
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f191,f163,f167,f194]) ).
fof(f198,plain,
( constant(resources(sk3,sk4(sk1(sk3))))
| spl0_5
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f192,f178]) ).
fof(f199,plain,
( ~ in_environment(sk3,sk2(sk3))
| spl0_3 ),
inference(resolution,[],[f169,f87]) ).
fof(f200,plain,
( $false
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f199,f74]) ).
fof(f201,plain,
spl0_3,
inference(avatar_contradiction_clause,[],[f200]) ).
fof(f202,plain,
! [X0] :
( ~ stable(sk3)
| ~ environment(sk3)
| ~ greater_or_equal(sk4(X0),sk2(sk3))
| greater(growth_rate(efficient_producers,sk4(X0)),growth_rate(first_movers,sk4(X0)))
| ~ in_environment(sk3,X0) ),
inference(resolution,[],[f53,f56]) ).
fof(f203,plain,
! [X0] :
( ~ environment(sk3)
| ~ greater_or_equal(sk4(X0),sk2(sk3))
| greater(growth_rate(efficient_producers,sk4(X0)),growth_rate(first_movers,sk4(X0)))
| ~ in_environment(sk3,X0) ),
inference(forward_subsumption_resolution,[],[f202,f55]) ).
fof(f204,plain,
! [X0] :
( ~ greater_or_equal(sk4(X0),sk2(sk3))
| greater(growth_rate(efficient_producers,sk4(X0)),growth_rate(first_movers,sk4(X0)))
| ~ in_environment(sk3,X0) ),
inference(forward_subsumption_resolution,[],[f203,f54]) ).
fof(f231,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk1(sk3)))
| ~ subpopulation(first_movers,X0,sk4(sk1(sk3)))
| ~ environment(X0)
| ~ constant(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| zero = growth_rate(first_movers,sk4(sk1(sk3))) ),
inference(resolution,[],[f27,f127]) ).
fof(f232,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk2(sk3)))
| ~ subpopulation(first_movers,X0,sk4(sk2(sk3)))
| ~ environment(X0)
| ~ constant(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| zero = growth_rate(first_movers,sk4(sk2(sk3))) ),
inference(resolution,[],[f27,f128]) ).
fof(f233,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk2(sk3)))
| ~ environment(X0)
| ~ constant(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| zero = growth_rate(first_movers,sk4(sk2(sk3))) ),
inference(forward_subsumption_resolution,[],[f232,f8]) ).
fof(f234,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk1(sk3)))
| ~ environment(X0)
| ~ constant(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| zero = growth_rate(first_movers,sk4(sk1(sk3))) ),
inference(forward_subsumption_resolution,[],[f231,f8]) ).
fof(f236,definition,
( spl0_8
<=> zero = growth_rate(first_movers,sk4(sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f238,plain,
( zero = growth_rate(first_movers,sk4(sk2(sk3)))
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f240,definition,
( spl0_9
<=> constant(cardinality_at_time(first_movers,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f242,plain,
( ~ constant(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| spl0_9 ),
inference(avatar_component_clause,[],[f240]) ).
fof(f244,definition,
( spl0_10
<=> ! [X0] :
( ~ in_environment(X0,sk4(sk2(sk3)))
| ~ environment(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f245,plain,
( ! [X0] :
( ~ in_environment(X0,sk4(sk2(sk3)))
| ~ environment(X0) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f246,plain,
( spl0_8
| ~ spl0_9
| spl0_10 ),
inference(avatar_split_clause,[],[f233,f244,f240,f236]) ).
fof(f248,definition,
( spl0_11
<=> zero = growth_rate(first_movers,sk4(sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f250,plain,
( zero = growth_rate(first_movers,sk4(sk1(sk3)))
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f252,definition,
( spl0_12
<=> constant(cardinality_at_time(first_movers,sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f254,plain,
( ~ constant(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| spl0_12 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f256,definition,
( spl0_13
<=> ! [X0] :
( ~ in_environment(X0,sk4(sk1(sk3)))
| ~ environment(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f257,plain,
( ! [X0] :
( ~ in_environment(X0,sk4(sk1(sk3)))
| ~ environment(X0) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f258,plain,
( spl0_11
| ~ spl0_12
| spl0_13 ),
inference(avatar_split_clause,[],[f234,f256,f252,f248]) ).
fof(f259,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk1(sk3)))
| ~ subpopulation(first_movers,X0,sk4(sk1(sk3)))
| ~ environment(X0)
| ~ increases(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero) ),
inference(resolution,[],[f28,f127]) ).
fof(f260,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk2(sk3)))
| ~ subpopulation(first_movers,X0,sk4(sk2(sk3)))
| ~ environment(X0)
| ~ increases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero) ),
inference(resolution,[],[f28,f128]) ).
fof(f261,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk2(sk3)))
| ~ environment(X0)
| ~ increases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| greater(growth_rate(first_movers,sk4(sk2(sk3))),zero) ),
inference(forward_subsumption_resolution,[],[f260,f8]) ).
fof(f262,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk1(sk3)))
| ~ environment(X0)
| ~ increases(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| greater(growth_rate(first_movers,sk4(sk1(sk3))),zero) ),
inference(forward_subsumption_resolution,[],[f259,f8]) ).
fof(f264,definition,
( spl0_14
<=> greater(growth_rate(first_movers,sk4(sk2(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f268,definition,
( spl0_15
<=> increases(cardinality_at_time(first_movers,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f270,plain,
( ~ increases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| spl0_15 ),
inference(avatar_component_clause,[],[f268]) ).
fof(f271,plain,
( spl0_14
| ~ spl0_15
| spl0_10 ),
inference(avatar_split_clause,[],[f261,f244,f268,f264]) ).
fof(f273,definition,
( spl0_16
<=> greater(growth_rate(first_movers,sk4(sk1(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f275,plain,
( greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f273]) ).
fof(f277,definition,
( spl0_17
<=> increases(cardinality_at_time(first_movers,sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f279,plain,
( ~ increases(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| spl0_17 ),
inference(avatar_component_clause,[],[f277]) ).
fof(f280,plain,
( spl0_16
| ~ spl0_17
| spl0_13 ),
inference(avatar_split_clause,[],[f262,f256,f277,f273]) ).
fof(f281,plain,
( ~ in_environment(sk3,sk4(sk2(sk3)))
| ~ environment(sk3)
| constant(number_of_organizations(sk3,sk4(sk2(sk3))))
| ~ spl0_7 ),
inference(resolution,[],[f196,f49]) ).
fof(f282,plain,
( ~ environment(sk3)
| constant(number_of_organizations(sk3,sk4(sk2(sk3))))
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f281,f168]) ).
fof(f283,plain,
( constant(number_of_organizations(sk3,sk4(sk2(sk3))))
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f282,f54]) ).
fof(f284,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk1(sk3)))
| ~ subpopulation(first_movers,X0,sk4(sk1(sk3)))
| ~ environment(X0)
| ~ decreases(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(resolution,[],[f29,f127]) ).
fof(f285,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk2(sk3)))
| ~ subpopulation(first_movers,X0,sk4(sk2(sk3)))
| ~ environment(X0)
| ~ decreases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3)))) ),
inference(resolution,[],[f29,f128]) ).
fof(f286,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk2(sk3)))
| ~ environment(X0)
| ~ decreases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk2(sk3)))) ),
inference(forward_subsumption_resolution,[],[f285,f8]) ).
fof(f287,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk1(sk3)))
| ~ environment(X0)
| ~ decreases(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))) ),
inference(forward_subsumption_resolution,[],[f284,f8]) ).
fof(f289,definition,
( spl0_18
<=> greater(zero,growth_rate(first_movers,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f290,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| spl0_18 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f291,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f293,definition,
( spl0_19
<=> decreases(cardinality_at_time(first_movers,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f296,plain,
( spl0_18
| ~ spl0_19
| spl0_10 ),
inference(avatar_split_clause,[],[f286,f244,f293,f289]) ).
fof(f298,definition,
( spl0_20
<=> greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f299,plain,
( ~ greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| spl0_20 ),
inference(avatar_component_clause,[],[f298]) ).
fof(f300,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f298]) ).
fof(f302,definition,
( spl0_21
<=> decreases(cardinality_at_time(first_movers,sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f304,plain,
( ~ decreases(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| spl0_21 ),
inference(avatar_component_clause,[],[f302]) ).
fof(f305,plain,
( spl0_20
| ~ spl0_21
| spl0_13 ),
inference(avatar_split_clause,[],[f287,f256,f302,f298]) ).
fof(f306,plain,
( ~ in_environment(sk3,sk4(sk1(sk3)))
| ~ environment(sk3)
| constant(number_of_organizations(sk3,sk4(sk1(sk3))))
| spl0_5
| ~ spl0_6 ),
inference(resolution,[],[f198,f49]) ).
fof(f307,plain,
( ~ environment(sk3)
| constant(number_of_organizations(sk3,sk4(sk1(sk3))))
| spl0_5
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f306,f181]) ).
fof(f308,plain,
( constant(number_of_organizations(sk3,sk4(sk1(sk3))))
| spl0_5
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f307,f54]) ).
fof(f309,plain,
greater(cardinality_at_time(efficient_producers,sk4(sk1(sk3))),zero),
inference(resolution,[],[f113,f72]) ).
fof(f310,plain,
greater(cardinality_at_time(efficient_producers,sk4(sk2(sk3))),zero),
inference(resolution,[],[f113,f74]) ).
fof(f314,plain,
( sk1(sk3) = sk4(sk1(sk3))
| greater(sk4(sk1(sk3)),sk1(sk3)) ),
inference(resolution,[],[f83,f72]) ).
fof(f315,plain,
( sk2(sk3) = sk4(sk2(sk3))
| greater(sk4(sk2(sk3)),sk2(sk3)) ),
inference(resolution,[],[f83,f74]) ).
fof(f338,definition,
( spl0_26
<=> greater(sk4(sk2(sk3)),sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f340,plain,
( greater(sk4(sk2(sk3)),sk2(sk3))
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f338]) ).
fof(f342,definition,
( spl0_27
<=> sk2(sk3) = sk4(sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f344,plain,
( sk2(sk3) = sk4(sk2(sk3))
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f345,plain,
( spl0_26
| spl0_27 ),
inference(avatar_split_clause,[],[f315,f342,f338]) ).
fof(f347,definition,
( spl0_28
<=> greater(sk4(sk1(sk3)),sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f349,plain,
( greater(sk4(sk1(sk3)),sk1(sk3))
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f351,definition,
( spl0_29
<=> sk1(sk3) = sk4(sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f353,plain,
( sk1(sk3) = sk4(sk1(sk3))
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f351]) ).
fof(f354,plain,
( spl0_28
| spl0_29 ),
inference(avatar_split_clause,[],[f314,f351,f347]) ).
fof(f360,plain,
( ~ greater(sk1(sk3),sk4(sk1(sk3)))
| ~ spl0_28 ),
inference(resolution,[],[f349,f33]) ).
fof(f361,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ~ in_environment(sk3,sk2(sk3))
| ~ in_environment(sk3,sk2(sk3)) ),
inference(resolution,[],[f204,f57]) ).
fof(f362,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))
| ~ in_environment(sk3,sk2(sk3)) ),
inference(duplicate_literal_removal,[],[f361]) ).
fof(f363,plain,
greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3)))),
inference(forward_subsumption_resolution,[],[f362,f74]) ).
fof(f364,plain,
( sk1(sk3) = equilibrium(sk3)
| greater(sk1(sk3),equilibrium(sk3))
| ~ environment(sk3) ),
inference(resolution,[],[f85,f55]) ).
fof(f365,plain,
( sk1(sk3) = equilibrium(sk3)
| greater(sk1(sk3),equilibrium(sk3)) ),
inference(forward_subsumption_resolution,[],[f364,f54]) ).
fof(f367,definition,
( spl0_30
<=> greater(sk1(sk3),equilibrium(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f369,plain,
( greater(sk1(sk3),equilibrium(sk3))
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f367]) ).
fof(f371,definition,
( spl0_31
<=> sk1(sk3) = equilibrium(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f373,plain,
( sk1(sk3) = equilibrium(sk3)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f371]) ).
fof(f374,plain,
( spl0_30
| spl0_31 ),
inference(avatar_split_clause,[],[f365,f371,f367]) ).
fof(f375,plain,
( ! [X0] :
( ~ greater(X0,sk1(sk3))
| greater(X0,equilibrium(sk3)) )
| ~ spl0_30 ),
inference(resolution,[],[f369,f34]) ).
fof(f378,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk1(sk3)))
| ~ subpopulation(efficient_producers,X0,sk4(sk1(sk3)))
| ~ environment(X0)
| ~ decreases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3)))) ),
inference(resolution,[],[f309,f29]) ).
fof(f379,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk1(sk3)))
| ~ subpopulation(efficient_producers,X0,sk4(sk1(sk3)))
| ~ environment(X0)
| ~ increases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero) ),
inference(resolution,[],[f309,f28]) ).
fof(f380,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk1(sk3)))
| ~ subpopulation(efficient_producers,X0,sk4(sk1(sk3)))
| ~ environment(X0)
| ~ constant(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| zero = growth_rate(efficient_producers,sk4(sk1(sk3))) ),
inference(resolution,[],[f309,f27]) ).
fof(f385,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk1(sk3)))
| ~ environment(X0)
| ~ constant(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| zero = growth_rate(efficient_producers,sk4(sk1(sk3))) ),
inference(forward_subsumption_resolution,[],[f380,f9]) ).
fof(f386,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk1(sk3)))
| ~ environment(X0)
| ~ increases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero) ),
inference(forward_subsumption_resolution,[],[f379,f9]) ).
fof(f387,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk1(sk3)))
| ~ environment(X0)
| ~ decreases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3)))) ),
inference(forward_subsumption_resolution,[],[f378,f9]) ).
fof(f389,definition,
( spl0_32
<=> zero = growth_rate(efficient_producers,sk4(sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f391,plain,
( zero = growth_rate(efficient_producers,sk4(sk1(sk3)))
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f393,definition,
( spl0_33
<=> constant(cardinality_at_time(efficient_producers,sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f395,plain,
( ~ constant(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| spl0_33 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f396,plain,
( spl0_32
| ~ spl0_33
| spl0_13 ),
inference(avatar_split_clause,[],[f385,f256,f393,f389]) ).
fof(f398,definition,
( spl0_34
<=> greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f400,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f398]) ).
fof(f402,definition,
( spl0_35
<=> increases(cardinality_at_time(efficient_producers,sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f405,plain,
( spl0_34
| ~ spl0_35
| spl0_13 ),
inference(avatar_split_clause,[],[f386,f256,f402,f398]) ).
fof(f407,definition,
( spl0_36
<=> greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f409,plain,
( greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f407]) ).
fof(f411,definition,
( spl0_37
<=> decreases(cardinality_at_time(efficient_producers,sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f413,plain,
( ~ decreases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| spl0_37 ),
inference(avatar_component_clause,[],[f411]) ).
fof(f414,plain,
( spl0_36
| ~ spl0_37
| spl0_13 ),
inference(avatar_split_clause,[],[f387,f256,f411,f407]) ).
fof(f417,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk2(sk3)))
| ~ subpopulation(efficient_producers,X0,sk4(sk2(sk3)))
| ~ environment(X0)
| ~ decreases(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3)))) ),
inference(resolution,[],[f310,f29]) ).
fof(f418,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk2(sk3)))
| ~ subpopulation(efficient_producers,X0,sk4(sk2(sk3)))
| ~ environment(X0)
| ~ increases(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero) ),
inference(resolution,[],[f310,f28]) ).
fof(f419,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk2(sk3)))
| ~ subpopulation(efficient_producers,X0,sk4(sk2(sk3)))
| ~ environment(X0)
| ~ constant(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| zero = growth_rate(efficient_producers,sk4(sk2(sk3))) ),
inference(resolution,[],[f310,f27]) ).
fof(f424,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk2(sk3)))
| ~ environment(X0)
| ~ constant(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| zero = growth_rate(efficient_producers,sk4(sk2(sk3))) ),
inference(forward_subsumption_resolution,[],[f419,f9]) ).
fof(f425,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk2(sk3)))
| ~ environment(X0)
| ~ increases(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero) ),
inference(forward_subsumption_resolution,[],[f418,f9]) ).
fof(f426,plain,
! [X0] :
( ~ in_environment(X0,sk4(sk2(sk3)))
| ~ environment(X0)
| ~ decreases(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3)))) ),
inference(forward_subsumption_resolution,[],[f417,f9]) ).
fof(f428,definition,
( spl0_38
<=> zero = growth_rate(efficient_producers,sk4(sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f430,plain,
( zero = growth_rate(efficient_producers,sk4(sk2(sk3)))
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f428]) ).
fof(f432,definition,
( spl0_39
<=> constant(cardinality_at_time(efficient_producers,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f434,plain,
( ~ constant(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| spl0_39 ),
inference(avatar_component_clause,[],[f432]) ).
fof(f435,plain,
( spl0_38
| ~ spl0_39
| spl0_10 ),
inference(avatar_split_clause,[],[f424,f244,f432,f428]) ).
fof(f437,definition,
( spl0_40
<=> greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f439,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f437]) ).
fof(f441,definition,
( spl0_41
<=> increases(cardinality_at_time(efficient_producers,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f443,plain,
( ~ increases(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| spl0_41 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f444,plain,
( spl0_40
| ~ spl0_41
| spl0_10 ),
inference(avatar_split_clause,[],[f425,f244,f441,f437]) ).
fof(f446,definition,
( spl0_42
<=> greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f448,plain,
( greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f446]) ).
fof(f450,definition,
( spl0_43
<=> decreases(cardinality_at_time(efficient_producers,sk4(sk2(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f452,plain,
( ~ decreases(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| spl0_43 ),
inference(avatar_component_clause,[],[f450]) ).
fof(f453,plain,
( spl0_42
| ~ spl0_43
| spl0_10 ),
inference(avatar_split_clause,[],[f426,f244,f450,f446]) ).
fof(f469,plain,
! [X0] :
( ~ greater(X0,growth_rate(efficient_producers,sk4(sk2(sk3))))
| greater(X0,growth_rate(first_movers,sk4(sk2(sk3)))) ),
inference(resolution,[],[f363,f34]) ).
fof(f471,plain,
~ greater(growth_rate(first_movers,sk4(sk2(sk3))),growth_rate(efficient_producers,sk4(sk2(sk3)))),
inference(resolution,[],[f363,f33]) ).
fof(f477,plain,
( greater(sk1(sk3),sk4(sk2(sk3)))
| sk1(sk3) = sk4(sk2(sk3))
| greater(sk4(sk2(sk3)),sk1(sk3))
| ~ spl0_3 ),
inference(resolution,[],[f121,f168]) ).
fof(f481,definition,
( spl0_44
<=> greater(sk4(sk2(sk3)),sk1(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f483,plain,
( greater(sk4(sk2(sk3)),sk1(sk3))
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f481]) ).
fof(f485,definition,
( spl0_45
<=> sk1(sk3) = sk4(sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f487,plain,
( sk1(sk3) = sk4(sk2(sk3))
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f485]) ).
fof(f489,definition,
( spl0_46
<=> greater(sk1(sk3),sk4(sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f490,plain,
( ~ greater(sk1(sk3),sk4(sk2(sk3)))
| spl0_46 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f491,plain,
( greater(sk1(sk3),sk4(sk2(sk3)))
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f492,plain,
( spl0_44
| spl0_45
| spl0_46
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f477,f167,f489,f485,f481]) ).
fof(f502,definition,
( spl0_49
<=> greater(sk1(sk3),sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f503,plain,
( ~ greater(sk1(sk3),sk2(sk3))
| spl0_49 ),
inference(avatar_component_clause,[],[f502]) ).
fof(f504,plain,
( greater(sk1(sk3),sk2(sk3))
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f502]) ).
fof(f517,definition,
( spl0_50
<=> greater(sk4(sk1(sk3)),sk2(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f518,plain,
( ~ greater(sk4(sk1(sk3)),sk2(sk3))
| spl0_50 ),
inference(avatar_component_clause,[],[f517]) ).
fof(f519,plain,
( greater(sk4(sk1(sk3)),sk2(sk3))
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f517]) ).
fof(f567,plain,
( greater_or_equal(sk4(sk1(sk3)),sk2(sk3))
| ~ spl0_50 ),
inference(resolution,[],[f519,f38]) ).
fof(f572,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))
| ~ in_environment(sk3,sk1(sk3))
| ~ spl0_50 ),
inference(resolution,[],[f567,f204]) ).
fof(f574,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f572,f72]) ).
fof(f575,plain,
( greater(sk4(sk1(sk3)),equilibrium(sk3))
| ~ spl0_28
| ~ spl0_30 ),
inference(resolution,[],[f375,f349]) ).
fof(f576,plain,
( greater(sk4(sk2(sk3)),equilibrium(sk3))
| ~ spl0_30
| ~ spl0_44 ),
inference(resolution,[],[f375,f483]) ).
fof(f592,plain,
( ~ greater(equilibrium(sk3),sk4(sk1(sk3)))
| ~ spl0_28
| ~ spl0_30 ),
inference(resolution,[],[f575,f33]) ).
fof(f594,plain,
( greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))
| ~ spl0_30
| ~ spl0_44 ),
inference(resolution,[],[f576,f38]) ).
fof(f857,definition,
( spl0_88
<=> greater(sk1(sk3),sk4(sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f858,plain,
( ~ greater(sk1(sk3),sk4(sk4(sk1(sk3))))
| spl0_88 ),
inference(avatar_component_clause,[],[f857]) ).
fof(f859,plain,
( greater(sk1(sk3),sk4(sk4(sk1(sk3))))
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f857]) ).
fof(f977,definition,
( spl0_102
<=> greater(equilibrium(sk3),sk4(sk4(sk1(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f978,plain,
( greater(equilibrium(sk3),sk4(sk4(sk1(sk3))))
| ~ spl0_102 ),
inference(avatar_component_clause,[],[f977]) ).
fof(f979,plain,
( ~ greater(equilibrium(sk3),sk4(sk4(sk1(sk3))))
| spl0_102 ),
inference(avatar_component_clause,[],[f977]) ).
fof(f1199,plain,
( greater(sk1(sk3),sk4(sk1(sk3)))
| ~ spl0_29
| ~ spl0_88 ),
inference(superposition,[],[f859,f353]) ).
fof(f1222,plain,
( greater(sk1(sk3),sk1(sk3))
| ~ spl0_29
| ~ spl0_88 ),
inference(forward_demodulation,[],[f1199,f353]) ).
fof(f1236,plain,
( $false
| ~ spl0_29
| ~ spl0_88 ),
inference(forward_subsumption_resolution,[],[f1222,f69]) ).
fof(f1237,plain,
( ~ spl0_29
| ~ spl0_88 ),
inference(avatar_contradiction_clause,[],[f1236]) ).
fof(f1266,plain,
( ~ greater(sk4(sk4(sk1(sk3))),equilibrium(sk3))
| ~ spl0_102 ),
inference(resolution,[],[f978,f33]) ).
fof(f1303,plain,
( ~ greater(equilibrium(sk3),sk4(equilibrium(sk3)))
| ~ spl0_28
| ~ spl0_31 ),
inference(superposition,[],[f360,f373]) ).
fof(f1321,plain,
( ~ greater(equilibrium(sk3),sk4(sk4(equilibrium(sk3))))
| ~ spl0_31
| spl0_88 ),
inference(superposition,[],[f858,f373]) ).
fof(f1330,plain,
( greater(equilibrium(sk3),sk4(sk4(equilibrium(sk3))))
| ~ spl0_31
| ~ spl0_102 ),
inference(superposition,[],[f978,f373]) ).
fof(f1337,plain,
( $false
| ~ spl0_31
| spl0_88
| ~ spl0_102 ),
inference(forward_subsumption_resolution,[],[f1321,f1330]) ).
fof(f1338,plain,
( ~ spl0_31
| spl0_88
| ~ spl0_102 ),
inference(avatar_contradiction_clause,[],[f1337]) ).
fof(f1399,plain,
( ~ environment(sk3)
| ~ greater(equilibrium(sk3),sk4(sk2(sk3)))
| ~ spl0_30
| ~ spl0_44 ),
inference(resolution,[],[f594,f40]) ).
fof(f1615,plain,
( ~ constant(number_of_organizations(sk3,sk4(sk2(sk3))))
| constant(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| increases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| decreases(cardinality_at_time(first_movers,sk4(sk2(sk3)))) ),
inference(superposition,[],[f61,f134]) ).
fof(f1616,plain,
( ~ constant(number_of_organizations(sk3,sk4(sk2(sk3))))
| constant(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| increases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| increases(cardinality_at_time(efficient_producers,sk4(sk2(sk3)))) ),
inference(superposition,[],[f62,f134]) ).
fof(f1617,plain,
( ~ constant(number_of_organizations(sk3,sk4(sk2(sk3))))
| constant(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| decreases(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| decreases(cardinality_at_time(first_movers,sk4(sk2(sk3)))) ),
inference(superposition,[],[f63,f134]) ).
fof(f1621,plain,
( ~ constant(number_of_organizations(sk3,sk4(sk2(sk3))))
| constant(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| decreases(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| decreases(cardinality_at_time(first_movers,sk4(sk2(sk3)))) ),
inference(superposition,[],[f67,f134]) ).
fof(f1624,plain,
( constant(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| decreases(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| decreases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f1621,f283]) ).
fof(f1628,plain,
( constant(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| decreases(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| decreases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f1617,f283]) ).
fof(f1629,plain,
( constant(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| increases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| increases(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f1616,f283]) ).
fof(f1630,plain,
( constant(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| increases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| decreases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| ~ spl0_3
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f1615,f283]) ).
fof(f1632,plain,
( decreases(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| decreases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| ~ spl0_3
| ~ spl0_7
| spl0_39 ),
inference(forward_subsumption_resolution,[],[f1624,f434]) ).
fof(f1636,plain,
( decreases(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| decreases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| ~ spl0_3
| ~ spl0_7
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f1628,f242]) ).
fof(f1637,plain,
( increases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| increases(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| ~ spl0_3
| ~ spl0_7
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f1629,f242]) ).
fof(f1638,plain,
( increases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| decreases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| ~ spl0_3
| ~ spl0_7
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f1630,f242]) ).
fof(f1640,plain,
( decreases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| ~ spl0_3
| ~ spl0_7
| spl0_39
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f1632,f452]) ).
fof(f1644,plain,
( decreases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| ~ spl0_3
| ~ spl0_7
| spl0_9
| spl0_43 ),
inference(forward_subsumption_resolution,[],[f1636,f452]) ).
fof(f1645,plain,
( increases(cardinality_at_time(efficient_producers,sk4(sk2(sk3))))
| ~ spl0_3
| ~ spl0_7
| spl0_9
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1637,f270]) ).
fof(f1646,plain,
( decreases(cardinality_at_time(first_movers,sk4(sk2(sk3))))
| ~ spl0_3
| ~ spl0_7
| spl0_9
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1638,f270]) ).
fof(f1659,plain,
( $false
| ~ spl0_3
| ~ spl0_7
| spl0_9
| spl0_15
| spl0_41 ),
inference(forward_subsumption_resolution,[],[f1645,f443]) ).
fof(f1660,plain,
( ~ spl0_3
| ~ spl0_7
| spl0_9
| spl0_15
| spl0_41 ),
inference(avatar_contradiction_clause,[],[f1659]) ).
fof(f1664,plain,
( ~ environment(sk3)
| ~ in_environment(sk3,sk2(sk3))
| ~ spl0_10 ),
inference(resolution,[],[f245,f87]) ).
fof(f1665,plain,
( ~ in_environment(sk3,sk2(sk3))
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f1664,f54]) ).
fof(f1668,plain,
( $false
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f1665,f74]) ).
fof(f1669,plain,
~ spl0_10,
inference(avatar_contradiction_clause,[],[f1668]) ).
fof(f1670,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))
| ~ spl0_8 ),
inference(superposition,[],[f471,f238]) ).
fof(f1672,plain,
( greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_8 ),
inference(superposition,[],[f363,f238]) ).
fof(f1675,plain,
( greater(zero,zero)
| ~ spl0_8
| ~ spl0_38 ),
inference(forward_demodulation,[],[f1672,f430]) ).
fof(f1678,plain,
( $false
| ~ spl0_8
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f1675,f69]) ).
fof(f1679,plain,
( ~ spl0_8
| ~ spl0_38 ),
inference(avatar_contradiction_clause,[],[f1678]) ).
fof(f1680,plain,
( greater(zero,zero)
| ~ spl0_8
| ~ spl0_18 ),
inference(forward_demodulation,[],[f291,f238]) ).
fof(f1683,plain,
( ~ spl0_42
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f1670,f236,f446]) ).
fof(f1684,plain,
( $false
| ~ spl0_8
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1680,f69]) ).
fof(f1685,plain,
( ~ spl0_8
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1684]) ).
fof(f1693,plain,
( ~ greater(equilibrium(sk3),sk4(sk2(sk3)))
| ~ spl0_30
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f1399,f54]) ).
fof(f1696,plain,
( $false
| ~ spl0_2
| ~ spl0_30
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f1693,f164]) ).
fof(f1697,plain,
( ~ spl0_2
| ~ spl0_30
| ~ spl0_44 ),
inference(avatar_contradiction_clause,[],[f1696]) ).
fof(f1793,plain,
( ! [X0] :
( ~ greater(X0,sk1(sk3))
| greater(X0,sk2(sk3)) )
| ~ spl0_49 ),
inference(resolution,[],[f504,f34]) ).
fof(f1803,plain,
( ~ greater(sk4(sk2(sk3)),equilibrium(sk3))
| ~ spl0_2 ),
inference(resolution,[],[f164,f33]) ).
fof(f1804,plain,
( ~ greater(sk1(sk3),equilibrium(sk3))
| ~ spl0_2
| ~ spl0_45 ),
inference(forward_demodulation,[],[f1803,f487]) ).
fof(f1807,plain,
( $false
| ~ spl0_2
| ~ spl0_30
| ~ spl0_45 ),
inference(forward_subsumption_resolution,[],[f1804,f369]) ).
fof(f1808,plain,
( ~ spl0_2
| ~ spl0_30
| ~ spl0_45 ),
inference(avatar_contradiction_clause,[],[f1807]) ).
fof(f1817,plain,
( ! [X0] :
( ~ greater(X0,sk4(sk2(sk3)))
| greater(X0,sk2(sk3)) )
| ~ spl0_26 ),
inference(resolution,[],[f340,f34]) ).
fof(f1823,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)
| ~ spl0_40 ),
inference(resolution,[],[f439,f38]) ).
fof(f1829,plain,
( greater(equilibrium(sk3),sk2(sk3))
| ~ spl0_2
| ~ spl0_26 ),
inference(resolution,[],[f1817,f164]) ).
fof(f1840,plain,
( greater(sk4(sk1(sk3)),sk2(sk3))
| ~ spl0_28
| ~ spl0_49 ),
inference(resolution,[],[f1793,f349]) ).
fof(f1893,plain,
( greater(sk1(sk3),sk2(sk3))
| ~ spl0_27
| ~ spl0_46 ),
inference(superposition,[],[f491,f344]) ).
fof(f1926,plain,
( $false
| ~ spl0_27
| ~ spl0_46
| spl0_49 ),
inference(forward_subsumption_resolution,[],[f1893,f503]) ).
fof(f1927,plain,
( ~ spl0_27
| ~ spl0_46
| spl0_49 ),
inference(avatar_contradiction_clause,[],[f1926]) ).
fof(f1951,plain,
( ! [X0] :
( ~ greater(X0,equilibrium(sk3))
| greater(X0,sk2(sk3)) )
| ~ spl0_2
| ~ spl0_26 ),
inference(resolution,[],[f1829,f34]) ).
fof(f2051,plain,
( ~ constant(number_of_organizations(sk3,sk4(sk1(sk3))))
| constant(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| increases(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| increases(cardinality_at_time(efficient_producers,sk4(sk1(sk3)))) ),
inference(superposition,[],[f62,f135]) ).
fof(f2053,plain,
( ~ constant(number_of_organizations(sk3,sk4(sk1(sk3))))
| constant(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| decreases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| increases(cardinality_at_time(efficient_producers,sk4(sk1(sk3)))) ),
inference(superposition,[],[f64,f135]) ).
fof(f2056,plain,
( ~ constant(number_of_organizations(sk3,sk4(sk1(sk3))))
| constant(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| decreases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| decreases(cardinality_at_time(first_movers,sk4(sk1(sk3)))) ),
inference(superposition,[],[f67,f135]) ).
fof(f2059,plain,
( constant(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| decreases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| decreases(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| spl0_5
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f2056,f308]) ).
fof(f2062,plain,
( constant(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| decreases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| increases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| spl0_5
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f2053,f308]) ).
fof(f2064,plain,
( constant(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| increases(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| increases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| spl0_5
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f2051,f308]) ).
fof(f2067,plain,
( decreases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| decreases(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| spl0_5
| ~ spl0_6
| spl0_33 ),
inference(forward_subsumption_resolution,[],[f2059,f395]) ).
fof(f2070,plain,
( decreases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| increases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| spl0_5
| ~ spl0_6
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f2062,f254]) ).
fof(f2072,plain,
( increases(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| increases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| spl0_5
| ~ spl0_6
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f2064,f254]) ).
fof(f2075,plain,
( decreases(cardinality_at_time(first_movers,sk4(sk1(sk3))))
| spl0_5
| ~ spl0_6
| spl0_33
| spl0_37 ),
inference(forward_subsumption_resolution,[],[f2067,f413]) ).
fof(f2078,plain,
( increases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| spl0_5
| ~ spl0_6
| spl0_12
| spl0_37 ),
inference(forward_subsumption_resolution,[],[f2070,f413]) ).
fof(f2080,plain,
( increases(cardinality_at_time(efficient_producers,sk4(sk1(sk3))))
| spl0_5
| ~ spl0_6
| spl0_12
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f2072,f279]) ).
fof(f2084,plain,
( $false
| spl0_5
| ~ spl0_6
| spl0_21
| spl0_33
| spl0_37 ),
inference(forward_subsumption_resolution,[],[f2075,f304]) ).
fof(f2085,plain,
( spl0_5
| ~ spl0_6
| spl0_21
| spl0_33
| spl0_37 ),
inference(avatar_contradiction_clause,[],[f2084]) ).
fof(f2629,plain,
( greater(sk1(sk3),sk2(sk3))
| ~ spl0_2
| ~ spl0_26
| ~ spl0_30 ),
inference(resolution,[],[f1951,f369]) ).
fof(f2811,plain,
( ~ greater(growth_rate(first_movers,sk4(sk1(sk3))),growth_rate(efficient_producers,sk4(sk1(sk3))))
| ~ spl0_50 ),
inference(resolution,[],[f574,f33]) ).
fof(f2812,plain,
( greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_32
| ~ spl0_50 ),
inference(superposition,[],[f574,f391]) ).
fof(f2813,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_11
| ~ spl0_50 ),
inference(superposition,[],[f574,f250]) ).
fof(f2826,plain,
( spl0_34
| ~ spl0_11
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f2813,f517,f248,f398]) ).
fof(f2827,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| ~ spl0_11
| ~ spl0_50 ),
inference(forward_demodulation,[],[f2811,f250]) ).
fof(f2829,plain,
( ~ spl0_36
| ~ spl0_11
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f2827,f517,f248,f407]) ).
fof(f2861,plain,
( ~ environment(sk3)
| ~ in_environment(sk3,sk1(sk3))
| ~ spl0_13 ),
inference(resolution,[],[f257,f87]) ).
fof(f2862,plain,
( ~ in_environment(sk3,sk1(sk3))
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f2861,f54]) ).
fof(f2865,plain,
( $false
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f2862,f72]) ).
fof(f2866,plain,
~ spl0_13,
inference(avatar_contradiction_clause,[],[f2865]) ).
fof(f2873,plain,
( ~ greater(sk1(sk3),sk2(sk3))
| ~ spl0_29
| spl0_50 ),
inference(forward_demodulation,[],[f518,f353]) ).
fof(f2889,plain,
( $false
| ~ spl0_29
| ~ spl0_49
| spl0_50 ),
inference(forward_subsumption_resolution,[],[f2873,f504]) ).
fof(f2890,plain,
( ~ spl0_29
| ~ spl0_49
| spl0_50 ),
inference(avatar_contradiction_clause,[],[f2889]) ).
fof(f2918,plain,
( ~ greater(equilibrium(sk3),sk4(sk2(sk3)))
| ~ spl0_31
| spl0_46 ),
inference(forward_demodulation,[],[f490,f373]) ).
fof(f2923,plain,
( ~ greater(equilibrium(sk3),sk2(sk3))
| ~ spl0_31
| spl0_49 ),
inference(forward_demodulation,[],[f503,f373]) ).
fof(f2959,plain,
( $false
| ~ spl0_2
| ~ spl0_31
| spl0_46 ),
inference(forward_subsumption_resolution,[],[f2918,f164]) ).
fof(f2960,plain,
( ~ spl0_2
| ~ spl0_31
| spl0_46 ),
inference(avatar_contradiction_clause,[],[f2959]) ).
fof(f2963,plain,
( $false
| ~ spl0_2
| ~ spl0_26
| ~ spl0_31
| spl0_49 ),
inference(forward_subsumption_resolution,[],[f2923,f1829]) ).
fof(f2964,plain,
( ~ spl0_2
| ~ spl0_26
| ~ spl0_31
| spl0_49 ),
inference(avatar_contradiction_clause,[],[f2963]) ).
fof(f3100,plain,
( greater(equilibrium(sk3),sk4(equilibrium(sk3)))
| ~ spl0_5
| ~ spl0_31 ),
inference(forward_demodulation,[],[f177,f373]) ).
fof(f3114,plain,
( $false
| ~ spl0_5
| ~ spl0_28
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f3100,f1303]) ).
fof(f3115,plain,
( ~ spl0_5
| ~ spl0_28
| ~ spl0_31 ),
inference(avatar_contradiction_clause,[],[f3114]) ).
fof(f3644,plain,
( spl0_19
| ~ spl0_3
| ~ spl0_7
| spl0_39
| spl0_43 ),
inference(avatar_split_clause,[],[f1640,f450,f432,f194,f167,f293]) ).
fof(f3646,plain,
( spl0_19
| ~ spl0_3
| ~ spl0_7
| spl0_9
| spl0_43 ),
inference(avatar_split_clause,[],[f1644,f450,f240,f194,f167,f293]) ).
fof(f3647,plain,
( spl0_19
| ~ spl0_3
| ~ spl0_7
| spl0_9
| spl0_15 ),
inference(avatar_split_clause,[],[f1646,f268,f240,f194,f167,f293]) ).
fof(f3749,plain,
( ~ greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)
| ~ spl0_18 ),
inference(resolution,[],[f291,f33]) ).
fof(f3750,plain,
( ~ spl0_14
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f3749,f289,f264]) ).
fof(f3753,plain,
( ! [X0,X1] :
( ~ greater(zero,growth_rate(X0,sk4(sk2(sk3))))
| ~ environment(X1)
| ~ subpopulations(X0,efficient_producers,X1,sk4(sk2(sk3)))
| outcompetes(efficient_producers,X0,sk4(sk2(sk3))) )
| ~ spl0_40 ),
inference(resolution,[],[f1823,f41]) ).
fof(f4740,plain,
( ! [X0] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,sk4(sk2(sk3)))
| outcompetes(efficient_producers,first_movers,sk4(sk2(sk3))) )
| ~ spl0_18
| ~ spl0_40 ),
inference(resolution,[],[f3753,f291]) ).
fof(f4782,plain,
( ~ spl0_5
| ~ spl0_28
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f592,f367,f347,f176]) ).
fof(f4795,plain,
( spl0_50
| ~ spl0_28
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f1840,f502,f347,f517]) ).
fof(f4813,plain,
( spl0_35
| spl0_5
| ~ spl0_6
| spl0_12
| spl0_37 ),
inference(avatar_split_clause,[],[f2078,f411,f252,f180,f176,f402]) ).
fof(f4814,plain,
( spl0_35
| spl0_5
| ~ spl0_6
| spl0_12
| spl0_17 ),
inference(avatar_split_clause,[],[f2080,f277,f252,f180,f176,f402]) ).
fof(f4917,plain,
( greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)
| ~ spl0_34 ),
inference(resolution,[],[f400,f38]) ).
fof(f4918,plain,
( ~ greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))
| ~ spl0_34 ),
inference(resolution,[],[f400,f33]) ).
fof(f4919,plain,
( ~ spl0_36
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f4918,f398,f407]) ).
fof(f4937,plain,
( ! [X0,X1] :
( ~ greater(zero,growth_rate(X0,sk4(sk1(sk3))))
| ~ environment(X1)
| ~ subpopulations(X0,efficient_producers,X1,sk4(sk1(sk3)))
| outcompetes(efficient_producers,X0,sk4(sk1(sk3))) )
| ~ spl0_34 ),
inference(resolution,[],[f4917,f41]) ).
fof(f5046,plain,
( ! [X0] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,sk4(sk1(sk3)))
| outcompetes(efficient_producers,first_movers,sk4(sk1(sk3))) )
| ~ spl0_20
| ~ spl0_34 ),
inference(resolution,[],[f4937,f300]) ).
fof(f5049,definition,
( spl0_161
<=> outcompetes(efficient_producers,first_movers,sk4(sk1(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f5051,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))
| ~ spl0_161 ),
inference(avatar_component_clause,[],[f5049]) ).
fof(f5053,definition,
( spl0_162
<=> ! [X0] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,sk4(sk1(sk3))) ) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f5054,plain,
( ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,sk4(sk1(sk3)))
| ~ environment(X0) )
| ~ spl0_162 ),
inference(avatar_component_clause,[],[f5053]) ).
fof(f5055,plain,
( spl0_161
| spl0_162
| ~ spl0_20
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f5046,f398,f298,f5053,f5049]) ).
fof(f5056,plain,
( ~ in_environment(sk3,sk1(sk3))
| ~ spl0_161 ),
inference(resolution,[],[f5051,f58]) ).
fof(f5057,plain,
( $false
| ~ spl0_161 ),
inference(forward_subsumption_resolution,[],[f5056,f72]) ).
fof(f5058,plain,
~ spl0_161,
inference(avatar_contradiction_clause,[],[f5057]) ).
fof(f5867,definition,
( spl0_216
<=> outcompetes(efficient_producers,first_movers,sk4(sk2(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_216])],[avatar_definition]) ).
fof(f5869,plain,
( outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))
| ~ spl0_216 ),
inference(avatar_component_clause,[],[f5867]) ).
fof(f5871,definition,
( spl0_217
<=> ! [X0] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,sk4(sk2(sk3))) ) ),
introduced(definition,[new_symbols(definition,[spl0_217])],[avatar_definition]) ).
fof(f5872,plain,
( ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,sk4(sk2(sk3)))
| ~ environment(X0) )
| ~ spl0_217 ),
inference(avatar_component_clause,[],[f5871]) ).
fof(f5873,plain,
( spl0_216
| spl0_217
| ~ spl0_18
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f4740,f437,f289,f5871,f5867]) ).
fof(f6037,plain,
( ~ in_environment(sk3,sk2(sk3))
| ~ spl0_216 ),
inference(resolution,[],[f5869,f58]) ).
fof(f6038,plain,
( $false
| ~ spl0_216 ),
inference(forward_subsumption_resolution,[],[f6037,f74]) ).
fof(f6039,plain,
~ spl0_216,
inference(avatar_contradiction_clause,[],[f6038]) ).
fof(f6701,plain,
( ~ environment(sk3)
| ~ in_environment(sk3,sk1(sk3))
| ~ spl0_162 ),
inference(resolution,[],[f5054,f56]) ).
fof(f6702,plain,
( ~ in_environment(sk3,sk1(sk3))
| ~ spl0_162 ),
inference(forward_subsumption_resolution,[],[f6701,f54]) ).
fof(f6703,plain,
( $false
| ~ spl0_162 ),
inference(forward_subsumption_resolution,[],[f6702,f72]) ).
fof(f6704,plain,
~ spl0_162,
inference(avatar_contradiction_clause,[],[f6703]) ).
fof(f6710,plain,
( $false
| spl0_20
| ~ spl0_32
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f2812,f299]) ).
fof(f6711,plain,
( spl0_20
| ~ spl0_32
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f6710]) ).
fof(f6819,plain,
( ~ greater(equilibrium(sk3),sk4(sk1(sk3)))
| ~ spl0_29
| spl0_102 ),
inference(superposition,[],[f979,f353]) ).
fof(f6888,plain,
( $false
| ~ spl0_5
| ~ spl0_29
| spl0_102 ),
inference(forward_subsumption_resolution,[],[f6819,f177]) ).
fof(f6889,plain,
( ~ spl0_5
| ~ spl0_29
| spl0_102 ),
inference(avatar_contradiction_clause,[],[f6888]) ).
fof(f6925,plain,
( ~ greater(sk4(sk1(sk3)),equilibrium(sk3))
| ~ spl0_29
| ~ spl0_102 ),
inference(forward_demodulation,[],[f1266,f353]) ).
fof(f6977,plain,
( ~ greater(sk1(sk3),equilibrium(sk3))
| ~ spl0_29
| ~ spl0_102 ),
inference(forward_demodulation,[],[f6925,f353]) ).
fof(f7016,plain,
( $false
| ~ spl0_29
| ~ spl0_30
| ~ spl0_102 ),
inference(forward_subsumption_resolution,[],[f6977,f369]) ).
fof(f7017,plain,
( ~ spl0_29
| ~ spl0_30
| ~ spl0_102 ),
inference(avatar_contradiction_clause,[],[f7016]) ).
fof(f11538,plain,
( ~ environment(sk3)
| ~ in_environment(sk3,sk2(sk3))
| ~ spl0_217 ),
inference(resolution,[],[f5872,f56]) ).
fof(f11539,plain,
( ~ in_environment(sk3,sk2(sk3))
| ~ spl0_217 ),
inference(forward_subsumption_resolution,[],[f11538,f54]) ).
fof(f11540,plain,
( $false
| ~ spl0_217 ),
inference(forward_subsumption_resolution,[],[f11539,f74]) ).
fof(f11541,plain,
~ spl0_217,
inference(avatar_contradiction_clause,[],[f11540]) ).
fof(f16875,plain,
( greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))
| ~ spl0_42 ),
inference(resolution,[],[f448,f469]) ).
fof(f16879,plain,
( $false
| spl0_18
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f16875,f290]) ).
fof(f16880,plain,
( spl0_18
| ~ spl0_42 ),
inference(avatar_contradiction_clause,[],[f16879]) ).
fof(f16884,plain,
( spl0_49
| ~ spl0_2
| ~ spl0_26
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f2629,f367,f338,f163,f502]) ).
fof(f19958,plain,
( ! [X0] :
( greater(X0,growth_rate(efficient_producers,sk4(sk1(sk3))))
| ~ greater(X0,zero) )
| ~ spl0_36 ),
inference(resolution,[],[f409,f34]) ).
fof(f20143,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))
| ~ in_environment(sk3,sk1(sk3))
| ~ spl0_50 ),
inference(resolution,[],[f567,f204]) ).
fof(f20145,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f20143,f72]) ).
fof(f20462,plain,
( ! [X0,X1] :
( ~ greater(X1,X0)
| ~ greater(X0,zero)
| greater(X1,growth_rate(efficient_producers,sk4(sk1(sk3)))) )
| ~ spl0_36 ),
inference(resolution,[],[f19958,f34]) ).
fof(f22541,plain,
( ~ greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)
| greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(efficient_producers,sk4(sk1(sk3))))
| ~ spl0_36
| ~ spl0_50 ),
inference(resolution,[],[f20145,f20462]) ).
fof(f22545,plain,
( greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(efficient_producers,sk4(sk1(sk3))))
| ~ spl0_16
| ~ spl0_36
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f22541,f275]) ).
fof(f22550,plain,
( $false
| ~ spl0_16
| ~ spl0_36
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f22545,f69]) ).
fof(f22551,plain,
( ~ spl0_16
| ~ spl0_36
| ~ spl0_50 ),
inference(avatar_contradiction_clause,[],[f22550]) ).
cnf(s3,plain,
spl0_6,
inference(sat_conversion,[],[f186]) ).
cnf(s4,plain,
( spl0_2
| ~ spl0_3
| spl0_7 ),
inference(sat_conversion,[],[f197]) ).
cnf(s5,plain,
spl0_3,
inference(sat_conversion,[],[f201]) ).
cnf(s6,plain,
( spl0_8
| ~ spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f246]) ).
cnf(s7,plain,
( spl0_11
| ~ spl0_12
| spl0_13 ),
inference(sat_conversion,[],[f258]) ).
cnf(s8,plain,
( spl0_10
| spl0_14
| ~ spl0_15 ),
inference(sat_conversion,[],[f271]) ).
cnf(s9,plain,
( spl0_13
| spl0_16
| ~ spl0_17 ),
inference(sat_conversion,[],[f280]) ).
cnf(s10,plain,
( spl0_10
| spl0_18
| ~ spl0_19 ),
inference(sat_conversion,[],[f296]) ).
cnf(s11,plain,
( spl0_13
| spl0_20
| ~ spl0_21 ),
inference(sat_conversion,[],[f305]) ).
cnf(s14,plain,
( spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f345]) ).
cnf(s15,plain,
( spl0_28
| spl0_29 ),
inference(sat_conversion,[],[f354]) ).
cnf(s16,plain,
( spl0_30
| spl0_31 ),
inference(sat_conversion,[],[f374]) ).
cnf(s17,plain,
( spl0_13
| spl0_32
| ~ spl0_33 ),
inference(sat_conversion,[],[f396]) ).
cnf(s18,plain,
( spl0_13
| spl0_34
| ~ spl0_35 ),
inference(sat_conversion,[],[f405]) ).
cnf(s19,plain,
( spl0_13
| spl0_36
| ~ spl0_37 ),
inference(sat_conversion,[],[f414]) ).
cnf(s20,plain,
( spl0_10
| spl0_38
| ~ spl0_39 ),
inference(sat_conversion,[],[f435]) ).
cnf(s21,plain,
( spl0_10
| spl0_40
| ~ spl0_41 ),
inference(sat_conversion,[],[f444]) ).
cnf(s22,plain,
( spl0_10
| spl0_42
| ~ spl0_43 ),
inference(sat_conversion,[],[f453]) ).
cnf(s23,plain,
( ~ spl0_3
| spl0_44
| spl0_45
| spl0_46 ),
inference(sat_conversion,[],[f492]) ).
cnf(s87,plain,
( ~ spl0_29
| ~ spl0_88 ),
inference(sat_conversion,[],[f1237]) ).
cnf(s91,plain,
( ~ spl0_31
| spl0_88
| ~ spl0_102 ),
inference(sat_conversion,[],[f1338]) ).
cnf(s100,plain,
( ~ spl0_3
| ~ spl0_7
| spl0_9
| spl0_15
| spl0_41 ),
inference(sat_conversion,[],[f1660]) ).
cnf(s103,plain,
~ spl0_10,
inference(sat_conversion,[],[f1669]) ).
cnf(s104,plain,
( ~ spl0_8
| ~ spl0_38 ),
inference(sat_conversion,[],[f1679]) ).
cnf(s107,plain,
( ~ spl0_8
| ~ spl0_42 ),
inference(sat_conversion,[],[f1683]) ).
cnf(s108,plain,
( ~ spl0_8
| ~ spl0_18 ),
inference(sat_conversion,[],[f1685]) ).
cnf(s111,plain,
( ~ spl0_2
| ~ spl0_30
| ~ spl0_44 ),
inference(sat_conversion,[],[f1697]) ).
cnf(s120,plain,
( ~ spl0_2
| ~ spl0_30
| ~ spl0_45 ),
inference(sat_conversion,[],[f1808]) ).
cnf(s129,plain,
( ~ spl0_27
| ~ spl0_46
| spl0_49 ),
inference(sat_conversion,[],[f1927]) ).
cnf(s152,plain,
( spl0_5
| ~ spl0_6
| spl0_21
| spl0_33
| spl0_37 ),
inference(sat_conversion,[],[f2085]) ).
cnf(s205,plain,
( ~ spl0_11
| spl0_34
| ~ spl0_50 ),
inference(sat_conversion,[],[f2826]) ).
cnf(s206,plain,
( ~ spl0_11
| ~ spl0_36
| ~ spl0_50 ),
inference(sat_conversion,[],[f2829]) ).
cnf(s217,plain,
~ spl0_13,
inference(sat_conversion,[],[f2866]) ).
cnf(s224,plain,
( ~ spl0_29
| ~ spl0_49
| spl0_50 ),
inference(sat_conversion,[],[f2890]) ).
cnf(s231,plain,
( ~ spl0_2
| ~ spl0_31
| spl0_46 ),
inference(sat_conversion,[],[f2960]) ).
cnf(s233,plain,
( ~ spl0_2
| ~ spl0_26
| ~ spl0_31
| spl0_49 ),
inference(sat_conversion,[],[f2964]) ).
cnf(s240,plain,
( ~ spl0_5
| ~ spl0_28
| ~ spl0_31 ),
inference(sat_conversion,[],[f3115]) ).
cnf(s251,plain,
( ~ spl0_3
| ~ spl0_7
| spl0_19
| spl0_39
| spl0_43 ),
inference(sat_conversion,[],[f3644]) ).
cnf(s253,plain,
( ~ spl0_3
| ~ spl0_7
| spl0_9
| spl0_19
| spl0_43 ),
inference(sat_conversion,[],[f3646]) ).
cnf(s254,plain,
( ~ spl0_3
| ~ spl0_7
| spl0_9
| spl0_15
| spl0_19 ),
inference(sat_conversion,[],[f3647]) ).
cnf(s272,plain,
( ~ spl0_14
| ~ spl0_18 ),
inference(sat_conversion,[],[f3750]) ).
cnf(s305,plain,
( ~ spl0_5
| ~ spl0_28
| ~ spl0_30 ),
inference(sat_conversion,[],[f4782]) ).
cnf(s313,plain,
( ~ spl0_28
| ~ spl0_49
| spl0_50 ),
inference(sat_conversion,[],[f4795]) ).
cnf(s323,plain,
( spl0_5
| ~ spl0_6
| spl0_12
| spl0_35
| spl0_37 ),
inference(sat_conversion,[],[f4813]) ).
cnf(s324,plain,
( spl0_5
| ~ spl0_6
| spl0_12
| spl0_17
| spl0_35 ),
inference(sat_conversion,[],[f4814]) ).
cnf(s334,plain,
( ~ spl0_34
| ~ spl0_36 ),
inference(sat_conversion,[],[f4919]) ).
cnf(s336,plain,
( ~ spl0_20
| ~ spl0_34
| spl0_161
| spl0_162 ),
inference(sat_conversion,[],[f5055]) ).
cnf(s337,plain,
~ spl0_161,
inference(sat_conversion,[],[f5058]) ).
cnf(s381,plain,
( ~ spl0_18
| ~ spl0_40
| spl0_216
| spl0_217 ),
inference(sat_conversion,[],[f5873]) ).
cnf(s420,plain,
~ spl0_216,
inference(sat_conversion,[],[f6039]) ).
cnf(s464,plain,
~ spl0_162,
inference(sat_conversion,[],[f6704]) ).
cnf(s468,plain,
( spl0_20
| ~ spl0_32
| ~ spl0_50 ),
inference(sat_conversion,[],[f6711]) ).
cnf(s474,plain,
( ~ spl0_5
| ~ spl0_29
| spl0_102 ),
inference(sat_conversion,[],[f6889]) ).
cnf(s487,plain,
( ~ spl0_29
| ~ spl0_30
| ~ spl0_102 ),
inference(sat_conversion,[],[f7017]) ).
cnf(s667,plain,
~ spl0_217,
inference(sat_conversion,[],[f11541]) ).
cnf(s951,plain,
( spl0_18
| ~ spl0_42 ),
inference(sat_conversion,[],[f16880]) ).
cnf(s954,plain,
( ~ spl0_2
| ~ spl0_26
| ~ spl0_30
| spl0_49 ),
inference(sat_conversion,[],[f16884]) ).
cnf(s1368,plain,
( ~ spl0_16
| ~ spl0_36
| ~ spl0_50 ),
inference(sat_conversion,[],[f22551]) ).
cnf(s1369,plain,
( ~ spl0_18
| ~ spl0_40 ),
inference(rat,[],[s381,s667,s420]) ).
cnf(s1370,plain,
( ~ spl0_20
| ~ spl0_34 ),
inference(rat,[],[s336,s464,s337]) ).
cnf(s1371,plain,
( spl0_42
| ~ spl0_43 ),
inference(rat,[],[s22,s103]) ).
cnf(s1372,plain,
( spl0_40
| ~ spl0_41 ),
inference(rat,[],[s21,s103]) ).
cnf(s1373,plain,
( spl0_38
| ~ spl0_39 ),
inference(rat,[],[s20,s103]) ).
cnf(s1374,plain,
( spl0_36
| ~ spl0_37 ),
inference(rat,[],[s19,s217]) ).
cnf(s1375,plain,
( spl0_34
| ~ spl0_35 ),
inference(rat,[],[s18,s217]) ).
cnf(s1376,plain,
( spl0_32
| ~ spl0_33 ),
inference(rat,[],[s17,s217]) ).
cnf(s1377,plain,
( spl0_20
| ~ spl0_21 ),
inference(rat,[],[s11,s217]) ).
cnf(s1378,plain,
( spl0_18
| ~ spl0_19 ),
inference(rat,[],[s10,s103]) ).
cnf(s1379,plain,
( spl0_16
| ~ spl0_17 ),
inference(rat,[],[s9,s217]) ).
cnf(s1380,plain,
( spl0_14
| ~ spl0_15 ),
inference(rat,[],[s8,s103]) ).
cnf(s1381,plain,
( spl0_11
| ~ spl0_12 ),
inference(rat,[],[s7,s217]) ).
cnf(s1382,plain,
( spl0_8
| ~ spl0_9 ),
inference(rat,[],[s6,s103]) ).
cnf(s1389,plain,
( spl0_2
| spl0_7 ),
inference(rat,[],[s4,s5]) ).
cnf(s1396,plain,
( spl0_15
| spl0_9
| ~ spl0_7 ),
inference(rat,[],[s1369,s1372,s1378,s100,s254,s5]) ).
cnf(s1397,plain,
( spl0_9
| ~ spl0_7 ),
inference(rat,[],[s253,s1371,s1378,s951,s272,s1380,s1396,s5]) ).
cnf(s1398,plain,
~ spl0_7,
inference(rat,[],[s251,s1373,s1371,s1378,s104,s107,s108,s1382,s1397,s5]) ).
cnf(s1399,plain,
spl0_2,
inference(rat,[],[s1389,s1398]) ).
cnf(s1404,plain,
( spl0_49
| ~ spl0_26 ),
inference(rat,[],[s16,s233,s954,s1399]) ).
cnf(s1405,plain,
( ~ spl0_49
| spl0_50 ),
inference(rat,[],[s15,s224,s313]) ).
cnf(s1407,plain,
spl0_46,
inference(rat,[],[s23,s111,s120,s16,s231,s5,s1399]) ).
cnf(s1409,plain,
spl0_49,
inference(rat,[],[s14,s129,s1404,s1407]) ).
cnf(s1410,plain,
spl0_50,
inference(rat,[],[s1405,s1409]) ).
cnf(s1415,plain,
( ~ spl0_28
| ~ spl0_5 ),
inference(rat,[],[s16,s240,s305]) ).
cnf(s1416,plain,
( ~ spl0_29
| ~ spl0_5 ),
inference(rat,[],[s16,s91,s487,s87,s474]) ).
cnf(s1417,plain,
~ spl0_5,
inference(rat,[],[s1416,s15,s1415]) ).
cnf(s1421,plain,
( spl0_20
| spl0_37 ),
inference(rat,[],[s1376,s152,s468,s1377,s3,s1417,s1410]) ).
cnf(s1422,plain,
spl0_37,
inference(rat,[],[s323,s1381,s1375,s205,s1370,s1421,s3,s1417,s1410]) ).
cnf(s1423,plain,
spl0_36,
inference(rat,[],[s1374,s1422]) ).
cnf(s1424,plain,
~ spl0_16,
inference(rat,[],[s1368,s1410,s1423]) ).
cnf(s1425,plain,
~ spl0_34,
inference(rat,[],[s334,s1423]) ).
cnf(s1426,plain,
~ spl0_11,
inference(rat,[],[s206,s1410,s1423]) ).
cnf(s1427,plain,
~ spl0_17,
inference(rat,[],[s1379,s1424]) ).
cnf(s1428,plain,
~ spl0_35,
inference(rat,[],[s1375,s1425]) ).
cnf(s1429,plain,
~ spl0_12,
inference(rat,[],[s1381,s1426]) ).
cnf(s1430,plain,
$false,
inference(rat,[],[s324,s1429,s1417,s3,s1427,s1428]) ).
fof(f22552,plain,
$false,
inference(avatar_sat_refutation,[],[s1430]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT035-2 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 % Computer : n019.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 17:22:49 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.60/0.92 % (3286783)Will run a generic schedule for satisfiability detection.
% 2.60/0.92 % (3286793)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1195335837:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.60/0.92 % (3286789)% WARNING: option uhcvi not known.
% 2.60/0.92 % (3286791)dis+10_1_sil=32000:sp=arity:random_seed=1929756836:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.60/0.92 % (3286788)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2397916400_2999 on theBenchmark for (2999ds/0Mi)
% 2.60/0.92 % (3286789)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4025368208:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.60/0.92 % (3286790)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4272135270:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.60/0.92 % (3286792)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1613556382:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.60/0.92 % (3286794)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1714999159:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.60/0.92 % TRYING [1]
% 2.60/0.92 % TRYING [2]
% 2.60/0.92 % TRYING [3]
% 2.60/0.92 % TRYING [4]
% 2.60/0.92 % (3286793)Instruction limit reached!
% 2.60/0.92 % (3286793)------------------------------
% 2.60/0.92 % (3286793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.92 % (3286793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.92 % (3286793)CaDiCaL version: 2.1.3
% 2.60/0.92 % (3286793)Termination reason: Instruction limit
% 2.60/0.92 % (3286793)Termination phase: Saturation
% 2.60/0.92 % (3286793)Time elapsed: 0.043 s
% 2.60/0.92 % (3286793)Peak memory usage: 12 MB
% 2.60/0.92 % (3286793)Instructions burned: 133 (million)
% 2.60/0.92 % (3286802)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2671032849:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.60/0.92 % TRYING [1]
% 2.60/0.92 % TRYING [2]
% 2.60/0.92 % TRYING [3]
% 2.60/0.92 % (3286792)Instruction limit reached!
% 2.60/0.92 % (3286792)------------------------------
% 2.60/0.92 % (3286792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.92 % (3286792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.92 % (3286792)CaDiCaL version: 2.1.3
% 2.60/0.92 % (3286792)Termination reason: Instruction limit
% 2.60/0.92 % (3286792)Termination phase: Saturation
% 2.60/0.92 % (3286792)Time elapsed: 0.058 s
% 2.60/0.92 % (3286792)Peak memory usage: 11 MB
% 2.60/0.92 % (3286792)Instructions burned: 117 (million)
% 2.60/0.92 % (3286791)Instruction limit reached!
% 2.60/0.92 % (3286791)------------------------------
% 2.60/0.92 % (3286791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.92 % (3286791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.92 % (3286791)CaDiCaL version: 2.1.3
% 2.60/0.92 % (3286791)Termination reason: Instruction limit
% 2.60/0.92 % (3286791)Termination phase: Saturation
% 2.60/0.92 % (3286791)Time elapsed: 0.065 s
% 2.60/0.92 % (3286791)Peak memory usage: 12 MB
% 2.60/0.92 % (3286791)Instructions burned: 107 (million)
% 2.60/0.92 % (3286794)Instruction limit reached!
% 2.60/0.92 % (3286794)------------------------------
% 2.60/0.92 % (3286794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.92 % (3286794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.92 % (3286794)CaDiCaL version: 2.1.3
% 2.60/0.92 % (3286794)Termination reason: Instruction limit
% 2.60/0.92 % (3286794)Termination phase: Saturation
% 2.60/0.92 % (3286794)Time elapsed: 0.071 s
% 2.60/0.92 % (3286794)Peak memory usage: 11 MB
% 2.60/0.92 % (3286794)Instructions burned: 159 (million)
% 2.60/0.92 % (3286804)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3147126055:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.60/0.92 % (3286805)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2400130553:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 2.60/0.92 % (3286806)ott-21_1_sil=16000:fs=off:random_seed=4073722652:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.60/0.92 % TRYING [4]
% 2.60/0.92 % TRYING [5]
% 2.60/0.92 % (3286804)Instruction limit reached!
% 2.60/0.92 % (3286804)------------------------------
% 2.60/0.92 % (3286804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.92 % (3286804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.92 % (3286804)CaDiCaL version: 2.1.3
% 2.60/0.92 % (3286804)Termination reason: Instruction limit
% 2.60/0.92 % (3286804)Termination phase: Saturation
% 2.60/0.92 % (3286804)Time elapsed: 0.080 s
% 2.60/0.92 % (3286804)Peak memory usage: 12 MB
% 2.60/0.92 % (3286804)Instructions burned: 131 (million)
% 2.60/0.92 % (3286810)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3779792430:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 2.60/0.92 % (3286806)Instruction limit reached!
% 2.60/0.92 % (3286806)------------------------------
% 2.60/0.92 % (3286806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.92 % (3286806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.92 % (3286806)CaDiCaL version: 2.1.3
% 2.60/0.92 % (3286806)Termination reason: Instruction limit
% 2.60/0.92 % (3286806)Termination phase: Saturation
% 2.60/0.92 % (3286806)Time elapsed: 0.093 s
% 2.60/0.92 % (3286806)Peak memory usage: 12 MB
% 2.60/0.92 % (3286806)Instructions burned: 180 (million)
% 2.60/0.92 % (3286812)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=605169983:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 2.60/0.92 % TRYING [1]
% 2.60/0.92 % TRYING [2]
% 2.60/0.92 % TRYING [3]
% 2.60/0.92 % TRYING [4]
% 2.60/0.92 % (3286802)Instruction limit reached!
% 2.60/0.92 % (3286802)------------------------------
% 2.60/0.92 % (3286802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.92 % (3286802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.92 % (3286802)CaDiCaL version: 2.1.3
% 2.60/0.92 % (3286802)Termination reason: Instruction limit
% 2.60/0.92 % (3286802)Termination phase: Finite model building SAT solving
% 2.60/0.92 % (3286802)Time elapsed: 0.212 s
% 2.60/0.92 % (3286802)Peak memory usage: 14 MB
% 2.60/0.92 % (3286802)Instructions burned: 715 (million)
% 2.60/0.92 % TRYING [5]
% 2.60/0.92 % (3286814)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1075274232:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 2.60/0.92 % (3286805)Instruction limit reached!
% 2.60/0.92 % (3286805)------------------------------
% 2.60/0.92 % (3286805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.92 % (3286805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.92 % (3286805)CaDiCaL version: 2.1.3
% 2.60/0.92 % (3286805)Termination reason: Instruction limit
% 2.60/0.92 % (3286805)Termination phase: Saturation
% 2.60/0.92 % (3286805)Time elapsed: 0.321 s
% 2.60/0.92 % (3286805)Peak memory usage: 20 MB
% 2.60/0.92 % (3286805)Instructions burned: 685 (million)
% 2.60/0.92 % (3286816)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3481058502:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 2.60/0.92 % (3286814) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3286783-3286814"...
% 2.60/0.92 % (3286814)...printing done.
% 2.60/0.92 % (3286814)Refutation found. Thanks to Tanya!
% 2.60/0.92 % SZS status Unsatisfiable for theBenchmark
% 2.60/0.92 % SZS output start Proof for theBenchmark
% See solution above
% 2.60/0.93 % (3286814)------------------------------
% 2.60/0.93 % (3286814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.93 % (3286814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.93 % (3286814)CaDiCaL version: 2.1.3
% 2.60/0.93 % (3286814)Termination reason: Refutation
% 2.60/0.93 % (3286814)Time elapsed: 0.179 s
% 2.60/0.93 % (3286814)Peak memory usage: 18 MB
% 2.60/0.93 % (3286814)Instructions burned: 609 (million)
% 2.60/0.93 % (3286783)Success in time 0.494 s
% 2.60/0.93 % Vampire exiting
%------------------------------------------------------------------------------