%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM926_3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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:12 PM UTC 2026
% Result : Theorem 82.32s 28.11s
% Output : Refutation 82.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 8
% Syntax : Number of formulae : 32 ( 17 unt; 0 typ; 0 def)
% Number of atoms : 51 ( 32 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 39 ( 20 ~; 15 |; 0 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of types : 20 ( 19 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 115 ( 115 usr; 32 con; 0-3 aty)
% Number of variables : 30 ( 18 !; 12 ?; 30 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
bool: $tType ).
tff(type_def_6,type,
int: $tType ).
tff(type_def_7,type,
nat: $tType ).
tff(type_def_8,type,
real: $tType ).
tff(type_def_9,type,
fun_bool_bool: $tType ).
tff(type_def_10,type,
fun_bo1549164019l_bool: $tType ).
tff(type_def_11,type,
fun_int_bool: $tType ).
tff(type_def_12,type,
fun_int_int: $tType ).
tff(type_def_13,type,
fun_in531499254l_bool: $tType ).
tff(type_def_14,type,
fun_int_fun_int_bool: $tType ).
tff(type_def_15,type,
fun_nat_bool: $tType ).
tff(type_def_16,type,
fun_nat_int: $tType ).
tff(type_def_17,type,
fun_nat_nat: $tType ).
tff(type_def_18,type,
fun_nat_real: $tType ).
tff(type_def_19,type,
fun_nat_fun_nat_bool: $tType ).
tff(type_def_20,type,
fun_real_bool: $tType ).
tff(type_def_21,type,
fun_real_real: $tType ).
tff(type_def_22,type,
fun_re413263731l_bool: $tType ).
tff(type_def_23,type,
product_prod_int_int: $tType ).
tff(func_def_0,type,
cOMBB_1652995168ol_int: ( fun_bo1549164019l_bool * fun_int_bool ) > fun_in531499254l_bool ).
tff(func_def_1,type,
cOMBC_int_int_bool: ( fun_int_fun_int_bool * int ) > fun_int_bool ).
tff(func_def_2,type,
cOMBS_int_bool_bool: ( fun_in531499254l_bool * fun_int_bool ) > fun_int_bool ).
tff(func_def_3,type,
div_mod_int: int > fun_int_int ).
tff(func_def_4,type,
div_mod_nat: nat > fun_nat_nat ).
tff(func_def_5,type,
minus_minus_int: int > fun_int_int ).
tff(func_def_6,type,
minus_minus_nat: nat > fun_nat_nat ).
tff(func_def_7,type,
minus_minus_real: real > fun_real_real ).
tff(func_def_8,type,
one_one_int: int ).
tff(func_def_9,type,
one_one_nat: nat ).
tff(func_def_10,type,
one_one_real: real ).
tff(func_def_11,type,
plus_plus_int: int > fun_int_int ).
tff(func_def_12,type,
plus_plus_nat: nat > fun_nat_nat ).
tff(func_def_13,type,
plus_plus_real: real > fun_real_real ).
tff(func_def_14,type,
times_times_int: int > fun_int_int ).
tff(func_def_15,type,
times_times_nat: nat > fun_nat_nat ).
tff(func_def_16,type,
times_times_real: real > fun_real_real ).
tff(func_def_17,type,
zero_zero_int: int ).
tff(func_def_18,type,
zero_zero_nat: nat ).
tff(func_def_19,type,
zero_zero_real: real ).
tff(func_def_20,type,
multInv: ( int * int ) > int ).
tff(func_def_21,type,
d22set: int > fun_int_bool ).
tff(func_def_22,type,
zfact: int > int ).
tff(func_def_23,type,
zcong: ( int * int ) > fun_int_bool ).
tff(func_def_24,type,
zprime: fun_int_bool ).
tff(func_def_25,type,
bit0: int > int ).
tff(func_def_26,type,
bit1: int > int ).
tff(func_def_27,type,
min: int ).
tff(func_def_28,type,
pls: int ).
tff(func_def_29,type,
number_number_of_int: int > int ).
tff(func_def_30,type,
number_number_of_nat: int > nat ).
tff(func_def_31,type,
number267125858f_real: int > real ).
tff(func_def_32,type,
ord_less_int: fun_int_fun_int_bool ).
tff(func_def_33,type,
ord_less_nat: fun_nat_fun_nat_bool ).
tff(func_def_34,type,
ord_less_real: fun_re413263731l_bool ).
tff(func_def_35,type,
ord_less_eq_int: fun_int_fun_int_bool ).
tff(func_def_36,type,
ord_less_eq_nat: fun_nat_fun_nat_bool ).
tff(func_def_37,type,
ord_less_eq_real: fun_re413263731l_bool ).
tff(func_def_38,type,
power_power_int: int > fun_nat_int ).
tff(func_def_39,type,
power_power_nat: nat > fun_nat_nat ).
tff(func_def_40,type,
power_power_real: real > fun_nat_real ).
tff(func_def_41,type,
product_Pair_int_int: ( int * int ) > product_prod_int_int ).
tff(func_def_42,type,
legendre: ( int * int ) > int ).
tff(func_def_43,type,
quadRes: int > fun_int_bool ).
tff(func_def_44,type,
sr: int > fun_int_bool ).
tff(func_def_45,type,
standardRes: ( int * int ) > int ).
tff(func_def_46,type,
dvd_dvd_int: fun_int_fun_int_bool ).
tff(func_def_47,type,
dvd_dvd_nat: fun_nat_fun_nat_bool ).
tff(func_def_48,type,
dvd_dvd_real: fun_re413263731l_bool ).
tff(func_def_49,type,
collect_int: fun_int_bool > fun_int_bool ).
tff(func_def_50,type,
twoSqu820444569sum2sq: fun_int_bool ).
tff(func_def_51,type,
twoSqu949963151sum2sq: product_prod_int_int > int ).
tff(func_def_52,type,
inv: ( int * int ) > int ).
tff(func_def_53,type,
wset: ( int * int ) > fun_int_bool ).
tff(func_def_54,type,
fconj: fun_bo1549164019l_bool ).
tff(func_def_55,type,
hAPP_bool_bool: ( fun_bool_bool * bool ) > bool ).
tff(func_def_56,type,
hAPP_b589554111l_bool: ( fun_bo1549164019l_bool * bool ) > fun_bool_bool ).
tff(func_def_57,type,
hAPP_int_bool: ( fun_int_bool * int ) > bool ).
tff(func_def_58,type,
hAPP_int_int: ( fun_int_int * int ) > int ).
tff(func_def_59,type,
hAPP_i68813070l_bool: ( fun_in531499254l_bool * int ) > fun_bool_bool ).
tff(func_def_60,type,
hAPP_i1948725293t_bool: ( fun_int_fun_int_bool * int ) > fun_int_bool ).
tff(func_def_61,type,
hAPP_nat_bool: ( fun_nat_bool * nat ) > bool ).
tff(func_def_62,type,
hAPP_nat_int: ( fun_nat_int * nat ) > int ).
tff(func_def_63,type,
hAPP_nat_nat: ( fun_nat_nat * nat ) > nat ).
tff(func_def_64,type,
hAPP_nat_real: ( fun_nat_real * nat ) > real ).
tff(func_def_65,type,
hAPP_n1699378549t_bool: ( fun_nat_fun_nat_bool * nat ) > fun_nat_bool ).
tff(func_def_66,type,
hAPP_real_bool: ( fun_real_bool * real ) > bool ).
tff(func_def_67,type,
hAPP_real_real: ( fun_real_real * real ) > real ).
tff(func_def_68,type,
hAPP_r1134773055l_bool: ( fun_re413263731l_bool * real ) > fun_real_bool ).
tff(func_def_69,type,
member_int: ( int * fun_int_bool ) > bool ).
tff(func_def_70,type,
m: int ).
tff(func_def_71,type,
s1: int ).
tff(func_def_72,type,
s: int ).
tff(func_def_73,type,
t: int ).
tff(func_def_74,type,
sK5: int ).
tff(func_def_75,type,
sK6: int ).
tff(func_def_76,type,
sK7: int ).
tff(func_def_77,type,
sK8: int ).
tff(func_def_78,type,
sK9: int ).
tff(func_def_79,type,
sK10: int ).
tff(func_def_80,type,
sK11: int ).
tff(func_def_81,type,
sK12: int > int ).
tff(func_def_82,type,
sK13: int ).
tff(func_def_83,type,
sK14: ( int * int * int ) > int ).
tff(func_def_84,type,
sK15: ( int * int ) > int ).
tff(func_def_85,type,
sK16: ( real * nat ) > real ).
tff(func_def_86,type,
sK17: ( real * nat ) > real ).
tff(func_def_87,type,
sK18: ( nat * nat ) > nat ).
tff(func_def_88,type,
sK19: ( fun_nat_bool * nat * nat ) > nat ).
tff(func_def_89,type,
sK20: ( fun_nat_bool * nat * nat ) > nat ).
tff(func_def_90,type,
sK21: ( nat * fun_nat_bool ) > nat ).
tff(func_def_91,type,
sK22: int > int ).
tff(func_def_92,type,
sK23: int > int ).
tff(func_def_93,type,
sK24: ( fun_int_bool * int ) > int ).
tff(func_def_94,type,
sK25: ( fun_int_bool * int ) > int ).
tff(func_def_95,type,
sK26: int > int ).
tff(func_def_96,type,
sK27: ( int * int ) > int ).
tff(func_def_97,type,
sK28: ( fun_int_bool * int ) > int ).
tff(func_def_98,type,
sK29: ( fun_int_bool * int ) > int ).
tff(func_def_99,type,
sK30: fun_int_bool > int ).
tff(func_def_100,type,
sK31: ( fun_int_bool * int ) > int ).
tff(func_def_101,type,
sK32: ( fun_int_bool * int ) > int ).
tff(func_def_102,type,
sK33: fun_nat_nat > nat ).
tff(func_def_103,type,
sK34: fun_nat_nat > nat ).
tff(func_def_104,type,
sK35: ( nat * fun_nat_bool ) > nat ).
tff(func_def_105,type,
sK36: ( nat * nat ) > nat ).
tff(func_def_106,type,
sK37: ( int * int ) > int ).
tff(func_def_107,type,
sK38: ( fun_int_bool * int * int ) > int ).
tff(func_def_108,type,
sK39: ( fun_int_bool * int * int ) > int ).
tff(func_def_109,type,
sK40: ( fun_int_bool * int * int ) > int ).
tff(func_def_110,type,
sK41: ( fun_int_bool * int * int ) > int ).
tff(func_def_111,type,
sK42: ( int * int ) > int ).
tff(func_def_112,type,
sK43: ( nat * nat ) > nat ).
tff(func_def_113,type,
sK44: ( nat * fun_nat_bool * nat ) > nat ).
tff(func_def_114,type,
sK45: ( nat * fun_nat_bool * nat ) > nat ).
tff(pred_def_1,type,
hBOOL: bool > $o ).
tff(pred_def_2,type,
sP0: ( bool * int * bool ) > $o ).
tff(pred_def_3,type,
sP1: ( int * bool * bool ) > $o ).
tff(pred_def_4,type,
sP2: ( fun_int_bool * int * int ) > $o ).
tff(pred_def_5,type,
sP3: ( fun_int_bool * int * int ) > $o ).
tff(pred_def_6,type,
sP4: ( nat * fun_nat_bool * nat ) > $o ).
tff(f1,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_tpos) ).
tff(f2,axiom,
( ( t = one_one_int )
=> ? [X0: int,X1: int] : ( hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(pls))))) = hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(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) ).
tff(f3,axiom,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t))
=> ? [X0: int,X1: int] : ( hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(pls))))) = hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(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) ).
tff(f207,axiom,
! [X0: int] : ( bit0(X0) = hAPP_int_int(plus_plus_int(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_Bit0__def) ).
tff(f254,axiom,
! [X0: int] : ( bit1(X0) = hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),X0)),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_253_Bit1__def) ).
tff(f359,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_358_Pls__def) ).
tff(f571,axiom,
! [X0: int,X1: int] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
=> ( ( X0 != X1 )
=> hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_570_order__le__neq__implies__less) ).
tff(f1205,conjecture,
? [X0: int,X1: int] : ( hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(pls))))) = hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
tff(f1206,negated_conjecture,
~ ? [X0: int,X1: int] : ( hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(pls))))) = hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int) ),
inference(negated_conjecture,[status(cth)],[f1205]) ).
tff(f1210,plain,
( ? [X0: int,X1: int] : ( hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(pls))))) = hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int) )
| ( one_one_int != t ) ),
inference(ennf_transformation,[],[f2]) ).
tff(f1211,plain,
( ? [X0: int,X1: int] : ( hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(pls))))) = hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int) )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)) ),
inference(ennf_transformation,[],[f3]) ).
tff(f1439,plain,
! [X0: int,X1: int] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| ( X0 = X1 )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1)) ),
inference(ennf_transformation,[],[f571]) ).
tff(f1440,plain,
! [X0: int,X1: int] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| ( X0 = X1 )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1)) ),
inference(flattening,[],[f1439]) ).
tff(f2083,plain,
! [X0: int,X1: int] : ( hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(pls))))) != hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int) ),
inference(ennf_transformation,[],[f1206]) ).
tff(f2093,plain,
( ( hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(sK5),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(sK6),number_number_of_nat(bit0(bit1(pls))))) )
| ( one_one_int != t ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6]),skolemize(X0,sK5),skolemize(X1,sK6)],[f1210]) ).
tff(f2094,plain,
( ( hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(sK7),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(sK8),number_number_of_nat(bit0(bit1(pls))))) )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8]),skolemize(X0,sK7),skolemize(X1,sK8)],[f1211]) ).
tff(f2486,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t)),
inference(cnf_transformation,[],[f1]) ).
tff(f2487,plain,
( ( hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(sK5),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(sK6),number_number_of_nat(bit0(bit1(pls))))) )
| ( one_one_int != t ) ),
inference(cnf_transformation,[],[f2093]) ).
tff(f2488,plain,
( ( hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(sK7),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(sK8),number_number_of_nat(bit0(bit1(pls))))) )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)) ),
inference(cnf_transformation,[],[f2094]) ).
tff(f2763,plain,
! [X0: int] : ( bit0(X0) = hAPP_int_int(plus_plus_int(X0),X0) ),
inference(cnf_transformation,[],[f207]) ).
tff(f2810,plain,
! [X0: int] : ( bit1(X0) = hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),X0)),X0) ),
inference(cnf_transformation,[],[f254]) ).
tff(f2939,plain,
pls = zero_zero_int,
inference(cnf_transformation,[],[f359]) ).
tff(f3244,plain,
! [X0: int,X1: int] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| ( X0 = X1 )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1)) ),
inference(cnf_transformation,[],[f1440]) ).
tff(f4174,plain,
! [X0: int,X1: int] : ( hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(pls))))) != hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int) ),
inference(cnf_transformation,[],[f2083]) ).
tff(f4175,plain,
( ( hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int))))),m)),one_one_int) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(sK5),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int))))),hAPP_nat_int(power_power_int(sK6),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int))))) )
| ( one_one_int != t ) ),
inference(definition_unfolding,[],[f2487,f2763,f2763,f2810,f2939,f2763,f2810,f2939,f2763,f2810,f2939]) ).
tff(f4176,plain,
( ( hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int))))),m)),one_one_int) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(sK7),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int))))),hAPP_nat_int(power_power_int(sK8),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int))))) )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)) ),
inference(definition_unfolding,[],[f2488,f2763,f2763,f2810,f2939,f2763,f2810,f2939,f2763,f2810,f2939]) ).
tff(f4572,plain,
! [X0: int,X1: int] : ( hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int))))),m)),one_one_int) != hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),zero_zero_int)),zero_zero_int))))) ),
inference(definition_unfolding,[],[f4174,f2763,f2810,f2939,f2763,f2810,f2939,f2763,f2763,f2810,f2939]) ).
tff(f5046,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)),
inference(forward_subsumption_resolution,[],[f4176,f4572]) ).
tff(f5047,plain,
one_one_int != t,
inference(forward_subsumption_resolution,[],[f4175,f4572]) ).
tff(f30325,plain,
( ( one_one_int = t )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t)) ),
inference(resolution,[],[f3244,f5046]) ).
tff(f30348,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t)),
inference(forward_subsumption_resolution,[],[f30325,f5047]) ).
tff(f30349,plain,
$false,
inference(forward_subsumption_resolution,[],[f30348,f2486]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM926_3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.37 % Computer : n007.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 21:42:26 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.41 Running first-order model finding
% 0.09/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.83/3.44 % (1805503)Will run a generic schedule for satisfiability detection.
% 20.83/3.44 % (1805511)dis+10_1_sil=32000:sp=arity:random_seed=3324050929:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 20.83/3.44 % (1805509)% WARNING: option uhcvi not known.
% 20.83/3.44 % (1805508)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4185458100_2999 on theBenchmark for (2999ds/0Mi)
% 20.83/3.44 % (1805509)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=555833028:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 20.83/3.44 % (1805512)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2973355659:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 20.83/3.44 % (1805510)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3632740823:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 20.83/3.44 % (1805513)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2332215431:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 20.83/3.44 % (1805514)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=623934003:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 20.83/3.44 % (1805511)Instruction limit reached!
% 20.83/3.44 % (1805511)------------------------------
% 20.83/3.44 % (1805511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.83/3.44 % (1805511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.83/3.44 % (1805511)CaDiCaL version: 2.1.3
% 20.83/3.44 % (1805511)Termination reason: Instruction limit
% 20.83/3.44 % (1805511)Termination phase: Saturation
% 20.83/3.44 % (1805511)Time elapsed: 0.027 s
% 20.83/3.44 % (1805511)Peak memory usage: 13 MB
% 20.83/3.44 % (1805511)Instructions burned: 107 (million)
% 20.83/3.44 % (1805522)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=723484623:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 20.83/3.44 % (1805512)Instruction limit reached!
% 20.83/3.44 % (1805512)------------------------------
% 20.83/3.44 % (1805512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.83/3.44 % (1805512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.83/3.44 % (1805512)CaDiCaL version: 2.1.3
% 20.83/3.44 % (1805512)Termination reason: Instruction limit
% 20.83/3.44 % (1805512)Termination phase: Blocked clause elimination
% 20.83/3.44 % (1805512)Time elapsed: 0.054 s
% 20.83/3.44 % (1805512)Peak memory usage: 13 MB
% 20.83/3.44 % (1805512)Instructions burned: 118 (million)
% 20.83/3.44 % (1805513)Instruction limit reached!
% 20.83/3.44 % (1805513)------------------------------
% 20.83/3.44 % (1805513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.83/3.44 % (1805513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.83/3.44 % (1805513)CaDiCaL version: 2.1.3
% 20.83/3.44 % (1805513)Termination reason: Instruction limit
% 20.83/3.44 % (1805513)Termination phase: Saturation
% 20.83/3.44 % (1805513)Time elapsed: 0.066 s
% 20.83/3.44 % (1805513)Peak memory usage: 14 MB
% 20.83/3.44 % (1805513)Instructions burned: 132 (million)
% 20.83/3.44 % (1805524)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2277581363:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 20.83/3.44 % (1805514)Instruction limit reached!
% 20.83/3.44 % (1805514)------------------------------
% 20.83/3.44 % (1805514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.83/3.44 % (1805514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.83/3.44 % (1805514)CaDiCaL version: 2.1.3
% 20.83/3.44 % (1805514)Termination reason: Instruction limit
% 20.83/3.44 % (1805514)Termination phase: Saturation
% 20.83/3.44 % (1805514)Time elapsed: 0.081 s
% 20.83/3.44 % (1805514)Peak memory usage: 15 MB
% 20.83/3.44 % (1805514)Instructions burned: 160 (million)
% 20.83/3.44 % (1805525)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=1932226245:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 20.83/3.44 % (1805527)ott-21_1_sil=16000:fs=off:random_seed=1121506821:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 20.83/3.44 % (1805524)Instruction limit reached!
% 20.83/3.44 % (1805524)------------------------------
% 20.83/3.44 % (1805524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.83/3.44 % (1805524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.82/6.56 % (1805524)CaDiCaL version: 2.1.3
% 42.82/6.56 % (1805524)Termination reason: Instruction limit
% 42.82/6.56 % (1805524)Termination phase: Blocked clause elimination
% 42.82/6.56 % (1805524)Time elapsed: 0.058 s
% 42.82/6.56 % (1805524)Peak memory usage: 13 MB
% 42.82/6.56 % (1805524)Instructions burned: 132 (million)
% 42.82/6.56 % (1805530)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1182262941:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 42.82/6.56 % (1805527)Instruction limit reached!
% 42.82/6.56 % (1805527)------------------------------
% 42.82/6.56 % (1805527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.82/6.56 % (1805527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.82/6.56 % (1805527)CaDiCaL version: 2.1.3
% 42.82/6.56 % (1805527)Termination reason: Instruction limit
% 42.82/6.56 % (1805527)Termination phase: Saturation
% 42.82/6.56 % (1805527)Time elapsed: 0.083 s
% 42.82/6.56 % (1805527)Peak memory usage: 14 MB
% 42.82/6.56 % (1805527)Instructions burned: 181 (million)
% 42.82/6.56 % (1805532)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3494394565:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 42.82/6.56 % (1805522)Instruction limit reached!
% 42.82/6.56 % (1805522)------------------------------
% 42.82/6.56 % (1805522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.82/6.56 % (1805522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.82/6.56 % (1805522)CaDiCaL version: 2.1.3
% 42.82/6.56 % (1805522)Termination reason: Instruction limit
% 42.82/6.56 % (1805522)Termination phase: Finite model building preprocessing
% 42.82/6.56 % (1805522)Time elapsed: 0.180 s
% 42.82/6.56 % (1805522)Peak memory usage: 21 MB
% 42.82/6.56 % (1805522)Instructions burned: 718 (million)
% 42.82/6.56 % (1805534)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3705260330:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 42.82/6.56 % (1805525)Instruction limit reached!
% 42.82/6.56 % (1805525)------------------------------
% 42.82/6.56 % (1805525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.82/6.56 % (1805525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.82/6.56 % (1805525)CaDiCaL version: 2.1.3
% 42.82/6.56 % (1805525)Termination reason: Instruction limit
% 42.82/6.56 % (1805525)Termination phase: Saturation
% 42.82/6.56 % (1805525)Time elapsed: 0.326 s
% 42.82/6.56 % (1805525)Peak memory usage: 18 MB
% 42.82/6.56 % (1805525)Instructions burned: 686 (million)
% 42.82/6.56 % (1805536)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=982096924:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 42.82/6.56 % (1805530)Instruction limit reached!
% 42.82/6.56 % (1805530)------------------------------
% 42.82/6.56 % (1805530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.82/6.56 % (1805530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.82/6.56 % (1805530)CaDiCaL version: 2.1.3
% 42.82/6.56 % (1805530)Termination reason: Instruction limit
% 42.82/6.56 % (1805530)Termination phase: Saturation
% 42.82/6.56 % (1805530)Time elapsed: 0.289 s
% 42.82/6.56 % (1805530)Peak memory usage: 16 MB
% 42.82/6.56 % (1805530)Instructions burned: 478 (million)
% 42.82/6.56 % (1805538)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=1648987313:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 42.82/6.56 % (1805534)Instruction limit reached!
% 42.82/6.56 % (1805534)------------------------------
% 42.82/6.56 % (1805534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.82/6.56 % (1805534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.82/6.56 % (1805534)CaDiCaL version: 2.1.3
% 42.82/6.56 % (1805534)Termination reason: Instruction limit
% 42.82/6.56 % (1805534)Termination phase: Saturation
% 42.82/6.56 % (1805534)Time elapsed: 0.367 s
% 42.82/6.56 % (1805534)Peak memory usage: 23 MB
% 42.82/6.56 % (1805534)Instructions burned: 1180 (million)
% 42.82/6.56 % (1805540)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=637563185:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 42.82/6.56 % (1805532)Instruction limit reached!
% 42.82/6.56 % (1805532)------------------------------
% 42.82/6.56 % (1805532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.82/6.56 % (1805532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.71/11.63 % (1805532)CaDiCaL version: 2.1.3
% 78.71/11.63 % (1805532)Termination reason: Instruction limit
% 78.71/11.63 % (1805532)Termination phase: Finite model building preprocessing
% 78.71/11.63 % (1805532)Time elapsed: 0.412 s
% 78.71/11.63 % (1805532)Peak memory usage: 22 MB
% 78.71/11.63 % (1805532)Instructions burned: 867 (million)
% 78.71/11.63 % (1805542)fmb+10_1_sil=64000:random_seed=3512790766:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 78.71/11.63 % (1805540)Instruction limit reached!
% 78.71/11.63 % (1805540)------------------------------
% 78.71/11.63 % (1805540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.71/11.63 % (1805540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.71/11.63 % (1805540)CaDiCaL version: 2.1.3
% 78.71/11.63 % (1805540)Termination reason: Instruction limit
% 78.71/11.63 % (1805540)Termination phase: Saturation
% 78.71/11.63 % (1805540)Time elapsed: 0.252 s
% 78.71/11.63 % (1805540)Peak memory usage: 19 MB
% 78.71/11.63 % (1805540)Instructions burned: 882 (million)
% 78.71/11.63 % (1805536)Instruction limit reached!
% 78.71/11.63 % (1805536)------------------------------
% 78.71/11.63 % (1805536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.71/11.63 % (1805536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.71/11.63 % (1805536)CaDiCaL version: 2.1.3
% 78.71/11.63 % (1805536)Termination reason: Instruction limit
% 78.71/11.63 % (1805536)Termination phase: Finite model building preprocessing
% 78.71/11.63 % (1805536)Time elapsed: 0.424 s
% 78.71/11.63 % (1805536)Peak memory usage: 23 MB
% 78.71/11.63 % (1805536)Instructions burned: 890 (million)
% 78.71/11.63 % (1805538)Instruction limit reached!
% 78.71/11.63 % (1805538)------------------------------
% 78.71/11.63 % (1805538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.71/11.63 % (1805538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.71/11.63 % (1805538)CaDiCaL version: 2.1.3
% 78.71/11.63 % (1805538)Termination reason: Instruction limit
% 78.71/11.63 % (1805538)Termination phase: Saturation
% 78.71/11.63 % (1805538)Time elapsed: 0.405 s
% 78.71/11.63 % (1805538)Peak memory usage: 18 MB
% 78.71/11.63 % (1805538)Instructions burned: 692 (million)
% 78.71/11.63 % (1805544)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3014450624:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 78.71/11.63 % (1805545)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3426989906:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 78.71/11.63 % (1805547)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=635385806:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 78.71/11.63 % (1805545)Instruction limit reached!
% 78.71/11.63 % (1805545)------------------------------
% 78.71/11.63 % (1805545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.71/11.63 % (1805545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.71/11.63 % (1805545)CaDiCaL version: 2.1.3
% 78.71/11.63 % (1805545)Termination reason: Instruction limit
% 78.71/11.63 % (1805545)Termination phase: Finite model building preprocessing
% 78.71/11.63 % (1805545)Time elapsed: 0.441 s
% 78.71/11.63 % (1805545)Peak memory usage: 23 MB
% 78.71/11.63 % (1805545)Instructions burned: 920 (million)
% 78.71/11.63 % (1805550)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3008305947:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 78.71/11.63 % TRYING [1,1,1,1,1]
% 78.71/11.63 % TRYING [2,1,1,1,1]
% 78.71/11.63 % TRYING [20,20,20,20,20]
% 78.71/11.63 % TRYING [2,1,1,1,2]
% 78.71/11.63 % TRYING [2,1,1,2,2]
% 78.71/11.63 % TRYING [2,1,2,2,2]
% 78.71/11.63 % (1805550)Instruction limit reached!
% 78.71/11.63 % (1805550)------------------------------
% 78.71/11.63 % (1805550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 78.71/11.63 % (1805550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.71/11.63 % (1805550)CaDiCaL version: 2.1.3
% 78.71/11.63 % (1805550)Termination reason: Instruction limit
% 78.71/11.63 % (1805550)Termination phase: Saturation
% 78.71/11.63 % (1805550)Time elapsed: 0.853 s
% 78.71/11.63 % (1805550)Peak memory usage: 34 MB
% 78.71/11.63 % (1805550)Instructions burned: 1473 (million)
% 78.71/11.63 % (1805552)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3676077681:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 78.71/11.63 % TRYING [3,1,2,2,2]
% 78.71/11.63 % TRYING [1,1,1,1,1]
% 78.71/11.63 % TRYING [1,1,1,1,2]
% 78.71/11.63 % TRYING [1,1,1,2,2]
% 78.71/11.63 % TRYING [1,1,2,2,2]
% 78.71/11.63 % TRYING [4,1,2,2,2]
% 78.71/11.63 % TRYING [2,1,2,2,2]
% 78.71/11.63 % (1805544)Instruction limit reached!
% 78.71/11.63 % (1805544)------------------------------
% 159.37/24.28 % (1805544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.37/24.28 % (1805544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.37/24.28 % (1805544)CaDiCaL version: 2.1.3
% 159.37/24.28 % (1805544)Termination reason: Instruction limit
% 159.37/24.28 % (1805544)Termination phase: Finite model building constraint generation
% 159.37/24.28 % (1805544)Time elapsed: 2.071 s
% 159.37/24.28 % (1805544)Peak memory usage: 401 MB
% 159.37/24.28 % (1805544)Instructions burned: 9517 (million)
% 159.37/24.28 % (1805554)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2923729545:fmbsr=2.30978:i=2174_2969 on theBenchmark for (2969ds/2174Mi)
% 159.37/24.28 % TRYING [3,1,2,2,3]
% 159.37/24.28 % TRYING [4,1,2,2,3]
% 159.37/24.28 % (1805554)Instruction limit reached!
% 159.37/24.28 % (1805554)------------------------------
% 159.37/24.28 % (1805554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.37/24.28 % (1805554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.37/24.28 % (1805554)CaDiCaL version: 2.1.3
% 159.37/24.28 % (1805554)Termination reason: Instruction limit
% 159.37/24.28 % (1805554)Termination phase: Finite model building preprocessing
% 159.37/24.28 % (1805554)Time elapsed: 0.556 s
% 159.37/24.28 % (1805554)Peak memory usage: 33 MB
% 159.37/24.28 % (1805554)Instructions burned: 2175 (million)
% 159.37/24.28 % (1805556)ott-2_1_sil=16000:newcnf=on:random_seed=928260213:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2963 on theBenchmark for (2963ds/869Mi)
% 159.37/24.28 % (1805547)Instruction limit reached!
% 159.37/24.28 % (1805547)------------------------------
% 159.37/24.28 % (1805547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.37/24.28 % (1805547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.37/24.28 % (1805547)CaDiCaL version: 2.1.3
% 159.37/24.28 % (1805547)Termination reason: Instruction limit
% 159.37/24.28 % (1805547)Termination phase: Saturation
% 159.37/24.28 % (1805547)Time elapsed: 2.858 s
% 159.37/24.28 % (1805547)Peak memory usage: 39 MB
% 159.37/24.28 % (1805547)Instructions burned: 5132 (million)
% 159.37/24.28 % (1805558)ott+10_1_sil=32000:tgt=ground:random_seed=397731038:i=5114:av=off_2961 on theBenchmark for (2961ds/5114Mi)
% 159.37/24.28 % TRYING [3,1,2,2,2]
% 159.37/24.28 % (1805556)Instruction limit reached!
% 159.37/24.28 % (1805556)------------------------------
% 159.37/24.28 % (1805556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.37/24.28 % (1805556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.37/24.28 % (1805556)CaDiCaL version: 2.1.3
% 159.37/24.28 % (1805556)Termination reason: Instruction limit
% 159.37/24.28 % (1805556)Termination phase: Saturation
% 159.37/24.28 % (1805556)Time elapsed: 0.260 s
% 159.37/24.28 % (1805556)Peak memory usage: 20 MB
% 159.37/24.28 % (1805556)Instructions burned: 873 (million)
% 159.37/24.28 % (1805560)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=647735655:i=54282_2961 on theBenchmark for (2961ds/54282Mi)
% 159.37/24.28 % (1805552)Cannot represent all propositional literals internally
% 159.37/24.28 % (1805552)Refutation not found, incomplete strategy
% 159.37/24.28 % (1805552)------------------------------
% 159.37/24.28 % (1805552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.37/24.28 % (1805552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.37/24.28 % (1805552)CaDiCaL version: 2.1.3
% 159.37/24.28 % (1805552)Termination reason: Refutation not found, incomplete strategy
% 159.37/24.28 % (1805552)Time elapsed: 1.795 s
% 159.37/24.28 % (1805552)Peak memory usage: 50 MB
% 159.37/24.28 % (1805552)Instructions burned: 3859 (million)
% 159.37/24.28 % (1805552)------------------------------
% 159.37/24.28 % (1805552)------------------------------
% 159.37/24.28 % (1805562)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1160475663:i=3512:aac=none_2958 on theBenchmark for (2958ds/3512Mi)
% 159.37/24.28 % TRYING [3,1,3,2,3]
% 159.37/24.28 % TRYING [5,1,2,2,2]
% 159.37/24.28 % TRYING [1,1,1,1,1]
% 159.37/24.28 % TRYING [2,1,1,1,1]
% 159.37/24.28 % TRYING [2,1,1,1,2]
% 159.37/24.28 % TRYING [2,1,1,2,2]
% 159.37/24.28 % TRYING [2,1,2,2,2]
% 159.37/24.28 % TRYING [3,1,2,2,2]
% 159.37/24.28 % TRYING [4,1,2,2,2]
% 159.37/24.28 % TRYING [4,1,3,2,3]
% 159.37/24.28 % TRYING [4,1,2,2,2]
% 159.37/24.28 % TRYING [3,1,2,2,3]
% 159.37/24.28 % TRYING [4,1,2,2,3]
% 159.37/24.28 % (1805562)Instruction limit reached!
% 159.37/24.28 % (1805562)------------------------------
% 159.37/24.28 % (1805562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.37/24.28 % (1805562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.37/24.28 % (1805562)CaDiCaL version: 2.1.3
% 159.37/24.28 % (1805562)Termination reason: Instruction limit
% 82.32/28.11 % (1805562)Termination phase: Saturation
% 82.32/28.11 % (1805562)Time elapsed: 2.018 s
% 82.32/28.11 % (1805562)Peak memory usage: 34 MB
% 82.32/28.11 % (1805562)Instructions burned: 3513 (million)
% 82.32/28.11 % (1805564)dis+21_1_sil=32000:sas=cadical:random_seed=1967328581:i=3773:amm=off_2938 on theBenchmark for (2938ds/3773Mi)
% 82.32/28.11 % TRYING [3,1,3,2,3]
% 82.32/28.11 % TRYING [3,1,4,2,3]
% 82.32/28.11 % TRYING [5,1,2,2,2]
% 82.32/28.11 % TRYING [4,1,3,2,3]
% 82.32/28.11 % (1805558)Instruction limit reached!
% 82.32/28.11 % (1805558)------------------------------
% 82.32/28.11 % (1805558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.32/28.11 % (1805558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.32/28.11 % (1805558)CaDiCaL version: 2.1.3
% 82.32/28.11 % (1805558)Termination reason: Instruction limit
% 82.32/28.11 % (1805558)Termination phase: Saturation
% 82.32/28.11 % (1805558)Time elapsed: 3.010 s
% 82.32/28.11 % (1805558)Peak memory usage: 41 MB
% 82.32/28.11 % (1805558)Instructions burned: 5115 (million)
% 82.32/28.11 % (1805566)ott+11_1_sil=16000:gs=on:random_seed=932622284:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2931 on theBenchmark for (2931ds/2251Mi)
% 82.32/28.11 % TRYING [5,1,2,2,3]
% 82.32/28.11 % TRYING [3,1,4,2,3]
% 82.32/28.11 % TRYING [5,1,2,2,3]
% 82.32/28.11 % TRYING [6,1,2,2,2]
% 82.32/28.11 % TRYING [5,1,2,2,2]
% 82.32/28.11 % (1805566)Instruction limit reached!
% 82.32/28.11 % (1805566)------------------------------
% 82.32/28.11 % (1805566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.32/28.11 % (1805566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.32/28.11 % (1805566)CaDiCaL version: 2.1.3
% 82.32/28.11 % (1805566)Termination reason: Instruction limit
% 82.32/28.11 % (1805566)Termination phase: Saturation
% 82.32/28.11 % (1805566)Time elapsed: 1.281 s
% 82.32/28.11 % (1805566)Peak memory usage: 31 MB
% 82.32/28.11 % (1805566)Instructions burned: 2251 (million)
% 82.32/28.11 % (1805568)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4100525979:fmbsr=1.6:i=67534_2918 on theBenchmark for (2918ds/67534Mi)
% 82.32/28.11 % TRYING [6,1,2,2,2]
% 82.32/28.11 % (1805564)Instruction limit reached!
% 82.32/28.11 % (1805564)------------------------------
% 82.32/28.11 % (1805564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.32/28.11 % (1805564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.32/28.11 % (1805564)CaDiCaL version: 2.1.3
% 82.32/28.11 % (1805564)Termination reason: Instruction limit
% 82.32/28.11 % (1805564)Termination phase: Saturation
% 82.32/28.11 % (1805564)Time elapsed: 2.155 s
% 82.32/28.11 % (1805564)Peak memory usage: 35 MB
% 82.32/28.11 % (1805564)Instructions burned: 3773 (million)
% 82.32/28.11 % (1805570)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3302488259:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2916 on theBenchmark for (2916ds/4591Mi)
% 82.32/28.11 % TRYING [6,1,2,2,3]
% 82.32/28.11 % TRYING [6,1,2,2,3]
% 82.32/28.11 % TRYING [5,1,3,2,3]
% 82.32/28.11 % TRYING [5,1,3,2,3]
% 82.32/28.11 % TRYING [3,1,4,2,4]
% 82.32/28.11 % TRYING [7]
% 82.32/28.11 % TRYING [7,1,2,2,2]
% 82.32/28.11 % (1805570)Instruction limit reached!
% 82.32/28.11 % (1805570)------------------------------
% 82.32/28.11 % (1805570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.32/28.11 % (1805570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.32/28.11 % (1805570)CaDiCaL version: 2.1.3
% 82.32/28.11 % (1805570)Termination reason: Instruction limit
% 82.32/28.11 % (1805570)Termination phase: Saturation
% 82.32/28.11 % (1805570)Time elapsed: 2.563 s
% 82.32/28.11 % (1805570)Peak memory usage: 65 MB
% 82.32/28.11 % (1805570)Instructions burned: 4592 (million)
% 82.32/28.11 % (1805572)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1065181328:i=29340_2890 on theBenchmark for (2890ds/29340Mi)
% 82.32/28.11 % TRYING [3,1,4,2,4]
% 82.32/28.11 % (1805542)Instruction limit reached!
% 82.32/28.11 % (1805542)------------------------------
% 82.32/28.11 % (1805542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.32/28.11 % (1805542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.32/28.11 % (1805542)CaDiCaL version: 2.1.3
% 82.32/28.11 % (1805542)Termination reason: Instruction limit
% 82.32/28.11 % (1805542)Termination phase: Finite model building SAT solving
% 82.32/28.11 % (1805542)Time elapsed: 10.380 s
% 82.32/28.11 % (1805542)Peak memory usage: 176 MB
% 82.32/28.11 % (1805542)Instructions burned: 22061 (million)
% 82.32/28.11 % (1805574)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2470629153:i=5211_2888 on theBenchmark for (2888ds/5211Mi)
% 82.32/28.11 % TRYING [4,1,4,2,4]
% 82.32/28.11 % TRYING [7,1,2,2,2]
% 82.32/28.11 % TRYING [7,1,2,2,3]
% 82.32/28.11 % TRYING [6,1,3,2,3]
% 82.32/28.11 % TRYING [4,1,4,2,4]
% 82.32/28.11 % TRYING [5,1,4,2,3]
% 82.32/28.11 % (1805574)Instruction limit reached!
% 82.32/28.11 % (1805574)------------------------------
% 82.32/28.11 % (1805574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.32/28.11 % (1805574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.32/28.11 % (1805574)CaDiCaL version: 2.1.3
% 82.32/28.11 % (1805574)Termination reason: Instruction limit
% 82.32/28.11 % (1805574)Termination phase: Saturation
% 82.32/28.11 % (1805574)Time elapsed: 2.621 s
% 82.32/28.11 % (1805574)Peak memory usage: 42 MB
% 82.32/28.11 % (1805574)Instructions burned: 5211 (million)
% 82.32/28.11 % (1805593)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3181327121:i=5497:nm=2_2862 on theBenchmark for (2862ds/5497Mi)
% 82.32/28.11 % TRYING [8,1,2,2,2]
% 82.32/28.11 % TRYING [7,1,2,2,3]
% 82.32/28.11 % (1805560)Instruction limit reached!
% 82.32/28.11 % (1805560)------------------------------
% 82.32/28.11 % (1805560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.32/28.11 % (1805560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.32/28.11 % (1805560)CaDiCaL version: 2.1.3
% 82.32/28.11 % (1805560)Termination reason: Instruction limit
% 82.32/28.11 % (1805560)Termination phase: Finite model building constraint generation
% 82.32/28.11 % (1805560)Time elapsed: 10.912 s
% 82.32/28.11 % (1805560)Peak memory usage: 371 MB
% 82.32/28.11 % (1805560)Instructions burned: 54284 (million)
% 82.32/28.11 % (1805730)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4010746587:fmbsr=2:i=46332_2851 on theBenchmark for (2851ds/46332Mi)
% 82.32/28.11 % TRYING [15]
% 82.32/28.11 % TRYING [17,17,17,17,17]
% 82.32/28.11 % TRYING [6,1,3,2,3]
% 82.32/28.11 % (1805593)Instruction limit reached!
% 82.32/28.11 % (1805593)------------------------------
% 82.32/28.11 % (1805593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.32/28.11 % (1805593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.32/28.11 % (1805593)CaDiCaL version: 2.1.3
% 82.32/28.11 % (1805593)Termination reason: Instruction limit
% 82.32/28.11 % (1805593)Termination phase: Finite model building constraint generation
% 82.32/28.11 % (1805593)Time elapsed: 2.361 s
% 82.32/28.11 % (1805593)Peak memory usage: 155 MB
% 82.32/28.11 % (1805593)Instructions burned: 5499 (million)
% 82.32/28.11 % (1805732)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=94493595:i=14071_2838 on theBenchmark for (2838ds/14071Mi)
% 82.32/28.11 % TRYING [5,1,4,2,3]
% 82.32/28.11 % TRYING [12,12,12,12,12]
% 82.32/28.11 % TRYING [8,1,2,2,2]
% 82.32/28.11 % TRYING [5,1,4,2,4]
% 82.32/28.11 % (1805732)Instruction limit reached!
% 82.32/28.11 % (1805732)------------------------------
% 82.32/28.11 % (1805732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.32/28.11 % (1805732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.32/28.11 % (1805732)CaDiCaL version: 2.1.3
% 82.32/28.11 % (1805732)Termination reason: Instruction limit
% 82.32/28.11 % (1805732)Termination phase: Finite model building constraint generation
% 82.32/28.11 % (1805732)Time elapsed: 5.422 s
% 82.32/28.11 % (1805732)Peak memory usage: 701 MB
% 82.32/28.11 % (1805732)Instructions burned: 14073 (million)
% 82.32/28.11 % (1805734)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3369076773:i=22565:add=on:rawr=on_2783 on theBenchmark for (2783ds/22565Mi)
% 82.32/28.11 % TRYING [4,1,5,2,4]
% 82.32/28.11 % (1805730)Instruction limit reached!
% 82.32/28.11 % (1805730)------------------------------
% 82.32/28.11 % (1805730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.32/28.11 % (1805730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.32/28.11 % (1805730)CaDiCaL version: 2.1.3
% 82.32/28.11 % (1805730)Termination reason: Instruction limit
% 82.32/28.11 % (1805730)Termination phase: Finite model building constraint generation
% 82.32/28.11 % (1805730)Time elapsed: 8.755 s
% 82.32/28.11 % (1805730)Peak memory usage: 2655 MB
% 82.32/28.11 % (1805730)Instructions burned: 46337 (million)
% 82.32/28.11 % (1805736)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2783632324:i=8173:av=off_2761 on theBenchmark for (2761ds/8173Mi)
% 82.32/28.11 % (1805572)Instruction limit reached!
% 82.32/28.11 % (1805572)------------------------------
% 82.32/28.11 % (1805572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.32/28.11 % (1805572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.32/28.11 % (1805572)CaDiCaL version: 2.1.3
% 82.32/28.11 % (1805572)Termination reason: Instruction limit
% 82.32/28.11 % (1805572)Termination phase: Saturation
% 82.32/28.11 % (1805572)Time elapsed: 12.920 s
% 82.32/28.11 % (1805572)Peak memory usage: 146 MB
% 82.32/28.11 % (1805572)Instructions burned: 29341 (million)
% 82.32/28.11 % (1805738)dis+10_16:1_sil=16000:random_seed=2157521343:i=9155:fsr=off_2761 on theBenchmark for (2761ds/9155Mi)
% 82.32/28.11 % TRYING [8,1,2,2,3]
% 82.32/28.11 % (1805736)Instruction limit reached!
% 82.32/28.11 % (1805736)------------------------------
% 82.32/28.11 % (1805736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.32/28.11 % (1805736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.32/28.11 % (1805736)CaDiCaL version: 2.1.3
% 82.32/28.11 % (1805736)Termination reason: Instruction limit
% 82.32/28.11 % (1805736)Termination phase: Saturation
% 82.32/28.11 % (1805736)Time elapsed: 2.544 s
% 82.32/28.11 % (1805736)Peak memory usage: 61 MB
% 82.32/28.11 % (1805736)Instructions burned: 8173 (million)
% 82.32/28.11 % (1805740)ott-3_8_sil=64000:random_seed=1619794320:i=20139:bs=on_2736 on theBenchmark for (2736ds/20139Mi)
% 82.32/28.11 % TRYING [7,1,3,2,3]
% 82.32/28.11 % (1805740) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1805503-1805740"...
% 82.32/28.11 % (1805740)...printing done.
% 82.32/28.11 % (1805740)Refutation found. Thanks to Tanya!
% 82.32/28.11 % SZS status Theorem for theBenchmark
% 82.32/28.11 % SZS output start Proof for theBenchmark
% See solution above
% 82.32/28.11 % (1805740)------------------------------
% 82.32/28.11 % (1805740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 82.32/28.11 % (1805740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.32/28.11 % (1805740)CaDiCaL version: 2.1.3
% 82.32/28.11 % (1805740)Termination reason: Refutation
% 82.32/28.11 % (1805740)Time elapsed: 0.954 s
% 82.32/28.11 % (1805740)Peak memory usage: 30 MB
% 82.32/28.11 % (1805740)Instructions burned: 3130 (million)
% 82.32/28.11 % (1805503)Success in time 27.693 s
% 82.32/28.11 % Vampire exiting
%------------------------------------------------------------------------------