%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWW657_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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n008.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:08 PM UTC 2025
% Result : Theorem 159.04s 105.93s
% Output : CNFRefutation 159.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 5
% Syntax : Number of formulae : 143 ( 70 unt; 0 typ; 0 def)
% Number of atoms : 310 ( 43 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 246 ( 79 ~; 156 |; 6 &)
% ( 2 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 6 ( 1 avg)
% Number arithmetic : 752 ( 212 atm; 276 fun; 172 num; 92 var)
% Number of types : 7 ( 5 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 3 usr; 1 prp; 0-4 aty)
% Number of functors : 61 ( 57 usr; 40 con; 0-5 aty)
% Number of variables : 120 ( 120 !; 0 ?; 120 :)
% Comments :
%------------------------------------------------------------------------------
%$ is_longest_common_prefix1 > is_common_prefix1 > sort1 > set > set2 > match_bool1 > get > mk_array1 > make1 > get2 > const > map > length1 > elts > #nlpp > witness1 > tb2t1 > tb2t > t2tb1 > t2tb > array > tuple03 > tuple0 > true1 > real > qtmark > int > false1 > bool > #skF_2 > #skF_1 > #skF_3
%Foreground sorts:
tff(tuple02,type,
tuple02: $tType ).
tff(bool1,type,
bool1: $tType ).
tff(array_int,type,
array_int: $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_11',type,
'#skE_11': $int ).
tff('#skE_25',type,
'#skE_25': $int ).
tff('#skE_23',type,
'#skE_23': $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_20',type,
'#skE_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_10',type,
'#skE_10': $int ).
tff('#skE_24',type,
'#skE_24': $int ).
tff('#skE_5',type,
'#skE_5': $int ).
tff('#skE_15',type,
'#skE_15': $int ).
tff('#skE_8',type,
'#skE_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_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_18',type,
'#skE_18': $int ).
tff('#skE_19',type,
'#skE_19': $int ).
tff('#skE_14',type,
'#skE_14': $int ).
%Foreground operators:
tff(length1,type,
length1: ( ty * uni ) > $int ).
tff(get2,type,
get2: ( ty * uni * $int ) > uni ).
tff(true1,type,
true1: bool1 ).
tff(const,type,
const: ( ty * ty * uni ) > uni ).
tff(elts,type,
elts: ( ty * uni ) > uni ).
tff(int,type,
int: ty ).
tff(false1,type,
false1: bool1 ).
tff(tb2t,type,
tb2t: uni > $int ).
tff(sort1,type,
sort1: ( ty * uni ) > $o ).
tff(t2tb,type,
t2tb: $int > uni ).
tff(witness1,type,
witness1: ty > uni ).
tff(real,type,
real: ty ).
tff('#skF_2',type,
'#skF_2': ( array_int * $int * $int * $int ) > $int ).
tff(set,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(match_bool1,type,
match_bool1: ( ty * bool1 * uni * uni ) > uni ).
tff(array,type,
array: ty > ty ).
tff('#skF_1',type,
'#skF_1': ( array_int * $int * $int * $int ) > $int ).
tff(make1,type,
make1: ( ty * $int * uni ) > uni ).
tff('#skF_3',type,
'#skF_3': array_int ).
tff(tuple0,type,
tuple0: ty ).
tff(qtmark,type,
qtmark: ty ).
tff(tb2t1,type,
tb2t1: uni > array_int ).
tff(bool,type,
bool: ty ).
tff(get,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(t2tb1,type,
t2tb1: array_int > uni ).
tff(is_longest_common_prefix1,type,
is_longest_common_prefix1: ( array_int * $int * $int * $int ) > $o ).
tff(tuple03,type,
tuple03: tuple02 ).
tff(map,type,
map: ( ty * ty ) > ty ).
tff(set2,type,
set2: ( ty * uni * $int * uni ) > uni ).
tff(mk_array1,type,
mk_array1: ( ty * $int * uni ) > uni ).
tff(is_common_prefix1,type,
is_common_prefix1: ( array_int * $int * $int * $int ) > $o ).
tff(f_161,negated_conjecture,
~ ! [A: array_int,Xa: $int,Ya: $int,La: $int] :
( ( is_common_prefix1(A,Xa,Ya,La)
& ~ is_common_prefix1(A,Xa,Ya,$sum(La,1)) )
=> is_longest_common_prefix1(A,Xa,Ya,La) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',longest_common_prefix_succ) ).
tff(f_131,axiom,
! [A: array_int,Xa: $int,Ya: $int,La: $int] :
( is_common_prefix1(A,Xa,Ya,La)
<=> ( $lesseq(0,La)
& $lesseq($sum(Xa,La),length1(int,t2tb1(A)))
& $lesseq($sum(Ya,La),length1(int,t2tb1(A)))
& ! [Ia: $int] :
( ( $lesseq(0,Ia)
& $less(Ia,La) )
=> ( tb2t(get2(int,t2tb1(A),$sum(Xa,Ia))) = tb2t(get2(int,t2tb1(A),$sum(Ya,Ia))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',is_common_prefix_def) ).
tff(f_100,axiom,
! [J: uni] : ( t2tb(tb2t(J)) = J ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR) ).
tff(f_153,axiom,
! [A: array_int,Xa: $int,Ya: $int,La: $int] :
( is_longest_common_prefix1(A,Xa,Ya,La)
<=> ( is_common_prefix1(A,Xa,Ya,La)
& ! [Ma: $int] :
( $less(La,Ma)
=> ~ is_common_prefix1(A,Xa,Ya,Ma) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',is_longest_common_prefix_def) ).
tff(f_98,axiom,
! [Ia: $int] : ( tb2t(t2tb(Ia)) = Ia ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL) ).
tff(c_196,plain,
is_common_prefix1('#skF_3','#skF_4','#skF_5','#skF_6'),
inference(cnfTransformation,[status(thm)],[f_161]) ).
tff(c_69,plain,
! [X_86a: $int,L_88a: $int,A_85: array_int,Y_87a: $int] :
( $lesseq($sum(X_86a,L_88a),length1(int,t2tb1(A_85)))
| ~ is_common_prefix1(A_85,X_86a,Y_87a,L_88a) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_156,plain,
! [A_85: array_int,L_88a: $int,X_86a: $int,Y_87a: $int] :
( ~ $less(length1(int,t2tb1(A_85)),$sum(L_88a,X_86a))
| ~ is_common_prefix1(A_85,X_86a,Y_87a,L_88a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_69]) ).
tff(c_591760,plain,
! [A_58926: array_int,X_58927a: $int,L_58928a: $int,Y_58929a: $int] :
( ~ $less(length1(int,t2tb1(A_58926)),$sum(X_58927a,L_58928a))
| ~ is_common_prefix1(A_58926,X_58927a,Y_58929a,L_58928a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_156]) ).
tff(c_591765,plain,
~ $less(length1(int,t2tb1('#skF_3')),$sum('#skF_4','#skF_6')),
inference(resolution,[status(thm)],[c_196,c_591760]) ).
tff(c_591769,plain,
length1(int,t2tb1('#skF_3')) = '#skE_19',
inference(define,[status(thm),theory(equality)],[c_591765]) ).
tff(c_77,plain,
! [A_85: array_int,X_86a: $int,Y_87a: $int,L_88a: $int] :
( $lesseq(0,'#skF_1'(A_85,X_86a,Y_87a,L_88a))
| is_common_prefix1(A_85,X_86a,Y_87a,L_88a)
| ~ $lesseq($sum(Y_87a,L_88a),length1(int,t2tb1(A_85)))
| ~ $lesseq($sum(X_86a,L_88a),length1(int,t2tb1(A_85)))
| ~ $lesseq(0,L_88a) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_140,plain,
! [A_85: array_int,X_86a: $int,Y_87a: $int,L_88a: $int] :
( ~ $less('#skF_1'(A_85,X_86a,Y_87a,L_88a),0)
| is_common_prefix1(A_85,X_86a,Y_87a,L_88a)
| $less(length1(int,t2tb1(A_85)),$sum(L_88a,Y_87a))
| $less(length1(int,t2tb1(A_85)),$sum(L_88a,X_86a))
| $less(L_88a,0) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_77]) ).
tff(c_593474,plain,
! [A_59152: array_int,X_59153a: $int,Y_59154a: $int,L_59155a: $int] :
( ~ $less('#skF_1'(A_59152,X_59153a,Y_59154a,L_59155a),0)
| is_common_prefix1(A_59152,X_59153a,Y_59154a,L_59155a)
| $less(length1(int,t2tb1(A_59152)),$sum(Y_59154a,L_59155a))
| $less(length1(int,t2tb1(A_59152)),$sum(X_59153a,L_59155a))
| $less(L_59155a,0) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_140]) ).
tff(c_91,plain,
~ is_common_prefix1('#skF_3','#skF_4','#skF_5',$sum('#skF_6',1)),
inference(cnfTransformation,[status(thm)],[f_161]) ).
tff(c_197,plain,
~ is_common_prefix1('#skF_3','#skF_4','#skF_5',$sum(1,'#skF_6')),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_91]) ).
tff(c_593494,plain,
( ~ $less('#skF_1'('#skF_3','#skF_4','#skF_5',$sum(1,'#skF_6')),0)
| $less(length1(int,t2tb1('#skF_3')),$sum('#skF_5',$sum(1,'#skF_6')))
| $less(length1(int,t2tb1('#skF_3')),$sum('#skF_4',$sum(1,'#skF_6')))
| $less($sum(1,'#skF_6'),0) ),
inference(resolution,[status(thm)],[c_593474,c_197]) ).
tff(c_593500,plain,
( ~ $less('#skF_1'('#skF_3','#skF_4','#skF_5',$sum(1,'#skF_6')),0)
| $less('#skE_19',$sum('#skF_5',$sum(1,'#skF_6')))
| $less('#skE_19',$sum('#skF_4',$sum(1,'#skF_6')))
| $less($sum(1,'#skF_6'),0) ),
inference(demodulation,[status(thm),theory(equality)],[c_591769,c_591769,c_593494]) ).
tff(c_593502,plain,
( ~ $less('#skF_1'('#skF_3','#skF_4','#skF_5',$sum(1,'#skF_6')),0)
| $less('#skE_19',$sum(1,$sum('#skF_5','#skF_6')))
| $less('#skE_19',$sum(1,$sum('#skF_4','#skF_6')))
| $less('#skF_6',$uminus(1)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_593500]) ).
tff(c_594035,plain,
'#skF_1'('#skF_3','#skF_4','#skF_5',$sum(1,'#skF_6')) = '#skE_21',
inference(define,[status(thm),theory(equality)],[c_593502]) ).
tff(c_75,plain,
! [A_85: array_int,X_86a: $int,Y_87a: $int,L_88a: $int] :
( $less('#skF_1'(A_85,X_86a,Y_87a,L_88a),L_88a)
| is_common_prefix1(A_85,X_86a,Y_87a,L_88a)
| ~ $lesseq($sum(Y_87a,L_88a),length1(int,t2tb1(A_85)))
| ~ $lesseq($sum(X_86a,L_88a),length1(int,t2tb1(A_85)))
| ~ $lesseq(0,L_88a) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_145,plain,
! [A_85: array_int,X_86a: $int,Y_87a: $int,L_88a: $int] :
( $less('#skF_1'(A_85,X_86a,Y_87a,L_88a),L_88a)
| is_common_prefix1(A_85,X_86a,Y_87a,L_88a)
| $less(length1(int,t2tb1(A_85)),$sum(L_88a,Y_87a))
| $less(length1(int,t2tb1(A_85)),$sum(L_88a,X_86a))
| $less(L_88a,0) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_75]) ).
tff(c_593874,plain,
! [A_59173: array_int,X_59174a: $int,Y_59175a: $int,L_59176a: $int] :
( $less('#skF_1'(A_59173,X_59174a,Y_59175a,L_59176a),L_59176a)
| is_common_prefix1(A_59173,X_59174a,Y_59175a,L_59176a)
| $less(length1(int,t2tb1(A_59173)),$sum(Y_59175a,L_59176a))
| $less(length1(int,t2tb1(A_59173)),$sum(X_59174a,L_59176a))
| $less(L_59176a,0) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_145]) ).
tff(c_593894,plain,
( $less('#skF_1'('#skF_3','#skF_4','#skF_5',$sum(1,'#skF_6')),$sum(1,'#skF_6'))
| $less(length1(int,t2tb1('#skF_3')),$sum('#skF_5',$sum(1,'#skF_6')))
| $less(length1(int,t2tb1('#skF_3')),$sum('#skF_4',$sum(1,'#skF_6')))
| $less($sum(1,'#skF_6'),0) ),
inference(resolution,[status(thm)],[c_593874,c_197]) ).
tff(c_593900,plain,
( $less('#skF_1'('#skF_3','#skF_4','#skF_5',$sum(1,'#skF_6')),$sum(1,'#skF_6'))
| $less('#skE_19',$sum('#skF_5',$sum(1,'#skF_6')))
| $less('#skE_19',$sum('#skF_4',$sum(1,'#skF_6')))
| $less($sum(1,'#skF_6'),0) ),
inference(demodulation,[status(thm),theory(equality)],[c_591769,c_591769,c_593894]) ).
tff(c_593902,plain,
( $less('#skF_1'('#skF_3','#skF_4','#skF_5',$sum(1,'#skF_6')),$sum(1,'#skF_6'))
| $less('#skE_19',$sum(1,$sum('#skF_5','#skF_6')))
| $less('#skE_19',$sum(1,$sum('#skF_4','#skF_6')))
| $less('#skF_6',$uminus(1)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_593900]) ).
tff(c_594360,plain,
( $less('#skE_21',$sum(1,'#skF_6'))
| $less('#skE_19',$sum(1,$sum('#skF_5','#skF_6')))
| $less('#skE_19',$sum(1,$sum('#skF_4','#skF_6')))
| $less('#skF_6',$uminus(1)) ),
inference(demodulation,[status(thm),theory(equality)],[c_594035,c_593902]) ).
tff(c_594362,plain,
( $less('#skE_21',$sum(1,'#skF_6'))
| $less('#skE_19',$sum(1,$sum('#skF_6','#skF_5')))
| $less('#skE_19',$sum(1,$sum('#skF_6','#skF_4')))
| $less('#skF_6',$uminus(1)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_594360]) ).
tff(c_594364,plain,
$less('#skF_6',$uminus(1)),
inference(splitLeft,[status(thm)],[c_594362]) ).
tff(c_71,plain,
! [A_85: array_int,X_86a: $int,Y_87a: $int,L_88a: $int] :
( ~ is_common_prefix1(A_85,X_86a,Y_87a,L_88a)
| $lesseq(0,L_88a) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_591044,plain,
! [A_58838: array_int,X_58839a: $int,Y_58840a: $int,L_58841a: $int] :
( ~ is_common_prefix1(A_58838,X_58839a,Y_58840a,L_58841a)
| ~ $less(L_58841a,0) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_71]) ).
tff(c_591049,plain,
~ $less('#skF_6',0),
inference(resolution,[status(thm)],[c_196,c_591044]) ).
tff(c_594365,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_594364,c_591049]) ).
tff(c_594366,plain,
( $less('#skE_19',$sum(1,$sum('#skF_6','#skF_4')))
| $less('#skE_19',$sum(1,$sum('#skF_6','#skF_5')))
| $less('#skE_21',$sum(1,'#skF_6')) ),
inference(splitRight,[status(thm)],[c_594362]) ).
tff(c_594369,plain,
( $less('#skE_19',$sum(1,$sum('#skF_4','#skF_6')))
| $less('#skE_19',$sum(1,$sum('#skF_5','#skF_6')))
| $less('#skE_21',$sum(1,'#skF_6')) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_594366]) ).
tff(c_604132,plain,
$less('#skE_21',$sum(1,'#skF_6')),
inference(splitLeft,[status(thm)],[c_594369]) ).
tff(c_594032,plain,
'#skF_1'('#skF_3','#skF_4','#skF_5',$sum(1,'#skF_6')) = '#skE_21',
inference(define,[status(thm),theory(equality)],[c_593502]) ).
tff(c_594034,plain,
( ~ $less('#skE_21',0)
| $less('#skE_19',$sum(1,$sum('#skF_5','#skF_6')))
| $less('#skE_19',$sum(1,$sum('#skF_4','#skF_6')))
| $less('#skF_6',$uminus(1)) ),
inference(demodulation,[status(thm),theory(equality)],[c_594032,c_593502]) ).
tff(c_594037,plain,
( ~ $less('#skE_21',0)
| $less('#skE_19',$sum(1,$sum('#skF_6','#skF_5')))
| $less('#skE_19',$sum(1,$sum('#skF_6','#skF_4')))
| $less('#skF_6',$uminus(1)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_594034]) ).
tff(c_599475,plain,
~ $less('#skE_21',0),
inference(splitLeft,[status(thm)],[c_594037]) ).
tff(c_73,plain,
! [A_85: array_int,Y_87a: $int,X_86a: $int,L_88a: $int] :
( ( tb2t(get2(int,t2tb1(A_85),$sum(Y_87a,'#skF_1'(A_85,X_86a,Y_87a,L_88a)))) != tb2t(get2(int,t2tb1(A_85),$sum(X_86a,'#skF_1'(A_85,X_86a,Y_87a,L_88a)))) )
| is_common_prefix1(A_85,X_86a,Y_87a,L_88a)
| ~ $lesseq($sum(Y_87a,L_88a),length1(int,t2tb1(A_85)))
| ~ $lesseq($sum(X_86a,L_88a),length1(int,t2tb1(A_85)))
| ~ $lesseq(0,L_88a) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_150,plain,
! [A_85: array_int,Y_87a: $int,X_86a: $int,L_88a: $int] :
( ( tb2t(get2(int,t2tb1(A_85),$sum(Y_87a,'#skF_1'(A_85,X_86a,Y_87a,L_88a)))) != tb2t(get2(int,t2tb1(A_85),$sum(X_86a,'#skF_1'(A_85,X_86a,Y_87a,L_88a)))) )
| is_common_prefix1(A_85,X_86a,Y_87a,L_88a)
| $less(length1(int,t2tb1(A_85)),$sum(L_88a,Y_87a))
| $less(length1(int,t2tb1(A_85)),$sum(L_88a,X_86a))
| $less(L_88a,0) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_73]) ).
tff(c_594542,plain,
! [A_59266: array_int,Y_59267a: $int,X_59268a: $int,L_59269a: $int] :
( ( tb2t(get2(int,t2tb1(A_59266),$sum(Y_59267a,'#skF_1'(A_59266,X_59268a,Y_59267a,L_59269a)))) != tb2t(get2(int,t2tb1(A_59266),$sum(X_59268a,'#skF_1'(A_59266,X_59268a,Y_59267a,L_59269a)))) )
| is_common_prefix1(A_59266,X_59268a,Y_59267a,L_59269a)
| $less(length1(int,t2tb1(A_59266)),$sum(Y_59267a,L_59269a))
| $less(length1(int,t2tb1(A_59266)),$sum(X_59268a,L_59269a))
| $less(L_59269a,0) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_150]) ).
tff(c_594567,plain,
( ( tb2t(get2(int,t2tb1('#skF_3'),$sum('#skF_5','#skF_1'('#skF_3','#skF_4','#skF_5',$sum(1,'#skF_6'))))) != tb2t(get2(int,t2tb1('#skF_3'),$sum('#skF_4','#skF_1'('#skF_3','#skF_4','#skF_5',$sum(1,'#skF_6'))))) )
| $less(length1(int,t2tb1('#skF_3')),$sum('#skF_5',$sum(1,'#skF_6')))
| $less(length1(int,t2tb1('#skF_3')),$sum('#skF_4',$sum(1,'#skF_6')))
| $less($sum(1,'#skF_6'),0) ),
inference(resolution,[status(thm)],[c_594542,c_197]) ).
tff(c_594575,plain,
( ( tb2t(get2(int,t2tb1('#skF_3'),$sum('#skF_5','#skE_21'))) != tb2t(get2(int,t2tb1('#skF_3'),$sum('#skF_4','#skE_21'))) )
| $less('#skE_19',$sum('#skF_5',$sum(1,'#skF_6')))
| $less('#skE_19',$sum('#skF_4',$sum(1,'#skF_6')))
| $less($sum(1,'#skF_6'),0) ),
inference(demodulation,[status(thm),theory(equality)],[c_591769,c_591769,c_594035,c_594035,c_594567]) ).
tff(c_594577,plain,
( ( tb2t(get2(int,t2tb1('#skF_3'),$sum('#skE_21','#skF_5'))) != tb2t(get2(int,t2tb1('#skF_3'),$sum('#skE_21','#skF_4'))) )
| $less('#skE_19',$sum(1,$sum('#skF_5','#skF_6')))
| $less('#skE_19',$sum(1,$sum('#skF_4','#skF_6')))
| $less('#skF_6',$uminus(1)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_594575]) ).
tff(c_594708,plain,
tb2t(get2(int,t2tb1('#skF_3'),$sum('#skE_21','#skF_4'))) = '#skE_23',
inference(define,[status(thm),theory(equality)],[c_594577]) ).
tff(c_594707,plain,
tb2t(get2(int,t2tb1('#skF_3'),$sum('#skE_21','#skF_5'))) = '#skE_22',
inference(define,[status(thm),theory(equality)],[c_594577]) ).
tff(c_594710,plain,
( ( '#skE_23' != '#skE_22' )
| $less('#skE_19',$sum(1,$sum('#skF_5','#skF_6')))
| $less('#skE_19',$sum(1,$sum('#skF_4','#skF_6')))
| $less('#skF_6',$uminus(1)) ),
inference(demodulation,[status(thm),theory(equality)],[c_594708,c_594707,c_594577]) ).
tff(c_594716,plain,
( ( '#skE_23' != '#skE_22' )
| $less('#skE_19',$sum(1,$sum('#skF_6','#skF_5')))
| $less('#skE_19',$sum(1,$sum('#skF_6','#skF_4')))
| $less('#skF_6',$uminus(1)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_594710]) ).
tff(c_599850,plain,
'#skE_23' != '#skE_22',
inference(splitLeft,[status(thm)],[c_594716]) ).
tff(c_594714,plain,
tb2t(get2(int,t2tb1('#skF_3'),$sum('#skF_4','#skE_21'))) = '#skE_23',
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_594708]) ).
tff(c_175,plain,
! [J_64: uni] : ( t2tb(tb2t(J_64)) = J_64 ),
inference(cnfTransformation,[status(thm)],[f_100]) ).
tff(c_592096,plain,
! [L_59011a: $int,A_59012: array_int,X_59013a: $int,Y_59014a: $int] :
( $less(L_59011a,'#skF_2'(A_59012,X_59013a,Y_59014a,L_59011a))
| is_longest_common_prefix1(A_59012,X_59013a,Y_59014a,L_59011a)
| ~ is_common_prefix1(A_59012,X_59013a,Y_59014a,L_59011a) ),
inference(cnfTransformation,[status(thm)],[f_153]) ).
tff(c_198,plain,
~ is_longest_common_prefix1('#skF_3','#skF_4','#skF_5','#skF_6'),
inference(cnfTransformation,[status(thm)],[f_161]) ).
tff(c_592108,plain,
( $less('#skF_6','#skF_2'('#skF_3','#skF_4','#skF_5','#skF_6'))
| ~ is_common_prefix1('#skF_3','#skF_4','#skF_5','#skF_6') ),
inference(resolution,[status(thm)],[c_592096,c_198]) ).
tff(c_592113,plain,
$less('#skF_6','#skF_2'('#skF_3','#skF_4','#skF_5','#skF_6')),
inference(demodulation,[status(thm),theory(equality)],[c_196,c_592108]) ).
tff(c_592117,plain,
'#skF_2'('#skF_3','#skF_4','#skF_5','#skF_6') = '#skE_20',
inference(define,[status(thm),theory(equality)],[c_592113]) ).
tff(c_592543,plain,
! [A_59096: array_int,X_59097a: $int,Y_59098a: $int,L_59099a: $int] :
( is_common_prefix1(A_59096,X_59097a,Y_59098a,'#skF_2'(A_59096,X_59097a,Y_59098a,L_59099a))
| is_longest_common_prefix1(A_59096,X_59097a,Y_59098a,L_59099a)
| ~ is_common_prefix1(A_59096,X_59097a,Y_59098a,L_59099a) ),
inference(cnfTransformation,[status(thm)],[f_153]) ).
tff(c_592555,plain,
( is_common_prefix1('#skF_3','#skF_4','#skF_5','#skF_2'('#skF_3','#skF_4','#skF_5','#skF_6'))
| ~ is_common_prefix1('#skF_3','#skF_4','#skF_5','#skF_6') ),
inference(resolution,[status(thm)],[c_592543,c_198]) ).
tff(c_592560,plain,
is_common_prefix1('#skF_3','#skF_4','#skF_5','#skE_20'),
inference(demodulation,[status(thm),theory(equality)],[c_196,c_592117,c_592555]) ).
tff(c_63,plain,
! [X_86a: $int,Y_87a: $int,L_88a: $int,I_91a: $int,A_85: array_int] :
( ( tb2t(get2(int,t2tb1(A_85),$sum(Y_87a,I_91a))) = tb2t(get2(int,t2tb1(A_85),$sum(X_86a,I_91a))) )
| ~ is_common_prefix1(A_85,X_86a,Y_87a,L_88a)
| ~ $lesseq(0,I_91a)
| ~ $less(I_91a,L_88a) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_166,plain,
! [X_86a: $int,Y_87a: $int,L_88a: $int,I_91a: $int,A_85: array_int] :
( ( tb2t(get2(int,t2tb1(A_85),$sum(I_91a,Y_87a))) = tb2t(get2(int,t2tb1(A_85),$sum(I_91a,X_86a))) )
| ~ is_common_prefix1(A_85,X_86a,Y_87a,L_88a)
| $less(I_91a,0)
| ~ $less(I_91a,L_88a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_63]) ).
tff(c_593100,plain,
! [A_59130: array_int,I_59133a: $int,L_59131a: $int,X_59132a: $int,Y_59134a: $int] :
( ( tb2t(get2(int,t2tb1(A_59130),$sum(Y_59134a,I_59133a))) = tb2t(get2(int,t2tb1(A_59130),$sum(X_59132a,I_59133a))) )
| ~ is_common_prefix1(A_59130,X_59132a,Y_59134a,L_59131a)
| $less(I_59133a,0)
| ~ $less(I_59133a,L_59131a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_166]) ).
tff(c_593104,plain,
! [I_59133a: $int] :
( ( tb2t(get2(int,t2tb1('#skF_3'),$sum('#skF_5',I_59133a))) = tb2t(get2(int,t2tb1('#skF_3'),$sum('#skF_4',I_59133a))) )
| $less(I_59133a,0)
| ~ $less(I_59133a,'#skE_20') ),
inference(resolution,[status(thm)],[c_592560,c_593100]) ).
tff(c_593632,plain,
! [I_59162a: $int] :
( ( tb2t(get2(int,t2tb1('#skF_3'),$sum(I_59162a,'#skF_5'))) = tb2t(get2(int,t2tb1('#skF_3'),$sum(I_59162a,'#skF_4'))) )
| $less(I_59162a,0)
| ~ $less(I_59162a,'#skE_20') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_593104]) ).
tff(c_593641,plain,
! [I_59162a: $int] :
( ( get2(int,t2tb1('#skF_3'),$sum(I_59162a,'#skF_5')) = t2tb(tb2t(get2(int,t2tb1('#skF_3'),$sum(I_59162a,'#skF_4')))) )
| $less(I_59162a,0)
| ~ $less(I_59162a,'#skE_20') ),
inference(superposition,[status(thm),theory(equality)],[c_593632,c_175]) ).
tff(c_593652,plain,
! [I_59162a: $int] :
( ( get2(int,t2tb1('#skF_3'),$sum(I_59162a,'#skF_5')) = get2(int,t2tb1('#skF_3'),$sum(I_59162a,'#skF_4')) )
| $less(I_59162a,0)
| ~ $less(I_59162a,'#skE_20') ),
inference(demodulation,[status(thm),theory(equality)],[c_175,c_593641]) ).
tff(c_601580,plain,
! [I_59762a: $int] :
( ( get2(int,t2tb1('#skF_3'),$sum('#skF_5',I_59762a)) = get2(int,t2tb1('#skF_3'),$sum('#skF_4',I_59762a)) )
| $less(I_59762a,0)
| ~ $less(I_59762a,'#skE_20') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_593652]) ).
tff(c_594712,plain,
tb2t(get2(int,t2tb1('#skF_3'),$sum('#skF_5','#skE_21'))) = '#skE_22',
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_594707]) ).
tff(c_601592,plain,
( ( tb2t(get2(int,t2tb1('#skF_3'),$sum('#skF_4','#skE_21'))) = '#skE_22' )
| $less('#skE_21',0)
| ~ $less('#skE_21','#skE_20') ),
inference(superposition,[status(thm),theory(equality)],[c_601580,c_594712]) ).
tff(c_601623,plain,
( ( '#skE_23' = '#skE_22' )
| $less('#skE_21',0)
| ~ $less('#skE_21','#skE_20') ),
inference(demodulation,[status(thm),theory(equality)],[c_594714,c_601592]) ).
tff(c_601625,plain,
~ $less('#skE_21','#skE_20'),
inference(negUnitSimplification,[status(thm)],[c_599475,c_599850,c_601623]) ).
tff(c_592114,plain,
'#skF_2'('#skF_3','#skF_4','#skF_5','#skF_6') = '#skE_20',
inference(define,[status(thm),theory(equality)],[c_592113]) ).
tff(c_592118,plain,
$less('#skF_6','#skE_20'),
inference(demodulation,[status(thm),theory(equality)],[c_592114,c_592113]) ).
tff(c_604133,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_604132,c_601625,c_592118]) ).
tff(c_604134,plain,
( $less('#skE_19',$sum(1,$sum('#skF_5','#skF_6')))
| $less('#skE_19',$sum(1,$sum('#skF_4','#skF_6'))) ),
inference(splitRight,[status(thm)],[c_594369]) ).
tff(c_604137,plain,
( $less('#skE_19',$sum(1,$sum('#skF_6','#skF_5')))
| $less('#skE_19',$sum(1,$sum('#skF_6','#skF_4'))) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_604134]) ).
tff(c_604193,plain,
$less('#skE_19',$sum(1,$sum('#skF_6','#skF_4'))),
inference(splitLeft,[status(thm)],[c_604137]) ).
tff(c_604195,plain,
$less('#skE_19',$sum(1,$sum('#skF_4','#skF_6'))),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_604193]) ).
tff(c_211,plain,
! [A_85: array_int,X_86a: $int,L_88a: $int,Y_87a: $int] :
( ~ $less(length1(int,t2tb1(A_85)),$sum(X_86a,L_88a))
| ~ is_common_prefix1(A_85,X_86a,Y_87a,L_88a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_156]) ).
tff(c_592568,plain,
~ $less(length1(int,t2tb1('#skF_3')),$sum('#skF_4','#skE_20')),
inference(resolution,[status(thm)],[c_592560,c_211]) ).
tff(c_592576,plain,
~ $less('#skE_19',$sum('#skF_4','#skE_20')),
inference(demodulation,[status(thm),theory(equality)],[c_591769,c_592568]) ).
tff(c_604196,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_604195,c_592576,c_592118]) ).
tff(c_604197,plain,
$less('#skE_19',$sum(1,$sum('#skF_6','#skF_5'))),
inference(splitRight,[status(thm)],[c_604137]) ).
tff(c_604200,plain,
$less('#skE_19',$sum(1,$sum('#skF_5','#skF_6'))),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_604197]) ).
tff(c_66,plain,
! [Y_87a: $int,L_88a: $int,A_85: array_int,X_86a: $int] :
( $lesseq($sum(Y_87a,L_88a),length1(int,t2tb1(A_85)))
| ~ is_common_prefix1(A_85,X_86a,Y_87a,L_88a) ),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_161,plain,
! [A_85: array_int,L_88a: $int,Y_87a: $int,X_86a: $int] :
( ~ $less(length1(int,t2tb1(A_85)),$sum(L_88a,Y_87a))
| ~ is_common_prefix1(A_85,X_86a,Y_87a,L_88a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_66]) ).
tff(c_213,plain,
! [A_85: array_int,Y_87a: $int,L_88a: $int,X_86a: $int] :
( ~ $less(length1(int,t2tb1(A_85)),$sum(Y_87a,L_88a))
| ~ is_common_prefix1(A_85,X_86a,Y_87a,L_88a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_161]) ).
tff(c_592564,plain,
~ $less(length1(int,t2tb1('#skF_3')),$sum('#skF_5','#skE_20')),
inference(resolution,[status(thm)],[c_592560,c_213]) ).
tff(c_592574,plain,
~ $less('#skE_19',$sum('#skF_5','#skE_20')),
inference(demodulation,[status(thm),theory(equality)],[c_591769,c_592564]) ).
tff(c_604203,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_604200,c_592574,c_592118]) ).
tff(c_604204,plain,
( $less('#skF_6',$uminus(1))
| $less('#skE_19',$sum(1,$sum('#skF_6','#skF_4')))
| $less('#skE_19',$sum(1,$sum('#skF_6','#skF_5'))) ),
inference(splitRight,[status(thm)],[c_594716]) ).
tff(c_604207,plain,
( $less('#skF_6',$uminus(1))
| $less('#skE_19',$sum(1,$sum('#skF_4','#skF_6')))
| $less('#skE_19',$sum(1,$sum('#skF_5','#skF_6'))) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_604204]) ).
tff(c_608464,plain,
$less('#skE_19',$sum(1,$sum('#skF_5','#skF_6'))),
inference(splitLeft,[status(thm)],[c_604207]) ).
tff(c_608466,plain,
$less('#skE_19',$sum(1,$sum('#skF_6','#skF_5'))),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_608464]) ).
tff(c_608467,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_608466,c_592574,c_592118]) ).
tff(c_608468,plain,
( $less('#skE_19',$sum(1,$sum('#skF_4','#skF_6')))
| $less('#skF_6',$uminus(1)) ),
inference(splitRight,[status(thm)],[c_604207]) ).
tff(c_608471,plain,
( $less('#skE_19',$sum(1,$sum('#skF_6','#skF_4')))
| $less('#skF_6',$uminus(1)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_608468]) ).
tff(c_608475,plain,
$less('#skF_6',$uminus(1)),
inference(splitLeft,[status(thm)],[c_608471]) ).
tff(c_608476,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_608475,c_591049]) ).
tff(c_608477,plain,
$less('#skE_19',$sum(1,$sum('#skF_6','#skF_4'))),
inference(splitRight,[status(thm)],[c_608471]) ).
tff(c_608480,plain,
$less('#skE_19',$sum(1,$sum('#skF_4','#skF_6'))),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_608477]) ).
tff(c_608481,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_608480,c_592576,c_592118]) ).
tff(c_608486,plain,
$less('#skE_21',0),
inference(splitRight,[status(thm)],[c_594037]) ).
tff(c_176,plain,
! [I_63a: $int] : ( tb2t(t2tb(I_63a)) = I_63a ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_594935,plain,
get2(int,t2tb1('#skF_3'),$sum('#skF_5','#skE_21')) = t2tb('#skE_22'),
inference(superposition,[status(thm),theory(equality)],[c_594712,c_175]) ).
tff(c_594940,plain,
get2(int,t2tb1('#skF_3'),$sum('#skE_21','#skF_5')) = t2tb('#skE_22'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_594935]) ).
tff(c_593108,plain,
! [I_59133a: $int] :
( ( tb2t(get2(int,t2tb1('#skF_3'),$sum('#skF_5',I_59133a))) = tb2t(get2(int,t2tb1('#skF_3'),$sum('#skF_4',I_59133a))) )
| $less(I_59133a,0)
| ~ $less(I_59133a,'#skF_6') ),
inference(resolution,[status(thm)],[c_196,c_593100]) ).
tff(c_593112,plain,
! [I_59133a: $int] :
( ( tb2t(get2(int,t2tb1('#skF_3'),$sum(I_59133a,'#skF_5'))) = tb2t(get2(int,t2tb1('#skF_3'),$sum(I_59133a,'#skF_4'))) )
| $less(I_59133a,0)
| ~ $less(I_59133a,'#skF_6') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_593108]) ).
tff(c_595898,plain,
( ( tb2t(get2(int,t2tb1('#skF_3'),$sum('#skE_21','#skF_4'))) = tb2t(t2tb('#skE_22')) )
| $less('#skE_21',0)
| ~ $less('#skE_21','#skF_6') ),
inference(superposition,[status(thm),theory(equality)],[c_594940,c_593112]) ).
tff(c_595913,plain,
( ( tb2t(get2(int,t2tb1('#skF_3'),$sum('#skE_21','#skF_4'))) = '#skE_22' )
| $less('#skE_21',0)
| ~ $less('#skE_21','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_176,c_595898]) ).
tff(c_595915,plain,
( ( tb2t(get2(int,t2tb1('#skF_3'),$sum('#skF_4','#skE_21'))) = '#skE_22' )
| $less('#skE_21',0)
| ~ $less('#skE_21','#skF_6') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_595913]) ).
tff(c_597119,plain,
( ( '#skE_23' = '#skE_22' )
| $less('#skE_21',0)
| ~ $less('#skE_21','#skF_6') ),
inference(demodulation,[status(thm),theory(equality)],[c_594714,c_595915]) ).
tff(c_597121,plain,
~ $less('#skE_21','#skF_6'),
inference(splitLeft,[status(thm)],[c_597119]) ).
tff(c_608510,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_608486,c_597121,c_591049]) ).
tff(c_608513,plain,
( $less('#skE_21',0)
| ( '#skE_23' = '#skE_22' ) ),
inference(splitRight,[status(thm)],[c_597119]) ).
tff(c_609021,plain,
'#skE_23' = '#skE_22',
inference(splitLeft,[status(thm)],[c_608513]) ).
tff(c_610840,plain,
( $less('#skE_19',$sum(1,$sum('#skF_6','#skF_5')))
| $less('#skE_19',$sum(1,$sum('#skF_6','#skF_4')))
| $less('#skF_6',$uminus(1)) ),
inference(demodulation,[status(thm),theory(equality)],[c_609021,c_594716]) ).
tff(c_610842,plain,
( $less('#skE_19',$sum(1,$sum('#skF_5','#skF_6')))
| $less('#skE_19',$sum(1,$sum('#skF_4','#skF_6')))
| $less('#skF_6',$uminus(1)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_610840]) ).
tff(c_610844,plain,
$less('#skF_6',$uminus(1)),
inference(splitLeft,[status(thm)],[c_610842]) ).
tff(c_610845,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_610844,c_591049]) ).
tff(c_610846,plain,
( $less('#skE_19',$sum(1,$sum('#skF_4','#skF_6')))
| $less('#skE_19',$sum(1,$sum('#skF_5','#skF_6'))) ),
inference(splitRight,[status(thm)],[c_610842]) ).
tff(c_610849,plain,
( $less('#skE_19',$sum(1,$sum('#skF_6','#skF_4')))
| $less('#skE_19',$sum(1,$sum('#skF_6','#skF_5'))) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_610846]) ).
tff(c_616630,plain,
$less('#skE_19',$sum(1,$sum('#skF_6','#skF_5'))),
inference(splitLeft,[status(thm)],[c_610849]) ).
tff(c_616632,plain,
$less('#skE_19',$sum(1,$sum('#skF_5','#skF_6'))),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_616630]) ).
tff(c_616633,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_616632,c_592574,c_592118]) ).
tff(c_616634,plain,
$less('#skE_19',$sum(1,$sum('#skF_6','#skF_4'))),
inference(splitRight,[status(thm)],[c_610849]) ).
tff(c_616637,plain,
$less('#skE_19',$sum(1,$sum('#skF_4','#skF_6'))),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_616634]) ).
tff(c_616640,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_616637,c_592576,c_592118]) ).
tff(c_616643,plain,
$less('#skE_21',0),
inference(splitRight,[status(thm)],[c_608513]) ).
tff(c_617930,plain,
( $less('#skE_19',$sum(1,$sum('#skF_6','#skF_5')))
| $less('#skE_19',$sum(1,$sum('#skF_6','#skF_4')))
| $less('#skF_6',$uminus(1)) ),
inference(demodulation,[status(thm),theory(equality)],[c_616643,c_594037]) ).
tff(c_617932,plain,
( $less('#skE_19',$sum(1,$sum('#skF_5','#skF_6')))
| $less('#skE_19',$sum(1,$sum('#skF_4','#skF_6')))
| $less('#skF_6',$uminus(1)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_617930]) ).
tff(c_617934,plain,
$less('#skF_6',$uminus(1)),
inference(splitLeft,[status(thm)],[c_617932]) ).
tff(c_617935,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_617934,c_591049]) ).
tff(c_617936,plain,
( $less('#skE_19',$sum(1,$sum('#skF_4','#skF_6')))
| $less('#skE_19',$sum(1,$sum('#skF_5','#skF_6'))) ),
inference(splitRight,[status(thm)],[c_617932]) ).
tff(c_617939,plain,
( $less('#skE_19',$sum(1,$sum('#skF_6','#skF_4')))
| $less('#skE_19',$sum(1,$sum('#skF_6','#skF_5'))) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_617936]) ).
tff(c_624189,plain,
$less('#skE_19',$sum(1,$sum('#skF_6','#skF_5'))),
inference(splitLeft,[status(thm)],[c_617939]) ).
tff(c_624191,plain,
$less('#skE_19',$sum(1,$sum('#skF_5','#skF_6'))),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_624189]) ).
tff(c_624192,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_624191,c_592574,c_592118]) ).
tff(c_624193,plain,
$less('#skE_19',$sum(1,$sum('#skF_6','#skF_4'))),
inference(splitRight,[status(thm)],[c_617939]) ).
tff(c_624196,plain,
$less('#skE_19',$sum(1,$sum('#skF_4','#skF_6'))),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_624193]) ).
tff(c_624199,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_624196,c_592576,c_592118]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SWW657_2 : TPTP v9.0.0. Released v6.1.0.
% 0.12/0.14 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.35 % Computer : n008.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Apr 9 06:21:17 EDT 2025
% 0.14/0.35 % CPUTime :
% 154.26/103.08 ***********************************************************************
% 154.26/103.08 After 101.2 sec it's time to try something different, got 99.0 sec left
% 154.26/103.08 ***********************************************************************
% 159.04/105.93 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 159.04/105.95
% 159.04/105.95 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------