%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : ALG036+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n020.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:13 EDT 2022
% Result : Theorem 0.71s 1.16s
% Output : Refutation 0.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ALG036+1 : TPTP v8.1.0. Released v2.7.0.
% 0.03/0.13 % Command : bliksem %s
% 0.12/0.34 % Computer : n020.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % DateTime : Thu Jun 9 04:22:36 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.71/1.13 *** allocated 10000 integers for termspace/termends
% 0.71/1.13 *** allocated 10000 integers for clauses
% 0.71/1.13 *** allocated 10000 integers for justifications
% 0.71/1.13 Bliksem 1.12
% 0.71/1.13
% 0.71/1.13
% 0.71/1.13 Automatic Strategy Selection
% 0.71/1.13
% 0.71/1.13
% 0.71/1.13 Clauses:
% 0.71/1.13
% 0.71/1.13 { op( e0, e0 ) = e0, op( e0, e0 ) = e1, op( e0, e0 ) = e2, op( e0, e0 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e0, e1 ) = e0, op( e0, e1 ) = e1, op( e0, e1 ) = e2, op( e0, e1 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e0, e2 ) = e0, op( e0, e2 ) = e1, op( e0, e2 ) = e2, op( e0, e2 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e0, e3 ) = e0, op( e0, e3 ) = e1, op( e0, e3 ) = e2, op( e0, e3 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e1, e0 ) = e0, op( e1, e0 ) = e1, op( e1, e0 ) = e2, op( e1, e0 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e1, e1 ) = e0, op( e1, e1 ) = e1, op( e1, e1 ) = e2, op( e1, e1 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e1, e2 ) = e0, op( e1, e2 ) = e1, op( e1, e2 ) = e2, op( e1, e2 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e1, e3 ) = e0, op( e1, e3 ) = e1, op( e1, e3 ) = e2, op( e1, e3 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e2, e0 ) = e0, op( e2, e0 ) = e1, op( e2, e0 ) = e2, op( e2, e0 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e2, e1 ) = e0, op( e2, e1 ) = e1, op( e2, e1 ) = e2, op( e2, e1 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e2, e2 ) = e0, op( e2, e2 ) = e1, op( e2, e2 ) = e2, op( e2, e2 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e2, e3 ) = e0, op( e2, e3 ) = e1, op( e2, e3 ) = e2, op( e2, e3 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e3, e0 ) = e0, op( e3, e0 ) = e1, op( e3, e0 ) = e2, op( e3, e0 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e3, e1 ) = e0, op( e3, e1 ) = e1, op( e3, e1 ) = e2, op( e3, e1 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e3, e2 ) = e0, op( e3, e2 ) = e1, op( e3, e2 ) = e2, op( e3, e2 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e3, e3 ) = e0, op( e3, e3 ) = e1, op( e3, e3 ) = e2, op( e3, e3 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( unit, e0 ) = e0 }.
% 0.71/1.13 { op( e0, unit ) = e0 }.
% 0.71/1.13 { op( unit, e1 ) = e1 }.
% 0.71/1.13 { op( e1, unit ) = e1 }.
% 0.71/1.13 { op( unit, e2 ) = e2 }.
% 0.71/1.13 { op( e2, unit ) = e2 }.
% 0.71/1.13 { op( unit, e3 ) = e3 }.
% 0.71/1.13 { op( e3, unit ) = e3 }.
% 0.71/1.13 { unit = e0, unit = e1, unit = e2, unit = e3 }.
% 0.71/1.13 { op( e0, e0 ) = e0, op( e0, e1 ) = e0, op( e0, e2 ) = e0, op( e0, e3 ) =
% 0.71/1.13 e0 }.
% 0.71/1.13 { op( e0, e0 ) = e0, op( e1, e0 ) = e0, op( e2, e0 ) = e0, op( e3, e0 ) =
% 0.71/1.13 e0 }.
% 0.71/1.13 { op( e0, e0 ) = e1, op( e0, e1 ) = e1, op( e0, e2 ) = e1, op( e0, e3 ) =
% 0.71/1.13 e1 }.
% 0.71/1.13 { op( e0, e0 ) = e1, op( e1, e0 ) = e1, op( e2, e0 ) = e1, op( e3, e0 ) =
% 0.71/1.13 e1 }.
% 0.71/1.13 { op( e0, e0 ) = e2, op( e0, e1 ) = e2, op( e0, e2 ) = e2, op( e0, e3 ) =
% 0.71/1.13 e2 }.
% 0.71/1.13 { op( e0, e0 ) = e2, op( e1, e0 ) = e2, op( e2, e0 ) = e2, op( e3, e0 ) =
% 0.71/1.13 e2 }.
% 0.71/1.13 { op( e0, e0 ) = e3, op( e0, e1 ) = e3, op( e0, e2 ) = e3, op( e0, e3 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e0, e0 ) = e3, op( e1, e0 ) = e3, op( e2, e0 ) = e3, op( e3, e0 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e1, e0 ) = e0, op( e1, e1 ) = e0, op( e1, e2 ) = e0, op( e1, e3 ) =
% 0.71/1.13 e0 }.
% 0.71/1.13 { op( e0, e1 ) = e0, op( e1, e1 ) = e0, op( e2, e1 ) = e0, op( e3, e1 ) =
% 0.71/1.13 e0 }.
% 0.71/1.13 { op( e1, e0 ) = e1, op( e1, e1 ) = e1, op( e1, e2 ) = e1, op( e1, e3 ) =
% 0.71/1.13 e1 }.
% 0.71/1.13 { op( e0, e1 ) = e1, op( e1, e1 ) = e1, op( e2, e1 ) = e1, op( e3, e1 ) =
% 0.71/1.13 e1 }.
% 0.71/1.13 { op( e1, e0 ) = e2, op( e1, e1 ) = e2, op( e1, e2 ) = e2, op( e1, e3 ) =
% 0.71/1.13 e2 }.
% 0.71/1.13 { op( e0, e1 ) = e2, op( e1, e1 ) = e2, op( e2, e1 ) = e2, op( e3, e1 ) =
% 0.71/1.13 e2 }.
% 0.71/1.13 { op( e1, e0 ) = e3, op( e1, e1 ) = e3, op( e1, e2 ) = e3, op( e1, e3 ) =
% 0.71/1.13 e3 }.
% 0.71/1.13 { op( e0, e1 ) = e3, op( e1, e1 ) = e3, op( e2, e1 ) = e3, op( e3, e1 ) =
% 0.71/1.14 e3 }.
% 0.71/1.14 { op( e2, e0 ) = e0, op( e2, e1 ) = e0, op( e2, e2 ) = e0, op( e2, e3 ) =
% 0.71/1.14 e0 }.
% 0.71/1.14 { op( e0, e2 ) = e0, op( e1, e2 ) = e0, op( e2, e2 ) = e0, op( e3, e2 ) =
% 0.71/1.14 e0 }.
% 0.71/1.14 { op( e2, e0 ) = e1, op( e2, e1 ) = e1, op( e2, e2 ) = e1, op( e2, e3 ) =
% 0.71/1.14 e1 }.
% 0.71/1.14 { op( e0, e2 ) = e1, op( e1, e2 ) = e1, op( e2, e2 ) = e1, op( e3, e2 ) =
% 0.71/1.14 e1 }.
% 0.71/1.14 { op( e2, e0 ) = e2, op( e2, e1 ) = e2, op( e2, e2 ) = e2, op( e2, e3 ) =
% 0.71/1.14 e2 }.
% 0.71/1.14 { op( e0, e2 ) = e2, op( e1, e2 ) = e2, op( e2, e2 ) = e2, op( e3, e2 ) =
% 0.71/1.14 e2 }.
% 0.71/1.14 { op( e2, e0 ) = e3, op( e2, e1 ) = e3, op( e2, e2 ) = e3, op( e2, e3 ) =
% 0.71/1.14 e3 }.
% 0.71/1.14 { op( e0, e2 ) = e3, op( e1, e2 ) = e3, op( e2, e2 ) = e3, op( e3, e2 ) =
% 0.71/1.14 e3 }.
% 0.71/1.14 { op( e3, e0 ) = e0, op( e3, e1 ) = e0, op( e3, e2 ) = e0, op( e3, e3 ) =
% 0.71/1.14 e0 }.
% 0.71/1.14 { op( e0, e3 ) = e0, op( e1, e3 ) = e0, op( e2, e3 ) = e0, op( e3, e3 ) =
% 0.71/1.14 e0 }.
% 0.71/1.14 { op( e3, e0 ) = e1, op( e3, e1 ) = e1, op( e3, e2 ) = e1, op( e3, e3 ) =
% 0.71/1.14 e1 }.
% 0.71/1.14 { op( e0, e3 ) = e1, op( e1, e3 ) = e1, op( e2, e3 ) = e1, op( e3, e3 ) =
% 0.71/1.14 e1 }.
% 0.71/1.16 { op( e3, e0 ) = e2, op( e3, e1 ) = e2, op( e3, e2 ) = e2, op( e3, e3 ) =
% 0.71/1.16 e2 }.
% 0.71/1.16 { op( e0, e3 ) = e2, op( e1, e3 ) = e2, op( e2, e3 ) = e2, op( e3, e3 ) =
% 0.71/1.16 e2 }.
% 0.71/1.16 { op( e3, e0 ) = e3, op( e3, e1 ) = e3, op( e3, e2 ) = e3, op( e3, e3 ) =
% 0.71/1.16 e3 }.
% 0.71/1.16 { op( e0, e3 ) = e3, op( e1, e3 ) = e3, op( e2, e3 ) = e3, op( e3, e3 ) =
% 0.71/1.16 e3 }.
% 0.71/1.16 { unit = e0 }.
% 0.71/1.16 { ! op( e0, e0 ) = op( e1, e0 ) }.
% 0.71/1.16 { ! op( e0, e0 ) = op( e2, e0 ) }.
% 0.71/1.16 { ! op( e0, e0 ) = op( e3, e0 ) }.
% 0.71/1.16 { ! op( e1, e0 ) = op( e2, e0 ) }.
% 0.71/1.16 { ! op( e1, e0 ) = op( e3, e0 ) }.
% 0.71/1.16 { ! op( e2, e0 ) = op( e3, e0 ) }.
% 0.71/1.16 { ! op( e0, e1 ) = op( e1, e1 ) }.
% 0.71/1.16 { ! op( e0, e1 ) = op( e2, e1 ) }.
% 0.71/1.16 { ! op( e0, e1 ) = op( e3, e1 ) }.
% 0.71/1.16 { ! op( e1, e1 ) = op( e2, e1 ) }.
% 0.71/1.16 { ! op( e1, e1 ) = op( e3, e1 ) }.
% 0.71/1.16 { ! op( e2, e1 ) = op( e3, e1 ) }.
% 0.71/1.16 { ! op( e0, e2 ) = op( e1, e2 ) }.
% 0.71/1.16 { ! op( e0, e2 ) = op( e2, e2 ) }.
% 0.71/1.16 { ! op( e0, e2 ) = op( e3, e2 ) }.
% 0.71/1.16 { ! op( e1, e2 ) = op( e2, e2 ) }.
% 0.71/1.16 { ! op( e1, e2 ) = op( e3, e2 ) }.
% 0.71/1.16 { ! op( e2, e2 ) = op( e3, e2 ) }.
% 0.71/1.16 { ! op( e0, e3 ) = op( e1, e3 ) }.
% 0.71/1.16 { ! op( e0, e3 ) = op( e2, e3 ) }.
% 0.71/1.16 { ! op( e0, e3 ) = op( e3, e3 ) }.
% 0.71/1.16 { ! op( e1, e3 ) = op( e2, e3 ) }.
% 0.71/1.16 { ! op( e1, e3 ) = op( e3, e3 ) }.
% 0.71/1.16 { ! op( e2, e3 ) = op( e3, e3 ) }.
% 0.71/1.16 { ! op( e0, e0 ) = op( e0, e1 ) }.
% 0.71/1.16 { ! op( e0, e0 ) = op( e0, e2 ) }.
% 0.71/1.16 { ! op( e0, e0 ) = op( e0, e3 ) }.
% 0.71/1.16 { ! op( e0, e1 ) = op( e0, e2 ) }.
% 0.71/1.16 { ! op( e0, e1 ) = op( e0, e3 ) }.
% 0.71/1.16 { ! op( e0, e2 ) = op( e0, e3 ) }.
% 0.71/1.16 { ! op( e1, e0 ) = op( e1, e1 ) }.
% 0.71/1.16 { ! op( e1, e0 ) = op( e1, e2 ) }.
% 0.71/1.16 { ! op( e1, e0 ) = op( e1, e3 ) }.
% 0.71/1.16 { ! op( e1, e1 ) = op( e1, e2 ) }.
% 0.71/1.16 { ! op( e1, e1 ) = op( e1, e3 ) }.
% 0.71/1.16 { ! op( e1, e2 ) = op( e1, e3 ) }.
% 0.71/1.16 { ! op( e2, e0 ) = op( e2, e1 ) }.
% 0.71/1.16 { ! op( e2, e0 ) = op( e2, e2 ) }.
% 0.71/1.16 { ! op( e2, e0 ) = op( e2, e3 ) }.
% 0.71/1.16 { ! op( e2, e1 ) = op( e2, e2 ) }.
% 0.71/1.16 { ! op( e2, e1 ) = op( e2, e3 ) }.
% 0.71/1.16 { ! op( e2, e2 ) = op( e2, e3 ) }.
% 0.71/1.16 { ! op( e3, e0 ) = op( e3, e1 ) }.
% 0.71/1.16 { ! op( e3, e0 ) = op( e3, e2 ) }.
% 0.71/1.16 { ! op( e3, e0 ) = op( e3, e3 ) }.
% 0.71/1.16 { ! op( e3, e1 ) = op( e3, e2 ) }.
% 0.71/1.16 { ! op( e3, e1 ) = op( e3, e3 ) }.
% 0.71/1.16 { ! op( e3, e2 ) = op( e3, e3 ) }.
% 0.71/1.16 { ! e0 = e1 }.
% 0.71/1.16 { ! e0 = e2 }.
% 0.71/1.16 { ! e0 = e3 }.
% 0.71/1.16 { ! e1 = e2 }.
% 0.71/1.16 { ! e1 = e3 }.
% 0.71/1.16 { ! e2 = e3 }.
% 0.71/1.16 { ! op( e0, e0 ) = e0, ! op( e1, e1 ) = e0, ! op( e2, e2 ) = e0, ! op( e3,
% 0.71/1.16 e3 ) = e0 }.
% 0.71/1.16 { ! op( e0, e0 ) = e1, ! op( e1, e1 ) = e1, ! op( e2, e2 ) = e1, ! op( e3,
% 0.71/1.16 e3 ) = e1 }.
% 0.71/1.16 { ! op( e0, e0 ) = e2, ! op( e1, e1 ) = e2, ! op( e2, e2 ) = e2, ! op( e3,
% 0.71/1.16 e3 ) = e2 }.
% 0.71/1.16 { ! op( e0, e0 ) = e3, ! op( e1, e1 ) = e3, ! op( e2, e2 ) = e3, ! op( e3,
% 0.71/1.16 e3 ) = e3 }.
% 0.71/1.16 { alpha1, alpha2 }.
% 0.71/1.16 { alpha1, op( e3, e3 ) = e3 }.
% 0.71/1.16 { ! alpha2, op( e0, e0 ) = e3 }.
% 0.71/1.16 { ! alpha2, op( e1, e1 ) = e3 }.
% 0.71/1.16 { ! alpha2, op( e2, e2 ) = e3 }.
% 0.71/1.16 { ! op( e0, e0 ) = e3, ! op( e1, e1 ) = e3, ! op( e2, e2 ) = e3, alpha2 }.
% 0.71/1.16 { ! alpha1, alpha3, alpha4 }.
% 0.71/1.16 { ! alpha3, alpha1 }.
% 0.71/1.16 { ! alpha4, alpha1 }.
% 0.71/1.16 { ! alpha4, alpha6 }.
% 0.71/1.16 { ! alpha4, op( e3, e3 ) = e2 }.
% 0.71/1.16 { ! alpha6, ! op( e3, e3 ) = e2, alpha4 }.
% 0.71/1.16 { ! alpha6, op( e0, e0 ) = e2 }.
% 0.71/1.16 { ! alpha6, op( e1, e1 ) = e2 }.
% 0.71/1.16 { ! alpha6, op( e2, e2 ) = e2 }.
% 0.71/1.16 { ! op( e0, e0 ) = e2, ! op( e1, e1 ) = e2, ! op( e2, e2 ) = e2, alpha6 }.
% 0.71/1.16 { ! alpha3, alpha5, alpha7 }.
% 0.71/1.16 { ! alpha5, alpha3 }.
% 0.71/1.16 { ! alpha7, alpha3 }.
% 0.71/1.16 { ! alpha7, alpha9 }.
% 0.71/1.16 { ! alpha7, op( e3, e3 ) = e1 }.
% 0.71/1.16 { ! alpha9, ! op( e3, e3 ) = e1, alpha7 }.
% 0.71/1.16 { ! alpha9, op( e0, e0 ) = e1 }.
% 0.71/1.16 { ! alpha9, op( e1, e1 ) = e1 }.
% 0.71/1.16 { ! alpha9, op( e2, e2 ) = e1 }.
% 0.71/1.16 { ! op( e0, e0 ) = e1, ! op( e1, e1 ) = e1, ! op( e2, e2 ) = e1, alpha9 }.
% 0.71/1.16 { ! alpha5, alpha8 }.
% 0.71/1.16 { ! alpha5, op( e3, e3 ) = e0 }.
% 0.71/1.16 { ! alpha8, ! op( e3, e3 ) = e0, alpha5 }.
% 0.71/1.16 { ! alpha8, op( e0, e0 ) = e0 }.
% 0.71/1.16 { ! alpha8, op( e1, e1 ) = e0 }.
% 0.71/1.16 { ! alpha8, op( e2, e2 ) = e0 }.
% 0.71/1.16 { ! op( e0, e0 ) = e0, ! op( e1, e1 ) = e0, ! op( e2, e2 ) = e0, alpha8 }.
% 0.71/1.16
% 0.71/1.16 percentage equality = 0.864407, percentage horn = 0.644295
% 0.71/1.16 This is a pure equality problem
% 0.71/1.16
% 0.71/1.16
% 0.71/1.16
% 0.71/1.16 Options Used:
% 0.71/1.16
% 0.71/1.16 useres = 1
% 0.71/1.16 useparamod = 1
% 0.71/1.16 useeqrefl = 1
% 0.71/1.16 useeqfact = 1
% 0.71/1.16 usefactor = 1
% 0.71/1.16 usesimpsplitting = 0
% 0.71/1.16 usesimpdemod = 5
% 0.71/1.16 usesimpres = 3
% 0.71/1.16
% 0.71/1.16 resimpinuse = 1000
% 0.71/1.16 resimpclauses = 20000
% 0.71/1.16 substype = eqrewr
% 0.71/1.16 backwardsubs = 1
% 0.71/1.16 selectoldest = 5
% 0.71/1.16
% 0.71/1.16 litorderings [0] = split
% 0.71/1.16 litorderings [1] = extend the termordering, first sorting on arguments
% 0.71/1.16
% 0.71/1.16 termordering = kbo
% 0.71/1.16
% 0.71/1.16 litapriori = 0
% 0.71/1.16 termapriori = 1
% 0.71/1.16 litaposteriori = 0
% 0.71/1.16 termaposteriori = 0
% 0.71/1.16 demodaposteriori = 0
% 0.71/1.16 ordereqreflfact = 0
% 0.71/1.16
% 0.71/1.16 litselect = negord
% 0.71/1.16
% 0.71/1.16 maxweight = 15
% 0.71/1.16 maxdepth = 30000
% 0.71/1.16 maxlength = 115
% 0.71/1.16 maxnrvars = 195
% 0.71/1.16 excuselevel = 1
% 0.71/1.16 increasemaxweight = 1
% 0.71/1.16
% 0.71/1.16 maxselected = 10000000
% 0.71/1.16 maxnrclauses = 10000000
% 0.71/1.16
% 0.71/1.16 showgenerated = 0
% 0.71/1.16 showkept = 0
% 0.71/1.16 showselected = 0
% 0.71/1.16 showdeleted = 0
% 0.71/1.16 showresimp = 1
% 0.71/1.16 showstatus = 2000
% 0.71/1.16
% 0.71/1.16 prologoutput = 0
% 0.71/1.16 nrgoals = 5000000
% 0.71/1.16 totalproof = 1
% 0.71/1.16
% 0.71/1.16 Symbols occurring in the translation:
% 0.71/1.16
% 0.71/1.16 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.71/1.16 . [1, 2] (w:1, o:25, a:1, s:1, b:0),
% 0.71/1.16 ! [4, 1] (w:0, o:20, a:1, s:1, b:0),
% 0.71/1.16 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.71/1.16 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.71/1.16 e0 [35, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.71/1.16 op [36, 2] (w:1, o:49, a:1, s:1, b:0),
% 0.71/1.16 e1 [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.71/1.16 e2 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.71/1.16 e3 [39, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.71/1.16 unit [40, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.71/1.16 alpha1 [41, 0] (w:1, o:11, a:1, s:1, b:1),
% 0.71/1.16 alpha2 [42, 0] (w:1, o:12, a:1, s:1, b:1),
% 0.71/1.16 alpha3 [43, 0] (w:1, o:13, a:1, s:1, b:1),
% 0.71/1.16 alpha4 [44, 0] (w:1, o:14, a:1, s:1, b:1),
% 0.71/1.16 alpha5 [45, 0] (w:1, o:15, a:1, s:1, b:1),
% 0.71/1.16 alpha6 [46, 0] (w:1, o:16, a:1, s:1, b:1),
% 0.71/1.16 alpha7 [47, 0] (w:1, o:17, a:1, s:1, b:1),
% 0.71/1.16 alpha8 [48, 0] (w:1, o:18, a:1, s:1, b:1),
% 0.71/1.16 alpha9 [49, 0] (w:1, o:19, a:1, s:1, b:1).
% 0.71/1.16
% 0.71/1.16
% 0.71/1.16 Starting Search:
% 0.71/1.16
% 0.71/1.16 *** allocated 15000 integers for clauses
% 0.71/1.16 *** allocated 22500 integers for clauses
% 0.71/1.16
% 0.71/1.16 Bliksems!, er is een bewijs:
% 0.71/1.16 % SZS status Theorem
% 0.71/1.16 % SZS output start Refutation
% 0.71/1.16
% 0.71/1.16 (17) {G0,W5,D3,L1,V0,M1} I { op( e0, unit ) ==> e0 }.
% 0.71/1.16 (57) {G0,W3,D2,L1,V0,M1} I { unit ==> e0 }.
% 0.71/1.16 (106) {G0,W3,D2,L1,V0,M1} I { ! e1 ==> e0 }.
% 0.71/1.16 (107) {G0,W3,D2,L1,V0,M1} I { ! e2 ==> e0 }.
% 0.71/1.16 (108) {G0,W3,D2,L1,V0,M1} I { ! e3 ==> e0 }.
% 0.71/1.16 (112) {G0,W20,D3,L4,V0,M4} I { ! op( e0, e0 ) ==> e0, ! op( e1, e1 ) ==> e0
% 0.71/1.16 , ! op( e2, e2 ) ==> e0, ! op( e3, e3 ) ==> e0 }.
% 0.71/1.16 (116) {G0,W2,D1,L2,V0,M2} I { alpha1, alpha2 }.
% 0.71/1.16 (118) {G0,W6,D3,L2,V0,M2} I { ! alpha2, op( e0, e0 ) ==> e3 }.
% 0.71/1.16 (122) {G0,W3,D1,L3,V0,M3} I { ! alpha1, alpha3, alpha4 }.
% 0.71/1.16 (125) {G0,W2,D1,L2,V0,M2} I { ! alpha4, alpha6 }.
% 0.71/1.16 (128) {G0,W6,D3,L2,V0,M2} I { ! alpha6, op( e0, e0 ) ==> e2 }.
% 0.71/1.16 (132) {G0,W3,D1,L3,V0,M3} I { ! alpha3, alpha5, alpha7 }.
% 0.71/1.16 (135) {G0,W2,D1,L2,V0,M2} I { ! alpha7, alpha9 }.
% 0.71/1.16 (138) {G0,W6,D3,L2,V0,M2} I { ! alpha9, op( e0, e0 ) ==> e1 }.
% 0.71/1.16 (142) {G0,W2,D1,L2,V0,M2} I { ! alpha5, alpha8 }.
% 0.71/1.16 (143) {G0,W6,D3,L2,V0,M2} I { ! alpha5, op( e3, e3 ) ==> e0 }.
% 0.71/1.16 (146) {G0,W6,D3,L2,V0,M2} I { ! alpha8, op( e1, e1 ) ==> e0 }.
% 0.71/1.16 (147) {G0,W6,D3,L2,V0,M2} I { ! alpha8, op( e2, e2 ) ==> e0 }.
% 0.71/1.16 (151) {G1,W3,D1,L3,V0,M3} R(132,135) { ! alpha3, alpha5, alpha9 }.
% 0.71/1.16 (153) {G2,W3,D1,L3,V0,M3} R(151,142) { ! alpha3, alpha9, alpha8 }.
% 0.71/1.16 (158) {G1,W3,D1,L3,V0,M3} R(122,116) { alpha3, alpha4, alpha2 }.
% 0.71/1.16 (164) {G2,W3,D1,L3,V0,M3} R(158,125) { alpha3, alpha2, alpha6 }.
% 0.71/1.16 (166) {G3,W4,D1,L4,V0,M4} R(164,153) { alpha2, alpha6, alpha9, alpha8 }.
% 0.71/1.16 (167) {G3,W4,D1,L4,V0,M4} R(164,151) { alpha2, alpha6, alpha5, alpha9 }.
% 0.71/1.16 (179) {G1,W5,D3,L1,V0,M1} S(17);d(57) { op( e0, e0 ) ==> e0 }.
% 0.71/1.16 (253) {G2,W4,D2,L2,V0,M2} S(138);d(179) { ! alpha9, e1 ==> e0 }.
% 0.71/1.16 (254) {G3,W1,D1,L1,V0,M1} S(253);r(106) { ! alpha9 }.
% 0.71/1.16 (259) {G4,W3,D1,L3,V0,M3} R(254,167) { alpha2, alpha6, alpha5 }.
% 0.71/1.16 (260) {G4,W3,D1,L3,V0,M3} R(254,166) { alpha2, alpha6, alpha8 }.
% 0.71/1.16 (313) {G2,W4,D2,L2,V0,M2} S(128);d(179) { ! alpha6, e2 ==> e0 }.
% 0.71/1.16 (314) {G3,W1,D1,L1,V0,M1} S(313);r(107) { ! alpha6 }.
% 0.71/1.16 (317) {G5,W2,D1,L2,V0,M2} R(314,260) { alpha2, alpha8 }.
% 0.71/1.16 (318) {G5,W2,D1,L2,V0,M2} R(314,259) { alpha2, alpha5 }.
% 0.71/1.16 (325) {G6,W6,D3,L2,V0,M2} R(317,146) { alpha2, op( e1, e1 ) ==> e0 }.
% 0.71/1.16 (326) {G6,W6,D3,L2,V0,M2} R(317,147) { alpha2, op( e2, e2 ) ==> e0 }.
% 0.71/1.16 (327) {G6,W6,D3,L2,V0,M2} R(318,143) { alpha2, op( e3, e3 ) ==> e0 }.
% 0.71/1.16 (356) {G2,W4,D2,L2,V0,M2} S(118);d(179) { ! alpha2, e3 ==> e0 }.
% 0.71/1.16 (357) {G3,W1,D1,L1,V0,M1} S(356);r(108) { ! alpha2 }.
% 0.71/1.16 (358) {G7,W5,D3,L1,V0,M1} R(357,326) { op( e2, e2 ) ==> e0 }.
% 0.71/1.16 (359) {G7,W5,D3,L1,V0,M1} R(357,325) { op( e1, e1 ) ==> e0 }.
% 0.71/1.16 (360) {G7,W5,D3,L1,V0,M1} R(357,327) { op( e3, e3 ) ==> e0 }.
% 0.71/1.16 (418) {G8,W0,D0,L0,V0,M0} S(112);d(179);q;d(359);d(358);d(360);q;q;q { }.
% 0.71/1.16
% 0.71/1.16
% 0.71/1.16 % SZS output end Refutation
% 0.71/1.16 found a proof!
% 0.71/1.16
% 0.71/1.16 *** allocated 33750 integers for clauses
% 0.71/1.16
% 0.71/1.16 Unprocessed initial clauses:
% 0.71/1.16
% 0.71/1.16 (420) {G0,W20,D3,L4,V0,M4} { op( e0, e0 ) = e0, op( e0, e0 ) = e1, op( e0
% 0.71/1.16 , e0 ) = e2, op( e0, e0 ) = e3 }.
% 0.71/1.16 (421) {G0,W20,D3,L4,V0,M4} { op( e0, e1 ) = e0, op( e0, e1 ) = e1, op( e0
% 0.71/1.16 , e1 ) = e2, op( e0, e1 ) = e3 }.
% 0.71/1.16 (422) {G0,W20,D3,L4,V0,M4} { op( e0, e2 ) = e0, op( e0, e2 ) = e1, op( e0
% 0.71/1.16 , e2 ) = e2, op( e0, e2 ) = e3 }.
% 0.71/1.16 (423) {G0,W20,D3,L4,V0,M4} { op( e0, e3 ) = e0, op( e0, e3 ) = e1, op( e0
% 0.71/1.16 , e3 ) = e2, op( e0, e3 ) = e3 }.
% 0.71/1.16 (424) {G0,W20,D3,L4,V0,M4} { op( e1, e0 ) = e0, op( e1, e0 ) = e1, op( e1
% 0.71/1.16 , e0 ) = e2, op( e1, e0 ) = e3 }.
% 0.71/1.16 (425) {G0,W20,D3,L4,V0,M4} { op( e1, e1 ) = e0, op( e1, e1 ) = e1, op( e1
% 0.71/1.16 , e1 ) = e2, op( e1, e1 ) = e3 }.
% 0.71/1.16 (426) {G0,W20,D3,L4,V0,M4} { op( e1, e2 ) = e0, op( e1, e2 ) = e1, op( e1
% 0.71/1.16 , e2 ) = e2, op( e1, e2 ) = e3 }.
% 0.71/1.16 (427) {G0,W20,D3,L4,V0,M4} { op( e1, e3 ) = e0, op( e1, e3 ) = e1, op( e1
% 0.71/1.16 , e3 ) = e2, op( e1, e3 ) = e3 }.
% 0.71/1.16 (428) {G0,W20,D3,L4,V0,M4} { op( e2, e0 ) = e0, op( e2, e0 ) = e1, op( e2
% 0.71/1.16 , e0 ) = e2, op( e2, e0 ) = e3 }.
% 0.71/1.16 (429) {G0,W20,D3,L4,V0,M4} { op( e2, e1 ) = e0, op( e2, e1 ) = e1, op( e2
% 0.71/1.16 , e1 ) = e2, op( e2, e1 ) = e3 }.
% 0.71/1.16 (430) {G0,W20,D3,L4,V0,M4} { op( e2, e2 ) = e0, op( e2, e2 ) = e1, op( e2
% 0.71/1.16 , e2 ) = e2, op( e2, e2 ) = e3 }.
% 0.71/1.16 (431) {G0,W20,D3,L4,V0,M4} { op( e2, e3 ) = e0, op( e2, e3 ) = e1, op( e2
% 0.71/1.16 , e3 ) = e2, op( e2, e3 ) = e3 }.
% 0.71/1.16 (432) {G0,W20,D3,L4,V0,M4} { op( e3, e0 ) = e0, op( e3, e0 ) = e1, op( e3
% 0.71/1.16 , e0 ) = e2, op( e3, e0 ) = e3 }.
% 0.71/1.16 (433) {G0,W20,D3,L4,V0,M4} { op( e3, e1 ) = e0, op( e3, e1 ) = e1, op( e3
% 0.71/1.16 , e1 ) = e2, op( e3, e1 ) = e3 }.
% 0.71/1.16 (434) {G0,W20,D3,L4,V0,M4} { op( e3, e2 ) = e0, op( e3, e2 ) = e1, op( e3
% 0.71/1.16 , e2 ) = e2, op( e3, e2 ) = e3 }.
% 0.71/1.16 (435) {G0,W20,D3,L4,V0,M4} { op( e3, e3 ) = e0, op( e3, e3 ) = e1, op( e3
% 0.71/1.16 , e3 ) = e2, op( e3, e3 ) = e3 }.
% 0.71/1.16 (436) {G0,W5,D3,L1,V0,M1} { op( unit, e0 ) = e0 }.
% 0.71/1.16 (437) {G0,W5,D3,L1,V0,M1} { op( e0, unit ) = e0 }.
% 0.71/1.16 (438) {G0,W5,D3,L1,V0,M1} { op( unit, e1 ) = e1 }.
% 0.71/1.16 (439) {G0,W5,D3,L1,V0,M1} { op( e1, unit ) = e1 }.
% 0.71/1.16 (440) {G0,W5,D3,L1,V0,M1} { op( unit, e2 ) = e2 }.
% 0.71/1.16 (441) {G0,W5,D3,L1,V0,M1} { op( e2, unit ) = e2 }.
% 0.71/1.16 (442) {G0,W5,D3,L1,V0,M1} { op( unit, e3 ) = e3 }.
% 0.71/1.16 (443) {G0,W5,D3,L1,V0,M1} { op( e3, unit ) = e3 }.
% 0.71/1.16 (444) {G0,W12,D2,L4,V0,M4} { unit = e0, unit = e1, unit = e2, unit = e3
% 0.71/1.16 }.
% 0.71/1.16 (445) {G0,W20,D3,L4,V0,M4} { op( e0, e0 ) = e0, op( e0, e1 ) = e0, op( e0
% 0.71/1.16 , e2 ) = e0, op( e0, e3 ) = e0 }.
% 0.71/1.16 (446) {G0,W20,D3,L4,V0,M4} { op( e0, e0 ) = e0, op( e1, e0 ) = e0, op( e2
% 0.71/1.16 , e0 ) = e0, op( e3, e0 ) = e0 }.
% 0.71/1.16 (447) {G0,W20,D3,L4,V0,M4} { op( e0, e0 ) = e1, op( e0, e1 ) = e1, op( e0
% 0.71/1.16 , e2 ) = e1, op( e0, e3 ) = e1 }.
% 0.71/1.16 (448) {G0,W20,D3,L4,V0,M4} { op( e0, e0 ) = e1, op( e1, e0 ) = e1, op( e2
% 0.71/1.16 , e0 ) = e1, op( e3, e0 ) = e1 }.
% 0.71/1.16 (449) {G0,W20,D3,L4,V0,M4} { op( e0, e0 ) = e2, op( e0, e1 ) = e2, op( e0
% 0.71/1.16 , e2 ) = e2, op( e0, e3 ) = e2 }.
% 0.71/1.16 (450) {G0,W20,D3,L4,V0,M4} { op( e0, e0 ) = e2, op( e1, e0 ) = e2, op( e2
% 0.71/1.16 , e0 ) = e2, op( e3, e0 ) = e2 }.
% 0.71/1.16 (451) {G0,W20,D3,L4,V0,M4} { op( e0, e0 ) = e3, op( e0, e1 ) = e3, op( e0
% 0.71/1.16 , e2 ) = e3, op( e0, e3 ) = e3 }.
% 0.71/1.16 (452) {G0,W20,D3,L4,V0,M4} { op( e0, e0 ) = e3, op( e1, e0 ) = e3, op( e2
% 0.71/1.16 , e0 ) = e3, op( e3, e0 ) = e3 }.
% 0.71/1.16 (453) {G0,W20,D3,L4,V0,M4} { op( e1, e0 ) = e0, op( e1, e1 ) = e0, op( e1
% 0.71/1.16 , e2 ) = e0, op( e1, e3 ) = e0 }.
% 0.71/1.16 (454) {G0,W20,D3,L4,V0,M4} { op( e0, e1 ) = e0, op( e1, e1 ) = e0, op( e2
% 0.71/1.16 , e1 ) = e0, op( e3, e1 ) = e0 }.
% 0.71/1.16 (455) {G0,W20,D3,L4,V0,M4} { op( e1, e0 ) = e1, op( e1, e1 ) = e1, op( e1
% 0.71/1.16 , e2 ) = e1, op( e1, e3 ) = e1 }.
% 0.71/1.16 (456) {G0,W20,D3,L4,V0,M4} { op( e0, e1 ) = e1, op( e1, e1 ) = e1, op( e2
% 0.71/1.16 , e1 ) = e1, op( e3, e1 ) = e1 }.
% 0.71/1.16 (457) {G0,W20,D3,L4,V0,M4} { op( e1, e0 ) = e2, op( e1, e1 ) = e2, op( e1
% 0.71/1.16 , e2 ) = e2, op( e1, e3 ) = e2 }.
% 0.71/1.16 (458) {G0,W20,D3,L4,V0,M4} { op( e0, e1 ) = e2, op( e1, e1 ) = e2, op( e2
% 0.71/1.16 , e1 ) = e2, op( e3, e1 ) = e2 }.
% 0.71/1.16 (459) {G0,W20,D3,L4,V0,M4} { op( e1, e0 ) = e3, op( e1, e1 ) = e3, op( e1
% 0.71/1.16 , e2 ) = e3, op( e1, e3 ) = e3 }.
% 0.71/1.16 (460) {G0,W20,D3,L4,V0,M4} { op( e0, e1 ) = e3, op( e1, e1 ) = e3, op( e2
% 0.71/1.16 , e1 ) = e3, op( e3, e1 ) = e3 }.
% 0.71/1.16 (461) {G0,W20,D3,L4,V0,M4} { op( e2, e0 ) = e0, op( e2, e1 ) = e0, op( e2
% 0.71/1.16 , e2 ) = e0, op( e2, e3 ) = e0 }.
% 0.71/1.16 (462) {G0,W20,D3,L4,V0,M4} { op( e0, e2 ) = e0, op( e1, e2 ) = e0, op( e2
% 0.71/1.16 , e2 ) = e0, op( e3, e2 ) = e0 }.
% 0.71/1.16 (463) {G0,W20,D3,L4,V0,M4} { op( e2, e0 ) = e1, op( e2, e1 ) = e1, op( e2
% 0.71/1.16 , e2 ) = e1, op( e2, e3 ) = e1 }.
% 0.71/1.16 (464) {G0,W20,D3,L4,V0,M4} { op( e0, e2 ) = e1, op( e1, e2 ) = e1, op( e2
% 0.71/1.16 , e2 ) = e1, op( e3, e2 ) = e1 }.
% 0.71/1.16 (465) {G0,W20,D3,L4,V0,M4} { op( e2, e0 ) = e2, op( e2, e1 ) = e2, op( e2
% 0.71/1.16 , e2 ) = e2, op( e2, e3 ) = e2 }.
% 0.71/1.16 (466) {G0,W20,D3,L4,V0,M4} { op( e0, e2 ) = e2, op( e1, e2 ) = e2, op( e2
% 0.71/1.16 , e2 ) = e2, op( e3, e2 ) = e2 }.
% 0.71/1.16 (467) {G0,W20,D3,L4,V0,M4} { op( e2, e0 ) = e3, op( e2, e1 ) = e3, op( e2
% 0.71/1.16 , e2 ) = e3, op( e2, e3 ) = e3 }.
% 0.71/1.16 (468) {G0,W20,D3,L4,V0,M4} { op( e0, e2 ) = e3, op( e1, e2 ) = e3, op( e2
% 0.71/1.16 , e2 ) = e3, op( e3, e2 ) = e3 }.
% 0.71/1.16 (469) {G0,W20,D3,L4,V0,M4} { op( e3, e0 ) = e0, op( e3, e1 ) = e0, op( e3
% 0.71/1.16 , e2 ) = e0, op( e3, e3 ) = e0 }.
% 0.71/1.16 (470) {G0,W20,D3,L4,V0,M4} { op( e0, e3 ) = e0, op( e1, e3 ) = e0, op( e2
% 0.71/1.16 , e3 ) = e0, op( e3, e3 ) = e0 }.
% 0.71/1.16 (471) {G0,W20,D3,L4,V0,M4} { op( e3, e0 ) = e1, op( e3, e1 ) = e1, op( e3
% 0.71/1.16 , e2 ) = e1, op( e3, e3 ) = e1 }.
% 0.71/1.16 (472) {G0,W20,D3,L4,V0,M4} { op( e0, e3 ) = e1, op( e1, e3 ) = e1, op( e2
% 0.71/1.16 , e3 ) = e1, op( e3, e3 ) = e1 }.
% 0.71/1.16 (473) {G0,W20,D3,L4,V0,M4} { op( e3, e0 ) = e2, op( e3, e1 ) = e2, op( e3
% 0.71/1.16 , e2 ) = e2, op( e3, e3 ) = e2 }.
% 0.71/1.16 (474) {G0,W20,D3,L4,V0,M4} { op( e0, e3 ) = e2, op( e1, e3 ) = e2, op( e2
% 0.71/1.16 , e3 ) = e2, op( e3, e3 ) = e2 }.
% 0.71/1.16 (475) {G0,W20,D3,L4,V0,M4} { op( e3, e0 ) = e3, op( e3, e1 ) = e3, op( e3
% 0.71/1.16 , e2 ) = e3, op( e3, e3 ) = e3 }.
% 0.71/1.16 (476) {G0,W20,D3,L4,V0,M4} { op( e0, e3 ) = e3, op( e1, e3 ) = e3, op( e2
% 0.71/1.16 , e3 ) = e3, op( e3, e3 ) = e3 }.
% 0.71/1.16 (477) {G0,W3,D2,L1,V0,M1} { unit = e0 }.
% 0.71/1.16 (478) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e1, e0 ) }.
% 0.71/1.16 (479) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e2, e0 ) }.
% 0.71/1.16 (480) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e3, e0 ) }.
% 0.71/1.16 (481) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e2, e0 ) }.
% 0.71/1.16 (482) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e3, e0 ) }.
% 0.71/1.16 (483) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e3, e0 ) }.
% 0.71/1.16 (484) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e1, e1 ) }.
% 0.71/1.16 (485) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e2, e1 ) }.
% 0.71/1.16 (486) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e3, e1 ) }.
% 0.71/1.16 (487) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e2, e1 ) }.
% 0.71/1.16 (488) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e3, e1 ) }.
% 0.71/1.16 (489) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e3, e1 ) }.
% 0.71/1.16 (490) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e1, e2 ) }.
% 0.71/1.16 (491) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e2, e2 ) }.
% 0.71/1.16 (492) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e3, e2 ) }.
% 0.71/1.16 (493) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e2, e2 ) }.
% 0.71/1.16 (494) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e3, e2 ) }.
% 0.71/1.16 (495) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e3, e2 ) }.
% 0.71/1.16 (496) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e1, e3 ) }.
% 0.71/1.16 (497) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e2, e3 ) }.
% 0.71/1.16 (498) {G0,W7,D3,L1,V0,M1} { ! op( e0, e3 ) = op( e3, e3 ) }.
% 0.71/1.16 (499) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e2, e3 ) }.
% 0.71/1.16 (500) {G0,W7,D3,L1,V0,M1} { ! op( e1, e3 ) = op( e3, e3 ) }.
% 0.71/1.16 (501) {G0,W7,D3,L1,V0,M1} { ! op( e2, e3 ) = op( e3, e3 ) }.
% 0.71/1.16 (502) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e1 ) }.
% 0.71/1.16 (503) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e2 ) }.
% 0.71/1.16 (504) {G0,W7,D3,L1,V0,M1} { ! op( e0, e0 ) = op( e0, e3 ) }.
% 0.71/1.16 (505) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e0, e2 ) }.
% 0.71/1.16 (506) {G0,W7,D3,L1,V0,M1} { ! op( e0, e1 ) = op( e0, e3 ) }.
% 0.71/1.16 (507) {G0,W7,D3,L1,V0,M1} { ! op( e0, e2 ) = op( e0, e3 ) }.
% 0.71/1.16 (508) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e1 ) }.
% 0.76/1.16 (509) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e2 ) }.
% 0.76/1.16 (510) {G0,W7,D3,L1,V0,M1} { ! op( e1, e0 ) = op( e1, e3 ) }.
% 0.76/1.16 (511) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e1, e2 ) }.
% 0.76/1.16 (512) {G0,W7,D3,L1,V0,M1} { ! op( e1, e1 ) = op( e1, e3 ) }.
% 0.76/1.16 (513) {G0,W7,D3,L1,V0,M1} { ! op( e1, e2 ) = op( e1, e3 ) }.
% 0.76/1.16 (514) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e1 ) }.
% 0.76/1.16 (515) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e2 ) }.
% 0.76/1.16 (516) {G0,W7,D3,L1,V0,M1} { ! op( e2, e0 ) = op( e2, e3 ) }.
% 0.76/1.16 (517) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e2 ) }.
% 0.76/1.16 (518) {G0,W7,D3,L1,V0,M1} { ! op( e2, e1 ) = op( e2, e3 ) }.
% 0.76/1.16 (519) {G0,W7,D3,L1,V0,M1} { ! op( e2, e2 ) = op( e2, e3 ) }.
% 0.76/1.16 (520) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e1 ) }.
% 0.76/1.16 (521) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e2 ) }.
% 0.76/1.16 (522) {G0,W7,D3,L1,V0,M1} { ! op( e3, e0 ) = op( e3, e3 ) }.
% 0.76/1.16 (523) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e3, e2 ) }.
% 0.76/1.16 (524) {G0,W7,D3,L1,V0,M1} { ! op( e3, e1 ) = op( e3, e3 ) }.
% 0.76/1.16 (525) {G0,W7,D3,L1,V0,M1} { ! op( e3, e2 ) = op( e3, e3 ) }.
% 0.76/1.16 (526) {G0,W3,D2,L1,V0,M1} { ! e0 = e1 }.
% 0.76/1.16 (527) {G0,W3,D2,L1,V0,M1} { ! e0 = e2 }.
% 0.76/1.16 (528) {G0,W3,D2,L1,V0,M1} { ! e0 = e3 }.
% 0.76/1.16 (529) {G0,W3,D2,L1,V0,M1} { ! e1 = e2 }.
% 0.76/1.16 (530) {G0,W3,D2,L1,V0,M1} { ! e1 = e3 }.
% 0.76/1.16 (531) {G0,W3,D2,L1,V0,M1} { ! e2 = e3 }.
% 0.76/1.16 (532) {G0,W20,D3,L4,V0,M4} { ! op( e0, e0 ) = e0, ! op( e1, e1 ) = e0, !
% 0.76/1.16 op( e2, e2 ) = e0, ! op( e3, e3 ) = e0 }.
% 0.76/1.16 (533) {G0,W20,D3,L4,V0,M4} { ! op( e0, e0 ) = e1, ! op( e1, e1 ) = e1, !
% 0.76/1.16 op( e2, e2 ) = e1, ! op( e3, e3 ) = e1 }.
% 0.76/1.16 (534) {G0,W20,D3,L4,V0,M4} { ! op( e0, e0 ) = e2, ! op( e1, e1 ) = e2, !
% 0.76/1.16 op( e2, e2 ) = e2, ! op( e3, e3 ) = e2 }.
% 0.76/1.16 (535) {G0,W20,D3,L4,V0,M4} { ! op( e0, e0 ) = e3, ! op( e1, e1 ) = e3, !
% 0.76/1.16 op( e2, e2 ) = e3, ! op( e3, e3 ) = e3 }.
% 0.76/1.16 (536) {G0,W2,D1,L2,V0,M2} { alpha1, alpha2 }.
% 0.76/1.16 (537) {G0,W6,D3,L2,V0,M2} { alpha1, op( e3, e3 ) = e3 }.
% 0.76/1.16 (538) {G0,W6,D3,L2,V0,M2} { ! alpha2, op( e0, e0 ) = e3 }.
% 0.76/1.16 (539) {G0,W6,D3,L2,V0,M2} { ! alpha2, op( e1, e1 ) = e3 }.
% 0.76/1.16 (540) {G0,W6,D3,L2,V0,M2} { ! alpha2, op( e2, e2 ) = e3 }.
% 0.76/1.16 (541) {G0,W16,D3,L4,V0,M4} { ! op( e0, e0 ) = e3, ! op( e1, e1 ) = e3, !
% 0.76/1.16 op( e2, e2 ) = e3, alpha2 }.
% 0.76/1.16 (542) {G0,W3,D1,L3,V0,M3} { ! alpha1, alpha3, alpha4 }.
% 0.76/1.16 (543) {G0,W2,D1,L2,V0,M2} { ! alpha3, alpha1 }.
% 0.76/1.16 (544) {G0,W2,D1,L2,V0,M2} { ! alpha4, alpha1 }.
% 0.76/1.16 (545) {G0,W2,D1,L2,V0,M2} { ! alpha4, alpha6 }.
% 0.76/1.16 (546) {G0,W6,D3,L2,V0,M2} { ! alpha4, op( e3, e3 ) = e2 }.
% 0.76/1.16 (547) {G0,W7,D3,L3,V0,M3} { ! alpha6, ! op( e3, e3 ) = e2, alpha4 }.
% 0.76/1.16 (548) {G0,W6,D3,L2,V0,M2} { ! alpha6, op( e0, e0 ) = e2 }.
% 0.76/1.16 (549) {G0,W6,D3,L2,V0,M2} { ! alpha6, op( e1, e1 ) = e2 }.
% 0.76/1.16 (550) {G0,W6,D3,L2,V0,M2} { ! alpha6, op( e2, e2 ) = e2 }.
% 0.76/1.16 (551) {G0,W16,D3,L4,V0,M4} { ! op( e0, e0 ) = e2, ! op( e1, e1 ) = e2, !
% 0.76/1.16 op( e2, e2 ) = e2, alpha6 }.
% 0.76/1.16 (552) {G0,W3,D1,L3,V0,M3} { ! alpha3, alpha5, alpha7 }.
% 0.76/1.16 (553) {G0,W2,D1,L2,V0,M2} { ! alpha5, alpha3 }.
% 0.76/1.16 (554) {G0,W2,D1,L2,V0,M2} { ! alpha7, alpha3 }.
% 0.76/1.16 (555) {G0,W2,D1,L2,V0,M2} { ! alpha7, alpha9 }.
% 0.76/1.16 (556) {G0,W6,D3,L2,V0,M2} { ! alpha7, op( e3, e3 ) = e1 }.
% 0.76/1.16 (557) {G0,W7,D3,L3,V0,M3} { ! alpha9, ! op( e3, e3 ) = e1, alpha7 }.
% 0.76/1.16 (558) {G0,W6,D3,L2,V0,M2} { ! alpha9, op( e0, e0 ) = e1 }.
% 0.76/1.16 (559) {G0,W6,D3,L2,V0,M2} { ! alpha9, op( e1, e1 ) = e1 }.
% 0.76/1.16 (560) {G0,W6,D3,L2,V0,M2} { ! alpha9, op( e2, e2 ) = e1 }.
% 0.76/1.16 (561) {G0,W16,D3,L4,V0,M4} { ! op( e0, e0 ) = e1, ! op( e1, e1 ) = e1, !
% 0.76/1.16 op( e2, e2 ) = e1, alpha9 }.
% 0.76/1.16 (562) {G0,W2,D1,L2,V0,M2} { ! alpha5, alpha8 }.
% 0.76/1.16 (563) {G0,W6,D3,L2,V0,M2} { ! alpha5, op( e3, e3 ) = e0 }.
% 0.76/1.16 (564) {G0,W7,D3,L3,V0,M3} { ! alpha8, ! op( e3, e3 ) = e0, alpha5 }.
% 0.76/1.16 (565) {G0,W6,D3,L2,V0,M2} { ! alpha8, op( e0, e0 ) = e0 }.
% 0.76/1.16 (566) {G0,W6,D3,L2,V0,M2} { ! alpha8, op( e1, e1 ) = e0 }.
% 0.76/1.16 (567) {G0,W6,D3,L2,V0,M2} { ! alpha8, op( e2, e2 ) = e0 }.
% 0.76/1.16 (568) {G0,W16,D3,L4,V0,M4} { ! op( e0, e0 ) = e0, ! op( e1, e1 ) = e0, !
% 0.76/1.16 op( e2, e2 ) = e0, alpha8 }.
% 0.76/1.16
% 0.76/1.16
% 0.76/1.16 Total Proof:
% 0.76/1.16
% 0.76/1.16 *** allocated 15000 integers for termspace/termends
% 0.76/1.16 subsumption: (17) {G0,W5,D3,L1,V0,M1} I { op( e0, unit ) ==> e0 }.
% 0.76/1.16 parent0: (437) {G0,W5,D3,L1,V0,M1} { op( e0, unit ) = e0 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35 permutation0:
% 0.76/1.35 0 ==> 0
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 *** allocated 22500 integers for termspace/termends
% 0.76/1.35 *** allocated 50625 integers for clauses
% 0.76/1.35 *** allocated 33750 integers for termspace/termends
% 0.76/1.35 subsumption: (57) {G0,W3,D2,L1,V0,M1} I { unit ==> e0 }.
% 0.76/1.35 parent0: (477) {G0,W3,D2,L1,V0,M1} { unit = e0 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35 permutation0:
% 0.76/1.35 0 ==> 0
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 *** allocated 75937 integers for clauses
% 0.76/1.35 *** allocated 50625 integers for termspace/termends
% 0.76/1.35 eqswap: (2347) {G0,W3,D2,L1,V0,M1} { ! e1 = e0 }.
% 0.76/1.35 parent0[0]: (526) {G0,W3,D2,L1,V0,M1} { ! e0 = e1 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 subsumption: (106) {G0,W3,D2,L1,V0,M1} I { ! e1 ==> e0 }.
% 0.76/1.35 parent0: (2347) {G0,W3,D2,L1,V0,M1} { ! e1 = e0 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35 permutation0:
% 0.76/1.35 0 ==> 0
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 *** allocated 75937 integers for termspace/termends
% 0.76/1.35 *** allocated 113905 integers for clauses
% 0.76/1.35 eqswap: (3141) {G0,W3,D2,L1,V0,M1} { ! e2 = e0 }.
% 0.76/1.35 parent0[0]: (527) {G0,W3,D2,L1,V0,M1} { ! e0 = e2 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 subsumption: (107) {G0,W3,D2,L1,V0,M1} I { ! e2 ==> e0 }.
% 0.76/1.35 parent0: (3141) {G0,W3,D2,L1,V0,M1} { ! e2 = e0 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35 permutation0:
% 0.76/1.35 0 ==> 0
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 eqswap: (3936) {G0,W3,D2,L1,V0,M1} { ! e3 = e0 }.
% 0.76/1.35 parent0[0]: (528) {G0,W3,D2,L1,V0,M1} { ! e0 = e3 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 subsumption: (108) {G0,W3,D2,L1,V0,M1} I { ! e3 ==> e0 }.
% 0.76/1.35 parent0: (3936) {G0,W3,D2,L1,V0,M1} { ! e3 = e0 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35 permutation0:
% 0.76/1.35 0 ==> 0
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 *** allocated 113905 integers for termspace/termends
% 0.76/1.35 *** allocated 170857 integers for clauses
% 0.76/1.35 subsumption: (112) {G0,W20,D3,L4,V0,M4} I { ! op( e0, e0 ) ==> e0, ! op( e1
% 0.76/1.35 , e1 ) ==> e0, ! op( e2, e2 ) ==> e0, ! op( e3, e3 ) ==> e0 }.
% 0.76/1.35 parent0: (532) {G0,W20,D3,L4,V0,M4} { ! op( e0, e0 ) = e0, ! op( e1, e1 )
% 0.76/1.35 = e0, ! op( e2, e2 ) = e0, ! op( e3, e3 ) = e0 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35 permutation0:
% 0.76/1.35 0 ==> 0
% 0.76/1.35 1 ==> 1
% 0.76/1.35 2 ==> 2
% 0.76/1.35 3 ==> 3
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 subsumption: (116) {G0,W2,D1,L2,V0,M2} I { alpha1, alpha2 }.
% 0.76/1.35 parent0: (536) {G0,W2,D1,L2,V0,M2} { alpha1, alpha2 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35 permutation0:
% 0.76/1.35 0 ==> 0
% 0.76/1.35 1 ==> 1
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 *** allocated 170857 integers for termspace/termends
% 0.76/1.35 subsumption: (118) {G0,W6,D3,L2,V0,M2} I { ! alpha2, op( e0, e0 ) ==> e3
% 0.76/1.35 }.
% 0.76/1.35 parent0: (538) {G0,W6,D3,L2,V0,M2} { ! alpha2, op( e0, e0 ) = e3 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35 permutation0:
% 0.76/1.35 0 ==> 0
% 0.76/1.35 1 ==> 1
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 *** allocated 256285 integers for clauses
% 0.76/1.35 subsumption: (122) {G0,W3,D1,L3,V0,M3} I { ! alpha1, alpha3, alpha4 }.
% 0.76/1.35 parent0: (542) {G0,W3,D1,L3,V0,M3} { ! alpha1, alpha3, alpha4 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35 permutation0:
% 0.76/1.35 0 ==> 0
% 0.76/1.35 1 ==> 1
% 0.76/1.35 2 ==> 2
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 subsumption: (125) {G0,W2,D1,L2,V0,M2} I { ! alpha4, alpha6 }.
% 0.76/1.35 parent0: (545) {G0,W2,D1,L2,V0,M2} { ! alpha4, alpha6 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35 permutation0:
% 0.76/1.35 0 ==> 0
% 0.76/1.35 1 ==> 1
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 *** allocated 256285 integers for termspace/termends
% 0.76/1.35 subsumption: (128) {G0,W6,D3,L2,V0,M2} I { ! alpha6, op( e0, e0 ) ==> e2
% 0.76/1.35 }.
% 0.76/1.35 parent0: (548) {G0,W6,D3,L2,V0,M2} { ! alpha6, op( e0, e0 ) = e2 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35 permutation0:
% 0.76/1.35 0 ==> 0
% 0.76/1.35 1 ==> 1
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 subsumption: (132) {G0,W3,D1,L3,V0,M3} I { ! alpha3, alpha5, alpha7 }.
% 0.76/1.35 parent0: (552) {G0,W3,D1,L3,V0,M3} { ! alpha3, alpha5, alpha7 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35 permutation0:
% 0.76/1.35 0 ==> 0
% 0.76/1.35 1 ==> 1
% 0.76/1.35 2 ==> 2
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 *** allocated 384427 integers for clauses
% 0.76/1.35 subsumption: (135) {G0,W2,D1,L2,V0,M2} I { ! alpha7, alpha9 }.
% 0.76/1.35 parent0: (555) {G0,W2,D1,L2,V0,M2} { ! alpha7, alpha9 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35 permutation0:
% 0.76/1.35 0 ==> 0
% 0.76/1.35 1 ==> 1
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 subsumption: (138) {G0,W6,D3,L2,V0,M2} I { ! alpha9, op( e0, e0 ) ==> e1
% 0.76/1.35 }.
% 0.76/1.35 parent0: (558) {G0,W6,D3,L2,V0,M2} { ! alpha9, op( e0, e0 ) = e1 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35 permutation0:
% 0.76/1.35 0 ==> 0
% 0.76/1.35 1 ==> 1
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 subsumption: (142) {G0,W2,D1,L2,V0,M2} I { ! alpha5, alpha8 }.
% 0.76/1.35 parent0: (562) {G0,W2,D1,L2,V0,M2} { ! alpha5, alpha8 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35 permutation0:
% 0.76/1.35 0 ==> 0
% 0.76/1.35 1 ==> 1
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 *** allocated 384427 integers for termspace/termends
% 0.76/1.35 subsumption: (143) {G0,W6,D3,L2,V0,M2} I { ! alpha5, op( e3, e3 ) ==> e0
% 0.76/1.35 }.
% 0.76/1.35 parent0: (563) {G0,W6,D3,L2,V0,M2} { ! alpha5, op( e3, e3 ) = e0 }.
% 0.76/1.35 substitution0:
% 0.76/1.35 end
% 0.76/1.35 permutation0:
% 0.76/1.35 0 ==> 0
% 0.76/1.35 1 ==> 1
% 0.76/1.35 end
% 0.76/1.35
% 0.76/1.35 subsumption: (146) {G0,W6,D3,L2,V0,M2} I { ! alpha8, op( e1, e1 ) ==> e0
% 0.76/1.36 }.
% 0.76/1.36 parent0: (566) {G0,W6,D3,L2,V0,M2} { ! alpha8, op( e1, e1 ) = e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 0
% 0.76/1.36 1 ==> 1
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (147) {G0,W6,D3,L2,V0,M2} I { ! alpha8, op( e2, e2 ) ==> e0
% 0.76/1.36 }.
% 0.76/1.36 parent0: (567) {G0,W6,D3,L2,V0,M2} { ! alpha8, op( e2, e2 ) = e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 0
% 0.76/1.36 1 ==> 1
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15306) {G1,W3,D1,L3,V0,M3} { alpha9, ! alpha3, alpha5 }.
% 0.76/1.36 parent0[0]: (135) {G0,W2,D1,L2,V0,M2} I { ! alpha7, alpha9 }.
% 0.76/1.36 parent1[2]: (132) {G0,W3,D1,L3,V0,M3} I { ! alpha3, alpha5, alpha7 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (151) {G1,W3,D1,L3,V0,M3} R(132,135) { ! alpha3, alpha5,
% 0.76/1.36 alpha9 }.
% 0.76/1.36 parent0: (15306) {G1,W3,D1,L3,V0,M3} { alpha9, ! alpha3, alpha5 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 2
% 0.76/1.36 1 ==> 0
% 0.76/1.36 2 ==> 1
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15307) {G1,W3,D1,L3,V0,M3} { alpha8, ! alpha3, alpha9 }.
% 0.76/1.36 parent0[0]: (142) {G0,W2,D1,L2,V0,M2} I { ! alpha5, alpha8 }.
% 0.76/1.36 parent1[1]: (151) {G1,W3,D1,L3,V0,M3} R(132,135) { ! alpha3, alpha5, alpha9
% 0.76/1.36 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (153) {G2,W3,D1,L3,V0,M3} R(151,142) { ! alpha3, alpha9,
% 0.76/1.36 alpha8 }.
% 0.76/1.36 parent0: (15307) {G1,W3,D1,L3,V0,M3} { alpha8, ! alpha3, alpha9 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 2
% 0.76/1.36 1 ==> 0
% 0.76/1.36 2 ==> 1
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15308) {G1,W3,D1,L3,V0,M3} { alpha3, alpha4, alpha2 }.
% 0.76/1.36 parent0[0]: (122) {G0,W3,D1,L3,V0,M3} I { ! alpha1, alpha3, alpha4 }.
% 0.76/1.36 parent1[0]: (116) {G0,W2,D1,L2,V0,M2} I { alpha1, alpha2 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (158) {G1,W3,D1,L3,V0,M3} R(122,116) { alpha3, alpha4, alpha2
% 0.76/1.36 }.
% 0.76/1.36 parent0: (15308) {G1,W3,D1,L3,V0,M3} { alpha3, alpha4, alpha2 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 0
% 0.76/1.36 1 ==> 1
% 0.76/1.36 2 ==> 2
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15309) {G1,W3,D1,L3,V0,M3} { alpha6, alpha3, alpha2 }.
% 0.76/1.36 parent0[0]: (125) {G0,W2,D1,L2,V0,M2} I { ! alpha4, alpha6 }.
% 0.76/1.36 parent1[1]: (158) {G1,W3,D1,L3,V0,M3} R(122,116) { alpha3, alpha4, alpha2
% 0.76/1.36 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (164) {G2,W3,D1,L3,V0,M3} R(158,125) { alpha3, alpha2, alpha6
% 0.76/1.36 }.
% 0.76/1.36 parent0: (15309) {G1,W3,D1,L3,V0,M3} { alpha6, alpha3, alpha2 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 2
% 0.76/1.36 1 ==> 0
% 0.76/1.36 2 ==> 1
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15310) {G3,W4,D1,L4,V0,M4} { alpha9, alpha8, alpha2, alpha6
% 0.76/1.36 }.
% 0.76/1.36 parent0[0]: (153) {G2,W3,D1,L3,V0,M3} R(151,142) { ! alpha3, alpha9, alpha8
% 0.76/1.36 }.
% 0.76/1.36 parent1[0]: (164) {G2,W3,D1,L3,V0,M3} R(158,125) { alpha3, alpha2, alpha6
% 0.76/1.36 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (166) {G3,W4,D1,L4,V0,M4} R(164,153) { alpha2, alpha6, alpha9
% 0.76/1.36 , alpha8 }.
% 0.76/1.36 parent0: (15310) {G3,W4,D1,L4,V0,M4} { alpha9, alpha8, alpha2, alpha6 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 2
% 0.76/1.36 1 ==> 3
% 0.76/1.36 2 ==> 0
% 0.76/1.36 3 ==> 1
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15311) {G2,W4,D1,L4,V0,M4} { alpha5, alpha9, alpha2, alpha6
% 0.76/1.36 }.
% 0.76/1.36 parent0[0]: (151) {G1,W3,D1,L3,V0,M3} R(132,135) { ! alpha3, alpha5, alpha9
% 0.76/1.36 }.
% 0.76/1.36 parent1[0]: (164) {G2,W3,D1,L3,V0,M3} R(158,125) { alpha3, alpha2, alpha6
% 0.76/1.36 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (167) {G3,W4,D1,L4,V0,M4} R(164,151) { alpha2, alpha6, alpha5
% 0.76/1.36 , alpha9 }.
% 0.76/1.36 parent0: (15311) {G2,W4,D1,L4,V0,M4} { alpha5, alpha9, alpha2, alpha6 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 2
% 0.76/1.36 1 ==> 3
% 0.76/1.36 2 ==> 0
% 0.76/1.36 3 ==> 1
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 paramod: (15314) {G1,W5,D3,L1,V0,M1} { op( e0, e0 ) ==> e0 }.
% 0.76/1.36 parent0[0]: (57) {G0,W3,D2,L1,V0,M1} I { unit ==> e0 }.
% 0.76/1.36 parent1[0; 3]: (17) {G0,W5,D3,L1,V0,M1} I { op( e0, unit ) ==> e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (179) {G1,W5,D3,L1,V0,M1} S(17);d(57) { op( e0, e0 ) ==> e0
% 0.76/1.36 }.
% 0.76/1.36 parent0: (15314) {G1,W5,D3,L1,V0,M1} { op( e0, e0 ) ==> e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 0
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 paramod: (15318) {G1,W4,D2,L2,V0,M2} { e0 ==> e1, ! alpha9 }.
% 0.76/1.36 parent0[0]: (179) {G1,W5,D3,L1,V0,M1} S(17);d(57) { op( e0, e0 ) ==> e0 }.
% 0.76/1.36 parent1[1; 1]: (138) {G0,W6,D3,L2,V0,M2} I { ! alpha9, op( e0, e0 ) ==> e1
% 0.76/1.36 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqswap: (15319) {G1,W4,D2,L2,V0,M2} { e1 ==> e0, ! alpha9 }.
% 0.76/1.36 parent0[0]: (15318) {G1,W4,D2,L2,V0,M2} { e0 ==> e1, ! alpha9 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (253) {G2,W4,D2,L2,V0,M2} S(138);d(179) { ! alpha9, e1 ==> e0
% 0.76/1.36 }.
% 0.76/1.36 parent0: (15319) {G1,W4,D2,L2,V0,M2} { e1 ==> e0, ! alpha9 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 1
% 0.76/1.36 1 ==> 0
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15322) {G1,W1,D1,L1,V0,M1} { ! alpha9 }.
% 0.76/1.36 parent0[0]: (106) {G0,W3,D2,L1,V0,M1} I { ! e1 ==> e0 }.
% 0.76/1.36 parent1[1]: (253) {G2,W4,D2,L2,V0,M2} S(138);d(179) { ! alpha9, e1 ==> e0
% 0.76/1.36 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (254) {G3,W1,D1,L1,V0,M1} S(253);r(106) { ! alpha9 }.
% 0.76/1.36 parent0: (15322) {G1,W1,D1,L1,V0,M1} { ! alpha9 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 0
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15323) {G4,W3,D1,L3,V0,M3} { alpha2, alpha6, alpha5 }.
% 0.76/1.36 parent0[0]: (254) {G3,W1,D1,L1,V0,M1} S(253);r(106) { ! alpha9 }.
% 0.76/1.36 parent1[3]: (167) {G3,W4,D1,L4,V0,M4} R(164,151) { alpha2, alpha6, alpha5,
% 0.76/1.36 alpha9 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (259) {G4,W3,D1,L3,V0,M3} R(254,167) { alpha2, alpha6, alpha5
% 0.76/1.36 }.
% 0.76/1.36 parent0: (15323) {G4,W3,D1,L3,V0,M3} { alpha2, alpha6, alpha5 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 0
% 0.76/1.36 1 ==> 1
% 0.76/1.36 2 ==> 2
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15324) {G4,W3,D1,L3,V0,M3} { alpha2, alpha6, alpha8 }.
% 0.76/1.36 parent0[0]: (254) {G3,W1,D1,L1,V0,M1} S(253);r(106) { ! alpha9 }.
% 0.76/1.36 parent1[2]: (166) {G3,W4,D1,L4,V0,M4} R(164,153) { alpha2, alpha6, alpha9,
% 0.76/1.36 alpha8 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (260) {G4,W3,D1,L3,V0,M3} R(254,166) { alpha2, alpha6, alpha8
% 0.76/1.36 }.
% 0.76/1.36 parent0: (15324) {G4,W3,D1,L3,V0,M3} { alpha2, alpha6, alpha8 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 0
% 0.76/1.36 1 ==> 1
% 0.76/1.36 2 ==> 2
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 paramod: (15327) {G1,W4,D2,L2,V0,M2} { e0 ==> e2, ! alpha6 }.
% 0.76/1.36 parent0[0]: (179) {G1,W5,D3,L1,V0,M1} S(17);d(57) { op( e0, e0 ) ==> e0 }.
% 0.76/1.36 parent1[1; 1]: (128) {G0,W6,D3,L2,V0,M2} I { ! alpha6, op( e0, e0 ) ==> e2
% 0.76/1.36 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqswap: (15328) {G1,W4,D2,L2,V0,M2} { e2 ==> e0, ! alpha6 }.
% 0.76/1.36 parent0[0]: (15327) {G1,W4,D2,L2,V0,M2} { e0 ==> e2, ! alpha6 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (313) {G2,W4,D2,L2,V0,M2} S(128);d(179) { ! alpha6, e2 ==> e0
% 0.76/1.36 }.
% 0.76/1.36 parent0: (15328) {G1,W4,D2,L2,V0,M2} { e2 ==> e0, ! alpha6 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 1
% 0.76/1.36 1 ==> 0
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15331) {G1,W1,D1,L1,V0,M1} { ! alpha6 }.
% 0.76/1.36 parent0[0]: (107) {G0,W3,D2,L1,V0,M1} I { ! e2 ==> e0 }.
% 0.76/1.36 parent1[1]: (313) {G2,W4,D2,L2,V0,M2} S(128);d(179) { ! alpha6, e2 ==> e0
% 0.76/1.36 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (314) {G3,W1,D1,L1,V0,M1} S(313);r(107) { ! alpha6 }.
% 0.76/1.36 parent0: (15331) {G1,W1,D1,L1,V0,M1} { ! alpha6 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 0
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15332) {G4,W2,D1,L2,V0,M2} { alpha2, alpha8 }.
% 0.76/1.36 parent0[0]: (314) {G3,W1,D1,L1,V0,M1} S(313);r(107) { ! alpha6 }.
% 0.76/1.36 parent1[1]: (260) {G4,W3,D1,L3,V0,M3} R(254,166) { alpha2, alpha6, alpha8
% 0.76/1.36 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (317) {G5,W2,D1,L2,V0,M2} R(314,260) { alpha2, alpha8 }.
% 0.76/1.36 parent0: (15332) {G4,W2,D1,L2,V0,M2} { alpha2, alpha8 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 0
% 0.76/1.36 1 ==> 1
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15333) {G4,W2,D1,L2,V0,M2} { alpha2, alpha5 }.
% 0.76/1.36 parent0[0]: (314) {G3,W1,D1,L1,V0,M1} S(313);r(107) { ! alpha6 }.
% 0.76/1.36 parent1[1]: (259) {G4,W3,D1,L3,V0,M3} R(254,167) { alpha2, alpha6, alpha5
% 0.76/1.36 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (318) {G5,W2,D1,L2,V0,M2} R(314,259) { alpha2, alpha5 }.
% 0.76/1.36 parent0: (15333) {G4,W2,D1,L2,V0,M2} { alpha2, alpha5 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 0
% 0.76/1.36 1 ==> 1
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqswap: (15334) {G0,W6,D3,L2,V0,M2} { e0 ==> op( e1, e1 ), ! alpha8 }.
% 0.76/1.36 parent0[1]: (146) {G0,W6,D3,L2,V0,M2} I { ! alpha8, op( e1, e1 ) ==> e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15335) {G1,W6,D3,L2,V0,M2} { e0 ==> op( e1, e1 ), alpha2 }.
% 0.76/1.36 parent0[1]: (15334) {G0,W6,D3,L2,V0,M2} { e0 ==> op( e1, e1 ), ! alpha8
% 0.76/1.36 }.
% 0.76/1.36 parent1[1]: (317) {G5,W2,D1,L2,V0,M2} R(314,260) { alpha2, alpha8 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqswap: (15336) {G1,W6,D3,L2,V0,M2} { op( e1, e1 ) ==> e0, alpha2 }.
% 0.76/1.36 parent0[0]: (15335) {G1,W6,D3,L2,V0,M2} { e0 ==> op( e1, e1 ), alpha2 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (325) {G6,W6,D3,L2,V0,M2} R(317,146) { alpha2, op( e1, e1 )
% 0.76/1.36 ==> e0 }.
% 0.76/1.36 parent0: (15336) {G1,W6,D3,L2,V0,M2} { op( e1, e1 ) ==> e0, alpha2 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 1
% 0.76/1.36 1 ==> 0
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqswap: (15337) {G0,W6,D3,L2,V0,M2} { e0 ==> op( e2, e2 ), ! alpha8 }.
% 0.76/1.36 parent0[1]: (147) {G0,W6,D3,L2,V0,M2} I { ! alpha8, op( e2, e2 ) ==> e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15338) {G1,W6,D3,L2,V0,M2} { e0 ==> op( e2, e2 ), alpha2 }.
% 0.76/1.36 parent0[1]: (15337) {G0,W6,D3,L2,V0,M2} { e0 ==> op( e2, e2 ), ! alpha8
% 0.76/1.36 }.
% 0.76/1.36 parent1[1]: (317) {G5,W2,D1,L2,V0,M2} R(314,260) { alpha2, alpha8 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqswap: (15339) {G1,W6,D3,L2,V0,M2} { op( e2, e2 ) ==> e0, alpha2 }.
% 0.76/1.36 parent0[0]: (15338) {G1,W6,D3,L2,V0,M2} { e0 ==> op( e2, e2 ), alpha2 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (326) {G6,W6,D3,L2,V0,M2} R(317,147) { alpha2, op( e2, e2 )
% 0.76/1.36 ==> e0 }.
% 0.76/1.36 parent0: (15339) {G1,W6,D3,L2,V0,M2} { op( e2, e2 ) ==> e0, alpha2 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 1
% 0.76/1.36 1 ==> 0
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqswap: (15340) {G0,W6,D3,L2,V0,M2} { e0 ==> op( e3, e3 ), ! alpha5 }.
% 0.76/1.36 parent0[1]: (143) {G0,W6,D3,L2,V0,M2} I { ! alpha5, op( e3, e3 ) ==> e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15341) {G1,W6,D3,L2,V0,M2} { e0 ==> op( e3, e3 ), alpha2 }.
% 0.76/1.36 parent0[1]: (15340) {G0,W6,D3,L2,V0,M2} { e0 ==> op( e3, e3 ), ! alpha5
% 0.76/1.36 }.
% 0.76/1.36 parent1[1]: (318) {G5,W2,D1,L2,V0,M2} R(314,259) { alpha2, alpha5 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqswap: (15342) {G1,W6,D3,L2,V0,M2} { op( e3, e3 ) ==> e0, alpha2 }.
% 0.76/1.36 parent0[0]: (15341) {G1,W6,D3,L2,V0,M2} { e0 ==> op( e3, e3 ), alpha2 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (327) {G6,W6,D3,L2,V0,M2} R(318,143) { alpha2, op( e3, e3 )
% 0.76/1.36 ==> e0 }.
% 0.76/1.36 parent0: (15342) {G1,W6,D3,L2,V0,M2} { op( e3, e3 ) ==> e0, alpha2 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 1
% 0.76/1.36 1 ==> 0
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 paramod: (15345) {G1,W4,D2,L2,V0,M2} { e0 ==> e3, ! alpha2 }.
% 0.76/1.36 parent0[0]: (179) {G1,W5,D3,L1,V0,M1} S(17);d(57) { op( e0, e0 ) ==> e0 }.
% 0.76/1.36 parent1[1; 1]: (118) {G0,W6,D3,L2,V0,M2} I { ! alpha2, op( e0, e0 ) ==> e3
% 0.76/1.36 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqswap: (15346) {G1,W4,D2,L2,V0,M2} { e3 ==> e0, ! alpha2 }.
% 0.76/1.36 parent0[0]: (15345) {G1,W4,D2,L2,V0,M2} { e0 ==> e3, ! alpha2 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (356) {G2,W4,D2,L2,V0,M2} S(118);d(179) { ! alpha2, e3 ==> e0
% 0.76/1.36 }.
% 0.76/1.36 parent0: (15346) {G1,W4,D2,L2,V0,M2} { e3 ==> e0, ! alpha2 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 1
% 0.76/1.36 1 ==> 0
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15349) {G1,W1,D1,L1,V0,M1} { ! alpha2 }.
% 0.76/1.36 parent0[0]: (108) {G0,W3,D2,L1,V0,M1} I { ! e3 ==> e0 }.
% 0.76/1.36 parent1[1]: (356) {G2,W4,D2,L2,V0,M2} S(118);d(179) { ! alpha2, e3 ==> e0
% 0.76/1.36 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (357) {G3,W1,D1,L1,V0,M1} S(356);r(108) { ! alpha2 }.
% 0.76/1.36 parent0: (15349) {G1,W1,D1,L1,V0,M1} { ! alpha2 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 0
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqswap: (15350) {G6,W6,D3,L2,V0,M2} { e0 ==> op( e2, e2 ), alpha2 }.
% 0.76/1.36 parent0[1]: (326) {G6,W6,D3,L2,V0,M2} R(317,147) { alpha2, op( e2, e2 ) ==>
% 0.76/1.36 e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15351) {G4,W5,D3,L1,V0,M1} { e0 ==> op( e2, e2 ) }.
% 0.76/1.36 parent0[0]: (357) {G3,W1,D1,L1,V0,M1} S(356);r(108) { ! alpha2 }.
% 0.76/1.36 parent1[1]: (15350) {G6,W6,D3,L2,V0,M2} { e0 ==> op( e2, e2 ), alpha2 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqswap: (15352) {G4,W5,D3,L1,V0,M1} { op( e2, e2 ) ==> e0 }.
% 0.76/1.36 parent0[0]: (15351) {G4,W5,D3,L1,V0,M1} { e0 ==> op( e2, e2 ) }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (358) {G7,W5,D3,L1,V0,M1} R(357,326) { op( e2, e2 ) ==> e0 }.
% 0.76/1.36 parent0: (15352) {G4,W5,D3,L1,V0,M1} { op( e2, e2 ) ==> e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 0
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqswap: (15353) {G6,W6,D3,L2,V0,M2} { e0 ==> op( e1, e1 ), alpha2 }.
% 0.76/1.36 parent0[1]: (325) {G6,W6,D3,L2,V0,M2} R(317,146) { alpha2, op( e1, e1 ) ==>
% 0.76/1.36 e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15354) {G4,W5,D3,L1,V0,M1} { e0 ==> op( e1, e1 ) }.
% 0.76/1.36 parent0[0]: (357) {G3,W1,D1,L1,V0,M1} S(356);r(108) { ! alpha2 }.
% 0.76/1.36 parent1[1]: (15353) {G6,W6,D3,L2,V0,M2} { e0 ==> op( e1, e1 ), alpha2 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqswap: (15355) {G4,W5,D3,L1,V0,M1} { op( e1, e1 ) ==> e0 }.
% 0.76/1.36 parent0[0]: (15354) {G4,W5,D3,L1,V0,M1} { e0 ==> op( e1, e1 ) }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (359) {G7,W5,D3,L1,V0,M1} R(357,325) { op( e1, e1 ) ==> e0 }.
% 0.76/1.36 parent0: (15355) {G4,W5,D3,L1,V0,M1} { op( e1, e1 ) ==> e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 0
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqswap: (15356) {G6,W6,D3,L2,V0,M2} { e0 ==> op( e3, e3 ), alpha2 }.
% 0.76/1.36 parent0[1]: (327) {G6,W6,D3,L2,V0,M2} R(318,143) { alpha2, op( e3, e3 ) ==>
% 0.76/1.36 e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 resolution: (15357) {G4,W5,D3,L1,V0,M1} { e0 ==> op( e3, e3 ) }.
% 0.76/1.36 parent0[0]: (357) {G3,W1,D1,L1,V0,M1} S(356);r(108) { ! alpha2 }.
% 0.76/1.36 parent1[1]: (15356) {G6,W6,D3,L2,V0,M2} { e0 ==> op( e3, e3 ), alpha2 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqswap: (15358) {G4,W5,D3,L1,V0,M1} { op( e3, e3 ) ==> e0 }.
% 0.76/1.36 parent0[0]: (15357) {G4,W5,D3,L1,V0,M1} { e0 ==> op( e3, e3 ) }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (360) {G7,W5,D3,L1,V0,M1} R(357,327) { op( e3, e3 ) ==> e0 }.
% 0.76/1.36 parent0: (15358) {G4,W5,D3,L1,V0,M1} { op( e3, e3 ) ==> e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 0 ==> 0
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 paramod: (15378) {G1,W18,D3,L4,V0,M4} { ! e0 ==> e0, ! op( e1, e1 ) ==> e0
% 0.76/1.36 , ! op( e2, e2 ) ==> e0, ! op( e3, e3 ) ==> e0 }.
% 0.76/1.36 parent0[0]: (179) {G1,W5,D3,L1,V0,M1} S(17);d(57) { op( e0, e0 ) ==> e0 }.
% 0.76/1.36 parent1[0; 2]: (112) {G0,W20,D3,L4,V0,M4} I { ! op( e0, e0 ) ==> e0, ! op(
% 0.76/1.36 e1, e1 ) ==> e0, ! op( e2, e2 ) ==> e0, ! op( e3, e3 ) ==> e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqrefl: (15379) {G0,W15,D3,L3,V0,M3} { ! op( e1, e1 ) ==> e0, ! op( e2, e2
% 0.76/1.36 ) ==> e0, ! op( e3, e3 ) ==> e0 }.
% 0.76/1.36 parent0[0]: (15378) {G1,W18,D3,L4,V0,M4} { ! e0 ==> e0, ! op( e1, e1 ) ==>
% 0.76/1.36 e0, ! op( e2, e2 ) ==> e0, ! op( e3, e3 ) ==> e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 paramod: (15380) {G1,W13,D3,L3,V0,M3} { ! e0 ==> e0, ! op( e2, e2 ) ==> e0
% 0.76/1.36 , ! op( e3, e3 ) ==> e0 }.
% 0.76/1.36 parent0[0]: (359) {G7,W5,D3,L1,V0,M1} R(357,325) { op( e1, e1 ) ==> e0 }.
% 0.76/1.36 parent1[0; 2]: (15379) {G0,W15,D3,L3,V0,M3} { ! op( e1, e1 ) ==> e0, ! op
% 0.76/1.36 ( e2, e2 ) ==> e0, ! op( e3, e3 ) ==> e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 paramod: (15381) {G2,W11,D3,L3,V0,M3} { ! e0 ==> e0, ! e0 ==> e0, ! op( e3
% 0.76/1.36 , e3 ) ==> e0 }.
% 0.76/1.36 parent0[0]: (358) {G7,W5,D3,L1,V0,M1} R(357,326) { op( e2, e2 ) ==> e0 }.
% 0.76/1.36 parent1[1; 2]: (15380) {G1,W13,D3,L3,V0,M3} { ! e0 ==> e0, ! op( e2, e2 )
% 0.76/1.36 ==> e0, ! op( e3, e3 ) ==> e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 paramod: (15388) {G3,W9,D2,L3,V0,M3} { ! e0 ==> e0, ! e0 ==> e0, ! e0 ==>
% 0.76/1.36 e0 }.
% 0.76/1.36 parent0[0]: (360) {G7,W5,D3,L1,V0,M1} R(357,327) { op( e3, e3 ) ==> e0 }.
% 0.76/1.36 parent1[2; 2]: (15381) {G2,W11,D3,L3,V0,M3} { ! e0 ==> e0, ! e0 ==> e0, !
% 0.76/1.36 op( e3, e3 ) ==> e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 substitution1:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqrefl: (15394) {G0,W6,D2,L2,V0,M2} { ! e0 ==> e0, ! e0 ==> e0 }.
% 0.76/1.36 parent0[0]: (15388) {G3,W9,D2,L3,V0,M3} { ! e0 ==> e0, ! e0 ==> e0, ! e0
% 0.76/1.36 ==> e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqrefl: (15397) {G0,W3,D2,L1,V0,M1} { ! e0 ==> e0 }.
% 0.76/1.36 parent0[0]: (15394) {G0,W6,D2,L2,V0,M2} { ! e0 ==> e0, ! e0 ==> e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 eqrefl: (15398) {G0,W0,D0,L0,V0,M0} { }.
% 0.76/1.36 parent0[0]: (15397) {G0,W3,D2,L1,V0,M1} { ! e0 ==> e0 }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 subsumption: (418) {G8,W0,D0,L0,V0,M0} S(112);d(179);q;d(359);d(358);d(360)
% 0.76/1.36 ;q;q;q { }.
% 0.76/1.36 parent0: (15398) {G0,W0,D0,L0,V0,M0} { }.
% 0.76/1.36 substitution0:
% 0.76/1.36 end
% 0.76/1.36 permutation0:
% 0.76/1.36 end
% 0.76/1.36
% 0.76/1.36 Proof check complete!
% 0.76/1.36
% 0.76/1.36 Memory use:
% 0.76/1.36
% 0.76/1.36 space for terms: 7851
% 0.76/1.36 space for clauses: 19793
% 0.76/1.36
% 0.76/1.36
% 0.76/1.36 clauses generated: 3910
% 0.76/1.36 clauses kept: 419
% 0.76/1.36 clauses selected: 181
% 0.76/1.36 clauses deleted: 100
% 0.76/1.36 clauses inuse deleted: 0
% 0.76/1.36
% 0.76/1.36 subsentry: 963611
% 0.76/1.36 literals s-matched: 107509
% 0.76/1.36 literals matched: 107509
% 0.76/1.36 full subsumption: 0
% 0.76/1.36
% 0.76/1.36 checksum: -3977638
% 0.76/1.36
% 0.76/1.36
% 0.76/1.36 Bliksem ended
%------------------------------------------------------------------------------