%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM996_5 : TPTP v9.3.1. Released v6.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 12:17:46 PM UTC 2026
% Result : Theorem 31.46s 5.39s
% Output : Refutation 32.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 33
% Syntax : Number of formulae : 140 ( 126 unt; 0 typ; 18 def)
% Number of atoms : 154 ( 133 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 29 ( 15 ~; 10 |; 0 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of FOOLs : 1 ( 1 fml; 0 var)
% Number of types : 5 ( 4 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 19 ( 17 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 23 con; 0-3 aty)
% Number of variables : 93 ( 93 !; 0 ?; 93 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
bool: $tType ).
tff(type_def_6,type,
int: $tType ).
tff(type_def_7,type,
nat: $tType ).
tff(type_def_8,type,
real: $tType ).
tff(func_def_0,type,
abs_abs:
!>[X0: $tType] : ( X0 > X0 ) ).
tff(func_def_1,type,
plus_plus:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_2,type,
times_times:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_3,type,
bit0: int > int ).
tff(func_def_4,type,
bit1: int > int ).
tff(func_def_5,type,
pls: int ).
tff(func_def_6,type,
number_number_of:
!>[X0: $tType] : ( int > X0 ) ).
tff(func_def_7,type,
power_power:
!>[X0: $tType] : ( ( X0 * nat ) > X0 ) ).
tff(func_def_8,type,
fFalse: bool ).
tff(func_def_9,type,
fTrue: bool ).
tff(func_def_10,type,
v: int ).
tff(func_def_11,type,
w: int ).
tff(func_def_12,type,
sF0: int ).
tff(func_def_13,type,
sF1: int ).
tff(func_def_14,type,
sF2: int ).
tff(func_def_15,type,
sF3: int ).
tff(func_def_16,type,
sF4: nat ).
tff(func_def_17,type,
sF5: int ).
tff(func_def_18,type,
sF6: int ).
tff(func_def_19,type,
sF7: int ).
tff(func_def_20,type,
sF8: int ).
tff(func_def_21,type,
sF9: int ).
tff(func_def_22,type,
sF10: int ).
tff(func_def_23,type,
sF11: int ).
tff(func_def_24,type,
sF12: int ).
tff(func_def_25,type,
sF13: int ).
tff(func_def_26,type,
sF14: int ).
tff(func_def_27,type,
sF15: int ).
tff(func_def_28,type,
sF16: int ).
tff(func_def_29,type,
sF17: int ).
tff(pred_def_1,type,
number:
!>[X0: $tType] : $o ).
tff(pred_def_2,type,
semiring:
!>[X0: $tType] : $o ).
tff(pred_def_3,type,
number_ring:
!>[X0: $tType] : $o ).
tff(pred_def_4,type,
ring_char_0:
!>[X0: $tType] : $o ).
tff(pred_def_5,type,
monoid_mult:
!>[X0: $tType] : $o ).
tff(pred_def_6,type,
number_semiring:
!>[X0: $tType] : $o ).
tff(pred_def_7,type,
comm_semiring:
!>[X0: $tType] : $o ).
tff(pred_def_8,type,
comm_semiring_1:
!>[X0: $tType] : $o ).
tff(pred_def_9,type,
linordered_idom:
!>[X0: $tType] : $o ).
tff(pred_def_10,type,
ab_semigroup_add:
!>[X0: $tType] : $o ).
tff(pred_def_11,type,
ab_semigroup_mult:
!>[X0: $tType] : $o ).
tff(pred_def_12,type,
cancel_semigroup_add:
!>[X0: $tType] : $o ).
tff(pred_def_13,type,
cancel146912293up_add:
!>[X0: $tType] : $o ).
tff(pred_def_14,type,
ordere142940540dd_abs:
!>[X0: $tType] : $o ).
tff(pred_def_15,type,
ab_sem1668676832m_mult:
!>[X0: $tType] : $o ).
tff(pred_def_16,type,
semiri456707255roduct:
!>[X0: $tType] : $o ).
tff(pred_def_17,type,
pp: bool > $o ).
tff(f4,axiom,
! [X0: int,X1: int] : ( times_times(int,bit1(X1),X0) = plus_plus(int,bit0(times_times(int,X1,X0)),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_mult__Bit1) ).
tff(f23,axiom,
! [X0: int] : ( times_times(int,pls,X0) = pls ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_mult__Pls) ).
tff(f33,axiom,
! [X0: int] : ( number_number_of(int,X0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_number__of__is__id) ).
tff(f36,axiom,
! [X0: int] : ( plus_plus(int,pls,X0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_add__Pls) ).
tff(f37,axiom,
! [X0: int] : ( bit0(X0) = plus_plus(int,X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_Bit0__def) ).
tff(f39,axiom,
! [X0: int,X1: int,X2: int] : ( times_times(int,plus_plus(int,X2,X1),X0) = plus_plus(int,times_times(int,X2,X0),times_times(int,X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_int__distrib_I1_J) ).
tff(f40,axiom,
! [X0: int,X1: int,X2: int] : ( times_times(int,X2,plus_plus(int,X1,X0)) = plus_plus(int,times_times(int,X2,X1),times_times(int,X2,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_int__distrib_I2_J) ).
tff(f53,axiom,
! [X0: $tType] :
( number_semiring(X0)
=> ! [X1: X0] : ( times_times(X0,X1,number_number_of(X0,bit0(bit1(pls)))) = plus_plus(X0,X1,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_semiring__mult__2__right) ).
tff(f60,axiom,
! [X0: $tType] :
( comm_semiring_1(X0)
=> ! [X1: X0] : ( times_times(X0,X1,X1) = power_power(X0,X1,number_number_of(nat,bit0(bit1(pls)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J) ).
tff(f62,axiom,
! [X0: $tType] :
( linordered_idom(X0)
=> ! [X1: X0] : ( times_times(X0,abs_abs(X0,X1),abs_abs(X0,X1)) = times_times(X0,X1,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_abs__mult__self) ).
tff(f70,axiom,
! [X0: $tType] :
( comm_semiring_1(X0)
=> ! [X1: X0,X2: X0] : ( times_times(X0,X2,X1) = times_times(X0,X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J) ).
tff(f105,axiom,
linordered_idom(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Olinordered__idom) ).
tff(f106,axiom,
comm_semiring_1(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Ocomm__semiring__1) ).
tff(f108,axiom,
number_semiring(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Int_Onumber__semiring) ).
tff(f142,conjecture,
plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),power_power(int,v,number_number_of(nat,bit0(bit1(pls))))),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),power_power(int,w,number_number_of(nat,bit0(bit1(pls)))))) = plus_plus(int,power_power(int,times_times(int,number_number_of(int,bit0(bit1(pls))),abs_abs(int,v)),number_number_of(nat,bit0(bit1(pls)))),power_power(int,times_times(int,number_number_of(int,bit0(bit1(pls))),abs_abs(int,w)),number_number_of(nat,bit0(bit1(pls))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
tff(f143,negated_conjecture,
( ( ~ plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),power_power(int,v,number_number_of(nat,bit0(bit1(pls))))),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),power_power(int,w,number_number_of(nat,bit0(bit1(pls)))))) ) = plus_plus(int,power_power(int,times_times(int,number_number_of(int,bit0(bit1(pls))),abs_abs(int,v)),number_number_of(nat,bit0(bit1(pls)))),power_power(int,times_times(int,number_number_of(int,bit0(bit1(pls))),abs_abs(int,w)),number_number_of(nat,bit0(bit1(pls))))) ),
inference(negated_conjecture,[status(cth)],[f142]) ).
tff(f145,plain,
plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),power_power(int,v,number_number_of(nat,bit0(bit1(pls))))),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),power_power(int,w,number_number_of(nat,bit0(bit1(pls)))))) != plus_plus(int,power_power(int,times_times(int,number_number_of(int,bit0(bit1(pls))),abs_abs(int,v)),number_number_of(nat,bit0(bit1(pls)))),power_power(int,times_times(int,number_number_of(int,bit0(bit1(pls))),abs_abs(int,w)),number_number_of(nat,bit0(bit1(pls))))),
inference(flattening,[],[f143]) ).
tff(f175,plain,
! [X0: $tType] :
( ! [X1: X0] : ( times_times(X0,X1,number_number_of(X0,bit0(bit1(pls)))) = plus_plus(X0,X1,X1) )
| ~ number_semiring(X0) ),
inference(ennf_transformation,[],[f53]) ).
tff(f179,plain,
! [X0: $tType] :
( ! [X1: X0] : ( times_times(X0,X1,X1) = power_power(X0,X1,number_number_of(nat,bit0(bit1(pls)))) )
| ~ comm_semiring_1(X0) ),
inference(ennf_transformation,[],[f60]) ).
tff(f181,plain,
! [X0: $tType] :
( ! [X1: X0] : ( times_times(X0,abs_abs(X0,X1),abs_abs(X0,X1)) = times_times(X0,X1,X1) )
| ~ linordered_idom(X0) ),
inference(ennf_transformation,[],[f62]) ).
tff(f185,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0] : ( times_times(X0,X2,X1) = times_times(X0,X1,X2) )
| ~ comm_semiring_1(X0) ),
inference(ennf_transformation,[],[f70]) ).
tff(f230,plain,
! [X0: int,X1: int] : ( times_times(int,bit1(X1),X0) = plus_plus(int,bit0(times_times(int,X1,X0)),X0) ),
inference(cnf_transformation,[],[f4]) ).
tff(f254,plain,
! [X0: int] : ( pls = times_times(int,pls,X0) ),
inference(cnf_transformation,[],[f23]) ).
tff(f265,plain,
! [X0: int] : ( number_number_of(int,X0) = X0 ),
inference(cnf_transformation,[],[f33]) ).
tff(f268,plain,
! [X0: int] : ( plus_plus(int,pls,X0) = X0 ),
inference(cnf_transformation,[],[f36]) ).
tff(f269,plain,
! [X0: int] : ( bit0(X0) = plus_plus(int,X0,X0) ),
inference(cnf_transformation,[],[f37]) ).
tff(f271,plain,
! [X2: int,X0: int,X1: int] : ( times_times(int,plus_plus(int,X2,X1),X0) = plus_plus(int,times_times(int,X2,X0),times_times(int,X1,X0)) ),
inference(cnf_transformation,[],[f39]) ).
tff(f272,plain,
! [X2: int,X0: int,X1: int] : ( times_times(int,X2,plus_plus(int,X1,X0)) = plus_plus(int,times_times(int,X2,X1),times_times(int,X2,X0)) ),
inference(cnf_transformation,[],[f40]) ).
tff(f285,plain,
! [X0: $tType,X1: X0] :
( ( plus_plus(X0,X1,X1) = times_times(X0,X1,number_number_of(X0,bit0(bit1(pls)))) )
| ~ number_semiring(X0) ),
inference(cnf_transformation,[],[f175]) ).
tff(f293,plain,
! [X0: $tType,X1: X0] :
( ( power_power(X0,X1,number_number_of(nat,bit0(bit1(pls)))) = times_times(X0,X1,X1) )
| ~ comm_semiring_1(X0) ),
inference(cnf_transformation,[],[f179]) ).
tff(f295,plain,
! [X0: $tType,X1: X0] :
( ~ linordered_idom(X0)
| ( times_times(X0,X1,X1) = times_times(X0,abs_abs(X0,X1),abs_abs(X0,X1)) ) ),
inference(cnf_transformation,[],[f181]) ).
tff(f302,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ~ comm_semiring_1(X0)
| ( times_times(X0,X2,X1) = times_times(X0,X1,X2) ) ),
inference(cnf_transformation,[],[f185]) ).
tff(f341,plain,
linordered_idom(int),
inference(cnf_transformation,[],[f105]) ).
tff(f342,plain,
comm_semiring_1(int),
inference(cnf_transformation,[],[f106]) ).
tff(f344,plain,
number_semiring(int),
inference(cnf_transformation,[],[f108]) ).
tff(f378,plain,
plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),power_power(int,v,number_number_of(nat,bit0(bit1(pls))))),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),power_power(int,w,number_number_of(nat,bit0(bit1(pls)))))) != plus_plus(int,power_power(int,times_times(int,number_number_of(int,bit0(bit1(pls))),abs_abs(int,v)),number_number_of(nat,bit0(bit1(pls)))),power_power(int,times_times(int,number_number_of(int,bit0(bit1(pls))),abs_abs(int,w)),number_number_of(nat,bit0(bit1(pls))))),
inference(cnf_transformation,[],[f145]) ).
tff(f382,plain,
! [X0: int,X1: int] : ( times_times(int,bit1(X1),X0) = plus_plus(int,plus_plus(int,times_times(int,X1,X0),times_times(int,X1,X0)),X0) ),
inference(definition_unfolding,[],[f230,f269]) ).
tff(f405,plain,
! [X0: $tType,X1: X0] :
( ~ number_semiring(X0)
| ( plus_plus(X0,X1,X1) = times_times(X0,X1,number_number_of(X0,plus_plus(int,bit1(pls),bit1(pls)))) ) ),
inference(definition_unfolding,[],[f285,f269]) ).
tff(f413,plain,
! [X0: $tType,X1: X0] :
( ~ comm_semiring_1(X0)
| ( times_times(X0,X1,X1) = power_power(X0,X1,number_number_of(nat,plus_plus(int,bit1(pls),bit1(pls)))) ) ),
inference(definition_unfolding,[],[f293,f269]) ).
tff(f415,plain,
plus_plus(int,times_times(int,number_number_of(int,plus_plus(int,plus_plus(int,bit1(pls),bit1(pls)),plus_plus(int,bit1(pls),bit1(pls)))),power_power(int,v,number_number_of(nat,plus_plus(int,bit1(pls),bit1(pls))))),times_times(int,number_number_of(int,plus_plus(int,plus_plus(int,bit1(pls),bit1(pls)),plus_plus(int,bit1(pls),bit1(pls)))),power_power(int,w,number_number_of(nat,plus_plus(int,bit1(pls),bit1(pls)))))) != plus_plus(int,power_power(int,times_times(int,number_number_of(int,plus_plus(int,bit1(pls),bit1(pls))),abs_abs(int,v)),number_number_of(nat,plus_plus(int,bit1(pls),bit1(pls)))),power_power(int,times_times(int,number_number_of(int,plus_plus(int,bit1(pls),bit1(pls))),abs_abs(int,w)),number_number_of(nat,plus_plus(int,bit1(pls),bit1(pls))))),
inference(definition_unfolding,[],[f378,f269,f269,f269,f269,f269,f269,f269,f269,f269,f269]) ).
tff(f429,definition,
sF0 = bit1(pls),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
tff(f430,plain,
bit1(pls) = sF0,
inference(reorient_equations,[],[f429]) ).
tff(f431,definition,
sF1 = plus_plus(int,sF0,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
tff(f432,plain,
plus_plus(int,sF0,sF0) = sF1,
inference(reorient_equations,[],[f431]) ).
tff(f433,definition,
sF2 = plus_plus(int,sF1,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
tff(f434,plain,
plus_plus(int,sF1,sF1) = sF2,
inference(reorient_equations,[],[f433]) ).
tff(f435,definition,
sF3 = number_number_of(int,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
tff(f436,plain,
number_number_of(int,sF2) = sF3,
inference(reorient_equations,[],[f435]) ).
tff(f437,definition,
sF4 = number_number_of(nat,sF1),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
tff(f438,plain,
number_number_of(nat,sF1) = sF4,
inference(reorient_equations,[],[f437]) ).
tff(f439,definition,
sF5 = power_power(int,v,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
tff(f440,plain,
power_power(int,v,sF4) = sF5,
inference(reorient_equations,[],[f439]) ).
tff(f441,definition,
sF6 = times_times(int,sF3,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
tff(f442,plain,
times_times(int,sF3,sF5) = sF6,
inference(reorient_equations,[],[f441]) ).
tff(f443,definition,
sF7 = power_power(int,w,sF4),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
tff(f444,plain,
power_power(int,w,sF4) = sF7,
inference(reorient_equations,[],[f443]) ).
tff(f445,definition,
sF8 = times_times(int,sF3,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
tff(f446,plain,
times_times(int,sF3,sF7) = sF8,
inference(reorient_equations,[],[f445]) ).
tff(f447,definition,
sF9 = plus_plus(int,sF6,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
tff(f448,plain,
plus_plus(int,sF6,sF8) = sF9,
inference(reorient_equations,[],[f447]) ).
tff(f449,definition,
sF10 = number_number_of(int,sF1),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
tff(f450,plain,
number_number_of(int,sF1) = sF10,
inference(reorient_equations,[],[f449]) ).
tff(f451,definition,
sF11 = abs_abs(int,v),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
tff(f452,plain,
abs_abs(int,v) = sF11,
inference(reorient_equations,[],[f451]) ).
tff(f453,definition,
sF12 = times_times(int,sF10,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
tff(f454,plain,
times_times(int,sF10,sF11) = sF12,
inference(reorient_equations,[],[f453]) ).
tff(f455,definition,
sF13 = power_power(int,sF12,sF4),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
tff(f456,plain,
power_power(int,sF12,sF4) = sF13,
inference(reorient_equations,[],[f455]) ).
tff(f457,definition,
sF14 = abs_abs(int,w),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f458,plain,
abs_abs(int,w) = sF14,
inference(reorient_equations,[],[f457]) ).
tff(f459,definition,
sF15 = times_times(int,sF10,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
tff(f460,plain,
times_times(int,sF10,sF14) = sF15,
inference(reorient_equations,[],[f459]) ).
tff(f461,definition,
sF16 = power_power(int,sF15,sF4),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
tff(f462,plain,
power_power(int,sF15,sF4) = sF16,
inference(reorient_equations,[],[f461]) ).
tff(f463,definition,
sF17 = plus_plus(int,sF13,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
tff(f464,plain,
plus_plus(int,sF13,sF16) = sF17,
inference(reorient_equations,[],[f463]) ).
tff(f465,plain,
sF9 != sF17,
inference(definition_folding,[],[f415,f464,f462,f438,f432,f430,f430,f460,f458,f450,f432,f430,f430,f456,f438,f432,f430,f430,f454,f452,f450,f432,f430,f430,f448,f446,f444,f438,f432,f430,f430,f436,f434,f432,f430,f430,f432,f430,f430,f442,f440,f438,f432,f430,f430,f436,f434,f432,f430,f430,f432,f430,f430]) ).
tff(f503,plain,
! [X0: int,X1: int] : ( times_times(int,plus_plus(int,X0,X0),X1) = times_times(int,X0,plus_plus(int,X1,X1)) ),
inference(superposition,[],[f272,f271]) ).
tff(f1241,plain,
! [X0: int] : ( power_power(int,X0,number_number_of(nat,plus_plus(int,bit1(pls),bit1(pls)))) = times_times(int,X0,X0) ),
inference(resolution,[],[f342,f413]) ).
tff(f1585,plain,
! [X0: int,X1: int] : ( times_times(int,bit1(X1),X0) = plus_plus(int,times_times(int,plus_plus(int,X1,X1),X0),X0) ),
inference(forward_demodulation,[],[f382,f271]) ).
tff(f1589,plain,
! [X0: int] : ( times_times(int,bit1(pls),X0) = plus_plus(int,times_times(int,pls,X0),X0) ),
inference(superposition,[],[f1585,f268]) ).
tff(f1617,plain,
! [X0: int] : ( plus_plus(int,pls,X0) = times_times(int,bit1(pls),X0) ),
inference(forward_demodulation,[],[f1589,f254]) ).
tff(f1623,plain,
! [X0: int] : ( times_times(int,bit1(pls),X0) = X0 ),
inference(forward_demodulation,[],[f1617,f268]) ).
tff(f1633,plain,
! [X0: int] : ( plus_plus(int,X0,X0) = times_times(int,plus_plus(int,bit1(pls),bit1(pls)),X0) ),
inference(superposition,[],[f1623,f503]) ).
tff(f2007,plain,
! [X0: int] : ( plus_plus(int,X0,X0) = times_times(int,X0,number_number_of(int,plus_plus(int,bit1(pls),bit1(pls)))) ),
inference(resolution,[],[f344,f405]) ).
tff(f2010,plain,
! [X0: int] : ( plus_plus(int,X0,X0) = times_times(int,X0,plus_plus(int,bit1(pls),bit1(pls))) ),
inference(forward_demodulation,[],[f2007,f265]) ).
tff(f2011,plain,
! [X0: int] : ( times_times(int,plus_plus(int,bit1(pls),bit1(pls)),X0) = times_times(int,X0,plus_plus(int,bit1(pls),bit1(pls))) ),
inference(superposition,[],[f2010,f1633]) ).
tff(f23188,plain,
sF2 = sF3,
inference(forward_demodulation,[],[f436,f265]) ).
tff(f24607,plain,
sF1 = sF10,
inference(forward_demodulation,[],[f450,f265]) ).
tff(f36216,plain,
plus_plus(int,bit1(pls),bit1(pls)) = sF1,
inference(forward_demodulation,[],[f432,f430]) ).
tff(f38996,plain,
plus_plus(int,sF1,sF1) = sF3,
inference(forward_demodulation,[],[f434,f23188]) ).
tff(f39009,plain,
! [X0: int] : ( times_times(int,plus_plus(int,X0,X0),sF1) = times_times(int,X0,sF3) ),
inference(superposition,[],[f503,f38996]) ).
tff(f40791,plain,
sF12 = times_times(int,sF10,abs_abs(int,v)),
inference(forward_demodulation,[],[f454,f452]) ).
tff(f40792,plain,
sF12 = times_times(int,sF1,abs_abs(int,v)),
inference(forward_demodulation,[],[f40791,f24607]) ).
tff(f40975,plain,
sF15 = times_times(int,sF10,abs_abs(int,w)),
inference(forward_demodulation,[],[f460,f458]) ).
tff(f40976,plain,
sF15 = times_times(int,sF1,abs_abs(int,w)),
inference(forward_demodulation,[],[f40975,f24607]) ).
tff(f41600,plain,
! [X0: int] : ( times_times(int,X0,X0) = power_power(int,X0,number_number_of(nat,sF1)) ),
inference(backward_demodulation,[],[f1241,f36216]) ).
tff(f41603,plain,
! [X0: int] : ( plus_plus(int,X0,X0) = times_times(int,sF1,X0) ),
inference(backward_demodulation,[],[f1633,f36216]) ).
tff(f41607,plain,
! [X0: int] : ( times_times(int,sF1,X0) = times_times(int,X0,sF1) ),
inference(backward_demodulation,[],[f2011,f36216]) ).
tff(f41852,plain,
! [X0: int] : ( times_times(int,X0,X0) = power_power(int,X0,sF4) ),
inference(forward_demodulation,[],[f41600,f438]) ).
tff(f42670,plain,
sF5 = times_times(int,v,v),
inference(backward_demodulation,[],[f440,f41852]) ).
tff(f42915,plain,
! [X0: int,X1: int] : ( times_times(int,plus_plus(int,X0,X0),X1) = times_times(int,sF1,times_times(int,X0,X1)) ),
inference(superposition,[],[f41603,f271]) ).
tff(f42916,plain,
! [X0: int,X1: int] : ( times_times(int,X0,plus_plus(int,X1,X1)) = times_times(int,sF1,times_times(int,X0,X1)) ),
inference(superposition,[],[f41603,f272]) ).
tff(f42931,plain,
! [X0: int,X1: int] : ( times_times(int,X0,plus_plus(int,X1,X1)) = times_times(int,times_times(int,sF1,X0),X1) ),
inference(superposition,[],[f503,f41603]) ).
tff(f43588,plain,
! [X0: int] : ( times_times(int,plus_plus(int,sF1,sF1),X0) = times_times(int,plus_plus(int,X0,X0),sF1) ),
inference(superposition,[],[f503,f41607]) ).
tff(f43995,plain,
! [X0: int] : ( times_times(int,plus_plus(int,sF1,sF1),X0) = times_times(int,X0,sF3) ),
inference(forward_demodulation,[],[f43588,f39009]) ).
tff(f44064,plain,
! [X0: int] : ( times_times(int,sF3,X0) = times_times(int,X0,sF3) ),
inference(forward_demodulation,[],[f43995,f38996]) ).
tff(f56250,plain,
! [X0: int,X1: int] : ( times_times(int,X1,X0) = times_times(int,X0,X1) ),
inference(resolution,[],[f302,f342]) ).
tff(f96704,plain,
! [X0: int] : ( times_times(int,X0,X0) = times_times(int,abs_abs(int,X0),abs_abs(int,X0)) ),
inference(resolution,[],[f295,f341]) ).
tff(f97716,plain,
! [X0: int] : ( times_times(int,X0,X0) = power_power(int,abs_abs(int,X0),sF4) ),
inference(superposition,[],[f96704,f41852]) ).
tff(f99057,plain,
! [X0: int] : ( power_power(int,X0,sF4) = power_power(int,abs_abs(int,X0),sF4) ),
inference(superposition,[],[f97716,f41852]) ).
tff(f99473,plain,
! [X0: int] : ( power_power(int,X0,sF4) = times_times(int,abs_abs(int,X0),abs_abs(int,X0)) ),
inference(superposition,[],[f99057,f41852]) ).
tff(f110744,plain,
! [X0: int] : ( times_times(int,sF12,X0) = times_times(int,abs_abs(int,v),plus_plus(int,X0,X0)) ),
inference(superposition,[],[f42931,f40792]) ).
tff(f110745,plain,
! [X0: int] : ( times_times(int,sF15,X0) = times_times(int,abs_abs(int,w),plus_plus(int,X0,X0)) ),
inference(superposition,[],[f42931,f40976]) ).
tff(f111443,plain,
! [X0: int] : ( times_times(int,sF12,X0) = times_times(int,sF1,times_times(int,abs_abs(int,v),X0)) ),
inference(superposition,[],[f110744,f42916]) ).
tff(f111542,plain,
! [X0: int] : ( times_times(int,sF15,X0) = times_times(int,sF1,times_times(int,abs_abs(int,w),X0)) ),
inference(superposition,[],[f110745,f42916]) ).
tff(f111787,plain,
times_times(int,sF1,times_times(int,v,v)) = times_times(int,sF12,abs_abs(int,v)),
inference(superposition,[],[f111443,f96704]) ).
tff(f111902,plain,
times_times(int,sF1,times_times(int,v,v)) = times_times(int,abs_abs(int,v),sF12),
inference(forward_demodulation,[],[f111787,f56250]) ).
tff(f111924,plain,
times_times(int,sF1,sF5) = times_times(int,abs_abs(int,v),sF12),
inference(forward_demodulation,[],[f111902,f42670]) ).
tff(f111942,plain,
times_times(int,sF12,sF12) = times_times(int,sF1,times_times(int,sF1,sF5)),
inference(superposition,[],[f111443,f111924]) ).
tff(f111956,plain,
times_times(int,sF12,sF12) = times_times(int,plus_plus(int,sF1,sF1),sF5),
inference(forward_demodulation,[],[f111942,f42915]) ).
tff(f111958,plain,
times_times(int,sF12,sF12) = times_times(int,sF5,plus_plus(int,sF1,sF1)),
inference(forward_demodulation,[],[f111956,f56250]) ).
tff(f111959,plain,
times_times(int,sF12,sF12) = times_times(int,sF5,sF3),
inference(forward_demodulation,[],[f111958,f38996]) ).
tff(f111960,plain,
times_times(int,sF3,sF5) = times_times(int,sF12,sF12),
inference(forward_demodulation,[],[f111959,f44064]) ).
tff(f111961,plain,
times_times(int,sF3,sF5) = power_power(int,sF12,sF4),
inference(forward_demodulation,[],[f111960,f41852]) ).
tff(f111962,plain,
times_times(int,sF3,sF5) = sF13,
inference(forward_demodulation,[],[f111961,f456]) ).
tff(f111963,plain,
sF6 = sF13,
inference(forward_demodulation,[],[f111962,f442]) ).
tff(f112689,plain,
sF17 = plus_plus(int,sF6,sF16),
inference(forward_demodulation,[],[f464,f111963]) ).
tff(f113390,plain,
times_times(int,sF15,abs_abs(int,w)) = times_times(int,sF1,power_power(int,w,sF4)),
inference(superposition,[],[f111542,f99473]) ).
tff(f113514,plain,
times_times(int,sF1,sF7) = times_times(int,sF15,abs_abs(int,w)),
inference(forward_demodulation,[],[f113390,f444]) ).
tff(f113539,plain,
times_times(int,sF1,sF7) = times_times(int,abs_abs(int,w),sF15),
inference(forward_demodulation,[],[f113514,f56250]) ).
tff(f113560,plain,
times_times(int,sF15,sF15) = times_times(int,sF1,times_times(int,sF1,sF7)),
inference(superposition,[],[f111542,f113539]) ).
tff(f113573,plain,
times_times(int,sF15,sF15) = times_times(int,plus_plus(int,sF1,sF1),sF7),
inference(forward_demodulation,[],[f113560,f42915]) ).
tff(f113576,plain,
times_times(int,sF3,sF7) = times_times(int,sF15,sF15),
inference(forward_demodulation,[],[f113573,f38996]) ).
tff(f113578,plain,
times_times(int,sF3,sF7) = power_power(int,sF15,sF4),
inference(forward_demodulation,[],[f113576,f41852]) ).
tff(f113579,plain,
times_times(int,sF3,sF7) = sF16,
inference(forward_demodulation,[],[f113578,f462]) ).
tff(f113580,plain,
sF8 = sF16,
inference(forward_demodulation,[],[f113579,f446]) ).
tff(f113601,plain,
plus_plus(int,sF6,sF8) = sF17,
inference(backward_demodulation,[],[f112689,f113580]) ).
tff(f113608,plain,
sF9 = sF17,
inference(forward_demodulation,[],[f113601,f448]) ).
tff(f113612,plain,
$false,
inference(forward_subsumption_resolution,[],[f113608,f465]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM996_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n002.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 21:52:21 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.47/1.77 % (3921529)Detected formulas, will run a generic FOF schedule.
% 5.47/1.77 % (3921537)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2727350997:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.47/1.77 % (3921537)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 5.47/1.77 % (3921537)Refutation not found, incomplete strategy
% 5.47/1.77 % (3921537)------------------------------
% 5.47/1.77 % (3921537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.47/1.77 % (3921537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.77 % (3921537)CaDiCaL version: 2.1.3
% 5.47/1.77 % (3921537)Termination reason: Refutation not found, incomplete strategy
% 5.47/1.77 % (3921537)Time elapsed: 0.011 s
% 5.47/1.77 % (3921537)Peak memory usage: 89 MB
% 5.47/1.77 % (3921537)Instructions burned: 40 (million)
% 5.47/1.77 % (3921536)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2017025498:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.47/1.77 % (3921539)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3497366384:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.47/1.77 % (3921538)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4148053053:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.47/1.77 % (3921534)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2258344437:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.47/1.77 % (3921540)dis-21_1_sil=8000:lcm=predicate:random_seed=2696284682:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 5.47/1.77 % (3921535)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2347488340:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.47/1.77 % (3921536)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 5.47/1.77 % (3921540)Refutation not found, incomplete strategy
% 5.47/1.77 % (3921540)------------------------------
% 5.47/1.77 % (3921540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.47/1.77 % (3921540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.77 % (3921540)CaDiCaL version: 2.1.3
% 5.47/1.77 % (3921540)Termination reason: Refutation not found, incomplete strategy
% 5.47/1.77 % (3921540)Time elapsed: 0.010 s
% 5.47/1.77 % (3921540)Peak memory usage: 88 MB
% 5.47/1.77 % (3921540)Instructions burned: 16 (million)
% 5.47/1.77 % (3921538)Instruction limit reached!
% 5.47/1.77 % (3921538)------------------------------
% 5.47/1.77 % (3921538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.47/1.77 % (3921538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.77 % (3921538)CaDiCaL version: 2.1.3
% 5.47/1.77 % (3921538)Termination reason: Instruction limit
% 5.47/1.77 % (3921538)Termination phase: Saturation
% 5.47/1.77 % (3921538)Time elapsed: 0.063 s
% 5.47/1.77 % (3921538)Peak memory usage: 88 MB
% 5.47/1.77 % (3921538)Instructions burned: 119 (million)
% 5.47/1.77 % (3921539)Instruction limit reached!
% 5.47/1.77 % (3921539)------------------------------
% 5.47/1.77 % (3921539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.47/1.77 % (3921539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.77 % (3921539)CaDiCaL version: 2.1.3
% 5.47/1.77 % (3921539)Termination reason: Instruction limit
% 5.47/1.77 % (3921539)Termination phase: Saturation
% 5.47/1.77 % (3921539)Time elapsed: 0.078 s
% 5.47/1.77 % (3921539)Peak memory usage: 89 MB
% 5.47/1.77 % (3921539)Instructions burned: 140 (million)
% 5.47/1.77 % (3921537)------------------------------
% 5.47/1.77 % (3921537)------------------------------
% 5.47/1.77 % (3921549)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2875999166:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.47/1.77 % (3921548)lrs+10_1_sil=8000:sp=occurrence:random_seed=4099261863:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.47/1.77 % (3921550)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1166545910:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 8.60/2.09 % (3921540)------------------------------
% 8.60/2.09 % (3921540)------------------------------
% 8.60/2.09 % (3921549)Instruction limit reached!
% 8.60/2.09 % (3921549)------------------------------
% 8.60/2.09 % (3921549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.09 % (3921549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.09 % (3921549)CaDiCaL version: 2.1.3
% 8.60/2.09 % (3921549)Termination reason: Instruction limit
% 8.60/2.09 % (3921549)Termination phase: Saturation
% 8.60/2.09 % (3921549)Time elapsed: 0.090 s
% 8.60/2.09 % (3921549)Peak memory usage: 89 MB
% 8.60/2.09 % (3921549)Instructions burned: 158 (million)
% 8.60/2.09 % (3921550)Instruction limit reached!
% 8.60/2.09 % (3921550)------------------------------
% 8.60/2.09 % (3921550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.09 % (3921550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.09 % (3921550)CaDiCaL version: 2.1.3
% 8.60/2.09 % (3921550)Termination reason: Instruction limit
% 8.60/2.09 % (3921550)Termination phase: Saturation
% 8.60/2.09 % (3921550)Time elapsed: 0.098 s
% 8.60/2.09 % (3921550)Peak memory usage: 91 MB
% 8.60/2.09 % (3921550)Instructions burned: 327 (million)
% 8.60/2.09 % (3921534)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.60/2.09 % (3921535)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.60/2.09 % (3921536)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.60/2.09 % (3921536)------------------------------
% 8.60/2.09 % (3921536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.09 % (3921534)------------------------------
% 8.60/2.09 % (3921534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.09 % (3921535)------------------------------
% 8.60/2.09 % (3921535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.09 % (3921534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.09 % (3921535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.09 % (3921536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.09 % (3921535)CaDiCaL version: 2.1.3
% 8.60/2.09 % (3921534)CaDiCaL version: 2.1.3
% 8.60/2.09 % (3921534)Termination reason: Unknown
% 8.60/2.09 % (3921534)Termination phase: Saturation
% 8.60/2.09 % (3921535)Termination reason: Unknown
% 8.60/2.09 % (3921535)Termination phase: Saturation
% 8.60/2.09 % (3921536)CaDiCaL version: 2.1.3
% 8.60/2.09 % (3921535)Time elapsed: 0.366 s
% 8.60/2.09 % (3921536)Termination reason: Unknown
% 8.60/2.09 % (3921536)Termination phase: Saturation
% 8.60/2.09 % (3921534)Time elapsed: 0.366 s
% 8.60/2.09 % (3921536)Time elapsed: 0.366 s
% 8.60/2.09 % (3921535)Peak memory usage: 111 MB
% 8.60/2.09 % (3921534)Peak memory usage: 111 MB
% 8.60/2.09 % (3921536)Peak memory usage: 112 MB
% 8.60/2.09 % (3921534)Instructions burned: 541 (million)
% 8.60/2.09 % (3921535)Instructions burned: 544 (million)
% 8.60/2.09 % (3921536)Instructions burned: 542 (million)
% 8.60/2.09 % (3921548)Instruction limit reached!
% 8.60/2.09 % (3921548)------------------------------
% 8.60/2.09 % (3921548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.09 % (3921548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.09 % (3921548)CaDiCaL version: 2.1.3
% 8.60/2.09 % (3921548)Termination reason: Instruction limit
% 8.60/2.09 % (3921548)Termination phase: Saturation
% 8.60/2.09 % (3921548)Time elapsed: 0.158 s
% 8.60/2.09 % (3921548)Peak memory usage: 90 MB
% 8.60/2.09 % (3921548)Instructions burned: 286 (million)
% 8.60/2.09 % (3921554)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=807747615:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 8.60/2.09 % (3921556)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4215419452:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 8.60/2.09 % (3921555)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1781826339:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 8.60/2.09 % (3921559)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3784618269:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 8.60/2.09 % (3921558)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=756783185:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 9.26/2.32 % (3921557)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3083640299:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 9.26/2.32 % (3921558)Refutation not found, incomplete strategy
% 9.26/2.32 % (3921558)------------------------------
% 9.26/2.32 % (3921558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.26/2.32 % (3921558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.26/2.32 % (3921558)CaDiCaL version: 2.1.3
% 9.26/2.32 % (3921558)Termination reason: Refutation not found, incomplete strategy
% 9.26/2.32 % (3921558)Time elapsed: 0.005 s
% 9.26/2.32 % (3921558)Peak memory usage: 88 MB
% 9.26/2.32 % (3921558)Instructions burned: 9 (million)
% 9.26/2.32 % (3921560)lrs+10_1_sil=8000:sp=occurrence:random_seed=1446401806:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi)
% 9.26/2.32 % (3921554)Instruction limit reached!
% 9.26/2.32 % (3921554)------------------------------
% 9.26/2.32 % (3921554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.26/2.32 % (3921554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.26/2.32 % (3921554)CaDiCaL version: 2.1.3
% 9.26/2.32 % (3921554)Termination reason: Instruction limit
% 9.26/2.32 % (3921554)Termination phase: Saturation
% 9.26/2.32 % (3921554)Time elapsed: 0.145 s
% 9.26/2.32 % (3921554)Peak memory usage: 90 MB
% 9.26/2.32 % (3921554)Instructions burned: 249 (million)
% 9.26/2.32 % (3921559)Instruction limit reached!
% 9.26/2.32 % (3921559)------------------------------
% 9.26/2.32 % (3921559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.26/2.32 % (3921559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.26/2.32 % (3921559)CaDiCaL version: 2.1.3
% 9.26/2.32 % (3921559)Termination reason: Instruction limit
% 9.26/2.32 % (3921559)Termination phase: Saturation
% 9.26/2.32 % (3921559)Time elapsed: 0.054 s
% 9.26/2.32 % (3921559)Peak memory usage: 88 MB
% 9.26/2.32 % (3921559)Instructions burned: 115 (million)
% 9.26/2.32 % (3921557)Instruction limit reached!
% 9.26/2.32 % (3921557)------------------------------
% 9.26/2.32 % (3921557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.26/2.32 % (3921557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.26/2.32 % (3921557)CaDiCaL version: 2.1.3
% 9.26/2.32 % (3921557)Termination reason: Instruction limit
% 9.26/2.32 % (3921557)Termination phase: Saturation
% 9.26/2.32 % (3921557)Time elapsed: 0.060 s
% 9.26/2.32 % (3921557)Peak memory usage: 89 MB
% 9.26/2.32 % (3921557)Instructions burned: 114 (million)
% 9.26/2.32 % (3921555)Instruction limit reached!
% 9.26/2.32 % (3921555)------------------------------
% 9.26/2.32 % (3921555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.26/2.32 % (3921555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.26/2.32 % (3921555)CaDiCaL version: 2.1.3
% 9.26/2.32 % (3921555)Termination reason: Instruction limit
% 9.26/2.32 % (3921555)Termination phase: Saturation
% 9.26/2.32 % (3921555)Time elapsed: 0.135 s
% 9.26/2.32 % (3921555)Peak memory usage: 89 MB
% 9.26/2.32 % (3921555)Instructions burned: 294 (million)
% 9.26/2.32 % (3921556)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.26/2.32 % (3921556)------------------------------
% 9.26/2.32 % (3921556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.26/2.32 % (3921556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.26/2.32 % (3921556)CaDiCaL version: 2.1.3
% 9.26/2.32 % (3921556)Termination reason: Unknown
% 9.26/2.32 % (3921556)Termination phase: Saturation
% 9.26/2.32 % (3921556)Time elapsed: 0.201 s
% 9.26/2.32 % (3921556)Peak memory usage: 113 MB
% 9.26/2.32 % (3921556)Instructions burned: 542 (million)
% 9.26/2.32 % (3921568)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=424390629:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 9.26/2.32 % (3921569)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=403288741:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 9.26/2.32 % (3921568)Refutation not found, incomplete strategy
% 9.26/2.32 % (3921568)------------------------------
% 9.26/2.32 % (3921568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.90/2.61 % (3921568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.90/2.61 % (3921568)CaDiCaL version: 2.1.3
% 10.90/2.61 % (3921568)Termination reason: Refutation not found, incomplete strategy
% 10.90/2.61 % (3921568)Time elapsed: 0.008 s
% 10.90/2.61 % (3921568)Peak memory usage: 88 MB
% 10.90/2.61 % (3921568)Instructions burned: 13 (million)
% 10.90/2.61 % (3921570)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4283084728:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi)
% 10.90/2.61 % (3921571)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4045746034:st=8:i=592:sd=3:ep=RST:ss=axioms_2992 on theBenchmark for (2992ds/592Mi)
% 10.90/2.61 % (3921558)------------------------------
% 10.90/2.61 % (3921558)------------------------------
% 10.90/2.61 % (3921572)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3895777691:st=3:i=13193:sd=3:ss=axioms_2991 on theBenchmark for (2991ds/13193Mi)
% 10.90/2.61 % (3921570)Instruction limit reached!
% 10.90/2.61 % (3921570)------------------------------
% 10.90/2.61 % (3921570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.90/2.61 % (3921570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.90/2.61 % (3921570)CaDiCaL version: 2.1.3
% 10.90/2.61 % (3921570)Termination reason: Instruction limit
% 10.90/2.61 % (3921570)Termination phase: Saturation
% 10.90/2.61 % (3921570)Time elapsed: 0.066 s
% 10.90/2.61 % (3921570)Peak memory usage: 89 MB
% 10.90/2.61 % (3921570)Instructions burned: 137 (million)
% 10.90/2.61 % (3921578)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=835304245:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/125Mi)
% 10.90/2.61 % (3921578)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 10.90/2.61 % (3921572)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.90/2.61 % (3921572)------------------------------
% 10.90/2.61 % (3921572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.90/2.61 % (3921572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.90/2.61 % (3921572)CaDiCaL version: 2.1.3
% 10.90/2.61 % (3921572)Termination reason: Unknown
% 10.90/2.61 % (3921572)Termination phase: Saturation
% 10.90/2.61 % (3921572)Time elapsed: 0.199 s
% 10.90/2.61 % (3921572)Peak memory usage: 113 MB
% 10.90/2.61 % (3921572)Instructions burned: 541 (million)
% 10.90/2.61 % (3921579)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1092366038:i=134:gtgl=5:slsql=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/134Mi)
% 10.90/2.61 % (3921568)------------------------------
% 10.90/2.61 % (3921568)------------------------------
% 10.90/2.61 % (3921578)Instruction limit reached!
% 10.90/2.61 % (3921578)------------------------------
% 10.90/2.61 % (3921578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.90/2.61 % (3921578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.90/2.61 % (3921578)CaDiCaL version: 2.1.3
% 10.90/2.61 % (3921578)Termination reason: Instruction limit
% 10.90/2.61 % (3921578)Termination phase: Saturation
% 10.90/2.61 % (3921578)Time elapsed: 0.072 s
% 10.90/2.61 % (3921578)Peak memory usage: 90 MB
% 10.90/2.61 % (3921578)Instructions burned: 126 (million)
% 10.90/2.61 % (3921560)Instruction limit reached!
% 10.90/2.61 % (3921560)------------------------------
% 10.90/2.61 % (3921560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.90/2.61 % (3921560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.90/2.61 % (3921560)CaDiCaL version: 2.1.3
% 10.90/2.61 % (3921560)Termination reason: Instruction limit
% 10.90/2.61 % (3921560)Termination phase: Saturation
% 10.90/2.61 % (3921560)Time elapsed: 0.494 s
% 10.90/2.61 % (3921560)Peak memory usage: 94 MB
% 10.90/2.61 % (3921560)Instructions burned: 908 (million)
% 10.90/2.61 % (3921579)Instruction limit reached!
% 10.90/2.61 % (3921579)------------------------------
% 10.90/2.61 % (3921579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.90/2.61 % (3921579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.90/2.61 % (3921579)CaDiCaL version: 2.1.3
% 10.90/2.61 % (3921579)Termination reason: Instruction limit
% 10.90/2.61 % (3921579)Termination phase: Saturation
% 10.90/2.61 % (3921579)Time elapsed: 0.078 s
% 10.90/2.61 % (3921579)Peak memory usage: 89 MB
% 16.44/3.15 % (3921579)Instructions burned: 136 (million)
% 16.44/3.15 % (3921571)Instruction limit reached!
% 16.44/3.15 % (3921571)------------------------------
% 16.44/3.15 % (3921571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.15 % (3921571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.15 % (3921571)CaDiCaL version: 2.1.3
% 16.44/3.15 % (3921571)Termination reason: Instruction limit
% 16.44/3.15 % (3921571)Termination phase: Saturation
% 16.44/3.15 % (3921571)Time elapsed: 0.319 s
% 16.44/3.15 % (3921571)Peak memory usage: 92 MB
% 16.44/3.15 % (3921571)Instructions burned: 593 (million)
% 16.44/3.15 % (3921582)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4064284497:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/141Mi)
% 16.44/3.15 % (3921582)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 16.44/3.15 % (3921569)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.44/3.15 % (3921569)------------------------------
% 16.44/3.15 % (3921569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.15 % (3921569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.15 % (3921569)CaDiCaL version: 2.1.3
% 16.44/3.15 % (3921569)Termination reason: Unknown
% 16.44/3.15 % (3921569)Termination phase: Saturation
% 16.44/3.15 % (3921569)Time elapsed: 0.369 s
% 16.44/3.15 % (3921569)Peak memory usage: 113 MB
% 16.44/3.15 % (3921569)Instructions burned: 543 (million)
% 16.44/3.15 % (3921582)Refutation not found, incomplete strategy
% 16.44/3.15 % (3921582)------------------------------
% 16.44/3.15 % (3921582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.15 % (3921582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.15 % (3921582)CaDiCaL version: 2.1.3
% 16.44/3.15 % (3921582)Termination reason: Refutation not found, incomplete strategy
% 16.44/3.15 % (3921582)Time elapsed: 0.001 s
% 16.44/3.15 % (3921582)Peak memory usage: 88 MB
% 16.44/3.15 % (3921582)Instructions burned: 3 (million)
% 16.44/3.15 % (3921583)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3432898955:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2988 on theBenchmark for (2988ds/431Mi)
% 16.44/3.15 % (3921583)Refutation not found, incomplete strategy
% 16.44/3.15 % (3921583)------------------------------
% 16.44/3.15 % (3921583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.44/3.15 % (3921583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.44/3.15 % (3921583)CaDiCaL version: 2.1.3
% 16.44/3.15 % (3921583)Termination reason: Refutation not found, incomplete strategy
% 16.44/3.15 % (3921583)Time elapsed: 0.006 s
% 16.44/3.15 % (3921583)Peak memory usage: 88 MB
% 16.44/3.15 % (3921583)Instructions burned: 9 (million)
% 16.44/3.15 % (3921584)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=957759125:i=6060:aac=none:ins=25_2988 on theBenchmark for (2988ds/6060Mi)
% 16.44/3.15 % (3921585)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=878126470:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2987 on theBenchmark for (2987ds/150Mi)
% 16.44/3.15 % (3921585)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 16.44/3.15 % (3921586)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4231261857:i=14155:bd=all_2987 on theBenchmark for (2987ds/14155Mi)
% 16.44/3.15 % (3921587)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3691428247:i=667:av=off:fsr=off_2987 on theBenchmark for (2987ds/667Mi)
% 16.44/3.15 % (3921582)------------------------------
% 16.44/3.15 % (3921582)------------------------------
% 16.44/3.15 % (3921589)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2352123423:s2a=on:i=185:s2at=1.8:fdi=4_2987 on theBenchmark for (2987ds/185Mi)
% 16.44/3.15 % (3921585)Instruction limit reached!
% 16.44/3.15 % (3921585)------------------------------
% 16.44/3.15 % (3921585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/3.77 % (3921585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/3.77 % (3921585)CaDiCaL version: 2.1.3
% 19.29/3.77 % (3921585)Termination reason: Instruction limit
% 19.29/3.77 % (3921585)Termination phase: Saturation
% 19.29/3.77 % (3921585)Time elapsed: 0.087 s
% 19.29/3.77 % (3921585)Peak memory usage: 90 MB
% 19.29/3.77 % (3921585)Instructions burned: 152 (million)
% 19.29/3.77 % (3921589)Instruction limit reached!
% 19.29/3.77 % (3921589)------------------------------
% 19.29/3.77 % (3921589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/3.77 % (3921589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/3.77 % (3921589)CaDiCaL version: 2.1.3
% 19.29/3.77 % (3921589)Termination reason: Instruction limit
% 19.29/3.77 % (3921589)Termination phase: Saturation
% 19.29/3.77 % (3921589)Time elapsed: 0.104 s
% 19.29/3.77 % (3921589)Peak memory usage: 90 MB
% 19.29/3.77 % (3921589)Instructions burned: 187 (million)
% 19.29/3.77 % (3921583)------------------------------
% 19.29/3.77 % (3921583)------------------------------
% 19.29/3.77 % (3921595)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3491568874:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2985 on theBenchmark for (2985ds/193Mi)
% 19.29/3.77 % (3921595)Instruction limit reached!
% 19.29/3.77 % (3921595)------------------------------
% 19.29/3.77 % (3921595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/3.77 % (3921595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/3.77 % (3921595)CaDiCaL version: 2.1.3
% 19.29/3.77 % (3921595)Termination reason: Instruction limit
% 19.29/3.77 % (3921595)Termination phase: Saturation
% 19.29/3.77 % (3921595)Time elapsed: 0.059 s
% 19.29/3.77 % (3921595)Peak memory usage: 90 MB
% 19.29/3.77 % (3921595)Instructions burned: 196 (million)
% 19.29/3.77 % (3921597)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2246626878:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2985 on theBenchmark for (2985ds/4850Mi)
% 19.29/3.77 % (3921597)Refutation not found, incomplete strategy
% 19.29/3.77 % (3921597)------------------------------
% 19.29/3.77 % (3921597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/3.77 % (3921597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/3.77 % (3921597)CaDiCaL version: 2.1.3
% 19.29/3.77 % (3921597)Termination reason: Refutation not found, incomplete strategy
% 19.29/3.77 % (3921597)Time elapsed: 0.005 s
% 19.29/3.77 % (3921597)Peak memory usage: 88 MB
% 19.29/3.77 % (3921597)Instructions burned: 7 (million)
% 19.29/3.77 % (3921584)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.29/3.77 % (3921584)------------------------------
% 19.29/3.77 % (3921584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/3.77 % (3921584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/3.77 % (3921584)CaDiCaL version: 2.1.3
% 19.29/3.77 % (3921584)Termination reason: Unknown
% 19.29/3.77 % (3921584)Termination phase: Saturation
% 19.29/3.77 % (3921584)Time elapsed: 0.369 s
% 19.29/3.77 % (3921584)Peak memory usage: 114 MB
% 19.29/3.77 % (3921584)Instructions burned: 542 (million)
% 19.29/3.77 % (3921599)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2223870851:i=12111:sd=1:ss=included_2984 on theBenchmark for (2984ds/12111Mi)
% 19.29/3.77 % (3921600)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3207202990:i=319:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/319Mi)
% 19.29/3.77 % (3921601)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3107526800:i=2064:ep=RST_2983 on theBenchmark for (2983ds/2064Mi)
% 19.29/3.77 % (3921587)Instruction limit reached!
% 19.29/3.77 % (3921587)------------------------------
% 19.29/3.77 % (3921587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/3.77 % (3921587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/3.77 % (3921587)CaDiCaL version: 2.1.3
% 19.29/3.77 % (3921587)Termination reason: Instruction limit
% 19.29/3.77 % (3921587)Termination phase: Saturation
% 19.29/3.77 % (3921587)Time elapsed: 0.328 s
% 19.29/3.77 % (3921587)Peak memory usage: 89 MB
% 19.29/3.77 % (3921587)Instructions burned: 667 (million)
% 19.29/3.77 % (3921586)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.29/3.77 % (3921586)------------------------------
% 19.29/3.77 % (3921586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.18/4.30 % (3921586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.18/4.30 % (3921586)CaDiCaL version: 2.1.3
% 24.18/4.30 % (3921586)Termination reason: Unknown
% 24.18/4.30 % (3921586)Termination phase: Saturation
% 24.18/4.30 % (3921586)Time elapsed: 0.369 s
% 24.18/4.30 % (3921586)Peak memory usage: 114 MB
% 24.18/4.30 % (3921586)Instructions burned: 542 (million)
% 24.18/4.30 % (3921604)dis-1011_128_sil=32000:random_seed=1349778920:i=3706:ep=RST:av=off_2983 on theBenchmark for (2983ds/3706Mi)
% 24.18/4.30 % (3921597)------------------------------
% 24.18/4.30 % (3921597)------------------------------
% 24.18/4.30 % (3921600)Instruction limit reached!
% 24.18/4.30 % (3921600)------------------------------
% 24.18/4.30 % (3921600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.18/4.30 % (3921600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.18/4.30 % (3921607)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=635885747:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2982 on theBenchmark for (2982ds/757Mi)
% 24.18/4.30 % (3921600)CaDiCaL version: 2.1.3
% 24.18/4.30 % (3921600)Termination reason: Instruction limit
% 24.18/4.30 % (3921600)Termination phase: Saturation
% 24.18/4.30 % (3921600)Time elapsed: 0.186 s
% 24.18/4.30 % (3921600)Peak memory usage: 92 MB
% 24.18/4.30 % (3921600)Instructions burned: 320 (million)
% 24.18/4.30 % (3921608)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3784964855:i=13913:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/13913Mi)
% 24.18/4.30 % (3921610)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=654347763:i=9925:aac=none_2981 on theBenchmark for (2981ds/9925Mi)
% 24.18/4.30 % (3921612)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2473192677:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2981 on theBenchmark for (2981ds/2479Mi)
% 24.18/4.30 % (3921599)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 24.18/4.30 % (3921599)------------------------------
% 24.18/4.30 % (3921599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.18/4.30 % (3921599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.18/4.30 % (3921599)CaDiCaL version: 2.1.3
% 24.18/4.30 % (3921599)Termination reason: Unknown
% 24.18/4.30 % (3921599)Termination phase: Saturation
% 24.18/4.30 % (3921599)Time elapsed: 0.367 s
% 24.18/4.30 % (3921599)Peak memory usage: 113 MB
% 24.18/4.30 % (3921599)Instructions burned: 542 (million)
% 24.18/4.30 % (3921616)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3151711793:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2979 on theBenchmark for (2979ds/440Mi)
% 24.18/4.30 % (3921616)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 24.18/4.30 % (3921608)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 24.18/4.30 % (3921608)------------------------------
% 24.18/4.30 % (3921608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.18/4.30 % (3921608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.18/4.30 % (3921608)CaDiCaL version: 2.1.3
% 24.18/4.30 % (3921608)Termination reason: Unknown
% 24.18/4.30 % (3921608)Termination phase: Saturation
% 24.18/4.30 % (3921608)Time elapsed: 0.360 s
% 24.18/4.30 % (3921608)Peak memory usage: 113 MB
% 24.18/4.30 % (3921608)Instructions burned: 540 (million)
% 24.18/4.30 % (3921607)Instruction limit reached!
% 24.18/4.30 % (3921607)------------------------------
% 24.18/4.30 % (3921607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.18/4.30 % (3921607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.18/4.30 % (3921607)CaDiCaL version: 2.1.3
% 24.18/4.30 % (3921607)Termination reason: Instruction limit
% 24.18/4.30 % (3921607)Termination phase: Saturation
% 24.18/4.30 % (3921607)Time elapsed: 0.393 s
% 24.18/4.30 % (3921607)Peak memory usage: 95 MB
% 24.18/4.30 % (3921607)Instructions burned: 759 (million)
% 24.18/4.30 % (3921601)Instruction limit reached!
% 24.18/4.30 % (3921601)------------------------------
% 24.18/4.30 % (3921601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.18/4.30 % (3921601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.18/4.30 % (3921601)CaDiCaL version: 2.1.3
% 24.18/4.30 % (3921601)Termination reason: Instruction limit
% 26.38/4.81 % (3921601)Termination phase: Saturation
% 26.38/4.81 % (3921601)Time elapsed: 0.572 s
% 26.38/4.81 % (3921601)Peak memory usage: 100 MB
% 26.38/4.81 % (3921601)Instructions burned: 2067 (million)
% 26.38/4.81 % (3921610)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 26.38/4.81 % (3921610)------------------------------
% 26.38/4.81 % (3921610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.38/4.81 % (3921610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.38/4.81 % (3921610)CaDiCaL version: 2.1.3
% 26.38/4.81 % (3921610)Termination reason: Unknown
% 26.38/4.81 % (3921610)Termination phase: Saturation
% 26.38/4.81 % (3921610)Time elapsed: 0.363 s
% 26.38/4.81 % (3921610)Peak memory usage: 113 MB
% 26.38/4.81 % (3921610)Instructions burned: 542 (million)
% 26.38/4.81 % (3921618)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=558587397:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2977 on theBenchmark for (2977ds/11145Mi)
% 26.38/4.81 % (3921620)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1514632161:st=2:s2a=on:i=524:s2at=2:ss=axioms_2977 on theBenchmark for (2977ds/524Mi)
% 26.38/4.81 % (3921619)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=4226279241:cts=off:i=3034:av=off:er=known:fsd=on_2977 on theBenchmark for (2977ds/3034Mi)
% 26.38/4.81 % (3921616)Instruction limit reached!
% 26.38/4.81 % (3921616)------------------------------
% 26.38/4.81 % (3921616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.38/4.81 % (3921616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.38/4.81 % (3921616)CaDiCaL version: 2.1.3
% 26.38/4.81 % (3921616)Termination reason: Instruction limit
% 26.38/4.81 % (3921616)Termination phase: Saturation
% 26.38/4.81 % (3921616)Time elapsed: 0.253 s
% 26.38/4.81 % (3921616)Peak memory usage: 91 MB
% 26.38/4.81 % (3921616)Instructions burned: 441 (million)
% 26.38/4.81 % (3921621)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=587326121:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2976 on theBenchmark for (2976ds/1016Mi)
% 26.38/4.81 % (3921620)Instruction limit reached!
% 26.38/4.81 % (3921620)------------------------------
% 26.38/4.81 % (3921620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.38/4.81 % (3921620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.38/4.81 % (3921620)CaDiCaL version: 2.1.3
% 26.38/4.81 % (3921620)Termination reason: Instruction limit
% 26.38/4.81 % (3921620)Termination phase: Saturation
% 26.38/4.81 % (3921620)Time elapsed: 0.157 s
% 26.38/4.81 % (3921620)Peak memory usage: 91 MB
% 26.38/4.81 % (3921620)Instructions burned: 524 (million)
% 26.38/4.81 % (3921625)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=166644009:i=14123:bd=preordered:ins=4_2975 on theBenchmark for (2975ds/14123Mi)
% 26.38/4.81 % (3921627)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=681717696:i=5781:kws=precedence:bd=all:rawr=on_2974 on theBenchmark for (2974ds/5781Mi)
% 26.38/4.81 % (3921618)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 26.38/4.81 % (3921618)------------------------------
% 26.38/4.81 % (3921618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.38/4.81 % (3921618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.38/4.81 % (3921618)CaDiCaL version: 2.1.3
% 26.38/4.81 % (3921618)Termination reason: Unknown
% 26.38/4.81 % (3921618)Termination phase: Saturation
% 26.38/4.81 % (3921618)Time elapsed: 0.361 s
% 26.38/4.81 % (3921618)Peak memory usage: 114 MB
% 26.38/4.81 % (3921618)Instructions burned: 541 (million)
% 26.38/4.81 % (3921619)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 26.38/4.81 % (3921619)------------------------------
% 26.38/4.81 % (3921619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.38/4.81 % (3921619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.38/4.81 % (3921619)CaDiCaL version: 2.1.3
% 26.38/4.81 % (3921619)Termination reason: Unknown
% 26.38/4.81 % (3921619)Termination phase: Saturation
% 26.38/4.81 % (3921619)Time elapsed: 0.359 s
% 26.38/4.81 % (3921619)Peak memory usage: 113 MB
% 26.38/4.81 % (3921619)Instructions burned: 541 (million)
% 26.38/4.81 % (3921630)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=4161412281:i=2448:gtgl=5:bd=preordered:gtg=all_2972 on theBenchmark for (2972ds/2448Mi)
% 31.46/5.38 % (3921631)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2231430250:i=3223:kws=precedence:fgj=on:av=off_2972 on theBenchmark for (2972ds/3223Mi)
% 31.46/5.38 % (3921625)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.46/5.38 % (3921625)------------------------------
% 31.46/5.38 % (3921625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.46/5.38 % (3921625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.46/5.38 % (3921625)CaDiCaL version: 2.1.3
% 31.46/5.38 % (3921625)Termination reason: Unknown
% 31.46/5.38 % (3921625)Termination phase: Saturation
% 31.46/5.38 % (3921625)Time elapsed: 0.360 s
% 31.46/5.38 % (3921625)Peak memory usage: 113 MB
% 31.46/5.38 % (3921625)Instructions burned: 542 (million)
% 31.46/5.38 % (3921621)Instruction limit reached!
% 31.46/5.38 % (3921621)------------------------------
% 31.46/5.38 % (3921621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.46/5.38 % (3921621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.46/5.38 % (3921621)CaDiCaL version: 2.1.3
% 31.46/5.38 % (3921621)Termination reason: Instruction limit
% 31.46/5.38 % (3921621)Termination phase: Saturation
% 31.46/5.38 % (3921621)Time elapsed: 0.549 s
% 31.46/5.38 % (3921621)Peak memory usage: 98 MB
% 31.46/5.38 % (3921621)Instructions burned: 1017 (million)
% 31.46/5.38 % (3921634)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1811086995:st=5.6:i=2033:sd=3:ss=axioms_2970 on theBenchmark for (2970ds/2033Mi)
% 31.46/5.38 % (3921612)Instruction limit reached!
% 31.46/5.38 % (3921612)------------------------------
% 31.46/5.38 % (3921612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.46/5.38 % (3921612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.46/5.38 % (3921612)CaDiCaL version: 2.1.3
% 31.46/5.38 % (3921612)Termination reason: Instruction limit
% 31.46/5.38 % (3921612)Termination phase: Saturation
% 31.46/5.38 % (3921612)Time elapsed: 1.145 s
% 31.46/5.38 % (3921612)Peak memory usage: 98 MB
% 31.46/5.38 % (3921612)Instructions burned: 2481 (million)
% 31.46/5.38 % (3921635)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3522610609:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2968 on theBenchmark for (2968ds/2055Mi)
% 31.46/5.38 % (3921630)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.46/5.38 % (3921630)------------------------------
% 31.46/5.38 % (3921630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.46/5.38 % (3921630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.46/5.38 % (3921630)CaDiCaL version: 2.1.3
% 31.46/5.38 % (3921630)Termination reason: Unknown
% 31.46/5.38 % (3921630)Termination phase: Saturation
% 31.46/5.38 % (3921630)Time elapsed: 0.362 s
% 31.46/5.38 % (3921630)Peak memory usage: 113 MB
% 31.46/5.38 % (3921630)Instructions burned: 544 (million)
% 31.46/5.38 % (3921631)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.46/5.38 % (3921631)------------------------------
% 31.46/5.38 % (3921631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.46/5.38 % (3921631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.46/5.38 % (3921631)CaDiCaL version: 2.1.3
% 31.46/5.38 % (3921631)Termination reason: Unknown
% 31.46/5.38 % (3921631)Termination phase: Saturation
% 31.46/5.38 % (3921631)Time elapsed: 0.359 s
% 31.46/5.38 % (3921631)Peak memory usage: 113 MB
% 31.46/5.38 % (3921631)Instructions burned: 541 (million)
% 31.46/5.38 % (3921637)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=3778575290:i=21611:sd=3:ss=axioms_2968 on theBenchmark for (2968ds/21611Mi)
% 31.46/5.38 % (3921639)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=712522843:i=4835:sd=13:ss=axioms:sgt=23_2967 on theBenchmark for (2967ds/4835Mi)
% 31.46/5.38 % (3921640)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=310515357:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2967 on theBenchmark for (2967ds/797Mi)
% 31.46/5.38 % (3921640)Refutation not found, incomplete strategy
% 31.46/5.38 % (3921640)------------------------------
% 31.46/5.38 % (3921640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.46/5.38 % (3921640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.46/5.38 % (3921640)CaDiCaL version: 2.1.3
% 31.46/5.38 % (3921640)Termination reason: Refutation not found, incomplete strategy
% 31.46/5.38 % (3921640)Time elapsed: 0.014 s
% 31.46/5.38 % (3921640)Peak memory usage: 88 MB
% 31.46/5.38 % (3921640)Instructions burned: 23 (million)
% 31.46/5.38 % (3921634)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.46/5.38 % (3921634)------------------------------
% 31.46/5.38 % (3921634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.46/5.38 % (3921634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.46/5.38 % (3921634)CaDiCaL version: 2.1.3
% 31.46/5.38 % (3921634)Termination reason: Unknown
% 31.46/5.38 % (3921634)Termination phase: Saturation
% 31.46/5.38 % (3921634)Time elapsed: 0.362 s
% 31.46/5.38 % (3921634)Peak memory usage: 113 MB
% 31.46/5.39 % (3921634)Instructions burned: 542 (million)
% 31.46/5.39 % (3921635)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.46/5.39 % (3921635)------------------------------
% 31.46/5.39 % (3921635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.46/5.39 % (3921635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.46/5.39 % (3921635)CaDiCaL version: 2.1.3
% 31.46/5.39 % (3921635)Termination reason: Unknown
% 31.46/5.39 % (3921635)Termination phase: Saturation
% 31.46/5.39 % (3921635)Time elapsed: 0.365 s
% 31.46/5.39 % (3921635)Peak memory usage: 113 MB
% 31.46/5.39 % (3921635)Instructions burned: 541 (million)
% 31.46/5.39 % (3921644)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=386286629:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2964 on theBenchmark for (2964ds/2326Mi)
% 31.46/5.39 % (3921640)------------------------------
% 31.46/5.39 % (3921640)------------------------------
% 31.46/5.39 % (3921644)Refutation not found, incomplete strategy
% 31.46/5.39 % (3921644)------------------------------
% 31.46/5.39 % (3921644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.46/5.39 % (3921644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.46/5.39 % (3921644)CaDiCaL version: 2.1.3
% 31.46/5.39 % (3921644)Termination reason: Refutation not found, incomplete strategy
% 31.46/5.39 % (3921644)Time elapsed: 0.019 s
% 31.46/5.39 % (3921644)Peak memory usage: 89 MB
% 31.46/5.39 % (3921644)Instructions burned: 33 (million)
% 31.46/5.39 % (3921637)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.46/5.39 % (3921637)------------------------------
% 31.46/5.39 % (3921637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.46/5.39 % (3921637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.46/5.39 % (3921637)CaDiCaL version: 2.1.3
% 31.46/5.39 % (3921637)Termination reason: Unknown
% 31.46/5.39 % (3921637)Termination phase: Saturation
% 31.46/5.39 % (3921637)Time elapsed: 0.362 s
% 31.46/5.39 % (3921637)Peak memory usage: 113 MB
% 31.46/5.39 % (3921637)Instructions burned: 540 (million)
% 31.46/5.39 % (3921645)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1752628411:i=6038:nm=6_2963 on theBenchmark for (2963ds/6038Mi)
% 31.46/5.39 % (3921647)lrs+10_1_sil=32000:sp=occurrence:random_seed=1322943777:st=2:i=33334:sd=3:ss=included:sgt=32_2962 on theBenchmark for (2962ds/33334Mi)
% 31.46/5.39 % (3921604)Instruction limit reached!
% 31.46/5.39 % (3921604)------------------------------
% 31.46/5.39 % (3921604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.46/5.39 % (3921604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.46/5.39 % (3921604)CaDiCaL version: 2.1.3
% 31.46/5.39 % (3921604)Termination reason: Instruction limit
% 31.46/5.39 % (3921604)Termination phase: Saturation
% 31.46/5.39 % (3921604)Time elapsed: 2.018 s
% 31.46/5.39 % (3921604)Peak memory usage: 109 MB
% 31.46/5.39 % (3921604)Instructions burned: 3706 (million)
% 31.46/5.39 % (3921648)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=866556156:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2962 on theBenchmark for (2962ds/1008Mi)
% 31.46/5.39 % (3921644)------------------------------
% 31.46/5.39 % (3921644)------------------------------
% 31.46/5.39 % (3921651)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=2494245146:i=8327:s2at=5:bd=preordered_2961 on theBenchmark for (2961ds/8327Mi)
% 31.46/5.39 % (3921653)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=4039228518:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2960 on theBenchmark for (2960ds/1083Mi)
% 31.46/5.39 % (3921645)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.46/5.39 % (3921645)------------------------------
% 31.46/5.39 % (3921645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.46/5.39 % (3921645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.46/5.39 % (3921645)CaDiCaL version: 2.1.3
% 31.46/5.39 % (3921645)Termination reason: Unknown
% 31.46/5.39 % (3921645)Termination phase: Saturation
% 31.46/5.39 % (3921645)Time elapsed: 0.363 s
% 31.46/5.39 % (3921645)Peak memory usage: 113 MB
% 31.46/5.39 % (3921645)Instructions burned: 542 (million)
% 31.46/5.39 % (3921656)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2420072249:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2958 on theBenchmark for (2958ds/1084Mi)
% 31.46/5.39 % (3921627)First to succeed.
% 31.46/5.39 % (3921627)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3921529"
% 31.46/5.39 % (3921651)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.46/5.39 % (3921651)------------------------------
% 31.46/5.39 % (3921651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.46/5.39 % (3921651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.46/5.39 % (3921651)CaDiCaL version: 2.1.3
% 31.46/5.39 % (3921651)Termination reason: Unknown
% 31.46/5.39 % (3921651)Termination phase: Saturation
% 31.46/5.39 % (3921651)Time elapsed: 0.361 s
% 31.46/5.39 % (3921651)Peak memory usage: 113 MB
% 31.46/5.39 % (3921651)Instructions burned: 542 (million)
% 31.46/5.39 % (3921648)Instruction limit reached!
% 31.46/5.39 % (3921648)------------------------------
% 31.46/5.39 % (3921648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.46/5.39 % (3921648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.46/5.39 % (3921648)CaDiCaL version: 2.1.3
% 31.46/5.39 % (3921648)Termination reason: Instruction limit
% 31.46/5.39 % (3921648)Termination phase: Saturation
% 31.46/5.39 % (3921648)Time elapsed: 0.518 s
% 31.46/5.39 % (3921648)Peak memory usage: 98 MB
% 31.46/5.39 % (3921648)Instructions burned: 1010 (million)
% 31.46/5.39 % (3921627)Refutation found. Thanks to Tanya!
% 31.46/5.39 % SZS status Theorem for theBenchmark
% 31.46/5.39 % SZS output start Proof for theBenchmark
% See solution above
% 32.44/5.49 % (3921627)------------------------------
% 32.44/5.49 % (3921627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.44/5.49 % (3921627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.44/5.49 % (3921627)CaDiCaL version: 2.1.3
% 32.44/5.49 % (3921627)Termination reason: Refutation
% 32.44/5.49 % (3921627)Time elapsed: 1.674 s
% 32.44/5.49 % (3921627)Peak memory usage: 120 MB
% 32.44/5.49 % (3921627)Instructions burned: 5434 (million)
% 32.44/5.49 % (3921627)------------------------------
% 32.44/5.49 % (3921627)------------------------------
% 32.44/5.49 % (3921529)Success in time 4.519 s
% 32.44/5.49 % Vampire exiting
%------------------------------------------------------------------------------