%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MED010+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/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 : 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:07 PM UTC 2025
% Result : Theorem 21.00s 6.96s
% Output : CNFRefutation 21.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 12
% Syntax : Number of formulae : 280 ( 138 unt; 0 typ; 0 def)
% Number of atoms : 627 ( 0 equ)
% Maximal formula atoms : 30 ( 2 avg)
% Number of connectives : 485 ( 138 ~; 298 |; 21 &)
% ( 0 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 21 ( 20 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 1 con; 0-1 aty)
% Number of variables : 195 ( 193 !; 2 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ gt > uptakepg > uptakelg > s3 > s2 > s1 > s0 > releaselg > qilt27 > qillt27 > drugsu > drugi > drugbg > conditionnormo > conditionhypo > conditionhyper > bsecretioni > bcapacitysn > bcapacityne > bcapacityex > #nlpp > n0 > #skF_9 > #skF_7 > #skF_5 > #skF_21 > #skF_16 > #skF_2 > #skF_4 > #skF_18 > #skF_19 > #skF_1 > #skF_22 > #skF_8 > #skF_15 > #skF_10 > #skF_23 > #skF_13 > #skF_17 > #skF_3 > #skF_11 > #skF_14 > #skF_12 > #skF_6 > #skF_20
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(bsecretioni,type,
bsecretioni: $i > $o ).
tff(qillt27,type,
qillt27: $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(s1,type,
s1: $i > $o ).
tff(conditionhypo,type,
conditionhypo: $i > $o ).
tff('#skF_21',type,
'#skF_21': $i > $i ).
tff('#skF_16',type,
'#skF_16': $i > $i ).
tff('#skF_2',type,
'#skF_2': $i > $i ).
tff('#skF_4',type,
'#skF_4': $i > $i ).
tff('#skF_18',type,
'#skF_18': $i > $i ).
tff(s0,type,
s0: $i > $o ).
tff('#skF_19',type,
'#skF_19': $i > $i ).
tff('#skF_1',type,
'#skF_1': $i > $i ).
tff(drugi,type,
drugi: $i > $o ).
tff(releaselg,type,
releaselg: $i > $o ).
tff('#skF_22',type,
'#skF_22': $i > $i ).
tff(drugbg,type,
drugbg: $i > $o ).
tff(s3,type,
s3: $i > $o ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff('#skF_15',type,
'#skF_15': $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('#skF_23',type,
'#skF_23': $i > $i ).
tff(bcapacitysn,type,
bcapacitysn: $i > $o ).
tff('#skF_13',type,
'#skF_13': $i > $i ).
tff(s2,type,
s2: $i > $o ).
tff(uptakelg,type,
uptakelg: $i > $o ).
tff('#skF_17',type,
'#skF_17': $i > $i ).
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('#skF_20',type,
'#skF_20': $i > $i ).
tff(f_610,negated_conjecture,
~ ( ( s2(n0)
& ! [X0] :
( gt(n0,X0)
=> conditionhyper(X0) )
& bcapacityex(n0) )
=> ? [X0] :
( ~ gt(n0,X0)
& s3(X0)
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) )
& bcapacityex(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unsuccesfuls2) ).
tff(f_466,axiom,
! [X0] :
( drugi(X0)
=> s3(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MED001+1.ax',insulincomp) ).
tff(f_329,axiom,
! [X0] :
( ~ s2(X0)
| ~ s3(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MED001+1.ax',xorstep7) ).
tff(f_492,axiom,
! [X0,X1] :
( ~ gt(X0,X1)
=> ( ~ releaselg(X1)
=> uptakelg(X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/MED001+1.ax',uptake_completion) ).
tff(f_53,axiom,
! [X] : ~ gt(X,X),
file('/export/starexec/sandbox/benchmark/Axioms/MED001+0.ax',irreflexivity_gt) ).
tff(f_484,axiom,
! [X0] :
( ( ! [X1] :
( ~ gt(X0,X1)
=> uptakelg(X1) )
| ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) ) )
=> ! [X1] :
( ~ gt(X0,X1)
=> drugi(X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/MED001+1.ax',insulin_completion) ).
tff(f_586,axiom,
! [X0] :
( ( s2(X0)
& ~ ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) ) )
=> ? [X1] :
( ~ gt(X0,X1)
& s3(X1)
& ! [X2] :
( gt(X1,X2)
=> conditionhyper(X2) )
& bcapacityex(X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/MED001+1.ax',trans_ax3) ).
tff(f_101,axiom,
! [X0] :
( ~ conditionhyper(X0)
| ~ conditionnormo(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MED001+0.ax',xorcondition3) ).
tff(f_412,axiom,
! [X0] :
( ! [X1] :
( ~ gt(X0,X1)
=> conditionnormo(X1) )
=> ( ( ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) )
& bcapacitysn(X0)
& qilt27(X0)
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) ) )
| ( ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) )
& bcapacitysn(X0)
& ~ qilt27(X0)
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) ) )
| ( ( ! [X1] :
( ~ gt(X0,X1)
=> ~ releaselg(X1) )
| ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) ) )
& bcapacityne(X0)
& ! [X1] :
( ~ gt(X0,X1)
=> bsecretioni(X1) )
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) ) )
| ( ! [X1] :
( ~ gt(X0,X1)
=> uptakelg(X1) )
& ! [X1] :
( ~ gt(X0,X1)
=> uptakepg(X1) )
& bcapacityex(X0)
& ! [X1] :
( gt(X0,X1)
=> conditionhyper(X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/MED001+1.ax',normo) ).
tff(f_71,axiom,
! [X0] :
( ~ bcapacityne(X0)
| ~ bcapacityex(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MED001+0.ax',xorcapacity2) ).
tff(f_83,axiom,
! [X0] :
( ~ bcapacityex(X0)
| ~ bcapacitysn(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/MED001+0.ax',xorcapacity4) ).
tff(f_129,axiom,
! [X0,X1] :
( ~ gt(X0,X1)
=> ( uptakelg(X1)
=> ~ releaselg(X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/MED001+0.ax',liver_glucose) ).
tff(c_1212,plain,
s2(n0),
inference(cnfTransformation,[status(thm)],[f_610]) ).
tff(c_1225,plain,
! [X0_134] :
( s3(X0_134)
| ~ drugi(X0_134) ),
inference(cnfTransformation,[status(thm)],[f_466]) ).
tff(c_116,plain,
! [X0_56] :
( ~ s3(X0_56)
| ~ s2(X0_56) ),
inference(cnfTransformation,[status(thm)],[f_329]) ).
tff(c_1269,plain,
! [X0_150] :
( ~ s2(X0_150)
| ~ drugi(X0_150) ),
inference(resolution,[status(thm)],[c_1225,c_116]) ).
tff(c_1273,plain,
~ drugi(n0),
inference(resolution,[status(thm)],[c_1212,c_1269]) ).
tff(c_1311,plain,
! [X1_159,X0_160] :
( uptakelg(X1_159)
| releaselg(X1_159)
| gt(X0_160,X1_159) ),
inference(cnfTransformation,[status(thm)],[f_492]) ).
tff(c_2,plain,
! [X_1] : ~ gt(X_1,X_1),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_1325,plain,
! [X1_159] :
( uptakelg(X1_159)
| releaselg(X1_159) ),
inference(resolution,[status(thm)],[c_1311,c_2]) ).
tff(c_1397,plain,
! [X0_172,X1_173] :
( ~ uptakelg('#skF_16'(X0_172))
| drugi(X1_173)
| gt(X0_172,X1_173) ),
inference(cnfTransformation,[status(thm)],[f_484]) ).
tff(c_1956,plain,
! [X1_227,X0_228] :
( drugi(X1_227)
| gt(X0_228,X1_227)
| releaselg('#skF_16'(X0_228)) ),
inference(resolution,[status(thm)],[c_1325,c_1397]) ).
tff(c_2003,plain,
! [X1_227] :
( drugi(X1_227)
| releaselg('#skF_16'(X1_227)) ),
inference(resolution,[status(thm)],[c_1956,c_2]) ).
tff(c_1200,plain,
! [X0_119,X1_124] :
( bcapacityex('#skF_22'(X0_119))
| conditionnormo(X1_124)
| gt(X0_119,X1_124)
| ~ s2(X0_119) ),
inference(cnfTransformation,[status(thm)],[f_586]) ).
tff(c_1204,plain,
! [X0_119,X1_124] :
( s3('#skF_22'(X0_119))
| conditionnormo(X1_124)
| gt(X0_119,X1_124)
| ~ s2(X0_119) ),
inference(cnfTransformation,[status(thm)],[f_586]) ).
tff(c_2159,plain,
! [X0_247,X1_248] :
( s3('#skF_22'(X0_247))
| conditionnormo(X1_248)
| gt(X0_247,X1_248)
| ~ s2(X0_247) ),
inference(cnfTransformation,[status(thm)],[f_586]) ).
tff(c_1210,plain,
! [X0_127] :
( conditionhyper(X0_127)
| ~ gt(n0,X0_127) ),
inference(cnfTransformation,[status(thm)],[f_610]) ).
tff(c_2212,plain,
! [X1_248] :
( conditionhyper(X1_248)
| s3('#skF_22'(n0))
| conditionnormo(X1_248)
| ~ s2(n0) ),
inference(resolution,[status(thm)],[c_2159,c_1210]) ).
tff(c_2235,plain,
! [X1_248] :
( conditionhyper(X1_248)
| s3('#skF_22'(n0))
| conditionnormo(X1_248) ),
inference(demodulation,[status(thm),theory(equality)],[c_1212,c_2212]) ).
tff(c_2237,plain,
s3('#skF_22'(n0)),
inference(splitLeft,[status(thm)],[c_2235]) ).
tff(c_2073,plain,
! [X0_240,X1_241] :
( bcapacityex('#skF_22'(X0_240))
| conditionnormo(X1_241)
| gt(X0_240,X1_241)
| ~ s2(X0_240) ),
inference(cnfTransformation,[status(thm)],[f_586]) ).
tff(c_2110,plain,
! [X1_241] :
( conditionhyper(X1_241)
| bcapacityex('#skF_22'(n0))
| conditionnormo(X1_241)
| ~ s2(n0) ),
inference(resolution,[status(thm)],[c_2073,c_1210]) ).
tff(c_2128,plain,
! [X1_241] :
( conditionhyper(X1_241)
| bcapacityex('#skF_22'(n0))
| conditionnormo(X1_241) ),
inference(demodulation,[status(thm),theory(equality)],[c_1212,c_2110]) ).
tff(c_2130,plain,
bcapacityex('#skF_22'(n0)),
inference(splitLeft,[status(thm)],[c_2128]) ).
tff(c_1216,plain,
! [X0_128] :
( gt(X0_128,'#skF_23'(X0_128))
| ~ bcapacityex(X0_128)
| ~ s3(X0_128)
| gt(n0,X0_128) ),
inference(cnfTransformation,[status(thm)],[f_610]) ).
tff(c_5850,plain,
! [X2_419,X0_420,X1_421] :
( conditionhyper(X2_419)
| ~ gt('#skF_22'(X0_420),X2_419)
| conditionnormo(X1_421)
| gt(X0_420,X1_421)
| ~ s2(X0_420) ),
inference(cnfTransformation,[status(thm)],[f_586]) ).
tff(c_7790,plain,
! [X0_478,X1_479] :
( conditionhyper('#skF_23'('#skF_22'(X0_478)))
| conditionnormo(X1_479)
| gt(X0_478,X1_479)
| ~ s2(X0_478)
| ~ bcapacityex('#skF_22'(X0_478))
| ~ s3('#skF_22'(X0_478))
| gt(n0,'#skF_22'(X0_478)) ),
inference(resolution,[status(thm)],[c_1216,c_5850]) ).
tff(c_7885,plain,
! [X1_479] :
( conditionhyper(X1_479)
| conditionhyper('#skF_23'('#skF_22'(n0)))
| conditionnormo(X1_479)
| ~ s2(n0)
| ~ bcapacityex('#skF_22'(n0))
| ~ s3('#skF_22'(n0))
| gt(n0,'#skF_22'(n0)) ),
inference(resolution,[status(thm)],[c_7790,c_1210]) ).
tff(c_7923,plain,
! [X1_479] :
( conditionhyper(X1_479)
| conditionhyper('#skF_23'('#skF_22'(n0)))
| conditionnormo(X1_479)
| gt(n0,'#skF_22'(n0)) ),
inference(demodulation,[status(thm),theory(equality)],[c_2237,c_2130,c_1212,c_7885]) ).
tff(c_7960,plain,
gt(n0,'#skF_22'(n0)),
inference(splitLeft,[status(thm)],[c_7923]) ).
tff(c_1206,plain,
! [X0_119,X1_124] :
( ~ gt(X0_119,'#skF_22'(X0_119))
| conditionnormo(X1_124)
| gt(X0_119,X1_124)
| ~ s2(X0_119) ),
inference(cnfTransformation,[status(thm)],[f_586]) ).
tff(c_7970,plain,
! [X1_124] :
( conditionnormo(X1_124)
| gt(n0,X1_124)
| ~ s2(n0) ),
inference(resolution,[status(thm)],[c_7960,c_1206]) ).
tff(c_8121,plain,
! [X1_485] :
( conditionnormo(X1_485)
| gt(n0,X1_485) ),
inference(demodulation,[status(thm),theory(equality)],[c_1212,c_7970]) ).
tff(c_1170,plain,
! [X0_88,X1_92] :
( ~ gt(X0_88,'#skF_16'(X0_88))
| drugi(X1_92)
| gt(X0_88,X1_92) ),
inference(cnfTransformation,[status(thm)],[f_484]) ).
tff(c_8222,plain,
! [X1_92] :
( drugi(X1_92)
| gt(n0,X1_92)
| conditionnormo('#skF_16'(n0)) ),
inference(resolution,[status(thm)],[c_8121,c_1170]) ).
tff(c_8773,plain,
conditionnormo('#skF_16'(n0)),
inference(splitLeft,[status(thm)],[c_8222]) ).
tff(c_18,plain,
! [X0_11] :
( ~ conditionnormo(X0_11)
| ~ conditionhyper(X0_11) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_8781,plain,
~ conditionhyper('#skF_16'(n0)),
inference(resolution,[status(thm)],[c_8773,c_18]) ).
tff(c_2002,plain,
! [X1_227] :
( conditionhyper(X1_227)
| drugi(X1_227)
| releaselg('#skF_16'(n0)) ),
inference(resolution,[status(thm)],[c_1956,c_1210]) ).
tff(c_2005,plain,
releaselg('#skF_16'(n0)),
inference(splitLeft,[status(thm)],[c_2002]) ).
tff(c_1208,plain,
bcapacityex(n0),
inference(cnfTransformation,[status(thm)],[f_610]) ).
tff(c_8229,plain,
conditionnormo(n0),
inference(resolution,[status(thm)],[c_8121,c_2]) ).
tff(c_8237,plain,
~ conditionhyper(n0),
inference(resolution,[status(thm)],[c_8229,c_18]) ).
tff(c_1166,plain,
! [X0_88,X1_92] :
( ~ gt(X0_88,'#skF_17'(X0_88))
| drugi(X1_92)
| gt(X0_88,X1_92) ),
inference(cnfTransformation,[status(thm)],[f_484]) ).
tff(c_8224,plain,
! [X1_92] :
( drugi(X1_92)
| gt(n0,X1_92)
| conditionnormo('#skF_17'(n0)) ),
inference(resolution,[status(thm)],[c_8121,c_1166]) ).
tff(c_9134,plain,
conditionnormo('#skF_17'(n0)),
inference(splitLeft,[status(thm)],[c_8224]) ).
tff(c_9142,plain,
~ conditionhyper('#skF_17'(n0)),
inference(resolution,[status(thm)],[c_9134,c_18]) ).
tff(c_1056,plain,
! [X0_57,X1_78] :
( ~ gt(X0_57,'#skF_15'(X0_57))
| bcapacitysn(X0_57)
| bcapacityne(X0_57)
| uptakelg(X1_78)
| gt(X0_57,X1_78) ),
inference(cnfTransformation,[status(thm)],[f_412]) ).
tff(c_8202,plain,
! [X1_78] :
( bcapacitysn(n0)
| bcapacityne(n0)
| uptakelg(X1_78)
| gt(n0,X1_78)
| conditionnormo('#skF_15'(n0)) ),
inference(resolution,[status(thm)],[c_8121,c_1056]) ).
tff(c_9521,plain,
conditionnormo('#skF_15'(n0)),
inference(splitLeft,[status(thm)],[c_8202]) ).
tff(c_798,plain,
! [X0_57,X1_79] :
( ~ conditionnormo('#skF_15'(X0_57))
| bcapacitysn(X0_57)
| bcapacityne(X0_57)
| uptakepg(X1_79)
| gt(X0_57,X1_79) ),
inference(cnfTransformation,[status(thm)],[f_412]) ).
tff(c_9566,plain,
! [X1_79] :
( bcapacitysn(n0)
| bcapacityne(n0)
| uptakepg(X1_79)
| gt(n0,X1_79) ),
inference(resolution,[status(thm)],[c_9521,c_798]) ).
tff(c_9577,plain,
bcapacityne(n0),
inference(splitLeft,[status(thm)],[c_9566]) ).
tff(c_8,plain,
! [X0_6] :
( ~ bcapacityex(X0_6)
| ~ bcapacityne(X0_6) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_9580,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_9577,c_8]) ).
tff(c_9584,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_9580]) ).
tff(c_9585,plain,
! [X1_79] :
( bcapacitysn(n0)
| uptakepg(X1_79)
| gt(n0,X1_79) ),
inference(splitRight,[status(thm)],[c_9566]) ).
tff(c_9612,plain,
bcapacitysn(n0),
inference(splitLeft,[status(thm)],[c_9585]) ).
tff(c_12,plain,
! [X0_8] :
( ~ bcapacitysn(X0_8)
| ~ bcapacityex(X0_8) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_9615,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_9612,c_12]) ).
tff(c_9622,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_9615]) ).
tff(c_9631,plain,
! [X1_521] :
( uptakepg(X1_521)
| gt(n0,X1_521) ),
inference(splitRight,[status(thm)],[c_9585]) ).
tff(c_9776,plain,
! [X1_525] :
( conditionhyper(X1_525)
| uptakepg(X1_525) ),
inference(resolution,[status(thm)],[c_9631,c_1210]) ).
tff(c_1164,plain,
! [X0_88,X1_92] :
( ~ uptakepg('#skF_17'(X0_88))
| drugi(X1_92)
| gt(X0_88,X1_92) ),
inference(cnfTransformation,[status(thm)],[f_484]) ).
tff(c_9781,plain,
! [X1_526,X0_527] :
( drugi(X1_526)
| gt(X0_527,X1_526)
| conditionhyper('#skF_17'(X0_527)) ),
inference(resolution,[status(thm)],[c_9776,c_1164]) ).
tff(c_9887,plain,
! [X1_526] :
( conditionhyper(X1_526)
| drugi(X1_526)
| conditionhyper('#skF_17'(n0)) ),
inference(resolution,[status(thm)],[c_9781,c_1210]) ).
tff(c_9934,plain,
! [X1_528] :
( conditionhyper(X1_528)
| drugi(X1_528) ),
inference(negUnitSimplification,[status(thm)],[c_9142,c_9887]) ).
tff(c_9970,plain,
conditionhyper(n0),
inference(resolution,[status(thm)],[c_9934,c_1273]) ).
tff(c_9985,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8237,c_9970]) ).
tff(c_9986,plain,
! [X1_78] :
( bcapacityne(n0)
| bcapacitysn(n0)
| uptakelg(X1_78)
| gt(n0,X1_78) ),
inference(splitRight,[status(thm)],[c_8202]) ).
tff(c_9992,plain,
bcapacitysn(n0),
inference(splitLeft,[status(thm)],[c_9986]) ).
tff(c_9995,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_9992,c_12]) ).
tff(c_10002,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_9995]) ).
tff(c_10003,plain,
! [X1_78] :
( bcapacityne(n0)
| uptakelg(X1_78)
| gt(n0,X1_78) ),
inference(splitRight,[status(thm)],[c_9986]) ).
tff(c_10015,plain,
bcapacityne(n0),
inference(splitLeft,[status(thm)],[c_10003]) ).
tff(c_10018,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_10015,c_8]) ).
tff(c_10022,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_10018]) ).
tff(c_10050,plain,
! [X1_534] :
( uptakelg(X1_534)
| gt(n0,X1_534) ),
inference(splitRight,[status(thm)],[c_10003]) ).
tff(c_10199,plain,
! [X1_538] :
( conditionhyper(X1_538)
| uptakelg(X1_538) ),
inference(resolution,[status(thm)],[c_10050,c_1210]) ).
tff(c_1328,plain,
! [X1_163,X0_164] :
( ~ releaselg(X1_163)
| ~ uptakelg(X1_163)
| gt(X0_164,X1_163) ),
inference(cnfTransformation,[status(thm)],[f_129]) ).
tff(c_1342,plain,
! [X1_163] :
( ~ releaselg(X1_163)
| ~ uptakelg(X1_163) ),
inference(resolution,[status(thm)],[c_1328,c_2]) ).
tff(c_10208,plain,
! [X1_539] :
( ~ releaselg(X1_539)
| conditionhyper(X1_539) ),
inference(resolution,[status(thm)],[c_10199,c_1342]) ).
tff(c_10322,plain,
conditionhyper('#skF_16'(n0)),
inference(resolution,[status(thm)],[c_2005,c_10208]) ).
tff(c_10381,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8781,c_10322]) ).
tff(c_10571,plain,
! [X1_542] :
( drugi(X1_542)
| gt(n0,X1_542) ),
inference(splitRight,[status(thm)],[c_8224]) ).
tff(c_10654,plain,
drugi(n0),
inference(resolution,[status(thm)],[c_10571,c_2]) ).
tff(c_10697,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1273,c_10654]) ).
tff(c_10709,plain,
! [X1_546] :
( drugi(X1_546)
| gt(n0,X1_546) ),
inference(splitRight,[status(thm)],[c_8222]) ).
tff(c_10789,plain,
drugi(n0),
inference(resolution,[status(thm)],[c_10709,c_2]) ).
tff(c_10830,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1273,c_10789]) ).
tff(c_10832,plain,
~ gt(n0,'#skF_22'(n0)),
inference(splitRight,[status(thm)],[c_7923]) ).
tff(c_5982,plain,
! [X0_420,X1_421] :
( conditionhyper('#skF_23'('#skF_22'(X0_420)))
| conditionnormo(X1_421)
| gt(X0_420,X1_421)
| ~ s2(X0_420)
| ~ bcapacityex('#skF_22'(X0_420))
| ~ s3('#skF_22'(X0_420))
| gt(n0,'#skF_22'(X0_420)) ),
inference(resolution,[status(thm)],[c_1216,c_5850]) ).
tff(c_10831,plain,
! [X1_479] :
( conditionhyper('#skF_23'('#skF_22'(n0)))
| conditionhyper(X1_479)
| conditionnormo(X1_479) ),
inference(splitRight,[status(thm)],[c_7923]) ).
tff(c_10977,plain,
conditionhyper('#skF_23'('#skF_22'(n0))),
inference(splitLeft,[status(thm)],[c_10831]) ).
tff(c_1214,plain,
! [X0_128] :
( ~ conditionhyper('#skF_23'(X0_128))
| ~ bcapacityex(X0_128)
| ~ s3(X0_128)
| gt(n0,X0_128) ),
inference(cnfTransformation,[status(thm)],[f_610]) ).
tff(c_11176,plain,
( ~ bcapacityex('#skF_22'(n0))
| ~ s3('#skF_22'(n0))
| gt(n0,'#skF_22'(n0)) ),
inference(resolution,[status(thm)],[c_10977,c_1214]) ).
tff(c_11179,plain,
gt(n0,'#skF_22'(n0)),
inference(demodulation,[status(thm),theory(equality)],[c_2237,c_2130,c_11176]) ).
tff(c_11181,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10832,c_11179]) ).
tff(c_11183,plain,
~ conditionhyper('#skF_23'('#skF_22'(n0))),
inference(splitRight,[status(thm)],[c_10831]) ).
tff(c_11364,plain,
! [X1_421] :
( conditionnormo(X1_421)
| gt(n0,X1_421)
| ~ s2(n0)
| ~ bcapacityex('#skF_22'(n0))
| ~ s3('#skF_22'(n0))
| gt(n0,'#skF_22'(n0)) ),
inference(resolution,[status(thm)],[c_5982,c_11183]) ).
tff(c_11367,plain,
! [X1_421] :
( conditionnormo(X1_421)
| gt(n0,X1_421)
| gt(n0,'#skF_22'(n0)) ),
inference(demodulation,[status(thm),theory(equality)],[c_2237,c_2130,c_1212,c_11364]) ).
tff(c_11570,plain,
! [X1_555] :
( conditionnormo(X1_555)
| gt(n0,X1_555) ),
inference(negUnitSimplification,[status(thm)],[c_10832,c_11367]) ).
tff(c_11676,plain,
! [X1_92] :
( drugi(X1_92)
| gt(n0,X1_92)
| conditionnormo('#skF_16'(n0)) ),
inference(resolution,[status(thm)],[c_11570,c_1170]) ).
tff(c_12398,plain,
conditionnormo('#skF_16'(n0)),
inference(splitLeft,[status(thm)],[c_11676]) ).
tff(c_12406,plain,
~ conditionhyper('#skF_16'(n0)),
inference(resolution,[status(thm)],[c_12398,c_18]) ).
tff(c_11683,plain,
conditionnormo(n0),
inference(resolution,[status(thm)],[c_11570,c_2]) ).
tff(c_11692,plain,
~ conditionhyper(n0),
inference(resolution,[status(thm)],[c_11683,c_18]) ).
tff(c_11678,plain,
! [X1_92] :
( drugi(X1_92)
| gt(n0,X1_92)
| conditionnormo('#skF_17'(n0)) ),
inference(resolution,[status(thm)],[c_11570,c_1166]) ).
tff(c_11750,plain,
conditionnormo('#skF_17'(n0)),
inference(splitLeft,[status(thm)],[c_11678]) ).
tff(c_11896,plain,
~ conditionhyper('#skF_17'(n0)),
inference(resolution,[status(thm)],[c_11750,c_18]) ).
tff(c_11317,plain,
! [X1_551] :
( conditionhyper(X1_551)
| conditionnormo(X1_551) ),
inference(splitRight,[status(thm)],[c_10831]) ).
tff(c_1054,plain,
! [X0_57,X1_78] :
( ~ conditionnormo('#skF_15'(X0_57))
| bcapacitysn(X0_57)
| bcapacityne(X0_57)
| uptakelg(X1_78)
| gt(X0_57,X1_78) ),
inference(cnfTransformation,[status(thm)],[f_412]) ).
tff(c_12509,plain,
! [X0_581,X1_582] :
( bcapacitysn(X0_581)
| bcapacityne(X0_581)
| uptakelg(X1_582)
| gt(X0_581,X1_582)
| conditionhyper('#skF_15'(X0_581)) ),
inference(resolution,[status(thm)],[c_11317,c_1054]) ).
tff(c_12622,plain,
( bcapacitysn(n0)
| bcapacityne(n0)
| uptakelg('#skF_22'(n0))
| conditionhyper('#skF_15'(n0)) ),
inference(resolution,[status(thm)],[c_12509,c_10832]) ).
tff(c_12656,plain,
conditionhyper('#skF_15'(n0)),
inference(splitLeft,[status(thm)],[c_12622]) ).
tff(c_800,plain,
! [X0_57,X1_79] :
( ~ gt(X0_57,'#skF_15'(X0_57))
| bcapacitysn(X0_57)
| bcapacityne(X0_57)
| uptakepg(X1_79)
| gt(X0_57,X1_79) ),
inference(cnfTransformation,[status(thm)],[f_412]) ).
tff(c_11659,plain,
! [X1_79] :
( bcapacitysn(n0)
| bcapacityne(n0)
| uptakepg(X1_79)
| gt(n0,X1_79)
| conditionnormo('#skF_15'(n0)) ),
inference(resolution,[status(thm)],[c_11570,c_800]) ).
tff(c_13128,plain,
conditionnormo('#skF_15'(n0)),
inference(splitLeft,[status(thm)],[c_11659]) ).
tff(c_13160,plain,
~ conditionhyper('#skF_15'(n0)),
inference(resolution,[status(thm)],[c_13128,c_18]) ).
tff(c_13184,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_12656,c_13160]) ).
tff(c_13185,plain,
! [X1_79] :
( bcapacityne(n0)
| bcapacitysn(n0)
| uptakepg(X1_79)
| gt(n0,X1_79) ),
inference(splitRight,[status(thm)],[c_11659]) ).
tff(c_13192,plain,
bcapacitysn(n0),
inference(splitLeft,[status(thm)],[c_13185]) ).
tff(c_13195,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_13192,c_12]) ).
tff(c_13202,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_13195]) ).
tff(c_13203,plain,
! [X1_79] :
( bcapacityne(n0)
| uptakepg(X1_79)
| gt(n0,X1_79) ),
inference(splitRight,[status(thm)],[c_13185]) ).
tff(c_13215,plain,
bcapacityne(n0),
inference(splitLeft,[status(thm)],[c_13203]) ).
tff(c_13218,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_13215,c_8]) ).
tff(c_13222,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_13218]) ).
tff(c_13225,plain,
! [X1_603] :
( uptakepg(X1_603)
| gt(n0,X1_603) ),
inference(splitRight,[status(thm)],[c_13203]) ).
tff(c_13361,plain,
! [X1_604] :
( conditionhyper(X1_604)
| uptakepg(X1_604) ),
inference(resolution,[status(thm)],[c_13225,c_1210]) ).
tff(c_13517,plain,
! [X1_607,X0_608] :
( drugi(X1_607)
| gt(X0_608,X1_607)
| conditionhyper('#skF_17'(X0_608)) ),
inference(resolution,[status(thm)],[c_13361,c_1164]) ).
tff(c_13625,plain,
! [X1_607] :
( conditionhyper(X1_607)
| drugi(X1_607)
| conditionhyper('#skF_17'(n0)) ),
inference(resolution,[status(thm)],[c_13517,c_1210]) ).
tff(c_13675,plain,
! [X1_609] :
( conditionhyper(X1_609)
| drugi(X1_609) ),
inference(negUnitSimplification,[status(thm)],[c_11896,c_13625]) ).
tff(c_13711,plain,
conditionhyper(n0),
inference(resolution,[status(thm)],[c_13675,c_1273]) ).
tff(c_13726,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11692,c_13711]) ).
tff(c_13727,plain,
( uptakelg('#skF_22'(n0))
| bcapacityne(n0)
| bcapacitysn(n0) ),
inference(splitRight,[status(thm)],[c_12622]) ).
tff(c_13747,plain,
bcapacitysn(n0),
inference(splitLeft,[status(thm)],[c_13727]) ).
tff(c_13750,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_13747,c_12]) ).
tff(c_13757,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_13750]) ).
tff(c_13759,plain,
~ bcapacitysn(n0),
inference(splitRight,[status(thm)],[c_13727]) ).
tff(c_13728,plain,
~ conditionhyper('#skF_15'(n0)),
inference(splitRight,[status(thm)],[c_12622]) ).
tff(c_12653,plain,
! [X1_582] :
( conditionhyper(X1_582)
| bcapacitysn(n0)
| bcapacityne(n0)
| uptakelg(X1_582)
| conditionhyper('#skF_15'(n0)) ),
inference(resolution,[status(thm)],[c_12509,c_1210]) ).
tff(c_13760,plain,
! [X1_582] :
( conditionhyper(X1_582)
| bcapacitysn(n0)
| bcapacityne(n0)
| uptakelg(X1_582) ),
inference(negUnitSimplification,[status(thm)],[c_13728,c_12653]) ).
tff(c_13761,plain,
bcapacityne(n0),
inference(splitLeft,[status(thm)],[c_13760]) ).
tff(c_13769,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_13761,c_8]) ).
tff(c_13773,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_13769]) ).
tff(c_13774,plain,
! [X1_582] :
( bcapacitysn(n0)
| conditionhyper(X1_582)
| uptakelg(X1_582) ),
inference(splitRight,[status(thm)],[c_13760]) ).
tff(c_13792,plain,
! [X1_616] :
( conditionhyper(X1_616)
| uptakelg(X1_616) ),
inference(negUnitSimplification,[status(thm)],[c_13759,c_13774]) ).
tff(c_13801,plain,
! [X1_617] :
( ~ releaselg(X1_617)
| conditionhyper(X1_617) ),
inference(resolution,[status(thm)],[c_13792,c_1342]) ).
tff(c_13909,plain,
conditionhyper('#skF_16'(n0)),
inference(resolution,[status(thm)],[c_2005,c_13801]) ).
tff(c_13966,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_12406,c_13909]) ).
tff(c_13998,plain,
! [X1_620] :
( drugi(X1_620)
| gt(n0,X1_620) ),
inference(splitRight,[status(thm)],[c_11676]) ).
tff(c_14081,plain,
drugi(n0),
inference(resolution,[status(thm)],[c_13998,c_2]) ).
tff(c_14124,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1273,c_14081]) ).
tff(c_14269,plain,
! [X1_623] :
( drugi(X1_623)
| gt(n0,X1_623) ),
inference(splitRight,[status(thm)],[c_11678]) ).
tff(c_14349,plain,
drugi(n0),
inference(resolution,[status(thm)],[c_14269,c_2]) ).
tff(c_14390,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1273,c_14349]) ).
tff(c_14392,plain,
~ s3('#skF_22'(n0)),
inference(splitRight,[status(thm)],[c_2235]) ).
tff(c_14395,plain,
! [X1_124] :
( conditionnormo(X1_124)
| gt(n0,X1_124)
| ~ s2(n0) ),
inference(resolution,[status(thm)],[c_1204,c_14392]) ).
tff(c_14453,plain,
! [X1_627] :
( conditionnormo(X1_627)
| gt(n0,X1_627) ),
inference(demodulation,[status(thm),theory(equality)],[c_1212,c_14395]) ).
tff(c_14503,plain,
conditionnormo(n0),
inference(resolution,[status(thm)],[c_14453,c_2]) ).
tff(c_14511,plain,
~ conditionhyper(n0),
inference(resolution,[status(thm)],[c_14503,c_18]) ).
tff(c_14498,plain,
! [X1_92] :
( drugi(X1_92)
| gt(n0,X1_92)
| conditionnormo('#skF_17'(n0)) ),
inference(resolution,[status(thm)],[c_14453,c_1166]) ).
tff(c_14996,plain,
conditionnormo('#skF_17'(n0)),
inference(splitLeft,[status(thm)],[c_14498]) ).
tff(c_15004,plain,
~ conditionhyper('#skF_17'(n0)),
inference(resolution,[status(thm)],[c_14996,c_18]) ).
tff(c_14391,plain,
! [X1_248] :
( conditionhyper(X1_248)
| conditionnormo(X1_248) ),
inference(splitRight,[status(thm)],[c_2235]) ).
tff(c_15193,plain,
! [X0_664,X1_665] :
( ~ conditionnormo('#skF_15'(X0_664))
| bcapacitysn(X0_664)
| bcapacityne(X0_664)
| uptakepg(X1_665)
| gt(X0_664,X1_665) ),
inference(cnfTransformation,[status(thm)],[f_412]) ).
tff(c_18961,plain,
! [X0_813,X1_814] :
( bcapacitysn(X0_813)
| bcapacityne(X0_813)
| uptakepg(X1_814)
| gt(X0_813,X1_814)
| conditionhyper('#skF_15'(X0_813)) ),
inference(resolution,[status(thm)],[c_14391,c_15193]) ).
tff(c_15941,plain,
! [X0_720,X1_721] :
( ~ conditionnormo('#skF_15'(X0_720))
| bcapacitysn(X0_720)
| bcapacityne(X0_720)
| conditionhyper(X1_721)
| ~ gt(X0_720,X1_721) ),
inference(cnfTransformation,[status(thm)],[f_412]) ).
tff(c_15945,plain,
! [X0_720,X1_721] :
( bcapacitysn(X0_720)
| bcapacityne(X0_720)
| conditionhyper(X1_721)
| ~ gt(X0_720,X1_721)
| conditionhyper('#skF_15'(X0_720)) ),
inference(resolution,[status(thm)],[c_14391,c_15941]) ).
tff(c_19061,plain,
! [X1_814,X0_813] :
( conditionhyper(X1_814)
| bcapacitysn(X0_813)
| bcapacityne(X0_813)
| uptakepg(X1_814)
| conditionhyper('#skF_15'(X0_813)) ),
inference(resolution,[status(thm)],[c_18961,c_15945]) ).
tff(c_19235,plain,
! [X0_813] :
( bcapacitysn(X0_813)
| bcapacityne(X0_813)
| conditionhyper('#skF_15'(X0_813)) ),
inference(splitLeft,[status(thm)],[c_19061]) ).
tff(c_14416,plain,
! [X1_124] :
( conditionnormo(X1_124)
| gt(n0,X1_124) ),
inference(demodulation,[status(thm),theory(equality)],[c_1212,c_14395]) ).
tff(c_16040,plain,
! [X0_727,X1_728] :
( ~ gt(X0_727,'#skF_15'(X0_727))
| bcapacitysn(X0_727)
| bcapacityne(X0_727)
| uptakepg(X1_728)
| gt(X0_727,X1_728) ),
inference(cnfTransformation,[status(thm)],[f_412]) ).
tff(c_16076,plain,
! [X1_728] :
( bcapacitysn(n0)
| bcapacityne(n0)
| uptakepg(X1_728)
| gt(n0,X1_728)
| conditionnormo('#skF_15'(n0)) ),
inference(resolution,[status(thm)],[c_14416,c_16040]) ).
tff(c_19237,plain,
conditionnormo('#skF_15'(n0)),
inference(splitLeft,[status(thm)],[c_16076]) ).
tff(c_19262,plain,
~ conditionhyper('#skF_15'(n0)),
inference(resolution,[status(thm)],[c_19237,c_18]) ).
tff(c_19371,plain,
( bcapacitysn(n0)
| bcapacityne(n0) ),
inference(resolution,[status(thm)],[c_19235,c_19262]) ).
tff(c_19374,plain,
bcapacityne(n0),
inference(splitLeft,[status(thm)],[c_19371]) ).
tff(c_19377,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_19374,c_8]) ).
tff(c_19381,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_19377]) ).
tff(c_19382,plain,
bcapacitysn(n0),
inference(splitRight,[status(thm)],[c_19371]) ).
tff(c_19420,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_19382,c_12]) ).
tff(c_19427,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_19420]) ).
tff(c_19428,plain,
! [X1_728] :
( bcapacityne(n0)
| bcapacitysn(n0)
| uptakepg(X1_728)
| gt(n0,X1_728) ),
inference(splitRight,[status(thm)],[c_16076]) ).
tff(c_19434,plain,
bcapacitysn(n0),
inference(splitLeft,[status(thm)],[c_19428]) ).
tff(c_19540,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_19434,c_12]) ).
tff(c_19547,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_19540]) ).
tff(c_19548,plain,
! [X1_728] :
( bcapacityne(n0)
| uptakepg(X1_728)
| gt(n0,X1_728) ),
inference(splitRight,[status(thm)],[c_19428]) ).
tff(c_19555,plain,
bcapacityne(n0),
inference(splitLeft,[status(thm)],[c_19548]) ).
tff(c_19592,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_19555,c_8]) ).
tff(c_19596,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_19592]) ).
tff(c_19599,plain,
! [X1_828] :
( uptakepg(X1_828)
| gt(n0,X1_828) ),
inference(splitRight,[status(thm)],[c_19548]) ).
tff(c_19702,plain,
! [X1_828] :
( conditionhyper(X1_828)
| uptakepg(X1_828) ),
inference(resolution,[status(thm)],[c_19599,c_1210]) ).
tff(c_19698,plain,
! [X1_92] :
( drugi(X1_92)
| gt(n0,X1_92)
| uptakepg('#skF_17'(n0)) ),
inference(resolution,[status(thm)],[c_19599,c_1166]) ).
tff(c_20026,plain,
uptakepg('#skF_17'(n0)),
inference(splitLeft,[status(thm)],[c_19698]) ).
tff(c_20030,plain,
! [X1_839] :
( drugi(X1_839)
| gt(n0,X1_839) ),
inference(resolution,[status(thm)],[c_20026,c_1164]) ).
tff(c_20105,plain,
drugi(n0),
inference(resolution,[status(thm)],[c_20030,c_2]) ).
tff(c_20150,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1273,c_20105]) ).
tff(c_20152,plain,
~ uptakepg('#skF_17'(n0)),
inference(splitRight,[status(thm)],[c_19698]) ).
tff(c_20160,plain,
conditionhyper('#skF_17'(n0)),
inference(resolution,[status(thm)],[c_19702,c_20152]) ).
tff(c_20164,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15004,c_20160]) ).
tff(c_20166,plain,
! [X1_842] :
( conditionhyper(X1_842)
| uptakepg(X1_842) ),
inference(splitRight,[status(thm)],[c_19061]) ).
tff(c_20171,plain,
! [X1_843,X0_844] :
( drugi(X1_843)
| gt(X0_844,X1_843)
| conditionhyper('#skF_17'(X0_844)) ),
inference(resolution,[status(thm)],[c_20166,c_1164]) ).
tff(c_20266,plain,
! [X1_843] :
( conditionhyper(X1_843)
| drugi(X1_843)
| conditionhyper('#skF_17'(n0)) ),
inference(resolution,[status(thm)],[c_20171,c_1210]) ).
tff(c_20309,plain,
! [X1_845] :
( conditionhyper(X1_845)
| drugi(X1_845) ),
inference(negUnitSimplification,[status(thm)],[c_15004,c_20266]) ).
tff(c_20339,plain,
conditionhyper(n0),
inference(resolution,[status(thm)],[c_20309,c_1273]) ).
tff(c_20352,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14511,c_20339]) ).
tff(c_20359,plain,
! [X1_846] :
( drugi(X1_846)
| gt(n0,X1_846) ),
inference(splitRight,[status(thm)],[c_14498]) ).
tff(c_20398,plain,
drugi(n0),
inference(resolution,[status(thm)],[c_20359,c_2]) ).
tff(c_20416,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1273,c_20398]) ).
tff(c_20418,plain,
~ bcapacityex('#skF_22'(n0)),
inference(splitRight,[status(thm)],[c_2128]) ).
tff(c_20421,plain,
! [X1_124] :
( conditionnormo(X1_124)
| gt(n0,X1_124)
| ~ s2(n0) ),
inference(resolution,[status(thm)],[c_1200,c_20418]) ).
tff(c_20436,plain,
! [X1_851] :
( conditionnormo(X1_851)
| gt(n0,X1_851) ),
inference(demodulation,[status(thm),theory(equality)],[c_1212,c_20421]) ).
tff(c_20479,plain,
! [X1_92] :
( drugi(X1_92)
| gt(n0,X1_92)
| conditionnormo('#skF_16'(n0)) ),
inference(resolution,[status(thm)],[c_20436,c_1170]) ).
tff(c_21116,plain,
conditionnormo('#skF_16'(n0)),
inference(splitLeft,[status(thm)],[c_20479]) ).
tff(c_21124,plain,
~ conditionhyper('#skF_16'(n0)),
inference(resolution,[status(thm)],[c_21116,c_18]) ).
tff(c_20481,plain,
! [X1_92] :
( drugi(X1_92)
| gt(n0,X1_92)
| conditionnormo('#skF_17'(n0)) ),
inference(resolution,[status(thm)],[c_20436,c_1166]) ).
tff(c_21066,plain,
conditionnormo('#skF_17'(n0)),
inference(splitLeft,[status(thm)],[c_20481]) ).
tff(c_21074,plain,
~ conditionhyper('#skF_17'(n0)),
inference(resolution,[status(thm)],[c_21066,c_18]) ).
tff(c_20417,plain,
! [X1_241] :
( conditionhyper(X1_241)
| conditionnormo(X1_241) ),
inference(splitRight,[status(thm)],[c_2128]) ).
tff(c_21909,plain,
! [X0_934,X1_935] :
( ~ conditionnormo('#skF_15'(X0_934))
| bcapacitysn(X0_934)
| bcapacityne(X0_934)
| uptakelg(X1_935)
| gt(X0_934,X1_935) ),
inference(cnfTransformation,[status(thm)],[f_412]) ).
tff(c_24236,plain,
! [X0_1029,X1_1030] :
( bcapacitysn(X0_1029)
| bcapacityne(X0_1029)
| uptakelg(X1_1030)
| gt(X0_1029,X1_1030)
| conditionhyper('#skF_15'(X0_1029)) ),
inference(resolution,[status(thm)],[c_20417,c_21909]) ).
tff(c_24354,plain,
! [X1_1030] :
( conditionhyper(X1_1030)
| bcapacitysn(n0)
| bcapacityne(n0)
| uptakelg(X1_1030)
| conditionhyper('#skF_15'(n0)) ),
inference(resolution,[status(thm)],[c_24236,c_1210]) ).
tff(c_24356,plain,
conditionhyper('#skF_15'(n0)),
inference(splitLeft,[status(thm)],[c_24354]) ).
tff(c_20424,plain,
! [X1_124] :
( conditionnormo(X1_124)
| gt(n0,X1_124) ),
inference(demodulation,[status(thm),theory(equality)],[c_1212,c_20421]) ).
tff(c_23172,plain,
! [X0_996,X1_997] :
( ~ gt(X0_996,'#skF_15'(X0_996))
| bcapacitysn(X0_996)
| bcapacityne(X0_996)
| uptakepg(X1_997)
| gt(X0_996,X1_997) ),
inference(cnfTransformation,[status(thm)],[f_412]) ).
tff(c_23241,plain,
! [X1_997] :
( bcapacitysn(n0)
| bcapacityne(n0)
| uptakepg(X1_997)
| gt(n0,X1_997)
| conditionnormo('#skF_15'(n0)) ),
inference(resolution,[status(thm)],[c_20424,c_23172]) ).
tff(c_24690,plain,
conditionnormo('#skF_15'(n0)),
inference(splitLeft,[status(thm)],[c_23241]) ).
tff(c_24706,plain,
~ conditionhyper('#skF_15'(n0)),
inference(resolution,[status(thm)],[c_24690,c_18]) ).
tff(c_24718,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_24356,c_24706]) ).
tff(c_24719,plain,
! [X1_997] :
( bcapacityne(n0)
| bcapacitysn(n0)
| uptakepg(X1_997)
| gt(n0,X1_997) ),
inference(splitRight,[status(thm)],[c_23241]) ).
tff(c_24855,plain,
bcapacitysn(n0),
inference(splitLeft,[status(thm)],[c_24719]) ).
tff(c_24858,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_24855,c_12]) ).
tff(c_24865,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_24858]) ).
tff(c_24866,plain,
! [X1_997] :
( bcapacityne(n0)
| uptakepg(X1_997)
| gt(n0,X1_997) ),
inference(splitRight,[status(thm)],[c_24719]) ).
tff(c_25003,plain,
bcapacityne(n0),
inference(splitLeft,[status(thm)],[c_24866]) ).
tff(c_25006,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_25003,c_8]) ).
tff(c_25010,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_25006]) ).
tff(c_25013,plain,
! [X1_1046] :
( uptakepg(X1_1046)
| gt(n0,X1_1046) ),
inference(splitRight,[status(thm)],[c_24866]) ).
tff(c_25116,plain,
! [X1_1046] :
( conditionhyper(X1_1046)
| uptakepg(X1_1046) ),
inference(resolution,[status(thm)],[c_25013,c_1210]) ).
tff(c_25112,plain,
! [X1_92] :
( drugi(X1_92)
| gt(n0,X1_92)
| uptakepg('#skF_17'(n0)) ),
inference(resolution,[status(thm)],[c_25013,c_1166]) ).
tff(c_25400,plain,
uptakepg('#skF_17'(n0)),
inference(splitLeft,[status(thm)],[c_25112]) ).
tff(c_25537,plain,
! [X1_1055] :
( drugi(X1_1055)
| gt(n0,X1_1055) ),
inference(resolution,[status(thm)],[c_25400,c_1164]) ).
tff(c_25609,plain,
drugi(n0),
inference(resolution,[status(thm)],[c_25537,c_2]) ).
tff(c_25651,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1273,c_25609]) ).
tff(c_25653,plain,
~ uptakepg('#skF_17'(n0)),
inference(splitRight,[status(thm)],[c_25112]) ).
tff(c_25656,plain,
conditionhyper('#skF_17'(n0)),
inference(resolution,[status(thm)],[c_25116,c_25653]) ).
tff(c_25660,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21074,c_25656]) ).
tff(c_25661,plain,
! [X1_1030] :
( bcapacityne(n0)
| bcapacitysn(n0)
| conditionhyper(X1_1030)
| uptakelg(X1_1030) ),
inference(splitRight,[status(thm)],[c_24354]) ).
tff(c_25667,plain,
bcapacitysn(n0),
inference(splitLeft,[status(thm)],[c_25661]) ).
tff(c_25670,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_25667,c_12]) ).
tff(c_25677,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_25670]) ).
tff(c_25678,plain,
! [X1_1030] :
( bcapacityne(n0)
| conditionhyper(X1_1030)
| uptakelg(X1_1030) ),
inference(splitRight,[status(thm)],[c_25661]) ).
tff(c_25685,plain,
bcapacityne(n0),
inference(splitLeft,[status(thm)],[c_25678]) ).
tff(c_25688,plain,
~ bcapacityex(n0),
inference(resolution,[status(thm)],[c_25685,c_8]) ).
tff(c_25692,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1208,c_25688]) ).
tff(c_25828,plain,
! [X1_1059] :
( conditionhyper(X1_1059)
| uptakelg(X1_1059) ),
inference(splitRight,[status(thm)],[c_25678]) ).
tff(c_25837,plain,
! [X1_1060] :
( ~ releaselg(X1_1060)
| conditionhyper(X1_1060) ),
inference(resolution,[status(thm)],[c_25828,c_1342]) ).
tff(c_25948,plain,
conditionhyper('#skF_16'(n0)),
inference(resolution,[status(thm)],[c_2005,c_25837]) ).
tff(c_26006,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_21124,c_25948]) ).
tff(c_26049,plain,
! [X1_1063] :
( drugi(X1_1063)
| gt(n0,X1_1063) ),
inference(splitRight,[status(thm)],[c_20479]) ).
tff(c_26088,plain,
drugi(n0),
inference(resolution,[status(thm)],[c_26049,c_2]) ).
tff(c_26106,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1273,c_26088]) ).
tff(c_26113,plain,
! [X1_1064] :
( drugi(X1_1064)
| gt(n0,X1_1064) ),
inference(splitRight,[status(thm)],[c_20481]) ).
tff(c_26152,plain,
drugi(n0),
inference(resolution,[status(thm)],[c_26113,c_2]) ).
tff(c_26170,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1273,c_26152]) ).
tff(c_26172,plain,
~ releaselg('#skF_16'(n0)),
inference(splitRight,[status(thm)],[c_2002]) ).
tff(c_26184,plain,
drugi(n0),
inference(resolution,[status(thm)],[c_2003,c_26172]) ).
tff(c_26191,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1273,c_26184]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : MED010+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/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.12/0.34 % Computer : n003.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Tue Apr 8 07:47:19 EDT 2025
% 0.12/0.34 % CPUTime :
% 21.00/6.96 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.23/6.99
% 21.23/6.99 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------