% SZS start RequiredInformation
% Congratulations - you have become a registered power user of SystemOnTPTP, at IP address 89.186.28.63.
% Please consider donating to the TPTP project - see www.tptp.org for details.
% When you donate this message will disappear.
% If you do not donate a random delay might be added to your processing time.
% SZS end RequiredInformation
% START OF SYSTEM OUTPUT
------- cvc4-fof 1.5pre2 : /tmp/SystemOnTPTPFormReply38382/SOT_bhnA_a at ...
--- Run --relevant-triggers --full-saturate-quant at 15...
% 10 wall clock seconds gone, waiting for system output
--- Run --no-e-matching --full-saturate-quant at 15...
% 20 wall clock seconds gone, waiting for system output
% 30 wall clock seconds gone, waiting for system output
--- Run --finite-model-find --quant-cf --qcf-all-conflict --sort-inference --uf-ss-fair at 15...
% SZS status Theorem for SOT_bhnA_a
% SZS output start Proof for SOT_bhnA_a
Skolem constants of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (= (txtpt X Y T) (and (pt X Y T) (txt X T) (txt Y T))) ) : 
  ( skv_1, skv_2, skv_3 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phtxt Y skv_1)) (not (txtdep skv_1 Y))) ) : 
  ( skv_90 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_1)) (overlap V skv_1 skv_1)) ) : 
  ( skv_91 )

Skolem constants of (forall ((Z $$unsorted)) (not (pt Z skv_1 skv_1)) ) : 
  ( skv_92 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_1 skv_1 skv_1)) ) : 
  ( skv_93 )

Skolem constants of (forall ((X1 $$unsorted) (Y1 $$unsorted)) (or (not (txtdep skv_1 X1)) (not (txtdep skv_1 Y1)) (not (pt X1 Y1 skv_1))) ) : 
  ( skv_94, skv_95 )

Skolem constants of (forall ((T $$unsorted)) (not (txt skv_1 T)) ) : 
  ( skv_96 )

Skolem constants of (forall ((T $$unsorted)) (not (phtxt skv_1 T)) ) : 
  ( skv_97 )

Skolem constants of (forall ((T $$unsorted)) (not (present skv_1 T)) ) : 
  ( skv_98 )

Skolem constants of (forall ((Z $$unsorted) (T1 $$unsorted)) (not (phtxtequiv Z skv_1 skv_1 T1)) ) : 
  ( skv_99, skv_100 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_1)) (overlap V skv_1 skv_1) (overlap V skv_3 skv_1)) ) : 
  ( skv_115 )

Skolem constants of (forall ((V $$unsorted)) (or (not (phpt V skv_1 skv_1)) (phoverlap V skv_1 skv_1) (phoverlap V skv_3 skv_1)) ) : 
  ( skv_116 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phtxt Y skv_3)) (not (txtdep skv_1 Y))) ) : 
  ( skv_128 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_1 skv_1 skv_3)) ) : 
  ( skv_129 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_3)) (overlap V skv_1 skv_3)) ) : 
  ( skv_130 )

Skolem constants of (forall ((T1 $$unsorted)) (or (not (time T1)) (present skv_3 T1)) ) : 
  ( skv_131 )

Skolem constants of (forall ((Z $$unsorted)) (or (phtxt Z skv_3) (not (pt Z skv_3 skv_3))) ) : 
  ( skv_132 )

Skolem constants of (forall ((R $$unsorted)) (not (occ skv_3 R skv_3)) ) : 
  ( skv_133 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phpt Y skv_3 skv_3)) (not (forall ((Z $$unsorted)) (or (not (phpt Z skv_3 skv_3)) (not (phtxtprec Z Y skv_3))) ))) ) : 
  ( skv_134 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phpt Y skv_3 skv_3)) (not (forall ((Z $$unsorted)) (or (not (phpt Z skv_3 skv_3)) (not (phtxtprec Y Z skv_3))) ))) ) : 
  ( skv_135 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (txt Y skv_3)) (not (txtdep Y skv_3))) ) : 
  ( skv_136 )

Skolem constants of (forall ((Y $$unsorted)) (not (phppt skv_3 Y skv_3)) ) : 
  ( skv_137 )

Skolem constants of (forall ((Y $$unsorted)) (phpt Y skv_3 skv_3) ) : 
  ( skv_138 )

Skolem constants of (forall ((X1 $$unsorted) (Y1 $$unsorted)) (or (not (txtdep skv_1 X1)) (not (txtdep skv_2 Y1)) (not (pt X1 Y1 skv_3))) ) : 
  ( skv_139, skv_140 )

Skolem constants of (forall ((X1 $$unsorted) (Y1 $$unsorted)) (or (not (txtdep skv_3 X1)) (not (txtdep skv_3 Y1)) (not (pt X1 Y1 skv_3))) ) : 
  ( skv_141, skv_142 )

Skolem constants of (forall ((T $$unsorted)) (not (present skv_3 T)) ) : 
  ( skv_143 )

Skolem constants of (forall ((T $$unsorted)) (not (phtxt skv_94 T)) ) : 
  ( skv_155 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_1 skv_1 skv_94)) ) : 
  ( skv_156 )

Skolem constants of (forall ((Z $$unsorted) (T1 $$unsorted)) (not (phtxtequiv Z skv_94 skv_94 T1)) ) : 
  ( skv_157, skv_158 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_94 skv_1)) (overlap V skv_94 skv_1)) ) : 
  ( skv_159 )

Skolem constants of (forall ((T $$unsorted)) (not (txt skv_3 T)) ) : 
  ( skv_160 )

Skolem constants of (forall ((T $$unsorted)) (not (phtxt skv_3 T)) ) : 
  ( skv_161 )

Skolem constants of (forall ((Z $$unsorted)) (not (pt Z skv_3 skv_3)) ) : 
  ( skv_162 )

Skolem constants of (forall ((T $$unsorted)) (not (phtxt skv_2 T)) ) : 
  ( skv_169 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_1 skv_1 skv_2)) ) : 
  ( skv_170 )

Skolem constants of (forall ((T1 $$unsorted)) (or (not (time T1)) (present skv_1 T1)) ) : 
  ( skv_171 )

Skolem constants of (forall ((Z $$unsorted)) (or (phtxt Z skv_1) (not (pt Z skv_1 skv_1))) ) : 
  ( skv_172 )

Skolem constants of (forall ((R $$unsorted)) (not (occ skv_1 R skv_1)) ) : 
  ( skv_173 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phpt Y skv_1 skv_1)) (not (forall ((Z $$unsorted)) (or (not (phpt Z skv_1 skv_1)) (not (phtxtprec Z Y skv_1))) ))) ) : 
  ( skv_174 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phpt Y skv_1 skv_1)) (not (forall ((Z $$unsorted)) (or (not (phpt Z skv_1 skv_1)) (not (phtxtprec Y Z skv_1))) ))) ) : 
  ( skv_175 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (txt Y skv_1)) (not (txtdep Y skv_1))) ) : 
  ( skv_176 )

Skolem constants of (forall ((Y $$unsorted)) (not (phppt skv_1 Y skv_1)) ) : 
  ( skv_177 )

Skolem constants of (forall ((Y $$unsorted)) (phpt Y skv_1 skv_1) ) : 
  ( skv_178 )

Skolem constants of (forall ((T $$unsorted)) (not (txt skv_2 T)) ) : 
  ( skv_179 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_3 skv_3 skv_3)) ) : 
  ( skv_180 )

Skolem constants of (forall ((T1 $$unsorted)) (or (not (time T1)) (present skv_128 T1)) ) : 
  ( skv_195 )

Skolem constants of (forall ((Z $$unsorted)) (or (phtxt Z skv_3) (not (pt Z skv_128 skv_3))) ) : 
  ( skv_196 )

Skolem constants of (forall ((R $$unsorted)) (not (occ skv_128 R skv_3)) ) : 
  ( skv_197 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phpt Y skv_128 skv_3)) (not (forall ((Z $$unsorted)) (or (not (phpt Z skv_128 skv_3)) (not (phtxtprec Z Y skv_3))) ))) ) : 
  ( skv_198 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phpt Y skv_128 skv_3)) (not (forall ((Z $$unsorted)) (or (not (phpt Z skv_128 skv_3)) (not (phtxtprec Y Z skv_3))) ))) ) : 
  ( skv_199 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (txt Y skv_3)) (not (txtdep Y skv_128))) ) : 
  ( skv_200 )

Skolem constants of (forall ((T $$unsorted)) (not (phtxt skv_128 T)) ) : 
  ( skv_201 )

Skolem constants of (forall ((Z $$unsorted) (T1 $$unsorted)) (not (phtxtequiv Z skv_3 skv_128 T1)) ) : 
  ( skv_202, skv_203 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_3)) (overlap V skv_1 skv_3) (overlap V skv_3 skv_3)) ) : 
  ( skv_204 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_3)) (overlap V skv_3 skv_3)) ) : 
  ( skv_205 )

Skolem constants of (forall ((Y $$unsorted)) (not (phppt skv_128 Y skv_3)) ) : 
  ( skv_206 )

Skolem constants of (forall ((Y $$unsorted)) (phpt Y skv_128 skv_3) ) : 
  ( skv_207 )

Skolem constants of (forall ((Z $$unsorted)) (or (not (pt Z skv_130 skv_3)) (not (pt Z skv_1 skv_3))) ) : 
  ( skv_208 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_129 skv_3)) (overlap V skv_1 skv_3)) ) : 
  ( skv_209 )

Skolem constants of (forall ((T $$unsorted)) (not (phtxt skv_95 T)) ) : 
  ( skv_221 )

Skolem constants of (forall ((Z $$unsorted) (T1 $$unsorted)) (not (phtxtequiv Z skv_94 skv_95 T1)) ) : 
  ( skv_222, skv_223 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phtxt Y skv_94)) (not (txtdep skv_1 Y))) ) : 
  ( skv_224 )

Skolem constants of (forall ((T1 $$unsorted)) (or (not (time T1)) (present skv_94 T1)) ) : 
  ( skv_225 )

Skolem constants of (forall ((Z $$unsorted)) (or (phtxt Z skv_94) (not (pt Z skv_94 skv_94))) ) : 
  ( skv_226 )

Skolem constants of (forall ((R $$unsorted)) (not (occ skv_94 R skv_94)) ) : 
  ( skv_227 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phpt Y skv_94 skv_94)) (not (forall ((Z $$unsorted)) (or (not (phpt Z skv_94 skv_94)) (not (phtxtprec Z Y skv_94))) ))) ) : 
  ( skv_228 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phpt Y skv_94 skv_94)) (not (forall ((Z $$unsorted)) (or (not (phpt Z skv_94 skv_94)) (not (phtxtprec Y Z skv_94))) ))) ) : 
  ( skv_229 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (txt Y skv_94)) (not (txtdep Y skv_94))) ) : 
  ( skv_230 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_94 skv_94 skv_94)) ) : 
  ( skv_231 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_94 skv_1 skv_94)) ) : 
  ( skv_232 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_1 skv_94 skv_94)) ) : 
  ( skv_233 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_95 skv_1)) (overlap V skv_94 skv_1)) ) : 
  ( skv_234 )

