%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS142+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n002.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:21 EDT 2023
% Result : Theorem 0.34s 1.39s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS142+1 : TPTP v8.1.2. Released v3.1.0.
% 0.11/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n002.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:49 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.34/1.39
% 0.34/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.34/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.34/1.39 %-----------------------------------------------------
% 0.34/1.39 ncf(matrix, plain, [(187 ^ _33337) ^ [] : [cowlThing(188 ^ []), -(cowlNothing(188 ^ [])), 200 ^ _33337 : [(201 ^ _33337) ^ [] : [-(xsd_string(197 ^ []))], (203 ^ _33337) ^ [] : [-(xsd_integer(197 ^ []))]], 204 ^ _33337 : [(205 ^ _33337) ^ [] : [xsd_integer(197 ^ [])], (207 ^ _33337) ^ [] : [xsd_string(197 ^ [])]], 211 ^ _33337 : [(212 ^ _33337) ^ [] : [-(cc(210 ^ []))], (214 ^ _33337) ^ [_39780] : [rp(210 ^ [], _39780)]], 216 ^ _33337 : [(217 ^ _33337) ^ [] : [-(cc(215 ^ []))], (221 ^ _33337) ^ [] : [-(rp(215 ^ [], 218 ^ []))], (223 ^ _33337) ^ [] : [-(rp(215 ^ [], 219 ^ []))], (225 ^ _33337) ^ [] : [218 ^ [] = 219 ^ []]]], (2 ^ _33337) ^ [_33461] : [-(_33461 = _33461)], (4 ^ _33337) ^ [_33568, _33570] : [_33570 = _33568, -(_33568 = _33570)], (10 ^ _33337) ^ [_33772, _33774, _33776] : [-(_33776 = _33772), _33776 = _33774, _33774 = _33772], (20 ^ _33337) ^ [_34085, _34087] : [-(cowlThing(_34085)), _34087 = _34085, cowlThing(_34087)], (30 ^ _33337) ^ [_34380, _34382] : [-(cowlNothing(_34380)), _34382 = _34380, cowlNothing(_34382)], (40 ^ _33337) ^ [_34675, _34677] : [-(xsd_string(_34675)), _34677 = _34675, xsd_string(_34677)], (50 ^ _33337) ^ [_34970, _34972] : [-(xsd_integer(_34970)), _34972 = _34970, xsd_integer(_34972)], (60 ^ _33337) ^ [_35265, _35267] : [-(cc(_35265)), _35267 = _35265, cc(_35267)], (70 ^ _33337) ^ [_35568, _35570, _35572, _35574] : [-(rp(_35572, _35568)), rp(_35574, _35570), _35574 = _35572, _35570 = _35568], (84 ^ _33337) ^ [_36000, _36002] : [-(cc(_36000)), _36002 = _36000, cc(_36002)], (94 ^ _33337) ^ [_36295, _36297] : [-(cowlNothing(_36295)), _36297 = _36295, cowlNothing(_36297)], (104 ^ _33337) ^ [_36590, _36592] : [-(cowlThing(_36590)), _36592 = _36590, cowlThing(_36592)], (114 ^ _33337) ^ [_36899, _36901, _36903] : [-(rp(_36901, _36899)), _36903 = _36901, rp(_36903, _36899)], (124 ^ _33337) ^ [_37222, _37224, _37226] : [-(rp(_37222, _37224)), _37226 = _37224, rp(_37222, _37226)], (134 ^ _33337) ^ [_37531, _37533] : [-(xsd_integer(_37531)), _37533 = _37531, xsd_integer(_37533)], (144 ^ _33337) ^ [_37826, _37828] : [-(xsd_string(_37826)), _37828 = _37826, xsd_string(_37828)], (154 ^ _33337) ^ [_38112] : [-(cowlThing(_38112))], (156 ^ _33337) ^ [_38154] : [cowlNothing(_38154)], (158 ^ _33337) ^ [_38277] : [xsd_string(_38277), xsd_integer(_38277)], (164 ^ _33337) ^ [_38430] : [-(xsd_integer(_38430)), -(xsd_string(_38430))], (170 ^ _33337) ^ [_38601] : [cc(_38601), 174 ^ _33337 : [(175 ^ _33337) ^ [] : [-(rp(_38601, 173 ^ [_38601]))], (177 ^ _33337) ^ [_38878, _38880] : [-(_38880 = _38878), rp(_38601, _38880), rp(_38601, _38878)]]]], input).
% 0.34/1.39 ncf('1',plain,[cowlNothing(188 ^ [])],start(156 ^ 0,bind([[_38154], [188 ^ []]]))).
% 0.34/1.39 ncf('1.1',plain,[-(cowlNothing(188 ^ [])), cowlThing(188 ^ []), 201 : -(xsd_string(197 ^ [])), 205 : xsd_integer(197 ^ []), 214 : rp(210 ^ [], 173 ^ [210 ^ []]), 217 : -(cc(215 ^ []))],extension(187 ^ 1,bind([[_39780], [173 ^ [210 ^ []]]]))).
% 0.34/1.39 ncf('1.1.1',plain,[-(cowlThing(188 ^ []))],extension(154 ^ 2,bind([[_38112], [188 ^ []]]))).
% 0.34/1.39 ncf('1.1.2',plain,[xsd_string(197 ^ []), xsd_integer(197 ^ [])],extension(158 ^ 4,bind([[_38277], [197 ^ []]]))).
% 0.34/1.39 ncf('1.1.2.1',plain,[-(xsd_integer(197 ^ []))],extension(203 ^ 5)).
% 0.34/1.39 ncf('1.1.3',plain,[-(xsd_integer(197 ^ [])), -(xsd_string(197 ^ []))],extension(164 ^ 4,bind([[_38430], [197 ^ []]]))).
% 0.34/1.39 ncf('1.1.3.1',plain,[xsd_string(197 ^ [])],extension(207 ^ 5)).
% 0.34/1.39 ncf('1.1.4',plain,[-(rp(210 ^ [], 173 ^ [210 ^ []])), cc(210 ^ [])],extension(170 ^ 4,bind([[_38601], [210 ^ []]]))).
% 0.34/1.39 ncf('1.1.4.1',plain,[-(cc(210 ^ []))],extension(212 ^ 5)).
% 0.34/1.39 ncf('1.1.5',plain,[cc(215 ^ []), 177 : -(218 ^ [] = 219 ^ []), 177 : rp(215 ^ [], 218 ^ []), 177 : rp(215 ^ [], 219 ^ [])],extension(170 ^ 4,bind([[_38601, _38878, _38880], [215 ^ [], 219 ^ [], 218 ^ []]]))).
% 0.34/1.39 ncf('1.1.5.1',plain,[218 ^ [] = 219 ^ []],extension(225 ^ 7)).
% 0.34/1.39 ncf('1.1.5.2',plain,[-(rp(215 ^ [], 218 ^ []))],extension(221 ^ 7)).
% 0.34/1.39 ncf('1.1.5.3',plain,[-(rp(215 ^ [], 219 ^ []))],extension(223 ^ 7)).
% 0.34/1.39 %-----------------------------------------------------
% 0.34/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------