%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : ALG194+1 : TPTP v8.1.2. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n028.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:11 EDT 2023
% Result : Theorem 0.38s 1.39s
% Output : Proof 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ALG194+1 : TPTP v8.1.2. Released v2.7.0.
% 0.03/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n028.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 23:28:48 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.38/1.39
% 0.38/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.38/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/1.39 %-----------------------------------------------------
% 0.38/1.39 ncf(matrix, plain, [(4580 ^ _96822) ^ [] : [-(op(e0, e0) = e0), -(op(e1, e1) = e1), -(op(e2, e2) = e2), -(op(e3, e3) = e3), -(op(e4, e4) = e4), -(op(e5, e5) = e5), -(op(e6, e6) = e6)], (4632 ^ _96822) ^ [] : [4633 ^ _96822 : [(4634 ^ _96822) ^ [] : [op(e0, e0) = e0], (4636 ^ _96822) ^ [] : [op(e1, e1) = e1], (4638 ^ _96822) ^ [] : [op(e2, e2) = e2], (4640 ^ _96822) ^ [] : [op(e3, e3) = e3], (4642 ^ _96822) ^ [] : [op(e4, e4) = e4], (4644 ^ _96822) ^ [] : [op(e5, e5) = e5], (4646 ^ _96822) ^ [] : [op(e6, e6) = e6]], 4647 ^ _96822 : [(4648 ^ _96822) ^ [] : [-(op(e0, e0) = e0)], (4650 ^ _96822) ^ [] : [-(op(e1, e1) = e1)], (4652 ^ _96822) ^ [] : [-(op(e2, e2) = e2)], (4654 ^ _96822) ^ [] : [-(op(e3, e3) = e3)], (4656 ^ _96822) ^ [] : [-(op(e4, e4) = e4)], (4658 ^ _96822) ^ [] : [-(op(e5, e5) = e5)], (4660 ^ _96822) ^ [] : [-(op(e6, e6) = e6)]]], (4606 ^ _96822) ^ [] : [op(e0, e0) = e0, op(e1, e1) = e1, op(e2, e2) = e2, op(e3, e3) = e3, op(e4, e4) = e4, op(e5, e5) = e5, op(e6, e6) = e6], (20 ^ _96822) ^ [_97578, _97580, _97582, _97584] : [-(op(_97584, _97580) = op(_97582, _97578)), _97584 = _97582, _97580 = _97578], (2 ^ _96822) ^ [_96946] : [-(_96946 = _96946)], (4 ^ _96822) ^ [_97053, _97055] : [_97055 = _97053, -(_97053 = _97055)], (10 ^ _96822) ^ [_97257, _97259, _97261] : [-(_97261 = _97257), _97261 = _97259, _97259 = _97257], (30 ^ _96822) ^ [] : [-(op(e0, e0) = e0), -(op(e0, e0) = e1), -(op(e0, e0) = e2), -(op(e0, e0) = e3), -(op(e0, e0) = e4), -(op(e0, e0) = e5), -(op(e0, e0) = e6)], (56 ^ _96822) ^ [] : [-(op(e0, e1) = e0), -(op(e0, e1) = e1), -(op(e0, e1) = e2), -(op(e0, e1) = e3), -(op(e0, e1) = e4), -(op(e0, e1) = e5), -(op(e0, e1) = e6)], (82 ^ _96822) ^ [] : [-(op(e0, e2) = e0), -(op(e0, e2) = e1), -(op(e0, e2) = e2), -(op(e0, e2) = e3), -(op(e0, e2) = e4), -(op(e0, e2) = e5), -(op(e0, e2) = e6)], (108 ^ _96822) ^ [] : [-(op(e0, e3) = e0), -(op(e0, e3) = e1), -(op(e0, e3) = e2), -(op(e0, e3) = e3), -(op(e0, e3) = e4), -(op(e0, e3) = e5), -(op(e0, e3) = e6)], (134 ^ _96822) ^ [] : [-(op(e0, e4) = e0), -(op(e0, e4) = e1), -(op(e0, e4) = e2), -(op(e0, e4) = e3), -(op(e0, e4) = e4), -(op(e0, e4) = e5), -(op(e0, e4) = e6)], (160 ^ _96822) ^ [] : [-(op(e0, e5) = e0), -(op(e0, e5) = e1), -(op(e0, e5) = e2), -(op(e0, e5) = e3), -(op(e0, e5) = e4), -(op(e0, e5) = e5), -(op(e0, e5) = e6)], (186 ^ _96822) ^ [] : [-(op(e0, e6) = e0), -(op(e0, e6) = e1), -(op(e0, e6) = e2), -(op(e0, e6) = e3), -(op(e0, e6) = e4), -(op(e0, e6) = e5), -(op(e0, e6) = e6)], (212 ^ _96822) ^ [] : [-(op(e1, e0) = e0), -(op(e1, e0) = e1), -(op(e1, e0) = e2), -(op(e1, e0) = e3), -(op(e1, e0) = e4), -(op(e1, e0) = e5), -(op(e1, e0) = e6)], (238 ^ _96822) ^ [] : [-(op(e1, e1) = e0), -(op(e1, e1) = e1), -(op(e1, e1) = e2), -(op(e1, e1) = e3), -(op(e1, e1) = e4), -(op(e1, e1) = e5), -(op(e1, e1) = e6)], (264 ^ _96822) ^ [] : [-(op(e1, e2) = e0), -(op(e1, e2) = e1), -(op(e1, e2) = e2), -(op(e1, e2) = e3), -(op(e1, e2) = e4), -(op(e1, e2) = e5), -(op(e1, e2) = e6)], (290 ^ _96822) ^ [] : [-(op(e1, e3) = e0), -(op(e1, e3) = e1), -(op(e1, e3) = e2), -(op(e1, e3) = e3), -(op(e1, e3) = e4), -(op(e1, e3) = e5), -(op(e1, e3) = e6)], (316 ^ _96822) ^ [] : [-(op(e1, e4) = e0), -(op(e1, e4) = e1), -(op(e1, e4) = e2), -(op(e1, e4) = e3), -(op(e1, e4) = e4), -(op(e1, e4) = e5), -(op(e1, e4) = e6)], (342 ^ _96822) ^ [] : [-(op(e1, e5) = e0), -(op(e1, e5) = e1), -(op(e1, e5) = e2), -(op(e1, e5) = e3), -(op(e1, e5) = e4), -(op(e1, e5) = e5), -(op(e1, e5) = e6)], (368 ^ _96822) ^ [] : [-(op(e1, e6) = e0), -(op(e1, e6) = e1), -(op(e1, e6) = e2), -(op(e1, e6) = e3), -(op(e1, e6) = e4), -(op(e1, e6) = e5), -(op(e1, e6) = e6)], (394 ^ _96822) ^ [] : [-(op(e2, e0) = e0), -(op(e2, e0) = e1), -(op(e2, e0) = e2), -(op(e2, e0) = e3), -(op(e2, e0) = e4), -(op(e2, e0) = e5), -(op(e2, e0) = e6)], (420 ^ _96822) ^ [] : [-(op(e2, e1) = e0), -(op(e2, e1) = e1), -(op(e2, e1) = e2), -(op(e2, e1) = e3), -(op(e2, e1) = e4), -(op(e2, e1) = e5), -(op(e2, e1) = e6)], (446 ^ _96822) ^ [] : [-(op(e2, e2) = e0), -(op(e2, e2) = e1), -(op(e2, e2) = e2), -(op(e2, e2) = e3), -(op(e2, e2) = e4), -(op(e2, e2) = e5), -(op(e2, e2) = e6)], (472 ^ _96822) ^ [] : [-(op(e2, e3) = e0), -(op(e2, e3) = e1), -(op(e2, e3) = e2), -(op(e2, e3) = e3), -(op(e2, e3) = e4), -(op(e2, e3) = e5), -(op(e2, e3) = e6)], (498 ^ _96822) ^ [] : [-(op(e2, e4) = e0), -(op(e2, e4) = e1), -(op(e2, e4) = e2), -(op(e2, e4) = e3), -(op(e2, e4) = e4), -(op(e2, e4) = e5), -(op(e2, e4) = e6)], (524 ^ _96822) ^ [] : [-(op(e2, e5) = e0), -(op(e2, e5) = e1), -(op(e2, e5) = e2), -(op(e2, e5) = e3), -(op(e2, e5) = e4), -(op(e2, e5) = e5), -(op(e2, e5) = e6)], (550 ^ _96822) ^ [] : [-(op(e2, e6) = e0), -(op(e2, e6) = e1), -(op(e2, e6) = e2), -(op(e2, e6) = e3), -(op(e2, e6) = e4), -(op(e2, e6) = e5), -(op(e2, e6) = e6)], (576 ^ _96822) ^ [] : [-(op(e3, e0) = e0), -(op(e3, e0) = e1), -(op(e3, e0) = e2), -(op(e3, e0) = e3), -(op(e3, e0) = e4), -(op(e3, e0) = e5), -(op(e3, e0) = e6)], (602 ^ _96822) ^ [] : [-(op(e3, e1) = e0), -(op(e3, e1) = e1), -(op(e3, e1) = e2), -(op(e3, e1) = e3), -(op(e3, e1) = e4), -(op(e3, e1) = e5), -(op(e3, e1) = e6)], (628 ^ _96822) ^ [] : [-(op(e3, e2) = e0), -(op(e3, e2) = e1), -(op(e3, e2) = e2), -(op(e3, e2) = e3), -(op(e3, e2) = e4), -(op(e3, e2) = e5), -(op(e3, e2) = e6)], (654 ^ _96822) ^ [] : [-(op(e3, e3) = e0), -(op(e3, e3) = e1), -(op(e3, e3) = e2), -(op(e3, e3) = e3), -(op(e3, e3) = e4), -(op(e3, e3) = e5), -(op(e3, e3) = e6)], (680 ^ _96822) ^ [] : [-(op(e3, e4) = e0), -(op(e3, e4) = e1), -(op(e3, e4) = e2), -(op(e3, e4) = e3), -(op(e3, e4) = e4), -(op(e3, e4) = e5), -(op(e3, e4) = e6)], (706 ^ _96822) ^ [] : [-(op(e3, e5) = e0), -(op(e3, e5) = e1), -(op(e3, e5) = e2), -(op(e3, e5) = e3), -(op(e3, e5) = e4), -(op(e3, e5) = e5), -(op(e3, e5) = e6)], (732 ^ _96822) ^ [] : [-(op(e3, e6) = e0), -(op(e3, e6) = e1), -(op(e3, e6) = e2), -(op(e3, e6) = e3), -(op(e3, e6) = e4), -(op(e3, e6) = e5), -(op(e3, e6) = e6)], (758 ^ _96822) ^ [] : [-(op(e4, e0) = e0), -(op(e4, e0) = e1), -(op(e4, e0) = e2), -(op(e4, e0) = e3), -(op(e4, e0) = e4), -(op(e4, e0) = e5), -(op(e4, e0) = e6)], (784 ^ _96822) ^ [] : [-(op(e4, e1) = e0), -(op(e4, e1) = e1), -(op(e4, e1) = e2), -(op(e4, e1) = e3), -(op(e4, e1) = e4), -(op(e4, e1) = e5), -(op(e4, e1) = e6)], (810 ^ _96822) ^ [] : [-(op(e4, e2) = e0), -(op(e4, e2) = e1), -(op(e4, e2) = e2), -(op(e4, e2) = e3), -(op(e4, e2) = e4), -(op(e4, e2) = e5), -(op(e4, e2) = e6)], (836 ^ _96822) ^ [] : [-(op(e4, e3) = e0), -(op(e4, e3) = e1), -(op(e4, e3) = e2), -(op(e4, e3) = e3), -(op(e4, e3) = e4), -(op(e4, e3) = e5), -(op(e4, e3) = e6)], (862 ^ _96822) ^ [] : [-(op(e4, e4) = e0), -(op(e4, e4) = e1), -(op(e4, e4) = e2), -(op(e4, e4) = e3), -(op(e4, e4) = e4), -(op(e4, e4) = e5), -(op(e4, e4) = e6)], (888 ^ _96822) ^ [] : [-(op(e4, e5) = e0), -(op(e4, e5) = e1), -(op(e4, e5) = e2), -(op(e4, e5) = e3), -(op(e4, e5) = e4), -(op(e4, e5) = e5), -(op(e4, e5) = e6)], (914 ^ _96822) ^ [] : [-(op(e4, e6) = e0), -(op(e4, e6) = e1), -(op(e4, e6) = e2), -(op(e4, e6) = e3), -(op(e4, e6) = e4), -(op(e4, e6) = e5), -(op(e4, e6) = e6)], (940 ^ _96822) ^ [] : [-(op(e5, e0) = e0), -(op(e5, e0) = e1), -(op(e5, e0) = e2), -(op(e5, e0) = e3), -(op(e5, e0) = e4), -(op(e5, e0) = e5), -(op(e5, e0) = e6)], (966 ^ _96822) ^ [] : [-(op(e5, e1) = e0), -(op(e5, e1) = e1), -(op(e5, e1) = e2), -(op(e5, e1) = e3), -(op(e5, e1) = e4), -(op(e5, e1) = e5), -(op(e5, e1) = e6)], (992 ^ _96822) ^ [] : [-(op(e5, e2) = e0), -(op(e5, e2) = e1), -(op(e5, e2) = e2), -(op(e5, e2) = e3), -(op(e5, e2) = e4), -(op(e5, e2) = e5), -(op(e5, e2) = e6)], (1018 ^ _96822) ^ [] : [-(op(e5, e3) = e0), -(op(e5, e3) = e1), -(op(e5, e3) = e2), -(op(e5, e3) = e3), -(op(e5, e3) = e4), -(op(e5, e3) = e5), -(op(e5, e3) = e6)], (1044 ^ _96822) ^ [] : [-(op(e5, e4) = e0), -(op(e5, e4) = e1), -(op(e5, e4) = e2), -(op(e5, e4) = e3), -(op(e5, e4) = e4), -(op(e5, e4) = e5), -(op(e5, e4) = e6)], (1070 ^ _96822) ^ [] : [-(op(e5, e5) = e0), -(op(e5, e5) = e1), -(op(e5, e5) = e2), -(op(e5, e5) = e3), -(op(e5, e5) = e4), -(op(e5, e5) = e5), -(op(e5, e5) = e6)], (1096 ^ _96822) ^ [] : [-(op(e5, e6) = e0), -(op(e5, e6) = e1), -(op(e5, e6) = e2), -(op(e5, e6) = e3), -(op(e5, e6) = e4), -(op(e5, e6) = e5), -(op(e5, e6) = e6)], (1122 ^ _96822) ^ [] : [-(op(e6, e0) = e0), -(op(e6, e0) = e1), -(op(e6, e0) = e2), -(op(e6, e0) = e3), -(op(e6, e0) = e4), -(op(e6, e0) = e5), -(op(e6, e0) = e6)], (1148 ^ _96822) ^ [] : [-(op(e6, e1) = e0), -(op(e6, e1) = e1), -(op(e6, e1) = e2), -(op(e6, e1) = e3), -(op(e6, e1) = e4), -(op(e6, e1) = e5), -(op(e6, e1) = e6)], (1174 ^ _96822) ^ [] : [-(op(e6, e2) = e0), -(op(e6, e2) = e1), -(op(e6, e2) = e2), -(op(e6, e2) = e3), -(op(e6, e2) = e4), -(op(e6, e2) = e5), -(op(e6, e2) = e6)], (1200 ^ _96822) ^ [] : [-(op(e6, e3) = e0), -(op(e6, e3) = e1), -(op(e6, e3) = e2), -(op(e6, e3) = e3), -(op(e6, e3) = e4), -(op(e6, e3) = e5), -(op(e6, e3) = e6)], (1226 ^ _96822) ^ [] : [-(op(e6, e4) = e0), -(op(e6, e4) = e1), -(op(e6, e4) = e2), -(op(e6, e4) = e3), -(op(e6, e4) = e4), -(op(e6, e4) = e5), -(op(e6, e4) = e6)], (1252 ^ _96822) ^ [] : [-(op(e6, e5) = e0), -(op(e6, e5) = e1), -(op(e6, e5) = e2), -(op(e6, e5) = e3), -(op(e6, e5) = e4), -(op(e6, e5) = e5), -(op(e6, e5) = e6)], (1278 ^ _96822) ^ [] : [-(op(e6, e6) = e0), -(op(e6, e6) = e1), -(op(e6, e6) = e2), -(op(e6, e6) = e3), -(op(e6, e6) = e4), -(op(e6, e6) = e5), -(op(e6, e6) = e6)], (3852 ^ _96822) ^ [] : [-(op(op(op(e0, e0), e0), e0) = e0)], (3854 ^ _96822) ^ [] : [-(op(op(op(e1, e0), e1), e1) = e0)], (3856 ^ _96822) ^ [] : [-(op(op(op(e2, e0), e2), e2) = e0)], (3858 ^ _96822) ^ [] : [-(op(op(op(e3, e0), e3), e3) = e0)], (3860 ^ _96822) ^ [] : [-(op(op(op(e4, e0), e4), e4) = e0)], (3862 ^ _96822) ^ [] : [-(op(op(op(e5, e0), e5), e5) = e0)], (3864 ^ _96822) ^ [] : [-(op(op(op(e6, e0), e6), e6) = e0)], (3866 ^ _96822) ^ [] : [-(op(op(op(e0, e1), e0), e0) = e1)], (3868 ^ _96822) ^ [] : [-(op(op(op(e1, e1), e1), e1) = e1)], (3870 ^ _96822) ^ [] : [-(op(op(op(e2, e1), e2), e2) = e1)], (3872 ^ _96822) ^ [] : [-(op(op(op(e3, e1), e3), e3) = e1)], (3874 ^ _96822) ^ [] : [-(op(op(op(e4, e1), e4), e4) = e1)], (3876 ^ _96822) ^ [] : [-(op(op(op(e5, e1), e5), e5) = e1)], (3878 ^ _96822) ^ [] : [-(op(op(op(e6, e1), e6), e6) = e1)], (3880 ^ _96822) ^ [] : [-(op(op(op(e0, e2), e0), e0) = e2)], (3882 ^ _96822) ^ [] : [-(op(op(op(e1, e2), e1), e1) = e2)], (3884 ^ _96822) ^ [] : [-(op(op(op(e2, e2), e2), e2) = e2)], (3886 ^ _96822) ^ [] : [-(op(op(op(e3, e2), e3), e3) = e2)], (3888 ^ _96822) ^ [] : [-(op(op(op(e4, e2), e4), e4) = e2)], (3890 ^ _96822) ^ [] : [-(op(op(op(e5, e2), e5), e5) = e2)], (3892 ^ _96822) ^ [] : [-(op(op(op(e6, e2), e6), e6) = e2)], (3894 ^ _96822) ^ [] : [-(op(op(op(e0, e3), e0), e0) = e3)], (3896 ^ _96822) ^ [] : [-(op(op(op(e1, e3), e1), e1) = e3)], (3898 ^ _96822) ^ [] : [-(op(op(op(e2, e3), e2), e2) = e3)], (3900 ^ _96822) ^ [] : [-(op(op(op(e3, e3), e3), e3) = e3)], (3902 ^ _96822) ^ [] : [-(op(op(op(e4, e3), e4), e4) = e3)], (3904 ^ _96822) ^ [] : [-(op(op(op(e5, e3), e5), e5) = e3)], (3906 ^ _96822) ^ [] : [-(op(op(op(e6, e3), e6), e6) = e3)], (3908 ^ _96822) ^ [] : [-(op(op(op(e0, e4), e0), e0) = e4)], (3910 ^ _96822) ^ [] : [-(op(op(op(e1, e4), e1), e1) = e4)], (3912 ^ _96822) ^ [] : [-(op(op(op(e2, e4), e2), e2) = e4)], (3914 ^ _96822) ^ [] : [-(op(op(op(e3, e4), e3), e3) = e4)], (3916 ^ _96822) ^ [] : [-(op(op(op(e4, e4), e4), e4) = e4)], (3918 ^ _96822) ^ [] : [-(op(op(op(e5, e4), e5), e5) = e4)], (3920 ^ _96822) ^ [] : [-(op(op(op(e6, e4), e6), e6) = e4)], (3922 ^ _96822) ^ [] : [-(op(op(op(e0, e5), e0), e0) = e5)], (3924 ^ _96822) ^ [] : [-(op(op(op(e1, e5), e1), e1) = e5)], (3926 ^ _96822) ^ [] : [-(op(op(op(e2, e5), e2), e2) = e5)], (3928 ^ _96822) ^ [] : [-(op(op(op(e3, e5), e3), e3) = e5)], (3930 ^ _96822) ^ [] : [-(op(op(op(e4, e5), e4), e4) = e5)], (3932 ^ _96822) ^ [] : [-(op(op(op(e5, e5), e5), e5) = e5)], (3934 ^ _96822) ^ [] : [-(op(op(op(e6, e5), e6), e6) = e5)], (3936 ^ _96822) ^ [] : [-(op(op(op(e0, e6), e0), e0) = e6)], (3938 ^ _96822) ^ [] : [-(op(op(op(e1, e6), e1), e1) = e6)], (3940 ^ _96822) ^ [] : [-(op(op(op(e2, e6), e2), e2) = e6)], (3942 ^ _96822) ^ [] : [-(op(op(op(e3, e6), e3), e3) = e6)], (3944 ^ _96822) ^ [] : [-(op(op(op(e4, e6), e4), e4) = e6)], (3946 ^ _96822) ^ [] : [-(op(op(op(e5, e6), e5), e5) = e6)], (3948 ^ _96822) ^ [] : [-(op(op(op(e6, e6), e6), e6) = e6)], (3950 ^ _96822) ^ [] : [op(e0, e0) = op(e1, e0)], (3952 ^ _96822) ^ [] : [op(e0, e0) = op(e2, e0)], (3954 ^ _96822) ^ [] : [op(e0, e0) = op(e3, e0)], (3956 ^ _96822) ^ [] : [op(e0, e0) = op(e4, e0)], (3958 ^ _96822) ^ [] : [op(e0, e0) = op(e5, e0)], (3960 ^ _96822) ^ [] : [op(e0, e0) = op(e6, e0)], (3962 ^ _96822) ^ [] : [op(e1, e0) = op(e2, e0)], (3964 ^ _96822) ^ [] : [op(e1, e0) = op(e3, e0)], (3966 ^ _96822) ^ [] : [op(e1, e0) = op(e4, e0)], (3968 ^ _96822) ^ [] : [op(e1, e0) = op(e5, e0)], (3970 ^ _96822) ^ [] : [op(e1, e0) = op(e6, e0)], (3972 ^ _96822) ^ [] : [op(e2, e0) = op(e3, e0)], (3974 ^ _96822) ^ [] : [op(e2, e0) = op(e4, e0)], (3976 ^ _96822) ^ [] : [op(e2, e0) = op(e5, e0)], (3978 ^ _96822) ^ [] : [op(e2, e0) = op(e6, e0)], (3980 ^ _96822) ^ [] : [op(e3, e0) = op(e4, e0)], (3982 ^ _96822) ^ [] : [op(e3, e0) = op(e5, e0)], (3984 ^ _96822) ^ [] : [op(e3, e0) = op(e6, e0)], (3986 ^ _96822) ^ [] : [op(e4, e0) = op(e5, e0)], (3988 ^ _96822) ^ [] : [op(e4, e0) = op(e6, e0)], (3990 ^ _96822) ^ [] : [op(e5, e0) = op(e6, e0)], (3992 ^ _96822) ^ [] : [op(e0, e1) = op(e1, e1)], (3994 ^ _96822) ^ [] : [op(e0, e1) = op(e2, e1)], (3996 ^ _96822) ^ [] : [op(e0, e1) = op(e3, e1)], (3998 ^ _96822) ^ [] : [op(e0, e1) = op(e4, e1)], (4000 ^ _96822) ^ [] : [op(e0, e1) = op(e5, e1)], (4002 ^ _96822) ^ [] : [op(e0, e1) = op(e6, e1)], (4004 ^ _96822) ^ [] : [op(e1, e1) = op(e2, e1)], (4006 ^ _96822) ^ [] : [op(e1, e1) = op(e3, e1)], (4008 ^ _96822) ^ [] : [op(e1, e1) = op(e4, e1)], (4010 ^ _96822) ^ [] : [op(e1, e1) = op(e5, e1)], (4012 ^ _96822) ^ [] : [op(e1, e1) = op(e6, e1)], (4014 ^ _96822) ^ [] : [op(e2, e1) = op(e3, e1)], (4016 ^ _96822) ^ [] : [op(e2, e1) = op(e4, e1)], (4018 ^ _96822) ^ [] : [op(e2, e1) = op(e5, e1)], (4020 ^ _96822) ^ [] : [op(e2, e1) = op(e6, e1)], (4022 ^ _96822) ^ [] : [op(e3, e1) = op(e4, e1)], (4024 ^ _96822) ^ [] : [op(e3, e1) = op(e5, e1)], (4026 ^ _96822) ^ [] : [op(e3, e1) = op(e6, e1)], (4028 ^ _96822) ^ [] : [op(e4, e1) = op(e5, e1)], (4030 ^ _96822) ^ [] : [op(e4, e1) = op(e6, e1)], (4032 ^ _96822) ^ [] : [op(e5, e1) = op(e6, e1)], (4034 ^ _96822) ^ [] : [op(e0, e2) = op(e1, e2)], (4036 ^ _96822) ^ [] : [op(e0, e2) = op(e2, e2)], (4038 ^ _96822) ^ [] : [op(e0, e2) = op(e3, e2)], (4040 ^ _96822) ^ [] : [op(e0, e2) = op(e4, e2)], (4042 ^ _96822) ^ [] : [op(e0, e2) = op(e5, e2)], (4044 ^ _96822) ^ [] : [op(e0, e2) = op(e6, e2)], (4046 ^ _96822) ^ [] : [op(e1, e2) = op(e2, e2)], (4048 ^ _96822) ^ [] : [op(e1, e2) = op(e3, e2)], (4050 ^ _96822) ^ [] : [op(e1, e2) = op(e4, e2)], (4052 ^ _96822) ^ [] : [op(e1, e2) = op(e5, e2)], (4054 ^ _96822) ^ [] : [op(e1, e2) = op(e6, e2)], (4056 ^ _96822) ^ [] : [op(e2, e2) = op(e3, e2)], (4058 ^ _96822) ^ [] : [op(e2, e2) = op(e4, e2)], (4060 ^ _96822) ^ [] : [op(e2, e2) = op(e5, e2)], (4062 ^ _96822) ^ [] : [op(e2, e2) = op(e6, e2)], (4064 ^ _96822) ^ [] : [op(e3, e2) = op(e4, e2)], (4066 ^ _96822) ^ [] : [op(e3, e2) = op(e5, e2)], (4068 ^ _96822) ^ [] : [op(e3, e2) = op(e6, e2)], (4070 ^ _96822) ^ [] : [op(e4, e2) = op(e5, e2)], (4072 ^ _96822) ^ [] : [op(e4, e2) = op(e6, e2)], (4074 ^ _96822) ^ [] : [op(e5, e2) = op(e6, e2)], (4076 ^ _96822) ^ [] : [op(e0, e3) = op(e1, e3)], (4078 ^ _96822) ^ [] : [op(e0, e3) = op(e2, e3)], (4080 ^ _96822) ^ [] : [op(e0, e3) = op(e3, e3)], (4082 ^ _96822) ^ [] : [op(e0, e3) = op(e4, e3)], (4084 ^ _96822) ^ [] : [op(e0, e3) = op(e5, e3)], (4086 ^ _96822) ^ [] : [op(e0, e3) = op(e6, e3)], (4088 ^ _96822) ^ [] : [op(e1, e3) = op(e2, e3)], (4090 ^ _96822) ^ [] : [op(e1, e3) = op(e3, e3)], (4092 ^ _96822) ^ [] : [op(e1, e3) = op(e4, e3)], (4094 ^ _96822) ^ [] : [op(e1, e3) = op(e5, e3)], (4096 ^ _96822) ^ [] : [op(e1, e3) = op(e6, e3)], (4098 ^ _96822) ^ [] : [op(e2, e3) = op(e3, e3)], (4100 ^ _96822) ^ [] : [op(e2, e3) = op(e4, e3)], (4102 ^ _96822) ^ [] : [op(e2, e3) = op(e5, e3)], (4104 ^ _96822) ^ [] : [op(e2, e3) = op(e6, e3)], (4106 ^ _96822) ^ [] : [op(e3, e3) = op(e4, e3)], (4108 ^ _96822) ^ [] : [op(e3, e3) = op(e5, e3)], (4110 ^ _96822) ^ [] : [op(e3, e3) = op(e6, e3)], (4112 ^ _96822) ^ [] : [op(e4, e3) = op(e5, e3)], (4114 ^ _96822) ^ [] : [op(e4, e3) = op(e6, e3)], (4116 ^ _96822) ^ [] : [op(e5, e3) = op(e6, e3)], (4118 ^ _96822) ^ [] : [op(e0, e4) = op(e1, e4)], (4120 ^ _96822) ^ [] : [op(e0, e4) = op(e2, e4)], (4122 ^ _96822) ^ [] : [op(e0, e4) = op(e3, e4)], (4124 ^ _96822) ^ [] : [op(e0, e4) = op(e4, e4)], (4126 ^ _96822) ^ [] : [op(e0, e4) = op(e5, e4)], (4128 ^ _96822) ^ [] : [op(e0, e4) = op(e6, e4)], (4130 ^ _96822) ^ [] : [op(e1, e4) = op(e2, e4)], (4132 ^ _96822) ^ [] : [op(e1, e4) = op(e3, e4)], (4134 ^ _96822) ^ [] : [op(e1, e4) = op(e4, e4)], (4136 ^ _96822) ^ [] : [op(e1, e4) = op(e5, e4)], (4138 ^ _96822) ^ [] : [op(e1, e4) = op(e6, e4)], (4140 ^ _96822) ^ [] : [op(e2, e4) = op(e3, e4)], (4142 ^ _96822) ^ [] : [op(e2, e4) = op(e4, e4)], (4144 ^ _96822) ^ [] : [op(e2, e4) = op(e5, e4)], (4146 ^ _96822) ^ [] : [op(e2, e4) = op(e6, e4)], (4148 ^ _96822) ^ [] : [op(e3, e4) = op(e4, e4)], (4150 ^ _96822) ^ [] : [op(e3, e4) = op(e5, e4)], (4152 ^ _96822) ^ [] : [op(e3, e4) = op(e6, e4)], (4154 ^ _96822) ^ [] : [op(e4, e4) = op(e5, e4)], (4156 ^ _96822) ^ [] : [op(e4, e4) = op(e6, e4)], (4158 ^ _96822) ^ [] : [op(e5, e4) = op(e6, e4)], (4160 ^ _96822) ^ [] : [op(e0, e5) = op(e1, e5)], (4162 ^ _96822) ^ [] : [op(e0, e5) = op(e2, e5)], (4164 ^ _96822) ^ [] : [op(e0, e5) = op(e3, e5)], (4166 ^ _96822) ^ [] : [op(e0, e5) = op(e4, e5)], (4168 ^ _96822) ^ [] : [op(e0, e5) = op(e5, e5)], (4170 ^ _96822) ^ [] : [op(e0, e5) = op(e6, e5)], (4172 ^ _96822) ^ [] : [op(e1, e5) = op(e2, e5)], (4174 ^ _96822) ^ [] : [op(e1, e5) = op(e3, e5)], (4176 ^ _96822) ^ [] : [op(e1, e5) = op(e4, e5)], (4178 ^ _96822) ^ [] : [op(e1, e5) = op(e5, e5)], (4180 ^ _96822) ^ [] : [op(e1, e5) = op(e6, e5)], (4182 ^ _96822) ^ [] : [op(e2, e5) = op(e3, e5)], (4184 ^ _96822) ^ [] : [op(e2, e5) = op(e4, e5)], (4186 ^ _96822) ^ [] : [op(e2, e5) = op(e5, e5)], (4188 ^ _96822) ^ [] : [op(e2, e5) = op(e6, e5)], (4190 ^ _96822) ^ [] : [op(e3, e5) = op(e4, e5)], (4192 ^ _96822) ^ [] : [op(e3, e5) = op(e5, e5)], (4194 ^ _96822) ^ [] : [op(e3, e5) = op(e6, e5)], (4196 ^ _96822) ^ [] : [op(e4, e5) = op(e5, e5)], (4198 ^ _96822) ^ [] : [op(e4, e5) = op(e6, e5)], (4200 ^ _96822) ^ [] : [op(e5, e5) = op(e6, e5)], (4202 ^ _96822) ^ [] : [op(e0, e6) = op(e1, e6)], (4204 ^ _96822) ^ [] : [op(e0, e6) = op(e2, e6)], (4206 ^ _96822) ^ [] : [op(e0, e6) = op(e3, e6)], (4208 ^ _96822) ^ [] : [op(e0, e6) = op(e4, e6)], (4210 ^ _96822) ^ [] : [op(e0, e6) = op(e5, e6)], (4212 ^ _96822) ^ [] : [op(e0, e6) = op(e6, e6)], (4214 ^ _96822) ^ [] : [op(e1, e6) = op(e2, e6)], (4216 ^ _96822) ^ [] : [op(e1, e6) = op(e3, e6)], (4218 ^ _96822) ^ [] : [op(e1, e6) = op(e4, e6)], (4220 ^ _96822) ^ [] : [op(e1, e6) = op(e5, e6)], (4222 ^ _96822) ^ [] : [op(e1, e6) = op(e6, e6)], (4224 ^ _96822) ^ [] : [op(e2, e6) = op(e3, e6)], (4226 ^ _96822) ^ [] : [op(e2, e6) = op(e4, e6)], (4228 ^ _96822) ^ [] : [op(e2, e6) = op(e5, e6)], (4230 ^ _96822) ^ [] : [op(e2, e6) = op(e6, e6)], (4232 ^ _96822) ^ [] : [op(e3, e6) = op(e4, e6)], (4234 ^ _96822) ^ [] : [op(e3, e6) = op(e5, e6)], (4236 ^ _96822) ^ [] : [op(e3, e6) = op(e6, e6)], (4238 ^ _96822) ^ [] : [op(e4, e6) = op(e5, e6)], (4240 ^ _96822) ^ [] : [op(e4, e6) = op(e6, e6)], (4242 ^ _96822) ^ [] : [op(e5, e6) = op(e6, e6)], (4244 ^ _96822) ^ [] : [op(e0, e0) = op(e0, e1)], (4246 ^ _96822) ^ [] : [op(e0, e0) = op(e0, e2)], (4248 ^ _96822) ^ [] : [op(e0, e0) = op(e0, e3)], (4250 ^ _96822) ^ [] : [op(e0, e0) = op(e0, e4)], (4252 ^ _96822) ^ [] : [op(e0, e0) = op(e0, e5)], (4254 ^ _96822) ^ [] : [op(e0, e0) = op(e0, e6)], (4256 ^ _96822) ^ [] : [op(e0, e1) = op(e0, e2)], (4258 ^ _96822) ^ [] : [op(e0, e1) = op(e0, e3)], (4260 ^ _96822) ^ [] : [op(e0, e1) = op(e0, e4)], (4262 ^ _96822) ^ [] : [op(e0, e1) = op(e0, e5)], (4264 ^ _96822) ^ [] : [op(e0, e1) = op(e0, e6)], (4266 ^ _96822) ^ [] : [op(e0, e2) = op(e0, e3)], (4268 ^ _96822) ^ [] : [op(e0, e2) = op(e0, e4)], (4270 ^ _96822) ^ [] : [op(e0, e2) = op(e0, e5)], (4272 ^ _96822) ^ [] : [op(e0, e2) = op(e0, e6)], (4274 ^ _96822) ^ [] : [op(e0, e3) = op(e0, e4)], (4276 ^ _96822) ^ [] : [op(e0, e3) = op(e0, e5)], (4278 ^ _96822) ^ [] : [op(e0, e3) = op(e0, e6)], (4280 ^ _96822) ^ [] : [op(e0, e4) = op(e0, e5)], (4282 ^ _96822) ^ [] : [op(e0, e4) = op(e0, e6)], (4284 ^ _96822) ^ [] : [op(e0, e5) = op(e0, e6)], (4286 ^ _96822) ^ [] : [op(e1, e0) = op(e1, e1)], (4288 ^ _96822) ^ [] : [op(e1, e0) = op(e1, e2)], (4290 ^ _96822) ^ [] : [op(e1, e0) = op(e1, e3)], (4292 ^ _96822) ^ [] : [op(e1, e0) = op(e1, e4)], (4294 ^ _96822) ^ [] : [op(e1, e0) = op(e1, e5)], (4296 ^ _96822) ^ [] : [op(e1, e0) = op(e1, e6)], (4298 ^ _96822) ^ [] : [op(e1, e1) = op(e1, e2)], (4300 ^ _96822) ^ [] : [op(e1, e1) = op(e1, e3)], (4302 ^ _96822) ^ [] : [op(e1, e1) = op(e1, e4)], (4304 ^ _96822) ^ [] : [op(e1, e1) = op(e1, e5)], (4306 ^ _96822) ^ [] : [op(e1, e1) = op(e1, e6)], (4308 ^ _96822) ^ [] : [op(e1, e2) = op(e1, e3)], (4310 ^ _96822) ^ [] : [op(e1, e2) = op(e1, e4)], (4312 ^ _96822) ^ [] : [op(e1, e2) = op(e1, e5)], (4314 ^ _96822) ^ [] : [op(e1, e2) = op(e1, e6)], (4316 ^ _96822) ^ [] : [op(e1, e3) = op(e1, e4)], (4318 ^ _96822) ^ [] : [op(e1, e3) = op(e1, e5)], (4320 ^ _96822) ^ [] : [op(e1, e3) = op(e1, e6)], (4322 ^ _96822) ^ [] : [op(e1, e4) = op(e1, e5)], (4324 ^ _96822) ^ [] : [op(e1, e4) = op(e1, e6)], (4326 ^ _96822) ^ [] : [op(e1, e5) = op(e1, e6)], (4328 ^ _96822) ^ [] : [op(e2, e0) = op(e2, e1)], (4330 ^ _96822) ^ [] : [op(e2, e0) = op(e2, e2)], (4332 ^ _96822) ^ [] : [op(e2, e0) = op(e2, e3)], (4334 ^ _96822) ^ [] : [op(e2, e0) = op(e2, e4)], (4336 ^ _96822) ^ [] : [op(e2, e0) = op(e2, e5)], (4338 ^ _96822) ^ [] : [op(e2, e0) = op(e2, e6)], (4340 ^ _96822) ^ [] : [op(e2, e1) = op(e2, e2)], (4342 ^ _96822) ^ [] : [op(e2, e1) = op(e2, e3)], (4344 ^ _96822) ^ [] : [op(e2, e1) = op(e2, e4)], (4346 ^ _96822) ^ [] : [op(e2, e1) = op(e2, e5)], (4348 ^ _96822) ^ [] : [op(e2, e1) = op(e2, e6)], (4350 ^ _96822) ^ [] : [op(e2, e2) = op(e2, e3)], (4352 ^ _96822) ^ [] : [op(e2, e2) = op(e2, e4)], (4354 ^ _96822) ^ [] : [op(e2, e2) = op(e2, e5)], (4356 ^ _96822) ^ [] : [op(e2, e2) = op(e2, e6)], (4358 ^ _96822) ^ [] : [op(e2, e3) = op(e2, e4)], (4360 ^ _96822) ^ [] : [op(e2, e3) = op(e2, e5)], (4362 ^ _96822) ^ [] : [op(e2, e3) = op(e2, e6)], (4364 ^ _96822) ^ [] : [op(e2, e4) = op(e2, e5)], (4366 ^ _96822) ^ [] : [op(e2, e4) = op(e2, e6)], (4368 ^ _96822) ^ [] : [op(e2, e5) = op(e2, e6)], (4370 ^ _96822) ^ [] : [op(e3, e0) = op(e3, e1)], (4372 ^ _96822) ^ [] : [op(e3, e0) = op(e3, e2)], (4374 ^ _96822) ^ [] : [op(e3, e0) = op(e3, e3)], (4376 ^ _96822) ^ [] : [op(e3, e0) = op(e3, e4)], (4378 ^ _96822) ^ [] : [op(e3, e0) = op(e3, e5)], (4380 ^ _96822) ^ [] : [op(e3, e0) = op(e3, e6)], (4382 ^ _96822) ^ [] : [op(e3, e1) = op(e3, e2)], (4384 ^ _96822) ^ [] : [op(e3, e1) = op(e3, e3)], (4386 ^ _96822) ^ [] : [op(e3, e1) = op(e3, e4)], (4388 ^ _96822) ^ [] : [op(e3, e1) = op(e3, e5)], (4390 ^ _96822) ^ [] : [op(e3, e1) = op(e3, e6)], (4392 ^ _96822) ^ [] : [op(e3, e2) = op(e3, e3)], (4394 ^ _96822) ^ [] : [op(e3, e2) = op(e3, e4)], (4396 ^ _96822) ^ [] : [op(e3, e2) = op(e3, e5)], (4398 ^ _96822) ^ [] : [op(e3, e2) = op(e3, e6)], (4400 ^ _96822) ^ [] : [op(e3, e3) = op(e3, e4)], (4402 ^ _96822) ^ [] : [op(e3, e3) = op(e3, e5)], (4404 ^ _96822) ^ [] : [op(e3, e3) = op(e3, e6)], (4406 ^ _96822) ^ [] : [op(e3, e4) = op(e3, e5)], (4408 ^ _96822) ^ [] : [op(e3, e4) = op(e3, e6)], (4410 ^ _96822) ^ [] : [op(e3, e5) = op(e3, e6)], (4412 ^ _96822) ^ [] : [op(e4, e0) = op(e4, e1)], (4414 ^ _96822) ^ [] : [op(e4, e0) = op(e4, e2)], (4416 ^ _96822) ^ [] : [op(e4, e0) = op(e4, e3)], (4418 ^ _96822) ^ [] : [op(e4, e0) = op(e4, e4)], (4420 ^ _96822) ^ [] : [op(e4, e0) = op(e4, e5)], (4422 ^ _96822) ^ [] : [op(e4, e0) = op(e4, e6)], (4424 ^ _96822) ^ [] : [op(e4, e1) = op(e4, e2)], (4426 ^ _96822) ^ [] : [op(e4, e1) = op(e4, e3)], (4428 ^ _96822) ^ [] : [op(e4, e1) = op(e4, e4)], (4430 ^ _96822) ^ [] : [op(e4, e1) = op(e4, e5)], (4432 ^ _96822) ^ [] : [op(e4, e1) = op(e4, e6)], (4434 ^ _96822) ^ [] : [op(e4, e2) = op(e4, e3)], (4436 ^ _96822) ^ [] : [op(e4, e2) = op(e4, e4)], (4438 ^ _96822) ^ [] : [op(e4, e2) = op(e4, e5)], (4440 ^ _96822) ^ [] : [op(e4, e2) = op(e4, e6)], (4442 ^ _96822) ^ [] : [op(e4, e3) = op(e4, e4)], (4444 ^ _96822) ^ [] : [op(e4, e3) = op(e4, e5)], (4446 ^ _96822) ^ [] : [op(e4, e3) = op(e4, e6)], (4448 ^ _96822) ^ [] : [op(e4, e4) = op(e4, e5)], (4450 ^ _96822) ^ [] : [op(e4, e4) = op(e4, e6)], (4452 ^ _96822) ^ [] : [op(e4, e5) = op(e4, e6)], (4454 ^ _96822) ^ [] : [op(e5, e0) = op(e5, e1)], (4456 ^ _96822) ^ [] : [op(e5, e0) = op(e5, e2)], (4458 ^ _96822) ^ [] : [op(e5, e0) = op(e5, e3)], (4460 ^ _96822) ^ [] : [op(e5, e0) = op(e5, e4)], (4462 ^ _96822) ^ [] : [op(e5, e0) = op(e5, e5)], (4464 ^ _96822) ^ [] : [op(e5, e0) = op(e5, e6)], (4466 ^ _96822) ^ [] : [op(e5, e1) = op(e5, e2)], (4468 ^ _96822) ^ [] : [op(e5, e1) = op(e5, e3)], (4470 ^ _96822) ^ [] : [op(e5, e1) = op(e5, e4)], (4472 ^ _96822) ^ [] : [op(e5, e1) = op(e5, e5)], (4474 ^ _96822) ^ [] : [op(e5, e1) = op(e5, e6)], (4476 ^ _96822) ^ [] : [op(e5, e2) = op(e5, e3)], (4478 ^ _96822) ^ [] : [op(e5, e2) = op(e5, e4)], (4480 ^ _96822) ^ [] : [op(e5, e2) = op(e5, e5)], (4482 ^ _96822) ^ [] : [op(e5, e2) = op(e5, e6)], (4484 ^ _96822) ^ [] : [op(e5, e3) = op(e5, e4)], (4486 ^ _96822) ^ [] : [op(e5, e3) = op(e5, e5)], (4488 ^ _96822) ^ [] : [op(e5, e3) = op(e5, e6)], (4490 ^ _96822) ^ [] : [op(e5, e4) = op(e5, e5)], (4492 ^ _96822) ^ [] : [op(e5, e4) = op(e5, e6)], (4494 ^ _96822) ^ [] : [op(e5, e5) = op(e5, e6)], (4496 ^ _96822) ^ [] : [op(e6, e0) = op(e6, e1)], (4498 ^ _96822) ^ [] : [op(e6, e0) = op(e6, e2)], (4500 ^ _96822) ^ [] : [op(e6, e0) = op(e6, e3)], (4502 ^ _96822) ^ [] : [op(e6, e0) = op(e6, e4)], (4504 ^ _96822) ^ [] : [op(e6, e0) = op(e6, e5)], (4506 ^ _96822) ^ [] : [op(e6, e0) = op(e6, e6)], (4508 ^ _96822) ^ [] : [op(e6, e1) = op(e6, e2)], (4510 ^ _96822) ^ [] : [op(e6, e1) = op(e6, e3)], (4512 ^ _96822) ^ [] : [op(e6, e1) = op(e6, e4)], (4514 ^ _96822) ^ [] : [op(e6, e1) = op(e6, e5)], (4516 ^ _96822) ^ [] : [op(e6, e1) = op(e6, e6)], (4518 ^ _96822) ^ [] : [op(e6, e2) = op(e6, e3)], (4520 ^ _96822) ^ [] : [op(e6, e2) = op(e6, e4)], (4522 ^ _96822) ^ [] : [op(e6, e2) = op(e6, e5)], (4524 ^ _96822) ^ [] : [op(e6, e2) = op(e6, e6)], (4526 ^ _96822) ^ [] : [op(e6, e3) = op(e6, e4)], (4528 ^ _96822) ^ [] : [op(e6, e3) = op(e6, e5)], (4530 ^ _96822) ^ [] : [op(e6, e3) = op(e6, e6)], (4532 ^ _96822) ^ [] : [op(e6, e4) = op(e6, e5)], (4534 ^ _96822) ^ [] : [op(e6, e4) = op(e6, e6)], (4536 ^ _96822) ^ [] : [op(e6, e5) = op(e6, e6)], (4538 ^ _96822) ^ [] : [e0 = e1], (4540 ^ _96822) ^ [] : [e0 = e2], (4542 ^ _96822) ^ [] : [e0 = e3], (4544 ^ _96822) ^ [] : [e0 = e4], (4546 ^ _96822) ^ [] : [e0 = e5], (4548 ^ _96822) ^ [] : [e0 = e6], (4550 ^ _96822) ^ [] : [e1 = e2], (4552 ^ _96822) ^ [] : [e1 = e3], (4554 ^ _96822) ^ [] : [e1 = e4], (4556 ^ _96822) ^ [] : [e1 = e5], (4558 ^ _96822) ^ [] : [e1 = e6], (4560 ^ _96822) ^ [] : [e2 = e3], (4562 ^ _96822) ^ [] : [e2 = e4], (4564 ^ _96822) ^ [] : [e2 = e5], (4566 ^ _96822) ^ [] : [e2 = e6], (4568 ^ _96822) ^ [] : [e3 = e4], (4570 ^ _96822) ^ [] : [e3 = e5], (4572 ^ _96822) ^ [] : [e3 = e6], (4574 ^ _96822) ^ [] : [e4 = e5], (4576 ^ _96822) ^ [] : [e4 = e6], (4578 ^ _96822) ^ [] : [e5 = e6], (1304 ^ _96822) ^ [] : [-(op(e0, e0) = e0), -(op(e0, e1) = e0), -(op(e0, e2) = e0), -(op(e0, e3) = e0), -(op(e0, e4) = e0), -(op(e0, e5) = e0), -(op(e0, e6) = e0)], (1330 ^ _96822) ^ [] : [-(op(e0, e0) = e0), -(op(e1, e0) = e0), -(op(e2, e0) = e0), -(op(e3, e0) = e0), -(op(e4, e0) = e0), -(op(e5, e0) = e0), -(op(e6, e0) = e0)], (1356 ^ _96822) ^ [] : [-(op(e0, e0) = e1), -(op(e0, e1) = e1), -(op(e0, e2) = e1), -(op(e0, e3) = e1), -(op(e0, e4) = e1), -(op(e0, e5) = e1), -(op(e0, e6) = e1)], (1382 ^ _96822) ^ [] : [-(op(e0, e0) = e1), -(op(e1, e0) = e1), -(op(e2, e0) = e1), -(op(e3, e0) = e1), -(op(e4, e0) = e1), -(op(e5, e0) = e1), -(op(e6, e0) = e1)], (1408 ^ _96822) ^ [] : [-(op(e0, e0) = e2), -(op(e0, e1) = e2), -(op(e0, e2) = e2), -(op(e0, e3) = e2), -(op(e0, e4) = e2), -(op(e0, e5) = e2), -(op(e0, e6) = e2)], (1434 ^ _96822) ^ [] : [-(op(e0, e0) = e2), -(op(e1, e0) = e2), -(op(e2, e0) = e2), -(op(e3, e0) = e2), -(op(e4, e0) = e2), -(op(e5, e0) = e2), -(op(e6, e0) = e2)], (1460 ^ _96822) ^ [] : [-(op(e0, e0) = e3), -(op(e0, e1) = e3), -(op(e0, e2) = e3), -(op(e0, e3) = e3), -(op(e0, e4) = e3), -(op(e0, e5) = e3), -(op(e0, e6) = e3)], (1486 ^ _96822) ^ [] : [-(op(e0, e0) = e3), -(op(e1, e0) = e3), -(op(e2, e0) = e3), -(op(e3, e0) = e3), -(op(e4, e0) = e3), -(op(e5, e0) = e3), -(op(e6, e0) = e3)], (1512 ^ _96822) ^ [] : [-(op(e0, e0) = e4), -(op(e0, e1) = e4), -(op(e0, e2) = e4), -(op(e0, e3) = e4), -(op(e0, e4) = e4), -(op(e0, e5) = e4), -(op(e0, e6) = e4)], (1538 ^ _96822) ^ [] : [-(op(e0, e0) = e4), -(op(e1, e0) = e4), -(op(e2, e0) = e4), -(op(e3, e0) = e4), -(op(e4, e0) = e4), -(op(e5, e0) = e4), -(op(e6, e0) = e4)], (1564 ^ _96822) ^ [] : [-(op(e0, e0) = e5), -(op(e0, e1) = e5), -(op(e0, e2) = e5), -(op(e0, e3) = e5), -(op(e0, e4) = e5), -(op(e0, e5) = e5), -(op(e0, e6) = e5)], (1590 ^ _96822) ^ [] : [-(op(e0, e0) = e5), -(op(e1, e0) = e5), -(op(e2, e0) = e5), -(op(e3, e0) = e5), -(op(e4, e0) = e5), -(op(e5, e0) = e5), -(op(e6, e0) = e5)], (1616 ^ _96822) ^ [] : [-(op(e0, e0) = e6), -(op(e0, e1) = e6), -(op(e0, e2) = e6), -(op(e0, e3) = e6), -(op(e0, e4) = e6), -(op(e0, e5) = e6), -(op(e0, e6) = e6)], (1642 ^ _96822) ^ [] : [-(op(e0, e0) = e6), -(op(e1, e0) = e6), -(op(e2, e0) = e6), -(op(e3, e0) = e6), -(op(e4, e0) = e6), -(op(e5, e0) = e6), -(op(e6, e0) = e6)], (1668 ^ _96822) ^ [] : [-(op(e1, e0) = e0), -(op(e1, e1) = e0), -(op(e1, e2) = e0), -(op(e1, e3) = e0), -(op(e1, e4) = e0), -(op(e1, e5) = e0), -(op(e1, e6) = e0)], (1694 ^ _96822) ^ [] : [-(op(e0, e1) = e0), -(op(e1, e1) = e0), -(op(e2, e1) = e0), -(op(e3, e1) = e0), -(op(e4, e1) = e0), -(op(e5, e1) = e0), -(op(e6, e1) = e0)], (1720 ^ _96822) ^ [] : [-(op(e1, e0) = e1), -(op(e1, e1) = e1), -(op(e1, e2) = e1), -(op(e1, e3) = e1), -(op(e1, e4) = e1), -(op(e1, e5) = e1), -(op(e1, e6) = e1)], (1746 ^ _96822) ^ [] : [-(op(e0, e1) = e1), -(op(e1, e1) = e1), -(op(e2, e1) = e1), -(op(e3, e1) = e1), -(op(e4, e1) = e1), -(op(e5, e1) = e1), -(op(e6, e1) = e1)], (1772 ^ _96822) ^ [] : [-(op(e1, e0) = e2), -(op(e1, e1) = e2), -(op(e1, e2) = e2), -(op(e1, e3) = e2), -(op(e1, e4) = e2), -(op(e1, e5) = e2), -(op(e1, e6) = e2)], (1798 ^ _96822) ^ [] : [-(op(e0, e1) = e2), -(op(e1, e1) = e2), -(op(e2, e1) = e2), -(op(e3, e1) = e2), -(op(e4, e1) = e2), -(op(e5, e1) = e2), -(op(e6, e1) = e2)], (1824 ^ _96822) ^ [] : [-(op(e1, e0) = e3), -(op(e1, e1) = e3), -(op(e1, e2) = e3), -(op(e1, e3) = e3), -(op(e1, e4) = e3), -(op(e1, e5) = e3), -(op(e1, e6) = e3)], (1850 ^ _96822) ^ [] : [-(op(e0, e1) = e3), -(op(e1, e1) = e3), -(op(e2, e1) = e3), -(op(e3, e1) = e3), -(op(e4, e1) = e3), -(op(e5, e1) = e3), -(op(e6, e1) = e3)], (1876 ^ _96822) ^ [] : [-(op(e1, e0) = e4), -(op(e1, e1) = e4), -(op(e1, e2) = e4), -(op(e1, e3) = e4), -(op(e1, e4) = e4), -(op(e1, e5) = e4), -(op(e1, e6) = e4)], (1902 ^ _96822) ^ [] : [-(op(e0, e1) = e4), -(op(e1, e1) = e4), -(op(e2, e1) = e4), -(op(e3, e1) = e4), -(op(e4, e1) = e4), -(op(e5, e1) = e4), -(op(e6, e1) = e4)], (1928 ^ _96822) ^ [] : [-(op(e1, e0) = e5), -(op(e1, e1) = e5), -(op(e1, e2) = e5), -(op(e1, e3) = e5), -(op(e1, e4) = e5), -(op(e1, e5) = e5), -(op(e1, e6) = e5)], (1954 ^ _96822) ^ [] : [-(op(e0, e1) = e5), -(op(e1, e1) = e5), -(op(e2, e1) = e5), -(op(e3, e1) = e5), -(op(e4, e1) = e5), -(op(e5, e1) = e5), -(op(e6, e1) = e5)], (1980 ^ _96822) ^ [] : [-(op(e1, e0) = e6), -(op(e1, e1) = e6), -(op(e1, e2) = e6), -(op(e1, e3) = e6), -(op(e1, e4) = e6), -(op(e1, e5) = e6), -(op(e1, e6) = e6)], (2006 ^ _96822) ^ [] : [-(op(e0, e1) = e6), -(op(e1, e1) = e6), -(op(e2, e1) = e6), -(op(e3, e1) = e6), -(op(e4, e1) = e6), -(op(e5, e1) = e6), -(op(e6, e1) = e6)], (2032 ^ _96822) ^ [] : [-(op(e2, e0) = e0), -(op(e2, e1) = e0), -(op(e2, e2) = e0), -(op(e2, e3) = e0), -(op(e2, e4) = e0), -(op(e2, e5) = e0), -(op(e2, e6) = e0)], (2058 ^ _96822) ^ [] : [-(op(e0, e2) = e0), -(op(e1, e2) = e0), -(op(e2, e2) = e0), -(op(e3, e2) = e0), -(op(e4, e2) = e0), -(op(e5, e2) = e0), -(op(e6, e2) = e0)], (2084 ^ _96822) ^ [] : [-(op(e2, e0) = e1), -(op(e2, e1) = e1), -(op(e2, e2) = e1), -(op(e2, e3) = e1), -(op(e2, e4) = e1), -(op(e2, e5) = e1), -(op(e2, e6) = e1)], (2110 ^ _96822) ^ [] : [-(op(e0, e2) = e1), -(op(e1, e2) = e1), -(op(e2, e2) = e1), -(op(e3, e2) = e1), -(op(e4, e2) = e1), -(op(e5, e2) = e1), -(op(e6, e2) = e1)], (2136 ^ _96822) ^ [] : [-(op(e2, e0) = e2), -(op(e2, e1) = e2), -(op(e2, e2) = e2), -(op(e2, e3) = e2), -(op(e2, e4) = e2), -(op(e2, e5) = e2), -(op(e2, e6) = e2)], (2162 ^ _96822) ^ [] : [-(op(e0, e2) = e2), -(op(e1, e2) = e2), -(op(e2, e2) = e2), -(op(e3, e2) = e2), -(op(e4, e2) = e2), -(op(e5, e2) = e2), -(op(e6, e2) = e2)], (2188 ^ _96822) ^ [] : [-(op(e2, e0) = e3), -(op(e2, e1) = e3), -(op(e2, e2) = e3), -(op(e2, e3) = e3), -(op(e2, e4) = e3), -(op(e2, e5) = e3), -(op(e2, e6) = e3)], (2214 ^ _96822) ^ [] : [-(op(e0, e2) = e3), -(op(e1, e2) = e3), -(op(e2, e2) = e3), -(op(e3, e2) = e3), -(op(e4, e2) = e3), -(op(e5, e2) = e3), -(op(e6, e2) = e3)], (2240 ^ _96822) ^ [] : [-(op(e2, e0) = e4), -(op(e2, e1) = e4), -(op(e2, e2) = e4), -(op(e2, e3) = e4), -(op(e2, e4) = e4), -(op(e2, e5) = e4), -(op(e2, e6) = e4)], (2266 ^ _96822) ^ [] : [-(op(e0, e2) = e4), -(op(e1, e2) = e4), -(op(e2, e2) = e4), -(op(e3, e2) = e4), -(op(e4, e2) = e4), -(op(e5, e2) = e4), -(op(e6, e2) = e4)], (2292 ^ _96822) ^ [] : [-(op(e2, e0) = e5), -(op(e2, e1) = e5), -(op(e2, e2) = e5), -(op(e2, e3) = e5), -(op(e2, e4) = e5), -(op(e2, e5) = e5), -(op(e2, e6) = e5)], (2318 ^ _96822) ^ [] : [-(op(e0, e2) = e5), -(op(e1, e2) = e5), -(op(e2, e2) = e5), -(op(e3, e2) = e5), -(op(e4, e2) = e5), -(op(e5, e2) = e5), -(op(e6, e2) = e5)], (2344 ^ _96822) ^ [] : [-(op(e2, e0) = e6), -(op(e2, e1) = e6), -(op(e2, e2) = e6), -(op(e2, e3) = e6), -(op(e2, e4) = e6), -(op(e2, e5) = e6), -(op(e2, e6) = e6)], (2370 ^ _96822) ^ [] : [-(op(e0, e2) = e6), -(op(e1, e2) = e6), -(op(e2, e2) = e6), -(op(e3, e2) = e6), -(op(e4, e2) = e6), -(op(e5, e2) = e6), -(op(e6, e2) = e6)], (2396 ^ _96822) ^ [] : [-(op(e3, e0) = e0), -(op(e3, e1) = e0), -(op(e3, e2) = e0), -(op(e3, e3) = e0), -(op(e3, e4) = e0), -(op(e3, e5) = e0), -(op(e3, e6) = e0)], (2422 ^ _96822) ^ [] : [-(op(e0, e3) = e0), -(op(e1, e3) = e0), -(op(e2, e3) = e0), -(op(e3, e3) = e0), -(op(e4, e3) = e0), -(op(e5, e3) = e0), -(op(e6, e3) = e0)], (2448 ^ _96822) ^ [] : [-(op(e3, e0) = e1), -(op(e3, e1) = e1), -(op(e3, e2) = e1), -(op(e3, e3) = e1), -(op(e3, e4) = e1), -(op(e3, e5) = e1), -(op(e3, e6) = e1)], (2474 ^ _96822) ^ [] : [-(op(e0, e3) = e1), -(op(e1, e3) = e1), -(op(e2, e3) = e1), -(op(e3, e3) = e1), -(op(e4, e3) = e1), -(op(e5, e3) = e1), -(op(e6, e3) = e1)], (2500 ^ _96822) ^ [] : [-(op(e3, e0) = e2), -(op(e3, e1) = e2), -(op(e3, e2) = e2), -(op(e3, e3) = e2), -(op(e3, e4) = e2), -(op(e3, e5) = e2), -(op(e3, e6) = e2)], (2526 ^ _96822) ^ [] : [-(op(e0, e3) = e2), -(op(e1, e3) = e2), -(op(e2, e3) = e2), -(op(e3, e3) = e2), -(op(e4, e3) = e2), -(op(e5, e3) = e2), -(op(e6, e3) = e2)], (2552 ^ _96822) ^ [] : [-(op(e3, e0) = e3), -(op(e3, e1) = e3), -(op(e3, e2) = e3), -(op(e3, e3) = e3), -(op(e3, e4) = e3), -(op(e3, e5) = e3), -(op(e3, e6) = e3)], (2578 ^ _96822) ^ [] : [-(op(e0, e3) = e3), -(op(e1, e3) = e3), -(op(e2, e3) = e3), -(op(e3, e3) = e3), -(op(e4, e3) = e3), -(op(e5, e3) = e3), -(op(e6, e3) = e3)], (2604 ^ _96822) ^ [] : [-(op(e3, e0) = e4), -(op(e3, e1) = e4), -(op(e3, e2) = e4), -(op(e3, e3) = e4), -(op(e3, e4) = e4), -(op(e3, e5) = e4), -(op(e3, e6) = e4)], (2630 ^ _96822) ^ [] : [-(op(e0, e3) = e4), -(op(e1, e3) = e4), -(op(e2, e3) = e4), -(op(e3, e3) = e4), -(op(e4, e3) = e4), -(op(e5, e3) = e4), -(op(e6, e3) = e4)], (2656 ^ _96822) ^ [] : [-(op(e3, e0) = e5), -(op(e3, e1) = e5), -(op(e3, e2) = e5), -(op(e3, e3) = e5), -(op(e3, e4) = e5), -(op(e3, e5) = e5), -(op(e3, e6) = e5)], (2682 ^ _96822) ^ [] : [-(op(e0, e3) = e5), -(op(e1, e3) = e5), -(op(e2, e3) = e5), -(op(e3, e3) = e5), -(op(e4, e3) = e5), -(op(e5, e3) = e5), -(op(e6, e3) = e5)], (2708 ^ _96822) ^ [] : [-(op(e3, e0) = e6), -(op(e3, e1) = e6), -(op(e3, e2) = e6), -(op(e3, e3) = e6), -(op(e3, e4) = e6), -(op(e3, e5) = e6), -(op(e3, e6) = e6)], (2734 ^ _96822) ^ [] : [-(op(e0, e3) = e6), -(op(e1, e3) = e6), -(op(e2, e3) = e6), -(op(e3, e3) = e6), -(op(e4, e3) = e6), -(op(e5, e3) = e6), -(op(e6, e3) = e6)], (2760 ^ _96822) ^ [] : [-(op(e4, e0) = e0), -(op(e4, e1) = e0), -(op(e4, e2) = e0), -(op(e4, e3) = e0), -(op(e4, e4) = e0), -(op(e4, e5) = e0), -(op(e4, e6) = e0)], (2786 ^ _96822) ^ [] : [-(op(e0, e4) = e0), -(op(e1, e4) = e0), -(op(e2, e4) = e0), -(op(e3, e4) = e0), -(op(e4, e4) = e0), -(op(e5, e4) = e0), -(op(e6, e4) = e0)], (2812 ^ _96822) ^ [] : [-(op(e4, e0) = e1), -(op(e4, e1) = e1), -(op(e4, e2) = e1), -(op(e4, e3) = e1), -(op(e4, e4) = e1), -(op(e4, e5) = e1), -(op(e4, e6) = e1)], (2838 ^ _96822) ^ [] : [-(op(e0, e4) = e1), -(op(e1, e4) = e1), -(op(e2, e4) = e1), -(op(e3, e4) = e1), -(op(e4, e4) = e1), -(op(e5, e4) = e1), -(op(e6, e4) = e1)], (2864 ^ _96822) ^ [] : [-(op(e4, e0) = e2), -(op(e4, e1) = e2), -(op(e4, e2) = e2), -(op(e4, e3) = e2), -(op(e4, e4) = e2), -(op(e4, e5) = e2), -(op(e4, e6) = e2)], (2890 ^ _96822) ^ [] : [-(op(e0, e4) = e2), -(op(e1, e4) = e2), -(op(e2, e4) = e2), -(op(e3, e4) = e2), -(op(e4, e4) = e2), -(op(e5, e4) = e2), -(op(e6, e4) = e2)], (2916 ^ _96822) ^ [] : [-(op(e4, e0) = e3), -(op(e4, e1) = e3), -(op(e4, e2) = e3), -(op(e4, e3) = e3), -(op(e4, e4) = e3), -(op(e4, e5) = e3), -(op(e4, e6) = e3)], (2942 ^ _96822) ^ [] : [-(op(e0, e4) = e3), -(op(e1, e4) = e3), -(op(e2, e4) = e3), -(op(e3, e4) = e3), -(op(e4, e4) = e3), -(op(e5, e4) = e3), -(op(e6, e4) = e3)], (2968 ^ _96822) ^ [] : [-(op(e4, e0) = e4), -(op(e4, e1) = e4), -(op(e4, e2) = e4), -(op(e4, e3) = e4), -(op(e4, e4) = e4), -(op(e4, e5) = e4), -(op(e4, e6) = e4)], (2994 ^ _96822) ^ [] : [-(op(e0, e4) = e4), -(op(e1, e4) = e4), -(op(e2, e4) = e4), -(op(e3, e4) = e4), -(op(e4, e4) = e4), -(op(e5, e4) = e4), -(op(e6, e4) = e4)], (3020 ^ _96822) ^ [] : [-(op(e4, e0) = e5), -(op(e4, e1) = e5), -(op(e4, e2) = e5), -(op(e4, e3) = e5), -(op(e4, e4) = e5), -(op(e4, e5) = e5), -(op(e4, e6) = e5)], (3046 ^ _96822) ^ [] : [-(op(e0, e4) = e5), -(op(e1, e4) = e5), -(op(e2, e4) = e5), -(op(e3, e4) = e5), -(op(e4, e4) = e5), -(op(e5, e4) = e5), -(op(e6, e4) = e5)], (3072 ^ _96822) ^ [] : [-(op(e4, e0) = e6), -(op(e4, e1) = e6), -(op(e4, e2) = e6), -(op(e4, e3) = e6), -(op(e4, e4) = e6), -(op(e4, e5) = e6), -(op(e4, e6) = e6)], (3098 ^ _96822) ^ [] : [-(op(e0, e4) = e6), -(op(e1, e4) = e6), -(op(e2, e4) = e6), -(op(e3, e4) = e6), -(op(e4, e4) = e6), -(op(e5, e4) = e6), -(op(e6, e4) = e6)], (3124 ^ _96822) ^ [] : [-(op(e5, e0) = e0), -(op(e5, e1) = e0), -(op(e5, e2) = e0), -(op(e5, e3) = e0), -(op(e5, e4) = e0), -(op(e5, e5) = e0), -(op(e5, e6) = e0)], (3150 ^ _96822) ^ [] : [-(op(e0, e5) = e0), -(op(e1, e5) = e0), -(op(e2, e5) = e0), -(op(e3, e5) = e0), -(op(e4, e5) = e0), -(op(e5, e5) = e0), -(op(e6, e5) = e0)], (3176 ^ _96822) ^ [] : [-(op(e5, e0) = e1), -(op(e5, e1) = e1), -(op(e5, e2) = e1), -(op(e5, e3) = e1), -(op(e5, e4) = e1), -(op(e5, e5) = e1), -(op(e5, e6) = e1)], (3202 ^ _96822) ^ [] : [-(op(e0, e5) = e1), -(op(e1, e5) = e1), -(op(e2, e5) = e1), -(op(e3, e5) = e1), -(op(e4, e5) = e1), -(op(e5, e5) = e1), -(op(e6, e5) = e1)], (3228 ^ _96822) ^ [] : [-(op(e5, e0) = e2), -(op(e5, e1) = e2), -(op(e5, e2) = e2), -(op(e5, e3) = e2), -(op(e5, e4) = e2), -(op(e5, e5) = e2), -(op(e5, e6) = e2)], (3254 ^ _96822) ^ [] : [-(op(e0, e5) = e2), -(op(e1, e5) = e2), -(op(e2, e5) = e2), -(op(e3, e5) = e2), -(op(e4, e5) = e2), -(op(e5, e5) = e2), -(op(e6, e5) = e2)], (3280 ^ _96822) ^ [] : [-(op(e5, e0) = e3), -(op(e5, e1) = e3), -(op(e5, e2) = e3), -(op(e5, e3) = e3), -(op(e5, e4) = e3), -(op(e5, e5) = e3), -(op(e5, e6) = e3)], (3306 ^ _96822) ^ [] : [-(op(e0, e5) = e3), -(op(e1, e5) = e3), -(op(e2, e5) = e3), -(op(e3, e5) = e3), -(op(e4, e5) = e3), -(op(e5, e5) = e3), -(op(e6, e5) = e3)], (3332 ^ _96822) ^ [] : [-(op(e5, e0) = e4), -(op(e5, e1) = e4), -(op(e5, e2) = e4), -(op(e5, e3) = e4), -(op(e5, e4) = e4), -(op(e5, e5) = e4), -(op(e5, e6) = e4)], (3358 ^ _96822) ^ [] : [-(op(e0, e5) = e4), -(op(e1, e5) = e4), -(op(e2, e5) = e4), -(op(e3, e5) = e4), -(op(e4, e5) = e4), -(op(e5, e5) = e4), -(op(e6, e5) = e4)], (3384 ^ _96822) ^ [] : [-(op(e5, e0) = e5), -(op(e5, e1) = e5), -(op(e5, e2) = e5), -(op(e5, e3) = e5), -(op(e5, e4) = e5), -(op(e5, e5) = e5), -(op(e5, e6) = e5)], (3410 ^ _96822) ^ [] : [-(op(e0, e5) = e5), -(op(e1, e5) = e5), -(op(e2, e5) = e5), -(op(e3, e5) = e5), -(op(e4, e5) = e5), -(op(e5, e5) = e5), -(op(e6, e5) = e5)], (3436 ^ _96822) ^ [] : [-(op(e5, e0) = e6), -(op(e5, e1) = e6), -(op(e5, e2) = e6), -(op(e5, e3) = e6), -(op(e5, e4) = e6), -(op(e5, e5) = e6), -(op(e5, e6) = e6)], (3462 ^ _96822) ^ [] : [-(op(e0, e5) = e6), -(op(e1, e5) = e6), -(op(e2, e5) = e6), -(op(e3, e5) = e6), -(op(e4, e5) = e6), -(op(e5, e5) = e6), -(op(e6, e5) = e6)], (3488 ^ _96822) ^ [] : [-(op(e6, e0) = e0), -(op(e6, e1) = e0), -(op(e6, e2) = e0), -(op(e6, e3) = e0), -(op(e6, e4) = e0), -(op(e6, e5) = e0), -(op(e6, e6) = e0)], (3514 ^ _96822) ^ [] : [-(op(e0, e6) = e0), -(op(e1, e6) = e0), -(op(e2, e6) = e0), -(op(e3, e6) = e0), -(op(e4, e6) = e0), -(op(e5, e6) = e0), -(op(e6, e6) = e0)], (3540 ^ _96822) ^ [] : [-(op(e6, e0) = e1), -(op(e6, e1) = e1), -(op(e6, e2) = e1), -(op(e6, e3) = e1), -(op(e6, e4) = e1), -(op(e6, e5) = e1), -(op(e6, e6) = e1)], (3566 ^ _96822) ^ [] : [-(op(e0, e6) = e1), -(op(e1, e6) = e1), -(op(e2, e6) = e1), -(op(e3, e6) = e1), -(op(e4, e6) = e1), -(op(e5, e6) = e1), -(op(e6, e6) = e1)], (3592 ^ _96822) ^ [] : [-(op(e6, e0) = e2), -(op(e6, e1) = e2), -(op(e6, e2) = e2), -(op(e6, e3) = e2), -(op(e6, e4) = e2), -(op(e6, e5) = e2), -(op(e6, e6) = e2)], (3618 ^ _96822) ^ [] : [-(op(e0, e6) = e2), -(op(e1, e6) = e2), -(op(e2, e6) = e2), -(op(e3, e6) = e2), -(op(e4, e6) = e2), -(op(e5, e6) = e2), -(op(e6, e6) = e2)], (3644 ^ _96822) ^ [] : [-(op(e6, e0) = e3), -(op(e6, e1) = e3), -(op(e6, e2) = e3), -(op(e6, e3) = e3), -(op(e6, e4) = e3), -(op(e6, e5) = e3), -(op(e6, e6) = e3)], (3670 ^ _96822) ^ [] : [-(op(e0, e6) = e3), -(op(e1, e6) = e3), -(op(e2, e6) = e3), -(op(e3, e6) = e3), -(op(e4, e6) = e3), -(op(e5, e6) = e3), -(op(e6, e6) = e3)], (3696 ^ _96822) ^ [] : [-(op(e6, e0) = e4), -(op(e6, e1) = e4), -(op(e6, e2) = e4), -(op(e6, e3) = e4), -(op(e6, e4) = e4), -(op(e6, e5) = e4), -(op(e6, e6) = e4)], (3722 ^ _96822) ^ [] : [-(op(e0, e6) = e4), -(op(e1, e6) = e4), -(op(e2, e6) = e4), -(op(e3, e6) = e4), -(op(e4, e6) = e4), -(op(e5, e6) = e4), -(op(e6, e6) = e4)], (3748 ^ _96822) ^ [] : [-(op(e6, e0) = e5), -(op(e6, e1) = e5), -(op(e6, e2) = e5), -(op(e6, e3) = e5), -(op(e6, e4) = e5), -(op(e6, e5) = e5), -(op(e6, e6) = e5)], (3774 ^ _96822) ^ [] : [-(op(e0, e6) = e5), -(op(e1, e6) = e5), -(op(e2, e6) = e5), -(op(e3, e6) = e5), -(op(e4, e6) = e5), -(op(e5, e6) = e5), -(op(e6, e6) = e5)], (3800 ^ _96822) ^ [] : [-(op(e6, e0) = e6), -(op(e6, e1) = e6), -(op(e6, e2) = e6), -(op(e6, e3) = e6), -(op(e6, e4) = e6), -(op(e6, e5) = e6), -(op(e6, e6) = e6)], (3826 ^ _96822) ^ [] : [-(op(e0, e6) = e6), -(op(e1, e6) = e6), -(op(e2, e6) = e6), -(op(e3, e6) = e6), -(op(e4, e6) = e6), -(op(e5, e6) = e6), -(op(e6, e6) = e6)]], input).
% 0.38/1.39 ncf('1',plain,[op(e0, e0) = e0, op(e1, e1) = e1, op(e2, e2) = e2, op(e3, e3) = e3, op(e4, e4) = e4, op(e5, e5) = e5, op(e6, e6) = e6],start(4606 ^ 0)).
% 0.38/1.39 ncf('1.1',plain,[-(op(e0, e0) = e0), -(op(e1, e1) = e1), -(op(e2, e2) = e2), -(op(e3, e3) = e3), -(op(e4, e4) = e4), -(op(e5, e5) = e5), -(op(e6, e6) = e6)],extension(4580 ^ 1)).
% 0.38/1.39 ncf('1.1.1',plain,[op(e1, e1) = e1, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.1.1.1',plain,[op(e0, e0) = e0],reduction('1')).
% 0.38/1.39 ncf('1.1.2',plain,[op(e2, e2) = e2, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.1.2.1',plain,[op(e0, e0) = e0],reduction('1')).
% 0.38/1.39 ncf('1.1.3',plain,[op(e3, e3) = e3, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.1.3.1',plain,[op(e0, e0) = e0],reduction('1')).
% 0.38/1.39 ncf('1.1.4',plain,[op(e4, e4) = e4, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.1.4.1',plain,[op(e0, e0) = e0],reduction('1')).
% 0.38/1.39 ncf('1.1.5',plain,[op(e5, e5) = e5, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.1.5.1',plain,[op(e0, e0) = e0],reduction('1')).
% 0.38/1.39 ncf('1.1.6',plain,[op(e6, e6) = e6, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.1.6.1',plain,[op(e0, e0) = e0],reduction('1')).
% 0.38/1.39 ncf('1.2',plain,[-(op(e1, e1) = e1), -(op(e0, e0) = e0), -(op(e2, e2) = e2), -(op(e3, e3) = e3), -(op(e4, e4) = e4), -(op(e5, e5) = e5), -(op(e6, e6) = e6)],extension(4580 ^ 1)).
% 0.38/1.39 ncf('1.2.1',plain,[op(e0, e0) = e0, 4650 : -(op(e1, e1) = e1)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.2.1.1',plain,[op(e1, e1) = e1],reduction('1')).
% 0.38/1.39 ncf('1.2.2',plain,[op(e2, e2) = e2, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.2.2.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.2.3',plain,[op(e3, e3) = e3, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.2.3.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.2.4',plain,[op(e4, e4) = e4, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.2.4.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.2.5',plain,[op(e5, e5) = e5, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.2.5.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.2.6',plain,[op(e6, e6) = e6, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.2.6.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.3',plain,[-(op(e2, e2) = e2), -(op(e0, e0) = e0), -(op(e1, e1) = e1), -(op(e3, e3) = e3), -(op(e4, e4) = e4), -(op(e5, e5) = e5), -(op(e6, e6) = e6)],extension(4580 ^ 1)).
% 0.38/1.39 ncf('1.3.1',plain,[op(e0, e0) = e0, 4652 : -(op(e2, e2) = e2)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.3.1.1',plain,[op(e2, e2) = e2],reduction('1')).
% 0.38/1.39 ncf('1.3.2',plain,[op(e1, e1) = e1, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.3.2.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.3.3',plain,[op(e3, e3) = e3, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.3.3.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.3.4',plain,[op(e4, e4) = e4, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.3.4.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.3.5',plain,[op(e5, e5) = e5, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.3.5.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.3.6',plain,[op(e6, e6) = e6, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.3.6.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.4',plain,[-(op(e3, e3) = e3), -(op(e0, e0) = e0), -(op(e1, e1) = e1), -(op(e2, e2) = e2), -(op(e4, e4) = e4), -(op(e5, e5) = e5), -(op(e6, e6) = e6)],extension(4580 ^ 1)).
% 0.38/1.39 ncf('1.4.1',plain,[op(e0, e0) = e0, 4654 : -(op(e3, e3) = e3)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.4.1.1',plain,[op(e3, e3) = e3],reduction('1')).
% 0.38/1.39 ncf('1.4.2',plain,[op(e1, e1) = e1, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.4.2.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.4.3',plain,[op(e2, e2) = e2, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.4.3.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.4.4',plain,[op(e4, e4) = e4, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.4.4.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.4.5',plain,[op(e5, e5) = e5, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.4.5.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.4.6',plain,[op(e6, e6) = e6, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.4.6.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.5',plain,[-(op(e4, e4) = e4), -(op(e0, e0) = e0), -(op(e1, e1) = e1), -(op(e2, e2) = e2), -(op(e3, e3) = e3), -(op(e5, e5) = e5), -(op(e6, e6) = e6)],extension(4580 ^ 1)).
% 0.38/1.39 ncf('1.5.1',plain,[op(e0, e0) = e0, 4656 : -(op(e4, e4) = e4)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.5.1.1',plain,[op(e4, e4) = e4],reduction('1')).
% 0.38/1.39 ncf('1.5.2',plain,[op(e1, e1) = e1, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.5.2.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.5.3',plain,[op(e2, e2) = e2, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.5.3.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.5.4',plain,[op(e3, e3) = e3, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.5.4.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.5.5',plain,[op(e5, e5) = e5, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.5.5.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.5.6',plain,[op(e6, e6) = e6, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.5.6.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.6',plain,[-(op(e5, e5) = e5), -(op(e0, e0) = e0), -(op(e1, e1) = e1), -(op(e2, e2) = e2), -(op(e3, e3) = e3), -(op(e4, e4) = e4), -(op(e6, e6) = e6)],extension(4580 ^ 1)).
% 0.38/1.39 ncf('1.6.1',plain,[op(e0, e0) = e0, 4658 : -(op(e5, e5) = e5)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.6.1.1',plain,[op(e5, e5) = e5],reduction('1')).
% 0.38/1.39 ncf('1.6.2',plain,[op(e1, e1) = e1, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.6.2.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.6.3',plain,[op(e2, e2) = e2, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.6.3.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.6.4',plain,[op(e3, e3) = e3, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.6.4.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.6.5',plain,[op(e4, e4) = e4, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.6.5.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.6.6',plain,[op(e6, e6) = e6, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.6.6.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.7',plain,[-(op(e6, e6) = e6), -(op(e0, e0) = e0), -(op(e1, e1) = e1), -(op(e2, e2) = e2), -(op(e3, e3) = e3), -(op(e4, e4) = e4), -(op(e5, e5) = e5)],extension(4580 ^ 1)).
% 0.38/1.39 ncf('1.7.1',plain,[op(e0, e0) = e0, 4660 : -(op(e6, e6) = e6)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.7.1.1',plain,[op(e6, e6) = e6],reduction('1')).
% 0.38/1.39 ncf('1.7.2',plain,[op(e1, e1) = e1, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.7.2.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.7.3',plain,[op(e2, e2) = e2, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.7.3.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.7.4',plain,[op(e3, e3) = e3, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.7.4.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.7.5',plain,[op(e4, e4) = e4, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.7.5.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 ncf('1.7.6',plain,[op(e5, e5) = e5, 4648 : -(op(e0, e0) = e0)],extension(4632 ^ 2)).
% 0.38/1.39 ncf('1.7.6.1',plain,[op(e0, e0) = e0],lemmata('[1].x')).
% 0.38/1.39 %-----------------------------------------------------
% 0.38/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------