%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : ALG025+1 : TPTP v8.1.2. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n014.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:54 EDT 2023
% Result : Theorem 0.34s 1.38s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : ALG025+1 : TPTP v8.1.2. Released v2.7.0.
% 0.12/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n014.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:30:12 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.34/1.38
% 0.34/1.38 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.34/1.38 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.34/1.38 %-----------------------------------------------------
% 0.34/1.38 ncf(matrix, plain, [(2256 ^ _412364) ^ [] : [-(op(e0, e0) = op(e0, e0))], (2258 ^ _412364) ^ [] : [-(op(e0, e1) = op(e1, e0))], (2260 ^ _412364) ^ [] : [-(op(e0, e2) = op(e2, e0))], (2262 ^ _412364) ^ [] : [-(op(e0, e3) = op(e3, e0))], (2264 ^ _412364) ^ [] : [-(op(e0, e4) = op(e4, e0))], (2266 ^ _412364) ^ [] : [-(op(e0, e5) = op(e5, e0))], (2268 ^ _412364) ^ [] : [-(op(e1, e0) = op(e0, e1))], (2270 ^ _412364) ^ [] : [-(op(e1, e1) = op(e1, e1))], (2272 ^ _412364) ^ [] : [-(op(e1, e2) = op(e2, e1))], (2274 ^ _412364) ^ [] : [-(op(e1, e3) = op(e3, e1))], (2276 ^ _412364) ^ [] : [-(op(e1, e4) = op(e4, e1))], (2278 ^ _412364) ^ [] : [-(op(e1, e5) = op(e5, e1))], (2280 ^ _412364) ^ [] : [-(op(e2, e0) = op(e0, e2))], (2282 ^ _412364) ^ [] : [-(op(e2, e1) = op(e1, e2))], (2284 ^ _412364) ^ [] : [-(op(e2, e2) = op(e2, e2))], (2286 ^ _412364) ^ [] : [-(op(e2, e3) = op(e3, e2))], (2288 ^ _412364) ^ [] : [-(op(e2, e4) = op(e4, e2))], (2290 ^ _412364) ^ [] : [-(op(e2, e5) = op(e5, e2))], (2292 ^ _412364) ^ [] : [-(op(e3, e0) = op(e0, e3))], (2294 ^ _412364) ^ [] : [-(op(e3, e1) = op(e1, e3))], (2296 ^ _412364) ^ [] : [-(op(e3, e2) = op(e2, e3))], (2298 ^ _412364) ^ [] : [-(op(e3, e3) = op(e3, e3))], (2300 ^ _412364) ^ [] : [-(op(e3, e4) = op(e4, e3))], (2302 ^ _412364) ^ [] : [-(op(e3, e5) = op(e5, e3))], (2304 ^ _412364) ^ [] : [-(op(e4, e0) = op(e0, e4))], (2306 ^ _412364) ^ [] : [-(op(e4, e1) = op(e1, e4))], (2308 ^ _412364) ^ [] : [-(op(e4, e2) = op(e2, e4))], (2310 ^ _412364) ^ [] : [-(op(e4, e3) = op(e3, e4))], (2312 ^ _412364) ^ [] : [-(op(e4, e4) = op(e4, e4))], (2314 ^ _412364) ^ [] : [-(op(e4, e5) = op(e5, e4))], (2316 ^ _412364) ^ [] : [-(op(e5, e0) = op(e0, e5))], (2318 ^ _412364) ^ [] : [-(op(e5, e1) = op(e1, e5))], (2320 ^ _412364) ^ [] : [-(op(e5, e2) = op(e2, e5))], (2322 ^ _412364) ^ [] : [-(op(e5, e3) = op(e3, e5))], (2324 ^ _412364) ^ [] : [-(op(e5, e4) = op(e4, e5))], (2326 ^ _412364) ^ [] : [-(op(e5, e5) = op(e5, e5))], (2114 ^ _412364) ^ [] : [op(e0, e0) = op(e0, e0), op(e0, e1) = op(e1, e0), op(e0, e2) = op(e2, e0), op(e0, e3) = op(e3, e0), op(e0, e4) = op(e4, e0), op(e0, e5) = op(e5, e0), op(e1, e0) = op(e0, e1), op(e1, e1) = op(e1, e1), op(e1, e2) = op(e2, e1), op(e1, e3) = op(e3, e1), op(e1, e4) = op(e4, e1), op(e1, e5) = op(e5, e1), op(e2, e0) = op(e0, e2), op(e2, e1) = op(e1, e2), op(e2, e2) = op(e2, e2), op(e2, e3) = op(e3, e2), op(e2, e4) = op(e4, e2), op(e2, e5) = op(e5, e2), op(e3, e0) = op(e0, e3), op(e3, e1) = op(e1, e3), op(e3, e2) = op(e2, e3), op(e3, e3) = op(e3, e3), op(e3, e4) = op(e4, e3), op(e3, e5) = op(e5, e3), op(e4, e0) = op(e0, e4), op(e4, e1) = op(e1, e4), op(e4, e2) = op(e2, e4), op(e4, e3) = op(e3, e4), op(e4, e4) = op(e4, e4), op(e4, e5) = op(e5, e4), op(e5, e0) = op(e0, e5), op(e5, e1) = op(e1, e5), op(e5, e2) = op(e2, e5), op(e5, e3) = op(e3, e5), op(e5, e4) = op(e4, e5), op(e5, e5) = op(e5, e5)], (2 ^ _412364) ^ [_412488] : [-(_412488 = _412488)], (4 ^ _412364) ^ [_412595, _412597] : [_412597 = _412595, -(_412595 = _412597)], (10 ^ _412364) ^ [_412799, _412801, _412803] : [-(_412803 = _412799), _412803 = _412801, _412801 = _412799], (20 ^ _412364) ^ [_413112, _413114] : [_413114 = _413112, -(inv(_413114) = inv(_413112))], (26 ^ _412364) ^ [_413338, _413340, _413342, _413344] : [-(op(_413344, _413340) = op(_413342, _413338)), _413344 = _413342, _413340 = _413338], (828 ^ _412364) ^ [] : [-(op(op(e0, e0), e0) = op(e0, op(e0, e0)))], (830 ^ _412364) ^ [] : [-(op(op(e0, e0), e1) = op(e0, op(e0, e1)))], (832 ^ _412364) ^ [] : [-(op(op(e0, e0), e2) = op(e0, op(e0, e2)))], (834 ^ _412364) ^ [] : [-(op(op(e0, e0), e3) = op(e0, op(e0, e3)))], (836 ^ _412364) ^ [] : [-(op(op(e0, e0), e4) = op(e0, op(e0, e4)))], (838 ^ _412364) ^ [] : [-(op(op(e0, e0), e5) = op(e0, op(e0, e5)))], (840 ^ _412364) ^ [] : [-(op(op(e0, e1), e0) = op(e0, op(e1, e0)))], (842 ^ _412364) ^ [] : [-(op(op(e0, e1), e1) = op(e0, op(e1, e1)))], (844 ^ _412364) ^ [] : [-(op(op(e0, e1), e2) = op(e0, op(e1, e2)))], (846 ^ _412364) ^ [] : [-(op(op(e0, e1), e3) = op(e0, op(e1, e3)))], (848 ^ _412364) ^ [] : [-(op(op(e0, e1), e4) = op(e0, op(e1, e4)))], (850 ^ _412364) ^ [] : [-(op(op(e0, e1), e5) = op(e0, op(e1, e5)))], (852 ^ _412364) ^ [] : [-(op(op(e0, e2), e0) = op(e0, op(e2, e0)))], (854 ^ _412364) ^ [] : [-(op(op(e0, e2), e1) = op(e0, op(e2, e1)))], (856 ^ _412364) ^ [] : [-(op(op(e0, e2), e2) = op(e0, op(e2, e2)))], (858 ^ _412364) ^ [] : [-(op(op(e0, e2), e3) = op(e0, op(e2, e3)))], (860 ^ _412364) ^ [] : [-(op(op(e0, e2), e4) = op(e0, op(e2, e4)))], (862 ^ _412364) ^ [] : [-(op(op(e0, e2), e5) = op(e0, op(e2, e5)))], (864 ^ _412364) ^ [] : [-(op(op(e0, e3), e0) = op(e0, op(e3, e0)))], (866 ^ _412364) ^ [] : [-(op(op(e0, e3), e1) = op(e0, op(e3, e1)))], (868 ^ _412364) ^ [] : [-(op(op(e0, e3), e2) = op(e0, op(e3, e2)))], (870 ^ _412364) ^ [] : [-(op(op(e0, e3), e3) = op(e0, op(e3, e3)))], (872 ^ _412364) ^ [] : [-(op(op(e0, e3), e4) = op(e0, op(e3, e4)))], (874 ^ _412364) ^ [] : [-(op(op(e0, e3), e5) = op(e0, op(e3, e5)))], (876 ^ _412364) ^ [] : [-(op(op(e0, e4), e0) = op(e0, op(e4, e0)))], (878 ^ _412364) ^ [] : [-(op(op(e0, e4), e1) = op(e0, op(e4, e1)))], (880 ^ _412364) ^ [] : [-(op(op(e0, e4), e2) = op(e0, op(e4, e2)))], (882 ^ _412364) ^ [] : [-(op(op(e0, e4), e3) = op(e0, op(e4, e3)))], (884 ^ _412364) ^ [] : [-(op(op(e0, e4), e4) = op(e0, op(e4, e4)))], (886 ^ _412364) ^ [] : [-(op(op(e0, e4), e5) = op(e0, op(e4, e5)))], (888 ^ _412364) ^ [] : [-(op(op(e0, e5), e0) = op(e0, op(e5, e0)))], (890 ^ _412364) ^ [] : [-(op(op(e0, e5), e1) = op(e0, op(e5, e1)))], (892 ^ _412364) ^ [] : [-(op(op(e0, e5), e2) = op(e0, op(e5, e2)))], (894 ^ _412364) ^ [] : [-(op(op(e0, e5), e3) = op(e0, op(e5, e3)))], (896 ^ _412364) ^ [] : [-(op(op(e0, e5), e4) = op(e0, op(e5, e4)))], (898 ^ _412364) ^ [] : [-(op(op(e0, e5), e5) = op(e0, op(e5, e5)))], (900 ^ _412364) ^ [] : [-(op(op(e1, e0), e0) = op(e1, op(e0, e0)))], (902 ^ _412364) ^ [] : [-(op(op(e1, e0), e1) = op(e1, op(e0, e1)))], (904 ^ _412364) ^ [] : [-(op(op(e1, e0), e2) = op(e1, op(e0, e2)))], (906 ^ _412364) ^ [] : [-(op(op(e1, e0), e3) = op(e1, op(e0, e3)))], (908 ^ _412364) ^ [] : [-(op(op(e1, e0), e4) = op(e1, op(e0, e4)))], (910 ^ _412364) ^ [] : [-(op(op(e1, e0), e5) = op(e1, op(e0, e5)))], (912 ^ _412364) ^ [] : [-(op(op(e1, e1), e0) = op(e1, op(e1, e0)))], (914 ^ _412364) ^ [] : [-(op(op(e1, e1), e1) = op(e1, op(e1, e1)))], (916 ^ _412364) ^ [] : [-(op(op(e1, e1), e2) = op(e1, op(e1, e2)))], (918 ^ _412364) ^ [] : [-(op(op(e1, e1), e3) = op(e1, op(e1, e3)))], (920 ^ _412364) ^ [] : [-(op(op(e1, e1), e4) = op(e1, op(e1, e4)))], (922 ^ _412364) ^ [] : [-(op(op(e1, e1), e5) = op(e1, op(e1, e5)))], (924 ^ _412364) ^ [] : [-(op(op(e1, e2), e0) = op(e1, op(e2, e0)))], (926 ^ _412364) ^ [] : [-(op(op(e1, e2), e1) = op(e1, op(e2, e1)))], (928 ^ _412364) ^ [] : [-(op(op(e1, e2), e2) = op(e1, op(e2, e2)))], (930 ^ _412364) ^ [] : [-(op(op(e1, e2), e3) = op(e1, op(e2, e3)))], (932 ^ _412364) ^ [] : [-(op(op(e1, e2), e4) = op(e1, op(e2, e4)))], (934 ^ _412364) ^ [] : [-(op(op(e1, e2), e5) = op(e1, op(e2, e5)))], (936 ^ _412364) ^ [] : [-(op(op(e1, e3), e0) = op(e1, op(e3, e0)))], (938 ^ _412364) ^ [] : [-(op(op(e1, e3), e1) = op(e1, op(e3, e1)))], (940 ^ _412364) ^ [] : [-(op(op(e1, e3), e2) = op(e1, op(e3, e2)))], (942 ^ _412364) ^ [] : [-(op(op(e1, e3), e3) = op(e1, op(e3, e3)))], (944 ^ _412364) ^ [] : [-(op(op(e1, e3), e4) = op(e1, op(e3, e4)))], (946 ^ _412364) ^ [] : [-(op(op(e1, e3), e5) = op(e1, op(e3, e5)))], (948 ^ _412364) ^ [] : [-(op(op(e1, e4), e0) = op(e1, op(e4, e0)))], (950 ^ _412364) ^ [] : [-(op(op(e1, e4), e1) = op(e1, op(e4, e1)))], (952 ^ _412364) ^ [] : [-(op(op(e1, e4), e2) = op(e1, op(e4, e2)))], (954 ^ _412364) ^ [] : [-(op(op(e1, e4), e3) = op(e1, op(e4, e3)))], (956 ^ _412364) ^ [] : [-(op(op(e1, e4), e4) = op(e1, op(e4, e4)))], (958 ^ _412364) ^ [] : [-(op(op(e1, e4), e5) = op(e1, op(e4, e5)))], (960 ^ _412364) ^ [] : [-(op(op(e1, e5), e0) = op(e1, op(e5, e0)))], (962 ^ _412364) ^ [] : [-(op(op(e1, e5), e1) = op(e1, op(e5, e1)))], (964 ^ _412364) ^ [] : [-(op(op(e1, e5), e2) = op(e1, op(e5, e2)))], (966 ^ _412364) ^ [] : [-(op(op(e1, e5), e3) = op(e1, op(e5, e3)))], (968 ^ _412364) ^ [] : [-(op(op(e1, e5), e4) = op(e1, op(e5, e4)))], (970 ^ _412364) ^ [] : [-(op(op(e1, e5), e5) = op(e1, op(e5, e5)))], (972 ^ _412364) ^ [] : [-(op(op(e2, e0), e0) = op(e2, op(e0, e0)))], (974 ^ _412364) ^ [] : [-(op(op(e2, e0), e1) = op(e2, op(e0, e1)))], (976 ^ _412364) ^ [] : [-(op(op(e2, e0), e2) = op(e2, op(e0, e2)))], (978 ^ _412364) ^ [] : [-(op(op(e2, e0), e3) = op(e2, op(e0, e3)))], (980 ^ _412364) ^ [] : [-(op(op(e2, e0), e4) = op(e2, op(e0, e4)))], (982 ^ _412364) ^ [] : [-(op(op(e2, e0), e5) = op(e2, op(e0, e5)))], (984 ^ _412364) ^ [] : [-(op(op(e2, e1), e0) = op(e2, op(e1, e0)))], (986 ^ _412364) ^ [] : [-(op(op(e2, e1), e1) = op(e2, op(e1, e1)))], (988 ^ _412364) ^ [] : [-(op(op(e2, e1), e2) = op(e2, op(e1, e2)))], (990 ^ _412364) ^ [] : [-(op(op(e2, e1), e3) = op(e2, op(e1, e3)))], (992 ^ _412364) ^ [] : [-(op(op(e2, e1), e4) = op(e2, op(e1, e4)))], (994 ^ _412364) ^ [] : [-(op(op(e2, e1), e5) = op(e2, op(e1, e5)))], (996 ^ _412364) ^ [] : [-(op(op(e2, e2), e0) = op(e2, op(e2, e0)))], (998 ^ _412364) ^ [] : [-(op(op(e2, e2), e1) = op(e2, op(e2, e1)))], (1000 ^ _412364) ^ [] : [-(op(op(e2, e2), e2) = op(e2, op(e2, e2)))], (1002 ^ _412364) ^ [] : [-(op(op(e2, e2), e3) = op(e2, op(e2, e3)))], (1004 ^ _412364) ^ [] : [-(op(op(e2, e2), e4) = op(e2, op(e2, e4)))], (1006 ^ _412364) ^ [] : [-(op(op(e2, e2), e5) = op(e2, op(e2, e5)))], (1008 ^ _412364) ^ [] : [-(op(op(e2, e3), e0) = op(e2, op(e3, e0)))], (1010 ^ _412364) ^ [] : [-(op(op(e2, e3), e1) = op(e2, op(e3, e1)))], (1012 ^ _412364) ^ [] : [-(op(op(e2, e3), e2) = op(e2, op(e3, e2)))], (1014 ^ _412364) ^ [] : [-(op(op(e2, e3), e3) = op(e2, op(e3, e3)))], (1016 ^ _412364) ^ [] : [-(op(op(e2, e3), e4) = op(e2, op(e3, e4)))], (1018 ^ _412364) ^ [] : [-(op(op(e2, e3), e5) = op(e2, op(e3, e5)))], (1020 ^ _412364) ^ [] : [-(op(op(e2, e4), e0) = op(e2, op(e4, e0)))], (1022 ^ _412364) ^ [] : [-(op(op(e2, e4), e1) = op(e2, op(e4, e1)))], (1024 ^ _412364) ^ [] : [-(op(op(e2, e4), e2) = op(e2, op(e4, e2)))], (1026 ^ _412364) ^ [] : [-(op(op(e2, e4), e3) = op(e2, op(e4, e3)))], (1028 ^ _412364) ^ [] : [-(op(op(e2, e4), e4) = op(e2, op(e4, e4)))], (1030 ^ _412364) ^ [] : [-(op(op(e2, e4), e5) = op(e2, op(e4, e5)))], (1032 ^ _412364) ^ [] : [-(op(op(e2, e5), e0) = op(e2, op(e5, e0)))], (1034 ^ _412364) ^ [] : [-(op(op(e2, e5), e1) = op(e2, op(e5, e1)))], (1036 ^ _412364) ^ [] : [-(op(op(e2, e5), e2) = op(e2, op(e5, e2)))], (1038 ^ _412364) ^ [] : [-(op(op(e2, e5), e3) = op(e2, op(e5, e3)))], (1040 ^ _412364) ^ [] : [-(op(op(e2, e5), e4) = op(e2, op(e5, e4)))], (1042 ^ _412364) ^ [] : [-(op(op(e2, e5), e5) = op(e2, op(e5, e5)))], (1044 ^ _412364) ^ [] : [-(op(op(e3, e0), e0) = op(e3, op(e0, e0)))], (1046 ^ _412364) ^ [] : [-(op(op(e3, e0), e1) = op(e3, op(e0, e1)))], (1048 ^ _412364) ^ [] : [-(op(op(e3, e0), e2) = op(e3, op(e0, e2)))], (1050 ^ _412364) ^ [] : [-(op(op(e3, e0), e3) = op(e3, op(e0, e3)))], (1052 ^ _412364) ^ [] : [-(op(op(e3, e0), e4) = op(e3, op(e0, e4)))], (1054 ^ _412364) ^ [] : [-(op(op(e3, e0), e5) = op(e3, op(e0, e5)))], (1056 ^ _412364) ^ [] : [-(op(op(e3, e1), e0) = op(e3, op(e1, e0)))], (1058 ^ _412364) ^ [] : [-(op(op(e3, e1), e1) = op(e3, op(e1, e1)))], (1060 ^ _412364) ^ [] : [-(op(op(e3, e1), e2) = op(e3, op(e1, e2)))], (1062 ^ _412364) ^ [] : [-(op(op(e3, e1), e3) = op(e3, op(e1, e3)))], (1064 ^ _412364) ^ [] : [-(op(op(e3, e1), e4) = op(e3, op(e1, e4)))], (1066 ^ _412364) ^ [] : [-(op(op(e3, e1), e5) = op(e3, op(e1, e5)))], (1068 ^ _412364) ^ [] : [-(op(op(e3, e2), e0) = op(e3, op(e2, e0)))], (1070 ^ _412364) ^ [] : [-(op(op(e3, e2), e1) = op(e3, op(e2, e1)))], (1072 ^ _412364) ^ [] : [-(op(op(e3, e2), e2) = op(e3, op(e2, e2)))], (1074 ^ _412364) ^ [] : [-(op(op(e3, e2), e3) = op(e3, op(e2, e3)))], (1076 ^ _412364) ^ [] : [-(op(op(e3, e2), e4) = op(e3, op(e2, e4)))], (1078 ^ _412364) ^ [] : [-(op(op(e3, e2), e5) = op(e3, op(e2, e5)))], (1080 ^ _412364) ^ [] : [-(op(op(e3, e3), e0) = op(e3, op(e3, e0)))], (1082 ^ _412364) ^ [] : [-(op(op(e3, e3), e1) = op(e3, op(e3, e1)))], (1084 ^ _412364) ^ [] : [-(op(op(e3, e3), e2) = op(e3, op(e3, e2)))], (1086 ^ _412364) ^ [] : [-(op(op(e3, e3), e3) = op(e3, op(e3, e3)))], (1088 ^ _412364) ^ [] : [-(op(op(e3, e3), e4) = op(e3, op(e3, e4)))], (1090 ^ _412364) ^ [] : [-(op(op(e3, e3), e5) = op(e3, op(e3, e5)))], (1092 ^ _412364) ^ [] : [-(op(op(e3, e4), e0) = op(e3, op(e4, e0)))], (1094 ^ _412364) ^ [] : [-(op(op(e3, e4), e1) = op(e3, op(e4, e1)))], (1096 ^ _412364) ^ [] : [-(op(op(e3, e4), e2) = op(e3, op(e4, e2)))], (1098 ^ _412364) ^ [] : [-(op(op(e3, e4), e3) = op(e3, op(e4, e3)))], (1100 ^ _412364) ^ [] : [-(op(op(e3, e4), e4) = op(e3, op(e4, e4)))], (1102 ^ _412364) ^ [] : [-(op(op(e3, e4), e5) = op(e3, op(e4, e5)))], (1104 ^ _412364) ^ [] : [-(op(op(e3, e5), e0) = op(e3, op(e5, e0)))], (1106 ^ _412364) ^ [] : [-(op(op(e3, e5), e1) = op(e3, op(e5, e1)))], (1108 ^ _412364) ^ [] : [-(op(op(e3, e5), e2) = op(e3, op(e5, e2)))], (1110 ^ _412364) ^ [] : [-(op(op(e3, e5), e3) = op(e3, op(e5, e3)))], (1112 ^ _412364) ^ [] : [-(op(op(e3, e5), e4) = op(e3, op(e5, e4)))], (1114 ^ _412364) ^ [] : [-(op(op(e3, e5), e5) = op(e3, op(e5, e5)))], (1116 ^ _412364) ^ [] : [-(op(op(e4, e0), e0) = op(e4, op(e0, e0)))], (1118 ^ _412364) ^ [] : [-(op(op(e4, e0), e1) = op(e4, op(e0, e1)))], (1120 ^ _412364) ^ [] : [-(op(op(e4, e0), e2) = op(e4, op(e0, e2)))], (1122 ^ _412364) ^ [] : [-(op(op(e4, e0), e3) = op(e4, op(e0, e3)))], (1124 ^ _412364) ^ [] : [-(op(op(e4, e0), e4) = op(e4, op(e0, e4)))], (1126 ^ _412364) ^ [] : [-(op(op(e4, e0), e5) = op(e4, op(e0, e5)))], (1128 ^ _412364) ^ [] : [-(op(op(e4, e1), e0) = op(e4, op(e1, e0)))], (1130 ^ _412364) ^ [] : [-(op(op(e4, e1), e1) = op(e4, op(e1, e1)))], (1132 ^ _412364) ^ [] : [-(op(op(e4, e1), e2) = op(e4, op(e1, e2)))], (1134 ^ _412364) ^ [] : [-(op(op(e4, e1), e3) = op(e4, op(e1, e3)))], (1136 ^ _412364) ^ [] : [-(op(op(e4, e1), e4) = op(e4, op(e1, e4)))], (1138 ^ _412364) ^ [] : [-(op(op(e4, e1), e5) = op(e4, op(e1, e5)))], (1140 ^ _412364) ^ [] : [-(op(op(e4, e2), e0) = op(e4, op(e2, e0)))], (1142 ^ _412364) ^ [] : [-(op(op(e4, e2), e1) = op(e4, op(e2, e1)))], (1144 ^ _412364) ^ [] : [-(op(op(e4, e2), e2) = op(e4, op(e2, e2)))], (1146 ^ _412364) ^ [] : [-(op(op(e4, e2), e3) = op(e4, op(e2, e3)))], (1148 ^ _412364) ^ [] : [-(op(op(e4, e2), e4) = op(e4, op(e2, e4)))], (1150 ^ _412364) ^ [] : [-(op(op(e4, e2), e5) = op(e4, op(e2, e5)))], (1152 ^ _412364) ^ [] : [-(op(op(e4, e3), e0) = op(e4, op(e3, e0)))], (1154 ^ _412364) ^ [] : [-(op(op(e4, e3), e1) = op(e4, op(e3, e1)))], (1156 ^ _412364) ^ [] : [-(op(op(e4, e3), e2) = op(e4, op(e3, e2)))], (1158 ^ _412364) ^ [] : [-(op(op(e4, e3), e3) = op(e4, op(e3, e3)))], (1160 ^ _412364) ^ [] : [-(op(op(e4, e3), e4) = op(e4, op(e3, e4)))], (1162 ^ _412364) ^ [] : [-(op(op(e4, e3), e5) = op(e4, op(e3, e5)))], (1164 ^ _412364) ^ [] : [-(op(op(e4, e4), e0) = op(e4, op(e4, e0)))], (1166 ^ _412364) ^ [] : [-(op(op(e4, e4), e1) = op(e4, op(e4, e1)))], (1168 ^ _412364) ^ [] : [-(op(op(e4, e4), e2) = op(e4, op(e4, e2)))], (1170 ^ _412364) ^ [] : [-(op(op(e4, e4), e3) = op(e4, op(e4, e3)))], (1172 ^ _412364) ^ [] : [-(op(op(e4, e4), e4) = op(e4, op(e4, e4)))], (1174 ^ _412364) ^ [] : [-(op(op(e4, e4), e5) = op(e4, op(e4, e5)))], (1176 ^ _412364) ^ [] : [-(op(op(e4, e5), e0) = op(e4, op(e5, e0)))], (1178 ^ _412364) ^ [] : [-(op(op(e4, e5), e1) = op(e4, op(e5, e1)))], (1180 ^ _412364) ^ [] : [-(op(op(e4, e5), e2) = op(e4, op(e5, e2)))], (1182 ^ _412364) ^ [] : [-(op(op(e4, e5), e3) = op(e4, op(e5, e3)))], (1184 ^ _412364) ^ [] : [-(op(op(e4, e5), e4) = op(e4, op(e5, e4)))], (1186 ^ _412364) ^ [] : [-(op(op(e4, e5), e5) = op(e4, op(e5, e5)))], (1188 ^ _412364) ^ [] : [-(op(op(e5, e0), e0) = op(e5, op(e0, e0)))], (1190 ^ _412364) ^ [] : [-(op(op(e5, e0), e1) = op(e5, op(e0, e1)))], (1192 ^ _412364) ^ [] : [-(op(op(e5, e0), e2) = op(e5, op(e0, e2)))], (1194 ^ _412364) ^ [] : [-(op(op(e5, e0), e3) = op(e5, op(e0, e3)))], (1196 ^ _412364) ^ [] : [-(op(op(e5, e0), e4) = op(e5, op(e0, e4)))], (1198 ^ _412364) ^ [] : [-(op(op(e5, e0), e5) = op(e5, op(e0, e5)))], (1200 ^ _412364) ^ [] : [-(op(op(e5, e1), e0) = op(e5, op(e1, e0)))], (1202 ^ _412364) ^ [] : [-(op(op(e5, e1), e1) = op(e5, op(e1, e1)))], (1204 ^ _412364) ^ [] : [-(op(op(e5, e1), e2) = op(e5, op(e1, e2)))], (1206 ^ _412364) ^ [] : [-(op(op(e5, e1), e3) = op(e5, op(e1, e3)))], (1208 ^ _412364) ^ [] : [-(op(op(e5, e1), e4) = op(e5, op(e1, e4)))], (1210 ^ _412364) ^ [] : [-(op(op(e5, e1), e5) = op(e5, op(e1, e5)))], (1212 ^ _412364) ^ [] : [-(op(op(e5, e2), e0) = op(e5, op(e2, e0)))], (1214 ^ _412364) ^ [] : [-(op(op(e5, e2), e1) = op(e5, op(e2, e1)))], (1216 ^ _412364) ^ [] : [-(op(op(e5, e2), e2) = op(e5, op(e2, e2)))], (1218 ^ _412364) ^ [] : [-(op(op(e5, e2), e3) = op(e5, op(e2, e3)))], (1220 ^ _412364) ^ [] : [-(op(op(e5, e2), e4) = op(e5, op(e2, e4)))], (1222 ^ _412364) ^ [] : [-(op(op(e5, e2), e5) = op(e5, op(e2, e5)))], (1224 ^ _412364) ^ [] : [-(op(op(e5, e3), e0) = op(e5, op(e3, e0)))], (1226 ^ _412364) ^ [] : [-(op(op(e5, e3), e1) = op(e5, op(e3, e1)))], (1228 ^ _412364) ^ [] : [-(op(op(e5, e3), e2) = op(e5, op(e3, e2)))], (1230 ^ _412364) ^ [] : [-(op(op(e5, e3), e3) = op(e5, op(e3, e3)))], (1232 ^ _412364) ^ [] : [-(op(op(e5, e3), e4) = op(e5, op(e3, e4)))], (1234 ^ _412364) ^ [] : [-(op(op(e5, e3), e5) = op(e5, op(e3, e5)))], (1236 ^ _412364) ^ [] : [-(op(op(e5, e4), e0) = op(e5, op(e4, e0)))], (1238 ^ _412364) ^ [] : [-(op(op(e5, e4), e1) = op(e5, op(e4, e1)))], (1240 ^ _412364) ^ [] : [-(op(op(e5, e4), e2) = op(e5, op(e4, e2)))], (1242 ^ _412364) ^ [] : [-(op(op(e5, e4), e3) = op(e5, op(e4, e3)))], (1244 ^ _412364) ^ [] : [-(op(op(e5, e4), e4) = op(e5, op(e4, e4)))], (1246 ^ _412364) ^ [] : [-(op(op(e5, e4), e5) = op(e5, op(e4, e5)))], (1248 ^ _412364) ^ [] : [-(op(op(e5, e5), e0) = op(e5, op(e5, e0)))], (1250 ^ _412364) ^ [] : [-(op(op(e5, e5), e1) = op(e5, op(e5, e1)))], (1252 ^ _412364) ^ [] : [-(op(op(e5, e5), e2) = op(e5, op(e5, e2)))], (1254 ^ _412364) ^ [] : [-(op(op(e5, e5), e3) = op(e5, op(e5, e3)))], (1256 ^ _412364) ^ [] : [-(op(op(e5, e5), e4) = op(e5, op(e5, e4)))], (1258 ^ _412364) ^ [] : [-(op(op(e5, e5), e5) = op(e5, op(e5, e5)))], (1260 ^ _412364) ^ [] : [-(op(unit, e0) = e0)], (1262 ^ _412364) ^ [] : [-(op(e0, unit) = e0)], (1264 ^ _412364) ^ [] : [-(op(unit, e1) = e1)], (1266 ^ _412364) ^ [] : [-(op(e1, unit) = e1)], (1268 ^ _412364) ^ [] : [-(op(unit, e2) = e2)], (1270 ^ _412364) ^ [] : [-(op(e2, unit) = e2)], (1272 ^ _412364) ^ [] : [-(op(unit, e3) = e3)], (1274 ^ _412364) ^ [] : [-(op(e3, unit) = e3)], (1276 ^ _412364) ^ [] : [-(op(unit, e4) = e4)], (1278 ^ _412364) ^ [] : [-(op(e4, unit) = e4)], (1280 ^ _412364) ^ [] : [-(op(unit, e5) = e5)], (1282 ^ _412364) ^ [] : [-(op(e5, unit) = e5)], (1284 ^ _412364) ^ [] : [-(unit = e0), -(unit = e1), -(unit = e2), -(unit = e3), -(unit = e4), -(unit = e5)], (1306 ^ _412364) ^ [] : [-(op(e0, inv(e0)) = unit)], (1308 ^ _412364) ^ [] : [-(op(inv(e0), e0) = unit)], (1310 ^ _412364) ^ [] : [-(op(e1, inv(e1)) = unit)], (1312 ^ _412364) ^ [] : [-(op(inv(e1), e1) = unit)], (1314 ^ _412364) ^ [] : [-(op(e2, inv(e2)) = unit)], (1316 ^ _412364) ^ [] : [-(op(inv(e2), e2) = unit)], (1318 ^ _412364) ^ [] : [-(op(e3, inv(e3)) = unit)], (1320 ^ _412364) ^ [] : [-(op(inv(e3), e3) = unit)], (1322 ^ _412364) ^ [] : [-(op(e4, inv(e4)) = unit)], (1324 ^ _412364) ^ [] : [-(op(inv(e4), e4) = unit)], (1326 ^ _412364) ^ [] : [-(op(e5, inv(e5)) = unit)], (1328 ^ _412364) ^ [] : [-(op(inv(e5), e5) = unit)], (1330 ^ _412364) ^ [] : [-(inv(e0) = e0), -(inv(e0) = e1), -(inv(e0) = e2), -(inv(e0) = e3), -(inv(e0) = e4), -(inv(e0) = e5)], (1352 ^ _412364) ^ [] : [-(inv(e1) = e0), -(inv(e1) = e1), -(inv(e1) = e2), -(inv(e1) = e3), -(inv(e1) = e4), -(inv(e1) = e5)], (1374 ^ _412364) ^ [] : [-(inv(e2) = e0), -(inv(e2) = e1), -(inv(e2) = e2), -(inv(e2) = e3), -(inv(e2) = e4), -(inv(e2) = e5)], (1396 ^ _412364) ^ [] : [-(inv(e3) = e0), -(inv(e3) = e1), -(inv(e3) = e2), -(inv(e3) = e3), -(inv(e3) = e4), -(inv(e3) = e5)], (1418 ^ _412364) ^ [] : [-(inv(e4) = e0), -(inv(e4) = e1), -(inv(e4) = e2), -(inv(e4) = e3), -(inv(e4) = e4), -(inv(e4) = e5)], (1440 ^ _412364) ^ [] : [-(inv(e5) = e0), -(inv(e5) = e1), -(inv(e5) = e2), -(inv(e5) = e3), -(inv(e5) = e4), -(inv(e5) = e5)], (1462 ^ _412364) ^ [] : [-(unit = e0)], (1464 ^ _412364) ^ [] : [-(inv(unit) = unit)], (1466 ^ _412364) ^ [] : [-(inv(inv(e0)) = e0)], (1468 ^ _412364) ^ [] : [-(inv(inv(e1)) = e1)], (1470 ^ _412364) ^ [] : [-(inv(inv(e2)) = e2)], (1472 ^ _412364) ^ [] : [-(inv(inv(e3)) = e3)], (1474 ^ _412364) ^ [] : [-(inv(inv(e4)) = e4)], (1476 ^ _412364) ^ [] : [-(inv(inv(e5)) = e5)], (1694 ^ _412364) ^ [] : [inv(e0) = inv(e1)], (1696 ^ _412364) ^ [] : [inv(e0) = inv(e2)], (1698 ^ _412364) ^ [] : [inv(e0) = inv(e3)], (1700 ^ _412364) ^ [] : [inv(e0) = inv(e4)], (1702 ^ _412364) ^ [] : [inv(e0) = inv(e5)], (1704 ^ _412364) ^ [] : [inv(e1) = inv(e2)], (1706 ^ _412364) ^ [] : [inv(e1) = inv(e3)], (1708 ^ _412364) ^ [] : [inv(e1) = inv(e4)], (1710 ^ _412364) ^ [] : [inv(e1) = inv(e5)], (1712 ^ _412364) ^ [] : [inv(e2) = inv(e3)], (1714 ^ _412364) ^ [] : [inv(e2) = inv(e4)], (1716 ^ _412364) ^ [] : [inv(e2) = inv(e5)], (1718 ^ _412364) ^ [] : [inv(e3) = inv(e4)], (1720 ^ _412364) ^ [] : [inv(e3) = inv(e5)], (1722 ^ _412364) ^ [] : [inv(e4) = inv(e5)], (1724 ^ _412364) ^ [] : [op(e0, e0) = op(e1, e0)], (1726 ^ _412364) ^ [] : [op(e0, e0) = op(e2, e0)], (1728 ^ _412364) ^ [] : [op(e0, e0) = op(e3, e0)], (1730 ^ _412364) ^ [] : [op(e0, e0) = op(e4, e0)], (1732 ^ _412364) ^ [] : [op(e0, e0) = op(e5, e0)], (1734 ^ _412364) ^ [] : [op(e1, e0) = op(e2, e0)], (1736 ^ _412364) ^ [] : [op(e1, e0) = op(e3, e0)], (1738 ^ _412364) ^ [] : [op(e1, e0) = op(e4, e0)], (1740 ^ _412364) ^ [] : [op(e1, e0) = op(e5, e0)], (1742 ^ _412364) ^ [] : [op(e2, e0) = op(e3, e0)], (1744 ^ _412364) ^ [] : [op(e2, e0) = op(e4, e0)], (1746 ^ _412364) ^ [] : [op(e2, e0) = op(e5, e0)], (1748 ^ _412364) ^ [] : [op(e3, e0) = op(e4, e0)], (1750 ^ _412364) ^ [] : [op(e3, e0) = op(e5, e0)], (1752 ^ _412364) ^ [] : [op(e4, e0) = op(e5, e0)], (1754 ^ _412364) ^ [] : [op(e0, e1) = op(e1, e1)], (1756 ^ _412364) ^ [] : [op(e0, e1) = op(e2, e1)], (1758 ^ _412364) ^ [] : [op(e0, e1) = op(e3, e1)], (1760 ^ _412364) ^ [] : [op(e0, e1) = op(e4, e1)], (1762 ^ _412364) ^ [] : [op(e0, e1) = op(e5, e1)], (1764 ^ _412364) ^ [] : [op(e1, e1) = op(e2, e1)], (1766 ^ _412364) ^ [] : [op(e1, e1) = op(e3, e1)], (1768 ^ _412364) ^ [] : [op(e1, e1) = op(e4, e1)], (1770 ^ _412364) ^ [] : [op(e1, e1) = op(e5, e1)], (1772 ^ _412364) ^ [] : [op(e2, e1) = op(e3, e1)], (1774 ^ _412364) ^ [] : [op(e2, e1) = op(e4, e1)], (1776 ^ _412364) ^ [] : [op(e2, e1) = op(e5, e1)], (1778 ^ _412364) ^ [] : [op(e3, e1) = op(e4, e1)], (1780 ^ _412364) ^ [] : [op(e3, e1) = op(e5, e1)], (1782 ^ _412364) ^ [] : [op(e4, e1) = op(e5, e1)], (1784 ^ _412364) ^ [] : [op(e0, e2) = op(e1, e2)], (1786 ^ _412364) ^ [] : [op(e0, e2) = op(e2, e2)], (1788 ^ _412364) ^ [] : [op(e0, e2) = op(e3, e2)], (1790 ^ _412364) ^ [] : [op(e0, e2) = op(e4, e2)], (1792 ^ _412364) ^ [] : [op(e0, e2) = op(e5, e2)], (1794 ^ _412364) ^ [] : [op(e1, e2) = op(e2, e2)], (1796 ^ _412364) ^ [] : [op(e1, e2) = op(e3, e2)], (1798 ^ _412364) ^ [] : [op(e1, e2) = op(e4, e2)], (1800 ^ _412364) ^ [] : [op(e1, e2) = op(e5, e2)], (1802 ^ _412364) ^ [] : [op(e2, e2) = op(e3, e2)], (1804 ^ _412364) ^ [] : [op(e2, e2) = op(e4, e2)], (1806 ^ _412364) ^ [] : [op(e2, e2) = op(e5, e2)], (1808 ^ _412364) ^ [] : [op(e3, e2) = op(e4, e2)], (1810 ^ _412364) ^ [] : [op(e3, e2) = op(e5, e2)], (1812 ^ _412364) ^ [] : [op(e4, e2) = op(e5, e2)], (1814 ^ _412364) ^ [] : [op(e0, e3) = op(e1, e3)], (1816 ^ _412364) ^ [] : [op(e0, e3) = op(e2, e3)], (1818 ^ _412364) ^ [] : [op(e0, e3) = op(e3, e3)], (1820 ^ _412364) ^ [] : [op(e0, e3) = op(e4, e3)], (1822 ^ _412364) ^ [] : [op(e0, e3) = op(e5, e3)], (1824 ^ _412364) ^ [] : [op(e1, e3) = op(e2, e3)], (1826 ^ _412364) ^ [] : [op(e1, e3) = op(e3, e3)], (1828 ^ _412364) ^ [] : [op(e1, e3) = op(e4, e3)], (1830 ^ _412364) ^ [] : [op(e1, e3) = op(e5, e3)], (1832 ^ _412364) ^ [] : [op(e2, e3) = op(e3, e3)], (1834 ^ _412364) ^ [] : [op(e2, e3) = op(e4, e3)], (1836 ^ _412364) ^ [] : [op(e2, e3) = op(e5, e3)], (1838 ^ _412364) ^ [] : [op(e3, e3) = op(e4, e3)], (1840 ^ _412364) ^ [] : [op(e3, e3) = op(e5, e3)], (1842 ^ _412364) ^ [] : [op(e4, e3) = op(e5, e3)], (1844 ^ _412364) ^ [] : [op(e0, e4) = op(e1, e4)], (1846 ^ _412364) ^ [] : [op(e0, e4) = op(e2, e4)], (1848 ^ _412364) ^ [] : [op(e0, e4) = op(e3, e4)], (1850 ^ _412364) ^ [] : [op(e0, e4) = op(e4, e4)], (1852 ^ _412364) ^ [] : [op(e0, e4) = op(e5, e4)], (1854 ^ _412364) ^ [] : [op(e1, e4) = op(e2, e4)], (1856 ^ _412364) ^ [] : [op(e1, e4) = op(e3, e4)], (1858 ^ _412364) ^ [] : [op(e1, e4) = op(e4, e4)], (1860 ^ _412364) ^ [] : [op(e1, e4) = op(e5, e4)], (1862 ^ _412364) ^ [] : [op(e2, e4) = op(e3, e4)], (1864 ^ _412364) ^ [] : [op(e2, e4) = op(e4, e4)], (1866 ^ _412364) ^ [] : [op(e2, e4) = op(e5, e4)], (1868 ^ _412364) ^ [] : [op(e3, e4) = op(e4, e4)], (1870 ^ _412364) ^ [] : [op(e3, e4) = op(e5, e4)], (1872 ^ _412364) ^ [] : [op(e4, e4) = op(e5, e4)], (1874 ^ _412364) ^ [] : [op(e0, e5) = op(e1, e5)], (1876 ^ _412364) ^ [] : [op(e0, e5) = op(e2, e5)], (1878 ^ _412364) ^ [] : [op(e0, e5) = op(e3, e5)], (1880 ^ _412364) ^ [] : [op(e0, e5) = op(e4, e5)], (1882 ^ _412364) ^ [] : [op(e0, e5) = op(e5, e5)], (1884 ^ _412364) ^ [] : [op(e1, e5) = op(e2, e5)], (1886 ^ _412364) ^ [] : [op(e1, e5) = op(e3, e5)], (1888 ^ _412364) ^ [] : [op(e1, e5) = op(e4, e5)], (1890 ^ _412364) ^ [] : [op(e1, e5) = op(e5, e5)], (1892 ^ _412364) ^ [] : [op(e2, e5) = op(e3, e5)], (1894 ^ _412364) ^ [] : [op(e2, e5) = op(e4, e5)], (1896 ^ _412364) ^ [] : [op(e2, e5) = op(e5, e5)], (1898 ^ _412364) ^ [] : [op(e3, e5) = op(e4, e5)], (1900 ^ _412364) ^ [] : [op(e3, e5) = op(e5, e5)], (1902 ^ _412364) ^ [] : [op(e4, e5) = op(e5, e5)], (1904 ^ _412364) ^ [] : [op(e0, e0) = op(e0, e1)], (1906 ^ _412364) ^ [] : [op(e0, e0) = op(e0, e2)], (1908 ^ _412364) ^ [] : [op(e0, e0) = op(e0, e3)], (1910 ^ _412364) ^ [] : [op(e0, e0) = op(e0, e4)], (1912 ^ _412364) ^ [] : [op(e0, e0) = op(e0, e5)], (1914 ^ _412364) ^ [] : [op(e0, e1) = op(e0, e2)], (1916 ^ _412364) ^ [] : [op(e0, e1) = op(e0, e3)], (1918 ^ _412364) ^ [] : [op(e0, e1) = op(e0, e4)], (1920 ^ _412364) ^ [] : [op(e0, e1) = op(e0, e5)], (1922 ^ _412364) ^ [] : [op(e0, e2) = op(e0, e3)], (1924 ^ _412364) ^ [] : [op(e0, e2) = op(e0, e4)], (1926 ^ _412364) ^ [] : [op(e0, e2) = op(e0, e5)], (1928 ^ _412364) ^ [] : [op(e0, e3) = op(e0, e4)], (1930 ^ _412364) ^ [] : [op(e0, e3) = op(e0, e5)], (1932 ^ _412364) ^ [] : [op(e0, e4) = op(e0, e5)], (1934 ^ _412364) ^ [] : [op(e1, e0) = op(e1, e1)], (1936 ^ _412364) ^ [] : [op(e1, e0) = op(e1, e2)], (1938 ^ _412364) ^ [] : [op(e1, e0) = op(e1, e3)], (1940 ^ _412364) ^ [] : [op(e1, e0) = op(e1, e4)], (1942 ^ _412364) ^ [] : [op(e1, e0) = op(e1, e5)], (1944 ^ _412364) ^ [] : [op(e1, e1) = op(e1, e2)], (1946 ^ _412364) ^ [] : [op(e1, e1) = op(e1, e3)], (1948 ^ _412364) ^ [] : [op(e1, e1) = op(e1, e4)], (1950 ^ _412364) ^ [] : [op(e1, e1) = op(e1, e5)], (1952 ^ _412364) ^ [] : [op(e1, e2) = op(e1, e3)], (1954 ^ _412364) ^ [] : [op(e1, e2) = op(e1, e4)], (1956 ^ _412364) ^ [] : [op(e1, e2) = op(e1, e5)], (1958 ^ _412364) ^ [] : [op(e1, e3) = op(e1, e4)], (1960 ^ _412364) ^ [] : [op(e1, e3) = op(e1, e5)], (1962 ^ _412364) ^ [] : [op(e1, e4) = op(e1, e5)], (1964 ^ _412364) ^ [] : [op(e2, e0) = op(e2, e1)], (1966 ^ _412364) ^ [] : [op(e2, e0) = op(e2, e2)], (1968 ^ _412364) ^ [] : [op(e2, e0) = op(e2, e3)], (1970 ^ _412364) ^ [] : [op(e2, e0) = op(e2, e4)], (1972 ^ _412364) ^ [] : [op(e2, e0) = op(e2, e5)], (1974 ^ _412364) ^ [] : [op(e2, e1) = op(e2, e2)], (1976 ^ _412364) ^ [] : [op(e2, e1) = op(e2, e3)], (1978 ^ _412364) ^ [] : [op(e2, e1) = op(e2, e4)], (1980 ^ _412364) ^ [] : [op(e2, e1) = op(e2, e5)], (1982 ^ _412364) ^ [] : [op(e2, e2) = op(e2, e3)], (1984 ^ _412364) ^ [] : [op(e2, e2) = op(e2, e4)], (1986 ^ _412364) ^ [] : [op(e2, e2) = op(e2, e5)], (1988 ^ _412364) ^ [] : [op(e2, e3) = op(e2, e4)], (1990 ^ _412364) ^ [] : [op(e2, e3) = op(e2, e5)], (1992 ^ _412364) ^ [] : [op(e2, e4) = op(e2, e5)], (1994 ^ _412364) ^ [] : [op(e3, e0) = op(e3, e1)], (1996 ^ _412364) ^ [] : [op(e3, e0) = op(e3, e2)], (1998 ^ _412364) ^ [] : [op(e3, e0) = op(e3, e3)], (2000 ^ _412364) ^ [] : [op(e3, e0) = op(e3, e4)], (2002 ^ _412364) ^ [] : [op(e3, e0) = op(e3, e5)], (2004 ^ _412364) ^ [] : [op(e3, e1) = op(e3, e2)], (2006 ^ _412364) ^ [] : [op(e3, e1) = op(e3, e3)], (2008 ^ _412364) ^ [] : [op(e3, e1) = op(e3, e4)], (2010 ^ _412364) ^ [] : [op(e3, e1) = op(e3, e5)], (2012 ^ _412364) ^ [] : [op(e3, e2) = op(e3, e3)], (2014 ^ _412364) ^ [] : [op(e3, e2) = op(e3, e4)], (2016 ^ _412364) ^ [] : [op(e3, e2) = op(e3, e5)], (2018 ^ _412364) ^ [] : [op(e3, e3) = op(e3, e4)], (2020 ^ _412364) ^ [] : [op(e3, e3) = op(e3, e5)], (2022 ^ _412364) ^ [] : [op(e3, e4) = op(e3, e5)], (2024 ^ _412364) ^ [] : [op(e4, e0) = op(e4, e1)], (2026 ^ _412364) ^ [] : [op(e4, e0) = op(e4, e2)], (2028 ^ _412364) ^ [] : [op(e4, e0) = op(e4, e3)], (2030 ^ _412364) ^ [] : [op(e4, e0) = op(e4, e4)], (2032 ^ _412364) ^ [] : [op(e4, e0) = op(e4, e5)], (2034 ^ _412364) ^ [] : [op(e4, e1) = op(e4, e2)], (2036 ^ _412364) ^ [] : [op(e4, e1) = op(e4, e3)], (2038 ^ _412364) ^ [] : [op(e4, e1) = op(e4, e4)], (2040 ^ _412364) ^ [] : [op(e4, e1) = op(e4, e5)], (2042 ^ _412364) ^ [] : [op(e4, e2) = op(e4, e3)], (2044 ^ _412364) ^ [] : [op(e4, e2) = op(e4, e4)], (2046 ^ _412364) ^ [] : [op(e4, e2) = op(e4, e5)], (2048 ^ _412364) ^ [] : [op(e4, e3) = op(e4, e4)], (2050 ^ _412364) ^ [] : [op(e4, e3) = op(e4, e5)], (2052 ^ _412364) ^ [] : [op(e4, e4) = op(e4, e5)], (2054 ^ _412364) ^ [] : [op(e5, e0) = op(e5, e1)], (2056 ^ _412364) ^ [] : [op(e5, e0) = op(e5, e2)], (2058 ^ _412364) ^ [] : [op(e5, e0) = op(e5, e3)], (2060 ^ _412364) ^ [] : [op(e5, e0) = op(e5, e4)], (2062 ^ _412364) ^ [] : [op(e5, e0) = op(e5, e5)], (2064 ^ _412364) ^ [] : [op(e5, e1) = op(e5, e2)], (2066 ^ _412364) ^ [] : [op(e5, e1) = op(e5, e3)], (2068 ^ _412364) ^ [] : [op(e5, e1) = op(e5, e4)], (2070 ^ _412364) ^ [] : [op(e5, e1) = op(e5, e5)], (2072 ^ _412364) ^ [] : [op(e5, e2) = op(e5, e3)], (2074 ^ _412364) ^ [] : [op(e5, e2) = op(e5, e4)], (2076 ^ _412364) ^ [] : [op(e5, e2) = op(e5, e5)], (2078 ^ _412364) ^ [] : [op(e5, e3) = op(e5, e4)], (2080 ^ _412364) ^ [] : [op(e5, e3) = op(e5, e5)], (2082 ^ _412364) ^ [] : [op(e5, e4) = op(e5, e5)], (2084 ^ _412364) ^ [] : [e0 = e1], (2086 ^ _412364) ^ [] : [e0 = e2], (2088 ^ _412364) ^ [] : [e0 = e3], (2090 ^ _412364) ^ [] : [e0 = e4], (2092 ^ _412364) ^ [] : [e0 = e5], (2094 ^ _412364) ^ [] : [e1 = e2], (2096 ^ _412364) ^ [] : [e1 = e3], (2098 ^ _412364) ^ [] : [e1 = e4], (2100 ^ _412364) ^ [] : [e1 = e5], (2102 ^ _412364) ^ [] : [e2 = e3], (2104 ^ _412364) ^ [] : [e2 = e4], (2106 ^ _412364) ^ [] : [e2 = e5], (2108 ^ _412364) ^ [] : [e3 = e4], (2110 ^ _412364) ^ [] : [e3 = e5], (2112 ^ _412364) ^ [] : [e4 = e5], (1478 ^ _412364) ^ [] : [inv(e0) = e0, -(inv(e0) = e0)], (1484 ^ _412364) ^ [] : [inv(e0) = e1, -(inv(e1) = e0)], (1490 ^ _412364) ^ [] : [inv(e0) = e2, -(inv(e2) = e0)], (1496 ^ _412364) ^ [] : [inv(e0) = e3, -(inv(e3) = e0)], (1502 ^ _412364) ^ [] : [inv(e0) = e4, -(inv(e4) = e0)], (1508 ^ _412364) ^ [] : [inv(e0) = e5, -(inv(e5) = e0)], (1514 ^ _412364) ^ [] : [inv(e1) = e0, -(inv(e0) = e1)], (1520 ^ _412364) ^ [] : [inv(e1) = e1, -(inv(e1) = e1)], (1526 ^ _412364) ^ [] : [inv(e1) = e2, -(inv(e2) = e1)], (1532 ^ _412364) ^ [] : [inv(e1) = e3, -(inv(e3) = e1)], (1538 ^ _412364) ^ [] : [inv(e1) = e4, -(inv(e4) = e1)], (1544 ^ _412364) ^ [] : [inv(e1) = e5, -(inv(e5) = e1)], (1550 ^ _412364) ^ [] : [inv(e2) = e0, -(inv(e0) = e2)], (1556 ^ _412364) ^ [] : [inv(e2) = e1, -(inv(e1) = e2)], (1562 ^ _412364) ^ [] : [inv(e2) = e2, -(inv(e2) = e2)], (1568 ^ _412364) ^ [] : [inv(e2) = e3, -(inv(e3) = e2)], (1574 ^ _412364) ^ [] : [inv(e2) = e4, -(inv(e4) = e2)], (1580 ^ _412364) ^ [] : [inv(e2) = e5, -(inv(e5) = e2)], (1586 ^ _412364) ^ [] : [inv(e3) = e0, -(inv(e0) = e3)], (1592 ^ _412364) ^ [] : [inv(e3) = e1, -(inv(e1) = e3)], (1598 ^ _412364) ^ [] : [inv(e3) = e2, -(inv(e2) = e3)], (1604 ^ _412364) ^ [] : [inv(e3) = e3, -(inv(e3) = e3)], (1610 ^ _412364) ^ [] : [inv(e3) = e4, -(inv(e4) = e3)], (1616 ^ _412364) ^ [] : [inv(e3) = e5, -(inv(e5) = e3)], (1622 ^ _412364) ^ [] : [inv(e4) = e0, -(inv(e0) = e4)], (1628 ^ _412364) ^ [] : [inv(e4) = e1, -(inv(e1) = e4)], (1634 ^ _412364) ^ [] : [inv(e4) = e2, -(inv(e2) = e4)], (1640 ^ _412364) ^ [] : [inv(e4) = e3, -(inv(e3) = e4)], (1646 ^ _412364) ^ [] : [inv(e4) = e4, -(inv(e4) = e4)], (1652 ^ _412364) ^ [] : [inv(e4) = e5, -(inv(e5) = e4)], (1658 ^ _412364) ^ [] : [inv(e5) = e0, -(inv(e0) = e5)], (1664 ^ _412364) ^ [] : [inv(e5) = e1, -(inv(e1) = e5)], (1670 ^ _412364) ^ [] : [inv(e5) = e2, -(inv(e2) = e5)], (1676 ^ _412364) ^ [] : [inv(e5) = e3, -(inv(e3) = e5)], (1682 ^ _412364) ^ [] : [inv(e5) = e4, -(inv(e4) = e5)], (1688 ^ _412364) ^ [] : [inv(e5) = e5, -(inv(e5) = e5)], (36 ^ _412364) ^ [] : [-(op(e0, e0) = e0), -(op(e0, e0) = e1), -(op(e0, e0) = e2), -(op(e0, e0) = e3), -(op(e0, e0) = e4), -(op(e0, e0) = e5)], (58 ^ _412364) ^ [] : [-(op(e0, e1) = e0), -(op(e0, e1) = e1), -(op(e0, e1) = e2), -(op(e0, e1) = e3), -(op(e0, e1) = e4), -(op(e0, e1) = e5)], (80 ^ _412364) ^ [] : [-(op(e0, e2) = e0), -(op(e0, e2) = e1), -(op(e0, e2) = e2), -(op(e0, e2) = e3), -(op(e0, e2) = e4), -(op(e0, e2) = e5)], (102 ^ _412364) ^ [] : [-(op(e0, e3) = e0), -(op(e0, e3) = e1), -(op(e0, e3) = e2), -(op(e0, e3) = e3), -(op(e0, e3) = e4), -(op(e0, e3) = e5)], (124 ^ _412364) ^ [] : [-(op(e0, e4) = e0), -(op(e0, e4) = e1), -(op(e0, e4) = e2), -(op(e0, e4) = e3), -(op(e0, e4) = e4), -(op(e0, e4) = e5)], (146 ^ _412364) ^ [] : [-(op(e0, e5) = e0), -(op(e0, e5) = e1), -(op(e0, e5) = e2), -(op(e0, e5) = e3), -(op(e0, e5) = e4), -(op(e0, e5) = e5)], (168 ^ _412364) ^ [] : [-(op(e1, e0) = e0), -(op(e1, e0) = e1), -(op(e1, e0) = e2), -(op(e1, e0) = e3), -(op(e1, e0) = e4), -(op(e1, e0) = e5)], (190 ^ _412364) ^ [] : [-(op(e1, e1) = e0), -(op(e1, e1) = e1), -(op(e1, e1) = e2), -(op(e1, e1) = e3), -(op(e1, e1) = e4), -(op(e1, e1) = e5)], (212 ^ _412364) ^ [] : [-(op(e1, e2) = e0), -(op(e1, e2) = e1), -(op(e1, e2) = e2), -(op(e1, e2) = e3), -(op(e1, e2) = e4), -(op(e1, e2) = e5)], (234 ^ _412364) ^ [] : [-(op(e1, e3) = e0), -(op(e1, e3) = e1), -(op(e1, e3) = e2), -(op(e1, e3) = e3), -(op(e1, e3) = e4), -(op(e1, e3) = e5)], (256 ^ _412364) ^ [] : [-(op(e1, e4) = e0), -(op(e1, e4) = e1), -(op(e1, e4) = e2), -(op(e1, e4) = e3), -(op(e1, e4) = e4), -(op(e1, e4) = e5)], (278 ^ _412364) ^ [] : [-(op(e1, e5) = e0), -(op(e1, e5) = e1), -(op(e1, e5) = e2), -(op(e1, e5) = e3), -(op(e1, e5) = e4), -(op(e1, e5) = e5)], (300 ^ _412364) ^ [] : [-(op(e2, e0) = e0), -(op(e2, e0) = e1), -(op(e2, e0) = e2), -(op(e2, e0) = e3), -(op(e2, e0) = e4), -(op(e2, e0) = e5)], (322 ^ _412364) ^ [] : [-(op(e2, e1) = e0), -(op(e2, e1) = e1), -(op(e2, e1) = e2), -(op(e2, e1) = e3), -(op(e2, e1) = e4), -(op(e2, e1) = e5)], (344 ^ _412364) ^ [] : [-(op(e2, e2) = e0), -(op(e2, e2) = e1), -(op(e2, e2) = e2), -(op(e2, e2) = e3), -(op(e2, e2) = e4), -(op(e2, e2) = e5)], (366 ^ _412364) ^ [] : [-(op(e2, e3) = e0), -(op(e2, e3) = e1), -(op(e2, e3) = e2), -(op(e2, e3) = e3), -(op(e2, e3) = e4), -(op(e2, e3) = e5)], (388 ^ _412364) ^ [] : [-(op(e2, e4) = e0), -(op(e2, e4) = e1), -(op(e2, e4) = e2), -(op(e2, e4) = e3), -(op(e2, e4) = e4), -(op(e2, e4) = e5)], (410 ^ _412364) ^ [] : [-(op(e2, e5) = e0), -(op(e2, e5) = e1), -(op(e2, e5) = e2), -(op(e2, e5) = e3), -(op(e2, e5) = e4), -(op(e2, e5) = e5)], (432 ^ _412364) ^ [] : [-(op(e3, e0) = e0), -(op(e3, e0) = e1), -(op(e3, e0) = e2), -(op(e3, e0) = e3), -(op(e3, e0) = e4), -(op(e3, e0) = e5)], (454 ^ _412364) ^ [] : [-(op(e3, e1) = e0), -(op(e3, e1) = e1), -(op(e3, e1) = e2), -(op(e3, e1) = e3), -(op(e3, e1) = e4), -(op(e3, e1) = e5)], (476 ^ _412364) ^ [] : [-(op(e3, e2) = e0), -(op(e3, e2) = e1), -(op(e3, e2) = e2), -(op(e3, e2) = e3), -(op(e3, e2) = e4), -(op(e3, e2) = e5)], (498 ^ _412364) ^ [] : [-(op(e3, e3) = e0), -(op(e3, e3) = e1), -(op(e3, e3) = e2), -(op(e3, e3) = e3), -(op(e3, e3) = e4), -(op(e3, e3) = e5)], (520 ^ _412364) ^ [] : [-(op(e3, e4) = e0), -(op(e3, e4) = e1), -(op(e3, e4) = e2), -(op(e3, e4) = e3), -(op(e3, e4) = e4), -(op(e3, e4) = e5)], (542 ^ _412364) ^ [] : [-(op(e3, e5) = e0), -(op(e3, e5) = e1), -(op(e3, e5) = e2), -(op(e3, e5) = e3), -(op(e3, e5) = e4), -(op(e3, e5) = e5)], (564 ^ _412364) ^ [] : [-(op(e4, e0) = e0), -(op(e4, e0) = e1), -(op(e4, e0) = e2), -(op(e4, e0) = e3), -(op(e4, e0) = e4), -(op(e4, e0) = e5)], (586 ^ _412364) ^ [] : [-(op(e4, e1) = e0), -(op(e4, e1) = e1), -(op(e4, e1) = e2), -(op(e4, e1) = e3), -(op(e4, e1) = e4), -(op(e4, e1) = e5)], (608 ^ _412364) ^ [] : [-(op(e4, e2) = e0), -(op(e4, e2) = e1), -(op(e4, e2) = e2), -(op(e4, e2) = e3), -(op(e4, e2) = e4), -(op(e4, e2) = e5)], (630 ^ _412364) ^ [] : [-(op(e4, e3) = e0), -(op(e4, e3) = e1), -(op(e4, e3) = e2), -(op(e4, e3) = e3), -(op(e4, e3) = e4), -(op(e4, e3) = e5)], (652 ^ _412364) ^ [] : [-(op(e4, e4) = e0), -(op(e4, e4) = e1), -(op(e4, e4) = e2), -(op(e4, e4) = e3), -(op(e4, e4) = e4), -(op(e4, e4) = e5)], (674 ^ _412364) ^ [] : [-(op(e4, e5) = e0), -(op(e4, e5) = e1), -(op(e4, e5) = e2), -(op(e4, e5) = e3), -(op(e4, e5) = e4), -(op(e4, e5) = e5)], (696 ^ _412364) ^ [] : [-(op(e5, e0) = e0), -(op(e5, e0) = e1), -(op(e5, e0) = e2), -(op(e5, e0) = e3), -(op(e5, e0) = e4), -(op(e5, e0) = e5)], (718 ^ _412364) ^ [] : [-(op(e5, e1) = e0), -(op(e5, e1) = e1), -(op(e5, e1) = e2), -(op(e5, e1) = e3), -(op(e5, e1) = e4), -(op(e5, e1) = e5)], (740 ^ _412364) ^ [] : [-(op(e5, e2) = e0), -(op(e5, e2) = e1), -(op(e5, e2) = e2), -(op(e5, e2) = e3), -(op(e5, e2) = e4), -(op(e5, e2) = e5)], (762 ^ _412364) ^ [] : [-(op(e5, e3) = e0), -(op(e5, e3) = e1), -(op(e5, e3) = e2), -(op(e5, e3) = e3), -(op(e5, e3) = e4), -(op(e5, e3) = e5)], (784 ^ _412364) ^ [] : [-(op(e5, e4) = e0), -(op(e5, e4) = e1), -(op(e5, e4) = e2), -(op(e5, e4) = e3), -(op(e5, e4) = e4), -(op(e5, e4) = e5)], (806 ^ _412364) ^ [] : [-(op(e5, e5) = e0), -(op(e5, e5) = e1), -(op(e5, e5) = e2), -(op(e5, e5) = e3), -(op(e5, e5) = e4), -(op(e5, e5) = e5)]], input).
% 0.34/1.38 ncf('1',plain,[op(e0, e0) = op(e0, e0), op(e0, e1) = op(e1, e0), op(e0, e2) = op(e2, e0), op(e0, e3) = op(e3, e0), op(e0, e4) = op(e4, e0), op(e0, e5) = op(e5, e0), op(e1, e0) = op(e0, e1), op(e1, e1) = op(e1, e1), op(e1, e2) = op(e2, e1), op(e1, e3) = op(e3, e1), op(e1, e4) = op(e4, e1), op(e1, e5) = op(e5, e1), op(e2, e0) = op(e0, e2), op(e2, e1) = op(e1, e2), op(e2, e2) = op(e2, e2), op(e2, e3) = op(e3, e2), op(e2, e4) = op(e4, e2), op(e2, e5) = op(e5, e2), op(e3, e0) = op(e0, e3), op(e3, e1) = op(e1, e3), op(e3, e2) = op(e2, e3), op(e3, e3) = op(e3, e3), op(e3, e4) = op(e4, e3), op(e3, e5) = op(e5, e3), op(e4, e0) = op(e0, e4), op(e4, e1) = op(e1, e4), op(e4, e2) = op(e2, e4), op(e4, e3) = op(e3, e4), op(e4, e4) = op(e4, e4), op(e4, e5) = op(e5, e4), op(e5, e0) = op(e0, e5), op(e5, e1) = op(e1, e5), op(e5, e2) = op(e2, e5), op(e5, e3) = op(e3, e5), op(e5, e4) = op(e4, e5), op(e5, e5) = op(e5, e5)],start(2114 ^ 0)).
% 0.34/1.38 ncf('1.1',plain,[-(op(e0, e0) = op(e0, e0))],extension(2256 ^ 1)).
% 0.34/1.38 ncf('1.2',plain,[-(op(e0, e1) = op(e1, e0))],extension(2258 ^ 1)).
% 0.34/1.38 ncf('1.3',plain,[-(op(e0, e2) = op(e2, e0))],extension(2260 ^ 1)).
% 0.34/1.38 ncf('1.4',plain,[-(op(e0, e3) = op(e3, e0))],extension(2262 ^ 1)).
% 0.34/1.38 ncf('1.5',plain,[-(op(e0, e4) = op(e4, e0))],extension(2264 ^ 1)).
% 0.34/1.38 ncf('1.6',plain,[-(op(e0, e5) = op(e5, e0))],extension(2266 ^ 1)).
% 0.34/1.38 ncf('1.7',plain,[-(op(e1, e0) = op(e0, e1))],extension(2268 ^ 1)).
% 0.34/1.38 ncf('1.8',plain,[-(op(e1, e1) = op(e1, e1))],extension(2270 ^ 1)).
% 0.34/1.38 ncf('1.9',plain,[-(op(e1, e2) = op(e2, e1))],extension(2272 ^ 1)).
% 0.34/1.38 ncf('1.10',plain,[-(op(e1, e3) = op(e3, e1))],extension(2274 ^ 1)).
% 0.34/1.38 ncf('1.11',plain,[-(op(e1, e4) = op(e4, e1))],extension(2276 ^ 1)).
% 0.34/1.38 ncf('1.12',plain,[-(op(e1, e5) = op(e5, e1))],extension(2278 ^ 1)).
% 0.34/1.38 ncf('1.13',plain,[-(op(e2, e0) = op(e0, e2))],extension(2280 ^ 1)).
% 0.34/1.38 ncf('1.14',plain,[-(op(e2, e1) = op(e1, e2))],extension(2282 ^ 1)).
% 0.34/1.38 ncf('1.15',plain,[-(op(e2, e2) = op(e2, e2))],extension(2284 ^ 1)).
% 0.34/1.38 ncf('1.16',plain,[-(op(e2, e3) = op(e3, e2))],extension(2286 ^ 1)).
% 0.34/1.38 ncf('1.17',plain,[-(op(e2, e4) = op(e4, e2))],extension(2288 ^ 1)).
% 0.34/1.38 ncf('1.18',plain,[-(op(e2, e5) = op(e5, e2))],extension(2290 ^ 1)).
% 0.34/1.38 ncf('1.19',plain,[-(op(e3, e0) = op(e0, e3))],extension(2292 ^ 1)).
% 0.34/1.38 ncf('1.20',plain,[-(op(e3, e1) = op(e1, e3))],extension(2294 ^ 1)).
% 0.34/1.38 ncf('1.21',plain,[-(op(e3, e2) = op(e2, e3))],extension(2296 ^ 1)).
% 0.34/1.38 ncf('1.22',plain,[-(op(e3, e3) = op(e3, e3))],extension(2298 ^ 1)).
% 0.34/1.38 ncf('1.23',plain,[-(op(e3, e4) = op(e4, e3))],extension(2300 ^ 1)).
% 0.34/1.38 ncf('1.24',plain,[-(op(e3, e5) = op(e5, e3))],extension(2302 ^ 1)).
% 0.34/1.38 ncf('1.25',plain,[-(op(e4, e0) = op(e0, e4))],extension(2304 ^ 1)).
% 0.34/1.38 ncf('1.26',plain,[-(op(e4, e1) = op(e1, e4))],extension(2306 ^ 1)).
% 0.34/1.38 ncf('1.27',plain,[-(op(e4, e2) = op(e2, e4))],extension(2308 ^ 1)).
% 0.34/1.38 ncf('1.28',plain,[-(op(e4, e3) = op(e3, e4))],extension(2310 ^ 1)).
% 0.34/1.38 ncf('1.29',plain,[-(op(e4, e4) = op(e4, e4))],extension(2312 ^ 1)).
% 0.34/1.38 ncf('1.30',plain,[-(op(e4, e5) = op(e5, e4))],extension(2314 ^ 1)).
% 0.34/1.38 ncf('1.31',plain,[-(op(e5, e0) = op(e0, e5))],extension(2316 ^ 1)).
% 0.34/1.38 ncf('1.32',plain,[-(op(e5, e1) = op(e1, e5))],extension(2318 ^ 1)).
% 0.34/1.38 ncf('1.33',plain,[-(op(e5, e2) = op(e2, e5))],extension(2320 ^ 1)).
% 0.34/1.38 ncf('1.34',plain,[-(op(e5, e3) = op(e3, e5))],extension(2322 ^ 1)).
% 0.34/1.38 ncf('1.35',plain,[-(op(e5, e4) = op(e4, e5))],extension(2324 ^ 1)).
% 0.34/1.38 ncf('1.36',plain,[-(op(e5, e5) = op(e5, e5))],extension(2326 ^ 1)).
% 0.34/1.38 %-----------------------------------------------------
% 0.34/1.38 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------