%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP046^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : 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 : Wed Sep 30 08:08:06 AM UTC 2026
% Result : Theorem 5.44s 1.23s
% Output : Refutation 5.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 8
% Syntax : Number of formulae : 42 ( 21 unt; 0 typ; 4 def)
% Number of atoms : 93 ( 29 equ; 0 cnn)
% Maximal formula atoms : 3 ( 2 avg)
% Number of connectives : 153 ( 29 ~; 18 |; 0 &; 99 @)
% ( 4 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 36 ( 35 usr)
% Number of type conns : 6 ( 6 >; 0 *; 0 +; 0 <<)
% Number of symbols : 339 ( 336 usr; 34 con; 0-7 aty)
% Number of variables : 18 ( 0 sgn 18 !; 0 ?; 18 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
set_Pr1409704485_r_l_v: $tType ).
thf(type_def_6,type,
produc1389397445_r_l_v: $tType ).
thf(type_def_7,type,
option1457017436_r_l_v: $tType ).
thf(type_def_8,type,
produc1156025366_r_l_v: $tType ).
thf(type_def_9,type,
produc1164766533_r_l_v: $tType ).
thf(type_def_10,type,
set_set_Sum_sum_r_l: $tType ).
thf(type_def_11,type,
set_set_Sum_sum_l_r: $tType ).
thf(type_def_12,type,
set_set_Sum_sum_l_l: $tType ).
thf(type_def_13,type,
option_val_r_l_v: $tType ).
thf(type_def_14,type,
set_Product_prod_r_r: $tType ).
thf(type_def_15,type,
set_Product_prod_r_l: $tType ).
thf(type_def_16,type,
set_Product_prod_l_r: $tType ).
thf(type_def_17,type,
set_Product_prod_l_l: $tType ).
thf(type_def_18,type,
set_set_set_r: $tType ).
thf(type_def_19,type,
set_set_set_l: $tType ).
thf(type_def_20,type,
set_Sum_sum_r_r: $tType ).
thf(type_def_21,type,
set_Sum_sum_r_l: $tType ).
thf(type_def_22,type,
set_Sum_sum_l_r: $tType ).
thf(type_def_23,type,
set_Sum_sum_l_l: $tType ).
thf(type_def_24,type,
set_option_r: $tType ).
thf(type_def_25,type,
set_option_l: $tType ).
thf(type_def_26,type,
cntxt_r_l_v: $tType ).
thf(type_def_27,type,
set_set_r: $tType ).
thf(type_def_28,type,
set_set_l: $tType ).
thf(type_def_29,type,
expr_r_l_v: $tType ).
thf(type_def_30,type,
sum_sum_r_l: $tType ).
thf(type_def_31,type,
sum_sum_l_r: $tType ).
thf(type_def_32,type,
sum_sum_l_l: $tType ).
thf(type_def_33,type,
val_r_l_v: $tType ).
thf(type_def_34,type,
set_r: $tType ).
thf(type_def_35,type,
set_l: $tType ).
thf(type_def_36,type,
const: $tType ).
thf(type_def_37,type,
v: $tType ).
thf(type_def_38,type,
r: $tType ).
thf(type_def_39,type,
l: $tType ).
thf(type_def_40,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
combine_l_val_r_l_v: ( l > option_val_r_l_v ) > ( l > option_val_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_1,type,
f: const ).
thf(func_def_2,type,
t: const ).
thf(func_def_3,type,
unit: const ).
thf(func_def_4,type,
doms_l_r_v: produc1156025366_r_l_v > set_l ).
thf(func_def_5,type,
assign_r_l_v: expr_r_l_v > expr_r_l_v > expr_r_l_v ).
thf(func_def_6,type,
ite_r_l_v: expr_r_l_v > expr_r_l_v > expr_r_l_v > expr_r_l_v ).
thf(func_def_7,type,
read_r_l_v: expr_r_l_v > expr_r_l_v ).
thf(func_def_8,type,
ref_r_l_v: expr_r_l_v > expr_r_l_v ).
thf(func_def_9,type,
rfork_r_l_v: expr_r_l_v > expr_r_l_v ).
thf(func_def_10,type,
rjoin_r_l_v: expr_r_l_v > expr_r_l_v ).
thf(func_def_11,type,
vE_r_l_v: val_r_l_v > expr_r_l_v ).
thf(func_def_12,type,
plug_r_l_v: cntxt_r_l_v > expr_r_l_v > expr_r_l_v ).
thf(func_def_13,type,
cV_r_l_v: const > val_r_l_v ).
thf(func_def_14,type,
loc_l_r_v: l > val_r_l_v ).
thf(func_def_15,type,
rid_r_l_v: r > val_r_l_v ).
thf(func_def_16,type,
execution_r_l_v: ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > expr_r_l_v > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > $o ).
thf(func_def_17,type,
induct1670415253_r_l_v: ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > ( ( r > option1457017436_r_l_v ) > $o ) > $o ).
thf(func_def_18,type,
maxima311842975_r_l_v: ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > expr_r_l_v > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > $o ).
thf(func_def_19,type,
reachable_r_l_v: ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > ( r > option1457017436_r_l_v ) > $o ).
thf(func_def_20,type,
steps_r_l_v: ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > set_Pr1409704485_r_l_v ).
thf(func_def_21,type,
terminates_in_r_l_v: ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > expr_r_l_v > ( r > option1457017436_r_l_v ) > $o ).
thf(func_def_22,type,
finite2114249848tion_l: set_option_l > $o ).
thf(func_def_23,type,
finite16335230tion_r: set_option_r > $o ).
thf(func_def_24,type,
finite1853159534_r_l_v: set_Pr1409704485_r_l_v > $o ).
thf(func_def_25,type,
finite785973648od_l_l: set_Product_prod_l_l > $o ).
thf(func_def_26,type,
finite835542678od_l_r: set_Product_prod_l_r > $o ).
thf(func_def_27,type,
finite1457622794od_r_l: set_Product_prod_r_l > $o ).
thf(func_def_28,type,
finite1507191824od_r_r: set_Product_prod_r_r > $o ).
thf(func_def_29,type,
finite1256628466_set_l: set_set_set_l > $o ).
thf(func_def_30,type,
finite1651563256_set_r: set_set_set_r > $o ).
thf(func_def_31,type,
finite88277554um_l_l: set_set_Sum_sum_l_l > $o ).
thf(func_def_32,type,
finite483212344um_l_r: set_set_Sum_sum_l_r > $o ).
thf(func_def_33,type,
finite1407742636um_r_l: set_set_Sum_sum_r_l > $o ).
thf(func_def_34,type,
finite_finite_set_l: set_set_l > $o ).
thf(func_def_35,type,
finite_finite_set_r: set_set_r > $o ).
thf(func_def_36,type,
finite1541484284um_l_l: set_Sum_sum_l_l > $o ).
thf(func_def_37,type,
finite1591053314um_l_r: set_Sum_sum_l_r > $o ).
thf(func_def_38,type,
finite65649782um_r_l: set_Sum_sum_r_l > $o ).
thf(func_def_39,type,
finite115218812um_r_r: set_Sum_sum_r_r > $o ).
thf(func_def_40,type,
finite_finite_l: set_l > $o ).
thf(func_def_41,type,
finite_finite_r: set_r > $o ).
thf(func_def_42,type,
fun_up1835647912_r_l_v: ( l > option_val_r_l_v ) > l > option_val_r_l_v > l > option_val_r_l_v ).
thf(func_def_43,type,
fun_up709272714_r_l_v: ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v > r > option1457017436_r_l_v ).
thf(func_def_44,type,
if_option_val_r_l_v: $o > option_val_r_l_v > option_val_r_l_v > option_val_r_l_v ).
thf(func_def_45,type,
if_opt1153928738_r_l_v: $o > option1457017436_r_l_v > option1457017436_r_l_v > option1457017436_r_l_v ).
thf(func_def_46,type,
dom_Pr939617279_r_l_v: ( produc1389397445_r_l_v > option_val_r_l_v ) > set_Pr1409704485_r_l_v ).
thf(func_def_47,type,
dom_Pr1162080227_r_l_v: ( produc1389397445_r_l_v > option1457017436_r_l_v ) > set_Pr1409704485_r_l_v ).
thf(func_def_48,type,
dom_l_val_r_l_v: ( l > option_val_r_l_v ) > set_l ).
thf(func_def_49,type,
dom_l_45837855_r_l_v: ( l > option1457017436_r_l_v ) > set_l ).
thf(func_def_50,type,
dom_r_val_r_l_v: ( r > option_val_r_l_v ) > set_r ).
thf(func_def_51,type,
dom_r_259548057_r_l_v: ( r > option1457017436_r_l_v ) > set_r ).
thf(func_def_52,type,
lID_G_r_l_v: ( r > option1457017436_r_l_v ) > set_l ).
thf(func_def_53,type,
lID_L_l_r_v: produc1156025366_r_l_v > set_l ).
thf(func_def_54,type,
rID_G_r_l_v: ( r > option1457017436_r_l_v ) > set_r ).
thf(func_def_55,type,
rID_L_l_r_v: produc1156025366_r_l_v > set_r ).
thf(func_def_56,type,
domain87684397_l_r_v: produc1156025366_r_l_v > $o ).
thf(func_def_57,type,
domain1547879849_r_l_v: ( r > option1457017436_r_l_v ) > $o ).
thf(func_def_58,type,
revision_step_r_l_v: ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > r > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > $o ).
thf(func_def_59,type,
revisi1291188644_r_l_v: ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > r > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > $o ).
thf(func_def_60,type,
subsum148050133_r_l_v: r > r > ( r > option1457017436_r_l_v ) > $o ).
thf(func_def_61,type,
subsum680764357_r_l_v: ( r > option1457017436_r_l_v ) > $o ).
thf(func_def_62,type,
none_val_r_l_v: option_val_r_l_v ).
thf(func_def_63,type,
none_P277133687_r_l_v: option1457017436_r_l_v ).
thf(func_def_64,type,
some_val_r_l_v: val_r_l_v > option_val_r_l_v ).
thf(func_def_65,type,
some_P1807977723_r_l_v: produc1156025366_r_l_v > option1457017436_r_l_v ).
thf(func_def_66,type,
the_val_r_l_v: option_val_r_l_v > val_r_l_v ).
thf(func_def_67,type,
ord_le2116509289_set_l: set_set_l > set_set_l > $o ).
thf(func_def_68,type,
ord_le363960431_set_r: set_set_r > set_set_r > $o ).
thf(func_def_69,type,
ord_le1122554619um_l_l: set_Sum_sum_l_l > set_Sum_sum_l_l > $o ).
thf(func_def_70,type,
ord_le1517489409um_l_r: set_Sum_sum_l_r > set_Sum_sum_l_r > $o ).
thf(func_def_71,type,
ord_le294536053um_r_l: set_Sum_sum_r_l > set_Sum_sum_r_l > $o ).
thf(func_def_72,type,
ord_less_eq_set_l: set_l > set_l > $o ).
thf(func_def_73,type,
ord_less_eq_set_r: set_r > set_r > $o ).
thf(func_def_74,type,
top_top_set_option_l: set_option_l ).
thf(func_def_75,type,
top_top_set_option_r: set_option_r ).
thf(func_def_76,type,
top_to1238153077_r_l_v: set_Pr1409704485_r_l_v ).
thf(func_def_77,type,
top_to320296343od_l_l: set_Product_prod_l_l ).
thf(func_def_78,type,
top_to715231133od_l_r: set_Product_prod_l_r ).
thf(func_def_79,type,
top_to1639761425od_r_l: set_Product_prod_r_l ).
thf(func_def_80,type,
top_to2034696215od_r_r: set_Product_prod_r_r ).
thf(func_def_81,type,
top_top_set_set_l: set_set_l ).
thf(func_def_82,type,
top_top_set_set_r: set_set_r ).
thf(func_def_83,type,
top_to1010946379um_l_l: set_Sum_sum_l_l ).
thf(func_def_84,type,
top_to1405881169um_l_r: set_Sum_sum_l_r ).
thf(func_def_85,type,
top_to182927813um_r_l: set_Sum_sum_r_l ).
thf(func_def_86,type,
top_to577862603um_r_r: set_Sum_sum_r_r ).
thf(func_def_87,type,
top_top_set_l: set_l ).
thf(func_def_88,type,
top_top_set_r: set_r ).
thf(func_def_89,type,
produc1834103605_r_l_v: ( l > option_val_r_l_v ) > expr_r_l_v > produc1164766533_r_l_v ).
thf(func_def_90,type,
produc297528454_r_l_v: ( l > option_val_r_l_v ) > produc1164766533_r_l_v > produc1156025366_r_l_v ).
thf(func_def_91,type,
produc1175464189_r_l_v: ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > produc1389397445_r_l_v ).
thf(func_def_92,type,
eq_states_r_l_v: ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > $o ).
thf(func_def_93,type,
collec1978425008_r_l_v: ( produc1389397445_r_l_v > $o ) > set_Pr1409704485_r_l_v ).
thf(func_def_94,type,
collect_set_set_l: ( set_set_l > $o ) > set_set_set_l ).
thf(func_def_95,type,
collect_set_set_r: ( set_set_r > $o ) > set_set_set_r ).
thf(func_def_96,type,
collec1593187440um_l_l: ( set_Sum_sum_l_l > $o ) > set_set_Sum_sum_l_l ).
thf(func_def_97,type,
collec1988122230um_l_r: ( set_Sum_sum_l_r > $o ) > set_set_Sum_sum_l_r ).
thf(func_def_98,type,
collec765168874um_r_l: ( set_Sum_sum_r_l > $o ) > set_set_Sum_sum_r_l ).
thf(func_def_99,type,
collect_set_l: ( set_l > $o ) > set_set_l ).
thf(func_def_100,type,
collect_set_r: ( set_r > $o ) > set_set_r ).
thf(func_def_101,type,
collect_Sum_sum_l_l: ( sum_sum_l_l > $o ) > set_Sum_sum_l_l ).
thf(func_def_102,type,
collect_Sum_sum_l_r: ( sum_sum_l_r > $o ) > set_Sum_sum_l_r ).
thf(func_def_103,type,
collect_Sum_sum_r_l: ( sum_sum_r_l > $o ) > set_Sum_sum_r_l ).
thf(func_def_104,type,
collect_l: ( l > $o ) > set_l ).
thf(func_def_105,type,
collect_r: ( r > $o ) > set_r ).
thf(func_def_106,type,
substitution_r_l_v: ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > $o ).
thf(func_def_107,type,
transi1323086383_r_l_v: set_Pr1409704485_r_l_v > set_Pr1409704485_r_l_v ).
thf(func_def_108,type,
member1522896238_r_l_v: produc1389397445_r_l_v > set_Pr1409704485_r_l_v > $o ).
thf(func_def_109,type,
member_set_l: set_l > set_set_l > $o ).
thf(func_def_110,type,
member_set_r: set_r > set_set_r > $o ).
thf(func_def_111,type,
member_l: l > set_l > $o ).
thf(func_def_112,type,
member_r: r > set_r > $o ).
thf(func_def_113,type,
e: cntxt_r_l_v ).
thf(func_def_114,type,
e2: cntxt_r_l_v ).
thf(func_def_115,type,
sigma: l > option_val_r_l_v ).
thf(func_def_116,type,
sigma2: l > option_val_r_l_v ).
thf(func_def_117,type,
tau: l > option_val_r_l_v ).
thf(func_def_118,type,
tau2: l > option_val_r_l_v ).
thf(func_def_119,type,
e3: expr_r_l_v ).
thf(func_def_120,type,
e4: expr_r_l_v ).
thf(func_def_121,type,
left_forkee: r ).
thf(func_def_122,type,
r2: r ).
thf(func_def_123,type,
r3: r ).
thf(func_def_124,type,
right_forkee: r ).
thf(func_def_125,type,
s_1: r > option1457017436_r_l_v ).
thf(func_def_126,type,
s_2: r > option1457017436_r_l_v ).
thf(func_def_127,type,
s_22: r > option1457017436_r_l_v ).
thf(func_def_128,type,
subst: expr_r_l_v > v > expr_r_l_v > expr_r_l_v ).
thf(func_def_132,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_133,type,
vOR: $o > $o > $o ).
thf(func_def_134,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_135,type,
vAND: $o > $o > $o ).
thf(func_def_136,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_137,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_138,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_139,type,
vNOT: $o > $o ).
thf(func_def_140,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_141,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_142,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_143,type,
vIMP: $o > $o > $o ).
thf(func_def_144,type,
sK0: expr_r_l_v > r > ( r > option1457017436_r_l_v ) > cntxt_r_l_v > ( l > option_val_r_l_v ) > ( r > option1457017436_r_l_v ) > ( l > option_val_r_l_v ) > r ).
thf(func_def_145,type,
sK1: ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r ).
thf(func_def_146,type,
sK2: ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r ).
thf(func_def_147,type,
sK3: set_set_l > set_l > set_l ).
thf(func_def_148,type,
sK4: ( r > option1457017436_r_l_v ) > produc1156025366_r_l_v ).
thf(func_def_149,type,
sK5: ( r > option1457017436_r_l_v ) > r ).
thf(func_def_150,type,
sK6: ( l > option_val_r_l_v ) > l ).
thf(func_def_151,type,
sK7: ( r > option1457017436_r_l_v ) > r > l > option_val_r_l_v ).
thf(func_def_152,type,
sK8: ( r > option1457017436_r_l_v ) > r > val_r_l_v ).
thf(func_def_153,type,
sK9: ( r > option1457017436_r_l_v ) > r > cntxt_r_l_v ).
thf(func_def_154,type,
sK10: ( r > option1457017436_r_l_v ) > r > l > option_val_r_l_v ).
thf(func_def_155,type,
sK11: r > ( r > option1457017436_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_156,type,
sK12: r > ( r > option1457017436_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_157,type,
sK13: set_r > set_Pr1409704485_r_l_v > ( produc1389397445_r_l_v > r > $o ) > r ).
thf(func_def_158,type,
sK14: set_r > set_Pr1409704485_r_l_v > ( produc1389397445_r_l_v > r > $o ) > produc1389397445_r_l_v ).
thf(func_def_159,type,
sK15: r > ( r > option1457017436_r_l_v ) > cntxt_r_l_v ).
thf(func_def_160,type,
sK16: r > ( r > option1457017436_r_l_v ) > val_r_l_v ).
thf(func_def_161,type,
sK17: r > ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_162,type,
sK18: r > ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_163,type,
sK19: produc1389397445_r_l_v > ( produc1389397445_r_l_v > option_val_r_l_v ) > val_r_l_v ).
thf(func_def_164,type,
sK20: set_Pr1409704485_r_l_v > produc1389397445_r_l_v ).
thf(func_def_165,type,
sK21: r > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_166,type,
sK22: r > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_167,type,
sK23: expr_r_l_v > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_168,type,
sK24: r > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_169,type,
sK25: r > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_170,type,
sK26: ( r > option1457017436_r_l_v ) > l ).
thf(func_def_171,type,
sK27: option_val_r_l_v > val_r_l_v ).
thf(func_def_172,type,
sK28: r > ( r > option_val_r_l_v ) > val_r_l_v ).
thf(func_def_173,type,
sK29: set_l > set_set_l > set_l ).
thf(func_def_174,type,
sK30: ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > ( r > option1457017436_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_175,type,
sK31: ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > ( r > option1457017436_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_176,type,
sK32: r > ( r > option1457017436_r_l_v ) > produc1156025366_r_l_v ).
thf(func_def_177,type,
sK33: option_val_r_l_v > val_r_l_v ).
thf(func_def_178,type,
sK34: ( r > option1457017436_r_l_v ) > r > expr_r_l_v ).
thf(func_def_179,type,
sK35: ( r > option1457017436_r_l_v ) > r > l > option_val_r_l_v ).
thf(func_def_180,type,
sK36: ( r > option1457017436_r_l_v ) > r > l > option_val_r_l_v ).
thf(func_def_181,type,
sK37: ( r > option1457017436_r_l_v ) > r > cntxt_r_l_v ).
thf(func_def_182,type,
sK38: option_val_r_l_v > ( ( l > option_val_r_l_v ) > $o ) > l ).
thf(func_def_183,type,
sK39: option_val_r_l_v > ( ( l > option_val_r_l_v ) > $o ) > l > option_val_r_l_v ).
thf(func_def_184,type,
sK40: option_val_r_l_v > ( ( l > option_val_r_l_v ) > $o ) > option_val_r_l_v ).
thf(func_def_185,type,
sK41: ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > r > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_186,type,
sK42: ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > r > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_187,type,
sK43: r > ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_188,type,
sK44: r > ( r > option1457017436_r_l_v ) > cntxt_r_l_v ).
thf(func_def_189,type,
sK45: r > ( r > option1457017436_r_l_v ) > expr_r_l_v ).
thf(func_def_190,type,
sK46: r > ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_191,type,
sK47: ( produc1389397445_r_l_v > option1457017436_r_l_v ) > produc1389397445_r_l_v > produc1156025366_r_l_v ).
thf(func_def_192,type,
sK48: ( r > option1457017436_r_l_v ) > r > ( r > option1457017436_r_l_v ) > val_r_l_v > cntxt_r_l_v > ( l > option_val_r_l_v ) > ( l > option_val_r_l_v ) > l ).
thf(func_def_193,type,
sK49: set_r > set_set_r > set_r ).
thf(func_def_194,type,
sK50: ( produc1156025366_r_l_v > $o ) > l > option_val_r_l_v ).
thf(func_def_195,type,
sK51: ( produc1156025366_r_l_v > $o ) > expr_r_l_v ).
thf(func_def_196,type,
sK52: ( produc1156025366_r_l_v > $o ) > l > option_val_r_l_v ).
thf(func_def_197,type,
sK53: set_l > l ).
thf(func_def_198,type,
sK54: ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > ( r > option1457017436_r_l_v ) > expr_r_l_v > r > option1457017436_r_l_v ).
thf(func_def_199,type,
sK55: option1457017436_r_l_v > produc1156025366_r_l_v ).
thf(func_def_200,type,
sK56: r > ( r > option1457017436_r_l_v ) > cntxt_r_l_v ).
thf(func_def_201,type,
sK57: r > ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_202,type,
sK58: r > ( r > option1457017436_r_l_v ) > val_r_l_v ).
thf(func_def_203,type,
sK59: r > ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_204,type,
sK60: ( r > option1457017436_r_l_v ) > r ).
thf(func_def_205,type,
sK61: ( r > option1457017436_r_l_v ) > expr_r_l_v ).
thf(func_def_206,type,
sK62: ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_207,type,
sK63: ( r > option1457017436_r_l_v ) > r ).
thf(func_def_208,type,
sK64: ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_209,type,
sK65: ( r > option1457017436_r_l_v ) > expr_r_l_v ).
thf(func_def_210,type,
sK66: ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_211,type,
sK67: ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_212,type,
sK68: ( produc1389397445_r_l_v > $o ) > ( produc1389397445_r_l_v > $o ) > produc1389397445_r_l_v ).
thf(func_def_213,type,
sK69: ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_214,type,
sK70: ( r > option1457017436_r_l_v ) > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_215,type,
sK71: ( option_val_r_l_v > $o ) > val_r_l_v ).
thf(func_def_216,type,
sK72: r > ( r > option1457017436_r_l_v ) > val_r_l_v ).
thf(func_def_217,type,
sK73: r > ( r > option1457017436_r_l_v ) > cntxt_r_l_v ).
thf(func_def_218,type,
sK74: r > ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_219,type,
sK75: r > ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_220,type,
sK76: ( set_l > $o ) > ( set_l > $o ) > set_l ).
thf(func_def_221,type,
sK77: ( set_r > $o ) > ( set_r > $o ) > set_r ).
thf(func_def_222,type,
sK78: ( option1457017436_r_l_v > $o ) > produc1156025366_r_l_v ).
thf(func_def_223,type,
sK79: ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_224,type,
sK80: ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_225,type,
sK81: ( l > option1457017436_r_l_v ) > l ).
thf(func_def_226,type,
sK82: r > ( r > option1457017436_r_l_v ) > cntxt_r_l_v ).
thf(func_def_227,type,
sK83: r > ( r > option1457017436_r_l_v ) > expr_r_l_v ).
thf(func_def_228,type,
sK84: r > ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_229,type,
sK85: r > ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_230,type,
sK86: ( r > option1457017436_r_l_v ) > r ).
thf(func_def_231,type,
sK87: ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_232,type,
sK88: ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_233,type,
sK89: ( r > option1457017436_r_l_v ) > expr_r_l_v ).
thf(func_def_234,type,
sK90: ( r > option1457017436_r_l_v ) > expr_r_l_v ).
thf(func_def_235,type,
sK91: ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_236,type,
sK92: ( r > option1457017436_r_l_v ) > r ).
thf(func_def_237,type,
sK93: ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_238,type,
sK94: r > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_239,type,
sK95: r > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_240,type,
sK96: ( r > option1457017436_r_l_v ) > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_241,type,
sK97: ( r > option1457017436_r_l_v ) > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_242,type,
sK98: ( l > r > $o ) > set_r > set_l > l ).
thf(func_def_243,type,
sK99: ( l > r > $o ) > set_r > set_l > r ).
thf(func_def_244,type,
sK100: ( r > option1457017436_r_l_v ) > r > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_245,type,
sK101: ( r > option1457017436_r_l_v ) > r > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_246,type,
sK102: option_val_r_l_v > option_val_r_l_v > ( option_val_r_l_v > option_val_r_l_v > $o ) > val_r_l_v ).
thf(func_def_247,type,
sK103: option_val_r_l_v > option_val_r_l_v > ( option_val_r_l_v > option_val_r_l_v > $o ) > val_r_l_v ).
thf(func_def_248,type,
sK104: ( option1457017436_r_l_v > option_val_r_l_v > $o ) > option1457017436_r_l_v > option_val_r_l_v > val_r_l_v ).
thf(func_def_249,type,
sK105: ( option1457017436_r_l_v > option_val_r_l_v > $o ) > option1457017436_r_l_v > option_val_r_l_v > produc1156025366_r_l_v ).
thf(func_def_250,type,
sK106: option1457017436_r_l_v > produc1156025366_r_l_v ).
thf(func_def_251,type,
sK107: ( produc1389397445_r_l_v > l > $o ) > set_Pr1409704485_r_l_v > set_l > l ).
thf(func_def_252,type,
sK108: ( produc1389397445_r_l_v > l > $o ) > set_Pr1409704485_r_l_v > set_l > produc1389397445_r_l_v ).
thf(func_def_253,type,
sK109: set_r > r ).
thf(func_def_254,type,
sK110: ( r > option1457017436_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_255,type,
sK111: ( r > option1457017436_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_256,type,
sK112: option1457017436_r_l_v > option1457017436_r_l_v > ( option1457017436_r_l_v > option1457017436_r_l_v > $o ) > produc1156025366_r_l_v ).
thf(func_def_257,type,
sK113: option1457017436_r_l_v > option1457017436_r_l_v > ( option1457017436_r_l_v > option1457017436_r_l_v > $o ) > produc1156025366_r_l_v ).
thf(func_def_258,type,
sK114: set_r > set_set_r > set_r ).
thf(func_def_259,type,
sK115: r > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_260,type,
sK116: r > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_261,type,
sK117: ( l > $o ) > ( l > $o ) > l ).
thf(func_def_262,type,
sK118: ( r > $o ) > r ).
thf(func_def_263,type,
sK119: ( r > $o ) > ( r > $o ) > r ).
thf(func_def_264,type,
sK120: ( l > option_val_r_l_v ) > l > val_r_l_v ).
thf(func_def_265,type,
sK121: cntxt_r_l_v > r > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > expr_r_l_v > ( l > option_val_r_l_v ) > ( l > option_val_r_l_v ) > r ).
thf(func_def_266,type,
sK122: r > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_267,type,
sK123: r > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_268,type,
sK124: ( ( r > option1457017436_r_l_v ) > $o ) > option1457017436_r_l_v > r > option1457017436_r_l_v ).
thf(func_def_269,type,
sK125: ( ( r > option1457017436_r_l_v ) > $o ) > option1457017436_r_l_v > option1457017436_r_l_v ).
thf(func_def_270,type,
sK126: ( ( r > option1457017436_r_l_v ) > $o ) > option1457017436_r_l_v > r ).
thf(func_def_271,type,
sK127: ( r > option1457017436_r_l_v ) > r ).
thf(func_def_272,type,
sK128: l > ( r > option1457017436_r_l_v ) > r ).
thf(func_def_273,type,
sK129: l > ( r > option1457017436_r_l_v ) > produc1156025366_r_l_v ).
thf(func_def_274,type,
sK130: ( r > option1457017436_r_l_v ) > expr_r_l_v ).
thf(func_def_275,type,
sK131: ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_276,type,
sK132: ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_277,type,
sK133: ( r > option1457017436_r_l_v ) > r ).
thf(func_def_278,type,
sK134: r > r > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_279,type,
sK135: r > r > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_280,type,
sK136: r > ( r > option1457017436_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_281,type,
sK137: r > ( r > option1457017436_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_282,type,
sK138: ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_283,type,
sK139: ( r > option1457017436_r_l_v ) > expr_r_l_v ).
thf(func_def_284,type,
sK140: ( r > option1457017436_r_l_v ) > r > r > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_285,type,
sK141: ( r > option1457017436_r_l_v ) > r > r > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_286,type,
sK142: ( l > $o ) > l ).
thf(func_def_287,type,
sK143: option1457017436_r_l_v > produc1156025366_r_l_v ).
thf(func_def_288,type,
sK144: produc1156025366_r_l_v > l > option_val_r_l_v ).
thf(func_def_289,type,
sK145: produc1156025366_r_l_v > l > option_val_r_l_v ).
thf(func_def_290,type,
sK146: produc1156025366_r_l_v > expr_r_l_v ).
thf(func_def_291,type,
sK147: l > ( l > option1457017436_r_l_v ) > produc1156025366_r_l_v ).
thf(func_def_292,type,
sK148: r > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_293,type,
sK149: r > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_294,type,
sK150: option_val_r_l_v > val_r_l_v ).
thf(func_def_295,type,
sK151: ( r > option1457017436_r_l_v ) > l ).
thf(func_def_296,type,
sK152: ( r > option1457017436_r_l_v ) > r ).
thf(func_def_297,type,
sK153: r > ( r > option1457017436_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_298,type,
sK154: r > ( r > option1457017436_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_299,type,
sK155: ( r > option1457017436_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_300,type,
sK156: ( r > option1457017436_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_301,type,
sK157: r > cntxt_r_l_v > ( l > option_val_r_l_v ) > ( l > option_val_r_l_v ) > ( r > option1457017436_r_l_v ) > val_r_l_v > ( r > option1457017436_r_l_v ) > l ).
thf(func_def_302,type,
sK158: ( r > option_val_r_l_v ) > r ).
thf(func_def_303,type,
sK159: ( r > option1457017436_r_l_v ) > r > r > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_304,type,
sK160: ( r > option1457017436_r_l_v ) > r > r > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_305,type,
sK161: ( r > option1457017436_r_l_v ) > expr_r_l_v ).
thf(func_def_306,type,
sK162: ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_307,type,
sK163: ( r > option1457017436_r_l_v ) > r ).
thf(func_def_308,type,
sK164: ( r > option1457017436_r_l_v ) > l > option_val_r_l_v ).
thf(func_def_309,type,
sK165: set_l > ( r > l > $o ) > set_r > l ).
thf(func_def_310,type,
sK166: set_l > ( r > l > $o ) > set_r > r ).
thf(func_def_311,type,
sK167: set_l > set_l > ( l > l > $o ) > l ).
thf(func_def_312,type,
sK168: set_l > set_l > ( l > l > $o ) > l ).
thf(func_def_313,type,
sK169: ( r > option1457017436_r_l_v ) > r > cntxt_r_l_v ).
thf(func_def_314,type,
sK170: ( r > option1457017436_r_l_v ) > r > expr_r_l_v ).
thf(func_def_315,type,
sK171: ( r > option1457017436_r_l_v ) > r > l > option_val_r_l_v ).
thf(func_def_316,type,
sK172: ( r > option1457017436_r_l_v ) > r > l > option_val_r_l_v ).
thf(func_def_317,type,
sK173: r > r > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_318,type,
sK174: r > r > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_319,type,
sK175: set_r > set_r > ( r > r > $o ) > r ).
thf(func_def_320,type,
sK176: set_r > set_r > ( r > r > $o ) > r ).
thf(func_def_321,type,
sK177: ( r > option1457017436_r_l_v ) > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > expr_r_l_v ).
thf(func_def_322,type,
sK178: ( r > option1457017436_r_l_v ) > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > r > option1457017436_r_l_v ).
thf(func_def_323,type,
sK179: ( r > option1457017436_r_l_v ) > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_324,type,
sK180: ( r > option1457017436_r_l_v ) > ( expr_r_l_v > v > expr_r_l_v > expr_r_l_v ) > r > ( r > option1457017436_r_l_v ) > r > r > option1457017436_r_l_v ).
thf(func_def_325,type,
sK181: option_val_r_l_v > option1457017436_r_l_v > ( option_val_r_l_v > option1457017436_r_l_v > $o ) > produc1156025366_r_l_v ).
thf(func_def_326,type,
sK182: option_val_r_l_v > option1457017436_r_l_v > ( option_val_r_l_v > option1457017436_r_l_v > $o ) > val_r_l_v ).
thf(func_def_327,type,
sK183: ( r > option1457017436_r_l_v ) > r ).
thf(func_def_329,type,
sK185: r > option1457017436_r_l_v > ( r > option1457017436_r_l_v ) > option1457017436_r_l_v > ( r > option1457017436_r_l_v ) > r ).
thf(func_def_330,type,
sK186: option1457017436_r_l_v > ( r > option1457017436_r_l_v ) > r ).
thf(func_def_331,type,
sK187: ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > r > produc1156025366_r_l_v > produc1156025366_r_l_v > r ).
thf(func_def_332,type,
sK188: produc1156025366_r_l_v > ( r > option1457017436_r_l_v ) > r ).
thf(func_def_333,type,
sK189: option1457017436_r_l_v > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > option1457017436_r_l_v > option1457017436_r_l_v > r ).
thf(func_def_334,type,
sK190: option1457017436_r_l_v > ( r > option1457017436_r_l_v ) > ( r > option1457017436_r_l_v ) > option1457017436_r_l_v > option1457017436_r_l_v > r ).
thf(f1,axiom,
~ ( member_r @ right_forkee @ ( rID_G_r_l_v @ s_1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_local_Ofork_I3_J) ).
thf(f7,axiom,
( ( s_1 @ r3 )
= ( some_P1807977723_r_l_v @ ( produc297528454_r_l_v @ sigma2 @ ( produc1834103605_r_l_v @ tau2 @ ( plug_r_l_v @ e2 @ ( rfork_r_l_v @ e4 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_6_local_Ofork_I2_J) ).
thf(f25,axiom,
! [X2: produc1156025366_r_l_v,X1: r,X0: r > option1457017436_r_l_v] :
( ( ( X0 @ X1 )
= ( some_P1807977723_r_l_v @ X2 ) )
=> ( member_r @ X1 @ ( rID_G_r_l_v @ X0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_24_RID_092_060_094sub_062GI_I1_J) ).
thf(f358,conjecture,
r3 != right_forkee,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
thf(f359,negated_conjecture,
~ ( ( r3 != right_forkee ) ),
inference(negated_conjecture,[status(cth)],[f358]) ).
thf(f745,plain,
~ ( member_r @ right_forkee @ ( rID_G_r_l_v @ s_1 ) ),
inference(rectify,[],[f1]) ).
thf(f746,plain,
( ( member_r @ right_forkee @ ( rID_G_r_l_v @ s_1 ) )
!= $true ),
inference(fool_elimination,[],[f745]) ).
thf(f834,plain,
! [X0: produc1156025366_r_l_v,X1: r,X2: r > option1457017436_r_l_v] :
( ( ( some_P1807977723_r_l_v @ X0 )
= ( X2 @ X1 ) )
=> ( member_r @ X1 @ ( rID_G_r_l_v @ X2 ) ) ),
inference(rectify,[],[f25]) ).
thf(f835,plain,
! [X2: r > option1457017436_r_l_v,X0: produc1156025366_r_l_v,X1: r] :
( ( ( some_P1807977723_r_l_v @ X0 )
= ( X2 @ X1 ) )
=> ( ( member_r @ X1 @ ( rID_G_r_l_v @ X2 ) )
= $true ) ),
inference(fool_elimination,[],[f834]) ).
thf(f971,plain,
( ( member_r @ right_forkee @ ( rID_G_r_l_v @ s_1 ) )
!= $true ),
inference(flattening,[],[f746]) ).
thf(f983,plain,
right_forkee = r3,
inference(flattening,[],[f359]) ).
thf(f1150,plain,
! [X0: produc1156025366_r_l_v,X2: r > option1457017436_r_l_v,X1: r] :
( ( ( some_P1807977723_r_l_v @ X0 )
!= ( X2 @ X1 ) )
| ( ( member_r @ X1 @ ( rID_G_r_l_v @ X2 ) )
= $true ) ),
inference(ennf_transformation,[],[f835]) ).
thf(f1360,plain,
! [X0: produc1156025366_r_l_v,X1: r > option1457017436_r_l_v,X2: r] :
( ( ( some_P1807977723_r_l_v @ X0 )
!= ( X1 @ X2 ) )
| ( ( member_r @ X2 @ ( rID_G_r_l_v @ X1 ) )
= $true ) ),
inference(rectify,[],[f1150]) ).
thf(f1746,plain,
! [X2: r,X0: produc1156025366_r_l_v,X1: r > option1457017436_r_l_v] :
( ( ( some_P1807977723_r_l_v @ X0 )
!= ( X1 @ X2 ) )
| ( ( member_r @ X2 @ ( rID_G_r_l_v @ X1 ) )
= $true ) ),
inference(cnf_transformation,[],[f1360]) ).
thf(f1784,plain,
right_forkee = r3,
inference(cnf_transformation,[],[f983]) ).
thf(f2099,plain,
( ( s_1 @ r3 )
= ( some_P1807977723_r_l_v @ ( produc297528454_r_l_v @ sigma2 @ ( produc1834103605_r_l_v @ tau2 @ ( plug_r_l_v @ e2 @ ( rfork_r_l_v @ e4 ) ) ) ) ) ),
inference(cnf_transformation,[],[f7]) ).
thf(f2140,plain,
( ( member_r @ right_forkee @ ( rID_G_r_l_v @ s_1 ) )
!= $true ),
inference(cnf_transformation,[],[f971]) ).
thf(f2610,definition,
( spl184_12
<=> ( ( s_1 @ r3 )
= ( some_P1807977723_r_l_v @ ( produc297528454_r_l_v @ sigma2 @ ( produc1834103605_r_l_v @ tau2 @ ( plug_r_l_v @ e2 @ ( rfork_r_l_v @ e4 ) ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl184_12])],[avatar_definition]) ).
thf(f2612,plain,
( ( ( s_1 @ r3 )
= ( some_P1807977723_r_l_v @ ( produc297528454_r_l_v @ sigma2 @ ( produc1834103605_r_l_v @ tau2 @ ( plug_r_l_v @ e2 @ ( rfork_r_l_v @ e4 ) ) ) ) ) )
| ~ spl184_12 ),
inference(avatar_component_clause,[],[f2610]) ).
thf(f2613,plain,
spl184_12,
inference(avatar_split_clause,[],[f2099,f2610]) ).
thf(f2868,definition,
( spl184_65
<=> ( right_forkee = r3 ) ),
introduced(definition,[new_symbols(definition,[spl184_65])],[avatar_definition]) ).
thf(f2870,plain,
( ( right_forkee = r3 )
| ~ spl184_65 ),
inference(avatar_component_clause,[],[f2868]) ).
thf(f2871,plain,
spl184_65,
inference(avatar_split_clause,[],[f1784,f2868]) ).
thf(f2873,definition,
( spl184_66
<=> ( ( member_r @ right_forkee @ ( rID_G_r_l_v @ s_1 ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl184_66])],[avatar_definition]) ).
thf(f2875,plain,
( ( ( member_r @ right_forkee @ ( rID_G_r_l_v @ s_1 ) )
!= $true )
| spl184_66 ),
inference(avatar_component_clause,[],[f2873]) ).
thf(f2876,plain,
~ spl184_66,
inference(avatar_split_clause,[],[f2140,f2873]) ).
thf(f3022,plain,
( ( ( member_r @ r3 @ ( rID_G_r_l_v @ s_1 ) )
!= $true )
| ~ spl184_65
| spl184_66 ),
inference(forward_demodulation,[],[f2875,f2870]) ).
thf(f3024,definition,
( spl184_94
<=> ( ( member_r @ r3 @ ( rID_G_r_l_v @ s_1 ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl184_94])],[avatar_definition]) ).
thf(f3026,plain,
( ( ( member_r @ r3 @ ( rID_G_r_l_v @ s_1 ) )
!= $true )
| spl184_94 ),
inference(avatar_component_clause,[],[f3024]) ).
thf(f3027,plain,
( ~ spl184_94
| ~ spl184_65
| spl184_66 ),
inference(avatar_split_clause,[],[f3022,f2873,f2868,f3024]) ).
thf(f3837,plain,
( ( ( member_r @ r3 @ ( rID_G_r_l_v @ s_1 ) )
= $true )
| ~ spl184_12 ),
inference(unit_resulting_resolution,[],[f1746,f2612]) ).
thf(f3879,plain,
( $false
| ~ spl184_12
| spl184_94 ),
inference(forward_subsumption_resolution,[],[f3837,f3026]) ).
thf(f3880,plain,
( ~ spl184_12
| spl184_94 ),
inference(avatar_contradiction_clause,[],[f3879]) ).
cnf(s8,plain,
spl184_12,
inference(sat_conversion,[],[f2613]) ).
cnf(s75,plain,
spl184_65,
inference(sat_conversion,[],[f2871]) ).
cnf(s76,plain,
~ spl184_66,
inference(sat_conversion,[],[f2876]) ).
cnf(s120,plain,
( ~ spl184_65
| spl184_66
| ~ spl184_94 ),
inference(sat_conversion,[],[f3027]) ).
cnf(s164,plain,
( ~ spl184_12
| spl184_94 ),
inference(sat_conversion,[],[f3880]) ).
cnf(s172,plain,
~ spl184_94,
inference(rat,[],[s120,s76,s75]) ).
cnf(s174,plain,
~ spl184_12,
inference(rat,[],[s164,s172]) ).
cnf(s207,plain,
$false,
inference(rat,[],[s8,s174]) ).
thf(f3896,plain,
$false,
inference(avatar_sat_refutation,[],[s207]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP046^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.20 % Computer : n020.cluster.edu
% 0.12/0.20 % Model : x86_64 x86_64
% 0.12/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.20 % Memory : 8046.5625MB
% 0.12/0.20 % OS : Linux 6.8.0-71-generic
% 0.12/0.20 % CPULimit : 300
% 0.12/0.20 % WCLimit : 300
% 0.12/0.20 % DateTime : Tue Sep 29 19:42:50 UTC 2026
% 0.12/0.21 % CPUTime :
% 0.12/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.24 Running higher-order theorem proving
% 0.36/0.39 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.85/0.60 % (1496359)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.85/0.60 % (1496371)lrs+10_16_si=on:nwc=1.5:random_seed=1458002778:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.85/0.60 % (1496370)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=4111682064:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.85/0.60 % (1496371)Instruction limit reached!
% 0.85/0.60 % (1496371)------------------------------
% 0.85/0.60 % (1496371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.60 % (1496371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.60 % (1496371)CaDiCaL version: 2.1.3
% 0.85/0.60 % (1496371)Termination reason: Instruction limit
% 0.85/0.60 % (1496371)Termination phase: shuffling
% 0.85/0.60 % (1496371)Time elapsed: 0.008 s
% 0.85/0.60 % (1496371)Peak memory usage: 10 MB
% 0.85/0.60 % (1496371)Instructions burned: 19 (million)
% 0.85/0.60 % (1496376)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.85/0.60 % (1496376)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.85/0.60 % (1496372)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3446302248:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.85/0.60 % (1496374)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1185644884:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.85/0.60 % (1496373)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=310341260:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.85/0.60 % (1496376)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=232813298:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.85/0.60 % (1496372)Instruction limit reached!
% 0.85/0.60 % (1496372)------------------------------
% 0.85/0.60 % (1496372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.60 % (1496372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.60 % (1496372)CaDiCaL version: 2.1.3
% 0.85/0.60 % (1496372)Termination reason: Instruction limit
% 0.85/0.60 % (1496372)Termination phase: shuffling
% 0.85/0.60 % (1496372)Time elapsed: 0.004 s
% 0.85/0.60 % (1496372)Peak memory usage: 10 MB
% 0.85/0.60 % (1496372)Instructions burned: 4 (million)
% 0.85/0.60 % (1496375)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1886041464:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.85/0.60 % (1496381)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=973895032:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.85/0.60 % (1496381)Instruction limit reached!
% 0.85/0.60 % (1496381)------------------------------
% 0.85/0.60 % (1496381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.60 % (1496381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.60 % (1496381)CaDiCaL version: 2.1.3
% 0.85/0.60 % (1496381)Termination reason: Instruction limit
% 0.85/0.60 % (1496381)Termination phase: shuffling
% 0.85/0.60 % (1496381)Time elapsed: 0.002 s
% 0.85/0.60 % (1496381)Peak memory usage: 10 MB
% 0.85/0.60 % (1496381)Instructions burned: 2 (million)
% 0.85/0.60 % (1496374)Instruction limit reached!
% 0.85/0.60 % (1496374)------------------------------
% 0.85/0.60 % (1496374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.60 % (1496374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.60 % (1496374)CaDiCaL version: 2.1.3
% 0.85/0.60 % (1496374)Termination reason: Instruction limit
% 0.85/0.60 % (1496374)Termination phase: shuffling
% 0.85/0.60 % (1496374)Time elapsed: 0.021 s
% 0.85/0.60 % (1496374)Peak memory usage: 10 MB
% 0.85/0.60 % (1496374)Instructions burned: 25 (million)
% 0.85/0.60 % (1496386)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3104155729:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.55/0.66 % (1496386)Instruction limit reached!
% 1.55/0.66 % (1496386)------------------------------
% 1.55/0.66 % (1496386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.66 % (1496386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.66 % (1496386)CaDiCaL version: 2.1.3
% 1.55/0.66 % (1496386)Termination reason: Instruction limit
% 1.55/0.66 % (1496386)Termination phase: shuffling
% 1.55/0.66 % (1496386)Time elapsed: 0.003 s
% 1.55/0.66 % (1496386)Peak memory usage: 11 MB
% 1.55/0.66 % (1496386)Instructions burned: 7 (million)
% 1.55/0.66 % (1496390)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.55/0.66 % (1496390)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2623017620:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.55/0.66 % (1496394)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.55/0.66 % (1496394)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.55/0.66 % (1496390)Instruction limit reached!
% 1.55/0.66 % (1496390)------------------------------
% 1.55/0.66 % (1496390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.66 % (1496390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.66 % (1496390)CaDiCaL version: 2.1.3
% 1.55/0.66 % (1496390)Termination reason: Instruction limit
% 1.55/0.66 % (1496390)Termination phase: shuffling
% 1.55/0.66 % (1496390)Time elapsed: 0.004 s
% 1.55/0.66 % (1496390)Peak memory usage: 10 MB
% 1.55/0.66 % (1496390)Instructions burned: 8 (million)
% 1.55/0.66 % (1496394)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1847752885:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.55/0.66 % (1496391)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2898768032:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.55/0.66 % (1496370)Instruction limit reached!
% 1.55/0.66 % (1496370)------------------------------
% 1.55/0.66 % (1496370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.66 % (1496370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.66 % (1496370)CaDiCaL version: 2.1.3
% 1.55/0.66 % (1496370)Termination reason: Instruction limit
% 1.55/0.66 % (1496370)Termination phase: Preprocessing 1
% 1.55/0.66 % (1496370)Time elapsed: 0.068 s
% 1.55/0.66 % (1496370)Peak memory usage: 12 MB
% 1.55/0.66 % (1496370)Instructions burned: 88 (million)
% 1.55/0.66 % (1496394)Instruction limit reached!
% 1.55/0.66 % (1496394)------------------------------
% 1.55/0.66 % (1496394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.66 % (1496394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.66 % (1496394)CaDiCaL version: 2.1.3
% 1.55/0.66 % (1496394)Termination reason: Instruction limit
% 1.55/0.66 % (1496394)Termination phase: shuffling
% 1.55/0.66 % (1496394)Time elapsed: 0.014 s
% 1.55/0.66 % (1496394)Peak memory usage: 11 MB
% 1.55/0.66 % (1496394)Instructions burned: 29 (million)
% 1.55/0.66 % (1496391)Instruction limit reached!
% 1.55/0.66 % (1496391)------------------------------
% 1.55/0.66 % (1496391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.55/0.66 % (1496391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.55/0.66 % (1496391)CaDiCaL version: 2.1.3
% 1.55/0.66 % (1496391)Termination reason: Instruction limit
% 1.55/0.66 % (1496391)Termination phase: shuffling
% 1.55/0.66 % (1496391)Time elapsed: 0.010 s
% 1.55/0.66 % (1496391)Peak memory usage: 10 MB
% 1.55/0.66 % (1496391)Instructions burned: 12 (million)
% 1.55/0.66 % (1496396)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=1628574177:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi)
% 1.55/0.66 % (1496375)Instruction limit reached!
% 1.55/0.66 % (1496375)------------------------------
% 1.55/0.66 % (1496375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.71 % (1496375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.71 % (1496375)CaDiCaL version: 2.1.3
% 1.97/0.71 % (1496375)Termination reason: Instruction limit
% 1.97/0.71 % (1496375)Termination phase: Property scanning
% 1.97/0.71 % (1496375)Time elapsed: 0.061 s
% 1.97/0.71 % (1496375)Peak memory usage: 11 MB
% 1.97/0.71 % (1496375)Instructions burned: 76 (million)
% 1.97/0.71 % (1496401)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.97/0.71 % (1496401)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=1281854174:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.97/0.71 % (1496401)Instruction limit reached!
% 1.97/0.71 % (1496401)------------------------------
% 1.97/0.71 % (1496401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.71 % (1496401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.71 % (1496401)CaDiCaL version: 2.1.3
% 1.97/0.71 % (1496401)Termination reason: Instruction limit
% 1.97/0.71 % (1496401)Termination phase: shuffling
% 1.97/0.71 % (1496401)Time elapsed: 0.002 s
% 1.97/0.71 % (1496401)Peak memory usage: 10 MB
% 1.97/0.71 % (1496401)Instructions burned: 3 (million)
% 1.97/0.71 % (1496399)lrs+10_1_si=on:cs=on:random_seed=899565467:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.97/0.71 % (1496403)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=297206168:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.97/0.71 % (1496399)Instruction limit reached!
% 1.97/0.71 % (1496399)------------------------------
% 1.97/0.71 % (1496399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.71 % (1496399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.71 % (1496399)CaDiCaL version: 2.1.3
% 1.97/0.71 % (1496399)Termination reason: Instruction limit
% 1.97/0.71 % (1496399)Termination phase: shuffling
% 1.97/0.71 % (1496399)Time elapsed: 0.010 s
% 1.97/0.71 % (1496399)Peak memory usage: 10 MB
% 1.97/0.71 % (1496399)Instructions burned: 11 (million)
% 1.97/0.71 % (1496407)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2914176398:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.97/0.71 % (1496405)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2206100939:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.97/0.71 % (1496396)Instruction limit reached!
% 1.97/0.71 % (1496396)------------------------------
% 1.97/0.71 % (1496396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.71 % (1496396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.71 % (1496396)CaDiCaL version: 2.1.3
% 1.97/0.71 % (1496396)Termination reason: Instruction limit
% 1.97/0.71 % (1496396)Termination phase: Property scanning
% 1.97/0.71 % (1496396)Time elapsed: 0.043 s
% 1.97/0.71 % (1496396)Peak memory usage: 12 MB
% 1.97/0.71 % (1496396)Instructions burned: 88 (million)
% 1.97/0.71 % (1496407)Instruction limit reached!
% 1.97/0.71 % (1496407)------------------------------
% 1.97/0.71 % (1496407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.71 % (1496407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.71 % (1496407)CaDiCaL version: 2.1.3
% 1.97/0.71 % (1496407)Termination reason: Instruction limit
% 1.97/0.71 % (1496407)Termination phase: shuffling
% 1.97/0.71 % (1496407)Time elapsed: 0.011 s
% 1.97/0.71 % (1496407)Peak memory usage: 10 MB
% 1.97/0.71 % (1496407)Instructions burned: 26 (million)
% 1.97/0.71 % (1496376)Instruction limit reached!
% 1.97/0.71 % (1496376)------------------------------
% 1.97/0.71 % (1496376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.71 % (1496376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.71 % (1496376)CaDiCaL version: 2.1.3
% 1.97/0.71 % (1496376)Termination reason: Instruction limit
% 1.97/0.71 % (1496376)Termination phase: Function definition elimination
% 1.97/0.71 % (1496376)Time elapsed: 0.129 s
% 1.97/0.71 % (1496376)Peak memory usage: 13 MB
% 1.97/0.71 % (1496376)Instructions burned: 157 (million)
% 1.97/0.71 % (1496403)Instruction limit reached!
% 1.97/0.71 % (1496403)------------------------------
% 1.97/0.77 % (1496403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.77 % (1496403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.77 % (1496403)CaDiCaL version: 2.1.3
% 1.97/0.77 % (1496403)Termination reason: Instruction limit
% 1.97/0.77 % (1496403)Termination phase: shuffling
% 1.97/0.77 % (1496403)Time elapsed: 0.032 s
% 1.97/0.77 % (1496403)Peak memory usage: 10 MB
% 1.97/0.77 % (1496403)Instructions burned: 38 (million)
% 1.97/0.77 % (1496414)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=647035970:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.97/0.77 % (1496411)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3792830006:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.97/0.77 % (1496415)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=922406352:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.97/0.77 % (1496411)Instruction limit reached!
% 1.97/0.77 % (1496411)------------------------------
% 1.97/0.77 % (1496411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.77 % (1496411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.77 % (1496411)CaDiCaL version: 2.1.3
% 1.97/0.77 % (1496411)Termination reason: Instruction limit
% 1.97/0.77 % (1496411)Termination phase: shuffling
% 1.97/0.77 % (1496411)Time elapsed: 0.012 s
% 1.97/0.77 % (1496411)Peak memory usage: 10 MB
% 1.97/0.77 % (1496411)Instructions burned: 14 (million)
% 1.97/0.77 % (1496415)Instruction limit reached!
% 1.97/0.77 % (1496415)------------------------------
% 1.97/0.77 % (1496415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.77 % (1496415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.77 % (1496415)CaDiCaL version: 2.1.3
% 1.97/0.77 % (1496415)Termination reason: Instruction limit
% 1.97/0.77 % (1496415)Termination phase: shuffling
% 1.97/0.77 % (1496415)Time elapsed: 0.008 s
% 1.97/0.77 % (1496415)Peak memory usage: 10 MB
% 1.97/0.77 % (1496415)Instructions burned: 14 (million)
% 1.97/0.77 % (1496418)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=290676035:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.97/0.77 % (1496419)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2532840717:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.97/0.77 % (1496418)Instruction limit reached!
% 1.97/0.77 % (1496418)------------------------------
% 1.97/0.77 % (1496418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.77 % (1496418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.77 % (1496418)CaDiCaL version: 2.1.3
% 1.97/0.77 % (1496418)Termination reason: Instruction limit
% 1.97/0.77 % (1496418)Termination phase: shuffling
% 1.97/0.77 % (1496418)Time elapsed: 0.003 s
% 1.97/0.77 % (1496418)Peak memory usage: 10 MB
% 1.97/0.77 % (1496418)Instructions burned: 3 (million)
% 1.97/0.77 % (1496423)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1405966507:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 1.97/0.77 % (1496422)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1173960953:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 1.97/0.77 % (1496405)Refutation not found, incomplete strategy
% 1.97/0.77 % (1496405)------------------------------
% 1.97/0.77 % (1496405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.77 % (1496405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.77 % (1496405)CaDiCaL version: 2.1.3
% 1.97/0.77 % (1496405)Termination reason: Refutation not found, incomplete strategy
% 1.97/0.77 % (1496405)Time elapsed: 0.076 s
% 1.97/0.77 % (1496405)Peak memory usage: 13 MB
% 1.97/0.77 % (1496405)Instructions burned: 91 (million)
% 1.97/0.77 % (1496419)Instruction limit reached!
% 1.97/0.77 % (1496419)------------------------------
% 1.97/0.77 % (1496419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.97/0.77 % (1496419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.97/0.77 % (1496419)CaDiCaL version: 2.1.3
% 2.60/0.89 % (1496419)Termination reason: Instruction limit
% 2.60/0.89 % (1496419)Termination phase: shuffling
% 2.60/0.89 % (1496419)Time elapsed: 0.023 s
% 2.60/0.89 % (1496419)Peak memory usage: 10 MB
% 2.60/0.89 % (1496419)Instructions burned: 27 (million)
% 2.60/0.89 % (1496405)------------------------------
% 2.60/0.89 % (1496405)------------------------------
% 2.60/0.89 % (1496428)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 2.60/0.89 % (1496428)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.60/0.89 % (1496422)Instruction limit reached!
% 2.60/0.89 % (1496422)------------------------------
% 2.60/0.89 % (1496422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.89 % (1496422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.89 % (1496422)CaDiCaL version: 2.1.3
% 2.60/0.89 % (1496422)Termination reason: Instruction limit
% 2.60/0.89 % (1496422)Termination phase: shuffling
% 2.60/0.89 % (1496422)Time elapsed: 0.020 s
% 2.60/0.89 % (1496422)Peak memory usage: 10 MB
% 2.60/0.89 % (1496422)Instructions burned: 24 (million)
% 2.60/0.89 % (1496428)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=119412163:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 2.60/0.89 % (1496423)Instruction limit reached!
% 2.60/0.89 % (1496423)------------------------------
% 2.60/0.89 % (1496423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.89 % (1496423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.89 % (1496423)CaDiCaL version: 2.1.3
% 2.60/0.89 % (1496423)Termination reason: Instruction limit
% 2.60/0.89 % (1496423)Termination phase: Property scanning
% 2.60/0.89 % (1496423)Time elapsed: 0.038 s
% 2.60/0.89 % (1496423)Peak memory usage: 11 MB
% 2.60/0.89 % (1496423)Instructions burned: 61 (million)
% 2.60/0.89 % (1496428)Instruction limit reached!
% 2.60/0.89 % (1496428)------------------------------
% 2.60/0.89 % (1496428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.89 % (1496428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.89 % (1496428)CaDiCaL version: 2.1.3
% 2.60/0.89 % (1496428)Termination reason: Instruction limit
% 2.60/0.89 % (1496428)Termination phase: shuffling
% 2.60/0.89 % (1496428)Time elapsed: 0.013 s
% 2.60/0.89 % (1496428)Peak memory usage: 10 MB
% 2.60/0.89 % (1496428)Instructions burned: 15 (million)
% 2.60/0.89 % (1496432)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.60/0.89 % (1496432)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=1216646901:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 2.60/0.89 % (1496433)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=3740011293:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.60/0.89 % (1496432)Instruction limit reached!
% 2.60/0.89 % (1496432)------------------------------
% 2.60/0.89 % (1496432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.89 % (1496432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.89 % (1496432)CaDiCaL version: 2.1.3
% 2.60/0.89 % (1496432)Termination reason: Instruction limit
% 2.60/0.89 % (1496432)Termination phase: shuffling
% 2.60/0.89 % (1496432)Time elapsed: 0.007 s
% 2.60/0.89 % (1496432)Peak memory usage: 10 MB
% 2.60/0.89 % (1496432)Instructions burned: 8 (million)
% 2.60/0.89 % (1496436)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=134286238:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.60/0.89 % (1496436)Instruction limit reached!
% 2.60/0.89 % (1496436)------------------------------
% 2.60/0.89 % (1496436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.89 % (1496436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.89 % (1496436)CaDiCaL version: 2.1.3
% 2.60/0.89 % (1496436)Termination reason: Instruction limit
% 2.60/0.89 % (1496436)Termination phase: shuffling
% 2.80/1.00 % (1496436)Time elapsed: 0.007 s
% 2.80/1.00 % (1496436)Peak memory usage: 11 MB
% 2.80/1.00 % (1496436)Instructions burned: 8 (million)
% 2.80/1.00 % (1496414)Instruction limit reached!
% 2.80/1.00 % (1496414)------------------------------
% 2.80/1.00 % (1496414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.80/1.00 % (1496437)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3960605870:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.80/1.00 % (1496414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.80/1.00 % (1496414)CaDiCaL version: 2.1.3
% 2.80/1.00 % (1496414)Termination reason: Instruction limit
% 2.80/1.00 % (1496414)Termination phase: Saturation
% 2.80/1.00 % (1496414)Time elapsed: 0.109 s
% 2.80/1.00 % (1496414)Peak memory usage: 15 MB
% 2.80/1.00 % (1496414)Instructions burned: 330 (million)
% 2.80/1.00 % (1496438)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2900472273:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 2.80/1.00 % (1496433)Instruction limit reached!
% 2.80/1.00 % (1496433)------------------------------
% 2.80/1.00 % (1496433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.80/1.00 % (1496433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.80/1.00 % (1496433)CaDiCaL version: 2.1.3
% 2.80/1.00 % (1496433)Termination reason: Instruction limit
% 2.80/1.00 % (1496433)Termination phase: shuffling
% 2.80/1.00 % (1496433)Time elapsed: 0.027 s
% 2.80/1.00 % (1496433)Peak memory usage: 11 MB
% 2.80/1.00 % (1496433)Instructions burned: 31 (million)
% 2.80/1.00 % (1496446)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3060306314:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/143Mi)
% 2.80/1.00 % (1496443)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3546401385:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 2.80/1.00 % (1496437)Instruction limit reached!
% 2.80/1.00 % (1496437)------------------------------
% 2.80/1.00 % (1496437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.80/1.00 % (1496437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.80/1.00 % (1496437)CaDiCaL version: 2.1.3
% 2.80/1.00 % (1496437)Termination reason: Instruction limit
% 2.80/1.00 % (1496437)Termination phase: shuffling
% 2.80/1.00 % (1496437)Time elapsed: 0.020 s
% 2.80/1.00 % (1496437)Peak memory usage: 10 MB
% 2.80/1.00 % (1496437)Instructions burned: 23 (million)
% 2.80/1.00 % (1496438)Instruction limit reached!
% 2.80/1.00 % (1496438)------------------------------
% 2.80/1.00 % (1496438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.80/1.00 % (1496438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.80/1.00 % (1496438)CaDiCaL version: 2.1.3
% 2.80/1.00 % (1496438)Termination reason: Instruction limit
% 2.80/1.00 % (1496438)Termination phase: shuffling
% 2.80/1.00 % (1496438)Time elapsed: 0.018 s
% 2.80/1.00 % (1496438)Peak memory usage: 10 MB
% 2.80/1.00 % (1496438)Instructions burned: 21 (million)
% 2.80/1.00 % (1496447)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1493834611:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 2.80/1.00 % (1496450)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1102488479:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 2.80/1.00 % (1496453)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.80/1.00 % (1496453)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4245636686:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 2.80/1.00 % (1496456)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1871107872:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 2.80/1.00 % (1496453)Instruction limit reached!
% 2.80/1.00 % (1496453)------------------------------
% 2.80/1.00 % (1496453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.80/1.00 % (1496453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.80/1.00 % (1496453)CaDiCaL version: 2.1.3
% 2.80/1.00 % (1496453)Termination reason: Instruction limit
% 4.55/1.10 % (1496453)Termination phase: shuffling
% 4.55/1.10 % (1496453)Time elapsed: 0.007 s
% 4.55/1.10 % (1496453)Peak memory usage: 10 MB
% 4.55/1.10 % (1496453)Instructions burned: 8 (million)
% 4.55/1.10 % (1496450)Instruction limit reached!
% 4.55/1.10 % (1496450)------------------------------
% 4.55/1.10 % (1496450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.55/1.10 % (1496450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.55/1.10 % (1496450)CaDiCaL version: 2.1.3
% 4.55/1.10 % (1496450)Termination reason: Instruction limit
% 4.55/1.10 % (1496450)Termination phase: shuffling
% 4.55/1.10 % (1496450)Time elapsed: 0.035 s
% 4.55/1.10 % (1496450)Peak memory usage: 10 MB
% 4.55/1.10 % (1496450)Instructions burned: 42 (million)
% 4.55/1.10 % (1496446)Instruction limit reached!
% 4.55/1.10 % (1496446)------------------------------
% 4.55/1.10 % (1496446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.55/1.10 % (1496446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.55/1.10 % (1496446)CaDiCaL version: 2.1.3
% 4.55/1.10 % (1496446)Termination reason: Instruction limit
% 4.55/1.10 % (1496446)Termination phase: Property scanning
% 4.55/1.10 % (1496446)Time elapsed: 0.061 s
% 4.55/1.10 % (1496446)Peak memory usage: 12 MB
% 4.55/1.10 % (1496446)Instructions burned: 145 (million)
% 4.55/1.10 % (1496467)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 4.55/1.10 % (1496468)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3231308297:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 4.55/1.10 % (1496465)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=1594092604:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 4.55/1.10 % (1496467)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3444003748:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 4.55/1.10 % (1496467)Instruction limit reached!
% 4.55/1.10 % (1496467)------------------------------
% 4.55/1.10 % (1496467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.55/1.10 % (1496467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.55/1.10 % (1496467)CaDiCaL version: 2.1.3
% 4.55/1.10 % (1496467)Termination reason: Instruction limit
% 4.55/1.10 % (1496467)Termination phase: shuffling
% 4.55/1.10 % (1496467)Time elapsed: 0.004 s
% 4.55/1.10 % (1496467)Peak memory usage: 10 MB
% 4.55/1.10 % (1496467)Instructions burned: 7 (million)
% 4.55/1.10 % (1496468)Instruction limit reached!
% 4.55/1.10 % (1496468)------------------------------
% 4.55/1.10 % (1496468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.55/1.10 % (1496468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.55/1.10 % (1496468)CaDiCaL version: 2.1.3
% 4.55/1.10 % (1496468)Termination reason: Instruction limit
% 4.55/1.10 % (1496468)Termination phase: shuffling
% 4.55/1.10 % (1496468)Time elapsed: 0.009 s
% 4.55/1.10 % (1496468)Peak memory usage: 10 MB
% 4.55/1.10 % (1496468)Instructions burned: 22 (million)
% 4.55/1.10 % (1496474)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1061274330:i=19:add=on:rtra=on_2995 on theBenchmark for (2995ds/19Mi)
% 4.55/1.10 % (1496475)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=2770443607:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/316Mi)
% 4.55/1.10 % (1496474)Instruction limit reached!
% 4.55/1.10 % (1496474)------------------------------
% 4.55/1.10 % (1496474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.55/1.10 % (1496474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.55/1.10 % (1496474)CaDiCaL version: 2.1.3
% 4.55/1.10 % (1496474)Termination reason: Instruction limit
% 4.55/1.10 % (1496474)Termination phase: shuffling
% 4.55/1.10 % (1496474)Time elapsed: 0.017 s
% 4.55/1.10 % (1496474)Peak memory usage: 10 MB
% 4.55/1.10 % (1496474)Instructions burned: 20 (million)
% 4.55/1.10 % (1496483)dis+1004_4:1_slsqr=1,2:to=lpo:plsq=on:fde=unused:e2e=on:si=on:spb=goal_then_units:acc=on:urr=on:uwa=off:fd=preordered:s2agt=16:slsqc=1:slsq=on:random_seed=2312709895:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2995 on theBenchmark for (2995ds/853Mi)
% 5.44/1.23 % (1496447)Instruction limit reached!
% 5.44/1.23 % (1496447)------------------------------
% 5.44/1.23 % (1496447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.44/1.23 % (1496447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.23 % (1496447)CaDiCaL version: 2.1.3
% 5.44/1.23 % (1496447)Termination reason: Instruction limit
% 5.44/1.23 % (1496447)Termination phase: Saturation
% 5.44/1.23 % (1496447)Time elapsed: 0.164 s
% 5.44/1.23 % (1496447)Peak memory usage: 14 MB
% 5.44/1.23 % (1496447)Instructions burned: 193 (million)
% 5.44/1.23 % (1496488)dis+1003_3:4_to=kbo:plsq=on:prc=on:sims=off:e2e=on:si=on:spb=intro:acc=on:urr=on:uwa=off:foolp=on:s2agt=32:slsqc=3:slsq=on:random_seed=129605520:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2994 on theBenchmark for (2994ds/45Mi)
% 5.44/1.23 % (1496456)Instruction limit reached!
% 5.44/1.23 % (1496456)------------------------------
% 5.44/1.23 % (1496456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.44/1.23 % (1496456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.23 % (1496456)CaDiCaL version: 2.1.3
% 5.44/1.23 % (1496456)Termination reason: Instruction limit
% 5.44/1.23 % (1496456)Termination phase: Saturation
% 5.44/1.23 % (1496456)Time elapsed: 0.159 s
% 5.44/1.23 % (1496456)Peak memory usage: 13 MB
% 5.44/1.23 % (1496456)Instructions burned: 182 (million)
% 5.44/1.23 % (1496465)Instruction limit reached!
% 5.44/1.23 % (1496465)------------------------------
% 5.44/1.23 % (1496465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.44/1.23 % (1496465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.23 % (1496465)CaDiCaL version: 2.1.3
% 5.44/1.23 % (1496465)Termination reason: Instruction limit
% 5.44/1.23 % (1496465)Termination phase: Saturation
% 5.44/1.23 % (1496465)Time elapsed: 0.138 s
% 5.44/1.23 % (1496465)Peak memory usage: 14 MB
% 5.44/1.23 % (1496465)Instructions burned: 170 (million)
% 5.44/1.23 % (1496488)Instruction limit reached!
% 5.44/1.23 % (1496488)------------------------------
% 5.44/1.23 % (1496488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.44/1.23 % (1496488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.23 % (1496488)CaDiCaL version: 2.1.3
% 5.44/1.23 % (1496488)Termination reason: Instruction limit
% 5.44/1.23 % (1496488)Termination phase: shuffling
% 5.44/1.23 % (1496488)Time elapsed: 0.020 s
% 5.44/1.23 % (1496488)Peak memory usage: 11 MB
% 5.44/1.23 % (1496488)Instructions burned: 47 (million)
% 5.44/1.23 % (1496491)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=2036305679:i=480:rtra=on_2994 on theBenchmark for (2994ds/480Mi)
% 5.44/1.23 % (1496493)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 5.44/1.23 % (1496493)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=2187630884:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 5.44/1.23 % (1496492)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=93261938:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2994 on theBenchmark for (2994ds/21Mi)
% 5.44/1.23 % (1496373)Instruction limit reached!
% 5.44/1.23 % (1496373)------------------------------
% 5.44/1.23 % (1496373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.44/1.23 % (1496373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.23 % (1496373)CaDiCaL version: 2.1.3
% 5.44/1.23 % (1496373)Termination reason: Instruction limit
% 5.44/1.23 % (1496373)Termination phase: Saturation
% 5.44/1.23 % (1496373)Time elapsed: 0.513 s
% 5.44/1.23 % (1496373)Peak memory usage: 17 MB
% 5.44/1.23 % (1496373)Instructions burned: 635 (million)
% 5.44/1.23 % (1496492)Instruction limit reached!
% 5.44/1.23 % (1496492)------------------------------
% 5.44/1.23 % (1496492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.44/1.23 % (1496492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.23 % (1496492)CaDiCaL version: 2.1.3
% 5.44/1.23 % (1496492)Termination reason: Instruction limit
% 5.44/1.23 % (1496492)Termination phase: shuffling
% 5.44/1.23 % (1496492)Time elapsed: 0.019 s
% 5.44/1.23 % (1496492)Peak memory usage: 11 MB
% 5.44/1.23 % (1496492)Instructions burned: 21 (million)
% 5.44/1.23 % (1496500)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3277509910:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2994 on theBenchmark for (2994ds/13Mi)
% 5.44/1.23 % (1496500)Instruction limit reached!
% 5.44/1.23 % (1496500)------------------------------
% 5.44/1.23 % (1496500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.44/1.23 % (1496500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.23 % (1496500)CaDiCaL version: 2.1.3
% 5.44/1.23 % (1496500)Termination reason: Instruction limit
% 5.44/1.23 % (1496500)Termination phase: shuffling
% 5.44/1.23 % (1496500)Time elapsed: 0.008 s
% 5.44/1.23 % (1496500)Peak memory usage: 10 MB
% 5.44/1.23 % (1496500)Instructions burned: 14 (million)
% 5.44/1.23 % (1496503)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=909338233:i=66:s2at=3:nm=2:rtra=on:rawr=on_2994 on theBenchmark for (2994ds/66Mi)
% 5.44/1.23 % (1496505)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=487031933:i=51:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/51Mi)
% 5.44/1.23 % (1496493)Instruction limit reached!
% 5.44/1.23 % (1496493)------------------------------
% 5.44/1.23 % (1496493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.44/1.23 % (1496493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.23 % (1496493)CaDiCaL version: 2.1.3
% 5.44/1.23 % (1496493)Termination reason: Instruction limit
% 5.44/1.23 % (1496493)Termination phase: Property scanning
% 5.44/1.23 % (1496493)Time elapsed: 0.075 s
% 5.44/1.23 % (1496493)Peak memory usage: 13 MB
% 5.44/1.23 % (1496493)Instructions burned: 201 (million)
% 5.44/1.23 % (1496511)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1534934806:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/31Mi)
% 5.44/1.23 % (1496511)Instruction limit reached!
% 5.44/1.23 % (1496511)------------------------------
% 5.44/1.23 % (1496511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.44/1.23 % (1496511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.23 % (1496511)CaDiCaL version: 2.1.3
% 5.44/1.23 % (1496511)Termination reason: Instruction limit
% 5.44/1.23 % (1496511)Termination phase: shuffling
% 5.44/1.23 % (1496511)Time elapsed: 0.009 s
% 5.44/1.23 % (1496511)Peak memory usage: 11 MB
% 5.44/1.23 % (1496511)Instructions burned: 33 (million)
% 5.44/1.23 % (1496503)Instruction limit reached!
% 5.44/1.23 % (1496503)------------------------------
% 5.44/1.23 % (1496503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.44/1.23 % (1496503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.23 % (1496503)CaDiCaL version: 2.1.3
% 5.44/1.23 % (1496503)Termination reason: Instruction limit
% 5.44/1.23 % (1496503)Termination phase: shuffling
% 5.44/1.23 % (1496503)Time elapsed: 0.047 s
% 5.44/1.23 % (1496503)Peak memory usage: 12 MB
% 5.44/1.23 % (1496503)Instructions burned: 67 (million)
% 5.44/1.23 % (1496505)Instruction limit reached!
% 5.44/1.23 % (1496505)------------------------------
% 5.44/1.23 % (1496505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.44/1.23 % (1496505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.23 % (1496505)CaDiCaL version: 2.1.3
% 5.44/1.23 % (1496505)Termination reason: Instruction limit
% 5.44/1.23 % (1496505)Termination phase: shuffling
% 5.44/1.23 % (1496505)Time elapsed: 0.042 s
% 5.44/1.23 % (1496505)Peak memory usage: 11 MB
% 5.44/1.23 % (1496505)Instructions burned: 52 (million)
% 5.44/1.23 % (1496516)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3668386613:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2993 on theBenchmark for (2993ds/137Mi)
% 5.44/1.23 % (1496475)Instruction limit reached!
% 5.44/1.23 % (1496475)------------------------------
% 5.44/1.23 % (1496475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.44/1.23 % (1496475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.23 % (1496475)CaDiCaL version: 2.1.3
% 5.44/1.23 % (1496475)Termination reason: Instruction limit
% 5.44/1.23 % (1496475)Termination phase: Saturation
% 5.44/1.23 % (1496475)Time elapsed: 0.254 s
% 5.44/1.23 % (1496475)Peak memory usage: 14 MB
% 5.44/1.23 % (1496475)Instructions burned: 317 (million)
% 5.44/1.23 % (1496517)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=2399129699:cond=on:i=34:hud=10:nm=10:rtra=on_2993 on theBenchmark for (2993ds/34Mi)
% 5.44/1.23 % (1496518)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=873969929:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2993 on theBenchmark for (2993ds/67Mi)
% 5.44/1.23 % (1496517)Instruction limit reached!
% 5.44/1.23 % (1496517)------------------------------
% 5.44/1.23 % (1496517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.44/1.23 % (1496517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.23 % (1496517)CaDiCaL version: 2.1.3
% 5.44/1.23 % (1496517)Termination reason: Instruction limit
% 5.44/1.23 % (1496517)Termination phase: shuffling
% 5.44/1.23 % (1496517)Time elapsed: 0.018 s
% 5.44/1.23 % (1496517)Peak memory usage: 11 MB
% 5.44/1.23 % (1496517)Instructions burned: 35 (million)
% 5.44/1.23 % (1496522)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.44/1.23 % (1496522)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=3361733653:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2993 on theBenchmark for (2993ds/180Mi)
% 5.44/1.23 % (1496516)Instruction limit reached!
% 5.44/1.23 % (1496516)------------------------------
% 5.44/1.23 % (1496516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.44/1.23 % (1496516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.23 % (1496516)CaDiCaL version: 2.1.3
% 5.44/1.23 % (1496516)Termination reason: Instruction limit
% 5.44/1.23 % (1496516)Termination phase: Property scanning
% 5.44/1.23 % (1496516)Time elapsed: 0.060 s
% 5.44/1.23 % (1496516)Peak memory usage: 12 MB
% 5.44/1.23 % (1496516)Instructions burned: 137 (million)
% 5.44/1.23 % (1496524)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=1637137527:st=2:i=246:sd=3:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/246Mi)
% 5.44/1.23 % (1496518)Instruction limit reached!
% 5.44/1.23 % (1496518)------------------------------
% 5.44/1.23 % (1496518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.44/1.23 % (1496518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.23 % (1496518)CaDiCaL version: 2.1.3
% 5.44/1.23 % (1496518)Termination reason: Instruction limit
% 5.44/1.23 % (1496518)Termination phase: Property scanning
% 5.44/1.23 % (1496518)Time elapsed: 0.055 s
% 5.44/1.23 % (1496518)Peak memory usage: 11 MB
% 5.44/1.23 % (1496518)Instructions burned: 68 (million)
% 5.44/1.23 % (1496526)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=3734058802:cond=on:i=96:bd=all:rtra=on_2992 on theBenchmark for (2992ds/96Mi)
% 5.44/1.23 % (1496530)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=2913410060:i=427:sd=1:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/427Mi)
% 5.44/1.23 % (1496483) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1496359-1496483"...
% 5.44/1.23 % (1496483)...printing done.
% 5.44/1.23 % (1496491) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1496359-1496491"...
% 5.44/1.23 % (1496483)Refutation found. Thanks to Tanya!
% 5.44/1.23 % SZS status Theorem for theBenchmark
% 5.44/1.23 % SZS output start Proof for theBenchmark
% See solution above
% 5.44/1.23 % (1496483)------------------------------
% 5.44/1.23 % (1496483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.44/1.23 % (1496483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.44/1.23 % (1496483)CaDiCaL version: 2.1.3
% 5.44/1.23 % (1496483)Termination reason: Refutation
% 5.44/1.23 % (1496483)Time elapsed: 0.333 s
% 5.44/1.23 % (1496483)Peak memory usage: 17 MB
% 5.44/1.23 % (1496483)Instructions burned: 427 (million)
% 5.44/1.23 % (1496359)Success in time 0.824 s
% 5.44/1.23 % Vampire exiting
%------------------------------------------------------------------------------