%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV408+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n013.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 12:20:35 EDT 2023
% Result : Theorem 0.65s 1.39s
% Output : Proof 0.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV408+2 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n013.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Fri May 19 02:32:50 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.65/1.39
% 0.65/1.39 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.65/1.39 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.65/1.39 %-----------------------------------------------------
% 0.65/1.39 ncf(matrix, plain, [(611 ^ _120271) ^ [] : [-(contains_slb(607 ^ [], 609 ^ []))], (613 ^ _120271) ^ [] : [-(strictly_less_than(609 ^ [], findmin_cpq_res(triple(606 ^ [], 607 ^ [], 608 ^ []))))], (615 ^ _120271) ^ [] : [pair_in_list(update_slb(607 ^ [], findmin_pqp_res(606 ^ [])), 609 ^ [], findmin_pqp_res(606 ^ []))], (617 ^ _120271) ^ [_142968] : [pair_in_list(update_slb(607 ^ [], findmin_pqp_res(606 ^ [])), 609 ^ [], _142968), less_than(findmin_pqp_res(606 ^ []), _142968)], (2 ^ _120271) ^ [_120415] : [-(_120415 = _120415)], (4 ^ _120271) ^ [_120522, _120524] : [_120524 = _120522, -(_120522 = _120524)], (10 ^ _120271) ^ [_120726, _120728, _120730] : [-(_120730 = _120726), _120730 = _120728, _120728 = _120726], (20 ^ _120271) ^ [_121039, _121041] : [-(isnonempty_slb(_121039)), _121041 = _121039, isnonempty_slb(_121041)], (30 ^ _120271) ^ [_121362, _121364, _121366, _121368] : [-(succ_cpq(_121366, _121362)), succ_cpq(_121368, _121364), _121368 = _121366, _121364 = _121362], (44 ^ _120271) ^ [_121778, _121780] : [-(check_cpq(_121778)), _121780 = _121778, check_cpq(_121780)], (54 ^ _120271) ^ [_122101, _122103, _122105, _122107] : [-(contains_cpq(_122105, _122101)), contains_cpq(_122107, _122103), _122107 = _122105, _122103 = _122101], (68 ^ _120271) ^ [_122517, _122519] : [-(ok(_122517)), _122519 = _122517, ok(_122519)], (78 ^ _120271) ^ [_122840, _122842, _122844, _122846] : [-(contains_slb(_122844, _122840)), contains_slb(_122846, _122842), _122846 = _122844, _122842 = _122840], (92 ^ _120271) ^ [_123284, _123286, _123288, _123290] : [-(strictly_less_than(_123288, _123284)), strictly_less_than(_123290, _123286), _123290 = _123288, _123286 = _123284], (124 ^ _120271) ^ [_124317, _124319, _124321, _124323] : [-(less_than(_124321, _124317)), less_than(_124323, _124319), _124323 = _124321, _124319 = _124317], (106 ^ _120271) ^ [_123756, _123758, _123760, _123762, _123764, _123766] : [-(pair_in_list(_123764, _123760, _123756)), pair_in_list(_123766, _123762, _123758), _123766 = _123764, _123762 = _123760, _123758 = _123756], (138 ^ _120271) ^ [_124783, _124785, _124787, _124789] : [-(insert_cpq(_124789, _124785) = insert_cpq(_124787, _124783)), _124789 = _124787, _124785 = _124783], (148 ^ _120271) ^ [_125142, _125144, _125146, _125148] : [-(insert_pqp(_125148, _125144) = insert_pqp(_125146, _125142)), _125148 = _125146, _125144 = _125142], (158 ^ _120271) ^ [_125501, _125503, _125505, _125507] : [-(insert_slb(_125507, _125503) = insert_slb(_125505, _125501)), _125507 = _125505, _125503 = _125501], (168 ^ _120271) ^ [_125860, _125862, _125864, _125866] : [-(pair(_125866, _125862) = pair(_125864, _125860)), _125866 = _125864, _125862 = _125860], (178 ^ _120271) ^ [_126219, _126221, _126223, _126225] : [-(remove_pqp(_126225, _126221) = remove_pqp(_126223, _126219)), _126225 = _126223, _126221 = _126219], (188 ^ _120271) ^ [_126578, _126580, _126582, _126584] : [-(remove_slb(_126584, _126580) = remove_slb(_126582, _126578)), _126584 = _126582, _126580 = _126578], (198 ^ _120271) ^ [_126937, _126939, _126941, _126943] : [-(lookup_slb(_126943, _126939) = lookup_slb(_126941, _126937)), _126943 = _126941, _126939 = _126937], (208 ^ _120271) ^ [_127268, _127270] : [_127270 = _127268, -(removemin_cpq_eff(_127270) = removemin_cpq_eff(_127268))], (214 ^ _120271) ^ [_127514, _127516, _127518, _127520] : [-(remove_cpq(_127520, _127516) = remove_cpq(_127518, _127514)), _127520 = _127518, _127516 = _127514], (224 ^ _120271) ^ [_127845, _127847] : [_127847 = _127845, -(findmin_cpq_eff(_127847) = findmin_cpq_eff(_127845))], (230 ^ _120271) ^ [_128063, _128065] : [_128065 = _128063, -(removemin_cpq_res(_128065) = removemin_cpq_res(_128063))], (236 ^ _120271) ^ [_128281, _128283] : [_128283 = _128281, -(findmin_cpq_res(_128283) = findmin_cpq_res(_128281))], (242 ^ _120271) ^ [_128555, _128557, _128559, _128561, _128563, _128565] : [-(triple(_128565, _128561, _128557) = triple(_128563, _128559, _128555)), _128565 = _128563, _128561 = _128559, _128557 = _128555], (266 ^ _120271) ^ [_129354, _129356] : [_129356 = _129354, -(findmin_pqp_res(_129356) = findmin_pqp_res(_129354))], (256 ^ _120271) ^ [_129043, _129045, _129047, _129049] : [-(update_slb(_129049, _129045) = update_slb(_129047, _129043)), _129049 = _129047, _129045 = _129043], (272 ^ _120271) ^ [_129690, _129692, _129694] : [-(less_than(_129694, _129690)), less_than(_129694, _129692), less_than(_129692, _129690)], (282 ^ _120271) ^ [_129999, _130001] : [-(less_than(_130001, _129999)), -(less_than(_129999, _130001))], (288 ^ _120271) ^ [_130181] : [-(less_than(_130181, _130181))], (308 ^ _120271) ^ [_130810] : [-(less_than(bottom, _130810))], (290 ^ _120271) ^ [_130317, _130319] : [strictly_less_than(_130319, _130317), 293 ^ _120271 : [(294 ^ _120271) ^ [] : [-(less_than(_130319, _130317))], (296 ^ _120271) ^ [] : [less_than(_130317, _130319)]]], (298 ^ _120271) ^ [_130555, _130557] : [-(strictly_less_than(_130557, _130555)), less_than(_130557, _130555), -(less_than(_130555, _130557))], (310 ^ _120271) ^ [] : [isnonempty_slb(create_slb)], (312 ^ _120271) ^ [_130996, _130998, _131000] : [-(isnonempty_slb(insert_slb(_131000, pair(_130998, _130996))))], (314 ^ _120271) ^ [_131082] : [contains_slb(create_slb, _131082)], (326 ^ _120271) ^ [_131530, _131532, _131534, _131536] : [327 ^ _120271 : [(328 ^ _120271) ^ [] : [contains_slb(_131536, _131532)], (330 ^ _120271) ^ [] : [_131534 = _131532]], -(contains_slb(insert_slb(_131536, pair(_131534, _131530)), _131532))], (316 ^ _120271) ^ [_131246, _131248, _131250, _131252] : [contains_slb(insert_slb(_131252, pair(_131250, _131246)), _131248), -(contains_slb(_131252, _131248)), -(_131250 = _131248)], (334 ^ _120271) ^ [_131828, _131830] : [pair_in_list(create_slb, _131830, _131828)], (336 ^ _120271) ^ [_132009, _132011, _132013, _132015, _132017] : [pair_in_list(insert_slb(_132017, pair(_132015, _132011)), _132013, _132009), -(pair_in_list(_132017, _132013, _132009)), 343 ^ _120271 : [(344 ^ _120271) ^ [] : [-(_132015 = _132013)], (346 ^ _120271) ^ [] : [-(_132011 = _132009)]]], (348 ^ _120271) ^ [_132388, _132390, _132392, _132394, _132396] : [-(pair_in_list(insert_slb(_132396, pair(_132394, _132390)), _132392, _132388)), 349 ^ _120271 : [(350 ^ _120271) ^ [] : [pair_in_list(_132396, _132392, _132388)], (352 ^ _120271) ^ [] : [_132394 = _132392, _132390 = _132388]]], (360 ^ _120271) ^ [_132814, _132816, _132818] : [-(remove_slb(insert_slb(_132818, pair(_132816, _132814)), _132816) = _132818)], (362 ^ _120271) ^ [_132962, _132964, _132966, _132968] : [-(remove_slb(insert_slb(_132968, pair(_132966, _132962)), _132964) = insert_slb(remove_slb(_132968, _132964), pair(_132966, _132962))), -(_132966 = _132964), contains_slb(_132968, _132964)], (372 ^ _120271) ^ [_133319, _133321, _133323] : [-(lookup_slb(insert_slb(_133323, pair(_133321, _133319)), _133321) = _133319)], (374 ^ _120271) ^ [_133467, _133469, _133471, _133473] : [-(lookup_slb(insert_slb(_133473, pair(_133471, _133467)), _133469) = lookup_slb(_133473, _133469)), -(_133471 = _133469), contains_slb(_133473, _133469)], (384 ^ _120271) ^ [_133784] : [-(update_slb(create_slb, _133784) = create_slb)], (386 ^ _120271) ^ [_133922, _133924, _133926, _133928] : [strictly_less_than(_133922, _133924), -(update_slb(insert_slb(_133928, pair(_133926, _133922)), _133924) = insert_slb(update_slb(_133928, _133924), pair(_133926, _133924)))], (392 ^ _120271) ^ [_134188, _134190, _134192, _134194] : [less_than(_134190, _134188), -(update_slb(insert_slb(_134194, pair(_134192, _134188)), _134190) = insert_slb(update_slb(_134194, _134190), pair(_134192, _134188)))], (580 ^ _120271) ^ [_141393, _141395] : [contains_slb(_141395, _141393), -(pair_in_list(_141395, _141393, 583 ^ [_141393, _141395]))], (587 ^ _120271) ^ [_141691, _141693, _141695, _141697] : [-(pair_in_list(update_slb(_141697, _141691), _141695, _141691)), pair_in_list(_141697, _141695, _141693), strictly_less_than(_141693, _141691)], (597 ^ _120271) ^ [_142028, _142030, _142032, _142034] : [-(pair_in_list(update_slb(_142034, _142028), _142032, _142030)), pair_in_list(_142034, _142032, _142030), less_than(_142028, _142030)], (398 ^ _120271) ^ [_134465] : [-(succ_cpq(_134465, _134465))], (400 ^ _120271) ^ [_134586, _134588, _134590] : [succ_cpq(_134590, _134588), -(succ_cpq(_134590, insert_cpq(_134588, _134586)))], (406 ^ _120271) ^ [_134822, _134824, _134826] : [succ_cpq(_134826, _134824), -(succ_cpq(_134826, remove_cpq(_134824, _134822)))], (412 ^ _120271) ^ [_135044, _135046] : [succ_cpq(_135046, _135044), -(succ_cpq(_135046, findmin_cpq_eff(_135044)))], (418 ^ _120271) ^ [_135258, _135260] : [succ_cpq(_135260, _135258), -(succ_cpq(_135260, removemin_cpq_eff(_135258)))], (424 ^ _120271) ^ [_135457, _135459] : [-(check_cpq(triple(_135459, create_slb, _135457)))], (426 ^ _120271) ^ [_135611, _135613, _135615, _135617, _135619] : [less_than(_135611, _135613), 429 ^ _120271 : [(430 ^ _120271) ^ [] : [check_cpq(triple(_135619, insert_slb(_135617, pair(_135613, _135611)), _135615)), -(check_cpq(triple(_135619, _135617, _135615)))], (436 ^ _120271) ^ [] : [check_cpq(triple(_135619, _135617, _135615)), -(check_cpq(triple(_135619, insert_slb(_135617, pair(_135613, _135611)), _135615)))]]], (442 ^ _120271) ^ [_136197, _136199, _136201, _136203, _136205] : [strictly_less_than(_136199, _136197), 445 ^ _120271 : [(446 ^ _120271) ^ [] : [check_cpq(triple(_136205, insert_slb(_136203, pair(_136199, _136197)), _136201)), 449 ^ _120271 : [(450 ^ _120271) ^ [] : [-(false___)], (452 ^ _120271) ^ [] : [false___]]], (454 ^ _120271) ^ [] : [-(check_cpq(triple(_136205, insert_slb(_136203, pair(_136199, _136197)), _136201))), false___, -(false___)]]], (464 ^ _120271) ^ [_136944, _136946, _136948, _136950] : [contains_cpq(triple(_136950, _136948, _136946), _136944), -(contains_slb(_136948, _136944))], (470 ^ _120271) ^ [_137126, _137128, _137130, _137132] : [contains_slb(_137130, _137126), -(contains_cpq(triple(_137132, _137130, _137128), _137126))], (476 ^ _120271) ^ [_137387, _137389] : [ok(triple(_137389, _137387, bad)), 479 ^ _120271 : [(480 ^ _120271) ^ [] : [-(false___)], (482 ^ _120271) ^ [] : [false___]]], (484 ^ _120271) ^ [_137611, _137613] : [-(ok(triple(_137613, _137611, bad))), false___, -(false___)], (494 ^ _120271) ^ [_137918, _137920, _137922] : [-(ok(triple(_137922, _137920, _137918))), -(_137918 = bad)], (500 ^ _120271) ^ [_138156, _138158, _138160, _138162] : [-(insert_cpq(triple(_138162, _138160, _138158), _138156) = triple(insert_pqp(_138162, _138156), insert_slb(_138160, pair(_138156, bottom)), _138158))], (502 ^ _120271) ^ [_138317, _138319, _138321, _138323] : [-(contains_slb(_138321, _138317)), -(remove_cpq(triple(_138323, _138321, _138319), _138317) = triple(_138323, _138321, bad))], (508 ^ _120271) ^ [_138592, _138594, _138596, _138598] : [-(remove_cpq(triple(_138598, _138596, _138594), _138592) = triple(remove_pqp(_138598, _138592), remove_slb(_138596, _138592), _138594)), contains_slb(_138596, _138592), less_than(lookup_slb(_138596, _138592), _138592)], (518 ^ _120271) ^ [_138979, _138981, _138983, _138985] : [-(remove_cpq(triple(_138985, _138983, _138981), _138979) = triple(remove_pqp(_138985, _138979), remove_slb(_138983, _138979), bad)), contains_slb(_138983, _138979), strictly_less_than(_138979, lookup_slb(_138983, _138979))], (528 ^ _120271) ^ [_139323, _139325] : [-(findmin_cpq_eff(triple(_139325, create_slb, _139323)) = triple(_139325, create_slb, bad))], (530 ^ _120271) ^ [_139470, _139472, _139474, _139476] : [-(findmin_cpq_eff(triple(_139476, _139474, _139472)) = triple(_139476, update_slb(_139474, findmin_pqp_res(_139476)), bad)), -(_139474 = create_slb), -(contains_slb(_139474, findmin_pqp_res(_139476)))], (540 ^ _120271) ^ [_139857, _139859, _139861, _139863] : [-(findmin_cpq_eff(triple(_139863, _139861, _139859)) = triple(_139863, update_slb(_139861, findmin_pqp_res(_139863)), bad)), -(_139861 = create_slb), contains_slb(_139861, findmin_pqp_res(_139863)), strictly_less_than(findmin_pqp_res(_139863), lookup_slb(_139861, findmin_pqp_res(_139863)))], (568 ^ _120271) ^ [_140804, _140806] : [-(findmin_cpq_res(triple(_140806, create_slb, _140804)) = bottom)], (576 ^ _120271) ^ [_141159] : [-(removemin_cpq_eff(_141159) = remove_cpq(findmin_cpq_eff(_141159), findmin_cpq_res(_141159)))], (578 ^ _120271) ^ [_141226] : [-(removemin_cpq_res(_141226) = findmin_cpq_res(_141226))], (570 ^ _120271) ^ [_140947, _140949, _140951, _140953] : [-(_140951 = create_slb), -(findmin_cpq_res(triple(_140953, _140951, _140949)) = findmin_pqp_res(_140953))], (554 ^ _120271) ^ [_140352, _140354, _140356, _140358] : [-(findmin_cpq_eff(triple(_140358, _140356, _140354)) = triple(_140358, update_slb(_140356, findmin_pqp_res(_140358)), _140354)), -(_140356 = create_slb), contains_slb(_140356, findmin_pqp_res(_140358)), less_than(lookup_slb(_140356, findmin_pqp_res(_140358)), findmin_pqp_res(_140358))]], input).
% 0.65/1.39 ncf('1',plain,[pair_in_list(update_slb(607 ^ [], findmin_pqp_res(606 ^ [])), 609 ^ [], 583 ^ [609 ^ [], 607 ^ []]), less_than(findmin_pqp_res(606 ^ []), 583 ^ [609 ^ [], 607 ^ []])],start(617 ^ 0,bind([[_142968], [583 ^ [609 ^ [], 607 ^ []]]]))).
% 0.65/1.39 ncf('1.1',plain,[-(pair_in_list(update_slb(607 ^ [], findmin_pqp_res(606 ^ [])), 609 ^ [], 583 ^ [609 ^ [], 607 ^ []])), pair_in_list(607 ^ [], 609 ^ [], 583 ^ [609 ^ [], 607 ^ []]), less_than(findmin_pqp_res(606 ^ []), 583 ^ [609 ^ [], 607 ^ []])],extension(597 ^ 1,bind([[_142028, _142030, _142032, _142034], [findmin_pqp_res(606 ^ []), 583 ^ [609 ^ [], 607 ^ []], 609 ^ [], 607 ^ []]]))).
% 0.65/1.39 ncf('1.1.1',plain,[-(pair_in_list(607 ^ [], 609 ^ [], 583 ^ [609 ^ [], 607 ^ []])), pair_in_list(607 ^ [], 609 ^ [], 583 ^ [609 ^ [], 607 ^ []]), 607 ^ [] = 607 ^ [], 609 ^ [] = 609 ^ [], 583 ^ [609 ^ [], 607 ^ []] = 583 ^ [609 ^ [], 607 ^ []]],extension(106 ^ 2,bind([[_123756, _123758, _123760, _123762, _123764, _123766], [583 ^ [609 ^ [], 607 ^ []], 583 ^ [609 ^ [], 607 ^ []], 609 ^ [], 609 ^ [], 607 ^ [], 607 ^ []]]))).
% 0.65/1.39 ncf('1.1.1.1',plain,[-(pair_in_list(607 ^ [], 609 ^ [], 583 ^ [609 ^ [], 607 ^ []])), contains_slb(607 ^ [], 609 ^ [])],extension(580 ^ 3,bind([[_141393, _141395], [609 ^ [], 607 ^ []]]))).
% 0.65/1.39 ncf('1.1.1.1.1',plain,[-(contains_slb(607 ^ [], 609 ^ []))],extension(611 ^ 4)).
% 0.65/1.39 ncf('1.1.1.2',plain,[-(607 ^ [] = 607 ^ [])],extension(2 ^ 3,bind([[_120415], [607 ^ []]]))).
% 0.65/1.39 ncf('1.1.1.3',plain,[-(609 ^ [] = 609 ^ [])],extension(2 ^ 3,bind([[_120415], [609 ^ []]]))).
% 0.65/1.39 ncf('1.1.1.4',plain,[-(583 ^ [609 ^ [], 607 ^ []] = 583 ^ [609 ^ [], 607 ^ []])],extension(2 ^ 3,bind([[_120415], [583 ^ [609 ^ [], 607 ^ []]]]))).
% 0.65/1.39 ncf('1.1.2',plain,[-(less_than(findmin_pqp_res(606 ^ []), 583 ^ [609 ^ [], 607 ^ []])), -(strictly_less_than(583 ^ [609 ^ [], 607 ^ []], findmin_pqp_res(606 ^ []))), less_than(583 ^ [609 ^ [], 607 ^ []], findmin_pqp_res(606 ^ []))],extension(298 ^ 2,bind([[_130555, _130557], [findmin_pqp_res(606 ^ []), 583 ^ [609 ^ [], 607 ^ []]]]))).
% 0.65/1.39 ncf('1.1.2.1',plain,[strictly_less_than(583 ^ [609 ^ [], 607 ^ []], findmin_pqp_res(606 ^ [])), -(pair_in_list(update_slb(607 ^ [], findmin_pqp_res(606 ^ [])), 609 ^ [], findmin_pqp_res(606 ^ []))), pair_in_list(607 ^ [], 609 ^ [], 583 ^ [609 ^ [], 607 ^ []])],extension(587 ^ 3,bind([[_141691, _141693, _141695, _141697], [findmin_pqp_res(606 ^ []), 583 ^ [609 ^ [], 607 ^ []], 609 ^ [], 607 ^ []]]))).
% 0.65/1.39 ncf('1.1.2.1.1',plain,[pair_in_list(update_slb(607 ^ [], findmin_pqp_res(606 ^ [])), 609 ^ [], findmin_pqp_res(606 ^ []))],extension(615 ^ 4)).
% 0.65/1.39 ncf('1.1.2.1.2',plain,[-(pair_in_list(607 ^ [], 609 ^ [], 583 ^ [609 ^ [], 607 ^ []]))],lemmata('[1].x')).
% 0.65/1.39 ncf('1.1.2.2',plain,[-(less_than(583 ^ [609 ^ [], 607 ^ []], findmin_pqp_res(606 ^ []))), -(less_than(findmin_pqp_res(606 ^ []), 583 ^ [609 ^ [], 607 ^ []]))],extension(282 ^ 3,bind([[_129999, _130001], [findmin_pqp_res(606 ^ []), 583 ^ [609 ^ [], 607 ^ []]]]))).
% 0.65/1.39 ncf('1.1.2.2.1',plain,[less_than(findmin_pqp_res(606 ^ []), 583 ^ [609 ^ [], 607 ^ []])],reduction('1.1')).
% 0.65/1.39 ncf('1.2',plain,[-(less_than(findmin_pqp_res(606 ^ []), 583 ^ [609 ^ [], 607 ^ []])), -(strictly_less_than(583 ^ [609 ^ [], 607 ^ []], findmin_pqp_res(606 ^ []))), less_than(583 ^ [609 ^ [], 607 ^ []], findmin_pqp_res(606 ^ []))],extension(298 ^ 1,bind([[_130555, _130557], [findmin_pqp_res(606 ^ []), 583 ^ [609 ^ [], 607 ^ []]]]))).
% 0.65/1.39 ncf('1.2.1',plain,[strictly_less_than(583 ^ [609 ^ [], 607 ^ []], findmin_pqp_res(606 ^ [])), -(pair_in_list(update_slb(607 ^ [], findmin_pqp_res(606 ^ [])), 609 ^ [], findmin_pqp_res(606 ^ []))), pair_in_list(607 ^ [], 609 ^ [], 583 ^ [609 ^ [], 607 ^ []])],extension(587 ^ 2,bind([[_141691, _141693, _141695, _141697], [findmin_pqp_res(606 ^ []), 583 ^ [609 ^ [], 607 ^ []], 609 ^ [], 607 ^ []]]))).
% 0.65/1.39 ncf('1.2.1.1',plain,[pair_in_list(update_slb(607 ^ [], findmin_pqp_res(606 ^ [])), 609 ^ [], findmin_pqp_res(606 ^ []))],extension(615 ^ 3)).
% 0.65/1.39 ncf('1.2.1.2',plain,[-(pair_in_list(607 ^ [], 609 ^ [], 583 ^ [609 ^ [], 607 ^ []])), contains_slb(607 ^ [], 609 ^ [])],extension(580 ^ 3,bind([[_141393, _141395], [609 ^ [], 607 ^ []]]))).
% 0.65/1.39 ncf('1.2.1.2.1',plain,[-(contains_slb(607 ^ [], 609 ^ []))],extension(611 ^ 4)).
% 0.65/1.39 ncf('1.2.2',plain,[-(less_than(583 ^ [609 ^ [], 607 ^ []], findmin_pqp_res(606 ^ []))), -(less_than(findmin_pqp_res(606 ^ []), 583 ^ [609 ^ [], 607 ^ []]))],extension(282 ^ 2,bind([[_129999, _130001], [findmin_pqp_res(606 ^ []), 583 ^ [609 ^ [], 607 ^ []]]]))).
% 0.65/1.39 ncf('1.2.2.1',plain,[less_than(findmin_pqp_res(606 ^ []), 583 ^ [609 ^ [], 607 ^ []])],reduction('1')).
% 0.65/1.39 %-----------------------------------------------------
% 0.65/1.39 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------