%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : COM146+1 : TPTP v8.1.2. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri May 19 10:14:46 EDT 2023
% Result : Theorem 11.21s 11.71s
% Output : Proof 11.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : COM146+1 : TPTP v8.1.2. Released v6.4.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n010.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Fri May 19 03:10:27 EDT 2023
% 0.13/0.34 % CPUTime :
% 11.21/11.71
% 11.21/11.71 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 11.21/11.71 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.21/11.71 %-----------------------------------------------------
% 11.21/11.71 ncf(matrix, plain, [(1202 ^ _259991) ^ [] : [-(vreduce(vvar(1197 ^ [])) = vsomeExp(1199 ^ []))], (1204 ^ _259991) ^ [] : [-(vtcheck(1198 ^ [], vvar(1197 ^ []), 1200 ^ []))], (1206 ^ _259991) ^ [] : [vtcheck(1198 ^ [], 1199 ^ [], 1200 ^ [])], (2 ^ _259991) ^ [_260135] : [-(_260135 = _260135)], (4 ^ _259991) ^ [_260242, _260244] : [_260244 = _260242, -(_260242 = _260244)], (10 ^ _259991) ^ [_260446, _260448, _260450] : [-(_260450 = _260446), _260450 = _260448, _260448 = _260446], (20 ^ _259991) ^ [_260759, _260761] : [-(visSomeType(_260759)), _260761 = _260759, visSomeType(_260761)], (30 ^ _259991) ^ [_261054, _261056] : [-(visValue(_261054)), _261056 = _261054, visValue(_261056)], (40 ^ _259991) ^ [_261349, _261351] : [-(visSomeExp(_261349)), _261351 = _261349, visSomeExp(_261351)], (50 ^ _259991) ^ [_261672, _261674, _261676, _261678] : [-(visFreeVar(_261676, _261672)), visFreeVar(_261678, _261674), _261678 = _261676, _261674 = _261672], (64 ^ _259991) ^ [_262124, _262126, _262128, _262130, _262132, _262134] : [-(vtcheck(_262132, _262128, _262124)), vtcheck(_262134, _262130, _262126), _262134 = _262132, _262130 = _262128, _262126 = _262124], (82 ^ _259991) ^ [_262691, _262693] : [_262693 = _262691, -(vgetSomeType(_262693) = vgetSomeType(_262691))], (88 ^ _259991) ^ [_262909, _262911] : [_262911 = _262909, -(vgensym(_262911) = vgensym(_262909))], (94 ^ _259991) ^ [_263127, _263129] : [_263129 = _263127, -(vgetSomeExp(_263129) = vgetSomeExp(_263127))], (100 ^ _259991) ^ [_263345, _263347] : [_263347 = _263345, -(vsomeType(_263347) = vsomeType(_263345))], (106 ^ _259991) ^ [_263619, _263621, _263623, _263625, _263627, _263629] : [-(vabs(_263629, _263625, _263621) = vabs(_263627, _263623, _263619)), _263629 = _263627, _263625 = _263623, _263621 = _263619], (120 ^ _259991) ^ [_264107, _264109, _264111, _264113] : [-(vapp(_264113, _264109) = vapp(_264111, _264107)), _264113 = _264111, _264109 = _264107], (130 ^ _259991) ^ [_264466, _264468, _264470, _264472] : [-(varrow(_264472, _264468) = varrow(_264470, _264466)), _264472 = _264470, _264468 = _264466], (140 ^ _259991) ^ [_264853, _264855, _264857, _264859, _264861, _264863] : [-(vsubst(_264863, _264859, _264855) = vsubst(_264861, _264857, _264853)), _264863 = _264861, _264859 = _264857, _264855 = _264853], (154 ^ _259991) ^ [_265341, _265343, _265345, _265347] : [-(vlookup(_265347, _265343) = vlookup(_265345, _265341)), _265347 = _265345, _265343 = _265341], (164 ^ _259991) ^ [_265728, _265730, _265732, _265734, _265736, _265738] : [-(vbind(_265738, _265734, _265730) = vbind(_265736, _265732, _265728)), _265738 = _265736, _265734 = _265732, _265730 = _265728], (178 ^ _259991) ^ [_266188, _266190] : [_266190 = _266188, -(vreduce(_266190) = vreduce(_266188))], (184 ^ _259991) ^ [_266406, _266408] : [_266408 = _266406, -(vsomeExp(_266408) = vsomeExp(_266406))], (190 ^ _259991) ^ [_266604, _266606] : [_266606 = _266604, -(vvar(_266606) = vvar(_266604))], (1158 ^ _259991) ^ [_309430, _309432, _309434, _309436, _309438] : [-(vtcheck(vbind(_309438, _309436, _309434), _309432, _309430)), -(visFreeVar(_309438, _309432)), vtcheck(_309434, _309432, _309430)], (1168 ^ _259991) ^ [_309830, _309832, _309834, _309836, _309838, _309840] : [-(vtcheck(_309838, vsubst(_309836, _309834, _309832), _309830)), vtcheck(_309838, _309834, _309840), vtcheck(vbind(_309836, _309840, _309838), _309832, _309830)], (1178 ^ _259991) ^ [_310233, _310235, _310237, _310239, _310241] : [-(vtcheck(vbind(_310241, _310239, _310237), _310235, _310233)), vlookup(_310241, _310237) = vnoType, vtcheck(_310237, _310235, _310233)], (1188 ^ _259991) ^ [_310602, _310604, _310606, _310608, _310610] : [-(vtcheck(_310606, _310604, _310602)), -(visFreeVar(_310610, _310604)), vtcheck(vbind(_310610, _310608, _310606), _310604, _310602)], (196 ^ _259991) ^ [_266902, _266904] : [vvar(_266904) = vvar(_266902), -(_266904 = _266902)], (202 ^ _259991) ^ [_267072, _267074] : [_267074 = _267072, -(vvar(_267074) = vvar(_267072))], (208 ^ _259991) ^ [_267368, _267370, _267372, _267374, _267376, _267378] : [vabs(_267378, _267376, _267374) = vabs(_267372, _267370, _267368), 211 ^ _259991 : [(212 ^ _259991) ^ [] : [-(_267378 = _267372)], (214 ^ _259991) ^ [] : [-(_267376 = _267370)], (216 ^ _259991) ^ [] : [-(_267374 = _267368)]]], (218 ^ _259991) ^ [_267735, _267737, _267739, _267741, _267743, _267745] : [-(vabs(_267745, _267743, _267741) = vabs(_267739, _267737, _267735)), _267745 = _267739, _267743 = _267737, _267741 = _267735], (232 ^ _259991) ^ [_268245, _268247, _268249, _268251] : [vapp(_268251, _268249) = vapp(_268247, _268245), 235 ^ _259991 : [(236 ^ _259991) ^ [] : [-(_268251 = _268247)], (238 ^ _259991) ^ [] : [-(_268249 = _268245)]]], (240 ^ _259991) ^ [_268510, _268512, _268514, _268516] : [-(vapp(_268516, _268514) = vapp(_268512, _268510)), _268516 = _268512, _268514 = _268510], (250 ^ _259991) ^ [_268855, _268857, _268859, _268861] : [vvar(_268861) = vabs(_268859, _268857, _268855)], (252 ^ _259991) ^ [_268972, _268974, _268976] : [vvar(_268976) = vapp(_268974, _268972)], (254 ^ _259991) ^ [_269114, _269116, _269118, _269120, _269122] : [vabs(_269122, _269120, _269118) = vapp(_269116, _269114)], (256 ^ _259991) ^ [_269264, _269266, _269268, _269270] : [_269264 = vabs(_269270, _269268, _269266), -(visValue(_269264))], (262 ^ _259991) ^ [_269492, _269494] : [_269492 = vvar(_269494), visValue(_269492)], (268 ^ _259991) ^ [_269719, _269721, _269723] : [_269719 = vapp(_269723, _269721), visValue(_269719)], (274 ^ _259991) ^ [_269968, _269970, _269972, _269974] : [_269974 = _269968, _269972 = vvar(_269970), 281 ^ _259991 : [(282 ^ _259991) ^ [] : [_269970 = _269968, -(visFreeVar(_269974, _269972))], (288 ^ _259991) ^ [] : [visFreeVar(_269974, _269972), -(_269970 = _269968)]]], (294 ^ _259991) ^ [_270622, _270624, _270626, _270628, _270630, _270632] : [_270630 = _270624, _270628 = vabs(_270626, _270632, _270622), 301 ^ _259991 : [(312 ^ _259991) ^ [] : [visFreeVar(_270630, _270628), 315 ^ _259991 : [(316 ^ _259991) ^ [] : [_270626 = _270624], (318 ^ _259991) ^ [] : [-(visFreeVar(_270624, _270622))]]], (302 ^ _259991) ^ [] : [-(visFreeVar(_270630, _270628)), -(_270626 = _270624), visFreeVar(_270624, _270622)]]], (320 ^ _259991) ^ [_271498, _271500, _271502, _271504, _271506] : [_271506 = _271500, _271504 = vapp(_271502, _271498), 327 ^ _259991 : [(328 ^ _259991) ^ [] : [329 ^ _259991 : [(330 ^ _259991) ^ [] : [visFreeVar(_271500, _271502)], (332 ^ _259991) ^ [] : [visFreeVar(_271500, _271498)]], -(visFreeVar(_271506, _271504))], (336 ^ _259991) ^ [] : [visFreeVar(_271506, _271504), -(visFreeVar(_271500, _271502)), -(visFreeVar(_271500, _271498))]]], (356 ^ _259991) ^ [] : [357 ^ _259991 : [(358 ^ _259991) ^ [] : [-(true___)], (360 ^ _259991) ^ [] : [true___]], -(vempty = vempty)], (346 ^ _259991) ^ [] : [vempty = vempty, true___, -(true___)], (364 ^ _259991) ^ [_272738, _272740, _272742, _272744, _272746, _272748] : [vbind(_272748, _272746, _272744) = vbind(_272742, _272740, _272738), 367 ^ _259991 : [(368 ^ _259991) ^ [] : [-(_272748 = _272742)], (370 ^ _259991) ^ [] : [-(_272746 = _272740)], (372 ^ _259991) ^ [] : [-(_272744 = _272738)]]], (374 ^ _259991) ^ [_273105, _273107, _273109, _273111, _273113, _273115] : [-(vbind(_273115, _273113, _273111) = vbind(_273109, _273107, _273105)), _273115 = _273109, _273113 = _273107, _273111 = _273105], (398 ^ _259991) ^ [] : [399 ^ _259991 : [(400 ^ _259991) ^ [] : [-(true___)], (402 ^ _259991) ^ [] : [true___]], -(vnoType = vnoType)], (388 ^ _259991) ^ [] : [vnoType = vnoType, true___, -(true___)], (406 ^ _259991) ^ [_273949, _273951] : [vsomeType(_273951) = vsomeType(_273949), -(_273951 = _273949)], (412 ^ _259991) ^ [_274119, _274121] : [_274121 = _274119, -(vsomeType(_274121) = vsomeType(_274119))], (418 ^ _259991) ^ [_274337, _274339, _274341] : [vempty = vbind(_274341, _274339, _274337)], (420 ^ _259991) ^ [_274422] : [vnoType = vsomeType(_274422)], (422 ^ _259991) ^ [_274517] : [_274517 = vnoType, visSomeType(_274517)], (428 ^ _259991) ^ [_274720, _274722] : [_274720 = vsomeType(_274722), -(visSomeType(_274720))], (434 ^ _259991) ^ [_274946, _274948, _274950] : [_274950 = vsomeType(_274946), _274948 = vgetSomeType(_274950), -(_274948 = _274946)], (444 ^ _259991) ^ [_275291, _275293, _275295, _275297] : [_275295 = _275297, _275293 = vempty, _275291 = vlookup(_275295, _275293), -(_275291 = vnoType)], (458 ^ _259991) ^ [_275785, _275787, _275789, _275791, _275793, _275795, _275797] : [_275791 = _275795, _275789 = vbind(_275793, _275785, _275797), _275795 = _275793, _275787 = vlookup(_275791, _275789), -(_275787 = vsomeType(_275785))], (476 ^ _259991) ^ [_276442, _276444, _276446, _276448, _276450, _276452, _276454] : [_276450 = _276444, _276448 = vbind(_276452, _276454, _276442), -(_276444 = _276452), _276446 = vlookup(_276450, _276448), -(_276446 = vlookup(_276444, _276442))], (494 ^ _259991) ^ [_277048, _277050, _277052] : [vlookup(_277052, _277050) = _277048, 500 ^ _259991 : [(501 ^ _259991) ^ [] : [-(_277052 = 499 ^ [_277048, _277050, _277052])], (503 ^ _259991) ^ [] : [-(_277050 = vempty)], (505 ^ _259991) ^ [] : [-(_277048 = vnoType)]], 512 ^ _259991 : [(513 ^ _259991) ^ [] : [-(_277052 = 509 ^ [_277048, _277050, _277052])], (515 ^ _259991) ^ [] : [-(_277050 = vbind(510 ^ [_277048, _277050, _277052], 511 ^ [_277048, _277050, _277052], 508 ^ [_277048, _277050, _277052]))], (517 ^ _259991) ^ [] : [-(509 ^ [_277048, _277050, _277052] = 510 ^ [_277048, _277050, _277052])], (519 ^ _259991) ^ [] : [-(_277048 = vsomeType(511 ^ [_277048, _277050, _277052]))]], 524 ^ _259991 : [(525 ^ _259991) ^ [] : [-(_277052 = 522 ^ [_277048, _277050, _277052])], (527 ^ _259991) ^ [] : [-(_277050 = vbind(521 ^ [_277048, _277050, _277052], 520 ^ [_277048, _277050, _277052], 523 ^ [_277048, _277050, _277052]))], (529 ^ _259991) ^ [] : [522 ^ [_277048, _277050, _277052] = 521 ^ [_277048, _277050, _277052]], (531 ^ _259991) ^ [] : [-(_277048 = vlookup(522 ^ [_277048, _277050, _277052], 523 ^ [_277048, _277050, _277052]))]]], (533 ^ _259991) ^ [_279243, _279245, _279247, _279249, _279251, _279253, _279255] : [-(vtcheck(vbind(_279251, _279249, _279247), _279245, _279243)), _279251 = _279255, vtcheck(vbind(_279251, _279249, vbind(_279255, _279253, _279247)), _279245, _279243)], (543 ^ _259991) ^ [_279690, _279692, _279694, _279696, _279698, _279700, _279702] : [-(vtcheck(vbind(_279702, _279700, vbind(_279698, _279696, _279694)), _279692, _279690)), -(_279698 = _279702), vtcheck(vbind(_279698, _279696, vbind(_279702, _279700, _279694)), _279692, _279690)], (553 ^ _259991) ^ [_280078, _280080] : [vgensym(_280078) = _280080, visFreeVar(_280080, _280078)], (559 ^ _259991) ^ [_280363, _280365, _280367, _280369, _280371, _280373, _280375] : [_280371 = _280375, _280369 = _280363, _280367 = vvar(_280373), _280375 = _280373, _280365 = vsubst(_280371, _280369, _280367), -(_280365 = _280363)], (581 ^ _259991) ^ [_281125, _281127, _281129, _281131, _281133, _281135, _281137] : [_281133 = _281135, _281131 = _281137, _281129 = vvar(_281125), -(_281135 = _281125), _281127 = vsubst(_281133, _281131, _281129), -(_281127 = vvar(_281125))], (603 ^ _259991) ^ [_281908, _281910, _281912, _281914, _281916, _281918, _281920, _281922] : [_281916 = vsubst(_281922, _281920, _281918), -(_281916 = vapp(vsubst(_281912, _281910, _281914), vsubst(_281912, _281910, _281908))), _281922 = _281912, _281920 = _281910, _281918 = vapp(_281914, _281908)], (621 ^ _259991) ^ [_282629, _282631, _282633, _282635, _282637, _282639, _282641, _282643, _282645] : [_282641 = _282643, _282639 = _282645, _282637 = vabs(_282633, _282631, _282629), _282643 = _282633, _282635 = vsubst(_282641, _282639, _282637), -(_282635 = vabs(_282633, _282631, _282629))], (643 ^ _259991) ^ [_283489, _283491, _283493, _283495, _283497, _283499, _283501, _283503, _283505, _283507] : [_283507 = _283499, _283505 = _283497, _283503 = vabs(_283493, _283495, _283489), _283501 = vsubst(_283507, _283505, _283503), -(_283501 = vsubst(_283499, _283497, vabs(_283491, _283495, vsubst(_283493, vvar(_283491), _283489)))), -(_283499 = _283493), visFreeVar(_283493, _283497), _283491 = vgensym(vapp(vapp(_283497, _283489), vvar(_283499)))], (673 ^ _259991) ^ [_284644, _284646, _284648, _284650, _284652, _284654, _284656, _284658, _284660] : [_284660 = _284648, _284658 = _284646, _284656 = vabs(_284652, _284650, _284644), -(_284648 = _284652), -(visFreeVar(_284652, _284646)), _284654 = vsubst(_284660, _284658, _284656), -(_284654 = vabs(_284652, _284650, vsubst(_284648, _284646, _284644)))], (699 ^ _259991) ^ [_285553, _285555, _285557, _285559] : [vsubst(_285559, _285557, _285555) = _285553, 707 ^ _259991 : [(708 ^ _259991) ^ [] : [-(_285559 = 704 ^ [_285553, _285555, _285557, _285559])], (710 ^ _259991) ^ [] : [-(_285557 = 706 ^ [_285553, _285555, _285557, _285559])], (712 ^ _259991) ^ [] : [-(_285555 = vvar(705 ^ [_285553, _285555, _285557, _285559]))], (714 ^ _259991) ^ [] : [-(704 ^ [_285553, _285555, _285557, _285559] = 705 ^ [_285553, _285555, _285557, _285559])], (716 ^ _259991) ^ [] : [-(_285553 = 706 ^ [_285553, _285555, _285557, _285559])]], 722 ^ _259991 : [(723 ^ _259991) ^ [] : [-(_285559 = 720 ^ [_285553, _285555, _285557, _285559])], (725 ^ _259991) ^ [] : [-(_285557 = 719 ^ [_285553, _285555, _285557, _285559])], (727 ^ _259991) ^ [] : [-(_285555 = vvar(721 ^ [_285553, _285555, _285557, _285559]))], (729 ^ _259991) ^ [] : [720 ^ [_285553, _285555, _285557, _285559] = 721 ^ [_285553, _285555, _285557, _285559]], (731 ^ _259991) ^ [] : [-(_285553 = vvar(721 ^ [_285553, _285555, _285557, _285559]))]], 738 ^ _259991 : [(739 ^ _259991) ^ [] : [-(_285559 = 735 ^ [_285553, _285555, _285557, _285559])], (741 ^ _259991) ^ [] : [-(_285557 = 736 ^ [_285553, _285555, _285557, _285559])], (743 ^ _259991) ^ [] : [-(_285555 = vapp(734 ^ [_285553, _285555, _285557, _285559], 737 ^ [_285553, _285555, _285557, _285559]))], (745 ^ _259991) ^ [] : [-(_285553 = vapp(vsubst(735 ^ [_285553, _285555, _285557, _285559], 736 ^ [_285553, _285555, _285557, _285559], 734 ^ [_285553, _285555, _285557, _285559]), vsubst(735 ^ [_285553, _285555, _285557, _285559], 736 ^ [_285553, _285555, _285557, _285559], 737 ^ [_285553, _285555, _285557, _285559])))]], 753 ^ _259991 : [(754 ^ _259991) ^ [] : [-(_285559 = 749 ^ [_285553, _285555, _285557, _285559])], (756 ^ _259991) ^ [] : [-(_285557 = 748 ^ [_285553, _285555, _285557, _285559])], (758 ^ _259991) ^ [] : [-(_285555 = vabs(750 ^ [_285553, _285555, _285557, _285559], 751 ^ [_285553, _285555, _285557, _285559], 752 ^ [_285553, _285555, _285557, _285559]))], (760 ^ _259991) ^ [] : [-(749 ^ [_285553, _285555, _285557, _285559] = 750 ^ [_285553, _285555, _285557, _285559])], (762 ^ _259991) ^ [] : [-(_285553 = vabs(750 ^ [_285553, _285555, _285557, _285559], 751 ^ [_285553, _285555, _285557, _285559], 752 ^ [_285553, _285555, _285557, _285559]))]], 771 ^ _259991 : [(772 ^ _259991) ^ [] : [-(_285559 = 765 ^ [_285553, _285555, _285557, _285559])], (774 ^ _259991) ^ [] : [-(_285557 = 766 ^ [_285553, _285555, _285557, _285559])], (776 ^ _259991) ^ [] : [-(_285555 = vabs(768 ^ [_285553, _285555, _285557, _285559], 767 ^ [_285553, _285555, _285557, _285559], 770 ^ [_285553, _285555, _285557, _285559]))], (778 ^ _259991) ^ [] : [765 ^ [_285553, _285555, _285557, _285559] = 768 ^ [_285553, _285555, _285557, _285559]], (780 ^ _259991) ^ [] : [-(visFreeVar(768 ^ [_285553, _285555, _285557, _285559], 766 ^ [_285553, _285555, _285557, _285559]))], (782 ^ _259991) ^ [] : [-(769 ^ [_285553, _285555, _285557, _285559] = vgensym(vapp(vapp(766 ^ [_285553, _285555, _285557, _285559], 770 ^ [_285553, _285555, _285557, _285559]), vvar(765 ^ [_285553, _285555, _285557, _285559]))))], (784 ^ _259991) ^ [] : [-(_285553 = vsubst(765 ^ [_285553, _285555, _285557, _285559], 766 ^ [_285553, _285555, _285557, _285559], vabs(769 ^ [_285553, _285555, _285557, _285559], 767 ^ [_285553, _285555, _285557, _285559], vsubst(768 ^ [_285553, _285555, _285557, _285559], vvar(769 ^ [_285553, _285555, _285557, _285559]), 770 ^ [_285553, _285555, _285557, _285559]))))]], 790 ^ _259991 : [(791 ^ _259991) ^ [] : [-(_285559 = 787 ^ [_285553, _285555, _285557, _285559])], (793 ^ _259991) ^ [] : [-(_285557 = 788 ^ [_285553, _285555, _285557, _285559])], (795 ^ _259991) ^ [] : [-(_285555 = vabs(785 ^ [_285553, _285555, _285557, _285559], 786 ^ [_285553, _285555, _285557, _285559], 789 ^ [_285553, _285555, _285557, _285559]))], (797 ^ _259991) ^ [] : [787 ^ [_285553, _285555, _285557, _285559] = 785 ^ [_285553, _285555, _285557, _285559]], (799 ^ _259991) ^ [] : [visFreeVar(785 ^ [_285553, _285555, _285557, _285559], 788 ^ [_285553, _285555, _285557, _285559])], (801 ^ _259991) ^ [] : [-(_285553 = vabs(785 ^ [_285553, _285555, _285557, _285559], 786 ^ [_285553, _285555, _285557, _285559], vsubst(787 ^ [_285553, _285555, _285557, _285559], 788 ^ [_285553, _285555, _285557, _285559], 789 ^ [_285553, _285555, _285557, _285559])))]]], (813 ^ _259991) ^ [] : [814 ^ _259991 : [(815 ^ _259991) ^ [] : [-(true___)], (817 ^ _259991) ^ [] : [true___]], -(vnoExp = vnoExp)], (803 ^ _259991) ^ [] : [vnoExp = vnoExp, true___, -(true___)], (821 ^ _259991) ^ [_293777, _293779] : [vsomeExp(_293779) = vsomeExp(_293777), -(_293779 = _293777)], (827 ^ _259991) ^ [_293947, _293949] : [_293949 = _293947, -(vsomeExp(_293949) = vsomeExp(_293947))], (833 ^ _259991) ^ [_294137] : [vnoExp = vsomeExp(_294137)], (835 ^ _259991) ^ [_294232] : [_294232 = vnoExp, visSomeExp(_294232)], (841 ^ _259991) ^ [_294435, _294437] : [_294435 = vsomeExp(_294437), -(visSomeExp(_294435))], (847 ^ _259991) ^ [_294661, _294663, _294665] : [_294665 = vsomeExp(_294661), _294663 = vgetSomeExp(_294665), -(_294663 = _294661)], (857 ^ _259991) ^ [_294992, _294994, _294996] : [_294994 = vvar(_294996), _294992 = vreduce(_294994), -(_294992 = vnoExp)], (867 ^ _259991) ^ [_295351, _295353, _295355, _295357, _295359] : [_295353 = vabs(_295359, _295357, _295355), _295351 = vreduce(_295353), -(_295351 = vnoExp)], (877 ^ _259991) ^ [_295762, _295764, _295766, _295768, _295770, _295772, _295774] : [_295772 = vapp(vabs(_295768, _295766, _295764), _295774), _295762 = vreduce(_295774), visSomeExp(_295762), _295770 = vreduce(_295772), -(_295770 = vsomeExp(vapp(vabs(_295768, _295766, _295764), vgetSomeExp(_295762))))], (895 ^ _259991) ^ [_296443, _296445, _296447, _296449, _296451, _296453, _296455] : [_296451 = vapp(vabs(_296447, _296455, _296443), _296445), _296449 = vreduce(_296451), -(_296449 = vsomeExp(vsubst(_296447, _296445, _296443))), _296453 = vreduce(_296445), -(visSomeExp(_296453)), visValue(_296445)], (917 ^ _259991) ^ [_297224, _297226, _297228, _297230, _297232, _297234, _297236] : [_297226 = vapp(vabs(_297236, _297234, _297232), _297228), _297224 = vreduce(_297226), -(_297224 = vnoExp), _297230 = vreduce(_297228), -(visSomeExp(_297230)), -(visValue(_297228))], (939 ^ _259991) ^ [_297968, _297970, _297972, _297974, _297976] : [_297974 = vapp(_297976, _297968), -(_297976 = vabs(944 ^ [_297968, _297970, _297972, _297974, _297976], 945 ^ [_297968, _297970, _297972, _297974, _297976], 946 ^ [_297968, _297970, _297972, _297974, _297976])), _297970 = vreduce(_297976), visSomeExp(_297970), _297972 = vreduce(_297974), -(_297972 = vsomeExp(vapp(vgetSomeExp(_297970), _297968)))], (964 ^ _259991) ^ [_298980, _298982, _298984, _298986, _298988] : [_298982 = vapp(_298986, _298988), -(_298986 = vabs(969 ^ [_298980, _298982, _298984, _298986, _298988], 970 ^ [_298980, _298982, _298984, _298986, _298988], 971 ^ [_298980, _298982, _298984, _298986, _298988])), _298984 = vreduce(_298986), -(visSomeExp(_298984)), _298980 = vreduce(_298982), -(_298980 = vnoExp)], (989 ^ _259991) ^ [_299939, _299941] : [vreduce(_299941) = _299939, 995 ^ _259991 : [(996 ^ _259991) ^ [] : [-(_299941 = vvar(994 ^ [_299939, _299941]))], (998 ^ _259991) ^ [] : [-(_299939 = vnoExp)]], 1004 ^ _259991 : [(1005 ^ _259991) ^ [] : [-(_299941 = vabs(1001 ^ [_299939, _299941], 1002 ^ [_299939, _299941], 1003 ^ [_299939, _299941]))], (1007 ^ _259991) ^ [] : [-(_299939 = vnoExp)]], 1015 ^ _259991 : [(1016 ^ _259991) ^ [] : [-(_299941 = vapp(vabs(1011 ^ [_299939, _299941], 1012 ^ [_299939, _299941], 1013 ^ [_299939, _299941]), 1010 ^ [_299939, _299941]))], (1018 ^ _259991) ^ [] : [-(1014 ^ [_299939, _299941] = vreduce(1010 ^ [_299939, _299941]))], (1020 ^ _259991) ^ [] : [-(visSomeExp(1014 ^ [_299939, _299941]))], (1022 ^ _259991) ^ [] : [-(_299939 = vsomeExp(vapp(vabs(1011 ^ [_299939, _299941], 1012 ^ [_299939, _299941], 1013 ^ [_299939, _299941]), vgetSomeExp(1014 ^ [_299939, _299941]))))]], 1030 ^ _259991 : [(1031 ^ _259991) ^ [] : [-(_299941 = vapp(vabs(1027 ^ [_299939, _299941], 1025 ^ [_299939, _299941], 1029 ^ [_299939, _299941]), 1028 ^ [_299939, _299941]))], (1033 ^ _259991) ^ [] : [-(1026 ^ [_299939, _299941] = vreduce(1028 ^ [_299939, _299941]))], (1035 ^ _259991) ^ [] : [visSomeExp(1026 ^ [_299939, _299941])], (1037 ^ _259991) ^ [] : [-(visValue(1028 ^ [_299939, _299941]))], (1039 ^ _259991) ^ [] : [-(_299939 = vsomeExp(vsubst(1027 ^ [_299939, _299941], 1028 ^ [_299939, _299941], 1029 ^ [_299939, _299941])))]], 1047 ^ _259991 : [(1048 ^ _259991) ^ [] : [-(_299941 = vapp(vabs(1042 ^ [_299939, _299941], 1043 ^ [_299939, _299941], 1044 ^ [_299939, _299941]), 1046 ^ [_299939, _299941]))], (1050 ^ _259991) ^ [] : [-(1045 ^ [_299939, _299941] = vreduce(1046 ^ [_299939, _299941]))], (1052 ^ _259991) ^ [] : [visSomeExp(1045 ^ [_299939, _299941])], (1054 ^ _259991) ^ [] : [visValue(1046 ^ [_299939, _299941])], (1056 ^ _259991) ^ [] : [-(_299939 = vnoExp)]], 1062 ^ _259991 : [(1063 ^ _259991) ^ [] : [-(_299941 = vapp(1059 ^ [_299939, _299941], 1061 ^ [_299939, _299941]))], (1065 ^ _259991) ^ [_304537, _304539, _304541] : [1059 ^ [_299939, _299941] = vabs(_304541, _304539, _304537)], (1067 ^ _259991) ^ [] : [-(1060 ^ [_299939, _299941] = vreduce(1059 ^ [_299939, _299941]))], (1069 ^ _259991) ^ [] : [-(visSomeExp(1060 ^ [_299939, _299941]))], (1071 ^ _259991) ^ [] : [-(_299939 = vsomeExp(vapp(vgetSomeExp(1060 ^ [_299939, _299941]), 1061 ^ [_299939, _299941])))]], 1075 ^ _259991 : [(1076 ^ _259991) ^ [] : [-(_299941 = vapp(1073 ^ [_299939, _299941], 1072 ^ [_299939, _299941]))], (1078 ^ _259991) ^ [_305311, _305313, _305315] : [1073 ^ [_299939, _299941] = vabs(_305315, _305313, _305311)], (1080 ^ _259991) ^ [] : [-(1074 ^ [_299939, _299941] = vreduce(1073 ^ [_299939, _299941]))], (1082 ^ _259991) ^ [] : [visSomeExp(1074 ^ [_299939, _299941])], (1084 ^ _259991) ^ [] : [-(_299939 = vnoExp)]]], (1086 ^ _259991) ^ [_305727, _305729, _305731, _305733] : [varrow(_305733, _305731) = varrow(_305729, _305727), 1089 ^ _259991 : [(1090 ^ _259991) ^ [] : [-(_305733 = _305729)], (1092 ^ _259991) ^ [] : [-(_305731 = _305727)]]], (1094 ^ _259991) ^ [_305992, _305994, _305996, _305998] : [-(varrow(_305998, _305996) = varrow(_305994, _305992)), _305998 = _305994, _305996 = _305992], (1104 ^ _259991) ^ [_306339, _306341, _306343] : [vlookup(_306341, _306343) = vsomeType(_306339), -(vtcheck(_306343, vvar(_306341), _306339))], (1110 ^ _259991) ^ [_306613, _306615, _306617, _306619, _306621] : [vtcheck(vbind(_306619, _306615, _306621), _306617, _306613), -(vtcheck(_306621, vabs(_306619, _306615, _306617), varrow(_306615, _306613)))], (1116 ^ _259991) ^ [_306909, _306911, _306913, _306915, _306917] : [-(vtcheck(_306915, vapp(_306913, _306911), _306909)), vtcheck(_306915, _306913, varrow(_306917, _306909)), vtcheck(_306915, _306911, _306917)], (1126 ^ _259991) ^ [_307250, _307252, _307254] : [vtcheck(_307250, _307254, _307252), 1132 ^ _259991 : [(1133 ^ _259991) ^ [] : [-(_307254 = vvar(1131 ^ [_307250, _307252, _307254]))], (1135 ^ _259991) ^ [] : [-(vlookup(1131 ^ [_307250, _307252, _307254], _307250) = vsomeType(_307252))]], 1142 ^ _259991 : [(1143 ^ _259991) ^ [] : [-(_307254 = vabs(1138 ^ [_307250, _307252, _307254], 1140 ^ [_307250, _307252, _307254], 1139 ^ [_307250, _307252, _307254]))], (1145 ^ _259991) ^ [] : [-(_307252 = varrow(1140 ^ [_307250, _307252, _307254], 1141 ^ [_307250, _307252, _307254]))], (1147 ^ _259991) ^ [] : [-(vtcheck(vbind(1138 ^ [_307250, _307252, _307254], 1140 ^ [_307250, _307252, _307254], _307250), 1139 ^ [_307250, _307252, _307254], 1141 ^ [_307250, _307252, _307254]))]], 1151 ^ _259991 : [(1152 ^ _259991) ^ [] : [-(_307254 = vapp(1148 ^ [_307250, _307252, _307254], 1149 ^ [_307250, _307252, _307254]))], (1154 ^ _259991) ^ [] : [-(vtcheck(_307250, 1148 ^ [_307250, _307252, _307254], varrow(1150 ^ [_307250, _307252, _307254], _307252)))], (1156 ^ _259991) ^ [] : [-(vtcheck(_307250, 1149 ^ [_307250, _307252, _307254], 1150 ^ [_307250, _307252, _307254]))]]]], input).
% 11.21/11.71 ncf('1',plain,[vvar(1197 ^ []) = vabs(1001 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1002 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1003 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])])],start(250 ^ 0,bind([[_268855, _268857, _268859, _268861], [1003 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1002 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1001 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1197 ^ []]]))).
% 11.21/11.71 ncf('1.1',plain,[-(vvar(1197 ^ []) = vabs(1001 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1002 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1003 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])])), vreduce(vvar(1197 ^ [])) = vsomeExp(1199 ^ []), 998 : -(vsomeExp(1199 ^ []) = vnoExp), 1016 : -(vvar(1197 ^ []) = vapp(vabs(1011 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1012 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1013 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1010 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])])), 1031 : -(vvar(1197 ^ []) = vapp(vabs(1027 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1025 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1029 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1028 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])])), 1048 : -(vvar(1197 ^ []) = vapp(vabs(1042 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1043 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1044 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1046 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])])), 1063 : -(vvar(1197 ^ []) = vapp(1059 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1061 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])])), 1076 : -(vvar(1197 ^ []) = vapp(1073 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1072 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]))],extension(989 ^ 1,bind([[_299939, _299941], [vsomeExp(1199 ^ []), vvar(1197 ^ [])]]))).
% 11.21/11.71 ncf('1.1.1',plain,[-(vreduce(vvar(1197 ^ [])) = vsomeExp(1199 ^ []))],extension(1202 ^ 2)).
% 11.21/11.71 ncf('1.1.2',plain,[vsomeExp(1199 ^ []) = vnoExp, -(vnoExp = vsomeExp(1199 ^ []))],extension(4 ^ 4,bind([[_260242, _260244], [vnoExp, vsomeExp(1199 ^ [])]]))).
% 11.21/11.71 ncf('1.1.2.1',plain,[vnoExp = vsomeExp(1199 ^ [])],extension(833 ^ 5,bind([[_294137], [1199 ^ []]]))).
% 11.21/11.71 ncf('1.1.3',plain,[vvar(1197 ^ []) = vapp(vabs(1011 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1012 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1013 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1010 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), -(vvar(1197 ^ []) = vapp(vabs(1011 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1012 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1013 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1010 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])])), vvar(1197 ^ []) = vvar(1197 ^ [])],extension(10 ^ 4,bind([[_260446, _260448, _260450], [vapp(vabs(1011 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1012 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1013 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1010 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), vvar(1197 ^ []), vvar(1197 ^ [])]]))).
% 11.21/11.71 ncf('1.1.3.1',plain,[vvar(1197 ^ []) = vapp(vabs(1011 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1012 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1013 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1010 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])])],extension(252 ^ 5,bind([[_268972, _268974, _268976], [1010 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], vabs(1011 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1012 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1013 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1197 ^ []]]))).
% 11.21/11.71 ncf('1.1.3.2',plain,[-(vvar(1197 ^ []) = vvar(1197 ^ []))],extension(2 ^ 5,bind([[_260135], [vvar(1197 ^ [])]]))).
% 11.21/11.71 ncf('1.1.4',plain,[vvar(1197 ^ []) = vapp(vabs(1027 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1025 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1029 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1028 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), -(vvar(1197 ^ []) = vapp(vabs(1027 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1025 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1029 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1028 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])])), vvar(1197 ^ []) = vvar(1197 ^ [])],extension(10 ^ 4,bind([[_260446, _260448, _260450], [vapp(vabs(1027 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1025 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1029 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1028 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), vvar(1197 ^ []), vvar(1197 ^ [])]]))).
% 11.21/11.71 ncf('1.1.4.1',plain,[vvar(1197 ^ []) = vapp(vabs(1027 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1025 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1029 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1028 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])])],extension(252 ^ 5,bind([[_268972, _268974, _268976], [1028 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], vabs(1027 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1025 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1029 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1197 ^ []]]))).
% 11.21/11.71 ncf('1.1.4.2',plain,[-(vvar(1197 ^ []) = vvar(1197 ^ []))],extension(2 ^ 5,bind([[_260135], [vvar(1197 ^ [])]]))).
% 11.21/11.71 ncf('1.1.5',plain,[vvar(1197 ^ []) = vapp(vabs(1042 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1043 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1044 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1046 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), -(vvar(1197 ^ []) = vapp(vabs(1042 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1043 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1044 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1046 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])])), vvar(1197 ^ []) = vvar(1197 ^ [])],extension(10 ^ 4,bind([[_260446, _260448, _260450], [vapp(vabs(1042 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1043 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1044 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1046 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), vvar(1197 ^ []), vvar(1197 ^ [])]]))).
% 11.21/11.71 ncf('1.1.5.1',plain,[vvar(1197 ^ []) = vapp(vabs(1042 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1043 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1044 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1046 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])])],extension(252 ^ 5,bind([[_268972, _268974, _268976], [1046 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], vabs(1042 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1043 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1044 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), 1197 ^ []]]))).
% 11.21/11.71 ncf('1.1.5.2',plain,[-(vvar(1197 ^ []) = vvar(1197 ^ []))],extension(2 ^ 5,bind([[_260135], [vvar(1197 ^ [])]]))).
% 11.21/11.71 ncf('1.1.6',plain,[vvar(1197 ^ []) = vapp(1059 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1061 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), -(vvar(1197 ^ []) = vapp(1059 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1061 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])])), vvar(1197 ^ []) = vvar(1197 ^ [])],extension(10 ^ 4,bind([[_260446, _260448, _260450], [vapp(1059 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1061 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), vvar(1197 ^ []), vvar(1197 ^ [])]]))).
% 11.21/11.71 ncf('1.1.6.1',plain,[vvar(1197 ^ []) = vapp(1059 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1061 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])])],extension(252 ^ 5,bind([[_268972, _268974, _268976], [1061 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1059 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1197 ^ []]]))).
% 11.21/11.71 ncf('1.1.6.2',plain,[-(vvar(1197 ^ []) = vvar(1197 ^ []))],extension(2 ^ 5,bind([[_260135], [vvar(1197 ^ [])]]))).
% 11.21/11.71 ncf('1.1.7',plain,[vvar(1197 ^ []) = vapp(1073 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1072 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), -(vvar(1197 ^ []) = vapp(1073 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1072 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])])), vvar(1197 ^ []) = vvar(1197 ^ [])],extension(10 ^ 4,bind([[_260446, _260448, _260450], [vapp(1073 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1072 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])]), vvar(1197 ^ []), vvar(1197 ^ [])]]))).
% 11.21/11.71 ncf('1.1.7.1',plain,[vvar(1197 ^ []) = vapp(1073 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1072 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])])],extension(252 ^ 5,bind([[_268972, _268974, _268976], [1072 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1073 ^ [vsomeExp(1199 ^ []), vvar(1197 ^ [])], 1197 ^ []]]))).
% 11.21/11.71 ncf('1.1.7.2',plain,[-(vvar(1197 ^ []) = vvar(1197 ^ []))],extension(2 ^ 5,bind([[_260135], [vvar(1197 ^ [])]]))).
% 11.21/11.71 %-----------------------------------------------------
% 11.21/11.71 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------