Skolem constants of (forall ((Y $$unsorted)) (not (phppt skv_94 Y skv_94)) ) : 
  ( skv_235 )

Skolem constants of (forall ((Y $$unsorted)) (phpt Y skv_94 skv_94) ) : 
  ( skv_236 )

Skolem constants of (forall ((T $$unsorted)) (not (phtxt skv_139 T)) ) : 
  ( skv_252 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phtxt Y skv_96)) (not (txtdep skv_1 Y))) ) : 
  ( skv_253 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_1 skv_1 skv_96)) ) : 
  ( skv_254 )

Skolem constants of (forall ((T $$unsorted)) (not (phtxt skv_96 T)) ) : 
  ( skv_255 )

Skolem constants of (forall ((Z $$unsorted) (T1 $$unsorted)) (not (phtxtequiv Z skv_96 skv_2 T1)) ) : 
  ( skv_256, skv_257 )

Skolem constants of (forall ((T1 $$unsorted)) (or (not (time T1)) (present skv_2 T1)) ) : 
  ( skv_258 )

Skolem constants of (forall ((Z $$unsorted)) (or (phtxt Z skv_96) (not (pt Z skv_2 skv_96))) ) : 
  ( skv_259 )

Skolem constants of (forall ((R $$unsorted)) (not (occ skv_2 R skv_96)) ) : 
  ( skv_260 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phpt Y skv_2 skv_96)) (not (forall ((Z $$unsorted)) (or (not (phpt Z skv_2 skv_96)) (not (phtxtprec Z Y skv_96))) ))) ) : 
  ( skv_261 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phpt Y skv_2 skv_96)) (not (forall ((Z $$unsorted)) (or (not (phpt Z skv_2 skv_96)) (not (phtxtprec Y Z skv_96))) ))) ) : 
  ( skv_262 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (txt Y skv_96)) (not (txtdep Y skv_2))) ) : 
  ( skv_263 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_96 skv_1)) (overlap V skv_2 skv_1)) ) : 
  ( skv_264 )

Skolem constants of (forall ((Y $$unsorted)) (not (phppt skv_2 Y skv_96)) ) : 
  ( skv_265 )

Skolem constants of (forall ((Y $$unsorted)) (phpt Y skv_2 skv_96) ) : 
  ( skv_266 )

Skolem constants of (forall ((Z $$unsorted) (T1 $$unsorted)) (not (phtxtequiv Z skv_2 skv_139 T1)) ) : 
  ( skv_267, skv_268 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_1)) (overlap V skv_139 skv_1)) ) : 
  ( skv_269 )

Skolem constants of (forall ((Z $$unsorted)) (or (not (phpt Z skv_128 skv_3)) (phoverlap Z skv_128 skv_3)) ) : 
  ( skv_270 )

Skolem constants of (forall ((T $$unsorted)) (not (present skv_128 T)) ) : 
  ( skv_290 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_128 skv_128 skv_3)) ) : 
  ( skv_291 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phtxt Y skv_3)) (not (txtdep skv_2 Y))) ) : 
  ( skv_292 )

Skolem constants of (forall ((Z $$unsorted)) (or (not (ppt Z skv_2 skv_3)) (overlap skv_1 Z skv_3)) ) : 
  ( skv_293 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_128 skv_1 skv_3)) ) : 
  ( skv_294 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_1 skv_128 skv_3)) ) : 
  ( skv_295 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_128 skv_2 skv_3)) ) : 
  ( skv_296 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_1 skv_2 skv_3)) ) : 
  ( skv_297 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_2 skv_128 skv_3)) ) : 
  ( skv_298 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_2 skv_1 skv_3)) ) : 
  ( skv_299 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_2 skv_2 skv_3)) ) : 
  ( skv_300 )

Skolem constants of (forall ((T $$unsorted)) (not (present skv_2 T)) ) : 
  ( skv_301 )

Skolem constants of (forall ((Z $$unsorted)) (or (not (ppt Z skv_128 skv_3)) (overlap skv_1 Z skv_3)) ) : 
  ( skv_302 )

Skolem constants of (forall ((T $$unsorted)) (not (present skv_130 T)) ) : 
  ( skv_303 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_128 skv_130 skv_3)) ) : 
  ( skv_304 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_130 skv_128 skv_3)) ) : 
  ( skv_305 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_130 skv_130 skv_3)) ) : 
  ( skv_306 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_130 skv_1 skv_3)) ) : 
  ( skv_307 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_130 skv_2 skv_3)) ) : 
  ( skv_308 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_1 skv_130 skv_3)) ) : 
  ( skv_309 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_2 skv_130 skv_3)) ) : 
  ( skv_310 )

Skolem constants of (forall ((R2 $$unsorted)) (or (not (ppt R2 skv_130 skv_3)) (not (occ skv_1 R2 skv_3))) ) : 
  ( skv_311 )

Skolem constants of (forall ((Z $$unsorted)) (or (not (ppt Z skv_1 skv_3)) (overlap skv_130 Z skv_3)) ) : 
  ( skv_312 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_128 skv_3)) (overlap V skv_128 skv_3)) ) : 
  ( skv_313 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_128 skv_3)) (overlap V skv_128 skv_3) (overlap V skv_1 skv_3)) ) : 
  ( skv_314 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_3)) (overlap V skv_130 skv_3)) ) : 
  ( skv_315 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_3)) (overlap V skv_130 skv_3) (overlap V skv_1 skv_3)) ) : 
  ( skv_316 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_2 skv_3)) ) : 
  ( skv_317 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_2 skv_3) (overlap V skv_1 skv_3)) ) : 
  ( skv_318 )

Skolem constants of (forall ((Z $$unsorted)) (or (not (pt Z skv_204 skv_3)) (not (pt Z skv_1 skv_3))) ) : 
  ( skv_319 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_128 skv_3)) (overlap V skv_1 skv_3)) ) : 
  ( skv_320 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_1 skv_3)) ) : 
  ( skv_321 )

Skolem constants of (forall ((T $$unsorted)) (not (present skv_197 T)) ) : 
  ( skv_344 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_128 skv_197 skv_3)) ) : 
  ( skv_345 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_197 skv_128 skv_3)) ) : 
  ( skv_346 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_197 skv_197 skv_3)) ) : 
  ( skv_347 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_197 skv_1 skv_3)) ) : 
  ( skv_348 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_1 skv_197 skv_3)) ) : 
  ( skv_349 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_197 skv_2 skv_3)) ) : 
  ( skv_350 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_2 skv_197 skv_3)) ) : 
  ( skv_351 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_128 skv_3)) (overlap V skv_128 skv_3) (overlap V skv_2 skv_3)) ) : 
  ( skv_352 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_128 skv_3)) ) : 
  ( skv_353 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_128 skv_3)) (overlap V skv_2 skv_3)) ) : 
  ( skv_354 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_195 skv_3)) (overlap V skv_2 skv_3)) ) : 
  ( skv_355 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_195 skv_3)) (overlap V skv_2 skv_3) (overlap V skv_128 skv_3)) ) : 
  ( skv_356 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_195 skv_3)) (overlap V skv_128 skv_3)) ) : 
  ( skv_357 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_197 skv_3)) ) : 
  ( skv_358 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_197 skv_3) (overlap V skv_2 skv_3)) ) : 
  ( skv_359 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_3)) (overlap V skv_195 skv_3)) ) : 
  ( skv_360 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_3)) (overlap V skv_195 skv_3) (overlap V skv_1 skv_3)) ) : 
  ( skv_361 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_195 skv_3)) (overlap V skv_1 skv_3)) ) : 
  ( skv_362 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_128 skv_3)) (overlap V skv_128 skv_3) (overlap V skv_3 skv_3)) ) : 
  ( skv_363 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_128 skv_3)) (overlap V skv_2 skv_3) (overlap V skv_3 skv_3)) ) : 
  ( skv_364 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_195 skv_3)) (overlap V skv_2 skv_3) (overlap V skv_1 skv_3)) ) : 
  ( skv_365 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_195 skv_3)) (overlap V skv_1 skv_3) (overlap V skv_128 skv_3)) ) : 
  ( skv_366 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_128 skv_3)) (overlap V skv_3 skv_3)) ) : 
  ( skv_367 )

Skolem constants of (forall ((Z $$unsorted)) (or (not (pt Z skv_1 skv_3)) (not (pt Z skv_128 skv_3))) ) : 
  ( skv_368 )

Skolem constants of (forall ((Z $$unsorted)) (or (not (pt Z skv_359 skv_3)) (not (pt Z skv_2 skv_3))) ) : 
  ( skv_369 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_197 skv_140 skv_3)) ) : 
  ( skv_386 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_1 skv_140 skv_3)) ) : 
  ( skv_387 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_2 skv_140 skv_3)) ) : 
  ( skv_388 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_140 skv_197 skv_3)) ) : 
  ( skv_389 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_140 skv_1 skv_3)) ) : 
  ( skv_390 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_140 skv_2 skv_3)) ) : 
  ( skv_391 )

Skolem constants of (forall ((Z $$unsorted)) (not (sumpt Z skv_140 skv_140 skv_3)) ) : 
  ( skv_392 )

Skolem constants of (forall ((T $$unsorted)) (not (present skv_140 T)) ) : 
  ( skv_393 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_197 skv_3)) (overlap V skv_2 skv_3)) ) : 
  ( skv_394 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_140 skv_3)) (overlap V skv_2 skv_3) (overlap V skv_1 skv_3)) ) : 
  ( skv_395 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_197 skv_3) (overlap V skv_1 skv_3)) ) : 
  ( skv_396 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_197 skv_3)) (overlap V skv_197 skv_3)) ) : 
  ( skv_397 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_1 skv_3) (overlap V skv_195 skv_3)) ) : 
  ( skv_398 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_195 skv_3)) ) : 
  ( skv_399 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_195 skv_3) (overlap V skv_2 skv_3)) ) : 
  ( skv_400 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_195 skv_3) (overlap V skv_197 skv_3)) ) : 
  ( skv_401 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_195 skv_3)) (overlap V skv_3 skv_3)) ) : 
  ( skv_402 )

Skolem constants of (forall ((V $$unsorted)) (or (not (pt V skv_197 skv_3)) (overlap V skv_2 skv_3) (overlap V skv_197 skv_3)) ) : 
  ( skv_403 )

Skolem constants of (forall ((T $$unsorted)) (not (phtxt skv_140 T)) ) : 
  ( skv_404 )

