%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : MGT011+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 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 : Tue Sep 8 06:11:19 AM UTC 2026
% Result : Theorem 18.62s 2.77s
% Output : CNFRefutation 18.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 7
% Syntax : Number of formulae : 48 ( 22 unt; 0 def)
% Number of atoms : 135 ( 3 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 145 ( 58 ~; 52 |; 28 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 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 : 62 ( 0 sgn 35 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t11_FOL,plain,
! [X,S1,S2,T1,T2] :
( ( organization(X,T1)
& organization(X,T2)
& reorganization_free(X,T1,T2)
& size(X,S1,T1)
& size(X,S2,T2)
& greater(T2,T1) )
=> ~ greater(S1,S2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_FOL) ).
fof(t11_FOL_negated,plain,
~ ! [X,S1,S2,T1,T2] :
( ( organization(X,T1)
& organization(X,T2)
& reorganization_free(X,T1,T2)
& size(X,S1,T1)
& size(X,S2,T2)
& greater(T2,T1) )
=> ~ greater(S1,S2) ),
inference(negate_conjecture,[status(cth)],[t11_FOL]) ).
cnf(7,plain,
organization(sK3,sK6),
inference(cnf,[status(esa)],[t11_FOL_negated]) ).
cnf(l0,plain,
organization(sK3,sK6),
inference(instantiation,[status(thm)],[7]) ).
fof(a5_FOL,plain,
! [X,Y,C,S1,S2,I1,I2,T1,T2] :
( ( organization(X,T1)
& organization(Y,T2)
& class(X,C,T1)
& class(Y,C,T2)
& size(X,S1,T1)
& size(Y,S2,T2)
& inertia(X,I1,T1)
& inertia(Y,I2,T2)
& greater(S2,S1) )
=> greater(I2,I1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a5_FOL) ).
cnf(5,plain,
( ~ size(X0,X1,X2)
| ~ size(X3,X4,X5)
| ~ class(X0,X6,X2)
| ~ class(X3,X6,X5)
| ~ organization(X0,X2)
| ~ organization(X3,X5)
| ~ inertia(X0,X7,X2)
| ~ inertia(X3,X8,X5)
| ~ greater(X4,X1)
| greater(X8,X7) ),
inference(cnf,[status(esa)],[a5_FOL]) ).
cnf(l1,plain,
( ~ size(sK3,sK5,sK7)
| ~ size(sK3,sK4,sK6)
| ~ class(sK3,sK2(sK3,sK7),sK7)
| ~ class(sK3,sK2(sK3,sK7),sK6)
| ~ organization(sK3,sK7)
| ~ organization(sK3,sK6)
| ~ inertia(sK3,sK1(sK3,sK7),sK7)
| ~ inertia(sK3,sK1(sK3,sK6),sK6)
| ~ greater(sK4,sK5)
| greater(sK1(sK3,sK6),sK1(sK3,sK7)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(10,plain,
size(sK3,sK4,sK6),
inference(cnf,[status(esa)],[t11_FOL_negated]) ).
cnf(l5,plain,
size(sK3,sK4,sK6),
inference(instantiation,[status(thm)],[10]) ).
cnf(8,plain,
organization(sK3,sK7),
inference(cnf,[status(esa)],[t11_FOL_negated]) ).
cnf(l226,plain,
organization(sK3,sK7),
inference(instantiation,[status(thm)],[8]) ).
cnf(13,plain,
greater(sK4,sK5),
inference(cnf,[status(esa)],[t11_FOL_negated]) ).
cnf(l1408,plain,
greater(sK4,sK5),
inference(instantiation,[status(thm)],[13]) ).
fof(mp9,plain,
! [X,T] :
( organization(X,T)
=> ? [C] : class(X,C,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp9) ).
cnf(3,plain,
( ~ organization(X0,X1)
| class(X0,sK2(X0,X1),X1) ),
inference(cnf,[status(esa)],[mp9]) ).
cnf(l3,plain,
( ~ organization(sK3,sK7)
| class(sK3,sK2(sK3,sK7),sK7) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l227,plain,
organization(sK3,sK7),
inference(instantiation,[status(thm)],[8]) ).
fof(mp5,plain,
! [X,T] :
( organization(X,T)
=> ? [I] : inertia(X,I,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp5) ).
cnf(0,plain,
( ~ organization(X0,X1)
| inertia(X0,sK1(X0,X1),X1) ),
inference(cnf,[status(esa)],[mp5]) ).
cnf(l1406,plain,
( ~ organization(sK3,sK6)
| inertia(sK3,sK1(sK3,sK6),sK6) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1143,plain,
( ~ organization(sK3,sK6)
| class(sK3,sK2(sK3,sK6),sK6) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l719,plain,
( ~ organization(sK3,sK7)
| inertia(sK3,sK1(sK3,sK7),sK7) ),
inference(instantiation,[status(thm)],[0]) ).
fof(mp6_2,plain,
! [X,Y] :
~ ( greater(X,Y)
& greater(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp6_2) ).
cnf(2,plain,
( ~ greater(X0,X1)
| ~ greater(X1,X0) ),
inference(cnf,[status(esa)],[mp6_2]) ).
cnf(l1419,plain,
( ~ greater(sK1(sK3,sK6),sK1(sK3,sK7))
| ~ greater(sK1(sK3,sK7),sK1(sK3,sK6)) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(11,plain,
size(sK3,sK5,sK7),
inference(cnf,[status(esa)],[t11_FOL_negated]) ).
cnf(l2,plain,
size(sK3,sK5,sK7),
inference(instantiation,[status(thm)],[11]) ).
fof(t2_FOL,plain,
! [X,I1,I2,T1,T2] :
( ( organization(X,T1)
& organization(X,T2)
& reorganization_free(X,T1,T2)
& inertia(X,I1,T1)
& inertia(X,I2,T2)
& greater(T2,T1) )
=> greater(I2,I1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_FOL) ).
cnf(6,plain,
( ~ reorganization_free(X0,X1,X2)
| ~ organization(X0,X1)
| ~ organization(X0,X2)
| ~ inertia(X0,X3,X1)
| ~ inertia(X0,X4,X2)
| ~ greater(X2,X1)
| greater(X4,X3) ),
inference(cnf,[status(esa)],[t2_FOL]) ).
cnf(l1434,plain,
( ~ reorganization_free(sK3,sK6,sK7)
| ~ organization(sK3,sK6)
| ~ organization(sK3,sK7)
| ~ inertia(sK3,sK1(sK3,sK6),sK6)
| ~ inertia(sK3,sK1(sK3,sK7),sK7)
| ~ greater(sK7,sK6)
| greater(sK1(sK3,sK7),sK1(sK3,sK6)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(9,plain,
reorganization_free(sK3,sK6,sK7),
inference(cnf,[status(esa)],[t11_FOL_negated]) ).
cnf(l1439,plain,
reorganization_free(sK3,sK6,sK7),
inference(instantiation,[status(thm)],[9]) ).
fof(mp10,plain,
! [X,T1,T2,C1,C2] :
( ( organization(X,T1)
& organization(X,T2)
& reorganization_free(X,T1,T2)
& class(X,C1,T1)
& class(X,C2,T2) )
=> C1 = C2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp10) ).
cnf(4,plain,
( ~ reorganization_free(X0,X1,X2)
| ~ class(X0,X3,X1)
| ~ class(X0,X4,X2)
| ~ organization(X0,X1)
| ~ organization(X0,X2)
| X3 = X4 ),
inference(cnf,[status(esa)],[mp10]) ).
cnf(l1148,plain,
( ~ reorganization_free(sK3,sK6,sK7)
| ~ class(sK3,sK2(sK3,sK6),sK6)
| ~ class(sK3,sK2(sK3,sK7),sK7)
| ~ organization(sK3,sK6)
| ~ organization(sK3,sK7)
| sK2(sK3,sK6) = sK2(sK3,sK7) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1166,plain,
( ~ organization(sK3,sK6)
| class(sK3,sK2(sK3,sK6),sK6) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1624,plain,
( ~ organization(sK3,sK7)
| inertia(sK3,sK1(sK3,sK7),sK7) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2028,plain,
organization(sK3,sK7),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1625,plain,
organization(sK3,sK7),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1660,plain,
( ~ organization(sK3,sK6)
| inertia(sK3,sK1(sK3,sK6),sK6) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1149,plain,
reorganization_free(sK3,sK6,sK7),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1224,plain,
organization(sK3,sK7),
inference(instantiation,[status(thm)],[8]) ).
cnf(12,plain,
greater(sK7,sK6),
inference(cnf,[status(esa)],[t11_FOL_negated]) ).
cnf(l2024,plain,
greater(sK7,sK6),
inference(instantiation,[status(thm)],[12]) ).
cnf(l987,plain,
organization(sK3,sK7),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1150,plain,
( ~ organization(sK3,sK7)
| class(sK3,sK2(sK3,sK7),sK7) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1219,plain,
organization(sK3,sK7),
inference(instantiation,[status(thm)],[8]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l5,l226,l1408,l3,l227,l1406,l1143,l719,l1419,l2,l1434,l1439,l1148,l1166,l1624,l2028,l1625,l1660,l1149,l1224,l2024,l987,l1150,l1219]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT011+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n018.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 : Mon Sep 7 11:50:22 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % launching worker at depth: 1
% 0.08/0.36 % launching worker at depth: 7
% 0.08/0.36 % launching worker at depth: 2
% 0.08/0.36 % launching worker at depth: 3
% 0.08/0.36 % launching worker at depth: 4
% 0.08/0.36 % launching worker at depth: 5
% 0.08/0.36 % launching worker at depth: 6
% 0.08/0.36 % launching worker at depth: 8
% 0.13/0.36 % launching worker at depth: 9
% 0.13/0.37 % launching worker at depth: 10
% 0.13/0.42 % launching worker at depth: 11
% 4.32/0.98 % launching worker at depth: 12
% 18.62/2.77 % SZS status Theorem for theBenchmark
% 18.62/2.77 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------