%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV367+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n025.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:30 EDT 2023
% Result : Theorem 0.33s 1.37s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : SWV367+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.11/0.33 % Computer : n025.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 : Fri May 19 02:43:03 EDT 2023
% 0.11/0.33 % CPUTime :
% 0.33/1.37
% 0.33/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 ncf(matrix, plain, [(985 ^ _164490) ^ [] : [-(contains_pq(i(triple(981 ^ [], create_slb, 982 ^ [])), 983 ^ []))], (987 ^ _164490) ^ [] : [i(remove_cpq(triple(981 ^ [], create_slb, 982 ^ []), 983 ^ [])) = remove_pq(i(triple(981 ^ [], create_slb, 982 ^ [])), 983 ^ [])], (262 ^ _164490) ^ [_172910, _172912, _172914, _172916] : [-(findmin_pq_eff(_172916, _172912) = findmin_pq_eff(_172914, _172910)), _172916 = _172914, _172912 = _172910], (272 ^ _164490) ^ [_173269, _173271, _173273, _173275] : [-(findmin_pq_res(_173275, _173271) = findmin_pq_res(_173273, _173269)), _173275 = _173273, _173271 = _173269], (282 ^ _164490) ^ [_173628, _173630, _173632, _173634] : [-(removemin_pq_eff(_173634, _173630) = removemin_pq_eff(_173632, _173628)), _173634 = _173632, _173630 = _173628], (292 ^ _164490) ^ [_173987, _173989, _173991, _173993] : [-(removemin_pq_res(_173993, _173989) = removemin_pq_res(_173991, _173987)), _173993 = _173991, _173989 = _173987], (302 ^ _164490) ^ [_174346, _174348, _174350, _174352] : [-(insert_cpq(_174352, _174348) = insert_cpq(_174350, _174346)), _174352 = _174350, _174348 = _174346], (312 ^ _164490) ^ [_174705, _174707, _174709, _174711] : [-(insert_pqp(_174711, _174707) = insert_pqp(_174709, _174705)), _174711 = _174709, _174707 = _174705], (322 ^ _164490) ^ [_175064, _175066, _175068, _175070] : [-(remove_pqp(_175070, _175066) = remove_pqp(_175068, _175064)), _175070 = _175068, _175066 = _175064], (332 ^ _164490) ^ [_175423, _175425, _175427, _175429] : [-(remove_slb(_175429, _175425) = remove_slb(_175427, _175423)), _175429 = _175427, _175425 = _175423], (342 ^ _164490) ^ [_175782, _175784, _175786, _175788] : [-(lookup_slb(_175788, _175784) = lookup_slb(_175786, _175782)), _175788 = _175786, _175784 = _175782], (352 ^ _164490) ^ [_176141, _176143, _176145, _176147] : [-(update_slb(_176147, _176143) = update_slb(_176145, _176141)), _176147 = _176145, _176143 = _176141], (362 ^ _164490) ^ [_176472, _176474] : [_176474 = _176472, -(findmin_pqp_res(_176474) = findmin_pqp_res(_176472))], (368 ^ _164490) ^ [_176690, _176692] : [_176692 = _176690, -(removemin_cpq_eff(_176692) = removemin_cpq_eff(_176690))], (374 ^ _164490) ^ [_176908, _176910] : [_176910 = _176908, -(findmin_cpq_eff(_176910) = findmin_cpq_eff(_176908))], (380 ^ _164490) ^ [_177126, _177128] : [_177128 = _177126, -(removemin_cpq_res(_177128) = removemin_cpq_res(_177126))], (386 ^ _164490) ^ [_177344, _177346] : [_177346 = _177344, -(findmin_cpq_res(_177346) = findmin_cpq_res(_177344))], (392 ^ _164490) ^ [_177590, _177592, _177594, _177596] : [-(insert_slb(_177596, _177592) = insert_slb(_177594, _177590)), _177596 = _177594, _177592 = _177590], (402 ^ _164490) ^ [_177949, _177951, _177953, _177955] : [-(pair(_177955, _177951) = pair(_177953, _177949)), _177955 = _177953, _177951 = _177949], (412 ^ _164490) ^ [_178308, _178310, _178312, _178314] : [-(insert_pq(_178314, _178310) = insert_pq(_178312, _178308)), _178314 = _178312, _178310 = _178308], (422 ^ _164490) ^ [_178667, _178669, _178671, _178673] : [-(remove_cpq(_178673, _178669) = remove_cpq(_178671, _178667)), _178673 = _178671, _178669 = _178667], (432 ^ _164490) ^ [_179026, _179028, _179030, _179032] : [-(remove_pq(_179032, _179028) = remove_pq(_179030, _179026)), _179032 = _179030, _179028 = _179026], (442 ^ _164490) ^ [_179357, _179359] : [_179359 = _179357, -(i(_179359) = i(_179357))], (448 ^ _164490) ^ [_179611, _179613, _179615, _179617, _179619, _179621] : [-(triple(_179621, _179617, _179613) = triple(_179619, _179615, _179611)), _179621 = _179619, _179617 = _179615, _179613 = _179611], (2 ^ _164490) ^ [_164634] : [-(_164634 = _164634)], (4 ^ _164490) ^ [_164741, _164743] : [_164743 = _164741, -(_164741 = _164743)], (10 ^ _164490) ^ [_164945, _164947, _164949] : [-(_164949 = _164945), _164949 = _164947, _164947 = _164945], (20 ^ _164490) ^ [_165258, _165260] : [-(isnonempty_pq(_165258)), _165260 = _165258, isnonempty_pq(_165260)], (30 ^ _164490) ^ [_165553, _165555] : [-(isnonempty_slb(_165553)), _165555 = _165553, isnonempty_slb(_165555)], (40 ^ _164490) ^ [_165904, _165906, _165908, _165910, _165912, _165914] : [-(pair_in_list(_165912, _165908, _165904)), pair_in_list(_165914, _165910, _165906), _165914 = _165912, _165910 = _165908, _165906 = _165904], (58 ^ _164490) ^ [_166485, _166487, _166489, _166491] : [-(contains_cpq(_166489, _166485)), contains_cpq(_166491, _166487), _166491 = _166489, _166487 = _166485], (72 ^ _164490) ^ [_166929, _166931, _166933, _166935] : [-(strictly_less_than(_166933, _166929)), strictly_less_than(_166935, _166931), _166935 = _166933, _166931 = _166929], (86 ^ _164490) ^ [_167373, _167375, _167377, _167379] : [-(contains_slb(_167377, _167373)), contains_slb(_167379, _167375), _167379 = _167377, _167375 = _167373], (100 ^ _164490) ^ [_167817, _167819, _167821, _167823] : [-(less_than(_167821, _167817)), less_than(_167823, _167819), _167823 = _167821, _167819 = _167817], (114 ^ _164490) ^ [_168261, _168263, _168265, _168267] : [-(pi_remove(_168265, _168261)), pi_remove(_168267, _168263), _168267 = _168265, _168263 = _168261], (128 ^ _164490) ^ [_168705, _168707, _168709, _168711] : [-(pi_sharp_remove(_168709, _168705)), pi_sharp_remove(_168711, _168707), _168711 = _168709, _168707 = _168705], (142 ^ _164490) ^ [_169121, _169123] : [-(pi_find_min(_169121)), _169123 = _169121, pi_find_min(_169123)], (152 ^ _164490) ^ [_169444, _169446, _169448, _169450] : [-(pi_sharp_removemin(_169448, _169444)), pi_sharp_removemin(_169450, _169446), _169450 = _169448, _169446 = _169444], (166 ^ _164490) ^ [_169888, _169890, _169892, _169894] : [-(issmallestelement_pq(_169892, _169888)), issmallestelement_pq(_169894, _169890), _169894 = _169892, _169890 = _169888], (180 ^ _164490) ^ [_170304, _170306] : [-(pi_removemin(_170304)), _170306 = _170304, pi_removemin(_170306)], (190 ^ _164490) ^ [_170627, _170629, _170631, _170633] : [-(pi_sharp_find_min(_170631, _170627)), pi_sharp_find_min(_170633, _170629), _170633 = _170631, _170629 = _170627], (204 ^ _164490) ^ [_171043, _171045] : [-(phi(_171043)), _171045 = _171043, phi(_171045)], (214 ^ _164490) ^ [_171366, _171368, _171370, _171372] : [-(succ_cpq(_171370, _171366)), succ_cpq(_171372, _171368), _171372 = _171370, _171368 = _171366], (228 ^ _164490) ^ [_171782, _171784] : [-(ok(_171782)), _171784 = _171782, ok(_171784)], (238 ^ _164490) ^ [_172077, _172079] : [-(check_cpq(_172077)), _172079 = _172077, check_cpq(_172079)], (248 ^ _164490) ^ [_172380, _172382, _172384, _172386] : [-(contains_pq(_172384, _172380)), contains_pq(_172386, _172382), _172386 = _172384, _172382 = _172380], (462 ^ _164490) ^ [_180226, _180228, _180230] : [-(less_than(_180230, _180226)), less_than(_180230, _180228), less_than(_180228, _180226)], (472 ^ _164490) ^ [_180535, _180537] : [-(less_than(_180537, _180535)), -(less_than(_180535, _180537))], (478 ^ _164490) ^ [_180717] : [-(less_than(_180717, _180717))], (498 ^ _164490) ^ [_181346] : [-(less_than(bottom, _181346))], (480 ^ _164490) ^ [_180853, _180855] : [strictly_less_than(_180855, _180853), 483 ^ _164490 : [(484 ^ _164490) ^ [] : [-(less_than(_180855, _180853))], (486 ^ _164490) ^ [] : [less_than(_180853, _180855)]]], (488 ^ _164490) ^ [_181091, _181093] : [-(strictly_less_than(_181093, _181091)), less_than(_181093, _181091), -(less_than(_181091, _181093))], (500 ^ _164490) ^ [] : [isnonempty_pq(create_pq)], (502 ^ _164490) ^ [_181518, _181520] : [-(isnonempty_pq(insert_pq(_181520, _181518)))], (504 ^ _164490) ^ [_181599] : [contains_pq(create_pq, _181599)], (516 ^ _164490) ^ [_182017, _182019, _182021] : [517 ^ _164490 : [(518 ^ _164490) ^ [] : [contains_pq(_182021, _182017)], (520 ^ _164490) ^ [] : [_182019 = _182017]], -(contains_pq(insert_pq(_182021, _182019), _182017))], (506 ^ _164490) ^ [_181749, _181751, _181753] : [contains_pq(insert_pq(_181753, _181751), _181749), -(contains_pq(_181753, _181749)), -(_181751 = _181749)], (534 ^ _164490) ^ [_182660, _182662] : [536 ^ _164490 : [(537 ^ _164490) ^ [] : [-(contains_pq(_182662, 535 ^ [_182660, _182662]))], (539 ^ _164490) ^ [] : [less_than(_182660, 535 ^ [_182660, _182662])]], -(issmallestelement_pq(_182662, _182660))], (524 ^ _164490) ^ [_182346, _182348] : [issmallestelement_pq(_182348, _182346), 527 ^ _164490 : [(528 ^ _164490) ^ [_182483] : [contains_pq(_182348, _182483), -(less_than(_182346, _182483))]]], (543 ^ _164490) ^ [_183002, _183004] : [-(remove_pq(insert_pq(_183004, _183002), _183002) = _183004)], (545 ^ _164490) ^ [_183131, _183133, _183135] : [-(remove_pq(insert_pq(_183135, _183133), _183131) = insert_pq(remove_pq(_183135, _183131), _183133)), contains_pq(_183135, _183131), -(_183133 = _183131)], (555 ^ _164490) ^ [_183467, _183469] : [-(findmin_pq_eff(_183469, _183467) = _183469), contains_pq(_183469, _183467), issmallestelement_pq(_183469, _183467)], (565 ^ _164490) ^ [_183772, _183774] : [-(findmin_pq_res(_183774, _183772) = _183772), contains_pq(_183774, _183772), issmallestelement_pq(_183774, _183772)], (575 ^ _164490) ^ [_184077, _184079] : [-(removemin_pq_eff(_184079, _184077) = remove_pq(_184079, _184077)), contains_pq(_184079, _184077), issmallestelement_pq(_184079, _184077)], (595 ^ _164490) ^ [_184672, _184674, _184676] : [-(insert_pq(insert_pq(_184676, _184674), _184672) = insert_pq(insert_pq(_184676, _184672), _184674))], (585 ^ _164490) ^ [_184388, _184390] : [-(removemin_pq_res(_184390, _184388) = _184388), contains_pq(_184390, _184388), issmallestelement_pq(_184390, _184388)], (597 ^ _164490) ^ [] : [isnonempty_slb(create_slb)], (599 ^ _164490) ^ [_184892, _184894, _184896] : [-(isnonempty_slb(insert_slb(_184896, pair(_184894, _184892))))], (601 ^ _164490) ^ [_184978] : [contains_slb(create_slb, _184978)], (613 ^ _164490) ^ [_185426, _185428, _185430, _185432] : [614 ^ _164490 : [(615 ^ _164490) ^ [] : [contains_slb(_185432, _185428)], (617 ^ _164490) ^ [] : [_185430 = _185428]], -(contains_slb(insert_slb(_185432, pair(_185430, _185426)), _185428))], (603 ^ _164490) ^ [_185142, _185144, _185146, _185148] : [contains_slb(insert_slb(_185148, pair(_185146, _185142)), _185144), -(contains_slb(_185148, _185144)), -(_185146 = _185144)], (621 ^ _164490) ^ [_185724, _185726] : [pair_in_list(create_slb, _185726, _185724)], (623 ^ _164490) ^ [_185905, _185907, _185909, _185911, _185913] : [pair_in_list(insert_slb(_185913, pair(_185911, _185907)), _185909, _185905), -(pair_in_list(_185913, _185909, _185905)), 630 ^ _164490 : [(631 ^ _164490) ^ [] : [-(_185911 = _185909)], (633 ^ _164490) ^ [] : [-(_185907 = _185905)]]], (635 ^ _164490) ^ [_186284, _186286, _186288, _186290, _186292] : [-(pair_in_list(insert_slb(_186292, pair(_186290, _186286)), _186288, _186284)), 636 ^ _164490 : [(637 ^ _164490) ^ [] : [pair_in_list(_186292, _186288, _186284)], (639 ^ _164490) ^ [] : [_186290 = _186288, _186286 = _186284]]], (647 ^ _164490) ^ [_186710, _186712, _186714] : [-(remove_slb(insert_slb(_186714, pair(_186712, _186710)), _186712) = _186714)], (649 ^ _164490) ^ [_186858, _186860, _186862, _186864] : [-(remove_slb(insert_slb(_186864, pair(_186862, _186858)), _186860) = insert_slb(remove_slb(_186864, _186860), pair(_186862, _186858))), -(_186862 = _186860), contains_slb(_186864, _186860)], (659 ^ _164490) ^ [_187215, _187217, _187219] : [-(lookup_slb(insert_slb(_187219, pair(_187217, _187215)), _187217) = _187215)], (661 ^ _164490) ^ [_187363, _187365, _187367, _187369] : [-(lookup_slb(insert_slb(_187369, pair(_187367, _187363)), _187365) = lookup_slb(_187369, _187365)), -(_187367 = _187365), contains_slb(_187369, _187365)], (671 ^ _164490) ^ [_187680] : [-(update_slb(create_slb, _187680) = create_slb)], (673 ^ _164490) ^ [_187818, _187820, _187822, _187824] : [strictly_less_than(_187818, _187820), -(update_slb(insert_slb(_187824, pair(_187822, _187818)), _187820) = insert_slb(update_slb(_187824, _187820), pair(_187822, _187820)))], (679 ^ _164490) ^ [_188084, _188086, _188088, _188090] : [less_than(_188086, _188084), -(update_slb(insert_slb(_188090, pair(_188088, _188084)), _188086) = insert_slb(update_slb(_188090, _188086), pair(_188088, _188084)))], (867 ^ _164490) ^ [_195274, _195276] : [-(i(triple(_195276, create_slb, _195274)) = create_pq)], (869 ^ _164490) ^ [_195416, _195418, _195420, _195422, _195424] : [-(i(triple(_195424, insert_slb(_195422, pair(_195418, _195416)), _195420)) = insert_pq(i(triple(_195424, _195422, _195420)), _195418))], (871 ^ _164490) ^ [_195581, _195583] : [pi_sharp_remove(_195583, _195581), -(contains_pq(_195583, _195581))], (877 ^ _164490) ^ [_195743, _195745] : [contains_pq(_195745, _195743), -(pi_sharp_remove(_195745, _195743))], (883 ^ _164490) ^ [_195984, _195986] : [pi_remove(_195986, _195984), -(pi_sharp_remove(i(_195986), _195984))], (889 ^ _164490) ^ [_196150, _196152] : [pi_sharp_remove(i(_196152), _196150), -(pi_remove(_196152, _196150))], (895 ^ _164490) ^ [_196395, _196397] : [pi_sharp_find_min(_196397, _196395), 898 ^ _164490 : [(899 ^ _164490) ^ [] : [-(contains_pq(_196397, _196395))], (901 ^ _164490) ^ [] : [-(issmallestelement_pq(_196397, _196395))]]], (903 ^ _164490) ^ [_196632, _196634] : [-(pi_sharp_find_min(_196634, _196632)), contains_pq(_196634, _196632), issmallestelement_pq(_196634, _196632)], (913 ^ _164490) ^ [_196948] : [pi_find_min(_196948), -(pi_sharp_find_min(i(_196948), 916 ^ [_196948]))], (920 ^ _164490) ^ [_197159] : [921 ^ _164490 : [(922 ^ _164490) ^ [_197228] : [pi_sharp_find_min(i(_197159), _197228)]], -(pi_find_min(_197159))], (926 ^ _164490) ^ [_197418, _197420] : [pi_sharp_removemin(_197420, _197418), 929 ^ _164490 : [(930 ^ _164490) ^ [] : [-(contains_pq(_197420, _197418))], (932 ^ _164490) ^ [] : [-(issmallestelement_pq(_197420, _197418))]]], (934 ^ _164490) ^ [_197655, _197657] : [-(pi_sharp_removemin(_197657, _197655)), contains_pq(_197657, _197655), issmallestelement_pq(_197657, _197655)], (944 ^ _164490) ^ [_197971] : [pi_removemin(_197971), -(pi_sharp_find_min(i(_197971), 947 ^ [_197971]))], (951 ^ _164490) ^ [_198182] : [952 ^ _164490 : [(953 ^ _164490) ^ [_198251] : [pi_sharp_find_min(i(_198182), _198251)]], -(pi_removemin(_198182))], (957 ^ _164490) ^ [_198407] : [phi(_198407), 961 ^ _164490 : [(962 ^ _164490) ^ [] : [-(succ_cpq(_198407, 960 ^ [_198407]))], (964 ^ _164490) ^ [] : [-(ok(960 ^ [_198407]))], (966 ^ _164490) ^ [] : [-(check_cpq(960 ^ [_198407]))]]], (968 ^ _164490) ^ [_198773] : [-(phi(_198773)), 969 ^ _164490 : [(970 ^ _164490) ^ [_198866] : [succ_cpq(_198773, _198866), ok(_198866), check_cpq(_198866)]]], (685 ^ _164490) ^ [_188361] : [-(succ_cpq(_188361, _188361))], (687 ^ _164490) ^ [_188482, _188484, _188486] : [succ_cpq(_188486, _188484), -(succ_cpq(_188486, insert_cpq(_188484, _188482)))], (693 ^ _164490) ^ [_188718, _188720, _188722] : [succ_cpq(_188722, _188720), -(succ_cpq(_188722, remove_cpq(_188720, _188718)))], (699 ^ _164490) ^ [_188940, _188942] : [succ_cpq(_188942, _188940), -(succ_cpq(_188942, findmin_cpq_eff(_188940)))], (705 ^ _164490) ^ [_189154, _189156] : [succ_cpq(_189156, _189154), -(succ_cpq(_189156, removemin_cpq_eff(_189154)))], (711 ^ _164490) ^ [_189353, _189355] : [-(check_cpq(triple(_189355, create_slb, _189353)))], (713 ^ _164490) ^ [_189507, _189509, _189511, _189513, _189515] : [less_than(_189507, _189509), 716 ^ _164490 : [(717 ^ _164490) ^ [] : [check_cpq(triple(_189515, insert_slb(_189513, pair(_189509, _189507)), _189511)), -(check_cpq(triple(_189515, _189513, _189511)))], (723 ^ _164490) ^ [] : [check_cpq(triple(_189515, _189513, _189511)), -(check_cpq(triple(_189515, insert_slb(_189513, pair(_189509, _189507)), _189511)))]]], (729 ^ _164490) ^ [_190093, _190095, _190097, _190099, _190101] : [strictly_less_than(_190095, _190093), 732 ^ _164490 : [(733 ^ _164490) ^ [] : [check_cpq(triple(_190101, insert_slb(_190099, pair(_190095, _190093)), _190097)), 736 ^ _164490 : [(737 ^ _164490) ^ [] : [-(false___)], (739 ^ _164490) ^ [] : [false___]]], (741 ^ _164490) ^ [] : [-(check_cpq(triple(_190101, insert_slb(_190099, pair(_190095, _190093)), _190097))), false___, -(false___)]]], (751 ^ _164490) ^ [_190840, _190842, _190844, _190846] : [contains_cpq(triple(_190846, _190844, _190842), _190840), -(contains_slb(_190844, _190840))], (757 ^ _164490) ^ [_191022, _191024, _191026, _191028] : [contains_slb(_191026, _191022), -(contains_cpq(triple(_191028, _191026, _191024), _191022))], (763 ^ _164490) ^ [_191283, _191285] : [ok(triple(_191285, _191283, bad)), 766 ^ _164490 : [(767 ^ _164490) ^ [] : [-(false___)], (769 ^ _164490) ^ [] : [false___]]], (771 ^ _164490) ^ [_191507, _191509] : [-(ok(triple(_191509, _191507, bad))), false___, -(false___)], (781 ^ _164490) ^ [_191814, _191816, _191818] : [-(ok(triple(_191818, _191816, _191814))), -(_191814 = bad)], (787 ^ _164490) ^ [_192052, _192054, _192056, _192058] : [-(insert_cpq(triple(_192058, _192056, _192054), _192052) = triple(insert_pqp(_192058, _192052), insert_slb(_192056, pair(_192052, bottom)), _192054))], (789 ^ _164490) ^ [_192213, _192215, _192217, _192219] : [-(contains_slb(_192217, _192213)), -(remove_cpq(triple(_192219, _192217, _192215), _192213) = triple(_192219, _192217, bad))], (795 ^ _164490) ^ [_192488, _192490, _192492, _192494] : [-(remove_cpq(triple(_192494, _192492, _192490), _192488) = triple(remove_pqp(_192494, _192488), remove_slb(_192492, _192488), _192490)), contains_slb(_192492, _192488), less_than(lookup_slb(_192492, _192488), _192488)], (805 ^ _164490) ^ [_192875, _192877, _192879, _192881] : [-(remove_cpq(triple(_192881, _192879, _192877), _192875) = triple(remove_pqp(_192881, _192875), remove_slb(_192879, _192875), bad)), contains_slb(_192879, _192875), strictly_less_than(_192875, lookup_slb(_192879, _192875))], (815 ^ _164490) ^ [_193219, _193221] : [-(findmin_cpq_eff(triple(_193221, create_slb, _193219)) = triple(_193221, create_slb, bad))], (817 ^ _164490) ^ [_193366, _193368, _193370, _193372] : [-(findmin_cpq_eff(triple(_193372, _193370, _193368)) = triple(_193372, update_slb(_193370, findmin_pqp_res(_193372)), bad)), -(_193370 = create_slb), -(contains_slb(_193370, findmin_pqp_res(_193372)))], (827 ^ _164490) ^ [_193753, _193755, _193757, _193759] : [-(findmin_cpq_eff(triple(_193759, _193757, _193755)) = triple(_193759, update_slb(_193757, findmin_pqp_res(_193759)), bad)), -(_193757 = create_slb), contains_slb(_193757, findmin_pqp_res(_193759)), strictly_less_than(findmin_pqp_res(_193759), lookup_slb(_193757, findmin_pqp_res(_193759)))], (855 ^ _164490) ^ [_194700, _194702] : [-(findmin_cpq_res(triple(_194702, create_slb, _194700)) = bottom)], (863 ^ _164490) ^ [_195055] : [-(removemin_cpq_eff(_195055) = remove_cpq(findmin_cpq_eff(_195055), findmin_cpq_res(_195055)))], (865 ^ _164490) ^ [_195122] : [-(removemin_cpq_res(_195122) = findmin_cpq_res(_195122))], (857 ^ _164490) ^ [_194843, _194845, _194847, _194849] : [-(_194847 = create_slb), -(findmin_cpq_res(triple(_194849, _194847, _194845)) = findmin_pqp_res(_194849))], (841 ^ _164490) ^ [_194248, _194250, _194252, _194254] : [-(findmin_cpq_eff(triple(_194254, _194252, _194250)) = triple(_194254, update_slb(_194252, findmin_pqp_res(_194254)), _194250)), -(_194252 = create_slb), contains_slb(_194252, findmin_pqp_res(_194254)), less_than(lookup_slb(_194252, findmin_pqp_res(_194254)), findmin_pqp_res(_194254))]], input).
% 0.33/1.37 ncf('1',plain,[contains_pq(create_pq, 983 ^ [])],start(504 ^ 0,bind([[_181599], [983 ^ []]]))).
% 0.33/1.37 ncf('1.1',plain,[-(contains_pq(create_pq, 983 ^ [])), contains_pq(i(triple(981 ^ [], create_slb, 982 ^ [])), 983 ^ []), i(triple(981 ^ [], create_slb, 982 ^ [])) = create_pq, 983 ^ [] = 983 ^ []],extension(248 ^ 1,bind([[_172380, _172382, _172384, _172386], [983 ^ [], 983 ^ [], create_pq, i(triple(981 ^ [], create_slb, 982 ^ []))]]))).
% 0.33/1.37 ncf('1.1.1',plain,[-(contains_pq(i(triple(981 ^ [], create_slb, 982 ^ [])), 983 ^ []))],extension(985 ^ 2)).
% 0.33/1.37 ncf('1.1.2',plain,[-(i(triple(981 ^ [], create_slb, 982 ^ [])) = create_pq)],extension(867 ^ 2,bind([[_195274, _195276], [982 ^ [], 981 ^ []]]))).
% 0.33/1.37 ncf('1.1.3',plain,[-(983 ^ [] = 983 ^ [])],extension(2 ^ 2,bind([[_164634], [983 ^ []]]))).
% 0.33/1.37 %-----------------------------------------------------
% 0.33/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------