%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW487_5 : TPTP v9.3.1. Released v6.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:30:40 PM UTC 2026
% Result : Theorem 169.82s 24.67s
% Output : Refutation 171.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 15
% Syntax : Number of formulae : 81 ( 48 unt; 0 typ; 0 def)
% Number of atoms : 135 ( 71 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 112 ( 58 ~; 38 |; 6 &)
% ( 2 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 15 ( 2 avg)
% Number of FOOLs : 1 ( 1 fml; 0 var)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 25 ( 23 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 3 con; 0-5 aty)
% Number of variables : 190 ( 190 !; 0 ?; 190 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
a: $tType ).
tff(type_def_6,type,
bool: $tType ).
tff(type_def_7,type,
nat: $tType ).
tff(type_def_8,type,
poly: $tType > $tType ).
tff(type_def_9,type,
fun: ( $tType * $tType ) > $tType ).
tff(func_def_0,type,
combb:
!>[X0: $tType,X1: $tType,X2: $tType] : fun(fun(X0,X1),fun(fun(X2,X0),fun(X2,X1))) ).
tff(func_def_1,type,
combc:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( fun(X0,fun(X1,X2)) * X1 ) > fun(X0,X2) ) ).
tff(func_def_2,type,
combk:
!>[X0: $tType,X1: $tType] : fun(X0,fun(X1,X0)) ).
tff(func_def_3,type,
combs:
!>[X0: $tType,X1: $tType,X2: $tType] : ( fun(X0,fun(X1,X2)) > fun(fun(X0,X1),fun(X0,X2)) ) ).
tff(func_def_4,type,
fundam296178794t_poly:
!>[X0: $tType] : ( ( poly(X0) * X0 ) > poly(X0) ) ).
tff(func_def_5,type,
plus_plus:
!>[X0: $tType] : fun(X0,fun(X0,X0)) ).
tff(func_def_6,type,
times_times:
!>[X0: $tType] : ( X0 > fun(X0,X0) ) ).
tff(func_def_7,type,
zero_zero:
!>[X0: $tType] : X0 ).
tff(func_def_8,type,
if:
!>[X0: $tType] : ( ( bool * X0 * X0 ) > X0 ) ).
tff(func_def_9,type,
abs_poly:
!>[X0: $tType] : ( fun(nat,X0) > poly(X0) ) ).
tff(func_def_10,type,
coeff:
!>[X0: $tType] : ( poly(X0) > fun(nat,X0) ) ).
tff(func_def_11,type,
order:
!>[X0: $tType] : ( ( X0 * poly(X0) ) > nat ) ).
tff(func_def_12,type,
pCons:
!>[X0: $tType] : fun(X0,fun(poly(X0),poly(X0))) ).
tff(func_def_13,type,
pcompose:
!>[X0: $tType] : ( ( poly(X0) * poly(X0) ) > poly(X0) ) ).
tff(func_def_14,type,
poly1:
!>[X0: $tType] : ( poly(X0) > fun(X0,X0) ) ).
tff(func_def_15,type,
poly_rec:
!>[X0: $tType,X1: $tType] : ( ( X0 * fun(X1,fun(poly(X1),fun(X0,X0))) * poly(X1) ) > X0 ) ).
tff(func_def_16,type,
smult:
!>[X0: $tType] : fun(X0,fun(poly(X0),poly(X0))) ).
tff(func_def_17,type,
synthetic_div:
!>[X0: $tType] : ( ( poly(X0) * X0 ) > poly(X0) ) ).
tff(func_def_18,type,
aa:
!>[X0: $tType,X1: $tType] : ( ( fun(X0,X1) * X0 ) > X1 ) ).
tff(func_def_19,type,
fFalse: bool ).
tff(func_def_20,type,
fTrue: bool ).
tff(func_def_21,type,
fequal:
!>[X0: $tType] : ( ( X0 * X0 ) > bool ) ).
tff(func_def_22,type,
h: a ).
tff(func_def_23,type,
sK0:
!>[X0: $tType] : ( fun(poly(X0),bool) > X0 ) ).
tff(func_def_24,type,
sK1:
!>[X0: $tType] : ( fun(poly(X0),bool) > poly(X0) ) ).
tff(func_def_25,type,
sK2:
!>[X0: $tType] : ( poly(X0) > X0 ) ).
tff(func_def_26,type,
sK3:
!>[X0: $tType] : ( poly(X0) > poly(X0) ) ).
tff(func_def_27,type,
sK4:
!>[X0: $tType,X1: $tType] : ( ( fun(X1,X0) * fun(X1,X0) ) > X1 ) ).
tff(pred_def_1,type,
cancel1352612707id_add:
!>[X0: $tType] : $o ).
tff(pred_def_2,type,
linordered_idom:
!>[X0: $tType] : $o ).
tff(pred_def_3,type,
idom:
!>[X0: $tType] : $o ).
tff(pred_def_4,type,
zero:
!>[X0: $tType] : $o ).
tff(pred_def_5,type,
semiring:
!>[X0: $tType] : $o ).
tff(pred_def_6,type,
ring_char_0:
!>[X0: $tType] : $o ).
tff(pred_def_7,type,
mult_zero:
!>[X0: $tType] : $o ).
tff(pred_def_8,type,
monoid_add:
!>[X0: $tType] : $o ).
tff(pred_def_9,type,
comm_semiring:
!>[X0: $tType] : $o ).
tff(pred_def_10,type,
comm_semiring_0:
!>[X0: $tType] : $o ).
tff(pred_def_11,type,
comm_semiring_1:
!>[X0: $tType] : $o ).
tff(pred_def_12,type,
comm_monoid_add:
!>[X0: $tType] : $o ).
tff(pred_def_13,type,
no_zero_divisors:
!>[X0: $tType] : $o ).
tff(pred_def_14,type,
ab_semigroup_add:
!>[X0: $tType] : $o ).
tff(pred_def_15,type,
ab_semigroup_mult:
!>[X0: $tType] : $o ).
tff(pred_def_16,type,
cancel_semigroup_add:
!>[X0: $tType] : $o ).
tff(pred_def_17,type,
ring_n68954251visors:
!>[X0: $tType] : $o ).
tff(pred_def_18,type,
linord581940658strict:
!>[X0: $tType] : $o ).
tff(pred_def_19,type,
cancel146912293up_add:
!>[X0: $tType] : $o ).
tff(pred_def_20,type,
linord219039673up_add:
!>[X0: $tType] : $o ).
tff(pred_def_21,type,
ab_sem1668676832m_mult:
!>[X0: $tType] : $o ).
tff(pred_def_22,type,
semiri456707255roduct:
!>[X0: $tType] : $o ).
tff(pred_def_23,type,
pp: bool > $o ).
tff(f6,axiom,
! [X0: $tType] :
( zero(X0)
=> ! [X1: poly(X0),X2: X0] :
( ( aa(poly(X0),poly(X0),aa(X0,fun(poly(X0),poly(X0)),pCons(X0),X2),X1) = zero_zero(poly(X0)) )
<=> ( ( X2 = zero_zero(X0) )
& ( X1 = zero_zero(poly(X0)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_pCons__eq__0__iff) ).
tff(f7,axiom,
! [X0: $tType] :
( comm_semiring_0(X0)
=> ! [X1: X0] : ( aa(poly(X0),poly(X0),aa(X0,fun(poly(X0),poly(X0)),smult(X0),X1),zero_zero(poly(X0))) = zero_zero(poly(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_6_smult__0__right) ).
tff(f12,axiom,
! [X0: $tType,X1: $tType] :
( zero(X0)
=> ! [X2: X1,X3: fun(X0,fun(poly(X0),fun(X1,X1)))] :
( ( aa(X1,X1,aa(poly(X0),fun(X1,X1),aa(X0,fun(poly(X0),fun(X1,X1)),X3,zero_zero(X0)),zero_zero(poly(X0))),X2) = X2 )
=> ( poly_rec(X1,X0,X2,X3,zero_zero(poly(X0))) = X2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_11_poly__rec__0) ).
tff(f24,axiom,
! [X0: $tType] :
( monoid_add(X0)
=> ! [X1: X0] : ( aa(X0,X0,aa(X0,fun(X0,X0),plus_plus(X0),zero_zero(X0)),X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_23_add__0__left) ).
tff(f104,axiom,
! [X0: $tType] :
( comm_semiring_0(X0)
=> monoid_add(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clar_Rings_Ocomm__semiring__0__Groups_Omonoid__add) ).
tff(f107,axiom,
! [X0: $tType] :
( comm_semiring_0(X0)
=> zero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clar_Rings_Ocomm__semiring__0__Groups_Ozero) ).
tff(f136,axiom,
! [X0: $tType] :
( comm_semiring_0(X0)
=> comm_semiring_0(poly(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Polynomial_Opoly___Rings_Ocomm__semiring__0) ).
tff(f149,axiom,
! [X0: $tType,X1: $tType,X2: $tType,X3: X2,X4: fun(X2,X1),X5: fun(X1,X0)] : ( aa(X2,X0,aa(fun(X2,X1),fun(X2,X0),aa(fun(X1,X0),fun(fun(X2,X1),fun(X2,X0)),combb(X1,X0,X2),X5),X4),X3) = aa(X1,X0,X5,aa(X2,X1,X4,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_COMBB_1_1_U) ).
tff(f150,axiom,
! [X0: $tType,X1: $tType,X2: $tType,X3: X0,X4: X2,X5: fun(X0,fun(X2,X1))] : ( aa(X0,X1,combc(X0,X2,X1,X5,X4),X3) = aa(X2,X1,aa(X0,fun(X2,X1),X5,X3),X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_COMBC_1_1_U) ).
tff(f151,axiom,
! [X0: $tType,X1: $tType,X2: X0,X3: X1] : ( aa(X0,X1,aa(X1,fun(X0,X1),combk(X1,X0),X3),X2) = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_COMBK_1_1_U) ).
tff(f152,axiom,
! [X0: $tType,X1: $tType,X2: $tType,X3: X2,X4: fun(X2,X1),X5: fun(X2,fun(X1,X0))] : ( aa(X2,X0,aa(fun(X2,X1),fun(X2,X0),combs(X2,X1,X0,X5),X4),X3) = aa(X1,X0,aa(X2,fun(X1,X0),X5,X3),aa(X2,X1,X4,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_COMBS_1_1_U) ).
tff(f153,axiom,
! [X0: $tType,X1: X0,X2: X0] :
( ~ pp(fequal(X0,X2,X1))
| ( X2 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fequal_1_1_T) ).
tff(f154,axiom,
! [X0: $tType,X1: X0,X2: X0] :
( ( X2 != X1 )
| pp(fequal(X0,X2,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fequal_2_1_T) ).
tff(f155,conjecture,
poly_rec(poly(a),a,zero_zero(poly(a)),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),fun(poly(a),poly(a)))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),fun(poly(a),poly(a))))),combb(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),a),combk(fun(poly(a),poly(a)),poly(a))),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),poly(a))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a)))),combb(fun(poly(a),poly(a)),fun(poly(a),poly(a)),a),combs(poly(a),poly(a),poly(a),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),aa(fun(poly(a),fun(poly(a),poly(a))),fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),combb(poly(a),fun(poly(a),poly(a)),poly(a)),plus_plus(poly(a))),aa(a,fun(poly(a),poly(a)),smult(a),h)))),pCons(a))),zero_zero(poly(a))) = zero_zero(poly(a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
tff(f156,negated_conjecture,
( ( ~ poly_rec(poly(a),a,zero_zero(poly(a)),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),fun(poly(a),poly(a)))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),fun(poly(a),poly(a))))),combb(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),a),combk(fun(poly(a),poly(a)),poly(a))),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),poly(a))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a)))),combb(fun(poly(a),poly(a)),fun(poly(a),poly(a)),a),combs(poly(a),poly(a),poly(a),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),aa(fun(poly(a),fun(poly(a),poly(a))),fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),combb(poly(a),fun(poly(a),poly(a)),poly(a)),plus_plus(poly(a))),aa(a,fun(poly(a),poly(a)),smult(a),h)))),pCons(a))),zero_zero(poly(a))) ) = zero_zero(poly(a)) ),
inference(negated_conjecture,[status(cth)],[f155]) ).
tff(f157,axiom,
comm_semiring_0(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tfree_0) ).
tff(f159,plain,
zero_zero(poly(a)) != poly_rec(poly(a),a,zero_zero(poly(a)),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),fun(poly(a),poly(a)))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),fun(poly(a),poly(a))))),combb(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),a),combk(fun(poly(a),poly(a)),poly(a))),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),poly(a))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a)))),combb(fun(poly(a),poly(a)),fun(poly(a),poly(a)),a),combs(poly(a),poly(a),poly(a),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),aa(fun(poly(a),fun(poly(a),poly(a))),fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),combb(poly(a),fun(poly(a),poly(a)),poly(a)),plus_plus(poly(a))),aa(a,fun(poly(a),poly(a)),smult(a),h)))),pCons(a))),zero_zero(poly(a))),
inference(flattening,[],[f156]) ).
tff(f168,plain,
! [X0: $tType] :
( ! [X1: poly(X0),X2: X0] :
( ( aa(poly(X0),poly(X0),aa(X0,fun(poly(X0),poly(X0)),pCons(X0),X2),X1) = zero_zero(poly(X0)) )
<=> ( ( X2 = zero_zero(X0) )
& ( X1 = zero_zero(poly(X0)) ) ) )
| ~ zero(X0) ),
inference(ennf_transformation,[],[f6]) ).
tff(f169,plain,
! [X0: $tType] :
( ! [X1: X0] : ( aa(poly(X0),poly(X0),aa(X0,fun(poly(X0),poly(X0)),smult(X0),X1),zero_zero(poly(X0))) = zero_zero(poly(X0)) )
| ~ comm_semiring_0(X0) ),
inference(ennf_transformation,[],[f7]) ).
tff(f174,plain,
! [X0: $tType,X1: $tType] :
( ! [X2: X1,X3: fun(X0,fun(poly(X0),fun(X1,X1)))] :
( ( poly_rec(X1,X0,X2,X3,zero_zero(poly(X0))) = X2 )
| ( aa(X1,X1,aa(poly(X0),fun(X1,X1),aa(X0,fun(poly(X0),fun(X1,X1)),X3,zero_zero(X0)),zero_zero(poly(X0))),X2) != X2 ) )
| ~ zero(X0) ),
inference(ennf_transformation,[],[f12]) ).
tff(f186,plain,
! [X0: $tType] :
( ! [X1: X0] : ( aa(X0,X0,aa(X0,fun(X0,X0),plus_plus(X0),zero_zero(X0)),X1) = X1 )
| ~ monoid_add(X0) ),
inference(ennf_transformation,[],[f24]) ).
tff(f269,plain,
! [X0: $tType] :
( monoid_add(X0)
| ~ comm_semiring_0(X0) ),
inference(ennf_transformation,[],[f104]) ).
tff(f272,plain,
! [X0: $tType] :
( zero(X0)
| ~ comm_semiring_0(X0) ),
inference(ennf_transformation,[],[f107]) ).
tff(f286,plain,
! [X0: $tType] :
( comm_semiring_0(poly(X0))
| ~ comm_semiring_0(X0) ),
inference(ennf_transformation,[],[f136]) ).
tff(f296,plain,
! [X0: $tType] :
( ! [X1: poly(X0),X2: X0] :
( ( ( aa(poly(X0),poly(X0),aa(X0,fun(poly(X0),poly(X0)),pCons(X0),X2),X1) = zero_zero(poly(X0)) )
| ( zero_zero(X0) != X2 )
| ( zero_zero(poly(X0)) != X1 ) )
& ( ( ( X2 = zero_zero(X0) )
& ( X1 = zero_zero(poly(X0)) ) )
| ( aa(poly(X0),poly(X0),aa(X0,fun(poly(X0),poly(X0)),pCons(X0),X2),X1) != zero_zero(poly(X0)) ) ) )
| ~ zero(X0) ),
inference(nnf_transformation,[],[f168]) ).
tff(f297,plain,
! [X0: $tType] :
( ! [X1: poly(X0),X2: X0] :
( ( ( aa(poly(X0),poly(X0),aa(X0,fun(poly(X0),poly(X0)),pCons(X0),X2),X1) = zero_zero(poly(X0)) )
| ( zero_zero(X0) != X2 )
| ( zero_zero(poly(X0)) != X1 ) )
& ( ( ( X2 = zero_zero(X0) )
& ( X1 = zero_zero(poly(X0)) ) )
| ( aa(poly(X0),poly(X0),aa(X0,fun(poly(X0),poly(X0)),pCons(X0),X2),X1) != zero_zero(poly(X0)) ) ) )
| ~ zero(X0) ),
inference(flattening,[],[f296]) ).
tff(f330,plain,
! [X0: $tType,X2: X0,X1: poly(X0)] :
( ( aa(poly(X0),poly(X0),aa(X0,fun(poly(X0),poly(X0)),pCons(X0),X2),X1) = zero_zero(poly(X0)) )
| ( zero_zero(X0) != X2 )
| ( zero_zero(poly(X0)) != X1 )
| ~ zero(X0) ),
inference(cnf_transformation,[],[f297]) ).
tff(f331,plain,
! [X0: $tType,X1: X0] :
( ( zero_zero(poly(X0)) = aa(poly(X0),poly(X0),aa(X0,fun(poly(X0),poly(X0)),smult(X0),X1),zero_zero(poly(X0))) )
| ~ comm_semiring_0(X0) ),
inference(cnf_transformation,[],[f169]) ).
tff(f338,plain,
! [X1: $tType,X0: $tType,X2: X1,X3: fun(X0,fun(poly(X0),fun(X1,X1)))] :
( ( poly_rec(X1,X0,X2,X3,zero_zero(poly(X0))) = X2 )
| ( aa(X1,X1,aa(poly(X0),fun(X1,X1),aa(X0,fun(poly(X0),fun(X1,X1)),X3,zero_zero(X0)),zero_zero(poly(X0))),X2) != X2 )
| ~ zero(X0) ),
inference(cnf_transformation,[],[f174]) ).
tff(f355,plain,
! [X0: $tType,X1: X0] :
( ( aa(X0,X0,aa(X0,fun(X0,X0),plus_plus(X0),zero_zero(X0)),X1) = X1 )
| ~ monoid_add(X0) ),
inference(cnf_transformation,[],[f186]) ).
tff(f447,plain,
! [X0: $tType] :
( ~ comm_semiring_0(X0)
| monoid_add(X0) ),
inference(cnf_transformation,[],[f269]) ).
tff(f450,plain,
! [X0: $tType] :
( ~ comm_semiring_0(X0)
| zero(X0) ),
inference(cnf_transformation,[],[f272]) ).
tff(f479,plain,
! [X0: $tType] :
( comm_semiring_0(poly(X0))
| ~ comm_semiring_0(X0) ),
inference(cnf_transformation,[],[f286]) ).
tff(f492,plain,
! [X1: $tType,X0: $tType,X2: $tType,X3: X2,X4: fun(X2,X1),X5: fun(X1,X0)] : ( aa(X2,X0,aa(fun(X2,X1),fun(X2,X0),aa(fun(X1,X0),fun(fun(X2,X1),fun(X2,X0)),combb(X1,X0,X2),X5),X4),X3) = aa(X1,X0,X5,aa(X2,X1,X4,X3)) ),
inference(cnf_transformation,[],[f149]) ).
tff(f493,plain,
! [X1: $tType,X0: $tType,X2: $tType,X3: X0,X4: X2,X5: fun(X0,fun(X2,X1))] : ( aa(X0,X1,combc(X0,X2,X1,X5,X4),X3) = aa(X2,X1,aa(X0,fun(X2,X1),X5,X3),X4) ),
inference(cnf_transformation,[],[f150]) ).
tff(f494,plain,
! [X1: $tType,X0: $tType,X2: X0,X3: X1] : ( aa(X0,X1,aa(X1,fun(X0,X1),combk(X1,X0),X3),X2) = X3 ),
inference(cnf_transformation,[],[f151]) ).
tff(f495,plain,
! [X1: $tType,X0: $tType,X2: $tType,X3: X2,X4: fun(X2,X1),X5: fun(X2,fun(X1,X0))] : ( aa(X2,X0,aa(fun(X2,X1),fun(X2,X0),combs(X2,X1,X0,X5),X4),X3) = aa(X1,X0,aa(X2,fun(X1,X0),X5,X3),aa(X2,X1,X4,X3)) ),
inference(cnf_transformation,[],[f152]) ).
tff(f496,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ~ pp(fequal(X0,X2,X1))
| ( X1 = X2 ) ),
inference(cnf_transformation,[],[f153]) ).
tff(f497,plain,
! [X0: $tType,X2: X0,X1: X0] :
( ( X1 != X2 )
| pp(fequal(X0,X2,X1)) ),
inference(cnf_transformation,[],[f154]) ).
tff(f498,plain,
zero_zero(poly(a)) != poly_rec(poly(a),a,zero_zero(poly(a)),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),fun(poly(a),poly(a)))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),fun(poly(a),poly(a))))),combb(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),a),combk(fun(poly(a),poly(a)),poly(a))),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),poly(a))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a)))),combb(fun(poly(a),poly(a)),fun(poly(a),poly(a)),a),combs(poly(a),poly(a),poly(a),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),aa(fun(poly(a),fun(poly(a),poly(a))),fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),combb(poly(a),fun(poly(a),poly(a)),poly(a)),plus_plus(poly(a))),aa(a,fun(poly(a),poly(a)),smult(a),h)))),pCons(a))),zero_zero(poly(a))),
inference(cnf_transformation,[],[f159]) ).
tff(f499,plain,
comm_semiring_0(a),
inference(cnf_transformation,[],[f157]) ).
tff(f502,plain,
! [X0: $tType,X1: poly(X0)] :
( ( zero_zero(poly(X0)) = aa(poly(X0),poly(X0),aa(X0,fun(poly(X0),poly(X0)),pCons(X0),zero_zero(X0)),X1) )
| ( zero_zero(poly(X0)) != X1 )
| ~ zero(X0) ),
inference(equality_resolution,[],[f330]) ).
tff(f503,plain,
! [X0: $tType] :
( ( zero_zero(poly(X0)) = aa(poly(X0),poly(X0),aa(X0,fun(poly(X0),poly(X0)),pCons(X0),zero_zero(X0)),zero_zero(poly(X0))) )
| ~ zero(X0) ),
inference(equality_resolution,[],[f502]) ).
tff(f525,plain,
! [X0: $tType,X2: X0] : pp(fequal(X0,X2,X2)),
inference(equality_resolution,[],[f497]) ).
tff(f573,plain,
! [X0: $tType,X1: X0] :
( ~ monoid_add(X0)
| ( aa(X0,X0,combc(X0,X0,X0,plus_plus(X0),X1),zero_zero(X0)) = X1 ) ),
inference(forward_demodulation,[],[f355,f493]) ).
tff(f585,plain,
! [X1: $tType,X0: $tType,X2: X1,X3: fun(X0,fun(poly(X0),fun(X1,X1)))] :
( ( aa(X1,X1,aa(X0,fun(X1,X1),combc(X0,poly(X0),fun(X1,X1),X3,zero_zero(poly(X0))),zero_zero(X0)),X2) != X2 )
| ( poly_rec(X1,X0,X2,X3,zero_zero(poly(X0))) = X2 )
| ~ zero(X0) ),
inference(forward_demodulation,[],[f338,f493]) ).
tff(f592,plain,
! [X0: $tType,X1: X0] :
( ~ comm_semiring_0(X0)
| ( zero_zero(poly(X0)) = aa(X0,poly(X0),combc(X0,poly(X0),poly(X0),smult(X0),zero_zero(poly(X0))),X1) ) ),
inference(forward_demodulation,[],[f331,f493]) ).
tff(f595,plain,
! [X0: $tType] :
( ~ zero(X0)
| ( zero_zero(poly(X0)) = aa(X0,poly(X0),combc(X0,poly(X0),poly(X0),pCons(X0),zero_zero(poly(X0))),zero_zero(X0)) ) ),
inference(forward_demodulation,[],[f503,f493]) ).
tff(f698,plain,
zero(a),
inference(unit_resulting_resolution,[],[f450,f499]) ).
tff(f719,plain,
comm_semiring_0(poly(a)),
inference(unit_resulting_resolution,[],[f479,f499]) ).
tff(f725,plain,
monoid_add(poly(a)),
inference(unit_resulting_resolution,[],[f447,f719]) ).
tff(f867,plain,
! [X0: poly(a)] : ( aa(poly(a),poly(a),combc(poly(a),poly(a),poly(a),plus_plus(poly(a)),X0),zero_zero(poly(a))) = X0 ),
inference(unit_resulting_resolution,[],[f573,f725]) ).
tff(f989,plain,
! [X1: $tType,X3: $tType,X2: $tType,X0: fun(X3,X2),X4: X3,X5: X1] : ( aa(X1,X2,combc(X1,X3,X2,aa(fun(X3,X2),fun(X1,fun(X3,X2)),combk(fun(X3,X2),X1),X0),X4),X5) = aa(X3,X2,X0,X4) ),
inference(superposition,[],[f493,f494]) ).
tff(f991,plain,
! [X1: $tType,X0: $tType,X3: $tType,X2: $tType,X6: X0,X7: X1,X4: fun(X3,fun(X0,fun(X1,X2))),X5: X3] : ( aa(X3,X2,combc(X3,X1,X2,combc(X3,X0,fun(X1,X2),X4,X6),X7),X5) = aa(X1,X2,aa(X0,fun(X1,X2),aa(X3,fun(X0,fun(X1,X2)),X4,X5),X6),X7) ),
inference(superposition,[],[f493,f493]) ).
tff(f1013,plain,
! [X0: a] : ( zero_zero(poly(a)) = aa(a,poly(a),combc(a,poly(a),poly(a),smult(a),zero_zero(poly(a))),X0) ),
inference(unit_resulting_resolution,[],[f592,f499]) ).
tff(f1052,plain,
zero_zero(poly(a)) = aa(a,poly(a),combc(a,poly(a),poly(a),pCons(a),zero_zero(poly(a))),zero_zero(a)),
inference(unit_resulting_resolution,[],[f595,f698]) ).
tff(f1234,plain,
! [X1: $tType,X3: $tType,X2: $tType,X0: fun(X3,X2),X4: fun(X1,X3),X5: X1] : ( aa(X1,X2,aa(fun(X1,X3),fun(X1,X2),combs(X1,X3,X2,aa(fun(X3,X2),fun(X1,fun(X3,X2)),combk(fun(X3,X2),X1),X0)),X4),X5) = aa(X3,X2,X0,aa(X1,X3,X4,X5)) ),
inference(superposition,[],[f495,f494]) ).
tff(f1241,plain,
! [X6: $tType,X1: $tType,X0: $tType,X2: $tType,X3: fun(X0,fun(X2,X1)),X7: fun(X2,fun(X1,X6)),X4: X2,X5: X0] : ( aa(X2,X6,aa(fun(X2,X1),fun(X2,X6),combs(X2,X1,X6,X7),aa(X0,fun(X2,X1),X3,X5)),X4) = aa(X1,X6,aa(X2,fun(X1,X6),X7,X4),aa(X0,X1,combc(X0,X2,X1,X3,X4),X5)) ),
inference(superposition,[],[f495,f493]) ).
tff(f1277,plain,
zero_zero(poly(a)) != aa(poly(a),poly(a),aa(a,fun(poly(a),poly(a)),combc(a,poly(a),fun(poly(a),poly(a)),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),fun(poly(a),poly(a)))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),fun(poly(a),poly(a))))),combb(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),a),combk(fun(poly(a),poly(a)),poly(a))),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),poly(a))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a)))),combb(fun(poly(a),poly(a)),fun(poly(a),poly(a)),a),combs(poly(a),poly(a),poly(a),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),aa(fun(poly(a),fun(poly(a),poly(a))),fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),combb(poly(a),fun(poly(a),poly(a)),poly(a)),plus_plus(poly(a))),aa(a,fun(poly(a),poly(a)),smult(a),h)))),pCons(a))),zero_zero(poly(a))),zero_zero(a)),zero_zero(poly(a))),
inference(unit_resulting_resolution,[],[f585,f698,f498]) ).
tff(f1283,plain,
zero_zero(poly(a)) != aa(a,poly(a),combc(a,poly(a),poly(a),combc(a,poly(a),fun(poly(a),poly(a)),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),fun(poly(a),poly(a)))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),fun(poly(a),poly(a))))),combb(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),a),combk(fun(poly(a),poly(a)),poly(a))),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),poly(a))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a)))),combb(fun(poly(a),poly(a)),fun(poly(a),poly(a)),a),combs(poly(a),poly(a),poly(a),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),aa(fun(poly(a),fun(poly(a),poly(a))),fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),combb(poly(a),fun(poly(a),poly(a)),poly(a)),plus_plus(poly(a))),aa(a,fun(poly(a),poly(a)),smult(a),h)))),pCons(a))),zero_zero(poly(a))),zero_zero(poly(a))),zero_zero(a)),
inference(forward_demodulation,[],[f1277,f493]) ).
tff(f1315,plain,
! [X4: $tType,X1: $tType,X0: $tType,X2: $tType,X3: fun(X0,fun(X1,X2)),X6: X4,X7: X1,X5: fun(X4,X0)] : ( aa(X4,X2,combc(X4,X1,X2,aa(fun(X4,X0),fun(X4,fun(X1,X2)),aa(fun(X0,fun(X1,X2)),fun(fun(X4,X0),fun(X4,fun(X1,X2))),combb(X0,fun(X1,X2),X4),X3),X5),X7),X6) = aa(X1,X2,aa(X0,fun(X1,X2),X3,aa(X4,X0,X5,X6)),X7) ),
inference(superposition,[],[f493,f492]) ).
tff(f4565,plain,
! [X5: $tType,X1: $tType,X0: $tType,X3: $tType,X2: $tType,X8: X1,X6: fun(X5,X0),X9: X2,X7: X5,X4: fun(X0,fun(X1,fun(X2,X3)))] : ( aa(X5,X3,combc(X5,X2,X3,combc(X5,X1,fun(X2,X3),aa(fun(X5,X0),fun(X5,fun(X1,fun(X2,X3))),aa(fun(X0,fun(X1,fun(X2,X3))),fun(fun(X5,X0),fun(X5,fun(X1,fun(X2,X3)))),combb(X0,fun(X1,fun(X2,X3)),X5),X4),X6),X8),X9),X7) = aa(X2,X3,aa(X1,fun(X2,X3),aa(X0,fun(X1,fun(X2,X3)),X4,aa(X5,X0,X6,X7)),X8),X9) ),
inference(superposition,[],[f991,f492]) ).
tff(f5871,plain,
! [X5: $tType,X1: $tType,X0: $tType,X2: $tType,X3: fun(X2,fun(X0,X1)),X6: fun(X5,fun(X2,X0)),X7: X5,X4: X2] : ( aa(X0,X1,aa(X2,fun(X0,X1),X3,X4),aa(X5,X0,combc(X5,X2,X0,X6,X4),X7)) = aa(X0,X1,aa(X2,fun(X0,X1),X3,X4),aa(X2,X0,aa(X5,fun(X2,X0),X6,X7),X4)) ),
inference(superposition,[],[f495,f1241]) ).
tff(f5872,plain,
! [X5: $tType,X1: $tType,X0: $tType,X2: $tType,X3: fun(X0,X1),X6: fun(X5,fun(X2,X0)),X7: X5,X4: X2] : ( aa(X0,X1,aa(X2,fun(X0,X1),aa(fun(X0,X1),fun(X2,fun(X0,X1)),combk(fun(X0,X1),X2),X3),X4),aa(X5,X0,combc(X5,X2,X0,X6,X4),X7)) = aa(X0,X1,X3,aa(X2,X0,aa(X5,fun(X2,X0),X6,X7),X4)) ),
inference(superposition,[],[f1234,f1241]) ).
tff(f5930,plain,
! [X5: $tType,X1: $tType,X0: $tType,X2: $tType,X3: fun(X0,X1),X6: fun(X5,fun(X2,X0)),X7: X5,X4: X2] : ( aa(X0,X1,X3,aa(X2,X0,aa(X5,fun(X2,X0),X6,X7),X4)) = aa(X0,X1,X3,aa(X5,X0,combc(X5,X2,X0,X6,X4),X7)) ),
inference(forward_demodulation,[],[f5872,f494]) ).
tff(f41200,plain,
~ pp(fequal(poly(a),aa(a,poly(a),combc(a,poly(a),poly(a),combc(a,poly(a),fun(poly(a),poly(a)),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),fun(poly(a),poly(a)))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),fun(poly(a),poly(a))))),combb(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),a),combk(fun(poly(a),poly(a)),poly(a))),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),poly(a))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a)))),combb(fun(poly(a),poly(a)),fun(poly(a),poly(a)),a),combs(poly(a),poly(a),poly(a),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),aa(fun(poly(a),fun(poly(a),poly(a))),fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),combb(poly(a),fun(poly(a),poly(a)),poly(a)),plus_plus(poly(a))),aa(a,fun(poly(a),poly(a)),smult(a),h)))),pCons(a))),zero_zero(poly(a))),zero_zero(poly(a))),zero_zero(a)),zero_zero(poly(a)))),
inference(unit_resulting_resolution,[],[f496,f1283]) ).
tff(f41211,plain,
~ pp(fequal(poly(a),aa(poly(a),poly(a),aa(poly(a),fun(poly(a),poly(a)),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),combk(fun(poly(a),poly(a)),poly(a)),aa(a,fun(poly(a),poly(a)),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),poly(a))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a)))),combb(fun(poly(a),poly(a)),fun(poly(a),poly(a)),a),combs(poly(a),poly(a),poly(a),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),aa(fun(poly(a),fun(poly(a),poly(a))),fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),combb(poly(a),fun(poly(a),poly(a)),poly(a)),plus_plus(poly(a))),aa(a,fun(poly(a),poly(a)),smult(a),h)))),pCons(a)),zero_zero(a))),zero_zero(poly(a))),zero_zero(poly(a))),zero_zero(poly(a)))),
inference(forward_demodulation,[],[f41200,f4565]) ).
tff(f41222,plain,
~ pp(fequal(poly(a),aa(poly(a),poly(a),combc(poly(a),poly(a),poly(a),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),combk(fun(poly(a),poly(a)),poly(a)),aa(a,fun(poly(a),poly(a)),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),poly(a))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a)))),combb(fun(poly(a),poly(a)),fun(poly(a),poly(a)),a),combs(poly(a),poly(a),poly(a),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),aa(fun(poly(a),fun(poly(a),poly(a))),fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),combb(poly(a),fun(poly(a),poly(a)),poly(a)),plus_plus(poly(a))),aa(a,fun(poly(a),poly(a)),smult(a),h)))),pCons(a)),zero_zero(a))),zero_zero(poly(a))),zero_zero(poly(a))),zero_zero(poly(a)))),
inference(forward_demodulation,[],[f41211,f493]) ).
tff(f41233,plain,
~ pp(fequal(poly(a),aa(poly(a),poly(a),aa(a,fun(poly(a),poly(a)),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),poly(a))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a)))),combb(fun(poly(a),poly(a)),fun(poly(a),poly(a)),a),combs(poly(a),poly(a),poly(a),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),aa(fun(poly(a),fun(poly(a),poly(a))),fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),combb(poly(a),fun(poly(a),poly(a)),poly(a)),plus_plus(poly(a))),aa(a,fun(poly(a),poly(a)),smult(a),h)))),pCons(a)),zero_zero(a)),zero_zero(poly(a))),zero_zero(poly(a)))),
inference(forward_demodulation,[],[f41222,f989]) ).
tff(f41244,plain,
~ pp(fequal(poly(a),aa(a,poly(a),combc(a,poly(a),poly(a),aa(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a))),aa(fun(fun(poly(a),poly(a)),fun(poly(a),poly(a))),fun(fun(a,fun(poly(a),poly(a))),fun(a,fun(poly(a),poly(a)))),combb(fun(poly(a),poly(a)),fun(poly(a),poly(a)),a),combs(poly(a),poly(a),poly(a),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),aa(fun(poly(a),fun(poly(a),poly(a))),fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),combb(poly(a),fun(poly(a),poly(a)),poly(a)),plus_plus(poly(a))),aa(a,fun(poly(a),poly(a)),smult(a),h)))),pCons(a)),zero_zero(poly(a))),zero_zero(a)),zero_zero(poly(a)))),
inference(forward_demodulation,[],[f41233,f493]) ).
tff(f41255,plain,
~ pp(fequal(poly(a),aa(poly(a),poly(a),aa(fun(poly(a),poly(a)),fun(poly(a),poly(a)),combs(poly(a),poly(a),poly(a),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),aa(fun(poly(a),fun(poly(a),poly(a))),fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),combb(poly(a),fun(poly(a),poly(a)),poly(a)),plus_plus(poly(a))),aa(a,fun(poly(a),poly(a)),smult(a),h))),aa(a,fun(poly(a),poly(a)),pCons(a),zero_zero(a))),zero_zero(poly(a))),zero_zero(poly(a)))),
inference(forward_demodulation,[],[f41244,f1315]) ).
tff(f41266,plain,
~ pp(fequal(poly(a),aa(poly(a),poly(a),aa(poly(a),fun(poly(a),poly(a)),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),aa(fun(poly(a),fun(poly(a),poly(a))),fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),combb(poly(a),fun(poly(a),poly(a)),poly(a)),plus_plus(poly(a))),aa(a,fun(poly(a),poly(a)),smult(a),h)),zero_zero(poly(a))),aa(poly(a),poly(a),aa(a,fun(poly(a),poly(a)),pCons(a),zero_zero(a)),zero_zero(poly(a)))),zero_zero(poly(a)))),
inference(forward_demodulation,[],[f41255,f495]) ).
tff(f41277,plain,
~ pp(fequal(poly(a),aa(poly(a),poly(a),aa(poly(a),fun(poly(a),poly(a)),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),aa(fun(poly(a),fun(poly(a),poly(a))),fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),combb(poly(a),fun(poly(a),poly(a)),poly(a)),plus_plus(poly(a))),aa(a,fun(poly(a),poly(a)),smult(a),h)),zero_zero(poly(a))),aa(a,poly(a),combc(a,poly(a),poly(a),pCons(a),zero_zero(poly(a))),zero_zero(a))),zero_zero(poly(a)))),
inference(forward_demodulation,[],[f41266,f5871]) ).
tff(f41288,plain,
~ pp(fequal(poly(a),aa(poly(a),poly(a),combc(poly(a),poly(a),poly(a),aa(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a))),aa(fun(poly(a),fun(poly(a),poly(a))),fun(fun(poly(a),poly(a)),fun(poly(a),fun(poly(a),poly(a)))),combb(poly(a),fun(poly(a),poly(a)),poly(a)),plus_plus(poly(a))),aa(a,fun(poly(a),poly(a)),smult(a),h)),aa(a,poly(a),combc(a,poly(a),poly(a),pCons(a),zero_zero(poly(a))),zero_zero(a))),zero_zero(poly(a))),zero_zero(poly(a)))),
inference(forward_demodulation,[],[f41277,f493]) ).
tff(f41299,plain,
~ pp(fequal(poly(a),aa(poly(a),poly(a),aa(poly(a),fun(poly(a),poly(a)),plus_plus(poly(a)),aa(poly(a),poly(a),aa(a,fun(poly(a),poly(a)),smult(a),h),zero_zero(poly(a)))),aa(a,poly(a),combc(a,poly(a),poly(a),pCons(a),zero_zero(poly(a))),zero_zero(a))),zero_zero(poly(a)))),
inference(forward_demodulation,[],[f41288,f1315]) ).
tff(f41310,plain,
~ pp(fequal(poly(a),aa(poly(a),poly(a),combc(poly(a),poly(a),poly(a),plus_plus(poly(a)),aa(a,poly(a),combc(a,poly(a),poly(a),pCons(a),zero_zero(poly(a))),zero_zero(a))),aa(poly(a),poly(a),aa(a,fun(poly(a),poly(a)),smult(a),h),zero_zero(poly(a)))),zero_zero(poly(a)))),
inference(forward_demodulation,[],[f41299,f493]) ).
tff(f41321,plain,
~ pp(fequal(poly(a),aa(poly(a),poly(a),combc(poly(a),poly(a),poly(a),plus_plus(poly(a)),aa(a,poly(a),combc(a,poly(a),poly(a),pCons(a),zero_zero(poly(a))),zero_zero(a))),aa(a,poly(a),combc(a,poly(a),poly(a),smult(a),zero_zero(poly(a))),h)),zero_zero(poly(a)))),
inference(forward_demodulation,[],[f41310,f5930]) ).
tff(f41332,plain,
~ pp(fequal(poly(a),aa(poly(a),poly(a),combc(poly(a),poly(a),poly(a),plus_plus(poly(a)),aa(a,poly(a),combc(a,poly(a),poly(a),pCons(a),zero_zero(poly(a))),zero_zero(a))),zero_zero(poly(a))),zero_zero(poly(a)))),
inference(forward_demodulation,[],[f41321,f1013]) ).
tff(f41343,plain,
~ pp(fequal(poly(a),aa(a,poly(a),combc(a,poly(a),poly(a),pCons(a),zero_zero(poly(a))),zero_zero(a)),zero_zero(poly(a)))),
inference(forward_demodulation,[],[f41332,f867]) ).
tff(f41354,plain,
~ pp(fequal(poly(a),zero_zero(poly(a)),zero_zero(poly(a)))),
inference(forward_demodulation,[],[f41343,f1052]) ).
tff(f41363,plain,
$false,
inference(forward_subsumption_resolution,[],[f41354,f525]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW487_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n009.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 14:14:30 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.33/1.30 % (3050356)Detected formulas, will run a generic FOF schedule.
% 5.33/1.30 % (3050367)dis-21_1_sil=8000:lcm=predicate:random_seed=1703074224:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 5.33/1.30 % (3050364)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=459102917:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.33/1.30 % (3050366)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4199443715:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.33/1.30 % (3050365)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=463523817:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.33/1.30 % (3050361)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=2057605935:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.33/1.30 % (3050362)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=1294950281:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.33/1.30 % (3050363)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=772219870:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.33/1.30 % (3050367)Instruction limit reached!
% 5.33/1.30 % (3050367)------------------------------
% 5.33/1.30 % (3050367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.30 % (3050367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.30 % (3050367)CaDiCaL version: 2.1.3
% 5.33/1.30 % (3050367)Termination reason: Instruction limit
% 5.33/1.30 % (3050367)Termination phase: Saturation
% 5.33/1.30 % (3050367)Time elapsed: 0.041 s
% 5.33/1.30 % (3050367)Peak memory usage: 89 MB
% 5.33/1.30 % (3050367)Instructions burned: 130 (million)
% 5.33/1.30 % (3050364)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 5.33/1.30 % (3050363)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 5.33/1.30 % (3050364)Instruction limit reached!
% 5.33/1.30 % (3050364)------------------------------
% 5.33/1.30 % (3050364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.30 % (3050364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.30 % (3050364)CaDiCaL version: 2.1.3
% 5.33/1.30 % (3050364)Termination reason: Instruction limit
% 5.33/1.30 % (3050364)Termination phase: Saturation
% 5.33/1.30 % (3050364)Time elapsed: 0.062 s
% 5.33/1.30 % (3050364)Peak memory usage: 89 MB
% 5.33/1.30 % (3050364)Instructions burned: 109 (million)
% 5.33/1.30 % (3050365)Instruction limit reached!
% 5.33/1.30 % (3050365)------------------------------
% 5.33/1.30 % (3050365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.30 % (3050365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.30 % (3050365)CaDiCaL version: 2.1.3
% 5.33/1.30 % (3050365)Termination reason: Instruction limit
% 5.33/1.30 % (3050365)Termination phase: Saturation
% 5.33/1.30 % (3050365)Time elapsed: 0.067 s
% 5.33/1.30 % (3050365)Peak memory usage: 89 MB
% 5.33/1.30 % (3050365)Instructions burned: 120 (million)
% 5.33/1.30 % (3050366)Instruction limit reached!
% 5.33/1.30 % (3050366)------------------------------
% 5.33/1.30 % (3050366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.30 % (3050366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.30 % (3050366)CaDiCaL version: 2.1.3
% 5.33/1.30 % (3050366)Termination reason: Instruction limit
% 5.33/1.30 % (3050366)Termination phase: Saturation
% 5.33/1.30 % (3050366)Time elapsed: 0.082 s
% 5.33/1.30 % (3050366)Peak memory usage: 89 MB
% 5.33/1.30 % (3050366)Instructions burned: 139 (million)
% 5.33/1.30 % (3050375)lrs+10_1_sil=8000:sp=occurrence:random_seed=329341720:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 5.33/1.30 % (3050375)Instruction limit reached!
% 5.33/1.30 % (3050375)------------------------------
% 5.33/1.30 % (3050375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.30 % (3050375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.30 % (3050375)CaDiCaL version: 2.1.3
% 7.44/1.65 % (3050375)Termination reason: Instruction limit
% 7.44/1.65 % (3050375)Termination phase: Saturation
% 7.44/1.65 % (3050375)Time elapsed: 0.078 s
% 7.44/1.65 % (3050375)Peak memory usage: 90 MB
% 7.44/1.65 % (3050375)Instructions burned: 286 (million)
% 7.44/1.65 % (3050376)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1576017138:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 7.44/1.65 % (3050377)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2256107771:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 7.44/1.65 % (3050379)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=3196427004:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 7.44/1.65 % (3050376)Instruction limit reached!
% 7.44/1.65 % (3050376)------------------------------
% 7.44/1.65 % (3050376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.44/1.65 % (3050376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.65 % (3050376)CaDiCaL version: 2.1.3
% 7.44/1.65 % (3050376)Termination reason: Instruction limit
% 7.44/1.65 % (3050376)Termination phase: Saturation
% 7.44/1.65 % (3050376)Time elapsed: 0.087 s
% 7.44/1.65 % (3050376)Peak memory usage: 90 MB
% 7.44/1.65 % (3050376)Instructions burned: 157 (million)
% 7.44/1.65 % (3050380)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1347513470:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 7.44/1.65 % (3050380)Refutation not found, incomplete strategy
% 7.44/1.65 % (3050380)------------------------------
% 7.44/1.65 % (3050380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.44/1.65 % (3050380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.65 % (3050380)CaDiCaL version: 2.1.3
% 7.44/1.65 % (3050380)Termination reason: Refutation not found, incomplete strategy
% 7.44/1.65 % (3050380)Time elapsed: 0.010 s
% 7.44/1.65 % (3050380)Peak memory usage: 88 MB
% 7.44/1.65 % (3050380)Instructions burned: 18 (million)
% 7.44/1.65 % (3050379)Instruction limit reached!
% 7.44/1.65 % (3050379)------------------------------
% 7.44/1.65 % (3050379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.44/1.65 % (3050379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.65 % (3050379)CaDiCaL version: 2.1.3
% 7.44/1.65 % (3050379)Termination reason: Instruction limit
% 7.44/1.65 % (3050379)Termination phase: Saturation
% 7.44/1.65 % (3050379)Time elapsed: 0.134 s
% 7.44/1.65 % (3050379)Peak memory usage: 90 MB
% 7.44/1.65 % (3050379)Instructions burned: 249 (million)
% 7.44/1.65 % (3050384)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=872871760:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 7.44/1.65 % Exception at run slice level
% 7.44/1.65 % Exception at run slice levelUser error: GNN currently only supports monomorphic FOL.
% 7.44/1.65
% 7.44/1.65 User error: GNN currently only supports monomorphic FOL.
% 7.44/1.65 % Exception at run slice level
% 7.44/1.65 User error: GNN currently only supports monomorphic FOL.
% 7.44/1.65 % (3050377)Instruction limit reached!
% 7.44/1.65 % (3050377)------------------------------
% 7.44/1.65 % (3050377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.44/1.65 % (3050377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.65 % (3050377)CaDiCaL version: 2.1.3
% 7.44/1.65 % (3050377)Termination reason: Instruction limit
% 7.44/1.65 % (3050377)Termination phase: Saturation
% 7.44/1.65 % (3050377)Time elapsed: 0.205 s
% 7.44/1.65 % (3050377)Peak memory usage: 93 MB
% 7.44/1.65 % (3050377)Instructions burned: 325 (million)
% 7.44/1.65 % (3050390)lrs+10_1_sil=8000:sp=occurrence:random_seed=4221043478:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi)
% 7.44/1.65 % (3050389)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4034758164:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 7.44/1.65 % (3050386)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=635940377:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 7.44/1.65 % (3050388)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3969453926:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 7.44/1.65 % (3050380)------------------------------
% 7.44/1.65 % (3050380)------------------------------
% 7.44/1.65 % (3050391)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3835018911:i=437:sd=1:aac=none:ss=included_2994 on theBenchmark for (2994ds/437Mi)
% 9.82/1.97 % (3050389)Instruction limit reached!
% 9.82/1.97 % (3050389)------------------------------
% 9.82/1.97 % (3050389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/1.97 % (3050389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/1.97 % (3050389)CaDiCaL version: 2.1.3
% 9.82/1.97 % (3050389)Termination reason: Instruction limit
% 9.82/1.97 % (3050389)Termination phase: Saturation
% 9.82/1.97 % (3050389)Time elapsed: 0.060 s
% 9.82/1.97 % (3050389)Peak memory usage: 89 MB
% 9.82/1.97 % (3050389)Instructions burned: 114 (million)
% 9.82/1.97 % (3050386)Instruction limit reached!
% 9.82/1.97 % (3050386)------------------------------
% 9.82/1.97 % (3050386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/1.97 % (3050386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/1.97 % (3050386)CaDiCaL version: 2.1.3
% 9.82/1.97 % (3050386)Termination reason: Instruction limit
% 9.82/1.97 % (3050386)Termination phase: Saturation
% 9.82/1.97 % (3050386)Time elapsed: 0.064 s
% 9.82/1.97 % (3050386)Peak memory usage: 90 MB
% 9.82/1.97 % (3050386)Instructions burned: 114 (million)
% 9.82/1.97 % (3050391)Refutation not found, incomplete strategy
% 9.82/1.97 % (3050391)------------------------------
% 9.82/1.97 % (3050391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/1.97 % (3050391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/1.97 % (3050391)CaDiCaL version: 2.1.3
% 9.82/1.97 % (3050391)Termination reason: Refutation not found, incomplete strategy
% 9.82/1.97 % (3050391)Time elapsed: 0.013 s
% 9.82/1.97 % (3050391)Peak memory usage: 89 MB
% 9.82/1.97 % (3050391)Instructions burned: 24 (million)
% 9.82/1.97 % (3050388)Instruction limit reached!
% 9.82/1.97 % (3050388)------------------------------
% 9.82/1.97 % (3050388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/1.97 % (3050388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/1.97 % (3050388)CaDiCaL version: 2.1.3
% 9.82/1.97 % (3050388)Termination reason: Instruction limit
% 9.82/1.97 % (3050388)Termination phase: Saturation
% 9.82/1.97 % (3050388)Time elapsed: 0.063 s
% 9.82/1.97 % (3050388)Peak memory usage: 89 MB
% 9.82/1.97 % (3050388)Instructions burned: 128 (million)
% 9.82/1.97 % Exception at run slice level
% 9.82/1.97 User error: GNN currently only supports monomorphic FOL.
% 9.82/1.97 % (3050401)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=3909922429:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/125Mi)
% 9.82/1.97 % (3050401)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 9.82/1.97 % (3050397)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1927304596:i=5202:ss=axioms:sgt=16_2993 on theBenchmark for (2993ds/5202Mi)
% 9.82/1.97 % (3050398)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1553854216:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2993 on theBenchmark for (2993ds/134Mi)
% 9.82/1.97 % (3050401)Instruction limit reached!
% 9.82/1.97 % (3050401)------------------------------
% 9.82/1.97 % (3050401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/1.97 % (3050401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.82/1.97 % (3050401)CaDiCaL version: 2.1.3
% 9.82/1.97 % (3050401)Termination reason: Instruction limit
% 9.82/1.97 % (3050401)Termination phase: Saturation
% 9.82/1.97 % (3050401)Time elapsed: 0.038 s
% 9.82/1.97 % (3050401)Peak memory usage: 90 MB
% 9.82/1.97 % (3050401)Instructions burned: 128 (million)
% 9.82/1.97 % (3050399)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=23126378:st=8:i=592:sd=3:ep=RST:ss=axioms_2993 on theBenchmark for (2993ds/592Mi)
% 9.82/1.97 % (3050400)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=572700142:st=3:i=13193:sd=3:ss=axioms_2993 on theBenchmark for (2993ds/13193Mi)
% 9.82/1.97 % (3050398)Instruction limit reached!
% 9.82/1.97 % (3050398)------------------------------
% 9.82/1.97 % (3050398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.82/1.97 % (3050398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.92/2.73 % (3050398)CaDiCaL version: 2.1.3
% 15.92/2.73 % (3050398)Termination reason: Instruction limit
% 15.92/2.73 % (3050398)Termination phase: Saturation
% 15.92/2.73 % (3050398)Time elapsed: 0.079 s
% 15.92/2.73 % (3050398)Peak memory usage: 90 MB
% 15.92/2.73 % (3050398)Instructions burned: 134 (million)
% 15.92/2.73 % (3050405)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=217466399:i=134:gtgl=5:slsql=off:gtg=exists_sym_2991 on theBenchmark for (2991ds/134Mi)
% 15.92/2.73 % Exception at run slice level
% 15.92/2.73 User error: Immediate (shared) subterms of term/literal aa(poly(X0),poly(X0),sF20(X0,X1),X2) have different types/not well-typed!
% 15.92/2.73 % (3050391)------------------------------
% 15.92/2.73 % (3050391)------------------------------
% 15.92/2.73 % (3050410)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2672524661:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2990 on theBenchmark for (2990ds/431Mi)
% 15.92/2.73 % (3050410)Refutation not found, incomplete strategy
% 15.92/2.73 % (3050410)------------------------------
% 15.92/2.73 % (3050410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.92/2.73 % (3050410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.92/2.73 % (3050410)CaDiCaL version: 2.1.3
% 15.92/2.73 % (3050410)Termination reason: Refutation not found, incomplete strategy
% 15.92/2.73 % (3050410)Time elapsed: 0.003 s
% 15.92/2.73 % (3050410)Peak memory usage: 88 MB
% 15.92/2.73 % (3050410)Instructions burned: 10 (million)
% 15.92/2.73 % (3050408)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1982082145:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/141Mi)
% 15.92/2.73 % (3050408)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 15.92/2.73 % (3050408)Refutation not found, incomplete strategy
% 15.92/2.73 % (3050408)------------------------------
% 15.92/2.73 % (3050408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.92/2.73 % (3050408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.92/2.73 % (3050408)CaDiCaL version: 2.1.3
% 15.92/2.73 % (3050408)Termination reason: Refutation not found, incomplete strategy
% 15.92/2.73 % (3050408)Time elapsed: 0.005 s
% 15.92/2.73 % (3050408)Peak memory usage: 88 MB
% 15.92/2.73 % (3050408)Instructions burned: 4 (million)
% 15.92/2.73 % (3050390)Instruction limit reached!
% 15.92/2.73 % (3050390)------------------------------
% 15.92/2.73 % (3050390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.92/2.73 % (3050390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.92/2.73 % (3050390)CaDiCaL version: 2.1.3
% 15.92/2.73 % (3050390)Termination reason: Instruction limit
% 15.92/2.73 % (3050390)Termination phase: Saturation
% 15.92/2.73 % (3050390)Time elapsed: 0.438 s
% 15.92/2.73 % (3050390)Peak memory usage: 90 MB
% 15.92/2.73 % (3050390)Instructions burned: 908 (million)
% 15.92/2.73 % (3050411)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=2660699573:i=6060:aac=none:ins=25_2990 on theBenchmark for (2990ds/6060Mi)
% 15.92/2.73 % (3050399)Instruction limit reached!
% 15.92/2.73 % (3050399)------------------------------
% 15.92/2.73 % (3050399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.92/2.73 % (3050399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.92/2.73 % (3050399)CaDiCaL version: 2.1.3
% 15.92/2.73 % (3050399)Termination reason: Instruction limit
% 15.92/2.73 % (3050399)Termination phase: Saturation
% 15.92/2.73 % (3050399)Time elapsed: 0.315 s
% 15.92/2.73 % (3050399)Peak memory usage: 92 MB
% 15.92/2.73 % (3050399)Instructions burned: 593 (million)
% 15.92/2.73 % (3050410)------------------------------
% 15.92/2.73 % (3050410)------------------------------
% 15.92/2.73 % Exception at run slice level
% 15.92/2.73 User error: GNN currently only supports monomorphic FOL.
% 15.92/2.73 % Exception at run slice level
% 15.92/2.73 User error: GNN currently only supports monomorphic FOL.
% 15.92/2.73 % (3050414)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=4070830154:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2989 on theBenchmark for (2989ds/150Mi)
% 15.92/2.73 % (3050414)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 15.92/2.73 % (3050417)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4047361819:i=667:av=off:fsr=off_2988 on theBenchmark for (2988ds/667Mi)
% 22.66/3.78 % (3050416)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2671264542:i=14155:bd=all_2988 on theBenchmark for (2988ds/14155Mi)
% 22.66/3.78 % (3050408)------------------------------
% 22.66/3.78 % (3050408)------------------------------
% 22.66/3.78 % (3050414)Instruction limit reached!
% 22.66/3.78 % (3050414)------------------------------
% 22.66/3.78 % (3050414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.66/3.78 % (3050414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.66/3.78 % (3050414)CaDiCaL version: 2.1.3
% 22.66/3.78 % (3050414)Termination reason: Instruction limit
% 22.66/3.78 % (3050414)Termination phase: Saturation
% 22.66/3.78 % (3050414)Time elapsed: 0.094 s
% 22.66/3.78 % (3050414)Peak memory usage: 91 MB
% 22.66/3.78 % (3050414)Instructions burned: 151 (million)
% 22.66/3.78 % (3050418)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=2627758200:s2a=on:i=185:s2at=1.8:fdi=4_2988 on theBenchmark for (2988ds/185Mi)
% 22.66/3.78 % (3050420)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3627570545:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2988 on theBenchmark for (2988ds/193Mi)
% 22.66/3.78 % (3050417)Instruction limit reached!
% 22.66/3.78 % (3050417)------------------------------
% 22.66/3.78 % (3050417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.66/3.78 % (3050417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.66/3.78 % (3050417)CaDiCaL version: 2.1.3
% 22.66/3.78 % (3050417)Termination reason: Instruction limit
% 22.66/3.78 % (3050417)Termination phase: Saturation
% 22.66/3.78 % (3050417)Time elapsed: 0.160 s
% 22.66/3.78 % (3050417)Peak memory usage: 89 MB
% 22.66/3.78 % (3050417)Instructions burned: 672 (million)
% 22.66/3.78 % (3050423)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=737402995:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2987 on theBenchmark for (2987ds/4850Mi)
% 22.66/3.78 % (3050424)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=78427331:i=12111:sd=1:ss=included_2987 on theBenchmark for (2987ds/12111Mi)
% 22.66/3.78 % (3050420)Instruction limit reached!
% 22.66/3.78 % (3050420)------------------------------
% 22.66/3.78 % (3050420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.66/3.78 % (3050420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.66/3.78 % (3050420)CaDiCaL version: 2.1.3
% 22.66/3.78 % (3050420)Termination reason: Instruction limit
% 22.66/3.78 % (3050420)Termination phase: Saturation
% 22.66/3.78 % (3050420)Time elapsed: 0.098 s
% 22.66/3.78 % (3050420)Peak memory usage: 89 MB
% 22.66/3.78 % (3050420)Instructions burned: 195 (million)
% 22.66/3.78 % (3050418)Instruction limit reached!
% 22.66/3.78 % (3050418)------------------------------
% 22.66/3.78 % (3050418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.66/3.78 % (3050418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.66/3.78 % (3050418)CaDiCaL version: 2.1.3
% 22.66/3.78 % (3050418)Termination reason: Instruction limit
% 22.66/3.78 % (3050418)Termination phase: Saturation
% 22.66/3.78 % (3050418)Time elapsed: 0.118 s
% 22.66/3.78 % (3050418)Peak memory usage: 91 MB
% 22.66/3.78 % (3050418)Instructions burned: 185 (million)
% 22.66/3.78 % Exception at run slice level
% 22.66/3.78 User error: GNN currently only supports monomorphic FOL.
% 22.66/3.78 % (3050427)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1737125298:i=319:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/319Mi)
% 22.66/3.78 % (3050431)dis-1011_128_sil=32000:random_seed=352622776:i=3706:ep=RST:av=off_2985 on theBenchmark for (2985ds/3706Mi)
% 22.66/3.78 % (3050430)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=747700501:i=2064:ep=RST_2985 on theBenchmark for (2985ds/2064Mi)
% 22.66/3.78 % (3050427)Instruction limit reached!
% 22.66/3.78 % (3050427)------------------------------
% 22.66/3.78 % (3050427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.66/3.78 % (3050427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.66/3.78 % (3050427)CaDiCaL version: 2.1.3
% 29.19/4.79 % (3050427)Termination reason: Instruction limit
% 29.19/4.79 % (3050427)Termination phase: Saturation
% 29.19/4.79 % (3050427)Time elapsed: 0.078 s
% 29.19/4.79 % (3050427)Peak memory usage: 89 MB
% 29.19/4.79 % (3050427)Instructions burned: 323 (million)
% 29.19/4.79 % (3050432)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1416650352:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2985 on theBenchmark for (2985ds/757Mi)
% 29.19/4.79 % (3050432)Refutation not found, incomplete strategy
% 29.19/4.79 % (3050432)------------------------------
% 29.19/4.79 % (3050432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.19/4.79 % (3050432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.19/4.79 % (3050432)CaDiCaL version: 2.1.3
% 29.19/4.79 % (3050432)Termination reason: Refutation not found, incomplete strategy
% 29.19/4.79 % (3050432)Time elapsed: 0.008 s
% 29.19/4.79 % (3050432)Peak memory usage: 89 MB
% 29.19/4.79 % (3050432)Instructions burned: 12 (million)
% 29.19/4.79 % Exception at run slice level
% 29.19/4.79 User error: GNN currently only supports monomorphic FOL.
% 29.19/4.79 % (3050436)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=716487200:i=13913:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/13913Mi)
% 29.19/4.79 % (3050438)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=4216769038:i=9925:aac=none_2983 on theBenchmark for (2983ds/9925Mi)
% 29.19/4.79 % Exception at run slice level
% 29.19/4.79 User error: GNN currently only supports monomorphic FOL.
% 29.19/4.79 % (3050432)------------------------------
% 29.19/4.79 % (3050432)------------------------------
% 29.19/4.79 % Exception at run slice level
% 29.19/4.79 User error: GNN currently only supports monomorphic FOL.
% 29.19/4.79 % (3050443)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2223170563:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2981 on theBenchmark for (2981ds/11145Mi)
% 29.19/4.79 % (3050441)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2529127865:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2982 on theBenchmark for (2982ds/2479Mi)
% 29.19/4.79 % (3050441)Refutation not found, incomplete strategy
% 29.19/4.79 % (3050441)------------------------------
% 29.19/4.79 % (3050441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.19/4.79 % (3050441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.19/4.79 % (3050441)CaDiCaL version: 2.1.3
% 29.19/4.79 % (3050441)Termination reason: Refutation not found, incomplete strategy
% 29.19/4.79 % (3050441)Time elapsed: 0.006 s
% 29.19/4.79 % (3050441)Peak memory usage: 89 MB
% 29.19/4.79 % (3050441)Instructions burned: 10 (million)
% 29.19/4.79 % (3050442)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=556844206:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/440Mi)
% 29.19/4.79 % (3050442)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 29.19/4.79 % Exception at run slice level
% 29.19/4.79 User error: GNN currently only supports monomorphic FOL.
% 29.19/4.79 % Exception at run slice level
% 29.19/4.79 User error: GNN currently only supports monomorphic FOL.
% 29.19/4.79 % (3050441)------------------------------
% 29.19/4.79 % (3050441)------------------------------
% 29.19/4.79 % (3050442)Instruction limit reached!
% 29.19/4.79 % (3050442)------------------------------
% 29.19/4.79 % (3050442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.19/4.79 % (3050442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.19/4.79 % (3050442)CaDiCaL version: 2.1.3
% 29.19/4.79 % (3050442)Termination reason: Instruction limit
% 29.19/4.79 % (3050442)Termination phase: Saturation
% 29.19/4.79 % (3050442)Time elapsed: 0.236 s
% 29.19/4.79 % (3050442)Peak memory usage: 89 MB
% 29.19/4.79 % (3050442)Instructions burned: 441 (million)
% 29.19/4.79 % (3050448)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1889270939:st=2:s2a=on:i=524:s2at=2:ss=axioms_2978 on theBenchmark for (2978ds/524Mi)
% 29.19/4.79 % (3050447)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=2814938194:cts=off:i=3034:av=off:er=known:fsd=on_2978 on theBenchmark for (2978ds/3034Mi)
% 29.19/4.79 % (3050449)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=893153666:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2978 on theBenchmark for (2978ds/1016Mi)
% 37.31/5.83 % (3050451)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3292767773:i=14123:bd=preordered:ins=4_2977 on theBenchmark for (2977ds/14123Mi)
% 37.31/5.83 % (3050448)Instruction limit reached!
% 37.31/5.83 % (3050448)------------------------------
% 37.31/5.83 % (3050448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.31/5.83 % (3050448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.31/5.83 % (3050448)CaDiCaL version: 2.1.3
% 37.31/5.83 % (3050448)Termination reason: Instruction limit
% 37.31/5.83 % (3050448)Termination phase: Saturation
% 37.31/5.83 % (3050448)Time elapsed: 0.166 s
% 37.31/5.83 % (3050448)Peak memory usage: 94 MB
% 37.31/5.83 % (3050448)Instructions burned: 524 (million)
% 37.31/5.83 % (3050455)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1895176054:i=5781:kws=precedence:bd=all:rawr=on_2976 on theBenchmark for (2976ds/5781Mi)
% 37.31/5.83 % (3050430)Instruction limit reached!
% 37.31/5.83 % (3050430)------------------------------
% 37.31/5.83 % (3050430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.31/5.83 % (3050430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.31/5.83 % (3050430)CaDiCaL version: 2.1.3
% 37.31/5.83 % (3050430)Termination reason: Instruction limit
% 37.31/5.83 % (3050430)Termination phase: Saturation
% 37.31/5.83 % (3050430)Time elapsed: 1.046 s
% 37.31/5.83 % (3050430)Peak memory usage: 97 MB
% 37.31/5.83 % (3050430)Instructions burned: 2064 (million)
% 37.31/5.83 % Exception at run slice level
% 37.31/5.83 User error: GNN currently only supports monomorphic FOL.
% 37.31/5.83 % Exception at run slice level
% 37.31/5.83 User error: GNN currently only supports monomorphic FOL.
% 37.31/5.83 % (3050457)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=13580165:i=2448:gtgl=5:bd=preordered:gtg=all_2973 on theBenchmark for (2973ds/2448Mi)
% 37.31/5.83 % (3050458)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=971855604:i=3223:kws=precedence:fgj=on:av=off_2973 on theBenchmark for (2973ds/3223Mi)
% 37.31/5.83 % (3050459)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1072478266:st=5.6:i=2033:sd=3:ss=axioms_2972 on theBenchmark for (2972ds/2033Mi)
% 37.31/5.83 % (3050449)Instruction limit reached!
% 37.31/5.83 % (3050449)------------------------------
% 37.31/5.83 % (3050449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.31/5.83 % (3050449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.31/5.83 % (3050449)CaDiCaL version: 2.1.3
% 37.31/5.83 % (3050449)Termination reason: Instruction limit
% 37.31/5.83 % (3050449)Termination phase: Saturation
% 37.31/5.83 % (3050449)Time elapsed: 0.614 s
% 37.31/5.83 % (3050449)Peak memory usage: 100 MB
% 37.31/5.83 % (3050449)Instructions burned: 1016 (million)
% 37.31/5.83 % (3050463)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3497003420:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2970 on theBenchmark for (2970ds/2055Mi)
% 37.31/5.83 % Exception at run slice level% Exception at run slice level
% 37.31/5.83
% 37.31/5.83 User error: User error: GNN currently only supports monomorphic FOL.GNN currently only supports monomorphic FOL.
% 37.31/5.83
% 37.31/5.83 % Exception at run slice level
% 37.31/5.83 User error: GNN currently only supports monomorphic FOL.
% 37.31/5.83 % (3050465)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=3957258182:i=21611:sd=3:ss=axioms_2969 on theBenchmark for (2969ds/21611Mi)
% 37.31/5.83 % (3050466)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2240802944:i=4835:sd=13:ss=axioms:sgt=23_2969 on theBenchmark for (2969ds/4835Mi)
% 37.31/5.83 % (3050467)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=3684263149:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2968 on theBenchmark for (2968ds/797Mi)
% 37.31/5.83 % (3050431)Instruction limit reached!
% 37.31/5.83 % (3050431)------------------------------
% 37.31/5.83 % (3050431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.31/5.83 % (3050431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.24/7.05 % (3050431)CaDiCaL version: 2.1.3
% 46.24/7.05 % (3050431)Termination reason: Instruction limit
% 46.24/7.05 % (3050431)Termination phase: Saturation
% 46.24/7.05 % (3050431)Time elapsed: 1.818 s
% 46.24/7.05 % (3050431)Peak memory usage: 102 MB
% 46.24/7.05 % (3050431)Instructions burned: 3706 (million)
% 46.24/7.05 % Exception at run slice level
% 46.24/7.05 User error: GNN currently only supports monomorphic FOL.
% 46.24/7.05 % (3050471)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=805749580:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2966 on theBenchmark for (2966ds/2326Mi)
% 46.24/7.05 % Exception at run slice level
% 46.24/7.05 User error: GNN currently only supports monomorphic FOL.
% 46.24/7.05 % (3050472)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2075154846:i=6038:nm=6_2965 on theBenchmark for (2965ds/6038Mi)
% 46.24/7.05 % (3050475)lrs+10_1_sil=32000:sp=occurrence:random_seed=1495901677:st=2:i=33334:sd=3:ss=included:sgt=32_2964 on theBenchmark for (2964ds/33334Mi)
% 46.24/7.05 % (3050467)Instruction limit reached!
% 46.24/7.05 % (3050467)------------------------------
% 46.24/7.05 % (3050467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.24/7.05 % (3050467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.24/7.05 % (3050467)CaDiCaL version: 2.1.3
% 46.24/7.05 % (3050467)Termination reason: Instruction limit
% 46.24/7.05 % (3050467)Termination phase: Saturation
% 46.24/7.05 % (3050467)Time elapsed: 0.381 s
% 46.24/7.05 % (3050467)Peak memory usage: 92 MB
% 46.24/7.05 % (3050467)Instructions burned: 797 (million)
% 46.24/7.05 % (3050477)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=629914902:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2962 on theBenchmark for (2962ds/1008Mi)
% 46.24/7.05 % Exception at run slice level
% 46.24/7.05 User error: GNN currently only supports monomorphic FOL.
% 46.24/7.05 % (3050423)Instruction limit reached!
% 46.24/7.05 % (3050423)------------------------------
% 46.24/7.05 % (3050423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.24/7.05 % (3050423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.24/7.05 % (3050423)CaDiCaL version: 2.1.3
% 46.24/7.05 % (3050423)Termination reason: Instruction limit
% 46.24/7.05 % (3050423)Termination phase: Saturation
% 46.24/7.05 % (3050423)Time elapsed: 2.584 s
% 46.24/7.05 % (3050423)Peak memory usage: 108 MB
% 46.24/7.05 % (3050423)Instructions burned: 4850 (million)
% 46.24/7.05 % (3050479)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=720213030:i=8327:s2at=5:bd=preordered_2960 on theBenchmark for (2960ds/8327Mi)
% 46.24/7.05 % (3050455)Instruction limit reached!
% 46.24/7.05 % (3050455)------------------------------
% 46.24/7.05 % (3050455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.24/7.05 % (3050455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.24/7.05 % (3050455)CaDiCaL version: 2.1.3
% 46.24/7.05 % (3050455)Termination reason: Instruction limit
% 46.24/7.05 % (3050455)Termination phase: Saturation
% 46.24/7.05 % (3050455)Time elapsed: 1.591 s
% 46.24/7.05 % (3050455)Peak memory usage: 107 MB
% 46.24/7.05 % (3050455)Instructions burned: 5784 (million)
% 46.24/7.05 % (3050480)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=552408206:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2959 on theBenchmark for (2959ds/1083Mi)
% 46.24/7.05 % (3050482)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=3711907876:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2958 on theBenchmark for (2958ds/1084Mi)
% 46.24/7.05 % (3050477)Instruction limit reached!
% 46.24/7.05 % (3050477)------------------------------
% 46.24/7.05 % (3050477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.24/7.05 % (3050477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.24/7.05 % (3050477)CaDiCaL version: 2.1.3
% 46.24/7.05 % (3050477)Termination reason: Instruction limit
% 46.24/7.05 % (3050477)Termination phase: Saturation
% 46.24/7.05 % (3050477)Time elapsed: 0.536 s
% 46.24/7.05 % (3050477)Peak memory usage: 98 MB
% 46.24/7.05 % (3050477)Instructions burned: 1008 (million)
% 57.12/8.73 % Exception at run slice level
% 57.12/8.73 User error: GNN currently only supports monomorphic FOL.
% 57.12/8.73 % (3050485)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=4294415483:i=6995:s2at=5:gtg=all_2956 on theBenchmark for (2956ds/6995Mi)
% 57.12/8.73 % (3050482)Instruction limit reached!
% 57.12/8.73 % (3050482)------------------------------
% 57.12/8.73 % (3050482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.12/8.73 % (3050482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.12/8.73 % (3050482)CaDiCaL version: 2.1.3
% 57.12/8.73 % (3050482)Termination reason: Instruction limit
% 57.12/8.73 % (3050482)Termination phase: Saturation
% 57.12/8.73 % (3050482)Time elapsed: 0.330 s
% 57.12/8.73 % (3050482)Peak memory usage: 100 MB
% 57.12/8.73 % (3050482)Instructions burned: 1087 (million)
% 57.12/8.73 % (3050486)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3330312239:st=2:i=6225:sd=15:ss=axioms_2955 on theBenchmark for (2955ds/6225Mi)
% 57.12/8.73 % (3050488)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3480008696:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2954 on theBenchmark for (2954ds/3372Mi)
% 57.12/8.73 % (3050471)Instruction limit reached!
% 57.12/8.73 % (3050471)------------------------------
% 57.12/8.73 % (3050471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.12/8.73 % (3050471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.12/8.73 % (3050471)CaDiCaL version: 2.1.3
% 57.12/8.73 % (3050471)Termination reason: Instruction limit
% 57.12/8.73 % (3050471)Termination phase: Saturation
% 57.12/8.73 % (3050471)Time elapsed: 1.258 s
% 57.12/8.73 % (3050471)Peak memory usage: 112 MB
% 57.12/8.73 % (3050471)Instructions burned: 2328 (million)
% 57.12/8.73 % (3050480)Instruction limit reached!
% 57.12/8.73 % (3050480)------------------------------
% 57.12/8.73 % (3050480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.12/8.73 % (3050480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.12/8.73 % (3050480)CaDiCaL version: 2.1.3
% 57.12/8.73 % (3050480)Termination reason: Instruction limit
% 57.12/8.73 % (3050480)Termination phase: Saturation
% 57.12/8.73 % (3050480)Time elapsed: 0.632 s
% 57.12/8.73 % (3050480)Peak memory usage: 102 MB
% 57.12/8.73 % (3050480)Instructions burned: 1084 (million)
% 57.12/8.73 % Exception at run slice level
% 57.12/8.73 User error: GNN currently only supports monomorphic FOL.
% 57.12/8.73 % (3050491)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1137426383:st=2.3:i=26457:sd=10:ss=included:sgt=8_2952 on theBenchmark for (2952ds/26457Mi)
% 57.12/8.73 % (3050493)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=1417039726:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2951 on theBenchmark for (2951ds/2503Mi)
% 57.12/8.73 % (3050493)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 57.12/8.73 % (3050492)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=4027933403:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2952 on theBenchmark for (2952ds/13494Mi)
% 57.12/8.73 % Exception at run slice level
% 57.12/8.73 User error: GNN currently only supports monomorphic FOL.
% 57.12/8.73 % Exception at run slice level
% 57.12/8.73 User error: GNN currently only supports monomorphic FOL.
% 57.12/8.73 % (3050497)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2340532062:i=2559:sd=1:ep=RSTC:ss=axioms_2950 on theBenchmark for (2950ds/2559Mi)
% 57.12/8.73 % (3050498)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1439462039:i=30753:av=off:ss=included_2948 on theBenchmark for (2948ds/30753Mi)
% 57.12/8.73 % Exception at run slice level
% 57.12/8.73 User error: GNN currently only supports monomorphic FOL.
% 57.12/8.73 % Exception at run slice level
% 57.12/8.73 User error: GNN currently only supports monomorphic FOL.
% 57.12/8.73 % (3050501)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3125423400:i=26473:ep=RSTC_2947 on theBenchmark for (2947ds/26473Mi)
% 57.12/8.73 % Exception at run slice level
% 57.12/8.73 User error: GNN currently only supports monomorphic FOL.
% 57.12/8.73 % (3050502)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=2725990484:cts=off:i=2759:kws=inv_arity:fgj=on_2947 on theBenchmark for (2947ds/2759Mi)
% 70.43/10.54 % (3050504)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=1067912413:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2946 on theBenchmark for (2946ds/5665Mi)
% 70.43/10.54 % Exception at run slice level
% 70.43/10.54 User error: GNN currently only supports monomorphic FOL.
% 70.43/10.54 % (3050504)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 70.43/10.54 % (3050507)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=1531215176:i=1532:ep=RS:ss=axioms_2945 on theBenchmark for (2945ds/1532Mi)
% 70.43/10.54 % Exception at run slice level
% 70.43/10.54 User error: GNN currently only supports monomorphic FOL.
% 70.43/10.54 % (3050466)Instruction limit reached!
% 70.43/10.54 % (3050466)------------------------------
% 70.43/10.54 % (3050466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.43/10.54 % (3050466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.43/10.54 % (3050466)CaDiCaL version: 2.1.3
% 70.43/10.54 % (3050466)Termination reason: Instruction limit
% 70.43/10.54 % (3050466)Termination phase: Saturation
% 70.43/10.54 % (3050466)Time elapsed: 2.560 s
% 70.43/10.54 % (3050466)Peak memory usage: 132 MB
% 70.43/10.54 % (3050466)Instructions burned: 4835 (million)
% 70.43/10.54 % Exception at run slice level
% 70.43/10.54 User error: GNN currently only supports monomorphic FOL.
% 70.43/10.54 % Exception at run slice level
% 70.43/10.54 User error: GNN currently only supports monomorphic FOL.
% 70.43/10.54 % (3050509)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1695658691:i=1565:sd=2:ss=axioms:sgt=32_2942 on theBenchmark for (2942ds/1565Mi)
% 70.43/10.54 % (3050511)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1922376163:i=6052:sd=4:ss=axioms:sgt=24_2941 on theBenchmark for (2941ds/6052Mi)
% 70.43/10.54 % (3050510)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=3474839496:i=1572:fgj=on:gsp=on_2942 on theBenchmark for (2942ds/1572Mi)
% 70.43/10.54 % (3050510)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 70.43/10.54 % (3050512)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=3342686585:i=3500:sd=1:bd=preordered:sup=off:ss=included_2939 on theBenchmark for (2939ds/3500Mi)
% 70.43/10.54 % Exception at run slice level
% 70.43/10.54 User error: GNN currently only supports monomorphic FOL.
% 70.43/10.54 % (3050517)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=3247932187:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2937 on theBenchmark for (2937ds/1842Mi)
% 70.43/10.54 % (3050517)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 70.43/10.54 % Exception at run slice level
% 70.43/10.54 User error: GNN currently only supports monomorphic FOL.
% 70.43/10.54 % Exception at run slice level
% 70.43/10.54 User error: GNN currently only supports monomorphic FOL.
% 70.43/10.54 % Exception at run slice level
% 70.43/10.54 User error: GNN currently only supports monomorphic FOL.
% 70.43/10.54 % Exception at run slice level
% 70.43/10.54 User error: GNN currently only supports monomorphic FOL.
% 70.43/10.54 % (3050519)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3986493394:i=66096:add=on_2935 on theBenchmark for (2935ds/66096Mi)
% 70.43/10.54 % (3050520)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=981496152:i=1884:sd=1:nm=60:ss=axioms_2935 on theBenchmark for (2935ds/1884Mi)
% 70.43/10.54 % (3050521)lrs-1011_4:1_sil=16000:bsr=on:random_seed=4021187688:cts=off:i=5469:bs=on:fsr=off_2934 on theBenchmark for (2934ds/5469Mi)
% 70.43/10.54 % (3050522)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=2416329634:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2934 on theBenchmark for (2934ds/2037Mi)
% 82.16/12.25 % Exception at run slice level
% 82.16/12.25 User error: GNN currently only supports monomorphic FOL.
% 82.16/12.25 % (3050527)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2581033679:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2931 on theBenchmark for (2931ds/2110Mi)
% 82.16/12.25 % Exception at run slice level
% 82.16/12.25 User error: GNN currently only supports monomorphic FOL.
% 82.16/12.25 % Exception at run slice level
% 82.16/12.25 User error: GNN currently only supports monomorphic FOL.
% 82.16/12.25 % (3050530)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=1518470661:cond=fast:i=4891_2930 on theBenchmark for (2930ds/4891Mi)
% 82.16/12.25 % (3050529)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=3245213930:i=2430:add=off:aac=none:nm=16_2930 on theBenchmark for (2930ds/2430Mi)
% 82.16/12.25 % Exception at run slice level
% 82.16/12.25 User error: GNN currently only supports monomorphic FOL.
% 82.16/12.25 % (3050533)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=996306236:st=2:i=14845:sd=2:ss=included:fsd=on_2928 on theBenchmark for (2928ds/14845Mi)
% 82.16/12.25 % Exception at run slice level
% 82.16/12.25 User error: GNN currently only supports monomorphic FOL.
% 82.16/12.25 % Exception at run slice level
% 82.16/12.25 User error: GNN currently only supports monomorphic FOL.
% 82.16/12.25 % Exception at run slice level
% 82.16/12.25 User error: GNN currently only supports monomorphic FOL.
% 82.16/12.25 % (3050535)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=3344676286:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2925 on theBenchmark for (2925ds/7534Mi)
% 82.16/12.25 % (3050536)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=2858689131:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2925 on theBenchmark for (2925ds/10353Mi)
% 82.16/12.25 % (3050537)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2736618569:i=7860_2925 on theBenchmark for (2925ds/7860Mi)
% 82.16/12.25 % Exception at run slice level
% 82.16/12.25 User error: GNN currently only supports monomorphic FOL.
% 82.16/12.25 % (3050541)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=557896030:i=7896:sd=2:bs=on:ss=included:sgt=20_2922 on theBenchmark for (2922ds/7896Mi)
% 82.16/12.25 % Exception at run slice level
% 82.16/12.25 User error: GNN currently only supports monomorphic FOL.
% 82.16/12.25 % (3050486)Instruction limit reached!
% 82.16/12.25 % (3050486)------------------------------
% 82.16/12.25 % (3050486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.16/12.25 % (3050486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.16/12.25 % (3050486)CaDiCaL version: 2.1.3
% 82.16/12.25 % (3050486)Termination reason: Instruction limit
% 82.16/12.25 % (3050486)Termination phase: Saturation
% 82.16/12.25 % (3050486)Time elapsed: 3.366 s
% 82.16/12.25 % (3050486)Peak memory usage: 138 MB
% 82.16/12.25 % (3050486)Instructions burned: 6225 (million)
% 82.16/12.25 % (3050543)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=3649181284:i=5812:gtgl=2:gtg=all_2921 on theBenchmark for (2921ds/5812Mi)
% 82.16/12.25 % Exception at run slice level
% 82.16/12.25 User error: GNN currently only supports monomorphic FOL.
% 82.16/12.25 % (3050544)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=2530839989:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2920 on theBenchmark for (2920ds/2965Mi)
% 82.16/12.25 % (3050546)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=2455226827:i=2967:kws=precedence:bd=preordered:av=off_2919 on theBenchmark for (2919ds/2967Mi)
% 82.16/12.25 % Exception at run slice level
% 82.16/12.25 User error: GNN currently only supports monomorphic FOL.
% 117.22/17.11 % Exception at run slice level
% 117.22/17.11 User error: GNN currently only supports monomorphic FOL.
% 117.22/17.11 % (3050549)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=3555823905:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2916 on theBenchmark for (2916ds/3022Mi)
% 117.22/17.11 % Exception at run slice level
% 117.22/17.11 User error: GNN currently only supports monomorphic FOL.
% 117.22/17.11 % (3050550)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=123904335:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2916 on theBenchmark for (2916ds/3207Mi)
% 117.22/17.11 % (3050552)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=3772641081:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2915 on theBenchmark for (2915ds/3289Mi)
% 117.22/17.11 % Exception at run slice level
% 117.22/17.11 User error: GNN currently only supports monomorphic FOL.
% 117.22/17.11 % (3050555)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=367538973:i=38569:sd=3:ss=axioms:sgt=32_2913 on theBenchmark for (2913ds/38569Mi)
% 117.22/17.11 % Exception at run slice level
% 117.22/17.11 User error: GNN currently only supports monomorphic FOL.
% 117.22/17.11 % Exception at run slice level
% 117.22/17.11 User error: GNN currently only supports monomorphic FOL.
% 117.22/17.11 % Exception at run slice level
% 117.22/17.11 User error: GNN currently only supports monomorphic FOL.
% 117.22/17.11 % (3050558)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=3767341078:i=33824:bd=preordered_2911 on theBenchmark for (2911ds/33824Mi)
% 117.22/17.11 % (3050557)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=2558955223:cts=off:i=3394_2911 on theBenchmark for (2911ds/3394Mi)
% 117.22/17.11 % (3050559)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=1385068969:i=20684:bd=all:gtg=exists_sym_2910 on theBenchmark for (2910ds/20684Mi)
% 117.22/17.11 % Exception at run slice level
% 117.22/17.11 User error: GNN currently only supports monomorphic FOL.
% 117.22/17.11 % (3050563)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=184071476: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_2908 on theBenchmark for (2908ds/7222Mi)
% 117.22/17.11 % (3050563)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 117.22/17.11 % Exception at run slice level
% 117.22/17.11 User error: GNN currently only supports monomorphic FOL.
% 117.22/17.11 % Exception at run slice level
% 117.22/17.11 User error: GNN currently only supports monomorphic FOL.
% 117.22/17.11 % Exception at run slice level
% 117.22/17.11 User error: GNN currently only supports monomorphic FOL.
% 117.22/17.11 % (3050565)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=2697170990:st=4:i=7295:sd=4:ep=R:ss=axioms_2906 on theBenchmark for (2906ds/7295Mi)
% 117.22/17.11 % (3050567)lrs+10_1_sil=128000:lcm=predicate:random_seed=416054640:st=3:i=43697:sd=5:ss=axioms_2905 on theBenchmark for (2905ds/43697Mi)
% 117.22/17.11 % (3050566)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=2634896089:i=4036:ins=10_2905 on theBenchmark for (2905ds/4036Mi)
% 117.22/17.11 % Exception at run slice level
% 117.22/17.11 User error: GNN currently only supports monomorphic FOL.
% 117.22/17.11 % Exception at run slice level
% 117.22/17.11 User error: GNN currently only supports monomorphic FOL.
% 117.22/17.11 % (3050571)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=220655538:i=17599:gtg=all:ss=axioms:fsd=on_2901 on theBenchmark for (2901ds/17599Mi)
% 117.22/17.11 % (3050572)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=3450859833:i=4547:bd=preordered_2900 on theBenchmark for (2900ds/4547Mi)
% 117.22/17.11 % (3050521)Instruction limit reached!
% 142.87/20.70 % (3050521)------------------------------
% 142.87/20.70 % (3050521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.87/20.70 % (3050521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.87/20.70 % (3050521)CaDiCaL version: 2.1.3
% 142.87/20.70 % (3050521)Termination reason: Instruction limit
% 142.87/20.70 % (3050521)Termination phase: Saturation
% 142.87/20.70 % (3050521)Time elapsed: 3.498 s
% 142.87/20.70 % (3050521)Peak memory usage: 115 MB
% 142.87/20.70 % (3050521)Instructions burned: 5470 (million)
% 142.87/20.70 % (3050575)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=4267625784:i=9294:av=off_2898 on theBenchmark for (2898ds/9294Mi)
% 142.87/20.70 % Exception at run slice level
% 142.87/20.70 User error: GNN currently only supports monomorphic FOL.
% 142.87/20.70 % Exception at run slice level
% 142.87/20.70 User error: GNN currently only supports monomorphic FOL.
% 142.87/20.70 % (3050577)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3000262084:i=32849:add=on_2896 on theBenchmark for (2896ds/32849Mi)
% 142.87/20.70 % (3050578)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2701608684:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2896 on theBenchmark for (2896ds/4793Mi)
% 142.87/20.70 % Exception at run slice level
% 142.87/20.70 User error: GNN currently only supports monomorphic FOL.
% 142.87/20.70 % (3050581)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=3490125150:i=4840:nm=4:av=off_2893 on theBenchmark for (2893ds/4840Mi)
% 142.87/20.70 % Exception at run slice level
% 142.87/20.70 User error: GNN currently only supports monomorphic FOL.
% 142.87/20.70 % Exception at run slice level
% 142.87/20.70 User error: GNN currently only supports monomorphic FOL.
% 142.87/20.70 % (3050583)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=4269185041:cts=off:i=5002_2891 on theBenchmark for (2891ds/5002Mi)
% 142.87/20.70 % (3050584)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=201978177:i=30479:sd=3:ss=axioms_2891 on theBenchmark for (2891ds/30479Mi)
% 142.87/20.70 % Exception at run slice level
% 142.87/20.70 User error: GNN currently only supports monomorphic FOL.
% 142.87/20.70 % (3050587)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=1707730246:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2888 on theBenchmark for (2888ds/11035Mi)
% 142.87/20.70 % (3050587)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 142.87/20.70 % Exception at run slice level
% 142.87/20.70 User error: GNN currently only supports monomorphic FOL.
% 142.87/20.70 % Exception at run slice level
% 142.87/20.70 User error: GNN currently only supports monomorphic FOL.
% 142.87/20.70 % (3050589)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=2874881207:i=5835_2887 on theBenchmark for (2887ds/5835Mi)
% 142.87/20.70 % (3050590)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=1555590350:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2886 on theBenchmark for (2886ds/5890Mi)
% 142.87/20.70 % Exception at run slice level
% 142.87/20.70 User error: GNN currently only supports monomorphic FOL.
% 142.87/20.70 % (3050537)Instruction limit reached!
% 142.87/20.70 % (3050537)------------------------------
% 142.87/20.70 % (3050537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.87/20.70 % (3050537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.87/20.70 % (3050537)CaDiCaL version: 2.1.3
% 142.87/20.70 % (3050537)Termination reason: Instruction limit
% 142.87/20.70 % (3050537)Termination phase: Saturation
% 142.87/20.70 % (3050537)Time elapsed: 4.159 s
% 142.87/20.70 % (3050537)Peak memory usage: 112 MB
% 142.87/20.70 % (3050537)Instructions burned: 7861 (million)
% 142.87/20.70 % (3050593)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=3183144126:cts=off:i=19910:ep=RS_2884 on theBenchmark for (2884ds/19910Mi)
% 142.87/20.70 % Exception at run slice level
% 142.87/20.70 User error: GNN currently only supports monomorphic FOL.
% 142.87/20.70 % (3050594)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=2923009014:i=20312:bd=preordered:fsr=off:er=filter_2882 on theBenchmark for (2882ds/20312Mi)
% 153.87/22.24 % Exception at run slice level
% 153.87/22.24 User error: GNN currently only supports monomorphic FOL.
% 153.87/22.24 % (3050596)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=2796334346:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2882 on theBenchmark for (2882ds/13822Mi)
% 153.87/22.24 % (3050598)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=754315306:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2881 on theBenchmark for (2881ds/7144Mi)
% 153.87/22.24 % Exception at run slice level
% 153.87/22.24 User error: GNN currently only supports monomorphic FOL.
% 153.87/22.24 % Exception at run slice level
% 153.87/22.24 User error: GNN currently only supports monomorphic FOL.
% 153.87/22.24 % (3050601)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=2980802795:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2877 on theBenchmark for (2877ds/15184Mi)
% 153.87/22.24 % (3050602)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=3061142773:i=107375_2877 on theBenchmark for (2877ds/107375Mi)
% 153.87/22.24 % Exception at run slice level
% 153.87/22.24 User error: GNN currently only supports monomorphic FOL.
% 153.87/22.24 % Exception at run slice level
% 153.87/22.24 User error: GNN currently only supports monomorphic FOL.
% 153.87/22.24 % (3050605)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=1032357327:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2873 on theBenchmark for (2873ds/7958Mi)
% 153.87/22.24 % (3050606)dis+10_128_sil=16000:nwc=0.7:random_seed=4057186344:i=15999:nm=2:gsp=on_2872 on theBenchmark for (2872ds/15999Mi)
% 153.87/22.24 % (3050606)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 153.87/22.24 % Exception at run slice level
% 153.87/22.24 User error: GNN currently only supports monomorphic FOL.
% 153.87/22.24 % (3050609)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=767566480:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2868 on theBenchmark for (2868ds/8139Mi)
% 153.87/22.24 % (3050598)Instruction limit reached!
% 153.87/22.24 % (3050598)------------------------------
% 153.87/22.24 % (3050598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.87/22.24 % (3050598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.87/22.24 % (3050598)CaDiCaL version: 2.1.3
% 153.87/22.24 % (3050598)Termination reason: Instruction limit
% 153.87/22.24 % (3050598)Termination phase: Saturation
% 153.87/22.24 % (3050598)Time elapsed: 3.554 s
% 153.87/22.24 % (3050598)Peak memory usage: 98 MB
% 153.87/22.24 % (3050598)Instructions burned: 7144 (million)
% 153.87/22.24 % (3050611)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=3093191865:st=4:i=8950:sd=5:ss=axioms_2844 on theBenchmark for (2844ds/8950Mi)
% 153.87/22.24 % Exception at run slice level
% 153.87/22.24 User error: GNN currently only supports monomorphic FOL.
% 153.87/22.24 % (3050613)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=974381370:i=9809:ins=10:av=off_2839 on theBenchmark for (2839ds/9809Mi)
% 153.87/22.24 % Exception at run slice level
% 153.87/22.24 User error: GNN currently only supports monomorphic FOL.
% 153.87/22.24 % (3050615)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=3374346483:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2834 on theBenchmark for (2834ds/9885Mi)
% 153.87/22.24 % (3050609)Instruction limit reached!
% 153.87/22.24 % (3050609)------------------------------
% 153.87/22.24 % (3050609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.87/22.24 % (3050609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.87/22.24 % (3050609)CaDiCaL version: 2.1.3
% 153.87/22.24 % (3050609)Termination reason: Instruction limit
% 153.87/22.24 % (3050609)Termination phase: Saturation
% 153.87/22.24 % (3050609)Time elapsed: 3.381 s
% 153.87/22.24 % (3050609)Peak memory usage: 90 MB
% 165.09/23.90 % (3050609)Instructions burned: 8140 (million)
% 165.09/23.90 % (3050617)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=2956001927:cond=fast:i=32078:fgj=on:av=off_2832 on theBenchmark for (2832ds/32078Mi)
% 165.09/23.90 % Exception at run slice level
% 165.09/23.90 User error: GNN currently only supports monomorphic FOL.
% 165.09/23.90 % (3050619)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=1991242678:i=11101:bd=all:ss=axioms:sgt=8_2829 on theBenchmark for (2829ds/11101Mi)
% 165.09/23.90 % Exception at run slice level
% 165.09/23.90 User error: GNN currently only supports monomorphic FOL.
% 165.09/23.90 % (3050621)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=1432225706:cond=on:i=13220:s2at=3:aac=none:fsd=on_2827 on theBenchmark for (2827ds/13220Mi)
% 165.09/23.90 % Exception at run slice level
% 165.09/23.90 User error: GNN currently only supports monomorphic FOL.
% 165.09/23.90 % (3050623)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=1579069086:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2822 on theBenchmark for (2822ds/13528Mi)
% 165.09/23.90 % Exception at run slice level
% 165.09/23.90 User error: GNN currently only supports monomorphic FOL.
% 165.09/23.90 % (3050625)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=701528558:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2818 on theBenchmark for (2818ds/14854Mi)
% 165.09/23.90 % Exception at run slice level
% 165.09/23.90 User error: GNN currently only supports monomorphic FOL.
% 165.09/23.90 % (3050627)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=3251255254:i=14974:ss=axioms:sgt=16_2812 on theBenchmark for (2812ds/14974Mi)
% 165.09/23.90 % Exception at run slice level
% 165.09/23.90 User error: GNN currently only supports monomorphic FOL.
% 165.09/23.90 % (3050629)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=3196860150:i=33081:aac=none:fgj=on:bd=all:fsr=off_2808 on theBenchmark for (2808ds/33081Mi)
% 165.09/23.90 % (3050501)Instruction limit reached!
% 165.09/23.90 % (3050501)------------------------------
% 165.09/23.90 % (3050501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 165.09/23.90 % (3050501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.09/23.90 % (3050501)CaDiCaL version: 2.1.3
% 165.09/23.90 % (3050501)Termination reason: Instruction limit
% 165.09/23.90 % (3050501)Termination phase: Saturation
% 165.09/23.90 % (3050501)Time elapsed: 13.949 s
% 165.09/23.90 % (3050501)Peak memory usage: 430 MB
% 165.09/23.90 % (3050501)Instructions burned: 26473 (million)
% 165.09/23.90 % (3050631)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=1371311930:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2806 on theBenchmark for (2806ds/50856Mi)
% 165.09/23.90 % Exception at run slice level
% 165.09/23.90 User error: GNN currently only supports monomorphic FOL.
% 165.09/23.90 % (3050633)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=2395909765:i=69865_2803 on theBenchmark for (2803ds/69865Mi)
% 165.09/23.90 % Exception at run slice level
% 165.09/23.90 User error: GNN currently only supports monomorphic FOL.
% 165.09/23.90 % (3050635)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=3196232352:cond=fast:i=17802:gtgl=3:gtg=all_2801 on theBenchmark for (2801ds/17802Mi)
% 165.09/23.90 % Exception at run slice level
% 165.09/23.90 User error: Immediate (shared) subterms of term/literal aa(poly(X0),poly(X0),sF20(X0,X1),X2) have different types/not well-typed!
% 165.09/23.90 % (3050637)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=254280613:i=96644_2799 on theBenchmark for (2799ds/96644Mi)
% 165.09/23.90 % Exception at run slice level
% 165.09/23.90 User error: GNN currently only supports monomorphic FOL.
% 165.09/23.90 % (3050639)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0
% 165.09/23.90 % (3050639)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=2239381957:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2798 on theBenchmark for (2798ds/21161Mi)
% 169.82/24.67 % (3050606)Instruction limit reached!
% 169.82/24.67 % (3050606)------------------------------
% 169.82/24.67 % (3050606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.82/24.67 % (3050606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.82/24.67 % (3050606)CaDiCaL version: 2.1.3
% 169.82/24.67 % (3050606)Termination reason: Instruction limit
% 169.82/24.67 % (3050606)Termination phase: Saturation
% 169.82/24.67 % (3050606)Time elapsed: 7.592 s
% 169.82/24.67 % (3050606)Peak memory usage: 109 MB
% 169.82/24.67 % (3050606)Instructions burned: 15999 (million)
% 169.82/24.67 % (3050641)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=485062576:i=22761:gtg=all:ss=axioms:fsd=on_2795 on theBenchmark for (2795ds/22761Mi)
% 169.82/24.67 % (3050475)Instruction limit reached!
% 169.82/24.67 % (3050475)------------------------------
% 169.82/24.67 % (3050475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.82/24.67 % (3050475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.82/24.67 % (3050475)CaDiCaL version: 2.1.3
% 169.82/24.67 % (3050475)Termination reason: Instruction limit
% 169.82/24.67 % (3050475)Termination phase: Saturation
% 169.82/24.67 % (3050475)Time elapsed: 17.228 s
% 169.82/24.67 % (3050475)Peak memory usage: 142 MB
% 169.82/24.67 % (3050475)Instructions burned: 33335 (million)
% 169.82/24.67 % Exception at run slice level
% 169.82/24.67 User error: GNN currently only supports monomorphic FOL.
% 169.82/24.67 % (3050643)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=4035124946:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2790 on theBenchmark for (2790ds/23713Mi)
% 169.82/24.67 % (3050643)Refutation not found, incomplete strategy
% 169.82/24.67 % (3050643)------------------------------
% 169.82/24.67 % (3050643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.82/24.67 % (3050643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.82/24.67 % (3050643)CaDiCaL version: 2.1.3
% 169.82/24.67 % (3050643)Termination reason: Refutation not found, incomplete strategy
% 169.82/24.67 % (3050643)Time elapsed: 0.007 s
% 169.82/24.67 % (3050643)Peak memory usage: 88 MB
% 169.82/24.67 % (3050643)Instructions burned: 12 (million)
% 169.82/24.67 % (3050644)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=3024001727:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2790 on theBenchmark for (2790ds/26509Mi)
% 169.82/24.67 % (3050567)Instruction limit reached!
% 169.82/24.67 % (3050567)------------------------------
% 169.82/24.67 % (3050567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.82/24.67 % (3050567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.82/24.67 % (3050567)CaDiCaL version: 2.1.3
% 169.82/24.67 % (3050567)Termination reason: Instruction limit
% 169.82/24.67 % (3050567)Termination phase: Saturation
% 169.82/24.67 % (3050567)Time elapsed: 11.687 s
% 169.82/24.67 % (3050567)Peak memory usage: 148 MB
% 169.82/24.67 % (3050567)Instructions burned: 43699 (million)
% 169.82/24.67 % (3050643)------------------------------
% 169.82/24.67 % (3050643)------------------------------
% 169.82/24.67 % (3050647)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=1689104534:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2787 on theBenchmark for (2787ds/28957Mi)
% 169.82/24.67 % (3050649)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=705204316:i=29246:s2at=-1:kws=inv_arity:ins=10_2786 on theBenchmark for (2786ds/29246Mi)
% 169.82/24.67 % Exception at run slice level
% 169.82/24.67 User error: GNN currently only supports monomorphic FOL.
% 169.82/24.67 % (3050651)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=3274232214:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2785 on theBenchmark for (2785ds/30082Mi)
% 169.82/24.67 % (3050651)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 169.82/24.67 % Exception at run slice level
% 169.82/24.67 User error: GNN currently only supports monomorphic FOL.
% 169.82/24.67 % (3050653)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=1569449986:i=32262:bd=preordered_2781 on theBenchmark for (2781ds/32262Mi)
% 169.82/24.67 % Exception at run slice level
% 169.82/24.67 User error: GNN currently only supports monomorphic FOL.
% 169.82/24.67 % (3050655)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=3078432566:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2780 on theBenchmark for (2780ds/32870Mi)
% 169.82/24.67 % Exception at run slice level
% 169.82/24.67 User error: GNN currently only supports monomorphic FOL.
% 169.82/24.67 % (3050657)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=4228576479:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2776 on theBenchmark for (2776ds/33295Mi)
% 169.82/24.67 % Exception at run slice level
% 169.82/24.67 User error: GNN currently only supports monomorphic FOL.
% 169.82/24.67 % (3050659)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=164604373:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2775 on theBenchmark for (2775ds/36826Mi)
% 169.82/24.67 % Exception at run slice level
% 169.82/24.67 User error: GNN currently only supports monomorphic FOL.
% 169.82/24.67 % (3050619)Instruction limit reached!
% 169.82/24.67 % (3050619)------------------------------
% 169.82/24.67 % (3050619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.82/24.67 % (3050619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.82/24.67 % (3050619)CaDiCaL version: 2.1.3
% 169.82/24.67 % (3050619)Termination reason: Instruction limit
% 169.82/24.67 % (3050619)Termination phase: Saturation
% 169.82/24.67 % (3050619)Time elapsed: 5.665 s
% 169.82/24.67 % (3050619)Peak memory usage: 105 MB
% 169.82/24.67 % (3050619)Instructions burned: 11101 (million)
% 169.82/24.67 % (3050593)Instruction limit reached!
% 169.82/24.67 % (3050593)------------------------------
% 169.82/24.67 % (3050593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.82/24.67 % (3050593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.82/24.67 % (3050593)CaDiCaL version: 2.1.3
% 169.82/24.67 % (3050593)Termination reason: Instruction limit
% 169.82/24.67 % (3050593)Termination phase: Saturation
% 169.82/24.67 % (3050593)Time elapsed: 11.136 s
% 169.82/24.67 % (3050593)Peak memory usage: 179 MB
% 169.82/24.67 % (3050593)Instructions burned: 19912 (million)
% 169.82/24.67 % (3050662)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=602718292:s2pl=on:i=49423_2771 on theBenchmark for (2771ds/49423Mi)
% 169.82/24.67 % (3050661)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=2979830603:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2771 on theBenchmark for (2771ds/92981Mi)
% 169.82/24.67 % (3050663)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=2448299315:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2771 on theBenchmark for (2771ds/57299Mi)
% 169.82/24.67 % Exception at run slice level
% 169.82/24.67 User error: GNN currently only supports monomorphic FOL.
% 169.82/24.67 % Exception at run slice level
% 169.82/24.67 User error: GNN currently only supports monomorphic FOL.
% 169.82/24.67 % Exception at run slice level
% 169.82/24.67 User error: GNN currently only supports monomorphic FOL.
% 169.82/24.67 % (3050668)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=2952790317:i=69402:add=on:aac=none:fsr=off_2766 on theBenchmark for (2766ds/69402Mi)
% 169.82/24.67 % (3050667)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=425995969:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2766 on theBenchmark for (2766ds/127679Mi)
% 169.82/24.67 % (3050669)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=3078483708:i=100512:doe=on:fgj=on:bd=all:fsd=on_2766 on theBenchmark for (2766ds/100512Mi)
% 169.82/24.67 % Exception at run slice level
% 169.82/24.67 User error: GNN currently only supports monomorphic FOL.
% 169.82/24.67 % Exception at run slice level
% 169.82/24.67 User error: GNN currently only supports monomorphic FOL.
% 169.82/24.67 % Exception at run slice level
% 169.82/24.67 User error: GNN currently only supports monomorphic FOL.
% 169.82/24.67 % (3050673)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=3248197451:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2762 on theBenchmark for (2762ds/138761Mi)
% 169.82/24.67 % (3050674)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=3425333581:i=282386:rtra=on_2762 on theBenchmark for (2762ds/282386Mi)
% 169.82/24.67 % (3050637)First to succeed.
% 169.82/24.67 % (3050637)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3050356"
% 169.82/24.67 % (3050675)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=1909463089:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2761 on theBenchmark for (2761ds/269354Mi)
% 169.82/24.67 % (3050637)Refutation found. Thanks to Tanya!
% 169.82/24.67 % SZS status Theorem for theBenchmark
% 169.82/24.67 % SZS output start Proof for theBenchmark
% See solution above
% 171.47/24.76 % (3050637)------------------------------
% 171.47/24.76 % (3050637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.47/24.76 % (3050637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.47/24.76 % (3050637)CaDiCaL version: 2.1.3
% 171.47/24.76 % (3050637)Termination reason: Refutation
% 171.47/24.76 % (3050637)Time elapsed: 3.845 s
% 171.47/24.76 % (3050637)Peak memory usage: 137 MB
% 171.47/24.76 % (3050637)Instructions burned: 6541 (million)
% 171.47/24.76 % (3050637)------------------------------
% 171.47/24.76 % (3050637)------------------------------
% 171.47/24.76 % (3050356)Success in time 24.263 s
% 171.47/24.76 % Vampire exiting
%------------------------------------------------------------------------------