%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM984_5 : TPTP v9.3.1. Released v6.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:45 PM UTC 2026
% Result : Theorem 122.07s 20.48s
% Output : Refutation 139.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 24
% Syntax : Number of formulae : 176 ( 152 unt; 0 typ; 0 def)
% Number of atoms : 200 ( 173 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 65 ( 41 ~; 18 |; 0 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of FOOLs : 1 ( 1 fml; 0 var)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 13 con; 0-3 aty)
% Number of variables : 330 ( 330 !; 0 ?; 330 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
bool: $tType ).
tff(type_def_6,type,
int: $tType ).
tff(type_def_7,type,
nat: $tType ).
tff(func_def_0,type,
minus_minus:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_1,type,
one_one:
!>[X0: $tType] : X0 ).
tff(func_def_2,type,
plus_plus:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_3,type,
times_times:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_4,type,
zero_zero:
!>[X0: $tType] : X0 ).
tff(func_def_5,type,
bit0: int > int ).
tff(func_def_6,type,
bit1: int > int ).
tff(func_def_7,type,
pls: int ).
tff(func_def_8,type,
number_number_of:
!>[X0: $tType] : ( int > X0 ) ).
tff(func_def_9,type,
semiring_1_of_nat:
!>[X0: $tType] : ( nat > X0 ) ).
tff(func_def_10,type,
power_power:
!>[X0: $tType] : ( ( X0 * nat ) > X0 ) ).
tff(func_def_11,type,
fFalse: bool ).
tff(func_def_12,type,
fTrue: bool ).
tff(func_def_13,type,
m: int ).
tff(func_def_14,type,
n: nat ).
tff(func_def_15,type,
r: int ).
tff(func_def_16,type,
sa: int ).
tff(func_def_17,type,
v: int ).
tff(func_def_18,type,
w: int ).
tff(func_def_19,type,
x: int ).
tff(func_def_20,type,
y: int ).
tff(func_def_21,type,
sK0: int ).
tff(func_def_22,type,
sK1: int ).
tff(pred_def_1,type,
number:
!>[X0: $tType] : $o ).
tff(pred_def_2,type,
ring:
!>[X0: $tType] : $o ).
tff(pred_def_3,type,
semiring:
!>[X0: $tType] : $o ).
tff(pred_def_4,type,
number_ring:
!>[X0: $tType] : $o ).
tff(pred_def_5,type,
ring_char_0:
!>[X0: $tType] : $o ).
tff(pred_def_6,type,
semiring_1:
!>[X0: $tType] : $o ).
tff(pred_def_7,type,
monoid_mult:
!>[X0: $tType] : $o ).
tff(pred_def_8,type,
number_semiring:
!>[X0: $tType] : $o ).
tff(pred_def_9,type,
zprime: int > $o ).
tff(pred_def_10,type,
ord_less:
!>[X0: $tType] : ( ( X0 * X0 ) > $o ) ).
tff(pred_def_11,type,
twoSqu1567020053sum2sq: int > $o ).
tff(pred_def_12,type,
pp: bool > $o ).
tff(f10,axiom,
! [X0: int,X1: int] : ( power_power(int,minus_minus(int,X1,X0),number_number_of(nat,bit0(bit1(pls)))) = plus_plus(int,minus_minus(int,power_power(int,X1,number_number_of(nat,bit0(bit1(pls)))),times_times(int,times_times(int,number_number_of(int,bit0(bit1(pls))),X1),X0)),power_power(int,X0,number_number_of(nat,bit0(bit1(pls))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9_zdiff__power2) ).
tff(f12,axiom,
! [X0: $tType] :
( number_ring(X0)
=> ! [X1: X0,X2: X0] : ( power_power(X0,minus_minus(X0,X2,X1),number_number_of(nat,bit0(bit1(pls)))) = minus_minus(X0,plus_plus(X0,power_power(X0,X2,number_number_of(nat,bit0(bit1(pls)))),power_power(X0,X1,number_number_of(nat,bit0(bit1(pls))))),times_times(X0,times_times(X0,number_number_of(X0,bit0(bit1(pls))),X2),X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_11_power2__diff) ).
tff(f23,axiom,
! [X0: int] : ( times_times(int,pls,X0) = pls ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_22_mult__Pls) ).
tff(f25,axiom,
! [X0: int,X1: int] : ( plus_plus(int,bit0(X1),bit0(X0)) = bit0(plus_plus(int,X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_24_add__Bit0__Bit0) ).
tff(f26,axiom,
! [X0: int,X1: int] : ( minus_minus(int,bit0(X1),bit0(X0)) = bit0(minus_minus(int,X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_25_diff__bin__simps_I7_J) ).
tff(f31,axiom,
! [X0: $tType] :
( number_ring(X0)
=> ! [X1: X0,X2: int,X3: int] : ( times_times(X0,number_number_of(X0,X3),times_times(X0,number_number_of(X0,X2),X1)) = times_times(X0,number_number_of(X0,times_times(int,X3,X2)),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_30_mult__number__of__left) ).
tff(f33,axiom,
! [X0: $tType] :
( number_ring(X0)
=> ! [X1: X0,X2: int,X3: int] : ( plus_plus(X0,number_number_of(X0,X3),plus_plus(X0,number_number_of(X0,X2),X1)) = plus_plus(X0,number_number_of(X0,plus_plus(int,X3,X2)),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_32_add__number__of__left) ).
tff(f38,axiom,
! [X0: int,X1: int] : ( minus_minus(int,bit1(X1),bit1(X0)) = bit0(minus_minus(int,X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_37_diff__bin__simps_I10_J) ).
tff(f41,axiom,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,bit0(bit1(pls))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_40_nat__1__add__1) ).
tff(f56,axiom,
! [X0: int] : ( number_number_of(int,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_55_number__of__is__id) ).
tff(f59,axiom,
! [X0: int] : ( plus_plus(int,X0,pls) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_58_add__Pls__right) ).
tff(f60,axiom,
! [X0: int] : ( plus_plus(int,pls,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_59_add__Pls) ).
tff(f61,axiom,
! [X0: int] : ( bit0(X0) = plus_plus(int,X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_60_Bit0__def) ).
tff(f63,axiom,
! [X0: int] : ( minus_minus(int,X0,pls) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_62_diff__bin__simps_I1_J) ).
tff(f65,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/sandbox2/benchmark/theBenchmark.p',fact_64_int__distrib_I2_J) ).
tff(f67,axiom,
! [X0: int,X1: int,X2: int] : ( times_times(int,minus_minus(int,X2,X1),X0) = minus_minus(int,times_times(int,X2,X0),times_times(int,X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_66_int__distrib_I3_J) ).
tff(f68,axiom,
! [X0: int,X1: int,X2: int] : ( times_times(int,X2,minus_minus(int,X1,X0)) = minus_minus(int,times_times(int,X2,X1),times_times(int,X2,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_67_int__distrib_I4_J) ).
tff(f74,axiom,
! [X0: int] : ( bit1(X0) = plus_plus(int,plus_plus(int,one_one(int),X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_73_Bit1__def) ).
tff(f77,axiom,
! [X0: $tType] :
( number_ring(X0)
=> ! [X1: X0] : ( times_times(X0,number_number_of(X0,bit1(pls)),X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_76_mult__numeral__1) ).
tff(f78,axiom,
! [X0: $tType] :
( number_ring(X0)
=> ! [X1: X0] : ( times_times(X0,X1,number_number_of(X0,bit1(pls))) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_77_mult__numeral__1__right) ).
tff(f81,axiom,
! [X0: $tType] :
( number_ring(X0)
=> ! [X1: X0,X2: int,X3: int] : ( plus_plus(X0,number_number_of(X0,X3),minus_minus(X0,number_number_of(X0,X2),X1)) = minus_minus(X0,number_number_of(X0,plus_plus(int,X3,X2)),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_80_add__number__of__diff1) ).
tff(f82,axiom,
one_one(int) = number_number_of(int,bit1(pls)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_81_one__is__num__one) ).
tff(f103,axiom,
number_ring(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Int_Oint___Int_Onumber__ring) ).
tff(f114,conjecture,
plus_plus(int,power_power(int,minus_minus(int,x,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,bit0(bit1(pls)))),power_power(int,minus_minus(int,y,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,plus_plus(int,minus_minus(int,minus_minus(int,plus_plus(int,power_power(int,x,number_number_of(nat,bit0(bit1(pls)))),power_power(int,y,number_number_of(nat,bit0(bit1(pls))))),times_times(int,times_times(int,number_number_of(int,bit0(bit1(pls))),x),times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),times_times(int,times_times(int,number_number_of(int,bit0(bit1(pls))),y),times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),power_power(int,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,bit0(bit1(pls))))),power_power(int,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,bit0(bit1(pls))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
tff(f115,negated_conjecture,
( ( ~ plus_plus(int,power_power(int,minus_minus(int,x,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,bit0(bit1(pls)))),power_power(int,minus_minus(int,y,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,bit0(bit1(pls))))) ) = plus_plus(int,plus_plus(int,minus_minus(int,minus_minus(int,plus_plus(int,power_power(int,x,number_number_of(nat,bit0(bit1(pls)))),power_power(int,y,number_number_of(nat,bit0(bit1(pls))))),times_times(int,times_times(int,number_number_of(int,bit0(bit1(pls))),x),times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),times_times(int,times_times(int,number_number_of(int,bit0(bit1(pls))),y),times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),power_power(int,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,bit0(bit1(pls))))),power_power(int,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,bit0(bit1(pls))))) ),
inference(negated_conjecture,[status(cth)],[f114]) ).
tff(f116,plain,
plus_plus(int,power_power(int,minus_minus(int,x,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,bit0(bit1(pls)))),power_power(int,minus_minus(int,y,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,plus_plus(int,minus_minus(int,minus_minus(int,plus_plus(int,power_power(int,x,number_number_of(nat,bit0(bit1(pls)))),power_power(int,y,number_number_of(nat,bit0(bit1(pls))))),times_times(int,times_times(int,number_number_of(int,bit0(bit1(pls))),x),times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),times_times(int,times_times(int,number_number_of(int,bit0(bit1(pls))),y),times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),power_power(int,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,bit0(bit1(pls))))),power_power(int,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,bit0(bit1(pls))))),
inference(flattening,[],[f115]) ).
tff(f126,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0] : ( power_power(X0,minus_minus(X0,X2,X1),number_number_of(nat,bit0(bit1(pls)))) = minus_minus(X0,plus_plus(X0,power_power(X0,X2,number_number_of(nat,bit0(bit1(pls)))),power_power(X0,X1,number_number_of(nat,bit0(bit1(pls))))),times_times(X0,times_times(X0,number_number_of(X0,bit0(bit1(pls))),X2),X1)) )
| ~ number_ring(X0) ),
inference(ennf_transformation,[],[f12]) ).
tff(f137,plain,
! [X0: $tType] :
( ! [X1: X0,X2: int,X3: int] : ( times_times(X0,number_number_of(X0,X3),times_times(X0,number_number_of(X0,X2),X1)) = times_times(X0,number_number_of(X0,times_times(int,X3,X2)),X1) )
| ~ number_ring(X0) ),
inference(ennf_transformation,[],[f31]) ).
tff(f139,plain,
! [X0: $tType] :
( ! [X1: X0,X2: int,X3: int] : ( plus_plus(X0,number_number_of(X0,X3),plus_plus(X0,number_number_of(X0,X2),X1)) = plus_plus(X0,number_number_of(X0,plus_plus(int,X3,X2)),X1) )
| ~ number_ring(X0) ),
inference(ennf_transformation,[],[f33]) ).
tff(f151,plain,
! [X0: $tType] :
( ! [X1: X0] : ( times_times(X0,number_number_of(X0,bit1(pls)),X1) = X1 )
| ~ number_ring(X0) ),
inference(ennf_transformation,[],[f77]) ).
tff(f152,plain,
! [X0: $tType] :
( ! [X1: X0] : ( times_times(X0,X1,number_number_of(X0,bit1(pls))) = X1 )
| ~ number_ring(X0) ),
inference(ennf_transformation,[],[f78]) ).
tff(f155,plain,
! [X0: $tType] :
( ! [X1: X0,X2: int,X3: int] : ( plus_plus(X0,number_number_of(X0,X3),minus_minus(X0,number_number_of(X0,X2),X1)) = minus_minus(X0,number_number_of(X0,plus_plus(int,X3,X2)),X1) )
| ~ number_ring(X0) ),
inference(ennf_transformation,[],[f81]) ).
tff(f183,plain,
! [X0: int,X1: int] : ( power_power(int,minus_minus(int,X1,X0),number_number_of(nat,bit0(bit1(pls)))) = plus_plus(int,minus_minus(int,power_power(int,X1,number_number_of(nat,bit0(bit1(pls)))),times_times(int,times_times(int,number_number_of(int,bit0(bit1(pls))),X1),X0)),power_power(int,X0,number_number_of(nat,bit0(bit1(pls))))) ),
inference(cnf_transformation,[],[f10]) ).
tff(f185,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ( power_power(X0,minus_minus(X0,X2,X1),number_number_of(nat,bit0(bit1(pls)))) = minus_minus(X0,plus_plus(X0,power_power(X0,X2,number_number_of(nat,bit0(bit1(pls)))),power_power(X0,X1,number_number_of(nat,bit0(bit1(pls))))),times_times(X0,times_times(X0,number_number_of(X0,bit0(bit1(pls))),X2),X1)) )
| ~ number_ring(X0) ),
inference(cnf_transformation,[],[f126]) ).
tff(f201,plain,
! [X0: int] : ( pls = times_times(int,pls,X0) ),
inference(cnf_transformation,[],[f23]) ).
tff(f203,plain,
! [X0: int,X1: int] : ( plus_plus(int,bit0(X1),bit0(X0)) = bit0(plus_plus(int,X1,X0)) ),
inference(cnf_transformation,[],[f25]) ).
tff(f204,plain,
! [X0: int,X1: int] : ( minus_minus(int,bit0(X1),bit0(X0)) = bit0(minus_minus(int,X1,X0)) ),
inference(cnf_transformation,[],[f26]) ).
tff(f209,plain,
! [X0: $tType,X2: int,X3: int,X1: X0] :
( ~ number_ring(X0)
| ( times_times(X0,number_number_of(X0,X3),times_times(X0,number_number_of(X0,X2),X1)) = times_times(X0,number_number_of(X0,times_times(int,X3,X2)),X1) ) ),
inference(cnf_transformation,[],[f137]) ).
tff(f211,plain,
! [X0: $tType,X2: int,X3: int,X1: X0] :
( ~ number_ring(X0)
| ( plus_plus(X0,number_number_of(X0,X3),plus_plus(X0,number_number_of(X0,X2),X1)) = plus_plus(X0,number_number_of(X0,plus_plus(int,X3,X2)),X1) ) ),
inference(cnf_transformation,[],[f139]) ).
tff(f216,plain,
! [X0: int,X1: int] : ( bit0(minus_minus(int,X1,X0)) = minus_minus(int,bit1(X1),bit1(X0)) ),
inference(cnf_transformation,[],[f38]) ).
tff(f219,plain,
number_number_of(nat,bit0(bit1(pls))) = plus_plus(nat,one_one(nat),one_one(nat)),
inference(cnf_transformation,[],[f41]) ).
tff(f234,plain,
! [X0: int] : ( number_number_of(int,X0) = X0 ),
inference(cnf_transformation,[],[f56]) ).
tff(f238,plain,
! [X0: int] : ( plus_plus(int,X0,pls) = X0 ),
inference(cnf_transformation,[],[f59]) ).
tff(f239,plain,
! [X0: int] : ( plus_plus(int,pls,X0) = X0 ),
inference(cnf_transformation,[],[f60]) ).
tff(f240,plain,
! [X0: int] : ( bit0(X0) = plus_plus(int,X0,X0) ),
inference(cnf_transformation,[],[f61]) ).
tff(f242,plain,
! [X0: int] : ( minus_minus(int,X0,pls) = X0 ),
inference(cnf_transformation,[],[f63]) ).
tff(f244,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,[],[f65]) ).
tff(f246,plain,
! [X2: int,X0: int,X1: int] : ( times_times(int,minus_minus(int,X2,X1),X0) = minus_minus(int,times_times(int,X2,X0),times_times(int,X1,X0)) ),
inference(cnf_transformation,[],[f67]) ).
tff(f247,plain,
! [X2: int,X0: int,X1: int] : ( times_times(int,X2,minus_minus(int,X1,X0)) = minus_minus(int,times_times(int,X2,X1),times_times(int,X2,X0)) ),
inference(cnf_transformation,[],[f68]) ).
tff(f253,plain,
! [X0: int] : ( bit1(X0) = plus_plus(int,plus_plus(int,one_one(int),X0),X0) ),
inference(cnf_transformation,[],[f74]) ).
tff(f256,plain,
! [X0: $tType,X1: X0] :
( ( times_times(X0,number_number_of(X0,bit1(pls)),X1) = X1 )
| ~ number_ring(X0) ),
inference(cnf_transformation,[],[f151]) ).
tff(f257,plain,
! [X0: $tType,X1: X0] :
( ( times_times(X0,X1,number_number_of(X0,bit1(pls))) = X1 )
| ~ number_ring(X0) ),
inference(cnf_transformation,[],[f152]) ).
tff(f260,plain,
! [X0: $tType,X2: int,X3: int,X1: X0] :
( ~ number_ring(X0)
| ( plus_plus(X0,number_number_of(X0,X3),minus_minus(X0,number_number_of(X0,X2),X1)) = minus_minus(X0,number_number_of(X0,plus_plus(int,X3,X2)),X1) ) ),
inference(cnf_transformation,[],[f155]) ).
tff(f261,plain,
one_one(int) = number_number_of(int,bit1(pls)),
inference(cnf_transformation,[],[f82]) ).
tff(f282,plain,
number_ring(int),
inference(cnf_transformation,[],[f103]) ).
tff(f293,plain,
plus_plus(int,power_power(int,minus_minus(int,x,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,bit0(bit1(pls)))),power_power(int,minus_minus(int,y,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,plus_plus(int,minus_minus(int,minus_minus(int,plus_plus(int,power_power(int,x,number_number_of(nat,bit0(bit1(pls)))),power_power(int,y,number_number_of(nat,bit0(bit1(pls))))),times_times(int,times_times(int,number_number_of(int,bit0(bit1(pls))),x),times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),times_times(int,times_times(int,number_number_of(int,bit0(bit1(pls))),y),times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),power_power(int,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,bit0(bit1(pls))))),power_power(int,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,bit0(bit1(pls))))),
inference(cnf_transformation,[],[f116]) ).
tff(f303,plain,
! [X0: int,X1: int] : ( power_power(int,minus_minus(int,X1,X0),number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))) = plus_plus(int,minus_minus(int,power_power(int,X1,number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls))),X1),X0)),power_power(int,X0,number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls))))) ),
inference(definition_unfolding,[],[f183,f240,f253,f240,f253,f240,f253,f240,f253]) ).
tff(f305,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ( power_power(X0,minus_minus(X0,X2,X1),number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))) = minus_minus(X0,plus_plus(X0,power_power(X0,X2,number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))),power_power(X0,X1,number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls))))),times_times(X0,times_times(X0,number_number_of(X0,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls))),X2),X1)) )
| ~ number_ring(X0) ),
inference(definition_unfolding,[],[f185,f240,f253,f240,f253,f240,f253,f240,f253]) ).
tff(f320,plain,
! [X0: int,X1: int] : ( plus_plus(int,plus_plus(int,X1,X1),plus_plus(int,X0,X0)) = plus_plus(int,plus_plus(int,X1,X0),plus_plus(int,X1,X0)) ),
inference(definition_unfolding,[],[f203,f240,f240,f240]) ).
tff(f321,plain,
! [X0: int,X1: int] : ( minus_minus(int,plus_plus(int,X1,X1),plus_plus(int,X0,X0)) = plus_plus(int,minus_minus(int,X1,X0),minus_minus(int,X1,X0)) ),
inference(definition_unfolding,[],[f204,f240,f240,f240]) ).
tff(f325,plain,
! [X0: int,X1: int] : ( plus_plus(int,minus_minus(int,X1,X0),minus_minus(int,X1,X0)) = minus_minus(int,plus_plus(int,plus_plus(int,one_one(int),X1),X1),plus_plus(int,plus_plus(int,one_one(int),X0),X0)) ),
inference(definition_unfolding,[],[f216,f240,f253,f253]) ).
tff(f328,plain,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls))),
inference(definition_unfolding,[],[f219,f240,f253]) ).
tff(f335,plain,
! [X0: $tType,X1: X0] :
( ~ number_ring(X0)
| ( times_times(X0,number_number_of(X0,plus_plus(int,plus_plus(int,one_one(int),pls),pls)),X1) = X1 ) ),
inference(definition_unfolding,[],[f256,f253]) ).
tff(f336,plain,
! [X0: $tType,X1: X0] :
( ~ number_ring(X0)
| ( times_times(X0,X1,number_number_of(X0,plus_plus(int,plus_plus(int,one_one(int),pls),pls))) = X1 ) ),
inference(definition_unfolding,[],[f257,f253]) ).
tff(f339,plain,
one_one(int) = number_number_of(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls)),
inference(definition_unfolding,[],[f261,f253]) ).
tff(f356,plain,
plus_plus(int,power_power(int,minus_minus(int,x,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))),power_power(int,minus_minus(int,y,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls))))) != plus_plus(int,plus_plus(int,minus_minus(int,minus_minus(int,plus_plus(int,power_power(int,x,number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))),power_power(int,y,number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls))))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls))),x),times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls))),y),times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),power_power(int,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls))))),power_power(int,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls))))),
inference(definition_unfolding,[],[f293,f240,f253,f240,f253,f240,f253,f240,f253,f240,f253,f240,f253,f240,f253,f240,f253]) ).
tff(f370,plain,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls))),
inference(forward_demodulation,[],[f328,f238]) ).
tff(f372,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ( power_power(X0,minus_minus(X0,X2,X1),number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls)))) = minus_minus(X0,plus_plus(X0,power_power(X0,X2,number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls)))),power_power(X0,X1,number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls))))),times_times(X0,times_times(X0,number_number_of(X0,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls))),X2),X1)) )
| ~ number_ring(X0) ),
inference(forward_demodulation,[],[f305,f238]) ).
tff(f374,plain,
! [X0: int,X1: int] : ( power_power(int,minus_minus(int,X1,X0),number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls)))) = plus_plus(int,minus_minus(int,power_power(int,X1,number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls)))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls))),X1),X0)),power_power(int,X0,number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls))))) ),
inference(forward_demodulation,[],[f303,f238]) ).
tff(f387,plain,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,plus_plus(int,one_one(int),one_one(int))),
inference(forward_demodulation,[],[f370,f238]) ).
tff(f389,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ( power_power(X0,minus_minus(X0,X2,X1),number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))) = minus_minus(X0,plus_plus(X0,power_power(X0,X2,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),power_power(X0,X1,number_number_of(nat,plus_plus(int,one_one(int),one_one(int))))),times_times(X0,times_times(X0,number_number_of(X0,plus_plus(int,one_one(int),one_one(int))),X2),X1)) )
| ~ number_ring(X0) ),
inference(forward_demodulation,[],[f372,f238]) ).
tff(f391,plain,
! [X0: int,X1: int] : ( power_power(int,minus_minus(int,X1,X0),number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))) = plus_plus(int,minus_minus(int,power_power(int,X1,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),X1),X0)),power_power(int,X0,number_number_of(nat,plus_plus(int,one_one(int),one_one(int))))) ),
inference(forward_demodulation,[],[f374,f238]) ).
tff(f399,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ~ number_ring(X0)
| ( power_power(X0,minus_minus(X0,X2,X1),plus_plus(nat,one_one(nat),one_one(nat))) = minus_minus(X0,plus_plus(X0,power_power(X0,X2,plus_plus(nat,one_one(nat),one_one(nat))),power_power(X0,X1,plus_plus(nat,one_one(nat),one_one(nat)))),times_times(X0,times_times(X0,number_number_of(X0,plus_plus(int,one_one(int),one_one(int))),X2),X1)) ) ),
inference(forward_demodulation,[],[f389,f387]) ).
tff(f401,plain,
! [X0: int,X1: int] : ( power_power(int,minus_minus(int,X1,X0),plus_plus(nat,one_one(nat),one_one(nat))) = plus_plus(int,minus_minus(int,power_power(int,X1,plus_plus(nat,one_one(nat),one_one(nat))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),X1),X0)),power_power(int,X0,plus_plus(nat,one_one(nat),one_one(nat)))) ),
inference(forward_demodulation,[],[f391,f387]) ).
tff(f407,plain,
! [X0: int,X1: int] : ( power_power(int,minus_minus(int,X1,X0),plus_plus(nat,one_one(nat),one_one(nat))) = plus_plus(int,minus_minus(int,power_power(int,X1,plus_plus(nat,one_one(nat),one_one(nat))),times_times(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),X1),X0)),power_power(int,X0,plus_plus(nat,one_one(nat),one_one(nat)))) ),
inference(forward_demodulation,[],[f401,f234]) ).
tff(f604,plain,
! [X0: int] : ( times_times(int,number_number_of(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls)),X0) = X0 ),
inference(resolution,[],[f335,f282]) ).
tff(f605,plain,
! [X0: int] : ( times_times(int,one_one(int),X0) = X0 ),
inference(forward_demodulation,[],[f604,f339]) ).
tff(f606,plain,
! [X0: int] : ( times_times(int,X0,number_number_of(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls))) = X0 ),
inference(resolution,[],[f336,f282]) ).
tff(f607,plain,
! [X0: int] : ( times_times(int,X0,one_one(int)) = X0 ),
inference(forward_demodulation,[],[f606,f339]) ).
tff(f681,plain,
! [X0: int,X1: int] : ( times_times(int,X0,plus_plus(int,one_one(int),X1)) = plus_plus(int,X0,times_times(int,X0,X1)) ),
inference(superposition,[],[f244,f607]) ).
tff(f752,plain,
! [X0: int,X1: int] : ( times_times(int,minus_minus(int,X0,X0),X1) = times_times(int,X0,minus_minus(int,X1,X1)) ),
inference(superposition,[],[f246,f247]) ).
tff(f1068,plain,
! [X2: int,X0: int,X1: int] : ( times_times(int,number_number_of(int,X0),times_times(int,number_number_of(int,X1),X2)) = times_times(int,number_number_of(int,times_times(int,X0,X1)),X2) ),
inference(resolution,[],[f209,f282]) ).
tff(f1069,plain,
! [X2: int,X0: int,X1: int] : ( times_times(int,number_number_of(int,X0),times_times(int,number_number_of(int,X1),X2)) = times_times(int,times_times(int,X0,X1),X2) ),
inference(forward_demodulation,[],[f1068,f234]) ).
tff(f1070,plain,
! [X2: int,X0: int,X1: int] : ( times_times(int,times_times(int,X0,X1),X2) = times_times(int,number_number_of(int,X0),times_times(int,X1,X2)) ),
inference(forward_demodulation,[],[f1069,f234]) ).
tff(f1071,plain,
! [X2: int,X0: int,X1: int] : ( times_times(int,times_times(int,X0,X1),X2) = times_times(int,X0,times_times(int,X1,X2)) ),
inference(forward_demodulation,[],[f1070,f234]) ).
tff(f1096,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,number_number_of(int,X0),plus_plus(int,number_number_of(int,X1),X2)) = plus_plus(int,number_number_of(int,plus_plus(int,X0,X1)),X2) ),
inference(resolution,[],[f211,f282]) ).
tff(f1097,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,plus_plus(int,X0,X1),X2) = plus_plus(int,number_number_of(int,X0),plus_plus(int,number_number_of(int,X1),X2)) ),
inference(forward_demodulation,[],[f1096,f234]) ).
tff(f1098,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,plus_plus(int,X0,X1),X2) = plus_plus(int,number_number_of(int,X0),plus_plus(int,X1,X2)) ),
inference(forward_demodulation,[],[f1097,f234]) ).
tff(f1099,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,plus_plus(int,X0,X1),X2) = plus_plus(int,X0,plus_plus(int,X1,X2)) ),
inference(forward_demodulation,[],[f1098,f234]) ).
tff(f1131,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,number_number_of(int,X0),minus_minus(int,number_number_of(int,X1),X2)) = minus_minus(int,number_number_of(int,plus_plus(int,X0,X1)),X2) ),
inference(resolution,[],[f260,f282]) ).
tff(f1132,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,number_number_of(int,X0),minus_minus(int,number_number_of(int,X1),X2)) = minus_minus(int,plus_plus(int,X0,X1),X2) ),
inference(forward_demodulation,[],[f1131,f234]) ).
tff(f1133,plain,
! [X2: int,X0: int,X1: int] : ( minus_minus(int,plus_plus(int,X0,X1),X2) = plus_plus(int,number_number_of(int,X0),minus_minus(int,X1,X2)) ),
inference(forward_demodulation,[],[f1132,f234]) ).
tff(f1134,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,X0,minus_minus(int,X1,X2)) = minus_minus(int,plus_plus(int,X0,X1),X2) ),
inference(forward_demodulation,[],[f1133,f234]) ).
tff(f1183,plain,
plus_plus(int,power_power(int,minus_minus(int,x,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls)))),power_power(int,minus_minus(int,y,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls))))) != plus_plus(int,plus_plus(int,minus_minus(int,minus_minus(int,plus_plus(int,power_power(int,x,number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls)))),power_power(int,y,number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls))))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls))),x),times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls))),y),times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),power_power(int,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls))))),power_power(int,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls))))),
inference(superposition,[],[f356,f238]) ).
tff(f1184,plain,
plus_plus(int,power_power(int,minus_minus(int,x,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls)))),power_power(int,minus_minus(int,y,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls))))) != plus_plus(int,minus_minus(int,minus_minus(int,plus_plus(int,power_power(int,x,number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls)))),power_power(int,y,number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls))))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls))),x),times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls))),y),times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),plus_plus(int,power_power(int,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls)))),power_power(int,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,plus_plus(int,plus_plus(int,one_one(int),pls),plus_plus(int,one_one(int),pls)))))),
inference(forward_demodulation,[],[f1183,f1099]) ).
tff(f1187,plain,
plus_plus(int,power_power(int,minus_minus(int,x,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,plus_plus(int,one_one(int),plus_plus(int,pls,plus_plus(int,one_one(int),pls))))),power_power(int,minus_minus(int,y,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,plus_plus(int,one_one(int),plus_plus(int,pls,plus_plus(int,one_one(int),pls)))))) != plus_plus(int,minus_minus(int,minus_minus(int,plus_plus(int,power_power(int,x,number_number_of(nat,plus_plus(int,one_one(int),plus_plus(int,pls,plus_plus(int,one_one(int),pls))))),power_power(int,y,number_number_of(nat,plus_plus(int,one_one(int),plus_plus(int,pls,plus_plus(int,one_one(int),pls)))))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,pls,plus_plus(int,one_one(int),pls)))),x),times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,pls,plus_plus(int,one_one(int),pls)))),y),times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),plus_plus(int,power_power(int,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,plus_plus(int,one_one(int),plus_plus(int,pls,plus_plus(int,one_one(int),pls))))),power_power(int,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,plus_plus(int,one_one(int),plus_plus(int,pls,plus_plus(int,one_one(int),pls))))))),
inference(forward_demodulation,[],[f1184,f1099]) ).
tff(f1190,plain,
plus_plus(int,power_power(int,minus_minus(int,x,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,plus_plus(int,one_one(int),plus_plus(int,one_one(int),pls)))),power_power(int,minus_minus(int,y,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,plus_plus(int,one_one(int),plus_plus(int,one_one(int),pls))))) != plus_plus(int,minus_minus(int,minus_minus(int,plus_plus(int,power_power(int,x,number_number_of(nat,plus_plus(int,one_one(int),plus_plus(int,one_one(int),pls)))),power_power(int,y,number_number_of(nat,plus_plus(int,one_one(int),plus_plus(int,one_one(int),pls))))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),pls))),x),times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),pls))),y),times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),plus_plus(int,power_power(int,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,plus_plus(int,one_one(int),plus_plus(int,one_one(int),pls)))),power_power(int,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,plus_plus(int,one_one(int),plus_plus(int,one_one(int),pls)))))),
inference(forward_demodulation,[],[f1187,f239]) ).
tff(f1193,plain,
plus_plus(int,power_power(int,minus_minus(int,x,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),power_power(int,minus_minus(int,y,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),number_number_of(nat,plus_plus(int,one_one(int),one_one(int))))) != plus_plus(int,minus_minus(int,minus_minus(int,plus_plus(int,power_power(int,x,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),power_power(int,y,number_number_of(nat,plus_plus(int,one_one(int),one_one(int))))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),x),times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),y),times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),plus_plus(int,power_power(int,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),power_power(int,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))))),
inference(forward_demodulation,[],[f1190,f238]) ).
tff(f1196,plain,
plus_plus(int,power_power(int,minus_minus(int,x,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,minus_minus(int,y,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat)))) != plus_plus(int,minus_minus(int,minus_minus(int,plus_plus(int,power_power(int,x,plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,y,plus_plus(nat,one_one(nat),one_one(nat)))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),x),times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),y),times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),plus_plus(int,power_power(int,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,times_times(int,sa,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))))),
inference(forward_demodulation,[],[f1193,f387]) ).
tff(f1199,plain,
plus_plus(int,power_power(int,minus_minus(int,x,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,minus_minus(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat)))) != plus_plus(int,minus_minus(int,minus_minus(int,plus_plus(int,power_power(int,x,plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,y,plus_plus(nat,one_one(nat),one_one(nat)))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),x),times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),y),plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))))),plus_plus(int,power_power(int,times_times(int,r,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))))),
inference(forward_demodulation,[],[f1196,f681]) ).
tff(f1202,plain,
plus_plus(int,power_power(int,minus_minus(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,minus_minus(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat)))) != plus_plus(int,minus_minus(int,minus_minus(int,plus_plus(int,power_power(int,x,plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,y,plus_plus(nat,one_one(nat),one_one(nat)))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),x),plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),y),plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))))),plus_plus(int,power_power(int,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))))),
inference(forward_demodulation,[],[f1199,f681]) ).
tff(f1205,plain,
plus_plus(int,power_power(int,minus_minus(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,minus_minus(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat)))) != plus_plus(int,minus_minus(int,minus_minus(int,plus_plus(int,power_power(int,x,plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,y,plus_plus(nat,one_one(nat),one_one(nat)))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),x),plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))))),times_times(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),times_times(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))))),plus_plus(int,power_power(int,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))))),
inference(forward_demodulation,[],[f1202,f1071]) ).
tff(f1208,plain,
plus_plus(int,power_power(int,minus_minus(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,minus_minus(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat)))) != plus_plus(int,minus_minus(int,minus_minus(int,plus_plus(int,power_power(int,x,plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,y,plus_plus(nat,one_one(nat),one_one(nat)))),times_times(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),x),plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))))),times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))))),plus_plus(int,power_power(int,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))))),
inference(forward_demodulation,[],[f1205,f234]) ).
tff(f1211,plain,
plus_plus(int,power_power(int,minus_minus(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,minus_minus(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat)))) != plus_plus(int,minus_minus(int,minus_minus(int,plus_plus(int,power_power(int,x,plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,y,plus_plus(nat,one_one(nat),one_one(nat)))),times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n)))))),times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))))),plus_plus(int,power_power(int,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))))),
inference(forward_demodulation,[],[f1208,f1071]) ).
tff(f1788,plain,
! [X0: int] : ( plus_plus(int,minus_minus(int,X0,pls),minus_minus(int,X0,pls)) = minus_minus(int,plus_plus(int,plus_plus(int,one_one(int),X0),X0),plus_plus(int,one_one(int),pls)) ),
inference(superposition,[],[f325,f238]) ).
tff(f1791,plain,
! [X0: int] : ( plus_plus(int,minus_minus(int,X0,pls),minus_minus(int,X0,pls)) = minus_minus(int,plus_plus(int,plus_plus(int,one_one(int),X0),X0),one_one(int)) ),
inference(forward_demodulation,[],[f1788,f238]) ).
tff(f1800,plain,
! [X0: int] : ( plus_plus(int,minus_minus(int,X0,pls),minus_minus(int,X0,pls)) = minus_minus(int,plus_plus(int,one_one(int),plus_plus(int,X0,X0)),one_one(int)) ),
inference(forward_demodulation,[],[f1791,f1099]) ).
tff(f1809,plain,
! [X0: int] : ( minus_minus(int,plus_plus(int,X0,X0),plus_plus(int,pls,pls)) = minus_minus(int,plus_plus(int,one_one(int),plus_plus(int,X0,X0)),one_one(int)) ),
inference(forward_demodulation,[],[f1800,f321]) ).
tff(f1818,plain,
! [X0: int] : ( minus_minus(int,plus_plus(int,X0,X0),pls) = minus_minus(int,plus_plus(int,one_one(int),plus_plus(int,X0,X0)),one_one(int)) ),
inference(forward_demodulation,[],[f1809,f239]) ).
tff(f1825,plain,
! [X0: int] : ( plus_plus(int,X0,X0) = minus_minus(int,plus_plus(int,one_one(int),plus_plus(int,X0,X0)),one_one(int)) ),
inference(forward_demodulation,[],[f1818,f242]) ).
tff(f2443,plain,
! [X0: int,X1: int] : ( power_power(int,minus_minus(int,X0,X1),plus_plus(nat,one_one(nat),one_one(nat))) = minus_minus(int,plus_plus(int,power_power(int,X0,plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,X1,plus_plus(nat,one_one(nat),one_one(nat)))),times_times(int,times_times(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),X0),X1)) ),
inference(resolution,[],[f399,f282]) ).
tff(f2444,plain,
! [X0: int,X1: int] : ( power_power(int,minus_minus(int,X0,X1),plus_plus(nat,one_one(nat),one_one(nat))) = minus_minus(int,plus_plus(int,power_power(int,X0,plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,X1,plus_plus(nat,one_one(nat),one_one(nat)))),times_times(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),times_times(int,X0,X1))) ),
inference(forward_demodulation,[],[f2443,f1071]) ).
tff(f2445,plain,
! [X0: int,X1: int] : ( power_power(int,minus_minus(int,X0,X1),plus_plus(nat,one_one(nat),one_one(nat))) = minus_minus(int,plus_plus(int,power_power(int,X0,plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,X1,plus_plus(nat,one_one(nat),one_one(nat)))),times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,X0,X1))) ),
inference(forward_demodulation,[],[f2444,f234]) ).
tff(f8172,plain,
pls = minus_minus(int,plus_plus(int,one_one(int),pls),one_one(int)),
inference(superposition,[],[f1825,f239]) ).
tff(f8184,plain,
pls = minus_minus(int,one_one(int),one_one(int)),
inference(forward_demodulation,[],[f8172,f238]) ).
tff(f8218,plain,
! [X0: int] : ( times_times(int,pls,X0) = times_times(int,one_one(int),minus_minus(int,X0,X0)) ),
inference(superposition,[],[f752,f8184]) ).
tff(f8219,plain,
! [X0: int] : ( times_times(int,pls,X0) = minus_minus(int,X0,X0) ),
inference(forward_demodulation,[],[f8218,f605]) ).
tff(f8224,plain,
! [X0: int] : ( pls = minus_minus(int,X0,X0) ),
inference(forward_demodulation,[],[f8219,f201]) ).
tff(f8334,plain,
! [X0: int,X1: int] : ( plus_plus(int,X0,pls) = minus_minus(int,plus_plus(int,X0,X1),X1) ),
inference(superposition,[],[f1134,f8224]) ).
tff(f8358,plain,
! [X0: int,X1: int] : ( minus_minus(int,plus_plus(int,X0,X1),X1) = X0 ),
inference(forward_demodulation,[],[f8334,f238]) ).
tff(f8892,plain,
! [X2: int,X0: int,X1: int] : ( minus_minus(int,minus_minus(int,plus_plus(int,X0,X1),X2),minus_minus(int,X1,X2)) = X0 ),
inference(superposition,[],[f8358,f1134]) ).
tff(f8923,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,X1,X0) = minus_minus(int,plus_plus(int,X1,plus_plus(int,X0,X2)),X2) ),
inference(superposition,[],[f1134,f8358]) ).
tff(f19801,plain,
! [X0: int,X1: int] : ( minus_minus(int,minus_minus(int,X0,X1),minus_minus(int,pls,X1)) = X0 ),
inference(superposition,[],[f8892,f238]) ).
tff(f19850,plain,
! [X0: int,X1: int] : ( minus_minus(int,pls,minus_minus(int,X1,plus_plus(int,X0,X1))) = X0 ),
inference(superposition,[],[f8892,f8224]) ).
tff(f20455,plain,
! [X0: int,X1: int] : ( plus_plus(int,X0,X1) = minus_minus(int,X0,minus_minus(int,pls,X1)) ),
inference(superposition,[],[f19801,f8358]) ).
tff(f21898,plain,
! [X2: int,X0: int,X1: int] : ( minus_minus(int,X1,X0) = plus_plus(int,X1,minus_minus(int,X2,plus_plus(int,X0,X2))) ),
inference(superposition,[],[f20455,f19850]) ).
tff(f21925,plain,
! [X0: int,X1: int] : ( plus_plus(int,minus_minus(int,X0,X1),X1) = X0 ),
inference(superposition,[],[f19801,f20455]) ).
tff(f21976,plain,
! [X2: int,X0: int,X1: int] : ( minus_minus(int,X1,X0) = minus_minus(int,plus_plus(int,X1,X2),plus_plus(int,X0,X2)) ),
inference(forward_demodulation,[],[f21898,f1134]) ).
tff(f22250,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,X0,X2) = plus_plus(int,minus_minus(int,X0,X1),plus_plus(int,X1,X2)) ),
inference(superposition,[],[f1099,f21925]) ).
tff(f22253,plain,
! [X0: int,X1: int] : ( minus_minus(int,X0,X1) = minus_minus(int,pls,minus_minus(int,X1,X0)) ),
inference(superposition,[],[f19850,f21925]) ).
tff(f23844,plain,
! [X0: int,X1: int] : ( minus_minus(int,pls,X0) = minus_minus(int,X1,plus_plus(int,X0,X1)) ),
inference(superposition,[],[f22253,f8358]) ).
tff(f43989,plain,
! [X2: int,X0: int,X1: int] : ( minus_minus(int,X0,X2) = plus_plus(int,minus_minus(int,X0,plus_plus(int,X1,X2)),X1) ),
inference(superposition,[],[f8923,f21925]) ).
tff(f43997,plain,
! [X0: int,X1: int] : ( plus_plus(int,plus_plus(int,X0,X1),X0) = minus_minus(int,plus_plus(int,plus_plus(int,X0,X0),plus_plus(int,X1,X1)),X1) ),
inference(superposition,[],[f8923,f320]) ).
tff(f44121,plain,
! [X0: int,X1: int] : ( plus_plus(int,plus_plus(int,X0,X0),X1) = plus_plus(int,plus_plus(int,X0,X1),X0) ),
inference(forward_demodulation,[],[f43997,f8923]) ).
tff(f44203,plain,
! [X0: int,X1: int] : ( plus_plus(int,plus_plus(int,X0,X0),X1) = plus_plus(int,X0,plus_plus(int,X1,X0)) ),
inference(forward_demodulation,[],[f44121,f1099]) ).
tff(f44252,plain,
! [X0: int,X1: int] : ( plus_plus(int,X0,plus_plus(int,X1,X0)) = plus_plus(int,X0,plus_plus(int,X0,X1)) ),
inference(forward_demodulation,[],[f44203,f1099]) ).
tff(f51051,plain,
! [X0: int,X1: int] : ( plus_plus(int,minus_minus(int,X0,X1),X0) = plus_plus(int,minus_minus(int,X0,X1),plus_plus(int,X1,minus_minus(int,X0,X1))) ),
inference(superposition,[],[f44252,f21925]) ).
tff(f51474,plain,
! [X0: int,X1: int] : ( plus_plus(int,minus_minus(int,X0,X1),X0) = plus_plus(int,X0,minus_minus(int,X0,X1)) ),
inference(forward_demodulation,[],[f51051,f22250]) ).
tff(f51698,plain,
! [X0: int,X1: int] : ( plus_plus(int,minus_minus(int,X0,X1),X0) = minus_minus(int,plus_plus(int,X0,X0),X1) ),
inference(forward_demodulation,[],[f51474,f1134]) ).
tff(f86025,plain,
! [X2: int,X0: int,X1: int] : ( minus_minus(int,minus_minus(int,X0,X1),X2) = minus_minus(int,X0,plus_plus(int,X2,X1)) ),
inference(superposition,[],[f21976,f21925]) ).
tff(f86126,plain,
! [X2: int,X0: int,X1: int] : ( minus_minus(int,plus_plus(int,X1,X2),X0) = minus_minus(int,X1,minus_minus(int,X0,X2)) ),
inference(superposition,[],[f21976,f21925]) ).
tff(f108628,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,pls,X2) = plus_plus(int,minus_minus(int,X0,X1),plus_plus(int,minus_minus(int,X1,X0),X2)) ),
inference(superposition,[],[f22250,f22253]) ).
tff(f108652,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,X2,plus_plus(int,X1,X0)) = plus_plus(int,minus_minus(int,X2,X0),plus_plus(int,X0,plus_plus(int,X0,X1))) ),
inference(superposition,[],[f22250,f44252]) ).
tff(f109004,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,X2,plus_plus(int,X0,X1)) = plus_plus(int,X2,plus_plus(int,X1,X0)) ),
inference(forward_demodulation,[],[f108652,f22250]) ).
tff(f109018,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,minus_minus(int,X0,X1),plus_plus(int,minus_minus(int,X1,X0),X2)) = X2 ),
inference(forward_demodulation,[],[f108628,f239]) ).
tff(f121650,plain,
! [X0: int,X1: int] : ( plus_plus(int,minus_minus(int,pls,X0),X1) = minus_minus(int,plus_plus(int,X1,X1),plus_plus(int,X0,X1)) ),
inference(superposition,[],[f51698,f23844]) ).
tff(f122035,plain,
! [X0: int,X1: int] : ( minus_minus(int,X1,X0) = plus_plus(int,minus_minus(int,pls,X0),X1) ),
inference(forward_demodulation,[],[f121650,f21976]) ).
tff(f125164,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,X0,X1) = minus_minus(int,X1,minus_minus(int,X2,plus_plus(int,X0,X2))) ),
inference(superposition,[],[f122035,f19850]) ).
tff(f125165,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,minus_minus(int,X0,X1),X2) = minus_minus(int,X2,minus_minus(int,X1,X0)) ),
inference(superposition,[],[f122035,f22253]) ).
tff(f126017,plain,
! [X0: int,X1: int] : ( plus_plus(int,X0,X1) = minus_minus(int,X1,minus_minus(int,pls,X0)) ),
inference(forward_demodulation,[],[f125164,f23844]) ).
tff(f147778,plain,
! [X2: int,X0: int,X1: int] : ( minus_minus(int,plus_plus(int,X0,X1),X2) = minus_minus(int,X1,plus_plus(int,X2,minus_minus(int,pls,X0))) ),
inference(superposition,[],[f86025,f126017]) ).
tff(f147832,plain,
! [X2: int,X0: int,X1: int] : ( minus_minus(int,power_power(int,minus_minus(int,X0,X1),plus_plus(nat,one_one(nat),one_one(nat))),X2) = minus_minus(int,plus_plus(int,power_power(int,X0,plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,X1,plus_plus(nat,one_one(nat),one_one(nat)))),plus_plus(int,X2,times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,X0,X1)))) ),
inference(superposition,[],[f86025,f2445]) ).
tff(f148122,plain,
! [X2: int,X0: int,X1: int] : ( minus_minus(int,power_power(int,minus_minus(int,X0,X1),plus_plus(nat,one_one(nat),one_one(nat))),X2) = minus_minus(int,power_power(int,X0,plus_plus(nat,one_one(nat),one_one(nat))),minus_minus(int,plus_plus(int,X2,times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,X0,X1))),power_power(int,X1,plus_plus(nat,one_one(nat),one_one(nat))))) ),
inference(forward_demodulation,[],[f147832,f86126]) ).
tff(f148171,plain,
! [X2: int,X0: int,X1: int] : ( minus_minus(int,plus_plus(int,X0,X1),X2) = minus_minus(int,X1,minus_minus(int,plus_plus(int,X2,pls),X0)) ),
inference(forward_demodulation,[],[f147778,f1134]) ).
tff(f148294,plain,
! [X2: int,X0: int,X1: int] : ( minus_minus(int,power_power(int,minus_minus(int,X0,X1),plus_plus(nat,one_one(nat),one_one(nat))),X2) = minus_minus(int,power_power(int,X0,plus_plus(nat,one_one(nat),one_one(nat))),minus_minus(int,X2,minus_minus(int,power_power(int,X1,plus_plus(nat,one_one(nat),one_one(nat))),times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,X0,X1))))) ),
inference(forward_demodulation,[],[f148122,f86126]) ).
tff(f148336,plain,
! [X2: int,X0: int,X1: int] : ( minus_minus(int,plus_plus(int,X0,X1),X2) = minus_minus(int,X1,minus_minus(int,X2,minus_minus(int,X0,pls))) ),
inference(forward_demodulation,[],[f148171,f86126]) ).
tff(f148477,plain,
! [X2: int,X0: int,X1: int] : ( minus_minus(int,plus_plus(int,X0,X1),X2) = minus_minus(int,X1,minus_minus(int,X2,X0)) ),
inference(forward_demodulation,[],[f148336,f242]) ).
tff(f188660,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,X2,power_power(int,minus_minus(int,X0,X1),plus_plus(nat,one_one(nat),one_one(nat)))) = plus_plus(int,X2,plus_plus(int,power_power(int,X1,plus_plus(nat,one_one(nat),one_one(nat))),minus_minus(int,power_power(int,X0,plus_plus(nat,one_one(nat),one_one(nat))),times_times(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),X0),X1)))) ),
inference(superposition,[],[f109004,f407]) ).
tff(f190827,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,X2,power_power(int,minus_minus(int,X0,X1),plus_plus(nat,one_one(nat),one_one(nat)))) = plus_plus(int,X2,minus_minus(int,plus_plus(int,power_power(int,X1,plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,X0,plus_plus(nat,one_one(nat),one_one(nat)))),times_times(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),X0),X1))) ),
inference(forward_demodulation,[],[f188660,f1134]) ).
tff(f191761,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,X2,power_power(int,minus_minus(int,X0,X1),plus_plus(nat,one_one(nat),one_one(nat)))) = minus_minus(int,plus_plus(int,X2,plus_plus(int,power_power(int,X1,plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,X0,plus_plus(nat,one_one(nat),one_one(nat))))),times_times(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),X0),X1)) ),
inference(forward_demodulation,[],[f190827,f1134]) ).
tff(f192532,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,X2,power_power(int,minus_minus(int,X0,X1),plus_plus(nat,one_one(nat),one_one(nat)))) = minus_minus(int,X2,minus_minus(int,times_times(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),X0),X1),plus_plus(int,power_power(int,X1,plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,X0,plus_plus(nat,one_one(nat),one_one(nat)))))) ),
inference(forward_demodulation,[],[f191761,f86126]) ).
tff(f193171,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus(int,X2,power_power(int,minus_minus(int,X0,X1),plus_plus(nat,one_one(nat),one_one(nat)))) = minus_minus(int,X2,minus_minus(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,X0,X1)),plus_plus(int,power_power(int,X1,plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,X0,plus_plus(nat,one_one(nat),one_one(nat)))))) ),
inference(forward_demodulation,[],[f192532,f1071]) ).
tff(f200054,plain,
! [X2: int,X3: int,X0: int,X1: int] : ( minus_minus(int,X1,plus_plus(int,minus_minus(int,X2,X3),X0)) = plus_plus(int,minus_minus(int,X1,X0),minus_minus(int,X3,X2)) ),
inference(superposition,[],[f43989,f109018]) ).
tff(f200093,plain,
! [X2: int,X3: int,X0: int,X1: int] : ( minus_minus(int,X1,plus_plus(int,minus_minus(int,X2,X3),X0)) = minus_minus(int,minus_minus(int,X3,X2),minus_minus(int,X0,X1)) ),
inference(forward_demodulation,[],[f200054,f125165]) ).
tff(f200484,plain,
! [X2: int,X3: int,X0: int,X1: int] : ( minus_minus(int,X1,plus_plus(int,minus_minus(int,X2,X3),X0)) = minus_minus(int,X3,plus_plus(int,minus_minus(int,X0,X1),X2)) ),
inference(forward_demodulation,[],[f200093,f86025]) ).
tff(f200838,plain,
! [X2: int,X3: int,X0: int,X1: int] : ( minus_minus(int,X1,plus_plus(int,minus_minus(int,X2,X3),X0)) = minus_minus(int,X3,minus_minus(int,X2,minus_minus(int,X1,X0))) ),
inference(forward_demodulation,[],[f200484,f125165]) ).
tff(f201178,plain,
! [X2: int,X3: int,X0: int,X1: int] : ( minus_minus(int,X3,minus_minus(int,X2,minus_minus(int,X1,X0))) = minus_minus(int,X1,minus_minus(int,X0,minus_minus(int,X3,X2))) ),
inference(forward_demodulation,[],[f200838,f125165]) ).
tff(f271177,plain,
plus_plus(int,power_power(int,minus_minus(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,minus_minus(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat)))) != plus_plus(int,minus_minus(int,minus_minus(int,power_power(int,y,plus_plus(nat,one_one(nat),one_one(nat))),minus_minus(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))))),power_power(int,x,plus_plus(nat,one_one(nat),one_one(nat))))),times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))))),plus_plus(int,power_power(int,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))))),
inference(superposition,[],[f1211,f148477]) ).
tff(f271194,plain,
plus_plus(int,power_power(int,minus_minus(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,minus_minus(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat)))) != minus_minus(int,plus_plus(int,power_power(int,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat)))),minus_minus(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))))),minus_minus(int,power_power(int,y,plus_plus(nat,one_one(nat),one_one(nat))),minus_minus(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))))),power_power(int,x,plus_plus(nat,one_one(nat),one_one(nat))))))),
inference(forward_demodulation,[],[f271177,f125165]) ).
tff(f271239,plain,
plus_plus(int,power_power(int,minus_minus(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,minus_minus(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat)))) != minus_minus(int,power_power(int,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),minus_minus(int,minus_minus(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))))),minus_minus(int,power_power(int,y,plus_plus(nat,one_one(nat),one_one(nat))),minus_minus(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))))),power_power(int,x,plus_plus(nat,one_one(nat),one_one(nat)))))),power_power(int,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))))),
inference(forward_demodulation,[],[f271194,f86126]) ).
tff(f271270,plain,
plus_plus(int,power_power(int,minus_minus(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,minus_minus(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat)))) != minus_minus(int,power_power(int,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),minus_minus(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))))),plus_plus(int,power_power(int,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),minus_minus(int,power_power(int,y,plus_plus(nat,one_one(nat),one_one(nat))),minus_minus(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))))),power_power(int,x,plus_plus(nat,one_one(nat),one_one(nat)))))))),
inference(forward_demodulation,[],[f271239,f86025]) ).
tff(f271291,plain,
plus_plus(int,power_power(int,minus_minus(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,minus_minus(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat)))) != minus_minus(int,power_power(int,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),minus_minus(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))))),minus_minus(int,plus_plus(int,power_power(int,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,y,plus_plus(nat,one_one(nat),one_one(nat)))),minus_minus(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))))),power_power(int,x,plus_plus(nat,one_one(nat),one_one(nat))))))),
inference(forward_demodulation,[],[f271270,f1134]) ).
tff(f271304,plain,
plus_plus(int,power_power(int,minus_minus(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,minus_minus(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat)))) != minus_minus(int,power_power(int,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),minus_minus(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))))),minus_minus(int,power_power(int,x,plus_plus(nat,one_one(nat),one_one(nat))),minus_minus(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))))),plus_plus(int,power_power(int,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,y,plus_plus(nat,one_one(nat),one_one(nat)))))))),
inference(forward_demodulation,[],[f271291,f201178]) ).
tff(f271309,plain,
plus_plus(int,power_power(int,minus_minus(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,minus_minus(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat)))) != minus_minus(int,power_power(int,x,plus_plus(nat,one_one(nat),one_one(nat))),minus_minus(int,minus_minus(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))))),plus_plus(int,power_power(int,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,y,plus_plus(nat,one_one(nat),one_one(nat))))),minus_minus(int,power_power(int,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n)))))))),
inference(forward_demodulation,[],[f271304,f201178]) ).
tff(f271312,plain,
plus_plus(int,power_power(int,minus_minus(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,minus_minus(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat)))) != minus_minus(int,power_power(int,minus_minus(int,x,plus_plus(int,r,times_times(int,r,semiring_1_of_nat(int,n)))),plus_plus(nat,one_one(nat),one_one(nat))),minus_minus(int,times_times(int,plus_plus(int,one_one(int),one_one(int)),times_times(int,y,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))))),plus_plus(int,power_power(int,plus_plus(int,sa,times_times(int,sa,semiring_1_of_nat(int,n))),plus_plus(nat,one_one(nat),one_one(nat))),power_power(int,y,plus_plus(nat,one_one(nat),one_one(nat)))))),
inference(forward_demodulation,[],[f271309,f148294]) ).
tff(f271315,plain,
$false,
inference(forward_subsumption_resolution,[],[f271312,f193171]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM984_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n014.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % 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:49:16 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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
% 5.15/1.74 % (1203287)Detected formulas, will run a generic FOF schedule.
% 5.15/1.74 % (1203295)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=971282088:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.15/1.74 % (1203295)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 5.15/1.74 % (1203295)Refutation not found, incomplete strategy
% 5.15/1.74 % (1203295)------------------------------
% 5.15/1.74 % (1203295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.15/1.74 % (1203295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.15/1.74 % (1203295)CaDiCaL version: 2.1.3
% 5.15/1.74 % (1203295)Termination reason: Refutation not found, incomplete strategy
% 5.15/1.74 % (1203295)Time elapsed: 0.007 s
% 5.15/1.74 % (1203295)Peak memory usage: 89 MB
% 5.15/1.74 % (1203295)Instructions burned: 24 (million)
% 5.15/1.74 % (1203293)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=2128080202:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.15/1.74 % (1203292)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=452792880:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.15/1.74 % (1203294)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=408083430:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.15/1.74 % (1203296)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=772565075:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.15/1.74 % (1203298)dis-21_1_sil=8000:lcm=predicate:random_seed=542024013: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.15/1.74 % (1203297)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3662197495:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.15/1.74 % (1203294)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 5.15/1.74 % (1203298)Refutation not found, incomplete strategy
% 5.15/1.74 % (1203298)------------------------------
% 5.15/1.74 % (1203298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.15/1.74 % (1203298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.15/1.74 % (1203298)CaDiCaL version: 2.1.3
% 5.15/1.74 % (1203298)Termination reason: Refutation not found, incomplete strategy
% 5.15/1.74 % (1203298)Time elapsed: 0.009 s
% 5.15/1.74 % (1203298)Peak memory usage: 88 MB
% 5.15/1.74 % (1203298)Instructions burned: 17 (million)
% 5.15/1.74 % (1203296)Instruction limit reached!
% 5.15/1.74 % (1203296)------------------------------
% 5.15/1.74 % (1203296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.15/1.74 % (1203296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.15/1.74 % (1203296)CaDiCaL version: 2.1.3
% 5.15/1.74 % (1203296)Termination reason: Instruction limit
% 5.15/1.74 % (1203296)Termination phase: Saturation
% 5.15/1.74 % (1203296)Time elapsed: 0.065 s
% 5.15/1.74 % (1203296)Peak memory usage: 89 MB
% 5.15/1.74 % (1203296)Instructions burned: 120 (million)
% 5.15/1.74 % (1203297)Instruction limit reached!
% 5.15/1.74 % (1203297)------------------------------
% 5.15/1.74 % (1203297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.15/1.74 % (1203297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.15/1.74 % (1203297)CaDiCaL version: 2.1.3
% 5.15/1.74 % (1203297)Termination reason: Instruction limit
% 5.15/1.74 % (1203297)Termination phase: Saturation
% 5.15/1.74 % (1203297)Time elapsed: 0.075 s
% 5.15/1.74 % (1203297)Peak memory usage: 89 MB
% 5.15/1.74 % (1203297)Instructions burned: 141 (million)
% 5.15/1.74 % (1203295)------------------------------
% 5.15/1.74 % (1203295)------------------------------
% 5.15/1.74 % (1203306)lrs+10_1_sil=8000:sp=occurrence:random_seed=906508636:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.15/1.74 % (1203308)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2090131436:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.15/1.74 % (1203307)lrs+10_1_sil=32000:urr=on:br=off:random_seed=112219291:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.68/2.04 % (1203298)------------------------------
% 8.68/2.04 % (1203298)------------------------------
% 8.68/2.04 % (1203307)Instruction limit reached!
% 8.68/2.04 % (1203307)------------------------------
% 8.68/2.04 % (1203307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.68/2.04 % (1203307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/2.04 % (1203307)CaDiCaL version: 2.1.3
% 8.68/2.04 % (1203307)Termination reason: Instruction limit
% 8.68/2.04 % (1203307)Termination phase: Saturation
% 8.68/2.04 % (1203307)Time elapsed: 0.082 s
% 8.68/2.04 % (1203307)Peak memory usage: 90 MB
% 8.68/2.04 % (1203307)Instructions burned: 158 (million)
% 8.68/2.04 % (1203308)Instruction limit reached!
% 8.68/2.04 % (1203308)------------------------------
% 8.68/2.04 % (1203308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.68/2.04 % (1203308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/2.04 % (1203308)CaDiCaL version: 2.1.3
% 8.68/2.04 % (1203308)Termination reason: Instruction limit
% 8.68/2.04 % (1203308)Termination phase: Saturation
% 8.68/2.04 % (1203308)Time elapsed: 0.092 s
% 8.68/2.04 % (1203308)Peak memory usage: 91 MB
% 8.68/2.04 % (1203308)Instructions burned: 327 (million)
% 8.68/2.04 % (1203306)Instruction limit reached!
% 8.68/2.04 % (1203306)------------------------------
% 8.68/2.04 % (1203306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.68/2.04 % (1203306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/2.04 % (1203306)CaDiCaL version: 2.1.3
% 8.68/2.04 % (1203306)Termination reason: Instruction limit
% 8.68/2.04 % (1203306)Termination phase: Saturation
% 8.68/2.04 % (1203306)Time elapsed: 0.143 s
% 8.68/2.04 % (1203306)Peak memory usage: 91 MB
% 8.68/2.04 % (1203306)Instructions burned: 286 (million)
% 8.68/2.04 % (1203292)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.68/2.04 % (1203294)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.68/2.04 % (1203294)------------------------------
% 8.68/2.04 % (1203294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.68/2.04 % (1203292)------------------------------
% 8.68/2.04 % (1203292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.68/2.04 % (1203292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/2.04 % (1203294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/2.04 % (1203294)CaDiCaL version: 2.1.3
% 8.68/2.04 % (1203292)CaDiCaL version: 2.1.3
% 8.68/2.04 % (1203292)Termination reason: Unknown
% 8.68/2.04 % (1203292)Termination phase: Saturation
% 8.68/2.04 % (1203294)Termination reason: Unknown
% 8.68/2.04 % (1203294)Termination phase: Saturation
% 8.68/2.04 % (1203292)Time elapsed: 0.366 s
% 8.68/2.04 % (1203294)Time elapsed: 0.366 s
% 8.68/2.04 % (1203292)Peak memory usage: 111 MB
% 8.68/2.04 % (1203294)Peak memory usage: 112 MB
% 8.68/2.04 % (1203294)Instructions burned: 543 (million)
% 8.68/2.04 % (1203292)Instructions burned: 543 (million)
% 8.68/2.04 % (1203293)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.68/2.04 % (1203293)------------------------------
% 8.68/2.04 % (1203293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.68/2.04 % (1203293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/2.04 % (1203293)CaDiCaL version: 2.1.3
% 8.68/2.04 % (1203293)Termination reason: Unknown
% 8.68/2.04 % (1203293)Termination phase: Saturation
% 8.68/2.04 % (1203293)Time elapsed: 0.366 s
% 8.68/2.04 % (1203293)Peak memory usage: 113 MB
% 8.68/2.04 % (1203293)Instructions burned: 548 (million)
% 8.68/2.04 % (1203314)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3015883549:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 8.68/2.04 % (1203312)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=610939084:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 8.68/2.04 % (1203313)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=641474380:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 8.68/2.04 % (1203313)Refutation not found, incomplete strategy
% 8.68/2.04 % (1203313)------------------------------
% 8.68/2.04 % (1203313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.68/2.04 % (1203313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.42/2.28 % (1203313)CaDiCaL version: 2.1.3
% 9.42/2.28 % (1203313)Termination reason: Refutation not found, incomplete strategy
% 9.42/2.28 % (1203313)Time elapsed: 0.010 s
% 9.42/2.28 % (1203313)Peak memory usage: 88 MB
% 9.42/2.28 % (1203313)Instructions burned: 19 (million)
% 9.42/2.28 % (1203316)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=582228628:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 9.42/2.28 % (1203318)lrs+10_1_sil=8000:sp=occurrence:random_seed=4236407568:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi)
% 9.42/2.28 % (1203315)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2703417224:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 9.42/2.28 % (1203317)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3276245094:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 9.42/2.28 % (1203316)Refutation not found, incomplete strategy
% 9.42/2.28 % (1203316)------------------------------
% 9.42/2.28 % (1203316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.42/2.28 % (1203316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.42/2.28 % (1203316)CaDiCaL version: 2.1.3
% 9.42/2.28 % (1203316)Termination reason: Refutation not found, incomplete strategy
% 9.42/2.28 % (1203316)Time elapsed: 0.006 s
% 9.42/2.28 % (1203316)Peak memory usage: 88 MB
% 9.42/2.28 % (1203316)Instructions burned: 12 (million)
% 9.42/2.28 % (1203312)Instruction limit reached!
% 9.42/2.28 % (1203312)------------------------------
% 9.42/2.28 % (1203312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.42/2.28 % (1203312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.42/2.28 % (1203312)CaDiCaL version: 2.1.3
% 9.42/2.28 % (1203312)Termination reason: Instruction limit
% 9.42/2.28 % (1203312)Termination phase: Saturation
% 9.42/2.28 % (1203312)Time elapsed: 0.145 s
% 9.42/2.28 % (1203312)Peak memory usage: 91 MB
% 9.42/2.28 % (1203312)Instructions burned: 249 (million)
% 9.42/2.28 % (1203317)Instruction limit reached!
% 9.42/2.28 % (1203317)------------------------------
% 9.42/2.28 % (1203317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.42/2.28 % (1203317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.42/2.28 % (1203317)CaDiCaL version: 2.1.3
% 9.42/2.28 % (1203317)Termination reason: Instruction limit
% 9.42/2.28 % (1203317)Termination phase: Saturation
% 9.42/2.28 % (1203317)Time elapsed: 0.052 s
% 9.42/2.28 % (1203317)Peak memory usage: 88 MB
% 9.42/2.28 % (1203317)Instructions burned: 116 (million)
% 9.42/2.28 % (1203315)Instruction limit reached!
% 9.42/2.28 % (1203315)------------------------------
% 9.42/2.28 % (1203315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.42/2.28 % (1203315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.42/2.28 % (1203315)CaDiCaL version: 2.1.3
% 9.42/2.28 % (1203315)Termination reason: Instruction limit
% 9.42/2.28 % (1203315)Termination phase: Saturation
% 9.42/2.28 % (1203315)Time elapsed: 0.059 s
% 9.42/2.28 % (1203315)Peak memory usage: 89 MB
% 9.42/2.28 % (1203315)Instructions burned: 114 (million)
% 9.42/2.28 % (1203314)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.42/2.28 % (1203314)------------------------------
% 9.42/2.28 % (1203314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.42/2.28 % (1203314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.42/2.28 % (1203314)CaDiCaL version: 2.1.3
% 9.42/2.28 % (1203314)Termination reason: Unknown
% 9.42/2.28 % (1203314)Termination phase: Saturation
% 9.42/2.28 % (1203314)Time elapsed: 0.201 s
% 9.42/2.28 % (1203314)Peak memory usage: 114 MB
% 9.42/2.28 % (1203314)Instructions burned: 544 (million)
% 9.42/2.28 % (1203326)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3210876547:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 9.42/2.28 % (1203313)------------------------------
% 9.42/2.28 % (1203313)------------------------------
% 9.42/2.28 % (1203326)Refutation not found, incomplete strategy
% 9.42/2.28 % (1203326)------------------------------
% 9.42/2.28 % (1203326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.42/2.28 % (1203326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.19/2.58 % (1203326)CaDiCaL version: 2.1.3
% 10.19/2.58 % (1203326)Termination reason: Refutation not found, incomplete strategy
% 10.19/2.58 % (1203326)Time elapsed: 0.008 s
% 10.19/2.58 % (1203326)Peak memory usage: 88 MB
% 10.19/2.58 % (1203326)Instructions burned: 14 (million)
% 10.19/2.58 % (1203328)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4012935934:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi)
% 10.19/2.58 % (1203327)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1446829485:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 10.19/2.58 % (1203329)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2708263162:st=8:i=592:sd=3:ep=RST:ss=axioms_2992 on theBenchmark for (2992ds/592Mi)
% 10.19/2.58 % (1203316)------------------------------
% 10.19/2.58 % (1203316)------------------------------
% 10.19/2.58 % (1203328)Instruction limit reached!
% 10.19/2.58 % (1203328)------------------------------
% 10.19/2.58 % (1203328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.19/2.58 % (1203328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.19/2.58 % (1203328)CaDiCaL version: 2.1.3
% 10.19/2.58 % (1203328)Termination reason: Instruction limit
% 10.19/2.58 % (1203328)Termination phase: Saturation
% 10.19/2.58 % (1203328)Time elapsed: 0.068 s
% 10.19/2.58 % (1203328)Peak memory usage: 89 MB
% 10.19/2.58 % (1203328)Instructions burned: 135 (million)
% 10.19/2.58 % (1203331)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2968715440:st=3:i=13193:sd=3:ss=axioms_2991 on theBenchmark for (2991ds/13193Mi)
% 10.19/2.58 % (1203329)Instruction limit reached!
% 10.19/2.58 % (1203329)------------------------------
% 10.19/2.58 % (1203329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.19/2.58 % (1203329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.19/2.58 % (1203329)CaDiCaL version: 2.1.3
% 10.19/2.58 % (1203329)Termination reason: Instruction limit
% 10.19/2.58 % (1203329)Termination phase: Saturation
% 10.19/2.58 % (1203329)Time elapsed: 0.153 s
% 10.19/2.58 % (1203329)Peak memory usage: 95 MB
% 10.19/2.58 % (1203329)Instructions burned: 595 (million)
% 10.19/2.58 % (1203335)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=1250139703:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/125Mi)
% 10.19/2.58 % (1203335)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 10.19/2.58 % (1203326)------------------------------
% 10.19/2.58 % (1203326)------------------------------
% 10.19/2.58 % (1203336)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4164225025:i=134:gtgl=5:slsql=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/134Mi)
% 10.19/2.58 % (1203338)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2939530587:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/141Mi)
% 10.19/2.58 % (1203338)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 10.19/2.58 % (1203338)Refutation not found, incomplete strategy
% 10.19/2.58 % (1203338)------------------------------
% 10.19/2.58 % (1203338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.19/2.58 % (1203338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.19/2.58 % (1203338)CaDiCaL version: 2.1.3
% 10.19/2.58 % (1203338)Termination reason: Refutation not found, incomplete strategy
% 10.19/2.58 % (1203338)Time elapsed: 0.002 s
% 10.19/2.58 % (1203338)Peak memory usage: 88 MB
% 10.19/2.58 % (1203338)Instructions burned: 5 (million)
% 10.19/2.58 % (1203335)Instruction limit reached!
% 10.19/2.58 % (1203335)------------------------------
% 10.19/2.58 % (1203335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.19/2.58 % (1203335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.19/2.58 % (1203335)CaDiCaL version: 2.1.3
% 10.19/2.58 % (1203335)Termination reason: Instruction limit
% 10.19/2.58 % (1203335)Termination phase: Saturation
% 10.19/2.58 % (1203335)Time elapsed: 0.067 s
% 10.19/2.58 % (1203335)Peak memory usage: 90 MB
% 10.19/2.58 % (1203335)Instructions burned: 126 (million)
% 10.19/2.58 % (1203318)Instruction limit reached!
% 10.19/2.58 % (1203318)------------------------------
% 10.19/2.58 % (1203318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/3.00 % (1203318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/3.00 % (1203318)CaDiCaL version: 2.1.3
% 13.01/3.00 % (1203318)Termination reason: Instruction limit
% 13.01/3.00 % (1203318)Termination phase: Saturation
% 13.01/3.00 % (1203318)Time elapsed: 0.491 s
% 13.01/3.00 % (1203318)Peak memory usage: 97 MB
% 13.01/3.00 % (1203318)Instructions burned: 909 (million)
% 13.01/3.00 % (1203336)Instruction limit reached!
% 13.01/3.00 % (1203336)------------------------------
% 13.01/3.00 % (1203336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/3.00 % (1203336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/3.00 % (1203336)CaDiCaL version: 2.1.3
% 13.01/3.00 % (1203336)Termination reason: Instruction limit
% 13.01/3.00 % (1203336)Termination phase: Saturation
% 13.01/3.00 % (1203336)Time elapsed: 0.073 s
% 13.01/3.00 % (1203336)Peak memory usage: 90 MB
% 13.01/3.00 % (1203336)Instructions burned: 135 (million)
% 13.01/3.00 % (1203327)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.01/3.00 % (1203327)------------------------------
% 13.01/3.00 % (1203327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/3.00 % (1203327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/3.00 % (1203327)CaDiCaL version: 2.1.3
% 13.01/3.00 % (1203327)Termination reason: Unknown
% 13.01/3.00 % (1203327)Termination phase: Saturation
% 13.01/3.00 % (1203327)Time elapsed: 0.368 s
% 13.01/3.00 % (1203327)Peak memory usage: 113 MB
% 13.01/3.00 % (1203327)Instructions burned: 545 (million)
% 13.01/3.00 % (1203341)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1670792496:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2988 on theBenchmark for (2988ds/431Mi)
% 13.01/3.00 % (1203341)Refutation not found, incomplete strategy
% 13.01/3.00 % (1203341)------------------------------
% 13.01/3.00 % (1203341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/3.00 % (1203341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/3.00 % (1203341)CaDiCaL version: 2.1.3
% 13.01/3.00 % (1203341)Termination reason: Refutation not found, incomplete strategy
% 13.01/3.00 % (1203341)Time elapsed: 0.007 s
% 13.01/3.00 % (1203341)Peak memory usage: 88 MB
% 13.01/3.00 % (1203341)Instructions burned: 12 (million)
% 13.01/3.00 % (1203338)------------------------------
% 13.01/3.00 % (1203338)------------------------------
% 13.01/3.00 % (1203344)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=1573375344:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2988 on theBenchmark for (2988ds/150Mi)
% 13.01/3.00 % (1203343)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=2748822051:i=6060:aac=none:ins=25_2988 on theBenchmark for (2988ds/6060Mi)
% 13.01/3.00 % (1203344)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 13.01/3.00 % (1203345)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1650936285:i=14155:bd=all_2987 on theBenchmark for (2987ds/14155Mi)
% 13.01/3.00 % (1203346)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2204173932:i=667:av=off:fsr=off_2987 on theBenchmark for (2987ds/667Mi)
% 13.01/3.00 % (1203331)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.01/3.00 % (1203331)------------------------------
% 13.01/3.00 % (1203331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/3.00 % (1203331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/3.00 % (1203331)CaDiCaL version: 2.1.3
% 13.01/3.00 % (1203331)Termination reason: Unknown
% 13.01/3.00 % (1203331)Termination phase: Saturation
% 13.01/3.00 % (1203331)Time elapsed: 0.369 s
% 13.01/3.00 % (1203331)Peak memory usage: 113 MB
% 13.01/3.00 % (1203331)Instructions burned: 543 (million)
% 13.01/3.00 % (1203346)Refutation not found, incomplete strategy
% 13.01/3.00 % (1203346)------------------------------
% 13.01/3.00 % (1203346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/3.00 % (1203346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/3.00 % (1203346)CaDiCaL version: 2.1.3
% 13.01/3.00 % (1203346)Termination reason: Refutation not found, incomplete strategy
% 17.86/3.54 % (1203346)Time elapsed: 0.008 s
% 17.86/3.54 % (1203346)Peak memory usage: 88 MB
% 17.86/3.54 % (1203346)Instructions burned: 13 (million)
% 17.86/3.54 % (1203344)Instruction limit reached!
% 17.86/3.54 % (1203344)------------------------------
% 17.86/3.54 % (1203344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.86/3.54 % (1203344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.86/3.54 % (1203344)CaDiCaL version: 2.1.3
% 17.86/3.54 % (1203344)Termination reason: Instruction limit
% 17.86/3.54 % (1203344)Termination phase: Saturation
% 17.86/3.54 % (1203344)Time elapsed: 0.095 s
% 17.86/3.54 % (1203344)Peak memory usage: 90 MB
% 17.86/3.54 % (1203344)Instructions burned: 151 (million)
% 17.86/3.54 % (1203348)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=3087476826:s2a=on:i=185:s2at=1.8:fdi=4_2986 on theBenchmark for (2986ds/185Mi)
% 17.86/3.54 % (1203348)Instruction limit reached!
% 17.86/3.54 % (1203348)------------------------------
% 17.86/3.54 % (1203348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.86/3.54 % (1203348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.86/3.54 % (1203348)CaDiCaL version: 2.1.3
% 17.86/3.54 % (1203348)Termination reason: Instruction limit
% 17.86/3.54 % (1203348)Termination phase: Saturation
% 17.86/3.54 % (1203348)Time elapsed: 0.059 s
% 17.86/3.54 % (1203348)Peak memory usage: 90 MB
% 17.86/3.54 % (1203348)Instructions burned: 188 (million)
% 17.86/3.54 % (1203341)------------------------------
% 17.86/3.54 % (1203341)------------------------------
% 17.86/3.54 % (1203353)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=696738831:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2985 on theBenchmark for (2985ds/193Mi)
% 17.86/3.54 % (1203354)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2968063980:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2985 on theBenchmark for (2985ds/4850Mi)
% 17.86/3.54 % (1203354)Refutation not found, incomplete strategy
% 17.86/3.54 % (1203354)------------------------------
% 17.86/3.54 % (1203354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.86/3.55 % (1203354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.86/3.55 % (1203354)CaDiCaL version: 2.1.3
% 17.86/3.55 % (1203354)Termination reason: Refutation not found, incomplete strategy
% 17.86/3.55 % (1203354)Time elapsed: 0.005 s
% 17.86/3.55 % (1203354)Peak memory usage: 88 MB
% 17.86/3.55 % (1203354)Instructions burned: 9 (million)
% 17.86/3.55 % (1203356)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3603742304:i=12111:sd=1:ss=included_2984 on theBenchmark for (2984ds/12111Mi)
% 17.86/3.55 % (1203346)------------------------------
% 17.86/3.55 % (1203346)------------------------------
% 17.86/3.55 % (1203353)Instruction limit reached!
% 17.86/3.55 % (1203353)------------------------------
% 17.86/3.55 % (1203353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.86/3.55 % (1203353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.86/3.55 % (1203353)CaDiCaL version: 2.1.3
% 17.86/3.55 % (1203353)Termination reason: Instruction limit
% 17.86/3.55 % (1203353)Termination phase: Saturation
% 17.86/3.55 % (1203353)Time elapsed: 0.100 s
% 17.86/3.55 % (1203353)Peak memory usage: 89 MB
% 17.86/3.55 % (1203353)Instructions burned: 194 (million)
% 17.86/3.55 % (1203343)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.86/3.55 % (1203343)------------------------------
% 17.86/3.55 % (1203343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.86/3.55 % (1203343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.86/3.55 % (1203343)CaDiCaL version: 2.1.3
% 17.86/3.55 % (1203343)Termination reason: Unknown
% 17.86/3.55 % (1203343)Termination phase: Saturation
% 17.86/3.55 % (1203343)Time elapsed: 0.368 s
% 17.86/3.55 % (1203343)Peak memory usage: 114 MB
% 17.86/3.55 % (1203343)Instructions burned: 543 (million)
% 17.86/3.55 % (1203357)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2785715074:i=319:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/319Mi)
% 17.86/3.55 % (1203345)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.86/3.55 % (1203345)------------------------------
% 17.86/3.55 % (1203345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.39/4.17 % (1203345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/4.17 % (1203345)CaDiCaL version: 2.1.3
% 23.39/4.17 % (1203345)Termination reason: Unknown
% 23.39/4.17 % (1203345)Termination phase: Saturation
% 23.39/4.17 % (1203345)Time elapsed: 0.365 s
% 23.39/4.17 % (1203345)Peak memory usage: 114 MB
% 23.39/4.17 % (1203345)Instructions burned: 544 (million)
% 23.39/4.17 % (1203361)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3605253213:i=2064:ep=RST_2983 on theBenchmark for (2983ds/2064Mi)
% 23.39/4.17 % (1203362)dis-1011_128_sil=32000:random_seed=3036042920:i=3706:ep=RST:av=off_2983 on theBenchmark for (2983ds/3706Mi)
% 23.39/4.17 % (1203356)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.39/4.17 % (1203356)------------------------------
% 23.39/4.17 % (1203356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.39/4.17 % (1203356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/4.17 % (1203356)CaDiCaL version: 2.1.3
% 23.39/4.17 % (1203356)Termination reason: Unknown
% 23.39/4.17 % (1203356)Termination phase: Saturation
% 23.39/4.17 % (1203356)Time elapsed: 0.201 s
% 23.39/4.17 % (1203356)Peak memory usage: 114 MB
% 23.39/4.17 % (1203356)Instructions burned: 544 (million)
% 23.39/4.17 % (1203354)------------------------------
% 23.39/4.17 % (1203354)------------------------------
% 23.39/4.17 % (1203364)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1787813063:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2982 on theBenchmark for (2982ds/757Mi)
% 23.39/4.17 % (1203364)Refutation not found, incomplete strategy
% 23.39/4.17 % (1203364)------------------------------
% 23.39/4.17 % (1203364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.39/4.17 % (1203364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/4.17 % (1203364)CaDiCaL version: 2.1.3
% 23.39/4.17 % (1203364)Termination reason: Refutation not found, incomplete strategy
% 23.39/4.17 % (1203364)Time elapsed: 0.008 s
% 23.39/4.17 % (1203364)Peak memory usage: 89 MB
% 23.39/4.17 % (1203364)Instructions burned: 13 (million)
% 23.39/4.17 % (1203365)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3454862558:i=13913:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/13913Mi)
% 23.39/4.17 % (1203357)Instruction limit reached!
% 23.39/4.17 % (1203357)------------------------------
% 23.39/4.17 % (1203357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.39/4.17 % (1203357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/4.17 % (1203357)CaDiCaL version: 2.1.3
% 23.39/4.17 % (1203357)Termination reason: Instruction limit
% 23.39/4.17 % (1203357)Termination phase: Saturation
% 23.39/4.17 % (1203357)Time elapsed: 0.193 s
% 23.39/4.17 % (1203357)Peak memory usage: 93 MB
% 23.39/4.17 % (1203357)Instructions burned: 320 (million)
% 23.39/4.17 % (1203368)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3801415940:i=9925:aac=none_2981 on theBenchmark for (2981ds/9925Mi)
% 23.39/4.17 % (1203369)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2667669208:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2981 on theBenchmark for (2981ds/2479Mi)
% 23.39/4.17 % (1203369)Refutation not found, incomplete strategy
% 23.39/4.17 % (1203369)------------------------------
% 23.39/4.17 % (1203369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.39/4.17 % (1203369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.39/4.17 % (1203369)CaDiCaL version: 2.1.3
% 23.39/4.17 % (1203369)Termination reason: Refutation not found, incomplete strategy
% 23.39/4.17 % (1203369)Time elapsed: 0.009 s
% 23.39/4.17 % (1203369)Peak memory usage: 88 MB
% 23.39/4.17 % (1203369)Instructions burned: 15 (million)
% 23.39/4.17 % (1203372)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1097714852:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/440Mi)
% 23.39/4.17 % (1203372)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 23.39/4.17 % (1203364)------------------------------
% 23.39/4.17 % (1203364)------------------------------
% 23.39/4.17 % (1203368)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.39/4.17 % (1203368)------------------------------
% 24.34/4.48 % (1203368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.34/4.48 % (1203368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.34/4.48 % (1203368)CaDiCaL version: 2.1.3
% 24.34/4.48 % (1203368)Termination reason: Unknown
% 24.34/4.48 % (1203368)Termination phase: Saturation
% 24.34/4.48 % (1203368)Time elapsed: 0.198 s
% 24.34/4.48 % (1203368)Peak memory usage: 113 MB
% 24.34/4.48 % (1203368)Instructions burned: 543 (million)
% 24.34/4.48 % (1203365)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.34/4.48 % (1203365)------------------------------
% 24.34/4.48 % (1203365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.34/4.48 % (1203365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.34/4.48 % (1203365)CaDiCaL version: 2.1.3
% 24.34/4.48 % (1203365)Termination reason: Unknown
% 24.34/4.48 % (1203365)Termination phase: Saturation
% 24.34/4.48 % (1203365)Time elapsed: 0.366 s
% 24.34/4.48 % (1203365)Peak memory usage: 113 MB
% 24.34/4.48 % (1203365)Instructions burned: 543 (million)
% 24.34/4.48 % (1203369)------------------------------
% 24.34/4.49 % (1203369)------------------------------
% 24.34/4.49 % (1203377)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=2294552859:cts=off:i=3034:av=off:er=known:fsd=on_2978 on theBenchmark for (2978ds/3034Mi)
% 24.34/4.49 % (1203376)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4105716249:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2978 on theBenchmark for (2978ds/11145Mi)
% 24.34/4.49 % (1203372)Instruction limit reached!
% 24.34/4.49 % (1203372)------------------------------
% 24.34/4.49 % (1203372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.34/4.49 % (1203372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.34/4.49 % (1203372)CaDiCaL version: 2.1.3
% 24.34/4.49 % (1203372)Termination reason: Instruction limit
% 24.34/4.49 % (1203372)Termination phase: Saturation
% 24.34/4.49 % (1203372)Time elapsed: 0.214 s
% 24.34/4.49 % (1203372)Peak memory usage: 90 MB
% 24.34/4.49 % (1203372)Instructions burned: 441 (million)
% 24.34/4.49 % (1203378)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3531916572:st=2:s2a=on:i=524:s2at=2:ss=axioms_2977 on theBenchmark for (2977ds/524Mi)
% 24.34/4.49 % (1203381)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1281167482:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2977 on theBenchmark for (2977ds/1016Mi)
% 24.34/4.49 % (1203382)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3603083124:i=14123:bd=preordered:ins=4_2977 on theBenchmark for (2977ds/14123Mi)
% 24.34/4.49 % (1203377)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.34/4.49 % (1203377)------------------------------
% 24.34/4.49 % (1203377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.34/4.49 % (1203377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.34/4.49 % (1203377)CaDiCaL version: 2.1.3
% 24.34/4.49 % (1203377)Termination reason: Unknown
% 24.34/4.49 % (1203377)Termination phase: Saturation
% 24.34/4.49 % (1203377)Time elapsed: 0.198 s
% 24.34/4.49 % (1203377)Peak memory usage: 114 MB
% 24.34/4.49 % (1203377)Instructions burned: 543 (million)
% 24.34/4.49 % (1203386)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1772198566:i=5781:kws=precedence:bd=all:rawr=on_2975 on theBenchmark for (2975ds/5781Mi)
% 24.34/4.49 % (1203376)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.34/4.49 % (1203376)------------------------------
% 24.34/4.49 % (1203376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.34/4.49 % (1203376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.34/4.49 % (1203376)CaDiCaL version: 2.1.3
% 24.34/4.49 % (1203376)Termination reason: Unknown
% 24.34/4.49 % (1203376)Termination phase: Saturation
% 24.34/4.49 % (1203376)Time elapsed: 0.365 s
% 24.34/4.49 % (1203376)Peak memory usage: 114 MB
% 24.34/4.49 % (1203376)Instructions burned: 543 (million)
% 24.34/4.49 % (1203378)Instruction limit reached!
% 24.34/4.49 % (1203378)------------------------------
% 24.34/4.49 % (1203378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.34/4.49 % (1203378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.53/5.18 % (1203378)CaDiCaL version: 2.1.3
% 30.53/5.18 % (1203378)Termination reason: Instruction limit
% 30.53/5.18 % (1203378)Termination phase: Saturation
% 30.53/5.18 % (1203378)Time elapsed: 0.270 s
% 30.53/5.18 % (1203378)Peak memory usage: 93 MB
% 30.53/5.18 % (1203378)Instructions burned: 524 (million)
% 30.53/5.18 % (1203382)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 30.53/5.18 % (1203382)------------------------------
% 30.53/5.18 % (1203382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.53/5.18 % (1203382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.53/5.18 % (1203382)CaDiCaL version: 2.1.3
% 30.53/5.18 % (1203382)Termination reason: Unknown
% 30.53/5.18 % (1203382)Termination phase: Saturation
% 30.53/5.18 % (1203382)Time elapsed: 0.359 s
% 30.53/5.18 % (1203382)Peak memory usage: 113 MB
% 30.53/5.18 % (1203382)Instructions burned: 541 (million)
% 30.53/5.18 % (1203388)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=1526614661:i=2448:gtgl=5:bd=preordered:gtg=all_2973 on theBenchmark for (2973ds/2448Mi)
% 30.53/5.18 % (1203361)Instruction limit reached!
% 30.53/5.18 % (1203361)------------------------------
% 30.53/5.18 % (1203361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.53/5.18 % (1203361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.53/5.18 % (1203361)CaDiCaL version: 2.1.3
% 30.53/5.18 % (1203361)Termination reason: Instruction limit
% 30.53/5.18 % (1203361)Termination phase: Saturation
% 30.53/5.18 % (1203361)Time elapsed: 0.979 s
% 30.53/5.18 % (1203361)Peak memory usage: 103 MB
% 30.53/5.18 % (1203361)Instructions burned: 2065 (million)
% 30.53/5.18 % (1203389)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=248076095:i=3223:kws=precedence:fgj=on:av=off_2973 on theBenchmark for (2973ds/3223Mi)
% 30.53/5.18 % (1203391)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3513933091:st=5.6:i=2033:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/2033Mi)
% 30.53/5.18 % (1203392)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=945618213:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2971 on theBenchmark for (2971ds/2055Mi)
% 30.53/5.18 % (1203381)Instruction limit reached!
% 30.53/5.18 % (1203381)------------------------------
% 30.53/5.18 % (1203381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.53/5.18 % (1203381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.53/5.18 % (1203381)CaDiCaL version: 2.1.3
% 30.53/5.18 % (1203381)Termination reason: Instruction limit
% 30.53/5.18 % (1203381)Termination phase: Saturation
% 30.53/5.18 % (1203381)Time elapsed: 0.541 s
% 30.53/5.18 % (1203381)Peak memory usage: 99 MB
% 30.53/5.18 % (1203381)Instructions burned: 1018 (million)
% 30.53/5.18 % (1203396)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=4185348451:i=21611:sd=3:ss=axioms_2970 on theBenchmark for (2970ds/21611Mi)
% 30.53/5.18 % (1203388)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 30.53/5.18 % (1203388)------------------------------
% 30.53/5.18 % (1203388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.53/5.18 % (1203388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.53/5.18 % (1203388)CaDiCaL version: 2.1.3
% 30.53/5.18 % (1203388)Termination reason: Unknown
% 30.53/5.18 % (1203388)Termination phase: Saturation
% 30.53/5.18 % (1203388)Time elapsed: 0.364 s
% 30.53/5.18 % (1203388)Peak memory usage: 113 MB
% 30.53/5.18 % (1203388)Instructions burned: 547 (million)
% 30.53/5.18 % (1203389)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 30.53/5.18 % (1203389)------------------------------
% 30.53/5.18 % (1203389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.53/5.18 % (1203389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.53/5.18 % (1203389)CaDiCaL version: 2.1.3
% 30.53/5.18 % (1203389)Termination reason: Unknown
% 30.53/5.18 % (1203389)Termination phase: Saturation
% 30.53/5.18 % (1203389)Time elapsed: 0.359 s
% 30.53/5.18 % (1203389)Peak memory usage: 114 MB
% 30.53/5.18 % (1203389)Instructions burned: 543 (million)
% 30.53/5.18 % (1203392)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 31.88/5.64 % (1203391)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 31.88/5.64 % (1203391)------------------------------
% 31.88/5.64 % (1203391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.64 % (1203392)------------------------------
% 31.88/5.64 % (1203392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.64 % (1203392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.64 % (1203391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.64 % (1203392)CaDiCaL version: 2.1.3
% 31.88/5.64 % (1203391)CaDiCaL version: 2.1.3
% 31.88/5.64 % (1203391)Termination reason: Unknown
% 31.88/5.64 % (1203391)Termination phase: Saturation
% 31.88/5.64 % (1203392)Termination reason: Unknown
% 31.88/5.64 % (1203392)Termination phase: Saturation
% 31.88/5.64 % (1203391)Time elapsed: 0.360 s
% 31.88/5.64 % (1203392)Time elapsed: 0.360 s
% 31.88/5.64 % (1203392)Peak memory usage: 112 MB
% 31.88/5.64 % (1203391)Peak memory usage: 112 MB
% 31.88/5.64 % (1203392)Instructions burned: 544 (million)
% 31.88/5.64 % (1203391)Instructions burned: 543 (million)
% 31.88/5.64 % (1203398)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=426625866:i=4835:sd=13:ss=axioms:sgt=23_2968 on theBenchmark for (2968ds/4835Mi)
% 31.88/5.64 % (1203398)Refutation not found, incomplete strategy
% 31.88/5.64 % (1203398)------------------------------
% 31.88/5.64 % (1203398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.64 % (1203398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.64 % (1203398)CaDiCaL version: 2.1.3
% 31.88/5.64 % (1203398)Termination reason: Refutation not found, incomplete strategy
% 31.88/5.64 % (1203398)Time elapsed: 0.009 s
% 31.88/5.64 % (1203398)Peak memory usage: 88 MB
% 31.88/5.64 % (1203398)Instructions burned: 15 (million)
% 31.88/5.64 % (1203399)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=352746316:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2967 on theBenchmark for (2967ds/797Mi)
% 31.88/5.64 % (1203399)Refutation not found, incomplete strategy
% 31.88/5.64 % (1203399)------------------------------
% 31.88/5.64 % (1203399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.64 % (1203399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.64 % (1203399)CaDiCaL version: 2.1.3
% 31.88/5.64 % (1203399)Termination reason: Refutation not found, incomplete strategy
% 31.88/5.64 % (1203399)Time elapsed: 0.011 s
% 31.88/5.64 % (1203399)Peak memory usage: 88 MB
% 31.88/5.64 % (1203399)Instructions burned: 19 (million)
% 31.88/5.64 % (1203401)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=258767632:i=6038:nm=6_2966 on theBenchmark for (2966ds/6038Mi)
% 31.88/5.64 % (1203400)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3896348104:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2966 on theBenchmark for (2966ds/2326Mi)
% 31.88/5.64 % (1203400)Refutation not found, incomplete strategy
% 31.88/5.64 % (1203400)------------------------------
% 31.88/5.64 % (1203400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.64 % (1203400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.64 % (1203400)CaDiCaL version: 2.1.3
% 31.88/5.64 % (1203400)Termination reason: Refutation not found, incomplete strategy
% 31.88/5.64 % (1203400)Time elapsed: 0.009 s
% 31.88/5.64 % (1203400)Peak memory usage: 88 MB
% 31.88/5.64 % (1203400)Instructions burned: 16 (million)
% 31.88/5.64 % (1203396)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 31.88/5.64 % (1203396)------------------------------
% 31.88/5.64 % (1203396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.64 % (1203396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.64 % (1203396)CaDiCaL version: 2.1.3
% 31.88/5.64 % (1203396)Termination reason: Unknown
% 31.88/5.64 % (1203396)Termination phase: Saturation
% 31.88/5.64 % (1203396)Time elapsed: 0.368 s
% 31.88/5.64 % (1203396)Peak memory usage: 113 MB
% 31.88/5.64 % (1203396)Instructions burned: 541 (million)
% 31.88/5.64 % (1203398)------------------------------
% 31.88/5.64 % (1203398)------------------------------
% 31.88/5.64 % (1203399)------------------------------
% 36.98/6.11 % (1203399)------------------------------
% 36.98/6.11 % (1203406)lrs+10_1_sil=32000:sp=occurrence:random_seed=1417418153:st=2:i=33334:sd=3:ss=included:sgt=32_2964 on theBenchmark for (2964ds/33334Mi)
% 36.98/6.11 % (1203400)------------------------------
% 36.98/6.11 % (1203400)------------------------------
% 36.98/6.11 % (1203407)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1012894519:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2963 on theBenchmark for (2963ds/1008Mi)
% 36.98/6.11 % (1203408)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=727535874:i=8327:s2at=5:bd=preordered_2963 on theBenchmark for (2963ds/8327Mi)
% 36.98/6.11 % (1203401)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 36.98/6.11 % (1203401)------------------------------
% 36.98/6.11 % (1203401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.98/6.11 % (1203401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.98/6.11 % (1203401)CaDiCaL version: 2.1.3
% 36.98/6.11 % (1203401)Termination reason: Unknown
% 36.98/6.11 % (1203401)Termination phase: Saturation
% 36.98/6.11 % (1203401)Time elapsed: 0.365 s
% 36.98/6.11 % (1203401)Peak memory usage: 113 MB
% 36.98/6.11 % (1203401)Instructions burned: 543 (million)
% 36.98/6.11 % (1203362)Instruction limit reached!
% 36.98/6.11 % (1203362)------------------------------
% 36.98/6.11 % (1203362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.98/6.11 % (1203362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.98/6.11 % (1203362)CaDiCaL version: 2.1.3
% 36.98/6.11 % (1203362)Termination reason: Instruction limit
% 36.98/6.11 % (1203362)Termination phase: Saturation
% 36.98/6.11 % (1203362)Time elapsed: 2.057 s
% 36.98/6.11 % (1203362)Peak memory usage: 114 MB
% 36.98/6.11 % (1203362)Instructions burned: 3708 (million)
% 36.98/6.11 % (1203410)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=2931263387:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2962 on theBenchmark for (2962ds/1083Mi)
% 36.98/6.11 % (1203413)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1089261267:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2961 on theBenchmark for (2961ds/1084Mi)
% 36.98/6.11 % (1203414)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=638225588:i=6995:s2at=5:gtg=all_2961 on theBenchmark for (2961ds/6995Mi)
% 36.98/6.11 % (1203408)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 36.98/6.11 % (1203408)------------------------------
% 36.98/6.11 % (1203408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.98/6.11 % (1203408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.98/6.11 % (1203408)CaDiCaL version: 2.1.3
% 36.98/6.11 % (1203408)Termination reason: Unknown
% 36.98/6.11 % (1203408)Termination phase: Saturation
% 36.98/6.11 % (1203408)Time elapsed: 0.362 s
% 36.98/6.11 % (1203408)Peak memory usage: 114 MB
% 36.98/6.11 % (1203408)Instructions burned: 542 (million)
% 36.98/6.11 % (1203407)Instruction limit reached!
% 36.98/6.11 % (1203407)------------------------------
% 36.98/6.11 % (1203407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.98/6.11 % (1203407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.98/6.11 % (1203407)CaDiCaL version: 2.1.3
% 36.98/6.11 % (1203407)Termination reason: Instruction limit
% 36.98/6.11 % (1203407)Termination phase: Saturation
% 36.98/6.11 % (1203407)Time elapsed: 0.497 s
% 36.98/6.11 % (1203407)Peak memory usage: 96 MB
% 36.98/6.11 % (1203407)Instructions burned: 1010 (million)
% 36.98/6.11 % (1203386)Instruction limit reached!
% 36.98/6.11 % (1203386)------------------------------
% 36.98/6.11 % (1203386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.98/6.11 % (1203386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.98/6.11 % (1203386)CaDiCaL version: 2.1.3
% 36.98/6.11 % (1203386)Termination reason: Instruction limit
% 36.98/6.11 % (1203386)Termination phase: Saturation
% 36.98/6.11 % (1203386)Time elapsed: 1.680 s
% 36.98/6.11 % (1203386)Peak memory usage: 128 MB
% 36.98/6.11 % (1203386)Instructions burned: 5785 (million)
% 36.98/6.11 % (1203418)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2153264056:st=2:i=6225:sd=15:ss=axioms_2958 on theBenchmark for (2958ds/6225Mi)
% 40.05/6.70 % (1203410)Instruction limit reached!
% 40.05/6.70 % (1203410)------------------------------
% 40.05/6.70 % (1203410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.05/6.70 % (1203410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.05/6.70 % (1203410)CaDiCaL version: 2.1.3
% 40.05/6.70 % (1203410)Termination reason: Instruction limit
% 40.05/6.70 % (1203410)Termination phase: Saturation
% 40.05/6.70 % (1203410)Time elapsed: 0.438 s
% 40.05/6.70 % (1203410)Peak memory usage: 94 MB
% 40.05/6.70 % (1203410)Instructions burned: 1085 (million)
% 40.05/6.70 % (1203420)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1216171807:st=2.3:i=26457:sd=10:ss=included:sgt=8_2957 on theBenchmark for (2957ds/26457Mi)
% 40.05/6.70 % (1203414)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 40.05/6.70 % (1203414)------------------------------
% 40.05/6.70 % (1203414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.05/6.70 % (1203414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.05/6.70 % (1203414)CaDiCaL version: 2.1.3
% 40.05/6.70 % (1203414)Termination reason: Unknown
% 40.05/6.70 % (1203414)Termination phase: Saturation
% 40.05/6.70 % (1203414)Time elapsed: 0.366 s
% 40.05/6.70 % (1203414)Peak memory usage: 114 MB
% 40.05/6.70 % (1203414)Instructions burned: 548 (million)
% 40.05/6.70 % (1203419)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2705740623:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2957 on theBenchmark for (2957ds/3372Mi)
% 40.05/6.70 % (1203422)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=3442318211:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2956 on theBenchmark for (2956ds/13494Mi)
% 40.05/6.70 % (1203413)Instruction limit reached!
% 40.05/6.70 % (1203413)------------------------------
% 40.05/6.70 % (1203413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.05/6.70 % (1203413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.05/6.70 % (1203413)CaDiCaL version: 2.1.3
% 40.05/6.70 % (1203413)Termination reason: Instruction limit
% 40.05/6.70 % (1203413)Termination phase: Saturation
% 40.05/6.70 % (1203413)Time elapsed: 0.569 s
% 40.05/6.70 % (1203413)Peak memory usage: 97 MB
% 40.05/6.70 % (1203413)Instructions burned: 1086 (million)
% 40.05/6.70 % (1203425)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=2189503157:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2955 on theBenchmark for (2955ds/2503Mi)
% 40.05/6.70 % (1203420)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 40.05/6.70 % (1203420)------------------------------
% 40.05/6.70 % (1203420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.05/6.70 % (1203420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.05/6.70 % (1203420)CaDiCaL version: 2.1.3
% 40.05/6.70 % (1203420)Termination reason: Unknown
% 40.05/6.70 % (1203420)Termination phase: Saturation
% 40.05/6.70 % (1203420)Time elapsed: 0.198 s
% 40.05/6.70 % (1203420)Peak memory usage: 113 MB
% 40.05/6.70 % (1203420)Instructions burned: 544 (million)
% 40.05/6.70 % (1203425)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 40.05/6.70 % (1203429)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2725783445:i=30753:av=off:ss=included_2954 on theBenchmark for (2954ds/30753Mi)
% 40.05/6.70 % (1203427)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2089061479:i=2559:sd=1:ep=RSTC:ss=axioms_2954 on theBenchmark for (2954ds/2559Mi)
% 40.05/6.70 % (1203419)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 40.05/6.70 % (1203419)------------------------------
% 40.05/6.70 % (1203419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.05/6.70 % (1203419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.05/6.70 % (1203419)CaDiCaL version: 2.1.3
% 40.05/6.70 % (1203419)Termination reason: Unknown
% 40.05/6.70 % (1203419)Termination phase: Saturation
% 45.71/7.37 % (1203419)Time elapsed: 0.362 s
% 45.71/7.37 % (1203419)Peak memory usage: 113 MB
% 45.71/7.37 % (1203419)Instructions burned: 542 (million)
% 45.71/7.37 % (1203422)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 45.71/7.37 % (1203422)------------------------------
% 45.71/7.37 % (1203422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.71/7.37 % (1203422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.71/7.37 % (1203422)CaDiCaL version: 2.1.3
% 45.71/7.37 % (1203422)Termination reason: Unknown
% 45.71/7.37 % (1203422)Termination phase: Saturation
% 45.71/7.37 % (1203422)Time elapsed: 0.362 s
% 45.71/7.37 % (1203422)Peak memory usage: 114 MB
% 45.71/7.37 % (1203422)Instructions burned: 547 (million)
% 45.71/7.37 % (1203429)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 45.71/7.37 % (1203429)------------------------------
% 45.71/7.37 % (1203429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.71/7.37 % (1203429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.71/7.37 % (1203429)CaDiCaL version: 2.1.3
% 45.71/7.37 % (1203429)Termination reason: Unknown
% 45.71/7.37 % (1203429)Termination phase: Saturation
% 45.71/7.37 % (1203429)Time elapsed: 0.195 s
% 45.71/7.37 % (1203429)Peak memory usage: 114 MB
% 45.71/7.37 % (1203429)Instructions burned: 544 (million)
% 45.71/7.37 % (1203425)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 45.71/7.37 % (1203425)------------------------------
% 45.71/7.37 % (1203425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.71/7.37 % (1203425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.71/7.37 % (1203425)CaDiCaL version: 2.1.3
% 45.71/7.37 % (1203425)Termination reason: Unknown
% 45.71/7.37 % (1203425)Termination phase: Saturation
% 45.71/7.37 % (1203425)Time elapsed: 0.361 s
% 45.71/7.37 % (1203425)Peak memory usage: 113 MB
% 45.71/7.37 % (1203425)Instructions burned: 540 (million)
% 45.71/7.37 % (1203432)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=886536758:i=26473:ep=RSTC_2952 on theBenchmark for (2952ds/26473Mi)
% 45.71/7.37 % (1203433)dis-1011_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:tgt=ground:npcc=on:sp=arity:sos=on:erd=off:rp=on:gs=on:kmz=on:random_seed=3969637460:cts=off:i=2759:kws=inv_arity:fgj=on_2951 on theBenchmark for (2951ds/2759Mi)
% 45.71/7.37 % (1203434)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:sos=all:spb=goal_then_units:urr=ec_only:sac=on:random_seed=2357078248:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2951 on theBenchmark for (2951ds/5665Mi)
% 45.71/7.37 % (1203434)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 45.71/7.37 % (1203427)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 45.71/7.37 % (1203427)------------------------------
% 45.71/7.37 % (1203427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.71/7.37 % (1203427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.71/7.37 % (1203427)CaDiCaL version: 2.1.3
% 45.71/7.37 % (1203427)Termination reason: Unknown
% 45.71/7.37 % (1203427)Termination phase: Saturation
% 45.71/7.37 % (1203427)Time elapsed: 0.363 s
% 45.71/7.37 % (1203427)Peak memory usage: 113 MB
% 45.71/7.37 % (1203427)Instructions burned: 543 (million)
% 45.71/7.37 % (1203435)dis+1011_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:sos=on:lsd=20:urr=full:alpa=true:sac=on:random_seed=299467058:i=1532:ep=RS:ss=axioms_2950 on theBenchmark for (2950ds/1532Mi)
% 45.71/7.37 % (1203434)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 45.71/7.37 % (1203434)------------------------------
% 45.71/7.37 % (1203434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.71/7.37 % (1203434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.71/7.37 % (1203434)CaDiCaL version: 2.1.3
% 45.71/7.37 % (1203434)Termination reason: Unknown
% 45.71/7.37 % (1203434)Termination phase: Saturation
% 45.71/7.37 % (1203434)Time elapsed: 0.195 s
% 45.71/7.37 % (1203434)Peak memory usage: 113 MB
% 45.71/7.37 % (1203434)Instructions burned: 542 (million)
% 45.71/7.37 % (1203440)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3262697730:i=1565:sd=2:ss=axioms:sgt=32_2949 on theBenchmark for (2949ds/1565Mi)
% 49.62/8.00 % (1203441)lrs-1011_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:sims=off:bsd=on:sp=unary_first:erd=off:spb=goal:lcm=reverse:gs=on:s2agt=8:random_seed=702930587:i=1572:fgj=on:gsp=on_2947 on theBenchmark for (2947ds/1572Mi)
% 49.62/8.00 % (1203441)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 49.62/8.00 % (1203433)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 49.62/8.00 % (1203433)------------------------------
% 49.62/8.00 % (1203433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/8.00 % (1203433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/8.00 % (1203433)CaDiCaL version: 2.1.3
% 49.62/8.00 % (1203433)Termination reason: Unknown
% 49.62/8.00 % (1203433)Termination phase: Saturation
% 49.62/8.00 % (1203433)Time elapsed: 0.360 s
% 49.62/8.00 % (1203433)Peak memory usage: 114 MB
% 49.62/8.00 % (1203433)Instructions burned: 544 (million)
% 49.62/8.00 % (1203435)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 49.62/8.00 % (1203435)------------------------------
% 49.62/8.00 % (1203435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/8.00 % (1203435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/8.00 % (1203435)CaDiCaL version: 2.1.3
% 49.62/8.00 % (1203435)Termination reason: Unknown
% 49.62/8.00 % (1203435)Termination phase: Saturation
% 49.62/8.00 % (1203435)Time elapsed: 0.361 s
% 49.62/8.00 % (1203435)Peak memory usage: 113 MB
% 49.62/8.00 % (1203435)Instructions burned: 545 (million)
% 49.62/8.00 % (1203441)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 49.62/8.00 % (1203441)------------------------------
% 49.62/8.00 % (1203441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/8.00 % (1203441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/8.00 % (1203441)CaDiCaL version: 2.1.3
% 49.62/8.00 % (1203441)Termination reason: Unknown
% 49.62/8.00 % (1203441)Termination phase: Saturation
% 49.62/8.00 % (1203441)Time elapsed: 0.197 s
% 49.62/8.00 % (1203441)Peak memory usage: 113 MB
% 49.62/8.00 % (1203441)Instructions burned: 543 (million)
% 49.62/8.00 % (1203444)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1661094527:i=6052:sd=4:ss=axioms:sgt=24_2946 on theBenchmark for (2946ds/6052Mi)
% 49.62/8.00 % (1203445)lrs+21_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:sos=on:erd=off:lcm=predicate:alpa=false:sac=on:random_seed=1566848519:i=3500:sd=1:bd=preordered:sup=off:ss=included_2945 on theBenchmark for (2945ds/3500Mi)
% 49.62/8.00 % (1203440)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 49.62/8.00 % (1203440)------------------------------
% 49.62/8.00 % (1203440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/8.00 % (1203440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/8.00 % (1203440)CaDiCaL version: 2.1.3
% 49.62/8.00 % (1203440)Termination reason: Unknown
% 49.62/8.00 % (1203440)Termination phase: Saturation
% 49.62/8.00 % (1203440)Time elapsed: 0.362 s
% 49.62/8.00 % (1203440)Peak memory usage: 113 MB
% 49.62/8.00 % (1203440)Instructions burned: 543 (million)
% 49.62/8.00 % (1203446)lrs+35_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:npcc=on:fde=none:sp=weighted_frequency:erd=off:spb=non_intro:updr=off:newcnf=on:random_seed=1768972958:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2944 on theBenchmark for (2944ds/1842Mi)
% 49.62/8.00 % (1203446)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 49.62/8.00 % (1203449)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=568678291:i=66096:add=on_2943 on theBenchmark for (2943ds/66096Mi)
% 49.62/8.00 % (1203446)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 49.62/8.00 % (1203446)------------------------------
% 49.62/8.00 % (1203446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.62/8.00 % (1203446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.62/8.00 % (1203446)CaDiCaL version: 2.1.3
% 49.62/8.00 % (1203446)Termination reason: Unknown
% 49.62/8.00 % (1203446)Termination phase: Saturation
% 49.62/8.00 % (1203446)Time elapsed: 0.195 s
% 53.59/8.57 % (1203446)Peak memory usage: 113 MB
% 53.59/8.57 % (1203446)Instructions burned: 542 (million)
% 53.59/8.57 % (1203444)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 53.59/8.57 % (1203444)------------------------------
% 53.59/8.57 % (1203444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.59/8.57 % (1203444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.59/8.57 % (1203444)CaDiCaL version: 2.1.3
% 53.59/8.57 % (1203444)Termination reason: Unknown
% 53.59/8.57 % (1203444)Termination phase: Saturation
% 53.59/8.57 % (1203444)Time elapsed: 0.362 s
% 53.59/8.57 % (1203444)Peak memory usage: 113 MB
% 53.59/8.57 % (1203444)Instructions burned: 541 (million)
% 53.59/8.57 % (1203445)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 53.59/8.57 % (1203445)------------------------------
% 53.59/8.57 % (1203445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.59/8.57 % (1203445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.59/8.57 % (1203445)CaDiCaL version: 2.1.3
% 53.59/8.57 % (1203445)Termination reason: Unknown
% 53.59/8.57 % (1203445)Termination phase: Saturation
% 53.59/8.57 % (1203445)Time elapsed: 0.360 s
% 53.59/8.57 % (1203445)Peak memory usage: 113 MB
% 53.59/8.57 % (1203445)Instructions burned: 543 (million)
% 53.59/8.57 % (1203452)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=760756751:i=1884:sd=1:nm=60:ss=axioms_2941 on theBenchmark for (2941ds/1884Mi)
% 53.59/8.57 % (1203453)lrs-1011_4:1_sil=16000:bsr=on:random_seed=11140945:cts=off:i=5469:bs=on:fsr=off_2940 on theBenchmark for (2940ds/5469Mi)
% 53.59/8.57 % (1203449)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 53.59/8.57 % (1203449)------------------------------
% 53.59/8.57 % (1203449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.59/8.57 % (1203449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.59/8.57 % (1203449)CaDiCaL version: 2.1.3
% 53.59/8.57 % (1203449)Termination reason: Unknown
% 53.59/8.57 % (1203449)Termination phase: Saturation
% 53.59/8.57 % (1203449)Time elapsed: 0.360 s
% 53.59/8.57 % (1203449)Peak memory usage: 113 MB
% 53.59/8.57 % (1203449)Instructions burned: 544 (million)
% 53.59/8.57 % (1203454)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=unary_frequency:urr=on:bce=on:alpa=false:sac=on:random_seed=2273890520:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2940 on theBenchmark for (2940ds/2037Mi)
% 53.59/8.57 % (1203452)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 53.59/8.57 % (1203452)------------------------------
% 53.59/8.57 % (1203452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.59/8.57 % (1203452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.59/8.57 % (1203452)CaDiCaL version: 2.1.3
% 53.59/8.57 % (1203452)Termination reason: Unknown
% 53.59/8.57 % (1203452)Termination phase: Saturation
% 53.59/8.57 % (1203452)Time elapsed: 0.197 s
% 53.59/8.57 % (1203452)Peak memory usage: 113 MB
% 53.59/8.57 % (1203452)Instructions burned: 541 (million)
% 53.59/8.57 % (1203457)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=522847831:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2938 on theBenchmark for (2938ds/2110Mi)
% 53.59/8.57 % (1203459)dis-1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lcm=reverse:fd=off:flr=on:random_seed=1571390327:i=2430:add=off:aac=none:nm=16_2938 on theBenchmark for (2938ds/2430Mi)
% 53.59/8.57 % (1203459)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 53.59/8.57 % (1203459)------------------------------
% 53.59/8.57 % (1203459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.59/8.57 % (1203459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.59/8.57 % (1203459)CaDiCaL version: 2.1.3
% 53.59/8.57 % (1203459)Termination reason: Unknown
% 53.59/8.57 % (1203459)Termination phase: Saturation
% 53.59/8.57 % (1203459)Time elapsed: 0.193 s
% 53.59/8.57 % (1203459)Peak memory usage: 114 MB
% 53.59/8.57 % (1203459)Instructions burned: 543 (million)
% 53.59/8.57 % (1203454)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 53.59/8.57 % (1203454)------------------------------
% 53.59/8.57 % (1203454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.27/9.09 % (1203454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.27/9.09 % (1203454)CaDiCaL version: 2.1.3
% 58.27/9.09 % (1203454)Termination reason: Unknown
% 58.27/9.09 % (1203454)Termination phase: Saturation
% 58.27/9.09 % (1203454)Time elapsed: 0.368 s
% 58.27/9.09 % (1203454)Peak memory usage: 114 MB
% 58.27/9.09 % (1203454)Instructions burned: 551 (million)
% 58.27/9.09 % (1203462)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:spb=units:acc=on:bsr=unit_only:gs=on:sac=on:random_seed=3199678964:cond=fast:i=4891_2934 on theBenchmark for (2934ds/4891Mi)
% 58.27/9.09 % (1203457)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 58.27/9.09 % (1203457)------------------------------
% 58.27/9.09 % (1203457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.27/9.09 % (1203457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.27/9.09 % (1203457)CaDiCaL version: 2.1.3
% 58.27/9.09 % (1203457)Termination reason: Unknown
% 58.27/9.09 % (1203457)Termination phase: Saturation
% 58.27/9.09 % (1203457)Time elapsed: 0.362 s
% 58.27/9.09 % (1203457)Peak memory usage: 114 MB
% 58.27/9.09 % (1203457)Instructions burned: 547 (million)
% 58.27/9.09 % (1203463)lrs+4_1_anc=all:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sos=on:spb=goal_then_units:lcm=reverse:gs=on:s2agt=16:sac=on:newcnf=on:random_seed=2603598272:st=2:i=14845:sd=2:ss=included:fsd=on_2934 on theBenchmark for (2934ds/14845Mi)
% 58.27/9.09 % (1203462)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 58.27/9.09 % (1203462)------------------------------
% 58.27/9.09 % (1203462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.27/9.09 % (1203462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.27/9.09 % (1203462)CaDiCaL version: 2.1.3
% 58.27/9.09 % (1203462)Termination reason: Unknown
% 58.27/9.09 % (1203462)Termination phase: Saturation
% 58.27/9.09 % (1203462)Time elapsed: 0.198 s
% 58.27/9.09 % (1203462)Peak memory usage: 114 MB
% 58.27/9.09 % (1203462)Instructions burned: 543 (million)
% 58.27/9.09 % (1203465)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=992183916:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2933 on theBenchmark for (2933ds/7534Mi)
% 58.27/9.09 % (1203467)lrs-1002_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=ground:npcc=on:prc=on:fde=none:sims=off:spb=goal:bsr=unit_only:s2agt=32:random_seed=693980917:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2931 on theBenchmark for (2931ds/10353Mi)
% 58.27/9.09 % (1203418)Instruction limit reached!
% 58.27/9.09 % (1203418)------------------------------
% 58.27/9.09 % (1203418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.27/9.09 % (1203418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.27/9.09 % (1203418)CaDiCaL version: 2.1.3
% 58.27/9.09 % (1203418)Termination reason: Instruction limit
% 58.27/9.09 % (1203418)Termination phase: Saturation
% 58.27/9.09 % (1203418)Time elapsed: 2.682 s
% 58.27/9.09 % (1203418)Peak memory usage: 115 MB
% 58.27/9.09 % (1203418)Instructions burned: 6226 (million)
% 58.27/9.09 % (1203463)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 58.27/9.09 % (1203463)------------------------------
% 58.27/9.09 % (1203463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.27/9.09 % (1203463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.27/9.09 % (1203463)CaDiCaL version: 2.1.3
% 58.27/9.09 % (1203463)Termination reason: Unknown
% 58.27/9.09 % (1203463)Termination phase: Saturation
% 58.27/9.09 % (1203463)Time elapsed: 0.360 s
% 58.27/9.09 % (1203463)Peak memory usage: 114 MB
% 58.27/9.09 % (1203463)Instructions burned: 543 (million)
% 58.27/9.09 % (1203467)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 58.27/9.09 % (1203467)------------------------------
% 58.27/9.09 % (1203467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.27/9.09 % (1203467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.27/9.09 % (1203467)CaDiCaL version: 2.1.3
% 58.27/9.09 % (1203467)Termination reason: Unknown
% 58.27/9.09 % (1203467)Termination phase: Saturation
% 58.27/9.09 % (1203467)Time elapsed: 0.196 s
% 58.27/9.09 % (1203467)Peak memory usage: 114 MB
% 58.27/9.09 % (1203467)Instructions burned: 542 (million)
% 62.21/9.71 % (1203470)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4165581793:i=7860_2929 on theBenchmark for (2929ds/7860Mi)
% 62.21/9.71 % (1203470)Refutation not found, incomplete strategy
% 62.21/9.71 % (1203470)------------------------------
% 62.21/9.71 % (1203470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.21/9.71 % (1203470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.21/9.71 % (1203470)CaDiCaL version: 2.1.3
% 62.21/9.71 % (1203470)Termination reason: Refutation not found, incomplete strategy
% 62.21/9.71 % (1203470)Time elapsed: 0.008 s
% 62.21/9.71 % (1203470)Peak memory usage: 88 MB
% 62.21/9.71 % (1203470)Instructions burned: 12 (million)
% 62.21/9.71 % (1203471)ott+1011_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:fde=unused:spb=goal:lsd=30:lcm=predicate:fd=off:gs=on:sac=on:random_seed=1727675545:i=7896:sd=2:bs=on:ss=included:sgt=20_2929 on theBenchmark for (2929ds/7896Mi)
% 62.21/9.71 % (1203465)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 62.21/9.71 % (1203465)------------------------------
% 62.21/9.71 % (1203465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.21/9.71 % (1203465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.21/9.71 % (1203465)CaDiCaL version: 2.1.3
% 62.21/9.71 % (1203465)Termination reason: Unknown
% 62.21/9.71 % (1203465)Termination phase: Saturation
% 62.21/9.71 % (1203465)Time elapsed: 0.363 s
% 62.21/9.71 % (1203465)Peak memory usage: 113 MB
% 62.21/9.71 % (1203465)Instructions burned: 547 (million)
% 62.21/9.71 % (1203472)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=2357280328:i=5812:gtgl=2:gtg=all_2928 on theBenchmark for (2928ds/5812Mi)
% 62.21/9.71 % (1203475)ott-1011_1_anc=none:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=const_frequency:sos=on:lsd=100:random_seed=971782029:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2928 on theBenchmark for (2928ds/2965Mi)
% 62.21/9.71 % (1203470)------------------------------
% 62.21/9.71 % (1203470)------------------------------
% 62.21/9.71 % (1203472)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 62.21/9.71 % (1203472)------------------------------
% 62.21/9.71 % (1203472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.21/9.71 % (1203472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.21/9.71 % (1203472)CaDiCaL version: 2.1.3
% 62.21/9.71 % (1203472)Termination reason: Unknown
% 62.21/9.71 % (1203472)Termination phase: Saturation
% 62.21/9.71 % (1203472)Time elapsed: 0.197 s
% 62.21/9.71 % (1203472)Peak memory usage: 114 MB
% 62.21/9.71 % (1203472)Instructions burned: 547 (million)
% 62.21/9.71 % (1203471)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 62.21/9.71 % (1203471)------------------------------
% 62.21/9.71 % (1203471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.21/9.71 % (1203471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.21/9.71 % (1203471)CaDiCaL version: 2.1.3
% 62.21/9.71 % (1203471)Termination reason: Unknown
% 62.21/9.71 % (1203471)Termination phase: Saturation
% 62.21/9.71 % (1203471)Time elapsed: 0.363 s
% 62.21/9.71 % (1203471)Peak memory usage: 113 MB
% 62.21/9.71 % (1203471)Instructions burned: 542 (million)
% 62.21/9.71 % (1203478)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1843086135:i=2967:kws=precedence:bd=preordered:av=off_2925 on theBenchmark for (2925ds/2967Mi)
% 62.21/9.71 % (1203479)ott+1002_1_anc=all:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:sos=on:spb=goal_then_units:alpa=false:sac=on:random_seed=4251625011:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2925 on theBenchmark for (2925ds/3022Mi)
% 62.21/9.71 % (1203475)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 62.21/9.71 % (1203475)------------------------------
% 62.21/9.71 % (1203475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.21/9.71 % (1203475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.21/9.71 % (1203475)CaDiCaL version: 2.1.3
% 62.21/9.71 % (1203475)Termination reason: Unknown
% 62.21/9.71 % (1203475)Termination phase: Saturation
% 62.21/9.71 % (1203475)Time elapsed: 0.363 s
% 62.21/9.71 % (1203475)Peak memory usage: 114 MB
% 66.85/10.35 % (1203475)Instructions burned: 544 (million)
% 66.85/10.35 % (1203480)lrs-1010_1_ncem=casc2026/models/loop4.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=const_frequency:sos=all:lcm=predicate:acc=on:bsr=unit_only:gs=on:sac=on:newcnf=on:random_seed=537029382:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2924 on theBenchmark for (2924ds/3207Mi)
% 66.85/10.35 % (1203479)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 66.85/10.35 % (1203479)------------------------------
% 66.85/10.35 % (1203479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.85/10.35 % (1203479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/10.35 % (1203479)CaDiCaL version: 2.1.3
% 66.85/10.35 % (1203479)Termination reason: Unknown
% 66.85/10.35 % (1203479)Termination phase: Saturation
% 66.85/10.35 % (1203479)Time elapsed: 0.196 s
% 66.85/10.35 % (1203479)Peak memory usage: 113 MB
% 66.85/10.35 % (1203479)Instructions burned: 542 (million)
% 66.85/10.35 % (1203484)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=1601872100:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2922 on theBenchmark for (2922ds/3289Mi)
% 66.85/10.35 % (1203485)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=2681685133:i=38569:sd=3:ss=axioms:sgt=32_2922 on theBenchmark for (2922ds/38569Mi)
% 66.85/10.35 % (1203478)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 66.85/10.35 % (1203478)------------------------------
% 66.85/10.35 % (1203478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.85/10.35 % (1203478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/10.35 % (1203478)CaDiCaL version: 2.1.3
% 66.85/10.35 % (1203478)Termination reason: Unknown
% 66.85/10.35 % (1203478)Termination phase: Saturation
% 66.85/10.35 % (1203478)Time elapsed: 0.361 s
% 66.85/10.35 % (1203478)Peak memory usage: 113 MB
% 66.85/10.35 % (1203478)Instructions burned: 543 (million)
% 66.85/10.35 % (1203480)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 66.85/10.35 % (1203480)------------------------------
% 66.85/10.35 % (1203480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.85/10.35 % (1203480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/10.35 % (1203480)CaDiCaL version: 2.1.3
% 66.85/10.35 % (1203480)Termination reason: Unknown
% 66.85/10.35 % (1203480)Termination phase: Saturation
% 66.85/10.35 % (1203480)Time elapsed: 0.363 s
% 66.85/10.35 % (1203480)Peak memory usage: 114 MB
% 66.85/10.35 % (1203480)Instructions burned: 542 (million)
% 66.85/10.35 % (1203488)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=1847187385:cts=off:i=3394_2920 on theBenchmark for (2920ds/3394Mi)
% 66.85/10.35 % (1203485)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 66.85/10.35 % (1203485)------------------------------
% 66.85/10.35 % (1203485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.85/10.35 % (1203485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/10.35 % (1203485)CaDiCaL version: 2.1.3
% 66.85/10.35 % (1203485)Termination reason: Unknown
% 66.85/10.35 % (1203485)Termination phase: Saturation
% 66.85/10.35 % (1203485)Time elapsed: 0.196 s
% 66.85/10.35 % (1203485)Peak memory usage: 113 MB
% 66.85/10.35 % (1203485)Instructions burned: 543 (million)
% 66.85/10.35 % (1203491)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=2996195317:i=20684:bd=all:gtg=exists_sym_2918 on theBenchmark for (2918ds/20684Mi)
% 66.85/10.35 % (1203489)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=arity:spb=intro:lcm=reverse:urr=ec_only:fd=preordered:gs=on:sac=on:random_seed=3186455112:i=33824:bd=preordered_2919 on theBenchmark for (2919ds/33824Mi)
% 66.85/10.35 % (1203484)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 66.85/10.35 % (1203484)------------------------------
% 66.85/10.35 % (1203484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.85/10.35 % (1203484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.85/10.35 % (1203484)CaDiCaL version: 2.1.3
% 66.85/10.35 % (1203484)Termination reason: Unknown
% 66.85/10.35 % (1203484)Termination phase: Saturation
% 66.85/10.35 % (1203484)Time elapsed: 0.361 s
% 66.85/10.35 % (1203484)Peak memory usage: 113 MB
% 66.85/10.35 % (1203484)Instructions burned: 543 (million)
% 69.83/10.88 % (1203494)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:irw=on:npcc=on:prc=on:bsd=on:sp=reverse_frequency:sos=on:erd=off:spb=goal:lcm=reverse:urr=full:bsr=on:s2agt=32:alpa=random:kmz=on:random_seed=1677767292:st=3:prac=on:i=7222:kws=arity_squared:add=on:fgj=on:bd=preordered:gtg=exists_top:gsp=on:ss=axioms:er=known:sgt=8:proc=on_2917 on theBenchmark for (2917ds/7222Mi)
% 69.83/10.88 % (1203494)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 69.83/10.88 % (1203491)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 69.83/10.88 % (1203491)------------------------------
% 69.83/10.88 % (1203491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.83/10.88 % (1203491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.83/10.88 % (1203491)CaDiCaL version: 2.1.3
% 69.83/10.88 % (1203491)Termination reason: Unknown
% 69.83/10.88 % (1203491)Termination phase: Saturation
% 69.83/10.88 % (1203491)Time elapsed: 0.196 s
% 69.83/10.88 % (1203491)Peak memory usage: 114 MB
% 69.83/10.88 % (1203491)Instructions burned: 546 (million)
% 69.83/10.88 % (1203488)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 69.83/10.88 % (1203488)------------------------------
% 69.83/10.88 % (1203488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.83/10.88 % (1203488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.83/10.88 % (1203488)CaDiCaL version: 2.1.3
% 69.83/10.88 % (1203488)Termination reason: Unknown
% 69.83/10.88 % (1203488)Termination phase: Saturation
% 69.83/10.88 % (1203488)Time elapsed: 0.362 s
% 69.83/10.88 % (1203488)Peak memory usage: 113 MB
% 69.83/10.88 % (1203488)Instructions burned: 544 (million)
% 69.83/10.88 % (1203496)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=199062041:st=4:i=7295:sd=4:ep=R:ss=axioms_2915 on theBenchmark for (2915ds/7295Mi)
% 69.83/10.88 % (1203489)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 69.83/10.88 % (1203489)------------------------------
% 69.83/10.88 % (1203489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.83/10.88 % (1203489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.83/10.88 % (1203489)CaDiCaL version: 2.1.3
% 69.83/10.88 % (1203489)Termination reason: Unknown
% 69.83/10.88 % (1203489)Termination phase: Saturation
% 69.83/10.88 % (1203489)Time elapsed: 0.360 s
% 69.83/10.88 % (1203489)Peak memory usage: 114 MB
% 69.83/10.88 % (1203489)Instructions burned: 543 (million)
% 69.83/10.88 % (1203497)lrs+32_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:fde=none:sp=occurrence:urr=ec_only:fd=preordered:random_seed=1235215320:i=4036:ins=10_2915 on theBenchmark for (2915ds/4036Mi)
% 69.83/10.88 % (1203496)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 69.83/10.88 % (1203496)------------------------------
% 69.83/10.88 % (1203496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.83/10.88 % (1203496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.83/10.88 % (1203496)CaDiCaL version: 2.1.3
% 69.83/10.88 % (1203496)Termination reason: Unknown
% 69.83/10.88 % (1203496)Termination phase: Saturation
% 69.83/10.88 % (1203496)Time elapsed: 0.198 s
% 69.83/10.88 % (1203496)Peak memory usage: 113 MB
% 69.83/10.88 % (1203496)Instructions burned: 547 (million)
% 69.83/10.88 % (1203499)lrs+10_1_sil=128000:lcm=predicate:random_seed=3781786276:st=3:i=43697:sd=5:ss=axioms_2914 on theBenchmark for (2914ds/43697Mi)
% 69.83/10.88 % (1203494)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 69.83/10.88 % (1203494)------------------------------
% 69.83/10.88 % (1203494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.83/10.88 % (1203494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.83/10.88 % (1203494)CaDiCaL version: 2.1.3
% 69.83/10.88 % (1203494)Termination reason: Unknown
% 69.83/10.88 % (1203494)Termination phase: Saturation
% 69.83/10.88 % (1203494)Time elapsed: 0.366 s
% 69.83/10.88 % (1203494)Peak memory usage: 114 MB
% 69.83/10.88 % (1203494)Instructions burned: 553 (million)
% 69.83/10.88 % (1203501)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=2758170387:i=17599:gtg=all:ss=axioms:fsd=on_2912 on theBenchmark for (2912ds/17599Mi)
% 77.17/11.93 % (1203503)lrs+1011_1_to=lpo:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=occurrence:lcm=reverse:urr=ec_only:gs=on:random_seed=174455876:i=4547:bd=preordered_2912 on theBenchmark for (2912ds/4547Mi)
% 77.17/11.93 % (1203497)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 77.17/11.93 % (1203497)------------------------------
% 77.17/11.93 % (1203497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.17/11.93 % (1203497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.17/11.93 % (1203497)CaDiCaL version: 2.1.3
% 77.17/11.93 % (1203497)Termination reason: Unknown
% 77.17/11.93 % (1203497)Termination phase: Saturation
% 77.17/11.93 % (1203497)Time elapsed: 0.361 s
% 77.17/11.93 % (1203497)Peak memory usage: 113 MB
% 77.17/11.93 % (1203497)Instructions burned: 541 (million)
% 77.17/11.93 % (1203501)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 77.17/11.93 % (1203501)------------------------------
% 77.17/11.93 % (1203501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.17/11.93 % (1203501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.17/11.93 % (1203501)CaDiCaL version: 2.1.3
% 77.17/11.93 % (1203501)Termination reason: Unknown
% 77.17/11.93 % (1203501)Termination phase: Saturation
% 77.17/11.93 % (1203501)Time elapsed: 0.197 s
% 77.17/11.93 % (1203501)Peak memory usage: 113 MB
% 77.17/11.93 % (1203501)Instructions burned: 547 (million)
% 77.17/11.93 % (1203506)lrs+1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:urr=ec_only:newcnf=on:random_seed=3138244814:i=9294:av=off_2910 on theBenchmark for (2910ds/9294Mi)
% 77.17/11.93 % (1203507)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=4037657346:i=32849:add=on_2909 on theBenchmark for (2909ds/32849Mi)
% 77.17/11.93 % (1203453)Instruction limit reached!
% 77.17/11.93 % (1203453)------------------------------
% 77.17/11.93 % (1203453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.17/11.93 % (1203453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.17/11.93 % (1203453)CaDiCaL version: 2.1.3
% 77.17/11.93 % (1203453)Termination reason: Instruction limit
% 77.17/11.93 % (1203453)Termination phase: Saturation
% 77.17/11.93 % (1203453)Time elapsed: 3.182 s
% 77.17/11.93 % (1203453)Peak memory usage: 123 MB
% 77.17/11.93 % (1203453)Instructions burned: 5471 (million)
% 77.17/11.93 % (1203503)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 77.17/11.93 % (1203503)------------------------------
% 77.17/11.93 % (1203503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.17/11.93 % (1203503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.17/11.93 % (1203503)CaDiCaL version: 2.1.3
% 77.17/11.93 % (1203503)Termination reason: Unknown
% 77.17/11.93 % (1203503)Termination phase: Saturation
% 77.17/11.93 % (1203503)Time elapsed: 0.360 s
% 77.17/11.93 % (1203503)Peak memory usage: 114 MB
% 77.17/11.93 % (1203503)Instructions burned: 543 (million)
% 77.17/11.93 % (1203507)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 77.17/11.93 % (1203507)------------------------------
% 77.17/11.93 % (1203507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.17/11.93 % (1203507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.17/11.93 % (1203507)CaDiCaL version: 2.1.3
% 77.17/11.93 % (1203507)Termination reason: Unknown
% 77.17/11.93 % (1203507)Termination phase: Saturation
% 77.17/11.93 % (1203507)Time elapsed: 0.196 s
% 77.17/11.93 % (1203507)Peak memory usage: 113 MB
% 77.17/11.93 % (1203507)Instructions burned: 543 (million)
% 77.17/11.93 % (1203510)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=504760693:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2907 on theBenchmark for (2907ds/4793Mi)
% 77.17/11.93 % (1203511)dis+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:prc=on:drc=off:sims=off:sp=const_frequency:sos=on:spb=non_intro:gs=on:updr=off:newcnf=on:random_seed=2246825896:i=4840:nm=4:av=off_2907 on theBenchmark for (2907ds/4840Mi)
% 77.17/11.93 % (1203512)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=3229310412:cts=off:i=5002_2906 on theBenchmark for (2906ds/5002Mi)
% 77.17/11.93 % (1203506)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 112.16/16.76 % (1203506)------------------------------
% 112.16/16.76 % (1203506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.76 % (1203506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.76 % (1203506)CaDiCaL version: 2.1.3
% 112.16/16.76 % (1203506)Termination reason: Unknown
% 112.16/16.76 % (1203506)Termination phase: Saturation
% 112.16/16.76 % (1203506)Time elapsed: 0.361 s
% 112.16/16.76 % (1203506)Peak memory usage: 114 MB
% 112.16/16.76 % (1203506)Instructions burned: 543 (million)
% 112.16/16.76 % (1203516)dis+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=3548263482:i=30479:sd=3:ss=axioms_2904 on theBenchmark for (2904ds/30479Mi)
% 112.16/16.76 % (1203512)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 112.16/16.76 % (1203512)------------------------------
% 112.16/16.76 % (1203512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.76 % (1203512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.76 % (1203512)CaDiCaL version: 2.1.3
% 112.16/16.76 % (1203512)Termination reason: Unknown
% 112.16/16.76 % (1203512)Termination phase: Saturation
% 112.16/16.76 % (1203512)Time elapsed: 0.196 s
% 112.16/16.76 % (1203512)Peak memory usage: 114 MB
% 112.16/16.76 % (1203512)Instructions burned: 542 (million)
% 112.16/16.76 % (1203510)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 112.16/16.76 % (1203510)------------------------------
% 112.16/16.76 % (1203510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.76 % (1203510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.76 % (1203510)CaDiCaL version: 2.1.3
% 112.16/16.76 % (1203510)Termination reason: Unknown
% 112.16/16.76 % (1203510)Termination phase: Saturation
% 112.16/16.76 % (1203510)Time elapsed: 0.363 s
% 112.16/16.76 % (1203510)Peak memory usage: 114 MB
% 112.16/16.76 % (1203510)Instructions burned: 543 (million)
% 112.16/16.76 % (1203511)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 112.16/16.76 % (1203511)------------------------------
% 112.16/16.76 % (1203511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.76 % (1203511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.76 % (1203511)CaDiCaL version: 2.1.3
% 112.16/16.76 % (1203511)Termination reason: Unknown
% 112.16/16.76 % (1203511)Termination phase: Saturation
% 112.16/16.76 % (1203511)Time elapsed: 0.363 s
% 112.16/16.76 % (1203511)Peak memory usage: 113 MB
% 112.16/16.76 % (1203511)Instructions burned: 543 (million)
% 112.16/16.76 % (1203518)lrs+1011_1_anc=none:ncem=casc2026/models/loop2.pt:sil=32000:tgt=full:npcc=on:fde=unused:sas=cadical:sp=const_frequency:spb=non_intro:lsd=10:lcm=predicate:rp=on:sac=on:newcnf=on:random_seed=701106261:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2903 on theBenchmark for (2903ds/11035Mi)
% 112.16/16.76 % (1203518)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 112.16/16.76 % (1203519)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=2504580369:i=5835_2902 on theBenchmark for (2902ds/5835Mi)
% 112.16/16.76 % (1203521)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=2669375025:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2901 on theBenchmark for (2901ds/5890Mi)
% 112.16/16.76 % (1203518)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 112.16/16.76 % (1203518)------------------------------
% 112.16/16.76 % (1203518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.76 % (1203518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.76 % (1203518)CaDiCaL version: 2.1.3
% 112.16/16.76 % (1203518)Termination reason: Unknown
% 112.16/16.76 % (1203518)Termination phase: Saturation
% 112.16/16.76 % (1203518)Time elapsed: 0.197 s
% 112.16/16.76 % (1203518)Peak memory usage: 114 MB
% 112.16/16.76 % (1203518)Instructions burned: 544 (million)
% 112.16/16.76 % (1203516)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 112.16/16.76 % (1203516)------------------------------
% 112.16/16.76 % (1203516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.16/16.76 % (1203516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.16/16.76 % (1203516)CaDiCaL version: 2.1.3
% 112.16/16.76 % (1203516)Termination reason: Unknown
% 130.03/19.17 % (1203516)Termination phase: Saturation
% 130.03/19.17 % (1203516)Time elapsed: 0.362 s
% 130.03/19.17 % (1203516)Peak memory usage: 113 MB
% 130.03/19.17 % (1203516)Instructions burned: 540 (million)
% 130.03/19.17 % (1203524)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=2536851169:cts=off:i=19910:ep=RS_2899 on theBenchmark for (2899ds/19910Mi)
% 130.03/19.17 % (1203525)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:drc=off:sp=arity:fd=preordered:s2agt=16:sac=on:random_seed=2221051763:i=20312:bd=preordered:fsr=off:er=filter_2899 on theBenchmark for (2899ds/20312Mi)
% 130.03/19.17 % (1203519)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 130.03/19.17 % (1203519)------------------------------
% 130.03/19.17 % (1203519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.03/19.17 % (1203519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.03/19.17 % (1203519)CaDiCaL version: 2.1.3
% 130.03/19.17 % (1203519)Termination reason: Unknown
% 130.03/19.17 % (1203519)Termination phase: Saturation
% 130.03/19.17 % (1203519)Time elapsed: 0.362 s
% 130.03/19.17 % (1203519)Peak memory usage: 113 MB
% 130.03/19.17 % (1203519)Instructions burned: 543 (million)
% 130.03/19.17 % (1203521)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 130.03/19.17 % (1203521)------------------------------
% 130.03/19.17 % (1203521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.03/19.17 % (1203521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.03/19.17 % (1203521)CaDiCaL version: 2.1.3
% 130.03/19.17 % (1203521)Termination reason: Unknown
% 130.03/19.17 % (1203521)Termination phase: Saturation
% 130.03/19.17 % (1203521)Time elapsed: 0.360 s
% 130.03/19.17 % (1203521)Peak memory usage: 114 MB
% 130.03/19.17 % (1203521)Instructions burned: 544 (million)
% 130.03/19.17 % (1203528)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal_then_units:urr=on:gs=on:sac=on:random_seed=418161221:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2896 on theBenchmark for (2896ds/13822Mi)
% 130.03/19.17 % (1203529)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=791570491:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2896 on theBenchmark for (2896ds/7144Mi)
% 130.03/19.17 % (1203525)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 130.03/19.17 % (1203525)------------------------------
% 130.03/19.17 % (1203525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.03/19.17 % (1203525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.03/19.17 % (1203525)CaDiCaL version: 2.1.3
% 130.03/19.17 % (1203525)Termination reason: Unknown
% 130.03/19.17 % (1203525)Termination phase: Saturation
% 130.03/19.17 % (1203525)Time elapsed: 0.361 s
% 130.03/19.17 % (1203525)Peak memory usage: 114 MB
% 130.03/19.17 % (1203525)Instructions burned: 543 (million)
% 130.03/19.17 % (1203532)lrs+21_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=2417495319:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2894 on theBenchmark for (2894ds/15184Mi)
% 130.03/19.17 % (1203528)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 130.03/19.17 % (1203528)------------------------------
% 130.03/19.17 % (1203528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.03/19.17 % (1203528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.03/19.17 % (1203528)CaDiCaL version: 2.1.3
% 130.03/19.17 % (1203528)Termination reason: Unknown
% 130.03/19.17 % (1203528)Termination phase: Saturation
% 130.03/19.17 % (1203528)Time elapsed: 0.359 s
% 130.03/19.17 % (1203528)Peak memory usage: 114 MB
% 130.03/19.17 % (1203528)Instructions burned: 543 (million)
% 130.03/19.17 % (1203534)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=1468050157:i=107375_2891 on theBenchmark for (2891ds/107375Mi)
% 130.03/19.17 % (1203532)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 130.03/19.17 % (1203532)------------------------------
% 130.03/19.17 % (1203532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 130.03/19.17 % (1203532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.03/19.17 % (1203532)CaDiCaL version: 2.1.3
% 130.03/19.17 % (1203532)Termination reason: Unknown
% 122.07/20.48 % (1203532)Termination phase: Saturation
% 122.07/20.48 % (1203532)Time elapsed: 0.358 s
% 122.07/20.48 % (1203532)Peak memory usage: 114 MB
% 122.07/20.48 % (1203532)Instructions burned: 544 (million)
% 122.07/20.48 % (1203536)dis+11_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=full:npcc=on:sp=const_frequency:spb=units:lcm=predicate:fd=off:sac=on:newcnf=on:random_seed=3310266878:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2889 on theBenchmark for (2889ds/7958Mi)
% 122.07/20.48 % (1203534)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 122.07/20.48 % (1203534)------------------------------
% 122.07/20.48 % (1203534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.07/20.48 % (1203534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.07/20.48 % (1203534)CaDiCaL version: 2.1.3
% 122.07/20.48 % (1203534)Termination reason: Unknown
% 122.07/20.48 % (1203534)Termination phase: Saturation
% 122.07/20.48 % (1203534)Time elapsed: 0.361 s
% 122.07/20.48 % (1203534)Peak memory usage: 113 MB
% 122.07/20.48 % (1203534)Instructions burned: 543 (million)
% 122.07/20.48 % (1203538)dis+10_128_sil=16000:nwc=0.7:random_seed=957548119:i=15999:nm=2:gsp=on_2886 on theBenchmark for (2886ds/15999Mi)
% 122.07/20.48 % (1203538)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 122.07/20.48 % (1203536)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 122.07/20.48 % (1203536)------------------------------
% 122.07/20.48 % (1203536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.07/20.48 % (1203536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.07/20.48 % (1203536)CaDiCaL version: 2.1.3
% 122.07/20.48 % (1203536)Termination reason: Unknown
% 122.07/20.48 % (1203536)Termination phase: Saturation
% 122.07/20.48 % (1203536)Time elapsed: 0.359 s
% 122.07/20.48 % (1203536)Peak memory usage: 114 MB
% 122.07/20.48 % (1203536)Instructions burned: 543 (million)
% 122.07/20.48 % (1203540)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=2724636608:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2883 on theBenchmark for (2883ds/8139Mi)
% 122.07/20.48 % (1203529)Instruction limit reached!
% 122.07/20.48 % (1203529)------------------------------
% 122.07/20.48 % (1203529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.07/20.48 % (1203529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.07/20.48 % (1203529)CaDiCaL version: 2.1.3
% 122.07/20.48 % (1203529)Termination reason: Instruction limit
% 122.07/20.48 % (1203529)Termination phase: Saturation
% 122.07/20.48 % (1203529)Time elapsed: 4.359 s
% 122.07/20.48 % (1203529)Peak memory usage: 149 MB
% 122.07/20.48 % (1203529)Instructions burned: 7145 (million)
% 122.07/20.48 % (1203780)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=3803345238:st=4:i=8950:sd=5:ss=axioms_2851 on theBenchmark for (2851ds/8950Mi)
% 122.07/20.48 % (1203524)Instruction limit reached!
% 122.07/20.48 % (1203524)------------------------------
% 122.07/20.48 % (1203524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.07/20.48 % (1203524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.07/20.48 % (1203524)CaDiCaL version: 2.1.3
% 122.07/20.48 % (1203524)Termination reason: Instruction limit
% 122.07/20.48 % (1203524)Termination phase: Saturation
% 122.07/20.48 % (1203524)Time elapsed: 5.268 s
% 122.07/20.48 % (1203524)Peak memory usage: 255 MB
% 122.07/20.48 % (1203524)Instructions burned: 19912 (million)
% 122.07/20.48 % (1203798)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=1926344827:i=9809:ins=10:av=off_2845 on theBenchmark for (2845ds/9809Mi)
% 122.07/20.48 % (1203780)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 122.07/20.48 % (1203780)------------------------------
% 122.07/20.48 % (1203780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.07/20.48 % (1203780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.07/20.48 % (1203780)CaDiCaL version: 2.1.3
% 122.07/20.48 % (1203780)Termination reason: Unknown
% 122.07/20.48 % (1203780)Termination phase: Saturation
% 122.07/20.48 % (1203780)Time elapsed: 0.568 s
% 122.07/20.48 % (1203780)Peak memory usage: 113 MB
% 122.07/20.48 % (1203780)Instructions burned: 544 (million)
% 122.07/20.48 % (1203798)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 122.07/20.48 % (1203798)------------------------------
% 122.07/20.48 % (1203798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.07/20.48 % (1203798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.07/20.48 % (1203798)CaDiCaL version: 2.1.3
% 122.07/20.48 % (1203798)Termination reason: Unknown
% 122.07/20.48 % (1203798)Termination phase: Saturation
% 122.07/20.48 % (1203798)Time elapsed: 0.253 s
% 122.07/20.48 % (1203798)Peak memory usage: 114 MB
% 122.07/20.48 % (1203798)Instructions burned: 544 (million)
% 122.07/20.48 % (1203808)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=63502187:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2842 on theBenchmark for (2842ds/9885Mi)
% 122.07/20.48 % (1203814)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=322690414:cond=fast:i=32078:fgj=on:av=off_2840 on theBenchmark for (2840ds/32078Mi)
% 122.07/20.48 % (1203814)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 122.07/20.48 % (1203814)------------------------------
% 122.07/20.48 % (1203814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.07/20.48 % (1203814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.07/20.48 % (1203814)CaDiCaL version: 2.1.3
% 122.07/20.48 % (1203814)Termination reason: Unknown
% 122.07/20.48 % (1203814)Termination phase: Saturation
% 122.07/20.48 % (1203814)Time elapsed: 0.295 s
% 122.07/20.48 % (1203814)Peak memory usage: 114 MB
% 122.07/20.48 % (1203814)Instructions burned: 543 (million)
% 122.07/20.48 % (1203808)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 122.07/20.48 % (1203808)------------------------------
% 122.07/20.48 % (1203808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.07/20.48 % (1203808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.07/20.48 % (1203808)CaDiCaL version: 2.1.3
% 122.07/20.48 % (1203808)Termination reason: Unknown
% 122.07/20.48 % (1203808)Termination phase: Saturation
% 122.07/20.48 % (1203808)Time elapsed: 0.557 s
% 122.07/20.48 % (1203808)Peak memory usage: 114 MB
% 122.07/20.48 % (1203808)Instructions burned: 543 (million)
% 122.07/20.48 % (1203829)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=3266662673:i=11101:bd=all:ss=axioms:sgt=8_2835 on theBenchmark for (2835ds/11101Mi)
% 122.07/20.48 % (1203833)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=3935695850:cond=on:i=13220:s2at=3:aac=none:fsd=on_2834 on theBenchmark for (2834ds/13220Mi)
% 122.07/20.48 % (1203833)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 122.07/20.48 % (1203833)------------------------------
% 122.07/20.48 % (1203833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.07/20.48 % (1203833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.07/20.48 % (1203833)CaDiCaL version: 2.1.3
% 122.07/20.48 % (1203833)Termination reason: Unknown
% 122.07/20.48 % (1203833)Termination phase: Saturation
% 122.07/20.48 % (1203833)Time elapsed: 0.560 s
% 122.07/20.48 % (1203833)Peak memory usage: 114 MB
% 122.07/20.48 % (1203833)Instructions burned: 544 (million)
% 122.07/20.48 % (1203540)Instruction limit reached!
% 122.07/20.48 % (1203540)------------------------------
% 122.07/20.48 % (1203540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.07/20.48 % (1203540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.07/20.48 % (1203540)CaDiCaL version: 2.1.3
% 122.07/20.48 % (1203540)Termination reason: Instruction limit
% 122.07/20.48 % (1203540)Termination phase: Saturation
% 122.07/20.48 % (1203540)Time elapsed: 5.662 s
% 122.07/20.48 % (1203540)Peak memory usage: 135 MB
% 122.07/20.48 % (1203540)Instructions burned: 8140 (million)
% 122.07/20.48 % (1203857)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=3391172134:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2825 on theBenchmark for (2825ds/13528Mi)
% 122.07/20.48 % (1203858)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:sp=reverse_frequency:bce=on:bsr=unit_only:s2agt=32:newcnf=on:random_seed=2142707343:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2825 on theBenchmark for (2825ds/14854Mi)
% 122.07/20.48 % (1203858)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 122.07/20.48 % (1203858)------------------------------
% 122.07/20.48 % (1203858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.07/20.48 % (1203858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.07/20.48 % (1203858)CaDiCaL version: 2.1.3
% 122.07/20.48 % (1203858)Termination reason: Unknown
% 122.07/20.48 % (1203858)Termination phase: Saturation
% 122.07/20.48 % (1203858)Time elapsed: 0.588 s
% 122.07/20.48 % (1203858)Peak memory usage: 114 MB
% 122.07/20.48 % (1203858)Instructions burned: 554 (million)
% 122.07/20.48 % (1203857)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 122.07/20.48 % (1203857)------------------------------
% 122.07/20.48 % (1203857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.07/20.48 % (1203857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.07/20.48 % (1203857)CaDiCaL version: 2.1.3
% 122.07/20.48 % (1203857)Termination reason: Unknown
% 122.07/20.48 % (1203857)Termination phase: Saturation
% 122.07/20.48 % (1203857)Time elapsed: 0.604 s
% 122.07/20.48 % (1203857)Peak memory usage: 114 MB
% 122.07/20.48 % (1203857)Instructions burned: 547 (million)
% 122.07/20.48 % (1203878)lrs-1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:sas=cadical:sp=arity:spb=units:lsd=1:acc=on:urr=ec_only:fd=preordered:gs=on:s2agt=16:random_seed=1976706253:i=33081:aac=none:fgj=on:bd=all:fsr=off_2816 on theBenchmark for (2816ds/33081Mi)
% 122.07/20.48 % (1203876)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=611835926:i=14974:ss=axioms:sgt=16_2816 on theBenchmark for (2816ds/14974Mi)
% 122.07/20.48 % (1203406)First to succeed.
% 122.07/20.48 % (1203406)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1203287"
% 122.07/20.48 % (1203878)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 122.07/20.48 % (1203878)------------------------------
% 122.07/20.48 % (1203878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.07/20.48 % (1203878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.07/20.48 % (1203878)CaDiCaL version: 2.1.3
% 122.07/20.48 % (1203878)Termination reason: Unknown
% 122.07/20.48 % (1203878)Termination phase: Saturation
% 122.07/20.48 % (1203878)Time elapsed: 0.604 s
% 122.07/20.48 % (1203878)Peak memory usage: 114 MB
% 122.07/20.48 % (1203878)Instructions burned: 544 (million)
% 122.07/20.48 % (1203876)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 122.07/20.48 % (1203876)------------------------------
% 122.07/20.48 % (1203876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.07/20.48 % (1203876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.07/20.48 % (1203876)CaDiCaL version: 2.1.3
% 122.07/20.48 % (1203876)Termination reason: Unknown
% 122.07/20.48 % (1203876)Termination phase: Saturation
% 122.07/20.48 % (1203876)Time elapsed: 0.600 s
% 122.07/20.48 % (1203876)Peak memory usage: 113 MB
% 122.07/20.48 % (1203876)Instructions burned: 543 (million)
% 122.07/20.48 % (1203892)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sims=off:sas=cadical:etr=on:spb=goal:acc=on:s2agt=60:alpa=true:random_seed=2983695448:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2808 on theBenchmark for (2808ds/50856Mi)
% 122.07/20.48 % (1203893)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=559301942:i=69865_2807 on theBenchmark for (2807ds/69865Mi)
% 122.07/20.48 % (1203406)Refutation found. Thanks to Tanya!
% 122.07/20.48 % SZS status Theorem for theBenchmark
% 122.07/20.48 % SZS output start Proof for theBenchmark
% See solution above
% 139.42/20.78 % (1203406)------------------------------
% 139.42/20.78 % (1203406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.42/20.78 % (1203406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.42/20.78 % (1203406)CaDiCaL version: 2.1.3
% 139.42/20.78 % (1203406)Termination reason: Refutation
% 139.42/20.78 % (1203406)Time elapsed: 15.463 s
% 139.42/20.78 % (1203406)Peak memory usage: 213 MB
% 139.42/20.78 % (1203406)Instructions burned: 22447 (million)
% 139.42/20.78 % (1203406)------------------------------
% 139.42/20.78 % (1203406)------------------------------
% 139.42/20.78 % (1203287)Success in time 19.623 s
% 139.42/20.78 % Vampire exiting
%------------------------------------------------------------------------------