Skolem constants of (forall ((Z $$unsorted) (T1 $$unsorted)) (not (phtxtequiv Z skv_3 skv_140 T1)) ) : 
  ( skv_405, skv_406 )

Skolem constants of (forall ((T1 $$unsorted)) (or (not (time T1)) (present skv_140 T1)) ) : 
  ( skv_407 )

Skolem constants of (forall ((Z $$unsorted)) (or (phtxt Z skv_3) (not (pt Z skv_140 skv_3))) ) : 
  ( skv_408 )

Skolem constants of (forall ((R $$unsorted)) (not (occ skv_140 R skv_3)) ) : 
  ( skv_409 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phpt Y skv_140 skv_3)) (not (forall ((Z $$unsorted)) (or (not (phpt Z skv_140 skv_3)) (not (phtxtprec Z Y skv_3))) ))) ) : 
  ( skv_410 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (phpt Y skv_140 skv_3)) (not (forall ((Z $$unsorted)) (or (not (phpt Z skv_140 skv_3)) (not (phtxtprec Y Z skv_3))) ))) ) : 
  ( skv_411 )

Skolem constants of (forall ((Y $$unsorted)) (or (not (txt Y skv_3)) (not (txtdep Y skv_140))) ) : 
  ( skv_412 )

Skolem constants of (forall ((Z $$unsorted)) (or (not (ppt Z skv_2 skv_3)) (overlap skv_197 Z skv_3)) ) : 
  ( skv_413 )

Skolem constants of (forall ((Z $$unsorted)) (or (not (ppt Z skv_140 skv_3)) (overlap skv_1 Z skv_3)) ) : 
  ( skv_414 )

Skolem constants of (forall ((Y $$unsorted)) (not (phppt skv_140 Y skv_3)) ) : 
  ( skv_415 )

