%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GEO080+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n021.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:53 EDT 2023
% Result : Theorem 0.32s 1.38s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GEO080+1 : TPTP v8.1.2. Released v2.4.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n021.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:27:12 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.32/1.38
% 0.32/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.32/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.32/1.38 %-----------------------------------------------------
% 0.32/1.38 ncf(matrix, plain, [(464 ^ _56532) ^ [] : [part_of(462 ^ [], 462 ^ [])], (114 ^ _56532) ^ [_60281, _60283, _60285, _60287] : [-(sum(_60287, _60283) = sum(_60285, _60281)), _60287 = _60285, _60283 = _60281], (2 ^ _56532) ^ [_56676] : [-(_56676 = _56676)], (4 ^ _56532) ^ [_56783, _56785] : [_56785 = _56783, -(_56783 = _56785)], (10 ^ _56532) ^ [_56987, _56989, _56991] : [-(_56991 = _56987), _56991 = _56989, _56989 = _56987], (20 ^ _56532) ^ [_57300, _57302] : [-(open(_57300)), _57302 = _57300, open(_57302)], (30 ^ _56532) ^ [_57623, _57625, _57627, _57629] : [-(inner_point(_57627, _57623)), inner_point(_57629, _57625), _57629 = _57627, _57625 = _57623], (44 ^ _56532) ^ [_58039, _58041] : [-(closed(_58039)), _58041 = _58039, closed(_58041)], (54 ^ _56532) ^ [_58362, _58364, _58366, _58368] : [-(end_point(_58366, _58362)), end_point(_58368, _58364), _58368 = _58366, _58364 = _58362], (68 ^ _56532) ^ [_58834, _58836, _58838, _58840, _58842, _58844] : [-(meet(_58842, _58838, _58834)), meet(_58844, _58840, _58836), _58844 = _58842, _58840 = _58838, _58836 = _58834], (86 ^ _56532) ^ [_59415, _59417, _59419, _59421] : [-(incident_c(_59419, _59415)), incident_c(_59421, _59417), _59421 = _59419, _59417 = _59415], (100 ^ _56532) ^ [_59839, _59841, _59843, _59845] : [-(part_of(_59843, _59839)), part_of(_59845, _59841), _59845 = _59843, _59841 = _59839], (134 ^ _56532) ^ [_60957, _60959] : [136 ^ _56532 : [(137 ^ _56532) ^ [] : [-(incident_c(135 ^ [_60957, _60959], _60957))], (139 ^ _56532) ^ [] : [incident_c(135 ^ [_60957, _60959], _60959)]], -(part_of(_60957, _60959))], (124 ^ _56532) ^ [_60643, _60645] : [part_of(_60643, _60645), 127 ^ _56532 : [(128 ^ _56532) ^ [_60780] : [incident_c(_60780, _60643), -(incident_c(_60780, _60645))]]], (165 ^ _56532) ^ [_62082, _62084, _62086] : [-(_62086 = sum(_62084, _62082)), 169 ^ _56532 : [(170 ^ _56532) ^ [] : [-(incident_c(166 ^ [_62082, _62084, _62086], _62086))], (172 ^ _56532) ^ [] : [incident_c(166 ^ [_62082, _62084, _62086], _62084)], (174 ^ _56532) ^ [] : [incident_c(166 ^ [_62082, _62084, _62086], _62082)]], 175 ^ _56532 : [(182 ^ _56532) ^ [] : [incident_c(166 ^ [_62082, _62084, _62086], _62086)], (176 ^ _56532) ^ [] : [-(incident_c(166 ^ [_62082, _62084, _62086], _62084)), -(incident_c(166 ^ [_62082, _62084, _62086], _62082))]]], (143 ^ _56532) ^ [_61357, _61359, _61361] : [_61361 = sum(_61359, _61357), 146 ^ _56532 : [(157 ^ _56532) ^ [_61817] : [158 ^ _56532 : [(159 ^ _56532) ^ [] : [incident_c(_61817, _61359)], (161 ^ _56532) ^ [] : [incident_c(_61817, _61357)]], -(incident_c(_61817, _61361))], (147 ^ _56532) ^ [_61539] : [incident_c(_61539, _61361), -(incident_c(_61539, _61359)), -(incident_c(_61539, _61357))]]], (214 ^ _56532) ^ [_63690, _63692] : [-(end_point(_63692, _63690)), incident_c(_63692, _63690), 221 ^ _56532 : [(222 ^ _56532) ^ [] : [-(part_of(219 ^ [_63690, _63692], _63690))], (224 ^ _56532) ^ [] : [-(part_of(220 ^ [_63690, _63692], _63690))], (226 ^ _56532) ^ [] : [-(incident_c(_63692, 219 ^ [_63690, _63692]))], (228 ^ _56532) ^ [] : [-(incident_c(_63692, 220 ^ [_63690, _63692]))], (230 ^ _56532) ^ [] : [part_of(219 ^ [_63690, _63692], 220 ^ [_63690, _63692])], (232 ^ _56532) ^ [] : [part_of(220 ^ [_63690, _63692], 219 ^ [_63690, _63692])]]], (186 ^ _56532) ^ [_62862, _62864] : [end_point(_62864, _62862), 189 ^ _56532 : [(190 ^ _56532) ^ [] : [-(incident_c(_62864, _62862))], (192 ^ _56532) ^ [_63114, _63116] : [-(part_of(_63116, _63114)), -(part_of(_63114, _63116)), part_of(_63116, _62862), part_of(_63114, _62862), incident_c(_62864, _63116), incident_c(_62864, _63114)]]], (236 ^ _56532) ^ [_64645, _64647] : [inner_point(_64647, _64645), 239 ^ _56532 : [(240 ^ _56532) ^ [] : [-(incident_c(_64647, _64645))], (242 ^ _56532) ^ [] : [end_point(_64647, _64645)]]], (244 ^ _56532) ^ [_64883, _64885] : [-(inner_point(_64885, _64883)), incident_c(_64885, _64883), -(end_point(_64885, _64883))], (254 ^ _56532) ^ [_65230, _65232, _65234] : [meet(_65234, _65232, _65230), 257 ^ _56532 : [(258 ^ _56532) ^ [] : [-(incident_c(_65234, _65232))], (260 ^ _56532) ^ [] : [-(incident_c(_65234, _65230))], (262 ^ _56532) ^ [_65533] : [269 ^ _56532 : [(270 ^ _56532) ^ [] : [-(end_point(_65533, _65232))], (272 ^ _56532) ^ [] : [-(end_point(_65533, _65230))]], incident_c(_65533, _65232), incident_c(_65533, _65230)]]], (274 ^ _56532) ^ [_65898, _65900, _65902] : [-(meet(_65902, _65900, _65898)), incident_c(_65902, _65900), incident_c(_65902, _65898), 284 ^ _56532 : [(285 ^ _56532) ^ [] : [-(incident_c(283 ^ [_65898, _65900, _65902], _65900))], (287 ^ _56532) ^ [] : [-(incident_c(283 ^ [_65898, _65900, _65902], _65898))], (289 ^ _56532) ^ [] : [end_point(283 ^ [_65898, _65900, _65902], _65900), end_point(283 ^ [_65898, _65900, _65902], _65898)]]], (297 ^ _56532) ^ [_66675] : [closed(_66675), 300 ^ _56532 : [(301 ^ _56532) ^ [_66786] : [end_point(_66786, _66675)]]], (303 ^ _56532) ^ [_66852] : [-(end_point(304 ^ [_66852], _66852)), -(closed(_66852))], (310 ^ _56532) ^ [_67125] : [open(_67125), -(end_point(313 ^ [_67125], _67125))], (317 ^ _56532) ^ [_67330] : [318 ^ _56532 : [(319 ^ _56532) ^ [_67397] : [end_point(_67397, _67330)]], -(open(_67330))], (323 ^ _56532) ^ [_67556, _67558] : [-(open(_67556)), part_of(_67556, _67558), -(_67556 = _67558)], (333 ^ _56532) ^ [_67884, _67886, _67888, _67890] : [part_of(_67888, _67890), part_of(_67886, _67890), part_of(_67884, _67890), 346 ^ _56532 : [(347 ^ _56532) ^ [_68295] : [end_point(_68295, _67888), end_point(_68295, _67886), end_point(_68295, _67884)]], -(part_of(_67886, _67884)), -(part_of(_67884, _67886)), -(part_of(_67888, _67886)), -(part_of(_67886, _67888)), -(part_of(_67888, _67884)), -(part_of(_67884, _67888))], (380 ^ _56532) ^ [_69174] : [-(inner_point(378 ^ [_69174], _69174))], (382 ^ _56532) ^ [_69286, _69288] : [inner_point(_69286, _69288), 387 ^ _56532 : [(388 ^ _56532) ^ [] : [-(meet(_69286, 385 ^ [_69286, _69288], 386 ^ [_69286, _69288]))], (390 ^ _56532) ^ [] : [-(_69288 = sum(385 ^ [_69286, _69288], 386 ^ [_69286, _69288]))]]], (392 ^ _56532) ^ [_69774, _69776, _69778, _69780] : [end_point(_69778, _69780), end_point(_69776, _69780), end_point(_69774, _69780), -(_69778 = _69776), -(_69778 = _69774), -(_69776 = _69774)], (414 ^ _56532) ^ [_70390, _70392] : [end_point(_70390, _70392), 418 ^ _56532 : [(419 ^ _56532) ^ [] : [-(end_point(417 ^ [_70390, _70392], _70392))], (421 ^ _56532) ^ [] : [_70390 = 417 ^ [_70390, _70392]]]], (423 ^ _56532) ^ [_70776, _70778, _70780, _70782] : [434 ^ _56532 : [(435 ^ _56532) ^ [_71122] : [end_point(_71122, _70780), -(meet(_71122, _70780, _70778))]], closed(_70782), meet(_70776, _70780, _70778), _70782 = sum(_70780, _70778)], (441 ^ _56532) ^ [_71365, _71367] : [442 ^ _56532 : [(443 ^ _56532) ^ [_71444] : [meet(_71444, _71367, _71365)]], -(444 ^ [_71365, _71367] = sum(_71367, _71365))], (448 ^ _56532) ^ [_71645, _71647] : [-(_71647 = _71645), 452 ^ _56532 : [(453 ^ _56532) ^ [] : [-(incident_c(449 ^ [_71645, _71647], _71647))], (455 ^ _56532) ^ [] : [incident_c(449 ^ [_71645, _71647], _71645)]], 456 ^ _56532 : [(457 ^ _56532) ^ [] : [-(incident_c(449 ^ [_71645, _71647], _71645))], (459 ^ _56532) ^ [] : [incident_c(449 ^ [_71645, _71647], _71647)]]]], input).
% 0.32/1.38 ncf('1',plain,[part_of(462 ^ [], 462 ^ [])],start(464 ^ 0)).
% 0.32/1.38 ncf('1.1',plain,[-(part_of(462 ^ [], 462 ^ [])), 137 : -(incident_c(135 ^ [462 ^ [], 462 ^ []], 462 ^ []))],extension(134 ^ 1,bind([[_60957, _60959], [462 ^ [], 462 ^ []]]))).
% 0.32/1.38 ncf('1.1.1',plain,[incident_c(135 ^ [462 ^ [], 462 ^ []], 462 ^ [])],extension(139 ^ 4)).
% 0.32/1.38 %-----------------------------------------------------
% 0.32/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------