%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT056-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n026.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:03:02 AM UTC 2026
% Result : Unsatisfiable 6.08s 3.19s
% Output : CNFRefutation 6.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 16
% Syntax : Number of formulae : 92 ( 48 unt; 0 typ; 0 def)
% Number of atoms : 170 ( 27 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 172 ( 94 ~; 78 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 63 ( 63 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ smaller_or_equal > smaller > has_immunity > greater_or_equal > greater > organization > has_endowment > hazard_of_mortality > age > #nlpp > sk1 > zero > sk5 > sk4 > sk3 > sk2 > sigma > eta
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(hazard_of_mortality,type,
hazard_of_mortality: ( $i * $i ) > $i ).
tff(greater,type,
greater: ( $i * $i ) > $o ).
tff(sk1,type,
sk1: $i > $i ).
tff(sk2,type,
sk2: $i ).
tff(organization,type,
organization: $i > $o ).
tff(has_endowment,type,
has_endowment: $i > $o ).
tff(eta,type,
eta: $i ).
tff(smaller,type,
smaller: ( $i * $i ) > $o ).
tff(sk4,type,
sk4: $i ).
tff(sk5,type,
sk5: $i ).
tff(sigma,type,
sigma: $i ).
tff(age,type,
age: ( $i * $i ) > $i ).
tff(has_immunity,type,
has_immunity: ( $i * $i ) > $o ).
tff(sk3,type,
sk3: $i ).
tff(greater_or_equal,type,
greater_or_equal: ( $i * $i ) > $o ).
tff(zero,type,
zero: $i ).
tff(smaller_or_equal,type,
smaller_or_equal: ( $i * $i ) > $o ).
tff(f_197,axiom,
has_endowment(sk2),
file(unknown,unknown) ).
tff(f_200,axiom,
greater(age(sk2,sk5),eta),
file(unknown,unknown) ).
tff(f_136,axiom,
! [A,B] :
( ~ has_endowment(A)
| ~ greater(age(A,B),eta)
| ~ has_immunity(A,B) ),
file(unknown,unknown) ).
tff(f_196,axiom,
organization(sk2),
file(unknown,unknown) ).
tff(f_201,axiom,
greater_or_equal(eta,sigma),
file(unknown,unknown) ).
tff(f_72,axiom,
! [A,B] :
( ~ greater_or_equal(A,B)
| greater(A,B)
| ( A = B ) ),
file(unknown,unknown) ).
tff(f_202,axiom,
greater(sigma,zero),
file(unknown,unknown) ).
tff(f_106,axiom,
! [A,B,C] :
( ~ greater(A,B)
| ~ greater(B,C)
| greater(A,C) ),
file(unknown,unknown) ).
tff(f_92,axiom,
! [A,B] :
( ~ greater(A,B)
| smaller(B,A) ),
file(unknown,unknown) ).
tff(f_60,axiom,
! [A,B] :
( ~ smaller(A,B)
| smaller_or_equal(A,B) ),
file(unknown,unknown) ).
tff(f_198,axiom,
age(sk2,sk3) = zero,
file(unknown,unknown) ).
tff(f_127,axiom,
! [A,B] :
( ~ has_endowment(A)
| ~ smaller_or_equal(age(A,B),eta)
| has_immunity(A,B) ),
file(unknown,unknown) ).
tff(f_195,axiom,
! [A,B,C] :
( ~ organization(A)
| ~ has_immunity(A,B)
| has_immunity(A,C)
| greater(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ),
file(unknown,unknown) ).
tff(f_199,axiom,
smaller_or_equal(age(sk2,sk4),eta),
file(unknown,unknown) ).
tff(f_185,axiom,
! [A,B,C] :
( ~ organization(A)
| ~ has_immunity(A,B)
| ~ has_immunity(A,C)
| ( hazard_of_mortality(A,B) = hazard_of_mortality(A,C) ) ),
file(unknown,unknown) ).
tff(f_207,axiom,
( ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))
| ( hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) ) ),
file(unknown,unknown) ).
tff(c_44,plain,
has_endowment(sk2),
inference(cnfTransformation,[status(thm)],[f_197]) ).
tff(c_50,plain,
greater(age(sk2,sk5),eta),
inference(cnfTransformation,[status(thm)],[f_200]) ).
tff(c_1016,plain,
! [A_120,B_121] :
( ~ has_immunity(A_120,B_121)
| ~ greater(age(A_120,B_121),eta)
| ~ has_endowment(A_120) ),
inference(cnfTransformation,[status(thm)],[f_136]) ).
tff(c_1019,plain,
( ~ has_immunity(sk2,sk5)
| ~ has_endowment(sk2) ),
inference(resolution,[status(thm)],[c_50,c_1016]) ).
tff(c_1025,plain,
~ has_immunity(sk2,sk5),
inference(demodulation,[status(thm),theory(equality)],[c_44,c_1019]) ).
tff(c_42,plain,
organization(sk2),
inference(cnfTransformation,[status(thm)],[f_196]) ).
tff(c_278,plain,
! [A_71,B_72] :
( ~ has_immunity(A_71,B_72)
| ~ greater(age(A_71,B_72),eta)
| ~ has_endowment(A_71) ),
inference(cnfTransformation,[status(thm)],[f_136]) ).
tff(c_287,plain,
( ~ has_immunity(sk2,sk5)
| ~ has_endowment(sk2) ),
inference(resolution,[status(thm)],[c_50,c_278]) ).
tff(c_295,plain,
~ has_immunity(sk2,sk5),
inference(demodulation,[status(thm),theory(equality)],[c_44,c_287]) ).
tff(c_52,plain,
greater_or_equal(eta,sigma),
inference(cnfTransformation,[status(thm)],[f_201]) ).
tff(c_93,plain,
! [B_54,A_55] :
( ( B_54 = A_55 )
| greater(A_55,B_54)
| ~ greater_or_equal(A_55,B_54) ),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_104,plain,
( ( sigma = eta )
| greater(eta,sigma) ),
inference(resolution,[status(thm)],[c_52,c_93]) ).
tff(c_112,plain,
greater(eta,sigma),
inference(splitLeft,[status(thm)],[c_104]) ).
tff(c_54,plain,
greater(sigma,zero),
inference(cnfTransformation,[status(thm)],[f_202]) ).
tff(c_161,plain,
! [A_60,C_61,B_62] :
( greater(A_60,C_61)
| ~ greater(B_62,C_61)
| ~ greater(A_60,B_62) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_255,plain,
! [A_70] :
( greater(A_70,zero)
| ~ greater(A_70,sigma) ),
inference(resolution,[status(thm)],[c_54,c_161]) ).
tff(c_16,plain,
! [B_16,A_15] :
( smaller(B_16,A_15)
| ~ greater(A_15,B_16) ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_4,plain,
! [A_3,B_4] :
( smaller_or_equal(A_3,B_4)
| ~ smaller(A_3,B_4) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_46,plain,
age(sk2,sk3) = zero,
inference(cnfTransformation,[status(thm)],[f_198]) ).
tff(c_177,plain,
! [A_63,B_64] :
( has_immunity(A_63,B_64)
| ~ smaller_or_equal(age(A_63,B_64),eta)
| ~ has_endowment(A_63) ),
inference(cnfTransformation,[status(thm)],[f_127]) ).
tff(c_186,plain,
( has_immunity(sk2,sk3)
| ~ smaller_or_equal(zero,eta)
| ~ has_endowment(sk2) ),
inference(superposition,[status(thm),theory(equality)],[c_46,c_177]) ).
tff(c_192,plain,
( has_immunity(sk2,sk3)
| ~ smaller_or_equal(zero,eta) ),
inference(demodulation,[status(thm),theory(equality)],[c_44,c_186]) ).
tff(c_193,plain,
~ smaller_or_equal(zero,eta),
inference(splitLeft,[status(thm)],[c_192]) ).
tff(c_197,plain,
~ smaller(zero,eta),
inference(resolution,[status(thm)],[c_4,c_193]) ).
tff(c_225,plain,
~ greater(eta,zero),
inference(resolution,[status(thm)],[c_16,c_197]) ).
tff(c_258,plain,
~ greater(eta,sigma),
inference(resolution,[status(thm)],[c_255,c_225]) ).
tff(c_266,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_112,c_258]) ).
tff(c_267,plain,
has_immunity(sk2,sk3),
inference(splitRight,[status(thm)],[c_192]) ).
tff(c_40,plain,
! [A_36,C_38,B_37] :
( greater(hazard_of_mortality(A_36,C_38),hazard_of_mortality(A_36,B_37))
| has_immunity(A_36,C_38)
| ~ has_immunity(A_36,B_37)
| ~ organization(A_36) ),
inference(cnfTransformation,[status(thm)],[f_195]) ).
tff(c_48,plain,
smaller_or_equal(age(sk2,sk4),eta),
inference(cnfTransformation,[status(thm)],[f_199]) ).
tff(c_183,plain,
( has_immunity(sk2,sk4)
| ~ has_endowment(sk2) ),
inference(resolution,[status(thm)],[c_48,c_177]) ).
tff(c_190,plain,
has_immunity(sk2,sk4),
inference(demodulation,[status(thm),theory(equality)],[c_44,c_183]) ).
tff(c_561,plain,
! [A_86,C_87,B_88] :
( ( hazard_of_mortality(A_86,C_87) = hazard_of_mortality(A_86,B_88) )
| ~ has_immunity(A_86,C_87)
| ~ has_immunity(A_86,B_88)
| ~ organization(A_86) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_565,plain,
! [B_88] :
( ( hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,B_88) )
| ~ has_immunity(sk2,B_88)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[c_190,c_561]) ).
tff(c_595,plain,
! [B_90] :
( ( hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,B_90) )
| ~ has_immunity(sk2,B_90) ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_565]) ).
tff(c_602,plain,
hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3),
inference(resolution,[status(thm)],[c_267,c_595]) ).
tff(c_56,plain,
( ( hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) )
| ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)) ),
inference(cnfTransformation,[status(thm)],[f_207]) ).
tff(c_312,plain,
~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)),
inference(splitLeft,[status(thm)],[c_56]) ).
tff(c_606,plain,
~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk3)),
inference(demodulation,[status(thm),theory(equality)],[c_602,c_312]) ).
tff(c_633,plain,
( has_immunity(sk2,sk5)
| ~ has_immunity(sk2,sk3)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[c_40,c_606]) ).
tff(c_642,plain,
has_immunity(sk2,sk5),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_267,c_633]) ).
tff(c_644,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_295,c_642]) ).
tff(c_645,plain,
hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3),
inference(splitRight,[status(thm)],[c_56]) ).
tff(c_649,plain,
! [A_94,C_95,B_96] :
( ( hazard_of_mortality(A_94,C_95) = hazard_of_mortality(A_94,B_96) )
| ~ has_immunity(A_94,C_95)
| ~ has_immunity(A_94,B_96)
| ~ organization(A_94) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_653,plain,
! [B_96] :
( ( hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,B_96) )
| ~ has_immunity(sk2,B_96)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[c_190,c_649]) ).
tff(c_948,plain,
! [B_114] :
( ( hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,B_114) )
| ~ has_immunity(sk2,B_114) ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_653]) ).
tff(c_951,plain,
hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3),
inference(resolution,[status(thm)],[c_267,c_948]) ).
tff(c_958,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_645,c_951]) ).
tff(c_959,plain,
sigma = eta,
inference(splitRight,[status(thm)],[c_104]) ).
tff(c_963,plain,
greater(eta,zero),
inference(demodulation,[status(thm),theory(equality)],[c_959,c_54]) ).
tff(c_980,plain,
! [A_118,B_119] :
( has_immunity(A_118,B_119)
| ~ smaller_or_equal(age(A_118,B_119),eta)
| ~ has_endowment(A_118) ),
inference(cnfTransformation,[status(thm)],[f_127]) ).
tff(c_989,plain,
( has_immunity(sk2,sk3)
| ~ smaller_or_equal(zero,eta)
| ~ has_endowment(sk2) ),
inference(superposition,[status(thm),theory(equality)],[c_46,c_980]) ).
tff(c_995,plain,
( has_immunity(sk2,sk3)
| ~ smaller_or_equal(zero,eta) ),
inference(demodulation,[status(thm),theory(equality)],[c_44,c_989]) ).
tff(c_996,plain,
~ smaller_or_equal(zero,eta),
inference(splitLeft,[status(thm)],[c_995]) ).
tff(c_1000,plain,
~ smaller(zero,eta),
inference(resolution,[status(thm)],[c_4,c_996]) ).
tff(c_1006,plain,
~ greater(eta,zero),
inference(resolution,[status(thm)],[c_16,c_1000]) ).
tff(c_1013,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_963,c_1006]) ).
tff(c_1014,plain,
has_immunity(sk2,sk3),
inference(splitRight,[status(thm)],[c_995]) ).
tff(c_1236,plain,
! [A_135,C_136,B_137] :
( greater(hazard_of_mortality(A_135,C_136),hazard_of_mortality(A_135,B_137))
| has_immunity(A_135,C_136)
| ~ has_immunity(A_135,B_137)
| ~ organization(A_135) ),
inference(cnfTransformation,[status(thm)],[f_195]) ).
tff(c_986,plain,
( has_immunity(sk2,sk4)
| ~ has_endowment(sk2) ),
inference(resolution,[status(thm)],[c_48,c_980]) ).
tff(c_993,plain,
has_immunity(sk2,sk4),
inference(demodulation,[status(thm),theory(equality)],[c_44,c_986]) ).
tff(c_1202,plain,
! [A_131,C_132,B_133] :
( ( hazard_of_mortality(A_131,C_132) = hazard_of_mortality(A_131,B_133) )
| ~ has_immunity(A_131,C_132)
| ~ has_immunity(A_131,B_133)
| ~ organization(A_131) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_1204,plain,
! [B_133] :
( ( hazard_of_mortality(sk2,sk3) = hazard_of_mortality(sk2,B_133) )
| ~ has_immunity(sk2,B_133)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[c_1014,c_1202]) ).
tff(c_1213,plain,
! [B_134] :
( ( hazard_of_mortality(sk2,sk3) = hazard_of_mortality(sk2,B_134) )
| ~ has_immunity(sk2,B_134) ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_1204]) ).
tff(c_1222,plain,
hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3),
inference(resolution,[status(thm)],[c_993,c_1213]) ).
tff(c_1032,plain,
~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)),
inference(splitLeft,[status(thm)],[c_56]) ).
tff(c_1223,plain,
~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk3)),
inference(demodulation,[status(thm),theory(equality)],[c_1222,c_1032]) ).
tff(c_1239,plain,
( has_immunity(sk2,sk5)
| ~ has_immunity(sk2,sk3)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[c_1236,c_1223]) ).
tff(c_1252,plain,
has_immunity(sk2,sk5),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_1014,c_1239]) ).
tff(c_1254,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1025,c_1252]) ).
tff(c_1255,plain,
hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3),
inference(splitRight,[status(thm)],[c_56]) ).
tff(c_1467,plain,
! [A_150,C_151,B_152] :
( ( hazard_of_mortality(A_150,C_151) = hazard_of_mortality(A_150,B_152) )
| ~ has_immunity(A_150,C_151)
| ~ has_immunity(A_150,B_152)
| ~ organization(A_150) ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_1469,plain,
! [B_152] :
( ( hazard_of_mortality(sk2,sk3) = hazard_of_mortality(sk2,B_152) )
| ~ has_immunity(sk2,B_152)
| ~ organization(sk2) ),
inference(resolution,[status(thm)],[c_1014,c_1467]) ).
tff(c_1478,plain,
! [B_153] :
( ( hazard_of_mortality(sk2,sk3) = hazard_of_mortality(sk2,B_153) )
| ~ has_immunity(sk2,B_153) ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_1469]) ).
tff(c_1484,plain,
hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3),
inference(resolution,[status(thm)],[c_993,c_1478]) ).
tff(c_1490,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1255,c_1484]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT056-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.04 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.11/0.37 % Computer : n026.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 7 13:31:27 UTC 2026
% 0.11/0.37 % CPUTime :
% 6.08/3.19 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.25/3.21
% 6.25/3.21 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------