%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT015+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 : n031.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:51 AM UTC 2026
% Result : Theorem 3.96s 2.54s
% Output : CNFRefutation 3.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 4
% Syntax : Number of formulae : 40 ( 17 unt; 0 typ; 0 def)
% Number of atoms : 203 ( 0 equ)
% Maximal formula atoms : 15 ( 5 avg)
% Number of connectives : 296 ( 133 ~; 129 |; 30 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 9 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 : 115 ( 114 !; 1 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ reorganization_type > reorganization > inertia > complexity > class > organization > greater > #nlpp > #skF_7 > #skF_10 > #skF_5 > #skF_6 > #skF_2 > #skF_3 > #skF_9 > #skF_8 > #skF_4 > #skF_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(greater,type,
greater: ( $i * $i ) > $o ).
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(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(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('#skF_4',type,
'#skF_4': $i ).
tff(organization,type,
organization: ( $i * $i ) > $o ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff(f_112,negated_conjecture,
~ ! [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/sandbox2/benchmark/theBenchmark.p',t15_FOL) ).
tff(f_31,axiom,
! [X,T] :
( organization(X,T)
=> ? [I] : inertia(X,I,T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp5) ).
tff(f_51,hypothesis,
! [X,Y,C,C1,C2,I1,I2,T1,T2] :
( ( organization(X,T1)
& organization(Y,T2)
& class(X,C,T1)
& class(Y,C,T2)
& complexity(X,C1,T1)
& complexity(Y,C2,T2)
& inertia(X,I1,T1)
& inertia(Y,I2,T2)
& greater(C2,C1) )
=> greater(I2,I1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a12_FOL) ).
tff(f_80,hypothesis,
! [X,Y,Rt,C,I1,I2,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,Rt,Ta)
& reorganization_type(Y,Rt,Ta)
& inertia(X,I1,Ta)
& inertia(Y,I2,Ta)
& greater(I2,I1) )
=> greater(Tc,Tb) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a13_FOL) ).
tff(c_8,plain,
~ greater('#skF_10','#skF_9'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_22,plain,
reorganization('#skF_2','#skF_8','#skF_9'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_28,plain,
organization('#skF_3','#skF_10'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_20,plain,
reorganization('#skF_3','#skF_8','#skF_10'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_24,plain,
class('#skF_3','#skF_5','#skF_8'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_26,plain,
class('#skF_2','#skF_5','#skF_8'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_32,plain,
organization('#skF_2','#skF_8'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_14,plain,
complexity('#skF_2','#skF_6','#skF_8'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_18,plain,
reorganization_type('#skF_2','#skF_4','#skF_8'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_16,plain,
reorganization_type('#skF_3','#skF_4','#skF_8'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_2,plain,
! [X_1,T_2] :
( inertia(X_1,'#skF_1'(X_1,T_2),T_2)
| ~ organization(X_1,T_2) ),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_30,plain,
organization('#skF_3','#skF_8'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_12,plain,
complexity('#skF_3','#skF_7','#skF_8'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_10,plain,
greater('#skF_7','#skF_6'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_34,plain,
! [C1_26,C_29,T1_28,I2_25,Y_27,I1_32,C2_31,T2_24,X_30] :
( greater(I2_25,I1_32)
| ~ greater(C2_31,C1_26)
| ~ inertia(Y_27,I2_25,T2_24)
| ~ inertia(X_30,I1_32,T1_28)
| ~ complexity(Y_27,C2_31,T2_24)
| ~ complexity(X_30,C1_26,T1_28)
| ~ class(Y_27,C_29,T2_24)
| ~ class(X_30,C_29,T1_28)
| ~ organization(Y_27,T2_24)
| ~ organization(X_30,T1_28) ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_42,plain,
! [C_42,I2_46,T1_43,T2_44,X_45,I1_47,Y_48] :
( greater(I2_46,I1_47)
| ~ inertia(Y_48,I2_46,T2_44)
| ~ inertia(X_45,I1_47,T1_43)
| ~ complexity(Y_48,'#skF_7',T2_44)
| ~ complexity(X_45,'#skF_6',T1_43)
| ~ class(Y_48,C_42,T2_44)
| ~ class(X_45,C_42,T1_43)
| ~ organization(Y_48,T2_44)
| ~ organization(X_45,T1_43) ),
inference(resolution,[status(thm)],[c_10,c_34]) ).
tff(c_46,plain,
! [X_51,X_54,I1_53,T_49,C_50,T1_52] :
( greater('#skF_1'(X_51,T_49),I1_53)
| ~ inertia(X_54,I1_53,T1_52)
| ~ complexity(X_51,'#skF_7',T_49)
| ~ complexity(X_54,'#skF_6',T1_52)
| ~ class(X_51,C_50,T_49)
| ~ class(X_54,C_50,T1_52)
| ~ organization(X_54,T1_52)
| ~ organization(X_51,T_49) ),
inference(resolution,[status(thm)],[c_2,c_42]) ).
tff(c_50,plain,
! [C_56,X_58,T_55,X_57,T_59] :
( greater('#skF_1'(X_58,T_59),'#skF_1'(X_57,T_55))
| ~ complexity(X_58,'#skF_7',T_59)
| ~ complexity(X_57,'#skF_6',T_55)
| ~ class(X_58,C_56,T_59)
| ~ class(X_57,C_56,T_55)
| ~ organization(X_58,T_59)
| ~ organization(X_57,T_55) ),
inference(resolution,[status(thm)],[c_2,c_46]) ).
tff(c_52,plain,
! [X_57,T_55] :
( greater('#skF_1'('#skF_3','#skF_8'),'#skF_1'(X_57,T_55))
| ~ complexity('#skF_3','#skF_7','#skF_8')
| ~ complexity(X_57,'#skF_6',T_55)
| ~ class(X_57,'#skF_5',T_55)
| ~ organization('#skF_3','#skF_8')
| ~ organization(X_57,T_55) ),
inference(resolution,[status(thm)],[c_24,c_50]) ).
tff(c_72,plain,
! [X_67,T_68] :
( greater('#skF_1'('#skF_3','#skF_8'),'#skF_1'(X_67,T_68))
| ~ complexity(X_67,'#skF_6',T_68)
| ~ class(X_67,'#skF_5',T_68)
| ~ organization(X_67,T_68) ),
inference(demodulation,[status(thm),theory(equality)],[c_30,c_12,c_52]) ).
tff(c_6,plain,
! [Y_14,Rt_15,Tc_21,C_16,I1_17,Tb_20,Ta_19,X_13,I2_18] :
( greater(Tc_21,Tb_20)
| ~ greater(I2_18,I1_17)
| ~ inertia(Y_14,I2_18,Ta_19)
| ~ inertia(X_13,I1_17,Ta_19)
| ~ reorganization_type(Y_14,Rt_15,Ta_19)
| ~ reorganization_type(X_13,Rt_15,Ta_19)
| ~ reorganization(Y_14,Ta_19,Tc_21)
| ~ reorganization(X_13,Ta_19,Tb_20)
| ~ class(Y_14,C_16,Ta_19)
| ~ class(X_13,C_16,Ta_19)
| ~ organization(Y_14,Tc_21)
| ~ organization(Y_14,Ta_19)
| ~ organization(X_13,Ta_19) ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_90,plain,
! [X_92,Rt_86,Y_88,Ta_89,X_87,C_91,Tc_94,Tb_93,T_90] :
( greater(Tc_94,Tb_93)
| ~ inertia(Y_88,'#skF_1'('#skF_3','#skF_8'),Ta_89)
| ~ inertia(X_87,'#skF_1'(X_92,T_90),Ta_89)
| ~ reorganization_type(Y_88,Rt_86,Ta_89)
| ~ reorganization_type(X_87,Rt_86,Ta_89)
| ~ reorganization(Y_88,Ta_89,Tc_94)
| ~ reorganization(X_87,Ta_89,Tb_93)
| ~ class(Y_88,C_91,Ta_89)
| ~ class(X_87,C_91,Ta_89)
| ~ organization(Y_88,Tc_94)
| ~ organization(Y_88,Ta_89)
| ~ organization(X_87,Ta_89)
| ~ complexity(X_92,'#skF_6',T_90)
| ~ class(X_92,'#skF_5',T_90)
| ~ organization(X_92,T_90) ),
inference(resolution,[status(thm)],[c_72,c_6]) ).
tff(c_93,plain,
! [X_92,Rt_86,X_87,C_91,Tc_94,Tb_93,T_90] :
( greater(Tc_94,Tb_93)
| ~ inertia(X_87,'#skF_1'(X_92,T_90),'#skF_8')
| ~ reorganization_type('#skF_3',Rt_86,'#skF_8')
| ~ reorganization_type(X_87,Rt_86,'#skF_8')
| ~ reorganization('#skF_3','#skF_8',Tc_94)
| ~ reorganization(X_87,'#skF_8',Tb_93)
| ~ class('#skF_3',C_91,'#skF_8')
| ~ class(X_87,C_91,'#skF_8')
| ~ organization('#skF_3',Tc_94)
| ~ organization(X_87,'#skF_8')
| ~ complexity(X_92,'#skF_6',T_90)
| ~ class(X_92,'#skF_5',T_90)
| ~ organization(X_92,T_90)
| ~ organization('#skF_3','#skF_8') ),
inference(resolution,[status(thm)],[c_2,c_90]) ).
tff(c_98,plain,
! [C_103,Tc_102,T_107,Tb_104,Rt_108,X_106,X_105] :
( greater(Tc_102,Tb_104)
| ~ inertia(X_106,'#skF_1'(X_105,T_107),'#skF_8')
| ~ reorganization_type('#skF_3',Rt_108,'#skF_8')
| ~ reorganization_type(X_106,Rt_108,'#skF_8')
| ~ reorganization('#skF_3','#skF_8',Tc_102)
| ~ reorganization(X_106,'#skF_8',Tb_104)
| ~ class('#skF_3',C_103,'#skF_8')
| ~ class(X_106,C_103,'#skF_8')
| ~ organization('#skF_3',Tc_102)
| ~ organization(X_106,'#skF_8')
| ~ complexity(X_105,'#skF_6',T_107)
| ~ class(X_105,'#skF_5',T_107)
| ~ organization(X_105,T_107) ),
inference(demodulation,[status(thm),theory(equality)],[c_30,c_93]) ).
tff(c_103,plain,
! [Tb_113,X_110,Tc_111,Rt_109,C_112] :
( greater(Tc_111,Tb_113)
| ~ reorganization_type('#skF_3',Rt_109,'#skF_8')
| ~ reorganization_type(X_110,Rt_109,'#skF_8')
| ~ reorganization('#skF_3','#skF_8',Tc_111)
| ~ reorganization(X_110,'#skF_8',Tb_113)
| ~ class('#skF_3',C_112,'#skF_8')
| ~ class(X_110,C_112,'#skF_8')
| ~ organization('#skF_3',Tc_111)
| ~ complexity(X_110,'#skF_6','#skF_8')
| ~ class(X_110,'#skF_5','#skF_8')
| ~ organization(X_110,'#skF_8') ),
inference(resolution,[status(thm)],[c_2,c_98]) ).
tff(c_107,plain,
! [Tc_114,Tb_115,X_116,C_117] :
( greater(Tc_114,Tb_115)
| ~ reorganization_type(X_116,'#skF_4','#skF_8')
| ~ reorganization('#skF_3','#skF_8',Tc_114)
| ~ reorganization(X_116,'#skF_8',Tb_115)
| ~ class('#skF_3',C_117,'#skF_8')
| ~ class(X_116,C_117,'#skF_8')
| ~ organization('#skF_3',Tc_114)
| ~ complexity(X_116,'#skF_6','#skF_8')
| ~ class(X_116,'#skF_5','#skF_8')
| ~ organization(X_116,'#skF_8') ),
inference(resolution,[status(thm)],[c_16,c_103]) ).
tff(c_111,plain,
! [Tc_114,Tb_115,C_117] :
( greater(Tc_114,Tb_115)
| ~ reorganization('#skF_3','#skF_8',Tc_114)
| ~ reorganization('#skF_2','#skF_8',Tb_115)
| ~ class('#skF_3',C_117,'#skF_8')
| ~ class('#skF_2',C_117,'#skF_8')
| ~ organization('#skF_3',Tc_114)
| ~ complexity('#skF_2','#skF_6','#skF_8')
| ~ class('#skF_2','#skF_5','#skF_8')
| ~ organization('#skF_2','#skF_8') ),
inference(resolution,[status(thm)],[c_18,c_107]) ).
tff(c_117,plain,
! [Tc_114,Tb_115,C_117] :
( greater(Tc_114,Tb_115)
| ~ reorganization('#skF_3','#skF_8',Tc_114)
| ~ reorganization('#skF_2','#skF_8',Tb_115)
| ~ class('#skF_3',C_117,'#skF_8')
| ~ class('#skF_2',C_117,'#skF_8')
| ~ organization('#skF_3',Tc_114) ),
inference(demodulation,[status(thm),theory(equality)],[c_32,c_26,c_14,c_111]) ).
tff(c_120,plain,
! [C_118] :
( ~ class('#skF_3',C_118,'#skF_8')
| ~ class('#skF_2',C_118,'#skF_8') ),
inference(splitLeft,[status(thm)],[c_117]) ).
tff(c_123,plain,
~ class('#skF_3','#skF_5','#skF_8'),
inference(resolution,[status(thm)],[c_26,c_120]) ).
tff(c_127,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_24,c_123]) ).
tff(c_129,plain,
! [Tc_119,Tb_120] :
( greater(Tc_119,Tb_120)
| ~ reorganization('#skF_3','#skF_8',Tc_119)
| ~ reorganization('#skF_2','#skF_8',Tb_120)
| ~ organization('#skF_3',Tc_119) ),
inference(splitRight,[status(thm)],[c_117]) ).
tff(c_131,plain,
! [Tb_120] :
( greater('#skF_10',Tb_120)
| ~ reorganization('#skF_2','#skF_8',Tb_120)
| ~ organization('#skF_3','#skF_10') ),
inference(resolution,[status(thm)],[c_20,c_129]) ).
tff(c_135,plain,
! [Tb_121] :
( greater('#skF_10',Tb_121)
| ~ reorganization('#skF_2','#skF_8',Tb_121) ),
inference(demodulation,[status(thm),theory(equality)],[c_28,c_131]) ).
tff(c_138,plain,
greater('#skF_10','#skF_9'),
inference(resolution,[status(thm)],[c_22,c_135]) ).
tff(c_142,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8,c_138]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT015+1 : TPTP v9.3.0. Released v2.0.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.12/0.37 % Computer : n031.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 7 11:57:41 UTC 2026
% 0.12/0.38 % CPUTime :
% 3.96/2.54 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.96/2.55
% 3.96/2.55 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------