%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS085+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n028.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:14 EDT 2023
% Result : Unsatisfiable 0.51s 1.38s
% Output : Proof 0.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS085+1 : TPTP v8.1.2. Released v3.1.0.
% 0.11/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n028.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 18 23:11:03 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.51/1.38
% 0.51/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is Unsatisfiable
% 0.51/1.38 Start of proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.51/1.38 %-----------------------------------------------------
% 0.51/1.38 ncf(matrix, plain, [(2 ^ _49662) ^ [_49766] : [-(_49766 = _49766)], (4 ^ _49662) ^ [_49873, _49875] : [_49875 = _49873, -(_49873 = _49875)], (10 ^ _49662) ^ [_50077, _50079, _50081] : [-(_50081 = _50077), _50081 = _50079, _50079 = _50077], (20 ^ _49662) ^ [_50390, _50392] : [-(cowlNothing(_50390)), _50392 = _50390, cowlNothing(_50392)], (30 ^ _49662) ^ [_50685, _50687] : [-(xsd_string(_50685)), _50687 = _50685, xsd_string(_50687)], (40 ^ _49662) ^ [_50980, _50982] : [-(xsd_integer(_50980)), _50982 = _50980, xsd_integer(_50982)], (50 ^ _49662) ^ [_51275, _51277] : [-(cp1(_51275)), _51277 = _51275, cp1(_51277)], (60 ^ _49662) ^ [_51570, _51572] : [-(cowlThing(_51570)), _51572 = _51570, cowlThing(_51572)], (70 ^ _49662) ^ [_51893, _51895, _51897, _51899] : [-(rinvF(_51897, _51893)), rinvF(_51899, _51895), _51899 = _51897, _51895 = _51893], (84 ^ _49662) ^ [_52337, _52339, _52341, _52343] : [-(rf(_52341, _52337)), rf(_52343, _52339), _52343 = _52341, _52339 = _52337], (98 ^ _49662) ^ [_52781, _52783, _52785, _52787] : [-(rinvR(_52785, _52781)), rinvR(_52787, _52783), _52787 = _52785, _52783 = _52781], (126 ^ _49662) ^ [_53621, _53623] : [-(cUnsatisfiable(_53621)), _53623 = _53621, cUnsatisfiable(_53623)], (112 ^ _49662) ^ [_53225, _53227, _53229, _53231] : [-(rr(_53229, _53225)), rr(_53231, _53227), _53231 = _53229, _53227 = _53225], (136 ^ _49662) ^ [_53940, _53942] : [-(cUnsatisfiable(_53940)), _53942 = _53940, cUnsatisfiable(_53942)], (146 ^ _49662) ^ [_54235, _54237] : [-(cowlNothing(_54235)), _54237 = _54235, cowlNothing(_54237)], (156 ^ _49662) ^ [_54530, _54532] : [-(cowlThing(_54530)), _54532 = _54530, cowlThing(_54532)], (166 ^ _49662) ^ [_54825, _54827] : [-(cp1(_54825)), _54827 = _54825, cp1(_54827)], (176 ^ _49662) ^ [_55134, _55136, _55138] : [-(rf(_55136, _55134)), _55138 = _55136, rf(_55138, _55134)], (186 ^ _49662) ^ [_55457, _55459, _55461] : [-(rf(_55457, _55459)), _55461 = _55459, rf(_55457, _55461)], (196 ^ _49662) ^ [_55780, _55782, _55784] : [-(rinvF(_55782, _55780)), _55784 = _55782, rinvF(_55784, _55780)], (206 ^ _49662) ^ [_56103, _56105, _56107] : [-(rinvF(_56103, _56105)), _56107 = _56105, rinvF(_56103, _56107)], (216 ^ _49662) ^ [_56426, _56428, _56430] : [-(rinvR(_56428, _56426)), _56430 = _56428, rinvR(_56430, _56426)], (226 ^ _49662) ^ [_56749, _56751, _56753] : [-(rinvR(_56749, _56751)), _56753 = _56751, rinvR(_56749, _56753)], (236 ^ _49662) ^ [_57072, _57074, _57076] : [-(rr(_57074, _57072)), _57076 = _57074, rr(_57076, _57072)], (246 ^ _49662) ^ [_57395, _57397, _57399] : [-(rr(_57395, _57397)), _57399 = _57397, rr(_57395, _57399)], (256 ^ _49662) ^ [_57704, _57706] : [-(xsd_integer(_57704)), _57706 = _57704, xsd_integer(_57706)], (266 ^ _49662) ^ [_57999, _58001] : [-(xsd_string(_57999)), _58001 = _57999, xsd_string(_58001)], (276 ^ _49662) ^ [_58285] : [-(cowlThing(_58285))], (278 ^ _49662) ^ [_58327] : [cowlNothing(_58327)], (280 ^ _49662) ^ [_58450] : [xsd_string(_58450), xsd_integer(_58450)], (286 ^ _49662) ^ [_58603] : [-(xsd_integer(_58603)), -(xsd_string(_58603))], (292 ^ _49662) ^ [_58823] : [cUnsatisfiable(_58823), 296 ^ _49662 : [(310 ^ _49662) ^ [] : [-(cp1(_58823))], (297 ^ _49662) ^ [] : [-(rr(_58823, 295 ^ [_58823]))], (300 ^ _49662) ^ [] : [-(rr(295 ^ [_58823], 298 ^ [_58823]))], (302 ^ _49662) ^ [] : [-(cp1(298 ^ [_58823]))], (304 ^ _49662) ^ [_59362] : [rinvR(298 ^ [_58823], _59362), cp1(_59362)]]], (312 ^ _49662) ^ [_59591] : [-(cUnsatisfiable(_59591)), cp1(_59591), 315 ^ _49662 : [(316 ^ _49662) ^ [_59745] : [rr(_59591, _59745), 319 ^ _49662 : [(320 ^ _49662) ^ [_59901] : [rr(_59745, _59901), cp1(_59901), 328 ^ _49662 : [(329 ^ _49662) ^ [] : [-(rinvR(_59901, 327 ^ [_59591, _59745, _59901]))], (331 ^ _49662) ^ [] : [-(cp1(327 ^ [_59591, _59745, _59901]))]]]]]]], (337 ^ _49662) ^ [_60455] : [cowlThing(_60455), 340 ^ _49662 : [(341 ^ _49662) ^ [_60611, _60613] : [-(_60613 = _60611), rf(_60455, _60613), rf(_60455, _60611)]]], (351 ^ _49662) ^ [_60956, _60958] : [rinvF(_60958, _60956), -(rf(_60956, _60958))], (357 ^ _49662) ^ [_61118, _61120] : [rf(_61118, _61120), -(rinvF(_61120, _61118))], (385 ^ _49662) ^ [] : [-(cUnsatisfiable(i2003_11_14_17_19_39537))], (375 ^ _49662) ^ [_61747, _61749, _61751] : [-(rr(_61751, _61747)), rr(_61751, _61749), rr(_61749, _61747)], (363 ^ _49662) ^ [_61359, _61361] : [rinvR(_61361, _61359), -(rr(_61359, _61361))], (369 ^ _49662) ^ [_61521, _61523] : [rr(_61521, _61523), -(rinvR(_61523, _61521))]], input).
% 0.51/1.38 ncf('1',plain,[cUnsatisfiable(i2003_11_14_17_19_39537), 304 : rinvR(298 ^ [i2003_11_14_17_19_39537], i2003_11_14_17_19_39537), 304 : cp1(i2003_11_14_17_19_39537)],start(292 ^ 0,bind([[_58823, _59362], [i2003_11_14_17_19_39537, i2003_11_14_17_19_39537]]))).
% 0.51/1.38 ncf('1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_19_39537))],extension(385 ^ 1)).
% 0.51/1.38 ncf('1.2',plain,[-(rinvR(298 ^ [i2003_11_14_17_19_39537], i2003_11_14_17_19_39537)), rr(i2003_11_14_17_19_39537, 298 ^ [i2003_11_14_17_19_39537])],extension(369 ^ 3,bind([[_61521, _61523], [i2003_11_14_17_19_39537, 298 ^ [i2003_11_14_17_19_39537]]]))).
% 0.51/1.38 ncf('1.2.1',plain,[-(rr(i2003_11_14_17_19_39537, 298 ^ [i2003_11_14_17_19_39537])), rr(i2003_11_14_17_19_39537, 295 ^ [i2003_11_14_17_19_39537]), rr(295 ^ [i2003_11_14_17_19_39537], 298 ^ [i2003_11_14_17_19_39537])],extension(375 ^ 4,bind([[_61747, _61749, _61751], [298 ^ [i2003_11_14_17_19_39537], 295 ^ [i2003_11_14_17_19_39537], i2003_11_14_17_19_39537]]))).
% 0.51/1.38 ncf('1.2.1.1',plain,[-(rr(i2003_11_14_17_19_39537, 295 ^ [i2003_11_14_17_19_39537]))],extension(297 ^ 5)).
% 0.51/1.38 ncf('1.2.1.2',plain,[-(rr(295 ^ [i2003_11_14_17_19_39537], 298 ^ [i2003_11_14_17_19_39537]))],extension(300 ^ 5)).
% 0.51/1.38 ncf('1.3',plain,[-(cp1(i2003_11_14_17_19_39537))],extension(310 ^ 3)).
% 0.51/1.38 %-----------------------------------------------------
% 0.51/1.38 End of proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------