%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW676_1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:31:06 PM UTC 2026
% Result : Theorem 19.99s 3.63s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 81
% Syntax : Number of formulae : 329 ( 53 unt; 0 typ; 78 def)
% Number of atoms : 1411 ( 335 equ)
% Maximal formula atoms : 37 ( 4 avg)
% Number of connectives : 1647 ( 565 ~; 760 |; 201 &)
% ( 76 <=>; 43 =>; 0 <=; 2 <~>)
% Maximal formula depth : 23 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 1176 ( 603 atm; 174 fun; 150 num; 249 var)
% Number of types : 3 ( 1 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 71 ( 65 usr; 66 prp; 0-3 aty)
% Number of functors : 43 ( 34 usr; 32 con; 0-3 aty)
% Number of variables : 270 ( 184 !; 86 ?; 270 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'Array[Int,Int]': $tType ).
tff(func_def_0,type,
'select:(Array[Int,Int]*Int)>Int': ( 'Array[Int,Int]' * $int ) > $int ).
tff(func_def_1,type,
'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]': ( 'Array[Int,Int]' * $int * $int ) > 'Array[Int,Int]' ).
tff(func_def_2,type,
'const:(Int)>Array[Int,Int]': $int > 'Array[Int,Int]' ).
tff(func_def_3,type,
length: 'Array[Int,Int]' > $int ).
tff(func_def_4,type,
div2: $int > $int ).
tff(func_def_12,type,
sK0: ( 'Array[Int,Int]' * 'Array[Int,Int]' ) > $int ).
tff(func_def_13,type,
sK1: $int ).
tff(func_def_14,type,
sK2: $int ).
tff(func_def_15,type,
sK3: $int ).
tff(func_def_16,type,
sK4: 'Array[Int,Int]' ).
tff(func_def_17,type,
sK5: $int ).
tff(func_def_18,type,
sK6: $int ).
tff(func_def_19,type,
sK7: $int ).
tff(func_def_20,type,
sK8: $int ).
tff(func_def_21,type,
sK9: $int ).
tff(func_def_22,type,
sK10: $int ).
tff(func_def_23,type,
sF11: $int ).
tff(func_def_24,type,
sF12: $int ).
tff(func_def_25,type,
sF13: $int ).
tff(func_def_26,type,
sF14: $int ).
tff(func_def_27,type,
sF15: $int ).
tff(func_def_28,type,
sF16: $int ).
tff(func_def_29,type,
sF17: $int ).
tff(func_def_30,type,
sF18: $int ).
tff(func_def_31,type,
sF19: $int ).
tff(func_def_32,type,
sF20: $int ).
tff(func_def_33,type,
sF21: $int ).
tff(func_def_34,type,
sF22: $int ).
tff(func_def_35,type,
sF23: $int ).
tff(func_def_36,type,
sF24: $int ).
tff(func_def_37,type,
2: $int > $int ).
tff(func_def_40,type,
'$inst26': $int ).
tff(func_def_41,type,
'$inst27': $int ).
tff(func_def_42,type,
'$inst28': $int ).
tff(func_def_43,type,
'$inst29': $int ).
tff(pred_def_1,type,
sorted: ( 'Array[Int,Int]' * $int * $int ) > $o ).
tff(f5,axiom,
! [X1: $int,X0: $int] :
( ( $lesseq($product(2,X1),X0)
& $greater($product(2,$sum(X1,1)),X0) )
<=> ( div2(X0) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_004) ).
tff(f7,axiom,
! [X0: 'Array[Int,Int]',X2: $int,X1: $int] :
( sorted(X0,X1,X2)
<=> ! [X3: $int,X4: $int] :
( ( $less(X3,X4)
& $lesseq(X1,X3)
& $lesseq(X4,X2) )
=> $lesseq('select:(Array[Int,Int]*Int)>Int'(X0,X3),'select:(Array[Int,Int]*Int)>Int'(X0,X4)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_006) ).
tff(f8,conjecture,
! [X1: $int,X2: 'Array[Int,Int]',X0: $int,X3: $int] :
( ( sorted(X2,0,$difference(length(X2),1))
& $less(X1,length(X2))
& $lesseq(0,X0) )
=> ( ? [X6: $int] :
( $lesseq(X0,X6)
& ( 'select:(Array[Int,Int]*Int)>Int'(X2,X6) = X3 )
& $lesseq(X6,X1) )
<=> ( ( ~ $greater(X0,X1)
=> ? [X4: $int] :
( ( ( 'select:(Array[Int,Int]*Int)>Int'(X2,X4) = X3 )
=> $true )
& ( ( 'select:(Array[Int,Int]*Int)>Int'(X2,X4) != X3 )
=> ( ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X2,X4),X3)
=> ? [X7: $int] :
( ( X7 = $difference(X4,1) )
& ? [X6: $int] :
( $lesseq(X6,X7)
& $lesseq(X0,X6)
& ( 'select:(Array[Int,Int]*Int)>Int'(X2,X6) = X3 ) ) ) )
& ( $less('select:(Array[Int,Int]*Int)>Int'(X2,X4),X3)
=> ? [X5: $int] :
( ( X5 = $sum(X4,1) )
& ? [X6: $int] :
( $lesseq(X5,X6)
& $lesseq(X6,X1)
& ( 'select:(Array[Int,Int]*Int)>Int'(X2,X6) = X3 ) ) ) ) ) )
& ( X4 = div2($sum(X0,X1)) ) ) )
& ( $greater(X0,X1)
=> $false ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_007) ).
tff(f9,negated_conjecture,
~ ! [X1: $int,X2: 'Array[Int,Int]',X0: $int,X3: $int] :
( ( sorted(X2,0,$difference(length(X2),1))
& $less(X1,length(X2))
& $lesseq(0,X0) )
=> ( ? [X6: $int] :
( $lesseq(X0,X6)
& ( 'select:(Array[Int,Int]*Int)>Int'(X2,X6) = X3 )
& $lesseq(X6,X1) )
<=> ( ( ~ $greater(X0,X1)
=> ? [X4: $int] :
( ( ( 'select:(Array[Int,Int]*Int)>Int'(X2,X4) = X3 )
=> $true )
& ( ( 'select:(Array[Int,Int]*Int)>Int'(X2,X4) != X3 )
=> ( ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X2,X4),X3)
=> ? [X7: $int] :
( ( X7 = $difference(X4,1) )
& ? [X6: $int] :
( $lesseq(X6,X7)
& $lesseq(X0,X6)
& ( 'select:(Array[Int,Int]*Int)>Int'(X2,X6) = X3 ) ) ) )
& ( $less('select:(Array[Int,Int]*Int)>Int'(X2,X4),X3)
=> ? [X5: $int] :
( ( X5 = $sum(X4,1) )
& ? [X6: $int] :
( $lesseq(X5,X6)
& $lesseq(X6,X1)
& ( 'select:(Array[Int,Int]*Int)>Int'(X2,X6) = X3 ) ) ) ) ) )
& ( X4 = div2($sum(X0,X1)) ) ) )
& ( $greater(X0,X1)
=> $false ) ) ) ),
inference(negated_conjecture,[status(cth)],[f8]) ).
tff(f10,plain,
! [X1: $int,X0: $int] :
( ( ~ $less(X0,$product(2,X1))
& $less(X0,$product(2,$sum(X1,1))) )
<=> ( div2(X0) = X1 ) ),
inference(theory_normalization,[],[f5]) ).
tff(f11,plain,
~ ! [X1: $int,X2: 'Array[Int,Int]',X0: $int,X3: $int] :
( ( sorted(X2,0,$sum(length(X2),$uminus(1)))
& $less(X1,length(X2))
& ~ $less(X0,0) )
=> ( ? [X6: $int] :
( ~ $less(X6,X0)
& ( 'select:(Array[Int,Int]*Int)>Int'(X2,X6) = X3 )
& ~ $less(X1,X6) )
<=> ( ( ~ $less(X1,X0)
=> ? [X4: $int] :
( ( ( 'select:(Array[Int,Int]*Int)>Int'(X2,X4) = X3 )
=> $true )
& ( ( 'select:(Array[Int,Int]*Int)>Int'(X2,X4) != X3 )
=> ( ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X2,X4),X3)
=> ? [X7: $int] :
( ( $sum(X4,$uminus(1)) = X7 )
& ? [X6: $int] :
( ~ $less(X7,X6)
& ~ $less(X6,X0)
& ( 'select:(Array[Int,Int]*Int)>Int'(X2,X6) = X3 ) ) ) )
& ( $less('select:(Array[Int,Int]*Int)>Int'(X2,X4),X3)
=> ? [X5: $int] :
( ( X5 = $sum(X4,1) )
& ? [X6: $int] :
( ~ $less(X6,X5)
& ~ $less(X1,X6)
& ( 'select:(Array[Int,Int]*Int)>Int'(X2,X6) = X3 ) ) ) ) ) )
& ( X4 = div2($sum(X0,X1)) ) ) )
& ( $less(X1,X0)
=> $false ) ) ) ),
inference(theory_normalization,[],[f9]) ).
tff(f13,plain,
! [X0: 'Array[Int,Int]',X2: $int,X1: $int] :
( sorted(X0,X1,X2)
<=> ! [X3: $int,X4: $int] :
( ( $less(X3,X4)
& ~ $less(X3,X1)
& ~ $less(X2,X4) )
=> ~ $less('select:(Array[Int,Int]*Int)>Int'(X0,X4),'select:(Array[Int,Int]*Int)>Int'(X0,X3)) ) ),
inference(theory_normalization,[],[f7]) ).
tff(f32,plain,
! [X0: $int,X1: $int] :
( ( div2(X1) = X0 )
<=> ( $less(X1,$product(2,$sum(X0,1)))
& ~ $less(X1,$product(2,X0)) ) ),
inference(rectify,[],[f10]) ).
tff(f33,plain,
~ ! [X0: $int,X1: 'Array[Int,Int]',X2: $int,X3: $int] :
( ( ~ $less(X2,0)
& sorted(X1,0,$sum(length(X1),$uminus(1)))
& $less(X0,length(X1)) )
=> ( ? [X4: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X4) = X3 )
& ~ $less(X4,X2)
& ~ $less(X0,X4) )
<=> ( ( ~ $less(X0,X2)
=> ? [X5: $int] :
( ( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X5) = X3 )
=> $true )
& ( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X5) != X3 )
=> ( ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
=> ? [X6: $int] :
( ? [X7: $int] :
( ~ $less(X6,X7)
& ( 'select:(Array[Int,Int]*Int)>Int'(X1,X7) = X3 )
& ~ $less(X7,X2) )
& ( $sum(X5,$uminus(1)) = X6 ) ) )
& ( $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
=> ? [X8: $int] :
( ? [X9: $int] :
( ~ $less(X9,X8)
& ( 'select:(Array[Int,Int]*Int)>Int'(X1,X9) = X3 )
& ~ $less(X0,X9) )
& ( $sum(X5,1) = X8 ) ) ) ) )
& ( div2($sum(X2,X0)) = X5 ) ) )
& ( $less(X0,X2)
=> $false ) ) ) ),
inference(rectify,[],[f11]) ).
tff(f34,plain,
~ ! [X0: $int,X1: 'Array[Int,Int]',X2: $int,X3: $int] :
( ( ~ $less(X2,0)
& sorted(X1,0,$sum(length(X1),$uminus(1)))
& $less(X0,length(X1)) )
=> ( ? [X4: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X4) = X3 )
& ~ $less(X4,X2)
& ~ $less(X0,X4) )
<=> ( ( ~ $less(X0,X2)
=> ? [X5: $int] :
( ( div2($sum(X2,X0)) = X5 )
& ( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X5) != X3 )
=> ( ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
=> ? [X6: $int] :
( ? [X7: $int] :
( ~ $less(X6,X7)
& ( 'select:(Array[Int,Int]*Int)>Int'(X1,X7) = X3 )
& ~ $less(X7,X2) )
& ( $sum(X5,$uminus(1)) = X6 ) ) )
& ( $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
=> ? [X8: $int] :
( ? [X9: $int] :
( ~ $less(X9,X8)
& ( 'select:(Array[Int,Int]*Int)>Int'(X1,X9) = X3 )
& ~ $less(X0,X9) )
& ( $sum(X5,1) = X8 ) ) ) ) ) ) )
& ~ $less(X0,X2) ) ) ),
inference(true_and_false_elimination,[],[f33]) ).
tff(f35,plain,
~ ! [X2: $int,X0: $int,X3: $int,X1: 'Array[Int,Int]'] :
( ( ~ $less(X2,0)
& sorted(X1,0,$sum(length(X1),$uminus(1)))
& $less(X0,length(X1)) )
=> ( ? [X4: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X4) = X3 )
& ~ $less(X4,X2)
& ~ $less(X0,X4) )
<=> ( ~ $less(X0,X2)
& ( ~ $less(X0,X2)
=> ? [X5: $int] :
( ( div2($sum(X2,X0)) = X5 )
& ( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X5) != X3 )
=> ( ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
=> ? [X6: $int] :
( ? [X7: $int] :
( ~ $less(X6,X7)
& ( 'select:(Array[Int,Int]*Int)>Int'(X1,X7) = X3 )
& ~ $less(X7,X2) )
& ( $sum(X5,$uminus(1)) = X6 ) ) )
& ( $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
=> ? [X8: $int] :
( ? [X9: $int] :
( ~ $less(X9,X8)
& ( 'select:(Array[Int,Int]*Int)>Int'(X1,X9) = X3 )
& ~ $less(X0,X9) )
& ( $sum(X5,1) = X8 ) ) ) ) ) ) ) ) ) ),
inference(flattening,[],[f34]) ).
tff(f38,plain,
! [X1: $int,X2: $int,X0: 'Array[Int,Int]'] :
( sorted(X0,X2,X1)
<=> ! [X4: $int,X3: $int] :
( ( $less(X3,X4)
& ~ $less(X3,X2)
& ~ $less(X1,X4) )
=> ~ $less('select:(Array[Int,Int]*Int)>Int'(X0,X4),'select:(Array[Int,Int]*Int)>Int'(X0,X3)) ) ),
inference(rectify,[],[f13]) ).
tff(f40,plain,
! [X1: $int,X2: $int,X0: 'Array[Int,Int]'] :
( sorted(X0,X2,X1)
=> ! [X4: $int,X3: $int] :
( ( $less(X3,X4)
& ~ $less(X3,X2)
& ~ $less(X1,X4) )
=> ~ $less('select:(Array[Int,Int]*Int)>Int'(X0,X4),'select:(Array[Int,Int]*Int)>Int'(X0,X3)) ) ),
inference(unused_predicate_definition_removal,[],[f38]) ).
tff(f42,plain,
! [X1: $int,X2: $int,X0: 'Array[Int,Int]'] :
( ! [X4: $int,X3: $int] :
( ~ $less('select:(Array[Int,Int]*Int)>Int'(X0,X4),'select:(Array[Int,Int]*Int)>Int'(X0,X3))
| ~ $less(X3,X4)
| $less(X3,X2)
| $less(X1,X4) )
| ~ sorted(X0,X2,X1) ),
inference(ennf_transformation,[],[f40]) ).
tff(f43,plain,
! [X2: $int,X0: 'Array[Int,Int]',X1: $int] :
( ! [X3: $int,X4: $int] :
( $less(X3,X2)
| ~ $less('select:(Array[Int,Int]*Int)>Int'(X0,X4),'select:(Array[Int,Int]*Int)>Int'(X0,X3))
| $less(X1,X4)
| ~ $less(X3,X4) )
| ~ sorted(X0,X2,X1) ),
inference(flattening,[],[f42]) ).
tff(f44,plain,
? [X2: $int,X0: $int,X3: $int,X1: 'Array[Int,Int]'] :
( ( ( ( ? [X5: $int] :
( ( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X5) = X3 )
| ( ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
| ? [X8: $int] :
( ? [X9: $int] :
( ~ $less(X9,X8)
& ( 'select:(Array[Int,Int]*Int)>Int'(X1,X9) = X3 )
& ~ $less(X0,X9) )
& ( $sum(X5,1) = X8 ) ) )
& ( $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
| ? [X6: $int] :
( ? [X7: $int] :
( ~ $less(X6,X7)
& ( 'select:(Array[Int,Int]*Int)>Int'(X1,X7) = X3 )
& ~ $less(X7,X2) )
& ( $sum(X5,$uminus(1)) = X6 ) ) ) ) )
& ( div2($sum(X2,X0)) = X5 ) )
| $less(X0,X2) )
& ~ $less(X0,X2) )
<~> ? [X4: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X4) = X3 )
& ~ $less(X4,X2)
& ~ $less(X0,X4) ) )
& ~ $less(X2,0)
& sorted(X1,0,$sum(length(X1),$uminus(1)))
& $less(X0,length(X1)) ),
inference(ennf_transformation,[],[f35]) ).
tff(f45,plain,
? [X0: $int,X2: $int,X3: $int,X1: 'Array[Int,Int]'] :
( ( ( ( ? [X5: $int] :
( ( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X5) = X3 )
| ( ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
| ? [X8: $int] :
( ? [X9: $int] :
( ~ $less(X9,X8)
& ( 'select:(Array[Int,Int]*Int)>Int'(X1,X9) = X3 )
& ~ $less(X0,X9) )
& ( $sum(X5,1) = X8 ) ) )
& ( $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
| ? [X6: $int] :
( ? [X7: $int] :
( ~ $less(X6,X7)
& ( 'select:(Array[Int,Int]*Int)>Int'(X1,X7) = X3 )
& ~ $less(X7,X2) )
& ( $sum(X5,$uminus(1)) = X6 ) ) ) ) )
& ( div2($sum(X2,X0)) = X5 ) )
| $less(X0,X2) )
& ~ $less(X0,X2) )
<~> ? [X4: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X4) = X3 )
& ~ $less(X4,X2)
& ~ $less(X0,X4) ) )
& $less(X0,length(X1))
& sorted(X1,0,$sum(length(X1),$uminus(1)))
& ~ $less(X2,0) ),
inference(flattening,[],[f44]) ).
tff(f49,plain,
! [X0: $int,X1: $int] :
( ( ( div2(X1) = X0 )
| ~ $less(X1,$product(2,$sum(X0,1)))
| $less(X1,$product(2,X0)) )
& ( ( $less(X1,$product(2,$sum(X0,1)))
& ~ $less(X1,$product(2,X0)) )
| ( div2(X1) != X0 ) ) ),
inference(nnf_transformation,[],[f32]) ).
tff(f50,plain,
! [X0: $int,X1: $int] :
( ( ( div2(X1) = X0 )
| ~ $less(X1,$product(2,$sum(X0,1)))
| $less(X1,$product(2,X0)) )
& ( ( $less(X1,$product(2,$sum(X0,1)))
& ~ $less(X1,$product(2,X0)) )
| ( div2(X1) != X0 ) ) ),
inference(flattening,[],[f49]) ).
tff(f52,plain,
! [X0: $int,X1: 'Array[Int,Int]',X2: $int] :
( ! [X3: $int,X4: $int] :
( $less(X3,X0)
| ~ $less('select:(Array[Int,Int]*Int)>Int'(X1,X4),'select:(Array[Int,Int]*Int)>Int'(X1,X3))
| $less(X2,X4)
| ~ $less(X3,X4) )
| ~ sorted(X1,X0,X2) ),
inference(rectify,[],[f43]) ).
tff(f53,plain,
? [X0: $int,X2: $int,X3: $int,X1: 'Array[Int,Int]'] :
( ( ! [X4: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X4) != X3 )
| $less(X4,X2)
| $less(X0,X4) )
| ( ! [X5: $int] :
( ( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X5) != X3 )
& ( ( $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
& ! [X8: $int] :
( ! [X9: $int] :
( $less(X9,X8)
| ( 'select:(Array[Int,Int]*Int)>Int'(X1,X9) != X3 )
| $less(X0,X9) )
| ( $sum(X5,1) != X8 ) ) )
| ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
& ! [X6: $int] :
( ! [X7: $int] :
( $less(X6,X7)
| ( 'select:(Array[Int,Int]*Int)>Int'(X1,X7) != X3 )
| $less(X7,X2) )
| ( $sum(X5,$uminus(1)) != X6 ) ) ) ) )
| ( div2($sum(X2,X0)) != X5 ) )
& ~ $less(X0,X2) )
| $less(X0,X2) )
& ( ? [X4: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X4) = X3 )
& ~ $less(X4,X2)
& ~ $less(X0,X4) )
| ( ( ? [X5: $int] :
( ( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X5) = X3 )
| ( ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
| ? [X8: $int] :
( ? [X9: $int] :
( ~ $less(X9,X8)
& ( 'select:(Array[Int,Int]*Int)>Int'(X1,X9) = X3 )
& ~ $less(X0,X9) )
& ( $sum(X5,1) = X8 ) ) )
& ( $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
| ? [X6: $int] :
( ? [X7: $int] :
( ~ $less(X6,X7)
& ( 'select:(Array[Int,Int]*Int)>Int'(X1,X7) = X3 )
& ~ $less(X7,X2) )
& ( $sum(X5,$uminus(1)) = X6 ) ) ) ) )
& ( div2($sum(X2,X0)) = X5 ) )
| $less(X0,X2) )
& ~ $less(X0,X2) ) )
& $less(X0,length(X1))
& sorted(X1,0,$sum(length(X1),$uminus(1)))
& ~ $less(X2,0) ),
inference(nnf_transformation,[],[f45]) ).
tff(f54,plain,
? [X0: $int,X2: $int,X3: $int,X1: 'Array[Int,Int]'] :
( ( ! [X4: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X4) != X3 )
| $less(X4,X2)
| $less(X0,X4) )
| ( ! [X5: $int] :
( ( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X5) != X3 )
& ( ( $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
& ! [X8: $int] :
( ! [X9: $int] :
( $less(X9,X8)
| ( 'select:(Array[Int,Int]*Int)>Int'(X1,X9) != X3 )
| $less(X0,X9) )
| ( $sum(X5,1) != X8 ) ) )
| ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
& ! [X6: $int] :
( ! [X7: $int] :
( $less(X6,X7)
| ( 'select:(Array[Int,Int]*Int)>Int'(X1,X7) != X3 )
| $less(X7,X2) )
| ( $sum(X5,$uminus(1)) != X6 ) ) ) ) )
| ( div2($sum(X2,X0)) != X5 ) )
& ~ $less(X0,X2) )
| $less(X0,X2) )
& ( ? [X4: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X4) = X3 )
& ~ $less(X4,X2)
& ~ $less(X0,X4) )
| ( ( ? [X5: $int] :
( ( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X5) = X3 )
| ( ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
| ? [X8: $int] :
( ? [X9: $int] :
( ~ $less(X9,X8)
& ( 'select:(Array[Int,Int]*Int)>Int'(X1,X9) = X3 )
& ~ $less(X0,X9) )
& ( $sum(X5,1) = X8 ) ) )
& ( $less('select:(Array[Int,Int]*Int)>Int'(X1,X5),X3)
| ? [X6: $int] :
( ? [X7: $int] :
( ~ $less(X6,X7)
& ( 'select:(Array[Int,Int]*Int)>Int'(X1,X7) = X3 )
& ~ $less(X7,X2) )
& ( $sum(X5,$uminus(1)) = X6 ) ) ) ) )
& ( div2($sum(X2,X0)) = X5 ) )
| $less(X0,X2) )
& ~ $less(X0,X2) ) )
& $less(X0,length(X1))
& sorted(X1,0,$sum(length(X1),$uminus(1)))
& ~ $less(X2,0) ),
inference(flattening,[],[f53]) ).
tff(f55,plain,
? [X0: $int,X1: $int,X2: $int,X3: 'Array[Int,Int]'] :
( ( ! [X4: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(X3,X4) != X2 )
| $less(X4,X1)
| $less(X0,X4) )
| ( ! [X5: $int] :
( ( ( 'select:(Array[Int,Int]*Int)>Int'(X3,X5) != X2 )
& ( ( $less('select:(Array[Int,Int]*Int)>Int'(X3,X5),X2)
& ! [X6: $int] :
( ! [X7: $int] :
( $less(X7,X6)
| ( 'select:(Array[Int,Int]*Int)>Int'(X3,X7) != X2 )
| $less(X0,X7) )
| ( $sum(X5,1) != X6 ) ) )
| ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X3,X5),X2)
& ! [X8: $int] :
( ! [X9: $int] :
( $less(X8,X9)
| ( 'select:(Array[Int,Int]*Int)>Int'(X3,X9) != X2 )
| $less(X9,X1) )
| ( $sum(X5,$uminus(1)) != X8 ) ) ) ) )
| ( div2($sum(X1,X0)) != X5 ) )
& ~ $less(X0,X1) )
| $less(X0,X1) )
& ( ? [X10: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(X3,X10) = X2 )
& ~ $less(X10,X1)
& ~ $less(X0,X10) )
| ( ( ? [X11: $int] :
( ( ( 'select:(Array[Int,Int]*Int)>Int'(X3,X11) = X2 )
| ( ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X3,X11),X2)
| ? [X12: $int] :
( ? [X13: $int] :
( ~ $less(X13,X12)
& ( 'select:(Array[Int,Int]*Int)>Int'(X3,X13) = X2 )
& ~ $less(X0,X13) )
& ( $sum(X11,1) = X12 ) ) )
& ( $less('select:(Array[Int,Int]*Int)>Int'(X3,X11),X2)
| ? [X14: $int] :
( ? [X15: $int] :
( ~ $less(X14,X15)
& ( 'select:(Array[Int,Int]*Int)>Int'(X3,X15) = X2 )
& ~ $less(X15,X1) )
& ( $sum(X11,$uminus(1)) = X14 ) ) ) ) )
& ( div2($sum(X1,X0)) = X11 ) )
| $less(X0,X1) )
& ~ $less(X0,X1) ) )
& $less(X0,length(X3))
& sorted(X3,0,$sum(length(X3),$uminus(1)))
& ~ $less(X1,0) ),
inference(rectify,[],[f54]) ).
tff(f56,plain,
( ( ! [X4: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,X4) != sK3 )
| $less(X4,sK2)
| $less(sK1,X4) )
| ( ! [X5: $int] :
( ( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,X5) != sK3 )
& ( ( $less('select:(Array[Int,Int]*Int)>Int'(sK4,X5),sK3)
& ! [X6: $int] :
( ! [X7: $int] :
( $less(X7,X6)
| ( sK3 != 'select:(Array[Int,Int]*Int)>Int'(sK4,X7) )
| $less(sK1,X7) )
| ( $sum(X5,1) != X6 ) ) )
| ( ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,X5),sK3)
& ! [X8: $int] :
( ! [X9: $int] :
( $less(X8,X9)
| ( sK3 != 'select:(Array[Int,Int]*Int)>Int'(sK4,X9) )
| $less(X9,sK2) )
| ( $sum(X5,$uminus(1)) != X8 ) ) ) ) )
| ( div2($sum(sK2,sK1)) != X5 ) )
& ~ $less(sK1,sK2) )
| $less(sK1,sK2) )
& ( ( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK5) = sK3 )
& ~ $less(sK5,sK2)
& ~ $less(sK1,sK5) )
| ( ( ( ( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| ( ( ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ( ~ $less(sK8,sK7)
& ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK8) = sK3 )
& ~ $less(sK1,sK8)
& ( sK7 = $sum(sK6,1) ) ) )
& ( $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ( ~ $less(sK9,sK10)
& ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK10) = sK3 )
& ~ $less(sK10,sK2)
& ( $sum(sK6,$uminus(1)) = sK9 ) ) ) ) )
& ( div2($sum(sK2,sK1)) = sK6 ) )
| $less(sK1,sK2) )
& ~ $less(sK1,sK2) ) )
& $less(sK1,length(sK4))
& sorted(sK4,0,$sum(length(sK4),$uminus(1)))
& ~ $less(sK2,0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3),skolemize(X3,sK4),skolemize(X10,sK5),skolemize(X11,sK6),skolemize(X12,sK7),skolemize(X13,sK8),skolemize(X14,sK9),skolemize(X15,sK10)],[f55]) ).
tff(f59,plain,
! [X0: $int,X1: $int] :
( ~ $less(X1,$product(2,X0))
| ( div2(X1) != X0 ) ),
inference(cnf_transformation,[],[f50]) ).
tff(f60,plain,
! [X0: $int,X1: $int] :
( $less(X1,$product(2,$sum(X0,1)))
| ( div2(X1) != X0 ) ),
inference(cnf_transformation,[],[f50]) ).
tff(f64,plain,
! [X2: $int,X3: $int,X0: $int,X1: 'Array[Int,Int]',X4: $int] :
( $less(X3,X0)
| $less(X2,X4)
| ~ sorted(X1,X0,X2)
| ~ $less(X3,X4)
| ~ $less('select:(Array[Int,Int]*Int)>Int'(X1,X4),'select:(Array[Int,Int]*Int)>Int'(X1,X3)) ),
inference(cnf_transformation,[],[f52]) ).
tff(f66,plain,
~ $less(sK2,0),
inference(cnf_transformation,[],[f56]) ).
tff(f67,plain,
sorted(sK4,0,$sum(length(sK4),$uminus(1))),
inference(cnf_transformation,[],[f56]) ).
tff(f68,plain,
$less(sK1,length(sK4)),
inference(cnf_transformation,[],[f56]) ).
tff(f69,plain,
( ~ $less(sK1,sK5)
| ~ $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f70,plain,
( ~ $less(sK1,sK5)
| ( div2($sum(sK2,sK1)) = sK6 )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f71,plain,
( ~ $less(sK1,sK5)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ( $sum(sK6,$uminus(1)) = sK9 )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f72,plain,
( ~ $less(sK1,sK5)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ~ $less(sK10,sK2)
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f73,plain,
( ~ $less(sK1,sK5)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK10) = sK3 )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f74,plain,
( ~ $less(sK1,sK5)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ~ $less(sK9,sK10)
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f75,plain,
( ~ $less(sK1,sK5)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ( sK7 = $sum(sK6,1) )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f76,plain,
( ~ $less(sK1,sK5)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ~ $less(sK1,sK8)
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f77,plain,
( ~ $less(sK1,sK5)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK8) = sK3 )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f78,plain,
( ~ $less(sK1,sK5)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ~ $less(sK8,sK7)
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f79,plain,
( ~ $less(sK1,sK2)
| ~ $less(sK5,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f80,plain,
( ~ $less(sK5,sK2)
| ( div2($sum(sK2,sK1)) = sK6 )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f81,plain,
( ~ $less(sK5,sK2)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ( $sum(sK6,$uminus(1)) = sK9 )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f82,plain,
( ~ $less(sK5,sK2)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ~ $less(sK10,sK2)
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f83,plain,
( ~ $less(sK5,sK2)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK10) = sK3 )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f84,plain,
( ~ $less(sK5,sK2)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ~ $less(sK9,sK10)
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f85,plain,
( ~ $less(sK5,sK2)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ( sK7 = $sum(sK6,1) )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f86,plain,
( ~ $less(sK5,sK2)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ~ $less(sK1,sK8)
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f87,plain,
( ~ $less(sK5,sK2)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK8) = sK3 )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f88,plain,
( ~ $less(sK5,sK2)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ~ $less(sK8,sK7)
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f90,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK5) = sK3 )
| ( div2($sum(sK2,sK1)) = sK6 )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f91,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK5) = sK3 )
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ( $sum(sK6,$uminus(1)) = sK9 )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f92,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK5) = sK3 )
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ~ $less(sK10,sK2)
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f93,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK5) = sK3 )
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK10) = sK3 )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f94,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK5) = sK3 )
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ~ $less(sK9,sK10)
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f95,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK5) = sK3 )
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ( sK7 = $sum(sK6,1) )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f96,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK5) = sK3 )
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ~ $less(sK1,sK8)
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f97,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK5) = sK3 )
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK8) = sK3 )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f98,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK5) = sK3 )
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sK3 )
| ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,sK6),sK3)
| ~ $less(sK8,sK7)
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f101,plain,
! [X6: $int,X7: $int,X4: $int,X5: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,X4) != sK3 )
| $less(X4,sK2)
| $less(sK1,X4)
| $less(X7,X6)
| ( sK3 != 'select:(Array[Int,Int]*Int)>Int'(sK4,X7) )
| $less(sK1,X7)
| ( $sum(X5,1) != X6 )
| ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,X5),sK3)
| ( div2($sum(sK2,sK1)) != X5 )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f102,plain,
! [X8: $int,X9: $int,X4: $int,X5: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,X4) != sK3 )
| $less(X4,sK2)
| $less(sK1,X4)
| $less('select:(Array[Int,Int]*Int)>Int'(sK4,X5),sK3)
| $less(X8,X9)
| ( sK3 != 'select:(Array[Int,Int]*Int)>Int'(sK4,X9) )
| $less(X9,sK2)
| ( $sum(X5,$uminus(1)) != X8 )
| ( div2($sum(sK2,sK1)) != X5 )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f104,plain,
! [X4: $int,X5: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,X4) != sK3 )
| $less(X4,sK2)
| $less(sK1,X4)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,X5) != sK3 )
| ( div2($sum(sK2,sK1)) != X5 )
| $less(sK1,sK2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f106,plain,
! [X1: $int] : $less(X1,$product(2,$sum(div2(X1),1))),
inference(equality_resolution,[],[f60]) ).
tff(f107,plain,
! [X1: $int] : ~ $less(X1,$product(2,div2(X1))),
inference(equality_resolution,[],[f59]) ).
tff(f109,plain,
! [X4: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,X4) != sK3 )
| $less(X4,sK2)
| $less(sK1,X4)
| ( sK3 != 'select:(Array[Int,Int]*Int)>Int'(sK4,div2($sum(sK2,sK1))) )
| $less(sK1,sK2) ),
inference(equality_resolution,[],[f104]) ).
tff(f111,plain,
! [X9: $int,X4: $int,X5: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,X4) != sK3 )
| $less(X4,sK2)
| $less(sK1,X4)
| $less('select:(Array[Int,Int]*Int)>Int'(sK4,X5),sK3)
| $less($sum(X5,$uminus(1)),X9)
| ( sK3 != 'select:(Array[Int,Int]*Int)>Int'(sK4,X9) )
| $less(X9,sK2)
| ( div2($sum(sK2,sK1)) != X5 )
| $less(sK1,sK2) ),
inference(equality_resolution,[],[f102]) ).
tff(f112,plain,
! [X9: $int,X4: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,X4) != sK3 )
| $less(X4,sK2)
| $less(sK1,X4)
| $less('select:(Array[Int,Int]*Int)>Int'(sK4,div2($sum(sK2,sK1))),sK3)
| $less($sum(div2($sum(sK2,sK1)),$uminus(1)),X9)
| ( sK3 != 'select:(Array[Int,Int]*Int)>Int'(sK4,X9) )
| $less(X9,sK2)
| $less(sK1,sK2) ),
inference(equality_resolution,[],[f111]) ).
tff(f113,plain,
! [X7: $int,X4: $int,X5: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,X4) != sK3 )
| $less(X4,sK2)
| $less(sK1,X4)
| $less(X7,$sum(X5,1))
| ( sK3 != 'select:(Array[Int,Int]*Int)>Int'(sK4,X7) )
| $less(sK1,X7)
| ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,X5),sK3)
| ( div2($sum(sK2,sK1)) != X5 )
| $less(sK1,sK2) ),
inference(equality_resolution,[],[f101]) ).
tff(f114,plain,
! [X7: $int,X4: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,X4) != sK3 )
| $less(X4,sK2)
| $less(sK1,X4)
| $less(X7,$sum(div2($sum(sK2,sK1)),1))
| ( sK3 != 'select:(Array[Int,Int]*Int)>Int'(sK4,X7) )
| $less(sK1,X7)
| ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,div2($sum(sK2,sK1))),sK3)
| $less(sK1,sK2) ),
inference(equality_resolution,[],[f113]) ).
tff(f118,definition,
sF11 = $sum(sK2,sK1),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
tff(f119,plain,
$sum(sK2,sK1) = sF11,
inference(reorient_equations,[],[f118]) ).
tff(f120,definition,
sF12 = div2(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
tff(f121,definition,
sF13 = 'select:(Array[Int,Int]*Int)>Int'(sK4,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
tff(f122,plain,
! [X4: $int] :
( ( sF13 != sK3 )
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,X4) != sK3 )
| $less(sK1,X4)
| $less(sK1,sK2)
| $less(X4,sK2) ),
inference(definition_folding,[],[f109,f121,f120,f119]) ).
tff(f124,definition,
sF14 = $uminus(1),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f125,plain,
$uminus(1) = sF14,
inference(reorient_equations,[],[f124]) ).
tff(f126,definition,
sF15 = $sum(sF12,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
tff(f127,plain,
! [X9: $int,X4: $int] :
( $less(X9,sK2)
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,X4) != sK3 )
| $less(sF13,sK3)
| $less(X4,sK2)
| $less(sK1,sK2)
| ( sK3 != 'select:(Array[Int,Int]*Int)>Int'(sK4,X9) )
| $less(sF15,X9)
| $less(sK1,X4) ),
inference(definition_folding,[],[f112,f126,f125,f120,f119,f121,f120,f119]) ).
tff(f128,definition,
sF16 = $sum(sF12,1),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
tff(f129,plain,
! [X7: $int,X4: $int] :
( $less(sK1,X4)
| ~ $less(sF13,sK3)
| $less(X4,sK2)
| ( sK3 != 'select:(Array[Int,Int]*Int)>Int'(sK4,X7) )
| ( 'select:(Array[Int,Int]*Int)>Int'(sK4,X4) != sK3 )
| $less(sK1,sK2)
| $less(sK1,X7)
| $less(X7,sF16) ),
inference(definition_folding,[],[f114,f121,f120,f119,f128,f120,f119]) ).
tff(f131,definition,
sF17 = 'select:(Array[Int,Int]*Int)>Int'(sK4,sK5),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
tff(f132,plain,
'select:(Array[Int,Int]*Int)>Int'(sK4,sK5) = sF17,
inference(reorient_equations,[],[f131]) ).
tff(f133,definition,
sF18 = 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
tff(f134,plain,
'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sF18,
inference(reorient_equations,[],[f133]) ).
tff(f135,plain,
( ( sK3 = sF18 )
| ~ $less(sK8,sK7)
| ( sK3 = sF17 )
| $less(sK1,sK2)
| ~ $less(sF18,sK3) ),
inference(definition_folding,[],[f98,f134,f134,f132]) ).
tff(f136,definition,
sF19 = 'select:(Array[Int,Int]*Int)>Int'(sK4,sK8),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
tff(f137,plain,
'select:(Array[Int,Int]*Int)>Int'(sK4,sK8) = sF19,
inference(reorient_equations,[],[f136]) ).
tff(f138,plain,
( ~ $less(sF18,sK3)
| ( sK3 = sF17 )
| ( sK3 = sF18 )
| $less(sK1,sK2)
| ( sK3 = sF19 ) ),
inference(definition_folding,[],[f97,f137,f134,f134,f132]) ).
tff(f139,plain,
( ( sK3 = sF17 )
| $less(sK1,sK2)
| ~ $less(sF18,sK3)
| ( sK3 = sF18 )
| ~ $less(sK1,sK8) ),
inference(definition_folding,[],[f96,f134,f134,f132]) ).
tff(f140,definition,
sF20 = $sum(sK6,1),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f141,plain,
( ( sK7 = sF20 )
| ~ $less(sF18,sK3)
| $less(sK1,sK2)
| ( sK3 = sF17 )
| ( sK3 = sF18 ) ),
inference(definition_folding,[],[f95,f140,f134,f134,f132]) ).
tff(f142,plain,
( $less(sF18,sK3)
| ~ $less(sK9,sK10)
| ( sK3 = sF18 )
| ( sK3 = sF17 )
| $less(sK1,sK2) ),
inference(definition_folding,[],[f94,f134,f134,f132]) ).
tff(f143,definition,
sF21 = 'select:(Array[Int,Int]*Int)>Int'(sK4,sK10),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f144,plain,
'select:(Array[Int,Int]*Int)>Int'(sK4,sK10) = sF21,
inference(reorient_equations,[],[f143]) ).
tff(f145,plain,
( $less(sF18,sK3)
| ( sK3 = sF18 )
| ( sF21 = sK3 )
| ( sK3 = sF17 )
| $less(sK1,sK2) ),
inference(definition_folding,[],[f93,f144,f134,f134,f132]) ).
tff(f146,plain,
( ( sK3 = sF18 )
| ~ $less(sK10,sK2)
| $less(sK1,sK2)
| $less(sF18,sK3)
| ( sK3 = sF17 ) ),
inference(definition_folding,[],[f92,f134,f134,f132]) ).
tff(f147,definition,
sF22 = $sum(sK6,sF14),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f148,plain,
$sum(sK6,sF14) = sF22,
inference(reorient_equations,[],[f147]) ).
tff(f149,plain,
( ( sF22 = sK9 )
| ( sK3 = sF17 )
| ( sK3 = sF18 )
| $less(sF18,sK3)
| $less(sK1,sK2) ),
inference(definition_folding,[],[f91,f148,f125,f134,f134,f132]) ).
tff(f150,plain,
( ( sK6 = sF12 )
| $less(sK1,sK2)
| ( sK3 = sF17 ) ),
inference(definition_folding,[],[f90,f120,f119,f132]) ).
tff(f152,plain,
( ~ $less(sK5,sK2)
| $less(sK1,sK2)
| ~ $less(sF18,sK3)
| ( sK3 = sF18 )
| ~ $less(sK8,sK7) ),
inference(definition_folding,[],[f88,f134,f134]) ).
tff(f153,plain,
( ~ $less(sF18,sK3)
| $less(sK1,sK2)
| ( sK3 = sF19 )
| ( sK3 = sF18 )
| ~ $less(sK5,sK2) ),
inference(definition_folding,[],[f87,f137,f134,f134]) ).
tff(f154,plain,
( ~ $less(sK1,sK8)
| ~ $less(sF18,sK3)
| ( sK3 = sF18 )
| ~ $less(sK5,sK2)
| $less(sK1,sK2) ),
inference(definition_folding,[],[f86,f134,f134]) ).
tff(f155,plain,
( ~ $less(sF18,sK3)
| ~ $less(sK5,sK2)
| ( sK7 = sF20 )
| ( sK3 = sF18 )
| $less(sK1,sK2) ),
inference(definition_folding,[],[f85,f140,f134,f134]) ).
tff(f156,plain,
( $less(sF18,sK3)
| ~ $less(sK5,sK2)
| ~ $less(sK9,sK10)
| $less(sK1,sK2)
| ( sK3 = sF18 ) ),
inference(definition_folding,[],[f84,f134,f134]) ).
tff(f157,plain,
( $less(sF18,sK3)
| $less(sK1,sK2)
| ~ $less(sK5,sK2)
| ( sK3 = sF18 )
| ( sF21 = sK3 ) ),
inference(definition_folding,[],[f83,f144,f134,f134]) ).
tff(f158,plain,
( ~ $less(sK10,sK2)
| $less(sF18,sK3)
| ( sK3 = sF18 )
| ~ $less(sK5,sK2)
| $less(sK1,sK2) ),
inference(definition_folding,[],[f82,f134,f134]) ).
tff(f159,plain,
( $less(sK1,sK2)
| ( sF22 = sK9 )
| ~ $less(sK5,sK2)
| $less(sF18,sK3)
| ( sK3 = sF18 ) ),
inference(definition_folding,[],[f81,f148,f125,f134,f134]) ).
tff(f160,plain,
( $less(sK1,sK2)
| ( sK6 = sF12 )
| ~ $less(sK5,sK2) ),
inference(definition_folding,[],[f80,f120,f119]) ).
tff(f161,plain,
( ( sK3 = sF18 )
| $less(sK1,sK2)
| ~ $less(sK1,sK5)
| ~ $less(sK8,sK7)
| ~ $less(sF18,sK3) ),
inference(definition_folding,[],[f78,f134,f134]) ).
tff(f162,plain,
( ( sK3 = sF19 )
| ~ $less(sK1,sK5)
| ~ $less(sF18,sK3)
| ( sK3 = sF18 )
| $less(sK1,sK2) ),
inference(definition_folding,[],[f77,f137,f134,f134]) ).
tff(f163,plain,
( ( sK3 = sF18 )
| ~ $less(sK1,sK8)
| ~ $less(sK1,sK5)
| ~ $less(sF18,sK3)
| $less(sK1,sK2) ),
inference(definition_folding,[],[f76,f134,f134]) ).
tff(f164,plain,
( ( sK3 = sF18 )
| ( sK7 = sF20 )
| $less(sK1,sK2)
| ~ $less(sK1,sK5)
| ~ $less(sF18,sK3) ),
inference(definition_folding,[],[f75,f140,f134,f134]) ).
tff(f165,plain,
( ~ $less(sK1,sK5)
| $less(sK1,sK2)
| ( sK3 = sF18 )
| $less(sF18,sK3)
| ~ $less(sK9,sK10) ),
inference(definition_folding,[],[f74,f134,f134]) ).
tff(f166,plain,
( $less(sF18,sK3)
| $less(sK1,sK2)
| ( sF21 = sK3 )
| ~ $less(sK1,sK5)
| ( sK3 = sF18 ) ),
inference(definition_folding,[],[f73,f144,f134,f134]) ).
tff(f167,plain,
( ( sK3 = sF18 )
| $less(sK1,sK2)
| ~ $less(sK10,sK2)
| $less(sF18,sK3)
| ~ $less(sK1,sK5) ),
inference(definition_folding,[],[f72,f134,f134]) ).
tff(f168,plain,
( ( sK3 = sF18 )
| $less(sK1,sK2)
| ( sF22 = sK9 )
| $less(sF18,sK3)
| ~ $less(sK1,sK5) ),
inference(definition_folding,[],[f71,f148,f125,f134,f134]) ).
tff(f169,plain,
( ~ $less(sK1,sK5)
| $less(sK1,sK2)
| ( sK6 = sF12 ) ),
inference(definition_folding,[],[f70,f120,f119]) ).
tff(f170,definition,
sF23 = length(sK4),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f171,plain,
length(sK4) = sF23,
inference(reorient_equations,[],[f170]) ).
tff(f172,plain,
$less(sK1,sF23),
inference(definition_folding,[],[f68,f171]) ).
tff(f173,definition,
sF24 = $sum(sF23,sF14),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f174,plain,
sorted(sK4,0,sF24),
inference(definition_folding,[],[f67,f173,f125,f171]) ).
tff(f175,plain,
sF11 = $sum(sK1,sK2),
inference(evaluation,[],[f119]) ).
tff(f176,plain,
! [X1: $int] : $less(X1,$sum(2,2(div2(X1)))),
inference(evaluation,[],[f106]) ).
tff(f177,plain,
! [X1: $int] : ~ $less(X1,2(div2(X1))),
inference(evaluation,[],[f107]) ).
tff(f179,plain,
sF14 = -1,
inference(evaluation,[],[f125]) ).
tff(f185,definition,
( spl25_2
<=> $less(sK5,sK2) ),
introduced(definition,[new_symbols(definition,[spl25_2])],[avatar_definition]) ).
tff(f187,plain,
( ~ $less(sK5,sK2)
| spl25_2 ),
inference(avatar_component_clause,[],[f185]) ).
tff(f189,definition,
( spl25_3
<=> $less(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl25_3])],[avatar_definition]) ).
tff(f193,definition,
( spl25_4
<=> ( sK6 = sF12 ) ),
introduced(definition,[new_symbols(definition,[spl25_4])],[avatar_definition]) ).
tff(f195,plain,
( ( sK6 = sF12 )
| ~ spl25_4 ),
inference(avatar_component_clause,[],[f193]) ).
tff(f196,plain,
( ~ spl25_2
| spl25_3
| spl25_4 ),
inference(avatar_split_clause,[],[f160,f193,f189,f185]) ).
tff(f198,definition,
( spl25_5
<=> ! [X4: $int,X0: $int,X3: $int,X2: $int,X1: 'Array[Int,Int]'] :
( $less(X3,X0)
| $less(X2,X4)
| ~ sorted(X1,X0,X2)
| ~ $less(X3,X4)
| ~ $less('select:(Array[Int,Int]*Int)>Int'(X1,X4),'select:(Array[Int,Int]*Int)>Int'(X1,X3)) ) ),
introduced(definition,[new_symbols(definition,[spl25_5])],[avatar_definition]) ).
tff(f199,plain,
( ! [X2: $int,X3: $int,X0: $int,X1: 'Array[Int,Int]',X4: $int] :
( ~ $less('select:(Array[Int,Int]*Int)>Int'(X1,X4),'select:(Array[Int,Int]*Int)>Int'(X1,X3))
| $less(X3,X0)
| ~ $less(X3,X4)
| $less(X2,X4)
| ~ sorted(X1,X0,X2) )
| ~ spl25_5 ),
inference(avatar_component_clause,[],[f198]) ).
tff(f200,plain,
spl25_5,
inference(avatar_split_clause,[],[f64,f198]) ).
tff(f202,definition,
( spl25_6
<=> $less(sK1,sK5) ),
introduced(definition,[new_symbols(definition,[spl25_6])],[avatar_definition]) ).
tff(f204,plain,
( ~ $less(sK1,sK5)
| spl25_6 ),
inference(avatar_component_clause,[],[f202]) ).
tff(f206,definition,
( spl25_7
<=> $less(sF18,sK3) ),
introduced(definition,[new_symbols(definition,[spl25_7])],[avatar_definition]) ).
tff(f210,definition,
( spl25_8
<=> ( sK7 = sF20 ) ),
introduced(definition,[new_symbols(definition,[spl25_8])],[avatar_definition]) ).
tff(f214,definition,
( spl25_9
<=> ( sK3 = sF18 ) ),
introduced(definition,[new_symbols(definition,[spl25_9])],[avatar_definition]) ).
tff(f216,plain,
( ( sK3 = sF18 )
| ~ spl25_9 ),
inference(avatar_component_clause,[],[f214]) ).
tff(f217,plain,
( ~ spl25_6
| ~ spl25_7
| spl25_8
| spl25_3
| spl25_9 ),
inference(avatar_split_clause,[],[f164,f214,f189,f210,f206,f202]) ).
tff(f219,definition,
( spl25_10
<=> ! [X4: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,X4) != sK3 )
| $less(sK1,X4)
| $less(X4,sK2) ) ),
introduced(definition,[new_symbols(definition,[spl25_10])],[avatar_definition]) ).
tff(f220,plain,
( ! [X4: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,X4) != sK3 )
| $less(sK1,X4)
| $less(X4,sK2) )
| ~ spl25_10 ),
inference(avatar_component_clause,[],[f219]) ).
tff(f222,definition,
( spl25_11
<=> ! [X9: $int] :
( $less(X9,sK2)
| $less(sF15,X9)
| ( sK3 != 'select:(Array[Int,Int]*Int)>Int'(sK4,X9) ) ) ),
introduced(definition,[new_symbols(definition,[spl25_11])],[avatar_definition]) ).
tff(f223,plain,
( ! [X9: $int] :
( ( sK3 != 'select:(Array[Int,Int]*Int)>Int'(sK4,X9) )
| $less(X9,sK2)
| $less(sF15,X9) )
| ~ spl25_11 ),
inference(avatar_component_clause,[],[f222]) ).
tff(f225,definition,
( spl25_12
<=> $less(sF13,sK3) ),
introduced(definition,[new_symbols(definition,[spl25_12])],[avatar_definition]) ).
tff(f227,plain,
( $less(sF13,sK3)
| ~ spl25_12 ),
inference(avatar_component_clause,[],[f225]) ).
tff(f228,plain,
( spl25_3
| spl25_10
| spl25_11
| spl25_12 ),
inference(avatar_split_clause,[],[f127,f225,f222,f219,f189]) ).
tff(f238,definition,
( spl25_15
<=> ( sF24 = $sum(sF23,sF14) ) ),
introduced(definition,[new_symbols(definition,[spl25_15])],[avatar_definition]) ).
tff(f241,plain,
spl25_15,
inference(avatar_split_clause,[],[f173,f238]) ).
tff(f251,definition,
( spl25_18
<=> ( sF11 = $sum(sK1,sK2) ) ),
introduced(definition,[new_symbols(definition,[spl25_18])],[avatar_definition]) ).
tff(f254,plain,
spl25_18,
inference(avatar_split_clause,[],[f175,f251]) ).
tff(f256,definition,
( spl25_19
<=> $less(sK1,sK8) ),
introduced(definition,[new_symbols(definition,[spl25_19])],[avatar_definition]) ).
tff(f258,plain,
( ~ $less(sK1,sK8)
| spl25_19 ),
inference(avatar_component_clause,[],[f256]) ).
tff(f259,plain,
( ~ spl25_19
| spl25_9
| ~ spl25_6
| ~ spl25_7
| spl25_3 ),
inference(avatar_split_clause,[],[f163,f189,f206,f202,f214,f256]) ).
tff(f264,plain,
( ~ spl25_3
| ~ spl25_2 ),
inference(avatar_split_clause,[],[f79,f185,f189]) ).
tff(f266,definition,
( spl25_21
<=> ( sK3 = sF17 ) ),
introduced(definition,[new_symbols(definition,[spl25_21])],[avatar_definition]) ).
tff(f268,plain,
( ( sK3 = sF17 )
| ~ spl25_21 ),
inference(avatar_component_clause,[],[f266]) ).
tff(f270,definition,
( spl25_22
<=> $less(sK10,sK2) ),
introduced(definition,[new_symbols(definition,[spl25_22])],[avatar_definition]) ).
tff(f272,plain,
( ~ $less(sK10,sK2)
| spl25_22 ),
inference(avatar_component_clause,[],[f270]) ).
tff(f273,plain,
( spl25_7
| spl25_9
| spl25_21
| ~ spl25_22
| spl25_3 ),
inference(avatar_split_clause,[],[f146,f189,f270,f266,f214,f206]) ).
tff(f275,definition,
( spl25_23
<=> ( sF20 = $sum(sK6,1) ) ),
introduced(definition,[new_symbols(definition,[spl25_23])],[avatar_definition]) ).
tff(f278,plain,
spl25_23,
inference(avatar_split_clause,[],[f140,f275]) ).
tff(f280,definition,
( spl25_24
<=> ( sF16 = $sum(sF12,1) ) ),
introduced(definition,[new_symbols(definition,[spl25_24])],[avatar_definition]) ).
tff(f283,plain,
spl25_24,
inference(avatar_split_clause,[],[f128,f280]) ).
tff(f285,definition,
( spl25_25
<=> $less(sK2,0) ),
introduced(definition,[new_symbols(definition,[spl25_25])],[avatar_definition]) ).
tff(f288,plain,
~ spl25_25,
inference(avatar_split_clause,[],[f66,f285]) ).
tff(f290,definition,
( spl25_26
<=> ! [X1: $int] : $less(X1,$sum(2,2(div2(X1)))) ),
introduced(definition,[new_symbols(definition,[spl25_26])],[avatar_definition]) ).
tff(f291,plain,
( ! [X1: $int] : $less(X1,$sum(2,2(div2(X1))))
| ~ spl25_26 ),
inference(avatar_component_clause,[],[f290]) ).
tff(f292,plain,
spl25_26,
inference(avatar_split_clause,[],[f176,f290]) ).
tff(f298,definition,
( spl25_28
<=> ( sF21 = sK3 ) ),
introduced(definition,[new_symbols(definition,[spl25_28])],[avatar_definition]) ).
tff(f300,plain,
( ( sF21 = sK3 )
| ~ spl25_28 ),
inference(avatar_component_clause,[],[f298]) ).
tff(f301,plain,
( spl25_3
| spl25_7
| spl25_28
| ~ spl25_2
| spl25_9 ),
inference(avatar_split_clause,[],[f157,f214,f185,f298,f206,f189]) ).
tff(f302,plain,
( ~ spl25_7
| spl25_8
| ~ spl25_2
| spl25_3
| spl25_9 ),
inference(avatar_split_clause,[],[f155,f214,f189,f185,f210,f206]) ).
tff(f304,definition,
( spl25_29
<=> sorted(sK4,0,sF24) ),
introduced(definition,[new_symbols(definition,[spl25_29])],[avatar_definition]) ).
tff(f306,plain,
( sorted(sK4,0,sF24)
| ~ spl25_29 ),
inference(avatar_component_clause,[],[f304]) ).
tff(f307,plain,
spl25_29,
inference(avatar_split_clause,[],[f174,f304]) ).
tff(f309,definition,
( spl25_30
<=> ! [X7: $int] :
( $less(X7,sF16)
| ( sK3 != 'select:(Array[Int,Int]*Int)>Int'(sK4,X7) )
| $less(sK1,X7) ) ),
introduced(definition,[new_symbols(definition,[spl25_30])],[avatar_definition]) ).
tff(f310,plain,
( ! [X7: $int] :
( ( sK3 != 'select:(Array[Int,Int]*Int)>Int'(sK4,X7) )
| $less(sK1,X7)
| $less(X7,sF16) )
| ~ spl25_30 ),
inference(avatar_component_clause,[],[f309]) ).
tff(f313,definition,
( spl25_31
<=> $less(sK9,sK10) ),
introduced(definition,[new_symbols(definition,[spl25_31])],[avatar_definition]) ).
tff(f316,plain,
( ~ spl25_6
| spl25_7
| ~ spl25_31
| spl25_9
| spl25_3 ),
inference(avatar_split_clause,[],[f165,f189,f214,f313,f206,f202]) ).
tff(f318,definition,
( spl25_32
<=> ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sF18 ) ),
introduced(definition,[new_symbols(definition,[spl25_32])],[avatar_definition]) ).
tff(f320,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK6) = sF18 )
| ~ spl25_32 ),
inference(avatar_component_clause,[],[f318]) ).
tff(f321,plain,
spl25_32,
inference(avatar_split_clause,[],[f134,f318]) ).
tff(f327,definition,
( spl25_34
<=> ( sK3 = sF19 ) ),
introduced(definition,[new_symbols(definition,[spl25_34])],[avatar_definition]) ).
tff(f330,plain,
( spl25_21
| ~ spl25_7
| spl25_3
| spl25_34
| spl25_9 ),
inference(avatar_split_clause,[],[f138,f214,f327,f189,f206,f266]) ).
tff(f331,plain,
( ~ spl25_31
| ~ spl25_2
| spl25_7
| spl25_3
| spl25_9 ),
inference(avatar_split_clause,[],[f156,f214,f189,f206,f185,f313]) ).
tff(f333,definition,
( spl25_35
<=> ! [X1: $int] : ~ $less(X1,2(div2(X1))) ),
introduced(definition,[new_symbols(definition,[spl25_35])],[avatar_definition]) ).
tff(f334,plain,
( ! [X1: $int] : ~ $less(X1,2(div2(X1)))
| ~ spl25_35 ),
inference(avatar_component_clause,[],[f333]) ).
tff(f335,plain,
spl25_35,
inference(avatar_split_clause,[],[f177,f333]) ).
tff(f337,definition,
( spl25_36
<=> $less(sK8,sK7) ),
introduced(definition,[new_symbols(definition,[spl25_36])],[avatar_definition]) ).
tff(f340,plain,
( ~ spl25_6
| ~ spl25_7
| spl25_9
| spl25_3
| ~ spl25_36 ),
inference(avatar_split_clause,[],[f161,f337,f189,f214,f206,f202]) ).
tff(f341,plain,
( spl25_9
| ~ spl25_22
| spl25_3
| spl25_7
| ~ spl25_6 ),
inference(avatar_split_clause,[],[f167,f202,f206,f189,f270,f214]) ).
tff(f342,plain,
( ~ spl25_7
| spl25_21
| spl25_3
| ~ spl25_36
| spl25_9 ),
inference(avatar_split_clause,[],[f135,f214,f337,f189,f266,f206]) ).
tff(f344,definition,
( spl25_37
<=> ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK5) = sF17 ) ),
introduced(definition,[new_symbols(definition,[spl25_37])],[avatar_definition]) ).
tff(f346,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK5) = sF17 )
| ~ spl25_37 ),
inference(avatar_component_clause,[],[f344]) ).
tff(f347,plain,
spl25_37,
inference(avatar_split_clause,[],[f132,f344]) ).
tff(f353,plain,
( spl25_3
| spl25_34
| ~ spl25_7
| ~ spl25_2
| spl25_9 ),
inference(avatar_split_clause,[],[f153,f214,f185,f206,f327,f189]) ).
tff(f354,plain,
( spl25_9
| ~ spl25_2
| spl25_3
| ~ spl25_22
| spl25_7 ),
inference(avatar_split_clause,[],[f158,f206,f270,f189,f185,f214]) ).
tff(f359,plain,
( ~ spl25_6
| ~ spl25_3 ),
inference(avatar_split_clause,[],[f69,f189,f202]) ).
tff(f361,definition,
( spl25_40
<=> ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK8) = sF19 ) ),
introduced(definition,[new_symbols(definition,[spl25_40])],[avatar_definition]) ).
tff(f363,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK8) = sF19 )
| ~ spl25_40 ),
inference(avatar_component_clause,[],[f361]) ).
tff(f364,plain,
spl25_40,
inference(avatar_split_clause,[],[f137,f361]) ).
tff(f374,definition,
( spl25_43
<=> ( sF13 = sK3 ) ),
introduced(definition,[new_symbols(definition,[spl25_43])],[avatar_definition]) ).
tff(f377,plain,
( spl25_10
| ~ spl25_43
| spl25_3 ),
inference(avatar_split_clause,[],[f122,f189,f374,f219]) ).
tff(f379,definition,
( spl25_44
<=> ( sF22 = sK9 ) ),
introduced(definition,[new_symbols(definition,[spl25_44])],[avatar_definition]) ).
tff(f381,plain,
( ( sF22 = sK9 )
| ~ spl25_44 ),
inference(avatar_component_clause,[],[f379]) ).
tff(f382,plain,
( spl25_21
| spl25_9
| spl25_7
| spl25_3
| spl25_44 ),
inference(avatar_split_clause,[],[f149,f379,f189,f206,f214,f266]) ).
tff(f387,plain,
( spl25_9
| ~ spl25_19
| spl25_3
| spl25_21
| ~ spl25_7 ),
inference(avatar_split_clause,[],[f139,f206,f266,f189,f256,f214]) ).
tff(f388,plain,
( spl25_4
| spl25_3
| spl25_21 ),
inference(avatar_split_clause,[],[f150,f266,f189,f193]) ).
tff(f389,plain,
( spl25_10
| spl25_30
| ~ spl25_12
| spl25_3 ),
inference(avatar_split_clause,[],[f129,f189,f225,f309,f219]) ).
tff(f398,plain,
( spl25_21
| spl25_8
| spl25_9
| ~ spl25_7
| spl25_3 ),
inference(avatar_split_clause,[],[f141,f189,f206,f214,f210,f266]) ).
tff(f400,definition,
( spl25_48
<=> ( sF15 = $sum(sF12,sF14) ) ),
introduced(definition,[new_symbols(definition,[spl25_48])],[avatar_definition]) ).
tff(f403,plain,
spl25_48,
inference(avatar_split_clause,[],[f126,f400]) ).
tff(f413,definition,
( spl25_51
<=> ( $sum(sK6,sF14) = sF22 ) ),
introduced(definition,[new_symbols(definition,[spl25_51])],[avatar_definition]) ).
tff(f415,plain,
( ( $sum(sK6,sF14) = sF22 )
| ~ spl25_51 ),
inference(avatar_component_clause,[],[f413]) ).
tff(f416,plain,
spl25_51,
inference(avatar_split_clause,[],[f148,f413]) ).
tff(f418,definition,
( spl25_52
<=> ( sF12 = div2(sF11) ) ),
introduced(definition,[new_symbols(definition,[spl25_52])],[avatar_definition]) ).
tff(f420,plain,
( ( sF12 = div2(sF11) )
| ~ spl25_52 ),
inference(avatar_component_clause,[],[f418]) ).
tff(f421,plain,
spl25_52,
inference(avatar_split_clause,[],[f120,f418]) ).
tff(f422,plain,
( spl25_44
| spl25_3
| spl25_9
| spl25_7
| ~ spl25_2 ),
inference(avatar_split_clause,[],[f159,f185,f206,f214,f189,f379]) ).
tff(f427,plain,
( spl25_9
| spl25_44
| spl25_7
| spl25_3
| ~ spl25_6 ),
inference(avatar_split_clause,[],[f168,f202,f189,f206,f379,f214]) ).
tff(f429,definition,
( spl25_54
<=> ( sF13 = 'select:(Array[Int,Int]*Int)>Int'(sK4,sF12) ) ),
introduced(definition,[new_symbols(definition,[spl25_54])],[avatar_definition]) ).
tff(f431,plain,
( ( sF13 = 'select:(Array[Int,Int]*Int)>Int'(sK4,sF12) )
| ~ spl25_54 ),
inference(avatar_component_clause,[],[f429]) ).
tff(f432,plain,
spl25_54,
inference(avatar_split_clause,[],[f121,f429]) ).
tff(f438,definition,
( spl25_56
<=> ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK10) = sF21 ) ),
introduced(definition,[new_symbols(definition,[spl25_56])],[avatar_definition]) ).
tff(f440,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK10) = sF21 )
| ~ spl25_56 ),
inference(avatar_component_clause,[],[f438]) ).
tff(f441,plain,
spl25_56,
inference(avatar_split_clause,[],[f144,f438]) ).
tff(f442,plain,
( spl25_28
| spl25_7
| spl25_21
| spl25_9
| spl25_3 ),
inference(avatar_split_clause,[],[f145,f189,f214,f266,f206,f298]) ).
tff(f443,plain,
( spl25_3
| spl25_9
| ~ spl25_19
| ~ spl25_7
| ~ spl25_2 ),
inference(avatar_split_clause,[],[f154,f185,f206,f256,f214,f189]) ).
tff(f448,plain,
( ~ spl25_6
| spl25_28
| spl25_7
| spl25_9
| spl25_3 ),
inference(avatar_split_clause,[],[f166,f189,f214,f206,f298,f202]) ).
tff(f453,plain,
( spl25_9
| ~ spl25_7
| ~ spl25_2
| spl25_3
| ~ spl25_36 ),
inference(avatar_split_clause,[],[f152,f337,f189,f185,f206,f214]) ).
tff(f454,plain,
( spl25_3
| spl25_21
| spl25_7
| ~ spl25_31
| spl25_9 ),
inference(avatar_split_clause,[],[f142,f214,f313,f206,f266,f189]) ).
tff(f459,plain,
( ~ spl25_7
| ~ spl25_6
| spl25_3
| spl25_9
| spl25_34 ),
inference(avatar_split_clause,[],[f162,f327,f214,f189,f202,f206]) ).
tff(f460,plain,
( spl25_4
| ~ spl25_6
| spl25_3 ),
inference(avatar_split_clause,[],[f169,f189,f202,f193]) ).
tff(f462,definition,
( spl25_60
<=> $less(sK1,sF23) ),
introduced(definition,[new_symbols(definition,[spl25_60])],[avatar_definition]) ).
tff(f465,plain,
spl25_60,
inference(avatar_split_clause,[],[f172,f462]) ).
tff(f476,definition,
( spl25_63
<=> ( sF14 = -1 ) ),
introduced(definition,[new_symbols(definition,[spl25_63])],[avatar_definition]) ).
tff(f478,plain,
( ( sF14 = -1 )
| ~ spl25_63 ),
inference(avatar_component_clause,[],[f476]) ).
tff(f479,plain,
spl25_63,
inference(avatar_split_clause,[],[f179,f476]) ).
tff(f485,plain,
( ( $sum(sK6,-1) = sF22 )
| ~ spl25_51
| ~ spl25_63 ),
inference(forward_demodulation,[],[f415,f478]) ).
tff(f487,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK5) = sK3 )
| ~ spl25_21
| ~ spl25_37 ),
inference(forward_demodulation,[],[f346,f268]) ).
tff(f494,definition,
( spl25_66
<=> ( $sum(sK6,-1) = sF22 ) ),
introduced(definition,[new_symbols(definition,[spl25_66])],[avatar_definition]) ).
tff(f496,plain,
( ( $sum(sK6,-1) = sF22 )
| ~ spl25_66 ),
inference(avatar_component_clause,[],[f494]) ).
tff(f497,plain,
( spl25_66
| ~ spl25_51
| ~ spl25_63 ),
inference(avatar_split_clause,[],[f485,f476,f413,f494]) ).
tff(f504,definition,
( spl25_68
<=> ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK5) = sK3 ) ),
introduced(definition,[new_symbols(definition,[spl25_68])],[avatar_definition]) ).
tff(f506,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sK5) = sK3 )
| ~ spl25_68 ),
inference(avatar_component_clause,[],[f504]) ).
tff(f507,plain,
( spl25_68
| ~ spl25_21
| ~ spl25_37 ),
inference(avatar_split_clause,[],[f487,f344,f266,f504]) ).
tff(f508,plain,
( $less(sK5,sK2)
| ( sK3 != sK3 )
| $less(sK1,sK5)
| ~ spl25_10
| ~ spl25_68 ),
inference(superposition,[],[f220,f506]) ).
tff(f509,plain,
( $less(sK5,sK2)
| $less(sK1,sK5)
| ~ spl25_10
| ~ spl25_68 ),
inference(trivial_inequality_removal,[],[f508]) ).
tff(f510,plain,
( $less(sK1,sK5)
| spl25_2
| ~ spl25_10
| ~ spl25_68 ),
inference(forward_subsumption_resolution,[],[f509,f187]) ).
tff(f511,plain,
( $false
| spl25_2
| spl25_6
| ~ spl25_10
| ~ spl25_68 ),
inference(forward_subsumption_resolution,[],[f510,f204]) ).
tff(f512,plain,
( spl25_2
| spl25_6
| ~ spl25_10
| ~ spl25_68 ),
inference(avatar_contradiction_clause,[],[f511]) ).
tff(f513,plain,
( $less(sK5,sK2)
| $less(sF15,sK5)
| ( sK3 != sK3 )
| ~ spl25_11
| ~ spl25_68 ),
inference(superposition,[],[f223,f506]) ).
tff(f517,definition,
( spl25_69
<=> $less(sF15,sK5) ),
introduced(definition,[new_symbols(definition,[spl25_69])],[avatar_definition]) ).
tff(f537,plain,
( ~ $less(sF11,2(sF12))
| ~ spl25_35
| ~ spl25_52 ),
inference(superposition,[],[f334,f420]) ).
tff(f539,definition,
( spl25_73
<=> $less(sF11,2(sF12)) ),
introduced(definition,[new_symbols(definition,[spl25_73])],[avatar_definition]) ).
tff(f542,plain,
( ~ spl25_73
| ~ spl25_35
| ~ spl25_52 ),
inference(avatar_split_clause,[],[f537,f418,f333,f539]) ).
tff(f545,definition,
( spl25_74
<=> $less(sK8,sK2) ),
introduced(definition,[new_symbols(definition,[spl25_74])],[avatar_definition]) ).
tff(f554,plain,
( $less(sF15,sK10)
| $less(sK10,sK2)
| ( sF21 != sK3 )
| ~ spl25_11
| ~ spl25_56 ),
inference(superposition,[],[f223,f440]) ).
tff(f556,definition,
( spl25_76
<=> $less(sF15,sK10) ),
introduced(definition,[new_symbols(definition,[spl25_76])],[avatar_definition]) ).
tff(f559,plain,
( spl25_22
| spl25_76
| ~ spl25_28
| ~ spl25_11
| ~ spl25_56 ),
inference(avatar_split_clause,[],[f554,f438,f222,f298,f556,f270]) ).
tff(f560,plain,
( $less(sF11,$sum(2,2(sF12)))
| ~ spl25_26
| ~ spl25_52 ),
inference(superposition,[],[f291,f420]) ).
tff(f561,plain,
( $less(sF11,$sum(2(sF12),2))
| ~ spl25_26
| ~ spl25_52 ),
inference(evaluation,[],[f560]) ).
tff(f563,definition,
( spl25_77
<=> $less(sF11,$sum(2(sF12),2)) ),
introduced(definition,[new_symbols(definition,[spl25_77])],[avatar_definition]) ).
tff(f566,plain,
( spl25_77
| ~ spl25_26
| ~ spl25_52 ),
inference(avatar_split_clause,[],[f561,f418,f290,f563]) ).
tff(f608,plain,
( ! [X2: $int,X0: $int,X1: $int] :
( ~ $less(sK3,'select:(Array[Int,Int]*Int)>Int'(sK4,X0))
| ~ sorted(sK4,X1,X2)
| ~ $less(X0,sK5)
| $less(X0,X1)
| $less(X2,sK5) )
| ~ spl25_5
| ~ spl25_68 ),
inference(superposition,[],[f199,f506]) ).
tff(f616,plain,
( ! [X2: $int,X0: $int,X1: $int] :
( ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,X0),sK3)
| ~ $less(sK5,X0)
| ~ sorted(sK4,X1,X2)
| $less(X2,X0)
| $less(sK5,X1) )
| ~ spl25_5
| ~ spl25_68 ),
inference(superposition,[],[f199,f506]) ).
tff(f629,definition,
( spl25_86
<=> ! [X2: $int,X0: $int,X1: $int] :
( ~ $less(sK3,'select:(Array[Int,Int]*Int)>Int'(sK4,X0))
| ~ sorted(sK4,X1,X2)
| ~ $less(X0,sK5)
| $less(X0,X1)
| $less(X2,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl25_86])],[avatar_definition]) ).
tff(f630,plain,
( ! [X2: $int,X0: $int,X1: $int] :
( ~ $less(sK3,'select:(Array[Int,Int]*Int)>Int'(sK4,X0))
| $less(X0,X1)
| ~ $less(X0,sK5)
| $less(X2,sK5)
| ~ sorted(sK4,X1,X2) )
| ~ spl25_86 ),
inference(avatar_component_clause,[],[f629]) ).
tff(f631,plain,
( spl25_86
| ~ spl25_5
| ~ spl25_68 ),
inference(avatar_split_clause,[],[f608,f504,f198,f629]) ).
tff(f641,definition,
( spl25_89
<=> ! [X2: $int,X0: $int,X1: $int] :
( ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,X0),sK3)
| ~ $less(sK5,X0)
| ~ sorted(sK4,X1,X2)
| $less(X2,X0)
| $less(sK5,X1) ) ),
introduced(definition,[new_symbols(definition,[spl25_89])],[avatar_definition]) ).
tff(f642,plain,
( ! [X2: $int,X0: $int,X1: $int] :
( ~ $less('select:(Array[Int,Int]*Int)>Int'(sK4,X0),sK3)
| $less(X2,X0)
| ~ sorted(sK4,X1,X2)
| ~ $less(sK5,X0)
| $less(sK5,X1) )
| ~ spl25_89 ),
inference(avatar_component_clause,[],[f641]) ).
tff(f643,plain,
( spl25_89
| ~ spl25_5
| ~ spl25_68 ),
inference(avatar_split_clause,[],[f616,f504,f198,f641]) ).
tff(f692,plain,
( ! [X0: $int,X1: $int] :
( $less(sF12,X0)
| $less(X1,sK5)
| ~ $less(sK3,sF13)
| ~ $less(sF12,sK5)
| ~ sorted(sK4,X0,X1) )
| ~ spl25_54
| ~ spl25_86 ),
inference(superposition,[],[f630,f431]) ).
tff(f730,definition,
( spl25_109
<=> $less(sF12,sK5) ),
introduced(definition,[new_symbols(definition,[spl25_109])],[avatar_definition]) ).
tff(f734,definition,
( spl25_110
<=> $less(sK3,sF13) ),
introduced(definition,[new_symbols(definition,[spl25_110])],[avatar_definition]) ).
tff(f738,definition,
( spl25_111
<=> ! [X0: $int,X1: $int] :
( $less(sF12,X0)
| ~ sorted(sK4,X0,X1)
| $less(X1,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl25_111])],[avatar_definition]) ).
tff(f739,plain,
( ! [X0: $int,X1: $int] :
( ~ sorted(sK4,X0,X1)
| $less(X1,sK5)
| $less(sF12,X0) )
| ~ spl25_111 ),
inference(avatar_component_clause,[],[f738]) ).
tff(f740,plain,
( ~ spl25_109
| ~ spl25_110
| spl25_111
| ~ spl25_54
| ~ spl25_86 ),
inference(avatar_split_clause,[],[f692,f629,f429,f738,f734,f730]) ).
tff(f755,definition,
( spl25_115
<=> $less(sF24,sK5) ),
introduced(definition,[new_symbols(definition,[spl25_115])],[avatar_definition]) ).
tff(f763,plain,
( $less(sK5,sF16)
| ( sK3 != sK3 )
| $less(sK1,sK5)
| ~ spl25_30
| ~ spl25_68 ),
inference(superposition,[],[f310,f506]) ).
tff(f765,plain,
( $less(sK8,sF16)
| $less(sK1,sK8)
| ( sK3 != sF19 )
| ~ spl25_30
| ~ spl25_40 ),
inference(superposition,[],[f310,f363]) ).
tff(f768,plain,
( $less(sK5,sF16)
| $less(sK1,sK5)
| ~ spl25_30
| ~ spl25_68 ),
inference(trivial_inequality_removal,[],[f763]) ).
tff(f769,plain,
( $less(sK5,sF16)
| spl25_6
| ~ spl25_30
| ~ spl25_68 ),
inference(forward_subsumption_resolution,[],[f768,f204]) ).
tff(f771,definition,
( spl25_117
<=> $less(sK5,sF16) ),
introduced(definition,[new_symbols(definition,[spl25_117])],[avatar_definition]) ).
tff(f774,plain,
( spl25_117
| spl25_6
| ~ spl25_30
| ~ spl25_68 ),
inference(avatar_split_clause,[],[f769,f504,f309,f202,f771]) ).
tff(f781,plain,
( ! [X0: $int,X1: $int] :
( ~ sorted(sK4,X1,X0)
| $less(X0,sF12)
| $less(sK5,X1)
| ~ $less(sF13,sK3)
| ~ $less(sK5,sF12) )
| ~ spl25_54
| ~ spl25_89 ),
inference(superposition,[],[f642,f431]) ).
tff(f806,plain,
( ! [X0: $int,X1: $int] :
( $less(sK5,X1)
| $less(X0,sF12)
| ~ $less(sK5,sF12)
| ~ sorted(sK4,X1,X0) )
| ~ spl25_12
| ~ spl25_54
| ~ spl25_89 ),
inference(forward_subsumption_resolution,[],[f781,f227]) ).
tff(f811,definition,
( spl25_125
<=> $less(sK5,0) ),
introduced(definition,[new_symbols(definition,[spl25_125])],[avatar_definition]) ).
tff(f820,definition,
( spl25_127
<=> $less(sK5,sF12) ),
introduced(definition,[new_symbols(definition,[spl25_127])],[avatar_definition]) ).
tff(f824,definition,
( spl25_128
<=> ! [X0: $int,X1: $int] :
( $less(sK5,X1)
| ~ sorted(sK4,X1,X0)
| $less(X0,sF12) ) ),
introduced(definition,[new_symbols(definition,[spl25_128])],[avatar_definition]) ).
tff(f825,plain,
( ! [X0: $int,X1: $int] :
( ~ sorted(sK4,X1,X0)
| $less(X0,sF12)
| $less(sK5,X1) )
| ~ spl25_128 ),
inference(avatar_component_clause,[],[f824]) ).
tff(f826,plain,
( ~ spl25_127
| spl25_128
| ~ spl25_12
| ~ spl25_54
| ~ spl25_89 ),
inference(avatar_split_clause,[],[f806,f641,f429,f225,f824,f820]) ).
tff(f828,definition,
( spl25_129
<=> $less(sK1,sK10) ),
introduced(definition,[new_symbols(definition,[spl25_129])],[avatar_definition]) ).
tff(f842,plain,
( $less(sF24,sF12)
| $less(sK5,0)
| ~ spl25_29
| ~ spl25_128 ),
inference(resolution,[],[f825,f306]) ).
tff(f844,definition,
( spl25_132
<=> $less(sF24,sF12) ),
introduced(definition,[new_symbols(definition,[spl25_132])],[avatar_definition]) ).
tff(f847,plain,
( spl25_132
| spl25_125
| ~ spl25_29
| ~ spl25_128 ),
inference(avatar_split_clause,[],[f842,f824,f304,f811,f844]) ).
tff(f849,definition,
( spl25_133
<=> $less(sK8,sF16) ),
introduced(definition,[new_symbols(definition,[spl25_133])],[avatar_definition]) ).
tff(f852,plain,
( spl25_133
| ~ spl25_34
| spl25_19
| ~ spl25_30
| ~ spl25_40 ),
inference(avatar_split_clause,[],[f765,f361,f309,f256,f327,f849]) ).
tff(f859,plain,
( ( $sum(sF12,-1) = sF22 )
| ~ spl25_4
| ~ spl25_66 ),
inference(superposition,[],[f496,f195]) ).
tff(f860,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sF12) = sF18 )
| ~ spl25_4
| ~ spl25_32 ),
inference(superposition,[],[f320,f195]) ).
tff(f862,plain,
( ( $sum(sF12,-1) = sK9 )
| ~ spl25_4
| ~ spl25_44
| ~ spl25_66 ),
inference(forward_demodulation,[],[f859,f381]) ).
tff(f864,definition,
( spl25_134
<=> ( 'select:(Array[Int,Int]*Int)>Int'(sK4,sF12) = sF18 ) ),
introduced(definition,[new_symbols(definition,[spl25_134])],[avatar_definition]) ).
tff(f867,plain,
( spl25_134
| ~ spl25_4
| ~ spl25_32 ),
inference(avatar_split_clause,[],[f860,f318,f193,f864]) ).
tff(f874,definition,
( spl25_136
<=> ( $sum(sF12,-1) = sK9 ) ),
introduced(definition,[new_symbols(definition,[spl25_136])],[avatar_definition]) ).
tff(f877,plain,
( spl25_136
| ~ spl25_4
| ~ spl25_44
| ~ spl25_66 ),
inference(avatar_split_clause,[],[f862,f494,f379,f193,f874]) ).
tff(f882,plain,
( $less(sK1,sK6)
| ( sK3 != sF18 )
| $less(sK6,sK2)
| ~ spl25_10
| ~ spl25_32 ),
inference(superposition,[],[f220,f320]) ).
tff(f883,plain,
( $less(sK8,sK2)
| ( sK3 != sF19 )
| $less(sK1,sK8)
| ~ spl25_10
| ~ spl25_40 ),
inference(superposition,[],[f220,f363]) ).
tff(f884,plain,
( $less(sK10,sK2)
| ( sF21 != sK3 )
| $less(sK1,sK10)
| ~ spl25_10
| ~ spl25_56 ),
inference(superposition,[],[f220,f440]) ).
tff(f887,plain,
( ( sK3 != sF19 )
| $less(sK8,sK2)
| ~ spl25_10
| spl25_19
| ~ spl25_40 ),
inference(forward_subsumption_resolution,[],[f883,f258]) ).
tff(f888,plain,
( $less(sK10,sK2)
| $less(sK1,sK10)
| ~ spl25_10
| ~ spl25_28
| ~ spl25_56 ),
inference(forward_subsumption_resolution,[],[f884,f300]) ).
tff(f889,plain,
( ~ spl25_34
| spl25_74
| ~ spl25_10
| spl25_19
| ~ spl25_40 ),
inference(avatar_split_clause,[],[f887,f361,f256,f219,f545,f327]) ).
tff(f890,plain,
( $less(sK1,sK10)
| ~ spl25_10
| spl25_22
| ~ spl25_28
| ~ spl25_56 ),
inference(forward_subsumption_resolution,[],[f888,f272]) ).
tff(f891,plain,
( spl25_129
| ~ spl25_10
| spl25_22
| ~ spl25_28
| ~ spl25_56 ),
inference(avatar_split_clause,[],[f890,f438,f298,f270,f219,f828]) ).
tff(f893,definition,
( spl25_137
<=> $less(sF12,sK2) ),
introduced(definition,[new_symbols(definition,[spl25_137])],[avatar_definition]) ).
tff(f897,definition,
( spl25_138
<=> $less(sK1,sF12) ),
introduced(definition,[new_symbols(definition,[spl25_138])],[avatar_definition]) ).
tff(f901,plain,
( ( sK3 != sF18 )
| $less(sK1,sF12)
| $less(sK6,sK2)
| ~ spl25_4
| ~ spl25_10
| ~ spl25_32 ),
inference(forward_demodulation,[],[f882,f195]) ).
tff(f907,plain,
( $less(sK1,sF12)
| $less(sK6,sK2)
| ~ spl25_4
| ~ spl25_9
| ~ spl25_10
| ~ spl25_32 ),
inference(forward_subsumption_resolution,[],[f901,f216]) ).
tff(f908,plain,
( $less(sK1,sF12)
| $less(sF12,sK2)
| ~ spl25_4
| ~ spl25_9
| ~ spl25_10
| ~ spl25_32 ),
inference(forward_demodulation,[],[f907,f195]) ).
tff(f909,plain,
( spl25_138
| spl25_137
| ~ spl25_4
| ~ spl25_9
| ~ spl25_10
| ~ spl25_32 ),
inference(avatar_split_clause,[],[f908,f318,f219,f214,f193,f893,f897]) ).
tff(f910,plain,
( $less(sK5,sK2)
| $less(sF15,sK5)
| ~ spl25_11
| ~ spl25_68 ),
inference(trivial_inequality_removal,[],[f513]) ).
tff(f911,plain,
( spl25_69
| spl25_2
| ~ spl25_11
| ~ spl25_68 ),
inference(avatar_split_clause,[],[f910,f504,f222,f185,f517]) ).
tff(f917,plain,
( $less(sF12,0)
| $less(sF24,sK5)
| ~ spl25_29
| ~ spl25_111 ),
inference(resolution,[],[f739,f306]) ).
tff(f919,definition,
( spl25_140
<=> $less(sF12,0) ),
introduced(definition,[new_symbols(definition,[spl25_140])],[avatar_definition]) ).
tff(f922,plain,
( spl25_140
| spl25_115
| ~ spl25_29
| ~ spl25_111 ),
inference(avatar_split_clause,[],[f917,f738,f304,f755,f919]) ).
tff(f923,plain,
$false,
inference(avatar_smt_refutation,[],[f922,f911,f909,f891,f889,f877,f867,f852,f847,f826,f774,f740,f643,f631,f566,f559,f542,f512,f507,f497,f479,f465,f460,f459,f454,f453,f448,f443,f442,f441,f432,f427,f422,f421,f416,f403,f398,f389,f388,f387,f382,f377,f364,f359,f354,f353,f347,f342,f341,f340,f335,f331,f330,f321,f316,f307,f302,f301,f292,f288,f283,f278,f273,f264,f259,f254,f241,f228,f217,f200,f196]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW676_1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n018.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 14:26:24 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.28/1.22 % (3424219)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.28/1.22 % (3424290)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3434905786:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.28/1.22 % (3424290)Instruction limit reached!
% 3.28/1.22 % (3424290)------------------------------
% 3.28/1.22 % (3424290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.28/1.22 % (3424290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.28/1.22 % (3424290)CaDiCaL version: 2.1.3
% 3.28/1.22 % (3424290)Termination reason: Instruction limit
% 3.28/1.22 % (3424290)Termination phase: Saturation
% 3.28/1.22 % (3424290)Time elapsed: 0.018 s
% 3.28/1.22 % (3424290)Peak memory usage: 116 MB
% 3.28/1.22 % (3424290)Instructions burned: 12 (million)
% 3.28/1.22 % (3424295)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1896191736:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.28/1.22 % (3424293)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1907089095:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.28/1.22 % (3424292)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3596224832:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.28/1.22 % (3424298)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2758529842:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.28/1.22 % (3424291)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3794255959:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.28/1.22 % (3424295)Instruction limit reached!
% 3.28/1.22 % (3424295)------------------------------
% 3.28/1.22 % (3424295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.28/1.22 % (3424295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.28/1.22 % (3424295)CaDiCaL version: 2.1.3
% 3.28/1.22 % (3424295)Termination reason: Instruction limit
% 3.28/1.22 % (3424295)Termination phase: Saturation
% 3.28/1.22 % (3424295)Time elapsed: 0.004 s
% 3.28/1.22 % (3424295)Peak memory usage: 89 MB
% 3.28/1.22 % (3424295)Instructions burned: 5 (million)
% 3.28/1.22 % (3424293)Instruction limit reached!
% 3.28/1.22 % (3424293)------------------------------
% 3.28/1.22 % (3424293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.28/1.22 % (3424293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.28/1.22 % (3424293)CaDiCaL version: 2.1.3
% 3.28/1.22 % (3424293)Termination reason: Instruction limit
% 3.28/1.22 % (3424293)Termination phase: Saturation
% 3.28/1.22 % (3424293)Time elapsed: 0.005 s
% 3.28/1.22 % (3424293)Peak memory usage: 89 MB
% 3.28/1.22 % (3424293)Instructions burned: 7 (million)
% 3.28/1.22 % (3424296)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1126426744:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.28/1.22 % (3424298)Instruction limit reached!
% 3.28/1.22 % (3424298)------------------------------
% 3.28/1.22 % (3424298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.28/1.22 % (3424298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.28/1.22 % (3424298)CaDiCaL version: 2.1.3
% 3.28/1.22 % (3424298)Termination reason: Instruction limit
% 3.28/1.22 % (3424298)Termination phase: Saturation
% 3.28/1.22 % (3424298)Time elapsed: 0.047 s
% 3.28/1.22 % (3424298)Peak memory usage: 116 MB
% 3.28/1.22 % (3424298)Instructions burned: 33 (million)
% 3.28/1.22 % (3424296)Instruction limit reached!
% 3.28/1.22 % (3424296)------------------------------
% 3.28/1.22 % (3424296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.28/1.22 % (3424296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.28/1.22 % (3424296)CaDiCaL version: 2.1.3
% 3.28/1.22 % (3424296)Termination reason: Instruction limit
% 3.28/1.22 % (3424296)Termination phase: Saturation
% 3.28/1.22 % (3424296)Time elapsed: 0.057 s
% 3.28/1.22 % (3424296)Peak memory usage: 116 MB
% 3.28/1.22 % (3424296)Instructions burned: 46 (million)
% 3.28/1.22 % (3424326)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2868749234:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.28/1.22 % (3424326)Instruction limit reached!
% 3.28/1.22 % (3424326)------------------------------
% 4.19/1.37 % (3424326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.19/1.37 % (3424326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/1.37 % (3424326)CaDiCaL version: 2.1.3
% 4.19/1.37 % (3424326)Termination reason: Instruction limit
% 4.19/1.37 % (3424326)Termination phase: Saturation
% 4.19/1.37 % (3424326)Time elapsed: 0.007 s
% 4.19/1.37 % (3424326)Peak memory usage: 89 MB
% 4.19/1.37 % (3424326)Instructions burned: 16 (million)
% 4.19/1.37 % (3424337)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=2427356577:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.19/1.37 % (3424338)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2191100984:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.19/1.37 % (3424292)Instruction limit reached!
% 4.19/1.37 % (3424292)------------------------------
% 4.19/1.37 % (3424292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.19/1.37 % (3424292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/1.37 % (3424292)CaDiCaL version: 2.1.3
% 4.19/1.37 % (3424292)Termination reason: Instruction limit
% 4.19/1.37 % (3424292)Termination phase: Saturation
% 4.19/1.37 % (3424292)Time elapsed: 0.159 s
% 4.19/1.37 % (3424292)Peak memory usage: 118 MB
% 4.19/1.37 % (3424292)Instructions burned: 201 (million)
% 4.19/1.37 % (3424338)Instruction limit reached!
% 4.19/1.37 % (3424338)------------------------------
% 4.19/1.37 % (3424338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.19/1.37 % (3424338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/1.37 % (3424338)CaDiCaL version: 2.1.3
% 4.19/1.37 % (3424338)Termination reason: Instruction limit
% 4.19/1.37 % (3424338)Termination phase: Saturation
% 4.19/1.37 % (3424338)Time elapsed: 0.010 s
% 4.19/1.37 % (3424338)Peak memory usage: 90 MB
% 4.19/1.37 % (3424338)Instructions burned: 16 (million)
% 4.19/1.37 % (3424337)Instruction limit reached!
% 4.19/1.37 % (3424337)------------------------------
% 4.19/1.37 % (3424337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.19/1.37 % (3424337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/1.37 % (3424337)CaDiCaL version: 2.1.3
% 4.19/1.37 % (3424337)Termination reason: Instruction limit
% 4.19/1.37 % (3424337)Termination phase: Saturation
% 4.19/1.37 % (3424337)Time elapsed: 0.023 s
% 4.19/1.37 % (3424337)Peak memory usage: 89 MB
% 4.19/1.37 % (3424337)Instructions burned: 30 (million)
% 4.19/1.37 % (3424348)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=742720987:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.19/1.37 % (3424348)Instruction limit reached!
% 4.19/1.37 % (3424348)------------------------------
% 4.19/1.37 % (3424348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.19/1.37 % (3424348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/1.37 % (3424348)CaDiCaL version: 2.1.3
% 4.19/1.37 % (3424348)Termination reason: Instruction limit
% 4.19/1.37 % (3424348)Termination phase: Saturation
% 4.19/1.37 % (3424348)Time elapsed: 0.021 s
% 4.19/1.37 % (3424348)Peak memory usage: 89 MB
% 4.19/1.37 % (3424348)Instructions burned: 25 (million)
% 4.19/1.37 % (3424363)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=4081340231:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.19/1.37 % (3424355)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=662722135:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.19/1.37 % (3424291)Instruction limit reached!
% 4.19/1.37 % (3424291)------------------------------
% 4.19/1.37 % (3424291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.19/1.37 % (3424291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.19/1.37 % (3424291)CaDiCaL version: 2.1.3
% 4.19/1.37 % (3424291)Termination reason: Instruction limit
% 4.19/1.37 % (3424291)Termination phase: Saturation
% 4.19/1.37 % (3424291)Time elapsed: 0.230 s
% 4.19/1.37 % (3424291)Peak memory usage: 117 MB
% 4.19/1.37 % (3424291)Instructions burned: 308 (million)
% 4.19/1.37 % (3424355)Instruction limit reached!
% 4.19/1.37 % (3424355)------------------------------
% 4.19/1.37 % (3424355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.62/1.61 % (3424355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.61 % (3424355)CaDiCaL version: 2.1.3
% 5.62/1.61 % (3424355)Termination reason: Instruction limit
% 5.62/1.61 % (3424355)Termination phase: Saturation
% 5.62/1.61 % (3424355)Time elapsed: 0.015 s
% 5.62/1.61 % (3424355)Peak memory usage: 89 MB
% 5.62/1.61 % (3424355)Instructions burned: 27 (million)
% 5.62/1.61 % (3424363)Instruction limit reached!
% 5.62/1.61 % (3424363)------------------------------
% 5.62/1.61 % (3424363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.62/1.61 % (3424363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.61 % (3424363)CaDiCaL version: 2.1.3
% 5.62/1.61 % (3424363)Termination reason: Instruction limit
% 5.62/1.61 % (3424363)Termination phase: Saturation
% 5.62/1.61 % (3424363)Time elapsed: 0.033 s
% 5.62/1.61 % (3424363)Peak memory usage: 90 MB
% 5.62/1.61 % (3424363)Instructions burned: 86 (million)
% 5.62/1.61 % (3424378)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1992828547:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.62/1.61 % (3424379)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3340731467:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.62/1.61 % (3424379)Instruction limit reached!
% 5.62/1.61 % (3424379)------------------------------
% 5.62/1.61 % (3424379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.62/1.61 % (3424379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.61 % (3424379)CaDiCaL version: 2.1.3
% 5.62/1.61 % (3424379)Termination reason: Instruction limit
% 5.62/1.61 % (3424379)Termination phase: Saturation
% 5.62/1.61 % (3424379)Time elapsed: 0.003 s
% 5.62/1.61 % (3424379)Peak memory usage: 89 MB
% 5.62/1.61 % (3424379)Instructions burned: 4 (million)
% 5.62/1.61 % (3424377)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1692498995:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.62/1.61 % (3424377)Instruction limit reached!
% 5.62/1.61 % (3424377)------------------------------
% 5.62/1.61 % (3424377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.62/1.61 % (3424377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.61 % (3424377)CaDiCaL version: 2.1.3
% 5.62/1.61 % (3424377)Termination reason: Instruction limit
% 5.62/1.61 % (3424377)Termination phase: Saturation
% 5.62/1.61 % (3424377)Time elapsed: 0.002 s
% 5.62/1.61 % (3424377)Peak memory usage: 87 MB
% 5.62/1.61 % (3424377)Instructions burned: 2 (million)
% 5.62/1.61 % (3424383)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1626487545:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.62/1.61 % (3424386)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1024086807:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 5.62/1.61 % (3424386)Instruction limit reached!
% 5.62/1.61 % (3424386)------------------------------
% 5.62/1.61 % (3424386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.62/1.61 % (3424384)lrs+10_1_thi=all:si=on:fd=off:random_seed=2795125033:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.62/1.61 % (3424386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.61 % (3424386)CaDiCaL version: 2.1.3
% 5.62/1.61 % (3424386)Termination reason: Instruction limit
% 5.62/1.61 % (3424386)Termination phase: Saturation
% 5.62/1.61 % (3424386)Time elapsed: 0.001 s
% 5.62/1.61 % (3424386)Peak memory usage: 87 MB
% 5.62/1.61 % (3424386)Instructions burned: 2 (million)
% 5.62/1.61 % (3424385)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=4056846967:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 5.62/1.61 % (3424385)Instruction limit reached!
% 5.62/1.61 % (3424385)------------------------------
% 5.62/1.61 % (3424385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.62/1.61 % (3424385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.62/1.61 % (3424385)CaDiCaL version: 2.1.3
% 5.62/1.61 % (3424385)Termination reason: Instruction limit
% 5.62/1.61 % (3424385)Termination phase: Saturation
% 7.75/2.02 % (3424385)Time elapsed: 0.006 s
% 7.75/2.02 % (3424385)Peak memory usage: 88 MB
% 7.75/2.02 % (3424385)Instructions burned: 8 (million)
% 7.75/2.02 % (3424384)Instruction limit reached!
% 7.75/2.02 % (3424384)------------------------------
% 7.75/2.02 % (3424384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3424384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3424384)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3424384)Termination reason: Instruction limit
% 7.75/2.02 % (3424384)Termination phase: Saturation
% 7.75/2.02 % (3424384)Time elapsed: 0.037 s
% 7.75/2.02 % (3424384)Peak memory usage: 116 MB
% 7.75/2.02 % (3424384)Instructions burned: 53 (million)
% 7.75/2.02 % (3424378)Instruction limit reached!
% 7.75/2.02 % (3424378)------------------------------
% 7.75/2.02 % (3424378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3424378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3424378)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3424378)Termination reason: Instruction limit
% 7.75/2.02 % (3424378)Termination phase: Saturation
% 7.75/2.02 % (3424378)Time elapsed: 0.120 s
% 7.75/2.02 % (3424378)Peak memory usage: 91 MB
% 7.75/2.02 % (3424378)Instructions burned: 182 (million)
% 7.75/2.02 % (3424383)Instruction limit reached!
% 7.75/2.02 % (3424383)------------------------------
% 7.75/2.02 % (3424383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3424383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3424383)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3424383)Termination reason: Instruction limit
% 7.75/2.02 % (3424383)Termination phase: Saturation
% 7.75/2.02 % (3424383)Time elapsed: 0.095 s
% 7.75/2.02 % (3424383)Peak memory usage: 134 MB
% 7.75/2.02 % (3424383)Instructions burned: 66 (million)
% 7.75/2.02 % (3424389)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3908618079:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 7.75/2.02 % (3424389)Instruction limit reached!
% 7.75/2.02 % (3424389)------------------------------
% 7.75/2.02 % (3424389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3424389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3424389)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3424389)Termination reason: Instruction limit
% 7.75/2.02 % (3424389)Termination phase: Saturation
% 7.75/2.02 % (3424389)Time elapsed: 0.003 s
% 7.75/2.02 % (3424389)Peak memory usage: 89 MB
% 7.75/2.02 % (3424389)Instructions burned: 3 (million)
% 7.75/2.02 % (3424396)dis+10_1_si=on:random_seed=3557462372:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 7.75/2.02 % (3424396)Instruction limit reached!
% 7.75/2.02 % (3424396)------------------------------
% 7.75/2.02 % (3424396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3424396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3424396)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3424396)Termination reason: Instruction limit
% 7.75/2.02 % (3424396)Termination phase: Saturation
% 7.75/2.02 % (3424396)Time elapsed: 0.008 s
% 7.75/2.02 % (3424396)Peak memory usage: 88 MB
% 7.75/2.02 % (3424396)Instructions burned: 11 (million)
% 7.75/2.02 % (3424398)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2614388797:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2994 on theBenchmark for (2994ds/35Mi)
% 7.75/2.02 % (3424391)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3164498356:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi)
% 7.75/2.02 % (3424397)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3741862571:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 7.75/2.02 % (3424398)Instruction limit reached!
% 7.75/2.02 % (3424398)------------------------------
% 7.75/2.02 % (3424398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.75/2.02 % (3424398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.75/2.02 % (3424398)CaDiCaL version: 2.1.3
% 7.75/2.02 % (3424398)Termination reason: Instruction limit
% 7.75/2.02 % (3424398)Termination phase: Saturation
% 7.75/2.02 % (3424398)Time elapsed: 0.015 s
% 7.75/2.02 % (3424398)Peak memory usage: 89 MB
% 7.75/2.02 % (3424398)Instructions burned: 36 (million)
% 7.75/2.02 % (3424397)Refutation not found, incomplete strategy
% 11.13/2.37 % (3424397)------------------------------
% 11.13/2.37 % (3424397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.13/2.37 % (3424397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.13/2.37 % (3424397)CaDiCaL version: 2.1.3
% 11.13/2.37 % (3424397)Termination reason: Refutation not found, incomplete strategy
% 11.13/2.37 % (3424397)Time elapsed: 0.004 s
% 11.13/2.37 % (3424397)Peak memory usage: 89 MB
% 11.13/2.37 % (3424397)Instructions burned: 4 (million)
% 11.13/2.37 % (3424399)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=297922107:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 11.13/2.37 % (3424399)Instruction limit reached!
% 11.13/2.37 % (3424399)------------------------------
% 11.13/2.37 % (3424399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.13/2.37 % (3424399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.13/2.37 % (3424399)CaDiCaL version: 2.1.3
% 11.13/2.37 % (3424399)Termination reason: Instruction limit
% 11.13/2.37 % (3424399)Termination phase: Saturation
% 11.13/2.37 % (3424399)Time elapsed: 0.002 s
% 11.13/2.37 % (3424399)Peak memory usage: 88 MB
% 11.13/2.37 % (3424399)Instructions burned: 2 (million)
% 11.13/2.37 % (3424400)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3902926216:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 11.13/2.37 % (3424391)Instruction limit reached!
% 11.13/2.37 % (3424391)------------------------------
% 11.13/2.37 % (3424391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.13/2.37 % (3424391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.13/2.37 % (3424391)CaDiCaL version: 2.1.3
% 11.13/2.37 % (3424391)Termination reason: Instruction limit
% 11.13/2.37 % (3424391)Termination phase: Saturation
% 11.13/2.37 % (3424391)Time elapsed: 0.104 s
% 11.13/2.37 % (3424391)Peak memory usage: 117 MB
% 11.13/2.37 % (3424391)Instructions burned: 127 (million)
% 11.13/2.37 % (3424400)Instruction limit reached!
% 11.13/2.37 % (3424400)------------------------------
% 11.13/2.37 % (3424400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.13/2.37 % (3424400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.13/2.37 % (3424400)CaDiCaL version: 2.1.3
% 11.13/2.37 % (3424400)Termination reason: Instruction limit
% 11.13/2.37 % (3424400)Termination phase: Saturation
% 11.13/2.37 % (3424400)Time elapsed: 0.007 s
% 11.13/2.37 % (3424400)Peak memory usage: 89 MB
% 11.13/2.37 % (3424400)Instructions burned: 9 (million)
% 11.13/2.37 % (3424402)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2214390137:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 11.13/2.37 % (3424402)Refutation not found, incomplete strategy
% 11.13/2.37 % (3424402)------------------------------
% 11.13/2.37 % (3424402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.13/2.37 % (3424402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.13/2.37 % (3424402)CaDiCaL version: 2.1.3
% 11.13/2.37 % (3424402)Termination reason: Refutation not found, incomplete strategy
% 11.13/2.37 % (3424402)Time elapsed: 0.004 s
% 11.13/2.37 % (3424402)Peak memory usage: 89 MB
% 11.13/2.37 % (3424402)Instructions burned: 3 (million)
% 11.13/2.37 % (3424408)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2018913657:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi)
% 11.13/2.37 % (3424405)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=4217716684:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 11.13/2.37 % (3424405)Instruction limit reached!
% 11.13/2.37 % (3424405)------------------------------
% 11.13/2.37 % (3424405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.13/2.37 % (3424405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.13/2.37 % (3424405)CaDiCaL version: 2.1.3
% 11.13/2.37 % (3424405)Termination reason: Instruction limit
% 11.13/2.37 % (3424405)Termination phase: Saturation
% 11.13/2.37 % (3424405)Time elapsed: 0.035 s
% 11.13/2.37 % (3424405)Peak memory usage: 116 MB
% 11.13/2.37 % (3424405)Instructions burned: 13 (million)
% 11.13/2.37 % (3424410)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=336425993:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 13.56/2.85 % (3424410)Instruction limit reached!
% 13.56/2.85 % (3424410)------------------------------
% 13.56/2.85 % (3424410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/2.85 % (3424410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/2.85 % (3424410)CaDiCaL version: 2.1.3
% 13.56/2.85 % (3424410)Termination reason: Instruction limit
% 13.56/2.85 % (3424410)Termination phase: Saturation
% 13.56/2.85 % (3424410)Time elapsed: 0.012 s
% 13.56/2.85 % (3424410)Peak memory usage: 89 MB
% 13.56/2.85 % (3424410)Instructions burned: 10 (million)
% 13.56/2.85 % (3424408)Instruction limit reached!
% 13.56/2.85 % (3424408)------------------------------
% 13.56/2.85 % (3424408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/2.85 % (3424408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/2.85 % (3424408)CaDiCaL version: 2.1.3
% 13.56/2.85 % (3424408)Termination reason: Instruction limit
% 13.56/2.85 % (3424408)Termination phase: Saturation
% 13.56/2.85 % (3424408)Time elapsed: 0.130 s
% 13.56/2.85 % (3424408)Peak memory usage: 118 MB
% 13.56/2.85 % (3424408)Instructions burned: 227 (million)
% 13.56/2.85 % (3424397)------------------------------
% 13.56/2.85 % (3424397)------------------------------
% 13.56/2.85 % (3424412)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=742451319:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 13.56/2.85 % (3424413)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=118173499:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 13.56/2.85 % (3424402)------------------------------
% 13.56/2.85 % (3424402)------------------------------
% 13.56/2.85 % (3424413)Instruction limit reached!
% 13.56/2.85 % (3424413)------------------------------
% 13.56/2.85 % (3424413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/2.85 % (3424413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/2.85 % (3424413)CaDiCaL version: 2.1.3
% 13.56/2.85 % (3424413)Termination reason: Instruction limit
% 13.56/2.85 % (3424413)Termination phase: Saturation
% 13.56/2.85 % (3424413)Time elapsed: 0.074 s
% 13.56/2.85 % (3424413)Peak memory usage: 90 MB
% 13.56/2.85 % (3424413)Instructions burned: 76 (million)
% 13.56/2.85 % (3424425)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=1035691079:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi)
% 13.56/2.85 % (3424428)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1592570463:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 13.56/2.85 % (3424412)Instruction limit reached!
% 13.56/2.85 % (3424412)------------------------------
% 13.56/2.85 % (3424412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/2.85 % (3424412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/2.85 % (3424412)CaDiCaL version: 2.1.3
% 13.56/2.85 % (3424412)Termination reason: Instruction limit
% 13.56/2.85 % (3424412)Termination phase: Saturation
% 13.56/2.85 % (3424412)Time elapsed: 0.120 s
% 13.56/2.85 % (3424412)Peak memory usage: 133 MB
% 13.56/2.85 % (3424412)Instructions burned: 72 (million)
% 13.56/2.85 % (3424427)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=704009607:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/130Mi)
% 13.56/2.85 % (3424428)Instruction limit reached!
% 13.56/2.85 % (3424428)------------------------------
% 13.56/2.85 % (3424428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.56/2.85 % (3424428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.56/2.85 % (3424428)CaDiCaL version: 2.1.3
% 13.56/2.85 % (3424428)Termination reason: Instruction limit
% 13.56/2.85 % (3424428)Termination phase: Saturation
% 13.56/2.85 % (3424428)Time elapsed: 0.107 s
% 13.56/2.85 % (3424428)Peak memory usage: 134 MB
% 13.56/2.85 % (3424428)Instructions burned: 132 (million)
% 13.56/2.85 % (3424432)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2652400894:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/40Mi)
% 13.56/2.85 % (3424446)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=788961239:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/598Mi)
% 18.28/3.40 % (3424443)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2183419422:i=307:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/307Mi)
% 18.28/3.40 % (3424451)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3187792315:i=131:canc=cautious:fsr=off:rtra=on_2988 on theBenchmark for (2988ds/131Mi)
% 18.28/3.40 % (3424427)Instruction limit reached!
% 18.28/3.40 % (3424427)------------------------------
% 18.28/3.40 % (3424427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.28/3.40 % (3424427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.28/3.40 % (3424427)CaDiCaL version: 2.1.3
% 18.28/3.40 % (3424427)Termination reason: Instruction limit
% 18.28/3.40 % (3424427)Termination phase: Saturation
% 18.28/3.40 % (3424427)Time elapsed: 0.168 s
% 18.28/3.40 % (3424427)Peak memory usage: 117 MB
% 18.28/3.40 % (3424427)Instructions burned: 131 (million)
% 18.28/3.40 % (3424432)Instruction limit reached!
% 18.28/3.40 % (3424432)------------------------------
% 18.28/3.40 % (3424432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.28/3.40 % (3424432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.28/3.40 % (3424432)CaDiCaL version: 2.1.3
% 18.28/3.40 % (3424432)Termination reason: Instruction limit
% 18.28/3.40 % (3424432)Termination phase: Saturation
% 18.28/3.40 % (3424432)Time elapsed: 0.102 s
% 18.28/3.40 % (3424432)Peak memory usage: 134 MB
% 18.28/3.40 % (3424432)Instructions burned: 41 (million)
% 18.28/3.40 % (3424455)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=2498097163:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2987 on theBenchmark for (2987ds/259Mi)
% 18.28/3.40 % (3424451)Instruction limit reached!
% 18.28/3.40 % (3424451)------------------------------
% 18.28/3.40 % (3424451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.28/3.40 % (3424451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.28/3.40 % (3424451)CaDiCaL version: 2.1.3
% 18.28/3.40 % (3424451)Termination reason: Instruction limit
% 18.28/3.40 % (3424451)Termination phase: Saturation
% 18.28/3.40 % (3424451)Time elapsed: 0.087 s
% 18.28/3.40 % (3424451)Peak memory usage: 118 MB
% 18.28/3.40 % (3424451)Instructions burned: 133 (million)
% 18.28/3.40 % (3424425)Instruction limit reached!
% 18.28/3.40 % (3424425)------------------------------
% 18.28/3.40 % (3424425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.28/3.40 % (3424425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.28/3.40 % (3424425)CaDiCaL version: 2.1.3
% 18.28/3.40 % (3424425)Termination reason: Instruction limit
% 18.28/3.40 % (3424425)Termination phase: Saturation
% 18.28/3.40 % (3424425)Time elapsed: 0.316 s
% 18.28/3.40 % (3424425)Peak memory usage: 91 MB
% 18.28/3.40 % (3424425)Instructions burned: 295 (million)
% 18.28/3.40 % (3424471)dis+10_1_si=on:random_seed=2561310596:s2a=on:i=1000:rtra=on:gtg=exists_all_2986 on theBenchmark for (2986ds/1000Mi)
% 18.28/3.40 % (3424475)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2219101768:i=65:nm=16:rtra=on_2985 on theBenchmark for (2985ds/65Mi)
% 18.28/3.40 % (3424443)Instruction limit reached!
% 18.28/3.40 % (3424443)------------------------------
% 18.28/3.40 % (3424443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.28/3.40 % (3424443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.28/3.40 % (3424443)CaDiCaL version: 2.1.3
% 18.28/3.40 % (3424443)Termination reason: Instruction limit
% 18.28/3.40 % (3424443)Termination phase: Saturation
% 18.28/3.40 % (3424443)Time elapsed: 0.321 s
% 18.28/3.40 % (3424443)Peak memory usage: 93 MB
% 18.28/3.40 % (3424443)Instructions burned: 307 (million)
% 18.28/3.40 % (3424472)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1689441827:i=383:fsr=off:rtra=on:ev=force_2985 on theBenchmark for (2985ds/383Mi)
% 18.28/3.40 % (3424455)Instruction limit reached!
% 18.28/3.40 % (3424455)------------------------------
% 18.28/3.40 % (3424455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.28/3.40 % (3424455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.28/3.40 % (3424455)CaDiCaL version: 2.1.3
% 18.28/3.40 % (3424455)Termination reason: Instruction limit
% 18.28/3.40 % (3424455)Termination phase: Saturation
% 19.99/3.62 % (3424455)Time elapsed: 0.249 s
% 19.99/3.62 % (3424455)Peak memory usage: 118 MB
% 19.99/3.62 % (3424455)Instructions burned: 260 (million)
% 19.99/3.62 % (3424475)Refutation not found, incomplete strategy
% 19.99/3.62 % (3424475)------------------------------
% 19.99/3.62 % (3424475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.99/3.62 % (3424475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.99/3.62 % (3424475)CaDiCaL version: 2.1.3
% 19.99/3.62 % (3424475)Termination reason: Refutation not found, incomplete strategy
% 19.99/3.62 % (3424475)Time elapsed: 0.050 s
% 19.99/3.62 % (3424475)Peak memory usage: 117 MB
% 19.99/3.62 % (3424475)Instructions burned: 65 (million)
% 19.99/3.62 % (3424474)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=1692392259:i=141:doe=on:rtra=on_2985 on theBenchmark for (2985ds/141Mi)
% 19.99/3.62 % (3424474)Instruction limit reached!
% 19.99/3.62 % (3424474)------------------------------
% 19.99/3.62 % (3424474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.99/3.62 % (3424474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.99/3.62 % (3424474)CaDiCaL version: 2.1.3
% 19.99/3.62 % (3424474)Termination reason: Instruction limit
% 19.99/3.62 % (3424474)Termination phase: Saturation
% 19.99/3.62 % (3424474)Time elapsed: 0.132 s
% 19.99/3.62 % (3424474)Peak memory usage: 90 MB
% 19.99/3.62 % (3424474)Instructions burned: 142 (million)
% 19.99/3.62 % (3424475)------------------------------
% 19.99/3.62 % (3424475)------------------------------
% 19.99/3.62 % (3424495)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3408634234:i=121:nm=16:rtra=on_2983 on theBenchmark for (2983ds/121Mi)
% 19.99/3.62 % (3424497)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=3779541517:s2a=on:i=128:s2at=5:ins=3:rtra=on_2982 on theBenchmark for (2982ds/128Mi)
% 19.99/3.62 % (3424446)Instruction limit reached!
% 19.99/3.62 % (3424446)------------------------------
% 19.99/3.62 % (3424446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.99/3.62 % (3424446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.99/3.62 % (3424446)CaDiCaL version: 2.1.3
% 19.99/3.62 % (3424446)Termination reason: Instruction limit
% 19.99/3.62 % (3424446)Termination phase: Saturation
% 19.99/3.62 % (3424446)Time elapsed: 0.652 s
% 19.99/3.62 % (3424446)Peak memory usage: 138 MB
% 19.99/3.62 % (3424446)Instructions burned: 598 (million)
% 19.99/3.62 % (3424472)Instruction limit reached!
% 19.99/3.62 % (3424472)------------------------------
% 19.99/3.62 % (3424472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.99/3.62 % (3424472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.99/3.62 % (3424472)CaDiCaL version: 2.1.3
% 19.99/3.62 % (3424472)Termination reason: Instruction limit
% 19.99/3.62 % (3424472)Termination phase: Saturation
% 19.99/3.62 % (3424472)Time elapsed: 0.335 s
% 19.99/3.62 % (3424472)Peak memory usage: 92 MB
% 19.99/3.62 % (3424472)Instructions burned: 383 (million)
% 19.99/3.62 % (3424495)Instruction limit reached!
% 19.99/3.62 % (3424495)------------------------------
% 19.99/3.62 % (3424495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.99/3.62 % (3424495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.99/3.62 % (3424495)CaDiCaL version: 2.1.3
% 19.99/3.62 % (3424495)Termination reason: Instruction limit
% 19.99/3.62 % (3424495)Termination phase: Saturation
% 19.99/3.62 % (3424495)Time elapsed: 0.096 s
% 19.99/3.62 % (3424495)Peak memory usage: 89 MB
% 19.99/3.62 % (3424495)Instructions burned: 121 (million)
% 19.99/3.62 % (3424508)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=255927667:i=39:ins=3:rtra=on_2981 on theBenchmark for (2981ds/39Mi)
% 19.99/3.62 % (3424510)dis+1010_1_to=kbo:si=on:random_seed=3584255763:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2980 on theBenchmark for (2980ds/175Mi)
% 19.99/3.62 % (3424497)Instruction limit reached!
% 19.99/3.62 % (3424497)------------------------------
% 19.99/3.62 % (3424497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.99/3.62 % (3424497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.99/3.62 % (3424497)CaDiCaL version: 2.1.3
% 19.99/3.62 % (3424497)Termination reason: Instruction limit
% 19.99/3.62 % (3424497)Termination phase: Saturation
% 19.99/3.62 % (3424497)Time elapsed: 0.182 s
% 19.99/3.62 % (3424497)Peak memory usage: 117 MB
% 19.99/3.62 % (3424497)Instructions burned: 128 (million)
% 19.99/3.62 % (3424508)Instruction limit reached!
% 19.99/3.62 % (3424508)------------------------------
% 19.99/3.62 % (3424508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.99/3.62 % (3424508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.99/3.62 % (3424508)CaDiCaL version: 2.1.3
% 19.99/3.62 % (3424508)Termination reason: Instruction limit
% 19.99/3.62 % (3424508)Termination phase: Saturation
% 19.99/3.62 % (3424508)Time elapsed: 0.076 s
% 19.99/3.62 % (3424508)Peak memory usage: 116 MB
% 19.99/3.62 % (3424508)Instructions burned: 40 (million)
% 19.99/3.62 % (3424518)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=14305111:s2a=on:i=483:doe=on:nm=32:rtra=on_2979 on theBenchmark for (2979ds/483Mi)
% 19.99/3.62 % (3424510)Instruction limit reached!
% 19.99/3.62 % (3424510)------------------------------
% 19.99/3.62 % (3424510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.99/3.62 % (3424510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.99/3.62 % (3424510)CaDiCaL version: 2.1.3
% 19.99/3.62 % (3424510)Termination reason: Instruction limit
% 19.99/3.62 % (3424510)Termination phase: Saturation
% 19.99/3.62 % (3424510)Time elapsed: 0.106 s
% 19.99/3.62 % (3424510)Peak memory usage: 91 MB
% 19.99/3.62 % (3424510)Instructions burned: 177 (million)
% 19.99/3.62 % (3424523)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=4150282237:thitd=on:i=215:nm=0:rtra=on:ev=force_2979 on theBenchmark for (2979ds/215Mi)
% 19.99/3.62 % (3424517)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2109629203:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2979 on theBenchmark for (2979ds/329Mi)
% 19.99/3.62 % (3424530)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1852902049:i=349:rtra=on_2978 on theBenchmark for (2978ds/349Mi)
% 19.99/3.62 % (3424535)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3241236818:i=328:kws=inv_frequency:nm=20:rtra=on_2977 on theBenchmark for (2977ds/328Mi)
% 19.99/3.62 % (3424533)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1324248021:st=2:i=295:rtra=on:ss=axioms_2977 on theBenchmark for (2977ds/295Mi)
% 19.99/3.62 % (3424523)First to succeed.
% 19.99/3.62 % (3424523)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3424219"
% 19.99/3.62 % (3424471)Instruction limit reached!
% 19.99/3.62 % (3424471)------------------------------
% 19.99/3.62 % (3424471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.99/3.62 % (3424471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.99/3.62 % (3424471)CaDiCaL version: 2.1.3
% 19.99/3.62 % (3424471)Termination reason: Instruction limit
% 19.99/3.62 % (3424471)Termination phase: Saturation
% 19.99/3.62 % (3424471)Time elapsed: 0.926 s
% 19.99/3.62 % (3424471)Peak memory usage: 94 MB
% 19.99/3.62 % (3424471)Instructions burned: 1000 (million)
% 19.99/3.62 % (3424517)Instruction limit reached!
% 19.99/3.62 % (3424517)------------------------------
% 19.99/3.62 % (3424517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.99/3.62 % (3424517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.99/3.62 % (3424517)CaDiCaL version: 2.1.3
% 19.99/3.62 % (3424517)Termination reason: Instruction limit
% 19.99/3.62 % (3424517)Termination phase: Saturation
% 19.99/3.62 % (3424517)Time elapsed: 0.340 s
% 19.99/3.62 % (3424517)Peak memory usage: 119 MB
% 19.99/3.62 % (3424517)Instructions burned: 329 (million)
% 19.99/3.62 % (3424535)Instruction limit reached!
% 19.99/3.62 % (3424535)------------------------------
% 19.99/3.62 % (3424535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.99/3.62 % (3424535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.99/3.62 % (3424535)CaDiCaL version: 2.1.3
% 19.99/3.62 % (3424535)Termination reason: Instruction limit
% 19.99/3.62 % (3424535)Termination phase: Saturation
% 19.99/3.62 % (3424535)Time elapsed: 0.185 s
% 19.99/3.62 % (3424535)Peak memory usage: 119 MB
% 19.99/3.62 % (3424535)Instructions burned: 328 (million)
% 19.99/3.62 % (3424533)Instruction limit reached!
% 19.99/3.62 % (3424533)------------------------------
% 19.99/3.62 % (3424533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.99/3.62 % (3424533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.99/3.62 % (3424533)CaDiCaL version: 2.1.3
% 19.99/3.62 % (3424533)Termination reason: Instruction limit
% 19.99/3.62 % (3424533)Termination phase: Saturation
% 19.99/3.62 % (3424533)Time elapsed: 0.263 s
% 19.99/3.62 % (3424533)Peak memory usage: 91 MB
% 19.99/3.62 % (3424533)Instructions burned: 295 (million)
% 19.99/3.62 % (3424518)Instruction limit reached!
% 19.99/3.62 % (3424518)------------------------------
% 19.99/3.62 % (3424518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.99/3.62 % (3424518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.99/3.62 % (3424518)CaDiCaL version: 2.1.3
% 19.99/3.62 % (3424518)Termination reason: Instruction limit
% 19.99/3.62 % (3424518)Termination phase: Saturation
% 19.99/3.62 % (3424518)Time elapsed: 0.535 s
% 19.99/3.62 % (3424518)Peak memory usage: 136 MB
% 19.99/3.62 % (3424518)Instructions burned: 483 (million)
% 19.99/3.62 % (3424557)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=143993519:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2973 on theBenchmark for (2973ds/321Mi)
% 19.99/3.62 % (3424530)Instruction limit reached!
% 19.99/3.62 % (3424530)------------------------------
% 19.99/3.62 % (3424530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.99/3.62 % (3424530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.99/3.62 % (3424530)CaDiCaL version: 2.1.3
% 19.99/3.62 % (3424530)Termination reason: Instruction limit
% 19.99/3.62 % (3424530)Termination phase: Saturation
% 19.99/3.62 % (3424530)Time elapsed: 0.382 s
% 19.99/3.62 % (3424530)Peak memory usage: 119 MB
% 19.99/3.62 % (3424530)Instructions burned: 349 (million)
% 19.99/3.62 % (3424551)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=465830796:i=281:gtgl=2:rtra=on:gtg=all_2974 on theBenchmark for (2974ds/281Mi)
% 19.99/3.62 % (3424556)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2586091684:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2973 on theBenchmark for (2973ds/484Mi)
% 19.99/3.62 % (3424557)Instruction limit reached!
% 19.99/3.62 % (3424557)------------------------------
% 19.99/3.62 % (3424557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.99/3.62 % (3424557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.99/3.63 % (3424557)CaDiCaL version: 2.1.3
% 19.99/3.63 % (3424557)Termination reason: Instruction limit
% 19.99/3.63 % (3424557)Termination phase: Saturation
% 19.99/3.63 % (3424557)Time elapsed: 0.131 s
% 19.99/3.63 % (3424557)Peak memory usage: 114 MB
% 19.99/3.63 % (3424557)Instructions burned: 322 (million)
% 19.99/3.63 % (3424523)Refutation found. Thanks to Tanya!
% 19.99/3.63 % SZS status Theorem for theBenchmark
% 19.99/3.63 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/3.90 % (3424523)------------------------------
% 0.20/3.90 % (3424523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.20/3.90 % (3424523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.90 % (3424523)CaDiCaL version: 2.1.3
% 0.20/3.90 % (3424523)Termination reason: Refutation
% 0.20/3.90 % (3424523)Time elapsed: 0.250 s
% 0.20/3.90 % (3424523)Peak memory usage: 136 MB
% 0.20/3.90 % (3424523)Instructions burned: 191 (million)
% 0.20/3.90 % (3424523)------------------------------
% 0.20/3.90 % (3424523)------------------------------
% 0.20/3.90 % (3424219)Success in time 2.95 s
% 0.20/3.90 % Vampire exiting
%------------------------------------------------------------------------------