%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW630_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:30:59 PM UTC 2026
% Result : Theorem 17.88s 3.52s
% Output : Refutation 20.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 78
% Syntax : Number of formulae : 267 ( 92 unt; 0 typ; 65 def)
% Number of atoms : 815 ( 189 equ)
% Maximal formula atoms : 24 ( 3 avg)
% Number of connectives : 884 ( 336 ~; 288 |; 134 &)
% ( 48 <=>; 78 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number arithmetic : 1117 ( 293 atm; 286 fun; 377 num; 161 var)
% Number of types : 10 ( 8 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 52 ( 48 usr; 47 prp; 0-2 aty)
% Number of functors : 85 ( 77 usr; 45 con; 0-5 aty)
% Number of variables : 263 ( 239 !; 24 ?; 263 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool: $tType ).
tff(type_def_8,type,
tuple0: $tType ).
tff(type_def_9,type,
candidate: $tType ).
tff(type_def_10,type,
lparray_candidatecm_candidaterp: $tType ).
tff(type_def_11,type,
array_candidate: $tType ).
tff(type_def_12,type,
map_int_candidate: $tType ).
tff(func_def_0,type,
witness: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool1: ty ).
tff(func_def_4,type,
true: bool ).
tff(func_def_5,type,
false: bool ).
tff(func_def_6,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(func_def_7,type,
tuple01: ty ).
tff(func_def_8,type,
tuple02: tuple0 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
ref: ty > ty ).
tff(func_def_13,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_14,type,
contents: ( ty * uni ) > uni ).
tff(func_def_15,type,
map: ( ty * ty ) > ty ).
tff(func_def_16,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_17,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_18,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_19,type,
array: ty > ty ).
tff(func_def_20,type,
mk_array: ( ty * $int * uni ) > uni ).
tff(func_def_21,type,
length: ( ty * uni ) > $int ).
tff(func_def_22,type,
elts: ( ty * uni ) > uni ).
tff(func_def_23,type,
get1: ( ty * uni * $int ) > uni ).
tff(func_def_24,type,
t2tb: $int > uni ).
tff(func_def_25,type,
tb2t: uni > $int ).
tff(func_def_26,type,
set1: ( ty * uni * $int * uni ) > uni ).
tff(func_def_27,type,
make: ( ty * $int * uni ) > uni ).
tff(func_def_28,type,
candidate1: ty ).
tff(func_def_29,type,
tuple2: ( ty * ty ) > ty ).
tff(func_def_30,type,
tuple21: ( ty * ty * uni * uni ) > uni ).
tff(func_def_31,type,
tuple2_proj_1: ( ty * ty * uni ) > uni ).
tff(func_def_32,type,
tuple2_proj_2: ( ty * ty * uni ) > uni ).
tff(func_def_33,type,
t2tb1: lparray_candidatecm_candidaterp > uni ).
tff(func_def_34,type,
tb2t1: uni > lparray_candidatecm_candidaterp ).
tff(func_def_35,type,
t2tb2: array_candidate > uni ).
tff(func_def_36,type,
tb2t2: uni > array_candidate ).
tff(func_def_37,type,
t2tb3: candidate > uni ).
tff(func_def_38,type,
tb2t3: uni > candidate ).
tff(func_def_39,type,
num_of: ( lparray_candidatecm_candidaterp * $int * $int ) > $int ).
tff(func_def_43,type,
numof: ( array_candidate * candidate * $int * $int ) > $int ).
tff(func_def_44,type,
t2tb4: map_int_candidate > uni ).
tff(func_def_45,type,
tb2t4: uni > map_int_candidate ).
tff(func_def_48,type,
sK0: ( $int * lparray_candidatecm_candidaterp * $int ) > $int ).
tff(func_def_49,type,
sK1: ( lparray_candidatecm_candidaterp * $int * $int ) > $int ).
tff(func_def_50,type,
sK2: ( lparray_candidatecm_candidaterp * $int * lparray_candidatecm_candidaterp * $int ) > $int ).
tff(func_def_51,type,
sK3: ( $int * lparray_candidatecm_candidaterp * lparray_candidatecm_candidaterp * $int ) > $int ).
tff(func_def_52,type,
sK4: map_int_candidate ).
tff(func_def_53,type,
sK5: $int ).
tff(func_def_54,type,
sK6: $int ).
tff(func_def_55,type,
sK7: candidate ).
tff(func_def_56,type,
sK8: $int ).
tff(func_def_57,type,
sK9: $int ).
tff(func_def_58,type,
sK10: $int ).
tff(func_def_59,type,
sK11: $int ).
tff(func_def_60,type,
sF12: $int ).
tff(func_def_61,type,
sF13: $int ).
tff(func_def_62,type,
sF14: $int ).
tff(func_def_63,type,
sF15: $int ).
tff(func_def_64,type,
sF16: $int ).
tff(func_def_65,type,
sF17: ty ).
tff(func_def_66,type,
sF18: uni ).
tff(func_def_67,type,
sF19: uni ).
tff(func_def_68,type,
sF20: uni ).
tff(func_def_69,type,
sF21: uni ).
tff(func_def_70,type,
sF22: lparray_candidatecm_candidaterp ).
tff(func_def_71,type,
sF23: $int ).
tff(func_def_72,type,
sF24: $int ).
tff(func_def_73,type,
sF25: $int ).
tff(func_def_74,type,
sF26: $int ).
tff(func_def_75,type,
sF27: uni ).
tff(func_def_76,type,
sF28: uni ).
tff(func_def_77,type,
sF29: candidate ).
tff(func_def_78,type,
sF30: $int ).
tff(func_def_79,type,
sF31: $int ).
tff(func_def_80,type,
sF32: $int ).
tff(func_def_81,type,
sF33: $int ).
tff(func_def_82,type,
sF34: $int ).
tff(func_def_83,type,
sF35: $int ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_3,type,
pr: ( lparray_candidatecm_candidaterp * $int ) > $o ).
tff(f13,axiom,
! [X1: ty,X0: ty,X2: uni,X3: uni] : sort(X1,get(X1,X0,X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',get_sort) ).
tff(f22,axiom,
! [X1: $int,X0: ty,X2: uni] :
( sort(map(int,X0),X2)
=> ( elts(X0,mk_array(X0,X1,X2)) = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',elts_def) ).
tff(f28,axiom,
! [X1: uni,X0: ty,X2: $int] : ( get1(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',get_def) ).
tff(f44,axiom,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR2) ).
tff(f46,axiom,
! [X0: candidate] : ( tb2t3(t2tb3(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeL3) ).
tff(f47,axiom,
! [X0: uni] :
( sort(candidate1,X0)
=> ( t2tb3(tb2t3(X0)) = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR3) ).
tff(f48,axiom,
! [X1: array_candidate,X2: candidate,X0: $int] :
( ( tb2t3(get1(candidate1,t2tb2(X1),X0)) = X2 )
<=> pr(tb2t1(tuple21(array(candidate1),candidate1,t2tb2(X1),t2tb3(X2))),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pr_def) ).
tff(f49,axiom,
! [X0: lparray_candidatecm_candidaterp,X2: $int,X1: $int] :
( $lesseq(X2,X1)
=> ( num_of(X0,X1,X2) = 0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',num_of_empty) ).
tff(f53,axiom,
! [X1: $int,X0: lparray_candidatecm_candidaterp,X3: $int,X2: $int] :
( ( $lesseq(X2,X3)
& $lesseq(X1,X2) )
=> ( num_of(X0,X1,X3) = $sum(num_of(X0,X1,X2),num_of(X0,X2,X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',num_of_append) ).
tff(f58,axiom,
! [X3: $int,X2: $int,X1: $int,X0: lparray_candidatecm_candidaterp] :
( ( $lesseq(X2,X3)
& $lesseq(X1,X2) )
=> $lesseq(num_of(X0,X1,X2),num_of(X0,X1,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',num_of_increasing) ).
tff(f59,axiom,
! [X2: $int,X0: lparray_candidatecm_candidaterp,X3: $int,X1: $int,X4: $int] :
( ( $lesseq(X1,X2)
& $lesseq(X2,X3)
& $less(X3,X4) )
=> ( pr(X0,X3)
=> $less(num_of(X0,X1,X2),num_of(X0,X1,X4)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',num_of_strictly_increasing) ).
tff(f63,axiom,
! [X0: map_int_candidate] : sort(map(int,candidate1),t2tb4(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort4) ).
tff(f66,conjecture,
! [X0: $int,X1: map_int_candidate] :
( ( $lesseq(0,X0)
& $lesseq(1,X0) )
=> ( ( $less(0,X0)
& $lesseq(0,0) )
=> ( $lesseq(0,$difference(X0,1))
=> ! [X3: candidate,X2: $int] :
( ( $lesseq($product(2,$difference(num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X3))),0,$sum($difference(X0,1),1)),X2)),$difference($sum($difference(X0,1),1),X2))
& $lesseq(0,X2)
& $lesseq(X2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X3))),0,$sum($difference(X0,1),1)))
& ! [X4: candidate] :
( ( X4 != X3 )
=> $lesseq($product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X4))),0,$sum($difference(X0,1),1))),$difference($sum($difference(X0,1),1),X2)) ) )
=> ( ( X2 != 0 )
=> ( ~ $less(X0,$product(2,X2))
=> ! [X5: $int] :
( ( X5 = 0 )
=> ( $lesseq(0,$difference(X0,1))
=> ! [X6: $int,X7: $int] :
( ( $lesseq(0,X7)
& $lesseq(X7,$difference(X0,1)) )
=> ( ( $lesseq($product(2,X6),X0)
& ( X6 = num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X3))),0,X7) ) )
=> ( ( $lesseq(0,X7)
& $less(X7,X0) )
=> ( ( tb2t3(get(candidate1,int,t2tb4(X1),t2tb(X7))) = X3 )
=> ! [X8: $int] :
( ( X8 = $sum(X6,1) )
=> ( $less(X0,$product(2,X8))
=> $less(X0,$product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X3))),0,X0))) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_mjrty) ).
tff(f67,negated_conjecture,
~ ! [X0: $int,X1: map_int_candidate] :
( ( $lesseq(0,X0)
& $lesseq(1,X0) )
=> ( ( $less(0,X0)
& $lesseq(0,0) )
=> ( $lesseq(0,$difference(X0,1))
=> ! [X3: candidate,X2: $int] :
( ( $lesseq($product(2,$difference(num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X3))),0,$sum($difference(X0,1),1)),X2)),$difference($sum($difference(X0,1),1),X2))
& $lesseq(0,X2)
& $lesseq(X2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X3))),0,$sum($difference(X0,1),1)))
& ! [X4: candidate] :
( ( X4 != X3 )
=> $lesseq($product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X4))),0,$sum($difference(X0,1),1))),$difference($sum($difference(X0,1),1),X2)) ) )
=> ( ( X2 != 0 )
=> ( ~ $less(X0,$product(2,X2))
=> ! [X5: $int] :
( ( X5 = 0 )
=> ( $lesseq(0,$difference(X0,1))
=> ! [X6: $int,X7: $int] :
( ( $lesseq(0,X7)
& $lesseq(X7,$difference(X0,1)) )
=> ( ( $lesseq($product(2,X6),X0)
& ( X6 = num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X3))),0,X7) ) )
=> ( ( $lesseq(0,X7)
& $less(X7,X0) )
=> ( ( tb2t3(get(candidate1,int,t2tb4(X1),t2tb(X7))) = X3 )
=> ! [X8: $int] :
( ( X8 = $sum(X6,1) )
=> ( $less(X0,$product(2,X8))
=> $less(X0,$product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X3))),0,X0))) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f66]) ).
tff(f69,plain,
! [X0: lparray_candidatecm_candidaterp,X2: $int,X1: $int] :
( ~ $less(X1,X2)
=> ( num_of(X0,X1,X2) = 0 ) ),
inference(theory_normalization,[],[f49]) ).
tff(f73,plain,
! [X3: $int,X2: $int,X1: $int,X0: lparray_candidatecm_candidaterp] :
( ( ~ $less(X3,X2)
& ~ $less(X2,X1) )
=> ~ $less(num_of(X0,X1,X3),num_of(X0,X1,X2)) ),
inference(theory_normalization,[],[f58]) ).
tff(f75,plain,
! [X1: $int,X0: lparray_candidatecm_candidaterp,X3: $int,X2: $int] :
( ( ~ $less(X3,X2)
& ~ $less(X2,X1) )
=> ( num_of(X0,X1,X3) = $sum(num_of(X0,X1,X2),num_of(X0,X2,X3)) ) ),
inference(theory_normalization,[],[f53]) ).
tff(f77,plain,
! [X2: $int,X0: lparray_candidatecm_candidaterp,X3: $int,X1: $int,X4: $int] :
( ( ~ $less(X2,X1)
& ~ $less(X3,X2)
& $less(X3,X4) )
=> ( pr(X0,X3)
=> $less(num_of(X0,X1,X2),num_of(X0,X1,X4)) ) ),
inference(theory_normalization,[],[f59]) ).
tff(f79,plain,
~ ! [X0: $int,X1: map_int_candidate] :
( ( ~ $less(X0,0)
& ~ $less(X0,1) )
=> ( ( ~ $less(0,0)
& $less(0,X0) )
=> ( ~ $less($sum(X0,$uminus(1)),0)
=> ! [X3: candidate,X2: $int] :
( ( ~ $less($sum($sum($sum(X0,$uminus(1)),1),$uminus(X2)),$product(2,$sum(num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X3))),0,$sum($sum(X0,$uminus(1)),1)),$uminus(X2))))
& ~ $less(X2,0)
& ~ $less(num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X3))),0,$sum($sum(X0,$uminus(1)),1)),X2)
& ! [X4: candidate] :
( ( X4 != X3 )
=> ~ $less($sum($sum($sum(X0,$uminus(1)),1),$uminus(X2)),$product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X4))),0,$sum($sum(X0,$uminus(1)),1)))) ) )
=> ( ( X2 != 0 )
=> ( ~ $less(X0,$product(2,X2))
=> ! [X5: $int] :
( ( X5 = 0 )
=> ( ~ $less($sum(X0,$uminus(1)),0)
=> ! [X6: $int,X7: $int] :
( ( ~ $less($sum(X0,$uminus(1)),X7)
& ~ $less(X7,0) )
=> ( ( ~ $less(X0,$product(2,X6))
& ( X6 = num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X3))),0,X7) ) )
=> ( ( ~ $less(X7,0)
& $less(X7,X0) )
=> ( ( tb2t3(get(candidate1,int,t2tb4(X1),t2tb(X7))) = X3 )
=> ! [X8: $int] :
( ( X8 = $sum(X6,1) )
=> ( $less(X0,$product(2,X8))
=> $less(X0,$product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X3))),0,X0))) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f67]) ).
tff(f82,plain,
! [X2: $int,X1: $int,X0: lparray_candidatecm_candidaterp] :
( ~ $less(X2,X1)
=> ( 0 = num_of(X0,X2,X1) ) ),
inference(rectify,[],[f69]) ).
tff(f97,plain,
! [X2: $int,X1: $int,X0: $int,X3: lparray_candidatecm_candidaterp] :
( ( ~ $less(X0,X1)
& ~ $less(X1,X2) )
=> ~ $less(num_of(X3,X2,X0),num_of(X3,X2,X1)) ),
inference(rectify,[],[f73]) ).
tff(f103,plain,
! [X0: $int,X2: $int,X1: lparray_candidatecm_candidaterp,X3: $int] :
( ( ~ $less(X2,X3)
& ~ $less(X3,X0) )
=> ( $sum(num_of(X1,X0,X3),num_of(X1,X3,X2)) = num_of(X1,X0,X2) ) ),
inference(rectify,[],[f75]) ).
tff(f107,plain,
! [X2: $int,X0: array_candidate,X1: candidate] :
( pr(tb2t1(tuple21(array(candidate1),candidate1,t2tb2(X0),t2tb3(X1))),X2)
<=> ( tb2t3(get1(candidate1,t2tb2(X0),X2)) = X1 ) ),
inference(rectify,[],[f48]) ).
tff(f108,plain,
! [X2: uni,X0: $int,X1: ty] :
( sort(map(int,X1),X2)
=> ( elts(X1,mk_array(X1,X0,X2)) = X2 ) ),
inference(rectify,[],[f22]) ).
tff(f109,plain,
! [X4: $int,X0: $int,X3: $int,X1: lparray_candidatecm_candidaterp,X2: $int] :
( ( ~ $less(X2,X0)
& ~ $less(X0,X3)
& $less(X2,X4) )
=> ( pr(X1,X2)
=> $less(num_of(X1,X3,X0),num_of(X1,X3,X4)) ) ),
inference(rectify,[],[f77]) ).
tff(f113,plain,
~ ! [X0: $int,X1: map_int_candidate] :
( ( ~ $less(X0,0)
& ~ $less(X0,1) )
=> ( ( ~ $less(0,0)
& $less(0,X0) )
=> ( ~ $less($sum(X0,$uminus(1)),0)
=> ! [X3: $int,X2: candidate] :
( ( ~ $less($sum($sum($sum(X0,$uminus(1)),1),$uminus(X3)),$product(2,$sum(num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X2))),0,$sum($sum(X0,$uminus(1)),1)),$uminus(X3))))
& ~ $less(X3,0)
& ~ $less(num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X2))),0,$sum($sum(X0,$uminus(1)),1)),X3)
& ! [X4: candidate] :
( ( X2 != X4 )
=> ~ $less($sum($sum($sum(X0,$uminus(1)),1),$uminus(X3)),$product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X4))),0,$sum($sum(X0,$uminus(1)),1)))) ) )
=> ( ( 0 != X3 )
=> ( ~ $less(X0,$product(2,X3))
=> ! [X5: $int] :
( ( X5 = 0 )
=> ( ~ $less($sum(X0,$uminus(1)),0)
=> ! [X6: $int,X7: $int] :
( ( ~ $less($sum(X0,$uminus(1)),X7)
& ~ $less(X7,0) )
=> ( ( ( num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X2))),0,X7) = X6 )
& ~ $less(X0,$product(2,X6)) )
=> ( ( ~ $less(X7,0)
& $less(X7,X0) )
=> ( ( tb2t3(get(candidate1,int,t2tb4(X1),t2tb(X7))) = X2 )
=> ! [X8: $int] :
( ( X8 = $sum(X6,1) )
=> ( $less(X0,$product(2,X8))
=> $less(X0,$product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X2))),0,X0))) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f79]) ).
tff(f114,plain,
! [X0: ty,X3: uni,X1: ty,X2: uni] : sort(X0,get(X0,X1,X2,X3)),
inference(rectify,[],[f13]) ).
tff(f119,plain,
! [X4: $int,X0: $int,X3: $int,X1: lparray_candidatecm_candidaterp,X2: $int] :
( $less(num_of(X1,X3,X0),num_of(X1,X3,X4))
| ~ pr(X1,X2)
| $less(X2,X0)
| $less(X0,X3)
| ~ $less(X2,X4) ),
inference(ennf_transformation,[],[f109]) ).
tff(f120,plain,
! [X1: lparray_candidatecm_candidaterp,X4: $int,X0: $int,X3: $int,X2: $int] :
( ~ $less(X2,X4)
| $less(X0,X3)
| $less(num_of(X1,X3,X0),num_of(X1,X3,X4))
| $less(X2,X0)
| ~ pr(X1,X2) ),
inference(flattening,[],[f119]) ).
tff(f121,plain,
! [X0: uni] :
( ( t2tb3(tb2t3(X0)) = X0 )
| ~ sort(candidate1,X0) ),
inference(ennf_transformation,[],[f47]) ).
tff(f122,plain,
! [X0: lparray_candidatecm_candidaterp,X1: $int,X2: $int] :
( $less(X2,X1)
| ( 0 = num_of(X0,X2,X1) ) ),
inference(ennf_transformation,[],[f82]) ).
tff(f123,plain,
! [X0: $int,X2: $int,X1: lparray_candidatecm_candidaterp,X3: $int] :
( ( $sum(num_of(X1,X0,X3),num_of(X1,X3,X2)) = num_of(X1,X0,X2) )
| $less(X2,X3)
| $less(X3,X0) ),
inference(ennf_transformation,[],[f103]) ).
tff(f124,plain,
! [X3: $int,X2: $int,X1: lparray_candidatecm_candidaterp,X0: $int] :
( $less(X3,X0)
| ( $sum(num_of(X1,X0,X3),num_of(X1,X3,X2)) = num_of(X1,X0,X2) )
| $less(X2,X3) ),
inference(flattening,[],[f123]) ).
tff(f139,plain,
? [X0: $int,X1: map_int_candidate] :
( ? [X3: $int,X2: candidate] :
( ? [X5: $int] :
( ? [X6: $int,X7: $int] :
( ? [X8: $int] :
( ~ $less(X0,$product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X2))),0,X0)))
& $less(X0,$product(2,X8))
& ( X8 = $sum(X6,1) ) )
& ( tb2t3(get(candidate1,int,t2tb4(X1),t2tb(X7))) = X2 )
& ~ $less(X7,0)
& $less(X7,X0)
& ( num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X2))),0,X7) = X6 )
& ~ $less(X0,$product(2,X6))
& ~ $less($sum(X0,$uminus(1)),X7)
& ~ $less(X7,0) )
& ~ $less($sum(X0,$uminus(1)),0)
& ( X5 = 0 ) )
& ~ $less(X0,$product(2,X3))
& ( 0 != X3 )
& ~ $less($sum($sum($sum(X0,$uminus(1)),1),$uminus(X3)),$product(2,$sum(num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X2))),0,$sum($sum(X0,$uminus(1)),1)),$uminus(X3))))
& ~ $less(X3,0)
& ~ $less(num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X2))),0,$sum($sum(X0,$uminus(1)),1)),X3)
& ! [X4: candidate] :
( ( X2 = X4 )
| ~ $less($sum($sum($sum(X0,$uminus(1)),1),$uminus(X3)),$product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X4))),0,$sum($sum(X0,$uminus(1)),1)))) ) )
& ~ $less($sum(X0,$uminus(1)),0)
& ~ $less(0,0)
& $less(0,X0)
& ~ $less(X0,0)
& ~ $less(X0,1) ),
inference(ennf_transformation,[],[f113]) ).
tff(f140,plain,
? [X1: map_int_candidate,X0: $int] :
( ~ $less($sum(X0,$uminus(1)),0)
& ~ $less(0,0)
& ~ $less(X0,1)
& $less(0,X0)
& ~ $less(X0,0)
& ? [X3: $int,X2: candidate] :
( ~ $less(X3,0)
& ~ $less($sum($sum($sum(X0,$uminus(1)),1),$uminus(X3)),$product(2,$sum(num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X2))),0,$sum($sum(X0,$uminus(1)),1)),$uminus(X3))))
& ~ $less(num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X2))),0,$sum($sum(X0,$uminus(1)),1)),X3)
& ( 0 != X3 )
& ! [X4: candidate] :
( ( X2 = X4 )
| ~ $less($sum($sum($sum(X0,$uminus(1)),1),$uminus(X3)),$product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X4))),0,$sum($sum(X0,$uminus(1)),1)))) )
& ? [X5: $int] :
( ~ $less($sum(X0,$uminus(1)),0)
& ? [X7: $int,X6: $int] :
( ~ $less(X7,0)
& ~ $less(X0,$product(2,X6))
& ( tb2t3(get(candidate1,int,t2tb4(X1),t2tb(X7))) = X2 )
& ? [X8: $int] :
( ( X8 = $sum(X6,1) )
& $less(X0,$product(2,X8))
& ~ $less(X0,$product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X2))),0,X0))) )
& ~ $less(X7,0)
& $less(X7,X0)
& ~ $less($sum(X0,$uminus(1)),X7)
& ( num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X0,t2tb4(X1)),t2tb3(X2))),0,X7) = X6 ) )
& ( X5 = 0 ) )
& ~ $less(X0,$product(2,X3)) ) ),
inference(flattening,[],[f139]) ).
tff(f144,plain,
! [X0: $int,X2: uni,X1: ty] :
( ( elts(X1,mk_array(X1,X0,X2)) = X2 )
| ~ sort(map(int,X1),X2) ),
inference(ennf_transformation,[],[f108]) ).
tff(f151,plain,
! [X2: $int,X1: $int,X0: $int,X3: lparray_candidatecm_candidaterp] :
( ~ $less(num_of(X3,X2,X0),num_of(X3,X2,X1))
| $less(X0,X1)
| $less(X1,X2) ),
inference(ennf_transformation,[],[f97]) ).
tff(f152,plain,
! [X3: lparray_candidatecm_candidaterp,X0: $int,X2: $int,X1: $int] :
( $less(X0,X1)
| $less(X1,X2)
| ~ $less(num_of(X3,X2,X0),num_of(X3,X2,X1)) ),
inference(flattening,[],[f151]) ).
tff(f169,plain,
! [X2: $int,X0: array_candidate,X1: candidate] :
( ( pr(tb2t1(tuple21(array(candidate1),candidate1,t2tb2(X0),t2tb3(X1))),X2)
| ( tb2t3(get1(candidate1,t2tb2(X0),X2)) != X1 ) )
& ( ( tb2t3(get1(candidate1,t2tb2(X0),X2)) = X1 )
| ~ pr(tb2t1(tuple21(array(candidate1),candidate1,t2tb2(X0),t2tb3(X1))),X2) ) ),
inference(nnf_transformation,[],[f107]) ).
tff(f170,plain,
! [X0: $int,X1: array_candidate,X2: candidate] :
( ( pr(tb2t1(tuple21(array(candidate1),candidate1,t2tb2(X1),t2tb3(X2))),X0)
| ( tb2t3(get1(candidate1,t2tb2(X1),X0)) != X2 ) )
& ( ( tb2t3(get1(candidate1,t2tb2(X1),X0)) = X2 )
| ~ pr(tb2t1(tuple21(array(candidate1),candidate1,t2tb2(X1),t2tb3(X2))),X0) ) ),
inference(rectify,[],[f169]) ).
tff(f172,plain,
! [X0: $int,X1: $int,X2: lparray_candidatecm_candidaterp,X3: $int] :
( $less(X0,X3)
| ( num_of(X2,X3,X1) = $sum(num_of(X2,X3,X0),num_of(X2,X0,X1)) )
| $less(X1,X0) ),
inference(rectify,[],[f124]) ).
tff(f175,plain,
! [X0: $int,X1: uni,X2: ty] :
( ( elts(X2,mk_array(X2,X0,X1)) = X1 )
| ~ sort(map(int,X2),X1) ),
inference(rectify,[],[f144]) ).
tff(f184,plain,
! [X0: uni,X1: ty,X2: $int] : ( get(X1,int,elts(X1,X0),t2tb(X2)) = get1(X1,X0,X2) ),
inference(rectify,[],[f28]) ).
tff(f192,plain,
! [X0: lparray_candidatecm_candidaterp,X1: $int,X2: $int,X3: $int,X4: $int] :
( ~ $less(X4,X1)
| $less(X2,X3)
| $less(num_of(X0,X3,X2),num_of(X0,X3,X1))
| $less(X4,X2)
| ~ pr(X0,X4) ),
inference(rectify,[],[f120]) ).
tff(f196,plain,
? [X0: map_int_candidate,X1: $int] :
( ~ $less($sum(X1,$uminus(1)),0)
& ~ $less(0,0)
& ~ $less(X1,1)
& $less(0,X1)
& ~ $less(X1,0)
& ? [X2: $int,X3: candidate] :
( ~ $less(X2,0)
& ~ $less($sum($sum($sum(X1,$uminus(1)),1),$uminus(X2)),$product(2,$sum(num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X1,t2tb4(X0)),t2tb3(X3))),0,$sum($sum(X1,$uminus(1)),1)),$uminus(X2))))
& ~ $less(num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X1,t2tb4(X0)),t2tb3(X3))),0,$sum($sum(X1,$uminus(1)),1)),X2)
& ( 0 != X2 )
& ! [X4: candidate] :
( ( X3 = X4 )
| ~ $less($sum($sum($sum(X1,$uminus(1)),1),$uminus(X2)),$product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X1,t2tb4(X0)),t2tb3(X4))),0,$sum($sum(X1,$uminus(1)),1)))) )
& ? [X5: $int] :
( ~ $less($sum(X1,$uminus(1)),0)
& ? [X6: $int,X7: $int] :
( ~ $less(X6,0)
& ~ $less(X1,$product(2,X7))
& ( tb2t3(get(candidate1,int,t2tb4(X0),t2tb(X6))) = X3 )
& ? [X8: $int] :
( ( $sum(X7,1) = X8 )
& $less(X1,$product(2,X8))
& ~ $less(X1,$product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X1,t2tb4(X0)),t2tb3(X3))),0,X1))) )
& ~ $less(X6,0)
& $less(X6,X1)
& ~ $less($sum(X1,$uminus(1)),X6)
& ( num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,X1,t2tb4(X0)),t2tb3(X3))),0,X6) = X7 ) )
& ( X5 = 0 ) )
& ~ $less(X1,$product(2,X2)) ) ),
inference(rectify,[],[f140]) ).
tff(f197,plain,
( ~ $less($sum(sK5,$uminus(1)),0)
& ~ $less(0,0)
& ~ $less(sK5,1)
& $less(0,sK5)
& ~ $less(sK5,0)
& ~ $less(sK6,0)
& ~ $less($sum($sum($sum(sK5,$uminus(1)),1),$uminus(sK6)),$product(2,$sum(num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,sK5,t2tb4(sK4)),t2tb3(sK7))),0,$sum($sum(sK5,$uminus(1)),1)),$uminus(sK6))))
& ~ $less(num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,sK5,t2tb4(sK4)),t2tb3(sK7))),0,$sum($sum(sK5,$uminus(1)),1)),sK6)
& ( 0 != sK6 )
& ! [X4: candidate] :
( ( sK7 = X4 )
| ~ $less($sum($sum($sum(sK5,$uminus(1)),1),$uminus(sK6)),$product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,sK5,t2tb4(sK4)),t2tb3(X4))),0,$sum($sum(sK5,$uminus(1)),1)))) )
& ~ $less($sum(sK5,$uminus(1)),0)
& ~ $less(sK9,0)
& ~ $less(sK5,$product(2,sK10))
& ( sK7 = tb2t3(get(candidate1,int,t2tb4(sK4),t2tb(sK9))) )
& ( $sum(sK10,1) = sK11 )
& $less(sK5,$product(2,sK11))
& ~ $less(sK5,$product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,sK5,t2tb4(sK4)),t2tb3(sK7))),0,sK5)))
& ~ $less(sK9,0)
& $less(sK9,sK5)
& ~ $less($sum(sK5,$uminus(1)),sK9)
& ( num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,sK5,t2tb4(sK4)),t2tb3(sK7))),0,sK9) = sK10 )
& ( 0 = sK8 )
& ~ $less(sK5,$product(2,sK6)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK6),skolemize(X3,sK7),skolemize(X5,sK8),skolemize(X6,sK9),skolemize(X7,sK10),skolemize(X8,sK11)],[f196]) ).
tff(f200,plain,
! [X0: ty,X1: uni,X2: ty,X3: uni] : sort(X0,get(X0,X2,X3,X1)),
inference(rectify,[],[f114]) ).
tff(f203,plain,
! [X0: lparray_candidatecm_candidaterp,X1: $int,X2: $int,X3: $int] :
( $less(X1,X3)
| $less(X3,X2)
| ~ $less(num_of(X0,X2,X1),num_of(X0,X2,X3)) ),
inference(rectify,[],[f152]) ).
tff(f214,plain,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
inference(cnf_transformation,[],[f44]) ).
tff(f222,plain,
! [X2: candidate,X0: $int,X1: array_candidate] :
( pr(tb2t1(tuple21(array(candidate1),candidate1,t2tb2(X1),t2tb3(X2))),X0)
| ( tb2t3(get1(candidate1,t2tb2(X1),X0)) != X2 ) ),
inference(cnf_transformation,[],[f170]) ).
tff(f223,plain,
! [X0: candidate] : ( tb2t3(t2tb3(X0)) = X0 ),
inference(cnf_transformation,[],[f46]) ).
tff(f226,plain,
! [X2: $int,X0: lparray_candidatecm_candidaterp,X1: $int] :
( ( 0 = num_of(X0,X2,X1) )
| $less(X2,X1) ),
inference(cnf_transformation,[],[f122]) ).
tff(f228,plain,
! [X2: lparray_candidatecm_candidaterp,X3: $int,X0: $int,X1: $int] :
( ( num_of(X2,X3,X1) = $sum(num_of(X2,X3,X0),num_of(X2,X0,X1)) )
| $less(X0,X3)
| $less(X1,X0) ),
inference(cnf_transformation,[],[f172]) ).
tff(f231,plain,
! [X2: ty,X0: $int,X1: uni] :
( ( elts(X2,mk_array(X2,X0,X1)) = X1 )
| ~ sort(map(int,X2),X1) ),
inference(cnf_transformation,[],[f175]) ).
tff(f233,plain,
! [X0: map_int_candidate] : sort(map(int,candidate1),t2tb4(X0)),
inference(cnf_transformation,[],[f63]) ).
tff(f234,plain,
! [X0: uni] :
( ( t2tb3(tb2t3(X0)) = X0 )
| ~ sort(candidate1,X0) ),
inference(cnf_transformation,[],[f121]) ).
tff(f247,plain,
! [X2: $int,X0: uni,X1: ty] : ( get(X1,int,elts(X1,X0),t2tb(X2)) = get1(X1,X0,X2) ),
inference(cnf_transformation,[],[f184]) ).
tff(f260,plain,
! [X2: $int,X3: $int,X0: lparray_candidatecm_candidaterp,X1: $int,X4: $int] :
( $less(num_of(X0,X3,X2),num_of(X0,X3,X1))
| ~ pr(X0,X4)
| $less(X2,X3)
| ~ $less(X4,X1)
| $less(X4,X2) ),
inference(cnf_transformation,[],[f192]) ).
tff(f266,plain,
~ $less(sK5,$product(2,sK6)),
inference(cnf_transformation,[],[f197]) ).
tff(f268,plain,
num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,sK5,t2tb4(sK4)),t2tb3(sK7))),0,sK9) = sK10,
inference(cnf_transformation,[],[f197]) ).
tff(f270,plain,
$less(sK9,sK5),
inference(cnf_transformation,[],[f197]) ).
tff(f271,plain,
~ $less(sK9,0),
inference(cnf_transformation,[],[f197]) ).
tff(f272,plain,
~ $less(sK5,$product(2,num_of(tb2t1(tuple21(array(candidate1),candidate1,mk_array(candidate1,sK5,t2tb4(sK4)),t2tb3(sK7))),0,sK5))),
inference(cnf_transformation,[],[f197]) ).
tff(f273,plain,
$less(sK5,$product(2,sK11)),
inference(cnf_transformation,[],[f197]) ).
tff(f274,plain,
$sum(sK10,1) = sK11,
inference(cnf_transformation,[],[f197]) ).
tff(f275,plain,
sK7 = tb2t3(get(candidate1,int,t2tb4(sK4),t2tb(sK9))),
inference(cnf_transformation,[],[f197]) ).
tff(f280,plain,
0 != sK6,
inference(cnf_transformation,[],[f197]) ).
tff(f283,plain,
~ $less(sK6,0),
inference(cnf_transformation,[],[f197]) ).
tff(f284,plain,
~ $less(sK5,0),
inference(cnf_transformation,[],[f197]) ).
tff(f295,plain,
! [X2: ty,X3: uni,X0: ty,X1: uni] : sort(X0,get(X0,X2,X3,X1)),
inference(cnf_transformation,[],[f200]) ).
tff(f300,plain,
! [X2: $int,X3: $int,X0: lparray_candidatecm_candidaterp,X1: $int] :
( ~ $less(num_of(X0,X2,X1),num_of(X0,X2,X3))
| $less(X3,X2)
| $less(X1,X3) ),
inference(cnf_transformation,[],[f203]) ).
tff(f308,plain,
! [X0: $int,X1: array_candidate] : pr(tb2t1(tuple21(array(candidate1),candidate1,t2tb2(X1),t2tb3(tb2t3(get1(candidate1,t2tb2(X1),X0))))),X0),
inference(equality_resolution,[],[f222]) ).
tff(f310,definition,
sF12 = $uminus(1),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
tff(f311,plain,
$uminus(1) = sF12,
inference(reorient_equations,[],[f310]) ).
tff(f312,definition,
sF13 = $sum(sK5,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
tff(f314,definition,
sF14 = $sum(sF13,1),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f315,plain,
$sum(sF13,1) = sF14,
inference(reorient_equations,[],[f314]) ).
tff(f320,definition,
sF17 = array(candidate1),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
tff(f321,plain,
array(candidate1) = sF17,
inference(reorient_equations,[],[f320]) ).
tff(f322,definition,
sF18 = t2tb4(sK4),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
tff(f323,plain,
t2tb4(sK4) = sF18,
inference(reorient_equations,[],[f322]) ).
tff(f324,definition,
sF19 = mk_array(candidate1,sK5,sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
tff(f325,definition,
sF20 = t2tb3(sK7),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f326,definition,
sF21 = tuple21(sF17,candidate1,sF19,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f327,plain,
tuple21(sF17,candidate1,sF19,sF20) = sF21,
inference(reorient_equations,[],[f326]) ).
tff(f328,definition,
sF22 = tb2t1(sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f329,plain,
tb2t1(sF21) = sF22,
inference(reorient_equations,[],[f328]) ).
tff(f330,definition,
sF23 = num_of(sF22,0,sF14),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f341,definition,
sF27 = t2tb(sK9),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f342,definition,
sF28 = get(candidate1,int,sF18,sF27),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
tff(f343,plain,
get(candidate1,int,sF18,sF27) = sF28,
inference(reorient_equations,[],[f342]) ).
tff(f344,definition,
sF29 = tb2t3(sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
tff(f345,plain,
sK7 = sF29,
inference(definition_folding,[],[f275,f344,f343,f341,f323]) ).
tff(f346,definition,
sF30 = $sum(sK10,1),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
tff(f347,plain,
sF30 = sK11,
inference(definition_folding,[],[f274,f346]) ).
tff(f348,definition,
sF31 = $product(2,sK11),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
tff(f349,plain,
$less(sK5,sF31),
inference(definition_folding,[],[f273,f348]) ).
tff(f350,definition,
sF32 = num_of(sF22,0,sK5),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
tff(f351,definition,
sF33 = $product(2,sF32),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
tff(f352,plain,
$product(2,sF32) = sF33,
inference(reorient_equations,[],[f351]) ).
tff(f353,plain,
~ $less(sK5,sF33),
inference(definition_folding,[],[f272,f352,f350,f329,f327,f325,f324,f323,f321]) ).
tff(f355,definition,
sF34 = num_of(sF22,0,sK9),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
tff(f356,plain,
num_of(sF22,0,sK9) = sF34,
inference(reorient_equations,[],[f355]) ).
tff(f357,plain,
sK10 = sF34,
inference(definition_folding,[],[f268,f356,f329,f327,f325,f324,f323,f321]) ).
tff(f358,definition,
sF35 = $product(2,sK6),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
tff(f359,plain,
~ $less(sK5,sF35),
inference(definition_folding,[],[f266,f358]) ).
tff(f360,plain,
-1 = sF12,
inference(evaluation,[],[f311]) ).
tff(f374,definition,
( spl36_3
<=> ( sK7 = sF29 ) ),
introduced(definition,[new_symbols(definition,[spl36_3])],[avatar_definition]) ).
tff(f376,plain,
( ( sK7 = sF29 )
| ~ spl36_3 ),
inference(avatar_component_clause,[],[f374]) ).
tff(f377,plain,
spl36_3,
inference(avatar_split_clause,[],[f345,f374]) ).
tff(f379,definition,
( spl36_4
<=> ( sF29 = tb2t3(sF28) ) ),
introduced(definition,[new_symbols(definition,[spl36_4])],[avatar_definition]) ).
tff(f381,plain,
( ( sF29 = tb2t3(sF28) )
| ~ spl36_4 ),
inference(avatar_component_clause,[],[f379]) ).
tff(f382,plain,
spl36_4,
inference(avatar_split_clause,[],[f344,f379]) ).
tff(f384,definition,
( spl36_5
<=> ( sF30 = sK11 ) ),
introduced(definition,[new_symbols(definition,[spl36_5])],[avatar_definition]) ).
tff(f386,plain,
( ( sF30 = sK11 )
| ~ spl36_5 ),
inference(avatar_component_clause,[],[f384]) ).
tff(f387,plain,
spl36_5,
inference(avatar_split_clause,[],[f347,f384]) ).
tff(f389,definition,
( spl36_6
<=> ( sF31 = $product(2,sK11) ) ),
introduced(definition,[new_symbols(definition,[spl36_6])],[avatar_definition]) ).
tff(f391,plain,
( ( sF31 = $product(2,sK11) )
| ~ spl36_6 ),
inference(avatar_component_clause,[],[f389]) ).
tff(f392,plain,
spl36_6,
inference(avatar_split_clause,[],[f348,f389]) ).
tff(f399,definition,
( spl36_8
<=> ( sF20 = t2tb3(sK7) ) ),
introduced(definition,[new_symbols(definition,[spl36_8])],[avatar_definition]) ).
tff(f401,plain,
( ( sF20 = t2tb3(sK7) )
| ~ spl36_8 ),
inference(avatar_component_clause,[],[f399]) ).
tff(f402,plain,
spl36_8,
inference(avatar_split_clause,[],[f325,f399]) ).
tff(f409,definition,
( spl36_10
<=> $less(sK5,0) ),
introduced(definition,[new_symbols(definition,[spl36_10])],[avatar_definition]) ).
tff(f411,plain,
( ~ $less(sK5,0)
| spl36_10 ),
inference(avatar_component_clause,[],[f409]) ).
tff(f412,plain,
~ spl36_10,
inference(avatar_split_clause,[],[f284,f409]) ).
tff(f414,definition,
( spl36_11
<=> $less(sK5,sF35) ),
introduced(definition,[new_symbols(definition,[spl36_11])],[avatar_definition]) ).
tff(f417,plain,
~ spl36_11,
inference(avatar_split_clause,[],[f359,f414]) ).
tff(f419,definition,
( spl36_12
<=> ( sF23 = num_of(sF22,0,sF14) ) ),
introduced(definition,[new_symbols(definition,[spl36_12])],[avatar_definition]) ).
tff(f421,plain,
( ( sF23 = num_of(sF22,0,sF14) )
| ~ spl36_12 ),
inference(avatar_component_clause,[],[f419]) ).
tff(f422,plain,
spl36_12,
inference(avatar_split_clause,[],[f330,f419]) ).
tff(f429,definition,
( spl36_14
<=> ( sF32 = num_of(sF22,0,sK5) ) ),
introduced(definition,[new_symbols(definition,[spl36_14])],[avatar_definition]) ).
tff(f431,plain,
( ( sF32 = num_of(sF22,0,sK5) )
| ~ spl36_14 ),
inference(avatar_component_clause,[],[f429]) ).
tff(f432,plain,
spl36_14,
inference(avatar_split_clause,[],[f350,f429]) ).
tff(f439,definition,
( spl36_16
<=> $less(sK6,0) ),
introduced(definition,[new_symbols(definition,[spl36_16])],[avatar_definition]) ).
tff(f442,plain,
~ spl36_16,
inference(avatar_split_clause,[],[f283,f439]) ).
tff(f444,definition,
( spl36_17
<=> ( 0 = sK6 ) ),
introduced(definition,[new_symbols(definition,[spl36_17])],[avatar_definition]) ).
tff(f447,plain,
~ spl36_17,
inference(avatar_split_clause,[],[f280,f444]) ).
tff(f449,definition,
( spl36_18
<=> ( -1 = sF12 ) ),
introduced(definition,[new_symbols(definition,[spl36_18])],[avatar_definition]) ).
tff(f452,plain,
spl36_18,
inference(avatar_split_clause,[],[f360,f449]) ).
tff(f454,definition,
( spl36_19
<=> ( get(candidate1,int,sF18,sF27) = sF28 ) ),
introduced(definition,[new_symbols(definition,[spl36_19])],[avatar_definition]) ).
tff(f456,plain,
( ( get(candidate1,int,sF18,sF27) = sF28 )
| ~ spl36_19 ),
inference(avatar_component_clause,[],[f454]) ).
tff(f457,plain,
spl36_19,
inference(avatar_split_clause,[],[f343,f454]) ).
tff(f459,definition,
( spl36_20
<=> ( tuple21(sF17,candidate1,sF19,sF20) = sF21 ) ),
introduced(definition,[new_symbols(definition,[spl36_20])],[avatar_definition]) ).
tff(f461,plain,
( ( tuple21(sF17,candidate1,sF19,sF20) = sF21 )
| ~ spl36_20 ),
inference(avatar_component_clause,[],[f459]) ).
tff(f462,plain,
spl36_20,
inference(avatar_split_clause,[],[f327,f459]) ).
tff(f464,definition,
( spl36_21
<=> $less(sK5,sF33) ),
introduced(definition,[new_symbols(definition,[spl36_21])],[avatar_definition]) ).
tff(f467,plain,
~ spl36_21,
inference(avatar_split_clause,[],[f353,f464]) ).
tff(f469,definition,
( spl36_22
<=> ( tb2t1(sF21) = sF22 ) ),
introduced(definition,[new_symbols(definition,[spl36_22])],[avatar_definition]) ).
tff(f471,plain,
( ( tb2t1(sF21) = sF22 )
| ~ spl36_22 ),
inference(avatar_component_clause,[],[f469]) ).
tff(f472,plain,
spl36_22,
inference(avatar_split_clause,[],[f329,f469]) ).
tff(f479,definition,
( spl36_24
<=> ( $product(2,sF32) = sF33 ) ),
introduced(definition,[new_symbols(definition,[spl36_24])],[avatar_definition]) ).
tff(f482,plain,
spl36_24,
inference(avatar_split_clause,[],[f352,f479]) ).
tff(f489,definition,
( spl36_26
<=> ( sF19 = mk_array(candidate1,sK5,sF18) ) ),
introduced(definition,[new_symbols(definition,[spl36_26])],[avatar_definition]) ).
tff(f491,plain,
( ( sF19 = mk_array(candidate1,sK5,sF18) )
| ~ spl36_26 ),
inference(avatar_component_clause,[],[f489]) ).
tff(f492,plain,
spl36_26,
inference(avatar_split_clause,[],[f324,f489]) ).
tff(f494,definition,
( spl36_27
<=> ( array(candidate1) = sF17 ) ),
introduced(definition,[new_symbols(definition,[spl36_27])],[avatar_definition]) ).
tff(f496,plain,
( ( array(candidate1) = sF17 )
| ~ spl36_27 ),
inference(avatar_component_clause,[],[f494]) ).
tff(f497,plain,
spl36_27,
inference(avatar_split_clause,[],[f321,f494]) ).
tff(f499,definition,
( spl36_28
<=> ( $sum(sF13,1) = sF14 ) ),
introduced(definition,[new_symbols(definition,[spl36_28])],[avatar_definition]) ).
tff(f502,plain,
spl36_28,
inference(avatar_split_clause,[],[f315,f499]) ).
tff(f504,definition,
( spl36_29
<=> $less(sK9,0) ),
introduced(definition,[new_symbols(definition,[spl36_29])],[avatar_definition]) ).
tff(f506,plain,
( ~ $less(sK9,0)
| spl36_29 ),
inference(avatar_component_clause,[],[f504]) ).
tff(f507,plain,
~ spl36_29,
inference(avatar_split_clause,[],[f271,f504]) ).
tff(f509,definition,
( spl36_30
<=> ( sF30 = $sum(sK10,1) ) ),
introduced(definition,[new_symbols(definition,[spl36_30])],[avatar_definition]) ).
tff(f512,plain,
spl36_30,
inference(avatar_split_clause,[],[f346,f509]) ).
tff(f514,definition,
( spl36_31
<=> ( sK10 = sF34 ) ),
introduced(definition,[new_symbols(definition,[spl36_31])],[avatar_definition]) ).
tff(f516,plain,
( ( sK10 = sF34 )
| ~ spl36_31 ),
inference(avatar_component_clause,[],[f514]) ).
tff(f517,plain,
spl36_31,
inference(avatar_split_clause,[],[f357,f514]) ).
tff(f539,definition,
( spl36_36
<=> ( num_of(sF22,0,sK9) = sF34 ) ),
introduced(definition,[new_symbols(definition,[spl36_36])],[avatar_definition]) ).
tff(f541,plain,
( ( num_of(sF22,0,sK9) = sF34 )
| ~ spl36_36 ),
inference(avatar_component_clause,[],[f539]) ).
tff(f542,plain,
spl36_36,
inference(avatar_split_clause,[],[f356,f539]) ).
tff(f544,definition,
( spl36_37
<=> $less(sK9,sK5) ),
introduced(definition,[new_symbols(definition,[spl36_37])],[avatar_definition]) ).
tff(f546,plain,
( $less(sK9,sK5)
| ~ spl36_37 ),
inference(avatar_component_clause,[],[f544]) ).
tff(f547,plain,
spl36_37,
inference(avatar_split_clause,[],[f270,f544]) ).
tff(f554,definition,
( spl36_39
<=> ( sF13 = $sum(sK5,sF12) ) ),
introduced(definition,[new_symbols(definition,[spl36_39])],[avatar_definition]) ).
tff(f557,plain,
spl36_39,
inference(avatar_split_clause,[],[f312,f554]) ).
tff(f559,definition,
( spl36_40
<=> ( t2tb4(sK4) = sF18 ) ),
introduced(definition,[new_symbols(definition,[spl36_40])],[avatar_definition]) ).
tff(f561,plain,
( ( t2tb4(sK4) = sF18 )
| ~ spl36_40 ),
inference(avatar_component_clause,[],[f559]) ).
tff(f562,plain,
spl36_40,
inference(avatar_split_clause,[],[f323,f559]) ).
tff(f564,definition,
( spl36_41
<=> ( sF35 = $product(2,sK6) ) ),
introduced(definition,[new_symbols(definition,[spl36_41])],[avatar_definition]) ).
tff(f567,plain,
spl36_41,
inference(avatar_split_clause,[],[f358,f564]) ).
tff(f569,definition,
( spl36_42
<=> $less(sK5,sF31) ),
introduced(definition,[new_symbols(definition,[spl36_42])],[avatar_definition]) ).
tff(f572,plain,
spl36_42,
inference(avatar_split_clause,[],[f349,f569]) ).
tff(f574,definition,
( spl36_43
<=> ( sF27 = t2tb(sK9) ) ),
introduced(definition,[new_symbols(definition,[spl36_43])],[avatar_definition]) ).
tff(f576,plain,
( ( sF27 = t2tb(sK9) )
| ~ spl36_43 ),
inference(avatar_component_clause,[],[f574]) ).
tff(f577,plain,
spl36_43,
inference(avatar_split_clause,[],[f341,f574]) ).
tff(f599,plain,
( ( sK7 = tb2t3(sF20) )
| ~ spl36_8 ),
inference(superposition,[],[f223,f401]) ).
tff(f601,definition,
( spl36_47
<=> ( sK7 = tb2t3(sF20) ) ),
introduced(definition,[new_symbols(definition,[spl36_47])],[avatar_definition]) ).
tff(f603,plain,
( ( sK7 = tb2t3(sF20) )
| ~ spl36_47 ),
inference(avatar_component_clause,[],[f601]) ).
tff(f604,plain,
( spl36_47
| ~ spl36_8 ),
inference(avatar_split_clause,[],[f599,f399,f601]) ).
tff(f630,plain,
( ( sF31 = $product(2,sF30) )
| ~ spl36_5
| ~ spl36_6 ),
inference(superposition,[],[f391,f386]) ).
tff(f632,definition,
( spl36_51
<=> ( sF31 = $product(2,sF30) ) ),
introduced(definition,[new_symbols(definition,[spl36_51])],[avatar_definition]) ).
tff(f635,plain,
( spl36_51
| ~ spl36_5
| ~ spl36_6 ),
inference(avatar_split_clause,[],[f630,f389,f384,f632]) ).
tff(f638,plain,
( sort(map(int,candidate1),sF18)
| ~ spl36_40 ),
inference(superposition,[],[f233,f561]) ).
tff(f640,definition,
( spl36_52
<=> sort(map(int,candidate1),sF18) ),
introduced(definition,[new_symbols(definition,[spl36_52])],[avatar_definition]) ).
tff(f642,plain,
( sort(map(int,candidate1),sF18)
| ~ spl36_52 ),
inference(avatar_component_clause,[],[f640]) ).
tff(f643,plain,
( spl36_52
| ~ spl36_40 ),
inference(avatar_split_clause,[],[f638,f559,f640]) ).
tff(f655,plain,
( sort(candidate1,sF28)
| ~ spl36_19 ),
inference(superposition,[],[f295,f456]) ).
tff(f657,definition,
( spl36_53
<=> sort(candidate1,sF28) ),
introduced(definition,[new_symbols(definition,[spl36_53])],[avatar_definition]) ).
tff(f659,plain,
( sort(candidate1,sF28)
| ~ spl36_53 ),
inference(avatar_component_clause,[],[f657]) ).
tff(f660,plain,
( spl36_53
| ~ spl36_19 ),
inference(avatar_split_clause,[],[f655,f454,f657]) ).
tff(f667,plain,
( ( t2tb3(sF29) = sF28 )
| ~ sort(candidate1,sF28)
| ~ spl36_4 ),
inference(superposition,[],[f234,f381]) ).
tff(f670,plain,
( ( t2tb3(sF29) = sF28 )
| ~ spl36_4
| ~ spl36_53 ),
inference(forward_subsumption_resolution,[],[f667,f659]) ).
tff(f671,plain,
( ( t2tb3(sK7) = sF28 )
| ~ spl36_3
| ~ spl36_4
| ~ spl36_53 ),
inference(forward_demodulation,[],[f670,f376]) ).
tff(f672,plain,
( ( sF20 = sF28 )
| ~ spl36_3
| ~ spl36_4
| ~ spl36_8
| ~ spl36_53 ),
inference(forward_demodulation,[],[f671,f401]) ).
tff(f674,definition,
( spl36_55
<=> ( sF20 = sF28 ) ),
introduced(definition,[new_symbols(definition,[spl36_55])],[avatar_definition]) ).
tff(f676,plain,
( ( sF20 = sF28 )
| ~ spl36_55 ),
inference(avatar_component_clause,[],[f674]) ).
tff(f677,plain,
( spl36_55
| ~ spl36_3
| ~ spl36_4
| ~ spl36_8
| ~ spl36_53 ),
inference(avatar_split_clause,[],[f672,f657,f399,f379,f374,f674]) ).
tff(f872,plain,
( ( elts(candidate1,sF19) = sF18 )
| ~ sort(map(int,candidate1),sF18)
| ~ spl36_26 ),
inference(superposition,[],[f231,f491]) ).
tff(f877,plain,
( ( elts(candidate1,sF19) = sF18 )
| ~ spl36_26
| ~ spl36_52 ),
inference(forward_subsumption_resolution,[],[f872,f642]) ).
tff(f880,definition,
( spl36_75
<=> ( elts(candidate1,sF19) = sF18 ) ),
introduced(definition,[new_symbols(definition,[spl36_75])],[avatar_definition]) ).
tff(f882,plain,
( ( elts(candidate1,sF19) = sF18 )
| ~ spl36_75 ),
inference(avatar_component_clause,[],[f880]) ).
tff(f883,plain,
( spl36_75
| ~ spl36_26
| ~ spl36_52 ),
inference(avatar_split_clause,[],[f877,f640,f489,f880]) ).
tff(f898,plain,
( ! [X0: $int] : ( get1(candidate1,sF19,X0) = get(candidate1,int,sF18,t2tb(X0)) )
| ~ spl36_75 ),
inference(superposition,[],[f247,f882]) ).
tff(f934,plain,
( ! [X0: $int] :
( $less(sF14,0)
| $less(X0,sF14)
| ~ $less(num_of(sF22,0,X0),sF23) )
| ~ spl36_12 ),
inference(superposition,[],[f300,f421]) ).
tff(f942,definition,
( spl36_80
<=> ! [X0: $int] :
( $less(X0,sF14)
| ~ $less(num_of(sF22,0,X0),sF23) ) ),
introduced(definition,[new_symbols(definition,[spl36_80])],[avatar_definition]) ).
tff(f943,plain,
( ! [X0: $int] :
( ~ $less(num_of(sF22,0,X0),sF23)
| $less(X0,sF14) )
| ~ spl36_80 ),
inference(avatar_component_clause,[],[f942]) ).
tff(f945,definition,
( spl36_81
<=> $less(sF14,0) ),
introduced(definition,[new_symbols(definition,[spl36_81])],[avatar_definition]) ).
tff(f948,plain,
( spl36_80
| spl36_81
| ~ spl36_12 ),
inference(avatar_split_clause,[],[f934,f419,f945,f942]) ).
tff(f1029,definition,
( spl36_89
<=> $less(sF14,sK5) ),
introduced(definition,[new_symbols(definition,[spl36_89])],[avatar_definition]) ).
tff(f1101,definition,
( spl36_97
<=> $less(sK9,sK9) ),
introduced(definition,[new_symbols(definition,[spl36_97])],[avatar_definition]) ).
tff(f1106,plain,
! [X0: uni,X1: $int] : pr(tb2t1(tuple21(array(candidate1),candidate1,X0,t2tb3(tb2t3(get1(candidate1,X0,X1))))),X1),
inference(superposition,[],[f308,f214]) ).
tff(f1109,plain,
( ! [X0: uni,X1: $int] : pr(tb2t1(tuple21(sF17,candidate1,X0,t2tb3(tb2t3(get1(candidate1,X0,X1))))),X1)
| ~ spl36_27 ),
inference(forward_demodulation,[],[f1106,f496]) ).
tff(f1137,plain,
( ~ $less(sF32,sF23)
| $less(sK5,sF14)
| ~ spl36_14
| ~ spl36_80 ),
inference(superposition,[],[f943,f431]) ).
tff(f1142,definition,
( spl36_98
<=> $less(sF32,sF23) ),
introduced(definition,[new_symbols(definition,[spl36_98])],[avatar_definition]) ).
tff(f1146,definition,
( spl36_99
<=> $less(sK5,sF14) ),
introduced(definition,[new_symbols(definition,[spl36_99])],[avatar_definition]) ).
tff(f1149,plain,
( ~ spl36_98
| spl36_99
| ~ spl36_14
| ~ spl36_80 ),
inference(avatar_split_clause,[],[f1137,f942,f429,f1146,f1142]) ).
tff(f1173,definition,
( spl36_105
<=> $less(sK10,sF23) ),
introduced(definition,[new_symbols(definition,[spl36_105])],[avatar_definition]) ).
tff(f1175,plain,
( ~ $less(sK10,sF23)
| spl36_105 ),
inference(avatar_component_clause,[],[f1173]) ).
tff(f1455,plain,
( ( get1(candidate1,sF19,sK9) = get(candidate1,int,sF18,sF27) )
| ~ spl36_43
| ~ spl36_75 ),
inference(superposition,[],[f898,f576]) ).
tff(f1458,plain,
( ( get1(candidate1,sF19,sK9) = sF28 )
| ~ spl36_19
| ~ spl36_43
| ~ spl36_75 ),
inference(forward_demodulation,[],[f1455,f456]) ).
tff(f1459,plain,
( ( sF20 = get1(candidate1,sF19,sK9) )
| ~ spl36_19
| ~ spl36_43
| ~ spl36_55
| ~ spl36_75 ),
inference(forward_demodulation,[],[f1458,f676]) ).
tff(f1461,definition,
( spl36_123
<=> ( sF20 = get1(candidate1,sF19,sK9) ) ),
introduced(definition,[new_symbols(definition,[spl36_123])],[avatar_definition]) ).
tff(f1463,plain,
( ( sF20 = get1(candidate1,sF19,sK9) )
| ~ spl36_123 ),
inference(avatar_component_clause,[],[f1461]) ).
tff(f1464,plain,
( spl36_123
| ~ spl36_19
| ~ spl36_43
| ~ spl36_55
| ~ spl36_75 ),
inference(avatar_split_clause,[],[f1459,f880,f674,f574,f454,f1461]) ).
tff(f1486,plain,
( ! [X0: $int] :
( ( num_of(sF22,0,X0) = $sum(sF32,num_of(sF22,sK5,X0)) )
| $less(X0,sK5)
| $less(sK5,0) )
| ~ spl36_14 ),
inference(superposition,[],[f228,f431]) ).
tff(f1496,plain,
( ! [X0: $int] :
( $less(sK5,0)
| ( $sum(num_of(sF22,X0,0),sF32) = num_of(sF22,X0,sK5) )
| $less(0,X0) )
| ~ spl36_14 ),
inference(superposition,[],[f228,f431]) ).
tff(f1513,plain,
( ! [X0: $int] :
( ( $sum(num_of(sF22,X0,0),sF32) = num_of(sF22,X0,sK5) )
| $less(0,X0) )
| spl36_10
| ~ spl36_14 ),
inference(forward_subsumption_resolution,[],[f1496,f411]) ).
tff(f1514,plain,
( ! [X0: $int] :
( ( num_of(sF22,0,X0) = $sum(sF32,num_of(sF22,sK5,X0)) )
| $less(X0,sK5) )
| spl36_10
| ~ spl36_14 ),
inference(forward_subsumption_resolution,[],[f1486,f411]) ).
tff(f1603,plain,
( ! [X0: $int,X1: $int] :
( ~ $less(X1,X0)
| $less(X1,sK9)
| $less(sK9,0)
| $less(sF34,num_of(sF22,0,X0))
| ~ pr(sF22,X1) )
| ~ spl36_36 ),
inference(superposition,[],[f260,f541]) ).
tff(f1626,plain,
( ! [X0: $int,X1: $int] :
( $less(X1,sK9)
| ~ pr(sF22,X1)
| ~ $less(X1,X0)
| $less(sF34,num_of(sF22,0,X0)) )
| spl36_29
| ~ spl36_36 ),
inference(forward_subsumption_resolution,[],[f1603,f506]) ).
tff(f1633,plain,
( ! [X0: $int,X1: $int] :
( $less(sK10,num_of(sF22,0,X0))
| ~ pr(sF22,X1)
| $less(X1,sK9)
| ~ $less(X1,X0) )
| spl36_29
| ~ spl36_31
| ~ spl36_36 ),
inference(forward_demodulation,[],[f1626,f516]) ).
tff(f2243,plain,
( pr(tb2t1(tuple21(sF17,candidate1,sF19,t2tb3(tb2t3(sF20)))),sK9)
| ~ spl36_27
| ~ spl36_123 ),
inference(superposition,[],[f1109,f1463]) ).
tff(f2246,plain,
( pr(tb2t1(tuple21(sF17,candidate1,sF19,t2tb3(sK7))),sK9)
| ~ spl36_27
| ~ spl36_47
| ~ spl36_123 ),
inference(forward_demodulation,[],[f2243,f603]) ).
tff(f2248,plain,
( pr(tb2t1(tuple21(sF17,candidate1,sF19,sF20)),sK9)
| ~ spl36_8
| ~ spl36_27
| ~ spl36_47
| ~ spl36_123 ),
inference(forward_demodulation,[],[f2246,f401]) ).
tff(f2249,plain,
( pr(tb2t1(sF21),sK9)
| ~ spl36_8
| ~ spl36_20
| ~ spl36_27
| ~ spl36_47
| ~ spl36_123 ),
inference(forward_demodulation,[],[f2248,f461]) ).
tff(f2250,plain,
( pr(sF22,sK9)
| ~ spl36_8
| ~ spl36_20
| ~ spl36_22
| ~ spl36_27
| ~ spl36_47
| ~ spl36_123 ),
inference(forward_demodulation,[],[f2249,f471]) ).
tff(f2252,definition,
( spl36_164
<=> pr(sF22,sK9) ),
introduced(definition,[new_symbols(definition,[spl36_164])],[avatar_definition]) ).
tff(f2254,plain,
( pr(sF22,sK9)
| ~ spl36_164 ),
inference(avatar_component_clause,[],[f2252]) ).
tff(f2255,plain,
( spl36_164
| ~ spl36_8
| ~ spl36_20
| ~ spl36_22
| ~ spl36_27
| ~ spl36_47
| ~ spl36_123 ),
inference(avatar_split_clause,[],[f2250,f1461,f601,f494,f469,f459,f399,f2252]) ).
tff(f2261,plain,
( ! [X0: $int] :
( $less(0,X0)
| $less(X0,0)
| ( $sum(0,sF32) = num_of(sF22,X0,sK5) ) )
| spl36_10
| ~ spl36_14 ),
inference(superposition,[],[f1513,f226]) ).
tff(f2264,plain,
( ! [X0: $int] :
( ( sF32 = num_of(sF22,X0,sK5) )
| $less(0,X0)
| $less(X0,0) )
| spl36_10
| ~ spl36_14 ),
inference(evaluation,[],[f2261]) ).
tff(f2337,plain,
( ! [X0: $int] :
( $less(X0,sK5)
| $less(sK5,X0)
| ( num_of(sF22,0,X0) = $sum(sF32,0) ) )
| spl36_10
| ~ spl36_14 ),
inference(superposition,[],[f1514,f226]) ).
tff(f2342,plain,
( ! [X0: $int] :
( ( num_of(sF22,0,X0) = sF32 )
| $less(sK5,X0)
| $less(X0,sK5) )
| spl36_10
| ~ spl36_14 ),
inference(evaluation,[],[f2337]) ).
tff(f2370,plain,
( $less(sF14,sK5)
| ( sF23 = sF32 )
| $less(sK5,sF14)
| spl36_10
| ~ spl36_12
| ~ spl36_14 ),
inference(superposition,[],[f421,f2342]) ).
tff(f2415,definition,
( spl36_170
<=> ( sF23 = sF32 ) ),
introduced(definition,[new_symbols(definition,[spl36_170])],[avatar_definition]) ).
tff(f2417,plain,
( ( sF23 = sF32 )
| ~ spl36_170 ),
inference(avatar_component_clause,[],[f2415]) ).
tff(f2428,plain,
( spl36_170
| spl36_89
| spl36_99
| spl36_10
| ~ spl36_12
| ~ spl36_14 ),
inference(avatar_split_clause,[],[f2370,f429,f419,f409,f1146,f1029,f2415]) ).
tff(f2879,plain,
( ! [X0: $int] :
( $less(sK10,sF32)
| $less(X0,sK9)
| ~ $less(X0,sK5)
| $less(0,0)
| ~ pr(sF22,X0)
| $less(0,0) )
| spl36_10
| ~ spl36_14
| spl36_29
| ~ spl36_31
| ~ spl36_36 ),
inference(superposition,[],[f1633,f2264]) ).
tff(f2885,plain,
( ! [X0: $int] :
( $less(sK10,sF32)
| ~ pr(sF22,X0)
| $less(X0,sK9)
| ~ $less(X0,sK5)
| $less(0,0) )
| spl36_10
| ~ spl36_14
| spl36_29
| ~ spl36_31
| ~ spl36_36 ),
inference(duplicate_literal_removal,[],[f2879]) ).
tff(f2886,plain,
( ! [X0: $int] :
( $less(X0,sK9)
| $less(sK10,sF32)
| ~ pr(sF22,X0)
| ~ $less(X0,sK5) )
| spl36_10
| ~ spl36_14
| spl36_29
| ~ spl36_31
| ~ spl36_36 ),
inference(evaluation,[],[f2885]) ).
tff(f2889,plain,
( ! [X0: $int] :
( ~ $less(X0,sK5)
| $less(sK10,sF23)
| $less(X0,sK9)
| ~ pr(sF22,X0) )
| spl36_10
| ~ spl36_14
| spl36_29
| ~ spl36_31
| ~ spl36_36
| ~ spl36_170 ),
inference(forward_demodulation,[],[f2886,f2417]) ).
tff(f2895,plain,
( ! [X0: $int] :
( ~ $less(X0,sK5)
| $less(X0,sK9)
| ~ pr(sF22,X0) )
| spl36_10
| ~ spl36_14
| spl36_29
| ~ spl36_31
| ~ spl36_36
| spl36_105
| ~ spl36_170 ),
inference(forward_subsumption_resolution,[],[f2889,f1175]) ).
tff(f2942,plain,
( ~ pr(sF22,sK9)
| $less(sK9,sK9)
| spl36_10
| ~ spl36_14
| spl36_29
| ~ spl36_31
| ~ spl36_36
| ~ spl36_37
| spl36_105
| ~ spl36_170 ),
inference(resolution,[],[f2895,f546]) ).
tff(f2948,plain,
( $less(sK9,sK9)
| spl36_10
| ~ spl36_14
| spl36_29
| ~ spl36_31
| ~ spl36_36
| ~ spl36_37
| spl36_105
| ~ spl36_164
| ~ spl36_170 ),
inference(forward_subsumption_resolution,[],[f2942,f2254]) ).
tff(f2950,plain,
( spl36_97
| spl36_10
| ~ spl36_14
| spl36_29
| ~ spl36_31
| ~ spl36_36
| ~ spl36_37
| spl36_105
| ~ spl36_164
| ~ spl36_170 ),
inference(avatar_split_clause,[],[f2948,f2415,f2252,f1173,f544,f539,f514,f504,f429,f409,f1101]) ).
tff(f2952,plain,
$false,
inference(avatar_smt_refutation,[],[f2950,f2428,f2255,f1464,f1149,f948,f883,f677,f660,f643,f635,f604,f577,f572,f567,f562,f557,f547,f542,f517,f512,f507,f502,f497,f492,f482,f472,f467,f462,f457,f452,f447,f442,f432,f422,f417,f412,f402,f392,f387,f382,f377]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW630_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n015.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 14:26:32 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running first-order theorem proving
% 0.09/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.57/1.30 % (2662820)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.57/1.30 % (2662850)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1951027404:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.57/1.30 % (2662850)Instruction limit reached!
% 3.57/1.30 % (2662850)------------------------------
% 3.57/1.30 % (2662850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.57/1.30 % (2662850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.57/1.30 % (2662850)CaDiCaL version: 2.1.3
% 3.57/1.30 % (2662850)Termination reason: Instruction limit
% 3.57/1.30 % (2662850)Termination phase: Saturation
% 3.57/1.30 % (2662850)Time elapsed: 0.003 s
% 3.57/1.30 % (2662850)Peak memory usage: 88 MB
% 3.57/1.30 % (2662850)Instructions burned: 8 (million)
% 3.57/1.30 % (2662847)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=696266892:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.57/1.30 % (2662849)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=976887920:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.57/1.30 % (2662848)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1839609937:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.57/1.30 % (2662852)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1557190529:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.57/1.30 % (2662851)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2230088069:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.57/1.30 % (2662851)Instruction limit reached!
% 3.57/1.30 % (2662851)------------------------------
% 3.57/1.30 % (2662851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.57/1.30 % (2662851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.57/1.30 % (2662851)CaDiCaL version: 2.1.3
% 3.57/1.30 % (2662851)Termination reason: Instruction limit
% 3.57/1.30 % (2662851)Termination phase: Function definition elimination
% 3.57/1.30 % (2662851)Time elapsed: 0.003 s
% 3.57/1.30 % (2662851)Peak memory usage: 86 MB
% 3.57/1.30 % (2662851)Instructions burned: 5 (million)
% 3.57/1.30 % (2662847)Instruction limit reached!
% 3.57/1.30 % (2662847)------------------------------
% 3.57/1.30 % (2662847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.57/1.30 % (2662847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.57/1.30 % (2662847)CaDiCaL version: 2.1.3
% 3.57/1.30 % (2662847)Termination reason: Instruction limit
% 3.57/1.30 % (2662847)Termination phase: Saturation
% 3.57/1.30 % (2662847)Time elapsed: 0.028 s
% 3.57/1.30 % (2662847)Peak memory usage: 111 MB
% 3.57/1.30 % (2662847)Instructions burned: 12 (million)
% 3.57/1.30 % (2662853)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1174314083:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.57/1.30 % (2662852)Instruction limit reached!
% 3.57/1.30 % (2662852)------------------------------
% 3.57/1.30 % (2662852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.57/1.30 % (2662852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.57/1.30 % (2662852)CaDiCaL version: 2.1.3
% 3.57/1.30 % (2662852)Termination reason: Instruction limit
% 3.57/1.30 % (2662852)Termination phase: Saturation
% 3.57/1.30 % (2662852)Time elapsed: 0.054 s
% 3.57/1.30 % (2662852)Peak memory usage: 116 MB
% 3.57/1.30 % (2662852)Instructions burned: 46 (million)
% 3.57/1.30 % (2662853)Instruction limit reached!
% 3.57/1.30 % (2662853)------------------------------
% 3.57/1.30 % (2662853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.57/1.30 % (2662853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.57/1.30 % (2662853)CaDiCaL version: 2.1.3
% 3.57/1.30 % (2662853)Termination reason: Instruction limit
% 3.57/1.30 % (2662853)Termination phase: Saturation
% 3.57/1.30 % (2662853)Time elapsed: 0.045 s
% 3.57/1.30 % (2662853)Peak memory usage: 116 MB
% 3.57/1.30 % (2662853)Instructions burned: 34 (million)
% 3.57/1.30 % (2662855)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3362889805:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.57/1.30 % (2662855)Instruction limit reached!
% 3.57/1.30 % (2662855)------------------------------
% 4.73/1.48 % (2662855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.48 % (2662855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.48 % (2662855)CaDiCaL version: 2.1.3
% 4.73/1.48 % (2662855)Termination reason: Instruction limit
% 4.73/1.48 % (2662855)Termination phase: Saturation
% 4.73/1.48 % (2662855)Time elapsed: 0.008 s
% 4.73/1.48 % (2662855)Peak memory usage: 89 MB
% 4.73/1.48 % (2662855)Instructions burned: 20 (million)
% 4.73/1.48 % (2662849)Instruction limit reached!
% 4.73/1.48 % (2662849)------------------------------
% 4.73/1.48 % (2662849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.48 % (2662849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.48 % (2662849)CaDiCaL version: 2.1.3
% 4.73/1.48 % (2662849)Termination reason: Instruction limit
% 4.73/1.48 % (2662849)Termination phase: Saturation
% 4.73/1.48 % (2662849)Time elapsed: 0.163 s
% 4.73/1.48 % (2662849)Peak memory usage: 117 MB
% 4.73/1.48 % (2662849)Instructions burned: 202 (million)
% 4.73/1.48 % (2662865)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=1583979261:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.73/1.48 % (2662868)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1662790261:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.73/1.48 % (2662868)Instruction limit reached!
% 4.73/1.48 % (2662868)------------------------------
% 4.73/1.48 % (2662868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.48 % (2662868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.48 % (2662868)CaDiCaL version: 2.1.3
% 4.73/1.48 % (2662868)Termination reason: Instruction limit
% 4.73/1.48 % (2662868)Termination phase: Saturation
% 4.73/1.48 % (2662868)Time elapsed: 0.011 s
% 4.73/1.48 % (2662868)Peak memory usage: 89 MB
% 4.73/1.48 % (2662868)Instructions burned: 17 (million)
% 4.73/1.48 % (2662865)Instruction limit reached!
% 4.73/1.48 % (2662865)------------------------------
% 4.73/1.48 % (2662865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.48 % (2662865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.48 % (2662865)CaDiCaL version: 2.1.3
% 4.73/1.48 % (2662865)Termination reason: Instruction limit
% 4.73/1.48 % (2662865)Termination phase: Saturation
% 4.73/1.48 % (2662865)Time elapsed: 0.023 s
% 4.73/1.48 % (2662865)Peak memory usage: 89 MB
% 4.73/1.48 % (2662865)Instructions burned: 30 (million)
% 4.73/1.48 % (2662891)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=399032568:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.73/1.48 % (2662882)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1783142199:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.73/1.48 % (2662884)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=529716630:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.73/1.48 % (2662848)Instruction limit reached!
% 4.73/1.48 % (2662848)------------------------------
% 4.73/1.48 % (2662848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.48 % (2662848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.48 % (2662848)CaDiCaL version: 2.1.3
% 4.73/1.48 % (2662848)Termination reason: Instruction limit
% 4.73/1.48 % (2662848)Termination phase: Saturation
% 4.73/1.48 % (2662848)Time elapsed: 0.226 s
% 4.73/1.48 % (2662848)Peak memory usage: 118 MB
% 4.73/1.48 % (2662848)Instructions burned: 307 (million)
% 4.73/1.48 % (2662882)Instruction limit reached!
% 4.73/1.48 % (2662882)------------------------------
% 4.73/1.48 % (2662882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.73/1.48 % (2662882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.73/1.48 % (2662882)CaDiCaL version: 2.1.3
% 4.73/1.48 % (2662882)Termination reason: Instruction limit
% 4.73/1.48 % (2662882)Termination phase: Saturation
% 4.73/1.48 % (2662882)Time elapsed: 0.016 s
% 4.73/1.48 % (2662882)Peak memory usage: 89 MB
% 4.73/1.48 % (2662882)Instructions burned: 25 (million)
% 4.73/1.48 % (2662884)Instruction limit reached!
% 4.73/1.48 % (2662884)------------------------------
% 4.73/1.48 % (2662884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.65 % (2662884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.65 % (2662884)CaDiCaL version: 2.1.3
% 5.84/1.65 % (2662884)Termination reason: Instruction limit
% 5.84/1.65 % (2662884)Termination phase: Saturation
% 5.84/1.65 % (2662884)Time elapsed: 0.018 s
% 5.84/1.65 % (2662884)Peak memory usage: 89 MB
% 5.84/1.65 % (2662884)Instructions burned: 28 (million)
% 5.84/1.65 % (2662891)Instruction limit reached!
% 5.84/1.65 % (2662891)------------------------------
% 5.84/1.65 % (2662891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.65 % (2662891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.65 % (2662891)CaDiCaL version: 2.1.3
% 5.84/1.65 % (2662891)Termination reason: Instruction limit
% 5.84/1.65 % (2662891)Termination phase: Saturation
% 5.84/1.65 % (2662891)Time elapsed: 0.026 s
% 5.84/1.65 % (2662891)Peak memory usage: 89 MB
% 5.84/1.65 % (2662891)Instructions burned: 89 (million)
% 5.84/1.65 % (2662907)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=549184942:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.84/1.65 % (2662907)Instruction limit reached!
% 5.84/1.65 % (2662907)------------------------------
% 5.84/1.65 % (2662907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.65 % (2662907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.65 % (2662907)CaDiCaL version: 2.1.3
% 5.84/1.65 % (2662907)Termination reason: Instruction limit
% 5.84/1.65 % (2662907)Termination phase: Naming
% 5.84/1.65 % (2662907)Time elapsed: 0.002 s
% 5.84/1.65 % (2662907)Peak memory usage: 86 MB
% 5.84/1.65 % (2662907)Instructions burned: 2 (million)
% 5.84/1.65 % (2662910)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3399895818:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.84/1.65 % (2662911)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2059627811:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.84/1.65 % (2662911)Instruction limit reached!
% 5.84/1.65 % (2662911)------------------------------
% 5.84/1.65 % (2662911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.65 % (2662911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.65 % (2662911)CaDiCaL version: 2.1.3
% 5.84/1.65 % (2662911)Termination reason: Instruction limit
% 5.84/1.65 % (2662911)Termination phase: Inequality splitting
% 5.84/1.65 % (2662911)Time elapsed: 0.003 s
% 5.84/1.65 % (2662911)Peak memory usage: 86 MB
% 5.84/1.65 % (2662911)Instructions burned: 5 (million)
% 5.84/1.65 % (2662918)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=120237104:st=3:i=2:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/2Mi)
% 5.84/1.65 % (2662918)Instruction limit reached!
% 5.84/1.65 % (2662918)------------------------------
% 5.84/1.65 % (2662918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.65 % (2662918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.65 % (2662918)CaDiCaL version: 2.1.3
% 5.84/1.65 % (2662918)Termination reason: Instruction limit
% 5.84/1.65 % (2662918)Termination phase: Preprocessing 3
% 5.84/1.66 % (2662918)Time elapsed: 0.001 s
% 5.84/1.66 % (2662918)Peak memory usage: 86 MB
% 5.84/1.66 % (2662918)Instructions burned: 2 (million)
% 5.84/1.66 % (2662915)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1985749050:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.84/1.66 % (2662917)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=2415966758:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 5.84/1.66 % (2662916)lrs+10_1_thi=all:si=on:fd=off:random_seed=3993044101:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.84/1.66 % (2662917)Instruction limit reached!
% 5.84/1.66 % (2662917)------------------------------
% 5.84/1.66 % (2662917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.84/1.66 % (2662917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.84/1.66 % (2662917)CaDiCaL version: 2.1.3
% 5.84/1.66 % (2662917)Termination reason: Instruction limit
% 7.45/1.90 % (2662917)Termination phase: Saturation
% 7.45/1.90 % (2662917)Time elapsed: 0.005 s
% 7.45/1.90 % (2662917)Peak memory usage: 86 MB
% 7.45/1.90 % (2662917)Instructions burned: 9 (million)
% 7.45/1.90 % (2662915)Instruction limit reached!
% 7.45/1.90 % (2662915)------------------------------
% 7.45/1.90 % (2662915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.90 % (2662915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.90 % (2662915)CaDiCaL version: 2.1.3
% 7.45/1.90 % (2662915)Termination reason: Instruction limit
% 7.45/1.90 % (2662915)Termination phase: Saturation
% 7.45/1.90 % (2662915)Time elapsed: 0.093 s
% 7.45/1.90 % (2662915)Peak memory usage: 134 MB
% 7.45/1.90 % (2662915)Instructions burned: 67 (million)
% 7.45/1.90 % (2662916)Instruction limit reached!
% 7.45/1.90 % (2662916)------------------------------
% 7.45/1.90 % (2662916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.90 % (2662916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.90 % (2662916)CaDiCaL version: 2.1.3
% 7.45/1.90 % (2662916)Termination reason: Instruction limit
% 7.45/1.90 % (2662916)Termination phase: Saturation
% 7.45/1.90 % (2662916)Time elapsed: 0.061 s
% 7.45/1.90 % (2662916)Peak memory usage: 116 MB
% 7.45/1.90 % (2662916)Instructions burned: 54 (million)
% 7.45/1.90 % (2662926)dis+10_1_si=on:random_seed=2102489032:i=10:ep=R:rtra=on_2995 on theBenchmark for (2995ds/10Mi)
% 7.45/1.90 % (2662920)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=4073885797:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 7.45/1.90 % (2662926)Instruction limit reached!
% 7.45/1.90 % (2662926)------------------------------
% 7.45/1.90 % (2662926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.90 % (2662926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.90 % (2662926)CaDiCaL version: 2.1.3
% 7.45/1.90 % (2662926)Termination reason: Instruction limit
% 7.45/1.90 % (2662926)Termination phase: Saturation
% 7.45/1.90 % (2662926)Time elapsed: 0.004 s
% 7.45/1.90 % (2662926)Peak memory usage: 88 MB
% 7.45/1.90 % (2662926)Instructions burned: 11 (million)
% 7.45/1.90 % (2662920)Instruction limit reached!
% 7.45/1.90 % (2662920)------------------------------
% 7.45/1.90 % (2662920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.90 % (2662920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.90 % (2662920)CaDiCaL version: 2.1.3
% 7.45/1.90 % (2662920)Termination reason: Instruction limit
% 7.45/1.90 % (2662920)Termination phase: Preprocessing 2
% 7.45/1.90 % (2662920)Time elapsed: 0.002 s
% 7.45/1.90 % (2662920)Peak memory usage: 86 MB
% 7.45/1.90 % (2662920)Instructions burned: 2 (million)
% 7.45/1.90 % (2662910)Instruction limit reached!
% 7.45/1.90 % (2662910)------------------------------
% 7.45/1.90 % (2662910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.90 % (2662910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.90 % (2662910)CaDiCaL version: 2.1.3
% 7.45/1.90 % (2662910)Termination reason: Instruction limit
% 7.45/1.90 % (2662910)Termination phase: Saturation
% 7.45/1.90 % (2662910)Time elapsed: 0.133 s
% 7.45/1.90 % (2662910)Peak memory usage: 91 MB
% 7.45/1.90 % (2662910)Instructions burned: 181 (million)
% 7.45/1.90 % (2662925)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=4267276690:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 7.45/1.90 % (2662932)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3016172400:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 7.45/1.90 % (2662932)Refutation not found, incomplete strategy
% 7.45/1.90 % (2662932)------------------------------
% 7.45/1.90 % (2662932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.45/1.90 % (2662932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.90 % (2662932)CaDiCaL version: 2.1.3
% 7.45/1.90 % (2662932)Termination reason: Refutation not found, incomplete strategy
% 7.45/1.90 % (2662932)Time elapsed: 0.012 s
% 7.45/1.90 % (2662932)Peak memory usage: 89 MB
% 7.45/1.90 % (2662932)Instructions burned: 18 (million)
% 7.45/1.90 % (2662953)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1628424436:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 7.45/1.90 % (2662944)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1789121212: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)
% 10.13/2.16 % (2662925)Instruction limit reached!
% 10.13/2.16 % (2662925)------------------------------
% 10.13/2.16 % (2662925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.13/2.16 % (2662925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.13/2.16 % (2662925)CaDiCaL version: 2.1.3
% 10.13/2.16 % (2662925)Termination reason: Instruction limit
% 10.13/2.16 % (2662925)Termination phase: Saturation
% 10.13/2.16 % (2662925)Time elapsed: 0.108 s
% 10.13/2.16 % (2662925)Peak memory usage: 119 MB
% 10.13/2.16 % (2662925)Instructions burned: 128 (million)
% 10.13/2.16 % (2662944)Instruction limit reached!
% 10.13/2.16 % (2662944)------------------------------
% 10.13/2.16 % (2662944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.13/2.16 % (2662944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.13/2.16 % (2662944)CaDiCaL version: 2.1.3
% 10.13/2.16 % (2662944)Termination reason: Instruction limit
% 10.13/2.16 % (2662944)Termination phase: Saturation
% 10.13/2.16 % (2662944)Time elapsed: 0.028 s
% 10.13/2.16 % (2662944)Peak memory usage: 89 MB
% 10.13/2.16 % (2662944)Instructions burned: 35 (million)
% 10.13/2.16 % (2662951)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1519782519:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 10.13/2.16 % (2662949)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=973863676:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 10.13/2.16 % (2662949)Instruction limit reached!
% 10.13/2.16 % (2662949)------------------------------
% 10.13/2.16 % (2662949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.13/2.16 % (2662949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.13/2.16 % (2662949)CaDiCaL version: 2.1.3
% 10.13/2.16 % (2662949)Termination reason: Instruction limit
% 10.13/2.16 % (2662949)Termination phase: Preprocessing 3
% 10.13/2.16 % (2662949)Time elapsed: 0.002 s
% 10.13/2.16 % (2662949)Peak memory usage: 86 MB
% 10.13/2.16 % (2662949)Instructions burned: 3 (million)
% 10.13/2.16 % (2662951)Instruction limit reached!
% 10.13/2.16 % (2662951)------------------------------
% 10.13/2.16 % (2662951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.13/2.16 % (2662951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.13/2.16 % (2662951)CaDiCaL version: 2.1.3
% 10.13/2.16 % (2662951)Termination reason: Instruction limit
% 10.13/2.16 % (2662951)Termination phase: Saturation
% 10.13/2.16 % (2662951)Time elapsed: 0.006 s
% 10.13/2.16 % (2662951)Peak memory usage: 88 MB
% 10.13/2.16 % (2662951)Instructions burned: 8 (million)
% 10.13/2.16 % (2662958)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=380506789:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 10.13/2.16 % (2662958)Instruction limit reached!
% 10.13/2.16 % (2662958)------------------------------
% 10.13/2.16 % (2662958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.13/2.16 % (2662958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.13/2.16 % (2662958)CaDiCaL version: 2.1.3
% 10.13/2.16 % (2662958)Termination reason: Instruction limit
% 10.13/2.16 % (2662958)Termination phase: Saturation
% 10.13/2.16 % (2662958)Time elapsed: 0.029 s
% 10.13/2.16 % (2662958)Peak memory usage: 112 MB
% 10.13/2.16 % (2662958)Instructions burned: 13 (million)
% 10.13/2.16 % (2662953)Instruction limit reached!
% 10.13/2.16 % (2662953)------------------------------
% 10.13/2.16 % (2662953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.13/2.16 % (2662953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.13/2.16 % (2662953)CaDiCaL version: 2.1.3
% 10.13/2.16 % (2662953)Termination reason: Instruction limit
% 10.13/2.16 % (2662953)Termination phase: Saturation
% 10.13/2.16 % (2662953)Time elapsed: 0.107 s
% 10.13/2.16 % (2662953)Peak memory usage: 91 MB
% 10.13/2.16 % (2662953)Instructions burned: 373 (million)
% 10.13/2.16 % (2662992)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=3951316440:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 10.13/2.16 % (2662990)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1242840246:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 11.55/2.40 % (2662991)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3917498205:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 11.55/2.40 % (2662988)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2407516242:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 11.55/2.40 % (2662990)Instruction limit reached!
% 11.55/2.40 % (2662990)------------------------------
% 11.55/2.40 % (2662990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.55/2.40 % (2662990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.55/2.40 % (2662990)CaDiCaL version: 2.1.3
% 11.55/2.40 % (2662990)Termination reason: Instruction limit
% 11.55/2.40 % (2662990)Termination phase: Saturation
% 11.55/2.40 % (2662990)Time elapsed: 0.007 s
% 11.55/2.40 % (2662990)Peak memory usage: 88 MB
% 11.55/2.40 % (2662990)Instructions burned: 11 (million)
% 11.55/2.40 % (2663003)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=581835274:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi)
% 11.55/2.40 % (2662992)Instruction limit reached!
% 11.55/2.40 % (2662992)------------------------------
% 11.55/2.40 % (2662992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.55/2.40 % (2662992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.55/2.40 % (2662992)CaDiCaL version: 2.1.3
% 11.55/2.40 % (2662992)Termination reason: Instruction limit
% 11.55/2.40 % (2662992)Termination phase: Saturation
% 11.55/2.40 % (2662992)Time elapsed: 0.052 s
% 11.55/2.40 % (2662992)Peak memory usage: 90 MB
% 11.55/2.40 % (2662992)Instructions burned: 75 (million)
% 11.55/2.40 % (2662932)------------------------------
% 11.55/2.40 % (2662932)------------------------------
% 11.55/2.40 % (2663004)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=295410759:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi)
% 11.55/2.40 % (2662991)Instruction limit reached!
% 11.55/2.40 % (2662991)------------------------------
% 11.55/2.40 % (2662991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.55/2.40 % (2662991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.55/2.40 % (2662991)CaDiCaL version: 2.1.3
% 11.55/2.40 % (2662991)Termination reason: Instruction limit
% 11.55/2.40 % (2662991)Termination phase: Saturation
% 11.55/2.40 % (2662991)Time elapsed: 0.092 s
% 11.55/2.40 % (2662991)Peak memory usage: 133 MB
% 11.55/2.40 % (2662991)Instructions burned: 71 (million)
% 11.55/2.40 % (2662988)Instruction limit reached!
% 11.55/2.40 % (2662988)------------------------------
% 11.55/2.40 % (2662988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.55/2.40 % (2662988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.55/2.40 % (2662988)CaDiCaL version: 2.1.3
% 11.55/2.40 % (2662988)Termination reason: Instruction limit
% 11.55/2.40 % (2662988)Termination phase: Saturation
% 11.55/2.40 % (2662988)Time elapsed: 0.153 s
% 11.55/2.40 % (2662988)Peak memory usage: 118 MB
% 11.55/2.40 % (2662988)Instructions burned: 228 (million)
% 11.55/2.40 % (2663020)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=4283862503:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 11.55/2.40 % (2663023)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3417042516:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 11.55/2.40 % (2663004)Instruction limit reached!
% 11.55/2.40 % (2663004)------------------------------
% 11.55/2.40 % (2663004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.55/2.40 % (2663004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.55/2.40 % (2663004)CaDiCaL version: 2.1.3
% 11.55/2.40 % (2663004)Termination reason: Instruction limit
% 11.55/2.40 % (2663004)Termination phase: Saturation
% 11.55/2.40 % (2663004)Time elapsed: 0.113 s
% 11.55/2.40 % (2663004)Peak memory usage: 117 MB
% 11.55/2.40 % (2663004)Instructions burned: 131 (million)
% 11.55/2.40 % (2663022)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=61033250:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 11.55/2.40 % (2663025)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=69835393:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi)
% 12.57/2.74 % (2663003)Instruction limit reached!
% 12.57/2.74 % (2663003)------------------------------
% 12.57/2.74 % (2663003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.57/2.74 % (2663003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.74 % (2663003)CaDiCaL version: 2.1.3
% 12.57/2.74 % (2663003)Termination reason: Instruction limit
% 12.57/2.74 % (2663003)Termination phase: Saturation
% 12.57/2.74 % (2663003)Time elapsed: 0.214 s
% 12.57/2.74 % (2663003)Peak memory usage: 91 MB
% 12.57/2.74 % (2663003)Instructions burned: 295 (million)
% 12.57/2.74 % (2663023)Instruction limit reached!
% 12.57/2.74 % (2663023)------------------------------
% 12.57/2.74 % (2663023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.57/2.74 % (2663023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.74 % (2663023)CaDiCaL version: 2.1.3
% 12.57/2.74 % (2663023)Termination reason: Instruction limit
% 12.57/2.74 % (2663023)Termination phase: Saturation
% 12.57/2.74 % (2663023)Time elapsed: 0.101 s
% 12.57/2.74 % (2663023)Peak memory usage: 91 MB
% 12.57/2.74 % (2663023)Instructions burned: 309 (million)
% 12.57/2.74 % (2663022)Instruction limit reached!
% 12.57/2.74 % (2663022)------------------------------
% 12.57/2.74 % (2663022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.57/2.74 % (2663022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.74 % (2663022)CaDiCaL version: 2.1.3
% 12.57/2.74 % (2663022)Termination reason: Instruction limit
% 12.57/2.74 % (2663022)Termination phase: Saturation
% 12.57/2.74 % (2663022)Time elapsed: 0.069 s
% 12.57/2.74 % (2663022)Peak memory usage: 134 MB
% 12.57/2.74 % (2663022)Instructions burned: 40 (million)
% 12.57/2.74 % (2663020)Instruction limit reached!
% 12.57/2.74 % (2663020)------------------------------
% 12.57/2.74 % (2663020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.57/2.74 % (2663020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.74 % (2663020)CaDiCaL version: 2.1.3
% 12.57/2.74 % (2663020)Termination reason: Instruction limit
% 12.57/2.74 % (2663020)Termination phase: Saturation
% 12.57/2.74 % (2663020)Time elapsed: 0.141 s
% 12.57/2.74 % (2663020)Peak memory usage: 134 MB
% 12.57/2.74 % (2663020)Instructions burned: 131 (million)
% 12.57/2.74 % (2663026)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2895464142:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 12.57/2.74 % (2663029)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=3037790175:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi)
% 12.57/2.74 % (2663038)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=292002118:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi)
% 12.57/2.74 % (2663037)dis+10_1_si=on:random_seed=3315686899:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi)
% 12.57/2.74 % (2663026)Instruction limit reached!
% 12.57/2.74 % (2663026)------------------------------
% 12.57/2.74 % (2663026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.57/2.74 % (2663026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.74 % (2663026)CaDiCaL version: 2.1.3
% 12.57/2.74 % (2663026)Termination reason: Instruction limit
% 12.57/2.74 % (2663026)Termination phase: Saturation
% 12.57/2.74 % (2663026)Time elapsed: 0.101 s
% 12.57/2.74 % (2663026)Peak memory usage: 117 MB
% 12.57/2.74 % (2663026)Instructions burned: 131 (million)
% 12.57/2.74 % (2663039)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4032461585:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi)
% 12.57/2.74 % (2663045)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3107605691:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi)
% 12.57/2.74 % (2663038)Instruction limit reached!
% 12.57/2.74 % (2663038)------------------------------
% 12.57/2.74 % (2663038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.57/2.74 % (2663038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.57/2.74 % (2663038)CaDiCaL version: 2.1.3
% 16.56/3.05 % (2663038)Termination reason: Instruction limit
% 16.56/3.05 % (2663038)Termination phase: Saturation
% 16.56/3.05 % (2663038)Time elapsed: 0.114 s
% 16.56/3.05 % (2663038)Peak memory usage: 92 MB
% 16.56/3.05 % (2663038)Instructions burned: 384 (million)
% 16.56/3.05 % (2663045)Refutation not found, incomplete strategy
% 16.56/3.05 % (2663045)------------------------------
% 16.56/3.05 % (2663045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.56/3.05 % (2663045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.56/3.05 % (2663045)CaDiCaL version: 2.1.3
% 16.56/3.05 % (2663045)Termination reason: Refutation not found, incomplete strategy
% 16.56/3.05 % (2663045)Time elapsed: 0.042 s
% 16.56/3.05 % (2663045)Peak memory usage: 116 MB
% 16.56/3.05 % (2663045)Instructions burned: 27 (million)
% 16.56/3.05 % (2663039)Instruction limit reached!
% 16.56/3.05 % (2663039)------------------------------
% 16.56/3.05 % (2663039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.56/3.05 % (2663039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.56/3.05 % (2663039)CaDiCaL version: 2.1.3
% 16.56/3.05 % (2663039)Termination reason: Instruction limit
% 16.56/3.05 % (2663039)Termination phase: Saturation
% 16.56/3.05 % (2663039)Time elapsed: 0.093 s
% 16.56/3.05 % (2663039)Peak memory usage: 90 MB
% 16.56/3.05 % (2663039)Instructions burned: 142 (million)
% 16.56/3.05 % (2663029)Instruction limit reached!
% 16.56/3.05 % (2663029)------------------------------
% 16.56/3.05 % (2663029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.56/3.05 % (2663029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.56/3.05 % (2663029)CaDiCaL version: 2.1.3
% 16.56/3.05 % (2663029)Termination reason: Instruction limit
% 16.56/3.05 % (2663029)Termination phase: Saturation
% 16.56/3.05 % (2663029)Time elapsed: 0.201 s
% 16.56/3.05 % (2663029)Peak memory usage: 117 MB
% 16.56/3.05 % (2663029)Instructions burned: 259 (million)
% 16.56/3.05 % (2663081)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=54189603:i=121:nm=16:rtra=on_2986 on theBenchmark for (2986ds/121Mi)
% 16.56/3.05 % (2663090)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=2555778663:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi)
% 16.56/3.05 % (2663025)Instruction limit reached!
% 16.56/3.05 % (2663025)------------------------------
% 16.56/3.05 % (2663025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.56/3.05 % (2663025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.56/3.05 % (2663025)CaDiCaL version: 2.1.3
% 16.56/3.05 % (2663025)Termination reason: Instruction limit
% 16.56/3.05 % (2663025)Termination phase: Saturation
% 16.56/3.05 % (2663025)Time elapsed: 0.398 s
% 16.56/3.05 % (2663025)Peak memory usage: 139 MB
% 16.56/3.05 % (2663025)Instructions burned: 598 (million)
% 16.56/3.05 % (2663081)Instruction limit reached!
% 16.56/3.05 % (2663081)------------------------------
% 16.56/3.05 % (2663081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.56/3.05 % (2663081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.56/3.05 % (2663081)CaDiCaL version: 2.1.3
% 16.56/3.05 % (2663081)Termination reason: Instruction limit
% 16.56/3.05 % (2663081)Termination phase: Saturation
% 16.56/3.05 % (2663081)Time elapsed: 0.080 s
% 16.56/3.05 % (2663081)Peak memory usage: 89 MB
% 16.56/3.05 % (2663081)Instructions burned: 122 (million)
% 16.56/3.05 % (2663090)Instruction limit reached!
% 16.56/3.05 % (2663090)------------------------------
% 16.56/3.05 % (2663090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.56/3.05 % (2663090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.56/3.05 % (2663090)CaDiCaL version: 2.1.3
% 16.56/3.05 % (2663090)Termination reason: Instruction limit
% 16.56/3.05 % (2663090)Termination phase: Saturation
% 16.56/3.05 % (2663090)Time elapsed: 0.061 s
% 16.56/3.05 % (2663090)Peak memory usage: 118 MB
% 16.56/3.05 % (2663090)Instructions burned: 129 (million)
% 16.56/3.05 % (2663092)dis+1010_1_to=kbo:si=on:random_seed=478530830:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2985 on theBenchmark for (2985ds/175Mi)
% 16.56/3.05 % (2663091)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=403944829:i=39:ins=3:rtra=on_2985 on theBenchmark for (2985ds/39Mi)
% 16.56/3.05 % (2663045)------------------------------
% 16.56/3.05 % (2663045)------------------------------
% 17.61/3.35 % (2663091)Instruction limit reached!
% 17.61/3.35 % (2663091)------------------------------
% 17.61/3.35 % (2663091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/3.35 % (2663091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/3.35 % (2663091)CaDiCaL version: 2.1.3
% 17.61/3.35 % (2663091)Termination reason: Instruction limit
% 17.61/3.35 % (2663091)Termination phase: Saturation
% 17.61/3.35 % (2663091)Time elapsed: 0.051 s
% 17.61/3.35 % (2663091)Peak memory usage: 116 MB
% 17.61/3.35 % (2663091)Instructions burned: 39 (million)
% 17.61/3.35 % (2663097)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3527302327:thitd=on:i=215:nm=0:rtra=on:ev=force_2984 on theBenchmark for (2984ds/215Mi)
% 17.61/3.35 % (2663096)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=133986351:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi)
% 17.61/3.35 % (2663095)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1469836448:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/329Mi)
% 17.61/3.35 % (2663092)Instruction limit reached!
% 17.61/3.35 % (2663092)------------------------------
% 17.61/3.35 % (2663092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/3.35 % (2663092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/3.35 % (2663092)CaDiCaL version: 2.1.3
% 17.61/3.35 % (2663092)Termination reason: Instruction limit
% 17.61/3.35 % (2663092)Termination phase: Saturation
% 17.61/3.35 % (2663092)Time elapsed: 0.128 s
% 17.61/3.35 % (2663092)Peak memory usage: 91 MB
% 17.61/3.35 % (2663092)Instructions burned: 175 (million)
% 17.61/3.35 % (2663097)Instruction limit reached!
% 17.61/3.35 % (2663097)------------------------------
% 17.61/3.35 % (2663097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/3.35 % (2663097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/3.35 % (2663097)CaDiCaL version: 2.1.3
% 17.61/3.35 % (2663097)Termination reason: Instruction limit
% 17.61/3.35 % (2663097)Termination phase: Saturation
% 17.61/3.35 % (2663097)Time elapsed: 0.095 s
% 17.61/3.35 % (2663097)Peak memory usage: 136 MB
% 17.61/3.35 % (2663097)Instructions burned: 216 (million)
% 17.61/3.35 % (2663101)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=848452773:st=2:i=295:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/295Mi)
% 17.61/3.35 % (2663100)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=4257402271:i=349:rtra=on_2983 on theBenchmark for (2983ds/349Mi)
% 17.61/3.35 % (2663105)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1128600989:i=328:kws=inv_frequency:nm=20:rtra=on_2982 on theBenchmark for (2982ds/328Mi)
% 17.61/3.35 % (2663037)Instruction limit reached!
% 17.61/3.35 % (2663037)------------------------------
% 17.61/3.35 % (2663037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/3.35 % (2663037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/3.35 % (2663037)CaDiCaL version: 2.1.3
% 17.61/3.35 % (2663037)Termination reason: Instruction limit
% 17.61/3.35 % (2663037)Termination phase: Saturation
% 17.61/3.35 % (2663037)Time elapsed: 0.576 s
% 17.61/3.35 % (2663037)Peak memory usage: 94 MB
% 17.61/3.35 % (2663037)Instructions burned: 1001 (million)
% 17.61/3.35 % (2663106)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=1682539387:i=281:gtgl=2:rtra=on:gtg=all_2982 on theBenchmark for (2982ds/281Mi)
% 17.61/3.35 % (2663095)Instruction limit reached!
% 17.61/3.35 % (2663095)------------------------------
% 17.61/3.35 % (2663095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/3.35 % (2663095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.61/3.35 % (2663095)CaDiCaL version: 2.1.3
% 17.61/3.35 % (2663095)Termination reason: Instruction limit
% 17.61/3.35 % (2663095)Termination phase: Saturation
% 17.61/3.35 % (2663095)Time elapsed: 0.256 s
% 17.61/3.35 % (2663095)Peak memory usage: 118 MB
% 17.61/3.35 % (2663095)Instructions burned: 330 (million)
% 17.61/3.35 % (2663101)Instruction limit reached!
% 17.61/3.35 % (2663101)------------------------------
% 17.61/3.35 % (2663101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.61/3.35 % (2663101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.52 % (2663101)CaDiCaL version: 2.1.3
% 17.88/3.52 % (2663101)Termination reason: Instruction limit
% 17.88/3.52 % (2663101)Termination phase: Saturation
% 17.88/3.52 % (2663101)Time elapsed: 0.167 s
% 17.88/3.52 % (2663101)Peak memory usage: 90 MB
% 17.88/3.52 % (2663101)Instructions burned: 295 (million)
% 17.88/3.52 % (2663106)Instruction limit reached!
% 17.88/3.52 % (2663106)------------------------------
% 17.88/3.52 % (2663106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.52 % (2663106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.52 % (2663106)CaDiCaL version: 2.1.3
% 17.88/3.52 % (2663106)Termination reason: Instruction limit
% 17.88/3.52 % (2663106)Termination phase: Saturation
% 17.88/3.52 % (2663106)Time elapsed: 0.109 s
% 17.88/3.52 % (2663106)Peak memory usage: 117 MB
% 17.88/3.52 % (2663106)Instructions burned: 281 (million)
% 17.88/3.52 % (2663100)Instruction limit reached!
% 17.88/3.52 % (2663100)------------------------------
% 17.88/3.52 % (2663100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.52 % (2663100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.52 % (2663100)CaDiCaL version: 2.1.3
% 17.88/3.52 % (2663100)Termination reason: Instruction limit
% 17.88/3.52 % (2663100)Termination phase: Saturation
% 17.88/3.52 % (2663100)Time elapsed: 0.225 s
% 17.88/3.52 % (2663100)Peak memory usage: 117 MB
% 17.88/3.52 % (2663100)Instructions burned: 350 (million)
% 17.88/3.52 % (2663110)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=2088466264:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/484Mi)
% 17.88/3.52 % (2663096)Instruction limit reached!
% 17.88/3.52 % (2663096)------------------------------
% 17.88/3.52 % (2663096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.52 % (2663096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.52 % (2663096)CaDiCaL version: 2.1.3
% 17.88/3.52 % (2663096)Termination reason: Instruction limit
% 17.88/3.52 % (2663096)Termination phase: Saturation
% 17.88/3.52 % (2663096)Time elapsed: 0.372 s
% 17.88/3.52 % (2663096)Peak memory usage: 136 MB
% 17.88/3.52 % (2663096)Instructions burned: 484 (million)
% 17.88/3.52 % (2663112)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=1873672201:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2980 on theBenchmark for (2980ds/321Mi)
% 17.88/3.52 % (2663105)Instruction limit reached!
% 17.88/3.52 % (2663105)------------------------------
% 17.88/3.52 % (2663105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.52 % (2663105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.52 % (2663105)CaDiCaL version: 2.1.3
% 17.88/3.52 % (2663105)Termination reason: Instruction limit
% 17.88/3.52 % (2663105)Termination phase: Saturation
% 17.88/3.52 % (2663105)Time elapsed: 0.236 s
% 17.88/3.52 % (2663105)Peak memory usage: 118 MB
% 17.88/3.52 % (2663105)Instructions burned: 328 (million)
% 17.88/3.52 % (2663113)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1377351037:i=416:rtra=on:gtg=position:ss=axioms_2980 on theBenchmark for (2980ds/416Mi)
% 17.88/3.52 % (2663114)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=539725944:i=471:thf=on:kws=precedence:rtra=on_2979 on theBenchmark for (2979ds/471Mi)
% 17.88/3.52 % (2663116)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=1534708562:avsq=on:i=276:avsqr=1,2:rtra=on_2979 on theBenchmark for (2979ds/276Mi)
% 17.88/3.52 % (2663117)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=4188089064:i=375:kws=inv_arity_squared:rtra=on_2979 on theBenchmark for (2979ds/375Mi)
% 17.88/3.52 % (2663112)Instruction limit reached!
% 17.88/3.52 % (2663112)------------------------------
% 17.88/3.52 % (2663112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.52 % (2663112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.52 % (2663112)CaDiCaL version: 2.1.3
% 17.88/3.52 % (2663112)Termination reason: Instruction limit
% 17.88/3.52 % (2663112)Termination phase: Saturation
% 17.88/3.52 % (2663112)Time elapsed: 0.160 s
% 17.88/3.52 % (2663112)Peak memory usage: 114 MB
% 17.88/3.52 % (2663112)Instructions burned: 321 (million)
% 17.88/3.52 % (2663120)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=2672787668:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/387Mi)
% 17.88/3.52 % (2663114)Instruction limit reached!
% 17.88/3.52 % (2663114)------------------------------
% 17.88/3.52 % (2663114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.52 % (2663114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.52 % (2663114)CaDiCaL version: 2.1.3
% 17.88/3.52 % (2663114)Termination reason: Instruction limit
% 17.88/3.52 % (2663114)Termination phase: Saturation
% 17.88/3.52 % (2663114)Time elapsed: 0.176 s
% 17.88/3.52 % (2663114)Peak memory usage: 119 MB
% 17.88/3.52 % (2663114)Instructions burned: 472 (million)
% 17.88/3.52 % (2663110)Instruction limit reached!
% 17.88/3.52 % (2663110)------------------------------
% 17.88/3.52 % (2663110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.52 % (2663110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.52 % (2663110)CaDiCaL version: 2.1.3
% 17.88/3.52 % (2663110)Termination reason: Instruction limit
% 17.88/3.52 % (2663110)Termination phase: Saturation
% 17.88/3.52 % (2663110)Time elapsed: 0.289 s
% 17.88/3.52 % (2663110)Peak memory usage: 94 MB
% 17.88/3.52 % (2663110)Instructions burned: 484 (million)
% 17.88/3.52 % (2663113)Instruction limit reached!
% 17.88/3.52 % (2663113)------------------------------
% 17.88/3.52 % (2663113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.52 % (2663113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.52 % (2663113)CaDiCaL version: 2.1.3
% 17.88/3.52 % (2663113)Termination reason: Instruction limit
% 17.88/3.52 % (2663113)Termination phase: Saturation
% 17.88/3.52 % (2663113)Time elapsed: 0.258 s
% 17.88/3.52 % (2663113)Peak memory usage: 121 MB
% 17.88/3.52 % (2663113)Instructions burned: 417 (million)
% 17.88/3.52 % (2663116)Instruction limit reached!
% 17.88/3.52 % (2663116)------------------------------
% 17.88/3.52 % (2663116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.52 % (2663116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.52 % (2663116)CaDiCaL version: 2.1.3
% 17.88/3.52 % (2663116)Termination reason: Instruction limit
% 17.88/3.52 % (2663116)Termination phase: Saturation
% 17.88/3.52 % (2663116)Time elapsed: 0.234 s
% 17.88/3.52 % (2663116)Peak memory usage: 135 MB
% 17.88/3.52 % (2663116)Instructions burned: 276 (million)
% 17.88/3.52 % (2663124)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1897455028:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2977 on theBenchmark for (2977ds/513Mi)
% 17.88/3.52 % (2663126)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1737064415:i=334:rtra=on_2976 on theBenchmark for (2976ds/334Mi)
% 17.88/3.52 % (2663117)First to succeed.
% 17.88/3.52 % (2663117)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2662820"
% 17.88/3.52 % (2663127)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=2632042092:i=359:rtra=on:gtg=exists_top:ss=axioms_2976 on theBenchmark for (2976ds/359Mi)
% 17.88/3.52 % (2663128)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=1211864957:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2976 on theBenchmark for (2976ds/341Mi)
% 17.88/3.52 % (2663120)Instruction limit reached!
% 17.88/3.52 % (2663120)------------------------------
% 17.88/3.52 % (2663120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.52 % (2663120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.52 % (2663120)CaDiCaL version: 2.1.3
% 17.88/3.52 % (2663120)Termination reason: Instruction limit
% 17.88/3.52 % (2663120)Termination phase: Saturation
% 17.88/3.52 % (2663120)Time elapsed: 0.292 s
% 17.88/3.52 % (2663120)Peak memory usage: 119 MB
% 17.88/3.52 % (2663120)Instructions burned: 387 (million)
% 17.88/3.52 % (2663131)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1917862959:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/261Mi)
% 17.88/3.52 % (2663126)Instruction limit reached!
% 17.88/3.52 % (2663126)------------------------------
% 17.88/3.52 % (2663126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.52 % (2663126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.52 % (2663126)CaDiCaL version: 2.1.3
% 17.88/3.52 % (2663126)Termination reason: Instruction limit
% 17.88/3.52 % (2663126)Termination phase: Saturation
% 17.88/3.52 % (2663126)Time elapsed: 0.157 s
% 17.88/3.52 % (2663126)Peak memory usage: 137 MB
% 17.88/3.52 % (2663126)Instructions burned: 334 (million)
% 17.88/3.52 % (2663136)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2112399388:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2974 on theBenchmark for (2974ds/273Mi)
% 17.88/3.52 % (2663127)Instruction limit reached!
% 17.88/3.52 % (2663127)------------------------------
% 17.88/3.52 % (2663127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.88/3.52 % (2663127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.88/3.52 % (2663127)CaDiCaL version: 2.1.3
% 17.88/3.52 % (2663127)Termination reason: Instruction limit
% 17.88/3.52 % (2663127)Termination phase: Saturation
% 17.88/3.52 % (2663127)Time elapsed: 0.235 s
% 17.88/3.52 % (2663127)Peak memory usage: 92 MB
% 17.88/3.52 % (2663127)Instructions burned: 360 (million)
% 17.88/3.52 % (2663135)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=3824465586:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2974 on theBenchmark for (2974ds/235Mi)
% 17.88/3.52 % (2663117)Refutation found. Thanks to Tanya!
% 17.88/3.52 % SZS status Theorem for theBenchmark
% 17.88/3.52 % SZS output start Proof for theBenchmark
% See solution above
% 20.21/3.72 % (2663117)------------------------------
% 20.21/3.72 % (2663117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.21/3.72 % (2663117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.21/3.72 % (2663117)CaDiCaL version: 2.1.3
% 20.21/3.72 % (2663117)Termination reason: Refutation
% 20.21/3.72 % (2663117)Time elapsed: 0.248 s
% 20.21/3.72 % (2663117)Peak memory usage: 119 MB
% 20.21/3.72 % (2663117)Instructions burned: 341 (million)
% 20.21/3.72 % (2663117)------------------------------
% 20.21/3.72 % (2663117)------------------------------
% 20.21/3.72 % (2662820)Success in time 2.75 s
% 20.21/3.72 % Vampire exiting
%------------------------------------------------------------------------------