%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM926+8 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:17:37 PM UTC 2026
% Result : Theorem 21.78s 4.66s
% Output : Refutation 22.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 13
% Syntax : Number of formulae : 59 ( 41 unt; 0 def)
% Number of atoms : 92 ( 61 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 57 ( 24 ~; 25 |; 5 &)
% ( 1 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 13 con; 0-4 aty)
% Number of variables : 54 ( 42 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f272,axiom,
ti(int,t) = t,
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',fact_22_zless__le) ).
fof(f362,axiom,
! [X0] : hAPP(int,int,number_number_of(int),X0) = ti(int,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_number__of__is__id) ).
fof(f400,axiom,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),pls),X0) = ti(int,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_add__Pls) ).
fof(f434,axiom,
one_one(int) = hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_161_one__is__num__one) ).
fof(f1863,axiom,
hAPP(int,int,succ,pls) = hAPP(int,int,bit1,pls),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1590_succ__Pls) ).
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/sandbox/benchmark/theBenchmark.p',fact_1593_succ__def) ).
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/sandbox/benchmark/theBenchmark.p',fact_4785_some__eq__trivial) ).
fof(f5720,axiom,
! [X0,X1] : hAPP(X0,X0,combi(X0),X1) = ti(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBI_1_1_U) ).
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/sandbox/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(f5879,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(f5880,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(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(f10598,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),sK11),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),sK12),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))))
| t != one_one(int) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12]),skolemize(X0,sK11),skolemize(X1,sK12)],[f5879]) ).
fof(f10599,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),sK13),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),sK14),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14]),skolemize(X0,sK13),skolemize(X1,sK14)],[f5880]) ).
fof(f10601,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))
| ti(int,X0) = ti(int,X1) )
& ( ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),X1))
& ti(int,X0) != ti(int,X1) )
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X0),X1)) ) ),
inference(nnf_transformation,[],[f295]) ).
fof(f10602,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))
| ti(int,X0) = ti(int,X1) )
& ( ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),X1))
& ti(int,X0) != ti(int,X1) )
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X0),X1)) ) ),
inference(flattening,[],[f10601]) ).
fof(f12749,plain,
t = ti(int,t),
inference(cnf_transformation,[],[f272]) ).
fof(f12750,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)),
inference(cnf_transformation,[],[f273]) ).
fof(f12751,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),sK11),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),sK12),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))))
| t != one_one(int) ),
inference(cnf_transformation,[],[f10598]) ).
fof(f12752,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),sK13),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),sK14),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(cnf_transformation,[],[f10599]) ).
fof(f12774,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))
| ti(int,X0) = ti(int,X1) ),
inference(cnf_transformation,[],[f10602]) ).
fof(f12869,plain,
! [X0] : ti(int,X0) = hAPP(int,int,number_number_of(int),X0),
inference(cnf_transformation,[],[f362]) ).
fof(f12929,plain,
! [X0] : ti(int,X0) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),pls),X0),
inference(cnf_transformation,[],[f400]) ).
fof(f12963,plain,
one_one(int) = hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,pls)),
inference(cnf_transformation,[],[f434]) ).
fof(f15104,plain,
hAPP(int,int,bit1,pls) = hAPP(int,int,succ,pls),
inference(cnf_transformation,[],[f1863]) ).
fof(f15107,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(f19905,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(f20712,plain,
! [X0,X1] : ti(X0,X1) = hAPP(X0,X0,combi(X0),X1),
inference(cnf_transformation,[],[f5720]) ).
fof(f20730,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(f21003,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,[],[f12749,f19905]) ).
fof(f21004,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(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)) ),
inference(definition_unfolding,[],[f12774,f19905,f19905]) ).
fof(f21019,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,[],[f12869,f19905]) ).
fof(f21035,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),pls),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,[],[f12929,f19905]) ).
fof(f21919,plain,
! [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)) = hAPP(X0,X0,combi(X0),X1),
inference(definition_unfolding,[],[f20712,f19905]) ).
fof(f23745,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),pls),X0) = hAPP(int,int,combi(int),X0),
inference(forward_demodulation,[],[f21035,f21919]) ).
fof(f23763,plain,
! [X0] : hAPP(int,int,number_number_of(int),X0) = hAPP(int,int,combi(int),X0),
inference(forward_demodulation,[],[f21019,f21919]) ).
fof(f23784,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(int,int,combi(int),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)) ),
inference(forward_demodulation,[],[f21004,f21919]) ).
fof(f23799,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)),
inference(forward_subsumption_resolution,[],[f12752,f20730]) ).
fof(f23800,plain,
t != one_one(int),
inference(forward_subsumption_resolution,[],[f12751,f20730]) ).
fof(f23801,plain,
t = hAPP(int,int,combi(int),t),
inference(forward_demodulation,[],[f21003,f21919]) ).
fof(f24889,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(int),X0),X1))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),X1)) ),
inference(forward_demodulation,[],[f23784,f23763]) ).
fof(f24904,plain,
t = hAPP(int,int,number_number_of(int),t),
inference(forward_demodulation,[],[f23801,f23763]) ).
fof(f25428,plain,
! [X0,X1] :
( hAPP(int,int,number_number_of(int),X1) = hAPP(int,int,combi(int),X0)
| 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)) ),
inference(forward_demodulation,[],[f24889,f21919]) ).
fof(f25767,plain,
! [X0,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))
| hAPP(int,int,number_number_of(int),X0) = hAPP(int,int,number_number_of(int),X1) ),
inference(forward_demodulation,[],[f25428,f23763]) ).
fof(f26243,plain,
hAPP(int,int,succ,pls) = hAPP(int,int,combi(int),one_one(int)),
inference(superposition,[],[f15107,f23745]) ).
fof(f26244,plain,
hAPP(int,int,succ,pls) = hAPP(int,int,number_number_of(int),one_one(int)),
inference(forward_demodulation,[],[f26243,f23763]) ).
fof(f26246,plain,
hAPP(int,int,bit1,pls) = hAPP(int,int,number_number_of(int),one_one(int)),
inference(forward_demodulation,[],[f26244,f15104]) ).
fof(f26863,plain,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))
| hAPP(int,int,number_number_of(int),t) = hAPP(int,int,number_number_of(int),one_one(int)) ),
inference(resolution,[],[f25767,f12750]) ).
fof(f26890,plain,
hAPP(int,int,number_number_of(int),t) = hAPP(int,int,number_number_of(int),one_one(int)),
inference(forward_subsumption_resolution,[],[f26863,f23799]) ).
fof(f26900,plain,
hAPP(int,int,bit1,pls) = hAPP(int,int,number_number_of(int),t),
inference(forward_demodulation,[],[f26890,f26246]) ).
fof(f26922,plain,
t = hAPP(int,int,bit1,pls),
inference(forward_demodulation,[],[f26900,f24904]) ).
fof(f26951,plain,
one_one(int) = hAPP(int,int,number_number_of(int),t),
inference(superposition,[],[f12963,f26922]) ).
fof(f27027,plain,
t = one_one(int),
inference(forward_demodulation,[],[f26951,f24904]) ).
fof(f27039,plain,
$false,
inference(forward_subsumption_resolution,[],[f27027,f23800]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM926+8 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.36 % Computer : n020.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 21:46:04 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.46/3.68 % (3785424)Detected formulas, will run a generic FOF schedule.
% 14.46/3.68 % (3785430)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1843998168:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2992 on theBenchmark for (2992ds/134677Mi)
% 14.46/3.68 % (3785429)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=687973690:i=141193_2992 on theBenchmark for (2992ds/141193Mi)
% 14.46/3.68 % (3785432)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1354806200:i=109:sd=1:ins=1:gsp=on:ss=axioms_2992 on theBenchmark for (2992ds/109Mi)
% 14.46/3.68 % (3785431)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3754415065:i=141695:sd=1:nm=32:gsp=on:ss=included_2992 on theBenchmark for (2992ds/141695Mi)
% 14.46/3.68 % (3785433)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2806223059:i=119:av=off:ss=axioms_2992 on theBenchmark for (2992ds/119Mi)
% 14.46/3.68 % (3785434)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3394696660:s2a=on:i=139:gtg=position_2992 on theBenchmark for (2992ds/139Mi)
% 14.46/3.68 % (3785435)dis-21_1_sil=8000:lcm=predicate:random_seed=1886949544:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2992 on theBenchmark for (2992ds/129Mi)
% 14.46/3.68 % (3785434)Instruction limit reached!
% 14.46/3.68 % (3785434)------------------------------
% 14.46/3.68 % (3785434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.46/3.68 % (3785434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.46/3.68 % (3785434)CaDiCaL version: 2.1.3
% 14.46/3.68 % (3785434)Termination reason: Instruction limit
% 14.46/3.68 % (3785434)Termination phase: Property scanning
% 14.46/3.68 % (3785434)Time elapsed: 0.050 s
% 14.46/3.68 % (3785434)Peak memory usage: 91 MB
% 14.46/3.68 % (3785434)Instructions burned: 140 (million)
% 14.46/3.68 % (3785432)Instruction limit reached!
% 14.46/3.68 % (3785432)------------------------------
% 14.46/3.68 % (3785432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.46/3.68 % (3785432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.46/3.68 % (3785432)CaDiCaL version: 2.1.3
% 14.46/3.68 % (3785432)Termination reason: Instruction limit
% 14.46/3.68 % (3785432)Termination phase: Blocked clause elimination
% 14.46/3.68 % (3785432)Time elapsed: 0.058 s
% 14.46/3.68 % (3785432)Peak memory usage: 92 MB
% 14.46/3.68 % (3785432)Instructions burned: 111 (million)
% 14.46/3.68 % (3785433)Instruction limit reached!
% 14.46/3.68 % (3785433)------------------------------
% 14.46/3.68 % (3785433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.46/3.68 % (3785433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.46/3.68 % (3785433)CaDiCaL version: 2.1.3
% 14.46/3.68 % (3785433)Termination reason: Instruction limit
% 14.46/3.68 % (3785433)Termination phase: Property scanning
% 14.46/3.68 % (3785433)Time elapsed: 0.069 s
% 14.46/3.68 % (3785433)Peak memory usage: 93 MB
% 14.46/3.68 % (3785433)Instructions burned: 122 (million)
% 14.46/3.68 % (3785435)Instruction limit reached!
% 14.46/3.68 % (3785435)------------------------------
% 14.46/3.68 % (3785435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.46/3.68 % (3785435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.46/3.68 % (3785435)CaDiCaL version: 2.1.3
% 14.46/3.68 % (3785435)Termination reason: Instruction limit
% 14.46/3.68 % (3785435)Termination phase: Naming
% 14.46/3.68 % (3785435)Time elapsed: 0.079 s
% 14.46/3.68 % (3785435)Peak memory usage: 93 MB
% 14.46/3.68 % (3785435)Instructions burned: 129 (million)
% 14.46/3.68 % (3785443)lrs+10_1_sil=8000:sp=occurrence:random_seed=2453826995:i=285:sd=3:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/285Mi)
% 14.46/3.68 % (3785444)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1804751981:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/157Mi)
% 14.46/3.68 % (3785445)lrs+1011_1_sil=32000:sp=occurrence:random_seed=423060514:i=325:sd=1:ss=axioms:sgt=32_2989 on theBenchmark for (2989ds/325Mi)
% 14.46/3.68 % (3785444)Instruction limit reached!
% 14.46/3.68 % (3785444)------------------------------
% 14.46/3.68 % (3785444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.46/3.68 % (3785444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.59 % (3785444)CaDiCaL version: 2.1.3
% 21.01/4.59 % (3785444)Termination reason: Instruction limit
% 21.01/4.59 % (3785444)Termination phase: Property scanning
% 21.01/4.59 % (3785444)Time elapsed: 0.058 s
% 21.01/4.59 % (3785444)Peak memory usage: 91 MB
% 21.01/4.59 % (3785444)Instructions burned: 158 (million)
% 21.01/4.59 % (3785446)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2428160790:s2a=on:i=248:s2at=1.23:gtg=position_2989 on theBenchmark for (2989ds/248Mi)
% 21.01/4.59 % (3785443)Instruction limit reached!
% 21.01/4.59 % (3785443)------------------------------
% 21.01/4.59 % (3785443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.59 % (3785443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.59 % (3785443)CaDiCaL version: 2.1.3
% 21.01/4.59 % (3785443)Termination reason: Instruction limit
% 21.01/4.59 % (3785443)Termination phase: Saturation
% 21.01/4.59 % (3785443)Time elapsed: 0.134 s
% 21.01/4.59 % (3785443)Peak memory usage: 95 MB
% 21.01/4.59 % (3785443)Instructions burned: 286 (million)
% 21.01/4.59 % (3785446)Instruction limit reached!
% 21.01/4.59 % (3785446)------------------------------
% 21.01/4.59 % (3785446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.59 % (3785446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.59 % (3785446)CaDiCaL version: 2.1.3
% 21.01/4.59 % (3785446)Termination reason: Instruction limit
% 21.01/4.59 % (3785446)Termination phase: Property scanning
% 21.01/4.59 % (3785446)Time elapsed: 0.089 s
% 21.01/4.59 % (3785446)Peak memory usage: 91 MB
% 21.01/4.59 % (3785446)Instructions burned: 249 (million)
% 21.01/4.59 % (3785445)Instruction limit reached!
% 21.01/4.59 % (3785445)------------------------------
% 21.01/4.59 % (3785445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.59 % (3785445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.59 % (3785445)CaDiCaL version: 2.1.3
% 21.01/4.59 % (3785445)Termination reason: Instruction limit
% 21.01/4.59 % (3785445)Termination phase: Saturation
% 21.01/4.59 % (3785445)Time elapsed: 0.187 s
% 21.01/4.59 % (3785445)Peak memory usage: 96 MB
% 21.01/4.59 % (3785445)Instructions burned: 326 (million)
% 21.01/4.59 % (3785451)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=893199263:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2987 on theBenchmark for (2987ds/294Mi)
% 21.01/4.59 % (3785452)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=130024986:i=2350_2987 on theBenchmark for (2987ds/2350Mi)
% 21.01/4.59 % (3785453)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1670805859:cts=off:i=113:fsr=off:ss=included:sgt=4_2986 on theBenchmark for (2986ds/113Mi)
% 21.01/4.59 % (3785451)Instruction limit reached!
% 21.01/4.59 % (3785451)------------------------------
% 21.01/4.59 % (3785451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.59 % (3785451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.59 % (3785451)CaDiCaL version: 2.1.3
% 21.01/4.59 % (3785451)Termination reason: Instruction limit
% 21.01/4.59 % (3785451)Termination phase: Property scanning
% 21.01/4.59 % (3785451)Time elapsed: 0.141 s
% 21.01/4.59 % (3785451)Peak memory usage: 94 MB
% 21.01/4.59 % (3785451)Instructions burned: 294 (million)
% 21.01/4.59 % (3785455)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1357986289:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 21.01/4.59 % (3785453)Instruction limit reached!
% 21.01/4.59 % (3785453)------------------------------
% 21.01/4.59 % (3785453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.59 % (3785453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.59 % (3785453)CaDiCaL version: 2.1.3
% 21.01/4.59 % (3785453)Termination reason: Instruction limit
% 21.01/4.59 % (3785453)Termination phase: Unused predicate definition removal
% 21.01/4.59 % (3785453)Time elapsed: 0.068 s
% 21.01/4.59 % (3785453)Peak memory usage: 91 MB
% 21.01/4.59 % (3785453)Instructions burned: 114 (million)
% 21.01/4.59 % (3785455)Instruction limit reached!
% 21.01/4.59 % (3785455)------------------------------
% 21.01/4.59 % (3785455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.01/4.59 % (3785455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.01/4.59 % (3785455)CaDiCaL version: 2.1.3
% 21.78/4.66 % (3785455)Termination reason: Instruction limit
% 21.78/4.66 % (3785455)Termination phase: Preprocessing 3
% 21.78/4.66 % (3785455)Time elapsed: 0.072 s
% 21.78/4.66 % (3785455)Peak memory usage: 95 MB
% 21.78/4.66 % (3785455)Instructions burned: 128 (million)
% 21.78/4.66 % (3785458)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=955111074:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi)
% 21.78/4.66 % (3785460)lrs+10_1_sil=8000:sp=occurrence:random_seed=4151168210:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 21.78/4.66 % (3785461)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=243961162:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 21.78/4.66 % (3785458)Instruction limit reached!
% 21.78/4.66 % (3785458)------------------------------
% 21.78/4.66 % (3785458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.78/4.66 % (3785458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.78/4.66 % (3785458)CaDiCaL version: 2.1.3
% 21.78/4.66 % (3785458)Termination reason: Instruction limit
% 21.78/4.66 % (3785458)Termination phase: Property scanning
% 21.78/4.66 % (3785458)Time elapsed: 0.069 s
% 21.78/4.66 % (3785458)Peak memory usage: 91 MB
% 21.78/4.66 % (3785458)Instructions burned: 117 (million)
% 21.78/4.66 % (3785465)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4220555103:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 21.78/4.66 % (3785461)Instruction limit reached!
% 21.78/4.66 % (3785461)------------------------------
% 21.78/4.66 % (3785461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.78/4.66 % (3785461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.78/4.66 % (3785461)CaDiCaL version: 2.1.3
% 21.78/4.66 % (3785461)Termination reason: Instruction limit
% 21.78/4.66 % (3785461)Termination phase: Property scanning
% 21.78/4.66 % (3785461)Time elapsed: 0.210 s
% 21.78/4.66 % (3785461)Peak memory usage: 97 MB
% 21.78/4.66 % (3785461)Instructions burned: 437 (million)
% 21.78/4.66 % (3785467)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3145041905:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 21.78/4.66 % (3785460)Instruction limit reached!
% 21.78/4.66 % (3785460)------------------------------
% 21.78/4.66 % (3785460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.78/4.66 % (3785460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.78/4.66 % (3785460)CaDiCaL version: 2.1.3
% 21.78/4.66 % (3785460)Termination reason: Instruction limit
% 21.78/4.66 % (3785460)Termination phase: Saturation
% 21.78/4.66 % (3785460)Time elapsed: 0.507 s
% 21.78/4.66 % (3785460)Peak memory usage: 101 MB
% 21.78/4.66 % (3785460)Instructions burned: 908 (million)
% 21.78/4.66 % (3785467)Instruction limit reached!
% 21.78/4.66 % (3785467)------------------------------
% 21.78/4.66 % (3785467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.78/4.66 % (3785467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.78/4.66 % (3785467)CaDiCaL version: 2.1.3
% 21.78/4.66 % (3785467)Termination reason: Instruction limit
% 21.78/4.66 % (3785467)Termination phase: NewCNF
% 21.78/4.66 % (3785467)Time elapsed: 0.087 s
% 21.78/4.66 % (3785467)Peak memory usage: 94 MB
% 21.78/4.66 % (3785467)Instructions burned: 135 (million)
% 21.78/4.66 % (3785469)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2740035925:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi)
% 21.78/4.66 % (3785470)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3935734460:st=3:i=13193:sd=3:ss=axioms_2977 on theBenchmark for (2977ds/13193Mi)
% 21.78/4.66 % (3785469)Instruction limit reached!
% 21.78/4.66 % (3785469)------------------------------
% 21.78/4.66 % (3785469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.78/4.66 % (3785469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.78/4.66 % (3785469)CaDiCaL version: 2.1.3
% 21.78/4.66 % (3785469)Termination reason: Instruction limit
% 21.78/4.66 % (3785469)Termination phase: Property scanning
% 21.78/4.66 % (3785469)Time elapsed: 0.282 s
% 21.78/4.66 % (3785469)Peak memory usage: 97 MB
% 21.78/4.66 % (3785469)Instructions burned: 595 (million)
% 21.78/4.66 % (3785452)Instruction limit reached!
% 21.78/4.66 % (3785452)------------------------------
% 21.78/4.66 % (3785452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.78/4.66 % (3785452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.78/4.66 % (3785452)CaDiCaL version: 2.1.3
% 21.78/4.66 % (3785452)Termination reason: Instruction limit
% 21.78/4.66 % (3785452)Termination phase: Saturation
% 21.78/4.66 % (3785452)Time elapsed: 1.392 s
% 21.78/4.66 % (3785452)Peak memory usage: 215 MB
% 21.78/4.66 % (3785452)Instructions burned: 2350 (million)
% 21.78/4.66 % (3785473)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3629830554:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/125Mi)
% 21.78/4.66 % (3785473)Instruction limit reached!
% 21.78/4.66 % (3785473)------------------------------
% 21.78/4.66 % (3785473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.78/4.66 % (3785473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.78/4.66 % (3785473)CaDiCaL version: 2.1.3
% 21.78/4.66 % (3785473)Termination reason: Instruction limit
% 21.78/4.66 % (3785473)Termination phase: Property scanning
% 21.78/4.66 % (3785473)Time elapsed: 0.046 s
% 21.78/4.66 % (3785473)Peak memory usage: 91 MB
% 21.78/4.66 % (3785473)Instructions burned: 126 (million)
% 21.78/4.66 % (3785475)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=99074274:i=134:gtgl=5:slsql=off:gtg=exists_sym_2971 on theBenchmark for (2971ds/134Mi)
% 21.78/4.66 % (3785476)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3063103201:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/141Mi)
% 21.78/4.66 % (3785475)Instruction limit reached!
% 21.78/4.66 % (3785475)------------------------------
% 21.78/4.66 % (3785475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.78/4.66 % (3785475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.78/4.66 % (3785475)CaDiCaL version: 2.1.3
% 21.78/4.66 % (3785475)Termination reason: Instruction limit
% 21.78/4.66 % (3785475)Termination phase: Property scanning
% 21.78/4.66 % (3785475)Time elapsed: 0.050 s
% 21.78/4.66 % (3785475)Peak memory usage: 91 MB
% 21.78/4.66 % (3785475)Instructions burned: 136 (million)
% 21.78/4.66 % (3785476)Refutation not found, incomplete strategy
% 21.78/4.66 % (3785476)------------------------------
% 21.78/4.66 % (3785476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.78/4.66 % (3785476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.78/4.66 % (3785476)CaDiCaL version: 2.1.3
% 21.78/4.66 % (3785476)Termination reason: Refutation not found, incomplete strategy
% 21.78/4.66 % (3785476)Time elapsed: 0.062 s
% 21.78/4.66 % (3785476)Peak memory usage: 95 MB
% 21.78/4.66 % (3785476)Instructions burned: 112 (million)
% 21.78/4.66 % (3785479)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4181392791:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2969 on theBenchmark for (2969ds/431Mi)
% 21.78/4.66 % (3785476)------------------------------
% 21.78/4.66 % (3785476)------------------------------
% 21.78/4.66 % (3785479)Instruction limit reached!
% 21.78/4.66 % (3785479)------------------------------
% 21.78/4.66 % (3785479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.78/4.66 % (3785479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.78/4.66 % (3785479)CaDiCaL version: 2.1.3
% 21.78/4.66 % (3785479)Termination reason: Instruction limit
% 21.78/4.66 % (3785479)Termination phase: Saturation
% 21.78/4.66 % (3785479)Time elapsed: 0.219 s
% 21.78/4.66 % (3785479)Peak memory usage: 96 MB
% 21.78/4.66 % (3785479)Instructions burned: 431 (million)
% 21.78/4.66 % (3785481)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2042804115:i=6060:aac=none:ins=25_2966 on theBenchmark for (2966ds/6060Mi)
% 21.78/4.66 % (3785430)First to succeed.
% 21.78/4.66 % (3785430)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3785424"
% 21.78/4.66 % (3785482)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=819120514:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2965 on theBenchmark for (2965ds/150Mi)
% 21.78/4.66 % (3785482)Instruction limit reached!
% 21.78/4.66 % (3785482)------------------------------
% 21.78/4.66 % (3785482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.78/4.66 % (3785482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.78/4.66 % (3785482)CaDiCaL version: 2.1.3
% 21.78/4.66 % (3785482)Termination reason: Instruction limit
% 21.78/4.66 % (3785482)Termination phase: Preprocessing 3
% 21.78/4.66 % (3785482)Time elapsed: 0.089 s
% 21.78/4.66 % (3785482)Peak memory usage: 94 MB
% 21.78/4.66 % (3785482)Instructions burned: 151 (million)
% 21.78/4.66 % (3785430)Refutation found. Thanks to Tanya!
% 21.78/4.66 % SZS status Theorem for theBenchmark
% 21.78/4.66 % SZS output start Proof for theBenchmark
% See solution above
% 22.65/4.87 % (3785430)------------------------------
% 22.65/4.87 % (3785430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.65/4.87 % (3785430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.65/4.87 % (3785430)CaDiCaL version: 2.1.3
% 22.65/4.87 % (3785430)Termination reason: Refutation
% 22.65/4.87 % (3785430)Time elapsed: 2.684 s
% 22.65/4.87 % (3785430)Peak memory usage: 288 MB
% 22.65/4.87 % (3785430)Instructions burned: 8864 (million)
% 22.65/4.87 % (3785430)------------------------------
% 22.65/4.87 % (3785430)------------------------------
% 22.65/4.87 % (3785424)Success in time 3.809 s
% 22.65/4.87 % Vampire exiting
%------------------------------------------------------------------------------