↑ Up

nanoCoP---2.0.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : nanoCoP---2.0
% Problem  : KRS161+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : nanocop.sh %s %d

% Computer : n004.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:24 EDT 2023

% Result   : Theorem 0.64s 1.39s
% Output   : Proof 0.64s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12  % Problem  : KRS161+1 : TPTP v8.1.2. Released v3.1.0.
% 0.04/0.13  % Command  : nanocop.sh %s %d
% 0.12/0.34  % Computer : n004.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 300
% 0.12/0.34  % DateTime : Thu May 18 22:52:54 EDT 2023
% 0.12/0.34  % CPUTime  : 
% 0.64/1.39  
% 0.64/1.39  /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.64/1.39  Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.64/1.39  %-----------------------------------------------------
% 0.64/1.39  ncf(matrix, plain, [(2652 ^ _375763) ^ [] : [cowlThing(2653 ^ []), -(cowlNothing(2653 ^ [])), 2665 ^ _375763 : [(2666 ^ _375763) ^ [] : [-(xsd_string(2662 ^ []))], (2668 ^ _375763) ^ [] : [-(xsd_integer(2662 ^ []))]], 2669 ^ _375763 : [(2670 ^ _375763) ^ [] : [xsd_integer(2662 ^ [])], (2672 ^ _375763) ^ [] : [xsd_string(2662 ^ [])]], cC130(iV16439), cC108(iV16439), cC104(iV16439), cC106(iV16439), cC28(iV16439), cowlThing(iV16439), cC98(iV16440), cC80(iV16440), cC82(iV16440), cowlThing(iV16440), cC38(iV16448), cowlThing(iV16448), cC76(iV16453), cC62(iV16453), cowlThing(iV16453), cC60(iV16453), cC56(iV16455), cC44(iV16455), cC42(iV16455), cowlThing(iV16455), cC38(iV16457), cowlThing(iV16457), cC50(iV16459), cC88(iV16459), cC34(iV16459), cC68(iV16459), cowlThing(iV16459), cC38(iV16460), cowlThing(iV16460), cC42(iV16461), cC56(iV16461), cC44(iV16461), cowlThing(iV16461), cC38(iV16462), cowlThing(iV16462), cC76(iV16463), cC62(iV16463), cowlThing(iV16463), cC60(iV16463), cC56(iV16464), cC42(iV16464), cC44(iV16464), cowlThing(iV16464), cC38(iV16465), cowlThing(iV16465)], (2 ^ _375763) ^ [_375867] : [-(cowlThing(_375867))], (4 ^ _375763) ^ [_375909] : [cowlNothing(_375909)], (6 ^ _375763) ^ [_376032] : [xsd_string(_376032), xsd_integer(_376032)], (12 ^ _375763) ^ [_376185] : [-(xsd_integer(_376185)), -(xsd_string(_376185))], (18 ^ _375763) ^ [_376405] : [cC10(_376405), 21 ^ _375763 : [(22 ^ _375763) ^ [] : [-(cC8(_376405))], (24 ^ _375763) ^ [] : [-(cC6(_376405))]]], (26 ^ _375763) ^ [_376628] : [-(cC10(_376628)), cC8(_376628), cC6(_376628)], (36 ^ _375763) ^ [_376928] : [cC10(_376928), 39 ^ _375763 : [(40 ^ _375763) ^ [_377039] : [ra_Px73(_376928, _377039)]]], (42 ^ _375763) ^ [_377105] : [-(ra_Px73(_377105, 43 ^ [_377105])), -(cC10(_377105))], (49 ^ _375763) ^ [_377378] : [cC10xcomp(_377378), -(ra_Px73(_377378, 52 ^ [_377378]))], (56 ^ _375763) ^ [_377583] : [57 ^ _375763 : [(58 ^ _375763) ^ [_377650] : [ra_Px73(_377583, _377650)]], -(cC10xcomp(_377583))], (62 ^ _375763) ^ [_377824] : [cC100(_377824), 66 ^ _375763 : [(67 ^ _375763) ^ [] : [-(rR1(_377824, 65 ^ [_377824]))], (69 ^ _375763) ^ [] : [-(cC98xcomp(65 ^ [_377824]))]]], (71 ^ _375763) ^ [_378110] : [-(cC100(_378110)), 72 ^ _375763 : [(73 ^ _375763) ^ [_378198] : [rR1(_378110, _378198), cC98xcomp(_378198)]]], (81 ^ _375763) ^ [_378472] : [cC100(_378472), 84 ^ _375763 : [(85 ^ _375763) ^ [_378583] : [ra_Px37(_378472, _378583)]]], (87 ^ _375763) ^ [_378649] : [-(ra_Px37(_378649, 88 ^ [_378649])), -(cC100(_378649))], (94 ^ _375763) ^ [_378922] : [cC100xcomp(_378922), -(ra_Px37(_378922, 97 ^ [_378922]))], (101 ^ _375763) ^ [_379127] : [102 ^ _375763 : [(103 ^ _375763) ^ [_379194] : [ra_Px37(_379127, _379194)]], -(cC100xcomp(_379127))], (107 ^ _375763) ^ [_379368] : [cC102(_379368), -(ra_Px36(_379368, 110 ^ [_379368]))], (114 ^ _375763) ^ [_379573] : [115 ^ _375763 : [(116 ^ _375763) ^ [_379640] : [ra_Px36(_379573, _379640)]], -(cC102(_379573))], (120 ^ _375763) ^ [_379814] : [cC102xcomp(_379814), 123 ^ _375763 : [(124 ^ _375763) ^ [_379925] : [ra_Px36(_379814, _379925)]]], (126 ^ _375763) ^ [_379991] : [-(ra_Px36(_379991, 127 ^ [_379991])), -(cC102xcomp(_379991))], (133 ^ _375763) ^ [_380264] : [cC104(_380264), 137 ^ _375763 : [(138 ^ _375763) ^ [] : [-(rR1(_380264, 136 ^ [_380264]))], (140 ^ _375763) ^ [] : [-(cC102xcomp(136 ^ [_380264]))]]], (142 ^ _375763) ^ [_380550] : [-(cC104(_380550)), 143 ^ _375763 : [(144 ^ _375763) ^ [_380638] : [rR1(_380550, _380638), cC102xcomp(_380638)]]], (152 ^ _375763) ^ [_380912] : [cC106(_380912), 155 ^ _375763 : [(156 ^ _375763) ^ [] : [-(cC104(_380912))], (158 ^ _375763) ^ [] : [-(cC100xcomp(_380912))]]], (160 ^ _375763) ^ [_381135] : [-(cC106(_381135)), cC104(_381135), cC100xcomp(_381135)], (170 ^ _375763) ^ [_381435] : [cC108(_381435), 173 ^ _375763 : [(174 ^ _375763) ^ [] : [-(cC28(_381435))], (176 ^ _375763) ^ [] : [-(cC106(_381435))]]], (178 ^ _375763) ^ [_381658] : [-(cC108(_381658)), cC28(_381658), cC106(_381658)], (188 ^ _375763) ^ [_381958] : [cC110(_381958), 191 ^ _375763 : [(192 ^ _375763) ^ [] : [-(cC4xcomp(_381958))], (194 ^ _375763) ^ [] : [-(cC12xcomp(_381958))]]], (196 ^ _375763) ^ [_382181] : [-(cC110(_382181)), cC4xcomp(_382181), cC12xcomp(_382181)], (206 ^ _375763) ^ [_382481] : [cC112(_382481), 209 ^ _375763 : [(210 ^ _375763) ^ [] : [-(cC110(_382481))], (212 ^ _375763) ^ [] : [-(cC102xcomp(_382481))]]], (214 ^ _375763) ^ [_382704] : [-(cC112(_382704)), cC110(_382704), cC102xcomp(_382704)], (224 ^ _375763) ^ [_383004] : [cC114(_383004), -(ra_Px41(_383004, 227 ^ [_383004]))], (231 ^ _375763) ^ [_383209] : [232 ^ _375763 : [(233 ^ _375763) ^ [_383276] : [ra_Px41(_383209, _383276)]], -(cC114(_383209))], (237 ^ _375763) ^ [_383450] : [cC114xcomp(_383450), 240 ^ _375763 : [(241 ^ _375763) ^ [_383561] : [ra_Px41(_383450, _383561)]]], (243 ^ _375763) ^ [_383627] : [-(ra_Px41(_383627, 244 ^ [_383627])), -(cC114xcomp(_383627))], (250 ^ _375763) ^ [_383900] : [cC116(_383900), 253 ^ _375763 : [(254 ^ _375763) ^ [] : [-(cC112(_383900))], (256 ^ _375763) ^ [] : [-(cC114xcomp(_383900))]]], (258 ^ _375763) ^ [_384123] : [-(cC116(_384123)), cC112(_384123), cC114xcomp(_384123)], (268 ^ _375763) ^ [_384423] : [cC118(_384423), -(ra_Px42(_384423, 271 ^ [_384423]))], (275 ^ _375763) ^ [_384628] : [276 ^ _375763 : [(277 ^ _375763) ^ [_384695] : [ra_Px42(_384628, _384695)]], -(cC118(_384628))], (281 ^ _375763) ^ [_384869] : [cC118xcomp(_384869), 284 ^ _375763 : [(285 ^ _375763) ^ [_384980] : [ra_Px42(_384869, _384980)]]], (287 ^ _375763) ^ [_385046] : [-(ra_Px42(_385046, 288 ^ [_385046])), -(cC118xcomp(_385046))], (294 ^ _375763) ^ [_385319] : [cC12(_385319), -(ra_Px18(_385319, 297 ^ [_385319]))], (301 ^ _375763) ^ [_385524] : [302 ^ _375763 : [(303 ^ _375763) ^ [_385591] : [ra_Px18(_385524, _385591)]], -(cC12(_385524))], (307 ^ _375763) ^ [_385765] : [cC12xcomp(_385765), 310 ^ _375763 : [(311 ^ _375763) ^ [_385876] : [ra_Px18(_385765, _385876)]]], (313 ^ _375763) ^ [_385942] : [-(ra_Px18(_385942, 314 ^ [_385942])), -(cC12xcomp(_385942))], (320 ^ _375763) ^ [_386215] : [cC120(_386215), 323 ^ _375763 : [(324 ^ _375763) ^ [] : [-(cC116(_386215))], (326 ^ _375763) ^ [] : [-(cC118xcomp(_386215))]]], (328 ^ _375763) ^ [_386438] : [-(cC120(_386438)), cC116(_386438), cC118xcomp(_386438)], (338 ^ _375763) ^ [_386738] : [cC120(_386738), 341 ^ _375763 : [(342 ^ _375763) ^ [_386849] : [ra_Px43(_386738, _386849)]]], (344 ^ _375763) ^ [_386915] : [-(ra_Px43(_386915, 345 ^ [_386915])), -(cC120(_386915))], (351 ^ _375763) ^ [_387188] : [cC120xcomp(_387188), -(ra_Px43(_387188, 354 ^ [_387188]))], (358 ^ _375763) ^ [_387393] : [359 ^ _375763 : [(360 ^ _375763) ^ [_387460] : [ra_Px43(_387393, _387460)]], -(cC120xcomp(_387393))], (364 ^ _375763) ^ [_387634] : [cC122(_387634), 368 ^ _375763 : [(369 ^ _375763) ^ [] : [-(rR1(_387634, 367 ^ [_387634]))], (371 ^ _375763) ^ [] : [-(cC120xcomp(367 ^ [_387634]))]]], (373 ^ _375763) ^ [_387920] : [-(cC122(_387920)), 374 ^ _375763 : [(375 ^ _375763) ^ [_388008] : [rR1(_387920, _388008), cC120xcomp(_388008)]]], (383 ^ _375763) ^ [_388282] : [cC124(_388282), 387 ^ _375763 : [(388 ^ _375763) ^ [] : [-(rR1(_388282, 386 ^ [_388282]))], (390 ^ _375763) ^ [] : [-(cC122(386 ^ [_388282]))]]], (392 ^ _375763) ^ [_388568] : [-(cC124(_388568)), 393 ^ _375763 : [(394 ^ _375763) ^ [_388656] : [rR1(_388568, _388656), cC122(_388656)]]], (402 ^ _375763) ^ [_388930] : [cC126(_388930), 406 ^ _375763 : [(407 ^ _375763) ^ [] : [-(rR1(_388930, 405 ^ [_388930]))], (409 ^ _375763) ^ [] : [-(cC124(405 ^ [_388930]))]]], (411 ^ _375763) ^ [_389216] : [-(cC126(_389216)), 412 ^ _375763 : [(413 ^ _375763) ^ [_389304] : [rR1(_389216, _389304), cC124(_389304)]]], (421 ^ _375763) ^ [_389578] : [cC128(_389578), 425 ^ _375763 : [(426 ^ _375763) ^ [] : [-(rR1(_389578, 424 ^ [_389578]))], (428 ^ _375763) ^ [] : [-(cC126(424 ^ [_389578]))]]], (430 ^ _375763) ^ [_389864] : [-(cC128(_389864)), 431 ^ _375763 : [(432 ^ _375763) ^ [_389952] : [rR1(_389864, _389952), cC126(_389952)]]], (440 ^ _375763) ^ [_390226] : [cC130(_390226), 444 ^ _375763 : [(445 ^ _375763) ^ [] : [-(rR1(_390226, 443 ^ [_390226]))], (447 ^ _375763) ^ [] : [-(cC128(443 ^ [_390226]))]]], (449 ^ _375763) ^ [_390512] : [-(cC130(_390512)), 450 ^ _375763 : [(451 ^ _375763) ^ [_390600] : [rR1(_390512, _390600), cC128(_390600)]]], (459 ^ _375763) ^ [_390874] : [cC14(_390874), -(ra_Px74(_390874, 462 ^ [_390874]))], (466 ^ _375763) ^ [_391079] : [467 ^ _375763 : [(468 ^ _375763) ^ [_391146] : [ra_Px74(_391079, _391146)]], -(cC14(_391079))], (472 ^ _375763) ^ [_391320] : [cC14(_391320), 475 ^ _375763 : [(476 ^ _375763) ^ [] : [-(cC10(_391320))], (478 ^ _375763) ^ [] : [-(cC12(_391320))]]], (480 ^ _375763) ^ [_391543] : [-(cC14(_391543)), cC10(_391543), cC12(_391543)], (490 ^ _375763) ^ [_391843] : [cC14xcomp(_391843), 493 ^ _375763 : [(494 ^ _375763) ^ [_391954] : [ra_Px74(_391843, _391954)]]], (496 ^ _375763) ^ [_392020] : [-(ra_Px74(_392020, 497 ^ [_392020])), -(cC14xcomp(_392020))], (503 ^ _375763) ^ [_392293] : [cC16(_392293), -(ra_Px27(_392293, 506 ^ [_392293]))], (510 ^ _375763) ^ [_392498] : [511 ^ _375763 : [(512 ^ _375763) ^ [_392565] : [ra_Px27(_392498, _392565)]], -(cC16(_392498))], (516 ^ _375763) ^ [_392739] : [cC16xcomp(_392739), 519 ^ _375763 : [(520 ^ _375763) ^ [_392850] : [ra_Px27(_392739, _392850)]]], (522 ^ _375763) ^ [_392916] : [-(ra_Px27(_392916, 523 ^ [_392916])), -(cC16xcomp(_392916))], (529 ^ _375763) ^ [_393189] : [cC18(_393189), 532 ^ _375763 : [(533 ^ _375763) ^ [_393300] : [ra_Px1(_393189, _393300)]]], (535 ^ _375763) ^ [_393366] : [-(ra_Px1(_393366, 536 ^ [_393366])), -(cC18(_393366))], (542 ^ _375763) ^ [_393639] : [cC18(_393639), 545 ^ _375763 : [(546 ^ _375763) ^ [] : [-(cC14(_393639))], (548 ^ _375763) ^ [] : [-(cC16(_393639))]]], (550 ^ _375763) ^ [_393862] : [-(cC18(_393862)), cC14(_393862), cC16(_393862)], (560 ^ _375763) ^ [_394162] : [cC18xcomp(_394162), -(ra_Px1(_394162, 563 ^ [_394162]))], (567 ^ _375763) ^ [_394367] : [568 ^ _375763 : [(569 ^ _375763) ^ [_394434] : [ra_Px1(_394367, _394434)]], -(cC18xcomp(_394367))], (573 ^ _375763) ^ [_394608] : [cC2(_394608), -(ra_Px2(_394608, 576 ^ [_394608]))], (580 ^ _375763) ^ [_394813] : [581 ^ _375763 : [(582 ^ _375763) ^ [_394880] : [ra_Px2(_394813, _394880)]], -(cC2(_394813))], (586 ^ _375763) ^ [_395054] : [cC2xcomp(_395054), 589 ^ _375763 : [(590 ^ _375763) ^ [_395165] : [ra_Px2(_395054, _395165)]]], (592 ^ _375763) ^ [_395231] : [-(ra_Px2(_395231, 593 ^ [_395231])), -(cC2xcomp(_395231))], (599 ^ _375763) ^ [_395504] : [cC20(_395504), 603 ^ _375763 : [(604 ^ _375763) ^ [] : [-(rR1(_395504, 602 ^ [_395504]))], (606 ^ _375763) ^ [] : [-(cC18xcomp(602 ^ [_395504]))]]], (608 ^ _375763) ^ [_395790] : [-(cC20(_395790)), 609 ^ _375763 : [(610 ^ _375763) ^ [_395878] : [rR1(_395790, _395878), cC18xcomp(_395878)]]], (618 ^ _375763) ^ [_396152] : [cC22(_396152), 622 ^ _375763 : [(623 ^ _375763) ^ [] : [-(rR1(_396152, 621 ^ [_396152]))], (625 ^ _375763) ^ [] : [-(cC20(621 ^ [_396152]))]]], (627 ^ _375763) ^ [_396438] : [-(cC22(_396438)), 628 ^ _375763 : [(629 ^ _375763) ^ [_396526] : [rR1(_396438, _396526), cC20(_396526)]]], (637 ^ _375763) ^ [_396800] : [cC24(_396800), 641 ^ _375763 : [(642 ^ _375763) ^ [] : [-(rR1(_396800, 640 ^ [_396800]))], (644 ^ _375763) ^ [] : [-(cC22(640 ^ [_396800]))]]], (646 ^ _375763) ^ [_397086] : [-(cC24(_397086)), 647 ^ _375763 : [(648 ^ _375763) ^ [_397174] : [rR1(_397086, _397174), cC22(_397174)]]], (656 ^ _375763) ^ [_397448] : [cC26(_397448), 660 ^ _375763 : [(661 ^ _375763) ^ [] : [-(rR1(_397448, 659 ^ [_397448]))], (663 ^ _375763) ^ [] : [-(cC24(659 ^ [_397448]))]]], (665 ^ _375763) ^ [_397734] : [-(cC26(_397734)), 666 ^ _375763 : [(667 ^ _375763) ^ [_397822] : [rR1(_397734, _397822), cC24(_397822)]]], (675 ^ _375763) ^ [_398096] : [cC28(_398096), 679 ^ _375763 : [(680 ^ _375763) ^ [] : [-(rR1(_398096, 678 ^ [_398096]))], (682 ^ _375763) ^ [] : [-(cC26(678 ^ [_398096]))]]], (684 ^ _375763) ^ [_398382] : [-(cC28(_398382)), 685 ^ _375763 : [(686 ^ _375763) ^ [_398470] : [rR1(_398382, _398470), cC26(_398470)]]], (694 ^ _375763) ^ [_398744] : [cC30(_398744), 697 ^ _375763 : [(698 ^ _375763) ^ [_398855] : [ra_Px4(_398744, _398855)]]], (700 ^ _375763) ^ [_398921] : [-(ra_Px4(_398921, 701 ^ [_398921])), -(cC30(_398921))], (707 ^ _375763) ^ [_399194] : [cC30(_399194), 710 ^ _375763 : [(711 ^ _375763) ^ [] : [-(cC2(_399194))], (713 ^ _375763) ^ [] : [-(cC4(_399194))]]], (715 ^ _375763) ^ [_399417] : [-(cC30(_399417)), cC2(_399417), cC4(_399417)], (725 ^ _375763) ^ [_399717] : [cC30xcomp(_399717), -(ra_Px4(_399717, 728 ^ [_399717]))], (732 ^ _375763) ^ [_399922] : [733 ^ _375763 : [(734 ^ _375763) ^ [_399989] : [ra_Px4(_399922, _399989)]], -(cC30xcomp(_399922))], (738 ^ _375763) ^ [_400163] : [cC32(_400163), -(ra_Px5(_400163, 741 ^ [_400163]))], (745 ^ _375763) ^ [_400368] : [746 ^ _375763 : [(747 ^ _375763) ^ [_400435] : [ra_Px5(_400368, _400435)]], -(cC32(_400368))], (751 ^ _375763) ^ [_400609] : [cC32(_400609), 754 ^ _375763 : [(755 ^ _375763) ^ [] : [-(cC4xcomp(_400609))], (757 ^ _375763) ^ [] : [-(cC2xcomp(_400609))]]], (759 ^ _375763) ^ [_400832] : [-(cC32(_400832)), cC4xcomp(_400832), cC2xcomp(_400832)], (769 ^ _375763) ^ [_401132] : [cC32xcomp(_401132), 772 ^ _375763 : [(773 ^ _375763) ^ [_401243] : [ra_Px5(_401132, _401243)]]], (775 ^ _375763) ^ [_401309] : [-(ra_Px5(_401309, 776 ^ [_401309])), -(cC32xcomp(_401309))], (782 ^ _375763) ^ [_401582] : [cC34(_401582), -(ra_Px6(_401582, 785 ^ [_401582]))], (789 ^ _375763) ^ [_401787] : [790 ^ _375763 : [(791 ^ _375763) ^ [_401854] : [ra_Px6(_401787, _401854)]], -(cC34(_401787))], (795 ^ _375763) ^ [_402028] : [cC34(_402028), 798 ^ _375763 : [(799 ^ _375763) ^ [] : [-(cC30xcomp(_402028))], (801 ^ _375763) ^ [] : [-(cC32xcomp(_402028))]]], (803 ^ _375763) ^ [_402251] : [-(cC34(_402251)), cC30xcomp(_402251), cC32xcomp(_402251)], (813 ^ _375763) ^ [_402551] : [cC34xcomp(_402551), 816 ^ _375763 : [(817 ^ _375763) ^ [_402662] : [ra_Px6(_402551, _402662)]]], (819 ^ _375763) ^ [_402728] : [-(ra_Px6(_402728, 820 ^ [_402728])), -(cC34xcomp(_402728))], (826 ^ _375763) ^ [_403001] : [cC36(_403001), 829 ^ _375763 : [(830 ^ _375763) ^ [_403112] : [ra_Px7(_403001, _403112)]]], (832 ^ _375763) ^ [_403178] : [-(ra_Px7(_403178, 833 ^ [_403178])), -(cC36(_403178))], (839 ^ _375763) ^ [_403451] : [cC36(_403451), 843 ^ _375763 : [(844 ^ _375763) ^ [] : [-(rR1(_403451, 842 ^ [_403451]))], (846 ^ _375763) ^ [] : [-(cC34xcomp(842 ^ [_403451]))]]], (848 ^ _375763) ^ [_403737] : [-(cC36(_403737)), 849 ^ _375763 : [(850 ^ _375763) ^ [_403825] : [rR1(_403737, _403825), cC34xcomp(_403825)]]], (858 ^ _375763) ^ [_404099] : [cC36xcomp(_404099), -(ra_Px7(_404099, 861 ^ [_404099]))], (865 ^ _375763) ^ [_404304] : [866 ^ _375763 : [(867 ^ _375763) ^ [_404371] : [ra_Px7(_404304, _404371)]], -(cC36xcomp(_404304))], (871 ^ _375763) ^ [_404545] : [cC38(_404545), 874 ^ _375763 : [(875 ^ _375763) ^ [] : [-(cTOP(_404545))], (877 ^ _375763) ^ [] : [-(cC36xcomp(_404545))]]], (879 ^ _375763) ^ [_404768] : [-(cC38(_404768)), cTOP(_404768), cC36xcomp(_404768)], (889 ^ _375763) ^ [_405068] : [cC38(_405068), -(ra_Px8(_405068, 892 ^ [_405068]))], (896 ^ _375763) ^ [_405273] : [897 ^ _375763 : [(898 ^ _375763) ^ [_405340] : [ra_Px8(_405273, _405340)]], -(cC38(_405273))], (902 ^ _375763) ^ [_405514] : [cC38xcomp(_405514), 905 ^ _375763 : [(906 ^ _375763) ^ [_405625] : [ra_Px8(_405514, _405625)]]], (908 ^ _375763) ^ [_405691] : [-(ra_Px8(_405691, 909 ^ [_405691])), -(cC38xcomp(_405691))], (915 ^ _375763) ^ [_405964] : [cC4(_405964), -(ra_Px3(_405964, 918 ^ [_405964]))], (922 ^ _375763) ^ [_406169] : [923 ^ _375763 : [(924 ^ _375763) ^ [_406236] : [ra_Px3(_406169, _406236)]], -(cC4(_406169))], (928 ^ _375763) ^ [_406410] : [cC4xcomp(_406410), 931 ^ _375763 : [(932 ^ _375763) ^ [_406521] : [ra_Px3(_406410, _406521)]]], (934 ^ _375763) ^ [_406587] : [-(ra_Px3(_406587, 935 ^ [_406587])), -(cC4xcomp(_406587))], (941 ^ _375763) ^ [_406860] : [cC40(_406860), 944 ^ _375763 : [(945 ^ _375763) ^ [_406971] : [ra_Px10(_406860, _406971)]]], (947 ^ _375763) ^ [_407037] : [-(ra_Px10(_407037, 948 ^ [_407037])), -(cC40(_407037))], (954 ^ _375763) ^ [_407310] : [cC40(_407310), 958 ^ _375763 : [(959 ^ _375763) ^ [] : [-(rR1(_407310, 957 ^ [_407310]))], (961 ^ _375763) ^ [] : [-(cC38xcomp(957 ^ [_407310]))]]], (963 ^ _375763) ^ [_407596] : [-(cC40(_407596)), 964 ^ _375763 : [(965 ^ _375763) ^ [_407684] : [rR1(_407596, _407684), cC38xcomp(_407684)]]], (973 ^ _375763) ^ [_407958] : [cC40xcomp(_407958), -(ra_Px10(_407958, 976 ^ [_407958]))], (980 ^ _375763) ^ [_408163] : [981 ^ _375763 : [(982 ^ _375763) ^ [_408230] : [ra_Px10(_408163, _408230)]], -(cC40xcomp(_408163))], (986 ^ _375763) ^ [_408404] : [cC42(_408404), 990 ^ _375763 : [(991 ^ _375763) ^ [] : [-(rR1(_408404, 989 ^ [_408404]))], (993 ^ _375763) ^ [] : [-(cC8xcomp(989 ^ [_408404]))]]], (995 ^ _375763) ^ [_408690] : [-(cC42(_408690)), 996 ^ _375763 : [(997 ^ _375763) ^ [_408778] : [rR1(_408690, _408778), cC8xcomp(_408778)]]], (1005 ^ _375763) ^ [_409052] : [cC44(_409052), 1008 ^ _375763 : [(1009 ^ _375763) ^ [] : [-(cC40xcomp(_409052))], (1011 ^ _375763) ^ [] : [-(cC42(_409052))]]], (1013 ^ _375763) ^ [_409275] : [-(cC44(_409275)), cC40xcomp(_409275), cC42(_409275)], (1023 ^ _375763) ^ [_409575] : [cC46(_409575), 1026 ^ _375763 : [(1027 ^ _375763) ^ [_409686] : [ra_Px13(_409575, _409686)]]], (1029 ^ _375763) ^ [_409752] : [-(ra_Px13(_409752, 1030 ^ [_409752])), -(cC46(_409752))], (1036 ^ _375763) ^ [_410025] : [cC46(_410025), 1039 ^ _375763 : [(1040 ^ _375763) ^ [] : [-(cC8(_410025))], (1042 ^ _375763) ^ [] : [-(cC4(_410025))]]], (1044 ^ _375763) ^ [_410248] : [-(cC46(_410248)), cC8(_410248), cC4(_410248)], (1054 ^ _375763) ^ [_410548] : [cC46xcomp(_410548), -(ra_Px13(_410548, 1057 ^ [_410548]))], (1061 ^ _375763) ^ [_410753] : [1062 ^ _375763 : [(1063 ^ _375763) ^ [_410820] : [ra_Px13(_410753, _410820)]], -(cC46xcomp(_410753))], (1067 ^ _375763) ^ [_410994] : [cC48(_410994), 1070 ^ _375763 : [(1071 ^ _375763) ^ [] : [-(cC4xcomp(_410994))], (1073 ^ _375763) ^ [] : [-(cC8xcomp(_410994))]]], (1075 ^ _375763) ^ [_411217] : [-(cC48(_411217)), cC4xcomp(_411217), cC8xcomp(_411217)], (1085 ^ _375763) ^ [_411517] : [cC48(_411517), -(ra_Px14(_411517, 1088 ^ [_411517]))], (1092 ^ _375763) ^ [_411722] : [1093 ^ _375763 : [(1094 ^ _375763) ^ [_411789] : [ra_Px14(_411722, _411789)]], -(cC48(_411722))], (1098 ^ _375763) ^ [_411963] : [cC48xcomp(_411963), 1101 ^ _375763 : [(1102 ^ _375763) ^ [_412074] : [ra_Px14(_411963, _412074)]]], (1104 ^ _375763) ^ [_412140] : [-(ra_Px14(_412140, 1105 ^ [_412140])), -(cC48xcomp(_412140))], (1111 ^ _375763) ^ [_412413] : [cC50(_412413), 1114 ^ _375763 : [(1115 ^ _375763) ^ [] : [-(cC46xcomp(_412413))], (1117 ^ _375763) ^ [] : [-(cC48xcomp(_412413))]]], (1119 ^ _375763) ^ [_412636] : [-(cC50(_412636)), cC46xcomp(_412636), cC48xcomp(_412636)], (1129 ^ _375763) ^ [_412936] : [cC50(_412936), -(ra_Px15(_412936, 1132 ^ [_412936]))], (1136 ^ _375763) ^ [_413141] : [1137 ^ _375763 : [(1138 ^ _375763) ^ [_413208] : [ra_Px15(_413141, _413208)]], -(cC50(_413141))], (1142 ^ _375763) ^ [_413382] : [cC50xcomp(_413382), 1145 ^ _375763 : [(1146 ^ _375763) ^ [_413493] : [ra_Px15(_413382, _413493)]]], (1148 ^ _375763) ^ [_413559] : [-(ra_Px15(_413559, 1149 ^ [_413559])), -(cC50xcomp(_413559))], (1155 ^ _375763) ^ [_413832] : [cC52(_413832), 1158 ^ _375763 : [(1159 ^ _375763) ^ [_413943] : [ra_Px49(_413832, _413943)]]], (1161 ^ _375763) ^ [_414009] : [-(ra_Px49(_414009, 1162 ^ [_414009])), -(cC52(_414009))], (1168 ^ _375763) ^ [_414282] : [cC52(_414282), 1172 ^ _375763 : [(1173 ^ _375763) ^ [] : [-(rR1(_414282, 1171 ^ [_414282]))], (1175 ^ _375763) ^ [] : [-(cC50xcomp(1171 ^ [_414282]))]]], (1177 ^ _375763) ^ [_414568] : [-(cC52(_414568)), 1178 ^ _375763 : [(1179 ^ _375763) ^ [_414656] : [rR1(_414568, _414656), cC50xcomp(_414656)]]], (1187 ^ _375763) ^ [_414930] : [cC52xcomp(_414930), -(ra_Px49(_414930, 1190 ^ [_414930]))], (1194 ^ _375763) ^ [_415135] : [1195 ^ _375763 : [(1196 ^ _375763) ^ [_415202] : [ra_Px49(_415135, _415202)]], -(cC52xcomp(_415135))], (1200 ^ _375763) ^ [_415376] : [cC54(_415376), 1203 ^ _375763 : [(1204 ^ _375763) ^ [_415487] : [ra_Px16(_415376, _415487)]]], (1206 ^ _375763) ^ [_415553] : [-(ra_Px16(_415553, 1207 ^ [_415553])), -(cC54(_415553))], (1213 ^ _375763) ^ [_415826] : [cC54(_415826), 1217 ^ _375763 : [(1218 ^ _375763) ^ [] : [-(rR1(_415826, 1216 ^ [_415826]))], (1220 ^ _375763) ^ [] : [-(cC52(1216 ^ [_415826]))]]], (1222 ^ _375763) ^ [_416112] : [-(cC54(_416112)), 1223 ^ _375763 : [(1224 ^ _375763) ^ [_416200] : [rR1(_416112, _416200), cC52(_416200)]]], (1232 ^ _375763) ^ [_416474] : [cC54xcomp(_416474), -(ra_Px16(_416474, 1235 ^ [_416474]))], (1239 ^ _375763) ^ [_416679] : [1240 ^ _375763 : [(1241 ^ _375763) ^ [_416746] : [ra_Px16(_416679, _416746)]], -(cC54xcomp(_416679))], (1245 ^ _375763) ^ [_416920] : [cC56(_416920), 1248 ^ _375763 : [(1249 ^ _375763) ^ [] : [-(cC54xcomp(_416920))], (1251 ^ _375763) ^ [] : [-(cC44(_416920))]]], (1253 ^ _375763) ^ [_417143] : [-(cC56(_417143)), cC54xcomp(_417143), cC44(_417143)], (1263 ^ _375763) ^ [_417443] : [cC56(_417443), -(ra_Px17(_417443, 1266 ^ [_417443]))], (1270 ^ _375763) ^ [_417648] : [1271 ^ _375763 : [(1272 ^ _375763) ^ [_417715] : [ra_Px17(_417648, _417715)]], -(cC56(_417648))], (1276 ^ _375763) ^ [_417889] : [cC56xcomp(_417889), 1279 ^ _375763 : [(1280 ^ _375763) ^ [_418000] : [ra_Px17(_417889, _418000)]]], (1282 ^ _375763) ^ [_418066] : [-(ra_Px17(_418066, 1283 ^ [_418066])), -(cC56xcomp(_418066))], (1289 ^ _375763) ^ [_418339] : [cC58(_418339), 1293 ^ _375763 : [(1294 ^ _375763) ^ [] : [-(rR1(_418339, 1292 ^ [_418339]))], (1296 ^ _375763) ^ [] : [-(cC56xcomp(1292 ^ [_418339]))]]], (1298 ^ _375763) ^ [_418625] : [-(cC58(_418625)), 1299 ^ _375763 : [(1300 ^ _375763) ^ [_418713] : [rR1(_418625, _418713), cC56xcomp(_418713)]]], (1308 ^ _375763) ^ [_418987] : [cC58(_418987), 1311 ^ _375763 : [(1312 ^ _375763) ^ [_419098] : [ra_Px19(_418987, _419098)]]], (1314 ^ _375763) ^ [_419164] : [-(ra_Px19(_419164, 1315 ^ [_419164])), -(cC58(_419164))], (1321 ^ _375763) ^ [_419437] : [cC58xcomp(_419437), -(ra_Px19(_419437, 1324 ^ [_419437]))], (1328 ^ _375763) ^ [_419642] : [1329 ^ _375763 : [(1330 ^ _375763) ^ [_419709] : [ra_Px19(_419642, _419709)]], -(cC58xcomp(_419642))], (1334 ^ _375763) ^ [_419883] : [cC6(_419883), 1337 ^ _375763 : [(1338 ^ _375763) ^ [] : [-(cC2(_419883))], (1340 ^ _375763) ^ [] : [-(cC4(_419883))]]], (1342 ^ _375763) ^ [_420106] : [-(cC6(_420106)), cC2(_420106), cC4(_420106)], (1352 ^ _375763) ^ [_420406] : [cC6(_420406), -(ra_Px72(_420406, 1355 ^ [_420406]))], (1359 ^ _375763) ^ [_420611] : [1360 ^ _375763 : [(1361 ^ _375763) ^ [_420678] : [ra_Px72(_420611, _420678)]], -(cC6(_420611))], (1365 ^ _375763) ^ [_420852] : [cC6xcomp(_420852), 1368 ^ _375763 : [(1369 ^ _375763) ^ [_420963] : [ra_Px72(_420852, _420963)]]], (1371 ^ _375763) ^ [_421029] : [-(ra_Px72(_421029, 1372 ^ [_421029])), -(cC6xcomp(_421029))], (1378 ^ _375763) ^ [_421302] : [cC60(_421302), 1382 ^ _375763 : [(1383 ^ _375763) ^ [] : [-(rR1(_421302, 1381 ^ [_421302]))], (1385 ^ _375763) ^ [] : [-(cC12xcomp(1381 ^ [_421302]))]]], (1387 ^ _375763) ^ [_421588] : [-(cC60(_421588)), 1388 ^ _375763 : [(1389 ^ _375763) ^ [_421676] : [rR1(_421588, _421676), cC12xcomp(_421676)]]], (1397 ^ _375763) ^ [_421950] : [cC62(_421950), 1400 ^ _375763 : [(1401 ^ _375763) ^ [] : [-(cC60(_421950))], (1403 ^ _375763) ^ [] : [-(cC58xcomp(_421950))]]], (1405 ^ _375763) ^ [_422173] : [-(cC62(_422173)), cC60(_422173), cC58xcomp(_422173)], (1415 ^ _375763) ^ [_422473] : [cC64(_422473), 1418 ^ _375763 : [(1419 ^ _375763) ^ [] : [-(cC8(_422473))], (1421 ^ _375763) ^ [] : [-(cC12(_422473))]]], (1423 ^ _375763) ^ [_422696] : [-(cC64(_422696)), cC8(_422696), cC12(_422696)], (1433 ^ _375763) ^ [_422996] : [cC64(_422996), 1436 ^ _375763 : [(1437 ^ _375763) ^ [_423107] : [ra_Px22(_422996, _423107)]]], (1439 ^ _375763) ^ [_423173] : [-(ra_Px22(_423173, 1440 ^ [_423173])), -(cC64(_423173))], (1446 ^ _375763) ^ [_423446] : [cC64xcomp(_423446), -(ra_Px22(_423446, 1449 ^ [_423446]))], (1453 ^ _375763) ^ [_423651] : [1454 ^ _375763 : [(1455 ^ _375763) ^ [_423718] : [ra_Px22(_423651, _423718)]], -(cC64xcomp(_423651))], (1459 ^ _375763) ^ [_423892] : [cC66(_423892), 1462 ^ _375763 : [(1463 ^ _375763) ^ [] : [-(cC12xcomp(_423892))], (1465 ^ _375763) ^ [] : [-(cC8xcomp(_423892))]]], (1467 ^ _375763) ^ [_424115] : [-(cC66(_424115)), cC12xcomp(_424115), cC8xcomp(_424115)], (1477 ^ _375763) ^ [_424415] : [cC66(_424415), -(ra_Px23(_424415, 1480 ^ [_424415]))], (1484 ^ _375763) ^ [_424620] : [1485 ^ _375763 : [(1486 ^ _375763) ^ [_424687] : [ra_Px23(_424620, _424687)]], -(cC66(_424620))], (1490 ^ _375763) ^ [_424861] : [cC66xcomp(_424861), 1493 ^ _375763 : [(1494 ^ _375763) ^ [_424972] : [ra_Px23(_424861, _424972)]]], (1496 ^ _375763) ^ [_425038] : [-(ra_Px23(_425038, 1497 ^ [_425038])), -(cC66xcomp(_425038))], (1503 ^ _375763) ^ [_425311] : [cC68(_425311), -(ra_Px24(_425311, 1506 ^ [_425311]))], (1510 ^ _375763) ^ [_425516] : [1511 ^ _375763 : [(1512 ^ _375763) ^ [_425583] : [ra_Px24(_425516, _425583)]], -(cC68(_425516))], (1516 ^ _375763) ^ [_425757] : [cC68(_425757), 1519 ^ _375763 : [(1520 ^ _375763) ^ [] : [-(cC64xcomp(_425757))], (1522 ^ _375763) ^ [] : [-(cC66xcomp(_425757))]]], (1524 ^ _375763) ^ [_425980] : [-(cC68(_425980)), cC64xcomp(_425980), cC66xcomp(_425980)], (1534 ^ _375763) ^ [_426280] : [cC68xcomp(_426280), 1537 ^ _375763 : [(1538 ^ _375763) ^ [_426391] : [ra_Px24(_426280, _426391)]]], (1540 ^ _375763) ^ [_426457] : [-(ra_Px24(_426457, 1541 ^ [_426457])), -(cC68xcomp(_426457))], (1547 ^ _375763) ^ [_426730] : [cC70(_426730), 1551 ^ _375763 : [(1552 ^ _375763) ^ [] : [-(rR1(_426730, 1550 ^ [_426730]))], (1554 ^ _375763) ^ [] : [-(cC68xcomp(1550 ^ [_426730]))]]], (1556 ^ _375763) ^ [_427016] : [-(cC70(_427016)), 1557 ^ _375763 : [(1558 ^ _375763) ^ [_427104] : [rR1(_427016, _427104), cC68xcomp(_427104)]]], (1566 ^ _375763) ^ [_427378] : [cC70(_427378), -(ra_Px51(_427378, 1569 ^ [_427378]))], (1573 ^ _375763) ^ [_427583] : [1574 ^ _375763 : [(1575 ^ _375763) ^ [_427650] : [ra_Px51(_427583, _427650)]], -(cC70(_427583))], (1579 ^ _375763) ^ [_427824] : [cC70xcomp(_427824), 1582 ^ _375763 : [(1583 ^ _375763) ^ [_427935] : [ra_Px51(_427824, _427935)]]], (1585 ^ _375763) ^ [_428001] : [-(ra_Px51(_428001, 1586 ^ [_428001])), -(cC70xcomp(_428001))], (1592 ^ _375763) ^ [_428274] : [cC72(_428274), 1596 ^ _375763 : [(1597 ^ _375763) ^ [] : [-(rR1(_428274, 1595 ^ [_428274]))], (1599 ^ _375763) ^ [] : [-(cC70(1595 ^ [_428274]))]]], (1601 ^ _375763) ^ [_428560] : [-(cC72(_428560)), 1602 ^ _375763 : [(1603 ^ _375763) ^ [_428648] : [rR1(_428560, _428648), cC70(_428648)]]], (1611 ^ _375763) ^ [_428922] : [cC72(_428922), 1614 ^ _375763 : [(1615 ^ _375763) ^ [_429033] : [ra_Px58(_428922, _429033)]]], (1617 ^ _375763) ^ [_429099] : [-(ra_Px58(_429099, 1618 ^ [_429099])), -(cC72(_429099))], (1624 ^ _375763) ^ [_429372] : [cC72xcomp(_429372), -(ra_Px58(_429372, 1627 ^ [_429372]))], (1631 ^ _375763) ^ [_429577] : [1632 ^ _375763 : [(1633 ^ _375763) ^ [_429644] : [ra_Px58(_429577, _429644)]], -(cC72xcomp(_429577))], (1637 ^ _375763) ^ [_429818] : [cC74(_429818), 1641 ^ _375763 : [(1642 ^ _375763) ^ [] : [-(rR1(_429818, 1640 ^ [_429818]))], (1644 ^ _375763) ^ [] : [-(cC72(1640 ^ [_429818]))]]], (1646 ^ _375763) ^ [_430104] : [-(cC74(_430104)), 1647 ^ _375763 : [(1648 ^ _375763) ^ [_430192] : [rR1(_430104, _430192), cC72(_430192)]]], (1656 ^ _375763) ^ [_430466] : [cC74(_430466), 1659 ^ _375763 : [(1660 ^ _375763) ^ [_430577] : [ra_Px25(_430466, _430577)]]], (1662 ^ _375763) ^ [_430643] : [-(ra_Px25(_430643, 1663 ^ [_430643])), -(cC74(_430643))], (1669 ^ _375763) ^ [_430916] : [cC74xcomp(_430916), -(ra_Px25(_430916, 1672 ^ [_430916]))], (1676 ^ _375763) ^ [_431121] : [1677 ^ _375763 : [(1678 ^ _375763) ^ [_431188] : [ra_Px25(_431121, _431188)]], -(cC74xcomp(_431121))], (1682 ^ _375763) ^ [_431362] : [cC76(_431362), -(ra_Px26(_431362, 1685 ^ [_431362]))], (1689 ^ _375763) ^ [_431567] : [1690 ^ _375763 : [(1691 ^ _375763) ^ [_431634] : [ra_Px26(_431567, _431634)]], -(cC76(_431567))], (1695 ^ _375763) ^ [_431808] : [cC76(_431808), 1698 ^ _375763 : [(1699 ^ _375763) ^ [] : [-(cC74xcomp(_431808))], (1701 ^ _375763) ^ [] : [-(cC62(_431808))]]], (1703 ^ _375763) ^ [_432031] : [-(cC76(_432031)), cC74xcomp(_432031), cC62(_432031)], (1713 ^ _375763) ^ [_432331] : [cC76xcomp(_432331), 1716 ^ _375763 : [(1717 ^ _375763) ^ [_432442] : [ra_Px26(_432331, _432442)]]], (1719 ^ _375763) ^ [_432508] : [-(ra_Px26(_432508, 1720 ^ [_432508])), -(cC76xcomp(_432508))], (1726 ^ _375763) ^ [_432781] : [cC78(_432781), 1730 ^ _375763 : [(1731 ^ _375763) ^ [] : [-(rR1(_432781, 1729 ^ [_432781]))], (1733 ^ _375763) ^ [] : [-(cC76xcomp(1729 ^ [_432781]))]]], (1735 ^ _375763) ^ [_433067] : [-(cC78(_433067)), 1736 ^ _375763 : [(1737 ^ _375763) ^ [_433155] : [rR1(_433067, _433155), cC76xcomp(_433155)]]], (1745 ^ _375763) ^ [_433429] : [cC78(_433429), 1748 ^ _375763 : [(1749 ^ _375763) ^ [_433540] : [ra_Px28(_433429, _433540)]]], (1751 ^ _375763) ^ [_433606] : [-(ra_Px28(_433606, 1752 ^ [_433606])), -(cC78(_433606))], (1758 ^ _375763) ^ [_433879] : [cC78xcomp(_433879), -(ra_Px28(_433879, 1761 ^ [_433879]))], (1765 ^ _375763) ^ [_434084] : [1766 ^ _375763 : [(1767 ^ _375763) ^ [_434151] : [ra_Px28(_434084, _434151)]], -(cC78xcomp(_434084))], (1771 ^ _375763) ^ [_434325] : [cC8(_434325), -(ra_Px9(_434325, 1774 ^ [_434325]))], (1778 ^ _375763) ^ [_434530] : [1779 ^ _375763 : [(1780 ^ _375763) ^ [_434597] : [ra_Px9(_434530, _434597)]], -(cC8(_434530))], (1784 ^ _375763) ^ [_434771] : [cC8xcomp(_434771), 1787 ^ _375763 : [(1788 ^ _375763) ^ [_434882] : [ra_Px9(_434771, _434882)]]], (1790 ^ _375763) ^ [_434948] : [-(ra_Px9(_434948, 1791 ^ [_434948])), -(cC8xcomp(_434948))], (1797 ^ _375763) ^ [_435221] : [cC80(_435221), 1801 ^ _375763 : [(1802 ^ _375763) ^ [] : [-(rR1(_435221, 1800 ^ [_435221]))], (1804 ^ _375763) ^ [] : [-(cC16xcomp(1800 ^ [_435221]))]]], (1806 ^ _375763) ^ [_435507] : [-(cC80(_435507)), 1807 ^ _375763 : [(1808 ^ _375763) ^ [_435595] : [rR1(_435507, _435595), cC16xcomp(_435595)]]], (1816 ^ _375763) ^ [_435869] : [cC82(_435869), 1819 ^ _375763 : [(1820 ^ _375763) ^ [] : [-(cC80(_435869))], (1822 ^ _375763) ^ [] : [-(cC78xcomp(_435869))]]], (1824 ^ _375763) ^ [_436092] : [-(cC82(_436092)), cC80(_436092), cC78xcomp(_436092)], (1834 ^ _375763) ^ [_436392] : [cC84(_436392), 1837 ^ _375763 : [(1838 ^ _375763) ^ [_436503] : [ra_Px31(_436392, _436503)]]], (1840 ^ _375763) ^ [_436569] : [-(ra_Px31(_436569, 1841 ^ [_436569])), -(cC84(_436569))], (1847 ^ _375763) ^ [_436842] : [cC84(_436842), 1850 ^ _375763 : [(1851 ^ _375763) ^ [] : [-(cC2(_436842))], (1853 ^ _375763) ^ [] : [-(cC12(_436842))]]], (1855 ^ _375763) ^ [_437065] : [-(cC84(_437065)), cC2(_437065), cC12(_437065)], (1865 ^ _375763) ^ [_437365] : [cC84xcomp(_437365), -(ra_Px31(_437365, 1868 ^ [_437365]))], (1872 ^ _375763) ^ [_437570] : [1873 ^ _375763 : [(1874 ^ _375763) ^ [_437637] : [ra_Px31(_437570, _437637)]], -(cC84xcomp(_437570))], (1878 ^ _375763) ^ [_437811] : [cC86(_437811), 1881 ^ _375763 : [(1882 ^ _375763) ^ [] : [-(cC12xcomp(_437811))], (1884 ^ _375763) ^ [] : [-(cC2xcomp(_437811))]]], (1886 ^ _375763) ^ [_438034] : [-(cC86(_438034)), cC12xcomp(_438034), cC2xcomp(_438034)], (1896 ^ _375763) ^ [_438334] : [cC86(_438334), -(ra_Px32(_438334, 1899 ^ [_438334]))], (1903 ^ _375763) ^ [_438539] : [1904 ^ _375763 : [(1905 ^ _375763) ^ [_438606] : [ra_Px32(_438539, _438606)]], -(cC86(_438539))], (1909 ^ _375763) ^ [_438780] : [cC86xcomp(_438780), 1912 ^ _375763 : [(1913 ^ _375763) ^ [_438891] : [ra_Px32(_438780, _438891)]]], (1915 ^ _375763) ^ [_438957] : [-(ra_Px32(_438957, 1916 ^ [_438957])), -(cC86xcomp(_438957))], (1922 ^ _375763) ^ [_439230] : [cC88(_439230), -(ra_Px33(_439230, 1925 ^ [_439230]))], (1929 ^ _375763) ^ [_439435] : [1930 ^ _375763 : [(1931 ^ _375763) ^ [_439502] : [ra_Px33(_439435, _439502)]], -(cC88(_439435))], (1935 ^ _375763) ^ [_439676] : [cC88(_439676), 1938 ^ _375763 : [(1939 ^ _375763) ^ [] : [-(cC84xcomp(_439676))], (1941 ^ _375763) ^ [] : [-(cC86xcomp(_439676))]]], (1943 ^ _375763) ^ [_439899] : [-(cC88(_439899)), cC84xcomp(_439899), cC86xcomp(_439899)], (1953 ^ _375763) ^ [_440199] : [cC88xcomp(_440199), 1956 ^ _375763 : [(1957 ^ _375763) ^ [_440310] : [ra_Px33(_440199, _440310)]]], (1959 ^ _375763) ^ [_440376] : [-(ra_Px33(_440376, 1960 ^ [_440376])), -(cC88xcomp(_440376))], (1966 ^ _375763) ^ [_440649] : [cC90(_440649), -(ra_Px50(_440649, 1969 ^ [_440649]))], (1973 ^ _375763) ^ [_440854] : [1974 ^ _375763 : [(1975 ^ _375763) ^ [_440921] : [ra_Px50(_440854, _440921)]], -(cC90(_440854))], (1979 ^ _375763) ^ [_441095] : [cC90(_441095), 1983 ^ _375763 : [(1984 ^ _375763) ^ [] : [-(rR1(_441095, 1982 ^ [_441095]))], (1986 ^ _375763) ^ [] : [-(cC88xcomp(1982 ^ [_441095]))]]], (1988 ^ _375763) ^ [_441381] : [-(cC90(_441381)), 1989 ^ _375763 : [(1990 ^ _375763) ^ [_441469] : [rR1(_441381, _441469), cC88xcomp(_441469)]]], (1998 ^ _375763) ^ [_441743] : [cC90xcomp(_441743), 2001 ^ _375763 : [(2002 ^ _375763) ^ [_441854] : [ra_Px50(_441743, _441854)]]], (2004 ^ _375763) ^ [_441920] : [-(ra_Px50(_441920, 2005 ^ [_441920])), -(cC90xcomp(_441920))], (2011 ^ _375763) ^ [_442193] : [cC92(_442193), -(ra_Px57(_442193, 2014 ^ [_442193]))], (2018 ^ _375763) ^ [_442398] : [2019 ^ _375763 : [(2020 ^ _375763) ^ [_442465] : [ra_Px57(_442398, _442465)]], -(cC92(_442398))], (2024 ^ _375763) ^ [_442639] : [cC92(_442639), 2028 ^ _375763 : [(2029 ^ _375763) ^ [] : [-(rR1(_442639, 2027 ^ [_442639]))], (2031 ^ _375763) ^ [] : [-(cC90(2027 ^ [_442639]))]]], (2033 ^ _375763) ^ [_442925] : [-(cC92(_442925)), 2034 ^ _375763 : [(2035 ^ _375763) ^ [_443013] : [rR1(_442925, _443013), cC90(_443013)]]], (2043 ^ _375763) ^ [_443287] : [cC92xcomp(_443287), 2046 ^ _375763 : [(2047 ^ _375763) ^ [_443398] : [ra_Px57(_443287, _443398)]]], (2049 ^ _375763) ^ [_443464] : [-(ra_Px57(_443464, 2050 ^ [_443464])), -(cC92xcomp(_443464))], (2056 ^ _375763) ^ [_443737] : [cC94(_443737), 2060 ^ _375763 : [(2061 ^ _375763) ^ [] : [-(rR1(_443737, 2059 ^ [_443737]))], (2063 ^ _375763) ^ [] : [-(cC92(2059 ^ [_443737]))]]], (2065 ^ _375763) ^ [_444023] : [-(cC94(_444023)), 2066 ^ _375763 : [(2067 ^ _375763) ^ [_444111] : [rR1(_444023, _444111), cC92(_444111)]]], (2075 ^ _375763) ^ [_444385] : [cC94(_444385), -(ra_Px48(_444385, 2078 ^ [_444385]))], (2082 ^ _375763) ^ [_444590] : [2083 ^ _375763 : [(2084 ^ _375763) ^ [_444657] : [ra_Px48(_444590, _444657)]], -(cC94(_444590))], (2088 ^ _375763) ^ [_444831] : [cC94xcomp(_444831), 2091 ^ _375763 : [(2092 ^ _375763) ^ [_444942] : [ra_Px48(_444831, _444942)]]], (2094 ^ _375763) ^ [_445008] : [-(ra_Px48(_445008, 2095 ^ [_445008])), -(cC94xcomp(_445008))], (2101 ^ _375763) ^ [_445281] : [cC96(_445281), 2105 ^ _375763 : [(2106 ^ _375763) ^ [] : [-(rR1(_445281, 2104 ^ [_445281]))], (2108 ^ _375763) ^ [] : [-(cC94(2104 ^ [_445281]))]]], (2110 ^ _375763) ^ [_445567] : [-(cC96(_445567)), 2111 ^ _375763 : [(2112 ^ _375763) ^ [_445655] : [rR1(_445567, _445655), cC94(_445655)]]], (2120 ^ _375763) ^ [_445929] : [cC96(_445929), 2123 ^ _375763 : [(2124 ^ _375763) ^ [_446040] : [ra_Px34(_445929, _446040)]]], (2126 ^ _375763) ^ [_446106] : [-(ra_Px34(_446106, 2127 ^ [_446106])), -(cC96(_446106))], (2133 ^ _375763) ^ [_446379] : [cC96xcomp(_446379), -(ra_Px34(_446379, 2136 ^ [_446379]))], (2140 ^ _375763) ^ [_446584] : [2141 ^ _375763 : [(2142 ^ _375763) ^ [_446651] : [ra_Px34(_446584, _446651)]], -(cC96xcomp(_446584))], (2146 ^ _375763) ^ [_446825] : [cC98(_446825), -(ra_Px35(_446825, 2149 ^ [_446825]))], (2153 ^ _375763) ^ [_447030] : [2154 ^ _375763 : [(2155 ^ _375763) ^ [_447097] : [ra_Px35(_447030, _447097)]], -(cC98(_447030))], (2159 ^ _375763) ^ [_447271] : [cC98(_447271), 2162 ^ _375763 : [(2163 ^ _375763) ^ [] : [-(cC96xcomp(_447271))], (2165 ^ _375763) ^ [] : [-(cC82(_447271))]]], (2167 ^ _375763) ^ [_447494] : [-(cC98(_447494)), cC96xcomp(_447494), cC82(_447494)], (2177 ^ _375763) ^ [_447794] : [cC98xcomp(_447794), 2180 ^ _375763 : [(2181 ^ _375763) ^ [_447905] : [ra_Px35(_447794, _447905)]]], (2183 ^ _375763) ^ [_447971] : [-(ra_Px35(_447971, 2184 ^ [_447971])), -(cC98xcomp(_447971))], (2190 ^ _375763) ^ [_448244] : [cTEST(_448244), 2193 ^ _375763 : [(2194 ^ _375763) ^ [] : [-(cC108(_448244))], (2196 ^ _375763) ^ [] : [-(cC130(_448244))]]], (2198 ^ _375763) ^ [_448467] : [-(cTEST(_448467)), cC108(_448467), cC130(_448467)], (2208 ^ _375763) ^ [_448738] : [rR1(iV16439, _448738), -(cC98(_448738))], (2214 ^ _375763) ^ [] : [-(cowlThing(iV16439))], (2216 ^ _375763) ^ [] : [-(cC100xcomp(iV16439))], (2218 ^ _375763) ^ [] : [-(cTEST(iV16439))], (2220 ^ _375763) ^ [] : [-(rR1(iV16439, iV16440))], (2222 ^ _375763) ^ [] : [-(rR1(iV16439, iV16442))], (2224 ^ _375763) ^ [] : [-(rR1(iV16439, iV16441))], (2226 ^ _375763) ^ [] : [-(cowlThing(iV16440))], (2228 ^ _375763) ^ [] : [-(cC96xcomp(iV16440))], (2230 ^ _375763) ^ [_449350] : [rR1(iV16440, _449350), -(cC94xcomp(_449350))], (2236 ^ _375763) ^ [_449538] : [rR1(iV16440, _449538), -(cC76(_449538))], (2242 ^ _375763) ^ [] : [-(cC102xcomp(iV16440))], (2244 ^ _375763) ^ [] : [-(cC78xcomp(iV16440))], (2246 ^ _375763) ^ [] : [-(rR1(iV16440, iV16463))], (2248 ^ _375763) ^ [] : [-(cowlThing(iV16441))], (2250 ^ _375763) ^ [] : [-(cowlThing(iV16442))], (2252 ^ _375763) ^ [] : [-(cowlThing(iV16448))], (2254 ^ _375763) ^ [] : [-(cTOP(iV16448))], (2256 ^ _375763) ^ [] : [-(cC52xcomp(iV16448))], (2258 ^ _375763) ^ [_450150] : [rR1(iV16448, _450150), -(cC50(_450150))], (2264 ^ _375763) ^ [_450338] : [rR1(iV16448, _450338), -(cC68(_450338))], (2270 ^ _375763) ^ [_450526] : [rR1(iV16448, _450526), -(cC34(_450526))], (2276 ^ _375763) ^ [] : [-(cC36xcomp(iV16448))], (2278 ^ _375763) ^ [] : [-(cC90xcomp(iV16448))], (2280 ^ _375763) ^ [_450820] : [rR1(iV16448, _450820), -(cC88(_450820))], (2286 ^ _375763) ^ [] : [-(cC70xcomp(iV16448))], (2288 ^ _375763) ^ [] : [-(rR1(iV16448, iV16449))], (2290 ^ _375763) ^ [] : [-(cowlThing(iV16449))], (2292 ^ _375763) ^ [] : [-(cC74xcomp(iV16453))], (2294 ^ _375763) ^ [] : [-(cowlThing(iV16453))], (2296 ^ _375763) ^ [_451273] : [rR1(iV16453, _451273), -(cC72xcomp(_451273))], (2302 ^ _375763) ^ [] : [-(cC16xcomp(iV16453))], (2304 ^ _375763) ^ [_451514] : [rR1(iV16453, _451514), -(cC56(_451514))], (2310 ^ _375763) ^ [_451702] : [rR1(iV16453, _451702), -(cC92xcomp(_451702))], (2316 ^ _375763) ^ [] : [-(cC94xcomp(iV16453))], (2318 ^ _375763) ^ [] : [-(cC58xcomp(iV16453))], (2320 ^ _375763) ^ [] : [-(rR1(iV16453, iV16461))], (2322 ^ _375763) ^ [_452049] : [rR1(iV16455, _452049), -(cC52xcomp(_452049))], (2328 ^ _375763) ^ [] : [-(cowlThing(iV16455))], (2330 ^ _375763) ^ [] : [-(cC40xcomp(iV16455))], (2332 ^ _375763) ^ [_452343] : [rR1(iV16455, _452343), -(cC90xcomp(_452343))], (2338 ^ _375763) ^ [] : [-(cC12xcomp(iV16455))], (2340 ^ _375763) ^ [_452584] : [rR1(iV16455, _452584), -(cC38(_452584))], (2346 ^ _375763) ^ [] : [-(cC92xcomp(iV16455))], (2348 ^ _375763) ^ [] : [-(cC54xcomp(iV16455))], (2350 ^ _375763) ^ [_452878] : [rR1(iV16455, _452878), -(cC70xcomp(_452878))], (2356 ^ _375763) ^ [] : [-(cC72xcomp(iV16455))], (2358 ^ _375763) ^ [] : [-(rR1(iV16455, iV16460))], (2360 ^ _375763) ^ [_453172] : [rR1(iV16457, _453172), -(cC68(_453172))], (2366 ^ _375763) ^ [] : [-(cowlThing(iV16457))], (2368 ^ _375763) ^ [_453413] : [rR1(iV16457, _453413), -(cC34(_453413))], (2374 ^ _375763) ^ [] : [-(cTOP(iV16457))], (2376 ^ _375763) ^ [] : [-(cC52xcomp(iV16457))], (2378 ^ _375763) ^ [] : [-(cC8xcomp(iV16457))], (2380 ^ _375763) ^ [_453760] : [rR1(iV16457, _453760), -(cC88(_453760))], (2386 ^ _375763) ^ [] : [-(cC36xcomp(iV16457))], (2388 ^ _375763) ^ [] : [-(cC90xcomp(iV16457))], (2390 ^ _375763) ^ [_454054] : [rR1(iV16457, _454054), -(cC50(_454054))], (2396 ^ _375763) ^ [] : [-(cC70xcomp(iV16457))], (2398 ^ _375763) ^ [] : [-(cowlThing(iV16459))], (2400 ^ _375763) ^ [] : [-(cC14xcomp(iV16459))], (2402 ^ _375763) ^ [] : [-(cC8xcomp(iV16459))], (2404 ^ _375763) ^ [] : [-(cC10xcomp(iV16459))], (2406 ^ _375763) ^ [] : [-(cC30xcomp(iV16459))], (2408 ^ _375763) ^ [] : [-(cC84xcomp(iV16459))], (2410 ^ _375763) ^ [] : [-(cC12(iV16459))], (2412 ^ _375763) ^ [] : [-(cC46xcomp(iV16459))], (2414 ^ _375763) ^ [] : [-(cC64xcomp(iV16459))], (2416 ^ _375763) ^ [] : [-(cC4(iV16459))], (2418 ^ _375763) ^ [] : [-(cC86xcomp(iV16459))], (2420 ^ _375763) ^ [] : [-(cC32xcomp(iV16459))], (2422 ^ _375763) ^ [] : [-(cC48xcomp(iV16459))], (2424 ^ _375763) ^ [] : [-(cC18xcomp(iV16459))], (2426 ^ _375763) ^ [] : [-(cC2xcomp(iV16459))], (2428 ^ _375763) ^ [] : [-(cC6xcomp(iV16459))], (2430 ^ _375763) ^ [] : [-(cC66xcomp(iV16459))], (2432 ^ _375763) ^ [_455196] : [rR1(iV16460, _455196), -(cC68(_455196))], (2438 ^ _375763) ^ [] : [-(cowlThing(iV16460))], (2440 ^ _375763) ^ [_455437] : [rR1(iV16460, _455437), -(cC34(_455437))], (2446 ^ _375763) ^ [] : [-(cTOP(iV16460))], (2448 ^ _375763) ^ [] : [-(cC52xcomp(iV16460))], (2450 ^ _375763) ^ [] : [-(cC8xcomp(iV16460))], (2452 ^ _375763) ^ [] : [-(cC36xcomp(iV16460))], (2454 ^ _375763) ^ [_455837] : [rR1(iV16460, _455837), -(cC50(_455837))], (2460 ^ _375763) ^ [_456025] : [rR1(iV16460, _456025), -(cC88(_456025))], (2466 ^ _375763) ^ [] : [-(cC90xcomp(iV16460))], (2468 ^ _375763) ^ [] : [-(cC70xcomp(iV16460))], (2470 ^ _375763) ^ [] : [-(cowlThing(iV16461))], (2472 ^ _375763) ^ [] : [-(cC40xcomp(iV16461))], (2474 ^ _375763) ^ [_456425] : [rR1(iV16461, _456425), -(cC90xcomp(_456425))], (2480 ^ _375763) ^ [_456613] : [rR1(iV16461, _456613), -(cC70xcomp(_456613))], (2486 ^ _375763) ^ [] : [-(cC12xcomp(iV16461))], (2488 ^ _375763) ^ [_456854] : [rR1(iV16461, _456854), -(cC52xcomp(_456854))], (2494 ^ _375763) ^ [] : [-(cC92xcomp(iV16461))], (2496 ^ _375763) ^ [] : [-(cC54xcomp(iV16461))], (2498 ^ _375763) ^ [_457148] : [rR1(iV16461, _457148), -(cC38(_457148))], (2504 ^ _375763) ^ [] : [-(cC72xcomp(iV16461))], (2506 ^ _375763) ^ [] : [-(rR1(iV16461, iV16462))], (2508 ^ _375763) ^ [_457442] : [rR1(iV16462, _457442), -(cC50(_457442))], (2514 ^ _375763) ^ [_457630] : [rR1(iV16462, _457630), -(cC68(_457630))], (2520 ^ _375763) ^ [] : [-(cowlThing(iV16462))], (2522 ^ _375763) ^ [] : [-(cTOP(iV16462))], (2524 ^ _375763) ^ [] : [-(cC52xcomp(iV16462))], (2526 ^ _375763) ^ [] : [-(cC8xcomp(iV16462))], (2528 ^ _375763) ^ [_458030] : [rR1(iV16462, _458030), -(cC34(_458030))], (2534 ^ _375763) ^ [_458218] : [rR1(iV16462, _458218), -(cC88(_458218))], (2540 ^ _375763) ^ [] : [-(cC36xcomp(iV16462))], (2542 ^ _375763) ^ [] : [-(cC90xcomp(iV16462))], (2544 ^ _375763) ^ [] : [-(cC70xcomp(iV16462))], (2546 ^ _375763) ^ [] : [-(cC74xcomp(iV16463))], (2548 ^ _375763) ^ [] : [-(cowlThing(iV16463))], (2550 ^ _375763) ^ [] : [-(cC16xcomp(iV16463))], (2552 ^ _375763) ^ [_458724] : [rR1(iV16463, _458724), -(cC92xcomp(_458724))], (2558 ^ _375763) ^ [_458912] : [rR1(iV16463, _458912), -(cC72xcomp(_458912))], (2564 ^ _375763) ^ [] : [-(cC94xcomp(iV16463))], (2566 ^ _375763) ^ [_459153] : [rR1(iV16463, _459153), -(cC56(_459153))], (2572 ^ _375763) ^ [] : [-(cC58xcomp(iV16463))], (2574 ^ _375763) ^ [] : [-(rR1(iV16463, iV16464))], (2576 ^ _375763) ^ [] : [-(cowlThing(iV16464))], (2578 ^ _375763) ^ [_459500] : [rR1(iV16464, _459500), -(cC38(_459500))], (2584 ^ _375763) ^ [] : [-(cC40xcomp(iV16464))], (2586 ^ _375763) ^ [] : [-(cC12xcomp(iV16464))], (2588 ^ _375763) ^ [_459794] : [rR1(iV16464, _459794), -(cC52xcomp(_459794))], (2594 ^ _375763) ^ [] : [-(cC92xcomp(iV16464))], (2596 ^ _375763) ^ [] : [-(cC54xcomp(iV16464))], (2598 ^ _375763) ^ [_460088] : [rR1(iV16464, _460088), -(cC90xcomp(_460088))], (2604 ^ _375763) ^ [_460276] : [rR1(iV16464, _460276), -(cC70xcomp(_460276))], (2610 ^ _375763) ^ [] : [-(cC72xcomp(iV16464))], (2612 ^ _375763) ^ [] : [-(rR1(iV16464, iV16465))], (2614 ^ _375763) ^ [_460570] : [rR1(iV16465, _460570), -(cC34(_460570))], (2620 ^ _375763) ^ [] : [-(cowlThing(iV16465))], (2622 ^ _375763) ^ [] : [-(cTOP(iV16465))], (2624 ^ _375763) ^ [_460864] : [rR1(iV16465, _460864), -(cC88(_460864))], (2630 ^ _375763) ^ [] : [-(cC52xcomp(iV16465))], (2632 ^ _375763) ^ [] : [-(cC8xcomp(iV16465))], (2634 ^ _375763) ^ [_461158] : [rR1(iV16465, _461158), -(cC68(_461158))], (2640 ^ _375763) ^ [] : [-(cC36xcomp(iV16465))], (2642 ^ _375763) ^ [] : [-(cC90xcomp(iV16465))], (2650 ^ _375763) ^ [] : [-(cC70xcomp(iV16465))], (2644 ^ _375763) ^ [_461452] : [rR1(iV16465, _461452), -(cC50(_461452))]], input).
% 0.64/1.39  ncf('1',plain,[cowlNothing(2653 ^ [])],start(4 ^ 0,bind([[_375909], [2653 ^ []]]))).
% 0.64/1.39  ncf('1.1',plain,[-(cowlNothing(2653 ^ [])), cowlThing(2653 ^ []), 2666 : -(xsd_string(2662 ^ [])), 2670 : xsd_integer(2662 ^ []), 2670 : cC130(iV16439), 2670 : cC108(iV16439), 2670 : cC104(iV16439), 2670 : cC106(iV16439), 2670 : cC28(iV16439), 2670 : cowlThing(iV16439), 2670 : cC98(iV16440), 2670 : cC80(iV16440), 2670 : cC82(iV16440), 2670 : cowlThing(iV16440), 2670 : cC38(iV16448), 2670 : cowlThing(iV16448), 2670 : cC76(iV16453), 2670 : cC62(iV16453), 2670 : cowlThing(iV16453), 2670 : cC60(iV16453), 2670 : cC56(iV16455), 2670 : cC44(iV16455), 2670 : cC42(iV16455), 2670 : cowlThing(iV16455), 2670 : cC38(iV16457), 2670 : cowlThing(iV16457), 2670 : cC50(iV16459), 2670 : cC88(iV16459), 2670 : cC34(iV16459), 2670 : cC68(iV16459), 2670 : cowlThing(iV16459), 2670 : cC38(iV16460), 2670 : cowlThing(iV16460), 2670 : cC42(iV16461), 2670 : cC56(iV16461), 2670 : cC44(iV16461), 2670 : cowlThing(iV16461), 2670 : cC38(iV16462), 2670 : cowlThing(iV16462), 2670 : cC76(iV16463), 2670 : cC62(iV16463), 2670 : cowlThing(iV16463), 2670 : cC60(iV16463), 2670 : cC56(iV16464), 2670 : cC42(iV16464), 2670 : cC44(iV16464), 2670 : cowlThing(iV16464), 2670 : cC38(iV16465), 2670 : cowlThing(iV16465)],extension(2652 ^ 1)).
% 0.64/1.39  ncf('1.1.1',plain,[-(cowlThing(2653 ^ []))],extension(2 ^ 2,bind([[_375867], [2653 ^ []]]))).
% 0.64/1.39  ncf('1.1.2',plain,[xsd_string(2662 ^ []), xsd_integer(2662 ^ [])],extension(6 ^ 4,bind([[_376032], [2662 ^ []]]))).
% 0.64/1.39  ncf('1.1.2.1',plain,[-(xsd_integer(2662 ^ []))],extension(2668 ^ 5)).
% 0.64/1.39  ncf('1.1.3',plain,[-(xsd_integer(2662 ^ [])), -(xsd_string(2662 ^ []))],extension(12 ^ 4,bind([[_376185], [2662 ^ []]]))).
% 0.64/1.39  ncf('1.1.3.1',plain,[xsd_string(2662 ^ [])],extension(2672 ^ 5)).
% 0.64/1.39  ncf('1.1.4',plain,[-(cC130(iV16439)), cTEST(iV16439)],extension(2190 ^ 2,bind([[_448244], [iV16439]]))).
% 0.64/1.39  ncf('1.1.4.1',plain,[-(cTEST(iV16439))],extension(2218 ^ 3)).
% 0.64/1.39  ncf('1.1.5',plain,[-(cC108(iV16439)), cTEST(iV16439)],extension(2190 ^ 2,bind([[_448244], [iV16439]]))).
% 0.64/1.39  ncf('1.1.5.1',plain,[-(cTEST(iV16439))],extension(2218 ^ 3)).
% 0.64/1.39  ncf('1.1.6',plain,[-(cC104(iV16439)), cC106(iV16439)],extension(152 ^ 2,bind([[_380912], [iV16439]]))).
% 0.64/1.39  ncf('1.1.6.1',plain,[-(cC106(iV16439)), cC108(iV16439)],extension(170 ^ 3,bind([[_381435], [iV16439]]))).
% 0.64/1.39  ncf('1.1.6.1.1',plain,[-(cC108(iV16439))],lemmata('[1].x')).
% 0.64/1.39  ncf('1.1.7',plain,[-(cC106(iV16439)), cC104(iV16439), cC100xcomp(iV16439)],extension(160 ^ 2,bind([[_381135], [iV16439]]))).
% 0.64/1.39  ncf('1.1.7.1',plain,[-(cC104(iV16439))],lemmata('[1].x')).
% 0.64/1.39  ncf('1.1.7.2',plain,[-(cC100xcomp(iV16439))],extension(2216 ^ 3)).
% 0.64/1.39  ncf('1.1.8',plain,[-(cC28(iV16439)), cC108(iV16439)],extension(170 ^ 2,bind([[_381435], [iV16439]]))).
% 0.64/1.39  ncf('1.1.8.1',plain,[-(cC108(iV16439))],lemmata('[1].x')).
% 0.64/1.39  ncf('1.1.9',plain,[-(cowlThing(iV16439))],extension(2 ^ 2,bind([[_375867], [iV16439]]))).
% 0.64/1.39  ncf('1.1.10',plain,[-(cC98(iV16440)), cC96xcomp(iV16440), cC82(iV16440)],extension(2167 ^ 2,bind([[_447494], [iV16440]]))).
% 0.64/1.39  ncf('1.1.10.1',plain,[-(cC96xcomp(iV16440))],extension(2228 ^ 3)).
% 0.64/1.39  ncf('1.1.10.2',plain,[-(cC82(iV16440)), cC80(iV16440), cC78xcomp(iV16440)],extension(1824 ^ 3,bind([[_436092], [iV16440]]))).
% 0.64/1.39  ncf('1.1.10.2.1',plain,[-(cC80(iV16440)), 1808 : rR1(iV16440, iV16463), 1808 : cC16xcomp(iV16463)],extension(1806 ^ 4,bind([[_435507, _435595], [iV16440, iV16463]]))).
% 0.64/1.39  ncf('1.1.10.2.1.1',plain,[-(rR1(iV16440, iV16463))],extension(2246 ^ 7)).
% 0.64/1.39  ncf('1.1.10.2.1.2',plain,[-(cC16xcomp(iV16463))],extension(2550 ^ 7)).
% 0.64/1.39  ncf('1.1.10.2.2',plain,[-(cC78xcomp(iV16440))],extension(2244 ^ 4)).
% 0.64/1.39  ncf('1.1.11',plain,[-(cC80(iV16440)), 1808 : rR1(iV16440, iV16463), 1808 : cC16xcomp(iV16463)],extension(1806 ^ 2,bind([[_435507, _435595], [iV16440, iV16463]]))).
% 0.64/1.39  ncf('1.1.11.1',plain,[-(rR1(iV16440, iV16463))],extension(2246 ^ 5)).
% 0.64/1.39  ncf('1.1.11.2',plain,[-(cC16xcomp(iV16463))],extension(2550 ^ 5)).
% 0.64/1.39  ncf('1.1.12',plain,[-(cC82(iV16440)), cC80(iV16440), cC78xcomp(iV16440)],extension(1824 ^ 2,bind([[_436092], [iV16440]]))).
% 0.64/1.39  ncf('1.1.12.1',plain,[-(cC80(iV16440))],lemmata('[1].x')).
% 0.64/1.39  ncf('1.1.12.2',plain,[-(cC78xcomp(iV16440))],extension(2244 ^ 3)).
% 0.64/1.39  ncf('1.1.13',plain,[-(cowlThing(iV16440))],extension(2 ^ 2,bind([[_375867], [iV16440]]))).
% 0.64/1.39  ncf('1.1.14',plain,[-(cC38(iV16448)), cTOP(iV16448), cC36xcomp(iV16448)],extension(879 ^ 2,bind([[_404768], [iV16448]]))).
% 0.64/1.39  ncf('1.1.14.1',plain,[-(cTOP(iV16448))],extension(2254 ^ 3)).
% 0.64/1.39  ncf('1.1.14.2',plain,[-(cC36xcomp(iV16448))],extension(2276 ^ 3)).
% 0.64/1.39  ncf('1.1.15',plain,[-(cowlThing(iV16448))],extension(2 ^ 2,bind([[_375867], [iV16448]]))).
% 0.64/1.39  ncf('1.1.16',plain,[-(cC76(iV16453)), cC74xcomp(iV16453), cC62(iV16453)],extension(1703 ^ 2,bind([[_432031], [iV16453]]))).
% 0.64/1.39  ncf('1.1.16.1',plain,[-(cC74xcomp(iV16453))],extension(2292 ^ 3)).
% 0.64/1.39  ncf('1.1.16.2',plain,[-(cC62(iV16453)), cC60(iV16453), cC58xcomp(iV16453)],extension(1405 ^ 3,bind([[_422173], [iV16453]]))).
% 0.64/1.39  ncf('1.1.16.2.1',plain,[-(cC60(iV16453)), 1389 : rR1(iV16453, iV16461), 1389 : cC12xcomp(iV16461)],extension(1387 ^ 4,bind([[_421588, _421676], [iV16453, iV16461]]))).
% 0.64/1.39  ncf('1.1.16.2.1.1',plain,[-(rR1(iV16453, iV16461))],extension(2320 ^ 7)).
% 0.64/1.39  ncf('1.1.16.2.1.2',plain,[-(cC12xcomp(iV16461))],extension(2486 ^ 7)).
% 0.64/1.39  ncf('1.1.16.2.2',plain,[-(cC58xcomp(iV16453))],extension(2318 ^ 4)).
% 0.64/1.39  ncf('1.1.17',plain,[-(cC62(iV16453)), cC60(iV16453), cC58xcomp(iV16453)],extension(1405 ^ 2,bind([[_422173], [iV16453]]))).
% 0.64/1.39  ncf('1.1.17.1',plain,[-(cC60(iV16453)), 1389 : rR1(iV16453, iV16461), 1389 : cC12xcomp(iV16461)],extension(1387 ^ 3,bind([[_421588, _421676], [iV16453, iV16461]]))).
% 0.64/1.39  ncf('1.1.17.1.1',plain,[-(rR1(iV16453, iV16461))],extension(2320 ^ 6)).
% 0.64/1.39  ncf('1.1.17.1.2',plain,[-(cC12xcomp(iV16461))],extension(2486 ^ 6)).
% 0.64/1.39  ncf('1.1.17.2',plain,[-(cC58xcomp(iV16453))],extension(2318 ^ 3)).
% 0.64/1.39  ncf('1.1.18',plain,[-(cowlThing(iV16453))],extension(2 ^ 2,bind([[_375867], [iV16453]]))).
% 0.64/1.39  ncf('1.1.19',plain,[-(cC60(iV16453)), 1389 : rR1(iV16453, iV16461), 1389 : cC12xcomp(iV16461)],extension(1387 ^ 2,bind([[_421588, _421676], [iV16453, iV16461]]))).
% 0.64/1.39  ncf('1.1.19.1',plain,[-(rR1(iV16453, iV16461))],extension(2320 ^ 5)).
% 0.64/1.39  ncf('1.1.19.2',plain,[-(cC12xcomp(iV16461))],extension(2486 ^ 5)).
% 0.64/1.39  ncf('1.1.20',plain,[-(cC56(iV16455)), cC54xcomp(iV16455), cC44(iV16455)],extension(1253 ^ 2,bind([[_417143], [iV16455]]))).
% 0.64/1.39  ncf('1.1.20.1',plain,[-(cC54xcomp(iV16455))],extension(2348 ^ 3)).
% 0.64/1.39  ncf('1.1.20.2',plain,[-(cC44(iV16455)), cC40xcomp(iV16455), cC42(iV16455)],extension(1013 ^ 3,bind([[_409275], [iV16455]]))).
% 0.64/1.39  ncf('1.1.20.2.1',plain,[-(cC40xcomp(iV16455))],extension(2330 ^ 4)).
% 0.64/1.39  ncf('1.1.20.2.2',plain,[-(cC42(iV16455)), 997 : rR1(iV16455, iV16460), 997 : cC8xcomp(iV16460)],extension(995 ^ 4,bind([[_408690, _408778], [iV16455, iV16460]]))).
% 0.64/1.39  ncf('1.1.20.2.2.1',plain,[-(rR1(iV16455, iV16460))],extension(2358 ^ 7)).
% 0.64/1.39  ncf('1.1.20.2.2.2',plain,[-(cC8xcomp(iV16460))],extension(2450 ^ 7)).
% 0.64/1.39  ncf('1.1.21',plain,[-(cC44(iV16455)), cC40xcomp(iV16455), cC42(iV16455)],extension(1013 ^ 2,bind([[_409275], [iV16455]]))).
% 0.64/1.39  ncf('1.1.21.1',plain,[-(cC40xcomp(iV16455))],extension(2330 ^ 3)).
% 0.64/1.39  ncf('1.1.21.2',plain,[-(cC42(iV16455)), 997 : rR1(iV16455, iV16460), 997 : cC8xcomp(iV16460)],extension(995 ^ 3,bind([[_408690, _408778], [iV16455, iV16460]]))).
% 0.64/1.39  ncf('1.1.21.2.1',plain,[-(rR1(iV16455, iV16460))],extension(2358 ^ 6)).
% 0.64/1.39  ncf('1.1.21.2.2',plain,[-(cC8xcomp(iV16460))],extension(2450 ^ 6)).
% 0.64/1.39  ncf('1.1.22',plain,[-(cC42(iV16455)), 997 : rR1(iV16455, iV16460), 997 : cC8xcomp(iV16460)],extension(995 ^ 2,bind([[_408690, _408778], [iV16455, iV16460]]))).
% 0.64/1.39  ncf('1.1.22.1',plain,[-(rR1(iV16455, iV16460))],extension(2358 ^ 5)).
% 0.64/1.39  ncf('1.1.22.2',plain,[-(cC8xcomp(iV16460))],extension(2450 ^ 5)).
% 0.64/1.39  ncf('1.1.23',plain,[-(cowlThing(iV16455))],extension(2 ^ 2,bind([[_375867], [iV16455]]))).
% 0.64/1.39  ncf('1.1.24',plain,[-(cC38(iV16457)), cTOP(iV16457), cC36xcomp(iV16457)],extension(879 ^ 2,bind([[_404768], [iV16457]]))).
% 0.64/1.39  ncf('1.1.24.1',plain,[-(cTOP(iV16457))],extension(2374 ^ 3)).
% 0.64/1.39  ncf('1.1.24.2',plain,[-(cC36xcomp(iV16457))],extension(2386 ^ 3)).
% 0.64/1.39  ncf('1.1.25',plain,[-(cowlThing(iV16457))],extension(2 ^ 2,bind([[_375867], [iV16457]]))).
% 0.64/1.39  ncf('1.1.26',plain,[-(cC50(iV16459)), cC46xcomp(iV16459), cC48xcomp(iV16459)],extension(1119 ^ 2,bind([[_412636], [iV16459]]))).
% 0.64/1.39  ncf('1.1.26.1',plain,[-(cC46xcomp(iV16459))],extension(2412 ^ 3)).
% 0.64/1.39  ncf('1.1.26.2',plain,[-(cC48xcomp(iV16459))],extension(2422 ^ 3)).
% 0.64/1.39  ncf('1.1.27',plain,[-(cC88(iV16459)), cC84xcomp(iV16459), cC86xcomp(iV16459)],extension(1943 ^ 2,bind([[_439899], [iV16459]]))).
% 0.64/1.39  ncf('1.1.27.1',plain,[-(cC84xcomp(iV16459))],extension(2408 ^ 3)).
% 0.64/1.39  ncf('1.1.27.2',plain,[-(cC86xcomp(iV16459))],extension(2418 ^ 3)).
% 0.64/1.39  ncf('1.1.28',plain,[-(cC34(iV16459)), cC30xcomp(iV16459), cC32xcomp(iV16459)],extension(803 ^ 2,bind([[_402251], [iV16459]]))).
% 0.64/1.39  ncf('1.1.28.1',plain,[-(cC30xcomp(iV16459))],extension(2406 ^ 3)).
% 0.64/1.39  ncf('1.1.28.2',plain,[-(cC32xcomp(iV16459))],extension(2420 ^ 3)).
% 0.64/1.39  ncf('1.1.29',plain,[-(cC68(iV16459)), cC64xcomp(iV16459), cC66xcomp(iV16459)],extension(1524 ^ 2,bind([[_425980], [iV16459]]))).
% 0.64/1.39  ncf('1.1.29.1',plain,[-(cC64xcomp(iV16459))],extension(2414 ^ 3)).
% 0.64/1.39  ncf('1.1.29.2',plain,[-(cC66xcomp(iV16459))],extension(2430 ^ 3)).
% 0.64/1.39  ncf('1.1.30',plain,[-(cowlThing(iV16459))],extension(2 ^ 2,bind([[_375867], [iV16459]]))).
% 0.64/1.39  ncf('1.1.31',plain,[-(cC38(iV16460)), cTOP(iV16460), cC36xcomp(iV16460)],extension(879 ^ 2,bind([[_404768], [iV16460]]))).
% 0.64/1.39  ncf('1.1.31.1',plain,[-(cTOP(iV16460))],extension(2446 ^ 3)).
% 0.64/1.39  ncf('1.1.31.2',plain,[-(cC36xcomp(iV16460))],extension(2452 ^ 3)).
% 0.64/1.39  ncf('1.1.32',plain,[-(cowlThing(iV16460))],extension(2 ^ 2,bind([[_375867], [iV16460]]))).
% 0.64/1.39  ncf('1.1.33',plain,[-(cC42(iV16461)), 997 : rR1(iV16461, iV16462), 997 : cC8xcomp(iV16462)],extension(995 ^ 2,bind([[_408690, _408778], [iV16461, iV16462]]))).
% 0.64/1.39  ncf('1.1.33.1',plain,[-(rR1(iV16461, iV16462))],extension(2506 ^ 5)).
% 0.64/1.39  ncf('1.1.33.2',plain,[-(cC8xcomp(iV16462))],extension(2526 ^ 5)).
% 0.64/1.39  ncf('1.1.34',plain,[-(cC56(iV16461)), cC54xcomp(iV16461), cC44(iV16461)],extension(1253 ^ 2,bind([[_417143], [iV16461]]))).
% 0.64/1.39  ncf('1.1.34.1',plain,[-(cC54xcomp(iV16461))],extension(2496 ^ 3)).
% 0.64/1.39  ncf('1.1.34.2',plain,[-(cC44(iV16461)), cC40xcomp(iV16461), cC42(iV16461)],extension(1013 ^ 3,bind([[_409275], [iV16461]]))).
% 0.64/1.39  ncf('1.1.34.2.1',plain,[-(cC40xcomp(iV16461))],extension(2472 ^ 4)).
% 0.64/1.39  ncf('1.1.34.2.2',plain,[-(cC42(iV16461))],lemmata('[1].x')).
% 0.64/1.39  ncf('1.1.35',plain,[-(cC44(iV16461)), cC40xcomp(iV16461), cC42(iV16461)],extension(1013 ^ 2,bind([[_409275], [iV16461]]))).
% 0.64/1.39  ncf('1.1.35.1',plain,[-(cC40xcomp(iV16461))],extension(2472 ^ 3)).
% 0.64/1.39  ncf('1.1.35.2',plain,[-(cC42(iV16461))],lemmata('[1].x')).
% 0.64/1.39  ncf('1.1.36',plain,[-(cowlThing(iV16461))],extension(2 ^ 2,bind([[_375867], [iV16461]]))).
% 0.64/1.39  ncf('1.1.37',plain,[-(cC38(iV16462)), cTOP(iV16462), cC36xcomp(iV16462)],extension(879 ^ 2,bind([[_404768], [iV16462]]))).
% 0.64/1.39  ncf('1.1.37.1',plain,[-(cTOP(iV16462))],extension(2522 ^ 3)).
% 0.64/1.39  ncf('1.1.37.2',plain,[-(cC36xcomp(iV16462))],extension(2540 ^ 3)).
% 0.64/1.39  ncf('1.1.38',plain,[-(cowlThing(iV16462))],extension(2 ^ 2,bind([[_375867], [iV16462]]))).
% 0.64/1.39  ncf('1.1.39',plain,[-(cC76(iV16463)), cC74xcomp(iV16463), cC62(iV16463)],extension(1703 ^ 2,bind([[_432031], [iV16463]]))).
% 0.64/1.39  ncf('1.1.39.1',plain,[-(cC74xcomp(iV16463))],extension(2546 ^ 3)).
% 0.64/1.39  ncf('1.1.39.2',plain,[-(cC62(iV16463)), cC60(iV16463), cC58xcomp(iV16463)],extension(1405 ^ 3,bind([[_422173], [iV16463]]))).
% 0.64/1.39  ncf('1.1.39.2.1',plain,[-(cC60(iV16463)), 1389 : rR1(iV16463, iV16464), 1389 : cC12xcomp(iV16464)],extension(1387 ^ 4,bind([[_421588, _421676], [iV16463, iV16464]]))).
% 0.64/1.39  ncf('1.1.39.2.1.1',plain,[-(rR1(iV16463, iV16464))],extension(2574 ^ 7)).
% 0.64/1.39  ncf('1.1.39.2.1.2',plain,[-(cC12xcomp(iV16464))],extension(2586 ^ 7)).
% 0.64/1.39  ncf('1.1.39.2.2',plain,[-(cC58xcomp(iV16463))],extension(2572 ^ 4)).
% 0.64/1.39  ncf('1.1.40',plain,[-(cC62(iV16463)), cC60(iV16463), cC58xcomp(iV16463)],extension(1405 ^ 2,bind([[_422173], [iV16463]]))).
% 0.64/1.39  ncf('1.1.40.1',plain,[-(cC60(iV16463)), 1389 : rR1(iV16463, iV16464), 1389 : cC12xcomp(iV16464)],extension(1387 ^ 3,bind([[_421588, _421676], [iV16463, iV16464]]))).
% 0.64/1.39  ncf('1.1.40.1.1',plain,[-(rR1(iV16463, iV16464))],extension(2574 ^ 6)).
% 0.64/1.39  ncf('1.1.40.1.2',plain,[-(cC12xcomp(iV16464))],extension(2586 ^ 6)).
% 0.64/1.39  ncf('1.1.40.2',plain,[-(cC58xcomp(iV16463))],extension(2572 ^ 3)).
% 0.64/1.39  ncf('1.1.41',plain,[-(cowlThing(iV16463))],extension(2 ^ 2,bind([[_375867], [iV16463]]))).
% 0.64/1.39  ncf('1.1.42',plain,[-(cC60(iV16463)), 1389 : rR1(iV16463, iV16464), 1389 : cC12xcomp(iV16464)],extension(1387 ^ 2,bind([[_421588, _421676], [iV16463, iV16464]]))).
% 0.64/1.39  ncf('1.1.42.1',plain,[-(rR1(iV16463, iV16464))],extension(2574 ^ 5)).
% 0.64/1.39  ncf('1.1.42.2',plain,[-(cC12xcomp(iV16464))],extension(2586 ^ 5)).
% 0.64/1.39  ncf('1.1.43',plain,[-(cC56(iV16464)), cC54xcomp(iV16464), cC44(iV16464)],extension(1253 ^ 2,bind([[_417143], [iV16464]]))).
% 0.64/1.39  ncf('1.1.43.1',plain,[-(cC54xcomp(iV16464))],extension(2596 ^ 3)).
% 0.64/1.39  ncf('1.1.43.2',plain,[-(cC44(iV16464)), cC40xcomp(iV16464), cC42(iV16464)],extension(1013 ^ 3,bind([[_409275], [iV16464]]))).
% 0.64/1.39  ncf('1.1.43.2.1',plain,[-(cC40xcomp(iV16464))],extension(2584 ^ 4)).
% 0.64/1.39  ncf('1.1.43.2.2',plain,[-(cC42(iV16464)), 997 : rR1(iV16464, iV16465), 997 : cC8xcomp(iV16465)],extension(995 ^ 4,bind([[_408690, _408778], [iV16464, iV16465]]))).
% 0.64/1.39  ncf('1.1.43.2.2.1',plain,[-(rR1(iV16464, iV16465))],extension(2612 ^ 7)).
% 0.64/1.39  ncf('1.1.43.2.2.2',plain,[-(cC8xcomp(iV16465))],extension(2632 ^ 7)).
% 0.64/1.39  ncf('1.1.44',plain,[-(cC42(iV16464)), 997 : rR1(iV16464, iV16465), 997 : cC8xcomp(iV16465)],extension(995 ^ 2,bind([[_408690, _408778], [iV16464, iV16465]]))).
% 0.64/1.39  ncf('1.1.44.1',plain,[-(rR1(iV16464, iV16465))],extension(2612 ^ 5)).
% 0.64/1.39  ncf('1.1.44.2',plain,[-(cC8xcomp(iV16465))],extension(2632 ^ 5)).
% 0.64/1.39  ncf('1.1.45',plain,[-(cC44(iV16464)), cC40xcomp(iV16464), cC42(iV16464)],extension(1013 ^ 2,bind([[_409275], [iV16464]]))).
% 0.64/1.39  ncf('1.1.45.1',plain,[-(cC40xcomp(iV16464))],extension(2584 ^ 3)).
% 0.64/1.39  ncf('1.1.45.2',plain,[-(cC42(iV16464))],lemmata('[1].x')).
% 0.64/1.39  ncf('1.1.46',plain,[-(cowlThing(iV16464))],extension(2 ^ 2,bind([[_375867], [iV16464]]))).
% 0.64/1.39  ncf('1.1.47',plain,[-(cC38(iV16465)), cTOP(iV16465), cC36xcomp(iV16465)],extension(879 ^ 2,bind([[_404768], [iV16465]]))).
% 0.64/1.39  ncf('1.1.47.1',plain,[-(cTOP(iV16465))],extension(2622 ^ 3)).
% 0.64/1.39  ncf('1.1.47.2',plain,[-(cC36xcomp(iV16465))],extension(2640 ^ 3)).
% 0.64/1.39  ncf('1.1.48',plain,[-(cowlThing(iV16465))],extension(2 ^ 2,bind([[_375867], [iV16465]]))).
% 0.64/1.39  %-----------------------------------------------------
% 0.64/1.39  End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------