%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWV399+1 : TPTP v8.1.2. Released v3.3.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 12:20:34 EDT 2023
% Result : Theorem 1.10s 1.36s
% Output : Proof 1.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWV399+1 : TPTP v8.1.2. Released v3.3.0.
% 0.00/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 : Fri May 19 02:06:31 EDT 2023
% 0.12/0.33 % CPUTime :
% 1.10/1.36
% 1.10/1.36 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 1.10/1.36 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.10/1.36 %-----------------------------------------------------
% 1.10/1.36 ncf(matrix, plain, [(289 ^ _58588) ^ [] : [-(pair_in_list(285 ^ [], 286 ^ [], 287 ^ []))], (291 ^ _58588) ^ [] : [-(strictly_less_than(286 ^ [], 287 ^ []))], (294 ^ _58588) ^ [_69310, _69312] : [pair_in_list(update_slb(285 ^ [], 292 ^ []), _69312, _69310), strictly_less_than(_69312, _69310)], (140 ^ _58588) ^ [_63413, _63415, _63417] : [-(less_than(_63417, _63413)), less_than(_63417, _63415), less_than(_63415, _63413)], (150 ^ _58588) ^ [_63722, _63724] : [-(less_than(_63724, _63722)), -(less_than(_63722, _63724))], (156 ^ _58588) ^ [_63904] : [-(less_than(_63904, _63904))], (176 ^ _58588) ^ [_64533] : [-(less_than(bottom, _64533))], (158 ^ _58588) ^ [_64040, _64042] : [strictly_less_than(_64042, _64040), 161 ^ _58588 : [(162 ^ _58588) ^ [] : [-(less_than(_64042, _64040))], (164 ^ _58588) ^ [] : [less_than(_64040, _64042)]]], (166 ^ _58588) ^ [_64278, _64280] : [-(strictly_less_than(_64280, _64278)), less_than(_64280, _64278), -(less_than(_64278, _64280))], (266 ^ _58588) ^ [_68225, _68227, _68229, _68231] : [-(pair_in_list(update_slb(_68231, _68225), _68229, _68227)), pair_in_list(_68231, _68229, _68227), less_than(_68225, _68227)], (276 ^ _58588) ^ [_68562, _68564, _68566, _68568] : [-(pair_in_list(update_slb(_68568, _68562), _68566, _68562)), pair_in_list(_68568, _68566, _68564), strictly_less_than(_68564, _68562)], (178 ^ _58588) ^ [] : [isnonempty_slb(create_slb)], (180 ^ _58588) ^ [_64719, _64721, _64723] : [-(isnonempty_slb(insert_slb(_64723, pair(_64721, _64719))))], (182 ^ _58588) ^ [_64805] : [contains_slb(create_slb, _64805)], (194 ^ _58588) ^ [_65253, _65255, _65257, _65259] : [195 ^ _58588 : [(196 ^ _58588) ^ [] : [contains_slb(_65259, _65255)], (198 ^ _58588) ^ [] : [_65257 = _65255]], -(contains_slb(insert_slb(_65259, pair(_65257, _65253)), _65255))], (184 ^ _58588) ^ [_64969, _64971, _64973, _64975] : [contains_slb(insert_slb(_64975, pair(_64973, _64969)), _64971), -(contains_slb(_64975, _64971)), -(_64973 = _64971)], (202 ^ _58588) ^ [_65551, _65553] : [pair_in_list(create_slb, _65553, _65551)], (204 ^ _58588) ^ [_65732, _65734, _65736, _65738, _65740] : [pair_in_list(insert_slb(_65740, pair(_65738, _65734)), _65736, _65732), -(pair_in_list(_65740, _65736, _65732)), 211 ^ _58588 : [(212 ^ _58588) ^ [] : [-(_65738 = _65736)], (214 ^ _58588) ^ [] : [-(_65734 = _65732)]]], (216 ^ _58588) ^ [_66111, _66113, _66115, _66117, _66119] : [-(pair_in_list(insert_slb(_66119, pair(_66117, _66113)), _66115, _66111)), 217 ^ _58588 : [(218 ^ _58588) ^ [] : [pair_in_list(_66119, _66115, _66111)], (220 ^ _58588) ^ [] : [_66117 = _66115, _66113 = _66111]]], (228 ^ _58588) ^ [_66537, _66539, _66541] : [-(remove_slb(insert_slb(_66541, pair(_66539, _66537)), _66539) = _66541)], (230 ^ _58588) ^ [_66685, _66687, _66689, _66691] : [-(remove_slb(insert_slb(_66691, pair(_66689, _66685)), _66687) = insert_slb(remove_slb(_66691, _66687), pair(_66689, _66685))), -(_66689 = _66687), contains_slb(_66691, _66687)], (240 ^ _58588) ^ [_67042, _67044, _67046] : [-(lookup_slb(insert_slb(_67046, pair(_67044, _67042)), _67044) = _67042)], (242 ^ _58588) ^ [_67190, _67192, _67194, _67196] : [-(lookup_slb(insert_slb(_67196, pair(_67194, _67190)), _67192) = lookup_slb(_67196, _67192)), -(_67194 = _67192), contains_slb(_67196, _67192)], (252 ^ _58588) ^ [_67507] : [-(update_slb(create_slb, _67507) = create_slb)], (254 ^ _58588) ^ [_67645, _67647, _67649, _67651] : [strictly_less_than(_67645, _67647), -(update_slb(insert_slb(_67651, pair(_67649, _67645)), _67647) = insert_slb(update_slb(_67651, _67647), pair(_67649, _67647)))], (260 ^ _58588) ^ [_67911, _67913, _67915, _67917] : [less_than(_67913, _67911), -(update_slb(insert_slb(_67917, pair(_67915, _67911)), _67913) = insert_slb(update_slb(_67917, _67913), pair(_67915, _67911)))], (90 ^ _58588) ^ [_61614, _61616, _61618, _61620] : [-(remove_slb(_61620, _61616) = remove_slb(_61618, _61614)), _61620 = _61618, _61616 = _61614], (100 ^ _58588) ^ [_61973, _61975, _61977, _61979] : [-(lookup_slb(_61979, _61975) = lookup_slb(_61977, _61973)), _61979 = _61977, _61975 = _61973], (110 ^ _58588) ^ [_62332, _62334, _62336, _62338] : [-(insert_slb(_62338, _62334) = insert_slb(_62336, _62332)), _62338 = _62336, _62334 = _62332], (120 ^ _58588) ^ [_62691, _62693, _62695, _62697] : [-(pair(_62697, _62693) = pair(_62695, _62691)), _62697 = _62695, _62693 = _62691], (130 ^ _58588) ^ [_63030, _63032, _63034, _63036] : [-(update_slb(_63036, _63032) = update_slb(_63034, _63030)), _63036 = _63034, _63032 = _63030], (2 ^ _58588) ^ [_58732] : [-(_58732 = _58732)], (4 ^ _58588) ^ [_58839, _58841] : [_58841 = _58839, -(_58839 = _58841)], (10 ^ _58588) ^ [_59043, _59045, _59047] : [-(_59047 = _59043), _59047 = _59045, _59045 = _59043], (20 ^ _58588) ^ [_59356, _59358] : [-(isnonempty_slb(_59356)), _59358 = _59356, isnonempty_slb(_59358)], (30 ^ _58588) ^ [_59679, _59681, _59683, _59685] : [-(contains_slb(_59683, _59679)), contains_slb(_59685, _59681), _59685 = _59683, _59681 = _59679], (44 ^ _58588) ^ [_60123, _60125, _60127, _60129] : [-(less_than(_60127, _60123)), less_than(_60129, _60125), _60129 = _60127, _60125 = _60123], (76 ^ _58588) ^ [_61156, _61158, _61160, _61162] : [-(strictly_less_than(_61160, _61156)), strictly_less_than(_61162, _61158), _61162 = _61160, _61158 = _61156], (58 ^ _58588) ^ [_60595, _60597, _60599, _60601, _60603, _60605] : [-(pair_in_list(_60603, _60599, _60595)), pair_in_list(_60605, _60601, _60597), _60605 = _60603, _60601 = _60599, _60597 = _60595]], input).
% 1.10/1.36 ncf('1',plain,[pair_in_list(update_slb(285 ^ [], 292 ^ []), 286 ^ [], 292 ^ []), strictly_less_than(286 ^ [], 292 ^ [])],start(294 ^ 0,bind([[_69310, _69312], [292 ^ [], 286 ^ []]]))).
% 1.10/1.36 ncf('1.1',plain,[-(pair_in_list(update_slb(285 ^ [], 292 ^ []), 286 ^ [], 292 ^ [])), pair_in_list(285 ^ [], 286 ^ [], 287 ^ []), strictly_less_than(287 ^ [], 292 ^ [])],extension(276 ^ 1,bind([[_68562, _68564, _68566, _68568], [292 ^ [], 287 ^ [], 286 ^ [], 285 ^ []]]))).
% 1.10/1.36 ncf('1.1.1',plain,[-(pair_in_list(285 ^ [], 286 ^ [], 287 ^ []))],extension(289 ^ 2)).
% 1.10/1.36 ncf('1.1.2',plain,[-(strictly_less_than(287 ^ [], 292 ^ [])), less_than(287 ^ [], 292 ^ []), -(less_than(292 ^ [], 287 ^ []))],extension(166 ^ 2,bind([[_64278, _64280], [292 ^ [], 287 ^ []]]))).
% 1.10/1.36 ncf('1.1.2.1',plain,[-(less_than(287 ^ [], 292 ^ [])), -(less_than(292 ^ [], 287 ^ []))],extension(150 ^ 3,bind([[_63722, _63724], [292 ^ [], 287 ^ []]]))).
% 1.10/1.36 ncf('1.1.2.1.1',plain,[less_than(292 ^ [], 287 ^ []), -(pair_in_list(update_slb(285 ^ [], 292 ^ []), 286 ^ [], 287 ^ [])), pair_in_list(285 ^ [], 286 ^ [], 287 ^ [])],extension(266 ^ 4,bind([[_68225, _68227, _68229, _68231], [292 ^ [], 287 ^ [], 286 ^ [], 285 ^ []]]))).
% 1.10/1.36 ncf('1.1.2.1.1.1',plain,[pair_in_list(update_slb(285 ^ [], 292 ^ []), 286 ^ [], 287 ^ []), strictly_less_than(286 ^ [], 287 ^ [])],extension(294 ^ 5,bind([[_69310, _69312], [287 ^ [], 286 ^ []]]))).
% 1.10/1.36 ncf('1.1.2.1.1.1.1',plain,[-(strictly_less_than(286 ^ [], 287 ^ []))],extension(291 ^ 6)).
% 1.10/1.36 ncf('1.1.2.1.1.2',plain,[-(pair_in_list(285 ^ [], 286 ^ [], 287 ^ []))],lemmata('[1].x')).
% 1.10/1.36 ncf('1.1.2.2',plain,[less_than(292 ^ [], 287 ^ []), -(less_than(292 ^ [], 287 ^ [])), less_than(292 ^ [], 292 ^ [])],extension(140 ^ 3,bind([[_63413, _63415, _63417], [287 ^ [], 292 ^ [], 292 ^ []]]))).
% 1.10/1.36 ncf('1.1.2.2.1',plain,[less_than(292 ^ [], 287 ^ []), -(pair_in_list(update_slb(285 ^ [], 292 ^ []), 286 ^ [], 287 ^ [])), pair_in_list(285 ^ [], 286 ^ [], 287 ^ [])],extension(266 ^ 4,bind([[_68225, _68227, _68229, _68231], [292 ^ [], 287 ^ [], 286 ^ [], 285 ^ []]]))).
% 1.10/1.36 ncf('1.1.2.2.1.1',plain,[pair_in_list(update_slb(285 ^ [], 292 ^ []), 286 ^ [], 287 ^ []), strictly_less_than(286 ^ [], 287 ^ [])],extension(294 ^ 5,bind([[_69310, _69312], [287 ^ [], 286 ^ []]]))).
% 1.10/1.36 ncf('1.1.2.2.1.1.1',plain,[-(strictly_less_than(286 ^ [], 287 ^ []))],extension(291 ^ 6)).
% 1.10/1.36 ncf('1.1.2.2.1.2',plain,[-(pair_in_list(285 ^ [], 286 ^ [], 287 ^ []))],lemmata('[1].x')).
% 1.10/1.36 ncf('1.1.2.2.2',plain,[-(less_than(292 ^ [], 292 ^ [])), less_than(292 ^ [], 287 ^ []), less_than(287 ^ [], 292 ^ [])],extension(140 ^ 4,bind([[_63413, _63415, _63417], [292 ^ [], 287 ^ [], 292 ^ []]]))).
% 1.10/1.36 ncf('1.1.2.2.2.1',plain,[-(less_than(292 ^ [], 287 ^ []))],reduction('1.1.2')).
% 1.10/1.36 ncf('1.1.2.2.2.2',plain,[-(less_than(287 ^ [], 292 ^ []))],lemmata('[1, 1].x')).
% 1.10/1.36 ncf('1.2',plain,[-(strictly_less_than(286 ^ [], 292 ^ [])), less_than(286 ^ [], 292 ^ []), -(less_than(292 ^ [], 286 ^ []))],extension(166 ^ 1,bind([[_64278, _64280], [292 ^ [], 286 ^ []]]))).
% 1.10/1.36 ncf('1.2.1',plain,[-(less_than(286 ^ [], 292 ^ [])), -(less_than(292 ^ [], 286 ^ []))],extension(150 ^ 2,bind([[_63722, _63724], [292 ^ [], 286 ^ []]]))).
% 1.10/1.36 ncf('1.2.1.1',plain,[less_than(292 ^ [], 286 ^ []), -(less_than(292 ^ [], 287 ^ [])), less_than(286 ^ [], 287 ^ [])],extension(140 ^ 3,bind([[_63413, _63415, _63417], [287 ^ [], 286 ^ [], 292 ^ []]]))).
% 1.10/1.36 ncf('1.2.1.1.1',plain,[less_than(292 ^ [], 287 ^ []), -(pair_in_list(update_slb(285 ^ [], 292 ^ []), 286 ^ [], 287 ^ [])), pair_in_list(285 ^ [], 286 ^ [], 287 ^ [])],extension(266 ^ 4,bind([[_68225, _68227, _68229, _68231], [292 ^ [], 287 ^ [], 286 ^ [], 285 ^ []]]))).
% 1.10/1.36 ncf('1.2.1.1.1.1',plain,[pair_in_list(update_slb(285 ^ [], 292 ^ []), 286 ^ [], 287 ^ []), strictly_less_than(286 ^ [], 287 ^ [])],extension(294 ^ 5,bind([[_69310, _69312], [287 ^ [], 286 ^ []]]))).
% 1.10/1.36 ncf('1.2.1.1.1.1.1',plain,[-(strictly_less_than(286 ^ [], 287 ^ []))],extension(291 ^ 6)).
% 1.10/1.36 ncf('1.2.1.1.1.2',plain,[-(pair_in_list(285 ^ [], 286 ^ [], 287 ^ []))],extension(289 ^ 5)).
% 1.10/1.36 ncf('1.2.1.1.2',plain,[-(less_than(286 ^ [], 287 ^ [])), -(less_than(287 ^ [], 286 ^ []))],extension(150 ^ 4,bind([[_63722, _63724], [287 ^ [], 286 ^ []]]))).
% 1.10/1.36 ncf('1.2.1.1.2.1',plain,[less_than(287 ^ [], 286 ^ []), strictly_less_than(286 ^ [], 287 ^ [])],extension(158 ^ 5,bind([[_64040, _64042], [287 ^ [], 286 ^ []]]))).
% 1.10/1.36 ncf('1.2.1.1.2.1.1',plain,[-(strictly_less_than(286 ^ [], 287 ^ []))],extension(291 ^ 6)).
% 1.10/1.36 ncf('1.2.2',plain,[less_than(292 ^ [], 286 ^ []), -(less_than(292 ^ [], 287 ^ [])), less_than(286 ^ [], 287 ^ [])],extension(140 ^ 2,bind([[_63413, _63415, _63417], [287 ^ [], 286 ^ [], 292 ^ []]]))).
% 1.10/1.36 ncf('1.2.2.1',plain,[less_than(292 ^ [], 287 ^ []), -(less_than(292 ^ [], 287 ^ [])), less_than(287 ^ [], 287 ^ [])],extension(140 ^ 3,bind([[_63413, _63415, _63417], [287 ^ [], 287 ^ [], 292 ^ []]]))).
% 1.10/1.36 ncf('1.2.2.1.1',plain,[less_than(292 ^ [], 287 ^ []), -(pair_in_list(update_slb(285 ^ [], 292 ^ []), 286 ^ [], 287 ^ [])), pair_in_list(285 ^ [], 286 ^ [], 287 ^ [])],extension(266 ^ 4,bind([[_68225, _68227, _68229, _68231], [292 ^ [], 287 ^ [], 286 ^ [], 285 ^ []]]))).
% 1.10/1.36 ncf('1.2.2.1.1.1',plain,[pair_in_list(update_slb(285 ^ [], 292 ^ []), 286 ^ [], 287 ^ []), strictly_less_than(286 ^ [], 287 ^ [])],extension(294 ^ 5,bind([[_69310, _69312], [287 ^ [], 286 ^ []]]))).
% 1.10/1.36 ncf('1.2.2.1.1.1.1',plain,[-(strictly_less_than(286 ^ [], 287 ^ []))],extension(291 ^ 6)).
% 1.10/1.36 ncf('1.2.2.1.1.2',plain,[-(pair_in_list(285 ^ [], 286 ^ [], 287 ^ []))],extension(289 ^ 5)).
% 1.10/1.36 ncf('1.2.2.1.2',plain,[-(less_than(287 ^ [], 287 ^ [])), -(less_than(287 ^ [], 287 ^ []))],extension(150 ^ 4,bind([[_63722, _63724], [287 ^ [], 287 ^ []]]))).
% 1.10/1.36 ncf('1.2.2.1.2.1',plain,[less_than(287 ^ [], 287 ^ [])],reduction('1.2.2.1')).
% 1.10/1.36 ncf('1.2.2.2',plain,[-(less_than(286 ^ [], 287 ^ [])), -(less_than(287 ^ [], 286 ^ []))],extension(150 ^ 3,bind([[_63722, _63724], [287 ^ [], 286 ^ []]]))).
% 1.10/1.36 ncf('1.2.2.2.1',plain,[less_than(287 ^ [], 286 ^ []), -(less_than(287 ^ [], 286 ^ [])), less_than(286 ^ [], 286 ^ [])],extension(140 ^ 4,bind([[_63413, _63415, _63417], [286 ^ [], 286 ^ [], 287 ^ []]]))).
% 1.10/1.36 ncf('1.2.2.2.1.1',plain,[less_than(287 ^ [], 286 ^ []), strictly_less_than(286 ^ [], 287 ^ [])],extension(158 ^ 5,bind([[_64040, _64042], [287 ^ [], 286 ^ []]]))).
% 1.10/1.36 ncf('1.2.2.2.1.1.1',plain,[-(strictly_less_than(286 ^ [], 287 ^ []))],extension(291 ^ 6)).
% 1.10/1.36 ncf('1.2.2.2.1.2',plain,[-(less_than(286 ^ [], 286 ^ [])), -(less_than(286 ^ [], 286 ^ []))],extension(150 ^ 5,bind([[_63722, _63724], [286 ^ [], 286 ^ []]]))).
% 1.10/1.36 ncf('1.2.2.2.1.2.1',plain,[less_than(286 ^ [], 286 ^ [])],reduction('1.2.2.2.1')).
% 1.10/1.36 %-----------------------------------------------------
% 1.10/1.36 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------