%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MGT004+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n009.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:14 PM UTC 2026
% Result : Theorem 4.72s 1.09s
% Output : Proof 4.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 5
% Syntax : Number of formulae : 65 ( 15 unt; 0 def)
% Number of atoms : 343 ( 0 equ)
% Maximal formula atoms : 12 ( 5 avg)
% Number of connectives : 463 ( 185 ~; 221 |; 51 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 201 ( 22 sgn 83 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,conjecture,
! [X,P1,P2,T1,T2,Ta,Tb] :
( ( ~ greater(T2,Tb)
& greater(T2,T1)
& ~ greater(Ta,T1)
& survival_chance(X,P2,T2)
& survival_chance(X,P1,T1)
& reorganization(X,Ta,Tb)
& organization(X,T2)
& organization(X,T1) )
=> greater(P1,P2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_FOL) ).
fof(f4_neg,negated_conjecture,
~ ! [X,P1,P2,T1,T2,Ta,Tb] :
( ( ~ greater(T2,Tb)
& greater(T2,T1)
& ~ greater(Ta,T1)
& survival_chance(X,P2,T2)
& survival_chance(X,P1,T1)
& reorganization(X,Ta,Tb)
& organization(X,T2)
& organization(X,T1) )
=> greater(P1,P2) ),
inference(negated_conjecture,[status(cth)],[f4]) ).
fof(f4_nnf,plain,
? [X,P1,P2,T1,T2,Ta,Tb] :
( ~ greater(P1,P2)
& ~ greater(T2,Tb)
& greater(T2,T1)
& ~ greater(Ta,T1)
& survival_chance(X,P2,T2)
& survival_chance(X,P1,T1)
& reorganization(X,Ta,Tb)
& organization(X,T2)
& organization(X,T1) ),
inference(nnf_transformation,[status(thm)],[f4_neg]) ).
fof(f4_sk,plain,
( ~ greater(sk3,sk4)
& ~ greater(sk6,sk8)
& greater(sk6,sk5)
& ~ greater(sk7,sk5)
& survival_chance(sk2,sk4,sk6)
& survival_chance(sk2,sk3,sk5)
& reorganization(sk2,sk7,sk8)
& organization(sk2,sk6)
& organization(sk2,sk5) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2,sk3,sk4,sk5,sk6,sk7,sk8])],[f4_nnf]) ).
cnf(c6,plain,
organization(sk2,sk6),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
fof(f2,hypothesis,
! [X,Y,R1,R2,A1,A2,P1,P2,T1,T2] :
( ( greater(A2,A1)
& greater(R2,R1)
& survival_chance(Y,P2,T2)
& survival_chance(X,P1,T1)
& accountability(Y,A2,T2)
& accountability(X,A1,T1)
& reliability(Y,R2,T2)
& reliability(X,R1,T1)
& organization(Y,T2)
& organization(X,T1) )
=> greater(P2,P1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1_FOL) ).
fof(f2_nnf,plain,
! [X,Y,R1,R2,A1,A2,P1,P2,T1,T2] :
( greater(P2,P1)
| ~ greater(A2,A1)
| ~ greater(R2,R1)
| ~ survival_chance(Y,P2,T2)
| ~ survival_chance(X,P1,T1)
| ~ accountability(Y,A2,T2)
| ~ accountability(X,A1,T1)
| ~ reliability(Y,R2,T2)
| ~ reliability(X,R1,T1)
| ~ organization(Y,T2)
| ~ organization(X,T1) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,T1,Y,T2,R1,R2,A1,A2,P1,P2] :
( greater(P2,P1)
| ~ greater(A2,A1)
| ~ greater(R2,R1)
| ~ survival_chance(Y,P2,T2)
| ~ survival_chance(X,P1,T1)
| ~ accountability(Y,A2,T2)
| ~ accountability(X,A1,T1)
| ~ reliability(Y,R2,T2)
| ~ reliability(X,R1,T1)
| ~ organization(Y,T2)
| ~ organization(X,T1) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( greater(X7,X6)
| ~ greater(X5,X4)
| ~ greater(X3,X2)
| ~ survival_chance(X1,X7,X9)
| ~ survival_chance(X0,X6,X8)
| ~ accountability(X1,X5,X9)
| ~ accountability(X0,X4,X8)
| ~ reliability(X1,X3,X9)
| ~ reliability(X0,X2,X8)
| ~ organization(X1,X9)
| ~ organization(X0,X8) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p36,plain,
( greater(X7,X6)
| ~ greater(X5,X4)
| ~ greater(X3,X2)
| ~ survival_chance(X0,X7,X1)
| ~ survival_chance(sk2,X6,sk6)
| ~ accountability(X0,X5,X1)
| ~ accountability(sk2,X4,sk6)
| ~ reliability(X0,X3,X1)
| ~ reliability(sk2,X2,sk6)
| ~ organization(X0,X1) ),
inference(resolution,[status(thm)],[c6,c2]) ).
cnf(c5,plain,
organization(sk2,sk5),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p75,plain,
( greater(X5,X4)
| ~ greater(X3,X2)
| ~ greater(X1,X0)
| ~ survival_chance(sk2,X5,sk5)
| ~ survival_chance(sk2,X4,sk6)
| ~ accountability(sk2,X3,sk5)
| ~ accountability(sk2,X2,sk6)
| ~ reliability(sk2,X1,sk5)
| ~ reliability(sk2,X0,sk6) ),
inference(resolution,[status(thm)],[p36,c5]) ).
fof(f0,axiom,
! [X,T] :
( organization(X,T)
=> ? [R] : reliability(X,R,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp1) ).
fof(f0_nnf,plain,
! [X,T] :
( ? [R] : reliability(X,R,T)
| ~ organization(X,T) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,T] :
( reliability(X,sk0(X,T),T)
| ~ organization(X,T) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f0_nnf]) ).
cnf(c0,plain,
( reliability(X0,sk0(X0,X1),X1)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p34,plain,
reliability(sk2,sk0(sk2,sk6),sk6),
inference(resolution,[status(thm)],[c6,c0]) ).
cnf(p127,plain,
( greater(X4,X3)
| ~ greater(X2,X1)
| ~ greater(X0,sk0(sk2,sk6))
| ~ survival_chance(sk2,X4,sk5)
| ~ survival_chance(sk2,X3,sk6)
| ~ accountability(sk2,X2,sk5)
| ~ accountability(sk2,X1,sk6)
| ~ reliability(sk2,X0,sk5) ),
inference(resolution,[status(thm)],[p75,p34]) ).
cnf(p29,plain,
reliability(sk2,sk0(sk2,sk5),sk5),
inference(resolution,[status(thm)],[c5,c0]) ).
cnf(p183,plain,
( greater(X3,X2)
| ~ greater(X1,X0)
| ~ greater(sk0(sk2,sk5),sk0(sk2,sk6))
| ~ survival_chance(sk2,X3,sk5)
| ~ survival_chance(sk2,X2,sk6)
| ~ accountability(sk2,X1,sk5)
| ~ accountability(sk2,X0,sk6) ),
inference(resolution,[status(thm)],[p127,p29]) ).
fof(f1,axiom,
! [X,T] :
( organization(X,T)
=> ? [A] : accountability(X,A,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp2) ).
fof(f1_nnf,plain,
! [X,T] :
( ? [A] : accountability(X,A,T)
| ~ organization(X,T) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,T] :
( accountability(X,sk1(X,T),T)
| ~ organization(X,T) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1])],[f1_nnf]) ).
cnf(c1,plain,
( accountability(X0,sk1(X0,X1),X1)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p35,plain,
accountability(sk2,sk1(sk2,sk6),sk6),
inference(resolution,[status(thm)],[c6,c1]) ).
cnf(p232,plain,
( greater(X2,X1)
| ~ greater(X0,sk1(sk2,sk6))
| ~ greater(sk0(sk2,sk5),sk0(sk2,sk6))
| ~ survival_chance(sk2,X2,sk5)
| ~ survival_chance(sk2,X1,sk6)
| ~ accountability(sk2,X0,sk5) ),
inference(resolution,[status(thm)],[p183,p35]) ).
cnf(p30,plain,
accountability(sk2,sk1(sk2,sk5),sk5),
inference(resolution,[status(thm)],[c5,c1]) ).
cnf(p264,plain,
( greater(X1,X0)
| ~ greater(sk1(sk2,sk5),sk1(sk2,sk6))
| ~ greater(sk0(sk2,sk5),sk0(sk2,sk6))
| ~ survival_chance(sk2,X1,sk5)
| ~ survival_chance(sk2,X0,sk6) ),
inference(resolution,[status(thm)],[p232,p30]) ).
cnf(c9,plain,
survival_chance(sk2,sk4,sk6),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p280,plain,
( greater(X0,sk4)
| ~ greater(sk1(sk2,sk5),sk1(sk2,sk6))
| ~ greater(sk0(sk2,sk5),sk0(sk2,sk6))
| ~ survival_chance(sk2,X0,sk5) ),
inference(resolution,[status(thm)],[p264,c9]) ).
cnf(c8,plain,
survival_chance(sk2,sk3,sk5),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p288,plain,
( greater(sk3,sk4)
| ~ greater(sk1(sk2,sk5),sk1(sk2,sk6))
| ~ greater(sk0(sk2,sk5),sk0(sk2,sk6)) ),
inference(resolution,[status(thm)],[p280,c8]) ).
fof(f3,hypothesis,
! [X,R1,R2,A1,A2,T1,T2,Ta,Tb] :
( ( ~ greater(T2,Tb)
& greater(T2,T1)
& ~ greater(Ta,T1)
& accountability(X,A2,T2)
& accountability(X,A1,T1)
& reliability(X,R2,T2)
& reliability(X,R1,T1)
& reorganization(X,Ta,Tb)
& organization(X,T2)
& organization(X,T1) )
=> ( greater(A1,A2)
& greater(R1,R2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a6_FOL) ).
fof(f3_nnf,plain,
! [X,R1,R2,A1,A2,T1,T2,Ta,Tb] :
( ( greater(A1,A2)
& greater(R1,R2) )
| greater(T2,Tb)
| ~ greater(T2,T1)
| greater(Ta,T1)
| ~ accountability(X,A2,T2)
| ~ accountability(X,A1,T1)
| ~ reliability(X,R2,T2)
| ~ reliability(X,R1,T1)
| ~ reorganization(X,Ta,Tb)
| ~ organization(X,T2)
| ~ organization(X,T1) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,T1,T2,Ta,Tb,R1,R2,A1,A2] :
( ( greater(A1,A2)
& greater(R1,R2) )
| greater(T2,Tb)
| ~ greater(T2,T1)
| greater(Ta,T1)
| ~ accountability(X,A2,T2)
| ~ accountability(X,A1,T1)
| ~ reliability(X,R2,T2)
| ~ reliability(X,R1,T1)
| ~ reorganization(X,Ta,Tb)
| ~ organization(X,T2)
| ~ organization(X,T1) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( greater(X1,X2)
| greater(X6,X8)
| ~ greater(X6,X5)
| greater(X7,X5)
| ~ accountability(X0,X4,X6)
| ~ accountability(X0,X3,X5)
| ~ reliability(X0,X2,X6)
| ~ reliability(X0,X1,X5)
| ~ reorganization(X0,X7,X8)
| ~ organization(X0,X6)
| ~ organization(X0,X5) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p32,plain,
( greater(X3,X4)
| greater(X0,X2)
| ~ greater(X0,sk5)
| greater(X1,sk5)
| ~ accountability(sk2,X6,X0)
| ~ accountability(sk2,X5,sk5)
| ~ reliability(sk2,X4,X0)
| ~ reliability(sk2,X3,sk5)
| ~ reorganization(sk2,X1,X2)
| ~ organization(sk2,X0) ),
inference(resolution,[status(thm)],[c5,c3]) ).
cnf(p72,plain,
( greater(X2,X3)
| greater(sk6,X1)
| ~ greater(sk6,sk5)
| greater(X0,sk5)
| ~ accountability(sk2,X5,sk6)
| ~ accountability(sk2,X4,sk5)
| ~ reliability(sk2,X3,sk6)
| ~ reliability(sk2,X2,sk5)
| ~ reorganization(sk2,X0,X1) ),
inference(resolution,[status(thm)],[p32,c6]) ).
cnf(c7,plain,
reorganization(sk2,sk7,sk8),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p125,plain,
( greater(X0,X1)
| greater(sk6,sk8)
| ~ greater(sk6,sk5)
| greater(sk7,sk5)
| ~ accountability(sk2,X3,sk6)
| ~ accountability(sk2,X2,sk5)
| ~ reliability(sk2,X1,sk6)
| ~ reliability(sk2,X0,sk5) ),
inference(resolution,[status(thm)],[p72,c7]) ).
cnf(p181,plain,
( greater(sk0(sk2,sk5),X0)
| greater(sk6,sk8)
| ~ greater(sk6,sk5)
| greater(sk7,sk5)
| ~ accountability(sk2,X2,sk6)
| ~ accountability(sk2,X1,sk5)
| ~ reliability(sk2,X0,sk6) ),
inference(resolution,[status(thm)],[p125,p29]) ).
cnf(p230,plain,
( greater(sk0(sk2,sk5),sk0(sk2,sk6))
| greater(sk6,sk8)
| ~ greater(sk6,sk5)
| greater(sk7,sk5)
| ~ accountability(sk2,X1,sk6)
| ~ accountability(sk2,X0,sk5) ),
inference(resolution,[status(thm)],[p181,p34]) ).
cnf(p262,plain,
( greater(sk0(sk2,sk5),sk0(sk2,sk6))
| greater(sk6,sk8)
| ~ greater(sk6,sk5)
| greater(sk7,sk5)
| ~ accountability(sk2,X0,sk6) ),
inference(resolution,[status(thm)],[p230,p30]) ).
cnf(p278,plain,
( greater(sk0(sk2,sk5),sk0(sk2,sk6))
| greater(sk6,sk8)
| ~ greater(sk6,sk5)
| greater(sk7,sk5) ),
inference(resolution,[status(thm)],[p262,p35]) ).
cnf(c11,plain,
greater(sk6,sk5),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p286,plain,
( greater(sk0(sk2,sk5),sk0(sk2,sk6))
| greater(sk6,sk8)
| greater(sk7,sk5) ),
inference(resolution,[status(thm)],[p278,c11]) ).
cnf(p289,plain,
( greater(sk6,sk8)
| greater(sk7,sk5)
| greater(sk3,sk4)
| ~ greater(sk1(sk2,sk5),sk1(sk2,sk6)) ),
inference(resolution,[status(thm)],[p288,p286]) ).
cnf(c4,plain,
( greater(X3,X4)
| greater(X6,X8)
| ~ greater(X6,X5)
| greater(X7,X5)
| ~ accountability(X0,X4,X6)
| ~ accountability(X0,X3,X5)
| ~ reliability(X0,X2,X6)
| ~ reliability(X0,X1,X5)
| ~ reorganization(X0,X7,X8)
| ~ organization(X0,X6)
| ~ organization(X0,X5) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p33,plain,
( greater(X5,X6)
| greater(X0,X2)
| ~ greater(X0,sk5)
| greater(X1,sk5)
| ~ accountability(sk2,X6,X0)
| ~ accountability(sk2,X5,sk5)
| ~ reliability(sk2,X4,X0)
| ~ reliability(sk2,X3,sk5)
| ~ reorganization(sk2,X1,X2)
| ~ organization(sk2,X0) ),
inference(resolution,[status(thm)],[c5,c4]) ).
cnf(p74,plain,
( greater(X4,X5)
| greater(sk6,X1)
| ~ greater(sk6,sk5)
| greater(X0,sk5)
| ~ accountability(sk2,X5,sk6)
| ~ accountability(sk2,X4,sk5)
| ~ reliability(sk2,X3,sk6)
| ~ reliability(sk2,X2,sk5)
| ~ reorganization(sk2,X0,X1) ),
inference(resolution,[status(thm)],[p33,c6]) ).
cnf(p126,plain,
( greater(X2,X3)
| greater(sk6,sk8)
| ~ greater(sk6,sk5)
| greater(sk7,sk5)
| ~ accountability(sk2,X3,sk6)
| ~ accountability(sk2,X2,sk5)
| ~ reliability(sk2,X1,sk6)
| ~ reliability(sk2,X0,sk5) ),
inference(resolution,[status(thm)],[p74,c7]) ).
cnf(p182,plain,
( greater(X1,X2)
| greater(sk6,sk8)
| ~ greater(sk6,sk5)
| greater(sk7,sk5)
| ~ accountability(sk2,X2,sk6)
| ~ accountability(sk2,X1,sk5)
| ~ reliability(sk2,X0,sk6) ),
inference(resolution,[status(thm)],[p126,p29]) ).
cnf(p231,plain,
( greater(X0,X1)
| greater(sk6,sk8)
| ~ greater(sk6,sk5)
| greater(sk7,sk5)
| ~ accountability(sk2,X1,sk6)
| ~ accountability(sk2,X0,sk5) ),
inference(resolution,[status(thm)],[p182,p34]) ).
cnf(p263,plain,
( greater(sk1(sk2,sk5),X0)
| greater(sk6,sk8)
| ~ greater(sk6,sk5)
| greater(sk7,sk5)
| ~ accountability(sk2,X0,sk6) ),
inference(resolution,[status(thm)],[p231,p30]) ).
cnf(p279,plain,
( greater(sk1(sk2,sk5),sk1(sk2,sk6))
| greater(sk6,sk8)
| ~ greater(sk6,sk5)
| greater(sk7,sk5) ),
inference(resolution,[status(thm)],[p263,p35]) ).
cnf(p287,plain,
( greater(sk1(sk2,sk5),sk1(sk2,sk6))
| greater(sk6,sk8)
| greater(sk7,sk5) ),
inference(resolution,[status(thm)],[p279,c11]) ).
cnf(p290,plain,
( greater(sk6,sk8)
| greater(sk7,sk5)
| greater(sk6,sk8)
| greater(sk7,sk5)
| greater(sk3,sk4) ),
inference(resolution,[status(thm)],[p289,p287]) ).
cnf(p291,plain,
( greater(sk6,sk8)
| greater(sk6,sk8)
| greater(sk7,sk5)
| greater(sk3,sk4) ),
inference(factoring,[status(thm)],[p290]) ).
cnf(p293,plain,
( greater(sk6,sk8)
| greater(sk7,sk5)
| greater(sk3,sk4) ),
inference(factoring,[status(thm)],[p291]) ).
cnf(c10,plain,
~ greater(sk7,sk5),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p294,plain,
( greater(sk6,sk8)
| greater(sk3,sk4) ),
inference(resolution,[status(thm)],[p293,c10]) ).
cnf(c12,plain,
~ greater(sk6,sk8),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p295,plain,
greater(sk3,sk4),
inference(resolution,[status(thm)],[p294,c12]) ).
cnf(c13,plain,
~ greater(sk3,sk4),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p296,plain,
$false,
inference(resolution,[status(thm)],[p295,c13]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT004+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n009.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 00:55:59 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 4.72/1.09 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.72/1.09 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------