%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS088+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n011.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:26:15 EDT 2023
% Result : Unsatisfiable 0.36s 1.41s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : KRS088+1 : TPTP v8.1.2. Released v3.1.0.
% 0.08/0.14 % Command : nanocop.sh %s %d
% 0.13/0.35 % Computer : n011.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 18 23:08:03 EDT 2023
% 0.13/0.36 % CPUTime :
% 0.36/1.41
% 0.36/1.41 /export/starexec/sandbox/benchmark/theBenchmark.p is Unsatisfiable
% 0.36/1.41 Start of proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/1.41 %-----------------------------------------------------
% 0.36/1.41 ncf(matrix, plain, [(2 ^ _49886) ^ [_49990] : [-(_49990 = _49990)], (4 ^ _49886) ^ [_50097, _50099] : [_50099 = _50097, -(_50097 = _50099)], (10 ^ _49886) ^ [_50301, _50303, _50305] : [-(_50305 = _50301), _50305 = _50303, _50303 = _50301], (20 ^ _49886) ^ [_50614, _50616] : [-(cowlThing(_50614)), _50616 = _50614, cowlThing(_50616)], (30 ^ _49886) ^ [_50909, _50911] : [-(cowlNothing(_50909)), _50911 = _50909, cowlNothing(_50911)], (40 ^ _49886) ^ [_51204, _51206] : [-(xsd_string(_51204)), _51206 = _51204, xsd_string(_51206)], (50 ^ _49886) ^ [_51499, _51501] : [-(xsd_integer(_51499)), _51501 = _51499, xsd_integer(_51501)], (60 ^ _49886) ^ [_51794, _51796] : [-(cp1(_51794)), _51796 = _51794, cp1(_51796)], (70 ^ _49886) ^ [_52117, _52119, _52121, _52123] : [-(rinvF(_52121, _52117)), rinvF(_52123, _52119), _52123 = _52121, _52119 = _52117], (84 ^ _49886) ^ [_52561, _52563, _52565, _52567] : [-(rf(_52565, _52561)), rf(_52567, _52563), _52567 = _52565, _52563 = _52561], (98 ^ _49886) ^ [_53005, _53007, _53009, _53011] : [-(rinvR(_53009, _53005)), rinvR(_53011, _53007), _53011 = _53009, _53007 = _53005], (126 ^ _49886) ^ [_53845, _53847] : [-(cUnsatisfiable(_53845)), _53847 = _53845, cUnsatisfiable(_53847)], (112 ^ _49886) ^ [_53449, _53451, _53453, _53455] : [-(rr(_53453, _53449)), rr(_53455, _53451), _53455 = _53453, _53451 = _53449], (136 ^ _49886) ^ [_54164, _54166] : [-(cUnsatisfiable(_54164)), _54166 = _54164, cUnsatisfiable(_54166)], (146 ^ _49886) ^ [_54459, _54461] : [-(cowlNothing(_54459)), _54461 = _54459, cowlNothing(_54461)], (156 ^ _49886) ^ [_54754, _54756] : [-(cowlThing(_54754)), _54756 = _54754, cowlThing(_54756)], (166 ^ _49886) ^ [_55049, _55051] : [-(cp1(_55049)), _55051 = _55049, cp1(_55051)], (176 ^ _49886) ^ [_55358, _55360, _55362] : [-(rf(_55360, _55358)), _55362 = _55360, rf(_55362, _55358)], (186 ^ _49886) ^ [_55681, _55683, _55685] : [-(rf(_55681, _55683)), _55685 = _55683, rf(_55681, _55685)], (196 ^ _49886) ^ [_56004, _56006, _56008] : [-(rinvF(_56006, _56004)), _56008 = _56006, rinvF(_56008, _56004)], (206 ^ _49886) ^ [_56327, _56329, _56331] : [-(rinvF(_56327, _56329)), _56331 = _56329, rinvF(_56327, _56331)], (216 ^ _49886) ^ [_56650, _56652, _56654] : [-(rinvR(_56652, _56650)), _56654 = _56652, rinvR(_56654, _56650)], (226 ^ _49886) ^ [_56973, _56975, _56977] : [-(rinvR(_56973, _56975)), _56977 = _56975, rinvR(_56973, _56977)], (236 ^ _49886) ^ [_57296, _57298, _57300] : [-(rr(_57298, _57296)), _57300 = _57298, rr(_57300, _57296)], (246 ^ _49886) ^ [_57619, _57621, _57623] : [-(rr(_57619, _57621)), _57623 = _57621, rr(_57619, _57623)], (256 ^ _49886) ^ [_57928, _57930] : [-(xsd_integer(_57928)), _57930 = _57928, xsd_integer(_57930)], (266 ^ _49886) ^ [_58223, _58225] : [-(xsd_string(_58223)), _58225 = _58223, xsd_string(_58225)], (276 ^ _49886) ^ [_58509] : [-(cowlThing(_58509))], (278 ^ _49886) ^ [_58551] : [cowlNothing(_58551)], (280 ^ _49886) ^ [_58674] : [xsd_string(_58674), xsd_integer(_58674)], (286 ^ _49886) ^ [_58827] : [-(xsd_integer(_58827)), -(xsd_string(_58827))], (292 ^ _49886) ^ [_59047] : [cUnsatisfiable(_59047), 296 ^ _49886 : [(297 ^ _49886) ^ [] : [-(rf(_59047, 295 ^ [_59047]))], (308 ^ _49886) ^ [] : [-(cp1(295 ^ [_59047]))], (299 ^ _49886) ^ [_59370] : [rinvF(295 ^ [_59047], _59370), 303 ^ _49886 : [(304 ^ _49886) ^ [] : [-(rf(_59370, 302 ^ [_59047, _59370]))], (306 ^ _49886) ^ [] : [cp1(302 ^ [_59047, _59370])]]]]], (310 ^ _49886) ^ [_59746] : [-(cUnsatisfiable(_59746)), 311 ^ _49886 : [(312 ^ _49886) ^ [_59863] : [rf(_59746, _59863), cp1(_59863), 318 ^ _49886 : [(319 ^ _49886) ^ [] : [-(rinvF(_59863, 317 ^ [_59746, _59863]))], (321 ^ _49886) ^ [_60189] : [rf(317 ^ [_59746, _59863], _60189), -(cp1(_60189))]]]]], (331 ^ _49886) ^ [_60542, _60544, _60546] : [-(_60544 = _60542), rf(_60546, _60544), rf(_60546, _60542)], (341 ^ _49886) ^ [_60880, _60882] : [rinvF(_60882, _60880), -(rf(_60880, _60882))], (347 ^ _49886) ^ [_61042, _61044] : [rf(_61042, _61044), -(rinvF(_61044, _61042))], (375 ^ _49886) ^ [] : [-(cUnsatisfiable(i2003_11_14_17_19_49673))], (365 ^ _49886) ^ [_61671, _61673, _61675] : [-(rr(_61675, _61671)), rr(_61675, _61673), rr(_61673, _61671)], (353 ^ _49886) ^ [_61283, _61285] : [rinvR(_61285, _61283), -(rr(_61283, _61285))], (359 ^ _49886) ^ [_61445, _61447] : [rr(_61445, _61447), -(rinvR(_61447, _61445))]], input).
% 0.36/1.41 ncf('1',plain,[cUnsatisfiable(i2003_11_14_17_19_49673), 299 : rinvF(295 ^ [i2003_11_14_17_19_49673], i2003_11_14_17_19_49673), 306 : cp1(302 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673])],start(292 ^ 0,bind([[_59047, _59370], [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673]]))).
% 0.36/1.41 ncf('1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_19_49673))],extension(375 ^ 1)).
% 0.36/1.41 ncf('1.2',plain,[-(rinvF(295 ^ [i2003_11_14_17_19_49673], i2003_11_14_17_19_49673)), rinvF(295 ^ [i2003_11_14_17_19_49673], i2003_11_14_17_19_49673), 295 ^ [i2003_11_14_17_19_49673] = 295 ^ [i2003_11_14_17_19_49673], i2003_11_14_17_19_49673 = i2003_11_14_17_19_49673],extension(70 ^ 3,bind([[_52117, _52119, _52121, _52123], [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673, 295 ^ [i2003_11_14_17_19_49673], 295 ^ [i2003_11_14_17_19_49673]]]))).
% 0.36/1.41 ncf('1.2.1',plain,[-(rinvF(295 ^ [i2003_11_14_17_19_49673], i2003_11_14_17_19_49673)), rf(i2003_11_14_17_19_49673, 295 ^ [i2003_11_14_17_19_49673])],extension(347 ^ 4,bind([[_61042, _61044], [i2003_11_14_17_19_49673, 295 ^ [i2003_11_14_17_19_49673]]]))).
% 0.36/1.41 ncf('1.2.1.1',plain,[-(rf(i2003_11_14_17_19_49673, 295 ^ [i2003_11_14_17_19_49673]))],extension(297 ^ 5)).
% 0.36/1.41 ncf('1.2.2',plain,[-(295 ^ [i2003_11_14_17_19_49673] = 295 ^ [i2003_11_14_17_19_49673])],extension(2 ^ 4,bind([[_49990], [295 ^ [i2003_11_14_17_19_49673]]]))).
% 0.36/1.41 ncf('1.2.3',plain,[-(i2003_11_14_17_19_49673 = i2003_11_14_17_19_49673)],extension(2 ^ 4,bind([[_49990], [i2003_11_14_17_19_49673]]))).
% 0.36/1.41 ncf('1.3',plain,[-(cp1(302 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673])), 295 ^ [i2003_11_14_17_19_49673] = 302 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673], cp1(295 ^ [i2003_11_14_17_19_49673])],extension(60 ^ 5,bind([[_51794, _51796], [302 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673], 295 ^ [i2003_11_14_17_19_49673]]]))).
% 0.36/1.41 ncf('1.3.1',plain,[-(295 ^ [i2003_11_14_17_19_49673] = 302 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673]), rf(i2003_11_14_17_19_49673, 295 ^ [i2003_11_14_17_19_49673]), rf(i2003_11_14_17_19_49673, 302 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673])],extension(331 ^ 6,bind([[_60542, _60544, _60546], [302 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673], 295 ^ [i2003_11_14_17_19_49673], i2003_11_14_17_19_49673]]))).
% 0.36/1.41 ncf('1.3.1.1',plain,[-(rf(i2003_11_14_17_19_49673, 295 ^ [i2003_11_14_17_19_49673]))],extension(297 ^ 7)).
% 0.36/1.41 ncf('1.3.1.2',plain,[-(rf(i2003_11_14_17_19_49673, 302 ^ [i2003_11_14_17_19_49673, i2003_11_14_17_19_49673]))],extension(304 ^ 7)).
% 0.36/1.41 ncf('1.3.2',plain,[-(cp1(295 ^ [i2003_11_14_17_19_49673]))],extension(308 ^ 6)).
% 0.36/1.41 %-----------------------------------------------------
% 0.36/1.41 End of proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------