%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : MGT027+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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 : Sun Sep 27 08:02:10 AM UTC 2026
% Result : Theorem 0.09s 0.38s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 9
% Syntax : Number of formulae : 86 ( 19 unt; 0 def)
% Number of atoms : 263 ( 5 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 301 ( 124 ~; 131 |; 34 &)
% ( 1 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 86 ( 0 sgn 39 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mp_contracts_from,axiom,
! [E,To] :
( ( ! [T] :
( ( greater_or_equal(T,To)
& greater(cardinality_at_time(first_movers,T),zero) )
=> greater(zero,growth_rate(first_movers,T)) )
& in_environment(E,To)
& stable(E)
& environment(E) )
=> contracts_from(To,first_movers) ),
file('theBenchmark.p',mp_contracts_from) ).
fof(mp_non_empty_fm_and_ep,axiom,
! [E,T] :
( ( greater(cardinality_at_time(efficient_producers,T),zero)
& greater(cardinality_at_time(first_movers,T),zero)
& in_environment(E,T)
& environment(E) )
=> subpopulations(first_movers,efficient_producers,E,T) ),
file('theBenchmark.p',mp_non_empty_fm_and_ep) ).
fof(mp_long_stable_environments,axiom,
! [E,T1,T2] :
( ( greater(T2,T1)
& in_environment(E,T1)
& stable(E)
& environment(E) )
=> in_environment(E,T2) ),
file('theBenchmark.p',mp_long_stable_environments) ).
fof(mp_EP_in_stable_environments,axiom,
! [E] :
( ( stable(E)
& environment(E) )
=> in_environment(E,appear(efficient_producers,E)) ),
file('theBenchmark.p',mp_EP_in_stable_environments) ).
fof(mp_greater_transitivity,axiom,
! [X,Y,Z] :
( ( greater(Y,Z)
& greater(X,Y) )
=> greater(X,Z) ),
file('theBenchmark.p',mp_greater_transitivity) ).
fof(mp_greater_or_equal,axiom,
! [X,Y] :
( greater_or_equal(X,Y)
<=> ( X = Y
| greater(X,Y) ) ),
file('theBenchmark.p',mp_greater_or_equal) ).
fof(t6,axiom,
! [E,T] :
( ( greater_or_equal(T,appear(efficient_producers,E))
& in_environment(E,T)
& environment(E) )
=> greater(cardinality_at_time(efficient_producers,T),zero) ),
file('theBenchmark.p',t6) ).
fof(l10,axiom,
! [E] :
( ( stable(E)
& environment(E) )
=> ? [To] :
( ! [T] :
( ( greater_or_equal(T,To)
& subpopulations(first_movers,efficient_producers,E,T) )
=> greater(zero,growth_rate(first_movers,T)) )
& greater(To,appear(efficient_producers,E)) ) ),
file('theBenchmark.p',l10) ).
fof(prove_l9,conjecture,
! [E] :
( ( stable(E)
& environment(E) )
=> ? [To] :
( contracts_from(To,first_movers)
& greater(To,appear(efficient_producers,E)) ) ),
file('theBenchmark.p',prove_l9) ).
fof(prove_l9_neg,negated_conjecture,
~ ! [E] :
( ( stable(E)
& environment(E) )
=> ? [To] :
( contracts_from(To,first_movers)
& greater(To,appear(efficient_producers,E)) ) ),
inference(assume_negation,[status(cth)],[prove_l9]) ).
fof(nnf_9,plain,
? [E] :
( ! [To] :
( ~ contracts_from(To,first_movers)
| ~ greater(To,appear(efficient_producers,E)) )
& stable(E)
& environment(E) ),
inference(fof_nnf,[status(thm)],[prove_l9_neg]) ).
fof(sk_prove_l9_neg,plain,
( ! [To] :
( ~ contracts_from(To,first_movers)
| ~ greater(To,appear(efficient_producers,sK0)) )
& stable(sK0)
& environment(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(E,sK0)],[nnf_9]) ).
cnf(c_10,negated_conjecture,
environment(sK0),
inference(split_conjunct,[status(thm)],[sk_prove_l9_neg]) ).
fof(nnf_8,plain,
! [E] :
( ? [To] :
( ! [T] :
( greater(zero,growth_rate(first_movers,T))
| ~ greater_or_equal(T,To)
| ~ subpopulations(first_movers,efficient_producers,E,T) )
& greater(To,appear(efficient_producers,E)) )
| ~ stable(E)
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[l10]) ).
fof(sk_l10_sk,plain,
! [E] :
( ( ! [T] :
( greater(zero,growth_rate(first_movers,T))
| ~ greater_or_equal(T,sK1(E))
| ~ subpopulations(first_movers,efficient_producers,E,T) )
& greater(sK1(E),appear(efficient_producers,E)) )
| ~ stable(E)
| ~ environment(E) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(To,sK1(E))],[nnf_8]) ).
fof(sk_l10,plain,
( ! [VAR_0,VAR_1] :
( greater(zero,growth_rate(first_movers,VAR_1))
| ~ greater_or_equal(VAR_1,sK1(VAR_0))
| ~ subpopulations(first_movers,efficient_producers,VAR_0,VAR_1)
| ~ stable(VAR_0)
| ~ environment(VAR_0) )
& ! [VAR_0] :
( greater(sK1(VAR_0),appear(efficient_producers,VAR_0))
| ~ stable(VAR_0)
| ~ environment(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_l10_sk]) ).
cnf(c_11,plain,
( greater(zero,growth_rate(first_movers,B))
| ~ greater_or_equal(B,sK1(A))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ stable(A)
| ~ environment(A) ),
inference(split_conjunct,[status(thm)],[sk_l10]) ).
cnf(c_12,plain,
( greater(sK1(A),appear(efficient_producers,A))
| ~ stable(A)
| ~ environment(A) ),
inference(split_conjunct,[status(thm)],[sk_l10]) ).
cnf(c_13,plain,
( greater(cardinality_at_time(efficient_producers,B),zero)
| ~ greater_or_equal(B,appear(efficient_producers,A))
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[t6]) ).
cnf(c_14,plain,
( in_environment(A,appear(efficient_producers,A))
| ~ stable(A)
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp_EP_in_stable_environments]) ).
cnf(c_15,plain,
( in_environment(A,C)
| ~ greater(C,B)
| ~ in_environment(A,B)
| ~ stable(A)
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp_long_stable_environments]) ).
cnf(c_16,plain,
( subpopulations(first_movers,efficient_producers,A,B)
| ~ greater(cardinality_at_time(efficient_producers,B),zero)
| ~ greater(cardinality_at_time(first_movers,B),zero)
| ~ in_environment(A,B)
| ~ environment(A) ),
inference(clausify,[status(thm)],[mp_non_empty_fm_and_ep]) ).
fof(nnf_1,plain,
! [E,To] :
( contracts_from(To,first_movers)
| ? [T] :
( ~ greater(zero,growth_rate(first_movers,T))
& greater_or_equal(T,To)
& greater(cardinality_at_time(first_movers,T),zero) )
| ~ in_environment(E,To)
| ~ stable(E)
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[mp_contracts_from]) ).
fof(sk_mp_contracts_from_sk,plain,
! [E,To] :
( contracts_from(To,first_movers)
| ( ~ greater(zero,growth_rate(first_movers,sK2(E,To)))
& greater_or_equal(sK2(E,To),To)
& greater(cardinality_at_time(first_movers,sK2(E,To)),zero) )
| ~ in_environment(E,To)
| ~ stable(E)
| ~ environment(E) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(T,sK2(E,To))],[nnf_1]) ).
fof(sk_mp_contracts_from,plain,
( ! [VAR_0,VAR_1] :
( contracts_from(VAR_1,first_movers)
| ~ greater(zero,growth_rate(first_movers,sK2(VAR_0,VAR_1)))
| ~ in_environment(VAR_0,VAR_1)
| ~ stable(VAR_0)
| ~ environment(VAR_0) )
& ! [VAR_0,VAR_1] :
( contracts_from(VAR_1,first_movers)
| greater_or_equal(sK2(VAR_0,VAR_1),VAR_1)
| ~ in_environment(VAR_0,VAR_1)
| ~ stable(VAR_0)
| ~ environment(VAR_0) )
& ! [VAR_0,VAR_1] :
( contracts_from(VAR_1,first_movers)
| greater(cardinality_at_time(first_movers,sK2(VAR_0,VAR_1)),zero)
| ~ in_environment(VAR_0,VAR_1)
| ~ stable(VAR_0)
| ~ environment(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_mp_contracts_from_sk]) ).
cnf(c_17,plain,
( contracts_from(B,first_movers)
| ~ greater(zero,growth_rate(first_movers,sK2(A,B)))
| ~ in_environment(A,B)
| ~ stable(A)
| ~ environment(A) ),
inference(split_conjunct,[status(thm)],[sk_mp_contracts_from]) ).
cnf(c_18,plain,
( contracts_from(B,first_movers)
| greater_or_equal(sK2(A,B),B)
| ~ in_environment(A,B)
| ~ stable(A)
| ~ environment(A) ),
inference(split_conjunct,[status(thm)],[sk_mp_contracts_from]) ).
cnf(c_19,plain,
( contracts_from(B,first_movers)
| greater(cardinality_at_time(first_movers,sK2(A,B)),zero)
| ~ in_environment(A,B)
| ~ stable(A)
| ~ environment(A) ),
inference(split_conjunct,[status(thm)],[sk_mp_contracts_from]) ).
cnf(c_20,negated_conjecture,
( contracts_from(A,first_movers)
| greater(cardinality_at_time(first_movers,sK2(sK0,A)),zero)
| ~ in_environment(sK0,A)
| ~ stable(sK0) ),
inference(resolve,[status(thm)],[c_10,c_19]) ).
cnf(c_21,negated_conjecture,
( contracts_from(A,first_movers)
| greater_or_equal(sK2(sK0,A),A)
| ~ in_environment(sK0,A)
| ~ stable(sK0) ),
inference(resolve,[status(thm)],[c_10,c_18]) ).
cnf(c_22,negated_conjecture,
( contracts_from(A,first_movers)
| ~ greater(zero,growth_rate(first_movers,sK2(sK0,A)))
| ~ in_environment(sK0,A)
| ~ stable(sK0) ),
inference(resolve,[status(thm)],[c_10,c_17]) ).
cnf(c_23,negated_conjecture,
( subpopulations(first_movers,efficient_producers,sK0,A)
| ~ greater(cardinality_at_time(efficient_producers,A),zero)
| ~ greater(cardinality_at_time(first_movers,A),zero)
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_10,c_16]) ).
cnf(c_24,negated_conjecture,
( in_environment(sK0,B)
| ~ greater(B,A)
| ~ in_environment(sK0,A)
| ~ stable(sK0) ),
inference(resolve,[status(thm)],[c_10,c_15]) ).
cnf(c_25,negated_conjecture,
( in_environment(sK0,appear(efficient_producers,sK0))
| ~ stable(sK0) ),
inference(resolve,[status(thm)],[c_10,c_14]) ).
cnf(c_26,negated_conjecture,
( greater(cardinality_at_time(efficient_producers,A),zero)
| ~ greater_or_equal(A,appear(efficient_producers,sK0))
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_10,c_13]) ).
cnf(c_27,negated_conjecture,
( greater(sK1(sK0),appear(efficient_producers,sK0))
| ~ stable(sK0) ),
inference(resolve,[status(thm)],[c_10,c_12]) ).
cnf(c_28,negated_conjecture,
( greater(zero,growth_rate(first_movers,A))
| ~ greater_or_equal(A,sK1(sK0))
| ~ subpopulations(first_movers,efficient_producers,sK0,A)
| ~ stable(sK0) ),
inference(resolve,[status(thm)],[c_10,c_11]) ).
cnf(c_29,negated_conjecture,
( ~ contracts_from(A,first_movers)
| ~ greater(A,appear(efficient_producers,sK0)) ),
inference(split_conjunct,[status(thm)],[sk_prove_l9_neg]) ).
cnf(c_30,negated_conjecture,
stable(sK0),
inference(split_conjunct,[status(thm)],[sk_prove_l9_neg]) ).
cnf(c_32,plain,
( ~ greater(A,B)
| greater_or_equal(A,B) ),
inference(clausify,[status(thm)],[mp_greater_or_equal]) ).
cnf(c_33,plain,
( B = A
| greater(A,B)
| ~ greater_or_equal(A,B) ),
inference(clausify,[status(thm)],[mp_greater_or_equal]) ).
cnf(c_34,plain,
( greater(A,C)
| ~ greater(B,C)
| ~ greater(A,B) ),
inference(clausify,[status(thm)],[mp_greater_transitivity]) ).
cnf(c_35,negated_conjecture,
( greater(zero,growth_rate(first_movers,A))
| ~ greater_or_equal(A,sK1(sK0))
| ~ subpopulations(first_movers,efficient_producers,sK0,A) ),
inference(resolve,[status(thm)],[c_30,c_28]) ).
cnf(c_36,negated_conjecture,
greater(sK1(sK0),appear(efficient_producers,sK0)),
inference(resolve,[status(thm)],[c_30,c_27]) ).
cnf(c_37,negated_conjecture,
in_environment(sK0,appear(efficient_producers,sK0)),
inference(resolve,[status(thm)],[c_30,c_25]) ).
cnf(c_38,negated_conjecture,
( in_environment(sK0,B)
| ~ greater(B,A)
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_30,c_24]) ).
cnf(c_39,negated_conjecture,
( contracts_from(A,first_movers)
| ~ greater(zero,growth_rate(first_movers,sK2(sK0,A)))
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_30,c_22]) ).
cnf(c_40,negated_conjecture,
( contracts_from(A,first_movers)
| greater_or_equal(sK2(sK0,A),A)
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_30,c_21]) ).
cnf(c_41,negated_conjecture,
( contracts_from(A,first_movers)
| greater(cardinality_at_time(first_movers,sK2(sK0,A)),zero)
| ~ in_environment(sK0,A) ),
inference(resolve,[status(thm)],[c_30,c_20]) ).
cnf(c_43,plain,
( greater(A,appear(efficient_producers,sK0))
| ~ greater(A,sK1(sK0)) ),
inference(resolve,[status(thm)],[c_36,c_34]) ).
cnf(c_45,plain,
greater_or_equal(sK1(sK0),appear(efficient_producers,sK0)),
inference(resolve,[status(thm)],[c_36,c_32]) ).
cnf(c_46,plain,
~ contracts_from(sK1(sK0),first_movers),
inference(resolve,[status(thm)],[c_36,c_29]) ).
cnf(c_137,negated_conjecture,
( in_environment(sK0,sK1(sK0))
| ~ in_environment(sK0,appear(efficient_producers,sK0)) ),
inference(resolve,[status(thm)],[c_38,c_36]) ).
cnf(c_50,negated_conjecture,
in_environment(sK0,sK1(sK0)),
inference(resolve,[status(thm)],[c_37,c_137]) ).
cnf(c_138,negated_conjecture,
( contracts_from(sK1(sK0),first_movers)
| greater(cardinality_at_time(first_movers,sK2(sK0,sK1(sK0))),zero) ),
inference(resolve,[status(thm)],[c_50,c_41]) ).
cnf(c_55,negated_conjecture,
greater(cardinality_at_time(first_movers,sK2(sK0,sK1(sK0))),zero),
inference(resolve,[status(thm)],[c_46,c_138]) ).
cnf(c_139,negated_conjecture,
( contracts_from(sK1(sK0),first_movers)
| greater_or_equal(sK2(sK0,sK1(sK0)),sK1(sK0)) ),
inference(resolve,[status(thm)],[c_50,c_40]) ).
cnf(c_56,negated_conjecture,
greater_or_equal(sK2(sK0,sK1(sK0)),sK1(sK0)),
inference(resolve,[status(thm)],[c_46,c_139]) ).
cnf(c_140,negated_conjecture,
( contracts_from(sK1(sK0),first_movers)
| ~ greater(zero,growth_rate(first_movers,sK2(sK0,sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_50,c_39]) ).
cnf(c_57,negated_conjecture,
~ greater(zero,growth_rate(first_movers,sK2(sK0,sK1(sK0)))),
inference(resolve,[status(thm)],[c_46,c_140]) ).
cnf(c_58,plain,
( in_environment(sK0,A)
| ~ greater(A,sK1(sK0)) ),
inference(resolve,[status(thm)],[c_50,c_38]) ).
cnf(c_141,negated_conjecture,
( greater(cardinality_at_time(efficient_producers,sK1(sK0)),zero)
| ~ greater_or_equal(sK1(sK0),appear(efficient_producers,sK0)) ),
inference(resolve,[status(thm)],[c_50,c_26]) ).
cnf(c_59,negated_conjecture,
greater(cardinality_at_time(efficient_producers,sK1(sK0)),zero),
inference(resolve,[status(thm)],[c_45,c_141]) ).
cnf(c_142,negated_conjecture,
( subpopulations(first_movers,efficient_producers,sK0,sK1(sK0))
| ~ greater(cardinality_at_time(efficient_producers,sK1(sK0)),zero)
| ~ greater(cardinality_at_time(first_movers,sK1(sK0)),zero) ),
inference(resolve,[status(thm)],[c_50,c_23]) ).
cnf(c_60,negated_conjecture,
( subpopulations(first_movers,efficient_producers,sK0,sK1(sK0))
| ~ greater(cardinality_at_time(first_movers,sK1(sK0)),zero) ),
inference(resolve,[status(thm)],[c_59,c_142]) ).
cnf(c_143,negated_conjecture,
( greater(zero,growth_rate(first_movers,sK2(sK0,sK1(sK0))))
| ~ subpopulations(first_movers,efficient_producers,sK0,sK2(sK0,sK1(sK0))) ),
inference(resolve,[status(thm)],[c_56,c_35]) ).
cnf(c_69,negated_conjecture,
~ subpopulations(first_movers,efficient_producers,sK0,sK2(sK0,sK1(sK0))),
inference(resolve,[status(thm)],[c_57,c_143]) ).
cnf(c_144,plain,
( sK1(sK0) = sK2(sK0,sK1(sK0))
| greater(sK2(sK0,sK1(sK0)),sK1(sK0)) ),
inference(resolve,[status(thm)],[c_56,c_33]) ).
cnf(c_70,plain,
( sK2(sK0,sK1(sK0)) = sK1(sK0)
| greater(sK2(sK0,sK1(sK0)),sK1(sK0)) ),
inference(copy,[status(thm)],[c_144]) ).
cnf(c_145,negated_conjecture,
( subpopulations(first_movers,efficient_producers,sK0,sK2(sK0,sK1(sK0)))
| ~ greater(cardinality_at_time(efficient_producers,sK2(sK0,sK1(sK0))),zero)
| ~ in_environment(sK0,sK2(sK0,sK1(sK0))) ),
inference(resolve,[status(thm)],[c_55,c_23]) ).
cnf(c_75,negated_conjecture,
( ~ greater(cardinality_at_time(efficient_producers,sK2(sK0,sK1(sK0))),zero)
| ~ in_environment(sK0,sK2(sK0,sK1(sK0))) ),
inference(resolve,[status(thm)],[c_69,c_145]) ).
cnf(c_84,plain,
( in_environment(sK0,sK2(sK0,sK1(sK0)))
| sK2(sK0,sK1(sK0)) = sK1(sK0) ),
inference(resolve,[status(thm)],[c_70,c_58]) ).
cnf(c_146,plain,
( ~ greater(cardinality_at_time(efficient_producers,sK1(sK0)),zero)
| ~ in_environment(sK0,sK2(sK0,sK1(sK0)))
| greater(sK2(sK0,sK1(sK0)),sK1(sK0)) ),
inference(paramod,[status(thm)],[c_70,c_75]) ).
cnf(c_93,plain,
( ~ in_environment(sK0,sK2(sK0,sK1(sK0)))
| greater(sK2(sK0,sK1(sK0)),sK1(sK0)) ),
inference(resolve,[status(thm)],[c_59,c_146]) ).
cnf(c_100,plain,
( ~ subpopulations(first_movers,efficient_producers,sK0,sK1(sK0))
| in_environment(sK0,sK2(sK0,sK1(sK0))) ),
inference(paramod,[status(thm)],[c_84,c_69]) ).
cnf(c_101,plain,
( greater(cardinality_at_time(first_movers,sK1(sK0)),zero)
| in_environment(sK0,sK2(sK0,sK1(sK0))) ),
inference(paramod,[status(thm)],[c_84,c_55]) ).
cnf(c_108,plain,
( subpopulations(first_movers,efficient_producers,sK0,sK1(sK0))
| in_environment(sK0,sK2(sK0,sK1(sK0))) ),
inference(resolve,[status(thm)],[c_101,c_60]) ).
cnf(c_147,plain,
( in_environment(sK0,sK2(sK0,sK1(sK0)))
| in_environment(sK0,sK2(sK0,sK1(sK0))) ),
inference(resolve,[status(thm)],[c_108,c_100]) ).
cnf(c_122,plain,
in_environment(sK0,sK2(sK0,sK1(sK0))),
inference(copy,[status(thm)],[c_147]) ).
cnf(c_123,plain,
greater(sK2(sK0,sK1(sK0)),sK1(sK0)),
inference(resolve,[status(thm)],[c_122,c_93]) ).
cnf(c_124,negated_conjecture,
~ greater(cardinality_at_time(efficient_producers,sK2(sK0,sK1(sK0))),zero),
inference(resolve,[status(thm)],[c_122,c_75]) ).
cnf(c_148,negated_conjecture,
( greater(cardinality_at_time(efficient_producers,sK2(sK0,sK1(sK0))),zero)
| ~ greater_or_equal(sK2(sK0,sK1(sK0)),appear(efficient_producers,sK0)) ),
inference(resolve,[status(thm)],[c_122,c_26]) ).
cnf(c_132,negated_conjecture,
~ greater_or_equal(sK2(sK0,sK1(sK0)),appear(efficient_producers,sK0)),
inference(resolve,[status(thm)],[c_124,c_148]) ).
cnf(c_133,plain,
greater(sK2(sK0,sK1(sK0)),appear(efficient_producers,sK0)),
inference(resolve,[status(thm)],[c_123,c_43]) ).
cnf(c_149,plain,
~ greater(sK2(sK0,sK1(sK0)),appear(efficient_producers,sK0)),
inference(resolve,[status(thm)],[c_32,c_132]) ).
cnf(c_136,plain,
$false,
inference(resolve,[status(thm)],[c_133,c_149]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT027+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 00:09:30 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 3626913 was started by sandbox2 on n016,
% 0.09/0.36 % Sat Sep 26 00:09:30 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.37
% 0.09/0.37 % From the command line: assign(max_seconds, 300).
% 0.09/0.38
% 0.09/0.38 % SZS status Theorem for theBenchmark
% 0.09/0.38
% 0.09/0.38 % Proof 1 at 0.01 (+ 0.00) seconds.
% 0.09/0.38 % Length of proof is 64.
% 0.09/0.38 % Level of proof is 13.
% 0.09/0.38 % Maximum clause weight is 22.000.
% 0.09/0.38 % Given clauses 60.
% 0.09/0.38
% 0.09/0.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------