%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MGT005-2 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n013.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 : Fri Sep 25 02:11:15 PM UTC 2026
% Result : Unsatisfiable 11.24s 2.07s
% Output : Proof 11.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 24
% Syntax : Number of formulae : 120 ( 70 unt; 0 def)
% Number of atoms : 491 ( 29 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 729 ( 358 ~; 371 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 13 con; 0-0 aty)
% Number of variables : 241 ( 13 sgn 56 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f9,hypothesis,
( greater(D,F)
| ~ greater(I,H)
| ~ complexity(C,I,B)
| ~ complexity(A,H,B)
| ~ reorganization_type(C,G,B)
| ~ reorganization_type(A,G,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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a10_FOL_35) ).
fof(f9_nnf,plain,
! [A,B,C,D,E,F,G,H,I] :
( greater(D,F)
| ~ greater(I,H)
| ~ complexity(C,I,B)
| ~ complexity(A,H,B)
| ~ reorganization_type(C,G,B)
| ~ reorganization_type(A,G,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(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A,B,C,D,E,F,G,H,I] :
( greater(D,F)
| ~ greater(I,H)
| ~ complexity(C,I,B)
| ~ complexity(A,H,B)
| ~ reorganization_type(C,G,B)
| ~ reorganization_type(A,G,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(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( greater(X3,X5)
| ~ greater(X8,X7)
| ~ complexity(X2,X8,X1)
| ~ complexity(X0,X7,X1)
| ~ reorganization_type(X2,X6,X1)
| ~ reorganization_type(X0,X6,X1)
| ~ reorganization(X2,X1,X3)
| ~ reorganization(X0,X1,X5)
| ~ class(X2,X4,X1)
| ~ class(X0,X4,X1)
| ~ organization(X2,X3)
| ~ organization(X2,X1)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(f16,negated_conjecture,
organization(sk5,sk15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_42) ).
fof(f16_nnf,plain,
organization(sk5,sk15),
inference(nnf_transformation,[status(thm)],[f16]) ).
cnf(c16,plain,
organization(sk5,sk15),
inference(cnf_transformation,[status(esa)],[f16_nnf]) ).
cnf(p77,plain,
( greater(X1,X3)
| ~ greater(X6,X5)
| ~ complexity(X0,X6,sk15)
| ~ complexity(sk5,X5,sk15)
| ~ reorganization_type(X0,X4,sk15)
| ~ reorganization_type(sk5,X4,sk15)
| ~ reorganization(X0,sk15,X1)
| ~ reorganization(sk5,sk15,X3)
| ~ class(X0,X2,sk15)
| ~ class(sk5,X2,sk15)
| ~ organization(X0,X1)
| ~ organization(X0,sk15) ),
inference(resolution,[status(thm)],[c9,c16]) ).
cnf(f17,negated_conjecture,
organization(sk6,sk15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_43) ).
fof(f17_nnf,plain,
organization(sk6,sk15),
inference(nnf_transformation,[status(thm)],[f17]) ).
cnf(c17,plain,
organization(sk6,sk15),
inference(cnf_transformation,[status(esa)],[f17_nnf]) ).
cnf(p214,plain,
( greater(X0,X2)
| ~ greater(X5,X4)
| ~ complexity(sk6,X5,sk15)
| ~ complexity(sk5,X4,sk15)
| ~ reorganization_type(sk6,X3,sk15)
| ~ reorganization_type(sk5,X3,sk15)
| ~ reorganization(sk6,sk15,X0)
| ~ reorganization(sk5,sk15,X2)
| ~ class(sk6,X1,sk15)
| ~ class(sk5,X1,sk15)
| ~ organization(sk6,X0) ),
inference(resolution,[status(thm)],[p77,c17]) ).
cnf(f19,negated_conjecture,
organization(sk6,sk17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_45) ).
fof(f19_nnf,plain,
organization(sk6,sk17),
inference(nnf_transformation,[status(thm)],[f19]) ).
cnf(c19,plain,
organization(sk6,sk17),
inference(cnf_transformation,[status(esa)],[f19_nnf]) ).
cnf(p677,plain,
( greater(sk17,X1)
| ~ greater(X4,X3)
| ~ complexity(sk6,X4,sk15)
| ~ complexity(sk5,X3,sk15)
| ~ reorganization_type(sk6,X2,sk15)
| ~ reorganization_type(sk5,X2,sk15)
| ~ reorganization(sk6,sk15,sk17)
| ~ reorganization(sk5,sk15,X1)
| ~ class(sk6,X0,sk15)
| ~ class(sk5,X0,sk15) ),
inference(resolution,[status(thm)],[p214,c19]) ).
cnf(f20,negated_conjecture,
class(sk5,sk8,sk15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_46) ).
fof(f20_nnf,plain,
class(sk5,sk8,sk15),
inference(nnf_transformation,[status(thm)],[f20]) ).
cnf(c20,plain,
class(sk5,sk8,sk15),
inference(cnf_transformation,[status(esa)],[f20_nnf]) ).
cnf(p933,plain,
( greater(sk17,X0)
| ~ greater(X3,X2)
| ~ complexity(sk6,X3,sk15)
| ~ complexity(sk5,X2,sk15)
| ~ reorganization_type(sk6,X1,sk15)
| ~ reorganization_type(sk5,X1,sk15)
| ~ reorganization(sk6,sk15,sk17)
| ~ reorganization(sk5,sk15,X0)
| ~ class(sk6,sk8,sk15) ),
inference(resolution,[status(thm)],[p677,c20]) ).
cnf(f21,negated_conjecture,
class(sk6,sk8,sk15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_47) ).
fof(f21_nnf,plain,
class(sk6,sk8,sk15),
inference(nnf_transformation,[status(thm)],[f21]) ).
cnf(c21,plain,
class(sk6,sk8,sk15),
inference(cnf_transformation,[status(esa)],[f21_nnf]) ).
cnf(p934,plain,
( greater(sk17,X0)
| ~ greater(X3,X2)
| ~ complexity(sk6,X3,sk15)
| ~ complexity(sk5,X2,sk15)
| ~ reorganization_type(sk6,X1,sk15)
| ~ reorganization_type(sk5,X1,sk15)
| ~ reorganization(sk6,sk15,sk17)
| ~ reorganization(sk5,sk15,X0) ),
inference(resolution,[status(thm)],[p933,c21]) ).
cnf(f24,negated_conjecture,
reorganization(sk5,sk15,sk16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_50) ).
fof(f24_nnf,plain,
reorganization(sk5,sk15,sk16),
inference(nnf_transformation,[status(thm)],[f24]) ).
cnf(c24,plain,
reorganization(sk5,sk15,sk16),
inference(cnf_transformation,[status(esa)],[f24_nnf]) ).
cnf(p935,plain,
( greater(sk17,sk16)
| ~ greater(X2,X1)
| ~ complexity(sk6,X2,sk15)
| ~ complexity(sk5,X1,sk15)
| ~ reorganization_type(sk6,X0,sk15)
| ~ reorganization_type(sk5,X0,sk15)
| ~ reorganization(sk6,sk15,sk17) ),
inference(resolution,[status(thm)],[p934,c24]) ).
cnf(f25,negated_conjecture,
reorganization(sk6,sk15,sk17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_51) ).
fof(f25_nnf,plain,
reorganization(sk6,sk15,sk17),
inference(nnf_transformation,[status(thm)],[f25]) ).
cnf(c25,plain,
reorganization(sk6,sk15,sk17),
inference(cnf_transformation,[status(esa)],[f25_nnf]) ).
cnf(p936,plain,
( greater(sk17,sk16)
| ~ greater(X2,X1)
| ~ complexity(sk6,X2,sk15)
| ~ complexity(sk5,X1,sk15)
| ~ reorganization_type(sk6,X0,sk15)
| ~ reorganization_type(sk5,X0,sk15) ),
inference(resolution,[status(thm)],[p935,c25]) ).
cnf(f26,negated_conjecture,
reorganization_type(sk5,sk7,sk15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_52) ).
fof(f26_nnf,plain,
reorganization_type(sk5,sk7,sk15),
inference(nnf_transformation,[status(thm)],[f26]) ).
cnf(c26,plain,
reorganization_type(sk5,sk7,sk15),
inference(cnf_transformation,[status(esa)],[f26_nnf]) ).
cnf(p937,plain,
( greater(sk17,sk16)
| ~ greater(X1,X0)
| ~ complexity(sk6,X1,sk15)
| ~ complexity(sk5,X0,sk15)
| ~ reorganization_type(sk6,sk7,sk15) ),
inference(resolution,[status(thm)],[p936,c26]) ).
cnf(f27,negated_conjecture,
reorganization_type(sk6,sk7,sk15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_53) ).
fof(f27_nnf,plain,
reorganization_type(sk6,sk7,sk15),
inference(nnf_transformation,[status(thm)],[f27]) ).
cnf(c27,plain,
reorganization_type(sk6,sk7,sk15),
inference(cnf_transformation,[status(esa)],[f27_nnf]) ).
cnf(p938,plain,
( greater(sk17,sk16)
| ~ greater(X1,X0)
| ~ complexity(sk6,X1,sk15)
| ~ complexity(sk5,X0,sk15) ),
inference(resolution,[status(thm)],[p937,c27]) ).
cnf(f31,negated_conjecture,
complexity(sk5,sk12,sk15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_57) ).
fof(f31_nnf,plain,
complexity(sk5,sk12,sk15),
inference(nnf_transformation,[status(thm)],[f31]) ).
cnf(c31,plain,
complexity(sk5,sk12,sk15),
inference(cnf_transformation,[status(esa)],[f31_nnf]) ).
cnf(p939,plain,
( greater(sk17,sk16)
| ~ greater(X0,sk12)
| ~ complexity(sk6,X0,sk15) ),
inference(resolution,[status(thm)],[p938,c31]) ).
cnf(f32,negated_conjecture,
complexity(sk6,sk13,sk15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_58) ).
fof(f32_nnf,plain,
complexity(sk6,sk13,sk15),
inference(nnf_transformation,[status(thm)],[f32]) ).
cnf(c32,plain,
complexity(sk6,sk13,sk15),
inference(cnf_transformation,[status(esa)],[f32_nnf]) ).
cnf(p940,plain,
( greater(sk17,sk16)
| ~ greater(sk13,sk12) ),
inference(resolution,[status(thm)],[p939,c32]) ).
cnf(f33,negated_conjecture,
greater(sk13,sk12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_59) ).
fof(f33_nnf,plain,
greater(sk13,sk12),
inference(nnf_transformation,[status(thm)],[f33]) ).
cnf(c33,plain,
greater(sk13,sk12),
inference(cnf_transformation,[status(esa)],[f33_nnf]) ).
cnf(p941,plain,
greater(sk17,sk16),
inference(resolution,[status(thm)],[p940,c33]) ).
cnf(f5,axiom,
( organization(A,D)
| ~ greater(C,D)
| ~ greater(D,B)
| ~ organization(A,C)
| ~ organization(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp13_31) ).
fof(f5_nnf,plain,
! [A,B,C,D] :
( organization(A,D)
| ~ greater(C,D)
| ~ greater(D,B)
| ~ organization(A,C)
| ~ organization(A,B) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A,B,C,D] :
( organization(A,D)
| ~ greater(C,D)
| ~ greater(D,B)
| ~ organization(A,C)
| ~ organization(A,B) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( organization(X0,X3)
| ~ greater(X2,X3)
| ~ greater(X3,X1)
| ~ organization(X0,X2)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p49,plain,
( organization(sk5,X1)
| ~ greater(X0,X1)
| ~ greater(X1,sk15)
| ~ organization(sk5,X0) ),
inference(resolution,[status(thm)],[c5,c16]) ).
cnf(f18,negated_conjecture,
organization(sk5,sk17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_44) ).
fof(f18_nnf,plain,
organization(sk5,sk17),
inference(nnf_transformation,[status(thm)],[f18]) ).
cnf(c18,plain,
organization(sk5,sk17),
inference(cnf_transformation,[status(esa)],[f18_nnf]) ).
cnf(p81,plain,
( organization(sk5,X0)
| ~ greater(sk17,X0)
| ~ greater(X0,sk15) ),
inference(resolution,[status(thm)],[p49,c18]) ).
cnf(f6,axiom,
( greater(C,B)
| ~ reorganization(A,B,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp7_32) ).
fof(f6_nnf,plain,
! [A,B,C] :
( greater(C,B)
| ~ reorganization(A,B,C) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B,C] :
( greater(C,B)
| ~ reorganization(A,B,C) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( greater(X2,X1)
| ~ reorganization(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p53,plain,
greater(sk16,sk15),
inference(resolution,[status(thm)],[c6,c24]) ).
cnf(p82,plain,
( organization(sk5,sk16)
| ~ greater(sk17,sk16) ),
inference(resolution,[status(thm)],[p81,p53]) ).
cnf(p945,plain,
organization(sk5,sk16),
inference(resolution,[status(thm)],[p941,p82]) ).
cnf(f10,hypothesis,
( I = J
| greater(I,J)
| ~ greater(L,K)
| ~ complexity(C,L,B)
| ~ complexity(A,K,B)
| ~ survival_chance(C,J,D)
| ~ survival_chance(A,I,D)
| ~ reorganization_type(C,H,B)
| ~ reorganization_type(A,H,B)
| ~ reorganization(C,B,G)
| ~ 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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a11_FOL_36) ).
fof(f10_nnf,plain,
! [A,B,C,D,E,F,G,H,I,J,K,L] :
( I = J
| greater(I,J)
| ~ greater(L,K)
| ~ complexity(C,L,B)
| ~ complexity(A,K,B)
| ~ survival_chance(C,J,D)
| ~ survival_chance(A,I,D)
| ~ reorganization_type(C,H,B)
| ~ reorganization_type(A,H,B)
| ~ reorganization(C,B,G)
| ~ 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(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [A,B,C,D,E,F,G,H,I,J,K,L] :
( I = J
| greater(I,J)
| ~ greater(L,K)
| ~ complexity(C,L,B)
| ~ complexity(A,K,B)
| ~ survival_chance(C,J,D)
| ~ survival_chance(A,I,D)
| ~ reorganization_type(C,H,B)
| ~ reorganization_type(A,H,B)
| ~ reorganization(C,B,G)
| ~ 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(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( X8 = X9
| greater(X8,X9)
| ~ greater(X11,X10)
| ~ complexity(X2,X11,X1)
| ~ complexity(X0,X10,X1)
| ~ survival_chance(X2,X9,X3)
| ~ survival_chance(X0,X8,X3)
| ~ reorganization_type(X2,X7,X1)
| ~ reorganization_type(X0,X7,X1)
| ~ reorganization(X2,X1,X6)
| ~ reorganization(X0,X1,X3)
| ~ survival_chance(X2,X5,X1)
| ~ survival_chance(X0,X5,X1)
| ~ class(X2,X4,X1)
| ~ class(X0,X4,X1)
| ~ organization(X2,X3)
| ~ organization(X0,X3)
| ~ organization(X2,X1)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p94,plain,
( X6 = X7
| greater(X6,X7)
| ~ greater(X9,X8)
| ~ complexity(X0,X9,sk15)
| ~ complexity(sk5,X8,sk15)
| ~ survival_chance(X0,X7,X1)
| ~ survival_chance(sk5,X6,X1)
| ~ reorganization_type(X0,X5,sk15)
| ~ reorganization_type(sk5,X5,sk15)
| ~ reorganization(X0,sk15,X4)
| ~ reorganization(sk5,sk15,X1)
| ~ survival_chance(X0,X3,sk15)
| ~ survival_chance(sk5,X3,sk15)
| ~ class(X0,X2,sk15)
| ~ class(sk5,X2,sk15)
| ~ organization(X0,X1)
| ~ organization(sk5,X1)
| ~ organization(X0,sk15) ),
inference(resolution,[status(thm)],[c10,c16]) ).
cnf(p257,plain,
( X5 = X6
| greater(X5,X6)
| ~ greater(X8,X7)
| ~ complexity(sk6,X8,sk15)
| ~ complexity(sk5,X7,sk15)
| ~ survival_chance(sk6,X6,X0)
| ~ survival_chance(sk5,X5,X0)
| ~ reorganization_type(sk6,X4,sk15)
| ~ reorganization_type(sk5,X4,sk15)
| ~ reorganization(sk6,sk15,X3)
| ~ reorganization(sk5,sk15,X0)
| ~ survival_chance(sk6,X2,sk15)
| ~ survival_chance(sk5,X2,sk15)
| ~ class(sk6,X1,sk15)
| ~ class(sk5,X1,sk15)
| ~ organization(sk6,X0)
| ~ organization(sk5,X0) ),
inference(resolution,[status(thm)],[p94,c17]) ).
cnf(p994,plain,
( X4 = X5
| greater(X4,X5)
| ~ greater(X7,X6)
| ~ complexity(sk6,X7,sk15)
| ~ complexity(sk5,X6,sk15)
| ~ survival_chance(sk6,X5,sk16)
| ~ survival_chance(sk5,X4,sk16)
| ~ reorganization_type(sk6,X3,sk15)
| ~ reorganization_type(sk5,X3,sk15)
| ~ reorganization(sk6,sk15,X2)
| ~ reorganization(sk5,sk15,sk16)
| ~ survival_chance(sk6,X1,sk15)
| ~ survival_chance(sk5,X1,sk15)
| ~ class(sk6,X0,sk15)
| ~ class(sk5,X0,sk15)
| ~ organization(sk6,sk16) ),
inference(resolution,[status(thm)],[p945,p257]) ).
cnf(p50,plain,
( organization(sk6,X1)
| ~ greater(X0,X1)
| ~ greater(X1,sk15)
| ~ organization(sk6,X0) ),
inference(resolution,[status(thm)],[c5,c17]) ).
cnf(p83,plain,
( organization(sk6,X0)
| ~ greater(sk17,X0)
| ~ greater(X0,sk15) ),
inference(resolution,[status(thm)],[p50,c19]) ).
cnf(p98,plain,
( organization(sk6,sk16)
| ~ greater(sk17,sk16) ),
inference(resolution,[status(thm)],[p83,p53]) ).
cnf(p946,plain,
organization(sk6,sk16),
inference(resolution,[status(thm)],[p941,p98]) ).
cnf(p1931,plain,
( X4 = X5
| greater(X4,X5)
| ~ greater(X7,X6)
| ~ complexity(sk6,X7,sk15)
| ~ complexity(sk5,X6,sk15)
| ~ survival_chance(sk6,X5,sk16)
| ~ survival_chance(sk5,X4,sk16)
| ~ reorganization_type(sk6,X3,sk15)
| ~ reorganization_type(sk5,X3,sk15)
| ~ reorganization(sk6,sk15,X2)
| ~ reorganization(sk5,sk15,sk16)
| ~ survival_chance(sk6,X1,sk15)
| ~ survival_chance(sk5,X1,sk15)
| ~ class(sk6,X0,sk15)
| ~ class(sk5,X0,sk15) ),
inference(resolution,[status(thm)],[p994,p946]) ).
cnf(p2408,plain,
( X3 = X4
| greater(X3,X4)
| ~ greater(X6,X5)
| ~ complexity(sk6,X6,sk15)
| ~ complexity(sk5,X5,sk15)
| ~ survival_chance(sk6,X4,sk16)
| ~ survival_chance(sk5,X3,sk16)
| ~ reorganization_type(sk6,X2,sk15)
| ~ reorganization_type(sk5,X2,sk15)
| ~ reorganization(sk6,sk15,X1)
| ~ reorganization(sk5,sk15,sk16)
| ~ survival_chance(sk6,X0,sk15)
| ~ survival_chance(sk5,X0,sk15)
| ~ class(sk6,sk8,sk15) ),
inference(resolution,[status(thm)],[p1931,c20]) ).
cnf(p2409,plain,
( X3 = X4
| greater(X3,X4)
| ~ greater(X6,X5)
| ~ complexity(sk6,X6,sk15)
| ~ complexity(sk5,X5,sk15)
| ~ survival_chance(sk6,X4,sk16)
| ~ survival_chance(sk5,X3,sk16)
| ~ reorganization_type(sk6,X2,sk15)
| ~ reorganization_type(sk5,X2,sk15)
| ~ reorganization(sk6,sk15,X1)
| ~ reorganization(sk5,sk15,sk16)
| ~ survival_chance(sk6,X0,sk15)
| ~ survival_chance(sk5,X0,sk15) ),
inference(resolution,[status(thm)],[p2408,c21]) ).
cnf(f22,negated_conjecture,
survival_chance(sk5,sk9,sk15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_48) ).
fof(f22_nnf,plain,
survival_chance(sk5,sk9,sk15),
inference(nnf_transformation,[status(thm)],[f22]) ).
cnf(c22,plain,
survival_chance(sk5,sk9,sk15),
inference(cnf_transformation,[status(esa)],[f22_nnf]) ).
cnf(p2410,plain,
( X2 = X3
| greater(X2,X3)
| ~ greater(X5,X4)
| ~ complexity(sk6,X5,sk15)
| ~ complexity(sk5,X4,sk15)
| ~ survival_chance(sk6,X3,sk16)
| ~ survival_chance(sk5,X2,sk16)
| ~ reorganization_type(sk6,X1,sk15)
| ~ reorganization_type(sk5,X1,sk15)
| ~ reorganization(sk6,sk15,X0)
| ~ reorganization(sk5,sk15,sk16)
| ~ survival_chance(sk6,sk9,sk15) ),
inference(resolution,[status(thm)],[p2409,c22]) ).
cnf(f23,negated_conjecture,
survival_chance(sk6,sk9,sk15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_49) ).
fof(f23_nnf,plain,
survival_chance(sk6,sk9,sk15),
inference(nnf_transformation,[status(thm)],[f23]) ).
cnf(c23,plain,
survival_chance(sk6,sk9,sk15),
inference(cnf_transformation,[status(esa)],[f23_nnf]) ).
cnf(p2412,plain,
( X2 = X3
| greater(X2,X3)
| ~ greater(X5,X4)
| ~ complexity(sk6,X5,sk15)
| ~ complexity(sk5,X4,sk15)
| ~ survival_chance(sk6,X3,sk16)
| ~ survival_chance(sk5,X2,sk16)
| ~ reorganization_type(sk6,X1,sk15)
| ~ reorganization_type(sk5,X1,sk15)
| ~ reorganization(sk6,sk15,X0)
| ~ reorganization(sk5,sk15,sk16) ),
inference(resolution,[status(thm)],[p2410,c23]) ).
cnf(p2413,plain,
( X2 = X3
| greater(X2,X3)
| ~ greater(X5,X4)
| ~ complexity(sk6,X5,sk15)
| ~ complexity(sk5,X4,sk15)
| ~ survival_chance(sk6,X3,sk16)
| ~ survival_chance(sk5,X2,sk16)
| ~ reorganization_type(sk6,X1,sk15)
| ~ reorganization_type(sk5,X1,sk15)
| ~ reorganization(sk6,sk15,X0) ),
inference(resolution,[status(thm)],[p2412,c24]) ).
cnf(p2414,plain,
( X1 = X2
| greater(X1,X2)
| ~ greater(X4,X3)
| ~ complexity(sk6,X4,sk15)
| ~ complexity(sk5,X3,sk15)
| ~ survival_chance(sk6,X2,sk16)
| ~ survival_chance(sk5,X1,sk16)
| ~ reorganization_type(sk6,X0,sk15)
| ~ reorganization_type(sk5,X0,sk15) ),
inference(resolution,[status(thm)],[p2413,c25]) ).
cnf(p2415,plain,
( X0 = X1
| greater(X0,X1)
| ~ greater(X3,X2)
| ~ complexity(sk6,X3,sk15)
| ~ complexity(sk5,X2,sk15)
| ~ survival_chance(sk6,X1,sk16)
| ~ survival_chance(sk5,X0,sk16)
| ~ reorganization_type(sk6,sk7,sk15) ),
inference(resolution,[status(thm)],[p2414,c26]) ).
cnf(p2416,plain,
( X0 = X1
| greater(X0,X1)
| ~ greater(X3,X2)
| ~ complexity(sk6,X3,sk15)
| ~ complexity(sk5,X2,sk15)
| ~ survival_chance(sk6,X1,sk16)
| ~ survival_chance(sk5,X0,sk16) ),
inference(resolution,[status(thm)],[p2415,c27]) ).
cnf(f35,negated_conjecture,
sk14 = sk16,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_61) ).
fof(f35_nnf,plain,
sk14 = sk16,
inference(nnf_transformation,[status(thm)],[f35]) ).
cnf(c35,plain,
sk14 = sk16,
inference(cnf_transformation,[status(esa)],[f35_nnf]) ).
cnf(f29,negated_conjecture,
survival_chance(sk5,sk10,sk14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_55) ).
fof(f29_nnf,plain,
survival_chance(sk5,sk10,sk14),
inference(nnf_transformation,[status(thm)],[f29]) ).
cnf(c29,plain,
survival_chance(sk5,sk10,sk14),
inference(cnf_transformation,[status(esa)],[f29_nnf]) ).
cnf(p43,plain,
survival_chance(sk5,sk10,sk16),
inference(superposition,[status(thm)],[c35,c29]) ).
cnf(p2417,plain,
( sk10 = X0
| greater(sk10,X0)
| ~ greater(X2,X1)
| ~ complexity(sk6,X2,sk15)
| ~ complexity(sk5,X1,sk15)
| ~ survival_chance(sk6,X0,sk16) ),
inference(resolution,[status(thm)],[p2416,p43]) ).
cnf(f30,negated_conjecture,
survival_chance(sk6,sk11,sk14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_56) ).
fof(f30_nnf,plain,
survival_chance(sk6,sk11,sk14),
inference(nnf_transformation,[status(thm)],[f30]) ).
cnf(c30,plain,
survival_chance(sk6,sk11,sk14),
inference(cnf_transformation,[status(esa)],[f30_nnf]) ).
cnf(p48,plain,
survival_chance(sk6,sk11,sk16),
inference(superposition,[status(thm)],[c35,c30]) ).
cnf(p2419,plain,
( sk10 = sk11
| greater(sk10,sk11)
| ~ greater(X1,X0)
| ~ complexity(sk6,X1,sk15)
| ~ complexity(sk5,X0,sk15) ),
inference(resolution,[status(thm)],[p2417,p48]) ).
cnf(p2421,plain,
( sk10 = sk11
| greater(sk10,sk11)
| ~ greater(X0,sk12)
| ~ complexity(sk6,X0,sk15) ),
inference(resolution,[status(thm)],[p2419,c31]) ).
cnf(p2422,plain,
( sk10 = sk11
| greater(sk10,sk11)
| ~ greater(sk13,sk12) ),
inference(resolution,[status(thm)],[p2421,c32]) ).
cnf(p2423,plain,
( sk10 = sk11
| greater(sk10,sk11) ),
inference(resolution,[status(thm)],[p2422,c33]) ).
cnf(f36,negated_conjecture,
~ greater(sk10,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_62) ).
fof(f36_nnf,plain,
~ greater(sk10,sk11),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
~ greater(sk10,sk11),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
~ greater(sk10,sk11),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p2424,plain,
sk10 = sk11,
inference(resolution,[status(thm)],[p2423,c36]) ).
cnf(f37,negated_conjecture,
sk10 != sk11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_plus_FOL_63) ).
fof(f37_nnf,plain,
sk10 != sk11,
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
sk10 != sk11,
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
sk10 != sk11,
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p2425,plain,
$false,
inference(resolution,[status(thm)],[p2424,c37]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT005-2 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n013.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 00:56:20 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 11.24/2.07 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.24/2.07 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------