Skolem constants of (forall ((Y $$unsorted)) (phpt Y skv_140 skv_3) ) : 
  ( skv_416 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (= (pt X Y T) (or (ppt X Y T) (and (= X Y) (present X T) (present Y T)))) ) : 
  ( skv_1, skv_1, skv_2 )
  ( skv_1, skv_1, skv_94 )
  ( skv_1, skv_1, skv_96 )
  ( skv_1, skv_2, skv_3 )
  ( skv_1, skv_128, skv_3 )
  ( skv_1, skv_195, skv_3 )
  ( skv_1, skv_254, skv_96 )
  ( skv_1, skv_294, skv_3 )
  ( skv_1, skv_295, skv_3 )
  ( skv_1, skv_309, skv_3 )
  ( skv_1, skv_348, skv_3 )
  ( skv_1, skv_349, skv_3 )
  ( skv_2, skv_1, skv_1 )
  ( skv_2, skv_2, skv_96 )
  ( skv_2, skv_96, skv_1 )
  ( skv_2, skv_128, skv_3 )
  ( skv_2, skv_195, skv_3 )
  ( skv_2, skv_197, skv_3 )
  ( skv_2, skv_254, skv_96 )
  ( skv_3, skv_1, skv_3 )
  ( skv_3, skv_3, skv_3 )
  ( skv_3, skv_128, skv_3 )
  ( skv_3, skv_195, skv_3 )
  ( skv_94, skv_94, skv_1 )
  ( skv_94, skv_94, skv_94 )
  ( skv_94, skv_95, skv_1 )
  ( skv_128, skv_2, skv_3 )
  ( skv_128, skv_128, skv_3 )
  ( skv_128, skv_130, skv_3 )
  ( skv_128, skv_195, skv_3 )
  ( skv_128, skv_292, skv_3 )
  ( skv_128, skv_294, skv_3 )
  ( skv_128, skv_295, skv_3 )
  ( skv_130, skv_1, skv_3 )
  ( skv_130, skv_130, skv_3 )
  ( skv_130, skv_304, skv_3 )
  ( skv_130, skv_305, skv_3 )
  ( skv_130, skv_306, skv_3 )
  ( skv_130, skv_307, skv_3 )
  ( skv_139, skv_2, skv_1 )
  ( skv_139, skv_140, skv_3 )
  ( skv_140, skv_140, skv_3 )
  ( skv_195, skv_1, skv_3 )
  ( skv_195, skv_2, skv_3 )
  ( skv_197, skv_2, skv_3 )
  ( skv_197, skv_197, skv_3 )
  ( skv_204, skv_1, skv_3 )
  ( skv_204, skv_129, skv_3 )
  ( skv_205, skv_1, skv_3 )
  ( skv_261, skv_2, skv_96 )
  ( skv_262, skv_2, skv_96 )
  ( skv_359, skv_2, skv_3 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted)) (not (ppt X X T)) ) : 
  ( skv_1, skv_1 )
  ( skv_1, skv_2 )
  ( skv_1, skv_3 )
  ( skv_1, skv_94 )
  ( skv_1, skv_96 )
  ( skv_2, skv_96 )
  ( skv_3, skv_3 )
  ( skv_94, skv_94 )
  ( skv_128, skv_3 )
  ( skv_130, skv_3 )
  ( skv_197, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (= (phppt X Y T) (and (ppt X Y T) (phtxt X T) (phtxt Y T))) ) : 
  ( skv_1, skv_1, skv_3 )
  ( skv_1, skv_3, skv_1 )
  ( skv_2, skv_265, skv_96 )
  ( skv_3, skv_1, skv_1 )
  ( skv_128, skv_206, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (= (phpt X Y T) (and (pt X Y T) (phtxt X T) (phtxt Y T))) ) : 
  ( skv_1, skv_3, skv_1 )
  ( skv_2, skv_2, skv_96 )
  ( skv_2, skv_140, skv_3 )
  ( skv_3, skv_1, skv_1 )
  ( skv_3, skv_2, skv_96 )
  ( skv_116, skv_1, skv_1 )
  ( skv_128, skv_128, skv_3 )
  ( skv_198, skv_128, skv_3 )
  ( skv_199, skv_128, skv_3 )
  ( skv_261, skv_2, skv_96 )
  ( skv_262, skv_2, skv_96 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted)) (not (phtxtprec X X T)) ) : 
  ( skv_1, skv_1 )
  ( skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted)) (or (not (nontime X)) (not (forall ((T $$unsorted)) (not (present X T)) ))) ) : 
  ( skv_1 )
  ( skv_2 )
  ( skv_3 )
  ( skv_128 )
  ( skv_130 )
  ( skv_140 )
  ( skv_197 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted) (BOUND_VARIABLE_1386 $$unsorted)) (or (not (phtxt X T)) (not (present X BOUND_VARIABLE_1386)) (phtxt X BOUND_VARIABLE_1386)) ) : 
  ( skv_1, skv_1, skv_3 )
  ( skv_1, skv_97, skv_1 )
  ( skv_2, skv_169, skv_3 )
  ( skv_139, skv_252, skv_3 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted) (BOUND_VARIABLE_1404 $$unsorted)) (or (not (txt X T)) (not (present X BOUND_VARIABLE_1404)) (txt X BOUND_VARIABLE_1404)) ) : 
  ( skv_1, skv_96, skv_1 )
  ( skv_1, skv_96, skv_3 )
  ( skv_2, skv_179, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (= (overlap X Y T) (not (forall ((Z $$unsorted)) (or (not (pt Z X T)) (not (pt Z Y T))) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_1, skv_128, skv_3 )
  ( skv_1, skv_293, skv_3 )
  ( skv_3, skv_3, skv_3 )
  ( skv_130, skv_1, skv_3 )
  ( skv_204, skv_1, skv_3 )
  ( skv_313, skv_128, skv_3 )
  ( skv_317, skv_2, skv_3 )
  ( skv_318, skv_2, skv_3 )
  ( skv_321, skv_1, skv_3 )
  ( skv_358, skv_197, skv_3 )
  ( skv_359, skv_2, skv_3 )
  ( skv_359, skv_197, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (Z $$unsorted) (T $$unsorted)) (= (sumpt X Y Z T) (and (pt Y X T) (pt Z X T) (forall ((V $$unsorted)) (or (not (pt V X T)) (overlap V Y T) (overlap V Z T)) ))) ) : 
  ( skv_1, skv_1, skv_1, skv_1 )
  ( skv_1, skv_1, skv_1, skv_2 )
  ( skv_1, skv_1, skv_1, skv_3 )
  ( skv_1, skv_1, skv_1, skv_94 )
  ( skv_1, skv_1, skv_3, skv_1 )
  ( skv_1, skv_1, skv_3, skv_3 )
  ( skv_1, skv_1, skv_130, skv_3 )
  ( skv_1, skv_1, skv_195, skv_3 )
  ( skv_1, skv_2, skv_2, skv_1 )
  ( skv_1, skv_3, skv_1, skv_1 )
  ( skv_1, skv_3, skv_1, skv_3 )
  ( skv_1, skv_3, skv_3, skv_3 )
  ( skv_1, skv_130, skv_1, skv_3 )
  ( skv_1, skv_130, skv_130, skv_3 )
  ( skv_1, skv_195, skv_1, skv_3 )
  ( skv_1, skv_195, skv_195, skv_3 )
  ( skv_2, skv_1, skv_1, skv_3 )
  ( skv_2, skv_1, skv_2, skv_3 )
  ( skv_2, skv_1, skv_195, skv_3 )
  ( skv_2, skv_1, skv_197, skv_3 )
  ( skv_2, skv_2, skv_1, skv_3 )
  ( skv_2, skv_2, skv_2, skv_3 )
  ( skv_2, skv_2, skv_195, skv_3 )
  ( skv_2, skv_2, skv_197, skv_3 )
  ( skv_2, skv_128, skv_128, skv_3 )
  ( skv_2, skv_139, skv_139, skv_1 )
  ( skv_2, skv_195, skv_1, skv_3 )
  ( skv_2, skv_195, skv_2, skv_3 )
  ( skv_2, skv_195, skv_195, skv_3 )
  ( skv_2, skv_195, skv_197, skv_3 )
  ( skv_2, skv_197, skv_1, skv_3 )
  ( skv_2, skv_197, skv_2, skv_3 )
  ( skv_2, skv_197, skv_195, skv_3 )
  ( skv_2, skv_197, skv_197, skv_3 )
  ( skv_3, skv_3, skv_3, skv_3 )
  ( skv_3, skv_197, skv_197, skv_3 )
  ( skv_94, skv_94, skv_94, skv_1 )
  ( skv_95, skv_94, skv_94, skv_1 )
  ( skv_96, skv_2, skv_2, skv_1 )
  ( skv_128, skv_1, skv_1, skv_3 )
  ( skv_128, skv_1, skv_128, skv_3 )
  ( skv_128, skv_2, skv_2, skv_3 )
  ( skv_128, skv_2, skv_3, skv_3 )
  ( skv_128, skv_2, skv_128, skv_3 )
  ( skv_128, skv_3, skv_2, skv_3 )
  ( skv_128, skv_3, skv_3, skv_3 )
  ( skv_128, skv_3, skv_128, skv_3 )
  ( skv_128, skv_128, skv_1, skv_3 )
  ( skv_128, skv_128, skv_2, skv_3 )
  ( skv_128, skv_128, skv_3, skv_3 )
  ( skv_128, skv_128, skv_128, skv_3 )
  ( skv_129, skv_1, skv_1, skv_3 )
  ( skv_140, skv_1, skv_1, skv_3 )
  ( skv_140, skv_1, skv_2, skv_3 )
  ( skv_140, skv_2, skv_1, skv_3 )
  ( skv_140, skv_2, skv_2, skv_3 )
  ( skv_195, skv_1, skv_1, skv_3 )
  ( skv_195, skv_1, skv_2, skv_3 )
  ( skv_195, skv_1, skv_128, skv_3 )
  ( skv_195, skv_2, skv_1, skv_3 )
  ( skv_195, skv_2, skv_2, skv_3 )
  ( skv_195, skv_2, skv_128, skv_3 )
  ( skv_195, skv_3, skv_3, skv_3 )
  ( skv_195, skv_128, skv_1, skv_3 )
  ( skv_195, skv_128, skv_2, skv_3 )
  ( skv_195, skv_128, skv_128, skv_3 )
  ( skv_197, skv_2, skv_2, skv_3 )
  ( skv_197, skv_2, skv_197, skv_3 )
  ( skv_197, skv_197, skv_2, skv_3 )
  ( skv_197, skv_197, skv_197, skv_3 )
  ( skv_254, skv_1, skv_1, skv_96 )
  ( skv_291, skv_128, skv_128, skv_3 )
  ( skv_294, skv_128, skv_1, skv_3 )
  ( skv_295, skv_1, skv_128, skv_3 )
  ( skv_296, skv_128, skv_2, skv_3 )
  ( skv_297, skv_1, skv_2, skv_3 )
  ( skv_298, skv_2, skv_128, skv_3 )
  ( skv_299, skv_2, skv_1, skv_3 )
  ( skv_300, skv_2, skv_2, skv_3 )
  ( skv_304, skv_128, skv_130, skv_3 )
  ( skv_305, skv_130, skv_128, skv_3 )
  ( skv_306, skv_130, skv_130, skv_3 )
  ( skv_307, skv_130, skv_1, skv_3 )
  ( skv_308, skv_130, skv_2, skv_3 )
  ( skv_309, skv_1, skv_130, skv_3 )
  ( skv_310, skv_2, skv_130, skv_3 )
  ( skv_345, skv_128, skv_197, skv_3 )
  ( skv_346, skv_197, skv_128, skv_3 )
  ( skv_348, skv_197, skv_1, skv_3 )
  ( skv_349, skv_1, skv_197, skv_3 )
  ( skv_350, skv_197, skv_2, skv_3 )
  ( skv_351, skv_2, skv_197, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (or (not (ppt X Y T)) (and (present X T) (present Y T))) ) : 
  ( skv_1, skv_2, skv_3 )
  ( skv_1, skv_3, skv_1 )
  ( skv_1, skv_3, skv_3 )
  ( skv_1, skv_128, skv_3 )
  ( skv_1, skv_140, skv_3 )
  ( skv_2, skv_96, skv_1 )
  ( skv_3, skv_1, skv_1 )
  ( skv_3, skv_1, skv_3 )
  ( skv_3, skv_195, skv_3 )
  ( skv_94, skv_95, skv_1 )
  ( skv_128, skv_206, skv_3 )
  ( skv_130, skv_1, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted) (Z $$unsorted)) (or (not (ppt X Y T)) (not (ppt Y Z T)) (ppt X Z T)) ) : 
  ( skv_1, skv_2, skv_3, skv_128 )
  ( skv_1, skv_2, skv_3, skv_140 )
  ( skv_1, skv_2, skv_3, skv_197 )
  ( skv_1, skv_2, skv_3, skv_265 )
  ( skv_1, skv_3, skv_1, skv_1 )
  ( skv_1, skv_3, skv_3, skv_1 )
  ( skv_1, skv_128, skv_3, skv_1 )
  ( skv_1, skv_128, skv_3, skv_206 )
  ( skv_1, skv_140, skv_3, skv_2 )
  ( skv_1, skv_195, skv_3, skv_1 )
  ( skv_2, skv_195, skv_3, skv_1 )
  ( skv_2, skv_197, skv_3, skv_2 )
  ( skv_128, skv_1, skv_3, skv_2 )
  ( skv_130, skv_1, skv_3, skv_2 )
  ( skv_130, skv_1, skv_3, skv_128 )
  ( skv_197, skv_2, skv_3, skv_140 )
  ( skv_204, skv_1, skv_3, skv_128 )
  ( skv_205, skv_1, skv_3, skv_140 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (or (not (ppt X Y T)) (not (forall ((Z $$unsorted)) (or (not (ppt Z Y T)) (overlap X Z T)) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_1, skv_2, skv_3 )
  ( skv_1, skv_128, skv_3 )
  ( skv_1, skv_140, skv_3 )
  ( skv_2, skv_140, skv_3 )
  ( skv_3, skv_3, skv_3 )
  ( skv_130, skv_1, skv_3 )
  ( skv_197, skv_2, skv_3 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted) (Y $$unsorted)) (or (not (present X T)) (not (present Y T)) (not (forall ((Z $$unsorted)) (not (sumpt Z X Y T)) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_1, skv_2, skv_1 )
  ( skv_1, skv_3, skv_1 )
  ( skv_1, skv_3, skv_2 )
  ( skv_1, skv_3, skv_128 )
  ( skv_1, skv_3, skv_130 )
  ( skv_1, skv_3, skv_140 )
  ( skv_1, skv_3, skv_197 )
  ( skv_1, skv_94, skv_1 )
  ( skv_1, skv_94, skv_94 )
  ( skv_1, skv_96, skv_1 )
  ( skv_2, skv_3, skv_1 )
  ( skv_2, skv_3, skv_2 )
  ( skv_2, skv_3, skv_128 )
  ( skv_2, skv_3, skv_130 )
  ( skv_2, skv_3, skv_140 )
  ( skv_2, skv_3, skv_197 )
  ( skv_3, skv_3, skv_3 )
  ( skv_94, skv_94, skv_1 )
  ( skv_94, skv_94, skv_94 )
  ( skv_128, skv_3, skv_1 )
  ( skv_128, skv_3, skv_2 )
  ( skv_128, skv_3, skv_128 )
  ( skv_128, skv_3, skv_130 )
  ( skv_128, skv_3, skv_197 )
  ( skv_130, skv_3, skv_1 )
  ( skv_130, skv_3, skv_2 )
  ( skv_130, skv_3, skv_128 )
  ( skv_130, skv_3, skv_130 )
  ( skv_140, skv_3, skv_1 )
  ( skv_140, skv_3, skv_2 )
  ( skv_140, skv_3, skv_140 )
  ( skv_140, skv_3, skv_197 )
  ( skv_197, skv_3, skv_1 )
  ( skv_197, skv_3, skv_2 )
  ( skv_197, skv_3, skv_128 )
  ( skv_197, skv_3, skv_140 )
  ( skv_197, skv_3, skv_197 )

Instantiations of (forall ((S $$unsorted) (T $$unsorted)) (or (not (reg S)) (not (time T)) (occ S S T)) ) : 
  ( skv_130, skv_3 )
  ( skv_197, skv_3 )

Instantiations of (forall ((S $$unsorted) (R $$unsorted) (T $$unsorted)) (or (not (occ S R T)) (and (present S T) (present R T))) ) : 
  ( skv_1, skv_3, skv_1 )
  ( skv_1, skv_173, skv_1 )
  ( skv_2, skv_260, skv_96 )
  ( skv_3, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3 )
  ( skv_3, skv_133, skv_3 )
  ( skv_128, skv_197, skv_3 )

Instantiations of (forall ((R1 $$unsorted) (R2 $$unsorted) (T $$unsorted)) (or (not (ppt R1 R2 T)) (not (reg R2)) (not (time T)) (occ R1 R1 T)) ) : 
  ( skv_1, skv_197, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted) (R1 $$unsorted)) (or (not (ppt X Y T)) (not (occ Y R1 T)) (not (forall ((R2 $$unsorted)) (or (not (ppt R2 R1 T)) (not (occ X R2 T))) ))) ) : 
  ( skv_1, skv_1, skv_1, skv_1 )
  ( skv_1, skv_2, skv_3, skv_197 )
  ( skv_1, skv_128, skv_3, skv_130 )
  ( skv_3, skv_3, skv_3, skv_3 )
  ( skv_197, skv_2, skv_3, skv_197 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted)) (or (not (phtxt X T)) (not (forall ((T1 $$unsorted)) (or (not (time T1)) (present X T1)) ))) ) : 
  ( skv_1, skv_1 )
  ( skv_2, skv_3 )
  ( skv_2, skv_96 )
  ( skv_3, skv_3 )
  ( skv_94, skv_94 )
  ( skv_128, skv_3 )
  ( skv_140, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (= (phoverlap X Y T) (not (forall ((Z $$unsorted)) (or (not (phpt Z X T)) (not (phpt Z Y T))) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (Z $$unsorted) (T $$unsorted)) (= (phsumpt X Y Z T) (and (phpt Y X T) (phpt Z X T) (forall ((V $$unsorted)) (or (not (phpt V X T)) (phoverlap V Y T) (phoverlap V Z T)) ))) ) : 
  ( skv_1, skv_1, skv_1, skv_1 )
  ( skv_1, skv_1, skv_3, skv_1 )
  ( skv_1, skv_3, skv_1, skv_1 )
  ( skv_2, skv_2, skv_2, skv_3 )
  ( skv_3, skv_3, skv_3, skv_3 )
  ( skv_128, skv_128, skv_128, skv_3 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted)) (= (compphtxt X T) (and (phtxt X T) (forall ((Y $$unsorted)) (not (phppt X Y T)) ))) ) : 
  ( skv_1, skv_1 )
  ( skv_2, skv_3 )
  ( skv_2, skv_96 )
  ( skv_3, skv_3 )
  ( skv_94, skv_94 )
  ( skv_128, skv_3 )
  ( skv_140, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted) (BOUND_VARIABLE_1552 $$unsorted)) (or (not (phppt X Y T)) (not (phppt Y X BOUND_VARIABLE_1552))) ) : 
  ( skv_1, skv_1, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted) (Y $$unsorted)) (or (not (phtxt X T)) (not (phtxt Y T)) (phpt X Y T) (not (forall ((Z $$unsorted)) (or (not (phpt Z X T)) (phoverlap Z Y T)) ))) ) : 
  ( skv_2, skv_3, skv_140 )
  ( skv_2, skv_96, skv_2 )
  ( skv_94, skv_94, skv_94 )
  ( skv_128, skv_3, skv_128 )
  ( skv_140, skv_3, skv_2 )
  ( skv_140, skv_3, skv_140 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted)) (or (not (phtxt X T)) (not (forall ((Z $$unsorted)) (or (phtxt Z T) (not (pt Z X T))) ))) ) : 
  ( skv_1, skv_1 )
  ( skv_2, skv_3 )
  ( skv_2, skv_96 )
  ( skv_3, skv_3 )
  ( skv_94, skv_94 )
  ( skv_128, skv_3 )
  ( skv_140, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (or (not (phppt X Y T)) (not (forall ((Z $$unsorted)) (or (not (phppt X Z T)) (not (forall ((V $$unsorted)) (or (not (phppt X V T)) (not (phppt V Z T))) ))) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_2, skv_140, skv_3 )
  ( skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (or (not (phppt X Y T)) (not (forall ((Z $$unsorted)) (or (not (phppt Z Y T)) (not (forall ((V $$unsorted)) (or (not (phppt Z V T)) (not (phppt V Y T))) ))) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_2, skv_140, skv_3 )
  ( skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted) (Y $$unsorted)) (or (not (phtxt X T)) (not (forall ((Y $$unsorted)) (phpt Y X T) )) (not (forall ((Z $$unsorted)) (or (not (phpt Z Y T)) (not (forall ((V $$unsorted)) (not (phppt V Z T)) ))) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_2, skv_3, skv_3 )
  ( skv_2, skv_96, skv_1 )
  ( skv_3, skv_3, skv_3 )
  ( skv_94, skv_94, skv_1 )
  ( skv_128, skv_3, skv_3 )
  ( skv_140, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted)) (or (not (phtxt X T)) (not (forall ((R $$unsorted)) (not (occ X R T)) ))) ) : 
  ( skv_1, skv_1 )
  ( skv_2, skv_3 )
  ( skv_2, skv_96 )
  ( skv_3, skv_3 )
  ( skv_94, skv_94 )
  ( skv_128, skv_3 )
  ( skv_140, skv_3 )

Instantiations of (forall ((X $$unsorted) (R $$unsorted) (T $$unsorted) (Y $$unsorted)) (or (not (occ X R T)) (not (occ Y R T)) (not (phtxt X T)) (not (phtxt Y T)) (= X Y)) ) : 
  ( skv_128, skv_197, skv_3, skv_256 )
  ( skv_128, skv_197, skv_3, skv_261 )
  ( skv_128, skv_197, skv_3, skv_262 )
  ( skv_128, skv_197, skv_3, skv_265 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (or (not (phtxtprec X Y T)) (and (phtxt X T) (phtxt Y T))) ) : 
  ( skv_1, skv_3, skv_1 )
  ( skv_3, skv_1, skv_1 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted) (Z $$unsorted)) (or (not (phtxtprec X Y T)) (not (phtxtprec Y Z T)) (phtxtprec X Z T)) ) : 
  ( skv_1, skv_3, skv_1, skv_1 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (or (not (phtxtprec X Y T)) (not (forall ((Z $$unsorted)) (or (not (phtxtprec X Z T)) (not (forall ((V $$unsorted)) (or (not (phtxtprec X V T)) (not (phtxtprec V Z T))) ))) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (or (not (phtxtprec X Y T)) (not (forall ((Z $$unsorted)) (or (not (phtxtprec Z Y T)) (not (forall ((V $$unsorted)) (or (not (phtxtprec Z V T)) (not (phtxtprec V Y T))) ))) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted) (BOUND_VARIABLE_1750 $$unsorted) (BOUND_VARIABLE_1753 $$unsorted)) (or (not (phtxtprec X Y T)) (and (not (phpt X Y BOUND_VARIABLE_1750)) (not (phpt Y X BOUND_VARIABLE_1753)))) ) : 
  ( skv_1, skv_1, skv_1, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted) (BOUND_VARIABLE_1768 $$unsorted)) (or (not (phtxtprec X Y T)) (not (phpt BOUND_VARIABLE_1768 X T)) (phtxtprec BOUND_VARIABLE_1768 Y T)) ) : 
  ( skv_3, skv_1, skv_1, skv_1 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted) (BOUND_VARIABLE_1786 $$unsorted)) (or (not (phtxtprec X Y T)) (not (phpt BOUND_VARIABLE_1786 Y T)) (phtxtprec X BOUND_VARIABLE_1786 T)) ) : 
  ( skv_1, skv_3, skv_1, skv_1 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (or (not (phtxtprec X Y T)) (not (forall ((Z $$unsorted)) (or (not (compphtxt Z T)) (not (phpt X Z T)) (not (phpt Y Z T))) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted)) (or (not (phtxt X T)) (not (forall ((Y $$unsorted)) (or (not (phpt Y X T)) (not (forall ((Z $$unsorted)) (or (not (phpt Z X T)) (not (phtxtprec Z Y T))) ))) ))) ) : 
  ( skv_1, skv_1 )
  ( skv_2, skv_3 )
  ( skv_2, skv_96 )
  ( skv_3, skv_3 )
  ( skv_94, skv_94 )
  ( skv_128, skv_3 )
  ( skv_140, skv_3 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted)) (or (not (phtxt X T)) (not (forall ((Y $$unsorted)) (or (not (phpt Y X T)) (not (forall ((Z $$unsorted)) (or (not (phpt Z X T)) (not (phtxtprec Y Z T))) ))) ))) ) : 
  ( skv_1, skv_1 )
  ( skv_2, skv_3 )
  ( skv_2, skv_96 )
  ( skv_3, skv_3 )
  ( skv_94, skv_94 )
  ( skv_128, skv_3 )
  ( skv_140, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (or (not (phtxtprec X Y T)) (not (forall ((Z $$unsorted)) (or (not (phtxtprec X Z T)) (not (phtxtprec Z Y T))) )) (not (forall ((Z $$unsorted)) (not (phsumpt Z X Y T)) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted) (R1 $$unsorted) (R2 $$unsorted)) (or (not (phtxtprec X Y T)) (not (occ X R1 T)) (not (occ Y R2 T)) (not (overlap R1 R2 T))) ) : 
  ( skv_1, skv_1, skv_1, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (or (not (phrep X Y T)) (phtxt X T)) ) : 
  ( skv_1, skv_3, skv_1 )

Instantiations of (forall ((T $$unsorted) (X $$unsorted) (BOUND_VARIABLE_1941 $$unsorted) (BOUND_VARIABLE_1944 $$unsorted)) (or (not (phrep X BOUND_VARIABLE_1941 T)) (not (present X BOUND_VARIABLE_1944)) (not (forall ((Y $$unsorted)) (not (phrep X Y BOUND_VARIABLE_1944)) ))) ) : 
  ( skv_1, skv_1, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted) (Y $$unsorted) (T1 $$unsorted)) (or (not (phtxtequiv X T Y T1)) (and (phtxt X T) (phtxt Y T1))) ) : 
  ( skv_1, skv_1, skv_3, skv_3 )
  ( skv_1, skv_2, skv_1, skv_2 )
  ( skv_3, skv_3, skv_1, skv_1 )
  ( skv_140, skv_3, skv_140, skv_3 )
  ( skv_157, skv_94, skv_94, skv_158 )
  ( skv_202, skv_3, skv_128, skv_203 )
  ( skv_256, skv_96, skv_2, skv_257 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted) (Y $$unsorted) (T1 $$unsorted)) (or (not (phtxtequiv X T Y T1)) (and (present X T) (present Y T1))) ) : 
  ( skv_1, skv_1, skv_3, skv_3 )
  ( skv_2, skv_96, skv_2, skv_96 )
  ( skv_3, skv_3, skv_1, skv_1 )
  ( skv_128, skv_3, skv_128, skv_3 )
  ( skv_157, skv_94, skv_94, skv_158 )
  ( skv_256, skv_96, skv_2, skv_257 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted)) (or (not (phtxt X T)) (phtxtequiv X T X T)) ) : 
  ( skv_1, skv_1 )
  ( skv_2, skv_96 )
  ( skv_3, skv_3 )
  ( skv_128, skv_3 )
  ( skv_140, skv_3 )

