%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MGT054-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n015.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:51 PM UTC 2026
% Result : Unsatisfiable 32.81s 4.78s
% Output : Proof 32.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 17
% Syntax : Number of formulae : 95 ( 26 unt; 0 def)
% Number of atoms : 240 ( 26 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 261 ( 116 ~; 145 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 131 ( 3 sgn 56 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f23,axiom,
( greater(age(A,C),sigma)
| ~ dissimilar(A,B,C)
| age(A,B) != zero
| ~ organization(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_15_50) ).
fof(f23_nnf,plain,
! [A,B,C] :
( greater(age(A,C),sigma)
| ~ dissimilar(A,B,C)
| age(A,B) != zero
| ~ organization(A) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [A,B,C] :
( greater(age(A,C),sigma)
| ~ dissimilar(A,B,C)
| age(A,B) != zero
| ~ organization(A) ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( greater(age(X0,X2),sigma)
| ~ dissimilar(X0,X1,X2)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(f25,negated_conjecture,
organization(sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_5_52) ).
fof(f25_nnf,plain,
organization(sk1),
inference(nnf_transformation,[status(thm)],[f25]) ).
cnf(c25,plain,
organization(sk1),
inference(cnf_transformation,[status(esa)],[f25_nnf]) ).
cnf(p120,plain,
( greater(age(sk1,X1),sigma)
| ~ dissimilar(sk1,X0,X1)
| age(sk1,X0) != zero ),
inference(resolution,[status(thm)],[c23,c25]) ).
cnf(f27,negated_conjecture,
age(sk1,sk2) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_5_54) ).
fof(f27_nnf,plain,
age(sk1,sk2) = zero,
inference(nnf_transformation,[status(thm)],[f27]) ).
cnf(c27,plain,
age(sk1,sk2) = zero,
inference(cnf_transformation,[status(esa)],[f27_nnf]) ).
cnf(p148,plain,
( greater(age(sk1,X0),sigma)
| ~ dissimilar(sk1,sk2,X0) ),
inference(resolution,[status(thm)],[p120,c27]) ).
cnf(f20,axiom,
( is_aligned(A,B)
| age(A,B) != zero
| ~ organization(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_13_47) ).
fof(f20_nnf,plain,
! [A,B] :
( is_aligned(A,B)
| age(A,B) != zero
| ~ organization(A) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [A,B] :
( is_aligned(A,B)
| age(A,B) != zero
| ~ organization(A) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( is_aligned(X0,X1)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p110,plain,
( is_aligned(sk1,X0)
| age(sk1,X0) != zero ),
inference(resolution,[status(thm)],[c20,c25]) ).
cnf(p111,plain,
is_aligned(sk1,sk2),
inference(resolution,[status(thm)],[p110,c27]) ).
cnf(f17,axiom,
( dissimilar(A,B,C)
| is_aligned(A,C)
| ~ is_aligned(A,B)
| ~ organization(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_2_44) ).
fof(f17_nnf,plain,
! [A,B,C] :
( dissimilar(A,B,C)
| is_aligned(A,C)
| ~ is_aligned(A,B)
| ~ organization(A) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [A,B,C] :
( dissimilar(A,B,C)
| is_aligned(A,C)
| ~ is_aligned(A,B)
| ~ organization(A) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( dissimilar(X0,X1,X2)
| is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p105,plain,
( dissimilar(sk1,X0,X1)
| is_aligned(sk1,X1)
| ~ is_aligned(sk1,X0) ),
inference(resolution,[status(thm)],[c17,c25]) ).
cnf(p112,plain,
( dissimilar(sk1,sk2,X0)
| is_aligned(sk1,X0) ),
inference(resolution,[status(thm)],[p111,p105]) ).
cnf(p149,plain,
( is_aligned(sk1,X0)
| greater(age(sk1,X0),sigma) ),
inference(resolution,[status(thm)],[p148,p112]) ).
cnf(f6,axiom,
( greater(B,A)
| ~ smaller(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_smaller_7) ).
fof(f6_nnf,plain,
! [A,B] :
( greater(B,A)
| ~ smaller(A,B) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B] :
( greater(B,A)
| ~ smaller(A,B) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( greater(X1,X0)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(f0,axiom,
( A = B
| smaller(A,B)
| ~ smaller_or_equal(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_smaller_or_equal_1) ).
fof(f0_nnf,plain,
! [A,B] :
( A = B
| smaller(A,B)
| ~ smaller_or_equal(A,B) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] :
( A = B
| smaller(A,B)
| ~ smaller_or_equal(A,B) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( X0 = X1
| smaller(X0,X1)
| ~ smaller_or_equal(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(f28,negated_conjecture,
smaller_or_equal(age(sk1,sk3),sigma),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_5_55) ).
fof(f28_nnf,plain,
smaller_or_equal(age(sk1,sk3),sigma),
inference(nnf_transformation,[status(thm)],[f28]) ).
cnf(c28,plain,
smaller_or_equal(age(sk1,sk3),sigma),
inference(cnf_transformation,[status(esa)],[f28_nnf]) ).
cnf(p32,plain,
( age(sk1,sk3) = sigma
| smaller(age(sk1,sk3),sigma) ),
inference(resolution,[status(thm)],[c0,c28]) ).
cnf(p37,plain,
( age(sk1,sk3) = sigma
| greater(sigma,age(sk1,sk3)) ),
inference(resolution,[status(thm)],[c6,p32]) ).
cnf(f8,axiom,
( ~ greater(B,A)
| ~ greater(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meaning_postulate_greater_strict_9) ).
fof(f8_nnf,plain,
! [A,B] :
( ~ greater(B,A)
| ~ greater(A,B) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A,B] :
( ~ greater(B,A)
| ~ greater(A,B) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p46,plain,
( ~ greater(age(sk1,sk3),sigma)
| age(sk1,sk3) = sigma ),
inference(resolution,[status(thm)],[p37,c8]) ).
cnf(p169,plain,
( age(sk1,sk3) = sigma
| is_aligned(sk1,sk3) ),
inference(resolution,[status(thm)],[p149,p46]) ).
cnf(p177,plain,
( is_aligned(sk1,sk3)
| greater(sigma,sigma)
| is_aligned(sk1,sk3) ),
inference(superposition,[status(thm)],[p169,p149]) ).
cnf(p186,plain,
( greater(sigma,sigma)
| is_aligned(sk1,sk3) ),
inference(factoring,[status(thm)],[p177]) ).
cnf(f21,axiom,
( greater(capability(A,B),capability(A,C))
| is_aligned(A,C)
| ~ is_aligned(A,B)
| ~ organization(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_14_48) ).
fof(f21_nnf,plain,
! [A,B,C] :
( greater(capability(A,B),capability(A,C))
| is_aligned(A,C)
| ~ is_aligned(A,B)
| ~ organization(A) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [A,B,C] :
( greater(capability(A,B),capability(A,C))
| is_aligned(A,C)
| ~ is_aligned(A,B)
| ~ organization(A) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( greater(capability(X0,X1),capability(X0,X2))
| is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p114,plain,
( greater(capability(sk1,X0),capability(sk1,X1))
| is_aligned(sk1,X1)
| ~ is_aligned(sk1,X0) ),
inference(resolution,[status(thm)],[c21,c25]) ).
cnf(p189,plain,
( greater(capability(sk1,sk3),capability(sk1,X0))
| is_aligned(sk1,X0)
| greater(sigma,sigma) ),
inference(resolution,[status(thm)],[p186,p114]) ).
cnf(f24,axiom,
( greater(hazard_of_mortality(A,B),hazard_of_mortality(A,C))
| ~ greater(capability(A,C),capability(A,B))
| has_immunity(A,C)
| has_immunity(A,B)
| ~ organization(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_16_51) ).
fof(f24_nnf,plain,
! [A,B,C] :
( greater(hazard_of_mortality(A,B),hazard_of_mortality(A,C))
| ~ greater(capability(A,C),capability(A,B))
| has_immunity(A,C)
| has_immunity(A,B)
| ~ organization(A) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [A,B,C] :
( greater(hazard_of_mortality(A,B),hazard_of_mortality(A,C))
| ~ greater(capability(A,C),capability(A,B))
| has_immunity(A,C)
| has_immunity(A,B)
| ~ organization(A) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( greater(hazard_of_mortality(X0,X1),hazard_of_mortality(X0,X2))
| ~ greater(capability(X0,X2),capability(X0,X1))
| has_immunity(X0,X2)
| has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p125,plain,
( greater(hazard_of_mortality(sk1,X0),hazard_of_mortality(sk1,X1))
| ~ greater(capability(sk1,X1),capability(sk1,X0))
| has_immunity(sk1,X1)
| has_immunity(sk1,X0) ),
inference(resolution,[status(thm)],[c24,c25]) ).
cnf(p319,plain,
( greater(hazard_of_mortality(sk1,X0),hazard_of_mortality(sk1,sk3))
| has_immunity(sk1,sk3)
| has_immunity(sk1,X0)
| is_aligned(sk1,X0)
| greater(sigma,sigma) ),
inference(resolution,[status(thm)],[p189,p125]) ).
cnf(f31,negated_conjecture,
~ greater(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_5_58) ).
fof(f31_nnf,plain,
~ greater(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3)),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
~ greater(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3)),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
~ greater(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3)),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p2371,plain,
( has_immunity(sk1,sk3)
| has_immunity(sk1,sk4)
| is_aligned(sk1,sk4)
| greater(sigma,sigma) ),
inference(resolution,[status(thm)],[p319,c31]) ).
cnf(f22,axiom,
( dissimilar(A,B,C)
| ~ greater(age(A,C),sigma)
| age(A,B) != zero
| ~ organization(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_15_49) ).
fof(f22_nnf,plain,
! [A,B,C] :
( dissimilar(A,B,C)
| ~ greater(age(A,C),sigma)
| age(A,B) != zero
| ~ organization(A) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [A,B,C] :
( dissimilar(A,B,C)
| ~ greater(age(A,C),sigma)
| age(A,B) != zero
| ~ organization(A) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( dissimilar(X0,X1,X2)
| ~ greater(age(X0,X2),sigma)
| age(X0,X1) != zero
| ~ organization(X0) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(p115,plain,
( dissimilar(sk1,X0,X1)
| ~ greater(age(sk1,X1),sigma)
| age(sk1,X0) != zero ),
inference(resolution,[status(thm)],[c22,c25]) ).
cnf(p140,plain,
( dissimilar(sk1,sk2,X0)
| ~ greater(age(sk1,X0),sigma) ),
inference(resolution,[status(thm)],[p115,c27]) ).
cnf(f29,negated_conjecture,
greater(age(sk1,sk4),sigma),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_5_56) ).
fof(f29_nnf,plain,
greater(age(sk1,sk4),sigma),
inference(nnf_transformation,[status(thm)],[f29]) ).
cnf(c29,plain,
greater(age(sk1,sk4),sigma),
inference(cnf_transformation,[status(esa)],[f29_nnf]) ).
cnf(p141,plain,
dissimilar(sk1,sk2,sk4),
inference(resolution,[status(thm)],[p140,c29]) ).
cnf(f15,axiom,
( ~ is_aligned(A,C)
| ~ is_aligned(A,B)
| ~ dissimilar(A,B,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_2_42) ).
fof(f15_nnf,plain,
! [A,B,C] :
( ~ is_aligned(A,C)
| ~ is_aligned(A,B)
| ~ dissimilar(A,B,C) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [A,B,C] :
( ~ is_aligned(A,C)
| ~ is_aligned(A,B)
| ~ dissimilar(A,B,C) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( ~ is_aligned(X0,X2)
| ~ is_aligned(X0,X1)
| ~ dissimilar(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p143,plain,
( ~ is_aligned(sk1,sk4)
| ~ is_aligned(sk1,sk2) ),
inference(resolution,[status(thm)],[p141,c15]) ).
cnf(p147,plain,
~ is_aligned(sk1,sk4),
inference(resolution,[status(thm)],[p143,p111]) ).
cnf(p2410,plain,
( has_immunity(sk1,sk3)
| has_immunity(sk1,sk4)
| greater(sigma,sigma) ),
inference(resolution,[status(thm)],[p2371,p147]) ).
cnf(f11,axiom,
( ~ has_immunity(A,B)
| has_endowment(A)
| ~ organization(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_1_38) ).
fof(f11_nnf,plain,
! [A,B] :
( ~ has_immunity(A,B)
| has_endowment(A)
| ~ organization(A) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A,B] :
( ~ has_immunity(A,B)
| has_endowment(A)
| ~ organization(A) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( ~ has_immunity(X0,X1)
| has_endowment(X0)
| ~ organization(X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p64,plain,
( ~ has_immunity(sk1,X0)
| has_endowment(sk1) ),
inference(resolution,[status(thm)],[c11,c25]) ).
cnf(p2411,plain,
( has_endowment(sk1)
| has_immunity(sk1,sk3)
| greater(sigma,sigma) ),
inference(resolution,[status(thm)],[p2410,p64]) ).
cnf(p2413,plain,
( has_endowment(sk1)
| has_endowment(sk1)
| greater(sigma,sigma) ),
inference(resolution,[status(thm)],[p2411,p64]) ).
cnf(p2415,plain,
( has_endowment(sk1)
| greater(sigma,sigma) ),
inference(factoring,[status(thm)],[p2413]) ).
cnf(p42,plain,
~ greater(X0,X0),
inference(factoring,[status(thm)],[c8]) ).
cnf(p2423,plain,
has_endowment(sk1),
inference(resolution,[status(thm)],[p2415,p42]) ).
cnf(f26,negated_conjecture,
~ has_endowment(sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_5_53) ).
fof(f26_nnf,plain,
~ has_endowment(sk1),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
~ has_endowment(sk1),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
~ has_endowment(sk1),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p2424,plain,
$false,
inference(resolution,[status(thm)],[p2423,c26]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT054-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n015.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 01:17:10 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 32.81/4.78 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 32.81/4.78 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------