%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : COM147+1 : TPTP v8.1.2. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n016.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 0.36s 1.37s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : COM147+1 : TPTP v8.1.2. Released v6.4.0.
% 0.06/0.13 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n016.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:49:42 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.36/1.37
% 0.36/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.36/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 ncf(matrix, plain, [(1192 ^ _251476) ^ [] : [-(vtcheck(vempty, vabs(1189 ^ [], 1190 ^ [], ve1), 1188 ^ []))], (1194 ^ _251476) ^ [] : [visValue(vabs(1189 ^ [], 1190 ^ [], ve1))], (1196 ^ _251476) ^ [_302308] : [vreduce(vabs(1189 ^ [], 1190 ^ [], ve1)) = vsomeExp(_302308)], (2 ^ _251476) ^ [_251620] : [-(_251620 = _251620)], (4 ^ _251476) ^ [_251727, _251729] : [_251729 = _251727, -(_251727 = _251729)], (10 ^ _251476) ^ [_251931, _251933, _251935] : [-(_251935 = _251931), _251935 = _251933, _251933 = _251931], (20 ^ _251476) ^ [_252244, _252246] : [-(visSomeType(_252244)), _252246 = _252244, visSomeType(_252246)], (30 ^ _251476) ^ [_252539, _252541] : [-(visSomeExp(_252539)), _252541 = _252539, visSomeExp(_252541)], (40 ^ _251476) ^ [_252862, _252864, _252866, _252868] : [-(visFreeVar(_252866, _252862)), visFreeVar(_252868, _252864), _252868 = _252866, _252864 = _252862], (72 ^ _251476) ^ [_253867, _253869] : [-(visValue(_253867)), _253869 = _253867, visValue(_253869)], (54 ^ _251476) ^ [_253334, _253336, _253338, _253340, _253342, _253344] : [-(vtcheck(_253342, _253338, _253334)), vtcheck(_253344, _253340, _253336), _253344 = _253342, _253340 = _253338, _253336 = _253334], (82 ^ _251476) ^ [_254176, _254178] : [_254178 = _254176, -(vgetSomeType(_254178) = vgetSomeType(_254176))], (88 ^ _251476) ^ [_254394, _254396] : [_254396 = _254394, -(vgensym(_254396) = vgensym(_254394))], (94 ^ _251476) ^ [_254668, _254670, _254672, _254674, _254676, _254678] : [-(vsubst(_254678, _254674, _254670) = vsubst(_254676, _254672, _254668)), _254678 = _254676, _254674 = _254672, _254670 = _254668], (108 ^ _251476) ^ [_255128, _255130] : [_255130 = _255128, -(vgetSomeExp(_255130) = vgetSomeExp(_255128))], (114 ^ _251476) ^ [_255346, _255348] : [_255348 = _255346, -(vvar(_255348) = vvar(_255346))], (120 ^ _251476) ^ [_255564, _255566] : [_255566 = _255564, -(vsomeType(_255566) = vsomeType(_255564))], (126 ^ _251476) ^ [_255810, _255812, _255814, _255816] : [-(vapp(_255816, _255812) = vapp(_255814, _255810)), _255816 = _255814, _255812 = _255810], (136 ^ _251476) ^ [_256169, _256171, _256173, _256175] : [-(varrow(_256175, _256171) = varrow(_256173, _256169)), _256175 = _256173, _256171 = _256169], (146 ^ _251476) ^ [_256528, _256530, _256532, _256534] : [-(vlookup(_256534, _256530) = vlookup(_256532, _256528)), _256534 = _256532, _256530 = _256528], (156 ^ _251476) ^ [_256915, _256917, _256919, _256921, _256923, _256925] : [-(vbind(_256925, _256921, _256917) = vbind(_256923, _256919, _256915)), _256925 = _256923, _256921 = _256919, _256917 = _256915], (170 ^ _251476) ^ [_257375, _257377] : [_257377 = _257375, -(vreduce(_257377) = vreduce(_257375))], (190 ^ _251476) ^ [_258089, _258091] : [_258091 = _258089, -(vsomeExp(_258091) = vsomeExp(_258089))], (176 ^ _251476) ^ [_257649, _257651, _257653, _257655, _257657, _257659] : [-(vabs(_257659, _257655, _257651) = vabs(_257657, _257653, _257649)), _257659 = _257657, _257655 = _257653, _257651 = _257649], (1158 ^ _251476) ^ [_300915, _300917, _300919, _300921, _300923] : [-(vtcheck(vbind(_300923, _300921, _300919), _300917, _300915)), vlookup(_300923, _300919) = vnoType, vtcheck(_300919, _300917, _300915)], (1168 ^ _251476) ^ [_301304, _301306, _301308, _301310, _301312] : [-(vtcheck(_301308, _301306, _301304)), -(visFreeVar(_301312, _301306)), vtcheck(vbind(_301312, _301310, _301308), _301306, _301304)], (1178 ^ _251476) ^ [_301614] : [-(vreduce(ve1) = vsomeExp(1185 ^ [_301614])), vtcheck(vempty, ve1, _301614), -(visValue(ve1))], (196 ^ _251476) ^ [_258387, _258389] : [vvar(_258389) = vvar(_258387), -(_258389 = _258387)], (202 ^ _251476) ^ [_258557, _258559] : [_258559 = _258557, -(vvar(_258559) = vvar(_258557))], (208 ^ _251476) ^ [_258853, _258855, _258857, _258859, _258861, _258863] : [vabs(_258863, _258861, _258859) = vabs(_258857, _258855, _258853), 211 ^ _251476 : [(212 ^ _251476) ^ [] : [-(_258863 = _258857)], (214 ^ _251476) ^ [] : [-(_258861 = _258855)], (216 ^ _251476) ^ [] : [-(_258859 = _258853)]]], (218 ^ _251476) ^ [_259220, _259222, _259224, _259226, _259228, _259230] : [-(vabs(_259230, _259228, _259226) = vabs(_259224, _259222, _259220)), _259230 = _259224, _259228 = _259222, _259226 = _259220], (232 ^ _251476) ^ [_259730, _259732, _259734, _259736] : [vapp(_259736, _259734) = vapp(_259732, _259730), 235 ^ _251476 : [(236 ^ _251476) ^ [] : [-(_259736 = _259732)], (238 ^ _251476) ^ [] : [-(_259734 = _259730)]]], (240 ^ _251476) ^ [_259995, _259997, _259999, _260001] : [-(vapp(_260001, _259999) = vapp(_259997, _259995)), _260001 = _259997, _259999 = _259995], (250 ^ _251476) ^ [_260340, _260342, _260344, _260346] : [vvar(_260346) = vabs(_260344, _260342, _260340)], (252 ^ _251476) ^ [_260457, _260459, _260461] : [vvar(_260461) = vapp(_260459, _260457)], (254 ^ _251476) ^ [_260599, _260601, _260603, _260605, _260607] : [vabs(_260607, _260605, _260603) = vapp(_260601, _260599)], (256 ^ _251476) ^ [_260749, _260751, _260753, _260755] : [_260749 = vabs(_260755, _260753, _260751), -(visValue(_260749))], (262 ^ _251476) ^ [_260977, _260979] : [_260977 = vvar(_260979), visValue(_260977)], (268 ^ _251476) ^ [_261204, _261206, _261208] : [_261204 = vapp(_261208, _261206), visValue(_261204)], (274 ^ _251476) ^ [_261453, _261455, _261457, _261459] : [_261459 = _261453, _261457 = vvar(_261455), 281 ^ _251476 : [(282 ^ _251476) ^ [] : [_261455 = _261453, -(visFreeVar(_261459, _261457))], (288 ^ _251476) ^ [] : [visFreeVar(_261459, _261457), -(_261455 = _261453)]]], (294 ^ _251476) ^ [_262107, _262109, _262111, _262113, _262115, _262117] : [_262115 = _262109, _262113 = vabs(_262111, _262117, _262107), 301 ^ _251476 : [(312 ^ _251476) ^ [] : [visFreeVar(_262115, _262113), 315 ^ _251476 : [(316 ^ _251476) ^ [] : [_262111 = _262109], (318 ^ _251476) ^ [] : [-(visFreeVar(_262109, _262107))]]], (302 ^ _251476) ^ [] : [-(visFreeVar(_262115, _262113)), -(_262111 = _262109), visFreeVar(_262109, _262107)]]], (320 ^ _251476) ^ [_262983, _262985, _262987, _262989, _262991] : [_262991 = _262985, _262989 = vapp(_262987, _262983), 327 ^ _251476 : [(328 ^ _251476) ^ [] : [329 ^ _251476 : [(330 ^ _251476) ^ [] : [visFreeVar(_262985, _262987)], (332 ^ _251476) ^ [] : [visFreeVar(_262985, _262983)]], -(visFreeVar(_262991, _262989))], (336 ^ _251476) ^ [] : [visFreeVar(_262991, _262989), -(visFreeVar(_262985, _262987)), -(visFreeVar(_262985, _262983))]]], (356 ^ _251476) ^ [] : [357 ^ _251476 : [(358 ^ _251476) ^ [] : [-(true___)], (360 ^ _251476) ^ [] : [true___]], -(vempty = vempty)], (346 ^ _251476) ^ [] : [vempty = vempty, true___, -(true___)], (364 ^ _251476) ^ [_264223, _264225, _264227, _264229, _264231, _264233] : [vbind(_264233, _264231, _264229) = vbind(_264227, _264225, _264223), 367 ^ _251476 : [(368 ^ _251476) ^ [] : [-(_264233 = _264227)], (370 ^ _251476) ^ [] : [-(_264231 = _264225)], (372 ^ _251476) ^ [] : [-(_264229 = _264223)]]], (374 ^ _251476) ^ [_264590, _264592, _264594, _264596, _264598, _264600] : [-(vbind(_264600, _264598, _264596) = vbind(_264594, _264592, _264590)), _264600 = _264594, _264598 = _264592, _264596 = _264590], (398 ^ _251476) ^ [] : [399 ^ _251476 : [(400 ^ _251476) ^ [] : [-(true___)], (402 ^ _251476) ^ [] : [true___]], -(vnoType = vnoType)], (388 ^ _251476) ^ [] : [vnoType = vnoType, true___, -(true___)], (406 ^ _251476) ^ [_265434, _265436] : [vsomeType(_265436) = vsomeType(_265434), -(_265436 = _265434)], (412 ^ _251476) ^ [_265604, _265606] : [_265606 = _265604, -(vsomeType(_265606) = vsomeType(_265604))], (418 ^ _251476) ^ [_265822, _265824, _265826] : [vempty = vbind(_265826, _265824, _265822)], (420 ^ _251476) ^ [_265907] : [vnoType = vsomeType(_265907)], (422 ^ _251476) ^ [_266002] : [_266002 = vnoType, visSomeType(_266002)], (428 ^ _251476) ^ [_266205, _266207] : [_266205 = vsomeType(_266207), -(visSomeType(_266205))], (434 ^ _251476) ^ [_266431, _266433, _266435] : [_266435 = vsomeType(_266431), _266433 = vgetSomeType(_266435), -(_266433 = _266431)], (444 ^ _251476) ^ [_266776, _266778, _266780, _266782] : [_266780 = _266782, _266778 = vempty, _266776 = vlookup(_266780, _266778), -(_266776 = vnoType)], (458 ^ _251476) ^ [_267270, _267272, _267274, _267276, _267278, _267280, _267282] : [_267276 = _267280, _267274 = vbind(_267278, _267270, _267282), _267280 = _267278, _267272 = vlookup(_267276, _267274), -(_267272 = vsomeType(_267270))], (476 ^ _251476) ^ [_267927, _267929, _267931, _267933, _267935, _267937, _267939] : [_267935 = _267929, _267933 = vbind(_267937, _267939, _267927), -(_267929 = _267937), _267931 = vlookup(_267935, _267933), -(_267931 = vlookup(_267929, _267927))], (494 ^ _251476) ^ [_268533, _268535, _268537] : [vlookup(_268537, _268535) = _268533, 500 ^ _251476 : [(501 ^ _251476) ^ [] : [-(_268537 = 499 ^ [_268533, _268535, _268537])], (503 ^ _251476) ^ [] : [-(_268535 = vempty)], (505 ^ _251476) ^ [] : [-(_268533 = vnoType)]], 512 ^ _251476 : [(513 ^ _251476) ^ [] : [-(_268537 = 509 ^ [_268533, _268535, _268537])], (515 ^ _251476) ^ [] : [-(_268535 = vbind(510 ^ [_268533, _268535, _268537], 511 ^ [_268533, _268535, _268537], 508 ^ [_268533, _268535, _268537]))], (517 ^ _251476) ^ [] : [-(509 ^ [_268533, _268535, _268537] = 510 ^ [_268533, _268535, _268537])], (519 ^ _251476) ^ [] : [-(_268533 = vsomeType(511 ^ [_268533, _268535, _268537]))]], 524 ^ _251476 : [(525 ^ _251476) ^ [] : [-(_268537 = 522 ^ [_268533, _268535, _268537])], (527 ^ _251476) ^ [] : [-(_268535 = vbind(521 ^ [_268533, _268535, _268537], 520 ^ [_268533, _268535, _268537], 523 ^ [_268533, _268535, _268537]))], (529 ^ _251476) ^ [] : [522 ^ [_268533, _268535, _268537] = 521 ^ [_268533, _268535, _268537]], (531 ^ _251476) ^ [] : [-(_268533 = vlookup(522 ^ [_268533, _268535, _268537], 523 ^ [_268533, _268535, _268537]))]]], (533 ^ _251476) ^ [_270728, _270730, _270732, _270734, _270736, _270738, _270740] : [-(vtcheck(vbind(_270736, _270734, _270732), _270730, _270728)), _270736 = _270740, vtcheck(vbind(_270736, _270734, vbind(_270740, _270738, _270732)), _270730, _270728)], (543 ^ _251476) ^ [_271175, _271177, _271179, _271181, _271183, _271185, _271187] : [-(vtcheck(vbind(_271187, _271185, vbind(_271183, _271181, _271179)), _271177, _271175)), -(_271183 = _271187), vtcheck(vbind(_271183, _271181, vbind(_271187, _271185, _271179)), _271177, _271175)], (553 ^ _251476) ^ [_271563, _271565] : [vgensym(_271563) = _271565, visFreeVar(_271565, _271563)], (559 ^ _251476) ^ [_271848, _271850, _271852, _271854, _271856, _271858, _271860] : [_271856 = _271860, _271854 = _271848, _271852 = vvar(_271858), _271860 = _271858, _271850 = vsubst(_271856, _271854, _271852), -(_271850 = _271848)], (581 ^ _251476) ^ [_272610, _272612, _272614, _272616, _272618, _272620, _272622] : [_272618 = _272620, _272616 = _272622, _272614 = vvar(_272610), -(_272620 = _272610), _272612 = vsubst(_272618, _272616, _272614), -(_272612 = vvar(_272610))], (603 ^ _251476) ^ [_273393, _273395, _273397, _273399, _273401, _273403, _273405, _273407] : [_273401 = vsubst(_273407, _273405, _273403), -(_273401 = vapp(vsubst(_273397, _273395, _273399), vsubst(_273397, _273395, _273393))), _273407 = _273397, _273405 = _273395, _273403 = vapp(_273399, _273393)], (621 ^ _251476) ^ [_274114, _274116, _274118, _274120, _274122, _274124, _274126, _274128, _274130] : [_274126 = _274128, _274124 = _274130, _274122 = vabs(_274118, _274116, _274114), _274128 = _274118, _274120 = vsubst(_274126, _274124, _274122), -(_274120 = vabs(_274118, _274116, _274114))], (643 ^ _251476) ^ [_274974, _274976, _274978, _274980, _274982, _274984, _274986, _274988, _274990, _274992] : [_274992 = _274984, _274990 = _274982, _274988 = vabs(_274978, _274980, _274974), _274986 = vsubst(_274992, _274990, _274988), -(_274986 = vsubst(_274984, _274982, vabs(_274976, _274980, vsubst(_274978, vvar(_274976), _274974)))), -(_274984 = _274978), visFreeVar(_274978, _274982), _274976 = vgensym(vapp(vapp(_274982, _274974), vvar(_274984)))], (673 ^ _251476) ^ [_276129, _276131, _276133, _276135, _276137, _276139, _276141, _276143, _276145] : [_276145 = _276133, _276143 = _276131, _276141 = vabs(_276137, _276135, _276129), -(_276133 = _276137), -(visFreeVar(_276137, _276131)), _276139 = vsubst(_276145, _276143, _276141), -(_276139 = vabs(_276137, _276135, vsubst(_276133, _276131, _276129)))], (699 ^ _251476) ^ [_277038, _277040, _277042, _277044] : [vsubst(_277044, _277042, _277040) = _277038, 707 ^ _251476 : [(708 ^ _251476) ^ [] : [-(_277044 = 704 ^ [_277038, _277040, _277042, _277044])], (710 ^ _251476) ^ [] : [-(_277042 = 706 ^ [_277038, _277040, _277042, _277044])], (712 ^ _251476) ^ [] : [-(_277040 = vvar(705 ^ [_277038, _277040, _277042, _277044]))], (714 ^ _251476) ^ [] : [-(704 ^ [_277038, _277040, _277042, _277044] = 705 ^ [_277038, _277040, _277042, _277044])], (716 ^ _251476) ^ [] : [-(_277038 = 706 ^ [_277038, _277040, _277042, _277044])]], 722 ^ _251476 : [(723 ^ _251476) ^ [] : [-(_277044 = 720 ^ [_277038, _277040, _277042, _277044])], (725 ^ _251476) ^ [] : [-(_277042 = 719 ^ [_277038, _277040, _277042, _277044])], (727 ^ _251476) ^ [] : [-(_277040 = vvar(721 ^ [_277038, _277040, _277042, _277044]))], (729 ^ _251476) ^ [] : [720 ^ [_277038, _277040, _277042, _277044] = 721 ^ [_277038, _277040, _277042, _277044]], (731 ^ _251476) ^ [] : [-(_277038 = vvar(721 ^ [_277038, _277040, _277042, _277044]))]], 738 ^ _251476 : [(739 ^ _251476) ^ [] : [-(_277044 = 735 ^ [_277038, _277040, _277042, _277044])], (741 ^ _251476) ^ [] : [-(_277042 = 736 ^ [_277038, _277040, _277042, _277044])], (743 ^ _251476) ^ [] : [-(_277040 = vapp(734 ^ [_277038, _277040, _277042, _277044], 737 ^ [_277038, _277040, _277042, _277044]))], (745 ^ _251476) ^ [] : [-(_277038 = vapp(vsubst(735 ^ [_277038, _277040, _277042, _277044], 736 ^ [_277038, _277040, _277042, _277044], 734 ^ [_277038, _277040, _277042, _277044]), vsubst(735 ^ [_277038, _277040, _277042, _277044], 736 ^ [_277038, _277040, _277042, _277044], 737 ^ [_277038, _277040, _277042, _277044])))]], 753 ^ _251476 : [(754 ^ _251476) ^ [] : [-(_277044 = 749 ^ [_277038, _277040, _277042, _277044])], (756 ^ _251476) ^ [] : [-(_277042 = 748 ^ [_277038, _277040, _277042, _277044])], (758 ^ _251476) ^ [] : [-(_277040 = vabs(750 ^ [_277038, _277040, _277042, _277044], 751 ^ [_277038, _277040, _277042, _277044], 752 ^ [_277038, _277040, _277042, _277044]))], (760 ^ _251476) ^ [] : [-(749 ^ [_277038, _277040, _277042, _277044] = 750 ^ [_277038, _277040, _277042, _277044])], (762 ^ _251476) ^ [] : [-(_277038 = vabs(750 ^ [_277038, _277040, _277042, _277044], 751 ^ [_277038, _277040, _277042, _277044], 752 ^ [_277038, _277040, _277042, _277044]))]], 771 ^ _251476 : [(772 ^ _251476) ^ [] : [-(_277044 = 765 ^ [_277038, _277040, _277042, _277044])], (774 ^ _251476) ^ [] : [-(_277042 = 766 ^ [_277038, _277040, _277042, _277044])], (776 ^ _251476) ^ [] : [-(_277040 = vabs(768 ^ [_277038, _277040, _277042, _277044], 767 ^ [_277038, _277040, _277042, _277044], 770 ^ [_277038, _277040, _277042, _277044]))], (778 ^ _251476) ^ [] : [765 ^ [_277038, _277040, _277042, _277044] = 768 ^ [_277038, _277040, _277042, _277044]], (780 ^ _251476) ^ [] : [-(visFreeVar(768 ^ [_277038, _277040, _277042, _277044], 766 ^ [_277038, _277040, _277042, _277044]))], (782 ^ _251476) ^ [] : [-(769 ^ [_277038, _277040, _277042, _277044] = vgensym(vapp(vapp(766 ^ [_277038, _277040, _277042, _277044], 770 ^ [_277038, _277040, _277042, _277044]), vvar(765 ^ [_277038, _277040, _277042, _277044]))))], (784 ^ _251476) ^ [] : [-(_277038 = vsubst(765 ^ [_277038, _277040, _277042, _277044], 766 ^ [_277038, _277040, _277042, _277044], vabs(769 ^ [_277038, _277040, _277042, _277044], 767 ^ [_277038, _277040, _277042, _277044], vsubst(768 ^ [_277038, _277040, _277042, _277044], vvar(769 ^ [_277038, _277040, _277042, _277044]), 770 ^ [_277038, _277040, _277042, _277044]))))]], 790 ^ _251476 : [(791 ^ _251476) ^ [] : [-(_277044 = 787 ^ [_277038, _277040, _277042, _277044])], (793 ^ _251476) ^ [] : [-(_277042 = 788 ^ [_277038, _277040, _277042, _277044])], (795 ^ _251476) ^ [] : [-(_277040 = vabs(785 ^ [_277038, _277040, _277042, _277044], 786 ^ [_277038, _277040, _277042, _277044], 789 ^ [_277038, _277040, _277042, _277044]))], (797 ^ _251476) ^ [] : [787 ^ [_277038, _277040, _277042, _277044] = 785 ^ [_277038, _277040, _277042, _277044]], (799 ^ _251476) ^ [] : [visFreeVar(785 ^ [_277038, _277040, _277042, _277044], 788 ^ [_277038, _277040, _277042, _277044])], (801 ^ _251476) ^ [] : [-(_277038 = vabs(785 ^ [_277038, _277040, _277042, _277044], 786 ^ [_277038, _277040, _277042, _277044], vsubst(787 ^ [_277038, _277040, _277042, _277044], 788 ^ [_277038, _277040, _277042, _277044], 789 ^ [_277038, _277040, _277042, _277044])))]]], (813 ^ _251476) ^ [] : [814 ^ _251476 : [(815 ^ _251476) ^ [] : [-(true___)], (817 ^ _251476) ^ [] : [true___]], -(vnoExp = vnoExp)], (803 ^ _251476) ^ [] : [vnoExp = vnoExp, true___, -(true___)], (821 ^ _251476) ^ [_285262, _285264] : [vsomeExp(_285264) = vsomeExp(_285262), -(_285264 = _285262)], (827 ^ _251476) ^ [_285432, _285434] : [_285434 = _285432, -(vsomeExp(_285434) = vsomeExp(_285432))], (833 ^ _251476) ^ [_285622] : [vnoExp = vsomeExp(_285622)], (835 ^ _251476) ^ [_285717] : [_285717 = vnoExp, visSomeExp(_285717)], (841 ^ _251476) ^ [_285920, _285922] : [_285920 = vsomeExp(_285922), -(visSomeExp(_285920))], (847 ^ _251476) ^ [_286146, _286148, _286150] : [_286150 = vsomeExp(_286146), _286148 = vgetSomeExp(_286150), -(_286148 = _286146)], (857 ^ _251476) ^ [_286477, _286479, _286481] : [_286479 = vvar(_286481), _286477 = vreduce(_286479), -(_286477 = vnoExp)], (867 ^ _251476) ^ [_286836, _286838, _286840, _286842, _286844] : [_286838 = vabs(_286844, _286842, _286840), _286836 = vreduce(_286838), -(_286836 = vnoExp)], (877 ^ _251476) ^ [_287247, _287249, _287251, _287253, _287255, _287257, _287259] : [_287257 = vapp(vabs(_287253, _287251, _287249), _287259), _287247 = vreduce(_287259), visSomeExp(_287247), _287255 = vreduce(_287257), -(_287255 = vsomeExp(vapp(vabs(_287253, _287251, _287249), vgetSomeExp(_287247))))], (895 ^ _251476) ^ [_287928, _287930, _287932, _287934, _287936, _287938, _287940] : [_287936 = vapp(vabs(_287932, _287940, _287928), _287930), _287934 = vreduce(_287936), -(_287934 = vsomeExp(vsubst(_287932, _287930, _287928))), _287938 = vreduce(_287930), -(visSomeExp(_287938)), visValue(_287930)], (917 ^ _251476) ^ [_288709, _288711, _288713, _288715, _288717, _288719, _288721] : [_288711 = vapp(vabs(_288721, _288719, _288717), _288713), _288709 = vreduce(_288711), -(_288709 = vnoExp), _288715 = vreduce(_288713), -(visSomeExp(_288715)), -(visValue(_288713))], (939 ^ _251476) ^ [_289453, _289455, _289457, _289459, _289461] : [_289459 = vapp(_289461, _289453), -(_289461 = vabs(944 ^ [_289453, _289455, _289457, _289459, _289461], 945 ^ [_289453, _289455, _289457, _289459, _289461], 946 ^ [_289453, _289455, _289457, _289459, _289461])), _289455 = vreduce(_289461), visSomeExp(_289455), _289457 = vreduce(_289459), -(_289457 = vsomeExp(vapp(vgetSomeExp(_289455), _289453)))], (964 ^ _251476) ^ [_290465, _290467, _290469, _290471, _290473] : [_290467 = vapp(_290471, _290473), -(_290471 = vabs(969 ^ [_290465, _290467, _290469, _290471, _290473], 970 ^ [_290465, _290467, _290469, _290471, _290473], 971 ^ [_290465, _290467, _290469, _290471, _290473])), _290469 = vreduce(_290471), -(visSomeExp(_290469)), _290465 = vreduce(_290467), -(_290465 = vnoExp)], (989 ^ _251476) ^ [_291424, _291426] : [vreduce(_291426) = _291424, 995 ^ _251476 : [(996 ^ _251476) ^ [] : [-(_291426 = vvar(994 ^ [_291424, _291426]))], (998 ^ _251476) ^ [] : [-(_291424 = vnoExp)]], 1004 ^ _251476 : [(1005 ^ _251476) ^ [] : [-(_291426 = vabs(1001 ^ [_291424, _291426], 1002 ^ [_291424, _291426], 1003 ^ [_291424, _291426]))], (1007 ^ _251476) ^ [] : [-(_291424 = vnoExp)]], 1015 ^ _251476 : [(1016 ^ _251476) ^ [] : [-(_291426 = vapp(vabs(1011 ^ [_291424, _291426], 1012 ^ [_291424, _291426], 1013 ^ [_291424, _291426]), 1010 ^ [_291424, _291426]))], (1018 ^ _251476) ^ [] : [-(1014 ^ [_291424, _291426] = vreduce(1010 ^ [_291424, _291426]))], (1020 ^ _251476) ^ [] : [-(visSomeExp(1014 ^ [_291424, _291426]))], (1022 ^ _251476) ^ [] : [-(_291424 = vsomeExp(vapp(vabs(1011 ^ [_291424, _291426], 1012 ^ [_291424, _291426], 1013 ^ [_291424, _291426]), vgetSomeExp(1014 ^ [_291424, _291426]))))]], 1030 ^ _251476 : [(1031 ^ _251476) ^ [] : [-(_291426 = vapp(vabs(1027 ^ [_291424, _291426], 1025 ^ [_291424, _291426], 1029 ^ [_291424, _291426]), 1028 ^ [_291424, _291426]))], (1033 ^ _251476) ^ [] : [-(1026 ^ [_291424, _291426] = vreduce(1028 ^ [_291424, _291426]))], (1035 ^ _251476) ^ [] : [visSomeExp(1026 ^ [_291424, _291426])], (1037 ^ _251476) ^ [] : [-(visValue(1028 ^ [_291424, _291426]))], (1039 ^ _251476) ^ [] : [-(_291424 = vsomeExp(vsubst(1027 ^ [_291424, _291426], 1028 ^ [_291424, _291426], 1029 ^ [_291424, _291426])))]], 1047 ^ _251476 : [(1048 ^ _251476) ^ [] : [-(_291426 = vapp(vabs(1042 ^ [_291424, _291426], 1043 ^ [_291424, _291426], 1044 ^ [_291424, _291426]), 1046 ^ [_291424, _291426]))], (1050 ^ _251476) ^ [] : [-(1045 ^ [_291424, _291426] = vreduce(1046 ^ [_291424, _291426]))], (1052 ^ _251476) ^ [] : [visSomeExp(1045 ^ [_291424, _291426])], (1054 ^ _251476) ^ [] : [visValue(1046 ^ [_291424, _291426])], (1056 ^ _251476) ^ [] : [-(_291424 = vnoExp)]], 1062 ^ _251476 : [(1063 ^ _251476) ^ [] : [-(_291426 = vapp(1059 ^ [_291424, _291426], 1061 ^ [_291424, _291426]))], (1065 ^ _251476) ^ [_296022, _296024, _296026] : [1059 ^ [_291424, _291426] = vabs(_296026, _296024, _296022)], (1067 ^ _251476) ^ [] : [-(1060 ^ [_291424, _291426] = vreduce(1059 ^ [_291424, _291426]))], (1069 ^ _251476) ^ [] : [-(visSomeExp(1060 ^ [_291424, _291426]))], (1071 ^ _251476) ^ [] : [-(_291424 = vsomeExp(vapp(vgetSomeExp(1060 ^ [_291424, _291426]), 1061 ^ [_291424, _291426])))]], 1075 ^ _251476 : [(1076 ^ _251476) ^ [] : [-(_291426 = vapp(1073 ^ [_291424, _291426], 1072 ^ [_291424, _291426]))], (1078 ^ _251476) ^ [_296796, _296798, _296800] : [1073 ^ [_291424, _291426] = vabs(_296800, _296798, _296796)], (1080 ^ _251476) ^ [] : [-(1074 ^ [_291424, _291426] = vreduce(1073 ^ [_291424, _291426]))], (1082 ^ _251476) ^ [] : [visSomeExp(1074 ^ [_291424, _291426])], (1084 ^ _251476) ^ [] : [-(_291424 = vnoExp)]]], (1086 ^ _251476) ^ [_297212, _297214, _297216, _297218] : [varrow(_297218, _297216) = varrow(_297214, _297212), 1089 ^ _251476 : [(1090 ^ _251476) ^ [] : [-(_297218 = _297214)], (1092 ^ _251476) ^ [] : [-(_297216 = _297212)]]], (1094 ^ _251476) ^ [_297477, _297479, _297481, _297483] : [-(varrow(_297483, _297481) = varrow(_297479, _297477)), _297483 = _297479, _297481 = _297477], (1104 ^ _251476) ^ [_297824, _297826, _297828] : [vlookup(_297826, _297828) = vsomeType(_297824), -(vtcheck(_297828, vvar(_297826), _297824))], (1110 ^ _251476) ^ [_298098, _298100, _298102, _298104, _298106] : [vtcheck(vbind(_298104, _298100, _298106), _298102, _298098), -(vtcheck(_298106, vabs(_298104, _298100, _298102), varrow(_298100, _298098)))], (1116 ^ _251476) ^ [_298394, _298396, _298398, _298400, _298402] : [-(vtcheck(_298400, vapp(_298398, _298396), _298394)), vtcheck(_298400, _298398, varrow(_298402, _298394)), vtcheck(_298400, _298396, _298402)], (1126 ^ _251476) ^ [_298735, _298737, _298739] : [vtcheck(_298735, _298739, _298737), 1132 ^ _251476 : [(1133 ^ _251476) ^ [] : [-(_298739 = vvar(1131 ^ [_298735, _298737, _298739]))], (1135 ^ _251476) ^ [] : [-(vlookup(1131 ^ [_298735, _298737, _298739], _298735) = vsomeType(_298737))]], 1142 ^ _251476 : [(1143 ^ _251476) ^ [] : [-(_298739 = vabs(1138 ^ [_298735, _298737, _298739], 1140 ^ [_298735, _298737, _298739], 1139 ^ [_298735, _298737, _298739]))], (1145 ^ _251476) ^ [] : [-(_298737 = varrow(1140 ^ [_298735, _298737, _298739], 1141 ^ [_298735, _298737, _298739]))], (1147 ^ _251476) ^ [] : [-(vtcheck(vbind(1138 ^ [_298735, _298737, _298739], 1140 ^ [_298735, _298737, _298739], _298735), 1139 ^ [_298735, _298737, _298739], 1141 ^ [_298735, _298737, _298739]))]], 1151 ^ _251476 : [(1152 ^ _251476) ^ [] : [-(_298739 = vapp(1148 ^ [_298735, _298737, _298739], 1149 ^ [_298735, _298737, _298739]))], (1154 ^ _251476) ^ [] : [-(vtcheck(_298735, 1148 ^ [_298735, _298737, _298739], varrow(1150 ^ [_298735, _298737, _298739], _298737)))], (1156 ^ _251476) ^ [] : [-(vtcheck(_298735, 1149 ^ [_298735, _298737, _298739], 1150 ^ [_298735, _298737, _298739]))]]]], input).
% 0.36/1.37 ncf('1',plain,[visValue(vabs(1189 ^ [], 1190 ^ [], ve1))],start(1194 ^ 0)).
% 0.36/1.37 ncf('1.1',plain,[-(visValue(vabs(1189 ^ [], 1190 ^ [], ve1))), vabs(1189 ^ [], 1190 ^ [], ve1) = vabs(1189 ^ [], 1190 ^ [], ve1)],extension(256 ^ 1,bind([[_260749, _260751, _260753, _260755], [vabs(1189 ^ [], 1190 ^ [], ve1), ve1, 1190 ^ [], 1189 ^ []]]))).
% 0.36/1.37 ncf('1.1.1',plain,[-(vabs(1189 ^ [], 1190 ^ [], ve1) = vabs(1189 ^ [], 1190 ^ [], ve1))],extension(2 ^ 2,bind([[_251620], [vabs(1189 ^ [], 1190 ^ [], ve1)]]))).
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------