Instantiations of (forall ((X $$unsorted) (T1 $$unsorted) (Y $$unsorted) (T2 $$unsorted) (Z $$unsorted) (T3 $$unsorted)) (or (not (phtxtequiv X T1 Y T2)) (not (phtxtequiv Y T2 Z T3)) (phtxtequiv X T1 Z T3)) ) : 
  ( skv_1, skv_1, skv_3, skv_3, skv_1, skv_1 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (or (not (ppt X Y T)) (not (phtxtequiv X T Y T))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3 )
  ( skv_94, skv_94, skv_94 )
  ( skv_128, skv_128, skv_3 )
  ( skv_204, skv_128, skv_3 )
  ( skv_293, skv_2, skv_3 )

Instantiations of (forall ((X1 $$unsorted) (T $$unsorted) (X2 $$unsorted) (Y1 $$unsorted)) (or (not (phtxtequiv X1 T X2 T)) (not (phppt Y1 X1 T)) (not (forall ((Y2 $$unsorted)) (or (not (phtxtequiv Y1 T Y2 T)) (not (ppt Y2 X2 T))) ))) ) : 
  ( skv_1, skv_1, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3, skv_3 )

Instantiations of (forall ((X1 $$unsorted) (T $$unsorted) (X2 $$unsorted) (Y1 $$unsorted)) (or (not (phtxtequiv X1 T X2 T)) (not (phppt X1 Y1 T)) (not (forall ((Y2 $$unsorted)) (or (not (phtxtequiv Y1 T Y2 T)) (not (ppt X2 Y2 T))) ))) ) : 
  ( skv_1, skv_1, skv_1, skv_1 )
  ( skv_2, skv_3, skv_2, skv_140 )
  ( skv_3, skv_3, skv_3, skv_3 )

Instantiations of (forall ((X1 $$unsorted) (T1 $$unsorted) (X2 $$unsorted) (T2 $$unsorted) (Y $$unsorted)) (or (not (phtxtequiv X1 T1 X2 T2)) (= (phrep X1 Y T1) (phrep X2 Y T2))) ) : 
  ( skv_1, skv_1, skv_3, skv_3, skv_1 )
  ( skv_3, skv_3, skv_1, skv_1, skv_1 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted)) (or (not (txtdep X Y)) (and (not (forall ((T $$unsorted)) (not (txt X T)) )) (not (forall ((T $$unsorted)) (not (phtxt Y T)) )))) ) : 
  ( skv_1, skv_1 )
  ( skv_1, skv_2 )
  ( skv_1, skv_94 )
  ( skv_1, skv_95 )
  ( skv_1, skv_128 )
  ( skv_1, skv_139 )
  ( skv_2, skv_1 )
  ( skv_2, skv_2 )
  ( skv_2, skv_96 )
  ( skv_2, skv_128 )
  ( skv_2, skv_140 )
  ( skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted)) (or (not (phtxt X T)) (not (forall ((Y $$unsorted)) (or (not (txt Y T)) (not (txtdep Y X))) ))) ) : 
  ( skv_1, skv_1 )
  ( skv_2, skv_3 )
  ( skv_2, skv_96 )
  ( skv_3, skv_3 )
  ( skv_94, skv_94 )
  ( skv_128, skv_3 )
  ( skv_140, skv_3 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted) (BOUND_VARIABLE_2059 $$unsorted) (BOUND_VARIABLE_2060 $$unsorted)) (or (not (phtxt X T)) (not (txt BOUND_VARIABLE_2059 T)) (not (txtdep BOUND_VARIABLE_2059 X)) (not (txt BOUND_VARIABLE_2060 T)) (not (txtdep BOUND_VARIABLE_2060 X)) (= BOUND_VARIABLE_2059 BOUND_VARIABLE_2060)) ) : 
  ( skv_128, skv_3, skv_1, skv_2 )
  ( skv_128, skv_3, skv_1, skv_200 )
  ( skv_128, skv_3, skv_1, skv_263 )
  ( skv_128, skv_3, skv_200, skv_1 )
  ( skv_128, skv_96, skv_263, skv_1 )
  ( skv_139, skv_3, skv_1, skv_2 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted)) (or (not (txt X T)) (not (forall ((Y $$unsorted)) (or (not (phtxt Y T)) (not (txtdep X Y))) ))) ) : 
  ( skv_1, skv_1 )
  ( skv_1, skv_3 )
  ( skv_1, skv_94 )
  ( skv_1, skv_96 )
  ( skv_2, skv_3 )
  ( skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y1 $$unsorted) (Y2 $$unsorted) (BOUND_VARIABLE_2107 $$unsorted) (BOUND_VARIABLE_2108 $$unsorted)) (or (not (txtdep X Y1)) (not (txtdep X Y2)) (not (present Y1 BOUND_VARIABLE_2107)) (not (present Y2 BOUND_VARIABLE_2108)) (phtxtequiv Y1 BOUND_VARIABLE_2107 Y2 BOUND_VARIABLE_2108)) ) : 
  ( skv_1, skv_1, skv_1, skv_1, skv_1 )
  ( skv_2, skv_1, skv_1, skv_2, skv_2 )
  ( skv_2, skv_140, skv_140, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (BOUND_VARIABLE_2133 $$unsorted)) (or (not (txtdep X Y)) (not (present X BOUND_VARIABLE_2133)) (not (forall ((Z $$unsorted) (T1 $$unsorted)) (not (phtxtequiv Z BOUND_VARIABLE_2133 Y T1)) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_1, skv_2, skv_2 )
  ( skv_1, skv_2, skv_3 )
  ( skv_1, skv_2, skv_96 )
  ( skv_1, skv_94, skv_94 )
  ( skv_1, skv_95, skv_94 )
  ( skv_1, skv_128, skv_3 )
  ( skv_1, skv_139, skv_2 )
  ( skv_2, skv_128, skv_3 )
  ( skv_2, skv_140, skv_3 )
  ( skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (BOUND_VARIABLE_2154 $$unsorted)) (or (not (txtdep X Y)) (not (present Y BOUND_VARIABLE_2154)) (present X BOUND_VARIABLE_2154)) ) : 
  ( skv_1, skv_3, skv_1 )
  ( skv_1, skv_94, skv_1 )
  ( skv_1, skv_128, skv_2 )
  ( skv_1, skv_139, skv_3 )
  ( skv_2, skv_1, skv_2 )
  ( skv_2, skv_140, skv_3 )

Instantiations of (forall ((Y1 $$unsorted) (T1 $$unsorted) (Y2 $$unsorted) (T2 $$unsorted) (BOUND_VARIABLE_2167 $$unsorted)) (or (not (phtxtequiv Y1 T1 Y2 T2)) (= (txtdep BOUND_VARIABLE_2167 Y1) (txtdep BOUND_VARIABLE_2167 Y2))) ) : 
  ( skv_1, skv_3, skv_3, skv_3, skv_1 )
  ( skv_3, skv_3, skv_1, skv_3, skv_1 )
  ( skv_157, skv_94, skv_94, skv_158, skv_1 )
  ( skv_202, skv_3, skv_128, skv_203, skv_1 )
  ( skv_256, skv_96, skv_2, skv_257, skv_1 )
  ( skv_256, skv_96, skv_2, skv_257, skv_2 )

Instantiations of (forall ((X1 $$unsorted) (Y1 $$unsorted) (X2 $$unsorted) (Y2 $$unsorted) (T $$unsorted)) (or (not (txtdep X1 Y1)) (not (txtdep X2 Y2)) (= (ppt X1 X2 T) (ppt Y1 Y2 T))) ) : 
  ( skv_1, skv_3, skv_1, skv_3, skv_1 )
  ( skv_1, skv_3, skv_1, skv_3, skv_3 )
  ( skv_1, skv_94, skv_1, skv_94, skv_1 )
  ( skv_1, skv_94, skv_1, skv_94, skv_94 )
  ( skv_1, skv_128, skv_1, skv_128, skv_3 )
  ( skv_1, skv_128, skv_1, skv_139, skv_3 )
  ( skv_1, skv_128, skv_1, skv_256, skv_3 )
  ( skv_1, skv_128, skv_2, skv_292, skv_3 )
  ( skv_1, skv_128, skv_263, skv_2, skv_3 )
  ( skv_1, skv_139, skv_1, skv_128, skv_3 )
  ( skv_1, skv_139, skv_2, skv_140, skv_3 )
  ( skv_1, skv_256, skv_1, skv_128, skv_3 )
  ( skv_2, skv_140, skv_1, skv_139, skv_3 )
  ( skv_3, skv_1, skv_3, skv_1, skv_1 )
  ( skv_3, skv_1, skv_3, skv_1, skv_3 )

Instantiations of (forall ((X1 $$unsorted) (Y1 $$unsorted) (X2 $$unsorted) (Y2 $$unsorted) (T $$unsorted)) (or (not (txtdep X1 Y1)) (not (txtdep X2 Y2)) (= (phtxtprec X1 X2 T) (phtxtprec Y1 Y2 T))) ) : 
  ( skv_1, skv_3, skv_1, skv_3, skv_1 )
  ( skv_3, skv_1, skv_3, skv_1, skv_1 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted) (Z $$unsorted)) (or (not (txt X T)) (not (ppt Z X T)) (txt Z T)) ) : 
  ( skv_1, skv_3, skv_3 )
  ( skv_1, skv_3, skv_128 )
  ( skv_1, skv_3, skv_130 )
  ( skv_1, skv_3, skv_205 )
  ( skv_2, skv_3, skv_128 )
  ( skv_3, skv_1, skv_1 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted)) (or (not (phtxt X T)) (not (txt X T))) ) : 
  ( skv_1, skv_1 )
  ( skv_1, skv_3 )
  ( skv_1, skv_97 )
  ( skv_2, skv_3 )
  ( skv_3, skv_3 )
  ( skv_94, skv_155 )
  ( skv_128, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (= (txtppt X Y T) (not (forall ((X1 $$unsorted) (Y1 $$unsorted)) (or (not (txtdep X X1)) (not (txtdep Y Y1)) (not (ppt X1 Y1 T))) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (= (txtpt X Y T) (not (forall ((X1 $$unsorted) (Y1 $$unsorted)) (or (not (txtdep X X1)) (not (txtdep Y Y1)) (not (pt X1 Y1 T))) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_1, skv_2, skv_3 )
  ( skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (= (txtoverlap X Y T) (not (forall ((X1 $$unsorted) (Y1 $$unsorted)) (or (not (txtdep X X1)) (not (txtdep Y Y1)) (not (phoverlap X1 Y1 T))) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (= (txtprec X Y T) (not (forall ((X1 $$unsorted) (Y1 $$unsorted)) (or (not (txtdep X X1)) (not (txtdep Y Y1)) (not (phtxtprec X1 Y1 T))) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (= (txtrep X Y T) (not (forall ((X1 $$unsorted)) (or (not (txtdep X X1)) (not (phrep X1 Y T))) ))) ) : 
  ( skv_1, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (Z $$unsorted) (T $$unsorted)) (= (txtsumpt X Y Z T) (not (forall ((X1 $$unsorted) (Y1 $$unsorted) (Z1 $$unsorted)) (or (not (txtdep X X1)) (not (txtdep Y Y1)) (not (txtdep Z Z1)) (not (phsumpt X1 Y1 Z1 T))) ))) ) : 
  ( skv_1, skv_1, skv_1, skv_1 )
  ( skv_3, skv_3, skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted)) (= (comptxt X T) (not (forall ((X1 $$unsorted)) (or (not (txtdep X X1)) (not (compphtxt X1 T))) ))) ) : 
  ( skv_1, skv_1 )
  ( skv_3, skv_3 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted)) (or (not (phtxt X T)) (and (obj X) (time T))) ) : 
  ( skv_1, skv_1 )
  ( skv_2, skv_3 )
  ( skv_2, skv_169 )
  ( skv_3, skv_1 )
  ( skv_3, skv_3 )
  ( skv_90, skv_1 )
  ( skv_94, skv_155 )
  ( skv_128, skv_3 )
  ( skv_128, skv_201 )
  ( skv_128, skv_203 )
  ( skv_139, skv_252 )
  ( skv_206, skv_3 )
  ( skv_253, skv_96 )
  ( skv_292, skv_3 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted)) (or (not (txt X T)) (and (obj X) (time T))) ) : 
  ( skv_1, skv_3 )
  ( skv_1, skv_96 )
  ( skv_2, skv_179 )
  ( skv_3, skv_1 )
  ( skv_3, skv_160 )
  ( skv_130, skv_3 )
  ( skv_263, skv_96 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted)) (or (not (txtdep X Y)) (and (obj X) (obj Y))) ) : 
  ( skv_1, skv_3 )
  ( skv_1, skv_90 )
  ( skv_1, skv_94 )
  ( skv_1, skv_128 )
  ( skv_1, skv_139 )
  ( skv_2, skv_140 )
  ( skv_2, skv_292 )
  ( skv_3, skv_1 )
  ( skv_263, skv_2 )

Instantiations of (forall ((X $$unsorted) (T $$unsorted)) (or (not (present X T)) (and (nontime X) (time T))) ) : 
  ( skv_1, skv_1 )
  ( skv_1, skv_2 )
  ( skv_1, skv_94 )
  ( skv_1, skv_98 )
  ( skv_2, skv_1 )
  ( skv_2, skv_2 )
  ( skv_2, skv_3 )
  ( skv_3, skv_1 )
  ( skv_94, skv_1 )
  ( skv_128, skv_2 )
  ( skv_139, skv_3 )
  ( skv_157, skv_94 )
  ( skv_197, skv_3 )
  ( skv_260, skv_96 )

Instantiations of (forall ((S $$unsorted) (R $$unsorted) (T $$unsorted)) (or (not (occ S R T)) (and (nontime S) (reg R) (time T))) ) : 
  ( skv_1, skv_1, skv_3 )
  ( skv_1, skv_173, skv_1 )
  ( skv_2, skv_260, skv_96 )
  ( skv_3, skv_1, skv_3 )
  ( skv_3, skv_3, skv_1 )
  ( skv_3, skv_3, skv_3 )
  ( skv_3, skv_133, skv_3 )
  ( skv_94, skv_227, skv_94 )
  ( skv_128, skv_197, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (or (not (ppt X Y T)) (and (nontime X) (nontime Y) (time T))) ) : 
  ( skv_1, skv_2, skv_3 )
  ( skv_1, skv_3, skv_3 )
  ( skv_1, skv_195, skv_3 )
  ( skv_2, skv_96, skv_1 )
  ( skv_2, skv_195, skv_3 )
  ( skv_3, skv_1, skv_3 )
  ( skv_3, skv_3, skv_1 )
  ( skv_3, skv_128, skv_3 )
  ( skv_3, skv_195, skv_3 )
  ( skv_94, skv_94, skv_1 )
  ( skv_94, skv_94, skv_94 )
  ( skv_128, skv_206, skv_3 )
  ( skv_130, skv_1, skv_3 )
  ( skv_195, skv_1, skv_3 )
  ( skv_195, skv_2, skv_3 )
  ( skv_204, skv_1, skv_3 )
  ( skv_205, skv_1, skv_3 )
  ( skv_293, skv_2, skv_3 )
  ( skv_359, skv_2, skv_3 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (or (not (phtxtprec X Y T)) (and (obj X) (obj Y) (time T))) ) : 
  ( skv_3, skv_3, skv_1 )

Instantiations of (forall ((X $$unsorted) (T1 $$unsorted) (Y $$unsorted) (T2 $$unsorted)) (or (not (phtxtequiv X T1 Y T2)) (and (obj X) (obj Y) (time T1) (time T2))) ) : 
  ( skv_3, skv_1, skv_3, skv_3 )
  ( skv_3, skv_3, skv_3, skv_1 )
  ( skv_99, skv_1, skv_1, skv_100 )
  ( skv_157, skv_94, skv_94, skv_158 )
  ( skv_202, skv_3, skv_128, skv_203 )
  ( skv_256, skv_96, skv_2, skv_257 )

Instantiations of (forall ((X $$unsorted) (Y $$unsorted) (T $$unsorted)) (or (not (phrep X Y T)) (and (obj X) (obj Y) (time T))) ) : 
  ( skv_3, skv_3, skv_1 )

Instantiations of (forall ((X $$unsorted)) (or (and (not (obj X)) (not (reg X))) (nontime X)) ) : 
  ( skv_1 )
  ( skv_2 )
  ( skv_3 )
  ( skv_94 )
  ( skv_96 )
  ( skv_195 )

Instantiations of (forall ((T $$unsorted)) (or (not (time T)) (not (nontime T))) ) : 
  ( skv_1 )
  ( skv_2 )
  ( skv_3 )
  ( skv_94 )
  ( skv_96 )
  ( skv_128 )
  ( skv_130 )
  ( skv_140 )
  ( skv_195 )
  ( skv_197 )

Instantiations of (forall ((X $$unsorted)) (or (not (obj X)) (not (reg X))) ) : 
  ( skv_1 )
  ( skv_2 )
  ( skv_3 )
  ( skv_128 )
  ( skv_139 )
  ( skv_140 )
  ( skv_206 )
  ( skv_256 )
  ( skv_263 )
  ( skv_292 )

Instantiations of (forall ((Z $$unsorted)) (not (pt Z skv_1 skv_1)) ) : 
  ( skv_1 )
  ( skv_3 )
  ( skv_94 )
  ( skv_115 )
  ( skv_139 )
  ( skv_172 )
  ( skv_209 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_1)) (overlap V skv_1 skv_1)) ) : 
  ( skv_115 )
  ( skv_209 )

