%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS167+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n004.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.36s 1.36s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS167+1 : TPTP v8.1.2. Released v3.1.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n004.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 : Thu May 18 22:53:54 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.36/1.36
% 0.36/1.36 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.36/1.36 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.36 %-----------------------------------------------------
% 0.36/1.36 ncf(matrix, plain, [(256 ^ _42233) ^ [] : [cowlThing(257 ^ []), -(cowlNothing(257 ^ [])), 269 ^ _42233 : [(270 ^ _42233) ^ [] : [-(xsd_string(266 ^ []))], (272 ^ _42233) ^ [] : [-(xsd_integer(266 ^ []))]], 273 ^ _42233 : [(274 ^ _42233) ^ [] : [xsd_integer(266 ^ [])], (276 ^ _42233) ^ [] : [xsd_string(266 ^ [])]], 280 ^ _42233 : [(281 ^ _42233) ^ [] : [-(cc1(277 ^ []))], (283 ^ _42233) ^ [] : [cc2(277 ^ [])]], 284 ^ _42233 : [(285 ^ _42233) ^ [] : [-(cc2(277 ^ []))], (287 ^ _42233) ^ [] : [cc1(277 ^ [])]]], (2 ^ _42233) ^ [_42357] : [-(_42357 = _42357)], (4 ^ _42233) ^ [_42464, _42466] : [_42466 = _42464, -(_42464 = _42466)], (10 ^ _42233) ^ [_42668, _42670, _42672] : [-(_42672 = _42668), _42672 = _42670, _42670 = _42668], (20 ^ _42233) ^ [_43009, _43011, _43013, _43015] : [-(rp(_43013, _43009)), rp(_43015, _43011), _43015 = _43013, _43011 = _43009], (34 ^ _42233) ^ [_43425, _43427] : [-(cowlThing(_43425)), _43427 = _43425, cowlThing(_43427)], (44 ^ _42233) ^ [_43720, _43722] : [-(cowlNothing(_43720)), _43722 = _43720, cowlNothing(_43722)], (54 ^ _42233) ^ [_44015, _44017] : [-(xsd_string(_44015)), _44017 = _44015, xsd_string(_44017)], (64 ^ _42233) ^ [_44310, _44312] : [-(xsd_integer(_44310)), _44312 = _44310, xsd_integer(_44312)], (74 ^ _42233) ^ [_44605, _44607] : [-(cc1(_44605)), _44607 = _44605, cc1(_44607)], (84 ^ _42233) ^ [_44880, _44882] : [-(cc2(_44880)), _44882 = _44880, cc2(_44882)], (94 ^ _42233) ^ [_45193, _45195] : [-(cc1(_45193)), _45195 = _45193, cc1(_45195)], (104 ^ _42233) ^ [_45488, _45490] : [-(cc2(_45488)), _45490 = _45488, cc2(_45490)], (114 ^ _42233) ^ [_45783, _45785] : [-(cowlNothing(_45783)), _45785 = _45783, cowlNothing(_45785)], (124 ^ _42233) ^ [_46078, _46080] : [-(cowlThing(_46078)), _46080 = _46078, cowlThing(_46080)], (134 ^ _42233) ^ [_46387, _46389, _46391] : [-(rp(_46389, _46387)), _46391 = _46389, rp(_46391, _46387)], (144 ^ _42233) ^ [_46710, _46712, _46714] : [-(rp(_46710, _46712)), _46714 = _46712, rp(_46710, _46714)], (154 ^ _42233) ^ [_47019, _47021] : [-(xsd_integer(_47019)), _47021 = _47019, xsd_integer(_47021)], (164 ^ _42233) ^ [_47314, _47316] : [-(xsd_string(_47314)), _47316 = _47314, xsd_string(_47316)], (174 ^ _42233) ^ [_47600] : [-(cowlThing(_47600))], (176 ^ _42233) ^ [_47642] : [cowlNothing(_47642)], (178 ^ _42233) ^ [_47765] : [xsd_string(_47765), xsd_integer(_47765)], (184 ^ _42233) ^ [_47918] : [-(xsd_integer(_47918)), -(xsd_string(_47918))], (207 ^ _42233) ^ [_48685] : [-(cc1(_48685)), 210 ^ _42233 : [(211 ^ _42233) ^ [_48812] : [rp(_48685, _48812)]], 214 ^ _42233 : [(215 ^ _42233) ^ [] : [-(rp(_48685, 212 ^ [_48685]))], (217 ^ _42233) ^ [] : [-(rp(_48685, 213 ^ [_48685]))], (219 ^ _42233) ^ [] : [212 ^ [_48685] = 213 ^ [_48685]]]], (190 ^ _42233) ^ [_48138] : [cc1(_48138), 194 ^ _42233 : [(195 ^ _42233) ^ [] : [-(rp(_48138, 193 ^ [_48138]))], (197 ^ _42233) ^ [_48415, _48417] : [-(_48417 = _48415), rp(_48138, _48417), rp(_48138, _48415)]]], (240 ^ _42233) ^ [_49836] : [-(cc2(_49836)), 243 ^ _42233 : [(244 ^ _42233) ^ [_49963] : [rp(_49836, _49963)]], 247 ^ _42233 : [(248 ^ _42233) ^ [] : [-(rp(_49836, 245 ^ [_49836]))], (250 ^ _42233) ^ [] : [-(rp(_49836, 246 ^ [_49836]))], (252 ^ _42233) ^ [] : [245 ^ [_49836] = 246 ^ [_49836]]]], (223 ^ _42233) ^ [_49289] : [cc2(_49289), 227 ^ _42233 : [(228 ^ _42233) ^ [] : [-(rp(_49289, 226 ^ [_49289]))], (230 ^ _42233) ^ [_49566, _49568] : [-(_49568 = _49566), rp(_49289, _49568), rp(_49289, _49566)]]]], input).
% 0.36/1.36 ncf('1',plain,[cowlNothing(257 ^ [])],start(176 ^ 0,bind([[_47642], [257 ^ []]]))).
% 0.36/1.36 ncf('1.1',plain,[-(cowlNothing(257 ^ [])), cowlThing(257 ^ []), 270 : -(xsd_string(266 ^ [])), 274 : xsd_integer(266 ^ []), 281 : -(cc1(277 ^ [])), 285 : -(cc2(277 ^ []))],extension(256 ^ 1)).
% 0.36/1.36 ncf('1.1.1',plain,[-(cowlThing(257 ^ []))],extension(174 ^ 2,bind([[_47600], [257 ^ []]]))).
% 0.36/1.36 ncf('1.1.2',plain,[xsd_string(266 ^ []), -(xsd_string(266 ^ [])), 266 ^ [] = 266 ^ []],extension(54 ^ 4,bind([[_44015, _44017], [266 ^ [], 266 ^ []]]))).
% 0.36/1.36 ncf('1.1.2.1',plain,[xsd_string(266 ^ []), -(xsd_string(266 ^ [])), 266 ^ [] = 266 ^ []],extension(54 ^ 5,bind([[_44015, _44017], [266 ^ [], 266 ^ []]]))).
% 0.36/1.36 ncf('1.1.2.1.1',plain,[xsd_string(266 ^ []), xsd_integer(266 ^ [])],extension(178 ^ 6,bind([[_47765], [266 ^ []]]))).
% 0.36/1.36 ncf('1.1.2.1.1.1',plain,[-(xsd_integer(266 ^ []))],extension(272 ^ 7)).
% 0.36/1.36 ncf('1.1.2.1.2',plain,[-(266 ^ [] = 266 ^ [])],extension(2 ^ 6,bind([[_42357], [266 ^ []]]))).
% 0.36/1.36 ncf('1.1.2.2',plain,[-(266 ^ [] = 266 ^ [])],extension(2 ^ 5,bind([[_42357], [266 ^ []]]))).
% 0.36/1.36 ncf('1.1.3',plain,[-(xsd_integer(266 ^ [])), -(xsd_string(266 ^ []))],extension(184 ^ 4,bind([[_47918], [266 ^ []]]))).
% 0.36/1.36 ncf('1.1.3.1',plain,[xsd_string(266 ^ [])],extension(276 ^ 5)).
% 0.36/1.36 ncf('1.1.4',plain,[cc1(277 ^ []), 197 : -(245 ^ [277 ^ []] = 246 ^ [277 ^ []]), 197 : rp(277 ^ [], 245 ^ [277 ^ []]), 197 : rp(277 ^ [], 246 ^ [277 ^ []])],extension(190 ^ 4,bind([[_48138, _48415, _48417], [277 ^ [], 246 ^ [277 ^ []], 245 ^ [277 ^ []]]]))).
% 0.36/1.36 ncf('1.1.4.1',plain,[245 ^ [277 ^ []] = 246 ^ [277 ^ []], -(cc2(277 ^ [])), 244 : rp(277 ^ [], 193 ^ [277 ^ []])],extension(240 ^ 7,bind([[_49836, _49963], [277 ^ [], 193 ^ [277 ^ []]]]))).
% 0.36/1.36 ncf('1.1.4.1.1',plain,[cc2(277 ^ [])],extension(283 ^ 8)).
% 0.36/1.36 ncf('1.1.4.1.2',plain,[-(rp(277 ^ [], 193 ^ [277 ^ []]))],extension(195 ^ 10)).
% 0.36/1.36 ncf('1.1.4.2',plain,[-(rp(277 ^ [], 245 ^ [277 ^ []])), -(cc2(277 ^ [])), 244 : rp(277 ^ [], 193 ^ [277 ^ []])],extension(240 ^ 7,bind([[_49836, _49963], [277 ^ [], 193 ^ [277 ^ []]]]))).
% 0.36/1.36 ncf('1.1.4.2.1',plain,[cc2(277 ^ [])],extension(283 ^ 8)).
% 0.36/1.36 ncf('1.1.4.2.2',plain,[-(rp(277 ^ [], 193 ^ [277 ^ []]))],extension(195 ^ 10)).
% 0.36/1.36 ncf('1.1.4.3',plain,[-(rp(277 ^ [], 246 ^ [277 ^ []])), -(cc2(277 ^ [])), 244 : rp(277 ^ [], 193 ^ [277 ^ []])],extension(240 ^ 7,bind([[_49836, _49963], [277 ^ [], 193 ^ [277 ^ []]]]))).
% 0.36/1.36 ncf('1.1.4.3.1',plain,[cc2(277 ^ [])],extension(283 ^ 8)).
% 0.36/1.36 ncf('1.1.4.3.2',plain,[-(rp(277 ^ [], 193 ^ [277 ^ []]))],extension(195 ^ 10)).
% 0.36/1.36 ncf('1.1.5',plain,[cc2(277 ^ []), 230 : -(212 ^ [277 ^ []] = 213 ^ [277 ^ []]), 230 : rp(277 ^ [], 212 ^ [277 ^ []]), 230 : rp(277 ^ [], 213 ^ [277 ^ []])],extension(223 ^ 4,bind([[_49289, _49566, _49568], [277 ^ [], 213 ^ [277 ^ []], 212 ^ [277 ^ []]]]))).
% 0.36/1.36 ncf('1.1.5.1',plain,[212 ^ [277 ^ []] = 213 ^ [277 ^ []], -(cc1(277 ^ [])), 211 : rp(277 ^ [], 226 ^ [277 ^ []])],extension(207 ^ 7,bind([[_48685, _48812], [277 ^ [], 226 ^ [277 ^ []]]]))).
% 0.36/1.36 ncf('1.1.5.1.1',plain,[cc1(277 ^ [])],extension(287 ^ 8)).
% 0.36/1.36 ncf('1.1.5.1.2',plain,[-(rp(277 ^ [], 226 ^ [277 ^ []]))],extension(228 ^ 10)).
% 0.36/1.36 ncf('1.1.5.2',plain,[-(rp(277 ^ [], 212 ^ [277 ^ []])), -(cc1(277 ^ [])), 211 : rp(277 ^ [], 226 ^ [277 ^ []])],extension(207 ^ 7,bind([[_48685, _48812], [277 ^ [], 226 ^ [277 ^ []]]]))).
% 0.36/1.36 ncf('1.1.5.2.1',plain,[cc1(277 ^ [])],extension(287 ^ 8)).
% 0.36/1.36 ncf('1.1.5.2.2',plain,[-(rp(277 ^ [], 226 ^ [277 ^ []]))],extension(228 ^ 10)).
% 0.36/1.36 ncf('1.1.5.3',plain,[-(rp(277 ^ [], 213 ^ [277 ^ []])), -(cc1(277 ^ [])), 211 : rp(277 ^ [], 226 ^ [277 ^ []])],extension(207 ^ 7,bind([[_48685, _48812], [277 ^ [], 226 ^ [277 ^ []]]]))).
% 0.36/1.36 ncf('1.1.5.3.1',plain,[cc1(277 ^ [])],extension(287 ^ 8)).
% 0.36/1.36 ncf('1.1.5.3.2',plain,[-(rp(277 ^ [], 226 ^ [277 ^ []]))],extension(228 ^ 10)).
% 0.36/1.36 %-----------------------------------------------------
% 0.36/1.36 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------