%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP026^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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 : Wed Sep 30 08:08:01 AM UTC 2026
% Result : Theorem 3.13s 0.84s
% Output : Refutation 3.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 19
% Syntax : Number of formulae : 144 ( 88 unt; 0 typ; 6 def)
% Number of atoms : 514 ( 185 equ; 0 cnn)
% Maximal formula atoms : 5 ( 3 avg)
% Number of connectives : 733 ( 50 ~; 69 |; 0 &; 527 @)
% ( 6 <=>; 41 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 20 ( 19 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 133 ( 128 usr; 25 con; 0-5 aty)
% ( 33 !!; 7 ??; 0 @@+; 0 @@-)
% Number of variables : 133 ( 0 sgn 74 !; 2 ?; 133 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
carrie377329159t_unit: $tType ).
thf(type_def_6,type,
carrie292259835t_unit: $tType ).
thf(type_def_7,type,
carrie1065537299t_unit: $tType ).
thf(type_def_8,type,
carrie980467975t_unit: $tType ).
thf(type_def_9,type,
carrie1963041556t_unit: $tType ).
thf(type_def_10,type,
carrie1821755406_e_b_f: $tType ).
thf(type_def_11,type,
carrie722926983_a_b_c: $tType ).
thf(type_def_12,type,
carrie1950868226xt_b_d: $tType ).
thf(type_def_13,type,
set_nat_e: $tType ).
thf(type_def_14,type,
set_nat_b: $tType ).
thf(type_def_15,type,
set_nat_a: $tType ).
thf(type_def_16,type,
set_nat: $tType ).
thf(type_def_17,type,
set_e: $tType ).
thf(type_def_18,type,
set_b: $tType ).
thf(type_def_19,type,
set_a: $tType ).
thf(type_def_20,type,
nat: $tType ).
thf(type_def_21,type,
e: $tType ).
thf(type_def_22,type,
b: $tType ).
thf(type_def_23,type,
a: $tType ).
thf(type_def_24,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
carrie1074654371t_unit: carrie1963041556t_unit > set_a ).
thf(func_def_1,type,
carrie2021454486_a_b_c: carrie722926983_a_b_c > set_a ).
thf(func_def_2,type,
carrie2079586589xt_b_d: carrie1950868226xt_b_d > set_b ).
thf(func_def_3,type,
carrie730238621_e_b_f: carrie1821755406_e_b_f > set_e ).
thf(func_def_4,type,
ring_b_d: carrie1950868226xt_b_d > $o ).
thf(func_def_5,type,
zero_a1261444626_a_b_c: carrie722926983_a_b_c > a ).
thf(func_def_6,type,
ideal_b_d: carrie1950868226xt_b_d > set_b > $o ).
thf(func_def_7,type,
annihi259882159t_unit: carrie1950868226xt_b_d > carrie1963041556t_unit > set_b ).
thf(func_def_8,type,
annihilator_b_d_a_c: carrie1950868226xt_b_d > carrie722926983_a_b_c > set_b ).
thf(func_def_9,type,
annihilator_b_d_e_f: carrie1950868226xt_b_d > carrie1821755406_e_b_f > set_b ).
thf(func_def_10,type,
hOM_b_1103679019t_unit: carrie1950868226xt_b_d > carrie1963041556t_unit > carrie1963041556t_unit > carrie980467975t_unit ).
thf(func_def_11,type,
hOM_b_796081438it_a_c: carrie1950868226xt_b_d > carrie1963041556t_unit > carrie722926983_a_b_c > carrie980467975t_unit ).
thf(func_def_12,type,
hOM_b_1959675421it_e_f: carrie1950868226xt_b_d > carrie1963041556t_unit > carrie1821755406_e_b_f > carrie1065537299t_unit ).
thf(func_def_13,type,
hOM_b_717364638t_unit: carrie1950868226xt_b_d > carrie722926983_a_b_c > carrie1963041556t_unit > carrie980467975t_unit ).
thf(func_def_14,type,
hOM_b_d_a_c_a_c: carrie1950868226xt_b_d > carrie722926983_a_b_c > carrie722926983_a_b_c > carrie980467975t_unit ).
thf(func_def_15,type,
hOM_b_d_a_c_e_f: carrie1950868226xt_b_d > carrie722926983_a_b_c > carrie1821755406_e_b_f > carrie1065537299t_unit ).
thf(func_def_16,type,
hOM_b_1375846429t_unit: carrie1950868226xt_b_d > carrie1821755406_e_b_f > carrie1963041556t_unit > carrie292259835t_unit ).
thf(func_def_17,type,
hOM_b_d_e_f_a_c: carrie1950868226xt_b_d > carrie1821755406_e_b_f > carrie722926983_a_b_c > carrie292259835t_unit ).
thf(func_def_18,type,
hOM_b_d_e_f_e_f: carrie1950868226xt_b_d > carrie1821755406_e_b_f > carrie1821755406_e_b_f > carrie377329159t_unit ).
thf(func_def_19,type,
module589927589unit_d: carrie980467975t_unit > carrie1950868226xt_b_d > $o ).
thf(func_def_20,type,
module1648870817unit_d: carrie1065537299t_unit > carrie1950868226xt_b_d > $o ).
thf(func_def_21,type,
module1330273449unit_d: carrie292259835t_unit > carrie1950868226xt_b_d > $o ).
thf(func_def_22,type,
module241733029unit_d: carrie377329159t_unit > carrie1950868226xt_b_d > $o ).
thf(func_def_23,type,
module1821517916unit_d: carrie1963041556t_unit > carrie1950868226xt_b_d > $o ).
thf(func_def_24,type,
module_a_b_c_d: carrie722926983_a_b_c > carrie1950868226xt_b_d > $o ).
thf(func_def_25,type,
module_e_b_f_d: carrie1821755406_e_b_f > carrie1950868226xt_b_d > $o ).
thf(func_def_26,type,
free_g637607517t_unit: carrie1950868226xt_b_d > carrie1963041556t_unit > set_a > $o ).
thf(func_def_27,type,
free_g1087686480_d_a_c: carrie1950868226xt_b_d > carrie722926983_a_b_c > set_a > $o ).
thf(func_def_28,type,
free_g103796815_d_e_f: carrie1950868226xt_b_d > carrie1821755406_e_b_f > set_e > $o ).
thf(func_def_29,type,
genera1692266857t_unit: carrie1950868226xt_b_d > carrie1963041556t_unit > set_a > $o ).
thf(func_def_30,type,
generator_b_d_a_c: carrie1950868226xt_b_d > carrie722926983_a_b_c > set_a > $o ).
thf(func_def_31,type,
generator_b_d_e_f: carrie1950868226xt_b_d > carrie1821755406_e_b_f > set_e > $o ).
thf(func_def_32,type,
l_comb1138968323t_unit: carrie1950868226xt_b_d > carrie1963041556t_unit > nat > ( nat > b ) > ( nat > a ) > a ).
thf(func_def_33,type,
l_comb_b_d_a_c: carrie1950868226xt_b_d > carrie722926983_a_b_c > nat > ( nat > b ) > ( nat > a ) > a ).
thf(func_def_34,type,
l_comb_b_d_e_f: carrie1950868226xt_b_d > carrie1821755406_e_b_f > nat > ( nat > b ) > ( nat > e ) > e ).
thf(func_def_35,type,
linear_span_b_d_a_c: carrie1950868226xt_b_d > carrie722926983_a_b_c > set_b > set_a > set_a ).
thf(func_def_36,type,
mdl_a_b_c: carrie722926983_a_b_c > set_a > carrie1963041556t_unit ).
thf(func_def_37,type,
misomo493403663t_unit: carrie1950868226xt_b_d > carrie1963041556t_unit > carrie1963041556t_unit > $o ).
thf(func_def_38,type,
misomo1935876354it_a_c: carrie1950868226xt_b_d > carrie1963041556t_unit > carrie722926983_a_b_c > $o ).
thf(func_def_39,type,
misomo951986689it_e_f: carrie1950868226xt_b_d > carrie1963041556t_unit > carrie1821755406_e_b_f > $o ).
thf(func_def_40,type,
misomo1857159554t_unit: carrie1950868226xt_b_d > carrie722926983_a_b_c > carrie1963041556t_unit > $o ).
thf(func_def_41,type,
misomo1282343797_c_a_c: carrie1950868226xt_b_d > carrie722926983_a_b_c > carrie722926983_a_b_c > $o ).
thf(func_def_42,type,
misomo298454132_c_e_f: carrie1950868226xt_b_d > carrie722926983_a_b_c > carrie1821755406_e_b_f > $o ).
thf(func_def_43,type,
misomo368157697t_unit: carrie1950868226xt_b_d > carrie1821755406_e_b_f > carrie1963041556t_unit > $o ).
thf(func_def_44,type,
misomo1752826100_f_a_c: carrie1950868226xt_b_d > carrie1821755406_e_b_f > carrie722926983_a_b_c > $o ).
thf(func_def_45,type,
misomo768936435_f_e_f: carrie1950868226xt_b_d > carrie1821755406_e_b_f > carrie1821755406_e_b_f > $o ).
thf(func_def_46,type,
quotie1196826005t_unit: carrie1950868226xt_b_d > carrie1963041556t_unit > set_a > set_a > set_b ).
thf(func_def_47,type,
quotie1153752712_d_a_c: carrie1950868226xt_b_d > carrie722926983_a_b_c > set_a > set_a > set_b ).
thf(func_def_48,type,
quotie169863047_d_e_f: carrie1950868226xt_b_d > carrie1821755406_e_b_f > set_e > set_e > set_b ).
thf(func_def_49,type,
smodul132175289t_unit: carrie1950868226xt_b_d > carrie1963041556t_unit > set_b > set_a ).
thf(func_def_50,type,
smodul818989740_d_a_c: carrie1950868226xt_b_d > carrie722926983_a_b_c > set_b > set_a ).
thf(func_def_51,type,
smodul1982583723_d_e_f: carrie1950868226xt_b_d > carrie1821755406_e_b_f > set_b > set_e ).
thf(func_def_52,type,
submod903911234t_unit: carrie1950868226xt_b_d > carrie1963041556t_unit > set_a > $o ).
thf(func_def_53,type,
submodule_b_d_a_c: carrie1950868226xt_b_d > carrie722926983_a_b_c > set_a > $o ).
thf(func_def_54,type,
submodule_b_d_e_f: carrie1950868226xt_b_d > carrie1821755406_e_b_f > set_e > $o ).
thf(func_def_55,type,
algebr1039611956t_unit: carrie1950868226xt_b_d > carrie1963041556t_unit > set_a > set_a ).
thf(func_def_56,type,
algebr1152250919_d_a_c: carrie1950868226xt_b_d > carrie722926983_a_b_c > set_a > set_a ).
thf(func_def_57,type,
algebr168361254_d_e_f: carrie1950868226xt_b_d > carrie1821755406_e_b_f > set_e > set_e ).
thf(func_def_58,type,
pi_nat_a: set_nat > ( nat > set_a ) > set_nat_a ).
thf(func_def_59,type,
pi_nat_b: set_nat > ( nat > set_b ) > set_nat_b ).
thf(func_def_60,type,
pi_nat_e: set_nat > ( nat > set_e ) > set_nat_e ).
thf(func_def_61,type,
minus_minus_nat: nat > nat > nat ).
thf(func_def_62,type,
minus_1788767276_nat_a: set_nat_a > set_nat_a > set_nat_a ).
thf(func_def_63,type,
minus_780847917_nat_b: set_nat_b > set_nat_b > set_nat_b ).
thf(func_def_64,type,
minus_minus_set_a: set_a > set_a > set_a ).
thf(func_def_65,type,
zero_zero_nat: nat ).
thf(func_def_66,type,
suc: nat > nat ).
thf(func_def_67,type,
bot_bot_set_nat_a: set_nat_a ).
thf(func_def_68,type,
bot_bot_set_nat_b: set_nat_b ).
thf(func_def_69,type,
bot_bot_set_nat: set_nat ).
thf(func_def_70,type,
bot_bot_set_a: set_a ).
thf(func_def_71,type,
bot_bot_set_e: set_e ).
thf(func_def_72,type,
ord_less_nat: nat > nat > $o ).
thf(func_def_73,type,
ord_less_set_a: set_a > set_a > $o ).
thf(func_def_74,type,
ord_less_eq_nat: nat > nat > $o ).
thf(func_def_75,type,
ord_le157368549_nat_a: set_nat_a > set_nat_a > $o ).
thf(func_def_76,type,
ord_le1296932838_nat_b: set_nat_b > set_nat_b > $o ).
thf(func_def_77,type,
ord_less_eq_set_a: set_a > set_a > $o ).
thf(func_def_78,type,
ord_less_eq_set_e: set_e > set_e > $o ).
thf(func_def_79,type,
collect_nat_a: ( ( nat > a ) > $o ) > set_nat_a ).
thf(func_def_80,type,
collect_nat_b: ( ( nat > b ) > $o ) > set_nat_b ).
thf(func_def_81,type,
collect_nat: ( nat > $o ) > set_nat ).
thf(func_def_82,type,
collect_a: ( a > $o ) > set_a ).
thf(func_def_83,type,
insert_nat_a: ( nat > a ) > set_nat_a > set_nat_a ).
thf(func_def_84,type,
insert_nat_b: ( nat > b ) > set_nat_b > set_nat_b ).
thf(func_def_85,type,
insert_a: a > set_a > set_a ).
thf(func_def_86,type,
member_nat_a: ( nat > a ) > set_nat_a > $o ).
thf(func_def_87,type,
member_nat_b: ( nat > b ) > set_nat_b > $o ).
thf(func_def_88,type,
member_nat_e: ( nat > e ) > set_nat_e > $o ).
thf(func_def_89,type,
member_nat: nat > set_nat > $o ).
thf(func_def_90,type,
member_a: a > set_a > $o ).
thf(func_def_91,type,
member_e: e > set_e > $o ).
thf(func_def_92,type,
h: set_a ).
thf(func_def_93,type,
h1: set_a ).
thf(func_def_94,type,
m: carrie722926983_a_b_c ).
thf(func_def_95,type,
n: carrie1821755406_e_b_f ).
thf(func_def_96,type,
r: carrie1950868226xt_b_d ).
thf(func_def_97,type,
g: nat > a ).
thf(func_def_98,type,
h2: a ).
thf(func_def_99,type,
m2: nat ).
thf(func_def_100,type,
t: nat > b ).
thf(func_def_101,type,
x: a ).
thf(func_def_102,type,
xa: nat ).
thf(func_def_106,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_107,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_108,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_109,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_110,type,
vIMP: $o > $o > $o ).
thf(func_def_111,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_112,type,
vNOT: $o > $o ).
thf(func_def_113,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_114,type,
db6:
!>[X0: $tType] : X0 ).
thf(func_def_115,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_116,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_117,type,
db7:
!>[X0: $tType] : X0 ).
thf(func_def_118,type,
db5:
!>[X0: $tType] : X0 ).
thf(func_def_119,type,
vAND: $o > $o > $o ).
thf(func_def_120,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_121,type,
vOR: $o > $o > $o ).
thf(func_def_122,type,
db8:
!>[X0: $tType] : X0 ).
thf(func_def_124,type,
sK1: nat > nat ).
thf(f81,axiom,
! [X0: nat,X1: nat] :
( ( minus_minus_nat @ ( suc @ X0 ) @ ( suc @ X1 ) )
= ( minus_minus_nat @ X0 @ X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_80_diff__Suc__Suc) ).
thf(f160,axiom,
! [X0: nat] :
~ ( ord_less_eq_nat @ ( suc @ X0 ) @ X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_159_Suc__n__not__le__n) ).
thf(f163,axiom,
! [X1: nat,X0: nat] :
( ( ord_less_eq_nat @ X0 @ X1 )
=> ( ord_less_eq_nat @ X0 @ ( suc @ X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_162_le__SucI) ).
thf(f215,axiom,
! [X0: nat,X1: nat] : ( ord_less_eq_nat @ ( minus_minus_nat @ X0 @ X1 ) @ X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_214_diff__le__self) ).
thf(f238,axiom,
( ord_less_nat
= ( ^ [X0: nat] : ( ord_less_eq_nat @ ( suc @ X0 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_237_less__eq__Suc__le) ).
thf(f248,axiom,
! [X0: nat] :
( ( ord_less_nat @ zero_zero_nat @ X0 )
=> ? [X1: nat] :
( X0
= ( suc @ X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_247_gr0__implies__Suc) ).
thf(f327,axiom,
! [X0: nat] :
( ( minus_minus_nat @ X0 @ zero_zero_nat )
= X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_326_diff__zero) ).
thf(f351,axiom,
! [X0: nat] :
( ( ord_less_eq_nat @ X0 @ m2 )
=> ! [X1: nat] :
( ( ord_less_eq_nat @ X1 @ m2 )
=> ( ( ( g @ X0 )
= ( g @ X1 ) )
=> ( X0 = X1 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1) ).
thf(f353,axiom,
( ( g @ m2 )
= h2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_3) ).
thf(f366,axiom,
ord_less_nat @ zero_zero_nat @ m2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_16) ).
thf(f369,axiom,
ord_less_eq_nat @ xa @ ( minus_minus_nat @ m2 @ ( suc @ zero_zero_nat ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_19) ).
thf(f370,axiom,
( ( ( g @ xa )
= h2 )
| ( member_a @ ( g @ xa ) @ h1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_20) ).
thf(f371,conjecture,
member_a @ ( g @ xa ) @ h1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_21) ).
thf(f372,negated_conjecture,
~ ( member_a @ ( g @ xa ) @ h1 ),
inference(negated_conjecture,[status(cth)],[f371]) ).
thf(f374,plain,
! [X0: nat,X1: nat] : ( ord_less_eq_nat @ ( minus_minus_nat @ X0 @ X1 ) @ X0 ),
inference(rectify,[],[f215]) ).
thf(f375,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] : ( ord_less_eq_nat @ ( minus_minus_nat @ Y1 @ Y0 ) @ Y1 ) ) )
= $true ),
inference(fool_elimination,[],[f374]) ).
thf(f384,plain,
! [X0: nat,X1: nat] :
( ( ord_less_eq_nat @ X1 @ X0 )
=> ( ord_less_eq_nat @ X1 @ ( suc @ X0 ) ) ),
inference(rectify,[],[f163]) ).
thf(f385,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( ( ord_less_eq_nat @ Y0 @ Y1 )
=> ( ord_less_eq_nat @ Y0 @ ( suc @ Y1 ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f384]) ).
thf(f502,plain,
( ( ( g @ xa )
= h2 )
| ( member_a @ ( g @ xa ) @ h1 ) ),
inference(rectify,[],[f370]) ).
thf(f503,plain,
( ( ( member_a @ ( g @ xa ) @ h1 )
| ( h2
= ( g @ xa ) ) )
= $true ),
inference(fool_elimination,[],[f502]) ).
thf(f517,plain,
ord_less_eq_nat @ xa @ ( minus_minus_nat @ m2 @ ( suc @ zero_zero_nat ) ),
inference(rectify,[],[f369]) ).
thf(f518,plain,
( ( ord_less_eq_nat @ xa @ ( minus_minus_nat @ m2 @ ( suc @ zero_zero_nat ) ) )
= $true ),
inference(fool_elimination,[],[f517]) ).
thf(f519,plain,
( ord_less_nat
= ( ^ [Y0: nat] : ( ord_less_eq_nat @ ( suc @ Y0 ) ) ) ),
inference(fool_elimination,[],[f238]) ).
thf(f596,plain,
~ ( member_a @ ( g @ xa ) @ h1 ),
inference(rectify,[],[f372]) ).
thf(f597,plain,
( $true
= ( ~ ( member_a @ ( g @ xa ) @ h1 ) ) ),
inference(fool_elimination,[],[f596]) ).
thf(f707,plain,
! [X0: nat] :
( ( ord_less_nat @ zero_zero_nat @ X0 )
=> ? [X1: nat] :
( X0
= ( suc @ X1 ) ) ),
inference(rectify,[],[f248]) ).
thf(f708,plain,
( $true
= ( !! @ nat
@ ^ [Y0: nat] :
( ( ord_less_nat @ zero_zero_nat @ Y0 )
=> ( ?? @ nat
@ ^ [Y1: nat] :
( ( suc @ Y1 )
= Y0 ) ) ) ) ),
inference(fool_elimination,[],[f707]) ).
thf(f790,plain,
ord_less_nat @ zero_zero_nat @ m2,
inference(rectify,[],[f366]) ).
thf(f791,plain,
( ( ord_less_nat @ zero_zero_nat @ m2 )
= $true ),
inference(fool_elimination,[],[f790]) ).
thf(f853,plain,
( h2
= ( g @ m2 ) ),
inference(fool_elimination,[],[f353]) ).
thf(f862,plain,
! [X0: nat] :
( ( ord_less_eq_nat @ X0 @ m2 )
=> ! [X1: nat] :
( ( ord_less_eq_nat @ X1 @ m2 )
=> ( ( ( g @ X0 )
= ( g @ X1 ) )
=> ( X0 = X1 ) ) ) ),
inference(rectify,[],[f351]) ).
thf(f863,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( ( ord_less_eq_nat @ Y0 @ m2 )
=> ( !! @ nat
@ ^ [Y1: nat] :
( ( ord_less_eq_nat @ Y1 @ m2 )
=> ( ( ( g @ Y0 )
= ( g @ Y1 ) )
=> ( Y0 = Y1 ) ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f862]) ).
thf(f894,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( ( minus_minus_nat @ Y0 @ zero_zero_nat )
= Y0 ) )
= $true ),
inference(fool_elimination,[],[f327]) ).
thf(f944,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( ( minus_minus_nat @ Y1 @ Y0 )
= ( minus_minus_nat @ ( suc @ Y1 ) @ ( suc @ Y0 ) ) ) ) )
= $true ),
inference(fool_elimination,[],[f81]) ).
thf(f984,plain,
! [X0: nat] :
~ ( ord_less_eq_nat @ ( suc @ X0 ) @ X0 ),
inference(rectify,[],[f160]) ).
thf(f985,plain,
( $true
= ( !! @ nat
@ ^ [Y0: nat] :
~ ( ord_less_eq_nat @ ( suc @ Y0 ) @ Y0 ) ) ),
inference(fool_elimination,[],[f984]) ).
thf(f1102,plain,
( ( ord_less_nat @ zero_zero_nat @ m2 )
= $true ),
inference(cnf_transformation,[],[f791]) ).
thf(f1158,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( ( minus_minus_nat @ Y0 @ zero_zero_nat )
= Y0 ) )
= $true ),
inference(cnf_transformation,[],[f894]) ).
thf(f1180,plain,
( ord_less_nat
= ( ^ [Y0: nat] : ( ord_less_eq_nat @ ( suc @ Y0 ) ) ) ),
inference(cnf_transformation,[],[f519]) ).
thf(f1227,plain,
( $true
= ( ~ ( member_a @ ( g @ xa ) @ h1 ) ) ),
inference(cnf_transformation,[],[f597]) ).
thf(f1228,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( ( ord_less_eq_nat @ Y0 @ m2 )
=> ( !! @ nat
@ ^ [Y1: nat] :
( ( ord_less_eq_nat @ Y1 @ m2 )
=> ( ( ( g @ Y0 )
= ( g @ Y1 ) )
=> ( Y0 = Y1 ) ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f863]) ).
thf(f1288,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] : ( ord_less_eq_nat @ ( minus_minus_nat @ Y1 @ Y0 ) @ Y1 ) ) )
= $true ),
inference(cnf_transformation,[],[f375]) ).
thf(f1318,plain,
( h2
= ( g @ m2 ) ),
inference(cnf_transformation,[],[f853]) ).
thf(f1374,plain,
( ( ord_less_eq_nat @ xa @ ( minus_minus_nat @ m2 @ ( suc @ zero_zero_nat ) ) )
= $true ),
inference(cnf_transformation,[],[f518]) ).
thf(f1398,plain,
( $true
= ( !! @ nat
@ ^ [Y0: nat] :
~ ( ord_less_eq_nat @ ( suc @ Y0 ) @ Y0 ) ) ),
inference(cnf_transformation,[],[f985]) ).
thf(f1406,plain,
( $true
= ( !! @ nat
@ ^ [Y0: nat] :
( ( ord_less_nat @ zero_zero_nat @ Y0 )
=> ( ?? @ nat
@ ^ [Y1: nat] :
( ( suc @ Y1 )
= Y0 ) ) ) ) ),
inference(cnf_transformation,[],[f708]) ).
thf(f1431,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( ( ord_less_eq_nat @ Y0 @ Y1 )
=> ( ord_less_eq_nat @ Y0 @ ( suc @ Y1 ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f385]) ).
thf(f1436,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( ( minus_minus_nat @ Y1 @ Y0 )
= ( minus_minus_nat @ ( suc @ Y1 ) @ ( suc @ Y0 ) ) ) ) )
= $true ),
inference(cnf_transformation,[],[f944]) ).
thf(f1443,plain,
( ( ( member_a @ ( g @ xa ) @ h1 )
| ( h2
= ( g @ xa ) ) )
= $true ),
inference(cnf_transformation,[],[f503]) ).
thf(f1454,plain,
( $true
= ( ^ [Y0: nat] : ( ord_less_eq_nat @ ( suc @ Y0 ) )
@ zero_zero_nat
@ m2 ) ),
inference(definition_unfolding,[],[f1102,f1180]) ).
thf(f1512,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( ( ^ [Y1: nat] : ( ord_less_eq_nat @ ( suc @ Y1 ) )
@ zero_zero_nat
@ Y0 )
=> ( ?? @ nat
@ ^ [Y1: nat] :
( ( suc @ Y1 )
= Y0 ) ) ) )
= $true ),
inference(definition_unfolding,[],[f1406,f1180]) ).
thf(f1565,plain,
( ( ord_less_eq_nat @ ( suc @ zero_zero_nat ) @ m2 )
= $true ),
inference(beta-eta_normalization,[],[f1454]) ).
thf(f1582,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( ( ord_less_eq_nat @ ( suc @ zero_zero_nat ) @ Y0 )
=> ( ?? @ nat
@ ^ [Y1: nat] :
( ( suc @ Y1 )
= Y0 ) ) ) )
= $true ),
inference(beta-eta_normalization,[],[f1512]) ).
thf(f1602,plain,
( ( ( member_a @ ( g @ xa ) @ h1 )
= $true )
| ( ( h2
= ( g @ xa ) )
= $true ) ),
inference(or_proxy_clausification,[],[f1443]) ).
thf(f1603,plain,
( ( member_a @ ( g @ xa ) @ h1 )
= $false ),
inference(not_proxy_clausification,[],[f1227]) ).
thf(f1604,plain,
( ( h2
= ( g @ xa ) )
| ( ( member_a @ ( g @ xa ) @ h1 )
= $true ) ),
inference(equality_proxy_clausification,[],[f1602]) ).
thf(f1606,definition,
( spl0_1
<=> ( h2
= ( g @ xa ) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
thf(f1608,plain,
( ( h2
= ( g @ xa ) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f1606]) ).
thf(f1610,definition,
( spl0_2
<=> ( ( member_a @ ( g @ xa ) @ h1 )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
thf(f1612,plain,
( ( ( member_a @ ( g @ xa ) @ h1 )
= $true )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f1610]) ).
thf(f1613,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f1604,f1610,f1606]) ).
thf(f1627,plain,
( ( $false = $true )
| ~ spl0_2 ),
inference(forward_demodulation,[],[f1612,f1603]) ).
thf(f1628,plain,
( $false
| ~ spl0_2 ),
inference(trivial_inequality_removal,[],[f1627]) ).
thf(f1629,plain,
~ spl0_2,
inference(avatar_contradiction_clause,[],[f1628]) ).
thf(f1637,plain,
! [X1: nat] :
( ( ^ [Y0: nat] :
( ( ord_less_eq_nat @ Y0 @ m2 )
=> ( !! @ nat
@ ^ [Y1: nat] :
( ( ord_less_eq_nat @ Y1 @ m2 )
=> ( ( ( g @ Y0 )
= ( g @ Y1 ) )
=> ( Y0 = Y1 ) ) ) ) )
@ X1 )
= $true ),
inference(pi_proxy_clausification,[],[f1228]) ).
thf(f1638,plain,
! [X1: nat] :
( $true
= ( ( ord_less_eq_nat @ X1 @ m2 )
=> ( !! @ nat
@ ^ [Y0: nat] :
( ( ord_less_eq_nat @ Y0 @ m2 )
=> ( ( ( g @ X1 )
= ( g @ Y0 ) )
=> ( X1 = Y0 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f1637]) ).
thf(f1639,plain,
! [X1: nat] :
( ( ( !! @ nat
@ ^ [Y0: nat] :
( ( ord_less_eq_nat @ Y0 @ m2 )
=> ( ( ( g @ X1 )
= ( g @ Y0 ) )
=> ( X1 = Y0 ) ) ) )
= $true )
| ( ( ord_less_eq_nat @ X1 @ m2 )
= $false ) ),
inference(imp_proxy_clausification,[],[f1638]) ).
thf(f1643,plain,
! [X2: nat,X1: nat] :
( ( ( ord_less_eq_nat @ X1 @ m2 )
= $false )
| ( ( ^ [Y0: nat] :
( ( ord_less_eq_nat @ Y0 @ m2 )
=> ( ( ( g @ X1 )
= ( g @ Y0 ) )
=> ( X1 = Y0 ) ) )
@ X2 )
= $true ) ),
inference(pi_proxy_clausification,[],[f1639]) ).
thf(f1644,plain,
! [X2: nat,X1: nat] :
( ( ( ord_less_eq_nat @ X1 @ m2 )
= $false )
| ( $true
= ( ( ord_less_eq_nat @ X2 @ m2 )
=> ( ( ( g @ X1 )
= ( g @ X2 ) )
=> ( X1 = X2 ) ) ) ) ),
inference(beta-eta_normalization,[],[f1643]) ).
thf(f1645,plain,
! [X2: nat,X1: nat] :
( ( ( ord_less_eq_nat @ X1 @ m2 )
= $false )
| ( $false
= ( ord_less_eq_nat @ X2 @ m2 ) )
| ( ( ( ( g @ X1 )
= ( g @ X2 ) )
=> ( X1 = X2 ) )
= $true ) ),
inference(imp_proxy_clausification,[],[f1644]) ).
thf(f1646,plain,
! [X2: nat,X1: nat] :
( ( $false
= ( ( g @ X1 )
= ( g @ X2 ) ) )
| ( $false
= ( ord_less_eq_nat @ X2 @ m2 ) )
| ( ( X1 = X2 )
= $true )
| ( ( ord_less_eq_nat @ X1 @ m2 )
= $false ) ),
inference(imp_proxy_clausification,[],[f1645]) ).
thf(f1647,plain,
! [X2: nat,X1: nat] :
( ( ( g @ X1 )
!= ( g @ X2 ) )
| ( ( X1 = X2 )
= $true )
| ( ( ord_less_eq_nat @ X1 @ m2 )
= $false )
| ( $false
= ( ord_less_eq_nat @ X2 @ m2 ) ) ),
inference(equality_proxy_clausification,[],[f1646]) ).
thf(f1648,plain,
! [X2: nat,X1: nat] :
( ( ( g @ X1 )
!= ( g @ X2 ) )
| ( ( ord_less_eq_nat @ X1 @ m2 )
= $false )
| ( X1 = X2 )
| ( $false
= ( ord_less_eq_nat @ X2 @ m2 ) ) ),
inference(equality_proxy_clausification,[],[f1647]) ).
thf(f1651,plain,
! [X0: nat] :
( ( $false
= ( ord_less_eq_nat @ m2 @ m2 ) )
| ( m2 = X0 )
| ( ( ord_less_eq_nat @ X0 @ m2 )
= $false )
| ( h2
!= ( g @ X0 ) ) ),
inference(superposition,[],[f1648,f1318]) ).
thf(f1661,definition,
( spl0_4
<=> ( $false
= ( ord_less_eq_nat @ xa @ m2 ) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
thf(f1663,plain,
( ( $false
= ( ord_less_eq_nat @ xa @ m2 ) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f1661]) ).
thf(f1667,definition,
( spl0_5
<=> ! [X0: nat] :
( ( m2 = X0 )
| ( ( ord_less_eq_nat @ X0 @ m2 )
= $false )
| ( h2
!= ( g @ X0 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
thf(f1668,plain,
( ! [X0: nat] :
( ( h2
!= ( g @ X0 ) )
| ( m2 = X0 )
| ( ( ord_less_eq_nat @ X0 @ m2 )
= $false ) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f1667]) ).
thf(f1670,definition,
( spl0_6
<=> ( $false
= ( ord_less_eq_nat @ m2 @ m2 ) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
thf(f1672,plain,
( ( $false
= ( ord_less_eq_nat @ m2 @ m2 ) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f1670]) ).
thf(f1674,plain,
( spl0_6
| spl0_5 ),
inference(avatar_split_clause,[],[f1651,f1667,f1670]) ).
thf(f1690,plain,
! [X1: nat] :
( ( ^ [Y0: nat] :
~ ( ord_less_eq_nat @ ( suc @ Y0 ) @ Y0 )
@ X1 )
= $true ),
inference(pi_proxy_clausification,[],[f1398]) ).
thf(f1691,plain,
! [X1: nat] :
( ( ~ ( ord_less_eq_nat @ ( suc @ X1 ) @ X1 ) )
= $true ),
inference(beta-eta_normalization,[],[f1690]) ).
thf(f1692,plain,
! [X1: nat] :
( $false
= ( ord_less_eq_nat @ ( suc @ X1 ) @ X1 ) ),
inference(not_proxy_clausification,[],[f1691]) ).
thf(f1708,plain,
! [X1: nat] :
( ( ^ [Y0: nat] :
( ( minus_minus_nat @ Y0 @ zero_zero_nat )
= Y0 )
@ X1 )
= $true ),
inference(pi_proxy_clausification,[],[f1158]) ).
thf(f1709,plain,
! [X1: nat] :
( ( ( minus_minus_nat @ X1 @ zero_zero_nat )
= X1 )
= $true ),
inference(beta-eta_normalization,[],[f1708]) ).
thf(f1710,plain,
! [X1: nat] :
( ( minus_minus_nat @ X1 @ zero_zero_nat )
= X1 ),
inference(equality_proxy_clausification,[],[f1709]) ).
thf(f1733,plain,
! [X1: nat] :
( ( ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] : ( ord_less_eq_nat @ ( minus_minus_nat @ Y1 @ Y0 ) @ Y1 ) )
@ X1 )
= $true ),
inference(pi_proxy_clausification,[],[f1288]) ).
thf(f1734,plain,
! [X1: nat] :
( ( !! @ nat
@ ^ [Y0: nat] : ( ord_less_eq_nat @ ( minus_minus_nat @ Y0 @ X1 ) @ Y0 ) )
= $true ),
inference(beta-eta_normalization,[],[f1733]) ).
thf(f1735,plain,
! [X2: nat,X1: nat] :
( ( ^ [Y0: nat] : ( ord_less_eq_nat @ ( minus_minus_nat @ Y0 @ X1 ) @ Y0 )
@ X2 )
= $true ),
inference(pi_proxy_clausification,[],[f1734]) ).
thf(f1736,plain,
! [X2: nat,X1: nat] :
( ( ord_less_eq_nat @ ( minus_minus_nat @ X2 @ X1 ) @ X2 )
= $true ),
inference(beta-eta_normalization,[],[f1735]) ).
thf(f1739,plain,
! [X0: nat] :
( ( ord_less_eq_nat @ X0 @ X0 )
= $true ),
inference(superposition,[],[f1736,f1710]) ).
thf(f2039,plain,
! [X1: nat] :
( $true
= ( ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( ( ord_less_eq_nat @ Y0 @ Y1 )
=> ( ord_less_eq_nat @ Y0 @ ( suc @ Y1 ) ) ) )
@ X1 ) ),
inference(pi_proxy_clausification,[],[f1431]) ).
thf(f2040,plain,
! [X1: nat] :
( ( !! @ nat
@ ^ [Y0: nat] :
( ( ord_less_eq_nat @ X1 @ Y0 )
=> ( ord_less_eq_nat @ X1 @ ( suc @ Y0 ) ) ) )
= $true ),
inference(beta-eta_normalization,[],[f2039]) ).
thf(f2041,plain,
! [X2: nat,X1: nat] :
( $true
= ( ^ [Y0: nat] :
( ( ord_less_eq_nat @ X1 @ Y0 )
=> ( ord_less_eq_nat @ X1 @ ( suc @ Y0 ) ) )
@ X2 ) ),
inference(pi_proxy_clausification,[],[f2040]) ).
thf(f2042,plain,
! [X2: nat,X1: nat] :
( ( ( ord_less_eq_nat @ X1 @ X2 )
=> ( ord_less_eq_nat @ X1 @ ( suc @ X2 ) ) )
= $true ),
inference(beta-eta_normalization,[],[f2041]) ).
thf(f2043,plain,
! [X2: nat,X1: nat] :
( ( $true
= ( ord_less_eq_nat @ X1 @ ( suc @ X2 ) ) )
| ( ( ord_less_eq_nat @ X1 @ X2 )
= $false ) ),
inference(imp_proxy_clausification,[],[f2042]) ).
thf(f2106,plain,
! [X1: nat] :
( ( ^ [Y0: nat] :
( ( ord_less_eq_nat @ ( suc @ zero_zero_nat ) @ Y0 )
=> ( ?? @ nat
@ ^ [Y1: nat] :
( ( suc @ Y1 )
= Y0 ) ) )
@ X1 )
= $true ),
inference(pi_proxy_clausification,[],[f1582]) ).
thf(f2107,plain,
! [X1: nat] :
( ( ( ord_less_eq_nat @ ( suc @ zero_zero_nat ) @ X1 )
=> ( ?? @ nat
@ ^ [Y0: nat] :
( ( suc @ Y0 )
= X1 ) ) )
= $true ),
inference(beta-eta_normalization,[],[f2106]) ).
thf(f2108,plain,
! [X1: nat] :
( ( $true
= ( ?? @ nat
@ ^ [Y0: nat] :
( ( suc @ Y0 )
= X1 ) ) )
| ( $false
= ( ord_less_eq_nat @ ( suc @ zero_zero_nat ) @ X1 ) ) ),
inference(imp_proxy_clausification,[],[f2107]) ).
thf(f2109,plain,
! [X1: nat] :
( ( ( ^ [Y0: nat] :
( ( suc @ Y0 )
= X1 )
@ ( sK1 @ X1 ) )
= $true )
| ( $false
= ( ord_less_eq_nat @ ( suc @ zero_zero_nat ) @ X1 ) ) ),
inference(sigma_proxy_clausification,[],[f2108]) ).
thf(f2110,plain,
! [X1: nat] :
( ( $true
= ( ( suc @ ( sK1 @ X1 ) )
= X1 ) )
| ( $false
= ( ord_less_eq_nat @ ( suc @ zero_zero_nat ) @ X1 ) ) ),
inference(beta-eta_normalization,[],[f2109]) ).
thf(f2111,plain,
! [X1: nat] :
( ( $false
= ( ord_less_eq_nat @ ( suc @ zero_zero_nat ) @ X1 ) )
| ( ( suc @ ( sK1 @ X1 ) )
= X1 ) ),
inference(equality_proxy_clausification,[],[f2110]) ).
thf(f2120,plain,
( ( $false = $true )
| ( m2
= ( suc @ ( sK1 @ m2 ) ) ) ),
inference(superposition,[],[f2111,f1565]) ).
thf(f2141,plain,
( m2
= ( suc @ ( sK1 @ m2 ) ) ),
inference(trivial_inequality_removal,[],[f2120]) ).
thf(f2157,plain,
( $false
= ( ord_less_eq_nat @ m2 @ ( sK1 @ m2 ) ) ),
inference(superposition,[],[f1692,f2141]) ).
thf(f2166,plain,
! [X0: nat] :
( ( $false
= ( ord_less_eq_nat @ X0 @ ( sK1 @ m2 ) ) )
| ( ( ord_less_eq_nat @ X0 @ m2 )
= $true ) ),
inference(superposition,[],[f2043,f2141]) ).
thf(f2526,plain,
( ( $false = $true )
| ~ spl0_6 ),
inference(forward_demodulation,[],[f1672,f1739]) ).
thf(f2527,plain,
( $false
| ~ spl0_6 ),
inference(trivial_inequality_removal,[],[f2526]) ).
thf(f2528,plain,
~ spl0_6,
inference(avatar_contradiction_clause,[],[f2527]) ).
thf(f2535,definition,
( spl0_11
<=> ( m2 = xa ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
thf(f2537,plain,
( ( m2 = xa )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f2535]) ).
thf(f2567,plain,
( ( h2 != h2 )
| ( $false
= ( ord_less_eq_nat @ xa @ m2 ) )
| ( m2 = xa )
| ~ spl0_1
| ~ spl0_5 ),
inference(superposition,[],[f1668,f1608]) ).
thf(f2568,plain,
( ( m2 = xa )
| ( $false
= ( ord_less_eq_nat @ xa @ m2 ) )
| ~ spl0_1
| ~ spl0_5 ),
inference(trivial_inequality_removal,[],[f2567]) ).
thf(f2583,plain,
! [X1: nat] :
( ( ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( ( minus_minus_nat @ Y1 @ Y0 )
= ( minus_minus_nat @ ( suc @ Y1 ) @ ( suc @ Y0 ) ) ) )
@ X1 )
= $true ),
inference(pi_proxy_clausification,[],[f1436]) ).
thf(f2584,plain,
! [X1: nat] :
( ( !! @ nat
@ ^ [Y0: nat] :
( ( minus_minus_nat @ Y0 @ X1 )
= ( minus_minus_nat @ ( suc @ Y0 ) @ ( suc @ X1 ) ) ) )
= $true ),
inference(beta-eta_normalization,[],[f2583]) ).
thf(f2587,plain,
! [X2: nat,X1: nat] :
( ( ^ [Y0: nat] :
( ( minus_minus_nat @ Y0 @ X1 )
= ( minus_minus_nat @ ( suc @ Y0 ) @ ( suc @ X1 ) ) )
@ X2 )
= $true ),
inference(pi_proxy_clausification,[],[f2584]) ).
thf(f2588,plain,
! [X2: nat,X1: nat] :
( ( ( minus_minus_nat @ X2 @ X1 )
= ( minus_minus_nat @ ( suc @ X2 ) @ ( suc @ X1 ) ) )
= $true ),
inference(beta-eta_normalization,[],[f2587]) ).
thf(f2589,plain,
! [X2: nat,X1: nat] :
( ( minus_minus_nat @ X2 @ X1 )
= ( minus_minus_nat @ ( suc @ X2 ) @ ( suc @ X1 ) ) ),
inference(equality_proxy_clausification,[],[f2588]) ).
thf(f2636,plain,
! [X0: nat] :
( ( minus_minus_nat @ m2 @ ( suc @ X0 ) )
= ( minus_minus_nat @ ( sK1 @ m2 ) @ X0 ) ),
inference(superposition,[],[f2589,f2141]) ).
thf(f2651,plain,
( ( minus_minus_nat @ m2 @ ( suc @ zero_zero_nat ) )
= ( sK1 @ m2 ) ),
inference(superposition,[],[f2636,f1710]) ).
thf(f2756,plain,
( ( ord_less_eq_nat @ xa @ ( sK1 @ m2 ) )
= $true ),
inference(superposition,[],[f1374,f2651]) ).
thf(f2761,plain,
( ( ( ord_less_eq_nat @ m2 @ ( sK1 @ m2 ) )
= $true )
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2756,f2537]) ).
thf(f2763,plain,
( ( $false = $true )
| ~ spl0_11 ),
inference(forward_demodulation,[],[f2761,f2157]) ).
thf(f2764,plain,
( $false
| ~ spl0_11 ),
inference(trivial_inequality_removal,[],[f2763]) ).
thf(f2765,plain,
~ spl0_11,
inference(avatar_contradiction_clause,[],[f2764]) ).
thf(f2769,plain,
( spl0_4
| spl0_11
| ~ spl0_1
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f2568,f1667,f1606,f2535,f1661]) ).
thf(f3168,plain,
( ( $false = $true )
| ( ( ord_less_eq_nat @ xa @ m2 )
= $true ) ),
inference(superposition,[],[f2166,f2756]) ).
thf(f3175,plain,
( ( ord_less_eq_nat @ xa @ m2 )
= $true ),
inference(trivial_inequality_removal,[],[f3168]) ).
thf(f3179,plain,
( ( $false = $true )
| ~ spl0_4 ),
inference(forward_demodulation,[],[f3175,f1663]) ).
thf(f3180,plain,
( $false
| ~ spl0_4 ),
inference(trivial_inequality_removal,[],[f3179]) ).
thf(f3181,plain,
~ spl0_4,
inference(avatar_contradiction_clause,[],[f3180]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f1613]) ).
cnf(s2,plain,
~ spl0_2,
inference(sat_conversion,[],[f1629]) ).
cnf(s6,plain,
( spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f1674]) ).
cnf(s20,plain,
~ spl0_6,
inference(sat_conversion,[],[f2528]) ).
cnf(s28,plain,
~ spl0_11,
inference(sat_conversion,[],[f2765]) ).
cnf(s31,plain,
( ~ spl0_1
| spl0_4
| ~ spl0_5
| spl0_11 ),
inference(sat_conversion,[],[f2769]) ).
cnf(s37,plain,
~ spl0_4,
inference(sat_conversion,[],[f3181]) ).
cnf(s38,plain,
( ~ spl0_1
| ~ spl0_5
| spl0_11 ),
inference(rat,[],[s31,s37]) ).
cnf(s42,plain,
spl0_5,
inference(rat,[],[s6,s20]) ).
cnf(s43,plain,
~ spl0_1,
inference(rat,[],[s38,s28,s42]) ).
cnf(s44,plain,
$false,
inference(rat,[],[s1,s2,s43]) ).
thf(f3182,plain,
$false,
inference(avatar_sat_refutation,[],[s44]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP026^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n003.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 19:39:44 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running higher-order theorem proving
% 0.08/0.25 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.67/0.43 % (2965509)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.67/0.43 % (2965517)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=695897269:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.67/0.43 % (2965516)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3426532468:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.67/0.43 % (2965515)lrs+10_16_si=on:nwc=1.5:random_seed=2249001551:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.67/0.43 % (2965514)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=196164227:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.67/0.43 % (2965516)Instruction limit reached!
% 0.67/0.43 % (2965516)------------------------------
% 0.67/0.43 % (2965516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.43 % (2965516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.43 % (2965516)CaDiCaL version: 2.1.3
% 0.67/0.43 % (2965516)Termination reason: Instruction limit
% 0.67/0.43 % (2965516)Termination phase: shuffling
% 0.67/0.43 % (2965516)Time elapsed: 0.002 s
% 0.67/0.43 % (2965516)Peak memory usage: 10 MB
% 0.67/0.43 % (2965516)Instructions burned: 3 (million)
% 0.67/0.43 % (2965518)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1637699213:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.67/0.43 % (2965515)Instruction limit reached!
% 0.67/0.43 % (2965515)------------------------------
% 0.67/0.43 % (2965515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.43 % (2965515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.43 % (2965515)CaDiCaL version: 2.1.3
% 0.67/0.43 % (2965515)Termination reason: Instruction limit
% 0.67/0.43 % (2965515)Termination phase: shuffling
% 0.67/0.43 % (2965515)Time elapsed: 0.008 s
% 0.67/0.43 % (2965515)Peak memory usage: 10 MB
% 0.67/0.43 % (2965515)Instructions burned: 18 (million)
% 0.67/0.43 % (2965520)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.67/0.43 % (2965520)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.67/0.43 % (2965519)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3790495149:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.67/0.43 % (2965520)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=2758068105:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.67/0.43 % (2965518)Instruction limit reached!
% 0.67/0.43 % (2965518)------------------------------
% 0.67/0.43 % (2965518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.43 % (2965518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.43 % (2965518)CaDiCaL version: 2.1.3
% 0.67/0.43 % (2965518)Termination reason: Instruction limit
% 0.67/0.43 % (2965518)Termination phase: shuffling
% 0.67/0.43 % (2965518)Time elapsed: 0.013 s
% 0.67/0.43 % (2965518)Peak memory usage: 10 MB
% 0.67/0.43 % (2965518)Instructions burned: 26 (million)
% 0.67/0.43 % (2965525)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2800113985:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.67/0.43 % (2965525)Instruction limit reached!
% 0.67/0.43 % (2965525)------------------------------
% 0.67/0.43 % (2965525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.67/0.43 % (2965525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.67/0.43 % (2965525)CaDiCaL version: 2.1.3
% 0.67/0.43 % (2965525)Termination reason: Instruction limit
% 0.67/0.43 % (2965525)Termination phase: shuffling
% 0.67/0.43 % (2965525)Time elapsed: 0.003 s
% 0.67/0.43 % (2965525)Peak memory usage: 10 MB
% 0.67/0.43 % (2965525)Instructions burned: 3 (million)
% 0.67/0.43 % (2965530)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.46/0.50 % (2965527)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2238479666:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.46/0.50 % (2965514)Instruction limit reached!
% 1.46/0.50 % (2965514)------------------------------
% 1.46/0.50 % (2965514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.50 % (2965514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.50 % (2965514)CaDiCaL version: 2.1.3
% 1.46/0.50 % (2965514)Termination reason: Instruction limit
% 1.46/0.50 % (2965514)Termination phase: Property scanning
% 1.46/0.50 % (2965514)Time elapsed: 0.042 s
% 1.46/0.50 % (2965514)Peak memory usage: 12 MB
% 1.46/0.50 % (2965514)Instructions burned: 89 (million)
% 1.46/0.50 % (2965530)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=294134115:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.46/0.50 % (2965527)Instruction limit reached!
% 1.46/0.50 % (2965527)------------------------------
% 1.46/0.50 % (2965527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.50 % (2965527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.50 % (2965527)CaDiCaL version: 2.1.3
% 1.46/0.50 % (2965527)Termination reason: Instruction limit
% 1.46/0.50 % (2965527)Termination phase: shuffling
% 1.46/0.50 % (2965527)Time elapsed: 0.007 s
% 1.46/0.50 % (2965527)Peak memory usage: 10 MB
% 1.46/0.50 % (2965527)Instructions burned: 7 (million)
% 1.46/0.50 % (2965530)Instruction limit reached!
% 1.46/0.50 % (2965530)------------------------------
% 1.46/0.50 % (2965530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.50 % (2965530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.50 % (2965530)CaDiCaL version: 2.1.3
% 1.46/0.50 % (2965530)Termination reason: Instruction limit
% 1.46/0.50 % (2965530)Termination phase: shuffling
% 1.46/0.50 % (2965530)Time elapsed: 0.005 s
% 1.46/0.50 % (2965530)Peak memory usage: 10 MB
% 1.46/0.50 % (2965530)Instructions burned: 7 (million)
% 1.46/0.50 % (2965532)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3603964357:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.46/0.50 % (2965535)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.46/0.50 % (2965535)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.46/0.50 % (2965535)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2598499697:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.46/0.50 % (2965519)Instruction limit reached!
% 1.46/0.50 % (2965519)------------------------------
% 1.46/0.50 % (2965519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.50 % (2965519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.50 % (2965519)CaDiCaL version: 2.1.3
% 1.46/0.50 % (2965519)Termination reason: Instruction limit
% 1.46/0.50 % (2965519)Termination phase: Preprocessing 3
% 1.46/0.50 % (2965519)Time elapsed: 0.047 s
% 1.46/0.50 % (2965519)Peak memory usage: 12 MB
% 1.46/0.50 % (2965519)Instructions burned: 76 (million)
% 1.46/0.50 % (2965532)Instruction limit reached!
% 1.46/0.50 % (2965532)------------------------------
% 1.46/0.50 % (2965532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.50 % (2965532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.50 % (2965532)CaDiCaL version: 2.1.3
% 1.46/0.50 % (2965532)Termination reason: Instruction limit
% 1.46/0.50 % (2965532)Termination phase: shuffling
% 1.46/0.50 % (2965532)Time elapsed: 0.007 s
% 1.46/0.50 % (2965532)Peak memory usage: 10 MB
% 1.46/0.50 % (2965532)Instructions burned: 14 (million)
% 1.46/0.50 % (2965537)lrs+10_1_si=on:cs=on:random_seed=1490811683:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.46/0.50 % (2965535)Instruction limit reached!
% 1.46/0.50 % (2965535)------------------------------
% 1.46/0.50 % (2965535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.50 % (2965535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.52 % (2965535)CaDiCaL version: 2.1.3
% 1.46/0.52 % (2965535)Termination reason: Instruction limit
% 1.46/0.52 % (2965535)Termination phase: shuffling
% 1.46/0.52 % (2965535)Time elapsed: 0.013 s
% 1.46/0.52 % (2965535)Peak memory usage: 11 MB
% 1.46/0.52 % (2965535)Instructions burned: 28 (million)
% 1.46/0.52 % (2965537)Instruction limit reached!
% 1.46/0.52 % (2965537)------------------------------
% 1.46/0.52 % (2965537)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.52 % (2965537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.52 % (2965537)CaDiCaL version: 2.1.3
% 1.46/0.52 % (2965537)Termination reason: Instruction limit
% 1.46/0.52 % (2965537)Termination phase: shuffling
% 1.46/0.52 % (2965537)Time elapsed: 0.004 s
% 1.46/0.52 % (2965537)Peak memory usage: 10 MB
% 1.46/0.52 % (2965537)Instructions burned: 8 (million)
% 1.46/0.52 % (2965540)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.46/0.52 % (2965536)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=166842161:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 1.46/0.53 % (2965540)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=3186456770:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.46/0.53 % (2965520)Instruction limit reached!
% 1.46/0.53 % (2965520)------------------------------
% 1.46/0.53 % (2965520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.53 % (2965520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.53 % (2965520)CaDiCaL version: 2.1.3
% 1.46/0.53 % (2965520)Termination reason: Instruction limit
% 1.46/0.53 % (2965520)Termination phase: Saturation
% 1.46/0.53 % (2965520)Time elapsed: 0.071 s
% 1.46/0.53 % (2965520)Peak memory usage: 14 MB
% 1.46/0.53 % (2965520)Instructions burned: 158 (million)
% 1.46/0.53 % (2965540)Instruction limit reached!
% 1.46/0.53 % (2965540)------------------------------
% 1.46/0.53 % (2965540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.53 % (2965540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.53 % (2965540)CaDiCaL version: 2.1.3
% 1.46/0.53 % (2965540)Termination reason: Instruction limit
% 1.46/0.53 % (2965540)Termination phase: shuffling
% 1.46/0.53 % (2965540)Time elapsed: 0.003 s
% 1.46/0.53 % (2965540)Peak memory usage: 10 MB
% 1.46/0.53 % (2965540)Instructions burned: 4 (million)
% 1.46/0.53 % (2965541)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1510262995:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.46/0.53 % (2965543)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1413464520:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.46/0.53 % (2965544)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1809495978:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.46/0.53 % (2965548)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=622925444:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.46/0.53 % (2965549)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3670178677:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.46/0.53 % (2965544)Instruction limit reached!
% 1.46/0.53 % (2965544)------------------------------
% 1.46/0.53 % (2965544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.53 % (2965544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.53 % (2965544)CaDiCaL version: 2.1.3
% 1.46/0.53 % (2965544)Termination reason: Instruction limit
% 1.46/0.53 % (2965544)Termination phase: shuffling
% 1.46/0.53 % (2965544)Time elapsed: 0.011 s
% 1.46/0.53 % (2965544)Peak memory usage: 10 MB
% 1.46/0.53 % (2965544)Instructions burned: 25 (million)
% 1.46/0.53 % (2965548)Instruction limit reached!
% 1.46/0.53 % (2965548)------------------------------
% 1.46/0.53 % (2965548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.53 % (2965548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.59 % (2965548)CaDiCaL version: 2.1.3
% 1.46/0.59 % (2965548)Termination reason: Instruction limit
% 1.46/0.59 % (2965548)Termination phase: shuffling
% 1.46/0.59 % (2965548)Time elapsed: 0.007 s
% 1.46/0.59 % (2965548)Peak memory usage: 10 MB
% 1.46/0.59 % (2965548)Instructions burned: 15 (million)
% 1.46/0.59 % (2965541)Instruction limit reached!
% 1.46/0.59 % (2965541)------------------------------
% 1.46/0.59 % (2965541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.59 % (2965541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.59 % (2965541)CaDiCaL version: 2.1.3
% 1.46/0.59 % (2965541)Termination reason: Instruction limit
% 1.46/0.59 % (2965541)Termination phase: Property scanning
% 1.46/0.59 % (2965541)Time elapsed: 0.032 s
% 1.46/0.59 % (2965541)Peak memory usage: 11 MB
% 1.46/0.59 % (2965541)Instructions burned: 39 (million)
% 1.46/0.59 % (2965554)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=723615837:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.46/0.59 % (2965555)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1332682251:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.46/0.59 % (2965554)Instruction limit reached!
% 1.46/0.59 % (2965554)------------------------------
% 1.46/0.59 % (2965554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.59 % (2965554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.59 % (2965554)CaDiCaL version: 2.1.3
% 1.46/0.59 % (2965554)Termination reason: Instruction limit
% 1.46/0.59 % (2965554)Termination phase: shuffling
% 1.46/0.59 % (2965554)Time elapsed: 0.013 s
% 1.46/0.59 % (2965554)Peak memory usage: 10 MB
% 1.46/0.59 % (2965554)Instructions burned: 15 (million)
% 1.46/0.59 % (2965556)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1361001795:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.46/0.59 % (2965555)Instruction limit reached!
% 1.46/0.59 % (2965555)------------------------------
% 1.46/0.59 % (2965555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.59 % (2965555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.59 % (2965555)CaDiCaL version: 2.1.3
% 1.46/0.59 % (2965555)Termination reason: Instruction limit
% 1.46/0.59 % (2965555)Termination phase: shuffling
% 1.46/0.59 % (2965555)Time elapsed: 0.003 s
% 1.46/0.59 % (2965555)Peak memory usage: 10 MB
% 1.46/0.59 % (2965555)Instructions burned: 2 (million)
% 1.46/0.59 % (2965536)Instruction limit reached!
% 1.46/0.59 % (2965536)------------------------------
% 1.46/0.59 % (2965536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.59 % (2965536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.59 % (2965536)CaDiCaL version: 2.1.3
% 1.46/0.59 % (2965536)Termination reason: Instruction limit
% 1.46/0.59 % (2965536)Termination phase: Property scanning
% 1.46/0.59 % (2965536)Time elapsed: 0.070 s
% 1.46/0.59 % (2965536)Peak memory usage: 11 MB
% 1.46/0.59 % (2965536)Instructions burned: 86 (million)
% 1.46/0.59 % (2965560)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3386262277:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.46/0.59 % (2965556)Instruction limit reached!
% 1.46/0.59 % (2965556)------------------------------
% 1.46/0.59 % (2965556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.46/0.59 % (2965556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.46/0.59 % (2965556)CaDiCaL version: 2.1.3
% 1.46/0.59 % (2965556)Termination reason: Instruction limit
% 1.46/0.59 % (2965556)Termination phase: shuffling
% 1.46/0.59 % (2965556)Time elapsed: 0.023 s
% 1.46/0.59 % (2965556)Peak memory usage: 11 MB
% 1.46/0.59 % (2965556)Instructions burned: 27 (million)
% 1.46/0.59 % (2965562)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.46/0.59 % (2965562)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.46/0.59 % (2965517)Instruction limit reached!
% 1.46/0.59 % (2965517)------------------------------
% 1.46/0.59 % (2965517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.66 % (2965517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.66 % (2965517)CaDiCaL version: 2.1.3
% 2.40/0.66 % (2965517)Termination reason: Instruction limit
% 2.40/0.66 % (2965517)Termination phase: Saturation
% 2.40/0.66 % (2965517)Time elapsed: 0.185 s
% 2.40/0.66 % (2965517)Peak memory usage: 17 MB
% 2.40/0.66 % (2965517)Instructions burned: 635 (million)
% 2.40/0.66 % (2965560)Instruction limit reached!
% 2.40/0.66 % (2965560)------------------------------
% 2.40/0.66 % (2965560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.66 % (2965560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.66 % (2965560)CaDiCaL version: 2.1.3
% 2.40/0.66 % (2965560)Termination reason: Instruction limit
% 2.40/0.66 % (2965560)Termination phase: shuffling
% 2.40/0.66 % (2965560)Time elapsed: 0.011 s
% 2.40/0.66 % (2965560)Peak memory usage: 10 MB
% 2.40/0.66 % (2965560)Instructions burned: 24 (million)
% 2.40/0.66 % (2965561)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1732938599:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 2.40/0.66 % (2965562)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=3603494372:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 2.40/0.66 % (2965568)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=2428541688:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.40/0.66 % (2965562)Instruction limit reached!
% 2.40/0.66 % (2965562)------------------------------
% 2.40/0.66 % (2965562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.66 % (2965562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.66 % (2965562)CaDiCaL version: 2.1.3
% 2.40/0.66 % (2965562)Termination reason: Instruction limit
% 2.40/0.66 % (2965562)Termination phase: shuffling
% 2.40/0.66 % (2965562)Time elapsed: 0.013 s
% 2.40/0.66 % (2965562)Peak memory usage: 10 MB
% 2.40/0.66 % (2965562)Instructions burned: 14 (million)
% 2.40/0.66 % (2965566)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.40/0.66 % (2965569)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=909147393:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.40/0.66 % (2965568)Instruction limit reached!
% 2.40/0.66 % (2965568)------------------------------
% 2.40/0.66 % (2965568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.66 % (2965568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.66 % (2965568)CaDiCaL version: 2.1.3
% 2.40/0.66 % (2965568)Termination reason: Instruction limit
% 2.40/0.66 % (2965568)Termination phase: shuffling
% 2.40/0.66 % (2965568)Time elapsed: 0.008 s
% 2.40/0.66 % (2965568)Peak memory usage: 11 MB
% 2.40/0.66 % (2965568)Instructions burned: 35 (million)
% 2.40/0.66 % (2965566)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=871433453:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 2.40/0.66 % (2965569)Instruction limit reached!
% 2.40/0.66 % (2965569)------------------------------
% 2.40/0.66 % (2965569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.66 % (2965569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.66 % (2965569)CaDiCaL version: 2.1.3
% 2.40/0.66 % (2965569)Termination reason: Instruction limit
% 2.40/0.66 % (2965569)Termination phase: shuffling
% 2.40/0.66 % (2965569)Time elapsed: 0.004 s
% 2.40/0.66 % (2965569)Peak memory usage: 10 MB
% 2.40/0.66 % (2965569)Instructions burned: 7 (million)
% 2.40/0.66 % (2965566)Instruction limit reached!
% 2.40/0.66 % (2965566)------------------------------
% 2.40/0.66 % (2965566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.66 % (2965566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.66 % (2965566)CaDiCaL version: 2.1.3
% 2.40/0.66 % (2965566)Termination reason: Instruction limit
% 2.40/0.66 % (2965566)Termination phase: shuffling
% 2.40/0.66 % (2965566)Time elapsed: 0.007 s
% 2.40/0.66 % (2965566)Peak memory usage: 10 MB
% 2.40/0.66 % (2965566)Instructions burned: 8 (million)
% 2.55/0.77 % (2965574)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3521569307:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 2.55/0.77 % (2965572)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1075349340:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.55/0.77 % (2965574)Instruction limit reached!
% 2.55/0.77 % (2965574)------------------------------
% 2.55/0.77 % (2965574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.77 % (2965574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.77 % (2965574)CaDiCaL version: 2.1.3
% 2.55/0.77 % (2965574)Termination reason: Instruction limit
% 2.55/0.77 % (2965574)Termination phase: shuffling
% 2.55/0.77 % (2965574)Time elapsed: 0.006 s
% 2.55/0.77 % (2965574)Peak memory usage: 10 MB
% 2.55/0.77 % (2965574)Instructions burned: 24 (million)
% 2.55/0.77 % (2965572)Instruction limit reached!
% 2.55/0.77 % (2965572)------------------------------
% 2.55/0.77 % (2965572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.77 % (2965572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.77 % (2965572)CaDiCaL version: 2.1.3
% 2.55/0.77 % (2965572)Termination reason: Instruction limit
% 2.55/0.77 % (2965572)Termination phase: shuffling
% 2.55/0.77 % (2965572)Time elapsed: 0.011 s
% 2.55/0.77 % (2965572)Peak memory usage: 10 MB
% 2.55/0.77 % (2965572)Instructions burned: 23 (million)
% 2.55/0.77 % (2965580)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2284083753:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.55/0.77 % (2965561)Instruction limit reached!
% 2.55/0.77 % (2965561)------------------------------
% 2.55/0.77 % (2965561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.77 % (2965561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.77 % (2965561)CaDiCaL version: 2.1.3
% 2.55/0.77 % (2965561)Termination reason: Instruction limit
% 2.55/0.77 % (2965561)Termination phase: Preprocessing 1
% 2.55/0.77 % (2965561)Time elapsed: 0.048 s
% 2.55/0.77 % (2965561)Peak memory usage: 11 MB
% 2.55/0.77 % (2965561)Instructions burned: 60 (million)
% 2.55/0.77 % (2965576)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=926071922:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 2.55/0.77 % (2965583)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.55/0.77 % (2965583)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1252978843:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.55/0.77 % (2965577)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2302299975:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 2.55/0.77 % (2965583)Instruction limit reached!
% 2.55/0.77 % (2965583)------------------------------
% 2.55/0.77 % (2965583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.77 % (2965583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.77 % (2965583)CaDiCaL version: 2.1.3
% 2.55/0.77 % (2965583)Termination reason: Instruction limit
% 2.55/0.77 % (2965583)Termination phase: shuffling
% 2.55/0.77 % (2965583)Time elapsed: 0.004 s
% 2.55/0.77 % (2965583)Peak memory usage: 10 MB
% 2.55/0.77 % (2965583)Instructions burned: 8 (million)
% 2.55/0.77 % (2965581)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3643851340:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.55/0.77 % (2965543)Instruction limit reached!
% 2.55/0.77 % (2965543)------------------------------
% 2.55/0.77 % (2965543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.77 % (2965543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.77 % (2965543)CaDiCaL version: 2.1.3
% 2.55/0.77 % (2965543)Termination reason: Instruction limit
% 2.55/0.77 % (2965543)Termination phase: Saturation
% 2.55/0.77 % (2965543)Time elapsed: 0.168 s
% 2.55/0.77 % (2965543)Peak memory usage: 15 MB
% 2.55/0.77 % (2965543)Instructions burned: 249 (million)
% 2.55/0.77 % (2965580)Instruction limit reached!
% 2.55/0.77 % (2965580)------------------------------
% 2.55/0.77 % (2965580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965580)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965580)Termination reason: Instruction limit
% 3.13/0.84 % (2965580)Termination phase: Saturation
% 3.13/0.84 % (2965580)Time elapsed: 0.050 s
% 3.13/0.84 % (2965580)Peak memory usage: 14 MB
% 3.13/0.84 % (2965580)Instructions burned: 195 (million)
% 3.13/0.84 % (2965587)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=888913732:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 3.13/0.84 % (2965590)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 3.13/0.84 % (2965590)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=679336863:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 3.13/0.84 % (2965581)Instruction limit reached!
% 3.13/0.84 % (2965581)------------------------------
% 3.13/0.84 % (2965581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965581)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965581)Termination reason: Instruction limit
% 3.13/0.84 % (2965581)Termination phase: Property scanning
% 3.13/0.84 % (2965581)Time elapsed: 0.034 s
% 3.13/0.84 % (2965581)Peak memory usage: 11 MB
% 3.13/0.84 % (2965581)Instructions burned: 43 (million)
% 3.13/0.84 % (2965590)Instruction limit reached!
% 3.13/0.84 % (2965590)------------------------------
% 3.13/0.84 % (2965590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965590)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965590)Termination reason: Instruction limit
% 3.13/0.84 % (2965590)Termination phase: shuffling
% 3.13/0.84 % (2965590)Time elapsed: 0.003 s
% 3.13/0.84 % (2965590)Peak memory usage: 10 MB
% 3.13/0.84 % (2965590)Instructions burned: 11 (million)
% 3.13/0.84 % (2965594)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3195494569:i=19:add=on:rtra=on_2996 on theBenchmark for (2996ds/19Mi)
% 3.13/0.84 % (2965589)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=2797036767:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 3.13/0.84 % (2965594)Instruction limit reached!
% 3.13/0.84 % (2965594)------------------------------
% 3.13/0.84 % (2965594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965594)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965594)Termination reason: Instruction limit
% 3.13/0.84 % (2965594)Termination phase: shuffling
% 3.13/0.84 % (2965594)Time elapsed: 0.005 s
% 3.13/0.84 % (2965594)Peak memory usage: 10 MB
% 3.13/0.84 % (2965594)Instructions burned: 21 (million)
% 3.13/0.84 % (2965593)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2113160388:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 3.13/0.84 % (2965598)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=998634828:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 3.13/0.84 % (2965593)Instruction limit reached!
% 3.13/0.84 % (2965593)------------------------------
% 3.13/0.84 % (2965593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965593)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965593)Termination reason: Instruction limit
% 3.13/0.84 % (2965593)Termination phase: shuffling
% 3.13/0.84 % (2965593)Time elapsed: 0.010 s
% 3.13/0.84 % (2965593)Peak memory usage: 10 MB
% 3.13/0.84 % (2965593)Instructions burned: 23 (million)
% 3.13/0.84 % (2965600)dis+1004_4:1_slsqr=1,2:to=lpo:plsq=on:fde=unused:e2e=on:si=on:spb=goal_then_units:acc=on:urr=on:uwa=off:fd=preordered:s2agt=16:slsqc=1:slsq=on:random_seed=121379976:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2996 on theBenchmark for (2996ds/853Mi)
% 3.13/0.84 % (2965549)Instruction limit reached!
% 3.13/0.84 % (2965549)------------------------------
% 3.13/0.84 % (2965549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965549)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965549)Termination reason: Instruction limit
% 3.13/0.84 % (2965549)Termination phase: Saturation
% 3.13/0.84 % (2965549)Time elapsed: 0.268 s
% 3.13/0.84 % (2965549)Peak memory usage: 15 MB
% 3.13/0.84 % (2965549)Instructions burned: 327 (million)
% 3.13/0.84 % (2965577)Instruction limit reached!
% 3.13/0.84 % (2965577)------------------------------
% 3.13/0.84 % (2965577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965577)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965577)Termination reason: Instruction limit
% 3.13/0.84 % (2965577)Termination phase: Saturation
% 3.13/0.84 % (2965577)Time elapsed: 0.127 s
% 3.13/0.84 % (2965577)Peak memory usage: 12 MB
% 3.13/0.84 % (2965577)Instructions burned: 143 (million)
% 3.13/0.84 % (2965589)Instruction limit reached!
% 3.13/0.84 % (2965589)------------------------------
% 3.13/0.84 % (2965589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965589)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965589)Termination reason: Instruction limit
% 3.13/0.84 % (2965589)Termination phase: Saturation
% 3.13/0.84 % (2965589)Time elapsed: 0.091 s
% 3.13/0.84 % (2965589)Peak memory usage: 14 MB
% 3.13/0.84 % (2965589)Instructions burned: 170 (million)
% 3.13/0.84 % (2965598)Instruction limit reached!
% 3.13/0.84 % (2965598)------------------------------
% 3.13/0.84 % (2965598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965598)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965598)Termination reason: Instruction limit
% 3.13/0.84 % (2965598)Termination phase: Saturation
% 3.13/0.84 % (2965598)Time elapsed: 0.080 s
% 3.13/0.84 % (2965598)Peak memory usage: 16 MB
% 3.13/0.84 % (2965598)Instructions burned: 316 (million)
% 3.13/0.84 % (2965605)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.13/0.84 % (2965603)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3201786139:i=480:rtra=on_2995 on theBenchmark for (2995ds/480Mi)
% 3.13/0.84 % (2965605)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=40062183:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/200Mi)
% 3.13/0.84 % (2965604)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=518739176:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2995 on theBenchmark for (2995ds/21Mi)
% 3.13/0.84 % (2965604)Instruction limit reached!
% 3.13/0.84 % (2965604)------------------------------
% 3.13/0.84 % (2965604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965604)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965604)Termination reason: Instruction limit
% 3.13/0.84 % (2965604)Termination phase: shuffling
% 3.13/0.84 % (2965604)Time elapsed: 0.010 s
% 3.13/0.84 % (2965604)Peak memory usage: 10 MB
% 3.13/0.84 % (2965604)Instructions burned: 23 (million)
% 3.13/0.84 % (2965602)dis+1003_3:4_to=kbo:plsq=on:prc=on:sims=off:e2e=on:si=on:spb=intro:acc=on:urr=on:uwa=off:foolp=on:s2agt=32:slsqc=3:slsq=on:random_seed=470074711:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2995 on theBenchmark for (2995ds/45Mi)
% 3.13/0.84 % (2965587)Instruction limit reached!
% 3.13/0.84 % (2965587)------------------------------
% 3.13/0.84 % (2965587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965587)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965587)Termination reason: Instruction limit
% 3.13/0.84 % (2965587)Termination phase: Saturation
% 3.13/0.84 % (2965587)Time elapsed: 0.168 s
% 3.13/0.84 % (2965587)Peak memory usage: 14 MB
% 3.13/0.84 % (2965587)Instructions burned: 182 (million)
% 3.13/0.84 % (2965609)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=4207818604:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2995 on theBenchmark for (2995ds/13Mi)
% 3.13/0.84 % (2965609)Instruction limit reached!
% 3.13/0.84 % (2965609)------------------------------
% 3.13/0.84 % (2965609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965609)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965609)Termination reason: Instruction limit
% 3.13/0.84 % (2965609)Termination phase: shuffling
% 3.13/0.84 % (2965609)Time elapsed: 0.006 s
% 3.13/0.84 % (2965609)Peak memory usage: 10 MB
% 3.13/0.84 % (2965609)Instructions burned: 13 (million)
% 3.13/0.84 % (2965605)Instruction limit reached!
% 3.13/0.84 % (2965605)------------------------------
% 3.13/0.84 % (2965605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965605)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965605)Termination reason: Instruction limit
% 3.13/0.84 % (2965605)Termination phase: Saturation
% 3.13/0.84 % (2965605)Time elapsed: 0.052 s
% 3.13/0.84 % (2965605)Peak memory usage: 14 MB
% 3.13/0.84 % (2965605)Instructions burned: 202 (million)
% 3.13/0.84 % (2965611)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=4031507275:i=66:s2at=3:nm=2:rtra=on:rawr=on_2994 on theBenchmark for (2994ds/66Mi)
% 3.13/0.84 % (2965602)Instruction limit reached!
% 3.13/0.84 % (2965602)------------------------------
% 3.13/0.84 % (2965602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965602)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965602)Termination reason: Instruction limit
% 3.13/0.84 % (2965602)Termination phase: shuffling
% 3.13/0.84 % (2965602)Time elapsed: 0.041 s
% 3.13/0.84 % (2965602)Peak memory usage: 11 MB
% 3.13/0.84 % (2965602)Instructions burned: 45 (million)
% 3.13/0.84 % (2965613)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3889606173:i=51:fsr=off:rtra=on_2994 on theBenchmark for (2994ds/51Mi)
% 3.13/0.84 % (2965614)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=196336107:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/31Mi)
% 3.13/0.84 % (2965611)Instruction limit reached!
% 3.13/0.84 % (2965611)------------------------------
% 3.13/0.84 % (2965611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965611)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965611)Termination reason: Instruction limit
% 3.13/0.84 % (2965611)Termination phase: Property scanning
% 3.13/0.84 % (2965611)Time elapsed: 0.030 s
% 3.13/0.84 % (2965611)Peak memory usage: 11 MB
% 3.13/0.84 % (2965611)Instructions burned: 67 (million)
% 3.13/0.84 % (2965576) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2965509-2965576"...
% 3.13/0.84 % (2965576)...printing done.
% 3.13/0.84 % (2965613)Instruction limit reached!
% 3.13/0.84 % (2965613)------------------------------
% 3.13/0.84 % (2965613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965613)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965613)Termination reason: Instruction limit
% 3.13/0.84 % (2965613)Termination phase: Property scanning
% 3.13/0.84 % (2965613)Time elapsed: 0.023 s
% 3.13/0.84 % (2965613)Peak memory usage: 11 MB
% 3.13/0.84 % (2965613)Instructions burned: 53 (million)
% 3.13/0.84 % (2965576)Refutation found. Thanks to Tanya!
% 3.13/0.84 % SZS status Theorem for theBenchmark
% 3.13/0.84 % SZS output start Proof for theBenchmark
% See solution above
% 3.13/0.84 % (2965576)------------------------------
% 3.13/0.84 % (2965576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.13/0.84 % (2965576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.13/0.84 % (2965576)CaDiCaL version: 2.1.3
% 3.13/0.84 % (2965576)Termination reason: Refutation
% 3.13/0.84 % (2965576)Time elapsed: 0.281 s
% 3.13/0.84 % (2965576)Peak memory usage: 16 MB
% 3.13/0.84 % (2965576)Instructions burned: 355 (million)
% 3.13/0.84 % (2965509)Success in time 0.574 s
% 3.13/0.84 % Vampire exiting
%------------------------------------------------------------------------------