%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : COM128+1 : TPTP v8.1.2. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n014.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:43 EDT 2023
% Result : Theorem 87.79s 84.51s
% Output : Proof 87.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : COM128+1 : TPTP v8.1.2. Released v6.4.0.
% 0.06/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n014.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Fri May 19 03:13:57 EDT 2023
% 0.13/0.34 % CPUTime :
% 87.79/84.51
% 87.79/84.51 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 87.79/84.51 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 87.79/84.51 %-----------------------------------------------------
% 87.79/84.51 ncf(matrix, plain, [(1270 ^ _335884) ^ [] : [-(1265 ^ [] = 1266 ^ [])], (1268 ^ _335884) ^ [] : [-(1266 ^ [] = vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))))], !, (617 ^ _282358) ^ [_304735, _304737, _304739, _304741, _304743, _304745, _304747, _304749] : [_304743 = vsubst(_304749, _304747, _304745), -(_304743 = vapp(vsubst(_304739, _304737, _304741), vsubst(_304739, _304737, _304735))), _304749 = _304739, _304747 = _304737, _304745 = vapp(_304741, _304735)], (687 ^ _282358) ^ [_307471, _307473, _307475, _307477, _307479, _307481, _307483, _307485, _307487] : [_307487 = _307475, _307485 = _307473, _307483 = vabs(_307479, _307477, _307471), -(_307475 = _307479), -(visFreeVar(_307479, _307473)), _307481 = vsubst(_307487, _307485, _307483), -(_307481 = vabs(_307479, _307477, vsubst(_307475, _307473, _307471)))], (50 ^ _282358) ^ [_284019, _284021, _284023, _284025] : [-(valphaEquivalent(_284023, _284019)), valphaEquivalent(_284025, _284021), _284025 = _284023, _284021 = _284019], (246 ^ _282358) ^ [_291072, _291074, _291076, _291078] : [vapp(_291078, _291076) = vapp(_291074, _291072), 249 ^ _282358 : [(252 ^ _282358) ^ [] : [-(_291076 = _291072)], (250 ^ _282358) ^ [] : [-(_291078 = _291074)]]], (861 ^ _282358) ^ [_317488, _317490, _317492] : [_317492 = vsomeExp(_317488), _317490 = vgetSomeExp(_317492), -(_317490 = _317488)], (412 ^ _282358) ^ [] : [413 ^ _282358 : [(416 ^ _282358) ^ [] : [true___], (414 ^ _282358) ^ [] : [-(true___)]], -(vnoType = vnoType)], (388 ^ _282358) ^ [_295932, _295934, _295936, _295938, _295940, _295942] : [-(vbind(_295942, _295940, _295938) = vbind(_295936, _295934, _295932)), _295942 = _295936, _295940 = _295934, _295938 = _295932], (114 ^ _282358) ^ [_286138, _286140] : [_286140 = _286138, -(vreduce(_286140) = vreduce(_286138))], (547 ^ _282358) ^ [_302070, _302072, _302074, _302076, _302078, _302080, _302082] : [-(vtcheck(vbind(_302078, _302076, _302074), _302072, _302070)), _302078 = _302082, vtcheck(vbind(_302078, _302076, vbind(_302082, _302080, _302074)), _302072, _302070)], (1140 ^ _282358) ^ [_330077, _330079, _330081] : [vtcheck(_330077, _330081, _330079), 1146 ^ _282358 : [(1149 ^ _282358) ^ [] : [-(vlookup(1145 ^ [_330077, _330079, _330081], _330077) = vsomeType(_330079))], (1147 ^ _282358) ^ [] : [-(_330081 = vvar(1145 ^ [_330077, _330079, _330081]))]], 1156 ^ _282358 : [(1161 ^ _282358) ^ [] : [-(vtcheck(vbind(1152 ^ [_330077, _330079, _330081], 1154 ^ [_330077, _330079, _330081], _330077), 1153 ^ [_330077, _330079, _330081], 1155 ^ [_330077, _330079, _330081]))], (1159 ^ _282358) ^ [] : [-(_330079 = varrow(1154 ^ [_330077, _330079, _330081], 1155 ^ [_330077, _330079, _330081]))], (1157 ^ _282358) ^ [] : [-(_330081 = vabs(1152 ^ [_330077, _330079, _330081], 1154 ^ [_330077, _330079, _330081], 1153 ^ [_330077, _330079, _330081]))]], 1165 ^ _282358 : [(1170 ^ _282358) ^ [] : [-(vtcheck(_330077, 1163 ^ [_330077, _330079, _330081], 1164 ^ [_330077, _330079, _330081]))], (1168 ^ _282358) ^ [] : [-(vtcheck(_330077, 1162 ^ [_330077, _330079, _330081], varrow(1164 ^ [_330077, _330079, _330081], _330079)))], (1166 ^ _282358) ^ [] : [-(_330081 = vapp(1162 ^ [_330077, _330079, _330081], 1163 ^ [_330077, _330079, _330081]))]]], (204 ^ _282358) ^ [_289397, _289399] : [_289399 = _289397, -(vvar(_289399) = vvar(_289397))], (490 ^ _282358) ^ [_299269, _299271, _299273, _299275, _299277, _299279, _299281] : [_299277 = _299271, _299275 = vbind(_299279, _299281, _299269), -(_299271 = _299279), _299273 = vlookup(_299277, _299275), -(_299273 = vlookup(_299271, _299269))], (472 ^ _282358) ^ [_298612, _298614, _298616, _298618, _298620, _298622, _298624] : [_298618 = _298622, _298616 = vbind(_298620, _298612, _298624), _298622 = _298620, _298614 = vlookup(_298618, _298616), -(_298614 = vsomeType(_298612))], (308 ^ _282358) ^ [_293449, _293451, _293453, _293455, _293457, _293459] : [_293457 = _293451, _293455 = vabs(_293453, _293459, _293449), 315 ^ _282358 : [(316 ^ _282358) ^ [] : [-(visFreeVar(_293457, _293455)), -(_293453 = _293451), visFreeVar(_293451, _293449)], (326 ^ _282358) ^ [] : [visFreeVar(_293457, _293455), 329 ^ _282358 : [(332 ^ _282358) ^ [] : [-(visFreeVar(_293451, _293449))], (330 ^ _282358) ^ [] : [_293453 = _293451]]]]], (1174 ^ _282358) ^ [_332313, _332315] : [valphaEquivalent(_332313, _332315), -(valphaEquivalent(_332315, _332313))], (96 ^ _282358) ^ [_285484, _285486] : [_285486 = _285484, -(vgetSomeType(_285486) = vgetSomeType(_285484))], (268 ^ _282358) ^ [_291941, _291943, _291945, _291947, _291949] : [vabs(_291949, _291947, _291945) = vapp(_291943, _291941)], (78 ^ _282358) ^ [_284915, _284917, _284919, _284921, _284923, _284925] : [-(vtcheck(_284923, _284919, _284915)), vtcheck(_284925, _284921, _284917), _284925 = _284923, _284921 = _284919, _284917 = _284915], (64 ^ _282358) ^ [_284463, _284465, _284467, _284469] : [-(visFreeVar(_284467, _284463)), visFreeVar(_284469, _284465), _284469 = _284467, _284465 = _284463], (841 ^ _282358) ^ [_316774, _316776] : [_316776 = _316774, -(vsomeExp(_316776) = vsomeExp(_316774))], (1226 ^ _282358) ^ [_334226, _334228, _334230, _334232, _334234] : [-(vtcheck(_334230, _334228, _334226)), -(visFreeVar(_334234, _334228)), vtcheck(vbind(_334234, _334232, _334230), _334228, _334226)], (1003 ^ _282358) ^ [_322766, _322768] : [vreduce(_322768) = _322766, 1009 ^ _282358 : [(1012 ^ _282358) ^ [] : [-(_322766 = vnoExp)], (1010 ^ _282358) ^ [] : [-(_322768 = vvar(1008 ^ [_322766, _322768]))]], 1018 ^ _282358 : [(1021 ^ _282358) ^ [] : [-(_322766 = vnoExp)], (1019 ^ _282358) ^ [] : [-(_322768 = vabs(1015 ^ [_322766, _322768], 1016 ^ [_322766, _322768], 1017 ^ [_322766, _322768]))]], 1029 ^ _282358 : [(1032 ^ _282358) ^ [] : [-(1028 ^ [_322766, _322768] = vreduce(1024 ^ [_322766, _322768]))], (1034 ^ _282358) ^ [] : [-(visSomeExp(1028 ^ [_322766, _322768]))], (1036 ^ _282358) ^ [] : [-(_322766 = vsomeExp(vapp(vabs(1025 ^ [_322766, _322768], 1026 ^ [_322766, _322768], 1027 ^ [_322766, _322768]), vgetSomeExp(1028 ^ [_322766, _322768]))))], (1030 ^ _282358) ^ [] : [-(_322768 = vapp(vabs(1025 ^ [_322766, _322768], 1026 ^ [_322766, _322768], 1027 ^ [_322766, _322768]), 1024 ^ [_322766, _322768]))]], 1044 ^ _282358 : [(1045 ^ _282358) ^ [] : [-(_322768 = vapp(vabs(1041 ^ [_322766, _322768], 1039 ^ [_322766, _322768], 1043 ^ [_322766, _322768]), 1042 ^ [_322766, _322768]))], (1049 ^ _282358) ^ [] : [visSomeExp(1040 ^ [_322766, _322768])], (1053 ^ _282358) ^ [] : [-(_322766 = vsomeExp(vsubst(1041 ^ [_322766, _322768], 1042 ^ [_322766, _322768], 1043 ^ [_322766, _322768])))], (1051 ^ _282358) ^ [] : [-(visValue(1042 ^ [_322766, _322768]))], (1047 ^ _282358) ^ [] : [-(1040 ^ [_322766, _322768] = vreduce(1042 ^ [_322766, _322768]))]], 1061 ^ _282358 : [(1062 ^ _282358) ^ [] : [-(_322768 = vapp(vabs(1056 ^ [_322766, _322768], 1057 ^ [_322766, _322768], 1058 ^ [_322766, _322768]), 1060 ^ [_322766, _322768]))], (1066 ^ _282358) ^ [] : [visSomeExp(1059 ^ [_322766, _322768])], (1070 ^ _282358) ^ [] : [-(_322766 = vnoExp)], (1068 ^ _282358) ^ [] : [visValue(1060 ^ [_322766, _322768])], (1064 ^ _282358) ^ [] : [-(1059 ^ [_322766, _322768] = vreduce(1060 ^ [_322766, _322768]))]], 1076 ^ _282358 : [(1077 ^ _282358) ^ [] : [-(_322768 = vapp(1073 ^ [_322766, _322768], 1075 ^ [_322766, _322768]))], (1081 ^ _282358) ^ [] : [-(1074 ^ [_322766, _322768] = vreduce(1073 ^ [_322766, _322768]))], (1085 ^ _282358) ^ [] : [-(_322766 = vsomeExp(vapp(vgetSomeExp(1074 ^ [_322766, _322768]), 1075 ^ [_322766, _322768])))], (1083 ^ _282358) ^ [] : [-(visSomeExp(1074 ^ [_322766, _322768]))], (1079 ^ _282358) ^ [_327364, _327366, _327368] : [1073 ^ [_322766, _322768] = vabs(_327368, _327366, _327364)]], 1089 ^ _282358 : [(1090 ^ _282358) ^ [] : [-(_322768 = vapp(1087 ^ [_322766, _322768], 1086 ^ [_322766, _322768]))], (1094 ^ _282358) ^ [] : [-(1088 ^ [_322766, _322768] = vreduce(1087 ^ [_322766, _322768]))], (1098 ^ _282358) ^ [] : [-(_322766 = vnoExp)], (1096 ^ _282358) ^ [] : [visSomeExp(1088 ^ [_322766, _322768])], (1092 ^ _282358) ^ [_328138, _328140, _328142] : [1087 ^ [_322766, _322768] = vabs(_328142, _328140, _328138)]]], (573 ^ _282358) ^ [_303190, _303192, _303194, _303196, _303198, _303200, _303202] : [_303198 = _303202, _303196 = _303190, _303194 = vvar(_303200), _303202 = _303200, _303192 = vsubst(_303198, _303196, _303194), -(_303192 = _303190)], (194 ^ _282358) ^ [_289086, _289088, _289090, _289092] : [-(vapp(_289092, _289088) = vapp(_289090, _289086)), _289092 = _289090, _289088 = _289086], (1196 ^ _282358) ^ [_333155, _333157, _333159, _333161] : [-(vtcheck(_333159, _333157, _333155)), vtcheck(_333159, _333161, _333155), valphaEquivalent(_333161, _333157)], (458 ^ _282358) ^ [_298118, _298120, _298122, _298124] : [_298122 = _298124, _298120 = vempty, _298118 = vlookup(_298122, _298120), -(_298118 = vnoType)], (434 ^ _282358) ^ [_297249] : [vnoType = vsomeType(_297249)], (174 ^ _282358) ^ [_288380, _288382, _288384, _288386, _288388, _288390] : [-(vabs(_288390, _288386, _288382) = vabs(_288388, _288384, _288380)), _288390 = _288388, _288386 = _288384, _288382 = _288380], (1130 ^ _282358) ^ [_329736, _329738, _329740, _329742, _329744] : [-(vtcheck(_329742, vapp(_329740, _329738), _329736)), vtcheck(_329742, _329740, varrow(_329744, _329736)), vtcheck(_329742, _329738, _329744)], (126 ^ _282358) ^ [_286602, _286604, _286606, _286608] : [-(varrow(_286608, _286604) = varrow(_286606, _286602)), _286608 = _286606, _286604 = _286602], (360 ^ _282358) ^ [] : [vempty = vempty, true___, -(true___)], (849 ^ _282358) ^ [_317059] : [_317059 = vnoExp, visSomeExp(_317059)], (847 ^ _282358) ^ [_316964] : [vnoExp = vsomeExp(_316964)], (370 ^ _282358) ^ [] : [371 ^ _282358 : [(374 ^ _282358) ^ [] : [true___], (372 ^ _282358) ^ [] : [-(true___)]], -(vempty = vempty)], (266 ^ _282358) ^ [_291799, _291801, _291803] : [vvar(_291803) = vapp(_291801, _291799)], (595 ^ _282358) ^ [_303952, _303954, _303956, _303958, _303960, _303962, _303964] : [_303960 = _303962, _303958 = _303964, _303956 = vvar(_303952), -(_303962 = _303952), _303954 = vsubst(_303960, _303958, _303956), -(_303954 = vvar(_303952))], (160 ^ _282358) ^ [_287864, _287866, _287868, _287870, _287872, _287874] : [-(vsubst(_287874, _287870, _287866) = vsubst(_287872, _287868, _287864)), _287874 = _287872, _287870 = _287868, _287866 = _287864], (1108 ^ _282358) ^ [_328819, _328821, _328823, _328825] : [-(varrow(_328825, _328823) = varrow(_328821, _328819)), _328825 = _328821, _328823 = _328819], (1118 ^ _282358) ^ [_329166, _329168, _329170] : [vlookup(_329168, _329170) = vsomeType(_329166), -(vtcheck(_329170, vvar(_329168), _329166))], (817 ^ _282358) ^ [] : [vnoExp = vnoExp, true___, -(true___)], (120 ^ _282358) ^ [_286356, _286358] : [_286358 = _286356, -(vsomeType(_286358) = vsomeType(_286356))], (557 ^ _282358) ^ [_302517, _302519, _302521, _302523, _302525, _302527, _302529] : [-(vtcheck(vbind(_302529, _302527, vbind(_302525, _302523, _302521)), _302519, _302517)), -(_302525 = _302529), vtcheck(vbind(_302525, _302523, vbind(_302529, _302527, _302521)), _302519, _302517)], (891 ^ _282358) ^ [_318589, _318591, _318593, _318595, _318597, _318599, _318601] : [_318599 = vapp(vabs(_318595, _318593, _318591), _318601), _318589 = vreduce(_318601), visSomeExp(_318589), _318597 = vreduce(_318599), -(_318597 = vsomeExp(vapp(vabs(_318595, _318593, _318591), vgetSomeExp(_318589))))], (978 ^ _282358) ^ [_321807, _321809, _321811, _321813, _321815] : [_321809 = vapp(_321813, _321815), -(_321813 = vabs(983 ^ [_321807, _321809, _321811, _321813, _321815], 984 ^ [_321807, _321809, _321811, _321813, _321815], 985 ^ [_321807, _321809, _321811, _321813, _321815])), _321811 = vreduce(_321813), -(visSomeExp(_321811)), _321807 = vreduce(_321809), -(_321807 = vnoExp)], (1236 ^ _282358) ^ [_334612, _334614, _334616, _334618, _334620] : [-(vtcheck(vbind(_334620, _334618, _334616), _334614, _334612)), -(visFreeVar(_334620, _334614)), vtcheck(_334616, _334614, _334612)], (1206 ^ _282358) ^ [_333472, _333474, _333476] : [visFreeVar(_333474, _333472), -(visFreeVar(_333474, _333476)), valphaEquivalent(_333476, _333472)], (334 ^ _282358) ^ [_294325, _294327, _294329, _294331, _294333] : [_294333 = _294327, _294331 = vapp(_294329, _294325), 341 ^ _282358 : [(350 ^ _282358) ^ [] : [visFreeVar(_294333, _294331), -(visFreeVar(_294327, _294329)), -(visFreeVar(_294327, _294325))], (342 ^ _282358) ^ [] : [343 ^ _282358 : [(346 ^ _282358) ^ [] : [visFreeVar(_294327, _294325)], (344 ^ _282358) ^ [] : [visFreeVar(_294327, _294329)]], -(visFreeVar(_294333, _294331))]]], (288 ^ _282358) ^ [_292795, _292797, _292799, _292801] : [_292801 = _292795, _292799 = vvar(_292797), 295 ^ _282358 : [(302 ^ _282358) ^ [] : [visFreeVar(_292801, _292799), -(_292797 = _292795)], (296 ^ _282358) ^ [] : [_292797 = _292795, -(visFreeVar(_292801, _292799))]]], (282 ^ _282358) ^ [_292546, _292548, _292550] : [_292546 = vapp(_292550, _292548), visValue(_292546)], (635 ^ _282358) ^ [_305456, _305458, _305460, _305462, _305464, _305466, _305468, _305470, _305472] : [_305468 = _305470, _305466 = _305472, _305464 = vabs(_305460, _305458, _305456), _305470 = _305460, _305462 = vsubst(_305468, _305466, _305464), -(_305462 = vabs(_305460, _305458, _305456))], (448 ^ _282358) ^ [_297773, _297775, _297777] : [_297777 = vsomeType(_297773), _297775 = vgetSomeType(_297777), -(_297775 = _297773)], (216 ^ _282358) ^ [_289899, _289901] : [_289901 = _289899, -(vvar(_289901) = vvar(_289899))], (2 ^ _282358) ^ [_282482] : [-(_282482 = _282482)], (420 ^ _282358) ^ [_296776, _296778] : [vsomeType(_296778) = vsomeType(_296776), -(_296778 = _296776)], (835 ^ _282358) ^ [_316604, _316606] : [vsomeExp(_316606) = vsomeExp(_316604), -(_316606 = _316604)], (432 ^ _282358) ^ [_297164, _297166, _297168] : [vempty = vbind(_297168, _297166, _297164)], (909 ^ _282358) ^ [_319270, _319272, _319274, _319276, _319278, _319280, _319282] : [_319278 = vapp(vabs(_319274, _319282, _319270), _319272), _319276 = vreduce(_319278), -(_319276 = vsomeExp(vsubst(_319274, _319272, _319270))), _319280 = vreduce(_319272), -(visSomeExp(_319280)), visValue(_319272)], (264 ^ _282358) ^ [_291682, _291684, _291686, _291688] : [vvar(_291688) = vabs(_291686, _291684, _291682)], (931 ^ _282358) ^ [_320051, _320053, _320055, _320057, _320059, _320061, _320063] : [_320053 = vapp(vabs(_320063, _320061, _320059), _320055), _320051 = vreduce(_320053), -(_320051 = vnoExp), _320057 = vreduce(_320055), -(visSomeExp(_320057)), -(visValue(_320055))], (1246 ^ _282358) ^ [_335020, _335022, _335024, _335026, _335028, _335030, _335032, _335034] : [-(vtcheck(_335032, vsubst(_335030, _335028, vabs(_335026, _335024, _335022)), _335020)), -(_335030 = _335026), -(visFreeVar(_335026, _335028)), vtcheck(_335032, _335028, _335034), vtcheck(vbind(_335030, _335034, _335032), vabs(_335026, _335024, _335022), _335020)], (827 ^ _282358) ^ [] : [828 ^ _282358 : [(831 ^ _282358) ^ [] : [true___], (829 ^ _282358) ^ [] : [-(true___)]], -(vnoExp = vnoExp)], (436 ^ _282358) ^ [_297344] : [_297344 = vnoType, visSomeType(_297344)], (871 ^ _282358) ^ [_317819, _317821, _317823] : [_317821 = vvar(_317823), _317819 = vreduce(_317821), -(_317819 = vnoExp)], (1190 ^ _282358) ^ [_332874, _332876, _332878, _332880] : [-(visFreeVar(_332876, _332874)), -(valphaEquivalent(vabs(_332878, _332880, _332874), vabs(_332876, _332880, vsubst(_332878, vvar(_332876), _332874))))], (378 ^ _282358) ^ [_295565, _295567, _295569, _295571, _295573, _295575] : [vbind(_295575, _295573, _295571) = vbind(_295569, _295567, _295565), 381 ^ _282358 : [(386 ^ _282358) ^ [] : [-(_295571 = _295565)], (384 ^ _282358) ^ [] : [-(_295573 = _295567)], (382 ^ _282358) ^ [] : [-(_295575 = _295569)]]], (40 ^ _282358) ^ [_283696, _283698] : [-(visSomeExp(_283696)), _283698 = _283696, visSomeExp(_283698)], (1180 ^ _282358) ^ [_332537, _332539, _332541] : [-(valphaEquivalent(_332539, _332537)), valphaEquivalent(_332539, _332541), valphaEquivalent(_332541, _332537)], (881 ^ _282358) ^ [_318178, _318180, _318182, _318184, _318186] : [_318180 = vabs(_318186, _318184, _318182), _318178 = vreduce(_318180), -(_318178 = vnoExp)], (1216 ^ _282358) ^ [_333837, _333839, _333841, _333843, _333845] : [-(vtcheck(vbind(_333845, _333843, _333841), _333839, _333837)), vlookup(_333845, _333841) = vnoType, vtcheck(_333841, _333839, _333837)], (855 ^ _282358) ^ [_317262, _317264] : [_317262 = vsomeExp(_317264), -(visSomeExp(_317262))], (210 ^ _282358) ^ [_289729, _289731] : [vvar(_289731) = vvar(_289729), -(_289731 = _289729)], (146 ^ _282358) ^ [_287348, _287350, _287352, _287354, _287356, _287358] : [-(vbind(_287358, _287354, _287350) = vbind(_287356, _287352, _287348)), _287358 = _287356, _287354 = _287352, _287350 = _287348], (232 ^ _282358) ^ [_290562, _290564, _290566, _290568, _290570, _290572] : [-(vabs(_290572, _290570, _290568) = vabs(_290566, _290564, _290562)), _290572 = _290566, _290570 = _290564, _290568 = _290562], (270 ^ _282358) ^ [_292091, _292093, _292095, _292097] : [_292091 = vabs(_292097, _292095, _292093), -(visValue(_292091))], (953 ^ _282358) ^ [_320795, _320797, _320799, _320801, _320803] : [_320801 = vapp(_320803, _320795), -(_320803 = vabs(958 ^ [_320795, _320797, _320799, _320801, _320803], 959 ^ [_320795, _320797, _320799, _320801, _320803], 960 ^ [_320795, _320797, _320799, _320801, _320803])), _320797 = vreduce(_320803), visSomeExp(_320797), _320799 = vreduce(_320801), -(_320799 = vsomeExp(vapp(vgetSomeExp(_320797), _320795)))], (276 ^ _282358) ^ [_292319, _292321] : [_292319 = vvar(_292321), visValue(_292319)], (222 ^ _282358) ^ [_290195, _290197, _290199, _290201, _290203, _290205] : [vabs(_290205, _290203, _290201) = vabs(_290199, _290197, _290195), 225 ^ _282358 : [(230 ^ _282358) ^ [] : [-(_290201 = _290195)], (228 ^ _282358) ^ [] : [-(_290203 = _290197)], (226 ^ _282358) ^ [] : [-(_290205 = _290199)]]], (254 ^ _282358) ^ [_291337, _291339, _291341, _291343] : [-(vapp(_291343, _291341) = vapp(_291339, _291337)), _291343 = _291339, _291341 = _291337], (102 ^ _282358) ^ [_285702, _285704] : [_285704 = _285702, -(vsomeExp(_285704) = vsomeExp(_285702))], (1124 ^ _282358) ^ [_329440, _329442, _329444, _329446, _329448] : [vtcheck(vbind(_329446, _329442, _329448), _329444, _329440), -(vtcheck(_329448, vabs(_329446, _329442, _329444), varrow(_329442, _329440)))], (1100 ^ _282358) ^ [_328554, _328556, _328558, _328560] : [varrow(_328560, _328558) = varrow(_328556, _328554), 1103 ^ _282358 : [(1106 ^ _282358) ^ [] : [-(_328558 = _328554)], (1104 ^ _282358) ^ [] : [-(_328560 = _328556)]]], (136 ^ _282358) ^ [_286961, _286963, _286965, _286967] : [-(vlookup(_286967, _286963) = vlookup(_286965, _286961)), _286967 = _286965, _286963 = _286961], (20 ^ _282358) ^ [_283106, _283108] : [-(visSomeType(_283106)), _283108 = _283106, visSomeType(_283108)], (1172 ^ _282358) ^ [_332206] : [-(valphaEquivalent(_332206, _332206))], (442 ^ _282358) ^ [_297547, _297549] : [_297547 = vsomeType(_297549), -(visSomeType(_297547))], (426 ^ _282358) ^ [_296946, _296948] : [_296948 = _296946, -(vsomeType(_296948) = vsomeType(_296946))], (10 ^ _282358) ^ [_282793, _282795, _282797] : [-(_282797 = _282793), _282797 = _282795, _282795 = _282793], (508 ^ _282358) ^ [_299875, _299877, _299879] : [vlookup(_299879, _299877) = _299875, 514 ^ _282358 : [(519 ^ _282358) ^ [] : [-(_299875 = vnoType)], (517 ^ _282358) ^ [] : [-(_299877 = vempty)], (515 ^ _282358) ^ [] : [-(_299879 = 513 ^ [_299875, _299877, _299879])]], 526 ^ _282358 : [(529 ^ _282358) ^ [] : [-(_299877 = vbind(524 ^ [_299875, _299877, _299879], 525 ^ [_299875, _299877, _299879], 522 ^ [_299875, _299877, _299879]))], (531 ^ _282358) ^ [] : [-(523 ^ [_299875, _299877, _299879] = 524 ^ [_299875, _299877, _299879])], (533 ^ _282358) ^ [] : [-(_299875 = vsomeType(525 ^ [_299875, _299877, _299879]))], (527 ^ _282358) ^ [] : [-(_299879 = 523 ^ [_299875, _299877, _299879])]], 538 ^ _282358 : [(541 ^ _282358) ^ [] : [-(_299877 = vbind(535 ^ [_299875, _299877, _299879], 534 ^ [_299875, _299877, _299879], 537 ^ [_299875, _299877, _299879]))], (543 ^ _282358) ^ [] : [536 ^ [_299875, _299877, _299879] = 535 ^ [_299875, _299877, _299879]], (545 ^ _282358) ^ [] : [-(_299875 = vlookup(536 ^ [_299875, _299877, _299879], 537 ^ [_299875, _299877, _299879]))], (539 ^ _282358) ^ [] : [-(_299879 = 536 ^ [_299875, _299877, _299879])]]], (4 ^ _282358) ^ [_282589, _282591] : [_282591 = _282589, -(_282589 = _282591)], (657 ^ _282358) ^ [_306316, _306318, _306320, _306322, _306324, _306326, _306328, _306330, _306332, _306334] : [_306334 = _306326, _306332 = _306324, _306330 = vabs(_306320, _306322, _306316), _306328 = vsubst(_306334, _306332, _306330), -(_306328 = vsubst(_306326, _306324, vabs(_306318, _306322, vsubst(_306320, vvar(_306318), _306316)))), -(_306326 = _306320), visFreeVar(_306320, _306324), _306318 = vgensym(vapp(vapp(_306324, _306316), vvar(_306326)))], (108 ^ _282358) ^ [_285920, _285922] : [_285922 = _285920, -(vgetSomeExp(_285922) = vgetSomeExp(_285920))], (188 ^ _282358) ^ [_288840, _288842] : [_288842 = _288840, -(vgensym(_288842) = vgensym(_288840))], (402 ^ _282358) ^ [] : [vnoType = vnoType, true___, -(true___)], (30 ^ _282358) ^ [_283401, _283403] : [-(visValue(_283401)), _283403 = _283401, visValue(_283403)], (713 ^ _282358) ^ [_308380, _308382, _308384, _308386] : [vsubst(_308386, _308384, _308382) = _308380, 721 ^ _282358 : [(722 ^ _282358) ^ [] : [-(_308386 = 718 ^ [_308380, _308382, _308384, _308386])], (726 ^ _282358) ^ [] : [-(_308382 = vvar(719 ^ [_308380, _308382, _308384, _308386]))], (730 ^ _282358) ^ [] : [-(_308380 = 720 ^ [_308380, _308382, _308384, _308386])], (728 ^ _282358) ^ [] : [-(718 ^ [_308380, _308382, _308384, _308386] = 719 ^ [_308380, _308382, _308384, _308386])], (724 ^ _282358) ^ [] : [-(_308384 = 720 ^ [_308380, _308382, _308384, _308386])]], 736 ^ _282358 : [(737 ^ _282358) ^ [] : [-(_308386 = 734 ^ [_308380, _308382, _308384, _308386])], (741 ^ _282358) ^ [] : [-(_308382 = vvar(735 ^ [_308380, _308382, _308384, _308386]))], (745 ^ _282358) ^ [] : [-(_308380 = vvar(735 ^ [_308380, _308382, _308384, _308386]))], (743 ^ _282358) ^ [] : [734 ^ [_308380, _308382, _308384, _308386] = 735 ^ [_308380, _308382, _308384, _308386]], (739 ^ _282358) ^ [] : [-(_308384 = 733 ^ [_308380, _308382, _308384, _308386])]], 752 ^ _282358 : [(755 ^ _282358) ^ [] : [-(_308384 = 750 ^ [_308380, _308382, _308384, _308386])], (757 ^ _282358) ^ [] : [-(_308382 = vapp(748 ^ [_308380, _308382, _308384, _308386], 751 ^ [_308380, _308382, _308384, _308386]))], (759 ^ _282358) ^ [] : [-(_308380 = vapp(vsubst(749 ^ [_308380, _308382, _308384, _308386], 750 ^ [_308380, _308382, _308384, _308386], 748 ^ [_308380, _308382, _308384, _308386]), vsubst(749 ^ [_308380, _308382, _308384, _308386], 750 ^ [_308380, _308382, _308384, _308386], 751 ^ [_308380, _308382, _308384, _308386])))], (753 ^ _282358) ^ [] : [-(_308386 = 749 ^ [_308380, _308382, _308384, _308386])]], 767 ^ _282358 : [(768 ^ _282358) ^ [] : [-(_308386 = 763 ^ [_308380, _308382, _308384, _308386])], (772 ^ _282358) ^ [] : [-(_308382 = vabs(764 ^ [_308380, _308382, _308384, _308386], 765 ^ [_308380, _308382, _308384, _308386], 766 ^ [_308380, _308382, _308384, _308386]))], (776 ^ _282358) ^ [] : [-(_308380 = vabs(764 ^ [_308380, _308382, _308384, _308386], 765 ^ [_308380, _308382, _308384, _308386], 766 ^ [_308380, _308382, _308384, _308386]))], (774 ^ _282358) ^ [] : [-(763 ^ [_308380, _308382, _308384, _308386] = 764 ^ [_308380, _308382, _308384, _308386])], (770 ^ _282358) ^ [] : [-(_308384 = 762 ^ [_308380, _308382, _308384, _308386])]], 785 ^ _282358 : [(790 ^ _282358) ^ [] : [-(_308382 = vabs(782 ^ [_308380, _308382, _308384, _308386], 781 ^ [_308380, _308382, _308384, _308386], 784 ^ [_308380, _308382, _308384, _308386]))], (796 ^ _282358) ^ [] : [-(783 ^ [_308380, _308382, _308384, _308386] = vgensym(vapp(vapp(780 ^ [_308380, _308382, _308384, _308386], 784 ^ [_308380, _308382, _308384, _308386]), vvar(779 ^ [_308380, _308382, _308384, _308386]))))], (798 ^ _282358) ^ [] : [-(_308380 = vsubst(779 ^ [_308380, _308382, _308384, _308386], 780 ^ [_308380, _308382, _308384, _308386], vabs(783 ^ [_308380, _308382, _308384, _308386], 781 ^ [_308380, _308382, _308384, _308386], vsubst(782 ^ [_308380, _308382, _308384, _308386], vvar(783 ^ [_308380, _308382, _308384, _308386]), 784 ^ [_308380, _308382, _308384, _308386]))))], (792 ^ _282358) ^ [] : [779 ^ [_308380, _308382, _308384, _308386] = 782 ^ [_308380, _308382, _308384, _308386]], (786 ^ _282358) ^ [] : [-(_308386 = 779 ^ [_308380, _308382, _308384, _308386])], (788 ^ _282358) ^ [] : [-(_308384 = 780 ^ [_308380, _308382, _308384, _308386])], (794 ^ _282358) ^ [] : [-(visFreeVar(782 ^ [_308380, _308382, _308384, _308386], 780 ^ [_308380, _308382, _308384, _308386]))]], 804 ^ _282358 : [(807 ^ _282358) ^ [] : [-(_308384 = 802 ^ [_308380, _308382, _308384, _308386])], (805 ^ _282358) ^ [] : [-(_308386 = 801 ^ [_308380, _308382, _308384, _308386])], (815 ^ _282358) ^ [] : [-(_308380 = vabs(799 ^ [_308380, _308382, _308384, _308386], 800 ^ [_308380, _308382, _308384, _308386], vsubst(801 ^ [_308380, _308382, _308384, _308386], 802 ^ [_308380, _308382, _308384, _308386], 803 ^ [_308380, _308382, _308384, _308386])))], (811 ^ _282358) ^ [] : [801 ^ [_308380, _308382, _308384, _308386] = 799 ^ [_308380, _308382, _308384, _308386]], (813 ^ _282358) ^ [] : [visFreeVar(799 ^ [_308380, _308382, _308384, _308386], 802 ^ [_308380, _308382, _308384, _308386])], (809 ^ _282358) ^ [] : [-(_308382 = vabs(799 ^ [_308380, _308382, _308384, _308386], 800 ^ [_308380, _308382, _308384, _308386], 803 ^ [_308380, _308382, _308384, _308386]))]]], (567 ^ _282358) ^ [_302905, _302907] : [vgensym(_302905) = _302907, visFreeVar(_302907, _302905)]], input).
% 87.79/84.51 ncf('1',plain,[-(1266 ^ [] = vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))))],start(1268 ^ 0)).
% 87.79/84.51 ncf('1.1',plain,[1266 ^ [] = vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))), vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ [])) = vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ [])), 346 : visFreeVar(vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))), vvar(1265 ^ [])), 346 : -(visFreeVar(1266 ^ [], vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))))],extension(334 ^ 1,bind([[_294325, _294327, _294329, _294331, _294333], [vvar(1265 ^ []), vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))), vapp(1263 ^ [], 1264 ^ []), vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ [])), 1266 ^ []]]))).
% 87.79/84.51 ncf('1.1.1',plain,[-(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ [])) = vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))), vapp(_199000, vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))) = vapp(_199000, vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ [])))],extension(246 ^ 2,bind([[_291072, _291074, _291076, _291078], [vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ [])), _199000, vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ [])), _199000]]))).
% 87.79/84.51 ncf('1.1.1.1',plain,[-(vapp(_199000, vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))) = vapp(_199000, vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))))],extension(2 ^ 3,bind([[_282482], [vapp(_199000, vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ [])))]]))).
% 87.79/84.51 ncf('1.1.2',plain,[-(visFreeVar(vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))), vvar(1265 ^ []))), 296 : 1266 ^ [] = vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))), 296 : vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))) = vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))), 296 : vvar(1265 ^ []) = vvar(1266 ^ [])],extension(288 ^ 6,bind([[_292795, _292797, _292799, _292801], [vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))), 1266 ^ [], vvar(1265 ^ []), vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ [])))]]))).
% 87.79/84.51 ncf('1.1.2.1',plain,[-(1266 ^ [] = vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))))],reduction('1')).
% 87.79/84.51 ncf('1.1.2.2',plain,[-(vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))) = vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))))],extension(2 ^ 7,bind([[_282482], [vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ [])))]]))).
% 87.79/84.51 ncf('1.1.2.3',plain,[-(vvar(1265 ^ []) = vvar(1266 ^ [])), 1265 ^ [] = 1266 ^ []],extension(204 ^ 7,bind([[_289397, _289399], [1266 ^ [], 1265 ^ []]]))).
% 87.79/84.51 ncf('1.1.2.3.1',plain,[-(1265 ^ [] = 1266 ^ [])],extension(1270 ^ 8)).
% 87.79/84.51 ncf('1.1.3',plain,[visFreeVar(1266 ^ [], vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))), vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))) = 1266 ^ []],extension(567 ^ 4,bind([[_302905, _302907], [vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ [])), 1266 ^ []]]))).
% 87.79/84.51 ncf('1.1.3.1',plain,[-(vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))) = 1266 ^ []), 1266 ^ [] = vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ [])))],extension(4 ^ 5,bind([[_282589, _282591], [vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))), 1266 ^ []]]))).
% 87.79/84.51 ncf('1.1.3.1.1',plain,[-(1266 ^ [] = vgensym(vapp(vapp(1263 ^ [], 1264 ^ []), vvar(1265 ^ []))))],reduction('1')).
% 87.79/84.51 %-----------------------------------------------------
% 87.79/84.51 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------