%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : MED001+1 : TPTP v8.1.2. Released v3.2.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:34:29 EDT 2023
% Result : Theorem 0.34s 1.37s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : MED001+1 : TPTP v8.1.2. Released v3.2.0.
% 0.11/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 : Thu May 18 16:45:33 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.34/1.37
% 0.34/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.34/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 ncf(matrix, plain, [(269 ^ _36599) ^ [] : [gt(n0, 267 ^ [])], (271 ^ _36599) ^ [] : [conditionnormo(267 ^ [])], (252 ^ _36599) ^ [_44706] : [-(gt(n0, _44706)), -(drugsu(_44706))], (264 ^ _36599) ^ [] : [-(bcapacitysn(n0))], (266 ^ _36599) ^ [] : [-(qilt27(n0))], (258 ^ _36599) ^ [_44897] : [gt(n0, _44897), -(conditionhyper(_44897))], (2 ^ _36599) ^ [_36682] : [gt(_36682, _36682)], (4 ^ _36599) ^ [_36803, _36805, _36807] : [-(gt(_36807, _36803)), gt(_36807, _36805), gt(_36805, _36803)], (14 ^ _36599) ^ [_37098] : [-(bcapacityne(_37098)), -(bcapacityex(_37098)), -(bcapacitysn(_37098))], (24 ^ _36599) ^ [_37369] : [bcapacityne(_37369), bcapacityex(_37369)], (30 ^ _36599) ^ [_37558] : [bcapacityne(_37558), bcapacitysn(_37558)], (36 ^ _36599) ^ [_37747] : [bcapacityex(_37747), bcapacitysn(_37747)], (42 ^ _36599) ^ [_37936] : [-(conditionhyper(_37936)), -(conditionhypo(_37936)), -(conditionnormo(_37936))], (52 ^ _36599) ^ [_38207] : [conditionhyper(_38207), conditionhypo(_38207)], (58 ^ _36599) ^ [_38396] : [conditionhyper(_38396), conditionnormo(_38396)], (64 ^ _36599) ^ [_38585] : [conditionhypo(_38585), conditionnormo(_38585)], (70 ^ _36599) ^ [_38774] : [72 ^ _36599 : [(73 ^ _36599) ^ [] : [gt(_38774, 71 ^ [_38774])], (75 ^ _36599) ^ [] : [drugi(71 ^ [_38774])]], 76 ^ _36599 : [(77 ^ _36599) ^ [_39047] : [-(gt(_38774, _39047)), 80 ^ _36599 : [(81 ^ _36599) ^ [] : [-(uptakelg(_39047))], (83 ^ _36599) ^ [] : [-(uptakepg(_39047))]]]]], (85 ^ _36599) ^ [_39339, _39341] : [-(gt(_39341, _39339)), uptakelg(_39339), releaselg(_39339)], (95 ^ _36599) ^ [_39624] : [99 ^ _36599 : [(100 ^ _36599) ^ [] : [gt(_39624, 98 ^ [_39624])], (102 ^ _36599) ^ [] : [drugsu(98 ^ [_39624])]], -(bcapacityex(_39624)), 105 ^ _36599 : [(106 ^ _36599) ^ [_39979] : [-(gt(_39624, _39979)), -(bsecretioni(_39979))]]], (112 ^ _36599) ^ [_40185] : [114 ^ _36599 : [(115 ^ _36599) ^ [] : [gt(_40185, 113 ^ [_40185])], (117 ^ _36599) ^ [] : [drugbg(113 ^ [_40185])]], 118 ^ _36599 : [(119 ^ _36599) ^ [_40455] : [-(gt(_40185, _40455)), releaselg(_40455)]]], (125 ^ _36599) ^ [_40661] : [146 ^ _36599 : [(147 ^ _36599) ^ [_41313] : [-(gt(_40661, _41313)), -(conditionnormo(_41313))]], 129 ^ _36599 : [(130 ^ _36599) ^ [] : [gt(_40661, 128 ^ [_40661])], (132 ^ _36599) ^ [] : [bsecretioni(128 ^ [_40661])]], bcapacitysn(_40661), qilt27(_40661), 142 ^ _36599 : [(143 ^ _36599) ^ [] : [-(gt(_40661, 141 ^ [_40661]))], (145 ^ _36599) ^ [] : [conditionhyper(141 ^ [_40661])]]], (153 ^ _36599) ^ [_41517] : [174 ^ _36599 : [(175 ^ _36599) ^ [_42177] : [-(gt(_41517, _42177)), -(conditionnormo(_42177))]], 157 ^ _36599 : [(158 ^ _36599) ^ [] : [gt(_41517, 156 ^ [_41517])], (160 ^ _36599) ^ [] : [-(releaselg(156 ^ [_41517]))]], bcapacitysn(_41517), -(qilt27(_41517)), 170 ^ _36599 : [(171 ^ _36599) ^ [] : [-(gt(_41517, 169 ^ [_41517]))], (173 ^ _36599) ^ [] : [conditionhyper(169 ^ [_41517])]]], (181 ^ _36599) ^ [_42381] : [210 ^ _36599 : [(211 ^ _36599) ^ [_43382] : [-(gt(_42381, _43382)), -(conditionnormo(_43382))]], 185 ^ _36599 : [(186 ^ _36599) ^ [] : [gt(_42381, 184 ^ [_42381])], (188 ^ _36599) ^ [] : [-(releaselg(184 ^ [_42381]))], (191 ^ _36599) ^ [] : [gt(_42381, 189 ^ [_42381])], (193 ^ _36599) ^ [] : [uptakepg(189 ^ [_42381])]], bcapacityne(_42381), 201 ^ _36599 : [(202 ^ _36599) ^ [] : [gt(_42381, 200 ^ [_42381])], (204 ^ _36599) ^ [] : [bsecretioni(200 ^ [_42381])]], 206 ^ _36599 : [(207 ^ _36599) ^ [] : [-(gt(_42381, 205 ^ [_42381]))], (209 ^ _36599) ^ [] : [conditionhyper(205 ^ [_42381])]]], (217 ^ _36599) ^ [_43566] : [241 ^ _36599 : [(242 ^ _36599) ^ [_44360] : [-(gt(_43566, _44360)), -(conditionnormo(_44360)), -(conditionhypo(_44360))]], 221 ^ _36599 : [(222 ^ _36599) ^ [] : [gt(_43566, 220 ^ [_43566])], (224 ^ _36599) ^ [] : [uptakelg(220 ^ [_43566])]], 228 ^ _36599 : [(229 ^ _36599) ^ [] : [gt(_43566, 227 ^ [_43566])], (231 ^ _36599) ^ [] : [uptakepg(227 ^ [_43566])]], bcapacityex(_43566), 237 ^ _36599 : [(238 ^ _36599) ^ [] : [-(gt(_43566, 236 ^ [_43566]))], (240 ^ _36599) ^ [] : [conditionhyper(236 ^ [_43566])]]]], input).
% 0.34/1.37 ncf('1',plain,[gt(n0, 267 ^ [])],start(269 ^ 0)).
% 0.34/1.37 ncf('1.1',plain,[-(gt(n0, 267 ^ [])), 147 : -(conditionnormo(267 ^ [])), 130 : gt(n0, 128 ^ [n0]), 130 : bcapacitysn(n0), 130 : qilt27(n0), 143 : -(gt(n0, 141 ^ [n0]))],extension(125 ^ 1,bind([[_40661, _41313], [n0, 267 ^ []]]))).
% 0.34/1.37 ncf('1.1.1',plain,[conditionnormo(267 ^ [])],extension(271 ^ 4)).
% 0.34/1.37 ncf('1.1.2',plain,[-(gt(n0, 128 ^ [n0])), 106 : -(bsecretioni(128 ^ [n0])), 100 : gt(n0, 98 ^ [n0]), 100 : -(bcapacityex(n0))],extension(95 ^ 4,bind([[_39624, _39979], [n0, 128 ^ [n0]]]))).
% 0.34/1.37 ncf('1.1.2.1',plain,[bsecretioni(128 ^ [n0])],extension(132 ^ 7)).
% 0.34/1.37 ncf('1.1.2.2',plain,[-(gt(n0, 98 ^ [n0])), -(drugsu(98 ^ [n0]))],extension(252 ^ 7,bind([[_44706], [98 ^ [n0]]]))).
% 0.34/1.37 ncf('1.1.2.2.1',plain,[drugsu(98 ^ [n0])],extension(102 ^ 8)).
% 0.34/1.37 ncf('1.1.2.3',plain,[bcapacityex(n0), bcapacitysn(n0)],extension(36 ^ 5,bind([[_37747], [n0]]))).
% 0.34/1.37 ncf('1.1.2.3.1',plain,[-(bcapacitysn(n0))],extension(264 ^ 6)).
% 0.34/1.37 ncf('1.1.3',plain,[-(bcapacitysn(n0))],extension(264 ^ 2)).
% 0.34/1.37 ncf('1.1.4',plain,[-(qilt27(n0))],extension(266 ^ 2)).
% 0.34/1.37 ncf('1.1.5',plain,[gt(n0, 141 ^ [n0]), -(conditionhyper(141 ^ [n0]))],extension(258 ^ 4,bind([[_44897], [141 ^ [n0]]]))).
% 0.34/1.37 ncf('1.1.5.1',plain,[conditionhyper(141 ^ [n0])],extension(145 ^ 5)).
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------