%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : MGT021-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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 : Thu Sep 24 08:50:36 AM UTC 2026
% Result : Unsatisfiable 0.02s 0.32s
% Output : Proof 0.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 10
% Syntax : Number of clauses : 60 ( 44 unt; 2 nHn; 60 RR)
% Number of literals : 102 ( 0 equ; 44 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 13 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(mp_time_point_in_environment_27,axiom,
( in_environment(A,B)
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ environment(A) ),
file('theBenchmark.p',mp_time_point_in_environment_27) ).
cnf(mp_environment_not_empty_28,axiom,
( greater(number_of_organizations(A,B),zero)
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ environment(A) ),
file('theBenchmark.p',mp_environment_not_empty_28) ).
cnf(mp_increase_not_decrease_29,axiom,
( ~ decreases(A)
| ~ increases(A) ),
file('theBenchmark.p',mp_increase_not_decrease_29) ).
cnf(a3_31,hypothesis,
( decreases(resources(A,B))
| ~ greater(equilibrium(A),B)
| ~ greater(number_of_organizations(A,B),zero)
| ~ in_environment(A,B)
| ~ environment(A) ),
file('theBenchmark.p',a3_31) ).
cnf(a3_32,hypothesis,
( constant(resources(A,B))
| greater(equilibrium(A),B)
| ~ greater(number_of_organizations(A,B),zero)
| ~ in_environment(A,B)
| ~ environment(A) ),
file('theBenchmark.p',a3_32) ).
cnf(l4_33,hypothesis,
( increases(difference(disbanding_rate(first_movers,B),disbanding_rate(efficient_producers,B)))
| ~ decreases(resources(A,B))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ environment(A) ),
file('theBenchmark.p',l4_33) ).
cnf(l4_34,hypothesis,
( ~ decreases(difference(disbanding_rate(first_movers,B),disbanding_rate(efficient_producers,B)))
| ~ constant(resources(A,B))
| ~ subpopulations(first_movers,efficient_producers,A,B)
| ~ environment(A) ),
file('theBenchmark.p',l4_34) ).
cnf(prove_l3_35,negated_conjecture,
environment(sk1),
file('theBenchmark.p',prove_l3_35) ).
cnf(prove_l3_36,negated_conjecture,
subpopulations(first_movers,efficient_producers,sk1,sk2),
file('theBenchmark.p',prove_l3_36) ).
cnf(prove_l3_37,negated_conjecture,
decreases(difference(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2))),
file('theBenchmark.p',prove_l3_37) ).
cnf(t1,plain,
( ~ decreases(difference(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2)))
| ~ increases(difference(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2))) ),
inference(start,[status(thm),parent(0:0)],[mp_increase_not_decrease_29]) ).
cnf(t2,plain,
( ~ subpopulations(first_movers,efficient_producers,sk1,sk2)
| ~ decreases(resources(sk1,sk2))
| ~ environment(sk1)
| increases(difference(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2))) ),
inference(extension,[status(thm),parent(t1:1)],[l4_33]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
environment(sk1),
inference(extension,[status(thm),parent(t2:2)],[prove_l3_35]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(l2,lemma,
environment(sk1),
inference(lemma,[status(cth),parent(t2:2),below(t1:1)],[t2:2]) ).
cnf(t6,plain,
( ~ in_environment(sk1,sk2)
| ~ greater(number_of_organizations(sk1,sk2),zero)
| ~ greater(equilibrium(sk1),sk2)
| ~ environment(sk1)
| decreases(resources(sk1,sk2)) ),
inference(extension,[status(thm),parent(t2:3)],[a3_31]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t2:3]) ).
cnf(t8,plain,
environment(sk1),
inference(lemma_extension,[status(thm),parent(t6:2)],[l2:1]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
( ~ in_environment(sk1,sk2)
| ~ greater(number_of_organizations(sk1,sk2),zero)
| constant(resources(sk1,sk2))
| ~ environment(sk1)
| greater(equilibrium(sk1),sk2) ),
inference(extension,[status(thm),parent(t6:3)],[a3_32]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t6:3]) ).
cnf(t12,plain,
environment(sk1),
inference(lemma_extension,[status(thm),parent(t10:2)],[l2:1]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t10:2]) ).
cnf(t14,plain,
( ~ subpopulations(first_movers,efficient_producers,sk1,sk2)
| ~ decreases(difference(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2)))
| ~ environment(sk1)
| ~ constant(resources(sk1,sk2)) ),
inference(extension,[status(thm),parent(t10:3)],[l4_34]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t10:3]) ).
cnf(t16,plain,
environment(sk1),
inference(lemma_extension,[status(thm),parent(t14:2)],[l2:1]) ).
cnf(t17,plain,
$false,
inference(connection,[status(thm),parent(t16:1)],[t16:1,t14:2]) ).
cnf(t18,plain,
decreases(difference(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2))),
inference(extension,[status(thm),parent(t14:3)],[prove_l3_37]) ).
cnf(t19,plain,
$false,
inference(connection,[status(thm),parent(t18:1)],[t18:1,t14:3]) ).
cnf(t20,plain,
subpopulations(first_movers,efficient_producers,sk1,sk2),
inference(extension,[status(thm),parent(t14:4)],[prove_l3_36]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t14:4]) ).
cnf(t22,plain,
( ~ subpopulations(first_movers,efficient_producers,sk1,sk2)
| ~ environment(sk1)
| greater(number_of_organizations(sk1,sk2),zero) ),
inference(extension,[status(thm),parent(t10:4)],[mp_environment_not_empty_28]) ).
cnf(t23,plain,
$false,
inference(connection,[status(thm),parent(t22:1)],[t22:1,t10:4]) ).
cnf(t24,plain,
environment(sk1),
inference(lemma_extension,[status(thm),parent(t22:2)],[l2:1]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t22:2]) ).
cnf(t26,plain,
subpopulations(first_movers,efficient_producers,sk1,sk2),
inference(extension,[status(thm),parent(t22:3)],[prove_l3_36]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t22:3]) ).
cnf(t28,plain,
( ~ subpopulations(first_movers,efficient_producers,sk1,sk2)
| ~ environment(sk1)
| in_environment(sk1,sk2) ),
inference(extension,[status(thm),parent(t10:5)],[mp_time_point_in_environment_27]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t10:5]) ).
cnf(t30,plain,
environment(sk1),
inference(lemma_extension,[status(thm),parent(t28:2)],[l2:1]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t28:2]) ).
cnf(t32,plain,
subpopulations(first_movers,efficient_producers,sk1,sk2),
inference(extension,[status(thm),parent(t28:3)],[prove_l3_36]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t28:3]) ).
cnf(t34,plain,
( ~ subpopulations(first_movers,efficient_producers,sk1,sk2)
| ~ environment(sk1)
| greater(number_of_organizations(sk1,sk2),zero) ),
inference(extension,[status(thm),parent(t6:4)],[mp_environment_not_empty_28]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t6:4]) ).
cnf(t36,plain,
environment(sk1),
inference(lemma_extension,[status(thm),parent(t34:2)],[l2:1]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t34:2]) ).
cnf(t38,plain,
subpopulations(first_movers,efficient_producers,sk1,sk2),
inference(extension,[status(thm),parent(t34:3)],[prove_l3_36]) ).
cnf(t39,plain,
$false,
inference(connection,[status(thm),parent(t38:1)],[t38:1,t34:3]) ).
cnf(t40,plain,
( ~ subpopulations(first_movers,efficient_producers,sk1,sk2)
| ~ environment(sk1)
| in_environment(sk1,sk2) ),
inference(extension,[status(thm),parent(t6:5)],[mp_time_point_in_environment_27]) ).
cnf(t41,plain,
$false,
inference(connection,[status(thm),parent(t40:1)],[t40:1,t6:5]) ).
cnf(t42,plain,
environment(sk1),
inference(lemma_extension,[status(thm),parent(t40:2)],[l2:1]) ).
cnf(t43,plain,
$false,
inference(connection,[status(thm),parent(t42:1)],[t42:1,t40:2]) ).
cnf(t44,plain,
subpopulations(first_movers,efficient_producers,sk1,sk2),
inference(extension,[status(thm),parent(t40:3)],[prove_l3_36]) ).
cnf(t45,plain,
$false,
inference(connection,[status(thm),parent(t44:1)],[t44:1,t40:3]) ).
cnf(t46,plain,
subpopulations(first_movers,efficient_producers,sk1,sk2),
inference(extension,[status(thm),parent(t2:4)],[prove_l3_36]) ).
cnf(t47,plain,
$false,
inference(connection,[status(thm),parent(t46:1)],[t46:1,t2:4]) ).
cnf(t48,plain,
decreases(difference(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2))),
inference(extension,[status(thm),parent(t1:2)],[prove_l3_37]) ).
cnf(t49,plain,
$false,
inference(connection,[status(thm),parent(t48:1)],[t48:1,t1:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : MGT021-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.01 This is a CNF_UNS_RFO_SEQ_NHN problem
% 0.00/0.02 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.02/0.29 % Computer : n012.cluster.edu
% 0.02/0.29 % Model : x86_64 x86_64
% 0.02/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.29 % Memory : 8046.5625MB
% 0.02/0.29 % OS : Linux 6.8.0-71-generic
% 0.02/0.29 % CPULimit : 300
% 0.02/0.29 % WCLimit : 300
% 0.02/0.29 % DateTime : Sat Sep 19 16:11:37 UTC 2026
% 0.02/0.29 % CPUTime :
% 0.02/0.32 % SZS status Unsatisfiable for theBenchmark
% 0.02/0.32 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------