%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWW634_2 : TPTP v9.0.0. Released v6.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 : n023.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 09:53:06 PM UTC 2025
% Result : Theorem 190.72s 133.08s
% Output : CNFRefutation 190.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 4
% Syntax : Number of formulae : 258 ( 91 unt; 0 typ; 0 def)
% Number of atoms : 654 ( 64 equ)
% Maximal formula atoms : 40 ( 2 avg)
% Number of connectives : 716 ( 320 ~; 354 |; 27 &)
% ( 6 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 763 ( 315 atm; 46 fun; 339 num; 63 var)
% Number of types : 9 ( 7 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 13 ( 9 usr; 1 prp; 0-4 aty)
% Number of functors : 104 ( 101 usr; 58 con; 0-5 aty)
% Number of variables : 143 ( 141 !; 2 ?; 143 :)
% Comments :
%------------------------------------------------------------------------------
%$ eq_prefix1 > subset > sorted1 > mem > infix_eqeq > sort1 > partial_solution1 > lt_sol1 > is_empty > set1 > match_bool1 > get > union > remove > inter > diff > const > add > mk_ref > map > contents > choose > cardinal1 > #nlpp > witness1 > tb2t3 > tb2t2 > tb2t1 > tb2t > t2tb3 > t2tb2 > t2tb1 > t2tb > succ1 > set > ref > pred1 > min_elt1 > max_elt1 > empty > below1 > tuple03 > tuple0 > true1 > real > qtmark > int > false1 > bool > #skF_19 > #skF_5 > #skF_22 > #skF_15 > #skF_6 > #skF_9 > #skF_14 > #skF_17 > #skF_23 > #skF_12 > #skF_8 > #skF_1 > #skF_16 > #skF_4 > #skF_3 > #skF_21 > #skF_7 > #skF_2 > #skF_25
%Foreground sorts:
tff(set_int,type,
set_int: $tType ).
tff(map_int_lpmap_int_intrp,type,
map_int_lpmap_int_intrp: $tType ).
tff(map_int_int,type,
map_int_int: $tType ).
tff(tuple02,type,
tuple02: $tType ).
tff(bool1,type,
bool1: $tType ).
tff(ty,type,
ty: $tType ).
tff(uni,type,
uni: $tType ).
%Background operators:
tff('#skE_7',type,
'#skE_7': $int ).
tff('#skE_21',type,
'#skE_21': $int ).
tff('#skE_30',type,
'#skE_30': $int ).
tff('#skE_11',type,
'#skE_11': $int ).
tff('#skE_25',type,
'#skE_25': $int ).
tff('#skE_28',type,
'#skE_28': $int ).
tff('#skE_23',type,
'#skE_23': $int ).
tff('#skE_12',type,
'#skE_12': $int ).
tff('#skF_13',type,
'#skF_13': $int ).
tff('#skE_2',type,
'#skE_2': $int ).
tff('#skE_1',type,
'#skE_1': $int ).
tff('#skE_33',type,
'#skE_33': $int ).
tff('#skF_11',type,
'#skF_11': $int ).
tff('#skE_20',type,
'#skE_20': $int ).
tff('#skF_20',type,
'#skF_20': $int ).
tff('#skE_6',type,
'#skE_6': $int ).
tff('#skE_13',type,
'#skE_13': $int ).
tff('#skE_26',type,
'#skE_26': $int ).
tff('#skE_32',type,
'#skE_32': $int ).
tff('#skE_10',type,
'#skE_10': $int ).
tff('#skE_24',type,
'#skE_24': $int ).
tff('#skE_5',type,
'#skE_5': $int ).
tff('#skF_24',type,
'#skF_24': $int ).
tff('#skF_18',type,
'#skF_18': $int ).
tff('#skE_31',type,
'#skE_31': $int ).
tff('#skE_15',type,
'#skE_15': $int ).
tff('#skE_8',type,
'#skE_8': $int ).
tff('#skE_36',type,
'#skE_36': $int ).
tff('#skE_4',type,
'#skE_4': $int ).
tff('#skF_10',type,
'#skF_10': $int ).
tff('#skE_22',type,
'#skE_22': $int ).
tff('#skE_16',type,
'#skE_16': $int ).
tff('#skE_17',type,
'#skE_17': $int ).
tff('#skE_3',type,
'#skE_3': $int ).
tff('#skE_9',type,
'#skE_9': $int ).
tff('#skE_29',type,
'#skE_29': $int ).
tff('#skE_34',type,
'#skE_34': $int ).
tff('#skE_27',type,
'#skE_27': $int ).
tff(n1,type,
n1: $int ).
tff('#skE_18',type,
'#skE_18': $int ).
tff('#skE_35',type,
'#skE_35': $int ).
tff('#skE_19',type,
'#skE_19': $int ).
tff('#skE_14',type,
'#skE_14': $int ).
%Foreground operators:
tff(diff,type,
diff: ( ty * uni * uni ) > uni ).
tff('#skF_19',type,
'#skF_19': map_int_lpmap_int_intrp ).
tff('#skF_5',type,
'#skF_5': ( $int * map_int_int ) > $int ).
tff(t2tb1,type,
t2tb1: $int > uni ).
tff('#skF_22',type,
'#skF_22': map_int_int > $int ).
tff(true1,type,
true1: bool1 ).
tff(add,type,
add: ( ty * uni * uni ) > uni ).
tff(set,type,
set: ty > ty ).
tff(const,type,
const: ( ty * ty * uni ) > uni ).
tff(t2tb3,type,
t2tb3: map_int_lpmap_int_intrp > uni ).
tff('#skF_15',type,
'#skF_15': $int > $int ).
tff(empty,type,
empty: ty > uni ).
tff(int,type,
int: ty ).
tff(tb2t,type,
tb2t: uni > set_int ).
tff(false1,type,
false1: bool1 ).
tff('#skF_6',type,
'#skF_6': ( $int * map_int_int ) > $int ).
tff('#skF_9',type,
'#skF_9': ( map_int_lpmap_int_intrp * $int * $int ) > $int ).
tff(sort1,type,
sort1: ( ty * uni ) > $o ).
tff('#skF_14',type,
'#skF_14': map_int_int ).
tff(contents,type,
contents: ( ty * uni ) > uni ).
tff(tb2t1,type,
tb2t1: uni > $int ).
tff(lt_sol1,type,
lt_sol1: ( map_int_int * map_int_int ) > $o ).
tff('#skF_17',type,
'#skF_17': $int > $int ).
tff(witness1,type,
witness1: ty > uni ).
tff(real,type,
real: ty ).
tff(pred1,type,
pred1: set_int > set_int ).
tff(union,type,
union: ( ty * uni * uni ) > uni ).
tff(subset,type,
subset: ( ty * uni * uni ) > $o ).
tff(match_bool1,type,
match_bool1: ( ty * bool1 * uni * uni ) > uni ).
tff(choose,type,
choose: ( ty * uni ) > uni ).
tff('#skF_23',type,
'#skF_23': map_int_int ).
tff(tb2t2,type,
tb2t2: uni > map_int_int ).
tff(tuple0,type,
tuple0: ty ).
tff(qtmark,type,
qtmark: ty ).
tff(min_elt1,type,
min_elt1: set_int > $int ).
tff(eq_prefix1,type,
eq_prefix1: ( ty * uni * uni * $int ) > $o ).
tff(t2tb2,type,
t2tb2: map_int_int > uni ).
tff('#skF_12',type,
'#skF_12': map_int_lpmap_int_intrp ).
tff(bool,type,
bool: ty ).
tff(get,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(t2tb,type,
t2tb: set_int > uni ).
tff(partial_solution1,type,
partial_solution1: ( $int * map_int_int ) > $o ).
tff('#skF_8',type,
'#skF_8': ( map_int_lpmap_int_intrp * $int * $int ) > $int ).
tff(max_elt1,type,
max_elt1: set_int > $int ).
tff(below1,type,
below1: $int > set_int ).
tff('#skF_1',type,
'#skF_1': ( ty * uni * uni ) > uni ).
tff(tuple03,type,
tuple03: tuple02 ).
tff(succ1,type,
succ1: set_int > set_int ).
tff(map,type,
map: ( ty * ty ) > ty ).
tff('#skF_16',type,
'#skF_16': $int > $int ).
tff(set1,type,
set1: ( ty * ty * uni * uni * uni ) > uni ).
tff('#skF_4',type,
'#skF_4': ( ty * uni * uni * $int ) > $int ).
tff(infix_eqeq,type,
infix_eqeq: ( ty * uni * uni ) > $o ).
tff(ref,type,
ref: ty > ty ).
tff(cardinal1,type,
cardinal1: ( ty * uni ) > $int ).
tff('#skF_3',type,
'#skF_3': ( ty * uni ) > uni ).
tff(mem,type,
mem: ( ty * uni * uni ) > $o ).
tff(is_empty,type,
is_empty: ( ty * uni ) > $o ).
tff(sorted1,type,
sorted1: ( map_int_lpmap_int_intrp * $int * $int ) > $o ).
tff(inter,type,
inter: ( ty * uni * uni ) > uni ).
tff('#skF_21',type,
'#skF_21': map_int_int ).
tff('#skF_7',type,
'#skF_7': ( map_int_int * map_int_int ) > $int ).
tff(tb2t3,type,
tb2t3: uni > map_int_lpmap_int_intrp ).
tff('#skF_2',type,
'#skF_2': ( ty * uni * uni ) > uni ).
tff('#skF_25',type,
'#skF_25': map_int_int ).
tff(remove,type,
remove: ( ty * uni * uni ) > uni ).
tff(mk_ref,type,
mk_ref: ( ty * uni ) > uni ).
tff(f_508,negated_conjecture,
~ ! [Qa: $int,Sa: $int,Sol: map_int_lpmap_int_intrp,Ka: $int,Col: map_int_int] :
( ( $lesseq(0,Qa)
& ( Qa = n1 )
& ( Sa = 0 )
& ( Ka = 0 ) )
=> ( ( $lesseq(0,Ka)
& ( $sum(Ka,cardinal1(int,t2tb(below1(Qa)))) = n1 )
& $lesseq(0,Sa)
& ! [Ia: $int] :
( mem(int,t2tb1(Ia),t2tb(below1(Qa)))
<=> ( $lesseq(0,Ia)
& $less(Ia,n1)
& ! [Ja: $int] :
( ( $lesseq(0,Ja)
& $less(Ja,Ka) )
=> ( tb2t1(get(int,int,t2tb2(Col),t2tb1(Ja))) != Ia ) ) ) )
& ! [Ia: $int] :
( $lesseq(0,Ia)
=> ( ~ mem(int,t2tb1(Ia),empty(int))
<=> ! [Ja: $int] :
( ( $lesseq(0,Ja)
& $less(Ja,Ka) )
=> ( tb2t1(get(int,int,t2tb2(Col),t2tb1(Ja))) != $difference($sum(Ia,Ja),Ka) ) ) ) )
& ! [Ia: $int] :
( $lesseq(0,Ia)
=> ( ~ mem(int,t2tb1(Ia),empty(int))
<=> ! [Ja: $int] :
( ( $lesseq(0,Ja)
& $less(Ja,Ka) )
=> ( tb2t1(get(int,int,t2tb2(Col),t2tb1(Ja))) != $difference($sum(Ia,Ka),Ja) ) ) ) )
& partial_solution1(Ka,Col) )
=> ! [S1a: $int,Sol1: map_int_lpmap_int_intrp,K1a: $int,Col1: map_int_int] :
( ( $lesseq(0,$difference(S1a,Sa))
& ( K1a = Ka )
& sorted1(Sol1,Sa,S1a)
& ! [T: map_int_int] :
( ( partial_solution1(n1,T)
& eq_prefix1(int,t2tb2(Col1),t2tb2(T),K1a) )
<=> ? [Ia: $int] :
( $lesseq(Sa,Ia)
& $less(Ia,S1a)
& eq_prefix1(int,t2tb2(T),get(map(int,int),int,t2tb3(Sol1),t2tb1(Ia)),n1) ) )
& eq_prefix1(int,t2tb2(Col),t2tb2(Col1),K1a)
& eq_prefix1(map(int,int),t2tb3(Sol),t2tb3(Sol1),Sa) )
=> ( ( $difference(S1a,Sa) = S1a )
& sorted1(Sol1,0,S1a)
& ! [T: map_int_int] :
( partial_solution1(n1,T)
<=> ? [Ia: $int] :
( $lesseq(0,Ia)
& $less(Ia,$difference(S1a,Sa))
& eq_prefix1(int,t2tb2(T),get(map(int,int),int,t2tb3(Sol1),t2tb1(Ia)),n1) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_queens3) ).
tff(f_338,axiom,
! [I: map_int_int] : ( tb2t2(t2tb2(I)) = I ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeL2) ).
tff(f_334,axiom,
! [A: ty,T: uni,U: uni,Ia: $int] :
( eq_prefix1(A,T,U,Ia)
<=> ! [Ka: $int] :
( ( $lesseq(0,Ka)
& $less(Ka,Ia) )
=> ( get(A,int,T,t2tb1(Ka)) = get(A,int,U,t2tb1(Ka)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq_prefix_def) ).
tff(f_340,axiom,
! [J: uni] : ( t2tb2(tb2t2(J)) = J ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR2) ).
tff(c_461,plain,
'#skF_11' = 0,
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_350955,plain,
sorted1('#skF_19','#skF_11','#skF_18'),
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_351082,plain,
sorted1('#skF_19',0,'#skF_18'),
inference(demodulation,[status(thm),theory(equality)],[c_461,c_350955]) ).
tff(c_460,plain,
n1 = '#skF_10',
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_297,plain,
( partial_solution1(n1,'#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( $difference('#skF_18','#skF_11') != '#skF_18' )
| $lesseq(0,'#skF_24') ),
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_619,plain,
( partial_solution1(n1,'#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| ~ $less('#skF_24',0) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_297]) ).
tff(c_350967,plain,
( partial_solution1('#skF_10','#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| ~ $less('#skF_24',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_460,c_619]) ).
tff(c_351008,plain,
( partial_solution1('#skF_10','#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18')
| ~ $less('#skF_24',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_461,c_350967]) ).
tff(c_351091,plain,
( partial_solution1('#skF_10','#skF_25')
| ~ $less('#skF_24',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_351082,c_351008]) ).
tff(c_351285,plain,
~ $less('#skF_24',0),
inference(splitLeft,[status(thm)],[c_351091]) ).
tff(c_291,plain,
( ~ partial_solution1(n1,'#skF_23')
| partial_solution1(n1,'#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( $difference('#skF_18','#skF_11') != '#skF_18' ) ),
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_625,plain,
( ~ partial_solution1(n1,'#skF_23')
| partial_solution1(n1,'#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 ) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_291]) ).
tff(c_350973,plain,
( ~ partial_solution1('#skF_10','#skF_23')
| partial_solution1('#skF_10','#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_460,c_460,c_625]) ).
tff(c_351005,plain,
( ~ partial_solution1('#skF_10','#skF_23')
| partial_solution1('#skF_10','#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_461,c_350973]) ).
tff(c_351085,plain,
( ~ partial_solution1('#skF_10','#skF_23')
| partial_solution1('#skF_10','#skF_25') ),
inference(demodulation,[status(thm),theory(equality)],[c_351082,c_351005]) ).
tff(c_351270,plain,
~ partial_solution1('#skF_10','#skF_23'),
inference(splitLeft,[status(thm)],[c_351085]) ).
tff(c_295,plain,
( partial_solution1(n1,'#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( $difference('#skF_18','#skF_11') != '#skF_18' )
| $less('#skF_24',$difference('#skF_18','#skF_11')) ),
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_621,plain,
( partial_solution1(n1,'#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| $less($sum('#skF_24','#skF_11'),'#skF_18') ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_295]) ).
tff(c_350984,plain,
( partial_solution1('#skF_10','#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| $less($sum('#skF_24','#skF_11'),'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_460,c_621]) ).
tff(c_350986,plain,
( partial_solution1('#skF_10','#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| $less($sum('#skF_11','#skF_24'),'#skF_18') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_350984]) ).
tff(c_351010,plain,
( partial_solution1('#skF_10','#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18')
| $less($sum(0,'#skF_24'),'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_461,c_461,c_350986]) ).
tff(c_351012,plain,
( partial_solution1('#skF_10','#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18')
| $less('#skF_24','#skF_18') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_351010]) ).
tff(c_351088,plain,
( partial_solution1('#skF_10','#skF_25')
| $less('#skF_24','#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_351082,c_351012]) ).
tff(c_351278,plain,
$less('#skF_24','#skF_18'),
inference(splitLeft,[status(thm)],[c_351088]) ).
tff(c_201,plain,
! [I_182: map_int_int] : ( tb2t2(t2tb2(I_182)) = I_182 ),
inference(cnfTransformation,[status(thm)],[f_338]) ).
tff(c_293,plain,
( eq_prefix1(int,t2tb2('#skF_23'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_24')),n1)
| partial_solution1(n1,'#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( $difference('#skF_18','#skF_11') != '#skF_18' ) ),
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_623,plain,
( eq_prefix1(int,t2tb2('#skF_23'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_24')),n1)
| partial_solution1(n1,'#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 ) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_293]) ).
tff(c_350988,plain,
( eq_prefix1(int,t2tb2('#skF_23'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_24')),'#skF_10')
| partial_solution1('#skF_10','#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_460,c_460,c_623]) ).
tff(c_351021,plain,
( eq_prefix1(int,t2tb2('#skF_23'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_24')),'#skF_10')
| partial_solution1('#skF_10','#skF_25')
| ~ sorted1('#skF_19',0,'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_461,c_350988]) ).
tff(c_351094,plain,
( eq_prefix1(int,t2tb2('#skF_23'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_24')),'#skF_10')
| partial_solution1('#skF_10','#skF_25') ),
inference(demodulation,[status(thm),theory(equality)],[c_351082,c_351021]) ).
tff(c_351836,plain,
partial_solution1('#skF_10','#skF_25'),
inference(splitLeft,[status(thm)],[c_351094]) ).
tff(c_196,plain,
! [A_174: ty,T_175: uni,U_176: uni,I_177a: $int] :
( $lesseq(0,'#skF_4'(A_174,T_175,U_176,I_177a))
| eq_prefix1(A_174,T_175,U_176,I_177a) ),
inference(cnfTransformation,[status(thm)],[f_334]) ).
tff(c_353472,plain,
! [A_39029: ty,T_39030: uni,U_39031: uni,I_39032a: $int] :
( ~ $less('#skF_4'(A_39029,T_39030,U_39031,I_39032a),0)
| eq_prefix1(A_39029,T_39030,U_39031,I_39032a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_196]) ).
tff(c_462,plain,
'#skF_13' = 0,
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_474,plain,
'#skF_20' = '#skF_13',
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_351072,plain,
'#skF_20' = 0,
inference(demodulation,[status(thm),theory(equality)],[c_462,c_474]) ).
tff(c_615,plain,
! [T_284: map_int_int] :
( $less('#skF_22'(T_284),'#skF_18')
| ~ eq_prefix1(int,t2tb2('#skF_21'),t2tb2(T_284),'#skF_20')
| ~ partial_solution1(n1,T_284) ),
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_350971,plain,
! [T_284: map_int_int] :
( $less('#skF_22'(T_284),'#skF_18')
| ~ eq_prefix1(int,t2tb2('#skF_21'),t2tb2(T_284),'#skF_20')
| ~ partial_solution1('#skF_10',T_284) ),
inference(demodulation,[status(thm),theory(equality)],[c_460,c_615]) ).
tff(c_351074,plain,
! [T_284: map_int_int] :
( $less('#skF_22'(T_284),'#skF_18')
| ~ eq_prefix1(int,t2tb2('#skF_21'),t2tb2(T_284),0)
| ~ partial_solution1('#skF_10',T_284) ),
inference(demodulation,[status(thm),theory(equality)],[c_351072,c_350971]) ).
tff(c_353615,plain,
! [T_39043: map_int_int] :
( $less('#skF_22'(T_39043),'#skF_18')
| ~ partial_solution1('#skF_10',T_39043)
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_39043),0),0) ),
inference(resolution,[status(thm)],[c_353472,c_351074]) ).
tff(c_353630,plain,
( $less('#skF_22'('#skF_25'),'#skF_18')
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(resolution,[status(thm)],[c_351836,c_353615]) ).
tff(c_354062,plain,
'#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0) = '#skE_26',
inference(define,[status(thm),theory(equality)],[c_353630]) ).
tff(c_354061,plain,
'#skF_22'('#skF_25') = '#skE_25',
inference(define,[status(thm),theory(equality)],[c_353630]) ).
tff(c_354067,plain,
( $less('#skE_25','#skF_18')
| ~ $less('#skE_26',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_354062,c_354061,c_353630]) ).
tff(c_354093,plain,
~ $less('#skE_26',0),
inference(splitLeft,[status(thm)],[c_354067]) ).
tff(c_354066,plain,
'#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0) = '#skE_26',
inference(define,[status(thm),theory(equality)],[c_353630]) ).
tff(c_354065,plain,
'#skF_22'('#skF_25') = '#skE_25',
inference(define,[status(thm),theory(equality)],[c_353630]) ).
tff(c_353256,plain,
! [A_39000: ty,T_39001: uni,U_39002: uni,I_39003a: $int] :
( $less('#skF_4'(A_39000,T_39001,U_39002,I_39003a),I_39003a)
| eq_prefix1(A_39000,T_39001,U_39002,I_39003a) ),
inference(cnfTransformation,[status(thm)],[f_334]) ).
tff(c_304,plain,
! [T_284: map_int_int] :
( $lesseq('#skF_11','#skF_22'(T_284))
| ~ eq_prefix1(int,t2tb2('#skF_21'),t2tb2(T_284),'#skF_20')
| ~ partial_solution1(n1,T_284) ),
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_613,plain,
! [T_284: map_int_int] :
( ~ $less('#skF_22'(T_284),'#skF_11')
| ~ eq_prefix1(int,t2tb2('#skF_21'),t2tb2(T_284),'#skF_20')
| ~ partial_solution1(n1,T_284) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_304]) ).
tff(c_350969,plain,
! [T_284: map_int_int] :
( ~ $less('#skF_22'(T_284),'#skF_11')
| ~ eq_prefix1(int,t2tb2('#skF_21'),t2tb2(T_284),'#skF_20')
| ~ partial_solution1('#skF_10',T_284) ),
inference(demodulation,[status(thm),theory(equality)],[c_460,c_613]) ).
tff(c_351014,plain,
! [T_284: map_int_int] :
( ~ $less('#skF_22'(T_284),0)
| ~ eq_prefix1(int,t2tb2('#skF_21'),t2tb2(T_284),'#skF_20')
| ~ partial_solution1('#skF_10',T_284) ),
inference(demodulation,[status(thm),theory(equality)],[c_461,c_350969]) ).
tff(c_351076,plain,
! [T_284: map_int_int] :
( ~ $less('#skF_22'(T_284),0)
| ~ eq_prefix1(int,t2tb2('#skF_21'),t2tb2(T_284),0)
| ~ partial_solution1('#skF_10',T_284) ),
inference(demodulation,[status(thm),theory(equality)],[c_351072,c_351014]) ).
tff(c_359641,plain,
! [T_39476: map_int_int] :
( ~ $less('#skF_22'(T_39476),0)
| ~ partial_solution1('#skF_10',T_39476)
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_39476),0),0) ),
inference(resolution,[status(thm)],[c_353256,c_351076]) ).
tff(c_359653,plain,
( ~ $less('#skF_22'('#skF_25'),0)
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(resolution,[status(thm)],[c_351836,c_359641]) ).
tff(c_359666,plain,
( ~ $less('#skE_25',0)
| $less('#skE_26',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_354066,c_354065,c_359653]) ).
tff(c_359668,plain,
~ $less('#skE_25',0),
inference(negUnitSimplification,[status(thm)],[c_354093,c_359666]) ).
tff(c_353327,plain,
! [T_39008: map_int_int] :
( $less('#skF_22'(T_39008),'#skF_18')
| ~ partial_solution1('#skF_10',T_39008)
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_39008),0),0) ),
inference(resolution,[status(thm)],[c_353256,c_351074]) ).
tff(c_353342,plain,
( $less('#skF_22'('#skF_25'),'#skF_18')
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(resolution,[status(thm)],[c_351836,c_353327]) ).
tff(c_354279,plain,
( $less('#skE_25','#skF_18')
| $less('#skE_26',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_354066,c_354065,c_353342]) ).
tff(c_354281,plain,
$less('#skE_25','#skF_18'),
inference(negUnitSimplification,[status(thm)],[c_354093,c_354279]) ).
tff(c_617,plain,
! [T_284: map_int_int] :
( eq_prefix1(int,t2tb2(T_284),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_22'(T_284))),n1)
| ~ eq_prefix1(int,t2tb2('#skF_21'),t2tb2(T_284),'#skF_20')
| ~ partial_solution1(n1,T_284) ),
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_350983,plain,
! [T_284: map_int_int] :
( eq_prefix1(int,t2tb2(T_284),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_22'(T_284))),'#skF_10')
| ~ eq_prefix1(int,t2tb2('#skF_21'),t2tb2(T_284),'#skF_20')
| ~ partial_solution1('#skF_10',T_284) ),
inference(demodulation,[status(thm),theory(equality)],[c_460,c_460,c_617]) ).
tff(c_351080,plain,
! [T_284: map_int_int] :
( eq_prefix1(int,t2tb2(T_284),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_22'(T_284))),'#skF_10')
| ~ eq_prefix1(int,t2tb2('#skF_21'),t2tb2(T_284),0)
| ~ partial_solution1('#skF_10',T_284) ),
inference(demodulation,[status(thm),theory(equality)],[c_351072,c_350983]) ).
tff(c_353303,plain,
! [T_284: map_int_int] :
( eq_prefix1(int,t2tb2(T_284),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_22'(T_284))),'#skF_10')
| ~ partial_solution1('#skF_10',T_284)
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_284),0),0) ),
inference(resolution,[status(thm)],[c_353256,c_351080]) ).
tff(c_354074,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| ~ partial_solution1('#skF_10','#skF_25')
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(superposition,[status(thm),theory(equality)],[c_354065,c_353303]) ).
tff(c_354083,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(demodulation,[status(thm),theory(equality)],[c_351836,c_354074]) ).
tff(c_375903,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| $less('#skE_26',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_354066,c_354083]) ).
tff(c_375905,plain,
eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10'),
inference(negUnitSimplification,[status(thm)],[c_354093,c_375903]) ).
tff(c_285,plain,
! [I_290a: $int] :
( eq_prefix1(int,t2tb2('#skF_23'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_24')),n1)
| ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),n1)
| ~ sorted1('#skF_19',0,'#skF_18')
| ( $difference('#skF_18','#skF_11') != '#skF_18' )
| ~ $lesseq(0,I_290a)
| ~ $less(I_290a,$difference('#skF_18','#skF_11')) ),
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_631,plain,
! [I_290a: $int] :
( eq_prefix1(int,t2tb2('#skF_23'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_24')),n1)
| ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),n1)
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| $less(I_290a,0)
| ~ $less($sum(I_290a,'#skF_11'),'#skF_18') ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_285]) ).
tff(c_350997,plain,
! [I_290a: $int] :
( eq_prefix1(int,t2tb2('#skF_23'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_24')),'#skF_10')
| ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| $less(I_290a,0)
| ~ $less($sum(I_290a,'#skF_11'),'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_460,c_460,c_631]) ).
tff(c_350999,plain,
! [I_290a: $int] :
( eq_prefix1(int,t2tb2('#skF_23'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_24')),'#skF_10')
| ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| $less(I_290a,0)
| ~ $less($sum('#skF_11',I_290a),'#skF_18') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_350997]) ).
tff(c_351031,plain,
! [I_290a: $int] :
( eq_prefix1(int,t2tb2('#skF_23'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_24')),'#skF_10')
| ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| ~ sorted1('#skF_19',0,'#skF_18')
| $less(I_290a,0)
| ~ $less($sum(0,I_290a),'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_461,c_461,c_350999]) ).
tff(c_351033,plain,
! [I_290a: $int] :
( eq_prefix1(int,t2tb2('#skF_23'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_24')),'#skF_10')
| ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| ~ sorted1('#skF_19',0,'#skF_18')
| $less(I_290a,0)
| ~ $less(I_290a,'#skF_18') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_351031]) ).
tff(c_351103,plain,
! [I_290a: $int] :
( eq_prefix1(int,t2tb2('#skF_23'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_24')),'#skF_10')
| ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| $less(I_290a,0)
| ~ $less(I_290a,'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_351082,c_351033]) ).
tff(c_365684,plain,
eq_prefix1(int,t2tb2('#skF_23'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_24')),'#skF_10'),
inference(splitLeft,[status(thm)],[c_351103]) ).
tff(c_203,plain,
! [J_183: uni] : ( t2tb2(tb2t2(J_183)) = J_183 ),
inference(cnfTransformation,[status(thm)],[f_340]) ).
tff(c_308,plain,
! [T_284: map_int_int,I_287a: $int] :
( partial_solution1(n1,T_284)
| ~ eq_prefix1(int,t2tb2(T_284),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_287a)),n1)
| ~ $lesseq('#skF_11',I_287a)
| ~ $less(I_287a,'#skF_18') ),
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_609,plain,
! [T_284: map_int_int,I_287a: $int] :
( partial_solution1(n1,T_284)
| ~ eq_prefix1(int,t2tb2(T_284),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_287a)),n1)
| $less(I_287a,'#skF_11')
| ~ $less(I_287a,'#skF_18') ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_308]) ).
tff(c_350977,plain,
! [T_284: map_int_int,I_287a: $int] :
( partial_solution1('#skF_10',T_284)
| ~ eq_prefix1(int,t2tb2(T_284),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_287a)),'#skF_10')
| $less(I_287a,'#skF_11')
| ~ $less(I_287a,'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_460,c_460,c_609]) ).
tff(c_351359,plain,
! [T_38747: map_int_int,I_38748a: $int] :
( partial_solution1('#skF_10',T_38747)
| ~ eq_prefix1(int,t2tb2(T_38747),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_38748a)),'#skF_10')
| $less(I_38748a,0)
| ~ $less(I_38748a,'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_461,c_350977]) ).
tff(c_351363,plain,
! [J_183: uni,I_38748a: $int] :
( partial_solution1('#skF_10',tb2t2(J_183))
| ~ eq_prefix1(int,J_183,get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_38748a)),'#skF_10')
| $less(I_38748a,0)
| ~ $less(I_38748a,'#skF_18') ),
inference(superposition,[status(thm),theory(equality)],[c_203,c_351359]) ).
tff(c_365908,plain,
( partial_solution1('#skF_10',tb2t2(t2tb2('#skF_23')))
| $less('#skF_24',0)
| ~ $less('#skF_24','#skF_18') ),
inference(resolution,[status(thm)],[c_365684,c_351363]) ).
tff(c_365919,plain,
( partial_solution1('#skF_10','#skF_23')
| $less('#skF_24',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_351278,c_201,c_365908]) ).
tff(c_365921,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_351285,c_351270,c_365919]) ).
tff(c_365924,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| $less(I_290a,0)
| ~ $less(I_290a,'#skF_18') ),
inference(splitRight,[status(thm)],[c_351103]) ).
tff(c_375913,plain,
( $less('#skE_25',0)
| ~ $less('#skE_25','#skF_18') ),
inference(resolution,[status(thm)],[c_375905,c_365924]) ).
tff(c_375937,plain,
$less('#skE_25',0),
inference(demodulation,[status(thm),theory(equality)],[c_354281,c_375913]) ).
tff(c_375939,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_359668,c_375937]) ).
tff(c_375943,plain,
$less('#skE_26',0),
inference(splitRight,[status(thm)],[c_354067]) ).
tff(c_382411,plain,
! [T_40814: map_int_int] :
( ~ $less('#skF_22'(T_40814),0)
| ~ partial_solution1('#skF_10',T_40814)
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_40814),0),0) ),
inference(resolution,[status(thm)],[c_353472,c_351076]) ).
tff(c_382431,plain,
( ~ $less('#skF_22'('#skF_25'),0)
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(resolution,[status(thm)],[c_351836,c_382411]) ).
tff(c_382450,plain,
~ $less('#skE_25',0),
inference(demodulation,[status(thm),theory(equality)],[c_375943,c_354066,c_354065,c_382431]) ).
tff(c_375942,plain,
$less('#skE_25','#skF_18'),
inference(splitRight,[status(thm)],[c_354067]) ).
tff(c_353519,plain,
! [T_284: map_int_int] :
( eq_prefix1(int,t2tb2(T_284),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_22'(T_284))),'#skF_10')
| ~ partial_solution1('#skF_10',T_284)
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_284),0),0) ),
inference(resolution,[status(thm)],[c_353472,c_351080]) ).
tff(c_354071,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| ~ partial_solution1('#skF_10','#skF_25')
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(superposition,[status(thm),theory(equality)],[c_354065,c_353519]) ).
tff(c_354080,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(demodulation,[status(thm),theory(equality)],[c_351836,c_354071]) ).
tff(c_395821,plain,
eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10'),
inference(demodulation,[status(thm),theory(equality)],[c_375943,c_354066,c_354080]) ).
tff(c_385858,plain,
eq_prefix1(int,t2tb2('#skF_23'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_24')),'#skF_10'),
inference(splitLeft,[status(thm)],[c_351103]) ).
tff(c_386002,plain,
( partial_solution1('#skF_10',tb2t2(t2tb2('#skF_23')))
| $less('#skF_24',0)
| ~ $less('#skF_24','#skF_18') ),
inference(resolution,[status(thm)],[c_385858,c_351363]) ).
tff(c_386013,plain,
( partial_solution1('#skF_10','#skF_23')
| $less('#skF_24',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_351278,c_201,c_386002]) ).
tff(c_386015,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_351285,c_351270,c_386013]) ).
tff(c_386018,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| $less(I_290a,0)
| ~ $less(I_290a,'#skF_18') ),
inference(splitRight,[status(thm)],[c_351103]) ).
tff(c_395829,plain,
( $less('#skE_25',0)
| ~ $less('#skE_25','#skF_18') ),
inference(resolution,[status(thm)],[c_395821,c_386018]) ).
tff(c_395853,plain,
$less('#skE_25',0),
inference(demodulation,[status(thm),theory(equality)],[c_375942,c_395829]) ).
tff(c_395855,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_382450,c_395853]) ).
tff(c_395858,plain,
eq_prefix1(int,t2tb2('#skF_23'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_24')),'#skF_10'),
inference(splitRight,[status(thm)],[c_351094]) ).
tff(c_396464,plain,
( partial_solution1('#skF_10',tb2t2(t2tb2('#skF_23')))
| $less('#skF_24',0)
| ~ $less('#skF_24','#skF_18') ),
inference(resolution,[status(thm)],[c_395858,c_351363]) ).
tff(c_396474,plain,
( partial_solution1('#skF_10','#skF_23')
| $less('#skF_24',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_351278,c_201,c_396464]) ).
tff(c_396476,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_351285,c_351270,c_396474]) ).
tff(c_396479,plain,
partial_solution1('#skF_10','#skF_25'),
inference(splitRight,[status(thm)],[c_351091]) ).
tff(c_398483,plain,
! [A_41996: ty,T_41997: uni,U_41998: uni,I_41999a: $int] :
( ~ $less('#skF_4'(A_41996,T_41997,U_41998,I_41999a),0)
| eq_prefix1(A_41996,T_41997,U_41998,I_41999a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_196]) ).
tff(c_398632,plain,
! [T_42014: map_int_int] :
( $less('#skF_22'(T_42014),'#skF_18')
| ~ partial_solution1('#skF_10',T_42014)
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_42014),0),0) ),
inference(resolution,[status(thm)],[c_398483,c_351074]) ).
tff(c_398649,plain,
( $less('#skF_22'('#skF_25'),'#skF_18')
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(resolution,[status(thm)],[c_396479,c_398632]) ).
tff(c_399197,plain,
'#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0) = '#skE_26',
inference(define,[status(thm),theory(equality)],[c_398649]) ).
tff(c_399196,plain,
'#skF_22'('#skF_25') = '#skE_25',
inference(define,[status(thm),theory(equality)],[c_398649]) ).
tff(c_399202,plain,
( $less('#skE_25','#skF_18')
| ~ $less('#skE_26',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_399197,c_399196,c_398649]) ).
tff(c_399228,plain,
~ $less('#skE_26',0),
inference(splitLeft,[status(thm)],[c_399202]) ).
tff(c_399201,plain,
'#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0) = '#skE_26',
inference(define,[status(thm),theory(equality)],[c_398649]) ).
tff(c_399200,plain,
'#skF_22'('#skF_25') = '#skE_25',
inference(define,[status(thm),theory(equality)],[c_398649]) ).
tff(c_398394,plain,
! [A_41983: ty,T_41984: uni,U_41985: uni,I_41986a: $int] :
( $less('#skF_4'(A_41983,T_41984,U_41985,I_41986a),I_41986a)
| eq_prefix1(A_41983,T_41984,U_41985,I_41986a) ),
inference(cnfTransformation,[status(thm)],[f_334]) ).
tff(c_405117,plain,
! [T_42373: map_int_int] :
( ~ $less('#skF_22'(T_42373),0)
| ~ partial_solution1('#skF_10',T_42373)
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_42373),0),0) ),
inference(resolution,[status(thm)],[c_398394,c_351076]) ).
tff(c_405139,plain,
( ~ $less('#skF_22'('#skF_25'),0)
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(resolution,[status(thm)],[c_396479,c_405117]) ).
tff(c_405144,plain,
( ~ $less('#skE_25',0)
| $less('#skE_26',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_399201,c_399200,c_405139]) ).
tff(c_405146,plain,
~ $less('#skE_25',0),
inference(negUnitSimplification,[status(thm)],[c_399228,c_405144]) ).
tff(c_398465,plain,
! [T_41995: map_int_int] :
( $less('#skF_22'(T_41995),'#skF_18')
| ~ partial_solution1('#skF_10',T_41995)
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_41995),0),0) ),
inference(resolution,[status(thm)],[c_398394,c_351074]) ).
tff(c_398482,plain,
( $less('#skF_22'('#skF_25'),'#skF_18')
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(resolution,[status(thm)],[c_396479,c_398465]) ).
tff(c_399346,plain,
( $less('#skE_25','#skF_18')
| $less('#skE_26',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_399201,c_399200,c_398482]) ).
tff(c_399348,plain,
$less('#skE_25','#skF_18'),
inference(negUnitSimplification,[status(thm)],[c_399228,c_399346]) ).
tff(c_398446,plain,
! [T_284: map_int_int] :
( eq_prefix1(int,t2tb2(T_284),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_22'(T_284))),'#skF_10')
| ~ partial_solution1('#skF_10',T_284)
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_284),0),0) ),
inference(resolution,[status(thm)],[c_398394,c_351080]) ).
tff(c_399209,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| ~ partial_solution1('#skF_10','#skF_25')
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(superposition,[status(thm),theory(equality)],[c_399200,c_398446]) ).
tff(c_399218,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(demodulation,[status(thm),theory(equality)],[c_396479,c_399209]) ).
tff(c_419519,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| $less('#skE_26',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_399201,c_399218]) ).
tff(c_419521,plain,
eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10'),
inference(negUnitSimplification,[status(thm)],[c_399228,c_419519]) ).
tff(c_396480,plain,
$less('#skF_24',0),
inference(splitRight,[status(thm)],[c_351091]) ).
tff(c_289,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),n1)
| ~ sorted1('#skF_19',0,'#skF_18')
| ( $difference('#skF_18','#skF_11') != '#skF_18' )
| ~ $lesseq(0,I_290a)
| ~ $less(I_290a,$difference('#skF_18','#skF_11'))
| $lesseq(0,'#skF_24') ),
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_627,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),n1)
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| $less(I_290a,0)
| ~ $less($sum(I_290a,'#skF_11'),'#skF_18')
| ~ $less('#skF_24',0) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_289]) ).
tff(c_350991,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| $less(I_290a,0)
| ~ $less($sum(I_290a,'#skF_11'),'#skF_18')
| ~ $less('#skF_24',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_460,c_627]) ).
tff(c_350993,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| $less(I_290a,0)
| ~ $less($sum('#skF_11',I_290a),'#skF_18')
| ~ $less('#skF_24',0) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_350991]) ).
tff(c_351023,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| ~ sorted1('#skF_19',0,'#skF_18')
| $less(I_290a,0)
| ~ $less($sum(0,I_290a),'#skF_18')
| ~ $less('#skF_24',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_461,c_461,c_350993]) ).
tff(c_351025,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| ~ sorted1('#skF_19',0,'#skF_18')
| $less(I_290a,0)
| ~ $less(I_290a,'#skF_18')
| ~ $less('#skF_24',0) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_351023]) ).
tff(c_351097,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| $less(I_290a,0)
| ~ $less(I_290a,'#skF_18')
| ~ $less('#skF_24',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_351082,c_351025]) ).
tff(c_398181,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| $less(I_290a,0)
| ~ $less(I_290a,'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_396480,c_351097]) ).
tff(c_419540,plain,
( $less('#skE_25',0)
| ~ $less('#skE_25','#skF_18') ),
inference(resolution,[status(thm)],[c_419521,c_398181]) ).
tff(c_419561,plain,
$less('#skE_25',0),
inference(demodulation,[status(thm),theory(equality)],[c_399348,c_419540]) ).
tff(c_419563,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_405146,c_419561]) ).
tff(c_419567,plain,
$less('#skE_26',0),
inference(splitRight,[status(thm)],[c_399202]) ).
tff(c_424749,plain,
! [T_43567: map_int_int] :
( ~ $less('#skF_22'(T_43567),0)
| ~ partial_solution1('#skF_10',T_43567)
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_43567),0),0) ),
inference(resolution,[status(thm)],[c_398483,c_351076]) ).
tff(c_424779,plain,
( ~ $less('#skF_22'('#skF_25'),0)
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(resolution,[status(thm)],[c_396479,c_424749]) ).
tff(c_424790,plain,
~ $less('#skE_25',0),
inference(demodulation,[status(thm),theory(equality)],[c_419567,c_399201,c_399200,c_424779]) ).
tff(c_419566,plain,
$less('#skE_25','#skF_18'),
inference(splitRight,[status(thm)],[c_399202]) ).
tff(c_398535,plain,
! [T_284: map_int_int] :
( eq_prefix1(int,t2tb2(T_284),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_22'(T_284))),'#skF_10')
| ~ partial_solution1('#skF_10',T_284)
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_284),0),0) ),
inference(resolution,[status(thm)],[c_398483,c_351080]) ).
tff(c_399206,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| ~ partial_solution1('#skF_10','#skF_25')
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(superposition,[status(thm),theory(equality)],[c_399200,c_398535]) ).
tff(c_399215,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(demodulation,[status(thm),theory(equality)],[c_396479,c_399206]) ).
tff(c_455382,plain,
eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10'),
inference(demodulation,[status(thm),theory(equality)],[c_419567,c_399201,c_399215]) ).
tff(c_455401,plain,
( $less('#skE_25',0)
| ~ $less('#skE_25','#skF_18') ),
inference(resolution,[status(thm)],[c_455382,c_398181]) ).
tff(c_455422,plain,
$less('#skE_25',0),
inference(demodulation,[status(thm),theory(equality)],[c_419566,c_455401]) ).
tff(c_455424,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_424790,c_455422]) ).
tff(c_455427,plain,
partial_solution1('#skF_10','#skF_25'),
inference(splitRight,[status(thm)],[c_351088]) ).
tff(c_457116,plain,
! [A_45356: ty,T_45357: uni,U_45358: uni,I_45359a: $int] :
( $less('#skF_4'(A_45356,T_45357,U_45358,I_45359a),I_45359a)
| eq_prefix1(A_45356,T_45357,U_45358,I_45359a) ),
inference(cnfTransformation,[status(thm)],[f_334]) ).
tff(c_457208,plain,
! [T_45366: map_int_int] :
( $less('#skF_22'(T_45366),'#skF_18')
| ~ partial_solution1('#skF_10',T_45366)
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_45366),0),0) ),
inference(resolution,[status(thm)],[c_457116,c_351074]) ).
tff(c_457225,plain,
( $less('#skF_22'('#skF_25'),'#skF_18')
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(resolution,[status(thm)],[c_455427,c_457208]) ).
tff(c_457507,plain,
'#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0) = '#skE_26',
inference(define,[status(thm),theory(equality)],[c_457225]) ).
tff(c_457506,plain,
'#skF_22'('#skF_25') = '#skE_25',
inference(define,[status(thm),theory(equality)],[c_457225]) ).
tff(c_457512,plain,
( $less('#skE_25','#skF_18')
| $less('#skE_26',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_457507,c_457506,c_457225]) ).
tff(c_457532,plain,
$less('#skE_26',0),
inference(splitLeft,[status(thm)],[c_457512]) ).
tff(c_457511,plain,
'#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0) = '#skE_26',
inference(define,[status(thm),theory(equality)],[c_457225]) ).
tff(c_457510,plain,
'#skF_22'('#skF_25') = '#skE_25',
inference(define,[status(thm),theory(equality)],[c_457225]) ).
tff(c_457565,plain,
! [A_45422: ty,T_45423: uni,U_45424: uni,I_45425a: $int] :
( ~ $less('#skF_4'(A_45422,T_45423,U_45424,I_45425a),0)
| eq_prefix1(A_45422,T_45423,U_45424,I_45425a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_196]) ).
tff(c_462406,plain,
! [T_45923: map_int_int] :
( ~ $less('#skF_22'(T_45923),0)
| ~ partial_solution1('#skF_10',T_45923)
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_45923),0),0) ),
inference(resolution,[status(thm)],[c_457565,c_351076]) ).
tff(c_462436,plain,
( ~ $less('#skF_22'('#skF_25'),0)
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(resolution,[status(thm)],[c_455427,c_462406]) ).
tff(c_462447,plain,
~ $less('#skE_25',0),
inference(demodulation,[status(thm),theory(equality)],[c_457532,c_457511,c_457510,c_462436]) ).
tff(c_457660,plain,
! [T_45432: map_int_int] :
( $less('#skF_22'(T_45432),'#skF_18')
| ~ partial_solution1('#skF_10',T_45432)
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_45432),0),0) ),
inference(resolution,[status(thm)],[c_457565,c_351074]) ).
tff(c_457674,plain,
( $less('#skF_22'('#skF_25'),'#skF_18')
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(resolution,[status(thm)],[c_455427,c_457660]) ).
tff(c_457679,plain,
$less('#skE_25','#skF_18'),
inference(demodulation,[status(thm),theory(equality)],[c_457532,c_457511,c_457510,c_457674]) ).
tff(c_457925,plain,
! [T_45454: map_int_int] :
( eq_prefix1(int,t2tb2(T_45454),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_22'(T_45454))),'#skF_10')
| ~ partial_solution1('#skF_10',T_45454)
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_45454),0),0) ),
inference(resolution,[status(thm)],[c_457565,c_351080]) ).
tff(c_457928,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| ~ partial_solution1('#skF_10','#skF_25')
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(superposition,[status(thm),theory(equality)],[c_457510,c_457925]) ).
tff(c_457934,plain,
eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10'),
inference(demodulation,[status(thm),theory(equality)],[c_457532,c_457511,c_455427,c_457928]) ).
tff(c_455428,plain,
~ $less('#skF_24','#skF_18'),
inference(splitRight,[status(thm)],[c_351088]) ).
tff(c_287,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),n1)
| ~ sorted1('#skF_19',0,'#skF_18')
| ( $difference('#skF_18','#skF_11') != '#skF_18' )
| ~ $lesseq(0,I_290a)
| ~ $less(I_290a,$difference('#skF_18','#skF_11'))
| $less('#skF_24',$difference('#skF_18','#skF_11')) ),
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_629,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),n1)
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| $less(I_290a,0)
| ~ $less($sum(I_290a,'#skF_11'),'#skF_18')
| $less($sum('#skF_24','#skF_11'),'#skF_18') ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_287]) ).
tff(c_350994,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| $less(I_290a,0)
| ~ $less($sum(I_290a,'#skF_11'),'#skF_18')
| $less($sum('#skF_24','#skF_11'),'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_460,c_629]) ).
tff(c_350996,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| $less(I_290a,0)
| ~ $less($sum('#skF_11',I_290a),'#skF_18')
| $less($sum('#skF_11','#skF_24'),'#skF_18') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_350994]) ).
tff(c_351027,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| ~ sorted1('#skF_19',0,'#skF_18')
| $less(I_290a,0)
| ~ $less($sum(0,I_290a),'#skF_18')
| $less($sum(0,'#skF_24'),'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_461,c_461,c_461,c_350996]) ).
tff(c_351029,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| ~ sorted1('#skF_19',0,'#skF_18')
| $less(I_290a,0)
| ~ $less(I_290a,'#skF_18')
| $less('#skF_24','#skF_18') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_351027]) ).
tff(c_351100,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| $less(I_290a,0)
| ~ $less(I_290a,'#skF_18')
| $less('#skF_24','#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_351082,c_351029]) ).
tff(c_457075,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| $less(I_290a,0)
| ~ $less(I_290a,'#skF_18') ),
inference(negUnitSimplification,[status(thm)],[c_455428,c_351100]) ).
tff(c_463304,plain,
( $less('#skE_25',0)
| ~ $less('#skE_25','#skF_18') ),
inference(resolution,[status(thm)],[c_457934,c_457075]) ).
tff(c_463323,plain,
$less('#skE_25',0),
inference(demodulation,[status(thm),theory(equality)],[c_457679,c_463304]) ).
tff(c_463325,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_462447,c_463323]) ).
tff(c_463329,plain,
~ $less('#skE_26',0),
inference(splitRight,[status(thm)],[c_457512]) ).
tff(c_468539,plain,
! [T_46471: map_int_int] :
( ~ $less('#skF_22'(T_46471),0)
| ~ partial_solution1('#skF_10',T_46471)
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_46471),0),0) ),
inference(resolution,[status(thm)],[c_457116,c_351076]) ).
tff(c_468569,plain,
( ~ $less('#skF_22'('#skF_25'),0)
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(resolution,[status(thm)],[c_455427,c_468539]) ).
tff(c_468578,plain,
( ~ $less('#skE_25',0)
| $less('#skE_26',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_457511,c_457510,c_468569]) ).
tff(c_468580,plain,
~ $less('#skE_25',0),
inference(negUnitSimplification,[status(thm)],[c_463329,c_468578]) ).
tff(c_463328,plain,
$less('#skE_25','#skF_18'),
inference(splitRight,[status(thm)],[c_457512]) ).
tff(c_457168,plain,
! [T_284: map_int_int] :
( eq_prefix1(int,t2tb2(T_284),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_22'(T_284))),'#skF_10')
| ~ partial_solution1('#skF_10',T_284)
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_284),0),0) ),
inference(resolution,[status(thm)],[c_457116,c_351080]) ).
tff(c_457516,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| ~ partial_solution1('#skF_10','#skF_25')
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(superposition,[status(thm),theory(equality)],[c_457510,c_457168]) ).
tff(c_457522,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(demodulation,[status(thm),theory(equality)],[c_455427,c_457516]) ).
tff(c_481742,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| $less('#skE_26',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_457511,c_457522]) ).
tff(c_481744,plain,
eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10'),
inference(negUnitSimplification,[status(thm)],[c_463329,c_481742]) ).
tff(c_481760,plain,
( $less('#skE_25',0)
| ~ $less('#skE_25','#skF_18') ),
inference(resolution,[status(thm)],[c_481744,c_457075]) ).
tff(c_481780,plain,
$less('#skE_25',0),
inference(demodulation,[status(thm),theory(equality)],[c_463328,c_481760]) ).
tff(c_481782,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_468580,c_481780]) ).
tff(c_481785,plain,
partial_solution1('#skF_10','#skF_25'),
inference(splitRight,[status(thm)],[c_351085]) ).
tff(c_483721,plain,
! [A_47395: ty,T_47396: uni,U_47397: uni,I_47398a: $int] :
( ~ $less('#skF_4'(A_47395,T_47396,U_47397,I_47398a),0)
| eq_prefix1(A_47395,T_47396,U_47397,I_47398a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_196]) ).
tff(c_483857,plain,
! [T_47411: map_int_int] :
( $less('#skF_22'(T_47411),'#skF_18')
| ~ partial_solution1('#skF_10',T_47411)
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_47411),0),0) ),
inference(resolution,[status(thm)],[c_483721,c_351074]) ).
tff(c_483879,plain,
( $less('#skF_22'('#skF_25'),'#skF_18')
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(resolution,[status(thm)],[c_481785,c_483857]) ).
tff(c_484298,plain,
'#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0) = '#skE_26',
inference(define,[status(thm),theory(equality)],[c_483879]) ).
tff(c_484297,plain,
'#skF_22'('#skF_25') = '#skE_25',
inference(define,[status(thm),theory(equality)],[c_483879]) ).
tff(c_484303,plain,
( $less('#skE_25','#skF_18')
| ~ $less('#skE_26',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_484298,c_484297,c_483879]) ).
tff(c_484329,plain,
~ $less('#skE_26',0),
inference(splitLeft,[status(thm)],[c_484303]) ).
tff(c_484302,plain,
'#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0) = '#skE_26',
inference(define,[status(thm),theory(equality)],[c_483879]) ).
tff(c_484301,plain,
'#skF_22'('#skF_25') = '#skE_25',
inference(define,[status(thm),theory(equality)],[c_483879]) ).
tff(c_483392,plain,
! [A_47344: ty,T_47345: uni,U_47346: uni,I_47347a: $int] :
( $less('#skF_4'(A_47344,T_47345,U_47346,I_47347a),I_47347a)
| eq_prefix1(A_47344,T_47345,U_47346,I_47347a) ),
inference(cnfTransformation,[status(thm)],[f_334]) ).
tff(c_490252,plain,
! [T_48026: map_int_int] :
( ~ $less('#skF_22'(T_48026),0)
| ~ partial_solution1('#skF_10',T_48026)
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_48026),0),0) ),
inference(resolution,[status(thm)],[c_483392,c_351076]) ).
tff(c_490286,plain,
( ~ $less('#skF_22'('#skF_25'),0)
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(resolution,[status(thm)],[c_481785,c_490252]) ).
tff(c_490298,plain,
( ~ $less('#skE_25',0)
| $less('#skE_26',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_484302,c_484301,c_490286]) ).
tff(c_490300,plain,
~ $less('#skE_25',0),
inference(negUnitSimplification,[status(thm)],[c_484329,c_490298]) ).
tff(c_483500,plain,
! [T_47357: map_int_int] :
( $less('#skF_22'(T_47357),'#skF_18')
| ~ partial_solution1('#skF_10',T_47357)
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_47357),0),0) ),
inference(resolution,[status(thm)],[c_483392,c_351074]) ).
tff(c_483522,plain,
( $less('#skF_22'('#skF_25'),'#skF_18')
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(resolution,[status(thm)],[c_481785,c_483500]) ).
tff(c_484359,plain,
( $less('#skE_25','#skF_18')
| $less('#skE_26',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_484302,c_484301,c_483522]) ).
tff(c_484361,plain,
$less('#skE_25','#skF_18'),
inference(negUnitSimplification,[status(thm)],[c_484329,c_484359]) ).
tff(c_483439,plain,
! [T_284: map_int_int] :
( eq_prefix1(int,t2tb2(T_284),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_22'(T_284))),'#skF_10')
| ~ partial_solution1('#skF_10',T_284)
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_284),0),0) ),
inference(resolution,[status(thm)],[c_483392,c_351080]) ).
tff(c_484310,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| ~ partial_solution1('#skF_10','#skF_25')
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(superposition,[status(thm),theory(equality)],[c_484301,c_483439]) ).
tff(c_484319,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(demodulation,[status(thm),theory(equality)],[c_481785,c_484310]) ).
tff(c_521520,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| $less('#skE_26',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_484302,c_484319]) ).
tff(c_521522,plain,
eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10'),
inference(negUnitSimplification,[status(thm)],[c_484329,c_521520]) ).
tff(c_481786,plain,
partial_solution1('#skF_10','#skF_23'),
inference(splitRight,[status(thm)],[c_351085]) ).
tff(c_283,plain,
! [I_290a: $int] :
( ~ partial_solution1(n1,'#skF_23')
| ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),n1)
| ~ sorted1('#skF_19',0,'#skF_18')
| ( $difference('#skF_18','#skF_11') != '#skF_18' )
| ~ $lesseq(0,I_290a)
| ~ $less(I_290a,$difference('#skF_18','#skF_11')) ),
inference(cnfTransformation,[status(thm)],[f_508]) ).
tff(c_633,plain,
! [I_290a: $int] :
( ~ partial_solution1(n1,'#skF_23')
| ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),n1)
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| $less(I_290a,0)
| ~ $less($sum(I_290a,'#skF_11'),'#skF_18') ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_283]) ).
tff(c_351000,plain,
! [I_290a: $int] :
( ~ partial_solution1('#skF_10','#skF_23')
| ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| $less(I_290a,0)
| ~ $less($sum(I_290a,'#skF_11'),'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_460,c_460,c_633]) ).
tff(c_351002,plain,
! [I_290a: $int] :
( ~ partial_solution1('#skF_10','#skF_23')
| ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| ~ sorted1('#skF_19',0,'#skF_18')
| ( '#skF_11' != 0 )
| $less(I_290a,0)
| ~ $less($sum('#skF_11',I_290a),'#skF_18') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_351000]) ).
tff(c_351035,plain,
! [I_290a: $int] :
( ~ partial_solution1('#skF_10','#skF_23')
| ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| ~ sorted1('#skF_19',0,'#skF_18')
| $less(I_290a,0)
| ~ $less($sum(0,I_290a),'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_461,c_461,c_351002]) ).
tff(c_351037,plain,
! [I_290a: $int] :
( ~ partial_solution1('#skF_10','#skF_23')
| ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| ~ sorted1('#skF_19',0,'#skF_18')
| $less(I_290a,0)
| ~ $less(I_290a,'#skF_18') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_351035]) ).
tff(c_351106,plain,
! [I_290a: $int] :
( ~ partial_solution1('#skF_10','#skF_23')
| ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| $less(I_290a,0)
| ~ $less(I_290a,'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_351082,c_351037]) ).
tff(c_490931,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| $less(I_290a,0)
| ~ $less(I_290a,'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_481786,c_351106]) ).
tff(c_521530,plain,
( $less('#skE_25',0)
| ~ $less('#skE_25','#skF_18') ),
inference(resolution,[status(thm)],[c_521522,c_490931]) ).
tff(c_521552,plain,
$less('#skE_25',0),
inference(demodulation,[status(thm),theory(equality)],[c_484361,c_521530]) ).
tff(c_521554,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_490300,c_521552]) ).
tff(c_521558,plain,
$less('#skE_26',0),
inference(splitRight,[status(thm)],[c_484303]) ).
tff(c_527460,plain,
! [T_49841: map_int_int] :
( ~ $less('#skF_22'(T_49841),0)
| ~ partial_solution1('#skF_10',T_49841)
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_49841),0),0) ),
inference(resolution,[status(thm)],[c_483721,c_351076]) ).
tff(c_527494,plain,
( ~ $less('#skF_22'('#skF_25'),0)
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(resolution,[status(thm)],[c_481785,c_527460]) ).
tff(c_527506,plain,
~ $less('#skE_25',0),
inference(demodulation,[status(thm),theory(equality)],[c_521558,c_484302,c_484301,c_527494]) ).
tff(c_521557,plain,
$less('#skE_25','#skF_18'),
inference(splitRight,[status(thm)],[c_484303]) ).
tff(c_483768,plain,
! [T_284: map_int_int] :
( eq_prefix1(int,t2tb2(T_284),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skF_22'(T_284))),'#skF_10')
| ~ partial_solution1('#skF_10',T_284)
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2(T_284),0),0) ),
inference(resolution,[status(thm)],[c_483721,c_351080]) ).
tff(c_484307,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| ~ partial_solution1('#skF_10','#skF_25')
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(superposition,[status(thm),theory(equality)],[c_484301,c_483768]) ).
tff(c_484316,plain,
( eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10')
| ~ $less('#skF_4'(int,t2tb2('#skF_21'),t2tb2('#skF_25'),0),0) ),
inference(demodulation,[status(thm),theory(equality)],[c_481785,c_484307]) ).
tff(c_539809,plain,
eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1('#skE_25')),'#skF_10'),
inference(demodulation,[status(thm),theory(equality)],[c_521558,c_484302,c_484316]) ).
tff(c_529365,plain,
! [I_290a: $int] :
( ~ eq_prefix1(int,t2tb2('#skF_25'),get(map(int,int),int,t2tb3('#skF_19'),t2tb1(I_290a)),'#skF_10')
| $less(I_290a,0)
| ~ $less(I_290a,'#skF_18') ),
inference(demodulation,[status(thm),theory(equality)],[c_481786,c_351106]) ).
tff(c_539813,plain,
( $less('#skE_25',0)
| ~ $less('#skE_25','#skF_18') ),
inference(resolution,[status(thm)],[c_539809,c_529365]) ).
tff(c_539838,plain,
$less('#skE_25',0),
inference(demodulation,[status(thm),theory(equality)],[c_521557,c_539813]) ).
tff(c_539840,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_527506,c_539838]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWW634_2 : TPTP v9.0.0. Released v6.1.0.
% 0.11/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.14/0.34 % Computer : n023.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed Apr 9 06:19:09 EDT 2025
% 0.14/0.34 % CPUTime :
% 152.48/101.71 ***********************************************************************
% 152.48/101.72 After 99.7 sec it's time to try something different, got 99.6 sec left
% 152.48/101.72 ***********************************************************************
% 190.72/133.08 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 190.72/133.11
% 190.72/133.11 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------