Instantiations of (forall ((Z $$unsorted)) (not (sumpt Z skv_1 skv_1 skv_1)) ) : 
  ( skv_3 )

Instantiations of (forall ((T1 $$unsorted)) (or (not (time T1)) (present skv_1 T1)) ) : 
  ( skv_2 )

Instantiations of (forall ((Z $$unsorted)) (not (phpt Z skv_1 skv_1)) ) : 
  ( skv_3 )
  ( skv_116 )
  ( skv_174 )

Instantiations of (forall ((Y $$unsorted)) (phpt Y skv_1 skv_1) ) : 
  ( skv_1 )

Instantiations of (forall ((T $$unsorted)) (not (txt skv_1 T)) ) : 
  ( skv_3 )

Instantiations of (forall ((T $$unsorted)) (not (phtxt skv_1 T)) ) : 
  ( skv_3 )

Instantiations of (forall ((Y $$unsorted)) (or (not (phtxt Y skv_1)) (not (txtdep skv_1 Y))) ) : 
  ( skv_1 )
  ( skv_3 )
  ( skv_94 )
  ( skv_128 )

Instantiations of (forall ((Z $$unsorted) (T1 $$unsorted)) (not (phtxtequiv Z skv_1 skv_1 T1)) ) : 
  ( skv_3, skv_3 )

