%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS113+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n021.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:18 EDT 2023
% Result : Unsatisfiable 44.01s 42.74s
% Output : Proof 44.01s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS113+1 : TPTP v8.1.2. Released v3.1.0.
% 0.11/0.13 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n021.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:27 EDT 2023
% 0.12/0.34 % CPUTime :
% 44.01/42.74
% 44.01/42.74 /export/starexec/sandbox/benchmark/theBenchmark.p is Unsatisfiable
% 44.01/42.74 Start of proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
% 44.01/42.74 %-----------------------------------------------------
% 44.01/42.74 ncf(matrix, plain, [(449 ^ _65567) ^ [_75066, _75068] : [rs(_75068, _75066), -(rr(_75068, _75066))], (256 ^ _65567) ^ [_68736, _68738, _68740] : [-(rr(_68738, _68736)), _68740 = _68738, rr(_68740, _68736)], (410 ^ _65567) ^ [_73756] : [411 ^ _65567 : [(412 ^ _65567) ^ [_73823] : [ra_Px1(_73756, _73823)]], -(cpxcomp(_73756))], (276 ^ _65567) ^ [_69382, _69384, _69386] : [-(rs(_69384, _69382)), _69386 = _69384, rs(_69386, _69382)], (326 ^ _65567) ^ [_70913] : [-(xsd_integer(_70913)), -(xsd_string(_70913))], (403 ^ _65567) ^ [_73551] : [cpxcomp(_73551), -(ra_Px1(_73551, 406 ^ [_73551]))], (320 ^ _65567) ^ [_70760] : [xsd_string(_70760), xsd_integer(_70760)], (332 ^ _65567) ^ [_71133] : [cUnsatisfiable(_71133), 335 ^ _65567 : [(349 ^ _65567) ^ [] : [-(ca_Vx2(345 ^ [_71133]))], (347 ^ _65567) ^ [] : [-(rr(_71133, 345 ^ [_71133]))], (336 ^ _65567) ^ [_71346, _71348] : [-(_71348 = _71346), rr(_71133, _71348), rr(_71133, _71346)], (354 ^ _65567) ^ [] : [-(cp(350 ^ [_71133]))], (356 ^ _65567) ^ [] : [-(cpxcomp(_71133))], (352 ^ _65567) ^ [] : [-(rs(_71133, 350 ^ [_71133]))]]], (318 ^ _65567) ^ [_70637] : [cowlNothing(_70637)], (426 ^ _65567) ^ [_74294] : [428 ^ _65567 : [(431 ^ _65567) ^ [] : [cp(427 ^ [_74294])], (429 ^ _65567) ^ [] : [-(rinvS(_74294, 427 ^ [_74294]))]], -(ca_Vx2(_74294))], (390 ^ _65567) ^ [_73101] : [cp(_73101), 393 ^ _65567 : [(394 ^ _65567) ^ [_73212] : [ra_Px1(_73101, _73212)]]], (396 ^ _65567) ^ [_73278] : [-(ra_Px1(_73278, 397 ^ [_73278])), -(cp(_73278))], (416 ^ _65567) ^ [_73997] : [ca_Vx2(_73997), 419 ^ _65567 : [(420 ^ _65567) ^ [_74127] : [rinvS(_73997, _74127), -(cp(_74127))]]], (306 ^ _65567) ^ [_70309, _70311] : [-(xsd_string(_70309)), _70311 = _70309, xsd_string(_70311)], (316 ^ _65567) ^ [_70595] : [-(cowlThing(_70595))], (246 ^ _65567) ^ [_68413, _68415, _68417] : [-(rinvS(_68413, _68415)), _68417 = _68415, rinvS(_68413, _68417)], (156 ^ _65567) ^ [_65660, _65662] : [-(cUnsatisfiable(_65660)), _65662 = _65660, cUnsatisfiable(_65662)], (236 ^ _65567) ^ [_68090, _68092, _68094] : [-(rinvS(_68092, _68090)), _68094 = _68092, rinvS(_68094, _68090)], (266 ^ _65567) ^ [_69059, _69061, _69063] : [-(rr(_69059, _69061)), _69063 = _69061, rr(_69059, _69063)], (166 ^ _65567) ^ [_65955, _65957] : [-(ca_Vx2(_65955)), _65957 = _65955, ca_Vx2(_65957)], (176 ^ _65567) ^ [_66250, _66252] : [-(cowlNothing(_66250)), _66252 = _66250, cowlNothing(_66252)], (286 ^ _65567) ^ [_69705, _69707, _69709] : [-(rs(_69705, _69707)), _69709 = _69707, rs(_69705, _69709)], (447 ^ _65567) ^ [] : [-(cUnsatisfiable(i2003_11_14_17_21_22376))], (358 ^ _65567) ^ [_72045] : [-(cUnsatisfiable(_72045)), 363 ^ _65567 : [(368 ^ _65567) ^ [] : [361 ^ [_72045] = 362 ^ [_72045]], (366 ^ _65567) ^ [] : [-(rr(_72045, 362 ^ [_72045]))], (364 ^ _65567) ^ [] : [-(rr(_72045, 361 ^ [_72045]))]], 371 ^ _65567 : [(372 ^ _65567) ^ [_72564] : [rr(_72045, _72564), ca_Vx2(_72564)]], cpxcomp(_72045), 379 ^ _65567 : [(380 ^ _65567) ^ [_72771] : [rs(_72045, _72771), cp(_72771)]]], (441 ^ _65567) ^ [_74821, _74823] : [rs(_74821, _74823), -(rinvS(_74823, _74821))], (186 ^ _65567) ^ [_66545, _66547] : [-(cowlThing(_66545)), _66547 = _66545, cowlThing(_66547)], (435 ^ _65567) ^ [_74659, _74661] : [rinvS(_74661, _74659), -(rs(_74659, _74661))], (206 ^ _65567) ^ [_67135, _67137] : [-(cpxcomp(_67135)), _67137 = _67135, cpxcomp(_67137)], (226 ^ _65567) ^ [_67767, _67769, _67771] : [-(ra_Px1(_67767, _67769)), _67771 = _67769, ra_Px1(_67767, _67771)], (296 ^ _65567) ^ [_70014, _70016] : [-(xsd_integer(_70014)), _70016 = _70014, xsd_integer(_70016)], (216 ^ _65567) ^ [_67444, _67446, _67448] : [-(ra_Px1(_67446, _67444)), _67448 = _67446, ra_Px1(_67448, _67444)], (196 ^ _65567) ^ [_66840, _66842] : [-(cp(_66840)), _66842 = _66840, cp(_66842)], !, (10 ^ _60808) ^ [_61203, _61205, _61207] : [-(_61207 = _61203), _61207 = _61205, _61205 = _61203], (2 ^ _60808) ^ [_60892] : [-(_60892 = _60892)], (128 ^ _60808) ^ [_64792, _64794, _64796, _64798] : [-(rs(_64796, _64792)), rs(_64798, _64794), _64798 = _64796, _64794 = _64792], (60 ^ _60808) ^ [_62696, _62698] : [-(cpxcomp(_62696)), _62698 = _62696, cpxcomp(_62698)], (30 ^ _60808) ^ [_61811, _61813] : [-(cowlNothing(_61811)), _61813 = _61811, cowlNothing(_61813)], (142 ^ _60808) ^ [_65216, _65218, _65220, _65222] : [-(rr(_65220, _65216)), rr(_65222, _65218), _65222 = _65220, _65218 = _65216], (84 ^ _60808) ^ [_63435, _63437] : [-(ca_Vx2(_63435)), _63437 = _63435, ca_Vx2(_63437)], (94 ^ _60808) ^ [_63730, _63732] : [-(cp(_63730)), _63732 = _63730, cp(_63732)], (50 ^ _60808) ^ [_62401, _62403] : [-(xsd_integer(_62401)), _62403 = _62401, xsd_integer(_62403)], (104 ^ _60808) ^ [_64053, _64055, _64057, _64059] : [-(rinvS(_64057, _64053)), rinvS(_64059, _64055), _64059 = _64057, _64055 = _64053], (4 ^ _60808) ^ [_60999, _61001] : [_61001 = _60999, -(_60999 = _61001)], (40 ^ _60808) ^ [_62106, _62108] : [-(xsd_string(_62106)), _62108 = _62106, xsd_string(_62108)], (118 ^ _60808) ^ [_64469, _64471] : [-(cUnsatisfiable(_64469)), _64471 = _64469, cUnsatisfiable(_64471)], (70 ^ _60808) ^ [_63019, _63021, _63023, _63025] : [-(ra_Px1(_63023, _63019)), ra_Px1(_63025, _63021), _63025 = _63023, _63021 = _63019], (20 ^ _60808) ^ [_61516, _61518] : [-(cowlThing(_61516)), _61518 = _61516, cowlThing(_61518)]], input).
% 44.01/42.74 ncf('1',plain,[ca_Vx2(345 ^ [i2003_11_14_17_21_22376]), 420 : rinvS(345 ^ [i2003_11_14_17_21_22376], i2003_11_14_17_21_22376), 420 : -(cp(i2003_11_14_17_21_22376))],start(416 ^ 0,bind([[_73997, _74127], [345 ^ [i2003_11_14_17_21_22376], i2003_11_14_17_21_22376]]))).
% 44.01/42.74 ncf('1.1',plain,[-(ca_Vx2(345 ^ [i2003_11_14_17_21_22376])), cUnsatisfiable(i2003_11_14_17_21_22376)],extension(332 ^ 1,bind([[_71133], [i2003_11_14_17_21_22376]]))).
% 44.01/42.74 ncf('1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_22376))],extension(447 ^ 2)).
% 44.01/42.74 ncf('1.2',plain,[-(rinvS(345 ^ [i2003_11_14_17_21_22376], i2003_11_14_17_21_22376)), 350 ^ [i2003_11_14_17_21_22376] = 345 ^ [i2003_11_14_17_21_22376], rinvS(350 ^ [i2003_11_14_17_21_22376], i2003_11_14_17_21_22376)],extension(236 ^ 3,bind([[_68090, _68092, _68094], [i2003_11_14_17_21_22376, 345 ^ [i2003_11_14_17_21_22376], 350 ^ [i2003_11_14_17_21_22376]]]))).
% 44.01/42.74 ncf('1.2.1',plain,[-(350 ^ [i2003_11_14_17_21_22376] = 345 ^ [i2003_11_14_17_21_22376]), 336 : rr(i2003_11_14_17_21_22376, 350 ^ [i2003_11_14_17_21_22376]), 336 : rr(i2003_11_14_17_21_22376, 345 ^ [i2003_11_14_17_21_22376]), 336 : cUnsatisfiable(i2003_11_14_17_21_22376)],extension(332 ^ 4,bind([[_71133, _71346, _71348], [i2003_11_14_17_21_22376, 345 ^ [i2003_11_14_17_21_22376], 350 ^ [i2003_11_14_17_21_22376]]]))).
% 44.01/42.74 ncf('1.2.1.1',plain,[-(rr(i2003_11_14_17_21_22376, 350 ^ [i2003_11_14_17_21_22376])), rs(i2003_11_14_17_21_22376, 350 ^ [i2003_11_14_17_21_22376])],extension(449 ^ 7,bind([[_75066, _75068], [350 ^ [i2003_11_14_17_21_22376], i2003_11_14_17_21_22376]]))).
% 44.01/42.74 ncf('1.2.1.1.1',plain,[-(rs(i2003_11_14_17_21_22376, 350 ^ [i2003_11_14_17_21_22376]))],extension(352 ^ 8)).
% 44.01/42.74 ncf('1.2.1.2',plain,[-(rr(i2003_11_14_17_21_22376, 345 ^ [i2003_11_14_17_21_22376]))],extension(347 ^ 7)).
% 44.01/42.74 ncf('1.2.1.3',plain,[-(cUnsatisfiable(i2003_11_14_17_21_22376))],extension(447 ^ 5)).
% 44.01/42.74 ncf('1.2.2',plain,[-(rinvS(350 ^ [i2003_11_14_17_21_22376], i2003_11_14_17_21_22376)), rs(i2003_11_14_17_21_22376, 350 ^ [i2003_11_14_17_21_22376])],extension(441 ^ 4,bind([[_74821, _74823], [i2003_11_14_17_21_22376, 350 ^ [i2003_11_14_17_21_22376]]]))).
% 44.01/42.74 ncf('1.2.2.1',plain,[-(rs(i2003_11_14_17_21_22376, 350 ^ [i2003_11_14_17_21_22376])), cUnsatisfiable(i2003_11_14_17_21_22376)],extension(332 ^ 5,bind([[_71133], [i2003_11_14_17_21_22376]]))).
% 44.01/42.74 ncf('1.2.2.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_22376))],extension(447 ^ 6)).
% 44.01/42.74 ncf('1.3',plain,[cp(i2003_11_14_17_21_22376), 394 : ra_Px1(i2003_11_14_17_21_22376, 406 ^ [i2003_11_14_17_21_22376])],extension(390 ^ 3,bind([[_73101, _73212], [i2003_11_14_17_21_22376, 406 ^ [i2003_11_14_17_21_22376]]]))).
% 44.01/42.74 ncf('1.3.1',plain,[-(ra_Px1(i2003_11_14_17_21_22376, 406 ^ [i2003_11_14_17_21_22376])), cpxcomp(i2003_11_14_17_21_22376)],extension(403 ^ 6,bind([[_73551], [i2003_11_14_17_21_22376]]))).
% 44.01/42.74 ncf('1.3.1.1',plain,[-(cpxcomp(i2003_11_14_17_21_22376)), cUnsatisfiable(i2003_11_14_17_21_22376)],extension(332 ^ 7,bind([[_71133], [i2003_11_14_17_21_22376]]))).
% 44.01/42.74 ncf('1.3.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_22376))],extension(447 ^ 8)).
% 44.01/42.74 %-----------------------------------------------------
% 44.01/42.74 End of proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------