%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : ALG028+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n032.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 : 0s
% DateTime : Thu Jul 14 12:09:10 EDT 2022
% Result : Theorem 0.69s 1.10s
% Output : Refutation 0.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.08 % Problem : ALG028+1 : TPTP v8.1.0. Released v2.7.0.
% 0.07/0.08 % Command : bliksem %s
% 0.07/0.27 % Computer : n032.cluster.edu
% 0.07/0.27 % Model : x86_64 x86_64
% 0.07/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.27 % Memory : 8042.1875MB
% 0.07/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.27 % CPULimit : 300
% 0.07/0.27 % DateTime : Wed Jun 8 07:31:06 EDT 2022
% 0.07/0.27 % CPUTime :
% 0.69/1.10 *** allocated 10000 integers for termspace/termends
% 0.69/1.10 *** allocated 10000 integers for clauses
% 0.69/1.10 *** allocated 10000 integers for justifications
% 0.69/1.10 Bliksem 1.12
% 0.69/1.10
% 0.69/1.10
% 0.69/1.10 Automatic Strategy Selection
% 0.69/1.10
% 0.69/1.10 *** allocated 15000 integers for termspace/termends
% 0.69/1.10 *** allocated 22500 integers for termspace/termends
% 0.69/1.10
% 0.69/1.10 Clauses:
% 0.69/1.10
% 0.69/1.10 { op( e0, e0 ) = e0, op( e0, e0 ) = e1, op( e0, e0 ) = e2, op( e0, e0 ) =
% 0.69/1.10 e3, op( e0, e0 ) = e4, op( e0, e0 ) = e5 }.
% 0.69/1.10 { op( e0, e1 ) = e0, op( e0, e1 ) = e1, op( e0, e1 ) = e2, op( e0, e1 ) =
% 0.69/1.10 e3, op( e0, e1 ) = e4, op( e0, e1 ) = e5 }.
% 0.69/1.10 { op( e0, e2 ) = e0, op( e0, e2 ) = e1, op( e0, e2 ) = e2, op( e0, e2 ) =
% 0.69/1.10 e3, op( e0, e2 ) = e4, op( e0, e2 ) = e5 }.
% 0.69/1.10 { op( e0, e3 ) = e0, op( e0, e3 ) = e1, op( e0, e3 ) = e2, op( e0, e3 ) =
% 0.69/1.10 e3, op( e0, e3 ) = e4, op( e0, e3 ) = e5 }.
% 0.69/1.10 { op( e0, e4 ) = e0, op( e0, e4 ) = e1, op( e0, e4 ) = e2, op( e0, e4 ) =
% 0.69/1.10 e3, op( e0, e4 ) = e4, op( e0, e4 ) = e5 }.
% 0.69/1.10 { op( e0, e5 ) = e0, op( e0, e5 ) = e1, op( e0, e5 ) = e2, op( e0, e5 ) =
% 0.69/1.10 e3, op( e0, e5 ) = e4, op( e0, e5 ) = e5 }.
% 0.69/1.10 { op( e1, e0 ) = e0, op( e1, e0 ) = e1, op( e1, e0 ) = e2, op( e1, e0 ) =
% 0.69/1.10 e3, op( e1, e0 ) = e4, op( e1, e0 ) = e5 }.
% 0.69/1.10 { op( e1, e1 ) = e0, op( e1, e1 ) = e1, op( e1, e1 ) = e2, op( e1, e1 ) =
% 0.69/1.10 e3, op( e1, e1 ) = e4, op( e1, e1 ) = e5 }.
% 0.69/1.10 { op( e1, e2 ) = e0, op( e1, e2 ) = e1, op( e1, e2 ) = e2, op( e1, e2 ) =
% 0.69/1.10 e3, op( e1, e2 ) = e4, op( e1, e2 ) = e5 }.
% 0.69/1.10 { op( e1, e3 ) = e0, op( e1, e3 ) = e1, op( e1, e3 ) = e2, op( e1, e3 ) =
% 0.69/1.10 e3, op( e1, e3 ) = e4, op( e1, e3 ) = e5 }.
% 0.69/1.10 { op( e1, e4 ) = e0, op( e1, e4 ) = e1, op( e1, e4 ) = e2, op( e1, e4 ) =
% 0.69/1.10 e3, op( e1, e4 ) = e4, op( e1, e4 ) = e5 }.
% 0.69/1.10 { op( e1, e5 ) = e0, op( e1, e5 ) = e1, op( e1, e5 ) = e2, op( e1, e5 ) =
% 0.69/1.10 e3, op( e1, e5 ) = e4, op( e1, e5 ) = e5 }.
% 0.69/1.10 { op( e2, e0 ) = e0, op( e2, e0 ) = e1, op( e2, e0 ) = e2, op( e2, e0 ) =
% 0.69/1.10 e3, op( e2, e0 ) = e4, op( e2, e0 ) = e5 }.
% 0.69/1.10 { op( e2, e1 ) = e0, op( e2, e1 ) = e1, op( e2, e1 ) = e2, op( e2, e1 ) =
% 0.69/1.10 e3, op( e2, e1 ) = e4, op( e2, e1 ) = e5 }.
% 0.69/1.10 { op( e2, e2 ) = e0, op( e2, e2 ) = e1, op( e2, e2 ) = e2, op( e2, e2 ) =
% 0.69/1.10 e3, op( e2, e2 ) = e4, op( e2, e2 ) = e5 }.
% 0.69/1.10 { op( e2, e3 ) = e0, op( e2, e3 ) = e1, op( e2, e3 ) = e2, op( e2, e3 ) =
% 0.69/1.10 e3, op( e2, e3 ) = e4, op( e2, e3 ) = e5 }.
% 0.69/1.10 { op( e2, e4 ) = e0, op( e2, e4 ) = e1, op( e2, e4 ) = e2, op( e2, e4 ) =
% 0.69/1.10 e3, op( e2, e4 ) = e4, op( e2, e4 ) = e5 }.
% 0.69/1.10 { op( e2, e5 ) = e0, op( e2, e5 ) = e1, op( e2, e5 ) = e2, op( e2, e5 ) =
% 0.69/1.10 e3, op( e2, e5 ) = e4, op( e2, e5 ) = e5 }.
% 0.69/1.10 { op( e3, e0 ) = e0, op( e3, e0 ) = e1, op( e3, e0 ) = e2, op( e3, e0 ) =
% 0.69/1.10 e3, op( e3, e0 ) = e4, op( e3, e0 ) = e5 }.
% 0.69/1.10 { op( e3, e1 ) = e0, op( e3, e1 ) = e1, op( e3, e1 ) = e2, op( e3, e1 ) =
% 0.69/1.10 e3, op( e3, e1 ) = e4, op( e3, e1 ) = e5 }.
% 0.69/1.10 { op( e3, e2 ) = e0, op( e3, e2 ) = e1, op( e3, e2 ) = e2, op( e3, e2 ) =
% 0.69/1.10 e3, op( e3, e2 ) = e4, op( e3, e2 ) = e5 }.
% 0.69/1.10 { op( e3, e3 ) = e0, op( e3, e3 ) = e1, op( e3, e3 ) = e2, op( e3, e3 ) =
% 0.69/1.10 e3, op( e3, e3 ) = e4, op( e3, e3 ) = e5 }.
% 0.69/1.10 { op( e3, e4 ) = e0, op( e3, e4 ) = e1, op( e3, e4 ) = e2, op( e3, e4 ) =
% 0.69/1.10 e3, op( e3, e4 ) = e4, op( e3, e4 ) = e5 }.
% 0.69/1.10 { op( e3, e5 ) = e0, op( e3, e5 ) = e1, op( e3, e5 ) = e2, op( e3, e5 ) =
% 0.69/1.10 e3, op( e3, e5 ) = e4, op( e3, e5 ) = e5 }.
% 0.69/1.10 { op( e4, e0 ) = e0, op( e4, e0 ) = e1, op( e4, e0 ) = e2, op( e4, e0 ) =
% 0.69/1.10 e3, op( e4, e0 ) = e4, op( e4, e0 ) = e5 }.
% 0.69/1.10 { op( e4, e1 ) = e0, op( e4, e1 ) = e1, op( e4, e1 ) = e2, op( e4, e1 ) =
% 0.69/1.10 e3, op( e4, e1 ) = e4, op( e4, e1 ) = e5 }.
% 0.69/1.10 { op( e4, e2 ) = e0, op( e4, e2 ) = e1, op( e4, e2 ) = e2, op( e4, e2 ) =
% 0.69/1.10 e3, op( e4, e2 ) = e4, op( e4, e2 ) = e5 }.
% 0.69/1.10 { op( e4, e3 ) = e0, op( e4, e3 ) = e1, op( e4, e3 ) = e2, op( e4, e3 ) =
% 0.69/1.10 e3, op( e4, e3 ) = e4, op( e4, e3 ) = e5 }.
% 0.69/1.10 { op( e4, e4 ) = e0, op( e4, e4 ) = e1, op( e4, e4 ) = e2, op( e4, e4 ) =
% 0.69/1.10 e3, op( e4, e4 ) = e4, op( e4, e4 ) = e5 }.
% 0.69/1.10 { op( e4, e5 ) = e0, op( e4, e5 ) = e1, op( e4, e5 ) = e2, op( e4, e5 ) =
% 0.69/1.10 e3, op( e4, e5 ) = e4, op( e4, e5 ) = e5 }.
% 0.69/1.10 { op( e5, e0 ) = e0, op( e5, e0 ) = e1, op( e5, e0 ) = e2, op( e5, e0 ) =
% 0.69/1.10 e3, op( e5, e0 ) = e4, op( e5, e0 ) = e5 }.
% 0.69/1.10 { op( e5, e1 ) = e0, op( e5, e1 ) = e1, op( e5, e1 ) = e2, op( e5, e1 ) =
% 0.69/1.10 e3, op( e5, e1 ) = e4, op( e5, e1 ) = e5 }.
% 0.69/1.10 { op( e5, e2 ) = e0, op( e5, e2 ) = e1, op( e5, e2 ) = e2, op( e5, e2 ) =
% 0.69/1.10 e3, op( e5, e2 ) = e4, op( e5, e2 ) = e5 }.
% 0.69/1.10 { op( e5, e3 ) = e0, op( e5, e3 ) = e1, op( e5, e3 ) = e2, op( e5, e3 ) =
% 0.69/1.10 e3, op( e5, e3 ) = e4, op( e5, e3 ) = e5 }.
% 0.69/1.10 { op( e5, e4 ) = e0, op( e5, e4 ) = e1, op( e5, e4 ) = e2, op( e5, e4 ) =
% 0.69/1.10 e3, op( e5, e4 ) = e4, op( e5, e4 ) = e5 }.
% 0.69/1.10 { op( e5, e5 ) = e0, op( e5, e5 ) = e1, op( e5, e5 ) = e2, op( e5, e5 ) =
% 0.69/1.10 e3, op( e5, e5 ) = e4, op( e5, e5 ) = e5 }.
% 0.69/1.10 { op( op( e0, e0 ), e0 ) = op( e0, op( e0, e0 ) ) }.
% 0.69/1.10 { op( op( e0, e0 ), e1 ) = op( e0, op( e0, e1 ) ) }.
% 0.69/1.10 { op( op( e0, e0 ), e2 ) = op( e0, op( e0, e2 ) ) }.
% 0.69/1.10 { op( op( e0, e0 ), e3 ) = op( e0, op( e0, e3 ) ) }.
% 0.69/1.10 { op( op( e0, e0 ), e4 ) = op( e0, op( e0, e4 ) ) }.
% 0.69/1.10 { op( op( e0, e0 ), e5 ) = op( e0, op( e0, e5 ) ) }.
% 0.69/1.10 { op( op( e0, e1 ), e0 ) = op( e0, op( e1, e0 ) ) }.
% 0.69/1.10 { op( op( e0, e1 ), e1 ) = op( e0, op( e1, e1 ) ) }.
% 0.69/1.10 { op( op( e0, e1 ), e2 ) = op( e0, op( e1, e2 ) ) }.
% 0.69/1.10 { op( op( e0, e1 ), e3 ) = op( e0, op( e1, e3 ) ) }.
% 0.69/1.10 { op( op( e0, e1 ), e4 ) = op( e0, op( e1, e4 ) ) }.
% 0.69/1.10 { op( op( e0, e1 ), e5 ) = op( e0, op( e1, e5 ) ) }.
% 0.69/1.10 { op( op( e0, e2 ), e0 ) = op( e0, op( e2, e0 ) ) }.
% 0.69/1.10 { op( op( e0, e2 ), e1 ) = op( e0, op( e2, e1 ) ) }.
% 0.69/1.10 { op( op( e0, e2 ), e2 ) = op( e0, op( e2, e2 ) ) }.
% 0.69/1.10 { op( op( e0, e2 ), e3 ) = op( e0, op( e2, e3 ) ) }.
% 0.69/1.10 { op( op( e0, e2 ), e4 ) = op( e0, op( e2, e4 ) ) }.
% 0.69/1.10 { op( op( e0, e2 ), e5 ) = op( e0, op( e2, e5 ) ) }.
% 0.69/1.10 { op( op( e0, e3 ), e0 ) = op( e0, op( e3, e0 ) ) }.
% 0.69/1.10 { op( op( e0, e3 ), e1 ) = op( e0, op( e3, e1 ) ) }.
% 0.69/1.10 { op( op( e0, e3 ), e2 ) = op( e0, op( e3, e2 ) ) }.
% 0.69/1.10 { op( op( e0, e3 ), e3 ) = op( e0, op( e3, e3 ) ) }.
% 0.69/1.10 { op( op( e0, e3 ), e4 ) = op( e0, op( e3, e4 ) ) }.
% 0.69/1.10 { op( op( e0, e3 ), e5 ) = op( e0, op( e3, e5 ) ) }.
% 0.69/1.10 { op( op( e0, e4 ), e0 ) = op( e0, op( e4, e0 ) ) }.
% 0.69/1.10 { op( op( e0, e4 ), e1 ) = op( e0, op( e4, e1 ) ) }.
% 0.69/1.10 { op( op( e0, e4 ), e2 ) = op( e0, op( e4, e2 ) ) }.
% 0.69/1.10 { op( op( e0, e4 ), e3 ) = op( e0, op( e4, e3 ) ) }.
% 0.69/1.10 { op( op( e0, e4 ), e4 ) = op( e0, op( e4, e4 ) ) }.
% 0.69/1.10 { op( op( e0, e4 ), e5 ) = op( e0, op( e4, e5 ) ) }.
% 0.69/1.10 { op( op( e0, e5 ), e0 ) = op( e0, op( e5, e0 ) ) }.
% 0.69/1.10 { op( op( e0, e5 ), e1 ) = op( e0, op( e5, e1 ) ) }.
% 0.69/1.10 { op( op( e0, e5 ), e2 ) = op( e0, op( e5, e2 ) ) }.
% 0.69/1.10 { op( op( e0, e5 ), e3 ) = op( e0, op( e5, e3 ) ) }.
% 0.69/1.10 { op( op( e0, e5 ), e4 ) = op( e0, op( e5, e4 ) ) }.
% 0.69/1.10 { op( op( e0, e5 ), e5 ) = op( e0, op( e5, e5 ) ) }.
% 0.69/1.10 { op( op( e1, e0 ), e0 ) = op( e1, op( e0, e0 ) ) }.
% 0.69/1.10 { op( op( e1, e0 ), e1 ) = op( e1, op( e0, e1 ) ) }.
% 0.69/1.10 { op( op( e1, e0 ), e2 ) = op( e1, op( e0, e2 ) ) }.
% 0.69/1.10 { op( op( e1, e0 ), e3 ) = op( e1, op( e0, e3 ) ) }.
% 0.69/1.10 { op( op( e1, e0 ), e4 ) = op( e1, op( e0, e4 ) ) }.
% 0.69/1.10 { op( op( e1, e0 ), e5 ) = op( e1, op( e0, e5 ) ) }.
% 0.69/1.10 { op( op( e1, e1 ), e0 ) = op( e1, op( e1, e0 ) ) }.
% 0.69/1.10 { op( op( e1, e1 ), e1 ) = op( e1, op( e1, e1 ) ) }.
% 0.69/1.10 { op( op( e1, e1 ), e2 ) = op( e1, op( e1, e2 ) ) }.
% 0.69/1.10 { op( op( e1, e1 ), e3 ) = op( e1, op( e1, e3 ) ) }.
% 0.69/1.10 { op( op( e1, e1 ), e4 ) = op( e1, op( e1, e4 ) ) }.
% 0.69/1.10 { op( op( e1, e1 ), e5 ) = op( e1, op( e1, e5 ) ) }.
% 0.69/1.10 { op( op( e1, e2 ), e0 ) = op( e1, op( e2, e0 ) ) }.
% 0.69/1.10 { op( op( e1, e2 ), e1 ) = op( e1, op( e2, e1 ) ) }.
% 0.69/1.10 { op( op( e1, e2 ), e2 ) = op( e1, op( e2, e2 ) ) }.
% 0.69/1.10 { op( op( e1, e2 ), e3 ) = op( e1, op( e2, e3 ) ) }.
% 0.69/1.10 { op( op( e1, e2 ), e4 ) = op( e1, op( e2, e4 ) ) }.
% 0.69/1.10 { op( op( e1, e2 ), e5 ) = op( e1, op( e2, e5 ) ) }.
% 0.69/1.10 { op( op( e1, e3 ), e0 ) = op( e1, op( e3, e0 ) ) }.
% 0.69/1.10 { op( op( e1, e3 ), e1 ) = op( e1, op( e3, e1 ) ) }.
% 0.69/1.10 { op( op( e1, e3 ), e2 ) = op( e1, op( e3, e2 ) ) }.
% 0.69/1.10 { op( op( e1, e3 ), e3 ) = op( e1, op( e3, e3 ) ) }.
% 0.69/1.10 { op( op( e1, e3 ), e4 ) = op( e1, op( e3, e4 ) ) }.
% 0.69/1.10 { op( op( e1, e3 ), e5 ) = op( e1, op( e3, e5 ) ) }.
% 0.69/1.10 { op( op( e1, e4 ), e0 ) = op( e1, op( e4, e0 ) ) }.
% 0.69/1.10 { op( op( e1, e4 ), e1 ) = op( e1, op( e4, e1 ) ) }.
% 0.69/1.10 { op( op( e1, e4 ), e2 ) = op( e1, op( e4, e2 ) ) }.
% 0.69/1.10 { op( op( e1, e4 ), e3 ) = op( e1, op( e4, e3 ) ) }.
% 0.69/1.10 { op( op( e1, e4 ), e4 ) = op( e1, op( e4, e4 ) ) }.
% 0.69/1.10 { op( op( e1, e4 ), e5 ) = op( e1, op( e4, e5 ) ) }.
% 0.69/1.10 { op( op( e1, e5 ), e0 ) = op( e1, op( e5, e0 ) ) }.
% 0.69/1.10 { op( op( e1, e5 ), e1 ) = op( e1, op( e5, e1 ) ) }.
% 0.69/1.10 { op( op( e1, e5 ), e2 ) = op( e1, op( e5, e2 ) ) }.
% 0.69/1.10 { op( op( e1, e5 ), e3 ) = op( e1, op( e5, e3 ) ) }.
% 0.69/1.10 { op( op( e1, e5 ), e4 ) = op( e1, op( e5, e4 ) ) }.
% 0.69/1.10 { op( op( e1, e5 ), e5 ) = op( e1, op( e5, e5 ) ) }.
% 0.69/1.10 { op( op( e2, e0 ), e0 ) = op( e2, op( e0, e0 ) ) }.
% 0.69/1.10 { op( op( e2, e0 ), e1 ) = op( e2, op( e0, e1 ) ) }.
% 0.69/1.10 { op( op( e2, e0 ), e2 ) = op( e2, op( e0, e2 ) ) }.
% 0.69/1.10 { op( op( e2, e0 ), e3 ) = op( e2, op( e0, e3 ) ) }.
% 0.69/1.10 { op( op( e2, e0 ), e4 ) = op( e2, op( e0, e4 ) ) }.
% 0.69/1.10 { op( op( e2, e0 ), e5 ) = op( e2, op( e0, e5 ) ) }.
% 0.69/1.10 { op( op( e2, e1 ), e0 ) = op( e2, op( e1, e0 ) ) }.
% 0.69/1.10 { op( op( e2, e1 ), e1 ) = op( e2, op( e1, e1 ) ) }.
% 0.69/1.10 { op( op( e2, e1 ), e2 ) = op( e2, op( e1, e2 ) ) }.
% 0.69/1.10 { op( op( e2, e1 ), e3 ) = op( e2, op( e1, e3 ) ) }.
% 0.69/1.10 { op( op( e2, e1 ), e4 ) = op( e2, op( e1, e4 ) ) }.
% 0.69/1.10 { op( op( e2, e1 ), e5 ) = op( e2, op( e1, e5 ) ) }.
% 0.69/1.10 { op( op( e2, e2 ), e0 ) = op( e2, op( e2, e0 ) ) }.
% 0.69/1.10 { op( op( e2, e2 ), e1 ) = op( e2, op( e2, e1 ) ) }.
% 0.69/1.10 { op( op( e2, e2 ), e2 ) = op( e2, op( e2, e2 ) ) }.
% 0.69/1.10 { op( op( e2, e2 ), e3 ) = op( e2, op( e2, e3 ) ) }.
% 0.69/1.10 { op( op( e2, e2 ), e4 ) = op( e2, op( e2, e4 ) ) }.
% 0.69/1.10 { op( op( e2, e2 ), e5 ) = op( e2, op( e2, e5 ) ) }.
% 0.69/1.10 { op( op( e2, e3 ), e0 ) = op( e2, op( e3, e0 ) ) }.
% 0.69/1.10 { op( op( e2, e3 ), e1 ) = op( e2, op( e3, e1 ) ) }.
% 0.69/1.10 { op( op( e2, e3 ), e2 ) = op( e2, op( e3, e2 ) ) }.
% 0.69/1.10 { op( op( e2, e3 ), e3 ) = op( e2, op( e3, e3 ) ) }.
% 0.69/1.10 { op( op( e2, e3 ), e4 ) = op( e2, op( e3, e4 ) ) }.
% 0.69/1.10 { op( op( e2, e3 ), e5 ) = op( e2, op( e3, e5 ) ) }.
% 0.69/1.10 { op( op( e2, e4 ), e0 ) = op( e2, op( e4, e0 ) ) }.
% 0.69/1.10 { op( op( e2, e4 ), e1 ) = op( e2, op( e4, e1 ) ) }.
% 0.69/1.10 { op( op( e2, e4 ), e2 ) = op( e2, op( e4, e2 ) ) }.
% 0.69/1.10 { op( op( e2, e4 ), e3 ) = op( e2, op( e4, e3 ) ) }.
% 0.69/1.10 { op( op( e2, e4 ), e4 ) = op( e2, op( e4, e4 ) ) }.
% 0.69/1.10 { op( op( e2, e4 ), e5 ) = op( e2, op( e4, e5 ) ) }.
% 0.69/1.10 { op( op( e2, e5 ), e0 ) = op( e2, op( e5, e0 ) ) }.
% 0.69/1.10 { op( op( e2, e5 ), e1 ) = op( e2, op( e5, e1 ) ) }.
% 0.69/1.10 { op( op( e2, e5 ), e2 ) = op( e2, op( e5, e2 ) ) }.
% 0.69/1.10 { op( op( e2, e5 ), e3 ) = op( e2, op( e5, e3 ) ) }.
% 0.69/1.10 { op( op( e2, e5 ), e4 ) = op( e2, op( e5, e4 ) ) }.
% 0.69/1.10 { op( op( e2, e5 ), e5 ) = op( e2, op( e5, e5 ) ) }.
% 0.69/1.10 { op( op( e3, e0 ), e0 ) = op( e3, op( e0, e0 ) ) }.
% 0.69/1.10 { op( op( e3, e0 ), e1 ) = op( e3, op( e0, e1 ) ) }.
% 0.69/1.10 { op( op( e3, e0 ), e2 ) = op( e3, op( e0, e2 ) ) }.
% 0.69/1.10 { op( op( e3, e0 ), e3 ) = op( e3, op( e0, e3 ) ) }.
% 0.69/1.10 { op( op( e3, e0 ), e4 ) = op( e3, op( e0, e4 ) ) }.
% 0.69/1.10 { op( op( e3, e0 ), e5 ) = op( e3, op( e0, e5 ) ) }.
% 0.69/1.10 { op( op( e3, e1 ), e0 ) = op( e3, op( e1, e0 ) ) }.
% 0.69/1.10 { op( op( e3, e1 ), e1 ) = op( e3, op( e1, e1 ) ) }.
% 0.69/1.10 { op( op( e3, e1 ), e2 ) = op( e3, op( e1, e2 ) ) }.
% 0.69/1.10 { op( op( e3, e1 ), e3 ) = op( e3, op( e1, e3 ) ) }.
% 0.69/1.10 { op( op( e3, e1 ), e4 ) = op( e3, op( e1, e4 ) ) }.
% 0.69/1.10 { op( op( e3, e1 ), e5 ) = op( e3, op( e1, e5 ) ) }.
% 0.69/1.10 { op( op( e3, e2 ), e0 ) = op( e3, op( e2, e0 ) ) }.
% 0.69/1.10 { op( op( e3, e2 ), e1 ) = op( e3, op( e2, e1 ) ) }.
% 0.69/1.10 { op( op( e3, e2 ), e2 ) = op( e3, op( e2, e2 ) ) }.
% 0.69/1.10 { op( op( e3, e2 ), e3 ) = op( e3, op( e2, e3 ) ) }.
% 0.69/1.10 { op( op( e3, e2 ), e4 ) = op( e3, op( e2, e4 ) ) }.
% 0.69/1.10 { op( op( e3, e2 ), e5 ) = op( e3, op( e2, e5 ) ) }.
% 0.69/1.10 { op( op( e3, e3 ), e0 ) = op( e3, op( e3, e0 ) ) }.
% 0.69/1.10 { op( op( e3, e3 ), e1 ) = op( e3, op( e3, e1 ) ) }.
% 0.69/1.10 { op( op( e3, e3 ), e2 ) = op( e3, op( e3, e2 ) ) }.
% 0.69/1.10 { op( op( e3, e3 ), e3 ) = op( e3, op( e3, e3 ) ) }.
% 0.69/1.10 { op( op( e3, e3 ), e4 ) = op( e3, op( e3, e4 ) ) }.
% 0.69/1.10 { op( op( e3, e3 ), e5 ) = op( e3, op( e3, e5 ) ) }.
% 0.69/1.10 { op( op( e3, e4 ), e0 ) = op( e3, op( e4, e0 ) ) }.
% 0.69/1.10 { op( op( e3, e4 ), e1 ) = op( e3, op( e4, e1 ) ) }.
% 0.69/1.10 { op( op( e3, e4 ), e2 ) = op( e3, op( e4, e2 ) ) }.
% 0.69/1.10 { op( op( e3, e4 ), e3 ) = op( e3, op( e4, e3 ) ) }.
% 0.69/1.10 { op( op( e3, e4 ), e4 ) = op( e3, op( e4, e4 ) ) }.
% 0.69/1.10 { op( op( e3, e4 ), e5 ) = op( e3, op( e4, e5 ) ) }.
% 0.69/1.10 { op( op( e3, e5 ), e0 ) = op( e3, op( e5, e0 ) ) }.
% 0.69/1.10 { op( op( e3, e5 ), e1 ) = op( e3, op( e5, e1 ) ) }.
% 0.69/1.10 { op( op( e3, e5 ), e2 ) = op( e3, op( e5, e2 ) ) }.
% 0.69/1.10 { op( op( e3, e5 ), e3 ) = op( e3, op( e5, e3 ) ) }.
% 0.69/1.10 { op( op( e3, e5 ), e4 ) = op( e3, op( e5, e4 ) ) }.
% 0.69/1.10 { op( op( e3, e5 ), e5 ) = op( e3, op( e5, e5 ) ) }.
% 0.69/1.10 { op( op( e4, e0 ), e0 ) = op( e4, op( e0, e0 ) ) }.
% 0.69/1.10 { op( op( e4, e0 ), e1 ) = op( e4, op( e0, e1 ) ) }.
% 0.69/1.10 { op( op( e4, e0 ), e2 ) = op( e4, op( e0, e2 ) ) }.
% 0.69/1.10 { op( op( e4, e0 ), e3 ) = op( e4, op( e0, e3 ) ) }.
% 0.69/1.10 { op( op( e4, e0 ), e4 ) = op( e4, op( e0, e4 ) ) }.
% 0.69/1.10 { op( op( e4, e0 ), e5 ) = op( e4, op( e0, e5 ) ) }.
% 0.69/1.10 { op( op( e4, e1 ), e0 ) = op( e4, op( e1, e0 ) ) }.
% 0.69/1.10 { op( op( e4, e1 ), e1 ) = op( e4, op( e1, e1 ) ) }.
% 0.69/1.10 { op( op( e4, e1 ), e2 ) = op( e4, op( e1, e2 ) ) }.
% 0.69/1.10 { op( op( e4, e1 ), e3 ) = op( e4, op( e1, e3 ) ) }.
% 0.69/1.10 { op( op( e4, e1 ), e4 ) = op( e4, op( e1, e4 ) ) }.
% 0.69/1.10 { op( op( e4, e1 ), e5 ) = op( e4, op( e1, e5 ) ) }.
% 0.69/1.10 { op( op( e4, e2 ), e0 ) = op( e4, op( e2, e0 ) ) }.
% 0.69/1.10 { op( op( e4, e2 ), e1 ) = op( e4, op( e2, e1 ) ) }.
% 0.69/1.10 { op( op( e4, e2 ), e2 ) = op( e4, op( e2, e2 ) ) }.
% 0.69/1.10 { op( op( e4, e2 ), e3 ) = op( e4, op( e2, e3 ) ) }.
% 0.69/1.10 { op( op( e4, e2 ), e4 ) = op( e4, op( e2, e4 ) ) }.
% 0.69/1.10 { op( op( e4, e2 ), e5 ) = op( e4, op( e2, e5 ) ) }.
% 0.69/1.10 { op( op( e4, e3 ), e0 ) = op( e4, op( e3, e0 ) ) }.
% 0.69/1.10 { op( op( e4, e3 ), e1 ) = op( e4, op( e3, e1 ) ) }.
% 0.69/1.10 { op( op( e4, e3 ), e2 ) = op( e4, op( e3, e2 ) ) }.
% 0.69/1.10 { op( op( e4, e3 ), e3 ) = op( e4, op( e3, e3 ) ) }.
% 0.69/1.10 { op( op( e4, e3 ), e4 ) = op( e4, op( e3, e4 ) ) }.
% 0.69/1.10 { op( op( e4, e3 ), e5 ) = op( e4, op( e3, e5 ) ) }.
% 0.69/1.10 { op( op( e4, e4 ), e0 ) = op( e4, op( e4, e0 ) ) }.
% 0.69/1.10 { op( op( e4, e4 ), e1 ) = op( e4, op( e4, e1 ) ) }.
% 0.69/1.10 { op( op( e4, e4 ), e2 ) = op( e4, op( e4, e2 ) ) }.
% 0.69/1.10 { op( op( e4, e4 ), e3 ) = op( e4, op( e4, e3 ) ) }.
% 0.69/1.10 { op( op( e4, e4 ), e4 ) = op( e4, op( e4, e4 ) ) }.
% 0.69/1.10 { op( op( e4, e4 ), e5 ) = op( e4, op( e4, e5 ) ) }.
% 0.69/1.10 { op( op( e4, e5 ), e0 ) = op( e4, op( e5, e0 ) ) }.
% 0.69/1.10 { op( op( e4, e5 ), e1 ) = op( e4, op( e5, e1 ) ) }.
% 0.69/1.10 { op( op( e4, e5 ), e2 ) = op( e4, op( e5, e2 ) ) }.
% 0.69/1.10 { op( op( e4, e5 ), e3 ) = op( e4, op( e5, e3 ) ) }.
% 0.69/1.10 { op( op( e4, e5 ), e4 ) = op( e4, op( e5, e4 ) ) }.
% 0.69/1.10 { op( op( e4, e5 ), e5 ) = op( e4, op( e5, e5 ) ) }.
% 0.69/1.10 { op( op( e5, e0 ), e0 ) = op( e5, op( e0, e0 ) ) }.
% 0.69/1.10 { op( op( e5, e0 ), e1 ) = op( e5, op( e0, e1 ) ) }.
% 0.69/1.10 { op( op( e5, e0 ), e2 ) = op( e5, op( e0, e2 ) ) }.
% 0.69/1.10 { op( op( e5, e0 ), e3 ) = op( e5, op( e0, e3 ) ) }.
% 0.69/1.10 { op( op( e5, e0 ), e4 ) = op( e5, op( e0, e4 ) ) }.
% 0.69/1.10 { op( op( e5, e0 ), e5 ) = op( e5, op( e0, e5 ) ) }.
% 0.69/1.10 { op( op( e5, e1 ), e0 ) = op( e5, op( e1, e0 ) ) }.
% 0.69/1.10 { op( op( e5, e1 ), e1 ) = op( e5, op( e1, e1 ) ) }.
% 0.69/1.10 { op( op( e5, e1 ), e2 ) = op( e5, op( e1, e2 ) ) }.
% 0.69/1.10 { op( op( e5, e1 ), e3 ) = op( e5, op( e1, e3 ) ) }.
% 0.69/1.10 { op( op( e5, e1 ), e4 ) = op( e5, op( e1, e4 ) ) }.
% 0.69/1.10 { op( op( e5, e1 ), e5 ) = op( e5, op( e1, e5 ) ) }.
% 0.69/1.10 { op( op( e5, e2 ), e0 ) = op( e5, op( e2, e0 ) ) }.
% 0.69/1.10 { op( op( e5, e2 ), e1 ) = op( e5, op( e2, e1 ) ) }.
% 0.69/1.10 { op( op( e5, e2 ), e2 ) = op( e5, op( e2, e2 ) ) }.
% 0.69/1.10 { op( op( e5, e2 ), e3 ) = op( e5, op( e2, e3 ) ) }.
% 0.69/1.10 { op( op( e5, e2 ), e4 ) = op( e5, op( e2, e4 ) ) }.
% 0.69/1.10 { op( op( e5, e2 ), e5 ) = op( e5, op( e2, e5 ) ) }.
% 0.69/1.10 { op( op( e5, e3 ), e0 ) = op( e5, op( e3, e0 ) ) }.
% 0.69/1.10 { op( op( e5, e3 ), e1 ) = op( e5, op( e3, e1 ) ) }.
% 0.69/1.10 { op( op( e5, e3 ), e2 ) = op( e5, op( e3, e2 ) ) }.
% 0.69/1.10 { op( op( e5, e3 ), e3 ) = op( e5, op( e3, e3 ) ) }.
% 0.69/1.10 { op( op( e5, e3 ), e4 ) = op( e5, op( e3, e4 ) ) }.
% 0.69/1.10 { op( op( e5, e3 ), e5 ) = op( e5, op( e3, e5 ) ) }.
% 0.69/1.10 { op( op( e5, e4 ), e0 ) = op( e5, op( e4, e0 ) ) }.
% 0.69/1.10 { op( op( e5, e4 ), e1 ) = op( e5, op( e4, e1 ) ) }.
% 0.69/1.10 { op( op( e5, e4 ), e2 ) = op( e5, op( e4, e2 ) ) }.
% 0.69/1.10 { op( op( e5, e4 ), e3 ) = op( e5, op( e4, e3 ) ) }.
% 0.69/1.10 { op( op( e5, e4 ), e4 ) = op( e5, op( e4, e4 ) ) }.
% 0.69/1.10 { op( op( e5, e4 ), e5 ) = op( e5, op( e4, e5 ) ) }.
% 0.69/1.10 { op( op( e5, e5 ), e0 ) = op( e5, op( e5, e0 ) ) }.
% 0.69/1.10 { op( op( e5, e5 ), e1 ) = op( e5, op( e5, e1 ) ) }.
% 0.69/1.10 { op( op( e5, e5 ), e2 ) = op( e5, op( e5, e2 ) ) }.
% 0.69/1.10 { op( op( e5, e5 ), e3 ) = op( e5, op( e5, e3 ) ) }.
% 0.69/1.10 { op( op( e5, e5 ), e4 ) = op( e5, op( e5, e4 ) ) }.
% 0.69/1.10 { op( op( e5, e5 ), e5 ) = op( e5, op( e5, e5 ) ) }.
% 0.69/1.10 { op( unit, e0 ) = e0 }.
% 0.69/1.10 { op( e0, unit ) = e0 }.
% 0.69/1.10 { op( unit, e1 ) = e1 }.
% 0.69/1.10 { op( e1, unit ) = e1 }.
% 0.69/1.10 { op( unit, e2 ) = e2 }.
% 0.69/1.10 { op( e2, unit ) = e2 }.
% 0.69/1.10 { op( unit, e3 ) = e3 }.
% 0.69/1.10 { op( e3, unit ) = e3 }.
% 0.69/1.10 { op( unit, e4 ) = e4 }.
% 0.69/1.10 { op( e4, unit ) = e4 }.
% 0.69/1.10 { op( unit, e5 ) = e5 }.
% 0.69/1.10 { op( e5, unit ) = e5 }.
% 0.69/1.10 { unit = e0, unit = e1, unit = e2, unit = e3, unit = e4, unit = e5 }.
% 0.69/1.10 { op( e0, inv( e0 ) ) = unit }.
% 0.69/1.10 { op( inv( e0 ), e0 ) = unit }.
% 0.69/1.10 { op( e1, inv( e1 ) ) = unit }.
% 0.69/1.10 { op( inv( e1 ), e1 ) = unit }.
% 0.69/1.10 { op( e2, inv( e2 ) ) = unit }.
% 0.69/1.10 { op( inv( e2 ), e2 ) = unit }.
% 0.69/1.10 { op( e3, inv( e3 ) ) = unit }.
% 0.69/1.10 { op( inv( e3 ), e3 ) = unit }.
% 0.69/1.10 { op( e4, inv( e4 ) ) = unit }.
% 0.69/1.10 { op( inv( e4 ), e4 ) = unit }.
% 0.69/1.10 { op( e5, inv( e5 ) ) = unit }.
% 0.69/1.10 { op( inv( e5 ), e5 ) = unit }.
% 0.69/1.10 { inv( e0 ) = e0, inv( e0 ) = e1, inv( e0 ) = e2, inv( e0 ) = e3, inv( e0 )
% 0.69/1.10 = e4, inv( e0 ) = e5 }.
% 0.69/1.10 { inv( e1 ) = e0, inv( e1 ) = e1, inv( e1 ) = e2, inv( e1 ) = e3, inv( e1 )
% 0.69/1.10 = e4, inv( e1 ) = e5 }.
% 0.69/1.10 { inv( e2 ) = e0, inv( e2 ) = e1, inv( e2 ) = e2, inv( e2 ) = e3, inv( e2 )
% 0.69/1.10 = e4, inv( e2 ) = e5 }.
% 0.69/1.10 { inv( e3 ) = e0, inv( e3 ) = e1, inv( e3 ) = e2, inv( e3 ) = e3, inv( e3 )
% 0.69/1.10 = e4, inv( e3 ) = e5 }.
% 0.69/1.10 { inv( e4 ) = e0, inv( e4 ) = e1, inv( e4 ) = e2, inv( e4 ) = e3, inv( e4 )
% 0.69/1.10 = e4, inv( e4 ) = e5 }.
% 0.69/1.10 { inv( e5 ) = e0, inv( e5 ) = e1, inv( e5 ) = e2, inv( e5 ) = e3, inv( e5 )
% 0.69/1.10 = e4, inv( e5 ) = e5 }.
% 0.69/1.10 { inv( unit ) = unit }.
% 0.69/1.10 { inv( inv( e0 ) ) = e0 }.
% 0.69/1.10 { inv( inv( e1 ) ) = e1 }.
% 0.69/1.10 { inv( inv( e2 ) ) = e2 }.
% 0.69/1.10 { inv( inv( e3 ) ) = e3 }.
% 0.69/1.10 { inv( inv( e4 ) ) = e4 }.
% 0.69/1.10 { inv( inv( e5 ) ) = e5 }.
% 0.69/1.10 { ! inv( e0 ) = e0, inv( e0 ) = e0 }.
% 0.69/1.10 { ! inv( e0 ) = e1, inv( e1 ) = e0 }.
% 0.69/1.10 { ! inv( e0 ) = e2, inv( e2 ) = e0 }.
% 0.69/1.10 { ! inv( e0 ) = e3, inv( e3 ) = e0 }.
% 0.69/1.10 { ! inv( e0 ) = e4, inv( e4 ) = e0 }.
% 0.69/1.10 { ! inv( e0 ) = e5, inv( e5 ) = e0 }.
% 0.69/1.10 { ! inv( e1 ) = e0, inv( e0 ) = e1 }.
% 0.69/1.10 { ! inv( e1 ) = e1, inv( e1 ) = e1 }.
% 0.69/1.10 { ! inv( e1 ) = e2, inv( e2 ) = e1 }.
% 0.69/1.10 { ! inv( e1 ) = e3, inv( e3 ) = e1 }.
% 0.69/1.10 { ! inv( e1 ) = e4, inv( e4 ) = e1 }.
% 0.69/1.10 { ! inv( e1 ) = e5, inv( e5 ) = e1 }.
% 0.69/1.10 { ! inv( e2 ) = e0, inv( e0 ) = e2 }.
% 0.69/1.10 { ! inv( e2 ) = e1, inv( e1 ) = e2 }.
% 0.69/1.10 { ! inv( e2 ) = e2, inv( e2 ) = e2 }.
% 0.69/1.10 { ! inv( e2 ) = e3, inv( e3 ) = e2 }.
% 0.69/1.10 { ! inv( e2 ) = e4, inv( e4 ) = e2 }.
% 0.69/1.10 { ! inv( e2 ) = e5, inv( e5 ) = e2 }.
% 0.69/1.10 { ! inv( e3 ) = e0, inv( e0 ) = e3 }.
% 0.69/1.10 { ! inv( e3 ) = e1, inv( e1 ) = e3 }.
% 0.69/1.10 { ! inv( e3 ) = e2, inv( e2 ) = e3 }.
% 0.69/1.10 { ! inv( e3 ) = e3, inv( e3 ) = e3 }.
% 0.69/1.10 { ! inv( e3 ) = e4, inv( e4 ) = e3 }.
% 0.69/1.10 { ! inv( e3 ) = e5, inv( e5 ) = e3 }.
% 0.69/1.10 { ! inv( e4 ) = e0, inv( e0 ) = e4 }.
% 0.69/1.10 { ! inv( e4 ) = e1, inv( e1 ) = e4 }.
% 0.69/1.10 { ! inv( e4 ) = e2, inv( e2 ) = e4 }.
% 0.69/1.10 { ! inv( e4 ) = e3, inv( e3 ) = e4 }.
% 0.69/1.10 { ! inv( e4 ) = e4, inv( e4 ) = e4 }.
% 0.69/1.10 { ! inv( e4 ) = e5, inv( e5 ) = e4 }.
% 0.69/1.10 { ! inv( e5 ) = e0, inv( e0 ) = e5 }.
% 0.69/1.10 { ! inv( e5 ) = e1, inv( e1 ) = e5 }.
% 0.69/1.10 { ! inv( e5 ) = e2, inv( e2 ) = e5 }.
% 0.69/1.10 { ! inv( e5 ) = e3, inv( e3 ) = e5 }.
% 0.69/1.10 { ! inv( e5 ) = e4, inv( e4 ) = e5 }.
% 0.69/1.10 { ! inv( e5 ) = e5, inv( e5 ) = e5 }.
% 0.69/1.10 { ! inv( e0 ) = inv( e1 ) }.
% 0.69/1.10 { ! inv( e0 ) = inv( e2 ) }.
% 0.69/1.10 { ! inv( e0 ) = inv( e3 ) }.
% 0.69/1.10 { ! inv( e0 ) = inv( e4 ) }.
% 0.69/1.10 { ! inv( e0 ) = inv( e5 ) }.
% 0.69/1.10 { ! inv( e1 ) = inv( e2 ) }.
% 0.69/1.10 { ! inv( e1 ) = inv( e3 ) }.
% 0.69/1.10 { ! inv( e1 ) = inv( e4 ) }.
% 0.69/1.10 { ! inv( e1 ) = inv( e5 ) }.
% 0.69/1.10 { ! inv( e2 ) = inv( e3 ) }.
% 0.69/1.10 { ! inv( e2 ) = inv( e4 ) }.
% 0.69/1.10 { ! inv( e2 ) = inv( e5 ) }.
% 0.69/1.10 { ! inv( e3 ) = inv( e4 ) }.
% 0.69/1.10 { ! inv( e3 ) = inv( e5 ) }.
% 0.69/1.10 { ! inv( e4 ) = inv( e5 ) }.
% 0.69/1.10 { ! op( e0, e0 ) = op( e1, e0 ) }.
% 0.69/1.10 { ! op( e0, e0 ) = op( e2, e0 ) }.
% 0.69/1.10 { ! op( e0, e0 ) = op( e3, e0 ) }.
% 0.69/1.10 { ! op( e0, e0 ) = op( e4, e0 ) }.
% 0.69/1.10 { ! op( e0, e0 ) = op( e5, e0 ) }.
% 0.69/1.10 { ! op( e1, e0 ) = op( e2, e0 ) }.
% 0.69/1.10 { ! op( e1, e0 ) = op( e3, e0 ) }.
% 0.69/1.10 { ! op( e1, e0 ) = op( e4, e0 ) }.
% 0.69/1.10 { ! op( e1, e0 ) = op( e5, e0 ) }.
% 0.69/1.10 { ! op( e2, e0 ) = op( e3, e0 ) }.
% 0.69/1.10 { ! op( e2, e0 ) = op( e4, e0 ) }.
% 0.69/1.10 { ! op( e2, e0 ) = op( e5, e0 ) }.
% 0.69/1.10 { ! op( e3, e0 ) = op( e4, e0 ) }.
% 0.69/1.10 { ! op( e3, e0 ) = op( e5, e0 ) }.
% 0.69/1.10 { ! op( e4, e0 ) = op( e5, e0 ) }.
% 0.69/1.10 { ! op( e0, e1 ) = op( e1, e1 ) }.
% 0.69/1.10 { ! op( e0, e1 ) = op( e2, e1 ) }.
% 0.69/1.10 { ! op( e0, e1 ) = op( e3, e1 ) }.
% 0.69/1.10 { ! op( e0, e1 ) = op( e4, e1 ) }.
% 0.69/1.10 { ! op( e0, e1 ) = op( e5, e1 ) }.
% 0.69/1.10 { ! op( e1, e1 ) = op( e2, e1 ) }.
% 0.69/1.10 { ! op( e1, e1 ) = op( e3, e1 ) }.
% 0.69/1.10 { ! op( e1, e1 ) = op( e4, e1 ) }.
% 0.69/1.10 { ! op( e1, e1 ) = op( e5, e1 ) }.
% 0.69/1.10 { ! op( e2, e1 ) = op( e3, e1 ) }.
% 0.69/1.10 { ! op( e2, e1 ) = op( e4, e1 ) }.
% 0.69/1.10 { ! op( e2, e1 ) = op( e5, e1 ) }.
% 0.69/1.10 { ! op( e3, e1 ) = op( e4, e1 ) }.
% 0.69/1.10 { ! op( e3, e1 ) = op( e5, e1 ) }.
% 0.69/1.10 { ! op( e4, e1 ) = op( e5, e1 ) }.
% 0.69/1.10 { ! op( e0, e2 ) = op( e1, e2 ) }.
% 0.69/1.10 { ! op( e0, e2 ) = op( e2, e2 ) }.
% 0.69/1.10 { ! op( e0, e2 ) = op( e3, e2 ) }.
% 0.69/1.10 { ! op( e0, e2 ) = op( e4, e2 ) }.
% 0.69/1.10 { ! op( e0, e2 ) = op( e5, e2 ) }.
% 0.69/1.10 { ! op( e1, e2 ) = op( e2, e2 ) }.
% 0.69/1.10 { ! op( e1, e2 ) = op( e3, e2 ) }.
% 0.69/1.10 { ! op( e1, e2 ) = op( e4, e2 ) }.
% 0.69/1.10 { ! op( e1, e2 ) = op( e5, e2 ) }.
% 0.69/1.10 { ! op( e2, e2 ) = op( e3, e2 ) }.
% 0.69/1.10 { ! op( e2, e2 ) = op( e4, e2 ) }.
% 0.69/1.10 { ! op( e2, e2 ) = op( e5, e2 ) }.
% 0.69/1.10 { ! op( e3, e2 ) = op( e4, e2 ) }.
% 0.69/1.10 { ! op( e3, e2 ) = op( e5, e2 ) }.
% 0.69/1.10 { ! op( e4, e2 ) = op( e5, e2 ) }.
% 0.69/1.10 { ! op( e0, e3 ) = op( e1, e3 ) }.
% 0.69/1.10 { ! op( e0, e3 ) = op( e2, e3 ) }.
% 0.69/1.10 { ! op( e0, e3 ) = op( e3, e3 ) }.
% 0.69/1.10 { ! op( e0, e3 ) = op( e4, e3 ) }.
% 0.69/1.10 { ! op( e0, e3 ) = op( e5, e3 ) }.
% 0.69/1.10 { ! op( e1, e3 ) = op( e2, e3 ) }.
% 0.69/1.10 { ! op( e1, e3 ) = op( e3, e3 ) }.
% 0.69/1.10 { ! op( e1, e3 ) = op( e4, e3 ) }.
% 0.69/1.10 { ! op( e1, e3 ) = op( e5, e3 ) }.
% 0.69/1.10 { ! op( e2, e3 ) = op( e3, e3 ) }.
% 0.69/1.10 { ! op( e2, e3 ) = op( e4, e3 ) }.
% 0.69/1.10 { ! op( e2, e3 ) = op( e5, e3 ) }.
% 0.69/1.10 { ! op( e3, e3 ) = op( e4, e3 ) }.
% 0.69/1.10 { ! op( e3, e3 ) = op( e5, e3 ) }.
% 0.69/1.10 { ! op( e4, e3 ) = op( e5, e3 ) }.
% 0.69/1.10 { ! op( e0, e4 ) = op( e1, e4 ) }.
% 0.69/1.10 { ! op( e0, e4 ) = op( e2, e4 ) }.
% 0.69/1.10 { ! op( e0, e4 ) = op( e3, e4 ) }.
% 0.69/1.10 { ! op( e0, e4 ) = op( e4, e4 ) }.
% 0.69/1.10 { ! op( e0, e4 ) = op( e5, e4 ) }.
% 0.69/1.10 { ! op( e1, e4 ) = op( e2, e4 ) }.
% 0.69/1.10 { ! op( e1, e4 ) = op( e3, e4 ) }.
% 0.69/1.10 { ! op( e1, e4 ) = op( e4, e4 ) }.
% 0.69/1.10 { ! op( e1, e4 ) = op( e5, e4 ) }.
% 0.69/1.10 { ! op( e2, e4 ) = op( e3, e4 ) }.
% 0.69/1.10 { ! op( e2, e4 ) = op( e4, e4 ) }.
% 0.69/1.10 { ! op( e2, e4 ) = op( e5, e4 ) }.
% 0.69/1.10 { ! op( e3, e4 ) = op( e4, e4 ) }.
% 0.69/1.10 { ! op( e3, e4 ) = op( e5, e4 ) }.
% 0.69/1.10 { ! op( e4, e4 ) = op( e5, e4 ) }.
% 0.69/1.10 { ! op( e0, e5 ) = op( e1, e5 ) }.
% 0.69/1.10 { ! op( e0, e5 ) = op( e2, e5 ) }.
% 0.69/1.10 { ! op( e0, e5 ) = op( e3, e5 ) }.
% 0.69/1.10 { ! op( e0, e5 ) = op( e4, e5 ) }.
% 0.69/1.10 { ! op( e0, e5 ) = op( e5, e5 ) }.
% 0.69/1.10 { ! op( e1, e5 ) = op( e2, e5 ) }.
% 0.69/1.10 { ! op( e1, e5 ) = op( e3, e5 ) }.
% 0.69/1.10 { ! op( e1, e5 ) = op( e4, e5 ) }.
% 0.69/1.10 { ! op( e1, e5 ) = op( e5, e5 ) }.
% 0.69/1.10 { ! op( e2, e5 ) = op( e3, e5 ) }.
% 0.69/1.10 { ! op( e2, e5 ) = op( e4, e5 ) }.
% 0.69/1.10 { ! op( e2, e5 ) = op( e5, e5 ) }.
% 0.69/1.10 { ! op( e3, e5 ) = op( e4, e5 ) }.
% 0.69/1.10 { ! op( e3, e5 ) = op( e5, e5 ) }.
% 0.69/1.10 { ! op( e4, e5 ) = op( e5, e5 ) }.
% 0.69/1.10 { ! op( e0, e0 ) = op( e0, e1 ) }.
% 0.69/1.10 { ! op( e0, e0 ) = op( e0, e2 ) }.
% 0.69/1.10 { ! op( e0, e0 ) = op( e0, e3 ) }.
% 0.69/1.10 { ! op( e0, e0 ) = op( e0, e4 ) }.
% 0.69/1.10 { ! op( e0, e0 ) = op( e0, e5 ) }.
% 0.69/1.10 { ! op( e0, e1 ) = op( e0, e2 ) }.
% 0.69/1.10 { ! op( e0, e1 ) = op( e0, e3 ) }.
% 0.69/1.10 { ! op( e0, e1 ) = op( e0, e4 ) }.
% 0.69/1.10 { ! op( e0, e1 ) = op( e0, e5 ) }.
% 0.69/1.10 { ! op( e0, e2 ) = op( e0, e3 ) }.
% 0.69/1.10 { ! op( e0, e2 ) = op( e0, e4 ) }.
% 0.69/1.10 { ! op( e0, e2 ) = op( e0, e5 ) }.
% 0.69/1.10 { ! op( e0, e3 ) = op( e0, e4 ) }.
% 0.69/1.10 { ! op( e0, e3 ) = op( e0, e5 ) }.
% 0.69/1.10 { ! op( e0, e4 ) = op( e0, e5 ) }.
% 0.69/1.10 { ! op( e1, e0 ) = op( e1, e1 ) }.
% 0.69/1.10 { ! op( e1, e0 ) = op( e1, e2 ) }.
% 0.69/1.10 { ! op( e1, e0 ) = op( e1, e3 ) }.
% 0.69/1.10 { ! op( e1, e0 ) = op( e1, e4 ) }.
% 0.69/1.10 { ! op( e1, e0 ) = op( e1, e5 ) }.
% 0.69/1.10 { ! op( e1, e1 ) = op( e1, e2 ) }.
% 0.69/1.10 { ! op( e1, e1 ) = op( e1, e3 ) }.
% 0.69/1.10 { ! op( e1, e1 ) = op( e1, e4 ) }.
% 0.69/1.10 { ! op( e1, e1 ) = op( e1, e5 ) }.
% 0.69/1.10 { ! op( e1, e2 ) = op( e1, e3 ) }.
% 0.69/1.10 { ! op( e1, e2 ) = op( e1, e4 ) }.
% 0.69/1.10 { ! op( e1, e2 ) = op( e1, e5 ) }.
% 0.69/1.10 { ! op( e1, e3 ) = op( e1, e4 ) }.
% 0.69/1.10 { ! op( e1, e3 ) = op( e1, e5 ) }.
% 0.69/1.10 { ! op( e1, e4 ) = op( e1, e5 ) }.
% 0.69/1.10 { ! op( e2, e0 ) = op( e2, e1 ) }.
% 0.69/1.10 { ! op( e2, e0 ) = op( e2, e2 ) }.
% 0.69/1.10 { ! op( e2, e0 ) = op( e2, e3 ) }.
% 0.69/1.10 { ! op( e2, e0 ) = op( e2, e4 ) }.
% 0.69/1.10 { ! op( e2, e0 ) = op( e2, e5 ) }.
% 0.69/1.10 { ! op( e2, e1 ) = op( e2, e2 ) }.
% 0.69/1.10 { ! op( e2, e1 ) = op( e2, e3 ) }.
% 0.69/1.10 { ! op( e2, e1 ) = op( e2, e4 ) }.
% 0.69/1.10 { ! op( e2, e1 ) = op( e2, e5 ) }.
% 0.69/1.10 { ! op( e2, e2 ) = op( e2, e3 ) }.
% 0.69/1.10 { ! op( e2, e2 ) = op( e2, e4 ) }.
% 0.69/1.10 { ! op( e2, e2 ) = op( e2, e5 ) }.
% 0.69/1.10 { ! op( e2, e3 ) = op( e2, e4 ) }.
% 0.69/1.10 { ! op( e2, e3 ) = op( e2, e5 ) }.
% 0.69/1.10 { ! op( e2, e4 ) = op( e2, e5 ) }.
% 0.69/1.10 { ! op( e3, e0 ) = op( e3, e1 ) }.
% 0.69/1.10 { ! op( e3, e0 ) = op( e3, e2 ) }.
% 0.69/1.10 { ! op( e3, e0 ) = op( e3, e3 ) }.
% 0.69/1.10 { ! op( e3, e0 ) = op( e3, e4 ) }.
% 0.69/1.10 { ! op( e3, e0 ) = op( e3, e5 ) }.
% 0.69/1.10 { ! op( e3, e1 ) = op( e3, e2 ) }.
% 0.69/1.10 { ! op( e3, e1 ) = op( e3, e3 ) }.
% 0.69/1.10 { ! op( e3, e1 ) = op( e3, e4 ) }.
% 0.69/1.10 { ! op( e3, e1 ) = op( e3, e5 ) }.
% 0.69/1.10 { ! op( e3, e2 ) = op( e3, e3 ) }.
% 0.69/1.10 { ! op( e3, e2 ) = op( e3, e4 ) }.
% 0.69/1.10 { ! op( e3, e2 ) = op( e3, e5 ) }.
% 0.69/1.10 { ! op( e3, e3 ) = op( e3, e4 ) }.
% 0.69/1.10 { ! op( e3, e3 ) = op( e3, e5 ) }.
% 0.69/1.10 { ! op( e3, e4 ) = op( e3, e5 ) }.
% 0.69/1.10 { ! op( e4, e0 ) = op( e4, e1 ) }.
% 0.69/1.10 { ! op( e4, e0 ) = op( e4, e2 ) }.
% 0.69/1.10 { ! op( e4, e0 ) = op( e4, e3 ) }.
% 0.69/1.10 { ! op( e4, e0 ) = op( e4, e4 ) }.
% 0.69/1.10 { ! op( e4, e0 ) = op( e4, e5 ) }.
% 0.69/1.10 { ! op( e4, e1 ) = op( e4, e2 ) }.
% 0.69/1.10 { ! op( e4, e1 ) = op( e4, e3 ) }.
% 0.69/1.10 { ! op( e4, e1 ) = op( e4, e4 ) }.
% 0.69/1.10 { ! op( e4, e1 ) = op( e4, e5 ) }.
% 0.69/1.10 { ! op( e4, e2 ) = op( e4, e3 ) }.
% 0.69/1.10 { ! op( e4, e2 ) = op( e4, e4 ) }.
% 0.69/1.10 { ! op( e4, e2 ) = op( e4, e5 ) }.
% 0.69/1.10 { ! op( e4, e3 ) = op( e4, e4 ) }.
% 0.69/1.10 { ! op( e4, e3 ) = op( e4, e5 ) }.
% 0.69/1.10 { ! op( e4, e4 ) = op( e4, e5 ) }.
% 0.69/1.10 { ! op( e5, e0 ) = op( e5, e1 ) }.
% 0.69/1.10 { ! op( e5, e0 ) = op( e5, e2 ) }.
% 0.69/1.10 { ! op( e5, e0 ) = op( e5, e3 ) }.
% 0.69/1.10 { ! op( e5, e0 ) = op( e5, e4 ) }.
% 0.69/1.10 { ! op( e5, e0 ) = op( e5, e5 ) }.
% 0.69/1.10 { ! op( e5, e1 ) = op( e5, e2 ) }.
% 0.69/1.10 { ! op( e5, e1 ) = op( e5, e3 ) }.
% 0.69/1.10 { ! op( e5, e1 ) = op( e5, e4 ) }.
% 0.69/1.10 { ! op( e5, e1 ) = op( e5, e5 ) }.
% 0.69/1.10 { ! op( e5, e2 ) = op( e5, e3 ) }.
% 0.69/1.10 { ! op( e5, e2 ) = op( e5, e4 ) }.
% 0.69/1.10 { ! op( e5, e2 ) = op( e5, e5 ) }.
% 0.69/1.10 { ! op( e5, e3 ) = op( e5, e4 ) }.
% 0.69/1.10 { ! op( e5, e3 ) = op( e5, e5 ) }.
% 0.69/1.10 { ! op( e5, e4 ) = op( e5, e5 ) }.
% 0.69/1.10 { ! e0 = e1 }.
% 0.69/1.10 { ! e0 = e2 }.
% 0.69/1.10 { ! e0 = e3 }.
% 0.69/1.10 { ! e0 = e4 }.
% 0.69/1.10 { ! e0 = e5 }.
% 0.69/1.10 { ! e1 = e2 }.
% 0.69/1.10 { ! e1 = e3 }.
% 0.69/1.10 { ! e1 = e4 }.
% 0.69/1.10 { ! e1 = e5 }.
% 0.69/1.10 { ! e2 = e3 }.
% 0.69/1.10 { ! e2 = e4 }.
% 0.69/1.10 { ! e2 = e5 }.
% 0.69/1.10 { ! e3 = e4 }.
% 0.69/1.10 { ! e3 = e5 }.
% 0.69/1.10 { ! e4 = e5 }.
% 0.69/1.10 { e0 = op( op( op( op( e4, e4 ), e4 ), e4 ), op( e4, e4 ) ) }.
% 0.69/1.10 { e1 = op( op( e4, e4 ), e4 ) }.
% 0.69/1.10 { e2 = op( op( op( e4, e4 ), e4 ), e4 ) }.
% 0.69/1.10 { e3 = op( e4, e4 ) }.
% 0.69/1.10 { e5 = op( op( op( op( e4, e4 ), e4 ), e4 ), e4 ) }.
% 0.69/1.10 { op( e0, e0 ) = op( e0, e0 ) }.
% 0.69/1.10 { op( e0, e1 ) = op( e1, e0 ) }.
% 0.69/1.10 { op( e0, e2 ) = op( e2, e0 ) }.
% 0.69/1.10 { op( e0, e3 ) = op( e3, e0 ) }.
% 0.69/1.10 { op( e0, e4 ) = op( e4, e0 ) }.
% 0.69/1.10 { op( e0, e5 ) = op( e5, e0 ) }.
% 0.69/1.10 { op( e1, e0 ) = op( e0, e1 ) }.
% 0.69/1.10 { op( e1, e1 ) = op( e1, e1 ) }.
% 0.69/1.10 { op( e1, e2 ) = op( e2, e1 ) }.
% 0.69/1.10 { op( e1, e3 ) = op( e3, e1 ) }.
% 0.69/1.10 { op( e1, e4 ) = op( e4, e1 ) }.
% 0.69/1.10 { op( e1, e5 ) = op( e5, e1 ) }.
% 0.69/1.10 { op( e2, e0 ) = op( e0, e2 ) }.
% 0.69/1.10 { op( e2, e1 ) = op( e1, e2 ) }.
% 0.69/1.10 { op( e2, e2 ) = op( e2, e2 ) }.
% 0.69/1.10 { op( e2, e3 ) = op( e3, e2 ) }.
% 0.69/1.10 { op( e2, e4 ) = op( e4, e2 ) }.
% 0.69/1.10 { op( e2, e5 ) = op( e5, e2 ) }.
% 0.69/1.10 { op( e3, e0 ) = op( e0, e3 ) }.
% 0.69/1.10 { op( e3, e1 ) = op( e1, e3 ) }.
% 0.69/1.10 { op( e3, e2 ) = op( e2, e3 ) }.
% 0.69/1.10 { op( e3, e3 ) = op( e3, e3 ) }.
% 0.69/1.10 { op( e3, e4 ) = op( e4, e3 ) }.
% 0.69/1.10 { op( e3, e5 ) = op( e5, e3 ) }.
% 0.69/1.10 { op( e4, e0 ) = op( e0, e4 ) }.
% 0.69/1.10 { op( e4, e1 ) = op( e1, e4 ) }.
% 0.69/1.10 { op( e4, e2 ) = op( e2, e4 ) }.
% 0.69/1.10 { op( e4, e3 ) = op( e3, e4 ) }.
% 0.69/1.10 { op( e4, e4 ) = op( e4, e4 ) }.
% 0.69/1.10 { op( e4, e5 ) = op( e5, e4 ) }.
% 0.69/1.10 { op( e5, e0 ) = op( e0, e5 ) }.
% 0.69/1.10 { op( e5, e1 ) = op( e1, e5 ) }.
% 0.69/1.10 { op( e5, e2 ) = op( e2, e5 ) }.
% 0.69/1.10 { op( e5, e3 ) = op( e3, e5 ) }.
% 0.69/1.10 { op( e5, e4 ) = op( e4, e5 ) }.
% 0.69/1.10 { op( e5, e5 ) = op( e5, e5 ) }.
% 0.69/1.10 { ! op( e0, e0 ) = op( e0, e0 ), ! op( e0, e1 ) = op( e1, e0 ), ! op( e0,
% 0.69/1.10 e2 ) = op( e2, e0 ), ! op( e0, e3 ) = op( e3, e0 ), ! op( e0, e4 ) = op(
% 0.69/1.10 e4, e0 ), ! op( e0, e5 ) = op( e5, e0 ), ! op( e1, e0 ) = op( e0, e1 ), !
% 0.69/1.10 op( e1, e1 ) = op( e1, e1 ), ! op( e1, e2 ) = op( e2, e1 ), ! op( e1, e3
% 0.69/1.10 ) = op( e3, e1 ), ! op( e1, e4 ) = op( e4, e1 ), ! op( e1, e5 ) = op( e5
% 0.69/1.10 , e1 ), ! op( e2, e0 ) = op( e0, e2 ), ! op( e2, e1 ) = op( e1, e2 ), !
% 0.69/1.10 op( e2, e2 ) = op( e2, e2 ), ! op( e2, e3 ) = op( e3, e2 ), ! op( e2, e4
% 0.69/1.10 ) = op( e4, e2 ), ! op( e2, e5 ) = op( e5, e2 ), ! op( e3, e0 ) = op( e0
% 0.69/1.10 , e3 ), ! op( e3, e1 ) = op( e1, e3 ), ! op( e3, e2 ) = op( e2, e3 ), !
% 0.69/1.10 op( e3, e3 ) = op( e3, e3 ), ! op( e3, e4 ) = op( e4, e3 ), ! op( e3, e5
% 0.69/1.10 ) = op( e5, e3 ), ! op( e4, e0 ) = op( e0, e4 ), ! op( e4, e1 ) = op( e1
% 0.69/1.10 , e4 ), ! op( e4, e2 ) = op( e2, e4 ), ! op( e4, e3 ) = op( e3, e4 ), !
% 0.69/1.10 op( e4, e4 ) = op( e4, e4 ), ! op( e4, e5 ) = op( e5, e4 ), ! op( e5, e0
% 0.69/1.10 ) = op( e0, e5 ), ! op( e5, e1 ) = op( e1, e5 ), ! op( e5, e2 ) = op( e2
% 0.69/1.10 , e5 ), ! op( e5, e3 ) = op( e3, e5 ), ! op( e5, e4 ) = op( e4, e5 ), !
% 0.69/1.10 op( e5, e5 ) = op( e5, e5 ) }.
% 0.69/1.10
% 0.69/1.10 *** allocated 15000 integers for clauses
% 0.69/1.10 *** allocated 22500 integers for clauses
% 0.69/1.10 *** allocated 33750 integers for clauses
% 0.69/1.10 percentage equality = 1.000000, percentage horn = 0.924028
% 0.69/1.10 This is a pure equality problem
% 0.69/1.10
% 0.69/1.10
% 0.69/1.10
% 0.69/1.10 Options Used:
% 0.69/1.10
% 0.69/1.10 useres = 1
% 0.69/1.10 useparamod = 1
% 0.69/1.10 useeqrefl = 1
% 0.69/1.10 useeqfact = 1
% 0.69/1.10 usefactor = 1
% 0.69/1.10 usesimpsplitting = 0
% 0.69/1.10 usesimpdemod = 5
% 0.69/1.10 usesimpres = 3
% 0.69/1.10
% 0.69/1.10 resimpinuse = 1000
% 0.69/1.10 resimpclauses = 20000
% 0.69/1.10 substype = eqrewr
% 0.69/1.10 backwardsubs = 1
% 0.69/1.10 selectoldest = 5
% 0.69/1.10
% 0.69/1.10 litorderings [0] = split
% 0.69/1.10 litorderings [1] = extend the termordering, first sorting on arguments
% 0.69/1.10
% 0.69/1.10 termordering = kbo
% 0.69/1.10
% 0.69/1.10 litapriori = 0
% 0.69/1.10 termapriori = 1
% 0.69/1.10 litaposteriori = 0
% 0.69/1.10 termaposteriori = 0
% 0.69/1.10 demodaposteriori = 0
% 0.69/1.10 ordereqreflfact = 0
% 0.69/1.10
% 0.69/1.10 litselect = negord
% 0.69/1.10
% 0.69/1.10 maxweight = 15
% 0.69/1.10 maxdepth = 30000
% 0.69/1.10 maxlength = 115
% 0.69/1.10 maxnrvars = 195
% 0.69/1.10 excuselevel = 1
% 0.69/1.10 increasemaxweight = 1
% 0.69/1.10
% 0.69/1.10 maxselected = 10000000
% 0.69/1.10 maxnrclauses = 10000000
% 0.69/1.10
% 0.69/1.10 showgenerated = 0
% 0.69/1.10 showkept = 0
% 0.69/1.10 showselected = 0
% 0.69/1.10 showdeleted = 0
% 0.69/1.10 showresimp = 1
% 0.69/1.10 showstatus = 2000
% 0.69/1.10
% 0.69/1.10 prologoutput = 0
% 0.69/1.10 nrgoals = 5000000
% 0.69/1.10 totalproof = 1
% 0.69/1.10
% 0.69/1.10 Symbols occurring in the translation:
% 0.69/1.10
% 0.69/1.10 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.69/1.10 . [1, 2] (w:1, o:19, a:1, s:1, b:0),
% 0.69/1.10 ! [4, 1] (w:0, o:13, a:1, s:1, b:0),
% 0.69/1.10 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.69/1.10 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.69/1.10 e0 [35, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.69/1.10 op [36, 2] (w:1, o:43, a:1, s:1, b:0),
% 0.69/1.10 e1 [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.69/1.10 e2 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.69/1.10 e3 [39, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.69/1.10 e4 [40, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.69/1.10 e5 [41, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.69/1.10 unit [42, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.69/1.10 inv [43, 1] (w:1, o:18, a:1, s:1, b:0).
% 0.69/1.10
% 0.69/1.10
% 0.69/1.10 Starting Search:
% 0.69/1.10
% 0.69/1.10 *** allocated 50625 integers for clauses
% 0.69/1.10
% 0.69/1.10 Bliksems!, er is een bewijs:
% 0.69/1.10 % SZS status Theorem
% 0.69/1.10 % SZS output start Refutation
% 0.69/1.10
% 0.69/1.10 (531) {G0,W7,D4,L1,V0,M1} I { op( op( e4, e4 ), e4 ) ==> e1 }.
% 0.69/1.10 (532) {G1,W5,D3,L1,V0,M1} I;d(531) { op( e1, e4 ) ==> e2 }.
% 0.69/1.10 (534) {G2,W5,D3,L1,V0,M1} I;d(531);d(532) { op( e2, e4 ) ==> e5 }.
% 0.69/1.10 (535) {G0,W7,D3,L1,V0,M1} I { op( e0, e1 ) ==> op( e1, e0 ) }.
% 0.69/1.10 (536) {G0,W7,D3,L1,V0,M1} I { op( e0, e2 ) ==> op( e2, e0 ) }.
% 0.69/1.10 (537) {G0,W7,D3,L1,V0,M1} I { op( e0, e3 ) ==> op( e3, e0 ) }.
% 0.69/1.10 (538) {G0,W7,D3,L1,V0,M1} I { op( e0, e4 ) ==> op( e4, e0 ) }.
% 0.69/1.10 (539) {G0,W7,D3,L1,V0,M1} I { op( e0, e5 ) ==> op( e5, e0 ) }.
% 0.69/1.10 (540) {G0,W7,D3,L1,V0,M1} I { op( e1, e2 ) ==> op( e2, e1 ) }.
% 0.69/1.10 (541) {G0,W7,D3,L1,V0,M1} I { op( e1, e3 ) ==> op( e3, e1 ) }.
% 0.69/1.10 (542) {G2,W5,D3,L1,V0,M1} I;d(532) { op( e4, e1 ) ==> e2 }.
% 0.69/1.10 (543) {G0,W7,D3,L1,V0,M1} I { op( e1, e5 ) ==> op( e5, e1 ) }.
% 0.69/1.10 (544) {G0,W7,D3,L1,V0,M1} I { op( e2, e3 ) ==> op( e3, e2 ) }.
% 0.69/1.10 (545) {G3,W5,D3,L1,V0,M1} I;d(534) { op( e4, e2 ) ==> e5 }.
% 0.69/1.10 (546) {G0,W7,D3,L1,V0,M1} I { op( e2, e5 ) ==> op( e5, e2 ) }.
% 0.69/1.10 (547) {G0,W7,D3,L1,V0,M1} I { op( e3, e4 ) ==> op( e4, e3 ) }.
% 0.69/1.10 (548) {G0,W7,D3,L1,V0,M1} I { op( e3, e5 ) ==> op( e5, e3 ) }.
% 0.69/1.10 (549) {G0,W7,D3,L1,V0,M1} I { op( e4, e5 ) ==> op( e5, e4 ) }.
% 0.69/1.10 (550) {G4,W0,D0,L0,V0,M0} I;q;q;q;q;q;q;d(535);d(536);d(537);d(538);d(539);
% 0.69/1.10 d(535);d(540);d(541);d(532);d(543);d(536);d(540);d(544);d(534);d(546);d(
% 0.69/1.10 537);d(541);d(544);d(547);d(548);d(538);d(542);d(545);d(547);d(549);d(539
% 0.69/1.10 );d(543);d(546);d(548);d(549);d(542);d(545);d(532);d(534);q;q;q;q;q;q;q;q
% 0.69/1.10 ;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q { }.
% 0.69/1.10
% 0.69/1.10
% 0.69/1.10 % SZS output end Refutation
% 0.69/1.10 found a proof!
% 0.69/1.10
% 0.69/1.10 *** allocated 33750 integers for termspace/termends
% 0.69/1.10
% 0.69/1.10 Unprocessed initial clauses:
% 0.69/1.10
% 0.69/1.10 (552) {G0,W30,D3,L6,V0,M6} { op( e0, e0 ) = e0, op( e0, e0 ) = e1, op( e0
% 0.69/1.10 , e0 ) = e2, op( e0, e0 ) = e3, op( e0, e0 ) = e4, op( e0, e0 ) = e5 }.
% 0.69/1.10 (553) {G0,W30,D3,L6,V0,M6} { op( e0, e1 ) = e0, op( e0, e1 ) = e1, op( e0
% 0.69/1.10 , e1 ) = e2, op( e0, e1 ) = e3, op( e0, e1 ) = e4, op( e0, e1 ) = e5 }.
% 0.69/1.10 (554) {G0,W30,D3,L6,V0,M6} { op( e0, e2 ) = e0, op( e0, e2 ) = e1, op( e0
% 0.69/1.10 , e2 ) = e2, op( e0, e2 ) = e3, op( e0, e2 ) = e4, op( e0, e2 ) = e5 }.
% 0.69/1.10 (555) {G0,W30,D3,L6,V0,M6} { op( e0, e3 ) = e0, op( e0, e3 ) = e1, op( e0
% 0.69/1.10 , e3 ) = e2, op( e0, e3 ) = e3, op( e0, e3 ) = e4, op( e0, e3 ) = e5 }.
% 0.69/1.10 (556) {G0,W30,D3,L6,V0,M6} { op( e0, e4 ) = e0, op( e0, e4 ) = e1, op( e0
% 0.69/1.10 , e4 ) = e2, op( e0, e4 ) = e3, op( e0, e4 ) = e4, op( e0, e4 ) = e5 }.
% 0.69/1.10 (557) {G0,W30,D3,L6,V0,M6} { op( e0, e5 ) = e0, op( e0, e5 ) = e1, op( e0
% 0.69/1.10 , e5 ) = e2, op( e0, e5 ) = e3, op( e0, e5 ) = e4, op( e0, e5 ) = e5 }.
% 0.69/1.10 (558) {G0,W30,D3,L6,V0,M6} { op( e1, e0 ) = e0, op( e1, e0 ) = e1, op( e1
% 0.69/1.10 , e0 ) = e2, op( e1, e0 ) = e3, op( e1, e0 ) = e4, op( e1, e0 ) = e5 }.
% 0.69/1.10 (559) {G0,W30,D3,L6,V0,M6} { op( e1, e1 ) = e0, op( e1, e1 ) = e1, op( e1
% 0.69/1.10 , e1 ) = e2, op( e1, e1 ) = e3, op( e1, e1 ) = e4, op( e1, e1 ) = e5 }.
% 0.69/1.10 (560) {G0,W30,D3,L6,V0,M6} { op( e1, e2 ) = e0, op( e1, e2 ) = e1, op( e1
% 0.69/1.10 , e2 ) = e2, op( e1, e2 ) = e3, op( e1, e2 ) = e4, op( e1, e2 ) = e5 }.
% 0.69/1.10 (561) {G0,W30,D3,L6,V0,M6} { op( e1, e3 ) = e0, op( e1, e3 ) = e1, op( e1
% 0.69/1.10 , e3 ) = e2, op( e1, e3 ) = e3, op( e1, e3 ) = e4, op( e1, e3 ) = e5 }.
% 0.69/1.10 (562) {G0,W30,D3,L6,V0,M6} { op( e1, e4 ) = e0, op( e1, e4 ) = e1, op( e1
% 0.69/1.10 , e4 ) = e2, op( e1, e4 ) = e3, op( e1, e4 ) = e4, op( e1, e4 ) = e5 }.
% 0.69/1.10 (563) {G0,W30,D3,L6,V0,M6} { op( e1, e5 ) = e0, op( e1, e5 ) = e1, op( e1
% 0.69/1.10 , e5 ) = e2, op( e1, e5 ) = e3, op( e1, e5 ) = e4, op( e1, e5 ) = e5 }.
% 0.69/1.10 (564) {G0,W30,D3,L6,V0,M6} { op( e2, e0 ) = e0, op( e2, e0 ) = e1, op( e2
% 0.69/1.10 , e0 ) = e2, op( e2, e0 ) = e3, op( e2, e0 ) = e4, op( e2, e0 ) = e5 }.
% 0.69/1.10 (565) {G0,W30,D3,L6,V0,M6} { op( e2, e1 ) = e0, op( e2, e1 ) = e1, op( e2
% 0.69/1.10 , e1 ) = e2, op( e2, e1 ) = e3, op( e2, e1 ) = e4, op( e2, e1 ) = e5 }.
% 0.69/1.10 (566) {G0,W30,D3,L6,V0,M6} { op( e2, e2 ) = e0, op( e2, e2 ) = e1, op( e2
% 0.69/1.10 , e2 ) = e2, op( e2, e2 ) = e3, op( e2, e2 ) = e4, op( e2, e2 ) = e5 }.
% 0.69/1.10 (567) {G0,W30,D3,L6,V0,M6} { op( e2, e3 ) = e0, op( e2, e3 ) = e1, op( e2
% 0.69/1.10 , e3 ) = e2, op( e2, e3 ) = e3, op( e2, e3 ) = e4, op( e2, e3 ) = e5 }.
% 0.69/1.10 (568) {G0,W30,D3,L6,V0,M6} { op( e2, e4 ) = e0, op( e2, e4 ) = e1, op( e2
% 0.69/1.10 , e4 ) = e2, op( e2, e4 ) = e3, op( e2, e4 ) = e4, op( e2, e4 ) = e5 }.
% 0.69/1.10 (569) {G0,W30,D3,L6,V0,M6} { op( e2, e5 ) = e0, op( e2, e5 ) = e1, op( e2
% 0.69/1.10 , e5 ) = e2, op( e2, e5 ) = e3, op( e2, e5 ) = e4, op( e2, e5 ) = e5 }.
% 0.69/1.10 (570) {G0,W30,D3,L6,V0,M6} { op( e3, e0 ) = e0, op( e3, e0 ) = e1, op( e3
% 0.69/1.10 , e0 ) = e2, op( e3, e0 ) = e3, op( e3, e0 ) = e4, op( e3, e0 ) = e5 }.
% 0.69/1.10 (571) {G0,W30,D3,L6,V0,M6} { op( e3, e1 ) = e0, op( e3, e1 ) = e1, op( e3
% 0.69/1.10 , e1 ) = e2, op( e3, e1 ) = e3, op( e3, e1 ) = e4, op( e3, e1 ) = e5 }.
% 0.69/1.10 (572) {G0,W30,D3,L6,V0,M6} { op( e3, e2 ) = e0, op( e3, e2 ) = e1, op( e3
% 0.69/1.10 , e2 ) = e2, op( e3, e2 ) = e3, op( e3, e2 ) = e4, op( e3, e2 ) = e5 }.
% 0.69/1.10 (573) {G0,W30,D3,L6,V0,M6} { op( e3, e3 ) = e0, op( e3, e3 ) = e1, op( e3
% 0.69/1.10 , e3 ) = e2, op( e3, e3 ) = e3, op( e3, e3 ) = e4, op( e3, e3 ) = e5 }.
% 0.69/1.10 (574) {G0,W30,D3,L6,V0,M6} { op( e3, e4 ) = e0, op( e3, e4 ) = e1, op( e3
% 0.69/1.10 , e4 ) = e2, op( e3, e4 ) = e3, op( e3, e4 ) = e4, op( e3, e4 ) = e5 }.
% 0.69/1.10 (575) {G0,W30,D3,L6,V0,M6} { op( e3, e5 ) = e0, op( e3, e5 ) = e1, op( e3
% 0.69/1.10 , e5 ) = e2, op( e3, e5 ) = e3, op( e3, e5 ) = e4, op( e3, e5 ) = e5 }.
% 0.69/1.10 (576) {G0,W30,D3,L6,V0,M6} { op( e4, e0 ) = e0, op( e4, e0 ) = e1, op( e4
% 0.69/1.10 , e0 ) = e2, op( e4, e0 ) = e3, op( e4, e0 ) = e4, op( e4, e0 ) = e5 }.
% 0.69/1.10 (577) {G0,W30,D3,L6,V0,M6} { op( e4, e1 ) = e0, op( e4, e1 ) = e1, op( e4
% 0.69/1.10 , e1 ) = e2, op( e4, e1 ) = e3, op( e4, e1 ) = e4, op( e4, e1 ) = e5 }.
% 0.69/1.10 (578) {G0,W30,D3,L6,V0,M6} { op( e4, e2 ) = e0, op( e4, e2 ) = e1, op( e4
% 0.69/1.10 , e2 ) = e2, op( e4, e2 ) = e3, op( e4, e2 ) = e4, op( e4, e2 ) = e5 }.
% 0.69/1.10 (579) {G0,W30,D3,L6,V0,M6} { op( e4, e3 ) = e0, op( e4, e3 ) = e1, op( e4
% 0.69/1.10 , e3 ) = e2, op( e4, e3 ) = e3, op( e4, e3 ) = e4, op( e4, e3 ) = e5 }.
% 0.69/1.10 (580) {G0,W30,D3,L6,V0,M6} { op( e4, e4 ) = e0, op( e4, e4 ) = e1, op( e4
% 0.69/1.10 , e4 ) = e2, op( e4, e4 ) = e3, op( e4, e4 ) = e4, op( e4, e4 ) = e5 }.
% 0.69/1.10 (581) {G0,W30,D3,L6,V0,M6} { op( e4, e5 ) = e0, op( e4, e5 ) = e1, op( e4
% 0.69/1.10 , e5 ) = e2, op( e4, e5 ) = e3, op( e4, e5 ) = e4, op( e4, e5 ) = e5 }.
% 0.69/1.10 (582) {G0,W30,D3,L6,V0,M6} { op( e5, e0 ) = e0, op( e5, e0 ) = e1, op( e5
% 0.69/1.10 , e0 ) = e2, op( e5, e0 ) = e3, op( e5, e0 ) = e4, op( e5, e0 ) = e5 }.
% 0.69/1.10 (583) {G0,W30,D3,L6,V0,M6} { op( e5, e1 ) = e0, op( e5, e1 ) = e1, op( e5
% 0.69/1.10 , e1 ) = e2, op( e5, e1 ) = e3, op( e5, e1 ) = e4, op( e5, e1 ) = e5 }.
% 0.69/1.10 (584) {G0,W30,D3,L6,V0,M6} { op( e5, e2 ) = e0, op( e5, e2 ) = e1, op( e5
% 0.69/1.10 , e2 ) = e2, op( e5, e2 ) = e3, op( e5, e2 ) = e4, op( e5, e2 ) = e5 }.
% 0.69/1.10 (585) {G0,W30,D3,L6,V0,M6} { op( e5, e3 ) = e0, op( e5, e3 ) = e1, op( e5
% 0.69/1.10 , e3 ) = e2, op( e5, e3 ) = e3, op( e5, e3 ) = e4, op( e5, e3 ) = e5 }.
% 0.69/1.10 (586) {G0,W30,D3,L6,V0,M6} { op( e5, e4 ) = e0, op( e5, e4 ) = e1, op( e5
% 0.69/1.10 , e4 ) = e2, op( e5, e4 ) = e3, op( e5, e4 ) = e4, op( e5, e4 ) = e5 }.
% 0.69/1.10 (587) {G0,W30,D3,L6,V0,M6} { op( e5, e5 ) = e0, op( e5, e5 ) = e1, op( e5
% 0.69/1.10 , e5 ) = e2, op( e5, e5 ) = e3, op( e5, e5 ) = e4, op( e5, e5 ) = e5 }.
% 0.69/1.10 (588) {G0,W11,D4,L1,V0,M1} { op( op( e0, e0 ), e0 ) = op( e0, op( e0, e0 )
% 0.69/1.10 ) }.
% 0.69/1.10 (589) {G0,W11,D4,L1,V0,M1} { op( op( e0, e0 ), e1 ) = op( e0, op( e0, e1 )
% 0.69/1.10 ) }.
% 0.69/1.10 (590) {G0,W11,D4,L1,V0,M1} { op( op( e0, e0 ), e2 ) = op( e0, op( e0, e2 )
% 0.69/1.10 ) }.
% 0.69/1.10 (591) {G0,W11,D4,L1,V0,M1} { op( op( e0, e0 ), e3 ) = op( e0, op( e0, e3 )
% 0.69/1.10 ) }.
% 0.69/1.10 (592) {G0,W11,D4,L1,V0,M1} { op( op( e0, e0 ), e4 ) = op( e0, op( e0, e4 )
% 0.69/1.10 ) }.
% 0.69/1.10 (593) {G0,W11,D4,L1,V0,M1} { op( op( e0, e0 ), e5 ) = op( e0, op( e0, e5 )
% 0.69/1.10 ) }.
% 0.69/1.10 (594) {G0,W11,D4,L1,V0,M1} { op( op( e0, e1 ), e0 ) = op( e0, op( e1, e0 )
% 0.69/1.10 ) }.
% 0.69/1.10 (595) {G0,W11,D4,L1,V0,M1} { op( op( e0, e1 ), e1 ) = op( e0, op( e1, e1 )
% 0.69/1.10 ) }.
% 0.69/1.10 (596) {G0,W11,D4,L1,V0,M1} { op( op( e0, e1 ), e2 ) = op( e0, op( e1, e2 )
% 0.69/1.10 ) }.
% 0.69/1.10 (597) {G0,W11,D4,L1,V0,M1} { op( op( e0, e1 ), e3 ) = op( e0, op( e1, e3 )
% 0.69/1.10 ) }.
% 0.69/1.10 (598) {G0,W11,D4,L1,V0,M1} { op( op( e0, e1 ), e4 ) = op( e0, op( e1, e4 )
% 0.69/1.10 ) }.
% 0.69/1.10 (599) {G0,W11,D4,L1,V0,M1} { op( op( e0, e1 ), e5 ) = op( e0, op( e1, e5 )
% 0.69/1.10 ) }.
% 0.69/1.10 (600) {G0,W11,D4,L1,V0,M1} { op( op( e0, e2 ), e0 ) = op( e0, op( e2, e0 )
% 0.69/1.10 ) }.
% 0.69/1.10 (601) {G0,W11,D4,L1,V0,M1} { op( op( e0, e2 ), e1 ) = op( e0, op( e2, e1 )
% 0.69/1.10 ) }.
% 0.69/1.10 (602) {G0,W11,D4,L1,V0,M1} { op( op( e0, e2 ), e2 ) = op( e0, op( e2, e2 )
% 0.69/1.10 ) }.
% 0.69/1.10 (603) {G0,W11,D4,L1,V0,M1} { op( op( e0, e2 ), e3 ) = op( e0, op( e2, e3 )
% 0.69/1.10 ) }.
% 0.69/1.10 (604) {G0,W11,D4,L1,V0,M1} { op( op( e0, e2 ), e4 ) = op( e0, op( e2, e4 )
% 0.69/1.10 ) }.
% 0.69/1.10 (605) {G0,W11,D4,L1,V0,M1} { op( op( e0, e2 ), e5 ) = op( e0, op( e2, e5 )
% 0.69/1.10 ) }.
% 0.69/1.10 (606) {G0,W11,D4,L1,V0,M1} { op( op( e0, e3 ), e0 ) = op( e0, op( e3, e0 )
% 0.69/1.10 ) }.
% 0.69/1.10 (607) {G0,W11,D4,L1,V0,M1} { op( op( e0, e3 ), e1 ) = op( e0, op( e3, e1 )
% 0.69/1.10 ) }.
% 0.69/1.10 (608) {G0,W11,D4,L1,V0,M1} { op( op( e0, e3 ), e2 ) = op( e0, op( e3, e2 )
% 0.69/1.10 ) }.
% 0.69/1.10 (609) {G0,W11,D4,L1,V0,M1} { op( op( e0, e3 ), e3 ) = op( e0, op( e3, e3 )
% 0.69/1.10 ) }.
% 0.69/1.10 (610) {G0,W11,D4,L1,V0,M1} { op( op( e0, e3 ), e4 ) = op( e0, op( e3, e4 )
% 0.69/1.10 ) }.
% 0.69/1.10 (611) {G0,W11,D4,L1,V0,M1} { op( op( e0, e3 ), e5 ) = op( e0, op( e3, e5 )
% 0.69/1.10 ) }.
% 0.69/1.10 (612) {G0,W11,D4,L1,V0,M1} { op( op( e0, e4 ), e0 ) = op( e0, op( e4, e0 )
% 0.69/1.10 ) }.
% 0.69/1.10 (613) {G0,W11,D4,L1,V0,M1} { op( op( e0, e4 ), e1 ) = op( e0, op( e4, e1 )
% 0.69/1.10 ) }.
% 0.69/1.10 (614) {G0,W11,D4,L1,V0,M1} { op( op( e0, e4 ), e2 ) = op( e0, op( e4, e2 )
% 0.69/1.10 ) }.
% 0.69/1.10 (615) {G0,W11,D4,L1,V0,M1} { op( op( e0, e4 ), e3 ) = op( e0, op( e4, e3 )
% 0.69/1.10 ) }.
% 0.69/1.10 (616) {G0,W11,D4,L1,V0,M1} { op( op( e0, e4 ), e4 ) = op( e0, op( e4, e4 )
% 0.69/1.10 ) }.
% 0.69/1.10 (617) {G0,W11,D4,L1,V0,M1} { op( op( e0, e4 ), e5 ) = op( e0, op( e4, e5 )
% 0.69/1.10 ) }.
% 0.69/1.10 (618) {G0,W11,D4,L1,V0,M1} { op( op( e0, e5 ), e0 ) = op( e0, op( e5, e0 )
% 0.69/1.10 ) }.
% 0.69/1.10 (619) {G0,W11,D4,L1,V0,M1} { op( op( e0, e5 ), e1 ) = op( e0, op( e5, e1 )
% 0.69/1.10 ) }.
% 0.69/1.10 (620) {G0,W11,D4,L1,V0,M1} { op( op( e0, e5 ), e2 ) = op( e0, op( e5, e2 )
% 0.69/1.10 ) }.
% 0.69/1.10 (621) {G0,W11,D4,L1,V0,M1} { op( op( e0, e5 ), e3 ) = op( e0, op( e5, e3 )
% 0.69/1.10 ) }.
% 0.69/1.10 (622) {G0,W11,D4,L1,V0,M1} { op( op( e0, e5 ), e4 ) = op( e0, op( e5, e4 )
% 0.69/1.10 ) }.
% 0.69/1.10 (623) {G0,W11,D4,L1,V0,M1} { op( op( e0, e5 ), e5 ) = op( e0, op( e5, e5 )
% 0.69/1.10 ) }.
% 0.69/1.10 (624) {G0,W11,D4,L1,V0,M1} { op( op( e1, e0 ), e0 ) = op( e1, op( e0, e0 )
% 0.69/1.10 ) }.
% 0.69/1.10 (625) {G0,W11,D4,L1,V0,M1} { op( op( e1, e0 ), e1 ) = op( e1, op( e0, e1 )
% 0.69/1.10 ) }.
% 0.69/1.10 (626) {G0,W11,D4,L1,V0,M1} { op( op( e1, e0 ), e2 ) = op( e1, op( e0, e2 )
% 0.69/1.10 ) }.
% 0.69/1.10 (627) {G0,W11,D4,L1,V0,M1} { op( op( e1, e0 ), e3 ) = op( e1, op( e0, e3 )
% 0.69/1.10 ) }.
% 0.69/1.10 (628) {G0,W11,D4,L1,V0,M1} { op( op( e1, e0 ), e4 ) = op( e1, op( e0, e4 )
% 0.69/1.10 ) }.
% 0.69/1.10 (629) {G0,W11,D4,L1,V0,M1} { op( op( e1, e0 ), e5 ) = op( e1, op( e0, e5 )
% 0.69/1.10 ) }.
% 0.69/1.10 (630) {G0,W11,D4,L1,V0,M1} { op( op( e1, e1 ), e0 ) = op( e1, op( e1, e0 )
% 0.69/1.10 ) }.
% 0.69/1.10 (631) {G0,W11,D4,L1,V0,M1} { op( op( e1, e1 ), e1 ) = op( e1, op( e1, e1 )
% 0.69/1.10 ) }.
% 0.69/1.10 (632) {G0,W11,D4,L1,V0,M1} { op( op( e1, e1 ), e2 ) = op( e1, op( e1, e2 )
% 0.69/1.10 ) }.
% 0.69/1.10 (633) {G0,W11,D4,L1,V0,M1} { op( op( e1, e1 ), e3 ) = op( e1, op( e1, e3 )
% 0.69/1.10 ) }.
% 0.69/1.10 (634) {G0,W11,D4,L1,V0,M1} { op( op( e1, e1 ), e4 ) = op( e1, op( e1, e4 )
% 0.69/1.10 ) }.
% 0.69/1.10 (635) {G0,W11,D4,L1,V0,M1} { op( op( e1, e1 ), e5 ) = op( e1, op( e1, e5 )
% 0.69/1.10 ) }.
% 0.69/1.10 (636) {G0,W11,D4,L1,V0,M1} { op( op( e1, e2 ), e0 ) = op( e1, op( e2, e0 )
% 0.69/1.10 ) }.
% 0.69/1.10 (637) {G0,W11,D4,L1,V0,M1} { op( op( e1, e2 ), e1 ) = op( e1, op( e2, e1 )
% 0.69/1.10 ) }.
% 0.69/1.10 (638) {G0,W11,D4,L1,V0,M1} { op( op( e1, e2 ), e2 ) = op( e1, op( e2, e2 )
% 0.69/1.10 ) }.
% 0.69/1.10 (639) {G0,W11,D4,L1,V0,M1} { op( op( e1, e2 ), e3 ) = op( e1, op( e2, e3 )
% 0.69/1.10 ) }.
% 0.69/1.10 (640) {G0,W11,D4,L1,V0,M1} { op( op( e1, e2 ), e4 ) = op( e1, op( e2, e4 )
% 0.69/1.10 ) }.
% 0.69/1.10 (641) {G0,W11,D4,L1,V0,M1} { op( op( e1, e2 ), e5 ) = op( e1, op( e2, e5 )
% 0.69/1.10 ) }.
% 0.69/1.10 (642) {G0,W11,D4,L1,V0,M1} { op( op( e1, e3 ), e0 ) = op( e1, op( e3, e0 )
% 0.69/1.10 ) }.
% 0.69/1.10 (643) {G0,W11,D4,L1,V0,M1} { op( op( e1, e3 ), e1 ) = op( e1, op( e3, e1 )
% 0.69/1.10 ) }.
% 0.69/1.10 (644) {G0,W11,D4,L1,V0,M1} { op( op( e1, e3 ), e2 ) = op( e1, op( e3, e2 )
% 0.69/1.10 ) }.
% 0.69/1.10 (645) {G0,W11,D4,L1,V0,M1} { op( op( e1, e3 ), e3 ) = op( e1, op( e3, e3 )
% 0.69/1.10 ) }.
% 0.69/1.10 (646) {G0,W11,D4,L1,V0,M1} { op( op( e1, e3 ), e4 ) = op( e1, op( e3, e4 )
% 0.69/1.10 ) }.
% 0.69/1.10 (647) {G0,W11,D4,L1,V0,M1} { op( op( e1, e3 ), e5 ) = op( e1, op( e3, e5 )
% 0.69/1.10 ) }.
% 0.69/1.10 (648) {G0,W11,D4,L1,V0,M1} { op( op( e1, e4 ), e0 ) = op( e1, op( e4, e0 )
% 0.69/1.10 ) }.
% 0.69/1.10 (649) {G0,W11,D4,L1,V0,M1} { op( op( e1, e4 ), e1 ) = op( e1, op( e4, e1 )
% 0.69/1.10 ) }.
% 0.69/1.10 (650) {G0,W11,D4,L1,V0,M1} { op( op( e1, e4 ), e2 ) = op( e1, op( e4, e2 )
% 0.69/1.10 ) }.
% 0.69/1.10 (651) {G0,W11,D4,L1,V0,M1} { op( op( e1, e4 ), e3 ) = op( e1, op( e4, e3 )
% 0.69/1.10 ) }.
% 0.69/1.10 (652) {G0,W11,D4,L1,V0,M1} { op( op( e1, e4 ), e4 ) = op( e1, op( e4, e4 )
% 0.69/1.10 ) }.
% 0.69/1.10 (653) {G0,W11,D4,L1,V0,M1} { op( op( e1, e4 ), e5 ) = op( e1, op( e4, e5 )
% 0.69/1.10 ) }.
% 0.69/1.10 (654) {G0,W11,D4,L1,V0,M1} { op( op( e1, e5 ), e0 ) = op( e1, op( e5, e0 )
% 0.69/1.10 ) }.
% 0.69/1.10 (655) {G0,W11,D4,L1,V0,M1} { op( op( e1, e5 ), e1 ) = op( e1, op( e5, e1 )
% 0.69/1.10 ) }.
% 0.69/1.10 (656) {G0,W11,D4,L1,V0,M1} { op( op( e1, e5 ), e2 ) = op( e1, op( e5, e2 )
% 0.69/1.10 ) }.
% 0.69/1.10 (657) {G0,W11,D4,L1,V0,M1} { op( op( e1, e5 ), e3 ) = op( e1, op( e5, e3 )
% 0.69/1.10 ) }.
% 0.69/1.10 (658) {G0,W11,D4,L1,V0,M1} { op( op( e1, e5 ), e4 ) = op( e1, op( e5, e4 )
% 0.69/1.10 ) }.
% 0.69/1.10 (659) {G0,W11,D4,L1,V0,M1} { op( op( e1, e5 ), e5 ) = op( e1, op( e5, e5 )
% 0.69/1.10 ) }.
% 0.69/1.10 (660) {G0,W11,D4,L1,V0,M1} { op( op( e2, e0 ), e0 ) = op( e2, op( e0, e0 )
% 0.69/1.10 ) }.
% 0.69/1.10 (661) {G0,W11,D4,L1,V0,M1} { op( op( e2, e0 ), e1 ) = op( e2, op( e0, e1 )
% 0.69/1.10 ) }.
% 0.69/1.10 (662) {G0,W11,D4,L1,V0,M1} { op( op( e2, e0 ), e2 ) = op( e2, op( e0, e2 )
% 0.69/1.10 ) }.
% 0.69/1.10 (663) {G0,W11,D4,L1,V0,M1} { op( op( e2, e0 ), e3 ) = op( e2, op( e0, e3 )
% 0.69/1.10 ) }.
% 0.69/1.10 (664) {G0,W11,D4,L1,V0,M1} { op( op( e2, e0 ), e4 ) = op( e2, op( e0, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (665) {G0,W11,D4,L1,V0,M1} { op( op( e2, e0 ), e5 ) = op( e2, op( e0, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (666) {G0,W11,D4,L1,V0,M1} { op( op( e2, e1 ), e0 ) = op( e2, op( e1, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (667) {G0,W11,D4,L1,V0,M1} { op( op( e2, e1 ), e1 ) = op( e2, op( e1, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (668) {G0,W11,D4,L1,V0,M1} { op( op( e2, e1 ), e2 ) = op( e2, op( e1, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (669) {G0,W11,D4,L1,V0,M1} { op( op( e2, e1 ), e3 ) = op( e2, op( e1, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (670) {G0,W11,D4,L1,V0,M1} { op( op( e2, e1 ), e4 ) = op( e2, op( e1, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (671) {G0,W11,D4,L1,V0,M1} { op( op( e2, e1 ), e5 ) = op( e2, op( e1, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (672) {G0,W11,D4,L1,V0,M1} { op( op( e2, e2 ), e0 ) = op( e2, op( e2, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (673) {G0,W11,D4,L1,V0,M1} { op( op( e2, e2 ), e1 ) = op( e2, op( e2, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (674) {G0,W11,D4,L1,V0,M1} { op( op( e2, e2 ), e2 ) = op( e2, op( e2, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (675) {G0,W11,D4,L1,V0,M1} { op( op( e2, e2 ), e3 ) = op( e2, op( e2, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (676) {G0,W11,D4,L1,V0,M1} { op( op( e2, e2 ), e4 ) = op( e2, op( e2, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (677) {G0,W11,D4,L1,V0,M1} { op( op( e2, e2 ), e5 ) = op( e2, op( e2, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (678) {G0,W11,D4,L1,V0,M1} { op( op( e2, e3 ), e0 ) = op( e2, op( e3, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (679) {G0,W11,D4,L1,V0,M1} { op( op( e2, e3 ), e1 ) = op( e2, op( e3, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (680) {G0,W11,D4,L1,V0,M1} { op( op( e2, e3 ), e2 ) = op( e2, op( e3, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (681) {G0,W11,D4,L1,V0,M1} { op( op( e2, e3 ), e3 ) = op( e2, op( e3, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (682) {G0,W11,D4,L1,V0,M1} { op( op( e2, e3 ), e4 ) = op( e2, op( e3, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (683) {G0,W11,D4,L1,V0,M1} { op( op( e2, e3 ), e5 ) = op( e2, op( e3, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (684) {G0,W11,D4,L1,V0,M1} { op( op( e2, e4 ), e0 ) = op( e2, op( e4, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (685) {G0,W11,D4,L1,V0,M1} { op( op( e2, e4 ), e1 ) = op( e2, op( e4, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (686) {G0,W11,D4,L1,V0,M1} { op( op( e2, e4 ), e2 ) = op( e2, op( e4, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (687) {G0,W11,D4,L1,V0,M1} { op( op( e2, e4 ), e3 ) = op( e2, op( e4, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (688) {G0,W11,D4,L1,V0,M1} { op( op( e2, e4 ), e4 ) = op( e2, op( e4, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (689) {G0,W11,D4,L1,V0,M1} { op( op( e2, e4 ), e5 ) = op( e2, op( e4, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (690) {G0,W11,D4,L1,V0,M1} { op( op( e2, e5 ), e0 ) = op( e2, op( e5, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (691) {G0,W11,D4,L1,V0,M1} { op( op( e2, e5 ), e1 ) = op( e2, op( e5, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (692) {G0,W11,D4,L1,V0,M1} { op( op( e2, e5 ), e2 ) = op( e2, op( e5, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (693) {G0,W11,D4,L1,V0,M1} { op( op( e2, e5 ), e3 ) = op( e2, op( e5, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (694) {G0,W11,D4,L1,V0,M1} { op( op( e2, e5 ), e4 ) = op( e2, op( e5, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (695) {G0,W11,D4,L1,V0,M1} { op( op( e2, e5 ), e5 ) = op( e2, op( e5, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (696) {G0,W11,D4,L1,V0,M1} { op( op( e3, e0 ), e0 ) = op( e3, op( e0, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (697) {G0,W11,D4,L1,V0,M1} { op( op( e3, e0 ), e1 ) = op( e3, op( e0, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (698) {G0,W11,D4,L1,V0,M1} { op( op( e3, e0 ), e2 ) = op( e3, op( e0, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (699) {G0,W11,D4,L1,V0,M1} { op( op( e3, e0 ), e3 ) = op( e3, op( e0, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (700) {G0,W11,D4,L1,V0,M1} { op( op( e3, e0 ), e4 ) = op( e3, op( e0, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (701) {G0,W11,D4,L1,V0,M1} { op( op( e3, e0 ), e5 ) = op( e3, op( e0, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (702) {G0,W11,D4,L1,V0,M1} { op( op( e3, e1 ), e0 ) = op( e3, op( e1, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (703) {G0,W11,D4,L1,V0,M1} { op( op( e3, e1 ), e1 ) = op( e3, op( e1, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (704) {G0,W11,D4,L1,V0,M1} { op( op( e3, e1 ), e2 ) = op( e3, op( e1, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (705) {G0,W11,D4,L1,V0,M1} { op( op( e3, e1 ), e3 ) = op( e3, op( e1, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (706) {G0,W11,D4,L1,V0,M1} { op( op( e3, e1 ), e4 ) = op( e3, op( e1, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (707) {G0,W11,D4,L1,V0,M1} { op( op( e3, e1 ), e5 ) = op( e3, op( e1, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (708) {G0,W11,D4,L1,V0,M1} { op( op( e3, e2 ), e0 ) = op( e3, op( e2, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (709) {G0,W11,D4,L1,V0,M1} { op( op( e3, e2 ), e1 ) = op( e3, op( e2, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (710) {G0,W11,D4,L1,V0,M1} { op( op( e3, e2 ), e2 ) = op( e3, op( e2, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (711) {G0,W11,D4,L1,V0,M1} { op( op( e3, e2 ), e3 ) = op( e3, op( e2, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (712) {G0,W11,D4,L1,V0,M1} { op( op( e3, e2 ), e4 ) = op( e3, op( e2, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (713) {G0,W11,D4,L1,V0,M1} { op( op( e3, e2 ), e5 ) = op( e3, op( e2, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (714) {G0,W11,D4,L1,V0,M1} { op( op( e3, e3 ), e0 ) = op( e3, op( e3, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (715) {G0,W11,D4,L1,V0,M1} { op( op( e3, e3 ), e1 ) = op( e3, op( e3, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (716) {G0,W11,D4,L1,V0,M1} { op( op( e3, e3 ), e2 ) = op( e3, op( e3, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (717) {G0,W11,D4,L1,V0,M1} { op( op( e3, e3 ), e3 ) = op( e3, op( e3, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (718) {G0,W11,D4,L1,V0,M1} { op( op( e3, e3 ), e4 ) = op( e3, op( e3, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (719) {G0,W11,D4,L1,V0,M1} { op( op( e3, e3 ), e5 ) = op( e3, op( e3, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (720) {G0,W11,D4,L1,V0,M1} { op( op( e3, e4 ), e0 ) = op( e3, op( e4, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (721) {G0,W11,D4,L1,V0,M1} { op( op( e3, e4 ), e1 ) = op( e3, op( e4, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (722) {G0,W11,D4,L1,V0,M1} { op( op( e3, e4 ), e2 ) = op( e3, op( e4, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (723) {G0,W11,D4,L1,V0,M1} { op( op( e3, e4 ), e3 ) = op( e3, op( e4, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (724) {G0,W11,D4,L1,V0,M1} { op( op( e3, e4 ), e4 ) = op( e3, op( e4, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (725) {G0,W11,D4,L1,V0,M1} { op( op( e3, e4 ), e5 ) = op( e3, op( e4, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (726) {G0,W11,D4,L1,V0,M1} { op( op( e3, e5 ), e0 ) = op( e3, op( e5, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (727) {G0,W11,D4,L1,V0,M1} { op( op( e3, e5 ), e1 ) = op( e3, op( e5, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (728) {G0,W11,D4,L1,V0,M1} { op( op( e3, e5 ), e2 ) = op( e3, op( e5, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (729) {G0,W11,D4,L1,V0,M1} { op( op( e3, e5 ), e3 ) = op( e3, op( e5, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (730) {G0,W11,D4,L1,V0,M1} { op( op( e3, e5 ), e4 ) = op( e3, op( e5, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (731) {G0,W11,D4,L1,V0,M1} { op( op( e3, e5 ), e5 ) = op( e3, op( e5, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (732) {G0,W11,D4,L1,V0,M1} { op( op( e4, e0 ), e0 ) = op( e4, op( e0, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (733) {G0,W11,D4,L1,V0,M1} { op( op( e4, e0 ), e1 ) = op( e4, op( e0, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (734) {G0,W11,D4,L1,V0,M1} { op( op( e4, e0 ), e2 ) = op( e4, op( e0, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (735) {G0,W11,D4,L1,V0,M1} { op( op( e4, e0 ), e3 ) = op( e4, op( e0, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (736) {G0,W11,D4,L1,V0,M1} { op( op( e4, e0 ), e4 ) = op( e4, op( e0, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (737) {G0,W11,D4,L1,V0,M1} { op( op( e4, e0 ), e5 ) = op( e4, op( e0, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (738) {G0,W11,D4,L1,V0,M1} { op( op( e4, e1 ), e0 ) = op( e4, op( e1, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (739) {G0,W11,D4,L1,V0,M1} { op( op( e4, e1 ), e1 ) = op( e4, op( e1, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (740) {G0,W11,D4,L1,V0,M1} { op( op( e4, e1 ), e2 ) = op( e4, op( e1, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (741) {G0,W11,D4,L1,V0,M1} { op( op( e4, e1 ), e3 ) = op( e4, op( e1, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (742) {G0,W11,D4,L1,V0,M1} { op( op( e4, e1 ), e4 ) = op( e4, op( e1, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (743) {G0,W11,D4,L1,V0,M1} { op( op( e4, e1 ), e5 ) = op( e4, op( e1, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (744) {G0,W11,D4,L1,V0,M1} { op( op( e4, e2 ), e0 ) = op( e4, op( e2, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (745) {G0,W11,D4,L1,V0,M1} { op( op( e4, e2 ), e1 ) = op( e4, op( e2, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (746) {G0,W11,D4,L1,V0,M1} { op( op( e4, e2 ), e2 ) = op( e4, op( e2, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (747) {G0,W11,D4,L1,V0,M1} { op( op( e4, e2 ), e3 ) = op( e4, op( e2, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (748) {G0,W11,D4,L1,V0,M1} { op( op( e4, e2 ), e4 ) = op( e4, op( e2, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (749) {G0,W11,D4,L1,V0,M1} { op( op( e4, e2 ), e5 ) = op( e4, op( e2, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (750) {G0,W11,D4,L1,V0,M1} { op( op( e4, e3 ), e0 ) = op( e4, op( e3, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (751) {G0,W11,D4,L1,V0,M1} { op( op( e4, e3 ), e1 ) = op( e4, op( e3, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (752) {G0,W11,D4,L1,V0,M1} { op( op( e4, e3 ), e2 ) = op( e4, op( e3, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (753) {G0,W11,D4,L1,V0,M1} { op( op( e4, e3 ), e3 ) = op( e4, op( e3, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (754) {G0,W11,D4,L1,V0,M1} { op( op( e4, e3 ), e4 ) = op( e4, op( e3, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (755) {G0,W11,D4,L1,V0,M1} { op( op( e4, e3 ), e5 ) = op( e4, op( e3, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (756) {G0,W11,D4,L1,V0,M1} { op( op( e4, e4 ), e0 ) = op( e4, op( e4, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (757) {G0,W11,D4,L1,V0,M1} { op( op( e4, e4 ), e1 ) = op( e4, op( e4, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (758) {G0,W11,D4,L1,V0,M1} { op( op( e4, e4 ), e2 ) = op( e4, op( e4, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (759) {G0,W11,D4,L1,V0,M1} { op( op( e4, e4 ), e3 ) = op( e4, op( e4, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (760) {G0,W11,D4,L1,V0,M1} { op( op( e4, e4 ), e4 ) = op( e4, op( e4, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (761) {G0,W11,D4,L1,V0,M1} { op( op( e4, e4 ), e5 ) = op( e4, op( e4, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (762) {G0,W11,D4,L1,V0,M1} { op( op( e4, e5 ), e0 ) = op( e4, op( e5, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (763) {G0,W11,D4,L1,V0,M1} { op( op( e4, e5 ), e1 ) = op( e4, op( e5, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (764) {G0,W11,D4,L1,V0,M1} { op( op( e4, e5 ), e2 ) = op( e4, op( e5, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (765) {G0,W11,D4,L1,V0,M1} { op( op( e4, e5 ), e3 ) = op( e4, op( e5, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (766) {G0,W11,D4,L1,V0,M1} { op( op( e4, e5 ), e4 ) = op( e4, op( e5, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (767) {G0,W11,D4,L1,V0,M1} { op( op( e4, e5 ), e5 ) = op( e4, op( e5, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (768) {G0,W11,D4,L1,V0,M1} { op( op( e5, e0 ), e0 ) = op( e5, op( e0, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (769) {G0,W11,D4,L1,V0,M1} { op( op( e5, e0 ), e1 ) = op( e5, op( e0, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (770) {G0,W11,D4,L1,V0,M1} { op( op( e5, e0 ), e2 ) = op( e5, op( e0, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (771) {G0,W11,D4,L1,V0,M1} { op( op( e5, e0 ), e3 ) = op( e5, op( e0, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (772) {G0,W11,D4,L1,V0,M1} { op( op( e5, e0 ), e4 ) = op( e5, op( e0, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (773) {G0,W11,D4,L1,V0,M1} { op( op( e5, e0 ), e5 ) = op( e5, op( e0, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (774) {G0,W11,D4,L1,V0,M1} { op( op( e5, e1 ), e0 ) = op( e5, op( e1, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (775) {G0,W11,D4,L1,V0,M1} { op( op( e5, e1 ), e1 ) = op( e5, op( e1, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (776) {G0,W11,D4,L1,V0,M1} { op( op( e5, e1 ), e2 ) = op( e5, op( e1, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (777) {G0,W11,D4,L1,V0,M1} { op( op( e5, e1 ), e3 ) = op( e5, op( e1, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (778) {G0,W11,D4,L1,V0,M1} { op( op( e5, e1 ), e4 ) = op( e5, op( e1, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (779) {G0,W11,D4,L1,V0,M1} { op( op( e5, e1 ), e5 ) = op( e5, op( e1, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (780) {G0,W11,D4,L1,V0,M1} { op( op( e5, e2 ), e0 ) = op( e5, op( e2, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (781) {G0,W11,D4,L1,V0,M1} { op( op( e5, e2 ), e1 ) = op( e5, op( e2, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (782) {G0,W11,D4,L1,V0,M1} { op( op( e5, e2 ), e2 ) = op( e5, op( e2, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (783) {G0,W11,D4,L1,V0,M1} { op( op( e5, e2 ), e3 ) = op( e5, op( e2, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (784) {G0,W11,D4,L1,V0,M1} { op( op( e5, e2 ), e4 ) = op( e5, op( e2, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (785) {G0,W11,D4,L1,V0,M1} { op( op( e5, e2 ), e5 ) = op( e5, op( e2, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (786) {G0,W11,D4,L1,V0,M1} { op( op( e5, e3 ), e0 ) = op( e5, op( e3, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (787) {G0,W11,D4,L1,V0,M1} { op( op( e5, e3 ), e1 ) = op( e5, op( e3, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (788) {G0,W11,D4,L1,V0,M1} { op( op( e5, e3 ), e2 ) = op( e5, op( e3, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (789) {G0,W11,D4,L1,V0,M1} { op( op( e5, e3 ), e3 ) = op( e5, op( e3, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (790) {G0,W11,D4,L1,V0,M1} { op( op( e5, e3 ), e4 ) = op( e5, op( e3, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (791) {G0,W11,D4,L1,V0,M1} { op( op( e5, e3 ), e5 ) = op( e5, op( e3, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (792) {G0,W11,D4,L1,V0,M1} { op( op( e5, e4 ), e0 ) = op( e5, op( e4, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (793) {G0,W11,D4,L1,V0,M1} { op( op( e5, e4 ), e1 ) = op( e5, op( e4, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (794) {G0,W11,D4,L1,V0,M1} { op( op( e5, e4 ), e2 ) = op( e5, op( e4, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (795) {G0,W11,D4,L1,V0,M1} { op( op( e5, e4 ), e3 ) = op( e5, op( e4, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (796) {G0,W11,D4,L1,V0,M1} { op( op( e5, e4 ), e4 ) = op( e5, op( e4, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (797) {G0,W11,D4,L1,V0,M1} { op( op( e5, e4 ), e5 ) = op( e5, op( e4, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (798) {G0,W11,D4,L1,V0,M1} { op( op( e5, e5 ), e0 ) = op( e5, op( e5, e0 )
% 0.69/1.11 ) }.
% 0.69/1.11 (799) {G0,W11,D4,L1,V0,M1} { op( op( e5, e5 ), e1 ) = op( e5, op( e5, e1 )
% 0.69/1.11 ) }.
% 0.69/1.11 (800) {G0,W11,D4,L1,V0,M1} { op( op( e5, e5 ), e2 ) = op( e5, op( e5, e2 )
% 0.69/1.11 ) }.
% 0.69/1.11 (801) {G0,W11,D4,L1,V0,M1} { op( op( e5, e5 ), e3 ) = op( e5, op( e5, e3 )
% 0.69/1.11 ) }.
% 0.69/1.11 (802) {G0,W11,D4,L1,V0,M1} { op( op( e5, e5 ), e4 ) = op( e5, op( e5, e4 )
% 0.69/1.11 ) }.
% 0.69/1.11 (803) {G0,W11,D4,L1,V0,M1} { op( op( e5, e5 ), e5 ) = op( e5, op( e5, e5 )
% 0.69/1.11 ) }.
% 0.69/1.11 (804) {G0,W5,D3,L1,V0,M1} { op( unit, e0 ) = e0 }.
% 0.69/1.11 (805) {G0,W5,D3,L1,V0,M1} { op( e0, unit ) = e0 }.
% 0.69/1.11 (806) {G0,W5,D3,L1,V0,M1} { op( unit, e1 ) = e1 }.
% 0.69/1.11 (807) {G0,W5,D3,L1,V0,M1} { op( e1, unit ) = e1 }.
% 0.69/1.11 (808) {G0,W5,D3,L1,V0,M1} { op( unit, e2 ) = e2 }.
% 0.69/1.11 (809) {G0,W5,D3,L1,V0,M1} { op( e2, unit ) = e2 }.
% 0.69/1.11 (810) {G0,W5,D3,L1,V0,M1} { op( unit, e3 ) = e3 }.
% 0.69/1.11 (811) {G0,W5,D3,L1,V0,M1} { op( e3, unit ) = e3 }.
% 0.69/1.11 (812) {G0,W5,D3,L1,V0,M1} { op( unit, e4 ) = e4 }.
% 0.69/1.11 (813) {G0,W5,D3,L1,V0,M1} { op( e4, unit ) = e4 }.
% 0.69/1.11 (814) {G0,W5,D3,L1,V0,M1} { op( unit, e5 ) = e5 }.
% 0.69/1.11 (815) {G0,W5,D3,L1,V0,M1} { op( e5, unit ) = e5 }.
% 0.69/1.11 (816) {G0,W18,D2,L6,V0,M6} { unit = e0, unit = e1, unit = e2, unit = e3,
% 0.69/1.11 unit = e4, unit = e5 }.
% 0.69/1.11 (817) {G0,W6,D4,L1,V0,M1} { op( e0, inv( e0 ) ) = unit }.
% 0.69/1.11 (818) {G0,W6,D4,L1,V0,M1} { op( inv( e0 ), e0 ) = unit }.
% 0.69/1.11 (819) {G0,W6,D4,L1,V0,M1} { op( e1, inv( e1 ) ) = unit }.
% 0.69/1.11 (820) {G0,W6,D4,L1,V0,M1} { op( inv( e1 ), e1 ) = unit }.
% 0.69/1.11 (821) {G0,W6,D4,L1,V0,M1} { op( e2, inv( e2 ) ) = unit }.
% 0.69/1.11 (822) {G0,W6,D4,L1,V0,M1} { op( inv( e2 ), e2 ) = unit }.
% 0.69/1.11 (823) {G0,W6,D4,L1,V0,M1} { op( e3, inv( e3 ) ) = unit }.
% 0.69/1.11 (824) {G0,W6,D4,L1,V0,M1} { op( inv( e3 ), e3 ) = unit }.
% 0.69/1.11 (825) {G0,W6,D4,L1,V0,M1} { op( e4, inv( e4 ) ) = unit }.
% 0.69/1.11 (826) {G0,W6,D4,L1,V0,M1} { op( inv( e4 ), e4 ) = unit }.
% 0.69/1.11 (827) {G0,W6,D4,L1,V0,M1} { op( e5, inv( e5 ) ) = unit }.
% 0.69/1.11 (828) {G0,W6,D4,L1,V0,M1} { op( inv( e5 ), e5 ) = unit }.
% 0.69/1.11 (829) {G0,W24,D3,L6,V0,M6} { inv( e0 ) = e0, inv( e0 ) = e1, inv( e0 ) =
% 0.69/1.11 e2, inv( e0 ) = e3, inv( e0 ) = e4, inv( e0 ) = e5 }.
% 0.69/1.11 (830) {G0,W24,D3,L6,V0,M6} { inv( e1 ) = e0, inv( e1 ) = e1, inv( e1 ) =
% 0.69/1.11 e2, inv( e1 ) = e3, inv( e1 ) = e4, inv( e1 ) = e5 }.
% 0.69/1.11 (831) {G0,W24,D3,L6,V0,M6} { inv( e2 ) = e0, inv( e2 ) = e1, inv( e2 ) =
% 0.69/1.11 e2, inv( e2 ) = e3, inv( e2 ) = e4, inv( e2 ) = e5 }.
% 0.69/1.11 (832) {G0,W24,D3,L6,V0,M6} { inv( e3 ) = e0, inv( e3 ) = e1, inv( e3 ) =
% 0.69/1.11 e2, inv( e3 ) = e3, inv( e3 ) = e4, inv( e3 ) = e5 }.
% 0.69/1.11 (833) {G0,W24,D3,L6,V0,M6} { inv( e4 ) = e0, inv( e4 ) = e1, inv( e4 ) =
% 0.69/1.11 e2, inv( e4 ) = e3, inv( e4 ) = e4, inv( e4 ) = e5 }.
% 0.69/1.11 (834) {G0,W24,D3,L6,V0,M6} { inv( e5 ) = e0, inv( e5 ) = e1, inv( e5 ) =
% 0.69/1.11 e2, inv( e5 ) = e3, inv( e5 ) = e4, inv( e5 ) = e5 }.
% 0.69/1.11 (835) {G0,W4,D3,L1,V0,M1} { inv( unit ) = unit }.
% 0.69/1.11 (836) {G0,W5,D4,L1,V0,M1} { inv( inv( e0 ) ) = e0 }.
% 0.69/1.11 (837) {G0,W5,D4,L1,V0,M1} { inv( inv( e1 ) ) = e1 }.
% 0.69/1.11 (838) {G0,W5,D4,L1,V0,M1} { inv( inv( e2 ) ) = e2 }.
% 0.69/1.11 (839) {G0,W5,D4,L1,V0,M1} { inv( inv( e3 ) ) = e3 }.
% 0.69/1.11 (840) {G0,W5,D4,L1,V0,M1} { inv( inv( e4 ) ) = e4 }.
% 0.69/1.11 (841) {G0,W5,D4,L1,V0,M1} { inv( inv( e5 ) ) = e5 }.
% 0.69/1.11 (842) {G0,W8,D3,L2,V0,M2} { ! inv( e0 ) = e0, inv( e0 ) = e0 }.
% 0.69/1.11 (843) {G0,W8,D3,L2,V0,M2} { ! inv( e0 ) = e1, inv( e1 ) = e0 }.
% 0.69/1.11 (844) {G0,W8,D3,L2,V0,M2} { ! inv( e0 ) = e2, inv( e2 ) = e0 }.
% 0.69/1.11 (845) {G0,W8,D3,L2,V0,M2} { ! inv( e0 ) = e3, inv( e3 ) = e0 }.
% 0.69/1.11 (846) {G0,W8,D3,L2,V0,M2} { ! inv( e0 ) = e4, inv( e4 ) = e0 }.
% 0.69/1.11 (847) {G0,W8,D3,L2,V0,M2} { ! inv( e0 ) = e5, inv( e5 ) = e0 }.
% 0.69/1.11 (848) {G0,W8,D3,L2,V0,M2} { ! inv( e1 ) = e0, inv( e0 ) = e1 }.
% 0.69/1.11 (849) {G0,W8,D3,L2,V0,M2} { ! inv( e1 ) = e1, inv( e1 ) = e1 }.
% 0.69/1.11 (850) {G0,W8,D3,L2,V0,M2} { ! inv( e1 ) = e2, inv( e2 ) = e1 }.
% 0.69/1.11 (851) {G0,W8,D3,L2,V0,M2} { ! inv( e1 ) = e3, inv( e3 ) = e1 }.
% 0.69/1.11 (852) {G0,W8,D3,L2,V0,M2} { ! inv( e1 ) = e4, inv( e4 ) = e1 }.
% 0.69/1.11 (853) {G0,W8,D3,L2,V0,M2} { ! inv( e1 ) = e5, inv( e5 ) = e1 }.
% 0.69/1.11 (854) {G0,W8,D3,L2,V0,M2} { ! inv( e2 ) = e0, inv( e0 ) = e2 }.
% 0.69/1.11 (855) {G0,W8,D3,L2,V0,M2} { ! inv( e2 ) = e1, inv( e1 ) = e2 }.
% 0.69/1.11 (856) {G0,W8,D3,L2,V0,M2} { ! inv( e2 ) = e2, inv( e2 ) = e2 }.
% 0.69/1.11 (857) {G0,W8,D3,L2,V0,M2} { ! inv( e2 ) = e3, inv( e3 ) = e2 }.
% 0.69/1.11 (858) {G0,W8,D3,L2,V0,M2} { ! inv( e2 ) = e4, inv( e4 ) = e2 }.
% 0.69/1.11 (859) {G0,W8,D3,L2,V0,M2} { ! inv( e2 ) = e5, inv( e5 ) = e2 }.
% 0.69/1.11 (860) {G0,W8,D3,L2,V0,M2} { ! inv( e3 ) = e0, inv( e0 ) = e3 }.
% 0.69/1.11 (861) {G0,W8,D3,L2,V0,M2} { ! inv( e3 ) = e1, inv( e1 ) = e3 }.
% 0.69/1.11 (862) {G0,W8,D3,L2,V0,M2} { ! inv( e3 ) = e2, inv( e2 ) = e3 }.
% 0.69/1.11 (863) {G0,W8,D3,L2,V0,M2} { ! inv( e3 ) = e3, inv( e3 ) = e3 }.
% 0.69/1.11 (864) {G0,W8,D3,L2,V0,M2} { ! inv( e3 ) = e4, inv( e4 ) = e3 }.
% 0.69/1.11 (865) {G0,W8,D3,L2,V0,M2} { ! inv( e3 ) = e5, inv( e5 ) = e3 }.
% 0.69/1.11 (866) {G0,W8,D3,L2,V0,M2} { ! inv( e4 ) = e0, inv( e0 ) = e4 }.
% 0.69/1.11 (867) {G0,W8,D3,L2,V0,M2} { ! inv( e4 ) = e1, inv( e1 ) = e4 }.
% 0.69/1.11 (868) {G0,W8,D3,L2,V0,M2} { ! inv( e4 ) = e2, inv( e2 ) = e4 }.
% 0.69/1.11 (869) {G0,W8,D3,L2,V0,M2} { ! inv( e4 ) = e3, inv( e3 ) = e4 }.
% 0.69/1.11 (870) {G0,W8,D3,L2,V0,M2} { ! inv( e4 ) = e4, inv( e4 ) = e4 }.
% 0.69/1.11 (871) {G0,W8,D3,L2,V0,M2} { ! inv( e4 ) = e5, inv( e5 ) = e4 }.
% 0.69/1.11 (872) {G0,W8,D3,L2,V0,M2} { ! inv( e5 ) = e0, inv( e0 ) = e5 }.
% 0.69/1.11 (873) {G0,W8,D3,L2,V0,M2} { ! inv( e5 ) = e1, inv( e1 ) = e5 }.
% 0.69/1.11 (874) {G0,W8,D3,L2,V0,M2} { ! inv( e5 ) = e2, inv( e2 ) = e5 }.
% 0.69/1.11 (875) {G0,W8,D3,L2,V0,M2} { ! inv( e5 ) = e3, inv( e3 ) = e5 }.
% 0.69/1.11 (876) {G0,W8,D3,L2,V0,M2} { ! inv( e5 ) = e4, inv( e4 ) = e5 }.
% 0.69/1.11 (877) {G0,W8,D3,L2,V0,M2} { ! inv( e5 ) = e5, inv( e5 ) = e5 }.
% 0.69/1.11 (878) {G0,W5,D3,L1,V0,M1} { ! inv( e0 ) = inv( e1 ) }.
% 0.69/1.11 (879) {G0,W5,D3,L1,V0,M1} { ! inv( e0 ) = inv( e2 ) }.
% 0.69/1.11 (880) {G0,W5,D3,L1,V0,M1} { ! inv( e0 ) = inv( e3 ) }.
% 0.69/1.11 (881) {G0,W5,D3,L1,V0,M1} { ! inv( e0 ) = inv( e4 ) }.
% 0.69/1.11 (882) {G0,W5,D3,L1,V0,M1} { ! inv( e0 ) = inv( e5 ) }.
% 0.69/1.11 (883) {G0,W5,D3,L1,V0,M1} { ! inv( e1 ) = inv( e2 ) }.
% 0.69/1.11 (884) {G0,W5,D3,L1,V0,M1} { ! inv( e1 ) = inv( e3 ) }.
% 0.69/1.11 (885) {G0,W5,D3,L1,V0,M1} { ! inv( e1 ) = inv( e4 ) }.
% 0.69/1.11 (886) {G0,W5,D3,L1,V0,M1} { ! inv( e1 ) = inv( e5 ) }.
% 0.69/1.11 (887) {G0,W5,D3,L1,V0,M1} { ! inv( e2 ) = inv( e3 ) }.
% 0.69/1.11 (888) {G0,W5,D3,L1,V0,M1} { ! inv( e2 ) = inv( e4 ) }.
% 0.69/1.11 (889) {G0,W5,D3,L1,V0,M1} { ! inv( e2 ) = inv( e5 ) }.
% 0.69/1.11 (890) {G0,W5,D3,L1,V0,M1} { ! inv( e3 ) = inv( e4 ) }.
% 0.69/1.11 (891) {G0,W5,D3,L1,V0,M1} { ! inv( e3 ) = inv( e5 ) }.
% 0.69/1.11 (892) {G0,W5,D3,L1,V0,M1} { ! inv( e4 ) = inv( e5 ) }.
% 0.69/1.11 (893) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e1, e0 ) }.
% 0.69/1.11 (894) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e2, e0 ) }.
% 0.69/1.11 (895) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e3, e0 ) }.
% 0.69/1.11 (896) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e4, e0 ) }.
% 0.69/1.11 (897) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e5, e0 ) }.
% 0.69/1.11 (898) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e2, e0 ) }.
% 0.69/1.11 (899) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e3, e0 ) }.
% 0.69/1.11 (900) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e4, e0 ) }.
% 0.69/1.11 (901) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e5, e0 ) }.
% 0.69/1.11 (902) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e3, e0 ) }.
% 0.69/1.11 (903) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e4, e0 ) }.
% 0.69/1.11 (904) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e5, e0 ) }.
% 0.69/1.11 (905) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e4, e0 ) }.
% 0.69/1.11 (906) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e5, e0 ) }.
% 0.69/1.11 (907) {G0,W7,D3,L1,V0,M1} { ! op( e4, e0 ) = op( e5, e0 ) }.
% 0.69/1.11 (908) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e1, e1 ) }.
% 0.69/1.11 (909) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e2, e1 ) }.
% 0.69/1.11 (910) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e3, e1 ) }.
% 0.69/1.11 (911) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e4, e1 ) }.
% 0.69/1.11 (912) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e5, e1 ) }.
% 0.69/1.11 (913) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e2, e1 ) }.
% 0.69/1.11 (914) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e3, e1 ) }.
% 0.69/1.11 (915) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e4, e1 ) }.
% 0.69/1.11 (916) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e5, e1 ) }.
% 0.69/1.11 (917) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e3, e1 ) }.
% 0.69/1.11 (918) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e4, e1 ) }.
% 0.69/1.11 (919) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e5, e1 ) }.
% 0.69/1.11 (920) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e4, e1 ) }.
% 0.69/1.11 (921) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e5, e1 ) }.
% 0.69/1.11 (922) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e5, e1 ) }.
% 0.69/1.11 (923) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e1, e2 ) }.
% 0.69/1.11 (924) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e2, e2 ) }.
% 0.69/1.11 (925) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e3, e2 ) }.
% 0.69/1.11 (926) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e4, e2 ) }.
% 0.69/1.11 (927) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e5, e2 ) }.
% 0.69/1.11 (928) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e2, e2 ) }.
% 0.69/1.11 (929) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e3, e2 ) }.
% 0.69/1.11 (930) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e4, e2 ) }.
% 0.69/1.11 (931) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e5, e2 ) }.
% 0.69/1.11 (932) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e3, e2 ) }.
% 0.69/1.11 (933) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e4, e2 ) }.
% 0.69/1.11 (934) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e5, e2 ) }.
% 0.69/1.11 (935) {G0,W7,D3,L1,V0,M1} { ! op( e3, e2 ) = op( e4, e2 ) }.
% 0.69/1.11 (936) {G0,W7,D3,L1,V0,M1} { ! op( e3, e2 ) = op( e5, e2 ) }.
% 0.69/1.11 (937) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e5, e2 ) }.
% 0.69/1.11 (938) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e1, e3 ) }.
% 0.69/1.11 (939) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e2, e3 ) }.
% 0.69/1.11 (940) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e3, e3 ) }.
% 0.69/1.11 (941) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e4, e3 ) }.
% 0.69/1.11 (942) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e5, e3 ) }.
% 0.69/1.11 (943) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e2, e3 ) }.
% 0.69/1.11 (944) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e3, e3 ) }.
% 0.69/1.11 (945) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e4, e3 ) }.
% 0.69/1.11 (946) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e5, e3 ) }.
% 0.69/1.11 (947) {G0,W7,D3,L1,V0,M1} { ! op( e2, e3 ) = op( e3, e3 ) }.
% 0.69/1.11 (948) {G0,W7,D3,L1,V0,M1} { ! op( e2, e3 ) = op( e4, e3 ) }.
% 0.69/1.11 (949) {G0,W7,D3,L1,V0,M1} { ! op( e2, e3 ) = op( e5, e3 ) }.
% 0.69/1.11 (950) {G0,W7,D3,L1,V0,M1} { ! op( e3, e3 ) = op( e4, e3 ) }.
% 0.69/1.11 (951) {G0,W7,D3,L1,V0,M1} { ! op( e3, e3 ) = op( e5, e3 ) }.
% 0.69/1.11 (952) {G0,W7,D3,L1,V0,M1} { ! op( e4, e3 ) = op( e5, e3 ) }.
% 0.69/1.11 (953) {G0,W7,D3,L1,V0,M1} { ! op( e0, e4 ) = op( e1, e4 ) }.
% 0.69/1.11 (954) {G0,W7,D3,L1,V0,M1} { ! op( e0, e4 ) = op( e2, e4 ) }.
% 0.69/1.11 (955) {G0,W7,D3,L1,V0,M1} { ! op( e0, e4 ) = op( e3, e4 ) }.
% 0.69/1.11 (956) {G0,W7,D3,L1,V0,M1} { ! op( e0, e4 ) = op( e4, e4 ) }.
% 0.69/1.11 (957) {G0,W7,D3,L1,V0,M1} { ! op( e0, e4 ) = op( e5, e4 ) }.
% 0.69/1.11 (958) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e2, e4 ) }.
% 0.69/1.11 (959) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e3, e4 ) }.
% 0.69/1.11 (960) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e4, e4 ) }.
% 0.69/1.11 (961) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e5, e4 ) }.
% 0.69/1.11 (962) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e3, e4 ) }.
% 0.69/1.11 (963) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e4, e4 ) }.
% 0.69/1.11 (964) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e5, e4 ) }.
% 0.69/1.11 (965) {G0,W7,D3,L1,V0,M1} { ! op( e3, e4 ) = op( e4, e4 ) }.
% 0.69/1.11 (966) {G0,W7,D3,L1,V0,M1} { ! op( e3, e4 ) = op( e5, e4 ) }.
% 0.69/1.11 (967) {G0,W7,D3,L1,V0,M1} { ! op( e4, e4 ) = op( e5, e4 ) }.
% 0.69/1.11 (968) {G0,W7,D3,L1,V0,M1} { ! op( e0, e5 ) = op( e1, e5 ) }.
% 0.69/1.11 (969) {G0,W7,D3,L1,V0,M1} { ! op( e0, e5 ) = op( e2, e5 ) }.
% 0.69/1.11 (970) {G0,W7,D3,L1,V0,M1} { ! op( e0, e5 ) = op( e3, e5 ) }.
% 0.69/1.11 (971) {G0,W7,D3,L1,V0,M1} { ! op( e0, e5 ) = op( e4, e5 ) }.
% 0.69/1.11 (972) {G0,W7,D3,L1,V0,M1} { ! op( e0, e5 ) = op( e5, e5 ) }.
% 0.69/1.11 (973) {G0,W7,D3,L1,V0,M1} { ! op( e1, e5 ) = op( e2, e5 ) }.
% 0.69/1.11 (974) {G0,W7,D3,L1,V0,M1} { ! op( e1, e5 ) = op( e3, e5 ) }.
% 0.69/1.11 (975) {G0,W7,D3,L1,V0,M1} { ! op( e1, e5 ) = op( e4, e5 ) }.
% 0.69/1.11 (976) {G0,W7,D3,L1,V0,M1} { ! op( e1, e5 ) = op( e5, e5 ) }.
% 0.69/1.11 (977) {G0,W7,D3,L1,V0,M1} { ! op( e2, e5 ) = op( e3, e5 ) }.
% 0.69/1.11 (978) {G0,W7,D3,L1,V0,M1} { ! op( e2, e5 ) = op( e4, e5 ) }.
% 0.69/1.11 (979) {G0,W7,D3,L1,V0,M1} { ! op( e2, e5 ) = op( e5, e5 ) }.
% 0.69/1.11 (980) {G0,W7,D3,L1,V0,M1} { ! op( e3, e5 ) = op( e4, e5 ) }.
% 0.69/1.11 (981) {G0,W7,D3,L1,V0,M1} { ! op( e3, e5 ) = op( e5, e5 ) }.
% 0.69/1.11 (982) {G0,W7,D3,L1,V0,M1} { ! op( e4, e5 ) = op( e5, e5 ) }.
% 0.69/1.11 (983) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e1 ) }.
% 0.69/1.11 (984) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e2 ) }.
% 0.69/1.11 (985) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e3 ) }.
% 0.69/1.11 (986) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e4 ) }.
% 0.69/1.11 (987) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e5 ) }.
% 0.69/1.11 (988) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e0, e2 ) }.
% 0.69/1.11 (989) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e0, e3 ) }.
% 0.69/1.11 (990) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e0, e4 ) }.
% 0.69/1.11 (991) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e0, e5 ) }.
% 0.69/1.11 (992) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e0, e3 ) }.
% 0.69/1.11 (993) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e0, e4 ) }.
% 0.69/1.11 (994) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e0, e5 ) }.
% 0.69/1.11 (995) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e0, e4 ) }.
% 0.69/1.11 (996) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e0, e5 ) }.
% 0.69/1.11 (997) {G0,W7,D3,L1,V0,M1} { ! op( e0, e4 ) = op( e0, e5 ) }.
% 0.69/1.11 (998) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e1 ) }.
% 0.69/1.11 (999) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e2 ) }.
% 0.69/1.11 (1000) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e3 ) }.
% 0.69/1.11 (1001) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e4 ) }.
% 0.69/1.11 (1002) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e5 ) }.
% 0.69/1.11 (1003) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e1, e2 ) }.
% 0.69/1.11 (1004) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e1, e3 ) }.
% 0.69/1.11 (1005) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e1, e4 ) }.
% 0.69/1.11 (1006) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e1, e5 ) }.
% 0.69/1.11 (1007) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e1, e3 ) }.
% 0.69/1.11 (1008) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e1, e4 ) }.
% 0.69/1.11 (1009) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e1, e5 ) }.
% 0.69/1.11 (1010) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e1, e4 ) }.
% 0.69/1.11 (1011) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e1, e5 ) }.
% 0.69/1.11 (1012) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e1, e5 ) }.
% 0.69/1.11 (1013) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e1 ) }.
% 0.69/1.11 (1014) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e2 ) }.
% 0.69/1.11 (1015) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e3 ) }.
% 0.69/1.11 (1016) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e4 ) }.
% 0.69/1.11 (1017) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e5 ) }.
% 0.69/1.11 (1018) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e2 ) }.
% 0.69/1.11 (1019) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e3 ) }.
% 0.69/1.11 (1020) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e4 ) }.
% 0.69/1.11 (1021) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e5 ) }.
% 0.69/1.11 (1022) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e2, e3 ) }.
% 0.69/1.11 (1023) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e2, e4 ) }.
% 0.69/1.11 (1024) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e2, e5 ) }.
% 0.69/1.11 (1025) {G0,W7,D3,L1,V0,M1} { ! op( e2, e3 ) = op( e2, e4 ) }.
% 0.69/1.11 (1026) {G0,W7,D3,L1,V0,M1} { ! op( e2, e3 ) = op( e2, e5 ) }.
% 0.69/1.11 (1027) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e2, e5 ) }.
% 0.69/1.11 (1028) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e1 ) }.
% 0.69/1.11 (1029) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e2 ) }.
% 0.69/1.11 (1030) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e3 ) }.
% 0.69/1.11 (1031) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e4 ) }.
% 0.69/1.11 (1032) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e5 ) }.
% 0.69/1.11 (1033) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e3, e2 ) }.
% 0.69/1.11 (1034) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e3, e3 ) }.
% 0.69/1.11 (1035) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e3, e4 ) }.
% 0.69/1.11 (1036) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e3, e5 ) }.
% 0.69/1.11 (1037) {G0,W7,D3,L1,V0,M1} { ! op( e3, e2 ) = op( e3, e3 ) }.
% 0.69/1.11 (1038) {G0,W7,D3,L1,V0,M1} { ! op( e3, e2 ) = op( e3, e4 ) }.
% 0.69/1.11 (1039) {G0,W7,D3,L1,V0,M1} { ! op( e3, e2 ) = op( e3, e5 ) }.
% 0.69/1.11 (1040) {G0,W7,D3,L1,V0,M1} { ! op( e3, e3 ) = op( e3, e4 ) }.
% 0.69/1.11 (1041) {G0,W7,D3,L1,V0,M1} { ! op( e3, e3 ) = op( e3, e5 ) }.
% 0.69/1.11 (1042) {G0,W7,D3,L1,V0,M1} { ! op( e3, e4 ) = op( e3, e5 ) }.
% 0.69/1.11 (1043) {G0,W7,D3,L1,V0,M1} { ! op( e4, e0 ) = op( e4, e1 ) }.
% 0.69/1.11 (1044) {G0,W7,D3,L1,V0,M1} { ! op( e4, e0 ) = op( e4, e2 ) }.
% 0.69/1.11 (1045) {G0,W7,D3,L1,V0,M1} { ! op( e4, e0 ) = op( e4, e3 ) }.
% 0.69/1.11 (1046) {G0,W7,D3,L1,V0,M1} { ! op( e4, e0 ) = op( e4, e4 ) }.
% 0.69/1.11 (1047) {G0,W7,D3,L1,V0,M1} { ! op( e4, e0 ) = op( e4, e5 ) }.
% 0.69/1.11 (1048) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e4, e2 ) }.
% 0.69/1.11 (1049) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e4, e3 ) }.
% 0.69/1.11 (1050) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e4, e4 ) }.
% 0.69/1.11 (1051) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e4, e5 ) }.
% 0.69/1.11 (1052) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e4, e3 ) }.
% 0.69/1.11 (1053) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e4, e4 ) }.
% 0.69/1.11 (1054) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e4, e5 ) }.
% 0.69/1.11 (1055) {G0,W7,D3,L1,V0,M1} { ! op( e4, e3 ) = op( e4, e4 ) }.
% 0.69/1.11 (1056) {G0,W7,D3,L1,V0,M1} { ! op( e4, e3 ) = op( e4, e5 ) }.
% 0.69/1.11 (1057) {G0,W7,D3,L1,V0,M1} { ! op( e4, e4 ) = op( e4, e5 ) }.
% 0.69/1.11 (1058) {G0,W7,D3,L1,V0,M1} { ! op( e5, e0 ) = op( e5, e1 ) }.
% 0.69/1.11 (1059) {G0,W7,D3,L1,V0,M1} { ! op( e5, e0 ) = op( e5, e2 ) }.
% 0.69/1.11 (1060) {G0,W7,D3,L1,V0,M1} { ! op( e5, e0 ) = op( e5, e3 ) }.
% 0.69/1.11 (1061) {G0,W7,D3,L1,V0,M1} { ! op( e5, e0 ) = op( e5, e4 ) }.
% 0.69/1.11 (1062) {G0,W7,D3,L1,V0,M1} { ! op( e5, e0 ) = op( e5, e5 ) }.
% 0.69/1.11 (1063) {G0,W7,D3,L1,V0,M1} { ! op( e5, e1 ) = op( e5, e2 ) }.
% 0.69/1.11 (1064) {G0,W7,D3,L1,V0,M1} { ! op( e5, e1 ) = op( e5, e3 ) }.
% 0.69/1.11 (1065) {G0,W7,D3,L1,V0,M1} { ! op( e5, e1 ) = op( e5, e4 ) }.
% 0.69/1.11 (1066) {G0,W7,D3,L1,V0,M1} { ! op( e5, e1 ) = op( e5, e5 ) }.
% 0.69/1.11 (1067) {G0,W7,D3,L1,V0,M1} { ! op( e5, e2 ) = op( e5, e3 ) }.
% 0.69/1.11 (1068) {G0,W7,D3,L1,V0,M1} { ! op( e5, e2 ) = op( e5, e4 ) }.
% 0.69/1.11 (1069) {G0,W7,D3,L1,V0,M1} { ! op( e5, e2 ) = op( e5, e5 ) }.
% 0.69/1.11 (1070) {G0,W7,D3,L1,V0,M1} { ! op( e5, e3 ) = op( e5, e4 ) }.
% 0.69/1.11 (1071) {G0,W7,D3,L1,V0,M1} { ! op( e5, e3 ) = op( e5, e5 ) }.
% 0.69/1.11 (1072) {G0,W7,D3,L1,V0,M1} { ! op( e5, e4 ) = op( e5, e5 ) }.
% 0.69/1.11 (1073) {G0,W3,D2,L1,V0,M1} { ! e0 = e1 }.
% 0.69/1.11 (1074) {G0,W3,D2,L1,V0,M1} { ! e0 = e2 }.
% 0.69/1.11 (1075) {G0,W3,D2,L1,V0,M1} { ! e0 = e3 }.
% 0.69/1.11 (1076) {G0,W3,D2,L1,V0,M1} { ! e0 = e4 }.
% 0.69/1.11 (1077) {G0,W3,D2,L1,V0,M1} { ! e0 = e5 }.
% 0.69/1.11 (1078) {G0,W3,D2,L1,V0,M1} { ! e1 = e2 }.
% 0.69/1.11 (1079) {G0,W3,D2,L1,V0,M1} { ! e1 = e3 }.
% 0.69/1.11 (1080) {G0,W3,D2,L1,V0,M1} { ! e1 = e4 }.
% 0.69/1.11 (1081) {G0,W3,D2,L1,V0,M1} { ! e1 = e5 }.
% 0.69/1.11 (1082) {G0,W3,D2,L1,V0,M1} { ! e2 = e3 }.
% 0.69/1.11 (1083) {G0,W3,D2,L1,V0,M1} { ! e2 = e4 }.
% 0.69/1.11 (1084) {G0,W3,D2,L1,V0,M1} { ! e2 = e5 }.
% 0.69/1.11 (1085) {G0,W3,D2,L1,V0,M1} { ! e3 = e4 }.
% 0.69/1.11 (1086) {G0,W3,D2,L1,V0,M1} { ! e3 = e5 }.
% 0.69/1.11 (1087) {G0,W3,D2,L1,V0,M1} { ! e4 = e5 }.
% 0.69/1.11 (1088) {G0,W13,D6,L1,V0,M1} { e0 = op( op( op( op( e4, e4 ), e4 ), e4 ),
% 0.69/1.11 op( e4, e4 ) ) }.
% 0.69/1.11 (1089) {G0,W7,D4,L1,V0,M1} { e1 = op( op( e4, e4 ), e4 ) }.
% 0.69/1.11 (1090) {G0,W9,D5,L1,V0,M1} { e2 = op( op( op( e4, e4 ), e4 ), e4 ) }.
% 0.69/1.11 (1091) {G0,W5,D3,L1,V0,M1} { e3 = op( e4, e4 ) }.
% 0.69/1.11 (1092) {G0,W11,D6,L1,V0,M1} { e5 = op( op( op( op( e4, e4 ), e4 ), e4 ),
% 0.69/1.11 e4 ) }.
% 0.87/1.29 (1093) {G0,W7,D3,L1,V0,M1} { op( e0, e0 ) = op( e0, e0 ) }.
% 0.87/1.29 (1094) {G0,W7,D3,L1,V0,M1} { op( e0, e1 ) = op( e1, e0 ) }.
% 0.87/1.29 (1095) {G0,W7,D3,L1,V0,M1} { op( e0, e2 ) = op( e2, e0 ) }.
% 0.87/1.29 (1096) {G0,W7,D3,L1,V0,M1} { op( e0, e3 ) = op( e3, e0 ) }.
% 0.87/1.29 (1097) {G0,W7,D3,L1,V0,M1} { op( e0, e4 ) = op( e4, e0 ) }.
% 0.87/1.29 (1098) {G0,W7,D3,L1,V0,M1} { op( e0, e5 ) = op( e5, e0 ) }.
% 0.87/1.29 (1099) {G0,W7,D3,L1,V0,M1} { op( e1, e0 ) = op( e0, e1 ) }.
% 0.87/1.29 (1100) {G0,W7,D3,L1,V0,M1} { op( e1, e1 ) = op( e1, e1 ) }.
% 0.87/1.29 (1101) {G0,W7,D3,L1,V0,M1} { op( e1, e2 ) = op( e2, e1 ) }.
% 0.87/1.29 (1102) {G0,W7,D3,L1,V0,M1} { op( e1, e3 ) = op( e3, e1 ) }.
% 0.87/1.29 (1103) {G0,W7,D3,L1,V0,M1} { op( e1, e4 ) = op( e4, e1 ) }.
% 0.87/1.29 (1104) {G0,W7,D3,L1,V0,M1} { op( e1, e5 ) = op( e5, e1 ) }.
% 0.87/1.29 (1105) {G0,W7,D3,L1,V0,M1} { op( e2, e0 ) = op( e0, e2 ) }.
% 0.87/1.29 (1106) {G0,W7,D3,L1,V0,M1} { op( e2, e1 ) = op( e1, e2 ) }.
% 0.87/1.29 (1107) {G0,W7,D3,L1,V0,M1} { op( e2, e2 ) = op( e2, e2 ) }.
% 0.87/1.29 (1108) {G0,W7,D3,L1,V0,M1} { op( e2, e3 ) = op( e3, e2 ) }.
% 0.87/1.29 (1109) {G0,W7,D3,L1,V0,M1} { op( e2, e4 ) = op( e4, e2 ) }.
% 0.87/1.29 (1110) {G0,W7,D3,L1,V0,M1} { op( e2, e5 ) = op( e5, e2 ) }.
% 0.87/1.29 (1111) {G0,W7,D3,L1,V0,M1} { op( e3, e0 ) = op( e0, e3 ) }.
% 0.87/1.29 (1112) {G0,W7,D3,L1,V0,M1} { op( e3, e1 ) = op( e1, e3 ) }.
% 0.87/1.29 (1113) {G0,W7,D3,L1,V0,M1} { op( e3, e2 ) = op( e2, e3 ) }.
% 0.87/1.29 (1114) {G0,W7,D3,L1,V0,M1} { op( e3, e3 ) = op( e3, e3 ) }.
% 0.87/1.29 (1115) {G0,W7,D3,L1,V0,M1} { op( e3, e4 ) = op( e4, e3 ) }.
% 0.87/1.29 (1116) {G0,W7,D3,L1,V0,M1} { op( e3, e5 ) = op( e5, e3 ) }.
% 0.87/1.29 (1117) {G0,W7,D3,L1,V0,M1} { op( e4, e0 ) = op( e0, e4 ) }.
% 0.87/1.29 (1118) {G0,W7,D3,L1,V0,M1} { op( e4, e1 ) = op( e1, e4 ) }.
% 0.87/1.29 (1119) {G0,W7,D3,L1,V0,M1} { op( e4, e2 ) = op( e2, e4 ) }.
% 0.87/1.29 (1120) {G0,W7,D3,L1,V0,M1} { op( e4, e3 ) = op( e3, e4 ) }.
% 0.87/1.29 (1121) {G0,W7,D3,L1,V0,M1} { op( e4, e4 ) = op( e4, e4 ) }.
% 0.87/1.29 (1122) {G0,W7,D3,L1,V0,M1} { op( e4, e5 ) = op( e5, e4 ) }.
% 0.87/1.29 (1123) {G0,W7,D3,L1,V0,M1} { op( e5, e0 ) = op( e0, e5 ) }.
% 0.87/1.29 (1124) {G0,W7,D3,L1,V0,M1} { op( e5, e1 ) = op( e1, e5 ) }.
% 0.87/1.29 (1125) {G0,W7,D3,L1,V0,M1} { op( e5, e2 ) = op( e2, e5 ) }.
% 0.87/1.29 (1126) {G0,W7,D3,L1,V0,M1} { op( e5, e3 ) = op( e3, e5 ) }.
% 0.87/1.29 (1127) {G0,W7,D3,L1,V0,M1} { op( e5, e4 ) = op( e4, e5 ) }.
% 0.87/1.29 (1128) {G0,W7,D3,L1,V0,M1} { op( e5, e5 ) = op( e5, e5 ) }.
% 0.87/1.29 (1129) {G0,W252,D3,L36,V0,M36} { ! op( e0, e0 ) = op( e0, e0 ), ! op( e0,
% 0.87/1.29 e1 ) = op( e1, e0 ), ! op( e0, e2 ) = op( e2, e0 ), ! op( e0, e3 ) = op(
% 0.87/1.29 e3, e0 ), ! op( e0, e4 ) = op( e4, e0 ), ! op( e0, e5 ) = op( e5, e0 ), !
% 0.87/1.29 op( e1, e0 ) = op( e0, e1 ), ! op( e1, e1 ) = op( e1, e1 ), ! op( e1, e2
% 0.87/1.29 ) = op( e2, e1 ), ! op( e1, e3 ) = op( e3, e1 ), ! op( e1, e4 ) = op( e4
% 0.87/1.29 , e1 ), ! op( e1, e5 ) = op( e5, e1 ), ! op( e2, e0 ) = op( e0, e2 ), !
% 0.87/1.29 op( e2, e1 ) = op( e1, e2 ), ! op( e2, e2 ) = op( e2, e2 ), ! op( e2, e3
% 0.87/1.29 ) = op( e3, e2 ), ! op( e2, e4 ) = op( e4, e2 ), ! op( e2, e5 ) = op( e5
% 0.87/1.29 , e2 ), ! op( e3, e0 ) = op( e0, e3 ), ! op( e3, e1 ) = op( e1, e3 ), !
% 0.87/1.29 op( e3, e2 ) = op( e2, e3 ), ! op( e3, e3 ) = op( e3, e3 ), ! op( e3, e4
% 0.87/1.29 ) = op( e4, e3 ), ! op( e3, e5 ) = op( e5, e3 ), ! op( e4, e0 ) = op( e0
% 0.87/1.29 , e4 ), ! op( e4, e1 ) = op( e1, e4 ), ! op( e4, e2 ) = op( e2, e4 ), !
% 0.87/1.29 op( e4, e3 ) = op( e3, e4 ), ! op( e4, e4 ) = op( e4, e4 ), ! op( e4, e5
% 0.87/1.29 ) = op( e5, e4 ), ! op( e5, e0 ) = op( e0, e5 ), ! op( e5, e1 ) = op( e1
% 0.87/1.29 , e5 ), ! op( e5, e2 ) = op( e2, e5 ), ! op( e5, e3 ) = op( e3, e5 ), !
% 0.87/1.29 op( e5, e4 ) = op( e4, e5 ), ! op( e5, e5 ) = op( e5, e5 ) }.
% 0.87/1.29
% 0.87/1.29
% 0.87/1.29 Total Proof:
% 0.87/1.29
% 0.87/1.29 *** allocated 75937 integers for clauses
% 0.87/1.29 *** allocated 50625 integers for termspace/termends
% 0.87/1.29 *** allocated 75937 integers for termspace/termends
% 0.87/1.29 *** allocated 113905 integers for clauses
% 0.87/1.29 *** allocated 113905 integers for termspace/termends
% 0.87/1.29 *** allocated 170857 integers for clauses
% 0.87/1.29 eqswap: (4405) {G0,W7,D4,L1,V0,M1} { op( op( e4, e4 ), e4 ) = e1 }.
% 0.87/1.29 parent0[0]: (1089) {G0,W7,D4,L1,V0,M1} { e1 = op( op( e4, e4 ), e4 ) }.
% 0.87/1.29 substitution0:
% 0.87/1.29 end
% 0.87/1.29
% 0.87/1.29 subsumption: (531) {G0,W7,D4,L1,V0,M1} I { op( op( e4, e4 ), e4 ) ==> e1
% 0.87/1.29 }.
% 0.87/1.29 parent0: (4405) {G0,W7,D4,L1,V0,M1} { op( op( e4, e4 ), e4 ) = e1 }.
% 0.87/1.29 substitution0:
% 0.87/1.29 end
% 0.87/1.29 permutation0:
% 0.87/1.29 0 ==> 0
% 0.87/1.29 end
% 0.87/1.29
% 0.87/1.29 *** allocated 170857 integers for termspace/termends
% 4.66/5.09 *** allocated 256285 integers for clauses
% 4.66/5.09 *** allocated 256285 integers for termspace/termends
% 4.66/5.09 paramod: (8232) {G1,W5,D3,L1,V0,M1} { e2 = op( e1, e4 ) }.
% 4.66/5.09 parent0[0]: (531) {G0,W7,D4,L1,V0,M1} I { op( op( e4, e4 ), e4 ) ==> e1 }.
% 4.66/5.09 parent1[0; 3]: (1090) {G0,W9,D5,L1,V0,M1} { e2 = op( op( op( e4, e4 ), e4
% 4.66/5.09 ), e4 ) }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09 substitution1:
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 eqswap: (8233) {G1,W5,D3,L1,V0,M1} { op( e1, e4 ) = e2 }.
% 4.66/5.09 parent0[0]: (8232) {G1,W5,D3,L1,V0,M1} { e2 = op( e1, e4 ) }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 subsumption: (532) {G1,W5,D3,L1,V0,M1} I;d(531) { op( e1, e4 ) ==> e2 }.
% 4.66/5.09 parent0: (8233) {G1,W5,D3,L1,V0,M1} { op( e1, e4 ) = e2 }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09 permutation0:
% 4.66/5.09 0 ==> 0
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 *** allocated 384427 integers for clauses
% 4.66/5.09 *** allocated 384427 integers for termspace/termends
% 4.66/5.09 paramod: (12609) {G1,W7,D4,L1,V0,M1} { e5 = op( op( e1, e4 ), e4 ) }.
% 4.66/5.09 parent0[0]: (531) {G0,W7,D4,L1,V0,M1} I { op( op( e4, e4 ), e4 ) ==> e1 }.
% 4.66/5.09 parent1[0; 4]: (1092) {G0,W11,D6,L1,V0,M1} { e5 = op( op( op( op( e4, e4 )
% 4.66/5.09 , e4 ), e4 ), e4 ) }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09 substitution1:
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 paramod: (12610) {G2,W5,D3,L1,V0,M1} { e5 = op( e2, e4 ) }.
% 4.66/5.09 parent0[0]: (532) {G1,W5,D3,L1,V0,M1} I;d(531) { op( e1, e4 ) ==> e2 }.
% 4.66/5.09 parent1[0; 3]: (12609) {G1,W7,D4,L1,V0,M1} { e5 = op( op( e1, e4 ), e4 )
% 4.66/5.09 }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09 substitution1:
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 eqswap: (12611) {G2,W5,D3,L1,V0,M1} { op( e2, e4 ) = e5 }.
% 4.66/5.09 parent0[0]: (12610) {G2,W5,D3,L1,V0,M1} { e5 = op( e2, e4 ) }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 subsumption: (534) {G2,W5,D3,L1,V0,M1} I;d(531);d(532) { op( e2, e4 ) ==>
% 4.66/5.09 e5 }.
% 4.66/5.09 parent0: (12611) {G2,W5,D3,L1,V0,M1} { op( e2, e4 ) = e5 }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09 permutation0:
% 4.66/5.09 0 ==> 0
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 *** allocated 576640 integers for clauses
% 4.66/5.09 subsumption: (535) {G0,W7,D3,L1,V0,M1} I { op( e0, e1 ) ==> op( e1, e0 )
% 4.66/5.09 }.
% 4.66/5.09 parent0: (1094) {G0,W7,D3,L1,V0,M1} { op( e0, e1 ) = op( e1, e0 ) }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09 permutation0:
% 4.66/5.09 0 ==> 0
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 *** allocated 576640 integers for termspace/termends
% 4.66/5.09 subsumption: (536) {G0,W7,D3,L1,V0,M1} I { op( e0, e2 ) ==> op( e2, e0 )
% 4.66/5.09 }.
% 4.66/5.09 parent0: (1095) {G0,W7,D3,L1,V0,M1} { op( e0, e2 ) = op( e2, e0 ) }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09 permutation0:
% 4.66/5.09 0 ==> 0
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 subsumption: (537) {G0,W7,D3,L1,V0,M1} I { op( e0, e3 ) ==> op( e3, e0 )
% 4.66/5.09 }.
% 4.66/5.09 parent0: (1096) {G0,W7,D3,L1,V0,M1} { op( e0, e3 ) = op( e3, e0 ) }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09 permutation0:
% 4.66/5.09 0 ==> 0
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 *** allocated 864960 integers for clauses
% 4.66/5.09 *** allocated 864960 integers for termspace/termends
% 4.66/5.09 subsumption: (538) {G0,W7,D3,L1,V0,M1} I { op( e0, e4 ) ==> op( e4, e0 )
% 4.66/5.09 }.
% 4.66/5.09 parent0: (1097) {G0,W7,D3,L1,V0,M1} { op( e0, e4 ) = op( e4, e0 ) }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09 permutation0:
% 4.66/5.09 0 ==> 0
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 subsumption: (539) {G0,W7,D3,L1,V0,M1} I { op( e0, e5 ) ==> op( e5, e0 )
% 4.66/5.09 }.
% 4.66/5.09 parent0: (1098) {G0,W7,D3,L1,V0,M1} { op( e0, e5 ) = op( e5, e0 ) }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09 permutation0:
% 4.66/5.09 0 ==> 0
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 subsumption: (540) {G0,W7,D3,L1,V0,M1} I { op( e1, e2 ) ==> op( e2, e1 )
% 4.66/5.09 }.
% 4.66/5.09 parent0: (1101) {G0,W7,D3,L1,V0,M1} { op( e1, e2 ) = op( e2, e1 ) }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09 permutation0:
% 4.66/5.09 0 ==> 0
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 *** allocated 1297440 integers for termspace/termends
% 4.66/5.09 *** allocated 1297440 integers for clauses
% 4.66/5.09 subsumption: (541) {G0,W7,D3,L1,V0,M1} I { op( e1, e3 ) ==> op( e3, e1 )
% 4.66/5.09 }.
% 4.66/5.09 parent0: (1102) {G0,W7,D3,L1,V0,M1} { op( e1, e3 ) = op( e3, e1 ) }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09 permutation0:
% 4.66/5.09 0 ==> 0
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 paramod: (108931) {G1,W5,D3,L1,V0,M1} { e2 = op( e4, e1 ) }.
% 4.66/5.09 parent0[0]: (532) {G1,W5,D3,L1,V0,M1} I;d(531) { op( e1, e4 ) ==> e2 }.
% 4.66/5.09 parent1[0; 1]: (1103) {G0,W7,D3,L1,V0,M1} { op( e1, e4 ) = op( e4, e1 )
% 4.66/5.09 }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09 substitution1:
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 eqswap: (108932) {G1,W5,D3,L1,V0,M1} { op( e4, e1 ) = e2 }.
% 4.66/5.09 parent0[0]: (108931) {G1,W5,D3,L1,V0,M1} { e2 = op( e4, e1 ) }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 subsumption: (542) {G2,W5,D3,L1,V0,M1} I;d(532) { op( e4, e1 ) ==> e2 }.
% 4.66/5.09 parent0: (108932) {G1,W5,D3,L1,V0,M1} { op( e4, e1 ) = e2 }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09 permutation0:
% 4.66/5.09 0 ==> 0
% 4.66/5.09 end
% 4.66/5.09
% 4.66/5.09 subsumption: (543) {G0,W7,D3,L1,V0,M1} I { op( e1, e5 ) ==> op( e5, e1 )
% 4.66/5.09 }.
% 4.66/5.09 parent0: (1104) {G0,W7,D3,L1,V0,M1} { op( e1, e5 ) = op( e5, e1 ) }.
% 4.66/5.09 substitution0:
% 4.66/5.09 end
% 4.66/5.09 permutation0:
% 8.03/8.43 0 ==> 0
% 8.03/8.43 end
% 8.03/8.43
% 8.03/8.43 subsumption: (544) {G0,W7,D3,L1,V0,M1} I { op( e2, e3 ) ==> op( e3, e2 )
% 8.03/8.43 }.
% 8.03/8.43 parent0: (1108) {G0,W7,D3,L1,V0,M1} { op( e2, e3 ) = op( e3, e2 ) }.
% 8.03/8.43 substitution0:
% 8.03/8.43 end
% 8.03/8.43 permutation0:
% 8.03/8.43 0 ==> 0
% 8.03/8.43 end
% 8.03/8.43
% 8.03/8.43 paramod: (189405) {G1,W5,D3,L1,V0,M1} { e5 = op( e4, e2 ) }.
% 8.03/8.43 parent0[0]: (534) {G2,W5,D3,L1,V0,M1} I;d(531);d(532) { op( e2, e4 ) ==> e5
% 8.03/8.43 }.
% 8.03/8.43 parent1[0; 1]: (1109) {G0,W7,D3,L1,V0,M1} { op( e2, e4 ) = op( e4, e2 )
% 8.03/8.43 }.
% 8.03/8.43 substitution0:
% 8.03/8.43 end
% 8.03/8.43 substitution1:
% 8.03/8.43 end
% 8.03/8.43
% 8.03/8.43 eqswap: (189406) {G1,W5,D3,L1,V0,M1} { op( e4, e2 ) = e5 }.
% 8.03/8.43 parent0[0]: (189405) {G1,W5,D3,L1,V0,M1} { e5 = op( e4, e2 ) }.
% 8.03/8.43 substitution0:
% 8.03/8.43 end
% 8.03/8.43
% 8.03/8.43 subsumption: (545) {G3,W5,D3,L1,V0,M1} I;d(534) { op( e4, e2 ) ==> e5 }.
% 8.03/8.43 parent0: (189406) {G1,W5,D3,L1,V0,M1} { op( e4, e2 ) = e5 }.
% 8.03/8.43 substitution0:
% 8.03/8.43 end
% 8.03/8.43 permutation0:
% 8.03/8.43 0 ==> 0
% 8.03/8.43 end
% 8.03/8.43
% 8.03/8.43 subsumption: (546) {G0,W7,D3,L1,V0,M1} I { op( e2, e5 ) ==> op( e5, e2 )
% 8.03/8.43 }.
% 8.03/8.43 parent0: (1110) {G0,W7,D3,L1,V0,M1} { op( e2, e5 ) = op( e5, e2 ) }.
% 8.03/8.43 substitution0:
% 8.03/8.43 end
% 8.03/8.43 permutation0:
% 8.03/8.43 0 ==> 0
% 8.03/8.43 end
% 8.03/8.43
% 8.03/8.43 *** allocated 1946160 integers for termspace/termends
% 8.03/8.43 *** allocated 1946160 integers for clauses
% 8.03/8.43 subsumption: (547) {G0,W7,D3,L1,V0,M1} I { op( e3, e4 ) ==> op( e4, e3 )
% 8.03/8.43 }.
% 8.03/8.43 parent0: (1115) {G0,W7,D3,L1,V0,M1} { op( e3, e4 ) = op( e4, e3 ) }.
% 8.03/8.43 substitution0:
% 8.03/8.43 end
% 8.03/8.43 permutation0:
% 8.03/8.43 0 ==> 0
% 8.03/8.43 end
% 8.03/8.43
% 8.03/8.43 subsumption: (548) {G0,W7,D3,L1,V0,M1} I { op( e3, e5 ) ==> op( e5, e3 )
% 8.03/8.43 }.
% 8.03/8.43 parent0: (1116) {G0,W7,D3,L1,V0,M1} { op( e3, e5 ) = op( e5, e3 ) }.
% 8.03/8.43 substitution0:
% 8.03/8.43 end
% 8.03/8.43 permutation0:
% 8.03/8.43 0 ==> 0
% 8.03/8.43 end
% 8.03/8.43
% 8.03/8.43 subsumption: (549) {G0,W7,D3,L1,V0,M1} I { op( e4, e5 ) ==> op( e5, e4 )
% 8.03/8.43 }.
% 8.03/8.43 parent0: (1122) {G0,W7,D3,L1,V0,M1} { op( e4, e5 ) = op( e5, e4 ) }.
% 8.03/8.43 substitution0:
% 8.03/8.43 end
% 8.03/8.43 permutation0:
% 8.03/8.43 0 ==> 0
% 8.03/8.43 end
% 8.03/8.43
% 8.03/8.43 *** allocated 2919240 integers for clauses
% 8.03/8.43
% 8.03/8.43 ==> (550) {G4,W0,D0,L0,V0,M0} I;q;q;q;q;q;q;d(535);d(536);d(537);d(538);d(
% 8.03/8.43 539);d(535);d(540);d(541);d(532);d(543);d(536);d(540);d(544);d(534);d(546
% 8.03/8.43 );d(537);d(541);d(544);d(547);d(548);d(538);d(542);d(545);d(547);d(549);d
% 8.03/8.43 (539);d(543);d(546);d(548);d(549);d(542);d(545);d(532);d(534);q;q;q;q;q;q
% 8.03/8.43 ;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q;q { }.
% 8.03/8.43
% 8.03/8.43
% 8.03/8.43
% 8.03/8.43 !!! Internal Problem: OH, OH, COULD NOT DERIVE GOAL !!!
% 8.03/8.43
% 8.03/8.43 Bliksem ended
%------------------------------------------------------------------------------