%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : MGT020+1 : TPTP v9.3.1. Released v2.0.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 : n001.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 : Theorem 0.45s 0.74s
% Output : Proof 0.45s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(l3,axiom,
! [E,T] :
( ( subpopulations(first_movers,efficient_producers,E,T)
& environment(E) )
=> ~ decreases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))) ),
file('theBenchmark.p',l3) ).
fof(mp_earliest_time_point,axiom,
! [E,T] :
( environment(E)
=> ( ( subpopulations(first_movers,efficient_producers,E,T)
=> greater_or_equal(T,initial_FM_EP(E)) )
& ( in_environment(E,initial_FM_EP(E))
=> subpopulations(first_movers,efficient_producers,E,initial_FM_EP(E)) ) ) ),
file('theBenchmark.p',mp_earliest_time_point) ).
fof(mp_positive_function_difference,axiom,
! [E,T,T1,T2] :
( ( greater(disbanding_rate(first_movers,T1),disbanding_rate(efficient_producers,T1))
& subpopulations(first_movers,efficient_producers,E,T2)
& greater_or_equal(T2,T)
& greater_or_equal(T,T1)
& environment(E) )
=> ( ~ decreases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T)))
=> greater(disbanding_rate(first_movers,T2),disbanding_rate(efficient_producers,T2)) ) ),
file('theBenchmark.p',mp_positive_function_difference) ).
fof(mp_time_point_occurs,axiom,
! [E,T] :
( ( subpopulations(first_movers,efficient_producers,E,T)
& environment(E) )
=> in_environment(E,T) ),
file('theBenchmark.p',mp_time_point_occurs) ).
fof(mp_initial_time,axiom,
! [E] :
( environment(E)
=> greater_or_equal(initial_FM_EP(E),start_time(E)) ),
file('theBenchmark.p',mp_initial_time) ).
fof(mp_times_in_order,axiom,
! [E,T1,T2] :
( ( in_environment(E,T2)
& greater(T2,T1)
& greater_or_equal(T1,start_time(E))
& environment(E) )
=> in_environment(E,T1) ),
file('theBenchmark.p',mp_times_in_order) ).
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(a8,hypothesis,
! [E] :
( environment(E)
=> greater(disbanding_rate(first_movers,initial_FM_EP(E)),disbanding_rate(efficient_producers,initial_FM_EP(E))) ),
file('theBenchmark.p',a8) ).
fof(a10,hypothesis,
! [E,T1,T2,T] :
( ( greater_or_equal(T2,T)
& greater_or_equal(T,T1)
& subpopulations(first_movers,efficient_producers,E,T2)
& subpopulations(first_movers,efficient_producers,E,T1)
& environment(E) )
=> subpopulations(first_movers,efficient_producers,E,T) ),
file('theBenchmark.p',a10) ).
fof(prove_l2,conjecture,
! [E,T] :
( ( subpopulations(first_movers,efficient_producers,E,T)
& environment(E) )
=> greater(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T)) ),
file('theBenchmark.p',prove_l2) ).
fof(f_1_1,plain,
! [E,T] :
( ~ decreases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T)))
| ~ subpopulations(first_movers,efficient_producers,E,T)
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[l3]) ).
fof(f_1_2,plain,
! [U_1,U_0] :
( ~ decreases(difference(disbanding_rate(first_movers,U_0),disbanding_rate(efficient_producers,U_0)))
| ~ subpopulations(first_movers,efficient_producers,U_1,U_0)
| ~ environment(U_1) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
cnf(f_1_3,plain,
( ~ decreases(difference(disbanding_rate(first_movers,U_0),disbanding_rate(efficient_producers,U_0)))
| ~ subpopulations(first_movers,efficient_producers,U_1,U_0)
| ~ environment(U_1) ),
inference(clausify,[status(thm)],[f_1_2]) ).
fof(f_2_1,plain,
! [E,T] :
( ( ( greater_or_equal(T,initial_FM_EP(E))
| ~ subpopulations(first_movers,efficient_producers,E,T) )
& ( subpopulations(first_movers,efficient_producers,E,initial_FM_EP(E))
| ~ in_environment(E,initial_FM_EP(E)) ) )
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[mp_earliest_time_point]) ).
fof(f_2_2,plain,
! [U_3,U_2] :
( ( ( greater_or_equal(U_2,initial_FM_EP(U_3))
| ~ subpopulations(first_movers,efficient_producers,U_3,U_2) )
& ( subpopulations(first_movers,efficient_producers,U_3,initial_FM_EP(U_3))
| ~ in_environment(U_3,initial_FM_EP(U_3)) ) )
| ~ environment(U_3) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
! [U_3] :
( ( ! [U_2] :
( greater_or_equal(U_2,initial_FM_EP(U_3))
| ~ subpopulations(first_movers,efficient_producers,U_3,U_2) )
& ( subpopulations(first_movers,efficient_producers,U_3,initial_FM_EP(U_3))
| ~ in_environment(U_3,initial_FM_EP(U_3)) ) )
| ~ environment(U_3) ),
inference(miniscope,[status(thm)],[f_2_2]) ).
cnf(f_2_4,plain,
( subpopulations(first_movers,efficient_producers,U_3,initial_FM_EP(U_3))
| ~ in_environment(U_3,initial_FM_EP(U_3))
| ~ environment(U_3) ),
inference(clausify,[status(thm)],[f_2_3]) ).
cnf(f_2_5,plain,
( greater_or_equal(U_2,initial_FM_EP(U_3))
| ~ subpopulations(first_movers,efficient_producers,U_3,U_2)
| ~ environment(U_3) ),
inference(clausify,[status(thm)],[f_2_3]) ).
fof(f_3_1,plain,
! [E,T,T1,T2] :
( greater(disbanding_rate(first_movers,T2),disbanding_rate(efficient_producers,T2))
| decreases(difference(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T)))
| ~ greater(disbanding_rate(first_movers,T1),disbanding_rate(efficient_producers,T1))
| ~ subpopulations(first_movers,efficient_producers,E,T2)
| ~ greater_or_equal(T2,T)
| ~ greater_or_equal(T,T1)
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[mp_positive_function_difference]) ).
fof(f_3_2,plain,
! [U_7,U_6,U_5,U_4] :
( greater(disbanding_rate(first_movers,U_4),disbanding_rate(efficient_producers,U_4))
| decreases(difference(disbanding_rate(first_movers,U_6),disbanding_rate(efficient_producers,U_6)))
| ~ greater(disbanding_rate(first_movers,U_5),disbanding_rate(efficient_producers,U_5))
| ~ subpopulations(first_movers,efficient_producers,U_7,U_4)
| ~ greater_or_equal(U_4,U_6)
| ~ greater_or_equal(U_6,U_5)
| ~ environment(U_7) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
cnf(f_3_3,plain,
( greater(disbanding_rate(first_movers,U_4),disbanding_rate(efficient_producers,U_4))
| decreases(difference(disbanding_rate(first_movers,U_6),disbanding_rate(efficient_producers,U_6)))
| ~ greater(disbanding_rate(first_movers,U_5),disbanding_rate(efficient_producers,U_5))
| ~ subpopulations(first_movers,efficient_producers,U_7,U_4)
| ~ greater_or_equal(U_4,U_6)
| ~ greater_or_equal(U_6,U_5)
| ~ environment(U_7) ),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
! [E,T] :
( in_environment(E,T)
| ~ subpopulations(first_movers,efficient_producers,E,T)
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[mp_time_point_occurs]) ).
fof(f_4_2,plain,
! [U_9,U_8] :
( in_environment(U_9,U_8)
| ~ subpopulations(first_movers,efficient_producers,U_9,U_8)
| ~ environment(U_9) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
cnf(f_4_3,plain,
( in_environment(U_9,U_8)
| ~ subpopulations(first_movers,efficient_producers,U_9,U_8)
| ~ environment(U_9) ),
inference(clausify,[status(thm)],[f_4_2]) ).
fof(f_5_1,plain,
! [E] :
( greater_or_equal(initial_FM_EP(E),start_time(E))
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[mp_initial_time]) ).
fof(f_5_2,plain,
! [U_10] :
( greater_or_equal(initial_FM_EP(U_10),start_time(U_10))
| ~ environment(U_10) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
cnf(f_5_3,plain,
( greater_or_equal(initial_FM_EP(U_10),start_time(U_10))
| ~ environment(U_10) ),
inference(clausify,[status(thm)],[f_5_2]) ).
fof(f_6_1,plain,
! [E,T1,T2] :
( in_environment(E,T1)
| ~ in_environment(E,T2)
| ~ greater(T2,T1)
| ~ greater_or_equal(T1,start_time(E))
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[mp_times_in_order]) ).
fof(f_6_2,plain,
! [U_13,U_12,U_11] :
( in_environment(U_13,U_12)
| ~ in_environment(U_13,U_11)
| ~ greater(U_11,U_12)
| ~ greater_or_equal(U_12,start_time(U_13))
| ~ environment(U_13) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
! [U_13,U_12] :
( ! [U_11] :
( ~ in_environment(U_13,U_11)
| ~ greater(U_11,U_12) )
| ~ greater_or_equal(U_12,start_time(U_13))
| ~ environment(U_13)
| in_environment(U_13,U_12) ),
inference(miniscope,[status(thm)],[f_6_2]) ).
cnf(f_6_4,plain,
( ~ in_environment(U_13,U_11)
| ~ greater(U_11,U_12)
| ~ greater_or_equal(U_12,start_time(U_13))
| ~ environment(U_13)
| in_environment(U_13,U_12) ),
inference(clausify,[status(thm)],[f_6_3]) ).
fof(f_7_1,plain,
! [X,Y,Z] :
( greater(X,Z)
| ~ greater(Y,Z)
| ~ greater(X,Y) ),
inference(fof_nnf,[status(thm)],[mp_greater_transitivity]) ).
fof(f_7_2,plain,
! [U_16,U_15,U_14] :
( greater(U_16,U_14)
| ~ greater(U_15,U_14)
| ~ greater(U_16,U_15) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
cnf(f_7_3,plain,
( greater(U_16,U_14)
| ~ greater(U_15,U_14)
| ~ greater(U_16,U_15) ),
inference(clausify,[status(thm)],[f_7_2]) ).
fof(f_8_1,plain,
! [X,Y] :
( X = Y
| greater(X,Y)
| ~ greater_or_equal(X,Y) ),
inference(fof_nnf,[status(thm)],[mp_greater_or_equal]) ).
fof(f_8_2,plain,
! [U_18,U_17] :
( U_18 = U_17
| greater(U_18,U_17)
| ~ greater_or_equal(U_18,U_17) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
cnf(f_8_3,plain,
( U_18 = U_17
| greater(U_18,U_17)
| ~ greater_or_equal(U_18,U_17) ),
inference(clausify,[status(thm)],[f_8_2]) ).
fof(f_9_1,plain,
! [E] :
( greater(disbanding_rate(first_movers,initial_FM_EP(E)),disbanding_rate(efficient_producers,initial_FM_EP(E)))
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[a8]) ).
fof(f_9_2,plain,
! [U_19] :
( greater(disbanding_rate(first_movers,initial_FM_EP(U_19)),disbanding_rate(efficient_producers,initial_FM_EP(U_19)))
| ~ environment(U_19) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
cnf(f_9_3,plain,
( greater(disbanding_rate(first_movers,initial_FM_EP(U_19)),disbanding_rate(efficient_producers,initial_FM_EP(U_19)))
| ~ environment(U_19) ),
inference(clausify,[status(thm)],[f_9_2]) ).
fof(f_10_1,plain,
! [E,T1,T2,T] :
( subpopulations(first_movers,efficient_producers,E,T)
| ~ greater_or_equal(T2,T)
| ~ greater_or_equal(T,T1)
| ~ subpopulations(first_movers,efficient_producers,E,T2)
| ~ subpopulations(first_movers,efficient_producers,E,T1)
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[a10]) ).
fof(f_10_2,plain,
! [U_23,U_22,U_21,U_20] :
( subpopulations(first_movers,efficient_producers,U_23,U_20)
| ~ greater_or_equal(U_21,U_20)
| ~ greater_or_equal(U_20,U_22)
| ~ subpopulations(first_movers,efficient_producers,U_23,U_21)
| ~ subpopulations(first_movers,efficient_producers,U_23,U_22)
| ~ environment(U_23) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
cnf(f_10_3,plain,
( subpopulations(first_movers,efficient_producers,U_23,U_20)
| ~ greater_or_equal(U_21,U_20)
| ~ greater_or_equal(U_20,U_22)
| ~ subpopulations(first_movers,efficient_producers,U_23,U_21)
| ~ subpopulations(first_movers,efficient_producers,U_23,U_22)
| ~ environment(U_23) ),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,negated_conjecture,
~ ! [E,T] :
( ( subpopulations(first_movers,efficient_producers,E,T)
& environment(E) )
=> greater(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T)) ),
inference(negate,[status(cth)],[prove_l2]) ).
fof(f_11_2,negated_conjecture,
? [E,T] :
( ~ greater(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))
& subpopulations(first_movers,efficient_producers,E,T)
& environment(E) ),
inference(fof_nnf,[status(thm)],[f_11_1]) ).
fof(f_11_3,negated_conjecture,
? [U_25,U_24] :
( ~ greater(disbanding_rate(first_movers,U_24),disbanding_rate(efficient_producers,U_24))
& subpopulations(first_movers,efficient_producers,U_25,U_24)
& environment(U_25) ),
inference(variable_rename,[status(thm)],[f_11_2]) ).
fof(f_11_4,negated_conjecture,
? [U_24] :
( ~ greater(disbanding_rate(first_movers,U_24),disbanding_rate(efficient_producers,U_24))
& subpopulations(first_movers,efficient_producers,sK1,U_24)
& environment(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_25,sK1)],[f_11_3]) ).
fof(f_11_5,negated_conjecture,
( ~ greater(disbanding_rate(first_movers,sK2),disbanding_rate(efficient_producers,sK2))
& subpopulations(first_movers,efficient_producers,sK1,sK2)
& environment(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_24,sK2)],[f_11_4]) ).
fof(f_11_6,negated_conjecture,
( ~ greater(disbanding_rate(first_movers,sK2),disbanding_rate(efficient_producers,sK2))
& subpopulations(first_movers,efficient_producers,sK1,sK2)
& environment(sK1) ),
inference(definitional_conversion,[status(esa)],[f_11_5]) ).
cnf(f_11_7,negated_conjecture,
environment(sK1),
inference(clausify,[status(thm)],[f_11_6]) ).
cnf(f_11_8,negated_conjecture,
subpopulations(first_movers,efficient_producers,sK1,sK2),
inference(clausify,[status(thm)],[f_11_6]) ).
cnf(f_11_9,negated_conjecture,
~ greater(disbanding_rate(first_movers,sK2),disbanding_rate(efficient_producers,sK2)),
inference(clausify,[status(thm)],[f_11_6]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( disbanding_rate(Eq_x_0,Eq_x_1) = disbanding_rate(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( difference(Eq_x_0,Eq_x_1) = difference(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( initial_FM_EP(Eq_x_0) = initial_FM_EP(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( start_time(Eq_x_0) = start_time(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( environment(Eq_y_0)
| ~ environment(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_9,axiom,
( subpopulations(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ subpopulations(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_10,axiom,
( decreases(Eq_y_0)
| ~ decreases(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_11,axiom,
( in_environment(Eq_y_0,Eq_y_1)
| ~ in_environment(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_12,axiom,
( greater_or_equal(Eq_y_0,Eq_y_1)
| ~ greater_or_equal(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_13,axiom,
( greater(Eq_y_0,Eq_y_1)
| ~ greater(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT020+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n001.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sat Sep 19 16:17:11 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.45/0.74 % SZS status Theorem for theBenchmark
% 0.45/0.74 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------