%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : MGT054+1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:29 AM UTC 2026
% Result : Theorem 242.33s 30.81s
% Output : CNFRefutation 242.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 10
% Syntax : Number of formulae : 53 ( 16 unt; 0 def)
% Number of atoms : 143 ( 17 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 157 ( 67 ~; 58 |; 20 &)
% ( 5 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 61 ( 2 sgn 30 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(theorem_5,plain,
! [X,T0,T1,T2] :
( ( organization(X)
& ~ has_endowment(X)
& age(X,T0) = zero
& smaller_or_equal(age(X,T1),sigma)
& greater(age(X,T2),sigma)
& greater(sigma,zero) )
=> greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_5) ).
fof(theorem_5_negated,plain,
~ ! [X,T0,T1,T2] :
( ( organization(X)
& ~ has_endowment(X)
& age(X,T0) = zero
& smaller_or_equal(age(X,T1),sigma)
& greater(age(X,T2),sigma)
& greater(sigma,zero) )
=> greater(hazard_of_mortality(X,T2),hazard_of_mortality(X,T1)) ),
inference(negate_conjecture,[status(cth)],[theorem_5]) ).
cnf(25,plain,
organization(sK1),
inference(cnf,[status(esa)],[theorem_5_negated]) ).
cnf(l0,plain,
organization(sK1),
inference(instantiation,[status(thm)],[25]) ).
fof(assumption_13,plain,
! [X,T] :
( ( organization(X)
& age(X,T) = zero )
=> is_aligned(X,T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_13) ).
cnf(20,plain,
( ~ organization(X0)
| age(X0,X1) != zero
| is_aligned(X0,X1) ),
inference(cnf,[status(esa)],[assumption_13]) ).
cnf(l1,plain,
( ~ organization(sK1)
| age(sK1,sK2) != zero
| is_aligned(sK1,sK2) ),
inference(instantiation,[status(thm)],[20]) ).
fof(definition_2,plain,
! [X,T0,T] :
( dissimilar(X,T0,T)
<=> ( organization(X)
& ~ ( is_aligned(X,T0)
<=> is_aligned(X,T) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',definition_2) ).
cnf(16,plain,
( ~ organization(X0)
| ~ is_aligned(X0,X1)
| sP0(X1,X0,X2)
| dissimilar(X0,X1,X2) ),
inference(cnf,[status(esa)],[definition_2]) ).
cnf(l3,plain,
( ~ organization(sK1)
| ~ is_aligned(sK1,sK2)
| sP0(sK2,sK1,sK3)
| dissimilar(sK1,sK2,sK3) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(19,plain,
( is_aligned(X0,X1)
| ~ sP0(X2,X0,X1) ),
inference(cnf,[status(esa)],[definition_2]) ).
cnf(l1858,plain,
( is_aligned(sK1,sK3)
| ~ sP0(sK2,sK1,sK3) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(27,plain,
age(sK1,sK2) = zero,
inference(cnf,[status(esa)],[theorem_5_negated]) ).
cnf(l2,plain,
age(sK1,sK2) = zero,
inference(instantiation,[status(thm)],[27]) ).
fof(assumption_15,plain,
! [X,T0,T] :
( ( organization(X)
& age(X,T0) = zero )
=> ( greater(age(X,T),sigma)
<=> dissimilar(X,T0,T) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_15) ).
cnf(23,plain,
( ~ organization(X0)
| ~ dissimilar(X0,X1,X2)
| age(X0,X1) != zero
| greater(age(X0,X2),sigma) ),
inference(cnf,[status(esa)],[assumption_15]) ).
cnf(l2682,plain,
( ~ organization(sK1)
| ~ dissimilar(sK1,sK2,sK3)
| age(sK1,sK2) != zero
| greater(age(sK1,sK3),sigma) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l2685,plain,
age(sK1,sK2) = zero,
inference(instantiation,[status(thm)],[27]) ).
fof(definition_smaller_or_equal,plain,
! [X,Y] :
( smaller_or_equal(X,Y)
<=> ( smaller(X,Y)
| X = Y ) ),
file('Axioms/MGT001+0.ax',definition_smaller_or_equal) ).
cnf(0,plain,
( ~ smaller_or_equal(X0,X1)
| smaller(X0,X1)
| X0 = X1 ),
inference(cnf,[status(esa)],[definition_smaller_or_equal]) ).
cnf(l3141,plain,
( ~ smaller_or_equal(age(sK1,sK3),sigma)
| smaller(age(sK1,sK3),sigma)
| age(sK1,sK3) = sigma ),
inference(instantiation,[status(thm)],[0]) ).
fof(assumption_14,plain,
! [X,T0,T] :
( ( organization(X)
& is_aligned(X,T0)
& ~ is_aligned(X,T) )
=> greater(capability(X,T0),capability(X,T)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_14) ).
cnf(21,plain,
( ~ organization(X0)
| ~ is_aligned(X0,X1)
| greater(capability(X0,X1),capability(X0,X2))
| is_aligned(X0,X2) ),
inference(cnf,[status(esa)],[assumption_14]) ).
cnf(l2513,plain,
( ~ organization(sK1)
| ~ is_aligned(sK1,sK3)
| greater(capability(sK1,sK3),capability(sK1,sK4))
| is_aligned(sK1,sK4) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(28,plain,
smaller_or_equal(age(sK1,sK3),sigma),
inference(cnf,[status(esa)],[theorem_5_negated]) ).
cnf(l3152,plain,
smaller_or_equal(age(sK1,sK3),sigma),
inference(instantiation,[status(thm)],[28]) ).
fof(assumption_16,plain,
! [X,T0,T] :
( ( organization(X)
& ~ has_immunity(X,T0)
& ~ has_immunity(X,T)
& greater(capability(X,T),capability(X,T0)) )
=> greater(hazard_of_mortality(X,T0),hazard_of_mortality(X,T)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_16) ).
cnf(24,plain,
( ~ organization(X0)
| ~ greater(capability(X0,X1),capability(X0,X2))
| greater(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X1))
| has_immunity(X0,X2)
| has_immunity(X0,X1) ),
inference(cnf,[status(esa)],[assumption_16]) ).
cnf(l2518,plain,
( ~ organization(sK1)
| ~ greater(capability(sK1,sK3),capability(sK1,sK4))
| greater(hazard_of_mortality(sK1,sK4),hazard_of_mortality(sK1,sK3))
| has_immunity(sK1,sK4)
| has_immunity(sK1,sK3) ),
inference(instantiation,[status(thm)],[24]) ).
fof(definition_smaller,plain,
! [X,Y] :
( smaller(X,Y)
<=> greater(Y,X) ),
file('Axioms/MGT001+0.ax',definition_smaller) ).
cnf(6,plain,
( ~ smaller(X0,X1)
| greater(X1,X0) ),
inference(cnf,[status(esa)],[definition_smaller]) ).
cnf(l3205,plain,
( ~ smaller(age(sK1,sK3),sigma)
| greater(sigma,age(sK1,sK3)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(31,plain,
~ greater(hazard_of_mortality(sK1,sK4),hazard_of_mortality(sK1,sK3)),
inference(cnf,[status(esa)],[theorem_5_negated]) ).
cnf(l2761,plain,
~ greater(hazard_of_mortality(sK1,sK4),hazard_of_mortality(sK1,sK3)),
inference(instantiation,[status(thm)],[31]) ).
fof(meaning_postulate_greater_strict,plain,
! [X,Y] :
~ ( greater(X,Y)
& greater(Y,X) ),
file('Axioms/MGT001+0.ax',meaning_postulate_greater_strict) ).
cnf(8,plain,
( ~ greater(X0,X1)
| ~ greater(X1,X0) ),
inference(cnf,[status(esa)],[meaning_postulate_greater_strict]) ).
cnf(l3109,plain,
( ~ greater(sigma,sigma)
| ~ greater(sigma,sigma) ),
inference(instantiation,[status(thm)],[8]) ).
fof(assumption_1,plain,
! [X,T] :
( ( organization(X)
& ~ has_endowment(X) )
=> ~ has_immunity(X,T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_1) ).
cnf(11,plain,
( ~ organization(X0)
| ~ has_immunity(X0,X1)
| has_endowment(X0) ),
inference(cnf,[status(esa)],[assumption_1]) ).
cnf(l2521,plain,
( ~ organization(sK1)
| ~ has_immunity(sK1,sK4)
| has_endowment(sK1) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(26,plain,
~ has_endowment(sK1),
inference(cnf,[status(esa)],[theorem_5_negated]) ).
cnf(l2843,plain,
~ has_endowment(sK1),
inference(instantiation,[status(thm)],[26]) ).
cnf(l3208,plain,
( ~ greater(age(sK1,sK3),sigma)
| ~ greater(sigma,age(sK1,sK3)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l2519,plain,
( ~ organization(sK1)
| ~ has_immunity(sK1,sK3)
| has_endowment(sK1) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(15,plain,
( ~ dissimilar(X0,X1,X2)
| ~ is_aligned(X0,X1)
| ~ is_aligned(X0,X2) ),
inference(cnf,[status(esa)],[definition_2]) ).
cnf(l2698,plain,
( ~ dissimilar(sK1,sK2,sK4)
| ~ is_aligned(sK1,sK2)
| ~ is_aligned(sK1,sK4) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(22,plain,
( ~ organization(X0)
| ~ greater(age(X0,X1),sigma)
| age(X0,X2) != zero
| dissimilar(X0,X2,X1) ),
inference(cnf,[status(esa)],[assumption_15]) ).
cnf(l2701,plain,
( ~ organization(sK1)
| ~ greater(age(sK1,sK4),sigma)
| age(sK1,sK2) != zero
| dissimilar(sK1,sK2,sK4) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(29,plain,
greater(age(sK1,sK4),sigma),
inference(cnf,[status(esa)],[theorem_5_negated]) ).
cnf(l2726,plain,
greater(age(sK1,sK4),sigma),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2728,plain,
age(sK1,sK2) = zero,
inference(instantiation,[status(thm)],[27]) ).
cnf(l2803,plain,
~ has_endowment(sK1),
inference(instantiation,[status(thm)],[26]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l3,l1858,l2,l2682,l2685,l3141,l2513,l3152,l2518,l3205,l2761,l3109,l2521,l2843,l3208,l2519,l2698,l2701,l2726,l2728,l2803]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT054+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n008.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 : Mon Sep 7 13:25:53 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.36 % launching worker at depth: 1
% 0.10/0.36 % launching worker at depth: 2
% 0.10/0.36 % launching worker at depth: 6
% 0.10/0.36 % launching worker at depth: 7
% 0.10/0.36 % launching worker at depth: 4
% 0.10/0.36 % launching worker at depth: 8
% 0.10/0.36 % launching worker at depth: 5
% 0.10/0.36 % launching worker at depth: 3
% 0.10/0.36 % launching worker at depth: 9
% 0.13/0.38 % launching worker at depth: 10
% 1.00/0.52 % launching worker at depth: 11
% 26.60/3.71 % launching worker at depth: 12
% 242.33/30.81 % SZS status Theorem for theBenchmark
% 242.33/30.81 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------