%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MGT057-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n005.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:52 PM UTC 2026
% Result : Unsatisfiable 1.93s 1.50s
% Output : Proof 1.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 18
% Syntax : Number of formulae : 138 ( 106 unt; 0 def)
% Number of atoms : 194 ( 98 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 122 ( 66 ~; 56 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-4 aty)
% Number of variables : 112 ( 2 sgn 32 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f26,negated_conjecture,
( hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3)
| ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_6_46) ).
fof(f26_nnf,plain,
( hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3)
| ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
( hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3)
| ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
( hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3)
| ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(t32,plain,
ifeq(greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)),true,ifeq(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3),false,true),true) = true,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(t51,plain,
ifeq(greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)),true,ifeq(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3),false,true),true) = true,
inference(orient,[status(thm)],[t32]) ).
cnf(f19,axiom,
( greater(hazard_of_mortality(A,C),hazard_of_mortality(A,B))
| has_immunity(A,C)
| ~ has_immunity(A,B)
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_3_39) ).
fof(f19_nnf,plain,
! [A,B,C] :
( greater(hazard_of_mortality(A,C),hazard_of_mortality(A,B))
| has_immunity(A,C)
| ~ has_immunity(A,B)
| ~ organization(A) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [A,B,C] :
( greater(hazard_of_mortality(A,C),hazard_of_mortality(A,B))
| has_immunity(A,C)
| ~ has_immunity(A,B)
| ~ organization(A) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
( greater(hazard_of_mortality(X0,X2),hazard_of_mortality(X0,X1))
| has_immunity(X0,X2)
| ~ has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(t37,plain,
ifeq(organization(X1),true,ifeq(has_immunity(X1,X2),true,or(has_immunity(X1,X3),greater(hazard_of_mortality(X1,X3),hazard_of_mortality(X1,X2))),true),true) = true,
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(t55,plain,
ifeq(organization(X1),true,ifeq(has_immunity(X1,X2),true,or(has_immunity(X1,X3),greater(hazard_of_mortality(X1,X3),hazard_of_mortality(X1,X2))),true),true) = true,
inference(orient,[status(thm)],[t37]) ).
cnf(f12,axiom,
( has_immunity(A,B)
| ~ smaller_or_equal(age(A,B),eta)
| ~ has_endowment(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',definition_1_32) ).
fof(f12_nnf,plain,
! [A,B] :
( has_immunity(A,B)
| ~ smaller_or_equal(age(A,B),eta)
| ~ has_endowment(A) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A,B] :
( has_immunity(A,B)
| ~ smaller_or_equal(age(A,B),eta)
| ~ has_endowment(A) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( has_immunity(X0,X1)
| ~ smaller_or_equal(age(X0,X1),eta)
| ~ has_endowment(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t30,plain,
ifeq(has_endowment(X1),true,ifeq(smaller_or_equal(age(X1,X2),eta),true,has_immunity(X1,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t53,plain,
ifeq(has_endowment(X1),true,ifeq(smaller_or_equal(age(X1,X2),eta),true,has_immunity(X1,X2),true),true) = true,
inference(orient,[status(thm)],[t30]) ).
cnf(f23,negated_conjecture,
smaller_or_equal(age(sk2,sk4),eta),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_6_43) ).
fof(f23_nnf,plain,
smaller_or_equal(age(sk2,sk4),eta),
inference(nnf_transformation,[status(thm)],[f23]) ).
cnf(c23,plain,
smaller_or_equal(age(sk2,sk4),eta),
inference(cnf_transformation,[status(esa)],[f23_nnf]) ).
cnf(t13,plain,
smaller_or_equal(age(sk2,sk4),eta) = true,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t107,plain,
smaller_or_equal(age(sk2,sk4),eta) = true,
inference(orient,[status(thm)],[t13]) ).
cnf(t111,plain,
true = ifeq(has_endowment(sk2),true,ifeq(true,true,has_immunity(sk2,sk4),true),true),
inference(cp,[status(thm)],[t53,t107]) ).
cnf(f21,negated_conjecture,
has_endowment(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_6_41) ).
fof(f21_nnf,plain,
has_endowment(sk2),
inference(nnf_transformation,[status(thm)],[f21]) ).
cnf(c21,plain,
has_endowment(sk2),
inference(cnf_transformation,[status(esa)],[f21_nnf]) ).
cnf(t0,plain,
has_endowment(sk2) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t96,plain,
has_endowment(sk2) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t416,plain,
true = ifeq(true,true,ifeq(true,true,has_immunity(sk2,sk4),true),true),
inference(step,[status(thm)],[t111,t96]) ).
cnf(t12,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t39,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t417,plain,
true = ifeq(true,true,has_immunity(sk2,sk4),true),
inference(step,[status(thm)],[t416,t39]) ).
cnf(t418,plain,
true = has_immunity(sk2,sk4),
inference(step,[status(thm)],[t417,t39]) ).
cnf(t133,plain,
has_immunity(sk2,sk4) = true,
inference(orient,[status(thm)],[t418]) ).
cnf(t137,plain,
true = ifeq(organization(sk2),true,ifeq(true,true,or(has_immunity(sk2,X1),greater(hazard_of_mortality(sk2,X1),hazard_of_mortality(sk2,sk4))),true),true),
inference(cp,[status(thm)],[t55,t133]) ).
cnf(f20,negated_conjecture,
organization(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_6_40) ).
fof(f20_nnf,plain,
organization(sk2),
inference(nnf_transformation,[status(thm)],[f20]) ).
cnf(c20,plain,
organization(sk2),
inference(cnf_transformation,[status(esa)],[f20_nnf]) ).
cnf(t3,plain,
organization(sk2) = true,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t104,plain,
organization(sk2) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t470,plain,
true = ifeq(true,true,ifeq(true,true,or(has_immunity(sk2,X1),greater(hazard_of_mortality(sk2,X1),hazard_of_mortality(sk2,sk4))),true),true),
inference(step,[status(thm)],[t137,t104]) ).
cnf(t471,plain,
true = ifeq(true,true,or(has_immunity(sk2,X1),greater(hazard_of_mortality(sk2,X1),hazard_of_mortality(sk2,sk4))),true),
inference(step,[status(thm)],[t470,t39]) ).
cnf(t472,plain,
true = or(has_immunity(sk2,X1),greater(hazard_of_mortality(sk2,X1),hazard_of_mortality(sk2,sk4))),
inference(step,[status(thm)],[t471,t39]) ).
cnf(t273,plain,
or(has_immunity(sk2,X1),greater(hazard_of_mortality(sk2,X1),hazard_of_mortality(sk2,sk4))) = true,
inference(orient,[status(thm)],[t472]) ).
cnf(t14,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t115,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t14]) ).
cnf(f13,axiom,
( ~ has_immunity(A,B)
| ~ greater(age(A,B),eta)
| ~ has_endowment(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',definition_1_33) ).
fof(f13_nnf,plain,
! [A,B] :
( ~ has_immunity(A,B)
| ~ greater(age(A,B),eta)
| ~ has_endowment(A) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [A,B] :
( ~ has_immunity(A,B)
| ~ greater(age(A,B),eta)
| ~ has_endowment(A) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( ~ has_immunity(X0,X1)
| ~ greater(age(X0,X1),eta)
| ~ has_endowment(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t29,plain,
or(not(has_endowment(X1)),or(not(greater(age(X1,X2),eta)),not(has_immunity(X1,X2)))) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t92,plain,
or(not(has_endowment(X1)),or(not(greater(age(X1,X2),eta)),not(has_immunity(X1,X2)))) = true,
inference(orient,[status(thm)],[t29]) ).
cnf(f24,negated_conjecture,
greater(age(sk2,sk5),eta),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_6_44) ).
fof(f24_nnf,plain,
greater(age(sk2,sk5),eta),
inference(nnf_transformation,[status(thm)],[f24]) ).
cnf(c24,plain,
greater(age(sk2,sk5),eta),
inference(cnf_transformation,[status(esa)],[f24_nnf]) ).
cnf(t11,plain,
greater(age(sk2,sk5),eta) = true,
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t73,plain,
greater(age(sk2,sk5),eta) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(t93,plain,
true = or(not(has_endowment(sk2)),or(not(true),not(has_immunity(sk2,sk5)))),
inference(cp,[status(thm)],[t92,t73]) ).
cnf(t460,plain,
true = or(not(true),or(not(true),not(has_immunity(sk2,sk5)))),
inference(step,[status(thm)],[t93,t96]) ).
cnf(t2,plain,
not(true) = false,
introduced(definition) ).
cnf(t118,plain,
not(true) = false,
inference(orient,[status(thm)],[t2]) ).
cnf(t461,plain,
true = or(false,or(not(true),not(has_immunity(sk2,sk5)))),
inference(step,[status(thm)],[t460,t118]) ).
cnf(t9,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t42,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t462,plain,
true = or(not(true),not(has_immunity(sk2,sk5))),
inference(step,[status(thm)],[t461,t42]) ).
cnf(t463,plain,
true = or(false,not(has_immunity(sk2,sk5))),
inference(step,[status(thm)],[t462,t118]) ).
cnf(t464,plain,
true = not(has_immunity(sk2,sk5)),
inference(step,[status(thm)],[t463,t42]) ).
cnf(t259,plain,
not(has_immunity(sk2,sk5)) = true,
inference(orient,[status(thm)],[t464]) ).
cnf(t260,plain,
false = ifeq(true,true,has_immunity(sk2,sk5),false),
inference(cp,[status(thm)],[t115,t259]) ).
cnf(t465,plain,
false = has_immunity(sk2,sk5),
inference(step,[status(thm)],[t260,t39]) ).
cnf(t261,plain,
has_immunity(sk2,sk5) = false,
inference(orient,[status(thm)],[t465]) ).
cnf(t274,plain,
true = or(false,greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))),
inference(cp,[status(thm)],[t273,t261]) ).
cnf(t473,plain,
true = greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)),
inference(step,[status(thm)],[t274,t42]) ).
cnf(t275,plain,
greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) = true,
inference(orient,[status(thm)],[t473]) ).
cnf(t474,plain,
ifeq(true,true,ifeq(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3),false,true),true) = true,
inference(step,[status(thm)],[t51,t275]) ).
cnf(t475,plain,
ifeq(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3),false,true) = true,
inference(step,[status(thm)],[t474,t39]) ).
cnf(t287,plain,
ifeq(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3),false,true) = true,
inference(rw,[status(thm)],[t475]) ).
cnf(t313,plain,
ifeq(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3),false,true) = true,
inference(orient,[status(thm)],[t287]) ).
cnf(f18,axiom,
( hazard_of_mortality(A,B) = hazard_of_mortality(A,C)
| ~ has_immunity(A,C)
| ~ has_immunity(A,B)
| ~ organization(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption_2_38) ).
fof(f18_nnf,plain,
! [A,B,C] :
( hazard_of_mortality(A,B) = hazard_of_mortality(A,C)
| ~ has_immunity(A,C)
| ~ has_immunity(A,B)
| ~ organization(A) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [A,B,C] :
( hazard_of_mortality(A,B) = hazard_of_mortality(A,C)
| ~ has_immunity(A,C)
| ~ has_immunity(A,B)
| ~ organization(A) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( hazard_of_mortality(X0,X1) = hazard_of_mortality(X0,X2)
| ~ has_immunity(X0,X2)
| ~ has_immunity(X0,X1)
| ~ organization(X0) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(t38,plain,
ifeq(organization(X1),true,ifeq(has_immunity(X1,X2),true,ifeq(has_immunity(X1,X3),true,hazard_of_mortality(X1,X2),hazard_of_mortality(X1,X3)),hazard_of_mortality(X1,X3)),hazard_of_mortality(X1,X3)) = hazard_of_mortality(X1,X3),
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t116,plain,
ifeq(organization(X1),true,ifeq(has_immunity(X1,X2),true,ifeq(has_immunity(X1,X3),true,hazard_of_mortality(X1,X2),hazard_of_mortality(X1,X3)),hazard_of_mortality(X1,X3)),hazard_of_mortality(X1,X3)) = hazard_of_mortality(X1,X3),
inference(orient,[status(thm)],[t38]) ).
cnf(t135,plain,
hazard_of_mortality(sk2,X1) = ifeq(organization(sk2),true,ifeq(true,true,ifeq(has_immunity(sk2,X1),true,hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,X1)),hazard_of_mortality(sk2,X1)),hazard_of_mortality(sk2,X1)),
inference(cp,[status(thm)],[t116,t133]) ).
cnf(t498,plain,
hazard_of_mortality(sk2,X1) = ifeq(true,true,ifeq(true,true,ifeq(has_immunity(sk2,X1),true,hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,X1)),hazard_of_mortality(sk2,X1)),hazard_of_mortality(sk2,X1)),
inference(step,[status(thm)],[t135,t104]) ).
cnf(t499,plain,
hazard_of_mortality(sk2,X1) = ifeq(true,true,ifeq(has_immunity(sk2,X1),true,hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,X1)),hazard_of_mortality(sk2,X1)),
inference(step,[status(thm)],[t498,t39]) ).
cnf(t500,plain,
hazard_of_mortality(sk2,X1) = ifeq(has_immunity(sk2,X1),true,hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,X1)),
inference(step,[status(thm)],[t499,t39]) ).
cnf(t363,plain,
ifeq(has_immunity(sk2,X1),true,hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,X1)) = hazard_of_mortality(sk2,X1),
inference(orient,[status(thm)],[t500]) ).
cnf(f22,negated_conjecture,
age(sk2,sk3) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_6_42) ).
fof(f22_nnf,plain,
age(sk2,sk3) = zero,
inference(nnf_transformation,[status(thm)],[f22]) ).
cnf(c22,plain,
age(sk2,sk3) = zero,
inference(cnf_transformation,[status(esa)],[f22_nnf]) ).
cnf(t4,plain,
age(sk2,sk3) = zero,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t120,plain,
age(sk2,sk3) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t122,plain,
true = ifeq(has_endowment(sk2),true,ifeq(smaller_or_equal(zero,eta),true,has_immunity(sk2,sk3),true),true),
inference(cp,[status(thm)],[t53,t120]) ).
cnf(t453,plain,
true = ifeq(true,true,ifeq(smaller_or_equal(zero,eta),true,has_immunity(sk2,sk3),true),true),
inference(step,[status(thm)],[t122,t96]) ).
cnf(t454,plain,
true = ifeq(smaller_or_equal(zero,eta),true,has_immunity(sk2,sk3),true),
inference(step,[status(thm)],[t453,t39]) ).
cnf(f1,axiom,
( smaller_or_equal(A,B)
| ~ smaller(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',definition_smaller_or_equal_2) ).
fof(f1_nnf,plain,
! [A,B] :
( smaller_or_equal(A,B)
| ~ smaller(A,B) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B] :
( smaller_or_equal(A,B)
| ~ smaller(A,B) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( smaller_or_equal(X0,X1)
| ~ smaller(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t22,plain,
ifeq(smaller(X1,X2),true,smaller_or_equal(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t61,plain,
ifeq(smaller(X1,X2),true,smaller_or_equal(X1,X2),true) = true,
inference(orient,[status(thm)],[t22]) ).
cnf(f7,axiom,
( smaller(B,A)
| ~ greater(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',definition_smaller_8) ).
fof(f7_nnf,plain,
! [A,B] :
( smaller(B,A)
| ~ greater(A,B) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A,B] :
( smaller(B,A)
| ~ greater(A,B) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( smaller(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t20,plain,
ifeq(greater(X1,X2),true,smaller(X2,X1),true) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t49,plain,
ifeq(greater(X1,X2),true,smaller(X2,X1),true) = true,
inference(orient,[status(thm)],[t20]) ).
cnf(f25,negated_conjecture,
greater(eta,zero),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_6_45) ).
fof(f25_nnf,plain,
greater(eta,zero),
inference(nnf_transformation,[status(thm)],[f25]) ).
cnf(c25,plain,
greater(eta,zero),
inference(cnf_transformation,[status(esa)],[f25_nnf]) ).
cnf(t6,plain,
greater(eta,zero) = true,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t63,plain,
greater(eta,zero) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(t66,plain,
true = ifeq(true,true,smaller(zero,eta),true),
inference(cp,[status(thm)],[t49,t63]) ).
cnf(t415,plain,
true = smaller(zero,eta),
inference(step,[status(thm)],[t66,t39]) ).
cnf(t130,plain,
smaller(zero,eta) = true,
inference(orient,[status(thm)],[t415]) ).
cnf(t131,plain,
true = ifeq(true,true,smaller_or_equal(zero,eta),true),
inference(cp,[status(thm)],[t61,t130]) ).
cnf(t419,plain,
true = smaller_or_equal(zero,eta),
inference(step,[status(thm)],[t131,t39]) ).
cnf(t140,plain,
smaller_or_equal(zero,eta) = true,
inference(orient,[status(thm)],[t419]) ).
cnf(t455,plain,
true = ifeq(true,true,has_immunity(sk2,sk3),true),
inference(step,[status(thm)],[t454,t140]) ).
cnf(t456,plain,
true = has_immunity(sk2,sk3),
inference(step,[status(thm)],[t455,t39]) ).
cnf(t240,plain,
has_immunity(sk2,sk3) = true,
inference(orient,[status(thm)],[t456]) ).
cnf(t365,plain,
hazard_of_mortality(sk2,sk3) = ifeq(true,true,hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3)),
inference(cp,[status(thm)],[t363,t240]) ).
cnf(t501,plain,
hazard_of_mortality(sk2,sk3) = hazard_of_mortality(sk2,sk4),
inference(step,[status(thm)],[t365,t39]) ).
cnf(t366,plain,
hazard_of_mortality(sk2,sk3) = hazard_of_mortality(sk2,sk4),
inference(orient,[status(thm)],[t501]) ).
cnf(t504,plain,
ifeq(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk4),false,true) = true,
inference(step,[status(thm)],[t313,t366]) ).
cnf(t505,plain,
false = true,
inference(step,[status(thm)],[t504,t39]) ).
cnf(t371,plain,
false = true,
inference(rw,[status(thm)],[t505]) ).
cnf(t373,plain,
false = true,
inference(orient,[status(thm)],[t371]) ).
cnf(f8,axiom,
( ~ greater(B,A)
| ~ greater(A,B) ),
file('/export/starexec/sandbox/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(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c8,c13,c26]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t373]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT057-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n005.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 01:15:33 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 1.93/1.50 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.93/1.50 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------