%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : MGT012+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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 : Sun Sep 27 08:01:00 AM UTC 2026
% Result : Theorem 11.76s 1.86s
% Output : CNFRefutation 11.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 7
% Syntax : Number of formulae : 50 ( 11 unt; 0 def)
% Number of atoms : 182 ( 9 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 237 ( 105 ~; 97 |; 28 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 111 ( 0 sgn 35 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mp5,axiom,
! [X0,X1] :
( organization(X0,X1)
=> ? [X2] : inertia(X0,X2,X1) ) ).
fof(mp6_2,axiom,
! [X0,X1] :
~ ( greater(X1,X0)
& greater(X0,X1) ) ).
fof(mp9,axiom,
! [X0,X1] :
( organization(X0,X1)
=> ? [X2] : class(X0,X2,X1) ) ).
fof(mp10,axiom,
! [X0,X1,X2,X3,X4] :
( ( class(X0,X4,X2)
& class(X0,X3,X1)
& 'reorganization$ufree'(X0,X1,X2)
& organization(X0,X2)
& organization(X0,X1) )
=> X3 = X4 ) ).
fof(a12_FOL,hypothesis,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ( 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) )
=> greater(X6,X5) ) ).
fof(t2_FOL,hypothesis,
! [X0,X1,X2,X3,X4] :
( ( greater(X4,X3)
& inertia(X0,X2,X4)
& inertia(X0,X1,X3)
& 'reorganization$ufree'(X0,X3,X4)
& organization(X0,X4)
& organization(X0,X3) )
=> greater(X2,X1) ) ).
fof(t12_FOL,conjecture,
! [X0,X1,X2,X3,X4] :
( ( greater(X4,X3)
& complexity(X0,X2,X4)
& complexity(X0,X1,X3)
& 'reorganization$ufree'(X0,X3,X4)
& organization(X0,X4)
& organization(X0,X3) )
=> ~ greater(X1,X2) ) ).
fof(negated_conjecture,negated_conjecture,
~ ! [X0,X1,X2,X3,X4] :
( ( greater(X4,X3)
& complexity(X0,X2,X4)
& complexity(X0,X1,X3)
& 'reorganization$ufree'(X0,X3,X4)
& organization(X0,X4)
& organization(X0,X3) )
=> ~ greater(X1,X2) ),
inference(negate_conjecture,[status(cth)],[t12_FOL]) ).
cnf(c0,plain,
( inertia(X0,sK2(X0,X1),X1)
| ~ organization(X0,X1) ),
inference(clausification,[status(esa)],[mp5]) ).
cnf(c2,plain,
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
inference(clausification,[status(esa)],[mp6_2]) ).
cnf(c3,plain,
( class(X0,sK9(X0,X1),X1)
| ~ organization(X0,X1) ),
inference(clausification,[status(esa)],[mp9]) ).
cnf(c4,plain,
( ~ organization(X0,X4)
| ~ 'reorganization$ufree'(X0,X2,X4)
| ~ class(X0,X3,X4)
| ~ organization(X0,X2)
| X1 = X3
| ~ class(X0,X1,X2) ),
inference(clausification,[status(esa)],[mp10]) ).
cnf(c5,plain,
( ~ complexity(X0,X5,X1)
| ~ inertia(X2,X8,X4)
| ~ class(X0,X3,X1)
| ~ inertia(X0,X7,X1)
| ~ complexity(X2,X6,X4)
| greater(X7,X8)
| ~ greater(X5,X6)
| ~ organization(X2,X4)
| ~ class(X2,X3,X4)
| ~ organization(X0,X1) ),
inference(clausification,[status(esa)],[a12_FOL]) ).
cnf(c6,plain,
( greater(X3,X4)
| ~ greater(X1,X2)
| ~ 'reorganization$ufree'(X0,X2,X1)
| ~ inertia(X0,X4,X2)
| ~ inertia(X0,X3,X1)
| ~ organization(X0,X2)
| ~ organization(X0,X1) ),
inference(clausification,[status(esa)],[t2_FOL]) ).
cnf(c7,plain,
organization(sK29,sK32),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c8,plain,
organization(sK29,sK33),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c9,plain,
'reorganization$ufree'(sK29,sK32,sK33),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c10,plain,
complexity(sK29,sK30,sK32),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c11,plain,
complexity(sK29,sK31,sK33),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c12,plain,
greater(sK33,sK32),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c13,plain,
greater(sK30,sK31),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ greater(sK33,sK32)
| greater(X1,X0)
| ~ inertia(sK29,X1,sK33)
| ~ inertia(sK29,X0,sK32)
| ~ organization(sK29,sK32)
| ~ organization(sK29,sK33) ),
inference(resolution,[status(thm)],[c6,c9]) ).
cnf(d1,plain,
( ~ greater(sK33,sK32)
| greater(X0,X1)
| ~ inertia(sK29,X1,sK32)
| ~ inertia(sK29,X0,sK33)
| ~ organization(sK29,sK33) ),
inference(resolution,[status(thm)],[c7,d0]) ).
cnf(d2,plain,
( ~ greater(sK33,sK32)
| greater(X1,X0)
| ~ inertia(sK29,X1,sK33)
| ~ inertia(sK29,X0,sK32) ),
inference(resolution,[status(thm)],[c8,d1]) ).
cnf(d3,plain,
( greater(X0,X1)
| ~ inertia(sK29,X1,sK32)
| ~ inertia(sK29,X0,sK33) ),
inference(resolution,[status(thm)],[c12,d2]) ).
cnf(d4,plain,
( ~ organization(sK29,sK33)
| greater(sK2(sK29,sK33),X0)
| ~ inertia(sK29,X0,sK32) ),
inference(resolution,[status(thm)],[d3,c0]) ).
cnf(d5,plain,
( greater(sK2(sK29,sK33),X0)
| ~ inertia(sK29,X0,sK32) ),
inference(resolution,[status(thm)],[c8,d4]) ).
cnf(d6,plain,
( ~ greater(X0,sK2(sK29,sK33))
| ~ inertia(sK29,X0,sK32) ),
inference(resolution,[status(thm)],[d5,c2]) ).
cnf(d7,plain,
( ~ class(sK29,X1,sK33)
| ~ class(sK29,X0,sK32)
| ~ organization(sK29,sK33)
| ~ organization(sK29,sK32)
| X0 = X1 ),
inference(resolution,[status(thm)],[c9,c4]) ).
cnf(d8,plain,
( ~ class(sK29,X0,sK32)
| ~ class(sK29,X1,sK33)
| ~ organization(sK29,sK33)
| X0 = X1 ),
inference(resolution,[status(thm)],[c7,d7]) ).
cnf(d9,plain,
( ~ class(sK29,X0,sK32)
| ~ class(sK29,X1,sK33)
| X0 = X1 ),
inference(resolution,[status(thm)],[c8,d8]) ).
cnf(d10,plain,
( ~ organization(sK29,sK32)
| ~ class(sK29,X0,sK33)
| sK9(sK29,sK32) = X0 ),
inference(resolution,[status(thm)],[d9,c3]) ).
cnf(d11,plain,
( ~ class(sK29,X0,sK33)
| sK9(sK29,sK32) = X0 ),
inference(resolution,[status(thm)],[c7,d10]) ).
cnf(d12,plain,
( ~ organization(sK29,sK33)
| sK9(sK29,sK32) = sK9(sK29,sK33) ),
inference(resolution,[status(thm)],[d11,c3]) ).
cnf(d13,plain,
sK9(sK29,sK32) = sK9(sK29,sK33),
inference(resolution,[status(thm)],[c8,d12]) ).
cnf(d14,plain,
( ~ organization(sK29,sK33)
| class(sK29,sK9(sK29,sK32),sK33) ),
inference(superposition,[status(thm)],[d13,c3]) ).
cnf(d15,plain,
class(sK29,sK9(sK29,sK32),sK33),
inference(resolution,[status(thm)],[c8,d14]) ).
cnf(d16,plain,
( ~ complexity(X0,X4,X1)
| ~ class(sK29,X5,sK33)
| ~ class(X0,X5,X1)
| ~ greater(X4,sK31)
| greater(X2,X3)
| ~ inertia(sK29,X3,sK33)
| ~ inertia(X0,X2,X1)
| ~ organization(sK29,sK33)
| ~ organization(X0,X1) ),
inference(resolution,[status(thm)],[c11,c5]) ).
cnf(d17,plain,
( ~ complexity(X0,X4,X1)
| ~ class(sK29,X5,sK33)
| ~ class(X0,X5,X1)
| greater(X2,X3)
| ~ greater(X4,sK31)
| ~ inertia(sK29,X3,sK33)
| ~ inertia(X0,X2,X1)
| ~ organization(X0,X1) ),
inference(resolution,[status(thm)],[c8,d16]) ).
cnf(d18,plain,
( ~ class(sK29,X2,sK33)
| ~ class(sK29,X2,sK32)
| greater(X0,X1)
| ~ greater(sK30,sK31)
| ~ inertia(sK29,X1,sK33)
| ~ inertia(sK29,X0,sK32)
| ~ organization(sK29,sK32) ),
inference(resolution,[status(thm)],[d17,c10]) ).
cnf(d19,plain,
( ~ class(sK29,X2,sK33)
| ~ class(sK29,X2,sK32)
| ~ greater(sK30,sK31)
| greater(X1,X0)
| ~ inertia(sK29,X1,sK32)
| ~ inertia(sK29,X0,sK33) ),
inference(resolution,[status(thm)],[c7,d18]) ).
cnf(d20,plain,
( ~ class(sK29,X2,sK33)
| ~ class(sK29,X2,sK32)
| greater(X0,X1)
| ~ inertia(sK29,X1,sK33)
| ~ inertia(sK29,X0,sK32) ),
inference(resolution,[status(thm)],[c13,d19]) ).
cnf(d21,plain,
( ~ class(sK29,sK9(sK29,sK32),sK32)
| greater(X1,X0)
| ~ inertia(sK29,X1,sK32)
| ~ inertia(sK29,X0,sK33) ),
inference(resolution,[status(thm)],[d20,d15]) ).
cnf(d22,plain,
( ~ organization(sK29,sK32)
| greater(X0,X1)
| ~ inertia(sK29,X1,sK33)
| ~ inertia(sK29,X0,sK32) ),
inference(resolution,[status(thm)],[d21,c3]) ).
cnf(d23,plain,
( greater(X1,X0)
| ~ inertia(sK29,X1,sK32)
| ~ inertia(sK29,X0,sK33) ),
inference(resolution,[status(thm)],[c7,d22]) ).
cnf(d24,plain,
( ~ organization(sK29,sK33)
| greater(X0,sK2(sK29,sK33))
| ~ inertia(sK29,X0,sK32) ),
inference(resolution,[status(thm)],[d23,c0]) ).
cnf(d25,plain,
( greater(X0,sK2(sK29,sK33))
| ~ inertia(sK29,X0,sK32) ),
inference(resolution,[status(thm)],[c8,d24]) ).
cnf(d26,plain,
( ~ inertia(sK29,X0,sK32)
| ~ inertia(sK29,X0,sK32) ),
inference(resolution,[status(thm)],[d25,d6]) ).
cnf(d27,plain,
~ organization(sK29,sK32),
inference(resolution,[status(thm)],[d26,c0]) ).
cnf(d28,plain,
$false,
inference(resolution,[status(thm)],[c7,d27]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT012+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 00:03:17 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.76/1.86 % SZS status Theorem for theBenchmark.p
% 11.76/1.86 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------