%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NLP009+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n020.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:36:46 EDT 2023
% Result : Theorem 0.33s 1.38s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NLP009+1 : TPTP v8.1.2. Released v2.4.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n020.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 14:53:47 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.33/1.38
% 0.33/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 ncf(matrix, plain, [(232 ^ _216118) ^ [] : [242 ^ _216118 : [(243 ^ _216118) ^ [] : [-(hollywood(233 ^ []))], (245 ^ _216118) ^ [] : [-(city(233 ^ []))], (247 ^ _216118) ^ [] : [-(event(234 ^ []))], (249 ^ _216118) ^ [] : [-(street(235 ^ []))], (251 ^ _216118) ^ [] : [-(way(235 ^ []))], (253 ^ _216118) ^ [] : [-(lonely(235 ^ []))], (255 ^ _216118) ^ [] : [-(chevy(236 ^ []))], (257 ^ _216118) ^ [] : [-(car(236 ^ []))], (259 ^ _216118) ^ [] : [-(white(236 ^ []))], (261 ^ _216118) ^ [] : [-(dirty(236 ^ []))], (263 ^ _216118) ^ [] : [-(old(236 ^ []))], (265 ^ _216118) ^ [] : [-(barrel(234 ^ [], 236 ^ []))], (267 ^ _216118) ^ [] : [-(down(234 ^ [], 235 ^ []))], (269 ^ _216118) ^ [] : [-(in(234 ^ [], 233 ^ []))], (271 ^ _216118) ^ [] : [-(seat(239 ^ []))], (273 ^ _216118) ^ [] : [-(furniture(239 ^ []))], (275 ^ _216118) ^ [] : [-(front(239 ^ []))], (277 ^ _216118) ^ [] : [237 ^ [] = 238 ^ []], (279 ^ _216118) ^ [] : [-(fellow(237 ^ []))], (281 ^ _216118) ^ [] : [-(man(237 ^ []))], (283 ^ _216118) ^ [] : [-(young(237 ^ []))], (285 ^ _216118) ^ [] : [-(fellow(238 ^ []))], (287 ^ _216118) ^ [] : [-(man(238 ^ []))], (289 ^ _216118) ^ [] : [-(young(238 ^ []))], (291 ^ _216118) ^ [] : [-(237 ^ [] = 240 ^ [])], (293 ^ _216118) ^ [] : [-(in(240 ^ [], 239 ^ []))], (295 ^ _216118) ^ [] : [-(238 ^ [] = 241 ^ [])], (297 ^ _216118) ^ [] : [-(in(241 ^ [], 239 ^ []))], (299 ^ _216118) ^ [_226450, _226452, _226454, _226456, _226458, _226460, _226462, _226464, _226466] : [hollywood(_226466), city(_226466), event(_226464), chevy(_226462), car(_226462), white(_226462), dirty(_226462), old(_226462), street(_226460), way(_226460), lonely(_226460), barrel(_226464, _226462), down(_226464, _226460), in(_226464, _226466), seat(_226454), furniture(_226454), front(_226454), -(_226458 = _226456), fellow(_226458), man(_226458), young(_226458), fellow(_226456), man(_226456), young(_226456), _226458 = _226452, in(_226452, _226454), _226456 = _226450, in(_226450, _226454)]], 417 ^ _216118 : [(418 ^ _216118) ^ [] : [-(hollywood(408 ^ []))], (420 ^ _216118) ^ [] : [-(city(408 ^ []))], (422 ^ _216118) ^ [] : [-(event(409 ^ []))], (424 ^ _216118) ^ [] : [-(chevy(410 ^ []))], (426 ^ _216118) ^ [] : [-(car(410 ^ []))], (428 ^ _216118) ^ [] : [-(white(410 ^ []))], (430 ^ _216118) ^ [] : [-(dirty(410 ^ []))], (432 ^ _216118) ^ [] : [-(old(410 ^ []))], (434 ^ _216118) ^ [] : [-(street(411 ^ []))], (436 ^ _216118) ^ [] : [-(way(411 ^ []))], (438 ^ _216118) ^ [] : [-(lonely(411 ^ []))], (440 ^ _216118) ^ [] : [-(barrel(409 ^ [], 410 ^ []))], (442 ^ _216118) ^ [] : [-(down(409 ^ [], 411 ^ []))], (444 ^ _216118) ^ [] : [-(in(409 ^ [], 408 ^ []))], (446 ^ _216118) ^ [] : [-(seat(414 ^ []))], (448 ^ _216118) ^ [] : [-(furniture(414 ^ []))], (450 ^ _216118) ^ [] : [-(front(414 ^ []))], (452 ^ _216118) ^ [] : [412 ^ [] = 413 ^ []], (454 ^ _216118) ^ [] : [-(fellow(412 ^ []))], (456 ^ _216118) ^ [] : [-(man(412 ^ []))], (458 ^ _216118) ^ [] : [-(young(412 ^ []))], (460 ^ _216118) ^ [] : [-(fellow(413 ^ []))], (462 ^ _216118) ^ [] : [-(man(413 ^ []))], (464 ^ _216118) ^ [] : [-(young(413 ^ []))], (466 ^ _216118) ^ [] : [-(412 ^ [] = 415 ^ [])], (468 ^ _216118) ^ [] : [-(in(415 ^ [], 414 ^ []))], (470 ^ _216118) ^ [] : [-(413 ^ [] = 416 ^ [])], (472 ^ _216118) ^ [] : [-(in(416 ^ [], 414 ^ []))], (474 ^ _216118) ^ [_232921, _232923, _232925, _232927, _232929, _232931, _232933, _232935, _232937] : [hollywood(_232937), city(_232937), event(_232935), street(_232933), way(_232933), lonely(_232933), chevy(_232931), car(_232931), white(_232931), dirty(_232931), old(_232931), barrel(_232935, _232931), down(_232935, _232933), in(_232935, _232937), seat(_232925), furniture(_232925), front(_232925), -(_232929 = _232927), fellow(_232929), man(_232929), young(_232929), fellow(_232927), man(_232927), young(_232927), _232929 = _232923, in(_232923, _232925), _232927 = _232921, in(_232921, _232925)]]], (2 ^ _216118) ^ [_216222] : [-(_216222 = _216222)], (4 ^ _216118) ^ [_216329, _216331] : [_216331 = _216329, -(_216329 = _216331)], (10 ^ _216118) ^ [_216533, _216535, _216537] : [-(_216537 = _216533), _216537 = _216535, _216535 = _216533], (20 ^ _216118) ^ [_216846, _216848] : [-(hollywood(_216846)), _216848 = _216846, hollywood(_216848)], (30 ^ _216118) ^ [_217141, _217143] : [-(city(_217141)), _217143 = _217141, city(_217143)], (40 ^ _216118) ^ [_217436, _217438] : [-(event(_217436)), _217438 = _217436, event(_217438)], (50 ^ _216118) ^ [_217731, _217733] : [-(street(_217731)), _217733 = _217731, street(_217733)], (60 ^ _216118) ^ [_218026, _218028] : [-(way(_218026)), _218028 = _218026, way(_218028)], (70 ^ _216118) ^ [_218321, _218323] : [-(lonely(_218321)), _218323 = _218321, lonely(_218323)], (80 ^ _216118) ^ [_218616, _218618] : [-(chevy(_218616)), _218618 = _218616, chevy(_218618)], (90 ^ _216118) ^ [_218911, _218913] : [-(car(_218911)), _218913 = _218911, car(_218913)], (100 ^ _216118) ^ [_219206, _219208] : [-(white(_219206)), _219208 = _219206, white(_219208)], (110 ^ _216118) ^ [_219501, _219503] : [-(dirty(_219501)), _219503 = _219501, dirty(_219503)], (120 ^ _216118) ^ [_219796, _219798] : [-(old(_219796)), _219798 = _219796, old(_219798)], (130 ^ _216118) ^ [_220119, _220121, _220123, _220125] : [-(barrel(_220123, _220119)), barrel(_220125, _220121), _220125 = _220123, _220121 = _220119], (144 ^ _216118) ^ [_220563, _220565, _220567, _220569] : [-(down(_220567, _220563)), down(_220569, _220565), _220569 = _220567, _220565 = _220563], (158 ^ _216118) ^ [_220979, _220981] : [-(seat(_220979)), _220981 = _220979, seat(_220981)], (168 ^ _216118) ^ [_221274, _221276] : [-(furniture(_221274)), _221276 = _221274, furniture(_221276)], (178 ^ _216118) ^ [_221569, _221571] : [-(front(_221569)), _221571 = _221569, front(_221571)], (188 ^ _216118) ^ [_221864, _221866] : [-(fellow(_221864)), _221866 = _221864, fellow(_221866)], (198 ^ _216118) ^ [_222159, _222161] : [-(man(_222159)), _222161 = _222159, man(_222161)], (208 ^ _216118) ^ [_222454, _222456] : [-(young(_222454)), _222456 = _222454, young(_222456)], (218 ^ _216118) ^ [_222757, _222759, _222761, _222763] : [-(in(_222761, _222757)), in(_222763, _222759), _222763 = _222761, _222759 = _222757]], input).
% 0.33/1.38 ncf('1',plain,[277 : 237 ^ [] = 238 ^ [], 452 : 412 ^ [] = 413 ^ []],start(232 ^ 0)).
% 0.33/1.38 ncf('1.1',plain,[-(237 ^ [] = 238 ^ []), hollywood(233 ^ []), city(233 ^ []), event(234 ^ []), chevy(236 ^ []), car(236 ^ []), white(236 ^ []), dirty(236 ^ []), old(236 ^ []), street(235 ^ []), way(235 ^ []), lonely(235 ^ []), barrel(234 ^ [], 236 ^ []), down(234 ^ [], 235 ^ []), in(234 ^ [], 233 ^ []), seat(239 ^ []), furniture(239 ^ []), front(239 ^ []), fellow(237 ^ []), man(237 ^ []), young(237 ^ []), fellow(238 ^ []), man(238 ^ []), young(238 ^ []), 237 ^ [] = 240 ^ [], in(240 ^ [], 239 ^ []), 238 ^ [] = 241 ^ [], in(241 ^ [], 239 ^ [])],extension(299 ^ 3,bind([[_226450, _226452, _226454, _226456, _226458, _226460, _226462, _226464, _226466], [241 ^ [], 240 ^ [], 239 ^ [], 238 ^ [], 237 ^ [], 235 ^ [], 236 ^ [], 234 ^ [], 233 ^ []]]))).
% 0.33/1.38 ncf('1.1.1',plain,[-(hollywood(233 ^ []))],extension(243 ^ 4)).
% 0.33/1.38 ncf('1.1.2',plain,[-(city(233 ^ []))],extension(245 ^ 4)).
% 0.33/1.38 ncf('1.1.3',plain,[-(event(234 ^ []))],extension(247 ^ 4)).
% 0.33/1.38 ncf('1.1.4',plain,[-(chevy(236 ^ []))],extension(255 ^ 4)).
% 0.33/1.38 ncf('1.1.5',plain,[-(car(236 ^ []))],extension(257 ^ 4)).
% 0.33/1.38 ncf('1.1.6',plain,[-(white(236 ^ []))],extension(259 ^ 4)).
% 0.33/1.38 ncf('1.1.7',plain,[-(dirty(236 ^ []))],extension(261 ^ 4)).
% 0.33/1.38 ncf('1.1.8',plain,[-(old(236 ^ []))],extension(263 ^ 4)).
% 0.33/1.38 ncf('1.1.9',plain,[-(street(235 ^ []))],extension(249 ^ 4)).
% 0.33/1.38 ncf('1.1.10',plain,[-(way(235 ^ []))],extension(251 ^ 4)).
% 0.33/1.38 ncf('1.1.11',plain,[-(lonely(235 ^ []))],extension(253 ^ 4)).
% 0.33/1.38 ncf('1.1.12',plain,[-(barrel(234 ^ [], 236 ^ []))],extension(265 ^ 4)).
% 0.33/1.38 ncf('1.1.13',plain,[-(down(234 ^ [], 235 ^ []))],extension(267 ^ 4)).
% 0.33/1.38 ncf('1.1.14',plain,[-(in(234 ^ [], 233 ^ []))],extension(269 ^ 4)).
% 0.33/1.38 ncf('1.1.15',plain,[-(seat(239 ^ []))],extension(271 ^ 4)).
% 0.33/1.38 ncf('1.1.16',plain,[-(furniture(239 ^ []))],extension(273 ^ 4)).
% 0.33/1.38 ncf('1.1.17',plain,[-(front(239 ^ []))],extension(275 ^ 4)).
% 0.33/1.38 ncf('1.1.18',plain,[-(fellow(237 ^ []))],extension(279 ^ 4)).
% 0.33/1.38 ncf('1.1.19',plain,[-(man(237 ^ []))],extension(281 ^ 4)).
% 0.33/1.38 ncf('1.1.20',plain,[-(young(237 ^ []))],extension(283 ^ 4)).
% 0.33/1.38 ncf('1.1.21',plain,[-(fellow(238 ^ []))],extension(285 ^ 4)).
% 0.33/1.38 ncf('1.1.22',plain,[-(man(238 ^ []))],extension(287 ^ 4)).
% 0.33/1.38 ncf('1.1.23',plain,[-(young(238 ^ []))],extension(289 ^ 4)).
% 0.33/1.38 ncf('1.1.24',plain,[-(237 ^ [] = 240 ^ [])],extension(291 ^ 4)).
% 0.33/1.38 ncf('1.1.25',plain,[-(in(240 ^ [], 239 ^ []))],extension(293 ^ 4)).
% 0.33/1.38 ncf('1.1.26',plain,[-(238 ^ [] = 241 ^ [])],extension(295 ^ 4)).
% 0.33/1.38 ncf('1.1.27',plain,[-(in(241 ^ [], 239 ^ []))],extension(297 ^ 4)).
% 0.33/1.38 ncf('1.2',plain,[-(412 ^ [] = 413 ^ []), hollywood(408 ^ []), city(408 ^ []), event(409 ^ []), street(411 ^ []), way(411 ^ []), lonely(411 ^ []), chevy(410 ^ []), car(410 ^ []), white(410 ^ []), dirty(410 ^ []), old(410 ^ []), barrel(409 ^ [], 410 ^ []), down(409 ^ [], 411 ^ []), in(409 ^ [], 408 ^ []), seat(414 ^ []), furniture(414 ^ []), front(414 ^ []), fellow(412 ^ []), man(412 ^ []), young(412 ^ []), fellow(413 ^ []), man(413 ^ []), young(413 ^ []), 412 ^ [] = 415 ^ [], in(415 ^ [], 414 ^ []), 413 ^ [] = 416 ^ [], in(416 ^ [], 414 ^ [])],extension(474 ^ 3,bind([[_232921, _232923, _232925, _232927, _232929, _232931, _232933, _232935, _232937], [416 ^ [], 415 ^ [], 414 ^ [], 413 ^ [], 412 ^ [], 410 ^ [], 411 ^ [], 409 ^ [], 408 ^ []]]))).
% 0.33/1.38 ncf('1.2.1',plain,[-(hollywood(408 ^ []))],extension(418 ^ 4)).
% 0.33/1.38 ncf('1.2.2',plain,[-(city(408 ^ []))],extension(420 ^ 4)).
% 0.33/1.38 ncf('1.2.3',plain,[-(event(409 ^ []))],extension(422 ^ 4)).
% 0.33/1.38 ncf('1.2.4',plain,[-(street(411 ^ []))],extension(434 ^ 4)).
% 0.33/1.38 ncf('1.2.5',plain,[-(way(411 ^ []))],extension(436 ^ 4)).
% 0.33/1.38 ncf('1.2.6',plain,[-(lonely(411 ^ []))],extension(438 ^ 4)).
% 0.33/1.38 ncf('1.2.7',plain,[-(chevy(410 ^ []))],extension(424 ^ 4)).
% 0.33/1.38 ncf('1.2.8',plain,[-(car(410 ^ []))],extension(426 ^ 4)).
% 0.33/1.38 ncf('1.2.9',plain,[-(white(410 ^ []))],extension(428 ^ 4)).
% 0.33/1.38 ncf('1.2.10',plain,[-(dirty(410 ^ []))],extension(430 ^ 4)).
% 0.33/1.38 ncf('1.2.11',plain,[-(old(410 ^ []))],extension(432 ^ 4)).
% 0.33/1.38 ncf('1.2.12',plain,[-(barrel(409 ^ [], 410 ^ []))],extension(440 ^ 4)).
% 0.33/1.38 ncf('1.2.13',plain,[-(down(409 ^ [], 411 ^ []))],extension(442 ^ 4)).
% 0.33/1.38 ncf('1.2.14',plain,[-(in(409 ^ [], 408 ^ []))],extension(444 ^ 4)).
% 0.33/1.38 ncf('1.2.15',plain,[-(seat(414 ^ []))],extension(446 ^ 4)).
% 0.33/1.38 ncf('1.2.16',plain,[-(furniture(414 ^ []))],extension(448 ^ 4)).
% 0.33/1.38 ncf('1.2.17',plain,[-(front(414 ^ []))],extension(450 ^ 4)).
% 0.33/1.38 ncf('1.2.18',plain,[-(fellow(412 ^ []))],extension(454 ^ 4)).
% 0.33/1.38 ncf('1.2.19',plain,[-(man(412 ^ []))],extension(456 ^ 4)).
% 0.33/1.38 ncf('1.2.20',plain,[-(young(412 ^ []))],extension(458 ^ 4)).
% 0.33/1.38 ncf('1.2.21',plain,[-(fellow(413 ^ []))],extension(460 ^ 4)).
% 0.33/1.38 ncf('1.2.22',plain,[-(man(413 ^ []))],extension(462 ^ 4)).
% 0.33/1.38 ncf('1.2.23',plain,[-(young(413 ^ []))],extension(464 ^ 4)).
% 0.33/1.38 ncf('1.2.24',plain,[-(412 ^ [] = 415 ^ [])],extension(466 ^ 4)).
% 0.33/1.38 ncf('1.2.25',plain,[-(in(415 ^ [], 414 ^ []))],extension(468 ^ 4)).
% 0.33/1.38 ncf('1.2.26',plain,[-(413 ^ [] = 416 ^ [])],extension(470 ^ 4)).
% 0.33/1.38 ncf('1.2.27',plain,[-(in(416 ^ [], 414 ^ []))],extension(472 ^ 4)).
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------