%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : GRA003+1 : TPTP v8.1.2. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n017.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 3.10s 3.46s
% Output : Proof 3.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRA003+1 : TPTP v8.1.2. Bugfixed v3.2.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n017.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 20:03:00 EDT 2023
% 0.12/0.34 % CPUTime :
% 3.10/3.46
% 3.10/3.46 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 3.10/3.46 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.10/3.46 %-----------------------------------------------------
% 3.10/3.46 ncf(matrix, plain, [(581 ^ _99260) ^ [] : [-(shortest_path(575 ^ [], 576 ^ [], 579 ^ []))], (583 ^ _99260) ^ [] : [-(precedes(577 ^ [], 578 ^ [], 579 ^ []))], (585 ^ _99260) ^ [] : [vertex(575 ^ []), vertex(576 ^ []), -(575 ^ [] = 576 ^ []), edge(577 ^ []), edge(578 ^ []), -(577 ^ [] = 578 ^ []), path(575 ^ [], 576 ^ [], 579 ^ [])], (168 ^ _99260) ^ [_104862, _104864, _104866, _104868] : [-(path_cons(_104868, _104864) = path_cons(_104866, _104862)), _104868 = _104866, _104864 = _104862], (178 ^ _99260) ^ [_105193, _105195] : [_105195 = _105193, -(tail_of(_105195) = tail_of(_105193))], (184 ^ _99260) ^ [_105411, _105413] : [_105413 = _105411, -(head_of(_105413) = head_of(_105411))], (190 ^ _99260) ^ [_105657, _105659, _105661, _105663] : [-(minus(_105663, _105659) = minus(_105661, _105657)), _105663 = _105661, _105659 = _105657], (200 ^ _99260) ^ [_105988, _105990] : [_105990 = _105988, -(length_of(_105990) = length_of(_105988))], (206 ^ _99260) ^ [_106214, _106216, _106218, _106220] : [-(number_of_in(_106220, _106216) = number_of_in(_106218, _106214)), _106220 = _106218, _106216 = _106214], (2 ^ _99260) ^ [_99404] : [-(_99404 = _99404)], (4 ^ _99260) ^ [_99511, _99513] : [_99513 = _99511, -(_99511 = _99513)], (10 ^ _99260) ^ [_99715, _99717, _99719] : [-(_99719 = _99715), _99719 = _99717, _99717 = _99715], (20 ^ _99260) ^ [_100056, _100058, _100060, _100062] : [-(in_path(_100060, _100056)), in_path(_100062, _100058), _100062 = _100060, _100058 = _100056], (34 ^ _99260) ^ [_100500, _100502, _100504, _100506] : [-(on_path(_100504, _100500)), on_path(_100506, _100502), _100506 = _100504, _100502 = _100500], (48 ^ _99260) ^ [_100944, _100946, _100948, _100950] : [-(sequential(_100948, _100944)), sequential(_100950, _100946), _100950 = _100948, _100946 = _100944], (62 ^ _99260) ^ [_101416, _101418, _101420, _101422, _101424, _101426] : [-(triangle(_101424, _101420, _101416)), triangle(_101426, _101422, _101418), _101426 = _101424, _101422 = _101420, _101418 = _101416], (80 ^ _99260) ^ [_101997, _101999, _102001, _102003] : [-(less_or_equal(_102001, _101997)), less_or_equal(_102003, _101999), _102003 = _102001, _101999 = _101997], (94 ^ _99260) ^ [_102469, _102471, _102473, _102475, _102477, _102479] : [-(shortest_path(_102477, _102473, _102469)), shortest_path(_102479, _102475, _102471), _102479 = _102477, _102475 = _102473, _102471 = _102469], (112 ^ _99260) ^ [_103078, _103080, _103082, _103084, _103086, _103088] : [-(precedes(_103086, _103082, _103078)), precedes(_103088, _103084, _103080), _103088 = _103086, _103084 = _103082, _103080 = _103078], (130 ^ _99260) ^ [_103631, _103633] : [-(vertex(_103631)), _103633 = _103631, vertex(_103633)], (140 ^ _99260) ^ [_103926, _103928] : [-(edge(_103926)), _103928 = _103926, edge(_103928)], (150 ^ _99260) ^ [_104257, _104259, _104261, _104263, _104265, _104267] : [-(path(_104265, _104261, _104257)), path(_104267, _104263, _104259), _104267 = _104265, _104263 = _104261, _104259 = _104257], (544 ^ _99260) ^ [_118215, _118217, _118219] : [path(_118219, _118217, _118215), -(length_of(_118215) = number_of_in(edges, _118215))], (550 ^ _99260) ^ [_118457, _118459, _118461] : [path(_118461, _118459, _118457), -(number_of_in(sequential_pairs, _118457) = minus(length_of(_118457), n1))], (574 ^ _99260) ^ [_119491, _119493] : [-(less_or_equal(number_of_in(_119493, _119491), number_of_in(_119493, graph)))], (556 ^ _99260) ^ [_118705, _118707, _118709] : [-(number_of_in(sequential_pairs, _118709) = number_of_in(triangles, _118709)), path(_118707, _118705, _118709), 563 ^ _99260 : [(564 ^ _99260) ^ [] : [-(on_path(561 ^ [_118705, _118707, _118709], _118709))], (566 ^ _99260) ^ [] : [-(on_path(562 ^ [_118705, _118707, _118709], _118709))], (568 ^ _99260) ^ [] : [-(sequential(561 ^ [_118705, _118707, _118709], 562 ^ [_118705, _118707, _118709]))], (570 ^ _99260) ^ [_119325] : [triangle(561 ^ [_118705, _118707, _118709], 562 ^ [_118705, _118707, _118709], _119325)]]], (502 ^ _99260) ^ [_116977, _116979, _116981] : [triangle(_116981, _116979, _116977), 505 ^ _99260 : [(506 ^ _99260) ^ [] : [-(edge(_116981))], (508 ^ _99260) ^ [] : [-(edge(_116979))], (510 ^ _99260) ^ [] : [-(edge(_116977))], (512 ^ _99260) ^ [] : [-(sequential(_116981, _116979))], (514 ^ _99260) ^ [] : [-(sequential(_116979, _116977))], (516 ^ _99260) ^ [] : [-(sequential(_116977, _116981))]]], (518 ^ _99260) ^ [_117522, _117524, _117526] : [-(triangle(_117526, _117524, _117522)), edge(_117526), edge(_117524), edge(_117522), sequential(_117526, _117524), sequential(_117524, _117522), sequential(_117522, _117526)], (216 ^ _99260) ^ [_106573] : [edge(_106573), head_of(_106573) = tail_of(_106573)], (222 ^ _99260) ^ [_106770] : [edge(_106770), 225 ^ _99260 : [(226 ^ _99260) ^ [] : [-(vertex(head_of(_106770)))], (228 ^ _99260) ^ [] : [-(vertex(tail_of(_106770)))]]], (230 ^ _99260) ^ [] : [complete, 233 ^ _99260 : [(234 ^ _99260) ^ [_107111, _107113] : [vertex(_107113), vertex(_107111), -(_107113 = _107111), 246 ^ _99260 : [(247 ^ _99260) ^ [] : [-(edge(245 ^ [_107111, _107113]))], (249 ^ _99260) ^ [] : [250 ^ _99260 : [(251 ^ _99260) ^ [] : [-(_107113 = head_of(245 ^ [_107111, _107113]))], (253 ^ _99260) ^ [] : [-(_107111 = tail_of(245 ^ [_107111, _107113]))], (255 ^ _99260) ^ [] : [_107111 = head_of(245 ^ [_107111, _107113]), _107113 = tail_of(245 ^ [_107111, _107113])]], 260 ^ _99260 : [(261 ^ _99260) ^ [] : [-(_107111 = head_of(245 ^ [_107111, _107113]))], (263 ^ _99260) ^ [] : [-(_107113 = tail_of(245 ^ [_107111, _107113]))], (265 ^ _99260) ^ [] : [_107113 = head_of(245 ^ [_107111, _107113]), _107111 = tail_of(245 ^ [_107111, _107113])]]]]]]], (271 ^ _99260) ^ [_108319, _108321, _108323] : [-(path(_108323, _108321, _108319)), vertex(_108323), vertex(_108321), 280 ^ _99260 : [(281 ^ _99260) ^ [_108629] : [edge(_108629), _108323 = tail_of(_108629), 288 ^ _99260 : [(289 ^ _99260) ^ [] : [_108321 = head_of(_108629), _108319 = path_cons(_108629, empty)], (295 ^ _99260) ^ [_109063] : [path(head_of(_108629), _108321, _109063), _108319 = path_cons(_108629, _109063)]]]]], (303 ^ _99260) ^ [_109397, _109399, _109401] : [path(_109401, _109399, _109397), 306 ^ _99260 : [(307 ^ _99260) ^ [] : [-(vertex(_109401))], (309 ^ _99260) ^ [] : [-(vertex(_109399))], (312 ^ _99260) ^ [] : [-(edge(310 ^ [_109397, _109399, _109401]))], (314 ^ _99260) ^ [] : [-(_109401 = tail_of(310 ^ [_109397, _109399, _109401]))], (316 ^ _99260) ^ [] : [317 ^ _99260 : [(318 ^ _99260) ^ [] : [-(_109399 = head_of(310 ^ [_109397, _109399, _109401]))], (320 ^ _99260) ^ [] : [-(_109397 = path_cons(310 ^ [_109397, _109399, _109401], empty))], (322 ^ _99260) ^ [_110186] : [path(head_of(310 ^ [_109397, _109399, _109401]), _109399, _110186), _109397 = path_cons(310 ^ [_109397, _109399, _109401], _110186)]], 328 ^ _99260 : [(329 ^ _99260) ^ [] : [-(path(head_of(310 ^ [_109397, _109399, _109401]), _109399, 327 ^ [_109397, _109399, _109401]))], (331 ^ _99260) ^ [] : [-(_109397 = path_cons(310 ^ [_109397, _109399, _109401], 327 ^ [_109397, _109399, _109401]))], (333 ^ _99260) ^ [] : [_109399 = head_of(310 ^ [_109397, _109399, _109401]), _109397 = path_cons(310 ^ [_109397, _109399, _109401], empty)]]]]], (339 ^ _99260) ^ [_110932, _110934, _110936, _110938] : [346 ^ _99260 : [(347 ^ _99260) ^ [] : [-(edge(_110932))], (349 ^ _99260) ^ [] : [-(in_path(head_of(_110932), _110934))], (351 ^ _99260) ^ [] : [-(in_path(tail_of(_110932), _110934))]], path(_110938, _110936, _110934), on_path(_110932, _110934)], (353 ^ _99260) ^ [_111444, _111446, _111448, _111450] : [path(_111450, _111448, _111446), in_path(_111444, _111446), 360 ^ _99260 : [(361 ^ _99260) ^ [] : [-(vertex(_111444))], (364 ^ _99260) ^ [] : [-(on_path(362 ^ [_111444, _111446, _111448, _111450], _111446))], (366 ^ _99260) ^ [] : [-(_111444 = head_of(362 ^ [_111444, _111446, _111448, _111450])), -(_111444 = tail_of(362 ^ [_111444, _111446, _111448, _111450]))]]], (372 ^ _99260) ^ [_112164, _112166] : [sequential(_112166, _112164), 375 ^ _99260 : [(376 ^ _99260) ^ [] : [-(edge(_112166))], (378 ^ _99260) ^ [] : [-(edge(_112164))], (380 ^ _99260) ^ [] : [_112166 = _112164], (382 ^ _99260) ^ [] : [-(head_of(_112166) = tail_of(_112164))]]], (384 ^ _99260) ^ [_112554, _112556] : [-(sequential(_112556, _112554)), edge(_112556), edge(_112554), -(_112556 = _112554), head_of(_112556) = tail_of(_112554)], (402 ^ _99260) ^ [_113054, _113056, _113058] : [path(_113056, _113054, _113058), 405 ^ _99260 : [(406 ^ _99260) ^ [_113247, _113249] : [-(precedes(_113249, _113247, _113058)), on_path(_113249, _113058), on_path(_113247, _113058), 415 ^ _99260 : [(416 ^ _99260) ^ [] : [sequential(_113249, _113247)], (418 ^ _99260) ^ [_113624] : [sequential(_113249, _113624), precedes(_113624, _113247, _113058)]]]]], (426 ^ _99260) ^ [_113956, _113958, _113960] : [path(_113958, _113956, _113960), 429 ^ _99260 : [(430 ^ _99260) ^ [_114151, _114153] : [precedes(_114153, _114151, _113960), 433 ^ _99260 : [(434 ^ _99260) ^ [] : [-(on_path(_114153, _113960))], (436 ^ _99260) ^ [] : [-(on_path(_114151, _113960))], (438 ^ _99260) ^ [] : [448 ^ _99260 : [(449 ^ _99260) ^ [] : [-(sequential(_114153, 447 ^ [_113956, _113958, _113960, _114151, _114153]))], (451 ^ _99260) ^ [] : [-(precedes(447 ^ [_113956, _113958, _113960, _114151, _114153], _114151, _113960))], (453 ^ _99260) ^ [] : [sequential(_114153, _114151)]], 439 ^ _99260 : [(440 ^ _99260) ^ [] : [-(sequential(_114153, _114151))], (442 ^ _99260) ^ [_114594] : [sequential(_114153, _114594), precedes(_114594, _114151, _113960)]]]]]]], (486 ^ _99260) ^ [_116297, _116299, _116301, _116303, _116305] : [shortest_path(_116305, _116303, _116297), precedes(_116301, _116299, _116297), 493 ^ _99260 : [(500 ^ _99260) ^ [] : [precedes(_116299, _116301, _116297)], (494 ^ _99260) ^ [_116590] : [tail_of(_116590) = tail_of(_116301), head_of(_116590) = head_of(_116299)]]], (455 ^ _99260) ^ [_115196, _115198, _115200] : [shortest_path(_115200, _115198, _115196), 458 ^ _99260 : [(459 ^ _99260) ^ [] : [-(path(_115200, _115198, _115196))], (461 ^ _99260) ^ [] : [_115200 = _115198], (463 ^ _99260) ^ [_115495] : [path(_115200, _115198, _115495), -(less_or_equal(length_of(_115196), length_of(_115495)))]]], (469 ^ _99260) ^ [_115694, _115696, _115698] : [-(shortest_path(_115698, _115696, _115694)), path(_115698, _115696, _115694), -(_115698 = _115696), 479 ^ _99260 : [(480 ^ _99260) ^ [] : [-(path(_115698, _115696, 478 ^ [_115694, _115696, _115698]))], (482 ^ _99260) ^ [] : [less_or_equal(length_of(_115694), length_of(478 ^ [_115694, _115696, _115698]))]]]], input).
% 3.10/3.46 ncf('1',plain,[shortest_path(575 ^ [], 576 ^ [], 579 ^ []), 461 : 575 ^ [] = 576 ^ []],start(455 ^ 0,bind([[_115196, _115198, _115200], [579 ^ [], 576 ^ [], 575 ^ []]]))).
% 3.10/3.46 ncf('1.1',plain,[-(shortest_path(575 ^ [], 576 ^ [], 579 ^ []))],extension(581 ^ 1)).
% 3.10/3.46 ncf('1.2',plain,[-(575 ^ [] = 576 ^ []), vertex(575 ^ []), vertex(576 ^ []), edge(577 ^ []), edge(578 ^ []), -(577 ^ [] = 578 ^ []), path(575 ^ [], 576 ^ [], 579 ^ [])],extension(585 ^ 3)).
% 3.10/3.46 ncf('1.2.1',plain,[-(vertex(575 ^ [])), path(575 ^ [], 576 ^ [], 579 ^ [])],extension(303 ^ 4,bind([[_109397, _109399, _109401], [579 ^ [], 576 ^ [], 575 ^ []]]))).
% 3.10/3.46 ncf('1.2.1.1',plain,[-(path(575 ^ [], 576 ^ [], 579 ^ [])), path(575 ^ [], 576 ^ [], 579 ^ []), 575 ^ [] = 575 ^ [], 576 ^ [] = 576 ^ [], 579 ^ [] = 579 ^ []],extension(150 ^ 5,bind([[_104257, _104259, _104261, _104263, _104265, _104267], [579 ^ [], 579 ^ [], 576 ^ [], 576 ^ [], 575 ^ [], 575 ^ []]]))).
% 3.10/3.46 ncf('1.2.1.1.1',plain,[-(path(575 ^ [], 576 ^ [], 579 ^ []))],extension(459 ^ 6)).
% 3.10/3.46 ncf('1.2.1.1.2',plain,[-(575 ^ [] = 575 ^ [])],extension(2 ^ 6,bind([[_99404], [575 ^ []]]))).
% 3.10/3.46 ncf('1.2.1.1.3',plain,[-(576 ^ [] = 576 ^ [])],extension(2 ^ 6,bind([[_99404], [576 ^ []]]))).
% 3.10/3.46 ncf('1.2.1.1.4',plain,[-(579 ^ [] = 579 ^ [])],extension(2 ^ 6,bind([[_99404], [579 ^ []]]))).
% 3.10/3.46 ncf('1.2.2',plain,[-(vertex(576 ^ [])), path(575 ^ [], 576 ^ [], 579 ^ [])],extension(303 ^ 4,bind([[_109397, _109399, _109401], [579 ^ [], 576 ^ [], 575 ^ []]]))).
% 3.10/3.46 ncf('1.2.2.1',plain,[-(path(575 ^ [], 576 ^ [], 579 ^ [])), path(575 ^ [], 576 ^ [], 579 ^ []), 575 ^ [] = 575 ^ [], 576 ^ [] = 576 ^ [], 579 ^ [] = 579 ^ []],extension(150 ^ 5,bind([[_104257, _104259, _104261, _104263, _104265, _104267], [579 ^ [], 579 ^ [], 576 ^ [], 576 ^ [], 575 ^ [], 575 ^ []]]))).
% 3.10/3.46 ncf('1.2.2.1.1',plain,[-(path(575 ^ [], 576 ^ [], 579 ^ []))],extension(459 ^ 6)).
% 3.10/3.46 ncf('1.2.2.1.2',plain,[-(575 ^ [] = 575 ^ [])],extension(2 ^ 6,bind([[_99404], [575 ^ []]]))).
% 3.10/3.46 ncf('1.2.2.1.3',plain,[-(576 ^ [] = 576 ^ [])],extension(2 ^ 6,bind([[_99404], [576 ^ []]]))).
% 3.10/3.46 ncf('1.2.2.1.4',plain,[-(579 ^ [] = 579 ^ [])],extension(2 ^ 6,bind([[_99404], [579 ^ []]]))).
% 3.10/3.46 ncf('1.2.3',plain,[-(edge(577 ^ [])), path(575 ^ [], 576 ^ [], 579 ^ []), on_path(577 ^ [], 579 ^ [])],extension(339 ^ 4,bind([[_110932, _110934, _110936, _110938], [577 ^ [], 579 ^ [], 576 ^ [], 575 ^ []]]))).
% 3.10/3.46 ncf('1.2.3.1',plain,[-(path(575 ^ [], 576 ^ [], 579 ^ [])), path(575 ^ [], 576 ^ [], 579 ^ []), 575 ^ [] = 575 ^ [], 576 ^ [] = 576 ^ [], 579 ^ [] = 579 ^ []],extension(150 ^ 5,bind([[_104257, _104259, _104261, _104263, _104265, _104267], [579 ^ [], 579 ^ [], 576 ^ [], 576 ^ [], 575 ^ [], 575 ^ []]]))).
% 3.10/3.46 ncf('1.2.3.1.1',plain,[-(path(575 ^ [], 576 ^ [], 579 ^ []))],extension(459 ^ 6)).
% 3.10/3.46 ncf('1.2.3.1.2',plain,[-(575 ^ [] = 575 ^ [])],extension(2 ^ 6,bind([[_99404], [575 ^ []]]))).
% 3.10/3.46 ncf('1.2.3.1.3',plain,[-(576 ^ [] = 576 ^ [])],extension(2 ^ 6,bind([[_99404], [576 ^ []]]))).
% 3.10/3.46 ncf('1.2.3.1.4',plain,[-(579 ^ [] = 579 ^ [])],extension(2 ^ 6,bind([[_99404], [579 ^ []]]))).
% 3.10/3.46 ncf('1.2.3.2',plain,[-(on_path(577 ^ [], 579 ^ [])), 430 : precedes(577 ^ [], 578 ^ [], 579 ^ []), 430 : path(575 ^ [], 576 ^ [], 579 ^ [])],extension(426 ^ 5,bind([[_113956, _113958, _113960, _114151, _114153], [576 ^ [], 575 ^ [], 579 ^ [], 578 ^ [], 577 ^ []]]))).
% 3.10/3.46 ncf('1.2.3.2.1',plain,[-(precedes(577 ^ [], 578 ^ [], 579 ^ []))],extension(583 ^ 8)).
% 3.10/3.46 ncf('1.2.3.2.2',plain,[-(path(575 ^ [], 576 ^ [], 579 ^ []))],extension(459 ^ 6)).
% 3.10/3.46 ncf('1.2.4',plain,[-(edge(578 ^ [])), path(575 ^ [], 576 ^ [], 579 ^ []), on_path(578 ^ [], 579 ^ [])],extension(339 ^ 4,bind([[_110932, _110934, _110936, _110938], [578 ^ [], 579 ^ [], 576 ^ [], 575 ^ []]]))).
% 3.10/3.46 ncf('1.2.4.1',plain,[-(path(575 ^ [], 576 ^ [], 579 ^ [])), path(575 ^ [], 576 ^ [], 579 ^ []), 575 ^ [] = 575 ^ [], 576 ^ [] = 576 ^ [], 579 ^ [] = 579 ^ []],extension(150 ^ 5,bind([[_104257, _104259, _104261, _104263, _104265, _104267], [579 ^ [], 579 ^ [], 576 ^ [], 576 ^ [], 575 ^ [], 575 ^ []]]))).
% 3.10/3.46 ncf('1.2.4.1.1',plain,[-(path(575 ^ [], 576 ^ [], 579 ^ []))],extension(459 ^ 6)).
% 3.10/3.46 ncf('1.2.4.1.2',plain,[-(575 ^ [] = 575 ^ [])],extension(2 ^ 6,bind([[_99404], [575 ^ []]]))).
% 3.10/3.46 ncf('1.2.4.1.3',plain,[-(576 ^ [] = 576 ^ [])],extension(2 ^ 6,bind([[_99404], [576 ^ []]]))).
% 3.10/3.46 ncf('1.2.4.1.4',plain,[-(579 ^ [] = 579 ^ [])],extension(2 ^ 6,bind([[_99404], [579 ^ []]]))).
% 3.10/3.46 ncf('1.2.4.2',plain,[-(on_path(578 ^ [], 579 ^ [])), 430 : precedes(577 ^ [], 578 ^ [], 579 ^ []), 430 : path(575 ^ [], 576 ^ [], 579 ^ [])],extension(426 ^ 5,bind([[_113956, _113958, _113960, _114151, _114153], [576 ^ [], 575 ^ [], 579 ^ [], 578 ^ [], 577 ^ []]]))).
% 3.10/3.46 ncf('1.2.4.2.1',plain,[-(precedes(577 ^ [], 578 ^ [], 579 ^ []))],extension(583 ^ 8)).
% 3.10/3.46 ncf('1.2.4.2.2',plain,[-(path(575 ^ [], 576 ^ [], 579 ^ []))],extension(459 ^ 6)).
% 3.10/3.46 ncf('1.2.5',plain,[577 ^ [] = 578 ^ [], -(578 ^ [] = 577 ^ [])],extension(4 ^ 4,bind([[_99511, _99513], [578 ^ [], 577 ^ []]]))).
% 3.10/3.46 ncf('1.2.5.1',plain,[578 ^ [] = 577 ^ [], -(precedes(577 ^ [], 577 ^ [], 579 ^ [])), precedes(577 ^ [], 578 ^ [], 579 ^ []), 577 ^ [] = 577 ^ [], 579 ^ [] = 579 ^ []],extension(112 ^ 5,bind([[_103078, _103080, _103082, _103084, _103086, _103088], [579 ^ [], 579 ^ [], 577 ^ [], 578 ^ [], 577 ^ [], 577 ^ []]]))).
% 3.10/3.46 ncf('1.2.5.1.1',plain,[precedes(577 ^ [], 577 ^ [], 579 ^ []), shortest_path(575 ^ [], 576 ^ [], 579 ^ []), 500 : precedes(577 ^ [], 577 ^ [], 579 ^ [])],extension(486 ^ 6,bind([[_116297, _116299, _116301, _116303, _116305], [579 ^ [], 577 ^ [], 577 ^ [], 576 ^ [], 575 ^ []]]))).
% 3.10/3.46 ncf('1.2.5.1.1.1',plain,[-(shortest_path(575 ^ [], 576 ^ [], 579 ^ []))],extension(581 ^ 7)).
% 3.10/3.46 ncf('1.2.5.1.1.2',plain,[-(precedes(577 ^ [], 577 ^ [], 579 ^ []))],reduction('1.2.5.1')).
% 3.10/3.46 ncf('1.2.5.1.2',plain,[-(precedes(577 ^ [], 578 ^ [], 579 ^ []))],extension(583 ^ 6)).
% 3.10/3.46 ncf('1.2.5.1.3',plain,[-(577 ^ [] = 577 ^ [])],extension(2 ^ 6,bind([[_99404], [577 ^ []]]))).
% 3.10/3.46 ncf('1.2.5.1.4',plain,[-(579 ^ [] = 579 ^ [])],extension(2 ^ 6,bind([[_99404], [579 ^ []]]))).
% 3.10/3.46 ncf('1.2.6',plain,[-(path(575 ^ [], 576 ^ [], 579 ^ [])), path(575 ^ [], 576 ^ [], 579 ^ []), 575 ^ [] = 575 ^ [], 576 ^ [] = 576 ^ [], 579 ^ [] = 579 ^ []],extension(150 ^ 4,bind([[_104257, _104259, _104261, _104263, _104265, _104267], [579 ^ [], 579 ^ [], 576 ^ [], 576 ^ [], 575 ^ [], 575 ^ []]]))).
% 3.10/3.46 ncf('1.2.6.1',plain,[-(path(575 ^ [], 576 ^ [], 579 ^ [])), path(575 ^ [], 576 ^ [], 579 ^ []), 575 ^ [] = 575 ^ [], 576 ^ [] = 576 ^ [], 579 ^ [] = 579 ^ []],extension(150 ^ 5,bind([[_104257, _104259, _104261, _104263, _104265, _104267], [579 ^ [], 579 ^ [], 576 ^ [], 576 ^ [], 575 ^ [], 575 ^ []]]))).
% 3.10/3.46 ncf('1.2.6.1.1',plain,[-(path(575 ^ [], 576 ^ [], 579 ^ []))],extension(459 ^ 6)).
% 3.10/3.46 ncf('1.2.6.1.2',plain,[-(575 ^ [] = 575 ^ [])],extension(2 ^ 6,bind([[_99404], [575 ^ []]]))).
% 3.10/3.46 ncf('1.2.6.1.3',plain,[-(576 ^ [] = 576 ^ [])],extension(2 ^ 6,bind([[_99404], [576 ^ []]]))).
% 3.10/3.46 ncf('1.2.6.1.4',plain,[-(579 ^ [] = 579 ^ [])],extension(2 ^ 6,bind([[_99404], [579 ^ []]]))).
% 3.10/3.46 ncf('1.2.6.2',plain,[-(575 ^ [] = 575 ^ [])],extension(2 ^ 5,bind([[_99404], [575 ^ []]]))).
% 3.10/3.46 ncf('1.2.6.3',plain,[-(576 ^ [] = 576 ^ [])],extension(2 ^ 5,bind([[_99404], [576 ^ []]]))).
% 3.10/3.46 ncf('1.2.6.4',plain,[-(579 ^ [] = 579 ^ [])],extension(2 ^ 5,bind([[_99404], [579 ^ []]]))).
% 3.10/3.46 %-----------------------------------------------------
% 3.10/3.46 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------