%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS097+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n017.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:16 EDT 2023
% Result : Unsatisfiable 0.36s 1.37s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : KRS097+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.11/0.33 % Computer : n017.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Thu May 18 22:36:45 EDT 2023
% 0.11/0.33 % CPUTime :
% 0.36/1.37
% 0.36/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is Unsatisfiable
% 0.36/1.37 Start of proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 ncf(matrix, plain, [(2 ^ _82629) ^ [_82733] : [-(_82733 = _82733)], (4 ^ _82629) ^ [_82840, _82842] : [_82842 = _82840, -(_82840 = _82842)], (10 ^ _82629) ^ [_83044, _83046, _83048] : [-(_83048 = _83044), _83048 = _83046, _83046 = _83044], (20 ^ _82629) ^ [_83357, _83359] : [-(cowlThing(_83357)), _83359 = _83357, cowlThing(_83359)], (30 ^ _82629) ^ [_83652, _83654] : [-(cowlNothing(_83652)), _83654 = _83652, cowlNothing(_83654)], (40 ^ _82629) ^ [_83947, _83949] : [-(xsd_string(_83947)), _83949 = _83947, xsd_string(_83949)], (50 ^ _82629) ^ [_84242, _84244] : [-(xsd_integer(_84242)), _84244 = _84242, xsd_integer(_84244)], (60 ^ _82629) ^ [_84537, _84539] : [-(ca(_84537)), _84539 = _84537, ca(_84539)], (70 ^ _82629) ^ [_84832, _84834] : [-(cUnsatisfiable(_84832)), _84834 = _84832, cUnsatisfiable(_84834)], (80 ^ _82629) ^ [_85127, _85129] : [-(cd(_85127)), _85129 = _85127, cd(_85129)], (90 ^ _82629) ^ [_85422, _85424] : [-(ce(_85422)), _85424 = _85422, ce(_85424)], (100 ^ _82629) ^ [_85717, _85719] : [-(cc(_85717)), _85719 = _85717, cc(_85719)], (110 ^ _82629) ^ [_86040, _86042, _86044, _86046] : [-(rt3(_86044, _86040)), rt3(_86046, _86042), _86046 = _86044, _86042 = _86040], (124 ^ _82629) ^ [_86484, _86486, _86488, _86490] : [-(rr1(_86488, _86484)), rr1(_86490, _86486), _86490 = _86488, _86486 = _86484], (138 ^ _82629) ^ [_86928, _86930, _86932, _86934] : [-(rr3(_86932, _86928)), rr3(_86934, _86930), _86934 = _86932, _86930 = _86928], (152 ^ _82629) ^ [_87372, _87374, _87376, _87378] : [-(rt1(_87376, _87372)), rt1(_87378, _87374), _87378 = _87376, _87374 = _87372], (166 ^ _82629) ^ [_87816, _87818, _87820, _87822] : [-(rr2(_87820, _87816)), rr2(_87822, _87818), _87822 = _87820, _87818 = _87816], (180 ^ _82629) ^ [_88260, _88262, _88264, _88266] : [-(rr(_88264, _88260)), rr(_88266, _88262), _88266 = _88264, _88262 = _88260], (194 ^ _82629) ^ [_88704, _88706, _88708, _88710] : [-(rt2(_88708, _88704)), rt2(_88710, _88706), _88710 = _88708, _88706 = _88704], (208 ^ _82629) ^ [_89128, _89130, _89132, _89134] : [-(rtt(_89132, _89128)), rtt(_89134, _89130), _89134 = _89132, _89130 = _89128], (222 ^ _82629) ^ [_89614, _89616] : [-(cUnsatisfiable(_89614)), _89616 = _89614, cUnsatisfiable(_89616)], (232 ^ _82629) ^ [_89909, _89911] : [-(ca(_89909)), _89911 = _89909, ca(_89911)], (242 ^ _82629) ^ [_90204, _90206] : [-(cc(_90204)), _90206 = _90204, cc(_90206)], (252 ^ _82629) ^ [_90499, _90501] : [-(cd(_90499)), _90501 = _90499, cd(_90501)], (262 ^ _82629) ^ [_90794, _90796] : [-(ce(_90794)), _90796 = _90794, ce(_90796)], (272 ^ _82629) ^ [_91089, _91091] : [-(cowlNothing(_91089)), _91091 = _91089, cowlNothing(_91091)], (282 ^ _82629) ^ [_91384, _91386] : [-(cowlThing(_91384)), _91386 = _91384, cowlThing(_91386)], (292 ^ _82629) ^ [_91693, _91695, _91697] : [-(rr(_91695, _91693)), _91697 = _91695, rr(_91697, _91693)], (302 ^ _82629) ^ [_92016, _92018, _92020] : [-(rr(_92016, _92018)), _92020 = _92018, rr(_92016, _92020)], (312 ^ _82629) ^ [_92339, _92341, _92343] : [-(rr1(_92341, _92339)), _92343 = _92341, rr1(_92343, _92339)], (322 ^ _82629) ^ [_92662, _92664, _92666] : [-(rr1(_92662, _92664)), _92666 = _92664, rr1(_92662, _92666)], (332 ^ _82629) ^ [_92985, _92987, _92989] : [-(rr2(_92987, _92985)), _92989 = _92987, rr2(_92989, _92985)], (342 ^ _82629) ^ [_93308, _93310, _93312] : [-(rr2(_93308, _93310)), _93312 = _93310, rr2(_93308, _93312)], (352 ^ _82629) ^ [_93631, _93633, _93635] : [-(rr3(_93633, _93631)), _93635 = _93633, rr3(_93635, _93631)], (362 ^ _82629) ^ [_93954, _93956, _93958] : [-(rr3(_93954, _93956)), _93958 = _93956, rr3(_93954, _93958)], (372 ^ _82629) ^ [_94277, _94279, _94281] : [-(rt1(_94279, _94277)), _94281 = _94279, rt1(_94281, _94277)], (382 ^ _82629) ^ [_94600, _94602, _94604] : [-(rt1(_94600, _94602)), _94604 = _94602, rt1(_94600, _94604)], (392 ^ _82629) ^ [_94923, _94925, _94927] : [-(rt2(_94925, _94923)), _94927 = _94925, rt2(_94927, _94923)], (402 ^ _82629) ^ [_95246, _95248, _95250] : [-(rt2(_95246, _95248)), _95250 = _95248, rt2(_95246, _95250)], (412 ^ _82629) ^ [_95569, _95571, _95573] : [-(rt3(_95571, _95569)), _95573 = _95571, rt3(_95573, _95569)], (422 ^ _82629) ^ [_95892, _95894, _95896] : [-(rt3(_95892, _95894)), _95896 = _95894, rt3(_95892, _95896)], (432 ^ _82629) ^ [_96215, _96217, _96219] : [-(rtt(_96217, _96215)), _96219 = _96217, rtt(_96219, _96215)], (442 ^ _82629) ^ [_96538, _96540, _96542] : [-(rtt(_96538, _96540)), _96542 = _96540, rtt(_96538, _96542)], (452 ^ _82629) ^ [_96847, _96849] : [-(xsd_integer(_96847)), _96849 = _96847, xsd_integer(_96849)], (462 ^ _82629) ^ [_97142, _97144] : [-(xsd_string(_97142)), _97144 = _97142, xsd_string(_97144)], (472 ^ _82629) ^ [_97428] : [-(cowlThing(_97428))], (474 ^ _82629) ^ [_97470] : [cowlNothing(_97470)], (476 ^ _82629) ^ [_97593] : [xsd_string(_97593), xsd_integer(_97593)], (482 ^ _82629) ^ [_97746] : [-(xsd_integer(_97746)), -(xsd_string(_97746))], (488 ^ _82629) ^ [_97966] : [cUnsatisfiable(_97966), 492 ^ _82629 : [(493 ^ _82629) ^ [] : [-(rr(_97966, 491 ^ [_97966]))], (496 ^ _82629) ^ [] : [-(rr(_97966, 494 ^ [_97966]))], (498 ^ _82629) ^ [] : [-(cd(494 ^ [_97966]))], (511 ^ _82629) ^ [] : [-(rr(_97966, 509 ^ [_97966]))], (513 ^ _82629) ^ [] : [-(cc(509 ^ [_97966]))], (500 ^ _82629) ^ [_98484, _98486] : [rr(_97966, _98486), rr(_97966, _98484), -(_98486 = _98484)]]], (515 ^ _82629) ^ [_98929] : [-(cUnsatisfiable(_98929)), 518 ^ _82629 : [(519 ^ _82629) ^ [_99092] : [rr(_98929, _99092)]], 522 ^ _82629 : [(523 ^ _82629) ^ [_99199] : [rr(_98929, _99199), cd(_99199)]], 532 ^ _82629 : [(533 ^ _82629) ^ [] : [-(rr(_98929, 530 ^ [_98929]))], (535 ^ _82629) ^ [] : [-(rr(_98929, 531 ^ [_98929]))], (537 ^ _82629) ^ [] : [530 ^ [_98929] = 531 ^ [_98929]]], 538 ^ _82629 : [(539 ^ _82629) ^ [_99726] : [rr(_98929, _99726), cc(_99726)]]], (557 ^ _82629) ^ [_100251] : [558 ^ _82629 : [(559 ^ _82629) ^ [] : [cd(_100251)], (561 ^ _82629) ^ [] : [cc(_100251)]], -(ca(_100251))], (547 ^ _82629) ^ [_100015] : [ca(_100015), -(cd(_100015)), -(cc(_100015))], (565 ^ _82629) ^ [] : [-(cUnsatisfiable(i2003_11_14_17_20_21603))], (567 ^ _82629) ^ [_100562] : [cd(_100562), ce(_100562)], (573 ^ _82629) ^ [_100747] : [cd(_100747), cc(_100747)], (579 ^ _82629) ^ [_100932] : [ce(_100932), cc(_100932)], (585 ^ _82629) ^ [_101131, _101133] : [rt3(_101133, _101131), -(rtt(_101133, _101131))], (591 ^ _82629) ^ [_101341, _101343] : [rr1(_101343, _101341), -(rr(_101343, _101341))], (597 ^ _82629) ^ [_101551, _101553] : [rr3(_101553, _101551), -(rr(_101553, _101551))], (603 ^ _82629) ^ [_101761, _101763] : [rt1(_101763, _101761), -(rtt(_101763, _101761))], (609 ^ _82629) ^ [_101971, _101973] : [rr2(_101973, _101971), -(rr(_101973, _101971))], (615 ^ _82629) ^ [_102161, _102163] : [rt2(_102163, _102161), -(rtt(_102163, _102161))]], input).
% 0.36/1.37 ncf('1',plain,[cd(494 ^ [i2003_11_14_17_20_21603]), cc(494 ^ [i2003_11_14_17_20_21603])],start(573 ^ 0,bind([[_100747], [494 ^ [i2003_11_14_17_20_21603]]]))).
% 0.36/1.37 ncf('1.1',plain,[-(cd(494 ^ [i2003_11_14_17_20_21603])), cUnsatisfiable(i2003_11_14_17_20_21603)],extension(488 ^ 1,bind([[_97966], [i2003_11_14_17_20_21603]]))).
% 0.36/1.37 ncf('1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_20_21603))],extension(565 ^ 2)).
% 0.36/1.37 ncf('1.2',plain,[-(cc(494 ^ [i2003_11_14_17_20_21603])), ca(494 ^ [i2003_11_14_17_20_21603]), -(cd(494 ^ [i2003_11_14_17_20_21603]))],extension(547 ^ 1,bind([[_100015], [494 ^ [i2003_11_14_17_20_21603]]]))).
% 0.36/1.37 ncf('1.2.1',plain,[-(ca(494 ^ [i2003_11_14_17_20_21603])), 559 : cd(494 ^ [i2003_11_14_17_20_21603])],extension(557 ^ 2,bind([[_100251], [494 ^ [i2003_11_14_17_20_21603]]]))).
% 0.36/1.37 ncf('1.2.1.1',plain,[-(cd(494 ^ [i2003_11_14_17_20_21603]))],lemmata('x')).
% 0.36/1.37 ncf('1.2.2',plain,[cd(494 ^ [i2003_11_14_17_20_21603]), -(cd(509 ^ [i2003_11_14_17_20_21603])), 494 ^ [i2003_11_14_17_20_21603] = 509 ^ [i2003_11_14_17_20_21603]],extension(80 ^ 2,bind([[_85127, _85129], [509 ^ [i2003_11_14_17_20_21603], 494 ^ [i2003_11_14_17_20_21603]]]))).
% 0.36/1.37 ncf('1.2.2.1',plain,[cd(509 ^ [i2003_11_14_17_20_21603]), cc(509 ^ [i2003_11_14_17_20_21603])],extension(573 ^ 3,bind([[_100747], [509 ^ [i2003_11_14_17_20_21603]]]))).
% 0.36/1.37 ncf('1.2.2.1.1',plain,[-(cc(509 ^ [i2003_11_14_17_20_21603])), cUnsatisfiable(i2003_11_14_17_20_21603)],extension(488 ^ 4,bind([[_97966], [i2003_11_14_17_20_21603]]))).
% 0.36/1.37 ncf('1.2.2.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_20_21603))],extension(565 ^ 5)).
% 0.36/1.37 ncf('1.2.2.2',plain,[-(494 ^ [i2003_11_14_17_20_21603] = 509 ^ [i2003_11_14_17_20_21603]), 500 : rr(i2003_11_14_17_20_21603, 494 ^ [i2003_11_14_17_20_21603]), 500 : rr(i2003_11_14_17_20_21603, 509 ^ [i2003_11_14_17_20_21603]), 500 : cUnsatisfiable(i2003_11_14_17_20_21603)],extension(488 ^ 3,bind([[_97966, _98484, _98486], [i2003_11_14_17_20_21603, 509 ^ [i2003_11_14_17_20_21603], 494 ^ [i2003_11_14_17_20_21603]]]))).
% 0.36/1.37 ncf('1.2.2.2.1',plain,[-(rr(i2003_11_14_17_20_21603, 494 ^ [i2003_11_14_17_20_21603]))],extension(496 ^ 6)).
% 0.36/1.37 ncf('1.2.2.2.2',plain,[-(rr(i2003_11_14_17_20_21603, 509 ^ [i2003_11_14_17_20_21603]))],extension(511 ^ 6)).
% 0.36/1.37 ncf('1.2.2.2.3',plain,[-(cUnsatisfiable(i2003_11_14_17_20_21603))],extension(565 ^ 4)).
% 0.36/1.37 %-----------------------------------------------------
% 0.36/1.37 End of proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------