%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS149+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n008.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:22 EDT 2023
% Result : Theorem 0.37s 1.37s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS149+1 : TPTP v8.1.2. Released v3.1.0.
% 0.11/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n008.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:00:39 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.37/1.37
% 0.37/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.37/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/1.37 %-----------------------------------------------------
% 0.37/1.37 ncf(matrix, plain, [(2034 ^ _168300) ^ [] : [cowlThing(2035 ^ []), -(cowlNothing(2035 ^ [])), 2047 ^ _168300 : [(2048 ^ _168300) ^ [] : [-(xsd_string(2044 ^ []))], (2050 ^ _168300) ^ [] : [-(xsd_integer(2044 ^ []))]], 2051 ^ _168300 : [(2052 ^ _168300) ^ [] : [xsd_integer(2044 ^ [])], (2054 ^ _168300) ^ [] : [xsd_string(2044 ^ [])]], cC216(iV3102), cC46(iV3102), cC30(iV3102), cC44(iV3102), cC28(iV3102), cC64(iV3102), cC14(iV3102), cowlThing(iV3102)], (2 ^ _168300) ^ [_168404] : [-(cowlThing(_168404))], (4 ^ _168300) ^ [_168446] : [cowlNothing(_168446)], (6 ^ _168300) ^ [_168569] : [xsd_string(_168569), xsd_integer(_168569)], (12 ^ _168300) ^ [_168722] : [-(xsd_integer(_168722)), -(xsd_string(_168722))], (18 ^ _168300) ^ [_168942] : [cC10(_168942), 21 ^ _168300 : [(22 ^ _168300) ^ [] : [cC8(_168942)], (24 ^ _168300) ^ [] : [cC2(_168942)]]], (26 ^ _168300) ^ [_169167] : [-(cC10(_169167)), -(cC8(_169167)), -(cC2(_169167))], (36 ^ _168300) ^ [_169473] : [cC100(_169473), 40 ^ _168300 : [(41 ^ _168300) ^ [] : [-(rR1(_169473, 39 ^ [_169473]))], (43 ^ _168300) ^ [] : [cC98(39 ^ [_169473])]]], (45 ^ _168300) ^ [_169762] : [-(cC100(_169762)), 46 ^ _168300 : [(47 ^ _168300) ^ [_169852] : [rR1(_169762, _169852), -(cC98(_169852))]]], (55 ^ _168300) ^ [_170129] : [cC102(_170129), 59 ^ _168300 : [(60 ^ _168300) ^ [] : [-(rR1(_170129, 58 ^ [_170129]))], (62 ^ _168300) ^ [] : [cC16(58 ^ [_170129])]]], (64 ^ _168300) ^ [_170418] : [-(cC102(_170418)), 65 ^ _168300 : [(66 ^ _168300) ^ [_170508] : [rR1(_170418, _170508), -(cC16(_170508))]]], (74 ^ _168300) ^ [_170785] : [cC104(_170785), 77 ^ _168300 : [(78 ^ _168300) ^ [] : [-(cC102(_170785))], (80 ^ _168300) ^ [] : [-(cC16(_170785))]]], (82 ^ _168300) ^ [_171008] : [-(cC104(_171008)), cC102(_171008), cC16(_171008)], (92 ^ _168300) ^ [_171308] : [cC106(_171308), 96 ^ _168300 : [(97 ^ _168300) ^ [] : [-(rR1(_171308, 95 ^ [_171308]))], (99 ^ _168300) ^ [] : [-(cC104(95 ^ [_171308]))]]], (101 ^ _168300) ^ [_171594] : [-(cC106(_171594)), 102 ^ _168300 : [(103 ^ _168300) ^ [_171682] : [rR1(_171594, _171682), cC104(_171682)]]], (111 ^ _168300) ^ [_171956] : [cC108(_171956), 114 ^ _168300 : [(115 ^ _168300) ^ [] : [cC106(_171956)], (117 ^ _168300) ^ [] : [cC16(_171956)]]], (119 ^ _168300) ^ [_172181] : [-(cC108(_172181)), -(cC106(_172181)), -(cC16(_172181))], (129 ^ _168300) ^ [_172487] : [cC110(_172487), 133 ^ _168300 : [(134 ^ _168300) ^ [] : [-(rR1(_172487, 132 ^ [_172487]))], (136 ^ _168300) ^ [] : [cC16(132 ^ [_172487])]]], (138 ^ _168300) ^ [_172776] : [-(cC110(_172776)), 139 ^ _168300 : [(140 ^ _168300) ^ [_172866] : [rR1(_172776, _172866), -(cC16(_172866))]]], (148 ^ _168300) ^ [_173143] : [cC112(_173143), 151 ^ _168300 : [(152 ^ _168300) ^ [] : [-(cC110(_173143))], (154 ^ _168300) ^ [] : [-(cC16(_173143))]]], (156 ^ _168300) ^ [_173366] : [-(cC112(_173366)), cC110(_173366), cC16(_173366)], (166 ^ _168300) ^ [_173666] : [cC114(_173666), 170 ^ _168300 : [(171 ^ _168300) ^ [] : [-(rR1(_173666, 169 ^ [_173666]))], (173 ^ _168300) ^ [] : [-(cC112(169 ^ [_173666]))]]], (175 ^ _168300) ^ [_173952] : [-(cC114(_173952)), 176 ^ _168300 : [(177 ^ _168300) ^ [_174040] : [rR1(_173952, _174040), cC112(_174040)]]], (185 ^ _168300) ^ [_174314] : [cC116(_174314), 188 ^ _168300 : [(189 ^ _168300) ^ [] : [cC16(_174314)], (191 ^ _168300) ^ [] : [cC114(_174314)]]], (193 ^ _168300) ^ [_174539] : [-(cC116(_174539)), -(cC16(_174539)), -(cC114(_174539))], (203 ^ _168300) ^ [_174845] : [cC118(_174845), 207 ^ _168300 : [(208 ^ _168300) ^ [] : [-(rR1(_174845, 206 ^ [_174845]))], (210 ^ _168300) ^ [] : [-(cC116(206 ^ [_174845]))]]], (212 ^ _168300) ^ [_175131] : [-(cC118(_175131)), 213 ^ _168300 : [(214 ^ _168300) ^ [_175219] : [rR1(_175131, _175219), cC116(_175219)]]], (222 ^ _168300) ^ [_175493] : [cC12(_175493), 226 ^ _168300 : [(227 ^ _168300) ^ [] : [-(rR1(_175493, 225 ^ [_175493]))], (229 ^ _168300) ^ [] : [-(cC10(225 ^ [_175493]))]]], (231 ^ _168300) ^ [_175779] : [-(cC12(_175779)), 232 ^ _168300 : [(233 ^ _168300) ^ [_175867] : [rR1(_175779, _175867), cC10(_175867)]]], (241 ^ _168300) ^ [_176141] : [cC120(_176141), 245 ^ _168300 : [(246 ^ _168300) ^ [] : [-(rR1(_176141, 244 ^ [_176141]))], (248 ^ _168300) ^ [] : [-(cC118(244 ^ [_176141]))]]], (250 ^ _168300) ^ [_176427] : [-(cC120(_176427)), 251 ^ _168300 : [(252 ^ _168300) ^ [_176515] : [rR1(_176427, _176515), cC118(_176515)]]], (260 ^ _168300) ^ [_176789] : [cC122(_176789), 264 ^ _168300 : [(265 ^ _168300) ^ [] : [-(rR1(_176789, 263 ^ [_176789]))], (267 ^ _168300) ^ [] : [cC16(263 ^ [_176789])]]], (269 ^ _168300) ^ [_177078] : [-(cC122(_177078)), 270 ^ _168300 : [(271 ^ _168300) ^ [_177168] : [rR1(_177078, _177168), -(cC16(_177168))]]], (279 ^ _168300) ^ [_177445] : [cC124(_177445), 282 ^ _168300 : [(283 ^ _168300) ^ [] : [-(cC122(_177445))], (285 ^ _168300) ^ [] : [-(cC16(_177445))]]], (287 ^ _168300) ^ [_177668] : [-(cC124(_177668)), cC122(_177668), cC16(_177668)], (297 ^ _168300) ^ [_177968] : [cC126(_177968), 301 ^ _168300 : [(302 ^ _168300) ^ [] : [-(rR1(_177968, 300 ^ [_177968]))], (304 ^ _168300) ^ [] : [-(cC124(300 ^ [_177968]))]]], (306 ^ _168300) ^ [_178254] : [-(cC126(_178254)), 307 ^ _168300 : [(308 ^ _168300) ^ [_178342] : [rR1(_178254, _178342), cC124(_178342)]]], (316 ^ _168300) ^ [_178616] : [cC128(_178616), 319 ^ _168300 : [(320 ^ _168300) ^ [] : [cC16(_178616)], (322 ^ _168300) ^ [] : [cC126(_178616)]]], (324 ^ _168300) ^ [_178841] : [-(cC128(_178841)), -(cC16(_178841)), -(cC126(_178841))], (334 ^ _168300) ^ [_179147] : [cC130(_179147), 338 ^ _168300 : [(339 ^ _168300) ^ [] : [-(rR1(_179147, 337 ^ [_179147]))], (341 ^ _168300) ^ [] : [-(cC128(337 ^ [_179147]))]]], (343 ^ _168300) ^ [_179433] : [-(cC130(_179433)), 344 ^ _168300 : [(345 ^ _168300) ^ [_179521] : [rR1(_179433, _179521), cC128(_179521)]]], (353 ^ _168300) ^ [_179795] : [cC132(_179795), 356 ^ _168300 : [(357 ^ _168300) ^ [] : [cC130(_179795)], (359 ^ _168300) ^ [] : [-(cC120(_179795))]]], (361 ^ _168300) ^ [_180019] : [-(cC132(_180019)), -(cC130(_180019)), cC120(_180019)], (371 ^ _168300) ^ [_180322] : [cC134(_180322), 374 ^ _168300 : [(375 ^ _168300) ^ [] : [cC132(_180322)], (377 ^ _168300) ^ [] : [cC108(_180322)]]], (379 ^ _168300) ^ [_180547] : [-(cC134(_180547)), -(cC132(_180547)), -(cC108(_180547))], (389 ^ _168300) ^ [_180853] : [cC136(_180853), 393 ^ _168300 : [(394 ^ _168300) ^ [] : [-(rR1(_180853, 392 ^ [_180853]))], (396 ^ _168300) ^ [] : [cC16(392 ^ [_180853])]]], (398 ^ _168300) ^ [_181142] : [-(cC136(_181142)), 399 ^ _168300 : [(400 ^ _168300) ^ [_181232] : [rR1(_181142, _181232), -(cC16(_181232))]]], (408 ^ _168300) ^ [_181509] : [cC138(_181509), 411 ^ _168300 : [(412 ^ _168300) ^ [] : [-(cC136(_181509))], (414 ^ _168300) ^ [] : [-(cC16(_181509))]]], (416 ^ _168300) ^ [_181732] : [-(cC138(_181732)), cC136(_181732), cC16(_181732)], (426 ^ _168300) ^ [_182032] : [cC14(_182032), 429 ^ _168300 : [(430 ^ _168300) ^ [] : [cC12(_182032)], (432 ^ _168300) ^ [] : [cC2(_182032)]]], (434 ^ _168300) ^ [_182257] : [-(cC14(_182257)), -(cC12(_182257)), -(cC2(_182257))], (444 ^ _168300) ^ [_182563] : [cC140(_182563), 448 ^ _168300 : [(449 ^ _168300) ^ [] : [-(rR1(_182563, 447 ^ [_182563]))], (451 ^ _168300) ^ [] : [-(cC138(447 ^ [_182563]))]]], (453 ^ _168300) ^ [_182849] : [-(cC140(_182849)), 454 ^ _168300 : [(455 ^ _168300) ^ [_182937] : [rR1(_182849, _182937), cC138(_182937)]]], (463 ^ _168300) ^ [_183211] : [cC142(_183211), 466 ^ _168300 : [(467 ^ _168300) ^ [] : [cC140(_183211)], (469 ^ _168300) ^ [] : [cC16(_183211)]]], (471 ^ _168300) ^ [_183436] : [-(cC142(_183436)), -(cC140(_183436)), -(cC16(_183436))], (481 ^ _168300) ^ [_183742] : [cC144(_183742), 485 ^ _168300 : [(486 ^ _168300) ^ [] : [-(rR1(_183742, 484 ^ [_183742]))], (488 ^ _168300) ^ [] : [cC16(484 ^ [_183742])]]], (490 ^ _168300) ^ [_184031] : [-(cC144(_184031)), 491 ^ _168300 : [(492 ^ _168300) ^ [_184121] : [rR1(_184031, _184121), -(cC16(_184121))]]], (500 ^ _168300) ^ [_184398] : [cC146(_184398), 503 ^ _168300 : [(504 ^ _168300) ^ [] : [-(cC144(_184398))], (506 ^ _168300) ^ [] : [-(cC16(_184398))]]], (508 ^ _168300) ^ [_184621] : [-(cC146(_184621)), cC144(_184621), cC16(_184621)], (518 ^ _168300) ^ [_184921] : [cC148(_184921), 522 ^ _168300 : [(523 ^ _168300) ^ [] : [-(rR1(_184921, 521 ^ [_184921]))], (525 ^ _168300) ^ [] : [-(cC146(521 ^ [_184921]))]]], (527 ^ _168300) ^ [_185207] : [-(cC148(_185207)), 528 ^ _168300 : [(529 ^ _168300) ^ [_185295] : [rR1(_185207, _185295), cC146(_185295)]]], (537 ^ _168300) ^ [_185569] : [cC150(_185569), 540 ^ _168300 : [(541 ^ _168300) ^ [] : [cC16(_185569)], (543 ^ _168300) ^ [] : [cC148(_185569)]]], (545 ^ _168300) ^ [_185794] : [-(cC150(_185794)), -(cC16(_185794)), -(cC148(_185794))], (555 ^ _168300) ^ [_186100] : [cC152(_186100), 559 ^ _168300 : [(560 ^ _168300) ^ [] : [-(rR1(_186100, 558 ^ [_186100]))], (562 ^ _168300) ^ [] : [-(cC150(558 ^ [_186100]))]]], (564 ^ _168300) ^ [_186386] : [-(cC152(_186386)), 565 ^ _168300 : [(566 ^ _168300) ^ [_186474] : [rR1(_186386, _186474), cC150(_186474)]]], (574 ^ _168300) ^ [_186748] : [cC154(_186748), 578 ^ _168300 : [(579 ^ _168300) ^ [] : [-(rR1(_186748, 577 ^ [_186748]))], (581 ^ _168300) ^ [] : [-(cC152(577 ^ [_186748]))]]], (583 ^ _168300) ^ [_187034] : [-(cC154(_187034)), 584 ^ _168300 : [(585 ^ _168300) ^ [_187122] : [rR1(_187034, _187122), cC152(_187122)]]], (593 ^ _168300) ^ [_187396] : [cC156(_187396), 597 ^ _168300 : [(598 ^ _168300) ^ [] : [-(rR1(_187396, 596 ^ [_187396]))], (600 ^ _168300) ^ [] : [cC16(596 ^ [_187396])]]], (602 ^ _168300) ^ [_187685] : [-(cC156(_187685)), 603 ^ _168300 : [(604 ^ _168300) ^ [_187775] : [rR1(_187685, _187775), -(cC16(_187775))]]], (612 ^ _168300) ^ [_188052] : [cC158(_188052), 615 ^ _168300 : [(616 ^ _168300) ^ [] : [-(cC156(_188052))], (618 ^ _168300) ^ [] : [-(cC16(_188052))]]], (620 ^ _168300) ^ [_188275] : [-(cC158(_188275)), cC156(_188275), cC16(_188275)], (630 ^ _168300) ^ [_188575] : [cC160(_188575), 634 ^ _168300 : [(635 ^ _168300) ^ [] : [-(rR1(_188575, 633 ^ [_188575]))], (637 ^ _168300) ^ [] : [-(cC158(633 ^ [_188575]))]]], (639 ^ _168300) ^ [_188861] : [-(cC160(_188861)), 640 ^ _168300 : [(641 ^ _168300) ^ [_188949] : [rR1(_188861, _188949), cC158(_188949)]]], (649 ^ _168300) ^ [_189223] : [cC162(_189223), 652 ^ _168300 : [(653 ^ _168300) ^ [] : [cC16(_189223)], (655 ^ _168300) ^ [] : [cC160(_189223)]]], (657 ^ _168300) ^ [_189448] : [-(cC162(_189448)), -(cC16(_189448)), -(cC160(_189448))], (667 ^ _168300) ^ [_189754] : [cC164(_189754), 671 ^ _168300 : [(672 ^ _168300) ^ [] : [-(rR1(_189754, 670 ^ [_189754]))], (674 ^ _168300) ^ [] : [-(cC162(670 ^ [_189754]))]]], (676 ^ _168300) ^ [_190040] : [-(cC164(_190040)), 677 ^ _168300 : [(678 ^ _168300) ^ [_190128] : [rR1(_190040, _190128), cC162(_190128)]]], (686 ^ _168300) ^ [_190402] : [cC166(_190402), 689 ^ _168300 : [(690 ^ _168300) ^ [] : [-(cC154(_190402))], (692 ^ _168300) ^ [] : [cC164(_190402)]]], (694 ^ _168300) ^ [_190626] : [-(cC166(_190626)), cC154(_190626), -(cC164(_190626))], (704 ^ _168300) ^ [_190929] : [cC168(_190929), 707 ^ _168300 : [(708 ^ _168300) ^ [] : [cC166(_190929)], (710 ^ _168300) ^ [] : [cC142(_190929)]]], (712 ^ _168300) ^ [_191154] : [-(cC168(_191154)), -(cC166(_191154)), -(cC142(_191154))], (722 ^ _168300) ^ [_191460] : [cC170(_191460), 726 ^ _168300 : [(727 ^ _168300) ^ [] : [-(rR1(_191460, 725 ^ [_191460]))], (729 ^ _168300) ^ [] : [cC168(725 ^ [_191460])]]], (731 ^ _168300) ^ [_191749] : [-(cC170(_191749)), 732 ^ _168300 : [(733 ^ _168300) ^ [_191839] : [rR1(_191749, _191839), -(cC168(_191839))]]], (741 ^ _168300) ^ [_192116] : [cC172(_192116), 745 ^ _168300 : [(746 ^ _168300) ^ [] : [-(rR1(_192116, 744 ^ [_192116]))], (748 ^ _168300) ^ [] : [cC16(744 ^ [_192116])]]], (750 ^ _168300) ^ [_192405] : [-(cC172(_192405)), 751 ^ _168300 : [(752 ^ _168300) ^ [_192495] : [rR1(_192405, _192495), -(cC16(_192495))]]], (760 ^ _168300) ^ [_192772] : [cC174(_192772), 763 ^ _168300 : [(764 ^ _168300) ^ [] : [-(cC172(_192772))], (766 ^ _168300) ^ [] : [-(cC16(_192772))]]], (768 ^ _168300) ^ [_192995] : [-(cC174(_192995)), cC172(_192995), cC16(_192995)], (778 ^ _168300) ^ [_193295] : [cC176(_193295), 782 ^ _168300 : [(783 ^ _168300) ^ [] : [-(rR1(_193295, 781 ^ [_193295]))], (785 ^ _168300) ^ [] : [-(cC174(781 ^ [_193295]))]]], (787 ^ _168300) ^ [_193581] : [-(cC176(_193581)), 788 ^ _168300 : [(789 ^ _168300) ^ [_193669] : [rR1(_193581, _193669), cC174(_193669)]]], (797 ^ _168300) ^ [_193943] : [cC178(_193943), 800 ^ _168300 : [(801 ^ _168300) ^ [] : [cC16(_193943)], (803 ^ _168300) ^ [] : [cC176(_193943)]]], (805 ^ _168300) ^ [_194168] : [-(cC178(_194168)), -(cC16(_194168)), -(cC176(_194168))], (815 ^ _168300) ^ [_194474] : [cC18(_194474), 819 ^ _168300 : [(820 ^ _168300) ^ [] : [-(rR1(_194474, 818 ^ [_194474]))], (822 ^ _168300) ^ [] : [cC16(818 ^ [_194474])]]], (824 ^ _168300) ^ [_194763] : [-(cC18(_194763)), 825 ^ _168300 : [(826 ^ _168300) ^ [_194853] : [rR1(_194763, _194853), -(cC16(_194853))]]], (834 ^ _168300) ^ [_195130] : [cC180(_195130), 838 ^ _168300 : [(839 ^ _168300) ^ [] : [-(rR1(_195130, 837 ^ [_195130]))], (841 ^ _168300) ^ [] : [cC16(837 ^ [_195130])]]], (843 ^ _168300) ^ [_195419] : [-(cC180(_195419)), 844 ^ _168300 : [(845 ^ _168300) ^ [_195509] : [rR1(_195419, _195509), -(cC16(_195509))]]], (853 ^ _168300) ^ [_195786] : [cC182(_195786), 856 ^ _168300 : [(857 ^ _168300) ^ [] : [-(cC16(_195786))], (859 ^ _168300) ^ [] : [-(cC180(_195786))]]], (861 ^ _168300) ^ [_196009] : [-(cC182(_196009)), cC16(_196009), cC180(_196009)], (871 ^ _168300) ^ [_196309] : [cC184(_196309), 875 ^ _168300 : [(876 ^ _168300) ^ [] : [-(rR1(_196309, 874 ^ [_196309]))], (878 ^ _168300) ^ [] : [-(cC182(874 ^ [_196309]))]]], (880 ^ _168300) ^ [_196595] : [-(cC184(_196595)), 881 ^ _168300 : [(882 ^ _168300) ^ [_196683] : [rR1(_196595, _196683), cC182(_196683)]]], (890 ^ _168300) ^ [_196957] : [cC186(_196957), 893 ^ _168300 : [(894 ^ _168300) ^ [] : [cC16(_196957)], (896 ^ _168300) ^ [] : [cC184(_196957)]]], (898 ^ _168300) ^ [_197182] : [-(cC186(_197182)), -(cC16(_197182)), -(cC184(_197182))], (908 ^ _168300) ^ [_197488] : [cC188(_197488), 912 ^ _168300 : [(913 ^ _168300) ^ [] : [-(rR1(_197488, 911 ^ [_197488]))], (915 ^ _168300) ^ [] : [-(cC186(911 ^ [_197488]))]]], (917 ^ _168300) ^ [_197774] : [-(cC188(_197774)), 918 ^ _168300 : [(919 ^ _168300) ^ [_197862] : [rR1(_197774, _197862), cC186(_197862)]]], (927 ^ _168300) ^ [_198136] : [cC190(_198136), 931 ^ _168300 : [(932 ^ _168300) ^ [] : [-(rR1(_198136, 930 ^ [_198136]))], (934 ^ _168300) ^ [] : [-(cC188(930 ^ [_198136]))]]], (936 ^ _168300) ^ [_198422] : [-(cC190(_198422)), 937 ^ _168300 : [(938 ^ _168300) ^ [_198510] : [rR1(_198422, _198510), cC188(_198510)]]], (946 ^ _168300) ^ [_198784] : [cC192(_198784), 950 ^ _168300 : [(951 ^ _168300) ^ [] : [-(rR1(_198784, 949 ^ [_198784]))], (953 ^ _168300) ^ [] : [cC16(949 ^ [_198784])]]], (955 ^ _168300) ^ [_199073] : [-(cC192(_199073)), 956 ^ _168300 : [(957 ^ _168300) ^ [_199163] : [rR1(_199073, _199163), -(cC16(_199163))]]], (965 ^ _168300) ^ [_199440] : [cC194(_199440), 968 ^ _168300 : [(969 ^ _168300) ^ [] : [-(cC192(_199440))], (971 ^ _168300) ^ [] : [-(cC16(_199440))]]], (973 ^ _168300) ^ [_199663] : [-(cC194(_199663)), cC192(_199663), cC16(_199663)], (983 ^ _168300) ^ [_199963] : [cC196(_199963), 987 ^ _168300 : [(988 ^ _168300) ^ [] : [-(rR1(_199963, 986 ^ [_199963]))], (990 ^ _168300) ^ [] : [-(cC194(986 ^ [_199963]))]]], (992 ^ _168300) ^ [_200249] : [-(cC196(_200249)), 993 ^ _168300 : [(994 ^ _168300) ^ [_200337] : [rR1(_200249, _200337), cC194(_200337)]]], (1002 ^ _168300) ^ [_200611] : [cC198(_200611), 1005 ^ _168300 : [(1006 ^ _168300) ^ [] : [cC196(_200611)], (1008 ^ _168300) ^ [] : [cC16(_200611)]]], (1010 ^ _168300) ^ [_200836] : [-(cC198(_200836)), -(cC196(_200836)), -(cC16(_200836))], (1020 ^ _168300) ^ [_201142] : [cC20(_201142), 1023 ^ _168300 : [(1024 ^ _168300) ^ [] : [-(cC18(_201142))], (1026 ^ _168300) ^ [] : [-(cC16(_201142))]]], (1028 ^ _168300) ^ [_201365] : [-(cC20(_201365)), cC18(_201365), cC16(_201365)], (1038 ^ _168300) ^ [_201665] : [cC200(_201665), 1042 ^ _168300 : [(1043 ^ _168300) ^ [] : [-(rR1(_201665, 1041 ^ [_201665]))], (1045 ^ _168300) ^ [] : [-(cC198(1041 ^ [_201665]))]]], (1047 ^ _168300) ^ [_201951] : [-(cC200(_201951)), 1048 ^ _168300 : [(1049 ^ _168300) ^ [_202039] : [rR1(_201951, _202039), cC198(_202039)]]], (1057 ^ _168300) ^ [_202313] : [cC202(_202313), 1060 ^ _168300 : [(1061 ^ _168300) ^ [] : [-(cC190(_202313))], (1063 ^ _168300) ^ [] : [cC200(_202313)]]], (1065 ^ _168300) ^ [_202537] : [-(cC202(_202537)), cC190(_202537), -(cC200(_202537))], (1075 ^ _168300) ^ [_202840] : [cC204(_202840), 1078 ^ _168300 : [(1079 ^ _168300) ^ [] : [cC178(_202840)], (1081 ^ _168300) ^ [] : [cC202(_202840)]]], (1083 ^ _168300) ^ [_203065] : [-(cC204(_203065)), -(cC178(_203065)), -(cC202(_203065))], (1093 ^ _168300) ^ [_203371] : [cC206(_203371), 1096 ^ _168300 : [(1097 ^ _168300) ^ [] : [-(cC170(_203371))], (1099 ^ _168300) ^ [] : [-(cC204(_203371))]]], (1101 ^ _168300) ^ [_203594] : [-(cC206(_203594)), cC170(_203594), cC204(_203594)], (1111 ^ _168300) ^ [_203894] : [cC208(_203894), 1115 ^ _168300 : [(1116 ^ _168300) ^ [] : [-(rR1(_203894, 1114 ^ [_203894]))], (1118 ^ _168300) ^ [] : [-(cC206(1114 ^ [_203894]))]]], (1120 ^ _168300) ^ [_204180] : [-(cC208(_204180)), 1121 ^ _168300 : [(1122 ^ _168300) ^ [_204268] : [rR1(_204180, _204268), cC206(_204268)]]], (1130 ^ _168300) ^ [_204542] : [cC210(_204542), 1133 ^ _168300 : [(1134 ^ _168300) ^ [] : [cC208(_204542)], (1136 ^ _168300) ^ [] : [cC134(_204542)]]], (1138 ^ _168300) ^ [_204767] : [-(cC210(_204767)), -(cC208(_204767)), -(cC134(_204767))], (1148 ^ _168300) ^ [_205073] : [cC212(_205073), 1152 ^ _168300 : [(1153 ^ _168300) ^ [] : [-(rR1(_205073, 1151 ^ [_205073]))], (1155 ^ _168300) ^ [] : [-(cC210(1151 ^ [_205073]))]]], (1157 ^ _168300) ^ [_205359] : [-(cC212(_205359)), 1158 ^ _168300 : [(1159 ^ _168300) ^ [_205447] : [rR1(_205359, _205447), cC210(_205447)]]], (1167 ^ _168300) ^ [_205721] : [cC214(_205721), 1170 ^ _168300 : [(1171 ^ _168300) ^ [] : [-(cC100(_205721))], (1173 ^ _168300) ^ [] : [cC212(_205721)]]], (1175 ^ _168300) ^ [_205945] : [-(cC214(_205945)), cC100(_205945), -(cC212(_205945))], (1185 ^ _168300) ^ [_206248] : [cC216(_206248), 1188 ^ _168300 : [(1189 ^ _168300) ^ [] : [cC214(_206248)], (1191 ^ _168300) ^ [] : [-(cC64(_206248))]]], (1193 ^ _168300) ^ [_206472] : [-(cC216(_206472)), -(cC214(_206472)), cC64(_206472)], (1203 ^ _168300) ^ [_206775] : [cC22(_206775), 1207 ^ _168300 : [(1208 ^ _168300) ^ [] : [-(rR1(_206775, 1206 ^ [_206775]))], (1210 ^ _168300) ^ [] : [-(cC20(1206 ^ [_206775]))]]], (1212 ^ _168300) ^ [_207061] : [-(cC22(_207061)), 1213 ^ _168300 : [(1214 ^ _168300) ^ [_207149] : [rR1(_207061, _207149), cC20(_207149)]]], (1222 ^ _168300) ^ [_207423] : [cC24(_207423), 1225 ^ _168300 : [(1226 ^ _168300) ^ [] : [cC22(_207423)], (1228 ^ _168300) ^ [] : [cC16(_207423)]]], (1230 ^ _168300) ^ [_207648] : [-(cC24(_207648)), -(cC22(_207648)), -(cC16(_207648))], (1240 ^ _168300) ^ [_207954] : [cC26(_207954), 1244 ^ _168300 : [(1245 ^ _168300) ^ [] : [-(rR1(_207954, 1243 ^ [_207954]))], (1247 ^ _168300) ^ [] : [-(cC24(1243 ^ [_207954]))]]], (1249 ^ _168300) ^ [_208240] : [-(cC26(_208240)), 1250 ^ _168300 : [(1251 ^ _168300) ^ [_208328] : [rR1(_208240, _208328), cC24(_208328)]]], (1259 ^ _168300) ^ [_208602] : [cC28(_208602), 1262 ^ _168300 : [(1263 ^ _168300) ^ [] : [cC26(_208602)], (1265 ^ _168300) ^ [] : [cC16(_208602)]]], (1267 ^ _168300) ^ [_208827] : [-(cC28(_208827)), -(cC26(_208827)), -(cC16(_208827))], (1277 ^ _168300) ^ [_209133] : [cC30(_209133), 1280 ^ _168300 : [(1281 ^ _168300) ^ [] : [-(cC14(_209133))], (1283 ^ _168300) ^ [] : [-(cC28(_209133))]]], (1285 ^ _168300) ^ [_209356] : [-(cC30(_209356)), cC14(_209356), cC28(_209356)], (1295 ^ _168300) ^ [_209656] : [cC34(_209656), 1299 ^ _168300 : [(1300 ^ _168300) ^ [] : [-(rR1(_209656, 1298 ^ [_209656]))], (1302 ^ _168300) ^ [] : [cC32(1298 ^ [_209656])]]], (1304 ^ _168300) ^ [_209945] : [-(cC34(_209945)), 1305 ^ _168300 : [(1306 ^ _168300) ^ [_210035] : [rR1(_209945, _210035), -(cC32(_210035))]]], (1314 ^ _168300) ^ [_210312] : [cC36(_210312), 1317 ^ _168300 : [(1318 ^ _168300) ^ [] : [-(cC32(_210312))], (1320 ^ _168300) ^ [] : [-(cC34(_210312))]]], (1322 ^ _168300) ^ [_210535] : [-(cC36(_210535)), cC32(_210535), cC34(_210535)], (1332 ^ _168300) ^ [_210835] : [cC38(_210835), 1336 ^ _168300 : [(1337 ^ _168300) ^ [] : [-(rR1(_210835, 1335 ^ [_210835]))], (1339 ^ _168300) ^ [] : [-(cC36(1335 ^ [_210835]))]]], (1341 ^ _168300) ^ [_211121] : [-(cC38(_211121)), 1342 ^ _168300 : [(1343 ^ _168300) ^ [_211209] : [rR1(_211121, _211209), cC36(_211209)]]], (1351 ^ _168300) ^ [_211483] : [cC4(_211483), 1355 ^ _168300 : [(1356 ^ _168300) ^ [] : [-(rR1(_211483, 1354 ^ [_211483]))], (1358 ^ _168300) ^ [] : [cC2(1354 ^ [_211483])]]], (1360 ^ _168300) ^ [_211772] : [-(cC4(_211772)), 1361 ^ _168300 : [(1362 ^ _168300) ^ [_211862] : [rR1(_211772, _211862), -(cC2(_211862))]]], (1370 ^ _168300) ^ [_212139] : [cC40(_212139), 1373 ^ _168300 : [(1374 ^ _168300) ^ [] : [cC38(_212139)], (1376 ^ _168300) ^ [] : [cC32(_212139)]]], (1378 ^ _168300) ^ [_212364] : [-(cC40(_212364)), -(cC38(_212364)), -(cC32(_212364))], (1388 ^ _168300) ^ [_212670] : [cC42(_212670), 1392 ^ _168300 : [(1393 ^ _168300) ^ [] : [-(rR1(_212670, 1391 ^ [_212670]))], (1395 ^ _168300) ^ [] : [-(cC40(1391 ^ [_212670]))]]], (1397 ^ _168300) ^ [_212956] : [-(cC42(_212956)), 1398 ^ _168300 : [(1399 ^ _168300) ^ [_213044] : [rR1(_212956, _213044), cC40(_213044)]]], (1407 ^ _168300) ^ [_213318] : [cC44(_213318), 1410 ^ _168300 : [(1411 ^ _168300) ^ [] : [cC32(_213318)], (1413 ^ _168300) ^ [] : [cC42(_213318)]]], (1415 ^ _168300) ^ [_213543] : [-(cC44(_213543)), -(cC32(_213543)), -(cC42(_213543))], (1425 ^ _168300) ^ [_213849] : [cC46(_213849), 1428 ^ _168300 : [(1429 ^ _168300) ^ [] : [-(cC30(_213849))], (1431 ^ _168300) ^ [] : [-(cC44(_213849))]]], (1433 ^ _168300) ^ [_214072] : [-(cC46(_214072)), cC30(_214072), cC44(_214072)], (1443 ^ _168300) ^ [_214372] : [cC48(_214372), 1447 ^ _168300 : [(1448 ^ _168300) ^ [] : [-(rR1(_214372, 1446 ^ [_214372]))], (1450 ^ _168300) ^ [] : [cC16(1446 ^ [_214372])]]], (1452 ^ _168300) ^ [_214661] : [-(cC48(_214661)), 1453 ^ _168300 : [(1454 ^ _168300) ^ [_214751] : [rR1(_214661, _214751), -(cC16(_214751))]]], (1462 ^ _168300) ^ [_215028] : [cC50(_215028), 1466 ^ _168300 : [(1467 ^ _168300) ^ [] : [-(rR1(_215028, 1465 ^ [_215028]))], (1469 ^ _168300) ^ [] : [cC16(1465 ^ [_215028])]]], (1471 ^ _168300) ^ [_215317] : [-(cC50(_215317)), 1472 ^ _168300 : [(1473 ^ _168300) ^ [_215407] : [rR1(_215317, _215407), -(cC16(_215407))]]], (1481 ^ _168300) ^ [_215684] : [cC52(_215684), 1484 ^ _168300 : [(1485 ^ _168300) ^ [] : [-(cC50(_215684))], (1487 ^ _168300) ^ [] : [-(cC16(_215684))]]], (1489 ^ _168300) ^ [_215907] : [-(cC52(_215907)), cC50(_215907), cC16(_215907)], (1499 ^ _168300) ^ [_216207] : [cC54(_216207), 1503 ^ _168300 : [(1504 ^ _168300) ^ [] : [-(rR1(_216207, 1502 ^ [_216207]))], (1506 ^ _168300) ^ [] : [-(cC52(1502 ^ [_216207]))]]], (1508 ^ _168300) ^ [_216493] : [-(cC54(_216493)), 1509 ^ _168300 : [(1510 ^ _168300) ^ [_216581] : [rR1(_216493, _216581), cC52(_216581)]]], (1518 ^ _168300) ^ [_216855] : [cC56(_216855), 1521 ^ _168300 : [(1522 ^ _168300) ^ [] : [cC16(_216855)], (1524 ^ _168300) ^ [] : [cC54(_216855)]]], (1526 ^ _168300) ^ [_217080] : [-(cC56(_217080)), -(cC16(_217080)), -(cC54(_217080))], (1536 ^ _168300) ^ [_217386] : [cC58(_217386), 1540 ^ _168300 : [(1541 ^ _168300) ^ [] : [-(rR1(_217386, 1539 ^ [_217386]))], (1543 ^ _168300) ^ [] : [-(cC56(1539 ^ [_217386]))]]], (1545 ^ _168300) ^ [_217672] : [-(cC58(_217672)), 1546 ^ _168300 : [(1547 ^ _168300) ^ [_217760] : [rR1(_217672, _217760), cC56(_217760)]]], (1555 ^ _168300) ^ [_218034] : [cC6(_218034), 1558 ^ _168300 : [(1559 ^ _168300) ^ [] : [-(cC2(_218034))], (1561 ^ _168300) ^ [] : [-(cC4(_218034))]]], (1563 ^ _168300) ^ [_218257] : [-(cC6(_218257)), cC2(_218257), cC4(_218257)], (1573 ^ _168300) ^ [_218557] : [cC60(_218557), 1576 ^ _168300 : [(1577 ^ _168300) ^ [] : [-(cC48(_218557))], (1579 ^ _168300) ^ [] : [cC58(_218557)]]], (1581 ^ _168300) ^ [_218781] : [-(cC60(_218781)), cC48(_218781), -(cC58(_218781))], (1591 ^ _168300) ^ [_219084] : [cC62(_219084), 1595 ^ _168300 : [(1596 ^ _168300) ^ [] : [-(rR1(_219084, 1594 ^ [_219084]))], (1598 ^ _168300) ^ [] : [-(cC60(1594 ^ [_219084]))]]], (1600 ^ _168300) ^ [_219370] : [-(cC62(_219370)), 1601 ^ _168300 : [(1602 ^ _168300) ^ [_219458] : [rR1(_219370, _219458), cC60(_219458)]]], (1610 ^ _168300) ^ [_219732] : [cC64(_219732), 1613 ^ _168300 : [(1614 ^ _168300) ^ [] : [cC62(_219732)], (1616 ^ _168300) ^ [] : [-(cTOP(_219732))]]], (1618 ^ _168300) ^ [_219956] : [-(cC64(_219956)), -(cC62(_219956)), cTOP(_219956)], (1628 ^ _168300) ^ [_220259] : [cC66(_220259), 1632 ^ _168300 : [(1633 ^ _168300) ^ [] : [-(rR1(_220259, 1631 ^ [_220259]))], (1635 ^ _168300) ^ [] : [cC16(1631 ^ [_220259])]]], (1637 ^ _168300) ^ [_220548] : [-(cC66(_220548)), 1638 ^ _168300 : [(1639 ^ _168300) ^ [_220638] : [rR1(_220548, _220638), -(cC16(_220638))]]], (1647 ^ _168300) ^ [_220915] : [cC68(_220915), 1650 ^ _168300 : [(1651 ^ _168300) ^ [] : [-(cC66(_220915))], (1653 ^ _168300) ^ [] : [-(cC16(_220915))]]], (1655 ^ _168300) ^ [_221138] : [-(cC68(_221138)), cC66(_221138), cC16(_221138)], (1665 ^ _168300) ^ [_221438] : [cC70(_221438), 1669 ^ _168300 : [(1670 ^ _168300) ^ [] : [-(rR1(_221438, 1668 ^ [_221438]))], (1672 ^ _168300) ^ [] : [-(cC68(1668 ^ [_221438]))]]], (1674 ^ _168300) ^ [_221724] : [-(cC70(_221724)), 1675 ^ _168300 : [(1676 ^ _168300) ^ [_221812] : [rR1(_221724, _221812), cC68(_221812)]]], (1684 ^ _168300) ^ [_222086] : [cC72(_222086), 1687 ^ _168300 : [(1688 ^ _168300) ^ [] : [cC70(_222086)], (1690 ^ _168300) ^ [] : [cC16(_222086)]]], (1692 ^ _168300) ^ [_222311] : [-(cC72(_222311)), -(cC70(_222311)), -(cC16(_222311))], (1702 ^ _168300) ^ [_222617] : [cC74(_222617), 1706 ^ _168300 : [(1707 ^ _168300) ^ [] : [-(rR1(_222617, 1705 ^ [_222617]))], (1709 ^ _168300) ^ [] : [cC16(1705 ^ [_222617])]]], (1711 ^ _168300) ^ [_222906] : [-(cC74(_222906)), 1712 ^ _168300 : [(1713 ^ _168300) ^ [_222996] : [rR1(_222906, _222996), -(cC16(_222996))]]], (1721 ^ _168300) ^ [_223273] : [cC76(_223273), 1724 ^ _168300 : [(1725 ^ _168300) ^ [] : [-(cC74(_223273))], (1727 ^ _168300) ^ [] : [-(cC16(_223273))]]], (1729 ^ _168300) ^ [_223496] : [-(cC76(_223496)), cC74(_223496), cC16(_223496)], (1739 ^ _168300) ^ [_223796] : [cC78(_223796), 1743 ^ _168300 : [(1744 ^ _168300) ^ [] : [-(rR1(_223796, 1742 ^ [_223796]))], (1746 ^ _168300) ^ [] : [-(cC76(1742 ^ [_223796]))]]], (1748 ^ _168300) ^ [_224082] : [-(cC78(_224082)), 1749 ^ _168300 : [(1750 ^ _168300) ^ [_224170] : [rR1(_224082, _224170), cC76(_224170)]]], (1758 ^ _168300) ^ [_224444] : [cC8(_224444), 1762 ^ _168300 : [(1763 ^ _168300) ^ [] : [-(rR1(_224444, 1761 ^ [_224444]))], (1765 ^ _168300) ^ [] : [-(cC6(1761 ^ [_224444]))]]], (1767 ^ _168300) ^ [_224730] : [-(cC8(_224730)), 1768 ^ _168300 : [(1769 ^ _168300) ^ [_224818] : [rR1(_224730, _224818), cC6(_224818)]]], (1777 ^ _168300) ^ [_225092] : [cC80(_225092), 1780 ^ _168300 : [(1781 ^ _168300) ^ [] : [cC16(_225092)], (1783 ^ _168300) ^ [] : [cC78(_225092)]]], (1785 ^ _168300) ^ [_225317] : [-(cC80(_225317)), -(cC16(_225317)), -(cC78(_225317))], (1795 ^ _168300) ^ [_225623] : [cC82(_225623), 1799 ^ _168300 : [(1800 ^ _168300) ^ [] : [-(rR1(_225623, 1798 ^ [_225623]))], (1802 ^ _168300) ^ [] : [-(cC80(1798 ^ [_225623]))]]], (1804 ^ _168300) ^ [_225909] : [-(cC82(_225909)), 1805 ^ _168300 : [(1806 ^ _168300) ^ [_225997] : [rR1(_225909, _225997), cC80(_225997)]]], (1814 ^ _168300) ^ [_226271] : [cC84(_226271), 1818 ^ _168300 : [(1819 ^ _168300) ^ [] : [-(rR1(_226271, 1817 ^ [_226271]))], (1821 ^ _168300) ^ [] : [-(cC82(1817 ^ [_226271]))]]], (1823 ^ _168300) ^ [_226557] : [-(cC84(_226557)), 1824 ^ _168300 : [(1825 ^ _168300) ^ [_226645] : [rR1(_226557, _226645), cC82(_226645)]]], (1833 ^ _168300) ^ [_226919] : [cC86(_226919), 1837 ^ _168300 : [(1838 ^ _168300) ^ [] : [-(rR1(_226919, 1836 ^ [_226919]))], (1840 ^ _168300) ^ [] : [cC16(1836 ^ [_226919])]]], (1842 ^ _168300) ^ [_227208] : [-(cC86(_227208)), 1843 ^ _168300 : [(1844 ^ _168300) ^ [_227298] : [rR1(_227208, _227298), -(cC16(_227298))]]], (1852 ^ _168300) ^ [_227575] : [cC88(_227575), 1855 ^ _168300 : [(1856 ^ _168300) ^ [] : [-(cC86(_227575))], (1858 ^ _168300) ^ [] : [-(cC16(_227575))]]], (1860 ^ _168300) ^ [_227798] : [-(cC88(_227798)), cC86(_227798), cC16(_227798)], (1870 ^ _168300) ^ [_228098] : [cC90(_228098), 1874 ^ _168300 : [(1875 ^ _168300) ^ [] : [-(rR1(_228098, 1873 ^ [_228098]))], (1877 ^ _168300) ^ [] : [-(cC88(1873 ^ [_228098]))]]], (1879 ^ _168300) ^ [_228384] : [-(cC90(_228384)), 1880 ^ _168300 : [(1881 ^ _168300) ^ [_228472] : [rR1(_228384, _228472), cC88(_228472)]]], (1889 ^ _168300) ^ [_228746] : [cC92(_228746), 1892 ^ _168300 : [(1893 ^ _168300) ^ [] : [cC90(_228746)], (1895 ^ _168300) ^ [] : [cC16(_228746)]]], (1897 ^ _168300) ^ [_228971] : [-(cC92(_228971)), -(cC90(_228971)), -(cC16(_228971))], (1907 ^ _168300) ^ [_229277] : [cC94(_229277), 1911 ^ _168300 : [(1912 ^ _168300) ^ [] : [-(rR1(_229277, 1910 ^ [_229277]))], (1914 ^ _168300) ^ [] : [-(cC92(1910 ^ [_229277]))]]], (1916 ^ _168300) ^ [_229563] : [-(cC94(_229563)), 1917 ^ _168300 : [(1918 ^ _168300) ^ [_229651] : [rR1(_229563, _229651), cC92(_229651)]]], (1926 ^ _168300) ^ [_229925] : [cC96(_229925), 1929 ^ _168300 : [(1930 ^ _168300) ^ [] : [-(cC84(_229925))], (1932 ^ _168300) ^ [] : [cC94(_229925)]]], (1934 ^ _168300) ^ [_230149] : [-(cC96(_230149)), cC84(_230149), -(cC94(_230149))], (1944 ^ _168300) ^ [_230452] : [cC98(_230452), 1947 ^ _168300 : [(1948 ^ _168300) ^ [] : [cC72(_230452)], (1950 ^ _168300) ^ [] : [cC96(_230452)]]], (1952 ^ _168300) ^ [_230677] : [-(cC98(_230677)), -(cC72(_230677)), -(cC96(_230677))], (1962 ^ _168300) ^ [_230983] : [cTEST(_230983), 1965 ^ _168300 : [(1966 ^ _168300) ^ [] : [-(cC216(_230983))], (1968 ^ _168300) ^ [] : [-(cC46(_230983))]]], (1970 ^ _168300) ^ [_231206] : [-(cTEST(_231206)), cC216(_231206), cC46(_231206)], (1980 ^ _168300) ^ [] : [-(cTEST(iV3102))], (1982 ^ _168300) ^ [] : [-(cowlThing(iV3102))], (1984 ^ _168300) ^ [_231583] : [rR1(iV3102, _231583), cC60(_231583)], (1990 ^ _168300) ^ [_231772] : [rR1(iV3102, _231772), cC10(_231772)], (1996 ^ _168300) ^ [] : [-(cTOP(iV3102))], (1998 ^ _168300) ^ [_232014] : [rR1(iV3102, _232014), cC24(_232014)], (2004 ^ _168300) ^ [] : [cC42(iV3102)], (2006 ^ _168300) ^ [] : [cC12(iV3102)], (2008 ^ _168300) ^ [] : [cC26(iV3102)], (2010 ^ _168300) ^ [_232359] : [rR1(iV3102, _232359), -(cC98(_232359))], (2016 ^ _168300) ^ [] : [cC214(iV3102)], (2018 ^ _168300) ^ [] : [cC62(iV3102)], (2026 ^ _168300) ^ [] : [cC16(iV3102)], (2028 ^ _168300) ^ [] : [cC2(iV3102)], (2030 ^ _168300) ^ [] : [cC32(iV3102)], (2032 ^ _168300) ^ [] : [cC100(iV3102)], (2020 ^ _168300) ^ [_232651] : [rR1(iV3102, _232651), cC40(_232651)]], input).
% 0.37/1.37 ncf('1',plain,[cowlNothing(2035 ^ [])],start(4 ^ 0,bind([[_168446], [2035 ^ []]]))).
% 0.37/1.37 ncf('1.1',plain,[-(cowlNothing(2035 ^ [])), cowlThing(2035 ^ []), 2048 : -(xsd_string(2044 ^ [])), 2052 : xsd_integer(2044 ^ []), 2052 : cC216(iV3102), 2052 : cC46(iV3102), 2052 : cC30(iV3102), 2052 : cC44(iV3102), 2052 : cC28(iV3102), 2052 : cC64(iV3102), 2052 : cC14(iV3102), 2052 : cowlThing(iV3102)],extension(2034 ^ 1)).
% 0.37/1.37 ncf('1.1.1',plain,[-(cowlThing(2035 ^ []))],extension(2 ^ 2,bind([[_168404], [2035 ^ []]]))).
% 0.37/1.37 ncf('1.1.2',plain,[xsd_string(2044 ^ []), xsd_integer(2044 ^ [])],extension(6 ^ 4,bind([[_168569], [2044 ^ []]]))).
% 0.37/1.37 ncf('1.1.2.1',plain,[-(xsd_integer(2044 ^ []))],extension(2050 ^ 5)).
% 0.37/1.37 ncf('1.1.3',plain,[-(xsd_integer(2044 ^ [])), -(xsd_string(2044 ^ []))],extension(12 ^ 4,bind([[_168722], [2044 ^ []]]))).
% 0.37/1.37 ncf('1.1.3.1',plain,[xsd_string(2044 ^ [])],extension(2054 ^ 5)).
% 0.37/1.37 ncf('1.1.4',plain,[-(cC216(iV3102)), cTEST(iV3102)],extension(1962 ^ 2,bind([[_230983], [iV3102]]))).
% 0.37/1.37 ncf('1.1.4.1',plain,[-(cTEST(iV3102))],extension(1980 ^ 3)).
% 0.37/1.37 ncf('1.1.5',plain,[-(cC46(iV3102)), cTEST(iV3102)],extension(1962 ^ 2,bind([[_230983], [iV3102]]))).
% 0.37/1.37 ncf('1.1.5.1',plain,[-(cTEST(iV3102))],extension(1980 ^ 3)).
% 0.37/1.37 ncf('1.1.6',plain,[-(cC30(iV3102)), cC46(iV3102)],extension(1425 ^ 2,bind([[_213849], [iV3102]]))).
% 0.37/1.37 ncf('1.1.6.1',plain,[-(cC46(iV3102))],lemmata('[1].x')).
% 0.37/1.37 ncf('1.1.7',plain,[-(cC44(iV3102)), -(cC32(iV3102)), -(cC42(iV3102))],extension(1415 ^ 2,bind([[_213543], [iV3102]]))).
% 0.37/1.37 ncf('1.1.7.1',plain,[cC32(iV3102)],extension(2030 ^ 3)).
% 0.37/1.37 ncf('1.1.7.2',plain,[cC42(iV3102)],extension(2004 ^ 3)).
% 0.37/1.37 ncf('1.1.8',plain,[-(cC28(iV3102)), -(cC26(iV3102)), -(cC16(iV3102))],extension(1267 ^ 2,bind([[_208827], [iV3102]]))).
% 0.37/1.37 ncf('1.1.8.1',plain,[cC26(iV3102)],extension(2008 ^ 3)).
% 0.37/1.37 ncf('1.1.8.2',plain,[cC16(iV3102)],extension(2026 ^ 3)).
% 0.37/1.37 ncf('1.1.9',plain,[-(cC64(iV3102)), cC216(iV3102)],extension(1185 ^ 2,bind([[_206248], [iV3102]]))).
% 0.37/1.37 ncf('1.1.9.1',plain,[-(cC216(iV3102))],lemmata('[1].x')).
% 0.37/1.37 ncf('1.1.10',plain,[-(cC14(iV3102)), -(cC12(iV3102)), -(cC2(iV3102))],extension(434 ^ 2,bind([[_182257], [iV3102]]))).
% 0.37/1.37 ncf('1.1.10.1',plain,[cC12(iV3102)],extension(2006 ^ 3)).
% 0.37/1.37 ncf('1.1.10.2',plain,[cC2(iV3102)],extension(2028 ^ 3)).
% 0.37/1.37 ncf('1.1.11',plain,[-(cowlThing(iV3102))],extension(2 ^ 2,bind([[_168404], [iV3102]]))).
% 0.37/1.37 %-----------------------------------------------------
% 0.37/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------