%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : MGT039+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 : n004.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:41 AM UTC 2026
% Result : Theorem 282.06s 282.37s
% Output : Proof 283.31s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(mp3_favoured_trategy,axiom,
! [P] :
( ( ! [E] :
( ( in_environment(P,E)
& environment(E) )
=> selection_favors(efficient_producers,first_movers,end_time(E)) )
& propagation_strategy(efficient_producers)
& propagation_strategy(first_movers)
& observational_period(P) )
=> selection_favors(efficient_producers,first_movers,P) ),
file('theBenchmark.p',mp3_favoured_trategy) ).
fof(mp4_critical_point,axiom,
! [P] :
( ( slow_change(P)
& observational_period(P) )
=> ! [E] :
( ( in_environment(P,E)
& environment(E) )
=> ? [T] :
( greater(T,critical_point(E))
& in_environment(E,T) ) ) ),
file('theBenchmark.p',mp4_critical_point) ).
fof(mp_organizational_sets1,axiom,
propagation_strategy(first_movers),
file('theBenchmark.p',mp_organizational_sets1) ).
fof(mp_organizational_sets2,axiom,
propagation_strategy(efficient_producers),
file('theBenchmark.p',mp_organizational_sets2) ).
fof(mp_time_in_environment,axiom,
! [E,T] :
( ( greater_or_equal(end_time(E),T)
& greater_or_equal(T,start_time(E))
& environment(E) )
=> in_environment(E,T) ),
file('theBenchmark.p',mp_time_in_environment) ).
fof(mp_environment_end_point,axiom,
! [E,T] :
( ( in_environment(E,T)
& environment(E) )
=> greater_or_equal(end_time(E),T) ),
file('theBenchmark.p',mp_environment_end_point) ).
fof(mp_time_of_critical_point,axiom,
! [E] :
( environment(E)
=> greater_or_equal(critical_point(E),start_time(E)) ),
file('theBenchmark.p',mp_time_of_critical_point) ).
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(mp_beginning_and_ending,axiom,
! [E,T] :
( ( ~ greater(T,end_time(E))
& greater(T,start_time(E))
& environment(E) )
=> greater_or_equal(end_time(E),T) ),
file('theBenchmark.p',mp_beginning_and_ending) ).
fof(l8,hypothesis,
! [E,T] :
( ( greater(T,critical_point(E))
& in_environment(E,T)
& environment(E) )
=> selection_favors(efficient_producers,first_movers,T) ),
file('theBenchmark.p',l8) ).
fof(prove_t8,conjecture,
! [P] :
( ( slow_change(P)
& observational_period(P) )
=> selection_favors(efficient_producers,first_movers,P) ),
file('theBenchmark.p',prove_t8) ).
fof(f_1_1,plain,
! [P] :
( selection_favors(efficient_producers,first_movers,P)
| ? [E] :
( ~ selection_favors(efficient_producers,first_movers,end_time(E))
& in_environment(P,E)
& environment(E) )
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(P) ),
inference(fof_nnf,[status(thm)],[mp3_favoured_trategy]) ).
fof(f_1_2,plain,
! [U_1] :
( selection_favors(efficient_producers,first_movers,U_1)
| ? [U_0] :
( ~ selection_favors(efficient_producers,first_movers,end_time(U_0))
& in_environment(U_1,U_0)
& environment(U_0) )
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(U_1) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
! [U_1] :
( selection_favors(efficient_producers,first_movers,U_1)
| ( ~ selection_favors(efficient_producers,first_movers,end_time(sK1(U_1)))
& in_environment(U_1,sK1(U_1))
& environment(sK1(U_1)) )
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(U_1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_0,sK1(U_1))],[f_1_2]) ).
cnf(f_1_4,plain,
( environment(sK1(U_1))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(U_1)
| selection_favors(efficient_producers,first_movers,U_1) ),
inference(clausify,[status(thm)],[f_1_3]) ).
cnf(f_1_5,plain,
( in_environment(U_1,sK1(U_1))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(U_1)
| selection_favors(efficient_producers,first_movers,U_1) ),
inference(clausify,[status(thm)],[f_1_3]) ).
cnf(f_1_6,plain,
( ~ selection_favors(efficient_producers,first_movers,end_time(sK1(U_1)))
| ~ propagation_strategy(efficient_producers)
| ~ propagation_strategy(first_movers)
| ~ observational_period(U_1)
| selection_favors(efficient_producers,first_movers,U_1) ),
inference(clausify,[status(thm)],[f_1_3]) ).
fof(f_2_1,plain,
! [P] :
( ! [E] :
( ? [T] :
( greater(T,critical_point(E))
& in_environment(E,T) )
| ~ in_environment(P,E)
| ~ environment(E) )
| ~ slow_change(P)
| ~ observational_period(P) ),
inference(fof_nnf,[status(thm)],[mp4_critical_point]) ).
fof(f_2_2,plain,
! [U_4] :
( ! [U_3] :
( ? [U_2] :
( greater(U_2,critical_point(U_3))
& in_environment(U_3,U_2) )
| ~ in_environment(U_4,U_3)
| ~ environment(U_3) )
| ~ slow_change(U_4)
| ~ observational_period(U_4) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
! [U_4] :
( ! [U_3] :
( ( greater(sK2(U_4,U_3),critical_point(U_3))
& in_environment(U_3,sK2(U_4,U_3)) )
| ~ in_environment(U_4,U_3)
| ~ environment(U_3) )
| ~ slow_change(U_4)
| ~ observational_period(U_4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_2,sK2(U_4,U_3))],[f_2_2]) ).
cnf(f_2_4,plain,
( in_environment(U_3,sK2(U_4,U_3))
| ~ in_environment(U_4,U_3)
| ~ environment(U_3)
| ~ slow_change(U_4)
| ~ observational_period(U_4) ),
inference(clausify,[status(thm)],[f_2_3]) ).
cnf(f_2_5,plain,
( greater(sK2(U_4,U_3),critical_point(U_3))
| ~ in_environment(U_4,U_3)
| ~ environment(U_3)
| ~ slow_change(U_4)
| ~ observational_period(U_4) ),
inference(clausify,[status(thm)],[f_2_3]) ).
fof(f_3_1,plain,
propagation_strategy(first_movers),
inference(fof_nnf,[status(thm)],[mp_organizational_sets1]) ).
cnf(f_3_2,plain,
propagation_strategy(first_movers),
inference(clausify,[status(thm)],[f_3_1]) ).
fof(f_4_1,plain,
propagation_strategy(efficient_producers),
inference(fof_nnf,[status(thm)],[mp_organizational_sets2]) ).
cnf(f_4_2,plain,
propagation_strategy(efficient_producers),
inference(clausify,[status(thm)],[f_4_1]) ).
fof(f_5_1,plain,
! [E,T] :
( in_environment(E,T)
| ~ greater_or_equal(end_time(E),T)
| ~ greater_or_equal(T,start_time(E))
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[mp_time_in_environment]) ).
fof(f_5_2,plain,
! [U_6,U_5] :
( in_environment(U_6,U_5)
| ~ greater_or_equal(end_time(U_6),U_5)
| ~ greater_or_equal(U_5,start_time(U_6))
| ~ environment(U_6) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
cnf(f_5_3,plain,
( in_environment(U_6,U_5)
| ~ greater_or_equal(end_time(U_6),U_5)
| ~ greater_or_equal(U_5,start_time(U_6))
| ~ environment(U_6) ),
inference(clausify,[status(thm)],[f_5_2]) ).
fof(f_6_1,plain,
! [E,T] :
( greater_or_equal(end_time(E),T)
| ~ in_environment(E,T)
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[mp_environment_end_point]) ).
fof(f_6_2,plain,
! [U_8,U_7] :
( greater_or_equal(end_time(U_8),U_7)
| ~ in_environment(U_8,U_7)
| ~ environment(U_8) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
cnf(f_6_3,plain,
( greater_or_equal(end_time(U_8),U_7)
| ~ in_environment(U_8,U_7)
| ~ environment(U_8) ),
inference(clausify,[status(thm)],[f_6_2]) ).
fof(f_7_1,plain,
! [E] :
( greater_or_equal(critical_point(E),start_time(E))
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[mp_time_of_critical_point]) ).
fof(f_7_2,plain,
! [U_9] :
( greater_or_equal(critical_point(U_9),start_time(U_9))
| ~ environment(U_9) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
cnf(f_7_3,plain,
( greater_or_equal(critical_point(U_9),start_time(U_9))
| ~ environment(U_9) ),
inference(clausify,[status(thm)],[f_7_2]) ).
fof(f_8_1,plain,
! [X,Y,Z] :
( greater(X,Z)
| ~ greater(Y,Z)
| ~ greater(X,Y) ),
inference(fof_nnf,[status(thm)],[mp_greater_transitivity]) ).
fof(f_8_2,plain,
! [U_12,U_11,U_10] :
( greater(U_12,U_10)
| ~ greater(U_11,U_10)
| ~ greater(U_12,U_11) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
cnf(f_8_3,plain,
( greater(U_12,U_10)
| ~ greater(U_11,U_10)
| ~ greater(U_12,U_11) ),
inference(clausify,[status(thm)],[f_8_2]) ).
fof(f_9_1,plain,
! [X,Y] :
( ( greater_or_equal(X,Y)
| ( X != Y
& ~ greater(X,Y) ) )
& ( X = Y
| greater(X,Y)
| ~ greater_or_equal(X,Y) ) ),
inference(fof_nnf,[status(thm)],[mp_greater_or_equal]) ).
fof(f_9_2,plain,
! [U_14,U_13] :
( ( greater_or_equal(U_14,U_13)
| ( U_14 != U_13
& ~ greater(U_14,U_13) ) )
& ( U_14 = U_13
| greater(U_14,U_13)
| ~ greater_or_equal(U_14,U_13) ) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
( ! [U_18,U_16] :
( greater_or_equal(U_18,U_16)
| ( U_18 != U_16
& ~ greater(U_18,U_16) ) )
& ! [U_17,U_15] :
( U_17 = U_15
| greater(U_17,U_15)
| ~ greater_or_equal(U_17,U_15) ) ),
inference(miniscope,[status(thm)],[f_9_2]) ).
cnf(f_9_4,plain,
( U_17 = U_15
| greater(U_17,U_15)
| ~ greater_or_equal(U_17,U_15) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_5,plain,
( ~ greater(U_18,U_16)
| greater_or_equal(U_18,U_16) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_6,plain,
( U_18 != U_16
| greater_or_equal(U_18,U_16) ),
inference(clausify,[status(thm)],[f_9_3]) ).
fof(f_10_1,plain,
! [E,T] :
( greater_or_equal(end_time(E),T)
| greater(T,end_time(E))
| ~ greater(T,start_time(E))
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[mp_beginning_and_ending]) ).
fof(f_10_2,plain,
! [U_20,U_19] :
( greater_or_equal(end_time(U_20),U_19)
| greater(U_19,end_time(U_20))
| ~ greater(U_19,start_time(U_20))
| ~ environment(U_20) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
cnf(f_10_3,plain,
( greater_or_equal(end_time(U_20),U_19)
| greater(U_19,end_time(U_20))
| ~ greater(U_19,start_time(U_20))
| ~ environment(U_20) ),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,plain,
! [E,T] :
( selection_favors(efficient_producers,first_movers,T)
| ~ greater(T,critical_point(E))
| ~ in_environment(E,T)
| ~ environment(E) ),
inference(fof_nnf,[status(thm)],[l8]) ).
fof(f_11_2,plain,
! [U_22,U_21] :
( selection_favors(efficient_producers,first_movers,U_21)
| ~ greater(U_21,critical_point(U_22))
| ~ in_environment(U_22,U_21)
| ~ environment(U_22) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
cnf(f_11_3,plain,
( selection_favors(efficient_producers,first_movers,U_21)
| ~ greater(U_21,critical_point(U_22))
| ~ in_environment(U_22,U_21)
| ~ environment(U_22) ),
inference(clausify,[status(thm)],[f_11_2]) ).
fof(f_12_1,negated_conjecture,
~ ! [P] :
( ( slow_change(P)
& observational_period(P) )
=> selection_favors(efficient_producers,first_movers,P) ),
inference(negate,[status(cth)],[prove_t8]) ).
fof(f_12_2,negated_conjecture,
? [P] :
( ~ selection_favors(efficient_producers,first_movers,P)
& slow_change(P)
& observational_period(P) ),
inference(fof_nnf,[status(thm)],[f_12_1]) ).
fof(f_12_3,negated_conjecture,
? [U_23] :
( ~ selection_favors(efficient_producers,first_movers,U_23)
& slow_change(U_23)
& observational_period(U_23) ),
inference(variable_rename,[status(thm)],[f_12_2]) ).
fof(f_12_4,negated_conjecture,
( ~ selection_favors(efficient_producers,first_movers,sK3)
& slow_change(sK3)
& observational_period(sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_23,sK3)],[f_12_3]) ).
cnf(f_12_5,negated_conjecture,
observational_period(sK3),
inference(clausify,[status(thm)],[f_12_4]) ).
cnf(f_12_6,negated_conjecture,
slow_change(sK3),
inference(clausify,[status(thm)],[f_12_4]) ).
cnf(f_12_7,negated_conjecture,
~ selection_favors(efficient_producers,first_movers,sK3),
inference(clausify,[status(thm)],[f_12_4]) ).
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,
( end_time(Eq_x_0) = end_time(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( critical_point(Eq_x_0) = critical_point(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( start_time(Eq_x_0) = start_time(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( sK1(Eq_x_0) = sK1(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( sK2(Eq_x_0,Eq_x_1) = sK2(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( observational_period(Eq_y_0)
| ~ observational_period(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_10,axiom,
( propagation_strategy(Eq_y_0)
| ~ propagation_strategy(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_11,axiom,
( environment(Eq_y_0)
| ~ environment(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_12,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_13,axiom,
( selection_favors(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ selection_favors(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_14,axiom,
( slow_change(Eq_y_0)
| ~ slow_change(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_15,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(equality_16,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(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT039+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.03 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n004.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 19 16:14:49 UTC 2026
% 0.08/0.35 % CPUTime :
% 282.06/282.37 % SZS status Theorem for theBenchmark
% 282.06/282.37 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------