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