%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM989_5 : TPTP v9.3.1. Released v6.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:17:45 PM UTC 2026
% Result : Theorem 29.78s 5.13s
% Output : Refutation 30.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 51
% Syntax : Number of formulae : 296 ( 75 unt; 0 typ; 15 def)
% Number of atoms : 724 ( 127 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 781 ( 353 ~; 339 |; 33 &)
% ( 42 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 28 ( 26 usr; 16 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-3 aty)
% Number of variables : 265 ( 0 sgn 265 !; 0 ?; 265 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
bool: $tType ).
tff(type_def_6,type,
int: $tType ).
tff(type_def_7,type,
nat: $tType ).
tff(func_def_0,type,
minus_minus:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_1,type,
one_one:
!>[X0: $tType] : X0 ).
tff(func_def_2,type,
plus_plus:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_3,type,
times_times:
!>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).
tff(func_def_4,type,
zero_zero:
!>[X0: $tType] : X0 ).
tff(func_def_5,type,
bit0: int > int ).
tff(func_def_6,type,
bit1: int > int ).
tff(func_def_7,type,
pls: int ).
tff(func_def_8,type,
number_number_of:
!>[X0: $tType] : ( int > X0 ) ).
tff(func_def_9,type,
semiring_1_of_nat:
!>[X0: $tType] : ( nat > X0 ) ).
tff(func_def_10,type,
fFalse: bool ).
tff(func_def_11,type,
fTrue: bool ).
tff(func_def_12,type,
m1: int ).
tff(func_def_13,type,
n: nat ).
tff(func_def_14,type,
t: int ).
tff(pred_def_1,type,
number:
!>[X0: $tType] : $o ).
tff(pred_def_2,type,
ring:
!>[X0: $tType] : $o ).
tff(pred_def_3,type,
semiring:
!>[X0: $tType] : $o ).
tff(pred_def_4,type,
number_ring:
!>[X0: $tType] : $o ).
tff(pred_def_5,type,
ring_char_0:
!>[X0: $tType] : $o ).
tff(pred_def_6,type,
linorder:
!>[X0: $tType] : $o ).
tff(pred_def_7,type,
linordered_idom:
!>[X0: $tType] : $o ).
tff(pred_def_8,type,
linord219039673up_add:
!>[X0: $tType] : $o ).
tff(pred_def_9,type,
ord_less:
!>[X0: $tType] : ( ( X0 * X0 ) > $o ) ).
tff(pred_def_10,type,
ord_less_eq:
!>[X0: $tType] : ( ( X0 * X0 ) > $o ) ).
tff(pred_def_11,type,
pp: bool > $o ).
tff(f1,axiom,
ord_less_eq(int,minus_minus(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),m1),zero_zero(int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0__0961_A_L_Aint_An_A_N_Am1_A_060_061_A0_096) ).
tff(f5,axiom,
! [X0: $tType] :
( ( number_ring(X0)
& linordered_idom(X0) )
=> ! [X1: int] :
( ord_less_eq(X0,one_one(X0),number_number_of(X0,X1))
<=> ord_less_eq(int,bit1(pls),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_le__special_I2_J) ).
tff(f7,axiom,
! [X0: $tType] :
( number_ring(X0)
=> ( plus_plus(X0,one_one(X0),one_one(X0)) = number_number_of(X0,bit0(bit1(pls))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_one__add__one__is__two) ).
tff(f10,axiom,
! [X0: int,X1: int] : ( times_times(int,bit1(X1),X0) = plus_plus(int,bit0(times_times(int,X1,X0)),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_mult__Bit1) ).
tff(f11,axiom,
! [X0: $tType] :
( number_ring(X0)
=> ( number_number_of(X0,bit1(pls)) = one_one(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_numeral__1__eq__1) ).
tff(f21,axiom,
! [X0: $tType] :
( linord219039673up_add(X0)
=> ! [X1: X0] :
( ( plus_plus(X0,X1,X1) = zero_zero(X0) )
<=> ( X1 = zero_zero(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_double__eq__0__iff) ).
tff(f28,axiom,
bit0(pls) = pls,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_Bit0__Pls) ).
tff(f35,axiom,
! [X0: int] : ( times_times(int,pls,X0) = pls ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_mult__Pls) ).
tff(f36,axiom,
! [X0: int,X1: int] : ( times_times(int,bit0(X1),X0) = bit0(times_times(int,X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_mult__Bit0) ).
tff(f37,axiom,
! [X0: int,X1: int] : ( plus_plus(int,bit0(X1),bit0(X0)) = bit0(plus_plus(int,X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_add__Bit0__Bit0) ).
tff(f41,axiom,
! [X0: $tType] :
( number_ring(X0)
=> ( number_number_of(X0,pls) = zero_zero(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_number__of__Pls) ).
tff(f43,axiom,
! [X0: $tType] :
( ( number(X0)
& ring(X0) )
=> ! [X1: X0,X2: X0,X3: int] : ( times_times(X0,number_number_of(X0,X3),minus_minus(X0,X2,X1)) = minus_minus(X0,times_times(X0,number_number_of(X0,X3),X2),times_times(X0,number_number_of(X0,X3),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_right__diff__distrib__number__of) ).
tff(f45,axiom,
! [X0: $tType] :
( ( number_ring(X0)
& linordered_idom(X0) )
=> ! [X1: int,X2: int] :
( ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
<=> ord_less_eq(int,X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_le__number__of) ).
tff(f47,axiom,
! [X0: $tType] :
( number_ring(X0)
=> ! [X1: int,X2: int] : ( times_times(X0,number_number_of(X0,X2),number_number_of(X0,X1)) = number_number_of(X0,times_times(int,X2,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_arith__simps_I32_J) ).
tff(f53,axiom,
! [X0: int] :
( ord_less(int,pls,bit0(X0))
<=> ord_less(int,pls,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_rel__simps_I4_J) ).
tff(f64,axiom,
! [X0: int,X1: int] :
( ord_less(int,X1,plus_plus(int,X0,one_one(int)))
<=> ord_less_eq(int,X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_zle__add1__eq__le) ).
tff(f67,axiom,
! [X0: $tType] :
( ( number_ring(X0)
& linordered_idom(X0) )
=> ! [X1: int] :
( ord_less(X0,zero_zero(X0),number_number_of(X0,X1))
<=> ord_less(int,pls,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_less__special_I1_J) ).
tff(f69,axiom,
! [X0: $tType] :
( ( number_ring(X0)
& linordered_idom(X0) )
=> ! [X1: int] :
( ord_less(X0,one_one(X0),number_number_of(X0,X1))
<=> ord_less(int,bit1(pls),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_less__special_I2_J) ).
tff(f72,axiom,
! [X0: int,X1: int] :
( ord_less(int,X1,X0)
<=> ( ord_less_eq(int,X1,X0)
& ( X1 != X0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_less__int__def) ).
tff(f73,axiom,
! [X0: int,X1: int] :
( ord_less(int,number_number_of(int,X1),number_number_of(int,X0))
<=> ord_less(int,X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_less__number__of__int__code) ).
tff(f75,axiom,
! [X0: $tType] :
( ( number(X0)
& linorder(X0) )
=> ! [X1: int,X2: int] :
( ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
<=> ~ ord_less(X0,number_number_of(X0,X1),number_number_of(X0,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_le__number__of__eq__not__less) ).
tff(f80,axiom,
! [X0: int,X1: int,X2: int] :
( ord_less(int,X2,X1)
=> ( ord_less(int,zero_zero(int),X0)
=> ord_less(int,times_times(int,X0,X2),times_times(int,X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_zmult__zless__mono2) ).
tff(f81,axiom,
! [X0: int,X1: int] :
( ord_less(int,X1,plus_plus(int,X0,one_one(int)))
<=> ( ord_less(int,X1,X0)
| ( X1 = X0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_zless__add1__eq) ).
tff(f82,axiom,
! [X0: int,X1: int] :
( ord_less(int,X1,X0)
<=> ord_less(int,minus_minus(int,X1,X0),zero_zero(int)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_less__bin__lemma) ).
tff(f87,axiom,
semiring_1_of_nat(int,one_one(nat)) = one_one(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_int__1) ).
tff(f89,axiom,
semiring_1_of_nat(int,zero_zero(nat)) = zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_int__0) ).
tff(f92,axiom,
! [X0: int] :
( ord_less_eq(int,one_one(int),X0)
<=> ord_less(int,zero_zero(int),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_int__one__le__iff__zero__less) ).
tff(f93,axiom,
! [X0: int,X1: int] :
( ord_less(int,zero_zero(int),X1)
=> ( ( times_times(int,X1,X0) = one_one(int) )
<=> ( ( X1 = one_one(int) )
& ( X0 = one_one(int) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_pos__zmult__eq__1__iff) ).
tff(f97,axiom,
! [X0: nat] :
( ord_less_eq(int,semiring_1_of_nat(int,X0),zero_zero(int))
<=> ( X0 = zero_zero(nat) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_int__le__0__conv) ).
tff(f99,axiom,
linord219039673up_add(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Groups_Olinordered__ab__group__add) ).
tff(f100,axiom,
linordered_idom(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Olinordered__idom) ).
tff(f101,axiom,
linorder(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Orderings_Olinorder) ).
tff(f103,axiom,
number_ring(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Int_Onumber__ring) ).
tff(f105,axiom,
ring(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Oring) ).
tff(f106,axiom,
number(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Int_Onumber) ).
tff(f113,conjecture,
ord_less_eq(int,minus_minus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m1)),zero_zero(int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
tff(f114,negated_conjecture,
~ ord_less_eq(int,minus_minus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m1)),zero_zero(int)),
inference(negated_conjecture,[status(cth)],[f113]) ).
tff(f115,plain,
~ ord_less_eq(int,minus_minus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m1)),zero_zero(int)),
inference(flattening,[],[f114]) ).
tff(f118,plain,
! [X0: $tType] :
( ! [X1: int] :
( ord_less_eq(X0,one_one(X0),number_number_of(X0,X1))
<=> ord_less_eq(int,bit1(pls),X1) )
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(ennf_transformation,[],[f5]) ).
tff(f119,plain,
! [X0: $tType] :
( ! [X1: int] :
( ord_less_eq(X0,one_one(X0),number_number_of(X0,X1))
<=> ord_less_eq(int,bit1(pls),X1) )
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(flattening,[],[f118]) ).
tff(f122,plain,
! [X0: $tType] :
( ( plus_plus(X0,one_one(X0),one_one(X0)) = number_number_of(X0,bit0(bit1(pls))) )
| ~ number_ring(X0) ),
inference(ennf_transformation,[],[f7]) ).
tff(f127,plain,
! [X0: $tType] :
( ( number_number_of(X0,bit1(pls)) = one_one(X0) )
| ~ number_ring(X0) ),
inference(ennf_transformation,[],[f11]) ).
tff(f130,plain,
! [X0: $tType] :
( ! [X1: X0] :
( ( plus_plus(X0,X1,X1) = zero_zero(X0) )
<=> ( X1 = zero_zero(X0) ) )
| ~ linord219039673up_add(X0) ),
inference(ennf_transformation,[],[f21]) ).
tff(f135,plain,
! [X0: $tType] :
( ( number_number_of(X0,pls) = zero_zero(X0) )
| ~ number_ring(X0) ),
inference(ennf_transformation,[],[f41]) ).
tff(f138,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0,X3: int] : ( times_times(X0,number_number_of(X0,X3),minus_minus(X0,X2,X1)) = minus_minus(X0,times_times(X0,number_number_of(X0,X3),X2),times_times(X0,number_number_of(X0,X3),X1)) )
| ~ number(X0)
| ~ ring(X0) ),
inference(ennf_transformation,[],[f43]) ).
tff(f139,plain,
! [X0: $tType] :
( ! [X1: X0,X2: X0,X3: int] : ( times_times(X0,number_number_of(X0,X3),minus_minus(X0,X2,X1)) = minus_minus(X0,times_times(X0,number_number_of(X0,X3),X2),times_times(X0,number_number_of(X0,X3),X1)) )
| ~ number(X0)
| ~ ring(X0) ),
inference(flattening,[],[f138]) ).
tff(f142,plain,
! [X0: $tType] :
( ! [X1: int,X2: int] :
( ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
<=> ord_less_eq(int,X2,X1) )
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(ennf_transformation,[],[f45]) ).
tff(f143,plain,
! [X0: $tType] :
( ! [X1: int,X2: int] :
( ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
<=> ord_less_eq(int,X2,X1) )
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(flattening,[],[f142]) ).
tff(f145,plain,
! [X0: $tType] :
( ! [X1: int,X2: int] : ( times_times(X0,number_number_of(X0,X2),number_number_of(X0,X1)) = number_number_of(X0,times_times(int,X2,X1)) )
| ~ number_ring(X0) ),
inference(ennf_transformation,[],[f47]) ).
tff(f150,plain,
! [X0: $tType] :
( ! [X1: int] :
( ord_less(X0,zero_zero(X0),number_number_of(X0,X1))
<=> ord_less(int,pls,X1) )
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(ennf_transformation,[],[f67]) ).
tff(f151,plain,
! [X0: $tType] :
( ! [X1: int] :
( ord_less(X0,zero_zero(X0),number_number_of(X0,X1))
<=> ord_less(int,pls,X1) )
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(flattening,[],[f150]) ).
tff(f154,plain,
! [X0: $tType] :
( ! [X1: int] :
( ord_less(X0,one_one(X0),number_number_of(X0,X1))
<=> ord_less(int,bit1(pls),X1) )
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(ennf_transformation,[],[f69]) ).
tff(f155,plain,
! [X0: $tType] :
( ! [X1: int] :
( ord_less(X0,one_one(X0),number_number_of(X0,X1))
<=> ord_less(int,bit1(pls),X1) )
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(flattening,[],[f154]) ).
tff(f157,plain,
! [X0: $tType] :
( ! [X1: int,X2: int] :
( ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
<=> ~ ord_less(X0,number_number_of(X0,X1),number_number_of(X0,X2)) )
| ~ number(X0)
| ~ linorder(X0) ),
inference(ennf_transformation,[],[f75]) ).
tff(f158,plain,
! [X0: $tType] :
( ! [X1: int,X2: int] :
( ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
<=> ~ ord_less(X0,number_number_of(X0,X1),number_number_of(X0,X2)) )
| ~ number(X0)
| ~ linorder(X0) ),
inference(flattening,[],[f157]) ).
tff(f159,plain,
! [X0: int,X1: int,X2: int] :
( ord_less(int,times_times(int,X0,X2),times_times(int,X0,X1))
| ~ ord_less(int,zero_zero(int),X0)
| ~ ord_less(int,X2,X1) ),
inference(ennf_transformation,[],[f80]) ).
tff(f160,plain,
! [X0: int,X1: int,X2: int] :
( ord_less(int,times_times(int,X0,X2),times_times(int,X0,X1))
| ~ ord_less(int,zero_zero(int),X0)
| ~ ord_less(int,X2,X1) ),
inference(flattening,[],[f159]) ).
tff(f161,plain,
! [X0: int,X1: int] :
( ( ( times_times(int,X1,X0) = one_one(int) )
<=> ( ( X1 = one_one(int) )
& ( X0 = one_one(int) ) ) )
| ~ ord_less(int,zero_zero(int),X1) ),
inference(ennf_transformation,[],[f93]) ).
tff(f164,plain,
! [X0: $tType] :
( ! [X1: int] :
( ( ord_less_eq(X0,one_one(X0),number_number_of(X0,X1))
| ~ ord_less_eq(int,bit1(pls),X1) )
& ( ord_less_eq(int,bit1(pls),X1)
| ~ ord_less_eq(X0,one_one(X0),number_number_of(X0,X1)) ) )
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(nnf_transformation,[],[f119]) ).
tff(f171,plain,
! [X0: $tType] :
( ! [X1: X0] :
( ( ( plus_plus(X0,X1,X1) = zero_zero(X0) )
| ( zero_zero(X0) != X1 ) )
& ( ( X1 = zero_zero(X0) )
| ( zero_zero(X0) != plus_plus(X0,X1,X1) ) ) )
| ~ linord219039673up_add(X0) ),
inference(nnf_transformation,[],[f130]) ).
tff(f179,plain,
! [X0: $tType] :
( ! [X1: int,X2: int] :
( ( ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
| ~ ord_less_eq(int,X2,X1) )
& ( ord_less_eq(int,X2,X1)
| ~ ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1)) ) )
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(nnf_transformation,[],[f143]) ).
tff(f183,plain,
! [X0: int] :
( ( ord_less(int,pls,bit0(X0))
| ~ ord_less(int,pls,X0) )
& ( ord_less(int,pls,X0)
| ~ ord_less(int,pls,bit0(X0)) ) ),
inference(nnf_transformation,[],[f53]) ).
tff(f192,plain,
! [X0: int,X1: int] :
( ( ord_less(int,X1,plus_plus(int,X0,one_one(int)))
| ~ ord_less_eq(int,X1,X0) )
& ( ord_less_eq(int,X1,X0)
| ~ ord_less(int,X1,plus_plus(int,X0,one_one(int))) ) ),
inference(nnf_transformation,[],[f64]) ).
tff(f195,plain,
! [X0: $tType] :
( ! [X1: int] :
( ( ord_less(X0,zero_zero(X0),number_number_of(X0,X1))
| ~ ord_less(int,pls,X1) )
& ( ord_less(int,pls,X1)
| ~ ord_less(X0,zero_zero(X0),number_number_of(X0,X1)) ) )
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(nnf_transformation,[],[f151]) ).
tff(f197,plain,
! [X0: $tType] :
( ! [X1: int] :
( ( ord_less(X0,one_one(X0),number_number_of(X0,X1))
| ~ ord_less(int,bit1(pls),X1) )
& ( ord_less(int,bit1(pls),X1)
| ~ ord_less(X0,one_one(X0),number_number_of(X0,X1)) ) )
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(nnf_transformation,[],[f155]) ).
tff(f200,plain,
! [X0: int,X1: int] :
( ( ord_less(int,X1,X0)
| ~ ord_less_eq(int,X1,X0)
| ( X0 = X1 ) )
& ( ( ord_less_eq(int,X1,X0)
& ( X1 != X0 ) )
| ~ ord_less(int,X1,X0) ) ),
inference(nnf_transformation,[],[f72]) ).
tff(f201,plain,
! [X0: int,X1: int] :
( ( ord_less(int,X1,X0)
| ~ ord_less_eq(int,X1,X0)
| ( X0 = X1 ) )
& ( ( ord_less_eq(int,X1,X0)
& ( X1 != X0 ) )
| ~ ord_less(int,X1,X0) ) ),
inference(flattening,[],[f200]) ).
tff(f202,plain,
! [X0: int,X1: int] :
( ( ord_less(int,number_number_of(int,X1),number_number_of(int,X0))
| ~ ord_less(int,X1,X0) )
& ( ord_less(int,X1,X0)
| ~ ord_less(int,number_number_of(int,X1),number_number_of(int,X0)) ) ),
inference(nnf_transformation,[],[f73]) ).
tff(f204,plain,
! [X0: $tType] :
( ! [X1: int,X2: int] :
( ( ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
| ord_less(X0,number_number_of(X0,X1),number_number_of(X0,X2)) )
& ( ~ ord_less(X0,number_number_of(X0,X1),number_number_of(X0,X2))
| ~ ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1)) ) )
| ~ number(X0)
| ~ linorder(X0) ),
inference(nnf_transformation,[],[f158]) ).
tff(f208,plain,
! [X0: int,X1: int] :
( ( ord_less(int,X1,plus_plus(int,X0,one_one(int)))
| ( ~ ord_less(int,X1,X0)
& ( X0 != X1 ) ) )
& ( ord_less(int,X1,X0)
| ( X1 = X0 )
| ~ ord_less(int,X1,plus_plus(int,X0,one_one(int))) ) ),
inference(nnf_transformation,[],[f81]) ).
tff(f209,plain,
! [X0: int,X1: int] :
( ( ord_less(int,X1,plus_plus(int,X0,one_one(int)))
| ( ~ ord_less(int,X1,X0)
& ( X0 != X1 ) ) )
& ( ord_less(int,X1,X0)
| ( X1 = X0 )
| ~ ord_less(int,X1,plus_plus(int,X0,one_one(int))) ) ),
inference(flattening,[],[f208]) ).
tff(f210,plain,
! [X0: int,X1: int] :
( ( ord_less(int,X1,X0)
| ~ ord_less(int,minus_minus(int,X1,X0),zero_zero(int)) )
& ( ord_less(int,minus_minus(int,X1,X0),zero_zero(int))
| ~ ord_less(int,X1,X0) ) ),
inference(nnf_transformation,[],[f82]) ).
tff(f215,plain,
! [X0: int] :
( ( ord_less_eq(int,one_one(int),X0)
| ~ ord_less(int,zero_zero(int),X0) )
& ( ord_less(int,zero_zero(int),X0)
| ~ ord_less_eq(int,one_one(int),X0) ) ),
inference(nnf_transformation,[],[f92]) ).
tff(f216,plain,
! [X0: int,X1: int] :
( ( ( ( times_times(int,X1,X0) = one_one(int) )
| ( one_one(int) != X1 )
| ( one_one(int) != X0 ) )
& ( ( ( X1 = one_one(int) )
& ( X0 = one_one(int) ) )
| ( one_one(int) != times_times(int,X1,X0) ) ) )
| ~ ord_less(int,zero_zero(int),X1) ),
inference(nnf_transformation,[],[f161]) ).
tff(f217,plain,
! [X0: int,X1: int] :
( ( ( ( times_times(int,X1,X0) = one_one(int) )
| ( one_one(int) != X1 )
| ( one_one(int) != X0 ) )
& ( ( ( X1 = one_one(int) )
& ( X0 = one_one(int) ) )
| ( one_one(int) != times_times(int,X1,X0) ) ) )
| ~ ord_less(int,zero_zero(int),X1) ),
inference(flattening,[],[f216]) ).
tff(f220,plain,
! [X0: nat] :
( ( ord_less_eq(int,semiring_1_of_nat(int,X0),zero_zero(int))
| ( zero_zero(nat) != X0 ) )
& ( ( X0 = zero_zero(nat) )
| ~ ord_less_eq(int,semiring_1_of_nat(int,X0),zero_zero(int)) ) ),
inference(nnf_transformation,[],[f97]) ).
tff(f221,plain,
ord_less_eq(int,minus_minus(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),m1),zero_zero(int)),
inference(cnf_transformation,[],[f1]) ).
tff(f226,plain,
! [X0: $tType,X1: int] :
( ord_less_eq(X0,one_one(X0),number_number_of(X0,X1))
| ~ ord_less_eq(int,bit1(pls),X1)
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(cnf_transformation,[],[f164]) ).
tff(f229,plain,
! [X0: $tType] :
( ~ number_ring(X0)
| ( plus_plus(X0,one_one(X0),one_one(X0)) = number_number_of(X0,bit0(bit1(pls))) ) ),
inference(cnf_transformation,[],[f122]) ).
tff(f234,plain,
! [X0: int,X1: int] : ( times_times(int,bit1(X1),X0) = plus_plus(int,bit0(times_times(int,X1,X0)),X0) ),
inference(cnf_transformation,[],[f10]) ).
tff(f235,plain,
! [X0: $tType] :
( ~ number_ring(X0)
| ( one_one(X0) = number_number_of(X0,bit1(pls)) ) ),
inference(cnf_transformation,[],[f127]) ).
tff(f249,plain,
! [X0: $tType,X1: X0] :
( ( zero_zero(X0) = plus_plus(X0,X1,X1) )
| ( zero_zero(X0) != X1 )
| ~ linord219039673up_add(X0) ),
inference(cnf_transformation,[],[f171]) ).
tff(f258,plain,
pls = bit0(pls),
inference(cnf_transformation,[],[f28]) ).
tff(f269,plain,
! [X0: int] : ( pls = times_times(int,pls,X0) ),
inference(cnf_transformation,[],[f35]) ).
tff(f270,plain,
! [X0: int,X1: int] : ( bit0(times_times(int,X1,X0)) = times_times(int,bit0(X1),X0) ),
inference(cnf_transformation,[],[f36]) ).
tff(f271,plain,
! [X0: int,X1: int] : ( plus_plus(int,bit0(X1),bit0(X0)) = bit0(plus_plus(int,X1,X0)) ),
inference(cnf_transformation,[],[f37]) ).
tff(f275,plain,
! [X0: $tType] :
( ~ number_ring(X0)
| ( zero_zero(X0) = number_number_of(X0,pls) ) ),
inference(cnf_transformation,[],[f135]) ).
tff(f277,plain,
! [X0: $tType,X2: X0,X3: int,X1: X0] :
( ~ ring(X0)
| ~ number(X0)
| ( times_times(X0,number_number_of(X0,X3),minus_minus(X0,X2,X1)) = minus_minus(X0,times_times(X0,number_number_of(X0,X3),X2),times_times(X0,number_number_of(X0,X3),X1)) ) ),
inference(cnf_transformation,[],[f139]) ).
tff(f280,plain,
! [X0: $tType,X2: int,X1: int] :
( ~ ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
| ord_less_eq(int,X2,X1)
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(cnf_transformation,[],[f179]) ).
tff(f281,plain,
! [X0: $tType,X2: int,X1: int] :
( ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
| ~ ord_less_eq(int,X2,X1)
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(cnf_transformation,[],[f179]) ).
tff(f283,plain,
! [X0: $tType,X2: int,X1: int] :
( ~ number_ring(X0)
| ( times_times(X0,number_number_of(X0,X2),number_number_of(X0,X1)) = number_number_of(X0,times_times(int,X2,X1)) ) ),
inference(cnf_transformation,[],[f145]) ).
tff(f293,plain,
! [X0: int] :
( ord_less(int,pls,bit0(X0))
| ~ ord_less(int,pls,X0) ),
inference(cnf_transformation,[],[f183]) ).
tff(f312,plain,
! [X0: int,X1: int] :
( ~ ord_less(int,X1,plus_plus(int,X0,one_one(int)))
| ord_less_eq(int,X1,X0) ),
inference(cnf_transformation,[],[f192]) ).
tff(f318,plain,
! [X0: $tType,X1: int] :
( ~ ord_less(X0,zero_zero(X0),number_number_of(X0,X1))
| ord_less(int,pls,X1)
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(cnf_transformation,[],[f195]) ).
tff(f322,plain,
! [X0: $tType,X1: int] :
( ~ ord_less(X0,one_one(X0),number_number_of(X0,X1))
| ord_less(int,bit1(pls),X1)
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(cnf_transformation,[],[f197]) ).
tff(f328,plain,
! [X0: int,X1: int] :
( ( X0 != X1 )
| ~ ord_less(int,X1,X0) ),
inference(cnf_transformation,[],[f201]) ).
tff(f329,plain,
! [X0: int,X1: int] :
( ~ ord_less(int,X1,X0)
| ord_less_eq(int,X1,X0) ),
inference(cnf_transformation,[],[f201]) ).
tff(f330,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq(int,X1,X0)
| ord_less(int,X1,X0)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f201]) ).
tff(f331,plain,
! [X0: int,X1: int] :
( ~ ord_less(int,number_number_of(int,X1),number_number_of(int,X0))
| ord_less(int,X1,X0) ),
inference(cnf_transformation,[],[f202]) ).
tff(f332,plain,
! [X0: int,X1: int] :
( ord_less(int,number_number_of(int,X1),number_number_of(int,X0))
| ~ ord_less(int,X1,X0) ),
inference(cnf_transformation,[],[f202]) ).
tff(f335,plain,
! [X0: $tType,X2: int,X1: int] :
( ~ ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
| ~ ord_less(X0,number_number_of(X0,X1),number_number_of(X0,X2))
| ~ number(X0)
| ~ linorder(X0) ),
inference(cnf_transformation,[],[f204]) ).
tff(f336,plain,
! [X0: $tType,X2: int,X1: int] :
( ord_less_eq(X0,number_number_of(X0,X2),number_number_of(X0,X1))
| ord_less(X0,number_number_of(X0,X1),number_number_of(X0,X2))
| ~ number(X0)
| ~ linorder(X0) ),
inference(cnf_transformation,[],[f204]) ).
tff(f344,plain,
! [X2: int,X0: int,X1: int] :
( ord_less(int,times_times(int,X0,X2),times_times(int,X0,X1))
| ~ ord_less(int,zero_zero(int),X0)
| ~ ord_less(int,X2,X1) ),
inference(cnf_transformation,[],[f160]) ).
tff(f346,plain,
! [X0: int,X1: int] :
( ord_less(int,X1,plus_plus(int,X0,one_one(int)))
| ( X0 != X1 ) ),
inference(cnf_transformation,[],[f209]) ).
tff(f348,plain,
! [X0: int,X1: int] :
( ord_less(int,minus_minus(int,X1,X0),zero_zero(int))
| ~ ord_less(int,X1,X0) ),
inference(cnf_transformation,[],[f210]) ).
tff(f349,plain,
! [X0: int,X1: int] :
( ~ ord_less(int,minus_minus(int,X1,X0),zero_zero(int))
| ord_less(int,X1,X0) ),
inference(cnf_transformation,[],[f210]) ).
tff(f355,plain,
one_one(int) = semiring_1_of_nat(int,one_one(nat)),
inference(cnf_transformation,[],[f87]) ).
tff(f358,plain,
zero_zero(int) = semiring_1_of_nat(int,zero_zero(nat)),
inference(cnf_transformation,[],[f89]) ).
tff(f363,plain,
! [X0: int] :
( ~ ord_less_eq(int,one_one(int),X0)
| ord_less(int,zero_zero(int),X0) ),
inference(cnf_transformation,[],[f215]) ).
tff(f364,plain,
! [X0: int] :
( ~ ord_less(int,zero_zero(int),X0)
| ord_less_eq(int,one_one(int),X0) ),
inference(cnf_transformation,[],[f215]) ).
tff(f365,plain,
! [X0: int,X1: int] :
( ( one_one(int) != times_times(int,X1,X0) )
| ( one_one(int) = X0 )
| ~ ord_less(int,zero_zero(int),X1) ),
inference(cnf_transformation,[],[f217]) ).
tff(f367,plain,
! [X0: int,X1: int] :
( ( one_one(int) = times_times(int,X1,X0) )
| ( one_one(int) != X1 )
| ( one_one(int) != X0 )
| ~ ord_less(int,zero_zero(int),X1) ),
inference(cnf_transformation,[],[f217]) ).
tff(f373,plain,
! [X0: nat] :
( ~ ord_less_eq(int,semiring_1_of_nat(int,X0),zero_zero(int))
| ( zero_zero(nat) = X0 ) ),
inference(cnf_transformation,[],[f220]) ).
tff(f376,plain,
linord219039673up_add(int),
inference(cnf_transformation,[],[f99]) ).
tff(f377,plain,
linordered_idom(int),
inference(cnf_transformation,[],[f100]) ).
tff(f378,plain,
linorder(int),
inference(cnf_transformation,[],[f101]) ).
tff(f380,plain,
number_ring(int),
inference(cnf_transformation,[],[f103]) ).
tff(f382,plain,
ring(int),
inference(cnf_transformation,[],[f105]) ).
tff(f383,plain,
number(int),
inference(cnf_transformation,[],[f106]) ).
tff(f390,plain,
~ ord_less_eq(int,minus_minus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m1)),zero_zero(int)),
inference(cnf_transformation,[],[f115]) ).
tff(f394,plain,
! [X0: $tType] :
( ~ linord219039673up_add(X0)
| ( zero_zero(X0) = plus_plus(X0,zero_zero(X0),zero_zero(X0)) ) ),
inference(equality_resolution,[],[f249]) ).
tff(f397,plain,
! [X1: int] : ~ ord_less(int,X1,X1),
inference(equality_resolution,[],[f328]) ).
tff(f398,plain,
! [X1: int] : ord_less(int,X1,plus_plus(int,X1,one_one(int))),
inference(equality_resolution,[],[f346]) ).
tff(f400,plain,
! [X0: int] :
( ( one_one(int) = times_times(int,one_one(int),X0) )
| ( one_one(int) != X0 )
| ~ ord_less(int,zero_zero(int),one_one(int)) ),
inference(equality_resolution,[],[f367]) ).
tff(f401,plain,
( ( one_one(int) = times_times(int,one_one(int),one_one(int)) )
| ~ ord_less(int,zero_zero(int),one_one(int)) ),
inference(equality_resolution,[],[f400]) ).
tff(f404,definition,
( spl0_1
<=> ord_less(int,zero_zero(int),one_one(int)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
tff(f405,plain,
( ord_less(int,zero_zero(int),one_one(int))
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f404]) ).
tff(f406,plain,
( ~ ord_less(int,zero_zero(int),one_one(int))
| spl0_1 ),
inference(avatar_component_clause,[],[f404]) ).
tff(f408,definition,
( spl0_2
<=> ( one_one(int) = times_times(int,one_one(int),one_one(int)) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
tff(f410,plain,
( ( one_one(int) = times_times(int,one_one(int),one_one(int)) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f408]) ).
tff(f411,plain,
( ~ spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f401,f408,f404]) ).
tff(f412,plain,
! [X0: int,X1: int] : ( times_times(int,bit1(X1),X0) = plus_plus(int,times_times(int,bit0(X1),X0),X0) ),
inference(forward_demodulation,[],[f234,f270]) ).
tff(f419,plain,
zero_zero(int) = number_number_of(int,pls),
inference(resolution,[],[f275,f380]) ).
tff(f423,plain,
one_one(int) = number_number_of(int,bit1(pls)),
inference(resolution,[],[f235,f380]) ).
tff(f473,definition,
( spl0_3
<=> ( zero_zero(nat) = one_one(nat) ) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
tff(f475,plain,
( ( zero_zero(nat) = one_one(nat) )
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f473]) ).
tff(f477,definition,
( spl0_4
<=> ( one_one(int) = zero_zero(int) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
tff(f478,plain,
( ( one_one(int) = zero_zero(int) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f477]) ).
tff(f479,plain,
( ( one_one(int) != zero_zero(int) )
| spl0_4 ),
inference(avatar_component_clause,[],[f477]) ).
tff(f492,plain,
ord_less_eq(int,one_one(int),plus_plus(int,zero_zero(int),one_one(int))),
inference(resolution,[],[f364,f398]) ).
tff(f593,plain,
( ord_less(int,one_one(int),plus_plus(int,zero_zero(int),one_one(int)))
| ( one_one(int) = plus_plus(int,zero_zero(int),one_one(int)) ) ),
inference(resolution,[],[f492,f330]) ).
tff(f595,definition,
( spl0_5
<=> ( one_one(int) = plus_plus(int,zero_zero(int),one_one(int)) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
tff(f596,plain,
( ( one_one(int) != plus_plus(int,zero_zero(int),one_one(int)) )
| spl0_5 ),
inference(avatar_component_clause,[],[f595]) ).
tff(f597,plain,
( ( one_one(int) = plus_plus(int,zero_zero(int),one_one(int)) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f595]) ).
tff(f599,definition,
( spl0_6
<=> ord_less(int,one_one(int),plus_plus(int,zero_zero(int),one_one(int))) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
tff(f601,plain,
( ord_less(int,one_one(int),plus_plus(int,zero_zero(int),one_one(int)))
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f599]) ).
tff(f602,plain,
( spl0_5
| spl0_6 ),
inference(avatar_split_clause,[],[f593,f599,f595]) ).
tff(f608,plain,
( ord_less(int,zero_zero(int),one_one(int))
| ~ spl0_5 ),
inference(superposition,[],[f398,f597]) ).
tff(f609,plain,
( $false
| spl0_1
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f608,f406]) ).
tff(f610,plain,
( spl0_1
| ~ spl0_5 ),
inference(avatar_contradiction_clause,[],[f609]) ).
tff(f617,plain,
( ~ ord_less_eq(int,one_one(int),zero_zero(int))
| ( zero_zero(nat) = one_one(nat) ) ),
inference(superposition,[],[f373,f355]) ).
tff(f619,definition,
( spl0_7
<=> ord_less_eq(int,one_one(int),zero_zero(int)) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
tff(f621,plain,
( ~ ord_less_eq(int,one_one(int),zero_zero(int))
| spl0_7 ),
inference(avatar_component_clause,[],[f619]) ).
tff(f622,plain,
( spl0_3
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f617,f619,f473]) ).
tff(f623,plain,
zero_zero(int) = plus_plus(int,zero_zero(int),zero_zero(int)),
inference(resolution,[],[f394,f376]) ).
tff(f630,plain,
! [X0: int] : ( bit0(plus_plus(int,pls,X0)) = plus_plus(int,pls,bit0(X0)) ),
inference(superposition,[],[f271,f258]) ).
tff(f671,plain,
( ord_less_eq(int,one_one(int),zero_zero(int))
| ~ spl0_6 ),
inference(resolution,[],[f312,f601]) ).
tff(f673,plain,
( $false
| ~ spl0_6
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f671,f621]) ).
tff(f674,plain,
( ~ spl0_6
| spl0_7 ),
inference(avatar_contradiction_clause,[],[f673]) ).
tff(f684,plain,
( ( zero_zero(int) = semiring_1_of_nat(int,one_one(nat)) )
| ~ spl0_3 ),
inference(superposition,[],[f358,f475]) ).
tff(f686,plain,
( ( one_one(int) = zero_zero(int) )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f684,f355]) ).
tff(f688,plain,
( $false
| ~ spl0_3
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f686,f479]) ).
tff(f689,plain,
( ~ spl0_3
| spl0_4 ),
inference(avatar_contradiction_clause,[],[f688]) ).
tff(f702,plain,
( ord_less(int,one_one(int),one_one(int))
| ~ spl0_1
| ~ spl0_4 ),
inference(superposition,[],[f405,f478]) ).
tff(f709,plain,
( ( one_one(int) != plus_plus(int,one_one(int),one_one(int)) )
| ~ spl0_4
| spl0_5 ),
inference(superposition,[],[f596,f478]) ).
tff(f711,plain,
( ( one_one(int) = plus_plus(int,one_one(int),one_one(int)) )
| ~ spl0_4 ),
inference(superposition,[],[f623,f478]) ).
tff(f715,plain,
( $false
| ~ spl0_4
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f709,f711]) ).
tff(f716,plain,
( ~ spl0_4
| spl0_5 ),
inference(avatar_contradiction_clause,[],[f715]) ).
tff(f717,plain,
( $false
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f702,f397]) ).
tff(f718,plain,
( ~ spl0_1
| ~ spl0_4 ),
inference(avatar_contradiction_clause,[],[f717]) ).
tff(f736,plain,
! [X0: int] :
( ord_less(int,zero_zero(int),number_number_of(int,X0))
| ~ ord_less(int,pls,X0) ),
inference(superposition,[],[f332,f419]) ).
tff(f746,plain,
! [X0: int,X1: int] :
( ord_less_eq(int,minus_minus(int,X0,X1),zero_zero(int))
| ~ ord_less(int,X0,X1) ),
inference(resolution,[],[f348,f329]) ).
tff(f794,plain,
( ord_less(int,minus_minus(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),m1),zero_zero(int))
| ( minus_minus(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),m1) = zero_zero(int) ) ),
inference(resolution,[],[f221,f330]) ).
tff(f809,plain,
plus_plus(int,one_one(int),one_one(int)) = number_number_of(int,bit0(bit1(pls))),
inference(resolution,[],[f229,f380]) ).
tff(f832,plain,
! [X0: int] : ( times_times(int,bit1(pls),X0) = plus_plus(int,times_times(int,pls,X0),X0) ),
inference(superposition,[],[f412,f258]) ).
tff(f844,plain,
! [X0: int] : ( plus_plus(int,pls,X0) = times_times(int,bit1(pls),X0) ),
inference(forward_demodulation,[],[f832,f269]) ).
tff(f893,plain,
! [X0: int] : ( bit0(plus_plus(int,pls,X0)) = times_times(int,bit0(bit1(pls)),X0) ),
inference(superposition,[],[f270,f844]) ).
tff(f894,plain,
! [X0: int] : ( plus_plus(int,pls,bit0(X0)) = times_times(int,bit0(bit1(pls)),X0) ),
inference(forward_demodulation,[],[f893,f630]) ).
tff(f970,plain,
! [X0: int] :
( ~ ord_less_eq(int,bit1(pls),X0)
| ~ number_ring(int)
| ~ linordered_idom(int)
| ord_less(int,zero_zero(int),number_number_of(int,X0)) ),
inference(resolution,[],[f226,f363]) ).
tff(f977,plain,
! [X0: int] :
( ~ ord_less_eq(int,bit1(pls),X0)
| ~ linordered_idom(int)
| ord_less(int,zero_zero(int),number_number_of(int,X0)) ),
inference(forward_subsumption_resolution,[],[f970,f380]) ).
tff(f979,plain,
! [X0: int] :
( ord_less(int,zero_zero(int),number_number_of(int,X0))
| ~ ord_less_eq(int,bit1(pls),X0) ),
inference(forward_subsumption_resolution,[],[f977,f377]) ).
tff(f1183,plain,
! [X0: int,X1: int] : ( times_times(int,number_number_of(int,X0),number_number_of(int,X1)) = number_number_of(int,times_times(int,X0,X1)) ),
inference(resolution,[],[f283,f380]) ).
tff(f1260,plain,
( ! [X0: int] :
( ord_less(int,times_times(int,one_one(int),X0),one_one(int))
| ~ ord_less(int,zero_zero(int),one_one(int))
| ~ ord_less(int,X0,one_one(int)) )
| ~ spl0_2 ),
inference(superposition,[],[f344,f410]) ).
tff(f1262,plain,
( ! [X0: int] :
( ord_less(int,times_times(int,one_one(int),X0),one_one(int))
| ~ ord_less(int,X0,one_one(int)) )
| ~ spl0_1
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f1260,f405]) ).
tff(f1275,plain,
! [X0: $tType,X2: int,X1: int] :
( ~ ord_less(X0,number_number_of(X0,X1),number_number_of(X0,X2))
| ~ number(X0)
| ~ linorder(X0)
| ~ ord_less_eq(int,X2,X1)
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(resolution,[],[f335,f281]) ).
tff(f1293,plain,
! [X0: $tType,X2: int,X1: int] :
( ord_less(X0,number_number_of(X0,X1),number_number_of(X0,X2))
| ~ number(X0)
| ~ linorder(X0)
| ord_less_eq(int,X2,X1)
| ~ number_ring(X0)
| ~ linordered_idom(X0) ),
inference(resolution,[],[f336,f280]) ).
tff(f1457,plain,
! [X2: int,X0: int,X1: int] :
( ~ number(int)
| ( times_times(int,number_number_of(int,X0),minus_minus(int,X1,X2)) = minus_minus(int,times_times(int,number_number_of(int,X0),X1),times_times(int,number_number_of(int,X0),X2)) ) ),
inference(resolution,[],[f277,f382]) ).
tff(f1458,plain,
! [X2: int,X0: int,X1: int] : ( times_times(int,number_number_of(int,X0),minus_minus(int,X1,X2)) = minus_minus(int,times_times(int,number_number_of(int,X0),X1),times_times(int,number_number_of(int,X0),X2)) ),
inference(forward_subsumption_resolution,[],[f1457,f383]) ).
tff(f1603,plain,
~ ord_less(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m1)),
inference(resolution,[],[f746,f390]) ).
tff(f1633,definition,
( spl0_24
<=> ord_less(int,zero_zero(int),number_number_of(int,bit0(bit0(bit1(pls))))) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
tff(f1634,plain,
( ord_less(int,zero_zero(int),number_number_of(int,bit0(bit0(bit1(pls)))))
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f1633]) ).
tff(f1635,plain,
( ~ ord_less(int,zero_zero(int),number_number_of(int,bit0(bit0(bit1(pls)))))
| spl0_24 ),
inference(avatar_component_clause,[],[f1633]) ).
tff(f1703,plain,
ord_less(int,one_one(int),number_number_of(int,bit0(bit1(pls)))),
inference(superposition,[],[f398,f809]) ).
tff(f1719,plain,
! [X0: int] :
( ~ ord_less_eq(int,bit1(pls),X0)
| ord_less(int,pls,X0)
| ~ number_ring(int)
| ~ linordered_idom(int) ),
inference(resolution,[],[f979,f318]) ).
tff(f1722,plain,
! [X0: int] :
( ~ ord_less_eq(int,bit1(pls),X0)
| ord_less(int,pls,X0)
| ~ linordered_idom(int) ),
inference(forward_subsumption_resolution,[],[f1719,f380]) ).
tff(f1723,plain,
! [X0: int] :
( ~ ord_less_eq(int,bit1(pls),X0)
| ord_less(int,pls,X0) ),
inference(forward_subsumption_resolution,[],[f1722,f377]) ).
tff(f1729,plain,
( ord_less(int,bit1(pls),bit0(bit1(pls)))
| ~ number_ring(int)
| ~ linordered_idom(int) ),
inference(resolution,[],[f1703,f322]) ).
tff(f1730,plain,
( ord_less(int,bit1(pls),bit0(bit1(pls)))
| ~ linordered_idom(int) ),
inference(forward_subsumption_resolution,[],[f1729,f380]) ).
tff(f1731,plain,
ord_less(int,bit1(pls),bit0(bit1(pls))),
inference(forward_subsumption_resolution,[],[f1730,f377]) ).
tff(f1738,plain,
ord_less_eq(int,bit1(pls),bit0(bit1(pls))),
inference(resolution,[],[f1731,f329]) ).
tff(f1855,plain,
ord_less(int,pls,bit0(bit1(pls))),
inference(resolution,[],[f1723,f1738]) ).
tff(f2728,plain,
! [X0: int] : ( number_number_of(int,times_times(int,X0,pls)) = times_times(int,number_number_of(int,X0),zero_zero(int)) ),
inference(superposition,[],[f1183,f419]) ).
tff(f4394,plain,
! [X0: int,X1: int] :
( ~ number(int)
| ~ linorder(int)
| ~ ord_less_eq(int,X0,X1)
| ~ number_ring(int)
| ~ linordered_idom(int)
| ~ ord_less(int,X1,X0) ),
inference(resolution,[],[f1275,f332]) ).
tff(f4414,definition,
( spl0_44
<=> ! [X2: int,X1: int] :
( ~ ord_less_eq(int,X1,X2)
| ~ ord_less(int,X2,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
tff(f4415,plain,
( ! [X2: int,X1: int] :
( ~ ord_less_eq(int,X1,X2)
| ~ ord_less(int,X2,X1) )
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f4414]) ).
tff(f4420,plain,
! [X0: int,X1: int] :
( ~ linorder(int)
| ~ ord_less_eq(int,X0,X1)
| ~ number_ring(int)
| ~ linordered_idom(int)
| ~ ord_less(int,X1,X0) ),
inference(forward_subsumption_resolution,[],[f4394,f383]) ).
tff(f4430,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq(int,X0,X1)
| ~ number_ring(int)
| ~ linordered_idom(int)
| ~ ord_less(int,X1,X0) ),
inference(forward_subsumption_resolution,[],[f4420,f378]) ).
tff(f4440,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq(int,X0,X1)
| ~ linordered_idom(int)
| ~ ord_less(int,X1,X0) ),
inference(forward_subsumption_resolution,[],[f4430,f380]) ).
tff(f4450,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq(int,X0,X1)
| ~ ord_less(int,X1,X0) ),
inference(forward_subsumption_resolution,[],[f4440,f377]) ).
tff(f4452,plain,
spl0_44,
inference(avatar_split_clause,[],[f4450,f4414]) ).
tff(f4548,plain,
! [X0: int,X1: int] :
( ~ number(int)
| ~ linorder(int)
| ord_less_eq(int,X0,X1)
| ~ number_ring(int)
| ~ linordered_idom(int)
| ord_less(int,X1,X0) ),
inference(resolution,[],[f1293,f331]) ).
tff(f4573,definition,
( spl0_46
<=> ! [X2: int,X1: int] :
( ord_less_eq(int,X1,X2)
| ord_less(int,X2,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
tff(f4574,plain,
( ! [X2: int,X1: int] :
( ord_less_eq(int,X1,X2)
| ord_less(int,X2,X1) )
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f4573]) ).
tff(f4577,plain,
! [X0: int,X1: int] :
( ~ linorder(int)
| ord_less_eq(int,X0,X1)
| ~ number_ring(int)
| ~ linordered_idom(int)
| ord_less(int,X1,X0) ),
inference(forward_subsumption_resolution,[],[f4548,f383]) ).
tff(f4587,plain,
! [X0: int,X1: int] :
( ord_less_eq(int,X0,X1)
| ~ number_ring(int)
| ~ linordered_idom(int)
| ord_less(int,X1,X0) ),
inference(forward_subsumption_resolution,[],[f4577,f378]) ).
tff(f4597,plain,
! [X0: int,X1: int] :
( ord_less_eq(int,X0,X1)
| ~ linordered_idom(int)
| ord_less(int,X1,X0) ),
inference(forward_subsumption_resolution,[],[f4587,f380]) ).
tff(f4607,plain,
! [X0: int,X1: int] :
( ord_less_eq(int,X0,X1)
| ord_less(int,X1,X0) ),
inference(forward_subsumption_resolution,[],[f4597,f377]) ).
tff(f4608,plain,
spl0_46,
inference(avatar_split_clause,[],[f4607,f4573]) ).
tff(f5186,plain,
~ ord_less_eq(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),minus_minus(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),m1)),zero_zero(int)),
inference(superposition,[],[f390,f1458]) ).
tff(f5625,plain,
( ~ ord_less(int,pls,bit0(bit0(bit1(pls))))
| spl0_24 ),
inference(resolution,[],[f1635,f736]) ).
tff(f5641,plain,
( ~ ord_less(int,pls,bit0(bit1(pls)))
| spl0_24 ),
inference(resolution,[],[f5625,f293]) ).
tff(f5642,plain,
( $false
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f5641,f1855]) ).
tff(f5643,plain,
spl0_24,
inference(avatar_contradiction_clause,[],[f5642]) ).
tff(f6344,plain,
! [X0: int] : ( times_times(int,bit0(bit0(bit1(pls))),X0) = bit0(plus_plus(int,pls,bit0(X0))) ),
inference(superposition,[],[f270,f894]) ).
tff(f6359,plain,
! [X0: int] : ( times_times(int,bit0(bit0(bit1(pls))),X0) = plus_plus(int,pls,bit0(bit0(X0))) ),
inference(forward_demodulation,[],[f6344,f630]) ).
tff(f6763,definition,
( spl0_77
<=> ord_less(int,one_one(int),number_number_of(int,plus_plus(int,pls,pls))) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
tff(f6764,plain,
( ~ ord_less(int,one_one(int),number_number_of(int,plus_plus(int,pls,pls)))
| spl0_77 ),
inference(avatar_component_clause,[],[f6763]) ).
tff(f6765,plain,
( ord_less(int,one_one(int),number_number_of(int,plus_plus(int,pls,pls)))
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f6763]) ).
tff(f6867,plain,
( ord_less_eq(int,one_one(int),number_number_of(int,plus_plus(int,pls,pls)))
| ~ spl0_77 ),
inference(resolution,[],[f6765,f329]) ).
tff(f6876,plain,
( ~ ord_less(int,number_number_of(int,plus_plus(int,pls,pls)),one_one(int))
| ~ spl0_44
| ~ spl0_77 ),
inference(resolution,[],[f6867,f4415]) ).
tff(f8743,plain,
times_times(int,one_one(int),zero_zero(int)) = number_number_of(int,times_times(int,bit1(pls),pls)),
inference(superposition,[],[f2728,f423]) ).
tff(f8764,plain,
times_times(int,one_one(int),zero_zero(int)) = number_number_of(int,plus_plus(int,pls,pls)),
inference(forward_demodulation,[],[f8743,f844]) ).
tff(f9429,definition,
( spl0_102
<=> ( minus_minus(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),m1) = zero_zero(int) ) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
tff(f9431,plain,
( ( minus_minus(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),m1) = zero_zero(int) )
| ~ spl0_102 ),
inference(avatar_component_clause,[],[f9429]) ).
tff(f9433,definition,
( spl0_103
<=> ord_less(int,minus_minus(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),m1),zero_zero(int)) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
tff(f9435,plain,
( ord_less(int,minus_minus(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),m1),zero_zero(int))
| ~ spl0_103 ),
inference(avatar_component_clause,[],[f9433]) ).
tff(f9436,plain,
( spl0_102
| spl0_103 ),
inference(avatar_split_clause,[],[f794,f9433,f9429]) ).
tff(f9438,plain,
( ~ ord_less(int,times_times(int,one_one(int),zero_zero(int)),one_one(int))
| ~ spl0_44
| ~ spl0_77 ),
inference(forward_demodulation,[],[f6876,f8764]) ).
tff(f9468,plain,
( ord_less(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),m1)
| ~ spl0_103 ),
inference(resolution,[],[f9435,f349]) ).
tff(f9474,plain,
( ~ ord_less(int,zero_zero(int),number_number_of(int,bit0(bit0(bit1(pls)))))
| ~ ord_less(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),m1) ),
inference(resolution,[],[f1603,f344]) ).
tff(f9475,plain,
( ~ ord_less(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),m1)
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f9474,f1634]) ).
tff(f9476,plain,
( $false
| ~ spl0_24
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f9475,f9468]) ).
tff(f9477,plain,
( ~ spl0_24
| ~ spl0_103 ),
inference(avatar_contradiction_clause,[],[f9476]) ).
tff(f9480,plain,
( ~ ord_less_eq(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),zero_zero(int)),zero_zero(int))
| ~ spl0_102 ),
inference(superposition,[],[f5186,f9431]) ).
tff(f9503,plain,
( ~ ord_less_eq(int,number_number_of(int,times_times(int,bit0(bit0(bit1(pls))),pls)),zero_zero(int))
| ~ spl0_102 ),
inference(forward_demodulation,[],[f9480,f2728]) ).
tff(f9504,plain,
( ~ ord_less_eq(int,number_number_of(int,plus_plus(int,pls,bit0(bit0(pls)))),zero_zero(int))
| ~ spl0_102 ),
inference(forward_demodulation,[],[f9503,f6359]) ).
tff(f9505,plain,
( ~ ord_less_eq(int,number_number_of(int,plus_plus(int,pls,bit0(pls))),zero_zero(int))
| ~ spl0_102 ),
inference(forward_demodulation,[],[f9504,f258]) ).
tff(f9506,plain,
( ~ ord_less_eq(int,number_number_of(int,plus_plus(int,pls,pls)),zero_zero(int))
| ~ spl0_102 ),
inference(forward_demodulation,[],[f9505,f258]) ).
tff(f9507,plain,
( ~ ord_less_eq(int,times_times(int,one_one(int),zero_zero(int)),zero_zero(int))
| ~ spl0_102 ),
inference(forward_demodulation,[],[f9506,f8764]) ).
tff(f9548,plain,
( ord_less(int,zero_zero(int),times_times(int,one_one(int),zero_zero(int)))
| ~ spl0_46
| ~ spl0_102 ),
inference(resolution,[],[f9507,f4574]) ).
tff(f9555,plain,
( ord_less_eq(int,one_one(int),times_times(int,one_one(int),zero_zero(int)))
| ~ spl0_46
| ~ spl0_102 ),
inference(resolution,[],[f9548,f364]) ).
tff(f9569,plain,
( ord_less(int,one_one(int),times_times(int,one_one(int),zero_zero(int)))
| ( one_one(int) = times_times(int,one_one(int),zero_zero(int)) )
| ~ spl0_46
| ~ spl0_102 ),
inference(resolution,[],[f9555,f330]) ).
tff(f9571,definition,
( spl0_106
<=> ( one_one(int) = times_times(int,one_one(int),zero_zero(int)) ) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
tff(f9573,plain,
( ( one_one(int) = times_times(int,one_one(int),zero_zero(int)) )
| ~ spl0_106 ),
inference(avatar_component_clause,[],[f9571]) ).
tff(f9575,definition,
( spl0_107
<=> ord_less(int,one_one(int),times_times(int,one_one(int),zero_zero(int))) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
tff(f9577,plain,
( ord_less(int,one_one(int),times_times(int,one_one(int),zero_zero(int)))
| ~ spl0_107 ),
inference(avatar_component_clause,[],[f9575]) ).
tff(f9578,plain,
( spl0_106
| spl0_107
| ~ spl0_46
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f9569,f9429,f4573,f9575,f9571]) ).
tff(f9642,plain,
( ~ ord_less(int,zero_zero(int),one_one(int))
| ~ spl0_1
| ~ spl0_2
| ~ spl0_44
| ~ spl0_77 ),
inference(resolution,[],[f9438,f1262]) ).
tff(f9643,plain,
( $false
| ~ spl0_1
| ~ spl0_2
| ~ spl0_44
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f9642,f405]) ).
tff(f9644,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_44
| ~ spl0_77 ),
inference(avatar_contradiction_clause,[],[f9643]) ).
tff(f9645,plain,
( ~ ord_less(int,one_one(int),times_times(int,one_one(int),zero_zero(int)))
| spl0_77 ),
inference(forward_demodulation,[],[f6764,f8764]) ).
tff(f9646,plain,
( $false
| spl0_77
| ~ spl0_107 ),
inference(forward_subsumption_resolution,[],[f9645,f9577]) ).
tff(f9647,plain,
( spl0_77
| ~ spl0_107 ),
inference(avatar_contradiction_clause,[],[f9646]) ).
tff(f9720,plain,
( ( one_one(int) != one_one(int) )
| ( one_one(int) = zero_zero(int) )
| ~ ord_less(int,zero_zero(int),one_one(int))
| ~ spl0_106 ),
inference(superposition,[],[f365,f9573]) ).
tff(f9723,plain,
( ( one_one(int) = zero_zero(int) )
| ~ ord_less(int,zero_zero(int),one_one(int))
| ~ spl0_106 ),
inference(trivial_inequality_removal,[],[f9720]) ).
tff(f9726,plain,
( ~ ord_less(int,zero_zero(int),one_one(int))
| spl0_4
| ~ spl0_106 ),
inference(forward_subsumption_resolution,[],[f9723,f479]) ).
tff(f9730,plain,
( $false
| ~ spl0_1
| spl0_4
| ~ spl0_106 ),
inference(forward_subsumption_resolution,[],[f9726,f405]) ).
tff(f9731,plain,
( ~ spl0_1
| spl0_4
| ~ spl0_106 ),
inference(avatar_contradiction_clause,[],[f9730]) ).
cnf(s1,plain,
( ~ spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f411]) ).
cnf(s3,plain,
( spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f602]) ).
cnf(s4,plain,
( spl0_1
| ~ spl0_5 ),
inference(sat_conversion,[],[f610]) ).
cnf(s5,plain,
( spl0_3
| ~ spl0_7 ),
inference(sat_conversion,[],[f622]) ).
cnf(s8,plain,
( ~ spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f674]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f689]) ).
cnf(s10,plain,
( ~ spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f716]) ).
cnf(s11,plain,
( ~ spl0_1
| ~ spl0_4 ),
inference(sat_conversion,[],[f718]) ).
cnf(s41,plain,
spl0_44,
inference(sat_conversion,[],[f4452]) ).
cnf(s43,plain,
spl0_46,
inference(sat_conversion,[],[f4608]) ).
cnf(s60,plain,
spl0_24,
inference(sat_conversion,[],[f5643]) ).
cnf(s109,plain,
( spl0_102
| spl0_103 ),
inference(sat_conversion,[],[f9436]) ).
cnf(s112,plain,
( ~ spl0_24
| ~ spl0_103 ),
inference(sat_conversion,[],[f9477]) ).
cnf(s113,plain,
( ~ spl0_46
| ~ spl0_102
| spl0_106
| spl0_107 ),
inference(sat_conversion,[],[f9578]) ).
cnf(s116,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_44
| ~ spl0_77 ),
inference(sat_conversion,[],[f9644]) ).
cnf(s117,plain,
( spl0_77
| ~ spl0_107 ),
inference(sat_conversion,[],[f9647]) ).
cnf(s118,plain,
( ~ spl0_1
| spl0_4
| ~ spl0_106 ),
inference(sat_conversion,[],[f9731]) ).
cnf(s123,plain,
~ spl0_103,
inference(rat,[],[s112,s60]) ).
cnf(s127,plain,
spl0_102,
inference(rat,[],[s109,s123]) ).
cnf(s132,plain,
spl0_5,
inference(rat,[],[s5,s8,s9,s3,s10]) ).
cnf(s135,plain,
spl0_1,
inference(rat,[],[s4,s132]) ).
cnf(s137,plain,
~ spl0_4,
inference(rat,[],[s11,s135]) ).
cnf(s138,plain,
spl0_2,
inference(rat,[],[s1,s135]) ).
cnf(s139,plain,
~ spl0_106,
inference(rat,[],[s118,s135,s137]) ).
cnf(s141,plain,
~ spl0_77,
inference(rat,[],[s116,s135,s41,s138]) ).
cnf(s142,plain,
spl0_107,
inference(rat,[],[s113,s43,s127,s139]) ).
cnf(s144,plain,
$false,
inference(rat,[],[s117,s142,s141]) ).
tff(f9734,plain,
$false,
inference(avatar_sat_refutation,[],[s144]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM989_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n015.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 21:52:46 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.43 Running first-order theorem proving
% 0.13/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.42/1.78 % (2041094)Detected formulas, will run a generic FOF schedule.
% 5.42/1.78 % (2041101)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=3583988441:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.42/1.78 % (2041101)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 5.42/1.78 % (2041099)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=135962277:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.42/1.78 % (2041102)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2554273691:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.42/1.78 % (2041100)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=1620745131:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.42/1.78 % (2041103)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=443365789:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.42/1.78 % (2041105)dis-21_1_sil=8000:lcm=predicate:random_seed=2566975568: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.42/1.78 % (2041102)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 5.42/1.78 % (2041104)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=801814232:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.42/1.78 % (2041102)Refutation not found, incomplete strategy
% 5.42/1.78 % (2041102)------------------------------
% 5.42/1.78 % (2041102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/1.78 % (2041102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.78 % (2041102)CaDiCaL version: 2.1.3
% 5.42/1.78 % (2041102)Termination reason: Refutation not found, incomplete strategy
% 5.42/1.78 % (2041102)Time elapsed: 0.007 s
% 5.42/1.78 % (2041102)Peak memory usage: 88 MB
% 5.42/1.78 % (2041102)Instructions burned: 10 (million)
% 5.42/1.78 % (2041104)Instruction limit reached!
% 5.42/1.78 % (2041104)------------------------------
% 5.42/1.78 % (2041104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/1.78 % (2041104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.78 % (2041104)CaDiCaL version: 2.1.3
% 5.42/1.78 % (2041104)Termination reason: Instruction limit
% 5.42/1.78 % (2041104)Termination phase: Saturation
% 5.42/1.78 % (2041104)Time elapsed: 0.049 s
% 5.42/1.78 % (2041104)Peak memory usage: 89 MB
% 5.42/1.78 % (2041104)Instructions burned: 140 (million)
% 5.42/1.78 % (2041103)Instruction limit reached!
% 5.42/1.78 % (2041103)------------------------------
% 5.42/1.78 % (2041103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/1.78 % (2041103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.78 % (2041103)CaDiCaL version: 2.1.3
% 5.42/1.78 % (2041103)Termination reason: Instruction limit
% 5.42/1.78 % (2041103)Termination phase: Saturation
% 5.42/1.78 % (2041103)Time elapsed: 0.071 s
% 5.42/1.78 % (2041103)Peak memory usage: 88 MB
% 5.42/1.78 % (2041103)Instructions burned: 120 (million)
% 5.42/1.78 % (2041105)Instruction limit reached!
% 5.42/1.78 % (2041105)------------------------------
% 5.42/1.78 % (2041105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.42/1.78 % (2041105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.78 % (2041105)CaDiCaL version: 2.1.3
% 5.42/1.78 % (2041105)Termination reason: Instruction limit
% 5.42/1.78 % (2041105)Termination phase: Saturation
% 5.42/1.78 % (2041105)Time elapsed: 0.075 s
% 5.42/1.78 % (2041105)Peak memory usage: 89 MB
% 5.42/1.78 % (2041105)Instructions burned: 131 (million)
% 5.42/1.78 % (2041113)lrs+10_1_sil=8000:sp=occurrence:random_seed=3872666419:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.42/1.78 % (2041114)lrs+10_1_sil=32000:urr=on:br=off:random_seed=308080909:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.42/1.78 % (2041115)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3572238405:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.42/1.78 % (2041102)------------------------------
% 8.54/2.12 % (2041102)------------------------------
% 8.54/2.12 % (2041113)Instruction limit reached!
% 8.54/2.12 % (2041113)------------------------------
% 8.54/2.12 % (2041113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.54/2.12 % (2041113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/2.12 % (2041113)CaDiCaL version: 2.1.3
% 8.54/2.12 % (2041113)Termination reason: Instruction limit
% 8.54/2.12 % (2041113)Termination phase: Saturation
% 8.54/2.12 % (2041113)Time elapsed: 0.093 s
% 8.54/2.12 % (2041113)Peak memory usage: 92 MB
% 8.54/2.12 % (2041113)Instructions burned: 285 (million)
% 8.54/2.12 % (2041114)Instruction limit reached!
% 8.54/2.12 % (2041114)------------------------------
% 8.54/2.12 % (2041114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.54/2.12 % (2041114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/2.12 % (2041114)CaDiCaL version: 2.1.3
% 8.54/2.12 % (2041114)Termination reason: Instruction limit
% 8.54/2.12 % (2041114)Termination phase: Saturation
% 8.54/2.12 % (2041114)Time elapsed: 0.088 s
% 8.54/2.12 % (2041114)Peak memory usage: 90 MB
% 8.54/2.12 % (2041114)Instructions burned: 157 (million)
% 8.54/2.12 % (2041101)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.54/2.12 % (2041101)------------------------------
% 8.54/2.12 % (2041101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.54/2.12 % (2041101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/2.12 % (2041101)CaDiCaL version: 2.1.3
% 8.54/2.12 % (2041101)Termination reason: Unknown
% 8.54/2.12 % (2041101)Termination phase: Saturation
% 8.54/2.12 % (2041101)Time elapsed: 0.363 s
% 8.54/2.12 % (2041101)Peak memory usage: 113 MB
% 8.54/2.12 % (2041101)Instructions burned: 540 (million)
% 8.54/2.12 % (2041099)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.54/2.12 % (2041100)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.54/2.12 % (2041099)------------------------------
% 8.54/2.12 % (2041099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.54/2.12 % (2041100)------------------------------
% 8.54/2.12 % (2041100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.54/2.12 % (2041099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/2.12 % (2041100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/2.12 % (2041100)CaDiCaL version: 2.1.3
% 8.54/2.12 % (2041099)CaDiCaL version: 2.1.3
% 8.54/2.12 % (2041099)Termination reason: Unknown
% 8.54/2.12 % (2041099)Termination phase: Saturation
% 8.54/2.12 % (2041100)Termination reason: Unknown
% 8.54/2.12 % (2041100)Termination phase: Saturation
% 8.54/2.12 % (2041099)Time elapsed: 0.364 s
% 8.54/2.12 % (2041100)Time elapsed: 0.364 s
% 8.54/2.12 % (2041099)Peak memory usage: 113 MB
% 8.54/2.12 % (2041100)Peak memory usage: 113 MB
% 8.54/2.12 % (2041099)Instructions burned: 541 (million)
% 8.54/2.12 % (2041100)Instructions burned: 544 (million)
% 8.54/2.12 % (2041120)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2543131412:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 8.54/2.12 % (2041119)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=524885639:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 8.54/2.12 % (2041120)Refutation not found, incomplete strategy
% 8.54/2.12 % (2041120)------------------------------
% 8.54/2.12 % (2041120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.54/2.12 % (2041120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/2.12 % (2041120)CaDiCaL version: 2.1.3
% 8.54/2.12 % (2041120)Termination reason: Refutation not found, incomplete strategy
% 8.54/2.12 % (2041120)Time elapsed: 0.006 s
% 8.54/2.12 % (2041120)Peak memory usage: 88 MB
% 8.54/2.12 % (2041120)Instructions burned: 20 (million)
% 8.54/2.12 % (2041115)Instruction limit reached!
% 8.54/2.12 % (2041115)------------------------------
% 8.54/2.12 % (2041115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.54/2.12 % (2041115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.54/2.12 % (2041115)CaDiCaL version: 2.1.3
% 8.54/2.12 % (2041115)Termination reason: Instruction limit
% 8.54/2.12 % (2041115)Termination phase: Saturation
% 8.54/2.12 % (2041115)Time elapsed: 0.214 s
% 8.54/2.12 % (2041115)Peak memory usage: 92 MB
% 9.66/2.32 % (2041115)Instructions burned: 325 (million)
% 9.66/2.32 % (2041121)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4085326533:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 9.66/2.32 % (2041122)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4209251781:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 9.66/2.32 % (2041123)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2355312124:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 9.66/2.32 % (2041124)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=917415729:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 9.66/2.32 % (2041119)Instruction limit reached!
% 9.66/2.32 % (2041119)------------------------------
% 9.66/2.32 % (2041119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.66/2.32 % (2041119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/2.32 % (2041119)CaDiCaL version: 2.1.3
% 9.66/2.32 % (2041119)Termination reason: Instruction limit
% 9.66/2.32 % (2041119)Termination phase: Saturation
% 9.66/2.32 % (2041119)Time elapsed: 0.152 s
% 9.66/2.32 % (2041119)Peak memory usage: 91 MB
% 9.66/2.32 % (2041119)Instructions burned: 249 (million)
% 9.66/2.32 % (2041122)Instruction limit reached!
% 9.66/2.32 % (2041122)------------------------------
% 9.66/2.32 % (2041122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.66/2.32 % (2041122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/2.32 % (2041122)CaDiCaL version: 2.1.3
% 9.66/2.32 % (2041122)Termination reason: Instruction limit
% 9.66/2.32 % (2041122)Termination phase: Saturation
% 9.66/2.32 % (2041122)Time elapsed: 0.071 s
% 9.66/2.32 % (2041122)Peak memory usage: 90 MB
% 9.66/2.32 % (2041122)Instructions burned: 114 (million)
% 9.66/2.32 % (2041120)------------------------------
% 9.66/2.32 % (2041120)------------------------------
% 9.66/2.32 % (2041123)Instruction limit reached!
% 9.66/2.32 % (2041123)------------------------------
% 9.66/2.32 % (2041123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.66/2.32 % (2041123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/2.32 % (2041123)CaDiCaL version: 2.1.3
% 9.66/2.32 % (2041123)Termination reason: Instruction limit
% 9.66/2.32 % (2041123)Termination phase: Saturation
% 9.66/2.32 % (2041123)Time elapsed: 0.054 s
% 9.66/2.32 % (2041123)Peak memory usage: 87 MB
% 9.66/2.32 % (2041123)Instructions burned: 128 (million)
% 9.66/2.32 % (2041124)Instruction limit reached!
% 9.66/2.32 % (2041124)------------------------------
% 9.66/2.32 % (2041124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.66/2.32 % (2041124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/2.32 % (2041124)CaDiCaL version: 2.1.3
% 9.66/2.32 % (2041124)Termination reason: Instruction limit
% 9.66/2.32 % (2041124)Termination phase: Saturation
% 9.66/2.32 % (2041124)Time elapsed: 0.057 s
% 9.66/2.32 % (2041124)Peak memory usage: 89 MB
% 9.66/2.32 % (2041124)Instructions burned: 115 (million)
% 9.66/2.32 % (2041128)lrs+10_1_sil=8000:sp=occurrence:random_seed=3655504643:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 9.66/2.32 % (2041134)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=248038698:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi)
% 9.66/2.32 % (2041133)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=195205309:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 9.66/2.32 % (2041132)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1683772039:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 9.66/2.32 % (2041132)Refutation not found, incomplete strategy
% 9.66/2.32 % (2041132)------------------------------
% 9.66/2.32 % (2041132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.66/2.32 % (2041132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.66/2.32 % (2041132)CaDiCaL version: 2.1.3
% 9.66/2.32 % (2041132)Termination reason: Refutation not found, incomplete strategy
% 9.66/2.32 % (2041132)Time elapsed: 0.008 s
% 9.66/2.32 % (2041132)Peak memory usage: 88 MB
% 9.66/2.32 % (2041132)Instructions burned: 12 (million)
% 9.66/2.32 % (2041134)Instruction limit reached!
% 11.39/2.66 % (2041134)------------------------------
% 11.39/2.66 % (2041134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.39/2.66 % (2041134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.39/2.66 % (2041134)CaDiCaL version: 2.1.3
% 11.39/2.66 % (2041134)Termination reason: Instruction limit
% 11.39/2.66 % (2041134)Termination phase: Saturation
% 11.39/2.66 % (2041134)Time elapsed: 0.045 s
% 11.39/2.66 % (2041134)Peak memory usage: 90 MB
% 11.39/2.66 % (2041134)Instructions burned: 135 (million)
% 11.39/2.66 % (2041136)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2650320795:st=3:i=13193:sd=3:ss=axioms_2992 on theBenchmark for (2992ds/13193Mi)
% 11.39/2.66 % (2041135)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=808451140:st=8:i=592:sd=3:ep=RST:ss=axioms_2992 on theBenchmark for (2992ds/592Mi)
% 11.39/2.66 % (2041135)Refutation not found, incomplete strategy
% 11.39/2.66 % (2041135)------------------------------
% 11.39/2.66 % (2041135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.39/2.66 % (2041135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.39/2.66 % (2041135)CaDiCaL version: 2.1.3
% 11.39/2.66 % (2041135)Termination reason: Refutation not found, incomplete strategy
% 11.39/2.66 % (2041135)Time elapsed: 0.006 s
% 11.39/2.66 % (2041135)Peak memory usage: 88 MB
% 11.39/2.66 % (2041135)Instructions burned: 9 (million)
% 11.39/2.66 % (2041121)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.39/2.66 % (2041121)------------------------------
% 11.39/2.66 % (2041121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.39/2.66 % (2041121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.39/2.66 % (2041121)CaDiCaL version: 2.1.3
% 11.39/2.66 % (2041121)Termination reason: Unknown
% 11.39/2.66 % (2041121)Termination phase: Saturation
% 11.39/2.66 % (2041121)Time elapsed: 0.367 s
% 11.39/2.66 % (2041121)Peak memory usage: 113 MB
% 11.39/2.66 % (2041121)Instructions burned: 540 (million)
% 11.39/2.66 % (2041141)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=2858359085:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/125Mi)
% 11.39/2.66 % (2041141)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 11.39/2.66 % (2041141)Instruction limit reached!
% 11.39/2.66 % (2041141)------------------------------
% 11.39/2.66 % (2041141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.39/2.66 % (2041141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.39/2.66 % (2041141)CaDiCaL version: 2.1.3
% 11.39/2.66 % (2041141)Termination reason: Instruction limit
% 11.39/2.66 % (2041141)Termination phase: Saturation
% 11.39/2.66 % (2041141)Time elapsed: 0.041 s
% 11.39/2.66 % (2041141)Peak memory usage: 90 MB
% 11.39/2.66 % (2041141)Instructions burned: 127 (million)
% 11.39/2.66 % (2041132)------------------------------
% 11.39/2.66 % (2041132)------------------------------
% 11.39/2.66 % (2041135)------------------------------
% 11.39/2.66 % (2041135)------------------------------
% 11.39/2.66 % (2041144)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3269058876:i=134:gtgl=5:slsql=off:gtg=exists_sym_2989 on theBenchmark for (2989ds/134Mi)
% 11.39/2.66 % (2041146)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2623340610:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/141Mi)
% 11.39/2.66 % (2041146)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 11.39/2.66 % (2041146)Refutation not found, incomplete strategy
% 11.39/2.66 % (2041146)------------------------------
% 11.39/2.66 % (2041146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.39/2.66 % (2041146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.39/2.66 % (2041146)CaDiCaL version: 2.1.3
% 11.39/2.66 % (2041146)Termination reason: Refutation not found, incomplete strategy
% 11.39/2.66 % (2041146)Time elapsed: 0.003 s
% 11.39/2.66 % (2041146)Peak memory usage: 88 MB
% 11.39/2.66 % (2041146)Instructions burned: 4 (million)
% 11.39/2.66 % (2041133)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.39/2.66 % (2041133)------------------------------
% 11.39/2.66 % (2041133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.56/3.07 % (2041133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.56/3.07 % (2041133)CaDiCaL version: 2.1.3
% 15.56/3.07 % (2041133)Termination reason: Unknown
% 15.56/3.07 % (2041133)Termination phase: Saturation
% 15.56/3.07 % (2041133)Time elapsed: 0.365 s
% 15.56/3.07 % (2041133)Peak memory usage: 113 MB
% 15.56/3.07 % (2041133)Instructions burned: 541 (million)
% 15.56/3.07 % (2041144)Instruction limit reached!
% 15.56/3.07 % (2041144)------------------------------
% 15.56/3.07 % (2041144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.56/3.07 % (2041144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.56/3.07 % (2041144)CaDiCaL version: 2.1.3
% 15.56/3.07 % (2041144)Termination reason: Instruction limit
% 15.56/3.07 % (2041144)Termination phase: Saturation
% 15.56/3.07 % (2041144)Time elapsed: 0.073 s
% 15.56/3.07 % (2041144)Peak memory usage: 89 MB
% 15.56/3.07 % (2041144)Instructions burned: 135 (million)
% 15.56/3.07 % (2041147)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3839150059:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2988 on theBenchmark for (2988ds/431Mi)
% 15.56/3.07 % (2041136)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.56/3.07 % (2041136)------------------------------
% 15.56/3.07 % (2041136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.56/3.07 % (2041136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.56/3.07 % (2041136)CaDiCaL version: 2.1.3
% 15.56/3.07 % (2041136)Termination reason: Unknown
% 15.56/3.07 % (2041136)Termination phase: Saturation
% 15.56/3.07 % (2041136)Time elapsed: 0.370 s
% 15.56/3.07 % (2041136)Peak memory usage: 113 MB
% 15.56/3.07 % (2041136)Instructions burned: 542 (million)
% 15.56/3.07 % (2041148)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=1789535435:i=6060:aac=none:ins=25_2988 on theBenchmark for (2988ds/6060Mi)
% 15.56/3.07 % (2041128)Instruction limit reached!
% 15.56/3.07 % (2041128)------------------------------
% 15.56/3.07 % (2041128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.56/3.07 % (2041128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.56/3.07 % (2041128)CaDiCaL version: 2.1.3
% 15.56/3.07 % (2041128)Termination reason: Instruction limit
% 15.56/3.07 % (2041128)Termination phase: Saturation
% 15.56/3.07 % (2041128)Time elapsed: 0.561 s
% 15.56/3.07 % (2041128)Peak memory usage: 98 MB
% 15.56/3.07 % (2041128)Instructions burned: 907 (million)
% 15.56/3.07 % (2041147)Instruction limit reached!
% 15.56/3.07 % (2041147)------------------------------
% 15.56/3.07 % (2041147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.56/3.07 % (2041147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.56/3.07 % (2041147)CaDiCaL version: 2.1.3
% 15.56/3.07 % (2041147)Termination reason: Instruction limit
% 15.56/3.07 % (2041147)Termination phase: Saturation
% 15.56/3.07 % (2041147)Time elapsed: 0.113 s
% 15.56/3.07 % (2041147)Peak memory usage: 92 MB
% 15.56/3.07 % (2041147)Instructions burned: 431 (million)
% 15.56/3.07 % (2041151)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=2426520036:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2987 on theBenchmark for (2987ds/150Mi)
% 15.56/3.07 % (2041151)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 15.56/3.07 % (2041153)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2169082524:i=14155:bd=all_2987 on theBenchmark for (2987ds/14155Mi)
% 15.56/3.07 % (2041154)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4021925005:i=667:av=off:fsr=off_2987 on theBenchmark for (2987ds/667Mi)
% 15.56/3.07 % (2041154)Refutation not found, incomplete strategy
% 15.56/3.07 % (2041154)------------------------------
% 15.56/3.07 % (2041154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.56/3.07 % (2041154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.56/3.07 % (2041154)CaDiCaL version: 2.1.3
% 15.56/3.07 % (2041154)Termination reason: Refutation not found, incomplete strategy
% 15.56/3.07 % (2041154)Time elapsed: 0.007 s
% 15.56/3.07 % (2041154)Peak memory usage: 88 MB
% 15.56/3.07 % (2041154)Instructions burned: 10 (million)
% 18.26/3.66 % (2041146)------------------------------
% 18.26/3.66 % (2041146)------------------------------
% 18.26/3.66 % (2041151)Instruction limit reached!
% 18.26/3.66 % (2041151)------------------------------
% 18.26/3.66 % (2041151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.26/3.66 % (2041151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.26/3.66 % (2041151)CaDiCaL version: 2.1.3
% 18.26/3.66 % (2041151)Termination reason: Instruction limit
% 18.26/3.66 % (2041151)Termination phase: Saturation
% 18.26/3.66 % (2041151)Time elapsed: 0.090 s
% 18.26/3.66 % (2041151)Peak memory usage: 90 MB
% 18.26/3.66 % (2041151)Instructions burned: 152 (million)
% 18.26/3.66 % (2041157)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=625431378:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2986 on theBenchmark for (2986ds/193Mi)
% 18.26/3.66 % (2041156)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=1461244141:s2a=on:i=185:s2at=1.8:fdi=4_2986 on theBenchmark for (2986ds/185Mi)
% 18.26/3.66 % (2041157)Instruction limit reached!
% 18.26/3.66 % (2041157)------------------------------
% 18.26/3.66 % (2041157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.26/3.66 % (2041157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.26/3.66 % (2041157)CaDiCaL version: 2.1.3
% 18.26/3.66 % (2041157)Termination reason: Instruction limit
% 18.26/3.66 % (2041157)Termination phase: Saturation
% 18.26/3.66 % (2041157)Time elapsed: 0.066 s
% 18.26/3.66 % (2041157)Peak memory usage: 91 MB
% 18.26/3.66 % (2041157)Instructions burned: 195 (million)
% 18.26/3.66 % (2041156)Instruction limit reached!
% 18.26/3.66 % (2041156)------------------------------
% 18.26/3.66 % (2041156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.26/3.66 % (2041156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.26/3.66 % (2041156)CaDiCaL version: 2.1.3
% 18.26/3.66 % (2041156)Termination reason: Instruction limit
% 18.26/3.66 % (2041156)Termination phase: Saturation
% 18.26/3.66 % (2041156)Time elapsed: 0.103 s
% 18.26/3.66 % (2041156)Peak memory usage: 90 MB
% 18.26/3.66 % (2041156)Instructions burned: 185 (million)
% 18.26/3.66 % (2041163)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3955866571:i=12111:sd=1:ss=included_2985 on theBenchmark for (2985ds/12111Mi)
% 18.26/3.66 % (2041161)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3456104182:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2985 on theBenchmark for (2985ds/4850Mi)
% 18.26/3.66 % (2041165)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3101483993:i=319:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/319Mi)
% 18.26/3.66 % (2041154)------------------------------
% 18.26/3.66 % (2041154)------------------------------
% 18.26/3.66 % (2041148)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.26/3.66 % (2041148)------------------------------
% 18.26/3.66 % (2041148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.26/3.66 % (2041148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.26/3.66 % (2041148)CaDiCaL version: 2.1.3
% 18.26/3.66 % (2041148)Termination reason: Unknown
% 18.26/3.66 % (2041148)Termination phase: Saturation
% 18.26/3.66 % (2041148)Time elapsed: 0.369 s
% 18.26/3.66 % (2041148)Peak memory usage: 114 MB
% 18.26/3.66 % (2041148)Instructions burned: 540 (million)
% 18.26/3.66 % (2041165)Instruction limit reached!
% 18.26/3.66 % (2041165)------------------------------
% 18.26/3.66 % (2041165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.26/3.66 % (2041165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.26/3.66 % (2041165)CaDiCaL version: 2.1.3
% 18.26/3.66 % (2041165)Termination reason: Instruction limit
% 18.26/3.66 % (2041165)Termination phase: Saturation
% 18.26/3.66 % (2041165)Time elapsed: 0.091 s
% 18.26/3.66 % (2041165)Peak memory usage: 92 MB
% 18.26/3.66 % (2041165)Instructions burned: 324 (million)
% 18.26/3.66 % (2041153)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.26/3.66 % (2041153)------------------------------
% 18.26/3.66 % (2041153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.26/3.66 % (2041153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.97/4.33 % (2041153)CaDiCaL version: 2.1.3
% 23.97/4.33 % (2041153)Termination reason: Unknown
% 23.97/4.33 % (2041153)Termination phase: Saturation
% 23.97/4.33 % (2041153)Time elapsed: 0.369 s
% 23.97/4.33 % (2041153)Peak memory usage: 114 MB
% 23.97/4.33 % (2041153)Instructions burned: 540 (million)
% 23.97/4.33 % (2041166)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=575983973:i=2064:ep=RST_2983 on theBenchmark for (2983ds/2064Mi)
% 23.97/4.33 % (2041166)Refutation not found, incomplete strategy
% 23.97/4.33 % (2041166)------------------------------
% 23.97/4.33 % (2041166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.97/4.33 % (2041166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.97/4.33 % (2041166)CaDiCaL version: 2.1.3
% 23.97/4.33 % (2041166)Termination reason: Refutation not found, incomplete strategy
% 23.97/4.33 % (2041166)Time elapsed: 0.005 s
% 23.97/4.33 % (2041166)Peak memory usage: 88 MB
% 23.97/4.33 % (2041166)Instructions burned: 9 (million)
% 23.97/4.33 % (2041170)dis-1011_128_sil=32000:random_seed=4140039304:i=3706:ep=RST:av=off_2983 on theBenchmark for (2983ds/3706Mi)
% 23.97/4.33 % (2041171)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1382767281:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2982 on theBenchmark for (2982ds/757Mi)
% 23.97/4.33 % (2041171)Refutation not found, incomplete strategy
% 23.97/4.33 % (2041171)------------------------------
% 23.97/4.33 % (2041171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.97/4.33 % (2041171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.97/4.33 % (2041171)CaDiCaL version: 2.1.3
% 23.97/4.33 % (2041171)Termination reason: Refutation not found, incomplete strategy
% 23.97/4.33 % (2041171)Time elapsed: 0.006 s
% 23.97/4.33 % (2041171)Peak memory usage: 88 MB
% 23.97/4.33 % (2041171)Instructions burned: 8 (million)
% 23.97/4.33 % (2041172)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1199000305:i=13913:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/13913Mi)
% 23.97/4.33 % (2041174)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2605075733:i=9925:aac=none_2982 on theBenchmark for (2982ds/9925Mi)
% 23.97/4.33 % (2041163)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 23.97/4.33 % (2041163)------------------------------
% 23.97/4.33 % (2041163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.97/4.33 % (2041163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.97/4.33 % (2041163)CaDiCaL version: 2.1.3
% 23.97/4.33 % (2041163)Termination reason: Unknown
% 23.97/4.33 % (2041163)Termination phase: Saturation
% 23.97/4.33 % (2041163)Time elapsed: 0.364 s
% 23.97/4.33 % (2041163)Peak memory usage: 113 MB
% 23.97/4.33 % (2041163)Instructions burned: 541 (million)
% 23.97/4.33 % (2041166)------------------------------
% 23.97/4.33 % (2041166)------------------------------
% 23.97/4.33 % (2041172)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 23.97/4.33 % (2041172)------------------------------
% 23.97/4.33 % (2041172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.97/4.33 % (2041172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.97/4.33 % (2041172)CaDiCaL version: 2.1.3
% 23.97/4.33 % (2041172)Termination reason: Unknown
% 23.97/4.33 % (2041172)Termination phase: Saturation
% 23.97/4.33 % (2041172)Time elapsed: 0.197 s
% 23.97/4.33 % (2041172)Peak memory usage: 113 MB
% 23.97/4.33 % (2041172)Instructions burned: 539 (million)
% 23.97/4.33 % (2041171)------------------------------
% 23.97/4.33 % (2041171)------------------------------
% 23.97/4.33 % (2041179)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=358076642:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2979 on theBenchmark for (2979ds/2479Mi)
% 23.97/4.33 % (2041179)Refutation not found, incomplete strategy
% 23.97/4.33 % (2041179)------------------------------
% 23.97/4.33 % (2041179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.97/4.33 % (2041179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.97/4.33 % (2041179)CaDiCaL version: 2.1.3
% 23.97/4.33 % (2041179)Termination reason: Refutation not found, incomplete strategy
% 23.97/4.33 % (2041179)Time elapsed: 0.007 s
% 23.97/4.33 % (2041179)Peak memory usage: 88 MB
% 23.97/4.33 % (2041179)Instructions burned: 10 (million)
% 23.97/4.33 % (2041181)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3335754065:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2979 on theBenchmark for (2979ds/11145Mi)
% 29.78/5.13 % (2041180)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3658884866:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2979 on theBenchmark for (2979ds/440Mi)
% 29.78/5.13 % (2041180)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 29.78/5.13 % (2041182)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=3351849112:cts=off:i=3034:av=off:er=known:fsd=on_2978 on theBenchmark for (2978ds/3034Mi)
% 29.78/5.13 % (2041174)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.78/5.13 % (2041174)------------------------------
% 29.78/5.13 % (2041174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.13 % (2041174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.13 % (2041174)CaDiCaL version: 2.1.3
% 29.78/5.13 % (2041174)Termination reason: Unknown
% 29.78/5.13 % (2041174)Termination phase: Saturation
% 29.78/5.13 % (2041174)Time elapsed: 0.362 s
% 29.78/5.13 % (2041174)Peak memory usage: 113 MB
% 29.78/5.13 % (2041174)Instructions burned: 540 (million)
% 29.78/5.13 % (2041181)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.78/5.13 % (2041181)------------------------------
% 29.78/5.13 % (2041181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.13 % (2041181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.13 % (2041181)CaDiCaL version: 2.1.3
% 29.78/5.13 % (2041181)Termination reason: Unknown
% 29.78/5.13 % (2041181)Termination phase: Saturation
% 29.78/5.13 % (2041181)Time elapsed: 0.196 s
% 29.78/5.13 % (2041181)Peak memory usage: 113 MB
% 29.78/5.13 % (2041181)Instructions burned: 541 (million)
% 29.78/5.13 % (2041179)------------------------------
% 29.78/5.13 % (2041179)------------------------------
% 29.78/5.13 % (2041180)Instruction limit reached!
% 29.78/5.13 % (2041180)------------------------------
% 29.78/5.13 % (2041180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.13 % (2041180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.13 % (2041180)CaDiCaL version: 2.1.3
% 29.78/5.13 % (2041180)Termination reason: Instruction limit
% 29.78/5.13 % (2041180)Termination phase: Saturation
% 29.78/5.13 % (2041180)Time elapsed: 0.238 s
% 29.78/5.13 % (2041180)Peak memory usage: 91 MB
% 29.78/5.13 % (2041180)Instructions burned: 441 (million)
% 29.78/5.13 % (2041187)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1350891620:st=2:s2a=on:i=524:s2at=2:ss=axioms_2976 on theBenchmark for (2976ds/524Mi)
% 29.78/5.13 % (2041188)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=990369557:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2976 on theBenchmark for (2976ds/1016Mi)
% 29.78/5.13 % (2041189)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2873952556:i=14123:bd=preordered:ins=4_2975 on theBenchmark for (2975ds/14123Mi)
% 29.78/5.13 % (2041190)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1123336933:i=5781:kws=precedence:bd=all:rawr=on_2975 on theBenchmark for (2975ds/5781Mi)
% 29.78/5.13 % (2041182)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.78/5.13 % (2041182)------------------------------
% 29.78/5.13 % (2041182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.13 % (2041182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.13 % (2041182)CaDiCaL version: 2.1.3
% 29.78/5.13 % (2041182)Termination reason: Unknown
% 29.78/5.13 % (2041182)Termination phase: Saturation
% 29.78/5.13 % (2041182)Time elapsed: 0.364 s
% 29.78/5.13 % (2041182)Peak memory usage: 113 MB
% 29.78/5.13 % (2041182)Instructions burned: 540 (million)
% 29.78/5.13 % (2041187)Instruction limit reached!
% 29.78/5.13 % (2041187)------------------------------
% 29.78/5.13 % (2041187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.13 % (2041187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.13 % (2041187)CaDiCaL version: 2.1.3
% 29.78/5.13 % (2041187)Termination reason: Instruction limit
% 29.78/5.13 % (2041187)Termination phase: Saturation
% 29.78/5.13 % (2041187)Time elapsed: 0.301 s
% 29.78/5.13 % (2041187)Peak memory usage: 94 MB
% 29.78/5.13 % (2041187)Instructions burned: 525 (million)
% 29.78/5.13 % (2041195)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=3614890797:i=2448:gtgl=5:bd=preordered:gtg=all_2973 on theBenchmark for (2973ds/2448Mi)
% 29.78/5.13 % (2041188)Instruction limit reached!
% 29.78/5.13 % (2041188)------------------------------
% 29.78/5.13 % (2041188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.13 % (2041188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.13 % (2041188)CaDiCaL version: 2.1.3
% 29.78/5.13 % (2041188)Termination reason: Instruction limit
% 29.78/5.13 % (2041188)Termination phase: Saturation
% 29.78/5.13 % (2041188)Time elapsed: 0.325 s
% 29.78/5.13 % (2041188)Peak memory usage: 100 MB
% 29.78/5.13 % (2041188)Instructions burned: 1018 (million)
% 29.78/5.13 % (2041189)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.78/5.13 % (2041189)------------------------------
% 29.78/5.13 % (2041189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.13 % (2041189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.13 % (2041189)CaDiCaL version: 2.1.3
% 29.78/5.13 % (2041189)Termination reason: Unknown
% 29.78/5.13 % (2041189)Termination phase: Saturation
% 29.78/5.13 % (2041189)Time elapsed: 0.359 s
% 29.78/5.13 % (2041189)Peak memory usage: 113 MB
% 29.78/5.13 % (2041189)Instructions burned: 540 (million)
% 29.78/5.13 % (2041196)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2813688159:i=3223:kws=precedence:fgj=on:av=off_2972 on theBenchmark for (2972ds/3223Mi)
% 29.78/5.13 % (2041198)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2644514318:st=5.6:i=2033:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/2033Mi)
% 29.78/5.13 % (2041199)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3237827763:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2970 on theBenchmark for (2970ds/2055Mi)
% 29.78/5.13 % (2041198)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.78/5.13 % (2041198)------------------------------
% 29.78/5.13 % (2041198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.13 % (2041198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.13 % (2041198)CaDiCaL version: 2.1.3
% 29.78/5.13 % (2041198)Termination reason: Unknown
% 29.78/5.13 % (2041198)Termination phase: Saturation
% 29.78/5.13 % (2041198)Time elapsed: 0.194 s
% 29.78/5.13 % (2041198)Peak memory usage: 113 MB
% 29.78/5.13 % (2041198)Instructions burned: 541 (million)
% 29.78/5.13 % (2041195)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.78/5.13 % (2041195)------------------------------
% 29.78/5.13 % (2041195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.13 % (2041195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.13 % (2041195)CaDiCaL version: 2.1.3
% 29.78/5.13 % (2041195)Termination reason: Unknown
% 29.78/5.13 % (2041195)Termination phase: Saturation
% 29.78/5.13 % (2041195)Time elapsed: 0.360 s
% 29.78/5.13 % (2041195)Peak memory usage: 113 MB
% 29.78/5.13 % (2041195)Instructions burned: 541 (million)
% 29.78/5.13 % (2041203)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=935885679:i=21611:sd=3:ss=axioms_2968 on theBenchmark for (2968ds/21611Mi)
% 29.78/5.13 % (2041196)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.78/5.13 % (2041196)------------------------------
% 29.78/5.13 % (2041196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.13 % (2041196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.13 % (2041196)CaDiCaL version: 2.1.3
% 29.78/5.13 % (2041196)Termination reason: Unknown
% 29.78/5.13 % (2041196)Termination phase: Saturation
% 29.78/5.13 % (2041196)Time elapsed: 0.362 s
% 29.78/5.13 % (2041196)Peak memory usage: 113 MB
% 29.78/5.13 % (2041196)Instructions burned: 540 (million)
% 29.78/5.13 % (2041204)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1673997652:i=4835:sd=13:ss=axioms:sgt=23_2968 on theBenchmark for (2968ds/4835Mi)
% 29.78/5.13 % (2041199)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.78/5.13 % (2041199)------------------------------
% 29.78/5.13 % (2041199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.13 % (2041199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.13 % (2041199)CaDiCaL version: 2.1.3
% 29.78/5.13 % (2041199)Termination reason: Unknown
% 29.78/5.13 % (2041199)Termination phase: Saturation
% 29.78/5.13 % (2041199)Time elapsed: 0.361 s
% 29.78/5.13 % (2041199)Peak memory usage: 113 MB
% 29.78/5.13 % (2041199)Instructions burned: 540 (million)
% 29.78/5.13 % (2041206)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=3572829417:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2966 on theBenchmark for (2966ds/797Mi)
% 29.78/5.13 % (2041203)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.78/5.13 % (2041203)------------------------------
% 29.78/5.13 % (2041203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.13 % (2041203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.13 % (2041203)CaDiCaL version: 2.1.3
% 29.78/5.13 % (2041203)Termination reason: Unknown
% 29.78/5.13 % (2041203)Termination phase: Saturation
% 29.78/5.13 % (2041203)Time elapsed: 0.194 s
% 29.78/5.13 % (2041203)Peak memory usage: 113 MB
% 29.78/5.13 % (2041203)Instructions burned: 540 (million)
% 29.78/5.13 % (2041210)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2707079491:i=6038:nm=6_2965 on theBenchmark for (2965ds/6038Mi)
% 29.78/5.13 % (2041209)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1893238332:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2965 on theBenchmark for (2965ds/2326Mi)
% 29.78/5.13 % (2041210)Aborted by signal SIGSEGV on /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.78/5.13 % (2041210)------------------------------
% 29.78/5.13 % (2041210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.13 % (2041210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.13 % (2041210)CaDiCaL version: 2.1.3
% 29.78/5.13 % (2041210)Termination reason: Unknown
% 29.78/5.13 % (2041210)Termination phase: Saturation
% 29.78/5.13 % (2041210)Time elapsed: 0.193 s
% 29.78/5.13 % (2041210)Peak memory usage: 113 MB
% 29.78/5.13 % (2041210)Instructions burned: 540 (million)
% 29.78/5.13 % (2041170)Instruction limit reached!
% 29.78/5.13 % (2041170)------------------------------
% 29.78/5.13 % (2041170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.13 % (2041170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.13 % (2041170)CaDiCaL version: 2.1.3
% 29.78/5.13 % (2041170)Termination reason: Instruction limit
% 29.78/5.13 % (2041170)Termination phase: Saturation
% 29.78/5.13 % (2041170)Time elapsed: 2.004 s
% 29.78/5.13 % (2041170)Peak memory usage: 102 MB
% 29.78/5.13 % (2041170)Instructions burned: 3708 (million)
% 29.78/5.13 % (2041213)lrs+10_1_sil=32000:sp=occurrence:random_seed=3691914295:st=2:i=33334:sd=3:ss=included:sgt=32_2962 on theBenchmark for (2962ds/33334Mi)
% 29.78/5.13 % (2041206)Instruction limit reached!
% 29.78/5.13 % (2041206)------------------------------
% 29.78/5.13 % (2041206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.78/5.13 % (2041206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.78/5.13 % (2041206)CaDiCaL version: 2.1.3
% 29.78/5.13 % (2041206)Termination reason: Instruction limit
% 29.78/5.13 % (2041206)Termination phase: Saturation
% 29.78/5.13 % (2041206)Time elapsed: 0.533 s
% 29.78/5.13 % (2041206)Peak memory usage: 103 MB
% 29.78/5.13 % (2041206)Instructions burned: 797 (million)
% 29.78/5.13 % (2041214)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1783809907:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2961 on theBenchmark for (2961ds/1008Mi)
% 29.78/5.13 % (2041213)First to succeed.
% 29.78/5.13 % (2041213)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2041094"
% 29.78/5.13 % (2041216)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=1094367675:i=8327:s2at=5:bd=preordered_2960 on theBenchmark for (2960ds/8327Mi)
% 29.78/5.13 % (2041213)Refutation found. Thanks to Tanya!
% 29.78/5.13 % SZS status Theorem for theBenchmark
% 29.78/5.13 % SZS output start Proof for theBenchmark
% See solution above
% 30.64/5.32 % (2041213)------------------------------
% 30.64/5.32 % (2041213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.64/5.32 % (2041213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.64/5.32 % (2041213)CaDiCaL version: 2.1.3
% 30.64/5.32 % (2041213)Termination reason: Refutation
% 30.64/5.32 % (2041213)Time elapsed: 0.154 s
% 30.64/5.32 % (2041213)Peak memory usage: 95 MB
% 30.64/5.32 % (2041213)Instructions burned: 452 (million)
% 30.64/5.32 % (2041213)------------------------------
% 30.64/5.32 % (2041213)------------------------------
% 30.64/5.32 % (2041094)Success in time 4.248 s
% 30.64/5.32 % Vampire exiting
%------------------------------------------------------------------------------