%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO631+1 : TPTP v8.1.2. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n028.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:43 EDT 2023
% Result : Theorem 153.17s 148.21s
% Output : Proof 153.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : GEO631+1 : TPTP v8.1.2. Released v7.5.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n028.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri May 19 04:12:33 EDT 2023
% 0.12/0.33 % CPUTime :
% 153.17/148.21
% 153.17/148.21 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 153.17/148.21 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 153.17/148.21 %-----------------------------------------------------
% 153.17/148.21 ncf(matrix, plain, [(941 ^ _286175) ^ [] : [-(circle(930 ^ [], 927 ^ [], 928 ^ [], 929 ^ []))], (943 ^ _286175) ^ [] : [-(circle(930 ^ [], 927 ^ [], 931 ^ [], 938 ^ []))], (945 ^ _286175) ^ [] : [-(circle(930 ^ [], 927 ^ [], 932 ^ [], 939 ^ []))], (947 ^ _286175) ^ [] : [-(perp(933 ^ [], 932 ^ [], 927 ^ [], 931 ^ []))], (949 ^ _286175) ^ [] : [-(coll(933 ^ [], 927 ^ [], 931 ^ []))], (951 ^ _286175) ^ [] : [-(perp(934 ^ [], 932 ^ [], 927 ^ [], 928 ^ []))], (953 ^ _286175) ^ [] : [-(coll(934 ^ [], 927 ^ [], 928 ^ []))], (955 ^ _286175) ^ [] : [-(perp(935 ^ [], 932 ^ [], 928 ^ [], 929 ^ []))], (957 ^ _286175) ^ [] : [-(coll(935 ^ [], 928 ^ [], 929 ^ []))], (959 ^ _286175) ^ [] : [-(perp(936 ^ [], 932 ^ [], 929 ^ [], 931 ^ []))], (961 ^ _286175) ^ [] : [-(coll(936 ^ [], 929 ^ [], 931 ^ []))], (963 ^ _286175) ^ [] : [-(coll(937 ^ [], 933 ^ [], 934 ^ []))], (965 ^ _286175) ^ [] : [-(coll(937 ^ [], 935 ^ [], 936 ^ []))], (967 ^ _286175) ^ [] : [cyclic(932 ^ [], 934 ^ [], 937 ^ [], 935 ^ [])], (2 ^ _286175) ^ [_286302, _286304, _286306] : [coll(_286306, _286304, _286302), -(coll(_286306, _286302, _286304))], (8 ^ _286175) ^ [_286536, _286538, _286540] : [coll(_286540, _286538, _286536), -(coll(_286538, _286540, _286536))], (14 ^ _286175) ^ [_286784, _286786, _286788, _286790] : [-(coll(_286786, _286784, _286790)), coll(_286790, _286788, _286786), coll(_286790, _286788, _286784)], (24 ^ _286175) ^ [_287137, _287139, _287141, _287143] : [para(_287143, _287141, _287139, _287137), -(para(_287143, _287141, _287137, _287139))], (30 ^ _286175) ^ [_287395, _287397, _287399, _287401] : [para(_287401, _287399, _287397, _287395), -(para(_287397, _287395, _287401, _287399))], (36 ^ _286175) ^ [_287681, _287683, _287685, _287687, _287689, _287691] : [-(para(_287691, _287689, _287683, _287681)), para(_287691, _287689, _287687, _287685), para(_287687, _287685, _287683, _287681)], (46 ^ _286175) ^ [_288060, _288062, _288064, _288066] : [perp(_288066, _288064, _288062, _288060), -(perp(_288066, _288064, _288060, _288062))], (52 ^ _286175) ^ [_288318, _288320, _288322, _288324] : [perp(_288324, _288322, _288320, _288318), -(perp(_288320, _288318, _288324, _288322))], (58 ^ _286175) ^ [_288604, _288606, _288608, _288610, _288612, _288614] : [-(para(_288614, _288612, _288606, _288604)), perp(_288614, _288612, _288610, _288608), perp(_288610, _288608, _288606, _288604)], (68 ^ _286175) ^ [_289011, _289013, _289015, _289017, _289019, _289021] : [-(perp(_289021, _289019, _289013, _289011)), para(_289021, _289019, _289017, _289015), perp(_289017, _289015, _289013, _289011)], (78 ^ _286175) ^ [_289376, _289378, _289380] : [midp(_289376, _289378, _289380), -(midp(_289376, _289380, _289378))], (84 ^ _286175) ^ [_289624, _289626, _289628, _289630] : [-(circle(_289624, _289630, _289628, _289626)), cong(_289624, _289630, _289624, _289628), cong(_289624, _289630, _289624, _289626)], (94 ^ _286175) ^ [_289997, _289999, _290001, _290003, _290005] : [-(cyclic(_290005, _290003, _290001, _289999)), cong(_289997, _290005, _289997, _290003), cong(_289997, _290005, _289997, _290001), cong(_289997, _290005, _289997, _289999)], (108 ^ _286175) ^ [_290471, _290473, _290475, _290477] : [cyclic(_290477, _290475, _290473, _290471), -(cyclic(_290477, _290475, _290471, _290473))], (114 ^ _286175) ^ [_290729, _290731, _290733, _290735] : [cyclic(_290735, _290733, _290731, _290729), -(cyclic(_290735, _290731, _290733, _290729))], (120 ^ _286175) ^ [_290987, _290989, _290991, _290993] : [cyclic(_290993, _290991, _290989, _290987), -(cyclic(_290991, _290993, _290989, _290987))], (126 ^ _286175) ^ [_291259, _291261, _291263, _291265, _291267] : [-(cyclic(_291265, _291263, _291261, _291259)), cyclic(_291267, _291265, _291263, _291261), cyclic(_291267, _291265, _291263, _291259)], (136 ^ _286175) ^ [_291684, _291686, _291688, _291690, _291692, _291694, _291696, _291698] : [eqangle(_291698, _291696, _291694, _291692, _291690, _291688, _291686, _291684), -(eqangle(_291696, _291698, _291694, _291692, _291690, _291688, _291686, _291684))], (142 ^ _286175) ^ [_292038, _292040, _292042, _292044, _292046, _292048, _292050, _292052] : [eqangle(_292052, _292050, _292048, _292046, _292044, _292042, _292040, _292038), -(eqangle(_292048, _292046, _292052, _292050, _292040, _292038, _292044, _292042))], (148 ^ _286175) ^ [_292392, _292394, _292396, _292398, _292400, _292402, _292404, _292406] : [eqangle(_292406, _292404, _292402, _292400, _292398, _292396, _292394, _292392), -(eqangle(_292398, _292396, _292394, _292392, _292406, _292404, _292402, _292400))], (154 ^ _286175) ^ [_292746, _292748, _292750, _292752, _292754, _292756, _292758, _292760] : [eqangle(_292760, _292758, _292756, _292754, _292752, _292750, _292748, _292746), -(eqangle(_292760, _292758, _292752, _292750, _292756, _292754, _292748, _292746))], (160 ^ _286175) ^ [_293156, _293158, _293160, _293162, _293164, _293166, _293168, _293170, _293172, _293174, _293176, _293178] : [-(eqangle(_293178, _293176, _293174, _293172, _293162, _293160, _293158, _293156)), eqangle(_293178, _293176, _293174, _293172, _293170, _293168, _293166, _293164), eqangle(_293170, _293168, _293166, _293164, _293162, _293160, _293158, _293156)], (170 ^ _286175) ^ [_293619, _293621, _293623, _293625] : [cong(_293625, _293623, _293621, _293619), -(cong(_293625, _293623, _293619, _293621))], (176 ^ _286175) ^ [_293877, _293879, _293881, _293883] : [cong(_293883, _293881, _293879, _293877), -(cong(_293879, _293877, _293883, _293881))], (182 ^ _286175) ^ [_294163, _294165, _294167, _294169, _294171, _294173] : [-(cong(_294173, _294171, _294165, _294163)), cong(_294173, _294171, _294169, _294167), cong(_294169, _294167, _294165, _294163)], (192 ^ _286175) ^ [_294598, _294600, _294602, _294604, _294606, _294608, _294610, _294612] : [eqratio(_294612, _294610, _294608, _294606, _294604, _294602, _294600, _294598), -(eqratio(_294610, _294612, _294608, _294606, _294604, _294602, _294600, _294598))], (198 ^ _286175) ^ [_294952, _294954, _294956, _294958, _294960, _294962, _294964, _294966] : [eqratio(_294966, _294964, _294962, _294960, _294958, _294956, _294954, _294952), -(eqratio(_294962, _294960, _294966, _294964, _294954, _294952, _294958, _294956))], (204 ^ _286175) ^ [_295306, _295308, _295310, _295312, _295314, _295316, _295318, _295320] : [eqratio(_295320, _295318, _295316, _295314, _295312, _295310, _295308, _295306), -(eqratio(_295312, _295310, _295308, _295306, _295320, _295318, _295316, _295314))], (210 ^ _286175) ^ [_295660, _295662, _295664, _295666, _295668, _295670, _295672, _295674] : [eqratio(_295674, _295672, _295670, _295668, _295666, _295664, _295662, _295660), -(eqratio(_295674, _295672, _295666, _295664, _295670, _295668, _295662, _295660))], (216 ^ _286175) ^ [_296070, _296072, _296074, _296076, _296078, _296080, _296082, _296084, _296086, _296088, _296090, _296092] : [-(eqratio(_296092, _296090, _296088, _296086, _296084, _296082, _296080, _296078)), eqratio(_296092, _296090, _296088, _296086, _296076, _296074, _296072, _296070), eqratio(_296076, _296074, _296072, _296070, _296084, _296082, _296080, _296078)], (226 ^ _286175) ^ [_296561, _296563, _296565, _296567, _296569, _296571] : [simtri(_296571, _296567, _296569, _296565, _296561, _296563), -(simtri(_296571, _296569, _296567, _296565, _296563, _296561))], (232 ^ _286175) ^ [_296867, _296869, _296871, _296873, _296875, _296877] : [simtri(_296875, _296877, _296873, _296869, _296871, _296867), -(simtri(_296877, _296875, _296873, _296871, _296869, _296867))], (238 ^ _286175) ^ [_297173, _297175, _297177, _297179, _297181, _297183] : [simtri(_297177, _297175, _297173, _297183, _297181, _297179), -(simtri(_297183, _297181, _297179, _297177, _297175, _297173))], (244 ^ _286175) ^ [_297521, _297523, _297525, _297527, _297529, _297531, _297533, _297535, _297537] : [-(simtri(_297537, _297535, _297533, _297525, _297523, _297521)), simtri(_297537, _297535, _297533, _297531, _297529, _297527), simtri(_297531, _297529, _297527, _297525, _297523, _297521)], (254 ^ _286175) ^ [_297970, _297972, _297974, _297976, _297978, _297980] : [contri(_297980, _297976, _297978, _297974, _297970, _297972), -(contri(_297980, _297978, _297976, _297974, _297972, _297970))], (260 ^ _286175) ^ [_298276, _298278, _298280, _298282, _298284, _298286] : [contri(_298284, _298286, _298282, _298278, _298280, _298276), -(contri(_298286, _298284, _298282, _298280, _298278, _298276))], (266 ^ _286175) ^ [_298582, _298584, _298586, _298588, _298590, _298592] : [contri(_298586, _298584, _298582, _298592, _298590, _298588), -(contri(_298592, _298590, _298588, _298586, _298584, _298582))], (272 ^ _286175) ^ [_298930, _298932, _298934, _298936, _298938, _298940, _298942, _298944, _298946] : [-(contri(_298946, _298944, _298942, _298934, _298932, _298930)), contri(_298946, _298944, _298942, _298940, _298938, _298936), contri(_298940, _298938, _298936, _298934, _298932, _298930)], (282 ^ _286175) ^ [_299379, _299381, _299383, _299385, _299387, _299389] : [eqangle(_299389, _299387, _299381, _299379, _299385, _299383, _299381, _299379), -(para(_299389, _299387, _299385, _299383))], (288 ^ _286175) ^ [_299685, _299687, _299689, _299691, _299693, _299695] : [para(_299695, _299693, _299691, _299689), -(eqangle(_299695, _299693, _299687, _299685, _299691, _299689, _299687, _299685))], (294 ^ _286175) ^ [_299963, _299965, _299967, _299969] : [cyclic(_299969, _299967, _299965, _299963), -(eqangle(_299965, _299969, _299965, _299967, _299963, _299969, _299963, _299967))], (300 ^ _286175) ^ [_300229, _300231, _300233, _300235] : [-(cyclic(_300235, _300233, _300231, _300229)), eqangle(_300231, _300235, _300231, _300233, _300229, _300235, _300229, _300233), -(coll(_300231, _300229, _300235))], (310 ^ _286175) ^ [_300597, _300599, _300601, _300603] : [-(cyclic(_300603, _300601, _300599, _300597)), eqangle(_300599, _300603, _300599, _300601, _300597, _300603, _300597, _300601), coll(_300599, _300597, _300601)], (320 ^ _286175) ^ [_300990, _300992, _300994, _300996, _300998, _301000] : [-(cong(_301000, _300998, _300994, _300992)), cyclic(_301000, _300998, _300996, _300994), cyclic(_301000, _300998, _300996, _300992), cyclic(_301000, _300998, _300996, _300990), eqangle(_300996, _301000, _300996, _300998, _300990, _300994, _300990, _300992)], (338 ^ _286175) ^ [_301609, _301611, _301613, _301615, _301617] : [-(para(_301611, _301609, _301615, _301613)), midp(_301611, _301617, _301615), midp(_301609, _301617, _301613)], (348 ^ _286175) ^ [_301988, _301990, _301992, _301994, _301996] : [-(midp(_301988, _301996, _301992)), midp(_301990, _301996, _301994), para(_301990, _301988, _301994, _301992), coll(_301988, _301996, _301992)], (362 ^ _286175) ^ [_302442, _302444, _302446] : [cong(_302442, _302446, _302442, _302444), -(eqangle(_302442, _302446, _302446, _302444, _302446, _302444, _302442, _302444))], (368 ^ _286175) ^ [_302688, _302690, _302692] : [-(cong(_302688, _302692, _302688, _302690)), eqangle(_302688, _302692, _302692, _302690, _302692, _302690, _302688, _302690), -(coll(_302688, _302692, _302690))], (378 ^ _286175) ^ [_303060, _303062, _303064, _303066, _303068] : [-(eqangle(_303068, _303060, _303068, _303066, _303064, _303068, _303064, _303066)), circle(_303062, _303068, _303066, _303064), perp(_303062, _303068, _303068, _303060)], (388 ^ _286175) ^ [_303451, _303453, _303455, _303457, _303459] : [-(perp(_303453, _303459, _303459, _303451)), circle(_303453, _303459, _303457, _303455), eqangle(_303459, _303451, _303459, _303457, _303455, _303459, _303455, _303457)], (398 ^ _286175) ^ [_303842, _303844, _303846, _303848, _303850] : [-(eqangle(_303850, _303848, _303850, _303846, _303844, _303848, _303844, _303842)), circle(_303844, _303850, _303848, _303846), midp(_303842, _303848, _303846)], (408 ^ _286175) ^ [_304231, _304233, _304235, _304237, _304239] : [-(midp(_304231, _304237, _304235)), circle(_304233, _304239, _304237, _304235), coll(_304231, _304237, _304235), eqangle(_304239, _304237, _304239, _304235, _304233, _304237, _304233, _304231)], (422 ^ _286175) ^ [_304709, _304711, _304713, _304715] : [-(cong(_304715, _304709, _304713, _304709)), perp(_304715, _304713, _304713, _304711), midp(_304709, _304715, _304711)], (432 ^ _286175) ^ [_305066, _305068, _305070, _305072] : [-(perp(_305072, _305070, _305070, _305068)), circle(_305066, _305072, _305070, _305068), coll(_305066, _305072, _305068)], (442 ^ _286175) ^ [_305423, _305425, _305427, _305429] : [-(eqangle(_305429, _305423, _305425, _305423, _305425, _305423, _305425, _305427)), cyclic(_305429, _305427, _305425, _305423), para(_305429, _305427, _305425, _305423)], (452 ^ _286175) ^ [_305790, _305792, _305794, _305796] : [-(cong(_305790, _305796, _305790, _305794)), midp(_305792, _305796, _305794), perp(_305790, _305792, _305796, _305794)], (462 ^ _286175) ^ [_306147, _306149, _306151, _306153] : [-(perp(_306153, _306151, _306149, _306147)), cong(_306153, _306149, _306151, _306149), cong(_306153, _306147, _306151, _306147)], (472 ^ _286175) ^ [_306506, _306508, _306510, _306512] : [-(perp(_306508, _306512, _306512, _306506)), cong(_306512, _306508, _306510, _306508), cong(_306512, _306506, _306510, _306506), cyclic(_306512, _306510, _306508, _306506)], (486 ^ _286175) ^ [_306994, _306996, _306998, _307000, _307002, _307004] : [-(simtri(_307004, _307002, _307000, _306998, _306996, _306994)), eqangle(_307004, _307002, _307002, _307000, _306998, _306996, _306996, _306994), eqangle(_307004, _307000, _307002, _307000, _306998, _306994, _306996, _306994), -(coll(_307004, _307002, _307000))], (500 ^ _286175) ^ [_307531, _307533, _307535, _307537, _307539, _307541] : [simtri(_307541, _307539, _307537, _307535, _307533, _307531), -(eqratio(_307541, _307539, _307541, _307537, _307535, _307533, _307535, _307531))], (506 ^ _286175) ^ [_307841, _307843, _307845, _307847, _307849, _307851] : [simtri(_307851, _307849, _307847, _307845, _307843, _307841), -(eqangle(_307851, _307849, _307849, _307847, _307845, _307843, _307843, _307841))], (512 ^ _286175) ^ [_308151, _308153, _308155, _308157, _308159, _308161] : [-(contri(_308161, _308159, _308157, _308155, _308153, _308151)), simtri(_308161, _308159, _308157, _308155, _308153, _308151), cong(_308161, _308159, _308155, _308153)], (522 ^ _286175) ^ [_308566, _308568, _308570, _308572, _308574, _308576] : [contri(_308576, _308574, _308572, _308570, _308568, _308566), -(cong(_308576, _308574, _308570, _308568))], (528 ^ _286175) ^ [_308854, _308856, _308858, _308860, _308862] : [-(para(_308862, _308858, _308860, _308856)), midp(_308854, _308862, _308860), midp(_308854, _308858, _308856)], (538 ^ _286175) ^ [_309233, _309235, _309237, _309239, _309241] : [-(midp(_309233, _309237, _309235)), midp(_309233, _309241, _309239), para(_309241, _309237, _309239, _309235), para(_309241, _309235, _309239, _309237)], (552 ^ _286175) ^ [_309717, _309719, _309721, _309723, _309725] : [-(eqratio(_309717, _309725, _309725, _309721, _309717, _309723, _309723, _309719)), para(_309725, _309723, _309721, _309719), coll(_309717, _309725, _309721), coll(_309717, _309723, _309719)], (566 ^ _286175) ^ [_310181, _310183, _310185] : [para(_310185, _310183, _310185, _310181), -(coll(_310185, _310183, _310181))], (572 ^ _286175) ^ [_310417, _310419, _310421] : [-(midp(_310421, _310419, _310417)), cong(_310421, _310419, _310421, _310417), coll(_310421, _310419, _310417)], (582 ^ _286175) ^ [_310748, _310750, _310752] : [midp(_310752, _310750, _310748), -(cong(_310752, _310750, _310752, _310748))], (588 ^ _286175) ^ [_310984, _310986, _310988] : [midp(_310988, _310986, _310984), -(coll(_310988, _310986, _310984))], (594 ^ _286175) ^ [_311260, _311262, _311264, _311266, _311268, _311270] : [-(eqratio(_311262, _311270, _311270, _311268, _311260, _311266, _311266, _311264)), midp(_311262, _311270, _311268), midp(_311260, _311266, _311264)], (604 ^ _286175) ^ [_311643, _311645, _311647, _311649] : [-(perp(_311649, _311647, _311645, _311643)), eqangle(_311649, _311647, _311645, _311643, _311645, _311643, _311649, _311647), -(para(_311649, _311647, _311645, _311643))], (614 ^ _286175) ^ [_312013, _312015, _312017, _312019] : [-(para(_312019, _312017, _312015, _312013)), eqangle(_312019, _312017, _312015, _312013, _312015, _312013, _312019, _312017), -(perp(_312019, _312017, _312015, _312013))], (624 ^ _286175) ^ [_312439, _312441, _312443, _312445, _312447, _312449, _312451, _312453] : [-(para(_312453, _312451, _312449, _312447)), eqangle(_312453, _312451, _312449, _312447, _312445, _312443, _312441, _312439), para(_312445, _312443, _312441, _312439)], (634 ^ _286175) ^ [_312902, _312904, _312906, _312908, _312910, _312912, _312914, _312916] : [-(perp(_312916, _312914, _312912, _312910)), eqangle(_312916, _312914, _312912, _312910, _312908, _312906, _312904, _312902), perp(_312908, _312906, _312904, _312902)], (644 ^ _286175) ^ [_313365, _313367, _313369, _313371, _313373, _313375, _313377, _313379] : [-(cong(_313379, _313377, _313375, _313373)), eqratio(_313379, _313377, _313375, _313373, _313371, _313369, _313367, _313365), cong(_313371, _313369, _313367, _313365)], (655 ^ _286175) ^ [_313845, _313847, _313849, _313851] : [662 ^ _286175 : [(663 ^ _286175) ^ [] : [-(coll(653 ^ [_313845, _313847, _313849, _313851], _313851, _313849))], (665 ^ _286175) ^ [] : [-(coll(653 ^ [_313845, _313847, _313849, _313851], _313847, _313845))]], perp(_313847, _313849, _313849, _313851), eqangle(_313845, _313847, _313849, _313847, _313849, _313847, _313851, _313847)], (668 ^ _286175) ^ [_314408, _314410, _314412, _314414] : [675 ^ _286175 : [(676 ^ _286175) ^ [] : [-(coll(_314412, _314414, 666 ^ [_314408, _314410, _314412, _314414]))], (678 ^ _286175) ^ [] : [-(coll(666 ^ [_314408, _314410, _314412, _314414], _314410, _314408))]], cong(_314410, _314414, _314410, _314412), eqangle(_314414, _314410, _314410, _314408, _314410, _314408, _314410, _314412)], (681 ^ _286175) ^ [_314971, _314973, _314975, _314977] : [688 ^ _286175 : [(689 ^ _286175) ^ [] : [-(coll(_314975, _314977, 679 ^ [_314971, _314973, _314975, _314977]))], (691 ^ _286175) ^ [] : [-(coll(679 ^ [_314971, _314973, _314975, _314977], _314973, _314971))]], perp(_314973, _314971, _314977, _314975), eqangle(_314977, _314973, _314973, _314971, _314973, _314971, _314973, _314975)], (694 ^ _286175) ^ [_315530, _315532, _315534, _315536] : [701 ^ _286175 : [(702 ^ _286175) ^ [] : [-(coll(_315534, _315536, 692 ^ [_315530, _315532, _315534, _315536]))], (704 ^ _286175) ^ [] : [-(coll(692 ^ [_315530, _315532, _315534, _315536], _315532, _315530))]], perp(_315532, _315530, _315536, _315534), cong(_315532, _315536, _315532, _315534)], (707 ^ _286175) ^ [_316108, _316110, _316112, _316114, _316116] : [714 ^ _286175 : [(715 ^ _286175) ^ [] : [-(eqangle(_316116, _316112, _316114, _316112, _316116, 705 ^ [_316108, _316110, _316112, _316114, _316116], _316114, 705 ^ [_316108, _316110, _316112, _316114, _316116]))], (717 ^ _286175) ^ [] : [-(cyclic(_316110, _316114, _316112, 705 ^ [_316108, _316110, _316112, _316114, _316116]))]], eqangle(_316116, _316112, _316114, _316112, _316116, _316110, _316114, _316108), -(coll(_316116, _316114, _316112))], (720 ^ _286175) ^ [_316765, _316767, _316769, _316771, _316773, _316775] : [727 ^ _286175 : [(728 ^ _286175) ^ [] : [-(midp(718 ^ [_316765, _316767, _316769, _316771, _316773, _316775], _316775, _316769))], (730 ^ _286175) ^ [] : [-(para(718 ^ [_316765, _316767, _316769, _316771, _316773, _316775], _316767, _316773, _316769))], (732 ^ _286175) ^ [] : [-(para(718 ^ [_316765, _316767, _316769, _316771, _316773, _316775], _316765, _316775, _316771))]], midp(_316767, _316775, _316773), midp(_316765, _316771, _316769)], (735 ^ _286175) ^ [_317523, _317525, _317527, _317529, _317531, _317533, _317535] : [-(midp(733 ^ [_317523, _317525, _317527, _317529, _317531, _317533, _317535], _317535, _317523)), midp(_317527, _317535, _317533), midp(_317525, _317531, _317529), coll(_317531, _317535, _317533), coll(_317529, _317535, _317533)], (754 ^ _286175) ^ [_318293, _318295, _318297, _318299, _318301, _318303, _318305] : [769 ^ _286175 : [(770 ^ _286175) ^ [] : [-(coll(752 ^ [_318293, _318295, _318297, _318299, _318301, _318303, _318305], _318305, _318297))], (772 ^ _286175) ^ [] : [-(coll(752 ^ [_318293, _318295, _318297, _318299, _318301, _318303, _318305], _318293, _318295))]], midp(_318293, _318305, _318303), para(_318305, _318299, _318295, _318293), para(_318305, _318299, _318303, _318297), coll(_318299, _318297, _318295)], (775 ^ _286175) ^ [_319152, _319154, _319156, _319158, _319160] : [782 ^ _286175 : [(783 ^ _286175) ^ [] : [-(cong(_319152, _319156, _319152, 773 ^ [_319152, _319154, _319156, _319158, _319160]))], (785 ^ _286175) ^ [] : [-(para(773 ^ [_319152, _319154, _319156, _319158, _319160], _319156, _319160, _319158))], (787 ^ _286175) ^ [] : [-(cong(_319158, _319156, _319158, 773 ^ [_319152, _319154, _319156, _319158, _319160]))]], cong(_319152, _319156, _319152, _319154), perp(_319160, _319158, _319158, _319152)], (791 ^ _286175) ^ [_319965, _319967, _319969, _319971] : [798 ^ _286175 : [(799 ^ _286175) ^ [] : [-(coll(788 ^ [_319965, _319967, _319969, _319971], _319967, _319969))], (801 ^ _286175) ^ [] : [-(perp(_319971, 788 ^ [_319965, _319967, _319969, _319971], _319967, _319969))], (803 ^ _286175) ^ [] : [-(coll(789 ^ [_319965, _319967, _319969, _319971], _319967, _319971))], (805 ^ _286175) ^ [] : [-(perp(_319969, 789 ^ [_319965, _319967, _319969, _319971], _319967, _319971))]], perp(_319971, _319965, _319969, _319967), perp(_319969, _319965, _319971, _319967)], (808 ^ _286175) ^ [_320710, _320712, _320714, _320716] : [circle(_320710, _320716, _320714, _320712), -(perp(806 ^ [_320710, _320712, _320714, _320716], _320716, _320716, _320710))], (816 ^ _286175) ^ [_321263, _321265, _321267, _321269, _321271, _321273] : [831 ^ _286175 : [(832 ^ _286175) ^ [] : [-(coll(813 ^ [_321263, _321265, _321267, _321269, _321271, _321273], _321273, _321269))], (834 ^ _286175) ^ [] : [-(cong(813 ^ [_321263, _321265, _321267, _321269, _321271, _321273], _321263, _321263, _321273))], (836 ^ _286175) ^ [] : [-(coll(814 ^ [_321263, _321265, _321267, _321269, _321271, _321273], _321271, _321267))], (838 ^ _286175) ^ [] : [-(cong(814 ^ [_321263, _321265, _321267, _321269, _321271, _321273], _321263, _321263, _321273))]], circle(_321265, _321273, _321271, _321269), cong(_321265, _321273, _321265, _321267), cong(_321263, _321273, _321263, _321271), -(_321265 = _321263)], (841 ^ _286175) ^ [_322320, _322322, _322324, _322326, _322328] : [-(circle(839 ^ [_322320, _322322, _322324, _322326, _322328], _322328, _322326, _322324)), cyclic(_322328, _322326, _322324, _322322), para(_322328, _322326, _322324, _322322), midp(_322320, _322328, _322326)], (856 ^ _286175) ^ [_322881, _322883, _322885, _322887] : [-(circle(854 ^ [_322881, _322883, _322885, _322887], _322887, _322885, _322883)), perp(_322887, _322883, _322883, _322885), cyclic(_322887, _322885, _322883, _322881)], (867 ^ _286175) ^ [_323347, _323349, _323351, _323353, _323355] : [874 ^ _286175 : [(875 ^ _286175) ^ [] : [-(coll(865 ^ [_323347, _323349, _323351, _323353, _323355], _323349, _323347))], (877 ^ _286175) ^ [] : [-(perp(865 ^ [_323347, _323349, _323351, _323353, _323355], _323355, _323349, _323347))]], perp(_323355, _323351, _323351, _323353), coll(_323353, _323349, _323347)], (880 ^ _286175) ^ [_323934, _323936, _323938, _323940, _323942] : [-(midp(878 ^ [_323934, _323936, _323938, _323940, _323942], _323942, _323938)), perp(_323942, _323940, _323942, _323938), perp(_323938, _323942, _323938, _323936), midp(_323934, _323940, _323936)], (895 ^ _286175) ^ [_324484, _324486, _324488] : [902 ^ _286175 : [(903 ^ _286175) ^ [] : [-(coll(_324488, _324484, 893 ^ [_324484, _324486, _324488]))], (905 ^ _286175) ^ [] : [-(cong(_324484, _324488, _324484, 893 ^ [_324484, _324486, _324488]))]], cong(_324484, _324488, _324484, _324486), perp(_324488, _324484, _324484, _324486)], (908 ^ _286175) ^ [_325042, _325044, _325046, _325048, _325050, _325052] : [923 ^ _286175 : [(924 ^ _286175) ^ [] : [-(coll(_325044, _325042, 906 ^ [_325042, _325044, _325046, _325048, _325050, _325052]))], (926 ^ _286175) ^ [] : [-(coll(906 ^ [_325042, _325044, _325046, _325048, _325050, _325052], _325048, _325046))]], para(_325052, _325050, _325048, _325046), coll(_325044, _325052, _325048), coll(_325044, _325050, _325046), coll(_325042, _325052, _325050)]], input).
% 153.17/148.21 ncf('1',plain,[cyclic(932 ^ [], 934 ^ [], 937 ^ [], 935 ^ [])],start(967 ^ 0)).
% 153.17/148.21 ncf('1.1',plain,[-(cyclic(932 ^ [], 934 ^ [], 937 ^ [], 935 ^ [])), cyclic(932 ^ [], 932 ^ [], 934 ^ [], 937 ^ []), cyclic(932 ^ [], 932 ^ [], 934 ^ [], 935 ^ [])],extension(126 ^ 1,bind([[_291259, _291261, _291263, _291265, _291267], [935 ^ [], 937 ^ [], 934 ^ [], 932 ^ [], 932 ^ []]]))).
% 153.17/148.21 ncf('1.1.1',plain,[-(cyclic(932 ^ [], 932 ^ [], 934 ^ [], 937 ^ [])), eqangle(934 ^ [], 932 ^ [], 934 ^ [], 932 ^ [], 937 ^ [], 932 ^ [], 937 ^ [], 932 ^ []), -(coll(934 ^ [], 937 ^ [], 932 ^ []))],extension(300 ^ 2,bind([[_300229, _300231, _300233, _300235], [937 ^ [], 934 ^ [], 932 ^ [], 932 ^ []]]))).
% 153.17/148.21 ncf('1.1.1.1',plain,[-(eqangle(934 ^ [], 932 ^ [], 934 ^ [], 932 ^ [], 937 ^ [], 932 ^ [], 937 ^ [], 932 ^ [])), eqangle(934 ^ [], 932 ^ [], 937 ^ [], 932 ^ [], 934 ^ [], 932 ^ [], 937 ^ [], 932 ^ [])],extension(154 ^ 3,bind([[_292746, _292748, _292750, _292752, _292754, _292756, _292758, _292760], [932 ^ [], 937 ^ [], 932 ^ [], 934 ^ [], 932 ^ [], 937 ^ [], 932 ^ [], 934 ^ []]]))).
% 153.17/148.21 ncf('1.1.1.1.1',plain,[-(eqangle(934 ^ [], 932 ^ [], 937 ^ [], 932 ^ [], 934 ^ [], 932 ^ [], 937 ^ [], 932 ^ [])), para(934 ^ [], 932 ^ [], 934 ^ [], 932 ^ [])],extension(288 ^ 4,bind([[_299685, _299687, _299689, _299691, _299693, _299695], [932 ^ [], 937 ^ [], 932 ^ [], 934 ^ [], 932 ^ [], 934 ^ []]]))).
% 153.17/148.21 ncf('1.1.1.1.1.1',plain,[-(para(934 ^ [], 932 ^ [], 934 ^ [], 932 ^ [])), perp(934 ^ [], 932 ^ [], 927 ^ [], 928 ^ []), perp(927 ^ [], 928 ^ [], 934 ^ [], 932 ^ [])],extension(58 ^ 5,bind([[_288604, _288606, _288608, _288610, _288612, _288614], [932 ^ [], 934 ^ [], 928 ^ [], 927 ^ [], 932 ^ [], 934 ^ []]]))).
% 153.17/148.21 ncf('1.1.1.1.1.1.1',plain,[-(perp(934 ^ [], 932 ^ [], 927 ^ [], 928 ^ []))],extension(951 ^ 6)).
% 153.17/148.21 ncf('1.1.1.1.1.1.2',plain,[-(perp(927 ^ [], 928 ^ [], 934 ^ [], 932 ^ [])), perp(934 ^ [], 932 ^ [], 927 ^ [], 928 ^ [])],extension(52 ^ 6,bind([[_288318, _288320, _288322, _288324], [928 ^ [], 927 ^ [], 932 ^ [], 934 ^ []]]))).
% 153.17/148.21 ncf('1.1.1.1.1.1.2.1',plain,[-(perp(934 ^ [], 932 ^ [], 927 ^ [], 928 ^ []))],lemmata('[1, 1, 1, 1, 1].x')).
% 153.17/148.21 ncf('1.1.1.2',plain,[coll(934 ^ [], 937 ^ [], 932 ^ []), -(coll(937 ^ [], 934 ^ [], 932 ^ []))],extension(8 ^ 3,bind([[_286536, _286538, _286540], [932 ^ [], 937 ^ [], 934 ^ []]]))).
% 153.17/148.21 ncf('1.1.1.2.1',plain,[coll(937 ^ [], 934 ^ [], 932 ^ []), -(coll(932 ^ [], 932 ^ [], 937 ^ [])), coll(937 ^ [], 934 ^ [], 932 ^ [])],extension(14 ^ 4,bind([[_286784, _286786, _286788, _286790], [932 ^ [], 932 ^ [], 934 ^ [], 937 ^ []]]))).
% 153.17/148.21 ncf('1.1.1.2.1.1',plain,[coll(932 ^ [], 932 ^ [], 937 ^ []), -(coll(934 ^ [], 937 ^ [], 932 ^ [])), coll(932 ^ [], 932 ^ [], 934 ^ [])],extension(14 ^ 5,bind([[_286784, _286786, _286788, _286790], [937 ^ [], 934 ^ [], 932 ^ [], 932 ^ []]]))).
% 153.17/148.21 ncf('1.1.1.2.1.1.1',plain,[coll(934 ^ [], 937 ^ [], 932 ^ []), -(cyclic(932 ^ [], 932 ^ [], 934 ^ [], 937 ^ [])), eqangle(934 ^ [], 932 ^ [], 934 ^ [], 932 ^ [], 937 ^ [], 932 ^ [], 937 ^ [], 932 ^ [])],extension(310 ^ 6,bind([[_300597, _300599, _300601, _300603], [937 ^ [], 934 ^ [], 932 ^ [], 932 ^ []]]))).
% 153.17/148.21 ncf('1.1.1.2.1.1.1.1',plain,[cyclic(932 ^ [], 932 ^ [], 934 ^ [], 937 ^ [])],reduction('1.1')).
% 153.17/148.21 ncf('1.1.1.2.1.1.1.2',plain,[-(eqangle(934 ^ [], 932 ^ [], 934 ^ [], 932 ^ [], 937 ^ [], 932 ^ [], 937 ^ [], 932 ^ []))],lemmata('[1, 1].x')).
% 153.17/148.21 ncf('1.1.1.2.1.1.2',plain,[-(coll(932 ^ [], 932 ^ [], 934 ^ [])), coll(934 ^ [], 937 ^ [], 932 ^ []), coll(934 ^ [], 937 ^ [], 932 ^ [])],extension(14 ^ 6,bind([[_286784, _286786, _286788, _286790], [932 ^ [], 932 ^ [], 937 ^ [], 934 ^ []]]))).
% 153.17/148.21 ncf('1.1.1.2.1.1.2.1',plain,[-(coll(934 ^ [], 937 ^ [], 932 ^ []))],reduction('1.1.1')).
% 153.17/148.21 ncf('1.1.1.2.1.1.2.2',plain,[-(coll(934 ^ [], 937 ^ [], 932 ^ []))],reduction('1.1.1')).
% 153.17/148.21 ncf('1.1.1.2.1.2',plain,[-(coll(937 ^ [], 934 ^ [], 932 ^ []))],reduction('1.1.1.2')).
% 153.17/148.21 ncf('1.1.2',plain,[-(cyclic(932 ^ [], 932 ^ [], 934 ^ [], 935 ^ [])), eqangle(934 ^ [], 932 ^ [], 934 ^ [], 932 ^ [], 935 ^ [], 932 ^ [], 935 ^ [], 932 ^ []), -(coll(934 ^ [], 935 ^ [], 932 ^ []))],extension(300 ^ 2,bind([[_300229, _300231, _300233, _300235], [935 ^ [], 934 ^ [], 932 ^ [], 932 ^ []]]))).
% 153.17/148.21 ncf('1.1.2.1',plain,[-(eqangle(934 ^ [], 932 ^ [], 934 ^ [], 932 ^ [], 935 ^ [], 932 ^ [], 935 ^ [], 932 ^ [])), eqangle(934 ^ [], 932 ^ [], 935 ^ [], 932 ^ [], 934 ^ [], 932 ^ [], 935 ^ [], 932 ^ [])],extension(154 ^ 3,bind([[_292746, _292748, _292750, _292752, _292754, _292756, _292758, _292760], [932 ^ [], 935 ^ [], 932 ^ [], 934 ^ [], 932 ^ [], 935 ^ [], 932 ^ [], 934 ^ []]]))).
% 153.17/148.21 ncf('1.1.2.1.1',plain,[-(eqangle(934 ^ [], 932 ^ [], 935 ^ [], 932 ^ [], 934 ^ [], 932 ^ [], 935 ^ [], 932 ^ [])), para(934 ^ [], 932 ^ [], 934 ^ [], 932 ^ [])],extension(288 ^ 4,bind([[_299685, _299687, _299689, _299691, _299693, _299695], [932 ^ [], 935 ^ [], 932 ^ [], 934 ^ [], 932 ^ [], 934 ^ []]]))).
% 153.17/148.21 ncf('1.1.2.1.1.1',plain,[-(para(934 ^ [], 932 ^ [], 934 ^ [], 932 ^ [])), perp(934 ^ [], 932 ^ [], 927 ^ [], 928 ^ []), perp(927 ^ [], 928 ^ [], 934 ^ [], 932 ^ [])],extension(58 ^ 5,bind([[_288604, _288606, _288608, _288610, _288612, _288614], [932 ^ [], 934 ^ [], 928 ^ [], 927 ^ [], 932 ^ [], 934 ^ []]]))).
% 153.17/148.21 ncf('1.1.2.1.1.1.1',plain,[-(perp(934 ^ [], 932 ^ [], 927 ^ [], 928 ^ []))],extension(951 ^ 6)).
% 153.17/148.21 ncf('1.1.2.1.1.1.2',plain,[-(perp(927 ^ [], 928 ^ [], 934 ^ [], 932 ^ [])), perp(934 ^ [], 932 ^ [], 927 ^ [], 928 ^ [])],extension(52 ^ 6,bind([[_288318, _288320, _288322, _288324], [928 ^ [], 927 ^ [], 932 ^ [], 934 ^ []]]))).
% 153.17/148.21 ncf('1.1.2.1.1.1.2.1',plain,[-(perp(934 ^ [], 932 ^ [], 927 ^ [], 928 ^ []))],lemmata('[1, 1, 2, 1, 1].x')).
% 153.17/148.21 ncf('1.1.2.2',plain,[coll(934 ^ [], 935 ^ [], 932 ^ []), -(coll(935 ^ [], 934 ^ [], 932 ^ []))],extension(8 ^ 3,bind([[_286536, _286538, _286540], [932 ^ [], 935 ^ [], 934 ^ []]]))).
% 153.17/148.21 ncf('1.1.2.2.1',plain,[coll(935 ^ [], 934 ^ [], 932 ^ []), -(coll(932 ^ [], 932 ^ [], 935 ^ [])), coll(935 ^ [], 934 ^ [], 932 ^ [])],extension(14 ^ 4,bind([[_286784, _286786, _286788, _286790], [932 ^ [], 932 ^ [], 934 ^ [], 935 ^ []]]))).
% 153.17/148.21 ncf('1.1.2.2.1.1',plain,[coll(932 ^ [], 932 ^ [], 935 ^ []), -(coll(934 ^ [], 935 ^ [], 932 ^ [])), coll(932 ^ [], 932 ^ [], 934 ^ [])],extension(14 ^ 5,bind([[_286784, _286786, _286788, _286790], [935 ^ [], 934 ^ [], 932 ^ [], 932 ^ []]]))).
% 153.17/148.21 ncf('1.1.2.2.1.1.1',plain,[coll(934 ^ [], 935 ^ [], 932 ^ []), -(cyclic(932 ^ [], 932 ^ [], 934 ^ [], 935 ^ [])), eqangle(934 ^ [], 932 ^ [], 934 ^ [], 932 ^ [], 935 ^ [], 932 ^ [], 935 ^ [], 932 ^ [])],extension(310 ^ 6,bind([[_300597, _300599, _300601, _300603], [935 ^ [], 934 ^ [], 932 ^ [], 932 ^ []]]))).
% 153.17/148.21 ncf('1.1.2.2.1.1.1.1',plain,[cyclic(932 ^ [], 932 ^ [], 934 ^ [], 935 ^ [])],reduction('1.1')).
% 153.17/148.21 ncf('1.1.2.2.1.1.1.2',plain,[-(eqangle(934 ^ [], 932 ^ [], 934 ^ [], 932 ^ [], 935 ^ [], 932 ^ [], 935 ^ [], 932 ^ []))],lemmata('[1, 1].x')).
% 153.17/148.21 ncf('1.1.2.2.1.1.2',plain,[-(coll(932 ^ [], 932 ^ [], 934 ^ [])), coll(934 ^ [], 935 ^ [], 932 ^ []), coll(934 ^ [], 935 ^ [], 932 ^ [])],extension(14 ^ 6,bind([[_286784, _286786, _286788, _286790], [932 ^ [], 932 ^ [], 935 ^ [], 934 ^ []]]))).
% 153.17/148.21 ncf('1.1.2.2.1.1.2.1',plain,[-(coll(934 ^ [], 935 ^ [], 932 ^ []))],reduction('1.1.2')).
% 153.17/148.21 ncf('1.1.2.2.1.1.2.2',plain,[-(coll(934 ^ [], 935 ^ [], 932 ^ []))],reduction('1.1.2')).
% 153.17/148.21 ncf('1.1.2.2.1.2',plain,[-(coll(935 ^ [], 934 ^ [], 932 ^ []))],reduction('1.1.2.2')).
% 153.17/148.21 %-----------------------------------------------------
% 153.17/148.21 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------