%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS109+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:17 EDT 2023
% Result : Unsatisfiable 56.55s 55.29s
% Output : Proof 56.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS109+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n017.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 22:30:15 EDT 2023
% 0.13/0.33 % CPUTime :
% 56.55/55.29
% 56.55/55.29 /export/starexec/sandbox/benchmark/theBenchmark.p is Unsatisfiable
% 56.55/55.29 Start of proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
% 56.55/55.29 %-----------------------------------------------------
% 56.55/55.29 ncf(matrix, plain, [(238 ^ _99260) ^ [_100238, _100240] : [-(cowlNothing(_100238)), _100240 = _100238, cowlNothing(_100240)], (442 ^ _99260) ^ [_106686] : [xsd_string(_106686), xsd_integer(_106686)], (378 ^ _99260) ^ [_104662, _104664, _104666] : [-(rinvS(_104664, _104662)), _104666 = _104664, rinvS(_104666, _104662)], (318 ^ _99260) ^ [_102724, _102726, _102728] : [-(rf1(_102726, _102724)), _102728 = _102726, rf1(_102728, _102724)], (485 ^ _99260) ^ [_108037] : [-(ra_Px1(_108037, 486 ^ [_108037])), -(cp(_108037))], (594 ^ _99260) ^ [_111708, _111710] : [rf1(_111708, _111710), -(rinvF1(_111710, _111708))], (546 ^ _99260) ^ [_110121] : [-(ca_Vx3(_110121)), 547 ^ _99260 : [(548 ^ _99260) ^ [_110209] : [rs(_110121, _110209), cp(_110209)]]], (505 ^ _99260) ^ [_108756] : [ca_Ax2(_108756), 508 ^ _99260 : [(515 ^ _99260) ^ [_109098] : [rinvF(_108756, _109098), -(ca_Vx3(_109098))], (509 ^ _99260) ^ [_108922] : [rinvS(_108756, _108922), -(cp(_108922))]]], (328 ^ _99260) ^ [_103047, _103049, _103051] : [-(rf1(_103047, _103049)), _103051 = _103049, rf1(_103047, _103051)], (418 ^ _99260) ^ [_105940, _105942] : [-(xsd_integer(_105940)), _105942 = _105940, xsd_integer(_105942)], (438 ^ _99260) ^ [_106521] : [-(cowlThing(_106521))], (576 ^ _99260) ^ [_111143, _111145] : [rinvF(_111145, _111143), -(rf(_111143, _111145))], (440 ^ _99260) ^ [_106563] : [cowlNothing(_106563)], (479 ^ _99260) ^ [_107860] : [cp(_107860), 482 ^ _99260 : [(483 ^ _99260) ^ [_107971] : [ra_Px1(_107860, _107971)]]], (428 ^ _99260) ^ [_106235, _106237] : [-(xsd_string(_106235)), _106237 = _106235, xsd_string(_106237)], (408 ^ _99260) ^ [_105631, _105633, _105635] : [-(rs(_105631, _105633)), _105635 = _105633, rs(_105631, _105635)], (537 ^ _99260) ^ [_109835] : [ca_Vx3(_109835), 541 ^ _99260 : [(544 ^ _99260) ^ [] : [-(cp(540 ^ [_109835]))], (542 ^ _99260) ^ [] : [-(rs(_109835, 540 ^ [_109835]))]]], (368 ^ _99260) ^ [_104339, _104341, _104343] : [-(rinvF1(_104339, _104341)), _104343 = _104341, rinvF1(_104339, _104343)], (606 ^ _99260) ^ [_112111, _112113] : [rs(_112111, _112113), -(rinvS(_112113, _112111))], (612 ^ _99260) ^ [_112337, _112339, _112341] : [-(_112339 = _112337), rs(_112341, _112339), rs(_112341, _112337)], (492 ^ _99260) ^ [_108310] : [cpxcomp(_108310), -(ra_Px1(_108310, 495 ^ [_108310]))], (278 ^ _99260) ^ [_101432, _101434, _101436] : [-(ra_Px1(_101434, _101432)), _101436 = _101434, ra_Px1(_101436, _101432)], (298 ^ _99260) ^ [_102078, _102080, _102082] : [-(rf(_102080, _102078)), _102082 = _102080, rf(_102082, _102078)], (600 ^ _99260) ^ [_111949, _111951] : [rinvS(_111951, _111949), -(rs(_111949, _111951))], (268 ^ _99260) ^ [_101123, _101125] : [-(cpxcomp(_101123)), _101125 = _101123, cpxcomp(_101125)], (388 ^ _99260) ^ [_104985, _104987, _104989] : [-(rinvS(_104985, _104987)), _104989 = _104987, rinvS(_104985, _104989)], (348 ^ _99260) ^ [_103693, _103695, _103697] : [-(rinvF(_103693, _103695)), _103697 = _103695, rinvF(_103693, _103697)], (622 ^ _99260) ^ [] : [-(cUnsatisfiable(i2003_11_14_17_21_08508))], (288 ^ _99260) ^ [_101755, _101757, _101759] : [-(ra_Px1(_101755, _101757)), _101759 = _101757, ra_Px1(_101755, _101759)], (228 ^ _99260) ^ [_99943, _99945] : [-(ca_Vx3(_99943)), _99945 = _99943, ca_Vx3(_99945)], (588 ^ _99260) ^ [_111546, _111548] : [rinvF1(_111548, _111546), -(rf1(_111546, _111548))], (630 ^ _99260) ^ [_112889, _112891] : [rs(_112891, _112889), -(rf1(_112891, _112889))], (465 ^ _99260) ^ [_107415] : [-(cUnsatisfiable(_107415)), cpxcomp(_107415), 470 ^ _99260 : [(471 ^ _99260) ^ [_107582] : [rf(_107415, _107582), ca_Ax2(_107582)]]], (448 ^ _99260) ^ [_106839] : [-(xsd_integer(_106839)), -(xsd_string(_106839))], (556 ^ _99260) ^ [_110482, _110484, _110486] : [-(_110484 = _110482), rf(_110486, _110484), rf(_110486, _110482)], (454 ^ _99260) ^ [_107059] : [cUnsatisfiable(_107059), 457 ^ _99260 : [(463 ^ _99260) ^ [] : [-(ca_Ax2(459 ^ [_107059]))], (461 ^ _99260) ^ [] : [-(rf(_107059, 459 ^ [_107059]))], (458 ^ _99260) ^ [] : [-(cpxcomp(_107059))]]], (258 ^ _99260) ^ [_100828, _100830] : [-(cp(_100828)), _100830 = _100828, cp(_100830)], (248 ^ _99260) ^ [_100533, _100535] : [-(cowlThing(_100533)), _100535 = _100533, cowlThing(_100535)], (499 ^ _99260) ^ [_108515] : [500 ^ _99260 : [(501 ^ _99260) ^ [_108582] : [ra_Px1(_108515, _108582)]], -(cpxcomp(_108515))], (566 ^ _99260) ^ [_110805, _110807, _110809] : [-(_110807 = _110805), rf1(_110809, _110807), rf1(_110809, _110805)], (338 ^ _99260) ^ [_103370, _103372, _103374] : [-(rinvF(_103372, _103370)), _103374 = _103372, rinvF(_103374, _103370)], (624 ^ _99260) ^ [_112699, _112701] : [rs(_112701, _112699), -(rf(_112701, _112699))], (358 ^ _99260) ^ [_104016, _104018, _104020] : [-(rinvF1(_104018, _104016)), _104020 = _104018, rinvF1(_104020, _104016)], (218 ^ _99260) ^ [_99648, _99650] : [-(ca_Ax2(_99648)), _99650 = _99648, ca_Ax2(_99650)], (308 ^ _99260) ^ [_102401, _102403, _102405] : [-(rf(_102401, _102403)), _102405 = _102403, rf(_102401, _102405)], (398 ^ _99260) ^ [_105308, _105310, _105312] : [-(rs(_105310, _105308)), _105312 = _105310, rs(_105312, _105308)], (582 ^ _99260) ^ [_111305, _111307] : [rf(_111305, _111307), -(rinvF(_111307, _111305))], (521 ^ _99260) ^ [_109267] : [-(ca_Ax2(_109267)), 525 ^ _99260 : [(528 ^ _99260) ^ [] : [cp(524 ^ [_109267])], (526 ^ _99260) ^ [] : [-(rinvS(_109267, 524 ^ [_109267]))]], 530 ^ _99260 : [(533 ^ _99260) ^ [] : [ca_Vx3(529 ^ [_109267])], (531 ^ _99260) ^ [] : [-(rinvF(_109267, 529 ^ [_109267]))]]], (208 ^ _99260) ^ [_99353, _99355] : [-(cUnsatisfiable(_99353)), _99355 = _99353, cUnsatisfiable(_99355)], !, (104 ^ _92866) ^ [_96083, _96085] : [-(cp(_96083)), _96085 = _96083, cp(_96085)], (40 ^ _92866) ^ [_94164, _94166] : [-(xsd_string(_94164)), _94166 = _94164, xsd_string(_94166)], (166 ^ _92866) ^ [_98033, _98035, _98037, _98039] : [-(rf(_98037, _98033)), rf(_98039, _98035), _98039 = _98037, _98035 = _98033], (70 ^ _92866) ^ [_95077, _95079, _95081, _95083] : [-(ra_Px1(_95081, _95077)), ra_Px1(_95083, _95079), _95083 = _95081, _95079 = _95077], (84 ^ _92866) ^ [_95493, _95495] : [-(ca_Ax2(_95493)), _95495 = _95493, ca_Ax2(_95495)], (2 ^ _92866) ^ [_92950] : [-(_92950 = _92950)], (20 ^ _92866) ^ [_93574, _93576] : [-(cowlThing(_93574)), _93576 = _93574, cowlThing(_93576)], (60 ^ _92866) ^ [_94754, _94756] : [-(cpxcomp(_94754)), _94756 = _94754, cpxcomp(_94756)], (30 ^ _92866) ^ [_93869, _93871] : [-(cowlNothing(_93869)), _93871 = _93869, cowlNothing(_93871)], (180 ^ _92866) ^ [_98477, _98479, _98481, _98483] : [-(rs(_98481, _98477)), rs(_98483, _98479), _98483 = _98481, _98479 = _98477], (114 ^ _92866) ^ [_96406, _96408, _96410, _96412] : [-(rinvF(_96410, _96406)), rinvF(_96412, _96408), _96412 = _96410, _96408 = _96406], (4 ^ _92866) ^ [_93057, _93059] : [_93059 = _93057, -(_93057 = _93059)], (194 ^ _92866) ^ [_98901, _98903, _98905, _98907] : [-(rf1(_98905, _98901)), rf1(_98907, _98903), _98907 = _98905, _98903 = _98901], (142 ^ _92866) ^ [_97294, _97296, _97298, _97300] : [-(rinvS(_97298, _97294)), rinvS(_97300, _97296), _97300 = _97298, _97296 = _97294], (128 ^ _92866) ^ [_96850, _96852, _96854, _96856] : [-(rinvF1(_96854, _96850)), rinvF1(_96856, _96852), _96856 = _96854, _96852 = _96850], (50 ^ _92866) ^ [_94459, _94461] : [-(xsd_integer(_94459)), _94461 = _94459, xsd_integer(_94461)], (10 ^ _92866) ^ [_93261, _93263, _93265] : [-(_93265 = _93261), _93265 = _93263, _93263 = _93261], (94 ^ _92866) ^ [_95788, _95790] : [-(ca_Vx3(_95788)), _95790 = _95788, ca_Vx3(_95790)], (156 ^ _92866) ^ [_97710, _97712] : [-(cUnsatisfiable(_97710)), _97712 = _97710, cUnsatisfiable(_97712)]], input).
% 56.55/55.29 ncf('1',plain,[-(rs(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])), 459 ^ [i2003_11_14_17_21_08508] = 459 ^ [i2003_11_14_17_21_08508], rs(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])],start(408 ^ 0,bind([[_105631, _105633, _105635], [i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508], 459 ^ [i2003_11_14_17_21_08508]]]))).
% 56.55/55.29 ncf('1.1',plain,[rs(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508]), -(rinvS(459 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508))],extension(606 ^ 1,bind([[_112111, _112113], [i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508]]]))).
% 56.55/55.29 ncf('1.1.1',plain,[rinvS(459 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508), 509 : -(cp(i2003_11_14_17_21_08508)), 509 : ca_Ax2(459 ^ [i2003_11_14_17_21_08508])],extension(505 ^ 2,bind([[_108756, _108922], [459 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.1.1.1',plain,[cp(i2003_11_14_17_21_08508), 483 : ra_Px1(i2003_11_14_17_21_08508, 495 ^ [i2003_11_14_17_21_08508])],extension(479 ^ 5,bind([[_107860, _107971], [i2003_11_14_17_21_08508, 495 ^ [i2003_11_14_17_21_08508]]]))).
% 56.55/55.29 ncf('1.1.1.1.1',plain,[-(ra_Px1(i2003_11_14_17_21_08508, 495 ^ [i2003_11_14_17_21_08508])), cpxcomp(i2003_11_14_17_21_08508)],extension(492 ^ 8,bind([[_108310], [i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.1.1.1.1.1',plain,[-(cpxcomp(i2003_11_14_17_21_08508)), cUnsatisfiable(i2003_11_14_17_21_08508)],extension(454 ^ 9,bind([[_107059], [i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.1.1.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_08508))],extension(622 ^ 10)).
% 56.55/55.29 ncf('1.1.1.2',plain,[-(ca_Ax2(459 ^ [i2003_11_14_17_21_08508])), cUnsatisfiable(i2003_11_14_17_21_08508)],extension(454 ^ 3,bind([[_107059], [i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.1.1.2.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_08508))],extension(622 ^ 4)).
% 56.55/55.29 ncf('1.2',plain,[-(459 ^ [i2003_11_14_17_21_08508] = 459 ^ [i2003_11_14_17_21_08508]), rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508]), rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])],extension(556 ^ 1,bind([[_110482, _110484, _110486], [459 ^ [i2003_11_14_17_21_08508], 459 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.2.1',plain,[-(rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])), rinvF(459 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508)],extension(576 ^ 2,bind([[_111143, _111145], [i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508]]]))).
% 56.55/55.29 ncf('1.2.1.1',plain,[-(rinvF(459 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508)), rinvF(459 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508), 459 ^ [i2003_11_14_17_21_08508] = 459 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508 = i2003_11_14_17_21_08508],extension(114 ^ 3,bind([[_96406, _96408, _96410, _96412], [i2003_11_14_17_21_08508, i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508], 459 ^ [i2003_11_14_17_21_08508]]]))).
% 56.55/55.29 ncf('1.2.1.1.1',plain,[-(rinvF(459 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508)), rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])],extension(582 ^ 4,bind([[_111305, _111307], [i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508]]]))).
% 56.55/55.29 ncf('1.2.1.1.1.1',plain,[-(rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])), cUnsatisfiable(i2003_11_14_17_21_08508)],extension(454 ^ 5,bind([[_107059], [i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.2.1.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_08508))],extension(622 ^ 6)).
% 56.55/55.29 ncf('1.2.1.1.2',plain,[-(459 ^ [i2003_11_14_17_21_08508] = 459 ^ [i2003_11_14_17_21_08508]), rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508]), rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])],extension(556 ^ 4,bind([[_110482, _110484, _110486], [459 ^ [i2003_11_14_17_21_08508], 459 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.2.1.1.2.1',plain,[-(rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])), cUnsatisfiable(i2003_11_14_17_21_08508)],extension(454 ^ 5,bind([[_107059], [i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.2.1.1.2.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_08508))],extension(622 ^ 6)).
% 56.55/55.29 ncf('1.2.1.1.2.2',plain,[-(rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])), cUnsatisfiable(i2003_11_14_17_21_08508)],extension(454 ^ 5,bind([[_107059], [i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.2.1.1.2.2.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_08508))],extension(622 ^ 6)).
% 56.55/55.29 ncf('1.2.1.1.3',plain,[-(i2003_11_14_17_21_08508 = i2003_11_14_17_21_08508)],extension(2 ^ 4,bind([[_92950], [i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.2.2',plain,[-(rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508]))],lemmata('[1].x')).
% 56.55/55.29 ncf('1.3',plain,[-(rs(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])), rs(i2003_11_14_17_21_08508, 540 ^ [i2003_11_14_17_21_08508]), i2003_11_14_17_21_08508 = i2003_11_14_17_21_08508, 540 ^ [i2003_11_14_17_21_08508] = 459 ^ [i2003_11_14_17_21_08508]],extension(180 ^ 1,bind([[_98477, _98479, _98481, _98483], [459 ^ [i2003_11_14_17_21_08508], 540 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508, i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.3.1',plain,[-(rs(i2003_11_14_17_21_08508, 540 ^ [i2003_11_14_17_21_08508])), ca_Vx3(i2003_11_14_17_21_08508)],extension(537 ^ 2,bind([[_109835], [i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.3.1.1',plain,[-(ca_Vx3(i2003_11_14_17_21_08508)), 515 : rinvF(459 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508), 515 : ca_Ax2(459 ^ [i2003_11_14_17_21_08508])],extension(505 ^ 3,bind([[_108756, _109098], [459 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.3.1.1.1',plain,[-(rinvF(459 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508)), rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])],extension(582 ^ 6,bind([[_111305, _111307], [i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508]]]))).
% 56.55/55.29 ncf('1.3.1.1.1.1',plain,[-(rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])), cUnsatisfiable(i2003_11_14_17_21_08508)],extension(454 ^ 7,bind([[_107059], [i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.3.1.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_08508))],extension(622 ^ 8)).
% 56.55/55.29 ncf('1.3.1.1.2',plain,[-(ca_Ax2(459 ^ [i2003_11_14_17_21_08508])), cUnsatisfiable(i2003_11_14_17_21_08508)],extension(454 ^ 4,bind([[_107059], [i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.3.1.1.2.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_08508))],extension(622 ^ 5)).
% 56.55/55.29 ncf('1.3.2',plain,[-(i2003_11_14_17_21_08508 = i2003_11_14_17_21_08508)],extension(2 ^ 2,bind([[_92950], [i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.3.3',plain,[-(540 ^ [i2003_11_14_17_21_08508] = 459 ^ [i2003_11_14_17_21_08508]), rf(i2003_11_14_17_21_08508, 540 ^ [i2003_11_14_17_21_08508]), rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])],extension(556 ^ 2,bind([[_110482, _110484, _110486], [459 ^ [i2003_11_14_17_21_08508], 540 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.3.3.1',plain,[-(rf(i2003_11_14_17_21_08508, 540 ^ [i2003_11_14_17_21_08508])), 459 ^ [i2003_11_14_17_21_08508] = 540 ^ [i2003_11_14_17_21_08508], rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])],extension(308 ^ 3,bind([[_102401, _102403, _102405], [i2003_11_14_17_21_08508, 540 ^ [i2003_11_14_17_21_08508], 459 ^ [i2003_11_14_17_21_08508]]]))).
% 56.55/55.29 ncf('1.3.3.1.1',plain,[-(459 ^ [i2003_11_14_17_21_08508] = 540 ^ [i2003_11_14_17_21_08508]), rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508]), rf(i2003_11_14_17_21_08508, 540 ^ [i2003_11_14_17_21_08508])],extension(556 ^ 4,bind([[_110482, _110484, _110486], [540 ^ [i2003_11_14_17_21_08508], 459 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.3.3.1.1.1',plain,[-(rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])), cUnsatisfiable(i2003_11_14_17_21_08508)],extension(454 ^ 5,bind([[_107059], [i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.3.3.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_08508))],extension(622 ^ 6)).
% 56.55/55.29 ncf('1.3.3.1.1.2',plain,[-(rf(i2003_11_14_17_21_08508, 540 ^ [i2003_11_14_17_21_08508])), rs(i2003_11_14_17_21_08508, 540 ^ [i2003_11_14_17_21_08508])],extension(624 ^ 5,bind([[_112699, _112701], [540 ^ [i2003_11_14_17_21_08508], i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.3.3.1.1.2.1',plain,[-(rs(i2003_11_14_17_21_08508, 540 ^ [i2003_11_14_17_21_08508]))],lemmata('[1].x')).
% 56.55/55.29 ncf('1.3.3.1.2',plain,[-(rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])), cUnsatisfiable(i2003_11_14_17_21_08508)],extension(454 ^ 4,bind([[_107059], [i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.3.3.1.2.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_08508))],extension(622 ^ 5)).
% 56.55/55.29 ncf('1.3.3.2',plain,[-(rf(i2003_11_14_17_21_08508, 459 ^ [i2003_11_14_17_21_08508])), cUnsatisfiable(i2003_11_14_17_21_08508)],extension(454 ^ 3,bind([[_107059], [i2003_11_14_17_21_08508]]))).
% 56.55/55.29 ncf('1.3.3.2.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_08508))],extension(622 ^ 4)).
% 56.55/55.29 %-----------------------------------------------------
% 56.55/55.29 End of proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------