%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : COM302_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 : n008.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 27.57s 8.21s
% Output : Refutation 52.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 47
% Syntax : Number of formulae : 256 ( 51 unt; 0 typ; 30 def)
% Number of atoms : 693 ( 232 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 746 ( 309 ~; 294 |; 104 &)
% ( 29 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 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 : 139 ( 137 usr; 28 prp; 0-4 aty)
% Number of functors : 629 ( 629 usr; 24 con; 0-5 aty)
% Number of variables : 320 ( 0 sgn 246 !; 74 ?; 315 :)
% 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,
sK49: vSelect > vAttrL ).
tff(func_def_78,type,
sK50: vQuery > vTable ).
tff(func_def_79,type,
sK51: vQuery > vSelect ).
tff(func_def_80,type,
sK52: vQuery > vName ).
tff(func_def_81,type,
sK53: vQuery > vPred ).
tff(func_def_82,type,
sK54: vQuery > vQuery ).
tff(func_def_83,type,
sK55: vQuery > vQuery ).
tff(func_def_84,type,
sK56: vQuery > vQuery ).
tff(func_def_85,type,
sK57: vQuery > vQuery ).
tff(func_def_86,type,
sK58: vQuery > vQuery ).
tff(func_def_87,type,
sK59: vQuery > vQuery ).
tff(func_def_88,type,
sK60: vOptTable > vTable ).
tff(func_def_89,type,
sK61: vTType > vName ).
tff(func_def_90,type,
sK62: vTType > vFType ).
tff(func_def_91,type,
sK63: vTType > vTType ).
tff(func_def_92,type,
sK64: vTTContext > vName ).
tff(func_def_93,type,
sK65: vTTContext > vTType ).
tff(func_def_94,type,
sK66: vTTContext > vTTContext ).
tff(func_def_95,type,
sK67: vOptRawTable > vRawTable ).
tff(func_def_96,type,
sK68: vOptTType > vTType ).
tff(func_def_97,type,
sK69: vRow > vVal ).
tff(func_def_98,type,
sK70: vRow > vRow ).
tff(func_def_99,type,
sK71: vRawTable > vRow ).
tff(func_def_100,type,
sK72: vRawTable > vRawTable ).
tff(func_def_101,type,
sK73: vOptQuery > vQuery ).
tff(func_def_102,type,
sK74: vExp > vVal ).
tff(func_def_103,type,
sK75: vExp > vName ).
tff(func_def_104,type,
sK76: vTable > vAttrL ).
tff(func_def_105,type,
sK77: vTable > vRawTable ).
tff(func_def_106,type,
sK78: vOptVal > vVal ).
tff(func_def_107,type,
sK79: vPred > vPred ).
tff(func_def_108,type,
sK80: vPred > vPred ).
tff(func_def_109,type,
sK81: vPred > vPred ).
tff(func_def_110,type,
sK82: vPred > vExp ).
tff(func_def_111,type,
sK83: vPred > vExp ).
tff(func_def_112,type,
sK84: vPred > vExp ).
tff(func_def_113,type,
sK85: vPred > vExp ).
tff(func_def_114,type,
sK86: vPred > vExp ).
tff(func_def_115,type,
sK87: vPred > vExp ).
tff(func_def_116,type,
sK88: vTStore > vName ).
tff(func_def_117,type,
sK89: vTStore > vTable ).
tff(func_def_118,type,
sK90: vTStore > vTStore ).
tff(func_def_119,type,
sK91: vOptFType > vFType ).
tff(func_def_120,type,
sK92: vAttrL > vName ).
tff(func_def_121,type,
sK93: vAttrL > vAttrL ).
tff(func_def_122,type,
sK94: ( vAttrL * vAttrL ) > vAttrL ).
tff(func_def_123,type,
sK95: ( vAttrL * vAttrL ) > vName ).
tff(func_def_124,type,
sK96: ( vAttrL * vAttrL ) > vAttrL ).
tff(func_def_125,type,
sK97: ( vAttrL * vAttrL ) > vAttrL ).
tff(func_def_126,type,
sK98: vTable > vAttrL ).
tff(func_def_127,type,
sK99: vTable > vRawTable ).
tff(func_def_128,type,
sK100: vTable > vAttrL ).
tff(func_def_129,type,
sK101: vTable > vRawTable ).
tff(func_def_130,type,
sK102: vTType > vName ).
tff(func_def_131,type,
sK103: vTType > vFType ).
tff(func_def_132,type,
sK104: vTType > vTType ).
tff(func_def_133,type,
sK105: vAttrL > vName ).
tff(func_def_134,type,
sK106: vAttrL > vAttrL ).
tff(func_def_135,type,
sK107: ( vTType * vAttrL ) > vTType ).
tff(func_def_136,type,
sK108: ( vTType * vAttrL ) > vName ).
tff(func_def_137,type,
sK109: ( vTType * vAttrL ) > vFType ).
tff(func_def_138,type,
sK110: ( vTType * vAttrL ) > vName ).
tff(func_def_139,type,
sK111: ( vTType * vAttrL ) > vAttrL ).
tff(func_def_140,type,
sK112: ( vTType * vAttrL ) > vTType ).
tff(func_def_141,type,
sK113: ( vTType * vAttrL ) > vName ).
tff(func_def_142,type,
sK114: ( vTType * vAttrL ) > vFType ).
tff(func_def_143,type,
sK115: ( vTType * vAttrL ) > vName ).
tff(func_def_144,type,
sK116: ( vTType * vAttrL ) > vAttrL ).
tff(func_def_145,type,
sK117: ( vTType * vAttrL ) > vTType ).
tff(func_def_146,type,
sK118: ( vTType * vAttrL ) > vAttrL ).
tff(func_def_147,type,
sK119: vTType > vName ).
tff(func_def_148,type,
sK120: vTType > vFType ).
tff(func_def_149,type,
sK121: vTType > vTType ).
tff(func_def_150,type,
sK122: vRow > vVal ).
tff(func_def_151,type,
sK123: vRow > vRow ).
tff(func_def_152,type,
sK124: ( vTType * vRow ) > vVal ).
tff(func_def_153,type,
sK125: ( vTType * vRow ) > vTType ).
tff(func_def_154,type,
sK126: ( vTType * vRow ) > vFType ).
tff(func_def_155,type,
sK127: ( vTType * vRow ) > vName ).
tff(func_def_156,type,
sK128: ( vTType * vRow ) > vRow ).
tff(func_def_157,type,
sK129: ( vTType * vRow ) > vVal ).
tff(func_def_158,type,
sK130: ( vTType * vRow ) > vTType ).
tff(func_def_159,type,
sK131: ( vTType * vRow ) > vFType ).
tff(func_def_160,type,
sK132: ( vTType * vRow ) > vName ).
tff(func_def_161,type,
sK133: ( vTType * vRow ) > vRow ).
tff(func_def_162,type,
sK134: ( vTType * vRow ) > vTType ).
tff(func_def_163,type,
sK135: ( vTType * vRow ) > vRow ).
tff(func_def_164,type,
sK136: ( vTType * vRawTable ) > vTType ).
tff(func_def_165,type,
sK137: ( vTType * vRawTable ) > vRow ).
tff(func_def_166,type,
sK138: ( vTType * vRawTable ) > vRawTable ).
tff(func_def_167,type,
sK139: ( vTType * vRawTable ) > vTType ).
tff(func_def_168,type,
sK140: ( vTType * vRawTable ) > vRow ).
tff(func_def_169,type,
sK141: ( vTType * vRawTable ) > vRawTable ).
tff(func_def_170,type,
sK142: ( vTType * vRawTable ) > vTType ).
tff(func_def_171,type,
sK143: ( vTType * vTable ) > vTType ).
tff(func_def_172,type,
sK144: ( vTType * vTable ) > vAttrL ).
tff(func_def_173,type,
sK145: ( vTType * vTable ) > vRawTable ).
tff(func_def_174,type,
sK146: ( vTType * vTable ) > vTType ).
tff(func_def_175,type,
sK147: ( vTType * vTable ) > vAttrL ).
tff(func_def_176,type,
sK148: ( vTType * vTable ) > vRawTable ).
tff(func_def_177,type,
sK149: ( vRow * vRawTable ) > vRow ).
tff(func_def_178,type,
sK150: ( vRow * vRawTable ) > vRawTable ).
tff(func_def_179,type,
sK151: ( vRow * vRawTable ) > vRow ).
tff(func_def_180,type,
sK152: ( vRow * vRawTable ) > vRow ).
tff(func_def_181,type,
sK153: ( vRow * vRawTable ) > vRow ).
tff(func_def_182,type,
sK154: ( vRow * vRawTable ) > vRawTable ).
tff(func_def_183,type,
sK155: ( vRow * vRawTable ) > vRow ).
tff(func_def_184,type,
sK156: vRawTable > vRawTable ).
tff(func_def_185,type,
sK157: vRawTable > vVal ).
tff(func_def_186,type,
sK158: vRawTable > vRow ).
tff(func_def_187,type,
sK159: vRawTable > vRawTable ).
tff(func_def_188,type,
sK160: vRawTable > vRawTable ).
tff(func_def_189,type,
sK161: vRawTable > vVal ).
tff(func_def_190,type,
sK162: vRawTable > vRow ).
tff(func_def_191,type,
sK163: vRawTable > vRawTable ).
tff(func_def_192,type,
sK164: vOptRawTable > vRawTable ).
tff(func_def_193,type,
sK165: vRawTable > vRow ).
tff(func_def_194,type,
sK166: vRawTable > vRawTable ).
tff(func_def_195,type,
sK167: vRawTable > vRow ).
tff(func_def_196,type,
sK168: vRawTable > vRawTable ).
tff(func_def_197,type,
sK169: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_198,type,
sK170: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_199,type,
sK171: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_200,type,
sK172: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_201,type,
sK173: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_202,type,
sK174: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_203,type,
sK175: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_204,type,
sK176: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_205,type,
sK177: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_206,type,
sK178: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_207,type,
sK179: vRawTable > vVal ).
tff(func_def_208,type,
sK180: vRawTable > vRawTable ).
tff(func_def_209,type,
sK181: vRawTable > vRow ).
tff(func_def_210,type,
sK182: vRawTable > vRawTable ).
tff(func_def_211,type,
sK183: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_212,type,
sK184: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_213,type,
sK185: ( vRawTable * vRawTable ) > vVal ).
tff(func_def_214,type,
sK186: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_215,type,
sK187: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_216,type,
sK188: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_217,type,
sK189: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_218,type,
sK190: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_219,type,
sK191: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_220,type,
sK192: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_221,type,
sK193: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_222,type,
sK194: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_223,type,
sK195: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_224,type,
sK196: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_225,type,
sK197: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_226,type,
sK198: ( vRow * vRawTable ) > vRow ).
tff(func_def_227,type,
sK199: ( vRow * vRawTable ) > vRow ).
tff(func_def_228,type,
sK200: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_229,type,
sK201: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_230,type,
sK202: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_231,type,
sK203: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_232,type,
sK204: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_233,type,
sK205: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_234,type,
sK206: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_235,type,
sK207: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_236,type,
sK208: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_237,type,
sK209: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_238,type,
sK210: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_239,type,
sK211: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_240,type,
sK212: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_241,type,
sK213: ( vRow * vRawTable ) > vRow ).
tff(func_def_242,type,
sK214: ( vRow * vRawTable ) > vRow ).
tff(func_def_243,type,
sK215: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_244,type,
sK216: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_245,type,
sK217: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_246,type,
sK218: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_247,type,
sK219: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_248,type,
sK220: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_249,type,
sK221: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_250,type,
sK222: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_251,type,
sK223: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_252,type,
sK224: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_253,type,
sK225: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_254,type,
sK226: ( vRawTable * vRawTable ) > vRow ).
tff(func_def_255,type,
sK227: ( vRawTable * vRawTable ) > vRawTable ).
tff(func_def_256,type,
sK228: vOptTable > vTable ).
tff(func_def_257,type,
sK229: ( vName * vTStore ) > vName ).
tff(func_def_258,type,
sK230: ( vName * vTStore ) > vTable ).
tff(func_def_259,type,
sK231: ( vName * vTStore ) > vTStore ).
tff(func_def_260,type,
sK232: ( vName * vTStore ) > vName ).
tff(func_def_261,type,
sK233: ( vName * vTStore ) > vName ).
tff(func_def_262,type,
sK234: ( vName * vTStore ) > vName ).
tff(func_def_263,type,
sK235: ( vName * vTStore ) > vTable ).
tff(func_def_264,type,
sK236: ( vName * vTStore ) > vTStore ).
tff(func_def_265,type,
sK237: ( vName * vTStore ) > vName ).
tff(func_def_266,type,
sK238: vOptTType > vTType ).
tff(func_def_267,type,
sK239: ( vName * vTTContext ) > vName ).
tff(func_def_268,type,
sK240: ( vName * vTTContext ) > vTType ).
tff(func_def_269,type,
sK241: ( vName * vTTContext ) > vTTContext ).
tff(func_def_270,type,
sK242: ( vName * vTTContext ) > vName ).
tff(func_def_271,type,
sK243: ( vName * vTTContext ) > vName ).
tff(func_def_272,type,
sK244: ( vName * vTTContext ) > vName ).
tff(func_def_273,type,
sK245: ( vName * vTTContext ) > vTType ).
tff(func_def_274,type,
sK246: ( vName * vTTContext ) > vTTContext ).
tff(func_def_275,type,
sK247: ( vName * vTTContext ) > vName ).
tff(func_def_276,type,
sK248: vQuery > vTable ).
tff(func_def_277,type,
sK249: vQuery > vSelect ).
tff(func_def_278,type,
sK250: vQuery > vName ).
tff(func_def_279,type,
sK251: vQuery > vPred ).
tff(func_def_280,type,
sK252: vQuery > vQuery ).
tff(func_def_281,type,
sK253: vQuery > vQuery ).
tff(func_def_282,type,
sK254: vQuery > vQuery ).
tff(func_def_283,type,
sK255: vQuery > vQuery ).
tff(func_def_284,type,
sK256: vQuery > vQuery ).
tff(func_def_285,type,
sK257: vQuery > vQuery ).
tff(func_def_286,type,
sK258: vOptQuery > vQuery ).
tff(func_def_287,type,
sK259: ( vName * vAttrL * vRawTable ) > vName ).
tff(func_def_288,type,
sK260: ( vName * vAttrL * vRawTable ) > vAttrL ).
tff(func_def_289,type,
sK261: ( vName * vAttrL * vRawTable ) > vName ).
tff(func_def_290,type,
sK262: ( vName * vAttrL * vRawTable ) > vRawTable ).
tff(func_def_291,type,
sK263: ( vName * vAttrL * vRawTable ) > vName ).
tff(func_def_292,type,
sK264: ( vName * vAttrL * vRawTable ) > vRawTable ).
tff(func_def_293,type,
sK265: ( vName * vAttrL * vRawTable ) > vName ).
tff(func_def_294,type,
sK266: ( vName * vAttrL * vRawTable ) > vAttrL ).
tff(func_def_295,type,
sK267: ( vName * vAttrL * vRawTable ) > vName ).
tff(func_def_296,type,
sK268: ( vName * vAttrL * vRawTable ) > vRawTable ).
tff(func_def_297,type,
sK269: vRawTable > vRow ).
tff(func_def_298,type,
sK270: vRawTable > vRawTable ).
tff(func_def_299,type,
sK271: ( vAttrL * vAttrL * vRawTable ) > vRawTable ).
tff(func_def_300,type,
sK272: ( vAttrL * vAttrL * vRawTable ) > vOptRawTable ).
tff(func_def_301,type,
sK273: ( vAttrL * vAttrL * vRawTable ) > vOptRawTable ).
tff(func_def_302,type,
sK274: ( vAttrL * vAttrL * vRawTable ) > vAttrL ).
tff(func_def_303,type,
sK275: ( vAttrL * vAttrL * vRawTable ) > vAttrL ).
tff(func_def_304,type,
sK276: ( vAttrL * vAttrL * vRawTable ) > vName ).
tff(func_def_305,type,
sK277: ( vAttrL * vAttrL * vRawTable ) > vAttrL ).
tff(func_def_306,type,
sK278: ( vAttrL * vAttrL * vRawTable ) > vRawTable ).
tff(func_def_307,type,
sK279: ( vAttrL * vAttrL * vRawTable ) > vRawTable ).
tff(func_def_308,type,
sK280: ( vAttrL * vAttrL * vRawTable ) > vOptRawTable ).
tff(func_def_309,type,
sK281: ( vAttrL * vAttrL * vRawTable ) > vOptRawTable ).
tff(func_def_310,type,
sK282: ( vAttrL * vAttrL * vRawTable ) > vAttrL ).
tff(func_def_311,type,
sK283: ( vAttrL * vAttrL * vRawTable ) > vAttrL ).
tff(func_def_312,type,
sK284: ( vAttrL * vAttrL * vRawTable ) > vName ).
tff(func_def_313,type,
sK285: ( vSelect * vTable ) > vAttrL ).
tff(func_def_314,type,
sK286: ( vSelect * vTable ) > vOptRawTable ).
tff(func_def_315,type,
sK287: ( vSelect * vTable ) > vTable ).
tff(func_def_316,type,
sK288: ( vSelect * vTable ) > vTable ).
tff(func_def_317,type,
sK289: ( vSelect * vTable ) > vAttrL ).
tff(func_def_318,type,
sK290: ( vSelect * vTable ) > vOptRawTable ).
tff(func_def_319,type,
sK291: ( vSelect * vTable ) > vTable ).
tff(func_def_320,type,
sK292: vOptVal > vVal ).
tff(func_def_321,type,
sK293: vExp > vVal ).
tff(func_def_322,type,
sK294: vExp > vName ).
tff(func_def_323,type,
sK295: vAttrL > vName ).
tff(func_def_324,type,
sK296: vAttrL > vAttrL ).
tff(func_def_325,type,
sK297: vRow > vVal ).
tff(func_def_326,type,
sK298: vRow > vRow ).
tff(func_def_327,type,
sK299: ( vExp * vAttrL * vRow ) > vVal ).
tff(func_def_328,type,
sK300: ( vExp * vAttrL * vRow ) > vName ).
tff(func_def_329,type,
sK301: ( vExp * vAttrL * vRow ) > vName ).
tff(func_def_330,type,
sK302: ( vExp * vAttrL * vRow ) > vRow ).
tff(func_def_331,type,
sK303: ( vExp * vAttrL * vRow ) > vAttrL ).
tff(func_def_332,type,
sK304: ( vExp * vAttrL * vRow ) > vExp ).
tff(func_def_333,type,
sK305: ( vExp * vAttrL * vRow ) > vAttrL ).
tff(func_def_334,type,
sK306: ( vExp * vAttrL * vRow ) > vRow ).
tff(func_def_335,type,
sK307: ( vExp * vAttrL * vRow ) > vVal ).
tff(func_def_336,type,
sK308: ( vExp * vAttrL * vRow ) > vAttrL ).
tff(func_def_337,type,
sK309: ( vExp * vAttrL * vRow ) > vRow ).
tff(func_def_338,type,
sK310: ( vExp * vAttrL * vRow ) > vVal ).
tff(func_def_339,type,
sK311: ( vExp * vAttrL * vRow ) > vName ).
tff(func_def_340,type,
sK312: ( vExp * vAttrL * vRow ) > vName ).
tff(func_def_341,type,
sK313: ( vExp * vAttrL * vRow ) > vRow ).
tff(func_def_342,type,
sK314: ( vExp * vAttrL * vRow ) > vAttrL ).
tff(func_def_343,type,
sK315: ( vPred * vAttrL * vRow ) > vPred ).
tff(func_def_344,type,
sK316: ( vPred * vAttrL * vRow ) > vPred ).
tff(func_def_345,type,
sK317: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_346,type,
sK318: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_347,type,
sK319: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_348,type,
sK320: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_349,type,
sK321: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_350,type,
sK322: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_351,type,
sK323: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_352,type,
sK324: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_353,type,
sK325: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_354,type,
sK326: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_355,type,
sK327: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_356,type,
sK328: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_357,type,
sK329: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_358,type,
sK330: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_359,type,
sK331: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_360,type,
sK332: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_361,type,
sK333: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_362,type,
sK334: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_363,type,
sK335: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_364,type,
sK336: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_365,type,
sK337: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_366,type,
sK338: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_367,type,
sK339: ( vPred * vAttrL * vRow ) > vPred ).
tff(func_def_368,type,
sK340: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_369,type,
sK341: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_370,type,
sK342: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_371,type,
sK343: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_372,type,
sK344: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_373,type,
sK345: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_374,type,
sK346: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_375,type,
sK347: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_376,type,
sK348: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_377,type,
sK349: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_378,type,
sK350: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_379,type,
sK351: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_380,type,
sK352: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_381,type,
sK353: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_382,type,
sK354: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_383,type,
sK355: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_384,type,
sK356: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_385,type,
sK357: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_386,type,
sK358: ( vPred * vAttrL * vRow ) > vOptVal ).
tff(func_def_387,type,
sK359: ( vPred * vAttrL * vRow ) > vExp ).
tff(func_def_388,type,
sK360: ( vPred * vAttrL * vRow ) > vPred ).
tff(func_def_389,type,
sK361: ( vPred * vAttrL * vRow ) > vPred ).
tff(func_def_390,type,
sK362: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_391,type,
sK363: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_392,type,
sK364: ( vPred * vAttrL * vRow ) > vPred ).
tff(func_def_393,type,
sK365: ( vPred * vAttrL * vRow ) > vAttrL ).
tff(func_def_394,type,
sK366: ( vPred * vAttrL * vRow ) > vRow ).
tff(func_def_395,type,
sK367: ( vRawTable * vAttrL * vPred ) > vPred ).
tff(func_def_396,type,
sK368: ( vRawTable * vAttrL * vPred ) > vRow ).
tff(func_def_397,type,
sK369: ( vRawTable * vAttrL * vPred ) > vRawTable ).
tff(func_def_398,type,
sK370: ( vRawTable * vAttrL * vPred ) > vAttrL ).
tff(func_def_399,type,
sK371: ( vRawTable * vAttrL * vPred ) > vRawTable ).
tff(func_def_400,type,
sK372: ( vRawTable * vAttrL * vPred ) > vAttrL ).
tff(func_def_401,type,
sK373: ( vRawTable * vAttrL * vPred ) > vPred ).
tff(func_def_402,type,
sK374: ( vRawTable * vAttrL * vPred ) > vPred ).
tff(func_def_403,type,
sK375: ( vRawTable * vAttrL * vPred ) > vRow ).
tff(func_def_404,type,
sK376: ( vRawTable * vAttrL * vPred ) > vRawTable ).
tff(func_def_405,type,
sK377: ( vRawTable * vAttrL * vPred ) > vAttrL ).
tff(func_def_406,type,
sK378: ( vRawTable * vAttrL * vPred ) > vRawTable ).
tff(func_def_407,type,
sK379: ( vTable * vPred ) > vAttrL ).
tff(func_def_408,type,
sK380: ( vTable * vPred ) > vRawTable ).
tff(func_def_409,type,
sK381: ( vTable * vPred ) > vPred ).
tff(func_def_410,type,
sK382: ( vTable * vQuery ) > vTable ).
tff(func_def_411,type,
sK383: ( vTable * vQuery ) > vTable ).
tff(func_def_412,type,
sK384: ( vTable * vQuery ) > vTable ).
tff(func_def_413,type,
sK385: ( vTable * vQuery ) > vTable ).
tff(func_def_414,type,
sK386: ( vQuery * vQuery ) > vTable ).
tff(func_def_415,type,
sK387: ( vQuery * vQuery ) > vTable ).
tff(func_def_416,type,
sK388: ( vQuery * vQuery ) > vTable ).
tff(func_def_417,type,
sK389: ( vQuery * vQuery ) > vQuery ).
tff(func_def_418,type,
sK390: ( vQuery * vQuery ) > vTable ).
tff(func_def_419,type,
sK391: ( vQuery * vQuery ) > vTable ).
tff(func_def_420,type,
sK392: ( vQuery * vQuery ) > vTable ).
tff(func_def_421,type,
sK393: ( vQuery * vQuery ) > vQuery ).
tff(func_def_422,type,
sK394: ( vTable * vQuery ) > vTable ).
tff(func_def_423,type,
sK395: ( vTable * vQuery ) > vTable ).
tff(func_def_424,type,
sK396: ( vTable * vQuery ) > vTable ).
tff(func_def_425,type,
sK397: ( vTable * vQuery ) > vTable ).
tff(func_def_426,type,
sK398: ( vQuery * vQuery ) > vTable ).
tff(func_def_427,type,
sK399: ( vQuery * vQuery ) > vTable ).
tff(func_def_428,type,
sK400: ( vQuery * vQuery ) > vTable ).
tff(func_def_429,type,
sK401: ( vQuery * vQuery ) > vQuery ).
tff(func_def_430,type,
sK402: ( vQuery * vQuery ) > vTable ).
tff(func_def_431,type,
sK403: ( vQuery * vQuery ) > vTable ).
tff(func_def_432,type,
sK404: ( vQuery * vQuery ) > vTable ).
tff(func_def_433,type,
sK405: ( vQuery * vQuery ) > vQuery ).
tff(func_def_434,type,
sK406: ( vTable * vQuery ) > vTable ).
tff(func_def_435,type,
sK407: ( vTable * vQuery ) > vTable ).
tff(func_def_436,type,
sK408: ( vTable * vQuery ) > vTable ).
tff(func_def_437,type,
sK409: ( vTable * vQuery ) > vTable ).
tff(func_def_438,type,
sK410: ( vQuery * vQuery ) > vTable ).
tff(func_def_439,type,
sK411: ( vQuery * vQuery ) > vTable ).
tff(func_def_440,type,
sK412: ( vQuery * vQuery ) > vTable ).
tff(func_def_441,type,
sK413: ( vQuery * vQuery ) > vQuery ).
tff(func_def_442,type,
sK414: ( vQuery * vQuery ) > vTable ).
tff(func_def_443,type,
sK415: ( vQuery * vQuery ) > vTable ).
tff(func_def_444,type,
sK416: ( vQuery * vQuery ) > vTable ).
tff(func_def_445,type,
sK417: ( vQuery * vQuery ) > vQuery ).
tff(func_def_446,type,
sK418: ( vQuery * vTStore ) > vTable ).
tff(func_def_447,type,
sK419: ( vQuery * vTStore ) > vTable ).
tff(func_def_448,type,
sK420: ( vQuery * vTStore ) > vTStore ).
tff(func_def_449,type,
sK421: ( vQuery * vTStore ) > vPred ).
tff(func_def_450,type,
sK422: ( vQuery * vTStore ) > vSelect ).
tff(func_def_451,type,
sK423: ( vQuery * vTStore ) > vOptTable ).
tff(func_def_452,type,
sK424: ( vQuery * vTStore ) > vTStore ).
tff(func_def_453,type,
sK425: ( vQuery * vTStore ) > vName ).
tff(func_def_454,type,
sK426: ( vQuery * vTStore ) > vTable ).
tff(func_def_455,type,
sK427: ( vQuery * vTStore ) > vQuery ).
tff(func_def_456,type,
sK428: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_457,type,
sK429: ( vQuery * vTStore ) > vTStore ).
tff(func_def_458,type,
sK430: ( vQuery * vTStore ) > vTable ).
tff(func_def_459,type,
sK431: ( vQuery * vTStore ) > vQuery ).
tff(func_def_460,type,
sK432: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_461,type,
sK433: ( vQuery * vTStore ) > vTStore ).
tff(func_def_462,type,
sK434: ( vQuery * vTStore ) > vTable ).
tff(func_def_463,type,
sK435: ( vQuery * vTStore ) > vQuery ).
tff(func_def_464,type,
sK436: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_465,type,
sK437: ( vQuery * vTStore ) > vTStore ).
tff(func_def_466,type,
sK438: ( vQuery * vTStore ) > vTable ).
tff(func_def_467,type,
sK439: ( vQuery * vTStore ) > vQuery ).
tff(func_def_468,type,
sK440: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_469,type,
sK441: ( vQuery * vTStore ) > vTStore ).
tff(func_def_470,type,
sK442: ( vQuery * vTStore ) > vTable ).
tff(func_def_471,type,
sK443: ( vQuery * vTStore ) > vQuery ).
tff(func_def_472,type,
sK444: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_473,type,
sK445: ( vQuery * vTStore ) > vTStore ).
tff(func_def_474,type,
sK446: ( vQuery * vTStore ) > vTable ).
tff(func_def_475,type,
sK447: ( vQuery * vTStore ) > vQuery ).
tff(func_def_476,type,
sK448: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_477,type,
sK449: ( vQuery * vTStore ) > vTStore ).
tff(func_def_478,type,
sK450: ( vQuery * vTStore ) > vQuery ).
tff(func_def_479,type,
sK451: ( vQuery * vTStore ) > vQuery ).
tff(func_def_480,type,
sK452: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_481,type,
sK453: ( vQuery * vTStore ) > vTStore ).
tff(func_def_482,type,
sK454: ( vQuery * vTStore ) > vQuery ).
tff(func_def_483,type,
sK455: ( vQuery * vTStore ) > vQuery ).
tff(func_def_484,type,
sK456: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_485,type,
sK457: ( vQuery * vTStore ) > vTStore ).
tff(func_def_486,type,
sK458: ( vQuery * vTStore ) > vQuery ).
tff(func_def_487,type,
sK459: ( vQuery * vTStore ) > vQuery ).
tff(func_def_488,type,
sK460: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_489,type,
sK461: ( vQuery * vTStore ) > vTStore ).
tff(func_def_490,type,
sK462: ( vQuery * vTStore ) > vQuery ).
tff(func_def_491,type,
sK463: ( vQuery * vTStore ) > vQuery ).
tff(func_def_492,type,
sK464: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_493,type,
sK465: ( vQuery * vTStore ) > vTStore ).
tff(func_def_494,type,
sK466: ( vQuery * vTStore ) > vQuery ).
tff(func_def_495,type,
sK467: ( vQuery * vTStore ) > vQuery ).
tff(func_def_496,type,
sK468: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_497,type,
sK469: ( vQuery * vTStore ) > vTStore ).
tff(func_def_498,type,
sK470: ( vQuery * vTStore ) > vQuery ).
tff(func_def_499,type,
sK471: ( vQuery * vTStore ) > vQuery ).
tff(func_def_500,type,
sK472: ( vQuery * vTStore ) > vOptQuery ).
tff(func_def_501,type,
sK473: ( vQuery * vTStore ) > vTStore ).
tff(func_def_502,type,
sK474: ( vQuery * vTStore ) > vPred ).
tff(func_def_503,type,
sK475: ( vQuery * vTStore ) > vTable ).
tff(func_def_504,type,
sK476: ( vQuery * vTStore ) > vSelect ).
tff(func_def_505,type,
sK477: ( vQuery * vTStore ) > vOptTable ).
tff(func_def_506,type,
sK478: ( vQuery * vTStore ) > vOptTable ).
tff(func_def_507,type,
sK479: ( vQuery * vTStore ) > vTStore ).
tff(func_def_508,type,
sK480: ( vQuery * vTStore ) > vName ).
tff(func_def_509,type,
sK481: ( vQuery * vTStore ) > vPred ).
tff(func_def_510,type,
sK482: ( vQuery * vTStore ) > vTable ).
tff(func_def_511,type,
sK483: ( vQuery * vTStore ) > vSelect ).
tff(func_def_512,type,
sK484: ( vQuery * vTStore ) > vOptTable ).
tff(func_def_513,type,
sK485: ( vQuery * vTStore ) > vOptTable ).
tff(func_def_514,type,
sK486: ( vQuery * vTStore ) > vTStore ).
tff(func_def_515,type,
sK487: ( vQuery * vTStore ) > vName ).
tff(func_def_516,type,
sK488: ( vQuery * vTStore ) > vTable ).
tff(func_def_517,type,
sK489: ( vQuery * vTStore ) > vTStore ).
tff(func_def_518,type,
sK490: ( vQuery * vTStore ) > vTable ).
tff(func_def_519,type,
sK491: ( vQuery * vTStore ) > vTable ).
tff(func_def_520,type,
sK492: ( vQuery * vTStore ) > vTStore ).
tff(func_def_521,type,
sK493: ( vQuery * vTStore ) > vTable ).
tff(func_def_522,type,
sK494: ( vQuery * vTStore ) > vTable ).
tff(func_def_523,type,
sK495: ( vQuery * vTStore ) > vTStore ).
tff(func_def_524,type,
sK496: vOptFType > vFType ).
tff(func_def_525,type,
sK497: ( vName * vTType ) > vName ).
tff(func_def_526,type,
sK498: ( vName * vTType ) > vFType ).
tff(func_def_527,type,
sK499: ( vName * vTType ) > vTType ).
tff(func_def_528,type,
sK500: ( vName * vTType ) > vName ).
tff(func_def_529,type,
sK501: ( vName * vTType ) > vName ).
tff(func_def_530,type,
sK502: ( vName * vTType ) > vName ).
tff(func_def_531,type,
sK503: ( vName * vTType ) > vFType ).
tff(func_def_532,type,
sK504: ( vName * vTType ) > vTType ).
tff(func_def_533,type,
sK505: ( vName * vTType ) > vName ).
tff(func_def_534,type,
sK506: ( vAttrL * vTType ) > vName ).
tff(func_def_535,type,
sK507: ( vAttrL * vTType ) > vOptFType ).
tff(func_def_536,type,
sK508: ( vAttrL * vTType ) > vTType ).
tff(func_def_537,type,
sK509: ( vAttrL * vTType ) > vAttrL ).
tff(func_def_538,type,
sK510: ( vAttrL * vTType ) > vOptTType ).
tff(func_def_539,type,
sK511: ( vAttrL * vTType ) > vTType ).
tff(func_def_540,type,
sK512: ( vAttrL * vTType ) > vName ).
tff(func_def_541,type,
sK513: ( vAttrL * vTType ) > vOptFType ).
tff(func_def_542,type,
sK514: ( vAttrL * vTType ) > vTType ).
tff(func_def_543,type,
sK515: ( vAttrL * vTType ) > vAttrL ).
tff(func_def_544,type,
sK516: ( vAttrL * vTType ) > vOptTType ).
tff(func_def_545,type,
sK517: ( vSelect * vTType ) > vTType ).
tff(func_def_546,type,
sK518: ( vSelect * vTType ) > vAttrL ).
tff(func_def_547,type,
sK519: ( vSelect * vTType ) > vTType ).
tff(func_def_548,type,
sK520: ( vExp * vTType ) > vName ).
tff(func_def_549,type,
sK521: ( vExp * vTType ) > vName ).
tff(func_def_550,type,
sK522: ( vExp * vTType ) > vFType ).
tff(func_def_551,type,
sK523: ( vExp * vTType ) > vTType ).
tff(func_def_552,type,
sK524: ( vExp * vTType ) > vName ).
tff(func_def_553,type,
sK525: ( vExp * vTType ) > vName ).
tff(func_def_554,type,
sK526: ( vExp * vTType ) > vFType ).
tff(func_def_555,type,
sK527: ( vExp * vTType ) > vTType ).
tff(func_def_556,type,
sK528: ( vExp * vTType ) > vVal ).
tff(func_def_557,type,
sK529: ( vExp * vTType ) > vTType ).
tff(func_def_558,type,
sK530: ( vExp * vTType ) > vName ).
tff(func_def_559,type,
sK531: ( vPred * vTType ) > vOptFType ).
tff(func_def_560,type,
sK532: ( vPred * vTType ) > vExp ).
tff(func_def_561,type,
sK533: ( vPred * vTType ) > vOptFType ).
tff(func_def_562,type,
sK534: ( vPred * vTType ) > vExp ).
tff(func_def_563,type,
sK535: ( vPred * vTType ) > vTType ).
tff(func_def_564,type,
sK536: ( vPred * vTType ) > vOptFType ).
tff(func_def_565,type,
sK537: ( vPred * vTType ) > vExp ).
tff(func_def_566,type,
sK538: ( vPred * vTType ) > vOptFType ).
tff(func_def_567,type,
sK539: ( vPred * vTType ) > vExp ).
tff(func_def_568,type,
sK540: ( vPred * vTType ) > vTType ).
tff(func_def_569,type,
sK541: ( vPred * vTType ) > vOptFType ).
tff(func_def_570,type,
sK542: ( vPred * vTType ) > vExp ).
tff(func_def_571,type,
sK543: ( vPred * vTType ) > vOptFType ).
tff(func_def_572,type,
sK544: ( vPred * vTType ) > vExp ).
tff(func_def_573,type,
sK545: ( vPred * vTType ) > vTType ).
tff(func_def_574,type,
sK546: ( vPred * vTType ) > vTType ).
tff(func_def_575,type,
sK547: ( vPred * vTType ) > vPred ).
tff(func_def_576,type,
sK548: ( vPred * vTType ) > vPred ).
tff(func_def_577,type,
sK549: ( vPred * vTType ) > vTType ).
tff(func_def_578,type,
sK550: ( vPred * vTType ) > vPred ).
tff(func_def_579,type,
sK551: ( vPred * vTType ) > vTType ).
tff(func_def_580,type,
sK552: ( vPred * vTType ) > vOptFType ).
tff(func_def_581,type,
sK553: ( vPred * vTType ) > vExp ).
tff(func_def_582,type,
sK554: ( vPred * vTType ) > vOptFType ).
tff(func_def_583,type,
sK555: ( vPred * vTType ) > vExp ).
tff(func_def_584,type,
sK556: ( vPred * vTType ) > vTType ).
tff(func_def_585,type,
sK557: ( vPred * vTType ) > vOptFType ).
tff(func_def_586,type,
sK558: ( vPred * vTType ) > vExp ).
tff(func_def_587,type,
sK559: ( vPred * vTType ) > vOptFType ).
tff(func_def_588,type,
sK560: ( vPred * vTType ) > vExp ).
tff(func_def_589,type,
sK561: ( vPred * vTType ) > vTType ).
tff(func_def_590,type,
sK562: ( vPred * vTType ) > vOptFType ).
tff(func_def_591,type,
sK563: ( vPred * vTType ) > vExp ).
tff(func_def_592,type,
sK564: ( vPred * vTType ) > vOptFType ).
tff(func_def_593,type,
sK565: ( vPred * vTType ) > vExp ).
tff(func_def_594,type,
sK566: ( vPred * vTType ) > vTType ).
tff(func_def_595,type,
sK567: ( vPred * vTType ) > vPred ).
tff(func_def_596,type,
sK568: ( vPred * vTType ) > vPred ).
tff(func_def_597,type,
sK569: ( vPred * vTType ) > vTType ).
tff(func_def_598,type,
sK570: ( vPred * vTType ) > vPred ).
tff(func_def_599,type,
sK571: ( vPred * vTType ) > vTType ).
tff(func_def_600,type,
sK572: vTStore > vName ).
tff(func_def_601,type,
sK573: vTStore > vTable ).
tff(func_def_602,type,
sK574: vTStore > vTStore ).
tff(func_def_603,type,
sK575: vTTContext > vName ).
tff(func_def_604,type,
sK576: vTTContext > vTType ).
tff(func_def_605,type,
sK577: vTTContext > vTTContext ).
tff(func_def_606,type,
sK578: ( vTStore * vTTContext ) > vName ).
tff(func_def_607,type,
sK579: ( vTStore * vTTContext ) > vTable ).
tff(func_def_608,type,
sK580: ( vTStore * vTTContext ) > vTTContext ).
tff(func_def_609,type,
sK581: ( vTStore * vTTContext ) > vName ).
tff(func_def_610,type,
sK582: ( vTStore * vTTContext ) > vTStore ).
tff(func_def_611,type,
sK583: ( vTStore * vTTContext ) > vTType ).
tff(func_def_612,type,
sK584: ( vTStore * vTTContext ) > vName ).
tff(func_def_613,type,
sK585: ( vTStore * vTTContext ) > vTable ).
tff(func_def_614,type,
sK586: ( vTStore * vTTContext ) > vTTContext ).
tff(func_def_615,type,
sK587: ( vTStore * vTTContext ) > vName ).
tff(func_def_616,type,
sK588: ( vTStore * vTTContext ) > vTStore ).
tff(func_def_617,type,
sK589: ( vTStore * vTTContext ) > vTType ).
tff(func_def_618,type,
sK590: ( vTStore * vTTContext ) > vTStore ).
tff(func_def_619,type,
sK591: ( vTStore * vTTContext ) > vTTContext ).
tff(func_def_620,type,
sK592: ( vPred * vTType * vSelect * vName * vTTContext ) > vTType ).
tff(func_def_621,type,
sK593: ( vRawTable * vAttrL * vName ) > vRawTable ).
tff(func_def_622,type,
sK594: ( vRawTable * vAttrL ) > vRawTable ).
tff(func_def_623,type,
sK595: vAttrL ).
tff(func_def_624,type,
sK596: vRawTable ).
tff(func_def_625,type,
sK597: vTType ).
tff(func_def_626,type,
sK598: vAttrL ).
tff(func_def_627,type,
sK599: vName ).
tff(func_def_628,type,
sK600: 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: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_21,type,
sP1: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_22,type,
sP2: ( vRawTable * vRawTable ) > $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: ( vName * vTStore ) > $o ).
tff(pred_def_29,type,
sP9: ( vName * vTTContext ) > $o ).
tff(pred_def_30,type,
sP10: ( vName * vAttrL * vRawTable ) > $o ).
tff(pred_def_31,type,
sP11: ( vAttrL * vAttrL * vRawTable ) > $o ).
tff(pred_def_32,type,
sP12: ( vSelect * vTable ) > $o ).
tff(pred_def_33,type,
sP13: ( vExp * vAttrL * vRow ) > $o ).
tff(pred_def_34,type,
sP14: ( vExp * vAttrL * vRow ) > $o ).
tff(pred_def_35,type,
sP15: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_36,type,
sP16: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_37,type,
sP17: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_38,type,
sP18: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_39,type,
sP19: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_40,type,
sP20: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_41,type,
sP21: ( vPred * vAttrL * vRow ) > $o ).
tff(pred_def_42,type,
sP22: ( vRawTable * vAttrL * vPred ) > $o ).
tff(pred_def_43,type,
sP23: ( vQuery * vTStore ) > $o ).
tff(pred_def_44,type,
sP24: ( vQuery * vTStore ) > $o ).
tff(pred_def_45,type,
sP25: ( vQuery * vTStore ) > $o ).
tff(pred_def_46,type,
sP26: ( vQuery * vTStore ) > $o ).
tff(pred_def_47,type,
sP27: ( vQuery * vTStore ) > $o ).
tff(pred_def_48,type,
sP28: ( vQuery * vTStore ) > $o ).
tff(pred_def_49,type,
sP29: ( vQuery * vTStore ) > $o ).
tff(pred_def_50,type,
sP30: ( vQuery * vTStore ) > $o ).
tff(pred_def_51,type,
sP31: ( vQuery * vTStore ) > $o ).
tff(pred_def_52,type,
sP32: ( vQuery * vTStore ) > $o ).
tff(pred_def_53,type,
sP33: ( vQuery * vTStore ) > $o ).
tff(pred_def_54,type,
sP34: ( vQuery * vTStore ) > $o ).
tff(pred_def_55,type,
sP35: ( vQuery * vTStore ) > $o ).
tff(pred_def_56,type,
sP36: ( vQuery * vTStore ) > $o ).
tff(pred_def_57,type,
sP37: ( vQuery * vTStore ) > $o ).
tff(pred_def_58,type,
sP38: ( vQuery * vTStore ) > $o ).
tff(pred_def_59,type,
sP39: ( vName * vTType ) > $o ).
tff(pred_def_60,type,
sP40: ( vAttrL * vTType ) > $o ).
tff(pred_def_61,type,
sP41: ( vExp * vTType ) > $o ).
tff(pred_def_62,type,
sP42: ( vExp * vTType ) > $o ).
tff(pred_def_63,type,
sP43: ( vPred * vTType ) > $o ).
tff(pred_def_64,type,
sP44: ( vPred * vTType ) > $o ).
tff(pred_def_65,type,
sP45: ( vPred * vTType ) > $o ).
tff(pred_def_66,type,
sP46: ( vPred * vTType ) > $o ).
tff(pred_def_67,type,
sP47: ( vPred * vTType ) > $o ).
tff(pred_def_68,type,
sP48: ( vPred * vTType ) > $o ).
tff(pred_def_69,type,
sP601: ( vTType * vAttrL * vAttrL ) > $o ).
tff(pred_def_70,type,
sP602: ( vTType * vAttrL ) > $o ).
tff(pred_def_71,type,
sP603: ( vTType * vAttrL * vAttrL ) > $o ).
tff(pred_def_72,type,
sP604: ( vTType * vAttrL ) > $o ).
tff(pred_def_73,type,
sP605: ( vTType * vAttrL * vAttrL ) > $o ).
tff(pred_def_74,type,
sP606: ( vTType * vAttrL ) > $o ).
tff(pred_def_75,type,
sP607: ( vTType * vRow * vRow ) > $o ).
tff(pred_def_76,type,
sP608: ( vTType * vRow ) > $o ).
tff(pred_def_77,type,
sP609: ( vTType * vRow * vRow ) > $o ).
tff(pred_def_78,type,
sP610: ( vTType * vRow ) > $o ).
tff(pred_def_79,type,
sP611: ( vTType * vRow * vRow ) > $o ).
tff(pred_def_80,type,
sP612: ( vTType * vRow ) > $o ).
tff(pred_def_81,type,
sP613: ( vRawTable * vRawTable * vRawTable ) > $o ).
tff(pred_def_82,type,
sP614: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_83,type,
sP615: ( vRawTable * vRawTable * vRawTable ) > $o ).
tff(pred_def_84,type,
sP616: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_85,type,
sP617: ( vRawTable * vRawTable * vRawTable ) > $o ).
tff(pred_def_86,type,
sP618: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_87,type,
sP619: ( vRawTable * vRawTable * vRawTable ) > $o ).
tff(pred_def_88,type,
sP620: ( vRawTable * vRawTable ) > $o ).
tff(pred_def_89,type,
sP621: ( vExp * vRow * vAttrL ) > $o ).
tff(pred_def_90,type,
sP622: ( vRow * vExp * vRow * vAttrL ) > $o ).
tff(pred_def_91,type,
sP623: ( vExp * vRow * vAttrL ) > $o ).
tff(pred_def_92,type,
sP624: ( vQuery * vTStore ) > $o ).
tff(pred_def_93,type,
sP625: ( vQuery * vTStore ) > $o ).
tff(pred_def_94,type,
sP626: ( vQuery * vTStore ) > $o ).
tff(pred_def_95,type,
sP627: ( vQuery * vTStore ) > $o ).
tff(pred_def_96,type,
sP628: ( vQuery * vTStore ) > $o ).
tff(pred_def_97,type,
sP629: ( vQuery * vTStore ) > $o ).
tff(pred_def_98,type,
sP630: ( vTable * vTStore * vTStore * vTTContext ) > $o ).
tff(pred_def_99,type,
sP631: ( vTStore * vTStore * vTTContext ) > $o ).
tff(pred_def_100,type,
sP632: ( vTStore * vTTContext ) > $o ).
tff(pred_def_101,type,
sP633: ( vTable * vTStore * vTStore * vTTContext ) > $o ).
tff(pred_def_102,type,
sP634: ( vTStore * vTStore * vTTContext ) > $o ).
tff(pred_def_103,type,
sP635: ( vTStore * vTTContext ) > $o ).
tff(pred_def_104,type,
sP636: ( vTable * vTStore * vTStore * vTTContext ) > $o ).
tff(pred_def_105,type,
sP637: ( vTStore * vTStore * vTTContext ) > $o ).
tff(pred_def_106,type,
sP638: ( vTStore * vTTContext ) > $o ).
tff(pred_def_107,type,
sP639: ( vName * vTType * vRawTable ) > $o ).
tff(pred_def_108,type,
sP640: vRawTable > $o ).
tff(pred_def_109,type,
sP641: ( vTType * vName ) > $o ).
tff(pred_def_110,type,
sP642: vTType > $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(f297,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(f298,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(f299,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-True') ).
tff(f300,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)],[f299]) ).
tff(f340,plain,
! [X0: vName,X1: vAttrL,X2: vName,X3: vAttrL] :
( ( ( X0 = X2 )
& ( X1 = X3 ) )
| ( vacons(X0,X1) != vacons(X2,X3) ) ),
inference(ennf_transformation,[],[f87]) ).
tff(f362,plain,
! [X0: vOptRawTable] :
( ( X0 = vnoRawTable )
| visSomeRawTable(X0) ),
inference(ennf_transformation,[],[f134]) ).
tff(f388,plain,
! [X0: vOptTType] :
( ? [X1: vTType] : ( X0 = vsomeTType(X1) )
| ~ visSomeTType(X0) ),
inference(ennf_transformation,[],[f170]) ).
tff(f397,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(f398,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,[],[f397]) ).
tff(f443,plain,
! [X0: vOptFType] :
( ? [X1: vFType] : ( X0 = vsomeFType(X1) )
| ~ visSomeFType(X0) ),
inference(ennf_transformation,[],[f247]) ).
tff(f448,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(f449,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(f488,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,[],[f297]) ).
tff(f489,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,[],[f488]) ).
tff(f490,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,[],[f298]) ).
tff(f491,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,[],[f490]) ).
tff(f492,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,[],[f300]) ).
tff(f493,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,[],[f492]) ).
tff(f549,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))) ) )
| ~ sP40(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP40])],[predicate_definition_introduction]) ).
tff(f550,plain,
! [X0: vAttrL,X1: vTType] :
( ? [X2: vTType] :
( ( X0 = vaempty )
& ( X1 = X2 )
& ( vprojectTypeAttrL(X0,X1) = vsomeTType(vttempty) ) )
| sP40(X0,X1)
| ? [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(definition_folding,[],[f449,f549]) ).
tff(f567,plain,
! [X0: vOptRawTable] :
( ( X0 = vnoRawTable )
| ( vsomeRawTable(sK67(X0)) = X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK67]),skolemize(X1,sK67(X0))],[f29]) ).
tff(f649,plain,
! [X0: vOptTType] :
( ( vsomeTType(sK238(X0)) = X0 )
| ~ visSomeTType(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK238]),skolemize(X1,sK238(X0))],[f388]) ).
tff(f780,plain,
! [X0: vOptFType] :
( ( vsomeFType(sK496(X0)) = X0 )
| ~ visSomeFType(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK496]),skolemize(X1,sK496(X0))],[f443]) ).
tff(f785,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))) ) )
| ~ sP40(X0,X1) ),
inference(nnf_transformation,[],[f549]) ).
tff(f786,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))) ) )
| ~ sP40(X0,X1) ),
inference(rectify,[],[f785]) ).
tff(f787,plain,
! [X0: vAttrL,X1: vTType] :
( ( ( sK507(X0,X1) = vfindColType(sK506(X0,X1),sK508(X0,X1)) )
& ( sK510(X0,X1) = vprojectTypeAttrL(sK509(X0,X1),sK508(X0,X1)) )
& visSomeFType(sK507(X0,X1))
& visSomeTType(sK510(X0,X1))
& ( vacons(sK506(X0,X1),sK509(X0,X1)) = X0 )
& ( sK508(X0,X1) = X1 )
& ( vprojectTypeAttrL(X0,X1) = vsomeTType(vttcons(sK506(X0,X1),vgetFType(sK507(X0,X1)),vgetTType(sK510(X0,X1)))) ) )
| ~ sP40(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK506,sK507,sK508,sK509,sK510]),skolemize(X2,sK506(X0,X1)),skolemize(X3,sK507(X0,X1)),skolemize(X4,sK508(X0,X1)),skolemize(X5,sK509(X0,X1)),skolemize(X6,sK510(X0,X1))],[f786]) ).
tff(f788,plain,
! [X0: vAttrL,X1: vTType] :
( ? [X2: vTType] :
( ( X0 = vaempty )
& ( X1 = X2 )
& ( vprojectTypeAttrL(X0,X1) = vsomeTType(vttempty) ) )
| sP40(X0,X1)
| ? [X3: vName,X4: vOptFType,X5: vTType,X6: vAttrL,X7: vOptTType] :
( ( vfindColType(X3,X5) = X4 )
& ( vprojectTypeAttrL(X6,X5) = X7 )
& ( ~ visSomeFType(X4)
| ~ visSomeTType(X7) )
& ( vacons(X3,X6) = X0 )
& ( X1 = X5 )
& ( vprojectTypeAttrL(X0,X1) = vnoTType ) ) ),
inference(rectify,[],[f550]) ).
tff(f789,plain,
! [X0: vAttrL,X1: vTType] :
( ( ( X0 = vaempty )
& ( sK511(X0,X1) = X1 )
& ( vprojectTypeAttrL(X0,X1) = vsomeTType(vttempty) ) )
| sP40(X0,X1)
| ( ( sK513(X0,X1) = vfindColType(sK512(X0,X1),sK514(X0,X1)) )
& ( sK516(X0,X1) = vprojectTypeAttrL(sK515(X0,X1),sK514(X0,X1)) )
& ( ~ visSomeFType(sK513(X0,X1))
| ~ visSomeTType(sK516(X0,X1)) )
& ( vacons(sK512(X0,X1),sK515(X0,X1)) = X0 )
& ( sK514(X0,X1) = X1 )
& ( vprojectTypeAttrL(X0,X1) = vnoTType ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK511,sK512,sK513,sK514,sK515,sK516]),skolemize(X2,sK511(X0,X1)),skolemize(X3,sK512(X0,X1)),skolemize(X4,sK513(X0,X1)),skolemize(X5,sK514(X0,X1)),skolemize(X6,sK515(X0,X1)),skolemize(X7,sK516(X0,X1))],[f788]) ).
tff(f833,plain,
! [X0: vRawTable,X1: vFType,X2: vAttrL,X3: vName,X4: vTType] :
( ( vfindCol(X3,X2,X0) = vsomeRawTable(sK593(X0,X2,X3)) )
| ~ vwelltypedRawtable(X4,X0)
| ~ vmatchingAttrL(X4,X2)
| ( vsomeFType(X1) != vfindColType(X3,X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK593]),skolemize(X5,sK593(X0,X2,X3))],[f489]) ).
tff(f834,plain,
! [X0: vTType,X1: vRawTable,X2: vAttrL,X3: vTType] :
( ( vprojectCols(val1,X2,X1) = vsomeRawTable(sK594(X1,X2)) )
| ~ vwelltypedRawtable(X0,X1)
| ~ vmatchingAttrL(X0,X2)
| ( vsomeTType(X3) != vprojectTypeAttrL(val1,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK594]),skolemize(X4,sK594(X1,X2))],[f491]) ).
tff(f835,plain,
( ! [X6: vRawTable] : ( vsomeRawTable(X6) != vprojectCols(vacons(sK599,val1),sK595,sK596) )
& visSomeRawTable(vfindCol(sK599,val1,sK596))
& visSomeRawTable(vprojectCols(sK598,val1,sK596))
& vwelltypedRawtable(sK600,sK596)
& vmatchingAttrL(sK600,sK595)
& ( vsomeTType(sK597) = vprojectTypeAttrL(vacons(sK599,val1),sK600) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK595,sK596,sK597,sK598,sK599,sK600]),skolemize(X0,sK595),skolemize(X1,sK596),skolemize(X2,sK597),skolemize(X3,sK598),skolemize(X4,sK599),skolemize(X5,sK600)],[f493]) ).
tff(f873,plain,
! [X0: vOptRawTable] :
( ( vnoRawTable = X0 )
| ( vsomeRawTable(sK67(X0)) = X0 ) ),
inference(cnf_transformation,[],[f567]) ).
tff(f875,plain,
! [X0: vRawTable] : ( vnoRawTable != vsomeRawTable(X0) ),
inference(cnf_transformation,[],[f31]) ).
tff(f878,plain,
! [X0: vTType] : ( vnoTType != vsomeTType(X0) ),
inference(cnf_transformation,[],[f34]) ).
tff(f941,plain,
! [X2: vName,X3: vAttrL,X0: vName,X1: vAttrL] :
( ( X0 = X2 )
| ( vacons(X0,X1) != vacons(X2,X3) ) ),
inference(cnf_transformation,[],[f340]) ).
tff(f942,plain,
! [X0: vName,X1: vAttrL] : ( vaempty != vacons(X0,X1) ),
inference(cnf_transformation,[],[f88]) ).
tff(f1085,plain,
! [X0: vRawTable] : visSomeRawTable(vsomeRawTable(X0)),
inference(cnf_transformation,[],[f132]) ).
tff(f1087,plain,
! [X0: vOptRawTable] :
( ( vnoRawTable = X0 )
| visSomeRawTable(X0) ),
inference(cnf_transformation,[],[f362]) ).
tff(f1251,plain,
! [X0: vOptTType] :
( ( vsomeTType(sK238(X0)) = X0 )
| ~ visSomeTType(X0) ),
inference(cnf_transformation,[],[f649]) ).
tff(f1318,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,[],[f398]) ).
tff(f1725,plain,
! [X0: vOptFType] :
( ( vsomeFType(sK496(X0)) = X0 )
| ~ visSomeFType(X0) ),
inference(cnf_transformation,[],[f780]) ).
tff(f1748,plain,
! [X2: vAttrL,X0: vName,X1: vTType] :
( ( vnoTType = vprojectTypeAttrL(vacons(X0,X2),X1) )
| visSomeTType(vprojectTypeAttrL(X2,X1)) ),
inference(cnf_transformation,[],[f448]) ).
tff(f1749,plain,
! [X2: vAttrL,X0: vName,X1: vTType] :
( ( vnoTType = vprojectTypeAttrL(vacons(X0,X2),X1) )
| visSomeFType(vfindColType(X0,X1)) ),
inference(cnf_transformation,[],[f448]) ).
tff(f1751,plain,
! [X0: vAttrL,X1: vTType] :
( ( sK508(X0,X1) = X1 )
| ~ sP40(X0,X1) ),
inference(cnf_transformation,[],[f787]) ).
tff(f1752,plain,
! [X0: vAttrL,X1: vTType] :
( ( vacons(sK506(X0,X1),sK509(X0,X1)) = X0 )
| ~ sP40(X0,X1) ),
inference(cnf_transformation,[],[f787]) ).
tff(f1756,plain,
! [X0: vAttrL,X1: vTType] :
( ( sK507(X0,X1) = vfindColType(sK506(X0,X1),sK508(X0,X1)) )
| ~ sP40(X0,X1) ),
inference(cnf_transformation,[],[f787]) ).
tff(f1769,plain,
! [X0: vAttrL,X1: vTType] :
( ( vaempty = X0 )
| sP40(X0,X1)
| ( vnoTType = vprojectTypeAttrL(X0,X1) ) ),
inference(cnf_transformation,[],[f789]) ).
tff(f1775,plain,
! [X0: vTType] : ( vsomeTType(X0) = vprojectType(vall,X0) ),
inference(cnf_transformation,[],[f257]) ).
tff(f1776,plain,
! [X0: vAttrL,X1: vTType] : ( vprojectTypeAttrL(X0,X1) = vprojectType(vlist(X0),X1) ),
inference(cnf_transformation,[],[f258]) ).
tff(f1946,plain,
! [X2: vAttrL,X3: vName,X0: vRawTable,X1: vFType,X4: vTType] :
( ( vfindCol(X3,X2,X0) = vsomeRawTable(sK593(X0,X2,X3)) )
| ~ vwelltypedRawtable(X4,X0)
| ~ vmatchingAttrL(X4,X2)
| ( vsomeFType(X1) != vfindColType(X3,X4) ) ),
inference(cnf_transformation,[],[f833]) ).
tff(f1947,plain,
! [X2: vAttrL,X3: vTType,X0: vTType,X1: vRawTable] :
( ( vprojectCols(val1,X2,X1) = vsomeRawTable(sK594(X1,X2)) )
| ~ vwelltypedRawtable(X0,X1)
| ~ vmatchingAttrL(X0,X2)
| ( vsomeTType(X3) != vprojectTypeAttrL(val1,X0) ) ),
inference(cnf_transformation,[],[f834]) ).
tff(f1948,plain,
vsomeTType(sK597) = vprojectTypeAttrL(vacons(sK599,val1),sK600),
inference(cnf_transformation,[],[f835]) ).
tff(f1949,plain,
vmatchingAttrL(sK600,sK595),
inference(cnf_transformation,[],[f835]) ).
tff(f1950,plain,
vwelltypedRawtable(sK600,sK596),
inference(cnf_transformation,[],[f835]) ).
tff(f1953,plain,
! [X6: vRawTable] : ( vsomeRawTable(X6) != vprojectCols(vacons(sK599,val1),sK595,sK596) ),
inference(cnf_transformation,[],[f835]) ).
tff(f1959,plain,
! [X0: vTType] : ( vnoTType != vprojectType(vall,X0) ),
inference(definition_unfolding,[],[f878,f1775]) ).
tff(f1971,plain,
! [X0: vOptTType] :
( ( vprojectType(vall,sK238(X0)) = X0 )
| ~ visSomeTType(X0) ),
inference(definition_unfolding,[],[f1251,f1775]) ).
tff(f2014,plain,
! [X2: vAttrL,X0: vName,X1: vTType] :
( ( vnoTType = vprojectType(vlist(vacons(X0,X2)),X1) )
| visSomeFType(vfindColType(X0,X1)) ),
inference(definition_unfolding,[],[f1749,f1776]) ).
tff(f2015,plain,
! [X2: vAttrL,X0: vName,X1: vTType] :
( ( vnoTType = vprojectType(vlist(vacons(X0,X2)),X1) )
| visSomeTType(vprojectType(vlist(X2),X1)) ),
inference(definition_unfolding,[],[f1748,f1776,f1776]) ).
tff(f2019,plain,
! [X0: vAttrL,X1: vTType] :
( ( vaempty = X0 )
| sP40(X0,X1)
| ( vnoTType = vprojectType(vlist(X0),X1) ) ),
inference(definition_unfolding,[],[f1769,f1776]) ).
tff(f2036,plain,
! [X2: vAttrL,X3: vTType,X0: vTType,X1: vRawTable] :
( ( vprojectCols(val1,X2,X1) = vsomeRawTable(sK594(X1,X2)) )
| ~ vwelltypedRawtable(X0,X1)
| ~ vmatchingAttrL(X0,X2)
| ( vprojectType(vall,X3) != vprojectType(vlist(val1),X0) ) ),
inference(definition_unfolding,[],[f1947,f1775,f1776]) ).
tff(f2037,plain,
vprojectType(vall,sK597) = vprojectType(vlist(vacons(sK599,val1)),sK600),
inference(definition_unfolding,[],[f1948,f1775,f1776]) ).
tff(f2138,plain,
! [X3: vName,X1: vFType,X4: vTType] :
( ( vsomeFType(X1) != vfindColType(X3,X4) )
| sP641(X4,X3) ),
inference(cnf_transformation,[],[f2138_D]) ).
tff(f2138_D,definition,
! [X3,X4] :
( ! [X1] : ( vsomeFType(X1) != vfindColType(X3,X4) )
<=> ~ sP641(X4,X3) ),
introduced(definition,[new_symbols(definition,[sP641])],[general_splitting_component_introduction]) ).
tff(f2139,plain,
! [X2: vAttrL,X3: vName,X0: vRawTable,X4: vTType] :
( ( vfindCol(X3,X2,X0) = vsomeRawTable(sK593(X0,X2,X3)) )
| ~ vwelltypedRawtable(X4,X0)
| ~ vmatchingAttrL(X4,X2)
| ~ sP641(X4,X3) ),
inference(general_splitting,[],[f1946,f2138_D]) ).
tff(f2140,plain,
! [X3: vTType,X0: vTType] :
( ( vprojectType(vall,X3) != vprojectType(vlist(val1),X0) )
| sP642(X0) ),
inference(cnf_transformation,[],[f2140_D]) ).
tff(f2140_D,definition,
! [X0] :
( ! [X3] : ( vprojectType(vall,X3) != vprojectType(vlist(val1),X0) )
<=> ~ sP642(X0) ),
introduced(definition,[new_symbols(definition,[sP642])],[general_splitting_component_introduction]) ).
tff(f2141,plain,
! [X2: vAttrL,X0: vTType,X1: vRawTable] :
( ( vprojectCols(val1,X2,X1) = vsomeRawTable(sK594(X1,X2)) )
| ~ vwelltypedRawtable(X0,X1)
| ~ vmatchingAttrL(X0,X2)
| ~ sP642(X0) ),
inference(general_splitting,[],[f2036,f2140_D]) ).
tff(f2143,definition,
( spl643_1
<=> ! [X6: vRawTable] : ( vsomeRawTable(X6) != vprojectCols(vacons(sK599,val1),sK595,sK596) ) ),
introduced(definition,[new_symbols(definition,[spl643_1])],[avatar_definition]) ).
tff(f2144,plain,
( ! [X6: vRawTable] : ( vsomeRawTable(X6) != vprojectCols(vacons(sK599,val1),sK595,sK596) )
| ~ spl643_1 ),
inference(avatar_component_clause,[],[f2143]) ).
tff(f2145,plain,
spl643_1,
inference(avatar_split_clause,[],[f1953,f2143]) ).
tff(f2150,plain,
( ! [X2: vAttrL,X3: vRawTable,X0: vName,X1: vAttrL] :
( ( vprojectCols(vacons(sK599,val1),sK595,sK596) != vprojectCols(vacons(X0,X1),X2,X3) )
| ~ visSomeRawTable(vfindCol(X0,X2,X3))
| ~ visSomeRawTable(vprojectCols(X1,X2,X3)) )
| ~ spl643_1 ),
inference(superposition,[],[f2144,f1318]) ).
tff(f2159,plain,
( ! [X0: vOptRawTable] :
( ( vprojectCols(vacons(sK599,val1),sK595,sK596) != X0 )
| ( vnoRawTable = X0 ) )
| ~ spl643_1 ),
inference(superposition,[],[f2144,f873]) ).
tff(f2170,definition,
( spl643_2
<=> vmatchingAttrL(sK600,sK595) ),
introduced(definition,[new_symbols(definition,[spl643_2])],[avatar_definition]) ).
tff(f2172,plain,
( vmatchingAttrL(sK600,sK595)
| ~ spl643_2 ),
inference(avatar_component_clause,[],[f2170]) ).
tff(f2173,plain,
spl643_2,
inference(avatar_split_clause,[],[f1949,f2170]) ).
tff(f2175,definition,
( spl643_3
<=> vwelltypedRawtable(sK600,sK596) ),
introduced(definition,[new_symbols(definition,[spl643_3])],[avatar_definition]) ).
tff(f2177,plain,
( vwelltypedRawtable(sK600,sK596)
| ~ spl643_3 ),
inference(avatar_component_clause,[],[f2175]) ).
tff(f2178,plain,
spl643_3,
inference(avatar_split_clause,[],[f1950,f2175]) ).
tff(f2194,plain,
( ! [X0: vName,X1: vRawTable] :
( ( vfindCol(X0,sK595,X1) = vsomeRawTable(sK593(X1,sK595,X0)) )
| ~ vwelltypedRawtable(sK600,X1)
| ~ sP641(sK600,X0) )
| ~ spl643_2 ),
inference(resolution,[],[f2172,f2139]) ).
tff(f2195,plain,
( ! [X0: vRawTable] :
( ( vprojectCols(val1,sK595,X0) = vsomeRawTable(sK594(X0,sK595)) )
| ~ vwelltypedRawtable(sK600,X0)
| ~ sP642(sK600) )
| ~ spl643_2 ),
inference(resolution,[],[f2172,f2141]) ).
tff(f2211,definition,
( spl643_4
<=> ( vprojectType(vall,sK597) = vprojectType(vlist(vacons(sK599,val1)),sK600) ) ),
introduced(definition,[new_symbols(definition,[spl643_4])],[avatar_definition]) ).
tff(f2213,plain,
( ( vprojectType(vall,sK597) = vprojectType(vlist(vacons(sK599,val1)),sK600) )
| ~ spl643_4 ),
inference(avatar_component_clause,[],[f2211]) ).
tff(f2214,plain,
spl643_4,
inference(avatar_split_clause,[],[f2037,f2211]) ).
tff(f2229,plain,
( ( vnoTType = vprojectType(vall,sK597) )
| ( vaempty = vacons(sK599,val1) )
| sP40(vacons(sK599,val1),sK600)
| ~ spl643_4 ),
inference(superposition,[],[f2019,f2213]) ).
tff(f2239,plain,
( ( vnoTType = vprojectType(vall,sK597) )
| visSomeTType(vprojectType(vlist(val1),sK600))
| ~ spl643_4 ),
inference(superposition,[],[f2015,f2213]) ).
tff(f2240,plain,
( ( vnoTType = vprojectType(vall,sK597) )
| visSomeFType(vfindColType(sK599,sK600))
| ~ spl643_4 ),
inference(superposition,[],[f2014,f2213]) ).
tff(f2241,plain,
( visSomeFType(vfindColType(sK599,sK600))
| ~ spl643_4 ),
inference(forward_subsumption_resolution,[],[f2240,f1959]) ).
tff(f2242,plain,
( visSomeTType(vprojectType(vlist(val1),sK600))
| ~ spl643_4 ),
inference(forward_subsumption_resolution,[],[f2239,f1959]) ).
tff(f2246,plain,
( ( vaempty = vacons(sK599,val1) )
| sP40(vacons(sK599,val1),sK600)
| ~ spl643_4 ),
inference(forward_subsumption_resolution,[],[f2229,f1959]) ).
tff(f2255,plain,
( sP40(vacons(sK599,val1),sK600)
| ~ spl643_4 ),
inference(forward_subsumption_resolution,[],[f2246,f942]) ).
tff(f2430,definition,
( spl643_16
<=> ! [X0: vOptRawTable] :
( ( vprojectCols(vacons(sK599,val1),sK595,sK596) != X0 )
| ( vnoRawTable = X0 ) ) ),
introduced(definition,[new_symbols(definition,[spl643_16])],[avatar_definition]) ).
tff(f2431,plain,
( ! [X0: vOptRawTable] :
( ( vprojectCols(vacons(sK599,val1),sK595,sK596) != X0 )
| ( vnoRawTable = X0 ) )
| ~ spl643_16 ),
inference(avatar_component_clause,[],[f2430]) ).
tff(f2432,plain,
( spl643_16
| ~ spl643_1 ),
inference(avatar_split_clause,[],[f2159,f2143,f2430]) ).
tff(f2439,plain,
( ( vnoRawTable = vprojectCols(vacons(sK599,val1),sK595,sK596) )
| ~ spl643_16 ),
inference(equality_resolution,[],[f2431]) ).
tff(f2447,definition,
( spl643_17
<=> ( vnoRawTable = vprojectCols(vacons(sK599,val1),sK595,sK596) ) ),
introduced(definition,[new_symbols(definition,[spl643_17])],[avatar_definition]) ).
tff(f2449,plain,
( ( vnoRawTable = vprojectCols(vacons(sK599,val1),sK595,sK596) )
| ~ spl643_17 ),
inference(avatar_component_clause,[],[f2447]) ).
tff(f2450,plain,
( spl643_17
| ~ spl643_16 ),
inference(avatar_split_clause,[],[f2439,f2430,f2447]) ).
tff(f2830,definition,
( spl643_35
<=> ! [X0: vName,X3: vRawTable,X2: vAttrL,X1: vAttrL] :
( ( vprojectCols(vacons(sK599,val1),sK595,sK596) != vprojectCols(vacons(X0,X1),X2,X3) )
| ~ visSomeRawTable(vfindCol(X0,X2,X3))
| ~ visSomeRawTable(vprojectCols(X1,X2,X3)) ) ),
introduced(definition,[new_symbols(definition,[spl643_35])],[avatar_definition]) ).
tff(f2831,plain,
( ! [X2: vAttrL,X3: vRawTable,X0: vName,X1: vAttrL] :
( ( vprojectCols(vacons(sK599,val1),sK595,sK596) != vprojectCols(vacons(X0,X1),X2,X3) )
| ~ visSomeRawTable(vfindCol(X0,X2,X3))
| ~ visSomeRawTable(vprojectCols(X1,X2,X3)) )
| ~ spl643_35 ),
inference(avatar_component_clause,[],[f2830]) ).
tff(f2832,plain,
( spl643_35
| ~ spl643_1 ),
inference(avatar_split_clause,[],[f2150,f2143,f2830]) ).
tff(f2833,plain,
( ! [X2: vAttrL,X3: vRawTable,X0: vName,X1: vAttrL] :
( ( vnoRawTable != vprojectCols(vacons(X0,X1),X2,X3) )
| ~ visSomeRawTable(vfindCol(X0,X2,X3))
| ~ visSomeRawTable(vprojectCols(X1,X2,X3)) )
| ~ spl643_17
| ~ spl643_35 ),
inference(forward_demodulation,[],[f2831,f2449]) ).
tff(f2835,definition,
( spl643_36
<=> ! [X0: vName,X3: vRawTable,X2: vAttrL,X1: vAttrL] :
( ( vnoRawTable != vprojectCols(vacons(X0,X1),X2,X3) )
| ~ visSomeRawTable(vfindCol(X0,X2,X3))
| ~ visSomeRawTable(vprojectCols(X1,X2,X3)) ) ),
introduced(definition,[new_symbols(definition,[spl643_36])],[avatar_definition]) ).
tff(f2836,plain,
( ! [X2: vAttrL,X3: vRawTable,X0: vName,X1: vAttrL] :
( ( vnoRawTable != vprojectCols(vacons(X0,X1),X2,X3) )
| ~ visSomeRawTable(vfindCol(X0,X2,X3))
| ~ visSomeRawTable(vprojectCols(X1,X2,X3)) )
| ~ spl643_36 ),
inference(avatar_component_clause,[],[f2835]) ).
tff(f2837,plain,
( spl643_36
| ~ spl643_17
| ~ spl643_35 ),
inference(avatar_split_clause,[],[f2833,f2830,f2447,f2835]) ).
tff(f2875,plain,
( ( vnoRawTable != vnoRawTable )
| ~ visSomeRawTable(vfindCol(sK599,sK595,sK596))
| ~ visSomeRawTable(vprojectCols(val1,sK595,sK596))
| ~ spl643_17
| ~ spl643_36 ),
inference(superposition,[],[f2836,f2449]) ).
tff(f2884,plain,
( ~ visSomeRawTable(vfindCol(sK599,sK595,sK596))
| ~ visSomeRawTable(vprojectCols(val1,sK595,sK596))
| ~ spl643_17
| ~ spl643_36 ),
inference(trivial_inequality_removal,[],[f2875]) ).
tff(f2887,definition,
( spl643_37
<=> visSomeRawTable(vprojectCols(val1,sK595,sK596)) ),
introduced(definition,[new_symbols(definition,[spl643_37])],[avatar_definition]) ).
tff(f2889,plain,
( ~ visSomeRawTable(vprojectCols(val1,sK595,sK596))
| spl643_37 ),
inference(avatar_component_clause,[],[f2887]) ).
tff(f2891,definition,
( spl643_38
<=> visSomeRawTable(vfindCol(sK599,sK595,sK596)) ),
introduced(definition,[new_symbols(definition,[spl643_38])],[avatar_definition]) ).
tff(f2893,plain,
( ~ visSomeRawTable(vfindCol(sK599,sK595,sK596))
| spl643_38 ),
inference(avatar_component_clause,[],[f2891]) ).
tff(f2894,plain,
( ~ spl643_37
| ~ spl643_38
| ~ spl643_17
| ~ spl643_36 ),
inference(avatar_split_clause,[],[f2884,f2835,f2447,f2891,f2887]) ).
tff(f2909,plain,
( ( vnoRawTable = vfindCol(sK599,sK595,sK596) )
| spl643_38 ),
inference(resolution,[],[f2893,f1087]) ).
tff(f3254,definition,
( spl643_54
<=> visSomeTType(vprojectType(vlist(val1),sK600)) ),
introduced(definition,[new_symbols(definition,[spl643_54])],[avatar_definition]) ).
tff(f3256,plain,
( visSomeTType(vprojectType(vlist(val1),sK600))
| ~ spl643_54 ),
inference(avatar_component_clause,[],[f3254]) ).
tff(f3257,plain,
( spl643_54
| ~ spl643_4 ),
inference(avatar_split_clause,[],[f2242,f2211,f3254]) ).
tff(f3259,plain,
( ( vprojectType(vlist(val1),sK600) = vprojectType(vall,sK238(vprojectType(vlist(val1),sK600))) )
| ~ spl643_54 ),
inference(resolution,[],[f3256,f1971]) ).
tff(f3648,definition,
( spl643_72
<=> sP642(sK600) ),
introduced(definition,[new_symbols(definition,[spl643_72])],[avatar_definition]) ).
tff(f3650,plain,
( ~ sP642(sK600)
| spl643_72 ),
inference(avatar_component_clause,[],[f3648]) ).
tff(f3852,definition,
( spl643_82
<=> ( vnoRawTable = vfindCol(sK599,sK595,sK596) ) ),
introduced(definition,[new_symbols(definition,[spl643_82])],[avatar_definition]) ).
tff(f3854,plain,
( ( vnoRawTable = vfindCol(sK599,sK595,sK596) )
| ~ spl643_82 ),
inference(avatar_component_clause,[],[f3852]) ).
tff(f3855,plain,
( spl643_82
| spl643_38 ),
inference(avatar_split_clause,[],[f2909,f2891,f3852]) ).
tff(f3909,definition,
( spl643_87
<=> ! [X0: vRawTable] :
( ( vprojectCols(val1,sK595,X0) = vsomeRawTable(sK594(X0,sK595)) )
| ~ vwelltypedRawtable(sK600,X0) ) ),
introduced(definition,[new_symbols(definition,[spl643_87])],[avatar_definition]) ).
tff(f3910,plain,
( ! [X0: vRawTable] :
( ( vprojectCols(val1,sK595,X0) = vsomeRawTable(sK594(X0,sK595)) )
| ~ vwelltypedRawtable(sK600,X0) )
| ~ spl643_87 ),
inference(avatar_component_clause,[],[f3909]) ).
tff(f3911,plain,
( ~ spl643_72
| spl643_87
| ~ spl643_2 ),
inference(avatar_split_clause,[],[f2195,f2170,f3909,f3648]) ).
tff(f4054,definition,
( spl643_96
<=> ! [X0: vName,X1: vRawTable] :
( ( vfindCol(X0,sK595,X1) = vsomeRawTable(sK593(X1,sK595,X0)) )
| ~ vwelltypedRawtable(sK600,X1)
| ~ sP641(sK600,X0) ) ),
introduced(definition,[new_symbols(definition,[spl643_96])],[avatar_definition]) ).
tff(f4055,plain,
( ! [X0: vName,X1: vRawTable] :
( ( vfindCol(X0,sK595,X1) = vsomeRawTable(sK593(X1,sK595,X0)) )
| ~ vwelltypedRawtable(sK600,X1)
| ~ sP641(sK600,X0) )
| ~ spl643_96 ),
inference(avatar_component_clause,[],[f4054]) ).
tff(f4056,plain,
( spl643_96
| ~ spl643_2 ),
inference(avatar_split_clause,[],[f2194,f2170,f4054]) ).
tff(f4242,definition,
( spl643_117
<=> sP40(vacons(sK599,val1),sK600) ),
introduced(definition,[new_symbols(definition,[spl643_117])],[avatar_definition]) ).
tff(f4244,plain,
( sP40(vacons(sK599,val1),sK600)
| ~ spl643_117 ),
inference(avatar_component_clause,[],[f4242]) ).
tff(f4311,plain,
( spl643_117
| ~ spl643_4 ),
inference(avatar_split_clause,[],[f2255,f2211,f4242]) ).
tff(f4726,definition,
( spl643_140
<=> visSomeFType(vfindColType(sK599,sK600)) ),
introduced(definition,[new_symbols(definition,[spl643_140])],[avatar_definition]) ).
tff(f4728,plain,
( visSomeFType(vfindColType(sK599,sK600))
| ~ spl643_140 ),
inference(avatar_component_clause,[],[f4726]) ).
tff(f4729,plain,
( spl643_140
| ~ spl643_4 ),
inference(avatar_split_clause,[],[f2241,f2211,f4726]) ).
tff(f4974,plain,
( ( sK600 = sK508(vacons(sK599,val1),sK600) )
| ~ spl643_117 ),
inference(resolution,[],[f4244,f1751]) ).
tff(f4975,plain,
( ( vacons(sK599,val1) = vacons(sK506(vacons(sK599,val1),sK600),sK509(vacons(sK599,val1),sK600)) )
| ~ spl643_117 ),
inference(resolution,[],[f4244,f1752]) ).
tff(f4983,definition,
( spl643_145
<=> ( sK600 = sK508(vacons(sK599,val1),sK600) ) ),
introduced(definition,[new_symbols(definition,[spl643_145])],[avatar_definition]) ).
tff(f4985,plain,
( ( sK600 = sK508(vacons(sK599,val1),sK600) )
| ~ spl643_145 ),
inference(avatar_component_clause,[],[f4983]) ).
tff(f4986,plain,
( spl643_145
| ~ spl643_117 ),
inference(avatar_split_clause,[],[f4974,f4242,f4983]) ).
tff(f4988,plain,
( ( sK507(vacons(sK599,val1),sK600) = vfindColType(sK506(vacons(sK599,val1),sK600),sK600) )
| ~ sP40(vacons(sK599,val1),sK600)
| ~ spl643_145 ),
inference(superposition,[],[f1756,f4985]) ).
tff(f4989,plain,
( ( sK507(vacons(sK599,val1),sK600) = vfindColType(sK506(vacons(sK599,val1),sK600),sK600) )
| ~ spl643_117
| ~ spl643_145 ),
inference(forward_subsumption_resolution,[],[f4988,f4244]) ).
tff(f5069,definition,
( spl643_147
<=> ( sK507(vacons(sK599,val1),sK600) = vfindColType(sK506(vacons(sK599,val1),sK600),sK600) ) ),
introduced(definition,[new_symbols(definition,[spl643_147])],[avatar_definition]) ).
tff(f5071,plain,
( ( sK507(vacons(sK599,val1),sK600) = vfindColType(sK506(vacons(sK599,val1),sK600),sK600) )
| ~ spl643_147 ),
inference(avatar_component_clause,[],[f5069]) ).
tff(f5072,plain,
( spl643_147
| ~ spl643_117
| ~ spl643_145 ),
inference(avatar_split_clause,[],[f4989,f4983,f4242,f5069]) ).
tff(f5085,plain,
( ! [X0: vFType] :
( ( vsomeFType(X0) != sK507(vacons(sK599,val1),sK600) )
| sP641(sK600,sK506(vacons(sK599,val1),sK600)) )
| ~ spl643_147 ),
inference(superposition,[],[f2138,f5071]) ).
tff(f5121,plain,
( ( vfindColType(sK599,sK600) = vsomeFType(sK496(vfindColType(sK599,sK600))) )
| ~ spl643_140 ),
inference(resolution,[],[f4728,f1725]) ).
tff(f5784,definition,
( spl643_164
<=> ( vacons(sK599,val1) = vacons(sK506(vacons(sK599,val1),sK600),sK509(vacons(sK599,val1),sK600)) ) ),
introduced(definition,[new_symbols(definition,[spl643_164])],[avatar_definition]) ).
tff(f5786,plain,
( ( vacons(sK599,val1) = vacons(sK506(vacons(sK599,val1),sK600),sK509(vacons(sK599,val1),sK600)) )
| ~ spl643_164 ),
inference(avatar_component_clause,[],[f5784]) ).
tff(f5787,plain,
( spl643_164
| ~ spl643_117 ),
inference(avatar_split_clause,[],[f4975,f4242,f5784]) ).
tff(f5792,plain,
( ! [X0: vName,X1: vAttrL] :
( ( vacons(X0,X1) != vacons(sK599,val1) )
| ( sK506(vacons(sK599,val1),sK600) = X0 ) )
| ~ spl643_164 ),
inference(superposition,[],[f941,f5786]) ).
tff(f5868,definition,
( spl643_167
<=> ( sK599 = sK506(vacons(sK599,val1),sK600) ) ),
introduced(definition,[new_symbols(definition,[spl643_167])],[avatar_definition]) ).
tff(f5870,plain,
( ( sK599 = sK506(vacons(sK599,val1),sK600) )
| ~ spl643_167 ),
inference(avatar_component_clause,[],[f5868]) ).
tff(f5980,definition,
( spl643_171
<=> ! [X0: vName,X1: vAttrL] :
( ( vacons(X0,X1) != vacons(sK599,val1) )
| ( sK506(vacons(sK599,val1),sK600) = X0 ) ) ),
introduced(definition,[new_symbols(definition,[spl643_171])],[avatar_definition]) ).
tff(f5981,plain,
( ! [X0: vName,X1: vAttrL] :
( ( vacons(X0,X1) != vacons(sK599,val1) )
| ( sK506(vacons(sK599,val1),sK600) = X0 ) )
| ~ spl643_171 ),
inference(avatar_component_clause,[],[f5980]) ).
tff(f5982,plain,
( spl643_171
| ~ spl643_164 ),
inference(avatar_split_clause,[],[f5792,f5784,f5980]) ).
tff(f6021,plain,
( ( sK599 = sK506(vacons(sK599,val1),sK600) )
| ~ spl643_171 ),
inference(equality_resolution,[],[f5981]) ).
tff(f6061,plain,
( spl643_167
| ~ spl643_171 ),
inference(avatar_split_clause,[],[f6021,f5980,f5868]) ).
tff(f6066,plain,
( ( vfindColType(sK599,sK600) = sK507(vacons(sK599,val1),sK600) )
| ~ spl643_147
| ~ spl643_167 ),
inference(superposition,[],[f5071,f5870]) ).
tff(f6119,plain,
( ! [X0: vName,X1: vRawTable] :
( ( vnoRawTable != vfindCol(X0,sK595,X1) )
| ~ vwelltypedRawtable(sK600,X1)
| ~ sP641(sK600,X0) )
| ~ spl643_96 ),
inference(superposition,[],[f875,f4055]) ).
tff(f6439,plain,
( ! [X0: vTType] : ( vprojectType(vall,X0) != vprojectType(vlist(val1),sK600) )
| spl643_72 ),
inference(resolution,[],[f3650,f2140]) ).
tff(f6441,plain,
( $false
| ~ spl643_54
| spl643_72 ),
inference(backward_subsumption_resolution,[],[f3259,f6439]) ).
tff(f6442,plain,
( ~ spl643_54
| spl643_72 ),
inference(avatar_contradiction_clause,[],[f6441]) ).
tff(f6463,plain,
( ! [X0: vRawTable] :
( visSomeRawTable(vprojectCols(val1,sK595,X0))
| ~ vwelltypedRawtable(sK600,X0) )
| ~ spl643_87 ),
inference(superposition,[],[f1085,f3910]) ).
tff(f6470,definition,
( spl643_178
<=> ! [X0: vRawTable] :
( visSomeRawTable(vprojectCols(val1,sK595,X0))
| ~ vwelltypedRawtable(sK600,X0) ) ),
introduced(definition,[new_symbols(definition,[spl643_178])],[avatar_definition]) ).
tff(f6471,plain,
( ! [X0: vRawTable] :
( visSomeRawTable(vprojectCols(val1,sK595,X0))
| ~ vwelltypedRawtable(sK600,X0) )
| ~ spl643_178 ),
inference(avatar_component_clause,[],[f6470]) ).
tff(f6472,plain,
( spl643_178
| ~ spl643_87 ),
inference(avatar_split_clause,[],[f6463,f3909,f6470]) ).
tff(f15267,definition,
( spl643_429
<=> ( vfindColType(sK599,sK600) = sK507(vacons(sK599,val1),sK600) ) ),
introduced(definition,[new_symbols(definition,[spl643_429])],[avatar_definition]) ).
tff(f15269,plain,
( ( vfindColType(sK599,sK600) = sK507(vacons(sK599,val1),sK600) )
| ~ spl643_429 ),
inference(avatar_component_clause,[],[f15267]) ).
tff(f15270,plain,
( spl643_429
| ~ spl643_147
| ~ spl643_167 ),
inference(avatar_split_clause,[],[f6066,f5868,f5069,f15267]) ).
tff(f18962,definition,
( spl643_543
<=> ! [X0: vName,X1: vRawTable] :
( ( vnoRawTable != vfindCol(X0,sK595,X1) )
| ~ vwelltypedRawtable(sK600,X1)
| ~ sP641(sK600,X0) ) ),
introduced(definition,[new_symbols(definition,[spl643_543])],[avatar_definition]) ).
tff(f18963,plain,
( ! [X0: vName,X1: vRawTable] :
( ( vnoRawTable != vfindCol(X0,sK595,X1) )
| ~ vwelltypedRawtable(sK600,X1)
| ~ sP641(sK600,X0) )
| ~ spl643_543 ),
inference(avatar_component_clause,[],[f18962]) ).
tff(f18964,plain,
( spl643_543
| ~ spl643_96 ),
inference(avatar_split_clause,[],[f6119,f4054,f18962]) ).
tff(f20073,definition,
( spl643_570
<=> sP641(sK600,sK506(vacons(sK599,val1),sK600)) ),
introduced(definition,[new_symbols(definition,[spl643_570])],[avatar_definition]) ).
tff(f20075,plain,
( sP641(sK600,sK506(vacons(sK599,val1),sK600))
| ~ spl643_570 ),
inference(avatar_component_clause,[],[f20073]) ).
tff(f20077,definition,
( spl643_571
<=> ! [X0: vFType] : ( vsomeFType(X0) != sK507(vacons(sK599,val1),sK600) ) ),
introduced(definition,[new_symbols(definition,[spl643_571])],[avatar_definition]) ).
tff(f20078,plain,
( ! [X0: vFType] : ( vsomeFType(X0) != sK507(vacons(sK599,val1),sK600) )
| ~ spl643_571 ),
inference(avatar_component_clause,[],[f20077]) ).
tff(f20079,plain,
( spl643_570
| spl643_571
| ~ spl643_147 ),
inference(avatar_split_clause,[],[f5085,f5069,f20077,f20073]) ).
tff(f20080,plain,
( ! [X0: vFType] : ( vsomeFType(X0) != vfindColType(sK599,sK600) )
| ~ spl643_429
| ~ spl643_571 ),
inference(forward_demodulation,[],[f20078,f15269]) ).
tff(f20082,plain,
( $false
| ~ spl643_140
| ~ spl643_429
| ~ spl643_571 ),
inference(backward_subsumption_resolution,[],[f5121,f20080]) ).
tff(f20083,plain,
( ~ spl643_140
| ~ spl643_429
| ~ spl643_571 ),
inference(avatar_contradiction_clause,[],[f20082]) ).
tff(f20084,plain,
( sP641(sK600,sK599)
| ~ spl643_167
| ~ spl643_570 ),
inference(forward_demodulation,[],[f20075,f5870]) ).
tff(f24994,plain,
( ( vnoRawTable != vnoRawTable )
| ~ vwelltypedRawtable(sK600,sK596)
| ~ sP641(sK600,sK599)
| ~ spl643_82
| ~ spl643_543 ),
inference(superposition,[],[f18963,f3854]) ).
tff(f25020,plain,
( ~ vwelltypedRawtable(sK600,sK596)
| ~ sP641(sK600,sK599)
| ~ spl643_82
| ~ spl643_543 ),
inference(trivial_inequality_removal,[],[f24994]) ).
tff(f25025,plain,
( ~ sP641(sK600,sK599)
| ~ spl643_3
| ~ spl643_82
| ~ spl643_543 ),
inference(forward_subsumption_resolution,[],[f25020,f2177]) ).
tff(f25029,plain,
( $false
| ~ spl643_3
| ~ spl643_82
| ~ spl643_167
| ~ spl643_543
| ~ spl643_570 ),
inference(forward_subsumption_resolution,[],[f25025,f20084]) ).
tff(f25030,plain,
( ~ spl643_3
| ~ spl643_82
| ~ spl643_167
| ~ spl643_543
| ~ spl643_570 ),
inference(avatar_contradiction_clause,[],[f25029]) ).
tff(f25036,plain,
( ~ vwelltypedRawtable(sK600,sK596)
| spl643_37
| ~ spl643_178 ),
inference(resolution,[],[f2889,f6471]) ).
tff(f25043,plain,
( $false
| ~ spl643_3
| spl643_37
| ~ spl643_178 ),
inference(forward_subsumption_resolution,[],[f25036,f2177]) ).
tff(f25044,plain,
( ~ spl643_3
| spl643_37
| ~ spl643_178 ),
inference(avatar_contradiction_clause,[],[f25043]) ).
cnf(s1,plain,
spl643_1,
inference(sat_conversion,[],[f2145]) ).
cnf(s2,plain,
spl643_2,
inference(sat_conversion,[],[f2173]) ).
cnf(s3,plain,
spl643_3,
inference(sat_conversion,[],[f2178]) ).
cnf(s4,plain,
spl643_4,
inference(sat_conversion,[],[f2214]) ).
cnf(s15,plain,
( ~ spl643_1
| spl643_16 ),
inference(sat_conversion,[],[f2432]) ).
cnf(s16,plain,
( ~ spl643_16
| spl643_17 ),
inference(sat_conversion,[],[f2450]) ).
cnf(s33,plain,
( ~ spl643_1
| spl643_35 ),
inference(sat_conversion,[],[f2832]) ).
cnf(s34,plain,
( ~ spl643_17
| ~ spl643_35
| spl643_36 ),
inference(sat_conversion,[],[f2837]) ).
cnf(s35,plain,
( ~ spl643_17
| ~ spl643_36
| ~ spl643_37
| ~ spl643_38 ),
inference(sat_conversion,[],[f2894]) ).
cnf(s50,plain,
( ~ spl643_4
| spl643_54 ),
inference(sat_conversion,[],[f3257]) ).
cnf(s75,plain,
( spl643_38
| spl643_82 ),
inference(sat_conversion,[],[f3855]) ).
cnf(s79,plain,
( ~ spl643_2
| ~ spl643_72
| spl643_87 ),
inference(sat_conversion,[],[f3911]) ).
cnf(s89,plain,
( ~ spl643_2
| spl643_96 ),
inference(sat_conversion,[],[f4056]) ).
cnf(s119,plain,
( ~ spl643_4
| spl643_117 ),
inference(sat_conversion,[],[f4311]) ).
cnf(s145,plain,
( ~ spl643_4
| spl643_140 ),
inference(sat_conversion,[],[f4729]) ).
cnf(s153,plain,
( ~ spl643_117
| spl643_145 ),
inference(sat_conversion,[],[f4986]) ).
cnf(s155,plain,
( ~ spl643_117
| ~ spl643_145
| spl643_147 ),
inference(sat_conversion,[],[f5072]) ).
cnf(s172,plain,
( ~ spl643_117
| spl643_164 ),
inference(sat_conversion,[],[f5787]) ).
cnf(s178,plain,
( ~ spl643_164
| spl643_171 ),
inference(sat_conversion,[],[f5982]) ).
cnf(s179,plain,
( spl643_167
| ~ spl643_171 ),
inference(sat_conversion,[],[f6061]) ).
cnf(s185,plain,
( ~ spl643_54
| spl643_72 ),
inference(sat_conversion,[],[f6442]) ).
cnf(s187,plain,
( ~ spl643_87
| spl643_178 ),
inference(sat_conversion,[],[f6472]) ).
cnf(s444,plain,
( ~ spl643_147
| ~ spl643_167
| spl643_429 ),
inference(sat_conversion,[],[f15270]) ).
cnf(s554,plain,
( ~ spl643_96
| spl643_543 ),
inference(sat_conversion,[],[f18964]) ).
cnf(s581,plain,
( ~ spl643_147
| spl643_570
| spl643_571 ),
inference(sat_conversion,[],[f20079]) ).
cnf(s582,plain,
( ~ spl643_140
| ~ spl643_429
| ~ spl643_571 ),
inference(sat_conversion,[],[f20083]) ).
cnf(s675,plain,
( ~ spl643_3
| ~ spl643_82
| ~ spl643_167
| ~ spl643_543
| ~ spl643_570 ),
inference(sat_conversion,[],[f25030]) ).
cnf(s677,plain,
( ~ spl643_3
| spl643_37
| ~ spl643_178 ),
inference(sat_conversion,[],[f25044]) ).
cnf(s702,plain,
spl643_140,
inference(rat,[],[s145,s4]) ).
cnf(s703,plain,
spl643_117,
inference(rat,[],[s119,s4]) ).
cnf(s704,plain,
spl643_54,
inference(rat,[],[s50,s4]) ).
cnf(s708,plain,
spl643_164,
inference(rat,[],[s172,s703]) ).
cnf(s713,plain,
spl643_145,
inference(rat,[],[s153,s703]) ).
cnf(s715,plain,
spl643_72,
inference(rat,[],[s185,s704]) ).
cnf(s717,plain,
spl643_171,
inference(rat,[],[s178,s708]) ).
cnf(s723,plain,
spl643_147,
inference(rat,[],[s155,s703,s713]) ).
cnf(s726,plain,
spl643_167,
inference(rat,[],[s179,s717]) ).
cnf(s742,plain,
spl643_429,
inference(rat,[],[s444,s723,s726]) ).
cnf(s746,plain,
~ spl643_571,
inference(rat,[],[s582,s702,s742]) ).
cnf(s748,plain,
spl643_570,
inference(rat,[],[s581,s723,s746]) ).
cnf(s766,plain,
spl643_96,
inference(rat,[],[s89,s2]) ).
cnf(s768,plain,
spl643_87,
inference(rat,[],[s79,s715,s2]) ).
cnf(s791,plain,
spl643_543,
inference(rat,[],[s554,s766]) ).
cnf(s799,plain,
spl643_178,
inference(rat,[],[s187,s768]) ).
cnf(s823,plain,
~ spl643_82,
inference(rat,[],[s675,s748,s3,s726,s791]) ).
cnf(s826,plain,
spl643_37,
inference(rat,[],[s677,s3,s799]) ).
cnf(s831,plain,
spl643_38,
inference(rat,[],[s75,s823]) ).
cnf(s884,plain,
spl643_35,
inference(rat,[],[s33,s1]) ).
cnf(s888,plain,
spl643_16,
inference(rat,[],[s15,s1]) ).
cnf(s891,plain,
spl643_17,
inference(rat,[],[s16,s888]) ).
cnf(s908,plain,
~ spl643_36,
inference(rat,[],[s35,s831,s826,s891]) ).
cnf(s909,plain,
$false,
inference(rat,[],[s34,s884,s908,s891]) ).
tff(f25045,plain,
$false,
inference(avatar_sat_refutation,[],[s909]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : COM302_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.27 % Computer : n008.cluster.edu
% 0.10/0.27 % Model : x86_64 x86_64
% 0.10/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.27 % Memory : 8046.5625MB
% 0.10/0.27 % OS : Linux 6.8.0-71-generic
% 0.10/0.27 % CPULimit : 300
% 0.10/0.27 % WCLimit : 300
% 0.10/0.27 % DateTime : Mon Sep 28 22:05:24 UTC 2026
% 0.10/0.27 % CPUTime :
% 0.10/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.28/0.33 Running first-order theorem proving
% 0.28/0.33 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
% 24.89/4.48 % (2707357)Detected formulas, will run a generic FOF schedule.
% 24.89/4.48 % (2707362)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=482642330:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 24.89/4.48 % (2707363)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=1043381348:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 24.89/4.48 % (2707368)dis-21_1_sil=8000:lcm=predicate:random_seed=1405389526: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)
% 24.89/4.48 % (2707366)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4193662116:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 24.89/4.48 % (2707367)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1484792485:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 24.89/4.48 % (2707365)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3613517005:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 24.89/4.48 % (2707364)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=1965902250:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 24.89/4.48 % (2707365)Refutation not found, incomplete strategy
% 24.89/4.48 % (2707365)------------------------------
% 24.89/4.48 % (2707365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.48 % (2707365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.48 % (2707365)CaDiCaL version: 2.1.3
% 24.89/4.48 % (2707365)Termination reason: Refutation not found, incomplete strategy
% 24.89/4.48 % (2707365)Time elapsed: 0.006 s
% 24.89/4.48 % (2707365)Peak memory usage: 89 MB
% 24.89/4.48 % (2707365)Instructions burned: 4 (million)
% 24.89/4.48 % (2707366)Instruction limit reached!
% 24.89/4.48 % (2707366)------------------------------
% 24.89/4.48 % (2707366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.48 % (2707366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.48 % (2707366)CaDiCaL version: 2.1.3
% 24.89/4.48 % (2707366)Termination reason: Instruction limit
% 24.89/4.48 % (2707366)Termination phase: Saturation
% 24.89/4.48 % (2707366)Time elapsed: 0.114 s
% 24.89/4.48 % (2707366)Peak memory usage: 88 MB
% 24.89/4.48 % (2707366)Instructions burned: 119 (million)
% 24.89/4.48 % (2707368)Instruction limit reached!
% 24.89/4.48 % (2707368)------------------------------
% 24.89/4.48 % (2707368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.48 % (2707368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.48 % (2707368)CaDiCaL version: 2.1.3
% 24.89/4.48 % (2707368)Termination reason: Instruction limit
% 24.89/4.48 % (2707368)Termination phase: Saturation
% 24.89/4.48 % (2707368)Time elapsed: 0.121 s
% 24.89/4.48 % (2707368)Peak memory usage: 91 MB
% 24.89/4.48 % (2707368)Instructions burned: 130 (million)
% 24.89/4.48 % (2707367)Instruction limit reached!
% 24.89/4.48 % (2707367)------------------------------
% 24.89/4.48 % (2707367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.89/4.48 % (2707367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.89/4.48 % (2707367)CaDiCaL version: 2.1.3
% 24.89/4.48 % (2707367)Termination reason: Instruction limit
% 24.89/4.48 % (2707367)Termination phase: Saturation
% 24.89/4.48 % (2707367)Time elapsed: 0.143 s
% 24.89/4.48 % (2707367)Peak memory usage: 90 MB
% 24.89/4.48 % (2707367)Instructions burned: 139 (million)
% 24.89/4.48 % (2707376)lrs+10_1_sil=8000:sp=occurrence:random_seed=4023921160:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 24.89/4.48 % (2707377)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2763343120:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 24.89/4.48 % (2707365)------------------------------
% 24.89/4.48 % (2707365)------------------------------
% 24.89/4.48 % (2707378)lrs+1011_1_sil=32000:sp=occurrence:random_seed=287934148:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 24.89/4.48 % (2707377)Instruction limit reached!
% 24.89/4.48 % (2707377)------------------------------
% 24.89/4.48 % (2707377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.93/5.99 % (2707377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.93/5.99 % (2707377)CaDiCaL version: 2.1.3
% 34.93/5.99 % (2707377)Termination reason: Instruction limit
% 34.93/5.99 % (2707377)Termination phase: Saturation
% 34.93/5.99 % (2707377)Time elapsed: 0.126 s
% 34.93/5.99 % (2707377)Peak memory usage: 90 MB
% 34.93/5.99 % (2707377)Instructions burned: 158 (million)
% 34.93/5.99 % (2707376)Instruction limit reached!
% 34.93/5.99 % (2707376)------------------------------
% 34.93/5.99 % (2707376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.93/5.99 % (2707376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.93/5.99 % (2707376)CaDiCaL version: 2.1.3
% 34.93/5.99 % (2707376)Termination reason: Instruction limit
% 34.93/5.99 % (2707376)Termination phase: Saturation
% 34.93/5.99 % (2707376)Time elapsed: 0.290 s
% 34.93/5.99 % (2707376)Peak memory usage: 92 MB
% 34.93/5.99 % (2707376)Instructions burned: 285 (million)
% 34.93/5.99 % (2707381)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=2990797919:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 34.93/5.99 % (2707378)Instruction limit reached!
% 34.93/5.99 % (2707378)------------------------------
% 34.93/5.99 % (2707378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.93/5.99 % (2707378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.93/5.99 % (2707378)CaDiCaL version: 2.1.3
% 34.93/5.99 % (2707378)Termination reason: Instruction limit
% 34.93/5.99 % (2707378)Termination phase: Saturation
% 34.93/5.99 % (2707378)Time elapsed: 0.325 s
% 34.93/5.99 % (2707378)Peak memory usage: 91 MB
% 34.93/5.99 % (2707378)Instructions burned: 325 (million)
% 34.93/5.99 % (2707383)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4226116162:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 34.93/5.99 % (2707381)Instruction limit reached!
% 34.93/5.99 % (2707381)------------------------------
% 34.93/5.99 % (2707381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.93/5.99 % (2707381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.93/5.99 % (2707381)CaDiCaL version: 2.1.3
% 34.93/5.99 % (2707381)Termination reason: Instruction limit
% 34.93/5.99 % (2707381)Termination phase: Saturation
% 34.93/5.99 % (2707381)Time elapsed: 0.262 s
% 34.93/5.99 % (2707381)Peak memory usage: 92 MB
% 34.93/5.99 % (2707381)Instructions burned: 249 (million)
% 34.93/5.99 % (2707385)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1722480775:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 34.93/5.99 % (2707386)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1433815866:cts=off:i=113:fsr=off:ss=included:sgt=4_2989 on theBenchmark for (2989ds/113Mi)
% 34.93/5.99 % (2707383)Instruction limit reached!
% 34.93/5.99 % (2707383)------------------------------
% 34.93/5.99 % (2707383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.93/5.99 % (2707383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.93/5.99 % (2707383)CaDiCaL version: 2.1.3
% 34.93/5.99 % (2707383)Termination reason: Instruction limit
% 34.93/5.99 % (2707383)Termination phase: Saturation
% 34.93/5.99 % (2707383)Time elapsed: 0.297 s
% 34.93/5.99 % (2707383)Peak memory usage: 92 MB
% 34.93/5.99 % (2707383)Instructions burned: 294 (million)
% 34.93/5.99 % (2707386)Instruction limit reached!
% 34.93/5.99 % (2707386)------------------------------
% 34.93/5.99 % (2707386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.93/5.99 % (2707386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.93/5.99 % (2707386)CaDiCaL version: 2.1.3
% 34.93/5.99 % (2707386)Termination reason: Instruction limit
% 34.93/5.99 % (2707386)Termination phase: Saturation
% 34.93/5.99 % (2707386)Time elapsed: 0.114 s
% 34.93/5.99 % (2707386)Peak memory usage: 91 MB
% 34.93/5.99 % (2707386)Instructions burned: 113 (million)
% 34.93/5.99 % (2707388)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3831277082:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 34.93/5.99 % (2707388)Instruction limit reached!
% 34.93/5.99 % (2707388)------------------------------
% 34.93/5.99 % (2707388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.93/5.99 % (2707388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.93/5.99 % (2707388)CaDiCaL version: 2.1.3
% 27.57/8.21 % (2707388)Termination reason: Instruction limit
% 27.57/8.21 % (2707388)Termination phase: Saturation
% 27.57/8.21 % (2707388)Time elapsed: 0.116 s
% 27.57/8.21 % (2707388)Peak memory usage: 90 MB
% 27.57/8.21 % (2707388)Instructions burned: 128 (million)
% 27.57/8.21 % (2707391)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3966318821:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 27.57/8.21 % (2707392)lrs+10_1_sil=8000:sp=occurrence:random_seed=4270148885:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 27.57/8.21 % (2707391)Instruction limit reached!
% 27.57/8.21 % (2707391)------------------------------
% 27.57/8.21 % (2707391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.57/8.21 % (2707391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.57/8.21 % (2707391)CaDiCaL version: 2.1.3
% 27.57/8.21 % (2707391)Termination reason: Instruction limit
% 27.57/8.21 % (2707391)Termination phase: Saturation
% 27.57/8.21 % (2707391)Time elapsed: 0.103 s
% 27.57/8.21 % (2707391)Peak memory usage: 89 MB
% 27.57/8.21 % (2707391)Instructions burned: 114 (million)
% 27.57/8.21 % (2707395)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=945089318:i=437:sd=1:aac=none:ss=included_2983 on theBenchmark for (2983ds/437Mi)
% 27.57/8.21 % (2707397)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3379195303:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 27.57/8.21 % (2707395)Instruction limit reached!
% 27.57/8.21 % (2707395)------------------------------
% 27.57/8.21 % (2707395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.57/8.21 % (2707395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.57/8.21 % (2707395)CaDiCaL version: 2.1.3
% 27.57/8.21 % (2707395)Termination reason: Instruction limit
% 27.57/8.21 % (2707395)Termination phase: Saturation
% 27.57/8.21 % (2707395)Time elapsed: 0.429 s
% 27.57/8.21 % (2707395)Peak memory usage: 93 MB
% 27.57/8.21 % (2707395)Instructions burned: 438 (million)
% 27.57/8.21 % (2707392)Instruction limit reached!
% 27.57/8.21 % (2707392)------------------------------
% 27.57/8.21 % (2707392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.57/8.21 % (2707392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.57/8.21 % (2707392)CaDiCaL version: 2.1.3
% 27.57/8.21 % (2707392)Termination reason: Instruction limit
% 27.57/8.21 % (2707392)Termination phase: Saturation
% 27.57/8.21 % (2707392)Time elapsed: 0.827 s
% 27.57/8.21 % (2707392)Peak memory usage: 97 MB
% 27.57/8.21 % (2707392)Instructions burned: 908 (million)
% 27.57/8.21 % (2707400)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2174976255:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2976 on theBenchmark for (2976ds/134Mi)
% 27.57/8.21 % (2707400)Instruction limit reached!
% 27.57/8.21 % (2707400)------------------------------
% 27.57/8.21 % (2707400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.57/8.21 % (2707400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.57/8.21 % (2707400)CaDiCaL version: 2.1.3
% 27.57/8.21 % (2707400)Termination reason: Instruction limit
% 27.57/8.21 % (2707400)Termination phase: Saturation
% 27.57/8.21 % (2707400)Time elapsed: 0.113 s
% 27.57/8.21 % (2707400)Peak memory usage: 90 MB
% 27.57/8.21 % (2707400)Instructions burned: 134 (million)
% 27.57/8.21 % (2707401)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1205943387:st=8:i=592:sd=3:ep=RST:ss=axioms_2975 on theBenchmark for (2975ds/592Mi)
% 27.57/8.21 % (2707403)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3651911917:st=3:i=13193:sd=3:ss=axioms_2972 on theBenchmark for (2972ds/13193Mi)
% 27.57/8.21 % (2707401)Instruction limit reached!
% 27.57/8.21 % (2707401)------------------------------
% 27.57/8.21 % (2707401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.57/8.21 % (2707401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.57/8.21 % (2707401)CaDiCaL version: 2.1.3
% 27.57/8.21 % (2707401)Termination reason: Instruction limit
% 27.57/8.21 % (2707401)Termination phase: Saturation
% 27.57/8.21 % (2707401)Time elapsed: 0.477 s
% 27.57/8.21 % (2707401)Peak memory usage: 92 MB
% 27.57/8.21 % (2707401)Instructions burned: 593 (million)
% 27.57/8.21 % (2707406)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=1455082193:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/125Mi)
% 27.57/8.21 % (2707406)Instruction limit reached!
% 27.57/8.21 % (2707406)------------------------------
% 27.57/8.21 % (2707406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.57/8.21 % (2707406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.57/8.21 % (2707406)CaDiCaL version: 2.1.3
% 27.57/8.21 % (2707406)Termination reason: Instruction limit
% 27.57/8.21 % (2707406)Termination phase: Saturation
% 27.57/8.21 % (2707406)Time elapsed: 0.123 s
% 27.57/8.21 % (2707406)Peak memory usage: 92 MB
% 27.57/8.21 % (2707406)Instructions burned: 125 (million)
% 27.57/8.21 % (2707385)Instruction limit reached!
% 27.57/8.21 % (2707385)------------------------------
% 27.57/8.21 % (2707385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.57/8.21 % (2707385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.57/8.21 % (2707385)CaDiCaL version: 2.1.3
% 27.57/8.21 % (2707385)Termination reason: Instruction limit
% 27.57/8.21 % (2707385)Termination phase: Saturation
% 27.57/8.21 % (2707385)Time elapsed: 2.449 s
% 27.57/8.21 % (2707385)Peak memory usage: 142 MB
% 27.57/8.21 % (2707385)Instructions burned: 2350 (million)
% 27.57/8.21 % (2707408)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2493827896:i=134:gtgl=5:slsql=off:gtg=exists_sym_2963 on theBenchmark for (2963ds/134Mi)
% 27.57/8.21 % (2707409)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=708087937:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2962 on theBenchmark for (2962ds/141Mi)
% 27.57/8.21 % (2707409)Refutation not found, incomplete strategy
% 27.57/8.21 % (2707409)------------------------------
% 27.57/8.21 % (2707409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.57/8.21 % (2707409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.57/8.21 % (2707409)CaDiCaL version: 2.1.3
% 27.57/8.21 % (2707409)Termination reason: Refutation not found, incomplete strategy
% 27.57/8.21 % (2707409)Time elapsed: 0.010 s
% 27.57/8.21 % (2707409)Peak memory usage: 89 MB
% 27.57/8.21 % (2707409)Instructions burned: 9 (million)
% 27.57/8.21 % (2707408)Instruction limit reached!
% 27.57/8.21 % (2707408)------------------------------
% 27.57/8.21 % (2707408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.57/8.21 % (2707408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.57/8.21 % (2707408)CaDiCaL version: 2.1.3
% 27.57/8.21 % (2707408)Termination reason: Instruction limit
% 27.57/8.21 % (2707408)Termination phase: Saturation
% 27.57/8.21 % (2707408)Time elapsed: 0.130 s
% 27.57/8.21 % (2707408)Peak memory usage: 91 MB
% 27.57/8.21 % (2707408)Instructions burned: 134 (million)
% 27.57/8.21 % (2707412)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3026446673:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2959 on theBenchmark for (2959ds/431Mi)
% 27.57/8.21 % (2707412)Refutation not found, incomplete strategy
% 27.57/8.21 % (2707412)------------------------------
% 27.57/8.21 % (2707412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.57/8.21 % (2707412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.57/8.21 % (2707412)CaDiCaL version: 2.1.3
% 27.57/8.21 % (2707412)Termination reason: Refutation not found, incomplete strategy
% 27.57/8.21 % (2707412)Time elapsed: 0.010 s
% 27.57/8.21 % (2707412)Peak memory usage: 89 MB
% 27.57/8.21 % (2707412)Instructions burned: 13 (million)
% 27.57/8.21 % (2707409)------------------------------
% 27.57/8.21 % (2707409)------------------------------
% 27.57/8.21 % (2707412)------------------------------
% 27.57/8.21 % (2707412)------------------------------
% 27.57/8.21 % (2707414)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=3564742059:i=6060:aac=none:ins=25_2955 on theBenchmark for (2955ds/6060Mi)
% 27.57/8.21 % (2707416)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=1377142232:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2952 on theBenchmark for (2952ds/150Mi)
% 27.57/8.21 % (2707416)Instruction limit reached!
% 27.57/8.21 % (2707416)------------------------------
% 27.57/8.21 % (2707416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.57/8.21 % (2707416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.57/8.21 % (2707416)CaDiCaL version: 2.1.3
% 27.57/8.21 % (2707416)Termination reason: Instruction limit
% 27.57/8.21 % (2707416)Termination phase: Saturation
% 27.57/8.21 % (2707416)Time elapsed: 0.123 s
% 27.57/8.21 % (2707416)Peak memory usage: 92 MB
% 27.57/8.21 % (2707416)Instructions burned: 150 (million)
% 27.57/8.21 % (2707418)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2824300804:i=14155:bd=all_2949 on theBenchmark for (2949ds/14155Mi)
% 27.57/8.21 % (2707364)First to succeed.
% 27.57/8.21 % (2707364)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2707357"
% 27.57/8.21 % (2707397)Instruction limit reached!
% 27.57/8.21 % (2707397)------------------------------
% 27.57/8.21 % (2707397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.57/8.21 % (2707397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.57/8.21 % (2707397)CaDiCaL version: 2.1.3
% 27.57/8.21 % (2707397)Termination reason: Instruction limit
% 27.57/8.21 % (2707397)Termination phase: Saturation
% 27.57/8.21 % (2707397)Time elapsed: 4.988 s
% 27.57/8.21 % (2707397)Peak memory usage: 161 MB
% 27.57/8.21 % (2707397)Instructions burned: 5202 (million)
% 27.57/8.21 % (2707364)Refutation found. Thanks to Tanya!
% 27.57/8.21 % SZS status Theorem for theBenchmark
% 27.57/8.21 % SZS output start Proof for theBenchmark
% See solution above
% 52.13/8.47 % (2707364)------------------------------
% 52.13/8.47 % (2707364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.13/8.47 % (2707364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.13/8.47 % (2707364)CaDiCaL version: 2.1.3
% 52.13/8.47 % (2707364)Termination reason: Refutation
% 52.13/8.47 % (2707364)Time elapsed: 6.503 s
% 52.13/8.47 % (2707364)Peak memory usage: 179 MB
% 52.13/8.47 % (2707364)Instructions burned: 6356 (million)
% 52.13/8.47 % (2707364)------------------------------
% 52.13/8.47 % (2707364)------------------------------
% 52.13/8.47 % (2707357)Success in time 7.263 s
% 52.13/8.47 % Vampire exiting
%------------------------------------------------------------------------------