%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NUM862_1 : TPTP v9.0.0. Released v4.1.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 : n020.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:57:24 PM UTC 2025
% Result : Theorem 14.27s 4.43s
% Output : CNFRefutation 15.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 9
% Syntax : Number of formulae : 982 ( 633 unt; 0 typ; 0 def)
% Number of atoms : 1530 ( 241 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 1010 ( 462 ~; 535 |; 4 &)
% ( 7 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 1632 ( 856 atm; 344 fun; 0 num; 432 var)
% Number of types : 2 ( 0 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 28 ( 27 usr; 22 con; 0-3 aty)
% Number of variables : 432 ( 431 !; 1 ?; 432 :)
% Comments :
%------------------------------------------------------------------------------
%$ ub > model_ub > model_max > minsol_model_ub > minsol_model_max > max > #nlpp > summation > #skF_3 > #skF_1 > #skF_2
%Foreground sorts:
%Background operators:
tff('#skE_7',type,
'#skE_7': $int ).
tff(c,type,
c: $int ).
tff('#skE_11',type,
'#skE_11': $int ).
tff('#skE_12',type,
'#skE_12': $int ).
tff('#skF_6',type,
'#skF_6': $int ).
tff('#skE_2',type,
'#skE_2': $int ).
tff('#skE_1',type,
'#skE_1': $int ).
tff('#skE_6',type,
'#skE_6': $int ).
tff('#skE_13',type,
'#skE_13': $int ).
tff('#skE_10',type,
'#skE_10': $int ).
tff('#skE_5',type,
'#skE_5': $int ).
tff('#skE_15',type,
'#skE_15': $int ).
tff('#skE_8',type,
'#skE_8': $int ).
tff('#skF_8',type,
'#skF_8': $int ).
tff('#skE_4',type,
'#skE_4': $int ).
tff('#skF_5',type,
'#skF_5': $int ).
tff('#skF_4',type,
'#skF_4': $int ).
tff('#skE_3',type,
'#skE_3': $int ).
tff('#skF_7',type,
'#skF_7': $int ).
tff('#skE_9',type,
'#skE_9': $int ).
tff('#skF_9',type,
'#skF_9': $int ).
tff('#skE_14',type,
'#skE_14': $int ).
%Foreground operators:
tff(minsol_model_ub,type,
minsol_model_ub: ( $int * $int * $int ) > $o ).
tff('#skF_3',type,
'#skF_3': ( $int * $int * $int ) > $int ).
tff(model_max,type,
model_max: ( $int * $int * $int ) > $o ).
tff(minsol_model_max,type,
minsol_model_max: ( $int * $int * $int ) > $o ).
tff(summation,type,
summation: $int > $int ).
tff(max,type,
max: ( $int * $int ) > $int ).
tff('#skF_1',type,
'#skF_1': ( $int * $int * $int ) > $int ).
tff(model_ub,type,
model_ub: ( $int * $int * $int ) > $o ).
tff(ub,type,
ub: ( $int * $int * $int ) > $o ).
tff('#skF_2',type,
'#skF_2': ( $int * $int * $int ) > $int ).
tff(f_49,axiom,
! [Xa: $int,Ya: $int] :
( ( max(Xa,Ya) = Ya )
| ~ $lesseq(Xa,Ya) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',max_2) ).
tff(f_95,negated_conjecture,
~ ! [Xa: $int,Ya: $int,Za: $int] :
( minsol_model_ub(Xa,Ya,Za)
<=> minsol_model_max(Xa,Ya,Za) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',max_is_ub_1) ).
tff(f_89,axiom,
! [Xa: $int,Ya: $int,Na: $int] :
( minsol_model_ub(Xa,Ya,Na)
<=> ( model_ub(Xa,Ya,Na)
& ! [Za: $int] :
( model_ub(Xa,Ya,Za)
=> $lesseq(Na,Za) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',minsol_model_ub) ).
tff(f_69,axiom,
! [Xa: $int,Ya: $int,Na: $int] :
( model_ub(Xa,Ya,Na)
<=> ? [Za: $int] :
( ub(Xa,Ya,Za)
& $lesseq($sum(c,summation(Za)),Na) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',model_ub_5) ).
tff(f_61,axiom,
! [Xa: $int,Ya: $int,Na: $int] :
( model_max(Xa,Ya,Na)
<=> $lesseq($sum(c,summation(max(Xa,Ya))),Na) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',model_max_5) ).
tff(f_79,axiom,
! [Xa: $int,Ya: $int,Na: $int] :
( minsol_model_max(Xa,Ya,Na)
<=> ( model_max(Xa,Ya,Na)
& ! [Za: $int] :
( model_max(Xa,Ya,Za)
=> $lesseq(Na,Za) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',minsol_model_max) ).
tff(f_44,axiom,
! [Xa: $int,Ya: $int] :
( ( max(Xa,Ya) = Xa )
| ~ $lesseq(Ya,Xa) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',max_1) ).
tff(f_56,axiom,
! [Xa: $int,Ya: $int,Za: $int] :
( ub(Xa,Ya,Za)
<=> ( $lesseq(Xa,Za)
& $lesseq(Ya,Za) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ub) ).
tff(f_38,axiom,
! [Xa: $int,Ya: $int] :
( $lesseq(Xa,Ya)
<=> $lesseq(summation(Xa),summation(Ya)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',summation_monotone) ).
tff(c_7,plain,
! [X_5a: $int,Y_6a: $int] :
( ( max(X_5a,Y_6a) = Y_6a )
| ~ $lesseq(X_5a,Y_6a) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_99,plain,
! [X_5a: $int,Y_6a: $int] :
( ( max(X_5a,Y_6a) = Y_6a )
| $less(Y_6a,X_5a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_7]) ).
tff(c_58,plain,
( minsol_model_max('#skF_4','#skF_5','#skF_6')
| minsol_model_ub('#skF_7','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_290,plain,
minsol_model_ub('#skF_7','#skF_8','#skF_9'),
inference(splitLeft,[status(thm)],[c_58]) ).
tff(c_73,plain,
! [X_25a: $int,Y_26a: $int,N_27a: $int] :
( model_ub(X_25a,Y_26a,N_27a)
| ~ minsol_model_ub(X_25a,Y_26a,N_27a) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_25,plain,
! [X_13a: $int,Y_14a: $int,N_15a: $int] :
( $lesseq($sum(c,summation('#skF_1'(X_13a,Y_14a,N_15a))),N_15a)
| ~ model_ub(X_13a,Y_14a,N_15a) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_242,plain,
! [N_165a: $int,X_167a: $int,Y_168a: $int] :
( ~ $less(N_165a,$sum(c,summation('#skF_1'(X_167a,Y_168a,N_165a))))
| ~ model_ub(X_167a,Y_168a,N_165a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_25]) ).
tff(c_248,plain,
! [N_27a: $int,X_25a: $int,Y_26a: $int] :
( ~ $less(N_27a,$sum(c,summation('#skF_1'(X_25a,Y_26a,N_27a))))
| ~ minsol_model_ub(X_25a,Y_26a,N_27a) ),
inference(resolution,[status(thm)],[c_73,c_242]) ).
tff(c_301,plain,
~ $less('#skF_9',$sum(c,summation('#skF_1'('#skF_7','#skF_8','#skF_9')))),
inference(resolution,[status(thm)],[c_290,c_248]) ).
tff(c_320,plain,
'#skF_1'('#skF_7','#skF_8','#skF_9') = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_301]) ).
tff(c_319,plain,
~ $less('#skF_9',$sum(c,summation('#skF_1'('#skF_7','#skF_8','#skF_9')))),
inference(resolution,[status(thm)],[c_290,c_248]) ).
tff(c_330,plain,
~ $less('#skF_9',$sum(c,summation('#skE_1'))),
inference(demodulation,[status(thm),theory(equality)],[c_320,c_319]) ).
tff(c_364,plain,
summation('#skE_1') = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_330]) ).
tff(c_19,plain,
! [X_10a: $int,Y_11a: $int,N_12a: $int] :
( model_max(X_10a,Y_11a,N_12a)
| ~ $lesseq($sum(c,summation(max(X_10a,Y_11a))),N_12a) ),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_213,plain,
! [X_147a: $int,Y_148a: $int,N_149a: $int] :
( model_max(X_147a,Y_148a,N_149a)
| $less(N_149a,$sum(c,summation(max(X_147a,Y_148a)))) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_19]) ).
tff(c_34,plain,
! [N_21a: $int,X_19a: $int,Y_20a: $int] :
( ~ $lesseq(N_21a,'#skF_2'(X_19a,Y_20a,N_21a))
| minsol_model_max(X_19a,Y_20a,N_21a)
| ~ model_max(X_19a,Y_20a,N_21a) ),
inference(cnfTransformation,[status(thm)],[f_79]) ).
tff(c_76,plain,
! [X_19a: $int,Y_20a: $int,N_21a: $int] :
( $less('#skF_2'(X_19a,Y_20a,N_21a),N_21a)
| minsol_model_max(X_19a,Y_20a,N_21a)
| ~ model_max(X_19a,Y_20a,N_21a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_34]) ).
tff(c_456,plain,
! [X_254a: $int,Y_255a: $int,N_256a: $int] :
( $less('#skF_2'(X_254a,Y_255a,N_256a),N_256a)
| minsol_model_max(X_254a,Y_255a,N_256a)
| $less(N_256a,$sum(c,summation(max(X_254a,Y_255a)))) ),
inference(resolution,[status(thm)],[c_213,c_76]) ).
tff(c_66,plain,
( minsol_model_max('#skF_4','#skF_5','#skF_6')
| ~ minsol_model_max('#skF_7','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_203,plain,
~ minsol_model_max('#skF_7','#skF_8','#skF_9'),
inference(splitLeft,[status(thm)],[c_66]) ).
tff(c_475,plain,
( $less('#skF_2'('#skF_7','#skF_8','#skF_9'),'#skF_9')
| $less('#skF_9',$sum(c,summation(max('#skF_7','#skF_8')))) ),
inference(resolution,[status(thm)],[c_456,c_203]) ).
tff(c_1003,plain,
max('#skF_7','#skF_8') = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_475]) ).
tff(c_1035,plain,
( ( '#skF_8' = '#skE_4' )
| $less('#skF_8','#skF_7') ),
inference(superposition,[status(thm),theory(equality)],[c_99,c_1003]) ).
tff(c_1039,plain,
$less('#skF_8','#skF_7'),
inference(splitLeft,[status(thm)],[c_1035]) ).
tff(c_5,plain,
! [X_3a: $int,Y_4a: $int] :
( ( max(X_3a,Y_4a) = X_3a )
| ~ $lesseq(Y_4a,X_3a) ),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_100,plain,
! [X_3a: $int,Y_4a: $int] :
( ( max(X_3a,Y_4a) = X_3a )
| $less(X_3a,Y_4a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_5]) ).
tff(c_1026,plain,
( ( '#skF_7' = '#skE_4' )
| $less('#skF_7','#skF_8') ),
inference(superposition,[status(thm),theory(equality)],[c_1003,c_100]) ).
tff(c_1037,plain,
$less('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_1026]) ).
tff(c_1040,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_1039,c_1037]) ).
tff(c_1043,plain,
'#skF_8' = '#skE_4',
inference(splitRight,[status(thm)],[c_1035]) ).
tff(c_1044,plain,
~ $less('#skF_8','#skF_7'),
inference(splitRight,[status(thm)],[c_1035]) ).
tff(c_1154,plain,
~ $less('#skE_4','#skF_7'),
inference(demodulation,[status(thm),theory(equality)],[c_1043,c_1044]) ).
tff(c_986,plain,
max('#skF_7','#skF_8') = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_475]) ).
tff(c_985,plain,
'#skF_2'('#skF_7','#skF_8','#skF_9') = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_475]) ).
tff(c_486,plain,
( $less('#skF_2'('#skF_7','#skF_8','#skF_9'),'#skF_9')
| $less('#skF_9',$sum(c,summation(max('#skF_7','#skF_8')))) ),
inference(resolution,[status(thm)],[c_456,c_203]) ).
tff(c_1000,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,summation('#skE_4'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_986,c_985,c_486]) ).
tff(c_1606,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_1000]) ).
tff(c_287,plain,
minsol_model_ub('#skF_7','#skF_8','#skF_9'),
inference(splitLeft,[status(thm)],[c_58]) ).
tff(c_13,plain,
! [X_7a: $int,Y_8a: $int,Z_9a: $int] :
( ub(X_7a,Y_8a,Z_9a)
| ~ $lesseq(X_7a,Z_9a)
| ~ $lesseq(Y_8a,Z_9a) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_96,plain,
! [X_7a: $int,Y_8a: $int,Z_9a: $int] :
( ub(X_7a,Y_8a,Z_9a)
| $less(Z_9a,X_7a)
| $less(Z_9a,Y_8a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_13]) ).
tff(c_22,plain,
! [X_13a: $int,Y_14a: $int,N_15a: $int,Z_18a: $int] :
( model_ub(X_13a,Y_14a,N_15a)
| ~ $lesseq($sum(c,summation(Z_18a)),N_15a)
| ~ ub(X_13a,Y_14a,Z_18a) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_253,plain,
! [X_177a: $int,Y_181a: $int,N_180a: $int,Z_179a: $int] :
( model_ub(X_177a,Y_181a,N_180a)
| $less(N_180a,$sum(c,summation(Z_179a)))
| ~ ub(X_177a,Y_181a,Z_179a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_22]) ).
tff(c_265,plain,
! [X_190a: $int,Y_191a: $int,N_189a: $int,Z_192a: $int] :
( model_ub(X_190a,Y_191a,N_189a)
| $less(N_189a,$sum(c,summation(Z_192a)))
| $less(Z_192a,X_190a)
| $less(Z_192a,Y_191a) ),
inference(resolution,[status(thm)],[c_96,c_253]) ).
tff(c_38,plain,
! [X_25a: $int,Y_26a: $int,Z_30a: $int,N_27a: $int] :
( ~ model_ub(X_25a,Y_26a,Z_30a)
| ~ minsol_model_ub(X_25a,Y_26a,N_27a)
| $lesseq(N_27a,Z_30a) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_74,plain,
! [X_25a: $int,Y_26a: $int,Z_30a: $int,N_27a: $int] :
( ~ model_ub(X_25a,Y_26a,Z_30a)
| ~ minsol_model_ub(X_25a,Y_26a,N_27a)
| ~ $less(Z_30a,N_27a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_38]) ).
tff(c_958,plain,
! [N_512a: $int,Z_513a: $int,X_511a: $int,N_515a: $int,Y_514a: $int] :
( ~ minsol_model_ub(X_511a,Y_514a,N_512a)
| ~ $less(N_515a,N_512a)
| $less(N_515a,$sum(c,summation(Z_513a)))
| $less(Z_513a,X_511a)
| $less(Z_513a,Y_514a) ),
inference(resolution,[status(thm)],[c_265,c_74]) ).
tff(c_964,plain,
! [N_515a: $int,Z_513a: $int] :
( ~ $less(N_515a,'#skF_9')
| $less(N_515a,$sum(c,summation(Z_513a)))
| $less(Z_513a,'#skF_7')
| $less(Z_513a,'#skF_8') ),
inference(resolution,[status(thm)],[c_287,c_958]) ).
tff(c_1713,plain,
! [N_839a: $int,Z_841a: $int] :
( ~ $less(N_839a,'#skF_9')
| $less(N_839a,$sum(c,summation(Z_841a)))
| $less(Z_841a,'#skF_7')
| $less(Z_841a,'#skE_4') ),
inference(demodulation,[status(thm),theory(equality)],[c_1043,c_964]) ).
tff(c_1720,plain,
! [N_839a: $int] :
( ~ $less(N_839a,'#skF_9')
| $less(N_839a,$sum(c,'#skE_5'))
| $less('#skE_4','#skF_7')
| $less('#skE_4','#skE_4') ),
inference(superposition,[status(thm),theory(equality)],[c_1606,c_1713]) ).
tff(c_1722,plain,
! [N_839a: $int] :
( ~ $less(N_839a,'#skF_9')
| $less(N_839a,$sum(c,'#skE_5'))
| $less('#skE_4','#skF_7') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1720]) ).
tff(c_1816,plain,
! [N_839a: $int] :
( ~ $less(N_839a,'#skF_9')
| $less(N_839a,$sum(c,'#skE_5')) ),
inference(negUnitSimplification,[status(thm)],[c_1154,c_1722]) ).
tff(c_1817,plain,
$lesseq('#skF_9',$sum('#skE_5',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_1816]) ).
tff(c_1819,plain,
~ $less($sum(c,'#skE_5'),'#skF_9'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1817]) ).
tff(c_1610,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_1000]) ).
tff(c_365,plain,
summation('#skE_1') = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_330]) ).
tff(c_1,plain,
! [X_1a: $int,Y_2a: $int] :
( $lesseq(summation(X_1a),summation(Y_2a))
| ~ $lesseq(X_1a,Y_2a) ),
inference(cnfTransformation,[status(thm)],[f_38]) ).
tff(c_102,plain,
! [Y_2a: $int,X_1a: $int] :
( ~ $less(summation(Y_2a),summation(X_1a))
| $less(Y_2a,X_1a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_1]) ).
tff(c_402,plain,
! [Y_2a: $int] :
( ~ $less(summation(Y_2a),'#skE_2')
| $less(Y_2a,'#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_365,c_102]) ).
tff(c_1657,plain,
( ~ $less('#skE_5','#skE_2')
| $less('#skE_4','#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_1610,c_402]) ).
tff(c_1703,plain,
~ $less('#skE_5','#skE_2'),
inference(splitLeft,[status(thm)],[c_1657]) ).
tff(c_3,plain,
! [X_1a: $int,Y_2a: $int] :
( ~ $lesseq(summation(X_1a),summation(Y_2a))
| $lesseq(X_1a,Y_2a) ),
inference(cnfTransformation,[status(thm)],[f_38]) ).
tff(c_101,plain,
! [Y_2a: $int,X_1a: $int] :
( $less(summation(Y_2a),summation(X_1a))
| ~ $less(Y_2a,X_1a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_3]) ).
tff(c_396,plain,
! [Y_2a: $int] :
( $less(summation(Y_2a),'#skE_2')
| ~ $less(Y_2a,'#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_365,c_101]) ).
tff(c_1661,plain,
( $less('#skE_5','#skE_2')
| ~ $less('#skE_4','#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_1610,c_396]) ).
tff(c_1705,plain,
~ $less('#skE_4','#skE_1'),
inference(negUnitSimplification,[status(thm)],[c_1703,c_1661]) ).
tff(c_361,plain,
summation('#skE_1') = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_330]) ).
tff(c_1663,plain,
( ( '#skE_5' = '#skE_2' )
| ( '#skE_4' != '#skE_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_1610,c_361]) ).
tff(c_1682,plain,
'#skE_4' != '#skE_1',
inference(splitLeft,[status(thm)],[c_1663]) ).
tff(c_505,plain,
max('#skF_7','#skF_8') = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_475]) ).
tff(c_530,plain,
( ( '#skF_8' = '#skE_4' )
| $less('#skF_8','#skF_7') ),
inference(superposition,[status(thm),theory(equality)],[c_505,c_99]) ).
tff(c_543,plain,
$less('#skF_8','#skF_7'),
inference(splitLeft,[status(thm)],[c_530]) ).
tff(c_528,plain,
( ( '#skF_7' = '#skE_4' )
| $less('#skF_7','#skF_8') ),
inference(superposition,[status(thm),theory(equality)],[c_505,c_100]) ).
tff(c_539,plain,
$less('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_528]) ).
tff(c_566,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_543,c_539]) ).
tff(c_569,plain,
'#skF_8' = '#skE_4',
inference(splitRight,[status(thm)],[c_530]) ).
tff(c_687,plain,
minsol_model_ub('#skF_7','#skE_4','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_569,c_287]) ).
tff(c_333,plain,
'#skF_1'('#skF_7','#skF_8','#skF_9') = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_301]) ).
tff(c_79,plain,
! [X_13a: $int,Y_14a: $int,N_15a: $int] :
( ub(X_13a,Y_14a,'#skF_1'(X_13a,Y_14a,N_15a))
| ~ model_ub(X_13a,Y_14a,N_15a) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_349,plain,
( ub('#skF_7','#skF_8','#skE_1')
| ~ model_ub('#skF_7','#skF_8','#skF_9') ),
inference(superposition,[status(thm),theory(equality)],[c_333,c_79]) ).
tff(c_484,plain,
~ model_ub('#skF_7','#skF_8','#skF_9'),
inference(splitLeft,[status(thm)],[c_349]) ).
tff(c_673,plain,
~ model_ub('#skF_7','#skE_4','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_569,c_484]) ).
tff(c_685,plain,
~ minsol_model_ub('#skF_7','#skE_4','#skF_9'),
inference(resolution,[status(thm)],[c_73,c_673]) ).
tff(c_734,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_687,c_685]) ).
tff(c_737,plain,
'#skF_7' = '#skE_4',
inference(splitRight,[status(thm)],[c_528]) ).
tff(c_783,plain,
minsol_model_ub('#skE_4','#skF_8','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_737,c_287]) ).
tff(c_895,plain,
~ model_ub('#skE_4','#skF_8','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_737,c_484]) ).
tff(c_901,plain,
~ minsol_model_ub('#skE_4','#skF_8','#skF_9'),
inference(resolution,[status(thm)],[c_73,c_895]) ).
tff(c_908,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_783,c_901]) ).
tff(c_915,plain,
ub('#skF_7','#skF_8','#skE_1'),
inference(splitRight,[status(thm)],[c_349]) ).
tff(c_9,plain,
! [X_7a: $int,Y_8a: $int,Z_9a: $int] :
( ~ ub(X_7a,Y_8a,Z_9a)
| $lesseq(Y_8a,Z_9a) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_98,plain,
! [X_7a: $int,Y_8a: $int,Z_9a: $int] :
( ~ ub(X_7a,Y_8a,Z_9a)
| ~ $less(Z_9a,Y_8a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_9]) ).
tff(c_932,plain,
~ $less('#skE_1','#skF_8'),
inference(resolution,[status(thm)],[c_915,c_98]) ).
tff(c_1137,plain,
~ $less('#skE_1','#skE_4'),
inference(demodulation,[status(thm),theory(equality)],[c_1043,c_932]) ).
tff(c_1706,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_1705,c_1682,c_1137]) ).
tff(c_1710,plain,
$less('#skE_5','#skE_2'),
inference(splitRight,[status(thm)],[c_1657]) ).
tff(c_355,plain,
summation('#skE_1') = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_330]) ).
tff(c_354,plain,
~ $less('#skF_9',$sum(c,summation('#skE_1'))),
inference(demodulation,[status(thm),theory(equality)],[c_320,c_319]) ).
tff(c_362,plain,
~ $less('#skF_9',$sum(c,'#skE_2')),
inference(demodulation,[status(thm),theory(equality)],[c_355,c_354]) ).
tff(c_1820,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_1819,c_1710,c_362]) ).
tff(c_1824,plain,
'#skE_4' = '#skE_1',
inference(splitRight,[status(thm)],[c_1663]) ).
tff(c_997,plain,
max('#skF_7','#skF_8') = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_475]) ).
tff(c_1127,plain,
max('#skF_7','#skE_4') = '#skE_4',
inference(demodulation,[status(thm),theory(equality)],[c_1043,c_997]) ).
tff(c_1950,plain,
max('#skF_7','#skE_1') = '#skE_1',
inference(demodulation,[status(thm),theory(equality)],[c_1824,c_1824,c_1127]) ).
tff(c_1185,plain,
max('#skF_7','#skE_4') = '#skE_4',
inference(demodulation,[status(thm),theory(equality)],[c_1043,c_997]) ).
tff(c_91,plain,
! [X_10a: $int,Y_11a: $int,N_12a: $int] :
( model_max(X_10a,Y_11a,N_12a)
| $less(N_12a,$sum(c,summation(max(X_10a,Y_11a)))) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_19]) ).
tff(c_1047,plain,
'#skF_2'('#skF_7','#skF_8','#skF_9') = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_475]) ).
tff(c_75,plain,
! [X_19a: $int,Y_20a: $int,N_21a: $int] :
( model_max(X_19a,Y_20a,'#skF_2'(X_19a,Y_20a,N_21a))
| minsol_model_max(X_19a,Y_20a,N_21a)
| ~ model_max(X_19a,Y_20a,N_21a) ),
inference(cnfTransformation,[status(thm)],[f_79]) ).
tff(c_1063,plain,
( model_max('#skF_7','#skF_8','#skE_3')
| minsol_model_max('#skF_7','#skF_8','#skF_9')
| ~ model_max('#skF_7','#skF_8','#skF_9') ),
inference(superposition,[status(thm),theory(equality)],[c_1047,c_75]) ).
tff(c_1340,plain,
( model_max('#skF_7','#skE_4','#skE_3')
| minsol_model_max('#skF_7','#skE_4','#skF_9')
| ~ model_max('#skF_7','#skE_4','#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_1043,c_1043,c_1043,c_1063]) ).
tff(c_1348,plain,
~ model_max('#skF_7','#skE_4','#skF_9'),
inference(splitLeft,[status(thm)],[c_1340]) ).
tff(c_1351,plain,
$less('#skF_9',$sum(c,summation(max('#skF_7','#skE_4')))),
inference(resolution,[status(thm)],[c_91,c_1348]) ).
tff(c_1360,plain,
$less('#skF_9',$sum(c,summation('#skE_4'))),
inference(demodulation,[status(thm),theory(equality)],[c_1185,c_1351]) ).
tff(c_1374,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_1360]) ).
tff(c_1425,plain,
( $less('#skE_5','#skE_2')
| ~ $less('#skE_4','#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_1374,c_396]) ).
tff(c_1450,plain,
~ $less('#skE_4','#skE_1'),
inference(splitLeft,[status(thm)],[c_1425]) ).
tff(c_1427,plain,
( ( '#skE_5' = '#skE_2' )
| ( '#skE_4' != '#skE_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_1374,c_361]) ).
tff(c_1448,plain,
'#skE_4' != '#skE_1',
inference(splitLeft,[status(thm)],[c_1427]) ).
tff(c_1470,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_1450,c_1448,c_1137]) ).
tff(c_1473,plain,
$less('#skE_5','#skE_2'),
inference(splitRight,[status(thm)],[c_1425]) ).
tff(c_1364,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_1360]) ).
tff(c_1363,plain,
$less('#skF_9',$sum(c,summation('#skE_4'))),
inference(demodulation,[status(thm),theory(equality)],[c_1185,c_1351]) ).
tff(c_1371,plain,
$less('#skF_9',$sum(c,'#skE_5')),
inference(demodulation,[status(thm),theory(equality)],[c_1364,c_1363]) ).
tff(c_1475,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_1473,c_1371,c_362]) ).
tff(c_1478,plain,
'#skE_5' = '#skE_2',
inference(splitRight,[status(thm)],[c_1427]) ).
tff(c_1592,plain,
$less('#skF_9',$sum(c,'#skE_2')),
inference(demodulation,[status(thm),theory(equality)],[c_1478,c_1371]) ).
tff(c_1593,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_362,c_1592]) ).
tff(c_1597,plain,
( minsol_model_max('#skF_7','#skE_4','#skF_9')
| model_max('#skF_7','#skE_4','#skE_3') ),
inference(splitRight,[status(thm)],[c_1340]) ).
tff(c_2086,plain,
( minsol_model_max('#skF_7','#skE_1','#skF_9')
| model_max('#skF_7','#skE_1','#skE_3') ),
inference(demodulation,[status(thm),theory(equality)],[c_1824,c_1824,c_1597]) ).
tff(c_2094,plain,
model_max('#skF_7','#skE_1','#skE_3'),
inference(splitLeft,[status(thm)],[c_2086]) ).
tff(c_16,plain,
! [X_10a: $int,Y_11a: $int,N_12a: $int] :
( $lesseq($sum(c,summation(max(X_10a,Y_11a))),N_12a)
| ~ model_max(X_10a,Y_11a,N_12a) ),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_95,plain,
! [N_12a: $int,X_10a: $int,Y_11a: $int] :
( ~ $less(N_12a,$sum(c,summation(max(X_10a,Y_11a))))
| ~ model_max(X_10a,Y_11a,N_12a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_16]) ).
tff(c_2097,plain,
~ $less('#skE_3',$sum(c,summation(max('#skF_7','#skE_1')))),
inference(resolution,[status(thm)],[c_2094,c_95]) ).
tff(c_2106,plain,
~ $less('#skE_3',$sum(c,'#skE_2')),
inference(demodulation,[status(thm),theory(equality)],[c_364,c_1950,c_2097]) ).
tff(c_1823,plain,
'#skE_5' = '#skE_2',
inference(splitRight,[status(thm)],[c_1663]) ).
tff(c_1600,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_1000]) ).
tff(c_1489,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,summation('#skE_4'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_986,c_985,c_486]) ).
tff(c_1607,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,'#skE_5')) ),
inference(demodulation,[status(thm),theory(equality)],[c_1600,c_1489]) ).
tff(c_1990,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,'#skE_2')) ),
inference(demodulation,[status(thm),theory(equality)],[c_1823,c_1607]) ).
tff(c_1992,plain,
$less('#skE_3','#skF_9'),
inference(negUnitSimplification,[status(thm)],[c_362,c_1990]) ).
tff(c_87,plain,
! [X_13a: $int,Y_14a: $int,N_15a: $int,Z_18a: $int] :
( model_ub(X_13a,Y_14a,N_15a)
| $less(N_15a,$sum(c,summation(Z_18a)))
| ~ ub(X_13a,Y_14a,Z_18a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_22]) ).
tff(c_918,plain,
! [N_15a: $int] :
( model_ub('#skF_7','#skF_8',N_15a)
| $less(N_15a,$sum(c,summation('#skE_1'))) ),
inference(resolution,[status(thm)],[c_915,c_87]) ).
tff(c_937,plain,
! [N_500a: $int] :
( model_ub('#skF_7','#skF_8',N_500a)
| $less(N_500a,$sum(c,'#skE_2')) ),
inference(demodulation,[status(thm),theory(equality)],[c_364,c_918]) ).
tff(c_967,plain,
! [N_519a: $int,N_520a: $int] :
( ~ minsol_model_ub('#skF_7','#skF_8',N_519a)
| ~ $less(N_520a,N_519a)
| $less(N_520a,$sum(c,'#skE_2')) ),
inference(resolution,[status(thm)],[c_937,c_74]) ).
tff(c_971,plain,
! [N_520a: $int] :
( ~ $less(N_520a,'#skF_9')
| $less(N_520a,$sum(c,'#skE_2')) ),
inference(resolution,[status(thm)],[c_287,c_967]) ).
tff(c_973,plain,
! [N_520a: $int] :
( ~ $less(N_520a,'#skF_9')
| $less(N_520a,$sum(c,'#skE_2')) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_971]) ).
tff(c_974,plain,
$lesseq('#skF_9',$sum('#skE_2',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_973]) ).
tff(c_976,plain,
~ $less($sum(c,'#skE_2'),'#skF_9'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_974]) ).
tff(c_2113,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_2106,c_1992,c_976]) ).
tff(c_2119,plain,
minsol_model_max('#skF_7','#skE_1','#skF_9'),
inference(splitRight,[status(thm)],[c_2086]) ).
tff(c_1152,plain,
~ minsol_model_max('#skF_7','#skE_4','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_1043,c_203]) ).
tff(c_1899,plain,
~ minsol_model_max('#skF_7','#skE_1','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_1824,c_1152]) ).
tff(c_2122,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2119,c_1899]) ).
tff(c_2125,plain,
'#skF_7' = '#skE_4',
inference(splitRight,[status(thm)],[c_1026]) ).
tff(c_2126,plain,
~ $less('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_1026]) ).
tff(c_2234,plain,
~ $less('#skE_4','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_2125,c_2126]) ).
tff(c_2427,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_1000]) ).
tff(c_2554,plain,
! [N_1172a: $int,Z_1174a: $int] :
( ~ $less(N_1172a,'#skF_9')
| $less(N_1172a,$sum(c,summation(Z_1174a)))
| $less(Z_1174a,'#skE_4')
| $less(Z_1174a,'#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_2125,c_964]) ).
tff(c_2561,plain,
! [N_1172a: $int] :
( ~ $less(N_1172a,'#skF_9')
| $less(N_1172a,$sum(c,'#skE_5'))
| $less('#skE_4','#skE_4')
| $less('#skE_4','#skF_8') ),
inference(superposition,[status(thm),theory(equality)],[c_2427,c_2554]) ).
tff(c_2563,plain,
! [N_1172a: $int] :
( ~ $less(N_1172a,'#skF_9')
| $less(N_1172a,$sum(c,'#skE_5'))
| $less('#skE_4','#skF_8') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2561]) ).
tff(c_2646,plain,
! [N_1172a: $int] :
( ~ $less(N_1172a,'#skF_9')
| $less(N_1172a,$sum(c,'#skE_5')) ),
inference(negUnitSimplification,[status(thm)],[c_2234,c_2563]) ).
tff(c_2647,plain,
$lesseq('#skF_9',$sum('#skE_5',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_2646]) ).
tff(c_2649,plain,
~ $less($sum(c,'#skE_5'),'#skF_9'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2647]) ).
tff(c_2431,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_1000]) ).
tff(c_2482,plain,
( $less('#skE_5','#skE_2')
| ~ $less('#skE_4','#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_2431,c_396]) ).
tff(c_2507,plain,
~ $less('#skE_4','#skE_1'),
inference(splitLeft,[status(thm)],[c_2482]) ).
tff(c_2484,plain,
( ( '#skE_5' = '#skE_2' )
| ( '#skE_4' != '#skE_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_2431,c_361]) ).
tff(c_2503,plain,
'#skE_4' != '#skE_1',
inference(splitLeft,[status(thm)],[c_2484]) ).
tff(c_11,plain,
! [X_7a: $int,Y_8a: $int,Z_9a: $int] :
( ~ ub(X_7a,Y_8a,Z_9a)
| $lesseq(X_7a,Z_9a) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_97,plain,
! [X_7a: $int,Y_8a: $int,Z_9a: $int] :
( ~ ub(X_7a,Y_8a,Z_9a)
| ~ $less(Z_9a,X_7a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_11]) ).
tff(c_934,plain,
~ $less('#skE_1','#skF_7'),
inference(resolution,[status(thm)],[c_915,c_97]) ).
tff(c_2216,plain,
~ $less('#skE_1','#skE_4'),
inference(demodulation,[status(thm),theory(equality)],[c_2125,c_934]) ).
tff(c_2522,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_2507,c_2503,c_2216]) ).
tff(c_2525,plain,
$less('#skE_5','#skE_2'),
inference(splitRight,[status(thm)],[c_2482]) ).
tff(c_2650,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_2649,c_2525,c_362]) ).
tff(c_2654,plain,
'#skE_4' = '#skE_1',
inference(splitRight,[status(thm)],[c_2484]) ).
tff(c_2206,plain,
max('#skE_4','#skF_8') = '#skE_4',
inference(demodulation,[status(thm),theory(equality)],[c_2125,c_997]) ).
tff(c_2767,plain,
max('#skE_1','#skF_8') = '#skE_1',
inference(demodulation,[status(thm),theory(equality)],[c_2654,c_2654,c_2206]) ).
tff(c_2740,plain,
'#skF_7' = '#skE_1',
inference(demodulation,[status(thm),theory(equality)],[c_2654,c_2125]) ).
tff(c_2127,plain,
'#skF_2'('#skF_7','#skF_8','#skF_9') = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_475]) ).
tff(c_2143,plain,
( model_max('#skF_7','#skF_8','#skE_3')
| minsol_model_max('#skF_7','#skF_8','#skF_9')
| ~ model_max('#skF_7','#skF_8','#skF_9') ),
inference(superposition,[status(thm),theory(equality)],[c_2127,c_75]) ).
tff(c_2976,plain,
( model_max('#skE_1','#skF_8','#skE_3')
| minsol_model_max('#skE_1','#skF_8','#skF_9')
| ~ model_max('#skE_1','#skF_8','#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_2740,c_2740,c_2740,c_2143]) ).
tff(c_2985,plain,
~ model_max('#skE_1','#skF_8','#skF_9'),
inference(splitLeft,[status(thm)],[c_2976]) ).
tff(c_2988,plain,
$less('#skF_9',$sum(c,summation(max('#skE_1','#skF_8')))),
inference(resolution,[status(thm)],[c_91,c_2985]) ).
tff(c_2993,plain,
$less('#skF_9',$sum(c,'#skE_2')),
inference(demodulation,[status(thm),theory(equality)],[c_364,c_2767,c_2988]) ).
tff(c_2995,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_362,c_2993]) ).
tff(c_2999,plain,
( minsol_model_max('#skE_1','#skF_8','#skF_9')
| model_max('#skE_1','#skF_8','#skE_3') ),
inference(splitRight,[status(thm)],[c_2976]) ).
tff(c_3019,plain,
model_max('#skE_1','#skF_8','#skE_3'),
inference(splitLeft,[status(thm)],[c_2999]) ).
tff(c_3022,plain,
~ $less('#skE_3',$sum(c,summation(max('#skE_1','#skF_8')))),
inference(resolution,[status(thm)],[c_3019,c_95]) ).
tff(c_3031,plain,
~ $less('#skE_3',$sum(c,'#skE_2')),
inference(demodulation,[status(thm),theory(equality)],[c_364,c_2767,c_3022]) ).
tff(c_2653,plain,
'#skE_5' = '#skE_2',
inference(splitRight,[status(thm)],[c_2484]) ).
tff(c_2421,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_1000]) ).
tff(c_2428,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,'#skE_5')) ),
inference(demodulation,[status(thm),theory(equality)],[c_2421,c_1489]) ).
tff(c_2805,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,'#skE_2')) ),
inference(demodulation,[status(thm),theory(equality)],[c_2653,c_2428]) ).
tff(c_2807,plain,
$less('#skE_3','#skF_9'),
inference(negUnitSimplification,[status(thm)],[c_362,c_2805]) ).
tff(c_3038,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_3031,c_2807,c_976]) ).
tff(c_3044,plain,
minsol_model_max('#skE_1','#skF_8','#skF_9'),
inference(splitRight,[status(thm)],[c_2999]) ).
tff(c_2232,plain,
~ minsol_model_max('#skE_4','#skF_8','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_2125,c_203]) ).
tff(c_2734,plain,
~ minsol_model_max('#skE_1','#skF_8','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_2654,c_2232]) ).
tff(c_3047,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3044,c_2734]) ).
tff(c_3054,plain,
minsol_model_max('#skF_4','#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_77,plain,
! [X_19a: $int,Y_20a: $int,N_21a: $int] :
( model_max(X_19a,Y_20a,N_21a)
| ~ minsol_model_max(X_19a,Y_20a,N_21a) ),
inference(cnfTransformation,[status(thm)],[f_79]) ).
tff(c_226,plain,
! [N_153a: $int,X_155a: $int,Y_156a: $int] :
( ~ $less(N_153a,$sum(c,summation(max(X_155a,Y_156a))))
| ~ model_max(X_155a,Y_156a,N_153a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_16]) ).
tff(c_237,plain,
! [N_21a: $int,X_19a: $int,Y_20a: $int] :
( ~ $less(N_21a,$sum(c,summation(max(X_19a,Y_20a))))
| ~ minsol_model_max(X_19a,Y_20a,N_21a) ),
inference(resolution,[status(thm)],[c_77,c_226]) ).
tff(c_3071,plain,
~ $less('#skF_6',$sum(c,summation(max('#skF_4','#skF_5')))),
inference(resolution,[status(thm)],[c_3054,c_237]) ).
tff(c_3103,plain,
max('#skF_4','#skF_5') = '#skE_6',
inference(define,[status(thm),theory(equality)],[c_3071]) ).
tff(c_3135,plain,
( ( '#skF_5' = '#skE_6' )
| $less('#skF_5','#skF_4') ),
inference(superposition,[status(thm),theory(equality)],[c_99,c_3103]) ).
tff(c_3139,plain,
$less('#skF_5','#skF_4'),
inference(splitLeft,[status(thm)],[c_3135]) ).
tff(c_3126,plain,
( ( '#skF_4' = '#skE_6' )
| $less('#skF_4','#skF_5') ),
inference(superposition,[status(thm),theory(equality)],[c_3103,c_100]) ).
tff(c_3137,plain,
$less('#skF_4','#skF_5'),
inference(splitLeft,[status(thm)],[c_3126]) ).
tff(c_3140,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_3139,c_3137]) ).
tff(c_3143,plain,
'#skF_5' = '#skE_6',
inference(splitRight,[status(thm)],[c_3135]) ).
tff(c_3144,plain,
~ $less('#skF_5','#skF_4'),
inference(splitRight,[status(thm)],[c_3135]) ).
tff(c_3181,plain,
~ $less('#skE_6','#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_3143,c_3144]) ).
tff(c_3090,plain,
max('#skF_4','#skF_5') = '#skE_6',
inference(define,[status(thm),theory(equality)],[c_3071]) ).
tff(c_3089,plain,
~ $less('#skF_6',$sum(c,summation(max('#skF_4','#skF_5')))),
inference(resolution,[status(thm)],[c_3054,c_237]) ).
tff(c_3100,plain,
~ $less('#skF_6',$sum(c,summation('#skE_6'))),
inference(demodulation,[status(thm),theory(equality)],[c_3090,c_3089]) ).
tff(c_3265,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_3100]) ).
tff(c_3264,plain,
~ $less('#skF_6',$sum(c,summation('#skE_6'))),
inference(demodulation,[status(thm),theory(equality)],[c_3090,c_3089]) ).
tff(c_3272,plain,
~ $less('#skF_6',$sum(c,'#skE_7')),
inference(demodulation,[status(thm),theory(equality)],[c_3265,c_3264]) ).
tff(c_3271,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_3100]) ).
tff(c_259,plain,
! [X_7a: $int,Y_8a: $int,N_180a: $int,Z_9a: $int] :
( model_ub(X_7a,Y_8a,N_180a)
| $less(N_180a,$sum(c,summation(Z_9a)))
| $less(Z_9a,X_7a)
| $less(Z_9a,Y_8a) ),
inference(resolution,[status(thm)],[c_96,c_253]) ).
tff(c_43,plain,
! [N_27a: $int,X_25a: $int,Y_26a: $int] :
( ~ $lesseq(N_27a,'#skF_3'(X_25a,Y_26a,N_27a))
| minsol_model_ub(X_25a,Y_26a,N_27a)
| ~ model_ub(X_25a,Y_26a,N_27a) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_72,plain,
! [X_25a: $int,Y_26a: $int,N_27a: $int] :
( $less('#skF_3'(X_25a,Y_26a,N_27a),N_27a)
| minsol_model_ub(X_25a,Y_26a,N_27a)
| ~ model_ub(X_25a,Y_26a,N_27a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_43]) ).
tff(c_3441,plain,
! [X_1523a: $int,Y_1525a: $int,N_1527a: $int,Z_1524a: $int] :
( $less('#skF_3'(X_1523a,Y_1525a,N_1527a),N_1527a)
| minsol_model_ub(X_1523a,Y_1525a,N_1527a)
| $less(N_1527a,$sum(c,summation(Z_1524a)))
| $less(Z_1524a,X_1523a)
| $less(Z_1524a,Y_1525a) ),
inference(resolution,[status(thm)],[c_265,c_72]) ).
tff(c_62,plain,
( ~ minsol_model_ub('#skF_4','#skF_5','#skF_6')
| minsol_model_ub('#skF_7','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_164,plain,
~ minsol_model_ub('#skF_4','#skF_5','#skF_6'),
inference(splitLeft,[status(thm)],[c_62]) ).
tff(c_3179,plain,
~ minsol_model_ub('#skF_4','#skE_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_3143,c_164]) ).
tff(c_3458,plain,
! [Z_1524a: $int] :
( $less('#skF_3'('#skF_4','#skE_6','#skF_6'),'#skF_6')
| $less('#skF_6',$sum(c,summation(Z_1524a)))
| $less(Z_1524a,'#skF_4')
| $less(Z_1524a,'#skE_6') ),
inference(resolution,[status(thm)],[c_3441,c_3179]) ).
tff(c_3997,plain,
'#skF_3'('#skF_4','#skE_6','#skF_6') = '#skE_8',
inference(define,[status(thm),theory(equality)],[c_3458]) ).
tff(c_71,plain,
! [X_25a: $int,Y_26a: $int,N_27a: $int] :
( model_ub(X_25a,Y_26a,'#skF_3'(X_25a,Y_26a,N_27a))
| minsol_model_ub(X_25a,Y_26a,N_27a)
| ~ model_ub(X_25a,Y_26a,N_27a) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_4013,plain,
( model_ub('#skF_4','#skE_6','#skE_8')
| minsol_model_ub('#skF_4','#skE_6','#skF_6')
| ~ model_ub('#skF_4','#skE_6','#skF_6') ),
inference(superposition,[status(thm),theory(equality)],[c_3997,c_71]) ).
tff(c_4106,plain,
~ model_ub('#skF_4','#skE_6','#skF_6'),
inference(splitLeft,[status(thm)],[c_4013]) ).
tff(c_4119,plain,
! [Z_1800a: $int] :
( $less('#skF_6',$sum(c,summation(Z_1800a)))
| $less(Z_1800a,'#skF_4')
| $less(Z_1800a,'#skE_6') ),
inference(resolution,[status(thm)],[c_259,c_4106]) ).
tff(c_4129,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_4')
| $less('#skE_6','#skE_6') ),
inference(superposition,[status(thm),theory(equality)],[c_3271,c_4119]) ).
tff(c_4131,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_4') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_4129]) ).
tff(c_4132,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3181,c_3272,c_4131]) ).
tff(c_4136,plain,
( minsol_model_ub('#skF_4','#skE_6','#skF_6')
| model_ub('#skF_4','#skE_6','#skE_8') ),
inference(splitRight,[status(thm)],[c_4013]) ).
tff(c_4144,plain,
model_ub('#skF_4','#skE_6','#skE_8'),
inference(splitLeft,[status(thm)],[c_4136]) ).
tff(c_4145,plain,
model_ub('#skF_4','#skE_6','#skE_8'),
inference(splitLeft,[status(thm)],[c_4136]) ).
tff(c_83,plain,
! [N_15a: $int,X_13a: $int,Y_14a: $int] :
( ~ $less(N_15a,$sum(c,summation('#skF_1'(X_13a,Y_14a,N_15a))))
| ~ model_ub(X_13a,Y_14a,N_15a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_25]) ).
tff(c_4157,plain,
~ $less('#skE_8',$sum(c,summation('#skF_1'('#skF_4','#skE_6','#skE_8')))),
inference(resolution,[status(thm)],[c_4145,c_83]) ).
tff(c_4188,plain,
'#skF_1'('#skF_4','#skE_6','#skE_8') = '#skE_9',
inference(define,[status(thm),theory(equality)],[c_4157]) ).
tff(c_4199,plain,
( ub('#skF_4','#skE_6','#skE_9')
| ~ model_ub('#skF_4','#skE_6','#skE_8') ),
inference(superposition,[status(thm),theory(equality)],[c_4188,c_79]) ).
tff(c_4221,plain,
ub('#skF_4','#skE_6','#skE_9'),
inference(demodulation,[status(thm),theory(equality)],[c_4144,c_4199]) ).
tff(c_4235,plain,
~ $less('#skE_9','#skE_6'),
inference(resolution,[status(thm)],[c_4221,c_98]) ).
tff(c_4175,plain,
'#skF_1'('#skF_4','#skE_6','#skE_8') = '#skE_9',
inference(define,[status(thm),theory(equality)],[c_4157]) ).
tff(c_4174,plain,
~ $less('#skE_8',$sum(c,summation('#skF_1'('#skF_4','#skE_6','#skE_8')))),
inference(resolution,[status(thm)],[c_4145,c_83]) ).
tff(c_4185,plain,
~ $less('#skE_8',$sum(c,summation('#skE_9'))),
inference(demodulation,[status(thm),theory(equality)],[c_4175,c_4174]) ).
tff(c_4251,plain,
summation('#skE_9') = '#skE_10',
inference(define,[status(thm),theory(equality)],[c_4185]) ).
tff(c_3290,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_3100]) ).
tff(c_3327,plain,
! [Y_2a: $int] :
( ~ $less(summation(Y_2a),'#skE_7')
| $less(Y_2a,'#skE_6') ),
inference(superposition,[status(thm),theory(equality)],[c_3290,c_102]) ).
tff(c_4324,plain,
( ~ $less('#skE_10','#skE_7')
| $less('#skE_9','#skE_6') ),
inference(superposition,[status(thm),theory(equality)],[c_4251,c_3327]) ).
tff(c_4359,plain,
~ $less('#skE_10','#skE_7'),
inference(negUnitSimplification,[status(thm)],[c_4235,c_4324]) ).
tff(c_4241,plain,
summation('#skE_9') = '#skE_10',
inference(define,[status(thm),theory(equality)],[c_4185]) ).
tff(c_4240,plain,
~ $less('#skE_8',$sum(c,summation('#skE_9'))),
inference(demodulation,[status(thm),theory(equality)],[c_4175,c_4174]) ).
tff(c_4248,plain,
~ $less('#skE_8',$sum(c,'#skE_10')),
inference(demodulation,[status(thm),theory(equality)],[c_4241,c_4240]) ).
tff(c_3979,plain,
'#skF_3'('#skF_4','#skE_6','#skF_6') = '#skE_8',
inference(define,[status(thm),theory(equality)],[c_3458]) ).
tff(c_3933,plain,
! [Z_1524a: $int] :
( $less('#skF_3'('#skF_4','#skE_6','#skF_6'),'#skF_6')
| $less('#skF_6',$sum(c,summation(Z_1524a)))
| $less(Z_1524a,'#skF_4')
| $less(Z_1524a,'#skE_6') ),
inference(resolution,[status(thm)],[c_3441,c_3179]) ).
tff(c_3989,plain,
! [Z_1524a: $int] :
( $less('#skE_8','#skF_6')
| $less('#skF_6',$sum(c,summation(Z_1524a)))
| $less(Z_1524a,'#skF_4')
| $less(Z_1524a,'#skE_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_3979,c_3933]) ).
tff(c_4073,plain,
$less('#skE_8','#skF_6'),
inference(splitLeft,[status(thm)],[c_3989]) ).
tff(c_3097,plain,
max('#skF_4','#skF_5') = '#skE_6',
inference(define,[status(thm),theory(equality)],[c_3071]) ).
tff(c_3212,plain,
max('#skF_4','#skE_6') = '#skE_6',
inference(demodulation,[status(thm),theory(equality)],[c_3143,c_3097]) ).
tff(c_29,plain,
! [X_19a: $int,Y_20a: $int,Z_24a: $int,N_21a: $int] :
( ~ model_max(X_19a,Y_20a,Z_24a)
| ~ minsol_model_max(X_19a,Y_20a,N_21a)
| $lesseq(N_21a,Z_24a) ),
inference(cnfTransformation,[status(thm)],[f_79]) ).
tff(c_78,plain,
! [X_19a: $int,Y_20a: $int,Z_24a: $int,N_21a: $int] :
( ~ model_max(X_19a,Y_20a,Z_24a)
| ~ minsol_model_max(X_19a,Y_20a,N_21a)
| ~ $less(Z_24a,N_21a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_29]) ).
tff(c_225,plain,
! [X_147a: $int,Y_148a: $int,N_21a: $int,N_149a: $int] :
( ~ minsol_model_max(X_147a,Y_148a,N_21a)
| ~ $less(N_149a,N_21a)
| $less(N_149a,$sum(c,summation(max(X_147a,Y_148a)))) ),
inference(resolution,[status(thm)],[c_213,c_78]) ).
tff(c_3068,plain,
! [N_149a: $int] :
( ~ $less(N_149a,'#skF_6')
| $less(N_149a,$sum(c,summation(max('#skF_4','#skF_5')))) ),
inference(resolution,[status(thm)],[c_3054,c_225]) ).
tff(c_3278,plain,
! [N_149a: $int] :
( ~ $less(N_149a,'#skF_6')
| $less(N_149a,$sum(c,summation('#skE_6'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_3212,c_3143,c_3068]) ).
tff(c_3280,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_3278]) ).
tff(c_3279,plain,
! [N_149a: $int] :
( ~ $less(N_149a,'#skF_6')
| $less(N_149a,$sum(c,summation('#skE_6'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_3212,c_3143,c_3068]) ).
tff(c_3287,plain,
! [N_149a: $int] :
( ~ $less(N_149a,'#skF_6')
| $less(N_149a,$sum(c,'#skE_7')) ),
inference(demodulation,[status(thm),theory(equality)],[c_3280,c_3279]) ).
tff(c_3333,plain,
$lesseq('#skF_6',$sum('#skE_7',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_3287]) ).
tff(c_3335,plain,
~ $less($sum(c,'#skE_7'),'#skF_6'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_3333]) ).
tff(c_4360,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_4359,c_4248,c_4073,c_3335]) ).
tff(c_4366,plain,
minsol_model_ub('#skF_4','#skE_6','#skF_6'),
inference(splitRight,[status(thm)],[c_4136]) ).
tff(c_4369,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4366,c_3179]) ).
tff(c_4400,plain,
! [Z_1910a: $int] :
( $less('#skF_6',$sum(c,summation(Z_1910a)))
| $less(Z_1910a,'#skF_4')
| $less(Z_1910a,'#skE_6') ),
inference(splitRight,[status(thm)],[c_3989]) ).
tff(c_4410,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_4')
| $less('#skE_6','#skE_6') ),
inference(superposition,[status(thm),theory(equality)],[c_3271,c_4400]) ).
tff(c_4412,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_4') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_4410]) ).
tff(c_4414,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3181,c_3272,c_4412]) ).
tff(c_4417,plain,
'#skF_4' = '#skE_6',
inference(splitRight,[status(thm)],[c_3126]) ).
tff(c_4418,plain,
~ $less('#skF_4','#skF_5'),
inference(splitRight,[status(thm)],[c_3126]) ).
tff(c_4455,plain,
~ $less('#skE_6','#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_4417,c_4418]) ).
tff(c_4465,plain,
max('#skE_6','#skF_5') = '#skE_6',
inference(demodulation,[status(thm),theory(equality)],[c_4417,c_3097]) ).
tff(c_3051,plain,
minsol_model_max('#skF_4','#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_58]) ).
tff(c_4505,plain,
minsol_model_max('#skE_6','#skF_5','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_4417,c_3051]) ).
tff(c_4511,plain,
~ $less('#skF_6',$sum(c,summation(max('#skE_6','#skF_5')))),
inference(resolution,[status(thm)],[c_4505,c_237]) ).
tff(c_4528,plain,
~ $less('#skF_6',$sum(c,summation('#skE_6'))),
inference(demodulation,[status(thm),theory(equality)],[c_4465,c_4511]) ).
tff(c_4549,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_4528]) ).
tff(c_4548,plain,
~ $less('#skF_6',$sum(c,summation('#skE_6'))),
inference(demodulation,[status(thm),theory(equality)],[c_4465,c_4511]) ).
tff(c_4556,plain,
~ $less('#skF_6',$sum(c,'#skE_7')),
inference(demodulation,[status(thm),theory(equality)],[c_4549,c_4548]) ).
tff(c_4555,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_4528]) ).
tff(c_4707,plain,
! [X_2020a: $int,Y_2022a: $int,N_2024a: $int,Z_2021a: $int] :
( $less('#skF_3'(X_2020a,Y_2022a,N_2024a),N_2024a)
| minsol_model_ub(X_2020a,Y_2022a,N_2024a)
| $less(N_2024a,$sum(c,summation(Z_2021a)))
| $less(Z_2021a,X_2020a)
| $less(Z_2021a,Y_2022a) ),
inference(resolution,[status(thm)],[c_265,c_72]) ).
tff(c_4453,plain,
~ minsol_model_ub('#skE_6','#skF_5','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_4417,c_164]) ).
tff(c_4724,plain,
! [Z_2021a: $int] :
( $less('#skF_3'('#skE_6','#skF_5','#skF_6'),'#skF_6')
| $less('#skF_6',$sum(c,summation(Z_2021a)))
| $less(Z_2021a,'#skE_6')
| $less(Z_2021a,'#skF_5') ),
inference(resolution,[status(thm)],[c_4707,c_4453]) ).
tff(c_5171,plain,
'#skF_3'('#skE_6','#skF_5','#skF_6') = '#skE_11',
inference(define,[status(thm),theory(equality)],[c_4724]) ).
tff(c_5187,plain,
( model_ub('#skE_6','#skF_5','#skE_11')
| minsol_model_ub('#skE_6','#skF_5','#skF_6')
| ~ model_ub('#skE_6','#skF_5','#skF_6') ),
inference(superposition,[status(thm),theory(equality)],[c_5171,c_71]) ).
tff(c_5213,plain,
~ model_ub('#skE_6','#skF_5','#skF_6'),
inference(splitLeft,[status(thm)],[c_5187]) ).
tff(c_5226,plain,
! [Z_2180a: $int] :
( $less('#skF_6',$sum(c,summation(Z_2180a)))
| $less(Z_2180a,'#skE_6')
| $less(Z_2180a,'#skF_5') ),
inference(resolution,[status(thm)],[c_259,c_5213]) ).
tff(c_5236,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skE_6')
| $less('#skE_6','#skF_5') ),
inference(superposition,[status(thm),theory(equality)],[c_4555,c_5226]) ).
tff(c_5238,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_5') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_5236]) ).
tff(c_5239,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4455,c_4556,c_5238]) ).
tff(c_5243,plain,
( minsol_model_ub('#skE_6','#skF_5','#skF_6')
| model_ub('#skE_6','#skF_5','#skE_11') ),
inference(splitRight,[status(thm)],[c_5187]) ).
tff(c_5269,plain,
model_ub('#skE_6','#skF_5','#skE_11'),
inference(splitLeft,[status(thm)],[c_5243]) ).
tff(c_5270,plain,
model_ub('#skE_6','#skF_5','#skE_11'),
inference(splitLeft,[status(thm)],[c_5243]) ).
tff(c_5282,plain,
~ $less('#skE_11',$sum(c,summation('#skF_1'('#skE_6','#skF_5','#skE_11')))),
inference(resolution,[status(thm)],[c_5270,c_83]) ).
tff(c_5313,plain,
'#skF_1'('#skE_6','#skF_5','#skE_11') = '#skE_12',
inference(define,[status(thm),theory(equality)],[c_5282]) ).
tff(c_5324,plain,
( ub('#skE_6','#skF_5','#skE_12')
| ~ model_ub('#skE_6','#skF_5','#skE_11') ),
inference(superposition,[status(thm),theory(equality)],[c_5313,c_79]) ).
tff(c_5346,plain,
ub('#skE_6','#skF_5','#skE_12'),
inference(demodulation,[status(thm),theory(equality)],[c_5269,c_5324]) ).
tff(c_5362,plain,
~ $less('#skE_12','#skE_6'),
inference(resolution,[status(thm)],[c_5346,c_97]) ).
tff(c_5300,plain,
'#skF_1'('#skE_6','#skF_5','#skE_11') = '#skE_12',
inference(define,[status(thm),theory(equality)],[c_5282]) ).
tff(c_5299,plain,
~ $less('#skE_11',$sum(c,summation('#skF_1'('#skE_6','#skF_5','#skE_11')))),
inference(resolution,[status(thm)],[c_5270,c_83]) ).
tff(c_5310,plain,
~ $less('#skE_11',$sum(c,summation('#skE_12'))),
inference(demodulation,[status(thm),theory(equality)],[c_5300,c_5299]) ).
tff(c_5428,plain,
summation('#skE_12') = '#skE_14',
inference(define,[status(thm),theory(equality)],[c_5310]) ).
tff(c_4559,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_4528]) ).
tff(c_4596,plain,
! [Y_2a: $int] :
( ~ $less(summation(Y_2a),'#skE_7')
| $less(Y_2a,'#skE_6') ),
inference(superposition,[status(thm),theory(equality)],[c_4559,c_102]) ).
tff(c_5503,plain,
( ~ $less('#skE_14','#skE_7')
| $less('#skE_12','#skE_6') ),
inference(superposition,[status(thm),theory(equality)],[c_5428,c_4596]) ).
tff(c_5565,plain,
~ $less('#skE_14','#skE_7'),
inference(negUnitSimplification,[status(thm)],[c_5362,c_5503]) ).
tff(c_5418,plain,
summation('#skE_12') = '#skE_14',
inference(define,[status(thm),theory(equality)],[c_5310]) ).
tff(c_5417,plain,
~ $less('#skE_11',$sum(c,summation('#skE_12'))),
inference(demodulation,[status(thm),theory(equality)],[c_5300,c_5299]) ).
tff(c_5425,plain,
~ $less('#skE_11',$sum(c,'#skE_14')),
inference(demodulation,[status(thm),theory(equality)],[c_5418,c_5417]) ).
tff(c_5158,plain,
'#skF_3'('#skE_6','#skF_5','#skF_6') = '#skE_11',
inference(define,[status(thm),theory(equality)],[c_4724]) ).
tff(c_5157,plain,
! [Z_2021a: $int] :
( $less('#skF_3'('#skE_6','#skF_5','#skF_6'),'#skF_6')
| $less('#skF_6',$sum(c,summation(Z_2021a)))
| $less(Z_2021a,'#skE_6')
| $less(Z_2021a,'#skF_5') ),
inference(resolution,[status(thm)],[c_4707,c_4453]) ).
tff(c_5168,plain,
! [Z_2021a: $int] :
( $less('#skE_11','#skF_6')
| $less('#skF_6',$sum(c,summation(Z_2021a)))
| $less(Z_2021a,'#skE_6')
| $less(Z_2021a,'#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_5158,c_5157]) ).
tff(c_5194,plain,
$less('#skE_11','#skF_6'),
inference(splitLeft,[status(thm)],[c_5168]) ).
tff(c_4558,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_4528]) ).
tff(c_4619,plain,
! [N_149a: $int] :
( ~ $less(N_149a,'#skF_6')
| $less(N_149a,$sum(c,'#skE_7')) ),
inference(demodulation,[status(thm),theory(equality)],[c_4558,c_4465,c_4417,c_3068]) ).
tff(c_4620,plain,
$lesseq('#skF_6',$sum('#skE_7',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_4619]) ).
tff(c_4622,plain,
~ $less($sum(c,'#skE_7'),'#skF_6'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_4620]) ).
tff(c_5566,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_5565,c_5425,c_5194,c_4622]) ).
tff(c_5572,plain,
minsol_model_ub('#skE_6','#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_5243]) ).
tff(c_5575,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5572,c_4453]) ).
tff(c_5584,plain,
! [Z_2302a: $int] :
( $less('#skF_6',$sum(c,summation(Z_2302a)))
| $less(Z_2302a,'#skE_6')
| $less(Z_2302a,'#skF_5') ),
inference(splitRight,[status(thm)],[c_5168]) ).
tff(c_5594,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skE_6')
| $less('#skE_6','#skF_5') ),
inference(superposition,[status(thm),theory(equality)],[c_4555,c_5584]) ).
tff(c_5596,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_5') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_5594]) ).
tff(c_5597,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4455,c_4556,c_5596]) ).
tff(c_5601,plain,
minsol_model_max('#skF_4','#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_5638,plain,
! [N_2323a: $int,X_2325a: $int,Y_2326a: $int] :
( ~ $less(N_2323a,$sum(c,summation(max(X_2325a,Y_2326a))))
| ~ model_max(X_2325a,Y_2326a,N_2323a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_16]) ).
tff(c_5652,plain,
! [N_2328a: $int,X_2330a: $int,Y_2331a: $int] :
( ~ $less(N_2328a,$sum(c,summation(max(X_2330a,Y_2331a))))
| ~ minsol_model_max(X_2330a,Y_2331a,N_2328a) ),
inference(resolution,[status(thm)],[c_77,c_5638]) ).
tff(c_5658,plain,
~ $less('#skF_6',$sum(c,summation(max('#skF_4','#skF_5')))),
inference(resolution,[status(thm)],[c_5601,c_5652]) ).
tff(c_5697,plain,
max('#skF_4','#skF_5') = '#skE_6',
inference(define,[status(thm),theory(equality)],[c_5658]) ).
tff(c_5729,plain,
( ( '#skF_5' = '#skE_6' )
| $less('#skF_5','#skF_4') ),
inference(superposition,[status(thm),theory(equality)],[c_99,c_5697]) ).
tff(c_5735,plain,
$less('#skF_5','#skF_4'),
inference(splitLeft,[status(thm)],[c_5729]) ).
tff(c_5720,plain,
( ( '#skF_4' = '#skE_6' )
| $less('#skF_4','#skF_5') ),
inference(superposition,[status(thm),theory(equality)],[c_5697,c_100]) ).
tff(c_5731,plain,
$less('#skF_4','#skF_5'),
inference(splitLeft,[status(thm)],[c_5720]) ).
tff(c_5736,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_5735,c_5731]) ).
tff(c_5739,plain,
'#skF_5' = '#skE_6',
inference(splitRight,[status(thm)],[c_5729]) ).
tff(c_5740,plain,
~ $less('#skF_5','#skF_4'),
inference(splitRight,[status(thm)],[c_5729]) ).
tff(c_5777,plain,
~ $less('#skE_6','#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_5739,c_5740]) ).
tff(c_5691,plain,
max('#skF_4','#skF_5') = '#skE_6',
inference(define,[status(thm),theory(equality)],[c_5658]) ).
tff(c_5781,plain,
max('#skF_4','#skE_6') = '#skE_6',
inference(demodulation,[status(thm),theory(equality)],[c_5739,c_5691]) ).
tff(c_5824,plain,
minsol_model_max('#skF_4','#skE_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_5739,c_5601]) ).
tff(c_5649,plain,
! [N_21a: $int,X_19a: $int,Y_20a: $int] :
( ~ $less(N_21a,$sum(c,summation(max(X_19a,Y_20a))))
| ~ minsol_model_max(X_19a,Y_20a,N_21a) ),
inference(resolution,[status(thm)],[c_77,c_5638]) ).
tff(c_5827,plain,
~ $less('#skF_6',$sum(c,summation(max('#skF_4','#skE_6')))),
inference(resolution,[status(thm)],[c_5824,c_5649]) ).
tff(c_5835,plain,
~ $less('#skF_6',$sum(c,summation('#skE_6'))),
inference(demodulation,[status(thm),theory(equality)],[c_5781,c_5827]) ).
tff(c_5851,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_5835]) ).
tff(c_5850,plain,
~ $less('#skF_6',$sum(c,summation('#skE_6'))),
inference(demodulation,[status(thm),theory(equality)],[c_5781,c_5827]) ).
tff(c_5858,plain,
~ $less('#skF_6',$sum(c,'#skE_7')),
inference(demodulation,[status(thm),theory(equality)],[c_5851,c_5850]) ).
tff(c_5857,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_5835]) ).
tff(c_5675,plain,
! [X_2354a: $int,Y_2358a: $int,N_2357a: $int,Z_2356a: $int] :
( model_ub(X_2354a,Y_2358a,N_2357a)
| $less(N_2357a,$sum(c,summation(Z_2356a)))
| ~ ub(X_2354a,Y_2358a,Z_2356a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_22]) ).
tff(c_5681,plain,
! [X_7a: $int,Y_8a: $int,N_2357a: $int,Z_9a: $int] :
( model_ub(X_7a,Y_8a,N_2357a)
| $less(N_2357a,$sum(c,summation(Z_9a)))
| $less(Z_9a,X_7a)
| $less(Z_9a,Y_8a) ),
inference(resolution,[status(thm)],[c_96,c_5675]) ).
tff(c_5966,plain,
! [X_2447a: $int,Y_2448a: $int,N_2446a: $int,Z_2449a: $int] :
( model_ub(X_2447a,Y_2448a,N_2446a)
| $less(N_2446a,$sum(c,summation(Z_2449a)))
| $less(Z_2449a,X_2447a)
| $less(Z_2449a,Y_2448a) ),
inference(resolution,[status(thm)],[c_96,c_5675]) ).
tff(c_6033,plain,
! [X_2483a: $int,Y_2484a: $int,N_2481a: $int,Z_2482a: $int] :
( $less('#skF_3'(X_2483a,Y_2484a,N_2481a),N_2481a)
| minsol_model_ub(X_2483a,Y_2484a,N_2481a)
| $less(N_2481a,$sum(c,summation(Z_2482a)))
| $less(Z_2482a,X_2483a)
| $less(Z_2482a,Y_2484a) ),
inference(resolution,[status(thm)],[c_5966,c_72]) ).
tff(c_5775,plain,
~ minsol_model_ub('#skF_4','#skE_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_5739,c_164]) ).
tff(c_6050,plain,
! [Z_2482a: $int] :
( $less('#skF_3'('#skF_4','#skE_6','#skF_6'),'#skF_6')
| $less('#skF_6',$sum(c,summation(Z_2482a)))
| $less(Z_2482a,'#skF_4')
| $less(Z_2482a,'#skE_6') ),
inference(resolution,[status(thm)],[c_6033,c_5775]) ).
tff(c_6087,plain,
'#skF_3'('#skF_4','#skE_6','#skF_6') = '#skE_8',
inference(define,[status(thm),theory(equality)],[c_6050]) ).
tff(c_6103,plain,
( model_ub('#skF_4','#skE_6','#skE_8')
| minsol_model_ub('#skF_4','#skE_6','#skF_6')
| ~ model_ub('#skF_4','#skE_6','#skF_6') ),
inference(superposition,[status(thm),theory(equality)],[c_6087,c_71]) ).
tff(c_6187,plain,
~ model_ub('#skF_4','#skE_6','#skF_6'),
inference(splitLeft,[status(thm)],[c_6103]) ).
tff(c_6200,plain,
! [Z_2574a: $int] :
( $less('#skF_6',$sum(c,summation(Z_2574a)))
| $less(Z_2574a,'#skF_4')
| $less(Z_2574a,'#skE_6') ),
inference(resolution,[status(thm)],[c_5681,c_6187]) ).
tff(c_6204,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_4')
| $less('#skE_6','#skE_6') ),
inference(superposition,[status(thm),theory(equality)],[c_5857,c_6200]) ).
tff(c_6206,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_4') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_6204]) ).
tff(c_6207,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5777,c_5858,c_6206]) ).
tff(c_6211,plain,
( minsol_model_ub('#skF_4','#skE_6','#skF_6')
| model_ub('#skF_4','#skE_6','#skE_8') ),
inference(splitRight,[status(thm)],[c_6103]) ).
tff(c_6220,plain,
model_ub('#skF_4','#skE_6','#skE_8'),
inference(splitLeft,[status(thm)],[c_6211]) ).
tff(c_6232,plain,
~ $less('#skE_8',$sum(c,summation('#skF_1'('#skF_4','#skE_6','#skE_8')))),
inference(resolution,[status(thm)],[c_6220,c_83]) ).
tff(c_6250,plain,
'#skF_1'('#skF_4','#skE_6','#skE_8') = '#skE_9',
inference(define,[status(thm),theory(equality)],[c_6232]) ).
tff(c_6249,plain,
~ $less('#skE_8',$sum(c,summation('#skF_1'('#skF_4','#skE_6','#skE_8')))),
inference(resolution,[status(thm)],[c_6220,c_83]) ).
tff(c_6260,plain,
~ $less('#skE_8',$sum(c,summation('#skE_9'))),
inference(demodulation,[status(thm),theory(equality)],[c_6250,c_6249]) ).
tff(c_6325,plain,
summation('#skE_9') = '#skE_10',
inference(define,[status(thm),theory(equality)],[c_6260]) ).
tff(c_5861,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_5835]) ).
tff(c_5895,plain,
! [X_1a: $int] :
( ~ $less('#skE_7',summation(X_1a))
| $less('#skE_6',X_1a) ),
inference(superposition,[status(thm),theory(equality)],[c_5861,c_102]) ).
tff(c_6376,plain,
( ~ $less('#skE_7','#skE_10')
| $less('#skE_6','#skE_9') ),
inference(superposition,[status(thm),theory(equality)],[c_6325,c_5895]) ).
tff(c_6399,plain,
~ $less('#skE_7','#skE_10'),
inference(splitLeft,[status(thm)],[c_6376]) ).
tff(c_5889,plain,
! [X_1a: $int] :
( $less('#skE_7',summation(X_1a))
| ~ $less('#skE_6',X_1a) ),
inference(superposition,[status(thm),theory(equality)],[c_5861,c_101]) ).
tff(c_6372,plain,
( $less('#skE_7','#skE_10')
| ~ $less('#skE_6','#skE_9') ),
inference(superposition,[status(thm),theory(equality)],[c_6325,c_5889]) ).
tff(c_6420,plain,
~ $less('#skE_6','#skE_9'),
inference(negUnitSimplification,[status(thm)],[c_6399,c_6372]) ).
tff(c_6378,plain,
( ( '#skE_7' = '#skE_10' )
| ( '#skE_9' != '#skE_6' ) ),
inference(superposition,[status(thm),theory(equality)],[c_6325,c_5857]) ).
tff(c_6397,plain,
'#skE_9' != '#skE_6',
inference(splitLeft,[status(thm)],[c_6378]) ).
tff(c_6219,plain,
model_ub('#skF_4','#skE_6','#skE_8'),
inference(splitLeft,[status(thm)],[c_6211]) ).
tff(c_6263,plain,
'#skF_1'('#skF_4','#skE_6','#skE_8') = '#skE_9',
inference(define,[status(thm),theory(equality)],[c_6232]) ).
tff(c_6274,plain,
( ub('#skF_4','#skE_6','#skE_9')
| ~ model_ub('#skF_4','#skE_6','#skE_8') ),
inference(superposition,[status(thm),theory(equality)],[c_6263,c_79]) ).
tff(c_6296,plain,
ub('#skF_4','#skE_6','#skE_9'),
inference(demodulation,[status(thm),theory(equality)],[c_6219,c_6274]) ).
tff(c_6310,plain,
~ $less('#skE_9','#skE_6'),
inference(resolution,[status(thm)],[c_6296,c_98]) ).
tff(c_6421,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_6420,c_6397,c_6310]) ).
tff(c_6425,plain,
$less('#skE_7','#skE_10'),
inference(splitRight,[status(thm)],[c_6376]) ).
tff(c_6315,plain,
summation('#skE_9') = '#skE_10',
inference(define,[status(thm),theory(equality)],[c_6260]) ).
tff(c_6314,plain,
~ $less('#skE_8',$sum(c,summation('#skE_9'))),
inference(demodulation,[status(thm),theory(equality)],[c_6250,c_6249]) ).
tff(c_6322,plain,
~ $less('#skE_8',$sum(c,'#skE_10')),
inference(demodulation,[status(thm),theory(equality)],[c_6315,c_6314]) ).
tff(c_6074,plain,
'#skF_3'('#skF_4','#skE_6','#skF_6') = '#skE_8',
inference(define,[status(thm),theory(equality)],[c_6050]) ).
tff(c_6073,plain,
! [Z_2482a: $int] :
( $less('#skF_3'('#skF_4','#skE_6','#skF_6'),'#skF_6')
| $less('#skF_6',$sum(c,summation(Z_2482a)))
| $less(Z_2482a,'#skF_4')
| $less(Z_2482a,'#skE_6') ),
inference(resolution,[status(thm)],[c_6033,c_5775]) ).
tff(c_6084,plain,
! [Z_2482a: $int] :
( $less('#skE_8','#skF_6')
| $less('#skF_6',$sum(c,summation(Z_2482a)))
| $less(Z_2482a,'#skF_4')
| $less(Z_2482a,'#skE_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_6074,c_6073]) ).
tff(c_6110,plain,
$less('#skE_8','#skF_6'),
inference(splitLeft,[status(thm)],[c_6084]) ).
tff(c_5860,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_5835]) ).
tff(c_5772,plain,
minsol_model_max('#skF_4','#skE_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_5739,c_5601]) ).
tff(c_5625,plain,
! [X_2317a: $int,Y_2318a: $int,N_2319a: $int] :
( model_max(X_2317a,Y_2318a,N_2319a)
| $less(N_2319a,$sum(c,summation(max(X_2317a,Y_2318a)))) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_19]) ).
tff(c_5954,plain,
! [X_2440a: $int,Y_2443a: $int,N_2444a: $int,N_2442a: $int] :
( ~ minsol_model_max(X_2440a,Y_2443a,N_2444a)
| ~ $less(N_2442a,N_2444a)
| $less(N_2442a,$sum(c,summation(max(X_2440a,Y_2443a)))) ),
inference(resolution,[status(thm)],[c_5625,c_78]) ).
tff(c_5957,plain,
! [N_2442a: $int] :
( ~ $less(N_2442a,'#skF_6')
| $less(N_2442a,$sum(c,summation(max('#skF_4','#skE_6')))) ),
inference(resolution,[status(thm)],[c_5772,c_5954]) ).
tff(c_5960,plain,
! [N_2442a: $int] :
( ~ $less(N_2442a,'#skF_6')
| $less(N_2442a,$sum(c,'#skE_7')) ),
inference(demodulation,[status(thm),theory(equality)],[c_5860,c_5781,c_5957]) ).
tff(c_5961,plain,
$lesseq('#skF_6',$sum('#skE_7',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_5960]) ).
tff(c_5963,plain,
~ $less($sum(c,'#skE_7'),'#skF_6'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_5961]) ).
tff(c_6427,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_6425,c_6322,c_6110,c_5963]) ).
tff(c_6430,plain,
'#skE_7' = '#skE_10',
inference(splitRight,[status(thm)],[c_6378]) ).
tff(c_6506,plain,
! [N_2442a: $int] :
( ~ $less(N_2442a,'#skF_6')
| $less(N_2442a,$sum(c,'#skE_10')) ),
inference(demodulation,[status(thm),theory(equality)],[c_6430,c_5960]) ).
tff(c_6573,plain,
$lesseq('#skF_6',$sum('#skE_10',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_6506]) ).
tff(c_6575,plain,
~ $less($sum(c,'#skE_10'),'#skF_6'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_6573]) ).
tff(c_6576,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_6575,c_6322,c_6110]) ).
tff(c_6582,plain,
minsol_model_ub('#skF_4','#skE_6','#skF_6'),
inference(splitRight,[status(thm)],[c_6211]) ).
tff(c_6585,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6582,c_5775]) ).
tff(c_6594,plain,
! [Z_2719a: $int] :
( $less('#skF_6',$sum(c,summation(Z_2719a)))
| $less(Z_2719a,'#skF_4')
| $less(Z_2719a,'#skE_6') ),
inference(splitRight,[status(thm)],[c_6084]) ).
tff(c_6598,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_4')
| $less('#skE_6','#skE_6') ),
inference(superposition,[status(thm),theory(equality)],[c_5857,c_6594]) ).
tff(c_6600,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_4') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_6598]) ).
tff(c_6601,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5777,c_5858,c_6600]) ).
tff(c_6604,plain,
'#skF_4' = '#skE_6',
inference(splitRight,[status(thm)],[c_5720]) ).
tff(c_6605,plain,
~ $less('#skF_4','#skF_5'),
inference(splitRight,[status(thm)],[c_5720]) ).
tff(c_6649,plain,
~ $less('#skE_6','#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_6604,c_6605]) ).
tff(c_6662,plain,
max('#skE_6','#skF_5') = '#skE_6',
inference(demodulation,[status(thm),theory(equality)],[c_6604,c_5691]) ).
tff(c_6702,plain,
minsol_model_max('#skE_6','#skF_5','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_6604,c_5601]) ).
tff(c_6705,plain,
~ $less('#skF_6',$sum(c,summation(max('#skE_6','#skF_5')))),
inference(resolution,[status(thm)],[c_6702,c_5649]) ).
tff(c_6713,plain,
~ $less('#skF_6',$sum(c,summation('#skE_6'))),
inference(demodulation,[status(thm),theory(equality)],[c_6662,c_6705]) ).
tff(c_6749,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_6713]) ).
tff(c_6748,plain,
~ $less('#skF_6',$sum(c,summation('#skE_6'))),
inference(demodulation,[status(thm),theory(equality)],[c_6662,c_6705]) ).
tff(c_6756,plain,
~ $less('#skF_6',$sum(c,'#skE_7')),
inference(demodulation,[status(thm),theory(equality)],[c_6749,c_6748]) ).
tff(c_6755,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_6713]) ).
tff(c_6855,plain,
! [X_2817a: $int,Y_2818a: $int,N_2816a: $int,Z_2819a: $int] :
( model_ub(X_2817a,Y_2818a,N_2816a)
| $less(N_2816a,$sum(c,summation(Z_2819a)))
| $less(Z_2819a,X_2817a)
| $less(Z_2819a,Y_2818a) ),
inference(resolution,[status(thm)],[c_96,c_5675]) ).
tff(c_6929,plain,
! [X_2864a: $int,Y_2863a: $int,N_2862a: $int,Z_2861a: $int] :
( $less('#skF_3'(X_2864a,Y_2863a,N_2862a),N_2862a)
| minsol_model_ub(X_2864a,Y_2863a,N_2862a)
| $less(N_2862a,$sum(c,summation(Z_2861a)))
| $less(Z_2861a,X_2864a)
| $less(Z_2861a,Y_2863a) ),
inference(resolution,[status(thm)],[c_6855,c_72]) ).
tff(c_6637,plain,
~ minsol_model_ub('#skE_6','#skF_5','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_6604,c_164]) ).
tff(c_6946,plain,
! [Z_2861a: $int] :
( $less('#skF_3'('#skE_6','#skF_5','#skF_6'),'#skF_6')
| $less('#skF_6',$sum(c,summation(Z_2861a)))
| $less(Z_2861a,'#skE_6')
| $less(Z_2861a,'#skF_5') ),
inference(resolution,[status(thm)],[c_6929,c_6637]) ).
tff(c_7322,plain,
'#skF_3'('#skE_6','#skF_5','#skF_6') = '#skE_11',
inference(define,[status(thm),theory(equality)],[c_6946]) ).
tff(c_7338,plain,
( model_ub('#skE_6','#skF_5','#skE_11')
| minsol_model_ub('#skE_6','#skF_5','#skF_6')
| ~ model_ub('#skE_6','#skF_5','#skF_6') ),
inference(superposition,[status(thm),theory(equality)],[c_7322,c_71]) ).
tff(c_7675,plain,
~ model_ub('#skE_6','#skF_5','#skF_6'),
inference(splitLeft,[status(thm)],[c_7338]) ).
tff(c_7688,plain,
! [Z_3160a: $int] :
( $less('#skF_6',$sum(c,summation(Z_3160a)))
| $less(Z_3160a,'#skE_6')
| $less(Z_3160a,'#skF_5') ),
inference(resolution,[status(thm)],[c_5681,c_7675]) ).
tff(c_7697,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skE_6')
| $less('#skE_6','#skF_5') ),
inference(superposition,[status(thm),theory(equality)],[c_6755,c_7688]) ).
tff(c_7699,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_5') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_7697]) ).
tff(c_7700,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6649,c_6756,c_7699]) ).
tff(c_7704,plain,
( minsol_model_ub('#skE_6','#skF_5','#skF_6')
| model_ub('#skE_6','#skF_5','#skE_11') ),
inference(splitRight,[status(thm)],[c_7338]) ).
tff(c_7712,plain,
model_ub('#skE_6','#skF_5','#skE_11'),
inference(splitLeft,[status(thm)],[c_7704]) ).
tff(c_7713,plain,
model_ub('#skE_6','#skF_5','#skE_11'),
inference(splitLeft,[status(thm)],[c_7704]) ).
tff(c_7725,plain,
~ $less('#skE_11',$sum(c,summation('#skF_1'('#skE_6','#skF_5','#skE_11')))),
inference(resolution,[status(thm)],[c_7713,c_83]) ).
tff(c_7756,plain,
'#skF_1'('#skE_6','#skF_5','#skE_11') = '#skE_12',
inference(define,[status(thm),theory(equality)],[c_7725]) ).
tff(c_7767,plain,
( ub('#skE_6','#skF_5','#skE_12')
| ~ model_ub('#skE_6','#skF_5','#skE_11') ),
inference(superposition,[status(thm),theory(equality)],[c_7756,c_79]) ).
tff(c_7789,plain,
ub('#skE_6','#skF_5','#skE_12'),
inference(demodulation,[status(thm),theory(equality)],[c_7712,c_7767]) ).
tff(c_7805,plain,
~ $less('#skE_12','#skE_6'),
inference(resolution,[status(thm)],[c_7789,c_97]) ).
tff(c_7743,plain,
'#skF_1'('#skE_6','#skF_5','#skE_11') = '#skE_12',
inference(define,[status(thm),theory(equality)],[c_7725]) ).
tff(c_7742,plain,
~ $less('#skE_11',$sum(c,summation('#skF_1'('#skE_6','#skF_5','#skE_11')))),
inference(resolution,[status(thm)],[c_7713,c_83]) ).
tff(c_7753,plain,
~ $less('#skE_11',$sum(c,summation('#skE_12'))),
inference(demodulation,[status(thm),theory(equality)],[c_7743,c_7742]) ).
tff(c_7818,plain,
summation('#skE_12') = '#skE_14',
inference(define,[status(thm),theory(equality)],[c_7753]) ).
tff(c_6759,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_6713]) ).
tff(c_6796,plain,
! [Y_2a: $int] :
( ~ $less(summation(Y_2a),'#skE_7')
| $less(Y_2a,'#skE_6') ),
inference(superposition,[status(thm),theory(equality)],[c_6759,c_102]) ).
tff(c_7913,plain,
( ~ $less('#skE_14','#skE_7')
| $less('#skE_12','#skE_6') ),
inference(superposition,[status(thm),theory(equality)],[c_7818,c_6796]) ).
tff(c_7980,plain,
~ $less('#skE_14','#skE_7'),
inference(negUnitSimplification,[status(thm)],[c_7805,c_7913]) ).
tff(c_7808,plain,
summation('#skE_12') = '#skE_14',
inference(define,[status(thm),theory(equality)],[c_7753]) ).
tff(c_7807,plain,
~ $less('#skE_11',$sum(c,summation('#skE_12'))),
inference(demodulation,[status(thm),theory(equality)],[c_7743,c_7742]) ).
tff(c_7815,plain,
~ $less('#skE_11',$sum(c,'#skE_14')),
inference(demodulation,[status(thm),theory(equality)],[c_7808,c_7807]) ).
tff(c_7309,plain,
'#skF_3'('#skE_6','#skF_5','#skF_6') = '#skE_11',
inference(define,[status(thm),theory(equality)],[c_6946]) ).
tff(c_7308,plain,
! [Z_2861a: $int] :
( $less('#skF_3'('#skE_6','#skF_5','#skF_6'),'#skF_6')
| $less('#skF_6',$sum(c,summation(Z_2861a)))
| $less(Z_2861a,'#skE_6')
| $less(Z_2861a,'#skF_5') ),
inference(resolution,[status(thm)],[c_6929,c_6637]) ).
tff(c_7319,plain,
! [Z_2861a: $int] :
( $less('#skE_11','#skF_6')
| $less('#skF_6',$sum(c,summation(Z_2861a)))
| $less(Z_2861a,'#skE_6')
| $less(Z_2861a,'#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_7309,c_7308]) ).
tff(c_7469,plain,
$less('#skE_11','#skF_6'),
inference(splitLeft,[status(thm)],[c_7319]) ).
tff(c_6758,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_6713]) ).
tff(c_6634,plain,
minsol_model_max('#skE_6','#skF_5','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_6604,c_5601]) ).
tff(c_6725,plain,
! [X_2784a: $int,Y_2787a: $int,N_2788a: $int,N_2786a: $int] :
( ~ minsol_model_max(X_2784a,Y_2787a,N_2788a)
| ~ $less(N_2786a,N_2788a)
| $less(N_2786a,$sum(c,summation(max(X_2784a,Y_2787a)))) ),
inference(resolution,[status(thm)],[c_5625,c_78]) ).
tff(c_6728,plain,
! [N_2786a: $int] :
( ~ $less(N_2786a,'#skF_6')
| $less(N_2786a,$sum(c,summation(max('#skE_6','#skF_5')))) ),
inference(resolution,[status(thm)],[c_6634,c_6725]) ).
tff(c_6734,plain,
! [N_2786a: $int] :
( ~ $less(N_2786a,'#skF_6')
| $less(N_2786a,$sum(c,summation('#skE_6'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_6662,c_6728]) ).
tff(c_6851,plain,
! [N_2786a: $int] :
( ~ $less(N_2786a,'#skF_6')
| $less(N_2786a,$sum(c,'#skE_7')) ),
inference(demodulation,[status(thm),theory(equality)],[c_6758,c_6734]) ).
tff(c_6852,plain,
$lesseq('#skF_6',$sum('#skE_7',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_6851]) ).
tff(c_6854,plain,
~ $less($sum(c,'#skE_7'),'#skF_6'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_6852]) ).
tff(c_7981,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_7980,c_7815,c_7469,c_6854]) ).
tff(c_7987,plain,
minsol_model_ub('#skE_6','#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_7704]) ).
tff(c_7990,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_7987,c_6637]) ).
tff(c_8076,plain,
! [Z_3258a: $int] :
( $less('#skF_6',$sum(c,summation(Z_3258a)))
| $less(Z_3258a,'#skE_6')
| $less(Z_3258a,'#skF_5') ),
inference(splitRight,[status(thm)],[c_7319]) ).
tff(c_8085,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skE_6')
| $less('#skE_6','#skF_5') ),
inference(superposition,[status(thm),theory(equality)],[c_6755,c_8076]) ).
tff(c_8087,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_5') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_8085]) ).
tff(c_8088,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6649,c_6756,c_8087]) ).
tff(c_8092,plain,
minsol_model_ub('#skF_7','#skF_8','#skF_9'),
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_8188,plain,
! [N_3325a: $int,X_3327a: $int,Y_3328a: $int] :
( ~ $less(N_3325a,$sum(c,summation('#skF_1'(X_3327a,Y_3328a,N_3325a))))
| ~ model_ub(X_3327a,Y_3328a,N_3325a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_25]) ).
tff(c_8198,plain,
! [N_3333a: $int,X_3335a: $int,Y_3336a: $int] :
( ~ $less(N_3333a,$sum(c,summation('#skF_1'(X_3335a,Y_3336a,N_3333a))))
| ~ minsol_model_ub(X_3335a,Y_3336a,N_3333a) ),
inference(resolution,[status(thm)],[c_73,c_8188]) ).
tff(c_8204,plain,
~ $less('#skF_9',$sum(c,summation('#skF_1'('#skF_7','#skF_8','#skF_9')))),
inference(resolution,[status(thm)],[c_8092,c_8198]) ).
tff(c_8238,plain,
'#skF_1'('#skF_7','#skF_8','#skF_9') = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_8204]) ).
tff(c_8237,plain,
~ $less('#skF_9',$sum(c,summation('#skF_1'('#skF_7','#skF_8','#skF_9')))),
inference(resolution,[status(thm)],[c_8092,c_8198]) ).
tff(c_8248,plain,
~ $less('#skF_9',$sum(c,summation('#skE_1'))),
inference(demodulation,[status(thm),theory(equality)],[c_8238,c_8237]) ).
tff(c_8282,plain,
summation('#skE_1') = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_8248]) ).
tff(c_8168,plain,
! [X_3311a: $int,Y_3312a: $int,N_3313a: $int] :
( $less('#skF_2'(X_3311a,Y_3312a,N_3313a),N_3313a)
| minsol_model_max(X_3311a,Y_3312a,N_3313a)
| ~ model_max(X_3311a,Y_3312a,N_3313a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_34]) ).
tff(c_8374,plain,
! [X_3403a: $int,Y_3404a: $int,N_3405a: $int] :
( $less('#skF_2'(X_3403a,Y_3404a,N_3405a),N_3405a)
| minsol_model_max(X_3403a,Y_3404a,N_3405a)
| $less(N_3405a,$sum(c,summation(max(X_3403a,Y_3404a)))) ),
inference(resolution,[status(thm)],[c_91,c_8168]) ).
tff(c_8122,plain,
~ minsol_model_max('#skF_7','#skF_8','#skF_9'),
inference(splitLeft,[status(thm)],[c_66]) ).
tff(c_8396,plain,
( $less('#skF_2'('#skF_7','#skF_8','#skF_9'),'#skF_9')
| $less('#skF_9',$sum(c,summation(max('#skF_7','#skF_8')))) ),
inference(resolution,[status(thm)],[c_8374,c_8122]) ).
tff(c_8417,plain,
max('#skF_7','#skF_8') = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_8396]) ).
tff(c_8442,plain,
( ( '#skF_8' = '#skE_4' )
| $less('#skF_8','#skF_7') ),
inference(superposition,[status(thm),theory(equality)],[c_8417,c_99]) ).
tff(c_8455,plain,
$less('#skF_8','#skF_7'),
inference(splitLeft,[status(thm)],[c_8442]) ).
tff(c_8440,plain,
( ( '#skF_7' = '#skE_4' )
| $less('#skF_7','#skF_8') ),
inference(superposition,[status(thm),theory(equality)],[c_8417,c_100]) ).
tff(c_8451,plain,
$less('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_8440]) ).
tff(c_8478,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_8455,c_8451]) ).
tff(c_8481,plain,
'#skF_8' = '#skE_4',
inference(splitRight,[status(thm)],[c_8442]) ).
tff(c_8482,plain,
~ $less('#skF_8','#skF_7'),
inference(splitRight,[status(thm)],[c_8442]) ).
tff(c_8527,plain,
~ $less('#skE_4','#skF_7'),
inference(demodulation,[status(thm),theory(equality)],[c_8481,c_8482]) ).
tff(c_8400,plain,
max('#skF_7','#skF_8') = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_8396]) ).
tff(c_8399,plain,
'#skF_2'('#skF_7','#skF_8','#skF_9') = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_8396]) ).
tff(c_8398,plain,
( $less('#skF_2'('#skF_7','#skF_8','#skF_9'),'#skF_9')
| $less('#skF_9',$sum(c,summation(max('#skF_7','#skF_8')))) ),
inference(resolution,[status(thm)],[c_8374,c_8122]) ).
tff(c_8414,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,summation('#skE_4'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_8400,c_8399,c_8398]) ).
tff(c_8662,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_8414]) ).
tff(c_8525,plain,
minsol_model_ub('#skF_7','#skE_4','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_8481,c_8092]) ).
tff(c_8205,plain,
! [X_3342a: $int,Y_3346a: $int,N_3345a: $int,Z_3344a: $int] :
( model_ub(X_3342a,Y_3346a,N_3345a)
| $less(N_3345a,$sum(c,summation(Z_3344a)))
| ~ ub(X_3342a,Y_3346a,Z_3344a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_22]) ).
tff(c_8217,plain,
! [X_3354a: $int,Y_3355a: $int,N_3356a: $int,Z_3357a: $int] :
( model_ub(X_3354a,Y_3355a,N_3356a)
| $less(N_3356a,$sum(c,summation(Z_3357a)))
| $less(Z_3357a,X_3354a)
| $less(Z_3357a,Y_3355a) ),
inference(resolution,[status(thm)],[c_96,c_8205]) ).
tff(c_9237,plain,
! [N_3671a: $int,N_3670a: $int,Y_3673a: $int,Z_3674a: $int,X_3675a: $int] :
( ~ minsol_model_ub(X_3675a,Y_3673a,N_3670a)
| ~ $less(N_3671a,N_3670a)
| $less(N_3671a,$sum(c,summation(Z_3674a)))
| $less(Z_3674a,X_3675a)
| $less(Z_3674a,Y_3673a) ),
inference(resolution,[status(thm)],[c_8217,c_74]) ).
tff(c_9246,plain,
! [N_3677a: $int,Z_3679a: $int] :
( ~ $less(N_3677a,'#skF_9')
| $less(N_3677a,$sum(c,summation(Z_3679a)))
| $less(Z_3679a,'#skF_7')
| $less(Z_3679a,'#skE_4') ),
inference(resolution,[status(thm)],[c_8525,c_9237]) ).
tff(c_9253,plain,
! [N_3677a: $int] :
( ~ $less(N_3677a,'#skF_9')
| $less(N_3677a,$sum(c,'#skE_5'))
| $less('#skE_4','#skF_7')
| $less('#skE_4','#skE_4') ),
inference(superposition,[status(thm),theory(equality)],[c_8662,c_9246]) ).
tff(c_9255,plain,
! [N_3677a: $int] :
( ~ $less(N_3677a,'#skF_9')
| $less(N_3677a,$sum(c,'#skE_5'))
| $less('#skE_4','#skF_7') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_9253]) ).
tff(c_9259,plain,
! [N_3677a: $int] :
( ~ $less(N_3677a,'#skF_9')
| $less(N_3677a,$sum(c,'#skE_5')) ),
inference(negUnitSimplification,[status(thm)],[c_8527,c_9255]) ).
tff(c_9260,plain,
$lesseq('#skF_9',$sum('#skE_5',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_9259]) ).
tff(c_9262,plain,
~ $less($sum(c,'#skE_5'),'#skF_9'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_9260]) ).
tff(c_8668,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_8414]) ).
tff(c_8283,plain,
summation('#skE_1') = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_8248]) ).
tff(c_8320,plain,
! [Y_2a: $int] :
( ~ $less(summation(Y_2a),'#skE_2')
| $less(Y_2a,'#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_8283,c_102]) ).
tff(c_8713,plain,
( ~ $less('#skE_5','#skE_2')
| $less('#skE_4','#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_8668,c_8320]) ).
tff(c_8742,plain,
~ $less('#skE_5','#skE_2'),
inference(splitLeft,[status(thm)],[c_8713]) ).
tff(c_8314,plain,
! [Y_2a: $int] :
( $less(summation(Y_2a),'#skE_2')
| ~ $less(Y_2a,'#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_8283,c_101]) ).
tff(c_8719,plain,
( $less('#skE_5','#skE_2')
| ~ $less('#skE_4','#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_8668,c_8314]) ).
tff(c_8793,plain,
~ $less('#skE_4','#skE_1'),
inference(negUnitSimplification,[status(thm)],[c_8742,c_8719]) ).
tff(c_8311,plain,
! [X_1a: $int] :
( $less('#skE_2',summation(X_1a))
| ~ $less('#skE_1',X_1a) ),
inference(superposition,[status(thm),theory(equality)],[c_8283,c_101]) ).
tff(c_8715,plain,
( $less('#skE_2','#skE_5')
| ~ $less('#skE_1','#skE_4') ),
inference(superposition,[status(thm),theory(equality)],[c_8668,c_8311]) ).
tff(c_8763,plain,
~ $less('#skE_1','#skE_4'),
inference(splitLeft,[status(thm)],[c_8715]) ).
tff(c_8279,plain,
summation('#skE_1') = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_8248]) ).
tff(c_8721,plain,
( ( '#skE_5' = '#skE_2' )
| ( '#skE_4' != '#skE_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_8668,c_8279]) ).
tff(c_8740,plain,
'#skE_4' != '#skE_1',
inference(splitLeft,[status(thm)],[c_8721]) ).
tff(c_8794,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_8793,c_8763,c_8740]) ).
tff(c_8798,plain,
$less('#skE_1','#skE_4'),
inference(splitRight,[status(thm)],[c_8715]) ).
tff(c_8529,plain,
minsol_model_ub('#skF_7','#skE_4','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_8481,c_8092]) ).
tff(c_8251,plain,
'#skF_1'('#skF_7','#skF_8','#skF_9') = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_8204]) ).
tff(c_8267,plain,
( ub('#skF_7','#skF_8','#skE_1')
| ~ model_ub('#skF_7','#skF_8','#skF_9') ),
inference(superposition,[status(thm),theory(equality)],[c_8251,c_79]) ).
tff(c_8830,plain,
( ub('#skF_7','#skE_4','#skE_1')
| ~ model_ub('#skF_7','#skE_4','#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_8481,c_8481,c_8267]) ).
tff(c_8890,plain,
~ model_ub('#skF_7','#skE_4','#skF_9'),
inference(splitLeft,[status(thm)],[c_8830]) ).
tff(c_8896,plain,
~ minsol_model_ub('#skF_7','#skE_4','#skF_9'),
inference(resolution,[status(thm)],[c_73,c_8890]) ).
tff(c_8903,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_8529,c_8896]) ).
tff(c_8961,plain,
ub('#skF_7','#skE_4','#skE_1'),
inference(splitRight,[status(thm)],[c_8830]) ).
tff(c_8967,plain,
~ $less('#skE_1','#skE_4'),
inference(resolution,[status(thm)],[c_8961,c_98]) ).
tff(c_8980,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_8798,c_8967]) ).
tff(c_8984,plain,
$less('#skE_5','#skE_2'),
inference(splitRight,[status(thm)],[c_8713]) ).
tff(c_8273,plain,
summation('#skE_1') = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_8248]) ).
tff(c_8272,plain,
~ $less('#skF_9',$sum(c,summation('#skE_1'))),
inference(demodulation,[status(thm),theory(equality)],[c_8238,c_8237]) ).
tff(c_8280,plain,
~ $less('#skF_9',$sum(c,'#skE_2')),
inference(demodulation,[status(thm),theory(equality)],[c_8273,c_8272]) ).
tff(c_9263,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_9262,c_8984,c_8280]) ).
tff(c_9267,plain,
'#skE_4' = '#skE_1',
inference(splitRight,[status(thm)],[c_8721]) ).
tff(c_8411,plain,
max('#skF_7','#skF_8') = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_8396]) ).
tff(c_8513,plain,
max('#skF_7','#skE_4') = '#skE_4',
inference(demodulation,[status(thm),theory(equality)],[c_8481,c_8411]) ).
tff(c_9361,plain,
max('#skF_7','#skE_1') = '#skE_1',
inference(demodulation,[status(thm),theory(equality)],[c_9267,c_9267,c_8513]) ).
tff(c_8408,plain,
'#skF_2'('#skF_7','#skF_8','#skF_9') = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_8396]) ).
tff(c_8601,plain,
'#skF_2'('#skF_7','#skE_4','#skF_9') = '#skE_3',
inference(demodulation,[status(thm),theory(equality)],[c_8481,c_8408]) ).
tff(c_8617,plain,
( model_max('#skF_7','#skE_4','#skE_3')
| minsol_model_max('#skF_7','#skE_4','#skF_9')
| ~ model_max('#skF_7','#skE_4','#skF_9') ),
inference(superposition,[status(thm),theory(equality)],[c_8601,c_75]) ).
tff(c_9819,plain,
( model_max('#skF_7','#skE_1','#skE_3')
| minsol_model_max('#skF_7','#skE_1','#skF_9')
| ~ model_max('#skF_7','#skE_1','#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_9267,c_9267,c_9267,c_8617]) ).
tff(c_9827,plain,
~ model_max('#skF_7','#skE_1','#skF_9'),
inference(splitLeft,[status(thm)],[c_9819]) ).
tff(c_9830,plain,
$less('#skF_9',$sum(c,summation(max('#skF_7','#skE_1')))),
inference(resolution,[status(thm)],[c_91,c_9827]) ).
tff(c_9835,plain,
$less('#skF_9',$sum(c,'#skE_2')),
inference(demodulation,[status(thm),theory(equality)],[c_8282,c_9361,c_9830]) ).
tff(c_9837,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8280,c_9835]) ).
tff(c_9841,plain,
( minsol_model_max('#skF_7','#skE_1','#skF_9')
| model_max('#skF_7','#skE_1','#skE_3') ),
inference(splitRight,[status(thm)],[c_9819]) ).
tff(c_9850,plain,
model_max('#skF_7','#skE_1','#skE_3'),
inference(splitLeft,[status(thm)],[c_9841]) ).
tff(c_9856,plain,
~ $less('#skE_3',$sum(c,summation(max('#skF_7','#skE_1')))),
inference(resolution,[status(thm)],[c_9850,c_95]) ).
tff(c_9865,plain,
~ $less('#skE_3',$sum(c,'#skE_2')),
inference(demodulation,[status(thm),theory(equality)],[c_8282,c_9361,c_9856]) ).
tff(c_9330,plain,
minsol_model_ub('#skF_7','#skE_1','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_9267,c_8525]) ).
tff(c_9334,plain,
minsol_model_ub('#skF_7','#skE_1','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_9267,c_8525]) ).
tff(c_9332,plain,
'#skF_8' = '#skE_1',
inference(demodulation,[status(thm),theory(equality)],[c_9267,c_8481]) ).
tff(c_9474,plain,
( ub('#skF_7','#skE_1','#skE_1')
| ~ model_ub('#skF_7','#skE_1','#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_9332,c_9332,c_8267]) ).
tff(c_9482,plain,
~ model_ub('#skF_7','#skE_1','#skF_9'),
inference(splitLeft,[status(thm)],[c_9474]) ).
tff(c_9488,plain,
~ minsol_model_ub('#skF_7','#skE_1','#skF_9'),
inference(resolution,[status(thm)],[c_73,c_9482]) ).
tff(c_9495,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_9334,c_9488]) ).
tff(c_9502,plain,
ub('#skF_7','#skE_1','#skE_1'),
inference(splitRight,[status(thm)],[c_9474]) ).
tff(c_9505,plain,
! [N_15a: $int] :
( model_ub('#skF_7','#skE_1',N_15a)
| $less(N_15a,$sum(c,summation('#skE_1'))) ),
inference(resolution,[status(thm)],[c_9502,c_87]) ).
tff(c_9535,plain,
! [N_3816a: $int] :
( model_ub('#skF_7','#skE_1',N_3816a)
| $less(N_3816a,$sum(c,'#skE_2')) ),
inference(demodulation,[status(thm),theory(equality)],[c_8282,c_9505]) ).
tff(c_9558,plain,
! [N_3828a: $int,N_3829a: $int] :
( ~ minsol_model_ub('#skF_7','#skE_1',N_3828a)
| ~ $less(N_3829a,N_3828a)
| $less(N_3829a,$sum(c,'#skE_2')) ),
inference(resolution,[status(thm)],[c_9535,c_74]) ).
tff(c_9562,plain,
! [N_3829a: $int] :
( ~ $less(N_3829a,'#skF_9')
| $less(N_3829a,$sum(c,'#skE_2')) ),
inference(resolution,[status(thm)],[c_9330,c_9558]) ).
tff(c_9564,plain,
! [N_3829a: $int] :
( ~ $less(N_3829a,'#skF_9')
| $less(N_3829a,$sum(c,'#skE_2')) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_9562]) ).
tff(c_9565,plain,
$lesseq('#skF_9',$sum('#skE_2',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_9564]) ).
tff(c_9567,plain,
~ $less($sum(c,'#skE_2'),'#skF_9'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_9565]) ).
tff(c_9266,plain,
'#skE_5' = '#skE_2',
inference(splitRight,[status(thm)],[c_8721]) ).
tff(c_8656,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_8414]) ).
tff(c_8655,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,summation('#skE_4'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_8400,c_8399,c_8398]) ).
tff(c_8663,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,'#skE_5')) ),
inference(demodulation,[status(thm),theory(equality)],[c_8656,c_8655]) ).
tff(c_9402,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,'#skE_2')) ),
inference(demodulation,[status(thm),theory(equality)],[c_9266,c_8663]) ).
tff(c_9404,plain,
$less('#skE_3','#skF_9'),
inference(negUnitSimplification,[status(thm)],[c_8280,c_9402]) ).
tff(c_9874,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_9865,c_9567,c_9404]) ).
tff(c_9880,plain,
minsol_model_max('#skF_7','#skE_1','#skF_9'),
inference(splitRight,[status(thm)],[c_9841]) ).
tff(c_8522,plain,
~ minsol_model_max('#skF_7','#skE_4','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_8481,c_8122]) ).
tff(c_9323,plain,
~ minsol_model_max('#skF_7','#skE_1','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_9267,c_8522]) ).
tff(c_9883,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_9880,c_9323]) ).
tff(c_9886,plain,
'#skF_7' = '#skE_4',
inference(splitRight,[status(thm)],[c_8440]) ).
tff(c_9887,plain,
~ $less('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_8440]) ).
tff(c_9929,plain,
~ $less('#skE_4','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_9886,c_9887]) ).
tff(c_10120,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_8414]) ).
tff(c_9927,plain,
minsol_model_ub('#skE_4','#skF_8','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_9886,c_8092]) ).
tff(c_10364,plain,
! [X_4188a: $int,N_4183a: $int,Z_4187a: $int,Y_4186a: $int,N_4184a: $int] :
( ~ minsol_model_ub(X_4188a,Y_4186a,N_4183a)
| ~ $less(N_4184a,N_4183a)
| $less(N_4184a,$sum(c,summation(Z_4187a)))
| $less(Z_4187a,X_4188a)
| $less(Z_4187a,Y_4186a) ),
inference(resolution,[status(thm)],[c_8217,c_74]) ).
tff(c_10373,plain,
! [N_4190a: $int,Z_4192a: $int] :
( ~ $less(N_4190a,'#skF_9')
| $less(N_4190a,$sum(c,summation(Z_4192a)))
| $less(Z_4192a,'#skE_4')
| $less(Z_4192a,'#skF_8') ),
inference(resolution,[status(thm)],[c_9927,c_10364]) ).
tff(c_10380,plain,
! [N_4190a: $int] :
( ~ $less(N_4190a,'#skF_9')
| $less(N_4190a,$sum(c,'#skE_5'))
| $less('#skE_4','#skE_4')
| $less('#skE_4','#skF_8') ),
inference(superposition,[status(thm),theory(equality)],[c_10120,c_10373]) ).
tff(c_10382,plain,
! [N_4190a: $int] :
( ~ $less(N_4190a,'#skF_9')
| $less(N_4190a,$sum(c,'#skE_5'))
| $less('#skE_4','#skF_8') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_10380]) ).
tff(c_10386,plain,
! [N_4190a: $int] :
( ~ $less(N_4190a,'#skF_9')
| $less(N_4190a,$sum(c,'#skE_5')) ),
inference(negUnitSimplification,[status(thm)],[c_9929,c_10382]) ).
tff(c_10387,plain,
$lesseq('#skF_9',$sum('#skE_5',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_10386]) ).
tff(c_10389,plain,
~ $less($sum(c,'#skE_5'),'#skF_9'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_10387]) ).
tff(c_10124,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_8414]) ).
tff(c_10175,plain,
( $less('#skE_5','#skE_2')
| ~ $less('#skE_4','#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_10124,c_8314]) ).
tff(c_10217,plain,
~ $less('#skE_4','#skE_1'),
inference(splitLeft,[status(thm)],[c_10175]) ).
tff(c_10177,plain,
( ( '#skE_5' = '#skE_2' )
| ( '#skE_4' != '#skE_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_10124,c_8279]) ).
tff(c_10196,plain,
'#skE_4' != '#skE_1',
inference(splitLeft,[status(thm)],[c_10177]) ).
tff(c_9966,plain,
minsol_model_ub('#skE_4','#skF_8','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_9886,c_8092]) ).
tff(c_10066,plain,
( ub('#skE_4','#skF_8','#skE_1')
| ~ model_ub('#skE_4','#skF_8','#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_9886,c_9886,c_8267]) ).
tff(c_10074,plain,
~ model_ub('#skE_4','#skF_8','#skF_9'),
inference(splitLeft,[status(thm)],[c_10066]) ).
tff(c_10080,plain,
~ minsol_model_ub('#skE_4','#skF_8','#skF_9'),
inference(resolution,[status(thm)],[c_73,c_10074]) ).
tff(c_10087,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_9966,c_10080]) ).
tff(c_10094,plain,
ub('#skE_4','#skF_8','#skE_1'),
inference(splitRight,[status(thm)],[c_10066]) ).
tff(c_10113,plain,
~ $less('#skE_1','#skE_4'),
inference(resolution,[status(thm)],[c_10094,c_97]) ).
tff(c_10218,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_10217,c_10196,c_10113]) ).
tff(c_10221,plain,
$less('#skE_5','#skE_2'),
inference(splitRight,[status(thm)],[c_10175]) ).
tff(c_10390,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_10389,c_10221,c_8280]) ).
tff(c_10394,plain,
'#skE_4' = '#skE_1',
inference(splitRight,[status(thm)],[c_10177]) ).
tff(c_9915,plain,
max('#skE_4','#skF_8') = '#skE_4',
inference(demodulation,[status(thm),theory(equality)],[c_9886,c_8411]) ).
tff(c_10476,plain,
max('#skE_1','#skF_8') = '#skE_1',
inference(demodulation,[status(thm),theory(equality)],[c_10394,c_10394,c_9915]) ).
tff(c_9938,plain,
'#skF_2'('#skE_4','#skF_8','#skF_9') = '#skE_3',
inference(demodulation,[status(thm),theory(equality)],[c_9886,c_8408]) ).
tff(c_9954,plain,
( model_max('#skE_4','#skF_8','#skE_3')
| minsol_model_max('#skE_4','#skF_8','#skF_9')
| ~ model_max('#skE_4','#skF_8','#skF_9') ),
inference(superposition,[status(thm),theory(equality)],[c_9938,c_75]) ).
tff(c_10929,plain,
( model_max('#skE_1','#skF_8','#skE_3')
| minsol_model_max('#skE_1','#skF_8','#skF_9')
| ~ model_max('#skE_1','#skF_8','#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_10394,c_10394,c_10394,c_9954]) ).
tff(c_10937,plain,
~ model_max('#skE_1','#skF_8','#skF_9'),
inference(splitLeft,[status(thm)],[c_10929]) ).
tff(c_10940,plain,
$less('#skF_9',$sum(c,summation(max('#skE_1','#skF_8')))),
inference(resolution,[status(thm)],[c_91,c_10937]) ).
tff(c_10945,plain,
$less('#skF_9',$sum(c,'#skE_2')),
inference(demodulation,[status(thm),theory(equality)],[c_8282,c_10476,c_10940]) ).
tff(c_10947,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_8280,c_10945]) ).
tff(c_10951,plain,
( minsol_model_max('#skE_1','#skF_8','#skF_9')
| model_max('#skE_1','#skF_8','#skE_3') ),
inference(splitRight,[status(thm)],[c_10929]) ).
tff(c_10960,plain,
model_max('#skE_1','#skF_8','#skE_3'),
inference(splitLeft,[status(thm)],[c_10951]) ).
tff(c_10966,plain,
~ $less('#skE_3',$sum(c,summation(max('#skE_1','#skF_8')))),
inference(resolution,[status(thm)],[c_10960,c_95]) ).
tff(c_10975,plain,
~ $less('#skE_3',$sum(c,'#skE_2')),
inference(demodulation,[status(thm),theory(equality)],[c_8282,c_10476,c_10966]) ).
tff(c_10465,plain,
minsol_model_ub('#skE_1','#skF_8','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_10394,c_9927]) ).
tff(c_10091,plain,
ub('#skE_4','#skF_8','#skE_1'),
inference(splitRight,[status(thm)],[c_10066]) ).
tff(c_10552,plain,
ub('#skE_1','#skF_8','#skE_1'),
inference(demodulation,[status(thm),theory(equality)],[c_10394,c_10091]) ).
tff(c_10555,plain,
! [N_15a: $int] :
( model_ub('#skE_1','#skF_8',N_15a)
| $less(N_15a,$sum(c,summation('#skE_1'))) ),
inference(resolution,[status(thm)],[c_10552,c_87]) ).
tff(c_10645,plain,
! [N_4312a: $int] :
( model_ub('#skE_1','#skF_8',N_4312a)
| $less(N_4312a,$sum(c,'#skE_2')) ),
inference(demodulation,[status(thm),theory(equality)],[c_8282,c_10555]) ).
tff(c_10672,plain,
! [N_4326a: $int,N_4327a: $int] :
( ~ minsol_model_ub('#skE_1','#skF_8',N_4326a)
| ~ $less(N_4327a,N_4326a)
| $less(N_4327a,$sum(c,'#skE_2')) ),
inference(resolution,[status(thm)],[c_10645,c_74]) ).
tff(c_10676,plain,
! [N_4327a: $int] :
( ~ $less(N_4327a,'#skF_9')
| $less(N_4327a,$sum(c,'#skE_2')) ),
inference(resolution,[status(thm)],[c_10465,c_10672]) ).
tff(c_10678,plain,
! [N_4327a: $int] :
( ~ $less(N_4327a,'#skF_9')
| $less(N_4327a,$sum(c,'#skE_2')) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_10676]) ).
tff(c_10679,plain,
$lesseq('#skF_9',$sum('#skE_2',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_10678]) ).
tff(c_10681,plain,
~ $less($sum(c,'#skE_2'),'#skF_9'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_10679]) ).
tff(c_10393,plain,
'#skE_5' = '#skE_2',
inference(splitRight,[status(thm)],[c_10177]) ).
tff(c_10114,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_8414]) ).
tff(c_10121,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,'#skE_5')) ),
inference(demodulation,[status(thm),theory(equality)],[c_10114,c_8655]) ).
tff(c_10539,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,'#skE_2')) ),
inference(demodulation,[status(thm),theory(equality)],[c_10393,c_10121]) ).
tff(c_10541,plain,
$less('#skE_3','#skF_9'),
inference(negUnitSimplification,[status(thm)],[c_8280,c_10539]) ).
tff(c_10979,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_10975,c_10681,c_10541]) ).
tff(c_10985,plain,
minsol_model_max('#skE_1','#skF_8','#skF_9'),
inference(splitRight,[status(thm)],[c_10951]) ).
tff(c_9924,plain,
~ minsol_model_max('#skE_4','#skF_8','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_9886,c_8122]) ).
tff(c_10459,plain,
~ minsol_model_max('#skE_1','#skF_8','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_10394,c_9924]) ).
tff(c_10988,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_10985,c_10459]) ).
tff(c_10992,plain,
minsol_model_max('#skF_4','#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_66]) ).
tff(c_11053,plain,
! [N_4550a: $int,X_4552a: $int,Y_4553a: $int] :
( ~ $less(N_4550a,$sum(c,summation(max(X_4552a,Y_4553a))))
| ~ model_max(X_4552a,Y_4553a,N_4550a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_16]) ).
tff(c_11067,plain,
! [N_4555a: $int,X_4557a: $int,Y_4558a: $int] :
( ~ $less(N_4555a,$sum(c,summation(max(X_4557a,Y_4558a))))
| ~ minsol_model_max(X_4557a,Y_4558a,N_4555a) ),
inference(resolution,[status(thm)],[c_77,c_11053]) ).
tff(c_11073,plain,
~ $less('#skF_6',$sum(c,summation(max('#skF_4','#skF_5')))),
inference(resolution,[status(thm)],[c_10992,c_11067]) ).
tff(c_15080,plain,
max('#skF_4','#skF_5') = '#skE_6',
inference(define,[status(thm),theory(equality)],[c_11073]) ).
tff(c_15105,plain,
( ( '#skF_5' = '#skE_6' )
| $less('#skF_5','#skF_4') ),
inference(superposition,[status(thm),theory(equality)],[c_15080,c_99]) ).
tff(c_15176,plain,
$less('#skF_5','#skF_4'),
inference(splitLeft,[status(thm)],[c_15105]) ).
tff(c_15103,plain,
( ( '#skF_4' = '#skE_6' )
| $less('#skF_4','#skF_5') ),
inference(superposition,[status(thm),theory(equality)],[c_15080,c_100]) ).
tff(c_15114,plain,
$less('#skF_4','#skF_5'),
inference(splitLeft,[status(thm)],[c_15103]) ).
tff(c_15177,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_15176,c_15114]) ).
tff(c_15180,plain,
'#skF_5' = '#skE_6',
inference(splitRight,[status(thm)],[c_15105]) ).
tff(c_15181,plain,
~ $less('#skF_5','#skF_4'),
inference(splitRight,[status(thm)],[c_15105]) ).
tff(c_15218,plain,
~ $less('#skE_6','#skF_4'),
inference(demodulation,[status(thm),theory(equality)],[c_15180,c_15181]) ).
tff(c_15079,plain,
max('#skF_4','#skF_5') = '#skE_6',
inference(define,[status(thm),theory(equality)],[c_11073]) ).
tff(c_11040,plain,
! [X_4544a: $int,Y_4545a: $int,N_4546a: $int] :
( model_max(X_4544a,Y_4545a,N_4546a)
| $less(N_4546a,$sum(c,summation(max(X_4544a,Y_4545a)))) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_19]) ).
tff(c_15060,plain,
! [X_5901a: $int,Y_5898a: $int,N_5900a: $int,N_5899a: $int] :
( ~ minsol_model_max(X_5901a,Y_5898a,N_5900a)
| ~ $less(N_5899a,N_5900a)
| $less(N_5899a,$sum(c,summation(max(X_5901a,Y_5898a)))) ),
inference(resolution,[status(thm)],[c_11040,c_78]) ).
tff(c_15066,plain,
! [N_5899a: $int] :
( ~ $less(N_5899a,'#skF_6')
| $less(N_5899a,$sum(c,summation(max('#skF_4','#skF_5')))) ),
inference(resolution,[status(thm)],[c_10992,c_15060]) ).
tff(c_15120,plain,
! [N_5899a: $int] :
( ~ $less(N_5899a,'#skF_6')
| $less(N_5899a,$sum(c,summation('#skE_6'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_15079,c_15066]) ).
tff(c_15131,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_15120]) ).
tff(c_15067,plain,
max('#skF_4','#skF_5') = '#skE_6',
inference(define,[status(thm),theory(equality)],[c_11073]) ).
tff(c_11114,plain,
~ $less('#skF_6',$sum(c,summation(max('#skF_4','#skF_5')))),
inference(resolution,[status(thm)],[c_10992,c_11067]) ).
tff(c_15077,plain,
~ $less('#skF_6',$sum(c,summation('#skE_6'))),
inference(demodulation,[status(thm),theory(equality)],[c_15067,c_11114]) ).
tff(c_15473,plain,
~ $less('#skF_6',$sum(c,'#skE_7')),
inference(demodulation,[status(thm),theory(equality)],[c_15131,c_15077]) ).
tff(c_15128,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_15120]) ).
tff(c_15053,plain,
! [X_5891a: $int,Y_5895a: $int,N_5894a: $int,Z_5893a: $int] :
( model_ub(X_5891a,Y_5895a,N_5894a)
| $less(N_5894a,$sum(c,summation(Z_5893a)))
| ~ ub(X_5891a,Y_5895a,Z_5893a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_22]) ).
tff(c_15059,plain,
! [X_7a: $int,Y_8a: $int,N_5894a: $int,Z_9a: $int] :
( model_ub(X_7a,Y_8a,N_5894a)
| $less(N_5894a,$sum(c,summation(Z_9a)))
| $less(Z_9a,X_7a)
| $less(Z_9a,Y_8a) ),
inference(resolution,[status(thm)],[c_96,c_15053]) ).
tff(c_15590,plain,
! [X_6032a: $int,Y_6034a: $int,N_6033a: $int,Z_6035a: $int] :
( model_ub(X_6032a,Y_6034a,N_6033a)
| $less(N_6033a,$sum(c,summation(Z_6035a)))
| $less(Z_6035a,X_6032a)
| $less(Z_6035a,Y_6034a) ),
inference(resolution,[status(thm)],[c_96,c_15053]) ).
tff(c_15811,plain,
! [X_6138a: $int,Y_6136a: $int,N_6137a: $int,Z_6134a: $int] :
( $less('#skF_3'(X_6138a,Y_6136a,N_6137a),N_6137a)
| minsol_model_ub(X_6138a,Y_6136a,N_6137a)
| $less(N_6137a,$sum(c,summation(Z_6134a)))
| $less(Z_6134a,X_6138a)
| $less(Z_6134a,Y_6136a) ),
inference(resolution,[status(thm)],[c_15590,c_72]) ).
tff(c_11074,plain,
! [N_4563a: $int,X_4565a: $int,Y_4566a: $int] :
( ~ $less(N_4563a,$sum(c,summation('#skF_1'(X_4565a,Y_4566a,N_4563a))))
| ~ model_ub(X_4565a,Y_4566a,N_4563a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_25]) ).
tff(c_11099,plain,
! [N_4580a: $int,X_4582a: $int,Y_4583a: $int] :
( ~ $less(N_4580a,$sum(c,summation('#skF_1'(X_4582a,Y_4583a,N_4580a))))
| ~ minsol_model_ub(X_4582a,Y_4583a,N_4580a) ),
inference(resolution,[status(thm)],[c_73,c_11074]) ).
tff(c_11105,plain,
~ $less('#skF_9',$sum(c,summation('#skF_1'('#skF_7','#skF_8','#skF_9')))),
inference(resolution,[status(thm)],[c_8092,c_11099]) ).
tff(c_11165,plain,
'#skF_1'('#skF_7','#skF_8','#skF_9') = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_11105]) ).
tff(c_11164,plain,
~ $less('#skF_9',$sum(c,summation('#skF_1'('#skF_7','#skF_8','#skF_9')))),
inference(resolution,[status(thm)],[c_8092,c_11099]) ).
tff(c_11175,plain,
~ $less('#skF_9',$sum(c,summation('#skE_1'))),
inference(demodulation,[status(thm),theory(equality)],[c_11165,c_11164]) ).
tff(c_11317,plain,
summation('#skE_1') = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_11175]) ).
tff(c_11992,plain,
! [X_4786a: $int,Y_4787a: $int,N_4788a: $int] :
( $less('#skF_2'(X_4786a,Y_4787a,N_4788a),N_4788a)
| minsol_model_max(X_4786a,Y_4787a,N_4788a)
| $less(N_4788a,$sum(c,summation(max(X_4786a,Y_4787a)))) ),
inference(resolution,[status(thm)],[c_11040,c_76]) ).
tff(c_70,plain,
( ~ minsol_model_ub('#skF_4','#skF_5','#skF_6')
| ~ minsol_model_max('#skF_7','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_11085,plain,
~ minsol_model_max('#skF_7','#skF_8','#skF_9'),
inference(splitLeft,[status(thm)],[c_70]) ).
tff(c_12015,plain,
( $less('#skF_2'('#skF_7','#skF_8','#skF_9'),'#skF_9')
| $less('#skF_9',$sum(c,summation(max('#skF_7','#skF_8')))) ),
inference(resolution,[status(thm)],[c_11992,c_11085]) ).
tff(c_12095,plain,
max('#skF_7','#skF_8') = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_12015]) ).
tff(c_12137,plain,
( ( '#skF_8' = '#skE_4' )
| $less('#skF_8','#skF_7') ),
inference(superposition,[status(thm),theory(equality)],[c_99,c_12095]) ).
tff(c_12141,plain,
$less('#skF_8','#skF_7'),
inference(splitLeft,[status(thm)],[c_12137]) ).
tff(c_12126,plain,
( ( '#skF_7' = '#skE_4' )
| $less('#skF_7','#skF_8') ),
inference(superposition,[status(thm),theory(equality)],[c_12095,c_100]) ).
tff(c_12139,plain,
$less('#skF_7','#skF_8'),
inference(splitLeft,[status(thm)],[c_12126]) ).
tff(c_12142,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_12141,c_12139]) ).
tff(c_12145,plain,
'#skF_8' = '#skE_4',
inference(splitRight,[status(thm)],[c_12137]) ).
tff(c_12146,plain,
~ $less('#skF_8','#skF_7'),
inference(splitRight,[status(thm)],[c_12137]) ).
tff(c_12267,plain,
~ $less('#skE_4','#skF_7'),
inference(demodulation,[status(thm),theory(equality)],[c_12145,c_12146]) ).
tff(c_12078,plain,
max('#skF_7','#skF_8') = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_12015]) ).
tff(c_12077,plain,
'#skF_2'('#skF_7','#skF_8','#skF_9') = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_12015]) ).
tff(c_12076,plain,
( $less('#skF_2'('#skF_7','#skF_8','#skF_9'),'#skF_9')
| $less('#skF_9',$sum(c,summation(max('#skF_7','#skF_8')))) ),
inference(resolution,[status(thm)],[c_11992,c_11085]) ).
tff(c_12092,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,summation('#skE_4'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_12078,c_12077,c_12076]) ).
tff(c_12812,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_12092]) ).
tff(c_11106,plain,
! [X_4589a: $int,Y_4593a: $int,N_4592a: $int,Z_4591a: $int] :
( model_ub(X_4589a,Y_4593a,N_4592a)
| $less(N_4592a,$sum(c,summation(Z_4591a)))
| ~ ub(X_4589a,Y_4593a,Z_4591a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_22]) ).
tff(c_11971,plain,
! [X_4778a: $int,Y_4780a: $int,N_4777a: $int,Z_4781a: $int] :
( model_ub(X_4778a,Y_4780a,N_4777a)
| $less(N_4777a,$sum(c,summation(Z_4781a)))
| $less(Z_4781a,X_4778a)
| $less(Z_4781a,Y_4780a) ),
inference(resolution,[status(thm)],[c_96,c_11106]) ).
tff(c_12034,plain,
! [N_4810a: $int,N_4813a: $int,Z_4809a: $int,Y_4812a: $int,X_4808a: $int] :
( ~ minsol_model_ub(X_4808a,Y_4812a,N_4810a)
| ~ $less(N_4813a,N_4810a)
| $less(N_4813a,$sum(c,summation(Z_4809a)))
| $less(Z_4809a,X_4808a)
| $less(Z_4809a,Y_4812a) ),
inference(resolution,[status(thm)],[c_11971,c_74]) ).
tff(c_12040,plain,
! [N_4813a: $int,Z_4809a: $int] :
( ~ $less(N_4813a,'#skF_9')
| $less(N_4813a,$sum(c,summation(Z_4809a)))
| $less(Z_4809a,'#skF_7')
| $less(Z_4809a,'#skF_8') ),
inference(resolution,[status(thm)],[c_8092,c_12034]) ).
tff(c_12987,plain,
! [N_5163a: $int,Z_5165a: $int] :
( ~ $less(N_5163a,'#skF_9')
| $less(N_5163a,$sum(c,summation(Z_5165a)))
| $less(Z_5165a,'#skF_7')
| $less(Z_5165a,'#skE_4') ),
inference(demodulation,[status(thm),theory(equality)],[c_12145,c_12040]) ).
tff(c_12997,plain,
! [N_5163a: $int] :
( ~ $less(N_5163a,'#skF_9')
| $less(N_5163a,$sum(c,'#skE_5'))
| $less('#skE_4','#skF_7')
| $less('#skE_4','#skE_4') ),
inference(superposition,[status(thm),theory(equality)],[c_12812,c_12987]) ).
tff(c_12999,plain,
! [N_5163a: $int] :
( ~ $less(N_5163a,'#skF_9')
| $less(N_5163a,$sum(c,'#skE_5'))
| $less('#skE_4','#skF_7') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_12997]) ).
tff(c_13209,plain,
! [N_5163a: $int] :
( ~ $less(N_5163a,'#skF_9')
| $less(N_5163a,$sum(c,'#skE_5')) ),
inference(negUnitSimplification,[status(thm)],[c_12267,c_12999]) ).
tff(c_13210,plain,
$lesseq('#skF_9',$sum('#skE_5',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_13209]) ).
tff(c_13212,plain,
~ $less($sum(c,'#skE_5'),'#skF_9'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_13210]) ).
tff(c_12816,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_12092]) ).
tff(c_11318,plain,
summation('#skE_1') = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_11175]) ).
tff(c_11355,plain,
! [Y_2a: $int] :
( ~ $less(summation(Y_2a),'#skE_2')
| $less(Y_2a,'#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_11318,c_102]) ).
tff(c_12898,plain,
( ~ $less('#skE_5','#skE_2')
| $less('#skE_4','#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_12816,c_11355]) ).
tff(c_12925,plain,
~ $less('#skE_5','#skE_2'),
inference(splitLeft,[status(thm)],[c_12898]) ).
tff(c_11349,plain,
! [Y_2a: $int] :
( $less(summation(Y_2a),'#skE_2')
| ~ $less(Y_2a,'#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_11318,c_101]) ).
tff(c_12888,plain,
( $less('#skE_5','#skE_2')
| ~ $less('#skE_4','#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_12816,c_11349]) ).
tff(c_12949,plain,
~ $less('#skE_4','#skE_1'),
inference(negUnitSimplification,[status(thm)],[c_12925,c_12888]) ).
tff(c_11314,plain,
summation('#skE_1') = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_11175]) ).
tff(c_12919,plain,
( ( '#skE_5' = '#skE_2' )
| ( '#skE_4' != '#skE_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_11314,c_12816]) ).
tff(c_12923,plain,
'#skE_4' != '#skE_1',
inference(splitLeft,[status(thm)],[c_12919]) ).
tff(c_8094,plain,
minsol_model_ub('#skF_7','#skF_8','#skF_9'),
inference(splitRight,[status(thm)],[c_62]) ).
tff(c_11214,plain,
'#skF_1'('#skF_7','#skF_8','#skF_9') = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_11105]) ).
tff(c_11230,plain,
( ub('#skF_7','#skF_8','#skE_1')
| ~ model_ub('#skF_7','#skF_8','#skF_9') ),
inference(superposition,[status(thm),theory(equality)],[c_11214,c_79]) ).
tff(c_11842,plain,
~ model_ub('#skF_7','#skF_8','#skF_9'),
inference(splitLeft,[status(thm)],[c_11230]) ).
tff(c_11845,plain,
~ minsol_model_ub('#skF_7','#skF_8','#skF_9'),
inference(resolution,[status(thm)],[c_73,c_11842]) ).
tff(c_11849,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_8094,c_11845]) ).
tff(c_11904,plain,
ub('#skF_7','#skF_8','#skE_1'),
inference(splitRight,[status(thm)],[c_11230]) ).
tff(c_11921,plain,
~ $less('#skE_1','#skF_8'),
inference(resolution,[status(thm)],[c_11904,c_98]) ).
tff(c_12250,plain,
~ $less('#skE_1','#skE_4'),
inference(demodulation,[status(thm),theory(equality)],[c_12145,c_11921]) ).
tff(c_12950,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_12949,c_12923,c_12250]) ).
tff(c_12954,plain,
$less('#skE_5','#skE_2'),
inference(splitRight,[status(thm)],[c_12898]) ).
tff(c_11308,plain,
summation('#skE_1') = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_11175]) ).
tff(c_11307,plain,
~ $less('#skF_9',$sum(c,summation('#skE_1'))),
inference(demodulation,[status(thm),theory(equality)],[c_11165,c_11164]) ).
tff(c_11315,plain,
~ $less('#skF_9',$sum(c,'#skE_2')),
inference(demodulation,[status(thm),theory(equality)],[c_11308,c_11307]) ).
tff(c_13213,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_13212,c_12954,c_11315]) ).
tff(c_13217,plain,
'#skE_4' = '#skE_1',
inference(splitRight,[status(thm)],[c_12919]) ).
tff(c_12089,plain,
max('#skF_7','#skF_8') = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_12015]) ).
tff(c_12236,plain,
max('#skF_7','#skE_4') = '#skE_4',
inference(demodulation,[status(thm),theory(equality)],[c_12145,c_12089]) ).
tff(c_13341,plain,
max('#skF_7','#skE_1') = '#skE_1',
inference(demodulation,[status(thm),theory(equality)],[c_13217,c_13217,c_12236]) ).
tff(c_12294,plain,
max('#skF_7','#skE_4') = '#skE_4',
inference(demodulation,[status(thm),theory(equality)],[c_12145,c_12089]) ).
tff(c_12149,plain,
'#skF_2'('#skF_7','#skF_8','#skF_9') = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_12015]) ).
tff(c_12165,plain,
( model_max('#skF_7','#skF_8','#skE_3')
| minsol_model_max('#skF_7','#skF_8','#skF_9')
| ~ model_max('#skF_7','#skF_8','#skF_9') ),
inference(superposition,[status(thm),theory(equality)],[c_12149,c_75]) ).
tff(c_12442,plain,
( model_max('#skF_7','#skE_4','#skE_3')
| minsol_model_max('#skF_7','#skE_4','#skF_9')
| ~ model_max('#skF_7','#skE_4','#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_12145,c_12145,c_12145,c_12165]) ).
tff(c_12450,plain,
~ model_max('#skF_7','#skE_4','#skF_9'),
inference(splitLeft,[status(thm)],[c_12442]) ).
tff(c_12453,plain,
$less('#skF_9',$sum(c,summation(max('#skF_7','#skE_4')))),
inference(resolution,[status(thm)],[c_91,c_12450]) ).
tff(c_12462,plain,
$less('#skF_9',$sum(c,summation('#skE_4'))),
inference(demodulation,[status(thm),theory(equality)],[c_12294,c_12453]) ).
tff(c_12487,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_12462]) ).
tff(c_12569,plain,
( ~ $less('#skE_5','#skE_2')
| $less('#skE_4','#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_12487,c_11355]) ).
tff(c_12618,plain,
~ $less('#skE_5','#skE_2'),
inference(splitLeft,[status(thm)],[c_12569]) ).
tff(c_12559,plain,
( $less('#skE_5','#skE_2')
| ~ $less('#skE_4','#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_12487,c_11349]) ).
tff(c_12620,plain,
~ $less('#skE_4','#skE_1'),
inference(negUnitSimplification,[status(thm)],[c_12618,c_12559]) ).
tff(c_12590,plain,
( ( '#skE_5' = '#skE_2' )
| ( '#skE_4' != '#skE_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_11314,c_12487]) ).
tff(c_12594,plain,
'#skE_4' != '#skE_1',
inference(splitLeft,[status(thm)],[c_12590]) ).
tff(c_12621,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_12620,c_12594,c_12250]) ).
tff(c_12625,plain,
$less('#skE_5','#skE_2'),
inference(splitRight,[status(thm)],[c_12569]) ).
tff(c_12467,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_12462]) ).
tff(c_12466,plain,
$less('#skF_9',$sum(c,summation('#skE_4'))),
inference(demodulation,[status(thm),theory(equality)],[c_12294,c_12453]) ).
tff(c_12474,plain,
$less('#skF_9',$sum(c,'#skE_5')),
inference(demodulation,[status(thm),theory(equality)],[c_12467,c_12466]) ).
tff(c_12656,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_12625,c_12474,c_11315]) ).
tff(c_12659,plain,
'#skE_5' = '#skE_2',
inference(splitRight,[status(thm)],[c_12590]) ).
tff(c_12779,plain,
$less('#skF_9',$sum(c,'#skE_2')),
inference(demodulation,[status(thm),theory(equality)],[c_12659,c_12474]) ).
tff(c_12780,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11315,c_12779]) ).
tff(c_12784,plain,
( minsol_model_max('#skF_7','#skE_4','#skF_9')
| model_max('#skF_7','#skE_4','#skE_3') ),
inference(splitRight,[status(thm)],[c_12442]) ).
tff(c_13535,plain,
( minsol_model_max('#skF_7','#skE_1','#skF_9')
| model_max('#skF_7','#skE_1','#skE_3') ),
inference(demodulation,[status(thm),theory(equality)],[c_13217,c_13217,c_12784]) ).
tff(c_13543,plain,
model_max('#skF_7','#skE_1','#skE_3'),
inference(splitLeft,[status(thm)],[c_13535]) ).
tff(c_13546,plain,
~ $less('#skE_3',$sum(c,summation(max('#skF_7','#skE_1')))),
inference(resolution,[status(thm)],[c_13543,c_95]) ).
tff(c_13555,plain,
~ $less('#skE_3',$sum(c,'#skE_2')),
inference(demodulation,[status(thm),theory(equality)],[c_11317,c_13341,c_13546]) ).
tff(c_13216,plain,
'#skE_5' = '#skE_2',
inference(splitRight,[status(thm)],[c_12919]) ).
tff(c_12806,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_12092]) ).
tff(c_12476,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,summation('#skE_4'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_12078,c_12077,c_12076]) ).
tff(c_12813,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,'#skE_5')) ),
inference(demodulation,[status(thm),theory(equality)],[c_12806,c_12476]) ).
tff(c_13422,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,'#skE_2')) ),
inference(demodulation,[status(thm),theory(equality)],[c_13216,c_12813]) ).
tff(c_13424,plain,
$less('#skE_3','#skF_9'),
inference(negUnitSimplification,[status(thm)],[c_11315,c_13422]) ).
tff(c_11907,plain,
! [N_15a: $int] :
( model_ub('#skF_7','#skF_8',N_15a)
| $less(N_15a,$sum(c,summation('#skE_1'))) ),
inference(resolution,[status(thm)],[c_11904,c_87]) ).
tff(c_11938,plain,
! [N_4763a: $int] :
( model_ub('#skF_7','#skF_8',N_4763a)
| $less(N_4763a,$sum(c,'#skE_2')) ),
inference(demodulation,[status(thm),theory(equality)],[c_11317,c_11907]) ).
tff(c_11959,plain,
! [N_4775a: $int,N_4776a: $int] :
( ~ minsol_model_ub('#skF_7','#skF_8',N_4775a)
| ~ $less(N_4776a,N_4775a)
| $less(N_4776a,$sum(c,'#skE_2')) ),
inference(resolution,[status(thm)],[c_11938,c_74]) ).
tff(c_11963,plain,
! [N_4776a: $int] :
( ~ $less(N_4776a,'#skF_9')
| $less(N_4776a,$sum(c,'#skE_2')) ),
inference(resolution,[status(thm)],[c_8092,c_11959]) ).
tff(c_11965,plain,
! [N_4776a: $int] :
( ~ $less(N_4776a,'#skF_9')
| $less(N_4776a,$sum(c,'#skE_2')) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_11963]) ).
tff(c_11966,plain,
$lesseq('#skF_9',$sum('#skE_2',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_11965]) ).
tff(c_11968,plain,
~ $less($sum(c,'#skE_2'),'#skF_9'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_11966]) ).
tff(c_13562,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_13555,c_13424,c_11968]) ).
tff(c_13568,plain,
minsol_model_max('#skF_7','#skE_1','#skF_9'),
inference(splitRight,[status(thm)],[c_13535]) ).
tff(c_12259,plain,
~ minsol_model_max('#skF_7','#skE_4','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_12145,c_11085]) ).
tff(c_13296,plain,
~ minsol_model_max('#skF_7','#skE_1','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_13217,c_12259]) ).
tff(c_13571,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_13568,c_13296]) ).
tff(c_13574,plain,
'#skF_7' = '#skE_4',
inference(splitRight,[status(thm)],[c_12126]) ).
tff(c_13575,plain,
~ $less('#skF_7','#skF_8'),
inference(splitRight,[status(thm)],[c_12126]) ).
tff(c_13691,plain,
~ $less('#skE_4','#skF_8'),
inference(demodulation,[status(thm),theory(equality)],[c_13574,c_13575]) ).
tff(c_14283,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_12092]) ).
tff(c_13663,plain,
! [N_4813a: $int,Z_4809a: $int] :
( ~ $less(N_4813a,'#skF_9')
| $less(N_4813a,$sum(c,summation(Z_4809a)))
| $less(Z_4809a,'#skE_4')
| $less(Z_4809a,'#skF_8') ),
inference(demodulation,[status(thm),theory(equality)],[c_13574,c_12040]) ).
tff(c_14348,plain,
! [N_4813a: $int] :
( ~ $less(N_4813a,'#skF_9')
| $less(N_4813a,$sum(c,'#skE_5'))
| $less('#skE_4','#skE_4')
| $less('#skE_4','#skF_8') ),
inference(superposition,[status(thm),theory(equality)],[c_14283,c_13663]) ).
tff(c_14350,plain,
! [N_4813a: $int] :
( ~ $less(N_4813a,'#skF_9')
| $less(N_4813a,$sum(c,'#skE_5'))
| $less('#skE_4','#skF_8') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_14348]) ).
tff(c_14661,plain,
! [N_4813a: $int] :
( ~ $less(N_4813a,'#skF_9')
| $less(N_4813a,$sum(c,'#skE_5')) ),
inference(negUnitSimplification,[status(thm)],[c_13691,c_14350]) ).
tff(c_14662,plain,
$lesseq('#skF_9',$sum('#skE_5',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_14661]) ).
tff(c_14664,plain,
~ $less($sum(c,'#skE_5'),'#skF_9'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_14662]) ).
tff(c_14368,plain,
( ~ $less('#skE_5','#skE_2')
| $less('#skE_4','#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_14283,c_11355]) ).
tff(c_14395,plain,
~ $less('#skE_5','#skE_2'),
inference(splitLeft,[status(thm)],[c_14368]) ).
tff(c_14358,plain,
( $less('#skE_5','#skE_2')
| ~ $less('#skE_4','#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_14283,c_11349]) ).
tff(c_14436,plain,
~ $less('#skE_4','#skE_1'),
inference(negUnitSimplification,[status(thm)],[c_14395,c_14358]) ).
tff(c_14389,plain,
( ( '#skE_5' = '#skE_2' )
| ( '#skE_4' != '#skE_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_11314,c_14283]) ).
tff(c_14393,plain,
'#skE_4' != '#skE_1',
inference(splitLeft,[status(thm)],[c_14389]) ).
tff(c_11923,plain,
~ $less('#skE_1','#skF_7'),
inference(resolution,[status(thm)],[c_11904,c_97]) ).
tff(c_13673,plain,
~ $less('#skE_1','#skE_4'),
inference(demodulation,[status(thm),theory(equality)],[c_13574,c_11923]) ).
tff(c_14437,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_14436,c_14393,c_13673]) ).
tff(c_14441,plain,
$less('#skE_5','#skE_2'),
inference(splitRight,[status(thm)],[c_14368]) ).
tff(c_14665,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_14664,c_14441,c_11315]) ).
tff(c_14669,plain,
'#skE_4' = '#skE_1',
inference(splitRight,[status(thm)],[c_14389]) ).
tff(c_13660,plain,
max('#skE_4','#skF_8') = '#skE_4',
inference(demodulation,[status(thm),theory(equality)],[c_13574,c_12089]) ).
tff(c_14801,plain,
max('#skE_1','#skF_8') = '#skE_1',
inference(demodulation,[status(thm),theory(equality)],[c_14669,c_14669,c_13660]) ).
tff(c_13723,plain,
max('#skE_4','#skF_8') = '#skE_4',
inference(demodulation,[status(thm),theory(equality)],[c_13574,c_12089]) ).
tff(c_13576,plain,
'#skF_2'('#skF_7','#skF_8','#skF_9') = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_12015]) ).
tff(c_13592,plain,
( model_max('#skF_7','#skF_8','#skE_3')
| minsol_model_max('#skF_7','#skF_8','#skF_9')
| ~ model_max('#skF_7','#skF_8','#skF_9') ),
inference(superposition,[status(thm),theory(equality)],[c_13576,c_75]) ).
tff(c_13893,plain,
( model_max('#skE_4','#skF_8','#skE_3')
| minsol_model_max('#skE_4','#skF_8','#skF_9')
| ~ model_max('#skE_4','#skF_8','#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_13574,c_13574,c_13574,c_13592]) ).
tff(c_13901,plain,
~ model_max('#skE_4','#skF_8','#skF_9'),
inference(splitLeft,[status(thm)],[c_13893]) ).
tff(c_13904,plain,
$less('#skF_9',$sum(c,summation(max('#skE_4','#skF_8')))),
inference(resolution,[status(thm)],[c_91,c_13901]) ).
tff(c_13913,plain,
$less('#skF_9',$sum(c,summation('#skE_4'))),
inference(demodulation,[status(thm),theory(equality)],[c_13723,c_13904]) ).
tff(c_13927,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_13913]) ).
tff(c_13996,plain,
( $less('#skE_5','#skE_2')
| ~ $less('#skE_4','#skE_1') ),
inference(superposition,[status(thm),theory(equality)],[c_13927,c_11349]) ).
tff(c_14065,plain,
~ $less('#skE_4','#skE_1'),
inference(splitLeft,[status(thm)],[c_13996]) ).
tff(c_14027,plain,
( ( '#skE_5' = '#skE_2' )
| ( '#skE_4' != '#skE_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_11314,c_13927]) ).
tff(c_14033,plain,
'#skE_4' != '#skE_1',
inference(splitLeft,[status(thm)],[c_14027]) ).
tff(c_14066,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_14065,c_14033,c_13673]) ).
tff(c_14069,plain,
$less('#skE_5','#skE_2'),
inference(splitRight,[status(thm)],[c_13996]) ).
tff(c_13926,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_13913]) ).
tff(c_14029,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,'#skE_5')) ),
inference(demodulation,[status(thm),theory(equality)],[c_13926,c_12092]) ).
tff(c_14031,plain,
$less('#skF_9',$sum(c,'#skE_5')),
inference(splitLeft,[status(thm)],[c_14029]) ).
tff(c_14101,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_14069,c_14031,c_11315]) ).
tff(c_14104,plain,
'#skE_5' = '#skE_2',
inference(splitRight,[status(thm)],[c_14027]) ).
tff(c_14228,plain,
$less('#skF_9',$sum(c,'#skE_2')),
inference(demodulation,[status(thm),theory(equality)],[c_14104,c_14031]) ).
tff(c_14229,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11315,c_14228]) ).
tff(c_14233,plain,
~ $less('#skF_9',$sum(c,'#skE_5')),
inference(splitRight,[status(thm)],[c_14029]) ).
tff(c_13917,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_13913]) ).
tff(c_13916,plain,
$less('#skF_9',$sum(c,summation('#skE_4'))),
inference(demodulation,[status(thm),theory(equality)],[c_13723,c_13904]) ).
tff(c_13924,plain,
$less('#skF_9',$sum(c,'#skE_5')),
inference(demodulation,[status(thm),theory(equality)],[c_13917,c_13916]) ).
tff(c_14256,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_14233,c_13924]) ).
tff(c_14260,plain,
( minsol_model_max('#skE_4','#skF_8','#skF_9')
| model_max('#skE_4','#skF_8','#skE_3') ),
inference(splitRight,[status(thm)],[c_13893]) ).
tff(c_14994,plain,
( minsol_model_max('#skE_1','#skF_8','#skF_9')
| model_max('#skE_1','#skF_8','#skE_3') ),
inference(demodulation,[status(thm),theory(equality)],[c_14669,c_14669,c_14260]) ).
tff(c_15002,plain,
model_max('#skE_1','#skF_8','#skE_3'),
inference(splitLeft,[status(thm)],[c_14994]) ).
tff(c_15005,plain,
~ $less('#skE_3',$sum(c,summation(max('#skE_1','#skF_8')))),
inference(resolution,[status(thm)],[c_15002,c_95]) ).
tff(c_15014,plain,
~ $less('#skE_3',$sum(c,'#skE_2')),
inference(demodulation,[status(thm),theory(equality)],[c_11317,c_14801,c_15005]) ).
tff(c_14668,plain,
'#skE_5' = '#skE_2',
inference(splitRight,[status(thm)],[c_14389]) ).
tff(c_14261,plain,
summation('#skE_4') = '#skE_5',
inference(define,[status(thm),theory(equality)],[c_12092]) ).
tff(c_14268,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,'#skE_5')) ),
inference(demodulation,[status(thm),theory(equality)],[c_14261,c_12476]) ).
tff(c_14881,plain,
( $less('#skE_3','#skF_9')
| $less('#skF_9',$sum(c,'#skE_2')) ),
inference(demodulation,[status(thm),theory(equality)],[c_14668,c_14268]) ).
tff(c_14883,plain,
$less('#skE_3','#skF_9'),
inference(negUnitSimplification,[status(thm)],[c_11315,c_14881]) ).
tff(c_15021,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_15014,c_14883,c_11968]) ).
tff(c_15027,plain,
minsol_model_max('#skE_1','#skF_8','#skF_9'),
inference(splitRight,[status(thm)],[c_14994]) ).
tff(c_13683,plain,
~ minsol_model_max('#skE_4','#skF_8','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_13574,c_11085]) ).
tff(c_14753,plain,
~ minsol_model_max('#skE_1','#skF_8','#skF_9'),
inference(demodulation,[status(thm),theory(equality)],[c_14669,c_13683]) ).
tff(c_15030,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_15027,c_14753]) ).
tff(c_15034,plain,
~ minsol_model_ub('#skF_4','#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_70]) ).
tff(c_15210,plain,
~ minsol_model_ub('#skF_4','#skE_6','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_15180,c_15034]) ).
tff(c_15837,plain,
! [Z_6134a: $int] :
( $less('#skF_3'('#skF_4','#skE_6','#skF_6'),'#skF_6')
| $less('#skF_6',$sum(c,summation(Z_6134a)))
| $less(Z_6134a,'#skF_4')
| $less(Z_6134a,'#skE_6') ),
inference(resolution,[status(thm)],[c_15811,c_15210]) ).
tff(c_15896,plain,
'#skF_3'('#skF_4','#skE_6','#skF_6') = '#skE_8',
inference(define,[status(thm),theory(equality)],[c_15837]) ).
tff(c_15922,plain,
( model_ub('#skF_4','#skE_6','#skE_8')
| minsol_model_ub('#skF_4','#skE_6','#skF_6')
| ~ model_ub('#skF_4','#skE_6','#skF_6') ),
inference(superposition,[status(thm),theory(equality)],[c_15896,c_71]) ).
tff(c_15939,plain,
~ model_ub('#skF_4','#skE_6','#skF_6'),
inference(splitLeft,[status(thm)],[c_15922]) ).
tff(c_15957,plain,
! [Z_6214a: $int] :
( $less('#skF_6',$sum(c,summation(Z_6214a)))
| $less(Z_6214a,'#skF_4')
| $less(Z_6214a,'#skE_6') ),
inference(resolution,[status(thm)],[c_15059,c_15939]) ).
tff(c_15966,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_4')
| $less('#skE_6','#skE_6') ),
inference(superposition,[status(thm),theory(equality)],[c_15128,c_15957]) ).
tff(c_15968,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_4') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_15966]) ).
tff(c_15978,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15218,c_15473,c_15968]) ).
tff(c_15982,plain,
( minsol_model_ub('#skF_4','#skE_6','#skF_6')
| model_ub('#skF_4','#skE_6','#skE_8') ),
inference(splitRight,[status(thm)],[c_15922]) ).
tff(c_15991,plain,
model_ub('#skF_4','#skE_6','#skE_8'),
inference(splitLeft,[status(thm)],[c_15982]) ).
tff(c_16003,plain,
~ $less('#skE_8',$sum(c,summation('#skF_1'('#skF_4','#skE_6','#skE_8')))),
inference(resolution,[status(thm)],[c_15991,c_83]) ).
tff(c_16032,plain,
'#skF_1'('#skF_4','#skE_6','#skE_8') = '#skE_9',
inference(define,[status(thm),theory(equality)],[c_16003]) ).
tff(c_16031,plain,
~ $less('#skE_8',$sum(c,summation('#skF_1'('#skF_4','#skE_6','#skE_8')))),
inference(resolution,[status(thm)],[c_15991,c_83]) ).
tff(c_16042,plain,
~ $less('#skE_8',$sum(c,summation('#skE_9'))),
inference(demodulation,[status(thm),theory(equality)],[c_16032,c_16031]) ).
tff(c_16177,plain,
summation('#skE_9') = '#skE_10',
inference(define,[status(thm),theory(equality)],[c_16042]) ).
tff(c_16176,plain,
~ $less('#skE_8',$sum(c,summation('#skE_9'))),
inference(demodulation,[status(thm),theory(equality)],[c_16032,c_16031]) ).
tff(c_16184,plain,
~ $less('#skE_8',$sum(c,'#skE_10')),
inference(demodulation,[status(thm),theory(equality)],[c_16177,c_16176]) ).
tff(c_16187,plain,
summation('#skE_9') = '#skE_10',
inference(define,[status(thm),theory(equality)],[c_16042]) ).
tff(c_15132,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_15120]) ).
tff(c_15160,plain,
! [X_1a: $int] :
( $less('#skE_7',summation(X_1a))
| ~ $less('#skE_6',X_1a) ),
inference(superposition,[status(thm),theory(equality)],[c_15132,c_101]) ).
tff(c_16265,plain,
( $less('#skE_7','#skE_10')
| ~ $less('#skE_6','#skE_9') ),
inference(superposition,[status(thm),theory(equality)],[c_16187,c_15160]) ).
tff(c_16300,plain,
~ $less('#skE_6','#skE_9'),
inference(splitLeft,[status(thm)],[c_16265]) ).
tff(c_16292,plain,
( ( '#skE_7' = '#skE_10' )
| ( '#skE_9' != '#skE_6' ) ),
inference(superposition,[status(thm),theory(equality)],[c_15128,c_16187]) ).
tff(c_16296,plain,
'#skE_9' != '#skE_6',
inference(splitLeft,[status(thm)],[c_16292]) ).
tff(c_15990,plain,
model_ub('#skF_4','#skE_6','#skE_8'),
inference(splitLeft,[status(thm)],[c_15982]) ).
tff(c_16058,plain,
'#skF_1'('#skF_4','#skE_6','#skE_8') = '#skE_9',
inference(define,[status(thm),theory(equality)],[c_16003]) ).
tff(c_16076,plain,
( ub('#skF_4','#skE_6','#skE_9')
| ~ model_ub('#skF_4','#skE_6','#skE_8') ),
inference(superposition,[status(thm),theory(equality)],[c_16058,c_79]) ).
tff(c_16108,plain,
ub('#skF_4','#skE_6','#skE_9'),
inference(demodulation,[status(thm),theory(equality)],[c_15990,c_16076]) ).
tff(c_16122,plain,
~ $less('#skE_9','#skE_6'),
inference(resolution,[status(thm)],[c_16108,c_98]) ).
tff(c_16301,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_16300,c_16296,c_16122]) ).
tff(c_16304,plain,
$less('#skE_7','#skE_10'),
inference(splitRight,[status(thm)],[c_16265]) ).
tff(c_15883,plain,
'#skF_3'('#skF_4','#skE_6','#skF_6') = '#skE_8',
inference(define,[status(thm),theory(equality)],[c_15837]) ).
tff(c_15882,plain,
! [Z_6134a: $int] :
( $less('#skF_3'('#skF_4','#skE_6','#skF_6'),'#skF_6')
| $less('#skF_6',$sum(c,summation(Z_6134a)))
| $less(Z_6134a,'#skF_4')
| $less(Z_6134a,'#skE_6') ),
inference(resolution,[status(thm)],[c_15811,c_15210]) ).
tff(c_15893,plain,
! [Z_6134a: $int] :
( $less('#skE_8','#skF_6')
| $less('#skF_6',$sum(c,summation(Z_6134a)))
| $less(Z_6134a,'#skF_4')
| $less(Z_6134a,'#skE_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_15883,c_15882]) ).
tff(c_15929,plain,
$less('#skE_8','#skF_6'),
inference(splitLeft,[status(thm)],[c_15893]) ).
tff(c_15122,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_15120]) ).
tff(c_15121,plain,
! [N_5899a: $int] :
( ~ $less(N_5899a,'#skF_6')
| $less(N_5899a,$sum(c,summation('#skE_6'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_15079,c_15066]) ).
tff(c_15129,plain,
! [N_5899a: $int] :
( ~ $less(N_5899a,'#skF_6')
| $less(N_5899a,$sum(c,'#skE_7')) ),
inference(demodulation,[status(thm),theory(equality)],[c_15122,c_15121]) ).
tff(c_15280,plain,
$lesseq('#skF_6',$sum('#skE_7',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_15129]) ).
tff(c_15282,plain,
~ $less($sum(c,'#skE_7'),'#skF_6'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_15280]) ).
tff(c_16336,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_16304,c_16184,c_15929,c_15282]) ).
tff(c_16339,plain,
'#skE_7' = '#skE_10',
inference(splitRight,[status(thm)],[c_16292]) ).
tff(c_16431,plain,
! [N_5899a: $int] :
( ~ $less(N_5899a,'#skF_6')
| $less(N_5899a,$sum(c,'#skE_10')) ),
inference(demodulation,[status(thm),theory(equality)],[c_16339,c_15129]) ).
tff(c_16526,plain,
$lesseq('#skF_6',$sum('#skE_10',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_16431]) ).
tff(c_16528,plain,
~ $less($sum(c,'#skE_10'),'#skF_6'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_16526]) ).
tff(c_16529,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_16184,c_16528,c_15929]) ).
tff(c_16535,plain,
minsol_model_ub('#skF_4','#skE_6','#skF_6'),
inference(splitRight,[status(thm)],[c_15982]) ).
tff(c_16538,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_16535,c_15210]) ).
tff(c_16547,plain,
! [Z_6387a: $int] :
( $less('#skF_6',$sum(c,summation(Z_6387a)))
| $less(Z_6387a,'#skF_4')
| $less(Z_6387a,'#skE_6') ),
inference(splitRight,[status(thm)],[c_15893]) ).
tff(c_16556,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_4')
| $less('#skE_6','#skE_6') ),
inference(superposition,[status(thm),theory(equality)],[c_15128,c_16547]) ).
tff(c_16558,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_4') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_16556]) ).
tff(c_16559,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_15218,c_15473,c_16558]) ).
tff(c_16562,plain,
'#skF_4' = '#skE_6',
inference(splitRight,[status(thm)],[c_15103]) ).
tff(c_16563,plain,
~ $less('#skF_4','#skF_5'),
inference(splitRight,[status(thm)],[c_15103]) ).
tff(c_16600,plain,
~ $less('#skE_6','#skF_5'),
inference(demodulation,[status(thm),theory(equality)],[c_16562,c_16563]) ).
tff(c_15074,plain,
max('#skF_4','#skF_5') = '#skE_6',
inference(define,[status(thm),theory(equality)],[c_11073]) ).
tff(c_16630,plain,
max('#skE_6','#skF_5') = '#skE_6',
inference(demodulation,[status(thm),theory(equality)],[c_16562,c_15074]) ).
tff(c_16709,plain,
! [N_5899a: $int] :
( ~ $less(N_5899a,'#skF_6')
| $less(N_5899a,$sum(c,summation('#skE_6'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_16630,c_16562,c_15066]) ).
tff(c_16720,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_16709]) ).
tff(c_16814,plain,
~ $less('#skF_6',$sum(c,'#skE_7')),
inference(demodulation,[status(thm),theory(equality)],[c_16720,c_15077]) ).
tff(c_16717,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_16709]) ).
tff(c_16676,plain,
! [X_6436a: $int,Y_6438a: $int,N_6437a: $int,Z_6439a: $int] :
( model_ub(X_6436a,Y_6438a,N_6437a)
| $less(N_6437a,$sum(c,summation(Z_6439a)))
| $less(Z_6439a,X_6436a)
| $less(Z_6439a,Y_6438a) ),
inference(resolution,[status(thm)],[c_96,c_15053]) ).
tff(c_17347,plain,
! [X_6613a: $int,Y_6610a: $int,N_6611a: $int,Z_6612a: $int] :
( $less('#skF_3'(X_6613a,Y_6610a,N_6611a),N_6611a)
| minsol_model_ub(X_6613a,Y_6610a,N_6611a)
| $less(N_6611a,$sum(c,summation(Z_6612a)))
| $less(Z_6612a,X_6613a)
| $less(Z_6612a,Y_6610a) ),
inference(resolution,[status(thm)],[c_16676,c_72]) ).
tff(c_16592,plain,
~ minsol_model_ub('#skE_6','#skF_5','#skF_6'),
inference(demodulation,[status(thm),theory(equality)],[c_16562,c_15034]) ).
tff(c_17373,plain,
! [Z_6612a: $int] :
( $less('#skF_3'('#skE_6','#skF_5','#skF_6'),'#skF_6')
| $less('#skF_6',$sum(c,summation(Z_6612a)))
| $less(Z_6612a,'#skE_6')
| $less(Z_6612a,'#skF_5') ),
inference(resolution,[status(thm)],[c_17347,c_16592]) ).
tff(c_17569,plain,
'#skF_3'('#skE_6','#skF_5','#skF_6') = '#skE_11',
inference(define,[status(thm),theory(equality)],[c_17373]) ).
tff(c_17595,plain,
( model_ub('#skE_6','#skF_5','#skE_11')
| minsol_model_ub('#skE_6','#skF_5','#skF_6')
| ~ model_ub('#skE_6','#skF_5','#skF_6') ),
inference(superposition,[status(thm),theory(equality)],[c_17569,c_71]) ).
tff(c_17612,plain,
~ model_ub('#skE_6','#skF_5','#skF_6'),
inference(splitLeft,[status(thm)],[c_17595]) ).
tff(c_17630,plain,
! [Z_6761a: $int] :
( $less('#skF_6',$sum(c,summation(Z_6761a)))
| $less(Z_6761a,'#skE_6')
| $less(Z_6761a,'#skF_5') ),
inference(resolution,[status(thm)],[c_15059,c_17612]) ).
tff(c_17639,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skE_6')
| $less('#skE_6','#skF_5') ),
inference(superposition,[status(thm),theory(equality)],[c_16717,c_17630]) ).
tff(c_17641,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_5') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_17639]) ).
tff(c_17651,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16600,c_16814,c_17641]) ).
tff(c_17655,plain,
( minsol_model_ub('#skE_6','#skF_5','#skF_6')
| model_ub('#skE_6','#skF_5','#skE_11') ),
inference(splitRight,[status(thm)],[c_17595]) ).
tff(c_17664,plain,
model_ub('#skE_6','#skF_5','#skE_11'),
inference(splitLeft,[status(thm)],[c_17655]) ).
tff(c_17676,plain,
~ $less('#skE_11',$sum(c,summation('#skF_1'('#skE_6','#skF_5','#skE_11')))),
inference(resolution,[status(thm)],[c_17664,c_83]) ).
tff(c_17705,plain,
'#skF_1'('#skE_6','#skF_5','#skE_11') = '#skE_12',
inference(define,[status(thm),theory(equality)],[c_17676]) ).
tff(c_17704,plain,
~ $less('#skE_11',$sum(c,summation('#skF_1'('#skE_6','#skF_5','#skE_11')))),
inference(resolution,[status(thm)],[c_17664,c_83]) ).
tff(c_17715,plain,
~ $less('#skE_11',$sum(c,summation('#skE_12'))),
inference(demodulation,[status(thm),theory(equality)],[c_17705,c_17704]) ).
tff(c_17860,plain,
summation('#skE_12') = '#skE_14',
inference(define,[status(thm),theory(equality)],[c_17715]) ).
tff(c_16721,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_16709]) ).
tff(c_16749,plain,
! [X_1a: $int] :
( $less('#skE_7',summation(X_1a))
| ~ $less('#skE_6',X_1a) ),
inference(superposition,[status(thm),theory(equality)],[c_16721,c_101]) ).
tff(c_17950,plain,
( $less('#skE_7','#skE_14')
| ~ $less('#skE_6','#skE_12') ),
inference(superposition,[status(thm),theory(equality)],[c_17860,c_16749]) ).
tff(c_17979,plain,
~ $less('#skE_6','#skE_12'),
inference(splitLeft,[status(thm)],[c_17950]) ).
tff(c_17952,plain,
( ( '#skE_7' = '#skE_14' )
| ( '#skE_6' != '#skE_12' ) ),
inference(superposition,[status(thm),theory(equality)],[c_17860,c_16717]) ).
tff(c_17975,plain,
'#skE_6' != '#skE_12',
inference(splitLeft,[status(thm)],[c_17952]) ).
tff(c_17663,plain,
model_ub('#skE_6','#skF_5','#skE_11'),
inference(splitLeft,[status(thm)],[c_17655]) ).
tff(c_17731,plain,
'#skF_1'('#skE_6','#skF_5','#skE_11') = '#skE_12',
inference(define,[status(thm),theory(equality)],[c_17676]) ).
tff(c_17749,plain,
( ub('#skE_6','#skF_5','#skE_12')
| ~ model_ub('#skE_6','#skF_5','#skE_11') ),
inference(superposition,[status(thm),theory(equality)],[c_17731,c_79]) ).
tff(c_17781,plain,
ub('#skE_6','#skF_5','#skE_12'),
inference(demodulation,[status(thm),theory(equality)],[c_17663,c_17749]) ).
tff(c_17797,plain,
~ $less('#skE_12','#skE_6'),
inference(resolution,[status(thm)],[c_17781,c_97]) ).
tff(c_17980,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_17979,c_17975,c_17797]) ).
tff(c_17983,plain,
$less('#skE_7','#skE_14'),
inference(splitRight,[status(thm)],[c_17950]) ).
tff(c_17850,plain,
summation('#skE_12') = '#skE_14',
inference(define,[status(thm),theory(equality)],[c_17715]) ).
tff(c_17849,plain,
~ $less('#skE_11',$sum(c,summation('#skE_12'))),
inference(demodulation,[status(thm),theory(equality)],[c_17705,c_17704]) ).
tff(c_17857,plain,
~ $less('#skE_11',$sum(c,'#skE_14')),
inference(demodulation,[status(thm),theory(equality)],[c_17850,c_17849]) ).
tff(c_17556,plain,
'#skF_3'('#skE_6','#skF_5','#skF_6') = '#skE_11',
inference(define,[status(thm),theory(equality)],[c_17373]) ).
tff(c_17555,plain,
! [Z_6612a: $int] :
( $less('#skF_3'('#skE_6','#skF_5','#skF_6'),'#skF_6')
| $less('#skF_6',$sum(c,summation(Z_6612a)))
| $less(Z_6612a,'#skE_6')
| $less(Z_6612a,'#skF_5') ),
inference(resolution,[status(thm)],[c_17347,c_16592]) ).
tff(c_17566,plain,
! [Z_6612a: $int] :
( $less('#skE_11','#skF_6')
| $less('#skF_6',$sum(c,summation(Z_6612a)))
| $less(Z_6612a,'#skE_6')
| $less(Z_6612a,'#skF_5') ),
inference(demodulation,[status(thm),theory(equality)],[c_17556,c_17555]) ).
tff(c_17602,plain,
$less('#skE_11','#skF_6'),
inference(splitLeft,[status(thm)],[c_17566]) ).
tff(c_16711,plain,
summation('#skE_6') = '#skE_7',
inference(define,[status(thm),theory(equality)],[c_16709]) ).
tff(c_16710,plain,
! [N_5899a: $int] :
( ~ $less(N_5899a,'#skF_6')
| $less(N_5899a,$sum(c,summation('#skE_6'))) ),
inference(demodulation,[status(thm),theory(equality)],[c_16630,c_16562,c_15066]) ).
tff(c_16718,plain,
! [N_5899a: $int] :
( ~ $less(N_5899a,'#skF_6')
| $less(N_5899a,$sum(c,'#skE_7')) ),
inference(demodulation,[status(thm),theory(equality)],[c_16711,c_16710]) ).
tff(c_16762,plain,
$lesseq('#skF_6',$sum('#skE_7',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_16718]) ).
tff(c_16764,plain,
~ $less($sum(c,'#skE_7'),'#skF_6'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_16762]) ).
tff(c_17985,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_17983,c_17857,c_17602,c_16764]) ).
tff(c_17988,plain,
'#skE_7' = '#skE_14',
inference(splitRight,[status(thm)],[c_17952]) ).
tff(c_18057,plain,
! [N_5899a: $int] :
( ~ $less(N_5899a,'#skF_6')
| $less(N_5899a,$sum(c,'#skE_14')) ),
inference(demodulation,[status(thm),theory(equality)],[c_17988,c_16718]) ).
tff(c_18305,plain,
$lesseq('#skF_6',$sum('#skE_14',c)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_18057]) ).
tff(c_18307,plain,
~ $less($sum(c,'#skE_14'),'#skF_6'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_18305]) ).
tff(c_18308,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_18307,c_17857,c_17602]) ).
tff(c_18314,plain,
minsol_model_ub('#skE_6','#skF_5','#skF_6'),
inference(splitRight,[status(thm)],[c_17655]) ).
tff(c_18317,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_18314,c_16592]) ).
tff(c_18326,plain,
! [Z_7038a: $int] :
( $less('#skF_6',$sum(c,summation(Z_7038a)))
| $less(Z_7038a,'#skE_6')
| $less(Z_7038a,'#skF_5') ),
inference(splitRight,[status(thm)],[c_17566]) ).
tff(c_18335,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skE_6')
| $less('#skE_6','#skF_5') ),
inference(superposition,[status(thm),theory(equality)],[c_16717,c_18326]) ).
tff(c_18337,plain,
( $less('#skF_6',$sum(c,'#skE_7'))
| $less('#skE_6','#skF_5') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_18335]) ).
tff(c_18338,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_16600,c_16814,c_18337]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NUM862_1 : TPTP v9.0.0. Released v4.1.0.
% 0.06/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 : n020.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 15:36:34 EDT 2025
% 0.13/0.34 % CPUTime :
% 14.27/4.43 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.10/4.62
% 15.10/4.62 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------