%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT008-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 : n019.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:49 AM UTC 2026
% Result : Unsatisfiable 4.06s 2.50s
% Output : CNFRefutation 4.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 15
% Syntax : Number of formulae : 47 ( 28 unt; 0 typ; 0 def)
% Number of atoms : 165 ( 0 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 242 ( 124 ~; 118 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 6 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 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 9 con; 0-2 aty)
% Number of variables : 89 ( 89 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ survival_chance > size > reorganization_free > inertia > class > organization > greater > sk1 > #nlpp > sk9 > sk8 > sk7 > sk6 > sk5 > sk4 > sk3 > sk2 > sk10
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(reorganization_free,type,
reorganization_free: ( $i * $i * $i ) > $o ).
tff(greater,type,
greater: ( $i * $i ) > $o ).
tff(size,type,
size: ( $i * $i * $i ) > $o ).
tff(sk9,type,
sk9: $i ).
tff(sk2,type,
sk2: $i ).
tff(sk6,type,
sk6: $i ).
tff(inertia,type,
inertia: ( $i * $i * $i ) > $o ).
tff(survival_chance,type,
survival_chance: ( $i * $i * $i ) > $o ).
tff(sk4,type,
sk4: $i ).
tff(sk8,type,
sk8: $i ).
tff(sk5,type,
sk5: $i ).
tff(sk3,type,
sk3: $i ).
tff(class,type,
class: ( $i * $i * $i ) > $o ).
tff(organization,type,
organization: ( $i * $i ) > $o ).
tff(sk10,type,
sk10: $i ).
tff(sk7,type,
sk7: $i ).
tff(sk1,type,
sk1: ( $i * $i ) > $i ).
tff(f_87,axiom,
organization(sk2,sk9),
file(unknown,unknown) ).
tff(f_91,axiom,
class(sk2,sk4,sk9),
file(unknown,unknown) ).
tff(f_95,axiom,
size(sk2,sk7,sk9),
file(unknown,unknown) ).
tff(f_28,axiom,
! [A,B] :
( ~ organization(A,B)
| inertia(A,sk1(B,A),B) ),
file(unknown,unknown) ).
tff(f_99,axiom,
~ greater(sk6,sk5),
file(unknown,unknown) ).
tff(f_89,axiom,
reorganization_free(sk2,sk9,sk9),
file(unknown,unknown) ).
tff(f_93,axiom,
survival_chance(sk2,sk5,sk9),
file(unknown,unknown) ).
tff(f_88,axiom,
organization(sk3,sk10),
file(unknown,unknown) ).
tff(f_90,axiom,
reorganization_free(sk3,sk10,sk10),
file(unknown,unknown) ).
tff(f_94,axiom,
survival_chance(sk3,sk6,sk10),
file(unknown,unknown) ).
tff(f_96,axiom,
size(sk3,sk8,sk10),
file(unknown,unknown) ).
tff(f_92,axiom,
class(sk3,sk4,sk10),
file(unknown,unknown) ).
tff(f_97,axiom,
greater(sk8,sk7),
file(unknown,unknown) ).
tff(f_57,axiom,
! [H,A,I,F,G,B,C,E,D] :
( ~ organization(A,B)
| ~ organization(C,D)
| ~ class(A,E,B)
| ~ class(C,E,D)
| ~ size(A,F,B)
| ~ size(C,G,D)
| ~ inertia(A,H,B)
| ~ inertia(C,I,D)
| ~ greater(G,F)
| greater(I,H) ),
file(unknown,unknown) ).
tff(f_86,axiom,
! [H,A,F,G,B,C,E,D] :
( ~ organization(A,B)
| ~ organization(C,D)
| ~ reorganization_free(A,B,B)
| ~ reorganization_free(C,D,D)
| ~ inertia(A,E,B)
| ~ inertia(C,F,D)
| ~ survival_chance(A,G,B)
| ~ survival_chance(C,H,D)
| ~ greater(F,E)
| greater(H,G) ),
file(unknown,unknown) ).
tff(c_8,plain,
organization(sk2,sk9),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_16,plain,
class(sk2,sk4,sk9),
inference(cnfTransformation,[status(thm)],[f_91]) ).
tff(c_24,plain,
size(sk2,sk7,sk9),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_2,plain,
! [A_1,B_2] :
( inertia(A_1,sk1(B_2,A_1),B_2)
| ~ organization(A_1,B_2) ),
inference(cnfTransformation,[status(thm)],[f_28]) ).
tff(c_30,plain,
~ greater(sk6,sk5),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_12,plain,
reorganization_free(sk2,sk9,sk9),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_20,plain,
survival_chance(sk2,sk5,sk9),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_10,plain,
organization(sk3,sk10),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_14,plain,
reorganization_free(sk3,sk10,sk10),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_22,plain,
survival_chance(sk3,sk6,sk10),
inference(cnfTransformation,[status(thm)],[f_94]) ).
tff(c_26,plain,
size(sk3,sk8,sk10),
inference(cnfTransformation,[status(thm)],[f_96]) ).
tff(c_18,plain,
class(sk3,sk4,sk10),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_28,plain,
greater(sk8,sk7),
inference(cnfTransformation,[status(thm)],[f_97]) ).
tff(c_47,plain,
! [C_39,D_44,B_38,H_41,F_36,G_37,I_40,E_42,A_43] :
( greater(I_40,H_41)
| ~ greater(G_37,F_36)
| ~ inertia(C_39,I_40,D_44)
| ~ inertia(A_43,H_41,B_38)
| ~ size(C_39,G_37,D_44)
| ~ size(A_43,F_36,B_38)
| ~ class(C_39,E_42,D_44)
| ~ class(A_43,E_42,B_38)
| ~ organization(C_39,D_44)
| ~ organization(A_43,B_38) ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_53,plain,
! [E_47,H_48,C_50,D_46,A_49,B_45,I_51] :
( greater(I_51,H_48)
| ~ inertia(C_50,I_51,D_46)
| ~ inertia(A_49,H_48,B_45)
| ~ size(C_50,sk8,D_46)
| ~ size(A_49,sk7,B_45)
| ~ class(C_50,E_47,D_46)
| ~ class(A_49,E_47,B_45)
| ~ organization(C_50,D_46)
| ~ organization(A_49,B_45) ),
inference(resolution,[status(thm)],[c_28,c_47]) ).
tff(c_57,plain,
! [A_57,E_55,H_52,B_53,A_56,B_54] :
( greater(sk1(B_54,A_57),H_52)
| ~ inertia(A_56,H_52,B_53)
| ~ size(A_57,sk8,B_54)
| ~ size(A_56,sk7,B_53)
| ~ class(A_57,E_55,B_54)
| ~ class(A_56,E_55,B_53)
| ~ organization(A_56,B_53)
| ~ organization(A_57,B_54) ),
inference(resolution,[status(thm)],[c_2,c_53]) ).
tff(c_61,plain,
! [B_59,A_61,B_62,A_60,E_58] :
( greater(sk1(B_62,A_61),sk1(B_59,A_60))
| ~ size(A_61,sk8,B_62)
| ~ size(A_60,sk7,B_59)
| ~ class(A_61,E_58,B_62)
| ~ class(A_60,E_58,B_59)
| ~ organization(A_61,B_62)
| ~ organization(A_60,B_59) ),
inference(resolution,[status(thm)],[c_2,c_57]) ).
tff(c_63,plain,
! [B_59,A_60] :
( greater(sk1(sk10,sk3),sk1(B_59,A_60))
| ~ size(sk3,sk8,sk10)
| ~ size(A_60,sk7,B_59)
| ~ class(A_60,sk4,B_59)
| ~ organization(sk3,sk10)
| ~ organization(A_60,B_59) ),
inference(resolution,[status(thm)],[c_18,c_61]) ).
tff(c_72,plain,
! [B_63,A_64] :
( greater(sk1(sk10,sk3),sk1(B_63,A_64))
| ~ size(A_64,sk7,B_63)
| ~ class(A_64,sk4,B_63)
| ~ organization(A_64,B_63) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_26,c_63]) ).
tff(c_6,plain,
! [B_16,H_12,A_13,E_18,D_19,F_14,G_15,C_17] :
( greater(H_12,G_15)
| ~ greater(F_14,E_18)
| ~ survival_chance(C_17,H_12,D_19)
| ~ survival_chance(A_13,G_15,B_16)
| ~ inertia(C_17,F_14,D_19)
| ~ inertia(A_13,E_18,B_16)
| ~ reorganization_free(C_17,D_19,D_19)
| ~ reorganization_free(A_13,B_16,B_16)
| ~ organization(C_17,D_19)
| ~ organization(A_13,B_16) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_89,plain,
! [C_89,A_95,G_93,A_92,H_96,D_94,B_91,B_90] :
( greater(H_96,G_93)
| ~ survival_chance(C_89,H_96,D_94)
| ~ survival_chance(A_92,G_93,B_90)
| ~ inertia(C_89,sk1(sk10,sk3),D_94)
| ~ inertia(A_92,sk1(B_91,A_95),B_90)
| ~ reorganization_free(C_89,D_94,D_94)
| ~ reorganization_free(A_92,B_90,B_90)
| ~ organization(C_89,D_94)
| ~ organization(A_92,B_90)
| ~ size(A_95,sk7,B_91)
| ~ class(A_95,sk4,B_91)
| ~ organization(A_95,B_91) ),
inference(resolution,[status(thm)],[c_72,c_6]) ).
tff(c_93,plain,
! [A_95,G_93,A_92,B_91,B_90] :
( greater(sk6,G_93)
| ~ survival_chance(A_92,G_93,B_90)
| ~ inertia(sk3,sk1(sk10,sk3),sk10)
| ~ inertia(A_92,sk1(B_91,A_95),B_90)
| ~ reorganization_free(sk3,sk10,sk10)
| ~ reorganization_free(A_92,B_90,B_90)
| ~ organization(sk3,sk10)
| ~ organization(A_92,B_90)
| ~ size(A_95,sk7,B_91)
| ~ class(A_95,sk4,B_91)
| ~ organization(A_95,B_91) ),
inference(resolution,[status(thm)],[c_22,c_89]) ).
tff(c_99,plain,
! [A_95,G_93,A_92,B_91,B_90] :
( greater(sk6,G_93)
| ~ survival_chance(A_92,G_93,B_90)
| ~ inertia(sk3,sk1(sk10,sk3),sk10)
| ~ inertia(A_92,sk1(B_91,A_95),B_90)
| ~ reorganization_free(A_92,B_90,B_90)
| ~ organization(A_92,B_90)
| ~ size(A_95,sk7,B_91)
| ~ class(A_95,sk4,B_91)
| ~ organization(A_95,B_91) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_14,c_93]) ).
tff(c_101,plain,
~ inertia(sk3,sk1(sk10,sk3),sk10),
inference(splitLeft,[status(thm)],[c_99]) ).
tff(c_104,plain,
~ organization(sk3,sk10),
inference(resolution,[status(thm)],[c_2,c_101]) ).
tff(c_108,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10,c_104]) ).
tff(c_131,plain,
! [B_98,G_97,A_101,B_99,A_100] :
( greater(sk6,G_97)
| ~ survival_chance(A_101,G_97,B_99)
| ~ inertia(A_101,sk1(B_98,A_100),B_99)
| ~ reorganization_free(A_101,B_99,B_99)
| ~ organization(A_101,B_99)
| ~ size(A_100,sk7,B_98)
| ~ class(A_100,sk4,B_98)
| ~ organization(A_100,B_98) ),
inference(splitRight,[status(thm)],[c_99]) ).
tff(c_133,plain,
! [B_98,A_100] :
( greater(sk6,sk5)
| ~ inertia(sk2,sk1(B_98,A_100),sk9)
| ~ reorganization_free(sk2,sk9,sk9)
| ~ organization(sk2,sk9)
| ~ size(A_100,sk7,B_98)
| ~ class(A_100,sk4,B_98)
| ~ organization(A_100,B_98) ),
inference(resolution,[status(thm)],[c_20,c_131]) ).
tff(c_138,plain,
! [B_98,A_100] :
( greater(sk6,sk5)
| ~ inertia(sk2,sk1(B_98,A_100),sk9)
| ~ size(A_100,sk7,B_98)
| ~ class(A_100,sk4,B_98)
| ~ organization(A_100,B_98) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_12,c_133]) ).
tff(c_143,plain,
! [B_102,A_103] :
( ~ inertia(sk2,sk1(B_102,A_103),sk9)
| ~ size(A_103,sk7,B_102)
| ~ class(A_103,sk4,B_102)
| ~ organization(A_103,B_102) ),
inference(negUnitSimplification,[status(thm)],[c_30,c_138]) ).
tff(c_147,plain,
( ~ size(sk2,sk7,sk9)
| ~ class(sk2,sk4,sk9)
| ~ organization(sk2,sk9) ),
inference(resolution,[status(thm)],[c_2,c_143]) ).
tff(c_151,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_16,c_24,c_147]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT008-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/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.10/0.37 % Computer : n019.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 : Mon Sep 7 11:46:07 UTC 2026
% 0.10/0.37 % CPUTime :
% 4.06/2.50 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.06/2.51
% 4.06/2.51 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------