Instantiations of (forall ((X1 $$unsorted) (Y1 $$unsorted)) (or (not (txtdep skv_1 X1)) (not (txtdep skv_1 Y1)) (not (ppt X1 Y1 skv_1))) ) : 
  ( skv_3, skv_3 )
  ( skv_94, skv_94 )
  ( skv_94, skv_95 )

Instantiations of (forall ((X1 $$unsorted) (Y1 $$unsorted)) (or (not (txtdep skv_1 X1)) (not (txtdep skv_1 Y1)) (not (pt X1 Y1 skv_1))) ) : 
  ( skv_3, skv_3 )
  ( skv_139, skv_139 )

Instantiations of (forall ((X1 $$unsorted) (Y1 $$unsorted)) (or (not (txtdep skv_1 X1)) (not (txtdep skv_1 Y1)) (not (phoverlap X1 Y1 skv_1))) ) : 
  ( skv_3, skv_3 )

Instantiations of (forall ((X1 $$unsorted) (Y1 $$unsorted)) (or (not (txtdep skv_1 X1)) (not (txtdep skv_1 Y1)) (not (phtxtprec X1 Y1 skv_1))) ) : 
  ( skv_3, skv_3 )

Instantiations of (forall ((X1 $$unsorted)) (or (not (txtdep skv_1 X1)) (not (phrep X1 skv_1 skv_1))) ) : 
  ( skv_3 )

Instantiations of (forall ((X1 $$unsorted) (Y1 $$unsorted) (Z1 $$unsorted)) (or (not (txtdep skv_1 X1)) (not (txtdep skv_1 Y1)) (not (txtdep skv_1 Z1)) (not (phsumpt X1 Y1 Z1 skv_1))) ) : 
  ( skv_3, skv_3, skv_3 )

Instantiations of (forall ((X1 $$unsorted)) (or (not (txtdep skv_1 X1)) (not (compphtxt X1 skv_1))) ) : 
  ( skv_3 )

Instantiations of (forall ((T $$unsorted)) (not (present skv_3 T)) ) : 
  ( skv_3 )

Instantiations of (forall ((Z $$unsorted)) (not (pt Z skv_3 skv_3)) ) : 
  ( skv_2 )
  ( skv_94 )
  ( skv_128 )
  ( skv_132 )
  ( skv_139 )
  ( skv_197 )
  ( skv_209 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_1)) (overlap V skv_1 skv_1) (overlap V skv_3 skv_1)) ) : 
  ( skv_209 )

Instantiations of (forall ((T1 $$unsorted)) (or (not (time T1)) (present skv_3 T1)) ) : 
  ( skv_2 )
  ( skv_3 )

Instantiations of (forall ((Z $$unsorted)) (not (phpt Z skv_3 skv_3)) ) : 
  ( skv_134 )

Instantiations of (forall ((Z $$unsorted)) (or (phtxt Z skv_3) (not (pt Z skv_3 skv_3))) ) : 
  ( skv_1 )
  ( skv_2 )

Instantiations of (forall ((Y $$unsorted)) (phpt Y skv_3 skv_3) ) : 
  ( skv_3 )

Instantiations of (forall ((T $$unsorted)) (not (txt skv_3 T)) ) : 
  ( skv_96 )
  ( skv_179 )

Instantiations of (forall ((X1 $$unsorted) (Y1 $$unsorted)) (or (not (txtdep skv_3 X1)) (not (txtdep skv_3 Y1)) (not (ppt X1 Y1 skv_3))) ) : 
  ( skv_94, skv_94 )
  ( skv_94, skv_95 )

Instantiations of (forall ((X1 $$unsorted) (Y1 $$unsorted)) (or (not (txtdep skv_3 X1)) (not (txtdep skv_3 Y1)) (not (pt X1 Y1 skv_3))) ) : 
  ( skv_139, skv_139 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_3)) (overlap V skv_1 skv_3)) ) : 
  ( skv_204 )
  ( skv_208 )
  ( skv_209 )
  ( skv_361 )
  ( skv_395 )

Instantiations of (forall ((Y $$unsorted)) (or (not (phtxt Y skv_3)) (not (txtdep skv_1 Y))) ) : 
  ( skv_94 )

Instantiations of (forall ((X1 $$unsorted) (Y1 $$unsorted)) (or (not (txtdep skv_1 X1)) (not (txtdep skv_2 Y1)) (not (pt X1 Y1 skv_3))) ) : 
  ( skv_128, skv_128 )
  ( skv_128, skv_292 )

Instantiations of (forall ((T $$unsorted)) (not (phtxt skv_2 T)) ) : 
  ( skv_3 )

Instantiations of (forall ((T $$unsorted)) (not (txt skv_2 T)) ) : 
  ( skv_3 )
  ( skv_96 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_129 skv_3)) (overlap V skv_1 skv_3)) ) : 
  ( skv_1 )
  ( skv_128 )
  ( skv_204 )
  ( skv_208 )
  ( skv_314 )
  ( skv_361 )
  ( skv_395 )

