%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO281+1 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n029.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 11:12:24 EDT 2023
% Result : Theorem 102.67s 98.99s
% Output : Proof 102.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : GEO281+1 : TPTP v8.1.2. Released v4.1.0.
% 0.12/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n029.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri May 19 04:29:58 EDT 2023
% 0.12/0.34 % CPUTime :
% 102.67/98.99
% 102.67/98.99 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 102.67/98.99 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 102.67/98.99 %-----------------------------------------------------
% 102.67/98.99 ncf(matrix, plain, [(4758 ^ _216680) ^ [_382021] : [rR(_382021, vd1123, vd1125), ron(_382021, vd1139), ron(_382021, vd1138), rpoint(_382021)], (204 ^ _216680) ^ [_223345, _223347, _223349, _223351, _223353, _223355, _223357, _223359] : [-(vskolem1078(_223359, _223355, _223351, _223347) = vskolem1078(_223357, _223353, _223349, _223345)), _223359 = _223357, _223355 = _223353, _223351 = _223349, _223347 = _223345], (222 ^ _216680) ^ [_224034, _224036, _224038, _224040, _224042, _224044, _224046, _224048] : [-(vskolem1052(_224048, _224044, _224040, _224036) = vskolem1052(_224046, _224042, _224038, _224034)), _224048 = _224046, _224044 = _224042, _224040 = _224038, _224036 = _224034], (240 ^ _216680) ^ [_224695, _224697, _224699, _224701, _224703, _224705] : [-(vtriangle(_224705, _224701, _224697) = vtriangle(_224703, _224699, _224695)), _224705 = _224703, _224701 = _224699, _224697 = _224695], (254 ^ _216680) ^ [_225211, _225213, _225215, _225217, _225219, _225221] : [-(vg(_225221, _225217, _225213) = vg(_225219, _225215, _225211)), _225221 = _225219, _225217 = _225215, _225213 = _225211], (268 ^ _216680) ^ [_225699, _225701, _225703, _225705] : [-(vplus(_225705, _225701) = vplus(_225703, _225699)), _225705 = _225703, _225701 = _225699], (292 ^ _216680) ^ [_226554, _226556, _226558, _226560] : [-(vf(_226560, _226556) = vf(_226558, _226554)), _226560 = _226558, _226556 = _226554], (278 ^ _216680) ^ [_226086, _226088, _226090, _226092, _226094, _226096] : [-(vangle(_226096, _226092, _226088) = vangle(_226094, _226090, _226086)), _226096 = _226094, _226092 = _226090, _226088 = _226086], (2 ^ _216680) ^ [_216824] : [-(_216824 = _216824)], (4 ^ _216680) ^ [_216931, _216933] : [_216933 = _216931, -(_216931 = _216933)], (10 ^ _216680) ^ [_217135, _217137, _217139] : [-(_217139 = _217135), _217139 = _217137, _217137 = _217135], (20 ^ _216680) ^ [_217476, _217478, _217480, _217482] : [-(rcenter(_217480, _217476)), rcenter(_217482, _217478), _217482 = _217480, _217478 = _217476], (34 ^ _216680) ^ [_217920, _217922, _217924, _217926] : [-(rinside(_217924, _217920)), rinside(_217926, _217922), _217926 = _217924, _217922 = _217920], (48 ^ _216680) ^ [_218336, _218338] : [-(rcircle(_218336)), _218338 = _218336, rcircle(_218338)], (58 ^ _216680) ^ [_218631, _218633] : [-(rtriangle(_218631)), _218633 = _218631, rtriangle(_218633)], (68 ^ _216680) ^ [_218954, _218956, _218958, _218960] : [-(rgeq(_218958, _218954)), rgeq(_218960, _218956), _218960 = _218958, _218956 = _218954], (82 ^ _216680) ^ [_219370, _219372] : [-(rreal(_219370)), _219372 = _219370, rreal(_219372)], (92 ^ _216680) ^ [_219693, _219695, _219697, _219699] : [-(rless(_219697, _219693)), rless(_219699, _219695), _219699 = _219697, _219695 = _219693], (106 ^ _216680) ^ [_220109, _220111] : [-(rline(_220109)), _220111 = _220109, rline(_220111)], (116 ^ _216680) ^ [_220460, _220462, _220464, _220466, _220468, _220470] : [-(rS(_220468, _220464, _220460)), rS(_220470, _220466, _220462), _220470 = _220468, _220466 = _220464, _220462 = _220460], (134 ^ _216680) ^ [_221041, _221043, _221045, _221047] : [-(rintersect(_221045, _221041)), rintersect(_221047, _221043), _221047 = _221045, _221043 = _221041], (148 ^ _216680) ^ [_221485, _221487, _221489, _221491] : [-(rleq(_221489, _221485)), rleq(_221491, _221487), _221491 = _221489, _221487 = _221485], (162 ^ _216680) ^ [_221957, _221959, _221961, _221963, _221965, _221967] : [-(rR(_221965, _221961, _221957)), rR(_221967, _221963, _221959), _221967 = _221965, _221963 = _221961, _221959 = _221957], (194 ^ _216680) ^ [_222934, _222936] : [-(rpoint(_222934)), _222936 = _222934, rpoint(_222936)], (180 ^ _216680) ^ [_222538, _222540, _222542, _222544] : [-(ron(_222542, _222538)), ron(_222544, _222540), _222544 = _222542, _222540 = _222538], (302 ^ _216680) ^ [] : [ron(vd1125, vd1139)], (304 ^ _216680) ^ [] : [rinside(vd1125, vd1139)], (306 ^ _216680) ^ [] : [-(ron(vd1136, vd1139))], (308 ^ _216680) ^ [] : [-(rcenter(vd1123, vd1139))], (310 ^ _216680) ^ [] : [-(rcircle(vd1139))], (312 ^ _216680) ^ [] : [-(ron(vd1125, vd1138))], (314 ^ _216680) ^ [] : [-(ron(vd1123, vd1138))], (316 ^ _216680) ^ [] : [-(vf(vd1127, vd1129) = vf(vd1123, vd1136))], (318 ^ _216680) ^ [] : [-(rpoint(vd1136))], (320 ^ _216680) ^ [] : [-(rless(vf(vd1127, vd1129), vf(vd1123, vd1125)))], (322 ^ _216680) ^ [] : [vd1127 = vd1129], (324 ^ _216680) ^ [] : [vd1123 = vd1125], (326 ^ _216680) ^ [] : [-(vd1129 = vd1130)], (328 ^ _216680) ^ [] : [-(rpoint(vd1130))], (330 ^ _216680) ^ [] : [-(vd1127 = vd1128)], (332 ^ _216680) ^ [] : [-(rpoint(vd1128))], (334 ^ _216680) ^ [] : [-(vd1125 = vd1126)], (336 ^ _216680) ^ [] : [-(rpoint(vd1126))], (338 ^ _216680) ^ [] : [-(vd1123 = vd1124)], (340 ^ _216680) ^ [] : [-(rpoint(vd1124))], (342 ^ _216680) ^ [_228083, _228085, _228087, _228089, _228091, _228093] : [365 ^ _216680 : [(366 ^ _216680) ^ [] : [vf(_228089, _228093) = vf(_228089, _228085), -(ron(_228093, _228087))], (372 ^ _216680) ^ [] : [ron(_228093, _228087), -(vf(_228089, _228093) = vf(_228089, _228085))]], ron(_228085, _228087), _228085 = _228083, rpoint(_228083), rcenter(_228089, _228087), _228093 = _228091, rpoint(_228091)], (378 ^ _216680) ^ [_229146, _229148] : [394 ^ _216680 : [(395 ^ _216680) ^ [] : [-(vf(_229148, _229146) = 393 ^ [_229146, _229148])], (397 ^ _216680) ^ [] : [-(rreal(393 ^ [_229146, _229148]))]], 381 ^ _216680 : [(382 ^ _216680) ^ [_229300] : [_229146 = _229300, rpoint(_229300)]], 387 ^ _216680 : [(388 ^ _216680) ^ [_229483] : [_229148 = _229483, rpoint(_229483)]]], (399 ^ _216680) ^ [_229894, _229896] : [rless(_229896, _229896), _229896 = _229894, rreal(_229894)], (409 ^ _216680) ^ [] : [-(rline(vd1138))], (411 ^ _216680) ^ [_230273, _230275, _230277, _230279] : [434 ^ _216680 : [(435 ^ _216680) ^ [] : [rless(vf(_230275, _230279), vf(_230275, _230277)), -(rinside(_230279, _230273))], (441 ^ _216680) ^ [] : [rinside(_230279, _230273), -(rless(vf(_230275, _230279), vf(_230275, _230277)))]], ron(_230277, _230273), rcenter(_230275, _230273), 422 ^ _216680 : [(423 ^ _216680) ^ [_230620] : [_230277 = _230620, rpoint(_230620)]], 428 ^ _216680 : [(429 ^ _216680) ^ [_230819] : [_230279 = _230819, rpoint(_230819)]]], (447 ^ _216680) ^ [_231424, _231426, _231428, _231430] : [rless(_231426, _231430), -(_231430 = _231426), rless(_231430, _231426), _231426 = _231424, rreal(_231424), _231430 = _231428, rreal(_231428)], (473 ^ _216680) ^ [_232215, _232217, _232219, _232221, _232223, _232225, _232227, _232229] : [525 ^ _216680 : [(526 ^ _216680) ^ [] : [-(rR(524 ^ [_232215, _232217, _232219, _232221, _232223, _232225, _232227, _232229], _232221, _232217))], (528 ^ _216680) ^ [] : [-(ron(524 ^ [_232215, _232217, _232219, _232221, _232223, _232225, _232227, _232229], _232229))], (530 ^ _216680) ^ [] : [-(ron(524 ^ [_232215, _232217, _232219, _232221, _232223, _232225, _232227, _232229], _232225))], (532 ^ _216680) ^ [] : [-(rpoint(524 ^ [_232215, _232217, _232219, _232221, _232223, _232225, _232227, _232229]))]], ron(_232217, _232225), -(ron(_232217, _232229)), -(rinside(_232217, _232229)), _232217 = _232215, rpoint(_232215), ron(_232221, _232225), rinside(_232221, _232229), _232221 = _232219, rpoint(_232219), _232225 = _232223, rline(_232223), _232229 = _232227, rcircle(_232227)], (534 ^ _216680) ^ [] : [vd1123 = vd1129], (536 ^ _216680) ^ [] : [vd1123 = vd1127], (538 ^ _216680) ^ [_234346, _234348] : [-(_234348 = _234346), 545 ^ _216680 : [(546 ^ _216680) ^ [_234623] : [_234346 = _234623, rpoint(_234623)]], 551 ^ _216680 : [(552 ^ _216680) ^ [_234806] : [_234348 = _234806, rpoint(_234806)]], 557 ^ _216680 : [(558 ^ _216680) ^ [_235013, _235015] : [-(vf(_234348, _234346) = vf(_235015, vskolem1078(_235015, _235013, _234348, _234346))), _235015 = _235013, -(_235015 = _234346), -(_235015 = _234348), rpoint(_235013)]]], (576 ^ _216680) ^ [_235565, _235567] : [-(_235567 = _235565), 583 ^ _216680 : [(584 ^ _216680) ^ [_235835] : [_235565 = _235835, rpoint(_235835)]], 589 ^ _216680 : [(590 ^ _216680) ^ [_236018] : [_235567 = _236018, rpoint(_236018)]], 595 ^ _216680 : [(596 ^ _216680) ^ [_236225, _236227] : [-(rpoint(vskolem1078(_236227, _236225, _235567, _235565))), _236227 = _236225, -(_236227 = _235565), -(_236227 = _235567), rpoint(_236225)]]], (614 ^ _216680) ^ [_236763, _236765] : [617 ^ _216680 : [(618 ^ _216680) ^ [_236913] : [_236763 = _236913, rpoint(_236913)]], 623 ^ _216680 : [(624 ^ _216680) ^ [_237096] : [_236765 = _237096, rpoint(_237096)]], 629 ^ _216680 : [(630 ^ _216680) ^ [] : [vf(_236765, _236763) = v0, -(_236765 = _236763)], (636 ^ _216680) ^ [] : [_236765 = _236763, -(vf(_236765, _236763) = v0)]]], (642 ^ _216680) ^ [_237621, _237623] : [662 ^ _216680 : [(663 ^ _216680) ^ [] : [-(ron(_237621, 661 ^ [_237621, _237623]))], (665 ^ _216680) ^ [] : [-(rcenter(_237623, 661 ^ [_237621, _237623]))], (667 ^ _216680) ^ [] : [-(rcircle(661 ^ [_237621, _237623]))]], -(_237623 = _237621), 649 ^ _216680 : [(650 ^ _216680) ^ [_237866] : [_237621 = _237866, rpoint(_237866)]], 655 ^ _216680 : [(656 ^ _216680) ^ [_238049] : [_237623 = _238049, rpoint(_238049)]]], (669 ^ _216680) ^ [_238539, _238541] : [689 ^ _216680 : [(690 ^ _216680) ^ [] : [-(ron(_238539, 688 ^ [_238539, _238541]))], (692 ^ _216680) ^ [] : [-(ron(_238541, 688 ^ [_238539, _238541]))], (694 ^ _216680) ^ [] : [-(rline(688 ^ [_238539, _238541]))]], -(_238541 = _238539), 676 ^ _216680 : [(677 ^ _216680) ^ [_238784] : [_238539 = _238784, rpoint(_238784)]], 682 ^ _216680 : [(683 ^ _216680) ^ [_238967] : [_238541 = _238967, rpoint(_238967)]]], (696 ^ _216680) ^ [_239457, _239459] : [rcenter(_239459, _239457), 701 ^ _216680 : [(702 ^ _216680) ^ [] : [-(_239457 = 700 ^ [_239457, _239459])], (704 ^ _216680) ^ [] : [-(rcircle(700 ^ [_239457, _239459]))], (706 ^ _216680) ^ [] : [-(_239459 = 699 ^ [_239457, _239459])], (708 ^ _216680) ^ [] : [-(rpoint(699 ^ [_239457, _239459]))]]], (710 ^ _216680) ^ [_240121, _240123, _240125, _240127, _240129, _240131] : [-(_240131 = _240127), vplus(_240131, _240123) = vplus(_240127, _240123), _240123 = _240121, rreal(_240121), _240127 = _240125, rreal(_240125), _240131 = _240129, rreal(_240129)], (740 ^ _216680) ^ [_241019, _241021, _241023, _241025] : [761 ^ _216680 : [(762 ^ _216680) ^ [] : [759 ^ [_241019, _241021, _241023, _241025] = 760 ^ [_241019, _241021, _241023, _241025]], (764 ^ _216680) ^ [] : [-(ron(760 ^ [_241019, _241021, _241023, _241025], _241025))], (766 ^ _216680) ^ [] : [-(ron(760 ^ [_241019, _241021, _241023, _241025], _241021))], (768 ^ _216680) ^ [] : [-(rpoint(760 ^ [_241019, _241021, _241023, _241025]))], (770 ^ _216680) ^ [] : [-(ron(759 ^ [_241019, _241021, _241023, _241025], _241025))], (772 ^ _216680) ^ [] : [-(ron(759 ^ [_241019, _241021, _241023, _241025], _241021))], (774 ^ _216680) ^ [] : [-(rpoint(759 ^ [_241019, _241021, _241023, _241025]))]], rintersect(_241021, _241025), _241021 = _241019, rline(_241019), _241025 = _241023, rcircle(_241023)], (776 ^ _216680) ^ [_242444, _242446, _242448, _242450] : [-(vf(_242446, vskolem1052(_242450, _242448, _242446, _242444)) = vf(vskolem1052(_242450, _242448, _242446, _242444), _242450)), _242446 = _242444, -(_242450 = _242446), rpoint(_242444), _242450 = _242448, rpoint(_242448)], (798 ^ _216680) ^ [_243113, _243115, _243117, _243119] : [-(vf(_243119, _243115) = vf(_243115, vskolem1052(_243119, _243117, _243115, _243113))), _243115 = _243113, -(_243119 = _243115), rpoint(_243113), _243119 = _243117, rpoint(_243117)], (820 ^ _216680) ^ [_243772, _243774, _243776, _243778] : [-(rpoint(vskolem1052(_243778, _243776, _243774, _243772))), _243774 = _243772, -(_243778 = _243774), rpoint(_243772), _243778 = _243776, rpoint(_243776)], (842 ^ _216680) ^ [_244445, _244447, _244449, _244451, _244453, _244455] : [925 ^ _216680 : [(926 ^ _216680) ^ [] : [vangle(_244453, _244455, _244451) = vplus(vangle(_244453, _244455, _244449), vangle(_244449, _244455, _244451)), 929 ^ _216680 : [(930 ^ _216680) ^ [] : [-(rS(_244451, _244449, _244447))], (932 ^ _216680) ^ [] : [-(rS(_244453, _244449, _244445))]]], (934 ^ _216680) ^ [] : [-(vangle(_244453, _244455, _244451) = vplus(vangle(_244453, _244455, _244449), vangle(_244449, _244455, _244451))), rS(_244451, _244449, _244447), rS(_244453, _244449, _244445)]], -(_244447 = _244445), -(ron(_244449, _244445)), -(ron(_244449, _244447)), -(_244455 = _244451), -(_244455 = _244453), ron(_244451, _244445), ron(_244453, _244447), ron(_244455, _244445), ron(_244455, _244447), 881 ^ _216680 : [(882 ^ _216680) ^ [_245619] : [_244445 = _245619, rline(_245619)]], 889 ^ _216680 : [(890 ^ _216680) ^ [_245876] : [_244447 = _245876, rline(_245876)]], 897 ^ _216680 : [(898 ^ _216680) ^ [_246133] : [_244449 = _246133, rpoint(_246133)]], 905 ^ _216680 : [(906 ^ _216680) ^ [_246390] : [_244451 = _246390, rpoint(_246390)]], 913 ^ _216680 : [(914 ^ _216680) ^ [_246647] : [_244453 = _246647, rpoint(_246647)]], 919 ^ _216680 : [(920 ^ _216680) ^ [_246862] : [_244455 = _246862, rpoint(_246862)]]], (944 ^ _216680) ^ [_247809, _247811, _247813, _247815, _247817, _247819, _247821, _247823] : [991 ^ _216680 : [(1002 ^ _216680) ^ [] : [vangle(_247819, _247823, _247815) = v0, 1005 ^ _216680 : [(1006 ^ _216680) ^ [] : [rR(_247823, _247819, _247815)], (1008 ^ _216680) ^ [] : [-(ron(_247815, _247811))]]], (992 ^ _216680) ^ [] : [-(vangle(_247819, _247823, _247815) = v0), -(rR(_247823, _247819, _247815)), ron(_247815, _247811)]], ron(_247819, _247811), ron(_247823, _247811), -(_247823 = _247815), -(_247823 = _247819), _247811 = _247809, rline(_247809), _247815 = _247813, rpoint(_247813), _247819 = _247817, rpoint(_247817), _247823 = _247821, rpoint(_247821)], (1010 ^ _216680) ^ [_249859, _249861, _249863, _249865, _249867] : [-(_249861 = _249859), vf(_249863, _249867) = vf(_249863, _249865), ron(_249865, _249859), ron(_249867, _249861), rcenter(_249863, _249859), rcenter(_249863, _249861), 1033 ^ _216680 : [(1034 ^ _216680) ^ [_250509] : [_249865 = _250509, rpoint(_250509)]], 1039 ^ _216680 : [(1040 ^ _216680) ^ [_250716] : [_249867 = _250716, rpoint(_250716)]]], (1048 ^ _216680) ^ [_251095, _251097, _251099, _251101, _251103, _251105] : [-(rless(vplus(_251105, _251097), vplus(_251101, _251097))), rless(_251105, _251101), _251097 = _251095, rreal(_251095), _251101 = _251099, rreal(_251099), _251105 = _251103, rreal(_251103)], (1078 ^ _216680) ^ [_252021, _252023, _252025, _252027, _252029, _252031] : [-(rless(_252031, _252023)), rless(_252027, _252023), rless(_252031, _252027), _252023 = _252021, rreal(_252021), _252027 = _252025, rreal(_252025), _252031 = _252029, rreal(_252029)], (1112 ^ _216680) ^ [_253012, _253014, _253016, _253018] : [-(rless(_253018, _253014)), -(_253018 = _253014), -(rless(_253014, _253018)), _253014 = _253012, rreal(_253012), _253018 = _253016, rreal(_253016)], (1138 ^ _216680) ^ [_253749, _253751, _253753, _253755] : [-(vplus(_253755, _253751) = vplus(_253751, _253755)), _253751 = _253749, rreal(_253749), _253755 = _253753, rreal(_253753)], (1156 ^ _216680) ^ [_254270, _254272] : [-(vplus(_254272, v0) = _254272), _254272 = _254270, rreal(_254270)], (1166 ^ _216680) ^ [_254601, _254603, _254605, _254607] : [1182 ^ _216680 : [(1183 ^ _216680) ^ [] : [-(vplus(_254607, _254603) = 1181 ^ [_254601, _254603, _254605, _254607])], (1185 ^ _216680) ^ [] : [-(rreal(1181 ^ [_254601, _254603, _254605, _254607]))]], _254603 = _254601, rreal(_254601), _254607 = _254605, rreal(_254605)], (1187 ^ _216680) ^ [] : [-(v0 = vd684)], (1189 ^ _216680) ^ [] : [-(rreal(vd684))], (1191 ^ _216680) ^ [_255415, _255417, _255419, _255421] : [-(rintersect(_255417, _255415)), ron(_255419, _255415), rinside(_255421, _255415), rinside(_255419, _255417), ron(_255421, _255417), 1210 ^ _216680 : [(1211 ^ _216680) ^ [_255936] : [_255419 = _255936, rpoint(_255936)]], 1216 ^ _216680 : [(1217 ^ _216680) ^ [_256135] : [_255421 = _256135, rpoint(_256135)]]], (1225 ^ _216680) ^ [_256472, _256474, _256476, _256478] : [-(rintersect(_256474, _256472)), -(rinside(_256476, _256472)), -(ron(_256476, _256472)), rinside(_256478, _256472), 1240 ^ _216680 : [(1241 ^ _216680) ^ [] : [ron(_256476, _256474)], (1243 ^ _216680) ^ [] : [rinside(_256476, _256474)]], ron(_256478, _256474), 1250 ^ _216680 : [(1251 ^ _216680) ^ [_257201] : [_256472 = _257201, rcircle(_257201)]], 1258 ^ _216680 : [(1259 ^ _216680) ^ [_257438] : [_256474 = _257438, rcircle(_257438)]], 1266 ^ _216680 : [(1267 ^ _216680) ^ [_257675] : [_256476 = _257675, rpoint(_257675)]], 1272 ^ _216680 : [(1273 ^ _216680) ^ [_257874] : [_256478 = _257874, rpoint(_257874)]]], (1281 ^ _216680) ^ [_258254, _258256, _258258, _258260, _258262, _258264] : [-(rintersect(_258256, _258260)), ron(_258264, _258256), rinside(_258264, _258260), _258256 = _258254, rline(_258254), _258260 = _258258, rcircle(_258258), _258264 = _258262, rpoint(_258262)], (1315 ^ _216680) ^ [_259245, _259247, _259249, _259251] : [-(rintersect(1363 ^ [_259245, _259247, _259249, _259251], _259247)), -(rS(_259251, _259249, 1318 ^ [_259245, _259247, _259249, _259251])), 1323 ^ _216680 : [(1324 ^ _216680) ^ [] : [ron(_259249, _259247)], (1326 ^ _216680) ^ [] : [rinside(_259249, _259247)]], 1329 ^ _216680 : [(1330 ^ _216680) ^ [] : [ron(_259251, _259247)], (1332 ^ _216680) ^ [] : [rinside(_259251, _259247)]], 1335 ^ _216680 : [(1336 ^ _216680) ^ [_259939] : [_259245 = _259939, rcircle(_259939)]], 1343 ^ _216680 : [(1344 ^ _216680) ^ [_260176] : [_259247 = _260176, rcircle(_260176)]], 1351 ^ _216680 : [(1352 ^ _216680) ^ [_260413] : [_259249 = _260413, rpoint(_260413)]], 1357 ^ _216680 : [(1358 ^ _216680) ^ [_260612] : [_259251 = _260612, rpoint(_260612)]]], (1367 ^ _216680) ^ [_261049, _261051, _261053, _261055, _261057, _261059] : [-(rintersect(_261055, _261051)), _261055 = _261053, _261051 = _261049, ron(_261057, _261051), ron(_261059, _261051), rline(_261049), -(rS(_261059, _261057, _261055)), rline(_261053), 1398 ^ _216680 : [(1399 ^ _216680) ^ [_261914] : [_261057 = _261914, rpoint(_261914)]], 1404 ^ _216680 : [(1405 ^ _216680) ^ [_262129] : [_261059 = _262129, rpoint(_262129)]]], (1413 ^ _216680) ^ [_262554, _262556, _262558, _262560, _262562, _262564, _262566, _262568] : [rS(_262564, _262562, _262556), ron(_262558, _262556), ron(_262560, _262556), _262556 = _262554, rline(_262554), rcenter(_262558, _262566), rcenter(_262560, _262568), -(_262564 = _262562), ron(_262562, _262566), ron(_262562, _262568), ron(_262564, _262566), ron(_262564, _262568), 1460 ^ _216680 : [(1461 ^ _216680) ^ [_263968] : [_262562 = _263968, rpoint(_263968)]], 1468 ^ _216680 : [(1469 ^ _216680) ^ [_264245] : [_262564 = _264245, rpoint(_264245)]], rintersect(_262568, _262566), -(_262568 = _262566), 1484 ^ _216680 : [(1485 ^ _216680) ^ [_264729] : [_262566 = _264729, rcircle(_264729)]], 1490 ^ _216680 : [(1491 ^ _216680) ^ [_264960] : [_262568 = _264960, rcircle(_264960)]]], (1499 ^ _216680) ^ [_265397, _265399, _265401, _265403, _265405] : [1544 ^ _216680 : [(1545 ^ _216680) ^ [] : [ron(_265403, _265399)], (1547 ^ _216680) ^ [] : [ron(_265403, _265399)]], rR(_265401, _265405, _265403), -(rinside(_265401, _265399)), 1510 ^ _216680 : [(1511 ^ _216680) ^ [] : [ron(_265405, _265399)], (1513 ^ _216680) ^ [] : [rinside(_265405, _265399)]], _265399 = _265397, rcircle(_265397), 1524 ^ _216680 : [(1525 ^ _216680) ^ [_266143] : [_265401 = _266143, rpoint(_266143)]], 1532 ^ _216680 : [(1533 ^ _216680) ^ [_266390] : [_265403 = _266390, rpoint(_266390)]], 1538 ^ _216680 : [(1539 ^ _216680) ^ [_266597] : [_265405 = _266597, rpoint(_266597)]]], (1549 ^ _216680) ^ [_267069, _267071, _267073, _267075, _267077, _267079, _267081] : [-(rinside(_267077, _267071)), rR(_267077, _267081, _267079), 1556 ^ _216680 : [(1557 ^ _216680) ^ [] : [ron(_267079, _267071)], (1559 ^ _216680) ^ [] : [rinside(_267079, _267071)]], 1562 ^ _216680 : [(1563 ^ _216680) ^ [] : [ron(_267081, _267071)], (1565 ^ _216680) ^ [] : [rinside(_267081, _267071)]], _267071 = _267069, rcircle(_267069), _267075 = _267073, rline(_267073), 1584 ^ _216680 : [(1585 ^ _216680) ^ [_268145] : [_267077 = _268145, rpoint(_268145)]], 1592 ^ _216680 : [(1593 ^ _216680) ^ [_268412] : [_267079 = _268412, rpoint(_268412)]], 1598 ^ _216680 : [(1599 ^ _216680) ^ [_268635] : [_267081 = _268635, rpoint(_268635)]]], (1607 ^ _216680) ^ [_269063, _269065, _269067, _269069, _269071, _269073, _269075] : [-(rR(_269075, _269073, _269071)), -(_269073 = _269071), ron(_269071, _269065), ron(_269073, _269065), rinside(_269075, _269065), ron(_269071, _269069), ron(_269073, _269069), ron(_269075, _269069), _269065 = _269063, rcircle(_269063), _269069 = _269067, rline(_269067), 1654 ^ _216680 : [(1655 ^ _216680) ^ [_270395] : [_269071 = _270395, rpoint(_270395)]], 1662 ^ _216680 : [(1663 ^ _216680) ^ [_270662] : [_269073 = _270662, rpoint(_270662)]], 1668 ^ _216680 : [(1669 ^ _216680) ^ [_270885] : [_269075 = _270885, rpoint(_270885)]]], (1677 ^ _216680) ^ [_271342, _271344, _271346, _271348, _271350, _271352, _271354, _271356] : [-(rS(_271346, _271342, _271356)), rS(_271346, _271342, _271352), rS(_271344, _271342, _271354), rS(_271348, _271346, _271352), rS(_271346, _271344, _271356), ron(_271344, _271352), ron(_271346, _271354), ron(_271348, _271356), ron(_271350, _271352), ron(_271350, _271354), ron(_271350, _271356), 1720 ^ _216680 : [(1721 ^ _216680) ^ [_272686] : [_271344 = _272686, rpoint(_272686)]], 1728 ^ _216680 : [(1729 ^ _216680) ^ [_272963] : [_271346 = _272963, rpoint(_272963)]], 1736 ^ _216680 : [(1737 ^ _216680) ^ [_273240] : [_271348 = _273240, rpoint(_273240)]], 1744 ^ _216680 : [(1745 ^ _216680) ^ [_273517] : [_271350 = _273517, rpoint(_273517)]], 1752 ^ _216680 : [(1753 ^ _216680) ^ [_273794] : [_271352 = _273794, rline(_273794)]], 1760 ^ _216680 : [(1761 ^ _216680) ^ [_274071] : [_271354 = _274071, rline(_274071)]], 1766 ^ _216680 : [(1767 ^ _216680) ^ [_274302] : [_271356 = _274302, rline(_274302)]]], (1775 ^ _216680) ^ [_274771, _274773, _274775, _274777, _274779, _274781, _274783] : [-(rS(_274775, _274773, _274779)), -(_274775 = _274777), -(ron(_274771, _274781)), -(rS(_274775, _274771, _274781)), rS(_274773, _274771, _274783), ron(_274771, _274779), ron(_274773, _274781), ron(_274775, _274783), ron(_274777, _274779), ron(_274777, _274781), ron(_274777, _274783), 1818 ^ _216680 : [(1819 ^ _216680) ^ [_276076] : [_274771 = _276076, rpoint(_276076)]], 1826 ^ _216680 : [(1827 ^ _216680) ^ [_276343] : [_274773 = _276343, rpoint(_276343)]], 1834 ^ _216680 : [(1835 ^ _216680) ^ [_276610] : [_274775 = _276610, rpoint(_276610)]], 1842 ^ _216680 : [(1843 ^ _216680) ^ [_276877] : [_274777 = _276877, rpoint(_276877)]], 1850 ^ _216680 : [(1851 ^ _216680) ^ [_277144] : [_274779 = _277144, rline(_277144)]], 1858 ^ _216680 : [(1859 ^ _216680) ^ [_277411] : [_274781 = _277411, rline(_277411)]], 1864 ^ _216680 : [(1865 ^ _216680) ^ [_277634] : [_274783 = _277634, rline(_277634)]]], (1873 ^ _216680) ^ [_278093, _278095, _278097, _278099, _278101, _278103, _278105] : [rS(_278097, _278093, _278103), rS(_278097, _278095, _278101), rS(_278095, _278093, _278105), ron(_278093, _278101), ron(_278095, _278101), ron(_278097, _278105), ron(_278099, _278101), ron(_278099, _278103), ron(_278099, _278105), 1908 ^ _216680 : [(1909 ^ _216680) ^ [_279181] : [_278093 = _279181, rpoint(_279181)]], 1916 ^ _216680 : [(1917 ^ _216680) ^ [_279448] : [_278095 = _279448, rpoint(_279448)]], 1924 ^ _216680 : [(1925 ^ _216680) ^ [_279715] : [_278097 = _279715, rpoint(_279715)]], 1932 ^ _216680 : [(1933 ^ _216680) ^ [_279982] : [_278099 = _279982, rpoint(_279982)]], 1940 ^ _216680 : [(1941 ^ _216680) ^ [_280249] : [_278101 = _280249, rline(_280249)]], 1948 ^ _216680 : [(1949 ^ _216680) ^ [_280516] : [_278103 = _280516, rline(_280516)]], 1954 ^ _216680 : [(1955 ^ _216680) ^ [_280739] : [_278105 = _280739, rline(_280739)]]], (1963 ^ _216680) ^ [_281161, _281163, _281165, _281167, _281169] : [-(rR(_281167, _281169, _281165)), ron(_281167, _281163), ron(_281167, _281161), -(rS(_281169, _281165, _281163)), ron(_281165, _281161), ron(_281169, _281161), -(_281163 = _281161), 1990 ^ _216680 : [(1991 ^ _216680) ^ [_281977] : [_281161 = _281977, rline(_281977)]], 1998 ^ _216680 : [(1999 ^ _216680) ^ [_282224] : [_281163 = _282224, rline(_282224)]], -(_281167 = _281165), -(_281169 = _281165), -(_281169 = _281167), 2018 ^ _216680 : [(2019 ^ _216680) ^ [_282747] : [_281165 = _282747, rpoint(_282747)]], 2026 ^ _216680 : [(2027 ^ _216680) ^ [_282994] : [_281167 = _282994, rpoint(_282994)]], 2032 ^ _216680 : [(2033 ^ _216680) ^ [_283201] : [_281169 = _283201, rpoint(_283201)]]], (2041 ^ _216680) ^ [_283598, _283600, _283602, _283604, _283606] : [rS(_283606, _283602, _283600), ron(_283604, _283600), rR(_283604, _283606, _283602), _283600 = _283598, rline(_283598), 2060 ^ _216680 : [(2061 ^ _216680) ^ [_284158] : [_283602 = _284158, rpoint(_284158)]], 2068 ^ _216680 : [(2069 ^ _216680) ^ [_284405] : [_283604 = _284405, rpoint(_284405)]], 2074 ^ _216680 : [(2075 ^ _216680) ^ [_284612] : [_283606 = _284612, rpoint(_284612)]]], (2083 ^ _216680) ^ [_284978, _284980, _284982, _284984, _284986] : [-(rS(_284984, _284982, _284980)), -(ron(_284984, _284980)), ron(_284986, _284980), rR(_284984, _284986, _284982), _284980 = _284978, rline(_284978), 2106 ^ _216680 : [(2107 ^ _216680) ^ [_285636] : [_284982 = _285636, rpoint(_285636)]], 2114 ^ _216680 : [(2115 ^ _216680) ^ [_285883] : [_284984 = _285883, rpoint(_285883)]], 2120 ^ _216680 : [(2121 ^ _216680) ^ [_286090] : [_284986 = _286090, rpoint(_286090)]]], (2129 ^ _216680) ^ [_286461, _286463, _286465, _286467, _286469] : [-(rS(_286469, _286467, _286463)), rS(_286469, _286465, _286463), rR(_286467, _286469, _286465), _286463 = _286461, rline(_286461), 2148 ^ _216680 : [(2149 ^ _216680) ^ [_287021] : [_286465 = _287021, rpoint(_287021)]], 2156 ^ _216680 : [(2157 ^ _216680) ^ [_287268] : [_286467 = _287268, rpoint(_287268)]], 2162 ^ _216680 : [(2163 ^ _216680) ^ [_287475] : [_286469 = _287475, rpoint(_287475)]]], (2171 ^ _216680) ^ [_287842, _287844, _287846, _287848, _287850] : [-(rS(_287850, _287846, _287844)), -(rS(_287848, _287846, _287844)), -(rS(_287850, _287848, _287844)), -(ron(_287846, _287844)), -(ron(_287848, _287844)), -(ron(_287850, _287844)), _287844 = _287842, rline(_287842), 2198 ^ _216680 : [(2199 ^ _216680) ^ [_288613] : [_287846 = _288613, rpoint(_288613)]], 2206 ^ _216680 : [(2207 ^ _216680) ^ [_288860] : [_287848 = _288860, rpoint(_288860)]], 2212 ^ _216680 : [(2213 ^ _216680) ^ [_289067] : [_287850 = _289067, rpoint(_289067)]]], (2225 ^ _216680) ^ [_289541, _289543, _289545, _289547, _289549] : [-(rS(_289547, _289545, _289543)), rS(_289549, _289545, _289543), rS(_289549, _289547, _289543), _289543 = _289541, rline(_289541), 2244 ^ _216680 : [(2245 ^ _216680) ^ [_290101] : [_289545 = _290101, rpoint(_290101)]], 2252 ^ _216680 : [(2253 ^ _216680) ^ [_290348] : [_289547 = _290348, rpoint(_290348)]], 2258 ^ _216680 : [(2259 ^ _216680) ^ [_290555] : [_289549 = _290555, rpoint(_290555)]]], (2267 ^ _216680) ^ [_290908, _290910, _290912, _290914] : [ron(_290914, _290910), rS(_290914, _290912, _290910), _290910 = _290908, rline(_290908), 2282 ^ _216680 : [(2283 ^ _216680) ^ [_291338] : [_290912 = _291338, rpoint(_291338)]], 2288 ^ _216680 : [(2289 ^ _216680) ^ [_291537] : [_290914 = _291537, rpoint(_291537)]]], (2297 ^ _216680) ^ [_291869, _291871, _291873, _291875] : [-(rS(_291873, _291875, _291871)), rS(_291875, _291873, _291871), _291871 = _291869, rline(_291869), 2312 ^ _216680 : [(2313 ^ _216680) ^ [_292298] : [_291873 = _292298, rpoint(_292298)]], 2318 ^ _216680 : [(2319 ^ _216680) ^ [_292497] : [_291875 = _292497, rpoint(_292497)]]], (2327 ^ _216680) ^ [_292831, _292833, _292835, _292837] : [-(rS(_292837, _292837, _292833)), -(ron(_292837, _292833)), _292833 = _292831, rline(_292831), _292837 = _292835, rpoint(_292835)], (2349 ^ _216680) ^ [_293470, _293472, _293474, _293476] : [rR(_293474, _293472, _293470), rR(_293474, _293476, _293470), rR(_293474, _293476, _293472), 2360 ^ _216680 : [(2361 ^ _216680) ^ [_293844] : [_293470 = _293844, rpoint(_293844)]], 2368 ^ _216680 : [(2369 ^ _216680) ^ [_294081] : [_293472 = _294081, rpoint(_294081)]], 2376 ^ _216680 : [(2377 ^ _216680) ^ [_294318] : [_293474 = _294318, rpoint(_294318)]], 2382 ^ _216680 : [(2383 ^ _216680) ^ [_294517] : [_293476 = _294517, rpoint(_294517)]]], (2391 ^ _216680) ^ [_294870, _294872, _294874, _294876, _294878] : [-(rR(_294876, _294878, _294874)), -(rR(_294878, _294876, _294874)), -(rR(_294874, _294878, _294876)), _294872 = _294870, ron(_294874, _294872), ron(_294876, _294872), ron(_294878, _294872), rline(_294870), -(_294876 = _294874), -(_294878 = _294874), -(_294878 = _294876), 2426 ^ _216680 : [(2427 ^ _216680) ^ [_295837] : [_294874 = _295837, rpoint(_295837)]], 2434 ^ _216680 : [(2435 ^ _216680) ^ [_296084] : [_294876 = _296084, rpoint(_296084)]], 2440 ^ _216680 : [(2441 ^ _216680) ^ [_296291] : [_294878 = _296291, rpoint(_296291)]]], (2457 ^ _216680) ^ [_296858, _296860, _296862, _296864] : [-(rR(_296862, _296864, _296858)), rR(_296860, _296862, _296858), rR(_296862, _296864, _296860), 2468 ^ _216680 : [(2469 ^ _216680) ^ [_297230] : [_296858 = _297230, rpoint(_297230)]], 2476 ^ _216680 : [(2477 ^ _216680) ^ [_297467] : [_296860 = _297467, rpoint(_297467)]], 2484 ^ _216680 : [(2485 ^ _216680) ^ [_297704] : [_296862 = _297704, rpoint(_297704)]], 2490 ^ _216680 : [(2491 ^ _216680) ^ [_297903] : [_296864 = _297903, rpoint(_297903)]]], (2499 ^ _216680) ^ [_298243, _298245, _298247, _298249] : [-(rR(_298243, _298249, _298245)), rR(_298243, _298249, _298247), rR(_298247, _298249, _298245), 2510 ^ _216680 : [(2511 ^ _216680) ^ [_298615] : [_298243 = _298615, rpoint(_298615)]], 2518 ^ _216680 : [(2519 ^ _216680) ^ [_298852] : [_298245 = _298852, rpoint(_298852)]], 2526 ^ _216680 : [(2527 ^ _216680) ^ [_299089] : [_298247 = _299089, rpoint(_299089)]], 2532 ^ _216680 : [(2533 ^ _216680) ^ [_299288] : [_298249 = _299288, rpoint(_299288)]]], (2541 ^ _216680) ^ [_299642, _299644, _299646, _299648, _299650] : [-(ron(_299648, _299644)), _299644 = _299642, ron(_299646, _299644), ron(_299650, _299644), rR(_299648, _299650, _299646), rline(_299642), 2564 ^ _216680 : [(2565 ^ _216680) ^ [_300296] : [_299646 = _300296, rpoint(_300296)]], 2572 ^ _216680 : [(2573 ^ _216680) ^ [_300543] : [_299648 = _300543, rpoint(_300543)]], 2578 ^ _216680 : [(2579 ^ _216680) ^ [_300750] : [_299650 = _300750, rpoint(_300750)]]], (2587 ^ _216680) ^ [_301120, _301122, _301124, _301126, _301128] : [-(ron(_301124, _301122)), _301122 = _301120, ron(_301126, _301122), ron(_301128, _301122), rR(_301126, _301128, _301124), rline(_301120), 2610 ^ _216680 : [(2611 ^ _216680) ^ [_301774] : [_301124 = _301774, rpoint(_301774)]], 2618 ^ _216680 : [(2619 ^ _216680) ^ [_302021] : [_301126 = _302021, rpoint(_302021)]], 2624 ^ _216680 : [(2625 ^ _216680) ^ [_302228] : [_301128 = _302228, rpoint(_302228)]]], (2633 ^ _216680) ^ [_302570, _302572, _302574] : [2660 ^ _216680 : [(2661 ^ _216680) ^ [] : [rR(_302574, _302572, _302570)], (2663 ^ _216680) ^ [] : [_302574 = _302570], (2665 ^ _216680) ^ [] : [_302574 = _302572], (2667 ^ _216680) ^ [] : [-(rR(_302572, _302570, _302574))]], rR(_302572, _302574, _302570), 2640 ^ _216680 : [(2641 ^ _216680) ^ [_302848] : [_302570 = _302848, rpoint(_302848)]], 2648 ^ _216680 : [(2649 ^ _216680) ^ [_303075] : [_302572 = _303075, rpoint(_303075)]], 2654 ^ _216680 : [(2655 ^ _216680) ^ [_303266] : [_302574 = _303266, rpoint(_303266)]]], (2669 ^ _216680) ^ [_303796, _303798, _303800, _303802] : [ron(_303802, _303798), rinside(_303802, _303798), _303798 = _303796, rcircle(_303796), _303802 = _303800, rpoint(_303800)], (2691 ^ _216680) ^ [_304403, _304405] : [rcenter(_304405, _304403), -(rinside(_304405, _304403))], (2697 ^ _216680) ^ [_304641, _304643, _304645, _304647] : [-(_304643 = _304641), rcenter(_304641, _304647), rcenter(_304643, _304647), _304647 = _304645, rcircle(_304645)], (2715 ^ _216680) ^ [_305180, _305182, _305184, _305186] : [-(_305182 = _305180), ron(_305184, _305180), ron(_305184, _305182), ron(_305186, _305180), ron(_305186, _305182), 2734 ^ _216680 : [(2735 ^ _216680) ^ [_305741] : [_305180 = _305741, rline(_305741)]], 2742 ^ _216680 : [(2743 ^ _216680) ^ [_305978] : [_305182 = _305978, rline(_305978)]], -(_305186 = _305184), 2754 ^ _216680 : [(2755 ^ _216680) ^ [_306303] : [_305184 = _306303, rpoint(_306303)]], 2760 ^ _216680 : [(2761 ^ _216680) ^ [_306502] : [_305186 = _306502, rpoint(_306502)]]], (2769 ^ _216680) ^ [_306895, _306897, _306899, _306901, _306903, _306905, _306907] : [2817 ^ _216680 : [(2818 ^ _216680) ^ [] : [rS(2816 ^ [_306895, _306897, _306899, _306901, _306903, _306905, _306907], _306895, _306903)], (2820 ^ _216680) ^ [] : [-(ron(2816 ^ [_306895, _306897, _306899, _306901, _306903, _306905, _306907], _306905))], (2822 ^ _216680) ^ [] : [-(ron(2816 ^ [_306895, _306897, _306899, _306901, _306903, _306905, _306907], _306907))], (2824 ^ _216680) ^ [] : [-(rpoint(2816 ^ [_306895, _306897, _306899, _306901, _306903, _306905, _306907]))]], -(ron(_306895, _306903)), ron(_306897, _306903), ron(_306899, _306903), rcenter(_306897, _306905), rcenter(_306899, _306907), rintersect(_306907, _306905), _306903 = _306901, rline(_306901), 2804 ^ _216680 : [(2805 ^ _216680) ^ [_307922] : [_306905 = _307922, rcircle(_307922)]], 2810 ^ _216680 : [(2811 ^ _216680) ^ [_308145] : [_306907 = _308145, rcircle(_308145)]]], (2826 ^ _216680) ^ [_308957, _308959, _308961, _308963, _308965, _308967, _308969] : [2874 ^ _216680 : [(2875 ^ _216680) ^ [] : [-(rS(2873 ^ [_308957, _308959, _308961, _308963, _308965, _308967, _308969], _308957, _308965))], (2877 ^ _216680) ^ [] : [-(ron(2873 ^ [_308957, _308959, _308961, _308963, _308965, _308967, _308969], _308967))], (2879 ^ _216680) ^ [] : [-(ron(2873 ^ [_308957, _308959, _308961, _308963, _308965, _308967, _308969], _308969))], (2881 ^ _216680) ^ [] : [-(rpoint(2873 ^ [_308957, _308959, _308961, _308963, _308965, _308967, _308969]))]], -(ron(_308957, _308965)), ron(_308959, _308965), ron(_308961, _308965), rcenter(_308959, _308967), rcenter(_308961, _308969), rintersect(_308969, _308967), _308965 = _308963, rline(_308963), 2861 ^ _216680 : [(2862 ^ _216680) ^ [_309982] : [_308967 = _309982, rcircle(_309982)]], 2867 ^ _216680 : [(2868 ^ _216680) ^ [_310205] : [_308969 = _310205, rcircle(_310205)]]], (2883 ^ _216680) ^ [_310946, _310948] : [2904 ^ _216680 : [(2905 ^ _216680) ^ [] : [2902 ^ [_310946, _310948] = 2903 ^ [_310946, _310948]], (2907 ^ _216680) ^ [] : [-(ron(2903 ^ [_310946, _310948], _310946))], (2909 ^ _216680) ^ [] : [-(ron(2903 ^ [_310946, _310948], _310948))], (2911 ^ _216680) ^ [] : [-(rpoint(2903 ^ [_310946, _310948]))], (2913 ^ _216680) ^ [] : [-(ron(2902 ^ [_310946, _310948], _310946))], (2915 ^ _216680) ^ [] : [-(ron(2902 ^ [_310946, _310948], _310948))], (2917 ^ _216680) ^ [] : [-(rpoint(2902 ^ [_310946, _310948]))]], rintersect(_310948, _310946), 2890 ^ _216680 : [(2891 ^ _216680) ^ [_311218] : [_310946 = _311218, rcircle(_311218)]], 2896 ^ _216680 : [(2897 ^ _216680) ^ [_311401] : [_310948 = _311401, rcircle(_311401)]]], (2919 ^ _216680) ^ [_312363, _312365, _312367, _312369] : [2939 ^ _216680 : [(2940 ^ _216680) ^ [] : [-(ron(2938 ^ [_312363, _312365, _312367, _312369], _312365))], (2942 ^ _216680) ^ [] : [-(ron(2938 ^ [_312363, _312365, _312367, _312369], _312369))], (2944 ^ _216680) ^ [] : [-(rpoint(2938 ^ [_312363, _312365, _312367, _312369]))]], rintersect(_312369, _312365), _312365 = _312363, rcircle(_312363), _312369 = _312367, rcircle(_312367)], (2946 ^ _216680) ^ [_313310, _313312, _313314, _313316, _313318, _313320, _313322, _313324] : [2994 ^ _216680 : [(2995 ^ _216680) ^ [] : [-(rR(_313316, 2993 ^ [_313310, _313312, _313314, _313316, _313318, _313320, _313322, _313324], _313312))], (2997 ^ _216680) ^ [] : [-(ron(2993 ^ [_313310, _313312, _313314, _313316, _313318, _313320, _313322, _313324], _313320))], (2999 ^ _216680) ^ [] : [-(ron(2993 ^ [_313310, _313312, _313314, _313316, _313318, _313320, _313322, _313324], _313324))], (3001 ^ _216680) ^ [] : [-(rpoint(2993 ^ [_313310, _313312, _313314, _313316, _313318, _313320, _313322, _313324]))]], -(_313312 = _313316), ron(_313312, _313320), _313312 = _313310, rpoint(_313310), ron(_313316, _313320), rinside(_313316, _313324), _313316 = _313314, rpoint(_313314), _313320 = _313318, rline(_313318), _313324 = _313322, rcircle(_313322)], (3003 ^ _216680) ^ [_315249, _315251, _315253, _315255] : [3023 ^ _216680 : [(3024 ^ _216680) ^ [] : [-(ron(3022 ^ [_315249, _315251, _315253, _315255], _315255))], (3026 ^ _216680) ^ [] : [-(ron(3022 ^ [_315249, _315251, _315253, _315255], _315251))], (3028 ^ _216680) ^ [] : [-(rpoint(3022 ^ [_315249, _315251, _315253, _315255]))]], rintersect(_315251, _315255), _315251 = _315249, rline(_315249), _315255 = _315253, rcircle(_315253)], (3030 ^ _216680) ^ [_316140, _316142, _316144, _316146] : [3050 ^ _216680 : [(3051 ^ _216680) ^ [] : [-(ron(3049 ^ [_316140, _316142, _316144, _316146], _316142))], (3053 ^ _216680) ^ [] : [-(ron(3049 ^ [_316140, _316142, _316144, _316146], _316146))], (3055 ^ _216680) ^ [] : [-(rpoint(3049 ^ [_316140, _316142, _316144, _316146]))]], rintersect(_316146, _316142), _316142 = _316140, rline(_316140), _316146 = _316144, rline(_316144)], (3057 ^ _216680) ^ [_317003, _317005] : [3065 ^ _216680 : [(3066 ^ _216680) ^ [] : [ron(3064 ^ [_317003, _317005], _317005)], (3068 ^ _216680) ^ [] : [rinside(3064 ^ [_317003, _317005], _317005)], (3070 ^ _216680) ^ [] : [-(rpoint(3064 ^ [_317003, _317005]))]], _317005 = _317003, rcircle(_317003)], (3072 ^ _216680) ^ [_317535, _317537] : [3080 ^ _216680 : [(3081 ^ _216680) ^ [] : [-(rinside(3079 ^ [_317535, _317537], _317537))], (3083 ^ _216680) ^ [] : [-(rpoint(3079 ^ [_317535, _317537]))]], _317537 = _317535, rcircle(_317535)], (3085 ^ _216680) ^ [_318002, _318004, _318006, _318008] : [3117 ^ _216680 : [(3118 ^ _216680) ^ [] : [3116 ^ [_318002, _318004, _318006, _318008] = _318002], (3120 ^ _216680) ^ [] : [3116 ^ [_318002, _318004, _318006, _318008] = _318004], (3122 ^ _216680) ^ [] : [-(ron(3116 ^ [_318002, _318004, _318006, _318008], _318008))], (3124 ^ _216680) ^ [] : [-(rpoint(3116 ^ [_318002, _318004, _318006, _318008]))]], ron(_318002, _318008), ron(_318004, _318008), 3096 ^ _216680 : [(3097 ^ _216680) ^ [_318374] : [_318002 = _318374, rpoint(_318374)]], 3104 ^ _216680 : [(3105 ^ _216680) ^ [_318611] : [_318004 = _318611, rpoint(_318611)]], _318008 = _318006, rcircle(_318006)], (3126 ^ _216680) ^ [_319415, _319417, _319419, _319421] : [3146 ^ _216680 : [(3147 ^ _216680) ^ [] : [3145 ^ [_319415, _319417, _319419, _319421] = _319417], (3149 ^ _216680) ^ [] : [-(ron(3145 ^ [_319415, _319417, _319419, _319421], _319421))], (3151 ^ _216680) ^ [] : [-(rpoint(3145 ^ [_319415, _319417, _319419, _319421]))]], ron(_319417, _319421), _319417 = _319415, rpoint(_319415), _319421 = _319419, rcircle(_319419)], (3153 ^ _216680) ^ [_320281, _320283] : [3161 ^ _216680 : [(3162 ^ _216680) ^ [] : [-(ron(3160 ^ [_320281, _320283], _320283))], (3164 ^ _216680) ^ [] : [-(rpoint(3160 ^ [_320281, _320283]))]], _320283 = _320281, rcircle(_320281)], (3166 ^ _216680) ^ [_320748, _320750, _320752, _320754] : [3186 ^ _216680 : [(3187 ^ _216680) ^ [] : [rS(3185 ^ [_320748, _320750, _320752, _320754], _320750, _320754)], (3189 ^ _216680) ^ [] : [-(rpoint(3185 ^ [_320748, _320750, _320752, _320754]))]], _320750 = _320748, -(ron(_320750, _320754)), rpoint(_320748), _320754 = _320752, rline(_320752)], (3191 ^ _216680) ^ [_321609, _321611, _321613, _321615, _321617, _321619, _321621, _321623] : [3235 ^ _216680 : [(3236 ^ _216680) ^ [] : [3234 ^ [_321609, _321611, _321613, _321615, _321617, _321619, _321621, _321623] = _321611], (3238 ^ _216680) ^ [] : [3234 ^ [_321609, _321611, _321613, _321615, _321617, _321619, _321621, _321623] = _321615], (3240 ^ _216680) ^ [] : [3234 ^ [_321609, _321611, _321613, _321615, _321617, _321619, _321621, _321623] = _321619], (3242 ^ _216680) ^ [] : [-(rS(3234 ^ [_321609, _321611, _321613, _321615, _321617, _321619, _321621, _321623], _321619, _321623))], (3244 ^ _216680) ^ [] : [-(rpoint(3234 ^ [_321609, _321611, _321613, _321615, _321617, _321619, _321621, _321623]))]], _321619 = _321617, _321615 = _321613, _321611 = _321609, rS(_321611, _321619, _321623), rpoint(_321609), rS(_321615, _321619, _321623), rpoint(_321613), -(ron(_321619, _321623)), rpoint(_321617), _321623 = _321621, rline(_321621)], (3246 ^ _216680) ^ [_323587, _323589, _323591, _323593, _323595, _323597] : [3278 ^ _216680 : [(3279 ^ _216680) ^ [] : [3277 ^ [_323587, _323589, _323591, _323593, _323595, _323597] = _323589], (3281 ^ _216680) ^ [] : [3277 ^ [_323587, _323589, _323591, _323593, _323595, _323597] = _323593], (3283 ^ _216680) ^ [] : [-(rS(3277 ^ [_323587, _323589, _323591, _323593, _323595, _323597], _323593, _323597))], (3285 ^ _216680) ^ [] : [-(rpoint(3277 ^ [_323587, _323589, _323591, _323593, _323595, _323597]))]], _323593 = _323591, _323589 = _323587, rS(_323589, _323593, _323597), rpoint(_323587), -(ron(_323593, _323597)), rpoint(_323591), _323597 = _323595, rline(_323595)], (3287 ^ _216680) ^ [_324980, _324982, _324984, _324986] : [3307 ^ _216680 : [(3308 ^ _216680) ^ [] : [3306 ^ [_324980, _324982, _324984, _324986] = _324982], (3310 ^ _216680) ^ [] : [-(rS(3306 ^ [_324980, _324982, _324984, _324986], _324982, _324986))], (3312 ^ _216680) ^ [] : [-(rpoint(3306 ^ [_324980, _324982, _324984, _324986]))]], _324982 = _324980, -(ron(_324982, _324986)), rpoint(_324980), _324986 = _324984, rline(_324984)], (3314 ^ _216680) ^ [_325908, _325910, _325912, _325914, _325916, _325918] : [3358 ^ _216680 : [(3359 ^ _216680) ^ [] : [3357 ^ [_325908, _325910, _325912, _325914, _325916, _325918] = _325910], (3361 ^ _216680) ^ [] : [-(rR(_325912, _325914, 3357 ^ [_325908, _325910, _325912, _325914, _325916, _325918]))], (3363 ^ _216680) ^ [] : [-(rpoint(3357 ^ [_325908, _325910, _325912, _325914, _325916, _325918]))]], _325910 = _325908, rR(_325912, _325914, _325910), rpoint(_325908), ron(_325912, _325918), ron(_325914, _325918), 3337 ^ _216680 : [(3338 ^ _216680) ^ [_326600] : [_325912 = _326600, rpoint(_326600)]], 3345 ^ _216680 : [(3346 ^ _216680) ^ [_326857] : [_325914 = _326857, rpoint(_326857)]], _325918 = _325916, rline(_325916)], (3365 ^ _216680) ^ [_327645, _327647, _327649, _327651] : [3401 ^ _216680 : [(3402 ^ _216680) ^ [] : [-(rR(_327645, _327647, 3400 ^ [_327645, _327647, _327649, _327651]))], (3404 ^ _216680) ^ [] : [-(rpoint(3400 ^ [_327645, _327647, _327649, _327651]))]], -(_327647 = _327645), ron(_327645, _327651), ron(_327647, _327651), 3380 ^ _216680 : [(3381 ^ _216680) ^ [_328098] : [_327645 = _328098, rpoint(_328098)]], 3388 ^ _216680 : [(3389 ^ _216680) ^ [_328335] : [_327647 = _328335, rpoint(_328335)]], _327651 = _327649, rline(_327649)], (3406 ^ _216680) ^ [_328993, _328995, _328997, _328999, _329001, _329003] : [3466 ^ _216680 : [(3467 ^ _216680) ^ [] : [3465 ^ [_328993, _328995, _328997, _328999, _329001, _329003] = _328993], (3469 ^ _216680) ^ [] : [3465 ^ [_328993, _328995, _328997, _328999, _329001, _329003] = _328995], (3471 ^ _216680) ^ [] : [-(rR(3465 ^ [_328993, _328995, _328997, _328999, _329001, _329003], _328999, _328997))], (3473 ^ _216680) ^ [] : [-(rpoint(3465 ^ [_328993, _328995, _328997, _328999, _329001, _329003]))]], rR(_328993, _328999, _328997), rR(_328995, _328999, _328997), ron(_328995, _329003), ron(_328997, _329003), ron(_328999, _329003), 3429 ^ _216680 : [(3430 ^ _216680) ^ [_329729] : [_328993 = _329729, rpoint(_329729)]], 3437 ^ _216680 : [(3438 ^ _216680) ^ [_329986] : [_328995 = _329986, rpoint(_329986)]], 3445 ^ _216680 : [(3446 ^ _216680) ^ [_330243] : [_328997 = _330243, rpoint(_330243)]], 3453 ^ _216680 : [(3454 ^ _216680) ^ [_330500] : [_328999 = _330500, rpoint(_330500)]], _329003 = _329001, rline(_329001)], (3475 ^ _216680) ^ [_331410, _331412, _331414, _331416, _331418] : [3519 ^ _216680 : [(3520 ^ _216680) ^ [] : [3518 ^ [_331410, _331412, _331414, _331416, _331418] = _331410], (3522 ^ _216680) ^ [] : [-(rR(3518 ^ [_331410, _331412, _331414, _331416, _331418], _331414, _331412))], (3524 ^ _216680) ^ [] : [-(rpoint(3518 ^ [_331410, _331412, _331414, _331416, _331418]))]], rR(_331410, _331414, _331412), ron(_331412, _331418), ron(_331414, _331418), 3490 ^ _216680 : [(3491 ^ _216680) ^ [_331902] : [_331410 = _331902, rpoint(_331902)]], 3498 ^ _216680 : [(3499 ^ _216680) ^ [_332149] : [_331412 = _332149, rpoint(_332149)]], 3506 ^ _216680 : [(3507 ^ _216680) ^ [_332396] : [_331414 = _332396, rpoint(_332396)]], _331418 = _331416, rline(_331416)], (3526 ^ _216680) ^ [_333151, _333153, _333155, _333157] : [3562 ^ _216680 : [(3563 ^ _216680) ^ [] : [-(rR(3561 ^ [_333151, _333153, _333155, _333157], _333153, _333151))], (3565 ^ _216680) ^ [] : [-(rpoint(3561 ^ [_333151, _333153, _333155, _333157]))]], -(_333153 = _333151), ron(_333151, _333157), ron(_333153, _333157), 3541 ^ _216680 : [(3542 ^ _216680) ^ [_333604] : [_333151 = _333604, rpoint(_333604)]], 3549 ^ _216680 : [(3550 ^ _216680) ^ [_333841] : [_333153 = _333841, rpoint(_333841)]], _333157 = _333155, rline(_333155)], (3567 ^ _216680) ^ [_334485, _334487, _334489, _334491, _334493] : [3611 ^ _216680 : [(3612 ^ _216680) ^ [] : [3610 ^ [_334485, _334487, _334489, _334491, _334493] = _334487], (3614 ^ _216680) ^ [] : [3610 ^ [_334485, _334487, _334489, _334491, _334493] = _334489], (3616 ^ _216680) ^ [] : [-(ron(3610 ^ [_334485, _334487, _334489, _334491, _334493], _334493))], (3618 ^ _216680) ^ [] : [-(rpoint(3610 ^ [_334485, _334487, _334489, _334491, _334493]))]], ron(_334485, _334493), ron(_334487, _334493), ron(_334489, _334493), 3582 ^ _216680 : [(3583 ^ _216680) ^ [_334982] : [_334485 = _334982, rpoint(_334982)]], 3590 ^ _216680 : [(3591 ^ _216680) ^ [_335229] : [_334487 = _335229, rpoint(_335229)]], 3598 ^ _216680 : [(3599 ^ _216680) ^ [_335476] : [_334489 = _335476, rpoint(_335476)]], _334493 = _334491, rline(_334491)], (3620 ^ _216680) ^ [_336351, _336353, _336355, _336357, _336359, _336361] : [3652 ^ _216680 : [(3653 ^ _216680) ^ [] : [3651 ^ [_336351, _336353, _336355, _336357, _336359, _336361] = _336353], (3655 ^ _216680) ^ [] : [3651 ^ [_336351, _336353, _336355, _336357, _336359, _336361] = _336357], (3657 ^ _216680) ^ [] : [-(ron(3651 ^ [_336351, _336353, _336355, _336357, _336359, _336361], _336361))], (3659 ^ _216680) ^ [] : [-(rpoint(3651 ^ [_336351, _336353, _336355, _336357, _336359, _336361]))]], ron(_336353, _336361), ron(_336357, _336361), _336353 = _336351, rpoint(_336351), _336357 = _336355, rpoint(_336355), _336361 = _336359, rline(_336359)], (3661 ^ _216680) ^ [_337736, _337738, _337740, _337742] : [3681 ^ _216680 : [(3682 ^ _216680) ^ [] : [3680 ^ [_337736, _337738, _337740, _337742] = _337738], (3684 ^ _216680) ^ [] : [-(ron(3680 ^ [_337736, _337738, _337740, _337742], _337742))], (3686 ^ _216680) ^ [] : [-(rpoint(3680 ^ [_337736, _337738, _337740, _337742]))]], ron(_337738, _337742), _337738 = _337736, rpoint(_337736), _337742 = _337740, rline(_337740)], (3688 ^ _216680) ^ [_338602, _338604] : [3696 ^ _216680 : [(3697 ^ _216680) ^ [] : [-(ron(3695 ^ [_338602, _338604], _338604))], (3699 ^ _216680) ^ [] : [-(rpoint(3695 ^ [_338602, _338604]))]], _338604 = _338602, rline(_338602)], (3701 ^ _216680) ^ [_339069, _339071, _339073, _339075] : [3733 ^ _216680 : [(3734 ^ _216680) ^ [] : [3732 ^ [_339069, _339071, _339073, _339075] = _339069], (3736 ^ _216680) ^ [] : [3732 ^ [_339069, _339071, _339073, _339075] = _339071], (3738 ^ _216680) ^ [] : [3732 ^ [_339069, _339071, _339073, _339075] = _339073], (3740 ^ _216680) ^ [] : [3732 ^ [_339069, _339071, _339073, _339075] = _339075], (3742 ^ _216680) ^ [] : [-(rpoint(3732 ^ [_339069, _339071, _339073, _339075]))]], 3704 ^ _216680 : [(3705 ^ _216680) ^ [_339286] : [_339069 = _339286, rpoint(_339286)]], 3712 ^ _216680 : [(3713 ^ _216680) ^ [_339523] : [_339071 = _339523, rpoint(_339523)]], 3720 ^ _216680 : [(3721 ^ _216680) ^ [_339760] : [_339073 = _339760, rpoint(_339760)]], 3726 ^ _216680 : [(3727 ^ _216680) ^ [_339959] : [_339075 = _339959, rpoint(_339959)]]], (3744 ^ _216680) ^ [_340699, _340701, _340703] : [3768 ^ _216680 : [(3769 ^ _216680) ^ [] : [3767 ^ [_340699, _340701, _340703] = _340699], (3771 ^ _216680) ^ [] : [3767 ^ [_340699, _340701, _340703] = _340701], (3773 ^ _216680) ^ [] : [3767 ^ [_340699, _340701, _340703] = _340703], (3775 ^ _216680) ^ [] : [-(rpoint(3767 ^ [_340699, _340701, _340703]))]], 3747 ^ _216680 : [(3748 ^ _216680) ^ [_340888] : [_340699 = _340888, rpoint(_340888)]], 3755 ^ _216680 : [(3756 ^ _216680) ^ [_341115] : [_340701 = _341115, rpoint(_341115)]], 3761 ^ _216680 : [(3762 ^ _216680) ^ [_341306] : [_340703 = _341306, rpoint(_341306)]]], (3777 ^ _216680) ^ [_341909, _341911] : [3793 ^ _216680 : [(3794 ^ _216680) ^ [] : [3792 ^ [_341909, _341911] = _341909], (3796 ^ _216680) ^ [] : [3792 ^ [_341909, _341911] = _341911], (3798 ^ _216680) ^ [] : [-(rpoint(3792 ^ [_341909, _341911]))]], 3780 ^ _216680 : [(3781 ^ _216680) ^ [_342070] : [_341909 = _342070, rpoint(_342070)]], 3786 ^ _216680 : [(3787 ^ _216680) ^ [_342253] : [_341911 = _342253, rpoint(_342253)]]], (3800 ^ _216680) ^ [_342741, _342743] : [3808 ^ _216680 : [(3809 ^ _216680) ^ [] : [3807 ^ [_342741, _342743] = _342743], (3811 ^ _216680) ^ [] : [-(rpoint(3807 ^ [_342741, _342743]))]], _342743 = _342741, rpoint(_342741)], (3813 ^ _216680) ^ [] : [-(rpoint(vd14))], (3815 ^ _216680) ^ [_343264, _343266, _343268, _343270] : [3822 ^ _216680 : [(3823 ^ _216680) ^ [] : [_343268 = _343266], (3825 ^ _216680) ^ [] : [_343270 = _343266], (3827 ^ _216680) ^ [] : [_343270 = _343268], (3830 ^ _216680) ^ [] : [-(_343266 = 3828 ^ [_343264, _343266, _343268, _343270])], (3832 ^ _216680) ^ [] : [-(rpoint(3828 ^ [_343264, _343266, _343268, _343270]))], (3835 ^ _216680) ^ [] : [-(_343268 = 3833 ^ [_343264, _343266, _343268, _343270])], (3837 ^ _216680) ^ [] : [-(rpoint(3833 ^ [_343264, _343266, _343268, _343270]))], (3840 ^ _216680) ^ [] : [-(_343270 = 3838 ^ [_343264, _343266, _343268, _343270])], (3842 ^ _216680) ^ [] : [-(rpoint(3838 ^ [_343264, _343266, _343268, _343270]))]], vtriangle(_343270, _343268, _343266) = _343264, rtriangle(_343264)], (3844 ^ _216680) ^ [_344540, _344542, _344544, _344546, _344548, _344550, _344552] : [-(vangle(_344550, _344552, _344548) = vangle(_344546, _344552, _344544)), -(rR(_344552, _344548, _344544)), -(rR(_344552, _344550, _344546)), -(_344544 = _344552), -(_344546 = _344552), -(_344548 = _344552), -(_344550 = _344552), ron(_344544, _344540), ron(_344548, _344540), ron(_344546, _344542), ron(_344550, _344542), ron(_344552, _344542), 3891 ^ _216680 : [(3892 ^ _216680) ^ [_345966] : [_344540 = _345966, rline(_345966)]], 3899 ^ _216680 : [(3900 ^ _216680) ^ [_346233] : [_344542 = _346233, rline(_346233)]], 3907 ^ _216680 : [(3908 ^ _216680) ^ [_346500] : [_344544 = _346500, rpoint(_346500)]], 3915 ^ _216680 : [(3916 ^ _216680) ^ [_346767] : [_344546 = _346767, rpoint(_346767)]], 3923 ^ _216680 : [(3924 ^ _216680) ^ [_347034] : [_344548 = _347034, rpoint(_347034)]], 3931 ^ _216680 : [(3932 ^ _216680) ^ [_347301] : [_344550 = _347301, rpoint(_347301)]], 3937 ^ _216680 : [(3938 ^ _216680) ^ [_347524] : [_344552 = _347524, rpoint(_347524)]]], (3946 ^ _216680) ^ [_347938, _347940, _347942] : [-(vplus(vf(_347942, _347940), vf(_347940, _347938)) = vf(_347942, _347938)), rR(_347940, _347942, _347938), 3953 ^ _216680 : [(3954 ^ _216680) ^ [_348202] : [_347938 = _348202, rpoint(_348202)]], 3961 ^ _216680 : [(3962 ^ _216680) ^ [_348429] : [_347940 = _348429, rpoint(_348429)]], 3967 ^ _216680 : [(3968 ^ _216680) ^ [_348620] : [_347942 = _348620, rpoint(_348620)]]], (3976 ^ _216680) ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182] : [4172 ^ _216680 : [(4173 ^ _216680) ^ [] : [-(vangle(_349162, _349160, _349158) = vangle(_349156, _349154, _349152))], (4175 ^ _216680) ^ [] : [-(vf(_349170, _349168) = vf(_349166, _349164))]], _349150 = _349148, 3986 ^ _216680 : [(3987 ^ _216680) ^ [] : [-(rS(3985 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182], _349172, _349150))], (3989 ^ _216680) ^ [] : [rR(_349176, 3984 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182], _349174)], (3991 ^ _216680) ^ [] : [-(ron(3984 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182], _349150))], (3993 ^ _216680) ^ [] : [-(vf(_349182, _349178) = vf(3983 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182], 3985 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182]))], (3995 ^ _216680) ^ [] : [-(vf(_349180, _349178) = vf(3984 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182], 3985 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182]))], (3997 ^ _216680) ^ [] : [-(vf(_349182, _349180) = vf(3983 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182], 3984 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182]))], (3999 ^ _216680) ^ [] : [-(vangle(3983 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182], 3985 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182], 3984 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182]) = vangle(_349182, _349178, _349180))], (4001 ^ _216680) ^ [] : [-(vangle(3984 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182], 3983 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182], 3985 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182]) = vangle(_349180, _349182, _349178))], (4003 ^ _216680) ^ [] : [-(vangle(3985 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182], 3984 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182], 3983 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182]) = vangle(_349178, _349180, _349182))], (4005 ^ _216680) ^ [] : [-(3983 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182] = _349176)], (4007 ^ _216680) ^ [] : [-(rpoint(3985 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182]))], (4009 ^ _216680) ^ [] : [-(rpoint(3984 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182]))], (4011 ^ _216680) ^ [] : [-(rpoint(3983 ^ [_349148, _349150, _349152, _349154, _349156, _349158, _349160, _349162, _349164, _349166, _349168, _349170, _349172, _349174, _349176, _349178, _349180, _349182]))], (4013 ^ _216680) ^ [] : [vangle(_349162, _349160, _349158) = vangle(_349156, _349154, _349152), vf(_349170, _349168) = vf(_349166, _349164)]], -(ron(_349172, _349150)), ron(_349174, _349150), ron(_349176, _349150), rline(_349148), 4036 ^ _216680 : [(4037 ^ _216680) ^ [_354678] : [_349152 = _354678, rpoint(_354678)]], 4044 ^ _216680 : [(4045 ^ _216680) ^ [_355055] : [_349154 = _355055, rpoint(_355055)]], 4052 ^ _216680 : [(4053 ^ _216680) ^ [_355432] : [_349156 = _355432, rpoint(_355432)]], 4060 ^ _216680 : [(4061 ^ _216680) ^ [_355809] : [_349158 = _355809, rpoint(_355809)]], 4068 ^ _216680 : [(4069 ^ _216680) ^ [_356186] : [_349160 = _356186, rpoint(_356186)]], 4076 ^ _216680 : [(4077 ^ _216680) ^ [_356563] : [_349162 = _356563, rpoint(_356563)]], 4084 ^ _216680 : [(4085 ^ _216680) ^ [_356940] : [_349164 = _356940, rpoint(_356940)]], 4092 ^ _216680 : [(4093 ^ _216680) ^ [_357317] : [_349166 = _357317, rpoint(_357317)]], 4100 ^ _216680 : [(4101 ^ _216680) ^ [_357694] : [_349168 = _357694, rpoint(_357694)]], 4108 ^ _216680 : [(4109 ^ _216680) ^ [_358071] : [_349170 = _358071, rpoint(_358071)]], 4116 ^ _216680 : [(4117 ^ _216680) ^ [_358448] : [_349172 = _358448, rpoint(_358448)]], 4124 ^ _216680 : [(4125 ^ _216680) ^ [_358825] : [_349174 = _358825, rpoint(_358825)]], 4132 ^ _216680 : [(4133 ^ _216680) ^ [_359202] : [_349176 = _359202, rpoint(_359202)]], -(_349180 = _349178), -(_349182 = _349178), -(_349182 = _349180), 4152 ^ _216680 : [(4153 ^ _216680) ^ [_360011] : [_349178 = _360011, rpoint(_360011)]], 4160 ^ _216680 : [(4161 ^ _216680) ^ [_360388] : [_349180 = _360388, rpoint(_360388)]], 4166 ^ _216680 : [(4167 ^ _216680) ^ [_360699] : [_349182 = _360699, rpoint(_360699)]]], (4177 ^ _216680) ^ [_361410, _361412, _361414, _361416, _361418, _361420] : [-(vg(_361420, _361418, _361416) = vg(_361414, _361412, _361410)), vangle(_361416, _361420, _361418) = vangle(_361410, _361414, _361412), vangle(_361418, _361416, _361420) = vangle(_361412, _361410, _361414), vangle(_361420, _361418, _361416) = vangle(_361414, _361412, _361410), vf(_361416, _361420) = vf(_361410, _361414), vf(_361418, _361416) = vf(_361412, _361410), vf(_361420, _361418) = vf(_361414, _361412), 4204 ^ _216680 : [(4205 ^ _216680) ^ [_362329] : [_361410 = _362329, rpoint(_362329)]], 4212 ^ _216680 : [(4213 ^ _216680) ^ [_362586] : [_361412 = _362586, rpoint(_362586)]], 4220 ^ _216680 : [(4221 ^ _216680) ^ [_362843] : [_361414 = _362843, rpoint(_362843)]], 4228 ^ _216680 : [(4229 ^ _216680) ^ [_363100] : [_361416 = _363100, rpoint(_363100)]], 4236 ^ _216680 : [(4237 ^ _216680) ^ [_363357] : [_361418 = _363357, rpoint(_363357)]], 4242 ^ _216680 : [(4243 ^ _216680) ^ [_363572] : [_361420 = _363572, rpoint(_363572)]]], (4251 ^ _216680) ^ [_363993, _363995, _363997, _363999, _364001, _364003] : [4318 ^ _216680 : [(4319 ^ _216680) ^ [] : [rR(_363999, _364003, _364001), -(vplus(vg(_364003, _363999, _363997), vg(_363997, _363999, _364001)) = vg(_364003, _363997, _364001))], (4325 ^ _216680) ^ [] : [vplus(vg(_364003, _363999, _363997), vg(_363997, _363999, _364001)) = vg(_364003, _363997, _364001), -(rR(_363999, _364003, _364001))]], -(ron(_363997, _363995)), _363995 = _363993, rline(_363993), -(_363999 = _363997), -(_364001 = _363997), -(_364001 = _363999), -(_364003 = _363997), -(_364003 = _363999), -(_364003 = _364001), 4290 ^ _216680 : [(4291 ^ _216680) ^ [_365132] : [_363997 = _365132, rpoint(_365132)]], 4298 ^ _216680 : [(4299 ^ _216680) ^ [_365389] : [_363999 = _365389, rpoint(_365389)]], 4306 ^ _216680 : [(4307 ^ _216680) ^ [_365646] : [_364001 = _365646, rpoint(_365646)]], 4312 ^ _216680 : [(4313 ^ _216680) ^ [_365861] : [_364003 = _365861, rpoint(_365861)]]], (4331 ^ _216680) ^ [_366592, _366594, _366596, _366598, _366600, _366602] : [4378 ^ _216680 : [(4379 ^ _216680) ^ [] : [vangle(_366602, _366598, _366596) = vangle(_366596, _366598, _366600), -(vangle(_366602, _366598, _366596) = vperp)], (4385 ^ _216680) ^ [] : [vangle(_366602, _366598, _366596) = vperp, -(vangle(_366602, _366598, _366596) = vangle(_366596, _366598, _366600))]], -(ron(_366596, _366594)), rR(_366598, _366602, _366600), _366594 = _366592, rline(_366592), 4350 ^ _216680 : [(4351 ^ _216680) ^ [_367206] : [_366596 = _367206, rpoint(_367206)]], 4358 ^ _216680 : [(4359 ^ _216680) ^ [_367463] : [_366598 = _367463, rpoint(_367463)]], 4366 ^ _216680 : [(4367 ^ _216680) ^ [_367720] : [_366600 = _367720, rpoint(_367720)]], 4372 ^ _216680 : [(4373 ^ _216680) ^ [_367935] : [_366602 = _367935, rpoint(_367935)]]], (4391 ^ _216680) ^ [_368596, _368598, _368600] : [4414 ^ _216680 : [(4415 ^ _216680) ^ [] : [-(vg(_368600, _368598, _368596) = vg(_368600, _368596, _368598))], (4417 ^ _216680) ^ [] : [-(vg(_368600, _368598, _368596) = vg(_368596, _368600, _368598))]], 4394 ^ _216680 : [(4395 ^ _216680) ^ [_368779] : [_368596 = _368779, rpoint(_368779)]], 4402 ^ _216680 : [(4403 ^ _216680) ^ [_369006] : [_368598 = _369006, rpoint(_369006)]], 4408 ^ _216680 : [(4409 ^ _216680) ^ [_369197] : [_368600 = _369197, rpoint(_369197)]]], (4419 ^ _216680) ^ [_369572, _369574] : [-(vf(_369574, _369572) = vf(_369572, _369574)), 4422 ^ _216680 : [(4423 ^ _216680) ^ [_369719] : [_369572 = _369719, rpoint(_369719)]], 4428 ^ _216680 : [(4429 ^ _216680) ^ [_369902] : [_369574 = _369902, rpoint(_369902)]]], (4437 ^ _216680) ^ [_370223, _370225, _370227, _370229, _370231] : [4480 ^ _216680 : [(4481 ^ _216680) ^ [] : [vg(_370231, _370229, _370227) = v0, -(ron(_370227, _370225))], (4487 ^ _216680) ^ [] : [ron(_370227, _370225), -(vg(_370231, _370229, _370227) = v0)]], ron(_370229, _370225), ron(_370231, _370225), -(_370231 = _370229), _370225 = _370223, rline(_370223), 4460 ^ _216680 : [(4461 ^ _216680) ^ [_370888] : [_370227 = _370888, rpoint(_370888)]], 4468 ^ _216680 : [(4469 ^ _216680) ^ [_371135] : [_370229 = _371135, rpoint(_371135)]], 4474 ^ _216680 : [(4475 ^ _216680) ^ [_371342] : [_370231 = _371342, rpoint(_371342)]]], (4493 ^ _216680) ^ [_372008, _372010, _372012, _372014, _372016, _372018] : [-(rgeq(vg(_372018, _372014, _372010), v0)), _372010 = _372008, rpoint(_372008), _372014 = _372012, rpoint(_372012), _372018 = _372016, rpoint(_372016)], (4519 ^ _216680) ^ [_372783, _372785, _372787] : [4543 ^ _216680 : [(4544 ^ _216680) ^ [] : [-(vg(_372787, _372785, _372783) = 4542 ^ [_372783, _372785, _372787])], (4546 ^ _216680) ^ [] : [-(rreal(4542 ^ [_372783, _372785, _372787]))]], 4522 ^ _216680 : [(4523 ^ _216680) ^ [_372958] : [_372783 = _372958, rpoint(_372958)]], 4530 ^ _216680 : [(4531 ^ _216680) ^ [_373185] : [_372785 = _373185, rpoint(_373185)]], 4536 ^ _216680 : [(4537 ^ _216680) ^ [_373376] : [_372787 = _373376, rpoint(_373376)]]], (4548 ^ _216680) ^ [_373898, _373900, _373902, _373904, _373906, _373908, _373910, _373912] : [4647 ^ _216680 : [(4658 ^ _216680) ^ [] : [-(rintersect(_373902, _373900))], (4648 ^ _216680) ^ [] : [-(rS(_373904, _373912, _373900)), ron(_373904, _373900), ron(_373904, _373902)]], rless(vplus(vangle(_373912, _373910, _373908), vangle(_373910, _373908, _373906)), vplus(vperp, vperp)), rS(_373912, _373906, _373900), -(_373910 = _373908), ron(_373906, _373898), ron(_373908, _373898), ron(_373908, _373900), ron(_373910, _373900), ron(_373910, _373902), ron(_373912, _373902), 4587 ^ _216680 : [(4588 ^ _216680) ^ [_375186] : [_373898 = _375186, rline(_375186)]], 4595 ^ _216680 : [(4596 ^ _216680) ^ [_375463] : [_373900 = _375463, rline(_375463)]], 4603 ^ _216680 : [(4604 ^ _216680) ^ [_375740] : [_373902 = _375740, rline(_375740)]], 4611 ^ _216680 : [(4612 ^ _216680) ^ [_376017] : [_373904 = _376017, rpoint(_376017)]], 4619 ^ _216680 : [(4620 ^ _216680) ^ [_376294] : [_373906 = _376294, rpoint(_376294)]], 4627 ^ _216680 : [(4628 ^ _216680) ^ [_376571] : [_373908 = _376571, rpoint(_376571)]], 4635 ^ _216680 : [(4636 ^ _216680) ^ [_376848] : [_373910 = _376848, rpoint(_376848)]], 4641 ^ _216680 : [(4642 ^ _216680) ^ [_377079] : [_373912 = _377079, rpoint(_377079)]]], (4660 ^ _216680) ^ [_377774, _377776] : [-(vg(_377776, _377776, _377774) = v0), 4663 ^ _216680 : [(4664 ^ _216680) ^ [_377919] : [_377774 = _377919, rpoint(_377919)]], 4669 ^ _216680 : [(4670 ^ _216680) ^ [_378102] : [_377776 = _378102, rpoint(_378102)]]], (4678 ^ _216680) ^ [_378393, _378395, _378397] : [4701 ^ _216680 : [(4702 ^ _216680) ^ [] : [-(rleq(vangle(_378397, _378395, _378393), vplus(vperp, vperp)))], (4704 ^ _216680) ^ [] : [-(rleq(v0, vangle(_378397, _378395, _378393)))]], 4681 ^ _216680 : [(4682 ^ _216680) ^ [_378568] : [_378393 = _378568, rpoint(_378568)]], 4689 ^ _216680 : [(4690 ^ _216680) ^ [_378795] : [_378395 = _378795, rpoint(_378795)]], 4695 ^ _216680 : [(4696 ^ _216680) ^ [_378986] : [_378397 = _378986, rpoint(_378986)]]], (4740 ^ _216680) ^ [_380422, _380424] : [-(rleq(v0, vf(_380424, _380422))), 4743 ^ _216680 : [(4744 ^ _216680) ^ [_380566] : [_380422 = _380566, rpoint(_380566)]], 4749 ^ _216680 : [(4750 ^ _216680) ^ [_380749] : [_380424 = _380749, rpoint(_380749)]]], (4706 ^ _216680) ^ [_379367, _379369, _379371] : [-(vangle(_379371, _379369, _379367) = vangle(_379367, _379369, _379371)), -(_379371 = _379367), -(_379371 = _379369), 4717 ^ _216680 : [(4718 ^ _216680) ^ [_379720] : [_379367 = _379720, rpoint(_379720)]], 4725 ^ _216680 : [(4726 ^ _216680) ^ [_379947] : [_379369 = _379947, rpoint(_379947)]], 4731 ^ _216680 : [(4732 ^ _216680) ^ [_380138] : [_379371 = _380138, rpoint(_380138)]]]], input).
% 102.71/98.99 ncf('1',plain,[rR(524 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139], vd1123, vd1125), ron(524 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139], vd1139), ron(524 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139], vd1138), rpoint(524 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139])],start(4758 ^ 0,bind([[_382021], [524 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139]]]))).
% 102.71/98.99 ncf('1.1',plain,[-(rR(524 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139], vd1123, vd1125)), ron(vd1125, vd1138), -(ron(vd1125, vd1139)), -(rinside(vd1125, vd1139)), vd1125 = vd1126, rpoint(vd1126), ron(vd1123, vd1138), rinside(vd1123, vd1139), vd1123 = vd1124, rpoint(vd1124), vd1138 = vd1138, rline(vd1138), vd1139 = vd1139, rcircle(vd1139)],extension(473 ^ 1,bind([[_232215, _232217, _232219, _232221, _232223, _232225, _232227, _232229], [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139]]))).
% 102.71/98.99 ncf('1.1.1',plain,[-(ron(vd1125, vd1138))],extension(312 ^ 2)).
% 102.71/98.99 ncf('1.1.2',plain,[ron(vd1125, vd1139)],extension(302 ^ 2)).
% 102.71/98.99 ncf('1.1.3',plain,[rinside(vd1125, vd1139)],extension(304 ^ 2)).
% 102.71/98.99 ncf('1.1.4',plain,[-(vd1125 = vd1126)],extension(334 ^ 2)).
% 102.71/98.99 ncf('1.1.5',plain,[-(rpoint(vd1126))],extension(336 ^ 2)).
% 102.71/98.99 ncf('1.1.6',plain,[-(ron(vd1123, vd1138))],extension(314 ^ 2)).
% 102.71/98.99 ncf('1.1.7',plain,[-(rinside(vd1123, vd1139)), rcenter(vd1123, vd1139)],extension(2691 ^ 2,bind([[_304403, _304405], [vd1139, vd1123]]))).
% 102.71/98.99 ncf('1.1.7.1',plain,[-(rcenter(vd1123, vd1139))],extension(308 ^ 3)).
% 102.71/98.99 ncf('1.1.8',plain,[-(vd1123 = vd1124)],extension(338 ^ 2)).
% 102.71/98.99 ncf('1.1.9',plain,[-(rpoint(vd1124))],extension(340 ^ 2)).
% 102.71/98.99 ncf('1.1.10',plain,[-(vd1138 = vd1138)],extension(2 ^ 2,bind([[_216824], [vd1138]]))).
% 102.71/98.99 ncf('1.1.11',plain,[-(rline(vd1138))],extension(409 ^ 2)).
% 102.71/98.99 ncf('1.1.12',plain,[-(vd1139 = vd1139)],extension(2 ^ 2,bind([[_216824], [vd1139]]))).
% 102.71/98.99 ncf('1.1.13',plain,[-(rcircle(vd1139))],extension(310 ^ 2)).
% 102.71/98.99 ncf('1.2',plain,[-(ron(524 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139], vd1139)), ron(vd1125, vd1138), -(ron(vd1125, vd1139)), -(rinside(vd1125, vd1139)), vd1125 = vd1126, rpoint(vd1126), ron(vd1123, vd1138), rinside(vd1123, vd1139), vd1123 = vd1124, rpoint(vd1124), vd1138 = vd1138, rline(vd1138), vd1139 = vd1139, rcircle(vd1139)],extension(473 ^ 1,bind([[_232215, _232217, _232219, _232221, _232223, _232225, _232227, _232229], [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139]]))).
% 102.71/98.99 ncf('1.2.1',plain,[-(ron(vd1125, vd1138))],extension(312 ^ 2)).
% 102.71/98.99 ncf('1.2.2',plain,[ron(vd1125, vd1139)],extension(302 ^ 2)).
% 102.71/98.99 ncf('1.2.3',plain,[rinside(vd1125, vd1139)],extension(304 ^ 2)).
% 102.71/98.99 ncf('1.2.4',plain,[-(vd1125 = vd1126)],extension(334 ^ 2)).
% 102.71/98.99 ncf('1.2.5',plain,[-(rpoint(vd1126))],extension(336 ^ 2)).
% 102.71/98.99 ncf('1.2.6',plain,[-(ron(vd1123, vd1138))],extension(314 ^ 2)).
% 102.71/98.99 ncf('1.2.7',plain,[-(rinside(vd1123, vd1139)), rcenter(vd1123, vd1139)],extension(2691 ^ 2,bind([[_304403, _304405], [vd1139, vd1123]]))).
% 102.71/98.99 ncf('1.2.7.1',plain,[-(rcenter(vd1123, vd1139))],extension(308 ^ 3)).
% 102.71/98.99 ncf('1.2.8',plain,[-(vd1123 = vd1124)],extension(338 ^ 2)).
% 102.71/98.99 ncf('1.2.9',plain,[-(rpoint(vd1124))],extension(340 ^ 2)).
% 102.71/98.99 ncf('1.2.10',plain,[-(vd1138 = vd1138)],extension(2 ^ 2,bind([[_216824], [vd1138]]))).
% 102.71/98.99 ncf('1.2.11',plain,[-(rline(vd1138))],extension(409 ^ 2)).
% 102.71/98.99 ncf('1.2.12',plain,[-(vd1139 = vd1139)],extension(2 ^ 2,bind([[_216824], [vd1139]]))).
% 102.71/98.99 ncf('1.2.13',plain,[-(rcircle(vd1139))],extension(310 ^ 2)).
% 102.71/98.99 ncf('1.3',plain,[-(ron(524 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139], vd1138)), ron(vd1125, vd1138), -(ron(vd1125, vd1139)), -(rinside(vd1125, vd1139)), vd1125 = vd1126, rpoint(vd1126), ron(vd1123, vd1138), rinside(vd1123, vd1139), vd1123 = vd1124, rpoint(vd1124), vd1138 = vd1138, rline(vd1138), vd1139 = vd1139, rcircle(vd1139)],extension(473 ^ 1,bind([[_232215, _232217, _232219, _232221, _232223, _232225, _232227, _232229], [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139]]))).
% 102.71/98.99 ncf('1.3.1',plain,[-(ron(vd1125, vd1138))],extension(312 ^ 2)).
% 102.71/98.99 ncf('1.3.2',plain,[ron(vd1125, vd1139)],extension(302 ^ 2)).
% 102.71/98.99 ncf('1.3.3',plain,[rinside(vd1125, vd1139)],extension(304 ^ 2)).
% 102.71/98.99 ncf('1.3.4',plain,[-(vd1125 = vd1126)],extension(334 ^ 2)).
% 102.71/98.99 ncf('1.3.5',plain,[-(rpoint(vd1126))],extension(336 ^ 2)).
% 102.71/98.99 ncf('1.3.6',plain,[-(ron(vd1123, vd1138))],extension(314 ^ 2)).
% 102.71/98.99 ncf('1.3.7',plain,[-(rinside(vd1123, vd1139)), rcenter(vd1123, vd1139)],extension(2691 ^ 2,bind([[_304403, _304405], [vd1139, vd1123]]))).
% 102.71/98.99 ncf('1.3.7.1',plain,[-(rcenter(vd1123, vd1139))],extension(308 ^ 3)).
% 102.71/98.99 ncf('1.3.8',plain,[-(vd1123 = vd1124)],extension(338 ^ 2)).
% 102.71/98.99 ncf('1.3.9',plain,[-(rpoint(vd1124))],extension(340 ^ 2)).
% 102.71/98.99 ncf('1.3.10',plain,[-(vd1138 = vd1138)],extension(2 ^ 2,bind([[_216824], [vd1138]]))).
% 102.71/98.99 ncf('1.3.11',plain,[-(rline(vd1138))],extension(409 ^ 2)).
% 102.71/98.99 ncf('1.3.12',plain,[-(vd1139 = vd1139)],extension(2 ^ 2,bind([[_216824], [vd1139]]))).
% 102.71/98.99 ncf('1.3.13',plain,[-(rcircle(vd1139))],extension(310 ^ 2)).
% 102.71/98.99 ncf('1.4',plain,[-(rpoint(524 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139])), ron(vd1125, vd1138), -(ron(vd1125, vd1139)), -(rinside(vd1125, vd1139)), vd1125 = vd1126, rpoint(vd1126), ron(vd1123, vd1138), rinside(vd1123, vd1139), vd1123 = vd1124, rpoint(vd1124), vd1138 = vd1138, rline(vd1138), vd1139 = vd1139, rcircle(vd1139)],extension(473 ^ 1,bind([[_232215, _232217, _232219, _232221, _232223, _232225, _232227, _232229], [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139]]))).
% 102.71/98.99 ncf('1.4.1',plain,[-(ron(vd1125, vd1138))],extension(312 ^ 2)).
% 102.71/98.99 ncf('1.4.2',plain,[ron(vd1125, vd1139)],extension(302 ^ 2)).
% 102.71/98.99 ncf('1.4.3',plain,[rinside(vd1125, vd1139)],extension(304 ^ 2)).
% 102.71/98.99 ncf('1.4.4',plain,[-(vd1125 = vd1126)],extension(334 ^ 2)).
% 102.71/98.99 ncf('1.4.5',plain,[-(rpoint(vd1126))],extension(336 ^ 2)).
% 102.71/98.99 ncf('1.4.6',plain,[-(ron(vd1123, vd1138))],extension(314 ^ 2)).
% 102.71/98.99 ncf('1.4.7',plain,[-(rinside(vd1123, vd1139)), rcenter(vd1123, vd1139)],extension(2691 ^ 2,bind([[_304403, _304405], [vd1139, vd1123]]))).
% 102.71/98.99 ncf('1.4.7.1',plain,[-(rcenter(vd1123, vd1139))],extension(308 ^ 3)).
% 102.71/98.99 ncf('1.4.8',plain,[-(vd1123 = vd1124)],extension(338 ^ 2)).
% 102.71/98.99 ncf('1.4.9',plain,[-(rpoint(vd1124))],extension(340 ^ 2)).
% 102.71/98.99 ncf('1.4.10',plain,[-(vd1138 = vd1138)],extension(2 ^ 2,bind([[_216824], [vd1138]]))).
% 102.71/98.99 ncf('1.4.11',plain,[-(rline(vd1138))],extension(409 ^ 2)).
% 102.71/98.99 ncf('1.4.12',plain,[-(vd1139 = vd1139)],extension(2 ^ 2,bind([[_216824], [vd1139]]))).
% 102.71/98.99 ncf('1.4.13',plain,[-(rcircle(vd1139))],extension(310 ^ 2)).
% 102.71/98.99 %-----------------------------------------------------
% 102.71/98.99 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------