%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : ALG017+1 : TPTP v8.1.2. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n002.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:07:53 EDT 2023
% Result : Theorem 0.40s 1.37s
% Output : Proof 0.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ALG017+1 : TPTP v8.1.2. Released v2.7.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n002.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:47:34 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.40/1.37
% 0.40/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.40/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/1.37 %-----------------------------------------------------
% 0.40/1.37 ncf(matrix, plain, [(720 ^ _169800) ^ [] : [721 ^ _169800 : [(722 ^ _169800) ^ [] : [-(op(e0, e0) = e0)], (724 ^ _169800) ^ [] : [-(op(e1, e1) = e0)], (726 ^ _169800) ^ [] : [-(op(e2, e2) = e0)], (728 ^ _169800) ^ [] : [-(op(e3, e3) = e0)]], 731 ^ _169800 : [(732 ^ _169800) ^ [] : [-(op(e0, e0) = e1)], (734 ^ _169800) ^ [] : [-(op(e1, e1) = e1)], (736 ^ _169800) ^ [] : [-(op(e2, e2) = e1)], (738 ^ _169800) ^ [] : [-(op(e3, e3) = e1)]], 741 ^ _169800 : [(742 ^ _169800) ^ [] : [-(op(e0, e0) = e2)], (744 ^ _169800) ^ [] : [-(op(e1, e1) = e2)], (746 ^ _169800) ^ [] : [-(op(e2, e2) = e2)], (748 ^ _169800) ^ [] : [-(op(e3, e3) = e2)]], 749 ^ _169800 : [(750 ^ _169800) ^ [] : [-(op(e0, e0) = e3)], (752 ^ _169800) ^ [] : [-(op(e1, e1) = e3)], (754 ^ _169800) ^ [] : [-(op(e2, e2) = e3)], (756 ^ _169800) ^ [] : [-(op(e3, e3) = e3)]]], (758 ^ _169800) ^ [] : [op(e0, e0) = e0, op(e1, e1) = e0, op(e2, e2) = e0, op(e3, e3) = e0], (772 ^ _169800) ^ [] : [op(e0, e0) = e1, op(e1, e1) = e1, op(e2, e2) = e1, op(e3, e3) = e1], (786 ^ _169800) ^ [] : [op(e0, e0) = e2, op(e1, e1) = e2, op(e2, e2) = e2, op(e3, e3) = e2], (800 ^ _169800) ^ [] : [op(e0, e0) = e3, op(e1, e1) = e3, op(e2, e2) = e3, op(e3, e3) = e3], (2 ^ _169800) ^ [_169924] : [-(_169924 = _169924)], (4 ^ _169800) ^ [_170031, _170033] : [_170033 = _170031, -(_170031 = _170033)], (10 ^ _169800) ^ [_170235, _170237, _170239] : [-(_170239 = _170235), _170239 = _170237, _170237 = _170235], (20 ^ _169800) ^ [_170548, _170550] : [_170550 = _170548, -(inv(_170550) = inv(_170548))], (26 ^ _169800) ^ [_170774, _170776, _170778, _170780] : [-(op(_170780, _170776) = op(_170778, _170774)), _170780 = _170778, _170776 = _170774], (260 ^ _169800) ^ [] : [-(op(op(e0, e0), e0) = op(e0, op(e0, e0)))], (262 ^ _169800) ^ [] : [-(op(op(e0, e0), e1) = op(e0, op(e0, e1)))], (264 ^ _169800) ^ [] : [-(op(op(e0, e0), e2) = op(e0, op(e0, e2)))], (266 ^ _169800) ^ [] : [-(op(op(e0, e0), e3) = op(e0, op(e0, e3)))], (268 ^ _169800) ^ [] : [-(op(op(e0, e1), e0) = op(e0, op(e1, e0)))], (270 ^ _169800) ^ [] : [-(op(op(e0, e1), e1) = op(e0, op(e1, e1)))], (272 ^ _169800) ^ [] : [-(op(op(e0, e1), e2) = op(e0, op(e1, e2)))], (274 ^ _169800) ^ [] : [-(op(op(e0, e1), e3) = op(e0, op(e1, e3)))], (276 ^ _169800) ^ [] : [-(op(op(e0, e2), e0) = op(e0, op(e2, e0)))], (278 ^ _169800) ^ [] : [-(op(op(e0, e2), e1) = op(e0, op(e2, e1)))], (280 ^ _169800) ^ [] : [-(op(op(e0, e2), e2) = op(e0, op(e2, e2)))], (282 ^ _169800) ^ [] : [-(op(op(e0, e2), e3) = op(e0, op(e2, e3)))], (284 ^ _169800) ^ [] : [-(op(op(e0, e3), e0) = op(e0, op(e3, e0)))], (286 ^ _169800) ^ [] : [-(op(op(e0, e3), e1) = op(e0, op(e3, e1)))], (288 ^ _169800) ^ [] : [-(op(op(e0, e3), e2) = op(e0, op(e3, e2)))], (290 ^ _169800) ^ [] : [-(op(op(e0, e3), e3) = op(e0, op(e3, e3)))], (292 ^ _169800) ^ [] : [-(op(op(e1, e0), e0) = op(e1, op(e0, e0)))], (294 ^ _169800) ^ [] : [-(op(op(e1, e0), e1) = op(e1, op(e0, e1)))], (296 ^ _169800) ^ [] : [-(op(op(e1, e0), e2) = op(e1, op(e0, e2)))], (298 ^ _169800) ^ [] : [-(op(op(e1, e0), e3) = op(e1, op(e0, e3)))], (300 ^ _169800) ^ [] : [-(op(op(e1, e1), e0) = op(e1, op(e1, e0)))], (302 ^ _169800) ^ [] : [-(op(op(e1, e1), e1) = op(e1, op(e1, e1)))], (304 ^ _169800) ^ [] : [-(op(op(e1, e1), e2) = op(e1, op(e1, e2)))], (306 ^ _169800) ^ [] : [-(op(op(e1, e1), e3) = op(e1, op(e1, e3)))], (308 ^ _169800) ^ [] : [-(op(op(e1, e2), e0) = op(e1, op(e2, e0)))], (310 ^ _169800) ^ [] : [-(op(op(e1, e2), e1) = op(e1, op(e2, e1)))], (312 ^ _169800) ^ [] : [-(op(op(e1, e2), e2) = op(e1, op(e2, e2)))], (314 ^ _169800) ^ [] : [-(op(op(e1, e2), e3) = op(e1, op(e2, e3)))], (316 ^ _169800) ^ [] : [-(op(op(e1, e3), e0) = op(e1, op(e3, e0)))], (318 ^ _169800) ^ [] : [-(op(op(e1, e3), e1) = op(e1, op(e3, e1)))], (320 ^ _169800) ^ [] : [-(op(op(e1, e3), e2) = op(e1, op(e3, e2)))], (322 ^ _169800) ^ [] : [-(op(op(e1, e3), e3) = op(e1, op(e3, e3)))], (324 ^ _169800) ^ [] : [-(op(op(e2, e0), e0) = op(e2, op(e0, e0)))], (326 ^ _169800) ^ [] : [-(op(op(e2, e0), e1) = op(e2, op(e0, e1)))], (328 ^ _169800) ^ [] : [-(op(op(e2, e0), e2) = op(e2, op(e0, e2)))], (330 ^ _169800) ^ [] : [-(op(op(e2, e0), e3) = op(e2, op(e0, e3)))], (332 ^ _169800) ^ [] : [-(op(op(e2, e1), e0) = op(e2, op(e1, e0)))], (334 ^ _169800) ^ [] : [-(op(op(e2, e1), e1) = op(e2, op(e1, e1)))], (336 ^ _169800) ^ [] : [-(op(op(e2, e1), e2) = op(e2, op(e1, e2)))], (338 ^ _169800) ^ [] : [-(op(op(e2, e1), e3) = op(e2, op(e1, e3)))], (340 ^ _169800) ^ [] : [-(op(op(e2, e2), e0) = op(e2, op(e2, e0)))], (342 ^ _169800) ^ [] : [-(op(op(e2, e2), e1) = op(e2, op(e2, e1)))], (344 ^ _169800) ^ [] : [-(op(op(e2, e2), e2) = op(e2, op(e2, e2)))], (346 ^ _169800) ^ [] : [-(op(op(e2, e2), e3) = op(e2, op(e2, e3)))], (348 ^ _169800) ^ [] : [-(op(op(e2, e3), e0) = op(e2, op(e3, e0)))], (350 ^ _169800) ^ [] : [-(op(op(e2, e3), e1) = op(e2, op(e3, e1)))], (352 ^ _169800) ^ [] : [-(op(op(e2, e3), e2) = op(e2, op(e3, e2)))], (354 ^ _169800) ^ [] : [-(op(op(e2, e3), e3) = op(e2, op(e3, e3)))], (356 ^ _169800) ^ [] : [-(op(op(e3, e0), e0) = op(e3, op(e0, e0)))], (358 ^ _169800) ^ [] : [-(op(op(e3, e0), e1) = op(e3, op(e0, e1)))], (360 ^ _169800) ^ [] : [-(op(op(e3, e0), e2) = op(e3, op(e0, e2)))], (362 ^ _169800) ^ [] : [-(op(op(e3, e0), e3) = op(e3, op(e0, e3)))], (364 ^ _169800) ^ [] : [-(op(op(e3, e1), e0) = op(e3, op(e1, e0)))], (366 ^ _169800) ^ [] : [-(op(op(e3, e1), e1) = op(e3, op(e1, e1)))], (368 ^ _169800) ^ [] : [-(op(op(e3, e1), e2) = op(e3, op(e1, e2)))], (370 ^ _169800) ^ [] : [-(op(op(e3, e1), e3) = op(e3, op(e1, e3)))], (372 ^ _169800) ^ [] : [-(op(op(e3, e2), e0) = op(e3, op(e2, e0)))], (374 ^ _169800) ^ [] : [-(op(op(e3, e2), e1) = op(e3, op(e2, e1)))], (376 ^ _169800) ^ [] : [-(op(op(e3, e2), e2) = op(e3, op(e2, e2)))], (378 ^ _169800) ^ [] : [-(op(op(e3, e2), e3) = op(e3, op(e2, e3)))], (380 ^ _169800) ^ [] : [-(op(op(e3, e3), e0) = op(e3, op(e3, e0)))], (382 ^ _169800) ^ [] : [-(op(op(e3, e3), e1) = op(e3, op(e3, e1)))], (384 ^ _169800) ^ [] : [-(op(op(e3, e3), e2) = op(e3, op(e3, e2)))], (386 ^ _169800) ^ [] : [-(op(op(e3, e3), e3) = op(e3, op(e3, e3)))], (388 ^ _169800) ^ [] : [-(op(unit, e0) = e0)], (390 ^ _169800) ^ [] : [-(op(e0, unit) = e0)], (392 ^ _169800) ^ [] : [-(op(unit, e1) = e1)], (394 ^ _169800) ^ [] : [-(op(e1, unit) = e1)], (396 ^ _169800) ^ [] : [-(op(unit, e2) = e2)], (398 ^ _169800) ^ [] : [-(op(e2, unit) = e2)], (400 ^ _169800) ^ [] : [-(op(unit, e3) = e3)], (402 ^ _169800) ^ [] : [-(op(e3, unit) = e3)], (404 ^ _169800) ^ [] : [-(unit = e0), -(unit = e1), -(unit = e2), -(unit = e3)], (418 ^ _169800) ^ [] : [-(op(e0, inv(e0)) = unit)], (420 ^ _169800) ^ [] : [-(op(inv(e0), e0) = unit)], (422 ^ _169800) ^ [] : [-(op(e1, inv(e1)) = unit)], (424 ^ _169800) ^ [] : [-(op(inv(e1), e1) = unit)], (426 ^ _169800) ^ [] : [-(op(e2, inv(e2)) = unit)], (428 ^ _169800) ^ [] : [-(op(inv(e2), e2) = unit)], (430 ^ _169800) ^ [] : [-(op(e3, inv(e3)) = unit)], (432 ^ _169800) ^ [] : [-(op(inv(e3), e3) = unit)], (434 ^ _169800) ^ [] : [-(inv(e0) = e0), -(inv(e0) = e1), -(inv(e0) = e2), -(inv(e0) = e3)], (448 ^ _169800) ^ [] : [-(inv(e1) = e0), -(inv(e1) = e1), -(inv(e1) = e2), -(inv(e1) = e3)], (462 ^ _169800) ^ [] : [-(inv(e2) = e0), -(inv(e2) = e1), -(inv(e2) = e2), -(inv(e2) = e3)], (476 ^ _169800) ^ [] : [-(inv(e3) = e0), -(inv(e3) = e1), -(inv(e3) = e2), -(inv(e3) = e3)], (490 ^ _169800) ^ [] : [-(inv(unit) = unit)], (492 ^ _169800) ^ [] : [-(inv(inv(e0)) = e0)], (494 ^ _169800) ^ [] : [-(inv(inv(e1)) = e1)], (496 ^ _169800) ^ [] : [-(inv(inv(e2)) = e2)], (498 ^ _169800) ^ [] : [-(inv(inv(e3)) = e3)], (596 ^ _169800) ^ [] : [inv(e0) = inv(e1)], (598 ^ _169800) ^ [] : [inv(e0) = inv(e2)], (600 ^ _169800) ^ [] : [inv(e0) = inv(e3)], (602 ^ _169800) ^ [] : [inv(e1) = inv(e2)], (604 ^ _169800) ^ [] : [inv(e1) = inv(e3)], (606 ^ _169800) ^ [] : [inv(e2) = inv(e3)], (608 ^ _169800) ^ [] : [op(e0, e0) = op(e1, e0)], (610 ^ _169800) ^ [] : [op(e0, e0) = op(e2, e0)], (612 ^ _169800) ^ [] : [op(e0, e0) = op(e3, e0)], (614 ^ _169800) ^ [] : [op(e1, e0) = op(e2, e0)], (616 ^ _169800) ^ [] : [op(e1, e0) = op(e3, e0)], (618 ^ _169800) ^ [] : [op(e2, e0) = op(e3, e0)], (620 ^ _169800) ^ [] : [op(e0, e1) = op(e1, e1)], (622 ^ _169800) ^ [] : [op(e0, e1) = op(e2, e1)], (624 ^ _169800) ^ [] : [op(e0, e1) = op(e3, e1)], (626 ^ _169800) ^ [] : [op(e1, e1) = op(e2, e1)], (628 ^ _169800) ^ [] : [op(e1, e1) = op(e3, e1)], (630 ^ _169800) ^ [] : [op(e2, e1) = op(e3, e1)], (632 ^ _169800) ^ [] : [op(e0, e2) = op(e1, e2)], (634 ^ _169800) ^ [] : [op(e0, e2) = op(e2, e2)], (636 ^ _169800) ^ [] : [op(e0, e2) = op(e3, e2)], (638 ^ _169800) ^ [] : [op(e1, e2) = op(e2, e2)], (640 ^ _169800) ^ [] : [op(e1, e2) = op(e3, e2)], (642 ^ _169800) ^ [] : [op(e2, e2) = op(e3, e2)], (644 ^ _169800) ^ [] : [op(e0, e3) = op(e1, e3)], (646 ^ _169800) ^ [] : [op(e0, e3) = op(e2, e3)], (648 ^ _169800) ^ [] : [op(e0, e3) = op(e3, e3)], (650 ^ _169800) ^ [] : [op(e1, e3) = op(e2, e3)], (652 ^ _169800) ^ [] : [op(e1, e3) = op(e3, e3)], (654 ^ _169800) ^ [] : [op(e2, e3) = op(e3, e3)], (656 ^ _169800) ^ [] : [op(e0, e0) = op(e0, e1)], (658 ^ _169800) ^ [] : [op(e0, e0) = op(e0, e2)], (660 ^ _169800) ^ [] : [op(e0, e0) = op(e0, e3)], (662 ^ _169800) ^ [] : [op(e0, e1) = op(e0, e2)], (664 ^ _169800) ^ [] : [op(e0, e1) = op(e0, e3)], (666 ^ _169800) ^ [] : [op(e0, e2) = op(e0, e3)], (668 ^ _169800) ^ [] : [op(e1, e0) = op(e1, e1)], (670 ^ _169800) ^ [] : [op(e1, e0) = op(e1, e2)], (672 ^ _169800) ^ [] : [op(e1, e0) = op(e1, e3)], (674 ^ _169800) ^ [] : [op(e1, e1) = op(e1, e2)], (676 ^ _169800) ^ [] : [op(e1, e1) = op(e1, e3)], (678 ^ _169800) ^ [] : [op(e1, e2) = op(e1, e3)], (680 ^ _169800) ^ [] : [op(e2, e0) = op(e2, e1)], (682 ^ _169800) ^ [] : [op(e2, e0) = op(e2, e2)], (684 ^ _169800) ^ [] : [op(e2, e0) = op(e2, e3)], (686 ^ _169800) ^ [] : [op(e2, e1) = op(e2, e2)], (688 ^ _169800) ^ [] : [op(e2, e1) = op(e2, e3)], (690 ^ _169800) ^ [] : [op(e2, e2) = op(e2, e3)], (692 ^ _169800) ^ [] : [op(e3, e0) = op(e3, e1)], (694 ^ _169800) ^ [] : [op(e3, e0) = op(e3, e2)], (696 ^ _169800) ^ [] : [op(e3, e0) = op(e3, e3)], (698 ^ _169800) ^ [] : [op(e3, e1) = op(e3, e2)], (700 ^ _169800) ^ [] : [op(e3, e1) = op(e3, e3)], (702 ^ _169800) ^ [] : [op(e3, e2) = op(e3, e3)], (704 ^ _169800) ^ [] : [e0 = e1], (706 ^ _169800) ^ [] : [e0 = e2], (708 ^ _169800) ^ [] : [e0 = e3], (710 ^ _169800) ^ [] : [e1 = e2], (712 ^ _169800) ^ [] : [e1 = e3], (714 ^ _169800) ^ [] : [e2 = e3], (716 ^ _169800) ^ [] : [-(e0 = op(e3, e3))], (718 ^ _169800) ^ [] : [-(e1 = op(e2, e3))], (500 ^ _169800) ^ [] : [inv(e0) = e0, -(inv(e0) = e0)], (506 ^ _169800) ^ [] : [inv(e0) = e1, -(inv(e1) = e0)], (512 ^ _169800) ^ [] : [inv(e0) = e2, -(inv(e2) = e0)], (518 ^ _169800) ^ [] : [inv(e0) = e3, -(inv(e3) = e0)], (524 ^ _169800) ^ [] : [inv(e1) = e0, -(inv(e0) = e1)], (530 ^ _169800) ^ [] : [inv(e1) = e1, -(inv(e1) = e1)], (536 ^ _169800) ^ [] : [inv(e1) = e2, -(inv(e2) = e1)], (542 ^ _169800) ^ [] : [inv(e1) = e3, -(inv(e3) = e1)], (548 ^ _169800) ^ [] : [inv(e2) = e0, -(inv(e0) = e2)], (554 ^ _169800) ^ [] : [inv(e2) = e1, -(inv(e1) = e2)], (560 ^ _169800) ^ [] : [inv(e2) = e2, -(inv(e2) = e2)], (566 ^ _169800) ^ [] : [inv(e2) = e3, -(inv(e3) = e2)], (572 ^ _169800) ^ [] : [inv(e3) = e0, -(inv(e0) = e3)], (578 ^ _169800) ^ [] : [inv(e3) = e1, -(inv(e1) = e3)], (584 ^ _169800) ^ [] : [inv(e3) = e2, -(inv(e2) = e3)], (590 ^ _169800) ^ [] : [inv(e3) = e3, -(inv(e3) = e3)], (36 ^ _169800) ^ [] : [-(op(e0, e0) = e0), -(op(e0, e0) = e1), -(op(e0, e0) = e2), -(op(e0, e0) = e3)], (50 ^ _169800) ^ [] : [-(op(e0, e1) = e0), -(op(e0, e1) = e1), -(op(e0, e1) = e2), -(op(e0, e1) = e3)], (64 ^ _169800) ^ [] : [-(op(e0, e2) = e0), -(op(e0, e2) = e1), -(op(e0, e2) = e2), -(op(e0, e2) = e3)], (78 ^ _169800) ^ [] : [-(op(e0, e3) = e0), -(op(e0, e3) = e1), -(op(e0, e3) = e2), -(op(e0, e3) = e3)], (92 ^ _169800) ^ [] : [-(op(e1, e0) = e0), -(op(e1, e0) = e1), -(op(e1, e0) = e2), -(op(e1, e0) = e3)], (106 ^ _169800) ^ [] : [-(op(e1, e1) = e0), -(op(e1, e1) = e1), -(op(e1, e1) = e2), -(op(e1, e1) = e3)], (120 ^ _169800) ^ [] : [-(op(e1, e2) = e0), -(op(e1, e2) = e1), -(op(e1, e2) = e2), -(op(e1, e2) = e3)], (134 ^ _169800) ^ [] : [-(op(e1, e3) = e0), -(op(e1, e3) = e1), -(op(e1, e3) = e2), -(op(e1, e3) = e3)], (148 ^ _169800) ^ [] : [-(op(e2, e0) = e0), -(op(e2, e0) = e1), -(op(e2, e0) = e2), -(op(e2, e0) = e3)], (162 ^ _169800) ^ [] : [-(op(e2, e1) = e0), -(op(e2, e1) = e1), -(op(e2, e1) = e2), -(op(e2, e1) = e3)], (176 ^ _169800) ^ [] : [-(op(e2, e2) = e0), -(op(e2, e2) = e1), -(op(e2, e2) = e2), -(op(e2, e2) = e3)], (190 ^ _169800) ^ [] : [-(op(e2, e3) = e0), -(op(e2, e3) = e1), -(op(e2, e3) = e2), -(op(e2, e3) = e3)], (204 ^ _169800) ^ [] : [-(op(e3, e0) = e0), -(op(e3, e0) = e1), -(op(e3, e0) = e2), -(op(e3, e0) = e3)], (218 ^ _169800) ^ [] : [-(op(e3, e1) = e0), -(op(e3, e1) = e1), -(op(e3, e1) = e2), -(op(e3, e1) = e3)], (232 ^ _169800) ^ [] : [-(op(e3, e2) = e0), -(op(e3, e2) = e1), -(op(e3, e2) = e2), -(op(e3, e2) = e3)], (246 ^ _169800) ^ [] : [-(op(e3, e3) = e0), -(op(e3, e3) = e1), -(op(e3, e3) = e2), -(op(e3, e3) = e3)]], input).
% 0.40/1.37 ncf('1',plain,[op(e0, e0) = e0, op(e1, e1) = e0, op(e2, e2) = e0, op(e3, e3) = e0],start(758 ^ 0)).
% 0.40/1.37 ncf('1.1',plain,[-(op(e0, e0) = e0), 732 : -(op(e0, e0) = e1), 742 : -(op(e0, e0) = e2), 750 : -(op(e0, e0) = e3)],extension(720 ^ 1)).
% 0.40/1.37 ncf('1.1.1',plain,[op(e0, e0) = e1, op(e1, e1) = e1, op(e2, e2) = e1, op(e3, e3) = e1],extension(772 ^ 4)).
% 0.40/1.37 ncf('1.1.1.1',plain,[-(op(e1, e1) = e1)],extension(734 ^ 5)).
% 0.40/1.37 ncf('1.1.1.2',plain,[-(op(e2, e2) = e1)],extension(736 ^ 5)).
% 0.40/1.37 ncf('1.1.1.3',plain,[-(op(e3, e3) = e1)],extension(738 ^ 5)).
% 0.40/1.37 ncf('1.1.2',plain,[op(e0, e0) = e2, op(e1, e1) = e2, op(e2, e2) = e2, op(e3, e3) = e2],extension(786 ^ 4)).
% 0.40/1.37 ncf('1.1.2.1',plain,[-(op(e1, e1) = e2)],extension(744 ^ 5)).
% 0.40/1.37 ncf('1.1.2.2',plain,[-(op(e2, e2) = e2)],extension(746 ^ 5)).
% 0.40/1.37 ncf('1.1.2.3',plain,[-(op(e3, e3) = e2)],extension(748 ^ 5)).
% 0.40/1.37 ncf('1.1.3',plain,[op(e0, e0) = e3, op(e1, e1) = e3, op(e2, e2) = e3, op(e3, e3) = e3],extension(800 ^ 4)).
% 0.40/1.37 ncf('1.1.3.1',plain,[-(op(e1, e1) = e3)],extension(752 ^ 5)).
% 0.40/1.37 ncf('1.1.3.2',plain,[-(op(e2, e2) = e3)],extension(754 ^ 5)).
% 0.40/1.37 ncf('1.1.3.3',plain,[-(op(e3, e3) = e3)],extension(756 ^ 5)).
% 0.40/1.37 ncf('1.2',plain,[-(op(e1, e1) = e0), 732 : -(op(e0, e0) = e1), 742 : -(op(e0, e0) = e2), 750 : -(op(e0, e0) = e3)],extension(720 ^ 1)).
% 0.40/1.37 ncf('1.2.1',plain,[op(e0, e0) = e1, op(e1, e1) = e1, op(e2, e2) = e1, op(e3, e3) = e1],extension(772 ^ 4)).
% 0.40/1.37 ncf('1.2.1.1',plain,[-(op(e1, e1) = e1)],extension(734 ^ 5)).
% 0.40/1.37 ncf('1.2.1.2',plain,[-(op(e2, e2) = e1)],extension(736 ^ 5)).
% 0.40/1.37 ncf('1.2.1.3',plain,[-(op(e3, e3) = e1)],extension(738 ^ 5)).
% 0.40/1.37 ncf('1.2.2',plain,[op(e0, e0) = e2, op(e1, e1) = e2, op(e2, e2) = e2, op(e3, e3) = e2],extension(786 ^ 4)).
% 0.40/1.37 ncf('1.2.2.1',plain,[-(op(e1, e1) = e2)],extension(744 ^ 5)).
% 0.40/1.37 ncf('1.2.2.2',plain,[-(op(e2, e2) = e2)],extension(746 ^ 5)).
% 0.40/1.37 ncf('1.2.2.3',plain,[-(op(e3, e3) = e2)],extension(748 ^ 5)).
% 0.40/1.37 ncf('1.2.3',plain,[op(e0, e0) = e3, op(e1, e1) = e3, op(e2, e2) = e3, op(e3, e3) = e3],extension(800 ^ 4)).
% 0.40/1.37 ncf('1.2.3.1',plain,[-(op(e1, e1) = e3)],extension(752 ^ 5)).
% 0.40/1.37 ncf('1.2.3.2',plain,[-(op(e2, e2) = e3)],extension(754 ^ 5)).
% 0.40/1.37 ncf('1.2.3.3',plain,[-(op(e3, e3) = e3)],extension(756 ^ 5)).
% 0.40/1.37 ncf('1.3',plain,[-(op(e2, e2) = e0), 732 : -(op(e0, e0) = e1), 742 : -(op(e0, e0) = e2), 750 : -(op(e0, e0) = e3)],extension(720 ^ 1)).
% 0.40/1.37 ncf('1.3.1',plain,[op(e0, e0) = e1, op(e1, e1) = e1, op(e2, e2) = e1, op(e3, e3) = e1],extension(772 ^ 4)).
% 0.40/1.37 ncf('1.3.1.1',plain,[-(op(e1, e1) = e1)],extension(734 ^ 5)).
% 0.40/1.37 ncf('1.3.1.2',plain,[-(op(e2, e2) = e1)],extension(736 ^ 5)).
% 0.40/1.37 ncf('1.3.1.3',plain,[-(op(e3, e3) = e1)],extension(738 ^ 5)).
% 0.40/1.37 ncf('1.3.2',plain,[op(e0, e0) = e2, op(e1, e1) = e2, op(e2, e2) = e2, op(e3, e3) = e2],extension(786 ^ 4)).
% 0.40/1.37 ncf('1.3.2.1',plain,[-(op(e1, e1) = e2)],extension(744 ^ 5)).
% 0.40/1.37 ncf('1.3.2.2',plain,[-(op(e2, e2) = e2)],extension(746 ^ 5)).
% 0.40/1.37 ncf('1.3.2.3',plain,[-(op(e3, e3) = e2)],extension(748 ^ 5)).
% 0.40/1.37 ncf('1.3.3',plain,[op(e0, e0) = e3, op(e1, e1) = e3, op(e2, e2) = e3, op(e3, e3) = e3],extension(800 ^ 4)).
% 0.40/1.37 ncf('1.3.3.1',plain,[-(op(e1, e1) = e3)],extension(752 ^ 5)).
% 0.40/1.37 ncf('1.3.3.2',plain,[-(op(e2, e2) = e3)],extension(754 ^ 5)).
% 0.40/1.37 ncf('1.3.3.3',plain,[-(op(e3, e3) = e3)],extension(756 ^ 5)).
% 0.40/1.37 ncf('1.4',plain,[-(op(e3, e3) = e0), 732 : -(op(e0, e0) = e1), 742 : -(op(e0, e0) = e2), 750 : -(op(e0, e0) = e3)],extension(720 ^ 1)).
% 0.40/1.37 ncf('1.4.1',plain,[op(e0, e0) = e1, op(e1, e1) = e1, op(e2, e2) = e1, op(e3, e3) = e1],extension(772 ^ 4)).
% 0.40/1.37 ncf('1.4.1.1',plain,[-(op(e1, e1) = e1)],extension(734 ^ 5)).
% 0.40/1.37 ncf('1.4.1.2',plain,[-(op(e2, e2) = e1)],extension(736 ^ 5)).
% 0.40/1.37 ncf('1.4.1.3',plain,[-(op(e3, e3) = e1)],extension(738 ^ 5)).
% 0.40/1.37 ncf('1.4.2',plain,[op(e0, e0) = e2, op(e1, e1) = e2, op(e2, e2) = e2, op(e3, e3) = e2],extension(786 ^ 4)).
% 0.40/1.37 ncf('1.4.2.1',plain,[-(op(e1, e1) = e2)],extension(744 ^ 5)).
% 0.40/1.37 ncf('1.4.2.2',plain,[-(op(e2, e2) = e2)],extension(746 ^ 5)).
% 0.40/1.37 ncf('1.4.2.3',plain,[-(op(e3, e3) = e2)],extension(748 ^ 5)).
% 0.40/1.37 ncf('1.4.3',plain,[op(e0, e0) = e3, op(e1, e1) = e3, op(e2, e2) = e3, op(e3, e3) = e3],extension(800 ^ 4)).
% 0.40/1.37 ncf('1.4.3.1',plain,[-(op(e1, e1) = e3)],extension(752 ^ 5)).
% 0.40/1.37 ncf('1.4.3.2',plain,[-(op(e2, e2) = e3)],extension(754 ^ 5)).
% 0.40/1.37 ncf('1.4.3.3',plain,[-(op(e3, e3) = e3)],extension(756 ^ 5)).
% 0.40/1.37 %-----------------------------------------------------
% 0.40/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------