%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS122+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n003.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:19 EDT 2023
% Result : Unsatisfiable 0.37s 1.38s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS122+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.14/0.34 % Computer : n003.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 18 23:04:15 EDT 2023
% 0.14/0.34 % CPUTime :
% 0.37/1.38
% 0.37/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is Unsatisfiable
% 0.37/1.38 Start of proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/1.38 %-----------------------------------------------------
% 0.37/1.38 ncf(matrix, plain, [(2 ^ _71364) ^ [_71468] : [-(_71468 = _71468)], (4 ^ _71364) ^ [_71575, _71577] : [_71577 = _71575, -(_71575 = _71577)], (10 ^ _71364) ^ [_71779, _71781, _71783] : [-(_71783 = _71779), _71783 = _71781, _71781 = _71779], (20 ^ _71364) ^ [_72092, _72094] : [-(cowlThing(_72092)), _72094 = _72092, cowlThing(_72094)], (30 ^ _71364) ^ [_72387, _72389] : [-(cowlNothing(_72387)), _72389 = _72387, cowlNothing(_72389)], (40 ^ _71364) ^ [_72682, _72684] : [-(xsd_string(_72682)), _72684 = _72682, xsd_string(_72684)], (50 ^ _71364) ^ [_72977, _72979] : [-(xsd_integer(_72977)), _72979 = _72977, xsd_integer(_72979)], (60 ^ _71364) ^ [_73300, _73302, _73304, _73306] : [-(ra_Px1(_73304, _73300)), ra_Px1(_73306, _73302), _73306 = _73304, _73302 = _73300], (74 ^ _71364) ^ [_73716, _73718] : [-(ca_Ax2(_73716)), _73718 = _73716, ca_Ax2(_73718)], (84 ^ _71364) ^ [_74011, _74013] : [-(cp1(_74011)), _74013 = _74011, cp1(_74013)], (94 ^ _71364) ^ [_74306, _74308] : [-(ca_Vx3(_74306)), _74308 = _74306, ca_Vx3(_74308)], (104 ^ _71364) ^ [_74601, _74603] : [-(cp1xcomp(_74601)), _74603 = _74601, cp1xcomp(_74603)], (114 ^ _71364) ^ [_74924, _74926, _74928, _74930] : [-(rinvF(_74928, _74924)), rinvF(_74930, _74926), _74930 = _74928, _74926 = _74924], (128 ^ _71364) ^ [_75368, _75370, _75372, _75374] : [-(rf(_75372, _75368)), rf(_75374, _75370), _75374 = _75372, _75370 = _75368], (142 ^ _71364) ^ [_75812, _75814, _75816, _75818] : [-(rinvR(_75816, _75812)), rinvR(_75818, _75814), _75818 = _75816, _75814 = _75812], (170 ^ _71364) ^ [_76652, _76654] : [-(cUnsatisfiable(_76652)), _76654 = _76652, cUnsatisfiable(_76654)], (156 ^ _71364) ^ [_76256, _76258, _76260, _76262] : [-(rr(_76260, _76256)), rr(_76262, _76258), _76262 = _76260, _76258 = _76256], (180 ^ _71364) ^ [_76979, _76981] : [-(cUnsatisfiable(_76979)), _76981 = _76979, cUnsatisfiable(_76981)], (190 ^ _71364) ^ [_77274, _77276] : [-(ca_Ax2(_77274)), _77276 = _77274, ca_Ax2(_77276)], (200 ^ _71364) ^ [_77569, _77571] : [-(ca_Vx3(_77569)), _77571 = _77569, ca_Vx3(_77571)], (210 ^ _71364) ^ [_77864, _77866] : [-(cowlNothing(_77864)), _77866 = _77864, cowlNothing(_77866)], (220 ^ _71364) ^ [_78159, _78161] : [-(cowlThing(_78159)), _78161 = _78159, cowlThing(_78161)], (230 ^ _71364) ^ [_78454, _78456] : [-(cp1(_78454)), _78456 = _78454, cp1(_78456)], (240 ^ _71364) ^ [_78749, _78751] : [-(cp1xcomp(_78749)), _78751 = _78749, cp1xcomp(_78751)], (250 ^ _71364) ^ [_79058, _79060, _79062] : [-(ra_Px1(_79060, _79058)), _79062 = _79060, ra_Px1(_79062, _79058)], (260 ^ _71364) ^ [_79381, _79383, _79385] : [-(ra_Px1(_79381, _79383)), _79385 = _79383, ra_Px1(_79381, _79385)], (270 ^ _71364) ^ [_79704, _79706, _79708] : [-(rf(_79706, _79704)), _79708 = _79706, rf(_79708, _79704)], (280 ^ _71364) ^ [_80027, _80029, _80031] : [-(rf(_80027, _80029)), _80031 = _80029, rf(_80027, _80031)], (290 ^ _71364) ^ [_80350, _80352, _80354] : [-(rinvF(_80352, _80350)), _80354 = _80352, rinvF(_80354, _80350)], (300 ^ _71364) ^ [_80673, _80675, _80677] : [-(rinvF(_80673, _80675)), _80677 = _80675, rinvF(_80673, _80677)], (310 ^ _71364) ^ [_80996, _80998, _81000] : [-(rinvR(_80998, _80996)), _81000 = _80998, rinvR(_81000, _80996)], (320 ^ _71364) ^ [_81319, _81321, _81323] : [-(rinvR(_81319, _81321)), _81323 = _81321, rinvR(_81319, _81323)], (330 ^ _71364) ^ [_81642, _81644, _81646] : [-(rr(_81644, _81642)), _81646 = _81644, rr(_81646, _81642)], (340 ^ _71364) ^ [_81965, _81967, _81969] : [-(rr(_81965, _81967)), _81969 = _81967, rr(_81965, _81969)], (350 ^ _71364) ^ [_82274, _82276] : [-(xsd_integer(_82274)), _82276 = _82274, xsd_integer(_82276)], (360 ^ _71364) ^ [_82569, _82571] : [-(xsd_string(_82569)), _82571 = _82569, xsd_string(_82571)], (370 ^ _71364) ^ [_82855] : [-(cowlThing(_82855))], (372 ^ _71364) ^ [_82897] : [cowlNothing(_82897)], (374 ^ _71364) ^ [_83020] : [xsd_string(_83020), xsd_integer(_83020)], (380 ^ _71364) ^ [_83173] : [-(xsd_integer(_83173)), -(xsd_string(_83173))], (386 ^ _71364) ^ [_83393] : [cUnsatisfiable(_83393), 390 ^ _71364 : [(391 ^ _71364) ^ [] : [-(rf(_83393, 389 ^ [_83393]))], (393 ^ _71364) ^ [] : [-(ca_Ax2(389 ^ [_83393]))]]], (395 ^ _71364) ^ [_83679] : [-(cUnsatisfiable(_83679)), 396 ^ _71364 : [(397 ^ _71364) ^ [_83767] : [rf(_83679, _83767), ca_Ax2(_83767)]]], (405 ^ _71364) ^ [_84041] : [cp1(_84041), 408 ^ _71364 : [(409 ^ _71364) ^ [_84152] : [ra_Px1(_84041, _84152)]]], (411 ^ _71364) ^ [_84218] : [-(ra_Px1(_84218, 412 ^ [_84218])), -(cp1(_84218))], (418 ^ _71364) ^ [_84491] : [cp1xcomp(_84491), -(ra_Px1(_84491, 421 ^ [_84491]))], (425 ^ _71364) ^ [_84696] : [426 ^ _71364 : [(427 ^ _71364) ^ [_84763] : [ra_Px1(_84696, _84763)]], -(cp1xcomp(_84696))], (431 ^ _71364) ^ [_84937] : [ca_Ax2(_84937), 434 ^ _71364 : [(435 ^ _71364) ^ [] : [-(cp1(_84937))], (437 ^ _71364) ^ [_85135] : [rinvF(_84937, _85135), -(ca_Vx3(_85135))]]], (443 ^ _71364) ^ [_85304] : [-(ca_Ax2(_85304)), cp1(_85304), 449 ^ _71364 : [(450 ^ _71364) ^ [] : [-(rinvF(_85304, 448 ^ [_85304]))], (452 ^ _71364) ^ [] : [ca_Vx3(448 ^ [_85304])]]], (456 ^ _71364) ^ [_85738] : [ca_Vx3(_85738), 460 ^ _71364 : [(461 ^ _71364) ^ [] : [-(rf(_85738, 459 ^ [_85738]))], (463 ^ _71364) ^ [] : [-(cp1xcomp(459 ^ [_85738]))]]], (465 ^ _71364) ^ [_86024] : [-(ca_Vx3(_86024)), 466 ^ _71364 : [(467 ^ _71364) ^ [_86112] : [rf(_86024, _86112), cp1xcomp(_86112)]]], (475 ^ _71364) ^ [_86385, _86387, _86389] : [-(_86387 = _86385), rf(_86389, _86387), rf(_86389, _86385)], (485 ^ _71364) ^ [_86723, _86725] : [rinvF(_86725, _86723), -(rf(_86723, _86725))], (491 ^ _71364) ^ [_86885, _86887] : [rf(_86885, _86887), -(rinvF(_86887, _86885))], (519 ^ _71364) ^ [] : [-(cUnsatisfiable(i2003_11_14_17_21_55116))], (509 ^ _71364) ^ [_87514, _87516, _87518] : [-(rr(_87518, _87514)), rr(_87518, _87516), rr(_87516, _87514)], (497 ^ _71364) ^ [_87126, _87128] : [rinvR(_87128, _87126), -(rr(_87126, _87128))], (503 ^ _71364) ^ [_87288, _87290] : [rr(_87288, _87290), -(rinvR(_87290, _87288))]], input).
% 0.37/1.38 ncf('1',plain,[cp1(389 ^ [i2003_11_14_17_21_55116]), 409 : ra_Px1(389 ^ [i2003_11_14_17_21_55116], 421 ^ [459 ^ [i2003_11_14_17_21_55116]])],start(405 ^ 0,bind([[_84041, _84152], [389 ^ [i2003_11_14_17_21_55116], 421 ^ [459 ^ [i2003_11_14_17_21_55116]]]]))).
% 0.37/1.38 ncf('1.1',plain,[-(cp1(389 ^ [i2003_11_14_17_21_55116])), -(ra_Px1(389 ^ [i2003_11_14_17_21_55116], 412 ^ [389 ^ [i2003_11_14_17_21_55116]]))],extension(411 ^ 1,bind([[_84218], [389 ^ [i2003_11_14_17_21_55116]]]))).
% 0.37/1.38 ncf('1.1.1',plain,[ra_Px1(389 ^ [i2003_11_14_17_21_55116], 412 ^ [389 ^ [i2003_11_14_17_21_55116]]), -(ra_Px1(389 ^ [i2003_11_14_17_21_55116], 412 ^ [389 ^ [i2003_11_14_17_21_55116]])), 389 ^ [i2003_11_14_17_21_55116] = 389 ^ [i2003_11_14_17_21_55116], 412 ^ [389 ^ [i2003_11_14_17_21_55116]] = 412 ^ [389 ^ [i2003_11_14_17_21_55116]]],extension(60 ^ 2,bind([[_73300, _73302, _73304, _73306], [412 ^ [389 ^ [i2003_11_14_17_21_55116]], 412 ^ [389 ^ [i2003_11_14_17_21_55116]], 389 ^ [i2003_11_14_17_21_55116], 389 ^ [i2003_11_14_17_21_55116]]]))).
% 0.37/1.38 ncf('1.1.1.1',plain,[ra_Px1(389 ^ [i2003_11_14_17_21_55116], 412 ^ [389 ^ [i2003_11_14_17_21_55116]]), -(ra_Px1(389 ^ [i2003_11_14_17_21_55116], 412 ^ [389 ^ [i2003_11_14_17_21_55116]])), 389 ^ [i2003_11_14_17_21_55116] = 389 ^ [i2003_11_14_17_21_55116], 412 ^ [389 ^ [i2003_11_14_17_21_55116]] = 412 ^ [389 ^ [i2003_11_14_17_21_55116]]],extension(60 ^ 3,bind([[_73300, _73302, _73304, _73306], [412 ^ [389 ^ [i2003_11_14_17_21_55116]], 412 ^ [389 ^ [i2003_11_14_17_21_55116]], 389 ^ [i2003_11_14_17_21_55116], 389 ^ [i2003_11_14_17_21_55116]]]))).
% 0.37/1.38 ncf('1.1.1.1.1',plain,[ra_Px1(389 ^ [i2003_11_14_17_21_55116], 412 ^ [389 ^ [i2003_11_14_17_21_55116]]), cp1(389 ^ [i2003_11_14_17_21_55116])],extension(405 ^ 4,bind([[_84041, _84152], [389 ^ [i2003_11_14_17_21_55116], 412 ^ [389 ^ [i2003_11_14_17_21_55116]]]]))).
% 0.37/1.38 ncf('1.1.1.1.1.1',plain,[-(cp1(389 ^ [i2003_11_14_17_21_55116])), ca_Ax2(389 ^ [i2003_11_14_17_21_55116])],extension(431 ^ 5,bind([[_84937], [389 ^ [i2003_11_14_17_21_55116]]]))).
% 0.37/1.38 ncf('1.1.1.1.1.1.1',plain,[-(ca_Ax2(389 ^ [i2003_11_14_17_21_55116])), cUnsatisfiable(i2003_11_14_17_21_55116)],extension(386 ^ 6,bind([[_83393], [i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.1.1.1.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_55116))],extension(519 ^ 7)).
% 0.37/1.38 ncf('1.1.1.1.2',plain,[-(389 ^ [i2003_11_14_17_21_55116] = 389 ^ [i2003_11_14_17_21_55116])],extension(2 ^ 4,bind([[_71468], [389 ^ [i2003_11_14_17_21_55116]]]))).
% 0.37/1.38 ncf('1.1.1.1.3',plain,[-(412 ^ [389 ^ [i2003_11_14_17_21_55116]] = 412 ^ [389 ^ [i2003_11_14_17_21_55116]])],extension(2 ^ 4,bind([[_71468], [412 ^ [389 ^ [i2003_11_14_17_21_55116]]]]))).
% 0.37/1.38 ncf('1.1.1.2',plain,[-(389 ^ [i2003_11_14_17_21_55116] = 389 ^ [i2003_11_14_17_21_55116])],extension(2 ^ 3,bind([[_71468], [389 ^ [i2003_11_14_17_21_55116]]]))).
% 0.37/1.38 ncf('1.1.1.3',plain,[-(412 ^ [389 ^ [i2003_11_14_17_21_55116]] = 412 ^ [389 ^ [i2003_11_14_17_21_55116]])],extension(2 ^ 3,bind([[_71468], [412 ^ [389 ^ [i2003_11_14_17_21_55116]]]]))).
% 0.37/1.38 ncf('1.2',plain,[-(ra_Px1(389 ^ [i2003_11_14_17_21_55116], 421 ^ [459 ^ [i2003_11_14_17_21_55116]])), ra_Px1(459 ^ [i2003_11_14_17_21_55116], 421 ^ [459 ^ [i2003_11_14_17_21_55116]]), 459 ^ [i2003_11_14_17_21_55116] = 389 ^ [i2003_11_14_17_21_55116], 421 ^ [459 ^ [i2003_11_14_17_21_55116]] = 421 ^ [459 ^ [i2003_11_14_17_21_55116]]],extension(60 ^ 3,bind([[_73300, _73302, _73304, _73306], [421 ^ [459 ^ [i2003_11_14_17_21_55116]], 421 ^ [459 ^ [i2003_11_14_17_21_55116]], 389 ^ [i2003_11_14_17_21_55116], 459 ^ [i2003_11_14_17_21_55116]]]))).
% 0.37/1.38 ncf('1.2.1',plain,[-(ra_Px1(459 ^ [i2003_11_14_17_21_55116], 421 ^ [459 ^ [i2003_11_14_17_21_55116]])), cp1xcomp(459 ^ [i2003_11_14_17_21_55116])],extension(418 ^ 4,bind([[_84491], [459 ^ [i2003_11_14_17_21_55116]]]))).
% 0.37/1.38 ncf('1.2.1.1',plain,[-(cp1xcomp(459 ^ [i2003_11_14_17_21_55116])), ca_Vx3(i2003_11_14_17_21_55116)],extension(456 ^ 5,bind([[_85738], [i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.2.1.1.1',plain,[-(ca_Vx3(i2003_11_14_17_21_55116)), 437 : rinvF(389 ^ [i2003_11_14_17_21_55116], i2003_11_14_17_21_55116), 437 : ca_Ax2(389 ^ [i2003_11_14_17_21_55116])],extension(431 ^ 6,bind([[_84937, _85135], [389 ^ [i2003_11_14_17_21_55116], i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.2.1.1.1.1',plain,[-(rinvF(389 ^ [i2003_11_14_17_21_55116], i2003_11_14_17_21_55116)), rf(i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116])],extension(491 ^ 9,bind([[_86885, _86887], [i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116]]]))).
% 0.37/1.38 ncf('1.2.1.1.1.1.1',plain,[-(rf(i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116])), cUnsatisfiable(i2003_11_14_17_21_55116)],extension(386 ^ 10,bind([[_83393], [i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.2.1.1.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_55116))],extension(519 ^ 11)).
% 0.37/1.38 ncf('1.2.1.1.1.2',plain,[-(ca_Ax2(389 ^ [i2003_11_14_17_21_55116])), cUnsatisfiable(i2003_11_14_17_21_55116)],extension(386 ^ 7,bind([[_83393], [i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.2.1.1.1.2.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_55116))],extension(519 ^ 8)).
% 0.37/1.38 ncf('1.2.2',plain,[-(459 ^ [i2003_11_14_17_21_55116] = 389 ^ [i2003_11_14_17_21_55116]), rf(i2003_11_14_17_21_55116, 459 ^ [i2003_11_14_17_21_55116]), rf(i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116])],extension(475 ^ 4,bind([[_86385, _86387, _86389], [389 ^ [i2003_11_14_17_21_55116], 459 ^ [i2003_11_14_17_21_55116], i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.2.2.1',plain,[-(rf(i2003_11_14_17_21_55116, 459 ^ [i2003_11_14_17_21_55116])), ca_Vx3(i2003_11_14_17_21_55116)],extension(456 ^ 5,bind([[_85738], [i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.2.2.1.1',plain,[-(ca_Vx3(i2003_11_14_17_21_55116)), 437 : rinvF(389 ^ [i2003_11_14_17_21_55116], i2003_11_14_17_21_55116), 437 : ca_Ax2(389 ^ [i2003_11_14_17_21_55116])],extension(431 ^ 6,bind([[_84937, _85135], [389 ^ [i2003_11_14_17_21_55116], i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.2.2.1.1.1',plain,[-(rinvF(389 ^ [i2003_11_14_17_21_55116], i2003_11_14_17_21_55116)), rf(i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116])],extension(491 ^ 9,bind([[_86885, _86887], [i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116]]]))).
% 0.37/1.38 ncf('1.2.2.1.1.1.1',plain,[-(rf(i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116])), cUnsatisfiable(i2003_11_14_17_21_55116)],extension(386 ^ 10,bind([[_83393], [i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.2.2.1.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_55116))],extension(519 ^ 11)).
% 0.37/1.38 ncf('1.2.2.1.1.2',plain,[-(ca_Ax2(389 ^ [i2003_11_14_17_21_55116])), cUnsatisfiable(i2003_11_14_17_21_55116)],extension(386 ^ 7,bind([[_83393], [i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.2.2.1.1.2.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_55116))],extension(519 ^ 8)).
% 0.37/1.38 ncf('1.2.2.2',plain,[-(rf(i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116])), rf(i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116]), i2003_11_14_17_21_55116 = i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116] = 389 ^ [i2003_11_14_17_21_55116]],extension(128 ^ 5,bind([[_75368, _75370, _75372, _75374], [389 ^ [i2003_11_14_17_21_55116], 389 ^ [i2003_11_14_17_21_55116], i2003_11_14_17_21_55116, i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.2.2.2.1',plain,[-(rf(i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116])), rf(i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116]), i2003_11_14_17_21_55116 = i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116] = 389 ^ [i2003_11_14_17_21_55116]],extension(128 ^ 6,bind([[_75368, _75370, _75372, _75374], [389 ^ [i2003_11_14_17_21_55116], 389 ^ [i2003_11_14_17_21_55116], i2003_11_14_17_21_55116, i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.2.2.2.1.1',plain,[-(rf(i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116])), rf(i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116]), i2003_11_14_17_21_55116 = i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116] = 389 ^ [i2003_11_14_17_21_55116]],extension(128 ^ 7,bind([[_75368, _75370, _75372, _75374], [389 ^ [i2003_11_14_17_21_55116], 389 ^ [i2003_11_14_17_21_55116], i2003_11_14_17_21_55116, i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.2.2.2.1.1.1',plain,[-(rf(i2003_11_14_17_21_55116, 389 ^ [i2003_11_14_17_21_55116])), cUnsatisfiable(i2003_11_14_17_21_55116)],extension(386 ^ 8,bind([[_83393], [i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.2.2.2.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_55116))],extension(519 ^ 9)).
% 0.37/1.38 ncf('1.2.2.2.1.1.2',plain,[-(i2003_11_14_17_21_55116 = i2003_11_14_17_21_55116)],extension(2 ^ 8,bind([[_71468], [i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.2.2.2.1.1.3',plain,[-(389 ^ [i2003_11_14_17_21_55116] = 389 ^ [i2003_11_14_17_21_55116])],extension(2 ^ 8,bind([[_71468], [389 ^ [i2003_11_14_17_21_55116]]]))).
% 0.37/1.38 ncf('1.2.2.2.1.2',plain,[-(i2003_11_14_17_21_55116 = i2003_11_14_17_21_55116)],extension(2 ^ 7,bind([[_71468], [i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.2.2.2.1.3',plain,[-(389 ^ [i2003_11_14_17_21_55116] = 389 ^ [i2003_11_14_17_21_55116])],extension(2 ^ 7,bind([[_71468], [389 ^ [i2003_11_14_17_21_55116]]]))).
% 0.37/1.38 ncf('1.2.2.2.2',plain,[-(i2003_11_14_17_21_55116 = i2003_11_14_17_21_55116)],extension(2 ^ 6,bind([[_71468], [i2003_11_14_17_21_55116]]))).
% 0.37/1.38 ncf('1.2.2.2.3',plain,[-(389 ^ [i2003_11_14_17_21_55116] = 389 ^ [i2003_11_14_17_21_55116])],extension(2 ^ 6,bind([[_71468], [389 ^ [i2003_11_14_17_21_55116]]]))).
% 0.37/1.38 ncf('1.2.3',plain,[-(421 ^ [459 ^ [i2003_11_14_17_21_55116]] = 421 ^ [459 ^ [i2003_11_14_17_21_55116]])],extension(2 ^ 4,bind([[_71468], [421 ^ [459 ^ [i2003_11_14_17_21_55116]]]]))).
% 0.37/1.38 %-----------------------------------------------------
% 0.37/1.38 End of proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------