%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : MGT005-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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:03 AM UTC 2026
% Result : Unsatisfiable 3.64s 1.58s
% Output : CNFRefutation 3.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 28
% Syntax : Number of formulae : 122 ( 54 unt; 0 def)
% Number of atoms : 506 ( 21 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 741 ( 357 ~; 384 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 12 con; 0-2 aty)
% Number of variables : 243 ( 12 sgn 47 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t5_FOL_48,axiom,
reorganization_free(sk2,sk12,sk13),
file('theBenchmark.p',t5_FOL_48) ).
cnf(c_1,plain,
reorganization_free(sk2,sk12,sk13),
inference(clausify,[status(thm)],[t5_FOL_48]) ).
fof(t3_FOL_32,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( greater(VAR_4,VAR_3)
| ~ greater(VAR_2,VAR_1)
| ~ survival_chance(VAR_0,VAR_4,VAR_2)
| ~ survival_chance(VAR_0,VAR_3,VAR_1)
| ~ reorganization_free(VAR_0,VAR_1,VAR_2)
| ~ organization(VAR_0,VAR_2)
| ~ organization(VAR_0,VAR_1) ),
file('theBenchmark.p',t3_FOL_32) ).
cnf(c_2,plain,
( greater(E,D)
| ~ greater(C,B)
| ~ survival_chance(A,E,C)
| ~ survival_chance(A,D,B)
| ~ reorganization_free(A,B,C)
| ~ organization(A,C)
| ~ organization(A,B) ),
inference(clausify,[status(thm)],[t3_FOL_32]) ).
cnf(c_3,plain,
( greater(B,A)
| ~ greater(sk13,sk12)
| ~ survival_chance(sk2,B,sk13)
| ~ survival_chance(sk2,A,sk12)
| ~ organization(sk2,sk13)
| ~ organization(sk2,sk12) ),
inference(resolve,[status(thm)],[c_1,c_2]) ).
fof(t5_FOL_54,axiom,
~ greater(sk7,sk8),
file('theBenchmark.p',t5_FOL_54) ).
cnf(c_4,plain,
~ greater(sk7,sk8),
inference(clausify,[status(thm)],[t5_FOL_54]) ).
fof(t5_FOL_53,axiom,
greater(sk10,sk9),
file('theBenchmark.p',t5_FOL_53) ).
cnf(c_5,plain,
greater(sk10,sk9),
inference(clausify,[status(thm)],[t5_FOL_53]) ).
fof(t5_FOL_52,axiom,
complexity(sk3,sk10,sk11),
file('theBenchmark.p',t5_FOL_52) ).
cnf(c_6,plain,
complexity(sk3,sk10,sk11),
inference(clausify,[status(thm)],[t5_FOL_52]) ).
fof(t5_FOL_51,axiom,
complexity(sk2,sk9,sk11),
file('theBenchmark.p',t5_FOL_51) ).
cnf(c_7,plain,
complexity(sk2,sk9,sk11),
inference(clausify,[status(thm)],[t5_FOL_51]) ).
fof(t5_FOL_50,axiom,
survival_chance(sk3,sk8,sk13),
file('theBenchmark.p',t5_FOL_50) ).
cnf(c_8,plain,
survival_chance(sk3,sk8,sk13),
inference(clausify,[status(thm)],[t5_FOL_50]) ).
fof(t5_FOL_49,axiom,
survival_chance(sk2,sk7,sk13),
file('theBenchmark.p',t5_FOL_49) ).
cnf(c_9,plain,
survival_chance(sk2,sk7,sk13),
inference(clausify,[status(thm)],[t5_FOL_49]) ).
fof(t5_FOL_47,axiom,
reorganization_type(sk3,sk4,sk11),
file('theBenchmark.p',t5_FOL_47) ).
cnf(c_10,plain,
reorganization_type(sk3,sk4,sk11),
inference(clausify,[status(thm)],[t5_FOL_47]) ).
fof(t5_FOL_46,axiom,
reorganization_type(sk2,sk4,sk11),
file('theBenchmark.p',t5_FOL_46) ).
cnf(c_11,plain,
reorganization_type(sk2,sk4,sk11),
inference(clausify,[status(thm)],[t5_FOL_46]) ).
fof(t5_FOL_45,axiom,
reorganization(sk3,sk11,sk13),
file('theBenchmark.p',t5_FOL_45) ).
cnf(c_12,plain,
reorganization(sk3,sk11,sk13),
inference(clausify,[status(thm)],[t5_FOL_45]) ).
fof(t5_FOL_44,axiom,
reorganization(sk2,sk11,sk12),
file('theBenchmark.p',t5_FOL_44) ).
cnf(c_13,plain,
reorganization(sk2,sk11,sk12),
inference(clausify,[status(thm)],[t5_FOL_44]) ).
fof(t5_FOL_43,axiom,
survival_chance(sk3,sk6,sk11),
file('theBenchmark.p',t5_FOL_43) ).
cnf(c_14,plain,
survival_chance(sk3,sk6,sk11),
inference(clausify,[status(thm)],[t5_FOL_43]) ).
fof(t5_FOL_42,axiom,
survival_chance(sk2,sk6,sk11),
file('theBenchmark.p',t5_FOL_42) ).
cnf(c_15,plain,
survival_chance(sk2,sk6,sk11),
inference(clausify,[status(thm)],[t5_FOL_42]) ).
fof(t5_FOL_41,axiom,
class(sk3,sk5,sk11),
file('theBenchmark.p',t5_FOL_41) ).
cnf(c_16,plain,
class(sk3,sk5,sk11),
inference(clausify,[status(thm)],[t5_FOL_41]) ).
fof(t5_FOL_40,axiom,
class(sk2,sk5,sk11),
file('theBenchmark.p',t5_FOL_40) ).
cnf(c_17,plain,
class(sk2,sk5,sk11),
inference(clausify,[status(thm)],[t5_FOL_40]) ).
fof(t5_FOL_39,axiom,
organization(sk3,sk13),
file('theBenchmark.p',t5_FOL_39) ).
cnf(c_18,plain,
organization(sk3,sk13),
inference(clausify,[status(thm)],[t5_FOL_39]) ).
fof(t5_FOL_38,axiom,
organization(sk2,sk13),
file('theBenchmark.p',t5_FOL_38) ).
cnf(c_19,plain,
organization(sk2,sk13),
inference(clausify,[status(thm)],[t5_FOL_38]) ).
fof(t5_FOL_37,axiom,
organization(sk3,sk11),
file('theBenchmark.p',t5_FOL_37) ).
cnf(c_20,plain,
organization(sk3,sk11),
inference(clausify,[status(thm)],[t5_FOL_37]) ).
fof(t5_FOL_36,axiom,
organization(sk2,sk11),
file('theBenchmark.p',t5_FOL_36) ).
cnf(c_21,plain,
organization(sk2,sk11),
inference(clausify,[status(thm)],[t5_FOL_36]) ).
fof(a11_FOL_35,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_8,VAR_9,VAR_10,VAR_11] :
( VAR_8 = VAR_9
| greater(VAR_8,VAR_9)
| ~ greater(VAR_11,VAR_10)
| ~ complexity(VAR_2,VAR_11,VAR_1)
| ~ complexity(VAR_0,VAR_10,VAR_1)
| ~ survival_chance(VAR_2,VAR_9,VAR_3)
| ~ survival_chance(VAR_0,VAR_8,VAR_3)
| ~ reorganization_type(VAR_2,VAR_7,VAR_1)
| ~ reorganization_type(VAR_0,VAR_7,VAR_1)
| ~ reorganization(VAR_2,VAR_1,VAR_6)
| ~ reorganization(VAR_0,VAR_1,VAR_3)
| ~ survival_chance(VAR_2,VAR_5,VAR_1)
| ~ survival_chance(VAR_0,VAR_5,VAR_1)
| ~ class(VAR_2,VAR_4,VAR_1)
| ~ class(VAR_0,VAR_4,VAR_1)
| ~ organization(VAR_2,VAR_3)
| ~ organization(VAR_0,VAR_3)
| ~ organization(VAR_2,VAR_1)
| ~ organization(VAR_0,VAR_1) ),
file('theBenchmark.p',a11_FOL_35) ).
cnf(c_22,plain,
( V8 = V9
| 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_35]) ).
fof(a10_FOL_34,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_8] :
( greater(VAR_3,VAR_5)
| ~ greater(VAR_8,VAR_7)
| ~ complexity(VAR_2,VAR_8,VAR_1)
| ~ complexity(VAR_0,VAR_7,VAR_1)
| ~ reorganization_type(VAR_2,VAR_6,VAR_1)
| ~ reorganization_type(VAR_0,VAR_6,VAR_1)
| ~ reorganization(VAR_2,VAR_1,VAR_3)
| ~ reorganization(VAR_0,VAR_1,VAR_5)
| ~ class(VAR_2,VAR_4,VAR_1)
| ~ class(VAR_0,VAR_4,VAR_1)
| ~ organization(VAR_2,VAR_3)
| ~ organization(VAR_2,VAR_1)
| ~ organization(VAR_0,VAR_1) ),
file('theBenchmark.p',a10_FOL_34) ).
cnf(c_23,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_34]) ).
fof(t4_FOL_33,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( greater(VAR_5,VAR_6)
| greater(VAR_2,VAR_4)
| ~ greater(VAR_2,VAR_1)
| greater(VAR_3,VAR_1)
| ~ survival_chance(VAR_0,VAR_6,VAR_2)
| ~ survival_chance(VAR_0,VAR_5,VAR_1)
| ~ reorganization(VAR_0,VAR_3,VAR_4)
| ~ organization(VAR_0,VAR_2)
| ~ organization(VAR_0,VAR_1) ),
file('theBenchmark.p',t4_FOL_33) ).
cnf(c_24,plain,
( greater(F,V6)
| greater(C,E)
| ~ greater(C,B)
| greater(D,B)
| ~ survival_chance(A,V6,C)
| ~ survival_chance(A,F,B)
| ~ reorganization(A,D,E)
| ~ organization(A,C)
| ~ organization(A,B) ),
inference(clausify,[status(thm)],[t4_FOL_33]) ).
fof(mp7_31,axiom,
! [VAR_0,VAR_1,VAR_2] :
( greater(VAR_2,VAR_1)
| ~ reorganization(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',mp7_31) ).
cnf(c_25,plain,
( greater(C,B)
| ~ reorganization(A,B,C) ),
inference(clausify,[status(thm)],[mp7_31]) ).
fof(mp13_30,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( organization(VAR_0,VAR_3)
| ~ greater(VAR_2,VAR_3)
| ~ greater(VAR_3,VAR_1)
| ~ organization(VAR_0,VAR_2)
| ~ organization(VAR_0,VAR_1) ),
file('theBenchmark.p',mp13_30) ).
cnf(c_26,plain,
( organization(A,D)
| ~ greater(C,D)
| ~ greater(D,B)
| ~ organization(A,C)
| ~ organization(A,B) ),
inference(clausify,[status(thm)],[mp13_30]) ).
fof(mp12_29,axiom,
! [VAR_0,VAR_1] :
( survival_chance(VAR_0,sk1(VAR_1,VAR_0),VAR_1)
| ~ organization(VAR_0,VAR_1) ),
file('theBenchmark.p',mp12_29) ).
cnf(c_27,plain,
( survival_chance(A,sk1(B,A),B)
| ~ organization(A,B) ),
inference(clausify,[status(thm)],[mp12_29]) ).
fof(mp11_28,axiom,
! [VAR_0,VAR_1,VAR_2] :
( greater(VAR_0,VAR_2)
| ~ greater(VAR_1,VAR_2)
| ~ greater(VAR_0,VAR_1) ),
file('theBenchmark.p',mp11_28) ).
cnf(c_28,plain,
( greater(A,C)
| ~ greater(B,C)
| ~ greater(A,B) ),
inference(clausify,[status(thm)],[mp11_28]) ).
fof(mp6_2_27,axiom,
! [VAR_0,VAR_1] :
( ~ greater(VAR_1,VAR_0)
| ~ greater(VAR_0,VAR_1) ),
file('theBenchmark.p',mp6_2_27) ).
cnf(c_29,plain,
( ~ greater(B,A)
| ~ greater(A,B) ),
inference(clausify,[status(thm)],[mp6_2_27]) ).
cnf(c_31,plain,
( greater(B,A)
| ~ greater(sk13,sk12)
| ~ survival_chance(sk2,B,sk13)
| ~ survival_chance(sk2,A,sk12)
| ~ organization(sk2,sk12) ),
inference(resolve,[status(thm)],[c_19,c_3]) ).
cnf(c_49,plain,
~ greater(A,A),
inference(factor,[status(thm)],[c_29]) ).
cnf(c_254,plain,
( F = V6
| greater(F,V6)
| ~ greater(V8,V7)
| ~ complexity(sk3,V8,sk11)
| ~ complexity(A,V7,sk11)
| ~ survival_chance(sk3,V6,B)
| ~ survival_chance(A,F,B)
| ~ reorganization_type(A,sk4,sk11)
| ~ reorganization(sk3,sk11,E)
| ~ reorganization(A,sk11,B)
| ~ survival_chance(sk3,D,sk11)
| ~ survival_chance(A,D,sk11)
| ~ class(sk3,C,sk11)
| ~ class(A,C,sk11)
| ~ organization(sk3,B)
| ~ organization(A,B)
| ~ organization(sk3,sk11)
| ~ organization(A,sk11) ),
inference(resolve,[status(thm)],[c_22,c_10]) ).
cnf(c_57,plain,
( F = V6
| greater(F,V6)
| ~ greater(V8,V7)
| ~ complexity(sk3,V8,sk11)
| ~ complexity(A,V7,sk11)
| ~ survival_chance(sk3,V6,B)
| ~ survival_chance(A,F,B)
| ~ reorganization_type(A,sk4,sk11)
| ~ reorganization(sk3,sk11,E)
| ~ reorganization(A,sk11,B)
| ~ survival_chance(sk3,D,sk11)
| ~ survival_chance(A,D,sk11)
| ~ class(sk3,C,sk11)
| ~ class(A,C,sk11)
| ~ organization(sk3,B)
| ~ organization(A,B)
| ~ organization(A,sk11) ),
inference(resolve,[status(thm)],[c_20,c_254]) ).
cnf(c_255,plain,
( greater(B,D)
| ~ greater(V6,F)
| ~ complexity(A,V6,sk11)
| ~ complexity(sk2,F,sk11)
| ~ reorganization_type(A,E,sk11)
| ~ reorganization_type(sk2,E,sk11)
| ~ reorganization(A,sk11,B)
| ~ reorganization(sk2,sk11,D)
| ~ class(A,C,sk11)
| ~ class(sk2,C,sk11)
| ~ organization(A,B)
| ~ organization(A,sk11) ),
inference(resolve,[status(thm)],[c_23,c_21]) ).
cnf(c_256,plain,
( greater(A,C)
| ~ greater(F,E)
| ~ complexity(sk3,F,sk11)
| ~ complexity(sk2,E,sk11)
| ~ reorganization_type(sk3,D,sk11)
| ~ reorganization_type(sk2,D,sk11)
| ~ reorganization(sk3,sk11,A)
| ~ reorganization(sk2,sk11,C)
| ~ class(sk3,B,sk11)
| ~ class(sk2,B,sk11)
| ~ organization(sk3,A) ),
inference(resolve,[status(thm)],[c_255,c_20]) ).
cnf(c_257,plain,
( greater(sk13,B)
| ~ greater(E,D)
| ~ complexity(sk3,E,sk11)
| ~ complexity(sk2,D,sk11)
| ~ reorganization_type(sk3,C,sk11)
| ~ reorganization_type(sk2,C,sk11)
| ~ reorganization(sk3,sk11,sk13)
| ~ reorganization(sk2,sk11,B)
| ~ class(sk3,A,sk11)
| ~ class(sk2,A,sk11) ),
inference(resolve,[status(thm)],[c_256,c_18]) ).
cnf(c_258,plain,
( greater(sk13,A)
| ~ greater(D,C)
| ~ complexity(sk3,D,sk11)
| ~ complexity(sk2,C,sk11)
| ~ reorganization_type(sk3,B,sk11)
| ~ reorganization_type(sk2,B,sk11)
| ~ reorganization(sk3,sk11,sk13)
| ~ reorganization(sk2,sk11,A)
| ~ class(sk3,sk5,sk11) ),
inference(resolve,[status(thm)],[c_257,c_17]) ).
cnf(c_259,plain,
( greater(sk13,A)
| ~ greater(D,C)
| ~ complexity(sk3,D,sk11)
| ~ complexity(sk2,C,sk11)
| ~ reorganization_type(sk3,B,sk11)
| ~ reorganization_type(sk2,B,sk11)
| ~ reorganization(sk3,sk11,sk13)
| ~ reorganization(sk2,sk11,A) ),
inference(resolve,[status(thm)],[c_258,c_16]) ).
cnf(c_260,plain,
( greater(sk13,sk12)
| ~ greater(C,B)
| ~ complexity(sk3,C,sk11)
| ~ complexity(sk2,B,sk11)
| ~ reorganization_type(sk3,A,sk11)
| ~ reorganization_type(sk2,A,sk11)
| ~ reorganization(sk3,sk11,sk13) ),
inference(resolve,[status(thm)],[c_259,c_13]) ).
cnf(c_261,plain,
( greater(sk13,sk12)
| ~ greater(C,B)
| ~ complexity(sk3,C,sk11)
| ~ complexity(sk2,B,sk11)
| ~ reorganization_type(sk3,A,sk11)
| ~ reorganization_type(sk2,A,sk11) ),
inference(resolve,[status(thm)],[c_260,c_12]) ).
cnf(c_262,plain,
( greater(sk13,sk12)
| ~ greater(B,A)
| ~ complexity(sk3,B,sk11)
| ~ complexity(sk2,A,sk11)
| ~ reorganization_type(sk3,sk4,sk11) ),
inference(resolve,[status(thm)],[c_261,c_11]) ).
cnf(c_263,plain,
( greater(sk13,sk12)
| ~ greater(B,A)
| ~ complexity(sk3,B,sk11)
| ~ complexity(sk2,A,sk11) ),
inference(resolve,[status(thm)],[c_262,c_10]) ).
cnf(c_264,plain,
( greater(sk13,sk12)
| ~ greater(A,sk9)
| ~ complexity(sk3,A,sk11) ),
inference(resolve,[status(thm)],[c_263,c_7]) ).
cnf(c_265,plain,
( greater(sk13,sk12)
| ~ greater(sk10,sk9) ),
inference(resolve,[status(thm)],[c_264,c_6]) ).
cnf(c_86,plain,
greater(sk13,sk12),
inference(resolve,[status(thm)],[c_265,c_5]) ).
cnf(c_95,plain,
( greater(B,A)
| ~ survival_chance(sk2,B,sk13)
| ~ survival_chance(sk2,A,sk12)
| ~ organization(sk2,sk12) ),
inference(resolve,[status(thm)],[c_86,c_31]) ).
cnf(c_104,plain,
greater(sk12,sk11),
inference(resolve,[status(thm)],[c_25,c_13]) ).
cnf(c_133,plain,
~ greater(sk11,sk12),
inference(resolve,[status(thm)],[c_104,c_29]) ).
cnf(c_266,plain,
( organization(sk2,B)
| ~ greater(A,B)
| ~ greater(B,sk11)
| ~ organization(sk2,A) ),
inference(resolve,[status(thm)],[c_26,c_21]) ).
cnf(c_267,plain,
( organization(sk2,A)
| ~ greater(sk13,A)
| ~ greater(A,sk11) ),
inference(resolve,[status(thm)],[c_266,c_19]) ).
cnf(c_268,plain,
( organization(sk2,sk12)
| ~ greater(sk13,sk12) ),
inference(resolve,[status(thm)],[c_267,c_104]) ).
cnf(c_138,plain,
organization(sk2,sk12),
inference(resolve,[status(thm)],[c_268,c_86]) ).
cnf(c_269,plain,
( organization(sk3,B)
| ~ greater(A,B)
| ~ greater(B,sk11)
| ~ organization(sk3,A) ),
inference(resolve,[status(thm)],[c_26,c_20]) ).
cnf(c_270,plain,
( organization(sk3,A)
| ~ greater(sk13,A)
| ~ greater(A,sk11) ),
inference(resolve,[status(thm)],[c_269,c_18]) ).
cnf(c_271,plain,
( organization(sk3,sk12)
| ~ greater(sk13,sk12) ),
inference(resolve,[status(thm)],[c_270,c_104]) ).
cnf(c_139,plain,
organization(sk3,sk12),
inference(resolve,[status(thm)],[c_271,c_86]) ).
cnf(c_140,plain,
( greater(B,A)
| ~ survival_chance(sk2,B,sk13)
| ~ survival_chance(sk2,A,sk12) ),
inference(resolve,[status(thm)],[c_138,c_95]) ).
cnf(c_151,plain,
survival_chance(sk2,sk1(sk12,sk2),sk12),
inference(resolve,[status(thm)],[c_138,c_27]) ).
cnf(c_158,plain,
survival_chance(sk3,sk1(sk12,sk3),sk12),
inference(resolve,[status(thm)],[c_139,c_27]) ).
cnf(c_198,plain,
( greater(sk7,A)
| ~ survival_chance(sk2,A,sk12) ),
inference(resolve,[status(thm)],[c_140,c_9]) ).
cnf(c_204,plain,
greater(sk7,sk1(sk12,sk2)),
inference(resolve,[status(thm)],[c_151,c_198]) ).
cnf(c_272,plain,
( greater(sk7,A)
| ~ greater(sk1(sk12,sk2),A) ),
inference(resolve,[status(thm)],[c_28,c_204]) ).
cnf(c_219,plain,
~ greater(sk1(sk12,sk2),sk8),
inference(resolve,[status(thm)],[c_272,c_4]) ).
cnf(c_273,plain,
( E = F
| greater(E,F)
| ~ greater(V7,V6)
| ~ complexity(sk3,V7,sk11)
| ~ complexity(sk2,V6,sk11)
| ~ survival_chance(sk3,F,A)
| ~ survival_chance(sk2,E,A)
| ~ reorganization_type(sk2,sk4,sk11)
| ~ reorganization(sk3,sk11,D)
| ~ reorganization(sk2,sk11,A)
| ~ survival_chance(sk3,C,sk11)
| ~ survival_chance(sk2,C,sk11)
| ~ class(sk3,B,sk11)
| ~ class(sk2,B,sk11)
| ~ organization(sk3,A)
| ~ organization(sk2,A) ),
inference(resolve,[status(thm)],[c_57,c_21]) ).
cnf(c_274,plain,
( D = E
| greater(D,E)
| ~ greater(V6,F)
| ~ complexity(sk3,V6,sk11)
| ~ complexity(sk2,F,sk11)
| ~ survival_chance(sk3,E,sk12)
| ~ survival_chance(sk2,D,sk12)
| ~ reorganization_type(sk2,sk4,sk11)
| ~ reorganization(sk3,sk11,C)
| ~ reorganization(sk2,sk11,sk12)
| ~ survival_chance(sk3,B,sk11)
| ~ survival_chance(sk2,B,sk11)
| ~ class(sk3,A,sk11)
| ~ class(sk2,A,sk11)
| ~ organization(sk3,sk12) ),
inference(resolve,[status(thm)],[c_273,c_138]) ).
cnf(c_275,plain,
( D = E
| greater(D,E)
| ~ greater(V6,F)
| ~ complexity(sk3,V6,sk11)
| ~ complexity(sk2,F,sk11)
| ~ survival_chance(sk3,E,sk12)
| ~ survival_chance(sk2,D,sk12)
| ~ reorganization_type(sk2,sk4,sk11)
| ~ reorganization(sk3,sk11,C)
| ~ reorganization(sk2,sk11,sk12)
| ~ survival_chance(sk3,B,sk11)
| ~ survival_chance(sk2,B,sk11)
| ~ class(sk3,A,sk11)
| ~ class(sk2,A,sk11) ),
inference(resolve,[status(thm)],[c_274,c_139]) ).
cnf(c_276,plain,
( C = D
| greater(C,D)
| ~ greater(F,E)
| ~ complexity(sk3,F,sk11)
| ~ complexity(sk2,E,sk11)
| ~ survival_chance(sk3,D,sk12)
| ~ survival_chance(sk2,C,sk12)
| ~ reorganization_type(sk2,sk4,sk11)
| ~ reorganization(sk3,sk11,B)
| ~ reorganization(sk2,sk11,sk12)
| ~ survival_chance(sk3,A,sk11)
| ~ survival_chance(sk2,A,sk11)
| ~ class(sk3,sk5,sk11) ),
inference(resolve,[status(thm)],[c_275,c_17]) ).
cnf(c_277,plain,
( C = D
| greater(C,D)
| ~ greater(F,E)
| ~ complexity(sk3,F,sk11)
| ~ complexity(sk2,E,sk11)
| ~ survival_chance(sk3,D,sk12)
| ~ survival_chance(sk2,C,sk12)
| ~ reorganization_type(sk2,sk4,sk11)
| ~ reorganization(sk3,sk11,B)
| ~ reorganization(sk2,sk11,sk12)
| ~ survival_chance(sk3,A,sk11)
| ~ survival_chance(sk2,A,sk11) ),
inference(resolve,[status(thm)],[c_276,c_16]) ).
cnf(c_278,plain,
( B = C
| greater(B,C)
| ~ greater(E,D)
| ~ complexity(sk3,E,sk11)
| ~ complexity(sk2,D,sk11)
| ~ survival_chance(sk3,C,sk12)
| ~ survival_chance(sk2,B,sk12)
| ~ reorganization_type(sk2,sk4,sk11)
| ~ reorganization(sk3,sk11,A)
| ~ reorganization(sk2,sk11,sk12)
| ~ survival_chance(sk3,sk6,sk11) ),
inference(resolve,[status(thm)],[c_277,c_15]) ).
cnf(c_279,plain,
( B = C
| greater(B,C)
| ~ greater(E,D)
| ~ complexity(sk3,E,sk11)
| ~ complexity(sk2,D,sk11)
| ~ survival_chance(sk3,C,sk12)
| ~ survival_chance(sk2,B,sk12)
| ~ reorganization_type(sk2,sk4,sk11)
| ~ reorganization(sk3,sk11,A)
| ~ reorganization(sk2,sk11,sk12) ),
inference(resolve,[status(thm)],[c_278,c_14]) ).
cnf(c_280,plain,
( B = C
| greater(B,C)
| ~ greater(E,D)
| ~ complexity(sk3,E,sk11)
| ~ complexity(sk2,D,sk11)
| ~ survival_chance(sk3,C,sk12)
| ~ survival_chance(sk2,B,sk12)
| ~ reorganization_type(sk2,sk4,sk11)
| ~ reorganization(sk3,sk11,A) ),
inference(resolve,[status(thm)],[c_279,c_13]) ).
cnf(c_281,plain,
( A = B
| greater(A,B)
| ~ greater(D,C)
| ~ complexity(sk3,D,sk11)
| ~ complexity(sk2,C,sk11)
| ~ survival_chance(sk3,B,sk12)
| ~ survival_chance(sk2,A,sk12)
| ~ reorganization_type(sk2,sk4,sk11) ),
inference(resolve,[status(thm)],[c_280,c_12]) ).
cnf(c_282,plain,
( A = B
| greater(A,B)
| ~ greater(D,C)
| ~ complexity(sk3,D,sk11)
| ~ complexity(sk2,C,sk11)
| ~ survival_chance(sk3,B,sk12)
| ~ survival_chance(sk2,A,sk12) ),
inference(resolve,[status(thm)],[c_281,c_11]) ).
cnf(c_283,plain,
( sk1(sk12,sk2) = A
| greater(sk1(sk12,sk2),A)
| ~ greater(C,B)
| ~ complexity(sk3,C,sk11)
| ~ complexity(sk2,B,sk11)
| ~ survival_chance(sk3,A,sk12) ),
inference(resolve,[status(thm)],[c_282,c_151]) ).
cnf(c_284,plain,
( sk1(sk12,sk2) = sk1(sk12,sk3)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| ~ greater(B,A)
| ~ complexity(sk3,B,sk11)
| ~ complexity(sk2,A,sk11) ),
inference(resolve,[status(thm)],[c_283,c_158]) ).
cnf(c_285,plain,
( sk1(sk12,sk2) = sk1(sk12,sk3)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| ~ greater(A,sk9)
| ~ complexity(sk3,A,sk11) ),
inference(resolve,[status(thm)],[c_284,c_7]) ).
cnf(c_286,plain,
( sk1(sk12,sk2) = sk1(sk12,sk3)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| ~ greater(sk10,sk9) ),
inference(resolve,[status(thm)],[c_285,c_6]) ).
cnf(c_287,plain,
( sk1(sk12,sk2) = sk1(sk12,sk3)
| greater(sk1(sk12,sk2),sk1(sk12,sk3)) ),
inference(resolve,[status(thm)],[c_286,c_5]) ).
cnf(c_225,plain,
( sk1(sk12,sk3) = sk1(sk12,sk2)
| greater(sk1(sk12,sk2),sk1(sk12,sk3)) ),
inference(copy,[status(thm)],[c_287]) ).
cnf(c_288,plain,
( greater(D,E)
| greater(A,C)
| ~ greater(A,sk12)
| greater(B,sk12)
| ~ survival_chance(sk3,E,A)
| ~ survival_chance(sk3,D,sk12)
| ~ reorganization(sk3,B,C)
| ~ organization(sk3,A) ),
inference(resolve,[status(thm)],[c_24,c_139]) ).
cnf(c_289,plain,
( greater(C,D)
| greater(sk13,B)
| ~ greater(sk13,sk12)
| greater(A,sk12)
| ~ survival_chance(sk3,D,sk13)
| ~ survival_chance(sk3,C,sk12)
| ~ reorganization(sk3,A,B) ),
inference(resolve,[status(thm)],[c_288,c_18]) ).
cnf(c_290,plain,
( greater(A,B)
| greater(sk13,sk13)
| ~ greater(sk13,sk12)
| greater(sk11,sk12)
| ~ survival_chance(sk3,B,sk13)
| ~ survival_chance(sk3,A,sk12) ),
inference(resolve,[status(thm)],[c_289,c_12]) ).
cnf(c_291,plain,
( greater(sk1(sk12,sk3),A)
| greater(sk13,sk13)
| ~ greater(sk13,sk12)
| greater(sk11,sk12)
| ~ survival_chance(sk3,A,sk13) ),
inference(resolve,[status(thm)],[c_290,c_158]) ).
cnf(c_292,plain,
( greater(sk1(sk12,sk3),sk8)
| greater(sk13,sk13)
| ~ greater(sk13,sk12)
| greater(sk11,sk12) ),
inference(resolve,[status(thm)],[c_291,c_8]) ).
cnf(c_293,plain,
( greater(sk1(sk12,sk3),sk8)
| greater(sk13,sk13)
| greater(sk11,sk12) ),
inference(resolve,[status(thm)],[c_292,c_86]) ).
cnf(c_294,plain,
( greater(sk1(sk12,sk3),sk8)
| greater(sk13,sk13) ),
inference(resolve,[status(thm)],[c_133,c_293]) ).
cnf(c_229,plain,
greater(sk1(sk12,sk3),sk8),
inference(resolve,[status(thm)],[c_49,c_294]) ).
cnf(c_295,plain,
( greater(A,sk8)
| ~ greater(A,sk1(sk12,sk3)) ),
inference(resolve,[status(thm)],[c_28,c_229]) ).
cnf(c_250,plain,
~ greater(sk1(sk12,sk2),sk1(sk12,sk3)),
inference(resolve,[status(thm)],[c_295,c_219]) ).
cnf(c_296,plain,
( greater(A,sk8)
| ~ greater(A,sk1(sk12,sk3)) ),
inference(resolve,[status(thm)],[c_28,c_229]) ).
cnf(c_251,plain,
~ greater(sk7,sk1(sk12,sk3)),
inference(resolve,[status(thm)],[c_296,c_4]) ).
cnf(c_252,plain,
sk1(sk12,sk3) = sk1(sk12,sk2),
inference(resolve,[status(thm)],[c_250,c_225]) ).
cnf(c_297,plain,
~ greater(sk7,sk1(sk12,sk2)),
inference(paramod,[status(thm)],[c_252,c_251]) ).
cnf(c_253,plain,
$false,
inference(resolve,[status(thm)],[c_204,c_297]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : MGT005-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.41 % Computer : n017.cluster.edu
% 0.08/0.41 % Model : x86_64 x86_64
% 0.08/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.41 % Memory : 8046.5625MB
% 0.08/0.41 % OS : Linux 6.8.0-71-generic
% 0.08/0.41 % CPULimit : 300
% 0.08/0.41 % WCLimit : 300
% 0.08/0.41 % DateTime : Fri Sep 25 23:58:02 UTC 2026
% 0.08/0.41 % CPUTime :
% 0.08/0.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.42 % Process 3505630 was started by sandbox on n017,
% 0.08/0.42 % Fri Sep 25 23:58:02 2026
% 0.08/0.42 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.42
% 0.08/0.42 % From the command line: assign(max_seconds, 300).
% 3.64/1.58
% 3.64/1.58 % SZS status Unsatisfiable for theBenchmark
% 3.64/1.58
% 3.64/1.58 % Proof 1 at 0.53 (+ 0.01) seconds.
% 3.64/1.58 % Length of proof is 50.
% 3.64/1.58 % Level of proof is 10.
% 3.64/1.58 % Maximum clause weight is 74.000.
% 3.64/1.58 % Given clauses 119.
% 3.64/1.58
% 3.64/1.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------