%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT043-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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n027.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:02:59 AM UTC 2026
% Result : Unsatisfiable 258.87s 216.19s
% Output : CNFRefutation 258.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 13
% Syntax : Number of formulae : 39 ( 19 unt; 0 typ; 0 def)
% Number of atoms : 95 ( 16 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 102 ( 46 ~; 56 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 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 : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-2 aty)
% Number of variables : 43 ( 43 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ smaller_or_equal > smaller > has_immunity > greater_or_equal > greater > organization > stock_of_knowledge > position > internal_friction > hazard_of_mortality > external_ties > capability > #nlpp > sk3 > sk2 > sk1
%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(sk2,type,
sk2: $i ).
tff(organization,type,
organization: $i > $o ).
tff(sk1,type,
sk1: $i ).
tff(position,type,
position: ( $i * $i ) > $i ).
tff(internal_friction,type,
internal_friction: ( $i * $i ) > $i ).
tff(smaller,type,
smaller: ( $i * $i ) > $o ).
tff(capability,type,
capability: ( $i * $i ) > $i ).
tff(stock_of_knowledge,type,
stock_of_knowledge: ( $i * $i ) > $i ).
tff(has_immunity,type,
has_immunity: ( $i * $i ) > $o ).
tff(sk3,type,
sk3: $i ).
tff(external_ties,type,
external_ties: ( $i * $i ) > $i ).
tff(greater_or_equal,type,
greater_or_equal: ( $i * $i ) > $o ).
tff(smaller_or_equal,type,
smaller_or_equal: ( $i * $i ) > $o ).
tff(f_213,axiom,
~ has_immunity(sk1,sk3),
file(unknown,unknown) ).
tff(f_211,axiom,
~ has_immunity(sk1,sk2),
file(unknown,unknown) ).
tff(f_218,axiom,
~ greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)),
file(unknown,unknown) ).
tff(f_216,axiom,
external_ties(sk1,sk2) = external_ties(sk1,sk3),
file(unknown,unknown) ).
tff(f_215,axiom,
greater(internal_friction(sk1,sk3),internal_friction(sk1,sk2)),
file(unknown,unknown) ).
tff(f_65,axiom,
! [A,B] :
( ( A != B )
| smaller_or_equal(A,B) ),
file(unknown,unknown) ).
tff(f_209,axiom,
organization(sk1),
file(unknown,unknown) ).
tff(f_214,axiom,
stock_of_knowledge(sk1,sk3) = stock_of_knowledge(sk1,sk2),
file(unknown,unknown) ).
tff(f_181,axiom,
! [A,B,C] :
( ~ organization(A)
| ~ smaller_or_equal(stock_of_knowledge(A,B),stock_of_knowledge(A,C))
| ~ greater(internal_friction(A,B),internal_friction(A,C))
| smaller(capability(A,B),capability(A,C)) ),
file(unknown,unknown) ).
tff(f_87,axiom,
! [A,B] :
( ~ smaller(A,B)
| greater(B,A) ),
file(unknown,unknown) ).
tff(f_82,axiom,
! [A,B] :
( ( A != B )
| greater_or_equal(A,B) ),
file(unknown,unknown) ).
tff(f_208,axiom,
! [A,B,C] :
( ~ organization(A)
| ( external_ties(A,B) != external_ties(A,C) )
| ( position(A,B) = position(A,C) ) ),
file(unknown,unknown) ).
tff(f_129,axiom,
! [A,B,C] :
( ~ organization(A)
| has_immunity(A,B)
| has_immunity(A,C)
| ~ greater(capability(A,C),capability(A,B))
| ~ greater_or_equal(position(A,C),position(A,B))
| smaller(hazard_of_mortality(A,C),hazard_of_mortality(A,B)) ),
file(unknown,unknown) ).
tff(c_44,plain,
~ has_immunity(sk1,sk3),
inference(cnfTransformation,[status(thm)],[f_213]) ).
tff(c_42,plain,
~ has_immunity(sk1,sk2),
inference(cnfTransformation,[status(thm)],[f_211]) ).
tff(c_52,plain,
~ greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)),
inference(cnfTransformation,[status(thm)],[f_218]) ).
tff(c_50,plain,
external_ties(sk1,sk3) = external_ties(sk1,sk2),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_48,plain,
greater(internal_friction(sk1,sk3),internal_friction(sk1,sk2)),
inference(cnfTransformation,[status(thm)],[f_215]) ).
tff(c_6,plain,
! [B_6] : smaller_or_equal(B_6,B_6),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_40,plain,
organization(sk1),
inference(cnfTransformation,[status(thm)],[f_209]) ).
tff(c_46,plain,
stock_of_knowledge(sk1,sk3) = stock_of_knowledge(sk1,sk2),
inference(cnfTransformation,[status(thm)],[f_214]) ).
tff(c_233820,plain,
! [A_32028,B_32029,C_32030] :
( smaller(capability(A_32028,B_32029),capability(A_32028,C_32030))
| ~ greater(internal_friction(A_32028,B_32029),internal_friction(A_32028,C_32030))
| ~ smaller_or_equal(stock_of_knowledge(A_32028,B_32029),stock_of_knowledge(A_32028,C_32030))
| ~ organization(A_32028) ),
inference(cnfTransformation,[status(thm)],[f_181]) ).
tff(c_233826,plain,
! [C_32030] :
( smaller(capability(sk1,sk3),capability(sk1,C_32030))
| ~ greater(internal_friction(sk1,sk3),internal_friction(sk1,C_32030))
| ~ smaller_or_equal(stock_of_knowledge(sk1,sk2),stock_of_knowledge(sk1,C_32030))
| ~ organization(sk1) ),
inference(superposition,[status(thm),theory(equality)],[c_46,c_233820]) ).
tff(c_1223691,plain,
! [C_166924] :
( smaller(capability(sk1,sk3),capability(sk1,C_166924))
| ~ greater(internal_friction(sk1,sk3),internal_friction(sk1,C_166924))
| ~ smaller_or_equal(stock_of_knowledge(sk1,sk2),stock_of_knowledge(sk1,C_166924)) ),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_233826]) ).
tff(c_1223805,plain,
( smaller(capability(sk1,sk3),capability(sk1,sk2))
| ~ greater(internal_friction(sk1,sk3),internal_friction(sk1,sk2)) ),
inference(resolution,[status(thm)],[c_6,c_1223691]) ).
tff(c_1223811,plain,
smaller(capability(sk1,sk3),capability(sk1,sk2)),
inference(demodulation,[status(thm),theory(equality)],[c_48,c_1223805]) ).
tff(c_14,plain,
! [B_14,A_13] :
( greater(B_14,A_13)
| ~ smaller(A_13,B_14) ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_1223945,plain,
greater(capability(sk1,sk2),capability(sk1,sk3)),
inference(resolution,[status(thm)],[c_1223811,c_14]) ).
tff(c_12,plain,
! [B_12] : greater_or_equal(B_12,B_12),
inference(cnfTransformation,[status(thm)],[f_82]) ).
tff(c_233287,plain,
! [A_31998,C_31999,B_32000] :
( ( position(A_31998,C_31999) = position(A_31998,B_32000) )
| ( external_ties(A_31998,C_31999) != external_ties(A_31998,B_32000) )
| ~ organization(A_31998) ),
inference(cnfTransformation,[status(thm)],[f_208]) ).
tff(c_233290,plain,
! [C_31999,B_32000] :
( ( position(sk1,C_31999) = position(sk1,B_32000) )
| ( external_ties(sk1,C_31999) != external_ties(sk1,B_32000) ) ),
inference(resolution,[status(thm)],[c_40,c_233287]) ).
tff(c_1212829,plain,
! [A_164559,C_164560,B_164561] :
( smaller(hazard_of_mortality(A_164559,C_164560),hazard_of_mortality(A_164559,B_164561))
| ~ greater_or_equal(position(A_164559,C_164560),position(A_164559,B_164561))
| ~ greater(capability(A_164559,C_164560),capability(A_164559,B_164561))
| has_immunity(A_164559,C_164560)
| has_immunity(A_164559,B_164561)
| ~ organization(A_164559) ),
inference(cnfTransformation,[status(thm)],[f_129]) ).
tff(c_1227625,plain,
! [A_167693,B_167694,C_167695] :
( greater(hazard_of_mortality(A_167693,B_167694),hazard_of_mortality(A_167693,C_167695))
| ~ greater_or_equal(position(A_167693,C_167695),position(A_167693,B_167694))
| ~ greater(capability(A_167693,C_167695),capability(A_167693,B_167694))
| has_immunity(A_167693,C_167695)
| has_immunity(A_167693,B_167694)
| ~ organization(A_167693) ),
inference(resolution,[status(thm)],[c_1212829,c_14]) ).
tff(c_1227688,plain,
! [B_167694,B_32000,C_31999] :
( greater(hazard_of_mortality(sk1,B_167694),hazard_of_mortality(sk1,B_32000))
| ~ greater_or_equal(position(sk1,C_31999),position(sk1,B_167694))
| ~ greater(capability(sk1,B_32000),capability(sk1,B_167694))
| has_immunity(sk1,B_32000)
| has_immunity(sk1,B_167694)
| ~ organization(sk1)
| ( external_ties(sk1,C_31999) != external_ties(sk1,B_32000) ) ),
inference(superposition,[status(thm),theory(equality)],[c_233290,c_1227625]) ).
tff(c_1371964,plain,
! [B_192952,B_192953,C_192954] :
( greater(hazard_of_mortality(sk1,B_192952),hazard_of_mortality(sk1,B_192953))
| ~ greater_or_equal(position(sk1,C_192954),position(sk1,B_192952))
| ~ greater(capability(sk1,B_192953),capability(sk1,B_192952))
| has_immunity(sk1,B_192953)
| has_immunity(sk1,B_192952)
| ( external_ties(sk1,C_192954) != external_ties(sk1,B_192953) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_1227688]) ).
tff(c_1483360,plain,
! [C_203631,B_203632] :
( greater(hazard_of_mortality(sk1,C_203631),hazard_of_mortality(sk1,B_203632))
| ~ greater(capability(sk1,B_203632),capability(sk1,C_203631))
| has_immunity(sk1,B_203632)
| has_immunity(sk1,C_203631)
| ( external_ties(sk1,C_203631) != external_ties(sk1,B_203632) ) ),
inference(resolution,[status(thm)],[c_12,c_1371964]) ).
tff(c_1484022,plain,
( greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2))
| has_immunity(sk1,sk2)
| has_immunity(sk1,sk3)
| ( external_ties(sk1,sk3) != external_ties(sk1,sk2) ) ),
inference(resolution,[status(thm)],[c_1223945,c_1483360]) ).
tff(c_1484388,plain,
( greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2))
| has_immunity(sk1,sk2)
| has_immunity(sk1,sk3) ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_1484022]) ).
tff(c_1484390,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_44,c_42,c_52,c_1484388]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT043-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.05 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.11/0.38 % Computer : n027.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 7 13:09:15 UTC 2026
% 0.03/0.38 % CPUTime :
% 258.87/216.19 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 258.94/216.20
% 258.94/216.20 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------