%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : MGT001+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 : n002.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:31 AM UTC 2026
% Result : Theorem 31.04s 31.30s
% Output : Proof 31.04s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(mp1,axiom,
! [X,T] :
( organization(X,T)
=> ? [R] : reliability(X,R,T) ),
file('theBenchmark.p',mp1) ).
fof(mp2,axiom,
! [X,T] :
( organization(X,T)
=> ? [A] : accountability(X,A,T) ),
file('theBenchmark.p',mp2) ).
fof(mp3,axiom,
! [X,T] :
( organization(X,T)
=> ? [Rp] : reproducibility(X,Rp,T) ),
file('theBenchmark.p',mp3) ).
fof(a1_FOL,hypothesis,
! [X,Y,R1,R2,A1,A2,P1,P2,T1,T2] :
( ( greater(A2,A1)
& greater(R2,R1)
& survival_chance(Y,P2,T2)
& survival_chance(X,P1,T1)
& accountability(Y,A2,T2)
& accountability(X,A1,T1)
& reliability(Y,R2,T2)
& reliability(X,R1,T1)
& organization(Y,T2)
& organization(X,T1) )
=> greater(P2,P1) ),
file('theBenchmark.p',a1_FOL) ).
fof(a2_FOL,hypothesis,
! [X,Y,T1,T2,R1,R2,A1,A2,Rp1,Rp2] :
( ( reproducibility(Y,Rp2,T2)
& reproducibility(X,Rp1,T1)
& accountability(Y,A2,T2)
& accountability(X,A1,T1)
& reliability(Y,R2,T2)
& reliability(X,R1,T1)
& organization(Y,T2)
& organization(X,T1) )
=> ( greater(Rp2,Rp1)
<=> ( greater(A2,A1)
& greater(R2,R1) ) ) ),
file('theBenchmark.p',a2_FOL) ).
fof(a3_FOL,hypothesis,
! [X,Y,T1,T2,Rp1,Rp2,I1,I2] :
( ( inertia(Y,I2,T2)
& inertia(X,I1,T1)
& reproducibility(Y,Rp2,T2)
& reproducibility(X,Rp1,T1)
& reorganization_free(Y,T2,T2)
& reorganization_free(X,T1,T1)
& organization(Y,T2)
& organization(X,T1) )
=> ( greater(Rp2,Rp1)
<=> greater(I2,I1) ) ),
file('theBenchmark.p',a3_FOL) ).
fof(t1_FOL,conjecture,
! [X,Y,T1,T2,I1,I2,P1,P2] :
( ( greater(I2,I1)
& survival_chance(Y,P2,T2)
& survival_chance(X,P1,T1)
& inertia(Y,I2,T2)
& inertia(X,I1,T1)
& reorganization_free(Y,T2,T2)
& reorganization_free(X,T1,T1)
& organization(Y,T2)
& organization(X,T1) )
=> greater(P2,P1) ),
file('theBenchmark.p',t1_FOL) ).
fof(f_1_1,plain,
! [X,T] :
( ? [R] : reliability(X,R,T)
| ~ organization(X,T) ),
inference(fof_nnf,[status(thm)],[mp1]) ).
fof(f_1_2,plain,
! [U_2,U_1] :
( ? [U_0] : reliability(U_2,U_0,U_1)
| ~ organization(U_2,U_1) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
! [U_2,U_1] :
( reliability(U_2,sK1(U_2,U_1),U_1)
| ~ organization(U_2,U_1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_0,sK1(U_2,U_1))],[f_1_2]) ).
fof(f_1_4,plain,
! [U_1,U_2] :
( reliability(U_2,sK1(U_2,U_1),U_1)
| ~ organization(U_2,U_1) ),
inference(definitional_conversion,[status(esa)],[f_1_3]) ).
cnf(f_1_5,plain,
( reliability(U_2,sK1(U_2,U_1),U_1)
| ~ organization(U_2,U_1) ),
inference(clausify,[status(thm)],[f_1_4]) ).
fof(f_2_1,plain,
! [X,T] :
( ? [A] : accountability(X,A,T)
| ~ organization(X,T) ),
inference(fof_nnf,[status(thm)],[mp2]) ).
fof(f_2_2,plain,
! [U_5,U_4] :
( ? [U_3] : accountability(U_5,U_3,U_4)
| ~ organization(U_5,U_4) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
! [U_5,U_4] :
( accountability(U_5,sK2(U_5,U_4),U_4)
| ~ organization(U_5,U_4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_3,sK2(U_5,U_4))],[f_2_2]) ).
fof(f_2_4,plain,
! [U_4,U_5] :
( accountability(U_5,sK2(U_5,U_4),U_4)
| ~ organization(U_5,U_4) ),
inference(definitional_conversion,[status(esa)],[f_2_3]) ).
cnf(f_2_5,plain,
( accountability(U_5,sK2(U_5,U_4),U_4)
| ~ organization(U_5,U_4) ),
inference(clausify,[status(thm)],[f_2_4]) ).
fof(f_3_1,plain,
! [X,T] :
( ? [Rp] : reproducibility(X,Rp,T)
| ~ organization(X,T) ),
inference(fof_nnf,[status(thm)],[mp3]) ).
fof(f_3_2,plain,
! [U_8,U_7] :
( ? [U_6] : reproducibility(U_8,U_6,U_7)
| ~ organization(U_8,U_7) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
! [U_8,U_7] :
( reproducibility(U_8,sK3(U_8,U_7),U_7)
| ~ organization(U_8,U_7) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_6,sK3(U_8,U_7))],[f_3_2]) ).
fof(f_3_4,plain,
! [U_7,U_8] :
( reproducibility(U_8,sK3(U_8,U_7),U_7)
| ~ organization(U_8,U_7) ),
inference(definitional_conversion,[status(esa)],[f_3_3]) ).
cnf(f_3_5,plain,
( reproducibility(U_8,sK3(U_8,U_7),U_7)
| ~ organization(U_8,U_7) ),
inference(clausify,[status(thm)],[f_3_4]) ).
fof(f_4_1,plain,
! [X,Y,R1,R2,A1,A2,P1,P2,T1,T2] :
( greater(P2,P1)
| ~ greater(A2,A1)
| ~ greater(R2,R1)
| ~ survival_chance(Y,P2,T2)
| ~ survival_chance(X,P1,T1)
| ~ accountability(Y,A2,T2)
| ~ accountability(X,A1,T1)
| ~ reliability(Y,R2,T2)
| ~ reliability(X,R1,T1)
| ~ organization(Y,T2)
| ~ organization(X,T1) ),
inference(fof_nnf,[status(thm)],[a1_FOL]) ).
fof(f_4_2,plain,
! [U_18,U_17,U_16,U_15,U_14,U_13,U_12,U_11,U_10,U_9] :
( greater(U_11,U_12)
| ~ greater(U_13,U_14)
| ~ greater(U_15,U_16)
| ~ survival_chance(U_17,U_11,U_9)
| ~ survival_chance(U_18,U_12,U_10)
| ~ accountability(U_17,U_13,U_9)
| ~ accountability(U_18,U_14,U_10)
| ~ reliability(U_17,U_15,U_9)
| ~ reliability(U_18,U_16,U_10)
| ~ organization(U_17,U_9)
| ~ organization(U_18,U_10) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
! [U_18,U_17,U_16,U_15,U_14,U_13,U_12,U_11] :
( ! [U_10] :
( ~ survival_chance(U_18,U_12,U_10)
| ~ accountability(U_18,U_14,U_10)
| ~ reliability(U_18,U_16,U_10)
| ~ organization(U_18,U_10) )
| ! [U_9] :
( ~ survival_chance(U_17,U_11,U_9)
| ~ accountability(U_17,U_13,U_9)
| ~ reliability(U_17,U_15,U_9)
| ~ organization(U_17,U_9) )
| ~ greater(U_13,U_14)
| ~ greater(U_15,U_16)
| greater(U_11,U_12) ),
inference(miniscope,[status(thm)],[f_4_2]) ).
fof(f_4_4,plain,
! [U_12,U_9,U_10,U_11,U_13,U_14,U_15,U_16,U_17,U_18] :
( ~ survival_chance(U_18,U_12,U_10)
| ~ accountability(U_18,U_14,U_10)
| ~ reliability(U_18,U_16,U_10)
| ~ organization(U_18,U_10)
| ~ survival_chance(U_17,U_11,U_9)
| ~ accountability(U_17,U_13,U_9)
| ~ reliability(U_17,U_15,U_9)
| ~ organization(U_17,U_9)
| ~ greater(U_13,U_14)
| ~ greater(U_15,U_16)
| greater(U_11,U_12) ),
inference(definitional_conversion,[status(esa)],[f_4_3]) ).
cnf(f_4_5,plain,
( ~ survival_chance(U_18,U_12,U_10)
| ~ accountability(U_18,U_14,U_10)
| ~ reliability(U_18,U_16,U_10)
| ~ organization(U_18,U_10)
| ~ survival_chance(U_17,U_11,U_9)
| ~ accountability(U_17,U_13,U_9)
| ~ reliability(U_17,U_15,U_9)
| ~ organization(U_17,U_9)
| ~ greater(U_13,U_14)
| ~ greater(U_15,U_16)
| greater(U_11,U_12) ),
inference(clausify,[status(thm)],[f_4_4]) ).
fof(f_5_1,plain,
! [X,Y,T1,T2,R1,R2,A1,A2,Rp1,Rp2] :
( ( ( greater(Rp2,Rp1)
| ~ greater(A2,A1)
| ~ greater(R2,R1) )
& ( ( greater(A2,A1)
& greater(R2,R1) )
| ~ greater(Rp2,Rp1) ) )
| ~ reproducibility(Y,Rp2,T2)
| ~ reproducibility(X,Rp1,T1)
| ~ accountability(Y,A2,T2)
| ~ accountability(X,A1,T1)
| ~ reliability(Y,R2,T2)
| ~ reliability(X,R1,T1)
| ~ organization(Y,T2)
| ~ organization(X,T1) ),
inference(fof_nnf,[status(thm)],[a2_FOL]) ).
fof(f_5_2,plain,
! [U_28,U_27,U_26,U_25,U_24,U_23,U_22,U_21,U_20,U_19] :
( ( ( greater(U_19,U_20)
| ~ greater(U_21,U_22)
| ~ greater(U_23,U_24) )
& ( ( greater(U_21,U_22)
& greater(U_23,U_24) )
| ~ greater(U_19,U_20) ) )
| ~ reproducibility(U_27,U_19,U_25)
| ~ reproducibility(U_28,U_20,U_26)
| ~ accountability(U_27,U_21,U_25)
| ~ accountability(U_28,U_22,U_26)
| ~ reliability(U_27,U_23,U_25)
| ~ reliability(U_28,U_24,U_26)
| ~ organization(U_27,U_25)
| ~ organization(U_28,U_26) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
( ! [U_21,U_23,U_24,U_22] :
( greater(U_21,U_22)
| ~ sP0(U_21,U_23,U_24,U_22) )
& ! [U_21,U_23,U_24,U_22] :
( greater(U_23,U_24)
| ~ sP0(U_21,U_23,U_24,U_22) )
& ! [U_19,U_21,U_23,U_24,U_22,U_20] :
( greater(U_19,U_20)
| ~ greater(U_21,U_22)
| ~ greater(U_23,U_24)
| ~ sP1(U_19,U_21,U_23,U_24,U_22,U_20) )
& ! [U_19,U_21,U_23,U_24,U_22,U_20] :
( sP0(U_21,U_23,U_24,U_22)
| ~ greater(U_19,U_20)
| ~ sP1(U_19,U_21,U_23,U_24,U_22,U_20) )
& ! [U_19,U_21,U_23,U_24,U_26,U_22,U_27,U_20,U_25,U_28] :
( sP1(U_19,U_21,U_23,U_24,U_22,U_20)
| ~ reproducibility(U_27,U_19,U_25)
| ~ reproducibility(U_28,U_20,U_26)
| ~ accountability(U_27,U_21,U_25)
| ~ accountability(U_28,U_22,U_26)
| ~ reliability(U_27,U_23,U_25)
| ~ reliability(U_28,U_24,U_26)
| ~ organization(U_27,U_25)
| ~ organization(U_28,U_26) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1])],[f_5_2]) ).
cnf(f_5_4,plain,
( sP1(U_19,U_21,U_23,U_24,U_22,U_20)
| ~ reproducibility(U_27,U_19,U_25)
| ~ reproducibility(U_28,U_20,U_26)
| ~ accountability(U_27,U_21,U_25)
| ~ accountability(U_28,U_22,U_26)
| ~ reliability(U_27,U_23,U_25)
| ~ reliability(U_28,U_24,U_26)
| ~ organization(U_27,U_25)
| ~ organization(U_28,U_26) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(f_5_5,plain,
( sP0(U_21,U_23,U_24,U_22)
| ~ greater(U_19,U_20)
| ~ sP1(U_19,U_21,U_23,U_24,U_22,U_20) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(f_5_6,plain,
( greater(U_19,U_20)
| ~ greater(U_21,U_22)
| ~ greater(U_23,U_24)
| ~ sP1(U_19,U_21,U_23,U_24,U_22,U_20) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(f_5_7,plain,
( greater(U_23,U_24)
| ~ sP0(U_21,U_23,U_24,U_22) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(f_5_8,plain,
( greater(U_21,U_22)
| ~ sP0(U_21,U_23,U_24,U_22) ),
inference(clausify,[status(thm)],[f_5_3]) ).
fof(f_6_1,plain,
! [X,Y,T1,T2,Rp1,Rp2,I1,I2] :
( ( ( greater(Rp2,Rp1)
| ~ greater(I2,I1) )
& ( greater(I2,I1)
| ~ greater(Rp2,Rp1) ) )
| ~ inertia(Y,I2,T2)
| ~ inertia(X,I1,T1)
| ~ reproducibility(Y,Rp2,T2)
| ~ reproducibility(X,Rp1,T1)
| ~ reorganization_free(Y,T2,T2)
| ~ reorganization_free(X,T1,T1)
| ~ organization(Y,T2)
| ~ organization(X,T1) ),
inference(fof_nnf,[status(thm)],[a3_FOL]) ).
fof(f_6_2,plain,
! [U_36,U_35,U_34,U_33,U_32,U_31,U_30,U_29] :
( ( ( greater(U_31,U_32)
| ~ greater(U_29,U_30) )
& ( greater(U_29,U_30)
| ~ greater(U_31,U_32) ) )
| ~ inertia(U_35,U_29,U_33)
| ~ inertia(U_36,U_30,U_34)
| ~ reproducibility(U_35,U_31,U_33)
| ~ reproducibility(U_36,U_32,U_34)
| ~ reorganization_free(U_35,U_33,U_33)
| ~ reorganization_free(U_36,U_34,U_34)
| ~ organization(U_35,U_33)
| ~ organization(U_36,U_34) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
( ! [U_31,U_32,U_29,U_30] :
( greater(U_31,U_32)
| ~ greater(U_29,U_30)
| ~ sP2(U_31,U_32,U_29,U_30) )
& ! [U_31,U_32,U_29,U_30] :
( greater(U_29,U_30)
| ~ greater(U_31,U_32)
| ~ sP2(U_31,U_32,U_29,U_30) )
& ! [U_31,U_34,U_36,U_33,U_35,U_32,U_29,U_30] :
( sP2(U_31,U_32,U_29,U_30)
| ~ inertia(U_35,U_29,U_33)
| ~ inertia(U_36,U_30,U_34)
| ~ reproducibility(U_35,U_31,U_33)
| ~ reproducibility(U_36,U_32,U_34)
| ~ reorganization_free(U_35,U_33,U_33)
| ~ reorganization_free(U_36,U_34,U_34)
| ~ organization(U_35,U_33)
| ~ organization(U_36,U_34) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP2])],[f_6_2]) ).
cnf(f_6_4,plain,
( sP2(U_31,U_32,U_29,U_30)
| ~ inertia(U_35,U_29,U_33)
| ~ inertia(U_36,U_30,U_34)
| ~ reproducibility(U_35,U_31,U_33)
| ~ reproducibility(U_36,U_32,U_34)
| ~ reorganization_free(U_35,U_33,U_33)
| ~ reorganization_free(U_36,U_34,U_34)
| ~ organization(U_35,U_33)
| ~ organization(U_36,U_34) ),
inference(clausify,[status(thm)],[f_6_3]) ).
cnf(f_6_5,plain,
( greater(U_29,U_30)
| ~ greater(U_31,U_32)
| ~ sP2(U_31,U_32,U_29,U_30) ),
inference(clausify,[status(thm)],[f_6_3]) ).
cnf(f_6_6,plain,
( greater(U_31,U_32)
| ~ greater(U_29,U_30)
| ~ sP2(U_31,U_32,U_29,U_30) ),
inference(clausify,[status(thm)],[f_6_3]) ).
fof(f_7_1,negated_conjecture,
~ ! [X,Y,T1,T2,I1,I2,P1,P2] :
( ( greater(I2,I1)
& survival_chance(Y,P2,T2)
& survival_chance(X,P1,T1)
& inertia(Y,I2,T2)
& inertia(X,I1,T1)
& reorganization_free(Y,T2,T2)
& reorganization_free(X,T1,T1)
& organization(Y,T2)
& organization(X,T1) )
=> greater(P2,P1) ),
inference(negate,[status(cth)],[t1_FOL]) ).
fof(f_7_2,negated_conjecture,
? [X,Y,T1,T2,I1,I2,P1,P2] :
( ~ greater(P2,P1)
& greater(I2,I1)
& survival_chance(Y,P2,T2)
& survival_chance(X,P1,T1)
& inertia(Y,I2,T2)
& inertia(X,I1,T1)
& reorganization_free(Y,T2,T2)
& reorganization_free(X,T1,T1)
& organization(Y,T2)
& organization(X,T1) ),
inference(fof_nnf,[status(thm)],[f_7_1]) ).
fof(f_7_3,negated_conjecture,
? [U_44,U_43,U_42,U_41,U_40,U_39,U_38,U_37] :
( ~ greater(U_37,U_38)
& greater(U_39,U_40)
& survival_chance(U_43,U_37,U_41)
& survival_chance(U_44,U_38,U_42)
& inertia(U_43,U_39,U_41)
& inertia(U_44,U_40,U_42)
& reorganization_free(U_43,U_41,U_41)
& reorganization_free(U_44,U_42,U_42)
& organization(U_43,U_41)
& organization(U_44,U_42) ),
inference(variable_rename,[status(thm)],[f_7_2]) ).
fof(f_7_4,negated_conjecture,
? [U_43,U_42,U_41,U_40,U_39,U_38,U_37] :
( ~ greater(U_37,U_38)
& greater(U_39,U_40)
& survival_chance(U_43,U_37,U_41)
& survival_chance(sK4,U_38,U_42)
& inertia(U_43,U_39,U_41)
& inertia(sK4,U_40,U_42)
& reorganization_free(U_43,U_41,U_41)
& reorganization_free(sK4,U_42,U_42)
& organization(U_43,U_41)
& organization(sK4,U_42) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_44,sK4)],[f_7_3]) ).
fof(f_7_5,negated_conjecture,
? [U_42,U_41,U_40,U_39,U_38,U_37] :
( ~ greater(U_37,U_38)
& greater(U_39,U_40)
& survival_chance(sK5,U_37,U_41)
& survival_chance(sK4,U_38,U_42)
& inertia(sK5,U_39,U_41)
& inertia(sK4,U_40,U_42)
& reorganization_free(sK5,U_41,U_41)
& reorganization_free(sK4,U_42,U_42)
& organization(sK5,U_41)
& organization(sK4,U_42) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_43,sK5)],[f_7_4]) ).
fof(f_7_6,negated_conjecture,
? [U_41,U_40,U_39,U_38,U_37] :
( ~ greater(U_37,U_38)
& greater(U_39,U_40)
& survival_chance(sK5,U_37,U_41)
& survival_chance(sK4,U_38,sK6)
& inertia(sK5,U_39,U_41)
& inertia(sK4,U_40,sK6)
& reorganization_free(sK5,U_41,U_41)
& reorganization_free(sK4,sK6,sK6)
& organization(sK5,U_41)
& organization(sK4,sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_42,sK6)],[f_7_5]) ).
fof(f_7_7,negated_conjecture,
? [U_40,U_39,U_38,U_37] :
( ~ greater(U_37,U_38)
& greater(U_39,U_40)
& survival_chance(sK5,U_37,sK7)
& survival_chance(sK4,U_38,sK6)
& inertia(sK5,U_39,sK7)
& inertia(sK4,U_40,sK6)
& reorganization_free(sK5,sK7,sK7)
& reorganization_free(sK4,sK6,sK6)
& organization(sK5,sK7)
& organization(sK4,sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_41,sK7)],[f_7_6]) ).
fof(f_7_8,negated_conjecture,
? [U_39,U_38,U_37] :
( ~ greater(U_37,U_38)
& greater(U_39,sK8)
& survival_chance(sK5,U_37,sK7)
& survival_chance(sK4,U_38,sK6)
& inertia(sK5,U_39,sK7)
& inertia(sK4,sK8,sK6)
& reorganization_free(sK5,sK7,sK7)
& reorganization_free(sK4,sK6,sK6)
& organization(sK5,sK7)
& organization(sK4,sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_40,sK8)],[f_7_7]) ).
fof(f_7_9,negated_conjecture,
? [U_38,U_37] :
( ~ greater(U_37,U_38)
& greater(sK9,sK8)
& survival_chance(sK5,U_37,sK7)
& survival_chance(sK4,U_38,sK6)
& inertia(sK5,sK9,sK7)
& inertia(sK4,sK8,sK6)
& reorganization_free(sK5,sK7,sK7)
& reorganization_free(sK4,sK6,sK6)
& organization(sK5,sK7)
& organization(sK4,sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_39,sK9)],[f_7_8]) ).
fof(f_7_10,negated_conjecture,
? [U_37] :
( ~ greater(U_37,sK10)
& greater(sK9,sK8)
& survival_chance(sK5,U_37,sK7)
& survival_chance(sK4,sK10,sK6)
& inertia(sK5,sK9,sK7)
& inertia(sK4,sK8,sK6)
& reorganization_free(sK5,sK7,sK7)
& reorganization_free(sK4,sK6,sK6)
& organization(sK5,sK7)
& organization(sK4,sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_38,sK10)],[f_7_9]) ).
fof(f_7_11,negated_conjecture,
( ~ greater(sK11,sK10)
& greater(sK9,sK8)
& survival_chance(sK5,sK11,sK7)
& survival_chance(sK4,sK10,sK6)
& inertia(sK5,sK9,sK7)
& inertia(sK4,sK8,sK6)
& reorganization_free(sK5,sK7,sK7)
& reorganization_free(sK4,sK6,sK6)
& organization(sK5,sK7)
& organization(sK4,sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_37,sK11)],[f_7_10]) ).
fof(f_7_12,negated_conjecture,
( ~ greater(sK11,sK10)
& greater(sK9,sK8)
& survival_chance(sK5,sK11,sK7)
& survival_chance(sK4,sK10,sK6)
& inertia(sK5,sK9,sK7)
& inertia(sK4,sK8,sK6)
& reorganization_free(sK5,sK7,sK7)
& reorganization_free(sK4,sK6,sK6)
& organization(sK5,sK7)
& organization(sK4,sK6) ),
inference(definitional_conversion,[status(esa)],[f_7_11]) ).
cnf(f_7_13,negated_conjecture,
organization(sK4,sK6),
inference(clausify,[status(thm)],[f_7_12]) ).
cnf(f_7_14,negated_conjecture,
organization(sK5,sK7),
inference(clausify,[status(thm)],[f_7_12]) ).
cnf(f_7_15,negated_conjecture,
reorganization_free(sK4,sK6,sK6),
inference(clausify,[status(thm)],[f_7_12]) ).
cnf(f_7_16,negated_conjecture,
reorganization_free(sK5,sK7,sK7),
inference(clausify,[status(thm)],[f_7_12]) ).
cnf(f_7_17,negated_conjecture,
inertia(sK4,sK8,sK6),
inference(clausify,[status(thm)],[f_7_12]) ).
cnf(f_7_18,negated_conjecture,
inertia(sK5,sK9,sK7),
inference(clausify,[status(thm)],[f_7_12]) ).
cnf(f_7_19,negated_conjecture,
survival_chance(sK4,sK10,sK6),
inference(clausify,[status(thm)],[f_7_12]) ).
cnf(f_7_20,negated_conjecture,
survival_chance(sK5,sK11,sK7),
inference(clausify,[status(thm)],[f_7_12]) ).
cnf(f_7_21,negated_conjecture,
greater(sK9,sK8),
inference(clausify,[status(thm)],[f_7_12]) ).
cnf(f_7_22,negated_conjecture,
~ greater(sK11,sK10),
inference(clausify,[status(thm)],[f_7_12]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT001+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.03 This is a FOF_THM_RFO_NEQ 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.10/0.39 % Computer : n002.cluster.edu
% 0.10/0.39 % Model : x86_64 x86_64
% 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.39 % Memory : 8046.5625MB
% 0.10/0.39 % OS : Linux 6.8.0-71-generic
% 0.10/0.39 % CPULimit : 300
% 0.10/0.39 % WCLimit : 300
% 0.10/0.39 % DateTime : Sat Sep 19 16:12:17 UTC 2026
% 0.10/0.39 % CPUTime :
% 31.04/31.30 % SZS status Theorem for theBenchmark
% 31.04/31.30 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------