%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS112+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n020.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 0.59s 1.40s
% Output : Proof 0.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS112+1 : TPTP v8.1.2. Released v3.1.0.
% 0.11/0.13 % Command : nanocop.sh %s %d
% 0.11/0.34 % Computer : n020.cluster.edu
% 0.11/0.34 % Model : x86_64 x86_64
% 0.11/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.34 % Memory : 8042.1875MB
% 0.11/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.34 % CPULimit : 300
% 0.11/0.34 % WCLimit : 300
% 0.11/0.34 % DateTime : Thu May 18 23:00:02 EDT 2023
% 0.11/0.34 % CPUTime :
% 0.59/1.40
% 0.59/1.40 /export/starexec/sandbox/benchmark/theBenchmark.p is Unsatisfiable
% 0.59/1.40 Start of proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.59/1.40 %-----------------------------------------------------
% 0.59/1.40 ncf(matrix, plain, [(2 ^ _90610) ^ [_90714] : [-(_90714 = _90714)], (4 ^ _90610) ^ [_90821, _90823] : [_90823 = _90821, -(_90821 = _90823)], (10 ^ _90610) ^ [_91025, _91027, _91029] : [-(_91029 = _91025), _91029 = _91027, _91027 = _91025], (20 ^ _90610) ^ [_91338, _91340] : [-(cowlNothing(_91338)), _91340 = _91338, cowlNothing(_91340)], (30 ^ _90610) ^ [_91633, _91635] : [-(xsd_string(_91633)), _91635 = _91633, xsd_string(_91635)], (40 ^ _90610) ^ [_91928, _91930] : [-(xsd_integer(_91928)), _91930 = _91928, xsd_integer(_91930)], (50 ^ _90610) ^ [_92223, _92225] : [-(cp(_92223)), _92225 = _92223, cp(_92225)], (60 ^ _90610) ^ [_92546, _92548, _92550, _92552] : [-(ra_Px1(_92550, _92546)), ra_Px1(_92552, _92548), _92552 = _92550, _92548 = _92546], (74 ^ _90610) ^ [_92962, _92964] : [-(ca_Ax2(_92962)), _92964 = _92962, ca_Ax2(_92964)], (84 ^ _90610) ^ [_93257, _93259] : [-(cpxcomp(_93257)), _93259 = _93257, cpxcomp(_93259)], (94 ^ _90610) ^ [_93552, _93554] : [-(ca_Vx3(_93552)), _93554 = _93552, ca_Vx3(_93554)], (104 ^ _90610) ^ [_93847, _93849] : [-(cowlThing(_93847)), _93849 = _93847, cowlThing(_93849)], (114 ^ _90610) ^ [_94170, _94172, _94174, _94176] : [-(rinvF(_94174, _94170)), rinvF(_94176, _94172), _94176 = _94174, _94172 = _94170], (128 ^ _90610) ^ [_94614, _94616, _94618, _94620] : [-(rinvF1(_94618, _94614)), rinvF1(_94620, _94616), _94620 = _94618, _94616 = _94614], (142 ^ _90610) ^ [_95058, _95060, _95062, _95064] : [-(rinvS(_95062, _95058)), rinvS(_95064, _95060), _95064 = _95062, _95060 = _95058], (156 ^ _90610) ^ [_95474, _95476] : [-(cUnsatisfiable(_95474)), _95476 = _95474, cUnsatisfiable(_95476)], (166 ^ _90610) ^ [_95797, _95799, _95801, _95803] : [-(rf(_95801, _95797)), rf(_95803, _95799), _95803 = _95801, _95799 = _95797], (180 ^ _90610) ^ [_96241, _96243, _96245, _96247] : [-(rs(_96245, _96241)), rs(_96247, _96243), _96247 = _96245, _96243 = _96241], (194 ^ _90610) ^ [_96665, _96667, _96669, _96671] : [-(rf1(_96669, _96665)), rf1(_96671, _96667), _96671 = _96669, _96667 = _96665], (208 ^ _90610) ^ [_97117, _97119] : [-(cUnsatisfiable(_97117)), _97119 = _97117, cUnsatisfiable(_97119)], (218 ^ _90610) ^ [_97412, _97414] : [-(ca_Ax2(_97412)), _97414 = _97412, ca_Ax2(_97414)], (228 ^ _90610) ^ [_97707, _97709] : [-(ca_Vx3(_97707)), _97709 = _97707, ca_Vx3(_97709)], (238 ^ _90610) ^ [_98002, _98004] : [-(cowlNothing(_98002)), _98004 = _98002, cowlNothing(_98004)], (248 ^ _90610) ^ [_98297, _98299] : [-(cowlThing(_98297)), _98299 = _98297, cowlThing(_98299)], (258 ^ _90610) ^ [_98592, _98594] : [-(cp(_98592)), _98594 = _98592, cp(_98594)], (268 ^ _90610) ^ [_98887, _98889] : [-(cpxcomp(_98887)), _98889 = _98887, cpxcomp(_98889)], (278 ^ _90610) ^ [_99196, _99198, _99200] : [-(ra_Px1(_99198, _99196)), _99200 = _99198, ra_Px1(_99200, _99196)], (288 ^ _90610) ^ [_99519, _99521, _99523] : [-(ra_Px1(_99519, _99521)), _99523 = _99521, ra_Px1(_99519, _99523)], (298 ^ _90610) ^ [_99842, _99844, _99846] : [-(rf(_99844, _99842)), _99846 = _99844, rf(_99846, _99842)], (308 ^ _90610) ^ [_100165, _100167, _100169] : [-(rf(_100165, _100167)), _100169 = _100167, rf(_100165, _100169)], (318 ^ _90610) ^ [_100488, _100490, _100492] : [-(rf1(_100490, _100488)), _100492 = _100490, rf1(_100492, _100488)], (328 ^ _90610) ^ [_100811, _100813, _100815] : [-(rf1(_100811, _100813)), _100815 = _100813, rf1(_100811, _100815)], (338 ^ _90610) ^ [_101134, _101136, _101138] : [-(rinvF(_101136, _101134)), _101138 = _101136, rinvF(_101138, _101134)], (348 ^ _90610) ^ [_101457, _101459, _101461] : [-(rinvF(_101457, _101459)), _101461 = _101459, rinvF(_101457, _101461)], (358 ^ _90610) ^ [_101780, _101782, _101784] : [-(rinvF1(_101782, _101780)), _101784 = _101782, rinvF1(_101784, _101780)], (368 ^ _90610) ^ [_102103, _102105, _102107] : [-(rinvF1(_102103, _102105)), _102107 = _102105, rinvF1(_102103, _102107)], (378 ^ _90610) ^ [_102426, _102428, _102430] : [-(rinvS(_102428, _102426)), _102430 = _102428, rinvS(_102430, _102426)], (388 ^ _90610) ^ [_102749, _102751, _102753] : [-(rinvS(_102749, _102751)), _102753 = _102751, rinvS(_102749, _102753)], (398 ^ _90610) ^ [_103072, _103074, _103076] : [-(rs(_103074, _103072)), _103076 = _103074, rs(_103076, _103072)], (408 ^ _90610) ^ [_103395, _103397, _103399] : [-(rs(_103395, _103397)), _103399 = _103397, rs(_103395, _103399)], (418 ^ _90610) ^ [_103704, _103706] : [-(xsd_integer(_103704)), _103706 = _103704, xsd_integer(_103706)], (428 ^ _90610) ^ [_103999, _104001] : [-(xsd_string(_103999)), _104001 = _103999, xsd_string(_104001)], (438 ^ _90610) ^ [_104285] : [-(cowlThing(_104285))], (440 ^ _90610) ^ [_104327] : [cowlNothing(_104327)], (442 ^ _90610) ^ [_104450] : [xsd_string(_104450), xsd_integer(_104450)], (448 ^ _90610) ^ [_104603] : [-(xsd_integer(_104603)), -(xsd_string(_104603))], (454 ^ _90610) ^ [_104823] : [cUnsatisfiable(_104823), 458 ^ _90610 : [(459 ^ _90610) ^ [] : [-(rf1(_104823, 457 ^ [_104823]))], (461 ^ _90610) ^ [] : [-(ca_Ax2(457 ^ [_104823]))], (464 ^ _90610) ^ [] : [-(rf(_104823, 462 ^ [_104823]))], (466 ^ _90610) ^ [] : [-(cp(462 ^ [_104823]))]]], (468 ^ _90610) ^ [_105314] : [-(cUnsatisfiable(_105314)), 471 ^ _90610 : [(472 ^ _90610) ^ [_105450] : [rf1(_105314, _105450), ca_Ax2(_105450)]], 477 ^ _90610 : [(478 ^ _90610) ^ [_105625] : [rf(_105314, _105625), cp(_105625)]]], (486 ^ _90610) ^ [_105904] : [cp(_105904), 489 ^ _90610 : [(490 ^ _90610) ^ [_106015] : [ra_Px1(_105904, _106015)]]], (492 ^ _90610) ^ [_106081] : [-(ra_Px1(_106081, 493 ^ [_106081])), -(cp(_106081))], (499 ^ _90610) ^ [_106354] : [cpxcomp(_106354), -(ra_Px1(_106354, 502 ^ [_106354]))], (506 ^ _90610) ^ [_106559] : [507 ^ _90610 : [(508 ^ _90610) ^ [_106626] : [ra_Px1(_106559, _106626)]], -(cpxcomp(_106559))], (512 ^ _90610) ^ [_106800] : [ca_Ax2(_106800), 515 ^ _90610 : [(516 ^ _90610) ^ [] : [-(cpxcomp(_106800))], (518 ^ _90610) ^ [_106998] : [rinvF1(_106800, _106998), -(ca_Vx3(_106998))]]], (524 ^ _90610) ^ [_107167] : [-(ca_Ax2(_107167)), cpxcomp(_107167), 530 ^ _90610 : [(531 ^ _90610) ^ [] : [-(rinvF1(_107167, 529 ^ [_107167]))], (533 ^ _90610) ^ [] : [ca_Vx3(529 ^ [_107167])]]], (537 ^ _90610) ^ [_107601] : [ca_Vx3(_107601), 541 ^ _90610 : [(542 ^ _90610) ^ [] : [-(rs(_107601, 540 ^ [_107601]))], (544 ^ _90610) ^ [] : [-(cowlThing(540 ^ [_107601]))]]], (546 ^ _90610) ^ [_107887] : [-(ca_Vx3(_107887)), 547 ^ _90610 : [(548 ^ _90610) ^ [_107975] : [rs(_107887, _107975), cowlThing(_107975)]]], (556 ^ _90610) ^ [_108248, _108250, _108252] : [-(_108250 = _108248), rf(_108252, _108250), rf(_108252, _108248)], (566 ^ _90610) ^ [_108571, _108573, _108575] : [-(_108573 = _108571), rf1(_108575, _108573), rf1(_108575, _108571)], (576 ^ _90610) ^ [_108909, _108911] : [rinvF(_108911, _108909), -(rf(_108909, _108911))], (582 ^ _90610) ^ [_109071, _109073] : [rf(_109071, _109073), -(rinvF(_109073, _109071))], (588 ^ _90610) ^ [_109312, _109314] : [rinvF1(_109314, _109312), -(rf1(_109312, _109314))], (594 ^ _90610) ^ [_109474, _109476] : [rf1(_109474, _109476), -(rinvF1(_109476, _109474))], (600 ^ _90610) ^ [_109715, _109717] : [rinvS(_109717, _109715), -(rs(_109715, _109717))], (606 ^ _90610) ^ [_109877, _109879] : [rs(_109877, _109879), -(rinvS(_109879, _109877))], (612 ^ _90610) ^ [_110103, _110105, _110107] : [-(_110105 = _110103), rs(_110107, _110105), rs(_110107, _110103)], (622 ^ _90610) ^ [] : [-(cUnsatisfiable(i2003_11_14_17_21_19256))], (624 ^ _90610) ^ [_110465, _110467] : [rs(_110467, _110465), -(rf(_110467, _110465))], (630 ^ _90610) ^ [_110655, _110657] : [rs(_110657, _110655), -(rf1(_110657, _110655))]], input).
% 0.59/1.40 ncf('1',plain,[cp(462 ^ [i2003_11_14_17_21_19256]), 490 : ra_Px1(462 ^ [i2003_11_14_17_21_19256], 502 ^ [457 ^ [i2003_11_14_17_21_19256]])],start(486 ^ 0,bind([[_105904, _106015], [462 ^ [i2003_11_14_17_21_19256], 502 ^ [457 ^ [i2003_11_14_17_21_19256]]]]))).
% 0.59/1.40 ncf('1.1',plain,[-(cp(462 ^ [i2003_11_14_17_21_19256])), cUnsatisfiable(i2003_11_14_17_21_19256)],extension(454 ^ 1,bind([[_104823], [i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_19256))],extension(622 ^ 2)).
% 0.59/1.40 ncf('1.2',plain,[-(ra_Px1(462 ^ [i2003_11_14_17_21_19256], 502 ^ [457 ^ [i2003_11_14_17_21_19256]])), ra_Px1(457 ^ [i2003_11_14_17_21_19256], 502 ^ [457 ^ [i2003_11_14_17_21_19256]]), 457 ^ [i2003_11_14_17_21_19256] = 462 ^ [i2003_11_14_17_21_19256], 502 ^ [457 ^ [i2003_11_14_17_21_19256]] = 502 ^ [457 ^ [i2003_11_14_17_21_19256]]],extension(60 ^ 3,bind([[_92546, _92548, _92550, _92552], [502 ^ [457 ^ [i2003_11_14_17_21_19256]], 502 ^ [457 ^ [i2003_11_14_17_21_19256]], 462 ^ [i2003_11_14_17_21_19256], 457 ^ [i2003_11_14_17_21_19256]]]))).
% 0.59/1.40 ncf('1.2.1',plain,[-(ra_Px1(457 ^ [i2003_11_14_17_21_19256], 502 ^ [457 ^ [i2003_11_14_17_21_19256]])), ra_Px1(457 ^ [i2003_11_14_17_21_19256], 502 ^ [457 ^ [i2003_11_14_17_21_19256]]), 457 ^ [i2003_11_14_17_21_19256] = 457 ^ [i2003_11_14_17_21_19256], 502 ^ [457 ^ [i2003_11_14_17_21_19256]] = 502 ^ [457 ^ [i2003_11_14_17_21_19256]]],extension(60 ^ 4,bind([[_92546, _92548, _92550, _92552], [502 ^ [457 ^ [i2003_11_14_17_21_19256]], 502 ^ [457 ^ [i2003_11_14_17_21_19256]], 457 ^ [i2003_11_14_17_21_19256], 457 ^ [i2003_11_14_17_21_19256]]]))).
% 0.59/1.40 ncf('1.2.1.1',plain,[-(ra_Px1(457 ^ [i2003_11_14_17_21_19256], 502 ^ [457 ^ [i2003_11_14_17_21_19256]])), ra_Px1(457 ^ [i2003_11_14_17_21_19256], 502 ^ [457 ^ [i2003_11_14_17_21_19256]]), 457 ^ [i2003_11_14_17_21_19256] = 457 ^ [i2003_11_14_17_21_19256], 502 ^ [457 ^ [i2003_11_14_17_21_19256]] = 502 ^ [457 ^ [i2003_11_14_17_21_19256]]],extension(60 ^ 5,bind([[_92546, _92548, _92550, _92552], [502 ^ [457 ^ [i2003_11_14_17_21_19256]], 502 ^ [457 ^ [i2003_11_14_17_21_19256]], 457 ^ [i2003_11_14_17_21_19256], 457 ^ [i2003_11_14_17_21_19256]]]))).
% 0.59/1.40 ncf('1.2.1.1.1',plain,[-(ra_Px1(457 ^ [i2003_11_14_17_21_19256], 502 ^ [457 ^ [i2003_11_14_17_21_19256]])), ra_Px1(457 ^ [i2003_11_14_17_21_19256], 502 ^ [457 ^ [i2003_11_14_17_21_19256]]), 457 ^ [i2003_11_14_17_21_19256] = 457 ^ [i2003_11_14_17_21_19256], 502 ^ [457 ^ [i2003_11_14_17_21_19256]] = 502 ^ [457 ^ [i2003_11_14_17_21_19256]]],extension(60 ^ 6,bind([[_92546, _92548, _92550, _92552], [502 ^ [457 ^ [i2003_11_14_17_21_19256]], 502 ^ [457 ^ [i2003_11_14_17_21_19256]], 457 ^ [i2003_11_14_17_21_19256], 457 ^ [i2003_11_14_17_21_19256]]]))).
% 0.59/1.40 ncf('1.2.1.1.1.1',plain,[-(ra_Px1(457 ^ [i2003_11_14_17_21_19256], 502 ^ [457 ^ [i2003_11_14_17_21_19256]])), cpxcomp(457 ^ [i2003_11_14_17_21_19256])],extension(499 ^ 7,bind([[_106354], [457 ^ [i2003_11_14_17_21_19256]]]))).
% 0.59/1.40 ncf('1.2.1.1.1.1.1',plain,[-(cpxcomp(457 ^ [i2003_11_14_17_21_19256])), ca_Ax2(457 ^ [i2003_11_14_17_21_19256])],extension(512 ^ 8,bind([[_106800], [457 ^ [i2003_11_14_17_21_19256]]]))).
% 0.59/1.40 ncf('1.2.1.1.1.1.1.1',plain,[-(ca_Ax2(457 ^ [i2003_11_14_17_21_19256])), cUnsatisfiable(i2003_11_14_17_21_19256)],extension(454 ^ 9,bind([[_104823], [i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.1.1.1.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_19256))],extension(622 ^ 10)).
% 0.59/1.40 ncf('1.2.1.1.1.2',plain,[-(457 ^ [i2003_11_14_17_21_19256] = 457 ^ [i2003_11_14_17_21_19256])],extension(2 ^ 7,bind([[_90714], [457 ^ [i2003_11_14_17_21_19256]]]))).
% 0.59/1.40 ncf('1.2.1.1.1.3',plain,[-(502 ^ [457 ^ [i2003_11_14_17_21_19256]] = 502 ^ [457 ^ [i2003_11_14_17_21_19256]])],extension(2 ^ 7,bind([[_90714], [502 ^ [457 ^ [i2003_11_14_17_21_19256]]]]))).
% 0.59/1.40 ncf('1.2.1.1.2',plain,[-(457 ^ [i2003_11_14_17_21_19256] = 457 ^ [i2003_11_14_17_21_19256])],extension(2 ^ 6,bind([[_90714], [457 ^ [i2003_11_14_17_21_19256]]]))).
% 0.59/1.40 ncf('1.2.1.1.3',plain,[-(502 ^ [457 ^ [i2003_11_14_17_21_19256]] = 502 ^ [457 ^ [i2003_11_14_17_21_19256]])],extension(2 ^ 6,bind([[_90714], [502 ^ [457 ^ [i2003_11_14_17_21_19256]]]]))).
% 0.59/1.40 ncf('1.2.1.2',plain,[-(457 ^ [i2003_11_14_17_21_19256] = 457 ^ [i2003_11_14_17_21_19256])],extension(2 ^ 5,bind([[_90714], [457 ^ [i2003_11_14_17_21_19256]]]))).
% 0.59/1.40 ncf('1.2.1.3',plain,[-(502 ^ [457 ^ [i2003_11_14_17_21_19256]] = 502 ^ [457 ^ [i2003_11_14_17_21_19256]])],extension(2 ^ 5,bind([[_90714], [502 ^ [457 ^ [i2003_11_14_17_21_19256]]]]))).
% 0.59/1.40 ncf('1.2.2',plain,[-(457 ^ [i2003_11_14_17_21_19256] = 462 ^ [i2003_11_14_17_21_19256]), rs(i2003_11_14_17_21_19256, 457 ^ [i2003_11_14_17_21_19256]), rs(i2003_11_14_17_21_19256, 462 ^ [i2003_11_14_17_21_19256])],extension(612 ^ 4,bind([[_110103, _110105, _110107], [462 ^ [i2003_11_14_17_21_19256], 457 ^ [i2003_11_14_17_21_19256], i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.1',plain,[-(rs(i2003_11_14_17_21_19256, 457 ^ [i2003_11_14_17_21_19256])), rs(i2003_11_14_17_21_19256, 540 ^ [i2003_11_14_17_21_19256]), i2003_11_14_17_21_19256 = i2003_11_14_17_21_19256, 540 ^ [i2003_11_14_17_21_19256] = 457 ^ [i2003_11_14_17_21_19256]],extension(180 ^ 5,bind([[_96241, _96243, _96245, _96247], [457 ^ [i2003_11_14_17_21_19256], 540 ^ [i2003_11_14_17_21_19256], i2003_11_14_17_21_19256, i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.1.1',plain,[-(rs(i2003_11_14_17_21_19256, 540 ^ [i2003_11_14_17_21_19256])), ca_Vx3(i2003_11_14_17_21_19256)],extension(537 ^ 6,bind([[_107601], [i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.1.1.1',plain,[-(ca_Vx3(i2003_11_14_17_21_19256)), 518 : rinvF1(457 ^ [i2003_11_14_17_21_19256], i2003_11_14_17_21_19256), 518 : ca_Ax2(457 ^ [i2003_11_14_17_21_19256])],extension(512 ^ 7,bind([[_106800, _106998], [457 ^ [i2003_11_14_17_21_19256], i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.1.1.1.1',plain,[-(rinvF1(457 ^ [i2003_11_14_17_21_19256], i2003_11_14_17_21_19256)), rf1(i2003_11_14_17_21_19256, 457 ^ [i2003_11_14_17_21_19256])],extension(594 ^ 10,bind([[_109474, _109476], [i2003_11_14_17_21_19256, 457 ^ [i2003_11_14_17_21_19256]]]))).
% 0.59/1.40 ncf('1.2.2.1.1.1.1.1',plain,[-(rf1(i2003_11_14_17_21_19256, 457 ^ [i2003_11_14_17_21_19256])), cUnsatisfiable(i2003_11_14_17_21_19256)],extension(454 ^ 11,bind([[_104823], [i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.1.1.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_19256))],extension(622 ^ 12)).
% 0.59/1.40 ncf('1.2.2.1.1.1.2',plain,[-(ca_Ax2(457 ^ [i2003_11_14_17_21_19256])), cUnsatisfiable(i2003_11_14_17_21_19256)],extension(454 ^ 8,bind([[_104823], [i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.1.1.1.2.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_19256))],extension(622 ^ 9)).
% 0.59/1.40 ncf('1.2.2.1.2',plain,[-(i2003_11_14_17_21_19256 = i2003_11_14_17_21_19256)],extension(2 ^ 6,bind([[_90714], [i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.1.3',plain,[-(540 ^ [i2003_11_14_17_21_19256] = 457 ^ [i2003_11_14_17_21_19256]), 457 ^ [i2003_11_14_17_21_19256] = 540 ^ [i2003_11_14_17_21_19256]],extension(4 ^ 6,bind([[_90821, _90823], [540 ^ [i2003_11_14_17_21_19256], 457 ^ [i2003_11_14_17_21_19256]]]))).
% 0.59/1.40 ncf('1.2.2.1.3.1',plain,[-(457 ^ [i2003_11_14_17_21_19256] = 540 ^ [i2003_11_14_17_21_19256]), rf1(i2003_11_14_17_21_19256, 457 ^ [i2003_11_14_17_21_19256]), rf1(i2003_11_14_17_21_19256, 540 ^ [i2003_11_14_17_21_19256])],extension(566 ^ 7,bind([[_108571, _108573, _108575], [540 ^ [i2003_11_14_17_21_19256], 457 ^ [i2003_11_14_17_21_19256], i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.1.3.1.1',plain,[-(rf1(i2003_11_14_17_21_19256, 457 ^ [i2003_11_14_17_21_19256])), rf1(i2003_11_14_17_21_19256, 457 ^ [i2003_11_14_17_21_19256]), i2003_11_14_17_21_19256 = i2003_11_14_17_21_19256, 457 ^ [i2003_11_14_17_21_19256] = 457 ^ [i2003_11_14_17_21_19256]],extension(194 ^ 8,bind([[_96665, _96667, _96669, _96671], [457 ^ [i2003_11_14_17_21_19256], 457 ^ [i2003_11_14_17_21_19256], i2003_11_14_17_21_19256, i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.1.3.1.1.1',plain,[-(rf1(i2003_11_14_17_21_19256, 457 ^ [i2003_11_14_17_21_19256])), cUnsatisfiable(i2003_11_14_17_21_19256)],extension(454 ^ 9,bind([[_104823], [i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.1.3.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_19256))],extension(622 ^ 10)).
% 0.59/1.40 ncf('1.2.2.1.3.1.1.2',plain,[-(i2003_11_14_17_21_19256 = i2003_11_14_17_21_19256)],extension(2 ^ 9,bind([[_90714], [i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.1.3.1.1.3',plain,[-(457 ^ [i2003_11_14_17_21_19256] = 457 ^ [i2003_11_14_17_21_19256])],extension(2 ^ 9,bind([[_90714], [457 ^ [i2003_11_14_17_21_19256]]]))).
% 0.59/1.40 ncf('1.2.2.1.3.1.2',plain,[-(rf1(i2003_11_14_17_21_19256, 540 ^ [i2003_11_14_17_21_19256])), rs(i2003_11_14_17_21_19256, 540 ^ [i2003_11_14_17_21_19256])],extension(630 ^ 8,bind([[_110655, _110657], [540 ^ [i2003_11_14_17_21_19256], i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.1.3.1.2.1',plain,[-(rs(i2003_11_14_17_21_19256, 540 ^ [i2003_11_14_17_21_19256]))],lemmata('[2, 2, 1].x')).
% 0.59/1.40 ncf('1.2.2.2',plain,[-(rs(i2003_11_14_17_21_19256, 462 ^ [i2003_11_14_17_21_19256])), rs(i2003_11_14_17_21_19256, 540 ^ [i2003_11_14_17_21_19256]), i2003_11_14_17_21_19256 = i2003_11_14_17_21_19256, 540 ^ [i2003_11_14_17_21_19256] = 462 ^ [i2003_11_14_17_21_19256]],extension(180 ^ 5,bind([[_96241, _96243, _96245, _96247], [462 ^ [i2003_11_14_17_21_19256], 540 ^ [i2003_11_14_17_21_19256], i2003_11_14_17_21_19256, i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.2.1',plain,[-(rs(i2003_11_14_17_21_19256, 540 ^ [i2003_11_14_17_21_19256])), ca_Vx3(i2003_11_14_17_21_19256)],extension(537 ^ 6,bind([[_107601], [i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.2.1.1',plain,[-(ca_Vx3(i2003_11_14_17_21_19256)), 518 : rinvF1(457 ^ [i2003_11_14_17_21_19256], i2003_11_14_17_21_19256), 518 : ca_Ax2(457 ^ [i2003_11_14_17_21_19256])],extension(512 ^ 7,bind([[_106800, _106998], [457 ^ [i2003_11_14_17_21_19256], i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.2.1.1.1',plain,[-(rinvF1(457 ^ [i2003_11_14_17_21_19256], i2003_11_14_17_21_19256)), rf1(i2003_11_14_17_21_19256, 457 ^ [i2003_11_14_17_21_19256])],extension(594 ^ 10,bind([[_109474, _109476], [i2003_11_14_17_21_19256, 457 ^ [i2003_11_14_17_21_19256]]]))).
% 0.59/1.40 ncf('1.2.2.2.1.1.1.1',plain,[-(rf1(i2003_11_14_17_21_19256, 457 ^ [i2003_11_14_17_21_19256])), cUnsatisfiable(i2003_11_14_17_21_19256)],extension(454 ^ 11,bind([[_104823], [i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.2.1.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_19256))],extension(622 ^ 12)).
% 0.59/1.40 ncf('1.2.2.2.1.1.2',plain,[-(ca_Ax2(457 ^ [i2003_11_14_17_21_19256])), cUnsatisfiable(i2003_11_14_17_21_19256)],extension(454 ^ 8,bind([[_104823], [i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.2.1.1.2.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_19256))],extension(622 ^ 9)).
% 0.59/1.40 ncf('1.2.2.2.2',plain,[-(i2003_11_14_17_21_19256 = i2003_11_14_17_21_19256)],extension(2 ^ 6,bind([[_90714], [i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.2.3',plain,[-(540 ^ [i2003_11_14_17_21_19256] = 462 ^ [i2003_11_14_17_21_19256]), 462 ^ [i2003_11_14_17_21_19256] = 540 ^ [i2003_11_14_17_21_19256]],extension(4 ^ 6,bind([[_90821, _90823], [540 ^ [i2003_11_14_17_21_19256], 462 ^ [i2003_11_14_17_21_19256]]]))).
% 0.59/1.40 ncf('1.2.2.2.3.1',plain,[-(462 ^ [i2003_11_14_17_21_19256] = 540 ^ [i2003_11_14_17_21_19256]), rf(i2003_11_14_17_21_19256, 462 ^ [i2003_11_14_17_21_19256]), rf(i2003_11_14_17_21_19256, 540 ^ [i2003_11_14_17_21_19256])],extension(556 ^ 7,bind([[_108248, _108250, _108252], [540 ^ [i2003_11_14_17_21_19256], 462 ^ [i2003_11_14_17_21_19256], i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.2.3.1.1',plain,[-(rf(i2003_11_14_17_21_19256, 462 ^ [i2003_11_14_17_21_19256])), rf(i2003_11_14_17_21_19256, 462 ^ [i2003_11_14_17_21_19256]), i2003_11_14_17_21_19256 = i2003_11_14_17_21_19256, 462 ^ [i2003_11_14_17_21_19256] = 462 ^ [i2003_11_14_17_21_19256]],extension(166 ^ 8,bind([[_95797, _95799, _95801, _95803], [462 ^ [i2003_11_14_17_21_19256], 462 ^ [i2003_11_14_17_21_19256], i2003_11_14_17_21_19256, i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.2.3.1.1.1',plain,[-(rf(i2003_11_14_17_21_19256, 462 ^ [i2003_11_14_17_21_19256])), cUnsatisfiable(i2003_11_14_17_21_19256)],extension(454 ^ 9,bind([[_104823], [i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.2.3.1.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_21_19256))],extension(622 ^ 10)).
% 0.59/1.40 ncf('1.2.2.2.3.1.1.2',plain,[-(i2003_11_14_17_21_19256 = i2003_11_14_17_21_19256)],extension(2 ^ 9,bind([[_90714], [i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.2.3.1.1.3',plain,[-(462 ^ [i2003_11_14_17_21_19256] = 462 ^ [i2003_11_14_17_21_19256])],extension(2 ^ 9,bind([[_90714], [462 ^ [i2003_11_14_17_21_19256]]]))).
% 0.59/1.40 ncf('1.2.2.2.3.1.2',plain,[-(rf(i2003_11_14_17_21_19256, 540 ^ [i2003_11_14_17_21_19256])), rs(i2003_11_14_17_21_19256, 540 ^ [i2003_11_14_17_21_19256])],extension(624 ^ 8,bind([[_110465, _110467], [540 ^ [i2003_11_14_17_21_19256], i2003_11_14_17_21_19256]]))).
% 0.59/1.40 ncf('1.2.2.2.3.1.2.1',plain,[-(rs(i2003_11_14_17_21_19256, 540 ^ [i2003_11_14_17_21_19256]))],lemmata('[2, 2, 1].x')).
% 0.59/1.40 ncf('1.2.3',plain,[-(502 ^ [457 ^ [i2003_11_14_17_21_19256]] = 502 ^ [457 ^ [i2003_11_14_17_21_19256]])],extension(2 ^ 4,bind([[_90714], [502 ^ [457 ^ [i2003_11_14_17_21_19256]]]]))).
% 0.59/1.40 %-----------------------------------------------------
% 0.59/1.40 End of proof for negated /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------