%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT005+2 : TPTP v9.3.0. Bugfixed v3.2.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 : n012.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:48 AM UTC 2026
% Result : Theorem 11.07s 4.22s
% Output : CNFRefutation 11.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 9
% Syntax : Number of formulae : 114 ( 50 unt; 0 typ; 0 def)
% Number of atoms : 517 ( 13 equ)
% Maximal formula atoms : 23 ( 4 avg)
% Number of connectives : 735 ( 332 ~; 332 |; 61 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 35 ( 7 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 : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 13 con; 0-8 aty)
% Number of variables : 248 ( 247 !; 1 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ survival_chance > reorganization_type > reorganization_free > reorganization > complexity > class > organization > greater > #nlpp > #skF_17 > #skF_3 > #skF_4 > #skF_11 > #skF_15 > #skF_7 > #skF_10 > #skF_16 > #skF_14 > #skF_5 > #skF_6 > #skF_13 > #skF_9 > #skF_8 > #skF_2 > #skF_1 > #skF_12
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(reorganization_free,type,
reorganization_free: ( $i * $i * $i ) > $o ).
tff(greater,type,
greater: ( $i * $i ) > $o ).
tff('#skF_17',type,
'#skF_17': $i ).
tff('#skF_3',type,
'#skF_3': ( $i * $i * $i * $i * $i * $i * $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i * $i * $i * $i * $i * $i * $i ) > $i ).
tff('#skF_11',type,
'#skF_11': $i ).
tff('#skF_15',type,
'#skF_15': $i ).
tff(complexity,type,
complexity: ( $i * $i * $i ) > $o ).
tff(reorganization,type,
reorganization: ( $i * $i * $i ) > $o ).
tff('#skF_7',type,
'#skF_7': $i ).
tff('#skF_10',type,
'#skF_10': $i ).
tff('#skF_16',type,
'#skF_16': $i ).
tff('#skF_14',type,
'#skF_14': $i ).
tff('#skF_5',type,
'#skF_5': $i ).
tff('#skF_6',type,
'#skF_6': $i ).
tff('#skF_13',type,
'#skF_13': $i ).
tff(survival_chance,type,
survival_chance: ( $i * $i * $i ) > $o ).
tff(reorganization_type,type,
reorganization_type: ( $i * $i * $i ) > $o ).
tff('#skF_9',type,
'#skF_9': $i ).
tff('#skF_8',type,
'#skF_8': $i ).
tff(class,type,
class: ( $i * $i * $i ) > $o ).
tff(organization,type,
organization: ( $i * $i ) > $o ).
tff('#skF_2',type,
'#skF_2': ( $i * $i * $i * $i * $i * $i * $i * $i ) > $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff('#skF_12',type,
'#skF_12': $i ).
tff(f_253,negated_conjecture,
~ ! [X,Y,Re,C,P,P1,P2,C1,C2,T,Ta,Tb,Tc] :
( ( organization(X,Ta)
& organization(Y,Ta)
& organization(X,Tc)
& organization(Y,Tc)
& class(X,C,Ta)
& class(Y,C,Ta)
& survival_chance(X,P,Ta)
& survival_chance(Y,P,Ta)
& reorganization(X,Ta,Tb)
& reorganization(Y,Ta,Tc)
& reorganization_type(X,Re,Ta)
& reorganization_type(Y,Re,Ta)
& reorganization_free(X,Tb,Tc)
& survival_chance(X,P1,T)
& survival_chance(Y,P2,T)
& complexity(X,C1,Ta)
& complexity(Y,C2,Ta)
& greater(C2,C1)
& ( ( T = Tc )
=> greater(P1,P2) ) )
=> ( ( T = Tb )
=> ( greater(P1,P2)
| ( P1 = P2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL) ).
tff(f_75,axiom,
! [X,Ta,Tb] :
( reorganization(X,Ta,Tb)
=> greater(Tb,Ta) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp7) ).
tff(f_89,hypothesis,
! [X,P1,P2,T1,T2] :
( ( organization(X,T1)
& organization(X,T2)
& reorganization_free(X,T1,T2)
& survival_chance(X,P1,T1)
& survival_chance(X,P2,T2)
& greater(T2,T1) )
=> greater(P2,P1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_FOL) ).
tff(f_35,axiom,
! [X,Y] :
~ ( greater(X,Y)
& ( X = Y ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp6_1) ).
tff(f_61,axiom,
! [X,T] :
( organization(X,T)
=> ? [P] : survival_chance(X,P,T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp12) ).
tff(f_110,hypothesis,
! [X,P1,P2,T1,T2,Ta,Tb] :
( ( organization(X,T1)
& organization(X,T2)
& reorganization(X,Ta,Tb)
& survival_chance(X,P1,T1)
& survival_chance(X,P2,T2)
& ~ greater(Ta,T1)
& greater(T2,T1)
& ~ greater(T2,Tb) )
=> greater(P1,P2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_FOL) ).
tff(f_71,axiom,
! [X,T,T1,T2] :
( ( organization(X,T1)
& organization(X,T2)
& greater(T,T1)
& greater(T2,T) )
=> organization(X,T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp13) ).
tff(f_137,hypothesis,
! [X,Y,Re,C,C1,C2,Ta,Tb,Tc] :
( ( organization(X,Ta)
& organization(Y,Ta)
& organization(Y,Tc)
& class(X,C,Ta)
& class(Y,C,Ta)
& reorganization(X,Ta,Tb)
& reorganization(Y,Ta,Tc)
& reorganization_type(X,Re,Ta)
& reorganization_type(Y,Re,Ta)
& complexity(X,C1,Ta)
& complexity(Y,C2,Ta)
& greater(C2,C1) )
=> greater(Tc,Tb) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a10_FOL) ).
tff(f_176,hypothesis,
! [X,Y,Re,C,P,P1,P2,C1,C2,Ta,Tb,Tc] :
( ( organization(X,Ta)
& organization(Y,Ta)
& organization(X,Tb)
& organization(Y,Tb)
& class(X,C,Ta)
& class(Y,C,Ta)
& survival_chance(X,P,Ta)
& survival_chance(Y,P,Ta)
& reorganization(X,Ta,Tb)
& reorganization(Y,Ta,Tc)
& reorganization_type(X,Re,Ta)
& reorganization_type(Y,Re,Ta)
& survival_chance(X,P1,Tb)
& survival_chance(Y,P2,Tb)
& complexity(X,C1,Ta)
& complexity(Y,C2,Ta)
& greater(C2,C1) )
=> ( greater(P1,P2)
| ( P1 = P2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a11_FOL) ).
tff(c_62,plain,
survival_chance('#skF_6','#skF_9','#skF_15'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_64,plain,
survival_chance('#skF_5','#skF_9','#skF_15'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_66,plain,
class('#skF_6','#skF_8','#skF_15'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_68,plain,
class('#skF_5','#skF_8','#skF_15'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_76,plain,
organization('#skF_5','#skF_15'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_74,plain,
organization('#skF_6','#skF_15'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_38,plain,
'#skF_16' = '#skF_14',
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_60,plain,
reorganization('#skF_5','#skF_15','#skF_16'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_78,plain,
reorganization('#skF_5','#skF_15','#skF_14'),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_60]) ).
tff(c_54,plain,
reorganization_type('#skF_6','#skF_7','#skF_15'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_46,plain,
complexity('#skF_5','#skF_12','#skF_15'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_44,plain,
complexity('#skF_6','#skF_13','#skF_15'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_56,plain,
reorganization_type('#skF_5','#skF_7','#skF_15'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_36,plain,
~ greater('#skF_10','#skF_11'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_34,plain,
'#skF_11' != '#skF_10',
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_89,plain,
! [Tb_70,Ta_71,X_72] :
( greater(Tb_70,Ta_71)
| ~ reorganization(X_72,Ta_71,Tb_70) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_97,plain,
greater('#skF_14','#skF_15'),
inference(resolution,[status(thm)],[c_78,c_89]) ).
tff(c_50,plain,
survival_chance('#skF_5','#skF_10','#skF_14'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_223,plain,
! [T2_102,P2_104,P1_106,T1_103,X_105] :
( greater(P2_104,P1_106)
| ~ greater(T2_102,T1_103)
| ~ survival_chance(X_105,P2_104,T2_102)
| ~ survival_chance(X_105,P1_106,T1_103)
| ~ reorganization_free(X_105,T1_103,T2_102)
| ~ organization(X_105,T2_102)
| ~ organization(X_105,T1_103) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_235,plain,
! [P1_106,T1_103] :
( greater('#skF_10',P1_106)
| ~ greater('#skF_14',T1_103)
| ~ survival_chance('#skF_5',P1_106,T1_103)
| ~ reorganization_free('#skF_5',T1_103,'#skF_14')
| ~ organization('#skF_5','#skF_14')
| ~ organization('#skF_5',T1_103) ),
inference(resolution,[status(thm)],[c_50,c_223]) ).
tff(c_5469,plain,
~ organization('#skF_5','#skF_14'),
inference(splitLeft,[status(thm)],[c_235]) ).
tff(c_72,plain,
organization('#skF_5','#skF_17'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_2,plain,
! [Y_2] : ~ greater(Y_2,Y_2),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_10,plain,
! [X_13,T_14] :
( survival_chance(X_13,'#skF_1'(X_13,T_14),T_14)
| ~ organization(X_13,T_14) ),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_58,plain,
reorganization('#skF_6','#skF_15','#skF_17'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_96,plain,
greater('#skF_17','#skF_15'),
inference(resolution,[status(thm)],[c_58,c_89]) ).
tff(c_316,plain,
! [P2_117,T1_122,Ta_116,T2_121,Tb_119,P1_118,X_120] :
( greater(P1_118,P2_117)
| greater(T2_121,Tb_119)
| ~ greater(T2_121,T1_122)
| greater(Ta_116,T1_122)
| ~ survival_chance(X_120,P2_117,T2_121)
| ~ survival_chance(X_120,P1_118,T1_122)
| ~ reorganization(X_120,Ta_116,Tb_119)
| ~ organization(X_120,T2_121)
| ~ organization(X_120,T1_122) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_7682,plain,
! [P2_1086,Ta_1087,X_1085,Tb_1084,P1_1083] :
( greater(P1_1083,P2_1086)
| greater('#skF_17',Tb_1084)
| greater(Ta_1087,'#skF_15')
| ~ survival_chance(X_1085,P2_1086,'#skF_17')
| ~ survival_chance(X_1085,P1_1083,'#skF_15')
| ~ reorganization(X_1085,Ta_1087,Tb_1084)
| ~ organization(X_1085,'#skF_17')
| ~ organization(X_1085,'#skF_15') ),
inference(resolution,[status(thm)],[c_96,c_316]) ).
tff(c_7687,plain,
! [P1_1088,X_1089,Tb_1090,Ta_1091] :
( greater(P1_1088,'#skF_1'(X_1089,'#skF_17'))
| greater('#skF_17',Tb_1090)
| greater(Ta_1091,'#skF_15')
| ~ survival_chance(X_1089,P1_1088,'#skF_15')
| ~ reorganization(X_1089,Ta_1091,Tb_1090)
| ~ organization(X_1089,'#skF_15')
| ~ organization(X_1089,'#skF_17') ),
inference(resolution,[status(thm)],[c_10,c_7682]) ).
tff(c_7691,plain,
! [P1_1088] :
( greater(P1_1088,'#skF_1'('#skF_5','#skF_17'))
| greater('#skF_17','#skF_14')
| greater('#skF_15','#skF_15')
| ~ survival_chance('#skF_5',P1_1088,'#skF_15')
| ~ organization('#skF_5','#skF_15')
| ~ organization('#skF_5','#skF_17') ),
inference(resolution,[status(thm)],[c_78,c_7687]) ).
tff(c_7698,plain,
! [P1_1088] :
( greater(P1_1088,'#skF_1'('#skF_5','#skF_17'))
| greater('#skF_17','#skF_14')
| greater('#skF_15','#skF_15')
| ~ survival_chance('#skF_5',P1_1088,'#skF_15') ),
inference(demodulation,[status(thm),theory(equality)],[c_72,c_76,c_7691]) ).
tff(c_7699,plain,
! [P1_1088] :
( greater(P1_1088,'#skF_1'('#skF_5','#skF_17'))
| greater('#skF_17','#skF_14')
| ~ survival_chance('#skF_5',P1_1088,'#skF_15') ),
inference(negUnitSimplification,[status(thm)],[c_2,c_7698]) ).
tff(c_7947,plain,
greater('#skF_17','#skF_14'),
inference(splitLeft,[status(thm)],[c_7699]) ).
tff(c_12,plain,
! [X_16,T_17,T2_19,T1_18] :
( organization(X_16,T_17)
| ~ greater(T2_19,T_17)
| ~ greater(T_17,T1_18)
| ~ organization(X_16,T2_19)
| ~ organization(X_16,T1_18) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_8114,plain,
! [X_1139,T1_1140] :
( organization(X_1139,'#skF_14')
| ~ greater('#skF_14',T1_1140)
| ~ organization(X_1139,'#skF_17')
| ~ organization(X_1139,T1_1140) ),
inference(resolution,[status(thm)],[c_7947,c_12]) ).
tff(c_8116,plain,
! [T1_1140] :
( organization('#skF_5','#skF_14')
| ~ greater('#skF_14',T1_1140)
| ~ organization('#skF_5',T1_1140) ),
inference(resolution,[status(thm)],[c_72,c_8114]) ).
tff(c_8124,plain,
! [T1_1141] :
( ~ greater('#skF_14',T1_1141)
| ~ organization('#skF_5',T1_1141) ),
inference(negUnitSimplification,[status(thm)],[c_5469,c_8116]) ).
tff(c_8127,plain,
~ greater('#skF_14','#skF_15'),
inference(resolution,[status(thm)],[c_76,c_8124]) ).
tff(c_8134,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_97,c_8127]) ).
tff(c_8136,plain,
~ greater('#skF_17','#skF_14'),
inference(splitRight,[status(thm)],[c_7699]) ).
tff(c_70,plain,
organization('#skF_6','#skF_17'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_42,plain,
greater('#skF_13','#skF_12'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_6173,plain,
! [C1_880,C_885,Y_884,X_883,Tc_882,Ta_879,C2_886,Tb_887,Re_881] :
( greater(Tc_882,Tb_887)
| ~ greater(C2_886,C1_880)
| ~ complexity(Y_884,C2_886,Ta_879)
| ~ complexity(X_883,C1_880,Ta_879)
| ~ reorganization_type(Y_884,Re_881,Ta_879)
| ~ reorganization_type(X_883,Re_881,Ta_879)
| ~ reorganization(Y_884,Ta_879,Tc_882)
| ~ reorganization(X_883,Ta_879,Tb_887)
| ~ class(Y_884,C_885,Ta_879)
| ~ class(X_883,C_885,Ta_879)
| ~ organization(Y_884,Tc_882)
| ~ organization(Y_884,Ta_879)
| ~ organization(X_883,Ta_879) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_7144,plain,
! [C_971,Ta_972,Re_969,Tb_970,Tc_967,X_966,Y_968] :
( greater(Tc_967,Tb_970)
| ~ complexity(Y_968,'#skF_13',Ta_972)
| ~ complexity(X_966,'#skF_12',Ta_972)
| ~ reorganization_type(Y_968,Re_969,Ta_972)
| ~ reorganization_type(X_966,Re_969,Ta_972)
| ~ reorganization(Y_968,Ta_972,Tc_967)
| ~ reorganization(X_966,Ta_972,Tb_970)
| ~ class(Y_968,C_971,Ta_972)
| ~ class(X_966,C_971,Ta_972)
| ~ organization(Y_968,Tc_967)
| ~ organization(Y_968,Ta_972)
| ~ organization(X_966,Ta_972) ),
inference(resolution,[status(thm)],[c_42,c_6173]) ).
tff(c_7146,plain,
! [Tc_967,Tb_970,X_966,C_971] :
( greater(Tc_967,Tb_970)
| ~ complexity('#skF_6','#skF_13','#skF_15')
| ~ complexity(X_966,'#skF_12','#skF_15')
| ~ reorganization_type(X_966,'#skF_7','#skF_15')
| ~ reorganization('#skF_6','#skF_15',Tc_967)
| ~ reorganization(X_966,'#skF_15',Tb_970)
| ~ class('#skF_6',C_971,'#skF_15')
| ~ class(X_966,C_971,'#skF_15')
| ~ organization('#skF_6',Tc_967)
| ~ organization('#skF_6','#skF_15')
| ~ organization(X_966,'#skF_15') ),
inference(resolution,[status(thm)],[c_54,c_7144]) ).
tff(c_8265,plain,
! [Tc_1156,Tb_1157,X_1158,C_1159] :
( greater(Tc_1156,Tb_1157)
| ~ complexity(X_1158,'#skF_12','#skF_15')
| ~ reorganization_type(X_1158,'#skF_7','#skF_15')
| ~ reorganization('#skF_6','#skF_15',Tc_1156)
| ~ reorganization(X_1158,'#skF_15',Tb_1157)
| ~ class('#skF_6',C_1159,'#skF_15')
| ~ class(X_1158,C_1159,'#skF_15')
| ~ organization('#skF_6',Tc_1156)
| ~ organization(X_1158,'#skF_15') ),
inference(demodulation,[status(thm),theory(equality)],[c_74,c_44,c_7146]) ).
tff(c_8269,plain,
! [Tc_1156,Tb_1157,C_1159] :
( greater(Tc_1156,Tb_1157)
| ~ complexity('#skF_5','#skF_12','#skF_15')
| ~ reorganization('#skF_6','#skF_15',Tc_1156)
| ~ reorganization('#skF_5','#skF_15',Tb_1157)
| ~ class('#skF_6',C_1159,'#skF_15')
| ~ class('#skF_5',C_1159,'#skF_15')
| ~ organization('#skF_6',Tc_1156)
| ~ organization('#skF_5','#skF_15') ),
inference(resolution,[status(thm)],[c_56,c_8265]) ).
tff(c_8275,plain,
! [Tc_1156,Tb_1157,C_1159] :
( greater(Tc_1156,Tb_1157)
| ~ reorganization('#skF_6','#skF_15',Tc_1156)
| ~ reorganization('#skF_5','#skF_15',Tb_1157)
| ~ class('#skF_6',C_1159,'#skF_15')
| ~ class('#skF_5',C_1159,'#skF_15')
| ~ organization('#skF_6',Tc_1156) ),
inference(demodulation,[status(thm),theory(equality)],[c_76,c_46,c_8269]) ).
tff(c_8686,plain,
! [C_1221] :
( ~ class('#skF_6',C_1221,'#skF_15')
| ~ class('#skF_5',C_1221,'#skF_15') ),
inference(splitLeft,[status(thm)],[c_8275]) ).
tff(c_8689,plain,
~ class('#skF_6','#skF_8','#skF_15'),
inference(resolution,[status(thm)],[c_68,c_8686]) ).
tff(c_8693,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_66,c_8689]) ).
tff(c_8695,plain,
! [Tc_1222,Tb_1223] :
( greater(Tc_1222,Tb_1223)
| ~ reorganization('#skF_6','#skF_15',Tc_1222)
| ~ reorganization('#skF_5','#skF_15',Tb_1223)
| ~ organization('#skF_6',Tc_1222) ),
inference(splitRight,[status(thm)],[c_8275]) ).
tff(c_8697,plain,
! [Tb_1223] :
( greater('#skF_17',Tb_1223)
| ~ reorganization('#skF_5','#skF_15',Tb_1223)
| ~ organization('#skF_6','#skF_17') ),
inference(resolution,[status(thm)],[c_58,c_8695]) ).
tff(c_8701,plain,
! [Tb_1224] :
( greater('#skF_17',Tb_1224)
| ~ reorganization('#skF_5','#skF_15',Tb_1224) ),
inference(demodulation,[status(thm),theory(equality)],[c_70,c_8697]) ).
tff(c_8704,plain,
greater('#skF_17','#skF_14'),
inference(resolution,[status(thm)],[c_78,c_8701]) ).
tff(c_8708,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8136,c_8704]) ).
tff(c_8710,plain,
organization('#skF_5','#skF_14'),
inference(splitRight,[status(thm)],[c_235]) ).
tff(c_48,plain,
survival_chance('#skF_6','#skF_11','#skF_14'),
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_242,plain,
! [P1_106,T1_103] :
( greater('#skF_11',P1_106)
| ~ greater('#skF_14',T1_103)
| ~ survival_chance('#skF_6',P1_106,T1_103)
| ~ reorganization_free('#skF_6',T1_103,'#skF_14')
| ~ organization('#skF_6','#skF_14')
| ~ organization('#skF_6',T1_103) ),
inference(resolution,[status(thm)],[c_48,c_223]) ).
tff(c_366,plain,
~ organization('#skF_6','#skF_14'),
inference(splitLeft,[status(thm)],[c_242]) ).
tff(c_4469,plain,
! [Ta_685,Tb_682,P1_681,P2_684,X_683] :
( greater(P1_681,P2_684)
| greater('#skF_17',Tb_682)
| greater(Ta_685,'#skF_15')
| ~ survival_chance(X_683,P2_684,'#skF_17')
| ~ survival_chance(X_683,P1_681,'#skF_15')
| ~ reorganization(X_683,Ta_685,Tb_682)
| ~ organization(X_683,'#skF_17')
| ~ organization(X_683,'#skF_15') ),
inference(resolution,[status(thm)],[c_96,c_316]) ).
tff(c_4474,plain,
! [P1_686,X_687,Tb_688,Ta_689] :
( greater(P1_686,'#skF_1'(X_687,'#skF_17'))
| greater('#skF_17',Tb_688)
| greater(Ta_689,'#skF_15')
| ~ survival_chance(X_687,P1_686,'#skF_15')
| ~ reorganization(X_687,Ta_689,Tb_688)
| ~ organization(X_687,'#skF_15')
| ~ organization(X_687,'#skF_17') ),
inference(resolution,[status(thm)],[c_10,c_4469]) ).
tff(c_4478,plain,
! [P1_686] :
( greater(P1_686,'#skF_1'('#skF_5','#skF_17'))
| greater('#skF_17','#skF_14')
| greater('#skF_15','#skF_15')
| ~ survival_chance('#skF_5',P1_686,'#skF_15')
| ~ organization('#skF_5','#skF_15')
| ~ organization('#skF_5','#skF_17') ),
inference(resolution,[status(thm)],[c_78,c_4474]) ).
tff(c_4485,plain,
! [P1_686] :
( greater(P1_686,'#skF_1'('#skF_5','#skF_17'))
| greater('#skF_17','#skF_14')
| greater('#skF_15','#skF_15')
| ~ survival_chance('#skF_5',P1_686,'#skF_15') ),
inference(demodulation,[status(thm),theory(equality)],[c_72,c_76,c_4478]) ).
tff(c_4486,plain,
! [P1_686] :
( greater(P1_686,'#skF_1'('#skF_5','#skF_17'))
| greater('#skF_17','#skF_14')
| ~ survival_chance('#skF_5',P1_686,'#skF_15') ),
inference(negUnitSimplification,[status(thm)],[c_2,c_4485]) ).
tff(c_4709,plain,
greater('#skF_17','#skF_14'),
inference(splitLeft,[status(thm)],[c_4486]) ).
tff(c_4897,plain,
! [X_733,T1_734] :
( organization(X_733,'#skF_14')
| ~ greater('#skF_14',T1_734)
| ~ organization(X_733,'#skF_17')
| ~ organization(X_733,T1_734) ),
inference(resolution,[status(thm)],[c_4709,c_12]) ).
tff(c_4901,plain,
! [T1_734] :
( organization('#skF_6','#skF_14')
| ~ greater('#skF_14',T1_734)
| ~ organization('#skF_6',T1_734) ),
inference(resolution,[status(thm)],[c_70,c_4897]) ).
tff(c_4907,plain,
! [T1_735] :
( ~ greater('#skF_14',T1_735)
| ~ organization('#skF_6',T1_735) ),
inference(negUnitSimplification,[status(thm)],[c_366,c_4901]) ).
tff(c_4913,plain,
~ greater('#skF_14','#skF_15'),
inference(resolution,[status(thm)],[c_74,c_4907]) ).
tff(c_4918,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_97,c_4913]) ).
tff(c_4920,plain,
~ greater('#skF_17','#skF_14'),
inference(splitRight,[status(thm)],[c_4486]) ).
tff(c_3315,plain,
! [Y_540,C1_536,C2_542,X_539,Re_537,Tc_538,Tb_543,Ta_535,C_541] :
( greater(Tc_538,Tb_543)
| ~ greater(C2_542,C1_536)
| ~ complexity(Y_540,C2_542,Ta_535)
| ~ complexity(X_539,C1_536,Ta_535)
| ~ reorganization_type(Y_540,Re_537,Ta_535)
| ~ reorganization_type(X_539,Re_537,Ta_535)
| ~ reorganization(Y_540,Ta_535,Tc_538)
| ~ reorganization(X_539,Ta_535,Tb_543)
| ~ class(Y_540,C_541,Ta_535)
| ~ class(X_539,C_541,Ta_535)
| ~ organization(Y_540,Tc_538)
| ~ organization(Y_540,Ta_535)
| ~ organization(X_539,Ta_535) ),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_4092,plain,
! [Tb_612,Ta_609,Re_613,Tc_614,Y_611,X_608,C_610] :
( greater(Tc_614,Tb_612)
| ~ complexity(Y_611,'#skF_13',Ta_609)
| ~ complexity(X_608,'#skF_12',Ta_609)
| ~ reorganization_type(Y_611,Re_613,Ta_609)
| ~ reorganization_type(X_608,Re_613,Ta_609)
| ~ reorganization(Y_611,Ta_609,Tc_614)
| ~ reorganization(X_608,Ta_609,Tb_612)
| ~ class(Y_611,C_610,Ta_609)
| ~ class(X_608,C_610,Ta_609)
| ~ organization(Y_611,Tc_614)
| ~ organization(Y_611,Ta_609)
| ~ organization(X_608,Ta_609) ),
inference(resolution,[status(thm)],[c_42,c_3315]) ).
tff(c_4094,plain,
! [Tc_614,Tb_612,X_608,C_610] :
( greater(Tc_614,Tb_612)
| ~ complexity('#skF_6','#skF_13','#skF_15')
| ~ complexity(X_608,'#skF_12','#skF_15')
| ~ reorganization_type(X_608,'#skF_7','#skF_15')
| ~ reorganization('#skF_6','#skF_15',Tc_614)
| ~ reorganization(X_608,'#skF_15',Tb_612)
| ~ class('#skF_6',C_610,'#skF_15')
| ~ class(X_608,C_610,'#skF_15')
| ~ organization('#skF_6',Tc_614)
| ~ organization('#skF_6','#skF_15')
| ~ organization(X_608,'#skF_15') ),
inference(resolution,[status(thm)],[c_54,c_4092]) ).
tff(c_5135,plain,
! [Tc_753,Tb_754,X_755,C_756] :
( greater(Tc_753,Tb_754)
| ~ complexity(X_755,'#skF_12','#skF_15')
| ~ reorganization_type(X_755,'#skF_7','#skF_15')
| ~ reorganization('#skF_6','#skF_15',Tc_753)
| ~ reorganization(X_755,'#skF_15',Tb_754)
| ~ class('#skF_6',C_756,'#skF_15')
| ~ class(X_755,C_756,'#skF_15')
| ~ organization('#skF_6',Tc_753)
| ~ organization(X_755,'#skF_15') ),
inference(demodulation,[status(thm),theory(equality)],[c_74,c_44,c_4094]) ).
tff(c_5139,plain,
! [Tc_753,Tb_754,C_756] :
( greater(Tc_753,Tb_754)
| ~ complexity('#skF_5','#skF_12','#skF_15')
| ~ reorganization('#skF_6','#skF_15',Tc_753)
| ~ reorganization('#skF_5','#skF_15',Tb_754)
| ~ class('#skF_6',C_756,'#skF_15')
| ~ class('#skF_5',C_756,'#skF_15')
| ~ organization('#skF_6',Tc_753)
| ~ organization('#skF_5','#skF_15') ),
inference(resolution,[status(thm)],[c_56,c_5135]) ).
tff(c_5145,plain,
! [Tc_753,Tb_754,C_756] :
( greater(Tc_753,Tb_754)
| ~ reorganization('#skF_6','#skF_15',Tc_753)
| ~ reorganization('#skF_5','#skF_15',Tb_754)
| ~ class('#skF_6',C_756,'#skF_15')
| ~ class('#skF_5',C_756,'#skF_15')
| ~ organization('#skF_6',Tc_753) ),
inference(demodulation,[status(thm),theory(equality)],[c_76,c_46,c_5139]) ).
tff(c_5258,plain,
! [C_769] :
( ~ class('#skF_6',C_769,'#skF_15')
| ~ class('#skF_5',C_769,'#skF_15') ),
inference(splitLeft,[status(thm)],[c_5145]) ).
tff(c_5261,plain,
~ class('#skF_6','#skF_8','#skF_15'),
inference(resolution,[status(thm)],[c_68,c_5258]) ).
tff(c_5265,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_66,c_5261]) ).
tff(c_5379,plain,
! [Tc_782,Tb_783] :
( greater(Tc_782,Tb_783)
| ~ reorganization('#skF_6','#skF_15',Tc_782)
| ~ reorganization('#skF_5','#skF_15',Tb_783)
| ~ organization('#skF_6',Tc_782) ),
inference(splitRight,[status(thm)],[c_5145]) ).
tff(c_5381,plain,
! [Tb_783] :
( greater('#skF_17',Tb_783)
| ~ reorganization('#skF_5','#skF_15',Tb_783)
| ~ organization('#skF_6','#skF_17') ),
inference(resolution,[status(thm)],[c_58,c_5379]) ).
tff(c_5385,plain,
! [Tb_784] :
( greater('#skF_17',Tb_784)
| ~ reorganization('#skF_5','#skF_15',Tb_784) ),
inference(demodulation,[status(thm),theory(equality)],[c_70,c_5381]) ).
tff(c_5388,plain,
greater('#skF_17','#skF_14'),
inference(resolution,[status(thm)],[c_78,c_5385]) ).
tff(c_5392,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4920,c_5388]) ).
tff(c_5394,plain,
organization('#skF_6','#skF_14'),
inference(splitRight,[status(thm)],[c_242]) ).
tff(c_9661,plain,
! [Tb_1335,X_1333,C2_1337,P2_1326,Re_1334,P1_1329,Tc_1328,Ta_1327,Y_1330,C1_1336,C_1332,P_1331] :
( ( P2_1326 = P1_1329 )
| greater(P1_1329,P2_1326)
| ~ greater(C2_1337,C1_1336)
| ~ complexity(Y_1330,C2_1337,Ta_1327)
| ~ complexity(X_1333,C1_1336,Ta_1327)
| ~ survival_chance(Y_1330,P2_1326,Tb_1335)
| ~ survival_chance(X_1333,P1_1329,Tb_1335)
| ~ reorganization_type(Y_1330,Re_1334,Ta_1327)
| ~ reorganization_type(X_1333,Re_1334,Ta_1327)
| ~ reorganization(Y_1330,Ta_1327,Tc_1328)
| ~ reorganization(X_1333,Ta_1327,Tb_1335)
| ~ survival_chance(Y_1330,P_1331,Ta_1327)
| ~ survival_chance(X_1333,P_1331,Ta_1327)
| ~ class(Y_1330,C_1332,Ta_1327)
| ~ class(X_1333,C_1332,Ta_1327)
| ~ organization(Y_1330,Tb_1335)
| ~ organization(X_1333,Tb_1335)
| ~ organization(Y_1330,Ta_1327)
| ~ organization(X_1333,Ta_1327) ),
inference(cnfTransformation,[status(thm)],[f_176]) ).
tff(c_10501,plain,
! [P2_1393,C_1396,Tc_1394,Y_1392,Re_1397,Ta_1391,X_1398,Tb_1400,P_1395,P1_1399] :
( ( P2_1393 = P1_1399 )
| greater(P1_1399,P2_1393)
| ~ complexity(Y_1392,'#skF_13',Ta_1391)
| ~ complexity(X_1398,'#skF_12',Ta_1391)
| ~ survival_chance(Y_1392,P2_1393,Tb_1400)
| ~ survival_chance(X_1398,P1_1399,Tb_1400)
| ~ reorganization_type(Y_1392,Re_1397,Ta_1391)
| ~ reorganization_type(X_1398,Re_1397,Ta_1391)
| ~ reorganization(Y_1392,Ta_1391,Tc_1394)
| ~ reorganization(X_1398,Ta_1391,Tb_1400)
| ~ survival_chance(Y_1392,P_1395,Ta_1391)
| ~ survival_chance(X_1398,P_1395,Ta_1391)
| ~ class(Y_1392,C_1396,Ta_1391)
| ~ class(X_1398,C_1396,Ta_1391)
| ~ organization(Y_1392,Tb_1400)
| ~ organization(X_1398,Tb_1400)
| ~ organization(Y_1392,Ta_1391)
| ~ organization(X_1398,Ta_1391) ),
inference(resolution,[status(thm)],[c_42,c_9661]) ).
tff(c_10515,plain,
! [C_1396,Tc_1394,Re_1397,Ta_1391,X_1398,P_1395,P1_1399] :
( ( P1_1399 = '#skF_11' )
| greater(P1_1399,'#skF_11')
| ~ complexity('#skF_6','#skF_13',Ta_1391)
| ~ complexity(X_1398,'#skF_12',Ta_1391)
| ~ survival_chance(X_1398,P1_1399,'#skF_14')
| ~ reorganization_type('#skF_6',Re_1397,Ta_1391)
| ~ reorganization_type(X_1398,Re_1397,Ta_1391)
| ~ reorganization('#skF_6',Ta_1391,Tc_1394)
| ~ reorganization(X_1398,Ta_1391,'#skF_14')
| ~ survival_chance('#skF_6',P_1395,Ta_1391)
| ~ survival_chance(X_1398,P_1395,Ta_1391)
| ~ class('#skF_6',C_1396,Ta_1391)
| ~ class(X_1398,C_1396,Ta_1391)
| ~ organization('#skF_6','#skF_14')
| ~ organization(X_1398,'#skF_14')
| ~ organization('#skF_6',Ta_1391)
| ~ organization(X_1398,Ta_1391) ),
inference(resolution,[status(thm)],[c_48,c_10501]) ).
tff(c_21088,plain,
! [Ta_2017,C_2016,Re_2013,Tc_2014,P_2012,X_2015,P1_2011] :
( ( P1_2011 = '#skF_11' )
| greater(P1_2011,'#skF_11')
| ~ complexity('#skF_6','#skF_13',Ta_2017)
| ~ complexity(X_2015,'#skF_12',Ta_2017)
| ~ survival_chance(X_2015,P1_2011,'#skF_14')
| ~ reorganization_type('#skF_6',Re_2013,Ta_2017)
| ~ reorganization_type(X_2015,Re_2013,Ta_2017)
| ~ reorganization('#skF_6',Ta_2017,Tc_2014)
| ~ reorganization(X_2015,Ta_2017,'#skF_14')
| ~ survival_chance('#skF_6',P_2012,Ta_2017)
| ~ survival_chance(X_2015,P_2012,Ta_2017)
| ~ class('#skF_6',C_2016,Ta_2017)
| ~ class(X_2015,C_2016,Ta_2017)
| ~ organization(X_2015,'#skF_14')
| ~ organization('#skF_6',Ta_2017)
| ~ organization(X_2015,Ta_2017) ),
inference(demodulation,[status(thm),theory(equality)],[c_5394,c_10515]) ).
tff(c_21093,plain,
! [Ta_2017,C_2016,Re_2013,Tc_2014,P_2012] :
( ( '#skF_11' = '#skF_10' )
| greater('#skF_10','#skF_11')
| ~ complexity('#skF_6','#skF_13',Ta_2017)
| ~ complexity('#skF_5','#skF_12',Ta_2017)
| ~ reorganization_type('#skF_6',Re_2013,Ta_2017)
| ~ reorganization_type('#skF_5',Re_2013,Ta_2017)
| ~ reorganization('#skF_6',Ta_2017,Tc_2014)
| ~ reorganization('#skF_5',Ta_2017,'#skF_14')
| ~ survival_chance('#skF_6',P_2012,Ta_2017)
| ~ survival_chance('#skF_5',P_2012,Ta_2017)
| ~ class('#skF_6',C_2016,Ta_2017)
| ~ class('#skF_5',C_2016,Ta_2017)
| ~ organization('#skF_5','#skF_14')
| ~ organization('#skF_6',Ta_2017)
| ~ organization('#skF_5',Ta_2017) ),
inference(resolution,[status(thm)],[c_50,c_21088]) ).
tff(c_21099,plain,
! [Ta_2017,C_2016,Re_2013,Tc_2014,P_2012] :
( ( '#skF_11' = '#skF_10' )
| greater('#skF_10','#skF_11')
| ~ complexity('#skF_6','#skF_13',Ta_2017)
| ~ complexity('#skF_5','#skF_12',Ta_2017)
| ~ reorganization_type('#skF_6',Re_2013,Ta_2017)
| ~ reorganization_type('#skF_5',Re_2013,Ta_2017)
| ~ reorganization('#skF_6',Ta_2017,Tc_2014)
| ~ reorganization('#skF_5',Ta_2017,'#skF_14')
| ~ survival_chance('#skF_6',P_2012,Ta_2017)
| ~ survival_chance('#skF_5',P_2012,Ta_2017)
| ~ class('#skF_6',C_2016,Ta_2017)
| ~ class('#skF_5',C_2016,Ta_2017)
| ~ organization('#skF_6',Ta_2017)
| ~ organization('#skF_5',Ta_2017) ),
inference(demodulation,[status(thm),theory(equality)],[c_8710,c_21093]) ).
tff(c_21547,plain,
! [Tc_2057,C_2061,Re_2058,Ta_2059,P_2060] :
( ~ complexity('#skF_6','#skF_13',Ta_2059)
| ~ complexity('#skF_5','#skF_12',Ta_2059)
| ~ reorganization_type('#skF_6',Re_2058,Ta_2059)
| ~ reorganization_type('#skF_5',Re_2058,Ta_2059)
| ~ reorganization('#skF_6',Ta_2059,Tc_2057)
| ~ reorganization('#skF_5',Ta_2059,'#skF_14')
| ~ survival_chance('#skF_6',P_2060,Ta_2059)
| ~ survival_chance('#skF_5',P_2060,Ta_2059)
| ~ class('#skF_6',C_2061,Ta_2059)
| ~ class('#skF_5',C_2061,Ta_2059)
| ~ organization('#skF_6',Ta_2059)
| ~ organization('#skF_5',Ta_2059) ),
inference(negUnitSimplification,[status(thm)],[c_36,c_34,c_21099]) ).
tff(c_21549,plain,
! [Tc_2057,P_2060,C_2061] :
( ~ complexity('#skF_6','#skF_13','#skF_15')
| ~ complexity('#skF_5','#skF_12','#skF_15')
| ~ reorganization_type('#skF_6','#skF_7','#skF_15')
| ~ reorganization('#skF_6','#skF_15',Tc_2057)
| ~ reorganization('#skF_5','#skF_15','#skF_14')
| ~ survival_chance('#skF_6',P_2060,'#skF_15')
| ~ survival_chance('#skF_5',P_2060,'#skF_15')
| ~ class('#skF_6',C_2061,'#skF_15')
| ~ class('#skF_5',C_2061,'#skF_15')
| ~ organization('#skF_6','#skF_15')
| ~ organization('#skF_5','#skF_15') ),
inference(resolution,[status(thm)],[c_56,c_21547]) ).
tff(c_21552,plain,
! [Tc_2057,P_2060,C_2061] :
( ~ reorganization('#skF_6','#skF_15',Tc_2057)
| ~ survival_chance('#skF_6',P_2060,'#skF_15')
| ~ survival_chance('#skF_5',P_2060,'#skF_15')
| ~ class('#skF_6',C_2061,'#skF_15')
| ~ class('#skF_5',C_2061,'#skF_15') ),
inference(demodulation,[status(thm),theory(equality)],[c_76,c_74,c_78,c_54,c_46,c_44,c_21549]) ).
tff(c_21554,plain,
! [C_2062] :
( ~ class('#skF_6',C_2062,'#skF_15')
| ~ class('#skF_5',C_2062,'#skF_15') ),
inference(splitLeft,[status(thm)],[c_21552]) ).
tff(c_21557,plain,
~ class('#skF_6','#skF_8','#skF_15'),
inference(resolution,[status(thm)],[c_68,c_21554]) ).
tff(c_21561,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_66,c_21557]) ).
tff(c_21562,plain,
! [P_2060,Tc_2057] :
( ~ survival_chance('#skF_6',P_2060,'#skF_15')
| ~ survival_chance('#skF_5',P_2060,'#skF_15')
| ~ reorganization('#skF_6','#skF_15',Tc_2057) ),
inference(splitRight,[status(thm)],[c_21552]) ).
tff(c_21563,plain,
! [Tc_2057] : ~ reorganization('#skF_6','#skF_15',Tc_2057),
inference(splitLeft,[status(thm)],[c_21562]) ).
tff(c_21565,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21563,c_58]) ).
tff(c_21567,plain,
! [P_2063] :
( ~ survival_chance('#skF_6',P_2063,'#skF_15')
| ~ survival_chance('#skF_5',P_2063,'#skF_15') ),
inference(splitRight,[status(thm)],[c_21562]) ).
tff(c_21574,plain,
~ survival_chance('#skF_6','#skF_9','#skF_15'),
inference(resolution,[status(thm)],[c_64,c_21567]) ).
tff(c_21581,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_62,c_21574]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : MGT005+2 : TPTP v9.3.0. Bugfixed v3.2.0.
% 0.00/0.02 % 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.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Mon Sep 7 11:39:26 UTC 2026
% 0.03/0.30 % CPUTime :
% 11.07/4.22 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.07/4.23
% 11.07/4.23 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------