%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : ALG090+1 : TPTP v8.1.2. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n023.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 10:08:01 EDT 2023
% Result : Theorem 0.81s 1.37s
% Output : Proof 0.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ALG090+1 : TPTP v8.1.2. Released v2.7.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n023.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:45:44 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.81/1.37
% 0.81/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.81/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.81/1.37 %-----------------------------------------------------
% 0.81/1.37 ncf(matrix, plain, [(30 ^ _195100) ^ [] : [e0 = e1], (32 ^ _195100) ^ [] : [e0 = e2], (34 ^ _195100) ^ [] : [e0 = e3], (36 ^ _195100) ^ [] : [e0 = e4], (38 ^ _195100) ^ [] : [e1 = e2], (40 ^ _195100) ^ [] : [e1 = e3], (42 ^ _195100) ^ [] : [e1 = e4], (44 ^ _195100) ^ [] : [e2 = e3], (46 ^ _195100) ^ [] : [e2 = e4], (48 ^ _195100) ^ [] : [e3 = e4], (50 ^ _195100) ^ [] : [-(op(e0, e0) = e0)], (52 ^ _195100) ^ [] : [-(op(e0, e1) = e1)], (54 ^ _195100) ^ [] : [-(op(e0, e2) = e2)], (56 ^ _195100) ^ [] : [-(op(e0, e3) = e3)], (58 ^ _195100) ^ [] : [-(op(e0, e4) = e4)], (60 ^ _195100) ^ [] : [-(op(e1, e0) = e1)], (62 ^ _195100) ^ [] : [-(op(e1, e1) = e4)], (64 ^ _195100) ^ [] : [-(op(e1, e2) = e0)], (66 ^ _195100) ^ [] : [-(op(e1, e3) = e2)], (68 ^ _195100) ^ [] : [-(op(e1, e4) = e3)], (70 ^ _195100) ^ [] : [-(op(e2, e0) = e2)], (72 ^ _195100) ^ [] : [-(op(e2, e1) = e0)], (74 ^ _195100) ^ [] : [-(op(e2, e2) = e3)], (76 ^ _195100) ^ [] : [-(op(e2, e3) = e4)], (78 ^ _195100) ^ [] : [-(op(e2, e4) = e1)], (80 ^ _195100) ^ [] : [-(op(e3, e0) = e3)], (82 ^ _195100) ^ [] : [-(op(e3, e1) = e2)], (84 ^ _195100) ^ [] : [-(op(e3, e2) = e4)], (86 ^ _195100) ^ [] : [-(op(e3, e3) = e1)], (88 ^ _195100) ^ [] : [-(op(e3, e4) = e0)], (90 ^ _195100) ^ [] : [-(op(e4, e0) = e4)], (92 ^ _195100) ^ [] : [-(op(e4, e1) = e3)], (94 ^ _195100) ^ [] : [-(op(e4, e2) = e1)], (96 ^ _195100) ^ [] : [-(op(e4, e3) = e0)], (98 ^ _195100) ^ [] : [-(op(e4, e4) = e2)], (100 ^ _195100) ^ [] : [-(unit = e0)], (20 ^ _195100) ^ [_195856, _195858, _195860, _195862] : [-(op(_195862, _195858) = op(_195860, _195856)), _195862 = _195860, _195858 = _195856], (2 ^ _195100) ^ [_195224] : [-(_195224 = _195224)], (4 ^ _195100) ^ [_195331, _195333] : [_195333 = _195331, -(_195331 = _195333)], (10 ^ _195100) ^ [_195535, _195537, _195539] : [-(_195539 = _195535), _195539 = _195537, _195537 = _195535], (102 ^ _195100) ^ [] : [103 ^ _195100 : [(104 ^ _195100) ^ [] : [op(e0, e0) = e0], (106 ^ _195100) ^ [] : [op(e1, e1) = e0], (108 ^ _195100) ^ [] : [op(e2, e2) = e0], (110 ^ _195100) ^ [] : [op(e3, e3) = e0], (112 ^ _195100) ^ [] : [op(e4, e4) = e0]], 115 ^ _195100 : [(116 ^ _195100) ^ [] : [op(e0, e0) = e1], (118 ^ _195100) ^ [] : [op(e1, e1) = e1], (120 ^ _195100) ^ [] : [op(e2, e2) = e1], (122 ^ _195100) ^ [] : [op(e3, e3) = e1], (124 ^ _195100) ^ [] : [op(e4, e4) = e1]], 127 ^ _195100 : [(128 ^ _195100) ^ [] : [op(e0, e0) = e2], (130 ^ _195100) ^ [] : [op(e1, e1) = e2], (132 ^ _195100) ^ [] : [op(e2, e2) = e2], (134 ^ _195100) ^ [] : [op(e3, e3) = e2], (136 ^ _195100) ^ [] : [op(e4, e4) = e2]], 139 ^ _195100 : [(140 ^ _195100) ^ [] : [op(e0, e0) = e3], (142 ^ _195100) ^ [] : [op(e1, e1) = e3], (144 ^ _195100) ^ [] : [op(e2, e2) = e3], (146 ^ _195100) ^ [] : [op(e3, e3) = e3], (148 ^ _195100) ^ [] : [op(e4, e4) = e3]], 151 ^ _195100 : [(152 ^ _195100) ^ [] : [op(e0, e0) = e4], (154 ^ _195100) ^ [] : [op(e1, e1) = e4], (156 ^ _195100) ^ [] : [op(e2, e2) = e4], (158 ^ _195100) ^ [] : [op(e3, e3) = e4], (160 ^ _195100) ^ [] : [op(e4, e4) = e4]], 163 ^ _195100 : [(164 ^ _195100) ^ [] : [op(e0, e0) = e0], (166 ^ _195100) ^ [] : [op(e0, e0) = e1], (168 ^ _195100) ^ [] : [op(e0, e0) = e2], (170 ^ _195100) ^ [] : [op(e0, e0) = e3], (172 ^ _195100) ^ [] : [op(e0, e0) = e4]], 175 ^ _195100 : [(176 ^ _195100) ^ [] : [op(e0, e1) = e0], (178 ^ _195100) ^ [] : [op(e0, e1) = e1], (180 ^ _195100) ^ [] : [op(e0, e1) = e2], (182 ^ _195100) ^ [] : [op(e0, e1) = e3], (184 ^ _195100) ^ [] : [op(e0, e1) = e4]], 187 ^ _195100 : [(188 ^ _195100) ^ [] : [op(e0, e2) = e0], (190 ^ _195100) ^ [] : [op(e0, e2) = e1], (192 ^ _195100) ^ [] : [op(e0, e2) = e2], (194 ^ _195100) ^ [] : [op(e0, e2) = e3], (196 ^ _195100) ^ [] : [op(e0, e2) = e4]], 199 ^ _195100 : [(200 ^ _195100) ^ [] : [op(e0, e3) = e0], (202 ^ _195100) ^ [] : [op(e0, e3) = e1], (204 ^ _195100) ^ [] : [op(e0, e3) = e2], (206 ^ _195100) ^ [] : [op(e0, e3) = e3], (208 ^ _195100) ^ [] : [op(e0, e3) = e4]], 211 ^ _195100 : [(212 ^ _195100) ^ [] : [op(e0, e4) = e0], (214 ^ _195100) ^ [] : [op(e0, e4) = e1], (216 ^ _195100) ^ [] : [op(e0, e4) = e2], (218 ^ _195100) ^ [] : [op(e0, e4) = e3], (220 ^ _195100) ^ [] : [op(e0, e4) = e4]], 223 ^ _195100 : [(224 ^ _195100) ^ [] : [op(e1, e0) = e0], (226 ^ _195100) ^ [] : [op(e1, e0) = e1], (228 ^ _195100) ^ [] : [op(e1, e0) = e2], (230 ^ _195100) ^ [] : [op(e1, e0) = e3], (232 ^ _195100) ^ [] : [op(e1, e0) = e4]], 235 ^ _195100 : [(236 ^ _195100) ^ [] : [op(e1, e1) = e0], (238 ^ _195100) ^ [] : [op(e1, e1) = e1], (240 ^ _195100) ^ [] : [op(e1, e1) = e2], (242 ^ _195100) ^ [] : [op(e1, e1) = e3], (244 ^ _195100) ^ [] : [op(e1, e1) = e4]], 247 ^ _195100 : [(248 ^ _195100) ^ [] : [op(e1, e2) = e0], (250 ^ _195100) ^ [] : [op(e1, e2) = e1], (252 ^ _195100) ^ [] : [op(e1, e2) = e2], (254 ^ _195100) ^ [] : [op(e1, e2) = e3], (256 ^ _195100) ^ [] : [op(e1, e2) = e4]], 259 ^ _195100 : [(260 ^ _195100) ^ [] : [op(e1, e3) = e0], (262 ^ _195100) ^ [] : [op(e1, e3) = e1], (264 ^ _195100) ^ [] : [op(e1, e3) = e2], (266 ^ _195100) ^ [] : [op(e1, e3) = e3], (268 ^ _195100) ^ [] : [op(e1, e3) = e4]], 271 ^ _195100 : [(272 ^ _195100) ^ [] : [op(e1, e4) = e0], (274 ^ _195100) ^ [] : [op(e1, e4) = e1], (276 ^ _195100) ^ [] : [op(e1, e4) = e2], (278 ^ _195100) ^ [] : [op(e1, e4) = e3], (280 ^ _195100) ^ [] : [op(e1, e4) = e4]], 283 ^ _195100 : [(284 ^ _195100) ^ [] : [op(e2, e0) = e0], (286 ^ _195100) ^ [] : [op(e2, e0) = e1], (288 ^ _195100) ^ [] : [op(e2, e0) = e2], (290 ^ _195100) ^ [] : [op(e2, e0) = e3], (292 ^ _195100) ^ [] : [op(e2, e0) = e4]], 295 ^ _195100 : [(296 ^ _195100) ^ [] : [op(e2, e1) = e0], (298 ^ _195100) ^ [] : [op(e2, e1) = e1], (300 ^ _195100) ^ [] : [op(e2, e1) = e2], (302 ^ _195100) ^ [] : [op(e2, e1) = e3], (304 ^ _195100) ^ [] : [op(e2, e1) = e4]], 307 ^ _195100 : [(308 ^ _195100) ^ [] : [op(e2, e2) = e0], (310 ^ _195100) ^ [] : [op(e2, e2) = e1], (312 ^ _195100) ^ [] : [op(e2, e2) = e2], (314 ^ _195100) ^ [] : [op(e2, e2) = e3], (316 ^ _195100) ^ [] : [op(e2, e2) = e4]], 319 ^ _195100 : [(320 ^ _195100) ^ [] : [op(e2, e3) = e0], (322 ^ _195100) ^ [] : [op(e2, e3) = e1], (324 ^ _195100) ^ [] : [op(e2, e3) = e2], (326 ^ _195100) ^ [] : [op(e2, e3) = e3], (328 ^ _195100) ^ [] : [op(e2, e3) = e4]], 331 ^ _195100 : [(332 ^ _195100) ^ [] : [op(e2, e4) = e0], (334 ^ _195100) ^ [] : [op(e2, e4) = e1], (336 ^ _195100) ^ [] : [op(e2, e4) = e2], (338 ^ _195100) ^ [] : [op(e2, e4) = e3], (340 ^ _195100) ^ [] : [op(e2, e4) = e4]], 343 ^ _195100 : [(344 ^ _195100) ^ [] : [op(e3, e0) = e0], (346 ^ _195100) ^ [] : [op(e3, e0) = e1], (348 ^ _195100) ^ [] : [op(e3, e0) = e2], (350 ^ _195100) ^ [] : [op(e3, e0) = e3], (352 ^ _195100) ^ [] : [op(e3, e0) = e4]], 355 ^ _195100 : [(356 ^ _195100) ^ [] : [op(e3, e1) = e0], (358 ^ _195100) ^ [] : [op(e3, e1) = e1], (360 ^ _195100) ^ [] : [op(e3, e1) = e2], (362 ^ _195100) ^ [] : [op(e3, e1) = e3], (364 ^ _195100) ^ [] : [op(e3, e1) = e4]], 367 ^ _195100 : [(368 ^ _195100) ^ [] : [op(e3, e2) = e0], (370 ^ _195100) ^ [] : [op(e3, e2) = e1], (372 ^ _195100) ^ [] : [op(e3, e2) = e2], (374 ^ _195100) ^ [] : [op(e3, e2) = e3], (376 ^ _195100) ^ [] : [op(e3, e2) = e4]], 379 ^ _195100 : [(380 ^ _195100) ^ [] : [op(e3, e3) = e0], (382 ^ _195100) ^ [] : [op(e3, e3) = e1], (384 ^ _195100) ^ [] : [op(e3, e3) = e2], (386 ^ _195100) ^ [] : [op(e3, e3) = e3], (388 ^ _195100) ^ [] : [op(e3, e3) = e4]], 391 ^ _195100 : [(392 ^ _195100) ^ [] : [op(e3, e4) = e0], (394 ^ _195100) ^ [] : [op(e3, e4) = e1], (396 ^ _195100) ^ [] : [op(e3, e4) = e2], (398 ^ _195100) ^ [] : [op(e3, e4) = e3], (400 ^ _195100) ^ [] : [op(e3, e4) = e4]], 403 ^ _195100 : [(404 ^ _195100) ^ [] : [op(e4, e0) = e0], (406 ^ _195100) ^ [] : [op(e4, e0) = e1], (408 ^ _195100) ^ [] : [op(e4, e0) = e2], (410 ^ _195100) ^ [] : [op(e4, e0) = e3], (412 ^ _195100) ^ [] : [op(e4, e0) = e4]], 415 ^ _195100 : [(416 ^ _195100) ^ [] : [op(e4, e1) = e0], (418 ^ _195100) ^ [] : [op(e4, e1) = e1], (420 ^ _195100) ^ [] : [op(e4, e1) = e2], (422 ^ _195100) ^ [] : [op(e4, e1) = e3], (424 ^ _195100) ^ [] : [op(e4, e1) = e4]], 427 ^ _195100 : [(428 ^ _195100) ^ [] : [op(e4, e2) = e0], (430 ^ _195100) ^ [] : [op(e4, e2) = e1], (432 ^ _195100) ^ [] : [op(e4, e2) = e2], (434 ^ _195100) ^ [] : [op(e4, e2) = e3], (436 ^ _195100) ^ [] : [op(e4, e2) = e4]], 439 ^ _195100 : [(440 ^ _195100) ^ [] : [op(e4, e3) = e0], (442 ^ _195100) ^ [] : [op(e4, e3) = e1], (444 ^ _195100) ^ [] : [op(e4, e3) = e2], (446 ^ _195100) ^ [] : [op(e4, e3) = e3], (448 ^ _195100) ^ [] : [op(e4, e3) = e4]], 451 ^ _195100 : [(452 ^ _195100) ^ [] : [op(e4, e4) = e0], (454 ^ _195100) ^ [] : [op(e4, e4) = e1], (456 ^ _195100) ^ [] : [op(e4, e4) = e2], (458 ^ _195100) ^ [] : [op(e4, e4) = e3], (460 ^ _195100) ^ [] : [op(e4, e4) = e4]], op(unit, e0) = e0, op(e0, unit) = e0, op(unit, e1) = e1, op(e1, unit) = e1, op(unit, e2) = e2, op(e2, unit) = e2, op(unit, e3) = e3, op(e3, unit) = e3, op(unit, e4) = e4, op(e4, unit) = e4, 503 ^ _195100 : [(504 ^ _195100) ^ [] : [unit = e0], (506 ^ _195100) ^ [] : [unit = e1], (508 ^ _195100) ^ [] : [unit = e2], (510 ^ _195100) ^ [] : [unit = e3], (512 ^ _195100) ^ [] : [unit = e4]], 515 ^ _195100 : [(516 ^ _195100) ^ [] : [op(e0, e0) = e0], (518 ^ _195100) ^ [] : [op(e0, e1) = e0], (520 ^ _195100) ^ [] : [op(e0, e2) = e0], (522 ^ _195100) ^ [] : [op(e0, e3) = e0], (524 ^ _195100) ^ [] : [op(e0, e4) = e0]], 527 ^ _195100 : [(528 ^ _195100) ^ [] : [op(e0, e0) = e0], (530 ^ _195100) ^ [] : [op(e1, e0) = e0], (532 ^ _195100) ^ [] : [op(e2, e0) = e0], (534 ^ _195100) ^ [] : [op(e3, e0) = e0], (536 ^ _195100) ^ [] : [op(e4, e0) = e0]], 539 ^ _195100 : [(540 ^ _195100) ^ [] : [op(e0, e0) = e1], (542 ^ _195100) ^ [] : [op(e0, e1) = e1], (544 ^ _195100) ^ [] : [op(e0, e2) = e1], (546 ^ _195100) ^ [] : [op(e0, e3) = e1], (548 ^ _195100) ^ [] : [op(e0, e4) = e1]], 551 ^ _195100 : [(552 ^ _195100) ^ [] : [op(e0, e0) = e1], (554 ^ _195100) ^ [] : [op(e1, e0) = e1], (556 ^ _195100) ^ [] : [op(e2, e0) = e1], (558 ^ _195100) ^ [] : [op(e3, e0) = e1], (560 ^ _195100) ^ [] : [op(e4, e0) = e1]], 563 ^ _195100 : [(564 ^ _195100) ^ [] : [op(e0, e0) = e2], (566 ^ _195100) ^ [] : [op(e0, e1) = e2], (568 ^ _195100) ^ [] : [op(e0, e2) = e2], (570 ^ _195100) ^ [] : [op(e0, e3) = e2], (572 ^ _195100) ^ [] : [op(e0, e4) = e2]], 575 ^ _195100 : [(576 ^ _195100) ^ [] : [op(e0, e0) = e2], (578 ^ _195100) ^ [] : [op(e1, e0) = e2], (580 ^ _195100) ^ [] : [op(e2, e0) = e2], (582 ^ _195100) ^ [] : [op(e3, e0) = e2], (584 ^ _195100) ^ [] : [op(e4, e0) = e2]], 587 ^ _195100 : [(588 ^ _195100) ^ [] : [op(e0, e0) = e3], (590 ^ _195100) ^ [] : [op(e0, e1) = e3], (592 ^ _195100) ^ [] : [op(e0, e2) = e3], (594 ^ _195100) ^ [] : [op(e0, e3) = e3], (596 ^ _195100) ^ [] : [op(e0, e4) = e3]], 599 ^ _195100 : [(600 ^ _195100) ^ [] : [op(e0, e0) = e3], (602 ^ _195100) ^ [] : [op(e1, e0) = e3], (604 ^ _195100) ^ [] : [op(e2, e0) = e3], (606 ^ _195100) ^ [] : [op(e3, e0) = e3], (608 ^ _195100) ^ [] : [op(e4, e0) = e3]], 611 ^ _195100 : [(612 ^ _195100) ^ [] : [op(e0, e0) = e4], (614 ^ _195100) ^ [] : [op(e0, e1) = e4], (616 ^ _195100) ^ [] : [op(e0, e2) = e4], (618 ^ _195100) ^ [] : [op(e0, e3) = e4], (620 ^ _195100) ^ [] : [op(e0, e4) = e4]], 623 ^ _195100 : [(624 ^ _195100) ^ [] : [op(e0, e0) = e4], (626 ^ _195100) ^ [] : [op(e1, e0) = e4], (628 ^ _195100) ^ [] : [op(e2, e0) = e4], (630 ^ _195100) ^ [] : [op(e3, e0) = e4], (632 ^ _195100) ^ [] : [op(e4, e0) = e4]], 635 ^ _195100 : [(636 ^ _195100) ^ [] : [op(e1, e0) = e0], (638 ^ _195100) ^ [] : [op(e1, e1) = e0], (640 ^ _195100) ^ [] : [op(e1, e2) = e0], (642 ^ _195100) ^ [] : [op(e1, e3) = e0], (644 ^ _195100) ^ [] : [op(e1, e4) = e0]], 647 ^ _195100 : [(648 ^ _195100) ^ [] : [op(e0, e1) = e0], (650 ^ _195100) ^ [] : [op(e1, e1) = e0], (652 ^ _195100) ^ [] : [op(e2, e1) = e0], (654 ^ _195100) ^ [] : [op(e3, e1) = e0], (656 ^ _195100) ^ [] : [op(e4, e1) = e0]], 659 ^ _195100 : [(660 ^ _195100) ^ [] : [op(e1, e0) = e1], (662 ^ _195100) ^ [] : [op(e1, e1) = e1], (664 ^ _195100) ^ [] : [op(e1, e2) = e1], (666 ^ _195100) ^ [] : [op(e1, e3) = e1], (668 ^ _195100) ^ [] : [op(e1, e4) = e1]], 671 ^ _195100 : [(672 ^ _195100) ^ [] : [op(e0, e1) = e1], (674 ^ _195100) ^ [] : [op(e1, e1) = e1], (676 ^ _195100) ^ [] : [op(e2, e1) = e1], (678 ^ _195100) ^ [] : [op(e3, e1) = e1], (680 ^ _195100) ^ [] : [op(e4, e1) = e1]], 683 ^ _195100 : [(684 ^ _195100) ^ [] : [op(e1, e0) = e2], (686 ^ _195100) ^ [] : [op(e1, e1) = e2], (688 ^ _195100) ^ [] : [op(e1, e2) = e2], (690 ^ _195100) ^ [] : [op(e1, e3) = e2], (692 ^ _195100) ^ [] : [op(e1, e4) = e2]], 695 ^ _195100 : [(696 ^ _195100) ^ [] : [op(e0, e1) = e2], (698 ^ _195100) ^ [] : [op(e1, e1) = e2], (700 ^ _195100) ^ [] : [op(e2, e1) = e2], (702 ^ _195100) ^ [] : [op(e3, e1) = e2], (704 ^ _195100) ^ [] : [op(e4, e1) = e2]], 707 ^ _195100 : [(708 ^ _195100) ^ [] : [op(e1, e0) = e3], (710 ^ _195100) ^ [] : [op(e1, e1) = e3], (712 ^ _195100) ^ [] : [op(e1, e2) = e3], (714 ^ _195100) ^ [] : [op(e1, e3) = e3], (716 ^ _195100) ^ [] : [op(e1, e4) = e3]], 719 ^ _195100 : [(720 ^ _195100) ^ [] : [op(e0, e1) = e3], (722 ^ _195100) ^ [] : [op(e1, e1) = e3], (724 ^ _195100) ^ [] : [op(e2, e1) = e3], (726 ^ _195100) ^ [] : [op(e3, e1) = e3], (728 ^ _195100) ^ [] : [op(e4, e1) = e3]], 731 ^ _195100 : [(732 ^ _195100) ^ [] : [op(e1, e0) = e4], (734 ^ _195100) ^ [] : [op(e1, e1) = e4], (736 ^ _195100) ^ [] : [op(e1, e2) = e4], (738 ^ _195100) ^ [] : [op(e1, e3) = e4], (740 ^ _195100) ^ [] : [op(e1, e4) = e4]], 743 ^ _195100 : [(744 ^ _195100) ^ [] : [op(e0, e1) = e4], (746 ^ _195100) ^ [] : [op(e1, e1) = e4], (748 ^ _195100) ^ [] : [op(e2, e1) = e4], (750 ^ _195100) ^ [] : [op(e3, e1) = e4], (752 ^ _195100) ^ [] : [op(e4, e1) = e4]], 755 ^ _195100 : [(756 ^ _195100) ^ [] : [op(e2, e0) = e0], (758 ^ _195100) ^ [] : [op(e2, e1) = e0], (760 ^ _195100) ^ [] : [op(e2, e2) = e0], (762 ^ _195100) ^ [] : [op(e2, e3) = e0], (764 ^ _195100) ^ [] : [op(e2, e4) = e0]], 767 ^ _195100 : [(768 ^ _195100) ^ [] : [op(e0, e2) = e0], (770 ^ _195100) ^ [] : [op(e1, e2) = e0], (772 ^ _195100) ^ [] : [op(e2, e2) = e0], (774 ^ _195100) ^ [] : [op(e3, e2) = e0], (776 ^ _195100) ^ [] : [op(e4, e2) = e0]], 779 ^ _195100 : [(780 ^ _195100) ^ [] : [op(e2, e0) = e1], (782 ^ _195100) ^ [] : [op(e2, e1) = e1], (784 ^ _195100) ^ [] : [op(e2, e2) = e1], (786 ^ _195100) ^ [] : [op(e2, e3) = e1], (788 ^ _195100) ^ [] : [op(e2, e4) = e1]], 791 ^ _195100 : [(792 ^ _195100) ^ [] : [op(e0, e2) = e1], (794 ^ _195100) ^ [] : [op(e1, e2) = e1], (796 ^ _195100) ^ [] : [op(e2, e2) = e1], (798 ^ _195100) ^ [] : [op(e3, e2) = e1], (800 ^ _195100) ^ [] : [op(e4, e2) = e1]], 803 ^ _195100 : [(804 ^ _195100) ^ [] : [op(e2, e0) = e2], (806 ^ _195100) ^ [] : [op(e2, e1) = e2], (808 ^ _195100) ^ [] : [op(e2, e2) = e2], (810 ^ _195100) ^ [] : [op(e2, e3) = e2], (812 ^ _195100) ^ [] : [op(e2, e4) = e2]], 815 ^ _195100 : [(816 ^ _195100) ^ [] : [op(e0, e2) = e2], (818 ^ _195100) ^ [] : [op(e1, e2) = e2], (820 ^ _195100) ^ [] : [op(e2, e2) = e2], (822 ^ _195100) ^ [] : [op(e3, e2) = e2], (824 ^ _195100) ^ [] : [op(e4, e2) = e2]], 827 ^ _195100 : [(828 ^ _195100) ^ [] : [op(e2, e0) = e3], (830 ^ _195100) ^ [] : [op(e2, e1) = e3], (832 ^ _195100) ^ [] : [op(e2, e2) = e3], (834 ^ _195100) ^ [] : [op(e2, e3) = e3], (836 ^ _195100) ^ [] : [op(e2, e4) = e3]], 839 ^ _195100 : [(840 ^ _195100) ^ [] : [op(e0, e2) = e3], (842 ^ _195100) ^ [] : [op(e1, e2) = e3], (844 ^ _195100) ^ [] : [op(e2, e2) = e3], (846 ^ _195100) ^ [] : [op(e3, e2) = e3], (848 ^ _195100) ^ [] : [op(e4, e2) = e3]], 851 ^ _195100 : [(852 ^ _195100) ^ [] : [op(e2, e0) = e4], (854 ^ _195100) ^ [] : [op(e2, e1) = e4], (856 ^ _195100) ^ [] : [op(e2, e2) = e4], (858 ^ _195100) ^ [] : [op(e2, e3) = e4], (860 ^ _195100) ^ [] : [op(e2, e4) = e4]], 863 ^ _195100 : [(864 ^ _195100) ^ [] : [op(e0, e2) = e4], (866 ^ _195100) ^ [] : [op(e1, e2) = e4], (868 ^ _195100) ^ [] : [op(e2, e2) = e4], (870 ^ _195100) ^ [] : [op(e3, e2) = e4], (872 ^ _195100) ^ [] : [op(e4, e2) = e4]], 875 ^ _195100 : [(876 ^ _195100) ^ [] : [op(e3, e0) = e0], (878 ^ _195100) ^ [] : [op(e3, e1) = e0], (880 ^ _195100) ^ [] : [op(e3, e2) = e0], (882 ^ _195100) ^ [] : [op(e3, e3) = e0], (884 ^ _195100) ^ [] : [op(e3, e4) = e0]], 887 ^ _195100 : [(888 ^ _195100) ^ [] : [op(e0, e3) = e0], (890 ^ _195100) ^ [] : [op(e1, e3) = e0], (892 ^ _195100) ^ [] : [op(e2, e3) = e0], (894 ^ _195100) ^ [] : [op(e3, e3) = e0], (896 ^ _195100) ^ [] : [op(e4, e3) = e0]], 899 ^ _195100 : [(900 ^ _195100) ^ [] : [op(e3, e0) = e1], (902 ^ _195100) ^ [] : [op(e3, e1) = e1], (904 ^ _195100) ^ [] : [op(e3, e2) = e1], (906 ^ _195100) ^ [] : [op(e3, e3) = e1], (908 ^ _195100) ^ [] : [op(e3, e4) = e1]], 911 ^ _195100 : [(912 ^ _195100) ^ [] : [op(e0, e3) = e1], (914 ^ _195100) ^ [] : [op(e1, e3) = e1], (916 ^ _195100) ^ [] : [op(e2, e3) = e1], (918 ^ _195100) ^ [] : [op(e3, e3) = e1], (920 ^ _195100) ^ [] : [op(e4, e3) = e1]], 923 ^ _195100 : [(924 ^ _195100) ^ [] : [op(e3, e0) = e2], (926 ^ _195100) ^ [] : [op(e3, e1) = e2], (928 ^ _195100) ^ [] : [op(e3, e2) = e2], (930 ^ _195100) ^ [] : [op(e3, e3) = e2], (932 ^ _195100) ^ [] : [op(e3, e4) = e2]], 935 ^ _195100 : [(936 ^ _195100) ^ [] : [op(e0, e3) = e2], (938 ^ _195100) ^ [] : [op(e1, e3) = e2], (940 ^ _195100) ^ [] : [op(e2, e3) = e2], (942 ^ _195100) ^ [] : [op(e3, e3) = e2], (944 ^ _195100) ^ [] : [op(e4, e3) = e2]], 947 ^ _195100 : [(948 ^ _195100) ^ [] : [op(e3, e0) = e3], (950 ^ _195100) ^ [] : [op(e3, e1) = e3], (952 ^ _195100) ^ [] : [op(e3, e2) = e3], (954 ^ _195100) ^ [] : [op(e3, e3) = e3], (956 ^ _195100) ^ [] : [op(e3, e4) = e3]], 959 ^ _195100 : [(960 ^ _195100) ^ [] : [op(e0, e3) = e3], (962 ^ _195100) ^ [] : [op(e1, e3) = e3], (964 ^ _195100) ^ [] : [op(e2, e3) = e3], (966 ^ _195100) ^ [] : [op(e3, e3) = e3], (968 ^ _195100) ^ [] : [op(e4, e3) = e3]], 971 ^ _195100 : [(972 ^ _195100) ^ [] : [op(e3, e0) = e4], (974 ^ _195100) ^ [] : [op(e3, e1) = e4], (976 ^ _195100) ^ [] : [op(e3, e2) = e4], (978 ^ _195100) ^ [] : [op(e3, e3) = e4], (980 ^ _195100) ^ [] : [op(e3, e4) = e4]], 983 ^ _195100 : [(984 ^ _195100) ^ [] : [op(e0, e3) = e4], (986 ^ _195100) ^ [] : [op(e1, e3) = e4], (988 ^ _195100) ^ [] : [op(e2, e3) = e4], (990 ^ _195100) ^ [] : [op(e3, e3) = e4], (992 ^ _195100) ^ [] : [op(e4, e3) = e4]], 995 ^ _195100 : [(996 ^ _195100) ^ [] : [op(e4, e0) = e0], (998 ^ _195100) ^ [] : [op(e4, e1) = e0], (1000 ^ _195100) ^ [] : [op(e4, e2) = e0], (1002 ^ _195100) ^ [] : [op(e4, e3) = e0], (1004 ^ _195100) ^ [] : [op(e4, e4) = e0]], 1007 ^ _195100 : [(1008 ^ _195100) ^ [] : [op(e0, e4) = e0], (1010 ^ _195100) ^ [] : [op(e1, e4) = e0], (1012 ^ _195100) ^ [] : [op(e2, e4) = e0], (1014 ^ _195100) ^ [] : [op(e3, e4) = e0], (1016 ^ _195100) ^ [] : [op(e4, e4) = e0]], 1019 ^ _195100 : [(1020 ^ _195100) ^ [] : [op(e4, e0) = e1], (1022 ^ _195100) ^ [] : [op(e4, e1) = e1], (1024 ^ _195100) ^ [] : [op(e4, e2) = e1], (1026 ^ _195100) ^ [] : [op(e4, e3) = e1], (1028 ^ _195100) ^ [] : [op(e4, e4) = e1]], 1031 ^ _195100 : [(1032 ^ _195100) ^ [] : [op(e0, e4) = e1], (1034 ^ _195100) ^ [] : [op(e1, e4) = e1], (1036 ^ _195100) ^ [] : [op(e2, e4) = e1], (1038 ^ _195100) ^ [] : [op(e3, e4) = e1], (1040 ^ _195100) ^ [] : [op(e4, e4) = e1]], 1043 ^ _195100 : [(1044 ^ _195100) ^ [] : [op(e4, e0) = e2], (1046 ^ _195100) ^ [] : [op(e4, e1) = e2], (1048 ^ _195100) ^ [] : [op(e4, e2) = e2], (1050 ^ _195100) ^ [] : [op(e4, e3) = e2], (1052 ^ _195100) ^ [] : [op(e4, e4) = e2]], 1055 ^ _195100 : [(1056 ^ _195100) ^ [] : [op(e0, e4) = e2], (1058 ^ _195100) ^ [] : [op(e1, e4) = e2], (1060 ^ _195100) ^ [] : [op(e2, e4) = e2], (1062 ^ _195100) ^ [] : [op(e3, e4) = e2], (1064 ^ _195100) ^ [] : [op(e4, e4) = e2]], 1067 ^ _195100 : [(1068 ^ _195100) ^ [] : [op(e4, e0) = e3], (1070 ^ _195100) ^ [] : [op(e4, e1) = e3], (1072 ^ _195100) ^ [] : [op(e4, e2) = e3], (1074 ^ _195100) ^ [] : [op(e4, e3) = e3], (1076 ^ _195100) ^ [] : [op(e4, e4) = e3]], 1079 ^ _195100 : [(1080 ^ _195100) ^ [] : [op(e0, e4) = e3], (1082 ^ _195100) ^ [] : [op(e1, e4) = e3], (1084 ^ _195100) ^ [] : [op(e2, e4) = e3], (1086 ^ _195100) ^ [] : [op(e3, e4) = e3], (1088 ^ _195100) ^ [] : [op(e4, e4) = e3]], 1091 ^ _195100 : [(1092 ^ _195100) ^ [] : [op(e4, e0) = e4], (1094 ^ _195100) ^ [] : [op(e4, e1) = e4], (1096 ^ _195100) ^ [] : [op(e4, e2) = e4], (1098 ^ _195100) ^ [] : [op(e4, e3) = e4], (1100 ^ _195100) ^ [] : [op(e4, e4) = e4]], 1101 ^ _195100 : [(1102 ^ _195100) ^ [] : [op(e0, e4) = e4], (1104 ^ _195100) ^ [] : [op(e1, e4) = e4], (1106 ^ _195100) ^ [] : [op(e2, e4) = e4], (1108 ^ _195100) ^ [] : [op(e3, e4) = e4], (1110 ^ _195100) ^ [] : [op(e4, e4) = e4]]]], input).
% 0.81/1.37 ncf('1',plain,[104 : op(e0, e0) = e0, 122 : op(e3, e3) = e1, 136 : op(e4, e4) = e2, 144 : op(e2, e2) = e3, 154 : op(e1, e1) = e4, 164 : op(e0, e0) = e0, 178 : op(e0, e1) = e1, 192 : op(e0, e2) = e2, 206 : op(e0, e3) = e3, 220 : op(e0, e4) = e4, 226 : op(e1, e0) = e1, 244 : op(e1, e1) = e4, 248 : op(e1, e2) = e0, 264 : op(e1, e3) = e2, 278 : op(e1, e4) = e3, 288 : op(e2, e0) = e2, 296 : op(e2, e1) = e0, 314 : op(e2, e2) = e3, 328 : op(e2, e3) = e4, 334 : op(e2, e4) = e1, 350 : op(e3, e0) = e3, 360 : op(e3, e1) = e2, 376 : op(e3, e2) = e4, 382 : op(e3, e3) = e1, 392 : op(e3, e4) = e0, 412 : op(e4, e0) = e4, 422 : op(e4, e1) = e3, 430 : op(e4, e2) = e1, 440 : op(e4, e3) = e0, 456 : op(e4, e4) = e2, 456 : op(unit, e0) = e0, 456 : op(e0, unit) = e0, 456 : op(unit, e1) = e1, 456 : op(e1, unit) = e1, 456 : op(unit, e2) = e2, 456 : op(e2, unit) = e2, 456 : op(unit, e3) = e3, 456 : op(e3, unit) = e3, 456 : op(unit, e4) = e4, 456 : op(e4, unit) = e4, 504 : unit = e0, 516 : op(e0, e0) = e0, 528 : op(e0, e0) = e0, 542 : op(e0, e1) = e1, 554 : op(e1, e0) = e1, 568 : op(e0, e2) = e2, 580 : op(e2, e0) = e2, 594 : op(e0, e3) = e3, 606 : op(e3, e0) = e3, 620 : op(e0, e4) = e4, 632 : op(e4, e0) = e4, 640 : op(e1, e2) = e0, 652 : op(e2, e1) = e0, 660 : op(e1, e0) = e1, 672 : op(e0, e1) = e1, 690 : op(e1, e3) = e2, 702 : op(e3, e1) = e2, 716 : op(e1, e4) = e3, 728 : op(e4, e1) = e3, 734 : op(e1, e1) = e4, 746 : op(e1, e1) = e4, 758 : op(e2, e1) = e0, 770 : op(e1, e2) = e0, 788 : op(e2, e4) = e1, 800 : op(e4, e2) = e1, 804 : op(e2, e0) = e2, 816 : op(e0, e2) = e2, 832 : op(e2, e2) = e3, 844 : op(e2, e2) = e3, 858 : op(e2, e3) = e4, 870 : op(e3, e2) = e4, 884 : op(e3, e4) = e0, 896 : op(e4, e3) = e0, 906 : op(e3, e3) = e1, 918 : op(e3, e3) = e1, 926 : op(e3, e1) = e2, 938 : op(e1, e3) = e2, 948 : op(e3, e0) = e3, 960 : op(e0, e3) = e3, 976 : op(e3, e2) = e4, 988 : op(e2, e3) = e4, 1002 : op(e4, e3) = e0, 1014 : op(e3, e4) = e0, 1024 : op(e4, e2) = e1, 1036 : op(e2, e4) = e1, 1052 : op(e4, e4) = e2, 1064 : op(e4, e4) = e2, 1070 : op(e4, e1) = e3, 1082 : op(e1, e4) = e3, 1092 : op(e4, e0) = e4, 1102 : op(e0, e4) = e4],start(102 ^ 0)).
% 0.81/1.37 ncf('1.1',plain,[-(op(e0, e0) = e0)],extension(50 ^ 3)).
% 0.81/1.37 ncf('1.2',plain,[-(op(e3, e3) = e1)],extension(86 ^ 3)).
% 0.81/1.37 ncf('1.3',plain,[-(op(e4, e4) = e2)],extension(98 ^ 3)).
% 0.81/1.37 ncf('1.4',plain,[-(op(e2, e2) = e3)],extension(74 ^ 3)).
% 0.81/1.37 ncf('1.5',plain,[-(op(e1, e1) = e4)],extension(62 ^ 3)).
% 0.81/1.37 ncf('1.6',plain,[-(op(e0, e0) = e0)],extension(50 ^ 3)).
% 0.81/1.37 ncf('1.7',plain,[-(op(e0, e1) = e1)],extension(52 ^ 3)).
% 0.81/1.37 ncf('1.8',plain,[-(op(e0, e2) = e2)],extension(54 ^ 3)).
% 0.81/1.37 ncf('1.9',plain,[-(op(e0, e3) = e3)],extension(56 ^ 3)).
% 0.81/1.37 ncf('1.10',plain,[-(op(e0, e4) = e4)],extension(58 ^ 3)).
% 0.81/1.37 ncf('1.11',plain,[-(op(e1, e0) = e1)],extension(60 ^ 3)).
% 0.81/1.37 ncf('1.12',plain,[-(op(e1, e1) = e4)],extension(62 ^ 3)).
% 0.81/1.37 ncf('1.13',plain,[-(op(e1, e2) = e0)],extension(64 ^ 3)).
% 0.81/1.37 ncf('1.14',plain,[-(op(e1, e3) = e2)],extension(66 ^ 3)).
% 0.81/1.37 ncf('1.15',plain,[-(op(e1, e4) = e3)],extension(68 ^ 3)).
% 0.81/1.37 ncf('1.16',plain,[-(op(e2, e0) = e2)],extension(70 ^ 3)).
% 0.81/1.37 ncf('1.17',plain,[-(op(e2, e1) = e0)],extension(72 ^ 3)).
% 0.81/1.37 ncf('1.18',plain,[-(op(e2, e2) = e3)],extension(74 ^ 3)).
% 0.81/1.37 ncf('1.19',plain,[-(op(e2, e3) = e4)],extension(76 ^ 3)).
% 0.81/1.37 ncf('1.20',plain,[-(op(e2, e4) = e1)],extension(78 ^ 3)).
% 0.81/1.37 ncf('1.21',plain,[-(op(e3, e0) = e3)],extension(80 ^ 3)).
% 0.81/1.37 ncf('1.22',plain,[-(op(e3, e1) = e2)],extension(82 ^ 3)).
% 0.81/1.37 ncf('1.23',plain,[-(op(e3, e2) = e4)],extension(84 ^ 3)).
% 0.81/1.37 ncf('1.24',plain,[-(op(e3, e3) = e1)],extension(86 ^ 3)).
% 0.81/1.37 ncf('1.25',plain,[-(op(e3, e4) = e0)],extension(88 ^ 3)).
% 0.81/1.37 ncf('1.26',plain,[-(op(e4, e0) = e4)],extension(90 ^ 3)).
% 0.81/1.37 ncf('1.27',plain,[-(op(e4, e1) = e3)],extension(92 ^ 3)).
% 0.81/1.37 ncf('1.28',plain,[-(op(e4, e2) = e1)],extension(94 ^ 3)).
% 0.81/1.37 ncf('1.29',plain,[-(op(e4, e3) = e0)],extension(96 ^ 3)).
% 0.81/1.37 ncf('1.30',plain,[-(op(e4, e4) = e2)],extension(98 ^ 3)).
% 0.81/1.37 ncf('1.31',plain,[-(op(unit, e0) = e0), op(unit, e0) = op(e0, e0), op(e0, e0) = e0],extension(10 ^ 1,bind([[_195535, _195537, _195539], [e0, op(e0, e0), op(unit, e0)]]))).
% 0.81/1.37 ncf('1.31.1',plain,[-(op(unit, e0) = op(e0, e0)), unit = e0, e0 = e0],extension(20 ^ 2,bind([[_195856, _195858, _195860, _195862], [e0, e0, e0, unit]]))).
% 0.81/1.37 ncf('1.31.1.1',plain,[-(unit = e0)],extension(100 ^ 3)).
% 0.81/1.37 ncf('1.31.1.2',plain,[-(e0 = e0)],extension(2 ^ 3,bind([[_195224], [e0]]))).
% 0.81/1.37 ncf('1.31.2',plain,[-(op(e0, e0) = e0)],extension(50 ^ 2)).
% 0.81/1.37 ncf('1.32',plain,[-(op(e0, unit) = e0), op(e0, unit) = op(e0, e0), op(e0, e0) = e0],extension(10 ^ 1,bind([[_195535, _195537, _195539], [e0, op(e0, e0), op(e0, unit)]]))).
% 0.81/1.37 ncf('1.32.1',plain,[-(op(e0, unit) = op(e0, e0)), e0 = e0, unit = e0],extension(20 ^ 2,bind([[_195856, _195858, _195860, _195862], [e0, unit, e0, e0]]))).
% 0.81/1.37 ncf('1.32.1.1',plain,[-(e0 = e0)],extension(2 ^ 3,bind([[_195224], [e0]]))).
% 0.81/1.37 ncf('1.32.1.2',plain,[-(unit = e0)],extension(100 ^ 3)).
% 0.81/1.37 ncf('1.32.2',plain,[-(op(e0, e0) = e0)],extension(50 ^ 2)).
% 0.81/1.37 ncf('1.33',plain,[-(op(unit, e1) = e1), op(unit, e1) = op(e0, e1), op(e0, e1) = e1],extension(10 ^ 1,bind([[_195535, _195537, _195539], [e1, op(e0, e1), op(unit, e1)]]))).
% 0.81/1.37 ncf('1.33.1',plain,[-(op(unit, e1) = op(e0, e1)), unit = e0, e1 = e1],extension(20 ^ 2,bind([[_195856, _195858, _195860, _195862], [e1, e1, e0, unit]]))).
% 0.81/1.37 ncf('1.33.1.1',plain,[-(unit = e0)],extension(100 ^ 3)).
% 0.81/1.37 ncf('1.33.1.2',plain,[-(e1 = e1)],extension(2 ^ 3,bind([[_195224], [e1]]))).
% 0.81/1.37 ncf('1.33.2',plain,[-(op(e0, e1) = e1)],extension(52 ^ 2)).
% 0.81/1.37 ncf('1.34',plain,[-(op(e1, unit) = e1), op(e1, unit) = op(e1, e0), op(e1, e0) = e1],extension(10 ^ 1,bind([[_195535, _195537, _195539], [e1, op(e1, e0), op(e1, unit)]]))).
% 0.81/1.37 ncf('1.34.1',plain,[-(op(e1, unit) = op(e1, e0)), e1 = e1, unit = e0],extension(20 ^ 2,bind([[_195856, _195858, _195860, _195862], [e0, unit, e1, e1]]))).
% 0.81/1.37 ncf('1.34.1.1',plain,[-(e1 = e1)],extension(2 ^ 3,bind([[_195224], [e1]]))).
% 0.81/1.37 ncf('1.34.1.2',plain,[-(unit = e0)],extension(100 ^ 3)).
% 0.81/1.37 ncf('1.34.2',plain,[-(op(e1, e0) = e1)],extension(60 ^ 2)).
% 0.81/1.37 ncf('1.35',plain,[-(op(unit, e2) = e2), op(unit, e2) = op(e0, e2), op(e0, e2) = e2],extension(10 ^ 1,bind([[_195535, _195537, _195539], [e2, op(e0, e2), op(unit, e2)]]))).
% 0.81/1.37 ncf('1.35.1',plain,[-(op(unit, e2) = op(e0, e2)), unit = e0, e2 = e2],extension(20 ^ 2,bind([[_195856, _195858, _195860, _195862], [e2, e2, e0, unit]]))).
% 0.81/1.37 ncf('1.35.1.1',plain,[-(unit = e0)],extension(100 ^ 3)).
% 0.81/1.37 ncf('1.35.1.2',plain,[-(e2 = e2)],extension(2 ^ 3,bind([[_195224], [e2]]))).
% 0.81/1.37 ncf('1.35.2',plain,[-(op(e0, e2) = e2)],extension(54 ^ 2)).
% 0.81/1.37 ncf('1.36',plain,[-(op(e2, unit) = e2), op(e2, unit) = op(e2, e0), op(e2, e0) = e2],extension(10 ^ 1,bind([[_195535, _195537, _195539], [e2, op(e2, e0), op(e2, unit)]]))).
% 0.81/1.37 ncf('1.36.1',plain,[-(op(e2, unit) = op(e2, e0)), e2 = e2, unit = e0],extension(20 ^ 2,bind([[_195856, _195858, _195860, _195862], [e0, unit, e2, e2]]))).
% 0.81/1.37 ncf('1.36.1.1',plain,[-(e2 = e2)],extension(2 ^ 3,bind([[_195224], [e2]]))).
% 0.81/1.37 ncf('1.36.1.2',plain,[-(unit = e0)],extension(100 ^ 3)).
% 0.81/1.37 ncf('1.36.2',plain,[-(op(e2, e0) = e2)],extension(70 ^ 2)).
% 0.81/1.37 ncf('1.37',plain,[-(op(unit, e3) = e3), op(unit, e3) = op(e0, e3), op(e0, e3) = e3],extension(10 ^ 1,bind([[_195535, _195537, _195539], [e3, op(e0, e3), op(unit, e3)]]))).
% 0.81/1.37 ncf('1.37.1',plain,[-(op(unit, e3) = op(e0, e3)), unit = e0, e3 = e3],extension(20 ^ 2,bind([[_195856, _195858, _195860, _195862], [e3, e3, e0, unit]]))).
% 0.81/1.37 ncf('1.37.1.1',plain,[-(unit = e0)],extension(100 ^ 3)).
% 0.81/1.37 ncf('1.37.1.2',plain,[-(e3 = e3)],extension(2 ^ 3,bind([[_195224], [e3]]))).
% 0.81/1.37 ncf('1.37.2',plain,[-(op(e0, e3) = e3)],extension(56 ^ 2)).
% 0.81/1.37 ncf('1.38',plain,[-(op(e3, unit) = e3), op(e3, unit) = op(e3, e0), op(e3, e0) = e3],extension(10 ^ 1,bind([[_195535, _195537, _195539], [e3, op(e3, e0), op(e3, unit)]]))).
% 0.81/1.37 ncf('1.38.1',plain,[-(op(e3, unit) = op(e3, e0)), e3 = e3, unit = e0],extension(20 ^ 2,bind([[_195856, _195858, _195860, _195862], [e0, unit, e3, e3]]))).
% 0.81/1.37 ncf('1.38.1.1',plain,[-(e3 = e3)],extension(2 ^ 3,bind([[_195224], [e3]]))).
% 0.81/1.37 ncf('1.38.1.2',plain,[-(unit = e0)],extension(100 ^ 3)).
% 0.81/1.37 ncf('1.38.2',plain,[-(op(e3, e0) = e3)],extension(80 ^ 2)).
% 0.81/1.37 ncf('1.39',plain,[-(op(unit, e4) = e4), op(unit, e4) = op(e0, e4), op(e0, e4) = e4],extension(10 ^ 1,bind([[_195535, _195537, _195539], [e4, op(e0, e4), op(unit, e4)]]))).
% 0.81/1.37 ncf('1.39.1',plain,[-(op(unit, e4) = op(e0, e4)), unit = e0, e4 = e4],extension(20 ^ 2,bind([[_195856, _195858, _195860, _195862], [e4, e4, e0, unit]]))).
% 0.81/1.37 ncf('1.39.1.1',plain,[-(unit = e0)],extension(100 ^ 3)).
% 0.81/1.37 ncf('1.39.1.2',plain,[-(e4 = e4)],extension(2 ^ 3,bind([[_195224], [e4]]))).
% 0.81/1.37 ncf('1.39.2',plain,[-(op(e0, e4) = e4)],extension(58 ^ 2)).
% 0.81/1.37 ncf('1.40',plain,[-(op(e4, unit) = e4), op(e4, unit) = op(e4, e0), op(e4, e0) = e4],extension(10 ^ 1,bind([[_195535, _195537, _195539], [e4, op(e4, e0), op(e4, unit)]]))).
% 0.81/1.37 ncf('1.40.1',plain,[-(op(e4, unit) = op(e4, e0)), e4 = e4, unit = e0],extension(20 ^ 2,bind([[_195856, _195858, _195860, _195862], [e0, unit, e4, e4]]))).
% 0.81/1.37 ncf('1.40.1.1',plain,[-(e4 = e4)],extension(2 ^ 3,bind([[_195224], [e4]]))).
% 0.81/1.37 ncf('1.40.1.2',plain,[-(unit = e0)],extension(100 ^ 3)).
% 0.81/1.37 ncf('1.40.2',plain,[-(op(e4, e0) = e4)],extension(90 ^ 2)).
% 0.81/1.37 ncf('1.41',plain,[-(unit = e0)],extension(100 ^ 3)).
% 0.81/1.37 ncf('1.42',plain,[-(op(e0, e0) = e0)],extension(50 ^ 3)).
% 0.81/1.37 ncf('1.43',plain,[-(op(e0, e0) = e0)],extension(50 ^ 3)).
% 0.81/1.37 ncf('1.44',plain,[-(op(e0, e1) = e1)],extension(52 ^ 3)).
% 0.81/1.37 ncf('1.45',plain,[-(op(e1, e0) = e1)],extension(60 ^ 3)).
% 0.81/1.37 ncf('1.46',plain,[-(op(e0, e2) = e2)],extension(54 ^ 3)).
% 0.81/1.37 ncf('1.47',plain,[-(op(e2, e0) = e2)],extension(70 ^ 3)).
% 0.81/1.37 ncf('1.48',plain,[-(op(e0, e3) = e3)],extension(56 ^ 3)).
% 0.81/1.37 ncf('1.49',plain,[-(op(e3, e0) = e3)],extension(80 ^ 3)).
% 0.81/1.37 ncf('1.50',plain,[-(op(e0, e4) = e4)],extension(58 ^ 3)).
% 0.81/1.37 ncf('1.51',plain,[-(op(e4, e0) = e4)],extension(90 ^ 3)).
% 0.81/1.37 ncf('1.52',plain,[-(op(e1, e2) = e0)],extension(64 ^ 3)).
% 0.81/1.37 ncf('1.53',plain,[-(op(e2, e1) = e0)],extension(72 ^ 3)).
% 0.81/1.37 ncf('1.54',plain,[-(op(e1, e0) = e1)],extension(60 ^ 3)).
% 0.81/1.37 ncf('1.55',plain,[-(op(e0, e1) = e1)],extension(52 ^ 3)).
% 0.81/1.37 ncf('1.56',plain,[-(op(e1, e3) = e2)],extension(66 ^ 3)).
% 0.81/1.37 ncf('1.57',plain,[-(op(e3, e1) = e2)],extension(82 ^ 3)).
% 0.81/1.37 ncf('1.58',plain,[-(op(e1, e4) = e3)],extension(68 ^ 3)).
% 0.81/1.37 ncf('1.59',plain,[-(op(e4, e1) = e3)],extension(92 ^ 3)).
% 0.81/1.37 ncf('1.60',plain,[-(op(e1, e1) = e4)],extension(62 ^ 3)).
% 0.81/1.37 ncf('1.61',plain,[-(op(e1, e1) = e4)],extension(62 ^ 3)).
% 0.81/1.37 ncf('1.62',plain,[-(op(e2, e1) = e0)],extension(72 ^ 3)).
% 0.81/1.37 ncf('1.63',plain,[-(op(e1, e2) = e0)],extension(64 ^ 3)).
% 0.81/1.37 ncf('1.64',plain,[-(op(e2, e4) = e1)],extension(78 ^ 3)).
% 0.81/1.37 ncf('1.65',plain,[-(op(e4, e2) = e1)],extension(94 ^ 3)).
% 0.81/1.37 ncf('1.66',plain,[-(op(e2, e0) = e2)],extension(70 ^ 3)).
% 0.81/1.37 ncf('1.67',plain,[-(op(e0, e2) = e2)],extension(54 ^ 3)).
% 0.81/1.37 ncf('1.68',plain,[-(op(e2, e2) = e3)],extension(74 ^ 3)).
% 0.81/1.37 ncf('1.69',plain,[-(op(e2, e2) = e3)],extension(74 ^ 3)).
% 0.81/1.37 ncf('1.70',plain,[-(op(e2, e3) = e4)],extension(76 ^ 3)).
% 0.81/1.37 ncf('1.71',plain,[-(op(e3, e2) = e4)],extension(84 ^ 3)).
% 0.81/1.37 ncf('1.72',plain,[-(op(e3, e4) = e0)],extension(88 ^ 3)).
% 0.81/1.37 ncf('1.73',plain,[-(op(e4, e3) = e0)],extension(96 ^ 3)).
% 0.81/1.37 ncf('1.74',plain,[-(op(e3, e3) = e1)],extension(86 ^ 3)).
% 0.81/1.37 ncf('1.75',plain,[-(op(e3, e3) = e1)],extension(86 ^ 3)).
% 0.81/1.37 ncf('1.76',plain,[-(op(e3, e1) = e2)],extension(82 ^ 3)).
% 0.81/1.37 ncf('1.77',plain,[-(op(e1, e3) = e2)],extension(66 ^ 3)).
% 0.81/1.37 ncf('1.78',plain,[-(op(e3, e0) = e3)],extension(80 ^ 3)).
% 0.81/1.37 ncf('1.79',plain,[-(op(e0, e3) = e3)],extension(56 ^ 3)).
% 0.81/1.37 ncf('1.80',plain,[-(op(e3, e2) = e4)],extension(84 ^ 3)).
% 0.81/1.37 ncf('1.81',plain,[-(op(e2, e3) = e4)],extension(76 ^ 3)).
% 0.81/1.37 ncf('1.82',plain,[-(op(e4, e3) = e0)],extension(96 ^ 3)).
% 0.81/1.37 ncf('1.83',plain,[-(op(e3, e4) = e0)],extension(88 ^ 3)).
% 0.81/1.37 ncf('1.84',plain,[-(op(e4, e2) = e1)],extension(94 ^ 3)).
% 0.81/1.37 ncf('1.85',plain,[-(op(e2, e4) = e1)],extension(78 ^ 3)).
% 0.81/1.37 ncf('1.86',plain,[-(op(e4, e4) = e2)],extension(98 ^ 3)).
% 0.81/1.37 ncf('1.87',plain,[-(op(e4, e4) = e2)],extension(98 ^ 3)).
% 0.81/1.37 ncf('1.88',plain,[-(op(e4, e1) = e3)],extension(92 ^ 3)).
% 0.81/1.37 ncf('1.89',plain,[-(op(e1, e4) = e3)],extension(68 ^ 3)).
% 0.81/1.37 ncf('1.90',plain,[-(op(e4, e0) = e4)],extension(90 ^ 3)).
% 0.81/1.38 ncf('1.91',plain,[-(op(e0, e4) = e4)],extension(58 ^ 3)).
% 0.81/1.38 %-----------------------------------------------------
% 0.81/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------