%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS172+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n016.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:25 EDT 2023
% Result : Theorem 0.52s 1.39s
% Output : Proof 0.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS172+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n016.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:26:27 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.52/1.39
% 0.52/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.52/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.52/1.39 %-----------------------------------------------------
% 0.52/1.39 ncf(matrix, plain, [(262 ^ _42355) ^ [] : [cowlThing(263 ^ []), -(cowlNothing(263 ^ [])), 275 ^ _42355 : [(276 ^ _42355) ^ [] : [-(xsd_string(272 ^ []))], (278 ^ _42355) ^ [] : [-(xsd_integer(272 ^ []))]], 279 ^ _42355 : [(280 ^ _42355) ^ [] : [xsd_integer(272 ^ [])], (282 ^ _42355) ^ [] : [xsd_string(272 ^ [])]], 287 ^ _42355 : [(288 ^ _42355) ^ [] : [-(rq(283 ^ [], 284 ^ []))], (290 ^ _42355) ^ [] : [rp(283 ^ [], 284 ^ [])]], 291 ^ _42355 : [(292 ^ _42355) ^ [] : [-(rp(283 ^ [], 284 ^ []))], (294 ^ _42355) ^ [] : [rq(283 ^ [], 284 ^ [])]]], (2 ^ _42355) ^ [_42479] : [-(_42479 = _42479)], (4 ^ _42355) ^ [_42586, _42588] : [_42588 = _42586, -(_42586 = _42588)], (10 ^ _42355) ^ [_42790, _42792, _42794] : [-(_42794 = _42790), _42794 = _42792, _42792 = _42790], (20 ^ _42355) ^ [_43103, _43105] : [-(cd(_43103)), _43105 = _43103, cd(_43105)], (30 ^ _42355) ^ [_43398, _43400] : [-(cowlThing(_43398)), _43400 = _43398, cowlThing(_43400)], (40 ^ _42355) ^ [_43693, _43695] : [-(cowlNothing(_43693)), _43695 = _43693, cowlNothing(_43695)], (50 ^ _42355) ^ [_43988, _43990] : [-(xsd_string(_43988)), _43990 = _43988, xsd_string(_43990)], (60 ^ _42355) ^ [_44283, _44285] : [-(xsd_integer(_44283)), _44285 = _44283, xsd_integer(_44285)], (70 ^ _42355) ^ [_44606, _44608, _44610, _44612] : [-(rq(_44610, _44606)), rq(_44612, _44608), _44612 = _44610, _44608 = _44606], (84 ^ _42355) ^ [_45030, _45032, _45034, _45036] : [-(rp(_45034, _45030)), rp(_45036, _45032), _45036 = _45034, _45032 = _45030], (98 ^ _42355) ^ [_45464, _45466] : [-(cd(_45464)), _45466 = _45464, cd(_45466)], (108 ^ _42355) ^ [_45759, _45761] : [-(cowlNothing(_45759)), _45761 = _45759, cowlNothing(_45761)], (118 ^ _42355) ^ [_46054, _46056] : [-(cowlThing(_46054)), _46056 = _46054, cowlThing(_46056)], (128 ^ _42355) ^ [_46363, _46365, _46367] : [-(rp(_46365, _46363)), _46367 = _46365, rp(_46367, _46363)], (138 ^ _42355) ^ [_46686, _46688, _46690] : [-(rp(_46686, _46688)), _46690 = _46688, rp(_46686, _46690)], (148 ^ _42355) ^ [_47009, _47011, _47013] : [-(rq(_47011, _47009)), _47013 = _47011, rq(_47013, _47009)], (158 ^ _42355) ^ [_47332, _47334, _47336] : [-(rq(_47332, _47334)), _47336 = _47334, rq(_47332, _47336)], (168 ^ _42355) ^ [_47641, _47643] : [-(xsd_integer(_47641)), _47643 = _47641, xsd_integer(_47643)], (178 ^ _42355) ^ [_47936, _47938] : [-(xsd_string(_47936)), _47938 = _47936, xsd_string(_47938)], (188 ^ _42355) ^ [_48222] : [-(cowlThing(_48222))], (190 ^ _42355) ^ [_48264] : [cowlNothing(_48264)], (192 ^ _42355) ^ [_48387] : [xsd_string(_48387), xsd_integer(_48387)], (198 ^ _42355) ^ [_48540] : [-(xsd_integer(_48540)), -(xsd_string(_48540))], (204 ^ _42355) ^ [_48760] : [cd(_48760), -(rq(_48760, iv))], (210 ^ _42355) ^ [_48914] : [rq(_48914, iv), -(cd(_48914))], (216 ^ _42355) ^ [_49133] : [cd(_49133), -(rp(_49133, iv))], (222 ^ _42355) ^ [_49287] : [rp(_49287, iv), -(cd(_49287))], (228 ^ _42355) ^ [_49505, _49507, _49509] : [-(_49507 = _49505), rp(_49509, _49507), rp(_49509, _49505)], (238 ^ _42355) ^ [_49814, _49816] : [rp(_49816, _49814), -(cd(_49816))], (260 ^ _42355) ^ [] : [-(cowlThing(iv))], (254 ^ _42355) ^ [_50345, _50347] : [rq(_50347, _50345), -(cd(_50347))], (244 ^ _42355) ^ [_50036, _50038, _50040] : [-(_50038 = _50036), rq(_50040, _50038), rq(_50040, _50036)]], input).
% 0.52/1.39 ncf('1',plain,[cowlNothing(263 ^ [])],start(190 ^ 0,bind([[_48264], [263 ^ []]]))).
% 0.52/1.39 ncf('1.1',plain,[-(cowlNothing(263 ^ [])), cowlThing(263 ^ []), 276 : -(xsd_string(272 ^ [])), 280 : xsd_integer(272 ^ []), 288 : -(rq(283 ^ [], 284 ^ [])), 292 : -(rp(283 ^ [], 284 ^ []))],extension(262 ^ 1)).
% 0.52/1.39 ncf('1.1.1',plain,[-(cowlThing(263 ^ []))],extension(188 ^ 2,bind([[_48222], [263 ^ []]]))).
% 0.52/1.39 ncf('1.1.2',plain,[xsd_string(272 ^ []), -(xsd_string(272 ^ [])), 272 ^ [] = 272 ^ []],extension(50 ^ 4,bind([[_43988, _43990], [272 ^ [], 272 ^ []]]))).
% 0.52/1.39 ncf('1.1.2.1',plain,[xsd_string(272 ^ []), -(xsd_string(272 ^ [])), 272 ^ [] = 272 ^ []],extension(50 ^ 5,bind([[_43988, _43990], [272 ^ [], 272 ^ []]]))).
% 0.52/1.39 ncf('1.1.2.1.1',plain,[xsd_string(272 ^ []), -(xsd_string(272 ^ [])), 272 ^ [] = 272 ^ []],extension(50 ^ 6,bind([[_43988, _43990], [272 ^ [], 272 ^ []]]))).
% 0.52/1.39 ncf('1.1.2.1.1.1',plain,[xsd_string(272 ^ []), xsd_integer(272 ^ [])],extension(192 ^ 7,bind([[_48387], [272 ^ []]]))).
% 0.52/1.39 ncf('1.1.2.1.1.1.1',plain,[-(xsd_integer(272 ^ []))],extension(278 ^ 8)).
% 0.52/1.39 ncf('1.1.2.1.1.2',plain,[-(272 ^ [] = 272 ^ [])],extension(2 ^ 7,bind([[_42479], [272 ^ []]]))).
% 0.52/1.39 ncf('1.1.2.1.2',plain,[-(272 ^ [] = 272 ^ [])],extension(2 ^ 6,bind([[_42479], [272 ^ []]]))).
% 0.52/1.39 ncf('1.1.2.2',plain,[-(272 ^ [] = 272 ^ [])],extension(2 ^ 5,bind([[_42479], [272 ^ []]]))).
% 0.52/1.39 ncf('1.1.3',plain,[-(xsd_integer(272 ^ [])), -(xsd_string(272 ^ []))],extension(198 ^ 4,bind([[_48540], [272 ^ []]]))).
% 0.52/1.39 ncf('1.1.3.1',plain,[xsd_string(272 ^ [])],extension(282 ^ 5)).
% 0.52/1.39 ncf('1.1.4',plain,[rq(283 ^ [], 284 ^ []), -(iv = 284 ^ []), rq(283 ^ [], iv)],extension(244 ^ 4,bind([[_50036, _50038, _50040], [284 ^ [], iv, 283 ^ []]]))).
% 0.52/1.39 ncf('1.1.4.1',plain,[iv = 284 ^ [], -(rp(283 ^ [], 284 ^ [])), rp(283 ^ [], iv), 283 ^ [] = 283 ^ []],extension(84 ^ 5,bind([[_45030, _45032, _45034, _45036], [284 ^ [], iv, 283 ^ [], 283 ^ []]]))).
% 0.52/1.39 ncf('1.1.4.1.1',plain,[rp(283 ^ [], 284 ^ [])],extension(290 ^ 6)).
% 0.52/1.39 ncf('1.1.4.1.2',plain,[-(rp(283 ^ [], iv)), cd(283 ^ [])],extension(216 ^ 6,bind([[_49133], [283 ^ []]]))).
% 0.52/1.39 ncf('1.1.4.1.2.1',plain,[-(cd(283 ^ [])), rq(283 ^ [], 284 ^ [])],extension(254 ^ 7,bind([[_50345, _50347], [284 ^ [], 283 ^ []]]))).
% 0.52/1.39 ncf('1.1.4.1.2.1.1',plain,[-(rq(283 ^ [], 284 ^ []))],reduction('1.1')).
% 0.52/1.39 ncf('1.1.4.1.3',plain,[-(283 ^ [] = 283 ^ [])],extension(2 ^ 6,bind([[_42479], [283 ^ []]]))).
% 0.52/1.39 ncf('1.1.4.2',plain,[-(rq(283 ^ [], iv)), cd(283 ^ [])],extension(204 ^ 5,bind([[_48760], [283 ^ []]]))).
% 0.52/1.39 ncf('1.1.4.2.1',plain,[-(cd(283 ^ [])), rq(283 ^ [], 284 ^ [])],extension(254 ^ 6,bind([[_50345, _50347], [284 ^ [], 283 ^ []]]))).
% 0.52/1.39 ncf('1.1.4.2.1.1',plain,[-(rq(283 ^ [], 284 ^ []))],reduction('1.1')).
% 0.52/1.39 ncf('1.1.5',plain,[rp(283 ^ [], 284 ^ []), -(iv = 284 ^ []), rp(283 ^ [], iv)],extension(228 ^ 4,bind([[_49505, _49507, _49509], [284 ^ [], iv, 283 ^ []]]))).
% 0.52/1.39 ncf('1.1.5.1',plain,[iv = 284 ^ [], -(rq(283 ^ [], 284 ^ [])), rq(283 ^ [], iv), 283 ^ [] = 283 ^ []],extension(70 ^ 5,bind([[_44606, _44608, _44610, _44612], [284 ^ [], iv, 283 ^ [], 283 ^ []]]))).
% 0.52/1.39 ncf('1.1.5.1.1',plain,[rq(283 ^ [], 284 ^ [])],extension(294 ^ 6)).
% 0.52/1.39 ncf('1.1.5.1.2',plain,[-(rq(283 ^ [], iv)), cd(283 ^ [])],extension(204 ^ 6,bind([[_48760], [283 ^ []]]))).
% 0.52/1.39 ncf('1.1.5.1.2.1',plain,[-(cd(283 ^ [])), rp(283 ^ [], 284 ^ [])],extension(238 ^ 7,bind([[_49814, _49816], [284 ^ [], 283 ^ []]]))).
% 0.52/1.39 ncf('1.1.5.1.2.1.1',plain,[-(rp(283 ^ [], 284 ^ []))],reduction('1.1')).
% 0.52/1.39 ncf('1.1.5.1.3',plain,[-(283 ^ [] = 283 ^ [])],extension(2 ^ 6,bind([[_42479], [283 ^ []]]))).
% 0.52/1.39 ncf('1.1.5.2',plain,[-(rp(283 ^ [], iv)), cd(283 ^ [])],extension(216 ^ 5,bind([[_49133], [283 ^ []]]))).
% 0.52/1.39 ncf('1.1.5.2.1',plain,[-(cd(283 ^ [])), rp(283 ^ [], 284 ^ [])],extension(238 ^ 6,bind([[_49814, _49816], [284 ^ [], 283 ^ []]]))).
% 0.52/1.39 ncf('1.1.5.2.1.1',plain,[-(rp(283 ^ [], 284 ^ []))],reduction('1.1')).
% 0.52/1.39 %-----------------------------------------------------
% 0.52/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------