%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS138+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n022.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.42s 1.37s
% Output : Proof 0.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : KRS138+1 : TPTP v8.1.2. Released v3.1.0.
% 0.00/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n022.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 23:01:16 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.42/1.37
% 0.42/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.42/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.42/1.37 %-----------------------------------------------------
% 0.42/1.37 ncf(matrix, plain, [(214 ^ _44535) ^ [] : [cowlThing(215 ^ []), -(cowlNothing(215 ^ [])), 227 ^ _44535 : [(228 ^ _44535) ^ [] : [-(xsd_string(224 ^ []))], (230 ^ _44535) ^ [] : [-(xsd_integer(224 ^ []))]], 231 ^ _44535 : [(232 ^ _44535) ^ [] : [xsd_integer(224 ^ [])], (234 ^ _44535) ^ [] : [xsd_string(224 ^ [])]], 239 ^ _44535 : [(240 ^ _44535) ^ [] : [-(requalityOnA(237 ^ [], 238 ^ []))], (242 ^ _44535) ^ [] : [237 ^ [] = ia], (244 ^ _44535) ^ [] : [237 ^ [] = ib], (246 ^ _44535) ^ [] : [237 ^ [] = ic]], 251 ^ _44535 : [(252 ^ _44535) ^ [] : [-(requalityOnA(249 ^ [], 250 ^ []))], (254 ^ _44535) ^ [] : [requalityOnA(250 ^ [], 249 ^ [])]], cowlThing(ia), requalityOnA(ia, ia), cowlThing(ib), cowlThing(ic)], (2 ^ _44535) ^ [_44659] : [-(_44659 = _44659)], (4 ^ _44535) ^ [_44766, _44768] : [_44768 = _44766, -(_44766 = _44768)], (10 ^ _44535) ^ [_44970, _44972, _44974] : [-(_44974 = _44970), _44974 = _44972, _44972 = _44970], (20 ^ _44535) ^ [_45283, _45285] : [-(cA(_45283)), _45285 = _45283, cA(_45285)], (30 ^ _44535) ^ [_45578, _45580] : [-(cowlNothing(_45578)), _45580 = _45578, cowlNothing(_45580)], (40 ^ _44535) ^ [_45873, _45875] : [-(xsd_string(_45873)), _45875 = _45873, xsd_string(_45875)], (50 ^ _44535) ^ [_46168, _46170] : [-(xsd_integer(_46168)), _46170 = _46168, xsd_integer(_46170)], (74 ^ _44535) ^ [_46887, _46889] : [-(cowlThing(_46887)), _46889 = _46887, cowlThing(_46889)], (60 ^ _44535) ^ [_46491, _46493, _46495, _46497] : [-(requalityOnA(_46495, _46491)), requalityOnA(_46497, _46493), _46497 = _46495, _46493 = _46491], (84 ^ _44535) ^ [_47198, _47200] : [-(cA(_47198)), _47200 = _47198, cA(_47200)], (94 ^ _44535) ^ [_47493, _47495] : [-(cowlNothing(_47493)), _47495 = _47493, cowlNothing(_47495)], (104 ^ _44535) ^ [_47788, _47790] : [-(cowlThing(_47788)), _47790 = _47788, cowlThing(_47790)], (114 ^ _44535) ^ [_48097, _48099, _48101] : [-(requalityOnA(_48099, _48097)), _48101 = _48099, requalityOnA(_48101, _48097)], (124 ^ _44535) ^ [_48420, _48422, _48424] : [-(requalityOnA(_48420, _48422)), _48424 = _48422, requalityOnA(_48420, _48424)], (134 ^ _44535) ^ [_48729, _48731] : [-(xsd_integer(_48729)), _48731 = _48729, xsd_integer(_48731)], (144 ^ _44535) ^ [_49024, _49026] : [-(xsd_string(_49024)), _49026 = _49024, xsd_string(_49026)], (154 ^ _44535) ^ [_49310] : [-(cowlThing(_49310))], (156 ^ _44535) ^ [_49352] : [cowlNothing(_49352)], (158 ^ _44535) ^ [_49475] : [xsd_string(_49475), xsd_integer(_49475)], (164 ^ _44535) ^ [_49628] : [-(xsd_integer(_49628)), -(xsd_string(_49628))], (180 ^ _44535) ^ [_50088] : [181 ^ _44535 : [(182 ^ _44535) ^ [] : [_50088 = ib], (184 ^ _44535) ^ [] : [_50088 = ia]], -(cA(_50088))], (170 ^ _44535) ^ [_49848] : [cA(_49848), -(_49848 = ib), -(_49848 = ia)], (204 ^ _44535) ^ [] : [-(cowlThing(ia))], (206 ^ _44535) ^ [] : [-(requalityOnA(ia, ia))], (208 ^ _44535) ^ [] : [-(cowlThing(ib))], (210 ^ _44535) ^ [] : [-(requalityOnA(ib, ib))], (212 ^ _44535) ^ [] : [-(cowlThing(ic))], (198 ^ _44535) ^ [_50687, _50689] : [requalityOnA(_50689, _50687), -(cA(_50687))], (188 ^ _44535) ^ [_50378, _50380, _50382] : [-(_50380 = _50378), requalityOnA(_50380, _50382), requalityOnA(_50378, _50382)]], input).
% 0.42/1.37 ncf('1',plain,[cowlNothing(215 ^ [])],start(156 ^ 0,bind([[_49352], [215 ^ []]]))).
% 0.42/1.37 ncf('1.1',plain,[-(cowlNothing(215 ^ [])), cowlThing(215 ^ []), 228 : -(xsd_string(224 ^ [])), 232 : xsd_integer(224 ^ []), 240 : -(requalityOnA(237 ^ [], 238 ^ [])), 252 : -(requalityOnA(249 ^ [], 250 ^ [])), 252 : cowlThing(ia), 252 : requalityOnA(ia, ia), 252 : cowlThing(ib), 252 : cowlThing(ic)],extension(214 ^ 1)).
% 0.42/1.37 ncf('1.1.1',plain,[-(cowlThing(215 ^ []))],extension(154 ^ 2,bind([[_49310], [215 ^ []]]))).
% 0.42/1.37 ncf('1.1.2',plain,[xsd_string(224 ^ []), -(xsd_string(224 ^ [])), 224 ^ [] = 224 ^ []],extension(40 ^ 4,bind([[_45873, _45875], [224 ^ [], 224 ^ []]]))).
% 0.42/1.37 ncf('1.1.2.1',plain,[xsd_string(224 ^ []), -(xsd_string(224 ^ [])), 224 ^ [] = 224 ^ []],extension(40 ^ 5,bind([[_45873, _45875], [224 ^ [], 224 ^ []]]))).
% 0.42/1.37 ncf('1.1.2.1.1',plain,[xsd_string(224 ^ []), -(xsd_string(224 ^ [])), 224 ^ [] = 224 ^ []],extension(40 ^ 6,bind([[_45873, _45875], [224 ^ [], 224 ^ []]]))).
% 0.42/1.37 ncf('1.1.2.1.1.1',plain,[xsd_string(224 ^ []), -(xsd_string(224 ^ [])), 224 ^ [] = 224 ^ []],extension(40 ^ 7,bind([[_45873, _45875], [224 ^ [], 224 ^ []]]))).
% 0.42/1.37 ncf('1.1.2.1.1.1.1',plain,[xsd_string(224 ^ []), xsd_integer(224 ^ [])],extension(158 ^ 8,bind([[_49475], [224 ^ []]]))).
% 0.42/1.37 ncf('1.1.2.1.1.1.1.1',plain,[-(xsd_integer(224 ^ []))],extension(230 ^ 9)).
% 0.42/1.37 ncf('1.1.2.1.1.1.2',plain,[-(224 ^ [] = 224 ^ [])],extension(2 ^ 8,bind([[_44659], [224 ^ []]]))).
% 0.42/1.37 ncf('1.1.2.1.1.2',plain,[-(224 ^ [] = 224 ^ [])],extension(2 ^ 7,bind([[_44659], [224 ^ []]]))).
% 0.42/1.37 ncf('1.1.2.1.2',plain,[-(224 ^ [] = 224 ^ [])],extension(2 ^ 6,bind([[_44659], [224 ^ []]]))).
% 0.42/1.37 ncf('1.1.2.2',plain,[-(224 ^ [] = 224 ^ [])],extension(2 ^ 5,bind([[_44659], [224 ^ []]]))).
% 0.42/1.37 ncf('1.1.3',plain,[-(xsd_integer(224 ^ [])), -(xsd_string(224 ^ []))],extension(164 ^ 4,bind([[_49628], [224 ^ []]]))).
% 0.42/1.37 ncf('1.1.3.1',plain,[xsd_string(224 ^ [])],extension(234 ^ 5)).
% 0.42/1.37 ncf('1.1.4',plain,[requalityOnA(237 ^ [], 238 ^ []), -(cA(238 ^ []))],extension(198 ^ 4,bind([[_50687, _50689], [238 ^ [], 237 ^ []]]))).
% 0.42/1.37 ncf('1.1.4.1',plain,[cA(238 ^ []), -(238 ^ [] = ib), -(238 ^ [] = ia)],extension(170 ^ 5,bind([[_49848], [238 ^ []]]))).
% 0.42/1.37 ncf('1.1.4.1.1',plain,[238 ^ [] = ib, -(238 ^ [] = 237 ^ []), ib = 237 ^ []],extension(10 ^ 6,bind([[_44970, _44972, _44974], [237 ^ [], ib, 238 ^ []]]))).
% 0.42/1.37 ncf('1.1.4.1.1.1',plain,[238 ^ [] = 237 ^ [], -(cA(237 ^ [])), cA(238 ^ [])],extension(20 ^ 7,bind([[_45283, _45285], [237 ^ [], 238 ^ []]]))).
% 0.42/1.37 ncf('1.1.4.1.1.1.1',plain,[cA(237 ^ []), -(237 ^ [] = ib), -(237 ^ [] = ia)],extension(170 ^ 8,bind([[_49848], [237 ^ []]]))).
% 0.42/1.37 ncf('1.1.4.1.1.1.1.1',plain,[237 ^ [] = ib],extension(244 ^ 9)).
% 0.42/1.37 ncf('1.1.4.1.1.1.1.2',plain,[237 ^ [] = ia],extension(242 ^ 9)).
% 0.42/1.37 ncf('1.1.4.1.1.1.2',plain,[-(cA(238 ^ []))],reduction('1.1.4')).
% 0.42/1.37 ncf('1.1.4.1.1.2',plain,[-(ib = 237 ^ []), requalityOnA(ib, ib), requalityOnA(237 ^ [], ib)],extension(188 ^ 7,bind([[_50378, _50380, _50382], [237 ^ [], ib, ib]]))).
% 0.42/1.37 ncf('1.1.4.1.1.2.1',plain,[-(requalityOnA(ib, ib))],extension(210 ^ 8)).
% 0.42/1.37 ncf('1.1.4.1.1.2.2',plain,[-(requalityOnA(237 ^ [], ib)), 238 ^ [] = ib, requalityOnA(237 ^ [], 238 ^ [])],extension(124 ^ 8,bind([[_48420, _48422, _48424], [237 ^ [], ib, 238 ^ []]]))).
% 0.42/1.37 ncf('1.1.4.1.1.2.2.1',plain,[-(238 ^ [] = ib)],reduction('1.1.4.1')).
% 0.42/1.37 ncf('1.1.4.1.1.2.2.2',plain,[-(requalityOnA(237 ^ [], 238 ^ []))],reduction('1.1')).
% 0.42/1.37 ncf('1.1.4.1.2',plain,[238 ^ [] = ia, -(ia = 238 ^ [])],extension(4 ^ 6,bind([[_44766, _44768], [ia, 238 ^ []]]))).
% 0.42/1.37 ncf('1.1.4.1.2.1',plain,[ia = 238 ^ [], -(requalityOnA(ia, 238 ^ [])), requalityOnA(238 ^ [], ia), 238 ^ [] = ia],extension(60 ^ 7,bind([[_46491, _46493, _46495, _46497], [238 ^ [], ia, ia, 238 ^ []]]))).
% 0.42/1.37 ncf('1.1.4.1.2.1.1',plain,[requalityOnA(ia, 238 ^ []), -(237 ^ [] = ia), requalityOnA(237 ^ [], 238 ^ [])],extension(188 ^ 8,bind([[_50378, _50380, _50382], [ia, 237 ^ [], 238 ^ []]]))).
% 0.42/1.38 ncf('1.1.4.1.2.1.1.1',plain,[237 ^ [] = ia],extension(242 ^ 9)).
% 0.42/1.38 ncf('1.1.4.1.2.1.1.2',plain,[-(requalityOnA(237 ^ [], 238 ^ []))],reduction('1.1')).
% 0.42/1.38 ncf('1.1.4.1.2.1.2',plain,[-(requalityOnA(238 ^ [], ia)), ia = 238 ^ [], requalityOnA(ia, ia)],extension(114 ^ 8,bind([[_48097, _48099, _48101], [ia, 238 ^ [], ia]]))).
% 0.42/1.38 ncf('1.1.4.1.2.1.2.1',plain,[-(ia = 238 ^ [])],reduction('1.1.4.1.2')).
% 0.42/1.38 ncf('1.1.4.1.2.1.2.2',plain,[-(requalityOnA(ia, ia))],extension(206 ^ 9)).
% 0.42/1.38 ncf('1.1.4.1.2.1.3',plain,[-(238 ^ [] = ia)],reduction('1.1.4.1')).
% 0.42/1.38 ncf('1.1.5',plain,[requalityOnA(249 ^ [], 250 ^ []), -(cA(250 ^ []))],extension(198 ^ 4,bind([[_50687, _50689], [250 ^ [], 249 ^ []]]))).
% 0.42/1.38 ncf('1.1.5.1',plain,[cA(250 ^ []), -(250 ^ [] = ib), -(250 ^ [] = ia)],extension(170 ^ 5,bind([[_49848], [250 ^ []]]))).
% 0.42/1.38 ncf('1.1.5.1.1',plain,[250 ^ [] = ib, -(250 ^ [] = 249 ^ []), ib = 249 ^ []],extension(10 ^ 6,bind([[_44970, _44972, _44974], [249 ^ [], ib, 250 ^ []]]))).
% 0.42/1.38 ncf('1.1.5.1.1.1',plain,[250 ^ [] = 249 ^ [], -(249 ^ [] = 250 ^ [])],extension(4 ^ 7,bind([[_44766, _44768], [249 ^ [], 250 ^ []]]))).
% 0.42/1.38 ncf('1.1.5.1.1.1.1',plain,[249 ^ [] = 250 ^ [], -(requalityOnA(250 ^ [], 249 ^ [])), requalityOnA(249 ^ [], 250 ^ []), 250 ^ [] = 249 ^ []],extension(60 ^ 8,bind([[_46491, _46493, _46495, _46497], [249 ^ [], 250 ^ [], 250 ^ [], 249 ^ []]]))).
% 0.42/1.38 ncf('1.1.5.1.1.1.1.1',plain,[requalityOnA(250 ^ [], 249 ^ [])],extension(254 ^ 9)).
% 0.42/1.38 ncf('1.1.5.1.1.1.1.2',plain,[-(requalityOnA(249 ^ [], 250 ^ []))],reduction('1.1')).
% 0.42/1.38 ncf('1.1.5.1.1.1.1.3',plain,[-(250 ^ [] = 249 ^ [])],reduction('1.1.5.1.1')).
% 0.42/1.38 ncf('1.1.5.1.1.2',plain,[-(ib = 249 ^ []), requalityOnA(ib, ib), requalityOnA(249 ^ [], ib)],extension(188 ^ 7,bind([[_50378, _50380, _50382], [249 ^ [], ib, ib]]))).
% 0.42/1.38 ncf('1.1.5.1.1.2.1',plain,[-(requalityOnA(ib, ib))],extension(210 ^ 8)).
% 0.42/1.38 ncf('1.1.5.1.1.2.2',plain,[-(requalityOnA(249 ^ [], ib)), 250 ^ [] = ib, requalityOnA(249 ^ [], 250 ^ [])],extension(124 ^ 8,bind([[_48420, _48422, _48424], [249 ^ [], ib, 250 ^ []]]))).
% 0.42/1.38 ncf('1.1.5.1.1.2.2.1',plain,[-(250 ^ [] = ib)],reduction('1.1.5.1')).
% 0.42/1.38 ncf('1.1.5.1.1.2.2.2',plain,[-(requalityOnA(249 ^ [], 250 ^ []))],reduction('1.1')).
% 0.42/1.38 ncf('1.1.5.1.2',plain,[250 ^ [] = ia, -(250 ^ [] = 249 ^ []), ia = 249 ^ []],extension(10 ^ 6,bind([[_44970, _44972, _44974], [249 ^ [], ia, 250 ^ []]]))).
% 0.42/1.38 ncf('1.1.5.1.2.1',plain,[250 ^ [] = 249 ^ [], -(249 ^ [] = 250 ^ [])],extension(4 ^ 7,bind([[_44766, _44768], [249 ^ [], 250 ^ []]]))).
% 0.42/1.38 ncf('1.1.5.1.2.1.1',plain,[249 ^ [] = 250 ^ [], -(requalityOnA(250 ^ [], 249 ^ [])), requalityOnA(249 ^ [], 250 ^ []), 250 ^ [] = 249 ^ []],extension(60 ^ 8,bind([[_46491, _46493, _46495, _46497], [249 ^ [], 250 ^ [], 250 ^ [], 249 ^ []]]))).
% 0.42/1.38 ncf('1.1.5.1.2.1.1.1',plain,[requalityOnA(250 ^ [], 249 ^ [])],extension(254 ^ 9)).
% 0.42/1.38 ncf('1.1.5.1.2.1.1.2',plain,[-(requalityOnA(249 ^ [], 250 ^ []))],reduction('1.1')).
% 0.42/1.38 ncf('1.1.5.1.2.1.1.3',plain,[-(250 ^ [] = 249 ^ [])],reduction('1.1.5.1.2')).
% 0.42/1.38 ncf('1.1.5.1.2.2',plain,[-(ia = 249 ^ []), requalityOnA(ia, ia), requalityOnA(249 ^ [], ia)],extension(188 ^ 7,bind([[_50378, _50380, _50382], [249 ^ [], ia, ia]]))).
% 0.42/1.38 ncf('1.1.5.1.2.2.1',plain,[-(requalityOnA(ia, ia))],extension(206 ^ 8)).
% 0.42/1.38 ncf('1.1.5.1.2.2.2',plain,[-(requalityOnA(249 ^ [], ia)), 250 ^ [] = ia, requalityOnA(249 ^ [], 250 ^ [])],extension(124 ^ 8,bind([[_48420, _48422, _48424], [249 ^ [], ia, 250 ^ []]]))).
% 0.42/1.38 ncf('1.1.5.1.2.2.2.1',plain,[-(250 ^ [] = ia)],reduction('1.1.5.1')).
% 0.42/1.38 ncf('1.1.5.1.2.2.2.2',plain,[-(requalityOnA(249 ^ [], 250 ^ []))],reduction('1.1')).
% 0.42/1.38 ncf('1.1.6',plain,[-(cowlThing(ia))],extension(154 ^ 2,bind([[_49310], [ia]]))).
% 0.42/1.38 ncf('1.1.7',plain,[-(requalityOnA(ia, ia)), requalityOnA(ia, ia), ia = ia, ia = ia],extension(60 ^ 2,bind([[_46491, _46493, _46495, _46497], [ia, ia, ia, ia]]))).
% 0.42/1.38 ncf('1.1.7.1',plain,[-(requalityOnA(ia, ia)), requalityOnA(ia, ia), ia = ia, ia = ia],extension(60 ^ 3,bind([[_46491, _46493, _46495, _46497], [ia, ia, ia, ia]]))).
% 0.42/1.38 ncf('1.1.7.1.1',plain,[-(requalityOnA(ia, ia)), requalityOnA(ia, ia), ia = ia, ia = ia],extension(60 ^ 4,bind([[_46491, _46493, _46495, _46497], [ia, ia, ia, ia]]))).
% 0.42/1.38 ncf('1.1.7.1.1.1',plain,[-(requalityOnA(ia, ia)), requalityOnA(ia, ia), ia = ia, ia = ia],extension(60 ^ 5,bind([[_46491, _46493, _46495, _46497], [ia, ia, ia, ia]]))).
% 0.42/1.38 ncf('1.1.7.1.1.1.1',plain,[-(requalityOnA(ia, ia))],extension(206 ^ 6)).
% 0.42/1.38 ncf('1.1.7.1.1.1.2',plain,[-(ia = ia)],extension(2 ^ 6,bind([[_44659], [ia]]))).
% 0.42/1.38 ncf('1.1.7.1.1.1.3',plain,[-(ia = ia)],extension(2 ^ 6,bind([[_44659], [ia]]))).
% 0.42/1.38 ncf('1.1.7.1.1.2',plain,[-(ia = ia)],extension(2 ^ 5,bind([[_44659], [ia]]))).
% 0.42/1.38 ncf('1.1.7.1.1.3',plain,[-(ia = ia)],extension(2 ^ 5,bind([[_44659], [ia]]))).
% 0.42/1.38 ncf('1.1.7.1.2',plain,[-(ia = ia)],extension(2 ^ 4,bind([[_44659], [ia]]))).
% 0.42/1.38 ncf('1.1.7.1.3',plain,[-(ia = ia)],extension(2 ^ 4,bind([[_44659], [ia]]))).
% 0.42/1.38 ncf('1.1.7.2',plain,[-(ia = ia)],extension(2 ^ 3,bind([[_44659], [ia]]))).
% 0.42/1.38 ncf('1.1.7.3',plain,[-(ia = ia)],lemmata('[1, 1].x')).
% 0.42/1.38 ncf('1.1.8',plain,[-(cowlThing(ib))],extension(154 ^ 2,bind([[_49310], [ib]]))).
% 0.42/1.38 ncf('1.1.9',plain,[-(cowlThing(ic))],extension(154 ^ 2,bind([[_49310], [ic]]))).
% 0.42/1.38 %-----------------------------------------------------
% 0.42/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------