%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : MGT064-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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:03:03 AM UTC 2026
% Result : Unsatisfiable 22.58s 3.72s
% Output : CNFRefutation 22.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 32
% Syntax : Number of formulae : 144 ( 53 unt; 0 def)
% Number of atoms : 304 ( 63 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 301 ( 141 ~; 160 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 125 ( 7 sgn 44 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(theorem_10_74,axiom,
organization(sk3),
file('theBenchmark.p',theorem_10_74) ).
cnf(c_5,plain,
organization(sk3),
inference(clausify,[status(thm)],[theorem_10_74]) ).
fof(assumption_17_66,axiom,
! [VAR_0,VAR_1] :
( hazard_of_mortality(VAR_0,VAR_1) = mod2
| positional_advantage(VAR_0,VAR_1)
| ~ is_aligned(VAR_0,VAR_1)
| has_immunity(VAR_0,VAR_1)
| ~ organization(VAR_0) ),
file('theBenchmark.p',assumption_17_66) ).
cnf(c_6,plain,
( hazard_of_mortality(A,B) = mod2
| positional_advantage(A,B)
| ~ is_aligned(A,B)
| has_immunity(A,B)
| ~ organization(A) ),
inference(clausify,[status(thm)],[assumption_17_66]) ).
fof(assumption_17_65,axiom,
! [VAR_0,VAR_1] :
( hazard_of_mortality(VAR_0,VAR_1) = mod1
| ~ positional_advantage(VAR_0,VAR_1)
| is_aligned(VAR_0,VAR_1)
| has_immunity(VAR_0,VAR_1)
| ~ organization(VAR_0) ),
file('theBenchmark.p',assumption_17_65) ).
cnf(c_7,plain,
( hazard_of_mortality(A,B) = mod1
| ~ positional_advantage(A,B)
| is_aligned(A,B)
| has_immunity(A,B)
| ~ organization(A) ),
inference(clausify,[status(thm)],[assumption_17_65]) ).
fof(assumption_17_64,axiom,
! [VAR_0,VAR_1] :
( hazard_of_mortality(VAR_0,VAR_1) = low
| ~ positional_advantage(VAR_0,VAR_1)
| ~ is_aligned(VAR_0,VAR_1)
| has_immunity(VAR_0,VAR_1)
| ~ organization(VAR_0) ),
file('theBenchmark.p',assumption_17_64) ).
cnf(c_8,plain,
( hazard_of_mortality(A,B) = low
| ~ positional_advantage(A,B)
| ~ is_aligned(A,B)
| has_immunity(A,B)
| ~ organization(A) ),
inference(clausify,[status(thm)],[assumption_17_64]) ).
fof(assumption_15_56,axiom,
! [VAR_0,VAR_1,VAR_2] :
( greater(age(VAR_0,VAR_2),sigma)
| ~ dissimilar(VAR_0,VAR_1,VAR_2)
| age(VAR_0,VAR_1) != zero
| ~ organization(VAR_0) ),
file('theBenchmark.p',assumption_15_56) ).
cnf(c_10,plain,
( greater(age(A,C),sigma)
| ~ dissimilar(A,B,C)
| age(A,B) != zero
| ~ organization(A) ),
inference(clausify,[status(thm)],[assumption_15_56]) ).
fof(assumption_15_55,axiom,
! [VAR_0,VAR_1,VAR_2] :
( dissimilar(VAR_0,VAR_1,VAR_2)
| ~ greater(age(VAR_0,VAR_2),sigma)
| age(VAR_0,VAR_1) != zero
| ~ organization(VAR_0) ),
file('theBenchmark.p',assumption_15_55) ).
cnf(c_11,plain,
( dissimilar(A,B,C)
| ~ greater(age(A,C),sigma)
| age(A,B) != zero
| ~ organization(A) ),
inference(clausify,[status(thm)],[assumption_15_55]) ).
fof(assumption_13_54,axiom,
! [VAR_0,VAR_1] :
( is_aligned(VAR_0,VAR_1)
| age(VAR_0,VAR_1) != zero
| ~ organization(VAR_0) ),
file('theBenchmark.p',assumption_13_54) ).
cnf(c_12,plain,
( is_aligned(A,B)
| age(A,B) != zero
| ~ organization(A) ),
inference(clausify,[status(thm)],[assumption_13_54]) ).
fof(definition_2_51,axiom,
! [VAR_0,VAR_1,VAR_2] :
( dissimilar(VAR_0,VAR_1,VAR_2)
| is_aligned(VAR_0,VAR_2)
| ~ is_aligned(VAR_0,VAR_1)
| ~ organization(VAR_0) ),
file('theBenchmark.p',definition_2_51) ).
cnf(c_15,plain,
( dissimilar(A,B,C)
| is_aligned(A,C)
| ~ is_aligned(A,B)
| ~ organization(A) ),
inference(clausify,[status(thm)],[definition_2_51]) ).
fof(definition_2_47,axiom,
! [VAR_0,VAR_1,VAR_2] :
( organization(VAR_0)
| ~ dissimilar(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',definition_2_47) ).
cnf(c_17,plain,
( organization(A)
| ~ dissimilar(A,B,C) ),
inference(clausify,[status(thm)],[definition_2_47]) ).
fof(assumption_1_46,axiom,
! [VAR_0,VAR_1] :
( ~ has_immunity(VAR_0,VAR_1)
| has_endowment(VAR_0)
| ~ organization(VAR_0) ),
file('theBenchmark.p',assumption_1_46) ).
cnf(c_18,plain,
( ~ has_immunity(A,B)
| has_endowment(A)
| ~ organization(A) ),
inference(clausify,[status(thm)],[assumption_1_46]) ).
fof(definition_4_58,axiom,
! [VAR_0,VAR_1] :
( positional_advantage(VAR_0,VAR_1)
| ~ greater(age(VAR_0,VAR_1),tau)
| ~ robust_position(VAR_0) ),
file('theBenchmark.p',definition_4_58) ).
cnf(c_25,plain,
( positional_advantage(A,B)
| ~ greater(age(A,B),tau)
| ~ robust_position(A) ),
inference(clausify,[status(thm)],[definition_4_58]) ).
fof(definition_4_57,axiom,
! [VAR_0,VAR_1] :
( ~ positional_advantage(VAR_0,VAR_1)
| ~ smaller_or_equal(age(VAR_0,VAR_1),tau)
| ~ robust_position(VAR_0) ),
file('theBenchmark.p',definition_4_57) ).
cnf(c_26,plain,
( ~ positional_advantage(A,B)
| ~ smaller_or_equal(age(A,B),tau)
| ~ robust_position(A) ),
inference(clausify,[status(thm)],[definition_4_57]) ).
fof(theorem_10_75,axiom,
robust_position(sk3),
file('theBenchmark.p',theorem_10_75) ).
cnf(c_30,plain,
robust_position(sk3),
inference(clausify,[status(thm)],[theorem_10_75]) ).
cnf(c_31,plain,
( ~ positional_advantage(sk3,A)
| ~ smaller_or_equal(age(sk3,A),tau) ),
inference(resolve,[status(thm)],[c_30,c_26]) ).
cnf(c_32,plain,
( positional_advantage(sk3,A)
| ~ greater(age(sk3,A),tau) ),
inference(resolve,[status(thm)],[c_30,c_25]) ).
fof(theorem_10_85,axiom,
( hazard_of_mortality(sk3,sk5) != hazard_of_mortality(sk3,sk4)
| ~ smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))
| ~ smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7)) ),
file('theBenchmark.p',theorem_10_85) ).
cnf(c_39,plain,
( hazard_of_mortality(sk3,sk5) != hazard_of_mortality(sk3,sk4)
| ~ smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))
| ~ smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7)) ),
inference(clausify,[status(thm)],[theorem_10_85]) ).
fof(theorem_10_84,axiom,
greater(age(sk3,sk7),sigma),
file('theBenchmark.p',theorem_10_84) ).
cnf(c_40,plain,
greater(age(sk3,sk7),sigma),
inference(clausify,[status(thm)],[theorem_10_84]) ).
fof(theorem_10_83,axiom,
smaller_or_equal(age(sk3,sk6),sigma),
file('theBenchmark.p',theorem_10_83) ).
cnf(c_41,plain,
smaller_or_equal(age(sk3,sk6),sigma),
inference(clausify,[status(thm)],[theorem_10_83]) ).
fof(theorem_10_82,axiom,
greater(age(sk3,sk6),tau),
file('theBenchmark.p',theorem_10_82) ).
cnf(c_42,plain,
greater(age(sk3,sk6),tau),
inference(clausify,[status(thm)],[theorem_10_82]) ).
fof(theorem_10_81,axiom,
smaller_or_equal(age(sk3,sk5),tau),
file('theBenchmark.p',theorem_10_81) ).
cnf(c_43,plain,
smaller_or_equal(age(sk3,sk5),tau),
inference(clausify,[status(thm)],[theorem_10_81]) ).
fof(theorem_10_80,axiom,
greater(sigma,tau),
file('theBenchmark.p',theorem_10_80) ).
cnf(c_44,plain,
greater(sigma,tau),
inference(clausify,[status(thm)],[theorem_10_80]) ).
fof(theorem_10_79,axiom,
greater(tau,zero),
file('theBenchmark.p',theorem_10_79) ).
cnf(c_45,plain,
greater(tau,zero),
inference(clausify,[status(thm)],[theorem_10_79]) ).
fof(theorem_10_77,axiom,
age(sk3,sk4) = zero,
file('theBenchmark.p',theorem_10_77) ).
cnf(c_47,plain,
age(sk3,sk4) = zero,
inference(clausify,[status(thm)],[theorem_10_77]) ).
fof(theorem_10_76,axiom,
~ has_endowment(sk3),
file('theBenchmark.p',theorem_10_76) ).
cnf(c_48,plain,
~ has_endowment(sk3),
inference(clausify,[status(thm)],[theorem_10_76]) ).
fof(assumption_19_73,axiom,
greater(mod2,mod1),
file('theBenchmark.p',assumption_19_73) ).
cnf(c_49,plain,
greater(mod2,mod1),
inference(clausify,[status(thm)],[assumption_19_73]) ).
fof(assumption_18b_69,axiom,
greater(mod1,low),
file('theBenchmark.p',assumption_18b_69) ).
cnf(c_53,plain,
greater(mod1,low),
inference(clausify,[status(thm)],[assumption_18b_69]) ).
fof(definition_2_49,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ is_aligned(VAR_0,VAR_2)
| ~ is_aligned(VAR_0,VAR_1)
| ~ dissimilar(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',definition_2_49) ).
cnf(c_55,plain,
( ~ is_aligned(A,C)
| ~ is_aligned(A,B)
| ~ dissimilar(A,B,C) ),
inference(clausify,[status(thm)],[definition_2_49]) ).
fof(meaning_postulate_greater_comparable_11,axiom,
! [VAR_0,VAR_1] :
( greater(VAR_0,VAR_1)
| VAR_0 = VAR_1
| smaller(VAR_0,VAR_1) ),
file('theBenchmark.p',meaning_postulate_greater_comparable_11) ).
cnf(c_59,plain,
( greater(A,B)
| A = B
| smaller(A,B) ),
inference(clausify,[status(thm)],[meaning_postulate_greater_comparable_11]) ).
fof(meaning_postulate_greater_transitive_10,axiom,
! [VAR_0,VAR_1,VAR_2] :
( greater(VAR_0,VAR_2)
| ~ greater(VAR_1,VAR_2)
| ~ greater(VAR_0,VAR_1) ),
file('theBenchmark.p',meaning_postulate_greater_transitive_10) ).
cnf(c_60,plain,
( greater(A,C)
| ~ greater(B,C)
| ~ greater(A,B) ),
inference(clausify,[status(thm)],[meaning_postulate_greater_transitive_10]) ).
fof(meaning_postulate_greater_strict_9,axiom,
! [VAR_0,VAR_1] :
( ~ greater(VAR_1,VAR_0)
| ~ greater(VAR_0,VAR_1) ),
file('theBenchmark.p',meaning_postulate_greater_strict_9) ).
cnf(c_61,plain,
( ~ greater(B,A)
| ~ greater(A,B) ),
inference(clausify,[status(thm)],[meaning_postulate_greater_strict_9]) ).
fof(definition_smaller_8,axiom,
! [VAR_0,VAR_1] :
( smaller(VAR_1,VAR_0)
| ~ greater(VAR_0,VAR_1) ),
file('theBenchmark.p',definition_smaller_8) ).
cnf(c_62,plain,
( smaller(B,A)
| ~ greater(A,B) ),
inference(clausify,[status(thm)],[definition_smaller_8]) ).
fof(definition_smaller_7,axiom,
! [VAR_0,VAR_1] :
( greater(VAR_1,VAR_0)
| ~ smaller(VAR_0,VAR_1) ),
file('theBenchmark.p',definition_smaller_7) ).
cnf(c_63,plain,
( greater(B,A)
| ~ smaller(A,B) ),
inference(clausify,[status(thm)],[definition_smaller_7]) ).
fof(definition_smaller_or_equal_2,axiom,
! [VAR_0,VAR_1] :
( smaller_or_equal(VAR_0,VAR_1)
| ~ smaller(VAR_0,VAR_1) ),
file('theBenchmark.p',definition_smaller_or_equal_2) ).
cnf(c_65,plain,
( smaller_or_equal(A,B)
| ~ smaller(A,B) ),
inference(clausify,[status(thm)],[definition_smaller_or_equal_2]) ).
fof(definition_smaller_or_equal_1,axiom,
! [VAR_0,VAR_1] :
( VAR_0 = VAR_1
| smaller(VAR_0,VAR_1)
| ~ smaller_or_equal(VAR_0,VAR_1) ),
file('theBenchmark.p',definition_smaller_or_equal_1) ).
cnf(c_66,plain,
( A = B
| smaller(A,B)
| ~ smaller_or_equal(A,B) ),
inference(clausify,[status(thm)],[definition_smaller_or_equal_1]) ).
cnf(c_68,plain,
( hazard_of_mortality(sk3,A) = mod2
| positional_advantage(sk3,A)
| ~ is_aligned(sk3,A)
| has_immunity(sk3,A) ),
inference(resolve,[status(thm)],[c_6,c_5]) ).
cnf(c_69,plain,
( hazard_of_mortality(sk3,A) = mod1
| ~ positional_advantage(sk3,A)
| is_aligned(sk3,A)
| has_immunity(sk3,A) ),
inference(resolve,[status(thm)],[c_7,c_5]) ).
cnf(c_70,plain,
( hazard_of_mortality(sk3,A) = low
| ~ positional_advantage(sk3,A)
| ~ is_aligned(sk3,A)
| has_immunity(sk3,A) ),
inference(resolve,[status(thm)],[c_8,c_5]) ).
cnf(c_73,plain,
( dissimilar(sk3,A,B)
| ~ greater(age(sk3,B),sigma)
| age(sk3,A) != zero ),
inference(resolve,[status(thm)],[c_11,c_5]) ).
cnf(c_74,plain,
( is_aligned(sk3,A)
| age(sk3,A) != zero ),
inference(resolve,[status(thm)],[c_12,c_5]) ).
cnf(c_76,plain,
( dissimilar(sk3,A,B)
| is_aligned(sk3,B)
| ~ is_aligned(sk3,A) ),
inference(resolve,[status(thm)],[c_15,c_5]) ).
cnf(c_81,plain,
( greater(age(A,E),sigma)
| ~ dissimilar(A,D,E)
| age(A,D) != zero
| ~ dissimilar(A,B,C) ),
inference(resolve,[status(thm)],[c_17,c_10]) ).
cnf(c_88,plain,
( ~ has_immunity(sk3,A)
| has_endowment(sk3) ),
inference(resolve,[status(thm)],[c_18,c_5]) ).
cnf(c_89,plain,
~ has_immunity(sk3,A),
inference(resolve,[status(thm)],[c_48,c_88]) ).
cnf(c_106,plain,
~ greater(A,A),
inference(factor,[status(thm)],[c_61]) ).
cnf(c_107,plain,
( greater(age(A,C),sigma)
| age(A,B) != zero
| ~ dissimilar(A,B,C) ),
inference(factor,[status(thm)],[c_81]) ).
cnf(c_108,plain,
( hazard_of_mortality(sk3,A) = low
| ~ positional_advantage(sk3,A)
| ~ is_aligned(sk3,A) ),
inference(resolve,[status(thm)],[c_89,c_70]) ).
cnf(c_109,plain,
( hazard_of_mortality(sk3,A) = mod1
| ~ positional_advantage(sk3,A)
| is_aligned(sk3,A) ),
inference(resolve,[status(thm)],[c_89,c_69]) ).
cnf(c_110,plain,
( hazard_of_mortality(sk3,A) = mod2
| positional_advantage(sk3,A)
| ~ is_aligned(sk3,A) ),
inference(resolve,[status(thm)],[c_89,c_68]) ).
cnf(c_114,plain,
positional_advantage(sk3,sk6),
inference(resolve,[status(thm)],[c_42,c_32]) ).
cnf(c_118,plain,
~ positional_advantage(sk3,sk5),
inference(resolve,[status(thm)],[c_43,c_31]) ).
cnf(c_119,plain,
( ~ positional_advantage(sk3,sk4)
| ~ smaller_or_equal(zero,tau) ),
inference(paramod,[status(thm)],[c_47,c_31]) ).
cnf(c_132,plain,
( greater(age(sk3,sk7),A)
| ~ greater(sigma,A) ),
inference(resolve,[status(thm)],[c_60,c_40]) ).
cnf(c_134,plain,
( greater(A,low)
| ~ greater(A,mod1) ),
inference(resolve,[status(thm)],[c_60,c_53]) ).
cnf(c_156,plain,
smaller(low,mod1),
inference(resolve,[status(thm)],[c_62,c_53]) ).
cnf(c_160,plain,
smaller(mod1,mod2),
inference(resolve,[status(thm)],[c_62,c_49]) ).
cnf(c_162,plain,
smaller(zero,tau),
inference(resolve,[status(thm)],[c_62,c_45]) ).
cnf(c_166,plain,
( greater(B,A)
| B = A
| greater(A,B) ),
inference(resolve,[status(thm)],[c_63,c_59]) ).
cnf(c_171,plain,
( age(sk3,sk6) = sigma
| smaller(age(sk3,sk6),sigma) ),
inference(resolve,[status(thm)],[c_66,c_41]) ).
cnf(c_172,plain,
( dissimilar(sk3,A,sk7)
| age(sk3,A) != zero ),
inference(resolve,[status(thm)],[c_73,c_40]) ).
cnf(c_173,plain,
is_aligned(sk3,sk4),
inference(resolve,[status(thm)],[c_74,c_47]) ).
cnf(c_175,plain,
~ smaller(A,A),
inference(resolve,[status(thm)],[c_63,c_106]) ).
cnf(c_178,plain,
( hazard_of_mortality(sk3,sk6) = low
| ~ is_aligned(sk3,sk6) ),
inference(resolve,[status(thm)],[c_114,c_108]) ).
cnf(c_181,plain,
~ greater(age(sk3,sk5),tau),
inference(resolve,[status(thm)],[c_32,c_118]) ).
cnf(c_200,plain,
smaller_or_equal(zero,tau),
inference(resolve,[status(thm)],[c_162,c_65]) ).
cnf(c_201,plain,
~ positional_advantage(sk3,sk4),
inference(resolve,[status(thm)],[c_200,c_119]) ).
cnf(c_7006,plain,
( hazard_of_mortality(sk3,sk4) = mod2
| positional_advantage(sk3,sk4) ),
inference(resolve,[status(thm)],[c_173,c_110]) ).
cnf(c_208,plain,
hazard_of_mortality(sk3,sk4) = mod2,
inference(resolve,[status(thm)],[c_201,c_7006]) ).
cnf(c_209,plain,
( dissimilar(sk3,sk4,A)
| is_aligned(sk3,A) ),
inference(resolve,[status(thm)],[c_173,c_76]) ).
cnf(c_214,plain,
( hazard_of_mortality(sk3,sk5) != mod2
| ~ smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))
| ~ smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7)) ),
inference(paramod,[status(thm)],[c_208,c_39]) ).
cnf(c_7007,plain,
( greater(A,tau)
| ~ greater(A,sigma) ),
inference(resolve,[status(thm)],[c_60,c_44]) ).
cnf(c_245,plain,
~ greater(age(sk3,sk5),sigma),
inference(resolve,[status(thm)],[c_7007,c_181]) ).
cnf(c_7008,plain,
( greater(age(sk3,A),sigma)
| ~ dissimilar(sk3,sk4,A) ),
inference(resolve,[status(thm)],[c_107,c_47]) ).
cnf(c_254,plain,
~ dissimilar(sk3,sk4,sk5),
inference(resolve,[status(thm)],[c_7008,c_245]) ).
cnf(c_263,plain,
greater(age(sk3,sk7),tau),
inference(resolve,[status(thm)],[c_132,c_44]) ).
cnf(c_274,plain,
positional_advantage(sk3,sk7),
inference(resolve,[status(thm)],[c_263,c_32]) ).
cnf(c_275,plain,
( hazard_of_mortality(sk3,sk7) = mod1
| is_aligned(sk3,sk7) ),
inference(resolve,[status(thm)],[c_274,c_109]) ).
cnf(c_301,plain,
( greater(A,low)
| greater(mod1,A)
| mod1 = A ),
inference(resolve,[status(thm)],[c_166,c_134]) ).
cnf(c_324,plain,
is_aligned(sk3,sk5),
inference(resolve,[status(thm)],[c_209,c_254]) ).
cnf(c_7009,plain,
( greater(age(sk3,A),sigma)
| age(sk3,sk4) != zero
| is_aligned(sk3,A) ),
inference(resolve,[status(thm)],[c_209,c_107]) ).
cnf(c_7010,plain,
( greater(age(sk3,A),sigma)
| zero != zero
| is_aligned(sk3,A) ),
inference(paramod,[status(thm)],[c_47,c_7009]) ).
cnf(c_325,plain,
( greater(age(sk3,A),sigma)
| is_aligned(sk3,A) ),
inference(copy,[status(thm)],[c_7010]) ).
cnf(c_7011,plain,
( hazard_of_mortality(sk3,sk5) = mod2
| positional_advantage(sk3,sk5) ),
inference(resolve,[status(thm)],[c_324,c_110]) ).
cnf(c_326,plain,
hazard_of_mortality(sk3,sk5) = mod2,
inference(resolve,[status(thm)],[c_118,c_7011]) ).
cnf(c_7012,plain,
( hazard_of_mortality(sk3,sk5) != mod2
| ~ smaller(hazard_of_mortality(sk3,sk7),mod2)
| ~ smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7)) ),
inference(paramod,[status(thm)],[c_326,c_214]) ).
cnf(c_7013,plain,
( mod2 != mod2
| ~ smaller(hazard_of_mortality(sk3,sk7),mod2)
| ~ smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7)) ),
inference(paramod,[status(thm)],[c_326,c_7012]) ).
cnf(c_331,plain,
( ~ smaller(hazard_of_mortality(sk3,sk7),mod2)
| ~ smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7)) ),
inference(copy,[status(thm)],[c_7013]) ).
cnf(c_346,plain,
( greater(sigma,age(sk3,sk6))
| age(sk3,sk6) = sigma ),
inference(resolve,[status(thm)],[c_171,c_63]) ).
cnf(c_352,plain,
dissimilar(sk3,sk4,sk7),
inference(resolve,[status(thm)],[c_172,c_47]) ).
cnf(c_7014,plain,
( ~ is_aligned(sk3,sk7)
| ~ is_aligned(sk3,sk4) ),
inference(resolve,[status(thm)],[c_352,c_55]) ).
cnf(c_353,plain,
~ is_aligned(sk3,sk7),
inference(resolve,[status(thm)],[c_173,c_7014]) ).
cnf(c_354,plain,
hazard_of_mortality(sk3,sk7) = mod1,
inference(resolve,[status(thm)],[c_353,c_275]) ).
cnf(c_7015,plain,
( ~ smaller(hazard_of_mortality(sk3,sk7),mod2)
| ~ smaller(hazard_of_mortality(sk3,sk6),mod1) ),
inference(paramod,[status(thm)],[c_354,c_331]) ).
cnf(c_7016,plain,
( ~ smaller(mod1,mod2)
| ~ smaller(hazard_of_mortality(sk3,sk6),mod1) ),
inference(paramod,[status(thm)],[c_354,c_7015]) ).
cnf(c_357,plain,
~ smaller(hazard_of_mortality(sk3,sk6),mod1),
inference(resolve,[status(thm)],[c_160,c_7016]) ).
cnf(c_358,plain,
( hazard_of_mortality(sk3,sk6) = low
| greater(age(sk3,sk6),sigma) ),
inference(resolve,[status(thm)],[c_325,c_178]) ).
cnf(c_388,plain,
~ greater(mod1,hazard_of_mortality(sk3,sk6)),
inference(resolve,[status(thm)],[c_62,c_357]) ).
cnf(c_7017,plain,
( greater(hazard_of_mortality(sk3,sk6),low)
| mod1 = hazard_of_mortality(sk3,sk6) ),
inference(resolve,[status(thm)],[c_301,c_388]) ).
cnf(c_711,plain,
( greater(hazard_of_mortality(sk3,sk6),low)
| hazard_of_mortality(sk3,sk6) = mod1 ),
inference(copy,[status(thm)],[c_7017]) ).
cnf(c_1787,plain,
( ~ greater(age(sk3,sk6),sigma)
| age(sk3,sk6) = sigma ),
inference(resolve,[status(thm)],[c_346,c_61]) ).
cnf(c_1896,plain,
( smaller(sigma,age(sk3,sk6))
| hazard_of_mortality(sk3,sk6) = low ),
inference(resolve,[status(thm)],[c_358,c_62]) ).
cnf(c_6228,plain,
( smaller(low,hazard_of_mortality(sk3,sk6))
| hazard_of_mortality(sk3,sk6) = mod1 ),
inference(resolve,[status(thm)],[c_711,c_62]) ).
cnf(c_6418,plain,
( hazard_of_mortality(sk3,sk6) = low
| age(sk3,sk6) = sigma ),
inference(resolve,[status(thm)],[c_1787,c_358]) ).
cnf(c_7018,plain,
( ~ smaller(low,mod1)
| age(sk3,sk6) = sigma ),
inference(paramod,[status(thm)],[c_6418,c_357]) ).
cnf(c_6451,plain,
age(sk3,sk6) = sigma,
inference(resolve,[status(thm)],[c_156,c_7018]) ).
cnf(c_7019,plain,
( smaller(sigma,sigma)
| hazard_of_mortality(sk3,sk6) = low ),
inference(paramod,[status(thm)],[c_6451,c_1896]) ).
cnf(c_6732,plain,
hazard_of_mortality(sk3,sk6) = low,
inference(resolve,[status(thm)],[c_175,c_7019]) ).
cnf(c_7020,plain,
( smaller(low,hazard_of_mortality(sk3,sk6))
| low = mod1 ),
inference(paramod,[status(thm)],[c_6732,c_6228]) ).
cnf(c_7021,plain,
( smaller(low,low)
| low = mod1 ),
inference(paramod,[status(thm)],[c_6732,c_7020]) ).
cnf(c_7022,plain,
( smaller(low,low)
| mod1 = low ),
inference(copy,[status(thm)],[c_7021]) ).
cnf(c_6737,plain,
mod1 = low,
inference(resolve,[status(thm)],[c_175,c_7022]) ).
cnf(c_7023,plain,
smaller(low,low),
inference(paramod,[status(thm)],[c_6737,c_156]) ).
cnf(c_7005,plain,
$false,
inference(resolve,[status(thm)],[c_175,c_7023]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT064-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n001.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sat Sep 26 00:16:41 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.44 % Process 401239 was started by sandbox2 on n001,
% 0.17/0.44 % Sat Sep 26 00:16:41 2026
% 0.17/0.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.44
% 0.17/0.44 % From the command line: assign(max_seconds, 300).
% 22.58/3.72
% 22.58/3.72 % given #500 (T,wt=9): 859 very_low = A | greater(A,very_low) | smaller(A,low). [resolve(311,c,62,a)].
% 22.58/3.72
% 22.58/3.72 % given #1000 (T,wt=9): 2474 very_low = tau | greater(sigma,very_low) | smaller(zero,mod2). [resolve(903,c,62,a)].
% 22.58/3.72
% 22.58/3.72 % given #1500 (T,wt=9): 5781 low = tau | greater(sigma,very_low) | smaller_or_equal(tau,mod2). [resolve(3769,c,65,a)].
% 22.58/3.72
% 22.58/3.72 % SZS status Unsatisfiable for theBenchmark
% 22.58/3.72
% 22.58/3.72 % Proof 1 at 2.44 (+ 0.79) seconds.
% 22.58/3.72 % Length of proof is 94.
% 22.58/3.72 % Level of proof is 14.
% 22.58/3.72 % Maximum clause weight is 21.000.
% 22.58/3.72 % Given clauses 1543.
% 22.58/3.72
% 22.58/3.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------