%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : COM038_5 : TPTP v9.3.1. Released v6.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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 09:39:27 AM UTC 2026
% Result : Theorem 120.07s 17.43s
% Output : Refutation 120.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 28
% Syntax : Number of formulae : 181 ( 47 unt; 0 typ; 2 def)
% Number of atoms : 372 ( 106 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 349 ( 158 ~; 158 |; 6 &)
% ( 8 <=>; 18 =>; 0 <=; 1 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 25 ( 23 usr; 3 prp; 0-3 aty)
% Number of functors : 35 ( 35 usr; 11 con; 0-5 aty)
% Number of variables : 308 ( 0 sgn 305 !; 3 ?; 308 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
bool: $tType ).
tff(type_def_6,type,
int: $tType ).
tff(type_def_7,type,
list: $tType > $tType ).
tff(type_def_8,type,
atom: $tType ).
tff(type_def_9,type,
fun: ( $tType * $tType ) > $tType ).
tff(func_def_0,type,
combk:
!>[X0: $tType,X1: $tType] : fun(X0,fun(X1,X0)) ).
tff(func_def_1,type,
div_mod:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_2,type,
one_one:
!>[X0: $tType] : X0 ).
tff(func_def_3,type,
plus_plus:
!>[X0: $tType] : fun(X0,fun(X0,X0)) ).
tff(func_def_4,type,
times_times:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_5,type,
zero_zero:
!>[X0: $tType] : X0 ).
tff(func_def_6,type,
iprod:
!>[X0: $tType] : ( ( list(X0) * list(X0) ) > X0 ) ).
tff(func_def_7,type,
zipwith0:
!>[X0: $tType,X1: $tType,X2: $tType] : ( fun(X0,fun(X1,X2)) > fun(list(X0),fun(list(X1),list(X2))) ) ).
tff(func_def_8,type,
cons:
!>[X0: $tType] : ( ( X0 * list(X0) ) > list(X0) ) ).
tff(func_def_9,type,
list_case:
!>[X0: $tType,X1: $tType] : ( ( X0 * fun(X1,fun(list(X1),X0)) * list(X1) ) > X0 ) ).
tff(func_def_10,type,
list_rec:
!>[X0: $tType,X1: $tType] : ( ( X0 * fun(X1,fun(list(X1),fun(X0,X0))) * list(X1) ) > X0 ) ).
tff(func_def_11,type,
splice:
!>[X0: $tType] : ( ( list(X0) * list(X0) ) > list(X0) ) ).
tff(func_def_12,type,
asubst: ( int * list(int) * atom ) > atom ).
tff(func_def_13,type,
dvd: ( int * int * list(int) ) > atom ).
tff(func_def_14,type,
c_PresArith_Oatom_OLe: ( int * list(int) ) > atom ).
tff(func_def_15,type,
atom_case:
!>[X0: $tType] : ( ( fun(int,fun(list(int),X0)) * fun(int,fun(int,fun(list(int),X0))) * fun(int,fun(int,fun(list(int),X0))) * atom ) > X0 ) ).
tff(func_def_16,type,
atom_rec:
!>[X0: $tType] : ( ( fun(int,fun(list(int),X0)) * fun(int,fun(int,fun(list(int),X0))) * fun(int,fun(int,fun(list(int),X0))) * atom ) > X0 ) ).
tff(func_def_17,type,
divisor: atom > int ).
tff(func_def_18,type,
hd_coeff: atom > int ).
tff(func_def_19,type,
aa:
!>[X0: $tType,X1: $tType] : ( ( fun(X0,X1) * X0 ) > X1 ) ).
tff(func_def_20,type,
fFalse: bool ).
tff(func_def_21,type,
fTrue: bool ).
tff(func_def_22,type,
a: atom ).
tff(func_def_23,type,
d: int ).
tff(func_def_24,type,
e: list(int) ).
tff(func_def_25,type,
i: int ).
tff(func_def_26,type,
j: int ).
tff(func_def_27,type,
ks1: list(int) ).
tff(func_def_28,type,
ks: list(int) ).
tff(func_def_29,type,
l: int ).
tff(func_def_30,type,
sK0: list(int) ).
tff(func_def_31,type,
sK1: ( int * int ) > int ).
tff(func_def_32,type,
sK2:
!>[X0: $tType,X1: $tType] : ( ( fun(X1,X0) * fun(X1,X0) ) > X1 ) ).
tff(pred_def_1,type,
one:
!>[X0: $tType] : $o ).
tff(pred_def_2,type,
idom:
!>[X0: $tType] : $o ).
tff(pred_def_3,type,
ring:
!>[X0: $tType] : $o ).
tff(pred_def_4,type,
cl_Groups_Oplus:
!>[X0: $tType] : $o ).
tff(pred_def_5,type,
zero:
!>[X0: $tType] : $o ).
tff(pred_def_6,type,
mult_zero:
!>[X0: $tType] : $o ).
tff(pred_def_7,type,
monoid_add:
!>[X0: $tType] : $o ).
tff(pred_def_8,type,
monoid_mult:
!>[X0: $tType] : $o ).
tff(pred_def_9,type,
semiring_div:
!>[X0: $tType] : $o ).
tff(pred_def_10,type,
comm_semiring_1:
!>[X0: $tType] : $o ).
tff(pred_def_11,type,
comm_monoid_add:
!>[X0: $tType] : $o ).
tff(pred_def_12,type,
ab_semigroup_add:
!>[X0: $tType] : $o ).
tff(pred_def_13,type,
comm_monoid_mult:
!>[X0: $tType] : $o ).
tff(pred_def_14,type,
ab_semigroup_mult:
!>[X0: $tType] : $o ).
tff(pred_def_15,type,
cancel_semigroup_add:
!>[X0: $tType] : $o ).
tff(pred_def_16,type,
ring_n68954251visors:
!>[X0: $tType] : $o ).
tff(pred_def_17,type,
cancel146912293up_add:
!>[X0: $tType] : $o ).
tff(pred_def_18,type,
linord219039673up_add:
!>[X0: $tType] : $o ).
tff(pred_def_19,type,
i_Z: ( atom * list(int) ) > $o ).
tff(pred_def_20,type,
dvd_dvd:
!>[X0: $tType] : ( ( X0 * X0 ) > $o ) ).
tff(pred_def_21,type,
pp: bool > $o ).
tff(f1,axiom,
a = dvd(d,l,ks),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_Dvd) ).
tff(f2,axiom,
div_mod(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),aa(int,int,aa(int,fun(int,int),plus_plus(int),i),iprod(int,ks1,e))),d) = div_mod(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),aa(int,int,aa(int,fun(int,int),plus_plus(int),j),iprod(int,ks1,e))),d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1__096_Il_A_L_A_Ii_A_L_A_092_060langle_062ks_H_Me_092_060rangle_062_J_J_Amod_Ad_A_061_Il_A_L_A_Ij_A_L_A_092_060langle_062ks_H_Me_092_060rangle_062_J_J_Amod_Ad_096) ).
tff(f4,axiom,
ks = cons(int,one_one(int),ks1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3__096ks_A_061_A1_A_D_Aks_H_096) ).
tff(f20,axiom,
! [X0: $tType] :
( semiring_div(X0)
=> ! [X1: X0,X2: X0] : ( div_mod(X0,aa(X0,X0,aa(X0,fun(X0,X0),plus_plus(X0),X2),X1),X2) = div_mod(X0,X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_mod__add__self1) ).
tff(f38,axiom,
! [X0: list(int),X1: list(int),X2: int,X3: int] :
( i_Z(dvd(X3,X2,X1),X0)
<=> dvd_dvd(int,X3,aa(int,int,aa(int,fun(int,int),plus_plus(int),X2),iprod(int,X1,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_I_092_060_094isub_062Z_Osimps_I2_J) ).
tff(f41,axiom,
! [X0: $tType] :
( ring(X0)
=> ! [X1: list(X0),X2: X0,X3: list(X0),X4: X0] : ( iprod(X0,cons(X0,X4,X3),cons(X0,X2,X1)) = aa(X0,X0,aa(X0,fun(X0,X0),plus_plus(X0),times_times(X0,X4,X2)),iprod(X0,X3,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_iprod__Cons) ).
tff(f48,axiom,
! [X0: int] : ( div_mod(int,zero_zero(int),X0) = zero_zero(int) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_zmod__zero) ).
tff(f49,axiom,
! [X0: int] : ( div_mod(int,X0,X0) = zero_zero(int) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_zmod__self) ).
tff(f51,axiom,
! [X0: $tType] :
( semiring_div(X0)
=> ! [X1: X0,X2: X0] : ( div_mod(X0,times_times(X0,X2,X1),X1) = zero_zero(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_mod__mult__self2__is__0) ).
tff(f53,axiom,
! [X0: $tType] :
( semiring_div(X0)
=> ! [X1: X0] : ( div_mod(X0,X1,one_one(X0)) = zero_zero(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_mod__by__1) ).
tff(f57,axiom,
! [X0: $tType] :
( semiring_div(X0)
=> ! [X1: X0,X2: X0] :
( dvd_dvd(X0,X2,X1)
<=> ( div_mod(X0,X1,X2) = zero_zero(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_dvd__eq__mod__eq__0) ).
tff(f58,axiom,
! [X0: int,X1: int] :
( ( div_mod(int,X1,X0) = zero_zero(int) )
<=> ? [X2: int] : ( X1 = times_times(int,X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_zmod__eq__0__iff) ).
tff(f67,axiom,
! [X0: $tType] :
( comm_monoid_mult(X0)
=> ! [X1: X0] : ( times_times(X0,X1,one_one(X0)) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_mult_Ocomm__neutral) ).
tff(f69,axiom,
! [X0: $tType] :
( comm_monoid_mult(X0)
=> ! [X1: X0] : ( times_times(X0,one_one(X0),X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_mult__1) ).
tff(f71,axiom,
! [X0: int,X1: int,X2: int] :
( dvd_dvd(int,X2,div_mod(int,X1,X0))
=> ( dvd_dvd(int,X2,X0)
=> dvd_dvd(int,X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_zdvd__zmod__imp__zdvd) ).
tff(f72,axiom,
! [X0: int,X1: int,X2: int] :
( dvd_dvd(int,X2,X1)
=> ( dvd_dvd(int,X2,X0)
=> dvd_dvd(int,X2,div_mod(int,X1,X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_zdvd__zmod) ).
tff(f75,axiom,
! [X0: $tType] :
( semiring_div(X0)
=> ! [X1: X0,X2: X0,X3: X0] : ( div_mod(X0,times_times(X0,div_mod(X0,X3,X2),X1),X2) = div_mod(X0,times_times(X0,X3,X1),X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_zmod__simps_I4_J) ).
tff(f76,axiom,
! [X0: $tType] :
( semiring_div(X0)
=> ! [X1: X0,X2: X0,X3: X0] : ( div_mod(X0,times_times(X0,X3,X2),times_times(X0,X1,X2)) = times_times(X0,div_mod(X0,X3,X1),X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_mod__mult__mult2) ).
tff(f87,axiom,
! [X0: $tType] :
( semiring_div(X0)
=> ! [X1: X0] : ( div_mod(X0,X1,zero_zero(X0)) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_mod__by__0) ).
tff(f93,axiom,
! [X0: $tType] :
( comm_semiring_1(X0)
=> ! [X1: X0] : dvd_dvd(X0,X1,zero_zero(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_dvd__0__right) ).
tff(f98,axiom,
! [X0: $tType] :
( comm_semiring_1(X0)
=> ! [X1: X0,X2: X0,X3: X0] :
( dvd_dvd(X0,X3,X2)
=> ( dvd_dvd(X0,X2,X1)
=> dvd_dvd(X0,X3,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_dvd__trans) ).
tff(f104,axiom,
comm_monoid_mult(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Groups_Ocomm__monoid__mult) ).
tff(f107,axiom,
comm_semiring_1(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Ocomm__semiring__1) ).
tff(f108,axiom,
semiring_div(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Divides_Osemiring__div) ).
tff(f114,axiom,
ring(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Oring) ).
tff(f125,conjecture,
( i_Z(a,cons(int,i,e))
<=> i_Z(a,cons(int,j,e)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
tff(f126,negated_conjecture,
~ ( i_Z(a,cons(int,i,e))
<=> i_Z(a,cons(int,j,e)) ),
inference(negated_conjecture,[status(cth)],[f125]) ).
tff(f129,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0] : ( div_mod(X0,aa(X0,X0,aa(X0,fun(X0,X0),plus_plus(X0),X2),X1),X2) = div_mod(X0,X1,X2) )
| ~ semiring_div(X0) ),
inference(ennf_transformation,[],[f20]) ).
tff(f151,plain,
! [X0: $tType] :
( ! [X1: list(X0),X2: X0,X3: list(X0),X4: X0] : ( iprod(X0,cons(X0,X4,X3),cons(X0,X2,X1)) = aa(X0,X0,aa(X0,fun(X0,X0),plus_plus(X0),times_times(X0,X4,X2)),iprod(X0,X3,X1)) )
| ~ ring(X0) ),
inference(ennf_transformation,[],[f41]) ).
tff(f157,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0] : ( div_mod(X0,times_times(X0,X2,X1),X1) = zero_zero(X0) )
| ~ semiring_div(X0) ),
inference(ennf_transformation,[],[f51]) ).
tff(f159,plain,
! [X0: $tType] :
( ! [X1: X0] : ( div_mod(X0,X1,one_one(X0)) = zero_zero(X0) )
| ~ semiring_div(X0) ),
inference(ennf_transformation,[],[f53]) ).
tff(f162,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0] :
( dvd_dvd(X0,X2,X1)
<=> ( div_mod(X0,X1,X2) = zero_zero(X0) ) )
| ~ semiring_div(X0) ),
inference(ennf_transformation,[],[f57]) ).
tff(f172,plain,
! [X0: $tType] :
( ! [X1: X0] : ( times_times(X0,X1,one_one(X0)) = X1 )
| ~ comm_monoid_mult(X0) ),
inference(ennf_transformation,[],[f67]) ).
tff(f174,plain,
! [X0: $tType] :
( ! [X1: X0] : ( times_times(X0,one_one(X0),X1) = X1 )
| ~ comm_monoid_mult(X0) ),
inference(ennf_transformation,[],[f69]) ).
tff(f176,plain,
! [X0: int,X1: int,X2: int] :
( dvd_dvd(int,X2,X1)
| ~ dvd_dvd(int,X2,X0)
| ~ dvd_dvd(int,X2,div_mod(int,X1,X0)) ),
inference(ennf_transformation,[],[f71]) ).
tff(f177,plain,
! [X0: int,X1: int,X2: int] :
( dvd_dvd(int,X2,X1)
| ~ dvd_dvd(int,X2,X0)
| ~ dvd_dvd(int,X2,div_mod(int,X1,X0)) ),
inference(flattening,[],[f176]) ).
tff(f178,plain,
! [X0: int,X1: int,X2: int] :
( dvd_dvd(int,X2,div_mod(int,X1,X0))
| ~ dvd_dvd(int,X2,X0)
| ~ dvd_dvd(int,X2,X1) ),
inference(ennf_transformation,[],[f72]) ).
tff(f179,plain,
! [X0: int,X1: int,X2: int] :
( dvd_dvd(int,X2,div_mod(int,X1,X0))
| ~ dvd_dvd(int,X2,X0)
| ~ dvd_dvd(int,X2,X1) ),
inference(flattening,[],[f178]) ).
tff(f183,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0,X3: X0] : ( div_mod(X0,times_times(X0,div_mod(X0,X3,X2),X1),X2) = div_mod(X0,times_times(X0,X3,X1),X2) )
| ~ semiring_div(X0) ),
inference(ennf_transformation,[],[f75]) ).
tff(f184,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0,X3: X0] : ( div_mod(X0,times_times(X0,X3,X2),times_times(X0,X1,X2)) = times_times(X0,div_mod(X0,X3,X1),X2) )
| ~ semiring_div(X0) ),
inference(ennf_transformation,[],[f76]) ).
tff(f193,plain,
! [X0: $tType] :
( ! [X1: X0] : ( div_mod(X0,X1,zero_zero(X0)) = X1 )
| ~ semiring_div(X0) ),
inference(ennf_transformation,[],[f87]) ).
tff(f196,plain,
! [X0: $tType] :
( ! [X1: X0] : dvd_dvd(X0,X1,zero_zero(X0))
| ~ comm_semiring_1(X0) ),
inference(ennf_transformation,[],[f93]) ).
tff(f201,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0,X3: X0] :
( dvd_dvd(X0,X3,X1)
| ~ dvd_dvd(X0,X2,X1)
| ~ dvd_dvd(X0,X3,X2) )
| ~ comm_semiring_1(X0) ),
inference(ennf_transformation,[],[f98]) ).
tff(f202,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0,X3: X0] :
( dvd_dvd(X0,X3,X1)
| ~ dvd_dvd(X0,X2,X1)
| ~ dvd_dvd(X0,X3,X2) )
| ~ comm_semiring_1(X0) ),
inference(flattening,[],[f201]) ).
tff(f205,plain,
( i_Z(a,cons(int,i,e))
<~> i_Z(a,cons(int,j,e)) ),
inference(ennf_transformation,[],[f126]) ).
tff(f215,plain,
! [X0: list(int),X1: list(int),X2: int,X3: int] :
( ( i_Z(dvd(X3,X2,X1),X0)
| ~ dvd_dvd(int,X3,aa(int,int,aa(int,fun(int,int),plus_plus(int),X2),iprod(int,X1,X0))) )
& ( dvd_dvd(int,X3,aa(int,int,aa(int,fun(int,int),plus_plus(int),X2),iprod(int,X1,X0)))
| ~ i_Z(dvd(X3,X2,X1),X0) ) ),
inference(nnf_transformation,[],[f38]) ).
tff(f219,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0] :
( ( dvd_dvd(X0,X2,X1)
| ( div_mod(X0,X1,X2) != zero_zero(X0) ) )
& ( ( div_mod(X0,X1,X2) = zero_zero(X0) )
| ~ dvd_dvd(X0,X2,X1) ) )
| ~ semiring_div(X0) ),
inference(nnf_transformation,[],[f162]) ).
tff(f220,plain,
! [X0: int,X1: int] :
( ( ( div_mod(int,X1,X0) = zero_zero(int) )
| ! [X2: int] : ( times_times(int,X0,X2) != X1 ) )
& ( ? [X2: int] : ( X1 = times_times(int,X0,X2) )
| ( zero_zero(int) != div_mod(int,X1,X0) ) ) ),
inference(nnf_transformation,[],[f58]) ).
tff(f221,plain,
! [X0: int,X1: int] :
( ( ( div_mod(int,X1,X0) = zero_zero(int) )
| ! [X2: int] : ( times_times(int,X0,X2) != X1 ) )
& ( ? [X3: int] : ( times_times(int,X0,X3) = X1 )
| ( zero_zero(int) != div_mod(int,X1,X0) ) ) ),
inference(rectify,[],[f220]) ).
tff(f222,plain,
! [X0: int,X1: int] :
( ( ( div_mod(int,X1,X0) = zero_zero(int) )
| ! [X2: int] : ( times_times(int,X0,X2) != X1 ) )
& ( ( times_times(int,X0,sK1(X0,X1)) = X1 )
| ( zero_zero(int) != div_mod(int,X1,X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X3,sK1(X0,X1))],[f221]) ).
tff(f233,plain,
( ( ~ i_Z(a,cons(int,j,e))
| ~ i_Z(a,cons(int,i,e)) )
& ( i_Z(a,cons(int,j,e))
| i_Z(a,cons(int,i,e)) ) ),
inference(nnf_transformation,[],[f205]) ).
tff(f234,plain,
a = dvd(d,l,ks),
inference(cnf_transformation,[],[f1]) ).
tff(f235,plain,
div_mod(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),aa(int,int,aa(int,fun(int,int),plus_plus(int),i),iprod(int,ks1,e))),d) = div_mod(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),aa(int,int,aa(int,fun(int,int),plus_plus(int),j),iprod(int,ks1,e))),d),
inference(cnf_transformation,[],[f2]) ).
tff(f237,plain,
ks = cons(int,one_one(int),ks1),
inference(cnf_transformation,[],[f4]) ).
tff(f259,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ~ semiring_div(X0)
| ( div_mod(X0,aa(X0,X0,aa(X0,fun(X0,X0),plus_plus(X0),X2),X1),X2) = div_mod(X0,X1,X2) ) ),
inference(cnf_transformation,[],[f129]) ).
tff(f280,plain,
! [X2: int,X3: int,X0: list(int),X1: list(int)] :
( dvd_dvd(int,X3,aa(int,int,aa(int,fun(int,int),plus_plus(int),X2),iprod(int,X1,X0)))
| ~ i_Z(dvd(X3,X2,X1),X0) ),
inference(cnf_transformation,[],[f215]) ).
tff(f281,plain,
! [X2: int,X3: int,X0: list(int),X1: list(int)] :
( ~ dvd_dvd(int,X3,aa(int,int,aa(int,fun(int,int),plus_plus(int),X2),iprod(int,X1,X0)))
| i_Z(dvd(X3,X2,X1),X0) ),
inference(cnf_transformation,[],[f215]) ).
tff(f284,plain,
! [X0: $tType,X2: X0,X3: list(X0),X1: list(X0),X4: X0] :
( ~ ring(X0)
| ( iprod(X0,cons(X0,X4,X3),cons(X0,X2,X1)) = aa(X0,X0,aa(X0,fun(X0,X0),plus_plus(X0),times_times(X0,X4,X2)),iprod(X0,X3,X1)) ) ),
inference(cnf_transformation,[],[f151]) ).
tff(f294,plain,
! [X0: int] : ( zero_zero(int) = div_mod(int,zero_zero(int),X0) ),
inference(cnf_transformation,[],[f48]) ).
tff(f295,plain,
! [X0: int] : ( zero_zero(int) = div_mod(int,X0,X0) ),
inference(cnf_transformation,[],[f49]) ).
tff(f297,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ~ semiring_div(X0)
| ( zero_zero(X0) = div_mod(X0,times_times(X0,X2,X1),X1) ) ),
inference(cnf_transformation,[],[f157]) ).
tff(f299,plain,
! [X0: $tType,X1: X0] :
( ~ semiring_div(X0)
| ( zero_zero(X0) = div_mod(X0,X1,one_one(X0)) ) ),
inference(cnf_transformation,[],[f159]) ).
tff(f303,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ~ semiring_div(X0)
| ~ dvd_dvd(X0,X2,X1)
| ( div_mod(X0,X1,X2) = zero_zero(X0) ) ),
inference(cnf_transformation,[],[f219]) ).
tff(f304,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ~ semiring_div(X0)
| ( div_mod(X0,X1,X2) != zero_zero(X0) )
| dvd_dvd(X0,X2,X1) ),
inference(cnf_transformation,[],[f219]) ).
tff(f305,plain,
! [X0: int,X1: int] :
( ( times_times(int,X0,sK1(X0,X1)) = X1 )
| ( zero_zero(int) != div_mod(int,X1,X0) ) ),
inference(cnf_transformation,[],[f222]) ).
tff(f306,plain,
! [X2: int,X0: int,X1: int] :
( ( zero_zero(int) = div_mod(int,X1,X0) )
| ( times_times(int,X0,X2) != X1 ) ),
inference(cnf_transformation,[],[f222]) ).
tff(f317,plain,
! [X0: $tType,X1: X0] :
( ~ comm_monoid_mult(X0)
| ( times_times(X0,X1,one_one(X0)) = X1 ) ),
inference(cnf_transformation,[],[f172]) ).
tff(f319,plain,
! [X0: $tType,X1: X0] :
( ~ comm_monoid_mult(X0)
| ( times_times(X0,one_one(X0),X1) = X1 ) ),
inference(cnf_transformation,[],[f174]) ).
tff(f321,plain,
! [X2: int,X0: int,X1: int] :
( ~ dvd_dvd(int,X2,X0)
| dvd_dvd(int,X2,X1)
| ~ dvd_dvd(int,X2,div_mod(int,X1,X0)) ),
inference(cnf_transformation,[],[f177]) ).
tff(f322,plain,
! [X2: int,X0: int,X1: int] :
( ~ dvd_dvd(int,X2,X1)
| ~ dvd_dvd(int,X2,X0)
| dvd_dvd(int,X2,div_mod(int,X1,X0)) ),
inference(cnf_transformation,[],[f179]) ).
tff(f325,plain,
! [X0: $tType,X2: X0,X3: X0,X1: X0] :
( ~ semiring_div(X0)
| ( div_mod(X0,times_times(X0,div_mod(X0,X3,X2),X1),X2) = div_mod(X0,times_times(X0,X3,X1),X2) ) ),
inference(cnf_transformation,[],[f183]) ).
tff(f326,plain,
! [X0: $tType,X2: X0,X3: X0,X1: X0] :
( ~ semiring_div(X0)
| ( div_mod(X0,times_times(X0,X3,X2),times_times(X0,X1,X2)) = times_times(X0,div_mod(X0,X3,X1),X2) ) ),
inference(cnf_transformation,[],[f184]) ).
tff(f337,plain,
! [X0: $tType,X1: X0] :
( ~ semiring_div(X0)
| ( div_mod(X0,X1,zero_zero(X0)) = X1 ) ),
inference(cnf_transformation,[],[f193]) ).
tff(f347,plain,
! [X0: $tType,X1: X0] :
( dvd_dvd(X0,X1,zero_zero(X0))
| ~ comm_semiring_1(X0) ),
inference(cnf_transformation,[],[f196]) ).
tff(f355,plain,
! [X0: $tType,X2: X0,X3: X0,X1: X0] :
( ~ comm_semiring_1(X0)
| ~ dvd_dvd(X0,X2,X1)
| ~ dvd_dvd(X0,X3,X2)
| dvd_dvd(X0,X3,X1) ),
inference(cnf_transformation,[],[f202]) ).
tff(f361,plain,
comm_monoid_mult(int),
inference(cnf_transformation,[],[f104]) ).
tff(f364,plain,
comm_semiring_1(int),
inference(cnf_transformation,[],[f107]) ).
tff(f365,plain,
semiring_div(int),
inference(cnf_transformation,[],[f108]) ).
tff(f371,plain,
ring(int),
inference(cnf_transformation,[],[f114]) ).
tff(f382,plain,
( i_Z(a,cons(int,j,e))
| i_Z(a,cons(int,i,e)) ),
inference(cnf_transformation,[],[f233]) ).
tff(f383,plain,
( ~ i_Z(a,cons(int,j,e))
| ~ i_Z(a,cons(int,i,e)) ),
inference(cnf_transformation,[],[f233]) ).
tff(f396,plain,
! [X2: int,X0: int] : ( zero_zero(int) = div_mod(int,times_times(int,X0,X2),X0) ),
inference(equality_resolution,[],[f306]) ).
tff(f405,definition,
( spl3_1
<=> i_Z(a,cons(int,i,e)) ),
introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition]) ).
tff(f406,plain,
( ~ i_Z(a,cons(int,i,e))
| spl3_1 ),
inference(avatar_component_clause,[],[f405]) ).
tff(f407,plain,
( i_Z(a,cons(int,i,e))
| ~ spl3_1 ),
inference(avatar_component_clause,[],[f405]) ).
tff(f409,definition,
( spl3_2
<=> i_Z(a,cons(int,j,e)) ),
introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition]) ).
tff(f410,plain,
( ~ i_Z(a,cons(int,j,e))
| spl3_2 ),
inference(avatar_component_clause,[],[f409]) ).
tff(f411,plain,
( i_Z(a,cons(int,j,e))
| ~ spl3_2 ),
inference(avatar_component_clause,[],[f409]) ).
tff(f412,plain,
( spl3_1
| spl3_2 ),
inference(avatar_split_clause,[],[f382,f409,f405]) ).
tff(f413,plain,
( ~ i_Z(a,cons(int,i,e))
| ~ spl3_2 ),
inference(forward_subsumption_resolution,[],[f383,f411]) ).
tff(f433,plain,
! [X0: int] : ( zero_zero(int) = div_mod(int,X0,one_one(int)) ),
inference(resolution,[],[f299,f365]) ).
tff(f446,plain,
! [X0: int,X1: int] :
( ~ dvd_dvd(int,X0,X1)
| ( zero_zero(int) = div_mod(int,X1,X0) ) ),
inference(resolution,[],[f303,f365]) ).
tff(f455,plain,
! [X0: int,X1: int] :
( dvd_dvd(int,X1,X0)
| ( zero_zero(int) != div_mod(int,X0,X1) ) ),
inference(resolution,[],[f304,f365]) ).
tff(f458,plain,
! [X2: int,X3: list(int),X0: int,X1: int,X4: list(int)] :
( ~ i_Z(dvd(X0,X2,X3),X4)
| ~ dvd_dvd(int,X0,div_mod(int,X1,aa(int,int,aa(int,fun(int,int),plus_plus(int),X2),iprod(int,X3,X4))))
| dvd_dvd(int,X0,X1) ),
inference(resolution,[],[f321,f280]) ).
tff(f461,plain,
! [X2: int,X3: list(int),X0: int,X1: int,X4: list(int)] :
( ~ i_Z(dvd(X0,X2,X3),X4)
| dvd_dvd(int,X0,div_mod(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),X2),iprod(int,X3,X4)),X1))
| ~ dvd_dvd(int,X0,X1) ),
inference(resolution,[],[f322,f280]) ).
tff(f471,plain,
! [X0: int] : ( div_mod(int,X0,zero_zero(int)) = X0 ),
inference(resolution,[],[f337,f365]) ).
tff(f494,plain,
! [X0: int,X1: int] : ( div_mod(int,X1,X0) = div_mod(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),X0),X1),X0) ),
inference(resolution,[],[f259,f365]) ).
tff(f506,plain,
! [X2: int,X3: list(int),X0: int,X1: list(int)] : ( iprod(int,cons(int,X0,X1),cons(int,X2,X3)) = aa(int,int,aa(int,fun(int,int),plus_plus(int),times_times(int,X0,X2)),iprod(int,X1,X3)) ),
inference(resolution,[],[f284,f371]) ).
tff(f524,plain,
! [X0: int] : ( times_times(int,X0,one_one(int)) = X0 ),
inference(resolution,[],[f317,f361]) ).
tff(f528,plain,
! [X0: int] : ( times_times(int,one_one(int),X0) = X0 ),
inference(resolution,[],[f319,f361]) ).
tff(f535,plain,
! [X0: int] : ( zero_zero(int) = times_times(int,zero_zero(int),X0) ),
inference(superposition,[],[f396,f471]) ).
tff(f597,plain,
! [X0: int,X1: int] : ( zero_zero(int) = div_mod(int,times_times(int,X0,X1),X1) ),
inference(resolution,[],[f297,f365]) ).
tff(f607,plain,
! [X2: int,X0: int,X1: int] :
( ~ dvd_dvd(int,X1,X2)
| ( zero_zero(int) != div_mod(int,X0,X1) )
| dvd_dvd(int,X1,div_mod(int,X0,X2)) ),
inference(resolution,[],[f455,f322]) ).
tff(f608,plain,
! [X2: int,X0: int,X1: int] :
( ( zero_zero(int) != div_mod(int,X0,X1) )
| dvd_dvd(int,X1,X2)
| ~ dvd_dvd(int,X1,div_mod(int,X2,X0)) ),
inference(resolution,[],[f455,f321]) ).
tff(f628,plain,
! [X0: int] :
( ( sK1(one_one(int),X0) = X0 )
| ( zero_zero(int) != div_mod(int,X0,one_one(int)) ) ),
inference(superposition,[],[f528,f305]) ).
tff(f631,plain,
! [X0: int] : ( sK1(one_one(int),X0) = X0 ),
inference(forward_subsumption_resolution,[],[f628,f433]) ).
tff(f691,plain,
! [X2: int,X0: int,X1: int] : ( div_mod(int,times_times(int,div_mod(int,X0,X1),X2),X1) = div_mod(int,times_times(int,X0,X2),X1) ),
inference(resolution,[],[f325,f365]) ).
tff(f700,plain,
! [X2: int,X0: int,X1: int] : ( div_mod(int,times_times(int,X0,X1),times_times(int,X2,X1)) = times_times(int,div_mod(int,X0,X2),X1) ),
inference(resolution,[],[f326,f365]) ).
tff(f838,plain,
! [X0: list(int),X1: int] :
( ~ i_Z(a,X0)
| ~ dvd_dvd(int,d,div_mod(int,X1,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),iprod(int,ks,X0))))
| dvd_dvd(int,d,X1) ),
inference(superposition,[],[f458,f234]) ).
tff(f844,plain,
! [X0: list(int),X1: int] :
( ~ i_Z(a,X0)
| dvd_dvd(int,d,div_mod(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),iprod(int,ks,X0)),X1))
| ~ dvd_dvd(int,d,X1) ),
inference(superposition,[],[f461,f234]) ).
tff(f930,plain,
! [X2: int,X0: int,X1: int] :
( ~ dvd_dvd(int,X2,X0)
| ~ dvd_dvd(int,X0,X1)
| dvd_dvd(int,X2,X1) ),
inference(resolution,[],[f355,f364]) ).
tff(f949,plain,
! [X0: int,X1: int] :
( ~ dvd_dvd(int,zero_zero(int),X0)
| dvd_dvd(int,X1,X0)
| ~ comm_semiring_1(int) ),
inference(resolution,[],[f930,f347]) ).
tff(f950,plain,
! [X0: int,X1: int] :
( ~ dvd_dvd(int,zero_zero(int),X0)
| dvd_dvd(int,X1,X0) ),
inference(forward_subsumption_resolution,[],[f949,f364]) ).
tff(f966,plain,
! [X0: int,X1: int] :
( dvd_dvd(int,X0,X1)
| ( zero_zero(int) != div_mod(int,X1,zero_zero(int)) ) ),
inference(resolution,[],[f950,f455]) ).
tff(f970,plain,
! [X0: int,X1: int] :
( ( zero_zero(int) != X1 )
| dvd_dvd(int,X0,X1) ),
inference(forward_demodulation,[],[f966,f471]) ).
tff(f975,plain,
! [X0: int] : dvd_dvd(int,X0,zero_zero(int)),
inference(equality_resolution,[],[f970]) ).
tff(f1143,plain,
! [X2: int,X0: int,X1: int] : ( div_mod(int,times_times(int,times_times(int,X0,X1),X2),X1) = div_mod(int,times_times(int,zero_zero(int),X2),X1) ),
inference(superposition,[],[f691,f597]) ).
tff(f1187,plain,
! [X2: int,X0: int,X1: int] : ( div_mod(int,zero_zero(int),X1) = div_mod(int,times_times(int,times_times(int,X0,X1),X2),X1) ),
inference(forward_demodulation,[],[f1143,f535]) ).
tff(f1192,plain,
! [X2: int,X0: int,X1: int] : ( zero_zero(int) = div_mod(int,times_times(int,times_times(int,X0,X1),X2),X1) ),
inference(forward_demodulation,[],[f1187,f294]) ).
tff(f1211,plain,
! [X2: int,X3: int,X0: int,X1: int] : ( div_mod(int,times_times(int,times_times(int,X0,X2),X3),times_times(int,X1,X2)) = div_mod(int,times_times(int,times_times(int,div_mod(int,X0,X1),X2),X3),times_times(int,X1,X2)) ),
inference(superposition,[],[f691,f700]) ).
tff(f1812,plain,
( ! [X0: int] :
( ~ dvd_dvd(int,d,div_mod(int,X0,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),iprod(int,ks,cons(int,j,e)))))
| dvd_dvd(int,d,X0) )
| ~ spl3_2 ),
inference(resolution,[],[f838,f411]) ).
tff(f1816,plain,
( ! [X0: int] :
( ~ dvd_dvd(int,d,zero_zero(int))
| dvd_dvd(int,d,times_times(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),iprod(int,ks,cons(int,j,e))),X0)) )
| ~ spl3_2 ),
inference(superposition,[],[f1812,f396]) ).
tff(f1836,plain,
( ! [X0: int] : dvd_dvd(int,d,times_times(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),iprod(int,ks,cons(int,j,e))),X0))
| ~ spl3_2 ),
inference(forward_subsumption_resolution,[],[f1816,f975]) ).
tff(f1850,plain,
! [X2: list(int),X3: list(int),X0: int,X1: int] :
( ( zero_zero(int) != div_mod(int,X0,X1) )
| ( iprod(int,cons(int,X1,X2),cons(int,sK1(X1,X0),X3)) = aa(int,int,aa(int,fun(int,int),plus_plus(int),X0),iprod(int,X2,X3)) ) ),
inference(superposition,[],[f506,f305]) ).
tff(f1855,plain,
! [X2: int,X3: list(int),X0: int,X1: list(int),X4: int] :
( ~ dvd_dvd(int,X4,iprod(int,cons(int,X0,X1),cons(int,X2,X3)))
| i_Z(dvd(X4,times_times(int,X0,X2),X1),X3) ),
inference(superposition,[],[f281,f506]) ).
tff(f1897,plain,
( ! [X0: int,X1: int] :
( ~ dvd_dvd(int,d,X0)
| dvd_dvd(int,d,div_mod(int,times_times(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),iprod(int,ks,cons(int,j,e))),X1),X0)) )
| ~ spl3_2 ),
inference(resolution,[],[f1836,f322]) ).
tff(f3510,plain,
( ! [X0: int,X1: int] :
( ( zero_zero(int) != div_mod(int,X1,d) )
| dvd_dvd(int,d,div_mod(int,times_times(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),iprod(int,ks,cons(int,j,e))),X0),X1)) )
| ~ spl3_2 ),
inference(resolution,[],[f1897,f455]) ).
tff(f4671,plain,
! [X0: int,X1: int] :
( ( zero_zero(int) != zero_zero(int) )
| dvd_dvd(int,X0,X1)
| ~ dvd_dvd(int,X0,div_mod(int,X1,X0)) ),
inference(superposition,[],[f608,f295]) ).
tff(f4741,plain,
! [X0: int,X1: int] :
( ~ dvd_dvd(int,X0,div_mod(int,X1,X0))
| dvd_dvd(int,X0,X1) ),
inference(trivial_inequality_removal,[],[f4671]) ).
tff(f5678,plain,
! [X2: int,X3: list(int),X0: int,X1: int,X4: list(int)] :
( ( zero_zero(int) != div_mod(int,iprod(int,cons(int,X1,X3),cons(int,X2,X4)),X0) )
| i_Z(dvd(X0,times_times(int,X1,X2),X3),X4) ),
inference(resolution,[],[f1855,f455]) ).
tff(f9706,plain,
( ! [X0: int,X1: int] :
( ( zero_zero(int) != zero_zero(int) )
| dvd_dvd(int,d,div_mod(int,times_times(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),iprod(int,ks,cons(int,j,e))),X1),times_times(int,X0,d))) )
| ~ spl3_2 ),
inference(superposition,[],[f3510,f597]) ).
tff(f9737,plain,
( ! [X0: int,X1: int] : dvd_dvd(int,d,div_mod(int,times_times(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),iprod(int,ks,cons(int,j,e))),X1),times_times(int,X0,d)))
| ~ spl3_2 ),
inference(trivial_inequality_removal,[],[f9706]) ).
tff(f9856,plain,
( ! [X0: int] : dvd_dvd(int,d,times_times(int,div_mod(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),iprod(int,ks,cons(int,j,e))),X0),d))
| ~ spl3_2 ),
inference(superposition,[],[f9737,f700]) ).
tff(f9924,plain,
( dvd_dvd(int,d,times_times(int,div_mod(int,iprod(int,ks,cons(int,j,e)),l),d))
| ~ spl3_2 ),
inference(superposition,[],[f9856,f494]) ).
tff(f9983,plain,
( ! [X0: int] :
( ~ dvd_dvd(int,d,div_mod(int,X0,times_times(int,div_mod(int,iprod(int,ks,cons(int,j,e)),l),d)))
| dvd_dvd(int,d,X0) )
| ~ spl3_2 ),
inference(resolution,[],[f9924,f321]) ).
tff(f9987,plain,
( ! [X0: int] :
( dvd_dvd(int,d,div_mod(int,X0,times_times(int,div_mod(int,iprod(int,ks,cons(int,j,e)),l),d)))
| ( zero_zero(int) != div_mod(int,X0,d) ) )
| ~ spl3_2 ),
inference(resolution,[],[f9924,f607]) ).
tff(f16267,plain,
! [X2: list(int),X0: int,X1: list(int)] :
( ( zero_zero(int) != zero_zero(int) )
| ( aa(int,int,aa(int,fun(int,int),plus_plus(int),X0),iprod(int,X1,X2)) = iprod(int,cons(int,one_one(int),X1),cons(int,sK1(one_one(int),X0),X2)) ) ),
inference(superposition,[],[f1850,f433]) ).
tff(f16339,plain,
! [X2: list(int),X0: int,X1: list(int)] : ( aa(int,int,aa(int,fun(int,int),plus_plus(int),X0),iprod(int,X1,X2)) = iprod(int,cons(int,one_one(int),X1),cons(int,sK1(one_one(int),X0),X2)) ),
inference(trivial_inequality_removal,[],[f16267]) ).
tff(f16384,plain,
! [X2: list(int),X0: int,X1: list(int)] : ( aa(int,int,aa(int,fun(int,int),plus_plus(int),X0),iprod(int,X1,X2)) = iprod(int,cons(int,one_one(int),X1),cons(int,X0,X2)) ),
inference(forward_demodulation,[],[f16339,f631]) ).
tff(f16706,plain,
( ! [X0: int,X1: int] :
( dvd_dvd(int,d,div_mod(int,times_times(int,times_times(int,X0,d),X1),times_times(int,div_mod(int,iprod(int,ks,cons(int,j,e)),l),d)))
| ( zero_zero(int) != div_mod(int,times_times(int,times_times(int,div_mod(int,X0,div_mod(int,iprod(int,ks,cons(int,j,e)),l)),d),X1),d) ) )
| ~ spl3_2 ),
inference(superposition,[],[f9987,f1211]) ).
tff(f16758,plain,
( ! [X0: int,X1: int] : dvd_dvd(int,d,div_mod(int,times_times(int,times_times(int,X0,d),X1),times_times(int,div_mod(int,iprod(int,ks,cons(int,j,e)),l),d)))
| ~ spl3_2 ),
inference(forward_subsumption_resolution,[],[f16706,f1192]) ).
tff(f18364,plain,
( ! [X0: int,X1: int] : dvd_dvd(int,d,times_times(int,times_times(int,X0,d),X1))
| ~ spl3_2 ),
inference(resolution,[],[f16758,f9983]) ).
tff(f18439,plain,
( ! [X0: int] : dvd_dvd(int,d,times_times(int,d,X0))
| ~ spl3_2 ),
inference(superposition,[],[f18364,f528]) ).
tff(f18606,plain,
( dvd_dvd(int,d,d)
| ~ spl3_2 ),
inference(superposition,[],[f18439,f524]) ).
tff(f56513,plain,
( ! [X0: int] :
( ~ dvd_dvd(int,d,X0)
| dvd_dvd(int,d,div_mod(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),iprod(int,ks,cons(int,j,e))),X0)) )
| ~ spl3_2 ),
inference(resolution,[],[f411,f844]) ).
tff(f181240,plain,
! [X2: int,X3: int,X0: list(int),X1: list(int)] :
( ~ i_Z(dvd(X3,X2,X1),X0)
| dvd_dvd(int,X3,iprod(int,cons(int,one_one(int),X1),cons(int,X2,X0))) ),
inference(backward_demodulation,[],[f280,f16384]) ).
tff(f181257,plain,
div_mod(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),aa(int,int,aa(int,fun(int,int),plus_plus(int),j),iprod(int,ks1,e))),d) = div_mod(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),iprod(int,cons(int,one_one(int),ks1),cons(int,i,e))),d),
inference(backward_demodulation,[],[f235,f16384]) ).
tff(f181268,plain,
( ! [X0: int] :
( dvd_dvd(int,d,div_mod(int,iprod(int,cons(int,one_one(int),ks),cons(int,l,cons(int,j,e))),X0))
| ~ dvd_dvd(int,d,X0) )
| ~ spl3_2 ),
inference(backward_demodulation,[],[f56513,f16384]) ).
tff(f181479,plain,
div_mod(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),aa(int,int,aa(int,fun(int,int),plus_plus(int),j),iprod(int,ks1,e))),d) = div_mod(int,iprod(int,cons(int,one_one(int),cons(int,one_one(int),ks1)),cons(int,l,cons(int,i,e))),d),
inference(forward_demodulation,[],[f181257,f16384]) ).
tff(f181504,plain,
div_mod(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),aa(int,int,aa(int,fun(int,int),plus_plus(int),j),iprod(int,ks1,e))),d) = div_mod(int,iprod(int,cons(int,one_one(int),ks),cons(int,l,cons(int,i,e))),d),
inference(forward_demodulation,[],[f181479,f237]) ).
tff(f181518,plain,
div_mod(int,iprod(int,cons(int,one_one(int),ks),cons(int,l,cons(int,i,e))),d) = div_mod(int,aa(int,int,aa(int,fun(int,int),plus_plus(int),l),iprod(int,cons(int,one_one(int),ks1),cons(int,j,e))),d),
inference(forward_demodulation,[],[f181504,f16384]) ).
tff(f181528,plain,
div_mod(int,iprod(int,cons(int,one_one(int),ks),cons(int,l,cons(int,i,e))),d) = div_mod(int,iprod(int,cons(int,one_one(int),cons(int,one_one(int),ks1)),cons(int,l,cons(int,j,e))),d),
inference(forward_demodulation,[],[f181518,f16384]) ).
tff(f181538,plain,
div_mod(int,iprod(int,cons(int,one_one(int),ks),cons(int,l,cons(int,i,e))),d) = div_mod(int,iprod(int,cons(int,one_one(int),ks),cons(int,l,cons(int,j,e))),d),
inference(forward_demodulation,[],[f181528,f237]) ).
tff(f181557,plain,
! [X0: list(int)] :
( ~ i_Z(a,X0)
| dvd_dvd(int,d,iprod(int,cons(int,one_one(int),ks),cons(int,l,X0))) ),
inference(superposition,[],[f181240,f234]) ).
tff(f183569,plain,
( dvd_dvd(int,d,div_mod(int,iprod(int,cons(int,one_one(int),ks),cons(int,l,cons(int,i,e))),d))
| ~ dvd_dvd(int,d,d)
| ~ spl3_2 ),
inference(superposition,[],[f181268,f181538]) ).
tff(f183571,plain,
( dvd_dvd(int,d,div_mod(int,iprod(int,cons(int,one_one(int),ks),cons(int,l,cons(int,i,e))),d))
| ~ spl3_2 ),
inference(forward_subsumption_resolution,[],[f183569,f18606]) ).
tff(f190964,plain,
( dvd_dvd(int,d,iprod(int,cons(int,one_one(int),ks),cons(int,l,cons(int,i,e))))
| ~ spl3_2 ),
inference(resolution,[],[f183571,f4741]) ).
tff(f190979,plain,
( i_Z(dvd(d,times_times(int,one_one(int),l),ks),cons(int,i,e))
| ~ spl3_2 ),
inference(resolution,[],[f190964,f1855]) ).
tff(f190990,plain,
( i_Z(dvd(d,l,ks),cons(int,i,e))
| ~ spl3_2 ),
inference(forward_demodulation,[],[f190979,f528]) ).
tff(f190992,plain,
( i_Z(a,cons(int,i,e))
| ~ spl3_2 ),
inference(forward_demodulation,[],[f190990,f234]) ).
tff(f190995,plain,
( $false
| spl3_1
| ~ spl3_2 ),
inference(forward_subsumption_resolution,[],[f190992,f406]) ).
tff(f190996,plain,
( spl3_1
| ~ spl3_2 ),
inference(avatar_contradiction_clause,[],[f190995]) ).
tff(f191014,plain,
( dvd_dvd(int,d,iprod(int,cons(int,one_one(int),ks),cons(int,l,cons(int,i,e))))
| ~ spl3_1 ),
inference(resolution,[],[f407,f181557]) ).
tff(f191026,plain,
( $false
| ~ spl3_1
| ~ spl3_2 ),
inference(forward_subsumption_resolution,[],[f413,f407]) ).
tff(f191027,plain,
( ~ spl3_1
| ~ spl3_2 ),
inference(avatar_contradiction_clause,[],[f191026]) ).
tff(f191295,plain,
( ( zero_zero(int) = div_mod(int,iprod(int,cons(int,one_one(int),ks),cons(int,l,cons(int,i,e))),d) )
| ~ spl3_1 ),
inference(resolution,[],[f191014,f446]) ).
tff(f192767,plain,
( ( zero_zero(int) = div_mod(int,iprod(int,cons(int,one_one(int),ks),cons(int,l,cons(int,j,e))),d) )
| ~ spl3_1 ),
inference(backward_demodulation,[],[f181538,f191295]) ).
tff(f193095,plain,
( ( zero_zero(int) != zero_zero(int) )
| i_Z(dvd(d,times_times(int,one_one(int),l),ks),cons(int,j,e))
| ~ spl3_1 ),
inference(superposition,[],[f5678,f192767]) ).
tff(f193096,plain,
( i_Z(dvd(d,times_times(int,one_one(int),l),ks),cons(int,j,e))
| ~ spl3_1 ),
inference(trivial_inequality_removal,[],[f193095]) ).
tff(f193126,plain,
( i_Z(dvd(d,l,ks),cons(int,j,e))
| ~ spl3_1 ),
inference(forward_demodulation,[],[f193096,f528]) ).
tff(f193188,plain,
( i_Z(a,cons(int,j,e))
| ~ spl3_1 ),
inference(forward_demodulation,[],[f193126,f234]) ).
tff(f193227,plain,
( $false
| ~ spl3_1
| spl3_2 ),
inference(forward_subsumption_resolution,[],[f193188,f410]) ).
tff(f193228,plain,
( ~ spl3_1
| spl3_2 ),
inference(avatar_contradiction_clause,[],[f193227]) ).
cnf(s1,plain,
( spl3_1
| spl3_2 ),
inference(sat_conversion,[],[f412]) ).
cnf(s18,plain,
( spl3_1
| ~ spl3_2 ),
inference(sat_conversion,[],[f190996]) ).
cnf(s19,plain,
( ~ spl3_1
| ~ spl3_2 ),
inference(sat_conversion,[],[f191027]) ).
cnf(s23,plain,
( ~ spl3_1
| spl3_2 ),
inference(sat_conversion,[],[f193228]) ).
cnf(s24,plain,
spl3_1,
inference(rat,[],[s1,s18]) ).
cnf(s25,plain,
spl3_2,
inference(rat,[],[s23,s24]) ).
cnf(s26,plain,
$false,
inference(rat,[],[s19,s25,s24]) ).
tff(f193253,plain,
$false,
inference(avatar_sat_refutation,[],[s26]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : COM038_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.10 % CPULimit : 300
% 0.00/0.10 % WCLimit : 300
% 0.00/0.10 % DateTime : Mon Sep 28 21:50:04 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.12 Running first-order theorem proving
% 0.08/0.12 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.48/1.00 % (3816390)Detected formulas, will run a generic FOF schedule.
% 3.48/1.00 % (3816396)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=3693811591:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.48/1.00 % (3816395)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=4274363515:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.48/1.00 % (3816400)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=995502032:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.48/1.00 % (3816401)dis-21_1_sil=8000:lcm=predicate:random_seed=1760611522: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)
% 3.48/1.00 % (3816398)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1684206296:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.48/1.00 % (3816397)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=2103420387:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.48/1.00 % (3816399)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2678710497:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.48/1.00 % (3816398)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 3.48/1.00 % (3816398)Refutation not found, incomplete strategy
% 3.48/1.00 % (3816398)------------------------------
% 3.48/1.00 % (3816398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.48/1.00 % (3816398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.48/1.00 % (3816398)CaDiCaL version: 2.1.3
% 3.48/1.00 % (3816398)Termination reason: Refutation not found, incomplete strategy
% 3.48/1.00 % (3816398)Time elapsed: 0.001 s
% 3.48/1.00 % (3816398)Peak memory usage: 88 MB
% 3.48/1.00 % (3816398)Instructions burned: 1 (million)
% 3.48/1.00 % (3816397)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 3.48/1.00 % (3816401)Instruction limit reached!
% 3.48/1.00 % (3816401)------------------------------
% 3.48/1.00 % (3816401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.48/1.00 % (3816401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.48/1.00 % (3816401)CaDiCaL version: 2.1.3
% 3.48/1.00 % (3816401)Termination reason: Instruction limit
% 3.48/1.00 % (3816401)Termination phase: Saturation
% 3.48/1.00 % (3816401)Time elapsed: 0.028 s
% 3.48/1.00 % (3816401)Peak memory usage: 90 MB
% 3.48/1.00 % (3816401)Instructions burned: 129 (million)
% 3.48/1.00 % (3816399)Instruction limit reached!
% 3.48/1.00 % (3816399)------------------------------
% 3.48/1.00 % (3816399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.48/1.00 % (3816399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.48/1.00 % (3816399)CaDiCaL version: 2.1.3
% 3.48/1.00 % (3816399)Termination reason: Instruction limit
% 3.48/1.00 % (3816399)Termination phase: Saturation
% 3.48/1.00 % (3816399)Time elapsed: 0.036 s
% 3.48/1.00 % (3816399)Peak memory usage: 88 MB
% 3.48/1.00 % (3816399)Instructions burned: 121 (million)
% 3.48/1.00 % (3816400)Instruction limit reached!
% 3.48/1.00 % (3816400)------------------------------
% 3.48/1.00 % (3816400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.48/1.00 % (3816400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.48/1.00 % (3816400)CaDiCaL version: 2.1.3
% 3.48/1.00 % (3816400)Termination reason: Instruction limit
% 3.48/1.00 % (3816400)Termination phase: Saturation
% 3.48/1.00 % (3816400)Time elapsed: 0.050 s
% 3.48/1.00 % (3816400)Peak memory usage: 89 MB
% 3.48/1.00 % (3816400)Instructions burned: 141 (million)
% 3.48/1.00 % (3816410)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3783916248:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 3.48/1.00 % (3816409)lrs+10_1_sil=8000:sp=occurrence:random_seed=1075938013:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 3.48/1.00 % (3816411)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2723030810:i=325:sd=1:ss=axioms:sgt=32_2998 on theBenchmark for (2998ds/325Mi)
% 3.48/1.00 % (3816398)------------------------------
% 5.51/1.19 % (3816398)------------------------------
% 5.51/1.19 % (3816410)Instruction limit reached!
% 5.51/1.19 % (3816410)------------------------------
% 5.51/1.19 % (3816410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.51/1.19 % (3816410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.19 % (3816410)CaDiCaL version: 2.1.3
% 5.51/1.19 % (3816410)Termination reason: Instruction limit
% 5.51/1.19 % (3816410)Termination phase: Saturation
% 5.51/1.19 % (3816410)Time elapsed: 0.045 s
% 5.51/1.19 % (3816410)Peak memory usage: 90 MB
% 5.51/1.19 % (3816410)Instructions burned: 160 (million)
% 5.51/1.19 % Exception at run slice level
% 5.51/1.19 User error: GNN currently only supports monomorphic FOL.
% 5.51/1.19 % Exception at run slice level
% 5.51/1.19 User error: GNN currently only supports monomorphic FOL.
% 5.51/1.19 % Exception at run slice level
% 5.51/1.19 User error: GNN currently only supports monomorphic FOL.
% 5.51/1.19 % (3816409)Instruction limit reached!
% 5.51/1.19 % (3816409)------------------------------
% 5.51/1.19 % (3816409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.51/1.19 % (3816409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.19 % (3816409)CaDiCaL version: 2.1.3
% 5.51/1.19 % (3816409)Termination reason: Instruction limit
% 5.51/1.19 % (3816409)Termination phase: Saturation
% 5.51/1.19 % (3816409)Time elapsed: 0.092 s
% 5.51/1.19 % (3816409)Peak memory usage: 91 MB
% 5.51/1.19 % (3816409)Instructions burned: 287 (million)
% 5.51/1.19 % (3816411)Instruction limit reached!
% 5.51/1.19 % (3816411)------------------------------
% 5.51/1.19 % (3816411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.51/1.19 % (3816411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.19 % (3816411)CaDiCaL version: 2.1.3
% 5.51/1.19 % (3816411)Termination reason: Instruction limit
% 5.51/1.19 % (3816411)Termination phase: Saturation
% 5.51/1.19 % (3816411)Time elapsed: 0.101 s
% 5.51/1.19 % (3816411)Peak memory usage: 92 MB
% 5.51/1.19 % (3816411)Instructions burned: 325 (million)
% 5.51/1.19 % (3816415)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=1439948484:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 5.51/1.19 % (3816416)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1635972243:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2997 on theBenchmark for (2997ds/294Mi)
% 5.51/1.19 % (3816416)Refutation not found, incomplete strategy
% 5.51/1.19 % (3816416)------------------------------
% 5.51/1.19 % (3816416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.51/1.19 % (3816416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.19 % (3816416)CaDiCaL version: 2.1.3
% 5.51/1.19 % (3816416)Termination reason: Refutation not found, incomplete strategy
% 5.51/1.19 % (3816416)Time elapsed: 0.003 s
% 5.51/1.19 % (3816416)Peak memory usage: 89 MB
% 5.51/1.19 % (3816416)Instructions burned: 7 (million)
% 5.51/1.19 % (3816419)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=196654875:i=127:av=off:fsr=off:sup=off_2996 on theBenchmark for (2996ds/127Mi)
% 5.51/1.19 % (3816417)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3661593962:i=2350_2996 on theBenchmark for (2996ds/2350Mi)
% 5.51/1.19 % (3816418)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3033617113:cts=off:i=113:fsr=off:ss=included:sgt=4_2996 on theBenchmark for (2996ds/113Mi)
% 5.51/1.19 % (3816419)Refutation not found, incomplete strategy
% 5.51/1.19 % (3816419)------------------------------
% 5.51/1.19 % (3816419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.51/1.19 % (3816419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.19 % (3816419)CaDiCaL version: 2.1.3
% 5.51/1.19 % (3816419)Termination reason: Refutation not found, incomplete strategy
% 5.51/1.19 % (3816419)Time elapsed: 0.002 s
% 5.51/1.19 % (3816419)Peak memory usage: 88 MB
% 5.51/1.19 % (3816419)Instructions burned: 7 (million)
% 5.51/1.19 % (3816418)Refutation not found, incomplete strategy
% 5.51/1.19 % (3816418)------------------------------
% 5.51/1.19 % (3816418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.51/1.19 % (3816418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.51/1.19 % (3816418)CaDiCaL version: 2.1.3
% 5.51/1.19 % (3816418)Termination reason: Refutation not found, incomplete strategy
% 7.00/1.40 % (3816418)Time elapsed: 0.004 s
% 7.00/1.40 % (3816418)Peak memory usage: 89 MB
% 7.00/1.40 % (3816418)Instructions burned: 11 (million)
% 7.00/1.40 % (3816415)Instruction limit reached!
% 7.00/1.40 % (3816415)------------------------------
% 7.00/1.40 % (3816415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.00/1.40 % (3816415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.00/1.40 % (3816415)CaDiCaL version: 2.1.3
% 7.00/1.40 % (3816415)Termination reason: Instruction limit
% 7.00/1.40 % (3816415)Termination phase: Saturation
% 7.00/1.40 % (3816415)Time elapsed: 0.067 s
% 7.00/1.40 % (3816415)Peak memory usage: 91 MB
% 7.00/1.40 % (3816415)Instructions burned: 249 (million)
% 7.00/1.40 % (3816420)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2736670325:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2996 on theBenchmark for (2996ds/114Mi)
% 7.00/1.40 % (3816420)Refutation not found, incomplete strategy
% 7.00/1.40 % (3816420)------------------------------
% 7.00/1.40 % (3816420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.00/1.40 % (3816420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.00/1.40 % (3816420)CaDiCaL version: 2.1.3
% 7.00/1.40 % (3816420)Termination reason: Refutation not found, incomplete strategy
% 7.00/1.40 % (3816420)Time elapsed: 0.002 s
% 7.00/1.40 % (3816420)Peak memory usage: 89 MB
% 7.00/1.40 % (3816420)Instructions burned: 5 (million)
% 7.00/1.40 % (3816422)lrs+10_1_sil=8000:sp=occurrence:random_seed=891187037:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2996 on theBenchmark for (2996ds/907Mi)
% 7.00/1.40 % (3816416)------------------------------
% 7.00/1.40 % (3816416)------------------------------
% 7.00/1.40 % (3816427)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3969871530:i=437:sd=1:aac=none:ss=included_2995 on theBenchmark for (2995ds/437Mi)
% 7.00/1.40 % (3816427)Refutation not found, incomplete strategy
% 7.00/1.40 % (3816427)------------------------------
% 7.00/1.40 % (3816427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.00/1.40 % (3816427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.00/1.40 % (3816427)CaDiCaL version: 2.1.3
% 7.00/1.40 % (3816427)Termination reason: Refutation not found, incomplete strategy
% 7.00/1.40 % (3816427)Time elapsed: 0.004 s
% 7.00/1.40 % (3816427)Peak memory usage: 89 MB
% 7.00/1.40 % (3816427)Instructions burned: 12 (million)
% 7.00/1.40 % (3816418)------------------------------
% 7.00/1.40 % (3816418)------------------------------
% 7.00/1.40 % (3816419)------------------------------
% 7.00/1.40 % (3816419)------------------------------
% 7.00/1.40 % (3816420)------------------------------
% 7.00/1.40 % (3816420)------------------------------
% 7.00/1.40 % Exception at run slice level
% 7.00/1.40 User error: GNN currently only supports monomorphic FOL.
% 7.00/1.40 % (3816430)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2819429115:i=5202:ss=axioms:sgt=16_2994 on theBenchmark for (2994ds/5202Mi)
% 7.00/1.40 % (3816433)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2280973064:st=8:i=592:sd=3:ep=RST:ss=axioms_2994 on theBenchmark for (2994ds/592Mi)
% 7.00/1.40 % (3816433)Refutation not found, incomplete strategy
% 7.00/1.40 % (3816433)------------------------------
% 7.00/1.40 % (3816433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.00/1.40 % (3816433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.00/1.40 % (3816433)CaDiCaL version: 2.1.3
% 7.00/1.40 % (3816433)Termination reason: Refutation not found, incomplete strategy
% 7.00/1.40 % (3816433)Time elapsed: 0.004 s
% 7.00/1.40 % (3816433)Peak memory usage: 88 MB
% 7.00/1.40 % (3816433)Instructions burned: 10 (million)
% 7.00/1.40 % (3816432)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2580939154:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2994 on theBenchmark for (2994ds/134Mi)
% 7.00/1.40 % (3816434)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=822933816:st=3:i=13193:sd=3:ss=axioms_2994 on theBenchmark for (2994ds/13193Mi)
% 7.00/1.40 % (3816427)------------------------------
% 7.00/1.40 % (3816427)------------------------------
% 7.00/1.40 % (3816422)Instruction limit reached!
% 7.00/1.40 % (3816422)------------------------------
% 7.00/1.40 % (3816422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.00/1.40 % (3816422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.66 % (3816422)CaDiCaL version: 2.1.3
% 8.18/1.66 % (3816422)Termination reason: Instruction limit
% 8.18/1.66 % (3816422)Termination phase: Saturation
% 8.18/1.66 % (3816422)Time elapsed: 0.255 s
% 8.18/1.66 % (3816422)Peak memory usage: 92 MB
% 8.18/1.66 % (3816422)Instructions burned: 907 (million)
% 8.18/1.66 % (3816432)Instruction limit reached!
% 8.18/1.66 % (3816432)------------------------------
% 8.18/1.66 % (3816432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.18/1.66 % (3816432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.66 % (3816432)CaDiCaL version: 2.1.3
% 8.18/1.66 % (3816432)Termination reason: Instruction limit
% 8.18/1.66 % (3816432)Termination phase: Saturation
% 8.18/1.66 % (3816432)Time elapsed: 0.038 s
% 8.18/1.66 % (3816432)Peak memory usage: 90 MB
% 8.18/1.66 % (3816432)Instructions burned: 137 (million)
% 8.18/1.66 % (3816435)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=1365308568:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/125Mi)
% 8.18/1.66 % (3816435)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 8.18/1.66 % (3816435)Instruction limit reached!
% 8.18/1.66 % (3816435)------------------------------
% 8.18/1.66 % (3816435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.18/1.66 % (3816435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.66 % (3816435)CaDiCaL version: 2.1.3
% 8.18/1.66 % (3816435)Termination reason: Instruction limit
% 8.18/1.66 % (3816435)Termination phase: Saturation
% 8.18/1.66 % (3816435)Time elapsed: 0.044 s
% 8.18/1.66 % (3816435)Peak memory usage: 90 MB
% 8.18/1.66 % (3816435)Instructions burned: 126 (million)
% 8.18/1.66 % (3816441)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3245210846:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/141Mi)
% 8.18/1.66 % (3816441)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 8.18/1.66 % (3816441)Refutation not found, incomplete strategy
% 8.18/1.66 % (3816441)------------------------------
% 8.18/1.66 % (3816441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.18/1.66 % (3816441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.66 % (3816441)CaDiCaL version: 2.1.3
% 8.18/1.66 % (3816441)Termination reason: Refutation not found, incomplete strategy
% 8.18/1.66 % (3816441)Time elapsed: 0.001 s
% 8.18/1.66 % (3816441)Peak memory usage: 89 MB
% 8.18/1.66 % (3816441)Instructions burned: 1 (million)
% 8.18/1.66 % (3816440)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4197245418:i=134:gtgl=5:slsql=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/134Mi)
% 8.18/1.66 % Exception at run slice level
% 8.18/1.66 User error: Immediate (shared) subterms of term/literal aa(X1,fun(list(X1),X0),X4,X3) = sF32(X1,X0,X4,X3) have different types/not well-typed!
% 8.18/1.66 % (3816442)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1821225322:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2993 on theBenchmark for (2993ds/431Mi)
% 8.18/1.66 % (3816442)Refutation not found, incomplete strategy
% 8.18/1.66 % (3816442)------------------------------
% 8.18/1.66 % (3816442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.18/1.66 % (3816442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.66 % (3816442)CaDiCaL version: 2.1.3
% 8.18/1.66 % (3816442)Termination reason: Refutation not found, incomplete strategy
% 8.18/1.66 % (3816442)Time elapsed: 0.002 s
% 8.18/1.66 % (3816442)Peak memory usage: 89 MB
% 8.18/1.66 % (3816442)Instructions burned: 3 (million)
% 8.18/1.66 % (3816433)------------------------------
% 8.18/1.66 % (3816433)------------------------------
% 8.18/1.66 % Exception at run slice level
% 8.18/1.66 User error: GNN currently only supports monomorphic FOL.
% 8.18/1.66 % (3816444)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=2305114126:i=6060:aac=none:ins=25_2992 on theBenchmark for (2992ds/6060Mi)
% 8.18/1.66 % Exception at run slice level
% 8.18/1.66 User error: GNN currently only supports monomorphic FOL.
% 8.18/1.66 % (3816448)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=2489504711:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2992 on theBenchmark for (2992ds/150Mi)
% 12.72/2.16 % (3816448)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 12.72/2.16 % (3816450)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=270799796:i=667:av=off:fsr=off_2991 on theBenchmark for (2991ds/667Mi)
% 12.72/2.16 % (3816449)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1014701699:i=14155:bd=all_2991 on theBenchmark for (2991ds/14155Mi)
% 12.72/2.16 % (3816450)Refutation not found, incomplete strategy
% 12.72/2.16 % (3816450)------------------------------
% 12.72/2.16 % (3816450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.72/2.16 % (3816450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.72/2.16 % (3816450)CaDiCaL version: 2.1.3
% 12.72/2.16 % (3816450)Termination reason: Refutation not found, incomplete strategy
% 12.72/2.16 % (3816450)Time elapsed: 0.003 s
% 12.72/2.16 % (3816450)Peak memory usage: 88 MB
% 12.72/2.16 % (3816450)Instructions burned: 10 (million)
% 12.72/2.16 % (3816448)Instruction limit reached!
% 12.72/2.16 % (3816448)------------------------------
% 12.72/2.16 % (3816448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.72/2.16 % (3816448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.72/2.16 % (3816448)CaDiCaL version: 2.1.3
% 12.72/2.16 % (3816448)Termination reason: Instruction limit
% 12.72/2.16 % (3816448)Termination phase: Saturation
% 12.72/2.16 % (3816448)Time elapsed: 0.050 s
% 12.72/2.16 % (3816448)Peak memory usage: 90 MB
% 12.72/2.16 % (3816448)Instructions burned: 151 (million)
% 12.72/2.16 % (3816441)------------------------------
% 12.72/2.16 % (3816441)------------------------------
% 12.72/2.16 % (3816442)------------------------------
% 12.72/2.16 % (3816442)------------------------------
% 12.72/2.16 % (3816453)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=2007038120:s2a=on:i=185:s2at=1.8:fdi=4_2991 on theBenchmark for (2991ds/185Mi)
% 12.72/2.16 % (3816457)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1694444573:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2990 on theBenchmark for (2990ds/4850Mi)
% 12.72/2.16 % (3816456)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=677136896:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2990 on theBenchmark for (2990ds/193Mi)
% 12.72/2.16 % (3816457)Refutation not found, incomplete strategy
% 12.72/2.16 % (3816457)------------------------------
% 12.72/2.16 % (3816457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.72/2.16 % (3816457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.72/2.16 % (3816457)CaDiCaL version: 2.1.3
% 12.72/2.16 % (3816457)Termination reason: Refutation not found, incomplete strategy
% 12.72/2.16 % (3816457)Time elapsed: 0.003 s
% 12.72/2.16 % (3816457)Peak memory usage: 88 MB
% 12.72/2.16 % (3816457)Instructions burned: 8 (million)
% 12.72/2.16 % (3816453)Instruction limit reached!
% 12.72/2.16 % (3816453)------------------------------
% 12.72/2.16 % (3816453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.72/2.16 % (3816453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.72/2.16 % (3816453)CaDiCaL version: 2.1.3
% 12.72/2.16 % (3816453)Termination reason: Instruction limit
% 12.72/2.16 % (3816453)Termination phase: Saturation
% 12.72/2.16 % (3816453)Time elapsed: 0.062 s
% 12.72/2.16 % (3816453)Peak memory usage: 91 MB
% 12.72/2.16 % (3816453)Instructions burned: 185 (million)
% 12.72/2.16 % (3816458)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2125521316:i=12111:sd=1:ss=included_2990 on theBenchmark for (2990ds/12111Mi)
% 12.72/2.16 % Exception at run slice level
% 12.72/2.16 User error: GNN currently only supports monomorphic FOL.
% 12.72/2.16 % (3816450)------------------------------
% 12.72/2.16 % (3816450)------------------------------
% 12.72/2.16 % (3816456)Instruction limit reached!
% 12.72/2.16 % (3816456)------------------------------
% 12.72/2.16 % (3816456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.72/2.16 % (3816456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.59/2.63 % (3816456)CaDiCaL version: 2.1.3
% 15.59/2.63 % (3816456)Termination reason: Instruction limit
% 15.59/2.63 % (3816456)Termination phase: Saturation
% 15.59/2.63 % (3816456)Time elapsed: 0.066 s
% 15.59/2.63 % (3816456)Peak memory usage: 90 MB
% 15.59/2.63 % (3816456)Instructions burned: 193 (million)
% 15.59/2.63 % (3816462)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3162775081:i=319:kws=precedence:fsr=off_2989 on theBenchmark for (2989ds/319Mi)
% 15.59/2.63 % Exception at run slice level
% 15.59/2.63 User error: GNN currently only supports monomorphic FOL.
% 15.59/2.63 % (3816464)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2753916736:i=2064:ep=RST_2989 on theBenchmark for (2989ds/2064Mi)
% 15.59/2.63 % (3816464)Refutation not found, incomplete strategy
% 15.59/2.63 % (3816464)------------------------------
% 15.59/2.63 % (3816464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.59/2.63 % (3816464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.59/2.63 % (3816464)CaDiCaL version: 2.1.3
% 15.59/2.63 % (3816464)Termination reason: Refutation not found, incomplete strategy
% 15.59/2.63 % (3816464)Time elapsed: 0.004 s
% 15.59/2.63 % (3816464)Peak memory usage: 88 MB
% 15.59/2.63 % (3816464)Instructions burned: 11 (million)
% 15.59/2.63 % (3816457)------------------------------
% 15.59/2.63 % (3816457)------------------------------
% 15.59/2.63 % (3816465)dis-1011_128_sil=32000:random_seed=3132989997:i=3706:ep=RST:av=off_2989 on theBenchmark for (2989ds/3706Mi)
% 15.59/2.63 % (3816466)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3769283517:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2989 on theBenchmark for (2989ds/757Mi)
% 15.59/2.63 % (3816466)Refutation not found, incomplete strategy
% 15.59/2.63 % (3816466)------------------------------
% 15.59/2.63 % (3816466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.59/2.63 % (3816466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.59/2.63 % (3816466)CaDiCaL version: 2.1.3
% 15.59/2.63 % (3816466)Termination reason: Refutation not found, incomplete strategy
% 15.59/2.63 % (3816466)Time elapsed: 0.002 s
% 15.59/2.63 % (3816466)Peak memory usage: 89 MB
% 15.59/2.63 % (3816466)Instructions burned: 5 (million)
% 15.59/2.63 % (3816462)Instruction limit reached!
% 15.59/2.63 % (3816462)------------------------------
% 15.59/2.63 % (3816462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.59/2.63 % (3816462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.59/2.63 % (3816462)CaDiCaL version: 2.1.3
% 15.59/2.63 % (3816462)Termination reason: Instruction limit
% 15.59/2.63 % (3816462)Termination phase: Saturation
% 15.59/2.63 % (3816462)Time elapsed: 0.079 s
% 15.59/2.63 % (3816462)Peak memory usage: 89 MB
% 15.59/2.63 % (3816462)Instructions burned: 323 (million)
% 15.59/2.63 % (3816468)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4099409483:i=13913:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/13913Mi)
% 15.59/2.63 % Exception at run slice level
% 15.59/2.63 User error: GNN currently only supports monomorphic FOL.
% 15.59/2.63 % (3816471)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1796857009:i=9925:aac=none_2988 on theBenchmark for (2988ds/9925Mi)
% 15.59/2.63 % (3816473)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3479361685:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2988 on theBenchmark for (2988ds/2479Mi)
% 15.59/2.63 % (3816473)Refutation not found, incomplete strategy
% 15.59/2.63 % (3816473)------------------------------
% 15.59/2.63 % (3816473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.59/2.63 % (3816473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.59/2.63 % (3816473)CaDiCaL version: 2.1.3
% 15.59/2.63 % (3816473)Termination reason: Refutation not found, incomplete strategy
% 15.59/2.63 % (3816473)Time elapsed: 0.002 s
% 15.59/2.63 % (3816473)Peak memory usage: 89 MB
% 15.59/2.63 % (3816473)Instructions burned: 3 (million)
% 15.59/2.63 % (3816464)------------------------------
% 15.59/2.63 % (3816464)------------------------------
% 15.59/2.63 % (3816475)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2297594018:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/440Mi)
% 15.59/2.63 % (3816466)------------------------------
% 15.59/2.63 % (3816466)------------------------------
% 18.86/3.06 % (3816475)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 18.86/3.06 % (3816478)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=820951299:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2986 on theBenchmark for (2986ds/11145Mi)
% 18.86/3.06 % Exception at run slice level
% 18.86/3.06 User error: GNN currently only supports monomorphic FOL.
% 18.86/3.06 % (3816473)------------------------------
% 18.86/3.06 % (3816473)------------------------------
% 18.86/3.06 % (3816480)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=2168117154:cts=off:i=3034:av=off:er=known:fsd=on_2986 on theBenchmark for (2986ds/3034Mi)
% 18.86/3.06 % (3816475)Instruction limit reached!
% 18.86/3.06 % (3816475)------------------------------
% 18.86/3.06 % (3816475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.86/3.06 % (3816475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.86/3.06 % (3816475)CaDiCaL version: 2.1.3
% 18.86/3.06 % (3816475)Termination reason: Instruction limit
% 18.86/3.06 % (3816475)Termination phase: Saturation
% 18.86/3.06 % (3816475)Time elapsed: 0.118 s
% 18.86/3.06 % (3816475)Peak memory usage: 89 MB
% 18.86/3.06 % (3816475)Instructions burned: 443 (million)
% 18.86/3.06 % Exception at run slice level
% 18.86/3.06 User error: GNN currently only supports monomorphic FOL.
% 18.86/3.06 % (3816482)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=478536309:st=2:s2a=on:i=524:s2at=2:ss=axioms_2985 on theBenchmark for (2985ds/524Mi)
% 18.86/3.06 % (3816483)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2498412779:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2985 on theBenchmark for (2985ds/1016Mi)
% 18.86/3.06 % (3816486)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2096782243:i=5781:kws=precedence:bd=all:rawr=on_2985 on theBenchmark for (2985ds/5781Mi)
% 18.86/3.06 % (3816485)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=4267639494:i=14123:bd=preordered:ins=4_2985 on theBenchmark for (2985ds/14123Mi)
% 18.86/3.06 % Exception at run slice level
% 18.86/3.06 User error: GNN currently only supports monomorphic FOL.
% 18.86/3.06 % Exception at run slice level
% 18.86/3.06 User error: GNN currently only supports monomorphic FOL.
% 18.86/3.06 % (3816482)Instruction limit reached!
% 18.86/3.06 % (3816482)------------------------------
% 18.86/3.06 % (3816482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.86/3.06 % (3816482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.86/3.06 % (3816482)CaDiCaL version: 2.1.3
% 18.86/3.06 % (3816482)Termination reason: Instruction limit
% 18.86/3.06 % (3816482)Termination phase: Saturation
% 18.86/3.06 % (3816482)Time elapsed: 0.131 s
% 18.86/3.06 % (3816482)Peak memory usage: 92 MB
% 18.86/3.06 % (3816482)Instructions burned: 526 (million)
% 18.86/3.06 % (3816491)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=1490626751:i=2448:gtgl=5:bd=preordered:gtg=all_2983 on theBenchmark for (2983ds/2448Mi)
% 18.86/3.06 % (3816492)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=971130078:i=3223:kws=precedence:fgj=on:av=off_2983 on theBenchmark for (2983ds/3223Mi)
% 18.86/3.06 % (3816493)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2005010388:st=5.6:i=2033:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/2033Mi)
% 18.86/3.06 % Exception at run slice level
% 18.86/3.06 User error: GNN currently only supports monomorphic FOL.
% 18.86/3.06 % (3816483)Instruction limit reached!
% 18.86/3.06 % (3816483)------------------------------
% 18.86/3.06 % (3816483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.86/3.06 % (3816483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.86/3.06 % (3816483)CaDiCaL version: 2.1.3
% 18.86/3.06 % (3816483)Termination reason: Instruction limit
% 18.86/3.06 % (3816483)Termination phase: Saturation
% 18.86/3.06 % (3816483)Time elapsed: 0.289 s
% 18.86/3.06 % (3816483)Peak memory usage: 96 MB
% 18.86/3.06 % (3816483)Instructions burned: 1019 (million)
% 18.86/3.06 % (3816497)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3563595905:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2982 on theBenchmark for (2982ds/2055Mi)
% 22.93/3.71 % Exception at run slice level
% 22.93/3.71 User error: GNN currently only supports monomorphic FOL.
% 22.93/3.71 % (3816498)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=2482938856:i=21611:sd=3:ss=axioms_2981 on theBenchmark for (2981ds/21611Mi)
% 22.93/3.71 % Exception at run slice level
% 22.93/3.71 User error: GNN currently only supports monomorphic FOL.
% 22.93/3.71 % Exception at run slice level
% 22.93/3.71 User error: GNN currently only supports monomorphic FOL.
% 22.93/3.71 % (3816500)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1805134585:i=4835:sd=13:ss=axioms:sgt=23_2980 on theBenchmark for (2980ds/4835Mi)
% 22.93/3.71 % (3816500)Refutation not found, incomplete strategy
% 22.93/3.71 % (3816500)------------------------------
% 22.93/3.71 % (3816500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.93/3.71 % (3816500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.93/3.71 % (3816500)CaDiCaL version: 2.1.3
% 22.93/3.71 % (3816500)Termination reason: Refutation not found, incomplete strategy
% 22.93/3.71 % (3816500)Time elapsed: 0.004 s
% 22.93/3.71 % (3816500)Peak memory usage: 89 MB
% 22.93/3.71 % (3816500)Instructions burned: 11 (million)
% 22.93/3.71 % (3816502)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=2001738830:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2980 on theBenchmark for (2980ds/797Mi)
% 22.93/3.71 % (3816503)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=4179485075:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2980 on theBenchmark for (2980ds/2326Mi)
% 22.93/3.71 % (3816503)Refutation not found, incomplete strategy
% 22.93/3.71 % (3816503)------------------------------
% 22.93/3.71 % (3816503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.93/3.71 % (3816503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.93/3.71 % Exception at run slice level
% 22.93/3.71 User error: GNN currently only supports monomorphic FOL.
% 22.93/3.71 % (3816503)CaDiCaL version: 2.1.3
% 22.93/3.71 % (3816503)Termination reason: Refutation not found, incomplete strategy
% 22.93/3.71 % (3816503)Time elapsed: 0.005 s
% 22.93/3.71 % (3816503)Peak memory usage: 89 MB
% 22.93/3.71 % (3816503)Instructions burned: 14 (million)
% 22.93/3.71 % Exception at run slice level
% 22.93/3.71 User error: GNN currently only supports monomorphic FOL.
% 22.93/3.71 % (3816507)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2108632730:i=6038:nm=6_2979 on theBenchmark for (2979ds/6038Mi)
% 22.93/3.71 % (3816500)------------------------------
% 22.93/3.71 % (3816500)------------------------------
% 22.93/3.71 % (3816503)------------------------------
% 22.93/3.71 % (3816503)------------------------------
% 22.93/3.71 % (3816508)lrs+10_1_sil=32000:sp=occurrence:random_seed=3121226204:st=2:i=33334:sd=3:ss=included:sgt=32_2978 on theBenchmark for (2978ds/33334Mi)
% 22.93/3.71 % (3816510)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=371707593:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2978 on theBenchmark for (2978ds/1008Mi)
% 22.93/3.71 % (3816502)Instruction limit reached!
% 22.93/3.71 % (3816502)------------------------------
% 22.93/3.71 % (3816502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.93/3.71 % (3816502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.93/3.71 % (3816502)CaDiCaL version: 2.1.3
% 22.93/3.71 % (3816502)Termination reason: Instruction limit
% 22.93/3.71 % (3816502)Termination phase: Saturation
% 22.93/3.71 % (3816502)Time elapsed: 0.209 s
% 22.93/3.71 % (3816502)Peak memory usage: 90 MB
% 22.93/3.71 % (3816502)Instructions burned: 798 (million)
% 22.93/3.71 % (3816511)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=3643785749:i=8327:s2at=5:bd=preordered_2978 on theBenchmark for (2978ds/8327Mi)
% 22.93/3.71 % (3816465)Instruction limit reached!
% 22.93/3.71 % (3816465)------------------------------
% 22.93/3.71 % (3816465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.93/3.71 % (3816465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.36/4.48 % (3816465)CaDiCaL version: 2.1.3
% 28.36/4.48 % (3816465)Termination reason: Instruction limit
% 28.36/4.48 % (3816465)Termination phase: Saturation
% 28.36/4.48 % (3816465)Time elapsed: 1.146 s
% 28.36/4.48 % (3816465)Peak memory usage: 102 MB
% 28.36/4.48 % (3816465)Instructions burned: 3706 (million)
% 28.36/4.48 % (3816514)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=1359445040:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2977 on theBenchmark for (2977ds/1083Mi)
% 28.36/4.48 % Exception at run slice level
% 28.36/4.48 User error: GNN currently only supports monomorphic FOL.
% 28.36/4.48 % (3816516)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=53017739:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2976 on theBenchmark for (2976ds/1084Mi)
% 28.36/4.48 % (3816518)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2620209199:i=6995:s2at=5:gtg=all_2976 on theBenchmark for (2976ds/6995Mi)
% 28.36/4.48 % Exception at run slice level
% 28.36/4.48 User error: Immediate (shared) subterms of term/literal aa(X1,fun(list(X1),fun(X0,X0)),X4,X3) = sF7(X1,X0,X4,X3) have different types/not well-typed!
% 28.36/4.48 % Exception at run slice level
% 28.36/4.48 User error: GNN currently only supports monomorphic FOL.
% 28.36/4.48 % (3816521)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=804930778:st=2:i=6225:sd=15:ss=axioms_2975 on theBenchmark for (2975ds/6225Mi)
% 28.36/4.48 % (3816521)Refutation not found, incomplete strategy
% 28.36/4.48 % (3816521)------------------------------
% 28.36/4.48 % (3816521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.36/4.48 % (3816521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.36/4.48 % (3816521)CaDiCaL version: 2.1.3
% 28.36/4.48 % (3816521)Termination reason: Refutation not found, incomplete strategy
% 28.36/4.48 % (3816521)Time elapsed: 0.003 s
% 28.36/4.48 % (3816521)Peak memory usage: 89 MB
% 28.36/4.48 % (3816521)Instructions burned: 7 (million)
% 28.36/4.48 % (3816510)Instruction limit reached!
% 28.36/4.48 % (3816510)------------------------------
% 28.36/4.48 % (3816510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.36/4.48 % (3816510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.36/4.48 % (3816510)CaDiCaL version: 2.1.3
% 28.36/4.48 % (3816510)Termination reason: Instruction limit
% 28.36/4.48 % (3816510)Termination phase: Saturation
% 28.36/4.48 % (3816510)Time elapsed: 0.304 s
% 28.36/4.48 % (3816510)Peak memory usage: 97 MB
% 28.36/4.48 % (3816510)Instructions burned: 1011 (million)
% 28.36/4.48 % (3816522)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=139625341:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2975 on theBenchmark for (2975ds/3372Mi)
% 28.36/4.48 % (3816514)Instruction limit reached!
% 28.36/4.48 % (3816514)------------------------------
% 28.36/4.48 % (3816514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.36/4.48 % (3816514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.36/4.48 % (3816514)CaDiCaL version: 2.1.3
% 28.36/4.48 % (3816514)Termination reason: Instruction limit
% 28.36/4.48 % (3816514)Termination phase: Saturation
% 28.36/4.48 % (3816514)Time elapsed: 0.301 s
% 28.36/4.48 % (3816514)Peak memory usage: 100 MB
% 28.36/4.48 % (3816514)Instructions burned: 1083 (million)
% 28.36/4.48 % (3816524)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=4130264536:st=2.3:i=26457:sd=10:ss=included:sgt=8_2974 on theBenchmark for (2974ds/26457Mi)
% 28.36/4.48 % (3816521)------------------------------
% 28.36/4.48 % (3816521)------------------------------
% 28.36/4.48 % (3816526)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=2314418864:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2973 on theBenchmark for (2973ds/13494Mi)
% 28.36/4.48 % (3816516)Instruction limit reached!
% 28.36/4.48 % (3816516)------------------------------
% 28.36/4.48 % (3816516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.36/4.48 % (3816516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.36/4.48 % (3816516)CaDiCaL version: 2.1.3
% 28.36/4.48 % (3816516)Termination reason: Instruction limit
% 28.36/4.48 % (3816516)Termination phase: Saturation
% 34.53/5.30 % (3816516)Time elapsed: 0.326 s
% 34.53/5.30 % (3816516)Peak memory usage: 99 MB
% 34.53/5.30 % (3816516)Instructions burned: 1085 (million)
% 34.53/5.30 % Exception at run slice level
% 34.53/5.30 User error: GNN currently only supports monomorphic FOL.
% 34.53/5.30 % (3816528)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=744740315:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2972 on theBenchmark for (2972ds/2503Mi)
% 34.53/5.30 % (3816528)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 34.53/5.30 % (3816530)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2685289071:i=2559:sd=1:ep=RSTC:ss=axioms_2972 on theBenchmark for (2972ds/2559Mi)
% 34.53/5.30 % Exception at run slice level
% 34.53/5.30 User error: GNN currently only supports monomorphic FOL.
% 34.53/5.30 % (3816531)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=532079261:i=30753:av=off:ss=included_2972 on theBenchmark for (2972ds/30753Mi)
% 34.53/5.30 % Exception at run slice level
% 34.53/5.30 User error: GNN currently only supports monomorphic FOL.
% 34.53/5.30 % (3816535)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3349264980:i=26473:ep=RSTC_2971 on theBenchmark for (2971ds/26473Mi)
% 34.53/5.30 % Exception at run slice level
% 34.53/5.30 User error: GNN currently only supports monomorphic FOL.
% 34.53/5.30 % (3816536)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=1965939194:cts=off:i=2759:kws=inv_arity:fgj=on_2970 on theBenchmark for (2970ds/2759Mi)
% 34.53/5.30 % Exception at run slice level
% 34.53/5.30 User error: GNN currently only supports monomorphic FOL.
% 34.53/5.30 % Exception at run slice level
% 34.53/5.30 User error: GNN currently only supports monomorphic FOL.
% 34.53/5.30 % (3816538)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=3758476526:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2969 on theBenchmark for (2969ds/5665Mi)
% 34.53/5.30 % (3816538)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 34.53/5.30 % (3816540)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=3689662203:i=1532:ep=RS:ss=axioms_2969 on theBenchmark for (2969ds/1532Mi)
% 34.53/5.30 % (3816541)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=2289523868:i=1565:sd=2:ss=axioms:sgt=32_2969 on theBenchmark for (2969ds/1565Mi)
% 34.53/5.30 % (3816486)Instruction limit reached!
% 34.53/5.30 % (3816486)------------------------------
% 34.53/5.30 % (3816486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.53/5.30 % (3816486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.53/5.30 % (3816486)CaDiCaL version: 2.1.3
% 34.53/5.30 % (3816486)Termination reason: Instruction limit
% 34.53/5.30 % (3816486)Termination phase: Saturation
% 34.53/5.30 % (3816486)Time elapsed: 1.657 s
% 34.53/5.30 % (3816486)Peak memory usage: 123 MB
% 34.53/5.30 % (3816486)Instructions burned: 5782 (million)
% 34.53/5.30 % Exception at run slice level
% 34.53/5.30 User error: GNN currently only supports monomorphic FOL.
% 34.53/5.30 % (3816545)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=2444405784:i=1572:fgj=on:gsp=on_2967 on theBenchmark for (2967ds/1572Mi)
% 34.53/5.30 % (3816545)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 34.53/5.30 % Exception at run slice level
% 34.53/5.30 User error: GNN currently only supports monomorphic FOL.
% 34.53/5.30 % Exception at run slice level
% 34.53/5.30 User error: GNN currently only supports monomorphic FOL.
% 34.53/5.30 % (3816546)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=3976409513:i=6052:sd=4:ss=axioms:sgt=24_2967 on theBenchmark for (2967ds/6052Mi)
% 34.53/5.30 % Exception at run slice level
% 34.53/5.30 User error: GNN currently only supports monomorphic FOL.
% 34.53/5.30 % (3816548)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=4083266659:i=3500:sd=1:bd=preordered:sup=off:ss=included_2966 on theBenchmark for (2966ds/3500Mi)
% 40.90/6.16 % (3816550)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=3466751221:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2966 on theBenchmark for (2966ds/1842Mi)
% 40.90/6.16 % (3816550)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 40.90/6.16 % (3816551)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1407903978:i=66096:add=on_2966 on theBenchmark for (2966ds/66096Mi)
% 40.90/6.16 % Exception at run slice level
% 40.90/6.16 User error: GNN currently only supports monomorphic FOL.
% 40.90/6.16 % Exception at run slice level
% 40.90/6.16 User error: GNN currently only supports monomorphic FOL.
% 40.90/6.16 % (3816555)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2117415364:i=1884:sd=1:nm=60:ss=axioms_2965 on theBenchmark for (2965ds/1884Mi)
% 40.90/6.16 % Exception at run slice level
% 40.90/6.16 User error: GNN currently only supports monomorphic FOL.
% 40.90/6.16 % Exception at run slice level
% 40.90/6.16 User error: GNN currently only supports monomorphic FOL.
% 40.90/6.16 % (3816556)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3663349209:cts=off:i=5469:bs=on:fsr=off_2964 on theBenchmark for (2964ds/5469Mi)
% 40.90/6.16 % Exception at run slice level
% 40.90/6.16 User error: GNN currently only supports monomorphic FOL.
% 40.90/6.16 % (3816558)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=2797179099:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2963 on theBenchmark for (2963ds/2037Mi)
% 40.90/6.16 % (3816559)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2066731709:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2963 on theBenchmark for (2963ds/2110Mi)
% 40.90/6.16 % (3816561)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=3448757232:i=2430:add=off:aac=none:nm=16_2963 on theBenchmark for (2963ds/2430Mi)
% 40.90/6.16 % Exception at run slice level
% 40.90/6.16 User error: GNN currently only supports monomorphic FOL.
% 40.90/6.16 % (3816565)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=3027854432:cond=fast:i=4891_2962 on theBenchmark for (2962ds/4891Mi)
% 40.90/6.16 % Exception at run slice level% Exception at run slice level
% 40.90/6.16
% 40.90/6.16 User error: User error: GNN currently only supports monomorphic FOL.GNN currently only supports monomorphic FOL.
% 40.90/6.16
% 40.90/6.16 % Exception at run slice level
% 40.90/6.16 User error: GNN currently only supports monomorphic FOL.
% 40.90/6.16 % (3816568)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=1195851116:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2961 on theBenchmark for (2961ds/7534Mi)
% 40.90/6.16 % (3816567)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=3076142023:st=2:i=14845:sd=2:ss=included:fsd=on_2961 on theBenchmark for (2961ds/14845Mi)
% 40.90/6.16 % (3816569)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=3655980232:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2960 on theBenchmark for (2960ds/10353Mi)
% 40.90/6.16 % Exception at run slice level
% 40.90/6.16 User error: GNN currently only supports monomorphic FOL.
% 40.90/6.16 % (3816573)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4026284423:i=7860_2959 on theBenchmark for (2959ds/7860Mi)
% 40.90/6.16 % (3816573)Refutation not found, incomplete strategy
% 40.90/6.16 % (3816573)------------------------------
% 40.90/6.16 % (3816573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.90/6.16 % (3816573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.90/6.16 % (3816573)CaDiCaL version: 2.1.3
% 40.90/6.16 % (3816573)Termination reason: Refutation not found, incomplete strategy
% 47.93/7.19 % (3816573)Time elapsed: 0.003 s
% 47.93/7.19 % (3816573)Peak memory usage: 89 MB
% 47.93/7.19 % (3816573)Instructions burned: 10 (million)
% 47.93/7.19 % Exception at run slice level
% 47.93/7.19 User error: GNN currently only supports monomorphic FOL.
% 47.93/7.19 % Exception at run slice level
% 47.93/7.19 User error: GNN currently only supports monomorphic FOL.
% 47.93/7.19 % Exception at run slice level
% 47.93/7.19 User error: GNN currently only supports monomorphic FOL.
% 47.93/7.19 % (3816575)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=3481771668:i=7896:sd=2:bs=on:ss=included:sgt=20_2958 on theBenchmark for (2958ds/7896Mi)
% 47.93/7.19 % (3816576)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1645404276:i=5812:gtgl=2:gtg=all_2958 on theBenchmark for (2958ds/5812Mi)
% 47.93/7.19 % (3816573)------------------------------
% 47.93/7.19 % (3816573)------------------------------
% 47.93/7.19 % (3816577)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=561192765:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2957 on theBenchmark for (2957ds/2965Mi)
% 47.93/7.19 % (3816581)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=521118281:i=2967:kws=precedence:bd=preordered:av=off_2956 on theBenchmark for (2956ds/2967Mi)
% 47.93/7.19 % Exception at run slice level
% 47.93/7.19 User error: GNN currently only supports monomorphic FOL.
% 47.93/7.19 % Exception at run slice level
% 47.93/7.19 User error: GNN currently only supports monomorphic FOL.
% 47.93/7.19 % Exception at run slice level
% 47.93/7.19 User error: GNN currently only supports monomorphic FOL.
% 47.93/7.19 % (3816584)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=4025382947:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2955 on theBenchmark for (2955ds/3207Mi)
% 47.93/7.19 % (3816583)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=1648012623:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2955 on theBenchmark for (2955ds/3022Mi)
% 47.93/7.19 % (3816585)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=362205019:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2954 on theBenchmark for (2954ds/3289Mi)
% 47.93/7.19 % Exception at run slice level
% 47.93/7.19 User error: GNN currently only supports monomorphic FOL.
% 47.93/7.19 % (3816589)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=4093955284:i=38569:sd=3:ss=axioms:sgt=32_2953 on theBenchmark for (2953ds/38569Mi)
% 47.93/7.19 % Exception at run slice level
% 47.93/7.19 User error: GNN currently only supports monomorphic FOL.
% 47.93/7.19 % Exception at run slice level
% 47.93/7.19 User error: GNN currently only supports monomorphic FOL.
% 47.93/7.19 % Exception at run slice level
% 47.93/7.19 User error: GNN currently only supports monomorphic FOL.
% 47.93/7.19 % (3816591)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=1550868357:cts=off:i=3394_2952 on theBenchmark for (2952ds/3394Mi)
% 47.93/7.19 % (3816592)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=1498181813:i=33824:bd=preordered_2952 on theBenchmark for (2952ds/33824Mi)
% 47.93/7.19 % Exception at run slice level
% 47.93/7.19 User error: GNN currently only supports monomorphic FOL.
% 47.93/7.19 % (3816593)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=494397946:i=20684:bd=all:gtg=exists_sym_2952 on theBenchmark for (2952ds/20684Mi)
% 47.93/7.19 % (3816596)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=1362510958: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_2951 on theBenchmark for (2951ds/7222Mi)
% 47.93/7.19 % (3816596)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 64.24/9.52 % Exception at run slice level
% 64.24/9.52 User error: GNN currently only supports monomorphic FOL.
% 64.24/9.52 % Exception at run slice level
% 64.24/9.52 User error: GNN currently only supports monomorphic FOL.
% 64.24/9.52 % Exception at run slice level
% 64.24/9.52 User error: GNN currently only supports monomorphic FOL.
% 64.24/9.52 % (3816600)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=3270184466:i=4036:ins=10_2949 on theBenchmark for (2949ds/4036Mi)
% 64.24/9.52 % (3816599)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=1402809609:st=4:i=7295:sd=4:ep=R:ss=axioms_2949 on theBenchmark for (2949ds/7295Mi)
% 64.24/9.52 % Exception at run slice level
% 64.24/9.52 User error: GNN currently only supports monomorphic FOL.
% 64.24/9.52 % (3816601)lrs+10_1_sil=128000:lcm=predicate:random_seed=278344324:st=3:i=43697:sd=5:ss=axioms_2948 on theBenchmark for (2948ds/43697Mi)
% 64.24/9.52 % (3816604)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=154481102:i=17599:gtg=all:ss=axioms:fsd=on_2948 on theBenchmark for (2948ds/17599Mi)
% 64.24/9.52 % (3816556)Instruction limit reached!
% 64.24/9.52 % (3816556)------------------------------
% 64.24/9.52 % (3816556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.24/9.52 % (3816556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.24/9.52 % (3816556)CaDiCaL version: 2.1.3
% 64.24/9.52 % (3816556)Termination reason: Instruction limit
% 64.24/9.52 % (3816556)Termination phase: Saturation
% 64.24/9.52 % (3816556)Time elapsed: 1.656 s
% 64.24/9.52 % (3816556)Peak memory usage: 104 MB
% 64.24/9.52 % (3816556)Instructions burned: 5473 (million)
% 64.24/9.52 % Exception at run slice level
% 64.24/9.52 User error: GNN currently only supports monomorphic FOL.
% 64.24/9.52 % Exception at run slice level
% 64.24/9.52 User error: GNN currently only supports monomorphic FOL.
% 64.24/9.52 % (3816607)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=1856145805:i=4547:bd=preordered_2947 on theBenchmark for (2947ds/4547Mi)
% 64.24/9.52 % (3816609)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2324445584:i=32849:add=on_2946 on theBenchmark for (2946ds/32849Mi)
% 64.24/9.52 % (3816608)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=312568994:i=9294:av=off_2946 on theBenchmark for (2946ds/9294Mi)
% 64.24/9.52 % Exception at run slice level
% 64.24/9.52 User error: GNN currently only supports monomorphic FOL.
% 64.24/9.52 % (3816613)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=96320760:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2945 on theBenchmark for (2945ds/4793Mi)
% 64.24/9.52 % Exception at run slice level
% 64.24/9.52 User error: GNN currently only supports monomorphic FOL.
% 64.24/9.52 % Exception at run slice level
% 64.24/9.52 User error: GNN currently only supports monomorphic FOL.
% 64.24/9.52 % Exception at run slice level
% 64.24/9.52 User error: GNN currently only supports monomorphic FOL.
% 64.24/9.52 % (3816615)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=2817737730:i=4840:nm=4:av=off_2944 on theBenchmark for (2944ds/4840Mi)
% 64.24/9.52 % (3816617)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=3624243753:i=30479:sd=3:ss=axioms_2943 on theBenchmark for (2943ds/30479Mi)
% 64.24/9.52 % (3816616)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=2435662196:cts=off:i=5002_2943 on theBenchmark for (2943ds/5002Mi)
% 64.24/9.52 % Exception at run slice level
% 64.24/9.52 User error: GNN currently only supports monomorphic FOL.
% 64.24/9.52 % (3816621)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=2667339541:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2942 on theBenchmark for (2942ds/11035Mi)
% 64.24/9.52 % (3816621)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 82.39/12.07 % Exception at run slice level
% 82.39/12.07 User error: GNN currently only supports monomorphic FOL.
% 82.39/12.07 % Exception at run slice level
% 82.39/12.07 User error: GNN currently only supports monomorphic FOL.
% 82.39/12.07 % Exception at run slice level
% 82.39/12.07 User error: GNN currently only supports monomorphic FOL.
% 82.39/12.07 % (3816623)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=3379207891:i=5835_2941 on theBenchmark for (2941ds/5835Mi)
% 82.39/12.07 % (3816625)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=3806057434:cts=off:i=19910:ep=RS_2940 on theBenchmark for (2940ds/19910Mi)
% 82.39/12.07 % (3816624)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=662049843:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2940 on theBenchmark for (2940ds/5890Mi)
% 82.39/12.07 % (3816625)Refutation not found, incomplete strategy
% 82.39/12.07 % (3816625)------------------------------
% 82.39/12.07 % (3816625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.39/12.07 % (3816625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.39/12.07 % (3816625)CaDiCaL version: 2.1.3
% 82.39/12.07 % (3816625)Termination reason: Refutation not found, incomplete strategy
% 82.39/12.07 % (3816625)Time elapsed: 0.003 s
% 82.39/12.07 % (3816625)Peak memory usage: 88 MB
% 82.39/12.07 % (3816625)Instructions burned: 11 (million)
% 82.39/12.07 % Exception at run slice level
% 82.39/12.07 User error: GNN currently only supports monomorphic FOL.
% 82.39/12.07 % (3816629)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=2421519188:i=20312:bd=preordered:fsr=off:er=filter_2939 on theBenchmark for (2939ds/20312Mi)
% 82.39/12.07 % Exception at run slice level
% 82.39/12.07 User error: GNN currently only supports monomorphic FOL.
% 82.39/12.07 % (3816625)------------------------------
% 82.39/12.07 % (3816625)------------------------------
% 82.39/12.07 % Exception at run slice level
% 82.39/12.07 User error: GNN currently only supports monomorphic FOL.
% 82.39/12.07 % (3816631)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=560958894:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2938 on theBenchmark for (2938ds/13822Mi)
% 82.39/12.07 % (3816632)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=1171429448:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2938 on theBenchmark for (2938ds/7144Mi)
% 82.39/12.07 % (3816633)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=2128018849:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2937 on theBenchmark for (2937ds/15184Mi)
% 82.39/12.07 % Exception at run slice level
% 82.39/12.07 User error: GNN currently only supports monomorphic FOL.
% 82.39/12.07 % (3816637)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=2240553785:i=107375_2936 on theBenchmark for (2936ds/107375Mi)
% 82.39/12.07 % Exception at run slice level
% 82.39/12.07 User error: GNN currently only supports monomorphic FOL.
% 82.39/12.07 % Exception at run slice level
% 82.39/12.07 User error: GNN currently only supports monomorphic FOL.
% 82.39/12.07 % (3816639)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=2007454260:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2935 on theBenchmark for (2935ds/7958Mi)
% 82.39/12.07 % Exception at run slice level
% 82.39/12.07 User error: GNN currently only supports monomorphic FOL.
% 82.39/12.07 % (3816640)dis+10_128_sil=16000:nwc=0.7:random_seed=2725814691:i=15999:nm=2:gsp=on_2934 on theBenchmark for (2934ds/15999Mi)
% 82.39/12.07 % (3816640)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 82.39/12.07 % (3816643)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=2755838260:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2933 on theBenchmark for (2933ds/8139Mi)
% 82.39/12.07 % Exception at run slice level
% 82.39/12.07 User error: GNN currently only supports monomorphic FOL.
% 82.39/12.07 % (3816645)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=1999320094:st=4:i=8950:sd=5:ss=axioms_2932 on theBenchmark for (2932ds/8950Mi)
% 90.68/13.26 % Exception at run slice level
% 90.68/13.26 User error: GNN currently only supports monomorphic FOL.
% 90.68/13.26 % (3816647)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=3448136363:i=9809:ins=10:av=off_2929 on theBenchmark for (2929ds/9809Mi)
% 90.68/13.26 % Exception at run slice level
% 90.68/13.26 User error: GNN currently only supports monomorphic FOL.
% 90.68/13.26 % (3816649)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=583358573:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2926 on theBenchmark for (2926ds/9885Mi)
% 90.68/13.26 % Exception at run slice level
% 90.68/13.26 User error: GNN currently only supports monomorphic FOL.
% 90.68/13.26 % (3816651)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=4218035707:cond=fast:i=32078:fgj=on:av=off_2923 on theBenchmark for (2923ds/32078Mi)
% 90.68/13.26 % Exception at run slice level
% 90.68/13.26 User error: GNN currently only supports monomorphic FOL.
% 90.68/13.26 % (3816653)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=957653951:i=11101:bd=all:ss=axioms:sgt=8_2919 on theBenchmark for (2919ds/11101Mi)
% 90.68/13.26 % (3816643)Instruction limit reached!
% 90.68/13.26 % (3816643)------------------------------
% 90.68/13.26 % (3816643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.68/13.26 % (3816643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.68/13.26 % (3816643)CaDiCaL version: 2.1.3
% 90.68/13.26 % (3816643)Termination reason: Instruction limit
% 90.68/13.26 % (3816643)Termination phase: Saturation
% 90.68/13.26 % (3816643)Time elapsed: 1.633 s
% 90.68/13.26 % (3816643)Peak memory usage: 89 MB
% 90.68/13.26 % (3816643)Instructions burned: 8141 (million)
% 90.68/13.26 % (3816632)Instruction limit reached!
% 90.68/13.26 % (3816632)------------------------------
% 90.68/13.26 % (3816632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 90.68/13.26 % (3816632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 90.68/13.26 % (3816632)CaDiCaL version: 2.1.3
% 90.68/13.26 % (3816632)Termination reason: Instruction limit
% 90.68/13.26 % (3816632)Termination phase: Saturation
% 90.68/13.26 % (3816632)Time elapsed: 2.137 s
% 90.68/13.26 % (3816632)Peak memory usage: 150 MB
% 90.68/13.26 % (3816632)Instructions burned: 7146 (million)
% 90.68/13.26 % (3816655)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=131802175:cond=on:i=13220:s2at=3:aac=none:fsd=on_2916 on theBenchmark for (2916ds/13220Mi)
% 90.68/13.26 % (3816656)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=3675412790:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2915 on theBenchmark for (2915ds/13528Mi)
% 90.68/13.26 % Exception at run slice level
% 90.68/13.26 User error: GNN currently only supports monomorphic FOL.
% 90.68/13.26 % (3816659)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=2594975850:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2913 on theBenchmark for (2913ds/14854Mi)
% 90.68/13.26 % Exception at run slice level
% 90.68/13.26 User error: GNN currently only supports monomorphic FOL.
% 90.68/13.26 % (3816661)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=1366887365:i=14974:ss=axioms:sgt=16_2912 on theBenchmark for (2912ds/14974Mi)
% 90.68/13.26 % Exception at run slice level
% 90.68/13.26 User error: GNN currently only supports monomorphic FOL.
% 90.68/13.26 % (3816663)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=2947386771:i=33081:aac=none:fgj=on:bd=all:fsr=off_2910 on theBenchmark for (2910ds/33081Mi)
% 90.68/13.26 % Exception at run slice level
% 90.68/13.26 User error: GNN currently only supports monomorphic FOL.
% 90.68/13.26 % (3816665)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=2214729007:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2909 on theBenchmark for (2909ds/50856Mi)
% 90.68/13.26 % Exception at run slice level
% 90.68/13.26 User error: GNN currently only supports monomorphic FOL.
% 100.51/14.65 % (3816667)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=2321536403:i=69865_2907 on theBenchmark for (2907ds/69865Mi)
% 100.51/14.65 % Exception at run slice level
% 100.51/14.65 User error: GNN currently only supports monomorphic FOL.
% 100.51/14.65 % (3816669)lrs+1002_1_anc=none:to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:sp=arity:sos=on:spb=intro:lcm=reverse:random_seed=3370405529:cond=fast:i=17802:gtgl=3:gtg=all_2906 on theBenchmark for (2906ds/17802Mi)
% 100.51/14.65 % Exception at run slice level
% 100.51/14.65 User error: Immediate (shared) subterms of term/literal aa(X1,fun(list(X1),X0),X4,X3) = sF32(X1,X0,X4,X3) have different types/not well-typed!
% 100.51/14.65 % (3816671)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=1212935675:i=96644_2905 on theBenchmark for (2905ds/96644Mi)
% 100.51/14.65 % Exception at run slice level
% 100.51/14.65 User error: GNN currently only supports monomorphic FOL.
% 100.51/14.65 % (3816673)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0
% 100.51/14.65 % (3816673)dis+1011_1_to=kbo:ncem=casc2026/models/loop8.pt:tgt=ground:irw=on:drc=off:sp=unary_first:bce=on:bsr=unit_only:kmz=on:sac=on:random_seed=2097280665:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2904 on theBenchmark for (2904ds/21161Mi)
% 100.51/14.65 % (3816535)Instruction limit reached!
% 100.51/14.65 % (3816535)------------------------------
% 100.51/14.65 % (3816535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.51/14.65 % (3816535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.51/14.65 % (3816535)CaDiCaL version: 2.1.3
% 100.51/14.65 % (3816535)Termination reason: Instruction limit
% 100.51/14.65 % (3816535)Termination phase: Saturation
% 100.51/14.65 % (3816535)Time elapsed: 7.914 s
% 100.51/14.65 % (3816535)Peak memory usage: 413 MB
% 100.51/14.65 % (3816535)Instructions burned: 26475 (million)
% 100.51/14.65 % (3816675)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=2165253996:i=22761:gtg=all:ss=axioms:fsd=on_2891 on theBenchmark for (2891ds/22761Mi)
% 100.51/14.65 % Exception at run slice level
% 100.51/14.65 User error: GNN currently only supports monomorphic FOL.
% 100.51/14.65 % (3816677)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=1509264395:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2888 on theBenchmark for (2888ds/23713Mi)
% 100.51/14.65 % (3816677)Refutation not found, incomplete strategy
% 100.51/14.65 % (3816677)------------------------------
% 100.51/14.65 % (3816677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.51/14.65 % (3816677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.51/14.65 % (3816677)CaDiCaL version: 2.1.3
% 100.51/14.65 % (3816677)Termination reason: Refutation not found, incomplete strategy
% 100.51/14.65 % (3816677)Time elapsed: 0.003 s
% 100.51/14.65 % (3816677)Peak memory usage: 88 MB
% 100.51/14.65 % (3816677)Instructions burned: 7 (million)
% 100.51/14.65 % (3816677)------------------------------
% 100.51/14.65 % (3816677)------------------------------
% 100.51/14.65 % (3816679)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=1881673804:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2885 on theBenchmark for (2885ds/26509Mi)
% 100.51/14.65 % (3816640)Instruction limit reached!
% 100.51/14.65 % (3816640)------------------------------
% 100.51/14.65 % (3816640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.51/14.65 % (3816640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.51/14.65 % (3816640)CaDiCaL version: 2.1.3
% 100.51/14.65 % (3816640)Termination reason: Instruction limit
% 100.51/14.65 % (3816640)Termination phase: Saturation
% 100.51/14.65 % (3816640)Time elapsed: 4.950 s
% 100.51/14.65 % (3816640)Peak memory usage: 203 MB
% 100.51/14.65 % (3816640)Instructions burned: 16000 (million)
% 100.51/14.65 % (3816681)dis+1011_1_to=kbo:ncem=casc2026/models/loop6.pt:tgt=ground:drc=off:fde=unused:sp=const_frequency:spb=units:bsr=on:sac=on:random_seed=2442966070:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2884 on theBenchmark for (2884ds/28957Mi)
% 100.51/14.65 % Exception at run slice level
% 100.51/14.65 User error: GNN currently only supports monomorphic FOL.
% 100.51/14.65 % (3816653)Instruction limit reached!
% 100.51/14.65 % (3816653)------------------------------
% 104.62/15.27 % (3816653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.62/15.27 % (3816653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.62/15.27 % (3816653)CaDiCaL version: 2.1.3
% 104.62/15.27 % (3816653)Termination reason: Instruction limit
% 104.62/15.27 % (3816653)Termination phase: Saturation
% 104.62/15.27 % (3816653)Time elapsed: 3.620 s
% 104.62/15.27 % (3816653)Peak memory usage: 169 MB
% 104.62/15.27 % (3816653)Instructions burned: 11102 (million)
% 104.62/15.27 % (3816683)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:drc=off:sp=const_max:spb=goal_then_units:lcm=predicate:urr=ec_only:fd=preordered:gs=on:sac=on:random_seed=2315046163:i=29246:s2at=-1:kws=inv_arity:ins=10_2882 on theBenchmark for (2882ds/29246Mi)
% 104.62/15.27 % (3816684)ott+1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:sp=weighted_frequency:urr=on:gs=on:s2agt=32:sac=on:random_seed=2269496607:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2882 on theBenchmark for (2882ds/30082Mi)
% 104.62/15.27 % (3816684)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 104.62/15.27 % Exception at run slice level
% 104.62/15.27 User error: GNN currently only supports monomorphic FOL.
% 104.62/15.27 % Exception at run slice level
% 104.62/15.27 User error: GNN currently only supports monomorphic FOL.
% 104.62/15.27 % (3816687)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=1041796356:i=32262:bd=preordered_2880 on theBenchmark for (2880ds/32262Mi)
% 104.62/15.27 % (3816688)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=3656252678:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2879 on theBenchmark for (2879ds/32870Mi)
% 104.62/15.27 % Exception at run slice level
% 104.62/15.27 User error: GNN currently only supports monomorphic FOL.
% 104.62/15.27 % Exception at run slice level
% 104.62/15.27 User error: GNN currently only supports monomorphic FOL.
% 104.62/15.27 % (3816691)lrs-1010_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:prc=on:sp=reverse_frequency:spb=goal:acc=on:kmz=on:random_seed=1438212714:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2877 on theBenchmark for (2877ds/33295Mi)
% 104.62/15.27 % (3816692)dis+11_1_anc=none:sfv=off:to=kbo:ncem=casc2026/models/loop6.pt:lma=off:bsr=unit_only:s2agt=8:kmz=on:sac=on:random_seed=2003610154:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2876 on theBenchmark for (2876ds/36826Mi)
% 104.62/15.27 % (3816508)Instruction limit reached!
% 104.62/15.27 % (3816508)------------------------------
% 104.62/15.27 % (3816508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.62/15.27 % (3816508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.62/15.27 % (3816508)CaDiCaL version: 2.1.3
% 104.62/15.27 % (3816508)Termination reason: Instruction limit
% 104.62/15.27 % (3816508)Termination phase: Saturation
% 104.62/15.27 % (3816508)Time elapsed: 10.289 s
% 104.62/15.27 % (3816508)Peak memory usage: 193 MB
% 104.62/15.27 % (3816508)Instructions burned: 33335 (million)
% 104.62/15.27 % Exception at run slice level
% 104.62/15.27 User error: GNN currently only supports monomorphic FOL.
% 104.62/15.27 % (3816695)lrs-1003_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:spb=goal:bsr=unit_only:gs=on:br=off:flr=on:sac=on:random_seed=3040698595:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2874 on theBenchmark for (2874ds/92981Mi)
% 104.62/15.27 % (3816696)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=2195654628:s2pl=on:i=49423_2874 on theBenchmark for (2874ds/49423Mi)
% 104.62/15.27 % Exception at run slice level
% 104.62/15.27 User error: GNN currently only supports monomorphic FOL.
% 104.62/15.27 % Exception at run slice level
% 104.62/15.27 User error: GNN currently only supports monomorphic FOL.
% 104.62/15.27 % (3816699)lrs+1002_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:tgt=ground:npcc=on:prc=on:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:rp=on:updr=off:sac=on:random_seed=3953279760:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2871 on theBenchmark for (2871ds/57299Mi)
% 104.62/15.27 % (3816700)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=627918400:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2871 on theBenchmark for (2871ds/127679Mi)
% 111.28/16.18 % Exception at run slice level
% 111.28/16.18 User error: GNN currently only supports monomorphic FOL.
% 111.28/16.18 % Exception at run slice level
% 111.28/16.18 User error: GNN currently only supports monomorphic FOL.
% 111.28/16.18 % (3816703)lrs+31_1_anc=all:to=lpo:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_arity:fs=off:lcm=predicate:alpa=false:flr=on:random_seed=1031498828:i=69402:add=on:aac=none:fsr=off_2868 on theBenchmark for (2868ds/69402Mi)
% 111.28/16.18 % (3816704)lrs-2_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:drc=off:sas=cadical:sp=reverse_frequency:lcm=predicate:acc=on:bsr=unit_only:fd=preordered:sac=on:random_seed=1414770733:i=100512:doe=on:fgj=on:bd=all:fsd=on_2868 on theBenchmark for (2868ds/100512Mi)
% 111.28/16.18 % Exception at run slice level
% 111.28/16.18 User error: GNN currently only supports monomorphic FOL.
% 111.28/16.18 % Exception at run slice level
% 111.28/16.18 User error: GNN currently only supports monomorphic FOL.
% 111.28/16.18 % (3816707)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=2694145096:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2865 on theBenchmark for (2865ds/138761Mi)
% 111.28/16.18 % (3816708)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:si=on:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3686179156:i=282386:rtra=on_2865 on theBenchmark for (2865ds/282386Mi)
% 111.28/16.18 % Exception at run slice level
% 111.28/16.18 User error: GNN currently only supports monomorphic FOL.
% 111.28/16.18 % Exception at run slice level
% 111.28/16.18 User error: GNN currently only supports monomorphic FOL.
% 111.28/16.18 % (3816711)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:si=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3787922358:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2862 on theBenchmark for (2862ds/269354Mi)
% 111.28/16.18 % (3816712)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:si=on:sos=all:bsr=unit_only:sac=on:random_seed=3184073323:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2862 on theBenchmark for (2862ds/283390Mi)
% 111.28/16.18 % (3816712)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 111.28/16.18 % Exception at run slice level
% 111.28/16.18 User error: GNN currently only supports monomorphic FOL.
% 111.28/16.18 % Exception at run slice level
% 111.28/16.18 User error: GNN currently only supports monomorphic FOL.
% 111.28/16.18 % (3816715)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=2642751734:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2860 on theBenchmark for (2860ds/218Mi)
% 111.28/16.18 % (3816715)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 111.28/16.18 % (3816715)Refutation not found, incomplete strategy
% 111.28/16.18 % (3816715)------------------------------
% 111.28/16.18 % (3816715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.28/16.18 % (3816715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.28/16.18 % (3816715)CaDiCaL version: 2.1.3
% 111.28/16.18 % (3816715)Termination reason: Refutation not found, incomplete strategy
% 111.28/16.18 % (3816715)Time elapsed: 0.001 s
% 111.28/16.18 % (3816715)Peak memory usage: 88 MB
% 111.28/16.18 % (3816715)Instructions burned: 1 (million)
% 111.28/16.18 % (3816716)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=1351102813:i=238:av=off:rtra=on:ss=axioms_2859 on theBenchmark for (2859ds/238Mi)
% 111.28/16.18 % (3816716)Instruction limit reached!
% 111.28/16.18 % (3816716)------------------------------
% 111.28/16.18 % (3816716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.28/16.18 % (3816716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.28/16.18 % (3816716)CaDiCaL version: 2.1.3
% 111.28/16.18 % (3816716)Termination reason: Instruction limit
% 111.28/16.18 % (3816716)Termination phase: Saturation
% 111.28/16.18 % (3816716)Time elapsed: 0.073 s
% 111.28/16.18 % (3816716)Peak memory usage: 89 MB
% 111.28/16.18 % (3816716)Instructions burned: 240 (million)
% 111.28/16.18 % (3816715)------------------------------
% 111.28/16.18 % (3816715)------------------------------
% 111.28/16.18 % (3816719)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=1696680174:s2a=on:i=278:rtra=on:gtg=position_2857 on theBenchmark for (2857ds/278Mi)
% 111.28/16.18 % (3816720)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=3112143227:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2857 on theBenchmark for (2857ds/258Mi)
% 115.09/16.75 % (3816720)Instruction limit reached!
% 115.09/16.75 % (3816720)------------------------------
% 115.09/16.75 % (3816720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.09/16.75 % (3816720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.09/16.75 % (3816720)CaDiCaL version: 2.1.3
% 115.09/16.75 % (3816720)Termination reason: Instruction limit
% 115.09/16.75 % (3816720)Termination phase: Saturation
% 115.09/16.75 % (3816720)Time elapsed: 0.054 s
% 115.09/16.75 % (3816720)Peak memory usage: 93 MB
% 115.09/16.75 % (3816720)Instructions burned: 261 (million)
% 115.09/16.75 % (3816719)Instruction limit reached!
% 115.09/16.75 % (3816719)------------------------------
% 115.09/16.75 % (3816719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.09/16.75 % (3816719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.09/16.75 % (3816719)CaDiCaL version: 2.1.3
% 115.09/16.75 % (3816719)Termination reason: Instruction limit
% 115.09/16.75 % (3816719)Termination phase: Saturation
% 115.09/16.75 % (3816719)Time elapsed: 0.096 s
% 115.09/16.75 % (3816719)Peak memory usage: 90 MB
% 115.09/16.75 % (3816719)Instructions burned: 278 (million)
% 115.09/16.75 % (3816723)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=1942333843:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2856 on theBenchmark for (2856ds/570Mi)
% 115.09/16.75 % (3816724)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=3162421055:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2856 on theBenchmark for (2856ds/314Mi)
% 115.09/16.75 % (3816724)Instruction limit reached!
% 115.09/16.75 % (3816724)------------------------------
% 115.09/16.75 % (3816724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.09/16.75 % (3816724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.09/16.75 % (3816724)CaDiCaL version: 2.1.3
% 115.09/16.75 % (3816724)Termination reason: Instruction limit
% 115.09/16.75 % (3816724)Termination phase: Saturation
% 115.09/16.75 % (3816724)Time elapsed: 0.089 s
% 115.09/16.75 % (3816724)Peak memory usage: 90 MB
% 115.09/16.75 % (3816724)Instructions burned: 317 (million)
% 115.09/16.75 % (3816727)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=1173587728:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2854 on theBenchmark for (2854ds/650Mi)
% 115.09/16.75 % (3816723)Instruction limit reached!
% 115.09/16.75 % (3816723)------------------------------
% 115.09/16.75 % (3816723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.09/16.75 % (3816723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.09/16.75 % (3816723)CaDiCaL version: 2.1.3
% 115.09/16.75 % (3816723)Termination reason: Instruction limit
% 115.09/16.75 % (3816723)Termination phase: Saturation
% 115.09/16.75 % (3816723)Time elapsed: 0.179 s
% 115.09/16.75 % (3816723)Peak memory usage: 93 MB
% 115.09/16.75 % (3816723)Instructions burned: 573 (million)
% 115.09/16.75 % (3816729)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:si=on:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2240442113:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2853 on theBenchmark for (2853ds/496Mi)
% 115.09/16.75 % (3816727)Instruction limit reached!
% 115.09/16.75 % (3816727)------------------------------
% 115.09/16.75 % (3816727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.09/16.75 % (3816727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.09/16.75 % (3816727)CaDiCaL version: 2.1.3
% 115.09/16.75 % (3816727)Termination reason: Instruction limit
% 115.09/16.75 % (3816727)Termination phase: Saturation
% 115.09/16.75 % (3816727)Time elapsed: 0.192 s
% 115.09/16.75 % (3816727)Peak memory usage: 94 MB
% 115.09/16.75 % (3816727)Instructions burned: 651 (million)
% 115.09/16.75 % (3816729)Instruction limit reached!
% 115.09/16.75 % (3816729)------------------------------
% 115.09/16.75 % (3816729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.09/16.75 % (3816729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.09/16.75 % (3816729)CaDiCaL version: 2.1.3
% 115.09/16.75 % (3816729)Termination reason: Instruction limit
% 115.09/16.75 % (3816729)Termination phase: Saturation
% 115.09/16.75 % (3816729)Time elapsed: 0.133 s
% 115.09/16.75 % (3816729)Peak memory usage: 93 MB
% 115.09/16.75 % (3816729)Instructions burned: 498 (million)
% 115.09/16.75 % (3816731)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=2835119978:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2851 on theBenchmark for (2851ds/588Mi)
% 118.30/17.16 % (3816731)Refutation not found, incomplete strategy
% 118.30/17.16 % (3816731)------------------------------
% 118.30/17.16 % (3816731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.30/17.16 % (3816731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.30/17.16 % (3816731)CaDiCaL version: 2.1.3
% 118.30/17.16 % (3816731)Termination reason: Refutation not found, incomplete strategy
% 118.30/17.16 % (3816731)Time elapsed: 0.003 s
% 118.30/17.16 % (3816731)Peak memory usage: 89 MB
% 118.30/17.16 % (3816731)Instructions burned: 8 (million)
% 118.30/17.16 % (3816732)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=435081781:i=4700:rtra=on_2851 on theBenchmark for (2851ds/4700Mi)
% 118.30/17.16 % (3816731)------------------------------
% 118.30/17.16 % (3816731)------------------------------
% 118.30/17.16 % Exception at run slice level
% 118.30/17.16 User error: GNN currently only supports monomorphic FOL.
% 118.30/17.16 % (3816735)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1226208929:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2848 on theBenchmark for (2848ds/226Mi)
% 118.30/17.16 % (3816735)Refutation not found, incomplete strategy
% 118.30/17.16 % (3816735)------------------------------
% 118.30/17.16 % (3816735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.30/17.16 % (3816735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.30/17.16 % (3816735)CaDiCaL version: 2.1.3
% 118.30/17.16 % (3816735)Termination reason: Refutation not found, incomplete strategy
% 118.30/17.16 % (3816735)Time elapsed: 0.004 s
% 118.30/17.16 % (3816735)Peak memory usage: 89 MB
% 118.30/17.16 % (3816735)Instructions burned: 12 (million)
% 118.30/17.16 % (3816736)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=17203129:i=254:av=off:fsr=off:rtra=on:sup=off_2848 on theBenchmark for (2848ds/254Mi)
% 118.30/17.16 % (3816736)Refutation not found, incomplete strategy
% 118.30/17.16 % (3816736)------------------------------
% 118.30/17.16 % (3816736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.30/17.16 % (3816736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.30/17.16 % (3816736)CaDiCaL version: 2.1.3
% 118.30/17.16 % (3816736)Termination reason: Refutation not found, incomplete strategy
% 118.30/17.16 % (3816736)Time elapsed: 0.003 s
% 118.30/17.16 % (3816736)Peak memory usage: 88 MB
% 118.30/17.16 % (3816736)Instructions burned: 8 (million)
% 118.30/17.16 % (3816735)------------------------------
% 118.30/17.16 % (3816735)------------------------------
% 118.30/17.16 % (3816736)------------------------------
% 118.30/17.16 % (3816736)------------------------------
% 118.30/17.16 % (3816739)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=1266602716:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2846 on theBenchmark for (2846ds/228Mi)
% 118.30/17.16 % (3816739)Refutation not found, incomplete strategy
% 118.30/17.16 % (3816739)------------------------------
% 118.30/17.16 % (3816739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.30/17.16 % (3816739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.30/17.16 % (3816739)CaDiCaL version: 2.1.3
% 118.30/17.16 % (3816739)Termination reason: Refutation not found, incomplete strategy
% 118.30/17.16 % (3816739)Time elapsed: 0.002 s
% 118.30/17.16 % (3816739)Peak memory usage: 89 MB
% 118.30/17.16 % (3816739)Instructions burned: 6 (million)
% 118.30/17.16 % (3816740)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=4054131140:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2845 on theBenchmark for (2845ds/1814Mi)
% 118.30/17.16 % (3816739)------------------------------
% 118.30/17.16 % (3816739)------------------------------
% 118.30/17.16 % (3816743)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=3601037029:i=874:sd=1:aac=none:rtra=on:ss=included_2843 on theBenchmark for (2843ds/874Mi)
% 118.30/17.16 % (3816743)Refutation not found, incomplete strategy
% 118.30/17.16 % (3816743)------------------------------
% 118.30/17.16 % (3816743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.30/17.16 % (3816743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.30/17.16 % (3816743)CaDiCaL version: 2.1.3
% 118.30/17.16 % (3816743)Termination reason: Refutation not found, incomplete strategy
% 118.30/17.16 % (3816743)Time elapsed: 0.005 s
% 118.30/17.16 % (3816743)Peak memory usage: 89 MB
% 118.30/17.16 % (3816743)Instructions burned: 13 (million)
% 118.30/17.16 % (3816743)------------------------------
% 120.07/17.43 % (3816743)------------------------------
% 120.07/17.43 % (3816673)Instruction limit reached!
% 120.07/17.43 % (3816673)------------------------------
% 120.07/17.43 % (3816673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.07/17.43 % (3816673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.07/17.43 % (3816673)CaDiCaL version: 2.1.3
% 120.07/17.43 % (3816673)Termination reason: Instruction limit
% 120.07/17.43 % (3816673)Termination phase: Saturation
% 120.07/17.43 % (3816673)Time elapsed: 6.340 s
% 120.07/17.43 % (3816673)Peak memory usage: 192 MB
% 120.07/17.43 % (3816673)Instructions burned: 21162 (million)
% 120.07/17.43 % (3816745)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=1674071077:i=10404:rtra=on:ss=axioms:sgt=16_2841 on theBenchmark for (2841ds/10404Mi)
% 120.07/17.43 % (3816746)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=516694766:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2840 on theBenchmark for (2840ds/268Mi)
% 120.07/17.43 % (3816740)Instruction limit reached!
% 120.07/17.43 % (3816740)------------------------------
% 120.07/17.43 % (3816740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.07/17.43 % (3816740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.07/17.43 % (3816740)CaDiCaL version: 2.1.3
% 120.07/17.43 % (3816740)Termination reason: Instruction limit
% 120.07/17.43 % (3816740)Termination phase: Saturation
% 120.07/17.43 % (3816740)Time elapsed: 0.527 s
% 120.07/17.43 % (3816740)Peak memory usage: 95 MB
% 120.07/17.43 % (3816740)Instructions burned: 1816 (million)
% 120.07/17.43 % (3816746)Instruction limit reached!
% 120.07/17.43 % (3816746)------------------------------
% 120.07/17.43 % (3816746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.07/17.43 % (3816746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.07/17.43 % (3816746)CaDiCaL version: 2.1.3
% 120.07/17.43 % (3816746)Termination reason: Instruction limit
% 120.07/17.43 % (3816746)Termination phase: Saturation
% 120.07/17.43 % (3816746)Time elapsed: 0.070 s
% 120.07/17.43 % (3816746)Peak memory usage: 90 MB
% 120.07/17.43 % (3816746)Instructions burned: 270 (million)
% 120.07/17.43 % Exception at run slice level
% 120.07/17.43 User error: GNN currently only supports monomorphic FOL.
% 120.07/17.43 % (3816749)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=3710223783:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2839 on theBenchmark for (2839ds/1184Mi)
% 120.07/17.43 % (3816749)Refutation not found, incomplete strategy
% 120.07/17.43 % (3816749)------------------------------
% 120.07/17.43 % (3816749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.07/17.43 % (3816749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.07/17.43 % (3816749)CaDiCaL version: 2.1.3
% 120.07/17.43 % (3816749)Termination reason: Refutation not found, incomplete strategy
% 120.07/17.43 % (3816749)Time elapsed: 0.004 s
% 120.07/17.43 % (3816749)Peak memory usage: 88 MB
% 120.07/17.43 % (3816749)Instructions burned: 11 (million)
% 120.07/17.43 % (3816750)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=4207350570:st=3:i=26386:sd=3:rtra=on:ss=axioms_2838 on theBenchmark for (2838ds/26386Mi)
% 120.07/17.43 % (3816752)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:si=on:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2699273998:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2838 on theBenchmark for (2838ds/250Mi)
% 120.07/17.43 % (3816752)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 120.07/17.43 % (3816749)------------------------------
% 120.07/17.43 % (3816749)------------------------------
% 120.07/17.43 % (3816752)Instruction limit reached!
% 120.07/17.43 % (3816752)------------------------------
% 120.07/17.43 % (3816752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.07/17.43 % (3816752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.07/17.43 % (3816752)CaDiCaL version: 2.1.3
% 120.07/17.43 % (3816752)Termination reason: Instruction limit
% 120.07/17.43 % (3816752)Termination phase: Saturation
% 120.07/17.43 % (3816752)Time elapsed: 0.090 s
% 120.07/17.43 % (3816752)Peak memory usage: 91 MB
% 120.07/17.43 % (3816752)Instructions burned: 252 (million)
% 120.07/17.43 % Exception at run slice level
% 120.07/17.43 User error: GNN currently only supports monomorphic FOL.
% 120.07/17.43 % (3816755)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=206341650:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2836 on theBenchmark for (2836ds/268Mi)
% 120.07/17.43 % Exception at run slice level
% 120.07/17.43 User error: Immediate (shared) subterms of term/literal aa(X0,fun(X2,X1),X5,X4) = sF21(X0,X2,X1,X5,X4) have different types/not well-typed!
% 120.07/17.43 % (3816756)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1045057088:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2836 on theBenchmark for (2836ds/282Mi)
% 120.07/17.43 % (3816756)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 120.07/17.43 % (3816756)Refutation not found, incomplete strategy
% 120.07/17.43 % (3816756)------------------------------
% 120.07/17.43 % (3816756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.07/17.43 % (3816756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.07/17.43 % (3816756)CaDiCaL version: 2.1.3
% 120.07/17.43 % (3816756)Termination reason: Refutation not found, incomplete strategy
% 120.07/17.43 % (3816756)Time elapsed: 0.001 s
% 120.07/17.43 % (3816756)Peak memory usage: 88 MB
% 120.07/17.43 % (3816756)Instructions burned: 1 (million)
% 120.07/17.43 % (3816757)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=86542596:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2835 on theBenchmark for (2835ds/862Mi)
% 120.07/17.43 % (3816757)Refutation not found, incomplete strategy
% 120.07/17.43 % (3816757)------------------------------
% 120.07/17.43 % (3816757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.07/17.43 % (3816757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.07/17.43 % (3816757)CaDiCaL version: 2.1.3
% 120.07/17.43 % (3816757)Termination reason: Refutation not found, incomplete strategy
% 120.07/17.43 % (3816757)Time elapsed: 0.002 s
% 120.07/17.43 % (3816757)Peak memory usage: 89 MB
% 120.07/17.43 % (3816757)Instructions burned: 4 (million)
% 120.07/17.43 % (3816759)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:si=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=914396361:i=12120:aac=none:ins=25:rtra=on_2835 on theBenchmark for (2835ds/12120Mi)
% 120.07/17.43 % (3816756)------------------------------
% 120.07/17.43 % (3816756)------------------------------
% 120.07/17.43 % (3816757)------------------------------
% 120.07/17.43 % (3816757)------------------------------
% 120.07/17.43 % (3816763)lrs+10_16_anc=all:slsqr=32,1:sil=8000:si=on: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=4196041367:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2833 on theBenchmark for (2833ds/300Mi)
% 120.07/17.43 % (3816763)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 120.07/17.43 % Exception at run slice level
% 120.07/17.43 User error: GNN currently only supports monomorphic FOL.
% 120.07/17.43 % (3816764)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=1131075022:i=28310:bd=all:rtra=on_2833 on theBenchmark for (2833ds/28310Mi)
% 120.07/17.43 % (3816763)Instruction limit reached!
% 120.07/17.43 % (3816763)------------------------------
% 120.07/17.43 % (3816763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.07/17.43 % (3816763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.07/17.43 % (3816763)CaDiCaL version: 2.1.3
% 120.07/17.43 % (3816763)Termination reason: Instruction limit
% 120.07/17.43 % (3816763)Termination phase: Saturation
% 120.07/17.43 % (3816763)Time elapsed: 0.098 s
% 120.07/17.43 % (3816763)Peak memory usage: 92 MB
% 120.07/17.43 % (3816763)Instructions burned: 300 (million)
% 120.07/17.43 % (3816766)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3232974835:i=1334:av=off:fsr=off:rtra=on_2832 on theBenchmark for (2832ds/1334Mi)
% 120.07/17.43 % (3816766)Refutation not found, incomplete strategy
% 120.07/17.43 % (3816766)------------------------------
% 120.07/17.43 % (3816766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.07/17.43 % (3816766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.07/17.43 % (3816766)CaDiCaL version: 2.1.3
% 120.07/17.43 % (3816766)Termination reason: Refutation not found, incomplete strategy
% 120.07/17.43 % (3816766)Time elapsed: 0.004 s
% 120.07/17.43 % (3816766)Peak memory usage: 89 MB
% 120.07/17.43 % (3816766)Instructions burned: 10 (million)
% 120.07/17.43 % (3816768)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:si=on:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3818884854:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2831 on theBenchmark for (2831ds/370Mi)
% 120.07/17.43 % (3816692)First to succeed.
% 120.07/17.43 % (3816692)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3816390"
% 120.07/17.43 % Exception at run slice level
% 120.07/17.43 User error: GNN currently only supports monomorphic FOL.
% 120.07/17.43 % (3816766)------------------------------
% 120.07/17.43 % (3816766)------------------------------
% 120.07/17.43 % (3816768)Instruction limit reached!
% 120.07/17.43 % (3816768)------------------------------
% 120.07/17.43 % (3816768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.07/17.43 % (3816768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.07/17.43 % (3816768)CaDiCaL version: 2.1.3
% 120.07/17.43 % (3816768)Termination reason: Instruction limit
% 120.07/17.43 % (3816768)Termination phase: Saturation
% 120.07/17.43 % (3816768)Time elapsed: 0.110 s
% 120.07/17.43 % (3816768)Peak memory usage: 93 MB
% 120.07/17.43 % (3816768)Instructions burned: 370 (million)
% 120.07/17.43 % (3816771)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=4151616951:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2830 on theBenchmark for (2830ds/386Mi)
% 120.07/17.43 % (3816772)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=2613911868:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2830 on theBenchmark for (2830ds/9700Mi)
% 120.07/17.43 % (3816773)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:si=on:sp=const_frequency:acc=on:urr=on:random_seed=3142504077:i=24222:sd=1:rtra=on:ss=included_2829 on theBenchmark for (2829ds/24222Mi)
% 120.07/17.43 % (3816772)Refutation not found, incomplete strategy
% 120.07/17.43 % (3816772)------------------------------
% 120.07/17.43 % (3816772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.07/17.43 % (3816772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.07/17.43 % (3816772)CaDiCaL version: 2.1.3
% 120.07/17.43 % (3816772)Termination reason: Refutation not found, incomplete strategy
% 120.07/17.43 % (3816772)Time elapsed: 0.003 s
% 120.07/17.43 % (3816772)Peak memory usage: 88 MB
% 120.07/17.43 % (3816772)Instructions burned: 9 (million)
% 120.07/17.43 % (3816692)Refutation found. Thanks to Tanya!
% 120.07/17.43 % SZS status Theorem for theBenchmark
% 120.07/17.43 % SZS output start Proof for theBenchmark
% See solution above
% 120.66/17.52 % (3816692)------------------------------
% 120.66/17.52 % (3816692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.66/17.52 % (3816692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.66/17.52 % (3816692)CaDiCaL version: 2.1.3
% 120.66/17.52 % (3816692)Termination reason: Refutation
% 120.66/17.52 % (3816692)Time elapsed: 4.485 s
% 120.66/17.52 % (3816692)Peak memory usage: 186 MB
% 120.66/17.52 % (3816692)Instructions burned: 15179 (million)
% 120.66/17.52 % (3816692)------------------------------
% 120.66/17.52 % (3816692)------------------------------
% 120.66/17.52 % (3816390)Success in time 17.116 s
% 120.66/17.52 % Vampire exiting
%------------------------------------------------------------------------------