%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : MGT019-2 : TPTP v9.2.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:47:07 PM UTC 2026
% Result : Satisfiable 1.23s 1.71s
% Output : Saturation 1.23s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(a8_28,hypothesis,
( greater_or_equal(founding_rate(efficient_producers,X2),founding_rate(first_movers,X2))
| ~ environment(X1)
| ~ stable(X1)
| ~ subpopulations(first_movers,efficient_producers,X1,X2)
| ~ greater_or_equal(X2,sk3(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a8_28) ).
cnf(prove_l1_31,negated_conjecture,
( subpopulations(first_movers,efficient_producers,sk4,sk5(X1))
| ~ in_environment(sk4,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l1_31) ).
cnf(prove_l1_30,negated_conjecture,
stable(sk4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l1_30) ).
cnf(prove_l1_29,negated_conjecture,
environment(sk4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l1_29) ).
cnf(mp_greater_or_equal_26,axiom,
( greater(X1,X2)
| X1 = X2
| ~ greater_or_equal(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_26) ).
cnf(prove_l1_32,negated_conjecture,
( greater_or_equal(sk5(X1),X1)
| ~ in_environment(sk4,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l1_32) ).
cnf(l2_23,axiom,
subpopulations(first_movers,efficient_producers,sk1,sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l2_23) ).
cnf(l2_22,axiom,
environment(sk1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l2_22) ).
cnf(a8_27,hypothesis,
( in_environment(X1,sk3(X1))
| ~ environment(X1)
| ~ stable(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a8_27) ).
cnf(mp_EP_lower_disbanding_rate_25,axiom,
( greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ greater(disbanding_rate(first_movers,X1),disbanding_rate(efficient_producers,X1))
| ~ greater_or_equal(founding_rate(efficient_producers,X1),founding_rate(first_movers,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_EP_lower_disbanding_rate_25) ).
cnf(prove_l1_33,negated_conjecture,
( ~ in_environment(sk4,X1)
| ~ greater(growth_rate(efficient_producers,sk5(X1)),growth_rate(first_movers,sk5(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l1_33) ).
cnf(l2_24,axiom,
~ greater(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l2_24) ).
cnf(c_0_12,hypothesis,
( greater_or_equal(founding_rate(efficient_producers,X2),founding_rate(first_movers,X2))
| ~ environment(X1)
| ~ stable(X1)
| ~ subpopulations(first_movers,efficient_producers,X1,X2)
| ~ greater_or_equal(X2,sk3(X1)) ),
a8_28,
[final] ).
cnf(c_0_13,negated_conjecture,
( subpopulations(first_movers,efficient_producers,sk4,sk5(X1))
| ~ in_environment(sk4,X1) ),
prove_l1_31,
[final] ).
cnf(c_0_14,negated_conjecture,
stable(sk4),
prove_l1_30,
[final] ).
cnf(c_0_15,negated_conjecture,
environment(sk4),
prove_l1_29,
[final] ).
cnf(c_0_16,axiom,
( greater(X1,X2)
| X1 = X2
| ~ greater_or_equal(X1,X2) ),
mp_greater_or_equal_26,
[final] ).
cnf(c_0_17,negated_conjecture,
( greater_or_equal(founding_rate(efficient_producers,sk5(X1)),founding_rate(first_movers,sk5(X1)))
| ~ in_environment(sk4,X1)
| ~ greater_or_equal(sk5(X1),sk3(sk4)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12,c_0_13]),c_0_14]),c_0_15])]),
[final] ).
cnf(c_0_18,negated_conjecture,
( founding_rate(efficient_producers,sk5(X1)) = founding_rate(first_movers,sk5(X1))
| greater(founding_rate(efficient_producers,sk5(X1)),founding_rate(first_movers,sk5(X1)))
| ~ in_environment(sk4,X1)
| ~ greater_or_equal(sk5(X1),sk3(sk4)) ),
inference(spm,[status(thm)],[c_0_16,c_0_17]),
[final] ).
cnf(c_0_19,negated_conjecture,
( greater_or_equal(sk5(X1),X1)
| ~ in_environment(sk4,X1) ),
prove_l1_32,
[final] ).
cnf(c_0_20,axiom,
subpopulations(first_movers,efficient_producers,sk1,sk2),
l2_23,
[final] ).
cnf(c_0_21,axiom,
environment(sk1),
l2_22,
[final] ).
cnf(c_0_22,negated_conjecture,
( founding_rate(efficient_producers,sk5(sk3(sk4))) = founding_rate(first_movers,sk5(sk3(sk4)))
| greater(founding_rate(efficient_producers,sk5(sk3(sk4))),founding_rate(first_movers,sk5(sk3(sk4))))
| ~ in_environment(sk4,sk3(sk4)) ),
inference(spm,[status(thm)],[c_0_18,c_0_19]) ).
cnf(c_0_23,hypothesis,
( in_environment(X1,sk3(X1))
| ~ environment(X1)
| ~ stable(X1) ),
a8_27,
[final] ).
cnf(c_0_24,hypothesis,
( greater_or_equal(founding_rate(efficient_producers,sk2),founding_rate(first_movers,sk2))
| ~ stable(sk1)
| ~ greater_or_equal(sk2,sk3(sk1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12,c_0_20]),c_0_21])]),
[final] ).
cnf(c_0_25,negated_conjecture,
( sk5(X1) = X1
| greater(sk5(X1),X1)
| ~ in_environment(sk4,X1) ),
inference(spm,[status(thm)],[c_0_16,c_0_19]),
[final] ).
cnf(c_0_26,hypothesis,
( founding_rate(efficient_producers,sk5(sk3(sk4))) = founding_rate(first_movers,sk5(sk3(sk4)))
| greater(founding_rate(efficient_producers,sk5(sk3(sk4))),founding_rate(first_movers,sk5(sk3(sk4)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_22,c_0_23]),c_0_14]),c_0_15])]),
[final] ).
cnf(c_0_27,hypothesis,
( founding_rate(efficient_producers,sk2) = founding_rate(first_movers,sk2)
| greater(founding_rate(efficient_producers,sk2),founding_rate(first_movers,sk2))
| ~ stable(sk1)
| ~ greater_or_equal(sk2,sk3(sk1)) ),
inference(spm,[status(thm)],[c_0_16,c_0_24]),
[final] ).
cnf(c_0_28,hypothesis,
( sk5(sk3(sk4)) = sk3(sk4)
| greater(sk5(sk3(sk4)),sk3(sk4)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25,c_0_23]),c_0_14]),c_0_15])]),
[final] ).
cnf(c_0_29,axiom,
( greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1))
| ~ greater(disbanding_rate(first_movers,X1),disbanding_rate(efficient_producers,X1))
| ~ greater_or_equal(founding_rate(efficient_producers,X1),founding_rate(first_movers,X1)) ),
mp_EP_lower_disbanding_rate_25,
[final] ).
cnf(c_0_30,negated_conjecture,
( ~ in_environment(sk4,X1)
| ~ greater(growth_rate(efficient_producers,sk5(X1)),growth_rate(first_movers,sk5(X1))) ),
prove_l1_33,
[final] ).
cnf(c_0_31,axiom,
~ greater(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2)),
l2_24,
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : MGT019-2 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n029.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 23:26:59 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 1.23/1.71 % Version : CSE_E---1.7
% 1.23/1.71 % Problem : theBenchmark.p
% 1.23/1.71 % SZS status Satisfiable for theBenchmark.p
% 1.23/1.71 % SZS output start Saturation
% See solution above
% 1.23/1.71 % Total time : 1.371s
%------------------------------------------------------------------------------