%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT005-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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 : Tue Sep 8 06:18:37 AM UTC 2026
% Result : Unsatisfiable 7.97s 8.20s
% Output : CNFRefutation 7.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 31
% Syntax : Number of clauses : 95 ( 33 unt; 30 nHn; 94 RR)
% Number of literals : 430 ( 26 equ; 303 neg)
% Maximal clause size : 19 ( 4 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 : 127 ( 8 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t5_FOL_54,negated_conjecture,
~ greater(sk7,sk8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_54) ).
cnf(t5_FOL_36,negated_conjecture,
organization(sk2,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_36) ).
cnf(t5_FOL_38,negated_conjecture,
organization(sk2,sk13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_38) ).
cnf(t5_FOL_44,negated_conjecture,
reorganization(sk2,sk11,sk12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_44) ).
cnf(mp7_31,axiom,
( ~ reorganization(X22,X21,X20)
| greater(X20,X21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp7_31) ).
cnf(c21,plain,
greater(sk12,sk11),
inference(resolution,[status(thm)],[mp7_31,t5_FOL_44]) ).
cnf(mp13_30,axiom,
( ~ organization(X17,X16)
| ~ organization(X17,X14)
| ~ greater(X15,X16)
| ~ greater(X14,X15)
| organization(X17,X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp13_30) ).
cnf(t5_FOL_37,negated_conjecture,
organization(sk3,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_37) ).
cnf(t5_FOL_39,negated_conjecture,
organization(sk3,sk13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_39) ).
cnf(t5_FOL_53,negated_conjecture,
greater(sk10,sk9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_53) ).
cnf(t5_FOL_40,negated_conjecture,
class(sk2,sk5,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_40) ).
cnf(t5_FOL_41,negated_conjecture,
class(sk3,sk5,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_41) ).
cnf(t5_FOL_45,negated_conjecture,
reorganization(sk3,sk11,sk13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_45) ).
cnf(t5_FOL_46,negated_conjecture,
reorganization_type(sk2,sk4,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_46) ).
cnf(t5_FOL_47,negated_conjecture,
reorganization_type(sk3,sk4,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_47) ).
cnf(t5_FOL_51,negated_conjecture,
complexity(sk2,sk9,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_51) ).
cnf(t5_FOL_52,negated_conjecture,
complexity(sk3,sk10,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_52) ).
cnf(a10_FOL_34,plain,
( ~ organization(X48,X53)
| ~ organization(X52,X53)
| ~ organization(X52,X46)
| ~ class(X48,X50,X53)
| ~ class(X52,X50,X53)
| ~ reorganization(X48,X53,X51)
| ~ reorganization(X52,X53,X46)
| ~ reorganization_type(X48,X49,X53)
| ~ reorganization_type(X52,X49,X53)
| ~ complexity(X48,X54,X53)
| ~ complexity(X52,X47,X53)
| ~ greater(X47,X54)
| greater(X46,X51) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a10_FOL_34) ).
cnf(c48,plain,
( ~ organization(X331,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk3,X328)
| ~ class(X331,X329,sk11)
| ~ class(sk3,X329,sk11)
| ~ reorganization(X331,sk11,X332)
| ~ reorganization(sk3,sk11,X328)
| ~ reorganization_type(X331,X327,sk11)
| ~ reorganization_type(sk3,X327,sk11)
| ~ complexity(X331,X330,sk11)
| ~ greater(sk10,X330)
| greater(X328,X332) ),
inference(resolution,[status(thm)],[a10_FOL_34,t5_FOL_52]) ).
cnf(c209,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk3,X525)
| ~ class(sk2,X527,sk11)
| ~ class(sk3,X527,sk11)
| ~ reorganization(sk2,sk11,X526)
| ~ reorganization(sk3,sk11,X525)
| ~ reorganization_type(sk2,X524,sk11)
| ~ reorganization_type(sk3,X524,sk11)
| ~ greater(sk10,sk9)
| greater(X525,X526) ),
inference(resolution,[status(thm)],[c48,t5_FOL_51]) ).
cnf(c363,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk3,X732)
| ~ class(sk2,X731,sk11)
| ~ class(sk3,X731,sk11)
| ~ reorganization(sk2,sk11,X733)
| ~ reorganization(sk3,sk11,X732)
| ~ reorganization_type(sk2,sk4,sk11)
| ~ greater(sk10,sk9)
| greater(X732,X733) ),
inference(resolution,[status(thm)],[c209,t5_FOL_47]) ).
cnf(c609,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk3,X1037)
| ~ class(sk2,X1036,sk11)
| ~ class(sk3,X1036,sk11)
| ~ reorganization(sk2,sk11,X1038)
| ~ reorganization(sk3,sk11,X1037)
| ~ greater(sk10,sk9)
| greater(X1037,X1038) ),
inference(resolution,[status(thm)],[c363,t5_FOL_46]) ).
cnf(c1037,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk3,sk13)
| ~ class(sk2,X1660,sk11)
| ~ class(sk3,X1660,sk11)
| ~ reorganization(sk2,sk11,X1659)
| ~ greater(sk10,sk9)
| greater(sk13,X1659) ),
inference(resolution,[status(thm)],[c609,t5_FOL_45]) ).
cnf(c1939,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk3,sk13)
| ~ class(sk2,X1872,sk11)
| ~ class(sk3,X1872,sk11)
| ~ greater(sk10,sk9)
| greater(sk13,sk12) ),
inference(resolution,[status(thm)],[c1037,t5_FOL_44]) ).
cnf(c2182,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk3,sk13)
| ~ class(sk2,sk5,sk11)
| ~ greater(sk10,sk9)
| greater(sk13,sk12) ),
inference(resolution,[status(thm)],[c1939,t5_FOL_41]) ).
cnf(c2183,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk3,sk13)
| ~ greater(sk10,sk9)
| greater(sk13,sk12) ),
inference(resolution,[status(thm)],[c2182,t5_FOL_40]) ).
cnf(c2184,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk3,sk13)
| greater(sk13,sk12) ),
inference(resolution,[status(thm)],[c2183,t5_FOL_53]) ).
cnf(c2185,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| greater(sk13,sk12) ),
inference(resolution,[status(thm)],[c2184,t5_FOL_39]) ).
cnf(c2186,plain,
( ~ organization(sk2,sk11)
| greater(sk13,sk12) ),
inference(resolution,[status(thm)],[c2185,t5_FOL_37]) ).
cnf(c2187,plain,
greater(sk13,sk12),
inference(resolution,[status(thm)],[c2186,t5_FOL_36]) ).
cnf(c2194,plain,
( ~ organization(X1880,X1881)
| ~ organization(X1880,sk13)
| ~ greater(sk12,X1881)
| organization(X1880,sk12) ),
inference(resolution,[status(thm)],[c2187,mp13_30]) ).
cnf(c2197,plain,
( ~ organization(X1882,sk11)
| ~ organization(X1882,sk13)
| organization(X1882,sk12) ),
inference(resolution,[status(thm)],[c2194,c21]) ).
cnf(c2198,plain,
( ~ organization(sk2,sk11)
| organization(sk2,sk12) ),
inference(resolution,[status(thm)],[c2197,t5_FOL_38]) ).
cnf(c2200,plain,
organization(sk2,sk12),
inference(resolution,[status(thm)],[c2198,t5_FOL_36]) ).
cnf(t5_FOL_48,negated_conjecture,
reorganization_free(sk2,sk12,sk13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_48) ).
cnf(t5_FOL_49,negated_conjecture,
survival_chance(sk2,sk7,sk13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_49) ).
cnf(t3_FOL_32,plain,
( ~ organization(X25,X28)
| ~ organization(X25,X27)
| ~ reorganization_free(X25,X28,X27)
| ~ survival_chance(X25,X24,X28)
| ~ survival_chance(X25,X26,X27)
| ~ greater(X27,X28)
| greater(X26,X24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_FOL_32) ).
cnf(c33,plain,
( ~ organization(sk2,X221)
| ~ organization(sk2,sk13)
| ~ reorganization_free(sk2,X221,sk13)
| ~ survival_chance(sk2,X222,X221)
| ~ greater(sk13,X221)
| greater(sk7,X222) ),
inference(resolution,[status(thm)],[t3_FOL_32,t5_FOL_49]) ).
cnf(mp12_29,axiom,
( ~ organization(X13,X12)
| survival_chance(X13,sk1(X12,X13),X12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp12_29) ).
cnf(c2202,plain,
survival_chance(sk2,sk1(sk12,sk2),sk12),
inference(resolution,[status(thm)],[c2200,mp12_29]) ).
cnf(c2223,plain,
( ~ organization(sk2,sk12)
| ~ organization(sk2,sk13)
| ~ reorganization_free(sk2,sk12,sk13)
| ~ greater(sk13,sk12)
| greater(sk7,sk1(sk12,sk2)) ),
inference(resolution,[status(thm)],[c2202,c33]) ).
cnf(c2259,plain,
( ~ organization(sk2,sk12)
| ~ organization(sk2,sk13)
| ~ greater(sk13,sk12)
| greater(sk7,sk1(sk12,sk2)) ),
inference(resolution,[status(thm)],[c2223,t5_FOL_48]) ).
cnf(c2260,plain,
( ~ organization(sk2,sk12)
| ~ organization(sk2,sk13)
| greater(sk7,sk1(sk12,sk2)) ),
inference(resolution,[status(thm)],[c2259,c2187]) ).
cnf(c2262,plain,
( ~ organization(sk2,sk12)
| greater(sk7,sk1(sk12,sk2)) ),
inference(resolution,[status(thm)],[c2260,t5_FOL_38]) ).
cnf(c2263,plain,
greater(sk7,sk1(sk12,sk2)),
inference(resolution,[status(thm)],[c2262,c2200]) ).
cnf(mp11_28,axiom,
( ~ greater(X11,X10)
| ~ greater(X10,X9)
| greater(X11,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp11_28) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(mp6_1_26,axiom,
( ~ greater(X4,X3)
| X4 != X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp6_1_26) ).
cnf(c9,plain,
~ greater(X5,X5),
inference(resolution,[status(thm)],[mp6_1_26,reflexivity]) ).
cnf(mp6_2_27,axiom,
( ~ greater(X7,X6)
| ~ greater(X6,X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp6_2_27) ).
cnf(c25,plain,
~ greater(sk11,sk12),
inference(resolution,[status(thm)],[c21,mp6_2_27]) ).
cnf(c2199,plain,
( ~ organization(sk3,sk11)
| organization(sk3,sk12) ),
inference(resolution,[status(thm)],[c2197,t5_FOL_39]) ).
cnf(c2203,plain,
organization(sk3,sk12),
inference(resolution,[status(thm)],[c2199,t5_FOL_37]) ).
cnf(t5_FOL_50,negated_conjecture,
survival_chance(sk3,sk8,sk13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_50) ).
cnf(t4_FOL_33,plain,
( ~ organization(X37,X42)
| ~ organization(X37,X41)
| ~ reorganization(X37,X36,X39)
| ~ survival_chance(X37,X40,X42)
| ~ survival_chance(X37,X38,X41)
| greater(X36,X42)
| ~ greater(X41,X42)
| greater(X41,X39)
| greater(X40,X38) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_FOL_33) ).
cnf(c38,plain,
( ~ organization(sk3,X257)
| ~ organization(sk3,sk13)
| ~ reorganization(sk3,X255,X258)
| ~ survival_chance(sk3,X256,X257)
| greater(X255,X257)
| ~ greater(sk13,X257)
| greater(sk13,X258)
| greater(X256,sk8) ),
inference(resolution,[status(thm)],[t4_FOL_33,t5_FOL_50]) ).
cnf(c2205,plain,
survival_chance(sk3,sk1(sk12,sk3),sk12),
inference(resolution,[status(thm)],[c2203,mp12_29]) ).
cnf(c2247,plain,
( ~ organization(sk3,sk12)
| ~ organization(sk3,sk13)
| ~ reorganization(sk3,X2002,X2001)
| greater(X2002,sk12)
| ~ greater(sk13,sk12)
| greater(sk13,X2001)
| greater(sk1(sk12,sk3),sk8) ),
inference(resolution,[status(thm)],[c2205,c38]) ).
cnf(c2353,plain,
( ~ organization(sk3,sk12)
| ~ organization(sk3,sk13)
| greater(sk11,sk12)
| ~ greater(sk13,sk12)
| greater(sk13,sk13)
| greater(sk1(sk12,sk3),sk8) ),
inference(resolution,[status(thm)],[c2247,t5_FOL_45]) ).
cnf(c2354,plain,
( ~ organization(sk3,sk12)
| ~ organization(sk3,sk13)
| greater(sk11,sk12)
| greater(sk13,sk13)
| greater(sk1(sk12,sk3),sk8) ),
inference(resolution,[status(thm)],[c2353,c2187]) ).
cnf(c2355,plain,
( ~ organization(sk3,sk12)
| greater(sk11,sk12)
| greater(sk13,sk13)
| greater(sk1(sk12,sk3),sk8) ),
inference(resolution,[status(thm)],[c2354,t5_FOL_39]) ).
cnf(c2356,plain,
( greater(sk11,sk12)
| greater(sk13,sk13)
| greater(sk1(sk12,sk3),sk8) ),
inference(resolution,[status(thm)],[c2355,c2203]) ).
cnf(c2363,plain,
( greater(sk13,sk13)
| greater(sk1(sk12,sk3),sk8) ),
inference(resolution,[status(thm)],[c2356,c25]) ).
cnf(c2381,plain,
greater(sk1(sk12,sk3),sk8),
inference(resolution,[status(thm)],[c2363,c9]) ).
cnf(c2394,plain,
( ~ greater(X2005,sk1(sk12,sk3))
| greater(X2005,sk8) ),
inference(resolution,[status(thm)],[c2381,mp11_28]) ).
cnf(c1,axiom,
( X57 != X60
| X58 != X59
| ~ greater(X57,X58)
| greater(X60,X59) ),
theory(equality) ).
cnf(c2267,plain,
( sk7 != X1913
| sk1(sk12,sk2) != X1912
| greater(X1913,X1912) ),
inference(resolution,[status(thm)],[c2263,c1]) ).
cnf(t5_FOL_42,negated_conjecture,
survival_chance(sk2,sk6,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_42) ).
cnf(t5_FOL_43,negated_conjecture,
survival_chance(sk3,sk6,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_FOL_43) ).
cnf(a11_FOL_35,plain,
( ~ organization(X66,X74)
| ~ organization(X73,X74)
| ~ organization(X66,X64)
| ~ organization(X73,X64)
| ~ class(X66,X68,X74)
| ~ class(X73,X68,X74)
| ~ survival_chance(X66,X71,X74)
| ~ survival_chance(X73,X71,X74)
| ~ reorganization(X66,X74,X64)
| ~ reorganization(X73,X74,X67)
| ~ reorganization_type(X66,X75,X74)
| ~ reorganization_type(X73,X75,X74)
| ~ survival_chance(X66,X65,X64)
| ~ survival_chance(X73,X72,X64)
| ~ complexity(X66,X69,X74)
| ~ complexity(X73,X70,X74)
| ~ greater(X70,X69)
| greater(X65,X72)
| X65 = X72 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a11_FOL_35) ).
cnf(c58,plain,
( ~ organization(X377,sk11)
| ~ organization(sk3,sk11)
| ~ organization(X377,X374)
| ~ organization(sk3,X374)
| ~ class(X377,X370,sk11)
| ~ class(sk3,X370,sk11)
| ~ survival_chance(X377,X373,sk11)
| ~ survival_chance(sk3,X373,sk11)
| ~ reorganization(X377,sk11,X374)
| ~ reorganization(sk3,sk11,X369)
| ~ reorganization_type(X377,X372,sk11)
| ~ reorganization_type(sk3,X372,sk11)
| ~ survival_chance(X377,X371,X374)
| ~ survival_chance(sk3,X376,X374)
| ~ complexity(X377,X375,sk11)
| ~ greater(sk10,X375)
| greater(X371,X376)
| X371 = X376 ),
inference(resolution,[status(thm)],[a11_FOL_35,t5_FOL_52]) ).
cnf(c254,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk2,X581)
| ~ organization(sk3,X581)
| ~ class(sk2,X578,sk11)
| ~ class(sk3,X578,sk11)
| ~ survival_chance(sk2,X579,sk11)
| ~ survival_chance(sk3,X579,sk11)
| ~ reorganization(sk2,sk11,X581)
| ~ reorganization(sk3,sk11,X580)
| ~ reorganization_type(sk2,X577,sk11)
| ~ reorganization_type(sk3,X577,sk11)
| ~ survival_chance(sk2,X582,X581)
| ~ survival_chance(sk3,X583,X581)
| ~ greater(sk10,sk9)
| greater(X582,X583)
| X582 = X583 ),
inference(resolution,[status(thm)],[c58,t5_FOL_51]) ).
cnf(c2239,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk2,sk12)
| ~ organization(sk3,sk12)
| ~ class(sk2,X2669,sk11)
| ~ class(sk3,X2669,sk11)
| ~ survival_chance(sk2,X2673,sk11)
| ~ survival_chance(sk3,X2673,sk11)
| ~ reorganization(sk2,sk11,sk12)
| ~ reorganization(sk3,sk11,X2671)
| ~ reorganization_type(sk2,X2672,sk11)
| ~ reorganization_type(sk3,X2672,sk11)
| ~ survival_chance(sk2,X2670,sk12)
| ~ greater(sk10,sk9)
| greater(X2670,sk1(sk12,sk3))
| X2670 = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[c2205,c254]) ).
cnf(c2870,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk2,sk12)
| ~ organization(sk3,sk12)
| ~ class(sk2,X2833,sk11)
| ~ class(sk3,X2833,sk11)
| ~ survival_chance(sk2,X2834,sk11)
| ~ survival_chance(sk3,X2834,sk11)
| ~ reorganization(sk2,sk11,sk12)
| ~ reorganization(sk3,sk11,X2835)
| ~ reorganization_type(sk2,X2832,sk11)
| ~ reorganization_type(sk3,X2832,sk11)
| ~ greater(sk10,sk9)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[c2239,c2202]) ).
cnf(c2932,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk2,sk12)
| ~ organization(sk3,sk12)
| ~ class(sk2,X2854,sk11)
| ~ class(sk3,X2854,sk11)
| ~ survival_chance(sk2,X2855,sk11)
| ~ survival_chance(sk3,X2855,sk11)
| ~ reorganization(sk2,sk11,sk12)
| ~ reorganization(sk3,sk11,X2853)
| ~ reorganization_type(sk2,sk4,sk11)
| ~ greater(sk10,sk9)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[c2870,t5_FOL_47]) ).
cnf(c3091,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk2,sk12)
| ~ organization(sk3,sk12)
| ~ class(sk2,X3002,sk11)
| ~ class(sk3,X3002,sk11)
| ~ survival_chance(sk2,X3003,sk11)
| ~ survival_chance(sk3,X3003,sk11)
| ~ reorganization(sk2,sk11,sk12)
| ~ reorganization(sk3,sk11,X3004)
| ~ greater(sk10,sk9)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[c2932,t5_FOL_46]) ).
cnf(c3103,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk2,sk12)
| ~ organization(sk3,sk12)
| ~ class(sk2,X3010,sk11)
| ~ class(sk3,X3010,sk11)
| ~ survival_chance(sk2,X3011,sk11)
| ~ survival_chance(sk3,X3011,sk11)
| ~ reorganization(sk2,sk11,sk12)
| ~ greater(sk10,sk9)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[c3091,t5_FOL_45]) ).
cnf(c3236,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk2,sk12)
| ~ organization(sk3,sk12)
| ~ class(sk2,X3157,sk11)
| ~ class(sk3,X3157,sk11)
| ~ survival_chance(sk2,X3156,sk11)
| ~ survival_chance(sk3,X3156,sk11)
| ~ greater(sk10,sk9)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[c3103,t5_FOL_44]) ).
cnf(c3263,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk2,sk12)
| ~ organization(sk3,sk12)
| ~ class(sk2,X3159,sk11)
| ~ class(sk3,X3159,sk11)
| ~ survival_chance(sk2,sk6,sk11)
| ~ greater(sk10,sk9)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[c3236,t5_FOL_43]) ).
cnf(c3265,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk2,sk12)
| ~ organization(sk3,sk12)
| ~ class(sk2,X3160,sk11)
| ~ class(sk3,X3160,sk11)
| ~ greater(sk10,sk9)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[c3263,t5_FOL_42]) ).
cnf(c3266,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk2,sk12)
| ~ organization(sk3,sk12)
| ~ class(sk2,sk5,sk11)
| ~ greater(sk10,sk9)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[c3265,t5_FOL_41]) ).
cnf(c3267,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk2,sk12)
| ~ organization(sk3,sk12)
| ~ greater(sk10,sk9)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[c3266,t5_FOL_40]) ).
cnf(c3268,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk2,sk12)
| ~ organization(sk3,sk12)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[c3267,t5_FOL_53]) ).
cnf(c3269,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| ~ organization(sk2,sk12)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[c3268,c2203]) ).
cnf(c3270,plain,
( ~ organization(sk2,sk11)
| ~ organization(sk3,sk11)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[c3269,c2200]) ).
cnf(c3271,plain,
( ~ organization(sk2,sk11)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[c3270,t5_FOL_37]) ).
cnf(c3272,plain,
( greater(sk1(sk12,sk2),sk1(sk12,sk3))
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[c3271,t5_FOL_36]) ).
cnf(c3281,plain,
( sk1(sk12,sk2) = sk1(sk12,sk3)
| greater(sk1(sk12,sk2),sk8) ),
inference(resolution,[status(thm)],[c3272,c2394]) ).
cnf(c3303,plain,
( greater(sk1(sk12,sk2),sk8)
| sk7 != X3164
| greater(X3164,sk1(sk12,sk3)) ),
inference(resolution,[status(thm)],[c3281,c2267]) ).
cnf(c3332,plain,
( greater(sk1(sk12,sk2),sk8)
| greater(sk7,sk1(sk12,sk3)) ),
inference(resolution,[status(thm)],[c3303,reflexivity]) ).
cnf(c3346,plain,
( greater(sk1(sk12,sk2),sk8)
| greater(sk7,sk8) ),
inference(resolution,[status(thm)],[c3332,c2394]) ).
cnf(c3356,plain,
greater(sk1(sk12,sk2),sk8),
inference(resolution,[status(thm)],[c3346,t5_FOL_54]) ).
cnf(c3368,plain,
( ~ greater(X3166,sk1(sk12,sk2))
| greater(X3166,sk8) ),
inference(resolution,[status(thm)],[c3356,mp11_28]) ).
cnf(c3370,plain,
greater(sk7,sk8),
inference(resolution,[status(thm)],[c3368,c2263]) ).
cnf(c3374,plain,
$false,
inference(resolution,[status(thm)],[c3370,t5_FOL_54]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT005-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.37 % Computer : n026.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 7 11:40:57 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.43 (re.compile("\."), Token.FullStop),
% 0.12/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.44 (re.compile("\("), Token.OpenPar),
% 0.12/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.44 (re.compile("\)"), Token.ClosePar),
% 0.12/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.44 (re.compile("\["), Token.OpenSquare),
% 0.12/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.44 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.44 (re.compile("~\|"), Token.Nor),
% 0.12/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.44 (re.compile("\|"), Token.Or),
% 0.12/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.44 (re.compile("\?"), Token.Existential),
% 0.12/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.44 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.44 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.24/0.51 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.51 """
% 0.24/0.51 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.51 """
% 0.33/0.60 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.60 """
% 7.97/8.20 % Version: 1.5
% 7.97/8.20 % SZS status Unsatisfiable
% 7.97/8.20 % SZS output start CNFRefutation
% See solution above
% 7.97/8.20
% 7.97/8.20 % Initial clauses : 41
% 7.97/8.20 % Processed clauses : 1215
% 7.97/8.20 % Factors computed : 29
% 7.97/8.20 % Resolvents computed: 3343
% 7.97/8.20 % Tautologies deleted: 151
% 7.97/8.20 % Forward subsumed : 1952
% 7.97/8.20 % Backward subsumed : 907
% 7.97/8.20 % -------- CPU Time ---------
% 7.97/8.20 % User time : 7.795 s
% 7.97/8.20 % System time : 0.031 s
% 7.97/8.20 % Total time : 7.826 s
%------------------------------------------------------------------------------