%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG253^2 : TPTP v9.3.1. Bugfixed v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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 07:45:12 AM UTC 2026
% Result : Theorem 6.23s 1.22s
% Output : Refutation 6.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 45
% Syntax : Number of formulae : 396 ( 57 unt; 0 typ; 40 def)
% Number of atoms : 3019 ( 766 equ; 0 cnn)
% Maximal formula atoms : 9 ( 7 avg)
% Number of connectives : 4463 ( 371 ~; 961 |; 0 &;2685 @)
% ( 40 <=>; 261 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 97 ( 97 >; 0 *; 0 +; 0 <<)
% Number of symbols : 349 ( 345 usr; 217 con; 0-4 aty)
% ( 145 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 576 ( 0 sgn 403 !; 0 ?; 576 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
term: $tType ).
thf(type_def_6,type,
subst: $tType ).
thf(type_def_7,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
one: term ).
thf(func_def_1,type,
ap: term > term > term ).
thf(func_def_2,type,
lam: term > term ).
thf(func_def_3,type,
sub: term > subst > term ).
thf(func_def_4,type,
id: subst ).
thf(func_def_5,type,
sh: subst ).
thf(func_def_6,type,
push: term > subst > subst ).
thf(func_def_7,type,
comp: subst > subst > subst ).
thf(func_def_8,type,
var: term > $o ).
thf(func_def_9,type,
pushprop_lem1v2: $o ).
thf(func_def_10,type,
pushprop_lem1_gthm: $o ).
thf(func_def_11,type,
axmap: $o ).
thf(func_def_12,type,
pushprop_lem0_gthm: $o ).
thf(func_def_13,type,
shinj: $o ).
thf(func_def_14,type,
hoasinduction_lem1v2: $o ).
thf(func_def_15,type,
hoasinduction_lem1v2_gthm: $o ).
thf(func_def_16,type,
hoasap: subst > term > subst > term > term ).
thf(func_def_17,type,
induction2lem: $o ).
thf(func_def_18,type,
hoasinduction_lem3v2_f: $o ).
thf(func_def_19,type,
axvarshift: $o ).
thf(func_def_20,type,
hoasapinj2: $o ).
thf(func_def_21,type,
hoasapnotvar_gthm: $o ).
thf(func_def_22,type,
hoasapinj1: $o ).
thf(func_def_23,type,
ulamvar1: $o ).
thf(func_def_24,type,
induction2lem_lthm: $o ).
thf(func_def_25,type,
hoasinduction_lem3v2_gthm: $o ).
thf(func_def_26,type,
apnotvar: $o ).
thf(func_def_27,type,
pushprop_lthm_orig: $o ).
thf(func_def_28,type,
hoasinduction_lem3v2_f_lthm: $o ).
thf(func_def_29,type,
hoasinduction_lthm: $o ).
thf(func_def_30,type,
hoasinduction_no_psi_cond_lthm: $o ).
thf(func_def_31,type,
hoaslaminj: $o ).
thf(func_def_32,type,
hoasinduction_lem3aaa: $o ).
thf(func_def_33,type,
induction2lem_gthm: $o ).
thf(func_def_34,type,
hoasinduction_lem3aa_lthm: $o ).
thf(func_def_35,type,
hoasinduction_lem3: $o ).
thf(func_def_36,type,
hoasinduction_lem2: $o ).
thf(func_def_37,type,
termmset_lthm: $o ).
thf(func_def_38,type,
hoasinduction_lem1: $o ).
thf(func_def_39,type,
hoaslamnotap_lthm: $o ).
thf(func_def_40,type,
pushprop_lem1v2_lthm: $o ).
thf(func_def_41,type,
hoasapnotvar: $o ).
thf(func_def_42,type,
hoasinduction_lem0: $o ).
thf(func_def_43,type,
hoasinduction: $o ).
thf(func_def_44,type,
hoasinduction_gthm: $o ).
thf(func_def_45,type,
axapp: $o ).
thf(func_def_46,type,
hoaslamnotvar_lthm: $o ).
thf(func_def_47,type,
pushprop_lem3v2_lthm: $o ).
thf(func_def_48,type,
hoasinduction_lem3b_lthm: $o ).
thf(func_def_49,type,
ulamvarind: $o ).
thf(func_def_50,type,
induction: $o ).
thf(func_def_51,type,
hoasinduction_lem3a_lthm: $o ).
thf(func_def_52,type,
termmset_gthm: $o ).
thf(func_def_53,type,
hoasinduction_lem3aa: $o ).
thf(func_def_54,type,
pushprop_lem1v2_gthm: $o ).
thf(func_def_55,type,
hoaslamnotap_gthm: $o ).
thf(func_def_56,type,
hoaslamnotvar_gthm: $o ).
thf(func_def_57,type,
hoasinduction_lem3b_gthm: $o ).
thf(func_def_58,type,
pushprop_lem2v2: $o ).
thf(func_def_59,type,
hoasinduction_lem3a_gthm: $o ).
thf(func_def_60,type,
axclos: $o ).
thf(func_def_61,type,
axassoc: $o ).
thf(func_def_62,type,
hoasinduction_lem2v2: $o ).
thf(func_def_63,type,
pushprop_lthm: $o ).
thf(func_def_64,type,
apinj2: $o ).
thf(func_def_65,type,
apinj1: $o ).
thf(func_def_66,type,
hoasapinj2_lthm: $o ).
thf(func_def_67,type,
hoasinduction_lem3v2a: $o ).
thf(func_def_68,type,
hoasapinj1_lthm: $o ).
thf(func_def_69,type,
hoaslaminj_lthm: $o ).
thf(func_def_70,type,
axvarcons: $o ).
thf(func_def_71,type,
hoaslam: subst > ( subst > term > term ) > term ).
thf(func_def_72,type,
axscons: $o ).
thf(func_def_73,type,
hoasinduction_lem2v2_gthm: $o ).
thf(func_def_74,type,
axidr: $o ).
thf(func_def_75,type,
pushprop_lem1: $o ).
thf(func_def_76,type,
laminj: $o ).
thf(func_def_77,type,
hoasinduction_lem3_lthm: $o ).
thf(func_def_78,type,
pushprop_lem0: $o ).
thf(func_def_79,type,
pushprop_gthm: $o ).
thf(func_def_80,type,
axabs: $o ).
thf(func_def_81,type,
hoasinduction_lem3v2a_lthm: $o ).
thf(func_def_82,type,
hoasinduction_lem2_lthm: $o ).
thf(func_def_83,type,
hoasapinj2_gthm: $o ).
thf(func_def_84,type,
hoasinduction_p_and_p_prime: ( subst > term > subst > $o ) > ( term > $o ) > $o ).
thf(func_def_85,type,
hoasinduction_lem1_lthm: $o ).
thf(func_def_86,type,
lamnotap: $o ).
thf(func_def_87,type,
hoasapinj1_gthm: $o ).
thf(func_def_88,type,
hoaslamnotvar: $o ).
thf(func_def_89,type,
axidl: $o ).
thf(func_def_90,type,
hoaslaminj_gthm: $o ).
thf(func_def_91,type,
induction2_lthm: $o ).
thf(func_def_92,type,
hoasinduction_lem0_lthm: $o ).
thf(func_def_93,type,
substmonoid_lthm: $o ).
thf(func_def_94,type,
pushprop: $o ).
thf(func_def_95,type,
hoasinduction_lem3_gthm: $o ).
thf(func_def_96,type,
hoasinduction_lem2_gthm: $o ).
thf(func_def_97,type,
hoasinduction_lem3b: $o ).
thf(func_def_98,type,
substmonoid: $o ).
thf(func_def_99,type,
lamnotvar: $o ).
thf(func_def_100,type,
hoasinduction_lem3a: $o ).
thf(func_def_101,type,
hoasinduction_lem1_gthm: $o ).
thf(func_def_102,type,
hoasinduction_no_psi_cond: $o ).
thf(func_def_103,type,
induction2_gthm: $o ).
thf(func_def_104,type,
pushprop_lem2v2_lthm: $o ).
thf(func_def_105,type,
hoasvar: subst > term > subst > $o ).
thf(func_def_106,type,
hoaslamnotap: $o ).
thf(func_def_107,type,
substmonoid_gthm: $o ).
thf(func_def_108,type,
ulamvarsh: $o ).
thf(func_def_109,type,
induction2: $o ).
thf(func_def_110,type,
pushprop_lem3v2: $o ).
thf(func_def_111,type,
pushprop_lem2v2_gthm: $o ).
thf(func_def_112,type,
pushprop_lem1_lthm: $o ).
thf(func_def_113,type,
hoasinduction_lem3v2: $o ).
thf(func_def_114,type,
axshiftcons: $o ).
thf(func_def_115,type,
termmset: $o ).
thf(func_def_116,type,
pushprop_lem0_lthm: $o ).
thf(func_def_117,type,
hoasapnotvar_lthm: $o ).
thf(func_def_118,type,
hoasinduction_lem3v2_lthm: $o ).
thf(func_def_119,type,
pushprop_p_and_p_prime: term > subst > ( term > $o ) > ( term > $o ) > $o ).
thf(func_def_120,type,
axvarid: $o ).
thf(func_def_121,type,
hoasinduction_lthm_3: $o ).
thf(func_def_123,type,
vAND: $o > $o > $o ).
thf(func_def_124,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_125,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_126,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_127,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_128,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_129,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_130,type,
vIMP: $o > $o > $o ).
thf(func_def_131,type,
db3:
!>[X0: $tType] : X0 ).
thf(func_def_132,type,
vNOT: $o > $o ).
thf(func_def_133,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_134,type,
db4:
!>[X0: $tType] : X0 ).
thf(func_def_135,type,
vIFF: $o > $o > $o ).
thf(func_def_138,type,
sK0: subst > ( term > $o ) > term ).
thf(func_def_139,type,
sK1: term > $o ).
thf(func_def_140,type,
sK2: term ).
thf(func_def_141,type,
sK3: subst ).
thf(func_def_142,type,
sK4: term ).
thf(func_def_143,type,
sK5: term ).
thf(func_def_144,type,
sK6: term ).
thf(func_def_145,type,
sK7: term ).
thf(func_def_146,type,
sK8: term ).
thf(func_def_147,type,
sK9: term ).
thf(func_def_148,type,
sK10: term ).
thf(func_def_149,type,
sK11: term ).
thf(func_def_150,type,
sK12: ( term > $o ) > term ).
thf(func_def_151,type,
sK13: term > $o ).
thf(func_def_152,type,
sK14: term ).
thf(func_def_153,type,
sK15: subst ).
thf(func_def_154,type,
sK16: subst ).
thf(func_def_155,type,
sK17: term ).
thf(func_def_156,type,
sK18: term ).
thf(func_def_157,type,
sK19: term ).
thf(func_def_158,type,
sK20: term ).
thf(func_def_159,type,
sK21: term ).
thf(func_def_160,type,
sK22: term ).
thf(func_def_161,type,
sK23: ( subst > term > subst > $o ) > term ).
thf(func_def_162,type,
sK24: ( subst > term > subst > $o ) > term ).
thf(func_def_163,type,
sK25: ( subst > term > subst > $o ) > subst > term > term ).
thf(func_def_164,type,
sK26: ( subst > term > subst > $o ) > term > term ).
thf(func_def_165,type,
sK27: ( subst > term > subst > $o ) > subst ).
thf(func_def_166,type,
sK28: ( subst > term > subst > $o ) > subst ).
thf(func_def_167,type,
sK29: ( subst > term > subst > $o ) > subst ).
thf(func_def_168,type,
sK30: ( subst > term > subst > $o ) > subst ).
thf(func_def_169,type,
sK31: ( subst > term > subst > $o ) > subst ).
thf(func_def_170,type,
sK32: ( subst > term > subst > $o ) > subst ).
thf(func_def_171,type,
sK33: ( subst > term > subst > $o ) > subst ).
thf(func_def_172,type,
sK34: ( subst > term > subst > $o ) > subst ).
thf(func_def_173,type,
sK35: ( subst > term > subst > $o ) > subst ).
thf(func_def_174,type,
sK36: ( subst > term > subst > $o ) > subst ).
thf(func_def_175,type,
sK37: ( subst > term > subst > $o ) > subst ).
thf(func_def_176,type,
sK38: ( subst > term > subst > $o ) > subst ).
thf(func_def_177,type,
sK39: ( subst > term > subst > $o ) > term > term ).
thf(func_def_178,type,
sK40: ( subst > term > subst > $o ) > subst ).
thf(func_def_179,type,
sK41: ( subst > term > subst > $o ) > subst ).
thf(func_def_180,type,
sK42: ( subst > term > subst > $o ) > subst ).
thf(func_def_181,type,
sK43: ( subst > term > subst > $o ) > subst ).
thf(func_def_182,type,
sK44: ( subst > term > subst > $o ) > subst ).
thf(func_def_183,type,
sK45: ( subst > term > subst > $o ) > subst ).
thf(func_def_184,type,
sK46: ( subst > term > subst > $o ) > subst ).
thf(func_def_185,type,
sK47: ( subst > term > subst > $o ) > subst ).
thf(func_def_186,type,
sK48: ( subst > term > subst > $o ) > subst ).
thf(func_def_187,type,
sK49: ( subst > term > subst > $o ) > subst ).
thf(func_def_188,type,
sK50: ( subst > term > subst > $o ) > subst ).
thf(func_def_189,type,
sK51: ( subst > term > subst > $o ) > subst ).
thf(func_def_190,type,
sK52: ( subst > term > subst > $o ) > subst ).
thf(func_def_191,type,
sK53: ( subst > term > subst > $o ) > subst ).
thf(func_def_192,type,
sK54: ( subst > term > subst > $o ) > subst ).
thf(func_def_193,type,
sK55: ( subst > term > subst > $o ) > subst ).
thf(func_def_194,type,
sK56: subst > term > subst > $o ).
thf(func_def_195,type,
sK57: ( subst > term > term ) > subst ).
thf(func_def_196,type,
sK58: ( subst > term > term ) > term ).
thf(func_def_197,type,
sK59: ( subst > term > term ) > subst ).
thf(func_def_198,type,
sK60: ( subst > term > term ) > term ).
thf(func_def_199,type,
sK61: ( subst > term > term ) > term ).
thf(func_def_200,type,
sK62: term ).
thf(func_def_201,type,
sK63: subst ).
thf(func_def_202,type,
sK64: subst ).
thf(func_def_203,type,
sK65: term ).
thf(func_def_204,type,
sK66: term ).
thf(func_def_205,type,
sK67: term ).
thf(func_def_206,type,
sK68: term ).
thf(func_def_207,type,
sK69: term ).
thf(func_def_208,type,
sK70: term ).
thf(func_def_209,type,
sK71: term ).
thf(func_def_210,type,
sK72: term ).
thf(func_def_211,type,
sK73: term ).
thf(func_def_212,type,
sK74: term ).
thf(func_def_213,type,
sK75: term ).
thf(func_def_214,type,
sK76: term ).
thf(func_def_215,type,
sK77: subst ).
thf(func_def_216,type,
sK78: term ).
thf(func_def_217,type,
sK79: term ).
thf(func_def_218,type,
sK80: term ).
thf(func_def_219,type,
sK81: subst ).
thf(func_def_220,type,
sK82: ( subst > term > subst > $o ) > subst ).
thf(func_def_221,type,
sK83: ( subst > term > subst > $o ) > term ).
thf(func_def_222,type,
sK84: ( subst > term > subst > $o ) > term ).
thf(func_def_223,type,
sK85: ( subst > term > subst > $o ) > subst ).
thf(func_def_224,type,
sK86: ( subst > term > subst > $o ) > subst ).
thf(func_def_225,type,
sK87: ( subst > term > subst > $o ) > term ).
thf(func_def_226,type,
sK88: ( subst > term > subst > $o ) > term ).
thf(func_def_227,type,
sK89: ( subst > term > subst > $o ) > subst ).
thf(func_def_228,type,
sK90: ( subst > term > subst > $o ) > subst ).
thf(func_def_229,type,
sK91: ( subst > term > subst > $o ) > subst ).
thf(func_def_230,type,
sK92: ( subst > term > subst > $o ) > subst ).
thf(func_def_231,type,
sK93: ( subst > term > subst > $o ) > subst ).
thf(func_def_232,type,
sK94: ( subst > term > subst > $o ) > subst ).
thf(func_def_233,type,
sK95: ( subst > term > subst > $o ) > subst ).
thf(func_def_234,type,
sK96: ( subst > term > subst > $o ) > subst ).
thf(func_def_235,type,
sK97: ( subst > term > subst > $o ) > subst ).
thf(func_def_236,type,
sK98: subst > term > subst > $o ).
thf(func_def_237,type,
sK99: term ).
thf(func_def_238,type,
sK100: term ).
thf(func_def_239,type,
sK101: ( term > $o ) > term ).
thf(func_def_240,type,
sK102: ( term > $o ) > term ).
thf(func_def_241,type,
sK103: ( term > $o ) > term ).
thf(func_def_242,type,
sK104: ( term > $o ) > term ).
thf(func_def_243,type,
sK105: ( term > $o ) > term ).
thf(func_def_244,type,
sK106: ( term > $o ) > term ).
thf(func_def_245,type,
sK107: term > $o ).
thf(func_def_246,type,
sK108: term > term ).
thf(func_def_247,type,
sK109: term ).
thf(func_def_248,type,
sK110: term ).
thf(func_def_249,type,
sK111: subst ).
thf(func_def_250,type,
sK112: subst ).
thf(func_def_251,type,
sK113: subst ).
thf(func_def_252,type,
sK114: subst ).
thf(func_def_253,type,
sK115: ( term > $o ) > term ).
thf(func_def_254,type,
sK116: ( term > $o ) > term ).
thf(func_def_255,type,
sK117: ( term > $o ) > term ).
thf(func_def_256,type,
sK118: ( term > $o ) > term ).
thf(func_def_257,type,
sK119: ( term > $o ) > term ).
thf(func_def_258,type,
sK120: term > $o ).
thf(func_def_259,type,
sK121: term ).
thf(func_def_260,type,
sK122: term ).
thf(func_def_261,type,
sK123: subst ).
thf(func_def_262,type,
sK124: subst ).
thf(func_def_263,type,
sK125: ( term > $o ) > term ).
thf(func_def_264,type,
sK126: ( term > $o ) > term ).
thf(func_def_265,type,
sK127: ( term > $o ) > term ).
thf(func_def_266,type,
sK128: ( term > $o ) > subst > term ).
thf(func_def_267,type,
sK129: ( term > $o ) > subst > term ).
thf(func_def_268,type,
sK130: ( term > $o ) > subst > term ).
thf(func_def_269,type,
sK131: ( term > $o ) > subst > term ).
thf(func_def_270,type,
sK132: term > $o ).
thf(func_def_271,type,
sK133: term > term ).
thf(func_def_272,type,
sK134: subst ).
thf(func_def_273,type,
sK135: term ).
thf(func_def_274,type,
sK136: term ).
thf(func_def_275,type,
sK137: term ).
thf(func_def_276,type,
sK138: term ).
thf(func_def_277,type,
sK139: ( subst > term > term ) > subst ).
thf(func_def_278,type,
sK140: ( subst > term > term ) > subst ).
thf(func_def_279,type,
sK141: ( subst > term > term ) > subst ).
thf(func_def_280,type,
sK142: ( subst > term > term ) > term ).
thf(func_def_281,type,
sK143: ( subst > term > term ) > term ).
thf(func_def_282,type,
sK144: ( subst > term > term ) > subst ).
thf(func_def_283,type,
sK145: subst > term > term ).
thf(func_def_284,type,
sK146: subst > term > term ).
thf(func_def_285,type,
sK147: term ).
thf(func_def_286,type,
sK148: subst ).
thf(func_def_287,type,
sK149: term ).
thf(func_def_288,type,
sK150: subst ).
thf(func_def_289,type,
sK151: ( subst > term > subst > $o ) > term ).
thf(func_def_290,type,
sK152: ( subst > term > subst > $o ) > term ).
thf(func_def_291,type,
sK153: ( subst > term > subst > $o ) > term ).
thf(func_def_292,type,
sK154: ( subst > term > subst > $o ) > subst ).
thf(func_def_293,type,
sK155: ( subst > term > subst > $o ) > subst ).
thf(func_def_294,type,
sK156: ( subst > term > subst > $o ) > subst ).
thf(func_def_295,type,
sK157: ( subst > term > subst > $o ) > subst ).
thf(func_def_296,type,
sK158: ( subst > term > subst > $o ) > subst ).
thf(func_def_297,type,
sK159: ( subst > term > subst > $o ) > subst ).
thf(func_def_298,type,
sK160: ( subst > term > subst > $o ) > subst ).
thf(func_def_299,type,
sK161: ( subst > term > subst > $o ) > subst ).
thf(func_def_300,type,
sK162: ( subst > term > subst > $o ) > subst ).
thf(func_def_301,type,
sK163: ( subst > term > subst > $o ) > subst ).
thf(func_def_302,type,
sK164: ( subst > term > subst > $o ) > subst ).
thf(func_def_303,type,
sK165: subst > term > subst > $o ).
thf(func_def_304,type,
sK166: term ).
thf(func_def_305,type,
sK167: subst ).
thf(func_def_306,type,
sK168: term ).
thf(f3,axiom,
! [X0: term] :
( ( ( sub @ X0 @ id )
= X0 )
= axvarid ),
file('/export/starexec/sandbox2/benchmark/Axioms/ALG003^0.ax',axvarid) ).
thf(f43,axiom,
! [X0: term > $o] :
( ( ! [X2: term,X1: term] :
( ( X0 @ X1 )
=> ( ( X0 @ X2 )
=> ( X0 @ ( ap @ X1 @ X2 ) ) ) )
=> ( ! [X1: term] :
( ! [X2: term] :
( ( X0 @ X2 )
=> ( X0 @ ( sub @ X1 @ ( push @ X2 @ id ) ) ) )
=> ( X0 @ ( lam @ X1 ) ) )
=> ! [X1: term,X3: subst] :
( ! [X2: term] :
( ( var @ X2 )
=> ( X0 @ ( sub @ X2 @ X3 ) ) )
=> ( X0 @ ( sub @ X1 @ X3 ) ) ) ) )
= induction2lem ),
file('/export/starexec/sandbox2/benchmark/Axioms/ALG003^0.ax',induction2lem) ).
thf(f46,axiom,
( induction2
= ( ! [X0: term > $o] :
( ! [X1: term] :
( ( var @ X1 )
=> ( X0 @ X1 ) )
=> ( ! [X2: term,X1: term] :
( ( X0 @ X1 )
=> ( ( X0 @ X2 )
=> ( X0 @ ( ap @ X1 @ X2 ) ) ) )
=> ( ! [X1: term] :
( ! [X2: term] :
( ( X0 @ X2 )
=> ( X0 @ ( sub @ X1 @ ( push @ X2 @ id ) ) ) )
=> ( X0 @ ( lam @ X1 ) ) )
=> ! [X1: term] : ( X0 @ X1 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ALG003^0.ax',induction2) ).
thf(f48,axiom,
( axvarid
=> ( ( induction2lem
=> induction2 )
= induction2_lthm ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ALG003^0.ax',induction2_lthm) ).
thf(f114,conjecture,
induction2_lthm,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm) ).
thf(f115,negated_conjecture,
~ induction2_lthm,
inference(negated_conjecture,[status(cth)],[f114]) ).
thf(f159,plain,
( induction2
= ( ! [X0: term > $o] :
( ! [X1: term] :
( ( var @ X1 )
=> ( X0 @ X1 ) )
=> ( ! [X2: term,X3: term] :
( ( X0 @ X3 )
=> ( ( X0 @ X2 )
=> ( X0 @ ( ap @ X3 @ X2 ) ) ) )
=> ( ! [X4: term] :
( ! [X5: term] :
( ( X0 @ X5 )
=> ( X0 @ ( sub @ X4 @ ( push @ X5 @ id ) ) ) )
=> ( X0 @ ( lam @ X4 ) ) )
=> ! [X6: term] : ( X0 @ X6 ) ) ) ) ) ),
inference(rectify,[],[f46]) ).
thf(f160,plain,
( induction2
= ( !! @ ( term > $o )
@ ^ [Y0: term > $o] :
( ( !! @ term
@ ^ [Y1: term] :
( ( var @ Y1 )
=> ( Y0 @ Y1 ) ) )
=> ( ( !! @ term
@ ^ [Y1: term] :
( !! @ term
@ ^ [Y2: term] :
( ( Y0 @ Y1 )
=> ( ( Y0 @ Y2 )
=> ( Y0 @ ( ap @ Y1 @ Y2 ) ) ) ) ) )
=> ( ( !! @ term
@ ^ [Y1: term] :
( ( !! @ term
@ ^ [Y2: term] :
( ( Y0 @ Y2 )
=> ( Y0 @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) ) ) )
=> ( Y0 @ ( lam @ Y1 ) ) ) )
=> ( !! @ term
@ ^ [Y1: term] : ( Y0 @ Y1 ) ) ) ) ) ) ),
inference(fool_elimination,[],[f159]) ).
thf(f208,plain,
( axvarid
=> ( ( induction2lem
=> induction2 )
= induction2_lthm ) ),
inference(rectify,[],[f48]) ).
thf(f209,plain,
( induction2_lthm
= ( axvarid
=> ( induction2lem
=> induction2 ) ) ),
inference(fool_elimination,[],[f208]) ).
thf(f216,plain,
~ induction2_lthm,
inference(rectify,[],[f115]) ).
thf(f217,plain,
induction2_lthm != $true,
inference(fool_elimination,[],[f216]) ).
thf(f249,plain,
( axvarid
= ( !! @ term
@ ^ [Y0: term] :
( ( sub @ Y0 @ id )
= Y0 ) ) ),
inference(fool_elimination,[],[f3]) ).
thf(f284,plain,
! [X0: term > $o] :
( ( ! [X1: term,X2: term] :
( ( X0 @ X2 )
=> ( ( X0 @ X1 )
=> ( X0 @ ( ap @ X2 @ X1 ) ) ) )
=> ( ! [X3: term] :
( ! [X4: term] :
( ( X0 @ X4 )
=> ( X0 @ ( sub @ X3 @ ( push @ X4 @ id ) ) ) )
=> ( X0 @ ( lam @ X3 ) ) )
=> ! [X5: term,X6: subst] :
( ! [X7: term] :
( ( var @ X7 )
=> ( X0 @ ( sub @ X7 @ X6 ) ) )
=> ( X0 @ ( sub @ X5 @ X6 ) ) ) ) )
= induction2lem ),
inference(rectify,[],[f43]) ).
thf(f285,plain,
( induction2lem
= ( !! @ ( term > $o )
@ ^ [Y0: term > $o] :
( ( !! @ term
@ ^ [Y1: term] :
( !! @ term
@ ^ [Y2: term] :
( ( Y0 @ Y1 )
=> ( ( Y0 @ Y2 )
=> ( Y0 @ ( ap @ Y1 @ Y2 ) ) ) ) ) )
=> ( ( !! @ term
@ ^ [Y1: term] :
( ( !! @ term
@ ^ [Y2: term] :
( ( Y0 @ Y2 )
=> ( Y0 @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) ) ) )
=> ( Y0 @ ( lam @ Y1 ) ) ) )
=> ( !! @ subst
@ ^ [Y1: subst] :
( !! @ term
@ ^ [Y2: term] :
( ( !! @ term
@ ^ [Y3: term] :
( ( var @ Y3 )
=> ( Y0 @ ( sub @ Y3 @ Y1 ) ) ) )
=> ( Y0 @ ( sub @ Y2 @ Y1 ) ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f284]) ).
thf(f317,plain,
induction2_lthm != $true,
inference(flattening,[],[f217]) ).
thf(f318,plain,
( induction2_lthm
= ( axvarid
=> ( induction2lem
=> induction2 ) ) ),
inference(cnf_transformation,[],[f209]) ).
thf(f327,plain,
induction2_lthm != $true,
inference(cnf_transformation,[],[f317]) ).
thf(f339,plain,
( induction2lem
= ( !! @ ( term > $o )
@ ^ [Y0: term > $o] :
( ( !! @ term
@ ^ [Y1: term] :
( !! @ term
@ ^ [Y2: term] :
( ( Y0 @ Y1 )
=> ( ( Y0 @ Y2 )
=> ( Y0 @ ( ap @ Y1 @ Y2 ) ) ) ) ) )
=> ( ( !! @ term
@ ^ [Y1: term] :
( ( !! @ term
@ ^ [Y2: term] :
( ( Y0 @ Y2 )
=> ( Y0 @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) ) ) )
=> ( Y0 @ ( lam @ Y1 ) ) ) )
=> ( !! @ subst
@ ^ [Y1: subst] :
( !! @ term
@ ^ [Y2: term] :
( ( !! @ term
@ ^ [Y3: term] :
( ( var @ Y3 )
=> ( Y0 @ ( sub @ Y3 @ Y1 ) ) ) )
=> ( Y0 @ ( sub @ Y2 @ Y1 ) ) ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f285]) ).
thf(f340,plain,
( axvarid
= ( !! @ term
@ ^ [Y0: term] :
( ( sub @ Y0 @ id )
= Y0 ) ) ),
inference(cnf_transformation,[],[f249]) ).
thf(f351,plain,
( induction2
= ( !! @ ( term > $o )
@ ^ [Y0: term > $o] :
( ( !! @ term
@ ^ [Y1: term] :
( ( var @ Y1 )
=> ( Y0 @ Y1 ) ) )
=> ( ( !! @ term
@ ^ [Y1: term] :
( !! @ term
@ ^ [Y2: term] :
( ( Y0 @ Y1 )
=> ( ( Y0 @ Y2 )
=> ( Y0 @ ( ap @ Y1 @ Y2 ) ) ) ) ) )
=> ( ( !! @ term
@ ^ [Y1: term] :
( ( !! @ term
@ ^ [Y2: term] :
( ( Y0 @ Y2 )
=> ( Y0 @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) ) ) )
=> ( Y0 @ ( lam @ Y1 ) ) ) )
=> ( !! @ term
@ ^ [Y1: term] : ( Y0 @ Y1 ) ) ) ) ) ) ),
inference(cnf_transformation,[],[f160]) ).
thf(f481,plain,
( ( induction2_lthm = $true )
| ( ( axvarid
=> ( induction2lem
=> induction2 ) )
= $false ) ),
inference(iff_proxy_clausification,[],[f318]) ).
thf(f485,plain,
( ( induction2_lthm = $true )
| ( ( induction2lem
=> induction2 )
= $false ) ),
inference(imp_proxy_clausification,[],[f481]) ).
thf(f486,plain,
( ( axvarid = $true )
| ( induction2_lthm = $true ) ),
inference(imp_proxy_clausification,[],[f481]) ).
thf(f487,plain,
( ( induction2_lthm = $true )
| ( induction2 = $false ) ),
inference(imp_proxy_clausification,[],[f485]) ).
thf(f488,plain,
( ( induction2lem = $true )
| ( induction2_lthm = $true ) ),
inference(imp_proxy_clausification,[],[f485]) ).
thf(f924,plain,
( ( induction2 = $true )
| ( ( !! @ ( term > $o )
@ ^ [Y0: term > $o] :
( ( !! @ term
@ ^ [Y1: term] :
( ( var @ Y1 )
=> ( Y0 @ Y1 ) ) )
=> ( ( !! @ term
@ ^ [Y1: term] :
( !! @ term
@ ^ [Y2: term] :
( ( Y0 @ Y1 )
=> ( ( Y0 @ Y2 )
=> ( Y0 @ ( ap @ Y1 @ Y2 ) ) ) ) ) )
=> ( ( !! @ term
@ ^ [Y1: term] :
( ( !! @ term
@ ^ [Y2: term] :
( ( Y0 @ Y2 )
=> ( Y0 @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) ) ) )
=> ( Y0 @ ( lam @ Y1 ) ) ) )
=> ( !! @ term
@ ^ [Y1: term] : ( Y0 @ Y1 ) ) ) ) ) )
= $false ) ),
inference(iff_proxy_clausification,[],[f351]) ).
thf(f971,plain,
( ( induction2 = $true )
| ( ( ^ [Y0: term > $o] :
( ( !! @ term
@ ^ [Y1: term] :
( ( var @ Y1 )
=> ( Y0 @ Y1 ) ) )
=> ( ( !! @ term
@ ^ [Y1: term] :
( !! @ term
@ ^ [Y2: term] :
( ( Y0 @ Y1 )
=> ( ( Y0 @ Y2 )
=> ( Y0 @ ( ap @ Y1 @ Y2 ) ) ) ) ) )
=> ( ( !! @ term
@ ^ [Y1: term] :
( ( !! @ term
@ ^ [Y2: term] :
( ( Y0 @ Y2 )
=> ( Y0 @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) ) ) )
=> ( Y0 @ ( lam @ Y1 ) ) ) )
=> ( !! @ term
@ ^ [Y1: term] : ( Y0 @ Y1 ) ) ) ) )
@ sK107 )
= $false ) ),
inference(sigma_proxy_clausification,[],[f924]) ).
thf(f972,plain,
( ( induction2 = $true )
| ( $false
= ( ( !! @ term
@ ^ [Y0: term] :
( ( var @ Y0 )
=> ( sK107 @ Y0 ) ) )
=> ( ( !! @ term
@ ^ [Y0: term] :
( !! @ term
@ ^ [Y1: term] :
( ( sK107 @ Y0 )
=> ( ( sK107 @ Y1 )
=> ( sK107 @ ( ap @ Y0 @ Y1 ) ) ) ) ) )
=> ( ( !! @ term
@ ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( sK107 @ Y1 )
=> ( sK107 @ ( sub @ Y0 @ ( push @ Y1 @ id ) ) ) ) )
=> ( sK107 @ ( lam @ Y0 ) ) ) )
=> ( !! @ term @ sK107 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f971]) ).
thf(f973,plain,
( ( induction2 = $true )
| ( ( ( !! @ term
@ ^ [Y0: term] :
( !! @ term
@ ^ [Y1: term] :
( ( sK107 @ Y0 )
=> ( ( sK107 @ Y1 )
=> ( sK107 @ ( ap @ Y0 @ Y1 ) ) ) ) ) )
=> ( ( !! @ term
@ ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( sK107 @ Y1 )
=> ( sK107 @ ( sub @ Y0 @ ( push @ Y1 @ id ) ) ) ) )
=> ( sK107 @ ( lam @ Y0 ) ) ) )
=> ( !! @ term @ sK107 ) ) )
= $false ) ),
inference(imp_proxy_clausification,[],[f972]) ).
thf(f974,plain,
( ( induction2 = $true )
| ( $true
= ( !! @ term
@ ^ [Y0: term] :
( ( var @ Y0 )
=> ( sK107 @ Y0 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f972]) ).
thf(f975,plain,
! [X1: term] :
( ( induction2 = $true )
| ( ( ^ [Y0: term] :
( ( var @ Y0 )
=> ( sK107 @ Y0 ) )
@ X1 )
= $true ) ),
inference(pi_proxy_clausification,[],[f974]) ).
thf(f976,plain,
! [X1: term] :
( ( induction2 = $true )
| ( $true
= ( ( var @ X1 )
=> ( sK107 @ X1 ) ) ) ),
inference(beta-eta_normalization,[],[f975]) ).
thf(f977,plain,
! [X1: term] :
( ( induction2 = $true )
| ( ( sK107 @ X1 )
= $true )
| ( ( var @ X1 )
= $false ) ),
inference(imp_proxy_clausification,[],[f976]) ).
thf(f978,plain,
( ( ( ( !! @ term
@ ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( sK107 @ Y1 )
=> ( sK107 @ ( sub @ Y0 @ ( push @ Y1 @ id ) ) ) ) )
=> ( sK107 @ ( lam @ Y0 ) ) ) )
=> ( !! @ term @ sK107 ) )
= $false )
| ( induction2 = $true ) ),
inference(imp_proxy_clausification,[],[f973]) ).
thf(f979,plain,
( ( induction2 = $true )
| ( ( !! @ term
@ ^ [Y0: term] :
( !! @ term
@ ^ [Y1: term] :
( ( sK107 @ Y0 )
=> ( ( sK107 @ Y1 )
=> ( sK107 @ ( ap @ Y0 @ Y1 ) ) ) ) ) )
= $true ) ),
inference(imp_proxy_clausification,[],[f973]) ).
thf(f980,plain,
! [X1: term] :
( ( induction2 = $true )
| ( ( ^ [Y0: term] :
( !! @ term
@ ^ [Y1: term] :
( ( sK107 @ Y0 )
=> ( ( sK107 @ Y1 )
=> ( sK107 @ ( ap @ Y0 @ Y1 ) ) ) ) )
@ X1 )
= $true ) ),
inference(pi_proxy_clausification,[],[f979]) ).
thf(f981,plain,
! [X1: term] :
( ( induction2 = $true )
| ( $true
= ( !! @ term
@ ^ [Y0: term] :
( ( sK107 @ X1 )
=> ( ( sK107 @ Y0 )
=> ( sK107 @ ( ap @ X1 @ Y0 ) ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f980]) ).
thf(f982,plain,
! [X2: term,X1: term] :
( ( $true
= ( ^ [Y0: term] :
( ( sK107 @ X1 )
=> ( ( sK107 @ Y0 )
=> ( sK107 @ ( ap @ X1 @ Y0 ) ) ) )
@ X2 ) )
| ( induction2 = $true ) ),
inference(pi_proxy_clausification,[],[f981]) ).
thf(f983,plain,
! [X2: term,X1: term] :
( ( ( ( sK107 @ X1 )
=> ( ( sK107 @ X2 )
=> ( sK107 @ ( ap @ X1 @ X2 ) ) ) )
= $true )
| ( induction2 = $true ) ),
inference(beta-eta_normalization,[],[f982]) ).
thf(f984,plain,
! [X2: term,X1: term] :
( ( ( sK107 @ X1 )
= $false )
| ( induction2 = $true )
| ( $true
= ( ( sK107 @ X2 )
=> ( sK107 @ ( ap @ X1 @ X2 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f983]) ).
thf(f985,plain,
! [X2: term,X1: term] :
( ( ( sK107 @ X1 )
= $false )
| ( induction2 = $true )
| ( ( sK107 @ ( ap @ X1 @ X2 ) )
= $true )
| ( ( sK107 @ X2 )
= $false ) ),
inference(imp_proxy_clausification,[],[f984]) ).
thf(f986,plain,
( ( induction2 = $true )
| ( ( !! @ term @ sK107 )
= $false ) ),
inference(imp_proxy_clausification,[],[f978]) ).
thf(f987,plain,
( ( ( !! @ term
@ ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( sK107 @ Y1 )
=> ( sK107 @ ( sub @ Y0 @ ( push @ Y1 @ id ) ) ) ) )
=> ( sK107 @ ( lam @ Y0 ) ) ) )
= $true )
| ( induction2 = $true ) ),
inference(imp_proxy_clausification,[],[f978]) ).
thf(f988,plain,
! [X1: term] :
( ( induction2 = $true )
| ( $true
= ( ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( sK107 @ Y1 )
=> ( sK107 @ ( sub @ Y0 @ ( push @ Y1 @ id ) ) ) ) )
=> ( sK107 @ ( lam @ Y0 ) ) )
@ X1 ) ) ),
inference(pi_proxy_clausification,[],[f987]) ).
thf(f989,plain,
! [X1: term] :
( ( $true
= ( ( !! @ term
@ ^ [Y0: term] :
( ( sK107 @ Y0 )
=> ( sK107 @ ( sub @ X1 @ ( push @ Y0 @ id ) ) ) ) )
=> ( sK107 @ ( lam @ X1 ) ) ) )
| ( induction2 = $true ) ),
inference(beta-eta_normalization,[],[f988]) ).
thf(f990,plain,
! [X1: term] :
( ( $true
= ( sK107 @ ( lam @ X1 ) ) )
| ( induction2 = $true )
| ( $false
= ( !! @ term
@ ^ [Y0: term] :
( ( sK107 @ Y0 )
=> ( sK107 @ ( sub @ X1 @ ( push @ Y0 @ id ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f989]) ).
thf(f991,plain,
! [X1: term] :
( ( ( ^ [Y0: term] :
( ( sK107 @ Y0 )
=> ( sK107 @ ( sub @ X1 @ ( push @ Y0 @ id ) ) ) )
@ ( sK108 @ X1 ) )
= $false )
| ( induction2 = $true )
| ( $true
= ( sK107 @ ( lam @ X1 ) ) ) ),
inference(sigma_proxy_clausification,[],[f990]) ).
thf(f992,plain,
! [X1: term] :
( ( induction2 = $true )
| ( ( ( sK107 @ ( sK108 @ X1 ) )
=> ( sK107 @ ( sub @ X1 @ ( push @ ( sK108 @ X1 ) @ id ) ) ) )
= $false )
| ( $true
= ( sK107 @ ( lam @ X1 ) ) ) ),
inference(beta-eta_normalization,[],[f991]) ).
thf(f993,plain,
! [X1: term] :
( ( ( sK107 @ ( sub @ X1 @ ( push @ ( sK108 @ X1 ) @ id ) ) )
= $false )
| ( $true
= ( sK107 @ ( lam @ X1 ) ) )
| ( induction2 = $true ) ),
inference(imp_proxy_clausification,[],[f992]) ).
thf(f994,plain,
! [X1: term] :
( ( induction2 = $true )
| ( $true
= ( sK107 @ ( sK108 @ X1 ) ) )
| ( $true
= ( sK107 @ ( lam @ X1 ) ) ) ),
inference(imp_proxy_clausification,[],[f992]) ).
thf(f995,plain,
( ( induction2 = $true )
| ( ( sK107 @ sK109 )
= $false ) ),
inference(sigma_proxy_clausification,[],[f986]) ).
thf(f1107,plain,
( ( $true
= ( !! @ ( term > $o )
@ ^ [Y0: term > $o] :
( ( !! @ term
@ ^ [Y1: term] :
( !! @ term
@ ^ [Y2: term] :
( ( Y0 @ Y1 )
=> ( ( Y0 @ Y2 )
=> ( Y0 @ ( ap @ Y1 @ Y2 ) ) ) ) ) )
=> ( ( !! @ term
@ ^ [Y1: term] :
( ( !! @ term
@ ^ [Y2: term] :
( ( Y0 @ Y2 )
=> ( Y0 @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) ) ) )
=> ( Y0 @ ( lam @ Y1 ) ) ) )
=> ( !! @ subst
@ ^ [Y1: subst] :
( !! @ term
@ ^ [Y2: term] :
( ( !! @ term
@ ^ [Y3: term] :
( ( var @ Y3 )
=> ( Y0 @ ( sub @ Y3 @ Y1 ) ) ) )
=> ( Y0 @ ( sub @ Y2 @ Y1 ) ) ) ) ) ) ) ) )
| ( induction2lem = $false ) ),
inference(iff_proxy_clausification,[],[f339]) ).
thf(f1108,plain,
! [X1: term > $o] :
( ( induction2lem = $false )
| ( ( ^ [Y0: term > $o] :
( ( !! @ term
@ ^ [Y1: term] :
( !! @ term
@ ^ [Y2: term] :
( ( Y0 @ Y1 )
=> ( ( Y0 @ Y2 )
=> ( Y0 @ ( ap @ Y1 @ Y2 ) ) ) ) ) )
=> ( ( !! @ term
@ ^ [Y1: term] :
( ( !! @ term
@ ^ [Y2: term] :
( ( Y0 @ Y2 )
=> ( Y0 @ ( sub @ Y1 @ ( push @ Y2 @ id ) ) ) ) )
=> ( Y0 @ ( lam @ Y1 ) ) ) )
=> ( !! @ subst
@ ^ [Y1: subst] :
( !! @ term
@ ^ [Y2: term] :
( ( !! @ term
@ ^ [Y3: term] :
( ( var @ Y3 )
=> ( Y0 @ ( sub @ Y3 @ Y1 ) ) ) )
=> ( Y0 @ ( sub @ Y2 @ Y1 ) ) ) ) ) ) )
@ X1 )
= $true ) ),
inference(pi_proxy_clausification,[],[f1107]) ).
thf(f1109,plain,
! [X1: term > $o] :
( ( induction2lem = $false )
| ( ( ( !! @ term
@ ^ [Y0: term] :
( !! @ term
@ ^ [Y1: term] :
( ( X1 @ Y0 )
=> ( ( X1 @ Y1 )
=> ( X1 @ ( ap @ Y0 @ Y1 ) ) ) ) ) )
=> ( ( !! @ term
@ ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( X1 @ Y1 )
=> ( X1 @ ( sub @ Y0 @ ( push @ Y1 @ id ) ) ) ) )
=> ( X1 @ ( lam @ Y0 ) ) ) )
=> ( !! @ subst
@ ^ [Y0: subst] :
( !! @ term
@ ^ [Y1: term] :
( ( !! @ term
@ ^ [Y2: term] :
( ( var @ Y2 )
=> ( X1 @ ( sub @ Y2 @ Y0 ) ) ) )
=> ( X1 @ ( sub @ Y1 @ Y0 ) ) ) ) ) ) )
= $true ) ),
inference(beta-eta_normalization,[],[f1108]) ).
thf(f1110,plain,
! [X1: term > $o] :
( ( induction2lem = $false )
| ( ( ( !! @ term
@ ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( X1 @ Y1 )
=> ( X1 @ ( sub @ Y0 @ ( push @ Y1 @ id ) ) ) ) )
=> ( X1 @ ( lam @ Y0 ) ) ) )
=> ( !! @ subst
@ ^ [Y0: subst] :
( !! @ term
@ ^ [Y1: term] :
( ( !! @ term
@ ^ [Y2: term] :
( ( var @ Y2 )
=> ( X1 @ ( sub @ Y2 @ Y0 ) ) ) )
=> ( X1 @ ( sub @ Y1 @ Y0 ) ) ) ) ) )
= $true )
| ( $false
= ( !! @ term
@ ^ [Y0: term] :
( !! @ term
@ ^ [Y1: term] :
( ( X1 @ Y0 )
=> ( ( X1 @ Y1 )
=> ( X1 @ ( ap @ Y0 @ Y1 ) ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f1109]) ).
thf(f1111,plain,
! [X1: term > $o] :
( ( $false
= ( !! @ term
@ ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( X1 @ Y1 )
=> ( X1 @ ( sub @ Y0 @ ( push @ Y1 @ id ) ) ) ) )
=> ( X1 @ ( lam @ Y0 ) ) ) ) )
| ( $false
= ( !! @ term
@ ^ [Y0: term] :
( !! @ term
@ ^ [Y1: term] :
( ( X1 @ Y0 )
=> ( ( X1 @ Y1 )
=> ( X1 @ ( ap @ Y0 @ Y1 ) ) ) ) ) ) )
| ( induction2lem = $false )
| ( ( !! @ subst
@ ^ [Y0: subst] :
( !! @ term
@ ^ [Y1: term] :
( ( !! @ term
@ ^ [Y2: term] :
( ( var @ Y2 )
=> ( X1 @ ( sub @ Y2 @ Y0 ) ) ) )
=> ( X1 @ ( sub @ Y1 @ Y0 ) ) ) ) )
= $true ) ),
inference(imp_proxy_clausification,[],[f1110]) ).
thf(f1112,plain,
! [X1: term > $o] :
( ( induction2lem = $false )
| ( ( ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( X1 @ Y1 )
=> ( X1 @ ( sub @ Y0 @ ( push @ Y1 @ id ) ) ) ) )
=> ( X1 @ ( lam @ Y0 ) ) )
@ ( sK125 @ X1 ) )
= $false )
| ( ( !! @ subst
@ ^ [Y0: subst] :
( !! @ term
@ ^ [Y1: term] :
( ( !! @ term
@ ^ [Y2: term] :
( ( var @ Y2 )
=> ( X1 @ ( sub @ Y2 @ Y0 ) ) ) )
=> ( X1 @ ( sub @ Y1 @ Y0 ) ) ) ) )
= $true )
| ( $false
= ( !! @ term
@ ^ [Y0: term] :
( !! @ term
@ ^ [Y1: term] :
( ( X1 @ Y0 )
=> ( ( X1 @ Y1 )
=> ( X1 @ ( ap @ Y0 @ Y1 ) ) ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f1111]) ).
thf(f1113,plain,
! [X2: subst,X1: term > $o] :
( ( induction2lem = $false )
| ( $false
= ( !! @ term
@ ^ [Y0: term] :
( !! @ term
@ ^ [Y1: term] :
( ( X1 @ Y0 )
=> ( ( X1 @ Y1 )
=> ( X1 @ ( ap @ Y0 @ Y1 ) ) ) ) ) ) )
| ( ( ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( X1 @ Y1 )
=> ( X1 @ ( sub @ Y0 @ ( push @ Y1 @ id ) ) ) ) )
=> ( X1 @ ( lam @ Y0 ) ) )
@ ( sK125 @ X1 ) )
= $false )
| ( ( ^ [Y0: subst] :
( !! @ term
@ ^ [Y1: term] :
( ( !! @ term
@ ^ [Y2: term] :
( ( var @ Y2 )
=> ( X1 @ ( sub @ Y2 @ Y0 ) ) ) )
=> ( X1 @ ( sub @ Y1 @ Y0 ) ) ) )
@ X2 )
= $true ) ),
inference(pi_proxy_clausification,[],[f1112]) ).
thf(f1114,plain,
! [X2: subst,X1: term > $o] :
( ( ( ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( X1 @ Y1 )
=> ( X1 @ ( sub @ Y0 @ ( push @ Y1 @ id ) ) ) ) )
=> ( X1 @ ( lam @ Y0 ) ) )
@ ( sK125 @ X1 ) )
= $false )
| ( ( ^ [Y0: term] :
( !! @ term
@ ^ [Y1: term] :
( ( X1 @ Y0 )
=> ( ( X1 @ Y1 )
=> ( X1 @ ( ap @ Y0 @ Y1 ) ) ) ) )
@ ( sK126 @ X1 ) )
= $false )
| ( induction2lem = $false )
| ( ( ^ [Y0: subst] :
( !! @ term
@ ^ [Y1: term] :
( ( !! @ term
@ ^ [Y2: term] :
( ( var @ Y2 )
=> ( X1 @ ( sub @ Y2 @ Y0 ) ) ) )
=> ( X1 @ ( sub @ Y1 @ Y0 ) ) ) )
@ X2 )
= $true ) ),
inference(sigma_proxy_clausification,[],[f1113]) ).
thf(f1115,plain,
! [X2: subst,X1: term > $o] :
( ( $true
= ( !! @ term
@ ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( var @ Y1 )
=> ( X1 @ ( sub @ Y1 @ X2 ) ) ) )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) ) ) )
| ( induction2lem = $false )
| ( $false
= ( !! @ term
@ ^ [Y0: term] :
( ( X1 @ ( sK126 @ X1 ) )
=> ( ( X1 @ Y0 )
=> ( X1 @ ( ap @ ( sK126 @ X1 ) @ Y0 ) ) ) ) ) )
| ( $false
= ( ( !! @ term
@ ^ [Y0: term] :
( ( X1 @ Y0 )
=> ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ Y0 @ id ) ) ) ) )
=> ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) ) ) ),
inference(beta-eta_normalization,[],[f1114]) ).
thf(f1116,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( $false
= ( !! @ term
@ ^ [Y0: term] :
( ( X1 @ ( sK126 @ X1 ) )
=> ( ( X1 @ Y0 )
=> ( X1 @ ( ap @ ( sK126 @ X1 ) @ Y0 ) ) ) ) ) )
| ( $true
= ( ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( var @ Y1 )
=> ( X1 @ ( sub @ Y1 @ X2 ) ) ) )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) )
@ X3 ) )
| ( induction2lem = $false )
| ( $false
= ( ( !! @ term
@ ^ [Y0: term] :
( ( X1 @ Y0 )
=> ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ Y0 @ id ) ) ) ) )
=> ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) ) ) ),
inference(pi_proxy_clausification,[],[f1115]) ).
thf(f1117,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( $false
= ( ^ [Y0: term] :
( ( X1 @ ( sK126 @ X1 ) )
=> ( ( X1 @ Y0 )
=> ( X1 @ ( ap @ ( sK126 @ X1 ) @ Y0 ) ) ) )
@ ( sK127 @ X1 ) ) )
| ( induction2lem = $false )
| ( $true
= ( ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( var @ Y1 )
=> ( X1 @ ( sub @ Y1 @ X2 ) ) ) )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) )
@ X3 ) )
| ( $false
= ( ( !! @ term
@ ^ [Y0: term] :
( ( X1 @ Y0 )
=> ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ Y0 @ id ) ) ) ) )
=> ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f1116]) ).
thf(f1118,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( induction2lem = $false )
| ( $false
= ( ^ [Y0: term] :
( ( X1 @ ( sK126 @ X1 ) )
=> ( ( X1 @ Y0 )
=> ( X1 @ ( ap @ ( sK126 @ X1 ) @ Y0 ) ) ) )
@ ( sK127 @ X1 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( $true
= ( ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( var @ Y1 )
=> ( X1 @ ( sub @ Y1 @ X2 ) ) ) )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) )
@ X3 ) ) ),
inference(imp_proxy_clausification,[],[f1117]) ).
thf(f1119,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( $false
= ( ^ [Y0: term] :
( ( X1 @ ( sK126 @ X1 ) )
=> ( ( X1 @ Y0 )
=> ( X1 @ ( ap @ ( sK126 @ X1 ) @ Y0 ) ) ) )
@ ( sK127 @ X1 ) ) )
| ( induction2lem = $false )
| ( $true
= ( ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( var @ Y1 )
=> ( X1 @ ( sub @ Y1 @ X2 ) ) ) )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) )
@ X3 ) )
| ( $true
= ( !! @ term
@ ^ [Y0: term] :
( ( X1 @ Y0 )
=> ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ Y0 @ id ) ) ) ) ) ) ),
inference(imp_proxy_clausification,[],[f1117]) ).
thf(f1120,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( $true
= ( ^ [Y0: term] :
( ( X1 @ Y0 )
=> ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ Y0 @ id ) ) ) )
@ X4 ) )
| ( induction2lem = $false )
| ( $false
= ( ^ [Y0: term] :
( ( X1 @ ( sK126 @ X1 ) )
=> ( ( X1 @ Y0 )
=> ( X1 @ ( ap @ ( sK126 @ X1 ) @ Y0 ) ) ) )
@ ( sK127 @ X1 ) ) )
| ( $true
= ( ^ [Y0: term] :
( ( !! @ term
@ ^ [Y1: term] :
( ( var @ Y1 )
=> ( X1 @ ( sub @ Y1 @ X2 ) ) ) )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) )
@ X3 ) ) ),
inference(pi_proxy_clausification,[],[f1119]) ).
thf(f1121,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( $true
= ( ( X1 @ X4 )
=> ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) ) ) )
| ( induction2lem = $false )
| ( ( ( X1 @ ( sK126 @ X1 ) )
=> ( ( X1 @ ( sK127 @ X1 ) )
=> ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) ) ) )
= $false )
| ( $true
= ( ( !! @ term
@ ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) ) )
=> ( X1 @ ( sub @ X3 @ X2 ) ) ) ) ),
inference(beta-eta_normalization,[],[f1120]) ).
thf(f1122,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( $true
= ( ( !! @ term
@ ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) ) )
=> ( X1 @ ( sub @ X3 @ X2 ) ) ) )
| ( induction2lem = $false )
| ( ( ( X1 @ ( sK126 @ X1 ) )
=> ( ( X1 @ ( sK127 @ X1 ) )
=> ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) ) ) )
= $false )
| ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( ( X1 @ X4 )
= $false ) ),
inference(imp_proxy_clausification,[],[f1121]) ).
thf(f1123,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( induction2lem = $false )
| ( $false
= ( !! @ term
@ ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) ) ) )
| ( ( X1 @ X4 )
= $false )
| ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( ( ( X1 @ ( sK126 @ X1 ) )
=> ( ( X1 @ ( sK127 @ X1 ) )
=> ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) ) ) )
= $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) ) ),
inference(imp_proxy_clausification,[],[f1122]) ).
thf(f1124,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( induction2lem = $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( ( X1 @ ( sK126 @ X1 ) )
=> ( ( X1 @ ( sK127 @ X1 ) )
=> ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) ) ) )
= $false )
| ( ( X1 @ X4 )
= $false )
| ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( ( ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) )
@ ( sK128 @ X1 @ X2 ) )
= $false ) ),
inference(sigma_proxy_clausification,[],[f1123]) ).
thf(f1125,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( induction2lem = $false )
| ( ( X1 @ X4 )
= $false )
| ( ( ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) )
@ ( sK128 @ X1 @ X2 ) )
= $false )
| ( ( ( X1 @ ( sK127 @ X1 ) )
=> ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) ) )
= $false ) ),
inference(imp_proxy_clausification,[],[f1124]) ).
thf(f1126,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( ( X1 @ X4 )
= $false )
| ( induction2lem = $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( sK126 @ X1 ) )
= $true )
| ( ( ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) )
@ ( sK128 @ X1 @ X2 ) )
= $false ) ),
inference(imp_proxy_clausification,[],[f1124]) ).
thf(f1127,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( $false
= ( ( var @ ( sK128 @ X1 @ X2 ) )
=> ( X1 @ ( sub @ ( sK128 @ X1 @ X2 ) @ X2 ) ) ) )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( ( X1 @ ( sK126 @ X1 ) )
= $true )
| ( ( X1 @ X4 )
= $false )
| ( induction2lem = $false ) ),
inference(beta-eta_normalization,[],[f1126]) ).
thf(f1128,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $false
= ( X1 @ ( sub @ ( sK128 @ X1 @ X2 ) @ X2 ) ) )
| ( ( X1 @ X4 )
= $false )
| ( induction2lem = $false )
| ( ( X1 @ ( sK126 @ X1 ) )
= $true ) ),
inference(imp_proxy_clausification,[],[f1127]) ).
thf(f1129,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( ( X1 @ X4 )
= $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( induction2lem = $false )
| ( $true
= ( var @ ( sK128 @ X1 @ X2 ) ) )
| ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( ( X1 @ ( sK126 @ X1 ) )
= $true ) ),
inference(imp_proxy_clausification,[],[f1127]) ).
thf(f1130,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( ( ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) )
@ ( sK128 @ X1 @ X2 ) )
= $false )
| ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false )
| ( induction2lem = $false )
| ( ( X1 @ X4 )
= $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) ) ),
inference(imp_proxy_clausification,[],[f1125]) ).
thf(f1131,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( ( ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) )
@ ( sK128 @ X1 @ X2 ) )
= $false )
| ( ( X1 @ ( sK127 @ X1 ) )
= $true )
| ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( ( X1 @ X4 )
= $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( induction2lem = $false ) ),
inference(imp_proxy_clausification,[],[f1125]) ).
thf(f1132,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( ( X1 @ ( sK127 @ X1 ) )
= $true )
| ( $false
= ( ( var @ ( sK128 @ X1 @ X2 ) )
=> ( X1 @ ( sub @ ( sK128 @ X1 @ X2 ) @ X2 ) ) ) )
| ( induction2lem = $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( ( X1 @ X4 )
= $false ) ),
inference(beta-eta_normalization,[],[f1131]) ).
thf(f1133,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( ( X1 @ X4 )
= $false )
| ( induction2lem = $false )
| ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( sK127 @ X1 ) )
= $true )
| ( $false
= ( X1 @ ( sub @ ( sK128 @ X1 @ X2 ) @ X2 ) ) ) ),
inference(imp_proxy_clausification,[],[f1132]) ).
thf(f1134,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( ( X1 @ ( sK127 @ X1 ) )
= $true )
| ( ( X1 @ X4 )
= $false )
| ( $true
= ( var @ ( sK128 @ X1 @ X2 ) ) )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( induction2lem = $false ) ),
inference(imp_proxy_clausification,[],[f1132]) ).
thf(f1135,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( ( X1 @ X4 )
= $false )
| ( $false
= ( ( var @ ( sK128 @ X1 @ X2 ) )
=> ( X1 @ ( sub @ ( sK128 @ X1 @ X2 ) @ X2 ) ) ) )
| ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( induction2lem = $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false ) ),
inference(beta-eta_normalization,[],[f1130]) ).
thf(f1136,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false )
| ( ( X1 @ X4 )
= $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( induction2lem = $false )
| ( $false
= ( X1 @ ( sub @ ( sK128 @ X1 @ X2 ) @ X2 ) ) ) ),
inference(imp_proxy_clausification,[],[f1135]) ).
thf(f1137,plain,
! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( induction2lem = $false )
| ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( $true
= ( var @ ( sK128 @ X1 @ X2 ) ) )
| ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false )
| ( ( X1 @ X4 )
= $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) ) ),
inference(imp_proxy_clausification,[],[f1135]) ).
thf(f1138,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( ( ( X1 @ ( sK126 @ X1 ) )
=> ( ( X1 @ ( sK127 @ X1 ) )
=> ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) ) ) )
= $false )
| ( $true
= ( ( !! @ term
@ ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) ) )
=> ( X1 @ ( sub @ X3 @ X2 ) ) ) )
| ( induction2lem = $false )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) ) ),
inference(beta-eta_normalization,[],[f1118]) ).
thf(f1139,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( induction2lem = $false )
| ( $true
= ( ( !! @ term
@ ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) ) )
=> ( X1 @ ( sub @ X3 @ X2 ) ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( ( ( X1 @ ( sK127 @ X1 ) )
=> ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) ) )
= $false ) ),
inference(imp_proxy_clausification,[],[f1138]) ).
thf(f1140,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( ( X1 @ ( sK126 @ X1 ) )
= $true )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( induction2lem = $false )
| ( $true
= ( ( !! @ term
@ ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) ) )
=> ( X1 @ ( sub @ X3 @ X2 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f1138]) ).
thf(f1141,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( ( X1 @ ( sK126 @ X1 ) )
= $true )
| ( $false
= ( !! @ term
@ ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) ) ) )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( induction2lem = $false ) ),
inference(imp_proxy_clausification,[],[f1140]) ).
thf(f1142,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( $false
= ( ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) )
@ ( sK129 @ X1 @ X2 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( sK126 @ X1 ) )
= $true )
| ( induction2lem = $false ) ),
inference(sigma_proxy_clausification,[],[f1141]) ).
thf(f1143,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( induction2lem = $false )
| ( ( X1 @ ( sK126 @ X1 ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( $false
= ( ( var @ ( sK129 @ X1 @ X2 ) )
=> ( X1 @ ( sub @ ( sK129 @ X1 @ X2 ) @ X2 ) ) ) ) ),
inference(beta-eta_normalization,[],[f1142]) ).
thf(f1144,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( induction2lem = $false )
| ( ( X1 @ ( sK126 @ X1 ) )
= $true )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( sub @ ( sK129 @ X1 @ X2 ) @ X2 ) )
= $false ) ),
inference(imp_proxy_clausification,[],[f1143]) ).
thf(f1145,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( $true
= ( var @ ( sK129 @ X1 @ X2 ) ) )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( induction2lem = $false )
| ( ( X1 @ ( sK126 @ X1 ) )
= $true )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f1143]) ).
thf(f1146,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( ( ( X1 @ ( sK127 @ X1 ) )
=> ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) ) )
= $false )
| ( $false
= ( !! @ term
@ ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( induction2lem = $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) ) ),
inference(imp_proxy_clausification,[],[f1139]) ).
thf(f1147,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false )
| ( $false
= ( !! @ term
@ ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) ) ) )
| ( induction2lem = $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f1146]) ).
thf(f1148,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( $false
= ( !! @ term
@ ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) ) ) )
| ( ( X1 @ ( sK127 @ X1 ) )
= $true )
| ( induction2lem = $false ) ),
inference(imp_proxy_clausification,[],[f1146]) ).
thf(f1149,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( ( ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) )
@ ( sK130 @ X1 @ X2 ) )
= $false )
| ( induction2lem = $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( sK127 @ X1 ) )
= $true )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) ) ),
inference(sigma_proxy_clausification,[],[f1148]) ).
thf(f1150,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( ( X1 @ ( sK127 @ X1 ) )
= $true )
| ( induction2lem = $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( $false
= ( ( var @ ( sK130 @ X1 @ X2 ) )
=> ( X1 @ ( sub @ ( sK130 @ X1 @ X2 ) @ X2 ) ) ) ) ),
inference(beta-eta_normalization,[],[f1149]) ).
thf(f1151,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $false
= ( X1 @ ( sub @ ( sK130 @ X1 @ X2 ) @ X2 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( induction2lem = $false )
| ( ( X1 @ ( sK127 @ X1 ) )
= $true ) ),
inference(imp_proxy_clausification,[],[f1150]) ).
thf(f1152,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( ( var @ ( sK130 @ X1 @ X2 ) )
= $true )
| ( induction2lem = $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( sK127 @ X1 ) )
= $true )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f1150]) ).
thf(f1153,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false )
| ( $false
= ( ^ [Y0: term] :
( ( var @ Y0 )
=> ( X1 @ ( sub @ Y0 @ X2 ) ) )
@ ( sK131 @ X1 @ X2 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( induction2lem = $false ) ),
inference(sigma_proxy_clausification,[],[f1147]) ).
thf(f1154,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( induction2lem = $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $false
= ( ( var @ ( sK131 @ X1 @ X2 ) )
=> ( X1 @ ( sub @ ( sK131 @ X1 @ X2 ) @ X2 ) ) ) ) ),
inference(beta-eta_normalization,[],[f1153]) ).
thf(f1155,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( induction2lem = $false )
| ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false )
| ( ( X1 @ ( sub @ ( sK131 @ X1 @ X2 ) @ X2 ) )
= $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) ) ),
inference(imp_proxy_clausification,[],[f1154]) ).
thf(f1156,plain,
! [X2: subst,X3: term,X1: term > $o] :
( ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( var @ ( sK131 @ X1 @ X2 ) )
= $true )
| ( induction2lem = $false ) ),
inference(imp_proxy_clausification,[],[f1154]) ).
thf(f1203,plain,
( ( axvarid = $false )
| ( ( !! @ term
@ ^ [Y0: term] :
( ( sub @ Y0 @ id )
= Y0 ) )
= $true ) ),
inference(iff_proxy_clausification,[],[f340]) ).
thf(f1204,plain,
! [X1: term] :
( ( $true
= ( ^ [Y0: term] :
( ( sub @ Y0 @ id )
= Y0 )
@ X1 ) )
| ( axvarid = $false ) ),
inference(pi_proxy_clausification,[],[f1203]) ).
thf(f1205,plain,
! [X1: term] :
( ( $true
= ( ( sub @ X1 @ id )
= X1 ) )
| ( axvarid = $false ) ),
inference(beta-eta_normalization,[],[f1204]) ).
thf(f1206,plain,
! [X1: term] :
( ( ( sub @ X1 @ id )
= X1 )
| ( axvarid = $false ) ),
inference(equality_proxy_clausification,[],[f1205]) ).
thf(f1511,definition,
( spl169_34
<=> ( induction2lem = $false ) ),
introduced(definition,[new_symbols(definition,[spl169_34])],[avatar_definition]) ).
thf(f1513,plain,
( ( induction2lem = $false )
| ~ spl169_34 ),
inference(avatar_component_clause,[],[f1511]) ).
thf(f1519,definition,
( spl169_36
<=> ( induction2 = $true ) ),
introduced(definition,[new_symbols(definition,[spl169_36])],[avatar_definition]) ).
thf(f1521,plain,
( ( induction2 = $true )
| ~ spl169_36 ),
inference(avatar_component_clause,[],[f1519]) ).
thf(f1523,definition,
( spl169_37
<=> ( axvarid = $false ) ),
introduced(definition,[new_symbols(definition,[spl169_37])],[avatar_definition]) ).
thf(f1525,plain,
( ( axvarid = $false )
| ~ spl169_37 ),
inference(avatar_component_clause,[],[f1523]) ).
thf(f1528,definition,
( spl169_38
<=> ( axvarid = $true ) ),
introduced(definition,[new_symbols(definition,[spl169_38])],[avatar_definition]) ).
thf(f1530,plain,
( ( axvarid = $true )
| ~ spl169_38 ),
inference(avatar_component_clause,[],[f1528]) ).
thf(f1532,definition,
( spl169_39
<=> ( induction2_lthm = $true ) ),
introduced(definition,[new_symbols(definition,[spl169_39])],[avatar_definition]) ).
thf(f1535,plain,
( spl169_38
| spl169_39 ),
inference(avatar_split_clause,[],[f486,f1532,f1528]) ).
thf(f1537,definition,
( spl169_40
<=> ( induction2lem = $true ) ),
introduced(definition,[new_symbols(definition,[spl169_40])],[avatar_definition]) ).
thf(f1539,plain,
( ( induction2lem = $true )
| ~ spl169_40 ),
inference(avatar_component_clause,[],[f1537]) ).
thf(f1540,plain,
( spl169_40
| spl169_39 ),
inference(avatar_split_clause,[],[f488,f1532,f1537]) ).
thf(f1542,definition,
( spl169_41
<=> ( induction2 = $false ) ),
introduced(definition,[new_symbols(definition,[spl169_41])],[avatar_definition]) ).
thf(f1544,plain,
( ( induction2 = $false )
| ~ spl169_41 ),
inference(avatar_component_clause,[],[f1542]) ).
thf(f1545,plain,
( spl169_39
| spl169_41 ),
inference(avatar_split_clause,[],[f487,f1542,f1532]) ).
thf(f2015,definition,
( spl169_154
<=> ! [X1: term] :
( ( ( sK107 @ X1 )
= $true )
| ( ( var @ X1 )
= $false ) ) ),
introduced(definition,[new_symbols(definition,[spl169_154])],[avatar_definition]) ).
thf(f2016,plain,
( ! [X1: term] :
( ( ( sK107 @ X1 )
= $true )
| ( ( var @ X1 )
= $false ) )
| ~ spl169_154 ),
inference(avatar_component_clause,[],[f2015]) ).
thf(f2017,plain,
( spl169_36
| spl169_154 ),
inference(avatar_split_clause,[],[f977,f2015,f1519]) ).
thf(f2019,definition,
( spl169_155
<=> ! [X2: term,X1: term] :
( ( ( sK107 @ X1 )
= $false )
| ( ( sK107 @ X2 )
= $false )
| ( ( sK107 @ ( ap @ X1 @ X2 ) )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl169_155])],[avatar_definition]) ).
thf(f2020,plain,
( ! [X2: term,X1: term] :
( ( ( sK107 @ ( ap @ X1 @ X2 ) )
= $true )
| ( ( sK107 @ X2 )
= $false )
| ( ( sK107 @ X1 )
= $false ) )
| ~ spl169_155 ),
inference(avatar_component_clause,[],[f2019]) ).
thf(f2021,plain,
( spl169_36
| spl169_155 ),
inference(avatar_split_clause,[],[f985,f2019,f1519]) ).
thf(f2023,definition,
( spl169_156
<=> ! [X1: term] :
( ( $true
= ( sK107 @ ( sK108 @ X1 ) ) )
| ( $true
= ( sK107 @ ( lam @ X1 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl169_156])],[avatar_definition]) ).
thf(f2024,plain,
( ! [X1: term] :
( ( $true
= ( sK107 @ ( sK108 @ X1 ) ) )
| ( $true
= ( sK107 @ ( lam @ X1 ) ) ) )
| ~ spl169_156 ),
inference(avatar_component_clause,[],[f2023]) ).
thf(f2025,plain,
( spl169_156
| spl169_36 ),
inference(avatar_split_clause,[],[f994,f1519,f2023]) ).
thf(f2027,definition,
( spl169_157
<=> ! [X1: term] :
( ( ( sK107 @ ( sub @ X1 @ ( push @ ( sK108 @ X1 ) @ id ) ) )
= $false )
| ( $true
= ( sK107 @ ( lam @ X1 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl169_157])],[avatar_definition]) ).
thf(f2028,plain,
( ! [X1: term] :
( ( ( sK107 @ ( sub @ X1 @ ( push @ ( sK108 @ X1 ) @ id ) ) )
= $false )
| ( $true
= ( sK107 @ ( lam @ X1 ) ) ) )
| ~ spl169_157 ),
inference(avatar_component_clause,[],[f2027]) ).
thf(f2029,plain,
( spl169_36
| spl169_157 ),
inference(avatar_split_clause,[],[f993,f2027,f1519]) ).
thf(f2031,definition,
( spl169_158
<=> ( ( sK107 @ sK109 )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl169_158])],[avatar_definition]) ).
thf(f2033,plain,
( ( ( sK107 @ sK109 )
= $false )
| ~ spl169_158 ),
inference(avatar_component_clause,[],[f2031]) ).
thf(f2034,plain,
( spl169_36
| spl169_158 ),
inference(avatar_split_clause,[],[f995,f2031,f1519]) ).
thf(f2182,definition,
( spl169_194
<=> ! [X2: subst,X4: term,X3: term,X1: term > $o] :
( ( ( X1 @ X4 )
= $false )
| ( ( X1 @ ( sK126 @ X1 ) )
= $true )
| ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( $true
= ( var @ ( sK128 @ X1 @ X2 ) ) )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl169_194])],[avatar_definition]) ).
thf(f2183,plain,
( ! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( sK126 @ X1 ) )
= $true )
| ( $true
= ( var @ ( sK128 @ X1 @ X2 ) ) )
| ( ( X1 @ X4 )
= $false ) )
| ~ spl169_194 ),
inference(avatar_component_clause,[],[f2182]) ).
thf(f2184,plain,
( spl169_194
| spl169_34 ),
inference(avatar_split_clause,[],[f1129,f1511,f2182]) ).
thf(f2186,definition,
( spl169_195
<=> ! [X2: subst,X4: term,X3: term,X1: term > $o] :
( ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( ( X1 @ ( sK126 @ X1 ) )
= $true )
| ( ( X1 @ X4 )
= $false )
| ( $false
= ( X1 @ ( sub @ ( sK128 @ X1 @ X2 ) @ X2 ) ) )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl169_195])],[avatar_definition]) ).
thf(f2187,plain,
( ! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( ( X1 @ ( sK126 @ X1 ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ X4 )
= $false )
| ( $false
= ( X1 @ ( sub @ ( sK128 @ X1 @ X2 ) @ X2 ) ) ) )
| ~ spl169_195 ),
inference(avatar_component_clause,[],[f2186]) ).
thf(f2188,plain,
( spl169_195
| spl169_34 ),
inference(avatar_split_clause,[],[f1128,f1511,f2186]) ).
thf(f2190,definition,
( spl169_196
<=> ! [X2: subst,X4: term,X3: term,X1: term > $o] :
( ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $true
= ( var @ ( sK128 @ X1 @ X2 ) ) )
| ( ( X1 @ X4 )
= $false )
| ( ( X1 @ ( sK127 @ X1 ) )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl169_196])],[avatar_definition]) ).
thf(f2191,plain,
( ! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( ( X1 @ X4 )
= $false )
| ( ( X1 @ ( sK127 @ X1 ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $true
= ( var @ ( sK128 @ X1 @ X2 ) ) ) )
| ~ spl169_196 ),
inference(avatar_component_clause,[],[f2190]) ).
thf(f2192,plain,
( spl169_34
| spl169_196 ),
inference(avatar_split_clause,[],[f1134,f2190,f1511]) ).
thf(f2194,definition,
( spl169_197
<=> ! [X2: subst,X4: term,X3: term,X1: term > $o] :
( ( ( X1 @ X4 )
= $false )
| ( $false
= ( X1 @ ( sub @ ( sK128 @ X1 @ X2 ) @ X2 ) ) )
| ( ( X1 @ ( sK127 @ X1 ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl169_197])],[avatar_definition]) ).
thf(f2195,plain,
( ! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( ( X1 @ ( sK127 @ X1 ) )
= $true )
| ( ( X1 @ X4 )
= $false )
| ( $false
= ( X1 @ ( sub @ ( sK128 @ X1 @ X2 ) @ X2 ) ) )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) ) )
| ~ spl169_197 ),
inference(avatar_component_clause,[],[f2194]) ).
thf(f2196,plain,
( spl169_197
| spl169_34 ),
inference(avatar_split_clause,[],[f1133,f1511,f2194]) ).
thf(f2198,definition,
( spl169_198
<=> ! [X2: subst,X4: term,X3: term,X1: term > $o] :
( ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ X4 )
= $false )
| ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false )
| ( $true
= ( var @ ( sK128 @ X1 @ X2 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl169_198])],[avatar_definition]) ).
thf(f2199,plain,
( ! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false )
| ( ( X1 @ X4 )
= $false )
| ( $true
= ( var @ ( sK128 @ X1 @ X2 ) ) )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) ) )
| ~ spl169_198 ),
inference(avatar_component_clause,[],[f2198]) ).
thf(f2200,plain,
( spl169_34
| spl169_198 ),
inference(avatar_split_clause,[],[f1137,f2198,f1511]) ).
thf(f2202,definition,
( spl169_199
<=> ! [X4: term,X3: term,X2: subst,X1: term > $o] :
( ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false )
| ( $false
= ( X1 @ ( sub @ ( sK128 @ X1 @ X2 ) @ X2 ) ) )
| ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ X4 )
= $false ) ) ),
introduced(definition,[new_symbols(definition,[spl169_199])],[avatar_definition]) ).
thf(f2203,plain,
( ! [X2: subst,X3: term,X1: term > $o,X4: term] :
( ( ( X1 @ ( sub @ ( sK125 @ X1 ) @ ( push @ X4 @ id ) ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false )
| ( ( X1 @ X4 )
= $false )
| ( $false
= ( X1 @ ( sub @ ( sK128 @ X1 @ X2 ) @ X2 ) ) ) )
| ~ spl169_199 ),
inference(avatar_component_clause,[],[f2202]) ).
thf(f2204,plain,
( spl169_199
| spl169_34 ),
inference(avatar_split_clause,[],[f1136,f1511,f2202]) ).
thf(f2206,definition,
( spl169_200
<=> ! [X2: subst,X1: term > $o,X3: term] :
( ( $true
= ( var @ ( sK129 @ X1 @ X2 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( ( X1 @ ( sK126 @ X1 ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl169_200])],[avatar_definition]) ).
thf(f2207,plain,
( ! [X2: subst,X3: term,X1: term > $o] :
( ( $true
= ( var @ ( sK129 @ X1 @ X2 ) ) )
| ( ( X1 @ ( sK126 @ X1 ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) ) )
| ~ spl169_200 ),
inference(avatar_component_clause,[],[f2206]) ).
thf(f2208,plain,
( spl169_200
| spl169_34 ),
inference(avatar_split_clause,[],[f1145,f1511,f2206]) ).
thf(f2210,definition,
( spl169_201
<=> ! [X2: subst,X1: term > $o,X3: term] :
( ( ( X1 @ ( sK126 @ X1 ) )
= $true )
| ( ( X1 @ ( sub @ ( sK129 @ X1 @ X2 ) @ X2 ) )
= $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl169_201])],[avatar_definition]) ).
thf(f2211,plain,
( ! [X2: subst,X3: term,X1: term > $o] :
( ( ( X1 @ ( sub @ ( sK129 @ X1 @ X2 ) @ X2 ) )
= $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( ( X1 @ ( sK126 @ X1 ) )
= $true ) )
| ~ spl169_201 ),
inference(avatar_component_clause,[],[f2210]) ).
thf(f2212,plain,
( spl169_201
| spl169_34 ),
inference(avatar_split_clause,[],[f1144,f1511,f2210]) ).
thf(f2214,definition,
( spl169_202
<=> ! [X2: subst,X1: term > $o,X3: term] :
( ( ( var @ ( sK130 @ X1 @ X2 ) )
= $true )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( ( X1 @ ( sK127 @ X1 ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl169_202])],[avatar_definition]) ).
thf(f2215,plain,
( ! [X2: subst,X3: term,X1: term > $o] :
( ( ( var @ ( sK130 @ X1 @ X2 ) )
= $true )
| ( ( X1 @ ( sK127 @ X1 ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) ) )
| ~ spl169_202 ),
inference(avatar_component_clause,[],[f2214]) ).
thf(f2216,plain,
( spl169_34
| spl169_202 ),
inference(avatar_split_clause,[],[f1152,f2214,f1511]) ).
thf(f2218,definition,
( spl169_203
<=> ! [X2: subst,X1: term > $o,X3: term] :
( ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( sK127 @ X1 ) )
= $true )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( $false
= ( X1 @ ( sub @ ( sK130 @ X1 @ X2 ) @ X2 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl169_203])],[avatar_definition]) ).
thf(f2219,plain,
( ! [X2: subst,X3: term,X1: term > $o] :
( ( $false
= ( X1 @ ( sub @ ( sK130 @ X1 @ X2 ) @ X2 ) ) )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( sK127 @ X1 ) )
= $true )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) ) )
| ~ spl169_203 ),
inference(avatar_component_clause,[],[f2218]) ).
thf(f2220,plain,
( spl169_34
| spl169_203 ),
inference(avatar_split_clause,[],[f1151,f2218,f1511]) ).
thf(f2222,definition,
( spl169_204
<=> ! [X2: subst,X1: term > $o,X3: term] :
( ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( ( var @ ( sK131 @ X1 @ X2 ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false ) ) ),
introduced(definition,[new_symbols(definition,[spl169_204])],[avatar_definition]) ).
thf(f2223,plain,
( ! [X2: subst,X3: term,X1: term > $o] :
( ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false )
| ( ( var @ ( sK131 @ X1 @ X2 ) )
= $true )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) ) )
| ~ spl169_204 ),
inference(avatar_component_clause,[],[f2222]) ).
thf(f2224,plain,
( spl169_34
| spl169_204 ),
inference(avatar_split_clause,[],[f1156,f2222,f1511]) ).
thf(f2226,definition,
( spl169_205
<=> ! [X2: subst,X1: term > $o,X3: term] :
( ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( ( X1 @ ( sub @ ( sK131 @ X1 @ X2 ) @ X2 ) )
= $false ) ) ),
introduced(definition,[new_symbols(definition,[spl169_205])],[avatar_definition]) ).
thf(f2227,plain,
( ! [X2: subst,X3: term,X1: term > $o] :
( ( ( X1 @ ( sub @ ( sK131 @ X1 @ X2 ) @ X2 ) )
= $false )
| ( $true
= ( X1 @ ( sub @ X3 @ X2 ) ) )
| ( $false
= ( X1 @ ( lam @ ( sK125 @ X1 ) ) ) )
| ( ( X1 @ ( ap @ ( sK126 @ X1 ) @ ( sK127 @ X1 ) ) )
= $false ) )
| ~ spl169_205 ),
inference(avatar_component_clause,[],[f2226]) ).
thf(f2228,plain,
( spl169_34
| spl169_205 ),
inference(avatar_split_clause,[],[f1155,f2226,f1511]) ).
thf(f2273,definition,
( spl169_216
<=> ! [X1: term] :
( ( sub @ X1 @ id )
= X1 ) ),
introduced(definition,[new_symbols(definition,[spl169_216])],[avatar_definition]) ).
thf(f2274,plain,
( ! [X1: term] :
( ( sub @ X1 @ id )
= X1 )
| ~ spl169_216 ),
inference(avatar_component_clause,[],[f2273]) ).
thf(f2275,plain,
( spl169_216
| spl169_37 ),
inference(avatar_split_clause,[],[f1206,f1523,f2273]) ).
thf(f2407,plain,
~ spl169_39,
inference(avatar_split_clause,[],[f327,f1532]) ).
thf(f2408,plain,
( ( $false = $true )
| ~ spl169_37
| ~ spl169_38 ),
inference(forward_demodulation,[],[f1530,f1525]) ).
thf(f2409,plain,
( $false
| ~ spl169_37
| ~ spl169_38 ),
inference(trivial_inequality_removal,[],[f2408]) ).
thf(f2410,plain,
( ~ spl169_37
| ~ spl169_38 ),
inference(avatar_contradiction_clause,[],[f2409]) ).
thf(f2412,plain,
( ( $false = $true )
| ~ spl169_34
| ~ spl169_40 ),
inference(forward_demodulation,[],[f1539,f1513]) ).
thf(f2413,plain,
( $false
| ~ spl169_34
| ~ spl169_40 ),
inference(trivial_inequality_removal,[],[f2412]) ).
thf(f2414,plain,
( ~ spl169_34
| ~ spl169_40 ),
inference(avatar_contradiction_clause,[],[f2413]) ).
thf(f2417,plain,
( ( $false = $true )
| ~ spl169_36
| ~ spl169_41 ),
inference(superposition,[],[f1521,f1544]) ).
thf(f2420,plain,
( $false
| ~ spl169_36
| ~ spl169_41 ),
inference(trivial_inequality_removal,[],[f2417]) ).
thf(f2421,plain,
( ~ spl169_36
| ~ spl169_41 ),
inference(avatar_contradiction_clause,[],[f2420]) ).
thf(f3252,plain,
( ! [X0: term > $o,X1: term] :
( ( ( X0 @ ( sK129 @ X0 @ id ) )
= $false )
| ( ( X0 @ ( sub @ X1 @ id ) )
= $true )
| ( ( X0 @ ( lam @ ( sK125 @ X0 ) ) )
= $false )
| ( ( X0 @ ( sK126 @ X0 ) )
= $true ) )
| ~ spl169_201
| ~ spl169_216 ),
inference(superposition,[],[f2211,f2274]) ).
thf(f3295,definition,
( spl169_289
<=> ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl169_289])],[avatar_definition]) ).
thf(f3296,plain,
( ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
!= $false )
| spl169_289 ),
inference(avatar_component_clause,[],[f3295]) ).
thf(f3297,plain,
( ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $false )
| ~ spl169_289 ),
inference(avatar_component_clause,[],[f3295]) ).
thf(f3302,definition,
( spl169_291
<=> ( $true
= ( sK107 @ ( sK126 @ sK107 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl169_291])],[avatar_definition]) ).
thf(f3303,plain,
( ( $true
!= ( sK107 @ ( sK126 @ sK107 ) ) )
| spl169_291 ),
inference(avatar_component_clause,[],[f3302]) ).
thf(f3304,plain,
( ( $true
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ~ spl169_291 ),
inference(avatar_component_clause,[],[f3302]) ).
thf(f3306,plain,
( ! [X0: term > $o,X1: term] :
( ( ( X0 @ ( sK129 @ X0 @ id ) )
= $false )
| ( ( X0 @ X1 )
= $true )
| ( ( X0 @ ( sK126 @ X0 ) )
= $true )
| ( ( X0 @ ( lam @ ( sK125 @ X0 ) ) )
= $false ) )
| ~ spl169_201
| ~ spl169_216 ),
inference(forward_demodulation,[],[f3252,f2274]) ).
thf(f3322,plain,
( ! [X0: term,X1: subst] :
( ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( $false = $true )
| ( $true
= ( var @ ( sK128 @ sK107 @ X1 ) ) )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $true )
| ( $true
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true ) )
| ~ spl169_157
| ~ spl169_194 ),
inference(superposition,[],[f2028,f2183]) ).
thf(f3337,plain,
( ! [X0: term,X1: subst] :
( ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( $true
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $true )
| ( $true
= ( var @ ( sK128 @ sK107 @ X1 ) ) ) )
| ~ spl169_157
| ~ spl169_194 ),
inference(trivial_inequality_removal,[],[f3322]) ).
thf(f3354,plain,
( ! [X0: term,X1: subst] :
( ( $true
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ( $true
= ( var @ ( sK128 @ sK107 @ X1 ) ) )
| ( $false = $true )
| ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) ) )
| ~ spl169_157
| ~ spl169_194
| ~ spl169_289 ),
inference(forward_demodulation,[],[f3337,f3297]) ).
thf(f3355,plain,
( ! [X0: term,X1: subst] :
( ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true )
| ( $true
= ( var @ ( sK128 @ sK107 @ X1 ) ) )
| ( $true
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) ) )
| ~ spl169_157
| ~ spl169_194
| ~ spl169_289 ),
inference(trivial_inequality_removal,[],[f3354]) ).
thf(f3357,definition,
( spl169_295
<=> ! [X0: term,X1: subst] :
( ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true )
| ( $true
= ( var @ ( sK128 @ sK107 @ X1 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl169_295])],[avatar_definition]) ).
thf(f3358,plain,
( ! [X0: term,X1: subst] :
( ( $true
= ( var @ ( sK128 @ sK107 @ X1 ) ) )
| ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true ) )
| ~ spl169_295 ),
inference(avatar_component_clause,[],[f3357]) ).
thf(f3360,definition,
( spl169_296
<=> ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl169_296])],[avatar_definition]) ).
thf(f3362,plain,
( ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ~ spl169_296 ),
inference(avatar_component_clause,[],[f3360]) ).
thf(f3364,plain,
( spl169_296
| spl169_295
| spl169_291
| ~ spl169_157
| ~ spl169_194
| ~ spl169_289 ),
inference(avatar_split_clause,[],[f3355,f3295,f2182,f2027,f3302,f3357,f3360]) ).
thf(f3372,plain,
( ! [X0: term,X1: subst] :
( ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true )
| ( $false
= ( sK107 @ ( sub @ ( sK128 @ sK107 @ X1 ) @ X1 ) ) )
| ( $true
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $true )
| ( $false = $true ) )
| ~ spl169_157
| ~ spl169_195 ),
inference(superposition,[],[f2028,f2187]) ).
thf(f3386,plain,
( ! [X0: term,X1: subst] :
( ( $false
= ( sK107 @ ( sub @ ( sK128 @ sK107 @ X1 ) @ X1 ) ) )
| ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( $true
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $true ) )
| ~ spl169_157
| ~ spl169_195 ),
inference(trivial_inequality_removal,[],[f3372]) ).
thf(f4089,plain,
( ! [X0: term] :
( ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $false )
| ( $true
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ( $false
= ( var @ ( sK129 @ sK107 @ id ) ) )
| ( $true
= ( sK107 @ X0 ) )
| ( $false = $true ) )
| ~ spl169_154
| ~ spl169_201
| ~ spl169_216 ),
inference(superposition,[],[f2016,f3306]) ).
thf(f4096,plain,
( ! [X0: term] :
( ( $true
= ( sK107 @ X0 ) )
| ( $true
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $false )
| ( $false
= ( var @ ( sK129 @ sK107 @ id ) ) ) )
| ~ spl169_154
| ~ spl169_201
| ~ spl169_216 ),
inference(trivial_inequality_removal,[],[f4089]) ).
thf(f4191,definition,
( spl169_315
<=> ! [X0: term] :
( $true
= ( sK107 @ X0 ) ) ),
introduced(definition,[new_symbols(definition,[spl169_315])],[avatar_definition]) ).
thf(f4192,plain,
( ! [X0: term] :
( $true
= ( sK107 @ X0 ) )
| ~ spl169_315 ),
inference(avatar_component_clause,[],[f4191]) ).
thf(f4349,plain,
( ( $false = $true )
| ~ spl169_158
| ~ spl169_315 ),
inference(superposition,[],[f2033,f4192]) ).
thf(f4369,plain,
( $false
| ~ spl169_158
| ~ spl169_315 ),
inference(trivial_inequality_removal,[],[f4349]) ).
thf(f4370,plain,
( ~ spl169_158
| ~ spl169_315 ),
inference(avatar_contradiction_clause,[],[f4369]) ).
thf(f4462,plain,
( ! [X0: term > $o,X1: term] :
( ( $true
= ( X0 @ ( sK127 @ X0 ) ) )
| ( ( X0 @ ( lam @ ( sK125 @ X0 ) ) )
= $false )
| ( ( X0 @ ( sK130 @ X0 @ id ) )
= $false )
| ( ( X0 @ ( sub @ X1 @ id ) )
= $true ) )
| ~ spl169_203
| ~ spl169_216 ),
inference(superposition,[],[f2219,f2274]) ).
thf(f4503,plain,
( ! [X0: term > $o,X1: term] :
( ( ( X0 @ ( sK130 @ X0 @ id ) )
= $false )
| ( $true
= ( X0 @ ( sK127 @ X0 ) ) )
| ( ( X0 @ X1 )
= $true )
| ( ( X0 @ ( lam @ ( sK125 @ X0 ) ) )
= $false ) )
| ~ spl169_203
| ~ spl169_216 ),
inference(forward_demodulation,[],[f4462,f2274]) ).
thf(f4514,plain,
( ! [X0: subst,X1: term] :
( ( $false = $true )
| ( $true
= ( var @ ( sK131 @ sK107 @ X0 ) ) )
| ( ( sK107 @ ( sub @ X1 @ X0 ) )
= $true )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $false )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $false )
| ( $false
= ( sK107 @ ( sK126 @ sK107 ) ) ) )
| ~ spl169_155
| ~ spl169_204 ),
inference(superposition,[],[f2020,f2223]) ).
thf(f4522,plain,
( ! [X0: subst,X1: term] :
( ( ( sK107 @ ( sK127 @ sK107 ) )
= $false )
| ( $true
= ( var @ ( sK131 @ sK107 @ X0 ) ) )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $false )
| ( $false
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ( ( sK107 @ ( sub @ X1 @ X0 ) )
= $true ) )
| ~ spl169_155
| ~ spl169_204 ),
inference(trivial_inequality_removal,[],[f4514]) ).
thf(f5248,plain,
( ! [X0: term] :
( ( ( sK107 @ ( sK127 @ sK107 ) )
= $true )
| ( ( var @ ( sK130 @ sK107 @ id ) )
= $false )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $false )
| ( $false = $true )
| ( $true
= ( sK107 @ X0 ) ) )
| ~ spl169_154
| ~ spl169_203
| ~ spl169_216 ),
inference(superposition,[],[f2016,f4503]) ).
thf(f5262,plain,
( ! [X0: term] :
( ( $true
= ( sK107 @ X0 ) )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $false )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $true )
| ( ( var @ ( sK130 @ sK107 @ id ) )
= $false ) )
| ~ spl169_154
| ~ spl169_203
| ~ spl169_216 ),
inference(trivial_inequality_removal,[],[f5248]) ).
thf(f6240,plain,
( ! [X0: term,X1: subst] :
( ( ( sK107 @ ( sK127 @ sK107 ) )
= $true )
| ( $false = $true )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $true )
| ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true )
| ( $true
= ( var @ ( sK128 @ sK107 @ X1 ) ) )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) ) )
| ~ spl169_157
| ~ spl169_196 ),
inference(superposition,[],[f2028,f2191]) ).
thf(f6253,plain,
( ! [X0: term,X1: subst] :
( ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $true )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $true )
| ( $true
= ( var @ ( sK128 @ sK107 @ X1 ) ) ) )
| ~ spl169_157
| ~ spl169_196 ),
inference(trivial_inequality_removal,[],[f6240]) ).
thf(f6265,plain,
( ! [X0: term,X1: subst] :
( ( $false = $true )
| ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $true )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( $true
= ( var @ ( sK128 @ sK107 @ X1 ) ) ) )
| ~ spl169_157
| ~ spl169_196
| ~ spl169_289 ),
inference(forward_demodulation,[],[f6253,f3297]) ).
thf(f6266,plain,
( ! [X0: term,X1: subst] :
( ( $true
= ( var @ ( sK128 @ sK107 @ X1 ) ) )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $true ) )
| ~ spl169_157
| ~ spl169_196
| ~ spl169_289 ),
inference(trivial_inequality_removal,[],[f6265]) ).
thf(f6268,definition,
( spl169_350
<=> ( ( sK107 @ ( sK127 @ sK107 ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl169_350])],[avatar_definition]) ).
thf(f6270,plain,
( ( ( sK107 @ ( sK127 @ sK107 ) )
= $true )
| ~ spl169_350 ),
inference(avatar_component_clause,[],[f6268]) ).
thf(f6272,plain,
( spl169_296
| spl169_295
| spl169_350
| ~ spl169_157
| ~ spl169_196
| ~ spl169_289 ),
inference(avatar_split_clause,[],[f6266,f3295,f2190,f2027,f6268,f3357,f3360]) ).
thf(f6367,plain,
( ! [X0: term > $o,X1: term] :
( ( ( X0 @ ( sub @ X1 @ id ) )
= $true )
| ( ( X0 @ ( lam @ ( sK125 @ X0 ) ) )
= $false )
| ( $false
= ( X0 @ ( sK131 @ X0 @ id ) ) )
| ( $false
= ( X0 @ ( ap @ ( sK126 @ X0 ) @ ( sK127 @ X0 ) ) ) ) )
| ~ spl169_205
| ~ spl169_216 ),
inference(superposition,[],[f2227,f2274]) ).
thf(f6445,plain,
( ! [X0: term > $o,X1: term] :
( ( $false
= ( X0 @ ( ap @ ( sK126 @ X0 ) @ ( sK127 @ X0 ) ) ) )
| ( ( X0 @ ( lam @ ( sK125 @ X0 ) ) )
= $false )
| ( ( X0 @ X1 )
= $true )
| ( $false
= ( X0 @ ( sK131 @ X0 @ id ) ) ) )
| ~ spl169_205
| ~ spl169_216 ),
inference(forward_demodulation,[],[f6367,f2274]) ).
thf(f6450,plain,
( ! [X0: term] :
( ( $false = $true )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $false )
| ( $false
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $false )
| ( ( sK107 @ ( sK131 @ sK107 @ id ) )
= $false )
| ( $true
= ( sK107 @ X0 ) ) )
| ~ spl169_155
| ~ spl169_205
| ~ spl169_216 ),
inference(superposition,[],[f6445,f2020]) ).
thf(f6465,plain,
( ! [X0: term] :
( ( ( sK107 @ ( sK131 @ sK107 @ id ) )
= $false )
| ( $true
= ( sK107 @ X0 ) )
| ( $false
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $false )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $false ) )
| ~ spl169_155
| ~ spl169_205
| ~ spl169_216 ),
inference(trivial_inequality_removal,[],[f6450]) ).
thf(f6687,plain,
( ! [X0: subst,X1: term] :
( ( $false = $true )
| ( ( sK107 @ ( sub @ X1 @ X0 ) )
= $true )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $true )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $true )
| ( $false
= ( sK107 @ ( sub @ ( sK128 @ sK107 @ X0 ) @ X0 ) ) )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) ) )
| ~ spl169_157
| ~ spl169_197 ),
inference(superposition,[],[f2028,f2195]) ).
thf(f6707,plain,
( ! [X0: subst,X1: term] :
( ( ( sK107 @ ( sub @ X1 @ X0 ) )
= $true )
| ( $false
= ( sK107 @ ( sub @ ( sK128 @ sK107 @ X0 ) @ X0 ) ) )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $true )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $true ) )
| ~ spl169_157
| ~ spl169_197 ),
inference(trivial_inequality_removal,[],[f6687]) ).
thf(f6791,plain,
( ! [X0: subst,X1: term] :
( ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $true )
| ( $false = $true )
| ( ( var @ ( sK128 @ sK107 @ X0 ) )
= $true )
| ( ( sK107 @ ( sub @ X1 @ X0 ) )
= $true )
| ( ( sK107 @ ( ap @ ( sK126 @ sK107 ) @ ( sK127 @ sK107 ) ) )
= $false ) )
| ~ spl169_157
| ~ spl169_198 ),
inference(superposition,[],[f2028,f2199]) ).
thf(f6819,plain,
( ! [X0: subst,X1: term] :
( ( ( sK107 @ ( sub @ X1 @ X0 ) )
= $true )
| ( ( sK107 @ ( ap @ ( sK126 @ sK107 ) @ ( sK127 @ sK107 ) ) )
= $false )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( ( var @ ( sK128 @ sK107 @ X0 ) )
= $true )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $true ) )
| ~ spl169_157
| ~ spl169_198 ),
inference(trivial_inequality_removal,[],[f6791]) ).
thf(f6822,plain,
( ! [X0: subst,X1: term] :
( ( $false = $true )
| ( ( var @ ( sK128 @ sK107 @ X0 ) )
= $true )
| ( ( sK107 @ ( sub @ X1 @ X0 ) )
= $true )
| ( ( sK107 @ ( ap @ ( sK126 @ sK107 ) @ ( sK127 @ sK107 ) ) )
= $false )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) ) )
| ~ spl169_157
| ~ spl169_198
| ~ spl169_289 ),
inference(forward_demodulation,[],[f6819,f3297]) ).
thf(f6823,plain,
( ! [X0: subst,X1: term] :
( ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( ( var @ ( sK128 @ sK107 @ X0 ) )
= $true )
| ( ( sK107 @ ( sub @ X1 @ X0 ) )
= $true )
| ( ( sK107 @ ( ap @ ( sK126 @ sK107 ) @ ( sK127 @ sK107 ) ) )
= $false ) )
| ~ spl169_157
| ~ spl169_198
| ~ spl169_289 ),
inference(trivial_inequality_removal,[],[f6822]) ).
thf(f6825,definition,
( spl169_359
<=> ( ( sK107 @ ( ap @ ( sK126 @ sK107 ) @ ( sK127 @ sK107 ) ) )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl169_359])],[avatar_definition]) ).
thf(f6827,plain,
( ( ( sK107 @ ( ap @ ( sK126 @ sK107 ) @ ( sK127 @ sK107 ) ) )
= $false )
| ~ spl169_359 ),
inference(avatar_component_clause,[],[f6825]) ).
thf(f6829,plain,
( spl169_359
| spl169_296
| spl169_295
| ~ spl169_157
| ~ spl169_198
| ~ spl169_289 ),
inference(avatar_split_clause,[],[f6823,f3295,f2198,f2027,f3357,f3360,f6825]) ).
thf(f6833,plain,
( ( ( sK107 @ ( sK127 @ sK107 ) )
= $false )
| ( $false
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ( $false = $true )
| ~ spl169_155
| ~ spl169_359 ),
inference(superposition,[],[f2020,f6827]) ).
thf(f7403,plain,
( ! [X0: term,X1: subst] :
( ( $false = $true )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $true )
| ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true )
| ( ( sK107 @ ( ap @ ( sK126 @ sK107 ) @ ( sK127 @ sK107 ) ) )
= $false )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( $false
= ( sK107 @ ( sub @ ( sK128 @ sK107 @ X1 ) @ X1 ) ) ) )
| ~ spl169_157
| ~ spl169_199 ),
inference(superposition,[],[f2028,f2203]) ).
thf(f7405,plain,
( ! [X0: term,X1: subst] :
( ( ( sK107 @ ( ap @ ( sK126 @ sK107 ) @ ( sK127 @ sK107 ) ) )
= $false )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $true )
| ( $false
= ( sK107 @ ( sub @ ( sK128 @ sK107 @ X1 ) @ X1 ) ) ) )
| ~ spl169_157
| ~ spl169_199 ),
inference(trivial_inequality_removal,[],[f7403]) ).
thf(f7453,definition,
( spl169_374
<=> ! [X0: term,X1: subst] :
( ( $false
= ( sK107 @ ( sub @ ( sK128 @ sK107 @ X1 ) @ X1 ) ) )
| ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl169_374])],[avatar_definition]) ).
thf(f7454,plain,
( ! [X0: term,X1: subst] :
( ( $false
= ( sK107 @ ( sub @ ( sK128 @ sK107 @ X1 ) @ X1 ) ) )
| ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true ) )
| ~ spl169_374 ),
inference(avatar_component_clause,[],[f7453]) ).
thf(f7457,plain,
( ! [X0: term] :
( ( ( sK107 @ ( sub @ X0 @ id ) )
= $true )
| ( $false
= ( sK107 @ ( sK128 @ sK107 @ id ) ) ) )
| ~ spl169_216
| ~ spl169_374 ),
inference(superposition,[],[f7454,f2274]) ).
thf(f7540,plain,
( ! [X0: term] :
( ( $true
= ( sK107 @ X0 ) )
| ( $false
= ( sK107 @ ( sK128 @ sK107 @ id ) ) ) )
| ~ spl169_216
| ~ spl169_374 ),
inference(forward_demodulation,[],[f7457,f2274]) ).
thf(f7546,definition,
( spl169_379
<=> ( $false
= ( sK107 @ ( sK128 @ sK107 @ id ) ) ) ),
introduced(definition,[new_symbols(definition,[spl169_379])],[avatar_definition]) ).
thf(f7548,plain,
( ( $false
= ( sK107 @ ( sK128 @ sK107 @ id ) ) )
| ~ spl169_379 ),
inference(avatar_component_clause,[],[f7546]) ).
thf(f7549,plain,
( spl169_315
| spl169_379
| ~ spl169_216
| ~ spl169_374 ),
inference(avatar_split_clause,[],[f7540,f7453,f2273,f7546,f4191]) ).
thf(f7558,plain,
( ( $false = $true )
| ( $false
= ( var @ ( sK128 @ sK107 @ id ) ) )
| ~ spl169_154
| ~ spl169_379 ),
inference(superposition,[],[f7548,f2016]) ).
thf(f7561,plain,
( ( $false
= ( var @ ( sK128 @ sK107 @ id ) ) )
| ~ spl169_154
| ~ spl169_379 ),
inference(trivial_inequality_removal,[],[f7558]) ).
thf(f7566,plain,
( ! [X0: term] :
( ( $false = $true )
| ( ( sK107 @ ( sub @ X0 @ id ) )
= $true ) )
| ~ spl169_154
| ~ spl169_295
| ~ spl169_379 ),
inference(superposition,[],[f3358,f7561]) ).
thf(f7568,plain,
( ! [X0: term] :
( ( sK107 @ ( sub @ X0 @ id ) )
= $true )
| ~ spl169_154
| ~ spl169_295
| ~ spl169_379 ),
inference(trivial_inequality_removal,[],[f7566]) ).
thf(f7570,plain,
( ! [X0: term] :
( $true
= ( sK107 @ X0 ) )
| ~ spl169_154
| ~ spl169_216
| ~ spl169_295
| ~ spl169_379 ),
inference(forward_demodulation,[],[f7568,f2274]) ).
thf(f7572,plain,
( spl169_315
| ~ spl169_154
| ~ spl169_216
| ~ spl169_295
| ~ spl169_379 ),
inference(avatar_split_clause,[],[f7570,f7546,f3357,f2273,f2015,f4191]) ).
thf(f7643,plain,
( ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $true )
| ( $false = $true )
| ~ spl169_156
| ~ spl169_296 ),
inference(superposition,[],[f2024,f3362]) ).
thf(f7649,plain,
( ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $true )
| ~ spl169_156
| ~ spl169_296 ),
inference(trivial_inequality_removal,[],[f7643]) ).
thf(f7653,plain,
( ( $false = $true )
| ~ spl169_156
| ~ spl169_289
| ~ spl169_296 ),
inference(forward_demodulation,[],[f7649,f3297]) ).
thf(f7654,plain,
( $false
| ~ spl169_156
| ~ spl169_289
| ~ spl169_296 ),
inference(trivial_inequality_removal,[],[f7653]) ).
thf(f7655,plain,
( ~ spl169_156
| ~ spl169_289
| ~ spl169_296 ),
inference(avatar_contradiction_clause,[],[f7654]) ).
thf(f7656,plain,
( ( $false
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $false )
| ~ spl169_155
| ~ spl169_359 ),
inference(trivial_inequality_removal,[],[f6833]) ).
thf(f7670,plain,
( ! [X0: term,X1: subst] :
( ( $false
= ( sK107 @ ( sub @ ( sK128 @ sK107 @ X1 ) @ X1 ) ) )
| ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( $false = $true )
| ( ( sK107 @ ( ap @ ( sK126 @ sK107 ) @ ( sK127 @ sK107 ) ) )
= $false ) )
| ~ spl169_157
| ~ spl169_199
| ~ spl169_289 ),
inference(forward_demodulation,[],[f7405,f3297]) ).
thf(f7671,plain,
( ! [X0: term,X1: subst] :
( ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( $false
= ( sK107 @ ( sub @ ( sK128 @ sK107 @ X1 ) @ X1 ) ) )
| ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true )
| ( ( sK107 @ ( ap @ ( sK126 @ sK107 ) @ ( sK127 @ sK107 ) ) )
= $false ) )
| ~ spl169_157
| ~ spl169_199
| ~ spl169_289 ),
inference(trivial_inequality_removal,[],[f7670]) ).
thf(f7672,plain,
( ( $false = $true )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $false )
| ~ spl169_155
| ~ spl169_291
| ~ spl169_359 ),
inference(forward_demodulation,[],[f7656,f3304]) ).
thf(f7678,plain,
( ! [X0: subst,X1: term] :
( ( $false
= ( sK107 @ ( sub @ ( sK128 @ sK107 @ X0 ) @ X0 ) ) )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( ( sK107 @ ( sub @ X1 @ X0 ) )
= $true )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $true )
| ( $false = $true ) )
| ~ spl169_157
| ~ spl169_197
| ~ spl169_289 ),
inference(forward_demodulation,[],[f6707,f3297]) ).
thf(f7679,plain,
( ! [X0: subst,X1: term] :
( ( $false
= ( sK107 @ ( sub @ ( sK128 @ sK107 @ X0 ) @ X0 ) ) )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $true )
| ( ( sK107 @ ( sub @ X1 @ X0 ) )
= $true )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) ) )
| ~ spl169_157
| ~ spl169_197
| ~ spl169_289 ),
inference(trivial_inequality_removal,[],[f7678]) ).
thf(f7689,plain,
( spl169_359
| spl169_296
| spl169_374
| ~ spl169_157
| ~ spl169_199
| ~ spl169_289 ),
inference(avatar_split_clause,[],[f7671,f3295,f2202,f2027,f7453,f3360,f6825]) ).
thf(f7690,plain,
( spl169_350
| spl169_296
| spl169_374
| ~ spl169_157
| ~ spl169_197
| ~ spl169_289 ),
inference(avatar_split_clause,[],[f7679,f3295,f2194,f2027,f7453,f3360,f6268]) ).
thf(f7698,definition,
( spl169_385
<=> ( ( sK107 @ ( sK127 @ sK107 ) )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl169_385])],[avatar_definition]) ).
thf(f7700,plain,
( ( ( sK107 @ ( sK127 @ sK107 ) )
= $false )
| ~ spl169_385 ),
inference(avatar_component_clause,[],[f7698]) ).
thf(f7702,definition,
( spl169_386
<=> ( $false
= ( sK107 @ ( sK126 @ sK107 ) ) ) ),
introduced(definition,[new_symbols(definition,[spl169_386])],[avatar_definition]) ).
thf(f7704,plain,
( ( $false
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ~ spl169_386 ),
inference(avatar_component_clause,[],[f7702]) ).
thf(f7721,plain,
( ! [X0: term,X1: subst] :
( ( $true
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) )
| ( $false
= ( sK107 @ ( sub @ ( sK128 @ sK107 @ X1 ) @ X1 ) ) )
| ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true )
| ( $false = $true ) )
| ~ spl169_157
| ~ spl169_195
| ~ spl169_289 ),
inference(forward_demodulation,[],[f3386,f3297]) ).
thf(f7722,plain,
( ! [X0: term,X1: subst] :
( ( ( sK107 @ ( sub @ X0 @ X1 ) )
= $true )
| ( $false
= ( sK107 @ ( sub @ ( sK128 @ sK107 @ X1 ) @ X1 ) ) )
| ( $true
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ( $false
= ( sK107 @ ( sK108 @ ( sK125 @ sK107 ) ) ) ) )
| ~ spl169_157
| ~ spl169_195
| ~ spl169_289 ),
inference(trivial_inequality_removal,[],[f7721]) ).
thf(f7727,plain,
( spl169_296
| spl169_291
| spl169_374
| ~ spl169_157
| ~ spl169_195
| ~ spl169_289 ),
inference(avatar_split_clause,[],[f7722,f3295,f2186,f2027,f7453,f3302,f3360]) ).
thf(f7728,plain,
( ( ( sK107 @ ( sK127 @ sK107 ) )
= $false )
| ~ spl169_155
| ~ spl169_291
| ~ spl169_359 ),
inference(trivial_inequality_removal,[],[f7672]) ).
thf(f7749,plain,
( spl169_385
| ~ spl169_155
| ~ spl169_291
| ~ spl169_359 ),
inference(avatar_split_clause,[],[f7728,f6825,f3302,f2019,f7698]) ).
thf(f7776,definition,
( spl169_397
<=> ! [X0: subst,X1: term] :
( ( $true
= ( var @ ( sK131 @ sK107 @ X0 ) ) )
| ( ( sK107 @ ( sub @ X1 @ X0 ) )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl169_397])],[avatar_definition]) ).
thf(f7777,plain,
( ! [X0: subst,X1: term] :
( ( $true
= ( var @ ( sK131 @ sK107 @ X0 ) ) )
| ( ( sK107 @ ( sub @ X1 @ X0 ) )
= $true ) )
| ~ spl169_397 ),
inference(avatar_component_clause,[],[f7776]) ).
thf(f7807,definition,
( spl169_403
<=> ( ( sK107 @ ( sK131 @ sK107 @ id ) )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl169_403])],[avatar_definition]) ).
thf(f7809,plain,
( ( ( sK107 @ ( sK131 @ sK107 @ id ) )
= $false )
| ~ spl169_403 ),
inference(avatar_component_clause,[],[f7807]) ).
thf(f7817,definition,
( spl169_405
<=> ( $false
= ( var @ ( sK129 @ sK107 @ id ) ) ) ),
introduced(definition,[new_symbols(definition,[spl169_405])],[avatar_definition]) ).
thf(f7819,plain,
( ( $false
= ( var @ ( sK129 @ sK107 @ id ) ) )
| ~ spl169_405 ),
inference(avatar_component_clause,[],[f7817]) ).
thf(f7839,plain,
( spl169_386
| spl169_385
| spl169_289
| spl169_403
| spl169_315
| ~ spl169_155
| ~ spl169_205
| ~ spl169_216 ),
inference(avatar_split_clause,[],[f6465,f2273,f2226,f2019,f4191,f7807,f3295,f7698,f7702]) ).
thf(f7857,plain,
( spl169_385
| spl169_397
| spl169_289
| spl169_386
| ~ spl169_155
| ~ spl169_204 ),
inference(avatar_split_clause,[],[f4522,f2222,f2019,f7702,f3295,f7776,f7698]) ).
thf(f7871,definition,
( spl169_413
<=> ( ( var @ ( sK130 @ sK107 @ id ) )
= $false ) ),
introduced(definition,[new_symbols(definition,[spl169_413])],[avatar_definition]) ).
thf(f7873,plain,
( ( ( var @ ( sK130 @ sK107 @ id ) )
= $false )
| ~ spl169_413 ),
inference(avatar_component_clause,[],[f7871]) ).
thf(f7876,plain,
( spl169_315
| spl169_289
| spl169_350
| spl169_413
| ~ spl169_154
| ~ spl169_203
| ~ spl169_216 ),
inference(avatar_split_clause,[],[f5262,f2273,f2218,f2015,f7871,f6268,f3295,f4191]) ).
thf(f7877,plain,
( spl169_289
| spl169_405
| spl169_315
| spl169_291
| ~ spl169_154
| ~ spl169_201
| ~ spl169_216 ),
inference(avatar_split_clause,[],[f4096,f2273,f2210,f2015,f3302,f4191,f7817,f3295]) ).
thf(f7996,plain,
( ( $false = $true )
| ~ spl169_291
| ~ spl169_386 ),
inference(superposition,[],[f3304,f7704]) ).
thf(f8003,plain,
( $false
| ~ spl169_291
| ~ spl169_386 ),
inference(trivial_inequality_removal,[],[f7996]) ).
thf(f8004,plain,
( ~ spl169_291
| ~ spl169_386 ),
inference(avatar_contradiction_clause,[],[f8003]) ).
thf(f8362,plain,
( ( ( var @ ( sK131 @ sK107 @ id ) )
= $false )
| ( $false = $true )
| ~ spl169_154
| ~ spl169_403 ),
inference(superposition,[],[f2016,f7809]) ).
thf(f8363,plain,
( ( ( var @ ( sK131 @ sK107 @ id ) )
= $false )
| ~ spl169_154
| ~ spl169_403 ),
inference(trivial_inequality_removal,[],[f8362]) ).
thf(f8398,plain,
( ! [X0: term] :
( ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $false )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $true )
| ( ( sK107 @ ( sub @ X0 @ id ) )
= $true )
| ( $false = $true ) )
| ~ spl169_202
| ~ spl169_413 ),
inference(superposition,[],[f7873,f2215]) ).
thf(f8403,plain,
( ! [X0: term] :
( ( ( sK107 @ ( sub @ X0 @ id ) )
= $true )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $false )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $true ) )
| ~ spl169_202
| ~ spl169_413 ),
inference(trivial_inequality_removal,[],[f8398]) ).
thf(f8412,plain,
( ( $false = $true )
| ~ spl169_350
| ~ spl169_385 ),
inference(forward_demodulation,[],[f6270,f7700]) ).
thf(f8413,plain,
( $false
| ~ spl169_350
| ~ spl169_385 ),
inference(trivial_inequality_removal,[],[f8412]) ).
thf(f8414,plain,
( ~ spl169_350
| ~ spl169_385 ),
inference(avatar_contradiction_clause,[],[f8413]) ).
thf(f8415,plain,
( ! [X0: term] :
( ( ( sK107 @ ( sub @ X0 @ id ) )
= $true )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $true ) )
| ~ spl169_202
| spl169_289
| ~ spl169_413 ),
inference(forward_subsumption_resolution,[],[f8403,f3296]) ).
thf(f8425,plain,
( ! [X0: term] :
( ( $true
= ( sK107 @ X0 ) )
| ( ( sK107 @ ( sK127 @ sK107 ) )
= $true ) )
| ~ spl169_202
| ~ spl169_216
| spl169_289
| ~ spl169_413 ),
inference(forward_demodulation,[],[f8415,f2274]) ).
thf(f8427,plain,
( spl169_350
| spl169_315
| ~ spl169_202
| ~ spl169_216
| spl169_289
| ~ spl169_413 ),
inference(avatar_split_clause,[],[f8425,f7871,f3295,f2273,f2214,f4191,f6268]) ).
thf(f8604,plain,
( ! [X0: term] :
( ( $true
= ( sK107 @ ( sK126 @ sK107 ) ) )
| ( $false = $true )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $false )
| ( ( sK107 @ ( sub @ X0 @ id ) )
= $true ) )
| ~ spl169_200
| ~ spl169_405 ),
inference(superposition,[],[f2207,f7819]) ).
thf(f8605,plain,
( ! [X0: term] :
( ( ( sK107 @ ( sub @ X0 @ id ) )
= $true )
| ( ( sK107 @ ( lam @ ( sK125 @ sK107 ) ) )
= $false )
| ( $true
= ( sK107 @ ( sK126 @ sK107 ) ) ) )
| ~ spl169_200
| ~ spl169_405 ),
inference(trivial_inequality_removal,[],[f8604]) ).
thf(f8608,plain,
( ! [X0: term] :
( ( ( sK107 @ ( sub @ X0 @ id ) )
= $true )
| ( $true
= ( sK107 @ ( sK126 @ sK107 ) ) ) )
| ~ spl169_200
| spl169_289
| ~ spl169_405 ),
inference(forward_subsumption_resolution,[],[f8605,f3296]) ).
thf(f8610,plain,
( ! [X0: term] :
( ( sK107 @ ( sub @ X0 @ id ) )
= $true )
| ~ spl169_200
| spl169_289
| spl169_291
| ~ spl169_405 ),
inference(forward_subsumption_resolution,[],[f8608,f3303]) ).
thf(f8612,plain,
( ! [X0: term] :
( $true
= ( sK107 @ X0 ) )
| ~ spl169_200
| ~ spl169_216
| spl169_289
| spl169_291
| ~ spl169_405 ),
inference(forward_demodulation,[],[f8610,f2274]) ).
thf(f8614,plain,
( spl169_315
| ~ spl169_200
| ~ spl169_216
| spl169_289
| spl169_291
| ~ spl169_405 ),
inference(avatar_split_clause,[],[f8612,f7817,f3302,f3295,f2273,f2206,f4191]) ).
thf(f8921,plain,
( ! [X0: term] :
( ( ( sK107 @ ( sub @ X0 @ id ) )
= $true )
| ( $false = $true ) )
| ~ spl169_154
| ~ spl169_397
| ~ spl169_403 ),
inference(superposition,[],[f7777,f8363]) ).
thf(f8923,plain,
( ! [X0: term] :
( ( sK107 @ ( sub @ X0 @ id ) )
= $true )
| ~ spl169_154
| ~ spl169_397
| ~ spl169_403 ),
inference(trivial_inequality_removal,[],[f8921]) ).
thf(f8925,plain,
( ! [X0: term] :
( $true
= ( sK107 @ X0 ) )
| ~ spl169_154
| ~ spl169_216
| ~ spl169_397
| ~ spl169_403 ),
inference(forward_demodulation,[],[f8923,f2274]) ).
thf(f8927,plain,
( spl169_315
| ~ spl169_154
| ~ spl169_216
| ~ spl169_397
| ~ spl169_403 ),
inference(avatar_split_clause,[],[f8925,f7807,f7776,f2273,f2015,f4191]) ).
cnf(s24,plain,
( spl169_38
| spl169_39 ),
inference(sat_conversion,[],[f1535]) ).
cnf(s25,plain,
( spl169_39
| spl169_40 ),
inference(sat_conversion,[],[f1540]) ).
cnf(s26,plain,
( spl169_39
| spl169_41 ),
inference(sat_conversion,[],[f1545]) ).
cnf(s113,plain,
( spl169_36
| spl169_154 ),
inference(sat_conversion,[],[f2017]) ).
cnf(s114,plain,
( spl169_36
| spl169_155 ),
inference(sat_conversion,[],[f2021]) ).
cnf(s115,plain,
( spl169_36
| spl169_156 ),
inference(sat_conversion,[],[f2025]) ).
cnf(s116,plain,
( spl169_36
| spl169_157 ),
inference(sat_conversion,[],[f2029]) ).
cnf(s117,plain,
( spl169_36
| spl169_158 ),
inference(sat_conversion,[],[f2034]) ).
cnf(s143,plain,
( spl169_34
| spl169_194 ),
inference(sat_conversion,[],[f2184]) ).
cnf(s144,plain,
( spl169_34
| spl169_195 ),
inference(sat_conversion,[],[f2188]) ).
cnf(s145,plain,
( spl169_34
| spl169_196 ),
inference(sat_conversion,[],[f2192]) ).
cnf(s146,plain,
( spl169_34
| spl169_197 ),
inference(sat_conversion,[],[f2196]) ).
cnf(s147,plain,
( spl169_34
| spl169_198 ),
inference(sat_conversion,[],[f2200]) ).
cnf(s148,plain,
( spl169_34
| spl169_199 ),
inference(sat_conversion,[],[f2204]) ).
cnf(s149,plain,
( spl169_34
| spl169_200 ),
inference(sat_conversion,[],[f2208]) ).
cnf(s150,plain,
( spl169_34
| spl169_201 ),
inference(sat_conversion,[],[f2212]) ).
cnf(s151,plain,
( spl169_34
| spl169_202 ),
inference(sat_conversion,[],[f2216]) ).
cnf(s152,plain,
( spl169_34
| spl169_203 ),
inference(sat_conversion,[],[f2220]) ).
cnf(s153,plain,
( spl169_34
| spl169_204 ),
inference(sat_conversion,[],[f2224]) ).
cnf(s154,plain,
( spl169_34
| spl169_205 ),
inference(sat_conversion,[],[f2228]) ).
cnf(s163,plain,
( spl169_37
| spl169_216 ),
inference(sat_conversion,[],[f2275]) ).
cnf(s187,plain,
~ spl169_39,
inference(sat_conversion,[],[f2407]) ).
cnf(s188,plain,
( ~ spl169_37
| ~ spl169_38 ),
inference(sat_conversion,[],[f2410]) ).
cnf(s189,plain,
( ~ spl169_34
| ~ spl169_40 ),
inference(sat_conversion,[],[f2414]) ).
cnf(s191,plain,
( ~ spl169_36
| ~ spl169_41 ),
inference(sat_conversion,[],[f2421]) ).
cnf(s242,plain,
( ~ spl169_157
| ~ spl169_194
| ~ spl169_289
| spl169_291
| spl169_295
| spl169_296 ),
inference(sat_conversion,[],[f3364]) ).
cnf(s267,plain,
( ~ spl169_158
| ~ spl169_315 ),
inference(sat_conversion,[],[f4370]) ).
cnf(s314,plain,
( ~ spl169_157
| ~ spl169_196
| ~ spl169_289
| spl169_295
| spl169_296
| spl169_350 ),
inference(sat_conversion,[],[f6272]) ).
cnf(s327,plain,
( ~ spl169_157
| ~ spl169_198
| ~ spl169_289
| spl169_295
| spl169_296
| spl169_359 ),
inference(sat_conversion,[],[f6829]) ).
cnf(s357,plain,
( ~ spl169_216
| spl169_315
| ~ spl169_374
| spl169_379 ),
inference(sat_conversion,[],[f7549]) ).
cnf(s358,plain,
( ~ spl169_154
| ~ spl169_216
| ~ spl169_295
| spl169_315
| ~ spl169_379 ),
inference(sat_conversion,[],[f7572]) ).
cnf(s363,plain,
( ~ spl169_156
| ~ spl169_289
| ~ spl169_296 ),
inference(sat_conversion,[],[f7655]) ).
cnf(s367,plain,
( ~ spl169_157
| ~ spl169_199
| ~ spl169_289
| spl169_296
| spl169_359
| spl169_374 ),
inference(sat_conversion,[],[f7689]) ).
cnf(s368,plain,
( ~ spl169_157
| ~ spl169_197
| ~ spl169_289
| spl169_296
| spl169_350
| spl169_374 ),
inference(sat_conversion,[],[f7690]) ).
cnf(s383,plain,
( ~ spl169_157
| ~ spl169_195
| ~ spl169_289
| spl169_291
| spl169_296
| spl169_374 ),
inference(sat_conversion,[],[f7727]) ).
cnf(s387,plain,
( ~ spl169_155
| ~ spl169_291
| ~ spl169_359
| spl169_385 ),
inference(sat_conversion,[],[f7749]) ).
cnf(s426,plain,
( ~ spl169_155
| ~ spl169_205
| ~ spl169_216
| spl169_289
| spl169_315
| spl169_385
| spl169_386
| spl169_403 ),
inference(sat_conversion,[],[f7839]) ).
cnf(s439,plain,
( ~ spl169_155
| ~ spl169_204
| spl169_289
| spl169_385
| spl169_386
| spl169_397 ),
inference(sat_conversion,[],[f7857]) ).
cnf(s451,plain,
( ~ spl169_154
| ~ spl169_203
| ~ spl169_216
| spl169_289
| spl169_315
| spl169_350
| spl169_413 ),
inference(sat_conversion,[],[f7876]) ).
cnf(s452,plain,
( ~ spl169_154
| ~ spl169_201
| ~ spl169_216
| spl169_289
| spl169_291
| spl169_315
| spl169_405 ),
inference(sat_conversion,[],[f7877]) ).
cnf(s477,plain,
( ~ spl169_291
| ~ spl169_386 ),
inference(sat_conversion,[],[f8004]) ).
cnf(s483,plain,
( ~ spl169_350
| ~ spl169_385 ),
inference(sat_conversion,[],[f8414]) ).
cnf(s489,plain,
( ~ spl169_202
| ~ spl169_216
| spl169_289
| spl169_315
| spl169_350
| ~ spl169_413 ),
inference(sat_conversion,[],[f8427]) ).
cnf(s493,plain,
( ~ spl169_200
| ~ spl169_216
| spl169_289
| spl169_291
| spl169_315
| ~ spl169_405 ),
inference(sat_conversion,[],[f8614]) ).
cnf(s498,plain,
( ~ spl169_154
| ~ spl169_216
| spl169_315
| ~ spl169_397
| ~ spl169_403 ),
inference(sat_conversion,[],[f8927]) ).
cnf(s500,plain,
spl169_41,
inference(rat,[],[s26,s187]) ).
cnf(s501,plain,
~ spl169_36,
inference(rat,[],[s191,s500]) ).
cnf(s502,plain,
spl169_158,
inference(rat,[],[s117,s501]) ).
cnf(s503,plain,
spl169_157,
inference(rat,[],[s116,s501]) ).
cnf(s504,plain,
spl169_156,
inference(rat,[],[s115,s501]) ).
cnf(s505,plain,
spl169_155,
inference(rat,[],[s114,s501]) ).
cnf(s506,plain,
spl169_154,
inference(rat,[],[s113,s501]) ).
cnf(s507,plain,
~ spl169_315,
inference(rat,[],[s267,s502]) ).
cnf(s508,plain,
spl169_40,
inference(rat,[],[s25,s187]) ).
cnf(s509,plain,
~ spl169_34,
inference(rat,[],[s189,s508]) ).
cnf(s510,plain,
spl169_205,
inference(rat,[],[s154,s509]) ).
cnf(s511,plain,
spl169_204,
inference(rat,[],[s153,s509]) ).
cnf(s512,plain,
spl169_203,
inference(rat,[],[s152,s509]) ).
cnf(s513,plain,
spl169_202,
inference(rat,[],[s151,s509]) ).
cnf(s514,plain,
spl169_201,
inference(rat,[],[s150,s509]) ).
cnf(s515,plain,
spl169_200,
inference(rat,[],[s149,s509]) ).
cnf(s516,plain,
spl169_199,
inference(rat,[],[s148,s509]) ).
cnf(s517,plain,
spl169_198,
inference(rat,[],[s147,s509]) ).
cnf(s518,plain,
spl169_197,
inference(rat,[],[s146,s509]) ).
cnf(s519,plain,
spl169_196,
inference(rat,[],[s145,s509]) ).
cnf(s520,plain,
spl169_195,
inference(rat,[],[s144,s509]) ).
cnf(s521,plain,
spl169_194,
inference(rat,[],[s143,s509]) ).
cnf(s522,plain,
spl169_38,
inference(rat,[],[s24,s187]) ).
cnf(s523,plain,
~ spl169_37,
inference(rat,[],[s188,s522]) ).
cnf(s524,plain,
spl169_216,
inference(rat,[],[s163,s523]) ).
cnf(s526,plain,
( spl169_350
| spl169_289 ),
inference(rat,[],[s451,s489,s513,s524,s507,s512,s506]) ).
cnf(s527,plain,
( spl169_385
| spl169_386
| spl169_289 ),
inference(rat,[],[s498,s426,s439,s511,s510,s505,s524,s506,s507]) ).
cnf(s528,plain,
( spl169_291
| spl169_289 ),
inference(rat,[],[s452,s493,s515,s507,s524,s514,s506]) ).
cnf(s529,plain,
( spl169_385
| spl169_289 ),
inference(rat,[],[s528,s477,s527]) ).
cnf(s530,plain,
spl169_289,
inference(rat,[],[s529,s483,s526]) ).
cnf(s531,plain,
~ spl169_296,
inference(rat,[],[s363,s504,s530]) ).
cnf(s532,plain,
spl169_350,
inference(rat,[],[s358,s357,s314,s368,s506,s507,s524,s503,s519,s531,s530,s518]) ).
cnf(s533,plain,
~ spl169_385,
inference(rat,[],[s483,s532]) ).
cnf(s534,plain,
spl169_359,
inference(rat,[],[s358,s357,s327,s367,s506,s507,s524,s503,s517,s531,s530,s516]) ).
cnf(s536,plain,
~ spl169_291,
inference(rat,[],[s387,s533,s505,s534]) ).
cnf(s538,plain,
spl169_374,
inference(rat,[],[s383,s530,s531,s520,s503,s536]) ).
cnf(s540,plain,
spl169_295,
inference(rat,[],[s242,s531,s530,s521,s503,s536]) ).
cnf(s541,plain,
spl169_379,
inference(rat,[],[s357,s524,s507,s538]) ).
cnf(s542,plain,
$false,
inference(rat,[],[s358,s524,s507,s506,s541,s540]) ).
thf(f8928,plain,
$false,
inference(avatar_sat_refutation,[],[s542]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG253^2 : TPTP v9.3.1. Bugfixed v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n026.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 17:35:27 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running higher-order theorem proving
% 0.21/0.27 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.72/0.41 % (920557)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.72/0.41 % (920567)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=4208937171:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.72/0.41 % (920568)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.72/0.41 % (920568)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.72/0.41 % (920564)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3837469904:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.72/0.41 % (920563)lrs+10_16_si=on:nwc=1.5:random_seed=2801498348:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.72/0.41 % (920562)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3882382068:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.72/0.41 % (920566)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2067574307:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.72/0.41 % (920565)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=3086605577:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.72/0.41 % (920568)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=3698471981:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.72/0.41 % (920564)Instruction limit reached!
% 0.72/0.41 % (920564)------------------------------
% 0.72/0.41 % (920564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.41 % (920564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.41 % (920564)CaDiCaL version: 2.1.3
% 0.72/0.41 % (920564)Termination reason: Instruction limit
% 0.72/0.41 % (920564)Termination phase: shuffling
% 0.72/0.41 % (920564)Time elapsed: 0.003 s
% 0.72/0.41 % (920564)Peak memory usage: 10 MB
% 0.72/0.41 % (920564)Instructions burned: 5 (million)
% 0.72/0.41 % (920563)Instruction limit reached!
% 0.72/0.41 % (920563)------------------------------
% 0.72/0.41 % (920563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.41 % (920563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.41 % (920563)CaDiCaL version: 2.1.3
% 0.72/0.41 % (920563)Termination reason: Instruction limit
% 0.72/0.41 % (920563)Termination phase: shuffling
% 0.72/0.41 % (920563)Time elapsed: 0.009 s
% 0.72/0.41 % (920563)Peak memory usage: 10 MB
% 0.72/0.41 % (920563)Instructions burned: 20 (million)
% 0.72/0.41 % (920566)Instruction limit reached!
% 0.72/0.41 % (920566)------------------------------
% 0.72/0.41 % (920566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.41 % (920566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.41 % (920566)CaDiCaL version: 2.1.3
% 0.72/0.41 % (920566)Termination reason: Instruction limit
% 0.72/0.41 % (920566)Termination phase: Naming
% 0.72/0.41 % (920566)Time elapsed: 0.012 s
% 0.72/0.41 % (920566)Peak memory usage: 11 MB
% 0.72/0.41 % (920566)Instructions burned: 25 (million)
% 0.72/0.41 % (920567)Instruction limit reached!
% 0.72/0.41 % (920567)------------------------------
% 0.72/0.41 % (920567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.41 % (920567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.41 % (920567)CaDiCaL version: 2.1.3
% 0.72/0.41 % (920567)Termination reason: Instruction limit
% 0.72/0.41 % (920567)Termination phase: Property scanning
% 0.72/0.41 % (920567)Time elapsed: 0.020 s
% 0.72/0.41 % (920567)Peak memory usage: 12 MB
% 0.72/0.41 % (920567)Instructions burned: 80 (million)
% 0.72/0.41 % (920578)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.72/0.41 % (920576)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3897245006:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.72/0.41 % (920578)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=959995455:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.72/0.45 % (920576)Instruction limit reached!
% 0.72/0.45 % (920576)------------------------------
% 0.72/0.45 % (920576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.45 % (920576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.45 % (920576)CaDiCaL version: 2.1.3
% 0.72/0.45 % (920576)Termination reason: Instruction limit
% 0.72/0.45 % (920576)Termination phase: shuffling
% 0.72/0.45 % (920576)Time elapsed: 0.002 s
% 0.72/0.45 % (920576)Peak memory usage: 10 MB
% 0.72/0.45 % (920576)Instructions burned: 3 (million)
% 0.72/0.45 % (920578)Instruction limit reached!
% 0.72/0.45 % (920578)------------------------------
% 0.72/0.45 % (920578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.45 % (920578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.45 % (920578)CaDiCaL version: 2.1.3
% 0.72/0.45 % (920578)Termination reason: Instruction limit
% 0.72/0.45 % (920578)Termination phase: shuffling
% 0.72/0.45 % (920578)Time elapsed: 0.002 s
% 0.72/0.45 % (920578)Peak memory usage: 10 MB
% 0.72/0.45 % (920578)Instructions burned: 11 (million)
% 0.72/0.45 % (920577)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2992081330:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.72/0.45 % (920577)Instruction limit reached!
% 0.72/0.45 % (920577)------------------------------
% 0.72/0.45 % (920577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.45 % (920577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.45 % (920577)CaDiCaL version: 2.1.3
% 0.72/0.45 % (920577)Termination reason: Instruction limit
% 0.72/0.45 % (920577)Termination phase: shuffling
% 0.72/0.45 % (920577)Time elapsed: 0.003 s
% 0.72/0.45 % (920577)Peak memory usage: 10 MB
% 0.72/0.45 % (920577)Instructions burned: 6 (million)
% 0.72/0.45 % (920579)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=646589392:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.72/0.45 % (920583)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=3950598447:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.72/0.45 % (920579)Instruction limit reached!
% 0.72/0.45 % (920579)------------------------------
% 0.72/0.45 % (920579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.45 % (920579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.45 % (920579)CaDiCaL version: 2.1.3
% 0.72/0.45 % (920579)Termination reason: Instruction limit
% 0.72/0.45 % (920579)Termination phase: shuffling
% 0.72/0.45 % (920579)Time elapsed: 0.006 s
% 0.72/0.45 % (920579)Peak memory usage: 10 MB
% 0.72/0.45 % (920579)Instructions burned: 14 (million)
% 0.72/0.45 % (920582)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.72/0.45 % (920582)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.72/0.45 % (920582)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3777186240:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.72/0.45 % (920586)lrs+10_1_si=on:cs=on:random_seed=3462238387:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.72/0.45 % (920586)Instruction limit reached!
% 0.72/0.45 % (920586)------------------------------
% 0.72/0.45 % (920586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.45 % (920586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.45 % (920586)CaDiCaL version: 2.1.3
% 0.72/0.45 % (920586)Termination reason: Instruction limit
% 0.72/0.45 % (920586)Termination phase: shuffling
% 0.72/0.45 % (920586)Time elapsed: 0.004 s
% 0.72/0.45 % (920586)Peak memory usage: 10 MB
% 0.72/0.45 % (920586)Instructions burned: 9 (million)
% 0.72/0.45 % (920582)Instruction limit reached!
% 0.72/0.45 % (920582)------------------------------
% 0.72/0.45 % (920582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (920582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.47 % (920582)CaDiCaL version: 2.1.3
% 0.72/0.47 % (920582)Termination reason: Instruction limit
% 0.72/0.47 % (920582)Termination phase: Property scanning
% 0.72/0.47 % (920582)Time elapsed: 0.012 s
% 0.72/0.47 % (920582)Peak memory usage: 10 MB
% 0.72/0.47 % (920582)Instructions burned: 28 (million)
% 0.72/0.47 % (920588)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.72/0.47 % (920568)Instruction limit reached!
% 0.72/0.47 % (920568)------------------------------
% 0.72/0.47 % (920568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (920568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.47 % (920568)CaDiCaL version: 2.1.3
% 0.72/0.47 % (920568)Termination reason: Instruction limit
% 0.72/0.47 % (920568)Termination phase: Saturation
% 0.72/0.47 % (920568)Time elapsed: 0.067 s
% 0.72/0.47 % (920568)Peak memory usage: 14 MB
% 0.72/0.47 % (920568)Instructions burned: 159 (million)
% 0.72/0.47 % (920583)Instruction limit reached!
% 0.72/0.47 % (920583)------------------------------
% 0.72/0.47 % (920583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (920583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.47 % (920588)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=2502693297:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.72/0.47 % (920583)CaDiCaL version: 2.1.3
% 0.72/0.47 % (920583)Termination reason: Instruction limit
% 0.72/0.47 % (920583)Termination phase: Saturation
% 0.72/0.47 % (920583)Time elapsed: 0.032 s
% 0.72/0.47 % (920583)Peak memory usage: 12 MB
% 0.72/0.47 % (920583)Instructions burned: 90 (million)
% 0.72/0.47 % (920588)Instruction limit reached!
% 0.72/0.47 % (920588)------------------------------
% 0.72/0.47 % (920588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (920588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.47 % (920588)CaDiCaL version: 2.1.3
% 0.72/0.47 % (920588)Termination reason: Instruction limit
% 0.72/0.47 % (920588)Termination phase: shuffling
% 0.72/0.47 % (920588)Time elapsed: 0.003 s
% 0.72/0.47 % (920588)Peak memory usage: 10 MB
% 0.72/0.47 % (920588)Instructions burned: 3 (million)
% 0.72/0.47 % (920562)Instruction limit reached!
% 0.72/0.47 % (920562)------------------------------
% 0.72/0.47 % (920562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (920562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.47 % (920562)CaDiCaL version: 2.1.3
% 0.72/0.47 % (920562)Termination reason: Instruction limit
% 0.72/0.47 % (920562)Termination phase: Function definition elimination
% 0.72/0.47 % (920562)Time elapsed: 0.074 s
% 0.72/0.47 % (920562)Peak memory usage: 12 MB
% 0.72/0.47 % (920591)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=298473545:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 0.72/0.47 % (920562)Instructions burned: 89 (million)
% 0.72/0.47 % (920592)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2375255216:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 0.72/0.47 % (920595)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=365160093:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 0.72/0.47 % (920595)Instruction limit reached!
% 0.72/0.47 % (920595)------------------------------
% 0.72/0.47 % (920595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (920595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.47 % (920595)CaDiCaL version: 2.1.3
% 0.72/0.47 % (920595)Termination reason: Instruction limit
% 0.72/0.47 % (920595)Termination phase: shuffling
% 0.72/0.47 % (920595)Time elapsed: 0.004 s
% 0.72/0.47 % (920595)Peak memory usage: 10 MB
% 0.72/0.47 % (920595)Instructions burned: 18 (million)
% 0.72/0.47 % (920591)Refutation not found, incomplete strategy
% 0.72/0.47 % (920591)------------------------------
% 0.72/0.47 % (920591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.47 % (920591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.52 % (920591)CaDiCaL version: 2.1.3
% 1.52/0.52 % (920591)Termination reason: Refutation not found, incomplete strategy
% 1.52/0.52 % (920591)Time elapsed: 0.012 s
% 1.52/0.52 % (920591)Peak memory usage: 12 MB
% 1.52/0.52 % (920591)Instructions burned: 25 (million)
% 1.52/0.52 % (920591)------------------------------
% 1.52/0.52 % (920591)------------------------------
% 1.52/0.52 % (920599)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1825563181:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.52/0.52 % (920597)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3654083434:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.52/0.52 % (920601)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=897632289:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.52/0.52 % (920593)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3382267930:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.52/0.52 % (920601)Instruction limit reached!
% 1.52/0.52 % (920601)------------------------------
% 1.52/0.52 % (920601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.52 % (920601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.52 % (920601)CaDiCaL version: 2.1.3
% 1.52/0.52 % (920601)Termination reason: Instruction limit
% 1.52/0.52 % (920601)Termination phase: shuffling
% 1.52/0.52 % (920601)Time elapsed: 0.002 s
% 1.52/0.52 % (920601)Peak memory usage: 10 MB
% 1.52/0.52 % (920601)Instructions burned: 9 (million)
% 1.52/0.52 % (920599)Instruction limit reached!
% 1.52/0.52 % (920599)------------------------------
% 1.52/0.52 % (920599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.52 % (920599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.52 % (920599)CaDiCaL version: 2.1.3
% 1.52/0.52 % (920599)Termination reason: Instruction limit
% 1.52/0.52 % (920599)Termination phase: shuffling
% 1.52/0.52 % (920599)Time elapsed: 0.007 s
% 1.52/0.52 % (920599)Peak memory usage: 10 MB
% 1.52/0.52 % (920599)Instructions burned: 16 (million)
% 1.52/0.52 % (920592)Refutation not found, incomplete strategy
% 1.52/0.52 % (920592)------------------------------
% 1.52/0.52 % (920592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.52 % (920592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.52 % (920592)CaDiCaL version: 2.1.3
% 1.52/0.52 % (920592)Termination reason: Refutation not found, incomplete strategy
% 1.52/0.52 % (920592)Time elapsed: 0.031 s
% 1.52/0.52 % (920592)Peak memory usage: 12 MB
% 1.52/0.52 % (920592)Instructions burned: 50 (million)
% 1.52/0.52 % (920602)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3321402255:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.52/0.52 % (920592)------------------------------
% 1.52/0.52 % (920592)------------------------------
% 1.52/0.52 % (920607)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=1456742826:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.52/0.52 % (920593)Instruction limit reached!
% 1.52/0.52 % (920593)------------------------------
% 1.52/0.52 % (920593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.52 % (920593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.52 % (920593)CaDiCaL version: 2.1.3
% 1.52/0.52 % (920593)Termination reason: Instruction limit
% 1.52/0.52 % (920593)Termination phase: Naming
% 1.52/0.52 % (920593)Time elapsed: 0.012 s
% 1.52/0.52 % (920593)Peak memory usage: 11 MB
% 1.52/0.52 % (920593)Instructions burned: 27 (million)
% 1.52/0.52 % (920607)Instruction limit reached!
% 1.52/0.52 % (920607)------------------------------
% 1.52/0.52 % (920607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.52 % (920607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.52 % (920607)CaDiCaL version: 2.1.3
% 1.52/0.52 % (920607)Termination reason: Instruction limit
% 1.52/0.52 % (920607)Termination phase: Property scanning
% 1.52/0.52 % (920607)Time elapsed: 0.005 s
% 1.52/0.52 % (920607)Peak memory usage: 10 MB
% 1.52/0.52 % (920607)Instructions burned: 24 (million)
% 1.52/0.52 % (920602)Instruction limit reached!
% 1.52/0.58 % (920602)------------------------------
% 1.52/0.58 % (920602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.58 % (920602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.58 % (920602)CaDiCaL version: 2.1.3
% 1.52/0.58 % (920602)Termination reason: Instruction limit
% 1.52/0.58 % (920602)Termination phase: Property scanning
% 1.52/0.58 % (920602)Time elapsed: 0.011 s
% 1.52/0.58 % (920602)Peak memory usage: 10 MB
% 1.52/0.58 % (920602)Instructions burned: 27 (million)
% 1.52/0.58 % (920608)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3185843254:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.52/0.58 % (920611)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
% 1.52/0.58 % (920611)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.52/0.58 % (920613)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=1232495864:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.52/0.58 % (920612)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.52/0.58 % (920611)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=3488610602:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.52/0.58 % (920612)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=1272910921:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.52/0.58 % (920613)Instruction limit reached!
% 1.52/0.58 % (920613)------------------------------
% 1.52/0.58 % (920613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.58 % (920613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.58 % (920613)CaDiCaL version: 2.1.3
% 1.52/0.58 % (920613)Termination reason: Instruction limit
% 1.52/0.58 % (920613)Termination phase: Property scanning
% 1.52/0.58 % (920613)Time elapsed: 0.007 s
% 1.52/0.58 % (920613)Peak memory usage: 10 MB
% 1.52/0.58 % (920613)Instructions burned: 34 (million)
% 1.52/0.58 % (920612)Instruction limit reached!
% 1.52/0.58 % (920612)------------------------------
% 1.52/0.58 % (920612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.58 % (920612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.58 % (920612)CaDiCaL version: 2.1.3
% 1.52/0.58 % (920612)Termination reason: Instruction limit
% 1.52/0.58 % (920612)Termination phase: shuffling
% 1.52/0.58 % (920612)Time elapsed: 0.004 s
% 1.52/0.58 % (920612)Peak memory usage: 10 MB
% 1.52/0.58 % (920612)Instructions burned: 9 (million)
% 1.52/0.58 % (920611)Instruction limit reached!
% 1.52/0.58 % (920611)------------------------------
% 1.52/0.58 % (920611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.58 % (920611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.58 % (920611)CaDiCaL version: 2.1.3
% 1.52/0.58 % (920611)Termination reason: Instruction limit
% 1.52/0.58 % (920611)Termination phase: shuffling
% 1.52/0.58 % (920611)Time elapsed: 0.009 s
% 1.52/0.58 % (920611)Peak memory usage: 10 MB
% 1.52/0.58 % (920611)Instructions burned: 20 (million)
% 1.52/0.58 % (920614)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=4145126409:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.52/0.58 % (920614)Instruction limit reached!
% 1.52/0.58 % (920614)------------------------------
% 1.52/0.58 % (920614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.58 % (920614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.58 % (920614)CaDiCaL version: 2.1.3
% 1.52/0.58 % (920614)Termination reason: Instruction limit
% 1.52/0.58 % (920614)Termination phase: shuffling
% 1.52/0.58 % (920614)Time elapsed: 0.003 s
% 1.52/0.58 % (920614)Peak memory usage: 10 MB
% 1.52/0.58 % (920614)Instructions burned: 7 (million)
% 1.52/0.58 % (920619)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=2793832510:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.11/0.65 % (920619)Instruction limit reached!
% 2.11/0.65 % (920619)------------------------------
% 2.11/0.65 % (920619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.65 % (920619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.65 % (920619)CaDiCaL version: 2.1.3
% 2.11/0.65 % (920619)Termination reason: Instruction limit
% 2.11/0.65 % (920619)Termination phase: Property scanning
% 2.11/0.65 % (920619)Time elapsed: 0.006 s
% 2.11/0.65 % (920619)Peak memory usage: 10 MB
% 2.11/0.65 % (920619)Instructions burned: 27 (million)
% 2.11/0.65 % (920620)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=4114638317:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.11/0.65 % (920621)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=1005280134:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.11/0.65 % (920625)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2684523008:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.11/0.65 % (920623)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3636145901:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.11/0.65 % (920620)Instruction limit reached!
% 2.11/0.65 % (920620)------------------------------
% 2.11/0.65 % (920620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.65 % (920620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.65 % (920620)CaDiCaL version: 2.1.3
% 2.11/0.65 % (920620)Termination reason: Instruction limit
% 2.11/0.65 % (920620)Termination phase: Property scanning
% 2.11/0.65 % (920620)Time elapsed: 0.010 s
% 2.11/0.65 % (920620)Peak memory usage: 10 MB
% 2.11/0.65 % (920620)Instructions burned: 21 (million)
% 2.11/0.65 % (920608)Instruction limit reached!
% 2.11/0.65 % (920608)------------------------------
% 2.11/0.65 % (920608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.65 % (920608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.65 % (920608)CaDiCaL version: 2.1.3
% 2.11/0.65 % (920608)Termination reason: Instruction limit
% 2.11/0.65 % (920608)Termination phase: Property scanning
% 2.11/0.65 % (920608)Time elapsed: 0.045 s
% 2.11/0.65 % (920608)Peak memory usage: 12 MB
% 2.11/0.65 % (920608)Instructions burned: 60 (million)
% 2.11/0.65 % (920625)Refutation not found, incomplete strategy
% 2.11/0.65 % (920625)------------------------------
% 2.11/0.65 % (920625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.65 % (920625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.65 % (920625)CaDiCaL version: 2.1.3
% 2.11/0.65 % (920625)Termination reason: Refutation not found, incomplete strategy
% 2.11/0.65 % (920625)Time elapsed: 0.014 s
% 2.11/0.65 % (920625)Peak memory usage: 13 MB
% 2.11/0.65 % (920625)Instructions burned: 60 (million)
% 2.11/0.65 % (920625)------------------------------
% 2.11/0.65 % (920625)------------------------------
% 2.11/0.65 % (920631)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.11/0.65 % (920631)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1118431309:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.11/0.65 % (920632)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=624205783:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.11/0.65 % (920631)Instruction limit reached!
% 2.11/0.65 % (920631)------------------------------
% 2.11/0.65 % (920631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.65 % (920631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.65 % (920631)CaDiCaL version: 2.1.3
% 2.11/0.65 % (920631)Termination reason: Instruction limit
% 2.11/0.65 % (920631)Termination phase: shuffling
% 2.11/0.65 % (920631)Time elapsed: 0.004 s
% 2.11/0.65 % (920631)Peak memory usage: 10 MB
% 2.11/0.65 % (920631)Instructions burned: 9 (million)
% 2.11/0.65 % (920630)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2868656888:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.55/0.73 % (920632)Refutation not found, incomplete strategy
% 2.55/0.73 % (920632)------------------------------
% 2.55/0.73 % (920632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.73 % (920632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.73 % (920632)CaDiCaL version: 2.1.3
% 2.55/0.73 % (920632)Termination reason: Refutation not found, incomplete strategy
% 2.55/0.73 % (920632)Time elapsed: 0.011 s
% 2.55/0.73 % (920632)Peak memory usage: 13 MB
% 2.55/0.73 % (920632)Instructions burned: 47 (million)
% 2.55/0.73 % (920632)------------------------------
% 2.55/0.73 % (920632)------------------------------
% 2.55/0.73 % (920637)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.55/0.73 % (920637)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=1409717107:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.55/0.73 % (920635)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=624347944:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.55/0.73 % (920637)Instruction limit reached!
% 2.55/0.73 % (920637)------------------------------
% 2.55/0.73 % (920637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.73 % (920637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.73 % (920637)CaDiCaL version: 2.1.3
% 2.55/0.73 % (920637)Termination reason: Instruction limit
% 2.55/0.73 % (920637)Termination phase: shuffling
% 2.55/0.73 % (920637)Time elapsed: 0.002 s
% 2.55/0.73 % (920637)Peak memory usage: 10 MB
% 2.55/0.73 % (920637)Instructions burned: 8 (million)
% 2.55/0.73 % (920623)Instruction limit reached!
% 2.55/0.73 % (920623)------------------------------
% 2.55/0.73 % (920623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.73 % (920623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.73 % (920623)CaDiCaL version: 2.1.3
% 2.55/0.73 % (920623)Termination reason: Instruction limit
% 2.55/0.73 % (920623)Termination phase: Saturation
% 2.55/0.73 % (920623)Time elapsed: 0.061 s
% 2.55/0.73 % (920623)Peak memory usage: 13 MB
% 2.55/0.73 % (920623)Instructions burned: 144 (million)
% 2.55/0.73 % (920640)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=2367479219:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.55/0.73 % (920630)Instruction limit reached!
% 2.55/0.73 % (920630)------------------------------
% 2.55/0.73 % (920630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.73 % (920630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.73 % (920630)CaDiCaL version: 2.1.3
% 2.55/0.73 % (920630)Termination reason: Instruction limit
% 2.55/0.73 % (920630)Termination phase: Property scanning
% 2.55/0.73 % (920630)Time elapsed: 0.035 s
% 2.55/0.73 % (920630)Peak memory usage: 11 MB
% 2.55/0.73 % (920630)Instructions burned: 43 (million)
% 2.55/0.73 % (920640)Instruction limit reached!
% 2.55/0.73 % (920640)------------------------------
% 2.55/0.73 % (920640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.73 % (920640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.73 % (920640)CaDiCaL version: 2.1.3
% 2.55/0.73 % (920640)Termination reason: Instruction limit
% 2.55/0.73 % (920640)Termination phase: Property scanning
% 2.55/0.73 % (920640)Time elapsed: 0.007 s
% 2.55/0.73 % (920640)Peak memory usage: 10 MB
% 2.55/0.73 % (920640)Instructions burned: 23 (million)
% 2.55/0.73 % (920641)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=2126774030:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.55/0.73 % (920643)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=3849267575:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.55/0.73 % (920641)Instruction limit reached!
% 2.55/0.73 % (920641)------------------------------
% 2.55/0.73 % (920641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.73 % (920641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.79 % (920641)CaDiCaL version: 2.1.3
% 2.55/0.79 % (920641)Termination reason: Instruction limit
% 2.55/0.79 % (920641)Termination phase: shuffling
% 2.55/0.79 % (920641)Time elapsed: 0.009 s
% 2.55/0.79 % (920641)Peak memory usage: 10 MB
% 2.55/0.79 % (920641)Instructions burned: 20 (million)
% 2.55/0.79 % (920597)Instruction limit reached!
% 2.55/0.79 % (920597)------------------------------
% 2.55/0.79 % (920597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.79 % (920597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.79 % (920597)CaDiCaL version: 2.1.3
% 2.55/0.79 % (920597)Termination reason: Instruction limit
% 2.55/0.79 % (920597)Termination phase: Saturation
% 2.55/0.79 % (920597)Time elapsed: 0.170 s
% 2.55/0.79 % (920597)Peak memory usage: 15 MB
% 2.55/0.79 % (920597)Instructions burned: 328 (million)
% 2.55/0.79 % (920644)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=3042935654:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2997 on theBenchmark for (2997ds/853Mi)
% 2.55/0.79 % (920647)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=1182326210:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2997 on theBenchmark for (2997ds/45Mi)
% 2.55/0.79 % (920647)Instruction limit reached!
% 2.55/0.79 % (920647)------------------------------
% 2.55/0.79 % (920647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.79 % (920647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.79 % (920647)CaDiCaL version: 2.1.3
% 2.55/0.79 % (920647)Termination reason: Instruction limit
% 2.55/0.79 % (920647)Termination phase: Preprocessing 3
% 2.55/0.79 % (920647)Time elapsed: 0.022 s
% 2.55/0.79 % (920647)Peak memory usage: 11 MB
% 2.55/0.79 % (920647)Instructions burned: 47 (million)
% 2.55/0.79 % (920648)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=560238780:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 2.55/0.79 % (920635)Instruction limit reached!
% 2.55/0.79 % (920635)------------------------------
% 2.55/0.79 % (920635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.79 % (920635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.79 % (920635)CaDiCaL version: 2.1.3
% 2.55/0.79 % (920635)Termination reason: Instruction limit
% 2.55/0.79 % (920635)Termination phase: Saturation
% 2.55/0.79 % (920635)Time elapsed: 0.091 s
% 2.55/0.79 % (920635)Peak memory usage: 13 MB
% 2.55/0.79 % (920635)Instructions burned: 170 (million)
% 2.55/0.79 % (920651)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=2801364790:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 2.55/0.79 % (920653)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 2.55/0.79 % (920643)Instruction limit reached!
% 2.55/0.79 % (920643)------------------------------
% 2.55/0.79 % (920643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.79 % (920643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.79 % (920643)CaDiCaL version: 2.1.3
% 2.55/0.79 % (920643)Termination reason: Instruction limit
% 2.55/0.79 % (920643)Termination phase: Saturation
% 2.55/0.79 % (920643)Time elapsed: 0.078 s
% 2.55/0.79 % (920643)Peak memory usage: 14 MB
% 2.55/0.79 % (920643)Instructions burned: 317 (million)
% 2.55/0.79 % (920565)Instruction limit reached!
% 2.55/0.79 % (920565)------------------------------
% 2.55/0.79 % (920565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.79 % (920565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.79 % (920565)CaDiCaL version: 2.1.3
% 2.55/0.79 % (920565)Termination reason: Instruction limit
% 2.55/0.79 % (920565)Termination phase: Saturation
% 2.55/0.79 % (920565)Time elapsed: 0.321 s
% 2.55/0.79 % (920565)Peak memory usage: 18 MB
% 2.55/0.79 % (920565)Instructions burned: 635 (million)
% 2.55/0.79 % (920653)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=3965782407:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 2.55/0.79 % (920651)Instruction limit reached!
% 3.67/0.92 % (920651)------------------------------
% 3.67/0.92 % (920651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.67/0.92 % (920651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/0.92 % (920651)CaDiCaL version: 2.1.3
% 3.67/0.92 % (920651)Termination reason: Instruction limit
% 3.67/0.92 % (920651)Termination phase: Property scanning
% 3.67/0.92 % (920651)Time elapsed: 0.010 s
% 3.67/0.92 % (920651)Peak memory usage: 10 MB
% 3.67/0.92 % (920651)Instructions burned: 23 (million)
% 3.67/0.92 % (920655)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=4232085990:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.67/0.92 % (920655)Instruction limit reached!
% 3.67/0.92 % (920655)------------------------------
% 3.67/0.92 % (920655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.67/0.92 % (920655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/0.92 % (920655)CaDiCaL version: 2.1.3
% 3.67/0.92 % (920655)Termination reason: Instruction limit
% 3.67/0.92 % (920655)Termination phase: shuffling
% 3.67/0.92 % (920655)Time elapsed: 0.004 s
% 3.67/0.92 % (920655)Peak memory usage: 10 MB
% 3.67/0.92 % (920655)Instructions burned: 17 (million)
% 3.67/0.92 % (920656)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=2460591247:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 3.67/0.92 % (920658)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=4206080299:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 3.67/0.92 % (920660)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3756708576:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/31Mi)
% 3.67/0.92 % (920660)Instruction limit reached!
% 3.67/0.92 % (920660)------------------------------
% 3.67/0.92 % (920660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.67/0.92 % (920660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/0.92 % (920660)CaDiCaL version: 2.1.3
% 3.67/0.92 % (920660)Termination reason: Instruction limit
% 3.67/0.92 % (920660)Termination phase: Property scanning
% 3.67/0.92 % (920660)Time elapsed: 0.009 s
% 3.67/0.92 % (920660)Peak memory usage: 10 MB
% 3.67/0.92 % (920660)Instructions burned: 35 (million)
% 3.67/0.92 % (920658)Instruction limit reached!
% 3.67/0.92 % (920658)------------------------------
% 3.67/0.92 % (920658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.67/0.92 % (920658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/0.92 % (920658)CaDiCaL version: 2.1.3
% 3.67/0.92 % (920658)Termination reason: Instruction limit
% 3.67/0.92 % (920658)Termination phase: Property scanning
% 3.67/0.92 % (920658)Time elapsed: 0.022 s
% 3.67/0.92 % (920658)Peak memory usage: 10 MB
% 3.67/0.92 % (920658)Instructions burned: 53 (million)
% 3.67/0.92 % (920664)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3208857815:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 3.67/0.92 % (920656)Instruction limit reached!
% 3.67/0.92 % (920656)------------------------------
% 3.67/0.92 % (920656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.67/0.92 % (920656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/0.92 % (920656)CaDiCaL version: 2.1.3
% 3.67/0.92 % (920656)Termination reason: Instruction limit
% 3.67/0.92 % (920656)Termination phase: Property scanning
% 3.67/0.92 % (920656)Time elapsed: 0.029 s
% 3.67/0.92 % (920656)Peak memory usage: 11 MB
% 3.67/0.92 % (920656)Instructions burned: 67 (million)
% 3.67/0.92 % (920665)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=2862843043:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.67/0.92 % (920667)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=1458875091:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 3.67/0.92 % (920665)Instruction limit reached!
% 3.67/0.92 % (920665)------------------------------
% 3.67/0.92 % (920665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.67/0.92 % (920665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.04 % (920665)CaDiCaL version: 2.1.3
% 3.67/1.04 % (920665)Termination reason: Instruction limit
% 3.67/1.04 % (920665)Termination phase: Property scanning
% 3.67/1.04 % (920665)Time elapsed: 0.015 s
% 3.67/1.04 % (920665)Peak memory usage: 10 MB
% 3.67/1.04 % (920665)Instructions burned: 35 (million)
% 3.67/1.04 % (920653)Instruction limit reached!
% 3.67/1.04 % (920653)------------------------------
% 3.67/1.04 % (920653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.67/1.04 % (920653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.04 % (920653)CaDiCaL version: 2.1.3
% 3.67/1.04 % (920653)Termination reason: Instruction limit
% 3.67/1.04 % (920653)Termination phase: Saturation
% 3.67/1.04 % (920653)Time elapsed: 0.087 s
% 3.67/1.04 % (920653)Peak memory usage: 14 MB
% 3.67/1.04 % (920653)Instructions burned: 200 (million)
% 3.67/1.04 % (920670)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 3.67/1.04 % (920667)Instruction limit reached!
% 3.67/1.04 % (920667)------------------------------
% 3.67/1.04 % (920667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.67/1.04 % (920667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.04 % (920667)CaDiCaL version: 2.1.3
% 3.67/1.04 % (920667)Termination reason: Instruction limit
% 3.67/1.04 % (920667)Termination phase: Property scanning
% 3.67/1.04 % (920667)Time elapsed: 0.028 s
% 3.67/1.04 % (920667)Peak memory usage: 11 MB
% 3.67/1.04 % (920667)Instructions burned: 69 (million)
% 3.67/1.04 % (920664)Instruction limit reached!
% 3.67/1.04 % (920664)------------------------------
% 3.67/1.04 % (920664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.67/1.04 % (920664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.04 % (920664)CaDiCaL version: 2.1.3
% 3.67/1.04 % (920664)Termination reason: Instruction limit
% 3.67/1.04 % (920664)Termination phase: Saturation
% 3.67/1.04 % (920664)Time elapsed: 0.052 s
% 3.67/1.04 % (920664)Peak memory usage: 13 MB
% 3.67/1.04 % (920664)Instructions burned: 140 (million)
% 3.67/1.04 % (920670)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=3136294477:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 3.67/1.04 % (920673)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=1204175439:i=427:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/427Mi)
% 3.67/1.04 % (920671)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=2735906720:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 3.67/1.04 % (920648)Refutation not found, incomplete strategy
% 3.67/1.04 % (920648)------------------------------
% 3.67/1.04 % (920648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.67/1.04 % (920648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.04 % (920648)CaDiCaL version: 2.1.3
% 3.67/1.04 % (920648)Termination reason: Refutation not found, incomplete strategy
% 3.67/1.04 % (920648)Time elapsed: 0.139 s
% 3.67/1.04 % (920648)Peak memory usage: 15 MB
% 3.67/1.04 % (920648)Instructions burned: 156 (million)
% 3.67/1.04 % (920648)------------------------------
% 3.67/1.04 % (920648)------------------------------
% 3.67/1.04 % (920672)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=1843509778:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 3.67/1.04 % (920673)Refutation not found, incomplete strategy
% 3.67/1.04 % (920673)------------------------------
% 3.67/1.04 % (920673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.67/1.04 % (920673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.67/1.04 % (920673)CaDiCaL version: 2.1.3
% 3.67/1.04 % (920673)Termination reason: Refutation not found, incomplete strategy
% 3.67/1.04 % (920673)Time elapsed: 0.011 s
% 3.67/1.04 % (920673)Peak memory usage: 12 MB
% 3.67/1.04 % (920673)Instructions burned: 47 (million)
% 3.67/1.04 % (920673)------------------------------
% 3.67/1.04 % (920673)------------------------------
% 3.67/1.04 % (920679)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=1360445534:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/515Mi)
% 3.67/1.04 % (920678)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1278525150:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/874Mi)
% 5.27/1.11 % (920672)Instruction limit reached!
% 5.27/1.11 % (920672)------------------------------
% 5.27/1.11 % (920672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.27/1.11 % (920672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.27/1.11 % (920672)CaDiCaL version: 2.1.3
% 5.27/1.11 % (920672)Termination reason: Instruction limit
% 5.27/1.11 % (920672)Termination phase: Saturation
% 5.27/1.11 % (920672)Time elapsed: 0.041 s
% 5.27/1.11 % (920672)Peak memory usage: 12 MB
% 5.27/1.11 % (920672)Instructions burned: 98 (million)
% 5.27/1.11 % (920682)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3042642758:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 5.27/1.11 % (920670)Instruction limit reached!
% 5.27/1.11 % (920670)------------------------------
% 5.27/1.11 % (920670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.27/1.11 % (920670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.27/1.11 % (920670)CaDiCaL version: 2.1.3
% 5.27/1.11 % (920670)Termination reason: Instruction limit
% 5.27/1.11 % (920670)Termination phase: Saturation
% 5.27/1.11 % (920670)Time elapsed: 0.081 s
% 5.27/1.11 % (920670)Peak memory usage: 13 MB
% 5.27/1.11 % (920670)Instructions burned: 181 (million)
% 5.27/1.11 % (920684)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=351696238:i=44:ep=R:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/44Mi)
% 5.27/1.11 % (920671)Instruction limit reached!
% 5.27/1.11 % (920671)------------------------------
% 5.27/1.11 % (920671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.27/1.11 % (920671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.27/1.11 % (920671)CaDiCaL version: 2.1.3
% 5.27/1.11 % (920671)Termination reason: Instruction limit
% 5.27/1.11 % (920671)Termination phase: Saturation
% 5.27/1.11 % (920671)Time elapsed: 0.099 s
% 5.27/1.11 % (920671)Peak memory usage: 13 MB
% 5.27/1.11 % (920671)Instructions burned: 247 (million)
% 5.27/1.11 % (920684)Instruction limit reached!
% 5.27/1.11 % (920684)------------------------------
% 5.27/1.11 % (920684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.27/1.11 % (920684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.27/1.11 % (920684)CaDiCaL version: 2.1.3
% 5.27/1.11 % (920684)Termination reason: Instruction limit
% 5.27/1.11 % (920684)Termination phase: Property scanning
% 5.27/1.11 % (920684)Time elapsed: 0.019 s
% 5.27/1.11 % (920684)Peak memory usage: 10 MB
% 5.27/1.11 % (920684)Instructions burned: 46 (million)
% 5.27/1.11 % (920686)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=3097580307:s2a=on:i=571:nm=16:rtra=on_2994 on theBenchmark for (2994ds/571Mi)
% 5.27/1.11 % (920687)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=2509122569:i=450:rtra=on:ixr=off:ntd=on_2994 on theBenchmark for (2994ds/450Mi)
% 5.27/1.11 % (920682)Instruction limit reached!
% 5.27/1.11 % (920682)------------------------------
% 5.27/1.11 % (920682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.27/1.11 % (920682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.27/1.11 % (920682)CaDiCaL version: 2.1.3
% 5.27/1.11 % (920682)Termination reason: Instruction limit
% 5.27/1.11 % (920682)Termination phase: Saturation
% 5.27/1.11 % (920682)Time elapsed: 0.063 s
% 5.27/1.11 % (920682)Peak memory usage: 14 MB
% 5.27/1.11 % (920682)Instructions burned: 130 (million)
% 5.27/1.11 % (920679)Instruction limit reached!
% 5.27/1.11 % (920679)------------------------------
% 5.27/1.11 % (920679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.27/1.11 % (920679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.27/1.11 % (920679)CaDiCaL version: 2.1.3
% 5.27/1.11 % (920679)Termination reason: Instruction limit
% 5.27/1.11 % (920679)Termination phase: Saturation
% 5.27/1.11 % (920679)Time elapsed: 0.124 s
% 5.27/1.11 % (920679)Peak memory usage: 17 MB
% 5.27/1.11 % (920679)Instructions burned: 517 (million)
% 5.27/1.11 % (920690)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=89914473:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/95Mi)
% 5.27/1.11 % (920691)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=3119521040:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2993 on theBenchmark for (2993ds/65Mi)
% 5.87/1.18 % (920691)Instruction limit reached!
% 5.87/1.18 % (920691)------------------------------
% 5.87/1.18 % (920691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.87/1.18 % (920691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.18 % (920691)CaDiCaL version: 2.1.3
% 5.87/1.18 % (920691)Termination reason: Instruction limit
% 5.87/1.18 % (920691)Termination phase: Function definition elimination
% 5.87/1.18 % (920691)Time elapsed: 0.014 s
% 5.87/1.18 % (920691)Peak memory usage: 11 MB
% 5.87/1.18 % (920691)Instructions burned: 68 (million)
% 5.87/1.18 % (920694)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=285123867: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_2993 on theBenchmark for (2993ds/105Mi)
% 5.87/1.18 % (920690)Instruction limit reached!
% 5.87/1.18 % (920690)------------------------------
% 5.87/1.18 % (920690)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.87/1.18 % (920690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.18 % (920690)CaDiCaL version: 2.1.3
% 5.87/1.18 % (920690)Termination reason: Instruction limit
% 5.87/1.18 % (920690)Termination phase: Saturation
% 5.87/1.18 % (920690)Time elapsed: 0.040 s
% 5.87/1.18 % (920690)Peak memory usage: 12 MB
% 5.87/1.18 % (920690)Instructions burned: 95 (million)
% 5.87/1.18 % (920694)Instruction limit reached!
% 5.87/1.18 % (920694)------------------------------
% 5.87/1.18 % (920694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.87/1.18 % (920694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.18 % (920694)CaDiCaL version: 2.1.3
% 5.87/1.18 % (920694)Termination reason: Instruction limit
% 5.87/1.18 % (920694)Termination phase: Saturation
% 5.87/1.18 % (920694)Time elapsed: 0.024 s
% 5.87/1.18 % (920694)Peak memory usage: 12 MB
% 5.87/1.18 % (920694)Instructions burned: 110 (million)
% 5.87/1.18 % (920696)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=3215186566:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2993 on theBenchmark for (2993ds/5755Mi)
% 5.87/1.18 % (920686)Refutation not found, incomplete strategy
% 5.87/1.18 % (920686)------------------------------
% 5.87/1.18 % (920686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.87/1.18 % (920686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.18 % (920686)CaDiCaL version: 2.1.3
% 5.87/1.18 % (920686)Termination reason: Refutation not found, incomplete strategy
% 5.87/1.18 % (920686)Time elapsed: 0.094 s
% 5.87/1.18 % (920686)Peak memory usage: 15 MB
% 5.87/1.18 % (920686)Instructions burned: 190 (million)
% 5.87/1.18 % (920686)------------------------------
% 5.87/1.18 % (920686)------------------------------
% 5.87/1.18 % (920697)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=3064115386:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/375Mi)
% 5.87/1.18 % (920696)Refutation not found, incomplete strategy
% 5.87/1.18 % (920696)------------------------------
% 5.87/1.18 % (920696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.87/1.18 % (920696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.18 % (920696)CaDiCaL version: 2.1.3
% 5.87/1.18 % (920696)Termination reason: Refutation not found, incomplete strategy
% 5.87/1.18 % (920696)Time elapsed: 0.013 s
% 5.87/1.18 % (920696)Peak memory usage: 13 MB
% 5.87/1.18 % (920696)Instructions burned: 27 (million)
% 5.87/1.18 % (920696)------------------------------
% 5.87/1.18 % (920696)------------------------------
% 5.87/1.18 % (920700)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3087365085:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2993 on theBenchmark for (2993ds/495Mi)
% 5.87/1.18 % (920701)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=3462146739:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 5.87/1.18 % (920644)Instruction limit reached!
% 5.87/1.18 % (920644)------------------------------
% 5.87/1.18 % (920644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.23/1.22 % (920644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.22 % (920644)CaDiCaL version: 2.1.3
% 6.23/1.22 % (920644)Termination reason: Instruction limit
% 6.23/1.22 % (920644)Termination phase: Saturation
% 6.23/1.22 % (920644)Time elapsed: 0.438 s
% 6.23/1.22 % (920644)Peak memory usage: 20 MB
% 6.23/1.22 % (920644)Instructions burned: 855 (million)
% 6.23/1.22 % (920701)Instruction limit reached!
% 6.23/1.22 % (920701)------------------------------
% 6.23/1.22 % (920701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.23/1.22 % (920701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.22 % (920701)CaDiCaL version: 2.1.3
% 6.23/1.22 % (920701)Termination reason: Instruction limit
% 6.23/1.22 % (920701)Termination phase: Property scanning
% 6.23/1.22 % (920701)Time elapsed: 0.031 s
% 6.23/1.22 % (920701)Peak memory usage: 10 MB
% 6.23/1.22 % (920701)Instructions burned: 35 (million)
% 6.23/1.22 % (920704)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=1260076687:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/91Mi)
% 6.23/1.22 % (920705)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=1629562880:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2992 on theBenchmark for (2992ds/66Mi)
% 6.23/1.22 % (920705)Refutation not found, incomplete strategy
% 6.23/1.22 % (920705)------------------------------
% 6.23/1.22 % (920705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.23/1.22 % (920705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.22 % (920705)CaDiCaL version: 2.1.3
% 6.23/1.22 % (920705)Termination reason: Refutation not found, incomplete strategy
% 6.23/1.22 % (920705)Time elapsed: 0.012 s
% 6.23/1.22 % (920705)Peak memory usage: 13 MB
% 6.23/1.22 % (920705)Instructions burned: 25 (million)
% 6.23/1.22 % (920705)------------------------------
% 6.23/1.22 % (920705)------------------------------
% 6.23/1.22 % (920697)Instruction limit reached!
% 6.23/1.22 % (920697)------------------------------
% 6.23/1.22 % (920697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.23/1.22 % (920697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.22 % (920697)CaDiCaL version: 2.1.3
% 6.23/1.22 % (920697)Termination reason: Instruction limit
% 6.23/1.22 % (920697)Termination phase: Saturation
% 6.23/1.22 % (920697)Time elapsed: 0.107 s
% 6.23/1.22 % (920697)Peak memory usage: 14 MB
% 6.23/1.22 % (920697)Instructions burned: 375 (million)
% 6.23/1.22 % (920704)Instruction limit reached!
% 6.23/1.22 % (920704)------------------------------
% 6.23/1.22 % (920704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.23/1.22 % (920704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.22 % (920704)CaDiCaL version: 2.1.3
% 6.23/1.22 % (920704)Termination reason: Instruction limit
% 6.23/1.22 % (920704)Termination phase: Saturation
% 6.23/1.22 % (920704)Time elapsed: 0.038 s
% 6.23/1.22 % (920704)Peak memory usage: 12 MB
% 6.23/1.22 % (920704)Instructions burned: 92 (million)
% 6.23/1.22 % (920709)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=2276082004:i=338:bd=all:ins=4:rtra=on_2991 on theBenchmark for (2991ds/338Mi)
% 6.23/1.22 % (920708)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=385156301:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2991 on theBenchmark for (2991ds/22Mi)
% 6.23/1.22 % (920687)Instruction limit reached!
% 6.23/1.22 % (920687)------------------------------
% 6.23/1.22 % (920687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.23/1.22 % (920687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.22 % (920687)CaDiCaL version: 2.1.3
% 6.23/1.22 % (920687)Termination reason: Instruction limit
% 6.23/1.22 % (920687)Termination phase: Saturation
% 6.23/1.22 % (920687)Time elapsed: 0.214 s
% 6.23/1.22 % (920687)Peak memory usage: 18 MB
% 6.23/1.22 % (920687)Instructions burned: 451 (million)
% 6.23/1.22 % (920708)Instruction limit reached!
% 6.23/1.22 % (920708)------------------------------
% 6.23/1.22 % (920708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.23/1.22 % (920708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.22 % (920708)CaDiCaL version: 2.1.3
% 6.23/1.22 % (920708)Termination reason: Instruction limit
% 6.23/1.22 % (920708)Termination phase: Property scanning
% 6.23/1.22 % (920708)Time elapsed: 0.010 s
% 6.23/1.22 % (920708)Peak memory usage: 10 MB
% 6.23/1.22 % (920708)Instructions burned: 24 (million)
% 6.23/1.22 % (920621)Instruction limit reached!
% 6.23/1.22 % (920621)------------------------------
% 6.23/1.22 % (920621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.23/1.22 % (920621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.22 % (920621)CaDiCaL version: 2.1.3
% 6.23/1.22 % (920621)Termination reason: Instruction limit
% 6.23/1.22 % (920621)Termination phase: Saturation
% 6.23/1.22 % (920621)Time elapsed: 0.629 s
% 6.23/1.22 % (920621)Peak memory usage: 20 MB
% 6.23/1.22 % (920621)Instructions burned: 1241 (million)
% 6.23/1.22 % (920710)lrs+10_1_sil=128000:si=on:urr=on:random_seed=3077866090:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/28Mi)
% 6.23/1.22 % (920713)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 6.23/1.22 % (920713)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=2626109430:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2991 on theBenchmark for (2991ds/137Mi)
% 6.23/1.22 % (920710)Instruction limit reached!
% 6.23/1.22 % (920710)------------------------------
% 6.23/1.22 % (920710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.23/1.22 % (920710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.22 % (920710)CaDiCaL version: 2.1.3
% 6.23/1.22 % (920710)Termination reason: Instruction limit
% 6.23/1.22 % (920710)Termination phase: Property scanning
% 6.23/1.22 % (920710)Time elapsed: 0.013 s
% 6.23/1.22 % (920710)Peak memory usage: 10 MB
% 6.23/1.22 % (920710)Instructions burned: 30 (million)
% 6.23/1.22 % (920715)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=3551973478:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2991 on theBenchmark for (2991ds/340Mi)
% 6.23/1.22 % (920718)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 6.23/1.22 % (920716)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=1139381771:i=227:sd=1:bd=all:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/227Mi)
% 6.23/1.22 % (920718)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=3113753268:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/373Mi)
% 6.23/1.22 % (920709)Instruction limit reached!
% 6.23/1.22 % (920709)------------------------------
% 6.23/1.22 % (920709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.23/1.22 % (920709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.22 % (920709)CaDiCaL version: 2.1.3
% 6.23/1.22 % (920709)Termination reason: Instruction limit
% 6.23/1.22 % (920709)Termination phase: Saturation
% 6.23/1.22 % (920709)Time elapsed: 0.079 s
% 6.23/1.22 % (920709)Peak memory usage: 15 MB
% 6.23/1.22 % (920709)Instructions burned: 340 (million)
% 6.23/1.22 % (920713)Instruction limit reached!
% 6.23/1.22 % (920713)------------------------------
% 6.23/1.22 % (920713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.23/1.22 % (920713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.22 % (920713)CaDiCaL version: 2.1.3
% 6.23/1.22 % (920713)Termination reason: Instruction limit
% 6.23/1.22 % (920713)Termination phase: Saturation
% 6.23/1.22 % (920713)Time elapsed: 0.056 s
% 6.23/1.22 % (920713)Peak memory usage: 12 MB
% 6.23/1.22 % (920713)Instructions burned: 138 (million)
% 6.23/1.22 % (920716)Refutation not found, incomplete strategy
% 6.23/1.22 % (920716)------------------------------
% 6.23/1.22 % (920716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.23/1.22 % (920716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.22 % (920716)CaDiCaL version: 2.1.3
% 6.23/1.22 % (920716)Termination reason: Refutation not found, incomplete strategy
% 6.23/1.22 % (920716)Time elapsed: 0.038 s
% 6.23/1.22 % (920716)Peak memory usage: 13 MB
% 6.23/1.22 % (920716)Instructions burned: 47 (million)
% 6.23/1.22 % (920716)------------------------------
% 6.23/1.22 % (920716)------------------------------
% 6.23/1.22 % (920724)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=3516679766:i=116:ep=RSTC:rtra=on:ntd=on_2991 on theBenchmark for (2991ds/116Mi)
% 6.23/1.22 % (920678) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-920557-920678"...
% 6.23/1.22 % (920724)Instruction limit reached!
% 6.23/1.22 % (920724)------------------------------
% 6.23/1.22 % (920724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.23/1.22 % (920724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.22 % (920724)CaDiCaL version: 2.1.3
% 6.23/1.22 % (920724)Termination reason: Instruction limit
% 6.23/1.22 % (920724)Termination phase: Property scanning
% 6.23/1.22 % (920724)Time elapsed: 0.027 s
% 6.23/1.22 % (920724)Peak memory usage: 12 MB
% 6.23/1.22 % (920724)Instructions burned: 120 (million)
% 6.23/1.22 % (920725)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=1058066618:i=575:rtra=on_2991 on theBenchmark for (2991ds/575Mi)
% 6.23/1.22 % (920678)...printing done.
% 6.23/1.22 % (920678)Refutation found. Thanks to Tanya!
% 6.23/1.22 % SZS status Theorem for theBenchmark
% 6.23/1.22 % SZS output start Proof for theBenchmark
% See solution above
% 6.23/1.22 % (920678)------------------------------
% 6.23/1.22 % (920678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.23/1.22 % (920678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.23/1.22 % (920678)CaDiCaL version: 2.1.3
% 6.23/1.22 % (920678)Termination reason: Refutation
% 6.23/1.22 % (920678)Time elapsed: 0.425 s
% 6.23/1.22 % (920678)Peak memory usage: 19 MB
% 6.23/1.22 % (920678)Instructions burned: 816 (million)
% 6.23/1.22 % (920557)Success in time 0.936 s
% 6.23/1.22 % Vampire exiting
%------------------------------------------------------------------------------