%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MED001+1 : TPTP v9.0.0. Released v3.2.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 : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 07:41:05 PM UTC 2025
% Result : Theorem 7.49s 2.79s
% Output : CNFRefutation 7.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 4
% Syntax : Number of formulae : 99 ( 37 unt; 0 typ; 0 def)
% Number of atoms : 294 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 306 ( 111 ~; 177 |; 7 &)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 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 : 16 ( 15 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 2 con; 0-1 aty)
% Number of variables : 83 ( 83 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ gt > uptakepg > uptakelg > releaselg > qilt27 > drugsu > drugi > drugbg > conditionnormo > conditionhypo > conditionhyper > bsecretioni > bcapacitysn > bcapacityne > bcapacityex > #nlpp > n0 > #skF_9 > #skF_7 > #skF_5 > #skF_2 > #skF_4 > #skF_15 > #skF_1 > #skF_8 > #skF_10 > #skF_13 > #skF_3 > #skF_11 > #skF_14 > #skF_12 > #skF_6
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(bsecretioni,type,
bsecretioni: $i > $o ).
tff(conditionnormo,type,
conditionnormo: $i > $o ).
tff('#skF_9',type,
'#skF_9': $i > $i ).
tff('#skF_7',type,
'#skF_7': $i > $i ).
tff('#skF_5',type,
'#skF_5': $i > $i ).
tff(conditionhypo,type,
conditionhypo: $i > $o ).
tff('#skF_2',type,
'#skF_2': $i > $i ).
tff('#skF_4',type,
'#skF_4': $i > $i ).
tff('#skF_15',type,
'#skF_15': $i ).
tff('#skF_1',type,
'#skF_1': $i > $i ).
tff(drugi,type,
drugi: $i > $o ).
tff(releaselg,type,
releaselg: $i > $o ).
tff(drugbg,type,
drugbg: $i > $o ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff(bcapacityex,type,
bcapacityex: $i > $o ).
tff(bcapacityne,type,
bcapacityne: $i > $o ).
tff(drugsu,type,
drugsu: $i > $o ).
tff('#skF_10',type,
'#skF_10': $i > $i ).
tff(uptakepg,type,
uptakepg: $i > $o ).
tff(qilt27,type,
qilt27: $i > $o ).
tff(n0,type,
n0: $i ).
tff(gt,type,
gt: ( $i * $i ) > $o ).
tff(bcapacitysn,type,
bcapacitysn: $i > $o ).
tff('#skF_13',type,
'#skF_13': $i > $i ).
tff(uptakelg,type,
uptakelg: $i > $o ).
tff('#skF_3',type,
'#skF_3': $i > $i ).
tff('#skF_11',type,
'#skF_11': $i > $i ).
tff('#skF_14',type,
'#skF_14': $i > $i ).
tff('#skF_12',type,
'#skF_12': $i > $i ).
tff('#skF_6',type,
'#skF_6': $i > $i ).
tff(conditionhyper,type,
conditionhyper: $i > $o ).
tff(f_283,negated_conjecture,
~ ( ( ! [X0] :
( ~ gt(n0,X0)
=> drugsu(X0) )
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& bcapacitysn(n0)
& qilt27(n0) )
=> ! [X0] :
( ~ gt(n0,X0)
=> conditionnormo(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',treatmentsn2) ).
tff(f_83,axiom,
! [X0] :
( ~ bcapacityex(X0)
| ~ bcapacitysn(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MED001+0.ax',xorcapacity4) ).
tff(f_144,axiom,
! [X0] :
( ( ! [X1] :
( ~ gt(X0,X1)
=> drugsu(X1) )
& ~ bcapacityex(X0) )
=> ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MED001+0.ax',sulfonylurea_effect) ).
tff(f_178,axiom,
! [X0] :
( ( ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) )
& bcapacitysn(X0)
& qilt27(X0)
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) ) )
=> ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MED001+0.ax',sn_cure_1) ).
tff(c_104,plain,
~ conditionnormo('#skF_15'),
inference(cnfTransformation,[status(thm)],[f_283]) ).
tff(c_110,plain,
bcapacitysn(n0),
inference(cnfTransformation,[status(thm)],[f_283]) ).
tff(c_108,plain,
qilt27(n0),
inference(cnfTransformation,[status(thm)],[f_283]) ).
tff(c_134,plain,
! [X0_58] :
( ~ bcapacitysn(X0_58)
| ~ bcapacityex(X0_58) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_138,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_110,c_134]) ).
tff(c_114,plain,
! [X0_50] :
( drugsu(X0_50)
| gt(n0,X0_50) ),
inference(cnfTransformation,[status(thm)],[f_283]) ).
tff(c_252,plain,
! [X0_89,X1_90] :
( ~ gt(X0_89,'#skF_2'(X0_89))
| bsecretioni(X1_90)
| gt(X0_89,X1_90)
| bcapacityex(X0_89) ),
inference(cnfTransformation,[status(thm)],[f_144]) ).
tff(c_258,plain,
! [X1_90] :
( bsecretioni(X1_90)
| gt(n0,X1_90)
| bcapacityex(n0)
| drugsu('#skF_2'(n0)) ),
inference(resolution,[status(thm)],[c_114,c_252]) ).
tff(c_262,plain,
! [X1_90] :
( bsecretioni(X1_90)
| gt(n0,X1_90)
| drugsu('#skF_2'(n0)) ),
inference(negUnitSimplification,[status(thm)],[c_138,c_258]) ).
tff(c_263,plain,
drugsu('#skF_2'(n0)),
inference(splitLeft,[status(thm)],[c_262]) ).
tff(c_32,plain,
! [X0_19,X1_22] :
( ~ drugsu('#skF_2'(X0_19))
| bsecretioni(X1_22)
| gt(X0_19,X1_22)
| bcapacityex(X0_19) ),
inference(cnfTransformation,[status(thm)],[f_144]) ).
tff(c_299,plain,
! [X1_22] :
( bsecretioni(X1_22)
| gt(n0,X1_22)
| bcapacityex(n0) ),
inference(resolution,[status(thm)],[c_263,c_32]) ).
tff(c_303,plain,
! [X1_93] :
( bsecretioni(X1_93)
| gt(n0,X1_93) ),
inference(negUnitSimplification,[status(thm)],[c_138,c_299]) ).
tff(c_112,plain,
! [X0_51] :
( conditionhyper(X0_51)
| ~ gt(n0,X0_51) ),
inference(cnfTransformation,[status(thm)],[f_283]) ).
tff(c_338,plain,
! [X1_93] :
( conditionhyper(X1_93)
| bsecretioni(X1_93) ),
inference(resolution,[status(thm)],[c_303,c_112]) ).
tff(c_344,plain,
! [X0_95,X1_96] :
( ~ bsecretioni('#skF_4'(X0_95))
| ~ conditionhyper('#skF_5'(X0_95))
| conditionnormo(X1_96)
| gt(X0_95,X1_96)
| ~ qilt27(X0_95)
| ~ bcapacitysn(X0_95) ),
inference(cnfTransformation,[status(thm)],[f_178]) ).
tff(c_364,plain,
! [X0_100,X1_101] :
( ~ bsecretioni('#skF_4'(X0_100))
| conditionnormo(X1_101)
| gt(X0_100,X1_101)
| ~ qilt27(X0_100)
| ~ bcapacitysn(X0_100)
| bsecretioni('#skF_5'(X0_100)) ),
inference(resolution,[status(thm)],[c_338,c_344]) ).
tff(c_384,plain,
! [X1_101] :
( conditionhyper(X1_101)
| ~ bsecretioni('#skF_4'(n0))
| conditionnormo(X1_101)
| ~ qilt27(n0)
| ~ bcapacitysn(n0)
| bsecretioni('#skF_5'(n0)) ),
inference(resolution,[status(thm)],[c_364,c_112]) ).
tff(c_397,plain,
! [X1_101] :
( conditionhyper(X1_101)
| ~ bsecretioni('#skF_4'(n0))
| conditionnormo(X1_101)
| bsecretioni('#skF_5'(n0)) ),
inference(demodulation,[status(thm),theory(equality)],[c_110,c_108,c_384]) ).
tff(c_399,plain,
~ bsecretioni('#skF_4'(n0)),
inference(splitLeft,[status(thm)],[c_397]) ).
tff(c_302,plain,
! [X1_22] :
( bsecretioni(X1_22)
| gt(n0,X1_22) ),
inference(negUnitSimplification,[status(thm)],[c_138,c_299]) ).
tff(c_437,plain,
! [X0_106,X1_107] :
( ~ gt(X0_106,'#skF_4'(X0_106))
| ~ conditionhyper('#skF_5'(X0_106))
| conditionnormo(X1_107)
| gt(X0_106,X1_107)
| ~ qilt27(X0_106)
| ~ bcapacitysn(X0_106) ),
inference(cnfTransformation,[status(thm)],[f_178]) ).
tff(c_446,plain,
! [X1_107] :
( ~ conditionhyper('#skF_5'(n0))
| conditionnormo(X1_107)
| gt(n0,X1_107)
| ~ qilt27(n0)
| ~ bcapacitysn(n0)
| bsecretioni('#skF_4'(n0)) ),
inference(resolution,[status(thm)],[c_302,c_437]) ).
tff(c_460,plain,
! [X1_107] :
( ~ conditionhyper('#skF_5'(n0))
| conditionnormo(X1_107)
| gt(n0,X1_107)
| bsecretioni('#skF_4'(n0)) ),
inference(demodulation,[status(thm),theory(equality)],[c_110,c_108,c_446]) ).
tff(c_461,plain,
! [X1_107] :
( ~ conditionhyper('#skF_5'(n0))
| conditionnormo(X1_107)
| gt(n0,X1_107) ),
inference(negUnitSimplification,[status(thm)],[c_399,c_460]) ).
tff(c_467,plain,
~ conditionhyper('#skF_5'(n0)),
inference(splitLeft,[status(thm)],[c_461]) ).
tff(c_1007,plain,
! [X0_146,X1_147] :
( ~ gt(X0_146,'#skF_4'(X0_146))
| gt(X0_146,'#skF_5'(X0_146))
| conditionnormo(X1_147)
| gt(X0_146,X1_147)
| ~ qilt27(X0_146)
| ~ bcapacitysn(X0_146) ),
inference(cnfTransformation,[status(thm)],[f_178]) ).
tff(c_1021,plain,
! [X1_147] :
( conditionhyper('#skF_5'(n0))
| ~ gt(n0,'#skF_4'(n0))
| conditionnormo(X1_147)
| gt(n0,X1_147)
| ~ qilt27(n0)
| ~ bcapacitysn(n0) ),
inference(resolution,[status(thm)],[c_1007,c_112]) ).
tff(c_1054,plain,
! [X1_147] :
( conditionhyper('#skF_5'(n0))
| ~ gt(n0,'#skF_4'(n0))
| conditionnormo(X1_147)
| gt(n0,X1_147) ),
inference(demodulation,[status(thm),theory(equality)],[c_110,c_108,c_1021]) ).
tff(c_1055,plain,
! [X1_147] :
( ~ gt(n0,'#skF_4'(n0))
| conditionnormo(X1_147)
| gt(n0,X1_147) ),
inference(negUnitSimplification,[status(thm)],[c_467,c_1054]) ).
tff(c_1064,plain,
~ gt(n0,'#skF_4'(n0)),
inference(splitLeft,[status(thm)],[c_1055]) ).
tff(c_1088,plain,
bsecretioni('#skF_4'(n0)),
inference(resolution,[status(thm)],[c_302,c_1064]) ).
tff(c_1117,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_399,c_1088]) ).
tff(c_1144,plain,
! [X1_148] :
( conditionnormo(X1_148)
| gt(n0,X1_148) ),
inference(splitRight,[status(thm)],[c_1055]) ).
tff(c_106,plain,
~ gt(n0,'#skF_15'),
inference(cnfTransformation,[status(thm)],[f_283]) ).
tff(c_1188,plain,
conditionnormo('#skF_15'),
inference(resolution,[status(thm)],[c_1144,c_106]) ).
tff(c_1212,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_104,c_1188]) ).
tff(c_1220,plain,
! [X1_149] :
( conditionnormo(X1_149)
| gt(n0,X1_149) ),
inference(splitRight,[status(thm)],[c_461]) ).
tff(c_1253,plain,
conditionnormo('#skF_15'),
inference(resolution,[status(thm)],[c_1220,c_106]) ).
tff(c_1270,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_104,c_1253]) ).
tff(c_1272,plain,
bsecretioni('#skF_4'(n0)),
inference(splitRight,[status(thm)],[c_397]) ).
tff(c_1274,plain,
! [X0_150,X1_151] :
( ~ gt(X0_150,'#skF_4'(X0_150))
| ~ conditionhyper('#skF_5'(X0_150))
| conditionnormo(X1_151)
| gt(X0_150,X1_151)
| ~ qilt27(X0_150)
| ~ bcapacitysn(X0_150) ),
inference(cnfTransformation,[status(thm)],[f_178]) ).
tff(c_1289,plain,
! [X1_151] :
( ~ conditionhyper('#skF_5'(n0))
| conditionnormo(X1_151)
| gt(n0,X1_151)
| ~ qilt27(n0)
| ~ bcapacitysn(n0)
| drugsu('#skF_4'(n0)) ),
inference(resolution,[status(thm)],[c_114,c_1274]) ).
tff(c_1298,plain,
! [X1_151] :
( ~ conditionhyper('#skF_5'(n0))
| conditionnormo(X1_151)
| gt(n0,X1_151)
| drugsu('#skF_4'(n0)) ),
inference(demodulation,[status(thm),theory(equality)],[c_110,c_108,c_1289]) ).
tff(c_1299,plain,
~ conditionhyper('#skF_5'(n0)),
inference(splitLeft,[status(thm)],[c_1298]) ).
tff(c_1439,plain,
! [X0_161,X1_162] :
( ~ bsecretioni('#skF_4'(X0_161))
| gt(X0_161,'#skF_5'(X0_161))
| conditionnormo(X1_162)
| gt(X0_161,X1_162)
| ~ qilt27(X0_161)
| ~ bcapacitysn(X0_161) ),
inference(cnfTransformation,[status(thm)],[f_178]) ).
tff(c_1445,plain,
! [X1_162] :
( conditionhyper('#skF_5'(n0))
| ~ bsecretioni('#skF_4'(n0))
| conditionnormo(X1_162)
| gt(n0,X1_162)
| ~ qilt27(n0)
| ~ bcapacitysn(n0) ),
inference(resolution,[status(thm)],[c_1439,c_112]) ).
tff(c_1465,plain,
! [X1_162] :
( conditionhyper('#skF_5'(n0))
| conditionnormo(X1_162)
| gt(n0,X1_162) ),
inference(demodulation,[status(thm),theory(equality)],[c_110,c_108,c_1272,c_1445]) ).
tff(c_1471,plain,
! [X1_163] :
( conditionnormo(X1_163)
| gt(n0,X1_163) ),
inference(negUnitSimplification,[status(thm)],[c_1299,c_1465]) ).
tff(c_1504,plain,
conditionnormo('#skF_15'),
inference(resolution,[status(thm)],[c_1471,c_106]) ).
tff(c_1521,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_104,c_1504]) ).
tff(c_1523,plain,
conditionhyper('#skF_5'(n0)),
inference(splitRight,[status(thm)],[c_1298]) ).
tff(c_40,plain,
! [X0_27,X1_31] :
( ~ bsecretioni('#skF_4'(X0_27))
| ~ conditionhyper('#skF_5'(X0_27))
| conditionnormo(X1_31)
| gt(X0_27,X1_31)
| ~ qilt27(X0_27)
| ~ bcapacitysn(X0_27) ),
inference(cnfTransformation,[status(thm)],[f_178]) ).
tff(c_1525,plain,
! [X1_31] :
( ~ bsecretioni('#skF_4'(n0))
| conditionnormo(X1_31)
| gt(n0,X1_31)
| ~ qilt27(n0)
| ~ bcapacitysn(n0) ),
inference(resolution,[status(thm)],[c_1523,c_40]) ).
tff(c_1529,plain,
! [X1_164] :
( conditionnormo(X1_164)
| gt(n0,X1_164) ),
inference(demodulation,[status(thm),theory(equality)],[c_110,c_108,c_1272,c_1525]) ).
tff(c_1562,plain,
conditionnormo('#skF_15'),
inference(resolution,[status(thm)],[c_1529,c_106]) ).
tff(c_1579,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_104,c_1562]) ).
tff(c_1587,plain,
! [X1_165] :
( bsecretioni(X1_165)
| gt(n0,X1_165) ),
inference(splitRight,[status(thm)],[c_262]) ).
tff(c_1622,plain,
! [X1_165] :
( conditionhyper(X1_165)
| bsecretioni(X1_165) ),
inference(resolution,[status(thm)],[c_1587,c_112]) ).
tff(c_1729,plain,
! [X0_178,X1_179] :
( ~ bsecretioni('#skF_4'(X0_178))
| ~ conditionhyper('#skF_5'(X0_178))
| conditionnormo(X1_179)
| gt(X0_178,X1_179)
| ~ qilt27(X0_178)
| ~ bcapacitysn(X0_178) ),
inference(cnfTransformation,[status(thm)],[f_178]) ).
tff(c_1811,plain,
! [X0_185,X1_186] :
( ~ bsecretioni('#skF_4'(X0_185))
| conditionnormo(X1_186)
| gt(X0_185,X1_186)
| ~ qilt27(X0_185)
| ~ bcapacitysn(X0_185)
| bsecretioni('#skF_5'(X0_185)) ),
inference(resolution,[status(thm)],[c_1622,c_1729]) ).
tff(c_1833,plain,
! [X1_186] :
( conditionhyper(X1_186)
| ~ bsecretioni('#skF_4'(n0))
| conditionnormo(X1_186)
| ~ qilt27(n0)
| ~ bcapacitysn(n0)
| bsecretioni('#skF_5'(n0)) ),
inference(resolution,[status(thm)],[c_1811,c_112]) ).
tff(c_1847,plain,
! [X1_186] :
( conditionhyper(X1_186)
| ~ bsecretioni('#skF_4'(n0))
| conditionnormo(X1_186)
| bsecretioni('#skF_5'(n0)) ),
inference(demodulation,[status(thm),theory(equality)],[c_110,c_108,c_1833]) ).
tff(c_1850,plain,
~ bsecretioni('#skF_4'(n0)),
inference(splitLeft,[status(thm)],[c_1847]) ).
tff(c_1580,plain,
! [X1_90] :
( bsecretioni(X1_90)
| gt(n0,X1_90) ),
inference(splitRight,[status(thm)],[c_262]) ).
tff(c_1888,plain,
! [X0_191,X1_192] :
( ~ gt(X0_191,'#skF_4'(X0_191))
| ~ conditionhyper('#skF_5'(X0_191))
| conditionnormo(X1_192)
| gt(X0_191,X1_192)
| ~ qilt27(X0_191)
| ~ bcapacitysn(X0_191) ),
inference(cnfTransformation,[status(thm)],[f_178]) ).
tff(c_1909,plain,
! [X1_192] :
( ~ conditionhyper('#skF_5'(n0))
| conditionnormo(X1_192)
| gt(n0,X1_192)
| ~ qilt27(n0)
| ~ bcapacitysn(n0)
| bsecretioni('#skF_4'(n0)) ),
inference(resolution,[status(thm)],[c_1580,c_1888]) ).
tff(c_1924,plain,
! [X1_192] :
( ~ conditionhyper('#skF_5'(n0))
| conditionnormo(X1_192)
| gt(n0,X1_192)
| bsecretioni('#skF_4'(n0)) ),
inference(demodulation,[status(thm),theory(equality)],[c_110,c_108,c_1909]) ).
tff(c_1925,plain,
! [X1_192] :
( ~ conditionhyper('#skF_5'(n0))
| conditionnormo(X1_192)
| gt(n0,X1_192) ),
inference(negUnitSimplification,[status(thm)],[c_1850,c_1924]) ).
tff(c_1930,plain,
~ conditionhyper('#skF_5'(n0)),
inference(splitLeft,[status(thm)],[c_1925]) ).
tff(c_3229,plain,
! [X0_265,X1_266] :
( ~ gt(X0_265,'#skF_4'(X0_265))
| gt(X0_265,'#skF_5'(X0_265))
| conditionnormo(X1_266)
| gt(X0_265,X1_266)
| ~ qilt27(X0_265)
| ~ bcapacitysn(X0_265) ),
inference(cnfTransformation,[status(thm)],[f_178]) ).
tff(c_3245,plain,
! [X1_266] :
( conditionhyper('#skF_5'(n0))
| ~ gt(n0,'#skF_4'(n0))
| conditionnormo(X1_266)
| gt(n0,X1_266)
| ~ qilt27(n0)
| ~ bcapacitysn(n0) ),
inference(resolution,[status(thm)],[c_3229,c_112]) ).
tff(c_3286,plain,
! [X1_266] :
( conditionhyper('#skF_5'(n0))
| ~ gt(n0,'#skF_4'(n0))
| conditionnormo(X1_266)
| gt(n0,X1_266) ),
inference(demodulation,[status(thm),theory(equality)],[c_110,c_108,c_3245]) ).
tff(c_3287,plain,
! [X1_266] :
( ~ gt(n0,'#skF_4'(n0))
| conditionnormo(X1_266)
| gt(n0,X1_266) ),
inference(negUnitSimplification,[status(thm)],[c_1930,c_3286]) ).
tff(c_3298,plain,
~ gt(n0,'#skF_4'(n0)),
inference(splitLeft,[status(thm)],[c_3287]) ).
tff(c_3344,plain,
bsecretioni('#skF_4'(n0)),
inference(resolution,[status(thm)],[c_1580,c_3298]) ).
tff(c_3387,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1850,c_3344]) ).
tff(c_3417,plain,
! [X1_267] :
( conditionnormo(X1_267)
| gt(n0,X1_267) ),
inference(splitRight,[status(thm)],[c_3287]) ).
tff(c_3472,plain,
conditionnormo('#skF_15'),
inference(resolution,[status(thm)],[c_3417,c_106]) ).
tff(c_3500,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_104,c_3472]) ).
tff(c_3508,plain,
! [X1_268] :
( conditionnormo(X1_268)
| gt(n0,X1_268) ),
inference(splitRight,[status(thm)],[c_1925]) ).
tff(c_3543,plain,
conditionnormo('#skF_15'),
inference(resolution,[status(thm)],[c_3508,c_106]) ).
tff(c_3561,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_104,c_3543]) ).
tff(c_3563,plain,
bsecretioni('#skF_4'(n0)),
inference(splitRight,[status(thm)],[c_1847]) ).
tff(c_3679,plain,
! [X0_279,X1_280] :
( ~ bsecretioni('#skF_4'(X0_279))
| gt(X0_279,'#skF_5'(X0_279))
| conditionnormo(X1_280)
| gt(X0_279,X1_280)
| ~ qilt27(X0_279)
| ~ bcapacitysn(X0_279) ),
inference(cnfTransformation,[status(thm)],[f_178]) ).
tff(c_3687,plain,
! [X1_280] :
( conditionhyper('#skF_5'(n0))
| ~ bsecretioni('#skF_4'(n0))
| conditionnormo(X1_280)
| gt(n0,X1_280)
| ~ qilt27(n0)
| ~ bcapacitysn(n0) ),
inference(resolution,[status(thm)],[c_3679,c_112]) ).
tff(c_3709,plain,
! [X1_280] :
( conditionhyper('#skF_5'(n0))
| conditionnormo(X1_280)
| gt(n0,X1_280) ),
inference(demodulation,[status(thm),theory(equality)],[c_110,c_108,c_3563,c_3687]) ).
tff(c_3761,plain,
conditionhyper('#skF_5'(n0)),
inference(splitLeft,[status(thm)],[c_3709]) ).
tff(c_3763,plain,
! [X1_31] :
( ~ bsecretioni('#skF_4'(n0))
| conditionnormo(X1_31)
| gt(n0,X1_31)
| ~ qilt27(n0)
| ~ bcapacitysn(n0) ),
inference(resolution,[status(thm)],[c_3761,c_40]) ).
tff(c_3767,plain,
! [X1_283] :
( conditionnormo(X1_283)
| gt(n0,X1_283) ),
inference(demodulation,[status(thm),theory(equality)],[c_110,c_108,c_3563,c_3763]) ).
tff(c_3802,plain,
conditionnormo('#skF_15'),
inference(resolution,[status(thm)],[c_3767,c_106]) ).
tff(c_3820,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_104,c_3802]) ).
tff(c_3978,plain,
! [X1_288] :
( conditionnormo(X1_288)
| gt(n0,X1_288) ),
inference(splitRight,[status(thm)],[c_3709]) ).
tff(c_4016,plain,
conditionnormo('#skF_15'),
inference(resolution,[status(thm)],[c_3978,c_106]) ).
tff(c_4035,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_104,c_4016]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : MED001+1 : TPTP v9.0.0. Released v3.2.0.
% 0.07/0.13 % 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.13/0.34 % Computer : n003.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Apr 8 07:47:03 EDT 2025
% 0.13/0.34 % CPUTime :
% 7.49/2.79 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.49/2.80
% 7.49/2.80 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------