%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : MGT005+2 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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:04 AM UTC 2026
% Result : Theorem 2.84s 0.83s
% Output : CNFRefutation 2.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 5
% Syntax : Number of formulae : 73 ( 27 unt; 0 def)
% Number of atoms : 462 ( 33 equ)
% Maximal formula atoms : 23 ( 6 avg)
% Number of connectives : 648 ( 259 ~; 271 |; 108 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 36 ( 8 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 13 con; 0-0 aty)
% Number of variables : 216 ( 10 sgn 54 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mp13,axiom,
! [X,T,T1,T2] :
( ( greater(T2,T)
& greater(T,T1)
& organization(X,T2)
& organization(X,T1) )
=> organization(X,T) ),
file('theBenchmark.p',mp13) ).
fof(mp7,axiom,
! [X,Ta,Tb] :
( reorganization(X,Ta,Tb)
=> greater(Tb,Ta) ),
file('theBenchmark.p',mp7) ).
fof(a10_FOL,axiom,
! [X,Y,Re,C,C1,C2,Ta,Tb,Tc] :
( ( greater(C2,C1)
& complexity(Y,C2,Ta)
& complexity(X,C1,Ta)
& reorganization_type(Y,Re,Ta)
& reorganization_type(X,Re,Ta)
& reorganization(Y,Ta,Tc)
& reorganization(X,Ta,Tb)
& class(Y,C,Ta)
& class(X,C,Ta)
& organization(Y,Tc)
& organization(Y,Ta)
& organization(X,Ta) )
=> greater(Tc,Tb) ),
file('theBenchmark.p',a10_FOL) ).
fof(a11_FOL,axiom,
! [X,Y,Re,C,P,P1,P2,C1,C2,Ta,Tb,Tc] :
( ( greater(C2,C1)
& complexity(Y,C2,Ta)
& complexity(X,C1,Ta)
& survival_chance(Y,P2,Tb)
& survival_chance(X,P1,Tb)
& reorganization_type(Y,Re,Ta)
& reorganization_type(X,Re,Ta)
& reorganization(Y,Ta,Tc)
& reorganization(X,Ta,Tb)
& survival_chance(Y,P,Ta)
& survival_chance(X,P,Ta)
& class(Y,C,Ta)
& class(X,C,Ta)
& organization(Y,Tb)
& organization(X,Tb)
& organization(Y,Ta)
& organization(X,Ta) )
=> ( P1 = P2
| greater(P1,P2) ) ),
file('theBenchmark.p',a11_FOL) ).
fof(t5_plus_FOL,conjecture,
! [X,Y,Re,C,P,P1,P2,C1,C2,T,Ta,Tb,Tc] :
( ( ( T = Tc
=> greater(P1,P2) )
& greater(C2,C1)
& complexity(Y,C2,Ta)
& complexity(X,C1,Ta)
& survival_chance(Y,P2,T)
& survival_chance(X,P1,T)
& reorganization_free(X,Tb,Tc)
& reorganization_type(Y,Re,Ta)
& reorganization_type(X,Re,Ta)
& reorganization(Y,Ta,Tc)
& reorganization(X,Ta,Tb)
& survival_chance(Y,P,Ta)
& survival_chance(X,P,Ta)
& class(Y,C,Ta)
& class(X,C,Ta)
& organization(Y,Tc)
& organization(X,Tc)
& organization(Y,Ta)
& organization(X,Ta) )
=> ( T = Tb
=> ( P1 = P2
| greater(P1,P2) ) ) ),
file('theBenchmark.p',t5_plus_FOL) ).
fof(t5_plus_FOL_neg,negated_conjecture,
~ ! [X,Y,Re,C,P,P1,P2,C1,C2,T,Ta,Tb,Tc] :
( ( ( T = Tc
=> greater(P1,P2) )
& greater(C2,C1)
& complexity(Y,C2,Ta)
& complexity(X,C1,Ta)
& survival_chance(Y,P2,T)
& survival_chance(X,P1,T)
& reorganization_free(X,Tb,Tc)
& reorganization_type(Y,Re,Ta)
& reorganization_type(X,Re,Ta)
& reorganization(Y,Ta,Tc)
& reorganization(X,Ta,Tb)
& survival_chance(Y,P,Ta)
& survival_chance(X,P,Ta)
& class(Y,C,Ta)
& class(X,C,Ta)
& organization(Y,Tc)
& organization(X,Tc)
& organization(Y,Ta)
& organization(X,Ta) )
=> ( T = Tb
=> ( P1 = P2
| greater(P1,P2) ) ) ),
inference(assume_negation,[status(cth)],[t5_plus_FOL]) ).
fof(nnf_13,plain,
? [X,Y,Re,C,P,P1,P2,C1,C2,T,Ta,Tb,Tc] :
( P2 != P1
& ~ greater(P1,P2)
& Tb = T
& ( greater(P1,P2)
| Tc != T )
& greater(C2,C1)
& complexity(Y,C2,Ta)
& complexity(X,C1,Ta)
& survival_chance(Y,P2,T)
& survival_chance(X,P1,T)
& reorganization_free(X,Tb,Tc)
& reorganization_type(Y,Re,Ta)
& reorganization_type(X,Re,Ta)
& reorganization(Y,Ta,Tc)
& reorganization(X,Ta,Tb)
& survival_chance(Y,P,Ta)
& survival_chance(X,P,Ta)
& class(Y,C,Ta)
& class(X,C,Ta)
& organization(Y,Tc)
& organization(X,Tc)
& organization(Y,Ta)
& organization(X,Ta) ),
inference(fof_nnf,[status(thm)],[t5_plus_FOL_neg]) ).
fof(sk_t5_plus_FOL_neg,plain,
( sK0 != sK1
& ~ greater(sK1,sK0)
& sK2 = sK3
& ( greater(sK1,sK0)
| sK10 != sK3 )
& greater(sK4,sK5)
& complexity(sK6,sK4,sK7)
& complexity(sK8,sK5,sK7)
& survival_chance(sK6,sK0,sK3)
& survival_chance(sK8,sK1,sK3)
& reorganization_free(sK8,sK2,sK10)
& reorganization_type(sK6,sK9,sK7)
& reorganization_type(sK8,sK9,sK7)
& reorganization(sK6,sK7,sK10)
& reorganization(sK8,sK7,sK2)
& survival_chance(sK6,sK11,sK7)
& survival_chance(sK8,sK11,sK7)
& class(sK6,sK12,sK7)
& class(sK8,sK12,sK7)
& organization(sK6,sK10)
& organization(sK8,sK10)
& organization(sK6,sK7)
& organization(sK8,sK7) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK7,sK6,sK10,sK12,sK11,sK2,sK9,sK1,sK3,sK0,sK5,sK4]),skolemize(X,sK8),skolemize(Y,sK6),skolemize(Re,sK9),skolemize(C,sK12),skolemize(P,sK11),skolemize(P1,sK1),skolemize(P2,sK0),skolemize(C1,sK5),skolemize(C2,sK4),skolemize(T,sK3),skolemize(Ta,sK7),skolemize(Tb,sK2),skolemize(Tc,sK10)],[nnf_13]) ).
cnf(c_17,negated_conjecture,
sK0 != sK1,
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_18,negated_conjecture,
~ greater(sK1,sK0),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_19,negated_conjecture,
sK2 = sK3,
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_22,negated_conjecture,
greater(sK4,sK5),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_23,negated_conjecture,
complexity(sK6,sK4,sK7),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_24,negated_conjecture,
complexity(sK8,sK5,sK7),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_25,negated_conjecture,
survival_chance(sK6,sK0,sK3),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_26,negated_conjecture,
survival_chance(sK8,sK1,sK3),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_27,negated_conjecture,
reorganization_type(sK6,sK9,sK7),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_28,negated_conjecture,
reorganization_type(sK8,sK9,sK7),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_29,negated_conjecture,
reorganization(sK6,sK7,sK10),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_30,negated_conjecture,
reorganization(sK8,sK7,sK2),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_31,negated_conjecture,
reorganization(sK8,sK7,sK3),
inference(paramod,[status(thm)],[c_19,c_30]) ).
cnf(c_32,negated_conjecture,
survival_chance(sK6,sK11,sK7),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_33,negated_conjecture,
survival_chance(sK8,sK11,sK7),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_34,negated_conjecture,
class(sK6,sK12,sK7),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_35,negated_conjecture,
class(sK8,sK12,sK7),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_36,negated_conjecture,
organization(sK6,sK10),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_37,negated_conjecture,
organization(sK8,sK10),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_38,negated_conjecture,
organization(sK6,sK7),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_39,negated_conjecture,
organization(sK8,sK7),
inference(split_conjunct,[status(thm)],[sk_t5_plus_FOL_neg]) ).
cnf(c_45,plain,
( V9 = V8
| greater(V8,V9)
| ~ greater(V11,V10)
| ~ complexity(C,V11,B)
| ~ complexity(A,V10,B)
| ~ survival_chance(C,V9,D)
| ~ survival_chance(A,V8,D)
| ~ reorganization_type(C,V7,B)
| ~ reorganization_type(A,V7,B)
| ~ reorganization(C,B,V6)
| ~ reorganization(A,B,D)
| ~ survival_chance(C,F,B)
| ~ survival_chance(A,F,B)
| ~ class(C,E,B)
| ~ class(A,E,B)
| ~ organization(C,D)
| ~ organization(A,D)
| ~ organization(C,B)
| ~ organization(A,B) ),
inference(clausify,[status(thm)],[a11_FOL]) ).
cnf(c_46,plain,
( greater(D,F)
| ~ greater(V8,V7)
| ~ complexity(C,V8,B)
| ~ complexity(A,V7,B)
| ~ reorganization_type(C,V6,B)
| ~ reorganization_type(A,V6,B)
| ~ reorganization(C,B,D)
| ~ reorganization(A,B,F)
| ~ class(C,E,B)
| ~ class(A,E,B)
| ~ organization(C,D)
| ~ organization(C,B)
| ~ organization(A,B) ),
inference(clausify,[status(thm)],[a10_FOL]) ).
cnf(c_48,plain,
( greater(C,B)
| ~ reorganization(A,B,C) ),
inference(clausify,[status(thm)],[mp7]) ).
cnf(c_49,plain,
( organization(A,D)
| ~ greater(C,D)
| ~ greater(D,B)
| ~ organization(A,C)
| ~ organization(A,B) ),
inference(clausify,[status(thm)],[mp13]) ).
cnf(c_556,negated_conjecture,
( greater(B,D)
| ~ greater(V6,F)
| ~ complexity(A,V6,sK7)
| ~ complexity(sK8,F,sK7)
| ~ reorganization_type(A,E,sK7)
| ~ reorganization_type(sK8,E,sK7)
| ~ reorganization(A,sK7,B)
| ~ reorganization(sK8,sK7,D)
| ~ class(A,C,sK7)
| ~ class(sK8,C,sK7)
| ~ organization(A,B)
| ~ organization(A,sK7) ),
inference(resolve,[status(thm)],[c_46,c_39]) ).
cnf(c_557,negated_conjecture,
( greater(A,C)
| ~ greater(F,E)
| ~ complexity(sK6,F,sK7)
| ~ complexity(sK8,E,sK7)
| ~ reorganization_type(sK6,D,sK7)
| ~ reorganization_type(sK8,D,sK7)
| ~ reorganization(sK6,sK7,A)
| ~ reorganization(sK8,sK7,C)
| ~ class(sK6,B,sK7)
| ~ class(sK8,B,sK7)
| ~ organization(sK6,A) ),
inference(resolve,[status(thm)],[c_556,c_38]) ).
cnf(c_558,negated_conjecture,
( greater(sK10,B)
| ~ greater(E,D)
| ~ complexity(sK6,E,sK7)
| ~ complexity(sK8,D,sK7)
| ~ reorganization_type(sK6,C,sK7)
| ~ reorganization_type(sK8,C,sK7)
| ~ reorganization(sK6,sK7,sK10)
| ~ reorganization(sK8,sK7,B)
| ~ class(sK6,A,sK7)
| ~ class(sK8,A,sK7) ),
inference(resolve,[status(thm)],[c_557,c_36]) ).
cnf(c_559,negated_conjecture,
( greater(sK10,A)
| ~ greater(D,C)
| ~ complexity(sK6,D,sK7)
| ~ complexity(sK8,C,sK7)
| ~ reorganization_type(sK6,B,sK7)
| ~ reorganization_type(sK8,B,sK7)
| ~ reorganization(sK6,sK7,sK10)
| ~ reorganization(sK8,sK7,A)
| ~ class(sK6,sK12,sK7) ),
inference(resolve,[status(thm)],[c_558,c_35]) ).
cnf(c_560,negated_conjecture,
( greater(sK10,A)
| ~ greater(D,C)
| ~ complexity(sK6,D,sK7)
| ~ complexity(sK8,C,sK7)
| ~ reorganization_type(sK6,B,sK7)
| ~ reorganization_type(sK8,B,sK7)
| ~ reorganization(sK6,sK7,sK10)
| ~ reorganization(sK8,sK7,A) ),
inference(resolve,[status(thm)],[c_559,c_34]) ).
cnf(c_561,negated_conjecture,
( greater(sK10,sK3)
| ~ greater(C,B)
| ~ complexity(sK6,C,sK7)
| ~ complexity(sK8,B,sK7)
| ~ reorganization_type(sK6,A,sK7)
| ~ reorganization_type(sK8,A,sK7)
| ~ reorganization(sK6,sK7,sK10) ),
inference(resolve,[status(thm)],[c_560,c_31]) ).
cnf(c_562,negated_conjecture,
( greater(sK10,sK3)
| ~ greater(C,B)
| ~ complexity(sK6,C,sK7)
| ~ complexity(sK8,B,sK7)
| ~ reorganization_type(sK6,A,sK7)
| ~ reorganization_type(sK8,A,sK7) ),
inference(resolve,[status(thm)],[c_561,c_29]) ).
cnf(c_563,negated_conjecture,
( greater(sK10,sK3)
| ~ greater(B,A)
| ~ complexity(sK6,B,sK7)
| ~ complexity(sK8,A,sK7)
| ~ reorganization_type(sK6,sK9,sK7) ),
inference(resolve,[status(thm)],[c_562,c_28]) ).
cnf(c_564,negated_conjecture,
( greater(sK10,sK3)
| ~ greater(B,A)
| ~ complexity(sK6,B,sK7)
| ~ complexity(sK8,A,sK7) ),
inference(resolve,[status(thm)],[c_563,c_27]) ).
cnf(c_565,negated_conjecture,
( greater(sK10,sK3)
| ~ greater(A,sK5)
| ~ complexity(sK6,A,sK7) ),
inference(resolve,[status(thm)],[c_564,c_24]) ).
cnf(c_566,negated_conjecture,
( greater(sK10,sK3)
| ~ greater(sK4,sK5) ),
inference(resolve,[status(thm)],[c_565,c_23]) ).
cnf(c_435,negated_conjecture,
greater(sK10,sK3),
inference(resolve,[status(thm)],[c_566,c_22]) ).
cnf(c_453,plain,
greater(sK3,sK7),
inference(resolve,[status(thm)],[c_48,c_31]) ).
cnf(c_567,negated_conjecture,
( organization(sK8,B)
| ~ greater(A,B)
| ~ greater(B,sK7)
| ~ organization(sK8,A) ),
inference(resolve,[status(thm)],[c_49,c_39]) ).
cnf(c_568,negated_conjecture,
( organization(sK8,A)
| ~ greater(sK10,A)
| ~ greater(A,sK7) ),
inference(resolve,[status(thm)],[c_567,c_37]) ).
cnf(c_569,negated_conjecture,
( organization(sK8,sK3)
| ~ greater(sK10,sK3) ),
inference(resolve,[status(thm)],[c_568,c_453]) ).
cnf(c_532,negated_conjecture,
organization(sK8,sK3),
inference(resolve,[status(thm)],[c_569,c_435]) ).
cnf(c_570,negated_conjecture,
( organization(sK6,B)
| ~ greater(A,B)
| ~ greater(B,sK7)
| ~ organization(sK6,A) ),
inference(resolve,[status(thm)],[c_49,c_38]) ).
cnf(c_571,negated_conjecture,
( organization(sK6,A)
| ~ greater(sK10,A)
| ~ greater(A,sK7) ),
inference(resolve,[status(thm)],[c_570,c_36]) ).
cnf(c_572,negated_conjecture,
( organization(sK6,sK3)
| ~ greater(sK10,sK3) ),
inference(resolve,[status(thm)],[c_571,c_453]) ).
cnf(c_533,negated_conjecture,
organization(sK6,sK3),
inference(resolve,[status(thm)],[c_572,c_435]) ).
cnf(c_573,negated_conjecture,
( V7 = V6
| greater(V6,V7)
| ~ greater(V9,V8)
| ~ complexity(A,V9,sK7)
| ~ complexity(sK8,V8,sK7)
| ~ survival_chance(A,V7,B)
| ~ survival_chance(sK8,V6,B)
| ~ reorganization_type(A,F,sK7)
| ~ reorganization_type(sK8,F,sK7)
| ~ reorganization(A,sK7,E)
| ~ reorganization(sK8,sK7,B)
| ~ survival_chance(A,D,sK7)
| ~ survival_chance(sK8,D,sK7)
| ~ class(A,C,sK7)
| ~ class(sK8,C,sK7)
| ~ organization(A,B)
| ~ organization(sK8,B)
| ~ organization(A,sK7) ),
inference(resolve,[status(thm)],[c_45,c_39]) ).
cnf(c_574,negated_conjecture,
( V6 = F
| greater(F,V6)
| ~ greater(V8,V7)
| ~ complexity(sK6,V8,sK7)
| ~ complexity(sK8,V7,sK7)
| ~ survival_chance(sK6,V6,A)
| ~ survival_chance(sK8,F,A)
| ~ reorganization_type(sK6,E,sK7)
| ~ reorganization_type(sK8,E,sK7)
| ~ reorganization(sK6,sK7,D)
| ~ reorganization(sK8,sK7,A)
| ~ survival_chance(sK6,C,sK7)
| ~ survival_chance(sK8,C,sK7)
| ~ class(sK6,B,sK7)
| ~ class(sK8,B,sK7)
| ~ organization(sK6,A)
| ~ organization(sK8,A) ),
inference(resolve,[status(thm)],[c_573,c_38]) ).
cnf(c_575,negated_conjecture,
( F = E
| greater(E,F)
| ~ greater(V7,V6)
| ~ complexity(sK6,V7,sK7)
| ~ complexity(sK8,V6,sK7)
| ~ survival_chance(sK6,F,sK3)
| ~ survival_chance(sK8,E,sK3)
| ~ reorganization_type(sK6,D,sK7)
| ~ reorganization_type(sK8,D,sK7)
| ~ reorganization(sK6,sK7,C)
| ~ reorganization(sK8,sK7,sK3)
| ~ survival_chance(sK6,B,sK7)
| ~ survival_chance(sK8,B,sK7)
| ~ class(sK6,A,sK7)
| ~ class(sK8,A,sK7)
| ~ organization(sK6,sK3) ),
inference(resolve,[status(thm)],[c_574,c_532]) ).
cnf(c_576,negated_conjecture,
( E = D
| greater(D,E)
| ~ greater(V6,F)
| ~ complexity(sK6,V6,sK7)
| ~ complexity(sK8,F,sK7)
| ~ survival_chance(sK6,E,sK3)
| ~ survival_chance(sK8,D,sK3)
| ~ reorganization_type(sK6,C,sK7)
| ~ reorganization_type(sK8,C,sK7)
| ~ reorganization(sK6,sK7,B)
| ~ reorganization(sK8,sK7,sK3)
| ~ survival_chance(sK6,A,sK7)
| ~ survival_chance(sK8,A,sK7)
| ~ class(sK6,sK12,sK7)
| ~ organization(sK6,sK3) ),
inference(resolve,[status(thm)],[c_575,c_35]) ).
cnf(c_577,negated_conjecture,
( E = D
| greater(D,E)
| ~ greater(V6,F)
| ~ complexity(sK6,V6,sK7)
| ~ complexity(sK8,F,sK7)
| ~ survival_chance(sK6,E,sK3)
| ~ survival_chance(sK8,D,sK3)
| ~ reorganization_type(sK6,C,sK7)
| ~ reorganization_type(sK8,C,sK7)
| ~ reorganization(sK6,sK7,B)
| ~ reorganization(sK8,sK7,sK3)
| ~ survival_chance(sK6,A,sK7)
| ~ survival_chance(sK8,A,sK7)
| ~ organization(sK6,sK3) ),
inference(resolve,[status(thm)],[c_576,c_34]) ).
cnf(c_578,negated_conjecture,
( D = C
| greater(C,D)
| ~ greater(F,E)
| ~ complexity(sK6,F,sK7)
| ~ complexity(sK8,E,sK7)
| ~ survival_chance(sK6,D,sK3)
| ~ survival_chance(sK8,C,sK3)
| ~ reorganization_type(sK6,B,sK7)
| ~ reorganization_type(sK8,B,sK7)
| ~ reorganization(sK6,sK7,A)
| ~ reorganization(sK8,sK7,sK3)
| ~ survival_chance(sK6,sK11,sK7)
| ~ organization(sK6,sK3) ),
inference(resolve,[status(thm)],[c_577,c_33]) ).
cnf(c_579,negated_conjecture,
( D = C
| greater(C,D)
| ~ greater(F,E)
| ~ complexity(sK6,F,sK7)
| ~ complexity(sK8,E,sK7)
| ~ survival_chance(sK6,D,sK3)
| ~ survival_chance(sK8,C,sK3)
| ~ reorganization_type(sK6,B,sK7)
| ~ reorganization_type(sK8,B,sK7)
| ~ reorganization(sK6,sK7,A)
| ~ reorganization(sK8,sK7,sK3)
| ~ organization(sK6,sK3) ),
inference(resolve,[status(thm)],[c_578,c_32]) ).
cnf(c_580,negated_conjecture,
( D = C
| greater(C,D)
| ~ greater(F,E)
| ~ complexity(sK6,F,sK7)
| ~ complexity(sK8,E,sK7)
| ~ survival_chance(sK6,D,sK3)
| ~ survival_chance(sK8,C,sK3)
| ~ reorganization_type(sK6,B,sK7)
| ~ reorganization_type(sK8,B,sK7)
| ~ reorganization(sK6,sK7,A)
| ~ organization(sK6,sK3) ),
inference(resolve,[status(thm)],[c_579,c_31]) ).
cnf(c_581,negated_conjecture,
( C = B
| greater(B,C)
| ~ greater(E,D)
| ~ complexity(sK6,E,sK7)
| ~ complexity(sK8,D,sK7)
| ~ survival_chance(sK6,C,sK3)
| ~ survival_chance(sK8,B,sK3)
| ~ reorganization_type(sK6,A,sK7)
| ~ reorganization_type(sK8,A,sK7)
| ~ organization(sK6,sK3) ),
inference(resolve,[status(thm)],[c_580,c_29]) ).
cnf(c_582,negated_conjecture,
( B = A
| greater(A,B)
| ~ greater(D,C)
| ~ complexity(sK6,D,sK7)
| ~ complexity(sK8,C,sK7)
| ~ survival_chance(sK6,B,sK3)
| ~ survival_chance(sK8,A,sK3)
| ~ reorganization_type(sK6,sK9,sK7)
| ~ organization(sK6,sK3) ),
inference(resolve,[status(thm)],[c_581,c_28]) ).
cnf(c_583,negated_conjecture,
( B = A
| greater(A,B)
| ~ greater(D,C)
| ~ complexity(sK6,D,sK7)
| ~ complexity(sK8,C,sK7)
| ~ survival_chance(sK6,B,sK3)
| ~ survival_chance(sK8,A,sK3)
| ~ organization(sK6,sK3) ),
inference(resolve,[status(thm)],[c_582,c_27]) ).
cnf(c_584,negated_conjecture,
( A = sK1
| greater(sK1,A)
| ~ greater(C,B)
| ~ complexity(sK6,C,sK7)
| ~ complexity(sK8,B,sK7)
| ~ survival_chance(sK6,A,sK3)
| ~ organization(sK6,sK3) ),
inference(resolve,[status(thm)],[c_583,c_26]) ).
cnf(c_585,negated_conjecture,
( sK0 = sK1
| greater(sK1,sK0)
| ~ greater(B,A)
| ~ complexity(sK6,B,sK7)
| ~ complexity(sK8,A,sK7)
| ~ organization(sK6,sK3) ),
inference(resolve,[status(thm)],[c_584,c_25]) ).
cnf(c_586,negated_conjecture,
( sK0 = sK1
| greater(sK1,sK0)
| ~ greater(A,sK5)
| ~ complexity(sK6,A,sK7)
| ~ organization(sK6,sK3) ),
inference(resolve,[status(thm)],[c_585,c_24]) ).
cnf(c_587,negated_conjecture,
( sK0 = sK1
| greater(sK1,sK0)
| ~ greater(sK4,sK5)
| ~ organization(sK6,sK3) ),
inference(resolve,[status(thm)],[c_586,c_23]) ).
cnf(c_588,negated_conjecture,
( sK0 = sK1
| greater(sK1,sK0)
| ~ organization(sK6,sK3) ),
inference(resolve,[status(thm)],[c_587,c_22]) ).
cnf(c_589,negated_conjecture,
( sK0 = sK1
| ~ organization(sK6,sK3) ),
inference(resolve,[status(thm)],[c_588,c_18]) ).
cnf(c_590,negated_conjecture,
~ organization(sK6,sK3),
inference(resolve,[status(thm)],[c_589,c_17]) ).
cnf(c_555,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_533,c_590]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT005+2 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n005.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sat Sep 26 00:02:31 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.45 % Process 603294 was started by sandbox2 on n005,
% 0.17/0.45 % Sat Sep 26 00:02:31 2026
% 0.17/0.45 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.45
% 0.17/0.45 % From the command line: assign(max_seconds, 300).
% 2.84/0.83
% 2.84/0.83 % SZS status Theorem for theBenchmark
% 2.84/0.83
% 2.84/0.83 % Proof 1 at 0.30 (+ 0.05) seconds.
% 2.84/0.83 % Length of proof is 35.
% 2.84/0.83 % Level of proof is 5.
% 2.84/0.83 % Maximum clause weight is 74.000.
% 2.84/0.83 % Given clauses 86.
% 2.84/0.83
% 2.84/0.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------