%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : MED010+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n010.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:34:30 EDT 2023
% Result : Theorem 3.59s 4.47s
% Output : Proof 3.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : MED010+1 : TPTP v8.1.2. Released v3.2.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n010.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 : Thu May 18 16:22:12 EDT 2023
% 0.12/0.33 % CPUTime :
% 3.59/4.47
% 3.59/4.47 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 3.59/4.47 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.59/4.47 %-----------------------------------------------------
% 3.59/4.47 ncf(matrix, plain, [(610 ^ _89280) ^ [] : [-(s2(n0))], (618 ^ _89280) ^ [] : [-(bcapacityex(n0))], (612 ^ _89280) ^ [_109115] : [gt(n0, _109115), -(conditionhyper(_109115))], (620 ^ _89280) ^ [_109320] : [-(gt(n0, _109320)), s3(_109320), 630 ^ _89280 : [(631 ^ _89280) ^ [] : [-(gt(_109320, 629 ^ [_109320]))], (633 ^ _89280) ^ [] : [conditionhyper(629 ^ [_109320])]], bcapacityex(_109320)], (2 ^ _89280) ^ [_89383] : [gt(_89383, _89383)], (4 ^ _89280) ^ [_89504, _89506, _89508] : [-(gt(_89508, _89504)), gt(_89508, _89506), gt(_89506, _89504)], (14 ^ _89280) ^ [_89799] : [-(bcapacityne(_89799)), -(bcapacityex(_89799)), -(bcapacitysn(_89799))], (24 ^ _89280) ^ [_90070] : [bcapacityne(_90070), bcapacityex(_90070)], (30 ^ _89280) ^ [_90259] : [bcapacityne(_90259), bcapacitysn(_90259)], (36 ^ _89280) ^ [_90448] : [bcapacityex(_90448), bcapacitysn(_90448)], (42 ^ _89280) ^ [_90637] : [-(conditionhyper(_90637)), -(conditionhypo(_90637)), -(conditionnormo(_90637))], (52 ^ _89280) ^ [_90908] : [conditionhyper(_90908), conditionhypo(_90908)], (58 ^ _89280) ^ [_91097] : [conditionhyper(_91097), conditionnormo(_91097)], (64 ^ _89280) ^ [_91286] : [conditionhypo(_91286), conditionnormo(_91286)], (70 ^ _89280) ^ [_91475] : [72 ^ _89280 : [(73 ^ _89280) ^ [] : [gt(_91475, 71 ^ [_91475])], (75 ^ _89280) ^ [] : [drugi(71 ^ [_91475])]], 76 ^ _89280 : [(77 ^ _89280) ^ [_91748] : [-(gt(_91475, _91748)), 80 ^ _89280 : [(81 ^ _89280) ^ [] : [-(uptakelg(_91748))], (83 ^ _89280) ^ [] : [-(uptakepg(_91748))]]]]], (85 ^ _89280) ^ [_92040, _92042] : [-(gt(_92042, _92040)), uptakelg(_92040), releaselg(_92040)], (95 ^ _89280) ^ [_92325] : [99 ^ _89280 : [(100 ^ _89280) ^ [] : [gt(_92325, 98 ^ [_92325])], (102 ^ _89280) ^ [] : [drugsu(98 ^ [_92325])]], -(bcapacityex(_92325)), 105 ^ _89280 : [(106 ^ _89280) ^ [_92680] : [-(gt(_92325, _92680)), -(bsecretioni(_92680))]]], (112 ^ _89280) ^ [_92886] : [114 ^ _89280 : [(115 ^ _89280) ^ [] : [gt(_92886, 113 ^ [_92886])], (117 ^ _89280) ^ [] : [drugbg(113 ^ [_92886])]], 118 ^ _89280 : [(119 ^ _89280) ^ [_93156] : [-(gt(_92886, _93156)), releaselg(_93156)]]], (125 ^ _89280) ^ [_93362] : [146 ^ _89280 : [(147 ^ _89280) ^ [_94014] : [-(gt(_93362, _94014)), -(conditionnormo(_94014))]], 129 ^ _89280 : [(130 ^ _89280) ^ [] : [gt(_93362, 128 ^ [_93362])], (132 ^ _89280) ^ [] : [bsecretioni(128 ^ [_93362])]], bcapacitysn(_93362), qilt27(_93362), 142 ^ _89280 : [(143 ^ _89280) ^ [] : [-(gt(_93362, 141 ^ [_93362]))], (145 ^ _89280) ^ [] : [conditionhyper(141 ^ [_93362])]]], (153 ^ _89280) ^ [_94218] : [174 ^ _89280 : [(175 ^ _89280) ^ [_94878] : [-(gt(_94218, _94878)), -(conditionnormo(_94878))]], 157 ^ _89280 : [(158 ^ _89280) ^ [] : [gt(_94218, 156 ^ [_94218])], (160 ^ _89280) ^ [] : [-(releaselg(156 ^ [_94218]))]], bcapacitysn(_94218), -(qilt27(_94218)), 170 ^ _89280 : [(171 ^ _89280) ^ [] : [-(gt(_94218, 169 ^ [_94218]))], (173 ^ _89280) ^ [] : [conditionhyper(169 ^ [_94218])]]], (181 ^ _89280) ^ [_95082] : [210 ^ _89280 : [(211 ^ _89280) ^ [_96083] : [-(gt(_95082, _96083)), -(conditionnormo(_96083))]], 185 ^ _89280 : [(186 ^ _89280) ^ [] : [gt(_95082, 184 ^ [_95082])], (188 ^ _89280) ^ [] : [-(releaselg(184 ^ [_95082]))], (191 ^ _89280) ^ [] : [gt(_95082, 189 ^ [_95082])], (193 ^ _89280) ^ [] : [uptakepg(189 ^ [_95082])]], bcapacityne(_95082), 201 ^ _89280 : [(202 ^ _89280) ^ [] : [gt(_95082, 200 ^ [_95082])], (204 ^ _89280) ^ [] : [bsecretioni(200 ^ [_95082])]], 206 ^ _89280 : [(207 ^ _89280) ^ [] : [-(gt(_95082, 205 ^ [_95082]))], (209 ^ _89280) ^ [] : [conditionhyper(205 ^ [_95082])]]], (217 ^ _89280) ^ [_96267] : [241 ^ _89280 : [(242 ^ _89280) ^ [_97061] : [-(gt(_96267, _97061)), -(conditionnormo(_97061)), -(conditionhypo(_97061))]], 221 ^ _89280 : [(222 ^ _89280) ^ [] : [gt(_96267, 220 ^ [_96267])], (224 ^ _89280) ^ [] : [uptakelg(220 ^ [_96267])]], 228 ^ _89280 : [(229 ^ _89280) ^ [] : [gt(_96267, 227 ^ [_96267])], (231 ^ _89280) ^ [] : [uptakepg(227 ^ [_96267])]], bcapacityex(_96267), 237 ^ _89280 : [(238 ^ _89280) ^ [] : [-(gt(_96267, 236 ^ [_96267]))], (240 ^ _89280) ^ [] : [conditionhyper(236 ^ [_96267])]]], (252 ^ _89280) ^ [_97387] : [-(s0(_97387)), -(s1(_97387)), -(s2(_97387)), -(s3(_97387))], (266 ^ _89280) ^ [_97742] : [s0(_97742), s1(_97742)], (272 ^ _89280) ^ [_97931] : [s0(_97931), s2(_97931)], (278 ^ _89280) ^ [_98120] : [s0(_98120), s3(_98120)], (284 ^ _89280) ^ [_98309] : [s1(_98309), s2(_98309)], (290 ^ _89280) ^ [_98498] : [s1(_98498), s3(_98498)], (296 ^ _89280) ^ [_98687] : [s2(_98687), s3(_98687)], (302 ^ _89280) ^ [_98876] : [304 ^ _89280 : [(305 ^ _89280) ^ [] : [gt(_98876, 303 ^ [_98876])], (307 ^ _89280) ^ [] : [conditionnormo(303 ^ [_98876])]], 310 ^ _89280 : [(311 ^ _89280) ^ [_99404] : [-(gt(_98876, _99404)), -(bsecretioni(_99404))], (317 ^ _89280) ^ [] : [-(bcapacitysn(_98876))], (319 ^ _89280) ^ [] : [-(qilt27(_98876))], (321 ^ _89280) ^ [_99709] : [gt(_98876, _99709), -(conditionhyper(_99709))]], 328 ^ _89280 : [(329 ^ _89280) ^ [_99943] : [-(gt(_98876, _99943)), releaselg(_99943)], (335 ^ _89280) ^ [] : [-(bcapacitysn(_98876))], (337 ^ _89280) ^ [] : [qilt27(_98876)], (339 ^ _89280) ^ [_100248] : [gt(_98876, _100248), -(conditionhyper(_100248))]], 374 ^ _89280 : [(375 ^ _89280) ^ [_101343] : [-(gt(_98876, _101343)), -(uptakelg(_101343))], (381 ^ _89280) ^ [_101542] : [-(gt(_98876, _101542)), -(uptakepg(_101542))], (387 ^ _89280) ^ [] : [-(bcapacityex(_98876))], (389 ^ _89280) ^ [_101784] : [gt(_98876, _101784), -(conditionhyper(_101784))]], 346 ^ _89280 : [(347 ^ _89280) ^ [] : [348 ^ _89280 : [(349 ^ _89280) ^ [_100514] : [-(gt(_98876, _100514)), releaselg(_100514)]], 354 ^ _89280 : [(355 ^ _89280) ^ [_100694] : [-(gt(_98876, _100694)), -(uptakepg(_100694))]]], (361 ^ _89280) ^ [] : [-(bcapacityne(_98876))], (363 ^ _89280) ^ [_100962] : [-(gt(_98876, _100962)), -(bsecretioni(_100962))], (369 ^ _89280) ^ [_101141] : [gt(_98876, _101141), -(conditionhyper(_101141))]]], (395 ^ _89280) ^ [_102007] : [-(drugsu(_102007)), s1(_102007), qilt27(_102007)], (405 ^ _89280) ^ [_102276] : [-(drugbg(_102276)), s1(_102276), -(qilt27(_102276))], (415 ^ _89280) ^ [_102548] : [s2(_102548), 418 ^ _89280 : [(419 ^ _89280) ^ [] : [-(drugbg(_102548))], (421 ^ _89280) ^ [] : [-(drugsu(_102548))]]], (423 ^ _89280) ^ [_102805] : [s3(_102805), -(drugi(_102805)), 428 ^ _89280 : [(429 ^ _89280) ^ [] : [-(drugi(_102805))], (431 ^ _89280) ^ [] : [-(drugsu(_102805)), -(drugbg(_102805))]]], (439 ^ _89280) ^ [_103230] : [drugbg(_103230), 444 ^ _89280 : [(445 ^ _89280) ^ [] : [-(s1(_103230))], (447 ^ _89280) ^ [] : [qilt27(_103230)]], -(s2(_103230)), -(s3(_103230))], (455 ^ _89280) ^ [_103656] : [drugsu(_103656), 460 ^ _89280 : [(461 ^ _89280) ^ [] : [-(s1(_103656))], (463 ^ _89280) ^ [] : [-(qillt27(_103656))]], -(s2(_103656)), -(s3(_103656))], (471 ^ _89280) ^ [_104081] : [drugi(_104081), -(s3(_104081))], (477 ^ _89280) ^ [_104267] : [479 ^ _89280 : [(480 ^ _89280) ^ [] : [gt(_104267, 478 ^ [_104267])], (482 ^ _89280) ^ [] : [uptakelg(478 ^ [_104267])], (485 ^ _89280) ^ [] : [gt(_104267, 483 ^ [_104267])], (487 ^ _89280) ^ [] : [uptakepg(483 ^ [_104267])]], 488 ^ _89280 : [(489 ^ _89280) ^ [_104742] : [-(gt(_104267, _104742)), -(drugi(_104742))]]], (495 ^ _89280) ^ [_104961, _104963] : [-(gt(_104963, _104961)), -(releaselg(_104961)), -(uptakelg(_104961))], (505 ^ _89280) ^ [_105248] : [507 ^ _89280 : [(508 ^ _89280) ^ [] : [gt(_105248, 506 ^ [_105248])], (510 ^ _89280) ^ [] : [bsecretioni(506 ^ [_105248])]], 511 ^ _89280 : [(518 ^ _89280) ^ [] : [bcapacityex(_105248)], (512 ^ _89280) ^ [_105543] : [-(gt(_105248, _105543)), -(drugsu(_105543))]]], (520 ^ _89280) ^ [_105792] : [522 ^ _89280 : [(523 ^ _89280) ^ [] : [gt(_105792, 521 ^ [_105792])], (525 ^ _89280) ^ [] : [-(releaselg(521 ^ [_105792]))]], 526 ^ _89280 : [(527 ^ _89280) ^ [_106065] : [-(gt(_105792, _106065)), -(drugbg(_106065))]]], (533 ^ _89280) ^ [_106270] : [545 ^ _89280 : [(546 ^ _89280) ^ [] : [gt(_106270, 544 ^ [_106270])], (548 ^ _89280) ^ [] : [-(s1(544 ^ [_106270]))], (550 ^ _89280) ^ [_106854] : [gt(544 ^ [_106270], _106854), -(conditionhyper(_106854))]], s0(_106270), 538 ^ _89280 : [(539 ^ _89280) ^ [_106470] : [-(gt(_106270, _106470)), -(conditionnormo(_106470))]]], (585 ^ _89280) ^ [_108024] : [597 ^ _89280 : [(598 ^ _89280) ^ [] : [gt(_108024, 596 ^ [_108024])], (600 ^ _89280) ^ [] : [-(s3(596 ^ [_108024]))], (608 ^ _89280) ^ [] : [-(bcapacityex(596 ^ [_108024]))], (602 ^ _89280) ^ [_108638] : [gt(596 ^ [_108024], _108638), -(conditionhyper(_108638))]], s2(_108024), 590 ^ _89280 : [(591 ^ _89280) ^ [_108229] : [-(gt(_108024, _108229)), -(conditionnormo(_108229))]]], (556 ^ _89280) ^ [_107069] : [s1(_107069), 561 ^ _89280 : [(562 ^ _89280) ^ [_107279] : [-(gt(_107069, _107279)), -(conditionnormo(_107279))]], 568 ^ _89280 : [(569 ^ _89280) ^ [] : [gt(_107069, 567 ^ [_107069])], (571 ^ _89280) ^ [] : [-(s2(567 ^ [_107069]))], (573 ^ _89280) ^ [_107693] : [gt(567 ^ [_107069], _107693), -(conditionhyper(_107693))], (579 ^ _89280) ^ [] : [-(bcapacityne(567 ^ [_107069])), -(bcapacityex(567 ^ [_107069]))]]]], input).
% 3.59/4.47 ncf('1',plain,[conditionhyper(n0), conditionnormo(n0)],start(58 ^ 0,bind([[_91097], [n0]]))).
% 3.59/4.47 ncf('1.1',plain,[-(conditionhyper(n0)), 339 : gt(n0, n0), 305 : gt(n0, 303 ^ [n0]), 317 : -(bcapacitysn(n0)), 389 : gt(n0, n0), 389 : -(conditionhyper(n0)), 361 : -(bcapacityne(n0))],extension(302 ^ 1,bind([[_98876, _100248, _101784], [n0, n0, n0]]))).
% 3.59/4.47 ncf('1.1.1',plain,[-(gt(n0, n0)), 489 : -(drugi(n0)), 480 : gt(n0, 478 ^ [n0])],extension(477 ^ 4,bind([[_104267, _104742], [n0, n0]]))).
% 3.59/4.47 ncf('1.1.1.1',plain,[drugi(n0), -(s3(n0))],extension(471 ^ 7,bind([[_104081], [n0]]))).
% 3.59/4.47 ncf('1.1.1.1.1',plain,[s3(n0), s2(n0)],extension(296 ^ 8,bind([[_98687], [n0]]))).
% 3.59/4.47 ncf('1.1.1.1.1.1',plain,[-(s2(n0))],extension(610 ^ 9)).
% 3.59/4.47 ncf('1.1.1.2',plain,[-(gt(n0, 478 ^ [n0])), -(releaselg(478 ^ [n0])), -(uptakelg(478 ^ [n0]))],extension(495 ^ 7,bind([[_104961, _104963], [478 ^ [n0], n0]]))).
% 3.59/4.47 ncf('1.1.1.2.1',plain,[releaselg(478 ^ [n0]), -(gt(n0, 478 ^ [n0]))],extension(329 ^ 8,bind([[_99943], [478 ^ [n0]]]))).
% 3.59/4.47 ncf('1.1.1.2.1.1',plain,[gt(n0, 478 ^ [n0])],reduction('1.1.1')).
% 3.59/4.47 ncf('1.1.1.2.2',plain,[uptakelg(478 ^ [n0])],extension(482 ^ 8)).
% 3.59/4.47 ncf('1.1.2',plain,[-(gt(n0, 303 ^ [n0])), 591 : -(conditionnormo(303 ^ [n0])), 602 : gt(596 ^ [n0], 629 ^ [596 ^ [n0]]), 602 : -(conditionhyper(629 ^ [596 ^ [n0]])), 602 : s2(n0)],extension(585 ^ 4,bind([[_108024, _108229, _108638], [n0, 303 ^ [n0], 629 ^ [596 ^ [n0]]]]))).
% 3.59/4.47 ncf('1.1.2.1',plain,[conditionnormo(303 ^ [n0])],extension(307 ^ 7)).
% 3.59/4.47 ncf('1.1.2.2',plain,[-(gt(596 ^ [n0], 629 ^ [596 ^ [n0]])), -(gt(n0, 596 ^ [n0])), s3(596 ^ [n0]), bcapacityex(596 ^ [n0])],extension(620 ^ 7,bind([[_109320], [596 ^ [n0]]]))).
% 3.59/4.47 ncf('1.1.2.2.1',plain,[gt(n0, 596 ^ [n0])],extension(598 ^ 8)).
% 3.59/4.47 ncf('1.1.2.2.2',plain,[-(s3(596 ^ [n0]))],extension(600 ^ 8)).
% 3.59/4.47 ncf('1.1.2.2.3',plain,[-(bcapacityex(596 ^ [n0]))],extension(608 ^ 8)).
% 3.59/4.47 ncf('1.1.2.3',plain,[conditionhyper(629 ^ [596 ^ [n0]]), -(gt(n0, 596 ^ [n0])), s3(596 ^ [n0]), bcapacityex(596 ^ [n0])],extension(620 ^ 7,bind([[_109320], [596 ^ [n0]]]))).
% 3.59/4.47 ncf('1.1.2.3.1',plain,[gt(n0, 596 ^ [n0])],extension(598 ^ 8)).
% 3.59/4.47 ncf('1.1.2.3.2',plain,[-(s3(596 ^ [n0]))],extension(600 ^ 8)).
% 3.59/4.47 ncf('1.1.2.3.3',plain,[-(bcapacityex(596 ^ [n0]))],extension(608 ^ 8)).
% 3.59/4.47 ncf('1.1.2.4',plain,[-(s2(n0))],extension(610 ^ 5)).
% 3.59/4.47 ncf('1.1.3',plain,[bcapacitysn(n0), bcapacityex(n0)],extension(36 ^ 4,bind([[_90448], [n0]]))).
% 3.59/4.47 ncf('1.1.3.1',plain,[-(bcapacityex(n0))],extension(618 ^ 5)).
% 3.59/4.47 ncf('1.1.4',plain,[-(gt(n0, n0)), 489 : -(drugi(n0)), 480 : gt(n0, 478 ^ [n0])],extension(477 ^ 4,bind([[_104267, _104742], [n0, n0]]))).
% 3.59/4.47 ncf('1.1.4.1',plain,[drugi(n0), -(s3(n0))],extension(471 ^ 7,bind([[_104081], [n0]]))).
% 3.59/4.47 ncf('1.1.4.1.1',plain,[s3(n0), s2(n0)],extension(296 ^ 8,bind([[_98687], [n0]]))).
% 3.59/4.47 ncf('1.1.4.1.1.1',plain,[-(s2(n0))],extension(610 ^ 9)).
% 3.59/4.47 ncf('1.1.4.2',plain,[-(gt(n0, 478 ^ [n0])), -(uptakelg(478 ^ [n0]))],extension(375 ^ 7,bind([[_101343], [478 ^ [n0]]]))).
% 3.59/4.47 ncf('1.1.4.2.1',plain,[uptakelg(478 ^ [n0])],extension(482 ^ 8)).
% 3.59/4.47 ncf('1.1.5',plain,[conditionhyper(n0)],reduction('1')).
% 3.59/4.47 ncf('1.1.6',plain,[bcapacityne(n0), bcapacityex(n0)],extension(24 ^ 4,bind([[_90070], [n0]]))).
% 3.59/4.47 ncf('1.1.6.1',plain,[-(bcapacityex(n0))],extension(618 ^ 5)).
% 3.59/4.47 ncf('1.2',plain,[-(conditionnormo(n0)), 591 : -(gt(n0, n0)), 598 : gt(n0, 596 ^ [n0]), 598 : s2(n0)],extension(585 ^ 1,bind([[_108024, _108229], [n0, n0]]))).
% 3.59/4.47 ncf('1.2.1',plain,[gt(n0, n0)],extension(2 ^ 4,bind([[_89383], [n0]]))).
% 3.59/4.47 ncf('1.2.2',plain,[-(gt(n0, 596 ^ [n0])), s3(596 ^ [n0]), 631 : -(gt(596 ^ [n0], 629 ^ [596 ^ [n0]])), 631 : bcapacityex(596 ^ [n0])],extension(620 ^ 4,bind([[_109320], [596 ^ [n0]]]))).
% 3.59/4.47 ncf('1.2.2.1',plain,[-(s3(596 ^ [n0]))],extension(600 ^ 5)).
% 3.59/4.47 ncf('1.2.2.2',plain,[gt(596 ^ [n0], 629 ^ [596 ^ [n0]]), -(conditionhyper(629 ^ [596 ^ [n0]]))],extension(602 ^ 7,bind([[_108638], [629 ^ [596 ^ [n0]]]]))).
% 3.59/4.47 ncf('1.2.2.2.1',plain,[conditionhyper(629 ^ [596 ^ [n0]])],extension(633 ^ 8)).
% 3.59/4.47 ncf('1.2.2.3',plain,[-(bcapacityex(596 ^ [n0]))],extension(608 ^ 5)).
% 3.59/4.47 ncf('1.2.3',plain,[-(s2(n0))],extension(610 ^ 2)).
% 3.59/4.47 %-----------------------------------------------------
% 3.59/4.47 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------