Instantiations of (forall ((Z $$unsorted)) (or (not (pt Z skv_130 skv_3)) (not (pt Z skv_1 skv_3))) ) : 
  ( skv_1 )
  ( skv_2 )
  ( skv_128 )
  ( skv_130 )
  ( skv_139 )
  ( skv_209 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_128 skv_3)) (overlap V skv_1 skv_3)) ) : 
  ( skv_128 )
  ( skv_314 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_3)) (overlap V skv_1 skv_3) (overlap V skv_3 skv_3)) ) : 
  ( skv_209 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_3)) (overlap V skv_3 skv_3)) ) : 
  ( skv_1 )
  ( skv_195 )
  ( skv_204 )
  ( skv_209 )

Instantiations of (forall ((T1 $$unsorted)) (or (not (time T1)) (present skv_128 T1)) ) : 
  ( skv_2 )

Instantiations of (forall ((Z $$unsorted)) (or (not (phpt Z skv_128 skv_3)) (phoverlap Z skv_128 skv_3)) ) : 
  ( skv_128 )

Instantiations of (forall ((Y $$unsorted)) (phpt Y skv_128 skv_3) ) : 
  ( skv_1 )

Instantiations of (forall ((T1 $$unsorted)) (or (not (time T1)) (present skv_94 T1)) ) : 
  ( skv_2 )

Instantiations of (forall ((Y $$unsorted)) (phpt Y skv_94 skv_94) ) : 
  ( skv_1 )

Instantiations of (forall ((Z $$unsorted)) (or (phtxt Z skv_96) (not (pt Z skv_2 skv_96))) ) : 
  ( skv_1 )
  ( skv_2 )

Instantiations of (forall ((Y $$unsorted)) (phpt Y skv_2 skv_96) ) : 
  ( skv_3 )

Instantiations of (forall ((T $$unsorted)) (not (phtxt skv_96 T)) ) : 
  ( skv_252 )

Instantiations of (forall ((Y $$unsorted)) (or (not (txt Y skv_96)) (not (txtdep Y skv_2))) ) : 
  ( skv_1 )

Instantiations of (forall ((Z $$unsorted) (T1 $$unsorted)) (not (phtxtequiv Z skv_96 skv_2 T1)) ) : 
  ( skv_2, skv_96 )

Instantiations of (forall ((Z $$unsorted)) (or (not (pt Z skv_204 skv_3)) (not (pt Z skv_1 skv_3))) ) : 
  ( skv_130 )
  ( skv_317 )
  ( skv_321 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_254 skv_96)) (overlap V skv_1 skv_96)) ) : 
  ( skv_2 )
  ( skv_197 )
  ( skv_208 )
  ( skv_317 )
  ( skv_318 )
  ( skv_396 )
  ( skv_398 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_1 skv_3)) ) : 
  ( skv_317 )
  ( skv_318 )
  ( skv_396 )
  ( skv_398 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_128 skv_3)) (overlap V skv_128 skv_3) (overlap V skv_1 skv_3)) ) : 
  ( skv_313 )
  ( skv_320 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_3)) (overlap V skv_130 skv_3)) ) : 
  ( skv_208 )
  ( skv_361 )
  ( skv_395 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_3)) (overlap V skv_130 skv_3) (overlap V skv_1 skv_3)) ) : 
  ( skv_208 )
  ( skv_361 )
  ( skv_395 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_2 skv_3)) ) : 
  ( skv_318 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_2 skv_3) (overlap V skv_1 skv_3)) ) : 
  ( skv_317 )

Instantiations of (forall ((Z $$unsorted)) (or (not (ppt Z skv_2 skv_3)) (overlap skv_1 Z skv_3)) ) : 
  ( skv_197 )

Instantiations of (forall ((Y $$unsorted)) (or (not (phtxt Y skv_3)) (not (txtdep skv_2 Y))) ) : 
  ( skv_128 )
  ( skv_139 )
  ( skv_206 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_294 skv_3)) (overlap V skv_128 skv_3) (overlap V skv_1 skv_3)) ) : 
  ( skv_2 )
  ( skv_128 )
  ( skv_313 )
  ( skv_317 )
  ( skv_320 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_295 skv_3)) (overlap V skv_1 skv_3) (overlap V skv_128 skv_3)) ) : 
  ( skv_2 )
  ( skv_128 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_296 skv_3)) (overlap V skv_128 skv_3) (overlap V skv_2 skv_3)) ) : 
  ( skv_1 )
  ( skv_2 )
  ( skv_128 )
  ( skv_197 )
  ( skv_365 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_297 skv_3)) (overlap V skv_1 skv_3) (overlap V skv_2 skv_3)) ) : 
  ( skv_2 )
  ( skv_128 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_298 skv_3)) (overlap V skv_2 skv_3) (overlap V skv_128 skv_3)) ) : 
  ( skv_1 )
  ( skv_2 )
  ( skv_128 )
  ( skv_197 )
  ( skv_365 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_299 skv_3)) (overlap V skv_2 skv_3) (overlap V skv_1 skv_3)) ) : 
  ( skv_2 )
  ( skv_128 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_300 skv_3)) (overlap V skv_2 skv_3)) ) : 
  ( skv_1 )
  ( skv_2 )
  ( skv_128 )
  ( skv_197 )
  ( skv_365 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_304 skv_3)) (overlap V skv_128 skv_3) (overlap V skv_130 skv_3)) ) : 
  ( skv_2 )
  ( skv_128 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_305 skv_3)) (overlap V skv_130 skv_3) (overlap V skv_128 skv_3)) ) : 
  ( skv_2 )
  ( skv_128 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_306 skv_3)) (overlap V skv_130 skv_3)) ) : 
  ( skv_2 )
  ( skv_197 )
  ( skv_208 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_307 skv_3)) (overlap V skv_130 skv_3) (overlap V skv_1 skv_3)) ) : 
  ( skv_2 )
  ( skv_197 )
  ( skv_208 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_309 skv_3)) (overlap V skv_1 skv_3) (overlap V skv_130 skv_3)) ) : 
  ( skv_2 )
  ( skv_197 )
  ( skv_208 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_308 skv_3)) (overlap V skv_130 skv_3) (overlap V skv_2 skv_3)) ) : 
  ( skv_2 )
  ( skv_128 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_310 skv_3)) (overlap V skv_2 skv_3) (overlap V skv_130 skv_3)) ) : 
  ( skv_2 )
  ( skv_128 )

Instantiations of (forall ((Z $$unsorted)) (or (not (pt Z skv_317 skv_3)) (not (pt Z skv_2 skv_3))) ) : 
  ( skv_197 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_128 skv_3)) ) : 
  ( skv_1 )
  ( skv_317 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_195 skv_3)) (overlap V skv_2 skv_3)) ) : 
  ( skv_365 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_195 skv_3)) (overlap V skv_2 skv_3) (overlap V skv_128 skv_3)) ) : 
  ( skv_365 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_197 skv_3)) ) : 
  ( skv_359 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_1 skv_3)) (overlap V skv_195 skv_3)) ) : 
  ( skv_1 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_195 skv_3)) (overlap V skv_1 skv_3)) ) : 
  ( skv_128 )
  ( skv_365 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_195 skv_3)) (overlap V skv_128 skv_3)) ) : 
  ( skv_356 )
  ( skv_365 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_128 skv_3)) (overlap V skv_2 skv_3)) ) : 
  ( skv_196 )
  ( skv_313 )
  ( skv_352 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_128 skv_3)) (overlap V skv_3 skv_3)) ) : 
  ( skv_363 )

Instantiations of (forall ((Z $$unsorted)) (or (not (pt Z skv_318 skv_3)) (not (pt Z skv_2 skv_3))) ) : 
  ( skv_197 )

Instantiations of (forall ((Z $$unsorted)) (or (not (pt Z skv_1 skv_3)) (not (pt Z skv_293 skv_3))) ) : 
  ( skv_197 )
  ( skv_208 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_291 skv_3)) (overlap V skv_128 skv_3)) ) : 
  ( skv_1 )
  ( skv_197 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_345 skv_3)) (overlap V skv_128 skv_3) (overlap V skv_197 skv_3)) ) : 
  ( skv_197 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_346 skv_3)) (overlap V skv_197 skv_3) (overlap V skv_128 skv_3)) ) : 
  ( skv_197 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_348 skv_3)) (overlap V skv_197 skv_3) (overlap V skv_1 skv_3)) ) : 
  ( skv_259 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_349 skv_3)) (overlap V skv_1 skv_3) (overlap V skv_197 skv_3)) ) : 
  ( skv_259 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_350 skv_3)) (overlap V skv_197 skv_3) (overlap V skv_2 skv_3)) ) : 
  ( skv_197 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_351 skv_3)) (overlap V skv_2 skv_3) (overlap V skv_197 skv_3)) ) : 
  ( skv_197 )

Instantiations of (forall ((Z $$unsorted)) (or (not (pt Z skv_313 skv_3)) (not (pt Z skv_128 skv_3))) ) : 
  ( skv_1 )

Instantiations of (forall ((Z $$unsorted)) (or (not (pt Z skv_1 skv_3)) (not (pt Z skv_128 skv_3))) ) : 
  ( skv_1 )

Instantiations of (forall ((Z $$unsorted)) (or (not (pt Z skv_359 skv_3)) (not (pt Z skv_2 skv_3))) ) : 
  ( skv_1 )
  ( skv_139 )

Instantiations of (forall ((Z $$unsorted)) (or (not (pt Z skv_359 skv_3)) (not (pt Z skv_197 skv_3))) ) : 
  ( skv_197 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_197 skv_3)) (overlap V skv_2 skv_3)) ) : 
  ( skv_403 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_140 skv_3)) (overlap V skv_1 skv_3)) ) : 
  ( skv_197 )
  ( skv_395 )

Instantiations of (forall ((V $$unsorted)) (or (not (pt V skv_2 skv_3)) (overlap V skv_195 skv_3)) ) : 
  ( skv_398 )
  ( skv_400 )

Instantiations of (forall ((Z $$unsorted)) (or (phtxt Z skv_3) (not (pt Z skv_140 skv_3))) ) : 
  ( skv_1 )

Instantiations of (forall ((Y $$unsorted)) (phpt Y skv_140 skv_3) ) : 
  ( skv_2 )

Instantiations of (forall ((Y $$unsorted)) (or (not (txt Y skv_3)) (not (txtdep Y skv_140))) ) : 
  ( skv_1 )

Instantiations of (forall ((Z $$unsorted)) (or (not (pt Z skv_358 skv_3)) (not (pt Z skv_197 skv_3))) ) : 
  ( skv_1 )

% SZS output end Proof for SOT_bhnA_a

% END OF SYSTEM OUTPUT
% RESULT: SOT_bhnA_a - CVC4---FOF-1.5pre says Theorem - CPU = 34.90 WC = 35.32 
% OUTPUT: SOT_bhnA_a - CVC4---FOF-1.5pre says Proof - CPU = 34.90 WC = 35.35