%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SCT197_5 : TPTP v9.3.1. Released v6.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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:37:45 PM UTC 2026
% Result : Theorem 212.30s 37.80s
% Output : Refutation 212.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 7
% Syntax : Number of formulae : 27 ( 22 unt; 0 typ; 0 def)
% Number of atoms : 34 ( 11 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 15 ( 8 ~; 4 |; 1 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-6 aty)
% Number of functors : 104 ( 104 usr; 7 con; 0-7 aty)
% Number of variables : 42 ( 41 !; 1 ?; 42 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
arrow_411405190le_alt: $tType ).
tff(type_def_6,type,
arrow_159774573e_indi: $tType ).
tff(type_def_7,type,
bool: $tType ).
tff(type_def_8,type,
fun: ( $tType * $tType ) > $tType ).
tff(type_def_9,type,
product_prod: ( $tType * $tType ) > $tType ).
tff(func_def_0,type,
arrow_1985332922le_Lin: fun(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),bool) ).
tff(func_def_1,type,
arrow_610318064e_Prof: fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),bool) ).
tff(func_def_2,type,
arrow_1158827142_above: ( fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool) * arrow_411405190le_alt * arrow_411405190le_alt ) > fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool) ).
tff(func_def_3,type,
arrow_319942042_below: ( fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool) * arrow_411405190le_alt * arrow_411405190le_alt ) > fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool) ).
tff(func_def_4,type,
arrow_276188178_mkbot: ( fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool) * arrow_411405190le_alt ) > fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool) ).
tff(func_def_5,type,
arrow_424895264_mktop: ( fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool) * arrow_411405190le_alt ) > fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool) ).
tff(func_def_6,type,
combb:
!>[X0: $tType,X1: $tType,X2: $tType] : ( fun(X0,X1) > fun(fun(X2,X0),fun(X2,X1)) ) ).
tff(func_def_7,type,
combc:
!>[X0: $tType,X1: $tType,X2: $tType] : fun(fun(X0,fun(X1,X2)),fun(X1,fun(X0,X2))) ).
tff(func_def_8,type,
combi:
!>[X0: $tType] : fun(X0,X0) ).
tff(func_def_9,type,
combk:
!>[X0: $tType,X1: $tType] : ( X0 > fun(X1,X0) ) ).
tff(func_def_10,type,
pi:
!>[X0: $tType,X1: $tType] : ( ( fun(X0,bool) * fun(X0,fun(X1,bool)) ) > fun(fun(X0,X1),bool) ) ).
tff(func_def_11,type,
extensional_funcset:
!>[X0: $tType,X1: $tType] : ( ( fun(X0,bool) * fun(X1,bool) ) > fun(fun(X0,X1),bool) ) ).
tff(func_def_12,type,
order_215145569der_on:
!>[X0: $tType] : ( fun(X0,bool) > fun(fun(product_prod(X0,X0),bool),bool) ) ).
tff(func_def_13,type,
bot_bot:
!>[X0: $tType] : X0 ).
tff(func_def_14,type,
top_top:
!>[X0: $tType] : X0 ).
tff(func_def_15,type,
conversep:
!>[X0: $tType,X1: $tType] : ( fun(X0,fun(X1,bool)) > fun(X1,fun(X0,bool)) ) ).
tff(func_def_16,type,
product_Pair:
!>[X0: $tType,X1: $tType] : fun(X0,fun(X1,product_prod(X0,X1))) ).
tff(func_def_17,type,
product_curry:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( fun(product_prod(X0,X1),X2) * X0 * X1 ) > X2 ) ).
tff(func_def_18,type,
produc1605651328_split:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( fun(X0,fun(X1,X2)) * product_prod(X0,X1) ) > X2 ) ).
tff(func_def_19,type,
product_prod_rec:
!>[X0: $tType,X1: $tType,X2: $tType] : ( ( fun(X0,fun(X1,X2)) * product_prod(X0,X1) ) > X2 ) ).
tff(func_def_20,type,
id_on:
!>[X0: $tType] : ( fun(X0,bool) > fun(product_prod(X0,X0),bool) ) ).
tff(func_def_21,type,
converse:
!>[X0: $tType,X1: $tType] : ( fun(product_prod(X0,X1),bool) > fun(product_prod(X1,X0),bool) ) ).
tff(func_def_22,type,
inv_image:
!>[X0: $tType,X1: $tType] : ( ( fun(product_prod(X0,X0),bool) * fun(X1,X0) ) > fun(product_prod(X1,X1),bool) ) ).
tff(func_def_23,type,
collect:
!>[X0: $tType] : ( fun(X0,bool) > fun(X0,bool) ) ).
tff(func_def_24,type,
aa:
!>[X0: $tType,X1: $tType] : ( ( fun(X0,X1) * X0 ) > X1 ) ).
tff(func_def_25,type,
fFalse: bool ).
tff(func_def_26,type,
fNot: fun(bool,bool) ).
tff(func_def_27,type,
fTrue: bool ).
tff(func_def_28,type,
fequal:
!>[X0: $tType] : fun(X0,fun(X0,bool)) ).
tff(func_def_29,type,
member:
!>[X0: $tType] : fun(X0,fun(fun(X0,bool),bool)) ).
tff(func_def_30,type,
l: fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool) ).
tff(func_def_31,type,
sK0:
!>[X0: $tType,X1: $tType] : ( ( fun(X0,X1) * fun(X0,X1) ) > X0 ) ).
tff(func_def_32,type,
sK1:
!>[X0: $tType,X1: $tType] : ( ( fun(product_prod(X1,X0),bool) * product_prod(X0,X1) ) > X0 ) ).
tff(func_def_33,type,
sK2:
!>[X0: $tType,X1: $tType] : ( ( fun(product_prod(X1,X0),bool) * product_prod(X0,X1) ) > X1 ) ).
tff(func_def_34,type,
sK3:
!>[X0: $tType,X1: $tType] : ( fun(product_prod(X0,X1),bool) > X0 ) ).
tff(func_def_35,type,
sK4:
!>[X0: $tType,X1: $tType] : ( fun(product_prod(X0,X1),bool) > X1 ) ).
tff(func_def_36,type,
sK5:
!>[X0: $tType,X1: $tType] : ( fun(product_prod(X0,X1),bool) > product_prod(X0,X1) ) ).
tff(func_def_37,type,
sK6:
!>[X0: $tType] : ( fun(X0,bool) > X0 ) ).
tff(func_def_38,type,
sK7:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( product_prod(X2,product_prod(X3,product_prod(X0,X1))) > X0 ) ).
tff(func_def_39,type,
sK8:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( product_prod(X2,product_prod(X3,product_prod(X0,X1))) > X1 ) ).
tff(func_def_40,type,
sK9:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( product_prod(X2,product_prod(X3,product_prod(X0,X1))) > X3 ) ).
tff(func_def_41,type,
sK10:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( product_prod(X2,product_prod(X3,product_prod(X0,X1))) > X2 ) ).
tff(func_def_42,type,
sK11:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( fun(product_prod(X0,product_prod(X1,product_prod(X3,X2))),bool) > X2 ) ).
tff(func_def_43,type,
sK12:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( fun(product_prod(X0,product_prod(X1,product_prod(X3,X2))),bool) > X0 ) ).
tff(func_def_44,type,
sK13:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( fun(product_prod(X0,product_prod(X1,product_prod(X3,X2))),bool) > X3 ) ).
tff(func_def_45,type,
sK14:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType] : ( fun(product_prod(X0,product_prod(X1,product_prod(X3,X2))),bool) > X1 ) ).
tff(func_def_46,type,
sK15:
!>[X0: $tType,X1: $tType,X2: $tType] : ( fun(product_prod(X1,product_prod(X0,X2)),bool) > X0 ) ).
tff(func_def_47,type,
sK16:
!>[X0: $tType,X1: $tType,X2: $tType] : ( fun(product_prod(X1,product_prod(X0,X2)),bool) > X2 ) ).
tff(func_def_48,type,
sK17:
!>[X0: $tType,X1: $tType,X2: $tType] : ( fun(product_prod(X1,product_prod(X0,X2)),bool) > X1 ) ).
tff(func_def_49,type,
sK18:
!>[X0: $tType,X1: $tType] : ( ( fun(X1,bool) * fun(X1,X0) * fun(X1,fun(X0,bool)) ) > X1 ) ).
tff(func_def_50,type,
sK19:
!>[X0: $tType] : ( fun(X0,bool) > X0 ) ).
tff(func_def_51,type,
sK20:
!>[X0: $tType,X1: $tType] : ( product_prod(X1,X0) > X0 ) ).
tff(func_def_52,type,
sK21:
!>[X0: $tType,X1: $tType] : ( product_prod(X1,X0) > X1 ) ).
tff(func_def_53,type,
sK22:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( fun(product_prod(X1,product_prod(X0,product_prod(X2,product_prod(X4,X3)))),bool) > X4 ) ).
tff(func_def_54,type,
sK23:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( fun(product_prod(X1,product_prod(X0,product_prod(X2,product_prod(X4,X3)))),bool) > X1 ) ).
tff(func_def_55,type,
sK24:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( fun(product_prod(X1,product_prod(X0,product_prod(X2,product_prod(X4,X3)))),bool) > X0 ) ).
tff(func_def_56,type,
sK25:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( fun(product_prod(X1,product_prod(X0,product_prod(X2,product_prod(X4,X3)))),bool) > X2 ) ).
tff(func_def_57,type,
sK26:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( fun(product_prod(X1,product_prod(X0,product_prod(X2,product_prod(X4,X3)))),bool) > X3 ) ).
tff(func_def_58,type,
sK27:
!>[X0: $tType,X1: $tType] : ( fun(product_prod(X0,X1),bool) > X0 ) ).
tff(func_def_59,type,
sK28:
!>[X0: $tType,X1: $tType] : ( fun(product_prod(X0,X1),bool) > X1 ) ).
tff(func_def_60,type,
sK29:
!>[X0: $tType,X1: $tType] : ( fun(product_prod(X0,X1),bool) > product_prod(X0,X1) ) ).
tff(func_def_61,type,
sK30:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType,X5: $tType] : ( product_prod(X3,product_prod(X1,product_prod(X4,product_prod(X0,product_prod(X2,X5))))) > X0 ) ).
tff(func_def_62,type,
sK31:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType,X5: $tType] : ( product_prod(X3,product_prod(X1,product_prod(X4,product_prod(X0,product_prod(X2,X5))))) > X5 ) ).
tff(func_def_63,type,
sK32:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType,X5: $tType] : ( product_prod(X3,product_prod(X1,product_prod(X4,product_prod(X0,product_prod(X2,X5))))) > X1 ) ).
tff(func_def_64,type,
sK33:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType,X5: $tType] : ( product_prod(X3,product_prod(X1,product_prod(X4,product_prod(X0,product_prod(X2,X5))))) > X2 ) ).
tff(func_def_65,type,
sK34:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType,X5: $tType] : ( product_prod(X3,product_prod(X1,product_prod(X4,product_prod(X0,product_prod(X2,X5))))) > X4 ) ).
tff(func_def_66,type,
sK35:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType,X5: $tType] : ( product_prod(X3,product_prod(X1,product_prod(X4,product_prod(X0,product_prod(X2,X5))))) > X3 ) ).
tff(func_def_67,type,
sK36:
!>[X0: $tType,X1: $tType] : ( ( fun(X0,X1) * fun(X0,bool) * fun(X0,X1) ) > X0 ) ).
tff(func_def_68,type,
sK37:
!>[X0: $tType,X1: $tType] : ( ( fun(X1,bool) * fun(X1,fun(X0,bool)) ) > X1 ) ).
tff(func_def_69,type,
sK38:
!>[X0: $tType] : ( fun(X0,bool) > X0 ) ).
tff(func_def_70,type,
sK39:
!>[X0: $tType] : X0 ).
tff(func_def_71,type,
sK40:
!>[X0: $tType] : ( fun(X0,bool) > X0 ) ).
tff(func_def_72,type,
sK41:
!>[X0: $tType,X1: $tType] : ( ( fun(product_prod(X0,X1),bool) * fun(product_prod(X0,X1),bool) ) > X0 ) ).
tff(func_def_73,type,
sK42:
!>[X0: $tType,X1: $tType] : ( ( fun(product_prod(X0,X1),bool) * fun(product_prod(X0,X1),bool) ) > X1 ) ).
tff(func_def_74,type,
sK43: fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool) ).
tff(func_def_75,type,
sK44:
!>[X0: $tType,X1: $tType,X2: $tType] : ( product_prod(X1,product_prod(X2,X0)) > X1 ) ).
tff(func_def_76,type,
sK45:
!>[X0: $tType,X1: $tType,X2: $tType] : ( product_prod(X1,product_prod(X2,X0)) > X2 ) ).
tff(func_def_77,type,
sK46:
!>[X0: $tType,X1: $tType,X2: $tType] : ( product_prod(X1,product_prod(X2,X0)) > X0 ) ).
tff(func_def_78,type,
sK47:
!>[X0: $tType,X1: $tType] : ( ( fun(X1,bool) * fun(X0,X1) * fun(X0,bool) ) > X0 ) ).
tff(func_def_79,type,
sK48:
!>[X0: $tType] : ( ( fun(product_prod(X0,X0),bool) * fun(X0,bool) ) > X0 ) ).
tff(func_def_80,type,
sK49:
!>[X0: $tType] : ( ( fun(product_prod(X0,X0),bool) * fun(X0,bool) ) > X0 ) ).
tff(func_def_81,type,
sK50:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( product_prod(X1,product_prod(X0,product_prod(X3,product_prod(X4,X2)))) > X2 ) ).
tff(func_def_82,type,
sK51:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( product_prod(X1,product_prod(X0,product_prod(X3,product_prod(X4,X2)))) > X0 ) ).
tff(func_def_83,type,
sK52:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( product_prod(X1,product_prod(X0,product_prod(X3,product_prod(X4,X2)))) > X1 ) ).
tff(func_def_84,type,
sK53:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( product_prod(X1,product_prod(X0,product_prod(X3,product_prod(X4,X2)))) > X3 ) ).
tff(func_def_85,type,
sK54:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType] : ( product_prod(X1,product_prod(X0,product_prod(X3,product_prod(X4,X2)))) > X4 ) ).
tff(func_def_86,type,
sK55:
!>[X0: $tType,X1: $tType] : ( ( fun(X0,bool) * fun(X0,X1) * fun(X0,fun(X1,bool)) ) > X0 ) ).
tff(func_def_87,type,
sK56:
!>[X0: $tType,X1: $tType] : ( product_prod(X1,X0) > X1 ) ).
tff(func_def_88,type,
sK57:
!>[X0: $tType,X1: $tType] : ( product_prod(X1,X0) > X0 ) ).
tff(func_def_89,type,
sK58: ( fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)) * arrow_159774573e_indi ) > fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)) ).
tff(func_def_90,type,
sK59: ( fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)) * arrow_159774573e_indi ) > arrow_411405190le_alt ).
tff(func_def_91,type,
sK60: ( fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)) * arrow_159774573e_indi ) > arrow_411405190le_alt ).
tff(func_def_92,type,
sK61:
!>[X0: $tType] : ( fun(X0,bool) > X0 ) ).
tff(func_def_93,type,
sK62:
!>[X0: $tType] : ( fun(X0,bool) > X0 ) ).
tff(func_def_94,type,
sK63:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType,X5: $tType] : ( fun(product_prod(X5,product_prod(X1,product_prod(X0,product_prod(X3,product_prod(X4,X2))))),bool) > X3 ) ).
tff(func_def_95,type,
sK64:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType,X5: $tType] : ( fun(product_prod(X5,product_prod(X1,product_prod(X0,product_prod(X3,product_prod(X4,X2))))),bool) > X2 ) ).
tff(func_def_96,type,
sK65:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType,X5: $tType] : ( fun(product_prod(X5,product_prod(X1,product_prod(X0,product_prod(X3,product_prod(X4,X2))))),bool) > X5 ) ).
tff(func_def_97,type,
sK66:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType,X5: $tType] : ( fun(product_prod(X5,product_prod(X1,product_prod(X0,product_prod(X3,product_prod(X4,X2))))),bool) > X4 ) ).
tff(func_def_98,type,
sK67:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType,X5: $tType] : ( fun(product_prod(X5,product_prod(X1,product_prod(X0,product_prod(X3,product_prod(X4,X2))))),bool) > X1 ) ).
tff(func_def_99,type,
sK68:
!>[X0: $tType,X1: $tType,X2: $tType,X3: $tType,X4: $tType,X5: $tType] : ( fun(product_prod(X5,product_prod(X1,product_prod(X0,product_prod(X3,product_prod(X4,X2))))),bool) > X0 ) ).
tff(func_def_100,type,
sK69:
!>[X0: $tType,X1: $tType] : ( ( X0 * X1 * fun(X1,fun(X0,bool)) ) > X0 ) ).
tff(func_def_101,type,
sK70:
!>[X0: $tType,X1: $tType] : ( ( X0 * X1 * fun(X1,fun(X0,bool)) ) > X1 ) ).
tff(pred_def_1,type,
bot:
!>[X0: $tType] : $o ).
tff(pred_def_2,type,
top:
!>[X0: $tType] : $o ).
tff(pred_def_3,type,
arrow_1958449194le_IIA: fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)) > $o ).
tff(pred_def_4,type,
arrow_987702531ctator: ( fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)) * arrow_159774573e_indi ) > $o ).
tff(pred_def_5,type,
arrow_2069624013nimity: fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)) > $o ).
tff(pred_def_6,type,
inv_imagep:
!>[X0: $tType,X1: $tType] : ( ( fun(X0,fun(X0,bool)) * fun(X1,X0) * X1 * X1 ) > $o ) ).
tff(pred_def_7,type,
total_on:
!>[X0: $tType] : ( ( fun(X0,bool) * fun(product_prod(X0,X0),bool) ) > $o ) ).
tff(pred_def_8,type,
pp: bool > $o ).
tff(f8,axiom,
arrow_610318064e_Prof = pi(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),top_top(fun(arrow_159774573e_indi,bool)),combk(fun(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),bool),arrow_159774573e_indi,arrow_1985332922le_Lin)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_Prof__def) ).
tff(f27,axiom,
! [X0: $tType] : ( top_top(fun(X0,bool)) = collect(X0,combk(bool,X0,fTrue)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_UNIV__def) ).
tff(f39,axiom,
! [X0: $tType,X1: $tType,X4: fun(X0,bool),X2: fun(X1,bool),X3: fun(X0,X1)] :
( ! [X5: X0] :
( pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X5),X4))
=> pp(aa(fun(X1,bool),bool,aa(X1,fun(fun(X1,bool),bool),member(X1),aa(X0,X1,X3,X5)),X2)) )
=> pp(aa(fun(fun(X0,X1),bool),bool,aa(fun(X0,X1),fun(fun(fun(X0,X1),bool),bool),member(fun(X0,X1)),X3),pi(X0,X1,X4,combk(fun(X1,bool),X0,X2)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_funcsetI) ).
tff(f78,axiom,
! [X0: $tType,X1: fun(X0,bool)] : ( collect(X0,X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_Collect__def) ).
tff(f112,axiom,
! [X0: $tType,X1: $tType,X3: X1,X2: X0] : ( aa(X0,X1,combk(X1,X0,X3),X2) = X3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBK_1_1_U) ).
tff(f119,axiom,
pp(aa(fun(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),bool),bool,aa(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),fun(fun(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),bool),bool),member(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),l),arrow_1985332922le_Lin)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
tff(f120,conjecture,
pp(aa(fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),bool),bool,aa(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),fun(fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),bool),bool),member(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool))),combk(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),arrow_159774573e_indi,l)),arrow_610318064e_Prof)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1) ).
tff(f121,negated_conjecture,
~ pp(aa(fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),bool),bool,aa(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),fun(fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),bool),bool),member(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool))),combk(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),arrow_159774573e_indi,l)),arrow_610318064e_Prof)),
inference(negated_conjecture,[status(cth)],[f120]) ).
tff(f128,plain,
! [X1: $tType,X0: $tType,X2: X1,X3: X0] : ( aa(X0,X1,combk(X1,X0,X2),X3) = X2 ),
inference(rectify,[],[f112]) ).
tff(f165,plain,
~ pp(aa(fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),bool),bool,aa(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),fun(fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),bool),bool),member(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool))),combk(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),arrow_159774573e_indi,l)),arrow_610318064e_Prof)),
inference(flattening,[],[f121]) ).
tff(f219,plain,
! [X1: $tType,X0: $tType,X3: fun(X0,X1),X4: fun(X0,bool),X2: fun(X1,bool)] :
( pp(aa(fun(fun(X0,X1),bool),bool,aa(fun(X0,X1),fun(fun(fun(X0,X1),bool),bool),member(fun(X0,X1)),X3),pi(X0,X1,X4,combk(fun(X1,bool),X0,X2))))
| ? [X5: X0] :
( ~ pp(aa(fun(X1,bool),bool,aa(X1,fun(fun(X1,bool),bool),member(X1),aa(X0,X1,X3,X5)),X2))
& pp(aa(fun(X0,bool),bool,aa(X0,fun(fun(X0,bool),bool),member(X0),X5),X4)) ) ),
inference(ennf_transformation,[],[f39]) ).
tff(f285,plain,
! [X0: $tType] : ( top_top(fun(X0,bool)) = collect(X0,combk(bool,X0,fTrue)) ),
inference(cnf_transformation,[],[f27]) ).
tff(f324,plain,
~ pp(aa(fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),bool),bool,aa(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),fun(fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),bool),bool),member(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool))),combk(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),arrow_159774573e_indi,l)),arrow_610318064e_Prof)),
inference(cnf_transformation,[],[f165]) ).
tff(f325,plain,
! [X0: $tType,X1: fun(X0,bool)] : ( collect(X0,X1) = X1 ),
inference(cnf_transformation,[],[f78]) ).
tff(f355,plain,
! [X1: $tType,X0: $tType,X2: fun(X1,bool),X3: fun(X0,X1),X4: fun(X0,bool)] :
( pp(aa(fun(fun(X0,X1),bool),bool,aa(fun(X0,X1),fun(fun(fun(X0,X1),bool),bool),member(fun(X0,X1)),X3),pi(X0,X1,X4,combk(fun(X1,bool),X0,X2))))
| ~ pp(aa(fun(X1,bool),bool,aa(X1,fun(fun(X1,bool),bool),member(X1),aa(X0,X1,X3,sK47(X0,X1,X2,X3,X4))),X2)) ),
inference(cnf_transformation,[],[f219]) ).
tff(f364,plain,
pp(aa(fun(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),bool),bool,aa(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),fun(fun(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),bool),bool),member(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),l),arrow_1985332922le_Lin)),
inference(cnf_transformation,[],[f119]) ).
tff(f379,plain,
arrow_610318064e_Prof = pi(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),top_top(fun(arrow_159774573e_indi,bool)),combk(fun(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),bool),arrow_159774573e_indi,arrow_1985332922le_Lin)),
inference(cnf_transformation,[],[f8]) ).
tff(f444,plain,
! [X1: $tType,X0: $tType,X2: X1,X3: X0] : ( aa(X0,X1,combk(X1,X0,X2),X3) = X2 ),
inference(cnf_transformation,[],[f128]) ).
tff(f507,plain,
~ pp(aa(fun(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),bool),bool,aa(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),fun(fun(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),bool),bool),member(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),l),arrow_1985332922le_Lin)),
inference(consistent_polarity_flipping,[],[f364]) ).
tff(f557,plain,
pp(aa(fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),bool),bool,aa(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),fun(fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),bool),bool),member(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool))),combk(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),arrow_159774573e_indi,l)),arrow_610318064e_Prof)),
inference(consistent_polarity_flipping,[],[f324]) ).
tff(f584,plain,
! [X1: $tType,X0: $tType,X2: fun(X1,bool),X3: fun(X0,X1),X4: fun(X0,bool)] :
( ~ pp(aa(fun(fun(X0,X1),bool),bool,aa(fun(X0,X1),fun(fun(fun(X0,X1),bool),bool),member(fun(X0,X1)),X3),pi(X0,X1,X4,combk(fun(X1,bool),X0,X2))))
| pp(aa(fun(X1,bool),bool,aa(X1,fun(fun(X1,bool),bool),member(X1),aa(X0,X1,X3,sK47(X0,X1,X2,X3,X4))),X2)) ),
inference(consistent_polarity_flipping,[],[f355]) ).
tff(f777,plain,
! [X0: $tType] : ( top_top(fun(X0,bool)) = combk(bool,X0,fTrue) ),
inference(forward_demodulation,[],[f285,f325]) ).
tff(f2305,plain,
arrow_610318064e_Prof = pi(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),combk(bool,arrow_159774573e_indi,fTrue),combk(fun(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),bool),arrow_159774573e_indi,arrow_1985332922le_Lin)),
inference(forward_demodulation,[],[f379,f777]) ).
tff(f7360,plain,
! [X0: fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool))] :
( ~ pp(aa(fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),bool),bool,aa(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),fun(fun(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),bool),bool),member(fun(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool))),X0),arrow_610318064e_Prof))
| pp(aa(fun(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),bool),bool,aa(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),fun(fun(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),bool),bool),member(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),aa(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),X0,sK47(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),arrow_1985332922le_Lin,X0,combk(bool,arrow_159774573e_indi,fTrue)))),arrow_1985332922le_Lin)) ),
inference(superposition,[],[f584,f2305]) ).
tff(f170531,plain,
pp(aa(fun(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),bool),bool,aa(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),fun(fun(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),bool),bool),member(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),aa(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),combk(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),arrow_159774573e_indi,l),sK47(arrow_159774573e_indi,fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),arrow_1985332922le_Lin,combk(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),arrow_159774573e_indi,l),combk(bool,arrow_159774573e_indi,fTrue)))),arrow_1985332922le_Lin)),
inference(resolution,[],[f7360,f557]) ).
tff(f170699,plain,
pp(aa(fun(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),bool),bool,aa(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),fun(fun(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool),bool),bool),member(fun(product_prod(arrow_411405190le_alt,arrow_411405190le_alt),bool)),l),arrow_1985332922le_Lin)),
inference(forward_demodulation,[],[f170531,f444]) ).
tff(f170736,plain,
$false,
inference(forward_subsumption_resolution,[],[f170699,f507]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SCT197_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n011.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 23:59:00 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/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
% 7.68/1.65 % (2896256)Will run a generic schedule for satisfiability detection.
% 7.68/1.65 % (2896269)% WARNING: option uhcvi not known.
% 7.68/1.65 % (2896269)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3664990561:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.68/1.65 % (2896268)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=193087021_2999 on theBenchmark for (2999ds/0Mi)
% 7.68/1.65 % (2896270)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4222968987:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.68/1.65 % (2896271)dis+10_1_sil=32000:sp=arity:random_seed=2449216725:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.68/1.65 % (2896272)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3357756902:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.68/1.65 % (2896274)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=233057490:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.68/1.65 % (2896273)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3643988171:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.68/1.65 % Exception at run slice level
% 7.68/1.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.68/1.65 % (2896295)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=528634386:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.68/1.65 % Exception at run slice level
% 7.68/1.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.68/1.65 % (2896271)Instruction limit reached!
% 7.68/1.65 % (2896271)------------------------------
% 7.68/1.65 % (2896271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.68/1.65 % (2896271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.68/1.65 % (2896271)CaDiCaL version: 2.1.3
% 7.68/1.65 % (2896271)Termination reason: Instruction limit
% 7.68/1.65 % (2896271)Termination phase: Saturation
% 7.68/1.65 % (2896271)Time elapsed: 0.058 s
% 7.68/1.65 % (2896271)Peak memory usage: 12 MB
% 7.68/1.65 % (2896271)Instructions burned: 103 (million)
% 7.68/1.65 % (2896311)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2762704533:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.68/1.65 % (2896272)Instruction limit reached!
% 7.68/1.65 % (2896272)------------------------------
% 7.68/1.65 % (2896272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.68/1.65 % (2896272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.68/1.65 % (2896272)CaDiCaL version: 2.1.3
% 7.68/1.65 % (2896272)Termination reason: Instruction limit
% 7.68/1.65 % (2896272)Termination phase: Saturation
% 7.68/1.65 % (2896272)Time elapsed: 0.065 s
% 7.68/1.65 % (2896272)Peak memory usage: 12 MB
% 7.68/1.65 % (2896272)Instructions burned: 117 (million)
% 7.68/1.65 % (2896273)Instruction limit reached!
% 7.68/1.65 % (2896273)------------------------------
% 7.68/1.65 % (2896273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.68/1.65 % (2896273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.68/1.65 % (2896273)CaDiCaL version: 2.1.3
% 7.68/1.65 % (2896273)Termination reason: Instruction limit
% 7.68/1.65 % (2896273)Termination phase: Saturation
% 7.68/1.66 % (2896273)Time elapsed: 0.075 s
% 7.68/1.66 % (2896273)Peak memory usage: 12 MB
% 7.68/1.66 % (2896273)Instructions burned: 133 (million)
% 7.68/1.66 % (2896324)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=1950682918:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.68/1.66 % (2896329)ott-21_1_sil=16000:fs=off:random_seed=2495750008:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.68/1.66 % (2896274)Instruction limit reached!
% 7.68/1.66 % (2896274)------------------------------
% 7.68/1.66 % (2896274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.68/1.66 % (2896274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.68/1.66 % (2896274)CaDiCaL version: 2.1.3
% 7.68/1.66 % (2896274)Termination reason: Instruction limit
% 7.68/1.66 % (2896274)Termination phase: Saturation
% 7.68/1.66 % (2896274)Time elapsed: 0.092 s
% 7.68/1.66 % (2896274)Peak memory usage: 13 MB
% 7.68/1.66 % (2896274)Instructions burned: 159 (million)
% 7.68/1.66 % (2896331)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1239979560:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 21.84/3.67 % (2896339)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1448183930:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 21.84/3.67 % Exception at run slice level
% 21.84/3.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.84/3.67 % (2896311)Instruction limit reached!
% 21.84/3.67 % (2896311)------------------------------
% 21.84/3.67 % (2896311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.84/3.67 % (2896311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.84/3.67 % (2896311)CaDiCaL version: 2.1.3
% 21.84/3.67 % (2896311)Termination reason: Instruction limit
% 21.84/3.67 % (2896311)Termination phase: Saturation
% 21.84/3.67 % (2896311)Time elapsed: 0.077 s
% 21.84/3.67 % (2896311)Peak memory usage: 13 MB
% 21.84/3.67 % (2896311)Instructions burned: 131 (million)
% 21.84/3.67 % (2896346)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1274471001:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 21.84/3.67 % (2896351)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3928289209:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 21.84/3.67 % Exception at run slice level
% 21.84/3.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.84/3.67 % (2896362)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=2138287431:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 21.84/3.67 % (2896329)Instruction limit reached!
% 21.84/3.67 % (2896329)------------------------------
% 21.84/3.67 % (2896329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.84/3.67 % (2896329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.84/3.67 % (2896329)CaDiCaL version: 2.1.3
% 21.84/3.67 % (2896329)Termination reason: Instruction limit
% 21.84/3.67 % (2896329)Termination phase: Saturation
% 21.84/3.67 % (2896329)Time elapsed: 0.125 s
% 21.84/3.67 % (2896329)Peak memory usage: 12 MB
% 21.84/3.67 % (2896329)Instructions burned: 182 (million)
% 21.84/3.67 % (2896368)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2752089720:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 21.84/3.67 % (2896331)Instruction limit reached!
% 21.84/3.67 % (2896331)------------------------------
% 21.84/3.67 % (2896331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.84/3.67 % (2896331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.84/3.67 % (2896331)CaDiCaL version: 2.1.3
% 21.84/3.67 % (2896331)Termination reason: Instruction limit
% 21.84/3.67 % (2896331)Termination phase: Saturation
% 21.84/3.67 % (2896331)Time elapsed: 0.268 s
% 21.84/3.67 % (2896331)Peak memory usage: 13 MB
% 21.84/3.67 % (2896331)Instructions burned: 477 (million)
% 21.84/3.67 % (2896385)fmb+10_1_sil=64000:random_seed=290972151:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 21.84/3.67 % (2896385)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 21.84/3.67 % Exception at run slice level
% 21.84/3.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.84/3.67 % (2896387)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1278574270:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 21.84/3.67 % (2896324)Instruction limit reached!
% 21.84/3.67 % (2896324)------------------------------
% 21.84/3.67 % (2896324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.84/3.67 % (2896324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.84/3.67 % (2896324)CaDiCaL version: 2.1.3
% 21.84/3.67 % (2896324)Termination reason: Instruction limit
% 21.84/3.67 % (2896324)Termination phase: Saturation
% 21.84/3.67 % (2896324)Time elapsed: 0.343 s
% 21.84/3.67 % (2896324)Peak memory usage: 14 MB
% 21.84/3.67 % (2896324)Instructions burned: 685 (million)
% 21.84/3.67 % Exception at run slice level
% 21.84/3.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.84/3.67 % (2896390)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3849522779:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 21.84/3.67 % (2896389)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=439926556:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 97.72/14.20 % Exception at run slice level
% 97.72/14.20 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 97.72/14.20 % (2896393)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2669243495:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 97.72/14.20 % (2896393)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 97.72/14.20 % (2896362)Instruction limit reached!
% 97.72/14.20 % (2896362)------------------------------
% 97.72/14.20 % (2896362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.72/14.20 % (2896362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.72/14.20 % (2896362)CaDiCaL version: 2.1.3
% 97.72/14.20 % (2896362)Termination reason: Instruction limit
% 97.72/14.20 % (2896362)Termination phase: Saturation
% 97.72/14.20 % (2896362)Time elapsed: 0.415 s
% 97.72/14.20 % (2896362)Peak memory usage: 15 MB
% 97.72/14.20 % (2896362)Instructions burned: 694 (million)
% 97.72/14.21 % (2896415)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1624615645:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 97.72/14.21 % Exception at run slice level
% 97.72/14.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 97.72/14.21 % (2896424)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2001034510:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 97.72/14.21 % Exception at run slice level
% 97.72/14.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 97.72/14.21 % (2896428)ott-2_1_sil=16000:newcnf=on:random_seed=1148587133:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi)
% 97.72/14.21 % (2896368)Instruction limit reached!
% 97.72/14.21 % (2896368)------------------------------
% 97.72/14.21 % (2896368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.72/14.21 % (2896368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.72/14.21 % (2896368)CaDiCaL version: 2.1.3
% 97.72/14.21 % (2896368)Termination reason: Instruction limit
% 97.72/14.21 % (2896368)Termination phase: Saturation
% 97.72/14.21 % (2896368)Time elapsed: 0.536 s
% 97.72/14.21 % (2896368)Peak memory usage: 18 MB
% 97.72/14.21 % (2896368)Instructions burned: 879 (million)
% 97.72/14.21 % (2896430)ott+10_1_sil=32000:tgt=ground:random_seed=2192981456:i=5114:av=off_2991 on theBenchmark for (2991ds/5114Mi)
% 97.72/14.21 % (2896346)Instruction limit reached!
% 97.72/14.21 % (2896346)------------------------------
% 97.72/14.21 % (2896346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.72/14.21 % (2896346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.72/14.21 % (2896346)CaDiCaL version: 2.1.3
% 97.72/14.21 % (2896346)Termination reason: Instruction limit
% 97.72/14.21 % (2896346)Termination phase: Saturation
% 97.72/14.21 % (2896346)Time elapsed: 0.702 s
% 97.72/14.21 % (2896346)Peak memory usage: 18 MB
% 97.72/14.21 % (2896346)Instructions burned: 1181 (million)
% 97.72/14.21 % (2896452)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2098980801:i=54282_2991 on theBenchmark for (2991ds/54282Mi)
% 97.72/14.21 % Exception at run slice level
% 97.72/14.21 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 97.72/14.21 % (2896470)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3170690300:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi)
% 97.72/14.21 % (2896428)Instruction limit reached!
% 97.72/14.21 % (2896428)------------------------------
% 97.72/14.21 % (2896428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.72/14.21 % (2896428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.72/14.21 % (2896428)CaDiCaL version: 2.1.3
% 97.72/14.21 % (2896428)Termination reason: Instruction limit
% 97.72/14.21 % (2896428)Termination phase: Saturation
% 97.72/14.21 % (2896428)Time elapsed: 0.381 s
% 97.72/14.21 % (2896428)Peak memory usage: 13 MB
% 97.72/14.21 % (2896428)Instructions burned: 869 (million)
% 97.72/14.21 % (2896541)dis+21_1_sil=32000:sas=cadical:random_seed=195991051:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 97.72/14.21 % (2896393)Instruction limit reached!
% 97.72/14.21 % (2896393)------------------------------
% 97.72/14.21 % (2896393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.98/19.35 % (2896393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.98/19.35 % (2896393)CaDiCaL version: 2.1.3
% 133.98/19.35 % (2896393)Termination reason: Instruction limit
% 133.98/19.35 % (2896393)Termination phase: Saturation
% 133.98/19.35 % (2896393)Time elapsed: 0.725 s
% 133.98/19.35 % (2896393)Peak memory usage: 16 MB
% 133.98/19.35 % (2896393)Instructions burned: 1474 (million)
% 133.98/19.35 % (2896543)ott+11_1_sil=16000:gs=on:random_seed=4144330339:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi)
% 133.98/19.35 % (2896543)Instruction limit reached!
% 133.98/19.35 % (2896543)------------------------------
% 133.98/19.35 % (2896543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.98/19.35 % (2896543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.98/19.35 % (2896543)CaDiCaL version: 2.1.3
% 133.98/19.35 % (2896543)Termination reason: Instruction limit
% 133.98/19.35 % (2896543)Termination phase: Saturation
% 133.98/19.35 % (2896543)Time elapsed: 1.152 s
% 133.98/19.35 % (2896543)Peak memory usage: 19 MB
% 133.98/19.35 % (2896543)Instructions burned: 2252 (million)
% 133.98/19.35 % (2896592)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=583729911:fmbsr=1.6:i=67534_2975 on theBenchmark for (2975ds/67534Mi)
% 133.98/19.35 % Exception at run slice level
% 133.98/19.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 133.98/19.35 % (2896594)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=590369377:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2975 on theBenchmark for (2975ds/4591Mi)
% 133.98/19.35 % (2896470)Instruction limit reached!
% 133.98/19.35 % (2896470)------------------------------
% 133.98/19.35 % (2896470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.98/19.35 % (2896470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.98/19.35 % (2896470)CaDiCaL version: 2.1.3
% 133.98/19.35 % (2896470)Termination reason: Instruction limit
% 133.98/19.35 % (2896470)Termination phase: Saturation
% 133.98/19.35 % (2896470)Time elapsed: 1.720 s
% 133.98/19.35 % (2896470)Peak memory usage: 20 MB
% 133.98/19.35 % (2896470)Instructions burned: 3513 (million)
% 133.98/19.35 % (2896596)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4198632457:i=29340_2973 on theBenchmark for (2973ds/29340Mi)
% 133.98/19.35 % (2896390)Instruction limit reached!
% 133.98/19.35 % (2896390)------------------------------
% 133.98/19.35 % (2896390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.98/19.35 % (2896390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.98/19.35 % (2896390)CaDiCaL version: 2.1.3
% 133.98/19.35 % (2896390)Termination reason: Instruction limit
% 133.98/19.35 % (2896390)Termination phase: Saturation
% 133.98/19.35 % (2896390)Time elapsed: 2.540 s
% 133.98/19.35 % (2896390)Peak memory usage: 23 MB
% 133.98/19.35 % (2896390)Instructions burned: 5132 (million)
% 133.98/19.35 % (2896598)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3840439265:i=5211_2969 on theBenchmark for (2969ds/5211Mi)
% 133.98/19.35 % (2896541)Instruction limit reached!
% 133.98/19.35 % (2896541)------------------------------
% 133.98/19.35 % (2896541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 133.98/19.35 % (2896541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.98/19.35 % (2896541)CaDiCaL version: 2.1.3
% 133.98/19.35 % (2896541)Termination reason: Instruction limit
% 133.98/19.35 % (2896541)Termination phase: Saturation
% 133.98/19.35 % (2896541)Time elapsed: 2.005 s
% 133.98/19.35 % (2896541)Peak memory usage: 28 MB
% 133.98/19.35 % (2896541)Instructions burned: 3774 (million)
% 133.98/19.35 % (2896600)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1379934186:i=5497:nm=2_2968 on theBenchmark for (2968ds/5497Mi)
% 133.98/19.35 % Exception at run slice level
% 133.98/19.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 133.98/19.35 % (2896602)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4024302028:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi)
% 133.98/19.35 % Exception at run slice level
% 133.98/19.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 133.98/19.35 % (2896604)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2011335487:i=14071_2967 on theBenchmark for (2967ds/14071Mi)
% 133.98/19.35 % Exception at run slice level
% 203.92/29.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 203.92/29.18 % (2896606)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2842283457:i=22565:add=on:rawr=on_2967 on theBenchmark for (2967ds/22565Mi)
% 203.92/29.18 % (2896430)Instruction limit reached!
% 203.92/29.18 % (2896430)------------------------------
% 203.92/29.18 % (2896430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.92/29.18 % (2896430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.92/29.18 % (2896430)CaDiCaL version: 2.1.3
% 203.92/29.18 % (2896430)Termination reason: Instruction limit
% 203.92/29.18 % (2896430)Termination phase: Saturation
% 203.92/29.18 % (2896430)Time elapsed: 2.599 s
% 203.92/29.18 % (2896430)Peak memory usage: 25 MB
% 203.92/29.18 % (2896430)Instructions burned: 5115 (million)
% 203.92/29.18 % (2896608)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1706827436:i=8173:av=off_2965 on theBenchmark for (2965ds/8173Mi)
% 203.92/29.18 % (2896594)Instruction limit reached!
% 203.92/29.18 % (2896594)------------------------------
% 203.92/29.18 % (2896594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.92/29.18 % (2896594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.92/29.18 % (2896594)CaDiCaL version: 2.1.3
% 203.92/29.18 % (2896594)Termination reason: Instruction limit
% 203.92/29.18 % (2896594)Termination phase: Saturation
% 203.92/29.18 % (2896594)Time elapsed: 2.210 s
% 203.92/29.18 % (2896594)Peak memory usage: 34 MB
% 203.92/29.18 % (2896594)Instructions burned: 4593 (million)
% 203.92/29.18 % (2896610)dis+10_16:1_sil=16000:random_seed=2662662429:i=9155:fsr=off_2953 on theBenchmark for (2953ds/9155Mi)
% 203.92/29.18 % (2896598)Instruction limit reached!
% 203.92/29.18 % (2896598)------------------------------
% 203.92/29.18 % (2896598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.92/29.18 % (2896598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.92/29.18 % (2896598)CaDiCaL version: 2.1.3
% 203.92/29.18 % (2896598)Termination reason: Instruction limit
% 203.92/29.18 % (2896598)Termination phase: Saturation
% 203.92/29.18 % (2896598)Time elapsed: 2.841 s
% 203.92/29.18 % (2896598)Peak memory usage: 45 MB
% 203.92/29.18 % (2896598)Instructions burned: 5211 (million)
% 203.92/29.18 % (2896612)ott-3_8_sil=64000:random_seed=2570064420:i=20139:bs=on_2941 on theBenchmark for (2941ds/20139Mi)
% 203.92/29.18 % (2896608)Instruction limit reached!
% 203.92/29.18 % (2896608)------------------------------
% 203.92/29.18 % (2896608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.92/29.18 % (2896608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.92/29.18 % (2896608)CaDiCaL version: 2.1.3
% 203.92/29.18 % (2896608)Termination reason: Instruction limit
% 203.92/29.18 % (2896608)Termination phase: Saturation
% 203.92/29.18 % (2896608)Time elapsed: 4.590 s
% 203.92/29.18 % (2896608)Peak memory usage: 95 MB
% 203.92/29.18 % (2896608)Instructions burned: 8174 (million)
% 203.92/29.18 % (2896614)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1722266144:fmbsr=2:i=32576_2919 on theBenchmark for (2919ds/32576Mi)
% 203.92/29.18 % Exception at run slice level
% 203.92/29.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 203.92/29.18 % (2896616)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2120018384:i=11404_2919 on theBenchmark for (2919ds/11404Mi)
% 203.92/29.18 % (2896610)Instruction limit reached!
% 203.92/29.18 % (2896610)------------------------------
% 203.92/29.18 % (2896610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.92/29.18 % (2896610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.92/29.18 % (2896610)CaDiCaL version: 2.1.3
% 203.92/29.18 % (2896610)Termination reason: Instruction limit
% 203.92/29.18 % (2896610)Termination phase: Saturation
% 203.92/29.18 % (2896610)Time elapsed: 4.911 s
% 203.92/29.18 % (2896610)Peak memory usage: 50 MB
% 203.92/29.18 % (2896610)Instructions burned: 9155 (million)
% 203.92/29.18 % (2896618)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3809704173:i=14134_2903 on theBenchmark for (2903ds/14134Mi)
% 203.92/29.18 % (2896606)Instruction limit reached!
% 203.92/29.18 % (2896606)------------------------------
% 203.92/29.18 % (2896606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.92/29.18 % (2896606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.92/29.18 % (2896606)CaDiCaL version: 2.1.3
% 226.39/32.39 % (2896606)Termination reason: Instruction limit
% 226.39/32.39 % (2896606)Termination phase: Saturation
% 226.39/32.39 % (2896606)Time elapsed: 10.520 s
% 226.39/32.39 % (2896606)Peak memory usage: 33 MB
% 226.39/32.39 % (2896606)Instructions burned: 22567 (million)
% 226.39/32.39 % (2896633)dis+33_16_sil=32000:sac=on:random_seed=3676794374:i=15851:nm=0_2862 on theBenchmark for (2862ds/15851Mi)
% 226.39/32.39 % (2896616)Instruction limit reached!
% 226.39/32.39 % (2896616)------------------------------
% 226.39/32.39 % (2896616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.39/32.39 % (2896616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.39/32.39 % (2896616)CaDiCaL version: 2.1.3
% 226.39/32.39 % (2896616)Termination reason: Instruction limit
% 226.39/32.39 % (2896616)Termination phase: Saturation
% 226.39/32.39 % (2896616)Time elapsed: 6.688 s
% 226.39/32.39 % (2896616)Peak memory usage: 64 MB
% 226.39/32.39 % (2896616)Instructions burned: 11404 (million)
% 226.39/32.39 % (2896836)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=562587793:avsq=on:i=17627:add=on:amm=off_2851 on theBenchmark for (2851ds/17627Mi)
% 226.39/32.39 % (2896612)Instruction limit reached!
% 226.39/32.39 % (2896612)------------------------------
% 226.39/32.39 % (2896612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.39/32.39 % (2896612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.39/32.39 % (2896612)CaDiCaL version: 2.1.3
% 226.39/32.39 % (2896612)Termination reason: Instruction limit
% 226.39/32.39 % (2896612)Termination phase: Saturation
% 226.39/32.39 % (2896612)Time elapsed: 10.069 s
% 226.39/32.39 % (2896612)Peak memory usage: 28 MB
% 226.39/32.39 % (2896612)Instructions burned: 20139 (million)
% 226.39/32.39 % (2896913)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=972981503:s2a=on:i=53295_2840 on theBenchmark for (2840ds/53295Mi)
% 226.39/32.39 % (2896596)Instruction limit reached!
% 226.39/32.39 % (2896596)------------------------------
% 226.39/32.39 % (2896596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.39/32.39 % (2896596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.39/32.39 % (2896596)CaDiCaL version: 2.1.3
% 226.39/32.39 % (2896596)Termination reason: Instruction limit
% 226.39/32.39 % (2896596)Termination phase: Saturation
% 226.39/32.39 % (2896596)Time elapsed: 13.938 s
% 226.39/32.39 % (2896596)Peak memory usage: 48 MB
% 226.39/32.39 % (2896596)Instructions burned: 29341 (million)
% 226.39/32.39 % (2896928)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1243367257:i=26857:ins=20_2833 on theBenchmark for (2833ds/26857Mi)
% 226.39/32.39 % Exception at run slice level
% 226.39/32.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 226.39/32.39 % (2896930)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1368821445:i=28120:bs=on:fsr=off_2833 on theBenchmark for (2833ds/28120Mi)
% 226.39/32.39 % (2896618)Instruction limit reached!
% 226.39/32.39 % (2896618)------------------------------
% 226.39/32.39 % (2896618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 226.39/32.39 % (2896618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.39/32.39 % (2896618)CaDiCaL version: 2.1.3
% 226.39/32.39 % (2896618)Termination reason: Instruction limit
% 226.39/32.39 % (2896618)Termination phase: Saturation
% 226.39/32.39 % (2896618)Time elapsed: 9.146 s
% 226.39/32.39 % (2896618)Peak memory usage: 47 MB
% 226.39/32.39 % (2896618)Instructions burned: 14134 (million)
% 226.39/32.39 % (2896940)fmb+10_1_sil=256000:fmbss=7:random_seed=3236680062:fmbsr=1.6:i=182295_2812 on theBenchmark for (2812ds/182295Mi)
% 226.39/32.39 % Exception at run slice level
% 226.39/32.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 226.39/32.39 % (2896942)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=369829523:i=44625:gsp=on_2811 on theBenchmark for (2811ds/44625Mi)
% 226.39/32.39 % (2896942)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 226.39/32.39 % Exception at run slice level
% 226.39/32.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 226.39/32.39 % (2896944)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=3701176493:i=160505_2811 on theBenchmark for (2811ds/160505Mi)
% 226.39/32.39 % Exception at run slice level
% 226.39/32.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 226.39/32.39 % (2896946)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=203639810:fmbsr=1.3:i=225729_2810 on theBenchmark for (2810ds/225729Mi)
% 251.02/35.86 % Exception at run slice level
% 251.02/35.86 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 251.02/35.86 % (2896948)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3025133762:fmbsr=2:i=185024:ins=7_2810 on theBenchmark for (2810ds/185024Mi)
% 251.02/35.86 % Exception at run slice level
% 251.02/35.86 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 251.02/35.86 % (2896950)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2519673535:rtra=on_2810 on theBenchmark for (2810ds/0Mi)
% 251.02/35.86 % Exception at run slice level
% 251.02/35.86 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 251.02/35.86 % (2896952)% WARNING: option uhcvi not known.
% 251.02/35.86 % (2896952)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1717227659:i=271062:add=off:rtra=on:rawr=on_2809 on theBenchmark for (2809ds/271062Mi)
% 251.02/35.86 % (2896633)Instruction limit reached!
% 251.02/35.86 % (2896633)------------------------------
% 251.02/35.86 % (2896633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 251.02/35.86 % (2896633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 251.02/35.86 % (2896633)CaDiCaL version: 2.1.3
% 251.02/35.86 % (2896633)Termination reason: Instruction limit
% 251.02/35.86 % (2896633)Termination phase: Saturation
% 251.02/35.86 % (2896633)Time elapsed: 10.491 s
% 251.02/35.86 % (2896633)Peak memory usage: 22 MB
% 251.02/35.86 % (2896633)Instructions burned: 15851 (million)
% 251.02/35.86 % (2896972)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2356318502:i=176048:add=on:rtra=on:rawr=on_2756 on theBenchmark for (2756ds/176048Mi)
% 251.02/35.86 % (2896836)Instruction limit reached!
% 251.02/35.86 % (2896836)------------------------------
% 251.02/35.86 % (2896836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 251.02/35.86 % (2896836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 251.02/35.86 % (2896836)CaDiCaL version: 2.1.3
% 251.02/35.86 % (2896836)Termination reason: Instruction limit
% 251.02/35.86 % (2896836)Termination phase: Saturation
% 251.02/35.86 % (2896836)Time elapsed: 13.171 s
% 251.02/35.86 % (2896836)Peak memory usage: 30 MB
% 251.02/35.86 % (2896836)Instructions burned: 17628 (million)
% 251.02/35.86 % (2896978)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3396270218:i=206:fgj=on:rtra=on_2720 on theBenchmark for (2720ds/206Mi)
% 251.02/35.86 % (2896978)Instruction limit reached!
% 251.02/35.86 % (2896978)------------------------------
% 251.02/35.86 % (2896978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 251.02/35.86 % (2896978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 251.02/35.86 % (2896978)CaDiCaL version: 2.1.3
% 251.02/35.86 % (2896978)Termination reason: Instruction limit
% 251.02/35.86 % (2896978)Termination phase: Saturation
% 251.02/35.86 % (2896978)Time elapsed: 0.180 s
% 251.02/35.86 % (2896978)Peak memory usage: 13 MB
% 251.02/35.86 % (2896978)Instructions burned: 206 (million)
% 251.02/35.86 % (2896980)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3345614510:i=232:rtra=on_2717 on theBenchmark for (2717ds/232Mi)
% 251.02/35.86 % (2896980)Instruction limit reached!
% 251.02/35.86 % (2896980)------------------------------
% 251.02/35.86 % (2896980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 251.02/35.86 % (2896980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 251.02/35.86 % (2896980)CaDiCaL version: 2.1.3
% 251.02/35.86 % (2896980)Termination reason: Instruction limit
% 251.02/35.86 % (2896980)Termination phase: Saturation
% 251.02/35.86 % (2896980)Time elapsed: 0.225 s
% 251.02/35.86 % (2896980)Peak memory usage: 13 MB
% 251.02/35.86 % (2896980)Instructions burned: 232 (million)
% 251.02/35.86 % (2896982)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2029421187:i=262:rtra=on_2715 on theBenchmark for (2715ds/262Mi)
% 251.02/35.86 % (2896982)Instruction limit reached!
% 251.02/35.86 % (2896982)------------------------------
% 251.02/35.86 % (2896982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 251.02/35.86 % (2896982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 251.02/35.86 % (2896982)CaDiCaL version: 2.1.3
% 251.02/35.86 % (2896982)Termination reason: Instruction limit
% 251.02/35.86 % (2896982)Termination phase: Saturation
% 212.30/37.80 % (2896982)Time elapsed: 0.276 s
% 212.30/37.80 % (2896982)Peak memory usage: 13 MB
% 212.30/37.80 % (2896982)Instructions burned: 263 (million)
% 212.30/37.80 % (2896984)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2306453224:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2712 on theBenchmark for (2712ds/318Mi)
% 212.30/37.80 % (2896984)Instruction limit reached!
% 212.30/37.80 % (2896984)------------------------------
% 212.30/37.80 % (2896984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 212.30/37.80 % (2896984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.30/37.80 % (2896984)CaDiCaL version: 2.1.3
% 212.30/37.80 % (2896984)Termination reason: Instruction limit
% 212.30/37.80 % (2896984)Termination phase: Saturation
% 212.30/37.80 % (2896984)Time elapsed: 0.287 s
% 212.30/37.80 % (2896984)Peak memory usage: 13 MB
% 212.30/37.80 % (2896984)Instructions burned: 318 (million)
% 212.30/37.80 % (2896988)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3940383747:i=1428:nm=2:rtra=on_2709 on theBenchmark for (2709ds/1428Mi)
% 212.30/37.80 % Exception at run slice level
% 212.30/37.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 212.30/37.80 % (2896990)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2121468735:i=262:bd=preordered:rtra=on:fsd=on_2708 on theBenchmark for (2708ds/262Mi)
% 212.30/37.80 % (2896990)Instruction limit reached!
% 212.30/37.80 % (2896990)------------------------------
% 212.30/37.80 % (2896990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 212.30/37.80 % (2896990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.30/37.80 % (2896990)CaDiCaL version: 2.1.3
% 212.30/37.80 % (2896990)Termination reason: Instruction limit
% 212.30/37.80 % (2896990)Termination phase: Saturation
% 212.30/37.80 % (2896990)Time elapsed: 0.247 s
% 212.30/37.80 % (2896990)Peak memory usage: 13 MB
% 212.30/37.80 % (2896990)Instructions burned: 262 (million)
% 212.30/37.80 % (2896992)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2028932273:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2705 on theBenchmark for (2705ds/1368Mi)
% 212.30/37.80 % (2896992)Instruction limit reached!
% 212.30/37.80 % (2896992)------------------------------
% 212.30/37.80 % (2896992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 212.30/37.80 % (2896992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.30/37.80 % (2896992)CaDiCaL version: 2.1.3
% 212.30/37.80 % (2896992)Termination reason: Instruction limit
% 212.30/37.80 % (2896992)Termination phase: Saturation
% 212.30/37.80 % (2896992)Time elapsed: 1.183 s
% 212.30/37.80 % (2896992)Peak memory usage: 16 MB
% 212.30/37.80 % (2896992)Instructions burned: 1368 (million)
% 212.30/37.80 % (2896994)ott-21_1_sil=16000:si=on:fs=off:random_seed=3263718240:i=360:av=off:fsr=off:rtra=on_2693 on theBenchmark for (2693ds/360Mi)
% 212.30/37.80 % (2896994)Instruction limit reached!
% 212.30/37.80 % (2896994)------------------------------
% 212.30/37.80 % (2896994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 212.30/37.80 % (2896994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.30/37.80 % (2896994)CaDiCaL version: 2.1.3
% 212.30/37.80 % (2896994)Termination reason: Instruction limit
% 212.30/37.80 % (2896994)Termination phase: Saturation
% 212.30/37.80 % (2896994)Time elapsed: 0.328 s
% 212.30/37.80 % (2896994)Peak memory usage: 13 MB
% 212.30/37.80 % (2896994)Instructions burned: 361 (million)
% 212.30/37.80 % (2896998)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1771895441:i=954:bd=all:rtra=on_2690 on theBenchmark for (2690ds/954Mi)
% 212.30/37.80 % (2896998)Instruction limit reached!
% 212.30/37.80 % (2896998)------------------------------
% 212.30/37.80 % (2896998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 212.30/37.80 % (2896998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.30/37.80 % (2896998)CaDiCaL version: 2.1.3
% 212.30/37.80 % (2896998)Termination reason: Instruction limit
% 212.30/37.80 % (2896998)Termination phase: Saturation
% 212.30/37.80 % (2896998)Time elapsed: 0.913 s
% 212.30/37.80 % (2896998)Peak memory usage: 15 MB
% 212.30/37.80 % (2896998)Instructions burned: 954 (million)
% 212.30/37.80 % (2897000)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2573977803:fmbsr=1.3:i=1730:ins=25:rtra=on_2680 on theBenchmark for (2680ds/1730Mi)
% 212.30/37.80 % Exception at run slice level
% 212.30/37.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 212.30/37.80 % (2897002)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=1513278113:i=2358:rtra=on_2680 on theBenchmark for (2680ds/2358Mi)
% 212.30/37.80 % (2896930)Instruction limit reached!
% 212.30/37.80 % (2896930)------------------------------
% 212.30/37.80 % (2896930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 212.30/37.80 % (2896930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.30/37.80 % (2896930)CaDiCaL version: 2.1.3
% 212.30/37.80 % (2896930)Termination reason: Instruction limit
% 212.30/37.80 % (2896930)Termination phase: Saturation
% 212.30/37.80 % (2896930)Time elapsed: 17.0000 s
% 212.30/37.80 % (2896930)Peak memory usage: 21 MB
% 212.30/37.80 % (2896930)Instructions burned: 28120 (million)
% 212.30/37.80 % (2897004)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2150567740:i=1778:ins=1:rtra=on_2663 on theBenchmark for (2663ds/1778Mi)
% 212.30/37.80 % Exception at run slice level
% 212.30/37.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 212.30/37.80 % (2897006)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3584239039:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2662 on theBenchmark for (2662ds/1384Mi)
% 212.30/37.80 % (2897002)Instruction limit reached!
% 212.30/37.80 % (2897002)------------------------------
% 212.30/37.80 % (2897002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 212.30/37.80 % (2897002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.30/37.80 % (2897002)CaDiCaL version: 2.1.3
% 212.30/37.80 % (2897002)Termination reason: Instruction limit
% 212.30/37.80 % (2897002)Termination phase: Saturation
% 212.30/37.80 % (2897002)Time elapsed: 1.823 s
% 212.30/37.80 % (2897002)Peak memory usage: 20 MB
% 212.30/37.80 % (2897002)Instructions burned: 2358 (million)
% 212.30/37.80 % (2897008)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=545232651:i=1758:kws=inv_precedence:fsr=off:rtra=on_2661 on theBenchmark for (2661ds/1758Mi)
% 212.30/37.80 % (2897006)Instruction limit reached!
% 212.30/37.80 % (2897006)------------------------------
% 212.30/37.80 % (2897006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 212.30/37.80 % (2897006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.30/37.80 % (2897006)CaDiCaL version: 2.1.3
% 212.30/37.80 % (2897006)Termination reason: Instruction limit
% 212.30/37.80 % (2897006)Termination phase: Saturation
% 212.30/37.80 % (2897006)Time elapsed: 1.240 s
% 212.30/37.80 % (2897006)Peak memory usage: 17 MB
% 212.30/37.80 % (2897006)Instructions burned: 1385 (million)
% 212.30/37.80 % (2897010)fmb+10_1_sil=64000:si=on:random_seed=3452424440:i=44122:nm=2:rtra=on:gsp=on_2649 on theBenchmark for (2649ds/44122Mi)
% 212.30/37.80 % (2897010)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 212.30/37.80 % Exception at run slice level
% 212.30/37.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 212.30/37.80 % (2897012)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2770947373:i=19030:nm=5:rtra=on_2649 on theBenchmark for (2649ds/19030Mi)
% 212.30/37.80 % Exception at run slice level
% 212.30/37.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 212.30/37.80 % (2897014)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=2721232478:fmbsr=1.7:i=1840:rtra=on_2649 on theBenchmark for (2649ds/1840Mi)
% 212.30/37.80 % Exception at run slice level
% 212.30/37.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 212.30/37.80 % (2897016)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3546715007:i=10262:rtra=on_2648 on theBenchmark for (2648ds/10262Mi)
% 212.30/37.80 % (2897008)Instruction limit reached!
% 212.30/37.80 % (2897008)------------------------------
% 212.30/37.80 % (2897008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 212.30/37.80 % (2897008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.30/37.80 % (2897008)CaDiCaL version: 2.1.3
% 212.30/37.80 % (2897008)Termination reason: Instruction limit
% 212.30/37.80 % (2897008)Termination phase: Saturation
% 212.30/37.80 % (2897008)Time elapsed: 1.589 s
% 212.30/37.80 % (2897008)Peak memory usage: 25 MB
% 212.30/37.80 % (2897008)Instructions burned: 1759 (million)
% 212.30/37.80 % (2897018)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2479183410:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2645 on theBenchmark for (2645ds/2944Mi)
% 212.30/37.80 % (2897018)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 212.30/37.80 % (2896952) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2896256-2896952"...
% 212.30/37.80 % (2896952)...printing done.
% 212.30/37.80 % (2896952)Refutation found. Thanks to Tanya!
% 212.30/37.80 % SZS status Theorem for theBenchmark
% 212.30/37.80 % SZS output start Proof for theBenchmark
% See solution above
% 212.30/37.81 % (2896952)------------------------------
% 212.30/37.81 % (2896952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 212.30/37.81 % (2896952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.30/37.81 % (2896952)CaDiCaL version: 2.1.3
% 212.30/37.81 % (2896952)Termination reason: Refutation
% 212.30/37.81 % (2896952)Time elapsed: 18.271 s
% 212.30/37.81 % (2896952)Peak memory usage: 64 MB
% 212.30/37.81 % (2896952)Instructions burned: 18934 (million)
% 212.30/37.81 % (2896256)Success in time 37.387 s
% 212.30/37.81 % Vampire exiting
%------------------------------------------------------------------------------