%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MGT016+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 : n018.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:18 PM UTC 2026
% Result : Theorem 3.24s 0.86s
% Output : Proof 3.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 4
% Syntax : Number of formulae : 53 ( 18 unt; 0 def)
% Number of atoms : 291 ( 0 equ)
% Maximal formula atoms : 13 ( 5 avg)
% Number of connectives : 402 ( 164 ~; 168 |; 65 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 9 con; 0-2 aty)
% Number of variables : 170 ( 0 sgn 78 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,hypothesis,
! [X,Y,Rt,C,I1,I2,Ta,Tb,Tc] :
( ( greater(I2,I1)
& inertia(Y,I2,Ta)
& inertia(X,I1,Ta)
& reorganization_type(Y,Rt,Ta)
& reorganization_type(X,Rt,Ta)
& reorganization(Y,Ta,Tc)
& reorganization(X,Ta,Tb)
& class(Y,C,Ta)
& class(X,C,Ta)
& ~ organization(Y,Tc)
& organization(Y,Ta)
& organization(X,Ta) )
=> greater(Tb,Tc) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a14_FOL) ).
fof(f2_nnf,plain,
! [X,Y,Rt,C,I1,I2,Ta,Tb,Tc] :
( greater(Tb,Tc)
| ~ greater(I2,I1)
| ~ inertia(Y,I2,Ta)
| ~ inertia(X,I1,Ta)
| ~ reorganization_type(Y,Rt,Ta)
| ~ reorganization_type(X,Rt,Ta)
| ~ reorganization(Y,Ta,Tc)
| ~ reorganization(X,Ta,Tb)
| ~ class(Y,C,Ta)
| ~ class(X,C,Ta)
| organization(Y,Tc)
| ~ organization(Y,Ta)
| ~ organization(X,Ta) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Ta,Y,Tc,C,Tb,Rt,I1,I2] :
( greater(Tb,Tc)
| ~ greater(I2,I1)
| ~ inertia(Y,I2,Ta)
| ~ inertia(X,I1,Ta)
| ~ reorganization_type(Y,Rt,Ta)
| ~ reorganization_type(X,Rt,Ta)
| ~ reorganization(Y,Ta,Tc)
| ~ reorganization(X,Ta,Tb)
| ~ class(Y,C,Ta)
| ~ class(X,C,Ta)
| organization(Y,Tc)
| ~ organization(Y,Ta)
| ~ organization(X,Ta) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( greater(X7,X8)
| ~ greater(X5,X4)
| ~ inertia(X1,X5,X6)
| ~ inertia(X0,X4,X6)
| ~ reorganization_type(X1,X2,X6)
| ~ reorganization_type(X0,X2,X6)
| ~ reorganization(X1,X6,X8)
| ~ reorganization(X0,X6,X7)
| ~ class(X1,X3,X6)
| ~ class(X0,X3,X6)
| organization(X1,X8)
| ~ organization(X1,X6)
| ~ organization(X0,X6) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
fof(f3,conjecture,
! [X,Y,Rt,C,C1,C2,Ta,Tb,Tc] :
( ( greater(C2,C1)
& complexity(Y,C2,Ta)
& complexity(X,C1,Ta)
& reorganization_type(Y,Rt,Ta)
& reorganization_type(X,Rt,Ta)
& reorganization(Y,Ta,Tc)
& reorganization(X,Ta,Tb)
& class(Y,C,Ta)
& class(X,C,Ta)
& ~ organization(Y,Tc)
& organization(Y,Ta)
& organization(X,Ta) )
=> greater(Tb,Tc) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t16_FOL) ).
fof(f3_neg,negated_conjecture,
~ ! [X,Y,Rt,C,C1,C2,Ta,Tb,Tc] :
( ( greater(C2,C1)
& complexity(Y,C2,Ta)
& complexity(X,C1,Ta)
& reorganization_type(Y,Rt,Ta)
& reorganization_type(X,Rt,Ta)
& reorganization(Y,Ta,Tc)
& reorganization(X,Ta,Tb)
& class(Y,C,Ta)
& class(X,C,Ta)
& ~ organization(Y,Tc)
& organization(Y,Ta)
& organization(X,Ta) )
=> greater(Tb,Tc) ),
inference(negated_conjecture,[status(cth)],[f3]) ).
fof(f3_nnf,plain,
? [X,Y,Rt,C,C1,C2,Ta,Tb,Tc] :
( ~ greater(Tb,Tc)
& greater(C2,C1)
& complexity(Y,C2,Ta)
& complexity(X,C1,Ta)
& reorganization_type(Y,Rt,Ta)
& reorganization_type(X,Rt,Ta)
& reorganization(Y,Ta,Tc)
& reorganization(X,Ta,Tb)
& class(Y,C,Ta)
& class(X,C,Ta)
& ~ organization(Y,Tc)
& organization(Y,Ta)
& organization(X,Ta) ),
inference(nnf_transformation,[status(thm)],[f3_neg]) ).
fof(f3_sk,plain,
( ~ greater(sk8,sk9)
& greater(sk6,sk5)
& complexity(sk2,sk6,sk7)
& complexity(sk1,sk5,sk7)
& reorganization_type(sk2,sk3,sk7)
& reorganization_type(sk1,sk3,sk7)
& reorganization(sk2,sk7,sk9)
& reorganization(sk1,sk7,sk8)
& class(sk2,sk4,sk7)
& class(sk1,sk4,sk7)
& ~ organization(sk2,sk9)
& organization(sk2,sk7)
& organization(sk1,sk7) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1,sk2,sk3,sk4,sk5,sk6,sk7,sk8,sk9])],[f3_nnf]) ).
cnf(c3,plain,
organization(sk1,sk7),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p29,plain,
( greater(X3,X1)
| ~ greater(X6,X5)
| ~ inertia(X0,X6,sk7)
| ~ inertia(sk1,X5,sk7)
| ~ reorganization_type(X0,X4,sk7)
| ~ reorganization_type(sk1,X4,sk7)
| ~ reorganization(X0,sk7,X1)
| ~ reorganization(sk1,sk7,X3)
| ~ class(X0,X2,sk7)
| ~ class(sk1,X2,sk7)
| organization(X0,X1)
| ~ organization(X0,sk7) ),
inference(resolution,[status(thm)],[c2,c3]) ).
cnf(c4,plain,
organization(sk2,sk7),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p59,plain,
( greater(X2,X0)
| ~ greater(X5,X4)
| ~ inertia(sk2,X5,sk7)
| ~ inertia(sk1,X4,sk7)
| ~ reorganization_type(sk2,X3,sk7)
| ~ reorganization_type(sk1,X3,sk7)
| ~ reorganization(sk2,sk7,X0)
| ~ reorganization(sk1,sk7,X2)
| ~ class(sk2,X1,sk7)
| ~ class(sk1,X1,sk7)
| organization(sk2,X0) ),
inference(resolution,[status(thm)],[p29,c4]) ).
cnf(c6,plain,
class(sk1,sk4,sk7),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p96,plain,
( greater(X1,X0)
| ~ greater(X4,X3)
| ~ inertia(sk2,X4,sk7)
| ~ inertia(sk1,X3,sk7)
| ~ reorganization_type(sk2,X2,sk7)
| ~ reorganization_type(sk1,X2,sk7)
| ~ reorganization(sk2,sk7,X0)
| ~ reorganization(sk1,sk7,X1)
| ~ class(sk2,sk4,sk7)
| organization(sk2,X0) ),
inference(resolution,[status(thm)],[p59,c6]) ).
cnf(c7,plain,
class(sk2,sk4,sk7),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p127,plain,
( greater(X1,X0)
| ~ greater(X4,X3)
| ~ inertia(sk2,X4,sk7)
| ~ inertia(sk1,X3,sk7)
| ~ reorganization_type(sk2,X2,sk7)
| ~ reorganization_type(sk1,X2,sk7)
| ~ reorganization(sk2,sk7,X0)
| ~ reorganization(sk1,sk7,X1)
| organization(sk2,X0) ),
inference(resolution,[status(thm)],[p96,c7]) ).
cnf(c8,plain,
reorganization(sk1,sk7,sk8),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p148,plain,
( greater(sk8,X0)
| ~ greater(X3,X2)
| ~ inertia(sk2,X3,sk7)
| ~ inertia(sk1,X2,sk7)
| ~ reorganization_type(sk2,X1,sk7)
| ~ reorganization_type(sk1,X1,sk7)
| ~ reorganization(sk2,sk7,X0)
| organization(sk2,X0) ),
inference(resolution,[status(thm)],[p127,c8]) ).
cnf(c9,plain,
reorganization(sk2,sk7,sk9),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p149,plain,
( greater(sk8,sk9)
| ~ greater(X2,X1)
| ~ inertia(sk2,X2,sk7)
| ~ inertia(sk1,X1,sk7)
| ~ reorganization_type(sk2,X0,sk7)
| ~ reorganization_type(sk1,X0,sk7)
| organization(sk2,sk9) ),
inference(resolution,[status(thm)],[p148,c9]) ).
cnf(c10,plain,
reorganization_type(sk1,sk3,sk7),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p150,plain,
( greater(sk8,sk9)
| ~ greater(X1,X0)
| ~ inertia(sk2,X1,sk7)
| ~ inertia(sk1,X0,sk7)
| ~ reorganization_type(sk2,sk3,sk7)
| organization(sk2,sk9) ),
inference(resolution,[status(thm)],[p149,c10]) ).
cnf(c11,plain,
reorganization_type(sk2,sk3,sk7),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p151,plain,
( greater(sk8,sk9)
| ~ greater(X1,X0)
| ~ inertia(sk2,X1,sk7)
| ~ inertia(sk1,X0,sk7)
| organization(sk2,sk9) ),
inference(resolution,[status(thm)],[p150,c11]) ).
fof(f0,axiom,
! [X,T] :
( organization(X,T)
=> ? [I] : inertia(X,I,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp5) ).
fof(f0_nnf,plain,
! [X,T] :
( ? [I] : inertia(X,I,T)
| ~ organization(X,T) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,T] :
( inertia(X,sk0(X,T),T)
| ~ organization(X,T) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f0_nnf]) ).
cnf(c0,plain,
( inertia(X0,sk0(X0,X1),X1)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p16,plain,
inertia(sk1,sk0(sk1,sk7),sk7),
inference(resolution,[status(thm)],[c0,c3]) ).
cnf(p152,plain,
( greater(sk8,sk9)
| ~ greater(X0,sk0(sk1,sk7))
| ~ inertia(sk2,X0,sk7)
| organization(sk2,sk9) ),
inference(resolution,[status(thm)],[p151,p16]) ).
cnf(p17,plain,
inertia(sk2,sk0(sk2,sk7),sk7),
inference(resolution,[status(thm)],[c0,c4]) ).
cnf(p154,plain,
( greater(sk8,sk9)
| ~ greater(sk0(sk2,sk7),sk0(sk1,sk7))
| organization(sk2,sk9) ),
inference(resolution,[status(thm)],[p152,p17]) ).
fof(f1,hypothesis,
! [X,Y,C,C1,C2,I1,I2,T1,T2] :
( ( greater(C2,C1)
& inertia(Y,I2,T2)
& inertia(X,I1,T1)
& complexity(Y,C2,T2)
& complexity(X,C1,T1)
& class(Y,C,T2)
& class(X,C,T1)
& organization(Y,T2)
& organization(X,T1) )
=> greater(I2,I1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a12_FOL) ).
fof(f1_nnf,plain,
! [X,Y,C,C1,C2,I1,I2,T1,T2] :
( greater(I2,I1)
| ~ greater(C2,C1)
| ~ inertia(Y,I2,T2)
| ~ inertia(X,I1,T1)
| ~ complexity(Y,C2,T2)
| ~ complexity(X,C1,T1)
| ~ class(Y,C,T2)
| ~ class(X,C,T1)
| ~ organization(Y,T2)
| ~ organization(X,T1) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,T1,Y,T2,C,C1,C2,I1,I2] :
( greater(I2,I1)
| ~ greater(C2,C1)
| ~ inertia(Y,I2,T2)
| ~ inertia(X,I1,T1)
| ~ complexity(Y,C2,T2)
| ~ complexity(X,C1,T1)
| ~ class(Y,C,T2)
| ~ class(X,C,T1)
| ~ organization(Y,T2)
| ~ organization(X,T1) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( greater(X6,X5)
| ~ greater(X4,X3)
| ~ inertia(X1,X6,X8)
| ~ inertia(X0,X5,X7)
| ~ complexity(X1,X4,X8)
| ~ complexity(X0,X3,X7)
| ~ class(X1,X2,X8)
| ~ class(X0,X2,X7)
| ~ organization(X1,X8)
| ~ organization(X0,X7) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p22,plain,
( greater(X6,X5)
| ~ greater(X4,X3)
| ~ inertia(X0,X6,X1)
| ~ inertia(sk1,X5,sk7)
| ~ complexity(X0,X4,X1)
| ~ complexity(sk1,X3,sk7)
| ~ class(X0,X2,X1)
| ~ class(sk1,X2,sk7)
| ~ organization(X0,X1) ),
inference(resolution,[status(thm)],[c1,c3]) ).
cnf(p37,plain,
( greater(X4,X3)
| ~ greater(X2,X1)
| ~ inertia(sk2,X4,sk7)
| ~ inertia(sk1,X3,sk7)
| ~ complexity(sk2,X2,sk7)
| ~ complexity(sk1,X1,sk7)
| ~ class(sk2,X0,sk7)
| ~ class(sk1,X0,sk7) ),
inference(resolution,[status(thm)],[p22,c4]) ).
cnf(p75,plain,
( greater(X3,X2)
| ~ greater(X1,X0)
| ~ inertia(sk2,X3,sk7)
| ~ inertia(sk1,X2,sk7)
| ~ complexity(sk2,X1,sk7)
| ~ complexity(sk1,X0,sk7)
| ~ class(sk2,sk4,sk7) ),
inference(resolution,[status(thm)],[p37,c6]) ).
cnf(p86,plain,
( greater(X3,X2)
| ~ greater(X1,X0)
| ~ inertia(sk2,X3,sk7)
| ~ inertia(sk1,X2,sk7)
| ~ complexity(sk2,X1,sk7)
| ~ complexity(sk1,X0,sk7) ),
inference(resolution,[status(thm)],[p75,c7]) ).
cnf(c12,plain,
complexity(sk1,sk5,sk7),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p87,plain,
( greater(X2,X1)
| ~ greater(X0,sk5)
| ~ inertia(sk2,X2,sk7)
| ~ inertia(sk1,X1,sk7)
| ~ complexity(sk2,X0,sk7) ),
inference(resolution,[status(thm)],[p86,c12]) ).
cnf(c13,plain,
complexity(sk2,sk6,sk7),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p88,plain,
( greater(X1,X0)
| ~ greater(sk6,sk5)
| ~ inertia(sk2,X1,sk7)
| ~ inertia(sk1,X0,sk7) ),
inference(resolution,[status(thm)],[p87,c13]) ).
cnf(p93,plain,
( greater(X0,sk0(sk1,sk7))
| ~ greater(sk6,sk5)
| ~ inertia(sk2,X0,sk7) ),
inference(resolution,[status(thm)],[p88,p16]) ).
cnf(p94,plain,
( greater(sk0(sk2,sk7),sk0(sk1,sk7))
| ~ greater(sk6,sk5) ),
inference(resolution,[status(thm)],[p93,p17]) ).
cnf(c14,plain,
greater(sk6,sk5),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p95,plain,
greater(sk0(sk2,sk7),sk0(sk1,sk7)),
inference(resolution,[status(thm)],[p94,c14]) ).
cnf(p155,plain,
( greater(sk8,sk9)
| organization(sk2,sk9) ),
inference(resolution,[status(thm)],[p154,p95]) ).
cnf(c15,plain,
~ greater(sk8,sk9),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p156,plain,
organization(sk2,sk9),
inference(resolution,[status(thm)],[p155,c15]) ).
cnf(c5,plain,
~ organization(sk2,sk9),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p157,plain,
$false,
inference(resolution,[status(thm)],[p156,c5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT016+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.35 % Computer : n018.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Thu Sep 24 01:02:34 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 3.24/0.86 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.24/0.86 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------