%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : ALG061+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n029.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:19 EDT 2022
% Result : Theorem 7.02s 7.46s
% Output : Refutation 7.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : ALG061+1 : TPTP v8.1.0. Released v2.7.0.
% 0.00/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n029.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 : Wed Jun 8 10:45:36 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.75/1.19 *** allocated 10000 integers for termspace/termends
% 0.75/1.19 *** allocated 10000 integers for clauses
% 0.75/1.19 *** allocated 10000 integers for justifications
% 0.75/1.19 Bliksem 1.12
% 0.75/1.19
% 0.75/1.19
% 0.75/1.19 Automatic Strategy Selection
% 0.75/1.19
% 0.75/1.19 *** allocated 15000 integers for termspace/termends
% 0.75/1.19
% 0.75/1.19 Clauses:
% 0.75/1.19
% 0.75/1.19 { op( e0, e0 ) = e0, op( e0, e0 ) = e1, op( e0, e0 ) = e2, op( e0, e0 ) =
% 0.75/1.19 e3, op( e0, e0 ) = e4 }.
% 0.75/1.19 { op( e0, e1 ) = e0, op( e0, e1 ) = e1, op( e0, e1 ) = e2, op( e0, e1 ) =
% 0.75/1.19 e3, op( e0, e1 ) = e4 }.
% 0.75/1.19 { op( e0, e2 ) = e0, op( e0, e2 ) = e1, op( e0, e2 ) = e2, op( e0, e2 ) =
% 0.75/1.19 e3, op( e0, e2 ) = e4 }.
% 0.75/1.19 { op( e0, e3 ) = e0, op( e0, e3 ) = e1, op( e0, e3 ) = e2, op( e0, e3 ) =
% 0.75/1.19 e3, op( e0, e3 ) = e4 }.
% 0.75/1.19 { op( e0, e4 ) = e0, op( e0, e4 ) = e1, op( e0, e4 ) = e2, op( e0, e4 ) =
% 0.75/1.19 e3, op( e0, e4 ) = e4 }.
% 0.75/1.19 { op( e1, e0 ) = e0, op( e1, e0 ) = e1, op( e1, e0 ) = e2, op( e1, e0 ) =
% 0.75/1.19 e3, op( e1, e0 ) = e4 }.
% 0.75/1.19 { op( e1, e1 ) = e0, op( e1, e1 ) = e1, op( e1, e1 ) = e2, op( e1, e1 ) =
% 0.75/1.19 e3, op( e1, e1 ) = e4 }.
% 0.75/1.19 { op( e1, e2 ) = e0, op( e1, e2 ) = e1, op( e1, e2 ) = e2, op( e1, e2 ) =
% 0.75/1.19 e3, op( e1, e2 ) = e4 }.
% 0.75/1.19 { op( e1, e3 ) = e0, op( e1, e3 ) = e1, op( e1, e3 ) = e2, op( e1, e3 ) =
% 0.75/1.19 e3, op( e1, e3 ) = e4 }.
% 0.75/1.19 { op( e1, e4 ) = e0, op( e1, e4 ) = e1, op( e1, e4 ) = e2, op( e1, e4 ) =
% 0.75/1.19 e3, op( e1, e4 ) = e4 }.
% 0.75/1.19 { op( e2, e0 ) = e0, op( e2, e0 ) = e1, op( e2, e0 ) = e2, op( e2, e0 ) =
% 0.75/1.19 e3, op( e2, e0 ) = e4 }.
% 0.75/1.19 { op( e2, e1 ) = e0, op( e2, e1 ) = e1, op( e2, e1 ) = e2, op( e2, e1 ) =
% 0.75/1.19 e3, op( e2, e1 ) = e4 }.
% 0.75/1.19 { op( e2, e2 ) = e0, op( e2, e2 ) = e1, op( e2, e2 ) = e2, op( e2, e2 ) =
% 0.75/1.19 e3, op( e2, e2 ) = e4 }.
% 0.75/1.19 { op( e2, e3 ) = e0, op( e2, e3 ) = e1, op( e2, e3 ) = e2, op( e2, e3 ) =
% 0.75/1.19 e3, op( e2, e3 ) = e4 }.
% 0.75/1.19 { op( e2, e4 ) = e0, op( e2, e4 ) = e1, op( e2, e4 ) = e2, op( e2, e4 ) =
% 0.75/1.19 e3, op( e2, e4 ) = e4 }.
% 0.75/1.19 { op( e3, e0 ) = e0, op( e3, e0 ) = e1, op( e3, e0 ) = e2, op( e3, e0 ) =
% 0.75/1.19 e3, op( e3, e0 ) = e4 }.
% 0.75/1.19 { op( e3, e1 ) = e0, op( e3, e1 ) = e1, op( e3, e1 ) = e2, op( e3, e1 ) =
% 0.75/1.19 e3, op( e3, e1 ) = e4 }.
% 0.75/1.19 { op( e3, e2 ) = e0, op( e3, e2 ) = e1, op( e3, e2 ) = e2, op( e3, e2 ) =
% 0.75/1.19 e3, op( e3, e2 ) = e4 }.
% 0.75/1.19 { op( e3, e3 ) = e0, op( e3, e3 ) = e1, op( e3, e3 ) = e2, op( e3, e3 ) =
% 0.75/1.19 e3, op( e3, e3 ) = e4 }.
% 0.75/1.19 { op( e3, e4 ) = e0, op( e3, e4 ) = e1, op( e3, e4 ) = e2, op( e3, e4 ) =
% 0.75/1.19 e3, op( e3, e4 ) = e4 }.
% 0.75/1.19 { op( e4, e0 ) = e0, op( e4, e0 ) = e1, op( e4, e0 ) = e2, op( e4, e0 ) =
% 0.75/1.19 e3, op( e4, e0 ) = e4 }.
% 0.75/1.19 { op( e4, e1 ) = e0, op( e4, e1 ) = e1, op( e4, e1 ) = e2, op( e4, e1 ) =
% 0.75/1.19 e3, op( e4, e1 ) = e4 }.
% 0.75/1.19 { op( e4, e2 ) = e0, op( e4, e2 ) = e1, op( e4, e2 ) = e2, op( e4, e2 ) =
% 0.75/1.19 e3, op( e4, e2 ) = e4 }.
% 0.75/1.19 { op( e4, e3 ) = e0, op( e4, e3 ) = e1, op( e4, e3 ) = e2, op( e4, e3 ) =
% 0.75/1.19 e3, op( e4, e3 ) = e4 }.
% 0.75/1.19 { op( e4, e4 ) = e0, op( e4, e4 ) = e1, op( e4, e4 ) = e2, op( e4, e4 ) =
% 0.75/1.19 e3, op( e4, e4 ) = e4 }.
% 0.75/1.19 { op( unit, e0 ) = e0 }.
% 0.75/1.19 { op( e0, unit ) = e0 }.
% 0.75/1.19 { op( unit, e1 ) = e1 }.
% 0.75/1.19 { op( e1, unit ) = e1 }.
% 0.75/1.19 { op( unit, e2 ) = e2 }.
% 0.75/1.19 { op( e2, unit ) = e2 }.
% 0.75/1.19 { op( unit, e3 ) = e3 }.
% 0.75/1.19 { op( e3, unit ) = e3 }.
% 0.75/1.19 { op( unit, e4 ) = e4 }.
% 0.75/1.19 { op( e4, unit ) = e4 }.
% 0.75/1.19 { unit = e0, unit = e1, unit = e2, unit = e3, unit = e4 }.
% 0.75/1.19 { op( e0, e0 ) = e0, op( e0, e1 ) = e0, op( e0, e2 ) = e0, op( e0, e3 ) =
% 0.75/1.19 e0, op( e0, e4 ) = e0 }.
% 0.75/1.19 { op( e0, e0 ) = e0, op( e1, e0 ) = e0, op( e2, e0 ) = e0, op( e3, e0 ) =
% 0.75/1.19 e0, op( e4, e0 ) = e0 }.
% 0.75/1.19 { op( e0, e0 ) = e1, op( e0, e1 ) = e1, op( e0, e2 ) = e1, op( e0, e3 ) =
% 0.75/1.19 e1, op( e0, e4 ) = e1 }.
% 0.75/1.19 { op( e0, e0 ) = e1, op( e1, e0 ) = e1, op( e2, e0 ) = e1, op( e3, e0 ) =
% 0.75/1.19 e1, op( e4, e0 ) = e1 }.
% 0.75/1.19 { op( e0, e0 ) = e2, op( e0, e1 ) = e2, op( e0, e2 ) = e2, op( e0, e3 ) =
% 0.75/1.19 e2, op( e0, e4 ) = e2 }.
% 0.75/1.19 { op( e0, e0 ) = e2, op( e1, e0 ) = e2, op( e2, e0 ) = e2, op( e3, e0 ) =
% 0.75/1.19 e2, op( e4, e0 ) = e2 }.
% 0.75/1.19 { op( e0, e0 ) = e3, op( e0, e1 ) = e3, op( e0, e2 ) = e3, op( e0, e3 ) =
% 0.75/1.19 e3, op( e0, e4 ) = e3 }.
% 0.75/1.19 { op( e0, e0 ) = e3, op( e1, e0 ) = e3, op( e2, e0 ) = e3, op( e3, e0 ) =
% 0.75/1.19 e3, op( e4, e0 ) = e3 }.
% 0.75/1.19 { op( e0, e0 ) = e4, op( e0, e1 ) = e4, op( e0, e2 ) = e4, op( e0, e3 ) =
% 0.75/1.19 e4, op( e0, e4 ) = e4 }.
% 0.75/1.19 { op( e0, e0 ) = e4, op( e1, e0 ) = e4, op( e2, e0 ) = e4, op( e3, e0 ) =
% 0.75/1.19 e4, op( e4, e0 ) = e4 }.
% 0.75/1.19 { op( e1, e0 ) = e0, op( e1, e1 ) = e0, op( e1, e2 ) = e0, op( e1, e3 ) =
% 0.75/1.19 e0, op( e1, e4 ) = e0 }.
% 0.75/1.19 { op( e0, e1 ) = e0, op( e1, e1 ) = e0, op( e2, e1 ) = e0, op( e3, e1 ) =
% 0.75/1.19 e0, op( e4, e1 ) = e0 }.
% 0.75/1.19 { op( e1, e0 ) = e1, op( e1, e1 ) = e1, op( e1, e2 ) = e1, op( e1, e3 ) =
% 0.75/1.19 e1, op( e1, e4 ) = e1 }.
% 0.75/1.19 { op( e0, e1 ) = e1, op( e1, e1 ) = e1, op( e2, e1 ) = e1, op( e3, e1 ) =
% 0.75/1.19 e1, op( e4, e1 ) = e1 }.
% 0.75/1.19 { op( e1, e0 ) = e2, op( e1, e1 ) = e2, op( e1, e2 ) = e2, op( e1, e3 ) =
% 0.75/1.19 e2, op( e1, e4 ) = e2 }.
% 0.75/1.19 { op( e0, e1 ) = e2, op( e1, e1 ) = e2, op( e2, e1 ) = e2, op( e3, e1 ) =
% 0.75/1.19 e2, op( e4, e1 ) = e2 }.
% 0.75/1.19 { op( e1, e0 ) = e3, op( e1, e1 ) = e3, op( e1, e2 ) = e3, op( e1, e3 ) =
% 0.75/1.19 e3, op( e1, e4 ) = e3 }.
% 0.75/1.19 { op( e0, e1 ) = e3, op( e1, e1 ) = e3, op( e2, e1 ) = e3, op( e3, e1 ) =
% 0.75/1.19 e3, op( e4, e1 ) = e3 }.
% 0.75/1.19 { op( e1, e0 ) = e4, op( e1, e1 ) = e4, op( e1, e2 ) = e4, op( e1, e3 ) =
% 0.75/1.19 e4, op( e1, e4 ) = e4 }.
% 0.75/1.19 { op( e0, e1 ) = e4, op( e1, e1 ) = e4, op( e2, e1 ) = e4, op( e3, e1 ) =
% 0.75/1.19 e4, op( e4, e1 ) = e4 }.
% 0.75/1.19 { op( e2, e0 ) = e0, op( e2, e1 ) = e0, op( e2, e2 ) = e0, op( e2, e3 ) =
% 0.75/1.19 e0, op( e2, e4 ) = e0 }.
% 0.75/1.19 { op( e0, e2 ) = e0, op( e1, e2 ) = e0, op( e2, e2 ) = e0, op( e3, e2 ) =
% 0.75/1.19 e0, op( e4, e2 ) = e0 }.
% 0.75/1.19 { op( e2, e0 ) = e1, op( e2, e1 ) = e1, op( e2, e2 ) = e1, op( e2, e3 ) =
% 0.75/1.19 e1, op( e2, e4 ) = e1 }.
% 0.75/1.19 { op( e0, e2 ) = e1, op( e1, e2 ) = e1, op( e2, e2 ) = e1, op( e3, e2 ) =
% 0.75/1.19 e1, op( e4, e2 ) = e1 }.
% 0.75/1.19 { op( e2, e0 ) = e2, op( e2, e1 ) = e2, op( e2, e2 ) = e2, op( e2, e3 ) =
% 0.75/1.19 e2, op( e2, e4 ) = e2 }.
% 0.75/1.19 { op( e0, e2 ) = e2, op( e1, e2 ) = e2, op( e2, e2 ) = e2, op( e3, e2 ) =
% 0.75/1.19 e2, op( e4, e2 ) = e2 }.
% 0.75/1.19 { op( e2, e0 ) = e3, op( e2, e1 ) = e3, op( e2, e2 ) = e3, op( e2, e3 ) =
% 0.75/1.19 e3, op( e2, e4 ) = e3 }.
% 0.75/1.19 { op( e0, e2 ) = e3, op( e1, e2 ) = e3, op( e2, e2 ) = e3, op( e3, e2 ) =
% 0.75/1.19 e3, op( e4, e2 ) = e3 }.
% 0.75/1.19 { op( e2, e0 ) = e4, op( e2, e1 ) = e4, op( e2, e2 ) = e4, op( e2, e3 ) =
% 0.75/1.19 e4, op( e2, e4 ) = e4 }.
% 0.75/1.19 { op( e0, e2 ) = e4, op( e1, e2 ) = e4, op( e2, e2 ) = e4, op( e3, e2 ) =
% 0.75/1.19 e4, op( e4, e2 ) = e4 }.
% 0.75/1.19 { op( e3, e0 ) = e0, op( e3, e1 ) = e0, op( e3, e2 ) = e0, op( e3, e3 ) =
% 0.75/1.19 e0, op( e3, e4 ) = e0 }.
% 0.75/1.19 { op( e0, e3 ) = e0, op( e1, e3 ) = e0, op( e2, e3 ) = e0, op( e3, e3 ) =
% 0.75/1.19 e0, op( e4, e3 ) = e0 }.
% 0.75/1.19 { op( e3, e0 ) = e1, op( e3, e1 ) = e1, op( e3, e2 ) = e1, op( e3, e3 ) =
% 0.75/1.19 e1, op( e3, e4 ) = e1 }.
% 0.75/1.19 { op( e0, e3 ) = e1, op( e1, e3 ) = e1, op( e2, e3 ) = e1, op( e3, e3 ) =
% 0.75/1.19 e1, op( e4, e3 ) = e1 }.
% 0.75/1.19 { op( e3, e0 ) = e2, op( e3, e1 ) = e2, op( e3, e2 ) = e2, op( e3, e3 ) =
% 0.75/1.19 e2, op( e3, e4 ) = e2 }.
% 0.75/1.19 { op( e0, e3 ) = e2, op( e1, e3 ) = e2, op( e2, e3 ) = e2, op( e3, e3 ) =
% 0.75/1.19 e2, op( e4, e3 ) = e2 }.
% 0.75/1.19 { op( e3, e0 ) = e3, op( e3, e1 ) = e3, op( e3, e2 ) = e3, op( e3, e3 ) =
% 0.75/1.19 e3, op( e3, e4 ) = e3 }.
% 0.75/1.19 { op( e0, e3 ) = e3, op( e1, e3 ) = e3, op( e2, e3 ) = e3, op( e3, e3 ) =
% 0.75/1.19 e3, op( e4, e3 ) = e3 }.
% 0.75/1.19 { op( e3, e0 ) = e4, op( e3, e1 ) = e4, op( e3, e2 ) = e4, op( e3, e3 ) =
% 0.75/1.19 e4, op( e3, e4 ) = e4 }.
% 0.75/1.19 { op( e0, e3 ) = e4, op( e1, e3 ) = e4, op( e2, e3 ) = e4, op( e3, e3 ) =
% 0.75/1.19 e4, op( e4, e3 ) = e4 }.
% 0.75/1.19 { op( e4, e0 ) = e0, op( e4, e1 ) = e0, op( e4, e2 ) = e0, op( e4, e3 ) =
% 0.75/1.19 e0, op( e4, e4 ) = e0 }.
% 0.75/1.19 { op( e0, e4 ) = e0, op( e1, e4 ) = e0, op( e2, e4 ) = e0, op( e3, e4 ) =
% 0.75/1.19 e0, op( e4, e4 ) = e0 }.
% 0.75/1.19 { op( e4, e0 ) = e1, op( e4, e1 ) = e1, op( e4, e2 ) = e1, op( e4, e3 ) =
% 0.75/1.19 e1, op( e4, e4 ) = e1 }.
% 0.75/1.19 { op( e0, e4 ) = e1, op( e1, e4 ) = e1, op( e2, e4 ) = e1, op( e3, e4 ) =
% 0.75/1.19 e1, op( e4, e4 ) = e1 }.
% 0.75/1.19 { op( e4, e0 ) = e2, op( e4, e1 ) = e2, op( e4, e2 ) = e2, op( e4, e3 ) =
% 0.75/1.19 e2, op( e4, e4 ) = e2 }.
% 0.75/1.19 { op( e0, e4 ) = e2, op( e1, e4 ) = e2, op( e2, e4 ) = e2, op( e3, e4 ) =
% 0.75/1.19 e2, op( e4, e4 ) = e2 }.
% 0.75/1.19 { op( e4, e0 ) = e3, op( e4, e1 ) = e3, op( e4, e2 ) = e3, op( e4, e3 ) =
% 0.75/1.19 e3, op( e4, e4 ) = e3 }.
% 0.75/1.19 { op( e0, e4 ) = e3, op( e1, e4 ) = e3, op( e2, e4 ) = e3, op( e3, e4 ) =
% 0.75/1.19 e3, op( e4, e4 ) = e3 }.
% 0.75/1.19 { op( e4, e0 ) = e4, op( e4, e1 ) = e4, op( e4, e2 ) = e4, op( e4, e3 ) =
% 0.75/1.19 e4, op( e4, e4 ) = e4 }.
% 0.75/1.19 { op( e0, e4 ) = e4, op( e1, e4 ) = e4, op( e2, e4 ) = e4, op( e3, e4 ) =
% 0.75/1.19 e4, op( e4, e4 ) = e4 }.
% 0.75/1.19 { ! op( e0, e0 ) = op( e1, e0 ) }.
% 0.75/1.19 { ! op( e0, e0 ) = op( e2, e0 ) }.
% 0.75/1.19 { ! op( e0, e0 ) = op( e3, e0 ) }.
% 0.75/1.19 { ! op( e0, e0 ) = op( e4, e0 ) }.
% 0.75/1.19 { ! op( e1, e0 ) = op( e2, e0 ) }.
% 0.75/1.19 { ! op( e1, e0 ) = op( e3, e0 ) }.
% 0.75/1.19 { ! op( e1, e0 ) = op( e4, e0 ) }.
% 0.75/1.19 { ! op( e2, e0 ) = op( e3, e0 ) }.
% 0.75/1.19 { ! op( e2, e0 ) = op( e4, e0 ) }.
% 0.75/1.19 { ! op( e3, e0 ) = op( e4, e0 ) }.
% 0.75/1.19 { ! op( e0, e1 ) = op( e1, e1 ) }.
% 0.75/1.19 { ! op( e0, e1 ) = op( e2, e1 ) }.
% 0.75/1.19 { ! op( e0, e1 ) = op( e3, e1 ) }.
% 0.75/1.19 { ! op( e0, e1 ) = op( e4, e1 ) }.
% 0.75/1.19 { ! op( e1, e1 ) = op( e2, e1 ) }.
% 0.75/1.19 { ! op( e1, e1 ) = op( e3, e1 ) }.
% 0.75/1.19 { ! op( e1, e1 ) = op( e4, e1 ) }.
% 0.75/1.19 { ! op( e2, e1 ) = op( e3, e1 ) }.
% 0.75/1.19 { ! op( e2, e1 ) = op( e4, e1 ) }.
% 0.75/1.19 { ! op( e3, e1 ) = op( e4, e1 ) }.
% 0.75/1.19 { ! op( e0, e2 ) = op( e1, e2 ) }.
% 0.75/1.19 { ! op( e0, e2 ) = op( e2, e2 ) }.
% 0.75/1.19 { ! op( e0, e2 ) = op( e3, e2 ) }.
% 0.75/1.19 { ! op( e0, e2 ) = op( e4, e2 ) }.
% 0.75/1.19 { ! op( e1, e2 ) = op( e2, e2 ) }.
% 0.75/1.19 { ! op( e1, e2 ) = op( e3, e2 ) }.
% 0.75/1.19 { ! op( e1, e2 ) = op( e4, e2 ) }.
% 0.75/1.19 { ! op( e2, e2 ) = op( e3, e2 ) }.
% 0.75/1.19 { ! op( e2, e2 ) = op( e4, e2 ) }.
% 0.75/1.19 { ! op( e3, e2 ) = op( e4, e2 ) }.
% 0.75/1.19 { ! op( e0, e3 ) = op( e1, e3 ) }.
% 0.75/1.19 { ! op( e0, e3 ) = op( e2, e3 ) }.
% 0.75/1.19 { ! op( e0, e3 ) = op( e3, e3 ) }.
% 0.75/1.19 { ! op( e0, e3 ) = op( e4, e3 ) }.
% 0.75/1.19 { ! op( e1, e3 ) = op( e2, e3 ) }.
% 0.75/1.19 { ! op( e1, e3 ) = op( e3, e3 ) }.
% 0.75/1.19 { ! op( e1, e3 ) = op( e4, e3 ) }.
% 0.75/1.19 { ! op( e2, e3 ) = op( e3, e3 ) }.
% 0.75/1.19 { ! op( e2, e3 ) = op( e4, e3 ) }.
% 0.75/1.19 { ! op( e3, e3 ) = op( e4, e3 ) }.
% 0.75/1.19 { ! op( e0, e4 ) = op( e1, e4 ) }.
% 0.75/1.19 { ! op( e0, e4 ) = op( e2, e4 ) }.
% 0.75/1.19 { ! op( e0, e4 ) = op( e3, e4 ) }.
% 0.75/1.19 { ! op( e0, e4 ) = op( e4, e4 ) }.
% 0.75/1.19 { ! op( e1, e4 ) = op( e2, e4 ) }.
% 0.75/1.19 { ! op( e1, e4 ) = op( e3, e4 ) }.
% 0.75/1.19 { ! op( e1, e4 ) = op( e4, e4 ) }.
% 0.75/1.19 { ! op( e2, e4 ) = op( e3, e4 ) }.
% 0.75/1.19 { ! op( e2, e4 ) = op( e4, e4 ) }.
% 0.75/1.19 { ! op( e3, e4 ) = op( e4, e4 ) }.
% 0.75/1.19 { ! op( e0, e0 ) = op( e0, e1 ) }.
% 0.75/1.19 { ! op( e0, e0 ) = op( e0, e2 ) }.
% 0.75/1.19 { ! op( e0, e0 ) = op( e0, e3 ) }.
% 0.75/1.19 { ! op( e0, e0 ) = op( e0, e4 ) }.
% 0.75/1.19 { ! op( e0, e1 ) = op( e0, e2 ) }.
% 0.75/1.19 { ! op( e0, e1 ) = op( e0, e3 ) }.
% 0.75/1.19 { ! op( e0, e1 ) = op( e0, e4 ) }.
% 0.75/1.19 { ! op( e0, e2 ) = op( e0, e3 ) }.
% 0.75/1.19 { ! op( e0, e2 ) = op( e0, e4 ) }.
% 0.75/1.19 { ! op( e0, e3 ) = op( e0, e4 ) }.
% 0.75/1.19 { ! op( e1, e0 ) = op( e1, e1 ) }.
% 0.75/1.19 { ! op( e1, e0 ) = op( e1, e2 ) }.
% 0.75/1.19 { ! op( e1, e0 ) = op( e1, e3 ) }.
% 0.75/1.19 { ! op( e1, e0 ) = op( e1, e4 ) }.
% 0.75/1.19 { ! op( e1, e1 ) = op( e1, e2 ) }.
% 0.75/1.19 { ! op( e1, e1 ) = op( e1, e3 ) }.
% 0.75/1.19 { ! op( e1, e1 ) = op( e1, e4 ) }.
% 0.75/1.19 { ! op( e1, e2 ) = op( e1, e3 ) }.
% 0.75/1.19 { ! op( e1, e2 ) = op( e1, e4 ) }.
% 0.75/1.19 { ! op( e1, e3 ) = op( e1, e4 ) }.
% 0.75/1.19 { ! op( e2, e0 ) = op( e2, e1 ) }.
% 0.75/1.19 { ! op( e2, e0 ) = op( e2, e2 ) }.
% 0.75/1.19 { ! op( e2, e0 ) = op( e2, e3 ) }.
% 0.75/1.19 { ! op( e2, e0 ) = op( e2, e4 ) }.
% 0.75/1.19 { ! op( e2, e1 ) = op( e2, e2 ) }.
% 0.75/1.19 { ! op( e2, e1 ) = op( e2, e3 ) }.
% 0.75/1.19 { ! op( e2, e1 ) = op( e2, e4 ) }.
% 0.75/1.19 { ! op( e2, e2 ) = op( e2, e3 ) }.
% 0.75/1.19 { ! op( e2, e2 ) = op( e2, e4 ) }.
% 0.75/1.19 { ! op( e2, e3 ) = op( e2, e4 ) }.
% 0.75/1.19 { ! op( e3, e0 ) = op( e3, e1 ) }.
% 0.75/1.19 { ! op( e3, e0 ) = op( e3, e2 ) }.
% 0.75/1.19 { ! op( e3, e0 ) = op( e3, e3 ) }.
% 0.75/1.19 { ! op( e3, e0 ) = op( e3, e4 ) }.
% 0.75/1.19 { ! op( e3, e1 ) = op( e3, e2 ) }.
% 0.75/1.19 { ! op( e3, e1 ) = op( e3, e3 ) }.
% 0.75/1.19 { ! op( e3, e1 ) = op( e3, e4 ) }.
% 0.75/1.19 { ! op( e3, e2 ) = op( e3, e3 ) }.
% 0.75/1.19 { ! op( e3, e2 ) = op( e3, e4 ) }.
% 0.75/1.19 { ! op( e3, e3 ) = op( e3, e4 ) }.
% 0.75/1.19 { ! op( e4, e0 ) = op( e4, e1 ) }.
% 0.75/1.19 { ! op( e4, e0 ) = op( e4, e2 ) }.
% 0.75/1.19 { ! op( e4, e0 ) = op( e4, e3 ) }.
% 0.75/1.19 { ! op( e4, e0 ) = op( e4, e4 ) }.
% 0.75/1.19 { ! op( e4, e1 ) = op( e4, e2 ) }.
% 0.75/1.19 { ! op( e4, e1 ) = op( e4, e3 ) }.
% 0.75/1.19 { ! op( e4, e1 ) = op( e4, e4 ) }.
% 0.75/1.19 { ! op( e4, e2 ) = op( e4, e3 ) }.
% 0.75/1.19 { ! op( e4, e2 ) = op( e4, e4 ) }.
% 0.75/1.19 { ! op( e4, e3 ) = op( e4, e4 ) }.
% 0.75/1.19 { ! e0 = e1 }.
% 0.75/1.19 { ! e0 = e2 }.
% 0.75/1.19 { ! e0 = e3 }.
% 0.75/1.19 { ! e0 = e4 }.
% 0.75/1.19 { ! e1 = e2 }.
% 0.75/1.19 { ! e1 = e3 }.
% 0.75/1.19 { ! e1 = e4 }.
% 0.75/1.19 { ! e2 = e3 }.
% 0.75/1.19 { ! e2 = e4 }.
% 0.75/1.19 { ! e3 = e4 }.
% 0.75/1.19 { e0 = op( e1, op( op( e1, e1 ), op( e1, e1 ) ) ) }.
% 0.75/1.19 { e2 = op( op( e1, e1 ), op( e1, e1 ) ) }.
% 0.75/1.19 { e3 = op( op( op( e1, e1 ), op( e1, e1 ) ), op( op( e1, e1 ), op( e1, e1 )
% 0.75/1.19 ) ) }.
% 0.75/1.19 { e4 = op( e1, e1 ) }.
% 0.75/1.19 { op( e0, e0 ) = e0, op( e1, e1 ) = e0, op( e2, e2 ) = e0, op( e3, e3 ) =
% 0.75/1.19 e0, op( e4, e4 ) = e0 }.
% 0.75/1.19 { op( e0, e0 ) = e1, op( e1, e1 ) = e1, op( e2, e2 ) = e1, op( e3, e3 ) =
% 0.75/1.19 e1, op( e4, e4 ) = e1 }.
% 0.75/1.19 { op( e0, e0 ) = e2, op( e1, e1 ) = e2, op( e2, e2 ) = e2, op( e3, e3 ) =
% 0.75/1.31 e2, op( e4, e4 ) = e2 }.
% 0.75/1.31 { op( e0, e0 ) = e3, op( e1, e1 ) = e3, op( e2, e2 ) = e3, op( e3, e3 ) =
% 0.75/1.31 e3, op( e4, e4 ) = e3 }.
% 0.75/1.31 { op( e0, e0 ) = e4, op( e1, e1 ) = e4, op( e2, e2 ) = e4, op( e3, e3 ) =
% 0.75/1.31 e4, op( e4, e4 ) = e4 }.
% 0.75/1.31 { alpha1 }.
% 0.75/1.31 { alpha2 }.
% 0.75/1.31 { alpha4 }.
% 0.75/1.31 { alpha7 }.
% 0.75/1.31 { alpha11, ! op( e4, op( e4, e4 ) ) = e4 }.
% 0.75/1.31 { alpha11, op( e4, op( e4, e4 ) ) = e4 }.
% 0.75/1.31 { ! alpha11, alpha16, ! op( e3, op( e3, e4 ) ) = e4 }.
% 0.75/1.31 { ! alpha11, alpha16, op( e4, op( e3, e4 ) ) = e3 }.
% 0.75/1.31 { ! alpha16, alpha11 }.
% 0.75/1.31 { op( e3, op( e3, e4 ) ) = e4, ! op( e4, op( e3, e4 ) ) = e3, alpha11 }.
% 0.75/1.31 { ! alpha16, alpha20, ! op( e2, op( e2, e4 ) ) = e4 }.
% 0.75/1.31 { ! alpha16, alpha20, op( e4, op( e2, e4 ) ) = e2 }.
% 0.75/1.31 { ! alpha20, alpha16 }.
% 0.75/1.31 { op( e2, op( e2, e4 ) ) = e4, ! op( e4, op( e2, e4 ) ) = e2, alpha16 }.
% 0.75/1.31 { ! alpha20, alpha23, ! op( e1, op( e1, e4 ) ) = e4 }.
% 0.75/1.31 { ! alpha20, alpha23, op( e4, op( e1, e4 ) ) = e1 }.
% 0.75/1.31 { ! alpha23, alpha20 }.
% 0.75/1.31 { op( e1, op( e1, e4 ) ) = e4, ! op( e4, op( e1, e4 ) ) = e1, alpha20 }.
% 0.75/1.31 { ! alpha23, ! op( e0, op( e0, e4 ) ) = e4 }.
% 0.75/1.31 { ! alpha23, op( e4, op( e0, e4 ) ) = e0 }.
% 0.75/1.31 { op( e0, op( e0, e4 ) ) = e4, ! op( e4, op( e0, e4 ) ) = e0, alpha23 }.
% 0.75/1.31 { ! alpha7, alpha12, ! op( e4, op( e4, e3 ) ) = e3 }.
% 0.75/1.31 { ! alpha7, alpha12, op( e3, op( e4, e3 ) ) = e4 }.
% 0.75/1.31 { ! alpha12, alpha7 }.
% 0.75/1.31 { op( e4, op( e4, e3 ) ) = e3, ! op( e3, op( e4, e3 ) ) = e4, alpha7 }.
% 0.75/1.31 { ! alpha12, alpha17, ! op( e3, op( e3, e3 ) ) = e3 }.
% 0.75/1.31 { ! alpha12, alpha17, op( e3, op( e3, e3 ) ) = e3 }.
% 0.75/1.31 { ! alpha17, alpha12 }.
% 0.75/1.31 { op( e3, op( e3, e3 ) ) = e3, ! op( e3, op( e3, e3 ) ) = e3, alpha12 }.
% 0.75/1.31 { ! alpha17, alpha21, ! op( e2, op( e2, e3 ) ) = e3 }.
% 0.75/1.31 { ! alpha17, alpha21, op( e3, op( e2, e3 ) ) = e2 }.
% 0.75/1.31 { ! alpha21, alpha17 }.
% 0.75/1.31 { op( e2, op( e2, e3 ) ) = e3, ! op( e3, op( e2, e3 ) ) = e2, alpha17 }.
% 0.75/1.31 { ! alpha21, alpha24, ! op( e1, op( e1, e3 ) ) = e3 }.
% 0.75/1.31 { ! alpha21, alpha24, op( e3, op( e1, e3 ) ) = e1 }.
% 0.75/1.31 { ! alpha24, alpha21 }.
% 0.75/1.31 { op( e1, op( e1, e3 ) ) = e3, ! op( e3, op( e1, e3 ) ) = e1, alpha21 }.
% 0.75/1.31 { ! alpha24, ! op( e0, op( e0, e3 ) ) = e3 }.
% 0.75/1.31 { ! alpha24, op( e3, op( e0, e3 ) ) = e0 }.
% 0.75/1.31 { op( e0, op( e0, e3 ) ) = e3, ! op( e3, op( e0, e3 ) ) = e0, alpha24 }.
% 0.75/1.31 { ! alpha4, alpha8, ! op( e4, op( e4, e2 ) ) = e2 }.
% 0.75/1.31 { ! alpha4, alpha8, op( e2, op( e4, e2 ) ) = e4 }.
% 0.75/1.31 { ! alpha8, alpha4 }.
% 0.75/1.31 { op( e4, op( e4, e2 ) ) = e2, ! op( e2, op( e4, e2 ) ) = e4, alpha4 }.
% 0.75/1.31 { ! alpha8, alpha13, ! op( e3, op( e3, e2 ) ) = e2 }.
% 0.75/1.31 { ! alpha8, alpha13, op( e2, op( e3, e2 ) ) = e3 }.
% 0.75/1.31 { ! alpha13, alpha8 }.
% 0.75/1.31 { op( e3, op( e3, e2 ) ) = e2, ! op( e2, op( e3, e2 ) ) = e3, alpha8 }.
% 0.75/1.31 { ! alpha13, alpha18, ! op( e2, op( e2, e2 ) ) = e2 }.
% 0.75/1.31 { ! alpha13, alpha18, op( e2, op( e2, e2 ) ) = e2 }.
% 0.75/1.31 { ! alpha18, alpha13 }.
% 0.75/1.31 { op( e2, op( e2, e2 ) ) = e2, ! op( e2, op( e2, e2 ) ) = e2, alpha13 }.
% 0.75/1.31 { ! alpha18, alpha22, ! op( e1, op( e1, e2 ) ) = e2 }.
% 0.75/1.31 { ! alpha18, alpha22, op( e2, op( e1, e2 ) ) = e1 }.
% 0.75/1.31 { ! alpha22, alpha18 }.
% 0.75/1.31 { op( e1, op( e1, e2 ) ) = e2, ! op( e2, op( e1, e2 ) ) = e1, alpha18 }.
% 0.75/1.31 { ! alpha22, ! op( e0, op( e0, e2 ) ) = e2 }.
% 0.75/1.31 { ! alpha22, op( e2, op( e0, e2 ) ) = e0 }.
% 0.75/1.31 { op( e0, op( e0, e2 ) ) = e2, ! op( e2, op( e0, e2 ) ) = e0, alpha22 }.
% 0.75/1.31 { ! alpha2, alpha5, ! op( e4, op( e4, e1 ) ) = e1 }.
% 0.75/1.31 { ! alpha2, alpha5, op( e1, op( e4, e1 ) ) = e4 }.
% 0.75/1.31 { ! alpha5, alpha2 }.
% 0.75/1.31 { op( e4, op( e4, e1 ) ) = e1, ! op( e1, op( e4, e1 ) ) = e4, alpha2 }.
% 0.75/1.31 { ! alpha5, alpha9, ! op( e3, op( e3, e1 ) ) = e1 }.
% 0.75/1.31 { ! alpha5, alpha9, op( e1, op( e3, e1 ) ) = e3 }.
% 0.75/1.31 { ! alpha9, alpha5 }.
% 0.75/1.31 { op( e3, op( e3, e1 ) ) = e1, ! op( e1, op( e3, e1 ) ) = e3, alpha5 }.
% 0.75/1.31 { ! alpha9, alpha14, ! op( e2, op( e2, e1 ) ) = e1 }.
% 0.75/1.31 { ! alpha9, alpha14, op( e1, op( e2, e1 ) ) = e2 }.
% 0.75/1.31 { ! alpha14, alpha9 }.
% 0.75/1.31 { op( e2, op( e2, e1 ) ) = e1, ! op( e1, op( e2, e1 ) ) = e2, alpha9 }.
% 0.75/1.31 { ! alpha14, alpha19, ! op( e1, op( e1, e1 ) ) = e1 }.
% 0.75/1.31 { ! alpha14, alpha19, op( e1, op( e1, e1 ) ) = e1 }.
% 0.75/1.31 { ! alpha19, alpha14 }.
% 0.75/1.31 { op( e1, op( e1, e1 ) ) = e1, ! op( e1, op( e1, e1 ) ) = e1, alpha14 }.
% 0.75/1.31 { ! alpha19, ! op( e0, op( e0, e1 ) ) = e1 }.
% 0.75/1.31 { ! alpha19, op( e1, op( e0, e1 ) ) = e0 }.
% 0.75/1.31 { op( e0, op( e0, e1 ) ) = e1, ! op( e1, op( e0, e1 ) ) = e0, alpha19 }.
% 7.02/7.46 { ! alpha1, alpha3, ! op( e4, op( e4, e0 ) ) = e0 }.
% 7.02/7.46 { ! alpha1, alpha3, op( e0, op( e4, e0 ) ) = e4 }.
% 7.02/7.46 { ! alpha3, alpha1 }.
% 7.02/7.46 { op( e4, op( e4, e0 ) ) = e0, ! op( e0, op( e4, e0 ) ) = e4, alpha1 }.
% 7.02/7.46 { ! alpha3, alpha6, ! op( e3, op( e3, e0 ) ) = e0 }.
% 7.02/7.46 { ! alpha3, alpha6, op( e0, op( e3, e0 ) ) = e3 }.
% 7.02/7.46 { ! alpha6, alpha3 }.
% 7.02/7.46 { op( e3, op( e3, e0 ) ) = e0, ! op( e0, op( e3, e0 ) ) = e3, alpha3 }.
% 7.02/7.46 { ! alpha6, alpha10, ! op( e2, op( e2, e0 ) ) = e0 }.
% 7.02/7.46 { ! alpha6, alpha10, op( e0, op( e2, e0 ) ) = e2 }.
% 7.02/7.46 { ! alpha10, alpha6 }.
% 7.02/7.46 { op( e2, op( e2, e0 ) ) = e0, ! op( e0, op( e2, e0 ) ) = e2, alpha6 }.
% 7.02/7.46 { ! alpha10, alpha15, ! op( e1, op( e1, e0 ) ) = e0 }.
% 7.02/7.46 { ! alpha10, alpha15, op( e0, op( e1, e0 ) ) = e1 }.
% 7.02/7.46 { ! alpha15, alpha10 }.
% 7.02/7.46 { op( e1, op( e1, e0 ) ) = e0, ! op( e0, op( e1, e0 ) ) = e1, alpha10 }.
% 7.02/7.46 { ! alpha15, ! op( e0, op( e0, e0 ) ) = e0 }.
% 7.02/7.46 { ! alpha15, op( e0, op( e0, e0 ) ) = e0 }.
% 7.02/7.46 { op( e0, op( e0, e0 ) ) = e0, ! op( e0, op( e0, e0 ) ) = e0, alpha15 }.
% 7.02/7.46
% 7.02/7.46 *** allocated 15000 integers for clauses
% 7.02/7.46 percentage equality = 0.815754, percentage horn = 0.596552
% 7.02/7.46 This is a pure equality problem
% 7.02/7.46
% 7.02/7.46
% 7.02/7.46
% 7.02/7.46 Options Used:
% 7.02/7.46
% 7.02/7.46 useres = 1
% 7.02/7.46 useparamod = 1
% 7.02/7.46 useeqrefl = 1
% 7.02/7.46 useeqfact = 1
% 7.02/7.46 usefactor = 1
% 7.02/7.46 usesimpsplitting = 0
% 7.02/7.46 usesimpdemod = 5
% 7.02/7.46 usesimpres = 3
% 7.02/7.46
% 7.02/7.46 resimpinuse = 1000
% 7.02/7.46 resimpclauses = 20000
% 7.02/7.46 substype = eqrewr
% 7.02/7.46 backwardsubs = 1
% 7.02/7.46 selectoldest = 5
% 7.02/7.46
% 7.02/7.46 litorderings [0] = split
% 7.02/7.46 litorderings [1] = extend the termordering, first sorting on arguments
% 7.02/7.46
% 7.02/7.46 termordering = kbo
% 7.02/7.46
% 7.02/7.46 litapriori = 0
% 7.02/7.46 termapriori = 1
% 7.02/7.46 litaposteriori = 0
% 7.02/7.46 termaposteriori = 0
% 7.02/7.46 demodaposteriori = 0
% 7.02/7.46 ordereqreflfact = 0
% 7.02/7.46
% 7.02/7.46 litselect = negord
% 7.02/7.46
% 7.02/7.46 maxweight = 15
% 7.02/7.46 maxdepth = 30000
% 7.02/7.46 maxlength = 115
% 7.02/7.46 maxnrvars = 195
% 7.02/7.46 excuselevel = 1
% 7.02/7.46 increasemaxweight = 1
% 7.02/7.46
% 7.02/7.46 maxselected = 10000000
% 7.02/7.46 maxnrclauses = 10000000
% 7.02/7.46
% 7.02/7.46 showgenerated = 0
% 7.02/7.46 showkept = 0
% 7.02/7.46 showselected = 0
% 7.02/7.46 showdeleted = 0
% 7.02/7.46 showresimp = 1
% 7.02/7.46 showstatus = 2000
% 7.02/7.46
% 7.02/7.46 prologoutput = 0
% 7.02/7.46 nrgoals = 5000000
% 7.02/7.46 totalproof = 1
% 7.02/7.46
% 7.02/7.46 Symbols occurring in the translation:
% 7.02/7.46
% 7.02/7.46 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 7.02/7.46 . [1, 2] (w:1, o:41, a:1, s:1, b:0),
% 7.02/7.46 ! [4, 1] (w:0, o:36, a:1, s:1, b:0),
% 7.02/7.46 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 7.02/7.46 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 7.02/7.46 e0 [35, 0] (w:1, o:6, a:1, s:1, b:0),
% 7.02/7.46 op [36, 2] (w:1, o:65, a:1, s:1, b:0),
% 7.02/7.46 e1 [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 7.02/7.46 e2 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 7.02/7.46 e3 [39, 0] (w:1, o:9, a:1, s:1, b:0),
% 7.02/7.46 e4 [40, 0] (w:1, o:10, a:1, s:1, b:0),
% 7.02/7.46 unit [41, 0] (w:1, o:11, a:1, s:1, b:0),
% 7.02/7.46 alpha1 [42, 0] (w:1, o:12, a:1, s:1, b:1),
% 7.02/7.46 alpha2 [43, 0] (w:1, o:23, a:1, s:1, b:1),
% 7.02/7.46 alpha3 [44, 0] (w:1, o:29, a:1, s:1, b:1),
% 7.02/7.46 alpha4 [45, 0] (w:1, o:30, a:1, s:1, b:1),
% 7.02/7.46 alpha5 [46, 0] (w:1, o:31, a:1, s:1, b:1),
% 7.02/7.46 alpha6 [47, 0] (w:1, o:32, a:1, s:1, b:1),
% 7.02/7.46 alpha7 [48, 0] (w:1, o:33, a:1, s:1, b:1),
% 7.02/7.46 alpha8 [49, 0] (w:1, o:34, a:1, s:1, b:1),
% 7.02/7.46 alpha9 [50, 0] (w:1, o:35, a:1, s:1, b:1),
% 7.02/7.46 alpha10 [51, 0] (w:1, o:13, a:1, s:1, b:1),
% 7.02/7.46 alpha11 [52, 0] (w:1, o:14, a:1, s:1, b:1),
% 7.02/7.46 alpha12 [53, 0] (w:1, o:15, a:1, s:1, b:1),
% 7.02/7.46 alpha13 [54, 0] (w:1, o:16, a:1, s:1, b:1),
% 7.02/7.46 alpha14 [55, 0] (w:1, o:17, a:1, s:1, b:1),
% 7.02/7.46 alpha15 [56, 0] (w:1, o:18, a:1, s:1, b:1),
% 7.02/7.46 alpha16 [57, 0] (w:1, o:19, a:1, s:1, b:1),
% 7.02/7.46 alpha17 [58, 0] (w:1, o:20, a:1, s:1, b:1),
% 7.02/7.46 alpha18 [59, 0] (w:1, o:21, a:1, s:1, b:1),
% 7.02/7.46 alpha19 [60, 0] (w:1, o:22, a:1, s:1, b:1),
% 7.02/7.46 alpha20 [61, 0] (w:1, o:24, a:1, s:1, b:1),
% 7.02/7.46 alpha21 [62, 0] (w:1, o:25, a:1, s:1, b:1),
% 7.02/7.46 alpha22 [63, 0] (w:1, o:26, a:1, s:1, b:1),
% 7.02/7.46 alpha23 [64, 0] (w:1, o:27, a:1, s:1, b:1),
% 7.02/7.46 alpha24 [65, 0] (w:1, o:28, a:1, s:1, b:1).
% 7.02/7.46
% 7.02/7.46
% 7.02/7.46 Starting Search:
% 7.02/7.46
% 7.02/7.46 *** allocated 22500 integers for clauses
% 7.02/7.46 *** allocated 33750 integers for clauses
% 7.02/7.46 *** allocated 22500 integers for termspace/termends
% 7.02/7.46 *** allocated 50625 integers for clauses
% 7.02/7.46 *** allocated 33750 integers for termspace/termends
% 7.02/7.46 *** allocated 75937 integers for clauses
% 7.02/7.46 Resimplifying inuse:
% 7.02/7.46 Done
% 7.02/7.46
% 7.02/7.46 *** allocated 50625 integers for termspace/termends
% 7.02/7.46 *** allocated 113905 integers for clauses
% 7.02/7.46
% 7.02/7.46 Intermediate Status:
% 7.02/7.46 Generated: 14745
% 7.02/7.46 Kept: 2000
% 7.02/7.46 Inuse: 430
% 7.02/7.46 Deleted: 132
% 7.02/7.46 Deletedinuse: 38
% 7.02/7.46
% 7.02/7.46 Resimplifying inuse:
% 7.02/7.46 Done
% 7.02/7.46
% 7.02/7.46 *** allocated 170857 integers for clauses
% 7.02/7.46 *** allocated 75937 integers for termspace/termends
% 7.02/7.46 Resimplifying inuse:
% 7.02/7.46 Done
% 7.02/7.46
% 7.02/7.46 *** allocated 256285 integers for clauses
% 7.02/7.46
% 7.02/7.46 Intermediate Status:
% 7.02/7.46 Generated: 43397
% 7.02/7.46 Kept: 4016
% 7.02/7.46 Inuse: 1014
% 7.02/7.46 Deleted: 646
% 7.02/7.46 Deletedinuse: 340
% 7.02/7.46
% 7.02/7.46 Resimplifying inuse:
% 7.02/7.46 Done
% 7.02/7.46
% 7.02/7.46 *** allocated 113905 integers for termspace/termends
% 7.02/7.46 Resimplifying inuse:
% 7.02/7.46 Done
% 7.02/7.46
% 7.02/7.46 *** allocated 384427 integers for clauses
% 7.02/7.46
% 7.02/7.46 Intermediate Status:
% 7.02/7.46 Generated: 164826
% 7.02/7.46 Kept: 6034
% 7.02/7.46 Inuse: 1815
% 7.02/7.46 Deleted: 1901
% 7.02/7.46 Deletedinuse: 586
% 7.02/7.46
% 7.02/7.46 Resimplifying inuse:
% 7.02/7.46 Done
% 7.02/7.46
% 7.02/7.46 Resimplifying inuse:
% 7.02/7.46 Done
% 7.02/7.46
% 7.02/7.46 *** allocated 170857 integers for termspace/termends
% 7.02/7.46
% 7.02/7.46 Intermediate Status:
% 7.02/7.46 Generated: 243633
% 7.02/7.46 Kept: 8057
% 7.02/7.46 Inuse: 2319
% 7.02/7.46 Deleted: 2711
% 7.02/7.46 Deletedinuse: 980
% 7.02/7.46
% 7.02/7.46 Resimplifying inuse:
% 7.02/7.46 Done
% 7.02/7.46
% 7.02/7.46
% 7.02/7.46 Bliksems!, er is een bewijs:
% 7.02/7.46 % SZS status Theorem
% 7.02/7.46 % SZS output start Refutation
% 7.02/7.46
% 7.02/7.46 (1) {G0,W25,D3,L5,V0,M5} I { op( e0, e1 ) ==> e0, op( e0, e1 ) ==> e1, op(
% 7.02/7.46 e0, e1 ) ==> e2, op( e0, e1 ) ==> e3, op( e0, e1 ) ==> e4 }.
% 7.02/7.46 (2) {G0,W25,D3,L5,V0,M5} I { op( e0, e2 ) ==> e0, op( e0, e2 ) ==> e1, op(
% 7.02/7.46 e0, e2 ) ==> e2, op( e0, e2 ) ==> e3, op( e0, e2 ) ==> e4 }.
% 7.02/7.46 (9) {G0,W25,D3,L5,V0,M5} I { op( e1, e4 ) ==> e0, op( e1, e4 ) ==> e1, op(
% 7.02/7.46 e1, e4 ) ==> e2, op( e1, e4 ) ==> e3, op( e1, e4 ) ==> e4 }.
% 7.02/7.46 (11) {G0,W25,D3,L5,V0,M5} I { op( e2, e1 ) ==> e0, op( e2, e1 ) ==> e1, op
% 7.02/7.46 ( e2, e1 ) ==> e2, op( e2, e1 ) ==> e3, op( e2, e1 ) ==> e4 }.
% 7.02/7.46 (14) {G0,W25,D3,L5,V0,M5} I { op( e2, e4 ) ==> e0, op( e2, e4 ) ==> e1, op
% 7.02/7.46 ( e2, e4 ) ==> e2, op( e2, e4 ) ==> e3, op( e2, e4 ) ==> e4 }.
% 7.02/7.46 (21) {G0,W25,D3,L5,V0,M5} I { op( e4, e1 ) ==> e0, op( e4, e1 ) ==> e1, op
% 7.02/7.46 ( e4, e1 ) ==> e2, op( e4, e1 ) ==> e3, op( e4, e1 ) ==> e4 }.
% 7.02/7.46 (22) {G0,W25,D3,L5,V0,M5} I { op( e4, e2 ) ==> e0, op( e4, e2 ) ==> e1, op
% 7.02/7.46 ( e4, e2 ) ==> e2, op( e4, e2 ) ==> e3, op( e4, e2 ) ==> e4 }.
% 7.02/7.46 (25) {G0,W5,D3,L1,V0,M1} I { op( unit, e0 ) ==> e0 }.
% 7.02/7.46 (27) {G0,W5,D3,L1,V0,M1} I { op( unit, e1 ) ==> e1 }.
% 7.02/7.46 (28) {G0,W5,D3,L1,V0,M1} I { op( e1, unit ) ==> e1 }.
% 7.02/7.46 (29) {G0,W5,D3,L1,V0,M1} I { op( unit, e2 ) ==> e2 }.
% 7.02/7.46 (30) {G0,W5,D3,L1,V0,M1} I { op( e2, unit ) ==> e2 }.
% 7.02/7.46 (33) {G0,W5,D3,L1,V0,M1} I { op( unit, e4 ) ==> e4 }.
% 7.02/7.46 (34) {G0,W5,D3,L1,V0,M1} I { op( e4, unit ) ==> e4 }.
% 7.02/7.46 (35) {G0,W15,D2,L5,V0,M5} I { unit ==> e0, unit ==> e1, unit ==> e2, unit
% 7.02/7.46 ==> e3, unit ==> e4 }.
% 7.02/7.46 (51) {G0,W25,D3,L5,V0,M5} I { op( e0, e1 ) ==> e2, op( e1, e1 ) ==> e2, op
% 7.02/7.46 ( e2, e1 ) ==> e2, op( e3, e1 ) ==> e2, op( e4, e1 ) ==> e2 }.
% 7.02/7.46 (97) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e1 ) ==> op( e0, e1 ) }.
% 7.02/7.46 (98) {G0,W7,D3,L1,V0,M1} I { ! op( e3, e1 ) ==> op( e0, e1 ) }.
% 7.02/7.46 (100) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e1 ) ==> op( e1, e1 ) }.
% 7.02/7.46 (102) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e1 ) ==> op( e1, e1 ) }.
% 7.02/7.46 (103) {G0,W7,D3,L1,V0,M1} I { ! op( e3, e1 ) ==> op( e2, e1 ) }.
% 7.02/7.46 (104) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e1 ) ==> op( e2, e1 ) }.
% 7.02/7.46 (106) {G0,W7,D3,L1,V0,M1} I { ! op( e1, e2 ) ==> op( e0, e2 ) }.
% 7.02/7.46 (107) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e2 ) ==> op( e0, e2 ) }.
% 7.02/7.46 (109) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e2 ) ==> op( e0, e2 ) }.
% 7.02/7.46 (112) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e2 ) ==> op( e1, e2 ) }.
% 7.02/7.46 (114) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e2 ) ==> op( e2, e2 ) }.
% 7.02/7.46 (127) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e4 ) ==> op( e0, e4 ) }.
% 7.02/7.46 (130) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e4 ) ==> op( e1, e4 ) }.
% 7.02/7.46 (132) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e4 ) ==> op( e1, e4 ) }.
% 7.02/7.46 (133) {G0,W7,D3,L1,V0,M1} I { ! op( e3, e4 ) ==> op( e2, e4 ) }.
% 7.02/7.46 (134) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e4 ) ==> op( e2, e4 ) }.
% 7.02/7.46 (136) {G0,W7,D3,L1,V0,M1} I { ! op( e0, e1 ) ==> op( e0, e0 ) }.
% 7.02/7.46 (140) {G0,W7,D3,L1,V0,M1} I { ! op( e0, e2 ) ==> op( e0, e1 ) }.
% 7.02/7.46 (147) {G0,W7,D3,L1,V0,M1} I { ! op( e1, e2 ) ==> op( e1, e0 ) }.
% 7.02/7.46 (151) {G0,W7,D3,L1,V0,M1} I { ! op( e1, e3 ) ==> op( e1, e1 ) }.
% 7.02/7.46 (152) {G0,W7,D3,L1,V0,M1} I { ! op( e1, e4 ) ==> op( e1, e1 ) }.
% 7.02/7.46 (154) {G0,W7,D3,L1,V0,M1} I { ! op( e1, e4 ) ==> op( e1, e2 ) }.
% 7.02/7.46 (156) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e1 ) ==> op( e2, e0 ) }.
% 7.02/7.46 (159) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e4 ) ==> op( e2, e0 ) }.
% 7.02/7.46 (160) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e2 ) ==> op( e2, e1 ) }.
% 7.02/7.46 (161) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e3 ) ==> op( e2, e1 ) }.
% 7.02/7.46 (162) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e4 ) ==> op( e2, e1 ) }.
% 7.02/7.46 (164) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e4 ) ==> op( e2, e2 ) }.
% 7.02/7.46 (177) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e2 ) ==> op( e4, e0 ) }.
% 7.02/7.46 (180) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e2 ) ==> op( e4, e1 ) }.
% 7.02/7.46 (182) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e4 ) ==> op( e4, e1 ) }.
% 7.02/7.46 (183) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e3 ) ==> op( e4, e2 ) }.
% 7.02/7.46 (184) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e4 ) ==> op( e4, e2 ) }.
% 7.02/7.46 (186) {G0,W3,D2,L1,V0,M1} I { ! e1 ==> e0 }.
% 7.02/7.46 (187) {G0,W3,D2,L1,V0,M1} I { ! e2 ==> e0 }.
% 7.02/7.46 (188) {G0,W3,D2,L1,V0,M1} I { ! e3 ==> e0 }.
% 7.02/7.46 (189) {G0,W3,D2,L1,V0,M1} I { ! e4 ==> e0 }.
% 7.02/7.46 (190) {G0,W3,D2,L1,V0,M1} I { ! e2 ==> e1 }.
% 7.02/7.46 (191) {G0,W3,D2,L1,V0,M1} I { ! e3 ==> e1 }.
% 7.02/7.46 (192) {G0,W3,D2,L1,V0,M1} I { ! e4 ==> e1 }.
% 7.02/7.46 (193) {G0,W3,D2,L1,V0,M1} I { ! e3 ==> e2 }.
% 7.02/7.46 (194) {G0,W3,D2,L1,V0,M1} I { ! e4 ==> e2 }.
% 7.02/7.46 (196) {G0,W11,D5,L1,V0,M1} I { op( e1, op( op( e1, e1 ), op( e1, e1 ) ) )
% 7.02/7.46 ==> e0 }.
% 7.02/7.46 (197) {G0,W9,D4,L1,V0,M1} I { op( op( e1, e1 ), op( e1, e1 ) ) ==> e2 }.
% 7.02/7.46 (198) {G1,W5,D3,L1,V0,M1} I;d(197) { op( e2, e2 ) ==> e3 }.
% 7.02/7.46 (199) {G0,W5,D3,L1,V0,M1} I { op( e1, e1 ) ==> e4 }.
% 7.02/7.46 (201) {G0,W1,D1,L1,V0,M1} I { alpha2 }.
% 7.02/7.46 (202) {G0,W1,D1,L1,V0,M1} I { alpha4 }.
% 7.02/7.46 (204) {G0,W8,D4,L2,V0,M2} I { alpha11, ! op( e4, op( e4, e4 ) ) ==> e4 }.
% 7.02/7.46 (205) {G0,W8,D4,L2,V0,M2} I { alpha11, op( e4, op( e4, e4 ) ) ==> e4 }.
% 7.02/7.46 (206) {G0,W9,D4,L3,V0,M3} I { ! alpha11, alpha16, ! op( e3, op( e3, e4 ) )
% 7.02/7.46 ==> e4 }.
% 7.02/7.46 (211) {G0,W9,D4,L3,V0,M3} I { ! alpha16, alpha20, op( e4, op( e2, e4 ) )
% 7.02/7.46 ==> e2 }.
% 7.02/7.46 (215) {G0,W9,D4,L3,V0,M3} I { ! alpha20, alpha23, op( e4, op( e1, e4 ) )
% 7.02/7.46 ==> e1 }.
% 7.02/7.46 (218) {G0,W8,D4,L2,V0,M2} I { ! alpha23, ! op( e0, op( e0, e4 ) ) ==> e4
% 7.02/7.46 }.
% 7.02/7.46 (237) {G1,W8,D4,L2,V0,M2} I;r(202) { alpha8, ! op( e4, op( e4, e2 ) ) ==>
% 7.02/7.46 e2 }.
% 7.02/7.46 (238) {G1,W8,D4,L2,V0,M2} I;r(202) { alpha8, op( e2, op( e4, e2 ) ) ==> e4
% 7.02/7.46 }.
% 7.02/7.46 (239) {G0,W9,D4,L3,V0,M3} I { ! alpha8, alpha13, ! op( e3, op( e3, e2 ) )
% 7.02/7.46 ==> e2 }.
% 7.02/7.46 (243) {G2,W7,D3,L3,V0,M3} I;d(198) { ! alpha13, alpha18, ! op( e2, e3 ) ==>
% 7.02/7.46 e2 }.
% 7.02/7.46 (244) {G2,W7,D3,L3,V0,M3} I;d(198) { ! alpha13, alpha18, op( e2, e3 ) ==>
% 7.02/7.46 e2 }.
% 7.02/7.46 (247) {G0,W9,D4,L3,V0,M3} I { ! alpha18, alpha22, op( e2, op( e1, e2 ) )
% 7.02/7.46 ==> e1 }.
% 7.02/7.46 (251) {G0,W8,D4,L2,V0,M2} I { ! alpha22, op( e2, op( e0, e2 ) ) ==> e0 }.
% 7.02/7.46 (253) {G1,W8,D4,L2,V0,M2} I;r(201) { alpha5, ! op( e4, op( e4, e1 ) ) ==>
% 7.02/7.46 e1 }.
% 7.02/7.46 (254) {G1,W8,D4,L2,V0,M2} I;r(201) { alpha5, op( e1, op( e4, e1 ) ) ==> e4
% 7.02/7.46 }.
% 7.02/7.46 (255) {G0,W9,D4,L3,V0,M3} I { ! alpha5, alpha9, ! op( e3, op( e3, e1 ) )
% 7.02/7.46 ==> e1 }.
% 7.02/7.46 (256) {G0,W9,D4,L3,V0,M3} I { ! alpha5, alpha9, op( e1, op( e3, e1 ) ) ==>
% 7.02/7.46 e3 }.
% 7.02/7.46 (257) {G0,W2,D1,L2,V0,M2} I { ! alpha9, alpha5 }.
% 7.02/7.46 (259) {G0,W9,D4,L3,V0,M3} I { ! alpha9, alpha14, ! op( e2, op( e2, e1 ) )
% 7.02/7.46 ==> e1 }.
% 7.02/7.46 (260) {G0,W9,D4,L3,V0,M3} I { ! alpha9, alpha14, op( e1, op( e2, e1 ) ) ==>
% 7.02/7.46 e2 }.
% 7.02/7.46 (263) {G1,W7,D3,L3,V0,M3} I;d(199) { ! alpha14, alpha19, ! op( e1, e4 ) ==>
% 7.02/7.46 e1 }.
% 7.02/7.46 (264) {G1,W7,D3,L3,V0,M3} I;d(199) { ! alpha14, alpha19, op( e1, e4 ) ==>
% 7.02/7.46 e1 }.
% 7.02/7.46 (265) {G0,W2,D1,L2,V0,M2} I { ! alpha19, alpha14 }.
% 7.02/7.46 (266) {G0,W8,D4,L2,V0,M2} I { ! alpha19, ! op( e0, op( e0, e1 ) ) ==> e1
% 7.02/7.46 }.
% 7.02/7.46 (267) {G0,W8,D4,L2,V0,M2} I { ! alpha19, op( e1, op( e0, e1 ) ) ==> e0 }.
% 7.02/7.46 (268) {G0,W15,D4,L3,V0,M3} I { op( e0, op( e0, e1 ) ) ==> e1, ! op( e1, op
% 7.02/7.46 ( e0, e1 ) ) ==> e0, alpha19 }.
% 7.02/7.46 (271) {G0,W9,D4,L3,V0,M3} I { ! alpha3, alpha6, ! op( e3, op( e3, e0 ) )
% 7.02/7.46 ==> e0 }.
% 7.02/7.46 (273) {G0,W2,D1,L2,V0,M2} I { ! alpha6, alpha3 }.
% 7.02/7.46 (275) {G0,W9,D4,L3,V0,M3} I { ! alpha6, alpha10, ! op( e2, op( e2, e0 ) )
% 7.02/7.46 ==> e0 }.
% 7.02/7.46 (277) {G0,W2,D1,L2,V0,M2} I { ! alpha10, alpha6 }.
% 7.02/7.46 (278) {G0,W15,D4,L3,V0,M3} I { op( e2, op( e2, e0 ) ) ==> e0, ! op( e0, op
% 7.02/7.46 ( e2, e0 ) ) ==> e2, alpha6 }.
% 7.02/7.46 (279) {G0,W9,D4,L3,V0,M3} I { ! alpha10, alpha15, ! op( e1, op( e1, e0 ) )
% 7.02/7.46 ==> e0 }.
% 7.02/7.46 (282) {G0,W15,D4,L3,V0,M3} I { op( e1, op( e1, e0 ) ) ==> e0, ! op( e0, op
% 7.02/7.46 ( e1, e0 ) ) ==> e1, alpha10 }.
% 7.02/7.46 (283) {G0,W8,D4,L2,V0,M2} I { ! alpha15, ! op( e0, op( e0, e0 ) ) ==> e0
% 7.02/7.46 }.
% 7.02/7.46 (284) {G0,W8,D4,L2,V0,M2} I { ! alpha15, op( e0, op( e0, e0 ) ) ==> e0 }.
% 7.02/7.46 (335) {G2,W5,D3,L1,V0,M1} S(164);d(198) { ! op( e2, e4 ) ==> e3 }.
% 7.02/7.46 (359) {G2,W5,D3,L1,V0,M1} S(160);d(198) { ! op( e2, e1 ) ==> e3 }.
% 7.02/7.46 (393) {G1,W5,D3,L1,V0,M1} S(152);d(199) { ! op( e1, e4 ) ==> e4 }.
% 7.02/7.46 (394) {G1,W5,D3,L1,V0,M1} S(151);d(199) { ! op( e1, e3 ) ==> e4 }.
% 7.02/7.46 (450) {G1,W12,D2,L4,V0,M4} P(35,27);d(199);r(192) { unit ==> e0, unit ==>
% 7.02/7.46 e2, unit ==> e3, unit ==> e4 }.
% 7.02/7.46 (452) {G2,W14,D3,L4,V0,M4} P(35,27);d(450);r(191) { op( e3, e1 ) ==> e1,
% 7.02/7.46 unit ==> e0, unit ==> e2, unit ==> e4 }.
% 7.02/7.46 (457) {G2,W12,D2,L4,V0,M4} P(35,29);d(198);d(450);r(193) { unit ==> e0,
% 7.02/7.46 unit ==> e3, unit ==> e4, e2 ==> e1 }.
% 7.02/7.46 (459) {G2,W14,D3,L4,V0,M4} P(35,29);d(450);r(192) { op( e4, e2 ) ==> e2,
% 7.02/7.46 unit ==> e0, unit ==> e2, unit ==> e3 }.
% 7.02/7.46 (496) {G1,W25,D3,L5,V0,M5} P(2,140) { ! op( e0, e1 ) ==> e2, op( e0, e2 )
% 7.02/7.46 ==> e0, op( e0, e2 ) ==> e1, op( e0, e2 ) ==> e3, op( e0, e2 ) ==> e4 }.
% 7.02/7.46 (680) {G2,W5,D3,L1,V0,M1} S(114);d(198) { ! op( e4, e2 ) ==> e3 }.
% 7.02/7.46 (721) {G2,W5,D3,L1,V0,M1} S(107);d(198) { ! op( e0, e2 ) ==> e3 }.
% 7.02/7.46 (736) {G1,W5,D3,L1,V0,M1} S(102);d(199) { ! op( e4, e1 ) ==> e4 }.
% 7.02/7.46 (739) {G1,W5,D3,L1,V0,M1} S(100);d(199) { ! op( e2, e1 ) ==> e4 }.
% 7.02/7.46 (740) {G3,W15,D3,L3,V0,M3} R(739,11);r(359) { op( e2, e1 ) ==> e0, op( e2,
% 7.02/7.46 e1 ) ==> e1, op( e2, e1 ) ==> e2 }.
% 7.02/7.46 (795) {G1,W20,D3,L4,V0,M4} S(51);d(199);r(194) { op( e0, e1 ) ==> e2, op(
% 7.02/7.46 e2, e1 ) ==> e2, op( e3, e1 ) ==> e2, op( e4, e1 ) ==> e2 }.
% 7.02/7.46 (812) {G2,W2,D1,L2,V0,M2} S(264);r(263) { ! alpha14, alpha19 }.
% 7.02/7.46 (813) {G3,W2,D1,L2,V0,M2} S(244);r(243) { ! alpha13, alpha18 }.
% 7.02/7.46 (814) {G1,W1,D1,L1,V0,M1} S(284);r(283) { ! alpha15 }.
% 7.02/7.46 (815) {G3,W8,D4,L2,V0,M2} R(267,812) { op( e1, op( e0, e1 ) ) ==> e0, !
% 7.02/7.46 alpha14 }.
% 7.02/7.46 (820) {G1,W26,D3,L6,V0,M6} P(1,267) { ! alpha19, op( e1, e4 ) ==> e0, op(
% 7.02/7.46 e0, e1 ) ==> e0, op( e0, e1 ) ==> e1, op( e0, e1 ) ==> e2, op( e0, e1 )
% 7.02/7.46 ==> e3 }.
% 7.02/7.46 (821) {G3,W8,D4,L2,V0,M2} R(266,812) { ! op( e0, op( e0, e1 ) ) ==> e1, !
% 7.02/7.46 alpha14 }.
% 7.02/7.46 (857) {G1,W1,D1,L1,V0,M1} S(205);r(204) { alpha11 }.
% 7.02/7.46 (858) {G1,W5,D3,L1,V0,M1} S(197);d(199) { op( e4, e4 ) ==> e2 }.
% 7.02/7.46 (860) {G2,W5,D3,L1,V0,M1} P(858,132) { ! op( e1, e4 ) ==> e2 }.
% 7.02/7.46 (861) {G2,W5,D3,L1,V0,M1} P(858,134) { ! op( e2, e4 ) ==> e2 }.
% 7.02/7.46 (864) {G2,W5,D3,L1,V0,M1} P(858,182) { ! op( e4, e1 ) ==> e2 }.
% 7.02/7.46 (865) {G2,W5,D3,L1,V0,M1} P(858,184) { ! op( e4, e2 ) ==> e2 }.
% 7.02/7.46 (867) {G3,W15,D3,L3,V0,M3} R(860,9);r(393) { op( e1, e4 ) ==> e0, op( e1,
% 7.02/7.46 e4 ) ==> e1, op( e1, e4 ) ==> e3 }.
% 7.02/7.46 (868) {G3,W15,D3,L3,V0,M3} R(861,14);r(335) { op( e2, e4 ) ==> e0, op( e2,
% 7.02/7.46 e4 ) ==> e1, op( e2, e4 ) ==> e4 }.
% 7.02/7.46 (869) {G3,W15,D3,L3,V0,M3} R(864,21);r(736) { op( e4, e1 ) ==> e0, op( e4,
% 7.02/7.46 e1 ) ==> e1, op( e4, e1 ) ==> e3 }.
% 7.02/7.46 (870) {G3,W15,D3,L3,V0,M3} R(865,22);r(680) { op( e4, e2 ) ==> e0, op( e4,
% 7.02/7.46 e2 ) ==> e1, op( e4, e2 ) ==> e4 }.
% 7.02/7.46 (872) {G2,W8,D4,L2,V0,M2} S(279);r(814) { ! alpha10, ! op( e1, op( e1, e0 )
% 7.02/7.46 ) ==> e0 }.
% 7.02/7.46 (906) {G3,W9,D4,L3,V0,M3} R(260,812) { ! alpha9, op( e1, op( e2, e1 ) ) ==>
% 7.02/7.46 e2, alpha19 }.
% 7.02/7.46 (909) {G3,W9,D4,L3,V0,M3} R(259,812) { ! alpha9, ! op( e2, op( e2, e1 ) )
% 7.02/7.46 ==> e1, alpha19 }.
% 7.02/7.46 (913) {G2,W15,D4,L3,V0,M3} R(256,254) { alpha9, op( e1, op( e3, e1 ) ) ==>
% 7.02/7.46 e3, op( e1, op( e4, e1 ) ) ==> e4 }.
% 7.02/7.46 (966) {G4,W9,D4,L3,V0,M3} R(239,813) { ! alpha8, ! op( e3, op( e3, e2 ) )
% 7.02/7.46 ==> e2, alpha18 }.
% 7.02/7.46 (1100) {G2,W8,D4,L2,V0,M2} S(206);r(857) { alpha16, ! op( e3, op( e3, e4 )
% 7.02/7.46 ) ==> e4 }.
% 7.02/7.46 (1103) {G2,W5,D3,L1,V0,M1} S(196);d(199);d(858) { op( e1, e2 ) ==> e0 }.
% 7.02/7.46 (1107) {G3,W7,D3,L3,V0,M3} P(1103,247) { ! alpha18, alpha22, op( e2, e0 )
% 7.02/7.46 ==> e1 }.
% 7.02/7.46 (1108) {G3,W5,D3,L1,V0,M1} P(1103,106) { ! op( e0, e2 ) ==> e0 }.
% 7.02/7.46 (1109) {G3,W5,D3,L1,V0,M1} P(1103,147) { ! op( e1, e0 ) ==> e0 }.
% 7.02/7.46 (1140) {G4,W9,D3,L5,V0,M5} P(1107,275) { ! alpha6, alpha10, ! op( e2, e1 )
% 7.02/7.46 ==> e0, ! alpha18, alpha22 }.
% 7.02/7.46 (1172) {G3,W12,D2,L4,V0,M4} S(450);d(457) { unit ==> e0, unit ==> e3, unit
% 7.02/7.46 ==> e4, unit ==> e1 }.
% 7.02/7.46 (1176) {G4,W9,D2,L3,V0,M3} P(1172,25);r(1109) { unit ==> e0, unit ==> e3,
% 7.02/7.46 unit ==> e4 }.
% 7.02/7.46 (1180) {G4,W11,D3,L3,V0,M3} P(1172,27);d(452);r(190) { op( e3, e1 ) ==> e1
% 7.02/7.46 , unit ==> e0, unit ==> e4 }.
% 7.02/7.46 (1187) {G4,W9,D2,L3,V0,M3} P(1172,29);d(459);r(865) { unit ==> e0, unit ==>
% 7.02/7.46 e3, e2 ==> e1 }.
% 7.02/7.46 (1196) {G5,W9,D2,L3,V0,M3} P(1172,33);d(858);d(1176);d(1187);r(192) { unit
% 7.02/7.46 ==> e0, unit ==> e3, e4 ==> e1 }.
% 7.02/7.46 (1199) {G6,W9,D2,L3,V0,M3} S(1176);d(1196) { unit ==> e0, unit ==> e3, unit
% 7.02/7.46 ==> e1 }.
% 7.02/7.46 (1202) {G7,W6,D2,L2,V0,M2} P(1199,25);r(1109) { unit ==> e0, unit ==> e3
% 7.02/7.46 }.
% 7.02/7.46 (1205) {G7,W8,D3,L2,V0,M2} P(1199,27);d(1180);r(192) { op( e3, e1 ) ==> e1
% 7.02/7.46 , unit ==> e0 }.
% 7.02/7.46 (1211) {G8,W8,D3,L2,V0,M2} P(1199,30);d(1202);r(191) { op( e2, e3 ) ==> e2
% 7.02/7.46 , unit ==> e0 }.
% 7.02/7.46 (1216) {G8,W8,D3,L2,V0,M2} P(1199,33);d(1202);r(191) { op( e3, e4 ) ==> e4
% 7.02/7.46 , unit ==> e0 }.
% 7.02/7.46 (1218) {G8,W8,D3,L2,V0,M2} P(1199,34);d(1202);r(191) { op( e4, e3 ) ==> e4
% 7.02/7.46 , unit ==> e0 }.
% 7.02/7.46 (1220) {G8,W8,D3,L2,V0,M2} P(1202,25) { op( e3, e0 ) ==> e0, unit ==> e0
% 7.02/7.46 }.
% 7.02/7.46 (1221) {G8,W8,D3,L2,V0,M2} P(1202,27) { op( e0, e1 ) ==> e1, unit ==> e3
% 7.02/7.46 }.
% 7.02/7.46 (1222) {G8,W8,D3,L2,V0,M2} P(1202,28) { op( e1, e0 ) ==> e1, unit ==> e3
% 7.02/7.46 }.
% 7.02/7.46 (1227) {G8,W8,D3,L2,V0,M2} P(1202,33) { op( e0, e4 ) ==> e4, unit ==> e3
% 7.02/7.46 }.
% 7.02/7.46 (1238) {G9,W5,D2,L3,V0,M3} P(1220,271);d(1220);q { ! alpha3, alpha6, unit
% 7.02/7.46 ==> e0 }.
% 7.02/7.46 (1267) {G10,W7,D3,L3,V0,M3} P(1238,29) { op( e0, e2 ) ==> e2, ! alpha3,
% 7.02/7.46 alpha6 }.
% 7.02/7.46 (1268) {G10,W7,D3,L3,V0,M3} P(1238,30) { op( e2, e0 ) ==> e2, ! alpha3,
% 7.02/7.46 alpha6 }.
% 7.02/7.46 (1427) {G9,W4,D2,L2,V0,M2} P(1221,821);d(1221);q { ! alpha14, unit ==> e3
% 7.02/7.46 }.
% 7.02/7.46 (1428) {G9,W4,D2,L2,V0,M2} P(1221,266);d(1221);q { ! alpha19, unit ==> e3
% 7.02/7.46 }.
% 7.02/7.46 (1444) {G10,W6,D3,L2,V0,M2} P(1427,28) { op( e1, e3 ) ==> e1, ! alpha14 }.
% 7.02/7.46 (1454) {G10,W6,D3,L2,V0,M2} P(1428,27) { op( e3, e1 ) ==> e1, ! alpha19 }.
% 7.02/7.46 (1456) {G10,W6,D3,L2,V0,M2} P(1428,29) { op( e3, e2 ) ==> e2, ! alpha19 }.
% 7.02/7.46 (1459) {G10,W6,D3,L2,V0,M2} P(1428,33) { op( e3, e4 ) ==> e4, ! alpha19 }.
% 7.02/7.46 (1460) {G10,W6,D3,L2,V0,M2} P(1428,34) { op( e4, e3 ) ==> e4, ! alpha19 }.
% 7.02/7.46 (1476) {G11,W6,D3,L2,V0,M2} P(1454,98) { ! op( e0, e1 ) ==> e1, ! alpha19
% 7.02/7.46 }.
% 7.02/7.46 (1495) {G11,W3,D1,L3,V0,M3} P(1456,966);d(1456);q { ! alpha8, alpha18, !
% 7.02/7.46 alpha19 }.
% 7.02/7.46 (1508) {G12,W9,D4,L3,V0,M3} R(1495,237) { alpha18, ! alpha19, ! op( e4, op
% 7.02/7.46 ( e4, e2 ) ) ==> e2 }.
% 7.02/7.46 (1509) {G12,W9,D4,L3,V0,M3} R(1495,238) { alpha18, ! alpha19, op( e2, op(
% 7.02/7.46 e4, e2 ) ) ==> e4 }.
% 7.02/7.46 (1569) {G11,W2,D1,L2,V0,M2} P(1459,1100);d(1459);q { alpha16, ! alpha19 }.
% 7.02/7.46 (1571) {G11,W6,D3,L2,V0,M2} P(1459,133) { ! op( e2, e4 ) ==> e4, ! alpha19
% 7.02/7.46 }.
% 7.02/7.46 (1574) {G12,W9,D4,L3,V0,M3} R(1569,909) { alpha16, ! alpha9, ! op( e2, op(
% 7.02/7.46 e2, e1 ) ) ==> e1 }.
% 7.02/7.46 (1575) {G12,W9,D4,L3,V0,M3} R(1569,906) { alpha16, ! alpha9, op( e1, op( e2
% 7.02/7.46 , e1 ) ) ==> e2 }.
% 7.02/7.46 (1591) {G11,W6,D3,L2,V0,M2} P(1460,183) { ! op( e4, e2 ) ==> e4, ! alpha19
% 7.02/7.46 }.
% 7.02/7.46 (1605) {G1,W15,D4,L3,V0,M3} R(268,265) { op( e0, op( e0, e1 ) ) ==> e1, !
% 7.02/7.46 op( e1, op( e0, e1 ) ) ==> e0, alpha14 }.
% 7.02/7.46 (1612) {G11,W2,D1,L2,V0,M2} P(1268,278);f;d(198);d(1267);q;r(188) { alpha6
% 7.02/7.46 , ! alpha3 }.
% 7.02/7.46 (2012) {G3,W5,D3,L1,V0,M1} S(112);d(1103) { ! op( e4, e2 ) ==> e0 }.
% 7.02/7.46 (2014) {G3,W5,D3,L1,V0,M1} S(154);d(1103) { ! op( e1, e4 ) ==> e0 }.
% 7.02/7.46 (2603) {G9,W4,D2,L2,V0,M2} P(1222,282);d(199);d(1221);q;r(189) { alpha10,
% 7.02/7.46 unit ==> e3 }.
% 7.02/7.46 (2613) {G10,W4,D2,L2,V0,M2} R(2603,277) { unit ==> e3, alpha6 }.
% 7.02/7.46 (2618) {G10,W6,D3,L2,V0,M2} P(2603,27) { op( e3, e1 ) ==> e1, alpha10 }.
% 7.02/7.46 (2620) {G10,W6,D3,L2,V0,M2} P(2603,29) { op( e3, e2 ) ==> e2, alpha10 }.
% 7.02/7.46 (2621) {G10,W6,D3,L2,V0,M2} P(2603,30) { op( e2, e3 ) ==> e2, alpha10 }.
% 7.02/7.46 (2623) {G10,W6,D3,L2,V0,M2} P(2603,33) { op( e3, e4 ) ==> e4, alpha10 }.
% 7.02/7.46 (2624) {G10,W6,D3,L2,V0,M2} P(2603,34) { op( e4, e3 ) ==> e4, alpha10 }.
% 7.02/7.46 (2640) {G11,W6,D3,L2,V0,M2} P(2613,27) { op( e3, e1 ) ==> e1, alpha6 }.
% 7.02/7.46 (2945) {G12,W3,D1,L3,V0,M3} P(2640,255);d(2640);q { ! alpha5, alpha9,
% 7.02/7.46 alpha6 }.
% 7.02/7.46 (2956) {G13,W3,D1,L3,V0,M3} R(2945,273) { ! alpha5, alpha9, alpha3 }.
% 7.02/7.46 (2958) {G14,W10,D4,L4,V0,M4} R(2956,259) { ! alpha5, alpha3, alpha14, ! op
% 7.02/7.46 ( e2, op( e2, e1 ) ) ==> e1 }.
% 7.02/7.46 (3077) {G11,W6,D3,L2,V0,M2} P(2618,103) { ! op( e2, e1 ) ==> e1, alpha10
% 7.02/7.46 }.
% 7.02/7.46 (3102) {G11,W3,D1,L3,V0,M3} P(2620,966);d(2620);q { ! alpha8, alpha18,
% 7.02/7.46 alpha10 }.
% 7.02/7.46 (3114) {G12,W9,D3,L5,V0,M5} R(3102,1140);f { ! alpha8, alpha10, ! alpha6, !
% 7.02/7.46 op( e2, e1 ) ==> e0, alpha22 }.
% 7.02/7.46 (3115) {G12,W8,D3,L4,V0,M4} R(3102,1107) { ! alpha8, alpha10, alpha22, op(
% 7.02/7.46 e2, e0 ) ==> e1 }.
% 7.02/7.46 (3135) {G11,W6,D3,L2,V0,M2} P(2621,161) { ! op( e2, e1 ) ==> e2, alpha10
% 7.02/7.46 }.
% 7.02/7.46 (3142) {G11,W6,D3,L2,V0,M2} P(2623,133) { ! op( e2, e4 ) ==> e4, alpha10
% 7.02/7.46 }.
% 7.02/7.46 (3310) {G9,W4,D2,L2,V0,M2} P(1227,218);d(1227);q { ! alpha23, unit ==> e3
% 7.02/7.46 }.
% 7.02/7.46 (3325) {G10,W6,D3,L2,V0,M2} P(3310,27) { op( e3, e1 ) ==> e1, ! alpha23 }.
% 7.02/7.46 (3326) {G10,W6,D3,L2,V0,M2} P(3310,28) { op( e1, e3 ) ==> e1, ! alpha23 }.
% 7.02/7.46 (3331) {G10,W6,D3,L2,V0,M2} P(3310,34) { op( e4, e3 ) ==> e4, ! alpha23 }.
% 7.02/7.46 (3346) {G11,W3,D1,L3,V0,M3} P(3325,255);d(3325);q { ! alpha5, alpha9, !
% 7.02/7.46 alpha23 }.
% 7.02/7.46 (3355) {G12,W9,D4,L3,V0,M3} R(3346,253) { alpha9, ! alpha23, ! op( e4, op(
% 7.02/7.46 e4, e1 ) ) ==> e1 }.
% 7.02/7.46 (3356) {G12,W9,D4,L3,V0,M3} R(3346,254) { alpha9, ! alpha23, op( e1, op( e4
% 7.02/7.46 , e1 ) ) ==> e4 }.
% 7.02/7.46 (3458) {G8,W5,D2,L3,V0,M3} P(1205,255);d(1205);q { ! alpha5, alpha9, unit
% 7.02/7.46 ==> e0 }.
% 7.02/7.46 (3460) {G8,W8,D3,L2,V0,M2} P(1205,103) { ! op( e2, e1 ) ==> e1, unit ==> e0
% 7.02/7.46 }.
% 7.02/7.46 (3477) {G9,W7,D3,L3,V0,M3} P(3458,27) { op( e0, e1 ) ==> e1, ! alpha5,
% 7.02/7.46 alpha9 }.
% 7.02/7.46 (3565) {G9,W10,D3,L2,V0,M2} P(3460,27) { op( e0, e1 ) ==> e1, ! op( e2, e1
% 7.02/7.46 ) ==> e1 }.
% 7.02/7.46 (3568) {G9,W10,D3,L2,V0,M2} P(3460,30) { op( e2, e0 ) ==> e2, ! op( e2, e1
% 7.02/7.46 ) ==> e1 }.
% 7.02/7.46 (3906) {G9,W8,D3,L2,V0,M2} P(1211,161) { ! op( e2, e1 ) ==> e2, unit ==> e0
% 7.02/7.46 }.
% 7.02/7.46 (3933) {G10,W10,D3,L2,V0,M2} P(3906,27) { op( e0, e1 ) ==> e1, ! op( e2, e1
% 7.02/7.46 ) ==> e2 }.
% 7.02/7.46 (3936) {G10,W10,D3,L2,V0,M2} P(3906,30) { op( e2, e0 ) ==> e2, ! op( e2, e1
% 7.02/7.46 ) ==> e2 }.
% 7.02/7.46 (3941) {G9,W4,D2,L2,V0,M2} P(1216,1100);d(1216);q { alpha16, unit ==> e0
% 7.02/7.46 }.
% 7.02/7.46 (3943) {G9,W8,D3,L2,V0,M2} P(1216,133) { ! op( e2, e4 ) ==> e4, unit ==> e0
% 7.02/7.46 }.
% 7.02/7.46 (3957) {G10,W6,D3,L2,V0,M2} P(3941,28) { op( e1, e0 ) ==> e1, alpha16 }.
% 7.02/7.46 (3959) {G10,W6,D3,L2,V0,M2} P(3941,30) { op( e2, e0 ) ==> e2, alpha16 }.
% 7.02/7.46 (4014) {G10,W10,D3,L2,V0,M2} P(3943,33) { op( e0, e4 ) ==> e4, ! op( e2, e4
% 7.02/7.46 ) ==> e4 }.
% 7.02/7.46 (4017) {G9,W8,D3,L2,V0,M2} P(1218,183) { ! op( e4, e2 ) ==> e4, unit ==> e0
% 7.02/7.46 }.
% 7.02/7.46 (4051) {G10,W10,D3,L2,V0,M2} P(4017,34) { op( e4, e0 ) ==> e4, ! op( e4, e2
% 7.02/7.46 ) ==> e4 }.
% 7.02/7.46 (4127) {G4,W15,D3,L3,V0,M3} S(496);r(1108);r(721) { ! op( e0, e1 ) ==> e2,
% 7.02/7.46 op( e0, e2 ) ==> e1, op( e0, e2 ) ==> e4 }.
% 7.02/7.46 (4230) {G13,W9,D3,L5,V0,M5} R(3114,1612) { ! alpha8, alpha10, ! op( e2, e1
% 7.02/7.46 ) ==> e0, alpha22, ! alpha3 }.
% 7.02/7.46 (4512) {G11,W10,D3,L2,V0,M2} R(740,3568);r(3936) { op( e2, e1 ) ==> e0, op
% 7.02/7.46 ( e2, e0 ) ==> e2 }.
% 7.02/7.46 (4515) {G11,W10,D3,L2,V0,M2} R(740,3565);r(3933) { op( e2, e1 ) ==> e0, op
% 7.02/7.46 ( e0, e1 ) ==> e1 }.
% 7.02/7.46 (4524) {G12,W6,D3,L2,V0,M2} R(740,3135);r(3077) { op( e2, e1 ) ==> e0,
% 7.02/7.46 alpha10 }.
% 7.02/7.46 (4588) {G12,W10,D3,L2,V0,M2} P(740,97);d(4515);q { op( e2, e1 ) ==> e0, op
% 7.02/7.46 ( e2, e1 ) ==> e2 }.
% 7.02/7.46 (4590) {G13,W5,D3,L1,V0,M1} P(740,156);d(4512);d(4588);q;r(190) { op( e2,
% 7.02/7.46 e1 ) ==> e0 }.
% 7.02/7.46 (4593) {G14,W4,D1,L4,V0,M4} R(4590,4230) { ! alpha8, alpha10, alpha22, !
% 7.02/7.46 alpha3 }.
% 7.02/7.46 (4639) {G14,W5,D2,L3,V0,M3} P(4590,1575);d(3957) { alpha16, ! alpha9, e2
% 7.02/7.46 ==> e1 }.
% 7.02/7.46 (4640) {G15,W2,D1,L2,V0,M2} P(4590,1574);d(3959);d(4639);q { alpha16, !
% 7.02/7.46 alpha9 }.
% 7.02/7.46 (4644) {G14,W7,D3,L3,V0,M3} P(4590,906) { ! alpha9, op( e1, e0 ) ==> e2,
% 7.02/7.46 alpha19 }.
% 7.02/7.46 (4645) {G14,W7,D3,L3,V0,M3} P(4590,260) { ! alpha9, alpha14, op( e1, e0 )
% 7.02/7.46 ==> e2 }.
% 7.02/7.46 (4646) {G14,W5,D3,L1,V0,M1} P(4590,97) { ! op( e0, e1 ) ==> e0 }.
% 7.02/7.46 (4657) {G16,W9,D4,L3,V0,M3} R(4640,211) { ! alpha9, alpha20, op( e4, op( e2
% 7.02/7.46 , e4 ) ) ==> e2 }.
% 7.02/7.46 (4714) {G15,W5,D1,L5,V0,M5} R(4593,2958);d(4524);d(3115);q { ! alpha8,
% 7.02/7.46 alpha10, alpha22, ! alpha5, alpha14 }.
% 7.02/7.46 (4747) {G16,W5,D1,L5,V0,M5} R(4714,257) { ! alpha8, alpha10, alpha22,
% 7.02/7.46 alpha14, ! alpha9 }.
% 7.02/7.46 (4754) {G17,W4,D1,L4,V0,M4} R(4747,872);d(4645);d(1103);q { ! alpha8,
% 7.02/7.46 alpha22, alpha14, ! alpha9 }.
% 7.02/7.46 (4803) {G18,W4,D1,L4,V0,M4} R(4754,812) { ! alpha8, alpha22, ! alpha9,
% 7.02/7.46 alpha19 }.
% 7.02/7.46 (4907) {G19,W10,D4,L4,V0,M4} R(4803,251) { ! alpha8, ! alpha9, alpha19, op
% 7.02/7.46 ( e2, op( e0, e2 ) ) ==> e0 }.
% 7.02/7.46 (5020) {G14,W5,D3,L1,V0,M1} S(104);d(4590) { ! op( e4, e1 ) ==> e0 }.
% 7.02/7.46 (5022) {G14,W5,D3,L1,V0,M1} S(162);d(4590) { ! op( e2, e4 ) ==> e0 }.
% 7.02/7.46 (5157) {G15,W3,D1,L3,V0,M3} P(4644,872);d(1103);q { ! alpha10, ! alpha9,
% 7.02/7.46 alpha19 }.
% 7.02/7.46 (5192) {G16,W6,D3,L2,V0,M2} R(5157,2624);r(1460) { ! alpha9, op( e4, e3 )
% 7.02/7.46 ==> e4 }.
% 7.02/7.46 (5193) {G16,W6,D3,L2,V0,M2} R(5157,3142);r(1571) { ! alpha9, ! op( e2, e4 )
% 7.02/7.46 ==> e4 }.
% 7.02/7.46 (5218) {G16,W3,D1,L3,V0,M3} R(5157,265) { ! alpha10, ! alpha9, alpha14 }.
% 7.02/7.46 (5247) {G17,W4,D1,L4,V0,M4} R(5218,3346) { ! alpha10, alpha14, ! alpha5, !
% 7.02/7.46 alpha23 }.
% 7.02/7.46 (5690) {G14,W13,D3,L3,V0,M3} S(795);d(4590);r(864) { op( e0, e1 ) ==> e2,
% 7.02/7.46 op( e3, e1 ) ==> e2, e2 ==> e0 }.
% 7.02/7.46 (5833) {G15,W11,D3,L3,V0,M3} S(820);r(2014);r(4646);r(1476) { ! alpha19, op
% 7.02/7.46 ( e0, e1 ) ==> e2, op( e0, e1 ) ==> e3 }.
% 7.02/7.46 (5890) {G16,W9,D3,L3,V0,M3} P(5833,815);d(1444);r(265) { ! alpha19, op( e0
% 7.02/7.46 , e1 ) ==> e2, e1 ==> e0 }.
% 7.02/7.46 (5892) {G16,W11,D3,L3,V0,M3} P(5833,136) { ! op( e0, e0 ) ==> e3, ! alpha19
% 7.02/7.46 , op( e0, e1 ) ==> e2 }.
% 7.02/7.46 (6034) {G17,W6,D3,L2,V0,M2} S(5833);d(5890);r(5892) { ! alpha19, op( e0, e1
% 7.02/7.46 ) ==> e2 }.
% 7.02/7.46 (6099) {G18,W6,D3,L2,V0,M2} R(6034,812) { op( e0, e1 ) ==> e2, ! alpha14
% 7.02/7.46 }.
% 7.02/7.46 (6293) {G4,W10,D3,L2,V0,M2} S(867);r(2014) { op( e1, e4 ) ==> e1, op( e1,
% 7.02/7.46 e4 ) ==> e3 }.
% 7.02/7.46 (6294) {G15,W10,D3,L2,V0,M2} S(868);r(5022) { op( e2, e4 ) ==> e1, op( e2,
% 7.02/7.46 e4 ) ==> e4 }.
% 7.02/7.46 (6301) {G15,W10,D3,L2,V0,M2} S(869);r(5020) { op( e4, e1 ) ==> e1, op( e4,
% 7.02/7.46 e1 ) ==> e3 }.
% 7.02/7.46 (6302) {G4,W10,D3,L2,V0,M2} S(870);r(2012) { op( e4, e2 ) ==> e1, op( e4,
% 7.02/7.46 e2 ) ==> e4 }.
% 7.02/7.46 (6416) {G11,W10,D3,L2,V0,M2} R(6302,4051) { op( e4, e2 ) ==> e1, op( e4, e0
% 7.02/7.46 ) ==> e4 }.
% 7.02/7.46 (6435) {G12,W6,D3,L2,V0,M2} R(6302,1591) { op( e4, e2 ) ==> e1, ! alpha19
% 7.02/7.46 }.
% 7.02/7.46 (6447) {G14,W8,D2,L4,V0,M4} P(6302,1509);d(4590);d(6435) { alpha18, !
% 7.02/7.46 alpha19, e4 ==> e0, e4 ==> e1 }.
% 7.02/7.46 (6448) {G18,W5,D2,L3,V0,M3} P(6302,1508);d(6435);d(6447);d(6034);q {
% 7.02/7.46 alpha18, ! alpha19, e4 ==> e1 }.
% 7.02/7.46 (6481) {G12,W5,D3,L1,V0,M1} P(6302,177);d(6416);q { op( e4, e2 ) ==> e1 }.
% 7.02/7.46 (6483) {G19,W2,D1,L2,V0,M2} S(6448);r(192) { alpha18, ! alpha19 }.
% 7.02/7.46 (6529) {G20,W7,D3,L3,V0,M3} R(6483,1107) { ! alpha19, alpha22, op( e2, e0 )
% 7.02/7.46 ==> e1 }.
% 7.02/7.46 (6702) {G14,W4,D2,L2,V0,M2} P(6481,238);d(4590) { alpha8, e4 ==> e0 }.
% 7.02/7.46 (6703) {G13,W5,D3,L1,V0,M1} P(6481,109) { ! op( e0, e2 ) ==> e1 }.
% 7.02/7.46 (6706) {G13,W5,D3,L1,V0,M1} P(6481,180) { ! op( e4, e1 ) ==> e1 }.
% 7.02/7.46 (6707) {G15,W1,D1,L1,V0,M1} S(6702);r(189) { alpha8 }.
% 7.02/7.46 (6730) {G20,W9,D4,L3,V0,M3} R(6707,4907) { ! alpha9, alpha19, op( e2, op(
% 7.02/7.46 e0, e2 ) ) ==> e0 }.
% 7.02/7.46 (7182) {G16,W5,D3,L1,V0,M1} S(6301);r(6706) { op( e4, e1 ) ==> e3 }.
% 7.02/7.46 (7184) {G17,W8,D4,L2,V0,M2} P(7182,913);r(394) { alpha9, op( e1, op( e3, e1
% 7.02/7.46 ) ) ==> e3 }.
% 7.02/7.46 (7215) {G17,W5,D2,L3,V0,M3} P(7182,3356);d(3326) { alpha9, ! alpha23, e4
% 7.02/7.46 ==> e1 }.
% 7.02/7.46 (7216) {G18,W2,D1,L2,V0,M2} P(7182,3355);d(3331);d(7215);q { alpha9, !
% 7.02/7.46 alpha23 }.
% 7.02/7.46 (7217) {G17,W1,D1,L1,V0,M1} P(7182,254);r(394) { alpha5 }.
% 7.02/7.46 (7347) {G18,W3,D1,L3,V0,M3} R(7217,5247) { ! alpha10, alpha14, ! alpha23
% 7.02/7.46 }.
% 7.02/7.46 (7361) {G18,W6,D3,L2,V0,M2} R(7217,3477) { op( e0, e1 ) ==> e1, alpha9 }.
% 7.02/7.46 (7413) {G21,W9,D4,L3,V0,M3} R(7216,6730) { ! alpha23, alpha19, op( e2, op(
% 7.02/7.46 e0, e2 ) ) ==> e0 }.
% 7.02/7.46 (7781) {G17,W6,D3,L2,V0,M2} R(6294,5193) { op( e2, e4 ) ==> e1, ! alpha9
% 7.02/7.46 }.
% 7.02/7.46 (7783) {G16,W10,D3,L2,V0,M2} R(6294,4014) { op( e2, e4 ) ==> e1, op( e0, e4
% 7.02/7.46 ) ==> e4 }.
% 7.02/7.46 (7802) {G18,W5,D2,L3,V0,M3} P(6294,4657);d(7182);d(7781);r(193) { ! alpha9
% 7.02/7.46 , alpha20, e4 ==> e1 }.
% 7.02/7.46 (7816) {G17,W5,D3,L1,V0,M1} P(6294,127);d(7783);q { op( e2, e4 ) ==> e1 }.
% 7.02/7.46 (7820) {G19,W2,D1,L2,V0,M2} S(7802);r(192) { ! alpha9, alpha20 }.
% 7.02/7.46 (7845) {G20,W9,D4,L3,V0,M3} R(7820,215) { ! alpha9, alpha23, op( e4, op( e1
% 7.02/7.46 , e4 ) ) ==> e1 }.
% 7.02/7.46 (7887) {G18,W5,D3,L1,V0,M1} P(7816,130) { ! op( e1, e4 ) ==> e1 }.
% 7.02/7.46 (7888) {G18,W5,D3,L1,V0,M1} P(7816,159) { ! op( e2, e0 ) ==> e1 }.
% 7.02/7.46 (7891) {G21,W2,D1,L2,V0,M2} R(7888,6529) { ! alpha19, alpha22 }.
% 7.02/7.46 (7915) {G22,W8,D4,L2,V0,M2} R(7891,7413);r(251) { ! alpha23, op( e2, op( e0
% 7.02/7.46 , e2 ) ) ==> e0 }.
% 7.02/7.46 (8132) {G19,W5,D3,L1,V0,M1} S(6293);r(7887) { op( e1, e4 ) ==> e3 }.
% 7.02/7.46 (8133) {G21,W2,D1,L2,V0,M2} P(8132,7845);d(5192);r(192) { ! alpha9, alpha23
% 7.02/7.46 }.
% 7.02/7.46 (8165) {G22,W8,D4,L2,V0,M2} R(8133,7184) { alpha23, op( e1, op( e3, e1 ) )
% 7.02/7.46 ==> e3 }.
% 7.02/7.46 (8170) {G22,W6,D3,L2,V0,M2} R(8133,7361) { alpha23, op( e0, e1 ) ==> e1 }.
% 7.02/7.46 (8548) {G15,W10,D3,L2,V0,M2} S(5690);r(187) { op( e0, e1 ) ==> e2, op( e3,
% 7.02/7.46 e1 ) ==> e2 }.
% 7.02/7.46 (8566) {G16,W6,D3,L2,V0,M2} P(8548,1605);d(1103);q;r(6703) { alpha14, op(
% 7.02/7.46 e3, e1 ) ==> e2 }.
% 7.02/7.46 (8568) {G23,W7,D2,L3,V0,M3} P(8548,8165);d(1103);d(8170) { alpha23, e3 ==>
% 7.02/7.46 e0, e2 ==> e1 }.
% 7.02/7.46 (8569) {G24,W4,D2,L2,V0,M2} P(8548,8170);d(8568);d(8170);r(190) { alpha23,
% 7.02/7.46 e2 ==> e1 }.
% 7.02/7.46 (8602) {G25,W1,D1,L1,V0,M1} S(8569);r(190) { alpha23 }.
% 7.02/7.46 (8613) {G26,W7,D4,L1,V0,M1} R(8602,7915) { op( e2, op( e0, e2 ) ) ==> e0
% 7.02/7.46 }.
% 7.02/7.46 (8618) {G26,W2,D1,L2,V0,M2} R(8602,7347) { ! alpha10, alpha14 }.
% 7.02/7.46 (8648) {G27,W1,D1,L1,V0,M1} R(8618,2618);d(8566);r(190) { alpha14 }.
% 7.02/7.46 (8649) {G28,W5,D3,L1,V0,M1} R(8648,6099) { op( e0, e1 ) ==> e2 }.
% 7.02/7.46 (8662) {G29,W5,D3,L1,V0,M1} S(4127);d(8649);q;r(6703) { op( e0, e2 ) ==> e4
% 7.02/7.46 }.
% 7.02/7.46 (8663) {G30,W0,D0,L0,V0,M0} P(8662,8613);d(7816);r(186) { }.
% 7.02/7.46
% 7.02/7.46
% 7.02/7.46 % SZS output end Refutation
% 7.02/7.46 found a proof!
% 7.02/7.46
% 7.02/7.46
% 7.02/7.46 Unprocessed initial clauses:
% 7.02/7.46
% 7.02/7.46 (8665) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e0, op( e0, e0 ) = e1, op( e0
% 7.02/7.46 , e0 ) = e2, op( e0, e0 ) = e3, op( e0, e0 ) = e4 }.
% 7.02/7.46 (8666) {G0,W25,D3,L5,V0,M5} { op( e0, e1 ) = e0, op( e0, e1 ) = e1, op( e0
% 7.02/7.46 , e1 ) = e2, op( e0, e1 ) = e3, op( e0, e1 ) = e4 }.
% 7.02/7.46 (8667) {G0,W25,D3,L5,V0,M5} { op( e0, e2 ) = e0, op( e0, e2 ) = e1, op( e0
% 7.02/7.46 , e2 ) = e2, op( e0, e2 ) = e3, op( e0, e2 ) = e4 }.
% 7.02/7.46 (8668) {G0,W25,D3,L5,V0,M5} { op( e0, e3 ) = e0, op( e0, e3 ) = e1, op( e0
% 7.02/7.46 , e3 ) = e2, op( e0, e3 ) = e3, op( e0, e3 ) = e4 }.
% 7.02/7.46 (8669) {G0,W25,D3,L5,V0,M5} { op( e0, e4 ) = e0, op( e0, e4 ) = e1, op( e0
% 7.02/7.46 , e4 ) = e2, op( e0, e4 ) = e3, op( e0, e4 ) = e4 }.
% 7.02/7.46 (8670) {G0,W25,D3,L5,V0,M5} { op( e1, e0 ) = e0, op( e1, e0 ) = e1, op( e1
% 7.02/7.46 , e0 ) = e2, op( e1, e0 ) = e3, op( e1, e0 ) = e4 }.
% 7.02/7.46 (8671) {G0,W25,D3,L5,V0,M5} { op( e1, e1 ) = e0, op( e1, e1 ) = e1, op( e1
% 7.02/7.46 , e1 ) = e2, op( e1, e1 ) = e3, op( e1, e1 ) = e4 }.
% 7.02/7.46 (8672) {G0,W25,D3,L5,V0,M5} { op( e1, e2 ) = e0, op( e1, e2 ) = e1, op( e1
% 7.02/7.46 , e2 ) = e2, op( e1, e2 ) = e3, op( e1, e2 ) = e4 }.
% 7.02/7.46 (8673) {G0,W25,D3,L5,V0,M5} { op( e1, e3 ) = e0, op( e1, e3 ) = e1, op( e1
% 7.02/7.46 , e3 ) = e2, op( e1, e3 ) = e3, op( e1, e3 ) = e4 }.
% 7.02/7.46 (8674) {G0,W25,D3,L5,V0,M5} { op( e1, e4 ) = e0, op( e1, e4 ) = e1, op( e1
% 7.02/7.46 , e4 ) = e2, op( e1, e4 ) = e3, op( e1, e4 ) = e4 }.
% 7.02/7.46 (8675) {G0,W25,D3,L5,V0,M5} { op( e2, e0 ) = e0, op( e2, e0 ) = e1, op( e2
% 7.02/7.46 , e0 ) = e2, op( e2, e0 ) = e3, op( e2, e0 ) = e4 }.
% 7.02/7.46 (8676) {G0,W25,D3,L5,V0,M5} { op( e2, e1 ) = e0, op( e2, e1 ) = e1, op( e2
% 7.02/7.46 , e1 ) = e2, op( e2, e1 ) = e3, op( e2, e1 ) = e4 }.
% 7.02/7.46 (8677) {G0,W25,D3,L5,V0,M5} { op( e2, e2 ) = e0, op( e2, e2 ) = e1, op( e2
% 7.02/7.46 , e2 ) = e2, op( e2, e2 ) = e3, op( e2, e2 ) = e4 }.
% 7.02/7.46 (8678) {G0,W25,D3,L5,V0,M5} { op( e2, e3 ) = e0, op( e2, e3 ) = e1, op( e2
% 7.02/7.46 , e3 ) = e2, op( e2, e3 ) = e3, op( e2, e3 ) = e4 }.
% 7.02/7.46 (8679) {G0,W25,D3,L5,V0,M5} { op( e2, e4 ) = e0, op( e2, e4 ) = e1, op( e2
% 7.02/7.46 , e4 ) = e2, op( e2, e4 ) = e3, op( e2, e4 ) = e4 }.
% 7.02/7.46 (8680) {G0,W25,D3,L5,V0,M5} { op( e3, e0 ) = e0, op( e3, e0 ) = e1, op( e3
% 7.02/7.46 , e0 ) = e2, op( e3, e0 ) = e3, op( e3, e0 ) = e4 }.
% 7.02/7.46 (8681) {G0,W25,D3,L5,V0,M5} { op( e3, e1 ) = e0, op( e3, e1 ) = e1, op( e3
% 7.02/7.46 , e1 ) = e2, op( e3, e1 ) = e3, op( e3, e1 ) = e4 }.
% 7.02/7.46 (8682) {G0,W25,D3,L5,V0,M5} { op( e3, e2 ) = e0, op( e3, e2 ) = e1, op( e3
% 7.02/7.46 , e2 ) = e2, op( e3, e2 ) = e3, op( e3, e2 ) = e4 }.
% 7.02/7.46 (8683) {G0,W25,D3,L5,V0,M5} { op( e3, e3 ) = e0, op( e3, e3 ) = e1, op( e3
% 7.02/7.46 , e3 ) = e2, op( e3, e3 ) = e3, op( e3, e3 ) = e4 }.
% 7.02/7.46 (8684) {G0,W25,D3,L5,V0,M5} { op( e3, e4 ) = e0, op( e3, e4 ) = e1, op( e3
% 7.02/7.46 , e4 ) = e2, op( e3, e4 ) = e3, op( e3, e4 ) = e4 }.
% 7.02/7.46 (8685) {G0,W25,D3,L5,V0,M5} { op( e4, e0 ) = e0, op( e4, e0 ) = e1, op( e4
% 7.02/7.46 , e0 ) = e2, op( e4, e0 ) = e3, op( e4, e0 ) = e4 }.
% 7.02/7.46 (8686) {G0,W25,D3,L5,V0,M5} { op( e4, e1 ) = e0, op( e4, e1 ) = e1, op( e4
% 7.02/7.46 , e1 ) = e2, op( e4, e1 ) = e3, op( e4, e1 ) = e4 }.
% 7.02/7.46 (8687) {G0,W25,D3,L5,V0,M5} { op( e4, e2 ) = e0, op( e4, e2 ) = e1, op( e4
% 7.02/7.46 , e2 ) = e2, op( e4, e2 ) = e3, op( e4, e2 ) = e4 }.
% 7.02/7.46 (8688) {G0,W25,D3,L5,V0,M5} { op( e4, e3 ) = e0, op( e4, e3 ) = e1, op( e4
% 7.02/7.46 , e3 ) = e2, op( e4, e3 ) = e3, op( e4, e3 ) = e4 }.
% 7.02/7.46 (8689) {G0,W25,D3,L5,V0,M5} { op( e4, e4 ) = e0, op( e4, e4 ) = e1, op( e4
% 7.02/7.46 , e4 ) = e2, op( e4, e4 ) = e3, op( e4, e4 ) = e4 }.
% 7.02/7.46 (8690) {G0,W5,D3,L1,V0,M1} { op( unit, e0 ) = e0 }.
% 7.02/7.46 (8691) {G0,W5,D3,L1,V0,M1} { op( e0, unit ) = e0 }.
% 7.02/7.46 (8692) {G0,W5,D3,L1,V0,M1} { op( unit, e1 ) = e1 }.
% 7.02/7.46 (8693) {G0,W5,D3,L1,V0,M1} { op( e1, unit ) = e1 }.
% 7.02/7.46 (8694) {G0,W5,D3,L1,V0,M1} { op( unit, e2 ) = e2 }.
% 7.02/7.46 (8695) {G0,W5,D3,L1,V0,M1} { op( e2, unit ) = e2 }.
% 7.02/7.46 (8696) {G0,W5,D3,L1,V0,M1} { op( unit, e3 ) = e3 }.
% 7.02/7.46 (8697) {G0,W5,D3,L1,V0,M1} { op( e3, unit ) = e3 }.
% 7.02/7.46 (8698) {G0,W5,D3,L1,V0,M1} { op( unit, e4 ) = e4 }.
% 7.02/7.46 (8699) {G0,W5,D3,L1,V0,M1} { op( e4, unit ) = e4 }.
% 7.02/7.46 (8700) {G0,W15,D2,L5,V0,M5} { unit = e0, unit = e1, unit = e2, unit = e3,
% 7.02/7.46 unit = e4 }.
% 7.02/7.46 (8701) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e0, op( e0, e1 ) = e0, op( e0
% 7.02/7.46 , e2 ) = e0, op( e0, e3 ) = e0, op( e0, e4 ) = e0 }.
% 7.02/7.46 (8702) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e0, op( e1, e0 ) = e0, op( e2
% 7.02/7.46 , e0 ) = e0, op( e3, e0 ) = e0, op( e4, e0 ) = e0 }.
% 7.02/7.46 (8703) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e1, op( e0, e1 ) = e1, op( e0
% 7.02/7.46 , e2 ) = e1, op( e0, e3 ) = e1, op( e0, e4 ) = e1 }.
% 7.02/7.46 (8704) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e1, op( e1, e0 ) = e1, op( e2
% 7.02/7.46 , e0 ) = e1, op( e3, e0 ) = e1, op( e4, e0 ) = e1 }.
% 7.02/7.46 (8705) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e2, op( e0, e1 ) = e2, op( e0
% 7.02/7.46 , e2 ) = e2, op( e0, e3 ) = e2, op( e0, e4 ) = e2 }.
% 7.02/7.46 (8706) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e2, op( e1, e0 ) = e2, op( e2
% 7.02/7.46 , e0 ) = e2, op( e3, e0 ) = e2, op( e4, e0 ) = e2 }.
% 7.02/7.46 (8707) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e3, op( e0, e1 ) = e3, op( e0
% 7.02/7.46 , e2 ) = e3, op( e0, e3 ) = e3, op( e0, e4 ) = e3 }.
% 7.02/7.46 (8708) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e3, op( e1, e0 ) = e3, op( e2
% 7.02/7.46 , e0 ) = e3, op( e3, e0 ) = e3, op( e4, e0 ) = e3 }.
% 7.02/7.46 (8709) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e4, op( e0, e1 ) = e4, op( e0
% 7.02/7.46 , e2 ) = e4, op( e0, e3 ) = e4, op( e0, e4 ) = e4 }.
% 7.02/7.46 (8710) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e4, op( e1, e0 ) = e4, op( e2
% 7.02/7.46 , e0 ) = e4, op( e3, e0 ) = e4, op( e4, e0 ) = e4 }.
% 7.02/7.46 (8711) {G0,W25,D3,L5,V0,M5} { op( e1, e0 ) = e0, op( e1, e1 ) = e0, op( e1
% 7.02/7.46 , e2 ) = e0, op( e1, e3 ) = e0, op( e1, e4 ) = e0 }.
% 7.02/7.46 (8712) {G0,W25,D3,L5,V0,M5} { op( e0, e1 ) = e0, op( e1, e1 ) = e0, op( e2
% 7.02/7.46 , e1 ) = e0, op( e3, e1 ) = e0, op( e4, e1 ) = e0 }.
% 7.02/7.46 (8713) {G0,W25,D3,L5,V0,M5} { op( e1, e0 ) = e1, op( e1, e1 ) = e1, op( e1
% 7.02/7.46 , e2 ) = e1, op( e1, e3 ) = e1, op( e1, e4 ) = e1 }.
% 7.02/7.46 (8714) {G0,W25,D3,L5,V0,M5} { op( e0, e1 ) = e1, op( e1, e1 ) = e1, op( e2
% 7.02/7.46 , e1 ) = e1, op( e3, e1 ) = e1, op( e4, e1 ) = e1 }.
% 7.02/7.46 (8715) {G0,W25,D3,L5,V0,M5} { op( e1, e0 ) = e2, op( e1, e1 ) = e2, op( e1
% 7.02/7.46 , e2 ) = e2, op( e1, e3 ) = e2, op( e1, e4 ) = e2 }.
% 7.02/7.46 (8716) {G0,W25,D3,L5,V0,M5} { op( e0, e1 ) = e2, op( e1, e1 ) = e2, op( e2
% 7.02/7.46 , e1 ) = e2, op( e3, e1 ) = e2, op( e4, e1 ) = e2 }.
% 7.02/7.46 (8717) {G0,W25,D3,L5,V0,M5} { op( e1, e0 ) = e3, op( e1, e1 ) = e3, op( e1
% 7.02/7.46 , e2 ) = e3, op( e1, e3 ) = e3, op( e1, e4 ) = e3 }.
% 7.02/7.46 (8718) {G0,W25,D3,L5,V0,M5} { op( e0, e1 ) = e3, op( e1, e1 ) = e3, op( e2
% 7.02/7.46 , e1 ) = e3, op( e3, e1 ) = e3, op( e4, e1 ) = e3 }.
% 7.02/7.46 (8719) {G0,W25,D3,L5,V0,M5} { op( e1, e0 ) = e4, op( e1, e1 ) = e4, op( e1
% 7.02/7.46 , e2 ) = e4, op( e1, e3 ) = e4, op( e1, e4 ) = e4 }.
% 7.02/7.46 (8720) {G0,W25,D3,L5,V0,M5} { op( e0, e1 ) = e4, op( e1, e1 ) = e4, op( e2
% 7.02/7.46 , e1 ) = e4, op( e3, e1 ) = e4, op( e4, e1 ) = e4 }.
% 7.02/7.46 (8721) {G0,W25,D3,L5,V0,M5} { op( e2, e0 ) = e0, op( e2, e1 ) = e0, op( e2
% 7.02/7.46 , e2 ) = e0, op( e2, e3 ) = e0, op( e2, e4 ) = e0 }.
% 7.02/7.46 (8722) {G0,W25,D3,L5,V0,M5} { op( e0, e2 ) = e0, op( e1, e2 ) = e0, op( e2
% 7.02/7.46 , e2 ) = e0, op( e3, e2 ) = e0, op( e4, e2 ) = e0 }.
% 7.02/7.46 (8723) {G0,W25,D3,L5,V0,M5} { op( e2, e0 ) = e1, op( e2, e1 ) = e1, op( e2
% 7.02/7.46 , e2 ) = e1, op( e2, e3 ) = e1, op( e2, e4 ) = e1 }.
% 7.02/7.46 (8724) {G0,W25,D3,L5,V0,M5} { op( e0, e2 ) = e1, op( e1, e2 ) = e1, op( e2
% 7.02/7.46 , e2 ) = e1, op( e3, e2 ) = e1, op( e4, e2 ) = e1 }.
% 7.02/7.46 (8725) {G0,W25,D3,L5,V0,M5} { op( e2, e0 ) = e2, op( e2, e1 ) = e2, op( e2
% 7.02/7.46 , e2 ) = e2, op( e2, e3 ) = e2, op( e2, e4 ) = e2 }.
% 7.02/7.46 (8726) {G0,W25,D3,L5,V0,M5} { op( e0, e2 ) = e2, op( e1, e2 ) = e2, op( e2
% 7.02/7.46 , e2 ) = e2, op( e3, e2 ) = e2, op( e4, e2 ) = e2 }.
% 7.02/7.46 (8727) {G0,W25,D3,L5,V0,M5} { op( e2, e0 ) = e3, op( e2, e1 ) = e3, op( e2
% 7.02/7.46 , e2 ) = e3, op( e2, e3 ) = e3, op( e2, e4 ) = e3 }.
% 7.02/7.46 (8728) {G0,W25,D3,L5,V0,M5} { op( e0, e2 ) = e3, op( e1, e2 ) = e3, op( e2
% 7.02/7.46 , e2 ) = e3, op( e3, e2 ) = e3, op( e4, e2 ) = e3 }.
% 7.02/7.46 (8729) {G0,W25,D3,L5,V0,M5} { op( e2, e0 ) = e4, op( e2, e1 ) = e4, op( e2
% 7.02/7.46 , e2 ) = e4, op( e2, e3 ) = e4, op( e2, e4 ) = e4 }.
% 7.02/7.46 (8730) {G0,W25,D3,L5,V0,M5} { op( e0, e2 ) = e4, op( e1, e2 ) = e4, op( e2
% 7.02/7.46 , e2 ) = e4, op( e3, e2 ) = e4, op( e4, e2 ) = e4 }.
% 7.02/7.46 (8731) {G0,W25,D3,L5,V0,M5} { op( e3, e0 ) = e0, op( e3, e1 ) = e0, op( e3
% 7.02/7.46 , e2 ) = e0, op( e3, e3 ) = e0, op( e3, e4 ) = e0 }.
% 7.02/7.46 (8732) {G0,W25,D3,L5,V0,M5} { op( e0, e3 ) = e0, op( e1, e3 ) = e0, op( e2
% 7.02/7.46 , e3 ) = e0, op( e3, e3 ) = e0, op( e4, e3 ) = e0 }.
% 7.02/7.46 (8733) {G0,W25,D3,L5,V0,M5} { op( e3, e0 ) = e1, op( e3, e1 ) = e1, op( e3
% 7.02/7.46 , e2 ) = e1, op( e3, e3 ) = e1, op( e3, e4 ) = e1 }.
% 7.02/7.46 (8734) {G0,W25,D3,L5,V0,M5} { op( e0, e3 ) = e1, op( e1, e3 ) = e1, op( e2
% 7.02/7.46 , e3 ) = e1, op( e3, e3 ) = e1, op( e4, e3 ) = e1 }.
% 7.02/7.46 (8735) {G0,W25,D3,L5,V0,M5} { op( e3, e0 ) = e2, op( e3, e1 ) = e2, op( e3
% 7.02/7.46 , e2 ) = e2, op( e3, e3 ) = e2, op( e3, e4 ) = e2 }.
% 7.02/7.46 (8736) {G0,W25,D3,L5,V0,M5} { op( e0, e3 ) = e2, op( e1, e3 ) = e2, op( e2
% 7.02/7.46 , e3 ) = e2, op( e3, e3 ) = e2, op( e4, e3 ) = e2 }.
% 7.02/7.46 (8737) {G0,W25,D3,L5,V0,M5} { op( e3, e0 ) = e3, op( e3, e1 ) = e3, op( e3
% 7.02/7.46 , e2 ) = e3, op( e3, e3 ) = e3, op( e3, e4 ) = e3 }.
% 7.02/7.46 (8738) {G0,W25,D3,L5,V0,M5} { op( e0, e3 ) = e3, op( e1, e3 ) = e3, op( e2
% 7.02/7.46 , e3 ) = e3, op( e3, e3 ) = e3, op( e4, e3 ) = e3 }.
% 7.02/7.46 (8739) {G0,W25,D3,L5,V0,M5} { op( e3, e0 ) = e4, op( e3, e1 ) = e4, op( e3
% 7.02/7.46 , e2 ) = e4, op( e3, e3 ) = e4, op( e3, e4 ) = e4 }.
% 7.02/7.46 (8740) {G0,W25,D3,L5,V0,M5} { op( e0, e3 ) = e4, op( e1, e3 ) = e4, op( e2
% 7.02/7.46 , e3 ) = e4, op( e3, e3 ) = e4, op( e4, e3 ) = e4 }.
% 7.02/7.46 (8741) {G0,W25,D3,L5,V0,M5} { op( e4, e0 ) = e0, op( e4, e1 ) = e0, op( e4
% 7.02/7.46 , e2 ) = e0, op( e4, e3 ) = e0, op( e4, e4 ) = e0 }.
% 7.02/7.46 (8742) {G0,W25,D3,L5,V0,M5} { op( e0, e4 ) = e0, op( e1, e4 ) = e0, op( e2
% 7.02/7.46 , e4 ) = e0, op( e3, e4 ) = e0, op( e4, e4 ) = e0 }.
% 7.02/7.46 (8743) {G0,W25,D3,L5,V0,M5} { op( e4, e0 ) = e1, op( e4, e1 ) = e1, op( e4
% 7.02/7.46 , e2 ) = e1, op( e4, e3 ) = e1, op( e4, e4 ) = e1 }.
% 7.02/7.46 (8744) {G0,W25,D3,L5,V0,M5} { op( e0, e4 ) = e1, op( e1, e4 ) = e1, op( e2
% 7.02/7.46 , e4 ) = e1, op( e3, e4 ) = e1, op( e4, e4 ) = e1 }.
% 7.02/7.46 (8745) {G0,W25,D3,L5,V0,M5} { op( e4, e0 ) = e2, op( e4, e1 ) = e2, op( e4
% 7.02/7.46 , e2 ) = e2, op( e4, e3 ) = e2, op( e4, e4 ) = e2 }.
% 7.02/7.46 (8746) {G0,W25,D3,L5,V0,M5} { op( e0, e4 ) = e2, op( e1, e4 ) = e2, op( e2
% 7.02/7.46 , e4 ) = e2, op( e3, e4 ) = e2, op( e4, e4 ) = e2 }.
% 7.02/7.46 (8747) {G0,W25,D3,L5,V0,M5} { op( e4, e0 ) = e3, op( e4, e1 ) = e3, op( e4
% 7.02/7.46 , e2 ) = e3, op( e4, e3 ) = e3, op( e4, e4 ) = e3 }.
% 7.02/7.46 (8748) {G0,W25,D3,L5,V0,M5} { op( e0, e4 ) = e3, op( e1, e4 ) = e3, op( e2
% 7.02/7.46 , e4 ) = e3, op( e3, e4 ) = e3, op( e4, e4 ) = e3 }.
% 7.02/7.46 (8749) {G0,W25,D3,L5,V0,M5} { op( e4, e0 ) = e4, op( e4, e1 ) = e4, op( e4
% 7.02/7.46 , e2 ) = e4, op( e4, e3 ) = e4, op( e4, e4 ) = e4 }.
% 7.02/7.46 (8750) {G0,W25,D3,L5,V0,M5} { op( e0, e4 ) = e4, op( e1, e4 ) = e4, op( e2
% 7.02/7.46 , e4 ) = e4, op( e3, e4 ) = e4, op( e4, e4 ) = e4 }.
% 7.02/7.46 (8751) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e1, e0 ) }.
% 7.02/7.46 (8752) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e2, e0 ) }.
% 7.02/7.46 (8753) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e3, e0 ) }.
% 7.02/7.46 (8754) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e4, e0 ) }.
% 7.02/7.46 (8755) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e2, e0 ) }.
% 7.02/7.46 (8756) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e3, e0 ) }.
% 7.02/7.46 (8757) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e4, e0 ) }.
% 7.02/7.46 (8758) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e3, e0 ) }.
% 7.02/7.46 (8759) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e4, e0 ) }.
% 7.02/7.46 (8760) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e4, e0 ) }.
% 7.02/7.46 (8761) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e1, e1 ) }.
% 7.02/7.46 (8762) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e2, e1 ) }.
% 7.02/7.46 (8763) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e3, e1 ) }.
% 7.02/7.46 (8764) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e4, e1 ) }.
% 7.02/7.46 (8765) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e2, e1 ) }.
% 7.02/7.46 (8766) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e3, e1 ) }.
% 7.02/7.46 (8767) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e4, e1 ) }.
% 7.02/7.46 (8768) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e3, e1 ) }.
% 7.02/7.46 (8769) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e4, e1 ) }.
% 7.02/7.46 (8770) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e4, e1 ) }.
% 7.02/7.46 (8771) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e1, e2 ) }.
% 7.02/7.46 (8772) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e2, e2 ) }.
% 7.02/7.46 (8773) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e3, e2 ) }.
% 7.02/7.46 (8774) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e4, e2 ) }.
% 7.02/7.46 (8775) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e2, e2 ) }.
% 7.02/7.46 (8776) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e3, e2 ) }.
% 7.02/7.46 (8777) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e4, e2 ) }.
% 7.02/7.46 (8778) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e3, e2 ) }.
% 7.02/7.46 (8779) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e4, e2 ) }.
% 7.02/7.46 (8780) {G0,W7,D3,L1,V0,M1} { ! op( e3, e2 ) = op( e4, e2 ) }.
% 7.02/7.46 (8781) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e1, e3 ) }.
% 7.02/7.46 (8782) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e2, e3 ) }.
% 7.02/7.46 (8783) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e3, e3 ) }.
% 7.02/7.46 (8784) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e4, e3 ) }.
% 7.02/7.46 (8785) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e2, e3 ) }.
% 7.02/7.46 (8786) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e3, e3 ) }.
% 7.02/7.46 (8787) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e4, e3 ) }.
% 7.02/7.46 (8788) {G0,W7,D3,L1,V0,M1} { ! op( e2, e3 ) = op( e3, e3 ) }.
% 7.02/7.46 (8789) {G0,W7,D3,L1,V0,M1} { ! op( e2, e3 ) = op( e4, e3 ) }.
% 7.02/7.46 (8790) {G0,W7,D3,L1,V0,M1} { ! op( e3, e3 ) = op( e4, e3 ) }.
% 7.02/7.46 (8791) {G0,W7,D3,L1,V0,M1} { ! op( e0, e4 ) = op( e1, e4 ) }.
% 7.02/7.46 (8792) {G0,W7,D3,L1,V0,M1} { ! op( e0, e4 ) = op( e2, e4 ) }.
% 7.02/7.46 (8793) {G0,W7,D3,L1,V0,M1} { ! op( e0, e4 ) = op( e3, e4 ) }.
% 7.02/7.46 (8794) {G0,W7,D3,L1,V0,M1} { ! op( e0, e4 ) = op( e4, e4 ) }.
% 7.02/7.46 (8795) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e2, e4 ) }.
% 7.02/7.46 (8796) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e3, e4 ) }.
% 7.02/7.46 (8797) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e4, e4 ) }.
% 7.02/7.46 (8798) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e3, e4 ) }.
% 7.02/7.46 (8799) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e4, e4 ) }.
% 7.02/7.46 (8800) {G0,W7,D3,L1,V0,M1} { ! op( e3, e4 ) = op( e4, e4 ) }.
% 7.02/7.46 (8801) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e1 ) }.
% 7.02/7.46 (8802) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e2 ) }.
% 7.02/7.46 (8803) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e3 ) }.
% 7.02/7.46 (8804) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e4 ) }.
% 7.02/7.46 (8805) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e0, e2 ) }.
% 7.02/7.46 (8806) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e0, e3 ) }.
% 7.02/7.46 (8807) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e0, e4 ) }.
% 7.02/7.46 (8808) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e0, e3 ) }.
% 7.02/7.46 (8809) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e0, e4 ) }.
% 7.02/7.46 (8810) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e0, e4 ) }.
% 7.02/7.46 (8811) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e1 ) }.
% 7.02/7.46 (8812) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e2 ) }.
% 7.02/7.46 (8813) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e3 ) }.
% 7.02/7.46 (8814) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e4 ) }.
% 7.02/7.46 (8815) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e1, e2 ) }.
% 7.02/7.46 (8816) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e1, e3 ) }.
% 7.02/7.46 (8817) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e1, e4 ) }.
% 7.02/7.46 (8818) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e1, e3 ) }.
% 7.02/7.46 (8819) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e1, e4 ) }.
% 7.02/7.46 (8820) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e1, e4 ) }.
% 7.02/7.46 (8821) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e1 ) }.
% 7.02/7.46 (8822) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e2 ) }.
% 7.02/7.46 (8823) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e3 ) }.
% 7.02/7.46 (8824) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e4 ) }.
% 7.02/7.46 (8825) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e2 ) }.
% 7.02/7.46 (8826) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e3 ) }.
% 7.02/7.46 (8827) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e4 ) }.
% 7.02/7.46 (8828) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e2, e3 ) }.
% 7.02/7.46 (8829) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e2, e4 ) }.
% 7.02/7.46 (8830) {G0,W7,D3,L1,V0,M1} { ! op( e2, e3 ) = op( e2, e4 ) }.
% 7.02/7.46 (8831) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e1 ) }.
% 7.02/7.46 (8832) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e2 ) }.
% 7.02/7.46 (8833) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e3 ) }.
% 7.02/7.46 (8834) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e4 ) }.
% 7.02/7.46 (8835) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e3, e2 ) }.
% 7.02/7.46 (8836) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e3, e3 ) }.
% 7.02/7.46 (8837) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e3, e4 ) }.
% 7.02/7.46 (8838) {G0,W7,D3,L1,V0,M1} { ! op( e3, e2 ) = op( e3, e3 ) }.
% 7.02/7.46 (8839) {G0,W7,D3,L1,V0,M1} { ! op( e3, e2 ) = op( e3, e4 ) }.
% 7.02/7.46 (8840) {G0,W7,D3,L1,V0,M1} { ! op( e3, e3 ) = op( e3, e4 ) }.
% 7.02/7.46 (8841) {G0,W7,D3,L1,V0,M1} { ! op( e4, e0 ) = op( e4, e1 ) }.
% 7.02/7.46 (8842) {G0,W7,D3,L1,V0,M1} { ! op( e4, e0 ) = op( e4, e2 ) }.
% 7.02/7.46 (8843) {G0,W7,D3,L1,V0,M1} { ! op( e4, e0 ) = op( e4, e3 ) }.
% 7.02/7.46 (8844) {G0,W7,D3,L1,V0,M1} { ! op( e4, e0 ) = op( e4, e4 ) }.
% 7.02/7.46 (8845) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e4, e2 ) }.
% 7.02/7.46 (8846) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e4, e3 ) }.
% 7.02/7.46 (8847) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e4, e4 ) }.
% 7.02/7.46 (8848) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e4, e3 ) }.
% 7.02/7.46 (8849) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e4, e4 ) }.
% 7.02/7.46 (8850) {G0,W7,D3,L1,V0,M1} { ! op( e4, e3 ) = op( e4, e4 ) }.
% 7.02/7.46 (8851) {G0,W3,D2,L1,V0,M1} { ! e0 = e1 }.
% 7.02/7.46 (8852) {G0,W3,D2,L1,V0,M1} { ! e0 = e2 }.
% 7.02/7.46 (8853) {G0,W3,D2,L1,V0,M1} { ! e0 = e3 }.
% 7.02/7.46 (8854) {G0,W3,D2,L1,V0,M1} { ! e0 = e4 }.
% 7.02/7.46 (8855) {G0,W3,D2,L1,V0,M1} { ! e1 = e2 }.
% 7.02/7.46 (8856) {G0,W3,D2,L1,V0,M1} { ! e1 = e3 }.
% 7.02/7.46 (8857) {G0,W3,D2,L1,V0,M1} { ! e1 = e4 }.
% 7.02/7.46 (8858) {G0,W3,D2,L1,V0,M1} { ! e2 = e3 }.
% 7.02/7.46 (8859) {G0,W3,D2,L1,V0,M1} { ! e2 = e4 }.
% 7.02/7.46 (8860) {G0,W3,D2,L1,V0,M1} { ! e3 = e4 }.
% 7.02/7.46 (8861) {G0,W11,D5,L1,V0,M1} { e0 = op( e1, op( op( e1, e1 ), op( e1, e1 )
% 7.02/7.46 ) ) }.
% 7.02/7.46 (8862) {G0,W9,D4,L1,V0,M1} { e2 = op( op( e1, e1 ), op( e1, e1 ) ) }.
% 7.02/7.46 (8863) {G0,W17,D5,L1,V0,M1} { e3 = op( op( op( e1, e1 ), op( e1, e1 ) ),
% 7.02/7.46 op( op( e1, e1 ), op( e1, e1 ) ) ) }.
% 7.02/7.46 (8864) {G0,W5,D3,L1,V0,M1} { e4 = op( e1, e1 ) }.
% 7.02/7.46 (8865) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e0, op( e1, e1 ) = e0, op( e2
% 7.02/7.46 , e2 ) = e0, op( e3, e3 ) = e0, op( e4, e4 ) = e0 }.
% 7.02/7.46 (8866) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e1, op( e1, e1 ) = e1, op( e2
% 7.02/7.46 , e2 ) = e1, op( e3, e3 ) = e1, op( e4, e4 ) = e1 }.
% 7.02/7.46 (8867) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e2, op( e1, e1 ) = e2, op( e2
% 7.02/7.46 , e2 ) = e2, op( e3, e3 ) = e2, op( e4, e4 ) = e2 }.
% 7.02/7.46 (8868) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e3, op( e1, e1 ) = e3, op( e2
% 7.02/7.46 , e2 ) = e3, op( e3, e3 ) = e3, op( e4, e4 ) = e3 }.
% 7.02/7.46 (8869) {G0,W25,D3,L5,V0,M5} { op( e0, e0 ) = e4, op( e1, e1 ) = e4, op( e2
% 7.02/7.46 , e2 ) = e4, op( e3, e3 ) = e4, op( e4, e4 ) = e4 }.
% 7.02/7.46 (8870) {G0,W1,D1,L1,V0,M1} { alpha1 }.
% 7.02/7.46 (8871) {G0,W1,D1,L1,V0,M1} { alpha2 }.
% 7.02/7.46 (8872) {G0,W1,D1,L1,V0,M1} { alpha4 }.
% 7.02/7.46 (8873) {G0,W1,D1,L1,V0,M1} { alpha7 }.
% 7.02/7.46 (8874) {G0,W8,D4,L2,V0,M2} { alpha11, ! op( e4, op( e4, e4 ) ) = e4 }.
% 7.02/7.46 (8875) {G0,W8,D4,L2,V0,M2} { alpha11, op( e4, op( e4, e4 ) ) = e4 }.
% 7.02/7.46 (8876) {G0,W9,D4,L3,V0,M3} { ! alpha11, alpha16, ! op( e3, op( e3, e4 ) )
% 7.02/7.46 = e4 }.
% 7.02/7.46 (8877) {G0,W9,D4,L3,V0,M3} { ! alpha11, alpha16, op( e4, op( e3, e4 ) ) =
% 7.02/7.46 e3 }.
% 7.02/7.46 (8878) {G0,W2,D1,L2,V0,M2} { ! alpha16, alpha11 }.
% 7.02/7.46 (8879) {G0,W15,D4,L3,V0,M3} { op( e3, op( e3, e4 ) ) = e4, ! op( e4, op(
% 7.02/7.46 e3, e4 ) ) = e3, alpha11 }.
% 7.02/7.46 (8880) {G0,W9,D4,L3,V0,M3} { ! alpha16, alpha20, ! op( e2, op( e2, e4 ) )
% 7.02/7.46 = e4 }.
% 7.02/7.46 (8881) {G0,W9,D4,L3,V0,M3} { ! alpha16, alpha20, op( e4, op( e2, e4 ) ) =
% 7.02/7.46 e2 }.
% 7.02/7.46 (8882) {G0,W2,D1,L2,V0,M2} { ! alpha20, alpha16 }.
% 7.02/7.46 (8883) {G0,W15,D4,L3,V0,M3} { op( e2, op( e2, e4 ) ) = e4, ! op( e4, op(
% 7.02/7.46 e2, e4 ) ) = e2, alpha16 }.
% 7.02/7.46 (8884) {G0,W9,D4,L3,V0,M3} { ! alpha20, alpha23, ! op( e1, op( e1, e4 ) )
% 7.02/7.46 = e4 }.
% 7.02/7.46 (8885) {G0,W9,D4,L3,V0,M3} { ! alpha20, alpha23, op( e4, op( e1, e4 ) ) =
% 7.02/7.46 e1 }.
% 7.02/7.46 (8886) {G0,W2,D1,L2,V0,M2} { ! alpha23, alpha20 }.
% 7.02/7.46 (8887) {G0,W15,D4,L3,V0,M3} { op( e1, op( e1, e4 ) ) = e4, ! op( e4, op(
% 7.02/7.46 e1, e4 ) ) = e1, alpha20 }.
% 7.02/7.46 (8888) {G0,W8,D4,L2,V0,M2} { ! alpha23, ! op( e0, op( e0, e4 ) ) = e4 }.
% 7.02/7.46 (8889) {G0,W8,D4,L2,V0,M2} { ! alpha23, op( e4, op( e0, e4 ) ) = e0 }.
% 7.02/7.46 (8890) {G0,W15,D4,L3,V0,M3} { op( e0, op( e0, e4 ) ) = e4, ! op( e4, op(
% 7.02/7.46 e0, e4 ) ) = e0, alpha23 }.
% 7.02/7.46 (8891) {G0,W9,D4,L3,V0,M3} { ! alpha7, alpha12, ! op( e4, op( e4, e3 ) ) =
% 7.02/7.46 e3 }.
% 7.02/7.46 (8892) {G0,W9,D4,L3,V0,M3} { ! alpha7, alpha12, op( e3, op( e4, e3 ) ) =
% 7.02/7.46 e4 }.
% 7.02/7.46 (8893) {G0,W2,D1,L2,V0,M2} { ! alpha12, alpha7 }.
% 7.02/7.46 (8894) {G0,W15,D4,L3,V0,M3} { op( e4, op( e4, e3 ) ) = e3, ! op( e3, op(
% 7.02/7.46 e4, e3 ) ) = e4, alpha7 }.
% 7.02/7.46 (8895) {G0,W9,D4,L3,V0,M3} { ! alpha12, alpha17, ! op( e3, op( e3, e3 ) )
% 7.02/7.46 = e3 }.
% 7.02/7.46 (8896) {G0,W9,D4,L3,V0,M3} { ! alpha12, alpha17, op( e3, op( e3, e3 ) ) =
% 7.02/7.46 e3 }.
% 7.02/7.46 (8897) {G0,W2,D1,L2,V0,M2} { ! alpha17, alpha12 }.
% 7.02/7.46 (8898) {G0,W15,D4,L3,V0,M3} { op( e3, op( e3, e3 ) ) = e3, ! op( e3, op(
% 7.02/7.46 e3, e3 ) ) = e3, alpha12 }.
% 7.02/7.46 (8899) {G0,W9,D4,L3,V0,M3} { ! alpha17, alpha21, ! op( e2, op( e2, e3 ) )
% 7.02/7.46 = e3 }.
% 7.02/7.46 (8900) {G0,W9,D4,L3,V0,M3} { ! alpha17, alpha21, op( e3, op( e2, e3 ) ) =
% 7.02/7.46 e2 }.
% 7.02/7.46 (8901) {G0,W2,D1,L2,V0,M2} { ! alpha21, alpha17 }.
% 7.02/7.46 (8902) {G0,W15,D4,L3,V0,M3} { op( e2, op( e2, e3 ) ) = e3, ! op( e3, op(
% 7.02/7.46 e2, e3 ) ) = e2, alpha17 }.
% 7.02/7.46 (8903) {G0,W9,D4,L3,V0,M3} { ! alpha21, alpha24, ! op( e1, op( e1, e3 ) )
% 7.02/7.46 = e3 }.
% 7.02/7.46 (8904) {G0,W9,D4,L3,V0,M3} { ! alpha21, alpha24, op( e3, op( e1, e3 ) ) =
% 7.02/7.46 e1 }.
% 7.02/7.46 (8905) {G0,W2,D1,L2,V0,M2} { ! alpha24, alpha21 }.
% 7.02/7.46 (8906) {G0,W15,D4,L3,V0,M3} { op( e1, op( e1, e3 ) ) = e3, ! op( e3, op(
% 7.02/7.46 e1, e3 ) ) = e1, alpha21 }.
% 7.02/7.46 (8907) {G0,W8,D4,L2,V0,M2} { ! alpha24, ! op( e0, op( e0, e3 ) ) = e3 }.
% 7.02/7.46 (8908) {G0,W8,D4,L2,V0,M2} { ! alpha24, op( e3, op( e0, e3 ) ) = e0 }.
% 7.02/7.46 (8909) {G0,W15,D4,L3,V0,M3} { op( e0, op( e0, e3 ) ) = e3, ! op( e3, op(
% 7.02/7.46 e0, e3 ) ) = e0, alpha24 }.
% 7.02/7.46 (8910) {G0,W9,D4,L3,V0,M3} { ! alpha4, alpha8, ! op( e4, op( e4, e2 ) ) =
% 7.02/7.46 e2 }.
% 7.02/7.46 (8911) {G0,W9,D4,L3,V0,M3} { ! alpha4, alpha8, op( e2, op( e4, e2 ) ) = e4
% 7.02/7.46 }.
% 7.02/7.46 (8912) {G0,W2,D1,L2,V0,M2} { ! alpha8, alpha4 }.
% 7.02/7.46 (8913) {G0,W15,D4,L3,V0,M3} { op( e4, op( e4, e2 ) ) = e2, ! op( e2, op(
% 7.02/7.46 e4, e2 ) ) = e4, alpha4 }.
% 7.02/7.46 (8914) {G0,W9,D4,L3,V0,M3} { ! alpha8, alpha13, ! op( e3, op( e3, e2 ) ) =
% 7.02/7.46 e2 }.
% 7.02/7.46 (8915) {G0,W9,D4,L3,V0,M3} { ! alpha8, alpha13, op( e2, op( e3, e2 ) ) =
% 7.02/7.46 e3 }.
% 7.02/7.46 (8916) {G0,W2,D1,L2,V0,M2} { ! alpha13, alpha8 }.
% 7.02/7.46 (8917) {G0,W15,D4,L3,V0,M3} { op( e3, op( e3, e2 ) ) = e2, ! op( e2, op(
% 7.02/7.46 e3, e2 ) ) = e3, alpha8 }.
% 7.02/7.46 (8918) {G0,W9,D4,L3,V0,M3} { ! alpha13, alpha18, ! op( e2, op( e2, e2 ) )
% 7.02/7.46 = e2 }.
% 7.02/7.46 (8919) {G0,W9,D4,L3,V0,M3} { ! alpha13, alpha18, op( e2, op( e2, e2 ) ) =
% 7.02/7.46 e2 }.
% 7.02/7.46 (8920) {G0,W2,D1,L2,V0,M2} { ! alpha18, alpha13 }.
% 7.02/7.46 (8921) {G0,W15,D4,L3,V0,M3} { op( e2, op( e2, e2 ) ) = e2, ! op( e2, op(
% 7.02/7.46 e2, e2 ) ) = e2, alpha13 }.
% 7.02/7.46 (8922) {G0,W9,D4,L3,V0,M3} { ! alpha18, alpha22, ! op( e1, op( e1, e2 ) )
% 7.02/7.46 = e2 }.
% 7.02/7.46 (8923) {G0,W9,D4,L3,V0,M3} { ! alpha18, alpha22, op( e2, op( e1, e2 ) ) =
% 7.02/7.46 e1 }.
% 7.02/7.46 (8924) {G0,W2,D1,L2,V0,M2} { ! alpha22, alpha18 }.
% 7.02/7.46 (8925) {G0,W15,D4,L3,V0,M3} { op( e1, op( e1, e2 ) ) = e2, ! op( e2, op(
% 7.02/7.46 e1, e2 ) ) = e1, alpha18 }.
% 7.02/7.46 (8926) {G0,W8,D4,L2,V0,M2} { ! alpha22, ! op( e0, op( e0, e2 ) ) = e2 }.
% 7.02/7.46 (8927) {G0,W8,D4,L2,V0,M2} { ! alpha22, op( e2, op( e0, e2 ) ) = e0 }.
% 7.02/7.46 (8928) {G0,W15,D4,L3,V0,M3} { op( e0, op( e0, e2 ) ) = e2, ! op( e2, op(
% 7.02/7.46 e0, e2 ) ) = e0, alpha22 }.
% 7.02/7.46 (8929) {G0,W9,D4,L3,V0,M3} { ! alpha2, alpha5, ! op( e4, op( e4, e1 ) ) =
% 7.02/7.46 e1 }.
% 7.02/7.46 (8930) {G0,W9,D4,L3,V0,M3} { ! alpha2, alpha5, op( e1, op( e4, e1 ) ) = e4
% 7.02/7.46 }.
% 7.02/7.46 (8931) {G0,W2,D1,L2,V0,M2} { ! alpha5, alpha2 }.
% 7.02/7.46 (8932) {G0,W15,D4,L3,V0,M3} { op( e4, op( e4, e1 ) ) = e1, ! op( e1, op(
% 7.02/7.46 e4, e1 ) ) = e4, alpha2 }.
% 7.02/7.46 (8933) {G0,W9,D4,L3,V0,M3} { ! alpha5, alpha9, ! op( e3, op( e3, e1 ) ) =
% 7.02/7.46 e1 }.
% 7.02/7.46 (8934) {G0,W9,D4,L3,V0,M3} { ! alpha5, alpha9, op( e1, op( e3, e1 ) ) = e3
% 7.02/7.46 }.
% 7.02/7.46 (8935) {G0,W2,D1,L2,V0,M2} { ! alpha9, alpha5 }.
% 7.11/7.48 (8936) {G0,W15,D4,L3,V0,M3} { op( e3, op( e3, e1 ) ) = e1, ! op( e1, op(
% 7.11/7.48 e3, e1 ) ) = e3, alpha5 }.
% 7.11/7.48 (8937) {G0,W9,D4,L3,V0,M3} { ! alpha9, alpha14, ! op( e2, op( e2, e1 ) ) =
% 7.11/7.48 e1 }.
% 7.11/7.48 (8938) {G0,W9,D4,L3,V0,M3} { ! alpha9, alpha14, op( e1, op( e2, e1 ) ) =
% 7.11/7.48 e2 }.
% 7.11/7.48 (8939) {G0,W2,D1,L2,V0,M2} { ! alpha14, alpha9 }.
% 7.11/7.48 (8940) {G0,W15,D4,L3,V0,M3} { op( e2, op( e2, e1 ) ) = e1, ! op( e1, op(
% 7.11/7.48 e2, e1 ) ) = e2, alpha9 }.
% 7.11/7.48 (8941) {G0,W9,D4,L3,V0,M3} { ! alpha14, alpha19, ! op( e1, op( e1, e1 ) )
% 7.11/7.48 = e1 }.
% 7.11/7.48 (8942) {G0,W9,D4,L3,V0,M3} { ! alpha14, alpha19, op( e1, op( e1, e1 ) ) =
% 7.11/7.48 e1 }.
% 7.11/7.48 (8943) {G0,W2,D1,L2,V0,M2} { ! alpha19, alpha14 }.
% 7.11/7.48 (8944) {G0,W15,D4,L3,V0,M3} { op( e1, op( e1, e1 ) ) = e1, ! op( e1, op(
% 7.11/7.48 e1, e1 ) ) = e1, alpha14 }.
% 7.11/7.48 (8945) {G0,W8,D4,L2,V0,M2} { ! alpha19, ! op( e0, op( e0, e1 ) ) = e1 }.
% 7.11/7.48 (8946) {G0,W8,D4,L2,V0,M2} { ! alpha19, op( e1, op( e0, e1 ) ) = e0 }.
% 7.11/7.48 (8947) {G0,W15,D4,L3,V0,M3} { op( e0, op( e0, e1 ) ) = e1, ! op( e1, op(
% 7.11/7.48 e0, e1 ) ) = e0, alpha19 }.
% 7.11/7.48 (8948) {G0,W9,D4,L3,V0,M3} { ! alpha1, alpha3, ! op( e4, op( e4, e0 ) ) =
% 7.11/7.48 e0 }.
% 7.11/7.48 (8949) {G0,W9,D4,L3,V0,M3} { ! alpha1, alpha3, op( e0, op( e4, e0 ) ) = e4
% 7.11/7.48 }.
% 7.11/7.48 (8950) {G0,W2,D1,L2,V0,M2} { ! alpha3, alpha1 }.
% 7.11/7.48 (8951) {G0,W15,D4,L3,V0,M3} { op( e4, op( e4, e0 ) ) = e0, ! op( e0, op(
% 7.11/7.48 e4, e0 ) ) = e4, alpha1 }.
% 7.11/7.48 (8952) {G0,W9,D4,L3,V0,M3} { ! alpha3, alpha6, ! op( e3, op( e3, e0 ) ) =
% 7.11/7.48 e0 }.
% 7.11/7.48 (8953) {G0,W9,D4,L3,V0,M3} { ! alpha3, alpha6, op( e0, op( e3, e0 ) ) = e3
% 7.11/7.48 }.
% 7.11/7.48 (8954) {G0,W2,D1,L2,V0,M2} { ! alpha6, alpha3 }.
% 7.11/7.48 (8955) {G0,W15,D4,L3,V0,M3} { op( e3, op( e3, e0 ) ) = e0, ! op( e0, op(
% 7.11/7.48 e3, e0 ) ) = e3, alpha3 }.
% 7.11/7.48 (8956) {G0,W9,D4,L3,V0,M3} { ! alpha6, alpha10, ! op( e2, op( e2, e0 ) ) =
% 7.11/7.48 e0 }.
% 7.11/7.48 (8957) {G0,W9,D4,L3,V0,M3} { ! alpha6, alpha10, op( e0, op( e2, e0 ) ) =
% 7.11/7.48 e2 }.
% 7.11/7.48 (8958) {G0,W2,D1,L2,V0,M2} { ! alpha10, alpha6 }.
% 7.11/7.48 (8959) {G0,W15,D4,L3,V0,M3} { op( e2, op( e2, e0 ) ) = e0, ! op( e0, op(
% 7.11/7.48 e2, e0 ) ) = e2, alpha6 }.
% 7.11/7.48 (8960) {G0,W9,D4,L3,V0,M3} { ! alpha10, alpha15, ! op( e1, op( e1, e0 ) )
% 7.11/7.48 = e0 }.
% 7.11/7.48 (8961) {G0,W9,D4,L3,V0,M3} { ! alpha10, alpha15, op( e0, op( e1, e0 ) ) =
% 7.11/7.48 e1 }.
% 7.11/7.48 (8962) {G0,W2,D1,L2,V0,M2} { ! alpha15, alpha10 }.
% 7.11/7.48 (8963) {G0,W15,D4,L3,V0,M3} { op( e1, op( e1, e0 ) ) = e0, ! op( e0, op(
% 7.11/7.48 e1, e0 ) ) = e1, alpha10 }.
% 7.11/7.48 (8964) {G0,W8,D4,L2,V0,M2} { ! alpha15, ! op( e0, op( e0, e0 ) ) = e0 }.
% 7.11/7.48 (8965) {G0,W8,D4,L2,V0,M2} { ! alpha15, op( e0, op( e0, e0 ) ) = e0 }.
% 7.11/7.48 (8966) {G0,W15,D4,L3,V0,M3} { op( e0, op( e0, e0 ) ) = e0, ! op( e0, op(
% 7.11/7.48 e0, e0 ) ) = e0, alpha15 }.
% 7.11/7.48
% 7.11/7.48
% 7.11/7.48 Total Proof:
% 7.11/7.48
% 7.11/7.48 subsumption: (1) {G0,W25,D3,L5,V0,M5} I { op( e0, e1 ) ==> e0, op( e0, e1 )
% 7.11/7.48 ==> e1, op( e0, e1 ) ==> e2, op( e0, e1 ) ==> e3, op( e0, e1 ) ==> e4
% 7.11/7.48 }.
% 7.11/7.48 parent0: (8666) {G0,W25,D3,L5,V0,M5} { op( e0, e1 ) = e0, op( e0, e1 ) =
% 7.11/7.48 e1, op( e0, e1 ) = e2, op( e0, e1 ) = e3, op( e0, e1 ) = e4 }.
% 7.11/7.48 substitution0:
% 7.11/7.48 end
% 7.11/7.48 permutation0:
% 7.11/7.48 0 ==> 0
% 7.11/7.48 1 ==> 1
% 7.11/7.48 2 ==> 2
% 7.11/7.48 3 ==> 3
% 7.11/7.48 4 ==> 4
% 7.11/7.48 end
% 7.11/7.48
% 7.11/7.48 *** allocated 576640 integers for clauses
% 7.11/7.48 subsumption: (2) {G0,W25,D3,L5,V0,M5} I { op( e0, e2 ) ==> e0, op( e0, e2 )
% 7.11/7.48 ==> e1, op( e0, e2 ) ==> e2, op( e0, e2 ) ==> e3, op( e0, e2 ) ==> e4
% 7.11/7.48 }.
% 7.11/7.48 parent0: (8667) {G0,W25,D3,L5,V0,M5} { op( e0, e2 ) = e0, op( e0, e2 ) =
% 7.11/7.48 e1, op( e0, e2 ) = e2, op( e0, e2 ) = e3, op( e0, e2 ) = e4 }.
% 7.11/7.48 substitution0:
% 7.11/7.48 end
% 7.11/7.48 permutation0:
% 7.11/7.48 0 ==> 0
% 7.11/7.48 1 ==> 1
% 7.11/7.48 2 ==> 2
% 7.11/7.48 3 ==> 3
% 7.11/7.48 4 ==> 4
% 7.11/7.48 end
% 7.11/7.48
% 7.11/7.48 subsumption: (9) {G0,W25,D3,L5,V0,M5} I { op( e1, e4 ) ==> e0, op( e1, e4 )
% 7.11/7.48 ==> e1, op( e1, e4 ) ==> e2, op( e1, e4 ) ==> e3, op( e1, e4 ) ==> e4
% 7.11/7.48 }.
% 7.11/7.48 parent0: (8674) {G0,W25,D3,L5,V0,M5} { op( e1, e4 ) = e0, op( e1, e4 ) =
% 7.11/7.48 e1, op( e1, e4 ) = e2, op( e1, e4 ) = e3, op( e1, e4 ) = e4 }.
% 7.11/7.48 substitution0:
% 7.11/7.48 end
% 7.11/7.48 permutation0:
% 7.11/7.48 0 ==> 0
% 7.11/7.48 1 ==> 1
% 7.11/7.48 2 ==> 2
% 7.11/7.48 3 ==> 3
% 7.11/7.48 4 ==> 4
% 7.11/7.48 end
% 7.11/7.48
% 7.11/7.48 subsumption: (11) {G0,W25,D3,L5,V0,M5} I { op( e2, e1 ) ==> e0, op( e2, e1
% 7.11/7.48 ) ==> e1, op( e2, e1 ) ==> e2, op( e2, e1 ) ==> e3, op( e2, e1 ) ==> e4
% 7.11/7.48 }.
% 7.11/7.48 parent0: (8676) {G0,W25,D3,L5,V0,M5} { op( e2, e1 ) = e0, op( e2, e1 ) =
% 7.11/7.48 e1, op( e2, e1 ) = e2, op( e2, e1 ) = e3, op( e2, e1 ) = e4 }.
% 7.43/7.79 substitution0:
% 7.43/7.79 end
% 7.43/7.79 permutation0:
% 7.43/7.79 0 ==> 0
% 7.43/7.79 1 ==> 1
% 7.43/7.79 2 ==> 2
% 7.43/7.79 3 ==> 3
% 7.43/7.79 4 ==> 4
% 7.43/7.79 end
% 7.43/7.79
% 7.43/7.79 subsumption: (14) {G0,W25,D3,L5,V0,M5} I { op( e2, e4 ) ==> e0, op( e2, e4
% 7.43/7.79 ) ==> e1, op( e2, e4 ) ==> e2, op( e2, e4 ) ==> e3, op( e2, e4 ) ==> e4
% 7.43/7.79 }.
% 7.43/7.79 parent0: (8679) {G0,W25,D3,L5,V0,M5} { op( e2, e4 ) = e0, op( e2, e4 ) =
% 7.43/7.79 e1, op( e2, e4 ) = e2, op( e2, e4 ) = e3, op( e2, e4 ) = e4 }.
% 7.43/7.79 substitution0:
% 7.43/7.79 end
% 7.43/7.79 permutation0:
% 7.43/7.79 0 ==> 0
% 7.43/7.79 1 ==> 1
% 7.43/7.79 2 ==> 2
% 7.43/7.79 3 ==> 3
% 7.43/7.79 4 ==> 4
% 7.43/7.79 end
% 7.43/7.79
% 7.43/7.79 *** allocated 256285 integers for termspace/termends
% 7.43/7.79 subsumption: (21) {G0,W25,D3,L5,V0,M5} I { op( e4, e1 ) ==> e0, op( e4, e1
% 7.43/7.79 ) ==> e1, op( e4, e1 ) ==> e2, op( e4, e1 ) ==> e3, op( e4, e1 ) ==> e4
% 7.43/7.79 }.
% 7.43/7.79 parent0: (8686) {G0,W25,D3,L5,V0,M5} { op( e4, e1 ) = e0, op( e4, e1 ) =
% 7.43/7.79 e1, op( e4, e1 ) = e2, op( e4, e1 ) = e3, op( e4, e1 ) = e4 }.
% 7.43/7.79 substitution0:
% 7.43/7.79 end
% 7.43/7.79 permutation0:
% 7.43/7.79 0 ==> 0
% 7.43/7.79 1 ==> 1
% 7.43/7.79 2 ==> 2
% 7.43/7.79 3 ==> 3
% 7.43/7.79 4 ==> 4
% 7.43/7.79 end
% 7.43/7.79
% 7.43/7.79 subsumption: (22) {G0,W25,D3,L5,V0,M5} I { op( e4, e2 ) ==> e0, op( e4, e2
% 7.43/7.79 ) ==> e1, op( e4, e2 ) ==> e2, op( e4, e2 ) ==> e3, op( e4, e2 ) ==> e4
% 7.43/7.79 }.
% 7.43/7.79 parent0: (8687) {G0,W25,D3,L5,V0,M5} { op( e4, e2 ) = e0, op( e4, e2 ) =
% 7.43/7.79 e1, op( e4, e2 ) = e2, op( e4, e2 ) = e3, op( e4, e2 ) = e4 }.
% 7.43/7.79 substitution0:
% 7.43/7.79 end
% 7.43/7.79 permutation0:
% 7.43/7.79 0 ==> 0
% 7.43/7.79 1 ==> 1
% 7.43/7.79 2 ==> 2
% 7.43/7.79 3 ==> 3
% 7.43/7.79 4 ==> 4
% 7.43/7.79 end
% 7.43/7.79
% 7.43/7.79 subsumption: (25) {G0,W5,D3,L1,V0,M1} I { op( unit, e0 ) ==> e0 }.
% 7.43/7.79 parent0: (8690) {G0,W5,D3,L1,V0,M1} { op( unit, e0 ) = e0 }.
% 7.43/7.79 substitution0:
% 7.43/7.79 end
% 7.43/7.79 permutation0:
% 7.43/7.79 0 ==> 0
% 7.43/7.79 end
% 7.43/7.79
% 7.43/7.79 subsumption: (27) {G0,W5,D3,L1,V0,M1} I { op( unit, e1 ) ==> e1 }.
% 7.43/7.79 parent0: (8692) {G0,W5,D3,L1,V0,M1} { op( unit, e1 ) = e1 }.
% 7.43/7.79 substitution0:
% 7.43/7.79 end
% 7.43/7.79 permutation0:
% 7.43/7.79 0 ==> 0
% 7.43/7.79 end
% 7.43/7.79
% 7.43/7.79 *** allocated 384427 integers for termspace/termends
% 7.43/7.79 subsumption: (28) {G0,W5,D3,L1,V0,M1} I { op( e1, unit ) ==> e1 }.
% 7.43/7.79 parent0: (8693) {G0,W5,D3,L1,V0,M1} { op( e1, unit ) = e1 }.
% 7.43/7.79 substitution0:
% 7.43/7.79 end
% 7.43/7.79 permutation0:
% 7.43/7.79 0 ==> 0
% 7.43/7.79 end
% 7.43/7.79
% 7.43/7.79 subsumption: (29) {G0,W5,D3,L1,V0,M1} I { op( unit, e2 ) ==> e2 }.
% 7.43/7.79 parent0: (8694) {G0,W5,D3,L1,V0,M1} { op( unit, e2 ) = e2 }.
% 7.43/7.79 substitution0:
% 7.43/7.79 end
% 7.43/7.79 permutation0:
% 7.43/7.79 0 ==> 0
% 7.43/7.79 end
% 7.43/7.79
% 7.43/7.79 subsumption: (30) {G0,W5,D3,L1,V0,M1} I { op( e2, unit ) ==> e2 }.
% 7.43/7.79 parent0: (8695) {G0,W5,D3,L1,V0,M1} { op( e2, unit ) = e2 }.
% 7.43/7.79 substitution0:
% 7.43/7.79 end
% 7.43/7.79 permutation0:
% 7.43/7.79 0 ==> 0
% 7.43/7.79 end
% 7.43/7.79
% 7.43/7.79 subsumption: (33) {G0,W5,D3,L1,V0,M1} I { op( unit, e4 ) ==> e4 }.
% 7.43/7.79 parent0: (8698) {G0,W5,D3,L1,V0,M1} { op( unit, e4 ) = e4 }.
% 7.43/7.79 substitution0:
% 7.43/7.79 end
% 7.43/7.79 permutation0:
% 7.43/7.79 0 ==> 0
% 7.43/7.79 end
% 7.43/7.79
% 7.43/7.79 *** allocated 864960 integers for clauses
% 7.43/7.79 subsumption: (34) {G0,W5,D3,L1,V0,M1} I { op( e4, unit ) ==> e4 }.
% 7.43/7.79 parent0: (8699) {G0,W5,D3,L1,V0,M1} { op( e4, unit ) = e4 }.
% 7.43/7.79 substitution0:
% 7.43/7.79 end
% 7.43/7.79 permutation0:
% 7.43/7.79 0 ==> 0
% 7.43/7.79 end
% 7.43/7.79
% 7.43/7.79 subsumption: (35) {G0,W15,D2,L5,V0,M5} I { unit ==> e0, unit ==> e1, unit
% 7.43/7.79 ==> e2, unit ==> e3, unit ==> e4 }.
% 7.43/7.79 parent0: (8700) {G0,W15,D2,L5,V0,M5} { unit = e0, unit = e1, unit = e2,
% 7.43/7.79 unit = e3, unit = e4 }.
% 7.43/7.79 substitution0:
% 7.43/7.79 end
% 7.43/7.79 permutation0:
% 7.43/7.79 0 ==> 0
% 7.43/7.79 1 ==> 1
% 7.43/7.79 2 ==> 2
% 7.43/7.79 3 ==> 3
% 7.43/7.79 4 ==> 4
% 7.43/7.79 end
% 7.43/7.79
% 7.43/7.79 *** allocated 576640 integers for termspace/termends
% 7.43/7.79 subsumption: (51) {G0,W25,D3,L5,V0,M5} I { op( e0, e1 ) ==> e2, op( e1, e1
% 7.43/7.79 ) ==> e2, op( e2, e1 ) ==> e2, op( e3, e1 ) ==> e2, op( e4, e1 ) ==> e2
% 7.43/7.79 }.
% 7.43/7.79 parent0: (8716) {G0,W25,D3,L5,V0,M5} { op( e0, e1 ) = e2, op( e1, e1 ) =
% 7.43/7.79 e2, op( e2, e1 ) = e2, op( e3, e1 ) = e2, op( e4, e1 ) = e2 }.
% 7.43/7.79 substitution0:
% 7.43/7.79 end
% 7.43/7.79 permutation0:
% 7.43/7.79 0 ==> 0
% 7.43/7.79 1 ==> 1
% 7.43/7.79 2 ==> 2
% 7.43/7.79 3 ==> 3
% 7.43/7.79 4 ==> 4
% 7.43/7.79 end
% 7.43/7.79
% 7.43/7.79 eqswap: (21632) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e0, e1 ) }.
% 7.43/7.79 parent0[0]: (8762) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e2, e1 ) }.
% 7.43/7.79 substitution0:
% 7.43/7.79 end
% 7.43/7.79
% 7.43/7.79 subsumption: (97) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e1 ) ==> op( e0, e1 )
% 7.43/7.79 }.
% 7.43/7.79 parent0: (21632) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e0, e1 ) }.
% 7.43/7.79 substitution0:
% 7.43/7.79 end
% 7.43/7.79 permutation0:
% 7.43/7.79 0 ==> 0
% 7.43/7.79 end
% 7.43/7.79
% 7.43/7.79 eqswap: (24011) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e0, e1 ) }.
% 7.43/7.79 parent0[0]: (8763) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e3, e1 ) }.
% 7.43/7.79 substitution0:
% 7.43/7.79 end
% 7.43/7.79
% 7.43/7.79 subsumption: (98) {G0,W7,D3,L1,V0,M1} I { ! op( e3, e1 ) ==> op( e0, e1 )
% 7.43/7.79 }.
% 7.43/7.79 parent0: (24011) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e0, e1 ) }.
% 7.43/7.79 substitution0:
% 7.86/8.25 end
% 7.86/8.25 permutation0:
% 7.86/8.25 0 ==> 0
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 eqswap: (26392) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e1, e1 ) }.
% 7.86/8.25 parent0[0]: (8765) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e2, e1 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 subsumption: (100) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e1 ) ==> op( e1, e1 )
% 7.86/8.25 }.
% 7.86/8.25 parent0: (26392) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e1, e1 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25 permutation0:
% 7.86/8.25 0 ==> 0
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 *** allocated 864960 integers for termspace/termends
% 7.86/8.25 eqswap: (28775) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e1, e1 ) }.
% 7.86/8.25 parent0[0]: (8767) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e4, e1 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 subsumption: (102) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e1 ) ==> op( e1, e1 )
% 7.86/8.25 }.
% 7.86/8.25 parent0: (28775) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e1, e1 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25 permutation0:
% 7.86/8.25 0 ==> 0
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 *** allocated 1297440 integers for clauses
% 7.86/8.25 eqswap: (31159) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e2, e1 ) }.
% 7.86/8.25 parent0[0]: (8768) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e3, e1 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 subsumption: (103) {G0,W7,D3,L1,V0,M1} I { ! op( e3, e1 ) ==> op( e2, e1 )
% 7.86/8.25 }.
% 7.86/8.25 parent0: (31159) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e2, e1 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25 permutation0:
% 7.86/8.25 0 ==> 0
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 eqswap: (33544) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e2, e1 ) }.
% 7.86/8.25 parent0[0]: (8769) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e4, e1 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 subsumption: (104) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e1 ) ==> op( e2, e1 )
% 7.86/8.25 }.
% 7.86/8.25 parent0: (33544) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e2, e1 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25 permutation0:
% 7.86/8.25 0 ==> 0
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 eqswap: (35931) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e0, e2 ) }.
% 7.86/8.25 parent0[0]: (8771) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e1, e2 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 subsumption: (106) {G0,W7,D3,L1,V0,M1} I { ! op( e1, e2 ) ==> op( e0, e2 )
% 7.86/8.25 }.
% 7.86/8.25 parent0: (35931) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e0, e2 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25 permutation0:
% 7.86/8.25 0 ==> 0
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 eqswap: (38319) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e0, e2 ) }.
% 7.86/8.25 parent0[0]: (8772) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e2, e2 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 subsumption: (107) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e2 ) ==> op( e0, e2 )
% 7.86/8.25 }.
% 7.86/8.25 parent0: (38319) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e0, e2 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25 permutation0:
% 7.86/8.25 0 ==> 0
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 *** allocated 1297440 integers for termspace/termends
% 7.86/8.25 eqswap: (40709) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e0, e2 ) }.
% 7.86/8.25 parent0[0]: (8774) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e4, e2 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 subsumption: (109) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e2 ) ==> op( e0, e2 )
% 7.86/8.25 }.
% 7.86/8.25 parent0: (40709) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e0, e2 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25 permutation0:
% 7.86/8.25 0 ==> 0
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 eqswap: (43102) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e1, e2 ) }.
% 7.86/8.25 parent0[0]: (8777) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e4, e2 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 subsumption: (112) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e2 ) ==> op( e1, e2 )
% 7.86/8.25 }.
% 7.86/8.25 parent0: (43102) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e1, e2 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25 permutation0:
% 7.86/8.25 0 ==> 0
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 eqswap: (45497) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e2, e2 ) }.
% 7.86/8.25 parent0[0]: (8779) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e4, e2 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 subsumption: (114) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e2 ) ==> op( e2, e2 )
% 7.86/8.25 }.
% 7.86/8.25 parent0: (45497) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e2, e2 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25 permutation0:
% 7.86/8.25 0 ==> 0
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 *** allocated 1946160 integers for clauses
% 7.86/8.25 eqswap: (47905) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e0, e4 ) }.
% 7.86/8.25 parent0[0]: (8792) {G0,W7,D3,L1,V0,M1} { ! op( e0, e4 ) = op( e2, e4 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 subsumption: (127) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e4 ) ==> op( e0, e4 )
% 7.86/8.25 }.
% 7.86/8.25 parent0: (47905) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e0, e4 ) }.
% 7.86/8.25 substitution0:
% 7.86/8.25 end
% 7.86/8.25 permutation0:
% 7.86/8.25 0 ==> 0
% 7.86/8.25 end
% 7.86/8.25
% 7.86/8.25 eqswap: (50316) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e1, e4 ) }.
% 7.86/8.25 parent0[0]: (8795) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e2, e4 ) }.
% 7.86/8.25 substitution0:
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 subsumption: (130) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e4 ) ==> op( e1, e4 )
% 8.36/8.76 }.
% 8.36/8.76 parent0: (50316) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e1, e4 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76 permutation0:
% 8.36/8.76 0 ==> 0
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 eqswap: (52729) {G0,W7,D3,L1,V0,M1} { ! op( e4, e4 ) = op( e1, e4 ) }.
% 8.36/8.76 parent0[0]: (8797) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e4, e4 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 subsumption: (132) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e4 ) ==> op( e1, e4 )
% 8.36/8.76 }.
% 8.36/8.76 parent0: (52729) {G0,W7,D3,L1,V0,M1} { ! op( e4, e4 ) = op( e1, e4 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76 permutation0:
% 8.36/8.76 0 ==> 0
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 eqswap: (55143) {G0,W7,D3,L1,V0,M1} { ! op( e3, e4 ) = op( e2, e4 ) }.
% 8.36/8.76 parent0[0]: (8798) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e3, e4 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 subsumption: (133) {G0,W7,D3,L1,V0,M1} I { ! op( e3, e4 ) ==> op( e2, e4 )
% 8.36/8.76 }.
% 8.36/8.76 parent0: (55143) {G0,W7,D3,L1,V0,M1} { ! op( e3, e4 ) = op( e2, e4 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76 permutation0:
% 8.36/8.76 0 ==> 0
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 *** allocated 1946160 integers for termspace/termends
% 8.36/8.76 eqswap: (57558) {G0,W7,D3,L1,V0,M1} { ! op( e4, e4 ) = op( e2, e4 ) }.
% 8.36/8.76 parent0[0]: (8799) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e4, e4 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 subsumption: (134) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e4 ) ==> op( e2, e4 )
% 8.36/8.76 }.
% 8.36/8.76 parent0: (57558) {G0,W7,D3,L1,V0,M1} { ! op( e4, e4 ) = op( e2, e4 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76 permutation0:
% 8.36/8.76 0 ==> 0
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 eqswap: (59975) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e0, e0 ) }.
% 8.36/8.76 parent0[0]: (8801) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e1 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 subsumption: (136) {G0,W7,D3,L1,V0,M1} I { ! op( e0, e1 ) ==> op( e0, e0 )
% 8.36/8.76 }.
% 8.36/8.76 parent0: (59975) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e0, e0 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76 permutation0:
% 8.36/8.76 0 ==> 0
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 eqswap: (62396) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e0, e1 ) }.
% 8.36/8.76 parent0[0]: (8805) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e0, e2 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 subsumption: (140) {G0,W7,D3,L1,V0,M1} I { ! op( e0, e2 ) ==> op( e0, e1 )
% 8.36/8.76 }.
% 8.36/8.76 parent0: (62396) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e0, e1 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76 permutation0:
% 8.36/8.76 0 ==> 0
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 eqswap: (64824) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e1, e0 ) }.
% 8.36/8.76 parent0[0]: (8812) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e2 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 subsumption: (147) {G0,W7,D3,L1,V0,M1} I { ! op( e1, e2 ) ==> op( e1, e0 )
% 8.36/8.76 }.
% 8.36/8.76 parent0: (64824) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e1, e0 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76 permutation0:
% 8.36/8.76 0 ==> 0
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 eqswap: (67256) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e1, e1 ) }.
% 8.36/8.76 parent0[0]: (8816) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e1, e3 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 subsumption: (151) {G0,W7,D3,L1,V0,M1} I { ! op( e1, e3 ) ==> op( e1, e1 )
% 8.36/8.76 }.
% 8.36/8.76 parent0: (67256) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e1, e1 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76 permutation0:
% 8.36/8.76 0 ==> 0
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 eqswap: (69689) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e1, e1 ) }.
% 8.36/8.76 parent0[0]: (8817) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e1, e4 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 subsumption: (152) {G0,W7,D3,L1,V0,M1} I { ! op( e1, e4 ) ==> op( e1, e1 )
% 8.36/8.76 }.
% 8.36/8.76 parent0: (69689) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e1, e1 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76 permutation0:
% 8.36/8.76 0 ==> 0
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 eqswap: (72124) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e1, e2 ) }.
% 8.36/8.76 parent0[0]: (8819) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e1, e4 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 subsumption: (154) {G0,W7,D3,L1,V0,M1} I { ! op( e1, e4 ) ==> op( e1, e2 )
% 8.36/8.76 }.
% 8.36/8.76 parent0: (72124) {G0,W7,D3,L1,V0,M1} { ! op( e1, e4 ) = op( e1, e2 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76 permutation0:
% 8.36/8.76 0 ==> 0
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 *** allocated 2919240 integers for clauses
% 8.36/8.76 eqswap: (74561) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e0 ) }.
% 8.36/8.76 parent0[0]: (8821) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e1 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 subsumption: (156) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e1 ) ==> op( e2, e0 )
% 8.36/8.76 }.
% 8.36/8.76 parent0: (74561) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e0 ) }.
% 8.36/8.76 substitution0:
% 8.36/8.76 end
% 8.36/8.76 permutation0:
% 8.36/8.76 0 ==> 0
% 8.36/8.76 end
% 8.36/8.76
% 8.36/8.76 eqswap: (77001) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e2, e0 ) }.
% 8.36/8.76 parent0[0]: (8824) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e4 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 subsumption: (159) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e4 ) ==> op( e2, e0 )
% 8.85/9.27 }.
% 8.85/9.27 parent0: (77001) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e2, e0 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27 permutation0:
% 8.85/9.27 0 ==> 0
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 eqswap: (79442) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e2, e1 ) }.
% 8.85/9.27 parent0[0]: (8825) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e2 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 subsumption: (160) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e2 ) ==> op( e2, e1 )
% 8.85/9.27 }.
% 8.85/9.27 parent0: (79442) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e2, e1 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27 permutation0:
% 8.85/9.27 0 ==> 0
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 eqswap: (81884) {G0,W7,D3,L1,V0,M1} { ! op( e2, e3 ) = op( e2, e1 ) }.
% 8.85/9.27 parent0[0]: (8826) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e3 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 subsumption: (161) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e3 ) ==> op( e2, e1 )
% 8.85/9.27 }.
% 8.85/9.27 parent0: (81884) {G0,W7,D3,L1,V0,M1} { ! op( e2, e3 ) = op( e2, e1 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27 permutation0:
% 8.85/9.27 0 ==> 0
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 *** allocated 2919240 integers for termspace/termends
% 8.85/9.27 eqswap: (84327) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e2, e1 ) }.
% 8.85/9.27 parent0[0]: (8827) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e4 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 subsumption: (162) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e4 ) ==> op( e2, e1 )
% 8.85/9.27 }.
% 8.85/9.27 parent0: (84327) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e2, e1 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27 permutation0:
% 8.85/9.27 0 ==> 0
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 eqswap: (86772) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e2, e2 ) }.
% 8.85/9.27 parent0[0]: (8829) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e2, e4 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 subsumption: (164) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e4 ) ==> op( e2, e2 )
% 8.85/9.27 }.
% 8.85/9.27 parent0: (86772) {G0,W7,D3,L1,V0,M1} { ! op( e2, e4 ) = op( e2, e2 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27 permutation0:
% 8.85/9.27 0 ==> 0
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 eqswap: (89230) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e4, e0 ) }.
% 8.85/9.27 parent0[0]: (8842) {G0,W7,D3,L1,V0,M1} { ! op( e4, e0 ) = op( e4, e2 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 subsumption: (177) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e2 ) ==> op( e4, e0 )
% 8.85/9.27 }.
% 8.85/9.27 parent0: (89230) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e4, e0 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27 permutation0:
% 8.85/9.27 0 ==> 0
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 eqswap: (91691) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e4, e1 ) }.
% 8.85/9.27 parent0[0]: (8845) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e4, e2 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 subsumption: (180) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e2 ) ==> op( e4, e1 )
% 8.85/9.27 }.
% 8.85/9.27 parent0: (91691) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e4, e1 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27 permutation0:
% 8.85/9.27 0 ==> 0
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 eqswap: (94154) {G0,W7,D3,L1,V0,M1} { ! op( e4, e4 ) = op( e4, e1 ) }.
% 8.85/9.27 parent0[0]: (8847) {G0,W7,D3,L1,V0,M1} { ! op( e4, e1 ) = op( e4, e4 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 subsumption: (182) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e4 ) ==> op( e4, e1 )
% 8.85/9.27 }.
% 8.85/9.27 parent0: (94154) {G0,W7,D3,L1,V0,M1} { ! op( e4, e4 ) = op( e4, e1 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27 permutation0:
% 8.85/9.27 0 ==> 0
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 eqswap: (96618) {G0,W7,D3,L1,V0,M1} { ! op( e4, e3 ) = op( e4, e2 ) }.
% 8.85/9.27 parent0[0]: (8848) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e4, e3 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 subsumption: (183) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e3 ) ==> op( e4, e2 )
% 8.85/9.27 }.
% 8.85/9.27 parent0: (96618) {G0,W7,D3,L1,V0,M1} { ! op( e4, e3 ) = op( e4, e2 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27 permutation0:
% 8.85/9.27 0 ==> 0
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 eqswap: (99083) {G0,W7,D3,L1,V0,M1} { ! op( e4, e4 ) = op( e4, e2 ) }.
% 8.85/9.27 parent0[0]: (8849) {G0,W7,D3,L1,V0,M1} { ! op( e4, e2 ) = op( e4, e4 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 subsumption: (184) {G0,W7,D3,L1,V0,M1} I { ! op( e4, e4 ) ==> op( e4, e2 )
% 8.85/9.27 }.
% 8.85/9.27 parent0: (99083) {G0,W7,D3,L1,V0,M1} { ! op( e4, e4 ) = op( e4, e2 ) }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27 permutation0:
% 8.85/9.27 0 ==> 0
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 eqswap: (101550) {G0,W3,D2,L1,V0,M1} { ! e1 = e0 }.
% 8.85/9.27 parent0[0]: (8851) {G0,W3,D2,L1,V0,M1} { ! e0 = e1 }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 subsumption: (186) {G0,W3,D2,L1,V0,M1} I { ! e1 ==> e0 }.
% 8.85/9.27 parent0: (101550) {G0,W3,D2,L1,V0,M1} { ! e1 = e0 }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27 permutation0:
% 8.85/9.27 0 ==> 0
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 eqswap: (104018) {G0,W3,D2,L1,V0,M1} { ! e2 = e0 }.
% 8.85/9.27 parent0[0]: (8852) {G0,W3,D2,L1,V0,M1} { ! e0 = e2 }.
% 8.85/9.27 substitution0:
% 8.85/9.27 end
% 8.85/9.27
% 8.85/9.27 subsumption: (187) {G0,W3,D2,L1,V0,M1} I { ! e2 ==> e0 }.
% 9.36/9.75 parent0: (104018) {G0,W3,D2,L1,V0,M1} { ! e2 = e0 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75 permutation0:
% 9.36/9.75 0 ==> 0
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 eqswap: (106487) {G0,W3,D2,L1,V0,M1} { ! e3 = e0 }.
% 9.36/9.75 parent0[0]: (8853) {G0,W3,D2,L1,V0,M1} { ! e0 = e3 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 subsumption: (188) {G0,W3,D2,L1,V0,M1} I { ! e3 ==> e0 }.
% 9.36/9.75 parent0: (106487) {G0,W3,D2,L1,V0,M1} { ! e3 = e0 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75 permutation0:
% 9.36/9.75 0 ==> 0
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 eqswap: (108957) {G0,W3,D2,L1,V0,M1} { ! e4 = e0 }.
% 9.36/9.75 parent0[0]: (8854) {G0,W3,D2,L1,V0,M1} { ! e0 = e4 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 subsumption: (189) {G0,W3,D2,L1,V0,M1} I { ! e4 ==> e0 }.
% 9.36/9.75 parent0: (108957) {G0,W3,D2,L1,V0,M1} { ! e4 = e0 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75 permutation0:
% 9.36/9.75 0 ==> 0
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 eqswap: (111428) {G0,W3,D2,L1,V0,M1} { ! e2 = e1 }.
% 9.36/9.75 parent0[0]: (8855) {G0,W3,D2,L1,V0,M1} { ! e1 = e2 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 subsumption: (190) {G0,W3,D2,L1,V0,M1} I { ! e2 ==> e1 }.
% 9.36/9.75 parent0: (111428) {G0,W3,D2,L1,V0,M1} { ! e2 = e1 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75 permutation0:
% 9.36/9.75 0 ==> 0
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 eqswap: (113900) {G0,W3,D2,L1,V0,M1} { ! e3 = e1 }.
% 9.36/9.75 parent0[0]: (8856) {G0,W3,D2,L1,V0,M1} { ! e1 = e3 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 subsumption: (191) {G0,W3,D2,L1,V0,M1} I { ! e3 ==> e1 }.
% 9.36/9.75 parent0: (113900) {G0,W3,D2,L1,V0,M1} { ! e3 = e1 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75 permutation0:
% 9.36/9.75 0 ==> 0
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 *** allocated 4378860 integers for clauses
% 9.36/9.75 eqswap: (116373) {G0,W3,D2,L1,V0,M1} { ! e4 = e1 }.
% 9.36/9.75 parent0[0]: (8857) {G0,W3,D2,L1,V0,M1} { ! e1 = e4 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 subsumption: (192) {G0,W3,D2,L1,V0,M1} I { ! e4 ==> e1 }.
% 9.36/9.75 parent0: (116373) {G0,W3,D2,L1,V0,M1} { ! e4 = e1 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75 permutation0:
% 9.36/9.75 0 ==> 0
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 eqswap: (118847) {G0,W3,D2,L1,V0,M1} { ! e3 = e2 }.
% 9.36/9.75 parent0[0]: (8858) {G0,W3,D2,L1,V0,M1} { ! e2 = e3 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 subsumption: (193) {G0,W3,D2,L1,V0,M1} I { ! e3 ==> e2 }.
% 9.36/9.75 parent0: (118847) {G0,W3,D2,L1,V0,M1} { ! e3 = e2 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75 permutation0:
% 9.36/9.75 0 ==> 0
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 eqswap: (121322) {G0,W3,D2,L1,V0,M1} { ! e4 = e2 }.
% 9.36/9.75 parent0[0]: (8859) {G0,W3,D2,L1,V0,M1} { ! e2 = e4 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 subsumption: (194) {G0,W3,D2,L1,V0,M1} I { ! e4 ==> e2 }.
% 9.36/9.75 parent0: (121322) {G0,W3,D2,L1,V0,M1} { ! e4 = e2 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75 permutation0:
% 9.36/9.75 0 ==> 0
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 *** allocated 4378860 integers for termspace/termends
% 9.36/9.75 eqswap: (123799) {G0,W11,D5,L1,V0,M1} { op( e1, op( op( e1, e1 ), op( e1,
% 9.36/9.75 e1 ) ) ) = e0 }.
% 9.36/9.75 parent0[0]: (8861) {G0,W11,D5,L1,V0,M1} { e0 = op( e1, op( op( e1, e1 ),
% 9.36/9.75 op( e1, e1 ) ) ) }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 subsumption: (196) {G0,W11,D5,L1,V0,M1} I { op( e1, op( op( e1, e1 ), op(
% 9.36/9.75 e1, e1 ) ) ) ==> e0 }.
% 9.36/9.75 parent0: (123799) {G0,W11,D5,L1,V0,M1} { op( e1, op( op( e1, e1 ), op( e1
% 9.36/9.75 , e1 ) ) ) = e0 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75 permutation0:
% 9.36/9.75 0 ==> 0
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 eqswap: (126277) {G0,W9,D4,L1,V0,M1} { op( op( e1, e1 ), op( e1, e1 ) ) =
% 9.36/9.75 e2 }.
% 9.36/9.75 parent0[0]: (8862) {G0,W9,D4,L1,V0,M1} { e2 = op( op( e1, e1 ), op( e1, e1
% 9.36/9.75 ) ) }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 subsumption: (197) {G0,W9,D4,L1,V0,M1} I { op( op( e1, e1 ), op( e1, e1 ) )
% 9.36/9.75 ==> e2 }.
% 9.36/9.75 parent0: (126277) {G0,W9,D4,L1,V0,M1} { op( op( e1, e1 ), op( e1, e1 ) ) =
% 9.36/9.75 e2 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75 permutation0:
% 9.36/9.75 0 ==> 0
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 paramod: (128963) {G1,W11,D5,L1,V0,M1} { e3 = op( op( op( e1, e1 ), op( e1
% 9.36/9.75 , e1 ) ), e2 ) }.
% 9.36/9.75 parent0[0]: (197) {G0,W9,D4,L1,V0,M1} I { op( op( e1, e1 ), op( e1, e1 ) )
% 9.36/9.75 ==> e2 }.
% 9.36/9.75 parent1[0; 10]: (8863) {G0,W17,D5,L1,V0,M1} { e3 = op( op( op( e1, e1 ),
% 9.36/9.75 op( e1, e1 ) ), op( op( e1, e1 ), op( e1, e1 ) ) ) }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75 substitution1:
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 paramod: (128964) {G1,W5,D3,L1,V0,M1} { e3 = op( e2, e2 ) }.
% 9.36/9.75 parent0[0]: (197) {G0,W9,D4,L1,V0,M1} I { op( op( e1, e1 ), op( e1, e1 ) )
% 9.36/9.75 ==> e2 }.
% 9.36/9.75 parent1[0; 3]: (128963) {G1,W11,D5,L1,V0,M1} { e3 = op( op( op( e1, e1 ),
% 9.36/9.75 op( e1, e1 ) ), e2 ) }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75 substitution1:
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 eqswap: (128966) {G1,W5,D3,L1,V0,M1} { op( e2, e2 ) = e3 }.
% 9.36/9.75 parent0[0]: (128964) {G1,W5,D3,L1,V0,M1} { e3 = op( e2, e2 ) }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75
% 9.36/9.75 subsumption: (198) {G1,W5,D3,L1,V0,M1} I;d(197) { op( e2, e2 ) ==> e3 }.
% 9.36/9.75 parent0: (128966) {G1,W5,D3,L1,V0,M1} { op( e2, e2 ) = e3 }.
% 9.36/9.75 substitution0:
% 9.36/9.75 end
% 9.36/9.75 permutation0:
% 10.57/11.00 0 ==> 0
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 eqswap: (131447) {G0,W5,D3,L1,V0,M1} { op( e1, e1 ) = e4 }.
% 10.57/11.00 parent0[0]: (8864) {G0,W5,D3,L1,V0,M1} { e4 = op( e1, e1 ) }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 subsumption: (199) {G0,W5,D3,L1,V0,M1} I { op( e1, e1 ) ==> e4 }.
% 10.57/11.00 parent0: (131447) {G0,W5,D3,L1,V0,M1} { op( e1, e1 ) = e4 }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00 permutation0:
% 10.57/11.00 0 ==> 0
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 subsumption: (201) {G0,W1,D1,L1,V0,M1} I { alpha2 }.
% 10.57/11.00 parent0: (8871) {G0,W1,D1,L1,V0,M1} { alpha2 }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00 permutation0:
% 10.57/11.00 0 ==> 0
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 subsumption: (202) {G0,W1,D1,L1,V0,M1} I { alpha4 }.
% 10.57/11.00 parent0: (8872) {G0,W1,D1,L1,V0,M1} { alpha4 }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00 permutation0:
% 10.57/11.00 0 ==> 0
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 subsumption: (204) {G0,W8,D4,L2,V0,M2} I { alpha11, ! op( e4, op( e4, e4 )
% 10.57/11.00 ) ==> e4 }.
% 10.57/11.00 parent0: (8874) {G0,W8,D4,L2,V0,M2} { alpha11, ! op( e4, op( e4, e4 ) ) =
% 10.57/11.00 e4 }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00 permutation0:
% 10.57/11.00 0 ==> 0
% 10.57/11.00 1 ==> 1
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 subsumption: (205) {G0,W8,D4,L2,V0,M2} I { alpha11, op( e4, op( e4, e4 ) )
% 10.57/11.00 ==> e4 }.
% 10.57/11.00 parent0: (8875) {G0,W8,D4,L2,V0,M2} { alpha11, op( e4, op( e4, e4 ) ) = e4
% 10.57/11.00 }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00 permutation0:
% 10.57/11.00 0 ==> 0
% 10.57/11.00 1 ==> 1
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 subsumption: (206) {G0,W9,D4,L3,V0,M3} I { ! alpha11, alpha16, ! op( e3, op
% 10.57/11.00 ( e3, e4 ) ) ==> e4 }.
% 10.57/11.00 parent0: (8876) {G0,W9,D4,L3,V0,M3} { ! alpha11, alpha16, ! op( e3, op( e3
% 10.57/11.00 , e4 ) ) = e4 }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00 permutation0:
% 10.57/11.00 0 ==> 0
% 10.57/11.00 1 ==> 1
% 10.57/11.00 2 ==> 2
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 subsumption: (211) {G0,W9,D4,L3,V0,M3} I { ! alpha16, alpha20, op( e4, op(
% 10.57/11.00 e2, e4 ) ) ==> e2 }.
% 10.57/11.00 parent0: (8881) {G0,W9,D4,L3,V0,M3} { ! alpha16, alpha20, op( e4, op( e2,
% 10.57/11.00 e4 ) ) = e2 }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00 permutation0:
% 10.57/11.00 0 ==> 0
% 10.57/11.00 1 ==> 1
% 10.57/11.00 2 ==> 2
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 subsumption: (215) {G0,W9,D4,L3,V0,M3} I { ! alpha20, alpha23, op( e4, op(
% 10.57/11.00 e1, e4 ) ) ==> e1 }.
% 10.57/11.00 parent0: (8885) {G0,W9,D4,L3,V0,M3} { ! alpha20, alpha23, op( e4, op( e1,
% 10.57/11.00 e4 ) ) = e1 }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00 permutation0:
% 10.57/11.00 0 ==> 0
% 10.57/11.00 1 ==> 1
% 10.57/11.00 2 ==> 2
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 subsumption: (218) {G0,W8,D4,L2,V0,M2} I { ! alpha23, ! op( e0, op( e0, e4
% 10.57/11.00 ) ) ==> e4 }.
% 10.57/11.00 parent0: (8888) {G0,W8,D4,L2,V0,M2} { ! alpha23, ! op( e0, op( e0, e4 ) )
% 10.57/11.00 = e4 }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00 permutation0:
% 10.57/11.00 0 ==> 0
% 10.57/11.00 1 ==> 1
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 resolution: (155258) {G1,W8,D4,L2,V0,M2} { alpha8, ! op( e4, op( e4, e2 )
% 10.57/11.00 ) = e2 }.
% 10.57/11.00 parent0[0]: (8910) {G0,W9,D4,L3,V0,M3} { ! alpha4, alpha8, ! op( e4, op(
% 10.57/11.00 e4, e2 ) ) = e2 }.
% 10.57/11.00 parent1[0]: (202) {G0,W1,D1,L1,V0,M1} I { alpha4 }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00 substitution1:
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 subsumption: (237) {G1,W8,D4,L2,V0,M2} I;r(202) { alpha8, ! op( e4, op( e4
% 10.57/11.00 , e2 ) ) ==> e2 }.
% 10.57/11.00 parent0: (155258) {G1,W8,D4,L2,V0,M2} { alpha8, ! op( e4, op( e4, e2 ) ) =
% 10.57/11.00 e2 }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00 permutation0:
% 10.57/11.00 0 ==> 0
% 10.57/11.00 1 ==> 1
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 resolution: (157948) {G1,W8,D4,L2,V0,M2} { alpha8, op( e2, op( e4, e2 ) )
% 10.57/11.00 = e4 }.
% 10.57/11.00 parent0[0]: (8911) {G0,W9,D4,L3,V0,M3} { ! alpha4, alpha8, op( e2, op( e4
% 10.57/11.00 , e2 ) ) = e4 }.
% 10.57/11.00 parent1[0]: (202) {G0,W1,D1,L1,V0,M1} I { alpha4 }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00 substitution1:
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 subsumption: (238) {G1,W8,D4,L2,V0,M2} I;r(202) { alpha8, op( e2, op( e4,
% 10.57/11.00 e2 ) ) ==> e4 }.
% 10.57/11.00 parent0: (157948) {G1,W8,D4,L2,V0,M2} { alpha8, op( e2, op( e4, e2 ) ) =
% 10.57/11.00 e4 }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00 permutation0:
% 10.57/11.00 0 ==> 0
% 10.57/11.00 1 ==> 1
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 subsumption: (239) {G0,W9,D4,L3,V0,M3} I { ! alpha8, alpha13, ! op( e3, op
% 10.57/11.00 ( e3, e2 ) ) ==> e2 }.
% 10.57/11.00 parent0: (8914) {G0,W9,D4,L3,V0,M3} { ! alpha8, alpha13, ! op( e3, op( e3
% 10.57/11.00 , e2 ) ) = e2 }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00 permutation0:
% 10.57/11.00 0 ==> 0
% 10.57/11.00 1 ==> 1
% 10.57/11.00 2 ==> 2
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 paramod: (190977) {G1,W7,D3,L3,V0,M3} { ! op( e2, e3 ) = e2, ! alpha13,
% 10.57/11.00 alpha18 }.
% 10.57/11.00 parent0[0]: (198) {G1,W5,D3,L1,V0,M1} I;d(197) { op( e2, e2 ) ==> e3 }.
% 10.57/11.00 parent1[2; 4]: (8918) {G0,W9,D4,L3,V0,M3} { ! alpha13, alpha18, ! op( e2,
% 10.57/11.00 op( e2, e2 ) ) = e2 }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00 substitution1:
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 subsumption: (243) {G2,W7,D3,L3,V0,M3} I;d(198) { ! alpha13, alpha18, ! op
% 10.57/11.00 ( e2, e3 ) ==> e2 }.
% 10.57/11.00 parent0: (190977) {G1,W7,D3,L3,V0,M3} { ! op( e2, e3 ) = e2, ! alpha13,
% 10.57/11.00 alpha18 }.
% 10.57/11.00 substitution0:
% 10.57/11.00 end
% 10.57/11.00 permutation0:
% 10.57/11.00 0 ==> 2
% 10.57/11.00 1 ==> 0
% 10.57/11.00 2 ==> 1
% 10.57/11.00 end
% 10.57/11.00
% 10.57/11.00 paramod: (221324) {G1,W7,D3,L3,V0,M3} { op( e2, e3 ) = e2, ! alpha13,
% 10.57/11.00 alpha18 }.
% 10.57/11.00 parent0[0]: (198) {G1,W5,D3,L1,V0,M1} I;d(197) { op( e2, e2 ) ==> e3 }.
% 11.76/12.16 parent1[2; 3]: (8919) {G0,W9,D4,L3,V0,M3} { ! alpha13, alpha18, op( e2, op
% 11.76/12.16 ( e2, e2 ) ) = e2 }.
% 11.76/12.16 substitution0:
% 11.76/12.16 end
% 11.76/12.16 substitution1:
% 11.76/12.16 end
% 11.76/12.16
% 11.76/12.16 subsumption: (244) {G2,W7,D3,L3,V0,M3} I;d(198) { ! alpha13, alpha18, op(
% 11.76/12.16 e2, e3 ) ==> e2 }.
% 11.76/12.16 parent0: (221324) {G1,W7,D3,L3,V0,M3} { op( e2, e3 ) = e2, ! alpha13,
% 11.76/12.16 alpha18 }.
% 11.76/12.16 substitution0:
% 11.76/12.16 end
% 11.76/12.16 permutation0:
% 11.76/12.16 0 ==> 2
% 11.76/12.16 1 ==> 0
% 11.76/12.16 2 ==> 1
% 11.76/12.16 end
% 11.76/12.16
% 11.76/12.16 subsumption: (247) {G0,W9,D4,L3,V0,M3} I { ! alpha18, alpha22, op( e2, op(
% 11.76/12.16 e1, e2 ) ) ==> e1 }.
% 11.76/12.16 parent0: (8923) {G0,W9,D4,L3,V0,M3} { ! alpha18, alpha22, op( e2, op( e1,
% 11.76/12.16 e2 ) ) = e1 }.
% 11.76/12.16 substitution0:
% 11.76/12.16 end
% 11.76/12.16 permutation0:
% 11.76/12.16 0 ==> 0
% 11.76/12.16 1 ==> 1
% 11.76/12.16 2 ==> 2
% 11.76/12.16 end
% 11.76/12.16
% 11.76/12.16 subsumption: (251) {G0,W8,D4,L2,V0,M2} I { ! alpha22, op( e2, op( e0, e2 )
% 11.76/12.16 ) ==> e0 }.
% 11.76/12.16 parent0: (8927) {G0,W8,D4,L2,V0,M2} { ! alpha22, op( e2, op( e0, e2 ) ) =
% 11.76/12.16 e0 }.
% 11.76/12.16 substitution0:
% 11.76/12.16 end
% 11.76/12.16 permutation0:
% 11.76/12.16 0 ==> 0
% 11.76/12.16 1 ==> 1
% 11.76/12.16 end
% 11.76/12.16
% 11.76/12.16 resolution: (229437) {G1,W8,D4,L2,V0,M2} { alpha5, ! op( e4, op( e4, e1 )
% 11.76/12.16 ) = e1 }.
% 11.76/12.16 parent0[0]: (8929) {G0,W9,D4,L3,V0,M3} { ! alpha2, alpha5, ! op( e4, op(
% 11.76/12.16 e4, e1 ) ) = e1 }.
% 11.76/12.16 parent1[0]: (201) {G0,W1,D1,L1,V0,M1} I { alpha2 }.
% 11.76/12.16 substitution0:
% 11.76/12.16 end
% 11.76/12.16 substitution1:
% 11.76/12.16 end
% 11.76/12.16
% 11.76/12.16 subsumption: (253) {G1,W8,D4,L2,V0,M2} I;r(201) { alpha5, ! op( e4, op( e4
% 11.76/12.16 , e1 ) ) ==> e1 }.
% 11.76/12.16 parent0: (229437) {G1,W8,D4,L2,V0,M2} { alpha5, ! op( e4, op( e4, e1 ) ) =
% 11.76/12.16 e1 }.
% 11.76/12.16 substitution0:
% 11.76/12.16 end
% 11.76/12.16 permutation0:
% 11.76/12.16 0 ==> 0
% 11.76/12.16 1 ==> 1
% 11.76/12.16 end
% 11.76/12.16
% 11.76/12.16 *** allocated 6568290 integers for clauses
% 11.76/12.16 resolution: (232152) {G1,W8,D4,L2,V0,M2} { alpha5, op( e1, op( e4, e1 ) )
% 11.76/12.16 = e4 }.
% 11.76/12.16 parent0[0]: (8930) {G0,W9,D4,L3,V0,M3} { ! alpha2, alpha5, op( e1, op( e4
% 11.76/12.16 , e1 ) ) = e4 }.
% 11.76/12.16 parent1[0]: (201) {G0,W1,D1,L1,V0,M1} I { alpha2 }.
% 11.76/12.16 substitution0:
% 11.76/12.16 end
% 11.76/12.16 substitution1:
% 11.76/12.16 end
% 11.76/12.16
% 11.76/12.16 subsumption: (254) {G1,W8,D4,L2,V0,M2} I;r(201) { alpha5, op( e1, op( e4,
% 11.76/12.16 e1 ) ) ==> e4 }.
% 11.76/12.16 parent0: (232152) {G1,W8,D4,L2,V0,M2} { alpha5, op( e1, op( e4, e1 ) ) =
% 11.76/12.16 e4 }.
% 11.76/12.16 substitution0:
% 11.76/12.16 end
% 11.76/12.16 permutation0:
% 11.76/12.16 0 ==> 0
% 11.76/12.16 1 ==> 1
% 11.76/12.16 end
% 11.76/12.16
% 11.76/12.16 subsumption: (255) {G0,W9,D4,L3,V0,M3} I { ! alpha5, alpha9, ! op( e3, op(
% 11.76/12.16 e3, e1 ) ) ==> e1 }.
% 11.76/12.16 parent0: (8933) {G0,W9,D4,L3,V0,M3} { ! alpha5, alpha9, ! op( e3, op( e3,
% 11.76/12.16 e1 ) ) = e1 }.
% 11.76/12.16 substitution0:
% 11.76/12.16 end
% 11.76/12.16 permutation0:
% 11.76/12.16 0 ==> 0
% 11.76/12.16 1 ==> 1
% 11.76/12.16 2 ==> 2
% 11.76/12.16 end
% 11.76/12.16
% 11.76/12.16 subsumption: (256) {G0,W9,D4,L3,V0,M3} I { ! alpha5, alpha9, op( e1, op( e3
% 11.76/12.16 , e1 ) ) ==> e3 }.
% 11.76/12.16 parent0: (8934) {G0,W9,D4,L3,V0,M3} { ! alpha5, alpha9, op( e1, op( e3, e1
% 11.76/12.16 ) ) = e3 }.
% 11.76/12.16 substitution0:
% 11.76/12.16 end
% 11.76/12.16 permutation0:
% 11.76/12.16 0 ==> 0
% 11.76/12.16 1 ==> 1
% 11.76/12.16 2 ==> 2
% 11.76/12.16 end
% 11.76/12.16
% 11.76/12.16 *** allocated 6568290 integers for termspace/termends
% 11.76/12.16 subsumption: (257) {G0,W2,D1,L2,V0,M2} I { ! alpha9, alpha5 }.
% 11.76/12.16 parent0: (8935) {G0,W2,D1,L2,V0,M2} { ! alpha9, alpha5 }.
% 11.76/12.16 substitution0:
% 11.76/12.16 end
% 11.76/12.16 permutation0:
% 11.76/12.16 0 ==> 0
% 11.76/12.16 1 ==> 1
% 11.76/12.16 end
% 11.76/12.16
% 11.76/12.16 subsumption: (259) {G0,W9,D4,L3,V0,M3} I { ! alpha9, alpha14, ! op( e2, op
% 11.76/12.16 ( e2, e1 ) ) ==> e1 }.
% 11.76/12.16 parent0: (8937) {G0,W9,D4,L3,V0,M3} { ! alpha9, alpha14, ! op( e2, op( e2
% 11.76/12.16 , e1 ) ) = e1 }.
% 11.76/12.16 substitution0:
% 11.76/12.16 end
% 11.76/12.16 permutation0:
% 11.76/12.16 0 ==> 0
% 11.76/12.16 1 ==> 1
% 11.76/12.16 2 ==> 2
% 11.76/12.16 end
% 11.76/12.16
% 11.76/12.16 subsumption: (260) {G0,W9,D4,L3,V0,M3} I { ! alpha9, alpha14, op( e1, op(
% 11.76/12.16 e2, e1 ) ) ==> e2 }.
% 11.76/12.16 parent0: (8938) {G0,W9,D4,L3,V0,M3} { ! alpha9, alpha14, op( e1, op( e2,
% 11.76/12.16 e1 ) ) = e2 }.
% 11.76/12.16 substitution0:
% 11.76/12.16 end
% 11.76/12.16 permutation0:
% 11.76/12.16 0 ==> 0
% 11.76/12.16 1 ==> 1
% 11.76/12.16 2 ==> 2
% 11.76/12.16 end
% 11.76/12.16
% 11.76/12.16 paramod: (276398) {G1,W7,D3,L3,V0,M3} { ! op( e1, e4 ) = e1, ! alpha14,
% 11.76/12.16 alpha19 }.
% 11.76/12.16 parent0[0]: (199) {G0,W5,D3,L1,V0,M1} I { op( e1, e1 ) ==> e4 }.
% 11.76/12.16 parent1[2; 4]: (8941) {G0,W9,D4,L3,V0,M3} { ! alpha14, alpha19, ! op( e1,
% 11.76/12.16 op( e1, e1 ) ) = e1 }.
% 11.76/12.16 substitution0:
% 11.76/12.16 end
% 11.76/12.16 substitution1:
% 11.76/12.16 end
% 11.76/12.16
% 11.76/12.16 subsumption: (263) {G1,W7,D3,L3,V0,M3} I;d(199) { ! alpha14, alpha19, ! op
% 11.76/12.16 ( e1, e4 ) ==> e1 }.
% 11.76/12.16 parent0: (276398) {G1,W7,D3,L3,V0,M3} { ! op( e1, e4 ) = e1, ! alpha14,
% 11.76/12.16 alpha19 }.
% 11.76/12.16 substitution0:
% 11.76/12.16 end
% 11.76/12.16 permutation0:
% 11.76/12.16 0 ==> 2
% 11.76/12.16 1 ==> 0
% 11.76/12.16 2 ==> 1
% 11.76/12.16 end
% 11.76/12.16
% 11.76/12.16 paramod: (307072) {G1,W7,D3,L3,V0,M3} { op( e1, e4 ) = e1, ! alpha14,
% 11.76/12.16 alpha19 }.
% 11.76/12.16 parent0[0]: (199) {G0,W5,D3,L1,V0,M1} I { op( e1, e1 ) ==> e4 }.
% 11.76/12.16 parent1[2; 3]: (8942) {G0,W9,D4,L3,V0,M3} { ! alpha14, alpha19, op( e1, op
% 11.76/12.16 ( e1, e1 ) ) = e1 }.
% 11.76/12.16 substitution0:
% 11.76/12.16 end
% 12.43/12.80 substitution1:
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 subsumption: (264) {G1,W7,D3,L3,V0,M3} I;d(199) { ! alpha14, alpha19, op(
% 12.43/12.80 e1, e4 ) ==> e1 }.
% 12.43/12.80 parent0: (307072) {G1,W7,D3,L3,V0,M3} { op( e1, e4 ) = e1, ! alpha14,
% 12.43/12.80 alpha19 }.
% 12.43/12.80 substitution0:
% 12.43/12.80 end
% 12.43/12.80 permutation0:
% 12.43/12.80 0 ==> 2
% 12.43/12.80 1 ==> 0
% 12.43/12.80 2 ==> 1
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 subsumption: (265) {G0,W2,D1,L2,V0,M2} I { ! alpha19, alpha14 }.
% 12.43/12.80 parent0: (8943) {G0,W2,D1,L2,V0,M2} { ! alpha19, alpha14 }.
% 12.43/12.80 substitution0:
% 12.43/12.80 end
% 12.43/12.80 permutation0:
% 12.43/12.80 0 ==> 0
% 12.43/12.80 1 ==> 1
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 subsumption: (266) {G0,W8,D4,L2,V0,M2} I { ! alpha19, ! op( e0, op( e0, e1
% 12.43/12.80 ) ) ==> e1 }.
% 12.43/12.80 parent0: (8945) {G0,W8,D4,L2,V0,M2} { ! alpha19, ! op( e0, op( e0, e1 ) )
% 12.43/12.80 = e1 }.
% 12.43/12.80 substitution0:
% 12.43/12.80 end
% 12.43/12.80 permutation0:
% 12.43/12.80 0 ==> 0
% 12.43/12.80 1 ==> 1
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 subsumption: (267) {G0,W8,D4,L2,V0,M2} I { ! alpha19, op( e1, op( e0, e1 )
% 12.43/12.80 ) ==> e0 }.
% 12.43/12.80 parent0: (8946) {G0,W8,D4,L2,V0,M2} { ! alpha19, op( e1, op( e0, e1 ) ) =
% 12.43/12.80 e0 }.
% 12.43/12.80 substitution0:
% 12.43/12.80 end
% 12.43/12.80 permutation0:
% 12.43/12.80 0 ==> 0
% 12.43/12.80 1 ==> 1
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 subsumption: (268) {G0,W15,D4,L3,V0,M3} I { op( e0, op( e0, e1 ) ) ==> e1,
% 12.43/12.80 ! op( e1, op( e0, e1 ) ) ==> e0, alpha19 }.
% 12.43/12.80 parent0: (8947) {G0,W15,D4,L3,V0,M3} { op( e0, op( e0, e1 ) ) = e1, ! op(
% 12.43/12.80 e1, op( e0, e1 ) ) = e0, alpha19 }.
% 12.43/12.80 substitution0:
% 12.43/12.80 end
% 12.43/12.80 permutation0:
% 12.43/12.80 0 ==> 0
% 12.43/12.80 1 ==> 1
% 12.43/12.80 2 ==> 2
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 subsumption: (271) {G0,W9,D4,L3,V0,M3} I { ! alpha3, alpha6, ! op( e3, op(
% 12.43/12.80 e3, e0 ) ) ==> e0 }.
% 12.43/12.80 parent0: (8952) {G0,W9,D4,L3,V0,M3} { ! alpha3, alpha6, ! op( e3, op( e3,
% 12.43/12.80 e0 ) ) = e0 }.
% 12.43/12.80 substitution0:
% 12.43/12.80 end
% 12.43/12.80 permutation0:
% 12.43/12.80 0 ==> 0
% 12.43/12.80 1 ==> 1
% 12.43/12.80 2 ==> 2
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 subsumption: (273) {G0,W2,D1,L2,V0,M2} I { ! alpha6, alpha3 }.
% 12.43/12.80 parent0: (8954) {G0,W2,D1,L2,V0,M2} { ! alpha6, alpha3 }.
% 12.43/12.80 substitution0:
% 12.43/12.80 end
% 12.43/12.80 permutation0:
% 12.43/12.80 0 ==> 0
% 12.43/12.80 1 ==> 1
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 subsumption: (275) {G0,W9,D4,L3,V0,M3} I { ! alpha6, alpha10, ! op( e2, op
% 12.43/12.80 ( e2, e0 ) ) ==> e0 }.
% 12.43/12.80 parent0: (8956) {G0,W9,D4,L3,V0,M3} { ! alpha6, alpha10, ! op( e2, op( e2
% 12.43/12.80 , e0 ) ) = e0 }.
% 12.43/12.80 substitution0:
% 12.43/12.80 end
% 12.43/12.80 permutation0:
% 12.43/12.80 0 ==> 0
% 12.43/12.80 1 ==> 1
% 12.43/12.80 2 ==> 2
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 subsumption: (277) {G0,W2,D1,L2,V0,M2} I { ! alpha10, alpha6 }.
% 12.43/12.80 parent0: (8958) {G0,W2,D1,L2,V0,M2} { ! alpha10, alpha6 }.
% 12.43/12.80 substitution0:
% 12.43/12.80 end
% 12.43/12.80 permutation0:
% 12.43/12.80 0 ==> 0
% 12.43/12.80 1 ==> 1
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 subsumption: (278) {G0,W15,D4,L3,V0,M3} I { op( e2, op( e2, e0 ) ) ==> e0,
% 12.43/12.80 ! op( e0, op( e2, e0 ) ) ==> e2, alpha6 }.
% 12.43/12.80 parent0: (8959) {G0,W15,D4,L3,V0,M3} { op( e2, op( e2, e0 ) ) = e0, ! op(
% 12.43/12.80 e0, op( e2, e0 ) ) = e2, alpha6 }.
% 12.43/12.80 substitution0:
% 12.43/12.80 end
% 12.43/12.80 permutation0:
% 12.43/12.80 0 ==> 0
% 12.43/12.80 1 ==> 1
% 12.43/12.80 2 ==> 2
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 subsumption: (279) {G0,W9,D4,L3,V0,M3} I { ! alpha10, alpha15, ! op( e1, op
% 12.43/12.80 ( e1, e0 ) ) ==> e0 }.
% 12.43/12.80 parent0: (8960) {G0,W9,D4,L3,V0,M3} { ! alpha10, alpha15, ! op( e1, op( e1
% 12.43/12.80 , e0 ) ) = e0 }.
% 12.43/12.80 substitution0:
% 12.43/12.80 end
% 12.43/12.80 permutation0:
% 12.43/12.80 0 ==> 0
% 12.43/12.80 1 ==> 1
% 12.43/12.80 2 ==> 2
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 subsumption: (282) {G0,W15,D4,L3,V0,M3} I { op( e1, op( e1, e0 ) ) ==> e0,
% 12.43/12.80 ! op( e0, op( e1, e0 ) ) ==> e1, alpha10 }.
% 12.43/12.80 parent0: (8963) {G0,W15,D4,L3,V0,M3} { op( e1, op( e1, e0 ) ) = e0, ! op(
% 12.43/12.80 e0, op( e1, e0 ) ) = e1, alpha10 }.
% 12.43/12.80 substitution0:
% 12.43/12.80 end
% 12.43/12.80 permutation0:
% 12.43/12.80 0 ==> 0
% 12.43/12.80 1 ==> 1
% 12.43/12.80 2 ==> 2
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 subsumption: (283) {G0,W8,D4,L2,V0,M2} I { ! alpha15, ! op( e0, op( e0, e0
% 12.43/12.80 ) ) ==> e0 }.
% 12.43/12.80 parent0: (8964) {G0,W8,D4,L2,V0,M2} { ! alpha15, ! op( e0, op( e0, e0 ) )
% 12.43/12.80 = e0 }.
% 12.43/12.80 substitution0:
% 12.43/12.80 end
% 12.43/12.80 permutation0:
% 12.43/12.80 0 ==> 0
% 12.43/12.80 1 ==> 1
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 subsumption: (284) {G0,W8,D4,L2,V0,M2} I { ! alpha15, op( e0, op( e0, e0 )
% 12.43/12.80 ) ==> e0 }.
% 12.43/12.80 parent0: (8965) {G0,W8,D4,L2,V0,M2} { ! alpha15, op( e0, op( e0, e0 ) ) =
% 12.43/12.80 e0 }.
% 12.43/12.80 substitution0:
% 12.43/12.80 end
% 12.43/12.80 permutation0:
% 12.43/12.80 0 ==> 0
% 12.43/12.80 1 ==> 1
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 paramod: (342707) {G1,W5,D3,L1,V0,M1} { ! op( e2, e4 ) ==> e3 }.
% 12.43/12.80 parent0[0]: (198) {G1,W5,D3,L1,V0,M1} I;d(197) { op( e2, e2 ) ==> e3 }.
% 12.43/12.80 parent1[0; 5]: (164) {G0,W7,D3,L1,V0,M1} I { ! op( e2, e4 ) ==> op( e2, e2
% 12.43/12.80 ) }.
% 12.43/12.80 substitution0:
% 12.43/12.80 end
% 12.43/12.80 substitution1:
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 subsumption: (335) {G2,W5,D3,L1,V0,M1} S(164);d(198) { ! op( e2, e4 ) ==>
% 12.43/12.80 e3 }.
% 12.43/12.80 parent0: (342707) {G1,W5,D3,L1,V0,M1} { ! op( e2, e4 ) ==> e3 }.
% 12.43/12.80 substitution0:
% 12.43/12.80 end
% 12.43/12.80 permutation0:
% 12.43/12.80 0 ==> 0
% 12.43/12.80 end
% 12.43/12.80
% 12.43/12.80 paramod: (342711) {G1,W5,D3,L1,V0,M1} { ! e3 ==> op( e2, e1 ) }.
% 12.43/12.80 parent0[0]: (198) {G1,W5,D3,L1,V0,M1} I;d(197) { op( e2, e2 ) ==> e3 }.
% 12.43/12.80 parent1[0; 2]: (Cputime limit exceeded (core dumped)
%------------------------------------------------------------------------------