%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : COM301_1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:40:02 AM UTC 2026
% Result : Theorem 106.92s 16.09s
% Output : Refutation 108.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 26
% Syntax : Number of formulae : 148 ( 35 unt; 0 typ; 9 def)
% Number of atoms : 425 ( 193 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 448 ( 171 ~; 156 |; 104 &)
% ( 7 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 21 ( 20 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 104 ( 102 usr; 8 prp; 0-3 aty)
% Number of functors : 629 ( 629 usr; 24 con; 0-5 aty)
% Number of variables : 278 ( 0 sgn 200 !; 78 ?; 278 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
vRow: $tType ).
tff(type_def_6,type,
vPred: $tType ).
tff(type_def_7,type,
vName: $tType ).
tff(type_def_8,type,
vAttrL: $tType ).
tff(type_def_9,type,
vRawTable: $tType ).
tff(type_def_10,type,
vOptRawTable: $tType ).
tff(type_def_11,type,
vFType: $tType ).
tff(type_def_12,type,
vOptTType: $tType ).
tff(type_def_13,type,
vTTContext: $tType ).
tff(type_def_14,type,
vQuery: $tType ).
tff(type_def_15,type,
vVal: $tType ).
tff(type_def_16,type,
vOptTable: $tType ).
tff(type_def_17,type,
vTStore: $tType ).
tff(type_def_18,type,
vExp: $tType ).
tff(type_def_19,type,
vTable: $tType ).
tff(type_def_20,type,
vTType: $tType ).
tff(type_def_21,type,
vSelect: $tType ).
tff(type_def_22,type,
vOptFType: $tType ).
tff(type_def_23,type,
vOptVal: $tType ).
tff(type_def_24,type,
vOptQuery: $tType ).
tff(func_def_0,type,
vrempty: vRow ).
tff(func_def_1,type,
vconstant: vVal > vExp ).
tff(func_def_2,type,
vlookup: vName > vExp ).
tff(func_def_3,type,
vtvalue: vTable > vQuery ).
tff(func_def_4,type,
vacons: ( vName * vAttrL ) > vAttrL ).
tff(func_def_5,type,
vsomeQuery: vQuery > vOptQuery ).
tff(func_def_6,type,
vsomeFType: vFType > vOptFType ).
tff(func_def_7,type,
vall: vSelect ).
tff(func_def_8,type,
vrcons: ( vVal * vRow ) > vRow ).
tff(func_def_9,type,
vttcons: ( vName * vFType * vTType ) > vTType ).
tff(func_def_10,type,
vtempty: vRawTable ).
tff(func_def_11,type,
vselectFromWhere: ( vSelect * vName * vPred ) > vQuery ).
tff(func_def_12,type,
vaempty: vAttrL ).
tff(func_def_13,type,
vnoRawTable: vOptRawTable ).
tff(func_def_14,type,
vtcons: ( vRow * vRawTable ) > vRawTable ).
tff(func_def_15,type,
vsomeTType: vTType > vOptTType ).
tff(func_def_16,type,
vsomeVal: vVal > vOptVal ).
tff(func_def_17,type,
vIntersection: ( vQuery * vQuery ) > vQuery ).
tff(func_def_18,type,
vptrue: vPred ).
tff(func_def_19,type,
vsomeRawTable: vRawTable > vOptRawTable ).
tff(func_def_20,type,
vbindStore: ( vName * vTable * vTStore ) > vTStore ).
tff(func_def_21,type,
vnoQuery: vOptQuery ).
tff(func_def_22,type,
val1: vAttrL ).
tff(func_def_23,type,
vnot: vPred > vPred ).
tff(func_def_24,type,
vnoVal: vOptVal ).
tff(func_def_25,type,
vnoTType: vOptTType ).
tff(func_def_26,type,
vttempty: vTType ).
tff(func_def_27,type,
vnoTable: vOptTable ).
tff(func_def_28,type,
vDifference: ( vQuery * vQuery ) > vQuery ).
tff(func_def_29,type,
vnoFType: vOptFType ).
tff(func_def_30,type,
vUnion: ( vQuery * vQuery ) > vQuery ).
tff(func_def_31,type,
vbindContext: ( vName * vTType * vTTContext ) > vTTContext ).
tff(func_def_32,type,
vlt: ( vExp * vExp ) > vPred ).
tff(func_def_33,type,
vemptyContext: vTTContext ).
tff(func_def_34,type,
vgt: ( vExp * vExp ) > vPred ).
tff(func_def_35,type,
vsomeTable: vTable > vOptTable ).
tff(func_def_36,type,
vemptyStore: vTStore ).
tff(func_def_37,type,
veq: ( vExp * vExp ) > vPred ).
tff(func_def_38,type,
vand: ( vPred * vPred ) > vPred ).
tff(func_def_39,type,
vlist: vAttrL > vSelect ).
tff(func_def_40,type,
vtable: ( vAttrL * vRawTable ) > vTable ).
tff(func_def_41,type,
vprojectTable: ( vSelect * vTable ) > vOptTable ).
tff(func_def_42,type,
vinitFType: vFType ).
tff(func_def_43,type,
vprojectTypeAttrL: ( vAttrL * vTType ) > vOptTType ).
tff(func_def_44,type,
venumVal: vVal > vVal ).
tff(func_def_45,type,
vinitVal: vVal ).
tff(func_def_46,type,
vgetRaw: vTable > vRawTable ).
tff(func_def_47,type,
vprojectFirstRaw: vRawTable > vRawTable ).
tff(func_def_48,type,
vlookupStore: ( vName * vTStore ) > vOptTable ).
tff(func_def_49,type,
vrawUnion: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_50,type,
venumFType: vFType > vFType ).
tff(func_def_51,type,
vattachColToFrontRaw: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_52,type,
vprojectEmptyCol: vRawTable > vRawTable ).
tff(func_def_53,type,
vfilterTable: ( vTable * vPred ) > vTable ).
tff(func_def_54,type,
venumName: vName > vName ).
tff(func_def_55,type,
vgetAttrL: vTable > vAttrL ).
tff(func_def_56,type,
vevalExpRow: ( vExp * vAttrL * vRow ) > vOptVal ).
tff(func_def_57,type,
vfindCol: ( vName * vAttrL * vRawTable ) > vOptRawTable ).
tff(func_def_58,type,
vlookupContext: ( vName * vTTContext ) > vOptTType ).
tff(func_def_59,type,
vreduce: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_60,type,
vfieldType: vVal > vFType ).
tff(func_def_61,type,
vrawIntersection: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_62,type,
vtypeOfExp: ( vExp * vTType ) > vOptFType ).
tff(func_def_63,type,
vdropFirstColRaw: vRawTable > vRawTable ).
tff(func_def_64,type,
vfindColType: ( vName * vTType ) > vOptFType ).
tff(func_def_65,type,
vinitName: vName ).
tff(func_def_66,type,
vfilterRows: ( vRawTable * vAttrL * vPred ) > vRawTable ).
tff(func_def_67,type,
vprojectType: ( vSelect * vTType ) > vOptTType ).
tff(func_def_68,type,
vprojectCols: ( vAttrL * vAttrL * vRawTable ) > vOptRawTable ).
tff(func_def_69,type,
vrawDifference: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_70,type,
vappend: ( vAttrL * vAttrL ) > vAttrL ).
tff(func_def_71,type,
vgetFType: vOptFType > vFType ).
tff(func_def_72,type,
vgetQuery: vOptQuery > vQuery ).
tff(func_def_73,type,
vgetTType: vOptTType > vTType ).
tff(func_def_74,type,
vgetVal: vOptVal > vVal ).
tff(func_def_75,type,
vgetTable: vOptTable > vTable ).
tff(func_def_76,type,
vgetRawTable: vOptRawTable > vRawTable ).
tff(func_def_77,type,
sK76: vSelect > vAttrL ).
tff(func_def_78,type,
sK77: vQuery > vTable ).
tff(func_def_79,type,
sK78: vQuery > vSelect ).
tff(func_def_80,type,
sK79: vQuery > vName ).
tff(func_def_81,type,
sK80: vQuery > vPred ).
tff(func_def_82,type,
sK81: vQuery > vQuery ).
tff(func_def_83,type,
sK82: vQuery > vQuery ).
tff(func_def_84,type,
sK83: vQuery > vQuery ).
tff(func_def_85,type,
sK84: vQuery > vQuery ).
tff(func_def_86,type,
sK85: vQuery > vQuery ).
tff(func_def_87,type,
sK86: vQuery > vQuery ).
tff(func_def_88,type,
sK87: vOptTable > vTable ).
tff(func_def_89,type,
sK88: vTType > vName ).
tff(func_def_90,type,
sK89: vTType > vFType ).
tff(func_def_91,type,
sK90: vTType > vTType ).
tff(func_def_92,type,
sK91: vTTContext > vName ).
tff(func_def_93,type,
sK92: vTTContext > vTType ).
tff(func_def_94,type,
sK93: vTTContext > vTTContext ).
tff(func_def_95,type,
sK94: vOptRawTable > vRawTable ).
tff(func_def_96,type,
sK95: vOptTType > vTType ).
tff(func_def_97,type,
sK96: vRow > vVal ).
tff(func_def_98,type,
sK97: vRow > vRow ).
tff(func_def_99,type,
sK98: vRawTable > vRow ).
tff(func_def_100,type,
sK99: vRawTable > vRawTable ).
tff(func_def_101,type,
sK100: vOptQuery > vQuery ).
tff(func_def_102,type,
sK101: vExp > vVal ).
tff(func_def_103,type,
sK102: vExp > vName ).
tff(func_def_104,type,
sK103: vTable > vAttrL ).
tff(func_def_105,type,
sK104: vTable > vRawTable ).
tff(func_def_106,type,
sK105: vOptVal > vVal ).
tff(func_def_107,type,
sK106: vPred > vPred ).
tff(func_def_108,type,
sK107: vPred > vPred ).
tff(func_def_109,type,
sK108: vPred > vPred ).
tff(func_def_110,type,
sK109: vPred > vExp ).
tff(func_def_111,type,
sK110: vPred > vExp ).
tff(func_def_112,type,
sK111: vPred > vExp ).
tff(func_def_113,type,
sK112: vPred > vExp ).
tff(func_def_114,type,
sK113: vPred > vExp ).
tff(func_def_115,type,
sK114: vPred > vExp ).
tff(func_def_116,type,
sK115: vTStore > vName ).
tff(func_def_117,type,
sK116: vTStore > vTable ).
tff(func_def_118,type,
sK117: vTStore > vTStore ).
tff(func_def_119,type,
sK118: vOptFType > vFType ).
tff(func_def_120,type,
sK119: vAttrL > vName ).
tff(func_def_121,type,
sK120: vAttrL > vAttrL ).
tff(func_def_122,type,
sK121: ( vAttrL * vAttrL ) > vName ).
tff(func_def_123,type,
sK122: ( vAttrL * vAttrL ) > vAttrL ).
tff(func_def_124,type,
sK123: ( vAttrL * vAttrL ) > vAttrL ).
tff(func_def_125,type,
sK124: ( vAttrL * vAttrL ) > vAttrL ).
tff(func_def_126,type,
sK125: vTable > vAttrL ).
tff(func_def_127,type,
sK126: vTable > vRawTable ).
tff(func_def_128,type,
sK127: vTable > vAttrL ).
tff(func_def_129,type,
sK128: vTable > vRawTable ).
tff(func_def_130,type,
sK129: vTType > vName ).
tff(func_def_131,type,
sK130: vTType > vFType ).
tff(func_def_132,type,
sK131: vTType > vTType ).
tff(func_def_133,type,
sK132: vAttrL > vName ).
tff(func_def_134,type,
sK133: vAttrL > vAttrL ).
tff(func_def_135,type,
sK134: ( vTType * vAttrL ) > vTType ).
tff(func_def_136,type,
sK135: ( vTType * vAttrL ) > vName ).
tff(func_def_137,type,
sK136: ( vTType * vAttrL ) > vFType ).
tff(func_def_138,type,
sK137: ( vTType * vAttrL ) > vName ).
tff(func_def_139,type,
sK138: ( vTType * vAttrL ) > vAttrL ).
tff(func_def_140,type,
sK139: ( vTType * vAttrL ) > vTType ).
tff(func_def_141,type,
sK140: ( vTType * vAttrL ) > vAttrL ).
tff(func_def_142,type,
sK141: ( vTType * vAttrL ) > vTType ).
tff(func_def_143,type,
sK142: ( vTType * vAttrL ) > vName ).
tff(func_def_144,type,
sK143: ( vTType * vAttrL ) > vFType ).
tff(func_def_145,type,
sK144: ( vTType * vAttrL ) > vName ).
tff(func_def_146,type,
sK145: ( vTType * vAttrL ) > vAttrL ).
tff(func_def_147,type,
sK146: vTType > vName ).
tff(func_def_148,type,
sK147: vTType > vFType ).
tff(func_def_149,type,
sK148: vTType > vTType ).
tff(func_def_150,type,
sK149: vRow > vVal ).
tff(func_def_151,type,
sK150: vRow > vRow ).
tff(func_def_152,type,
sK151: ( vTType * vRow ) > vVal ).
tff(func_def_153,type,
sK152: ( vTType * vRow ) > vTType ).
tff(func_def_154,type,
sK153: ( vTType * vRow ) > vFType ).
tff(func_def_155,type,
sK154: ( vTType * vRow ) > vName ).
tff(func_def_156,type,
sK155: ( vTType * vRow ) > vRow ).
tff(func_def_157,type,
sK156: ( vTType * vRow ) > vTType ).
tff(func_def_158,type,
sK157: ( vTType * vRow ) > vRow ).
tff(func_def_159,type,
sK158: ( vTType * vRow ) > vVal ).
tff(func_def_160,type,
sK159: ( vTType * vRow ) > vTType ).
tff(func_def_161,type,
sK160: ( vTType * vRow ) > vFType ).
tff(func_def_162,type,
sK161: ( vTType * vRow ) > vName ).
tff(func_def_163,type,
sK162: ( vTType * vRow ) > vRow ).
tff(func_def_164,type,
sK163: ( vTType * vRawTable ) > vTType ).
tff(func_def_165,type,
sK164: ( vTType * vRawTable ) > vRow ).
tff(func_def_166,type,
sK165: ( vTType * vRawTable ) > vRawTable ).
tff(func_def_167,type,
sK166: ( vTType * vRawTable ) > vTType ).
tff(func_def_168,type,
sK167: ( vTType * vRawTable ) > vRow ).
tff(func_def_169,type,
sK168: ( vTType * vRawTable ) > vRawTable ).
tff(func_def_170,type,
sK169: ( vTType * vRawTable ) > vTType ).
tff(func_def_171,type,
sK170: ( vTType * vTable ) > vTType ).
tff(func_def_172,type,
sK171: ( vTType * vTable ) > vAttrL ).
tff(func_def_173,type,
sK172: ( vTType * vTable ) > vRawTable ).
tff(func_def_174,type,
sK173: ( vTType * vTable ) > vTType ).
tff(func_def_175,type,
sK174: ( vTType * vTable ) > vAttrL ).
tff(func_def_176,type,
sK175: ( vTType * vTable ) > vRawTable ).
tff(func_def_177,type,
sK176: ( vRow * vRawTable ) > vRow ).
tff(func_def_178,type,
sK177: ( vRow * vRawTable ) > vRawTable ).
tff(func_def_179,type,
sK178: ( vRow * vRawTable ) > vRow ).
tff(func_def_180,type,
sK179: ( vRow * vRawTable ) > vRow ).
tff(func_def_181,type,
sK180: ( vRow * vRawTable ) > vRow ).
tff(func_def_182,type,
sK181: ( vRow * vRawTable ) > vRawTable ).
tff(func_def_183,type,
sK182: ( vRow * vRawTable ) > vRow ).
tff(func_def_184,type,
sK183: vRawTable > vRawTable ).
tff(func_def_185,type,
sK184: vRawTable > vVal ).
tff(func_def_186,type,
sK185: vRawTable > vRow ).
tff(func_def_187,type,
sK186: vRawTable > vRawTable ).
tff(func_def_188,type,
sK187: vRawTable > vRawTable ).
tff(func_def_189,type,
sK188: vRawTable > vVal ).
tff(func_def_190,type,
sK189: vRawTable > vRow ).
tff(func_def_191,type,
sK190: vRawTable > vRawTable ).
tff(func_def_192,type,
sK191: vOptRawTable > vRawTable ).
tff(func_def_193,type,
sK192: vRawTable > vRow ).
tff(func_def_194,type,
sK193: vRawTable > vRawTable ).
tff(func_def_195,type,
sK194: vRawTable > vRow ).
tff(func_def_196,type,
sK195: vRawTable > vRawTable ).
tff(func_def_197,type,
sK196: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_198,type,
sK197: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_199,type,
sK198: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_200,type,
sK199: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_201,type,
sK200: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_202,type,
sK201: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_203,type,
sK202: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_204,type,
sK203: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_205,type,
sK204: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_206,type,
sK205: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_207,type,
sK206: vRawTable > vVal ).
tff(func_def_208,type,
sK207: vRawTable > vRawTable ).
tff(func_def_209,type,
sK208: vRawTable > vRow ).
tff(func_def_210,type,
sK209: vRawTable > vRawTable ).
tff(func_def_211,type,
sK210: ( vRawTable * vRawTable ) > vVal ).
tff(func_def_212,type,
sK211: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_213,type,
sK212: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_214,type,
sK213: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_215,type,
sK214: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_216,type,
sK215: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_217,type,
sK216: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_218,type,
sK217: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_219,type,
sK218: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_220,type,
sK219: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_221,type,
sK220: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_222,type,
sK221: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_223,type,
sK222: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_224,type,
sK223: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_225,type,
sK224: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_226,type,
sK225: ( vRow * vRawTable ) > vRow ).
tff(func_def_227,type,
sK226: ( vRow * vRawTable ) > vRow ).
tff(func_def_228,type,
sK227: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_229,type,
sK228: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_230,type,
sK229: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_231,type,
sK230: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_232,type,
sK231: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_233,type,
sK232: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_234,type,
sK233: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_235,type,
sK234: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_236,type,
sK235: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_237,type,
sK236: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_238,type,
sK237: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_239,type,
sK238: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_240,type,
sK239: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_241,type,
sK240: ( vRow * vRawTable ) > vRow ).
tff(func_def_242,type,
sK241: ( vRow * vRawTable ) > vRow ).
tff(func_def_243,type,
sK242: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_244,type,
sK243: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_245,type,
sK244: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_246,type,
sK245: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_247,type,
sK246: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_248,type,
sK247: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_249,type,
sK248: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_250,type,
sK249: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_251,type,
sK250: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_252,type,
sK251: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_253,type,
sK252: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_254,type,
sK253: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_255,type,
sK254: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_256,type,
sK255: vOptTable > vTable ).
tff(func_def_257,type,
sK256: ( vName * vTStore ) > vName ).
tff(func_def_258,type,
sK257: ( vName * vTStore ) > vTable ).
tff(func_def_259,type,
sK258: ( vName * vTStore ) > vTStore ).
tff(func_def_260,type,
sK259: ( vName * vTStore ) > vName ).
tff(func_def_261,type,
sK260: ( vName * vTStore ) > vName ).
tff(func_def_262,type,
sK261: ( vName * vTStore ) > vTable ).
tff(func_def_263,type,
sK262: ( vName * vTStore ) > vTStore ).
tff(func_def_264,type,
sK263: ( vName * vTStore ) > vName ).
tff(func_def_265,type,
sK264: ( vName * vTStore ) > vName ).
tff(func_def_266,type,
sK265: vOptTType > vTType ).
tff(func_def_267,type,
sK266: ( vName * vTTContext ) > vName ).
tff(func_def_268,type,
sK267: ( vName * vTTContext ) > vTType ).
tff(func_def_269,type,
sK268: ( vName * vTTContext ) > vTTContext ).
tff(func_def_270,type,
sK269: ( vName * vTTContext ) > vName ).
tff(func_def_271,type,
sK270: ( vName * vTTContext ) > vName ).
tff(func_def_272,type,
sK271: ( vName * vTTContext ) > vTType ).
tff(func_def_273,type,
sK272: ( vName * vTTContext ) > vTTContext ).
tff(func_def_274,type,
sK273: ( vName * vTTContext ) > vName ).
tff(func_def_275,type,
sK274: ( vName * vTTContext ) > vName ).
tff(func_def_276,type,
sK275: vQuery > vTable ).
tff(func_def_277,type,
sK276: vQuery > vSelect ).
tff(func_def_278,type,
sK277: vQuery > vName ).
tff(func_def_279,type,
sK278: vQuery > vPred ).
tff(func_def_280,type,
sK279: vQuery > vQuery ).
tff(func_def_281,type,
sK280: vQuery > vQuery ).
tff(func_def_282,type,
sK281: vQuery > vQuery ).
tff(func_def_283,type,
sK282: vQuery > vQuery ).
tff(func_def_284,type,
sK283: vQuery > vQuery ).
tff(func_def_285,type,
sK284: vQuery > vQuery ).
tff(func_def_286,type,
sK285: vOptQuery > vQuery ).
tff(func_def_287,type,
sK286: ( vName * vAttrL * vRawTable ) > vName ).
tff(func_def_288,type,
sK287: ( vName * vAttrL * vRawTable ) > vAttrL ).
tff(func_def_289,type,
sK288: ( vName * vAttrL * vRawTable ) > vName ).
tff(func_def_290,type,
sK289: ( vName * vAttrL * vRawTable ) > vRawTable ).
tff(func_def_291,type,
sK290: ( vName * vAttrL * vRawTable ) > vName ).
tff(func_def_292,type,
sK291: ( vName * vAttrL * vRawTable ) > vAttrL ).
tff(func_def_293,type,
sK292: ( vName * vAttrL * vRawTable ) > vName ).
tff(func_def_294,type,
sK293: ( vName * vAttrL * vRawTable ) > vRawTable ).
tff(func_def_295,type,
sK294: ( vName * vAttrL * vRawTable ) > vName ).
tff(func_def_296,type,
sK295: ( vName * vAttrL * vRawTable ) > vRawTable ).
tff(func_def_297,type,
sK296: vRawTable > vRow ).
tff(func_def_298,type,
sK297: vRawTable > vRawTable ).
tff(func_def_299,type,
sK298: ( vAttrL * vAttrL * vRawTable ) > vRawTable ).
tff(func_def_300,type,
sK299: ( vAttrL * vAttrL * vRawTable ) > vOptRawTable ).
tff(func_def_301,type,
sK300: ( vAttrL * vAttrL * vRawTable ) > vOptRawTable ).
tff(func_def_302,type,
sK301: ( vAttrL * vAttrL * vRawTable ) > vAttrL ).
tff(func_def_303,type,
sK302: ( vAttrL * vAttrL * vRawTable ) > vAttrL ).
tff(func_def_304,type,
sK303: ( vAttrL * vAttrL * vRawTable ) > vName ).
tff(func_def_305,type,
sK304: ( vAttrL * vAttrL * vRawTable ) > vRawTable ).
tff(func_def_306,type,
sK305: ( vAttrL * vAttrL * vRawTable ) > vOptRawTable ).
tff(func_def_307,type,
sK306: ( vAttrL * vAttrL * vRawTable ) > vOptRawTable ).
tff(func_def_308,type,
sK307: ( vAttrL * vAttrL * vRawTable ) > vAttrL ).
tff(func_def_309,type,
sK308: ( vAttrL * vAttrL * vRawTable ) > vAttrL ).
tff(func_def_310,type,
sK309: ( vAttrL * vAttrL * vRawTable ) > vName ).
tff(func_def_311,type,
sK310: ( vAttrL * vAttrL * vRawTable ) > vAttrL ).
tff(func_def_312,type,
sK311: ( vAttrL * vAttrL * vRawTable ) > vRawTable ).
tff(func_def_313,type,
sK312: ( vSelect * vTable ) > vAttrL ).
tff(func_def_314,type,
sK313: ( vSelect * vTable ) > vOptRawTable ).
tff(func_def_315,type,
sK314: ( vSelect * vTable ) > vTable ).
tff(func_def_316,type,
sK315: ( vSelect * vTable ) > vAttrL ).
tff(func_def_317,type,
sK316: ( vSelect * vTable ) > vOptRawTable ).
tff(func_def_318,type,
sK317: ( vSelect * vTable ) > vTable ).
tff(func_def_319,type,
sK318: ( vSelect * vTable ) > vTable ).
tff(func_def_320,type,
sK319: vOptVal > vVal ).
tff(func_def_321,type,
sK320: vExp > vVal ).
tff(func_def_322,type,
sK321: vExp > vName ).
tff(func_def_323,type,
sK322: vAttrL > vName ).
tff(func_def_324,type,
sK323: vAttrL > vAttrL ).
tff(func_def_325,type,
sK324: vRow > vVal ).
tff(func_def_326,type,
sK325: vRow > vRow ).
tff(func_def_327,type,
sK326: ( vExp * vAttrL * vRow ) > vVal ).
tff(func_def_328,type,
sK327: ( vExp * vAttrL * vRow ) > vName ).
tff(func_def_329,type,
sK328: ( vExp * vAttrL * vRow ) > vName ).
tff(func_def_330,type,
sK329: ( vExp * vAttrL * vRow ) > vRow ).
tff(func_def_331,type,
sK330: ( vExp * vAttrL * vRow ) > vAttrL ).
tff(func_def_332,type,
sK331: ( vExp * vAttrL * vRow ) > vVal ).
tff(func_def_333,type,
sK332: ( vExp * vAttrL * vRow ) > vName ).
tff(func_def_334,type,
sK333: ( vExp * vAttrL * vRow ) > vName ).
tff(func_def_335,type,
sK334: ( vExp * vAttrL * vRow ) > vRow ).
tff(func_def_336,type,
sK335: ( vExp * vAttrL * vRow ) > vAttrL ).
tff(func_def_337,type,
sK336: ( vExp * vAttrL * vRow ) > vExp ).
tff(func_def_338,type,
sK337: ( vExp * vAttrL * vRow ) > vAttrL ).
tff(func_def_339,type,
sK338: ( vExp * vAttrL * vRow ) > vRow ).
tff(func_def_340,type,
sK339: ( vExp * vAttrL * vRow ) > vVal ).
tff(func_def_341,type,
sK340: ( vExp * vAttrL * vRow ) > vAttrL ).
tff(func_def_342,type,
sK341: ( vExp * vAttrL * vRow ) > vRow ).
tff(func_def_343,type,
sK342: ( vPred * vAttrL * vRow ) > vPred ).
tff(func_def_344,type,
sK343: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_345,type,
sK344: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_346,type,
sK345: ( vPred * vAttrL * vRow ) > vPred ).
tff(func_def_347,type,
sK346: ( vPred * vAttrL * vRow ) > vPred ).
tff(func_def_348,type,
sK347: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_349,type,
sK348: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_350,type,
sK349: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_351,type,
sK350: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_352,type,
sK351: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_353,type,
sK352: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_354,type,
sK353: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_355,type,
sK354: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_356,type,
sK355: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_357,type,
sK356: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_358,type,
sK357: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_359,type,
sK358: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_360,type,
sK359: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_361,type,
sK360: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_362,type,
sK361: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_363,type,
sK362: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_364,type,
sK363: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_365,type,
sK364: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_366,type,
sK365: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_367,type,
sK366: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_368,type,
sK367: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_369,type,
sK368: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_370,type,
sK369: ( vPred * vAttrL * vRow ) > vPred ).
tff(func_def_371,type,
sK370: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_372,type,
sK371: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_373,type,
sK372: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_374,type,
sK373: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_375,type,
sK374: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_376,type,
sK375: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_377,type,
sK376: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_378,type,
sK377: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_379,type,
sK378: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_380,type,
sK379: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_381,type,
sK380: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_382,type,
sK381: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_383,type,
sK382: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_384,type,
sK383: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_385,type,
sK384: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_386,type,
sK385: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_387,type,
sK386: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_388,type,
sK387: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_389,type,
sK388: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_390,type,
sK389: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_391,type,
sK390: ( vPred * vAttrL * vRow ) > vPred ).
tff(func_def_392,type,
sK391: ( vPred * vAttrL * vRow ) > vPred ).
tff(func_def_393,type,
sK392: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_394,type,
sK393: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_395,type,
sK394: ( vRawTable * vAttrL * vPred ) > vPred ).
tff(func_def_396,type,
sK395: ( vRawTable * vAttrL * vPred ) > vRow ).
tff(func_def_397,type,
sK396: ( vRawTable * vAttrL * vPred ) > vRawTable ).
tff(func_def_398,type,
sK397: ( vRawTable * vAttrL * vPred ) > vAttrL ).
tff(func_def_399,type,
sK398: ( vRawTable * vAttrL * vPred ) > vRawTable ).
tff(func_def_400,type,
sK399: ( vRawTable * vAttrL * vPred ) > vPred ).
tff(func_def_401,type,
sK400: ( vRawTable * vAttrL * vPred ) > vRow ).
tff(func_def_402,type,
sK401: ( vRawTable * vAttrL * vPred ) > vRawTable ).
tff(func_def_403,type,
sK402: ( vRawTable * vAttrL * vPred ) > vAttrL ).
tff(func_def_404,type,
sK403: ( vRawTable * vAttrL * vPred ) > vRawTable ).
tff(func_def_405,type,
sK404: ( vRawTable * vAttrL * vPred ) > vAttrL ).
tff(func_def_406,type,
sK405: ( vRawTable * vAttrL * vPred ) > vPred ).
tff(func_def_407,type,
sK406: ( vTable * vPred ) > vAttrL ).
tff(func_def_408,type,
sK407: ( vTable * vPred ) > vRawTable ).
tff(func_def_409,type,
sK408: ( vTable * vPred ) > vPred ).
tff(func_def_410,type,
sK409: ( vTable * vQuery ) > vTable ).
tff(func_def_411,type,
sK410: ( vTable * vQuery ) > vTable ).
tff(func_def_412,type,
sK411: ( vTable * vQuery ) > vTable ).
tff(func_def_413,type,
sK412: ( vTable * vQuery ) > vTable ).
tff(func_def_414,type,
sK413: ( vQuery * vQuery ) > vTable ).
tff(func_def_415,type,
sK414: ( vQuery * vQuery ) > vTable ).
tff(func_def_416,type,
sK415: ( vQuery * vQuery ) > vTable ).
tff(func_def_417,type,
sK416: ( vQuery * vQuery ) > vQuery ).
tff(func_def_418,type,
sK417: ( vQuery * vQuery ) > vTable ).
tff(func_def_419,type,
sK418: ( vQuery * vQuery ) > vTable ).
tff(func_def_420,type,
sK419: ( vQuery * vQuery ) > vTable ).
tff(func_def_421,type,
sK420: ( vQuery * vQuery ) > vQuery ).
tff(func_def_422,type,
sK421: ( vTable * vQuery ) > vTable ).
tff(func_def_423,type,
sK422: ( vTable * vQuery ) > vTable ).
tff(func_def_424,type,
sK423: ( vTable * vQuery ) > vTable ).
tff(func_def_425,type,
sK424: ( vTable * vQuery ) > vTable ).
tff(func_def_426,type,
sK425: ( vQuery * vQuery ) > vTable ).
tff(func_def_427,type,
sK426: ( vQuery * vQuery ) > vTable ).
tff(func_def_428,type,
sK427: ( vQuery * vQuery ) > vTable ).
tff(func_def_429,type,
sK428: ( vQuery * vQuery ) > vQuery ).
tff(func_def_430,type,
sK429: ( vQuery * vQuery ) > vTable ).
tff(func_def_431,type,
sK430: ( vQuery * vQuery ) > vTable ).
tff(func_def_432,type,
sK431: ( vQuery * vQuery ) > vTable ).
tff(func_def_433,type,
sK432: ( vQuery * vQuery ) > vQuery ).
tff(func_def_434,type,
sK433: ( vTable * vQuery ) > vTable ).
tff(func_def_435,type,
sK434: ( vTable * vQuery ) > vTable ).
tff(func_def_436,type,
sK435: ( vTable * vQuery ) > vTable ).
tff(func_def_437,type,
sK436: ( vTable * vQuery ) > vTable ).
tff(func_def_438,type,
sK437: ( vQuery * vQuery ) > vTable ).
tff(func_def_439,type,
sK438: ( vQuery * vQuery ) > vTable ).
tff(func_def_440,type,
sK439: ( vQuery * vQuery ) > vTable ).
tff(func_def_441,type,
sK440: ( vQuery * vQuery ) > vQuery ).
tff(func_def_442,type,
sK441: ( vQuery * vQuery ) > vTable ).
tff(func_def_443,type,
sK442: ( vQuery * vQuery ) > vTable ).
tff(func_def_444,type,
sK443: ( vQuery * vQuery ) > vTable ).
tff(func_def_445,type,
sK444: ( vQuery * vQuery ) > vQuery ).
tff(func_def_446,type,
sK445: ( vQuery * vTStore ) > vTable ).
tff(func_def_447,type,
sK446: ( vQuery * vTStore ) > vTable ).
tff(func_def_448,type,
sK447: ( vQuery * vTStore ) > vTStore ).
tff(func_def_449,type,
sK448: ( vQuery * vTStore ) > vTable ).
tff(func_def_450,type,
sK449: ( vQuery * vTStore ) > vTable ).
tff(func_def_451,type,
sK450: ( vQuery * vTStore ) > vTStore ).
tff(func_def_452,type,
sK451: ( vQuery * vTStore ) > vTable ).
tff(func_def_453,type,
sK452: ( vQuery * vTStore ) > vTable ).
tff(func_def_454,type,
sK453: ( vQuery * vTStore ) > vTStore ).
tff(func_def_455,type,
sK454: ( vQuery * vTStore ) > vPred ).
tff(func_def_456,type,
sK455: ( vQuery * vTStore ) > vSelect ).
tff(func_def_457,type,
sK456: ( vQuery * vTStore ) > vOptTable ).
tff(func_def_458,type,
sK457: ( vQuery * vTStore ) > vTStore ).
tff(func_def_459,type,
sK458: ( vQuery * vTStore ) > vName ).
tff(func_def_460,type,
sK459: ( vQuery * vTStore ) > vTable ).
tff(func_def_461,type,
sK460: ( vQuery * vTStore ) > vQuery ).
tff(func_def_462,type,
sK461: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_463,type,
sK462: ( vQuery * vTStore ) > vTStore ).
tff(func_def_464,type,
sK463: ( vQuery * vTStore ) > vTable ).
tff(func_def_465,type,
sK464: ( vQuery * vTStore ) > vQuery ).
tff(func_def_466,type,
sK465: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_467,type,
sK466: ( vQuery * vTStore ) > vTStore ).
tff(func_def_468,type,
sK467: ( vQuery * vTStore ) > vTable ).
tff(func_def_469,type,
sK468: ( vQuery * vTStore ) > vQuery ).
tff(func_def_470,type,
sK469: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_471,type,
sK470: ( vQuery * vTStore ) > vTStore ).
tff(func_def_472,type,
sK471: ( vQuery * vTStore ) > vTable ).
tff(func_def_473,type,
sK472: ( vQuery * vTStore ) > vQuery ).
tff(func_def_474,type,
sK473: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_475,type,
sK474: ( vQuery * vTStore ) > vTStore ).
tff(func_def_476,type,
sK475: ( vQuery * vTStore ) > vTable ).
tff(func_def_477,type,
sK476: ( vQuery * vTStore ) > vQuery ).
tff(func_def_478,type,
sK477: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_479,type,
sK478: ( vQuery * vTStore ) > vTStore ).
tff(func_def_480,type,
sK479: ( vQuery * vTStore ) > vTable ).
tff(func_def_481,type,
sK480: ( vQuery * vTStore ) > vQuery ).
tff(func_def_482,type,
sK481: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_483,type,
sK482: ( vQuery * vTStore ) > vTStore ).
tff(func_def_484,type,
sK483: ( vQuery * vTStore ) > vQuery ).
tff(func_def_485,type,
sK484: ( vQuery * vTStore ) > vQuery ).
tff(func_def_486,type,
sK485: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_487,type,
sK486: ( vQuery * vTStore ) > vTStore ).
tff(func_def_488,type,
sK487: ( vQuery * vTStore ) > vQuery ).
tff(func_def_489,type,
sK488: ( vQuery * vTStore ) > vQuery ).
tff(func_def_490,type,
sK489: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_491,type,
sK490: ( vQuery * vTStore ) > vTStore ).
tff(func_def_492,type,
sK491: ( vQuery * vTStore ) > vQuery ).
tff(func_def_493,type,
sK492: ( vQuery * vTStore ) > vQuery ).
tff(func_def_494,type,
sK493: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_495,type,
sK494: ( vQuery * vTStore ) > vTStore ).
tff(func_def_496,type,
sK495: ( vQuery * vTStore ) > vQuery ).
tff(func_def_497,type,
sK496: ( vQuery * vTStore ) > vQuery ).
tff(func_def_498,type,
sK497: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_499,type,
sK498: ( vQuery * vTStore ) > vTStore ).
tff(func_def_500,type,
sK499: ( vQuery * vTStore ) > vQuery ).
tff(func_def_501,type,
sK500: ( vQuery * vTStore ) > vQuery ).
tff(func_def_502,type,
sK501: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_503,type,
sK502: ( vQuery * vTStore ) > vTStore ).
tff(func_def_504,type,
sK503: ( vQuery * vTStore ) > vQuery ).
tff(func_def_505,type,
sK504: ( vQuery * vTStore ) > vQuery ).
tff(func_def_506,type,
sK505: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_507,type,
sK506: ( vQuery * vTStore ) > vTStore ).
tff(func_def_508,type,
sK507: ( vQuery * vTStore ) > vPred ).
tff(func_def_509,type,
sK508: ( vQuery * vTStore ) > vTable ).
tff(func_def_510,type,
sK509: ( vQuery * vTStore ) > vSelect ).
tff(func_def_511,type,
sK510: ( vQuery * vTStore ) > vOptTable ).
tff(func_def_512,type,
sK511: ( vQuery * vTStore ) > vOptTable ).
tff(func_def_513,type,
sK512: ( vQuery * vTStore ) > vTStore ).
tff(func_def_514,type,
sK513: ( vQuery * vTStore ) > vName ).
tff(func_def_515,type,
sK514: ( vQuery * vTStore ) > vPred ).
tff(func_def_516,type,
sK515: ( vQuery * vTStore ) > vTable ).
tff(func_def_517,type,
sK516: ( vQuery * vTStore ) > vSelect ).
tff(func_def_518,type,
sK517: ( vQuery * vTStore ) > vOptTable ).
tff(func_def_519,type,
sK518: ( vQuery * vTStore ) > vOptTable ).
tff(func_def_520,type,
sK519: ( vQuery * vTStore ) > vTStore ).
tff(func_def_521,type,
sK520: ( vQuery * vTStore ) > vName ).
tff(func_def_522,type,
sK521: ( vQuery * vTStore ) > vTable ).
tff(func_def_523,type,
sK522: ( vQuery * vTStore ) > vTStore ).
tff(func_def_524,type,
sK523: vOptFType > vFType ).
tff(func_def_525,type,
sK524: ( vName * vTType ) > vName ).
tff(func_def_526,type,
sK525: ( vName * vTType ) > vFType ).
tff(func_def_527,type,
sK526: ( vName * vTType ) > vTType ).
tff(func_def_528,type,
sK527: ( vName * vTType ) > vName ).
tff(func_def_529,type,
sK528: ( vName * vTType ) > vName ).
tff(func_def_530,type,
sK529: ( vName * vTType ) > vFType ).
tff(func_def_531,type,
sK530: ( vName * vTType ) > vTType ).
tff(func_def_532,type,
sK531: ( vName * vTType ) > vName ).
tff(func_def_533,type,
sK532: ( vName * vTType ) > vName ).
tff(func_def_534,type,
sK533: ( vAttrL * vTType ) > vName ).
tff(func_def_535,type,
sK534: ( vAttrL * vTType ) > vOptFType ).
tff(func_def_536,type,
sK535: ( vAttrL * vTType ) > vTType ).
tff(func_def_537,type,
sK536: ( vAttrL * vTType ) > vAttrL ).
tff(func_def_538,type,
sK537: ( vAttrL * vTType ) > vOptTType ).
tff(func_def_539,type,
sK538: ( vAttrL * vTType ) > vName ).
tff(func_def_540,type,
sK539: ( vAttrL * vTType ) > vOptFType ).
tff(func_def_541,type,
sK540: ( vAttrL * vTType ) > vTType ).
tff(func_def_542,type,
sK541: ( vAttrL * vTType ) > vAttrL ).
tff(func_def_543,type,
sK542: ( vAttrL * vTType ) > vOptTType ).
tff(func_def_544,type,
sK543: ( vAttrL * vTType ) > vTType ).
tff(func_def_545,type,
sK544: ( vSelect * vTType ) > vAttrL ).
tff(func_def_546,type,
sK545: ( vSelect * vTType ) > vTType ).
tff(func_def_547,type,
sK546: ( vSelect * vTType ) > vTType ).
tff(func_def_548,type,
sK547: ( vExp * vTType ) > vName ).
tff(func_def_549,type,
sK548: ( vExp * vTType ) > vName ).
tff(func_def_550,type,
sK549: ( vExp * vTType ) > vName ).
tff(func_def_551,type,
sK550: ( vExp * vTType ) > vFType ).
tff(func_def_552,type,
sK551: ( vExp * vTType ) > vTType ).
tff(func_def_553,type,
sK552: ( vExp * vTType ) > vName ).
tff(func_def_554,type,
sK553: ( vExp * vTType ) > vName ).
tff(func_def_555,type,
sK554: ( vExp * vTType ) > vFType ).
tff(func_def_556,type,
sK555: ( vExp * vTType ) > vTType ).
tff(func_def_557,type,
sK556: ( vExp * vTType ) > vVal ).
tff(func_def_558,type,
sK557: ( vExp * vTType ) > vTType ).
tff(func_def_559,type,
sK558: ( vPred * vTType ) > vPred ).
tff(func_def_560,type,
sK559: ( vPred * vTType ) > vPred ).
tff(func_def_561,type,
sK560: ( vPred * vTType ) > vTType ).
tff(func_def_562,type,
sK561: ( vPred * vTType ) > vOptFType ).
tff(func_def_563,type,
sK562: ( vPred * vTType ) > vExp ).
tff(func_def_564,type,
sK563: ( vPred * vTType ) > vOptFType ).
tff(func_def_565,type,
sK564: ( vPred * vTType ) > vExp ).
tff(func_def_566,type,
sK565: ( vPred * vTType ) > vTType ).
tff(func_def_567,type,
sK566: ( vPred * vTType ) > vOptFType ).
tff(func_def_568,type,
sK567: ( vPred * vTType ) > vExp ).
tff(func_def_569,type,
sK568: ( vPred * vTType ) > vOptFType ).
tff(func_def_570,type,
sK569: ( vPred * vTType ) > vExp ).
tff(func_def_571,type,
sK570: ( vPred * vTType ) > vTType ).
tff(func_def_572,type,
sK571: ( vPred * vTType ) > vOptFType ).
tff(func_def_573,type,
sK572: ( vPred * vTType ) > vExp ).
tff(func_def_574,type,
sK573: ( vPred * vTType ) > vOptFType ).
tff(func_def_575,type,
sK574: ( vPred * vTType ) > vExp ).
tff(func_def_576,type,
sK575: ( vPred * vTType ) > vTType ).
tff(func_def_577,type,
sK576: ( vPred * vTType ) > vTType ).
tff(func_def_578,type,
sK577: ( vPred * vTType ) > vPred ).
tff(func_def_579,type,
sK578: ( vPred * vTType ) > vTType ).
tff(func_def_580,type,
sK579: ( vPred * vTType ) > vPred ).
tff(func_def_581,type,
sK580: ( vPred * vTType ) > vTType ).
tff(func_def_582,type,
sK581: ( vPred * vTType ) > vOptFType ).
tff(func_def_583,type,
sK582: ( vPred * vTType ) > vExp ).
tff(func_def_584,type,
sK583: ( vPred * vTType ) > vOptFType ).
tff(func_def_585,type,
sK584: ( vPred * vTType ) > vExp ).
tff(func_def_586,type,
sK585: ( vPred * vTType ) > vTType ).
tff(func_def_587,type,
sK586: ( vPred * vTType ) > vOptFType ).
tff(func_def_588,type,
sK587: ( vPred * vTType ) > vExp ).
tff(func_def_589,type,
sK588: ( vPred * vTType ) > vOptFType ).
tff(func_def_590,type,
sK589: ( vPred * vTType ) > vExp ).
tff(func_def_591,type,
sK590: ( vPred * vTType ) > vTType ).
tff(func_def_592,type,
sK591: ( vPred * vTType ) > vOptFType ).
tff(func_def_593,type,
sK592: ( vPred * vTType ) > vExp ).
tff(func_def_594,type,
sK593: ( vPred * vTType ) > vOptFType ).
tff(func_def_595,type,
sK594: ( vPred * vTType ) > vExp ).
tff(func_def_596,type,
sK595: ( vPred * vTType ) > vTType ).
tff(func_def_597,type,
sK596: ( vPred * vTType ) > vPred ).
tff(func_def_598,type,
sK597: ( vPred * vTType ) > vPred ).
tff(func_def_599,type,
sK598: ( vPred * vTType ) > vTType ).
tff(func_def_600,type,
sK599: vTStore > vName ).
tff(func_def_601,type,
sK600: vTStore > vTable ).
tff(func_def_602,type,
sK601: vTStore > vTStore ).
tff(func_def_603,type,
sK602: vTTContext > vName ).
tff(func_def_604,type,
sK603: vTTContext > vTType ).
tff(func_def_605,type,
sK604: vTTContext > vTTContext ).
tff(func_def_606,type,
sK605: ( vTStore * vTTContext ) > vName ).
tff(func_def_607,type,
sK606: ( vTStore * vTTContext ) > vTable ).
tff(func_def_608,type,
sK607: ( vTStore * vTTContext ) > vTTContext ).
tff(func_def_609,type,
sK608: ( vTStore * vTTContext ) > vName ).
tff(func_def_610,type,
sK609: ( vTStore * vTTContext ) > vTStore ).
tff(func_def_611,type,
sK610: ( vTStore * vTTContext ) > vTType ).
tff(func_def_612,type,
sK611: ( vTStore * vTTContext ) > vTStore ).
tff(func_def_613,type,
sK612: ( vTStore * vTTContext ) > vTTContext ).
tff(func_def_614,type,
sK613: ( vTStore * vTTContext ) > vName ).
tff(func_def_615,type,
sK614: ( vTStore * vTTContext ) > vTable ).
tff(func_def_616,type,
sK615: ( vTStore * vTTContext ) > vTTContext ).
tff(func_def_617,type,
sK616: ( vTStore * vTTContext ) > vName ).
tff(func_def_618,type,
sK617: ( vTStore * vTTContext ) > vTStore ).
tff(func_def_619,type,
sK618: ( vTStore * vTTContext ) > vTType ).
tff(func_def_620,type,
sK619: ( vPred * vTType * vSelect * vName * vTTContext ) > vTType ).
tff(func_def_621,type,
sK620: ( vRawTable * vAttrL ) > vRawTable ).
tff(func_def_622,type,
sK621: ( vRawTable * vAttrL * vName ) > vRawTable ).
tff(func_def_623,type,
sK622: vAttrL ).
tff(func_def_624,type,
sK623: vRawTable ).
tff(func_def_625,type,
sK624: vTType ).
tff(func_def_626,type,
sK625: vAttrL ).
tff(func_def_627,type,
sK626: vName ).
tff(func_def_628,type,
sK627: vTType ).
tff(pred_def_1,type,
vmatchingAttrL: ( vTType * vAttrL ) > $o ).
tff(pred_def_2,type,
visSomeTType: vOptTType > $o ).
tff(pred_def_3,type,
visSomeRawTable: vOptRawTable > $o ).
tff(pred_def_4,type,
vsameLength: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_5,type,
vfilterSingleRow: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_6,type,
vlessThan: ( vVal * vVal ) > $o ).
tff(pred_def_7,type,
visSomeVal: vOptVal > $o ).
tff(pred_def_8,type,
vwelltypedRawtable: ( vTType * vRawTable ) > $o ).
tff(pred_def_9,type,
vgreaterThan: ( vVal * vVal ) > $o ).
tff(pred_def_10,type,
visValue: vQuery > $o ).
tff(pred_def_11,type,
vwelltypedtable: ( vTType * vTable ) > $o ).
tff(pred_def_12,type,
visSomeFType: vOptFType > $o ).
tff(pred_def_13,type,
vtcheckPred: ( vPred * vTType ) > $o ).
tff(pred_def_14,type,
vrowIn: ( vRow * vRawTable ) > $o ).
tff(pred_def_15,type,
visSomeTable: vOptTable > $o ).
tff(pred_def_16,type,
vwelltypedRow: ( vTType * vRow ) > $o ).
tff(pred_def_17,type,
visSomeQuery: vOptQuery > $o ).
tff(pred_def_18,type,
vstoreContextConsistent: ( vTStore * vTTContext ) > $o ).
tff(pred_def_19,type,
vptcheck: ( vTTContext * vQuery * vTType ) > $o ).
tff(pred_def_20,type,
sP0: ( vAttrL * vAttrL ) > $o ).
tff(pred_def_21,type,
sP1: ( vTType * vAttrL ) > $o ).
tff(pred_def_22,type,
sP2: ( vTType * vRow ) > $o ).
tff(pred_def_23,type,
sP3: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_24,type,
sP4: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_25,type,
sP5: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_26,type,
sP6: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_27,type,
sP7: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_28,type,
sP8: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_29,type,
sP9: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_30,type,
sP10: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_31,type,
sP11: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_32,type,
sP12: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_33,type,
sP13: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_34,type,
sP14: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_35,type,
sP15: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_36,type,
sP16: ( vName * vTStore ) > $o ).
tff(pred_def_37,type,
sP17: ( vName * vTStore ) > $o ).
tff(pred_def_38,type,
sP18: ( vName * vTTContext ) > $o ).
tff(pred_def_39,type,
sP19: ( vName * vTTContext ) > $o ).
tff(pred_def_40,type,
sP20: ( vName * vAttrL * vRawTable ) > $o ).
tff(pred_def_41,type,
sP21: ( vName * vAttrL * vRawTable ) > $o ).
tff(pred_def_42,type,
sP22: ( vAttrL * vAttrL * vRawTable ) > $o ).
tff(pred_def_43,type,
sP23: ( vAttrL * vAttrL * vRawTable ) > $o ).
tff(pred_def_44,type,
sP24: ( vSelect * vTable ) > $o ).
tff(pred_def_45,type,
sP25: ( vSelect * vTable ) > $o ).
tff(pred_def_46,type,
sP26: ( vExp * vAttrL * vRow ) > $o ).
tff(pred_def_47,type,
sP27: ( vExp * vAttrL * vRow ) > $o ).
tff(pred_def_48,type,
sP28: ( vExp * vAttrL * vRow ) > $o ).
tff(pred_def_49,type,
sP29: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_50,type,
sP30: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_51,type,
sP31: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_52,type,
sP32: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_53,type,
sP33: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_54,type,
sP34: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_55,type,
sP35: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_56,type,
sP36: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_57,type,
sP37: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_58,type,
sP38: ( vRawTable * vAttrL * vPred ) > $o ).
tff(pred_def_59,type,
sP39: ( vRawTable * vAttrL * vPred ) > $o ).
tff(pred_def_60,type,
sP40: ( vQuery * vTStore ) > $o ).
tff(pred_def_61,type,
sP41: ( vQuery * vTStore ) > $o ).
tff(pred_def_62,type,
sP42: ( vQuery * vTStore ) > $o ).
tff(pred_def_63,type,
sP43: ( vQuery * vTStore ) > $o ).
tff(pred_def_64,type,
sP44: ( vQuery * vTStore ) > $o ).
tff(pred_def_65,type,
sP45: ( vQuery * vTStore ) > $o ).
tff(pred_def_66,type,
sP46: ( vQuery * vTStore ) > $o ).
tff(pred_def_67,type,
sP47: ( vQuery * vTStore ) > $o ).
tff(pred_def_68,type,
sP48: ( vQuery * vTStore ) > $o ).
tff(pred_def_69,type,
sP49: ( vQuery * vTStore ) > $o ).
tff(pred_def_70,type,
sP50: ( vQuery * vTStore ) > $o ).
tff(pred_def_71,type,
sP51: ( vQuery * vTStore ) > $o ).
tff(pred_def_72,type,
sP52: ( vQuery * vTStore ) > $o ).
tff(pred_def_73,type,
sP53: ( vQuery * vTStore ) > $o ).
tff(pred_def_74,type,
sP54: ( vQuery * vTStore ) > $o ).
tff(pred_def_75,type,
sP55: ( vQuery * vTStore ) > $o ).
tff(pred_def_76,type,
sP56: ( vQuery * vTStore ) > $o ).
tff(pred_def_77,type,
sP57: ( vQuery * vTStore ) > $o ).
tff(pred_def_78,type,
sP58: ( vName * vTType ) > $o ).
tff(pred_def_79,type,
sP59: ( vName * vTType ) > $o ).
tff(pred_def_80,type,
sP60: ( vAttrL * vTType ) > $o ).
tff(pred_def_81,type,
sP61: ( vAttrL * vTType ) > $o ).
tff(pred_def_82,type,
sP62: ( vSelect * vTType ) > $o ).
tff(pred_def_83,type,
sP63: ( vExp * vTType ) > $o ).
tff(pred_def_84,type,
sP64: ( vExp * vTType ) > $o ).
tff(pred_def_85,type,
sP65: ( vExp * vTType ) > $o ).
tff(pred_def_86,type,
sP66: ( vPred * vTType ) > $o ).
tff(pred_def_87,type,
sP67: ( vPred * vTType ) > $o ).
tff(pred_def_88,type,
sP68: ( vPred * vTType ) > $o ).
tff(pred_def_89,type,
sP69: ( vPred * vTType ) > $o ).
tff(pred_def_90,type,
sP70: ( vPred * vTType ) > $o ).
tff(pred_def_91,type,
sP71: ( vPred * vTType ) > $o ).
tff(pred_def_92,type,
sP72: ( vPred * vTType ) > $o ).
tff(pred_def_93,type,
sP73: ( vPred * vTType ) > $o ).
tff(pred_def_94,type,
sP74: ( vTStore * vTTContext ) > $o ).
tff(pred_def_95,type,
sP75: ( vTStore * vTTContext ) > $o ).
tff(f29,axiom,
! [X0: vOptRawTable] :
( ( X0 = vnoRawTable )
| ? [X1: vRawTable] : ( X0 = vsomeRawTable(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','dom-OptRawTable') ).
tff(f31,axiom,
! [X0: vRawTable] : ( vnoRawTable != vsomeRawTable(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noRawTable-someRawTable') ).
tff(f34,axiom,
! [X0: vTType] : ( vnoTType != vsomeTType(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-noTType-someTType') ).
tff(f87,axiom,
! [X0: vName,X1: vAttrL,X2: vName,X3: vAttrL] :
( ( vacons(X0,X1) = vacons(X2,X3) )
=> ( ( X0 = X2 )
& ( X1 = X3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','EQ-acons') ).
tff(f88,axiom,
! [X0: vName,X1: vAttrL] : ( vaempty != vacons(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','DIFF-aempty-acons') ).
tff(f132,axiom,
! [X0: vRawTable] : visSomeRawTable(vsomeRawTable(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeRawTable-1') ).
tff(f134,axiom,
! [X0: vOptRawTable] :
( ~ visSomeRawTable(X0)
=> ( X0 = vnoRawTable ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeRawTable-false-INV') ).
tff(f170,axiom,
! [X0: vOptTType] :
( visSomeTType(X0)
=> ? [X1: vTType] : ( X0 = vsomeTType(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeTType-true-INV') ).
tff(f195,axiom,
! [X0: vName,X1: vAttrL,X2: vRawTable,X3: vAttrL] :
( ( visSomeRawTable(vfindCol(X0,X1,X2))
& visSomeRawTable(vprojectCols(X3,X1,X2)) )
=> ( vprojectCols(vacons(X0,X3),X1,X2) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(X0,X1,X2)),vgetRawTable(vprojectCols(X3,X1,X2)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','projectCols-1') ).
tff(f247,axiom,
! [X0: vOptFType] :
( visSomeFType(X0)
=> ? [X1: vFType] : ( X0 = vsomeFType(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','isSomeFType-true-INV') ).
tff(f255,axiom,
! [X0: vName,X1: vTType,X2: vAttrL] :
( ~ ( visSomeFType(vfindColType(X0,X1))
& visSomeTType(vprojectTypeAttrL(X2,X1)) )
=> ( vprojectTypeAttrL(vacons(X0,X2),X1) = vnoTType ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','projectTypeAttrL-2') ).
tff(f256,axiom,
! [X0: vAttrL,X1: vTType] :
( ? [X2: vTType] :
( ( X0 = vaempty )
& ( X1 = X2 )
& ( vprojectTypeAttrL(X0,X1) = vsomeTType(vttempty) ) )
| ? [X3: vName,X4: vOptFType,X5: vTType,X6: vAttrL,X7: vOptTType] :
( ( X4 = vfindColType(X3,X5) )
& ( X7 = vprojectTypeAttrL(X6,X5) )
& visSomeFType(X4)
& visSomeTType(X7)
& ( X0 = vacons(X3,X6) )
& ( X1 = X5 )
& ( vprojectTypeAttrL(X0,X1) = vsomeTType(vttcons(X3,vgetFType(X4),vgetTType(X7))) ) )
| ? [X8: vName,X9: vOptFType,X10: vTType,X11: vAttrL,X12: vOptTType] :
( ( X9 = vfindColType(X8,X10) )
& ( X12 = vprojectTypeAttrL(X11,X10) )
& ~ ( visSomeFType(X9)
& visSomeTType(X12) )
& ( X0 = vacons(X8,X11) )
& ( X1 = X10 )
& ( vprojectTypeAttrL(X0,X1) = vnoTType ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','projectTypeAttrL-INV') ).
tff(f257,axiom,
! [X0: vTType] : ( vprojectType(vall,X0) = vsomeTType(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','projectType-0') ).
tff(f258,axiom,
! [X0: vAttrL,X1: vTType] : ( vprojectType(vlist(X0),X1) = vprojectTypeAttrL(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','projectType-1') ).
tff(f293,axiom,
! [X0: vTType,X1: vRawTable,X2: vAttrL,X3: vTType] :
( ( vwelltypedRawtable(X0,X1)
& vmatchingAttrL(X0,X2)
& ( vprojectTypeAttrL(val1,X0) = vsomeTType(X3) ) )
=> ? [X4: vRawTable] : ( vprojectCols(val1,X2,X1) = vsomeRawTable(X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','projectColsProgress-acons-IH0') ).
tff(f294,axiom,
! [X0: vRawTable,X1: vFType,X2: vAttrL,X3: vName,X4: vTType] :
( ( vwelltypedRawtable(X4,X0)
& vmatchingAttrL(X4,X2)
& ( vfindColType(X3,X4) = vsomeFType(X1) ) )
=> ? [X5: vRawTable] : ( vfindCol(X3,X2,X0) = vsomeRawTable(X5) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',findColTypeImpliesfindCol) ).
tff(f297,conjecture,
! [X0: vAttrL,X1: vRawTable,X2: vTType,X3: vAttrL,X4: vName,X5: vTType] :
( ( ~ ( visSomeRawTable(vfindCol(X4,val1,X1))
& visSomeRawTable(vprojectCols(X3,val1,X1)) )
& vwelltypedRawtable(X5,X1)
& vmatchingAttrL(X5,X0)
& ( vprojectTypeAttrL(vacons(X4,val1),X5) = vsomeTType(X2) ) )
=> ? [X6: vRawTable] : ( vprojectCols(vacons(X4,val1),X0,X1) = vsomeRawTable(X6) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','projectColsProgress-acons-isSomeRawTable-isSomeRawTable-False') ).
tff(f298,negated_conjecture,
~ ! [X0: vAttrL,X1: vRawTable,X2: vTType,X3: vAttrL,X4: vName,X5: vTType] :
( ( ~ ( visSomeRawTable(vfindCol(X4,val1,X1))
& visSomeRawTable(vprojectCols(X3,val1,X1)) )
& vwelltypedRawtable(X5,X1)
& vmatchingAttrL(X5,X0)
& ( vprojectTypeAttrL(vacons(X4,val1),X5) = vsomeTType(X2) ) )
=> ? [X6: vRawTable] : ( vprojectCols(vacons(X4,val1),X0,X1) = vsomeRawTable(X6) ) ),
inference(negated_conjecture,[status(cth)],[f297]) ).
tff(f338,plain,
! [X0: vName,X1: vAttrL,X2: vName,X3: vAttrL] :
( ( ( X0 = X2 )
& ( X1 = X3 ) )
| ( vacons(X0,X1) != vacons(X2,X3) ) ),
inference(ennf_transformation,[],[f87]) ).
tff(f360,plain,
! [X0: vOptRawTable] :
( ( X0 = vnoRawTable )
| visSomeRawTable(X0) ),
inference(ennf_transformation,[],[f134]) ).
tff(f386,plain,
! [X0: vOptTType] :
( ? [X1: vTType] : ( X0 = vsomeTType(X1) )
| ~ visSomeTType(X0) ),
inference(ennf_transformation,[],[f170]) ).
tff(f395,plain,
! [X0: vName,X1: vAttrL,X2: vRawTable,X3: vAttrL] :
( ( vprojectCols(vacons(X0,X3),X1,X2) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(X0,X1,X2)),vgetRawTable(vprojectCols(X3,X1,X2)))) )
| ~ visSomeRawTable(vfindCol(X0,X1,X2))
| ~ visSomeRawTable(vprojectCols(X3,X1,X2)) ),
inference(ennf_transformation,[],[f195]) ).
tff(f396,plain,
! [X0: vName,X1: vAttrL,X2: vRawTable,X3: vAttrL] :
( ( vprojectCols(vacons(X0,X3),X1,X2) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(X0,X1,X2)),vgetRawTable(vprojectCols(X3,X1,X2)))) )
| ~ visSomeRawTable(vfindCol(X0,X1,X2))
| ~ visSomeRawTable(vprojectCols(X3,X1,X2)) ),
inference(flattening,[],[f395]) ).
tff(f441,plain,
! [X0: vOptFType] :
( ? [X1: vFType] : ( X0 = vsomeFType(X1) )
| ~ visSomeFType(X0) ),
inference(ennf_transformation,[],[f247]) ).
tff(f446,plain,
! [X0: vName,X1: vTType,X2: vAttrL] :
( ( vprojectTypeAttrL(vacons(X0,X2),X1) = vnoTType )
| ( visSomeFType(vfindColType(X0,X1))
& visSomeTType(vprojectTypeAttrL(X2,X1)) ) ),
inference(ennf_transformation,[],[f255]) ).
tff(f447,plain,
! [X0: vAttrL,X1: vTType] :
( ? [X2: vTType] :
( ( X0 = vaempty )
& ( X1 = X2 )
& ( vprojectTypeAttrL(X0,X1) = vsomeTType(vttempty) ) )
| ? [X3: vName,X4: vOptFType,X5: vTType,X6: vAttrL,X7: vOptTType] :
( ( X4 = vfindColType(X3,X5) )
& ( X7 = vprojectTypeAttrL(X6,X5) )
& visSomeFType(X4)
& visSomeTType(X7)
& ( X0 = vacons(X3,X6) )
& ( X1 = X5 )
& ( vprojectTypeAttrL(X0,X1) = vsomeTType(vttcons(X3,vgetFType(X4),vgetTType(X7))) ) )
| ? [X8: vName,X9: vOptFType,X10: vTType,X11: vAttrL,X12: vOptTType] :
( ( X9 = vfindColType(X8,X10) )
& ( X12 = vprojectTypeAttrL(X11,X10) )
& ( ~ visSomeFType(X9)
| ~ visSomeTType(X12) )
& ( X0 = vacons(X8,X11) )
& ( X1 = X10 )
& ( vprojectTypeAttrL(X0,X1) = vnoTType ) ) ),
inference(ennf_transformation,[],[f256]) ).
tff(f479,plain,
! [X0: vTType,X1: vRawTable,X2: vAttrL,X3: vTType] :
( ? [X4: vRawTable] : ( vprojectCols(val1,X2,X1) = vsomeRawTable(X4) )
| ~ vwelltypedRawtable(X0,X1)
| ~ vmatchingAttrL(X0,X2)
| ( vsomeTType(X3) != vprojectTypeAttrL(val1,X0) ) ),
inference(ennf_transformation,[],[f293]) ).
tff(f480,plain,
! [X0: vTType,X1: vRawTable,X2: vAttrL,X3: vTType] :
( ? [X4: vRawTable] : ( vprojectCols(val1,X2,X1) = vsomeRawTable(X4) )
| ~ vwelltypedRawtable(X0,X1)
| ~ vmatchingAttrL(X0,X2)
| ( vsomeTType(X3) != vprojectTypeAttrL(val1,X0) ) ),
inference(flattening,[],[f479]) ).
tff(f481,plain,
! [X0: vRawTable,X1: vFType,X2: vAttrL,X3: vName,X4: vTType] :
( ? [X5: vRawTable] : ( vfindCol(X3,X2,X0) = vsomeRawTable(X5) )
| ~ vwelltypedRawtable(X4,X0)
| ~ vmatchingAttrL(X4,X2)
| ( vsomeFType(X1) != vfindColType(X3,X4) ) ),
inference(ennf_transformation,[],[f294]) ).
tff(f482,plain,
! [X0: vRawTable,X1: vFType,X2: vAttrL,X3: vName,X4: vTType] :
( ? [X5: vRawTable] : ( vfindCol(X3,X2,X0) = vsomeRawTable(X5) )
| ~ vwelltypedRawtable(X4,X0)
| ~ vmatchingAttrL(X4,X2)
| ( vsomeFType(X1) != vfindColType(X3,X4) ) ),
inference(flattening,[],[f481]) ).
tff(f486,plain,
? [X0: vAttrL,X1: vRawTable,X2: vTType,X3: vAttrL,X4: vName,X5: vTType] :
( ! [X6: vRawTable] : ( vprojectCols(vacons(X4,val1),X0,X1) != vsomeRawTable(X6) )
& ( ~ visSomeRawTable(vfindCol(X4,val1,X1))
| ~ visSomeRawTable(vprojectCols(X3,val1,X1)) )
& vwelltypedRawtable(X5,X1)
& vmatchingAttrL(X5,X0)
& ( vprojectTypeAttrL(vacons(X4,val1),X5) = vsomeTType(X2) ) ),
inference(ennf_transformation,[],[f298]) ).
tff(f487,plain,
? [X0: vAttrL,X1: vRawTable,X2: vTType,X3: vAttrL,X4: vName,X5: vTType] :
( ! [X6: vRawTable] : ( vprojectCols(vacons(X4,val1),X0,X1) != vsomeRawTable(X6) )
& ( ~ visSomeRawTable(vfindCol(X4,val1,X1))
| ~ visSomeRawTable(vprojectCols(X3,val1,X1)) )
& vwelltypedRawtable(X5,X1)
& vmatchingAttrL(X5,X0)
& ( vprojectTypeAttrL(vacons(X4,val1),X5) = vsomeTType(X2) ) ),
inference(flattening,[],[f486]) ).
tff(f567,definition,
! [X0: vAttrL,X1: vTType] :
( ? [X3: vName,X4: vOptFType,X5: vTType,X6: vAttrL,X7: vOptTType] :
( ( X4 = vfindColType(X3,X5) )
& ( X7 = vprojectTypeAttrL(X6,X5) )
& visSomeFType(X4)
& visSomeTType(X7)
& ( X0 = vacons(X3,X6) )
& ( X1 = X5 )
& ( vprojectTypeAttrL(X0,X1) = vsomeTType(vttcons(X3,vgetFType(X4),vgetTType(X7))) ) )
| ~ sP60(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP60])],[predicate_definition_introduction]) ).
tff(f568,definition,
! [X0: vAttrL,X1: vTType] :
( ? [X8: vName,X9: vOptFType,X10: vTType,X11: vAttrL,X12: vOptTType] :
( ( X9 = vfindColType(X8,X10) )
& ( X12 = vprojectTypeAttrL(X11,X10) )
& ( ~ visSomeFType(X9)
| ~ visSomeTType(X12) )
& ( X0 = vacons(X8,X11) )
& ( X1 = X10 )
& ( vprojectTypeAttrL(X0,X1) = vnoTType ) )
| ~ sP61(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP61])],[predicate_definition_introduction]) ).
tff(f569,plain,
! [X0: vAttrL,X1: vTType] :
( ? [X2: vTType] :
( ( X0 = vaempty )
& ( X1 = X2 )
& ( vprojectTypeAttrL(X0,X1) = vsomeTType(vttempty) ) )
| sP60(X0,X1)
| sP61(X0,X1) ),
inference(definition_folding,[],[f447,f568,f567]) ).
tff(f595,plain,
! [X0: vOptRawTable] :
( ( X0 = vnoRawTable )
| ( vsomeRawTable(sK94(X0)) = X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK94]),skolemize(X1,sK94(X0))],[f29]) ).
tff(f702,plain,
! [X0: vOptTType] :
( ( vsomeTType(sK265(X0)) = X0 )
| ~ visSomeTType(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK265]),skolemize(X1,sK265(X0))],[f386]) ).
tff(f860,plain,
! [X0: vOptFType] :
( ( vsomeFType(sK523(X0)) = X0 )
| ~ visSomeFType(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK523]),skolemize(X1,sK523(X0))],[f441]) ).
tff(f868,plain,
! [X0: vAttrL,X1: vTType] :
( ? [X8: vName,X9: vOptFType,X10: vTType,X11: vAttrL,X12: vOptTType] :
( ( X9 = vfindColType(X8,X10) )
& ( X12 = vprojectTypeAttrL(X11,X10) )
& ( ~ visSomeFType(X9)
| ~ visSomeTType(X12) )
& ( X0 = vacons(X8,X11) )
& ( X1 = X10 )
& ( vprojectTypeAttrL(X0,X1) = vnoTType ) )
| ~ sP61(X0,X1) ),
inference(nnf_transformation,[],[f568]) ).
tff(f869,plain,
! [X0: vAttrL,X1: vTType] :
( ? [X2: vName,X3: vOptFType,X4: vTType,X5: vAttrL,X6: vOptTType] :
( ( vfindColType(X2,X4) = X3 )
& ( vprojectTypeAttrL(X5,X4) = X6 )
& ( ~ visSomeFType(X3)
| ~ visSomeTType(X6) )
& ( vacons(X2,X5) = X0 )
& ( X1 = X4 )
& ( vprojectTypeAttrL(X0,X1) = vnoTType ) )
| ~ sP61(X0,X1) ),
inference(rectify,[],[f868]) ).
tff(f870,plain,
! [X0: vAttrL,X1: vTType] :
( ( ( sK534(X0,X1) = vfindColType(sK533(X0,X1),sK535(X0,X1)) )
& ( sK537(X0,X1) = vprojectTypeAttrL(sK536(X0,X1),sK535(X0,X1)) )
& ( ~ visSomeFType(sK534(X0,X1))
| ~ visSomeTType(sK537(X0,X1)) )
& ( vacons(sK533(X0,X1),sK536(X0,X1)) = X0 )
& ( sK535(X0,X1) = X1 )
& ( vprojectTypeAttrL(X0,X1) = vnoTType ) )
| ~ sP61(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK533,sK534,sK535,sK536,sK537]),skolemize(X2,sK533(X0,X1)),skolemize(X3,sK534(X0,X1)),skolemize(X4,sK535(X0,X1)),skolemize(X5,sK536(X0,X1)),skolemize(X6,sK537(X0,X1))],[f869]) ).
tff(f871,plain,
! [X0: vAttrL,X1: vTType] :
( ? [X3: vName,X4: vOptFType,X5: vTType,X6: vAttrL,X7: vOptTType] :
( ( X4 = vfindColType(X3,X5) )
& ( X7 = vprojectTypeAttrL(X6,X5) )
& visSomeFType(X4)
& visSomeTType(X7)
& ( X0 = vacons(X3,X6) )
& ( X1 = X5 )
& ( vprojectTypeAttrL(X0,X1) = vsomeTType(vttcons(X3,vgetFType(X4),vgetTType(X7))) ) )
| ~ sP60(X0,X1) ),
inference(nnf_transformation,[],[f567]) ).
tff(f872,plain,
! [X0: vAttrL,X1: vTType] :
( ? [X2: vName,X3: vOptFType,X4: vTType,X5: vAttrL,X6: vOptTType] :
( ( vfindColType(X2,X4) = X3 )
& ( vprojectTypeAttrL(X5,X4) = X6 )
& visSomeFType(X3)
& visSomeTType(X6)
& ( vacons(X2,X5) = X0 )
& ( X1 = X4 )
& ( vprojectTypeAttrL(X0,X1) = vsomeTType(vttcons(X2,vgetFType(X3),vgetTType(X6))) ) )
| ~ sP60(X0,X1) ),
inference(rectify,[],[f871]) ).
tff(f873,plain,
! [X0: vAttrL,X1: vTType] :
( ( ( sK539(X0,X1) = vfindColType(sK538(X0,X1),sK540(X0,X1)) )
& ( sK542(X0,X1) = vprojectTypeAttrL(sK541(X0,X1),sK540(X0,X1)) )
& visSomeFType(sK539(X0,X1))
& visSomeTType(sK542(X0,X1))
& ( vacons(sK538(X0,X1),sK541(X0,X1)) = X0 )
& ( sK540(X0,X1) = X1 )
& ( vprojectTypeAttrL(X0,X1) = vsomeTType(vttcons(sK538(X0,X1),vgetFType(sK539(X0,X1)),vgetTType(sK542(X0,X1)))) ) )
| ~ sP60(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK538,sK539,sK540,sK541,sK542]),skolemize(X2,sK538(X0,X1)),skolemize(X3,sK539(X0,X1)),skolemize(X4,sK540(X0,X1)),skolemize(X5,sK541(X0,X1)),skolemize(X6,sK542(X0,X1))],[f872]) ).
tff(f874,plain,
! [X0: vAttrL,X1: vTType] :
( ( ( X0 = vaempty )
& ( sK543(X0,X1) = X1 )
& ( vprojectTypeAttrL(X0,X1) = vsomeTType(vttempty) ) )
| sP60(X0,X1)
| sP61(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK543]),skolemize(X2,sK543(X0,X1))],[f569]) ).
tff(f935,plain,
! [X0: vTType,X1: vRawTable,X2: vAttrL,X3: vTType] :
( ( vprojectCols(val1,X2,X1) = vsomeRawTable(sK620(X1,X2)) )
| ~ vwelltypedRawtable(X0,X1)
| ~ vmatchingAttrL(X0,X2)
| ( vsomeTType(X3) != vprojectTypeAttrL(val1,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK620]),skolemize(X4,sK620(X1,X2))],[f480]) ).
tff(f936,plain,
! [X0: vRawTable,X1: vFType,X2: vAttrL,X3: vName,X4: vTType] :
( ( vfindCol(X3,X2,X0) = vsomeRawTable(sK621(X0,X2,X3)) )
| ~ vwelltypedRawtable(X4,X0)
| ~ vmatchingAttrL(X4,X2)
| ( vsomeFType(X1) != vfindColType(X3,X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK621]),skolemize(X5,sK621(X0,X2,X3))],[f482]) ).
tff(f937,plain,
( ! [X6: vRawTable] : ( vsomeRawTable(X6) != vprojectCols(vacons(sK626,val1),sK622,sK623) )
& ( ~ visSomeRawTable(vfindCol(sK626,val1,sK623))
| ~ visSomeRawTable(vprojectCols(sK625,val1,sK623)) )
& vwelltypedRawtable(sK627,sK623)
& vmatchingAttrL(sK627,sK622)
& ( vsomeTType(sK624) = vprojectTypeAttrL(vacons(sK626,val1),sK627) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK622,sK623,sK624,sK625,sK626,sK627]),skolemize(X0,sK622),skolemize(X1,sK623),skolemize(X2,sK624),skolemize(X3,sK625),skolemize(X4,sK626),skolemize(X5,sK627)],[f487]) ).
tff(f975,plain,
! [X0: vOptRawTable] :
( ( vnoRawTable = X0 )
| ( vsomeRawTable(sK94(X0)) = X0 ) ),
inference(cnf_transformation,[],[f595]) ).
tff(f977,plain,
! [X0: vRawTable] : ( vnoRawTable != vsomeRawTable(X0) ),
inference(cnf_transformation,[],[f31]) ).
tff(f980,plain,
! [X0: vTType] : ( vnoTType != vsomeTType(X0) ),
inference(cnf_transformation,[],[f34]) ).
tff(f1043,plain,
! [X2: vName,X3: vAttrL,X0: vName,X1: vAttrL] :
( ( X0 = X2 )
| ( vacons(X0,X1) != vacons(X2,X3) ) ),
inference(cnf_transformation,[],[f338]) ).
tff(f1044,plain,
! [X0: vName,X1: vAttrL] : ( vaempty != vacons(X0,X1) ),
inference(cnf_transformation,[],[f88]) ).
tff(f1174,plain,
! [X0: vRawTable] : visSomeRawTable(vsomeRawTable(X0)),
inference(cnf_transformation,[],[f132]) ).
tff(f1176,plain,
! [X0: vOptRawTable] :
( ( vnoRawTable = X0 )
| visSomeRawTable(X0) ),
inference(cnf_transformation,[],[f360]) ).
tff(f1310,plain,
! [X0: vOptTType] :
( ( vsomeTType(sK265(X0)) = X0 )
| ~ visSomeTType(X0) ),
inference(cnf_transformation,[],[f702]) ).
tff(f1361,plain,
! [X2: vRawTable,X3: vAttrL,X0: vName,X1: vAttrL] :
( ( vprojectCols(vacons(X0,X3),X1,X2) = vsomeRawTable(vattachColToFrontRaw(vgetRawTable(vfindCol(X0,X1,X2)),vgetRawTable(vprojectCols(X3,X1,X2)))) )
| ~ visSomeRawTable(vfindCol(X0,X1,X2))
| ~ visSomeRawTable(vprojectCols(X3,X1,X2)) ),
inference(cnf_transformation,[],[f396]) ).
tff(f1688,plain,
! [X0: vOptFType] :
( ( vsomeFType(sK523(X0)) = X0 )
| ~ visSomeFType(X0) ),
inference(cnf_transformation,[],[f860]) ).
tff(f1706,plain,
! [X2: vAttrL,X0: vName,X1: vTType] :
( ( vnoTType = vprojectTypeAttrL(vacons(X0,X2),X1) )
| visSomeTType(vprojectTypeAttrL(X2,X1)) ),
inference(cnf_transformation,[],[f446]) ).
tff(f1708,plain,
! [X0: vAttrL,X1: vTType] :
( ( vnoTType = vprojectTypeAttrL(X0,X1) )
| ~ sP61(X0,X1) ),
inference(cnf_transformation,[],[f870]) ).
tff(f1715,plain,
! [X0: vAttrL,X1: vTType] :
( ( sK540(X0,X1) = X1 )
| ~ sP60(X0,X1) ),
inference(cnf_transformation,[],[f873]) ).
tff(f1716,plain,
! [X0: vAttrL,X1: vTType] :
( ( vacons(sK538(X0,X1),sK541(X0,X1)) = X0 )
| ~ sP60(X0,X1) ),
inference(cnf_transformation,[],[f873]) ).
tff(f1718,plain,
! [X0: vAttrL,X1: vTType] :
( visSomeFType(sK539(X0,X1))
| ~ sP60(X0,X1) ),
inference(cnf_transformation,[],[f873]) ).
tff(f1720,plain,
! [X0: vAttrL,X1: vTType] :
( ( sK539(X0,X1) = vfindColType(sK538(X0,X1),sK540(X0,X1)) )
| ~ sP60(X0,X1) ),
inference(cnf_transformation,[],[f873]) ).
tff(f1723,plain,
! [X0: vAttrL,X1: vTType] :
( ( vaempty = X0 )
| sP60(X0,X1)
| sP61(X0,X1) ),
inference(cnf_transformation,[],[f874]) ).
tff(f1724,plain,
! [X0: vTType] : ( vsomeTType(X0) = vprojectType(vall,X0) ),
inference(cnf_transformation,[],[f257]) ).
tff(f1725,plain,
! [X0: vAttrL,X1: vTType] : ( vprojectTypeAttrL(X0,X1) = vprojectType(vlist(X0),X1) ),
inference(cnf_transformation,[],[f258]) ).
tff(f1860,plain,
! [X2: vAttrL,X3: vTType,X0: vTType,X1: vRawTable] :
( ( vprojectCols(val1,X2,X1) = vsomeRawTable(sK620(X1,X2)) )
| ~ vwelltypedRawtable(X0,X1)
| ~ vmatchingAttrL(X0,X2)
| ( vsomeTType(X3) != vprojectTypeAttrL(val1,X0) ) ),
inference(cnf_transformation,[],[f935]) ).
tff(f1861,plain,
! [X2: vAttrL,X3: vName,X0: vRawTable,X1: vFType,X4: vTType] :
( ( vfindCol(X3,X2,X0) = vsomeRawTable(sK621(X0,X2,X3)) )
| ~ vwelltypedRawtable(X4,X0)
| ~ vmatchingAttrL(X4,X2)
| ( vsomeFType(X1) != vfindColType(X3,X4) ) ),
inference(cnf_transformation,[],[f936]) ).
tff(f1864,plain,
vsomeTType(sK624) = vprojectTypeAttrL(vacons(sK626,val1),sK627),
inference(cnf_transformation,[],[f937]) ).
tff(f1865,plain,
vmatchingAttrL(sK627,sK622),
inference(cnf_transformation,[],[f937]) ).
tff(f1866,plain,
vwelltypedRawtable(sK627,sK623),
inference(cnf_transformation,[],[f937]) ).
tff(f1868,plain,
! [X6: vRawTable] : ( vsomeRawTable(X6) != vprojectCols(vacons(sK626,val1),sK622,sK623) ),
inference(cnf_transformation,[],[f937]) ).
tff(f1874,plain,
! [X0: vTType] : ( vnoTType != vprojectType(vall,X0) ),
inference(definition_unfolding,[],[f980,f1724]) ).
tff(f1884,plain,
! [X0: vOptTType] :
( ( vprojectType(vall,sK265(X0)) = X0 )
| ~ visSomeTType(X0) ),
inference(definition_unfolding,[],[f1310,f1724]) ).
tff(f1907,plain,
! [X2: vAttrL,X0: vName,X1: vTType] :
( ( vnoTType = vprojectType(vlist(vacons(X0,X2)),X1) )
| visSomeTType(vprojectType(vlist(X2),X1)) ),
inference(definition_unfolding,[],[f1706,f1725,f1725]) ).
tff(f1909,plain,
! [X0: vAttrL,X1: vTType] :
( ( vnoTType = vprojectType(vlist(X0),X1) )
| ~ sP61(X0,X1) ),
inference(definition_unfolding,[],[f1708,f1725]) ).
tff(f1918,plain,
! [X2: vAttrL,X3: vTType,X0: vTType,X1: vRawTable] :
( ( vprojectCols(val1,X2,X1) = vsomeRawTable(sK620(X1,X2)) )
| ~ vwelltypedRawtable(X0,X1)
| ~ vmatchingAttrL(X0,X2)
| ( vprojectType(vall,X3) != vprojectType(vlist(val1),X0) ) ),
inference(definition_unfolding,[],[f1860,f1724,f1725]) ).
tff(f1919,plain,
vprojectType(vall,sK624) = vprojectType(vlist(vacons(sK626,val1)),sK627),
inference(definition_unfolding,[],[f1864,f1724,f1725]) ).
tff(f1965,definition,
( spl628_3
<=> ! [X1: vTType] : ( vprojectType(vall,X1) != vprojectType(vlist(val1),sK627) ) ),
introduced(definition,[new_symbols(definition,[spl628_3])],[avatar_definition]) ).
tff(f1966,plain,
( ! [X1: vTType] : ( vprojectType(vall,X1) != vprojectType(vlist(val1),sK627) )
| ~ spl628_3 ),
inference(avatar_component_clause,[],[f1965]) ).
tff(f2019,plain,
! [X0: vAttrL,X1: vTType] :
( ( vprojectCols(val1,X0,sK623) = vsomeRawTable(sK620(sK623,X0)) )
| ~ vmatchingAttrL(sK627,X0)
| ( vprojectType(vall,X1) != vprojectType(vlist(val1),sK627) ) ),
inference(resolution,[],[f1866,f1918]) ).
tff(f2106,plain,
( ( vnoTType = vprojectType(vall,sK624) )
| ~ sP61(vacons(sK626,val1),sK627) ),
inference(superposition,[],[f1909,f1919]) ).
tff(f2110,plain,
( ( vnoTType = vprojectType(vall,sK624) )
| visSomeTType(vprojectType(vlist(val1),sK627)) ),
inference(superposition,[],[f1907,f1919]) ).
tff(f2114,plain,
visSomeTType(vprojectType(vlist(val1),sK627)),
inference(forward_subsumption_resolution,[],[f2110,f1874]) ).
tff(f2117,plain,
~ sP61(vacons(sK626,val1),sK627),
inference(forward_subsumption_resolution,[],[f2106,f1874]) ).
tff(f2122,definition,
( spl628_25
<=> sP60(vacons(sK626,val1),sK627) ),
introduced(definition,[new_symbols(definition,[spl628_25])],[avatar_definition]) ).
tff(f2123,plain,
( sP60(vacons(sK626,val1),sK627)
| ~ spl628_25 ),
inference(avatar_component_clause,[],[f2122]) ).
tff(f2137,plain,
! [X2: vAttrL,X3: vRawTable,X0: vName,X1: vAttrL] :
( ( vprojectCols(vacons(sK626,val1),sK622,sK623) != vprojectCols(vacons(X0,X1),X2,X3) )
| ~ visSomeRawTable(vfindCol(X0,X2,X3))
| ~ visSomeRawTable(vprojectCols(X1,X2,X3)) ),
inference(superposition,[],[f1868,f1361]) ).
tff(f2140,plain,
! [X0: vOptRawTable] :
( ( vprojectCols(vacons(sK626,val1),sK622,sK623) != X0 )
| ( vnoRawTable = X0 ) ),
inference(superposition,[],[f1868,f975]) ).
tff(f2191,plain,
( ( sK627 = sK540(vacons(sK626,val1),sK627) )
| ~ spl628_25 ),
inference(resolution,[],[f2123,f1715]) ).
tff(f2200,plain,
( ( sK539(vacons(sK626,val1),sK627) = vfindColType(sK538(vacons(sK626,val1),sK627),sK627) )
| ~ sP60(vacons(sK626,val1),sK627)
| ~ spl628_25 ),
inference(superposition,[],[f1720,f2191]) ).
tff(f2201,plain,
( ( sK539(vacons(sK626,val1),sK627) = vfindColType(sK538(vacons(sK626,val1),sK627),sK627) )
| ~ spl628_25 ),
inference(forward_subsumption_resolution,[],[f2200,f2123]) ).
tff(f2211,plain,
vprojectType(vlist(val1),sK627) = vprojectType(vall,sK265(vprojectType(vlist(val1),sK627))),
inference(resolution,[],[f2114,f1884]) ).
tff(f2215,plain,
( $false
| ~ spl628_3 ),
inference(forward_subsumption_resolution,[],[f2211,f1966]) ).
tff(f2216,plain,
~ spl628_3,
inference(avatar_contradiction_clause,[],[f2215]) ).
tff(f2225,definition,
( spl628_28
<=> ! [X0: vAttrL] :
( ( vprojectCols(val1,X0,sK623) = vsomeRawTable(sK620(sK623,X0)) )
| ~ vmatchingAttrL(sK627,X0) ) ),
introduced(definition,[new_symbols(definition,[spl628_28])],[avatar_definition]) ).
tff(f2226,plain,
( ! [X0: vAttrL] :
( ~ vmatchingAttrL(sK627,X0)
| ( vprojectCols(val1,X0,sK623) = vsomeRawTable(sK620(sK623,X0)) ) )
| ~ spl628_28 ),
inference(avatar_component_clause,[],[f2225]) ).
tff(f2227,plain,
( spl628_3
| spl628_28 ),
inference(avatar_split_clause,[],[f2019,f2225,f1965]) ).
tff(f2257,definition,
( spl628_31
<=> visSomeRawTable(vfindCol(sK626,sK622,sK623)) ),
introduced(definition,[new_symbols(definition,[spl628_31])],[avatar_definition]) ).
tff(f2261,definition,
( spl628_32
<=> visSomeRawTable(vprojectCols(val1,sK622,sK623)) ),
introduced(definition,[new_symbols(definition,[spl628_32])],[avatar_definition]) ).
tff(f2302,plain,
vnoRawTable = vprojectCols(vacons(sK626,val1),sK622,sK623),
inference(equality_resolution,[],[f2140]) ).
tff(f2596,plain,
( ! [X2: vRawTable,X0: vFType,X1: vAttrL] :
( ( vsomeFType(X0) != sK539(vacons(sK626,val1),sK627) )
| ( vfindCol(sK538(vacons(sK626,val1),sK627),X1,X2) = vsomeRawTable(sK621(X2,X1,sK538(vacons(sK626,val1),sK627))) )
| ~ vwelltypedRawtable(sK627,X2)
| ~ vmatchingAttrL(sK627,X1) )
| ~ spl628_25 ),
inference(superposition,[],[f1861,f2201]) ).
tff(f2614,definition,
( spl628_60
<=> ! [X2: vRawTable,X1: vAttrL] :
( ( vfindCol(sK538(vacons(sK626,val1),sK627),X1,X2) = vsomeRawTable(sK621(X2,X1,sK538(vacons(sK626,val1),sK627))) )
| ~ vmatchingAttrL(sK627,X1)
| ~ vwelltypedRawtable(sK627,X2) ) ),
introduced(definition,[new_symbols(definition,[spl628_60])],[avatar_definition]) ).
tff(f2615,plain,
( ! [X2: vRawTable,X1: vAttrL] :
( ( vfindCol(sK538(vacons(sK626,val1),sK627),X1,X2) = vsomeRawTable(sK621(X2,X1,sK538(vacons(sK626,val1),sK627))) )
| ~ vmatchingAttrL(sK627,X1)
| ~ vwelltypedRawtable(sK627,X2) )
| ~ spl628_60 ),
inference(avatar_component_clause,[],[f2614]) ).
tff(f2617,definition,
( spl628_61
<=> ! [X0: vFType] : ( vsomeFType(X0) != sK539(vacons(sK626,val1),sK627) ) ),
introduced(definition,[new_symbols(definition,[spl628_61])],[avatar_definition]) ).
tff(f2618,plain,
( ! [X0: vFType] : ( vsomeFType(X0) != sK539(vacons(sK626,val1),sK627) )
| ~ spl628_61 ),
inference(avatar_component_clause,[],[f2617]) ).
tff(f2619,plain,
( spl628_60
| spl628_61
| ~ spl628_25 ),
inference(avatar_split_clause,[],[f2596,f2122,f2617,f2614]) ).
tff(f2669,plain,
( ( vaempty = vacons(sK626,val1) )
| sP60(vacons(sK626,val1),sK627) ),
inference(resolution,[],[f2117,f1723]) ).
tff(f2670,plain,
sP60(vacons(sK626,val1),sK627),
inference(forward_subsumption_resolution,[],[f2669,f1044]) ).
tff(f2771,plain,
( ( vnoRawTable != vnoRawTable )
| ~ visSomeRawTable(vfindCol(sK626,sK622,sK623))
| ~ visSomeRawTable(vprojectCols(val1,sK622,sK623)) ),
inference(superposition,[],[f2137,f2302]) ).
tff(f2774,plain,
( ~ visSomeRawTable(vfindCol(sK626,sK622,sK623))
| ~ visSomeRawTable(vprojectCols(val1,sK622,sK623)) ),
inference(trivial_inequality_removal,[],[f2771]) ).
tff(f3387,plain,
( ( vprojectCols(val1,sK622,sK623) = vsomeRawTable(sK620(sK623,sK622)) )
| ~ spl628_28 ),
inference(resolution,[],[f2226,f1865]) ).
tff(f4357,plain,
spl628_25,
inference(avatar_split_clause,[],[f2670,f2122]) ).
tff(f4399,plain,
( ( vacons(sK626,val1) = vacons(sK538(vacons(sK626,val1),sK627),sK541(vacons(sK626,val1),sK627)) )
| ~ spl628_25 ),
inference(resolution,[],[f2123,f1716]) ).
tff(f4401,plain,
( visSomeFType(sK539(vacons(sK626,val1),sK627))
| ~ spl628_25 ),
inference(resolution,[],[f2123,f1718]) ).
tff(f4506,plain,
( ! [X0: vName,X1: vAttrL] :
( ( vacons(X0,X1) != vacons(sK626,val1) )
| ( sK538(vacons(sK626,val1),sK627) = X0 ) )
| ~ spl628_25 ),
inference(superposition,[],[f1043,f4399]) ).
tff(f4557,plain,
( ( sK626 = sK538(vacons(sK626,val1),sK627) )
| ~ spl628_25 ),
inference(equality_resolution,[],[f4506]) ).
tff(f5240,plain,
( ( sK539(vacons(sK626,val1),sK627) = vsomeFType(sK523(sK539(vacons(sK626,val1),sK627))) )
| ~ spl628_25 ),
inference(resolution,[],[f4401,f1688]) ).
tff(f5242,plain,
( $false
| ~ spl628_25
| ~ spl628_61 ),
inference(forward_subsumption_resolution,[],[f5240,f2618]) ).
tff(f5243,plain,
( ~ spl628_25
| ~ spl628_61 ),
inference(avatar_contradiction_clause,[],[f5242]) ).
tff(f5247,plain,
( ! [X2: vRawTable,X1: vAttrL] :
( ~ vwelltypedRawtable(sK627,X2)
| ~ vmatchingAttrL(sK627,X1)
| ( vfindCol(sK626,X1,X2) = vsomeRawTable(sK621(X2,X1,sK626)) ) )
| ~ spl628_25
| ~ spl628_60 ),
inference(forward_demodulation,[],[f2615,f4557]) ).
tff(f5264,plain,
( ~ visSomeRawTable(vfindCol(sK626,sK622,sK623))
| spl628_31 ),
inference(avatar_component_clause,[],[f2257]) ).
tff(f5266,plain,
( ~ spl628_32
| ~ spl628_31 ),
inference(avatar_split_clause,[],[f2774,f2257,f2261]) ).
tff(f5284,plain,
( ( vnoRawTable = vfindCol(sK626,sK622,sK623) )
| spl628_31 ),
inference(resolution,[],[f5264,f1176]) ).
tff(f5508,plain,
( visSomeRawTable(vprojectCols(val1,sK622,sK623))
| ~ spl628_28 ),
inference(superposition,[],[f1174,f3387]) ).
tff(f5509,plain,
( spl628_32
| ~ spl628_28 ),
inference(avatar_split_clause,[],[f5508,f2225,f2261]) ).
tff(f5612,plain,
( ! [X0: vAttrL] :
( ~ vmatchingAttrL(sK627,X0)
| ( vfindCol(sK626,X0,sK623) = vsomeRawTable(sK621(sK623,X0,sK626)) ) )
| ~ spl628_25
| ~ spl628_60 ),
inference(resolution,[],[f5247,f1866]) ).
tff(f5620,plain,
( ( vfindCol(sK626,sK622,sK623) = vsomeRawTable(sK621(sK623,sK622,sK626)) )
| ~ spl628_25
| ~ spl628_60 ),
inference(resolution,[],[f5612,f1865]) ).
tff(f5626,plain,
( ( vnoRawTable = vsomeRawTable(sK621(sK623,sK622,sK626)) )
| ~ spl628_25
| spl628_31
| ~ spl628_60 ),
inference(forward_demodulation,[],[f5620,f5284]) ).
tff(f5627,plain,
( $false
| ~ spl628_25
| spl628_31
| ~ spl628_60 ),
inference(forward_subsumption_resolution,[],[f5626,f977]) ).
tff(f5628,plain,
( ~ spl628_25
| spl628_31
| ~ spl628_60 ),
inference(avatar_contradiction_clause,[],[f5627]) ).
cnf(s36,plain,
~ spl628_3,
inference(sat_conversion,[],[f2216]) ).
cnf(s38,plain,
( spl628_3
| spl628_28 ),
inference(sat_conversion,[],[f2227]) ).
cnf(s73,plain,
( ~ spl628_25
| spl628_60
| spl628_61 ),
inference(sat_conversion,[],[f2619]) ).
cnf(s134,plain,
spl628_25,
inference(sat_conversion,[],[f4357]) ).
cnf(s154,plain,
( ~ spl628_25
| ~ spl628_61 ),
inference(sat_conversion,[],[f5243]) ).
cnf(s157,plain,
( ~ spl628_31
| ~ spl628_32 ),
inference(sat_conversion,[],[f5266]) ).
cnf(s174,plain,
( ~ spl628_28
| spl628_32 ),
inference(sat_conversion,[],[f5509]) ).
cnf(s175,plain,
( ~ spl628_25
| spl628_31
| ~ spl628_60 ),
inference(sat_conversion,[],[f5628]) ).
cnf(s176,plain,
~ spl628_61,
inference(rat,[],[s154,s134]) ).
cnf(s184,plain,
spl628_60,
inference(rat,[],[s73,s176,s134]) ).
cnf(s185,plain,
spl628_31,
inference(rat,[],[s175,s134,s184]) ).
cnf(s186,plain,
~ spl628_32,
inference(rat,[],[s157,s185]) ).
cnf(s187,plain,
~ spl628_28,
inference(rat,[],[s174,s186]) ).
cnf(s194,plain,
spl628_3,
inference(rat,[],[s38,s187]) ).
cnf(s195,plain,
$false,
inference(rat,[],[s36,s194]) ).
tff(f5629,plain,
$false,
inference(avatar_sat_refutation,[],[s195]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM301_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.26 % Computer : n006.cluster.edu
% 0.09/0.26 % Model : x86_64 x86_64
% 0.09/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.26 % Memory : 8046.5625MB
% 0.09/0.26 % OS : Linux 6.8.0-71-generic
% 0.09/0.26 % CPULimit : 300
% 0.09/0.26 % WCLimit : 300
% 0.09/0.26 % DateTime : Mon Sep 28 22:04:25 UTC 2026
% 0.09/0.26 % CPUTime :
% 0.09/0.26 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.26/0.31 Running first-order theorem proving
% 0.26/0.31 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.15/3.12 % (263462)Detected formulas, will run a generic FOF schedule.
% 17.15/3.12 % (263477)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1445300909:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 17.15/3.12 % (263478)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2510814713:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 17.15/3.12 % (263477)Instruction limit reached!
% 17.15/3.12 % (263477)------------------------------
% 17.15/3.12 % (263477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.15/3.12 % (263477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.15/3.12 % (263477)CaDiCaL version: 2.1.3
% 17.15/3.12 % (263477)Termination reason: Instruction limit
% 17.15/3.12 % (263477)Termination phase: Saturation
% 17.15/3.12 % (263477)Time elapsed: 0.058 s
% 17.15/3.12 % (263477)Peak memory usage: 89 MB
% 17.15/3.12 % (263477)Instructions burned: 120 (million)
% 17.15/3.12 % (263479)dis-21_1_sil=8000:lcm=predicate:random_seed=4248703014:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 17.15/3.12 % (263476)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3835541689:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 17.15/3.12 % (263473)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=883643041:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 17.15/3.12 % (263475)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1726946831:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 17.15/3.12 % (263474)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3425120648:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 17.15/3.12 % (263476)Refutation not found, incomplete strategy
% 17.15/3.12 % (263476)------------------------------
% 17.15/3.12 % (263476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.15/3.12 % (263476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.15/3.12 % (263476)CaDiCaL version: 2.1.3
% 17.15/3.12 % (263476)Termination reason: Refutation not found, incomplete strategy
% 17.15/3.12 % (263476)Time elapsed: 0.006 s
% 17.15/3.12 % (263476)Peak memory usage: 89 MB
% 17.15/3.12 % (263476)Instructions burned: 4 (million)
% 17.15/3.12 % (263478)Instruction limit reached!
% 17.15/3.12 % (263478)------------------------------
% 17.15/3.12 % (263478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.15/3.12 % (263478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.15/3.12 % (263478)CaDiCaL version: 2.1.3
% 17.15/3.12 % (263478)Termination reason: Instruction limit
% 17.15/3.12 % (263478)Termination phase: Saturation
% 17.15/3.12 % (263478)Time elapsed: 0.099 s
% 17.15/3.12 % (263478)Peak memory usage: 90 MB
% 17.15/3.12 % (263478)Instructions burned: 139 (million)
% 17.15/3.12 % (263479)Instruction limit reached!
% 17.15/3.12 % (263479)------------------------------
% 17.15/3.12 % (263479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.15/3.12 % (263479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.15/3.12 % (263479)CaDiCaL version: 2.1.3
% 17.15/3.12 % (263479)Termination reason: Instruction limit
% 17.15/3.12 % (263479)Termination phase: Saturation
% 17.15/3.12 % (263479)Time elapsed: 0.122 s
% 17.15/3.12 % (263479)Peak memory usage: 91 MB
% 17.15/3.12 % (263479)Instructions burned: 130 (million)
% 17.15/3.12 % (263484)lrs+10_1_sil=8000:sp=occurrence:random_seed=1379924324:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 17.15/3.12 % (263490)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2851437075:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 17.15/3.12 % (263490)Instruction limit reached!
% 17.15/3.12 % (263490)------------------------------
% 17.15/3.12 % (263490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.15/3.12 % (263490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.15/3.12 % (263490)CaDiCaL version: 2.1.3
% 17.15/3.12 % (263490)Termination reason: Instruction limit
% 17.15/3.12 % (263490)Termination phase: Saturation
% 17.15/3.12 % (263490)Time elapsed: 0.069 s
% 27.10/4.65 % (263490)Peak memory usage: 90 MB
% 27.10/4.65 % (263490)Instructions burned: 158 (million)
% 27.10/4.65 % (263491)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3380176003:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 27.10/4.65 % (263476)------------------------------
% 27.10/4.65 % (263476)------------------------------
% 27.10/4.65 % (263496)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3890449313:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 27.10/4.65 % (263484)Instruction limit reached!
% 27.10/4.65 % (263484)------------------------------
% 27.10/4.65 % (263484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.10/4.65 % (263484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.10/4.65 % (263484)CaDiCaL version: 2.1.3
% 27.10/4.65 % (263484)Termination reason: Instruction limit
% 27.10/4.65 % (263484)Termination phase: Saturation
% 27.10/4.65 % (263484)Time elapsed: 0.281 s
% 27.10/4.65 % (263484)Peak memory usage: 91 MB
% 27.10/4.65 % (263484)Instructions burned: 285 (million)
% 27.10/4.65 % (263498)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=462985352:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 27.10/4.65 % (263491)Instruction limit reached!
% 27.10/4.65 % (263491)------------------------------
% 27.10/4.65 % (263491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.10/4.65 % (263491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.10/4.65 % (263491)CaDiCaL version: 2.1.3
% 27.10/4.65 % (263491)Termination reason: Instruction limit
% 27.10/4.65 % (263491)Termination phase: Saturation
% 27.10/4.65 % (263491)Time elapsed: 0.290 s
% 27.10/4.65 % (263491)Peak memory usage: 94 MB
% 27.10/4.65 % (263491)Instructions burned: 325 (million)
% 27.10/4.65 % (263496)Instruction limit reached!
% 27.10/4.65 % (263496)------------------------------
% 27.10/4.65 % (263496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.10/4.65 % (263496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.10/4.65 % (263496)CaDiCaL version: 2.1.3
% 27.10/4.65 % (263496)Termination reason: Instruction limit
% 27.10/4.65 % (263496)Termination phase: Saturation
% 27.10/4.65 % (263496)Time elapsed: 0.223 s
% 27.10/4.65 % (263496)Peak memory usage: 92 MB
% 27.10/4.65 % (263496)Instructions burned: 248 (million)
% 27.10/4.65 % (263500)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2915592907:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 27.10/4.65 % (263498)Instruction limit reached!
% 27.10/4.65 % (263498)------------------------------
% 27.10/4.65 % (263498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.10/4.65 % (263498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.10/4.65 % (263498)CaDiCaL version: 2.1.3
% 27.10/4.65 % (263498)Termination reason: Instruction limit
% 27.10/4.65 % (263498)Termination phase: Saturation
% 27.10/4.65 % (263498)Time elapsed: 0.177 s
% 27.10/4.65 % (263498)Peak memory usage: 92 MB
% 27.10/4.65 % (263498)Instructions burned: 294 (million)
% 27.10/4.65 % (263502)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1234403348:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 27.10/4.65 % (263503)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2513029638:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 27.10/4.65 % (263505)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1468681489:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 27.10/4.65 % (263505)Instruction limit reached!
% 27.10/4.65 % (263505)------------------------------
% 27.10/4.65 % (263505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.10/4.65 % (263505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.10/4.65 % (263505)CaDiCaL version: 2.1.3
% 27.10/4.65 % (263505)Termination reason: Instruction limit
% 27.10/4.65 % (263505)Termination phase: Saturation
% 27.10/4.65 % (263505)Time elapsed: 0.057 s
% 27.10/4.65 % (263505)Peak memory usage: 89 MB
% 27.10/4.65 % (263505)Instructions burned: 115 (million)
% 27.10/4.65 % (263502)Instruction limit reached!
% 27.10/4.65 % (263502)------------------------------
% 27.10/4.65 % (263502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.10/4.65 % (263502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.75/12.55 % (263502)CaDiCaL version: 2.1.3
% 83.75/12.55 % (263502)Termination reason: Instruction limit
% 83.75/12.55 % (263502)Termination phase: Saturation
% 83.75/12.55 % (263502)Time elapsed: 0.116 s
% 83.75/12.55 % (263502)Peak memory usage: 91 MB
% 83.75/12.55 % (263502)Instructions burned: 113 (million)
% 83.75/12.55 % (263503)Instruction limit reached!
% 83.75/12.55 % (263503)------------------------------
% 83.75/12.55 % (263503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.75/12.55 % (263503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.75/12.55 % (263503)CaDiCaL version: 2.1.3
% 83.75/12.55 % (263503)Termination reason: Instruction limit
% 83.75/12.55 % (263503)Termination phase: Saturation
% 83.75/12.55 % (263503)Time elapsed: 0.113 s
% 83.75/12.55 % (263503)Peak memory usage: 89 MB
% 83.75/12.55 % (263503)Instructions burned: 127 (million)
% 83.75/12.55 % (263512)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1170384058:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 83.75/12.55 % (263511)lrs+10_1_sil=8000:sp=occurrence:random_seed=548482187:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 83.75/12.55 % (263513)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3716651131:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 83.75/12.55 % (263512)Instruction limit reached!
% 83.75/12.55 % (263512)------------------------------
% 83.75/12.55 % (263512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.75/12.55 % (263512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.75/12.55 % (263512)CaDiCaL version: 2.1.3
% 83.75/12.55 % (263512)Termination reason: Instruction limit
% 83.75/12.55 % (263512)Termination phase: Saturation
% 83.75/12.55 % (263512)Time elapsed: 0.219 s
% 83.75/12.55 % (263512)Peak memory usage: 93 MB
% 83.75/12.55 % (263512)Instructions burned: 440 (million)
% 83.75/12.55 % (263519)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3815117233:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 83.75/12.55 % (263519)Instruction limit reached!
% 83.75/12.55 % (263519)------------------------------
% 83.75/12.55 % (263519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.75/12.55 % (263519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.75/12.55 % (263519)CaDiCaL version: 2.1.3
% 83.75/12.55 % (263519)Termination reason: Instruction limit
% 83.75/12.55 % (263519)Termination phase: Saturation
% 83.75/12.55 % (263519)Time elapsed: 0.056 s
% 83.75/12.55 % (263519)Peak memory usage: 90 MB
% 83.75/12.55 % (263519)Instructions burned: 136 (million)
% 83.75/12.55 % (263521)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=334646561:st=8:i=592:sd=3:ep=RST:ss=axioms_2982 on theBenchmark for (2982ds/592Mi)
% 83.75/12.55 % (263511)Instruction limit reached!
% 83.75/12.55 % (263511)------------------------------
% 83.75/12.55 % (263511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.75/12.55 % (263511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.75/12.55 % (263511)CaDiCaL version: 2.1.3
% 83.75/12.55 % (263511)Termination reason: Instruction limit
% 83.75/12.55 % (263511)Termination phase: Saturation
% 83.75/12.55 % (263511)Time elapsed: 0.861 s
% 83.75/12.55 % (263511)Peak memory usage: 97 MB
% 83.75/12.55 % (263511)Instructions burned: 907 (million)
% 83.75/12.55 % (263521)Instruction limit reached!
% 83.75/12.55 % (263521)------------------------------
% 83.75/12.55 % (263521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.75/12.55 % (263521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.75/12.55 % (263521)CaDiCaL version: 2.1.3
% 83.75/12.55 % (263521)Termination reason: Instruction limit
% 83.75/12.55 % (263521)Termination phase: Saturation
% 83.75/12.55 % (263521)Time elapsed: 0.279 s
% 83.75/12.55 % (263521)Peak memory usage: 92 MB
% 83.75/12.55 % (263521)Instructions burned: 594 (million)
% 83.75/12.55 % (263525)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2990109962:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/125Mi)
% 83.75/12.55 % (263524)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1965166632:st=3:i=13193:sd=3:ss=axioms_2977 on theBenchmark for (2977ds/13193Mi)
% 83.75/12.55 % (263525)Instruction limit reached!
% 83.75/12.55 % (263525)------------------------------
% 106.92/16.09 % (263525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263525)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263525)Termination reason: Instruction limit
% 106.92/16.09 % (263525)Termination phase: Saturation
% 106.92/16.09 % (263525)Time elapsed: 0.067 s
% 106.92/16.09 % (263525)Peak memory usage: 92 MB
% 106.92/16.09 % (263525)Instructions burned: 126 (million)
% 106.92/16.09 % (263528)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3379752297:i=134:gtgl=5:slsql=off:gtg=exists_sym_2975 on theBenchmark for (2975ds/134Mi)
% 106.92/16.09 % (263528)Instruction limit reached!
% 106.92/16.09 % (263528)------------------------------
% 106.92/16.09 % (263528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263528)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263528)Termination reason: Instruction limit
% 106.92/16.09 % (263528)Termination phase: Saturation
% 106.92/16.09 % (263528)Time elapsed: 0.101 s
% 106.92/16.09 % (263528)Peak memory usage: 91 MB
% 106.92/16.09 % (263528)Instructions burned: 134 (million)
% 106.92/16.09 % (263530)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4282088567:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/141Mi)
% 106.92/16.09 % (263530)Refutation not found, incomplete strategy
% 106.92/16.09 % (263530)------------------------------
% 106.92/16.09 % (263530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263530)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263530)Termination reason: Refutation not found, incomplete strategy
% 106.92/16.09 % (263530)Time elapsed: 0.008 s
% 106.92/16.09 % (263530)Peak memory usage: 89 MB
% 106.92/16.09 % (263530)Instructions burned: 9 (million)
% 106.92/16.09 % (263530)------------------------------
% 106.92/16.09 % (263530)------------------------------
% 106.92/16.09 % (263534)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3610535450:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2968 on theBenchmark for (2968ds/431Mi)
% 106.92/16.09 % (263534)Refutation not found, incomplete strategy
% 106.92/16.09 % (263534)------------------------------
% 106.92/16.09 % (263534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263534)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263534)Termination reason: Refutation not found, incomplete strategy
% 106.92/16.09 % (263534)Time elapsed: 0.010 s
% 106.92/16.09 % (263534)Peak memory usage: 89 MB
% 106.92/16.09 % (263534)Instructions burned: 13 (million)
% 106.92/16.09 % (263500)Instruction limit reached!
% 106.92/16.09 % (263500)------------------------------
% 106.92/16.09 % (263500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263500)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263500)Termination reason: Instruction limit
% 106.92/16.09 % (263500)Termination phase: Saturation
% 106.92/16.09 % (263500)Time elapsed: 2.361 s
% 106.92/16.09 % (263500)Peak memory usage: 143 MB
% 106.92/16.09 % (263500)Instructions burned: 2350 (million)
% 106.92/16.09 % (263536)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2172349398:i=6060:aac=none:ins=25_2966 on theBenchmark for (2966ds/6060Mi)
% 106.92/16.09 % (263534)------------------------------
% 106.92/16.09 % (263534)------------------------------
% 106.92/16.09 % (263540)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3947554996:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2963 on theBenchmark for (2963ds/150Mi)
% 106.92/16.09 % (263540)Instruction limit reached!
% 106.92/16.09 % (263540)------------------------------
% 106.92/16.09 % (263540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263540)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263540)Termination reason: Instruction limit
% 106.92/16.09 % (263540)Termination phase: Saturation
% 106.92/16.09 % (263540)Time elapsed: 0.080 s
% 106.92/16.09 % (263540)Peak memory usage: 92 MB
% 106.92/16.09 % (263540)Instructions burned: 151 (million)
% 106.92/16.09 % (263542)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1551506581:i=14155:bd=all_2960 on theBenchmark for (2960ds/14155Mi)
% 106.92/16.09 % (263513)Instruction limit reached!
% 106.92/16.09 % (263513)------------------------------
% 106.92/16.09 % (263513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263513)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263513)Termination reason: Instruction limit
% 106.92/16.09 % (263513)Termination phase: Saturation
% 106.92/16.09 % (263513)Time elapsed: 5.032 s
% 106.92/16.09 % (263513)Peak memory usage: 157 MB
% 106.92/16.09 % (263513)Instructions burned: 5202 (million)
% 106.92/16.09 % (263548)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3786846065:i=667:av=off:fsr=off_2935 on theBenchmark for (2935ds/667Mi)
% 106.92/16.09 % (263548)Instruction limit reached!
% 106.92/16.09 % (263548)------------------------------
% 106.92/16.09 % (263548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263548)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263548)Termination reason: Instruction limit
% 106.92/16.09 % (263548)Termination phase: Saturation
% 106.92/16.09 % (263548)Time elapsed: 0.537 s
% 106.92/16.09 % (263548)Peak memory usage: 104 MB
% 106.92/16.09 % (263548)Instructions burned: 667 (million)
% 106.92/16.09 % (263552)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3426843061:s2a=on:i=185:s2at=1.8:fdi=4_2927 on theBenchmark for (2927ds/185Mi)
% 106.92/16.09 % (263552)Instruction limit reached!
% 106.92/16.09 % (263552)------------------------------
% 106.92/16.09 % (263552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263552)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263552)Termination reason: Instruction limit
% 106.92/16.09 % (263552)Termination phase: Saturation
% 106.92/16.09 % (263552)Time elapsed: 0.153 s
% 106.92/16.09 % (263552)Peak memory usage: 91 MB
% 106.92/16.09 % (263552)Instructions burned: 185 (million)
% 106.92/16.09 % (263554)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1720466613:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2924 on theBenchmark for (2924ds/193Mi)
% 106.92/16.09 % (263554)Instruction limit reached!
% 106.92/16.09 % (263554)------------------------------
% 106.92/16.09 % (263554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263554)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263554)Termination reason: Instruction limit
% 106.92/16.09 % (263554)Termination phase: Saturation
% 106.92/16.09 % (263554)Time elapsed: 0.192 s
% 106.92/16.09 % (263554)Peak memory usage: 90 MB
% 106.92/16.09 % (263554)Instructions burned: 193 (million)
% 106.92/16.09 % (263556)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2131700278:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2920 on theBenchmark for (2920ds/4850Mi)
% 106.92/16.09 % (263536)Instruction limit reached!
% 106.92/16.09 % (263536)------------------------------
% 106.92/16.09 % (263536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263536)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263536)Termination reason: Instruction limit
% 106.92/16.09 % (263536)Termination phase: Saturation
% 106.92/16.09 % (263536)Time elapsed: 5.995 s
% 106.92/16.09 % (263536)Peak memory usage: 173 MB
% 106.92/16.09 % (263536)Instructions burned: 6061 (million)
% 106.92/16.09 % (263560)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4282234977:i=12111:sd=1:ss=included_2904 on theBenchmark for (2904ds/12111Mi)
% 106.92/16.09 % (263542)Instruction limit reached!
% 106.92/16.09 % (263542)------------------------------
% 106.92/16.09 % (263542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263542)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263542)Termination reason: Instruction limit
% 106.92/16.09 % (263542)Termination phase: Saturation
% 106.92/16.09 % (263542)Time elapsed: 7.737 s
% 106.92/16.09 % (263542)Peak memory usage: 200 MB
% 106.92/16.09 % (263542)Instructions burned: 14158 (million)
% 106.92/16.09 % (263566)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2802677540:i=319:kws=precedence:fsr=off_2881 on theBenchmark for (2881ds/319Mi)
% 106.92/16.09 % (263566)Instruction limit reached!
% 106.92/16.09 % (263566)------------------------------
% 106.92/16.09 % (263566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263566)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263566)Termination reason: Instruction limit
% 106.92/16.09 % (263566)Termination phase: Saturation
% 106.92/16.09 % (263566)Time elapsed: 0.185 s
% 106.92/16.09 % (263566)Peak memory usage: 94 MB
% 106.92/16.09 % (263566)Instructions burned: 320 (million)
% 106.92/16.09 % (263568)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3963046300:i=2064:ep=RST_2877 on theBenchmark for (2877ds/2064Mi)
% 106.92/16.09 % (263556)Instruction limit reached!
% 106.92/16.09 % (263556)------------------------------
% 106.92/16.09 % (263556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263556)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263556)Termination reason: Instruction limit
% 106.92/16.09 % (263556)Termination phase: Saturation
% 106.92/16.09 % (263556)Time elapsed: 4.396 s
% 106.92/16.09 % (263556)Peak memory usage: 127 MB
% 106.92/16.09 % (263556)Instructions burned: 4850 (million)
% 106.92/16.09 % (263570)dis-1011_128_sil=32000:random_seed=3005405566:i=3706:ep=RST:av=off_2873 on theBenchmark for (2873ds/3706Mi)
% 106.92/16.09 % (263524)Instruction limit reached!
% 106.92/16.09 % (263524)------------------------------
% 106.92/16.09 % (263524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263524)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263524)Termination reason: Instruction limit
% 106.92/16.09 % (263524)Termination phase: Saturation
% 106.92/16.09 % (263524)Time elapsed: 10.390 s
% 106.92/16.09 % (263524)Peak memory usage: 157 MB
% 106.92/16.09 % (263524)Instructions burned: 13193 (million)
% 106.92/16.09 % (263572)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3832071858:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2871 on theBenchmark for (2871ds/757Mi)
% 106.92/16.09 % (263568)Instruction limit reached!
% 106.92/16.09 % (263568)------------------------------
% 106.92/16.09 % (263568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263568)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263568)Termination reason: Instruction limit
% 106.92/16.09 % (263568)Termination phase: Saturation
% 106.92/16.09 % (263568)Time elapsed: 0.877 s
% 106.92/16.09 % (263568)Peak memory usage: 95 MB
% 106.92/16.09 % (263568)Instructions burned: 2067 (million)
% 106.92/16.09 % (263574)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3895344087:i=13913:ss=axioms:sgt=8_2867 on theBenchmark for (2867ds/13913Mi)
% 106.92/16.09 % (263572)Instruction limit reached!
% 106.92/16.09 % (263572)------------------------------
% 106.92/16.09 % (263572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.92/16.09 % (263572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.92/16.09 % (263572)CaDiCaL version: 2.1.3
% 106.92/16.09 % (263572)Termination reason: Instruction limit
% 106.92/16.09 % (263572)Termination phase: Saturation
% 106.92/16.09 % (263572)Time elapsed: 0.515 s
% 106.92/16.09 % (263572)Peak memory usage: 96 MB
% 106.92/16.09 % (263572)Instructions burned: 760 (million)
% 106.92/16.09 % (263576)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1874937746:i=9925:aac=none_2864 on theBenchmark for (2864ds/9925Mi)
% 106.92/16.09 % (263576)First to succeed.
% 106.92/16.09 % (263576)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-263462"
% 106.92/16.09 % (263576)Refutation found. Thanks to Tanya!
% 106.92/16.09 % SZS status Theorem for theBenchmark
% 106.92/16.09 % SZS output start Proof for theBenchmark
% See solution above
% 108.86/16.29 % (263576)------------------------------
% 108.86/16.29 % (263576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.86/16.29 % (263576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.86/16.29 % (263576)CaDiCaL version: 2.1.3
% 108.86/16.29 % (263576)Termination reason: Refutation
% 108.86/16.29 % (263576)Time elapsed: 1.203 s
% 108.86/16.29 % (263576)Peak memory usage: 142 MB
% 108.86/16.29 % (263576)Instructions burned: 1757 (million)
% 108.86/16.29 % (263576)------------------------------
% 108.86/16.29 % (263576)------------------------------
% 108.86/16.29 % (263462)Success in time 15.407 s
% 108.86/16.29 % Vampire exiting
%------------------------------------------------------------------------------