%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : MGT039+2 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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:10 PM UTC 2026
% Result : Theorem 5.85s 1.75s
% Output : Refutation 7.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 71
% Syntax : Number of formulae : 378 ( 53 unt; 49 def)
% Number of atoms : 1198 ( 50 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 1494 ( 674 ~; 698 |; 53 &)
% ( 50 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 61 ( 59 usr; 50 prp; 0-4 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-2 aty)
% Number of variables : 219 ( 0 sgn 212 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2,X3] :
( ( environment(X0)
& subpopulations(X1,X2,X0,X3)
& greater(growth_rate(X2,X3),growth_rate(X1,X3)) )
=> selection_favors(X2,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp1_high_growth_rates) ).
fof(f2,axiom,
! [X0,X1,X2,X3] :
( ( environment(X0)
& subpopulation(X1,X0,X3)
& subpopulation(X2,X0,X3)
& greater(cardinality_at_time(X1,X3),zero)
& cardinality_at_time(X2,X3) = zero )
=> selection_favors(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp2_favour_members) ).
fof(f3,axiom,
! [X0] :
( ( observational_period(X0)
& propagation_strategy(first_movers)
& propagation_strategy(efficient_producers)
& ! [X1] :
( ( environment(X1)
& in_environment(X0,X1) )
=> selection_favors(efficient_producers,first_movers,end_time(X1)) ) )
=> selection_favors(efficient_producers,first_movers,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp3_favoured_trategy) ).
fof(f4,axiom,
! [X0] :
( ( observational_period(X0)
& slow_change(X0) )
=> ! [X1] :
( ( environment(X1)
& in_environment(X0,X1) )
=> ? [X2] :
( in_environment(X1,X2)
& greater(X2,critical_point(X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp4_critical_point) ).
fof(f5,axiom,
propagation_strategy(first_movers),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_organizational_sets1) ).
fof(f6,axiom,
propagation_strategy(efficient_producers),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_organizational_sets2) ).
fof(f7,axiom,
! [X0,X1] :
( ( environment(X0)
& greater_or_equal(X1,start_time(X0))
& greater_or_equal(end_time(X0),X1) )
=> in_environment(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_time_in_environment) ).
fof(f8,axiom,
! [X0,X1] :
( ( environment(X0)
& in_environment(X0,X1) )
=> greater_or_equal(end_time(X0),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_environment_end_point) ).
fof(f9,axiom,
! [X0,X1] :
( ( environment(X0)
& in_environment(X0,X1)
& greater(cardinality_at_time(first_movers,X1),zero)
& greater(cardinality_at_time(efficient_producers,X1),zero) )
=> subpopulations(first_movers,efficient_producers,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_contains_FM_and_EP) ).
fof(f10,axiom,
! [X0,X1] :
( ( environment(X0)
& in_environment(X0,X1) )
=> greater_or_equal(cardinality_at_time(first_movers,X1),zero) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_first_movers_exist) ).
fof(f11,axiom,
! [X0,X1] :
( ( environment(X0)
& in_environment(X0,X1) )
=> ( subpopulation(first_movers,X0,X1)
& subpopulation(efficient_producers,X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_subpopulations) ).
fof(f12,axiom,
! [X0] :
( environment(X0)
=> greater_or_equal(critical_point(X0),appear(efficient_producers,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_critical_point_after_EP) ).
fof(f13,axiom,
! [X0] :
( environment(X0)
=> greater_or_equal(critical_point(X0),start_time(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_time_of_critical_point) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( greater(X0,X1)
& greater(X1,X2) )
=> greater(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_transitivity) ).
fof(f16,axiom,
! [X0,X1] :
( greater_or_equal(X0,X1)
<=> ( greater(X0,X1)
| X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal) ).
fof(f17,axiom,
! [X0,X1] :
( ( environment(X0)
& X1 = critical_point(X0) )
=> ( ~ greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
& ! [X2] :
( ( subpopulations(first_movers,efficient_producers,X0,X2)
& greater(X2,X1) )
=> greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1) ).
fof(f18,axiom,
! [X0,X1] :
( ( environment(X0)
& in_environment(X0,X1)
& greater_or_equal(X1,appear(efficient_producers,X0)) )
=> greater(cardinality_at_time(efficient_producers,X1),zero) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6) ).
fof(f19,conjecture,
! [X0] :
( ( observational_period(X0)
& slow_change(X0) )
=> selection_favors(efficient_producers,first_movers,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t8) ).
fof(f20,negated_conjecture,
~ ! [X0] :
( ( observational_period(X0)
& slow_change(X0) )
=> selection_favors(efficient_producers,first_movers,X0) ),
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f21,plain,
! [X0,X1,X2,X3] :
( selection_favors(X2,X1,X3)
| ~ environment(X0)
| ~ subpopulations(X1,X2,X0,X3)
| ~ greater(growth_rate(X2,X3),growth_rate(X1,X3)) ),
inference(ennf_transformation,[],[f1]) ).
fof(f22,plain,
! [X0,X1,X2,X3] :
( selection_favors(X2,X1,X3)
| ~ environment(X0)
| ~ subpopulations(X1,X2,X0,X3)
| ~ greater(growth_rate(X2,X3),growth_rate(X1,X3)) ),
inference(flattening,[],[f21]) ).
fof(f23,plain,
! [X0,X1,X2,X3] :
( selection_favors(X1,X2,X3)
| ~ environment(X0)
| ~ subpopulation(X1,X0,X3)
| ~ subpopulation(X2,X0,X3)
| ~ greater(cardinality_at_time(X1,X3),zero)
| zero != cardinality_at_time(X2,X3) ),
inference(ennf_transformation,[],[f2]) ).
fof(f24,plain,
! [X0,X1,X2,X3] :
( selection_favors(X1,X2,X3)
| ~ environment(X0)
| ~ subpopulation(X1,X0,X3)
| ~ subpopulation(X2,X0,X3)
| ~ greater(cardinality_at_time(X1,X3),zero)
| zero != cardinality_at_time(X2,X3) ),
inference(flattening,[],[f23]) ).
fof(f25,plain,
! [X0] :
( selection_favors(efficient_producers,first_movers,X0)
| ~ observational_period(X0)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| ? [X1] :
( ~ selection_favors(efficient_producers,first_movers,end_time(X1))
& environment(X1)
& in_environment(X0,X1) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f26,plain,
! [X0] :
( selection_favors(efficient_producers,first_movers,X0)
| ~ observational_period(X0)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| ? [X1] :
( ~ selection_favors(efficient_producers,first_movers,end_time(X1))
& environment(X1)
& in_environment(X0,X1) ) ),
inference(flattening,[],[f25]) ).
fof(f27,plain,
! [X0] :
( ! [X1] :
( ? [X2] :
( in_environment(X1,X2)
& greater(X2,critical_point(X1)) )
| ~ environment(X1)
| ~ in_environment(X0,X1) )
| ~ observational_period(X0)
| ~ slow_change(X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f28,plain,
! [X0] :
( ! [X1] :
( ? [X2] :
( in_environment(X1,X2)
& greater(X2,critical_point(X1)) )
| ~ environment(X1)
| ~ in_environment(X0,X1) )
| ~ observational_period(X0)
| ~ slow_change(X0) ),
inference(flattening,[],[f27]) ).
fof(f29,plain,
! [X0,X1] :
( in_environment(X0,X1)
| ~ environment(X0)
| ~ greater_or_equal(X1,start_time(X0))
| ~ greater_or_equal(end_time(X0),X1) ),
inference(ennf_transformation,[],[f7]) ).
fof(f30,plain,
! [X0,X1] :
( in_environment(X0,X1)
| ~ environment(X0)
| ~ greater_or_equal(X1,start_time(X0))
| ~ greater_or_equal(end_time(X0),X1) ),
inference(flattening,[],[f29]) ).
fof(f31,plain,
! [X0,X1] :
( greater_or_equal(end_time(X0),X1)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f32,plain,
! [X0,X1] :
( greater_or_equal(end_time(X0),X1)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(flattening,[],[f31]) ).
fof(f33,plain,
! [X0,X1] :
( subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| ~ in_environment(X0,X1)
| ~ greater(cardinality_at_time(first_movers,X1),zero)
| ~ greater(cardinality_at_time(efficient_producers,X1),zero) ),
inference(ennf_transformation,[],[f9]) ).
fof(f34,plain,
! [X0,X1] :
( subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| ~ in_environment(X0,X1)
| ~ greater(cardinality_at_time(first_movers,X1),zero)
| ~ greater(cardinality_at_time(efficient_producers,X1),zero) ),
inference(flattening,[],[f33]) ).
fof(f35,plain,
! [X0,X1] :
( greater_or_equal(cardinality_at_time(first_movers,X1),zero)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f36,plain,
! [X0,X1] :
( greater_or_equal(cardinality_at_time(first_movers,X1),zero)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(flattening,[],[f35]) ).
fof(f37,plain,
! [X0,X1] :
( ( subpopulation(first_movers,X0,X1)
& subpopulation(efficient_producers,X0,X1) )
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f38,plain,
! [X0,X1] :
( ( subpopulation(first_movers,X0,X1)
& subpopulation(efficient_producers,X0,X1) )
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(flattening,[],[f37]) ).
fof(f39,plain,
! [X0] :
( greater_or_equal(critical_point(X0),appear(efficient_producers,X0))
| ~ environment(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f40,plain,
! [X0] :
( greater_or_equal(critical_point(X0),start_time(X0))
| ~ environment(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f41,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X0,X1)
| ~ greater(X1,X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f42,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X0,X1)
| ~ greater(X1,X2) ),
inference(flattening,[],[f41]) ).
fof(f45,plain,
! [X0,X1] :
( ( ~ greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
& ! [X2] :
( greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| ~ greater(X2,X1) ) )
| ~ environment(X0)
| critical_point(X0) != X1 ),
inference(ennf_transformation,[],[f17]) ).
fof(f46,plain,
! [X0,X1] :
( ( ~ greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
& ! [X2] :
( greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| ~ greater(X2,X1) ) )
| ~ environment(X0)
| critical_point(X0) != X1 ),
inference(flattening,[],[f45]) ).
fof(f47,plain,
! [X0,X1] :
( greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ environment(X0)
| ~ in_environment(X0,X1)
| ~ greater_or_equal(X1,appear(efficient_producers,X0)) ),
inference(ennf_transformation,[],[f18]) ).
fof(f48,plain,
! [X0,X1] :
( greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ environment(X0)
| ~ in_environment(X0,X1)
| ~ greater_or_equal(X1,appear(efficient_producers,X0)) ),
inference(flattening,[],[f47]) ).
fof(f49,plain,
? [X0] :
( ~ selection_favors(efficient_producers,first_movers,X0)
& observational_period(X0)
& slow_change(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f50,plain,
? [X0] :
( ~ selection_favors(efficient_producers,first_movers,X0)
& observational_period(X0)
& slow_change(X0) ),
inference(flattening,[],[f49]) ).
fof(f51,plain,
! [X0] :
( selection_favors(efficient_producers,first_movers,X0)
| ~ observational_period(X0)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| ( ~ selection_favors(efficient_producers,first_movers,end_time(sK0(X0)))
& environment(sK0(X0))
& in_environment(X0,sK0(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X1,sK0(X0))],[f26]) ).
fof(f52,plain,
! [X0] :
( ! [X1] :
( ( in_environment(X1,sK1(X1))
& greater(sK1(X1),critical_point(X1)) )
| ~ environment(X1)
| ~ in_environment(X0,X1) )
| ~ observational_period(X0)
| ~ slow_change(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X1))],[f28]) ).
fof(f53,plain,
! [X0,X1] :
( ( greater_or_equal(X0,X1)
| ( ~ greater(X0,X1)
& X0 != X1 ) )
& ( greater(X0,X1)
| X0 = X1
| ~ greater_or_equal(X0,X1) ) ),
inference(nnf_transformation,[],[f16]) ).
fof(f54,plain,
! [X0,X1] :
( ( greater_or_equal(X0,X1)
| ( ~ greater(X0,X1)
& X0 != X1 ) )
& ( greater(X0,X1)
| X0 = X1
| ~ greater_or_equal(X0,X1) ) ),
inference(flattening,[],[f53]) ).
fof(f55,plain,
( ~ selection_favors(efficient_producers,first_movers,sK2)
& observational_period(sK2)
& slow_change(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X0,sK2)],[f50]) ).
fof(f56,plain,
! [X2,X3,X0,X1] :
( selection_favors(X2,X1,X3)
| ~ environment(X0)
| ~ subpopulations(X1,X2,X0,X3)
| ~ greater(growth_rate(X2,X3),growth_rate(X1,X3)) ),
inference(cnf_transformation,[],[f22]) ).
fof(f57,plain,
! [X2,X3,X0,X1] :
( selection_favors(X1,X2,X3)
| ~ environment(X0)
| ~ subpopulation(X1,X0,X3)
| ~ subpopulation(X2,X0,X3)
| ~ greater(cardinality_at_time(X1,X3),zero)
| zero != cardinality_at_time(X2,X3) ),
inference(cnf_transformation,[],[f24]) ).
fof(f58,plain,
! [X0] :
( selection_favors(efficient_producers,first_movers,X0)
| ~ observational_period(X0)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| in_environment(X0,sK0(X0)) ),
inference(cnf_transformation,[],[f51]) ).
fof(f59,plain,
! [X0] :
( selection_favors(efficient_producers,first_movers,X0)
| ~ observational_period(X0)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| environment(sK0(X0)) ),
inference(cnf_transformation,[],[f51]) ).
fof(f60,plain,
! [X0] :
( selection_favors(efficient_producers,first_movers,X0)
| ~ observational_period(X0)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| ~ selection_favors(efficient_producers,first_movers,end_time(sK0(X0))) ),
inference(cnf_transformation,[],[f51]) ).
fof(f61,plain,
! [X0,X1] :
( greater(sK1(X1),critical_point(X1))
| ~ environment(X1)
| ~ in_environment(X0,X1)
| ~ observational_period(X0)
| ~ slow_change(X0) ),
inference(cnf_transformation,[],[f52]) ).
fof(f62,plain,
! [X0,X1] :
( in_environment(X1,sK1(X1))
| ~ environment(X1)
| ~ in_environment(X0,X1)
| ~ observational_period(X0)
| ~ slow_change(X0) ),
inference(cnf_transformation,[],[f52]) ).
fof(f63,plain,
propagation_strategy(first_movers),
inference(cnf_transformation,[],[f5]) ).
fof(f64,plain,
propagation_strategy(efficient_producers),
inference(cnf_transformation,[],[f6]) ).
fof(f65,plain,
! [X0,X1] :
( in_environment(X0,X1)
| ~ environment(X0)
| ~ greater_or_equal(X1,start_time(X0))
| ~ greater_or_equal(end_time(X0),X1) ),
inference(cnf_transformation,[],[f30]) ).
fof(f66,plain,
! [X0,X1] :
( greater_or_equal(end_time(X0),X1)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f32]) ).
fof(f67,plain,
! [X0,X1] :
( subpopulations(first_movers,efficient_producers,X0,X1)
| ~ environment(X0)
| ~ in_environment(X0,X1)
| ~ greater(cardinality_at_time(first_movers,X1),zero)
| ~ greater(cardinality_at_time(efficient_producers,X1),zero) ),
inference(cnf_transformation,[],[f34]) ).
fof(f68,plain,
! [X0,X1] :
( greater_or_equal(cardinality_at_time(first_movers,X1),zero)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f36]) ).
fof(f69,plain,
! [X0,X1] :
( subpopulation(efficient_producers,X0,X1)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f38]) ).
fof(f70,plain,
! [X0,X1] :
( subpopulation(first_movers,X0,X1)
| ~ environment(X0)
| ~ in_environment(X0,X1) ),
inference(cnf_transformation,[],[f38]) ).
fof(f71,plain,
! [X0] :
( greater_or_equal(critical_point(X0),appear(efficient_producers,X0))
| ~ environment(X0) ),
inference(cnf_transformation,[],[f39]) ).
fof(f72,plain,
! [X0] :
( greater_or_equal(critical_point(X0),start_time(X0))
| ~ environment(X0) ),
inference(cnf_transformation,[],[f40]) ).
fof(f73,plain,
! [X2,X0,X1] :
( greater(X0,X2)
| ~ greater(X0,X1)
| ~ greater(X1,X2) ),
inference(cnf_transformation,[],[f42]) ).
fof(f75,plain,
! [X0,X1] :
( greater(X0,X1)
| X0 = X1
| ~ greater_or_equal(X0,X1) ),
inference(cnf_transformation,[],[f54]) ).
fof(f76,plain,
! [X0,X1] :
( greater_or_equal(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[],[f54]) ).
fof(f77,plain,
! [X0,X1] :
( greater_or_equal(X0,X1)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f54]) ).
fof(f78,plain,
! [X2,X0,X1] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,X2)
| ~ greater(X2,X1)
| greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2))
| critical_point(X0) != X1 ),
inference(cnf_transformation,[],[f46]) ).
fof(f80,plain,
! [X0,X1] :
( ~ environment(X0)
| greater(cardinality_at_time(efficient_producers,X1),zero)
| ~ in_environment(X0,X1)
| ~ greater_or_equal(X1,appear(efficient_producers,X0)) ),
inference(cnf_transformation,[],[f48]) ).
fof(f81,plain,
slow_change(sK2),
inference(cnf_transformation,[],[f55]) ).
fof(f82,plain,
observational_period(sK2),
inference(cnf_transformation,[],[f55]) ).
fof(f83,plain,
~ selection_favors(efficient_producers,first_movers,sK2),
inference(cnf_transformation,[],[f55]) ).
fof(f85,definition,
( spl3_1
<=> slow_change(sK2) ),
introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition]) ).
fof(f87,plain,
( slow_change(sK2)
| ~ spl3_1 ),
inference(avatar_component_clause,[],[f85]) ).
fof(f88,plain,
spl3_1,
inference(avatar_split_clause,[],[f81,f85]) ).
fof(f90,definition,
( spl3_2
<=> observational_period(sK2) ),
introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition]) ).
fof(f92,plain,
( observational_period(sK2)
| ~ spl3_2 ),
inference(avatar_component_clause,[],[f90]) ).
fof(f93,plain,
spl3_2,
inference(avatar_split_clause,[],[f82,f90]) ).
fof(f95,definition,
( spl3_3
<=> selection_favors(efficient_producers,first_movers,sK2) ),
introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition]) ).
fof(f97,plain,
( ~ selection_favors(efficient_producers,first_movers,sK2)
| spl3_3 ),
inference(avatar_component_clause,[],[f95]) ).
fof(f98,plain,
~ spl3_3,
inference(avatar_split_clause,[],[f83,f95]) ).
fof(f115,definition,
( spl3_6
<=> selection_favors(efficient_producers,first_movers,end_time(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_6])],[avatar_definition]) ).
fof(f117,plain,
( ~ selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| spl3_6 ),
inference(avatar_component_clause,[],[f115]) ).
fof(f119,definition,
( spl3_7
<=> propagation_strategy(efficient_producers) ),
introduced(definition,[new_symbols(definition,[spl3_7])],[avatar_definition]) ).
fof(f121,plain,
( ~ propagation_strategy(efficient_producers)
| spl3_7 ),
inference(avatar_component_clause,[],[f119]) ).
fof(f123,definition,
( spl3_8
<=> propagation_strategy(first_movers) ),
introduced(definition,[new_symbols(definition,[spl3_8])],[avatar_definition]) ).
fof(f125,plain,
( ~ propagation_strategy(first_movers)
| spl3_8 ),
inference(avatar_component_clause,[],[f123]) ).
fof(f128,definition,
( spl3_9
<=> environment(sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl3_9])],[avatar_definition]) ).
fof(f130,plain,
( environment(sK0(sK2))
| ~ spl3_9 ),
inference(avatar_component_clause,[],[f128]) ).
fof(f133,definition,
( spl3_10
<=> in_environment(sK2,sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl3_10])],[avatar_definition]) ).
fof(f135,plain,
( in_environment(sK2,sK0(sK2))
| ~ spl3_10 ),
inference(avatar_component_clause,[],[f133]) ).
fof(f139,plain,
( ~ observational_period(sK2)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| in_environment(sK2,sK0(sK2))
| spl3_3 ),
inference(resolution,[],[f97,f58]) ).
fof(f140,plain,
( ~ observational_period(sK2)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| environment(sK0(sK2))
| spl3_3 ),
inference(resolution,[],[f97,f59]) ).
fof(f141,plain,
( ~ observational_period(sK2)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| ~ selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| spl3_3 ),
inference(resolution,[],[f97,f60]) ).
fof(f164,plain,
( ~ spl3_6
| ~ spl3_7
| ~ spl3_8
| ~ spl3_2
| spl3_3 ),
inference(avatar_split_clause,[],[f141,f95,f90,f123,f119,f115]) ).
fof(f165,plain,
( spl3_9
| ~ spl3_7
| ~ spl3_8
| ~ spl3_2
| spl3_3 ),
inference(avatar_split_clause,[],[f140,f95,f90,f123,f119,f128]) ).
fof(f166,plain,
( spl3_10
| ~ spl3_7
| ~ spl3_8
| ~ spl3_2
| spl3_3 ),
inference(avatar_split_clause,[],[f139,f95,f90,f123,f119,f133]) ).
fof(f172,plain,
! [X0,X1] :
( greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ in_environment(sK0(X1),X0)
| ~ greater_or_equal(X0,appear(efficient_producers,sK0(X1)))
| selection_favors(efficient_producers,first_movers,X1)
| ~ observational_period(X1)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers) ),
inference(resolution,[],[f80,f59]) ).
fof(f174,definition,
( spl3_17
<=> ! [X0,X1] :
( greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ observational_period(X1)
| selection_favors(efficient_producers,first_movers,X1)
| ~ greater_or_equal(X0,appear(efficient_producers,sK0(X1)))
| ~ in_environment(sK0(X1),X0) ) ),
introduced(definition,[new_symbols(definition,[spl3_17])],[avatar_definition]) ).
fof(f175,plain,
( ! [X0,X1] :
( ~ observational_period(X1)
| greater(cardinality_at_time(efficient_producers,X0),zero)
| selection_favors(efficient_producers,first_movers,X1)
| ~ greater_or_equal(X0,appear(efficient_producers,sK0(X1)))
| ~ in_environment(sK0(X1),X0) )
| ~ spl3_17 ),
inference(avatar_component_clause,[],[f174]) ).
fof(f176,plain,
( ~ spl3_7
| ~ spl3_8
| spl3_17 ),
inference(avatar_split_clause,[],[f172,f174,f123,f119]) ).
fof(f177,plain,
! [X2,X0,X1] :
( ~ subpopulations(first_movers,efficient_producers,sK0(X0),X1)
| ~ greater(X1,X2)
| greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| critical_point(sK0(X0)) != X2
| selection_favors(efficient_producers,first_movers,X0)
| ~ observational_period(X0)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers) ),
inference(resolution,[],[f78,f59]) ).
fof(f179,definition,
( spl3_18
<=> ! [X2,X0,X1] :
( ~ subpopulations(first_movers,efficient_producers,sK0(X0),X1)
| ~ observational_period(X0)
| selection_favors(efficient_producers,first_movers,X0)
| critical_point(sK0(X0)) != X2
| greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ greater(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl3_18])],[avatar_definition]) ).
fof(f180,plain,
( ! [X2,X0,X1] :
( ~ observational_period(X0)
| ~ subpopulations(first_movers,efficient_producers,sK0(X0),X1)
| selection_favors(efficient_producers,first_movers,X0)
| critical_point(sK0(X0)) != X2
| greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ greater(X1,X2) )
| ~ spl3_18 ),
inference(avatar_component_clause,[],[f179]) ).
fof(f181,plain,
( ~ spl3_7
| ~ spl3_8
| spl3_18 ),
inference(avatar_split_clause,[],[f177,f179,f123,f119]) ).
fof(f182,plain,
( $false
| spl3_7 ),
inference(resolution,[],[f121,f64]) ).
fof(f183,plain,
spl3_7,
inference(avatar_contradiction_clause,[],[f182]) ).
fof(f184,plain,
( $false
| spl3_8 ),
inference(resolution,[],[f125,f63]) ).
fof(f185,plain,
spl3_8,
inference(avatar_contradiction_clause,[],[f184]) ).
fof(f190,plain,
( ! [X0] :
( ~ greater_or_equal(end_time(sK0(sK2)),X0)
| ~ greater_or_equal(X0,start_time(sK0(sK2)))
| in_environment(sK0(sK2),X0) )
| ~ spl3_9 ),
inference(resolution,[],[f130,f65]) ).
fof(f191,plain,
( ! [X0] :
( greater_or_equal(end_time(sK0(sK2)),X0)
| ~ in_environment(sK0(sK2),X0) )
| ~ spl3_9 ),
inference(resolution,[],[f130,f66]) ).
fof(f193,plain,
( ! [X0] :
( greater_or_equal(cardinality_at_time(first_movers,X0),zero)
| ~ in_environment(sK0(sK2),X0) )
| ~ spl3_9 ),
inference(resolution,[],[f130,f68]) ).
fof(f194,plain,
( ! [X0] :
( subpopulation(efficient_producers,sK0(sK2),X0)
| ~ in_environment(sK0(sK2),X0) )
| ~ spl3_9 ),
inference(resolution,[],[f130,f69]) ).
fof(f195,plain,
( ! [X0] :
( subpopulation(first_movers,sK0(sK2),X0)
| ~ in_environment(sK0(sK2),X0) )
| ~ spl3_9 ),
inference(resolution,[],[f130,f70]) ).
fof(f196,plain,
( greater_or_equal(critical_point(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| ~ spl3_9 ),
inference(resolution,[],[f130,f71]) ).
fof(f197,plain,
( greater_or_equal(critical_point(sK0(sK2)),start_time(sK0(sK2)))
| ~ spl3_9 ),
inference(resolution,[],[f130,f72]) ).
fof(f203,definition,
( spl3_19
<=> greater_or_equal(critical_point(sK0(sK2)),start_time(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_19])],[avatar_definition]) ).
fof(f205,plain,
( greater_or_equal(critical_point(sK0(sK2)),start_time(sK0(sK2)))
| ~ spl3_19 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f206,plain,
( spl3_19
| ~ spl3_9 ),
inference(avatar_split_clause,[],[f197,f128,f203]) ).
fof(f208,definition,
( spl3_20
<=> greater_or_equal(critical_point(sK0(sK2)),appear(efficient_producers,sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_20])],[avatar_definition]) ).
fof(f210,plain,
( greater_or_equal(critical_point(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| ~ spl3_20 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f211,plain,
( spl3_20
| ~ spl3_9 ),
inference(avatar_split_clause,[],[f196,f128,f208]) ).
fof(f213,definition,
( spl3_21
<=> ! [X0] :
( ~ in_environment(X0,sK0(sK2))
| ~ slow_change(X0)
| ~ observational_period(X0) ) ),
introduced(definition,[new_symbols(definition,[spl3_21])],[avatar_definition]) ).
fof(f214,plain,
( ! [X0] :
( ~ slow_change(X0)
| ~ in_environment(X0,sK0(sK2))
| ~ observational_period(X0) )
| ~ spl3_21 ),
inference(avatar_component_clause,[],[f213]) ).
fof(f216,definition,
( spl3_22
<=> in_environment(sK0(sK2),sK1(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_22])],[avatar_definition]) ).
fof(f218,plain,
( in_environment(sK0(sK2),sK1(sK0(sK2)))
| ~ spl3_22 ),
inference(avatar_component_clause,[],[f216]) ).
fof(f221,definition,
( spl3_23
<=> greater(sK1(sK0(sK2)),critical_point(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_23])],[avatar_definition]) ).
fof(f223,plain,
( greater(sK1(sK0(sK2)),critical_point(sK0(sK2)))
| ~ spl3_23 ),
inference(avatar_component_clause,[],[f221]) ).
fof(f225,plain,
( greater(sK1(sK0(sK2)),critical_point(sK0(sK2)))
| ~ environment(sK0(sK2))
| ~ observational_period(sK2)
| ~ slow_change(sK2)
| ~ spl3_10 ),
inference(resolution,[],[f135,f61]) ).
fof(f226,plain,
( in_environment(sK0(sK2),sK1(sK0(sK2)))
| ~ environment(sK0(sK2))
| ~ observational_period(sK2)
| ~ slow_change(sK2)
| ~ spl3_10 ),
inference(resolution,[],[f135,f62]) ).
fof(f269,plain,
( ~ spl3_1
| ~ spl3_2
| ~ spl3_9
| spl3_22
| ~ spl3_10 ),
inference(avatar_split_clause,[],[f226,f133,f216,f128,f90,f85]) ).
fof(f270,plain,
( ~ spl3_1
| ~ spl3_2
| ~ spl3_9
| spl3_23
| ~ spl3_10 ),
inference(avatar_split_clause,[],[f225,f133,f221,f128,f90,f85]) ).
fof(f286,plain,
( ! [X0] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,end_time(sK0(sK2)))
| ~ greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) )
| spl3_6 ),
inference(resolution,[],[f117,f56]) ).
fof(f288,definition,
( spl3_34
<=> greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2)))) ),
introduced(definition,[new_symbols(definition,[spl3_34])],[avatar_definition]) ).
fof(f292,definition,
( spl3_35
<=> ! [X0] :
( ~ environment(X0)
| ~ subpopulations(first_movers,efficient_producers,X0,end_time(sK0(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl3_35])],[avatar_definition]) ).
fof(f293,plain,
( ! [X0] :
( ~ subpopulations(first_movers,efficient_producers,X0,end_time(sK0(sK2)))
| ~ environment(X0) )
| ~ spl3_35 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f294,plain,
( ~ spl3_34
| spl3_35
| spl3_6 ),
inference(avatar_split_clause,[],[f286,f115,f292,f288]) ).
fof(f296,definition,
( spl3_36
<=> zero = cardinality_at_time(first_movers,end_time(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_36])],[avatar_definition]) ).
fof(f297,plain,
( zero = cardinality_at_time(first_movers,end_time(sK0(sK2)))
| ~ spl3_36 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f300,definition,
( spl3_37
<=> greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero) ),
introduced(definition,[new_symbols(definition,[spl3_37])],[avatar_definition]) ).
fof(f301,plain,
( greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ spl3_37 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f356,plain,
( ! [X0] :
( greater(cardinality_at_time(efficient_producers,X0),zero)
| selection_favors(efficient_producers,first_movers,sK2)
| ~ greater_or_equal(X0,appear(efficient_producers,sK0(sK2)))
| ~ in_environment(sK0(sK2),X0) )
| ~ spl3_2
| ~ spl3_17 ),
inference(resolution,[],[f175,f92]) ).
fof(f358,definition,
( spl3_48
<=> ! [X0] :
( greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ in_environment(sK0(sK2),X0)
| ~ greater_or_equal(X0,appear(efficient_producers,sK0(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl3_48])],[avatar_definition]) ).
fof(f359,plain,
( ! [X0] :
( ~ in_environment(sK0(sK2),X0)
| greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater_or_equal(X0,appear(efficient_producers,sK0(sK2))) )
| ~ spl3_48 ),
inference(avatar_component_clause,[],[f358]) ).
fof(f360,plain,
( spl3_3
| spl3_48
| ~ spl3_2
| ~ spl3_17 ),
inference(avatar_split_clause,[],[f356,f174,f90,f358,f95]) ).
fof(f361,plain,
( ! [X0,X1] :
( ~ subpopulations(first_movers,efficient_producers,sK0(sK2),X0)
| selection_favors(efficient_producers,first_movers,sK2)
| critical_point(sK0(sK2)) != X1
| greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| ~ greater(X0,X1) )
| ~ spl3_2
| ~ spl3_18 ),
inference(resolution,[],[f180,f92]) ).
fof(f363,definition,
( spl3_49
<=> ! [X0,X1] :
( ~ subpopulations(first_movers,efficient_producers,sK0(sK2),X0)
| ~ greater(X0,X1)
| greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| critical_point(sK0(sK2)) != X1 ) ),
introduced(definition,[new_symbols(definition,[spl3_49])],[avatar_definition]) ).
fof(f364,plain,
( ! [X0,X1] :
( ~ subpopulations(first_movers,efficient_producers,sK0(sK2),X0)
| ~ greater(X0,X1)
| greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| critical_point(sK0(sK2)) != X1 )
| ~ spl3_49 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f365,plain,
( spl3_3
| spl3_49
| ~ spl3_2
| ~ spl3_18 ),
inference(avatar_split_clause,[],[f361,f179,f90,f363,f95]) ).
fof(f371,plain,
( greater_or_equal(end_time(sK0(sK2)),sK1(sK0(sK2)))
| ~ environment(sK0(sK2))
| ~ spl3_22 ),
inference(resolution,[],[f218,f66]) ).
fof(f392,definition,
( spl3_53
<=> greater(cardinality_at_time(efficient_producers,sK1(sK0(sK2))),zero) ),
introduced(definition,[new_symbols(definition,[spl3_53])],[avatar_definition]) ).
fof(f405,definition,
( spl3_56
<=> greater_or_equal(end_time(sK0(sK2)),sK1(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_56])],[avatar_definition]) ).
fof(f407,plain,
( greater_or_equal(end_time(sK0(sK2)),sK1(sK0(sK2)))
| ~ spl3_56 ),
inference(avatar_component_clause,[],[f405]) ).
fof(f408,plain,
( ~ spl3_9
| spl3_56
| ~ spl3_22 ),
inference(avatar_split_clause,[],[f371,f216,f405,f128]) ).
fof(f432,plain,
( greater(critical_point(sK0(sK2)),start_time(sK0(sK2)))
| critical_point(sK0(sK2)) = start_time(sK0(sK2))
| ~ spl3_19 ),
inference(resolution,[],[f205,f75]) ).
fof(f434,definition,
( spl3_62
<=> critical_point(sK0(sK2)) = start_time(sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl3_62])],[avatar_definition]) ).
fof(f438,definition,
( spl3_63
<=> greater(critical_point(sK0(sK2)),start_time(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_63])],[avatar_definition]) ).
fof(f440,plain,
( greater(critical_point(sK0(sK2)),start_time(sK0(sK2)))
| ~ spl3_63 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f441,plain,
( spl3_62
| spl3_63
| ~ spl3_19 ),
inference(avatar_split_clause,[],[f432,f203,f438,f434]) ).
fof(f443,definition,
( spl3_64
<=> greater_or_equal(end_time(sK0(sK2)),critical_point(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_64])],[avatar_definition]) ).
fof(f445,plain,
( ~ greater_or_equal(end_time(sK0(sK2)),critical_point(sK0(sK2)))
| spl3_64 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f451,plain,
( greater_or_equal(sK1(sK0(sK2)),critical_point(sK0(sK2)))
| ~ spl3_23 ),
inference(resolution,[],[f223,f77]) ).
fof(f452,plain,
( ! [X0] :
( ~ greater(X0,sK1(sK0(sK2)))
| greater(X0,critical_point(sK0(sK2))) )
| ~ spl3_23 ),
inference(resolution,[],[f223,f73]) ).
fof(f453,plain,
( ! [X0] :
( ~ greater(critical_point(sK0(sK2)),X0)
| greater(sK1(sK0(sK2)),X0) )
| ~ spl3_23 ),
inference(resolution,[],[f223,f73]) ).
fof(f455,definition,
( spl3_66
<=> greater_or_equal(sK1(sK0(sK2)),critical_point(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_66])],[avatar_definition]) ).
fof(f458,plain,
( spl3_66
| ~ spl3_23 ),
inference(avatar_split_clause,[],[f451,f221,f455]) ).
fof(f462,plain,
( greater(critical_point(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| critical_point(sK0(sK2)) = appear(efficient_producers,sK0(sK2))
| ~ spl3_20 ),
inference(resolution,[],[f210,f75]) ).
fof(f464,definition,
( spl3_67
<=> critical_point(sK0(sK2)) = appear(efficient_producers,sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl3_67])],[avatar_definition]) ).
fof(f468,definition,
( spl3_68
<=> greater(critical_point(sK0(sK2)),appear(efficient_producers,sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_68])],[avatar_definition]) ).
fof(f470,plain,
( greater(critical_point(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| ~ spl3_68 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f471,plain,
( spl3_67
| spl3_68
| ~ spl3_20 ),
inference(avatar_split_clause,[],[f462,f208,f468,f464]) ).
fof(f472,plain,
( ~ in_environment(sK2,sK0(sK2))
| ~ observational_period(sK2)
| ~ spl3_1
| ~ spl3_21 ),
inference(resolution,[],[f214,f87]) ).
fof(f473,plain,
( ~ spl3_2
| ~ spl3_10
| ~ spl3_1
| ~ spl3_21 ),
inference(avatar_split_clause,[],[f472,f213,f85,f133,f90]) ).
fof(f479,plain,
( ! [X0] :
( ~ in_environment(sK0(sK2),X0)
| greater(cardinality_at_time(first_movers,X0),zero)
| zero = cardinality_at_time(first_movers,X0) )
| ~ spl3_9 ),
inference(resolution,[],[f193,f75]) ).
fof(f481,plain,
( ! [X0,X1] :
( ~ in_environment(sK0(sK2),X0)
| selection_favors(efficient_producers,X1,X0)
| ~ environment(sK0(sK2))
| ~ subpopulation(X1,sK0(sK2),X0)
| ~ greater(cardinality_at_time(efficient_producers,X0),zero)
| zero != cardinality_at_time(X1,X0) )
| ~ spl3_9 ),
inference(resolution,[],[f194,f57]) ).
fof(f483,definition,
( spl3_69
<=> ! [X0,X1] :
( ~ in_environment(sK0(sK2),X0)
| zero != cardinality_at_time(X1,X0)
| ~ greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ subpopulation(X1,sK0(sK2),X0)
| selection_favors(efficient_producers,X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl3_69])],[avatar_definition]) ).
fof(f484,plain,
( ! [X0,X1] :
( zero != cardinality_at_time(X1,X0)
| ~ in_environment(sK0(sK2),X0)
| ~ greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ subpopulation(X1,sK0(sK2),X0)
| selection_favors(efficient_producers,X1,X0) )
| ~ spl3_69 ),
inference(avatar_component_clause,[],[f483]) ).
fof(f485,plain,
( ~ spl3_9
| spl3_69
| ~ spl3_9 ),
inference(avatar_split_clause,[],[f481,f128,f483,f128]) ).
fof(f523,plain,
( ! [X0] :
( end_time(sK0(sK2)) != X0
| in_environment(sK0(sK2),X0)
| ~ greater_or_equal(X0,start_time(sK0(sK2))) )
| ~ spl3_9 ),
inference(resolution,[],[f190,f76]) ).
fof(f534,plain,
( ! [X0] :
( greater(cardinality_at_time(efficient_producers,sK1(sK0(sK2))),zero)
| ~ greater_or_equal(sK1(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| ~ environment(sK0(sK2))
| ~ in_environment(X0,sK0(sK2))
| ~ observational_period(X0)
| ~ slow_change(X0) )
| ~ spl3_48 ),
inference(resolution,[],[f359,f62]) ).
fof(f535,plain,
( ! [X0] :
( greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater_or_equal(X0,appear(efficient_producers,sK0(sK2)))
| ~ environment(sK0(sK2))
| ~ greater_or_equal(X0,start_time(sK0(sK2)))
| ~ greater_or_equal(end_time(sK0(sK2)),X0) )
| ~ spl3_48 ),
inference(resolution,[],[f359,f65]) ).
fof(f537,definition,
( spl3_77
<=> ! [X0] :
( greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater_or_equal(end_time(sK0(sK2)),X0)
| ~ greater_or_equal(X0,start_time(sK0(sK2)))
| ~ greater_or_equal(X0,appear(efficient_producers,sK0(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl3_77])],[avatar_definition]) ).
fof(f538,plain,
( ! [X0] :
( ~ greater_or_equal(end_time(sK0(sK2)),X0)
| greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater_or_equal(X0,start_time(sK0(sK2)))
| ~ greater_or_equal(X0,appear(efficient_producers,sK0(sK2))) )
| ~ spl3_77 ),
inference(avatar_component_clause,[],[f537]) ).
fof(f539,plain,
( ~ spl3_9
| spl3_77
| ~ spl3_48 ),
inference(avatar_split_clause,[],[f535,f358,f537,f128]) ).
fof(f541,definition,
( spl3_78
<=> greater_or_equal(sK1(sK0(sK2)),appear(efficient_producers,sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_78])],[avatar_definition]) ).
fof(f543,plain,
( ~ greater_or_equal(sK1(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| spl3_78 ),
inference(avatar_component_clause,[],[f541]) ).
fof(f544,plain,
( spl3_21
| ~ spl3_9
| ~ spl3_78
| spl3_53
| ~ spl3_48 ),
inference(avatar_split_clause,[],[f534,f358,f392,f541,f128,f213]) ).
fof(f546,plain,
( critical_point(sK0(sK2)) != appear(efficient_producers,sK0(sK2))
| greater_or_equal(sK1(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| ~ greater_or_equal(sK1(sK0(sK2)),critical_point(sK0(sK2))) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f557,plain,
( ! [X0,X1] :
( ~ greater(X0,X1)
| greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))
| critical_point(sK0(sK2)) != X1
| ~ environment(sK0(sK2))
| ~ in_environment(sK0(sK2),X0)
| ~ greater(cardinality_at_time(first_movers,X0),zero)
| ~ greater(cardinality_at_time(efficient_producers,X0),zero) )
| ~ spl3_49 ),
inference(resolution,[],[f364,f67]) ).
fof(f559,definition,
( spl3_80
<=> ! [X0,X1] :
( ~ greater(X0,X1)
| ~ greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater(cardinality_at_time(first_movers,X0),zero)
| ~ in_environment(sK0(sK2),X0)
| critical_point(sK0(sK2)) != X1
| greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl3_80])],[avatar_definition]) ).
fof(f560,plain,
( ! [X0,X1] :
( critical_point(sK0(sK2)) != X1
| ~ greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater(cardinality_at_time(first_movers,X0),zero)
| ~ in_environment(sK0(sK2),X0)
| ~ greater(X0,X1)
| greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0)) )
| ~ spl3_80 ),
inference(avatar_component_clause,[],[f559]) ).
fof(f561,plain,
( ~ spl3_9
| spl3_80
| ~ spl3_49 ),
inference(avatar_split_clause,[],[f557,f363,f559,f128]) ).
fof(f612,plain,
( greater(end_time(sK0(sK2)),sK1(sK0(sK2)))
| end_time(sK0(sK2)) = sK1(sK0(sK2))
| ~ spl3_56 ),
inference(resolution,[],[f407,f75]) ).
fof(f614,definition,
( spl3_89
<=> end_time(sK0(sK2)) = sK1(sK0(sK2)) ),
introduced(definition,[new_symbols(definition,[spl3_89])],[avatar_definition]) ).
fof(f616,plain,
( end_time(sK0(sK2)) = sK1(sK0(sK2))
| ~ spl3_89 ),
inference(avatar_component_clause,[],[f614]) ).
fof(f618,definition,
( spl3_90
<=> greater(end_time(sK0(sK2)),sK1(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_90])],[avatar_definition]) ).
fof(f620,plain,
( greater(end_time(sK0(sK2)),sK1(sK0(sK2)))
| ~ spl3_90 ),
inference(avatar_component_clause,[],[f618]) ).
fof(f621,plain,
( spl3_89
| spl3_90
| ~ spl3_56 ),
inference(avatar_split_clause,[],[f612,f405,f618,f614]) ).
fof(f717,definition,
( spl3_102
<=> greater(end_time(sK0(sK2)),critical_point(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_102])],[avatar_definition]) ).
fof(f719,plain,
( greater(end_time(sK0(sK2)),critical_point(sK0(sK2)))
| ~ spl3_102 ),
inference(avatar_component_clause,[],[f717]) ).
fof(f743,plain,
( ~ greater(end_time(sK0(sK2)),critical_point(sK0(sK2)))
| spl3_64 ),
inference(resolution,[],[f445,f77]) ).
fof(f744,plain,
( ~ spl3_102
| spl3_64 ),
inference(avatar_split_clause,[],[f743,f443,f717]) ).
fof(f748,plain,
( ! [X0] :
( ~ greater(X0,critical_point(sK0(sK2)))
| greater(X0,appear(efficient_producers,sK0(sK2))) )
| ~ spl3_68 ),
inference(resolution,[],[f470,f73]) ).
fof(f751,plain,
( ~ greater(sK1(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| spl3_78 ),
inference(resolution,[],[f543,f77]) ).
fof(f753,definition,
( spl3_104
<=> greater(sK1(sK0(sK2)),appear(efficient_producers,sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_104])],[avatar_definition]) ).
fof(f756,plain,
( ~ spl3_104
| spl3_78 ),
inference(avatar_split_clause,[],[f751,f541,f753]) ).
fof(f764,plain,
( greater(sK1(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| ~ spl3_23
| ~ spl3_68 ),
inference(resolution,[],[f453,f470]) ).
fof(f768,plain,
( spl3_104
| ~ spl3_23
| ~ spl3_68 ),
inference(avatar_split_clause,[],[f764,f468,f221,f753]) ).
fof(f843,plain,
( ! [X0] :
( greater(cardinality_at_time(first_movers,X0),zero)
| zero = cardinality_at_time(first_movers,X0)
| ~ environment(sK0(sK2))
| ~ greater_or_equal(X0,start_time(sK0(sK2)))
| ~ greater_or_equal(end_time(sK0(sK2)),X0) )
| ~ spl3_9 ),
inference(resolution,[],[f479,f65]) ).
fof(f845,definition,
( spl3_113
<=> ! [X0] :
( greater(cardinality_at_time(first_movers,X0),zero)
| ~ greater_or_equal(end_time(sK0(sK2)),X0)
| ~ greater_or_equal(X0,start_time(sK0(sK2)))
| zero = cardinality_at_time(first_movers,X0) ) ),
introduced(definition,[new_symbols(definition,[spl3_113])],[avatar_definition]) ).
fof(f846,plain,
( ! [X0] :
( ~ greater_or_equal(X0,start_time(sK0(sK2)))
| ~ greater_or_equal(end_time(sK0(sK2)),X0)
| greater(cardinality_at_time(first_movers,X0),zero)
| zero = cardinality_at_time(first_movers,X0) )
| ~ spl3_113 ),
inference(avatar_component_clause,[],[f845]) ).
fof(f847,plain,
( ~ spl3_9
| spl3_113
| ~ spl3_9 ),
inference(avatar_split_clause,[],[f843,f128,f845,f128]) ).
fof(f850,plain,
( in_environment(sK0(sK2),end_time(sK0(sK2)))
| ~ greater_or_equal(end_time(sK0(sK2)),start_time(sK0(sK2)))
| ~ spl3_9 ),
inference(equality_resolution,[],[f523]) ).
fof(f852,definition,
( spl3_114
<=> greater_or_equal(end_time(sK0(sK2)),start_time(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_114])],[avatar_definition]) ).
fof(f854,plain,
( ~ greater_or_equal(end_time(sK0(sK2)),start_time(sK0(sK2)))
| spl3_114 ),
inference(avatar_component_clause,[],[f852]) ).
fof(f856,definition,
( spl3_115
<=> in_environment(sK0(sK2),end_time(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_115])],[avatar_definition]) ).
fof(f858,plain,
( in_environment(sK0(sK2),end_time(sK0(sK2)))
| ~ spl3_115 ),
inference(avatar_component_clause,[],[f856]) ).
fof(f859,plain,
( ~ spl3_114
| spl3_115
| ~ spl3_9 ),
inference(avatar_split_clause,[],[f850,f128,f856,f852]) ).
fof(f892,plain,
( ! [X0] :
( end_time(sK0(sK2)) != X0
| ~ greater_or_equal(X0,start_time(sK0(sK2)))
| ~ greater_or_equal(X0,appear(efficient_producers,sK0(sK2)))
| greater(cardinality_at_time(efficient_producers,X0),zero) )
| ~ spl3_77 ),
inference(resolution,[],[f538,f76]) ).
fof(f907,plain,
( ! [X0] :
( ~ greater(cardinality_at_time(efficient_producers,X0),zero)
| ~ greater(cardinality_at_time(first_movers,X0),zero)
| ~ in_environment(sK0(sK2),X0)
| ~ greater(X0,critical_point(sK0(sK2)))
| greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0)) )
| ~ spl3_80 ),
inference(equality_resolution,[],[f560]) ).
fof(f911,plain,
( greater(end_time(sK0(sK2)),critical_point(sK0(sK2)))
| ~ spl3_23
| ~ spl3_90 ),
inference(resolution,[],[f620,f452]) ).
fof(f915,plain,
( spl3_102
| ~ spl3_23
| ~ spl3_90 ),
inference(avatar_split_clause,[],[f911,f618,f221,f717]) ).
fof(f920,plain,
( end_time(sK0(sK2)) != sK1(sK0(sK2))
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ greater(cardinality_at_time(efficient_producers,sK1(sK0(sK2))),zero) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f922,plain,
( critical_point(sK0(sK2)) != start_time(sK0(sK2))
| greater_or_equal(end_time(sK0(sK2)),start_time(sK0(sK2)))
| ~ greater_or_equal(end_time(sK0(sK2)),critical_point(sK0(sK2))) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f926,definition,
( spl3_118
<=> greater_or_equal(end_time(sK0(sK2)),end_time(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_118])],[avatar_definition]) ).
fof(f956,definition,
( spl3_121
<=> subpopulation(first_movers,sK0(sK2),end_time(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_121])],[avatar_definition]) ).
fof(f958,plain,
( ~ subpopulation(first_movers,sK0(sK2),end_time(sK0(sK2)))
| spl3_121 ),
inference(avatar_component_clause,[],[f956]) ).
fof(f974,definition,
( spl3_125
<=> ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,end_time(sK0(sK2))) ) ),
introduced(definition,[new_symbols(definition,[spl3_125])],[avatar_definition]) ).
fof(f975,plain,
( ! [X0] :
( ~ in_environment(X0,end_time(sK0(sK2)))
| ~ environment(X0) )
| ~ spl3_125 ),
inference(avatar_component_clause,[],[f974]) ).
fof(f1009,definition,
( spl3_131
<=> greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero) ),
introduced(definition,[new_symbols(definition,[spl3_131])],[avatar_definition]) ).
fof(f1056,plain,
( ! [X0] :
( ~ greater(X0,critical_point(sK0(sK2)))
| greater(X0,start_time(sK0(sK2))) )
| ~ spl3_63 ),
inference(resolution,[],[f440,f73]) ).
fof(f1131,plain,
( greater_or_equal(end_time(sK0(sK2)),end_time(sK0(sK2)))
| ~ environment(sK0(sK2))
| ~ spl3_115 ),
inference(resolution,[],[f858,f66]) ).
fof(f1143,plain,
( ~ spl3_9
| spl3_118
| ~ spl3_115 ),
inference(avatar_split_clause,[],[f1131,f856,f926,f128]) ).
fof(f1161,plain,
( ! [X0] :
( greater(end_time(sK0(sK2)),critical_point(sK0(sK2)))
| ~ environment(sK0(sK2))
| ~ in_environment(X0,sK0(sK2))
| ~ observational_period(X0)
| ~ slow_change(X0) )
| ~ spl3_89 ),
inference(superposition,[],[f61,f616]) ).
fof(f1163,plain,
( spl3_21
| ~ spl3_9
| spl3_102
| ~ spl3_89 ),
inference(avatar_split_clause,[],[f1161,f614,f717,f128,f213]) ).
fof(f1171,definition,
( spl3_142
<=> greater_or_equal(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_142])],[avatar_definition]) ).
fof(f1172,plain,
( ~ greater_or_equal(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| spl3_142 ),
inference(avatar_component_clause,[],[f1171]) ).
fof(f1278,definition,
( spl3_154
<=> greater(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_154])],[avatar_definition]) ).
fof(f1289,definition,
( spl3_156
<=> greater(end_time(sK0(sK2)),start_time(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_156])],[avatar_definition]) ).
fof(f1320,definition,
( spl3_158
<=> in_environment(sK0(sK2),start_time(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_158])],[avatar_definition]) ).
fof(f1321,plain,
( ~ in_environment(sK0(sK2),start_time(sK0(sK2)))
| spl3_158 ),
inference(avatar_component_clause,[],[f1320]) ).
fof(f1324,definition,
( spl3_159
<=> greater_or_equal(start_time(sK0(sK2)),start_time(sK0(sK2))) ),
introduced(definition,[new_symbols(definition,[spl3_159])],[avatar_definition]) ).
fof(f1326,plain,
( ~ greater_or_equal(start_time(sK0(sK2)),start_time(sK0(sK2)))
| spl3_159 ),
inference(avatar_component_clause,[],[f1324]) ).
fof(f1453,plain,
( zero != zero
| ~ in_environment(sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ subpopulation(first_movers,sK0(sK2),end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| ~ spl3_36
| ~ spl3_69 ),
inference(superposition,[],[f484,f297]) ).
fof(f1459,plain,
( ~ in_environment(sK0(sK2),end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ subpopulation(first_movers,sK0(sK2),end_time(sK0(sK2)))
| selection_favors(efficient_producers,first_movers,end_time(sK0(sK2)))
| ~ spl3_36
| ~ spl3_69 ),
inference(trivial_inequality_removal,[],[f1453]) ).
fof(f1466,plain,
( spl3_6
| ~ spl3_121
| ~ spl3_37
| ~ spl3_115
| ~ spl3_36
| ~ spl3_69 ),
inference(avatar_split_clause,[],[f1459,f483,f296,f856,f300,f956,f115]) ).
fof(f1477,plain,
( ! [X0] :
( ~ environment(X0)
| ~ environment(X0)
| ~ in_environment(X0,end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero) )
| ~ spl3_35 ),
inference(resolution,[],[f293,f67]) ).
fof(f1479,plain,
( ! [X0] :
( ~ environment(X0)
| ~ in_environment(X0,end_time(sK0(sK2)))
| ~ greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| ~ greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero) )
| ~ spl3_35 ),
inference(duplicate_literal_removal,[],[f1477]) ).
fof(f1481,plain,
( ~ spl3_37
| ~ spl3_131
| spl3_125
| ~ spl3_35 ),
inference(avatar_split_clause,[],[f1479,f292,f974,f1009,f300]) ).
fof(f1496,plain,
( ~ in_environment(sK0(sK2),end_time(sK0(sK2)))
| ~ spl3_9
| spl3_121 ),
inference(resolution,[],[f958,f195]) ).
fof(f1499,plain,
( ~ spl3_115
| ~ spl3_9
| spl3_121 ),
inference(avatar_split_clause,[],[f1496,f956,f128,f856]) ).
fof(f1580,plain,
( ~ greater(end_time(sK0(sK2)),start_time(sK0(sK2)))
| spl3_114 ),
inference(resolution,[],[f854,f77]) ).
fof(f1581,plain,
( ~ spl3_156
| spl3_114 ),
inference(avatar_split_clause,[],[f1580,f852,f1289]) ).
fof(f1600,plain,
( greater(end_time(sK0(sK2)),start_time(sK0(sK2)))
| ~ spl3_63
| ~ spl3_102 ),
inference(resolution,[],[f1056,f719]) ).
fof(f1604,plain,
( spl3_156
| ~ spl3_63
| ~ spl3_102 ),
inference(avatar_split_clause,[],[f1600,f717,f438,f1289]) ).
fof(f1617,plain,
( greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| zero = cardinality_at_time(first_movers,end_time(sK0(sK2)))
| ~ spl3_9
| ~ spl3_115 ),
inference(resolution,[],[f858,f479]) ).
fof(f1620,plain,
( ~ environment(sK0(sK2))
| ~ spl3_115
| ~ spl3_125 ),
inference(resolution,[],[f858,f975]) ).
fof(f1629,plain,
( ~ spl3_9
| ~ spl3_115
| ~ spl3_125 ),
inference(avatar_split_clause,[],[f1620,f974,f856,f128]) ).
fof(f1687,plain,
( greater(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| ~ spl3_68
| ~ spl3_102 ),
inference(resolution,[],[f748,f719]) ).
fof(f1691,plain,
( spl3_154
| ~ spl3_68
| ~ spl3_102 ),
inference(avatar_split_clause,[],[f1687,f717,f468,f1278]) ).
fof(f1821,plain,
( ~ greater_or_equal(end_time(sK0(sK2)),end_time(sK0(sK2)))
| greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| zero = cardinality_at_time(first_movers,end_time(sK0(sK2)))
| ~ in_environment(sK0(sK2),start_time(sK0(sK2)))
| ~ spl3_9
| ~ spl3_113 ),
inference(resolution,[],[f846,f191]) ).
fof(f1836,plain,
( ~ greater_or_equal(end_time(sK0(sK2)),start_time(sK0(sK2)))
| ~ greater_or_equal(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| greater(cardinality_at_time(efficient_producers,end_time(sK0(sK2))),zero)
| ~ spl3_77 ),
inference(equality_resolution,[],[f892]) ).
fof(f1837,plain,
( spl3_37
| ~ spl3_142
| ~ spl3_114
| ~ spl3_77 ),
inference(avatar_split_clause,[],[f1836,f537,f852,f1171,f300]) ).
fof(f1848,plain,
( ~ environment(sK0(sK2))
| ~ greater_or_equal(start_time(sK0(sK2)),start_time(sK0(sK2)))
| ~ greater_or_equal(end_time(sK0(sK2)),start_time(sK0(sK2)))
| spl3_158 ),
inference(resolution,[],[f1321,f65]) ).
fof(f1849,plain,
( ~ spl3_114
| ~ spl3_159
| ~ spl3_9
| spl3_158 ),
inference(avatar_split_clause,[],[f1848,f1320,f128,f1324,f852]) ).
fof(f2004,plain,
( start_time(sK0(sK2)) != start_time(sK0(sK2))
| spl3_159 ),
inference(resolution,[],[f1326,f76]) ).
fof(f2006,plain,
( $false
| spl3_159 ),
inference(trivial_inequality_removal,[],[f2004]) ).
fof(f2007,plain,
spl3_159,
inference(avatar_contradiction_clause,[],[f2006]) ).
fof(f2105,plain,
( ~ greater(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| spl3_142 ),
inference(resolution,[],[f1172,f77]) ).
fof(f2106,plain,
( ~ spl3_154
| spl3_142 ),
inference(avatar_split_clause,[],[f2105,f1171,f1278]) ).
fof(f2122,plain,
( critical_point(sK0(sK2)) != appear(efficient_producers,sK0(sK2))
| greater_or_equal(end_time(sK0(sK2)),appear(efficient_producers,sK0(sK2)))
| ~ greater_or_equal(end_time(sK0(sK2)),critical_point(sK0(sK2))) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f2133,plain,
( spl3_36
| spl3_131
| ~ spl3_9
| ~ spl3_115 ),
inference(avatar_split_clause,[],[f1617,f856,f128,f1009,f296]) ).
fof(f2134,plain,
( ~ spl3_158
| spl3_36
| spl3_131
| ~ spl3_118
| ~ spl3_9
| ~ spl3_113 ),
inference(avatar_split_clause,[],[f1821,f845,f128,f926,f1009,f296,f1320]) ).
fof(f2141,plain,
( ~ greater(cardinality_at_time(first_movers,end_time(sK0(sK2))),zero)
| ~ in_environment(sK0(sK2),end_time(sK0(sK2)))
| ~ greater(end_time(sK0(sK2)),critical_point(sK0(sK2)))
| greater(growth_rate(efficient_producers,end_time(sK0(sK2))),growth_rate(first_movers,end_time(sK0(sK2))))
| ~ spl3_37
| ~ spl3_80 ),
inference(resolution,[],[f301,f907]) ).
fof(f2154,plain,
( spl3_34
| ~ spl3_102
| ~ spl3_115
| ~ spl3_131
| ~ spl3_37
| ~ spl3_80 ),
inference(avatar_split_clause,[],[f2141,f559,f300,f1009,f856,f717,f288]) ).
cnf(s1,plain,
spl3_1,
inference(sat_conversion,[],[f88]) ).
cnf(s2,plain,
spl3_2,
inference(sat_conversion,[],[f93]) ).
cnf(s3,plain,
~ spl3_3,
inference(sat_conversion,[],[f98]) ).
cnf(s13,plain,
( ~ spl3_2
| spl3_3
| ~ spl3_6
| ~ spl3_7
| ~ spl3_8 ),
inference(sat_conversion,[],[f164]) ).
cnf(s14,plain,
( ~ spl3_2
| spl3_3
| ~ spl3_7
| ~ spl3_8
| spl3_9 ),
inference(sat_conversion,[],[f165]) ).
cnf(s15,plain,
( ~ spl3_2
| spl3_3
| ~ spl3_7
| ~ spl3_8
| spl3_10 ),
inference(sat_conversion,[],[f166]) ).
cnf(s17,plain,
( ~ spl3_7
| ~ spl3_8
| spl3_17 ),
inference(sat_conversion,[],[f176]) ).
cnf(s18,plain,
( ~ spl3_7
| ~ spl3_8
| spl3_18 ),
inference(sat_conversion,[],[f181]) ).
cnf(s19,plain,
spl3_7,
inference(sat_conversion,[],[f183]) ).
cnf(s20,plain,
spl3_8,
inference(sat_conversion,[],[f185]) ).
cnf(s21,plain,
( ~ spl3_9
| spl3_19 ),
inference(sat_conversion,[],[f206]) ).
cnf(s22,plain,
( ~ spl3_9
| spl3_20 ),
inference(sat_conversion,[],[f211]) ).
cnf(s30,plain,
( ~ spl3_1
| ~ spl3_2
| ~ spl3_9
| ~ spl3_10
| spl3_22 ),
inference(sat_conversion,[],[f269]) ).
cnf(s31,plain,
( ~ spl3_1
| ~ spl3_2
| ~ spl3_9
| ~ spl3_10
| spl3_23 ),
inference(sat_conversion,[],[f270]) ).
cnf(s33,plain,
( spl3_6
| ~ spl3_34
| spl3_35 ),
inference(sat_conversion,[],[f294]) ).
cnf(s44,plain,
( ~ spl3_2
| spl3_3
| ~ spl3_17
| spl3_48 ),
inference(sat_conversion,[],[f360]) ).
cnf(s45,plain,
( ~ spl3_2
| spl3_3
| ~ spl3_18
| spl3_49 ),
inference(sat_conversion,[],[f365]) ).
cnf(s51,plain,
( ~ spl3_9
| ~ spl3_22
| spl3_56 ),
inference(sat_conversion,[],[f408]) ).
cnf(s54,plain,
( ~ spl3_19
| spl3_62
| spl3_63 ),
inference(sat_conversion,[],[f441]) ).
cnf(s56,plain,
( ~ spl3_23
| spl3_66 ),
inference(sat_conversion,[],[f458]) ).
cnf(s58,plain,
( ~ spl3_20
| spl3_67
| spl3_68 ),
inference(sat_conversion,[],[f471]) ).
cnf(s59,plain,
( ~ spl3_1
| ~ spl3_2
| ~ spl3_10
| ~ spl3_21 ),
inference(sat_conversion,[],[f473]) ).
cnf(s60,plain,
( ~ spl3_9
| ~ spl3_9
| spl3_69 ),
inference(sat_conversion,[],[f485]) ).
cnf(s61,plain,
( ~ spl3_9
| spl3_69 ),
inference(rat,[],[s60]) ).
cnf(s74,plain,
( ~ spl3_9
| ~ spl3_48
| spl3_77 ),
inference(sat_conversion,[],[f539]) ).
cnf(s75,plain,
( ~ spl3_9
| spl3_21
| ~ spl3_48
| spl3_53
| ~ spl3_78 ),
inference(sat_conversion,[],[f544]) ).
cnf(s77,plain,
( ~ spl3_66
| ~ spl3_67
| spl3_78 ),
inference(sat_conversion,[],[f546]) ).
cnf(s81,plain,
( ~ spl3_9
| ~ spl3_49
| spl3_80 ),
inference(sat_conversion,[],[f561]) ).
cnf(s89,plain,
( ~ spl3_56
| spl3_89
| spl3_90 ),
inference(sat_conversion,[],[f621]) ).
cnf(s121,plain,
( spl3_64
| ~ spl3_102 ),
inference(sat_conversion,[],[f744]) ).
cnf(s123,plain,
( spl3_78
| ~ spl3_104 ),
inference(sat_conversion,[],[f756]) ).
cnf(s125,plain,
( ~ spl3_23
| ~ spl3_68
| spl3_104 ),
inference(sat_conversion,[],[f768]) ).
cnf(s141,plain,
( ~ spl3_9
| ~ spl3_9
| spl3_113 ),
inference(sat_conversion,[],[f847]) ).
cnf(s142,plain,
( ~ spl3_9
| spl3_113 ),
inference(rat,[],[s141]) ).
cnf(s143,plain,
( ~ spl3_9
| ~ spl3_114
| spl3_115 ),
inference(sat_conversion,[],[f859]) ).
cnf(s147,plain,
( ~ spl3_23
| ~ spl3_90
| spl3_102 ),
inference(sat_conversion,[],[f915]) ).
cnf(s152,plain,
( spl3_37
| ~ spl3_53
| ~ spl3_89 ),
inference(sat_conversion,[],[f920]) ).
cnf(s154,plain,
( ~ spl3_62
| ~ spl3_64
| spl3_114 ),
inference(sat_conversion,[],[f922]) ).
cnf(s207,plain,
( ~ spl3_9
| ~ spl3_115
| spl3_118 ),
inference(sat_conversion,[],[f1143]) ).
cnf(s209,plain,
( ~ spl3_9
| spl3_21
| ~ spl3_89
| spl3_102 ),
inference(sat_conversion,[],[f1163]) ).
cnf(s277,plain,
( spl3_6
| ~ spl3_36
| ~ spl3_37
| ~ spl3_69
| ~ spl3_115
| ~ spl3_121 ),
inference(sat_conversion,[],[f1466]) ).
cnf(s286,plain,
( ~ spl3_35
| ~ spl3_37
| spl3_125
| ~ spl3_131 ),
inference(sat_conversion,[],[f1481]) ).
cnf(s293,plain,
( ~ spl3_9
| ~ spl3_115
| spl3_121 ),
inference(sat_conversion,[],[f1499]) ).
cnf(s305,plain,
( spl3_114
| ~ spl3_156 ),
inference(sat_conversion,[],[f1581]) ).
cnf(s310,plain,
( ~ spl3_63
| ~ spl3_102
| spl3_156 ),
inference(sat_conversion,[],[f1604]) ).
cnf(s318,plain,
( ~ spl3_9
| ~ spl3_115
| ~ spl3_125 ),
inference(sat_conversion,[],[f1629]) ).
cnf(s327,plain,
( ~ spl3_68
| ~ spl3_102
| spl3_154 ),
inference(sat_conversion,[],[f1691]) ).
cnf(s336,plain,
( spl3_37
| ~ spl3_77
| ~ spl3_114
| ~ spl3_142 ),
inference(sat_conversion,[],[f1837]) ).
cnf(s337,plain,
( ~ spl3_9
| ~ spl3_114
| spl3_158
| ~ spl3_159 ),
inference(sat_conversion,[],[f1849]) ).
cnf(s352,plain,
spl3_159,
inference(sat_conversion,[],[f2007]) ).
cnf(s366,plain,
( spl3_142
| ~ spl3_154 ),
inference(sat_conversion,[],[f2106]) ).
cnf(s374,plain,
( ~ spl3_64
| ~ spl3_67
| spl3_142 ),
inference(sat_conversion,[],[f2122]) ).
cnf(s382,plain,
( ~ spl3_9
| spl3_36
| ~ spl3_115
| spl3_131 ),
inference(sat_conversion,[],[f2133]) ).
cnf(s383,plain,
( ~ spl3_9
| spl3_36
| ~ spl3_113
| ~ spl3_118
| spl3_131
| ~ spl3_158 ),
inference(sat_conversion,[],[f2134]) ).
cnf(s389,plain,
( spl3_34
| ~ spl3_37
| ~ spl3_80
| ~ spl3_102
| ~ spl3_115
| ~ spl3_131 ),
inference(sat_conversion,[],[f2154]) ).
cnf(s392,plain,
( ~ spl3_9
| ~ spl3_114
| spl3_158 ),
inference(rat,[],[s337,s352]) ).
cnf(s399,plain,
spl3_18,
inference(rat,[],[s18,s20,s19]) ).
cnf(s400,plain,
spl3_17,
inference(rat,[],[s17,s20,s19]) ).
cnf(s402,plain,
( ~ spl3_2
| spl3_3
| spl3_10 ),
inference(rat,[],[s15,s20,s19]) ).
cnf(s403,plain,
( ~ spl3_2
| spl3_3
| spl3_9 ),
inference(rat,[],[s14,s20,s19]) ).
cnf(s404,plain,
( ~ spl3_2
| spl3_3
| ~ spl3_6 ),
inference(rat,[],[s13,s20,s19]) ).
cnf(s408,plain,
spl3_49,
inference(rat,[],[s45,s3,s399,s2]) ).
cnf(s409,plain,
spl3_48,
inference(rat,[],[s44,s3,s400,s2]) ).
cnf(s411,plain,
spl3_10,
inference(rat,[],[s402,s3,s2]) ).
cnf(s412,plain,
spl3_9,
inference(rat,[],[s403,s3,s2]) ).
cnf(s413,plain,
~ spl3_6,
inference(rat,[],[s404,s3,s2]) ).
cnf(s417,plain,
spl3_113,
inference(rat,[],[s142,s412]) ).
cnf(s418,plain,
spl3_80,
inference(rat,[],[s81,s408,s412]) ).
cnf(s420,plain,
spl3_77,
inference(rat,[],[s74,s409,s412]) ).
cnf(s425,plain,
spl3_69,
inference(rat,[],[s61,s412]) ).
cnf(s426,plain,
spl3_20,
inference(rat,[],[s22,s412]) ).
cnf(s427,plain,
spl3_19,
inference(rat,[],[s21,s412]) ).
cnf(s430,plain,
~ spl3_21,
inference(rat,[],[s59,s411,s2,s1]) ).
cnf(s431,plain,
spl3_23,
inference(rat,[],[s31,s412,s411,s2,s1]) ).
cnf(s432,plain,
spl3_22,
inference(rat,[],[s30,s412,s411,s2,s1]) ).
cnf(s436,plain,
spl3_66,
inference(rat,[],[s56,s431]) ).
cnf(s438,plain,
spl3_56,
inference(rat,[],[s51,s412,s432]) ).
cnf(s444,plain,
spl3_78,
inference(rat,[],[s58,s125,s77,s123,s426,s431,s436]) ).
cnf(s445,plain,
spl3_53,
inference(rat,[],[s75,s430,s412,s409,s444]) ).
cnf(s448,plain,
( spl3_142
| ~ spl3_102 ),
inference(rat,[],[s58,s327,s374,s366,s121,s426]) ).
cnf(s449,plain,
spl3_37,
inference(rat,[],[s54,s310,s154,s305,s336,s448,s121,s147,s89,s152,s427,s420,s431,s438,s445]) ).
cnf(s451,plain,
( ~ spl3_115
| ~ spl3_102
| spl3_36
| spl3_34 ),
inference(rat,[],[s389,s382,s418,s449,s412]) ).
cnf(s452,plain,
( ~ spl3_102
| ~ spl3_64
| spl3_36
| spl3_34 ),
inference(rat,[],[s54,s310,s154,s305,s143,s451,s427,s412]) ).
cnf(s453,plain,
spl3_102,
inference(rat,[],[s89,s147,s209,s438,s431,s412,s430]) ).
cnf(s454,plain,
spl3_64,
inference(rat,[],[s121,s453]) ).
cnf(s463,plain,
( ~ spl3_115
| ~ spl3_36 ),
inference(rat,[],[s277,s293,s413,s425,s449,s412]) ).
cnf(s464,plain,
spl3_114,
inference(rat,[],[s54,s310,s154,s305,s427,s453,s454]) ).
cnf(s465,plain,
spl3_158,
inference(rat,[],[s392,s412,s464]) ).
cnf(s466,plain,
spl3_115,
inference(rat,[],[s143,s412,s464]) ).
cnf(s470,plain,
~ spl3_125,
inference(rat,[],[s318,s412,s466]) ).
cnf(s473,plain,
spl3_118,
inference(rat,[],[s207,s412,s466]) ).
cnf(s475,plain,
~ spl3_36,
inference(rat,[],[s463,s466]) ).
cnf(s480,plain,
spl3_131,
inference(rat,[],[s383,s465,s475,s417,s412,s473]) ).
cnf(s481,plain,
spl3_34,
inference(rat,[],[s452,s454,s453,s475]) ).
cnf(s486,plain,
~ spl3_35,
inference(rat,[],[s286,s449,s470,s480]) ).
cnf(s488,plain,
$false,
inference(rat,[],[s33,s413,s486,s481]) ).
fof(f2155,plain,
$false,
inference(avatar_sat_refutation,[],[s488]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT039+2 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 % Computer : n019.cluster.edu
% 0.12/0.41 % Model : x86_64 x86_64
% 0.12/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.41 % Memory : 8046.5625MB
% 0.12/0.41 % OS : Linux 6.8.0-71-generic
% 0.12/0.41 % CPULimit : 300
% 0.12/0.41 % WCLimit : 300
% 0.12/0.41 % DateTime : Sun Sep 27 17:23:49 UTC 2026
% 0.12/0.41 % CPUTime :
% 0.12/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.46 Running first-order theorem proving
% 0.12/0.46 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.85/1.75 % (3290031)Detected formulas, will run a generic FOF schedule.
% 5.85/1.75 % (3290043)dis-21_1_sil=8000:lcm=predicate:random_seed=1970139806:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_3000 on theBenchmark for (3000ds/129Mi)
% 5.85/1.75 % (3290043)Instruction limit reached!
% 5.85/1.75 % (3290043)------------------------------
% 5.85/1.75 % (3290043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.85/1.75 % (3290043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.75 % (3290043)CaDiCaL version: 2.1.3
% 5.85/1.75 % (3290043)Termination reason: Instruction limit
% 5.85/1.75 % (3290043)Termination phase: Saturation
% 5.85/1.75 % (3290043)Time elapsed: 0.027 s
% 5.85/1.75 % (3290043)Peak memory usage: 88 MB
% 5.85/1.75 % (3290043)Instructions burned: 132 (million)
% 5.85/1.75 % (3290040)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2507248398:i=109:sd=1:ins=1:gsp=on:ss=axioms_3000 on theBenchmark for (3000ds/109Mi)
% 5.85/1.75 % (3290042)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=300462879:s2a=on:i=139:gtg=position_3000 on theBenchmark for (3000ds/139Mi)
% 5.85/1.75 % (3290037)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=494601529:i=141193_3000 on theBenchmark for (3000ds/141193Mi)
% 5.85/1.75 % (3290038)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2480304667:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_3000 on theBenchmark for (3000ds/134677Mi)
% 5.85/1.75 % (3290039)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=4095698604:i=141695:sd=1:nm=32:gsp=on:ss=included_3000 on theBenchmark for (3000ds/141695Mi)
% 5.85/1.75 % (3290040)Refutation not found, incomplete strategy
% 5.85/1.75 % (3290040)------------------------------
% 5.85/1.75 % (3290040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.85/1.75 % (3290040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.75 % (3290040)CaDiCaL version: 2.1.3
% 5.85/1.75 % (3290040)Termination reason: Refutation not found, incomplete strategy
% 5.85/1.75 % (3290040)Time elapsed: 0.001 s
% 5.85/1.75 % (3290040)Peak memory usage: 87 MB
% 5.85/1.75 % (3290041)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=452008407:i=119:av=off:ss=axioms_3000 on theBenchmark for (3000ds/119Mi)
% 5.85/1.75 % (3290045)lrs+10_1_sil=8000:sp=occurrence:random_seed=634774684:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 5.85/1.75 % (3290041)Instruction limit reached!
% 5.85/1.75 % (3290041)------------------------------
% 5.85/1.75 % (3290041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.85/1.75 % (3290041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.75 % (3290041)CaDiCaL version: 2.1.3
% 5.85/1.75 % (3290041)Termination reason: Instruction limit
% 5.85/1.75 % (3290041)Termination phase: Saturation
% 5.85/1.75 % (3290041)Time elapsed: 0.070 s
% 5.85/1.75 % (3290041)Peak memory usage: 88 MB
% 5.85/1.75 % (3290041)Instructions burned: 119 (million)
% 5.85/1.75 % (3290042)Instruction limit reached!
% 5.85/1.75 % (3290042)------------------------------
% 5.85/1.75 % (3290042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.85/1.75 % (3290042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.75 % (3290042)CaDiCaL version: 2.1.3
% 5.85/1.75 % (3290042)Termination reason: Instruction limit
% 5.85/1.75 % (3290042)Termination phase: Saturation
% 5.85/1.75 % (3290042)Time elapsed: 0.094 s
% 5.85/1.75 % (3290042)Peak memory usage: 89 MB
% 5.85/1.75 % (3290042)Instructions burned: 140 (million)
% 5.85/1.75 % (3290045)Instruction limit reached!
% 5.85/1.75 % (3290045)------------------------------
% 5.85/1.75 % (3290045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.85/1.75 % (3290045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.75 % (3290045)CaDiCaL version: 2.1.3
% 5.85/1.75 % (3290045)Termination reason: Instruction limit
% 5.85/1.75 % (3290045)Termination phase: Saturation
% 5.85/1.75 % (3290045)Time elapsed: 0.079 s
% 5.85/1.75 % (3290045)Peak memory usage: 90 MB
% 5.85/1.75 % (3290045)Instructions burned: 287 (million)
% 5.85/1.75 % (3290054)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3299987471:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.85/1.75 % (3290054)Refutation not found, incomplete strategy
% 5.85/1.75 % (3290054)------------------------------
% 5.85/1.75 % (3290054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.85/1.75 % (3290054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.75 % (3290054)CaDiCaL version: 2.1.3
% 5.85/1.75 % (3290054)Termination reason: Refutation not found, incomplete strategy
% 5.85/1.75 % (3290054)Time elapsed: 0.003 s
% 5.85/1.75 % (3290054)Peak memory usage: 88 MB
% 5.85/1.75 % (3290054)Instructions burned: 2 (million)
% 5.85/1.75 % (3290055)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2002371869:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.85/1.75 % (3290040)------------------------------
% 5.85/1.75 % (3290040)------------------------------
% 5.85/1.75 % (3290056)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=460814652:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 5.85/1.75 % (3290056)Refutation not found, incomplete strategy
% 5.85/1.75 % (3290056)------------------------------
% 5.85/1.75 % (3290056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.85/1.75 % (3290056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.75 % (3290056)CaDiCaL version: 2.1.3
% 5.85/1.75 % (3290056)Termination reason: Refutation not found, incomplete strategy
% 5.85/1.75 % (3290056)Time elapsed: 0.002 s
% 5.85/1.75 % (3290056)Peak memory usage: 89 MB
% 5.85/1.75 % (3290056)Instructions burned: 3 (million)
% 5.85/1.75 % (3290063)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2521930926:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 5.85/1.75 % (3290056)------------------------------
% 5.85/1.75 % (3290056)------------------------------
% 5.85/1.75 % (3290055)Instruction limit reached!
% 5.85/1.75 % (3290055)------------------------------
% 5.85/1.75 % (3290055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.85/1.75 % (3290055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.75 % (3290055)CaDiCaL version: 2.1.3
% 5.85/1.75 % (3290055)Termination reason: Instruction limit
% 5.85/1.75 % (3290055)Termination phase: Saturation
% 5.85/1.75 % (3290055)Time elapsed: 0.197 s
% 5.85/1.75 % (3290055)Peak memory usage: 90 MB
% 5.85/1.75 % (3290055)Instructions burned: 326 (million)
% 5.85/1.75 % (3290054)------------------------------
% 5.85/1.75 % (3290054)------------------------------
% 5.85/1.75 % (3290111)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=688506236:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 5.85/1.75 % (3290063)Instruction limit reached!
% 5.85/1.75 % (3290063)------------------------------
% 5.85/1.75 % (3290063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.85/1.75 % (3290063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.75 % (3290063)CaDiCaL version: 2.1.3
% 5.85/1.75 % (3290063)Termination reason: Instruction limit
% 5.85/1.75 % (3290063)Termination phase: Saturation
% 5.85/1.75 % (3290063)Time elapsed: 0.139 s
% 5.85/1.75 % (3290063)Peak memory usage: 88 MB
% 5.85/1.75 % (3290063)Instructions burned: 295 (million)
% 5.85/1.75 % (3290127)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3990771572:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 5.85/1.75 % (3290132)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2033525008:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 5.85/1.75 % (3290127)First to succeed.
% 5.85/1.75 % (3290127)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3290031"
% 5.85/1.75 % (3290143)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=588370175:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 5.85/1.75 % (3290143)Refutation not found, incomplete strategy
% 5.85/1.75 % (3290143)------------------------------
% 5.85/1.75 % (3290143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.85/1.75 % (3290143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.75 % (3290143)CaDiCaL version: 2.1.3
% 5.85/1.75 % (3290143)Termination reason: Refutation not found, incomplete strategy
% 5.85/1.75 % (3290143)Time elapsed: 0.001 s
% 5.85/1.75 % (3290143)Peak memory usage: 87 MB
% 5.85/1.75 % (3290132)Instruction limit reached!
% 5.85/1.75 % (3290132)------------------------------
% 5.85/1.75 % (3290132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.85/1.75 % (3290132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.85/1.75 % (3290132)CaDiCaL version: 2.1.3
% 5.85/1.75 % (3290132)Termination reason: Instruction limit
% 5.85/1.75 % (3290132)Termination phase: Saturation
% 5.85/1.75 % (3290132)Time elapsed: 0.067 s
% 5.85/1.75 % (3290132)Peak memory usage: 88 MB
% 5.85/1.75 % (3290132)Instructions burned: 128 (million)
% 5.85/1.75 % (3290038)Also succeeded, but the first one will report.
% 5.85/1.75 % (3290037)Also succeeded, but the first one will report.
% 5.85/1.75 % (3290175)lrs+10_1_sil=8000:sp=occurrence:random_seed=3903215655:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 5.85/1.75 % (3290127)Refutation found. Thanks to Tanya!
% 5.85/1.75 % SZS status Theorem for theBenchmark
% 5.85/1.75 % SZS output start Proof for theBenchmark
% See solution above
% 7.67/1.94 % (3290127)------------------------------
% 7.67/1.94 % (3290127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.67/1.94 % (3290127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.67/1.94 % (3290127)CaDiCaL version: 2.1.3
% 7.67/1.94 % (3290127)Termination reason: Refutation
% 7.67/1.94 % (3290127)Time elapsed: 0.055 s
% 7.67/1.94 % (3290127)Peak memory usage: 90 MB
% 7.67/1.94 % (3290127)Instructions burned: 74 (million)
% 7.67/1.94 % (3290127)------------------------------
% 7.67/1.94 % (3290127)------------------------------
% 7.67/1.94 % (3290031)Success in time 1.012 s
% 7.67/1.94 % Vampire exiting
%------------------------------------------------------------------------------