%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO089+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n001.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:11:54 EDT 2023
% Result : Theorem 196.24s 189.56s
% Output : Proof 196.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : GEO089+1 : TPTP v8.1.2. Released v2.4.0.
% 0.10/0.11 % Command : nanocop.sh %s %d
% 0.12/0.31 % Computer : n001.cluster.edu
% 0.12/0.31 % Model : x86_64 x86_64
% 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.31 % Memory : 8042.1875MB
% 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.31 % CPULimit : 300
% 0.12/0.31 % WCLimit : 300
% 0.12/0.31 % DateTime : Fri May 19 04:34:21 EDT 2023
% 0.12/0.31 % CPUTime :
% 196.24/189.56
% 196.24/189.56 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 196.24/189.56 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 196.24/189.56 %-----------------------------------------------------
% 196.24/189.56 ncf(matrix, plain, [(470 ^ _92254) ^ [] : [inner_point(463 ^ [], 462 ^ [])], (468 ^ _92254) ^ [] : [-(inner_point(463 ^ [], 464 ^ []))], (466 ^ _92254) ^ [] : [-(part_of(464 ^ [], 462 ^ []))], !, (114 ^ _76505) ^ [_80234, _80236, _80238, _80240] : [-(sum(_80240, _80236) = sum(_80238, _80234)), _80240 = _80238, _80236 = _80234], (165 ^ _76505) ^ [_82035, _82037, _82039] : [-(_82039 = sum(_82037, _82035)), 169 ^ _76505 : [(174 ^ _76505) ^ [] : [incident_c(166 ^ [_82035, _82037, _82039], _82035)], (172 ^ _76505) ^ [] : [incident_c(166 ^ [_82035, _82037, _82039], _82037)], (170 ^ _76505) ^ [] : [-(incident_c(166 ^ [_82035, _82037, _82039], _82039))]], 175 ^ _76505 : [(176 ^ _76505) ^ [] : [-(incident_c(166 ^ [_82035, _82037, _82039], _82037)), -(incident_c(166 ^ [_82035, _82037, _82039], _82035))], (182 ^ _76505) ^ [] : [incident_c(166 ^ [_82035, _82037, _82039], _82039)]]], (382 ^ _76505) ^ [_89239, _89241] : [inner_point(_89239, _89241), 387 ^ _76505 : [(390 ^ _76505) ^ [] : [-(_89241 = sum(385 ^ [_89239, _89241], 386 ^ [_89239, _89241]))], (388 ^ _76505) ^ [] : [-(meet(_89239, 385 ^ [_89239, _89241], 386 ^ [_89239, _89241]))]]], (254 ^ _76505) ^ [_85183, _85185, _85187] : [meet(_85187, _85185, _85183), 257 ^ _76505 : [(262 ^ _76505) ^ [_85486] : [269 ^ _76505 : [(272 ^ _76505) ^ [] : [-(end_point(_85486, _85183))], (270 ^ _76505) ^ [] : [-(end_point(_85486, _85185))]], incident_c(_85486, _85185), incident_c(_85486, _85183)], (260 ^ _76505) ^ [] : [-(incident_c(_85187, _85183))], (258 ^ _76505) ^ [] : [-(incident_c(_85187, _85185))]]], (317 ^ _76505) ^ [_87283] : [318 ^ _76505 : [(319 ^ _76505) ^ [_87350] : [end_point(_87350, _87283)]], -(open(_87283))], (303 ^ _76505) ^ [_86805] : [-(end_point(304 ^ [_86805], _86805)), -(closed(_86805))], (244 ^ _76505) ^ [_84836, _84838] : [-(inner_point(_84838, _84836)), incident_c(_84838, _84836), -(end_point(_84838, _84836))], (86 ^ _76505) ^ [_79368, _79370, _79372, _79374] : [-(part_of(_79372, _79368)), part_of(_79374, _79370), _79374 = _79372, _79370 = _79368], (297 ^ _76505) ^ [_86628] : [closed(_86628), 300 ^ _76505 : [(301 ^ _76505) ^ [_86739] : [end_point(_86739, _86628)]]], (323 ^ _76505) ^ [_87509, _87511] : [-(open(_87509)), part_of(_87509, _87511), -(_87509 = _87511)], (392 ^ _76505) ^ [_89727, _89729, _89731, _89733] : [end_point(_89731, _89733), end_point(_89729, _89733), end_point(_89727, _89733), -(_89731 = _89729), -(_89731 = _89727), -(_89729 = _89727)], (236 ^ _76505) ^ [_84598, _84600] : [inner_point(_84600, _84598), 239 ^ _76505 : [(242 ^ _76505) ^ [] : [end_point(_84600, _84598)], (240 ^ _76505) ^ [] : [-(incident_c(_84600, _84598))]]], (124 ^ _76505) ^ [_80596, _80598] : [part_of(_80596, _80598), 127 ^ _76505 : [(128 ^ _76505) ^ [_80733] : [incident_c(_80733, _80596), -(incident_c(_80733, _80598))]]], (380 ^ _76505) ^ [_89127] : [-(inner_point(378 ^ [_89127], _89127))], (20 ^ _76505) ^ [_77253, _77255] : [-(open(_77253)), _77255 = _77253, open(_77255)], (441 ^ _76505) ^ [_91318, _91320] : [442 ^ _76505 : [(443 ^ _76505) ^ [_91397] : [meet(_91397, _91320, _91318)]], -(444 ^ [_91318, _91320] = sum(_91320, _91318))], (448 ^ _76505) ^ [_91598, _91600] : [-(_91600 = _91598), 452 ^ _76505 : [(455 ^ _76505) ^ [] : [incident_c(449 ^ [_91598, _91600], _91598)], (453 ^ _76505) ^ [] : [-(incident_c(449 ^ [_91598, _91600], _91600))]], 456 ^ _76505 : [(459 ^ _76505) ^ [] : [incident_c(449 ^ [_91598, _91600], _91600)], (457 ^ _76505) ^ [] : [-(incident_c(449 ^ [_91598, _91600], _91598))]]], (100 ^ _76505) ^ [_79792, _79794, _79796, _79798] : [-(inner_point(_79796, _79792)), inner_point(_79798, _79794), _79798 = _79796, _79794 = _79792], (134 ^ _76505) ^ [_80910, _80912] : [136 ^ _76505 : [(139 ^ _76505) ^ [] : [incident_c(135 ^ [_80910, _80912], _80912)], (137 ^ _76505) ^ [] : [-(incident_c(135 ^ [_80910, _80912], _80910))]], -(part_of(_80910, _80912))], (10 ^ _76505) ^ [_76940, _76942, _76944] : [-(_76944 = _76940), _76944 = _76942, _76942 = _76940], (414 ^ _76505) ^ [_90343, _90345] : [end_point(_90343, _90345), 418 ^ _76505 : [(421 ^ _76505) ^ [] : [_90343 = 417 ^ [_90343, _90345]], (419 ^ _76505) ^ [] : [-(end_point(417 ^ [_90343, _90345], _90345))]]], (274 ^ _76505) ^ [_85851, _85853, _85855] : [-(meet(_85855, _85853, _85851)), incident_c(_85855, _85853), incident_c(_85855, _85851), 284 ^ _76505 : [(289 ^ _76505) ^ [] : [end_point(283 ^ [_85851, _85853, _85855], _85853), end_point(283 ^ [_85851, _85853, _85855], _85851)], (287 ^ _76505) ^ [] : [-(incident_c(283 ^ [_85851, _85853, _85855], _85851))], (285 ^ _76505) ^ [] : [-(incident_c(283 ^ [_85851, _85853, _85855], _85853))]]], (423 ^ _76505) ^ [_90729, _90731, _90733, _90735] : [434 ^ _76505 : [(435 ^ _76505) ^ [_91075] : [end_point(_91075, _90733), -(meet(_91075, _90733, _90731))]], closed(_90735), meet(_90729, _90733, _90731), _90735 = sum(_90733, _90731)], (186 ^ _76505) ^ [_82815, _82817] : [end_point(_82817, _82815), 189 ^ _76505 : [(192 ^ _76505) ^ [_83067, _83069] : [-(part_of(_83069, _83067)), -(part_of(_83067, _83069)), part_of(_83069, _82815), part_of(_83067, _82815), incident_c(_82817, _83069), incident_c(_82817, _83067)], (190 ^ _76505) ^ [] : [-(incident_c(_82817, _82815))]]], (30 ^ _76505) ^ [_77548, _77550] : [-(closed(_77548)), _77550 = _77548, closed(_77550)], (2 ^ _76505) ^ [_76629] : [-(_76629 = _76629)], (4 ^ _76505) ^ [_76736, _76738] : [_76738 = _76736, -(_76736 = _76738)], (333 ^ _76505) ^ [_87837, _87839, _87841, _87843] : [part_of(_87841, _87843), part_of(_87839, _87843), part_of(_87837, _87843), 346 ^ _76505 : [(347 ^ _76505) ^ [_88248] : [end_point(_88248, _87841), end_point(_88248, _87839), end_point(_88248, _87837)]], -(part_of(_87839, _87837)), -(part_of(_87837, _87839)), -(part_of(_87841, _87839)), -(part_of(_87839, _87841)), -(part_of(_87841, _87837)), -(part_of(_87837, _87841))], (40 ^ _76505) ^ [_77871, _77873, _77875, _77877] : [-(end_point(_77875, _77871)), end_point(_77877, _77873), _77877 = _77875, _77873 = _77871], (310 ^ _76505) ^ [_87078] : [open(_87078), -(end_point(313 ^ [_87078], _87078))], (143 ^ _76505) ^ [_81310, _81312, _81314] : [_81314 = sum(_81312, _81310), 146 ^ _76505 : [(147 ^ _76505) ^ [_81492] : [incident_c(_81492, _81314), -(incident_c(_81492, _81312)), -(incident_c(_81492, _81310))], (157 ^ _76505) ^ [_81770] : [158 ^ _76505 : [(161 ^ _76505) ^ [] : [incident_c(_81770, _81310)], (159 ^ _76505) ^ [] : [incident_c(_81770, _81312)]], -(incident_c(_81770, _81314))]]], (72 ^ _76505) ^ [_78924, _78926, _78928, _78930] : [-(incident_c(_78928, _78924)), incident_c(_78930, _78926), _78930 = _78928, _78926 = _78924], (214 ^ _76505) ^ [_83643, _83645] : [-(end_point(_83645, _83643)), incident_c(_83645, _83643), 221 ^ _76505 : [(230 ^ _76505) ^ [] : [part_of(219 ^ [_83643, _83645], 220 ^ [_83643, _83645])], (228 ^ _76505) ^ [] : [-(incident_c(_83645, 220 ^ [_83643, _83645]))], (232 ^ _76505) ^ [] : [part_of(220 ^ [_83643, _83645], 219 ^ [_83643, _83645])], (222 ^ _76505) ^ [] : [-(part_of(219 ^ [_83643, _83645], _83643))], (224 ^ _76505) ^ [] : [-(part_of(220 ^ [_83643, _83645], _83643))], (226 ^ _76505) ^ [] : [-(incident_c(_83645, 219 ^ [_83643, _83645]))]]], (54 ^ _76505) ^ [_78343, _78345, _78347, _78349, _78351, _78353] : [-(meet(_78351, _78347, _78343)), meet(_78353, _78349, _78345), _78353 = _78351, _78349 = _78347, _78345 = _78343]], input).
% 196.24/189.56 ncf('1',plain,[inner_point(463 ^ [], 462 ^ [])],start(470 ^ 0)).
% 196.24/189.56 ncf('1.1',plain,[-(inner_point(463 ^ [], 462 ^ [])), incident_c(463 ^ [], 462 ^ []), -(end_point(463 ^ [], 462 ^ []))],extension(244 ^ 1,bind([[_84836, _84838], [462 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.1',plain,[-(incident_c(463 ^ [], 462 ^ [])), 128 : incident_c(463 ^ [], 386 ^ [463 ^ [], 464 ^ []]), 128 : part_of(386 ^ [463 ^ [], 464 ^ []], 462 ^ [])],extension(124 ^ 2,bind([[_80596, _80598, _80733], [386 ^ [463 ^ [], 464 ^ []], 462 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.1.1',plain,[-(incident_c(463 ^ [], 386 ^ [463 ^ [], 464 ^ []])), meet(463 ^ [], 385 ^ [463 ^ [], 464 ^ []], 386 ^ [463 ^ [], 464 ^ []])],extension(254 ^ 5,bind([[_85183, _85185, _85187], [386 ^ [463 ^ [], 464 ^ []], 385 ^ [463 ^ [], 464 ^ []], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.1.1.1',plain,[-(meet(463 ^ [], 385 ^ [463 ^ [], 464 ^ []], 386 ^ [463 ^ [], 464 ^ []])), inner_point(463 ^ [], 464 ^ [])],extension(382 ^ 6,bind([[_89239, _89241], [463 ^ [], 464 ^ []]]))).
% 196.24/189.56 ncf('1.1.1.1.1.1',plain,[-(inner_point(463 ^ [], 464 ^ []))],extension(468 ^ 7)).
% 196.24/189.56 ncf('1.1.1.2',plain,[-(part_of(386 ^ [463 ^ [], 464 ^ []], 462 ^ [])), 137 : -(incident_c(135 ^ [386 ^ [463 ^ [], 464 ^ []], 462 ^ []], 386 ^ [463 ^ [], 464 ^ []]))],extension(134 ^ 3,bind([[_80910, _80912], [386 ^ [463 ^ [], 464 ^ []], 462 ^ []]]))).
% 196.24/189.56 ncf('1.1.1.2.1',plain,[incident_c(135 ^ [386 ^ [463 ^ [], 464 ^ []], 462 ^ []], 386 ^ [463 ^ [], 464 ^ []]), 157 : -(incident_c(135 ^ [386 ^ [463 ^ [], 464 ^ []], 462 ^ []], 464 ^ [])), 157 : 464 ^ [] = sum(385 ^ [463 ^ [], 464 ^ []], 386 ^ [463 ^ [], 464 ^ []])],extension(143 ^ 6,bind([[_81310, _81312, _81314, _81770], [386 ^ [463 ^ [], 464 ^ []], 385 ^ [463 ^ [], 464 ^ []], 464 ^ [], 135 ^ [386 ^ [463 ^ [], 464 ^ []], 462 ^ []]]]))).
% 196.24/189.56 ncf('1.1.1.2.1.1',plain,[incident_c(135 ^ [386 ^ [463 ^ [], 464 ^ []], 462 ^ []], 464 ^ []), 128 : -(incident_c(135 ^ [386 ^ [463 ^ [], 464 ^ []], 462 ^ []], 462 ^ [])), 128 : part_of(464 ^ [], 462 ^ [])],extension(124 ^ 9,bind([[_80596, _80598, _80733], [464 ^ [], 462 ^ [], 135 ^ [386 ^ [463 ^ [], 464 ^ []], 462 ^ []]]]))).
% 196.24/189.56 ncf('1.1.1.2.1.1.1',plain,[incident_c(135 ^ [386 ^ [463 ^ [], 464 ^ []], 462 ^ []], 462 ^ [])],extension(139 ^ 12)).
% 196.24/189.56 ncf('1.1.1.2.1.1.2',plain,[-(part_of(464 ^ [], 462 ^ []))],extension(466 ^ 10)).
% 196.24/189.56 ncf('1.1.1.2.1.2',plain,[-(464 ^ [] = sum(385 ^ [463 ^ [], 464 ^ []], 386 ^ [463 ^ [], 464 ^ []])), inner_point(463 ^ [], 464 ^ [])],extension(382 ^ 7,bind([[_89239, _89241], [463 ^ [], 464 ^ []]]))).
% 196.24/189.56 ncf('1.1.1.2.1.2.1',plain,[-(inner_point(463 ^ [], 464 ^ []))],extension(468 ^ 8)).
% 196.24/189.56 ncf('1.1.2',plain,[end_point(463 ^ [], 462 ^ []), 192 : -(part_of(219 ^ [464 ^ [], 463 ^ []], 220 ^ [464 ^ [], 463 ^ []])), 192 : -(part_of(220 ^ [464 ^ [], 463 ^ []], 219 ^ [464 ^ [], 463 ^ []])), 192 : part_of(219 ^ [464 ^ [], 463 ^ []], 462 ^ []), 192 : part_of(220 ^ [464 ^ [], 463 ^ []], 462 ^ []), 192 : incident_c(463 ^ [], 219 ^ [464 ^ [], 463 ^ []]), 192 : incident_c(463 ^ [], 220 ^ [464 ^ [], 463 ^ []])],extension(186 ^ 2,bind([[_82815, _82817, _83067, _83069], [462 ^ [], 463 ^ [], 220 ^ [464 ^ [], 463 ^ []], 219 ^ [464 ^ [], 463 ^ []]]]))).
% 196.24/189.56 ncf('1.1.2.1',plain,[part_of(219 ^ [464 ^ [], 463 ^ []], 220 ^ [464 ^ [], 463 ^ []]), -(end_point(463 ^ [], 464 ^ [])), incident_c(463 ^ [], 464 ^ [])],extension(214 ^ 5,bind([[_83643, _83645], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.1.1',plain,[end_point(463 ^ [], 464 ^ []), end_point(463 ^ [], 464 ^ []), end_point(463 ^ [], 464 ^ []), -(463 ^ [] = 463 ^ []), -(463 ^ [] = 463 ^ []), -(463 ^ [] = 463 ^ [])],extension(392 ^ 6,bind([[_89727, _89729, _89731, _89733], [463 ^ [], 463 ^ [], 463 ^ [], 464 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.1.1.1',plain,[-(end_point(463 ^ [], 464 ^ []))],reduction('1.1.2.1')).
% 196.24/189.56 ncf('1.1.2.1.1.2',plain,[-(end_point(463 ^ [], 464 ^ []))],reduction('1.1.2.1')).
% 196.24/189.56 ncf('1.1.2.1.1.3',plain,[463 ^ [] = 463 ^ [], -(end_point(463 ^ [], 464 ^ [])), end_point(463 ^ [], 464 ^ []), 464 ^ [] = 464 ^ []],extension(40 ^ 7,bind([[_77871, _77873, _77875, _77877], [464 ^ [], 464 ^ [], 463 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.1.1.3.1',plain,[end_point(463 ^ [], 464 ^ []), inner_point(463 ^ [], 464 ^ [])],extension(236 ^ 8,bind([[_84598, _84600], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.1.1.3.1.1',plain,[-(inner_point(463 ^ [], 464 ^ []))],extension(468 ^ 9)).
% 196.24/189.56 ncf('1.1.2.1.1.3.2',plain,[-(end_point(463 ^ [], 464 ^ []))],reduction('1.1.2.1')).
% 196.24/189.56 ncf('1.1.2.1.1.3.3',plain,[-(464 ^ [] = 464 ^ [])],extension(2 ^ 8,bind([[_76629], [464 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.1.1.4',plain,[463 ^ [] = 463 ^ []],lemmata('[1, 2, 1, 1].x')).
% 196.24/189.56 ncf('1.1.2.1.1.5',plain,[463 ^ [] = 463 ^ []],lemmata('[1, 2, 1, 1].x')).
% 196.24/189.56 ncf('1.1.2.1.2',plain,[-(incident_c(463 ^ [], 464 ^ [])), inner_point(463 ^ [], 464 ^ [])],extension(236 ^ 6,bind([[_84598, _84600], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.1.2.1',plain,[-(inner_point(463 ^ [], 464 ^ []))],extension(468 ^ 7)).
% 196.24/189.56 ncf('1.1.2.2',plain,[part_of(220 ^ [464 ^ [], 463 ^ []], 219 ^ [464 ^ [], 463 ^ []]), -(end_point(463 ^ [], 464 ^ [])), incident_c(463 ^ [], 464 ^ [])],extension(214 ^ 5,bind([[_83643, _83645], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.2.1',plain,[end_point(463 ^ [], 464 ^ []), end_point(463 ^ [], 464 ^ []), end_point(463 ^ [], 464 ^ []), -(463 ^ [] = 463 ^ []), -(463 ^ [] = 463 ^ []), -(463 ^ [] = 463 ^ [])],extension(392 ^ 6,bind([[_89727, _89729, _89731, _89733], [463 ^ [], 463 ^ [], 463 ^ [], 464 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.2.1.1',plain,[-(end_point(463 ^ [], 464 ^ []))],reduction('1.1.2.2')).
% 196.24/189.56 ncf('1.1.2.2.1.2',plain,[-(end_point(463 ^ [], 464 ^ []))],reduction('1.1.2.2')).
% 196.24/189.56 ncf('1.1.2.2.1.3',plain,[463 ^ [] = 463 ^ [], -(end_point(463 ^ [], 464 ^ [])), end_point(463 ^ [], 464 ^ []), 464 ^ [] = 464 ^ []],extension(40 ^ 7,bind([[_77871, _77873, _77875, _77877], [464 ^ [], 464 ^ [], 463 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.2.1.3.1',plain,[end_point(463 ^ [], 464 ^ []), inner_point(463 ^ [], 464 ^ [])],extension(236 ^ 8,bind([[_84598, _84600], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.2.1.3.1.1',plain,[-(inner_point(463 ^ [], 464 ^ []))],extension(468 ^ 9)).
% 196.24/189.56 ncf('1.1.2.2.1.3.2',plain,[-(end_point(463 ^ [], 464 ^ []))],reduction('1.1.2.2')).
% 196.24/189.56 ncf('1.1.2.2.1.3.3',plain,[-(464 ^ [] = 464 ^ [])],extension(2 ^ 8,bind([[_76629], [464 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.2.1.4',plain,[463 ^ [] = 463 ^ []],lemmata('[2, 2, 1, 1].x')).
% 196.24/189.56 ncf('1.1.2.2.1.5',plain,[463 ^ [] = 463 ^ []],lemmata('[2, 2, 1, 1].x')).
% 196.24/189.56 ncf('1.1.2.2.2',plain,[-(incident_c(463 ^ [], 464 ^ [])), inner_point(463 ^ [], 464 ^ [])],extension(236 ^ 6,bind([[_84598, _84600], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.2.2.1',plain,[-(inner_point(463 ^ [], 464 ^ []))],extension(468 ^ 7)).
% 196.24/189.56 ncf('1.1.2.3',plain,[-(part_of(219 ^ [464 ^ [], 463 ^ []], 462 ^ [])), 137 : -(incident_c(135 ^ [219 ^ [464 ^ [], 463 ^ []], 462 ^ []], 219 ^ [464 ^ [], 463 ^ []]))],extension(134 ^ 5,bind([[_80910, _80912], [219 ^ [464 ^ [], 463 ^ []], 462 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.3.1',plain,[incident_c(135 ^ [219 ^ [464 ^ [], 463 ^ []], 462 ^ []], 219 ^ [464 ^ [], 463 ^ []]), 128 : -(incident_c(135 ^ [219 ^ [464 ^ [], 463 ^ []], 462 ^ []], 464 ^ [])), 128 : part_of(219 ^ [464 ^ [], 463 ^ []], 464 ^ [])],extension(124 ^ 8,bind([[_80596, _80598, _80733], [219 ^ [464 ^ [], 463 ^ []], 464 ^ [], 135 ^ [219 ^ [464 ^ [], 463 ^ []], 462 ^ []]]]))).
% 196.24/189.56 ncf('1.1.2.3.1.1',plain,[incident_c(135 ^ [219 ^ [464 ^ [], 463 ^ []], 462 ^ []], 464 ^ []), 128 : -(incident_c(135 ^ [219 ^ [464 ^ [], 463 ^ []], 462 ^ []], 462 ^ [])), 128 : part_of(464 ^ [], 462 ^ [])],extension(124 ^ 11,bind([[_80596, _80598, _80733], [464 ^ [], 462 ^ [], 135 ^ [219 ^ [464 ^ [], 463 ^ []], 462 ^ []]]]))).
% 196.24/189.56 ncf('1.1.2.3.1.1.1',plain,[incident_c(135 ^ [219 ^ [464 ^ [], 463 ^ []], 462 ^ []], 462 ^ [])],extension(139 ^ 14)).
% 196.24/189.56 ncf('1.1.2.3.1.1.2',plain,[-(part_of(464 ^ [], 462 ^ []))],extension(466 ^ 12)).
% 196.24/189.56 ncf('1.1.2.3.1.2',plain,[-(part_of(219 ^ [464 ^ [], 463 ^ []], 464 ^ [])), -(end_point(463 ^ [], 464 ^ [])), incident_c(463 ^ [], 464 ^ [])],extension(214 ^ 9,bind([[_83643, _83645], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.3.1.2.1',plain,[end_point(463 ^ [], 464 ^ []), inner_point(463 ^ [], 464 ^ [])],extension(236 ^ 10,bind([[_84598, _84600], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.3.1.2.1.1',plain,[-(inner_point(463 ^ [], 464 ^ []))],extension(468 ^ 11)).
% 196.24/189.56 ncf('1.1.2.3.1.2.2',plain,[-(incident_c(463 ^ [], 464 ^ [])), inner_point(463 ^ [], 464 ^ [])],extension(236 ^ 10,bind([[_84598, _84600], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.3.1.2.2.1',plain,[-(inner_point(463 ^ [], 464 ^ []))],extension(468 ^ 11)).
% 196.24/189.56 ncf('1.1.2.4',plain,[-(part_of(220 ^ [464 ^ [], 463 ^ []], 462 ^ [])), 137 : -(incident_c(135 ^ [220 ^ [464 ^ [], 463 ^ []], 462 ^ []], 220 ^ [464 ^ [], 463 ^ []]))],extension(134 ^ 5,bind([[_80910, _80912], [220 ^ [464 ^ [], 463 ^ []], 462 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.4.1',plain,[incident_c(135 ^ [220 ^ [464 ^ [], 463 ^ []], 462 ^ []], 220 ^ [464 ^ [], 463 ^ []]), 128 : -(incident_c(135 ^ [220 ^ [464 ^ [], 463 ^ []], 462 ^ []], 464 ^ [])), 128 : part_of(220 ^ [464 ^ [], 463 ^ []], 464 ^ [])],extension(124 ^ 8,bind([[_80596, _80598, _80733], [220 ^ [464 ^ [], 463 ^ []], 464 ^ [], 135 ^ [220 ^ [464 ^ [], 463 ^ []], 462 ^ []]]]))).
% 196.24/189.56 ncf('1.1.2.4.1.1',plain,[incident_c(135 ^ [220 ^ [464 ^ [], 463 ^ []], 462 ^ []], 464 ^ []), 128 : -(incident_c(135 ^ [220 ^ [464 ^ [], 463 ^ []], 462 ^ []], 462 ^ [])), 128 : part_of(464 ^ [], 462 ^ [])],extension(124 ^ 11,bind([[_80596, _80598, _80733], [464 ^ [], 462 ^ [], 135 ^ [220 ^ [464 ^ [], 463 ^ []], 462 ^ []]]]))).
% 196.24/189.56 ncf('1.1.2.4.1.1.1',plain,[incident_c(135 ^ [220 ^ [464 ^ [], 463 ^ []], 462 ^ []], 462 ^ [])],extension(139 ^ 14)).
% 196.24/189.56 ncf('1.1.2.4.1.1.2',plain,[-(part_of(464 ^ [], 462 ^ []))],extension(466 ^ 12)).
% 196.24/189.56 ncf('1.1.2.4.1.2',plain,[-(part_of(220 ^ [464 ^ [], 463 ^ []], 464 ^ [])), -(end_point(463 ^ [], 464 ^ [])), incident_c(463 ^ [], 464 ^ [])],extension(214 ^ 9,bind([[_83643, _83645], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.4.1.2.1',plain,[end_point(463 ^ [], 464 ^ []), inner_point(463 ^ [], 464 ^ [])],extension(236 ^ 10,bind([[_84598, _84600], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.4.1.2.1.1',plain,[-(inner_point(463 ^ [], 464 ^ []))],extension(468 ^ 11)).
% 196.24/189.56 ncf('1.1.2.4.1.2.2',plain,[-(incident_c(463 ^ [], 464 ^ [])), inner_point(463 ^ [], 464 ^ [])],extension(236 ^ 10,bind([[_84598, _84600], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.4.1.2.2.1',plain,[-(inner_point(463 ^ [], 464 ^ []))],extension(468 ^ 11)).
% 196.24/189.56 ncf('1.1.2.5',plain,[-(incident_c(463 ^ [], 219 ^ [464 ^ [], 463 ^ []])), -(end_point(463 ^ [], 464 ^ [])), incident_c(463 ^ [], 464 ^ [])],extension(214 ^ 5,bind([[_83643, _83645], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.5.1',plain,[end_point(463 ^ [], 464 ^ []), end_point(463 ^ [], 464 ^ []), end_point(463 ^ [], 464 ^ []), -(463 ^ [] = 463 ^ []), -(463 ^ [] = 463 ^ []), -(463 ^ [] = 463 ^ [])],extension(392 ^ 6,bind([[_89727, _89729, _89731, _89733], [463 ^ [], 463 ^ [], 463 ^ [], 464 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.5.1.1',plain,[-(end_point(463 ^ [], 464 ^ []))],reduction('1.1.2.5')).
% 196.24/189.56 ncf('1.1.2.5.1.2',plain,[-(end_point(463 ^ [], 464 ^ []))],reduction('1.1.2.5')).
% 196.24/189.56 ncf('1.1.2.5.1.3',plain,[463 ^ [] = 463 ^ [], -(end_point(463 ^ [], 464 ^ [])), end_point(463 ^ [], 464 ^ []), 464 ^ [] = 464 ^ []],extension(40 ^ 7,bind([[_77871, _77873, _77875, _77877], [464 ^ [], 464 ^ [], 463 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.5.1.3.1',plain,[end_point(463 ^ [], 464 ^ []), inner_point(463 ^ [], 464 ^ [])],extension(236 ^ 8,bind([[_84598, _84600], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.5.1.3.1.1',plain,[-(inner_point(463 ^ [], 464 ^ []))],extension(468 ^ 9)).
% 196.24/189.56 ncf('1.1.2.5.1.3.2',plain,[-(end_point(463 ^ [], 464 ^ []))],reduction('1.1.2.5')).
% 196.24/189.56 ncf('1.1.2.5.1.3.3',plain,[-(464 ^ [] = 464 ^ [])],extension(2 ^ 8,bind([[_76629], [464 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.5.1.4',plain,[463 ^ [] = 463 ^ []],lemmata('[5, 2, 1, 1].x')).
% 196.24/189.56 ncf('1.1.2.5.1.5',plain,[463 ^ [] = 463 ^ []],lemmata('[5, 2, 1, 1].x')).
% 196.24/189.56 ncf('1.1.2.5.2',plain,[-(incident_c(463 ^ [], 464 ^ [])), inner_point(463 ^ [], 464 ^ [])],extension(236 ^ 6,bind([[_84598, _84600], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.5.2.1',plain,[-(inner_point(463 ^ [], 464 ^ []))],extension(468 ^ 7)).
% 196.24/189.56 ncf('1.1.2.6',plain,[-(incident_c(463 ^ [], 220 ^ [464 ^ [], 463 ^ []])), -(end_point(463 ^ [], 464 ^ [])), incident_c(463 ^ [], 464 ^ [])],extension(214 ^ 5,bind([[_83643, _83645], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.6.1',plain,[end_point(463 ^ [], 464 ^ []), end_point(463 ^ [], 464 ^ []), end_point(463 ^ [], 464 ^ []), -(463 ^ [] = 463 ^ []), -(463 ^ [] = 463 ^ []), -(463 ^ [] = 463 ^ [])],extension(392 ^ 6,bind([[_89727, _89729, _89731, _89733], [463 ^ [], 463 ^ [], 463 ^ [], 464 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.6.1.1',plain,[-(end_point(463 ^ [], 464 ^ []))],reduction('1.1.2.6')).
% 196.24/189.56 ncf('1.1.2.6.1.2',plain,[-(end_point(463 ^ [], 464 ^ []))],reduction('1.1.2.6')).
% 196.24/189.56 ncf('1.1.2.6.1.3',plain,[463 ^ [] = 463 ^ [], -(end_point(463 ^ [], 464 ^ [])), end_point(463 ^ [], 464 ^ []), 464 ^ [] = 464 ^ []],extension(40 ^ 7,bind([[_77871, _77873, _77875, _77877], [464 ^ [], 464 ^ [], 463 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.6.1.3.1',plain,[end_point(463 ^ [], 464 ^ []), inner_point(463 ^ [], 464 ^ [])],extension(236 ^ 8,bind([[_84598, _84600], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.6.1.3.1.1',plain,[-(inner_point(463 ^ [], 464 ^ []))],extension(468 ^ 9)).
% 196.24/189.56 ncf('1.1.2.6.1.3.2',plain,[-(end_point(463 ^ [], 464 ^ []))],reduction('1.1.2.6')).
% 196.24/189.56 ncf('1.1.2.6.1.3.3',plain,[-(464 ^ [] = 464 ^ [])],extension(2 ^ 8,bind([[_76629], [464 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.6.1.4',plain,[463 ^ [] = 463 ^ []],lemmata('[6, 2, 1, 1].x')).
% 196.24/189.56 ncf('1.1.2.6.1.5',plain,[463 ^ [] = 463 ^ []],lemmata('[6, 2, 1, 1].x')).
% 196.24/189.56 ncf('1.1.2.6.2',plain,[-(incident_c(463 ^ [], 464 ^ [])), inner_point(463 ^ [], 464 ^ [])],extension(236 ^ 6,bind([[_84598, _84600], [464 ^ [], 463 ^ []]]))).
% 196.24/189.56 ncf('1.1.2.6.2.1',plain,[-(inner_point(463 ^ [], 464 ^ []))],extension(468 ^ 7)).
% 196.24/189.56 %-----------------------------------------------------
% 196.24/189.56 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------