%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : MGT005-2 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:11:18 AM UTC 2026
% Result : Unsatisfiable 196.36s 25.07s
% Output : CNFRefutation 196.36s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named t5_plus_FOL_42ERROR: Could not build tree for root finalERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(16,plain,
organization(sk5,sk15),
inference(cnf,[status(esa)],[t5_plus_FOL_42]) ).
cnf(l0,plain,
organization(sk5,sk15),
inference(instantiation,[status(thm)],[16]) ).
cnf(10,plain,
( ~ reorganization(X0,X1,X2)
| ~ reorganization(X3,X1,X4)
| ~ organization(X0,X1)
| ~ organization(X0,X2)
| ~ organization(X3,X1)
| ~ organization(X3,X2)
| ~ class(X0,X5,X1)
| ~ class(X3,X5,X1)
| ~ reorganization_type(X0,X6,X1)
| ~ reorganization_type(X3,X6,X1)
| ~ complexity(X0,X7,X1)
| ~ complexity(X3,X8,X1)
| ~ survival_chance(X0,X9,X1)
| ~ survival_chance(X0,X10,X2)
| ~ survival_chance(X3,X9,X1)
| ~ survival_chance(X3,X11,X2)
| ~ greater(X8,X7)
| greater(X10,X11)
| X10 = X11 ),
inference(cnf,[status(esa)],[a11_FOL_36]) ).
cnf(l1,plain,
( ~ reorganization(sk5,sk15,sk16)
| ~ reorganization(sk6,sk15,sk17)
| ~ organization(sk5,sk15)
| ~ organization(sk5,sk16)
| ~ organization(sk6,sk15)
| ~ organization(sk6,sk16)
| ~ class(sk5,sk8,sk15)
| ~ class(sk6,sk8,sk15)
| ~ reorganization_type(sk5,sk7,sk15)
| ~ reorganization_type(sk6,sk7,sk15)
| ~ complexity(sk5,sk12,sk15)
| ~ complexity(sk6,sk13,sk15)
| ~ survival_chance(sk5,sk9,sk15)
| ~ survival_chance(sk5,sk10,sk16)
| ~ survival_chance(sk6,sk9,sk15)
| ~ survival_chance(sk6,sk11,sk16)
| ~ greater(sk13,sk12)
| greater(sk10,sk11)
| sk10 = sk11 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(20,plain,
class(sk5,sk8,sk15),
inference(cnf,[status(esa)],[t5_plus_FOL_46]) ).
cnf(l56,plain,
class(sk5,sk8,sk15),
inference(instantiation,[status(thm)],[20]) ).
cnf(33,plain,
greater(sk13,sk12),
inference(cnf,[status(esa)],[t5_plus_FOL_59]) ).
cnf(l2,plain,
greater(sk13,sk12),
inference(instantiation,[status(thm)],[33]) ).
cnf(24,plain,
reorganization(sk5,sk15,sk16),
inference(cnf,[status(esa)],[t5_plus_FOL_50]) ).
cnf(l38,plain,
reorganization(sk5,sk15,sk16),
inference(instantiation,[status(thm)],[24]) ).
cnf(17,plain,
organization(sk6,sk15),
inference(cnf,[status(esa)],[t5_plus_FOL_43]) ).
cnf(l129,plain,
organization(sk6,sk15),
inference(instantiation,[status(thm)],[17]) ).
cnf(5,plain,
( ~ organization(X0,X1)
| ~ organization(X0,X2)
| ~ greater(X2,X3)
| ~ greater(X3,X1)
| organization(X0,X3) ),
inference(cnf,[status(esa)],[mp13_31]) ).
cnf(l487,plain,
( ~ organization(sk6,sk15)
| ~ organization(sk6,sk17)
| ~ greater(sk17,sk16)
| ~ greater(sk16,sk15)
| organization(sk6,sk16) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(27,plain,
reorganization_type(sk6,sk7,sk15),
inference(cnf,[status(esa)],[t5_plus_FOL_53]) ).
cnf(l19,plain,
reorganization_type(sk6,sk7,sk15),
inference(instantiation,[status(thm)],[27]) ).
cnf(19,plain,
organization(sk6,sk17),
inference(cnf,[status(esa)],[t5_plus_FOL_45]) ).
cnf(l518,plain,
organization(sk6,sk17),
inference(instantiation,[status(thm)],[19]) ).
cnf(25,plain,
reorganization(sk6,sk15,sk17),
inference(cnf,[status(esa)],[t5_plus_FOL_51]) ).
cnf(l6,plain,
reorganization(sk6,sk15,sk17),
inference(instantiation,[status(thm)],[25]) ).
cnf(32,plain,
complexity(sk6,sk13,sk15),
inference(cnf,[status(esa)],[t5_plus_FOL_58]) ).
cnf(l146,plain,
complexity(sk6,sk13,sk15),
inference(instantiation,[status(thm)],[32]) ).
cnf(30,plain,
survival_chance(sk6,sk11,sk14),
inference(cnf,[status(esa)],[t5_plus_FOL_56]) ).
cnf(l584,plain,
survival_chance(sk6,sk11,sk14),
inference(instantiation,[status(thm)],[30]) ).
cnf(6,plain,
( ~ reorganization(X0,X1,X2)
| greater(X2,X1) ),
inference(cnf,[status(esa)],[mp7_32]) ).
cnf(l516,plain,
( ~ reorganization(sk5,sk15,sk16)
| greater(sk16,sk15) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(26,plain,
reorganization_type(sk5,sk7,sk15),
inference(cnf,[status(esa)],[t5_plus_FOL_52]) ).
cnf(l51,plain,
reorganization_type(sk5,sk7,sk15),
inference(instantiation,[status(thm)],[26]) ).
cnf(29,plain,
survival_chance(sk5,sk10,sk14),
inference(cnf,[status(esa)],[t5_plus_FOL_55]) ).
cnf(l11,plain,
survival_chance(sk5,sk10,sk14),
inference(instantiation,[status(thm)],[29]) ).
cnf(l513,plain,
organization(sk6,sk15),
inference(instantiation,[status(thm)],[17]) ).
cnf(l760,plain,
( ~ organization(sk5,sk15)
| ~ organization(sk5,sk17)
| ~ greater(sk17,sk16)
| ~ greater(sk16,sk15)
| organization(sk5,sk16) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(9,plain,
( ~ reorganization(X0,X1,X2)
| ~ reorganization(X3,X1,X4)
| ~ organization(X0,X1)
| ~ organization(X3,X1)
| ~ organization(X3,X4)
| ~ class(X0,X5,X1)
| ~ class(X3,X5,X1)
| ~ reorganization_type(X0,X6,X1)
| ~ reorganization_type(X3,X6,X1)
| ~ complexity(X0,X7,X1)
| ~ complexity(X3,X8,X1)
| ~ greater(X8,X7)
| greater(X4,X2) ),
inference(cnf,[status(esa)],[a10_FOL_35]) ).
cnf(l523,plain,
( ~ reorganization(sk5,sk15,sk16)
| ~ reorganization(sk6,sk15,sk17)
| ~ organization(sk5,sk15)
| ~ organization(sk6,sk15)
| ~ organization(sk6,sk17)
| ~ class(sk5,sk8,sk15)
| ~ class(sk6,sk8,sk15)
| ~ reorganization_type(sk5,sk7,sk15)
| ~ reorganization_type(sk6,sk7,sk15)
| ~ complexity(sk5,sk12,sk15)
| ~ complexity(sk6,sk13,sk15)
| ~ greater(sk13,sk12)
| greater(sk17,sk16) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(18,plain,
organization(sk5,sk17),
inference(cnf,[status(esa)],[t5_plus_FOL_44]) ).
cnf(l789,plain,
organization(sk5,sk17),
inference(instantiation,[status(thm)],[18]) ).
cnf(l893,plain,
organization(sk6,sk17),
inference(instantiation,[status(thm)],[19]) ).
cnf(l905,plain,
greater(sk13,sk12),
inference(instantiation,[status(thm)],[33]) ).
cnf(22,plain,
survival_chance(sk5,sk9,sk15),
inference(cnf,[status(esa)],[t5_plus_FOL_48]) ).
cnf(l3,plain,
survival_chance(sk5,sk9,sk15),
inference(instantiation,[status(thm)],[22]) ).
cnf(35,plain,
sk14 = sk16,
inference(cnf,[status(esa)],[t5_plus_FOL_61]) ).
cnf(l27,plain,
sk14 = sk16,
inference(instantiation,[status(thm)],[35]) ).
cnf(31,plain,
complexity(sk5,sk12,sk15),
inference(cnf,[status(esa)],[t5_plus_FOL_57]) ).
cnf(l9,plain,
complexity(sk5,sk12,sk15),
inference(instantiation,[status(thm)],[31]) ).
cnf(l599,plain,
sk14 = sk16,
inference(instantiation,[status(thm)],[35]) ).
cnf(l774,plain,
( ~ reorganization(sk5,sk15,sk16)
| ~ reorganization(sk6,sk15,sk17)
| ~ organization(sk5,sk15)
| ~ organization(sk6,sk15)
| ~ organization(sk6,sk17)
| ~ class(sk5,sk8,sk15)
| ~ class(sk6,sk8,sk15)
| ~ reorganization_type(sk5,sk7,sk15)
| ~ reorganization_type(sk6,sk7,sk15)
| ~ complexity(sk5,sk12,sk15)
| ~ complexity(sk6,sk13,sk15)
| ~ greater(sk13,sk12)
| greater(sk17,sk16) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(21,plain,
class(sk6,sk8,sk15),
inference(cnf,[status(esa)],[t5_plus_FOL_47]) ).
cnf(l901,plain,
class(sk6,sk8,sk15),
inference(instantiation,[status(thm)],[21]) ).
cnf(l834,plain,
reorganization(sk6,sk15,sk17),
inference(instantiation,[status(thm)],[25]) ).
cnf(l762,plain,
( ~ reorganization(sk5,sk15,sk16)
| greater(sk16,sk15) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l853,plain,
reorganization(sk6,sk15,sk17),
inference(instantiation,[status(thm)],[25]) ).
cnf(l890,plain,
organization(sk6,sk15),
inference(instantiation,[status(thm)],[17]) ).
cnf(l898,plain,
reorganization(sk5,sk15,sk16),
inference(instantiation,[status(thm)],[24]) ).
cnf(l891,plain,
reorganization_type(sk5,sk7,sk15),
inference(instantiation,[status(thm)],[26]) ).
cnf(l1482,plain,
greater(sk13,sk12),
inference(instantiation,[status(thm)],[33]) ).
cnf(l904,plain,
reorganization_type(sk6,sk7,sk15),
inference(instantiation,[status(thm)],[27]) ).
cnf(l906,plain,
organization(sk6,sk17),
inference(instantiation,[status(thm)],[19]) ).
cnf(l781,plain,
class(sk6,sk8,sk15),
inference(instantiation,[status(thm)],[21]) ).
cnf(l856,plain,
reorganization(sk5,sk15,sk16),
inference(instantiation,[status(thm)],[24]) ).
cnf(l23,plain,
class(sk6,sk8,sk15),
inference(instantiation,[status(thm)],[21]) ).
cnf(l526,plain,
reorganization(sk5,sk15,sk16),
inference(instantiation,[status(thm)],[24]) ).
cnf(l2074,plain,
complexity(sk5,sk12,sk15),
inference(instantiation,[status(thm)],[31]) ).
cnf(l804,plain,
complexity(sk6,sk13,sk15),
inference(instantiation,[status(thm)],[32]) ).
cnf(l835,plain,
class(sk5,sk8,sk15),
inference(instantiation,[status(thm)],[20]) ).
cnf(23,plain,
survival_chance(sk6,sk9,sk15),
inference(cnf,[status(esa)],[t5_plus_FOL_49]) ).
cnf(l128,plain,
survival_chance(sk6,sk9,sk15),
inference(instantiation,[status(thm)],[23]) ).
cnf(l861,plain,
complexity(sk5,sk12,sk15),
inference(instantiation,[status(thm)],[31]) ).
cnf(l862,plain,
reorganization_type(sk5,sk7,sk15),
inference(instantiation,[status(thm)],[26]) ).
cnf(l900,plain,
organization(sk6,sk15),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1484,plain,
complexity(sk6,sk13,sk15),
inference(instantiation,[status(thm)],[32]) ).
cnf(l803,plain,
reorganization(sk5,sk15,sk16),
inference(instantiation,[status(thm)],[24]) ).
cnf(37,plain,
sk10 != sk11,
inference(cnf,[status(esa)],[t5_plus_FOL_63]) ).
cnf(l8,plain,
sk10 != sk11,
inference(instantiation,[status(thm)],[37]) ).
cnf(l907,plain,
class(sk5,sk8,sk15),
inference(instantiation,[status(thm)],[20]) ).
cnf(l920,plain,
reorganization_type(sk6,sk7,sk15),
inference(instantiation,[status(thm)],[27]) ).
cnf(36,plain,
~ greater(sk10,sk11),
inference(cnf,[status(esa)],[t5_plus_FOL_62]) ).
cnf(l7,plain,
~ greater(sk10,sk11),
inference(instantiation,[status(thm)],[36]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l56,l2,l38,l129,l487,l19,l518,l6,l146,l584,l516,l51,l11,l513,l760,l523,l789,l893,l905,l3,l27,l9,l599,l774,l901,l834,l762,l853,l890,l898,l891,l1482,l904,l906,l781,l856,l23,l526,l2074,l804,l835,l128,l861,l862,l900,l1484,l803,l8,l907,l920,l7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT005-2 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n006.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 7 11:40:46 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % launching worker at depth: 1
% 0.09/0.38 % launching worker at depth: 3
% 0.09/0.38 % launching worker at depth: 8
% 0.09/0.38 % launching worker at depth: 4
% 0.09/0.38 % launching worker at depth: 5
% 0.09/0.38 % launching worker at depth: 6
% 0.09/0.38 % launching worker at depth: 7
% 0.09/0.38 % launching worker at depth: 2
% 0.09/0.39 % launching worker at depth: 9
% 0.09/0.46 % launching worker at depth: 10
% 12.17/1.95 % launching worker at depth: 11
% 196.36/25.07 % SZS status Theorem for theBenchmark
% 196.36/25.07 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------