%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : ALG172+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n019.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:47 EDT 2022
% Result : Theorem 0.81s 1.36s
% Output : Refutation 0.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ALG172+1 : TPTP v8.1.0. Released v2.7.0.
% 0.07/0.13 % Command : bliksem %s
% 0.14/0.34 % Computer : n019.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % DateTime : Wed Jun 8 12:05:40 EDT 2022
% 0.14/0.34 % CPUTime :
% 0.81/1.22 *** allocated 10000 integers for termspace/termends
% 0.81/1.22 *** allocated 10000 integers for clauses
% 0.81/1.22 *** allocated 10000 integers for justifications
% 0.81/1.22 Bliksem 1.12
% 0.81/1.22
% 0.81/1.22
% 0.81/1.22 Automatic Strategy Selection
% 0.81/1.22
% 0.81/1.22 *** allocated 15000 integers for termspace/termends
% 0.81/1.22
% 0.81/1.22 Clauses:
% 0.81/1.22
% 0.81/1.22 { op( e0, e0 ) = e0, op( e0, e0 ) = e1, op( e0, e0 ) = e2, op( e0, e0 ) =
% 0.81/1.22 e3, op( e0, e0 ) = e4 }.
% 0.81/1.22 { op( e0, e1 ) = e0, op( e0, e1 ) = e1, op( e0, e1 ) = e2, op( e0, e1 ) =
% 0.81/1.22 e3, op( e0, e1 ) = e4 }.
% 0.81/1.22 { op( e0, e2 ) = e0, op( e0, e2 ) = e1, op( e0, e2 ) = e2, op( e0, e2 ) =
% 0.81/1.22 e3, op( e0, e2 ) = e4 }.
% 0.81/1.22 { op( e0, e3 ) = e0, op( e0, e3 ) = e1, op( e0, e3 ) = e2, op( e0, e3 ) =
% 0.81/1.22 e3, op( e0, e3 ) = e4 }.
% 0.81/1.22 { op( e0, e4 ) = e0, op( e0, e4 ) = e1, op( e0, e4 ) = e2, op( e0, e4 ) =
% 0.81/1.22 e3, op( e0, e4 ) = e4 }.
% 0.81/1.22 { op( e1, e0 ) = e0, op( e1, e0 ) = e1, op( e1, e0 ) = e2, op( e1, e0 ) =
% 0.81/1.22 e3, op( e1, e0 ) = e4 }.
% 0.81/1.22 { op( e1, e1 ) = e0, op( e1, e1 ) = e1, op( e1, e1 ) = e2, op( e1, e1 ) =
% 0.81/1.22 e3, op( e1, e1 ) = e4 }.
% 0.81/1.22 { op( e1, e2 ) = e0, op( e1, e2 ) = e1, op( e1, e2 ) = e2, op( e1, e2 ) =
% 0.81/1.22 e3, op( e1, e2 ) = e4 }.
% 0.81/1.22 { op( e1, e3 ) = e0, op( e1, e3 ) = e1, op( e1, e3 ) = e2, op( e1, e3 ) =
% 0.81/1.22 e3, op( e1, e3 ) = e4 }.
% 0.81/1.22 { op( e1, e4 ) = e0, op( e1, e4 ) = e1, op( e1, e4 ) = e2, op( e1, e4 ) =
% 0.81/1.22 e3, op( e1, e4 ) = e4 }.
% 0.81/1.22 { op( e2, e0 ) = e0, op( e2, e0 ) = e1, op( e2, e0 ) = e2, op( e2, e0 ) =
% 0.81/1.22 e3, op( e2, e0 ) = e4 }.
% 0.81/1.22 { op( e2, e1 ) = e0, op( e2, e1 ) = e1, op( e2, e1 ) = e2, op( e2, e1 ) =
% 0.81/1.22 e3, op( e2, e1 ) = e4 }.
% 0.81/1.22 { op( e2, e2 ) = e0, op( e2, e2 ) = e1, op( e2, e2 ) = e2, op( e2, e2 ) =
% 0.81/1.22 e3, op( e2, e2 ) = e4 }.
% 0.81/1.22 { op( e2, e3 ) = e0, op( e2, e3 ) = e1, op( e2, e3 ) = e2, op( e2, e3 ) =
% 0.81/1.22 e3, op( e2, e3 ) = e4 }.
% 0.81/1.22 { op( e2, e4 ) = e0, op( e2, e4 ) = e1, op( e2, e4 ) = e2, op( e2, e4 ) =
% 0.81/1.22 e3, op( e2, e4 ) = e4 }.
% 0.81/1.22 { op( e3, e0 ) = e0, op( e3, e0 ) = e1, op( e3, e0 ) = e2, op( e3, e0 ) =
% 0.81/1.22 e3, op( e3, e0 ) = e4 }.
% 0.81/1.22 { op( e3, e1 ) = e0, op( e3, e1 ) = e1, op( e3, e1 ) = e2, op( e3, e1 ) =
% 0.81/1.22 e3, op( e3, e1 ) = e4 }.
% 0.81/1.22 { op( e3, e2 ) = e0, op( e3, e2 ) = e1, op( e3, e2 ) = e2, op( e3, e2 ) =
% 0.81/1.22 e3, op( e3, e2 ) = e4 }.
% 0.81/1.22 { op( e3, e3 ) = e0, op( e3, e3 ) = e1, op( e3, e3 ) = e2, op( e3, e3 ) =
% 0.81/1.22 e3, op( e3, e3 ) = e4 }.
% 0.81/1.22 { op( e3, e4 ) = e0, op( e3, e4 ) = e1, op( e3, e4 ) = e2, op( e3, e4 ) =
% 0.81/1.22 e3, op( e3, e4 ) = e4 }.
% 0.81/1.22 { op( e4, e0 ) = e0, op( e4, e0 ) = e1, op( e4, e0 ) = e2, op( e4, e0 ) =
% 0.81/1.22 e3, op( e4, e0 ) = e4 }.
% 0.81/1.22 { op( e4, e1 ) = e0, op( e4, e1 ) = e1, op( e4, e1 ) = e2, op( e4, e1 ) =
% 0.81/1.22 e3, op( e4, e1 ) = e4 }.
% 0.81/1.22 { op( e4, e2 ) = e0, op( e4, e2 ) = e1, op( e4, e2 ) = e2, op( e4, e2 ) =
% 0.81/1.22 e3, op( e4, e2 ) = e4 }.
% 0.81/1.22 { op( e4, e3 ) = e0, op( e4, e3 ) = e1, op( e4, e3 ) = e2, op( e4, e3 ) =
% 0.81/1.22 e3, op( e4, e3 ) = e4 }.
% 0.81/1.22 { op( e4, e4 ) = e0, op( e4, e4 ) = e1, op( e4, e4 ) = e2, op( e4, e4 ) =
% 0.81/1.22 e3, op( e4, e4 ) = e4 }.
% 0.81/1.22 { op( e0, e0 ) = e0, op( e0, e1 ) = e0, op( e0, e2 ) = e0, op( e0, e3 ) =
% 0.81/1.22 e0, op( e0, e4 ) = e0 }.
% 0.81/1.22 { op( e0, e0 ) = e0, op( e1, e0 ) = e0, op( e2, e0 ) = e0, op( e3, e0 ) =
% 0.81/1.22 e0, op( e4, e0 ) = e0 }.
% 0.81/1.22 { op( e0, e0 ) = e1, op( e0, e1 ) = e1, op( e0, e2 ) = e1, op( e0, e3 ) =
% 0.81/1.22 e1, op( e0, e4 ) = e1 }.
% 0.81/1.22 { op( e0, e0 ) = e1, op( e1, e0 ) = e1, op( e2, e0 ) = e1, op( e3, e0 ) =
% 0.81/1.22 e1, op( e4, e0 ) = e1 }.
% 0.81/1.22 { op( e0, e0 ) = e2, op( e0, e1 ) = e2, op( e0, e2 ) = e2, op( e0, e3 ) =
% 0.81/1.22 e2, op( e0, e4 ) = e2 }.
% 0.81/1.22 { op( e0, e0 ) = e2, op( e1, e0 ) = e2, op( e2, e0 ) = e2, op( e3, e0 ) =
% 0.81/1.22 e2, op( e4, e0 ) = e2 }.
% 0.81/1.22 { op( e0, e0 ) = e3, op( e0, e1 ) = e3, op( e0, e2 ) = e3, op( e0, e3 ) =
% 0.81/1.22 e3, op( e0, e4 ) = e3 }.
% 0.81/1.22 { op( e0, e0 ) = e3, op( e1, e0 ) = e3, op( e2, e0 ) = e3, op( e3, e0 ) =
% 0.81/1.22 e3, op( e4, e0 ) = e3 }.
% 0.81/1.22 { op( e0, e0 ) = e4, op( e0, e1 ) = e4, op( e0, e2 ) = e4, op( e0, e3 ) =
% 0.81/1.22 e4, op( e0, e4 ) = e4 }.
% 0.81/1.22 { op( e0, e0 ) = e4, op( e1, e0 ) = e4, op( e2, e0 ) = e4, op( e3, e0 ) =
% 0.81/1.22 e4, op( e4, e0 ) = e4 }.
% 0.81/1.22 { op( e1, e0 ) = e0, op( e1, e1 ) = e0, op( e1, e2 ) = e0, op( e1, e3 ) =
% 0.81/1.22 e0, op( e1, e4 ) = e0 }.
% 0.81/1.22 { op( e0, e1 ) = e0, op( e1, e1 ) = e0, op( e2, e1 ) = e0, op( e3, e1 ) =
% 0.81/1.22 e0, op( e4, e1 ) = e0 }.
% 0.81/1.22 { op( e1, e0 ) = e1, op( e1, e1 ) = e1, op( e1, e2 ) = e1, op( e1, e3 ) =
% 0.81/1.22 e1, op( e1, e4 ) = e1 }.
% 0.81/1.22 { op( e0, e1 ) = e1, op( e1, e1 ) = e1, op( e2, e1 ) = e1, op( e3, e1 ) =
% 0.81/1.22 e1, op( e4, e1 ) = e1 }.
% 0.81/1.22 { op( e1, e0 ) = e2, op( e1, e1 ) = e2, op( e1, e2 ) = e2, op( e1, e3 ) =
% 0.81/1.22 e2, op( e1, e4 ) = e2 }.
% 0.81/1.22 { op( e0, e1 ) = e2, op( e1, e1 ) = e2, op( e2, e1 ) = e2, op( e3, e1 ) =
% 0.81/1.22 e2, op( e4, e1 ) = e2 }.
% 0.81/1.22 { op( e1, e0 ) = e3, op( e1, e1 ) = e3, op( e1, e2 ) = e3, op( e1, e3 ) =
% 0.81/1.22 e3, op( e1, e4 ) = e3 }.
% 0.81/1.22 { op( e0, e1 ) = e3, op( e1, e1 ) = e3, op( e2, e1 ) = e3, op( e3, e1 ) =
% 0.81/1.22 e3, op( e4, e1 ) = e3 }.
% 0.81/1.22 { op( e1, e0 ) = e4, op( e1, e1 ) = e4, op( e1, e2 ) = e4, op( e1, e3 ) =
% 0.81/1.22 e4, op( e1, e4 ) = e4 }.
% 0.81/1.22 { op( e0, e1 ) = e4, op( e1, e1 ) = e4, op( e2, e1 ) = e4, op( e3, e1 ) =
% 0.81/1.22 e4, op( e4, e1 ) = e4 }.
% 0.81/1.22 { op( e2, e0 ) = e0, op( e2, e1 ) = e0, op( e2, e2 ) = e0, op( e2, e3 ) =
% 0.81/1.22 e0, op( e2, e4 ) = e0 }.
% 0.81/1.22 { op( e0, e2 ) = e0, op( e1, e2 ) = e0, op( e2, e2 ) = e0, op( e3, e2 ) =
% 0.81/1.22 e0, op( e4, e2 ) = e0 }.
% 0.81/1.22 { op( e2, e0 ) = e1, op( e2, e1 ) = e1, op( e2, e2 ) = e1, op( e2, e3 ) =
% 0.81/1.22 e1, op( e2, e4 ) = e1 }.
% 0.81/1.22 { op( e0, e2 ) = e1, op( e1, e2 ) = e1, op( e2, e2 ) = e1, op( e3, e2 ) =
% 0.81/1.22 e1, op( e4, e2 ) = e1 }.
% 0.81/1.22 { op( e2, e0 ) = e2, op( e2, e1 ) = e2, op( e2, e2 ) = e2, op( e2, e3 ) =
% 0.81/1.22 e2, op( e2, e4 ) = e2 }.
% 0.81/1.22 { op( e0, e2 ) = e2, op( e1, e2 ) = e2, op( e2, e2 ) = e2, op( e3, e2 ) =
% 0.81/1.22 e2, op( e4, e2 ) = e2 }.
% 0.81/1.22 { op( e2, e0 ) = e3, op( e2, e1 ) = e3, op( e2, e2 ) = e3, op( e2, e3 ) =
% 0.81/1.22 e3, op( e2, e4 ) = e3 }.
% 0.81/1.22 { op( e0, e2 ) = e3, op( e1, e2 ) = e3, op( e2, e2 ) = e3, op( e3, e2 ) =
% 0.81/1.22 e3, op( e4, e2 ) = e3 }.
% 0.81/1.22 { op( e2, e0 ) = e4, op( e2, e1 ) = e4, op( e2, e2 ) = e4, op( e2, e3 ) =
% 0.81/1.22 e4, op( e2, e4 ) = e4 }.
% 0.81/1.22 { op( e0, e2 ) = e4, op( e1, e2 ) = e4, op( e2, e2 ) = e4, op( e3, e2 ) =
% 0.81/1.22 e4, op( e4, e2 ) = e4 }.
% 0.81/1.22 { op( e3, e0 ) = e0, op( e3, e1 ) = e0, op( e3, e2 ) = e0, op( e3, e3 ) =
% 0.81/1.22 e0, op( e3, e4 ) = e0 }.
% 0.81/1.22 { op( e0, e3 ) = e0, op( e1, e3 ) = e0, op( e2, e3 ) = e0, op( e3, e3 ) =
% 0.81/1.22 e0, op( e4, e3 ) = e0 }.
% 0.81/1.22 { op( e3, e0 ) = e1, op( e3, e1 ) = e1, op( e3, e2 ) = e1, op( e3, e3 ) =
% 0.81/1.22 e1, op( e3, e4 ) = e1 }.
% 0.81/1.22 { op( e0, e3 ) = e1, op( e1, e3 ) = e1, op( e2, e3 ) = e1, op( e3, e3 ) =
% 0.81/1.22 e1, op( e4, e3 ) = e1 }.
% 0.81/1.22 { op( e3, e0 ) = e2, op( e3, e1 ) = e2, op( e3, e2 ) = e2, op( e3, e3 ) =
% 0.81/1.22 e2, op( e3, e4 ) = e2 }.
% 0.81/1.22 { op( e0, e3 ) = e2, op( e1, e3 ) = e2, op( e2, e3 ) = e2, op( e3, e3 ) =
% 0.81/1.22 e2, op( e4, e3 ) = e2 }.
% 0.81/1.22 { op( e3, e0 ) = e3, op( e3, e1 ) = e3, op( e3, e2 ) = e3, op( e3, e3 ) =
% 0.81/1.22 e3, op( e3, e4 ) = e3 }.
% 0.81/1.22 { op( e0, e3 ) = e3, op( e1, e3 ) = e3, op( e2, e3 ) = e3, op( e3, e3 ) =
% 0.81/1.22 e3, op( e4, e3 ) = e3 }.
% 0.81/1.22 { op( e3, e0 ) = e4, op( e3, e1 ) = e4, op( e3, e2 ) = e4, op( e3, e3 ) =
% 0.81/1.22 e4, op( e3, e4 ) = e4 }.
% 0.81/1.22 { op( e0, e3 ) = e4, op( e1, e3 ) = e4, op( e2, e3 ) = e4, op( e3, e3 ) =
% 0.81/1.22 e4, op( e4, e3 ) = e4 }.
% 0.81/1.22 { op( e4, e0 ) = e0, op( e4, e1 ) = e0, op( e4, e2 ) = e0, op( e4, e3 ) =
% 0.81/1.22 e0, op( e4, e4 ) = e0 }.
% 0.81/1.22 { op( e0, e4 ) = e0, op( e1, e4 ) = e0, op( e2, e4 ) = e0, op( e3, e4 ) =
% 0.81/1.22 e0, op( e4, e4 ) = e0 }.
% 0.81/1.22 { op( e4, e0 ) = e1, op( e4, e1 ) = e1, op( e4, e2 ) = e1, op( e4, e3 ) =
% 0.81/1.22 e1, op( e4, e4 ) = e1 }.
% 0.81/1.22 { op( e0, e4 ) = e1, op( e1, e4 ) = e1, op( e2, e4 ) = e1, op( e3, e4 ) =
% 0.81/1.22 e1, op( e4, e4 ) = e1 }.
% 0.81/1.22 { op( e4, e0 ) = e2, op( e4, e1 ) = e2, op( e4, e2 ) = e2, op( e4, e3 ) =
% 0.81/1.22 e2, op( e4, e4 ) = e2 }.
% 0.81/1.22 { op( e0, e4 ) = e2, op( e1, e4 ) = e2, op( e2, e4 ) = e2, op( e3, e4 ) =
% 0.81/1.22 e2, op( e4, e4 ) = e2 }.
% 0.81/1.22 { op( e4, e0 ) = e3, op( e4, e1 ) = e3, op( e4, e2 ) = e3, op( e4, e3 ) =
% 0.81/1.22 e3, op( e4, e4 ) = e3 }.
% 0.81/1.22 { op( e0, e4 ) = e3, op( e1, e4 ) = e3, op( e2, e4 ) = e3, op( e3, e4 ) =
% 0.81/1.22 e3, op( e4, e4 ) = e3 }.
% 0.81/1.22 { op( e4, e0 ) = e4, op( e4, e1 ) = e4, op( e4, e2 ) = e4, op( e4, e3 ) =
% 0.81/1.22 e4, op( e4, e4 ) = e4 }.
% 0.81/1.22 { op( e0, e4 ) = e4, op( e1, e4 ) = e4, op( e2, e4 ) = e4, op( e3, e4 ) =
% 0.81/1.22 e4, op( e4, e4 ) = e4 }.
% 0.81/1.22 { op( op( e0, e0 ), op( e0, e0 ) ) = e0 }.
% 0.81/1.22 { op( op( e1, e0 ), op( e0, e1 ) ) = e0 }.
% 0.81/1.22 { op( op( e2, e0 ), op( e0, e2 ) ) = e0 }.
% 0.81/1.22 { op( op( e3, e0 ), op( e0, e3 ) ) = e0 }.
% 0.81/1.22 { op( op( e4, e0 ), op( e0, e4 ) ) = e0 }.
% 0.81/1.22 { op( op( e0, e1 ), op( e1, e0 ) ) = e1 }.
% 0.81/1.22 { op( op( e1, e1 ), op( e1, e1 ) ) = e1 }.
% 0.81/1.22 { op( op( e2, e1 ), op( e1, e2 ) ) = e1 }.
% 0.81/1.22 { op( op( e3, e1 ), op( e1, e3 ) ) = e1 }.
% 0.81/1.22 { op( op( e4, e1 ), op( e1, e4 ) ) = e1 }.
% 0.81/1.22 { op( op( e0, e2 ), op( e2, e0 ) ) = e2 }.
% 0.81/1.22 { op( op( e1, e2 ), op( e2, e1 ) ) = e2 }.
% 0.81/1.22 { op( op( e2, e2 ), op( e2, e2 ) ) = e2 }.
% 0.81/1.22 { op( op( e3, e2 ), op( e2, e3 ) ) = e2 }.
% 0.81/1.22 { op( op( e4, e2 ), op( e2, e4 ) ) = e2 }.
% 0.81/1.22 { op( op( e0, e3 ), op( e3, e0 ) ) = e3 }.
% 0.81/1.22 { op( op( e1, e3 ), op( e3, e1 ) ) = e3 }.
% 0.81/1.22 { op( op( e2, e3 ), op( e3, e2 ) ) = e3 }.
% 0.81/1.22 { op( op( e3, e3 ), op( e3, e3 ) ) = e3 }.
% 0.81/1.22 { op( op( e4, e3 ), op( e3, e4 ) ) = e3 }.
% 0.81/1.22 { op( op( e0, e4 ), op( e4, e0 ) ) = e4 }.
% 0.81/1.22 { op( op( e1, e4 ), op( e4, e1 ) ) = e4 }.
% 0.81/1.22 { op( op( e2, e4 ), op( e4, e2 ) ) = e4 }.
% 0.81/1.22 { op( op( e3, e4 ), op( e4, e3 ) ) = e4 }.
% 0.81/1.22 { op( op( e4, e4 ), op( e4, e4 ) ) = e4 }.
% 0.81/1.22 { ! op( e0, e0 ) = op( e1, e0 ) }.
% 0.81/1.22 { ! op( e0, e0 ) = op( e2, e0 ) }.
% 0.81/1.22 { ! op( e0, e0 ) = op( e3, e0 ) }.
% 0.81/1.22 { ! op( e0, e0 ) = op( e4, e0 ) }.
% 0.81/1.22 { ! op( e1, e0 ) = op( e2, e0 ) }.
% 0.81/1.22 { ! op( e1, e0 ) = op( e3, e0 ) }.
% 0.81/1.22 { ! op( e1, e0 ) = op( e4, e0 ) }.
% 0.81/1.22 { ! op( e2, e0 ) = op( e3, e0 ) }.
% 0.81/1.22 { ! op( e2, e0 ) = op( e4, e0 ) }.
% 0.81/1.22 { ! op( e3, e0 ) = op( e4, e0 ) }.
% 0.81/1.22 { ! op( e0, e1 ) = op( e1, e1 ) }.
% 0.81/1.22 { ! op( e0, e1 ) = op( e2, e1 ) }.
% 0.81/1.22 { ! op( e0, e1 ) = op( e3, e1 ) }.
% 0.81/1.22 { ! op( e0, e1 ) = op( e4, e1 ) }.
% 0.81/1.22 { ! op( e1, e1 ) = op( e2, e1 ) }.
% 0.81/1.22 { ! op( e1, e1 ) = op( e3, e1 ) }.
% 0.81/1.22 { ! op( e1, e1 ) = op( e4, e1 ) }.
% 0.81/1.22 { ! op( e2, e1 ) = op( e3, e1 ) }.
% 0.81/1.22 { ! op( e2, e1 ) = op( e4, e1 ) }.
% 0.81/1.22 { ! op( e3, e1 ) = op( e4, e1 ) }.
% 0.81/1.22 { ! op( e0, e2 ) = op( e1, e2 ) }.
% 0.81/1.22 { ! op( e0, e2 ) = op( e2, e2 ) }.
% 0.81/1.22 { ! op( e0, e2 ) = op( e3, e2 ) }.
% 0.81/1.22 { ! op( e0, e2 ) = op( e4, e2 ) }.
% 0.81/1.22 { ! op( e1, e2 ) = op( e2, e2 ) }.
% 0.81/1.22 { ! op( e1, e2 ) = op( e3, e2 ) }.
% 0.81/1.22 { ! op( e1, e2 ) = op( e4, e2 ) }.
% 0.81/1.22 { ! op( e2, e2 ) = op( e3, e2 ) }.
% 0.81/1.22 { ! op( e2, e2 ) = op( e4, e2 ) }.
% 0.81/1.22 { ! op( e3, e2 ) = op( e4, e2 ) }.
% 0.81/1.22 { ! op( e0, e3 ) = op( e1, e3 ) }.
% 0.81/1.22 { ! op( e0, e3 ) = op( e2, e3 ) }.
% 0.81/1.22 { ! op( e0, e3 ) = op( e3, e3 ) }.
% 0.81/1.22 { ! op( e0, e3 ) = op( e4, e3 ) }.
% 0.81/1.22 { ! op( e1, e3 ) = op( e2, e3 ) }.
% 0.81/1.22 { ! op( e1, e3 ) = op( e3, e3 ) }.
% 0.81/1.22 { ! op( e1, e3 ) = op( e4, e3 ) }.
% 0.81/1.22 { ! op( e2, e3 ) = op( e3, e3 ) }.
% 0.81/1.22 { ! op( e2, e3 ) = op( e4, e3 ) }.
% 0.81/1.22 { ! op( e3, e3 ) = op( e4, e3 ) }.
% 0.81/1.22 { ! op( e0, e4 ) = op( e1, e4 ) }.
% 0.81/1.22 { ! op( e0, e4 ) = op( e2, e4 ) }.
% 0.81/1.22 { ! op( e0, e4 ) = op( e3, e4 ) }.
% 0.81/1.22 { ! op( e0, e4 ) = op( e4, e4 ) }.
% 0.81/1.22 { ! op( e1, e4 ) = op( e2, e4 ) }.
% 0.81/1.22 { ! op( e1, e4 ) = op( e3, e4 ) }.
% 0.81/1.22 { ! op( e1, e4 ) = op( e4, e4 ) }.
% 0.81/1.22 { ! op( e2, e4 ) = op( e3, e4 ) }.
% 0.81/1.22 { ! op( e2, e4 ) = op( e4, e4 ) }.
% 0.81/1.22 { ! op( e3, e4 ) = op( e4, e4 ) }.
% 0.81/1.22 { ! op( e0, e0 ) = op( e0, e1 ) }.
% 0.81/1.22 { ! op( e0, e0 ) = op( e0, e2 ) }.
% 0.81/1.22 { ! op( e0, e0 ) = op( e0, e3 ) }.
% 0.81/1.22 { ! op( e0, e0 ) = op( e0, e4 ) }.
% 0.81/1.22 { ! op( e0, e1 ) = op( e0, e2 ) }.
% 0.81/1.22 { ! op( e0, e1 ) = op( e0, e3 ) }.
% 0.81/1.22 { ! op( e0, e1 ) = op( e0, e4 ) }.
% 0.81/1.22 { ! op( e0, e2 ) = op( e0, e3 ) }.
% 0.81/1.22 { ! op( e0, e2 ) = op( e0, e4 ) }.
% 0.81/1.22 { ! op( e0, e3 ) = op( e0, e4 ) }.
% 0.81/1.22 { ! op( e1, e0 ) = op( e1, e1 ) }.
% 0.81/1.22 { ! op( e1, e0 ) = op( e1, e2 ) }.
% 0.81/1.22 { ! op( e1, e0 ) = op( e1, e3 ) }.
% 0.81/1.22 { ! op( e1, e0 ) = op( e1, e4 ) }.
% 0.81/1.22 { ! op( e1, e1 ) = op( e1, e2 ) }.
% 0.81/1.22 { ! op( e1, e1 ) = op( e1, e3 ) }.
% 0.81/1.22 { ! op( e1, e1 ) = op( e1, e4 ) }.
% 0.81/1.22 { ! op( e1, e2 ) = op( e1, e3 ) }.
% 0.81/1.22 { ! op( e1, e2 ) = op( e1, e4 ) }.
% 0.81/1.22 { ! op( e1, e3 ) = op( e1, e4 ) }.
% 0.81/1.22 { ! op( e2, e0 ) = op( e2, e1 ) }.
% 0.81/1.22 { ! op( e2, e0 ) = op( e2, e2 ) }.
% 0.81/1.22 { ! op( e2, e0 ) = op( e2, e3 ) }.
% 0.81/1.22 { ! op( e2, e0 ) = op( e2, e4 ) }.
% 0.81/1.22 { ! op( e2, e1 ) = op( e2, e2 ) }.
% 0.81/1.22 { ! op( e2, e1 ) = op( e2, e3 ) }.
% 0.81/1.22 { ! op( e2, e1 ) = op( e2, e4 ) }.
% 0.81/1.22 { ! op( e2, e2 ) = op( e2, e3 ) }.
% 0.81/1.22 { ! op( e2, e2 ) = op( e2, e4 ) }.
% 0.81/1.22 { ! op( e2, e3 ) = op( e2, e4 ) }.
% 0.81/1.22 { ! op( e3, e0 ) = op( e3, e1 ) }.
% 0.81/1.22 { ! op( e3, e0 ) = op( e3, e2 ) }.
% 0.81/1.22 { ! op( e3, e0 ) = op( e3, e3 ) }.
% 0.81/1.22 { ! op( e3, e0 ) = op( e3, e4 ) }.
% 0.81/1.22 { ! op( e3, e1 ) = op( e3, e2 ) }.
% 0.81/1.22 { ! op( e3, e1 ) = op( e3, e3 ) }.
% 0.81/1.22 { ! op( e3, e1 ) = op( e3, e4 ) }.
% 0.81/1.22 { ! op( e3, e2 ) = op( e3, e3 ) }.
% 0.81/1.22 { ! op( e3, e2 ) = op( e3, e4 ) }.
% 0.81/1.22 { ! op( e3, e3 ) = op( e3, e4 ) }.
% 0.81/1.22 { ! op( e4, e0 ) = op( e4, e1 ) }.
% 0.81/1.22 { ! op( e4, e0 ) = op( e4, e2 ) }.
% 0.81/1.22 { ! op( e4, e0 ) = op( e4, e3 ) }.
% 0.81/1.22 { ! op( e4, e0 ) = op( e4, e4 ) }.
% 0.81/1.22 { ! op( e4, e1 ) = op( e4, e2 ) }.
% 0.81/1.36 { ! op( e4, e1 ) = op( e4, e3 ) }.
% 0.81/1.36 { ! op( e4, e1 ) = op( e4, e4 ) }.
% 0.81/1.36 { ! op( e4, e2 ) = op( e4, e3 ) }.
% 0.81/1.36 { ! op( e4, e2 ) = op( e4, e4 ) }.
% 0.81/1.36 { ! op( e4, e3 ) = op( e4, e4 ) }.
% 0.81/1.36 { ! e0 = e1 }.
% 0.81/1.36 { ! e0 = e2 }.
% 0.81/1.36 { ! e0 = e3 }.
% 0.81/1.36 { ! e0 = e4 }.
% 0.81/1.36 { ! e1 = e2 }.
% 0.81/1.36 { ! e1 = e3 }.
% 0.81/1.36 { ! e1 = e4 }.
% 0.81/1.36 { ! e2 = e3 }.
% 0.81/1.36 { ! e2 = e4 }.
% 0.81/1.36 { ! e3 = e4 }.
% 0.81/1.36 { e0 = op( e4, op( e4, e4 ) ) }.
% 0.81/1.36 { e1 = op( e4, e4 ) }.
% 0.81/1.36 { e2 = op( op( e4, op( e4, e4 ) ), op( e4, e4 ) ) }.
% 0.81/1.36 { e3 = op( op( e4, op( e4, e4 ) ), op( e4, op( e4, e4 ) ) ) }.
% 0.81/1.36 { alpha1, alpha2 }.
% 0.81/1.36 { alpha1, ! op( e4, e4 ) = e4 }.
% 0.81/1.36 { op( op( e0, e0 ), e0 ) = e0 }.
% 0.81/1.36 { op( op( e0, e1 ), e1 ) = e0 }.
% 0.81/1.36 { op( op( e0, e2 ), e2 ) = e0 }.
% 0.81/1.36 { op( op( e0, e3 ), e3 ) = e0 }.
% 0.81/1.36 { op( op( e0, e4 ), e4 ) = e0 }.
% 0.81/1.36 { op( op( e1, e0 ), e0 ) = e1 }.
% 0.81/1.36 { op( op( e1, e1 ), e1 ) = e1 }.
% 0.81/1.36 { op( op( e1, e2 ), e2 ) = e1 }.
% 0.81/1.36 { op( op( e1, e3 ), e3 ) = e1 }.
% 0.81/1.36 { op( op( e1, e4 ), e4 ) = e1 }.
% 0.81/1.36 { op( op( e2, e0 ), e0 ) = e2 }.
% 0.81/1.36 { op( op( e2, e1 ), e1 ) = e2 }.
% 0.81/1.36 { op( op( e2, e2 ), e2 ) = e2 }.
% 0.81/1.36 { op( op( e2, e3 ), e3 ) = e2 }.
% 0.81/1.36 { op( op( e2, e4 ), e4 ) = e2 }.
% 0.81/1.36 { op( op( e3, e0 ), e0 ) = e3 }.
% 0.81/1.36 { op( op( e3, e1 ), e1 ) = e3 }.
% 0.81/1.36 { op( op( e3, e2 ), e2 ) = e3 }.
% 0.81/1.36 { op( op( e3, e3 ), e3 ) = e3 }.
% 0.81/1.36 { op( op( e3, e4 ), e4 ) = e3 }.
% 0.81/1.36 { op( op( e4, e0 ), e0 ) = e4 }.
% 0.81/1.36 { op( op( e4, e1 ), e1 ) = e4 }.
% 0.81/1.36 { op( op( e4, e2 ), e2 ) = e4 }.
% 0.81/1.36 { op( op( e4, e3 ), e3 ) = e4 }.
% 0.81/1.36 { op( op( e4, e4 ), e4 ) = e4 }.
% 0.81/1.36 { ! alpha2, alpha4 }.
% 0.81/1.36 { ! alpha2, ! op( e3, e4 ) = e3 }.
% 0.81/1.36 { ! alpha4, op( e3, e4 ) = e3, alpha2 }.
% 0.81/1.36 { ! alpha4, ! op( e0, e4 ) = e0 }.
% 0.81/1.36 { ! alpha4, ! op( e1, e4 ) = e1 }.
% 0.81/1.36 { ! alpha4, ! op( e2, e4 ) = e2 }.
% 0.81/1.36 { op( e0, e4 ) = e0, op( e1, e4 ) = e1, op( e2, e4 ) = e2, alpha4 }.
% 0.81/1.36 { ! alpha1, alpha3, alpha5 }.
% 0.81/1.36 { ! alpha3, alpha1 }.
% 0.81/1.36 { ! alpha5, alpha1 }.
% 0.81/1.36 { ! alpha5, alpha7 }.
% 0.81/1.36 { ! alpha5, ! op( e4, e3 ) = e4 }.
% 0.81/1.36 { ! alpha7, op( e4, e3 ) = e4, alpha5 }.
% 0.81/1.36 { ! alpha7, alpha10 }.
% 0.81/1.36 { ! alpha7, ! op( e3, e3 ) = e3 }.
% 0.81/1.36 { ! alpha10, op( e3, e3 ) = e3, alpha7 }.
% 0.81/1.36 { ! alpha10, ! op( e0, e3 ) = e0 }.
% 0.81/1.36 { ! alpha10, ! op( e1, e3 ) = e1 }.
% 0.81/1.36 { ! alpha10, ! op( e2, e3 ) = e2 }.
% 0.81/1.36 { op( e0, e3 ) = e0, op( e1, e3 ) = e1, op( e2, e3 ) = e2, alpha10 }.
% 0.81/1.36 { ! alpha3, alpha6, alpha8 }.
% 0.81/1.36 { ! alpha6, alpha3 }.
% 0.81/1.36 { ! alpha8, alpha3 }.
% 0.81/1.36 { ! alpha8, alpha11 }.
% 0.81/1.36 { ! alpha8, ! op( e4, e2 ) = e4 }.
% 0.81/1.36 { ! alpha11, op( e4, e2 ) = e4, alpha8 }.
% 0.81/1.36 { ! alpha11, alpha14 }.
% 0.81/1.36 { ! alpha11, ! op( e3, e2 ) = e3 }.
% 0.81/1.36 { ! alpha14, op( e3, e2 ) = e3, alpha11 }.
% 0.81/1.36 { ! alpha14, ! op( e0, e2 ) = e0 }.
% 0.81/1.36 { ! alpha14, ! op( e1, e2 ) = e1 }.
% 0.81/1.36 { ! alpha14, ! op( e2, e2 ) = e2 }.
% 0.81/1.36 { op( e0, e2 ) = e0, op( e1, e2 ) = e1, op( e2, e2 ) = e2, alpha14 }.
% 0.81/1.36 { ! alpha6, alpha9, alpha12 }.
% 0.81/1.36 { ! alpha9, alpha6 }.
% 0.81/1.36 { ! alpha12, alpha6 }.
% 0.81/1.36 { ! alpha12, alpha15 }.
% 0.81/1.36 { ! alpha12, ! op( e4, e1 ) = e4 }.
% 0.81/1.36 { ! alpha15, op( e4, e1 ) = e4, alpha12 }.
% 0.81/1.36 { ! alpha15, alpha17 }.
% 0.81/1.36 { ! alpha15, ! op( e3, e1 ) = e3 }.
% 0.81/1.36 { ! alpha17, op( e3, e1 ) = e3, alpha15 }.
% 0.81/1.36 { ! alpha17, ! op( e0, e1 ) = e0 }.
% 0.81/1.36 { ! alpha17, ! op( e1, e1 ) = e1 }.
% 0.81/1.36 { ! alpha17, ! op( e2, e1 ) = e2 }.
% 0.81/1.36 { op( e0, e1 ) = e0, op( e1, e1 ) = e1, op( e2, e1 ) = e2, alpha17 }.
% 0.81/1.36 { ! alpha9, alpha13 }.
% 0.81/1.36 { ! alpha9, ! op( e4, e0 ) = e4 }.
% 0.81/1.36 { ! alpha13, op( e4, e0 ) = e4, alpha9 }.
% 0.81/1.36 { ! alpha13, alpha16 }.
% 0.81/1.36 { ! alpha13, ! op( e3, e0 ) = e3 }.
% 0.81/1.36 { ! alpha16, op( e3, e0 ) = e3, alpha13 }.
% 0.81/1.36 { ! alpha16, ! op( e0, e0 ) = e0 }.
% 0.81/1.36 { ! alpha16, ! op( e1, e0 ) = e1 }.
% 0.81/1.36 { ! alpha16, ! op( e2, e0 ) = e2 }.
% 0.81/1.36 { op( e0, e0 ) = e0, op( e1, e0 ) = e1, op( e2, e0 ) = e2, alpha16 }.
% 0.81/1.36
% 0.81/1.36 *** allocated 15000 integers for clauses
% 0.81/1.36 percentage equality = 0.868538, percentage horn = 0.686869
% 0.81/1.36 This is a pure equality problem
% 0.81/1.36
% 0.81/1.36
% 0.81/1.36
% 0.81/1.36 Options Used:
% 0.81/1.36
% 0.81/1.36 useres = 1
% 0.81/1.36 useparamod = 1
% 0.81/1.36 useeqrefl = 1
% 0.81/1.36 useeqfact = 1
% 0.81/1.36 usefactor = 1
% 0.81/1.36 usesimpsplitting = 0
% 0.81/1.36 usesimpdemod = 5
% 0.81/1.36 usesimpres = 3
% 0.81/1.36
% 0.81/1.36 resimpinuse = 1000
% 0.81/1.36 resimpclauses = 20000
% 0.81/1.36 substype = eqrewr
% 0.81/1.36 backwardsubs = 1
% 0.81/1.36 selectoldest = 5
% 0.81/1.36
% 0.81/1.36 litorderings [0] = split
% 0.81/1.36 litorderings [1] = extend the termordering, first sorting on arguments
% 0.81/1.36
% 0.81/1.36 termordering = kbo
% 0.81/1.36
% 0.81/1.36 litapriori = 0
% 0.81/1.36 termapriori = 1
% 0.81/1.36 litaposteriori = 0
% 0.81/1.36 termaposteriori = 0
% 0.81/1.36 demodaposteriori = 0
% 0.81/1.36 ordereqreflfact = 0
% 0.81/1.36
% 0.81/1.36 litselect = negord
% 0.81/1.36
% 0.81/1.36 maxweight = 15
% 0.81/1.36 maxdepth = 30000
% 0.81/1.36 maxlength = 115
% 0.81/1.36 maxnrvars = 195
% 0.81/1.36 excuselevel = 1
% 0.81/1.36 increasemaxweight = 1
% 0.81/1.36
% 0.81/1.36 maxselected = 10000000
% 0.81/1.36 maxnrclauses = 10000000
% 0.81/1.36
% 0.81/1.36 showgenerated = 0
% 0.81/1.36 showkept = 0
% 0.81/1.36 showselected = 0
% 0.81/1.36 showdeleted = 0
% 0.81/1.36 showresimp = 1
% 0.81/1.36 showstatus = 2000
% 0.81/1.36
% 0.81/1.36 prologoutput = 0
% 0.81/1.36 nrgoals = 5000000
% 0.81/1.36 totalproof = 1
% 0.81/1.36
% 0.81/1.36 Symbols occurring in the translation:
% 0.81/1.36
% 0.81/1.36 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.81/1.36 . [1, 2] (w:1, o:33, a:1, s:1, b:0),
% 0.81/1.36 ! [4, 1] (w:0, o:28, a:1, s:1, b:0),
% 0.81/1.36 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.81/1.36 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.81/1.36 e0 [35, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.81/1.36 op [36, 2] (w:1, o:57, a:1, s:1, b:0),
% 0.81/1.36 e1 [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.81/1.36 e2 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.81/1.36 e3 [39, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.81/1.36 e4 [40, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.81/1.36 alpha1 [41, 0] (w:1, o:11, a:1, s:1, b:1),
% 0.81/1.36 alpha2 [42, 0] (w:1, o:20, a:1, s:1, b:1),
% 0.81/1.36 alpha3 [43, 0] (w:1, o:21, a:1, s:1, b:1),
% 0.81/1.36 alpha4 [44, 0] (w:1, o:22, a:1, s:1, b:1),
% 0.81/1.36 alpha5 [45, 0] (w:1, o:23, a:1, s:1, b:1),
% 0.81/1.36 alpha6 [46, 0] (w:1, o:24, a:1, s:1, b:1),
% 0.81/1.36 alpha7 [47, 0] (w:1, o:25, a:1, s:1, b:1),
% 0.81/1.36 alpha8 [48, 0] (w:1, o:26, a:1, s:1, b:1),
% 0.81/1.36 alpha9 [49, 0] (w:1, o:27, a:1, s:1, b:1),
% 0.81/1.36 alpha10 [50, 0] (w:1, o:12, a:1, s:1, b:1),
% 0.81/1.36 alpha11 [51, 0] (w:1, o:13, a:1, s:1, b:1),
% 0.81/1.36 alpha12 [52, 0] (w:1, o:14, a:1, s:1, b:1),
% 0.81/1.36 alpha13 [53, 0] (w:1, o:15, a:1, s:1, b:1),
% 0.81/1.36 alpha14 [54, 0] (w:1, o:16, a:1, s:1, b:1),
% 0.81/1.36 alpha15 [55, 0] (w:1, o:17, a:1, s:1, b:1),
% 0.81/1.36 alpha16 [56, 0] (w:1, o:18, a:1, s:1, b:1),
% 0.81/1.36 alpha17 [57, 0] (w:1, o:19, a:1, s:1, b:1).
% 0.81/1.36
% 0.81/1.36
% 0.81/1.36 Starting Search:
% 0.81/1.36
% 0.81/1.36 *** allocated 22500 integers for clauses
% 0.81/1.36 *** allocated 33750 integers for clauses
% 0.81/1.36 *** allocated 22500 integers for termspace/termends
% 0.81/1.36 *** allocated 50625 integers for clauses
% 0.81/1.36 Resimplifying inuse:
% 0.81/1.36 Done
% 0.81/1.36
% 0.81/1.36 *** allocated 33750 integers for termspace/termends
% 0.81/1.36 *** allocated 75937 integers for clauses
% 0.81/1.36 *** allocated 113905 integers for clauses
% 0.81/1.36
% 0.81/1.36 Intermediate Status:
% 0.81/1.36 Generated: 11144
% 0.81/1.36 Kept: 2007
% 0.81/1.36 Inuse: 434
% 0.81/1.36 Deleted: 73
% 0.81/1.36 Deletedinuse: 16
% 0.81/1.36
% 0.81/1.36 Resimplifying inuse:
% 0.81/1.36 Done
% 0.81/1.36
% 0.81/1.36 *** allocated 50625 integers for termspace/termends
% 0.81/1.36
% 0.81/1.36 Bliksems!, er is een bewijs:
% 0.81/1.36 % SZS status Theorem
% 0.81/1.36 % SZS output start Refutation
% 0.81/1.36
% 0.81/1.36 (75) {G0,W9,D4,L1,V0,M1} I { op( op( e0, e0 ), op( e0, e0 ) ) ==> e0 }.
% 0.81/1.36 (182) {G0,W7,D3,L1,V0,M1} I { ! op( e3, e3 ) ==> op( e3, e0 ) }.
% 0.81/1.36 (210) {G0,W7,D4,L1,V0,M1} I { op( e4, op( e4, e4 ) ) ==> e0 }.
% 0.81/1.36 (213) {G1,W5,D3,L1,V0,M1} I;d(210) { op( e0, e0 ) ==> e3 }.
% 0.81/1.36 (215) {G2,W5,D3,L1,V0,M1} I;d(213) { op( e3, e0 ) ==> e0 }.
% 0.81/1.36 (720) {G2,W5,D3,L1,V0,M1} S(75);d(213) { op( e3, e3 ) ==> e0 }.
% 0.81/1.36 (2518) {G3,W0,D0,L0,V0,M0} S(182);d(720);d(215);q { }.
% 0.81/1.36
% 0.81/1.36
% 0.81/1.36 % SZS output end Refutation
% 0.81/1.36 found a proof!
% 0.81/1.36
% 0.81/1.36
% 0.81/1.36 Unprocessed initial clauses:
% 0.81/1.36
% 0.81/1.36 (2520) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e0, op( e0, e0 ) = e1, op( e0
% 0.81/1.36 , e0 ) = e2, op( e0, e0 ) = e3, op( e0, e0 ) = e4 }.
% 0.81/1.36 (2521) {G0,W25,D3,L5,V0,M5} { op( e0, e1 ) = e0, op( e0, e1 ) = e1, op( e0
% 0.81/1.36 , e1 ) = e2, op( e0, e1 ) = e3, op( e0, e1 ) = e4 }.
% 0.81/1.36 (2522) {G0,W25,D3,L5,V0,M5} { op( e0, e2 ) = e0, op( e0, e2 ) = e1, op( e0
% 0.81/1.36 , e2 ) = e2, op( e0, e2 ) = e3, op( e0, e2 ) = e4 }.
% 0.81/1.36 (2523) {G0,W25,D3,L5,V0,M5} { op( e0, e3 ) = e0, op( e0, e3 ) = e1, op( e0
% 0.81/1.36 , e3 ) = e2, op( e0, e3 ) = e3, op( e0, e3 ) = e4 }.
% 0.81/1.36 (2524) {G0,W25,D3,L5,V0,M5} { op( e0, e4 ) = e0, op( e0, e4 ) = e1, op( e0
% 0.81/1.36 , e4 ) = e2, op( e0, e4 ) = e3, op( e0, e4 ) = e4 }.
% 0.81/1.36 (2525) {G0,W25,D3,L5,V0,M5} { op( e1, e0 ) = e0, op( e1, e0 ) = e1, op( e1
% 0.81/1.36 , e0 ) = e2, op( e1, e0 ) = e3, op( e1, e0 ) = e4 }.
% 0.81/1.36 (2526) {G0,W25,D3,L5,V0,M5} { op( e1, e1 ) = e0, op( e1, e1 ) = e1, op( e1
% 0.81/1.36 , e1 ) = e2, op( e1, e1 ) = e3, op( e1, e1 ) = e4 }.
% 0.81/1.36 (2527) {G0,W25,D3,L5,V0,M5} { op( e1, e2 ) = e0, op( e1, e2 ) = e1, op( e1
% 0.81/1.36 , e2 ) = e2, op( e1, e2 ) = e3, op( e1, e2 ) = e4 }.
% 0.81/1.36 (2528) {G0,W25,D3,L5,V0,M5} { op( e1, e3 ) = e0, op( e1, e3 ) = e1, op( e1
% 0.81/1.36 , e3 ) = e2, op( e1, e3 ) = e3, op( e1, e3 ) = e4 }.
% 0.81/1.36 (2529) {G0,W25,D3,L5,V0,M5} { op( e1, e4 ) = e0, op( e1, e4 ) = e1, op( e1
% 0.81/1.36 , e4 ) = e2, op( e1, e4 ) = e3, op( e1, e4 ) = e4 }.
% 0.81/1.36 (2530) {G0,W25,D3,L5,V0,M5} { op( e2, e0 ) = e0, op( e2, e0 ) = e1, op( e2
% 0.81/1.36 , e0 ) = e2, op( e2, e0 ) = e3, op( e2, e0 ) = e4 }.
% 0.81/1.36 (2531) {G0,W25,D3,L5,V0,M5} { op( e2, e1 ) = e0, op( e2, e1 ) = e1, op( e2
% 0.81/1.36 , e1 ) = e2, op( e2, e1 ) = e3, op( e2, e1 ) = e4 }.
% 0.81/1.36 (2532) {G0,W25,D3,L5,V0,M5} { op( e2, e2 ) = e0, op( e2, e2 ) = e1, op( e2
% 0.81/1.36 , e2 ) = e2, op( e2, e2 ) = e3, op( e2, e2 ) = e4 }.
% 0.81/1.36 (2533) {G0,W25,D3,L5,V0,M5} { op( e2, e3 ) = e0, op( e2, e3 ) = e1, op( e2
% 0.81/1.36 , e3 ) = e2, op( e2, e3 ) = e3, op( e2, e3 ) = e4 }.
% 0.81/1.36 (2534) {G0,W25,D3,L5,V0,M5} { op( e2, e4 ) = e0, op( e2, e4 ) = e1, op( e2
% 0.81/1.36 , e4 ) = e2, op( e2, e4 ) = e3, op( e2, e4 ) = e4 }.
% 0.81/1.36 (2535) {G0,W25,D3,L5,V0,M5} { op( e3, e0 ) = e0, op( e3, e0 ) = e1, op( e3
% 0.81/1.36 , e0 ) = e2, op( e3, e0 ) = e3, op( e3, e0 ) = e4 }.
% 0.81/1.36 (2536) {G0,W25,D3,L5,V0,M5} { op( e3, e1 ) = e0, op( e3, e1 ) = e1, op( e3
% 0.81/1.36 , e1 ) = e2, op( e3, e1 ) = e3, op( e3, e1 ) = e4 }.
% 0.81/1.36 (2537) {G0,W25,D3,L5,V0,M5} { op( e3, e2 ) = e0, op( e3, e2 ) = e1, op( e3
% 0.81/1.36 , e2 ) = e2, op( e3, e2 ) = e3, op( e3, e2 ) = e4 }.
% 0.81/1.36 (2538) {G0,W25,D3,L5,V0,M5} { op( e3, e3 ) = e0, op( e3, e3 ) = e1, op( e3
% 0.81/1.36 , e3 ) = e2, op( e3, e3 ) = e3, op( e3, e3 ) = e4 }.
% 0.81/1.36 (2539) {G0,W25,D3,L5,V0,M5} { op( e3, e4 ) = e0, op( e3, e4 ) = e1, op( e3
% 0.81/1.36 , e4 ) = e2, op( e3, e4 ) = e3, op( e3, e4 ) = e4 }.
% 0.81/1.36 (2540) {G0,W25,D3,L5,V0,M5} { op( e4, e0 ) = e0, op( e4, e0 ) = e1, op( e4
% 0.81/1.36 , e0 ) = e2, op( e4, e0 ) = e3, op( e4, e0 ) = e4 }.
% 0.81/1.36 (2541) {G0,W25,D3,L5,V0,M5} { op( e4, e1 ) = e0, op( e4, e1 ) = e1, op( e4
% 0.81/1.36 , e1 ) = e2, op( e4, e1 ) = e3, op( e4, e1 ) = e4 }.
% 0.81/1.36 (2542) {G0,W25,D3,L5,V0,M5} { op( e4, e2 ) = e0, op( e4, e2 ) = e1, op( e4
% 0.81/1.36 , e2 ) = e2, op( e4, e2 ) = e3, op( e4, e2 ) = e4 }.
% 0.81/1.36 (2543) {G0,W25,D3,L5,V0,M5} { op( e4, e3 ) = e0, op( e4, e3 ) = e1, op( e4
% 0.81/1.36 , e3 ) = e2, op( e4, e3 ) = e3, op( e4, e3 ) = e4 }.
% 0.81/1.36 (2544) {G0,W25,D3,L5,V0,M5} { op( e4, e4 ) = e0, op( e4, e4 ) = e1, op( e4
% 0.81/1.36 , e4 ) = e2, op( e4, e4 ) = e3, op( e4, e4 ) = e4 }.
% 0.81/1.36 (2545) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e0, op( e0, e1 ) = e0, op( e0
% 0.81/1.36 , e2 ) = e0, op( e0, e3 ) = e0, op( e0, e4 ) = e0 }.
% 0.81/1.36 (2546) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e0, op( e1, e0 ) = e0, op( e2
% 0.81/1.36 , e0 ) = e0, op( e3, e0 ) = e0, op( e4, e0 ) = e0 }.
% 0.81/1.36 (2547) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e1, op( e0, e1 ) = e1, op( e0
% 0.81/1.36 , e2 ) = e1, op( e0, e3 ) = e1, op( e0, e4 ) = e1 }.
% 0.81/1.36 (2548) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e1, op( e1, e0 ) = e1, op( e2
% 0.81/1.36 , e0 ) = e1, op( e3, e0 ) = e1, op( e4, e0 ) = e1 }.
% 0.81/1.36 (2549) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e2, op( e0, e1 ) = e2, op( e0
% 0.81/1.36 , e2 ) = e2, op( e0, e3 ) = e2, op( e0, e4 ) = e2 }.
% 0.81/1.36 (2550) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e2, op( e1, e0 ) = e2, op( e2
% 0.81/1.36 , e0 ) = e2, op( e3, e0 ) = e2, op( e4, e0 ) = e2 }.
% 0.81/1.36 (2551) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e3, op( e0, e1 ) = e3, op( e0
% 0.81/1.36 , e2 ) = e3, op( e0, e3 ) = e3, op( e0, e4 ) = e3 }.
% 0.81/1.36 (2552) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e3, op( e1, e0 ) = e3, op( e2
% 0.81/1.36 , e0 ) = e3, op( e3, e0 ) = e3, op( e4, e0 ) = e3 }.
% 0.81/1.36 (2553) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e4, op( e0, e1 ) = e4, op( e0
% 0.81/1.36 , e2 ) = e4, op( e0, e3 ) = e4, op( e0, e4 ) = e4 }.
% 0.81/1.36 (2554) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e4, op( e1, e0 ) = e4, op( e2
% 0.81/1.36 , e0 ) = e4, op( e3, e0 ) = e4, op( e4, e0 ) = e4 }.
% 0.81/1.36 (2555) {G0,W25,D3,L5,V0,M5} { op( e1, e0 ) = e0, op( e1, e1 ) = e0, op( e1
% 0.81/1.36 , e2 ) = e0, op( e1, e3 ) = e0, op( e1, e4 ) = e0 }.
% 0.81/1.36 (2556) {G0,W25,D3,L5,V0,M5} { op( e0, e1 ) = e0, op( e1, e1 ) = e0, op( e2
% 0.81/1.36 , e1 ) = e0, op( e3, e1 ) = e0, op( e4, e1 ) = e0 }.
% 0.81/1.36 (2557) {G0,W25,D3,L5,V0,M5} { op( e1, e0 ) = e1, op( e1, e1 ) = e1, op( e1
% 0.81/1.36 , e2 ) = e1, op( e1, e3 ) = e1, op( e1, e4 ) = e1 }.
% 0.81/1.36 (2558) {G0,W25,D3,L5,V0,M5} { op( e0, e1 ) = e1, op( e1, e1 ) = e1, op( e2
% 0.81/1.36 , e1 ) = e1, op( e3, e1 ) = e1, op( e4, e1 ) = e1 }.
% 0.81/1.36 (2559) {G0,W25,D3,L5,V0,M5} { op( e1, e0 ) = e2, op( e1, e1 ) = e2, op( e1
% 0.81/1.36 , e2 ) = e2, op( e1, e3 ) = e2, op( e1, e4 ) = e2 }.
% 0.81/1.36 (2560) {G0,W25,D3,L5,V0,M5} { op( e0, e1 ) = e2, op( e1, e1 ) = e2, op( e2
% 0.81/1.36 , e1 ) = e2, op( e3, e1 ) = e2, op( e4, e1 ) = e2 }.
% 0.81/1.36 (2561) {G0,W25,D3,L5,V0,M5} { op( e1, e0 ) = e3, op( e1, e1 ) = e3, op( e1
% 0.81/1.36 , e2 ) = e3, op( e1, e3 ) = e3, op( e1, e4 ) = e3 }.
% 0.81/1.36 (2562) {G0,W25,D3,L5,V0,M5} { op( e0, e1 ) = e3, op( e1, e1 ) = e3, op( e2
% 0.81/1.36 , e1 ) = e3, op( e3, e1 ) = e3, op( e4, e1 ) = e3 }.
% 0.81/1.36 (2563) {G0,W25,D3,L5,V0,M5} { op( e1, e0 ) = e4, op( e1, e1 ) = e4, op( e1
% 0.81/1.36 , e2 ) = e4, op( e1, e3 ) = e4, op( e1, e4 ) = e4 }.
% 0.81/1.36 (2564) {G0,W25,D3,L5,V0,M5} { op( e0, e1 ) = e4, op( e1, e1 ) = e4, op( e2
% 0.81/1.36 , e1 ) = e4, op( e3, e1 ) = e4, op( e4, e1 ) = e4 }.
% 0.81/1.36 (2565) {G0,W25,D3,L5,V0,M5} { op( e2, e0 ) = e0, op( e2, e1 ) = e0, op( e2
% 0.81/1.36 , e2 ) = e0, op( e2, e3 ) = e0, op( e2, e4 ) = e0 }.
% 0.81/1.36 (2566) {G0,W25,D3,L5,V0,M5} { op( e0, e2 ) = e0, op( e1, e2 ) = e0, op( e2
% 0.81/1.36 , e2 ) = e0, op( e3, e2 ) = e0, op( e4, e2 ) = e0 }.
% 0.81/1.36 (2567) {G0,W25,D3,L5,V0,M5} { op( e2, e0 ) = e1, op( e2, e1 ) = e1, op( e2
% 0.81/1.36 , e2 ) = e1, op( e2, e3 ) = e1, op( e2, e4 ) = e1 }.
% 0.81/1.36 (2568) {G0,W25,D3,L5,V0,M5} { op( e0, e2 ) = e1, op( e1, e2 ) = e1, op( e2
% 0.81/1.36 , e2 ) = e1, op( e3, e2 ) = e1, op( e4, e2 ) = e1 }.
% 0.81/1.36 (2569) {G0,W25,D3,L5,V0,M5} { op( e2, e0 ) = e2, op( e2, e1 ) = e2, op( e2
% 0.81/1.36 , e2 ) = e2, op( e2, e3 ) = e2, op( e2, e4 ) = e2 }.
% 0.81/1.36 (2570) {G0,W25,D3,L5,V0,M5} { op( e0, e2 ) = e2, op( e1, e2 ) = e2, op( e2
% 0.81/1.36 , e2 ) = e2, op( e3, e2 ) = e2, op( e4, e2 ) = e2 }.
% 0.81/1.36 (2571) {G0,W25,D3,L5,V0,M5} { op( e2, e0 ) = e3, op( e2, e1 ) = e3, op( e2
% 0.81/1.36 , e2 ) = e3, op( e2, e3 ) = e3, op( e2, e4 ) = e3 }.
% 0.81/1.36 (2572) {G0,W25,D3,L5,V0,M5} { op( e0, e2 ) = e3, op( e1, e2 ) = e3, op( e2
% 0.81/1.36 , e2 ) = e3, op( e3, e2 ) = e3, op( e4, e2 ) = e3 }.
% 0.81/1.36 (2573) {G0,W25,D3,L5,V0,M5} { op( e2, e0 ) = e4, op( e2, e1 ) = e4, op( e2
% 0.81/1.36 , e2 ) = e4, op( e2, e3 ) = e4, op( e2, e4 ) = e4 }.
% 0.81/1.36 (2574) {G0,W25,D3,L5,V0,M5} { op( e0, e2 ) = e4, op( e1, e2 ) = e4, op( e2
% 0.81/1.36 , e2 ) = e4, op( e3, e2 ) = e4, op( e4, e2 ) = e4 }.
% 0.81/1.36 (2575) {G0,W25,D3,L5,V0,M5} { op( e3, e0 ) = e0, op( e3, e1 ) = e0, op( e3
% 0.81/1.36 , e2 ) = e0, op( e3, e3 ) = e0, op( e3, e4 ) = e0 }.
% 0.81/1.36 (2576) {G0,W25,D3,L5,V0,M5} { op( e0, e3 ) = e0, op( e1, e3 ) = e0, op( e2
% 0.81/1.36 , e3 ) = e0, op( e3, e3 ) = e0, op( e4, e3 ) = e0 }.
% 0.81/1.36 (2577) {G0,W25,D3,L5,V0,M5} { op( e3, e0 ) = e1, op( e3, e1 ) = e1, op( e3
% 0.81/1.36 , e2 ) = e1, op( e3, e3 ) = e1, op( e3, e4 ) = e1 }.
% 0.81/1.36 (2578) {G0,W25,D3,L5,V0,M5} { op( e0, e3 ) = e1, op( e1, e3 ) = e1, op( e2
% 0.81/1.36 , e3 ) = e1, op( e3, e3 ) = e1, op( e4, e3 ) = e1 }.
% 0.81/1.36 (2579) {G0,W25,D3,L5,V0,M5} { op( e3, e0 ) = e2, op( e3, e1 ) = e2, op( e3
% 0.81/1.36 , e2 ) = e2, op( e3, e3 ) = e2, op( e3, e4 ) = e2 }.
% 0.81/1.36 (2580) {G0,W25,D3,L5,V0,M5} { op( e0, e3 ) = e2, op( e1, e3 ) = e2, op( e2
% 0.81/1.36 , e3 ) = e2, op( e3, e3 ) = e2, op( e4, e3 ) = e2 }.
% 0.81/1.36 (2581) {G0,W25,D3,L5,V0,M5} { op( e3, e0 ) = e3, op( e3, e1 ) = e3, op( e3
% 0.81/1.36 , e2 ) = e3, op( e3, e3 ) = e3, op( e3, e4 ) = e3 }.
% 0.81/1.36 (2582) {G0,W25,D3,L5,V0,M5} { op( e0, e3 ) = e3, op( e1, e3 ) = e3, op( e2
% 0.81/1.36 , e3 ) = e3, op( e3, e3 ) = e3, op( e4, e3 ) = e3 }.
% 0.81/1.36 (2583) {G0,W25,D3,L5,V0,M5} { op( e3, e0 ) = e4, op( e3, e1 ) = e4, op( e3
% 0.81/1.36 , e2 ) = e4, op( e3, e3 ) = e4, op( e3, e4 ) = e4 }.
% 0.81/1.36 (2584) {G0,W25,D3,L5,V0,M5} { op( e0, e3 ) = e4, op( e1, e3 ) = e4, op( e2
% 0.81/1.36 , e3 ) = e4, op( e3, e3 ) = e4, op( e4, e3 ) = e4 }.
% 0.81/1.36 (2585) {G0,W25,D3,L5,V0,M5} { op( e4, e0 ) = e0, op( e4, e1 ) = e0, op( e4
% 0.81/1.36 , e2 ) = e0, op( e4, e3 ) = e0, op( e4, e4 ) = e0 }.
% 0.81/1.36 (2586) {G0,W25,D3,L5,V0,M5} { op( e0, e4 ) = e0, op( e1, e4 ) = e0, op( e2
% 0.81/1.36 , e4 ) = e0, op( e3, e4 ) = e0, op( e4, e4 ) = e0 }.
% 0.81/1.36 (2587) {G0,W25,D3,L5,V0,M5} { op( e4, e0 ) = e1, op( e4, e1 ) = e1, op( e4
% 0.81/1.36 , e2 ) = e1, op( e4, e3 ) = e1, op( e4, e4 ) = e1 }.
% 0.81/1.36 (2588) {G0,W25,D3,L5,V0,M5} { op( e0, e4 ) = e1, op( e1, e4 ) = e1, op( e2
% 0.81/1.36 , e4 ) = e1, op( e3, e4 ) = e1, op( e4, e4 ) = e1 }.
% 0.81/1.36 (2589) {G0,W25,D3,L5,V0,M5} { op( e4, e0 ) = e2, op( e4, e1 ) = e2, op( e4
% 0.81/1.36 , e2 ) = e2, op( e4, e3 ) = e2, op( e4, e4 ) = e2 }.
% 0.81/1.36 (2590) {G0,W25,D3,L5,V0,M5} { op( e0, e4 ) = e2, op( e1, e4 ) = e2, op( e2
% 0.81/1.36 , e4 ) = e2, op( e3, e4 ) = e2, op( e4, e4 ) = e2 }.
% 0.81/1.36 (2591) {G0,W25,D3,L5,V0,M5} { op( e4, e0 ) = e3, op( e4, e1 ) = e3, op( e4
% 0.81/1.36 , e2 ) = e3, op( e4, e3 ) = e3, op( e4, e4 ) = e3 }.
% 0.81/1.36 (2592) {G0,W25,D3,L5,V0,M5} { op( e0, e4 ) = e3, op( e1, e4 ) = e3, op( e2
% 0.81/1.36 , e4 ) = e3, op( e3, e4 ) = e3, op( e4, e4 ) = e3 }.
% 0.81/1.36 (2593) {G0,W25,D3,L5,V0,M5} { op( e4, e0 ) = e4, op( e4, e1 ) = e4, op( e4
% 0.81/1.36 , e2 ) = e4, op( e4, e3 ) = e4, op( e4, e4 ) = e4 }.
% 0.81/1.36 (2594) {G0,W25,D3,L5,V0,M5} { op( e0, e4 ) = e4, op( e1, e4 ) = e4, op( e2
% 0.81/1.36 , e4 ) = e4, op( e3, e4 ) = e4, op( e4, e4 ) = e4 }.
% 0.81/1.36 (2595) {G0,W9,D4,L1,V0,M1} { op( op( e0, e0 ), op( e0, e0 ) ) = e0 }.
% 0.81/1.36 (2596) {G0,W9,D4,L1,V0,M1} { op( op( e1, e0 ), op( e0, e1 ) ) = e0 }.
% 0.81/1.36 (2597) {G0,W9,D4,L1,V0,M1} { op( op( e2, e0 ), op( e0, e2 ) ) = e0 }.
% 0.81/1.36 (2598) {G0,W9,D4,L1,V0,M1} { op( op( e3, e0 ), op( e0, e3 ) ) = e0 }.
% 0.81/1.36 (2599) {G0,W9,D4,L1,V0,M1} { op( op( e4, e0 ), op( e0, e4 ) ) = e0 }.
% 0.81/1.36 (2600) {G0,W9,D4,L1,V0,M1} { op( op( e0, e1 ), op( e1, e0 ) ) = e1 }.
% 0.81/1.36 (2601) {G0,W9,D4,L1,V0,M1} { op( op( e1, e1 ), op( e1, e1 ) ) = e1 }.
% 0.81/1.36 (2602) {G0,W9,D4,L1,V0,M1} { op( op( e2, e1 ), op( e1, e2 ) ) = e1 }.
% 0.81/1.36 (2603) {G0,W9,D4,L1,V0,M1} { op( op( e3, e1 ), op( e1, e3 ) ) = e1 }.
% 0.81/1.36 (2604) {G0,W9,D4,L1,V0,M1} { op( op( e4, e1 ), op( e1, e4 ) ) = e1 }.
% 0.81/1.36 (2605) {G0,W9,D4,L1,V0,M1} { op( op( e0, e2 ), op( e2, e0 ) ) = e2 }.
% 0.81/1.36 (2606) {G0,W9,D4,L1,V0,M1} { op( op( e1, e2 ), op( e2, e1 ) ) = e2 }.
% 0.81/1.36 (2607) {G0,W9,D4,L1,V0,M1} { op( op( e2, e2 ), op( e2, e2 ) ) = e2 }.
% 0.81/1.36 (2608) {G0,W9,D4,L1,V0,M1} { op( op( e3, e2 ), op( e2, e3 ) ) = e2 }.
% 0.81/1.36 (2609) {G0,W9,D4,L1,V0,M1} { op( op( e4, e2 ), op( e2, e4 ) ) = e2 }.
% 0.81/1.36 (2610) {G0,W9,D4,L1,V0,M1} { op( op( e0, e3 ), op( e3, e0 ) ) = e3 }.
% 0.81/1.36 (2611) {G0,W9,D4,L1,V0,M1} { op( op( e1, e3 ), op( e3, e1 ) ) = e3 }.
% 0.81/1.36 (2612) {G0,W9,D4,L1,V0,M1} { op( op( e2, e3 ), op( e3, e2 ) ) = e3 }.
% 0.81/1.36 (2613) {G0,W9,D4,L1,V0,M1} { op( op( e3, e3 ), op( e3, e3 ) ) = e3 }.
% 0.81/1.36 (2614) {G0,W9,D4,L1,V0,M1} { op( op( e4, e3 ), op( e3, e4 ) ) = e3 }.
% 0.81/1.36 (2615) {G0,W9,D4,L1,V0,M1} { op( op( e0, e4 ), op( e4, e0 ) ) = e4 }.
% 0.81/1.36 (2616) {G0,W9,D4,L1,V0,M1} { op( op( e1, e4 ), op( e4, e1 ) ) = e4 }.
% 0.81/1.36 (2617) {G0,W9,D4,L1,V0,M1} { op( op( e2, e4 ), op( e4, e2 ) ) = e4 }.
% 0.81/1.36 (2618) {G0,W9,D4,L1,V0,M1} { op( op( e3, e4 ), op( e4, e3 ) ) = e4 }.
% 0.81/1.36 (2619) {G0,W9,D4,L1,V0,M1} { op( op( e4, e4 ), op( e4, e4 ) ) = e4 }.
% 0.81/1.36 (2620) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e1, e0 ) }.
% 0.81/1.36 (2621) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e2, e0 ) }.
% 0.81/1.36 (2622) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e3, e0 ) }.
% 0.81/1.36 (2623) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e4, e0 ) }.
% 0.81/1.36 (2624) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e2, e0 ) }.
% 0.81/1.36 (2625) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e3, e0 ) }.
% 0.81/1.36 (2626) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e4, e0 ) }.
% 0.81/1.36 (2627) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e3, e0 ) }.
% 0.81/1.36 (2628) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e4, e0 ) }.
% 0.81/1.36 (2629) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e4, e0 ) }.
% 0.81/1.36 (2630) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e1, e1 ) }.
% 0.81/1.36 (2631) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e2, e1 ) }.
% 0.81/1.36 (2632) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e3, e1 ) }.
% 0.81/1.36 (2633) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e4, e1 ) }.
% 0.81/1.36 (2634) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e2, e1 ) }.
% 0.81/1.36 (2635) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e3, e1 ) }.
% 0.81/1.36 (2636) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e4, e1 ) }.
% 0.81/1.36 (2637) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e3, e1 ) }.
% 0.81/1.36 (2638) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e4, e1 ) }.
% 0.81/1.36 (2639) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e4, e1 ) }.
% 0.81/1.36 (2640) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e1, e2 ) }.
% 0.81/1.36 (2641) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e2, e2 ) }.
% 0.81/1.36 (2642) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e3, e2 ) }.
% 0.81/1.36 (2643) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e4, e2 ) }.
% 0.81/1.36 (2644) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e2, e2 ) }.
% 0.81/1.36 (2645) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e3, e2 ) }.
% 0.81/1.36 (2646) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e4, e2 ) }.
% 0.81/1.36 (2647) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e3, e2 ) }.
% 0.81/1.36 (2648) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e4, e2 ) }.
% 0.81/1.36 (2649) {G0,W7,D3,L1,V0,M1} { ! op( e3, e2 ) = op( e4, e2 ) }.
% 0.81/1.36 (2650) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e1, e3 ) }.
% 0.81/1.36 (2651) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e2, e3 ) }.
% 0.81/1.36 (2652) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e3, e3 ) }.
% 0.81/1.36 (2653) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e4, e3 ) }.
% 0.81/1.36 (2654) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e2, e3 ) }.
% 0.81/1.36 (2655) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e3, e3 ) }.
% 0.81/1.36 (2656) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e4, e3 ) }.
% 0.81/1.36 (2657) {G0,W7,D3,L1,V0,M1} { ! op( e2, e3 ) = op( e3, e3 ) }.
% 0.81/1.36 (2658) {G0,W7,D3,L1,V0,M1} { ! op( e2, e3 ) = op( e4, e3 ) }.
% 0.81/1.36 (2659) {G0,W7,D3,L1,V0,M1} { ! op( e3, e3 ) = op( e4, e3 ) }.
% 0.81/1.36 (2660) {G0,W7,D3,L1,V0,M1} { ! op( e0, e4 ) = op( e1, e4 ) }.
% 0.81/1.36 (2661) {G0,W7,D3,L1,V0,M1} { ! op( e0, e4 ) = op( e2, e4 ) }.
% 0.81/1.36 (2662) {G0,W7,D3,L1,V0,M1} { ! op( e0, e4 ) = op( e3, e4 ) }.
% 0.81/1.36 (2663) {G0,W7,D3,L1,V0,M1} { ! op( e0, e4 ) = op( e4, e4 ) }.
% 0.81/1.36 (2664) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e2, e4 ) }.
% 0.81/1.36 (2665) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e3, e4 ) }.
% 0.81/1.36 (2666) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e4, e4 ) }.
% 0.81/1.36 (2667) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e3, e4 ) }.
% 0.81/1.36 (2668) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e4, e4 ) }.
% 0.81/1.36 (2669) {G0,W7,D3,L1,V0,M1} { ! op( e3, e4 ) = op( e4, e4 ) }.
% 0.81/1.36 (2670) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e1 ) }.
% 0.81/1.36 (2671) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e2 ) }.
% 0.81/1.36 (2672) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e3 ) }.
% 0.81/1.36 (2673) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e4 ) }.
% 0.81/1.36 (2674) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e0, e2 ) }.
% 0.81/1.36 (2675) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e0, e3 ) }.
% 0.81/1.36 (2676) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e0, e4 ) }.
% 0.81/1.36 (2677) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e0, e3 ) }.
% 0.81/1.36 (2678) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e0, e4 ) }.
% 0.81/1.36 (2679) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e0, e4 ) }.
% 0.81/1.36 (2680) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e1 ) }.
% 0.81/1.36 (2681) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e2 ) }.
% 0.81/1.36 (2682) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e3 ) }.
% 0.81/1.36 (2683) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e4 ) }.
% 0.81/1.36 (2684) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e1, e2 ) }.
% 0.81/1.36 (2685) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e1, e3 ) }.
% 0.81/1.36 (2686) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e1, e4 ) }.
% 0.81/1.36 (2687) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e1, e3 ) }.
% 0.81/1.36 (2688) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e1, e4 ) }.
% 0.81/1.36 (2689) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e1, e4 ) }.
% 0.81/1.36 (2690) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e1 ) }.
% 0.81/1.36 (2691) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e2 ) }.
% 0.81/1.36 (2692) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e3 ) }.
% 0.81/1.36 (2693) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e4 ) }.
% 0.81/1.36 (2694) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e2 ) }.
% 0.81/1.36 (2695) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e3 ) }.
% 0.81/1.36 (2696) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e4 ) }.
% 0.81/1.36 (2697) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e2, e3 ) }.
% 0.81/1.36 (2698) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e2, e4 ) }.
% 0.81/1.36 (2699) {G0,W7,D3,L1,V0,M1} { ! op( e2, e3 ) = op( e2, e4 ) }.
% 0.81/1.36 (2700) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e1 ) }.
% 0.81/1.36 (2701) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e2 ) }.
% 0.81/1.36 (2702) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e3 ) }.
% 0.81/1.36 (2703) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e4 ) }.
% 0.81/1.36 (2704) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e3, e2 ) }.
% 0.81/1.36 (2705) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e3, e3 ) }.
% 0.81/1.36 (2706) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e3, e4 ) }.
% 0.81/1.36 (2707) {G0,W7,D3,L1,V0,M1} { ! op( e3, e2 ) = op( e3, e3 ) }.
% 0.81/1.36 (2708) {G0,W7,D3,L1,V0,M1} { ! op( e3, e2 ) = op( e3, e4 ) }.
% 0.81/1.36 (2709) {G0,W7,D3,L1,V0,M1} { ! op( e3, e3 ) = op( e3, e4 ) }.
% 0.81/1.36 (2710) {G0,W7,D3,L1,V0,M1} { ! op( e4, e0 ) = op( e4, e1 ) }.
% 0.81/1.36 (2711) {G0,W7,D3,L1,V0,M1} { ! op( e4, e0 ) = op( e4, e2 ) }.
% 0.81/1.36 (2712) {G0,W7,D3,L1,V0,M1} { ! op( e4, e0 ) = op( e4, e3 ) }.
% 0.81/1.36 (2713) {G0,W7,D3,L1,V0,M1} { ! op( e4, e0 ) = op( e4, e4 ) }.
% 0.81/1.36 (2714) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e4, e2 ) }.
% 0.81/1.36 (2715) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e4, e3 ) }.
% 0.81/1.36 (2716) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e4, e4 ) }.
% 0.81/1.36 (2717) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e4, e3 ) }.
% 0.81/1.36 (2718) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e4, e4 ) }.
% 0.81/1.36 (2719) {G0,W7,D3,L1,V0,M1} { ! op( e4, e3 ) = op( e4, e4 ) }.
% 0.81/1.36 (2720) {G0,W3,D2,L1,V0,M1} { ! e0 = e1 }.
% 0.81/1.36 (2721) {G0,W3,D2,L1,V0,M1} { ! e0 = e2 }.
% 0.81/1.36 (2722) {G0,W3,D2,L1,V0,M1} { ! e0 = e3 }.
% 0.81/1.36 (2723) {G0,W3,D2,L1,V0,M1} { ! e0 = e4 }.
% 0.81/1.36 (2724) {G0,W3,D2,L1,V0,M1} { ! e1 = e2 }.
% 0.81/1.36 (2725) {G0,W3,D2,L1,V0,M1} { ! e1 = e3 }.
% 0.81/1.36 (2726) {G0,W3,D2,L1,V0,M1} { ! e1 = e4 }.
% 0.81/1.36 (2727) {G0,W3,D2,L1,V0,M1} { ! e2 = e3 }.
% 0.81/1.36 (2728) {G0,W3,D2,L1,V0,M1} { ! e2 = e4 }.
% 0.81/1.36 (2729) {G0,W3,D2,L1,V0,M1} { ! e3 = e4 }.
% 0.81/1.36 (2730) {G0,W7,D4,L1,V0,M1} { e0 = op( e4, op( e4, e4 ) ) }.
% 0.81/1.36 (2731) {G0,W5,D3,L1,V0,M1} { e1 = op( e4, e4 ) }.
% 0.81/1.36 (2732) {G0,W11,D5,L1,V0,M1} { e2 = op( op( e4, op( e4, e4 ) ), op( e4, e4
% 0.81/1.36 ) ) }.
% 0.81/1.36 (2733) {G0,W13,D5,L1,V0,M1} { e3 = op( op( e4, op( e4, e4 ) ), op( e4, op
% 0.81/1.36 ( e4, e4 ) ) ) }.
% 0.81/1.36 (2734) {G0,W2,D1,L2,V0,M2} { alpha1, alpha2 }.
% 0.81/1.36 (2735) {G0,W6,D3,L2,V0,M2} { alpha1, ! op( e4, e4 ) = e4 }.
% 0.81/1.36 (2736) {G0,W7,D4,L1,V0,M1} { op( op( e0, e0 ), e0 ) = e0 }.
% 0.81/1.36 (2737) {G0,W7,D4,L1,V0,M1} { op( op( e0, e1 ), e1 ) = e0 }.
% 0.81/1.36 (2738) {G0,W7,D4,L1,V0,M1} { op( op( e0, e2 ), e2 ) = e0 }.
% 0.81/1.36 (2739) {G0,W7,D4,L1,V0,M1} { op( op( e0, e3 ), e3 ) = e0 }.
% 0.81/1.36 (2740) {G0,W7,D4,L1,V0,M1} { op( op( e0, e4 ), e4 ) = e0 }.
% 0.81/1.36 (2741) {G0,W7,D4,L1,V0,M1} { op( op( e1, e0 ), e0 ) = e1 }.
% 0.81/1.36 (2742) {G0,W7,D4,L1,V0,M1} { op( op( e1, e1 ), e1 ) = e1 }.
% 0.81/1.36 (2743) {G0,W7,D4,L1,V0,M1} { op( op( e1, e2 ), e2 ) = e1 }.
% 0.81/1.36 (2744) {G0,W7,D4,L1,V0,M1} { op( op( e1, e3 ), e3 ) = e1 }.
% 0.81/1.36 (2745) {G0,W7,D4,L1,V0,M1} { op( op( e1, e4 ), e4 ) = e1 }.
% 0.81/1.36 (2746) {G0,W7,D4,L1,V0,M1} { op( op( e2, e0 ), e0 ) = e2 }.
% 0.81/1.36 (2747) {G0,W7,D4,L1,V0,M1} { op( op( e2, e1 ), e1 ) = e2 }.
% 0.81/1.36 (2748) {G0,W7,D4,L1,V0,M1} { op( op( e2, e2 ), e2 ) = e2 }.
% 0.81/1.36 (2749) {G0,W7,D4,L1,V0,M1} { op( op( e2, e3 ), e3 ) = e2 }.
% 0.81/1.36 (2750) {G0,W7,D4,L1,V0,M1} { op( op( e2, e4 ), e4 ) = e2 }.
% 0.81/1.36 (2751) {G0,W7,D4,L1,V0,M1} { op( op( e3, e0 ), e0 ) = e3 }.
% 0.81/1.36 (2752) {G0,W7,D4,L1,V0,M1} { op( op( e3, e1 ), e1 ) = e3 }.
% 0.81/1.36 (2753) {G0,W7,D4,L1,V0,M1} { op( op( e3, e2 ), e2 ) = e3 }.
% 0.81/1.36 (2754) {G0,W7,D4,L1,V0,M1} { op( op( e3, e3 ), e3 ) = e3 }.
% 0.81/1.36 (2755) {G0,W7,D4,L1,V0,M1} { op( op( e3, e4 ), e4 ) = e3 }.
% 0.81/1.36 (2756) {G0,W7,D4,L1,V0,M1} { op( op( e4, e0 ), e0 ) = e4 }.
% 0.81/1.36 (2757) {G0,W7,D4,L1,V0,M1} { op( op( e4, e1 ), e1 ) = e4 }.
% 0.81/1.36 (2758) {G0,W7,D4,L1,V0,M1} { op( op( e4, e2 ), e2 ) = e4 }.
% 0.81/1.36 (2759) {G0,W7,D4,L1,V0,M1} { op( op( e4, e3 ), e3 ) = e4 }.
% 0.81/1.36 (2760) {G0,W7,D4,L1,V0,M1} { op( op( e4, e4 ), e4 ) = e4 }.
% 0.81/1.36 (2761) {G0,W2,D1,L2,V0,M2} { ! alpha2, alpha4 }.
% 0.81/1.36 (2762) {G0,W6,D3,L2,V0,M2} { ! alpha2, ! op( e3, e4 ) = e3 }.
% 0.81/1.36 (2763) {G0,W7,D3,L3,V0,M3} { ! alpha4, op( e3, e4 ) = e3, alpha2 }.
% 0.81/1.36 (2764) {G0,W6,D3,L2,V0,M2} { ! alpha4, ! op( e0, e4 ) = e0 }.
% 0.81/1.36 (2765) {G0,W6,D3,L2,V0,M2} { ! alpha4, ! op( e1, e4 ) = e1 }.
% 0.81/1.36 (2766) {G0,W6,D3,L2,V0,M2} { ! alpha4, ! op( e2, e4 ) = e2 }.
% 0.81/1.36 (2767) {G0,W16,D3,L4,V0,M4} { op( e0, e4 ) = e0, op( e1, e4 ) = e1, op( e2
% 0.81/1.36 , e4 ) = e2, alpha4 }.
% 0.81/1.36 (2768) {G0,W3,D1,L3,V0,M3} { ! alpha1, alpha3, alpha5 }.
% 0.81/1.36 (2769) {G0,W2,D1,L2,V0,M2} { ! alpha3, alpha1 }.
% 0.81/1.36 (2770) {G0,W2,D1,L2,V0,M2} { ! alpha5, alpha1 }.
% 0.81/1.36 (2771) {G0,W2,D1,L2,V0,M2} { ! alpha5, alpha7 }.
% 0.81/1.36 (2772) {G0,W6,D3,L2,V0,M2} { ! alpha5, ! op( e4, e3 ) = e4 }.
% 0.81/1.36 (2773) {G0,W7,D3,L3,V0,M3} { ! alpha7, op( e4, e3 ) = e4, alpha5 }.
% 0.81/1.36 (2774) {G0,W2,D1,L2,V0,M2} { ! alpha7, alpha10 }.
% 0.81/1.36 (2775) {G0,W6,D3,L2,V0,M2} { ! alpha7, ! op( e3, e3 ) = e3 }.
% 0.81/1.36 (2776) {G0,W7,D3,L3,V0,M3} { ! alpha10, op( e3, e3 ) = e3, alpha7 }.
% 0.81/1.36 (2777) {G0,W6,D3,L2,V0,M2} { ! alpha10, ! op( e0, e3 ) = e0 }.
% 0.81/1.36 (2778) {G0,W6,D3,L2,V0,M2} { ! alpha10, ! op( e1, e3 ) = e1 }.
% 0.81/1.36 (2779) {G0,W6,D3,L2,V0,M2} { ! alpha10, ! op( e2, e3 ) = e2 }.
% 0.81/1.36 (2780) {G0,W16,D3,L4,V0,M4} { op( e0, e3 ) = e0, op( e1, e3 ) = e1, op( e2
% 0.81/1.36 , e3 ) = e2, alpha10 }.
% 0.81/1.36 (2781) {G0,W3,D1,L3,V0,M3} { ! alpha3, alpha6, alpha8 }.
% 0.81/1.57 (2782) {G0,W2,D1,L2,V0,M2} { ! alpha6, alpha3 }.
% 0.81/1.57 (2783) {G0,W2,D1,L2,V0,M2} { ! alpha8, alpha3 }.
% 0.81/1.57 (2784) {G0,W2,D1,L2,V0,M2} { ! alpha8, alpha11 }.
% 0.81/1.57 (2785) {G0,W6,D3,L2,V0,M2} { ! alpha8, ! op( e4, e2 ) = e4 }.
% 0.81/1.57 (2786) {G0,W7,D3,L3,V0,M3} { ! alpha11, op( e4, e2 ) = e4, alpha8 }.
% 0.81/1.57 (2787) {G0,W2,D1,L2,V0,M2} { ! alpha11, alpha14 }.
% 0.81/1.57 (2788) {G0,W6,D3,L2,V0,M2} { ! alpha11, ! op( e3, e2 ) = e3 }.
% 0.81/1.57 (2789) {G0,W7,D3,L3,V0,M3} { ! alpha14, op( e3, e2 ) = e3, alpha11 }.
% 0.81/1.57 (2790) {G0,W6,D3,L2,V0,M2} { ! alpha14, ! op( e0, e2 ) = e0 }.
% 0.81/1.57 (2791) {G0,W6,D3,L2,V0,M2} { ! alpha14, ! op( e1, e2 ) = e1 }.
% 0.81/1.57 (2792) {G0,W6,D3,L2,V0,M2} { ! alpha14, ! op( e2, e2 ) = e2 }.
% 0.81/1.57 (2793) {G0,W16,D3,L4,V0,M4} { op( e0, e2 ) = e0, op( e1, e2 ) = e1, op( e2
% 0.81/1.57 , e2 ) = e2, alpha14 }.
% 0.81/1.57 (2794) {G0,W3,D1,L3,V0,M3} { ! alpha6, alpha9, alpha12 }.
% 0.81/1.57 (2795) {G0,W2,D1,L2,V0,M2} { ! alpha9, alpha6 }.
% 0.81/1.57 (2796) {G0,W2,D1,L2,V0,M2} { ! alpha12, alpha6 }.
% 0.81/1.57 (2797) {G0,W2,D1,L2,V0,M2} { ! alpha12, alpha15 }.
% 0.81/1.57 (2798) {G0,W6,D3,L2,V0,M2} { ! alpha12, ! op( e4, e1 ) = e4 }.
% 0.81/1.57 (2799) {G0,W7,D3,L3,V0,M3} { ! alpha15, op( e4, e1 ) = e4, alpha12 }.
% 0.81/1.57 (2800) {G0,W2,D1,L2,V0,M2} { ! alpha15, alpha17 }.
% 0.81/1.57 (2801) {G0,W6,D3,L2,V0,M2} { ! alpha15, ! op( e3, e1 ) = e3 }.
% 0.81/1.57 (2802) {G0,W7,D3,L3,V0,M3} { ! alpha17, op( e3, e1 ) = e3, alpha15 }.
% 0.81/1.57 (2803) {G0,W6,D3,L2,V0,M2} { ! alpha17, ! op( e0, e1 ) = e0 }.
% 0.81/1.57 (2804) {G0,W6,D3,L2,V0,M2} { ! alpha17, ! op( e1, e1 ) = e1 }.
% 0.81/1.57 (2805) {G0,W6,D3,L2,V0,M2} { ! alpha17, ! op( e2, e1 ) = e2 }.
% 0.81/1.57 (2806) {G0,W16,D3,L4,V0,M4} { op( e0, e1 ) = e0, op( e1, e1 ) = e1, op( e2
% 0.81/1.57 , e1 ) = e2, alpha17 }.
% 0.81/1.57 (2807) {G0,W2,D1,L2,V0,M2} { ! alpha9, alpha13 }.
% 0.81/1.57 (2808) {G0,W6,D3,L2,V0,M2} { ! alpha9, ! op( e4, e0 ) = e4 }.
% 0.81/1.57 (2809) {G0,W7,D3,L3,V0,M3} { ! alpha13, op( e4, e0 ) = e4, alpha9 }.
% 0.81/1.57 (2810) {G0,W2,D1,L2,V0,M2} { ! alpha13, alpha16 }.
% 0.81/1.57 (2811) {G0,W6,D3,L2,V0,M2} { ! alpha13, ! op( e3, e0 ) = e3 }.
% 0.81/1.57 (2812) {G0,W7,D3,L3,V0,M3} { ! alpha16, op( e3, e0 ) = e3, alpha13 }.
% 0.81/1.57 (2813) {G0,W6,D3,L2,V0,M2} { ! alpha16, ! op( e0, e0 ) = e0 }.
% 0.81/1.57 (2814) {G0,W6,D3,L2,V0,M2} { ! alpha16, ! op( e1, e0 ) = e1 }.
% 0.81/1.57 (2815) {G0,W6,D3,L2,V0,M2} { ! alpha16, ! op( e2, e0 ) = e2 }.
% 0.81/1.57 (2816) {G0,W16,D3,L4,V0,M4} { op( e0, e0 ) = e0, op( e1, e0 ) = e1, op( e2
% 0.81/1.57 , e0 ) = e2, alpha16 }.
% 0.81/1.57
% 0.81/1.57
% 0.81/1.57 Total Proof:
% 0.81/1.57
% 0.81/1.57 *** allocated 75937 integers for termspace/termends
% 0.81/1.57 *** allocated 170857 integers for clauses
% 0.81/1.57 *** allocated 113905 integers for termspace/termends
% 0.81/1.57 subsumption: (75) {G0,W9,D4,L1,V0,M1} I { op( op( e0, e0 ), op( e0, e0 ) )
% 0.81/1.57 ==> e0 }.
% 0.81/1.57 parent0: (2595) {G0,W9,D4,L1,V0,M1} { op( op( e0, e0 ), op( e0, e0 ) ) =
% 0.81/1.57 e0 }.
% 0.81/1.57 substitution0:
% 0.81/1.57 end
% 0.81/1.57 permutation0:
% 0.81/1.57 0 ==> 0
% 0.81/1.57 end
% 0.81/1.57
% 0.81/1.57 *** allocated 170857 integers for termspace/termends
% 0.81/1.57 *** allocated 256285 integers for clauses
% 0.81/1.57 eqswap: (7575) {G0,W7,D3,L1,V0,M1} { ! op( e3, e3 ) = op( e3, e0 ) }.
% 0.81/1.57 parent0[0]: (2702) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e3 ) }.
% 0.81/1.57 substitution0:
% 0.81/1.57 end
% 0.81/1.57
% 0.81/1.57 subsumption: (182) {G0,W7,D3,L1,V0,M1} I { ! op( e3, e3 ) ==> op( e3, e0 )
% 0.81/1.57 }.
% 0.81/1.57 parent0: (7575) {G0,W7,D3,L1,V0,M1} { ! op( e3, e3 ) = op( e3, e0 ) }.
% 0.81/1.57 substitution0:
% 0.81/1.57 end
% 0.81/1.57 permutation0:
% 0.81/1.57 0 ==> 0
% 0.81/1.57 end
% 0.81/1.57
% 0.81/1.57 *** allocated 256285 integers for termspace/termends
% 0.81/1.57 *** allocated 384427 integers for clauses
% 0.81/1.57 eqswap: (10036) {G0,W7,D4,L1,V0,M1} { op( e4, op( e4, e4 ) ) = e0 }.
% 0.81/1.57 parent0[0]: (2730) {G0,W7,D4,L1,V0,M1} { e0 = op( e4, op( e4, e4 ) ) }.
% 0.81/1.57 substitution0:
% 0.81/1.57 end
% 0.81/1.57
% 0.81/1.57 subsumption: (210) {G0,W7,D4,L1,V0,M1} I { op( e4, op( e4, e4 ) ) ==> e0
% 0.81/1.57 }.
% 0.81/1.57 parent0: (10036) {G0,W7,D4,L1,V0,M1} { op( e4, op( e4, e4 ) ) = e0 }.
% 0.81/1.57 substitution0:
% 0.81/1.57 end
% 0.81/1.57 permutation0:
% 0.81/1.57 0 ==> 0
% 0.81/1.57 end
% 0.81/1.57
% 0.81/1.57 *** allocated 384427 integers for termspace/termends
% 0.81/1.57 paramod: (12722) {G1,W9,D5,L1,V0,M1} { e3 = op( op( e4, op( e4, e4 ) ), e0
% 0.81/1.57 ) }.
% 0.81/1.57 parent0[0]: (210) {G0,W7,D4,L1,V0,M1} I { op( e4, op( e4, e4 ) ) ==> e0 }.
% 0.81/1.57 parent1[0; 8]: (2733) {G0,W13,D5,L1,V0,M1} { e3 = op( op( e4, op( e4, e4 )
% 0.81/1.57 ), op( e4, op( e4, e4 ) ) ) }.
% 0.81/1.57 substitution0:
% 0.81/1.57 end
% 0.81/1.57 substitution1:
% 0.81/1.57 end
% 0.81/1.57
% 0.81/1.57 paramod: (12723) {G1,W5,D3,L1,V0,M1} { e3 = op( e0, e0 ) }.
% 0.81/1.57 parent0[0]: (210) {G0,W7,D4,L1,V0,M1} I { op( e4, op( e4, e4 ) ) ==> e0 }.
% 0.81/1.57 parent1[0; 3]: (12722) {G1,W9,D5,L1,V0,M1} { e3 = op( op( e4, op( e4, e4 )
% 1.69/2.04 ), e0 ) }.
% 1.69/2.04 substitution0:
% 1.69/2.04 end
% 1.69/2.04 substitution1:
% 1.69/2.04 end
% 1.69/2.04
% 1.69/2.04 eqswap: (12725) {G1,W5,D3,L1,V0,M1} { op( e0, e0 ) = e3 }.
% 1.69/2.04 parent0[0]: (12723) {G1,W5,D3,L1,V0,M1} { e3 = op( e0, e0 ) }.
% 1.69/2.04 substitution0:
% 1.69/2.04 end
% 1.69/2.04
% 1.69/2.04 subsumption: (213) {G1,W5,D3,L1,V0,M1} I;d(210) { op( e0, e0 ) ==> e3 }.
% 1.69/2.04 parent0: (12725) {G1,W5,D3,L1,V0,M1} { op( e0, e0 ) = e3 }.
% 1.69/2.04 substitution0:
% 1.69/2.04 end
% 1.69/2.04 permutation0:
% 1.69/2.04 0 ==> 0
% 1.69/2.04 end
% 1.69/2.04
% 1.69/2.04 *** allocated 576640 integers for clauses
% 1.69/2.04 paramod: (38206) {G1,W5,D3,L1,V0,M1} { op( e3, e0 ) = e0 }.
% 1.69/2.04 parent0[0]: (213) {G1,W5,D3,L1,V0,M1} I;d(210) { op( e0, e0 ) ==> e3 }.
% 1.69/2.04 parent1[0; 2]: (2736) {G0,W7,D4,L1,V0,M1} { op( op( e0, e0 ), e0 ) = e0
% 1.69/2.04 }.
% 1.69/2.04 substitution0:
% 1.69/2.04 end
% 1.69/2.04 substitution1:
% 1.69/2.04 end
% 1.69/2.04
% 1.69/2.04 subsumption: (215) {G2,W5,D3,L1,V0,M1} I;d(213) { op( e3, e0 ) ==> e0 }.
% 1.69/2.04 parent0: (38206) {G1,W5,D3,L1,V0,M1} { op( e3, e0 ) = e0 }.
% 1.69/2.04 substitution0:
% 1.69/2.04 end
% 1.69/2.04 permutation0:
% 1.69/2.04 0 ==> 0
% 1.69/2.04 end
% 1.69/2.04
% 1.69/2.04 paramod: (38211) {G1,W7,D4,L1,V0,M1} { op( op( e0, e0 ), e3 ) ==> e0 }.
% 1.69/2.04 parent0[0]: (213) {G1,W5,D3,L1,V0,M1} I;d(210) { op( e0, e0 ) ==> e3 }.
% 1.69/2.04 parent1[0; 5]: (75) {G0,W9,D4,L1,V0,M1} I { op( op( e0, e0 ), op( e0, e0 )
% 1.69/2.04 ) ==> e0 }.
% 1.69/2.04 substitution0:
% 1.69/2.04 end
% 1.69/2.04 substitution1:
% 1.69/2.04 end
% 1.69/2.04
% 1.69/2.04 paramod: (38212) {G2,W5,D3,L1,V0,M1} { op( e3, e3 ) ==> e0 }.
% 1.69/2.04 parent0[0]: (213) {G1,W5,D3,L1,V0,M1} I;d(210) { op( e0, e0 ) ==> e3 }.
% 1.69/2.04 parent1[0; 2]: (38211) {G1,W7,D4,L1,V0,M1} { op( op( e0, e0 ), e3 ) ==> e0
% 1.69/2.04 }.
% 1.69/2.04 substitution0:
% 1.69/2.04 end
% 1.69/2.04 substitution1:
% 1.69/2.04 end
% 1.69/2.04
% 1.69/2.04 subsumption: (720) {G2,W5,D3,L1,V0,M1} S(75);d(213) { op( e3, e3 ) ==> e0
% 1.69/2.04 }.
% 1.69/2.04 parent0: (38212) {G2,W5,D3,L1,V0,M1} { op( e3, e3 ) ==> e0 }.
% 1.69/2.04 substitution0:
% 1.69/2.04 end
% 1.69/2.04 permutation0:
% 1.69/2.04 0 ==> 0
% 1.69/2.04 end
% 1.69/2.04
% 1.69/2.04 paramod: (38219) {G1,W5,D3,L1,V0,M1} { ! e0 ==> op( e3, e0 ) }.
% 1.69/2.04 parent0[0]: (720) {G2,W5,D3,L1,V0,M1} S(75);d(213) { op( e3, e3 ) ==> e0
% 1.69/2.04 }.
% 1.69/2.04 parent1[0; 2]: (182) {G0,W7,D3,L1,V0,M1} I { ! op( e3, e3 ) ==> op( e3, e0
% 1.69/2.04 ) }.
% 1.69/2.04 substitution0:
% 1.69/2.04 end
% 1.69/2.04 substitution1:
% 1.69/2.04 end
% 1.69/2.04
% 1.69/2.04 paramod: (38220) {G2,W3,D2,L1,V0,M1} { ! e0 ==> e0 }.
% 1.69/2.04 parent0[0]: (215) {G2,W5,D3,L1,V0,M1} I;d(213) { op( e3, e0 ) ==> e0 }.
% 1.69/2.04 parent1[0; 3]: (38219) {G1,W5,D3,L1,V0,M1} { ! e0 ==> op( e3, e0 ) }.
% 1.69/2.04 substitution0:
% 1.69/2.04 end
% 1.69/2.04 substitution1:
% 1.69/2.04 end
% 1.69/2.04
% 1.69/2.04 eqrefl: (38221) {G0,W0,D0,L0,V0,M0} { }.
% 1.69/2.04 parent0[0]: (38220) {G2,W3,D2,L1,V0,M1} { ! e0 ==> e0 }.
% 1.69/2.04 substitution0:
% 1.69/2.04 end
% 1.69/2.04
% 1.69/2.04 subsumption: (2518) {G3,W0,D0,L0,V0,M0} S(182);d(720);d(215);q { }.
% 1.69/2.04 parent0: (38221) {G0,W0,D0,L0,V0,M0} { }.
% 1.69/2.04 substitution0:
% 1.69/2.04 end
% 1.69/2.04 permutation0:
% 1.69/2.04 end
% 1.69/2.04
% 1.69/2.04 Proof check complete!
% 1.69/2.04
% 1.69/2.04 Memory use:
% 1.69/2.04
% 1.69/2.04 space for terms: 37585
% 1.69/2.04 space for clauses: 93628
% 1.69/2.04
% 1.69/2.04
% 1.69/2.04 clauses generated: 12769
% 1.69/2.04 clauses kept: 2519
% 1.69/2.04 clauses selected: 476
% 1.69/2.04 clauses deleted: 95
% 1.69/2.04 clauses inuse deleted: 21
% 1.69/2.04
% 1.69/2.04 subsentry: 6132602
% 1.69/2.04 literals s-matched: 184028
% 1.69/2.04 literals matched: 184028
% 1.69/2.04 full subsumption: 0
% 1.69/2.04
% 1.69/2.04 checksum: 1496439059
% 1.69/2.04
% 1.69/2.04
% 1.69/2.04 Bliksem ended
%------------------------------------------------------------------------------