%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM926+8 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:26:14 PM UTC 2026
% Result : Theorem 144.66s 43.36s
% Output : Refutation 144.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 25
% Syntax : Number of formulae : 103 ( 60 unt; 4 def)
% Number of atoms : 153 ( 80 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 96 ( 46 ~; 40 |; 1 &)
% ( 5 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 5 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 15 con; 0-4 aty)
% Number of variables : 60 ( 0 sgn 48 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f272,axiom,
ti(int,t) = t,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_v_t_____res) ).
fof(f273,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_tpos) ).
fof(f274,axiom,
( t = one_one(int)
=> ? [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
fof(f275,axiom,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))
=> ? [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
fof(f295,axiom,
! [X0,X1] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X0),X1))
<=> ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),X1))
& ti(int,X0) != ti(int,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_22_zless__le) ).
fof(f361,axiom,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X0),X1) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X1),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_88_zmult__commute) ).
fof(f362,axiom,
! [X0] : hAPP(int,int,number_number_of(int),X0) = ti(int,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_89_number__of__is__id) ).
fof(f434,axiom,
one_one(int) = hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,pls)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_161_one__is__num__one) ).
fof(f1604,axiom,
one_one(nat) = hAPP(nat,nat,suc,zero_zero(nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1331_One__nat__def) ).
fof(f1699,axiom,
hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))) = hAPP(nat,nat,suc,hAPP(nat,nat,suc,zero_zero(nat))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1426_numeral__2__eq__2) ).
fof(f1866,axiom,
! [X0] : hAPP(int,int,succ,X0) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1593_succ__def) ).
fof(f2375,axiom,
! [X0] :
( number_ring(X0)
=> hAPP(X0,X0,uminus_uminus(X0),one_one(X0)) = hAPP(int,X0,number_number_of(X0),min_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2102_arith__simps_I31_J) ).
fof(f2413,axiom,
! [X0] : hAPP(int,int,uminus_uminus(int),hAPP(int,int,number_number_of(int),X0)) = hAPP(int,int,number_number_of(int),hAPP(int,int,uminus_uminus(int),X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2140_minus__numeral__code_I5_J) ).
fof(f2429,axiom,
min_1 = hAPP(int,int,uminus_uminus(int),one_one(int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2156_Int_OMin__def) ).
fof(f2436,axiom,
hAPP(int,int,uminus_uminus(int),min_1) = hAPP(int,int,bit1,pls),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2163_minus__Min) ).
fof(f3853,axiom,
! [X0] : hAPP(int,int,number_number_of(int),X0) = hAPP(int,int,ring_1_of_int(int),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3580_int__number__of__def) ).
fof(f3855,axiom,
! [X0] :
( ring_1(X0)
=> hAPP(int,X0,ring_1_of_int(X0),one_one(int)) = one_one(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3582_of__int__1) ).
fof(f5058,axiom,
! [X0,X1] : hAPP(fun(X0,bool),X0,hilbert_Eps(X0),hAPP(X0,fun(X0,bool),hAPP(fun(X0,fun(X0,bool)),fun(X0,fun(X0,bool)),combc(X0,X0,bool),fequal(X0)),X1)) = ti(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4785_some__eq__trivial) ).
fof(f5325,axiom,
number_ring(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Int_Oint___Int_Onumber__ring) ).
fof(f5331,axiom,
ring_1(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Oring__1) ).
fof(f5738,conjecture,
? [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f5739,negated_conjecture,
~ ? [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)),
inference(negated_conjecture,[status(cth)],[f5738]) ).
fof(f5883,plain,
( ? [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))
| t != one_one(int) ),
inference(ennf_transformation,[],[f274]) ).
fof(f5884,plain,
( ? [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(ennf_transformation,[],[f275]) ).
fof(f7934,plain,
! [X0] :
( hAPP(X0,X0,uminus_uminus(X0),one_one(X0)) = hAPP(int,X0,number_number_of(X0),min_1)
| ~ number_ring(X0) ),
inference(ennf_transformation,[],[f2375]) ).
fof(f9094,plain,
! [X0] :
( hAPP(int,X0,ring_1_of_int(X0),one_one(int)) = one_one(X0)
| ~ ring_1(X0) ),
inference(ennf_transformation,[],[f3855]) ).
fof(f10577,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) != hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)),
inference(ennf_transformation,[],[f5739]) ).
fof(f10850,plain,
t = ti(int,t),
inference(cnf_transformation,[],[f272]) ).
fof(f10851,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)),
inference(cnf_transformation,[],[f273]) ).
fof(f10852,plain,
( t != one_one(int)
| hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) ),
inference(cnf_transformation,[],[f5883]) ).
fof(f10853,plain,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))
| hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK2),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK3),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) ),
inference(cnf_transformation,[],[f5884]) ).
fof(f10875,plain,
! [X0,X1] :
( ti(int,X0) = ti(int,X1)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),X1))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X0),X1)) ),
inference(cnf_transformation,[],[f295]) ).
fof(f10967,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X1),X0) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X0),X1),
inference(cnf_transformation,[],[f361]) ).
fof(f10968,plain,
! [X0] : ti(int,X0) = hAPP(int,int,number_number_of(int),X0),
inference(cnf_transformation,[],[f362]) ).
fof(f11062,plain,
one_one(int) = hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,pls)),
inference(cnf_transformation,[],[f434]) ).
fof(f12752,plain,
one_one(nat) = hAPP(nat,nat,suc,zero_zero(nat)),
inference(cnf_transformation,[],[f1604]) ).
fof(f12893,plain,
hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))) = hAPP(nat,nat,suc,hAPP(nat,nat,suc,zero_zero(nat))),
inference(cnf_transformation,[],[f1699]) ).
fof(f13147,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int)) = hAPP(int,int,succ,X0),
inference(cnf_transformation,[],[f1866]) ).
fof(f13967,plain,
! [X0] :
( ~ number_ring(X0)
| hAPP(int,X0,number_number_of(X0),min_1) = hAPP(X0,X0,uminus_uminus(X0),one_one(X0)) ),
inference(cnf_transformation,[],[f7934]) ).
fof(f14026,plain,
! [X0] : hAPP(int,int,uminus_uminus(int),hAPP(int,int,number_number_of(int),X0)) = hAPP(int,int,number_number_of(int),hAPP(int,int,uminus_uminus(int),X0)),
inference(cnf_transformation,[],[f2413]) ).
fof(f14048,plain,
min_1 = hAPP(int,int,uminus_uminus(int),one_one(int)),
inference(cnf_transformation,[],[f2429]) ).
fof(f14055,plain,
hAPP(int,int,bit1,pls) = hAPP(int,int,uminus_uminus(int),min_1),
inference(cnf_transformation,[],[f2436]) ).
fof(f16096,plain,
! [X0] : hAPP(int,int,number_number_of(int),X0) = hAPP(int,int,ring_1_of_int(int),X0),
inference(cnf_transformation,[],[f3853]) ).
fof(f16098,plain,
! [X0] :
( ~ ring_1(X0)
| one_one(X0) = hAPP(int,X0,ring_1_of_int(X0),one_one(int)) ),
inference(cnf_transformation,[],[f9094]) ).
fof(f17910,plain,
! [X0,X1] : ti(X0,X1) = hAPP(fun(X0,bool),X0,hilbert_Eps(X0),hAPP(X0,fun(X0,bool),hAPP(fun(X0,fun(X0,bool)),fun(X0,fun(X0,bool)),combc(X0,X0,bool),fequal(X0)),X1)),
inference(cnf_transformation,[],[f5058]) ).
fof(f18339,plain,
number_ring(int),
inference(cnf_transformation,[],[f5325]) ).
fof(f18345,plain,
ring_1(int),
inference(cnf_transformation,[],[f5331]) ).
fof(f18752,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) != hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)),
inference(cnf_transformation,[],[f10577]) ).
fof(f19025,plain,
t = hAPP(fun(int,bool),int,hilbert_Eps(int),hAPP(int,fun(int,bool),hAPP(fun(int,fun(int,bool)),fun(int,fun(int,bool)),combc(int,int,bool),fequal(int)),t)),
inference(definition_unfolding,[],[f10850,f17910]) ).
fof(f19026,plain,
! [X0,X1] :
( hAPP(fun(int,bool),int,hilbert_Eps(int),hAPP(int,fun(int,bool),hAPP(fun(int,fun(int,bool)),fun(int,fun(int,bool)),combc(int,int,bool),fequal(int)),X0)) = hAPP(fun(int,bool),int,hilbert_Eps(int),hAPP(int,fun(int,bool),hAPP(fun(int,fun(int,bool)),fun(int,fun(int,bool)),combc(int,int,bool),fequal(int)),X1))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),X1))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X0),X1)) ),
inference(definition_unfolding,[],[f10875,f17910,f17910]) ).
fof(f19039,plain,
! [X0] : hAPP(int,int,number_number_of(int),X0) = hAPP(fun(int,bool),int,hilbert_Eps(int),hAPP(int,fun(int,bool),hAPP(fun(int,fun(int,bool)),fun(int,fun(int,bool)),combc(int,int,bool),fequal(int)),X0)),
inference(definition_unfolding,[],[f10968,f17910]) ).
fof(f20350,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)),
inference(consistent_polarity_flipping,[],[f10851]) ).
fof(f20351,plain,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))
| hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK2),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK3),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) ),
inference(consistent_polarity_flipping,[],[f10853]) ).
fof(f20363,plain,
! [X0,X1] :
( hAPP(fun(int,bool),int,hilbert_Eps(int),hAPP(int,fun(int,bool),hAPP(fun(int,fun(int,bool)),fun(int,fun(int,bool)),combc(int,int,bool),fequal(int)),X0)) = hAPP(fun(int,bool),int,hilbert_Eps(int),hAPP(int,fun(int,bool),hAPP(fun(int,fun(int,bool)),fun(int,fun(int,bool)),combc(int,int,bool),fequal(int)),X1))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),X1))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X0),X1)) ),
inference(consistent_polarity_flipping,[],[f19026]) ).
fof(f22778,plain,
! [X0] :
( number_ring(X0)
| hAPP(int,X0,number_number_of(X0),min_1) = hAPP(X0,X0,uminus_uminus(X0),one_one(X0)) ),
inference(consistent_polarity_flipping,[],[f13967]) ).
fof(f26050,plain,
~ number_ring(int),
inference(consistent_polarity_flipping,[],[f18339]) ).
fof(f26288,definition,
( spl869_13
<=> hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK2),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK3),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) ),
introduced(definition,[new_symbols(definition,[spl869_13])],[avatar_definition]) ).
fof(f26290,plain,
( hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK2),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK3),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))))
| ~ spl869_13 ),
inference(avatar_component_clause,[],[f26288]) ).
fof(f26292,definition,
( spl869_14
<=> hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
introduced(definition,[new_symbols(definition,[spl869_14])],[avatar_definition]) ).
fof(f26294,plain,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))
| ~ spl869_14 ),
inference(avatar_component_clause,[],[f26292]) ).
fof(f26295,plain,
( spl869_13
| spl869_14 ),
inference(avatar_split_clause,[],[f20351,f26292,f26288]) ).
fof(f26297,definition,
( spl869_15
<=> hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) ),
introduced(definition,[new_symbols(definition,[spl869_15])],[avatar_definition]) ).
fof(f26299,plain,
( hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))))
| ~ spl869_15 ),
inference(avatar_component_clause,[],[f26297]) ).
fof(f26301,definition,
( spl869_16
<=> t = one_one(int) ),
introduced(definition,[new_symbols(definition,[spl869_16])],[avatar_definition]) ).
fof(f26304,plain,
( spl869_15
| ~ spl869_16 ),
inference(avatar_split_clause,[],[f10852,f26301,f26297]) ).
fof(f26431,plain,
one_one(int) = hAPP(int,int,ring_1_of_int(int),one_one(int)),
inference(resolution,[],[f16098,f18345]) ).
fof(f26487,plain,
one_one(int) = hAPP(int,int,number_number_of(int),one_one(int)),
inference(superposition,[],[f26431,f16096]) ).
fof(f26736,plain,
hAPP(int,int,number_number_of(int),min_1) = hAPP(int,int,uminus_uminus(int),one_one(int)),
inference(resolution,[],[f22778,f26050]) ).
fof(f26741,plain,
min_1 = hAPP(int,int,number_number_of(int),min_1),
inference(forward_demodulation,[],[f26736,f14048]) ).
fof(f32835,plain,
hAPP(int,int,uminus_uminus(int),min_1) = hAPP(int,int,number_number_of(int),hAPP(int,int,uminus_uminus(int),min_1)),
inference(superposition,[],[f14026,f26741]) ).
fof(f32843,plain,
hAPP(int,int,bit1,pls) = hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,pls)),
inference(forward_demodulation,[],[f32835,f14055]) ).
fof(f32845,plain,
one_one(int) = hAPP(int,int,bit1,pls),
inference(forward_demodulation,[],[f32843,f11062]) ).
fof(f39748,plain,
hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))) = hAPP(nat,nat,suc,one_one(nat)),
inference(forward_demodulation,[],[f12893,f12752]) ).
fof(f39749,plain,
hAPP(nat,nat,suc,one_one(nat)) = hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int))),
inference(forward_demodulation,[],[f39748,f32845]) ).
fof(f85331,plain,
t = hAPP(int,int,number_number_of(int),t),
inference(superposition,[],[f19039,f19025]) ).
fof(f684672,plain,
! [X0,X1] :
( hAPP(int,int,number_number_of(int),X1) = hAPP(fun(int,bool),int,hilbert_Eps(int),hAPP(int,fun(int,bool),hAPP(fun(int,fun(int,bool)),fun(int,fun(int,bool)),combc(int,int,bool),fequal(int)),X0))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),X1))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X0),X1)) ),
inference(forward_demodulation,[],[f20363,f19039]) ).
fof(f684673,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X0),X1))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),X1))
| hAPP(int,int,number_number_of(int),X0) = hAPP(int,int,number_number_of(int),X1) ),
inference(forward_demodulation,[],[f684672,f19039]) ).
fof(f844829,plain,
( $false
| ~ spl869_13 ),
inference(forward_subsumption_resolution,[],[f26290,f18752]) ).
fof(f844830,plain,
~ spl869_13,
inference(avatar_contradiction_clause,[],[f844829]) ).
fof(f844868,plain,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t))
| hAPP(int,int,number_number_of(int),one_one(int)) = hAPP(int,int,number_number_of(int),t)
| ~ spl869_14 ),
inference(resolution,[],[f26294,f684673]) ).
fof(f844945,plain,
( hAPP(int,int,number_number_of(int),one_one(int)) = hAPP(int,int,number_number_of(int),t)
| ~ spl869_14 ),
inference(forward_subsumption_resolution,[],[f844868,f20350]) ).
fof(f844957,plain,
( t = hAPP(int,int,number_number_of(int),one_one(int))
| ~ spl869_14 ),
inference(forward_demodulation,[],[f844945,f85331]) ).
fof(f959732,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) != hAPP(int,int,succ,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),
inference(forward_demodulation,[],[f18752,f13147]) ).
fof(f959749,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))) != hAPP(int,int,succ,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),m),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))))),
inference(forward_demodulation,[],[f959732,f10967]) ).
fof(f959753,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int))))) != hAPP(int,int,succ,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),m),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int)))))),
inference(forward_demodulation,[],[f959749,f32845]) ).
fof(f959755,plain,
! [X0,X1] : hAPP(int,int,succ,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),m),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int)))))) != hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X0),hAPP(nat,nat,suc,one_one(nat)))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X1),hAPP(nat,nat,suc,one_one(nat)))),
inference(forward_demodulation,[],[f959753,f39749]) ).
fof(f1088412,plain,
( t = one_one(int)
| ~ spl869_14 ),
inference(superposition,[],[f26487,f844957]) ).
fof(f1088833,plain,
( hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m)),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int))))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK1),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int)))))
| ~ spl869_15 ),
inference(forward_demodulation,[],[f26299,f32845]) ).
fof(f1088867,plain,
( spl869_16
| ~ spl869_14 ),
inference(avatar_split_clause,[],[f1088412,f26292,f26301]) ).
fof(f1088869,plain,
( hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m)),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK0),hAPP(nat,nat,suc,one_one(nat)))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK1),hAPP(nat,nat,suc,one_one(nat))))
| ~ spl869_15 ),
inference(forward_demodulation,[],[f1088833,f39749]) ).
fof(f1088875,plain,
( hAPP(int,int,succ,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m)) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK0),hAPP(nat,nat,suc,one_one(nat)))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK1),hAPP(nat,nat,suc,one_one(nat))))
| ~ spl869_15 ),
inference(forward_demodulation,[],[f1088869,f13147]) ).
fof(f1088876,plain,
( hAPP(int,int,succ,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),m),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int)))))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK0),hAPP(nat,nat,suc,one_one(nat)))),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),sK1),hAPP(nat,nat,suc,one_one(nat))))
| ~ spl869_15 ),
inference(forward_demodulation,[],[f1088875,f10967]) ).
fof(f1088877,plain,
( $false
| ~ spl869_15 ),
inference(forward_subsumption_resolution,[],[f1088876,f959755]) ).
fof(f1088878,plain,
~ spl869_15,
inference(avatar_contradiction_clause,[],[f1088877]) ).
cnf(s12,plain,
( spl869_13
| spl869_14 ),
inference(sat_conversion,[],[f26295]) ).
cnf(s13,plain,
( spl869_15
| ~ spl869_16 ),
inference(sat_conversion,[],[f26304]) ).
cnf(s50239,plain,
~ spl869_13,
inference(sat_conversion,[],[f844830]) ).
cnf(s66133,plain,
( ~ spl869_14
| spl869_16 ),
inference(sat_conversion,[],[f1088867]) ).
cnf(s66138,plain,
~ spl869_15,
inference(sat_conversion,[],[f1088878]) ).
cnf(s68403,plain,
~ spl869_16,
inference(rat,[],[s13,s66138]) ).
cnf(s68404,plain,
~ spl869_14,
inference(rat,[],[s66133,s68403]) ).
cnf(s68422,plain,
$false,
inference(rat,[],[s12,s68404,s50239]) ).
fof(f1088879,plain,
$false,
inference(avatar_sat_refutation,[],[s68422]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM926+8 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n009.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 21:45:15 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.90/4.81 % (2427945)Will run a generic schedule for satisfiability detection.
% 26.90/4.81 % (2427951)% WARNING: option uhcvi not known.
% 26.90/4.81 % (2427951)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2005926052:i=135531:add=off:rawr=on_2993 on theBenchmark for (2993ds/135531Mi)
% 26.90/4.81 % (2427950)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1021391603_2993 on theBenchmark for (2993ds/0Mi)
% 26.90/4.81 % (2427952)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=6382617:i=88024:add=on:rawr=on_2993 on theBenchmark for (2993ds/88024Mi)
% 26.90/4.81 % (2427953)dis+10_1_sil=32000:sp=arity:random_seed=2514239221:i=103:fgj=on_2993 on theBenchmark for (2993ds/103Mi)
% 26.90/4.81 % (2427955)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3942940987:i=131_2993 on theBenchmark for (2993ds/131Mi)
% 26.90/4.81 % (2427954)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2645460814:i=116_2993 on theBenchmark for (2993ds/116Mi)
% 26.90/4.81 % (2427956)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=627803267:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2993 on theBenchmark for (2993ds/159Mi)
% 26.90/4.81 % (2427953)Instruction limit reached!
% 26.90/4.81 % (2427953)------------------------------
% 26.90/4.81 % (2427953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.90/4.81 % (2427953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.90/4.81 % (2427953)CaDiCaL version: 2.1.3
% 26.90/4.81 % (2427953)Termination reason: Instruction limit
% 26.90/4.81 % (2427953)Termination phase: Preprocessing 3
% 26.90/4.81 % (2427953)Time elapsed: 0.060 s
% 26.90/4.81 % (2427953)Peak memory usage: 21 MB
% 26.90/4.81 % (2427953)Instructions burned: 105 (million)
% 26.90/4.81 % (2427954)Instruction limit reached!
% 26.90/4.81 % (2427954)------------------------------
% 26.90/4.81 % (2427954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.90/4.81 % (2427954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.90/4.81 % (2427954)CaDiCaL version: 2.1.3
% 26.90/4.81 % (2427954)Termination reason: Instruction limit
% 26.90/4.81 % (2427954)Termination phase: NewCNF
% 26.90/4.81 % (2427954)Time elapsed: 0.071 s
% 26.90/4.81 % (2427954)Peak memory usage: 22 MB
% 26.90/4.81 % (2427954)Instructions burned: 117 (million)
% 26.90/4.81 % (2427955)Instruction limit reached!
% 26.90/4.81 % (2427955)------------------------------
% 26.90/4.81 % (2427955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.90/4.81 % (2427955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.90/4.81 % (2427955)CaDiCaL version: 2.1.3
% 26.90/4.81 % (2427955)Termination reason: Instruction limit
% 26.90/4.81 % (2427955)Termination phase: Preprocessing 3
% 26.90/4.81 % (2427955)Time elapsed: 0.072 s
% 26.90/4.81 % (2427955)Peak memory usage: 21 MB
% 26.90/4.81 % (2427955)Instructions burned: 131 (million)
% 26.90/4.81 % (2427964)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1050846428:i=714:nm=2_2992 on theBenchmark for (2992ds/714Mi)
% 26.90/4.81 % (2427956)Instruction limit reached!
% 26.90/4.81 % (2427956)------------------------------
% 26.90/4.81 % (2427956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.90/4.81 % (2427956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.90/4.81 % (2427956)CaDiCaL version: 2.1.3
% 26.90/4.81 % (2427956)Termination reason: Instruction limit
% 26.90/4.81 % (2427956)Termination phase: Preprocessing 3
% 26.90/4.81 % (2427956)Time elapsed: 0.087 s
% 26.90/4.81 % (2427956)Peak memory usage: 22 MB
% 26.90/4.81 % (2427956)Instructions burned: 160 (million)
% 26.90/4.81 % (2427965)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2917207435:i=131:bd=preordered:fsd=on_2992 on theBenchmark for (2992ds/131Mi)
% 26.90/4.81 % (2427966)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1958448480:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2992 on theBenchmark for (2992ds/684Mi)
% 26.90/4.81 % (2427968)ott-21_1_sil=16000:fs=off:random_seed=424771089:i=180:av=off:fsr=off_2992 on theBenchmark for (2992ds/180Mi)
% 26.90/4.81 % (2427965)Instruction limit reached!
% 26.90/4.81 % (2427965)------------------------------
% 26.90/4.81 % (2427965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.90/4.81 % (2427965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.56/8.99 % (2427965)CaDiCaL version: 2.1.3
% 55.56/8.99 % (2427965)Termination reason: Instruction limit
% 55.56/8.99 % (2427965)Termination phase: Preprocessing 3
% 55.56/8.99 % (2427965)Time elapsed: 0.070 s
% 55.56/8.99 % (2427965)Peak memory usage: 21 MB
% 55.56/8.99 % (2427965)Instructions burned: 131 (million)
% 55.56/8.99 % (2427972)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3603861180:i=477:bd=all_2991 on theBenchmark for (2991ds/477Mi)
% 55.56/8.99 % (2427968)Instruction limit reached!
% 55.56/8.99 % (2427968)------------------------------
% 55.56/8.99 % (2427968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.56/8.99 % (2427968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.56/8.99 % (2427968)CaDiCaL version: 2.1.3
% 55.56/8.99 % (2427968)Termination reason: Instruction limit
% 55.56/8.99 % (2427968)Termination phase: Preprocessing 3
% 55.56/8.99 % (2427968)Time elapsed: 0.094 s
% 55.56/8.99 % (2427968)Peak memory usage: 22 MB
% 55.56/8.99 % (2427968)Instructions burned: 180 (million)
% 55.56/8.99 % (2427974)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4016786774:fmbsr=1.3:i=865:ins=25_2990 on theBenchmark for (2990ds/865Mi)
% 55.56/9.00 % (2427964)Instruction limit reached!
% 55.56/9.00 % (2427964)------------------------------
% 55.56/9.00 % (2427964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.56/9.00 % (2427964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.56/9.00 % (2427964)CaDiCaL version: 2.1.3
% 55.56/9.00 % (2427964)Termination reason: Instruction limit
% 55.56/9.00 % (2427964)Termination phase: Function definition elimination
% 55.56/9.00 % (2427964)Time elapsed: 0.312 s
% 55.56/9.00 % (2427964)Peak memory usage: 26 MB
% 55.56/9.00 % (2427964)Instructions burned: 714 (million)
% 55.56/9.00 % (2427966)Instruction limit reached!
% 55.56/9.00 % (2427966)------------------------------
% 55.56/9.00 % (2427966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.56/9.00 % (2427966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.56/9.00 % (2427966)CaDiCaL version: 2.1.3
% 55.56/9.00 % (2427966)Termination reason: Instruction limit
% 55.56/9.00 % (2427966)Termination phase: Property scanning
% 55.56/9.00 % (2427966)Time elapsed: 0.304 s
% 55.56/9.00 % (2427966)Peak memory usage: 25 MB
% 55.56/9.00 % (2427966)Instructions burned: 685 (million)
% 55.56/9.00 % (2427972)Instruction limit reached!
% 55.56/9.00 % (2427972)------------------------------
% 55.56/9.00 % (2427972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.56/9.00 % (2427972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.56/9.00 % (2427972)CaDiCaL version: 2.1.3
% 55.56/9.00 % (2427972)Termination reason: Instruction limit
% 55.56/9.00 % (2427972)Termination phase: Property scanning
% 55.56/9.00 % (2427972)Time elapsed: 0.212 s
% 55.56/9.00 % (2427972)Peak memory usage: 24 MB
% 55.56/9.00 % (2427972)Instructions burned: 478 (million)
% 55.56/9.00 % (2427976)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2960567193:i=1179_2988 on theBenchmark for (2988ds/1179Mi)
% 55.56/9.00 % (2427977)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1994322519:i=889:ins=1_2988 on theBenchmark for (2988ds/889Mi)
% 55.56/9.00 % (2427978)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1534911124:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2988 on theBenchmark for (2988ds/692Mi)
% 55.56/9.00 % (2427974)Instruction limit reached!
% 55.56/9.00 % (2427974)------------------------------
% 55.56/9.00 % (2427974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.56/9.00 % (2427974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.56/9.00 % (2427974)CaDiCaL version: 2.1.3
% 55.56/9.00 % (2427974)Termination reason: Instruction limit
% 55.56/9.00 % (2427974)Termination phase: Property scanning
% 55.56/9.00 % (2427974)Time elapsed: 0.359 s
% 55.56/9.00 % (2427974)Peak memory usage: 25 MB
% 55.56/9.00 % (2427974)Instructions burned: 866 (million)
% 55.56/9.00 % (2427983)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=830161011:i=879:kws=inv_precedence:fsr=off_2987 on theBenchmark for (2987ds/879Mi)
% 55.56/9.00 % (2427978)Instruction limit reached!
% 55.56/9.00 % (2427978)------------------------------
% 55.56/9.00 % (2427978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 55.56/9.00 % (2427978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.62/18.32 % (2427978)CaDiCaL version: 2.1.3
% 122.62/18.32 % (2427978)Termination reason: Instruction limit
% 122.62/18.32 % (2427978)Termination phase: Property scanning
% 122.62/18.32 % (2427978)Time elapsed: 0.307 s
% 122.62/18.32 % (2427978)Peak memory usage: 25 MB
% 122.62/18.32 % (2427978)Instructions burned: 694 (million)
% 122.62/18.32 % (2427985)fmb+10_1_sil=64000:random_seed=3043355110:i=22061:nm=2:gsp=on_2985 on theBenchmark for (2985ds/22061Mi)
% 122.62/18.32 % (2427977)Instruction limit reached!
% 122.62/18.32 % (2427977)------------------------------
% 122.62/18.32 % (2427977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.62/18.32 % (2427977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.62/18.32 % (2427977)CaDiCaL version: 2.1.3
% 122.62/18.32 % (2427977)Termination reason: Instruction limit
% 122.62/18.32 % (2427977)Termination phase: Property scanning
% 122.62/18.32 % (2427977)Time elapsed: 0.369 s
% 122.62/18.32 % (2427977)Peak memory usage: 25 MB
% 122.62/18.32 % (2427977)Instructions burned: 891 (million)
% 122.62/18.32 % (2427987)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2746274388:i=9515:nm=5_2985 on theBenchmark for (2985ds/9515Mi)
% 122.62/18.32 % (2427976)Instruction limit reached!
% 122.62/18.32 % (2427976)------------------------------
% 122.62/18.32 % (2427976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.62/18.32 % (2427976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.62/18.32 % (2427976)CaDiCaL version: 2.1.3
% 122.62/18.32 % (2427976)Termination reason: Instruction limit
% 122.62/18.32 % (2427976)Termination phase: Property scanning
% 122.62/18.32 % (2427976)Time elapsed: 0.475 s
% 122.62/18.32 % (2427976)Peak memory usage: 25 MB
% 122.62/18.32 % (2427976)Instructions burned: 1181 (million)
% 122.62/18.32 % (2427989)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3194502903:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 122.62/18.32 % (2427983)Instruction limit reached!
% 122.62/18.32 % (2427983)------------------------------
% 122.62/18.32 % (2427983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.62/18.32 % (2427983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.62/18.32 % (2427983)CaDiCaL version: 2.1.3
% 122.62/18.32 % (2427983)Termination reason: Instruction limit
% 122.62/18.32 % (2427983)Termination phase: Property scanning
% 122.62/18.32 % (2427983)Time elapsed: 0.375 s
% 122.62/18.32 % (2427983)Peak memory usage: 25 MB
% 122.62/18.32 % (2427983)Instructions burned: 880 (million)
% 122.62/18.32 % (2427991)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1921379857:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 122.62/18.32 % (2427989)Instruction limit reached!
% 122.62/18.32 % (2427989)------------------------------
% 122.62/18.32 % (2427989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.62/18.32 % (2427989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.62/18.32 % (2427989)CaDiCaL version: 2.1.3
% 122.62/18.32 % (2427989)Termination reason: Instruction limit
% 122.62/18.32 % (2427989)Termination phase: Property scanning
% 122.62/18.32 % (2427989)Time elapsed: 0.380 s
% 122.62/18.32 % (2427989)Peak memory usage: 25 MB
% 122.62/18.32 % (2427989)Instructions burned: 920 (million)
% 122.62/18.32 % (2427993)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=628558717:i=1472:ins=7:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/1472Mi)
% 122.62/18.32 % (2427993)Instruction limit reached!
% 122.62/18.32 % (2427993)------------------------------
% 122.62/18.32 % (2427993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.62/18.32 % (2427993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.62/18.32 % (2427993)CaDiCaL version: 2.1.3
% 122.62/18.32 % (2427993)Termination reason: Instruction limit
% 122.62/18.32 % (2427993)Termination phase: Saturation
% 122.62/18.32 % (2427993)Time elapsed: 0.626 s
% 122.62/18.32 % (2427993)Peak memory usage: 29 MB
% 122.62/18.32 % (2427993)Instructions burned: 1472 (million)
% 122.62/18.32 % (2427995)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=932421016:i=6324_2973 on theBenchmark for (2973ds/6324Mi)
% 122.62/18.32 % (2427991)Instruction limit reached!
% 122.62/18.32 % (2427991)------------------------------
% 122.62/18.32 % (2427991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 122.62/18.32 % (2427991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.62/18.32 % (2427991)CaDiCaL version: 2.1.3
% 122.62/18.32 % (2427991)Termination reason: Instruction limit
% 122.62/18.32 % (2427991)Termination phase: Saturation
% 144.66/43.36 % (2427991)Time elapsed: 2.665 s
% 144.66/43.36 % (2427991)Peak memory usage: 48 MB
% 144.66/43.36 % (2427991)Instructions burned: 5131 (million)
% 144.66/43.36 % (2427997)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4289011140:fmbsr=2.30978:i=2174_2956 on theBenchmark for (2956ds/2174Mi)
% 144.66/43.36 % (2427997)Instruction limit reached!
% 144.66/43.36 % (2427997)------------------------------
% 144.66/43.36 % (2427997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.36 % (2427997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.36 % (2427997)CaDiCaL version: 2.1.3
% 144.66/43.36 % (2427997)Termination reason: Instruction limit
% 144.66/43.36 % (2427997)Termination phase: Finite model building preprocessing
% 144.66/43.36 % (2427997)Time elapsed: 0.898 s
% 144.66/43.36 % (2427997)Peak memory usage: 39 MB
% 144.66/43.36 % (2427997)Instructions burned: 2175 (million)
% 144.66/43.36 % (2427999)ott-2_1_sil=16000:newcnf=on:random_seed=3504197776:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2946 on theBenchmark for (2946ds/869Mi)
% 144.66/43.36 % (2427999)Instruction limit reached!
% 144.66/43.36 % (2427999)------------------------------
% 144.66/43.36 % (2427999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.36 % (2427999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.36 % (2427999)CaDiCaL version: 2.1.3
% 144.66/43.36 % (2427999)Termination reason: Instruction limit
% 144.66/43.36 % (2427999)Termination phase: Property scanning
% 144.66/43.36 % (2427999)Time elapsed: 0.361 s
% 144.66/43.36 % (2427999)Peak memory usage: 25 MB
% 144.66/43.36 % (2427999)Instructions burned: 869 (million)
% 144.66/43.36 % (2428001)ott+10_1_sil=32000:tgt=ground:random_seed=3381562388:i=5114:av=off_2943 on theBenchmark for (2943ds/5114Mi)
% 144.66/43.36 % (2427995)Instruction limit reached!
% 144.66/43.36 % (2427995)------------------------------
% 144.66/43.36 % (2427995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.36 % (2427995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.36 % (2427995)CaDiCaL version: 2.1.3
% 144.66/43.36 % (2427995)Termination reason: Instruction limit
% 144.66/43.36 % (2427995)Termination phase: Finite model building preprocessing
% 144.66/43.36 % (2427995)Time elapsed: 3.045 s
% 144.66/43.36 % (2427995)Peak memory usage: 62 MB
% 144.66/43.36 % (2427995)Instructions burned: 6325 (million)
% 144.66/43.36 % (2428003)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3118274517:i=54282_2942 on theBenchmark for (2942ds/54282Mi)
% 144.66/43.36 % (2427987)Instruction limit reached!
% 144.66/43.36 % (2427987)------------------------------
% 144.66/43.36 % (2427987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.36 % (2427987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.36 % (2427987)CaDiCaL version: 2.1.3
% 144.66/43.36 % (2427987)Termination reason: Instruction limit
% 144.66/43.36 % (2427987)Termination phase: Finite model building preprocessing
% 144.66/43.36 % (2427987)Time elapsed: 4.742 s
% 144.66/43.36 % (2427987)Peak memory usage: 75 MB
% 144.66/43.36 % (2427987)Instructions burned: 9516 (million)
% 144.66/43.36 % (2428005)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1286411100:i=3512:aac=none_2937 on theBenchmark for (2937ds/3512Mi)
% 144.66/43.36 % (2428005)Instruction limit reached!
% 144.66/43.36 % (2428005)------------------------------
% 144.66/43.36 % (2428005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.36 % (2428005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.36 % (2428005)CaDiCaL version: 2.1.3
% 144.66/43.36 % (2428005)Termination reason: Instruction limit
% 144.66/43.36 % (2428005)Termination phase: Saturation
% 144.66/43.36 % (2428005)Time elapsed: 1.762 s
% 144.66/43.36 % (2428005)Peak memory usage: 44 MB
% 144.66/43.36 % (2428005)Instructions burned: 3513 (million)
% 144.66/43.36 % (2428007)dis+21_1_sil=32000:sas=cadical:random_seed=2734150601:i=3773:amm=off_2919 on theBenchmark for (2919ds/3773Mi)
% 144.66/43.36 % (2428001)Instruction limit reached!
% 144.66/43.36 % (2428001)------------------------------
% 144.66/43.36 % (2428001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.36 % (2428001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.36 % (2428001)CaDiCaL version: 2.1.3
% 144.66/43.36 % (2428001)Termination reason: Instruction limit
% 144.66/43.36 % (2428001)Termination phase: Saturation
% 144.66/43.36 % (2428001)Time elapsed: 2.858 s
% 144.66/43.36 % (2428001)Peak memory usage: 57 MB
% 144.66/43.36 % (2428001)Instructions burned: 5115 (million)
% 144.66/43.36 % (2428009)ott+11_1_sil=16000:gs=on:random_seed=4093860680:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2914 on theBenchmark for (2914ds/2251Mi)
% 144.66/43.36 % (2428009)Instruction limit reached!
% 144.66/43.36 % (2428009)------------------------------
% 144.66/43.36 % (2428009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.36 % (2428009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.36 % (2428009)CaDiCaL version: 2.1.3
% 144.66/43.36 % (2428009)Termination reason: Instruction limit
% 144.66/43.36 % (2428009)Termination phase: Saturation
% 144.66/43.36 % (2428009)Time elapsed: 1.073 s
% 144.66/43.36 % (2428009)Peak memory usage: 35 MB
% 144.66/43.36 % (2428009)Instructions burned: 2251 (million)
% 144.66/43.36 % (2428011)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3140926764:fmbsr=1.6:i=67534_2903 on theBenchmark for (2903ds/67534Mi)
% 144.66/43.36 % (2428007)Instruction limit reached!
% 144.66/43.36 % (2428007)------------------------------
% 144.66/43.36 % (2428007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.36 % (2428007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.36 % (2428007)CaDiCaL version: 2.1.3
% 144.66/43.36 % (2428007)Termination reason: Instruction limit
% 144.66/43.36 % (2428007)Termination phase: Saturation
% 144.66/43.36 % (2428007)Time elapsed: 1.934 s
% 144.66/43.36 % (2428007)Peak memory usage: 48 MB
% 144.66/43.36 % (2428007)Instructions burned: 3774 (million)
% 144.66/43.36 % (2428013)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=120875148:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2899 on theBenchmark for (2899ds/4591Mi)
% 144.66/43.36 % (2428013)Instruction limit reached!
% 144.66/43.36 % (2428013)------------------------------
% 144.66/43.36 % (2428013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.36 % (2428013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.36 % (2428013)CaDiCaL version: 2.1.3
% 144.66/43.36 % (2428013)Termination reason: Instruction limit
% 144.66/43.36 % (2428013)Termination phase: Saturation
% 144.66/43.36 % (2428013)Time elapsed: 1.845 s
% 144.66/43.36 % (2428013)Peak memory usage: 35 MB
% 144.66/43.36 % (2428013)Instructions burned: 4593 (million)
% 144.66/43.36 % (2428015)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4057029589:i=29340_2881 on theBenchmark for (2881ds/29340Mi)
% 144.66/43.36 % (2427985)Instruction limit reached!
% 144.66/43.36 % (2427985)------------------------------
% 144.66/43.36 % (2427985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.36 % (2427985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.36 % (2427985)CaDiCaL version: 2.1.3
% 144.66/43.36 % (2427985)Termination reason: Instruction limit
% 144.66/43.36 % (2427985)Termination phase: Finite model building preprocessing
% 144.66/43.36 % (2427985)Time elapsed: 11.700 s
% 144.66/43.36 % (2427985)Peak memory usage: 121 MB
% 144.66/43.36 % (2427985)Instructions burned: 22061 (million)
% 144.66/43.36 % (2428017)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=294111656:i=5211_2868 on theBenchmark for (2868ds/5211Mi)
% 144.66/43.36 % (2428017)Instruction limit reached!
% 144.66/43.36 % (2428017)------------------------------
% 144.66/43.36 % (2428017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.36 % (2428017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.36 % (2428017)CaDiCaL version: 2.1.3
% 144.66/43.36 % (2428017)Termination reason: Instruction limit
% 144.66/43.36 % (2428017)Termination phase: Saturation
% 144.66/43.36 % (2428017)Time elapsed: 2.026 s
% 144.66/43.36 % (2428017)Peak memory usage: 45 MB
% 144.66/43.36 % (2428017)Instructions burned: 5213 (million)
% 144.66/43.36 % (2428019)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3675783866:i=5497:nm=2_2847 on theBenchmark for (2847ds/5497Mi)
% 144.66/43.36 % (2428019)Instruction limit reached!
% 144.66/43.36 % (2428019)------------------------------
% 144.66/43.36 % (2428019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.36 % (2428019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.36 % (2428019)CaDiCaL version: 2.1.3
% 144.66/43.36 % (2428019)Termination reason: Instruction limit
% 144.66/43.36 % (2428019)Termination phase: Finite model building preprocessing
% 144.66/43.36 % (2428019)Time elapsed: 2.648 s
% 144.66/43.36 % (2428019)Peak memory usage: 61 MB
% 144.66/43.36 % (2428019)Instructions burned: 5498 (million)
% 144.66/43.36 % (2428021)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2847903125:fmbsr=2:i=46332_2821 on theBenchmark for (2821ds/46332Mi)
% 144.66/43.36 % (2428015)Instruction limit reached!
% 144.66/43.36 % (2428015)------------------------------
% 144.66/43.36 % (2428015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.36 % (2428015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.36 % (2428015)CaDiCaL version: 2.1.3
% 144.66/43.36 % (2428015)Termination reason: Instruction limit
% 144.66/43.36 % (2428015)Termination phase: Saturation
% 144.66/43.36 % (2428015)Time elapsed: 12.928 s
% 144.66/43.36 % (2428015)Peak memory usage: 439 MB
% 144.66/43.36 % (2428015)Instructions burned: 29340 (million)
% 144.66/43.36 % (2428023)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3169894371:i=14071_2751 on theBenchmark for (2751ds/14071Mi)
% 144.66/43.36 % (2428023)Instruction limit reached!
% 144.66/43.36 % (2428023)------------------------------
% 144.66/43.36 % (2428023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.36 % (2428023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.36 % (2428023)CaDiCaL version: 2.1.3
% 144.66/43.36 % (2428023)Termination reason: Instruction limit
% 144.66/43.36 % (2428023)Termination phase: Finite model building preprocessing
% 144.66/43.36 % (2428023)Time elapsed: 7.259 s
% 144.66/43.36 % (2428023)Peak memory usage: 88 MB
% 144.66/43.36 % (2428023)Instructions burned: 14072 (million)
% 144.66/43.36 % (2428025)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3595736820:i=22565:add=on:rawr=on_2678 on theBenchmark for (2678ds/22565Mi)
% 144.66/43.36 % (2428003)Instruction limit reached!
% 144.66/43.36 % (2428003)------------------------------
% 144.66/43.36 % (2428003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.36 % (2428003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.36 % (2428003)CaDiCaL version: 2.1.3
% 144.66/43.36 % (2428003)Termination reason: Instruction limit
% 144.66/43.36 % (2428003)Termination phase: Finite model building preprocessing
% 144.66/43.36 % (2428003)Time elapsed: 29.947 s
% 144.66/43.36 % (2428003)Peak memory usage: 201 MB
% 144.66/43.36 % (2428003)Instructions burned: 54284 (million)
% 144.66/43.36 % (2428027)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4010355027:i=8173:av=off_2642 on theBenchmark for (2642ds/8173Mi)
% 144.66/43.36 % (2428027)Instruction limit reached!
% 144.66/43.36 % (2428027)------------------------------
% 144.66/43.36 % (2428027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.36 % (2428027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.36 % (2428027)CaDiCaL version: 2.1.3
% 144.66/43.36 % (2428027)Termination reason: Instruction limit
% 144.66/43.36 % (2428027)Termination phase: Saturation
% 144.66/43.36 % (2428027)Time elapsed: 4.354 s
% 144.66/43.36 % (2428027)Peak memory usage: 85 MB
% 144.66/43.36 % (2428027)Instructions burned: 8173 (million)
% 144.66/43.36 % (2428029)dis+10_16:1_sil=16000:random_seed=986711405:i=9155:fsr=off_2598 on theBenchmark for (2598ds/9155Mi)
% 144.66/43.36 % (2427951) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2427945-2427951"...
% 144.66/43.36 % (2427951)...printing done.
% 144.66/43.36 % (2427951)Refutation found. Thanks to Tanya!
% 144.66/43.36 % SZS status Theorem for theBenchmark
% 144.66/43.36 % SZS output start Proof for theBenchmark
% See solution above
% 144.66/43.37 % (2427951)------------------------------
% 144.66/43.37 % (2427951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.66/43.37 % (2427951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.66/43.37 % (2427951)CaDiCaL version: 2.1.3
% 144.66/43.37 % (2427951)Termination reason: Refutation
% 144.66/43.37 % (2427951)Time elapsed: 41.952 s
% 144.66/43.37 % (2427951)Peak memory usage: 431 MB
% 144.66/43.37 % (2427951)Instructions burned: 134210 (million)
% 144.66/43.37 % (2427945)Success in time 42.93 s
% 144.66/43.37 % Vampire exiting
%------------------------------------------------------------------------------