%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP005^5 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:07:38 AM UTC 2026
% Result : Theorem 14.96s 3.28s
% Output : Refutation 14.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 6
% Syntax : Number of formulae : 42 ( 18 unt; 0 typ; 2 def)
% Number of atoms : 112 ( 41 equ; 0 cnn)
% Maximal formula atoms : 3 ( 2 avg)
% Number of connectives : 366 ( 22 ~; 14 |; 3 &; 318 @)
% ( 2 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 10 ( 8 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 746 ( 743 usr; 15 con; 0-5 aty)
% Number of variables : 60 ( 0 sgn 54 !; 6 ?; 60 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
del: $tType ).
thf(type_def_6,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(type_def_7,type,
tp__i: $tType ).
thf(type_def_8,type,
tp__ty_2Enum_2Enum: $tType ).
thf(type_def_9,type,
tp__ty_2Eone_2Eone: $tType ).
thf(type_def_10,type,
tp__c_ty_2Eoption_2Eoption_ty_2Eone_2Eone: $tType ).
thf(type_def_11,type,
tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum: $tType ).
thf(type_def_12,type,
tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum: $tType ).
thf(type_def_13,type,
tp__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum: $tType ).
thf(func_def_0,type,
bool: del ).
thf(func_def_1,type,
ind: del ).
thf(func_def_2,type,
arr: del > del > del ).
thf(func_def_3,type,
mem: $i > del > $o ).
thf(func_def_4,type,
ap: $i > $i > $i ).
thf(func_def_5,type,
lam: del > ( $i > $i ) > $i ).
thf(func_def_6,type,
p: $i > $o ).
thf(func_def_7,type,
inj__o: $o > $i ).
thf(func_def_9,type,
c_2Emin_2E_3D: del > $i ).
thf(func_def_11,type,
c_2Emin_2E_40: del > $i ).
thf(func_def_12,type,
ty_2Ebool_2Eitself: del > del ).
thf(func_def_13,type,
c_2Ebool_2E_21: del > $i ).
thf(func_def_15,type,
c_2Ebool_2E_3F: del > $i ).
thf(func_def_16,type,
c_2Ebool_2E_3F_21: del > $i ).
thf(func_def_17,type,
c_2Ebool_2EARB: del > $i ).
thf(func_def_19,type,
c_2Ebool_2ECOND: del > $i ).
thf(func_def_20,type,
c_2Ebool_2EDATATYPE: del > $i ).
thf(func_def_22,type,
c_2Ebool_2EIN: del > $i ).
thf(func_def_23,type,
c_2Ebool_2ELET: del > del > $i ).
thf(func_def_24,type,
c_2Ebool_2EONE__ONE: del > del > $i ).
thf(func_def_25,type,
c_2Ebool_2EONTO: del > del > $i ).
thf(func_def_26,type,
c_2Ebool_2ERES__ABSTRACT: del > del > $i ).
thf(func_def_27,type,
c_2Ebool_2ERES__EXISTS: del > $i ).
thf(func_def_28,type,
c_2Ebool_2ERES__EXISTS__UNIQUE: del > $i ).
thf(func_def_29,type,
c_2Ebool_2ERES__FORALL: del > $i ).
thf(func_def_30,type,
c_2Ebool_2ERES__SELECT: del > $i ).
thf(func_def_32,type,
c_2Ebool_2ETYPE__DEFINITION: del > del > $i ).
thf(func_def_34,type,
c_2Ebool_2Eitself__case: del > del > $i ).
thf(func_def_35,type,
c_2Ebool_2Eliteral__case: del > del > $i ).
thf(func_def_36,type,
c_2Ebool_2Ethe__value: del > $i ).
thf(func_def_38,type,
inj__i: tp__i > $i ).
thf(func_def_39,type,
surj__i: $i > tp__i ).
thf(func_def_41,type,
c_2EnormalForms_2EEXT__POINT: del > del > $i ).
thf(func_def_42,type,
c_2EnormalForms_2EUNIV__POINT: del > $i ).
thf(func_def_48,type,
c_2Emarker_2Estmarker: del > $i ).
thf(func_def_49,type,
c_2Emarker_2Eunint: del > $i ).
thf(func_def_50,type,
c_2Ecombin_2E_3A_3E: del > del > $i ).
thf(func_def_51,type,
c_2Ecombin_2EASSOC: del > $i ).
thf(func_def_52,type,
c_2Ecombin_2EC: del > del > del > $i ).
thf(func_def_53,type,
c_2Ecombin_2ECOMM: del > del > $i ).
thf(func_def_54,type,
c_2Ecombin_2EFAIL: del > del > $i ).
thf(func_def_55,type,
c_2Ecombin_2EFCOMM: del > del > del > $i ).
thf(func_def_56,type,
c_2Ecombin_2EI: del > $i ).
thf(func_def_57,type,
c_2Ecombin_2EK: del > del > $i ).
thf(func_def_58,type,
c_2Ecombin_2ELEFT__ID: del > del > $i ).
thf(func_def_59,type,
c_2Ecombin_2EMONOID: del > $i ).
thf(func_def_60,type,
c_2Ecombin_2ERIGHT__ID: del > del > $i ).
thf(func_def_61,type,
c_2Ecombin_2ES: del > del > del > $i ).
thf(func_def_62,type,
c_2Ecombin_2EUPDATE: del > del > $i ).
thf(func_def_63,type,
c_2Ecombin_2EW: del > del > $i ).
thf(func_def_64,type,
c_2Ecombin_2Eo: del > del > del > $i ).
thf(func_def_65,type,
ty_2Enum_2Enum: del ).
thf(func_def_66,type,
inj__ty_2Enum_2Enum: tp__ty_2Enum_2Enum > $i ).
thf(func_def_67,type,
surj__ty_2Enum_2Enum: $i > tp__ty_2Enum_2Enum ).
thf(func_def_69,type,
fo__c_2Enum_2E0: tp__ty_2Enum_2Enum ).
thf(func_def_71,type,
fo__c_2Enum_2EABS__num: tp__i > tp__ty_2Enum_2Enum ).
thf(func_def_74,type,
fo__c_2Enum_2EREP__num: tp__ty_2Enum_2Enum > tp__i ).
thf(func_def_76,type,
fo__c_2Enum_2ESUC: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_78,type,
fo__c_2Enum_2ESUC__REP: tp__i > tp__i ).
thf(func_def_80,type,
fo__c_2Enum_2EZERO__REP: tp__i ).
thf(func_def_81,type,
ty_2Eone_2Eone: del ).
thf(func_def_82,type,
inj__ty_2Eone_2Eone: tp__ty_2Eone_2Eone > $i ).
thf(func_def_83,type,
surj__ty_2Eone_2Eone: $i > tp__ty_2Eone_2Eone ).
thf(func_def_85,type,
fo__c_2Eone_2Eone: tp__ty_2Eone_2Eone ).
thf(func_def_86,type,
c_2Eone_2Eone__CASE: del > $i ).
thf(func_def_87,type,
ty_2Esum_2Esum: del > del > del ).
thf(func_def_88,type,
c_2Esum_2E_2B_2B: del > del > del > del > $i ).
thf(func_def_89,type,
c_2Esum_2EABS__sum: del > del > $i ).
thf(func_def_90,type,
c_2Esum_2EINL: del > del > $i ).
thf(func_def_91,type,
c_2Esum_2EINR: del > del > $i ).
thf(func_def_92,type,
c_2Esum_2EISL: del > del > $i ).
thf(func_def_93,type,
c_2Esum_2EISR: del > del > $i ).
thf(func_def_94,type,
c_2Esum_2EIS__SUM__REP: del > del > $i ).
thf(func_def_95,type,
c_2Esum_2EOUTL: del > del > $i ).
thf(func_def_96,type,
c_2Esum_2EOUTR: del > del > $i ).
thf(func_def_97,type,
c_2Esum_2EREP__sum: del > del > $i ).
thf(func_def_98,type,
c_2Esum_2ESUM__ALL: del > del > $i ).
thf(func_def_99,type,
c_2Esum_2Esum__CASE: del > del > del > $i ).
thf(func_def_100,type,
c_2Erelation_2ECR: del > $i ).
thf(func_def_101,type,
c_2Erelation_2EEMPTY__REL: del > $i ).
thf(func_def_102,type,
c_2Erelation_2EEQC: del > $i ).
thf(func_def_103,type,
c_2Erelation_2EIDEM: del > $i ).
thf(func_def_104,type,
c_2Erelation_2EINDUCTIVE__INVARIANT: del > del > $i ).
thf(func_def_105,type,
c_2Erelation_2EINDUCTIVE__INVARIANT__ON: del > del > $i ).
thf(func_def_106,type,
c_2Erelation_2EINVOL: del > $i ).
thf(func_def_107,type,
c_2Erelation_2ELinearOrder: del > $i ).
thf(func_def_108,type,
c_2Erelation_2EO: del > del > del > $i ).
thf(func_def_109,type,
c_2Erelation_2EOrder: del > $i ).
thf(func_def_110,type,
c_2Erelation_2EPreOrder: del > $i ).
thf(func_def_111,type,
c_2Erelation_2ERC: del > $i ).
thf(func_def_112,type,
c_2Erelation_2ERCOMPL: del > del > $i ).
thf(func_def_113,type,
c_2Erelation_2ERDOM: del > del > $i ).
thf(func_def_114,type,
c_2Erelation_2ERDOM__DELETE: del > del > $i ).
thf(func_def_115,type,
c_2Erelation_2ERESTRICT: del > del > $i ).
thf(func_def_116,type,
c_2Erelation_2ERINTER: del > del > $i ).
thf(func_def_117,type,
c_2Erelation_2ERRANGE: del > del > $i ).
thf(func_def_118,type,
c_2Erelation_2ERRESTRICT: del > del > $i ).
thf(func_def_119,type,
c_2Erelation_2ERSUBSET: del > del > $i ).
thf(func_def_120,type,
c_2Erelation_2ERTC: del > $i ).
thf(func_def_121,type,
c_2Erelation_2ERUNION: del > del > $i ).
thf(func_def_122,type,
c_2Erelation_2ERUNIV: del > del > $i ).
thf(func_def_123,type,
c_2Erelation_2ESC: del > $i ).
thf(func_def_124,type,
c_2Erelation_2ESN: del > $i ).
thf(func_def_125,type,
c_2Erelation_2ESTRORD: del > $i ).
thf(func_def_126,type,
c_2Erelation_2EStrongLinearOrder: del > $i ).
thf(func_def_127,type,
c_2Erelation_2EStrongOrder: del > $i ).
thf(func_def_128,type,
c_2Erelation_2ETC: del > $i ).
thf(func_def_129,type,
c_2Erelation_2EWCR: del > $i ).
thf(func_def_130,type,
c_2Erelation_2EWF: del > $i ).
thf(func_def_131,type,
c_2Erelation_2EWFP: del > $i ).
thf(func_def_132,type,
c_2Erelation_2EWFREC: del > del > $i ).
thf(func_def_133,type,
c_2Erelation_2EWeakLinearOrder: del > $i ).
thf(func_def_134,type,
c_2Erelation_2EWeakOrder: del > $i ).
thf(func_def_135,type,
c_2Erelation_2Eantisymmetric: del > $i ).
thf(func_def_136,type,
c_2Erelation_2Eapprox: del > del > $i ).
thf(func_def_137,type,
c_2Erelation_2Ediag: del > $i ).
thf(func_def_138,type,
c_2Erelation_2Ediamond: del > $i ).
thf(func_def_139,type,
c_2Erelation_2Eequivalence: del > $i ).
thf(func_def_140,type,
c_2Erelation_2Einv: del > del > $i ).
thf(func_def_141,type,
c_2Erelation_2Einv__image: del > del > $i ).
thf(func_def_142,type,
c_2Erelation_2Eirreflexive: del > $i ).
thf(func_def_143,type,
c_2Erelation_2Enf: del > del > $i ).
thf(func_def_144,type,
c_2Erelation_2Ercdiamond: del > $i ).
thf(func_def_145,type,
c_2Erelation_2Ereflexive: del > $i ).
thf(func_def_146,type,
c_2Erelation_2Esymmetric: del > $i ).
thf(func_def_147,type,
c_2Erelation_2Ethe__fun: del > del > $i ).
thf(func_def_148,type,
c_2Erelation_2Etotal: del > $i ).
thf(func_def_149,type,
c_2Erelation_2Etransitive: del > $i ).
thf(func_def_150,type,
c_2Erelation_2Etrichotomous: del > $i ).
thf(func_def_151,type,
ty_2Eoption_2Eoption: del > del ).
thf(func_def_152,type,
c_2Eoption_2EIS__NONE: del > $i ).
thf(func_def_153,type,
c_2Eoption_2EIS__SOME: del > $i ).
thf(func_def_154,type,
c_2Eoption_2ENONE: del > $i ).
thf(func_def_155,type,
c_2Eoption_2EOPTION__ALL: del > $i ).
thf(func_def_156,type,
c_2Eoption_2EOPTION__APPLY: del > del > $i ).
thf(func_def_157,type,
c_2Eoption_2EOPTION__BIND: del > del > $i ).
thf(func_def_158,type,
c_2Eoption_2EOPTION__CHOICE: del > $i ).
thf(func_def_159,type,
inj__c_ty_2Eoption_2Eoption_ty_2Eone_2Eone: tp__c_ty_2Eoption_2Eoption_ty_2Eone_2Eone > $i ).
thf(func_def_160,type,
surj__c_ty_2Eoption_2Eoption_ty_2Eone_2Eone: $i > tp__c_ty_2Eoption_2Eoption_ty_2Eone_2Eone ).
thf(func_def_162,type,
c_2Eoption_2EOPTION__IGNORE__BIND: del > del > $i ).
thf(func_def_163,type,
c_2Eoption_2EOPTION__JOIN: del > $i ).
thf(func_def_164,type,
c_2Eoption_2EOPTION__MAP: del > del > $i ).
thf(func_def_165,type,
c_2Eoption_2EOPTION__MAP2: del > del > del > $i ).
thf(func_def_166,type,
c_2Eoption_2EOPTION__MCOMP: del > del > del > $i ).
thf(func_def_167,type,
c_2Eoption_2EOPTREL: del > del > $i ).
thf(func_def_168,type,
c_2Eoption_2ESOME: del > $i ).
thf(func_def_169,type,
c_2Eoption_2ETHE: del > $i ).
thf(func_def_170,type,
c_2Eoption_2Eoption__ABS: del > $i ).
thf(func_def_171,type,
c_2Eoption_2Eoption__CASE: del > del > $i ).
thf(func_def_172,type,
c_2Eoption_2Eoption__REP: del > $i ).
thf(func_def_173,type,
c_2Eoption_2Esome: del > $i ).
thf(func_def_174,type,
ty_2Epair_2Eprod: del > del > del ).
thf(func_def_175,type,
c_2Epair_2E_23_23: del > del > del > del > $i ).
thf(func_def_176,type,
c_2Epair_2E_2C: del > del > $i ).
thf(func_def_177,type,
c_2Epair_2EABS__prod: del > del > $i ).
thf(func_def_178,type,
c_2Epair_2ECURRY: del > del > del > $i ).
thf(func_def_179,type,
c_2Epair_2EFST: del > del > $i ).
thf(func_def_180,type,
c_2Epair_2ELEX: del > del > $i ).
thf(func_def_181,type,
c_2Epair_2EPROD__ALL: del > del > $i ).
thf(func_def_182,type,
c_2Epair_2EREP__prod: del > del > $i ).
thf(func_def_183,type,
c_2Epair_2ERPROD: del > del > $i ).
thf(func_def_184,type,
c_2Epair_2ESND: del > del > $i ).
thf(func_def_185,type,
c_2Epair_2ESWAP: del > del > $i ).
thf(func_def_186,type,
c_2Epair_2EUNCURRY: del > del > del > $i ).
thf(func_def_187,type,
c_2Epair_2Epair__CASE: del > del > del > $i ).
thf(func_def_190,type,
fo__c_2Eprim__rec_2EPRE: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_191,type,
c_2Eprim__rec_2EPRIM__REC: del > $i ).
thf(func_def_192,type,
c_2Eprim__rec_2EPRIM__REC__FUN: del > $i ).
thf(func_def_193,type,
c_2Eprim__rec_2ESIMP__REC: del > $i ).
thf(func_def_194,type,
c_2Eprim__rec_2ESIMP__REC__REL: del > $i ).
thf(func_def_195,type,
c_2Eprim__rec_2Emeasure: del > $i ).
thf(func_def_196,type,
c_2Eprim__rec_2Ewellfounded: del > $i ).
thf(func_def_197,type,
c_2Eposet_2Ebottom: del > $i ).
thf(func_def_198,type,
c_2Eposet_2Ecarrier: del > $i ).
thf(func_def_199,type,
c_2Eposet_2Echain: del > $i ).
thf(func_def_200,type,
c_2Eposet_2Ecomplete: del > $i ).
thf(func_def_201,type,
c_2Eposet_2Econtinuous: del > $i ).
thf(func_def_202,type,
c_2Eposet_2Edown__continuous: del > $i ).
thf(func_def_203,type,
c_2Eposet_2Efunction: del > del > $i ).
thf(func_def_204,type,
c_2Eposet_2Egfp: del > $i ).
thf(func_def_205,type,
c_2Eposet_2Eglb: del > $i ).
thf(func_def_206,type,
c_2Eposet_2Elfp: del > $i ).
thf(func_def_207,type,
c_2Eposet_2Elub: del > $i ).
thf(func_def_208,type,
c_2Eposet_2Emonotonic: del > $i ).
thf(func_def_209,type,
c_2Eposet_2Epointwise__lift: del > del > $i ).
thf(func_def_210,type,
c_2Eposet_2Eposet: del > $i ).
thf(func_def_211,type,
c_2Eposet_2Erelation: del > $i ).
thf(func_def_212,type,
c_2Eposet_2Etop: del > $i ).
thf(func_def_213,type,
c_2Eposet_2Eup__continuous: del > $i ).
thf(func_def_215,type,
fo__c_2Earithmetic_2E_2A: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_217,type,
fo__c_2Earithmetic_2E_2B: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_219,type,
fo__c_2Earithmetic_2E_2D: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_224,type,
fo__c_2Earithmetic_2EABS__DIFF: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_226,type,
fo__c_2Earithmetic_2EBIT1: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_228,type,
fo__c_2Earithmetic_2EBIT2: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_230,type,
fo__c_2Earithmetic_2EDIV: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_232,type,
fo__c_2Earithmetic_2EDIV2: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_233,type,
inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum: tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > $i ).
thf(func_def_234,type,
surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum: $i > tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum ).
thf(func_def_235,type,
inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum: tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > $i ).
thf(func_def_236,type,
surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum: $i > tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum ).
thf(func_def_240,type,
fo__c_2Earithmetic_2EEXP: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_242,type,
fo__c_2Earithmetic_2EFACT: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_243,type,
c_2Earithmetic_2EFUNPOW: del > $i ).
thf(func_def_245,type,
fo__c_2Earithmetic_2EMAX: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_247,type,
fo__c_2Earithmetic_2EMIN: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_249,type,
fo__c_2Earithmetic_2EMOD: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_251,type,
c_2Earithmetic_2ENRC: del > $i ).
thf(func_def_253,type,
fo__c_2Earithmetic_2ENUMERAL: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_256,type,
fo__c_2Earithmetic_2EZERO: tp__ty_2Enum_2Enum ).
thf(func_def_258,type,
fo__c_2Earithmetic_2Efindq: tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_260,type,
fo__c_2Earithmetic_2Enat__elim____magic: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_261,type,
c_2Earithmetic_2Enum__CASE: del > $i ).
thf(func_def_262,type,
c_2Ewhile_2EHOARE__SPEC: del > del > $i ).
thf(func_def_264,type,
inj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum: tp__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum > $i ).
thf(func_def_265,type,
surj__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum: $i > tp__c_ty_2Eoption_2Eoption_ty_2Enum_2Enum ).
thf(func_def_267,type,
c_2Ewhile_2EOWHILE: del > $i ).
thf(func_def_268,type,
c_2Ewhile_2EWHILE: del > $i ).
thf(func_def_270,type,
fo__c_2Enumeral_2Eexactlog: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_271,type,
c_2Enumeral_2EiBIT__cases: del > $i ).
thf(func_def_273,type,
fo__c_2Enumeral_2EiDUB: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_275,type,
fo__c_2Enumeral_2EiSQR: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_278,type,
fo__c_2Enumeral_2EiZ: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_280,type,
fo__c_2Enumeral_2EiiSUC: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_282,type,
fo__c_2Enumeral_2Einternal__mult: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_284,type,
fo__c_2Enumeral_2Eonecount: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_286,type,
fo__c_2Enumeral_2Etexp__help: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_288,type,
fo__c_2Edivides_2EPRIMES: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_291,type,
ty_2Eind__type_2Erecspace: del > del ).
thf(func_def_292,type,
c_2Eind__type_2EBOTTOM: del > $i ).
thf(func_def_293,type,
c_2Eind__type_2ECONSTR: del > $i ).
thf(func_def_294,type,
c_2Eind__type_2EFCONS: del > $i ).
thf(func_def_295,type,
c_2Eind__type_2EFNIL: del > $i ).
thf(func_def_296,type,
c_2Eind__type_2EINJA: del > $i ).
thf(func_def_297,type,
c_2Eind__type_2EINJF: del > $i ).
thf(func_def_298,type,
c_2Eind__type_2EINJN: del > $i ).
thf(func_def_299,type,
c_2Eind__type_2EINJP: del > $i ).
thf(func_def_300,type,
c_2Eind__type_2EISO: del > del > $i ).
thf(func_def_302,type,
fo__c_2Eind__type_2ENUMFST: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_305,type,
fo__c_2Eind__type_2ENUMPAIR: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_307,type,
fo__c_2Eind__type_2ENUMRIGHT: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_309,type,
fo__c_2Eind__type_2ENUMSND: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_311,type,
c_2Eind__type_2EZBOT: del > $i ).
thf(func_def_312,type,
c_2Eind__type_2EZCONSTR: del > $i ).
thf(func_def_313,type,
c_2Eind__type_2EZRECSPACE: del > $i ).
thf(func_def_314,type,
c_2Eind__type_2Edest__rec: del > $i ).
thf(func_def_315,type,
c_2Eind__type_2Emk__rec: del > $i ).
thf(func_def_318,type,
fo__c_2EbasicSize_2Eone__size: tp__ty_2Eone_2Eone > tp__ty_2Enum_2Enum ).
thf(func_def_319,type,
c_2EbasicSize_2Eoption__size: del > $i ).
thf(func_def_320,type,
c_2EbasicSize_2Epair__size: del > del > $i ).
thf(func_def_321,type,
c_2EbasicSize_2Esum__size: del > del > $i ).
thf(func_def_323,type,
fo__c_2Elogroot_2ELOG: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_325,type,
fo__c_2Elogroot_2EROOT: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_332,type,
fo__c_2Egcd_2Egcd: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_335,type,
fo__c_2Egcd_2Elcm: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_337,type,
fo__c_2Enumpair_2Einvtri: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_340,type,
fo__c_2Enumpair_2Enapp: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_342,type,
fo__c_2Enumpair_2Encons: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_343,type,
c_2Enumpair_2Enfoldl: del > $i ).
thf(func_def_345,type,
fo__c_2Enumpair_2Enfst: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_347,type,
fo__c_2Enumpair_2Enlen: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_348,type,
c_2Enumpair_2Enlistrec: del > $i ).
thf(func_def_351,type,
fo__c_2Enumpair_2Enpair: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_353,type,
fo__c_2Enumpair_2Ensnd: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_355,type,
fo__c_2Enumpair_2Etri: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_358,type,
fo__c_2Ebit_2EBITS: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_360,type,
fo__c_2Ebit_2EBITV: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_364,type,
fo__c_2Ebit_2EBIT__REVERSE: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_367,type,
fo__c_2Ebit_2EDIV__2EXP: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_369,type,
fo__c_2Ebit_2ELOG2: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_371,type,
fo__c_2Ebit_2ELOWEST__SET__BIT: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_373,type,
fo__c_2Ebit_2EMOD__2EXP: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_378,type,
fo__c_2Ebit_2ESIGN__EXTEND: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_380,type,
fo__c_2Ebit_2ESLICE: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_382,type,
fo__c_2Ebit_2ETIMES__2EXP: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_383,type,
c_2Epred__set_2EBIGINTER: del > $i ).
thf(func_def_384,type,
c_2Epred__set_2EBIGUNION: del > $i ).
thf(func_def_385,type,
c_2Epred__set_2EBIJ: del > del > $i ).
thf(func_def_386,type,
c_2Epred__set_2ECARD: del > $i ).
thf(func_def_387,type,
c_2Epred__set_2ECHOICE: del > $i ).
thf(func_def_388,type,
c_2Epred__set_2ECOMPL: del > $i ).
thf(func_def_389,type,
c_2Epred__set_2ECROSS: del > del > $i ).
thf(func_def_390,type,
c_2Epred__set_2EDELETE: del > $i ).
thf(func_def_391,type,
c_2Epred__set_2EDFUNSET: del > del > $i ).
thf(func_def_392,type,
c_2Epred__set_2EDIFF: del > $i ).
thf(func_def_393,type,
c_2Epred__set_2EDISJOINT: del > $i ).
thf(func_def_394,type,
c_2Epred__set_2EEMPTY: del > $i ).
thf(func_def_395,type,
c_2Epred__set_2EFINITE: del > $i ).
thf(func_def_396,type,
c_2Epred__set_2EFUNSET: del > del > $i ).
thf(func_def_397,type,
c_2Epred__set_2EGSPEC: del > del > $i ).
thf(func_def_398,type,
c_2Epred__set_2EIMAGE: del > del > $i ).
thf(func_def_399,type,
c_2Epred__set_2EINJ: del > del > $i ).
thf(func_def_400,type,
c_2Epred__set_2EINSERT: del > $i ).
thf(func_def_401,type,
c_2Epred__set_2EINTER: del > $i ).
thf(func_def_402,type,
c_2Epred__set_2EITSET: del > del > $i ).
thf(func_def_403,type,
c_2Epred__set_2ELINV: del > del > $i ).
thf(func_def_404,type,
c_2Epred__set_2ELINV__OPT: del > del > $i ).
thf(func_def_407,type,
c_2Epred__set_2EPOW: del > $i ).
thf(func_def_408,type,
c_2Epred__set_2EPREIMAGE: del > del > $i ).
thf(func_def_409,type,
c_2Epred__set_2EPROD__IMAGE: del > $i ).
thf(func_def_411,type,
c_2Epred__set_2EPSUBSET: del > $i ).
thf(func_def_412,type,
c_2Epred__set_2EREL__RESTRICT: del > $i ).
thf(func_def_413,type,
c_2Epred__set_2EREST: del > $i ).
thf(func_def_414,type,
c_2Epred__set_2ERINV: del > del > $i ).
thf(func_def_415,type,
c_2Epred__set_2ESING: del > $i ).
thf(func_def_416,type,
c_2Epred__set_2ESUBSET: del > $i ).
thf(func_def_417,type,
c_2Epred__set_2ESUM__IMAGE: del > $i ).
thf(func_def_419,type,
c_2Epred__set_2ESURJ: del > del > $i ).
thf(func_def_420,type,
c_2Epred__set_2EUNION: del > $i ).
thf(func_def_421,type,
c_2Epred__set_2EUNIV: del > $i ).
thf(func_def_422,type,
c_2Epred__set_2Echooser: del > $i ).
thf(func_def_424,type,
c_2Epred__set_2Ecountable: del > $i ).
thf(func_def_425,type,
c_2Epred__set_2Eenumerate: del > $i ).
thf(func_def_426,type,
c_2Epred__set_2Eequiv__on: del > $i ).
thf(func_def_427,type,
c_2Epred__set_2Eis__measure__maximal: del > $i ).
thf(func_def_430,type,
fo__c_2Epred__set_2Epair__to__num: tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_431,type,
c_2Epred__set_2Epairwise: del > $i ).
thf(func_def_432,type,
c_2Epred__set_2Epartition: del > $i ).
thf(func_def_433,type,
c_2Epred__set_2Eschroeder__close: del > $i ).
thf(func_def_434,type,
c_2EfixedPoint_2Eclosed: del > $i ).
thf(func_def_435,type,
c_2EfixedPoint_2Edense: del > $i ).
thf(func_def_436,type,
c_2EfixedPoint_2Eempty: del > del > $i ).
thf(func_def_437,type,
c_2EfixedPoint_2Efnsum: del > del > $i ).
thf(func_def_438,type,
c_2EfixedPoint_2Egfp: del > $i ).
thf(func_def_439,type,
c_2EfixedPoint_2Elfp: del > $i ).
thf(func_def_440,type,
c_2EfixedPoint_2Emonotone: del > del > $i ).
thf(func_def_443,type,
fo__c_2Enumeral__bit_2EBIT__REV: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_448,type,
fo__c_2Enumeral__bit_2EiDIV2: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_450,type,
fo__c_2Enumeral__bit_2EiLOG2: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_452,type,
fo__c_2Enumeral__bit_2EiMOD__2EXP: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_454,type,
fo__c_2Enumeral__bit_2EiSUC: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_456,type,
c_2Eset__relation_2ERREFL__EXP: del > $i ).
thf(func_def_457,type,
c_2Eset__relation_2ERRUNIV: del > $i ).
thf(func_def_458,type,
c_2Eset__relation_2Eacyclic: del > $i ).
thf(func_def_459,type,
c_2Eset__relation_2Eall__choices: del > $i ).
thf(func_def_460,type,
c_2Eset__relation_2Eantisym: del > $i ).
thf(func_def_461,type,
c_2Eset__relation_2Echain: del > $i ).
thf(func_def_462,type,
c_2Eset__relation_2Edomain: del > del > $i ).
thf(func_def_463,type,
c_2Eset__relation_2Efchains: del > $i ).
thf(func_def_464,type,
c_2Eset__relation_2Efinite__prefixes: del > del > $i ).
thf(func_def_465,type,
c_2Eset__relation_2Eget__min: del > $i ).
thf(func_def_466,type,
c_2Eset__relation_2Eirreflexive: del > $i ).
thf(func_def_467,type,
c_2Eset__relation_2Elinear__order: del > $i ).
thf(func_def_468,type,
c_2Eset__relation_2Emaximal__elements: del > $i ).
thf(func_def_469,type,
c_2Eset__relation_2Eminimal__elements: del > $i ).
thf(func_def_470,type,
c_2Eset__relation_2Enth__min: del > $i ).
thf(func_def_471,type,
c_2Eset__relation_2Enum__order: del > $i ).
thf(func_def_472,type,
c_2Eset__relation_2Epartial__order: del > $i ).
thf(func_def_473,type,
c_2Eset__relation_2Eper: del > $i ).
thf(func_def_474,type,
c_2Eset__relation_2Eper__restrict: del > $i ).
thf(func_def_475,type,
c_2Eset__relation_2Erange: del > del > $i ).
thf(func_def_476,type,
c_2Eset__relation_2Ercomp: del > del > del > $i ).
thf(func_def_477,type,
c_2Eset__relation_2Ereflexive: del > $i ).
thf(func_def_478,type,
c_2Eset__relation_2Erel__to__reln: del > del > $i ).
thf(func_def_479,type,
c_2Eset__relation_2Ereln__to__rel: del > del > $i ).
thf(func_def_480,type,
c_2Eset__relation_2Errestrict: del > $i ).
thf(func_def_481,type,
c_2Eset__relation_2Estrict: del > $i ).
thf(func_def_482,type,
c_2Eset__relation_2Estrict__linear__order: del > $i ).
thf(func_def_483,type,
c_2Eset__relation_2Etc: del > $i ).
thf(func_def_484,type,
c_2Eset__relation_2Etransitive: del > $i ).
thf(func_def_485,type,
c_2Eset__relation_2Euniv__reln: del > $i ).
thf(func_def_486,type,
c_2Eset__relation_2Eupper__bounds: del > del > $i ).
thf(func_def_489,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_490,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_491,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_492,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_493,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_494,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_495,type,
db5:
!>[X0: $tType] : X0 ).
thf(func_def_496,type,
sP0: $i > $i > $i > $o ).
thf(func_def_497,type,
sP1: $i > $i > $i > $o ).
thf(func_def_498,type,
sP2: $i > $i > $i > $o ).
thf(func_def_499,type,
sP3: $i > $i > $i > $o ).
thf(func_def_500,type,
sP4: $i > $i > $i > $o ).
thf(func_def_501,type,
sP5: $i > $i > $i > $o ).
thf(func_def_502,type,
sP6: $i > $i > $i > $o ).
thf(func_def_503,type,
sP7: $i > $i > $i > $o ).
thf(func_def_504,type,
sP8: $i > $i > $i > $o ).
thf(func_def_505,type,
sP9: $i > $i > $i > $o ).
thf(func_def_506,type,
sP10: $i > $i > $i > $o ).
thf(func_def_508,type,
sK12: $i > del > $i ).
thf(func_def_509,type,
sK13: $i > del > $i ).
thf(func_def_510,type,
sK14: del > $i > $i ).
thf(func_def_511,type,
sK15: del > $i > $i ).
thf(func_def_512,type,
sK16: $i > $i > del > $i ).
thf(func_def_513,type,
sK17: $i > del > del > $i ).
thf(func_def_514,type,
sK18: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_515,type,
sK19: del > $i > $i ).
thf(func_def_516,type,
sK20: $i > $i > del > $i ).
thf(func_def_517,type,
sK21: $i > $i > del > $i ).
thf(func_def_518,type,
sK22: $i > $i > del > $i > $i ).
thf(func_def_519,type,
sK23: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_520,type,
sK24: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_521,type,
sK25: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_522,type,
sK26: del > del > $i > $i ).
thf(func_def_523,type,
sK27: del > del > $i > $i ).
thf(func_def_524,type,
sK28: $i > $i > del > $i ).
thf(func_def_525,type,
sK29: $i > $i > del > $i ).
thf(func_def_526,type,
sK30: $i > del > $i ).
thf(func_def_527,type,
sK31: $i > $i > del > $i > $i ).
thf(func_def_528,type,
sK32: $i > del > $i > $i ).
thf(func_def_529,type,
sK33: $i > del > $i > $i ).
thf(func_def_530,type,
sK34: del > $i > $i ).
thf(func_def_531,type,
sK35: $i > del > $i ).
thf(func_def_532,type,
sK36: $i > $i > del > $i ).
thf(func_def_533,type,
sK37: $i > $i > del > $i ).
thf(func_def_534,type,
sK38: $i > del > $i ).
thf(func_def_535,type,
sK39: $i > del > $i ).
thf(func_def_536,type,
sK40: $i > del > $i ).
thf(func_def_537,type,
sK41: $i > tp__ty_2Enum_2Enum ).
thf(func_def_538,type,
sK42: del > $i > $i ).
thf(func_def_539,type,
sK43: $i > $i > del > $i > $i ).
thf(func_def_540,type,
sK44: $i > del > $i > $i ).
thf(func_def_541,type,
sK45: $i > del > $i ).
thf(func_def_542,type,
sK46: $i > del > $i ).
thf(func_def_543,type,
sK47: tp__ty_2Enum_2Enum > $i > tp__ty_2Enum_2Enum ).
thf(func_def_544,type,
sK48: tp__ty_2Enum_2Enum > $i > tp__ty_2Enum_2Enum ).
thf(func_def_545,type,
sK49: $i > tp__ty_2Enum_2Enum ).
thf(func_def_546,type,
sK50: $i > tp__ty_2Enum_2Enum ).
thf(func_def_547,type,
sK51: $i > tp__ty_2Enum_2Enum ).
thf(func_def_548,type,
sK52: tp__ty_2Enum_2Enum > $i > tp__ty_2Enum_2Enum ).
thf(func_def_549,type,
sK53: del > $i ).
thf(func_def_550,type,
sK54: del > $i ).
thf(func_def_551,type,
sK55: $i > $i > del > $i ).
thf(func_def_552,type,
sK56: $i > del > $i ).
thf(func_def_553,type,
sK57: $i > del > $i ).
thf(func_def_554,type,
sK58: $i > del > del > $i ).
thf(func_def_555,type,
sK59: $i > del > del > $i ).
thf(func_def_556,type,
sK60: $i > del > del > $i ).
thf(func_def_557,type,
sK61: $i > del > $i > $i ).
thf(func_def_558,type,
sK62: $i > del > $i > $i ).
thf(func_def_559,type,
sK63: $i > tp__ty_2Enum_2Enum ).
thf(func_def_560,type,
sK64: $i > tp__ty_2Enum_2Enum ).
thf(func_def_561,type,
sK65: $i > $i > del > $i ).
thf(func_def_562,type,
sK66: $i > $i > del > $i ).
thf(func_def_563,type,
sK67: $i > $i > $i > del > $i ).
thf(func_def_564,type,
sK68: $i > del > $i > $i ).
thf(func_def_565,type,
sK69: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_566,type,
sK70: del > $i > $i ).
thf(func_def_567,type,
sK71: del > $i > $i ).
thf(func_def_568,type,
sK72: del > $i > $i ).
thf(func_def_569,type,
sK73: del > $i > $i ).
thf(func_def_570,type,
sK74: del > $i > $i ).
thf(func_def_571,type,
sK75: del > del > $i > $i ).
thf(func_def_572,type,
sK76: del > del > $i > $i ).
thf(func_def_573,type,
sK77: del > del > $i > $i ).
thf(func_def_574,type,
sK78: del > del > $i > $i ).
thf(func_def_575,type,
sK79: del > del > del > $i > $i ).
thf(func_def_576,type,
sK80: del > del > del > $i > $i ).
thf(func_def_577,type,
sK81: $i > del > $i > $i ).
thf(func_def_578,type,
sK82: $i > del > $i > $i ).
thf(func_def_579,type,
sK83: $i > del > $i > $i ).
thf(func_def_580,type,
sK84: $i > del > $i > $i ).
thf(func_def_581,type,
sK85: $i > del > $i > $i ).
thf(func_def_582,type,
sK86: $i > $i > del > del > $i ).
thf(func_def_583,type,
sK87: $i > $i > del > del > $i ).
thf(func_def_584,type,
sK88: $i > del > $i > $i ).
thf(func_def_585,type,
sK89: $i > del > $i ).
thf(func_def_586,type,
sK90: $i > tp__ty_2Enum_2Enum ).
thf(func_def_587,type,
sK91: $i > tp__ty_2Enum_2Enum ).
thf(func_def_588,type,
sK92: $i > del > del > $i > $i ).
thf(func_def_589,type,
sK93: $i > del > $i > $i ).
thf(func_def_590,type,
sK94: $i > del > $i > $i ).
thf(func_def_591,type,
sK95: $i > $i > $i > del > $i ).
thf(func_def_592,type,
sK96: $i > $i > del > $i ).
thf(func_def_593,type,
sK97: $i > $i > del > $i ).
thf(func_def_594,type,
sK98: del > $i > $i ).
thf(func_def_595,type,
sK99: $i > del > $i > $i ).
thf(func_def_596,type,
sK100: $i > del > $i > $i ).
thf(func_def_597,type,
sK101: $i > del > $i ).
thf(func_def_598,type,
sK102: $i > tp__ty_2Enum_2Enum ).
thf(func_def_599,type,
sK103: $i > tp__ty_2Enum_2Enum ).
thf(func_def_600,type,
sK104: $i > $i > del > $i > $i ).
thf(func_def_601,type,
sK105: $i > del > del > $i ).
thf(func_def_602,type,
sK106: $i > del > del > $i ).
thf(func_def_603,type,
sK107: $i > $i > del > $i ).
thf(func_def_604,type,
sK108: $i > $i > del > $i ).
thf(func_def_605,type,
sK109: $i > del > $i ).
thf(func_def_606,type,
sK110: del > $i > $i ).
thf(func_def_607,type,
sK111: $i > del > $i > $i ).
thf(func_def_608,type,
sK112: $i > del > $i > $i ).
thf(func_def_609,type,
sK113: $i > del > $i > $i ).
thf(func_def_610,type,
sK114: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_611,type,
sK115: $i > $i > del > $i ).
thf(func_def_612,type,
sK116: del > $i > $i ).
thf(func_def_613,type,
sK117: $i > tp__ty_2Enum_2Enum ).
thf(func_def_614,type,
sK118: $i > tp__ty_2Enum_2Enum ).
thf(func_def_615,type,
sK119: $i > tp__ty_2Enum_2Enum ).
thf(func_def_616,type,
sK120: $i > tp__ty_2Enum_2Enum ).
thf(func_def_617,type,
sK121: $i > tp__ty_2Enum_2Enum ).
thf(func_def_618,type,
sK122: $i > tp__ty_2Enum_2Enum ).
thf(func_def_619,type,
sK123: $i > $i > $i > del > $i ).
thf(func_def_620,type,
sK124: del > $i > $i ).
thf(func_def_621,type,
sK125: del > $i > tp__ty_2Enum_2Enum ).
thf(func_def_622,type,
sK126: $i > del > $i > tp__ty_2Enum_2Enum ).
thf(func_def_623,type,
sK127: tp__ty_2Enum_2Enum > $i > del > $i > $i ).
thf(func_def_624,type,
sK128: tp__ty_2Enum_2Enum > $i > del > $i > tp__ty_2Enum_2Enum ).
thf(func_def_625,type,
sK129: $i > del > del > $i > $i ).
thf(func_def_626,type,
sK130: $i > tp__ty_2Enum_2Enum ).
thf(func_def_627,type,
sK131: $i > del > $i > $i ).
thf(func_def_628,type,
sK132: $i > del > $i ).
thf(func_def_629,type,
sK133: del > del > $i > $i ).
thf(func_def_630,type,
sK134: del > del > $i > $i ).
thf(func_def_631,type,
sK135: $i > $i > $i > del > del > $i ).
thf(func_def_632,type,
sK136: $i > $i > del > $i ).
thf(func_def_633,type,
sK137: $i > $i > del > $i ).
thf(func_def_634,type,
sK138: $i > $i > del > $i > $i ).
thf(func_def_635,type,
sK139: del > $i > $i ).
thf(func_def_636,type,
sK140: del > $i > $i ).
thf(func_def_637,type,
sK141: $i > del > $i > $i ).
thf(func_def_638,type,
sK142: $i > del > $i > $i ).
thf(func_def_639,type,
sK143: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_640,type,
sK144: del > del > $i > $i ).
thf(func_def_641,type,
sK145: $i > del > del > $i ).
thf(func_def_642,type,
sK146: $i > del > del > $i ).
thf(func_def_643,type,
sK147: $i > del > del > $i ).
thf(func_def_644,type,
sK148: $i > del > $i ).
thf(func_def_645,type,
sK149: $i > del > $i ).
thf(func_def_646,type,
sK150: $i > del > $i ).
thf(func_def_647,type,
sK151: $i > del > $i > $i ).
thf(func_def_648,type,
sK152: $i > del > $i > $i ).
thf(func_def_649,type,
sK153: $i > $i > del > $i > $i ).
thf(func_def_650,type,
sK154: $i > $i > del > $i ).
thf(func_def_651,type,
sK155: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_652,type,
sK156: $i > $i > $i > del > $i ).
thf(func_def_653,type,
sK157: $i > $i > del > $i ).
thf(func_def_654,type,
sK158: $i > $i > del > $i ).
thf(func_def_655,type,
sK159: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_656,type,
sK160: $i > $i > del > $i ).
thf(func_def_657,type,
sK161: $i > $i > del > $i ).
thf(func_def_658,type,
sK162: $i > $i > del > $i ).
thf(func_def_659,type,
sK163: $i > $i > del > $i ).
thf(func_def_660,type,
sK164: $i > $i > del > $i ).
thf(func_def_661,type,
sK165: $i > $i > del > $i ).
thf(func_def_662,type,
sK166: $i > del > $i ).
thf(func_def_663,type,
sK167: $i > del > $i > $i ).
thf(func_def_664,type,
sK168: $i > del > $i > $i ).
thf(func_def_665,type,
sK169: $i > del > $i > $i ).
thf(func_def_666,type,
sK170: $i > del > $i ).
thf(func_def_667,type,
sK171: $i > $i > del > $i > $i ).
thf(func_def_668,type,
sK172: $i > del > $i > $i ).
thf(func_def_669,type,
sK173: $i > del > $i > $i ).
thf(func_def_670,type,
sK174: $i > del > $i > $i ).
thf(func_def_671,type,
sK175: $i > del > $i > $i ).
thf(func_def_672,type,
sK176: $i > del > $i ).
thf(func_def_673,type,
sK177: $i > $i > $i > del > $i ).
thf(func_def_674,type,
sK178: $i > $i > del > $i ).
thf(func_def_675,type,
sK179: $i > $i > del > $i ).
thf(func_def_676,type,
sK180: $i > del > del > $i ).
thf(func_def_677,type,
sK181: $i > del > del > $i ).
thf(func_def_678,type,
sK182: $i > del > del > $i ).
thf(func_def_679,type,
sK183: $i > del > $i ).
thf(func_def_680,type,
sK184: $i > del > $i ).
thf(func_def_681,type,
sK185: $i > $i > del > $i ).
thf(func_def_682,type,
sK186: $i > tp__ty_2Enum_2Enum ).
thf(func_def_683,type,
sK187: $i > tp__ty_2Enum_2Enum ).
thf(func_def_684,type,
sK188: $i > $i > tp__ty_2Enum_2Enum ).
thf(func_def_685,type,
sK189: $i > $i > tp__ty_2Enum_2Enum ).
thf(func_def_686,type,
sK190: $i > $i > tp__ty_2Enum_2Enum ).
thf(func_def_687,type,
sK191: $i > del > $i > $i ).
thf(func_def_688,type,
sK192: $i > $i > del > $i > $i ).
thf(func_def_689,type,
sK193: $i > tp__ty_2Enum_2Enum ).
thf(func_def_690,type,
sK194: tp__ty_2Enum_2Enum > $i > tp__ty_2Enum_2Enum ).
thf(func_def_691,type,
sK195: $i > tp__ty_2Enum_2Enum ).
thf(func_def_692,type,
sK196: $i > tp__ty_2Enum_2Enum ).
thf(func_def_693,type,
sK197: $i > del > $i ).
thf(func_def_694,type,
sK198: $i > $i > del > $i ).
thf(func_def_695,type,
sK199: $i > $i > del > $i ).
thf(func_def_696,type,
sK200: $i > del > tp__ty_2Enum_2Enum ).
thf(func_def_697,type,
sK201: $i > $i > $i > del > $i ).
thf(func_def_698,type,
sK202: $i > $i > del > $i > $i ).
thf(func_def_699,type,
sK203: $i > $i > del > $i > $i ).
thf(func_def_700,type,
sK204: $i > del > $i > $i ).
thf(func_def_701,type,
sK205: $i > del > $i ).
thf(func_def_702,type,
sK206: $i > del > $i > $i ).
thf(func_def_703,type,
sK207: $i > del > $i > $i ).
thf(func_def_704,type,
sK208: $i > $i > del > del > $i > $i ).
thf(func_def_705,type,
sK209: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_706,type,
sK210: del > $i > $i ).
thf(func_def_707,type,
sK211: del > $i > $i ).
thf(func_def_708,type,
sK212: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_709,type,
sK213: $i > del > $i ).
thf(func_def_710,type,
sK214: $i > del > $i > $i ).
thf(func_def_711,type,
sK215: $i > del > $i > $i ).
thf(func_def_712,type,
sK216: $i > del > $i > $i ).
thf(func_def_713,type,
sK217: $i > $i > del > $i ).
thf(func_def_714,type,
sK218: $i > del > $i ).
thf(func_def_715,type,
sK219: del > $i > $i ).
thf(func_def_716,type,
sK220: $i > del > $i > $i ).
thf(func_def_717,type,
sK221: $i > tp__ty_2Enum_2Enum ).
thf(func_def_718,type,
sK222: $i > $i > del > $i ).
thf(func_def_719,type,
sK223: $i > del > $i ).
thf(func_def_720,type,
sK224: $i > del > $i ).
thf(func_def_721,type,
sK225: $i > $i > del > $i > $i ).
thf(func_def_722,type,
sK226: $i > $i > del > $i > $i ).
thf(func_def_723,type,
sK227: $i > del > $i > $i ).
thf(func_def_724,type,
sK228: $i > $i > del > $i > $i ).
thf(func_def_725,type,
sK229: $i > del > $i > $i ).
thf(func_def_726,type,
sK230: $i > del > $i > $i ).
thf(func_def_727,type,
sK231: $i > $i > del > $i ).
thf(func_def_728,type,
sK232: $i > $i > del > $i ).
thf(func_def_729,type,
sK233: del > $i > $i ).
thf(func_def_730,type,
sK234: del > $i > $i ).
thf(func_def_731,type,
sK235: $i > $i > del > $i ).
thf(func_def_732,type,
sK236: $i > del > $i ).
thf(func_def_733,type,
sK237: $i > tp__ty_2Enum_2Enum ).
thf(func_def_734,type,
sK238: $i > tp__ty_2Enum_2Enum ).
thf(func_def_735,type,
sK239: $i > tp__ty_2Enum_2Enum ).
thf(func_def_736,type,
sK240: $i > tp__ty_2Enum_2Enum ).
thf(func_def_737,type,
sK241: $i > del > $i ).
thf(func_def_738,type,
sK242: $i > del > $i ).
thf(func_def_739,type,
sK243: $i > $i > del > $i ).
thf(func_def_740,type,
sK244: $i > del > $i > $i ).
thf(func_def_741,type,
sK245: $i > del > $i ).
thf(func_def_742,type,
sK246: del > $i > $i ).
thf(func_def_743,type,
sK247: del > $i > $i ).
thf(func_def_744,type,
sK248: del > $i > $i ).
thf(func_def_745,type,
sK249: $i > del > $i > $i ).
thf(func_def_746,type,
sK250: $i > del > $i > $i ).
thf(func_def_747,type,
sK251: $i > del > $i > $i ).
thf(func_def_748,type,
sK252: $i > del > $i > $i ).
thf(func_def_749,type,
sK253: $i > del > $i > $i ).
thf(func_def_750,type,
sK254: $i > del > $i > $i ).
thf(func_def_751,type,
sK255: $i > del > $i > $i ).
thf(func_def_752,type,
sK256: $i > del > $i > $i ).
thf(func_def_753,type,
sK257: del > $i > $i ).
thf(func_def_754,type,
sK258: $i > del > $i > $i ).
thf(func_def_755,type,
sK259: del > $i > $i ).
thf(func_def_756,type,
sK260: del > $i > $i ).
thf(func_def_757,type,
sK261: $i > del > $i > $i ).
thf(func_def_759,type,
sK263: del > $i > $i ).
thf(func_def_760,type,
sK264: $i > $i > del > $i ).
thf(func_def_761,type,
sK265: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > $i > tp__ty_2Enum_2Enum ).
thf(func_def_762,type,
sK266: $i > del > $i ).
thf(func_def_763,type,
sK267: del > $i ).
thf(func_def_764,type,
sK268: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_765,type,
sK269: $i > del > del > $i ).
thf(func_def_766,type,
sK270: $i > del > del > $i ).
thf(func_def_767,type,
sK271: $i > del > del > $i ).
thf(func_def_768,type,
sK272: del > $i > $i ).
thf(func_def_769,type,
sK273: $i > del > $i > $i ).
thf(func_def_770,type,
sK274: $i > del > $i > $i ).
thf(func_def_771,type,
sK275: $i > $i > $i > del > $i ).
thf(func_def_772,type,
sK276: $i > $i > del > $i > del > $i ).
thf(func_def_773,type,
sK277: $i > $i > del > $i ).
thf(func_def_774,type,
sK278: $i > del > $i ).
thf(func_def_775,type,
sK279: $i > $i > del > $i ).
thf(func_def_776,type,
sK280: $i > del > $i ).
thf(func_def_777,type,
sK281: $i > $i > del > $i ).
thf(func_def_778,type,
sK282: $i > del > $i ).
thf(func_def_779,type,
sK283: $i > del > $i > $i ).
thf(func_def_780,type,
sK284: $i > del > $i ).
thf(func_def_781,type,
sK285: $i > del > $i ).
thf(func_def_782,type,
sK286: $i > $i > del > $i ).
thf(func_def_783,type,
sK287: $i > $i > $i > del > $i ).
thf(func_def_784,type,
sK288: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_785,type,
sK289: $i > $i > del > $i ).
thf(func_def_786,type,
sK290: $i > $i > del > $i ).
thf(func_def_787,type,
sK291: $i > $i > del > $i ).
thf(func_def_788,type,
sK292: $i > $i > del > $i ).
thf(func_def_789,type,
sK293: $i > $i > del > $i ).
thf(func_def_790,type,
sK294: $i > del > del > $i ).
thf(func_def_791,type,
sK295: $i > del > del > $i ).
thf(func_def_792,type,
sK296: $i > del > del > $i ).
thf(func_def_793,type,
sK297: $i > del > del > $i ).
thf(func_def_794,type,
sK298: $i > $i > del > $i ).
thf(func_def_795,type,
sK299: $i > $i > del > $i ).
thf(func_def_796,type,
sK300: $i > del > $i > $i ).
thf(func_def_797,type,
sK301: $i > del > $i > $i ).
thf(func_def_798,type,
sK302: $i > del > $i > $i ).
thf(func_def_799,type,
sK303: $i > del > $i > $i ).
thf(func_def_800,type,
sK304: $i > del > $i > $i ).
thf(func_def_801,type,
sK305: $i > del > $i ).
thf(func_def_802,type,
sK306: $i > $i > del > $i ).
thf(func_def_803,type,
sK307: $i > del > $i ).
thf(func_def_804,type,
sK308: del > $i > del > $i ).
thf(func_def_805,type,
sK309: del > $i > del > $i ).
thf(func_def_806,type,
sK310: del > $i > del > $i ).
thf(func_def_807,type,
sK311: del > $i > del > $i ).
thf(func_def_808,type,
sK312: $i > $i > del > $i ).
thf(func_def_809,type,
sK313: $i > $i > del > $i ).
thf(func_def_810,type,
sK314: $i > del > $i ).
thf(func_def_811,type,
sK315: del > $i > del > del > $i ).
thf(func_def_812,type,
sK316: $i > $i > $i > del > $i ).
thf(func_def_813,type,
sK317: del > $i > $i ).
thf(func_def_814,type,
sK318: $i > del > $i > $i ).
thf(func_def_815,type,
sK319: del > $i > del > $i ).
thf(func_def_816,type,
sK320: del > $i > del > $i ).
thf(func_def_817,type,
sK321: $i > tp__ty_2Enum_2Enum ).
thf(func_def_818,type,
sK322: $i > tp__ty_2Enum_2Enum ).
thf(func_def_819,type,
sK323: del ).
thf(func_def_820,type,
sK324: del ).
thf(func_def_822,type,
sK326: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_823,type,
sK327: del > del > ( $i > $i ) > $i ).
thf(func_def_824,type,
sK328: $i > $i > del > del > $i > $i ).
thf(func_def_825,type,
sK329: $i > $i > del > del > $i > $i ).
thf(func_def_826,type,
sK330: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_827,type,
sK331: $i > del > $i > $i ).
thf(func_def_828,type,
sK332: $i > del > $i > $i ).
thf(func_def_829,type,
sK333: $i > $i > $i > del > del > $i ).
thf(func_def_830,type,
sK334: $i > $i > $i > del > $i ).
thf(func_def_831,type,
sK335: $i > $i > del > $i ).
thf(func_def_832,type,
sK336: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
thf(func_def_833,type,
sK337: $i > $i > del > $i ).
thf(func_def_834,type,
sK338: $i > $i > del > $i ).
thf(func_def_835,type,
sK339: $i > $i > del > $i ).
thf(func_def_836,type,
sK340: $i > del > $i ).
thf(func_def_837,type,
sK341: $i > del > $i ).
thf(func_def_838,type,
sK342: del > $i > $i ).
thf(func_def_839,type,
sK343: del > $i > $i ).
thf(func_def_840,type,
sK344: $i > del > $i ).
thf(func_def_841,type,
sK345: $i > del > $i > $i ).
thf(func_def_842,type,
sK346: $i > del > $i > $i ).
thf(func_def_843,type,
sK347: $i > $i > del > $i ).
thf(func_def_844,type,
sK348: $i > del > $i ).
thf(func_def_845,type,
sK349: $i > del > $i > $i ).
thf(func_def_846,type,
sK350: $i > del > $i > $i ).
thf(func_def_847,type,
sK351: $i > $i > del > $i > $i ).
thf(func_def_848,type,
sK352: $i > $i > $i > del > $i ).
thf(func_def_849,type,
sK353: $i > del > $i ).
thf(func_def_850,type,
sK354: $i > del > $i ).
thf(func_def_851,type,
sK355: $i > del > $i ).
thf(func_def_852,type,
sK356: $i > del > $i ).
thf(func_def_853,type,
sK357: $i > $i > $i > del > $i ).
thf(func_def_854,type,
sK358: $i > del > $i ).
thf(func_def_855,type,
sK359: $i > $i > del > $i ).
thf(func_def_856,type,
sK360: $i > $i > del > $i ).
thf(func_def_857,type,
sK361: $i > $i > del > $i ).
thf(func_def_858,type,
sK362: $i > $i > del > $i ).
thf(func_def_859,type,
sK363: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum > $i ).
thf(func_def_860,type,
sK364: $i > tp__ty_2Enum_2Enum ).
thf(func_def_861,type,
sK365: $i > $i > del > $i ).
thf(func_def_862,type,
sK366: $i > del > $i ).
thf(func_def_863,type,
sK367: $i > del > $i ).
thf(func_def_864,type,
sK368: tp__ty_2Enum_2Enum > $i > tp__ty_2Enum_2Enum ).
thf(func_def_865,type,
sK369: tp__ty_2Enum_2Enum > $i > tp__ty_2Enum_2Enum ).
thf(func_def_866,type,
sK370: $i > $i > $i > del > $i ).
thf(func_def_867,type,
sK371: $i > del > $i > $i ).
thf(func_def_868,type,
sK372: $i > tp__ty_2Enum_2Enum ).
thf(f906,axiom,
! [X2: del,X3: $i,X1: del,X0: del] :
( ( mem @ X3 @ ( arr @ X0 @ ( arr @ X1 @ X2 ) ) )
=> ( ( ap @ ( c_2Epair_2ECURRY @ X0 @ X1 @ X2 ) @ ( ap @ ( c_2Epair_2EUNCURRY @ X0 @ X1 @ X2 ) @ X3 ) )
= X3 ) ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP014^5.ax',conj_thm_2Epair_2ECURRY__UNCURRY__THM) ).
thf(f2891,axiom,
! [X1: del,X0: del] :
( ( c_2Eset__relation_2Erel__to__reln @ X0 @ X1 )
= ( c_2Epair_2EUNCURRY @ X0 @ X1 @ bool ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Eset__relation_2Erel__to__reln__IS__UNCURRY) ).
thf(f2892,axiom,
! [X0: del,X1: del] :
( ( c_2Eset__relation_2Ereln__to__rel @ X0 @ X1 )
= ( c_2Epair_2ECURRY @ X0 @ X1 @ bool ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Eset__relation_2Ereln__to__rel__IS__CURRY) ).
thf(f2893,conjecture,
! [X1: del,X2: $i,X0: del] :
( ( mem @ X2 @ ( arr @ X0 @ ( arr @ X1 @ bool ) ) )
=> ( ( ap @ ( c_2Eset__relation_2Ereln__to__rel @ X0 @ X1 ) @ ( ap @ ( c_2Eset__relation_2Erel__to__reln @ X0 @ X1 ) @ X2 ) )
= X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Eset__relation_2Erel__to__reln__inv) ).
thf(f2894,negated_conjecture,
~ ! [X1: del,X2: $i,X0: del] :
( ( mem @ X2 @ ( arr @ X0 @ ( arr @ X1 @ bool ) ) )
=> ( ( ap @ ( c_2Eset__relation_2Ereln__to__rel @ X0 @ X1 ) @ ( ap @ ( c_2Eset__relation_2Erel__to__reln @ X0 @ X1 ) @ X2 ) )
= X2 ) ),
inference(negated_conjecture,[status(cth)],[f2893]) ).
thf(f2996,plain,
! [X1: del,X0: del] :
( ( c_2Eset__relation_2Ereln__to__rel @ X0 @ X1 )
= ( c_2Epair_2ECURRY @ X0 @ X1 @ bool ) ),
inference(fool_elimination,[],[f2892]) ).
thf(f4518,plain,
~ ! [X0: del,X1: $i,X2: del] :
( ( mem @ X1 @ ( arr @ X2 @ ( arr @ X0 @ bool ) ) )
=> ( ( ap @ ( c_2Eset__relation_2Ereln__to__rel @ X2 @ X0 ) @ ( ap @ ( c_2Eset__relation_2Erel__to__reln @ X2 @ X0 ) @ X1 ) )
= X1 ) ),
inference(rectify,[],[f2894]) ).
thf(f4519,plain,
~ ! [X1: $i,X0: del,X2: del] :
( ( $true
= ( mem @ X1 @ ( arr @ X2 @ ( arr @ X0 @ bool ) ) ) )
=> ( ( ap @ ( c_2Eset__relation_2Ereln__to__rel @ X2 @ X0 ) @ ( ap @ ( c_2Eset__relation_2Erel__to__reln @ X2 @ X0 ) @ X1 ) )
= X1 ) ),
inference(fool_elimination,[],[f4518]) ).
thf(f6517,plain,
! [X0: del,X1: del] :
( ( c_2Eset__relation_2Erel__to__reln @ X1 @ X0 )
= ( c_2Epair_2EUNCURRY @ X1 @ X0 @ bool ) ),
inference(rectify,[],[f2891]) ).
thf(f6518,plain,
! [X1: del,X0: del] :
( ( c_2Eset__relation_2Erel__to__reln @ X1 @ X0 )
= ( c_2Epair_2EUNCURRY @ X1 @ X0 @ bool ) ),
inference(fool_elimination,[],[f6517]) ).
thf(f7372,plain,
! [X0: del,X1: $i,X2: del,X3: del] :
( ( mem @ X1 @ ( arr @ X3 @ ( arr @ X2 @ X0 ) ) )
=> ( ( ap @ ( c_2Epair_2ECURRY @ X3 @ X2 @ X0 ) @ ( ap @ ( c_2Epair_2EUNCURRY @ X3 @ X2 @ X0 ) @ X1 ) )
= X1 ) ),
inference(rectify,[],[f906]) ).
thf(f7373,plain,
! [X1: $i,X0: del,X2: del,X3: del] :
( ( ( mem @ X1 @ ( arr @ X3 @ ( arr @ X2 @ X0 ) ) )
= $true )
=> ( ( ap @ ( c_2Epair_2ECURRY @ X3 @ X2 @ X0 ) @ ( ap @ ( c_2Epair_2EUNCURRY @ X3 @ X2 @ X0 ) @ X1 ) )
= X1 ) ),
inference(fool_elimination,[],[f7372]) ).
thf(f9085,plain,
! [X3: del,X0: del,X2: del,X1: $i] :
( ( ( mem @ X1 @ ( arr @ X3 @ ( arr @ X2 @ X0 ) ) )
!= $true )
| ( ( ap @ ( c_2Epair_2ECURRY @ X3 @ X2 @ X0 ) @ ( ap @ ( c_2Epair_2EUNCURRY @ X3 @ X2 @ X0 ) @ X1 ) )
= X1 ) ),
inference(ennf_transformation,[],[f7373]) ).
thf(f9235,plain,
? [X2: del,X0: del,X1: $i] :
( ( $true
= ( mem @ X1 @ ( arr @ X2 @ ( arr @ X0 @ bool ) ) ) )
& ( ( ap @ ( c_2Eset__relation_2Ereln__to__rel @ X2 @ X0 ) @ ( ap @ ( c_2Eset__relation_2Erel__to__reln @ X2 @ X0 ) @ X1 ) )
!= X1 ) ),
inference(ennf_transformation,[],[f4519]) ).
thf(f9429,plain,
! [X0: del,X1: del,X2: del,X3: $i] :
( ( ( mem @ X3 @ ( arr @ X0 @ ( arr @ X2 @ X1 ) ) )
!= $true )
| ( ( ap @ ( c_2Epair_2ECURRY @ X0 @ X2 @ X1 ) @ ( ap @ ( c_2Epair_2EUNCURRY @ X0 @ X2 @ X1 ) @ X3 ) )
= X3 ) ),
inference(rectify,[],[f9085]) ).
thf(f9546,plain,
! [X0: del,X1: del] :
( ( c_2Epair_2ECURRY @ X1 @ X0 @ bool )
= ( c_2Eset__relation_2Ereln__to__rel @ X1 @ X0 ) ),
inference(rectify,[],[f2996]) ).
thf(f9897,plain,
! [X0: del,X1: del] :
( ( c_2Epair_2EUNCURRY @ X0 @ X1 @ bool )
= ( c_2Eset__relation_2Erel__to__reln @ X0 @ X1 ) ),
inference(rectify,[],[f6518]) ).
thf(f10177,plain,
? [X0: del,X1: del,X2: $i] :
( ( ( mem @ X2 @ ( arr @ X0 @ ( arr @ X1 @ bool ) ) )
= $true )
& ( ( ap @ ( c_2Eset__relation_2Ereln__to__rel @ X0 @ X1 ) @ ( ap @ ( c_2Eset__relation_2Erel__to__reln @ X0 @ X1 ) @ X2 ) )
!= X2 ) ),
inference(rectify,[],[f9235]) ).
thf(f10178,plain,
( ( ( mem @ sK325 @ ( arr @ sK323 @ ( arr @ sK324 @ bool ) ) )
= $true )
& ( sK325
!= ( ap @ ( c_2Eset__relation_2Ereln__to__rel @ sK323 @ sK324 ) @ ( ap @ ( c_2Eset__relation_2Erel__to__reln @ sK323 @ sK324 ) @ sK325 ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK323,sK324,sK325]),skolemize(X0,sK323),skolemize(X1,sK324),skolemize(X2,sK325)],[f10177]) ).
thf(f10540,plain,
! [X2: del,X3: $i,X0: del,X1: del] :
( ( ( mem @ X3 @ ( arr @ X0 @ ( arr @ X2 @ X1 ) ) )
!= $true )
| ( ( ap @ ( c_2Epair_2ECURRY @ X0 @ X2 @ X1 ) @ ( ap @ ( c_2Epair_2EUNCURRY @ X0 @ X2 @ X1 ) @ X3 ) )
= X3 ) ),
inference(cnf_transformation,[],[f9429]) ).
thf(f10780,plain,
! [X0: del,X1: del] :
( ( c_2Epair_2ECURRY @ X1 @ X0 @ bool )
= ( c_2Eset__relation_2Ereln__to__rel @ X1 @ X0 ) ),
inference(cnf_transformation,[],[f9546]) ).
thf(f11750,plain,
! [X0: del,X1: del] :
( ( c_2Epair_2EUNCURRY @ X0 @ X1 @ bool )
= ( c_2Eset__relation_2Erel__to__reln @ X0 @ X1 ) ),
inference(cnf_transformation,[],[f9897]) ).
thf(f12490,plain,
( sK325
!= ( ap @ ( c_2Eset__relation_2Ereln__to__rel @ sK323 @ sK324 ) @ ( ap @ ( c_2Eset__relation_2Erel__to__reln @ sK323 @ sK324 ) @ sK325 ) ) ),
inference(cnf_transformation,[],[f10178]) ).
thf(f12491,plain,
( ( mem @ sK325 @ ( arr @ sK323 @ ( arr @ sK324 @ bool ) ) )
= $true ),
inference(cnf_transformation,[],[f10178]) ).
thf(f13218,definition,
( spl373_3
<=> ( sK325
= ( ap @ ( c_2Eset__relation_2Ereln__to__rel @ sK323 @ sK324 ) @ ( ap @ ( c_2Eset__relation_2Erel__to__reln @ sK323 @ sK324 ) @ sK325 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl373_3])],[avatar_definition]) ).
thf(f13220,plain,
( ( sK325
!= ( ap @ ( c_2Eset__relation_2Ereln__to__rel @ sK323 @ sK324 ) @ ( ap @ ( c_2Eset__relation_2Erel__to__reln @ sK323 @ sK324 ) @ sK325 ) ) )
| spl373_3 ),
inference(avatar_component_clause,[],[f13218]) ).
thf(f13221,plain,
~ spl373_3,
inference(avatar_split_clause,[],[f12490,f13218]) ).
thf(f13515,definition,
( spl373_65
<=> ( ( mem @ sK325 @ ( arr @ sK323 @ ( arr @ sK324 @ bool ) ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl373_65])],[avatar_definition]) ).
thf(f13517,plain,
( ( ( mem @ sK325 @ ( arr @ sK323 @ ( arr @ sK324 @ bool ) ) )
= $true )
| ~ spl373_65 ),
inference(avatar_component_clause,[],[f13515]) ).
thf(f13518,plain,
spl373_65,
inference(avatar_split_clause,[],[f12491,f13515]) ).
thf(f19403,plain,
( ( $true != $true )
| ( ( ap @ ( c_2Epair_2ECURRY @ sK323 @ sK324 @ bool ) @ ( ap @ ( c_2Epair_2EUNCURRY @ sK323 @ sK324 @ bool ) @ sK325 ) )
= sK325 )
| ~ spl373_65 ),
inference(superposition,[],[f10540,f13517]) ).
thf(f19421,plain,
( ( ( ap @ ( c_2Epair_2ECURRY @ sK323 @ sK324 @ bool ) @ ( ap @ ( c_2Epair_2EUNCURRY @ sK323 @ sK324 @ bool ) @ sK325 ) )
= sK325 )
| ~ spl373_65 ),
inference(trivial_inequality_removal,[],[f19403]) ).
thf(f19437,plain,
( ( ( ap @ ( c_2Eset__relation_2Ereln__to__rel @ sK323 @ sK324 ) @ ( ap @ ( c_2Epair_2EUNCURRY @ sK323 @ sK324 @ bool ) @ sK325 ) )
= sK325 )
| ~ spl373_65 ),
inference(forward_demodulation,[],[f19421,f10780]) ).
thf(f19446,plain,
( ( sK325
= ( ap @ ( c_2Eset__relation_2Ereln__to__rel @ sK323 @ sK324 ) @ ( ap @ ( c_2Eset__relation_2Erel__to__reln @ sK323 @ sK324 ) @ sK325 ) ) )
| ~ spl373_65 ),
inference(forward_demodulation,[],[f19437,f11750]) ).
thf(f19455,plain,
( $false
| spl373_3
| ~ spl373_65 ),
inference(forward_subsumption_resolution,[],[f19446,f13220]) ).
thf(f19456,plain,
( spl373_3
| ~ spl373_65 ),
inference(avatar_contradiction_clause,[],[f19455]) ).
cnf(s2,plain,
~ spl373_3,
inference(sat_conversion,[],[f13221]) ).
cnf(s88,plain,
spl373_65,
inference(sat_conversion,[],[f13518]) ).
cnf(s624,plain,
( spl373_3
| ~ spl373_65 ),
inference(sat_conversion,[],[f19456]) ).
cnf(s630,plain,
spl373_3,
inference(rat,[],[s624,s88]) ).
cnf(s656,plain,
$false,
inference(rat,[],[s2,s630]) ).
thf(f19474,plain,
$false,
inference(avatar_sat_refutation,[],[s656]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP005^5 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n003.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 19:22:59 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running higher-order theorem proving
% 0.87/0.96 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.22/1.28 % (2940494)Detected a higher-order problem, will run a greedy HOL sequence.
% 1.22/1.28 % (2940505)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 1.22/1.28 % (2940505)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.22/1.28 % (2940500)lrs+10_16_si=on:nwc=1.5:random_seed=961762728:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/18Mi)
% 1.22/1.28 % (2940502)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=2990912131: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_2998 on theBenchmark for (2998ds/634Mi)
% 1.22/1.28 % (2940503)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=948321362:i=24:av=off:rtra=on_2998 on theBenchmark for (2998ds/24Mi)
% 1.22/1.28 % (2940499)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2544094469:s2a=on:i=87:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/87Mi)
% 1.22/1.28 % (2940504)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=328814843:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/75Mi)
% 1.22/1.28 % (2940501)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3827085580:i=3:rtra=on:inj=on:ntd=on_2998 on theBenchmark for (2998ds/3Mi)
% 1.22/1.28 % (2940505)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=1345160408:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2998 on theBenchmark for (2998ds/157Mi)
% 1.22/1.28 % (2940501)Instruction limit reached!
% 1.22/1.28 % (2940501)------------------------------
% 1.22/1.28 % (2940501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.22/1.28 % (2940501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.22/1.28 % (2940501)CaDiCaL version: 2.1.3
% 1.22/1.28 % (2940501)Termination reason: Instruction limit
% 1.22/1.28 % (2940501)Termination phase: shuffling
% 1.22/1.28 % (2940501)Time elapsed: 0.008 s
% 1.22/1.28 % (2940501)Peak memory usage: 16 MB
% 1.22/1.28 % (2940501)Instructions burned: 3 (million)
% 1.22/1.28 % (2940500)Instruction limit reached!
% 1.22/1.28 % (2940500)------------------------------
% 1.22/1.28 % (2940500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.22/1.28 % (2940500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.22/1.28 % (2940500)CaDiCaL version: 2.1.3
% 1.22/1.28 % (2940500)Termination reason: Instruction limit
% 1.22/1.28 % (2940500)Termination phase: shuffling
% 1.22/1.28 % (2940500)Time elapsed: 0.013 s
% 1.22/1.28 % (2940500)Peak memory usage: 16 MB
% 1.22/1.28 % (2940500)Instructions burned: 19 (million)
% 1.22/1.28 % (2940503)Instruction limit reached!
% 1.22/1.28 % (2940503)------------------------------
% 1.22/1.28 % (2940503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.22/1.28 % (2940503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.22/1.28 % (2940503)CaDiCaL version: 2.1.3
% 1.22/1.28 % (2940503)Termination reason: Instruction limit
% 1.22/1.28 % (2940503)Termination phase: shuffling
% 1.22/1.28 % (2940503)Time elapsed: 0.016 s
% 1.22/1.28 % (2940503)Peak memory usage: 16 MB
% 1.22/1.28 % (2940503)Instructions burned: 28 (million)
% 1.22/1.28 % (2940504)Instruction limit reached!
% 1.22/1.28 % (2940504)------------------------------
% 1.22/1.28 % (2940504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.22/1.28 % (2940504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.22/1.28 % (2940504)CaDiCaL version: 2.1.3
% 1.22/1.28 % (2940504)Termination reason: Instruction limit
% 1.22/1.28 % (2940504)Termination phase: shuffling
% 1.22/1.28 % (2940504)Time elapsed: 0.030 s
% 1.22/1.28 % (2940504)Peak memory usage: 17 MB
% 1.22/1.28 % (2940504)Instructions burned: 80 (million)
% 1.22/1.28 % (2940515)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.22/1.28 % (2940514)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=245917951:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2997 on theBenchmark for (2997ds/5Mi)
% 1.70/1.34 % (2940515)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4201821575:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 1.70/1.34 % (2940499)Instruction limit reached!
% 1.70/1.34 % (2940499)------------------------------
% 1.70/1.34 % (2940499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/1.34 % (2940499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/1.34 % (2940499)CaDiCaL version: 2.1.3
% 1.70/1.34 % (2940499)Termination reason: Instruction limit
% 1.70/1.34 % (2940499)Termination phase: shuffling
% 1.70/1.34 % (2940499)Time elapsed: 0.040 s
% 1.70/1.34 % (2940499)Peak memory usage: 17 MB
% 1.70/1.34 % (2940499)Instructions burned: 89 (million)
% 1.70/1.34 % (2940514)Instruction limit reached!
% 1.70/1.34 % (2940514)------------------------------
% 1.70/1.34 % (2940514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/1.34 % (2940514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/1.34 % (2940514)CaDiCaL version: 2.1.3
% 1.70/1.34 % (2940514)Termination reason: Instruction limit
% 1.70/1.34 % (2940514)Termination phase: shuffling
% 1.70/1.34 % (2940514)Time elapsed: 0.007 s
% 1.70/1.34 % (2940514)Peak memory usage: 16 MB
% 1.70/1.34 % (2940514)Instructions burned: 6 (million)
% 1.70/1.34 % (2940513)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3080365843:i=2:hud=10:rtra=on_2997 on theBenchmark for (2997ds/2Mi)
% 1.70/1.34 % (2940516)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2710022077:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/12Mi)
% 1.70/1.34 % (2940515)Instruction limit reached!
% 1.70/1.34 % (2940515)------------------------------
% 1.70/1.34 % (2940515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/1.34 % (2940515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/1.34 % (2940515)CaDiCaL version: 2.1.3
% 1.70/1.34 % (2940515)Termination reason: Instruction limit
% 1.70/1.34 % (2940515)Termination phase: shuffling
% 1.70/1.34 % (2940515)Time elapsed: 0.009 s
% 1.70/1.34 % (2940515)Peak memory usage: 16 MB
% 1.70/1.34 % (2940515)Instructions burned: 9 (million)
% 1.70/1.34 % (2940513)Instruction limit reached!
% 1.70/1.34 % (2940513)------------------------------
% 1.70/1.34 % (2940513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/1.34 % (2940513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/1.34 % (2940513)CaDiCaL version: 2.1.3
% 1.70/1.34 % (2940513)Termination reason: Instruction limit
% 1.70/1.34 % (2940513)Termination phase: shuffling
% 1.70/1.34 % (2940513)Time elapsed: 0.004 s
% 1.70/1.34 % (2940513)Peak memory usage: 15 MB
% 1.70/1.34 % (2940513)Instructions burned: 2 (million)
% 1.70/1.34 % (2940516)Instruction limit reached!
% 1.70/1.34 % (2940516)------------------------------
% 1.70/1.34 % (2940516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/1.34 % (2940516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/1.34 % (2940516)CaDiCaL version: 2.1.3
% 1.70/1.34 % (2940516)Termination reason: Instruction limit
% 1.70/1.34 % (2940516)Termination phase: shuffling
% 1.70/1.34 % (2940516)Time elapsed: 0.006 s
% 1.70/1.34 % (2940516)Peak memory usage: 16 MB
% 1.70/1.34 % (2940516)Instructions burned: 13 (million)
% 1.70/1.34 % (2940519)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.70/1.34 % (2940519)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.70/1.34 % (2940524)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.70/1.34 % (2940519)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=4036441423:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2997 on theBenchmark for (2997ds/28Mi)
% 1.70/1.34 % (2940520)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=589942209:i=86:piset=equals:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/86Mi)
% 1.70/1.34 % (2940524)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=1923875389:i=2:add=on:rtra=on_2997 on theBenchmark for (2997ds/2Mi)
% 1.70/1.37 % (2940524)Instruction limit reached!
% 1.70/1.37 % (2940524)------------------------------
% 1.70/1.37 % (2940524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/1.37 % (2940524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/1.37 % (2940524)CaDiCaL version: 2.1.3
% 1.70/1.37 % (2940524)Termination reason: Instruction limit
% 1.70/1.37 % (2940524)Termination phase: shuffling
% 1.70/1.37 % (2940524)Time elapsed: 0.004 s
% 1.70/1.37 % (2940524)Peak memory usage: 16 MB
% 1.70/1.37 % (2940524)Instructions burned: 3 (million)
% 1.70/1.37 % (2940523)lrs+10_1_si=on:cs=on:random_seed=1185757702:i=8:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/8Mi)
% 1.70/1.37 % (2940525)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2657737060:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/38Mi)
% 1.70/1.37 % (2940505)Instruction limit reached!
% 1.70/1.37 % (2940505)------------------------------
% 1.70/1.37 % (2940505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/1.37 % (2940505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/1.37 % (2940505)CaDiCaL version: 2.1.3
% 1.70/1.37 % (2940505)Termination reason: Instruction limit
% 1.70/1.37 % (2940505)Termination phase: shuffling
% 1.70/1.37 % (2940505)Time elapsed: 0.070 s
% 1.70/1.37 % (2940505)Peak memory usage: 18 MB
% 1.70/1.37 % (2940505)Instructions burned: 158 (million)
% 1.70/1.37 % (2940523)Instruction limit reached!
% 1.70/1.37 % (2940523)------------------------------
% 1.70/1.37 % (2940523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/1.37 % (2940523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/1.37 % (2940523)CaDiCaL version: 2.1.3
% 1.70/1.37 % (2940523)Termination reason: Instruction limit
% 1.70/1.37 % (2940523)Termination phase: shuffling
% 1.70/1.37 % (2940523)Time elapsed: 0.009 s
% 1.70/1.37 % (2940523)Peak memory usage: 16 MB
% 1.70/1.37 % (2940523)Instructions burned: 10 (million)
% 1.70/1.37 % (2940529)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=622434150:st=2:i=249:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/249Mi)
% 1.70/1.37 % (2940519)Instruction limit reached!
% 1.70/1.37 % (2940519)------------------------------
% 1.70/1.37 % (2940519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/1.37 % (2940519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/1.37 % (2940519)CaDiCaL version: 2.1.3
% 1.70/1.37 % (2940519)Termination reason: Instruction limit
% 1.70/1.37 % (2940519)Termination phase: shuffling
% 1.70/1.37 % (2940519)Time elapsed: 0.017 s
% 1.70/1.37 % (2940519)Peak memory usage: 17 MB
% 1.70/1.37 % (2940519)Instructions burned: 29 (million)
% 1.70/1.37 % (2940525)Instruction limit reached!
% 1.70/1.37 % (2940525)------------------------------
% 1.70/1.37 % (2940525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/1.37 % (2940525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/1.37 % (2940525)CaDiCaL version: 2.1.3
% 1.70/1.37 % (2940525)Termination reason: Instruction limit
% 1.70/1.37 % (2940525)Termination phase: shuffling
% 1.70/1.37 % (2940525)Time elapsed: 0.020 s
% 1.70/1.37 % (2940525)Peak memory usage: 16 MB
% 1.70/1.37 % (2940525)Instructions burned: 39 (million)
% 1.70/1.37 % (2940535)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3065288066:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/327Mi)
% 1.70/1.37 % (2940520)Instruction limit reached!
% 1.70/1.37 % (2940520)------------------------------
% 1.70/1.37 % (2940520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/1.37 % (2940520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/1.37 % (2940520)CaDiCaL version: 2.1.3
% 1.70/1.37 % (2940520)Termination reason: Instruction limit
% 1.70/1.37 % (2940520)Termination phase: shuffling
% 1.70/1.37 % (2940520)Time elapsed: 0.041 s
% 1.70/1.37 % (2940520)Peak memory usage: 17 MB
% 1.70/1.37 % (2940520)Instructions burned: 87 (million)
% 1.70/1.37 % (2940532)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2467458341:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/25Mi)
% 2.21/1.44 % (2940534)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2467405948:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2997 on theBenchmark for (2997ds/14Mi)
% 2.21/1.44 % (2940536)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2503937358:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/14Mi)
% 2.21/1.44 % (2940532)Instruction limit reached!
% 2.21/1.44 % (2940532)------------------------------
% 2.21/1.44 % (2940532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/1.44 % (2940532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/1.44 % (2940532)CaDiCaL version: 2.1.3
% 2.21/1.44 % (2940532)Termination reason: Instruction limit
% 2.21/1.44 % (2940532)Termination phase: shuffling
% 2.21/1.44 % (2940532)Time elapsed: 0.016 s
% 2.21/1.44 % (2940532)Peak memory usage: 17 MB
% 2.21/1.44 % (2940532)Instructions burned: 27 (million)
% 2.21/1.44 % (2940534)Instruction limit reached!
% 2.21/1.44 % (2940534)------------------------------
% 2.21/1.44 % (2940534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/1.44 % (2940534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/1.44 % (2940534)CaDiCaL version: 2.1.3
% 2.21/1.44 % (2940534)Termination reason: Instruction limit
% 2.21/1.44 % (2940534)Termination phase: shuffling
% 2.21/1.44 % (2940534)Time elapsed: 0.012 s
% 2.21/1.44 % (2940534)Peak memory usage: 16 MB
% 2.21/1.44 % (2940534)Instructions burned: 15 (million)
% 2.21/1.44 % (2940539)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=4098358714:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2996 on theBenchmark for (2996ds/2Mi)
% 2.21/1.44 % (2940536)Instruction limit reached!
% 2.21/1.44 % (2940536)------------------------------
% 2.21/1.44 % (2940536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/1.44 % (2940536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/1.44 % (2940536)CaDiCaL version: 2.1.3
% 2.21/1.44 % (2940536)Termination reason: Instruction limit
% 2.21/1.44 % (2940536)Termination phase: shuffling
% 2.21/1.44 % (2940536)Time elapsed: 0.011 s
% 2.21/1.44 % (2940536)Peak memory usage: 16 MB
% 2.21/1.44 % (2940536)Instructions burned: 16 (million)
% 2.21/1.44 % (2940539)Instruction limit reached!
% 2.21/1.44 % (2940539)------------------------------
% 2.21/1.44 % (2940539)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/1.44 % (2940539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/1.44 % (2940539)CaDiCaL version: 2.1.3
% 2.21/1.44 % (2940539)Termination reason: Instruction limit
% 2.21/1.44 % (2940539)Termination phase: shuffling
% 2.21/1.44 % (2940539)Time elapsed: 0.004 s
% 2.21/1.44 % (2940539)Peak memory usage: 15 MB
% 2.21/1.44 % (2940539)Instructions burned: 2 (million)
% 2.21/1.44 % (2940529)Instruction limit reached!
% 2.21/1.44 % (2940529)------------------------------
% 2.21/1.44 % (2940529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.21/1.44 % (2940529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.21/1.44 % (2940529)CaDiCaL version: 2.1.3
% 2.21/1.44 % (2940529)Termination reason: Instruction limit
% 2.21/1.44 % (2940529)Termination phase: shuffling
% 2.21/1.44 % (2940529)Time elapsed: 0.057 s
% 2.21/1.44 % (2940529)Peak memory usage: 19 MB
% 2.21/1.44 % (2940529)Instructions burned: 253 (million)
% 2.21/1.44 % (2940542)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1151335404:i=26:ep=R:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/26Mi)
% 2.21/1.44 % (2940545)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=909078568:cond=on:i=60:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/60Mi)
% 2.21/1.44 % (2940547)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.21/1.44 % (2940543)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=2974210943:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2996 on theBenchmark for (2996ds/23Mi)
% 2.21/1.44 % (2940547)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=933180315:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2996 on theBenchmark for (2996ds/8Mi)
% 2.69/1.51 % (2940542)Instruction limit reached!
% 2.69/1.51 % (2940542)------------------------------
% 2.69/1.51 % (2940542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/1.51 % (2940542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/1.51 % (2940542)CaDiCaL version: 2.1.3
% 2.69/1.51 % (2940542)Termination reason: Instruction limit
% 2.69/1.51 % (2940542)Termination phase: shuffling
% 2.69/1.51 % (2940542)Time elapsed: 0.017 s
% 2.69/1.51 % (2940542)Peak memory usage: 16 MB
% 2.69/1.51 % (2940542)Instructions burned: 28 (million)
% 2.69/1.51 % (2940546)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.69/1.51 % (2940546)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.69/1.51 % (2940547)Instruction limit reached!
% 2.69/1.51 % (2940547)------------------------------
% 2.69/1.51 % (2940547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/1.51 % (2940547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/1.51 % (2940547)CaDiCaL version: 2.1.3
% 2.69/1.51 % (2940547)Termination reason: Instruction limit
% 2.69/1.51 % (2940547)Termination phase: shuffling
% 2.69/1.51 % (2940547)Time elapsed: 0.009 s
% 2.69/1.51 % (2940547)Peak memory usage: 16 MB
% 2.69/1.51 % (2940547)Instructions burned: 10 (million)
% 2.69/1.51 % (2940546)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=3893609339:i=14:add=off:nm=40:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/14Mi)
% 2.69/1.51 % (2940545)Instruction limit reached!
% 2.69/1.51 % (2940545)------------------------------
% 2.69/1.51 % (2940545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/1.51 % (2940545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/1.51 % (2940545)CaDiCaL version: 2.1.3
% 2.69/1.51 % (2940545)Termination reason: Instruction limit
% 2.69/1.51 % (2940545)Termination phase: shuffling
% 2.69/1.51 % (2940545)Time elapsed: 0.030 s
% 2.69/1.51 % (2940545)Peak memory usage: 17 MB
% 2.69/1.51 % (2940545)Instructions burned: 62 (million)
% 2.69/1.51 % (2940552)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=3733098645:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2996 on theBenchmark for (2996ds/31Mi)
% 2.69/1.51 % (2940553)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=4002203232:i=7:hud=5:bd=preordered:rtra=on:bet=on_2996 on theBenchmark for (2996ds/7Mi)
% 2.69/1.51 % (2940543)Instruction limit reached!
% 2.69/1.51 % (2940543)------------------------------
% 2.69/1.51 % (2940543)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/1.51 % (2940543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/1.51 % (2940543)CaDiCaL version: 2.1.3
% 2.69/1.51 % (2940543)Termination reason: Instruction limit
% 2.69/1.51 % (2940543)Termination phase: shuffling
% 2.69/1.51 % (2940543)Time elapsed: 0.033 s
% 2.69/1.51 % (2940543)Peak memory usage: 16 MB
% 2.69/1.51 % (2940543)Instructions burned: 24 (million)
% 2.69/1.51 % (2940546)Instruction limit reached!
% 2.69/1.51 % (2940546)------------------------------
% 2.69/1.51 % (2940546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/1.51 % (2940546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/1.51 % (2940546)CaDiCaL version: 2.1.3
% 2.69/1.51 % (2940546)Termination reason: Instruction limit
% 2.69/1.51 % (2940546)Termination phase: shuffling
% 2.69/1.51 % (2940546)Time elapsed: 0.022 s
% 2.69/1.51 % (2940546)Peak memory usage: 16 MB
% 2.69/1.51 % (2940546)Instructions burned: 16 (million)
% 2.69/1.51 % (2940553)Instruction limit reached!
% 2.69/1.51 % (2940553)------------------------------
% 2.69/1.51 % (2940553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/1.51 % (2940553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/1.51 % (2940553)CaDiCaL version: 2.1.3
% 2.69/1.51 % (2940553)Termination reason: Instruction limit
% 2.69/1.51 % (2940553)Termination phase: shuffling
% 2.69/1.51 % (2940553)Time elapsed: 0.008 s
% 2.69/1.51 % (2940553)Peak memory usage: 16 MB
% 2.69/1.51 % (2940553)Instructions burned: 9 (million)
% 3.06/1.60 % (2940555)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1441658907:i=23:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/23Mi)
% 3.06/1.60 % (2940552)Instruction limit reached!
% 3.06/1.60 % (2940552)------------------------------
% 3.06/1.60 % (2940552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.06/1.60 % (2940552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/1.60 % (2940552)CaDiCaL version: 2.1.3
% 3.06/1.60 % (2940552)Termination reason: Instruction limit
% 3.06/1.60 % (2940552)Termination phase: shuffling
% 3.06/1.60 % (2940552)Time elapsed: 0.019 s
% 3.06/1.60 % (2940552)Peak memory usage: 17 MB
% 3.06/1.60 % (2940552)Instructions burned: 33 (million)
% 3.06/1.60 % (2940558)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=801727977:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2995 on theBenchmark for (2995ds/20Mi)
% 3.06/1.60 % (2940555)Instruction limit reached!
% 3.06/1.60 % (2940555)------------------------------
% 3.06/1.60 % (2940555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.06/1.60 % (2940555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/1.60 % (2940555)CaDiCaL version: 2.1.3
% 3.06/1.60 % (2940555)Termination reason: Instruction limit
% 3.06/1.60 % (2940555)Termination phase: shuffling
% 3.06/1.60 % (2940555)Time elapsed: 0.016 s
% 3.06/1.60 % (2940555)Peak memory usage: 16 MB
% 3.06/1.60 % (2940555)Instructions burned: 25 (million)
% 3.06/1.60 % (2940559)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2187074376:i=1240:rtra=on:ixr=off_2995 on theBenchmark for (2995ds/1240Mi)
% 3.06/1.60 % (2940560)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=4013745228:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2995 on theBenchmark for (2995ds/143Mi)
% 3.06/1.60 % (2940562)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1622396710:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/193Mi)
% 3.06/1.60 % (2940558)Instruction limit reached!
% 3.06/1.60 % (2940558)------------------------------
% 3.06/1.60 % (2940558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.06/1.60 % (2940558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/1.60 % (2940558)CaDiCaL version: 2.1.3
% 3.06/1.60 % (2940558)Termination reason: Instruction limit
% 3.06/1.60 % (2940558)Termination phase: shuffling
% 3.06/1.60 % (2940558)Time elapsed: 0.016 s
% 3.06/1.60 % (2940558)Peak memory usage: 17 MB
% 3.06/1.60 % (2940558)Instructions burned: 24 (million)
% 3.06/1.60 % (2940535)Instruction limit reached!
% 3.06/1.60 % (2940535)------------------------------
% 3.06/1.60 % (2940535)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.06/1.60 % (2940535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/1.60 % (2940535)CaDiCaL version: 2.1.3
% 3.06/1.60 % (2940535)Termination reason: Instruction limit
% 3.06/1.60 % (2940535)Termination phase: shuffling
% 3.06/1.60 % (2940535)Time elapsed: 0.134 s
% 3.06/1.60 % (2940535)Peak memory usage: 19 MB
% 3.06/1.60 % (2940535)Instructions burned: 327 (million)
% 3.06/1.60 % (2940564)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2966237240:i=42:hud=10:rtra=on_2995 on theBenchmark for (2995ds/42Mi)
% 3.06/1.60 % (2940568)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 3.06/1.60 % (2940568)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1765566156:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2995 on theBenchmark for (2995ds/7Mi)
% 3.06/1.60 % (2940570)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=1953845034:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/181Mi)
% 3.06/1.60 % (2940564)Instruction limit reached!
% 3.06/1.60 % (2940564)------------------------------
% 3.06/1.60 % (2940564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.06/1.60 % (2940564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/1.60 % (2940564)CaDiCaL version: 2.1.3
% 3.06/1.60 % (2940564)Termination reason: Instruction limit
% 3.06/1.60 % (2940564)Termination phase: shuffling
% 3.06/1.60 % (2940564)Time elapsed: 0.022 s
% 3.06/1.60 % (2940564)Peak memory usage: 17 MB
% 3.06/1.60 % (2940564)Instructions burned: 42 (million)
% 3.06/1.69 % (2940568)Instruction limit reached!
% 3.06/1.69 % (2940568)------------------------------
% 3.06/1.69 % (2940568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.06/1.69 % (2940568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/1.69 % (2940568)CaDiCaL version: 2.1.3
% 3.06/1.69 % (2940568)Termination reason: Instruction limit
% 3.06/1.69 % (2940568)Termination phase: shuffling
% 3.06/1.69 % (2940568)Time elapsed: 0.009 s
% 3.06/1.69 % (2940568)Peak memory usage: 16 MB
% 3.06/1.69 % (2940568)Instructions burned: 8 (million)
% 3.06/1.69 % (2940574)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 3.06/1.69 % (2940560)Instruction limit reached!
% 3.06/1.69 % (2940560)------------------------------
% 3.06/1.69 % (2940560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.06/1.69 % (2940560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/1.69 % (2940573)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=1330649625:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2995 on theBenchmark for (2995ds/169Mi)
% 3.06/1.69 % (2940560)CaDiCaL version: 2.1.3
% 3.06/1.69 % (2940560)Termination reason: Instruction limit
% 3.06/1.69 % (2940560)Termination phase: shuffling
% 3.06/1.69 % (2940560)Time elapsed: 0.062 s
% 3.06/1.69 % (2940560)Peak memory usage: 17 MB
% 3.06/1.69 % (2940560)Instructions burned: 145 (million)
% 3.06/1.69 % (2940574)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=333195603:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2995 on theBenchmark for (2995ds/6Mi)
% 3.06/1.69 % (2940574)Instruction limit reached!
% 3.06/1.69 % (2940574)------------------------------
% 3.06/1.69 % (2940574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.06/1.69 % (2940574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/1.69 % (2940574)CaDiCaL version: 2.1.3
% 3.06/1.69 % (2940574)Termination reason: Instruction limit
% 3.06/1.69 % (2940574)Termination phase: shuffling
% 3.06/1.69 % (2940574)Time elapsed: 0.012 s
% 3.06/1.69 % (2940574)Peak memory usage: 16 MB
% 3.06/1.69 % (2940574)Instructions burned: 6 (million)
% 3.06/1.69 % (2940562)Instruction limit reached!
% 3.06/1.69 % (2940562)------------------------------
% 3.06/1.69 % (2940562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.06/1.69 % (2940562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/1.69 % (2940562)CaDiCaL version: 2.1.3
% 3.06/1.69 % (2940562)Termination reason: Instruction limit
% 3.06/1.69 % (2940562)Termination phase: shuffling
% 3.06/1.69 % (2940562)Time elapsed: 0.082 s
% 3.06/1.69 % (2940562)Peak memory usage: 18 MB
% 3.06/1.69 % (2940562)Instructions burned: 195 (million)
% 3.06/1.69 % (2940577)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1333925580:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2995 on theBenchmark for (2995ds/22Mi)
% 3.06/1.69 % (2940579)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=1901478030:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/316Mi)
% 3.06/1.69 % (2940577)Instruction limit reached!
% 3.06/1.69 % (2940577)------------------------------
% 3.06/1.69 % (2940577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.06/1.69 % (2940577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/1.69 % (2940577)CaDiCaL version: 2.1.3
% 3.06/1.69 % (2940577)Termination reason: Instruction limit
% 3.06/1.69 % (2940577)Termination phase: shuffling
% 3.06/1.69 % (2940577)Time elapsed: 0.019 s
% 3.06/1.69 % (2940577)Peak memory usage: 16 MB
% 3.06/1.69 % (2940577)Instructions burned: 24 (million)
% 3.06/1.69 % (2940578)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=58243996:i=19:add=on:rtra=on_2994 on theBenchmark for (2994ds/19Mi)
% 3.06/1.69 % (2940570)Instruction limit reached!
% 3.06/1.69 % (2940570)------------------------------
% 3.06/1.69 % (2940570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.06/1.69 % (2940570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.30/1.79 % (2940570)CaDiCaL version: 2.1.3
% 4.30/1.79 % (2940570)Termination reason: Instruction limit
% 4.30/1.79 % (2940570)Termination phase: shuffling
% 4.30/1.79 % (2940570)Time elapsed: 0.076 s
% 4.30/1.79 % (2940570)Peak memory usage: 18 MB
% 4.30/1.79 % (2940570)Instructions burned: 182 (million)
% 4.30/1.79 % (2940582)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=3498904504:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2994 on theBenchmark for (2994ds/853Mi)
% 4.30/1.79 % (2940573)Instruction limit reached!
% 4.30/1.79 % (2940573)------------------------------
% 4.30/1.79 % (2940573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.30/1.79 % (2940573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.30/1.79 % (2940573)CaDiCaL version: 2.1.3
% 4.30/1.79 % (2940573)Termination reason: Instruction limit
% 4.30/1.79 % (2940573)Termination phase: shuffling
% 4.30/1.79 % (2940573)Time elapsed: 0.072 s
% 4.30/1.79 % (2940573)Peak memory usage: 18 MB
% 4.30/1.79 % (2940573)Instructions burned: 169 (million)
% 4.30/1.79 % (2940578)Instruction limit reached!
% 4.30/1.79 % (2940578)------------------------------
% 4.30/1.79 % (2940578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.30/1.79 % (2940578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.30/1.79 % (2940578)CaDiCaL version: 2.1.3
% 4.30/1.79 % (2940578)Termination reason: Instruction limit
% 4.30/1.79 % (2940578)Termination phase: shuffling
% 4.30/1.79 % (2940578)Time elapsed: 0.022 s
% 4.30/1.79 % (2940578)Peak memory usage: 16 MB
% 4.30/1.79 % (2940578)Instructions burned: 19 (million)
% 4.30/1.79 % (2940584)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=297908432: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)
% 4.30/1.79 % (2940586)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=4245162272:i=480:rtra=on_2994 on theBenchmark for (2994ds/480Mi)
% 4.30/1.79 % (2940588)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=2519673825: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)
% 4.30/1.79 % (2940584)Instruction limit reached!
% 4.30/1.79 % (2940584)------------------------------
% 4.30/1.79 % (2940584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.30/1.79 % (2940584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.30/1.79 % (2940584)CaDiCaL version: 2.1.3
% 4.30/1.79 % (2940584)Termination reason: Instruction limit
% 4.30/1.79 % (2940584)Termination phase: Property scanning
% 4.30/1.79 % (2940584)Time elapsed: 0.022 s
% 4.30/1.79 % (2940584)Peak memory usage: 16 MB
% 4.30/1.79 % (2940584)Instructions burned: 45 (million)
% 4.30/1.79 % (2940588)Instruction limit reached!
% 4.30/1.79 % (2940588)------------------------------
% 4.30/1.79 % (2940588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.30/1.79 % (2940588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.30/1.79 % (2940588)CaDiCaL version: 2.1.3
% 4.30/1.79 % (2940588)Termination reason: Instruction limit
% 4.30/1.79 % (2940588)Termination phase: shuffling
% 4.30/1.79 % (2940588)Time elapsed: 0.014 s
% 4.30/1.79 % (2940588)Peak memory usage: 17 MB
% 4.30/1.79 % (2940588)Instructions burned: 23 (million)
% 4.30/1.79 % (2940591)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 4.30/1.79 % (2940591)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=2460611317:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/200Mi)
% 4.30/1.79 % (2940592)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=4210921538:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2993 on theBenchmark for (2993ds/13Mi)
% 4.30/1.79 % (2940592)Instruction limit reached!
% 4.30/1.79 % (2940592)------------------------------
% 4.30/1.79 % (2940592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.30/1.79 % (2940592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.30/1.79 % (2940592)CaDiCaL version: 2.1.3
% 4.63/1.89 % (2940592)Termination reason: Instruction limit
% 4.63/1.89 % (2940592)Termination phase: shuffling
% 4.63/1.89 % (2940592)Time elapsed: 0.010 s
% 4.63/1.89 % (2940592)Peak memory usage: 16 MB
% 4.63/1.89 % (2940592)Instructions burned: 13 (million)
% 4.63/1.89 % (2940595)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=1319542161:i=66:s2at=3:nm=2:rtra=on:rawr=on_2993 on theBenchmark for (2993ds/66Mi)
% 4.63/1.89 % (2940579)Instruction limit reached!
% 4.63/1.89 % (2940579)------------------------------
% 4.63/1.89 % (2940579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.63/1.89 % (2940579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.89 % (2940579)CaDiCaL version: 2.1.3
% 4.63/1.89 % (2940579)Termination reason: Instruction limit
% 4.63/1.89 % (2940579)Termination phase: shuffling
% 4.63/1.89 % (2940579)Time elapsed: 0.140 s
% 4.63/1.89 % (2940579)Peak memory usage: 21 MB
% 4.63/1.89 % (2940579)Instructions burned: 318 (million)
% 4.63/1.89 % (2940502)Instruction limit reached!
% 4.63/1.89 % (2940502)------------------------------
% 4.63/1.89 % (2940502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.63/1.89 % (2940502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.89 % (2940502)CaDiCaL version: 2.1.3
% 4.63/1.89 % (2940502)Termination reason: Instruction limit
% 4.63/1.89 % (2940502)Termination phase: shuffling
% 4.63/1.89 % (2940502)Time elapsed: 0.470 s
% 4.63/1.89 % (2940502)Peak memory usage: 18 MB
% 4.63/1.89 % (2940502)Instructions burned: 635 (million)
% 4.63/1.89 % (2940595)Instruction limit reached!
% 4.63/1.89 % (2940595)------------------------------
% 4.63/1.89 % (2940595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.63/1.89 % (2940595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.89 % (2940595)CaDiCaL version: 2.1.3
% 4.63/1.89 % (2940595)Termination reason: Instruction limit
% 4.63/1.89 % (2940595)Termination phase: shuffling
% 4.63/1.89 % (2940595)Time elapsed: 0.034 s
% 4.63/1.89 % (2940595)Peak memory usage: 17 MB
% 4.63/1.89 % (2940595)Instructions burned: 68 (million)
% 4.63/1.89 % (2940591)Instruction limit reached!
% 4.63/1.89 % (2940591)------------------------------
% 4.63/1.89 % (2940591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.63/1.89 % (2940591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.89 % (2940591)CaDiCaL version: 2.1.3
% 4.63/1.89 % (2940591)Termination reason: Instruction limit
% 4.63/1.89 % (2940591)Termination phase: shuffling
% 4.63/1.89 % (2940591)Time elapsed: 0.084 s
% 4.63/1.89 % (2940591)Peak memory usage: 18 MB
% 4.63/1.89 % (2940591)Instructions burned: 201 (million)
% 4.63/1.89 % (2940598)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3528976864:i=51:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/51Mi)
% 4.63/1.89 % (2940599)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2096724302:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/31Mi)
% 4.63/1.89 % (2940600)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=1529302400:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2993 on theBenchmark for (2993ds/137Mi)
% 4.63/1.89 % (2940559)Instruction limit reached!
% 4.63/1.89 % (2940559)------------------------------
% 4.63/1.89 % (2940559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.63/1.89 % (2940559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.89 % (2940559)CaDiCaL version: 2.1.3
% 4.63/1.89 % (2940559)Termination reason: Instruction limit
% 4.63/1.89 % (2940559)Termination phase: Property scanning
% 4.63/1.89 % (2940559)Time elapsed: 0.282 s
% 4.63/1.89 % (2940559)Peak memory usage: 28 MB
% 4.63/1.89 % (2940559)Instructions burned: 1242 (million)
% 4.63/1.89 % (2940601)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=3496186061:cond=on:i=34:hud=10:nm=10:rtra=on_2993 on theBenchmark for (2993ds/34Mi)
% 4.63/1.89 % (2940599)Instruction limit reached!
% 4.63/1.89 % (2940599)------------------------------
% 4.63/1.89 % (2940599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.63/1.89 % (2940599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.89 % (2940599)CaDiCaL version: 2.1.3
% 5.72/2.02 % (2940599)Termination reason: Instruction limit
% 5.72/2.02 % (2940599)Termination phase: shuffling
% 5.72/2.02 % (2940599)Time elapsed: 0.019 s
% 5.72/2.02 % (2940599)Peak memory usage: 17 MB
% 5.72/2.02 % (2940599)Instructions burned: 33 (million)
% 5.72/2.02 % (2940598)Instruction limit reached!
% 5.72/2.02 % (2940598)------------------------------
% 5.72/2.02 % (2940598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.72/2.02 % (2940598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/2.02 % (2940598)CaDiCaL version: 2.1.3
% 5.72/2.02 % (2940598)Termination reason: Instruction limit
% 5.72/2.02 % (2940598)Termination phase: shuffling
% 5.72/2.02 % (2940598)Time elapsed: 0.026 s
% 5.72/2.02 % (2940598)Peak memory usage: 17 MB
% 5.72/2.02 % (2940598)Instructions burned: 53 (million)
% 5.72/2.02 % (2940605)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=1724827142:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2992 on theBenchmark for (2992ds/67Mi)
% 5.72/2.02 % (2940601)Instruction limit reached!
% 5.72/2.02 % (2940601)------------------------------
% 5.72/2.02 % (2940601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.72/2.02 % (2940601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/2.02 % (2940601)CaDiCaL version: 2.1.3
% 5.72/2.02 % (2940601)Termination reason: Instruction limit
% 5.72/2.02 % (2940601)Termination phase: shuffling
% 5.72/2.02 % (2940601)Time elapsed: 0.019 s
% 5.72/2.02 % (2940601)Peak memory usage: 17 MB
% 5.72/2.02 % (2940601)Instructions burned: 34 (million)
% 5.72/2.02 % (2940607)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.72/2.02 % (2940607)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=1423343394:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2992 on theBenchmark for (2992ds/180Mi)
% 5.72/2.02 % (2940605)Instruction limit reached!
% 5.72/2.02 % (2940605)------------------------------
% 5.72/2.02 % (2940605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.72/2.02 % (2940605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/2.02 % (2940605)CaDiCaL version: 2.1.3
% 5.72/2.03 % (2940605)Termination reason: Instruction limit
% 5.72/2.03 % (2940605)Termination phase: shuffling
% 5.72/2.03 % (2940605)Time elapsed: 0.018 s
% 5.72/2.03 % (2940605)Peak memory usage: 17 MB
% 5.72/2.03 % (2940605)Instructions burned: 71 (million)
% 5.72/2.03 % (2940609)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=2740791589:st=2:i=246:sd=3:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/246Mi)
% 5.72/2.03 % (2940612)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=3228657164:i=427:sd=1:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/427Mi)
% 5.72/2.03 % (2940610)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=913899845:cond=on:i=96:bd=all:rtra=on_2992 on theBenchmark for (2992ds/96Mi)
% 5.72/2.03 % (2940600)Instruction limit reached!
% 5.72/2.03 % (2940600)------------------------------
% 5.72/2.03 % (2940600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.72/2.03 % (2940600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/2.03 % (2940600)CaDiCaL version: 2.1.3
% 5.72/2.03 % (2940600)Termination reason: Instruction limit
% 5.72/2.03 % (2940600)Termination phase: shuffling
% 5.72/2.03 % (2940600)Time elapsed: 0.059 s
% 5.72/2.03 % (2940600)Peak memory usage: 18 MB
% 5.72/2.03 % (2940600)Instructions burned: 137 (million)
% 5.72/2.03 % (2940616)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3999459720:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/874Mi)
% 5.72/2.03 % (2940610)Instruction limit reached!
% 5.72/2.03 % (2940610)------------------------------
% 5.72/2.03 % (2940610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.72/2.03 % (2940610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/2.03 % (2940610)CaDiCaL version: 2.1.3
% 5.72/2.03 % (2940610)Termination reason: Instruction limit
% 5.72/2.03 % (2940610)Termination phase: shuffling
% 5.72/2.03 % (2940610)Time elapsed: 0.043 s
% 5.72/2.03 % (2940610)Peak memory usage: 17 MB
% 5.72/2.03 % (2940610)Instructions burned: 97 (million)
% 5.72/2.03 % (2940618)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=3021998150:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/515Mi)
% 5.72/2.03 % (2940607)Instruction limit reached!
% 7.19/2.11 % (2940607)------------------------------
% 7.19/2.11 % (2940607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/2.11 % (2940607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/2.11 % (2940607)CaDiCaL version: 2.1.3
% 7.19/2.11 % (2940607)Termination reason: Instruction limit
% 7.19/2.11 % (2940607)Termination phase: shuffling
% 7.19/2.11 % (2940607)Time elapsed: 0.082 s
% 7.19/2.11 % (2940607)Peak memory usage: 19 MB
% 7.19/2.11 % (2940607)Instructions burned: 182 (million)
% 7.19/2.11 % (2940620)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=750818850:st=1.5:i=130:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/130Mi)
% 7.19/2.11 % (2940609)Instruction limit reached!
% 7.19/2.11 % (2940609)------------------------------
% 7.19/2.11 % (2940609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/2.11 % (2940609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/2.11 % (2940609)CaDiCaL version: 2.1.3
% 7.19/2.11 % (2940609)Termination reason: Instruction limit
% 7.19/2.11 % (2940609)Termination phase: shuffling
% 7.19/2.11 % (2940609)Time elapsed: 0.101 s
% 7.19/2.11 % (2940609)Peak memory usage: 18 MB
% 7.19/2.11 % (2940609)Instructions burned: 248 (million)
% 7.19/2.11 % (2940612)Instruction limit reached!
% 7.19/2.11 % (2940612)------------------------------
% 7.19/2.11 % (2940612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/2.11 % (2940612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/2.11 % (2940612)CaDiCaL version: 2.1.3
% 7.19/2.11 % (2940612)Termination reason: Instruction limit
% 7.19/2.11 % (2940612)Termination phase: shuffling
% 7.19/2.11 % (2940612)Time elapsed: 0.093 s
% 7.19/2.11 % (2940612)Peak memory usage: 20 MB
% 7.19/2.11 % (2940612)Instructions burned: 430 (million)
% 7.19/2.11 % (2940623)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=1224451181:s2a=on:i=571:nm=16:rtra=on_2991 on theBenchmark for (2991ds/571Mi)
% 7.19/2.11 % (2940622)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1056674516:i=44:ep=R:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/44Mi)
% 7.19/2.11 % (2940622)Instruction limit reached!
% 7.19/2.11 % (2940622)------------------------------
% 7.19/2.11 % (2940622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/2.11 % (2940622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/2.11 % (2940622)CaDiCaL version: 2.1.3
% 7.19/2.11 % (2940622)Termination reason: Instruction limit
% 7.19/2.11 % (2940622)Termination phase: shuffling
% 7.19/2.11 % (2940622)Time elapsed: 0.023 s
% 7.19/2.11 % (2940622)Peak memory usage: 17 MB
% 7.19/2.11 % (2940622)Instructions burned: 45 (million)
% 7.19/2.11 % (2940582)Instruction limit reached!
% 7.19/2.11 % (2940582)------------------------------
% 7.19/2.11 % (2940582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/2.11 % (2940582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/2.11 % (2940582)CaDiCaL version: 2.1.3
% 7.19/2.11 % (2940582)Termination reason: Instruction limit
% 7.19/2.11 % (2940582)Termination phase: shuffling
% 7.19/2.11 % (2940582)Time elapsed: 0.341 s
% 7.19/2.11 % (2940582)Peak memory usage: 22 MB
% 7.19/2.11 % (2940582)Instructions burned: 853 (million)
% 7.19/2.11 % (2940620)Instruction limit reached!
% 7.19/2.11 % (2940620)------------------------------
% 7.19/2.11 % (2940620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/2.11 % (2940620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/2.11 % (2940620)CaDiCaL version: 2.1.3
% 7.19/2.11 % (2940620)Termination reason: Instruction limit
% 7.19/2.11 % (2940620)Termination phase: shuffling
% 7.19/2.11 % (2940620)Time elapsed: 0.061 s
% 7.19/2.11 % (2940620)Peak memory usage: 18 MB
% 7.19/2.11 % (2940620)Instructions burned: 132 (million)
% 7.19/2.11 % (2940626)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=737461946:i=450:rtra=on:ixr=off:ntd=on_2991 on theBenchmark for (2991ds/450Mi)
% 7.19/2.11 % (2940586)Instruction limit reached!
% 7.19/2.11 % (2940586)------------------------------
% 7.19/2.11 % (2940586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.19/2.11 % (2940586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.19/2.11 % (2940586)CaDiCaL version: 2.1.3
% 7.71/2.19 % (2940586)Termination reason: Instruction limit
% 7.71/2.19 % (2940586)Termination phase: shuffling
% 7.71/2.19 % (2940586)Time elapsed: 0.335 s
% 7.71/2.19 % (2940586)Peak memory usage: 21 MB
% 7.71/2.19 % (2940586)Instructions burned: 481 (million)
% 7.71/2.19 % (2940627)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=4034777994:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/95Mi)
% 7.71/2.19 % (2940628)lrs+1003_1_sil=128000:drc=off:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:fd=off:rp=on:sac=on:random_seed=2870878980:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2990 on theBenchmark for (2990ds/65Mi)
% 7.71/2.19 % (2940630)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=3786101061:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2990 on theBenchmark for (2990ds/105Mi)
% 7.71/2.19 % (2940627)Instruction limit reached!
% 7.71/2.19 % (2940627)------------------------------
% 7.71/2.19 % (2940627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.71/2.19 % (2940627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.71/2.19 % (2940627)CaDiCaL version: 2.1.3
% 7.71/2.19 % (2940627)Termination reason: Instruction limit
% 7.71/2.19 % (2940627)Termination phase: shuffling
% 7.71/2.19 % (2940627)Time elapsed: 0.044 s
% 7.71/2.19 % (2940627)Peak memory usage: 17 MB
% 7.71/2.19 % (2940627)Instructions burned: 97 (million)
% 7.71/2.19 % (2940628)Instruction limit reached!
% 7.71/2.19 % (2940628)------------------------------
% 7.71/2.19 % (2940628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.71/2.19 % (2940628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.71/2.19 % (2940628)CaDiCaL version: 2.1.3
% 7.71/2.19 % (2940628)Termination reason: Instruction limit
% 7.71/2.19 % (2940628)Termination phase: shuffling
% 7.71/2.19 % (2940628)Time elapsed: 0.032 s
% 7.71/2.19 % (2940628)Peak memory usage: 17 MB
% 7.71/2.19 % (2940628)Instructions burned: 66 (million)
% 7.71/2.19 % (2940623)Instruction limit reached!
% 7.71/2.19 % (2940623)------------------------------
% 7.71/2.19 % (2940623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.71/2.19 % (2940623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.71/2.19 % (2940623)CaDiCaL version: 2.1.3
% 7.71/2.19 % (2940623)Termination reason: Instruction limit
% 7.71/2.19 % (2940623)Termination phase: shuffling
% 7.71/2.19 % (2940623)Time elapsed: 0.125 s
% 7.71/2.19 % (2940623)Peak memory usage: 22 MB
% 7.71/2.19 % (2940623)Instructions burned: 576 (million)
% 7.71/2.19 % (2940634)dis+10_4:1_sfv=off:to=kbo:fde=unused:cnfonf=off:sas=cadical:e2e=on:si=on:sp=occurrence:acc=on:uwa=off:fd=preordered:foolp=on:random_seed=2471038422:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2990 on theBenchmark for (2990ds/5755Mi)
% 7.71/2.19 % (2940635)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=1847712484:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/375Mi)
% 7.71/2.19 % (2940636)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=150901305:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2990 on theBenchmark for (2990ds/495Mi)
% 7.71/2.19 % (2940618)Instruction limit reached!
% 7.71/2.19 % (2940618)------------------------------
% 7.71/2.19 % (2940618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.71/2.19 % (2940618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.71/2.19 % (2940618)CaDiCaL version: 2.1.3
% 7.71/2.19 % (2940618)Termination reason: Instruction limit
% 7.71/2.19 % (2940618)Termination phase: shuffling
% 7.71/2.19 % (2940618)Time elapsed: 0.211 s
% 7.71/2.19 % (2940618)Peak memory usage: 22 MB
% 7.71/2.19 % (2940618)Instructions burned: 523 (million)
% 7.71/2.19 % (2940640)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=2668360808:cond=on:i=34:hud=10:nm=10:rtra=on_2989 on theBenchmark for (2989ds/34Mi)
% 7.71/2.19 % (2940630)Instruction limit reached!
% 7.71/2.19 % (2940630)------------------------------
% 7.71/2.19 % (2940630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.71/2.19 % (2940630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.40/2.37 % (2940630)CaDiCaL version: 2.1.3
% 8.40/2.37 % (2940630)Termination reason: Instruction limit
% 8.40/2.37 % (2940630)Termination phase: shuffling
% 8.40/2.37 % (2940630)Time elapsed: 0.092 s
% 8.40/2.37 % (2940630)Peak memory usage: 18 MB
% 8.40/2.37 % (2940630)Instructions burned: 105 (million)
% 8.40/2.37 % (2940640)Instruction limit reached!
% 8.40/2.37 % (2940640)------------------------------
% 8.40/2.37 % (2940640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.40/2.37 % (2940640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.40/2.37 % (2940640)CaDiCaL version: 2.1.3
% 8.40/2.37 % (2940640)Termination reason: Instruction limit
% 8.40/2.37 % (2940640)Termination phase: shuffling
% 8.40/2.37 % (2940640)Time elapsed: 0.020 s
% 8.40/2.37 % (2940640)Peak memory usage: 17 MB
% 8.40/2.37 % (2940640)Instructions burned: 36 (million)
% 8.40/2.37 % (2940626)Instruction limit reached!
% 8.40/2.37 % (2940626)------------------------------
% 8.40/2.37 % (2940626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.40/2.37 % (2940626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.40/2.37 % (2940626)CaDiCaL version: 2.1.3
% 8.40/2.37 % (2940626)Termination reason: Instruction limit
% 8.40/2.37 % (2940626)Termination phase: shuffling
% 8.40/2.37 % (2940626)Time elapsed: 0.181 s
% 8.40/2.37 % (2940626)Peak memory usage: 20 MB
% 8.40/2.37 % (2940626)Instructions burned: 451 (million)
% 8.40/2.37 % (2940643)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=3930501599:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2989 on theBenchmark for (2989ds/66Mi)
% 8.40/2.37 % (2940642)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=460813099:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2989 on theBenchmark for (2989ds/91Mi)
% 8.40/2.37 % (2940636)Instruction limit reached!
% 8.40/2.37 % (2940636)------------------------------
% 8.40/2.37 % (2940636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.40/2.37 % (2940636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.40/2.37 % (2940636)CaDiCaL version: 2.1.3
% 8.40/2.37 % (2940636)Termination reason: Instruction limit
% 8.40/2.37 % (2940636)Termination phase: shuffling
% 8.40/2.37 % (2940636)Time elapsed: 0.107 s
% 8.40/2.37 % (2940636)Peak memory usage: 21 MB
% 8.40/2.37 % (2940636)Instructions burned: 498 (million)
% 8.40/2.37 % (2940645)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3745384897:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2988 on theBenchmark for (2988ds/22Mi)
% 8.40/2.37 % (2940647)lrs+21_16_anc=none:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:sas=cadical:si=on:plsqr=32,1:uwa=interpreted_only:foolp=on:nwc=3:random_seed=1149113387:i=338:bd=all:ins=4:rtra=on_2988 on theBenchmark for (2988ds/338Mi)
% 8.40/2.37 % (2940643)Instruction limit reached!
% 8.40/2.37 % (2940643)------------------------------
% 8.40/2.37 % (2940643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.40/2.37 % (2940643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.40/2.37 % (2940643)CaDiCaL version: 2.1.3
% 8.40/2.37 % (2940643)Termination reason: Instruction limit
% 8.40/2.37 % (2940643)Termination phase: shuffling
% 8.40/2.37 % (2940643)Time elapsed: 0.032 s
% 8.40/2.37 % (2940643)Peak memory usage: 17 MB
% 8.40/2.37 % (2940643)Instructions burned: 67 (million)
% 8.40/2.37 % (2940645)Instruction limit reached!
% 8.40/2.37 % (2940645)------------------------------
% 8.40/2.37 % (2940645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.40/2.37 % (2940645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.40/2.37 % (2940645)CaDiCaL version: 2.1.3
% 8.40/2.37 % (2940645)Termination reason: Instruction limit
% 8.40/2.37 % (2940645)Termination phase: shuffling
% 8.40/2.37 % (2940645)Time elapsed: 0.014 s
% 8.40/2.37 % (2940645)Peak memory usage: 16 MB
% 8.40/2.37 % (2940645)Instructions burned: 23 (million)
% 8.40/2.37 % (2940642)Instruction limit reached!
% 8.40/2.37 % (2940642)------------------------------
% 8.40/2.37 % (2940642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.40/2.37 % (2940642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.40/2.37 % (2940642)CaDiCaL version: 2.1.3
% 8.40/2.37 % (2940642)Termination reason: Instruction limit
% 8.40/2.37 % (2940642)Termination phase: shuffling
% 9.27/2.55 % (2940642)Time elapsed: 0.042 s
% 9.27/2.55 % (2940642)Peak memory usage: 17 MB
% 9.27/2.55 % (2940642)Instructions burned: 93 (million)
% 9.27/2.55 % (2940616)Instruction limit reached!
% 9.27/2.55 % (2940616)------------------------------
% 9.27/2.55 % (2940616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.27/2.55 % (2940616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.27/2.55 % (2940616)CaDiCaL version: 2.1.3
% 9.27/2.55 % (2940616)Termination reason: Instruction limit
% 9.27/2.55 % (2940616)Termination phase: Property scanning
% 9.27/2.55 % (2940616)Time elapsed: 0.356 s
% 9.27/2.55 % (2940616)Peak memory usage: 23 MB
% 9.27/2.55 % (2940616)Instructions burned: 875 (million)
% 9.27/2.55 % (2940651)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 9.27/2.55 % (2940650)lrs+10_1_sil=128000:si=on:urr=on:random_seed=1620812684:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2988 on theBenchmark for (2988ds/28Mi)
% 9.27/2.55 % (2940651)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=2192706885:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2988 on theBenchmark for (2988ds/137Mi)
% 9.27/2.55 % (2940652)dis+10_32_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=32,1:uwa=one_side_interpreted:nwc=1:random_seed=3733999699:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2988 on theBenchmark for (2988ds/340Mi)
% 9.27/2.55 % (2940653)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=2366644168:i=227:sd=1:bd=all:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/227Mi)
% 9.27/2.55 % (2940650)Instruction limit reached!
% 9.27/2.55 % (2940650)------------------------------
% 9.27/2.55 % (2940650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.27/2.55 % (2940650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.27/2.55 % (2940650)CaDiCaL version: 2.1.3
% 9.27/2.55 % (2940650)Termination reason: Instruction limit
% 9.27/2.55 % (2940650)Termination phase: shuffling
% 9.27/2.55 % (2940650)Time elapsed: 0.017 s
% 9.27/2.55 % (2940650)Peak memory usage: 16 MB
% 9.27/2.55 % (2940650)Instructions burned: 30 (million)
% 9.27/2.55 % (2940658)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 9.27/2.55 % (2940658)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=2663415550:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/373Mi)
% 9.27/2.55 % (2940647)Instruction limit reached!
% 9.27/2.55 % (2940647)------------------------------
% 9.27/2.55 % (2940647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.27/2.55 % (2940647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.27/2.55 % (2940647)CaDiCaL version: 2.1.3
% 9.27/2.55 % (2940647)Termination reason: Instruction limit
% 9.27/2.55 % (2940647)Termination phase: shuffling
% 9.27/2.55 % (2940647)Time elapsed: 0.080 s
% 9.27/2.55 % (2940647)Peak memory usage: 21 MB
% 9.27/2.55 % (2940647)Instructions burned: 340 (million)
% 9.27/2.55 % (2940660)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=3620841971:i=116:ep=RSTC:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/116Mi)
% 9.27/2.55 % (2940651)Instruction limit reached!
% 9.27/2.55 % (2940651)------------------------------
% 9.27/2.55 % (2940651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.27/2.55 % (2940651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.27/2.55 % (2940651)CaDiCaL version: 2.1.3
% 9.27/2.55 % (2940651)Termination reason: Instruction limit
% 9.27/2.55 % (2940651)Termination phase: shuffling
% 9.27/2.55 % (2940651)Time elapsed: 0.063 s
% 9.27/2.55 % (2940651)Peak memory usage: 18 MB
% 9.27/2.55 % (2940651)Instructions burned: 137 (million)
% 9.27/2.55 % (2940635)Instruction limit reached!
% 9.27/2.55 % (2940635)------------------------------
% 9.27/2.55 % (2940635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.27/2.55 % (2940635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.27/2.55 % (2940635)CaDiCaL version: 2.1.3
% 9.27/2.55 % (2940635)Termination reason: Instruction limit
% 9.27/2.55 % (2940635)Termination phase: shuffling
% 9.27/2.55 % (2940635)Time elapsed: 0.230 s
% 9.27/2.55 % (2940635)Peak memory usage: 20 MB
% 10.85/2.85 % (2940635)Instructions burned: 376 (million)
% 10.85/2.85 % (2940660)Instruction limit reached!
% 10.85/2.85 % (2940660)------------------------------
% 10.85/2.85 % (2940660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.85/2.85 % (2940660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.85 % (2940660)CaDiCaL version: 2.1.3
% 10.85/2.85 % (2940660)Termination reason: Instruction limit
% 10.85/2.85 % (2940660)Termination phase: shuffling
% 10.85/2.85 % (2940660)Time elapsed: 0.027 s
% 10.85/2.85 % (2940660)Peak memory usage: 17 MB
% 10.85/2.85 % (2940660)Instructions burned: 118 (million)
% 10.85/2.85 % (2940662)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=4102786390:i=575:rtra=on_2987 on theBenchmark for (2987ds/575Mi)
% 10.85/2.85 % (2940664)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=579207012:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2987 on theBenchmark for (2987ds/9840Mi)
% 10.85/2.85 % (2940663)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=4128569333:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2987 on theBenchmark for (2987ds/270Mi)
% 10.85/2.85 % (2940653)Instruction limit reached!
% 10.85/2.85 % (2940653)------------------------------
% 10.85/2.85 % (2940653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.85/2.85 % (2940653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.85 % (2940653)CaDiCaL version: 2.1.3
% 10.85/2.85 % (2940653)Termination reason: Instruction limit
% 10.85/2.85 % (2940653)Termination phase: shuffling
% 10.85/2.85 % (2940653)Time elapsed: 0.095 s
% 10.85/2.85 % (2940653)Peak memory usage: 18 MB
% 10.85/2.85 % (2940653)Instructions burned: 228 (million)
% 10.85/2.85 % (2940668)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=3463105127:i=421:rtra=on:ss=axioms_2987 on theBenchmark for (2987ds/421Mi)
% 10.85/2.85 % (2940652)Instruction limit reached!
% 10.85/2.85 % (2940652)------------------------------
% 10.85/2.85 % (2940652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.85/2.85 % (2940652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.85 % (2940652)CaDiCaL version: 2.1.3
% 10.85/2.85 % (2940652)Termination reason: Instruction limit
% 10.85/2.85 % (2940652)Termination phase: shuffling
% 10.85/2.85 % (2940652)Time elapsed: 0.149 s
% 10.85/2.85 % (2940652)Peak memory usage: 21 MB
% 10.85/2.85 % (2940652)Instructions burned: 341 (million)
% 10.85/2.85 % (2940670)WARNING Broken Constraint: if sine_to_age_tolerance(3) 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
% 10.85/2.85 % (2940670)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=2071401443:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2986 on theBenchmark for (2986ds/270Mi)
% 10.85/2.85 % (2940658)Instruction limit reached!
% 10.85/2.85 % (2940658)------------------------------
% 10.85/2.85 % (2940658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.85/2.85 % (2940658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.85 % (2940658)CaDiCaL version: 2.1.3
% 10.85/2.85 % (2940658)Termination reason: Instruction limit
% 10.85/2.85 % (2940658)Termination phase: shuffling
% 10.85/2.85 % (2940658)Time elapsed: 0.165 s
% 10.85/2.85 % (2940658)Peak memory usage: 24 MB
% 10.85/2.85 % (2940658)Instructions burned: 373 (million)
% 10.85/2.85 % (2940672)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=995799721:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2986 on theBenchmark for (2986ds/31Mi)
% 10.85/2.85 % (2940672)Instruction limit reached!
% 10.85/2.85 % (2940672)------------------------------
% 10.85/2.85 % (2940672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.85/2.85 % (2940672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.85/2.85 % (2940672)CaDiCaL version: 2.1.3
% 10.85/2.85 % (2940672)Termination reason: Instruction limit
% 10.85/2.85 % (2940672)Termination phase: shuffling
% 10.85/2.85 % (2940672)Time elapsed: 0.018 s
% 10.85/2.85 % (2940672)Peak memory usage: 17 MB
% 13.96/3.10 % (2940672)Instructions burned: 32 (million)
% 13.96/3.10 % (2940674)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 13.96/3.10 % (2940674)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
% 13.96/3.10 % (2940674)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=1551261986:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2985 on theBenchmark for (2985ds/1440Mi)
% 13.96/3.10 % (2940663)Instruction limit reached!
% 13.96/3.10 % (2940663)------------------------------
% 13.96/3.10 % (2940663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/3.10 % (2940663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/3.10 % (2940663)CaDiCaL version: 2.1.3
% 13.96/3.10 % (2940663)Termination reason: Instruction limit
% 13.96/3.10 % (2940663)Termination phase: shuffling
% 13.96/3.11 % (2940663)Time elapsed: 0.190 s
% 13.96/3.11 % (2940663)Peak memory usage: 20 MB
% 13.96/3.11 % (2940663)Instructions burned: 271 (million)
% 13.96/3.11 % (2940676)dis+10_2_sil=128000:si=on:random_seed=3867407489:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2985 on theBenchmark for (2985ds/339Mi)
% 13.96/3.11 % (2940668)Instruction limit reached!
% 13.96/3.11 % (2940668)------------------------------
% 13.96/3.11 % (2940668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/3.11 % (2940668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/3.11 % (2940668)CaDiCaL version: 2.1.3
% 13.96/3.11 % (2940668)Termination reason: Instruction limit
% 13.96/3.11 % (2940668)Termination phase: shuffling
% 13.96/3.11 % (2940668)Time elapsed: 0.199 s
% 13.96/3.11 % (2940668)Peak memory usage: 20 MB
% 13.96/3.11 % (2940668)Instructions burned: 422 (million)
% 13.96/3.11 % (2940678)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=2214530112:i=111:add=on:fgj=on:rtra=on:fdi=1024_2985 on theBenchmark for (2985ds/111Mi)
% 13.96/3.11 % (2940670)Instruction limit reached!
% 13.96/3.11 % (2940670)------------------------------
% 13.96/3.11 % (2940670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/3.11 % (2940670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/3.11 % (2940670)CaDiCaL version: 2.1.3
% 13.96/3.11 % (2940670)Termination reason: Instruction limit
% 13.96/3.11 % (2940670)Termination phase: shuffling
% 13.96/3.11 % (2940670)Time elapsed: 0.200 s
% 13.96/3.11 % (2940670)Peak memory usage: 19 MB
% 13.96/3.11 % (2940670)Instructions burned: 271 (million)
% 13.96/3.11 % (2940662)Instruction limit reached!
% 13.96/3.11 % (2940662)------------------------------
% 13.96/3.11 % (2940662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/3.11 % (2940662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/3.11 % (2940662)CaDiCaL version: 2.1.3
% 13.96/3.11 % (2940662)Termination reason: Instruction limit
% 13.96/3.11 % (2940662)Termination phase: shuffling
% 13.96/3.11 % (2940662)Time elapsed: 0.287 s
% 13.96/3.11 % (2940662)Peak memory usage: 22 MB
% 13.96/3.11 % (2940662)Instructions burned: 576 (million)
% 13.96/3.11 % (2940678)Instruction limit reached!
% 13.96/3.11 % (2940678)------------------------------
% 13.96/3.11 % (2940678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/3.11 % (2940678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/3.11 % (2940678)CaDiCaL version: 2.1.3
% 13.96/3.11 % (2940678)Termination reason: Instruction limit
% 13.96/3.11 % (2940678)Termination phase: shuffling
% 13.96/3.11 % (2940678)Time elapsed: 0.048 s
% 13.96/3.11 % (2940678)Peak memory usage: 17 MB
% 13.96/3.11 % (2940678)Instructions burned: 111 (million)
% 13.96/3.11 % (2940681)dis+1010_3:2_anc=all_dependent:sil=128000:si=on:sos=on:lma=off:spb=goal_then_units:bce=on:fd=off:random_seed=1687719762:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2984 on theBenchmark for (2984ds/136Mi)
% 13.96/3.11 % (2940680)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=257358656:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2984 on theBenchmark for (2984ds/122Mi)
% 13.96/3.11 % (2940682)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1586773345:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2984 on theBenchmark for (2984ds/232Mi)
% 14.96/3.25 % (2940676)Instruction limit reached!
% 14.96/3.25 % (2940676)------------------------------
% 14.96/3.25 % (2940676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.25 % (2940676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.25 % (2940676)CaDiCaL version: 2.1.3
% 14.96/3.25 % (2940676)Termination reason: Instruction limit
% 14.96/3.25 % (2940676)Termination phase: shuffling
% 14.96/3.25 % (2940676)Time elapsed: 0.139 s
% 14.96/3.25 % (2940676)Peak memory usage: 20 MB
% 14.96/3.25 % (2940676)Instructions burned: 341 (million)
% 14.96/3.25 % (2940681)Instruction limit reached!
% 14.96/3.25 % (2940681)------------------------------
% 14.96/3.25 % (2940681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.25 % (2940681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.25 % (2940681)CaDiCaL version: 2.1.3
% 14.96/3.25 % (2940681)Termination reason: Instruction limit
% 14.96/3.25 % (2940681)Termination phase: shuffling
% 14.96/3.25 % (2940681)Time elapsed: 0.059 s
% 14.96/3.25 % (2940681)Peak memory usage: 17 MB
% 14.96/3.25 % (2940681)Instructions burned: 137 (million)
% 14.96/3.25 % (2940686)lrs+1010_8:1_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sos=on:plsqr=256,1:uwa=off:random_seed=1251672196:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2983 on theBenchmark for (2983ds/1254Mi)
% 14.96/3.25 % (2940687)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 14.96/3.25 % (2940687)dis+1002_5:4_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_simp:si=on:plsqr=878,253:plsql=on:uwa=interpreted_only:lwlo=on:random_seed=1263466713:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2983 on theBenchmark for (2983ds/281Mi)
% 14.96/3.25 % (2940682)Instruction limit reached!
% 14.96/3.25 % (2940682)------------------------------
% 14.96/3.25 % (2940682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.25 % (2940682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.25 % (2940682)CaDiCaL version: 2.1.3
% 14.96/3.25 % (2940682)Termination reason: Instruction limit
% 14.96/3.25 % (2940682)Termination phase: shuffling
% 14.96/3.25 % (2940682)Time elapsed: 0.095 s
% 14.96/3.25 % (2940682)Peak memory usage: 19 MB
% 14.96/3.25 % (2940682)Instructions burned: 232 (million)
% 14.96/3.25 % (2940680)Instruction limit reached!
% 14.96/3.25 % (2940680)------------------------------
% 14.96/3.25 % (2940680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.25 % (2940680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.25 % (2940680)CaDiCaL version: 2.1.3
% 14.96/3.25 % (2940680)Termination reason: Instruction limit
% 14.96/3.25 % (2940680)Termination phase: shuffling
% 14.96/3.25 % (2940680)Time elapsed: 0.100 s
% 14.96/3.25 % (2940680)Peak memory usage: 18 MB
% 14.96/3.25 % (2940680)Instructions burned: 123 (million)
% 14.96/3.25 % (2940690)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3524449993:i=619:add=on:rtra=on_2983 on theBenchmark for (2983ds/619Mi)
% 14.96/3.25 % (2940691)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=3562495615:i=865:bs=unit_only:ins=25:rtra=on:ntd=on_2983 on theBenchmark for (2983ds/865Mi)
% 14.96/3.25 % (2940687)Instruction limit reached!
% 14.96/3.25 % (2940687)------------------------------
% 14.96/3.25 % (2940687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.25 % (2940687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.25 % (2940687)CaDiCaL version: 2.1.3
% 14.96/3.25 % (2940687)Termination reason: Instruction limit
% 14.96/3.25 % (2940687)Termination phase: shuffling
% 14.96/3.25 % (2940687)Time elapsed: 0.127 s
% 14.96/3.25 % (2940687)Peak memory usage: 21 MB
% 14.96/3.25 % (2940687)Instructions burned: 283 (million)
% 14.96/3.25 % (2940694)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3794471716:i=212:sd=1:rtra=on:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/212Mi)
% 14.96/3.25 % (2940694)Instruction limit reached!
% 14.96/3.25 % (2940694)------------------------------
% 14.96/3.25 % (2940694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.25 % (2940694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.28 % (2940694)CaDiCaL version: 2.1.3
% 14.96/3.28 % (2940694)Termination reason: Instruction limit
% 14.96/3.28 % (2940694)Termination phase: shuffling
% 14.96/3.28 % (2940694)Time elapsed: 0.088 s
% 14.96/3.28 % (2940694)Peak memory usage: 18 MB
% 14.96/3.28 % (2940694)Instructions burned: 212 (million)
% 14.96/3.28 % (2940696)lrs+1010_64_sil=128000:si=on:avsql=on:uwa=off:random_seed=1928360717:hsq=on:st=3:avsq=on:i=130:avsqr=1,16:sd=1:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/130Mi)
% 14.96/3.28 % (2940696)Instruction limit reached!
% 14.96/3.28 % (2940696)------------------------------
% 14.96/3.28 % (2940696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.28 % (2940696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.28 % (2940696)CaDiCaL version: 2.1.3
% 14.96/3.28 % (2940696)Termination reason: Instruction limit
% 14.96/3.28 % (2940696)Termination phase: shuffling
% 14.96/3.28 % (2940696)Time elapsed: 0.056 s
% 14.96/3.28 % (2940696)Peak memory usage: 17 MB
% 14.96/3.28 % (2940696)Instructions burned: 130 (million)
% 14.96/3.28 % (2940698)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2014998934:st=1.5:i=346:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/346Mi)
% 14.96/3.28 % (2940674)Instruction limit reached!
% 14.96/3.28 % (2940674)------------------------------
% 14.96/3.28 % (2940674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.28 % (2940674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.28 % (2940674)CaDiCaL version: 2.1.3
% 14.96/3.28 % (2940674)Termination reason: Instruction limit
% 14.96/3.28 % (2940674)Termination phase: Preprocessing 3
% 14.96/3.28 % (2940674)Time elapsed: 0.603 s
% 14.96/3.28 % (2940674)Peak memory usage: 32 MB
% 14.96/3.28 % (2940674)Instructions burned: 1442 (million)
% 14.96/3.28 % (2940690)Instruction limit reached!
% 14.96/3.28 % (2940690)------------------------------
% 14.96/3.28 % (2940690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.28 % (2940690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.28 % (2940690)CaDiCaL version: 2.1.3
% 14.96/3.28 % (2940690)Termination reason: Instruction limit
% 14.96/3.28 % (2940690)Termination phase: shuffling
% 14.96/3.28 % (2940690)Time elapsed: 0.333 s
% 14.96/3.28 % (2940690)Peak memory usage: 26 MB
% 14.96/3.28 % (2940690)Instructions burned: 619 (million)
% 14.96/3.28 % (2940700)lrs+1010_3_sil=128000:si=on:slsq=on:random_seed=932346594:avsq=on:i=152:avsqr=8,1:hud=5:ins=1:fsr=off:rtra=on_2979 on theBenchmark for (2979ds/152Mi)
% 14.96/3.28 % (2940701)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2733783319:i=75:ep=R:rtra=on:ntd=on_2979 on theBenchmark for (2979ds/75Mi)
% 14.96/3.28 % (2940691)Instruction limit reached!
% 14.96/3.28 % (2940691)------------------------------
% 14.96/3.28 % (2940691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.28 % (2940691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.28 % (2940691)CaDiCaL version: 2.1.3
% 14.96/3.28 % (2940691)Termination reason: Instruction limit
% 14.96/3.28 % (2940691)Termination phase: Property scanning
% 14.96/3.28 % (2940691)Time elapsed: 0.369 s
% 14.96/3.28 % (2940691)Peak memory usage: 28 MB
% 14.96/3.28 % (2940691)Instructions burned: 865 (million)
% 14.96/3.28 % (2940704)dis+10_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:nwc=5:random_seed=2150294425:st=2.5:i=387:sd=2:rtra=on:ss=axioms_2979 on theBenchmark for (2979ds/387Mi)
% 14.96/3.28 % (2940700)Instruction limit reached!
% 14.96/3.28 % (2940700)------------------------------
% 14.96/3.28 % (2940700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.28 % (2940700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.28 % (2940700)CaDiCaL version: 2.1.3
% 14.96/3.28 % (2940700)Termination reason: Instruction limit
% 14.96/3.28 % (2940700)Termination phase: shuffling
% 14.96/3.28 % (2940700)Time elapsed: 0.067 s
% 14.96/3.28 % (2940700)Peak memory usage: 18 MB
% 14.96/3.28 % (2940700)Instructions burned: 154 (million)
% 14.96/3.28 % (2940698)Instruction limit reached!
% 14.96/3.28 % (2940698)------------------------------
% 14.96/3.28 % (2940698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.28 % (2940698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.28 % (2940698)CaDiCaL version: 2.1.3
% 14.96/3.28 % (2940698)Termination reason: Instruction limit
% 14.96/3.28 % (2940698)Termination phase: shuffling
% 14.96/3.28 % (2940698)Time elapsed: 0.152 s
% 14.96/3.28 % (2940698)Peak memory usage: 22 MB
% 14.96/3.28 % (2940698)Instructions burned: 347 (million)
% 14.96/3.28 % (2940701)Instruction limit reached!
% 14.96/3.28 % (2940701)------------------------------
% 14.96/3.28 % (2940701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.28 % (2940701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.28 % (2940701)CaDiCaL version: 2.1.3
% 14.96/3.28 % (2940701)Termination reason: Instruction limit
% 14.96/3.28 % (2940701)Termination phase: shuffling
% 14.96/3.28 % (2940701)Time elapsed: 0.061 s
% 14.96/3.28 % (2940701)Peak memory usage: 17 MB
% 14.96/3.28 % (2940701)Instructions burned: 76 (million)
% 14.96/3.28 % (2940706)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=655692780:uwa_fpi=on:i=148:doe=on:bd=preordered:rtra=on:fsd=on_2978 on theBenchmark for (2978ds/148Mi)
% 14.96/3.28 % (2940707)dis+1010_3_si=on:uwa=one_side_interpreted:random_seed=1350913252:i=161:piset=and:rtra=on:ntd=on_2978 on theBenchmark for (2978ds/161Mi)
% 14.96/3.28 % (2940708)lrs+10_1_sil=128000:si=on:random_seed=4261634394:st=5:i=888:sd=3:bd=preordered:rtra=on:ss=axioms_2978 on theBenchmark for (2978ds/888Mi)
% 14.96/3.28 % (2940686)Instruction limit reached!
% 14.96/3.28 % (2940686)------------------------------
% 14.96/3.28 % (2940686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.28 % (2940686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.28 % (2940686)CaDiCaL version: 2.1.3
% 14.96/3.28 % (2940686)Termination reason: Instruction limit
% 14.96/3.28 % (2940686)Termination phase: Property scanning
% 14.96/3.28 % (2940686)Time elapsed: 0.557 s
% 14.96/3.28 % (2940686)Peak memory usage: 28 MB
% 14.96/3.28 % (2940686)Instructions burned: 1255 (million)
% 14.96/3.28 % (2940706)Instruction limit reached!
% 14.96/3.28 % (2940706)------------------------------
% 14.96/3.28 % (2940706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.28 % (2940706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.28 % (2940706)CaDiCaL version: 2.1.3
% 14.96/3.28 % (2940706)Termination reason: Instruction limit
% 14.96/3.28 % (2940706)Termination phase: shuffling
% 14.96/3.28 % (2940706)Time elapsed: 0.069 s
% 14.96/3.28 % (2940706)Peak memory usage: 19 MB
% 14.96/3.28 % (2940706)Instructions burned: 150 (million)
% 14.96/3.28 % (2940712)ott-1003_1_sil=128000:plsq=on:plsqc=1:si=on:sp=weighted_frequency:lma=off:plsqr=1,32:urr=on:cbe=off:random_seed=3130897847:i=136:add=on:ins=4:rtra=on:sup=off_2977 on theBenchmark for (2977ds/136Mi)
% 14.96/3.28 % (2940707)Instruction limit reached!
% 14.96/3.28 % (2940707)------------------------------
% 14.96/3.28 % (2940707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.28 % (2940707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.28 % (2940707)CaDiCaL version: 2.1.3
% 14.96/3.28 % (2940707)Termination reason: Instruction limit
% 14.96/3.28 % (2940707)Termination phase: shuffling
% 14.96/3.28 % (2940707)Time elapsed: 0.068 s
% 14.96/3.28 % (2940707)Peak memory usage: 18 MB
% 14.96/3.28 % (2940707)Instructions burned: 161 (million)
% 14.96/3.28 % (2940714)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=3151469177:i=88:s2at=3:nm=2:rtra=on:rawr=on_2977 on theBenchmark for (2977ds/88Mi)
% 14.96/3.28 % (2940715)dis+1002_5:4_to=kbo:sil=128000:cnfonf=conj_eager:si=on:sp=reverse_arity:lma=off:hi=on:nwc=20:random_seed=3332656143:s2a=on:cond=on:i=93:add=on:bd=preordered:rtra=on:er=filter_2977 on theBenchmark for (2977ds/93Mi)
% 14.96/3.28 % (2940712)Instruction limit reached!
% 14.96/3.28 % (2940712)------------------------------
% 14.96/3.28 % (2940712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.28 % (2940712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.28 % (2940712)CaDiCaL version: 2.1.3
% 14.96/3.28 % (2940712)Termination reason: Instruction limit
% 14.96/3.28 % (2940712)Termination phase: shuffling
% 14.96/3.28 % (2940712)Time elapsed: 0.059 s
% 14.96/3.28 % (2940712)Peak memory usage: 17 MB
% 14.96/3.28 % (2940712)Instructions burned: 137 (million)
% 14.96/3.28 % (2940714)Instruction limit reached!
% 14.96/3.28 % (2940714)------------------------------
% 14.96/3.28 % (2940714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.28 % (2940714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.28 % (2940714)CaDiCaL version: 2.1.3
% 14.96/3.28 % (2940714)Termination reason: Instruction limit
% 14.96/3.28 % (2940714)Termination phase: shuffling
% 14.96/3.28 % (2940714)Time elapsed: 0.043 s
% 14.96/3.28 % (2940714)Peak memory usage: 18 MB
% 14.96/3.28 % (2940714)Instructions burned: 88 (million)
% 14.96/3.28 % (2940704)Instruction limit reached!
% 14.96/3.28 % (2940704)------------------------------
% 14.96/3.28 % (2940704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.28 % (2940704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.28 % (2940704)CaDiCaL version: 2.1.3
% 14.96/3.28 % (2940704)Termination reason: Instruction limit
% 14.96/3.28 % (2940704)Termination phase: shuffling
% 14.96/3.28 % (2940704)Time elapsed: 0.175 s
% 14.96/3.28 % (2940704)Peak memory usage: 24 MB
% 14.96/3.28 % (2940704)Instructions burned: 388 (million)
% 14.96/3.28 % (2940634) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2940494-2940634"...
% 14.96/3.28 % (2940715)Instruction limit reached!
% 14.96/3.28 % (2940715)------------------------------
% 14.96/3.28 % (2940715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.28 % (2940715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.28 % (2940715)CaDiCaL version: 2.1.3
% 14.96/3.28 % (2940715)Termination reason: Instruction limit
% 14.96/3.28 % (2940715)Termination phase: shuffling
% 14.96/3.28 % (2940715)Time elapsed: 0.046 s
% 14.96/3.28 % (2940715)Peak memory usage: 18 MB
% 14.96/3.28 % (2940715)Instructions burned: 94 (million)
% 14.96/3.28 % (2940718)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2631238328:i=2186:rtra=on:ixr=off_2977 on theBenchmark for (2977ds/2186Mi)
% 14.96/3.28 % (2940634)...printing done.
% 14.96/3.28 % (2940634)Refutation found. Thanks to Tanya!
% 14.96/3.28 % SZS status Theorem for theBenchmark
% 14.96/3.28 % SZS output start Proof for theBenchmark
% See solution above
% 14.96/3.29 % (2940634)------------------------------
% 14.96/3.29 % (2940634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.96/3.29 % (2940634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.96/3.29 % (2940634)CaDiCaL version: 2.1.3
% 14.96/3.29 % (2940634)Termination reason: Refutation
% 14.96/3.29 % (2940634)Time elapsed: 1.304 s
% 14.96/3.29 % (2940634)Peak memory usage: 34 MB
% 14.96/3.29 % (2940634)Instructions burned: 2893 (million)
% 14.96/3.29 % (2940494)Success in time 2.314 s
% 14.96/3.29 % Vampire exiting
%------------------------------------------------------------------------------