%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GRA005+1 : TPTP v8.1.2. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n027.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:12:52 EDT 2023
% Result : Theorem 0.30s 1.37s
% Output : Proof 0.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : GRA005+1 : TPTP v8.1.2. Bugfixed v3.2.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.11/0.33 % Computer : n027.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Thu May 18 20:53:50 EDT 2023
% 0.11/0.33 % CPUTime :
% 0.30/1.37
% 0.30/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.30/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/1.37 %-----------------------------------------------------
% 0.30/1.37 ncf(matrix, plain, [(581 ^ _88006) ^ [] : [-(shortest_path(575 ^ [], 576 ^ [], 579 ^ []))], (583 ^ _88006) ^ [] : [-(precedes(577 ^ [], 578 ^ [], 579 ^ []))], (586 ^ _88006) ^ [] : [-(edge(584 ^ []))], (588 ^ _88006) ^ [] : [-(tail_of(584 ^ []) = tail_of(577 ^ []))], (590 ^ _88006) ^ [] : [-(head_of(584 ^ []) = head_of(578 ^ []))], (168 ^ _88006) ^ [_93608, _93610, _93612, _93614] : [-(path_cons(_93614, _93610) = path_cons(_93612, _93608)), _93614 = _93612, _93610 = _93608], (178 ^ _88006) ^ [_93967, _93969, _93971, _93973] : [-(minus(_93973, _93969) = minus(_93971, _93967)), _93973 = _93971, _93969 = _93967], (188 ^ _88006) ^ [_94298, _94300] : [_94300 = _94298, -(length_of(_94300) = length_of(_94298))], (194 ^ _88006) ^ [_94544, _94546, _94548, _94550] : [-(number_of_in(_94550, _94546) = number_of_in(_94548, _94544)), _94550 = _94548, _94546 = _94544], (204 ^ _88006) ^ [_94875, _94877] : [_94877 = _94875, -(tail_of(_94877) = tail_of(_94875))], (210 ^ _88006) ^ [_95073, _95075] : [_95075 = _95073, -(head_of(_95075) = head_of(_95073))], (2 ^ _88006) ^ [_88150] : [-(_88150 = _88150)], (4 ^ _88006) ^ [_88257, _88259] : [_88259 = _88257, -(_88257 = _88259)], (10 ^ _88006) ^ [_88461, _88463, _88465] : [-(_88465 = _88461), _88465 = _88463, _88463 = _88461], (20 ^ _88006) ^ [_88802, _88804, _88806, _88808] : [-(in_path(_88806, _88802)), in_path(_88808, _88804), _88808 = _88806, _88804 = _88802], (34 ^ _88006) ^ [_89218, _89220] : [-(vertex(_89218)), _89220 = _89218, vertex(_89220)], (44 ^ _88006) ^ [_89569, _89571, _89573, _89575, _89577, _89579] : [-(path(_89577, _89573, _89569)), path(_89579, _89575, _89571), _89579 = _89577, _89575 = _89573, _89571 = _89569], (62 ^ _88006) ^ [_90150, _90152, _90154, _90156] : [-(on_path(_90154, _90150)), on_path(_90156, _90152), _90156 = _90154, _90152 = _90150], (76 ^ _88006) ^ [_90594, _90596, _90598, _90600] : [-(sequential(_90598, _90594)), sequential(_90600, _90596), _90600 = _90598, _90596 = _90594], (90 ^ _88006) ^ [_91066, _91068, _91070, _91072, _91074, _91076] : [-(triangle(_91074, _91070, _91066)), triangle(_91076, _91072, _91068), _91076 = _91074, _91072 = _91070, _91068 = _91066], (108 ^ _88006) ^ [_91647, _91649, _91651, _91653] : [-(less_or_equal(_91651, _91647)), less_or_equal(_91653, _91649), _91653 = _91651, _91649 = _91647], (122 ^ _88006) ^ [_92119, _92121, _92123, _92125, _92127, _92129] : [-(shortest_path(_92127, _92123, _92119)), shortest_path(_92129, _92125, _92121), _92129 = _92127, _92125 = _92123, _92121 = _92119], (158 ^ _88006) ^ [_93261, _93263] : [-(edge(_93261)), _93263 = _93261, edge(_93263)], (140 ^ _88006) ^ [_92728, _92730, _92732, _92734, _92736, _92738] : [-(precedes(_92736, _92732, _92728)), precedes(_92738, _92734, _92730), _92738 = _92736, _92734 = _92732, _92730 = _92728], (544 ^ _88006) ^ [_106961, _106963, _106965] : [path(_106965, _106963, _106961), -(length_of(_106961) = number_of_in(edges, _106961))], (550 ^ _88006) ^ [_107203, _107205, _107207] : [path(_107207, _107205, _107203), -(number_of_in(sequential_pairs, _107203) = minus(length_of(_107203), n1))], (574 ^ _88006) ^ [_108237, _108239] : [-(less_or_equal(number_of_in(_108239, _108237), number_of_in(_108239, graph)))], (556 ^ _88006) ^ [_107451, _107453, _107455] : [-(number_of_in(sequential_pairs, _107455) = number_of_in(triangles, _107455)), path(_107453, _107451, _107455), 563 ^ _88006 : [(564 ^ _88006) ^ [] : [-(on_path(561 ^ [_107451, _107453, _107455], _107455))], (566 ^ _88006) ^ [] : [-(on_path(562 ^ [_107451, _107453, _107455], _107455))], (568 ^ _88006) ^ [] : [-(sequential(561 ^ [_107451, _107453, _107455], 562 ^ [_107451, _107453, _107455]))], (570 ^ _88006) ^ [_108071] : [triangle(561 ^ [_107451, _107453, _107455], 562 ^ [_107451, _107453, _107455], _108071)]]], (502 ^ _88006) ^ [_105723, _105725, _105727] : [triangle(_105727, _105725, _105723), 505 ^ _88006 : [(506 ^ _88006) ^ [] : [-(edge(_105727))], (508 ^ _88006) ^ [] : [-(edge(_105725))], (510 ^ _88006) ^ [] : [-(edge(_105723))], (512 ^ _88006) ^ [] : [-(sequential(_105727, _105725))], (514 ^ _88006) ^ [] : [-(sequential(_105725, _105723))], (516 ^ _88006) ^ [] : [-(sequential(_105723, _105727))]]], (518 ^ _88006) ^ [_106268, _106270, _106272] : [-(triangle(_106272, _106270, _106268)), edge(_106272), edge(_106270), edge(_106268), sequential(_106272, _106270), sequential(_106270, _106268), sequential(_106268, _106272)], (216 ^ _88006) ^ [_95319] : [edge(_95319), head_of(_95319) = tail_of(_95319)], (222 ^ _88006) ^ [_95516] : [edge(_95516), 225 ^ _88006 : [(226 ^ _88006) ^ [] : [-(vertex(head_of(_95516)))], (228 ^ _88006) ^ [] : [-(vertex(tail_of(_95516)))]]], (230 ^ _88006) ^ [] : [complete, 233 ^ _88006 : [(234 ^ _88006) ^ [_95857, _95859] : [vertex(_95859), vertex(_95857), -(_95859 = _95857), 246 ^ _88006 : [(247 ^ _88006) ^ [] : [-(edge(245 ^ [_95857, _95859]))], (249 ^ _88006) ^ [] : [250 ^ _88006 : [(251 ^ _88006) ^ [] : [-(_95859 = head_of(245 ^ [_95857, _95859]))], (253 ^ _88006) ^ [] : [-(_95857 = tail_of(245 ^ [_95857, _95859]))], (255 ^ _88006) ^ [] : [_95857 = head_of(245 ^ [_95857, _95859]), _95859 = tail_of(245 ^ [_95857, _95859])]], 260 ^ _88006 : [(261 ^ _88006) ^ [] : [-(_95857 = head_of(245 ^ [_95857, _95859]))], (263 ^ _88006) ^ [] : [-(_95859 = tail_of(245 ^ [_95857, _95859]))], (265 ^ _88006) ^ [] : [_95859 = head_of(245 ^ [_95857, _95859]), _95857 = tail_of(245 ^ [_95857, _95859])]]]]]]], (271 ^ _88006) ^ [_97065, _97067, _97069] : [-(path(_97069, _97067, _97065)), vertex(_97069), vertex(_97067), 280 ^ _88006 : [(281 ^ _88006) ^ [_97375] : [edge(_97375), _97069 = tail_of(_97375), 288 ^ _88006 : [(289 ^ _88006) ^ [] : [_97067 = head_of(_97375), _97065 = path_cons(_97375, empty)], (295 ^ _88006) ^ [_97809] : [path(head_of(_97375), _97067, _97809), _97065 = path_cons(_97375, _97809)]]]]], (303 ^ _88006) ^ [_98143, _98145, _98147] : [path(_98147, _98145, _98143), 306 ^ _88006 : [(307 ^ _88006) ^ [] : [-(vertex(_98147))], (309 ^ _88006) ^ [] : [-(vertex(_98145))], (312 ^ _88006) ^ [] : [-(edge(310 ^ [_98143, _98145, _98147]))], (314 ^ _88006) ^ [] : [-(_98147 = tail_of(310 ^ [_98143, _98145, _98147]))], (316 ^ _88006) ^ [] : [317 ^ _88006 : [(318 ^ _88006) ^ [] : [-(_98145 = head_of(310 ^ [_98143, _98145, _98147]))], (320 ^ _88006) ^ [] : [-(_98143 = path_cons(310 ^ [_98143, _98145, _98147], empty))], (322 ^ _88006) ^ [_98932] : [path(head_of(310 ^ [_98143, _98145, _98147]), _98145, _98932), _98143 = path_cons(310 ^ [_98143, _98145, _98147], _98932)]], 328 ^ _88006 : [(329 ^ _88006) ^ [] : [-(path(head_of(310 ^ [_98143, _98145, _98147]), _98145, 327 ^ [_98143, _98145, _98147]))], (331 ^ _88006) ^ [] : [-(_98143 = path_cons(310 ^ [_98143, _98145, _98147], 327 ^ [_98143, _98145, _98147]))], (333 ^ _88006) ^ [] : [_98145 = head_of(310 ^ [_98143, _98145, _98147]), _98143 = path_cons(310 ^ [_98143, _98145, _98147], empty)]]]]], (339 ^ _88006) ^ [_99678, _99680, _99682, _99684] : [346 ^ _88006 : [(347 ^ _88006) ^ [] : [-(edge(_99678))], (349 ^ _88006) ^ [] : [-(in_path(head_of(_99678), _99680))], (351 ^ _88006) ^ [] : [-(in_path(tail_of(_99678), _99680))]], path(_99684, _99682, _99680), on_path(_99678, _99680)], (353 ^ _88006) ^ [_100190, _100192, _100194, _100196] : [path(_100196, _100194, _100192), in_path(_100190, _100192), 360 ^ _88006 : [(361 ^ _88006) ^ [] : [-(vertex(_100190))], (364 ^ _88006) ^ [] : [-(on_path(362 ^ [_100190, _100192, _100194, _100196], _100192))], (366 ^ _88006) ^ [] : [-(_100190 = head_of(362 ^ [_100190, _100192, _100194, _100196])), -(_100190 = tail_of(362 ^ [_100190, _100192, _100194, _100196]))]]], (372 ^ _88006) ^ [_100910, _100912] : [sequential(_100912, _100910), 375 ^ _88006 : [(376 ^ _88006) ^ [] : [-(edge(_100912))], (378 ^ _88006) ^ [] : [-(edge(_100910))], (380 ^ _88006) ^ [] : [_100912 = _100910], (382 ^ _88006) ^ [] : [-(head_of(_100912) = tail_of(_100910))]]], (384 ^ _88006) ^ [_101300, _101302] : [-(sequential(_101302, _101300)), edge(_101302), edge(_101300), -(_101302 = _101300), head_of(_101302) = tail_of(_101300)], (402 ^ _88006) ^ [_101800, _101802, _101804] : [path(_101802, _101800, _101804), 405 ^ _88006 : [(406 ^ _88006) ^ [_101993, _101995] : [-(precedes(_101995, _101993, _101804)), on_path(_101995, _101804), on_path(_101993, _101804), 415 ^ _88006 : [(416 ^ _88006) ^ [] : [sequential(_101995, _101993)], (418 ^ _88006) ^ [_102370] : [sequential(_101995, _102370), precedes(_102370, _101993, _101804)]]]]], (426 ^ _88006) ^ [_102702, _102704, _102706] : [path(_102704, _102702, _102706), 429 ^ _88006 : [(430 ^ _88006) ^ [_102897, _102899] : [precedes(_102899, _102897, _102706), 433 ^ _88006 : [(434 ^ _88006) ^ [] : [-(on_path(_102899, _102706))], (436 ^ _88006) ^ [] : [-(on_path(_102897, _102706))], (438 ^ _88006) ^ [] : [448 ^ _88006 : [(449 ^ _88006) ^ [] : [-(sequential(_102899, 447 ^ [_102702, _102704, _102706, _102897, _102899]))], (451 ^ _88006) ^ [] : [-(precedes(447 ^ [_102702, _102704, _102706, _102897, _102899], _102897, _102706))], (453 ^ _88006) ^ [] : [sequential(_102899, _102897)]], 439 ^ _88006 : [(440 ^ _88006) ^ [] : [-(sequential(_102899, _102897))], (442 ^ _88006) ^ [_103340] : [sequential(_102899, _103340), precedes(_103340, _102897, _102706)]]]]]]], (486 ^ _88006) ^ [_105043, _105045, _105047, _105049, _105051] : [shortest_path(_105051, _105049, _105043), precedes(_105047, _105045, _105043), 493 ^ _88006 : [(500 ^ _88006) ^ [] : [precedes(_105045, _105047, _105043)], (494 ^ _88006) ^ [_105336] : [tail_of(_105336) = tail_of(_105047), head_of(_105336) = head_of(_105045)]]], (455 ^ _88006) ^ [_103942, _103944, _103946] : [shortest_path(_103946, _103944, _103942), 458 ^ _88006 : [(459 ^ _88006) ^ [] : [-(path(_103946, _103944, _103942))], (461 ^ _88006) ^ [] : [_103946 = _103944], (463 ^ _88006) ^ [_104241] : [path(_103946, _103944, _104241), -(less_or_equal(length_of(_103942), length_of(_104241)))]]], (469 ^ _88006) ^ [_104440, _104442, _104444] : [-(shortest_path(_104444, _104442, _104440)), path(_104444, _104442, _104440), -(_104444 = _104442), 479 ^ _88006 : [(480 ^ _88006) ^ [] : [-(path(_104444, _104442, 478 ^ [_104440, _104442, _104444]))], (482 ^ _88006) ^ [] : [less_or_equal(length_of(_104440), length_of(478 ^ [_104440, _104442, _104444]))]]]], input).
% 0.30/1.37 ncf('1',plain,[shortest_path(575 ^ [], 576 ^ [], 579 ^ []), precedes(577 ^ [], 578 ^ [], 579 ^ []), 494 : tail_of(584 ^ []) = tail_of(577 ^ []), 494 : head_of(584 ^ []) = head_of(578 ^ [])],start(486 ^ 0,bind([[_105043, _105045, _105047, _105049, _105051, _105336], [579 ^ [], 578 ^ [], 577 ^ [], 576 ^ [], 575 ^ [], 584 ^ []]]))).
% 0.30/1.37 ncf('1.1',plain,[-(shortest_path(575 ^ [], 576 ^ [], 579 ^ []))],extension(581 ^ 1)).
% 0.30/1.37 ncf('1.2',plain,[-(precedes(577 ^ [], 578 ^ [], 579 ^ []))],extension(583 ^ 1)).
% 0.30/1.37 ncf('1.3',plain,[-(tail_of(584 ^ []) = tail_of(577 ^ []))],extension(588 ^ 3)).
% 0.30/1.37 ncf('1.4',plain,[-(head_of(584 ^ []) = head_of(578 ^ []))],extension(590 ^ 3)).
% 0.30/1.37 %-----------------------------------------------------
% 0.30/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------