%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT002+1 : TPTP v9.3.0. Released v2.0.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 : n004.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:47 AM UTC 2026
% Result : Theorem 3.97s 2.44s
% Output : CNFRefutation 3.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 5
% Syntax : Number of formulae : 31 ( 10 unt; 0 typ; 0 def)
% Number of atoms : 142 ( 0 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 204 ( 93 ~; 87 |; 18 &)
% ( 1 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 8 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 : 6 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 84 ( 83 !; 1 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ reproducibility > reorganization_free > inertia > organization > greater > #nlpp > #skF_5 > #skF_6 > #skF_2 > #skF_3 > #skF_4 > #skF_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(reorganization_free,type,
reorganization_free: ( $i * $i * $i ) > $o ).
tff(greater,type,
greater: ( $i * $i ) > $o ).
tff(reproducibility,type,
reproducibility: ( $i * $i * $i ) > $o ).
tff(inertia,type,
inertia: ( $i * $i * $i ) > $o ).
tff('#skF_5',type,
'#skF_5': $i ).
tff('#skF_6',type,
'#skF_6': $i ).
tff('#skF_2',type,
'#skF_2': $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_4',type,
'#skF_4': $i ).
tff(organization,type,
organization: ( $i * $i ) > $o ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff(f_90,negated_conjecture,
~ ! [X,I1,I2,T1,T2] :
( ( organization(X,T1)
& organization(X,T2)
& reorganization_free(X,T1,T2)
& inertia(X,I1,T1)
& inertia(X,I2,T2)
& greater(T2,T1) )
=> greater(I2,I1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_FOL) ).
tff(f_32,axiom,
! [X,T] :
( organization(X,T)
=> ? [Rp] : reproducibility(X,Rp,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp3) ).
tff(f_38,axiom,
! [X,T1,T2] :
( reorganization_free(X,T1,T2)
=> ( reorganization_free(X,T1,T1)
& reorganization_free(X,T2,T2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp4) ).
tff(f_75,hypothesis,
! [X,Rp1,Rp2,T1,T2] :
( ( organization(X,T1)
& organization(X,T2)
& reorganization_free(X,T1,T2)
& reproducibility(X,Rp1,T1)
& reproducibility(X,Rp2,T2)
& greater(T2,T1) )
=> greater(Rp2,Rp1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a4_FOL) ).
tff(f_60,hypothesis,
! [X,Y,T1,T2,Rp1,Rp2,I1,I2] :
( ( organization(X,T1)
& organization(Y,T2)
& reorganization_free(X,T1,T1)
& reorganization_free(Y,T2,T2)
& reproducibility(X,Rp1,T1)
& reproducibility(Y,Rp2,T2)
& inertia(X,I1,T1)
& inertia(Y,I2,T2) )
=> ( greater(Rp2,Rp1)
<=> greater(I2,I1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a3_FOL) ).
tff(c_26,plain,
organization('#skF_2','#skF_5'),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_22,plain,
reorganization_free('#skF_2','#skF_5','#skF_6'),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_16,plain,
greater('#skF_6','#skF_5'),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_2,plain,
! [X_1,T_2] :
( reproducibility(X_1,'#skF_1'(X_1,T_2),T_2)
| ~ organization(X_1,T_2) ),
inference(cnfTransformation,[status(thm)],[f_32]) ).
tff(c_24,plain,
organization('#skF_2','#skF_6'),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_14,plain,
~ greater('#skF_4','#skF_3'),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_27,plain,
! [X_20,T1_21,T2_22] :
( reorganization_free(X_20,T1_21,T1_21)
| ~ reorganization_free(X_20,T1_21,T2_22) ),
inference(cnfTransformation,[status(thm)],[f_38]) ).
tff(c_30,plain,
reorganization_free('#skF_2','#skF_5','#skF_5'),
inference(resolution,[status(thm)],[c_22,c_27]) ).
tff(c_20,plain,
inertia('#skF_2','#skF_3','#skF_5'),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_35,plain,
! [X_23,T2_24,T1_25] :
( reorganization_free(X_23,T2_24,T2_24)
| ~ reorganization_free(X_23,T1_25,T2_24) ),
inference(cnfTransformation,[status(thm)],[f_38]) ).
tff(c_42,plain,
reorganization_free('#skF_2','#skF_6','#skF_6'),
inference(resolution,[status(thm)],[c_22,c_35]) ).
tff(c_18,plain,
inertia('#skF_2','#skF_4','#skF_6'),
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_52,plain,
! [Rp1_29,T1_31,Rp2_32,T2_28,X_30] :
( greater(Rp2_32,Rp1_29)
| ~ greater(T2_28,T1_31)
| ~ reproducibility(X_30,Rp2_32,T2_28)
| ~ reproducibility(X_30,Rp1_29,T1_31)
| ~ reorganization_free(X_30,T1_31,T2_28)
| ~ organization(X_30,T2_28)
| ~ organization(X_30,T1_31) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_56,plain,
! [X_33,T_34,Rp1_35,T1_36] :
( greater('#skF_1'(X_33,T_34),Rp1_35)
| ~ greater(T_34,T1_36)
| ~ reproducibility(X_33,Rp1_35,T1_36)
| ~ reorganization_free(X_33,T1_36,T_34)
| ~ organization(X_33,T1_36)
| ~ organization(X_33,T_34) ),
inference(resolution,[status(thm)],[c_2,c_52]) ).
tff(c_59,plain,
! [X_1,T_34,T_2] :
( greater('#skF_1'(X_1,T_34),'#skF_1'(X_1,T_2))
| ~ greater(T_34,T_2)
| ~ reorganization_free(X_1,T_2,T_34)
| ~ organization(X_1,T_34)
| ~ organization(X_1,T_2) ),
inference(resolution,[status(thm)],[c_2,c_56]) ).
tff(c_89,plain,
! [T1_66,I1_68,Rp1_70,T2_64,X_65,Rp2_69,I2_67,Y_63] :
( greater(I2_67,I1_68)
| ~ greater(Rp2_69,Rp1_70)
| ~ inertia(Y_63,I2_67,T2_64)
| ~ inertia(X_65,I1_68,T1_66)
| ~ reproducibility(Y_63,Rp2_69,T2_64)
| ~ reproducibility(X_65,Rp1_70,T1_66)
| ~ reorganization_free(Y_63,T2_64,T2_64)
| ~ reorganization_free(X_65,T1_66,T1_66)
| ~ organization(Y_63,T2_64)
| ~ organization(X_65,T1_66) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_109,plain,
! [I1_85,I2_80,T1_81,X_83,T_82,Y_84,T_77,T2_79,X_78] :
( greater(I2_80,I1_85)
| ~ inertia(Y_84,I2_80,T2_79)
| ~ inertia(X_78,I1_85,T1_81)
| ~ reproducibility(Y_84,'#skF_1'(X_83,T_82),T2_79)
| ~ reproducibility(X_78,'#skF_1'(X_83,T_77),T1_81)
| ~ reorganization_free(Y_84,T2_79,T2_79)
| ~ reorganization_free(X_78,T1_81,T1_81)
| ~ organization(Y_84,T2_79)
| ~ organization(X_78,T1_81)
| ~ greater(T_82,T_77)
| ~ reorganization_free(X_83,T_77,T_82)
| ~ organization(X_83,T_82)
| ~ organization(X_83,T_77) ),
inference(resolution,[status(thm)],[c_59,c_89]) ).
tff(c_111,plain,
! [I1_85,T1_81,X_83,T_82,T_77,X_78] :
( greater('#skF_4',I1_85)
| ~ inertia(X_78,I1_85,T1_81)
| ~ reproducibility('#skF_2','#skF_1'(X_83,T_82),'#skF_6')
| ~ reproducibility(X_78,'#skF_1'(X_83,T_77),T1_81)
| ~ reorganization_free('#skF_2','#skF_6','#skF_6')
| ~ reorganization_free(X_78,T1_81,T1_81)
| ~ organization('#skF_2','#skF_6')
| ~ organization(X_78,T1_81)
| ~ greater(T_82,T_77)
| ~ reorganization_free(X_83,T_77,T_82)
| ~ organization(X_83,T_82)
| ~ organization(X_83,T_77) ),
inference(resolution,[status(thm)],[c_18,c_109]) ).
tff(c_120,plain,
! [X_86,I1_89,X_88,T_91,T1_87,T_90] :
( greater('#skF_4',I1_89)
| ~ inertia(X_86,I1_89,T1_87)
| ~ reproducibility('#skF_2','#skF_1'(X_88,T_91),'#skF_6')
| ~ reproducibility(X_86,'#skF_1'(X_88,T_90),T1_87)
| ~ reorganization_free(X_86,T1_87,T1_87)
| ~ organization(X_86,T1_87)
| ~ greater(T_91,T_90)
| ~ reorganization_free(X_88,T_90,T_91)
| ~ organization(X_88,T_91)
| ~ organization(X_88,T_90) ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_42,c_111]) ).
tff(c_124,plain,
! [X_88,T_91,T_90] :
( greater('#skF_4','#skF_3')
| ~ reproducibility('#skF_2','#skF_1'(X_88,T_91),'#skF_6')
| ~ reproducibility('#skF_2','#skF_1'(X_88,T_90),'#skF_5')
| ~ reorganization_free('#skF_2','#skF_5','#skF_5')
| ~ organization('#skF_2','#skF_5')
| ~ greater(T_91,T_90)
| ~ reorganization_free(X_88,T_90,T_91)
| ~ organization(X_88,T_91)
| ~ organization(X_88,T_90) ),
inference(resolution,[status(thm)],[c_20,c_120]) ).
tff(c_130,plain,
! [X_88,T_91,T_90] :
( greater('#skF_4','#skF_3')
| ~ reproducibility('#skF_2','#skF_1'(X_88,T_91),'#skF_6')
| ~ reproducibility('#skF_2','#skF_1'(X_88,T_90),'#skF_5')
| ~ greater(T_91,T_90)
| ~ reorganization_free(X_88,T_90,T_91)
| ~ organization(X_88,T_91)
| ~ organization(X_88,T_90) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_30,c_124]) ).
tff(c_132,plain,
! [X_92,T_93,T_94] :
( ~ reproducibility('#skF_2','#skF_1'(X_92,T_93),'#skF_6')
| ~ reproducibility('#skF_2','#skF_1'(X_92,T_94),'#skF_5')
| ~ greater(T_93,T_94)
| ~ reorganization_free(X_92,T_94,T_93)
| ~ organization(X_92,T_93)
| ~ organization(X_92,T_94) ),
inference(negUnitSimplification,[status(thm)],[c_14,c_130]) ).
tff(c_135,plain,
! [T_94] :
( ~ reproducibility('#skF_2','#skF_1'('#skF_2',T_94),'#skF_5')
| ~ greater('#skF_6',T_94)
| ~ reorganization_free('#skF_2',T_94,'#skF_6')
| ~ organization('#skF_2',T_94)
| ~ organization('#skF_2','#skF_6') ),
inference(resolution,[status(thm)],[c_2,c_132]) ).
tff(c_139,plain,
! [T_95] :
( ~ reproducibility('#skF_2','#skF_1'('#skF_2',T_95),'#skF_5')
| ~ greater('#skF_6',T_95)
| ~ reorganization_free('#skF_2',T_95,'#skF_6')
| ~ organization('#skF_2',T_95) ),
inference(demodulation,[status(thm),theory(equality)],[c_24,c_135]) ).
tff(c_143,plain,
( ~ greater('#skF_6','#skF_5')
| ~ reorganization_free('#skF_2','#skF_5','#skF_6')
| ~ organization('#skF_2','#skF_5') ),
inference(resolution,[status(thm)],[c_2,c_139]) ).
tff(c_147,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_26,c_22,c_16,c_143]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT002+1 : TPTP v9.3.0. Released v2.0.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.08/0.34 % Computer : n004.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 7 11:32:30 UTC 2026
% 0.08/0.35 % CPUTime :
% 3.97/2.44 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.97/2.45
% 3.97/2.45 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------