%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MGT010+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/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 : n026.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 : Theorem 5.62s 2.40s
% Output : CNFRefutation 5.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 4
% Syntax : Number of formulae : 79 ( 33 unt; 0 typ; 0 def)
% Number of atoms : 331 ( 0 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 484 ( 232 ~; 216 |; 31 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 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 : 9 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 11 con; 0-2 aty)
% Number of variables : 214 ( 213 !; 1 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ size > reproducibility > reorganization_free > reliability > class > accountability > organization > greater > #nlpp > #skF_11 > #skF_7 > #skF_10 > #skF_5 > #skF_6 > #skF_2 > #skF_3 > #skF_9 > #skF_8 > #skF_4 > #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(reliability,type,
reliability: ( $i * $i * $i ) > $o ).
tff(reproducibility,type,
reproducibility: ( $i * $i * $i ) > $o ).
tff(size,type,
size: ( $i * $i * $i ) > $o ).
tff('#skF_11',type,
'#skF_11': $i ).
tff(accountability,type,
accountability: ( $i * $i * $i ) > $o ).
tff('#skF_7',type,
'#skF_7': $i ).
tff('#skF_10',type,
'#skF_10': $i ).
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_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('#skF_12',type,
'#skF_12': $i ).
tff(f_112,negated_conjecture,
~ ! [X,Y,C,R1,R2,A1,A2,S1,S2,T1,T2] :
( ( organization(X,T1)
& organization(Y,T2)
& reorganization_free(X,T1,T1)
& reorganization_free(Y,T2,T2)
& class(X,C,T1)
& class(Y,C,T2)
& reliability(X,R1,T1)
& reliability(Y,R2,T2)
& accountability(X,A1,T1)
& accountability(Y,A2,T2)
& size(X,S1,T1)
& size(Y,S2,T2)
& greater(S2,S1) )
=> ( greater(R2,R1)
& greater(A2,A1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_FOL) ).
tff(f_33,axiom,
! [X,T] :
( organization(X,T)
=> ? [Rp] : reproducibility(X,Rp,T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp3) ).
tff(f_81,hypothesis,
! [X,Y,C,Rp1,Rp2,S1,S2,T1,T2] :
( ( organization(X,T1)
& organization(Y,T2)
& reorganization_free(X,T1,T1)
& reorganization_free(Y,T2,T2)
& class(X,C,T1)
& class(Y,C,T2)
& reproducibility(X,Rp1,T1)
& reproducibility(Y,Rp2,T2)
& size(X,S1,T1)
& size(Y,S2,T2)
& greater(S2,S1) )
=> greater(Rp2,Rp1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t9_FOL) ).
tff(f_57,hypothesis,
! [X,Y,T1,T2,R1,R2,A1,A2,Rp1,Rp2] :
( ( organization(X,T1)
& organization(Y,T2)
& reliability(X,R1,T1)
& reliability(Y,R2,T2)
& accountability(X,A1,T1)
& accountability(Y,A2,T2)
& reproducibility(X,Rp1,T1)
& reproducibility(Y,Rp2,T2) )
=> ( greater(Rp2,Rp1)
<=> ( greater(R2,R1)
& greater(A2,A1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2_FOL) ).
tff(c_38,plain,
organization('#skF_2','#skF_11'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
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_33]) ).
tff(c_12,plain,
( ~ greater('#skF_8','#skF_7')
| ~ greater('#skF_6','#skF_5') ),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_39,plain,
~ greater('#skF_6','#skF_5'),
inference(splitLeft,[status(thm)],[c_12]) ).
tff(c_26,plain,
reliability('#skF_2','#skF_5','#skF_11'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_24,plain,
reliability('#skF_3','#skF_6','#skF_12'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_22,plain,
accountability('#skF_2','#skF_7','#skF_11'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_36,plain,
organization('#skF_3','#skF_12'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_28,plain,
class('#skF_3','#skF_4','#skF_12'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_30,plain,
class('#skF_2','#skF_4','#skF_11'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_34,plain,
reorganization_free('#skF_2','#skF_11','#skF_11'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_18,plain,
size('#skF_2','#skF_9','#skF_11'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_32,plain,
reorganization_free('#skF_3','#skF_12','#skF_12'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_16,plain,
size('#skF_3','#skF_10','#skF_12'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_14,plain,
greater('#skF_10','#skF_9'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_80,plain,
! [S2_95,Rp2_96,T1_99,T2_94,X_98,S1_102,Rp1_101,C_100,Y_97] :
( greater(Rp2_96,Rp1_101)
| ~ greater(S2_95,S1_102)
| ~ size(Y_97,S2_95,T2_94)
| ~ size(X_98,S1_102,T1_99)
| ~ reproducibility(Y_97,Rp2_96,T2_94)
| ~ reproducibility(X_98,Rp1_101,T1_99)
| ~ class(Y_97,C_100,T2_94)
| ~ class(X_98,C_100,T1_99)
| ~ reorganization_free(Y_97,T2_94,T2_94)
| ~ reorganization_free(X_98,T1_99,T1_99)
| ~ organization(Y_97,T2_94)
| ~ organization(X_98,T1_99) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_87,plain,
! [Y_108,Rp2_106,X_103,Rp1_104,T1_105,C_107,T2_109] :
( greater(Rp2_106,Rp1_104)
| ~ size(Y_108,'#skF_10',T2_109)
| ~ size(X_103,'#skF_9',T1_105)
| ~ reproducibility(Y_108,Rp2_106,T2_109)
| ~ reproducibility(X_103,Rp1_104,T1_105)
| ~ class(Y_108,C_107,T2_109)
| ~ class(X_103,C_107,T1_105)
| ~ reorganization_free(Y_108,T2_109,T2_109)
| ~ reorganization_free(X_103,T1_105,T1_105)
| ~ organization(Y_108,T2_109)
| ~ organization(X_103,T1_105) ),
inference(resolution,[status(thm)],[c_14,c_80]) ).
tff(c_89,plain,
! [Rp2_106,X_103,Rp1_104,T1_105,C_107] :
( greater(Rp2_106,Rp1_104)
| ~ size(X_103,'#skF_9',T1_105)
| ~ reproducibility('#skF_3',Rp2_106,'#skF_12')
| ~ reproducibility(X_103,Rp1_104,T1_105)
| ~ class('#skF_3',C_107,'#skF_12')
| ~ class(X_103,C_107,T1_105)
| ~ reorganization_free('#skF_3','#skF_12','#skF_12')
| ~ reorganization_free(X_103,T1_105,T1_105)
| ~ organization('#skF_3','#skF_12')
| ~ organization(X_103,T1_105) ),
inference(resolution,[status(thm)],[c_16,c_87]) ).
tff(c_93,plain,
! [X_111,C_114,T1_113,Rp2_110,Rp1_112] :
( greater(Rp2_110,Rp1_112)
| ~ size(X_111,'#skF_9',T1_113)
| ~ reproducibility('#skF_3',Rp2_110,'#skF_12')
| ~ reproducibility(X_111,Rp1_112,T1_113)
| ~ class('#skF_3',C_114,'#skF_12')
| ~ class(X_111,C_114,T1_113)
| ~ reorganization_free(X_111,T1_113,T1_113)
| ~ organization(X_111,T1_113) ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_32,c_89]) ).
tff(c_95,plain,
! [Rp2_110,Rp1_112,C_114] :
( greater(Rp2_110,Rp1_112)
| ~ reproducibility('#skF_3',Rp2_110,'#skF_12')
| ~ reproducibility('#skF_2',Rp1_112,'#skF_11')
| ~ class('#skF_3',C_114,'#skF_12')
| ~ class('#skF_2',C_114,'#skF_11')
| ~ reorganization_free('#skF_2','#skF_11','#skF_11')
| ~ organization('#skF_2','#skF_11') ),
inference(resolution,[status(thm)],[c_18,c_93]) ).
tff(c_98,plain,
! [Rp2_110,Rp1_112,C_114] :
( greater(Rp2_110,Rp1_112)
| ~ reproducibility('#skF_3',Rp2_110,'#skF_12')
| ~ reproducibility('#skF_2',Rp1_112,'#skF_11')
| ~ class('#skF_3',C_114,'#skF_12')
| ~ class('#skF_2',C_114,'#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_34,c_95]) ).
tff(c_104,plain,
! [C_125] :
( ~ class('#skF_3',C_125,'#skF_12')
| ~ class('#skF_2',C_125,'#skF_11') ),
inference(splitLeft,[status(thm)],[c_98]) ).
tff(c_107,plain,
~ class('#skF_3','#skF_4','#skF_12'),
inference(resolution,[status(thm)],[c_30,c_104]) ).
tff(c_111,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_28,c_107]) ).
tff(c_113,plain,
! [Rp2_126,Rp1_127] :
( greater(Rp2_126,Rp1_127)
| ~ reproducibility('#skF_3',Rp2_126,'#skF_12')
| ~ reproducibility('#skF_2',Rp1_127,'#skF_11') ),
inference(splitRight,[status(thm)],[c_98]) ).
tff(c_116,plain,
! [Rp1_127] :
( greater('#skF_1'('#skF_3','#skF_12'),Rp1_127)
| ~ reproducibility('#skF_2',Rp1_127,'#skF_11')
| ~ organization('#skF_3','#skF_12') ),
inference(resolution,[status(thm)],[c_2,c_113]) ).
tff(c_120,plain,
! [Rp1_128] :
( greater('#skF_1'('#skF_3','#skF_12'),Rp1_128)
| ~ reproducibility('#skF_2',Rp1_128,'#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_116]) ).
tff(c_8,plain,
! [Rp2_13,Rp1_12,T1_6,A2_11,X_4,A1_10,Y_5,T2_7,R2_9,R1_8] :
( greater(R2_9,R1_8)
| ~ greater(Rp2_13,Rp1_12)
| ~ reproducibility(Y_5,Rp2_13,T2_7)
| ~ reproducibility(X_4,Rp1_12,T1_6)
| ~ accountability(Y_5,A2_11,T2_7)
| ~ accountability(X_4,A1_10,T1_6)
| ~ reliability(Y_5,R2_9,T2_7)
| ~ reliability(X_4,R1_8,T1_6)
| ~ organization(Y_5,T2_7)
| ~ organization(X_4,T1_6) ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_144,plain,
! [T2_144,X_149,Y_147,R2_146,T1_145,A2_148,A1_142,R1_143,Rp1_150] :
( greater(R2_146,R1_143)
| ~ reproducibility(Y_147,'#skF_1'('#skF_3','#skF_12'),T2_144)
| ~ reproducibility(X_149,Rp1_150,T1_145)
| ~ accountability(Y_147,A2_148,T2_144)
| ~ accountability(X_149,A1_142,T1_145)
| ~ reliability(Y_147,R2_146,T2_144)
| ~ reliability(X_149,R1_143,T1_145)
| ~ organization(Y_147,T2_144)
| ~ organization(X_149,T1_145)
| ~ reproducibility('#skF_2',Rp1_150,'#skF_11') ),
inference(resolution,[status(thm)],[c_120,c_8]) ).
tff(c_147,plain,
! [X_149,R2_146,T1_145,A2_148,A1_142,R1_143,Rp1_150] :
( greater(R2_146,R1_143)
| ~ reproducibility(X_149,Rp1_150,T1_145)
| ~ accountability('#skF_3',A2_148,'#skF_12')
| ~ accountability(X_149,A1_142,T1_145)
| ~ reliability('#skF_3',R2_146,'#skF_12')
| ~ reliability(X_149,R1_143,T1_145)
| ~ organization(X_149,T1_145)
| ~ reproducibility('#skF_2',Rp1_150,'#skF_11')
| ~ organization('#skF_3','#skF_12') ),
inference(resolution,[status(thm)],[c_2,c_144]) ).
tff(c_150,plain,
! [X_149,R2_146,T1_145,A2_148,A1_142,R1_143,Rp1_150] :
( greater(R2_146,R1_143)
| ~ reproducibility(X_149,Rp1_150,T1_145)
| ~ accountability('#skF_3',A2_148,'#skF_12')
| ~ accountability(X_149,A1_142,T1_145)
| ~ reliability('#skF_3',R2_146,'#skF_12')
| ~ reliability(X_149,R1_143,T1_145)
| ~ organization(X_149,T1_145)
| ~ reproducibility('#skF_2',Rp1_150,'#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_147]) ).
tff(c_151,plain,
! [A2_148] : ~ accountability('#skF_3',A2_148,'#skF_12'),
inference(splitLeft,[status(thm)],[c_150]) ).
tff(c_20,plain,
accountability('#skF_3','#skF_8','#skF_12'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_153,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_151,c_20]) ).
tff(c_155,plain,
! [A1_154,R2_151,Rp1_156,T1_152,R1_155,X_153] :
( ~ reproducibility(X_153,Rp1_156,T1_152)
| ~ accountability(X_153,A1_154,T1_152)
| greater(R2_151,R1_155)
| ~ reliability('#skF_3',R2_151,'#skF_12')
| ~ reliability(X_153,R1_155,T1_152)
| ~ organization(X_153,T1_152)
| ~ reproducibility('#skF_2',Rp1_156,'#skF_11') ),
inference(splitRight,[status(thm)],[c_150]) ).
tff(c_163,plain,
! [T_167,R1_170,A1_168,R2_171,X_169] :
( ~ accountability(X_169,A1_168,T_167)
| greater(R2_171,R1_170)
| ~ reliability('#skF_3',R2_171,'#skF_12')
| ~ reliability(X_169,R1_170,T_167)
| ~ reproducibility('#skF_2','#skF_1'(X_169,T_167),'#skF_11')
| ~ organization(X_169,T_167) ),
inference(resolution,[status(thm)],[c_2,c_155]) ).
tff(c_167,plain,
! [R2_171,R1_170] :
( greater(R2_171,R1_170)
| ~ reliability('#skF_3',R2_171,'#skF_12')
| ~ reliability('#skF_2',R1_170,'#skF_11')
| ~ reproducibility('#skF_2','#skF_1'('#skF_2','#skF_11'),'#skF_11')
| ~ organization('#skF_2','#skF_11') ),
inference(resolution,[status(thm)],[c_22,c_163]) ).
tff(c_173,plain,
! [R2_171,R1_170] :
( greater(R2_171,R1_170)
| ~ reliability('#skF_3',R2_171,'#skF_12')
| ~ reliability('#skF_2',R1_170,'#skF_11')
| ~ reproducibility('#skF_2','#skF_1'('#skF_2','#skF_11'),'#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_167]) ).
tff(c_175,plain,
~ reproducibility('#skF_2','#skF_1'('#skF_2','#skF_11'),'#skF_11'),
inference(splitLeft,[status(thm)],[c_173]) ).
tff(c_178,plain,
~ organization('#skF_2','#skF_11'),
inference(resolution,[status(thm)],[c_2,c_175]) ).
tff(c_182,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_38,c_178]) ).
tff(c_222,plain,
! [R2_181,R1_182] :
( greater(R2_181,R1_182)
| ~ reliability('#skF_3',R2_181,'#skF_12')
| ~ reliability('#skF_2',R1_182,'#skF_11') ),
inference(splitRight,[status(thm)],[c_173]) ).
tff(c_226,plain,
! [R1_183] :
( greater('#skF_6',R1_183)
| ~ reliability('#skF_2',R1_183,'#skF_11') ),
inference(resolution,[status(thm)],[c_24,c_222]) ).
tff(c_229,plain,
greater('#skF_6','#skF_5'),
inference(resolution,[status(thm)],[c_26,c_226]) ).
tff(c_233,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_39,c_229]) ).
tff(c_234,plain,
~ greater('#skF_8','#skF_7'),
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_298,plain,
! [S1_290,Rp2_284,X_286,C_288,S2_283,Rp1_289,T1_287,T2_282,Y_285] :
( greater(Rp2_284,Rp1_289)
| ~ greater(S2_283,S1_290)
| ~ size(Y_285,S2_283,T2_282)
| ~ size(X_286,S1_290,T1_287)
| ~ reproducibility(Y_285,Rp2_284,T2_282)
| ~ reproducibility(X_286,Rp1_289,T1_287)
| ~ class(Y_285,C_288,T2_282)
| ~ class(X_286,C_288,T1_287)
| ~ reorganization_free(Y_285,T2_282,T2_282)
| ~ reorganization_free(X_286,T1_287,T1_287)
| ~ organization(Y_285,T2_282)
| ~ organization(X_286,T1_287) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_391,plain,
! [Rp2_334,C_337,T1_333,Y_336,X_338,Rp1_339,T2_335] :
( greater(Rp2_334,Rp1_339)
| ~ size(Y_336,'#skF_10',T2_335)
| ~ size(X_338,'#skF_9',T1_333)
| ~ reproducibility(Y_336,Rp2_334,T2_335)
| ~ reproducibility(X_338,Rp1_339,T1_333)
| ~ class(Y_336,C_337,T2_335)
| ~ class(X_338,C_337,T1_333)
| ~ reorganization_free(Y_336,T2_335,T2_335)
| ~ reorganization_free(X_338,T1_333,T1_333)
| ~ organization(Y_336,T2_335)
| ~ organization(X_338,T1_333) ),
inference(resolution,[status(thm)],[c_14,c_298]) ).
tff(c_393,plain,
! [Rp2_334,C_337,T1_333,X_338,Rp1_339] :
( greater(Rp2_334,Rp1_339)
| ~ size(X_338,'#skF_9',T1_333)
| ~ reproducibility('#skF_3',Rp2_334,'#skF_12')
| ~ reproducibility(X_338,Rp1_339,T1_333)
| ~ class('#skF_3',C_337,'#skF_12')
| ~ class(X_338,C_337,T1_333)
| ~ reorganization_free('#skF_3','#skF_12','#skF_12')
| ~ reorganization_free(X_338,T1_333,T1_333)
| ~ organization('#skF_3','#skF_12')
| ~ organization(X_338,T1_333) ),
inference(resolution,[status(thm)],[c_16,c_391]) ).
tff(c_398,plain,
! [Rp2_349,Rp1_348,C_351,T1_350,X_347] :
( greater(Rp2_349,Rp1_348)
| ~ size(X_347,'#skF_9',T1_350)
| ~ reproducibility('#skF_3',Rp2_349,'#skF_12')
| ~ reproducibility(X_347,Rp1_348,T1_350)
| ~ class('#skF_3',C_351,'#skF_12')
| ~ class(X_347,C_351,T1_350)
| ~ reorganization_free(X_347,T1_350,T1_350)
| ~ organization(X_347,T1_350) ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_32,c_393]) ).
tff(c_400,plain,
! [Rp2_349,Rp1_348,C_351] :
( greater(Rp2_349,Rp1_348)
| ~ reproducibility('#skF_3',Rp2_349,'#skF_12')
| ~ reproducibility('#skF_2',Rp1_348,'#skF_11')
| ~ class('#skF_3',C_351,'#skF_12')
| ~ class('#skF_2',C_351,'#skF_11')
| ~ reorganization_free('#skF_2','#skF_11','#skF_11')
| ~ organization('#skF_2','#skF_11') ),
inference(resolution,[status(thm)],[c_18,c_398]) ).
tff(c_403,plain,
! [Rp2_349,Rp1_348,C_351] :
( greater(Rp2_349,Rp1_348)
| ~ reproducibility('#skF_3',Rp2_349,'#skF_12')
| ~ reproducibility('#skF_2',Rp1_348,'#skF_11')
| ~ class('#skF_3',C_351,'#skF_12')
| ~ class('#skF_2',C_351,'#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_34,c_400]) ).
tff(c_405,plain,
! [C_352] :
( ~ class('#skF_3',C_352,'#skF_12')
| ~ class('#skF_2',C_352,'#skF_11') ),
inference(splitLeft,[status(thm)],[c_403]) ).
tff(c_408,plain,
~ class('#skF_3','#skF_4','#skF_12'),
inference(resolution,[status(thm)],[c_30,c_405]) ).
tff(c_412,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_28,c_408]) ).
tff(c_418,plain,
! [Rp2_363,Rp1_364] :
( greater(Rp2_363,Rp1_364)
| ~ reproducibility('#skF_3',Rp2_363,'#skF_12')
| ~ reproducibility('#skF_2',Rp1_364,'#skF_11') ),
inference(splitRight,[status(thm)],[c_403]) ).
tff(c_421,plain,
! [Rp1_364] :
( greater('#skF_1'('#skF_3','#skF_12'),Rp1_364)
| ~ reproducibility('#skF_2',Rp1_364,'#skF_11')
| ~ organization('#skF_3','#skF_12') ),
inference(resolution,[status(thm)],[c_2,c_418]) ).
tff(c_425,plain,
! [Rp1_365] :
( greater('#skF_1'('#skF_3','#skF_12'),Rp1_365)
| ~ reproducibility('#skF_2',Rp1_365,'#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_421]) ).
tff(c_6,plain,
! [Rp2_13,Rp1_12,T1_6,A2_11,X_4,A1_10,Y_5,T2_7,R2_9,R1_8] :
( greater(A2_11,A1_10)
| ~ greater(Rp2_13,Rp1_12)
| ~ reproducibility(Y_5,Rp2_13,T2_7)
| ~ reproducibility(X_4,Rp1_12,T1_6)
| ~ accountability(Y_5,A2_11,T2_7)
| ~ accountability(X_4,A1_10,T1_6)
| ~ reliability(Y_5,R2_9,T2_7)
| ~ reliability(X_4,R1_8,T1_6)
| ~ organization(Y_5,T2_7)
| ~ organization(X_4,T1_6) ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_463,plain,
! [R2_388,T2_386,X_392,A1_384,T1_387,R1_385,Y_389,A2_390,Rp1_391] :
( greater(A2_390,A1_384)
| ~ reproducibility(Y_389,'#skF_1'('#skF_3','#skF_12'),T2_386)
| ~ reproducibility(X_392,Rp1_391,T1_387)
| ~ accountability(Y_389,A2_390,T2_386)
| ~ accountability(X_392,A1_384,T1_387)
| ~ reliability(Y_389,R2_388,T2_386)
| ~ reliability(X_392,R1_385,T1_387)
| ~ organization(Y_389,T2_386)
| ~ organization(X_392,T1_387)
| ~ reproducibility('#skF_2',Rp1_391,'#skF_11') ),
inference(resolution,[status(thm)],[c_425,c_6]) ).
tff(c_466,plain,
! [R2_388,X_392,A1_384,T1_387,R1_385,A2_390,Rp1_391] :
( greater(A2_390,A1_384)
| ~ reproducibility(X_392,Rp1_391,T1_387)
| ~ accountability('#skF_3',A2_390,'#skF_12')
| ~ accountability(X_392,A1_384,T1_387)
| ~ reliability('#skF_3',R2_388,'#skF_12')
| ~ reliability(X_392,R1_385,T1_387)
| ~ organization(X_392,T1_387)
| ~ reproducibility('#skF_2',Rp1_391,'#skF_11')
| ~ organization('#skF_3','#skF_12') ),
inference(resolution,[status(thm)],[c_2,c_463]) ).
tff(c_469,plain,
! [R2_388,X_392,A1_384,T1_387,R1_385,A2_390,Rp1_391] :
( greater(A2_390,A1_384)
| ~ reproducibility(X_392,Rp1_391,T1_387)
| ~ accountability('#skF_3',A2_390,'#skF_12')
| ~ accountability(X_392,A1_384,T1_387)
| ~ reliability('#skF_3',R2_388,'#skF_12')
| ~ reliability(X_392,R1_385,T1_387)
| ~ organization(X_392,T1_387)
| ~ reproducibility('#skF_2',Rp1_391,'#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_466]) ).
tff(c_476,plain,
! [R2_388] : ~ reliability('#skF_3',R2_388,'#skF_12'),
inference(splitLeft,[status(thm)],[c_469]) ).
tff(c_478,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_476,c_24]) ).
tff(c_480,plain,
! [R1_403,X_404,Rp1_401,A2_402,A1_405,T1_400] :
( ~ reproducibility(X_404,Rp1_401,T1_400)
| greater(A2_402,A1_405)
| ~ accountability('#skF_3',A2_402,'#skF_12')
| ~ accountability(X_404,A1_405,T1_400)
| ~ reliability(X_404,R1_403,T1_400)
| ~ organization(X_404,T1_400)
| ~ reproducibility('#skF_2',Rp1_401,'#skF_11') ),
inference(splitRight,[status(thm)],[c_469]) ).
tff(c_484,plain,
! [A2_409,T_406,R1_410,X_407,A1_408] :
( greater(A2_409,A1_408)
| ~ accountability('#skF_3',A2_409,'#skF_12')
| ~ accountability(X_407,A1_408,T_406)
| ~ reliability(X_407,R1_410,T_406)
| ~ reproducibility('#skF_2','#skF_1'(X_407,T_406),'#skF_11')
| ~ organization(X_407,T_406) ),
inference(resolution,[status(thm)],[c_2,c_480]) ).
tff(c_495,plain,
! [A1_420,X_421,T_422,R1_423] :
( greater('#skF_8',A1_420)
| ~ accountability(X_421,A1_420,T_422)
| ~ reliability(X_421,R1_423,T_422)
| ~ reproducibility('#skF_2','#skF_1'(X_421,T_422),'#skF_11')
| ~ organization(X_421,T_422) ),
inference(resolution,[status(thm)],[c_20,c_484]) ).
tff(c_499,plain,
! [R1_423] :
( greater('#skF_8','#skF_7')
| ~ reliability('#skF_2',R1_423,'#skF_11')
| ~ reproducibility('#skF_2','#skF_1'('#skF_2','#skF_11'),'#skF_11')
| ~ organization('#skF_2','#skF_11') ),
inference(resolution,[status(thm)],[c_22,c_495]) ).
tff(c_505,plain,
! [R1_423] :
( greater('#skF_8','#skF_7')
| ~ reliability('#skF_2',R1_423,'#skF_11')
| ~ reproducibility('#skF_2','#skF_1'('#skF_2','#skF_11'),'#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_499]) ).
tff(c_506,plain,
! [R1_423] :
( ~ reliability('#skF_2',R1_423,'#skF_11')
| ~ reproducibility('#skF_2','#skF_1'('#skF_2','#skF_11'),'#skF_11') ),
inference(negUnitSimplification,[status(thm)],[c_234,c_505]) ).
tff(c_507,plain,
~ reproducibility('#skF_2','#skF_1'('#skF_2','#skF_11'),'#skF_11'),
inference(splitLeft,[status(thm)],[c_506]) ).
tff(c_510,plain,
~ organization('#skF_2','#skF_11'),
inference(resolution,[status(thm)],[c_2,c_507]) ).
tff(c_514,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_38,c_510]) ).
tff(c_515,plain,
! [R1_423] : ~ reliability('#skF_2',R1_423,'#skF_11'),
inference(splitRight,[status(thm)],[c_506]) ).
tff(c_519,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_515,c_26]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT010+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/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.09/0.36 % Computer : n026.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 7 11:50:27 UTC 2026
% 0.12/0.36 % CPUTime :
% 5.62/2.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.62/2.42
% 5.62/2.42 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------