%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS070+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n015.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:12 EDT 2023
% Result : Unsatisfiable 0.57s 1.37s
% Output : Proof 0.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : KRS070+1 : TPTP v8.1.2. Released v3.1.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n015.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:17:37 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.57/1.37
% 0.57/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is Unsatisfiable
% 0.57/1.37 Start of proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.57/1.37 %-----------------------------------------------------
% 0.57/1.37 ncf(matrix, plain, [(2 ^ _92776) ^ [_92880] : [-(_92880 = _92880)], (4 ^ _92776) ^ [_92987, _92989] : [_92989 = _92987, -(_92987 = _92989)], (10 ^ _92776) ^ [_93191, _93193, _93195] : [-(_93195 = _93191), _93195 = _93193, _93193 = _93191], (20 ^ _92776) ^ [_93504, _93506] : [-(cowlThing(_93504)), _93506 = _93504, cowlThing(_93506)], (30 ^ _92776) ^ [_93799, _93801] : [-(cowlNothing(_93799)), _93801 = _93799, cowlNothing(_93801)], (40 ^ _92776) ^ [_94094, _94096] : [-(xsd_string(_94094)), _94096 = _94094, xsd_string(_94096)], (50 ^ _92776) ^ [_94389, _94391] : [-(xsd_integer(_94389)), _94391 = _94389, xsd_integer(_94391)], (60 ^ _92776) ^ [_94684, _94686] : [-(cc2(_94684)), _94686 = _94684, cc2(_94686)], (70 ^ _92776) ^ [_94979, _94981] : [-(cc1(_94979)), _94981 = _94979, cc1(_94981)], (80 ^ _92776) ^ [_95274, _95276] : [-(cUnsatisfiable(_95274)), _95276 = _95274, cUnsatisfiable(_95276)], (90 ^ _92776) ^ [_95597, _95599, _95601, _95603] : [-(rrxa(_95601, _95597)), rrxa(_95603, _95599), _95603 = _95601, _95599 = _95597], (104 ^ _92776) ^ [_96041, _96043, _96045, _96047] : [-(rrx2(_96045, _96041)), rrx2(_96047, _96043), _96047 = _96045, _96043 = _96041], (118 ^ _92776) ^ [_96485, _96487, _96489, _96491] : [-(rrx3a(_96489, _96485)), rrx3a(_96491, _96487), _96491 = _96489, _96487 = _96485], (132 ^ _92776) ^ [_96929, _96931, _96933, _96935] : [-(rrx1a(_96933, _96929)), rrx1a(_96935, _96931), _96935 = _96933, _96931 = _96929], (146 ^ _92776) ^ [_97373, _97375, _97377, _97379] : [-(rrx4a(_97377, _97373)), rrx4a(_97379, _97375), _97379 = _97377, _97375 = _97373], (160 ^ _92776) ^ [_97817, _97819, _97821, _97823] : [-(rrx2a(_97821, _97817)), rrx2a(_97823, _97819), _97823 = _97821, _97819 = _97817], (174 ^ _92776) ^ [_98261, _98263, _98265, _98267] : [-(rrx3(_98265, _98261)), rrx3(_98267, _98263), _98267 = _98265, _98263 = _98261], (188 ^ _92776) ^ [_98705, _98707, _98709, _98711] : [-(rrx1(_98709, _98705)), rrx1(_98711, _98707), _98711 = _98709, _98707 = _98705], (202 ^ _92776) ^ [_99149, _99151, _99153, _99155] : [-(rrx4(_99153, _99149)), rrx4(_99155, _99151), _99155 = _99153, _99151 = _99149], (216 ^ _92776) ^ [_99573, _99575, _99577, _99579] : [-(rrx(_99577, _99573)), rrx(_99579, _99575), _99579 = _99577, _99575 = _99573], (230 ^ _92776) ^ [_100063, _100065] : [-(cUnsatisfiable(_100063)), _100065 = _100063, cUnsatisfiable(_100065)], (240 ^ _92776) ^ [_100358, _100360] : [-(cc1(_100358)), _100360 = _100358, cc1(_100360)], (250 ^ _92776) ^ [_100653, _100655] : [-(cc2(_100653)), _100655 = _100653, cc2(_100655)], (260 ^ _92776) ^ [_100948, _100950] : [-(cowlNothing(_100948)), _100950 = _100948, cowlNothing(_100950)], (270 ^ _92776) ^ [_101243, _101245] : [-(cowlThing(_101243)), _101245 = _101243, cowlThing(_101245)], (280 ^ _92776) ^ [_101552, _101554, _101556] : [-(rrx(_101554, _101552)), _101556 = _101554, rrx(_101556, _101552)], (290 ^ _92776) ^ [_101875, _101877, _101879] : [-(rrx(_101875, _101877)), _101879 = _101877, rrx(_101875, _101879)], (300 ^ _92776) ^ [_102198, _102200, _102202] : [-(rrx1(_102200, _102198)), _102202 = _102200, rrx1(_102202, _102198)], (310 ^ _92776) ^ [_102521, _102523, _102525] : [-(rrx1(_102521, _102523)), _102525 = _102523, rrx1(_102521, _102525)], (320 ^ _92776) ^ [_102844, _102846, _102848] : [-(rrx1a(_102846, _102844)), _102848 = _102846, rrx1a(_102848, _102844)], (330 ^ _92776) ^ [_103167, _103169, _103171] : [-(rrx1a(_103167, _103169)), _103171 = _103169, rrx1a(_103167, _103171)], (340 ^ _92776) ^ [_103490, _103492, _103494] : [-(rrx2(_103492, _103490)), _103494 = _103492, rrx2(_103494, _103490)], (350 ^ _92776) ^ [_103813, _103815, _103817] : [-(rrx2(_103813, _103815)), _103817 = _103815, rrx2(_103813, _103817)], (360 ^ _92776) ^ [_104136, _104138, _104140] : [-(rrx2a(_104138, _104136)), _104140 = _104138, rrx2a(_104140, _104136)], (370 ^ _92776) ^ [_104459, _104461, _104463] : [-(rrx2a(_104459, _104461)), _104463 = _104461, rrx2a(_104459, _104463)], (380 ^ _92776) ^ [_104782, _104784, _104786] : [-(rrx3(_104784, _104782)), _104786 = _104784, rrx3(_104786, _104782)], (390 ^ _92776) ^ [_105105, _105107, _105109] : [-(rrx3(_105105, _105107)), _105109 = _105107, rrx3(_105105, _105109)], (400 ^ _92776) ^ [_105428, _105430, _105432] : [-(rrx3a(_105430, _105428)), _105432 = _105430, rrx3a(_105432, _105428)], (410 ^ _92776) ^ [_105751, _105753, _105755] : [-(rrx3a(_105751, _105753)), _105755 = _105753, rrx3a(_105751, _105755)], (420 ^ _92776) ^ [_106074, _106076, _106078] : [-(rrx4(_106076, _106074)), _106078 = _106076, rrx4(_106078, _106074)], (430 ^ _92776) ^ [_106397, _106399, _106401] : [-(rrx4(_106397, _106399)), _106401 = _106399, rrx4(_106397, _106401)], (440 ^ _92776) ^ [_106720, _106722, _106724] : [-(rrx4a(_106722, _106720)), _106724 = _106722, rrx4a(_106724, _106720)], (450 ^ _92776) ^ [_107043, _107045, _107047] : [-(rrx4a(_107043, _107045)), _107047 = _107045, rrx4a(_107043, _107047)], (460 ^ _92776) ^ [_107366, _107368, _107370] : [-(rrxa(_107368, _107366)), _107370 = _107368, rrxa(_107370, _107366)], (470 ^ _92776) ^ [_107689, _107691, _107693] : [-(rrxa(_107689, _107691)), _107693 = _107691, rrxa(_107689, _107693)], (480 ^ _92776) ^ [_107998, _108000] : [-(xsd_integer(_107998)), _108000 = _107998, xsd_integer(_108000)], (490 ^ _92776) ^ [_108293, _108295] : [-(xsd_string(_108293)), _108295 = _108293, xsd_string(_108295)], (500 ^ _92776) ^ [_108579] : [-(cowlThing(_108579))], (502 ^ _92776) ^ [_108621] : [cowlNothing(_108621)], (504 ^ _92776) ^ [_108744] : [xsd_string(_108744), xsd_integer(_108744)], (510 ^ _92776) ^ [_108897] : [-(xsd_integer(_108897)), -(xsd_string(_108897))], (516 ^ _92776) ^ [_109117] : [cUnsatisfiable(_109117), 520 ^ _92776 : [(521 ^ _92776) ^ [] : [-(rrx4(_109117, 519 ^ [_109117]))], (523 ^ _92776) ^ [] : [-(cc2(519 ^ [_109117]))], (536 ^ _92776) ^ [] : [-(rrx3(_109117, 534 ^ [_109117]))], (538 ^ _92776) ^ [] : [-(cc1(534 ^ [_109117]))], (525 ^ _92776) ^ [_109491] : [rrx3(_109117, _109491), cc2(_109491), cc1(_109491)]]], (540 ^ _92776) ^ [_109917] : [-(cUnsatisfiable(_109917)), 543 ^ _92776 : [(544 ^ _92776) ^ [_110076] : [rrx4(_109917, _110076), cc2(_110076)]], 552 ^ _92776 : [(553 ^ _92776) ^ [] : [-(rrx3(_109917, 551 ^ [_109917]))], (555 ^ _92776) ^ [] : [-(cc2(551 ^ [_109917]))], (557 ^ _92776) ^ [] : [-(cc1(551 ^ [_109917]))]], 558 ^ _92776 : [(559 ^ _92776) ^ [_110523] : [rrx3(_109917, _110523), cc1(_110523)]]], (567 ^ _92776) ^ [_110806, _110808, _110810] : [-(_110808 = _110806), rrx(_110810, _110808), rrx(_110810, _110806)], (577 ^ _92776) ^ [_111129, _111131, _111133] : [-(_111131 = _111129), rrx3(_111133, _111131), rrx3(_111133, _111129)], (587 ^ _92776) ^ [_111452, _111454, _111456] : [-(_111454 = _111452), rrx3a(_111456, _111454), rrx3a(_111456, _111452)], (597 ^ _92776) ^ [_111775, _111777, _111779] : [-(_111777 = _111775), rrx4(_111779, _111777), rrx4(_111779, _111775)], (607 ^ _92776) ^ [_112098, _112100, _112102] : [-(_112100 = _112098), rrx4a(_112102, _112100), rrx4a(_112102, _112098)], (617 ^ _92776) ^ [] : [-(cUnsatisfiable(i2003_11_14_17_18_32242))], (619 ^ _92776) ^ [_112460, _112462] : [rrx3(_112462, _112460), -(rrx(_112462, _112460))], (625 ^ _92776) ^ [_112670, _112672] : [rrx3a(_112672, _112670), -(rrxa(_112672, _112670))], (631 ^ _92776) ^ [_112880, _112882] : [rrx4a(_112882, _112880), -(rrxa(_112882, _112880))], (637 ^ _92776) ^ [_113090, _113092] : [rrx4(_113092, _113090), -(rrx2(_113092, _113090))], (643 ^ _92776) ^ [_113300, _113302] : [rrx3a(_113302, _113300), -(rrx1a(_113302, _113300))], (649 ^ _92776) ^ [_113510, _113512] : [rrx4a(_113512, _113510), -(rrx2a(_113512, _113510))], (655 ^ _92776) ^ [_113720, _113722] : [rrx3(_113722, _113720), -(rrx1(_113722, _113720))], (661 ^ _92776) ^ [_113910, _113912] : [rrx4(_113912, _113910), -(rrx(_113912, _113910))]], input).
% 0.57/1.37 ncf('1',plain,[cUnsatisfiable(i2003_11_14_17_18_32242), 525 : rrx3(i2003_11_14_17_18_32242, 534 ^ [i2003_11_14_17_18_32242]), 525 : cc2(534 ^ [i2003_11_14_17_18_32242]), 525 : cc1(534 ^ [i2003_11_14_17_18_32242])],start(516 ^ 0,bind([[_109117, _109491], [i2003_11_14_17_18_32242, 534 ^ [i2003_11_14_17_18_32242]]]))).
% 0.57/1.37 ncf('1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_18_32242))],extension(617 ^ 1)).
% 0.57/1.37 ncf('1.2',plain,[-(rrx3(i2003_11_14_17_18_32242, 534 ^ [i2003_11_14_17_18_32242])), rrx3(i2003_11_14_17_18_32242, 534 ^ [i2003_11_14_17_18_32242]), i2003_11_14_17_18_32242 = i2003_11_14_17_18_32242, 534 ^ [i2003_11_14_17_18_32242] = 534 ^ [i2003_11_14_17_18_32242]],extension(174 ^ 3,bind([[_98261, _98263, _98265, _98267], [534 ^ [i2003_11_14_17_18_32242], 534 ^ [i2003_11_14_17_18_32242], i2003_11_14_17_18_32242, i2003_11_14_17_18_32242]]))).
% 0.57/1.37 ncf('1.2.1',plain,[-(rrx3(i2003_11_14_17_18_32242, 534 ^ [i2003_11_14_17_18_32242])), rrx3(i2003_11_14_17_18_32242, 534 ^ [i2003_11_14_17_18_32242]), i2003_11_14_17_18_32242 = i2003_11_14_17_18_32242, 534 ^ [i2003_11_14_17_18_32242] = 534 ^ [i2003_11_14_17_18_32242]],extension(174 ^ 4,bind([[_98261, _98263, _98265, _98267], [534 ^ [i2003_11_14_17_18_32242], 534 ^ [i2003_11_14_17_18_32242], i2003_11_14_17_18_32242, i2003_11_14_17_18_32242]]))).
% 0.57/1.37 ncf('1.2.1.1',plain,[-(rrx3(i2003_11_14_17_18_32242, 534 ^ [i2003_11_14_17_18_32242])), rrx3(i2003_11_14_17_18_32242, 534 ^ [i2003_11_14_17_18_32242]), i2003_11_14_17_18_32242 = i2003_11_14_17_18_32242, 534 ^ [i2003_11_14_17_18_32242] = 534 ^ [i2003_11_14_17_18_32242]],extension(174 ^ 5,bind([[_98261, _98263, _98265, _98267], [534 ^ [i2003_11_14_17_18_32242], 534 ^ [i2003_11_14_17_18_32242], i2003_11_14_17_18_32242, i2003_11_14_17_18_32242]]))).
% 0.57/1.37 ncf('1.2.1.1.1',plain,[-(rrx3(i2003_11_14_17_18_32242, 534 ^ [i2003_11_14_17_18_32242]))],extension(536 ^ 6)).
% 0.57/1.37 ncf('1.2.1.1.2',plain,[-(i2003_11_14_17_18_32242 = i2003_11_14_17_18_32242)],extension(2 ^ 6,bind([[_92880], [i2003_11_14_17_18_32242]]))).
% 0.57/1.37 ncf('1.2.1.1.3',plain,[-(534 ^ [i2003_11_14_17_18_32242] = 534 ^ [i2003_11_14_17_18_32242])],extension(2 ^ 6,bind([[_92880], [534 ^ [i2003_11_14_17_18_32242]]]))).
% 0.57/1.37 ncf('1.2.1.2',plain,[-(i2003_11_14_17_18_32242 = i2003_11_14_17_18_32242)],extension(2 ^ 5,bind([[_92880], [i2003_11_14_17_18_32242]]))).
% 0.57/1.37 ncf('1.2.1.3',plain,[-(534 ^ [i2003_11_14_17_18_32242] = 534 ^ [i2003_11_14_17_18_32242])],extension(2 ^ 5,bind([[_92880], [534 ^ [i2003_11_14_17_18_32242]]]))).
% 0.57/1.37 ncf('1.2.2',plain,[-(i2003_11_14_17_18_32242 = i2003_11_14_17_18_32242)],extension(2 ^ 4,bind([[_92880], [i2003_11_14_17_18_32242]]))).
% 0.57/1.37 ncf('1.2.3',plain,[-(534 ^ [i2003_11_14_17_18_32242] = 534 ^ [i2003_11_14_17_18_32242])],extension(2 ^ 4,bind([[_92880], [534 ^ [i2003_11_14_17_18_32242]]]))).
% 0.57/1.37 ncf('1.3',plain,[-(cc2(534 ^ [i2003_11_14_17_18_32242])), 519 ^ [i2003_11_14_17_18_32242] = 534 ^ [i2003_11_14_17_18_32242], cc2(519 ^ [i2003_11_14_17_18_32242])],extension(60 ^ 3,bind([[_94684, _94686], [534 ^ [i2003_11_14_17_18_32242], 519 ^ [i2003_11_14_17_18_32242]]]))).
% 0.57/1.37 ncf('1.3.1',plain,[-(519 ^ [i2003_11_14_17_18_32242] = 534 ^ [i2003_11_14_17_18_32242]), rrx(i2003_11_14_17_18_32242, 519 ^ [i2003_11_14_17_18_32242]), rrx(i2003_11_14_17_18_32242, 534 ^ [i2003_11_14_17_18_32242])],extension(567 ^ 4,bind([[_110806, _110808, _110810], [534 ^ [i2003_11_14_17_18_32242], 519 ^ [i2003_11_14_17_18_32242], i2003_11_14_17_18_32242]]))).
% 0.57/1.37 ncf('1.3.1.1',plain,[-(rrx(i2003_11_14_17_18_32242, 519 ^ [i2003_11_14_17_18_32242])), rrx4(i2003_11_14_17_18_32242, 519 ^ [i2003_11_14_17_18_32242])],extension(661 ^ 5,bind([[_113910, _113912], [519 ^ [i2003_11_14_17_18_32242], i2003_11_14_17_18_32242]]))).
% 0.57/1.37 ncf('1.3.1.1.1',plain,[-(rrx4(i2003_11_14_17_18_32242, 519 ^ [i2003_11_14_17_18_32242]))],extension(521 ^ 6)).
% 0.57/1.37 ncf('1.3.1.2',plain,[-(rrx(i2003_11_14_17_18_32242, 534 ^ [i2003_11_14_17_18_32242])), rrx3(i2003_11_14_17_18_32242, 534 ^ [i2003_11_14_17_18_32242])],extension(619 ^ 5,bind([[_112460, _112462], [534 ^ [i2003_11_14_17_18_32242], i2003_11_14_17_18_32242]]))).
% 0.57/1.37 ncf('1.3.1.2.1',plain,[-(rrx3(i2003_11_14_17_18_32242, 534 ^ [i2003_11_14_17_18_32242]))],lemmata('x')).
% 0.57/1.37 ncf('1.3.2',plain,[-(cc2(519 ^ [i2003_11_14_17_18_32242]))],extension(523 ^ 4)).
% 0.57/1.37 ncf('1.4',plain,[-(cc1(534 ^ [i2003_11_14_17_18_32242]))],extension(538 ^ 3)).
% 0.57/1.37 %-----------------------------------------------------
% 0.57/1.37 End of proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------