%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : ALG180+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n028.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:49 EDT 2022
% Result : Theorem 0.73s 1.36s
% Output : Refutation 0.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : ALG180+1 : TPTP v8.1.0. Released v2.7.0.
% 0.03/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n028.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 : Tue Jun 7 22:16:15 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.69/1.11 *** allocated 10000 integers for termspace/termends
% 0.69/1.11 *** allocated 10000 integers for clauses
% 0.69/1.11 *** allocated 10000 integers for justifications
% 0.69/1.11 Bliksem 1.12
% 0.69/1.11
% 0.69/1.11
% 0.69/1.11 Automatic Strategy Selection
% 0.69/1.11
% 0.69/1.11
% 0.69/1.11 Clauses:
% 0.69/1.11
% 0.69/1.11 { ! e10 = e11 }.
% 0.69/1.11 { ! e10 = e12 }.
% 0.69/1.11 { ! e10 = e13 }.
% 0.69/1.11 { ! e10 = e14 }.
% 0.69/1.11 { ! e11 = e12 }.
% 0.69/1.11 { ! e11 = e13 }.
% 0.69/1.11 { ! e11 = e14 }.
% 0.69/1.11 { ! e12 = e13 }.
% 0.69/1.11 { ! e12 = e14 }.
% 0.69/1.11 { ! e13 = e14 }.
% 0.69/1.11 { ! e20 = e21 }.
% 0.69/1.11 { ! e20 = e22 }.
% 0.69/1.11 { ! e20 = e23 }.
% 0.69/1.11 { ! e20 = e24 }.
% 0.69/1.11 { ! e21 = e22 }.
% 0.69/1.11 { ! e21 = e23 }.
% 0.69/1.11 { ! e21 = e24 }.
% 0.69/1.11 { ! e22 = e23 }.
% 0.69/1.11 { ! e22 = e24 }.
% 0.69/1.11 { ! e23 = e24 }.
% 0.69/1.11 { ! e10 = e20 }.
% 0.69/1.11 { ! e10 = e21 }.
% 0.69/1.11 { ! e10 = e22 }.
% 0.69/1.11 { ! e10 = e23 }.
% 0.69/1.11 { ! e10 = e24 }.
% 0.69/1.11 { ! e11 = e20 }.
% 0.69/1.11 { ! e11 = e21 }.
% 0.69/1.11 { ! e11 = e22 }.
% 0.69/1.11 { ! e11 = e23 }.
% 0.69/1.11 { ! e11 = e24 }.
% 0.69/1.11 { ! e12 = e20 }.
% 0.69/1.11 { ! e12 = e21 }.
% 0.69/1.11 { ! e12 = e22 }.
% 0.69/1.11 { ! e12 = e23 }.
% 0.69/1.11 { ! e12 = e24 }.
% 0.69/1.11 { ! e13 = e20 }.
% 0.69/1.11 { ! e13 = e21 }.
% 0.69/1.11 { ! e13 = e22 }.
% 0.69/1.11 { ! e13 = e23 }.
% 0.69/1.11 { ! e13 = e24 }.
% 0.69/1.11 { ! e14 = e20 }.
% 0.69/1.11 { ! e14 = e21 }.
% 0.69/1.11 { ! e14 = e22 }.
% 0.69/1.11 { ! e14 = e23 }.
% 0.69/1.11 { ! e14 = e24 }.
% 0.69/1.11 { op1( e10, e10 ) = e13 }.
% 0.69/1.11 { op1( e10, e11 ) = e12 }.
% 0.69/1.11 { op1( e10, e12 ) = e10 }.
% 0.69/1.11 { op1( e10, e13 ) = e11 }.
% 0.69/1.11 { op1( e10, e14 ) = e14 }.
% 0.69/1.11 { op1( e11, e10 ) = e10 }.
% 0.69/1.11 { op1( e11, e11 ) = e14 }.
% 0.69/1.11 { op1( e11, e12 ) = e11 }.
% 0.69/1.11 { op1( e11, e13 ) = e12 }.
% 0.69/1.11 { op1( e11, e14 ) = e13 }.
% 0.69/1.11 { op1( e12, e10 ) = e11 }.
% 0.69/1.11 { op1( e12, e11 ) = e13 }.
% 0.69/1.11 { op1( e12, e12 ) = e12 }.
% 0.69/1.11 { op1( e12, e13 ) = e14 }.
% 0.69/1.11 { op1( e12, e14 ) = e10 }.
% 0.69/1.11 { op1( e13, e10 ) = e14 }.
% 0.69/1.11 { op1( e13, e11 ) = e11 }.
% 0.69/1.11 { op1( e13, e12 ) = e13 }.
% 0.69/1.11 { op1( e13, e13 ) = e10 }.
% 0.69/1.11 { op1( e13, e14 ) = e12 }.
% 0.69/1.11 { op1( e14, e10 ) = e12 }.
% 0.69/1.11 { op1( e14, e11 ) = e10 }.
% 0.69/1.11 { op1( e14, e12 ) = e14 }.
% 0.69/1.11 { op1( e14, e13 ) = e13 }.
% 0.69/1.11 { op1( e14, e14 ) = e11 }.
% 0.69/1.11 { op2( e20, e20 ) = e24 }.
% 0.69/1.11 { op2( e20, e21 ) = e22 }.
% 0.69/1.11 { op2( e20, e22 ) = e20 }.
% 0.69/1.11 { op2( e20, e23 ) = e21 }.
% 0.69/1.11 { op2( e20, e24 ) = e23 }.
% 0.69/1.11 { op2( e21, e20 ) = e20 }.
% 0.69/1.11 { op2( e21, e21 ) = e21 }.
% 0.69/1.11 { op2( e21, e22 ) = e22 }.
% 0.69/1.11 { op2( e21, e23 ) = e23 }.
% 0.69/1.11 { op2( e21, e24 ) = e24 }.
% 0.69/1.11 { op2( e22, e20 ) = e21 }.
% 0.69/1.11 { op2( e22, e21 ) = e24 }.
% 0.69/1.11 { op2( e22, e22 ) = e23 }.
% 0.69/1.11 { op2( e22, e23 ) = e20 }.
% 0.69/1.11 { op2( e22, e24 ) = e22 }.
% 0.69/1.11 { op2( e23, e20 ) = e23 }.
% 0.69/1.11 { op2( e23, e21 ) = e20 }.
% 0.69/1.11 { op2( e23, e22 ) = e24 }.
% 0.69/1.11 { op2( e23, e23 ) = e22 }.
% 0.69/1.11 { op2( e23, e24 ) = e21 }.
% 0.69/1.11 { op2( e24, e20 ) = e22 }.
% 0.69/1.11 { op2( e24, e21 ) = e23 }.
% 0.69/1.11 { op2( e24, e22 ) = e21 }.
% 0.69/1.11 { op2( e24, e23 ) = e24 }.
% 0.69/1.11 { op2( e24, e24 ) = e20 }.
% 0.69/1.11 { h( e10 ) = e20, h( e10 ) = e21, h( e10 ) = e22, h( e10 ) = e23, h( e10 )
% 0.69/1.11 = e24 }.
% 0.69/1.11 { h( e11 ) = e20, h( e11 ) = e21, h( e11 ) = e22, h( e11 ) = e23, h( e11 )
% 0.69/1.11 = e24 }.
% 0.69/1.11 { h( e12 ) = e20, h( e12 ) = e21, h( e12 ) = e22, h( e12 ) = e23, h( e12 )
% 0.69/1.11 = e24 }.
% 0.69/1.11 { h( e13 ) = e20, h( e13 ) = e21, h( e13 ) = e22, h( e13 ) = e23, h( e13 )
% 0.69/1.11 = e24 }.
% 0.69/1.11 { h( e14 ) = e20, h( e14 ) = e21, h( e14 ) = e22, h( e14 ) = e23, h( e14 )
% 0.69/1.11 = e24 }.
% 0.69/1.11 { j( e20 ) = e10, j( e20 ) = e11, j( e20 ) = e12, j( e20 ) = e13, j( e20 )
% 0.69/1.11 = e14 }.
% 0.69/1.11 { j( e21 ) = e10, j( e21 ) = e11, j( e21 ) = e12, j( e21 ) = e13, j( e21 )
% 0.69/1.11 = e14 }.
% 0.69/1.11 { j( e22 ) = e10, j( e22 ) = e11, j( e22 ) = e12, j( e22 ) = e13, j( e22 )
% 0.69/1.11 = e14 }.
% 0.69/1.11 { j( e23 ) = e10, j( e23 ) = e11, j( e23 ) = e12, j( e23 ) = e13, j( e23 )
% 0.69/1.11 = e14 }.
% 0.69/1.11 { j( e24 ) = e10, j( e24 ) = e11, j( e24 ) = e12, j( e24 ) = e13, j( e24 )
% 0.69/1.11 = e14 }.
% 0.69/1.11 { h( op1( e10, e10 ) ) = op2( h( e10 ), h( e10 ) ) }.
% 0.69/1.11 { h( op1( e10, e11 ) ) = op2( h( e10 ), h( e11 ) ) }.
% 0.69/1.11 { h( op1( e10, e12 ) ) = op2( h( e10 ), h( e12 ) ) }.
% 0.69/1.11 { h( op1( e10, e13 ) ) = op2( h( e10 ), h( e13 ) ) }.
% 0.69/1.11 { h( op1( e10, e14 ) ) = op2( h( e10 ), h( e14 ) ) }.
% 0.69/1.11 { h( op1( e11, e10 ) ) = op2( h( e11 ), h( e10 ) ) }.
% 0.69/1.11 { h( op1( e11, e11 ) ) = op2( h( e11 ), h( e11 ) ) }.
% 0.69/1.11 { h( op1( e11, e12 ) ) = op2( h( e11 ), h( e12 ) ) }.
% 0.69/1.11 { h( op1( e11, e13 ) ) = op2( h( e11 ), h( e13 ) ) }.
% 0.69/1.11 { h( op1( e11, e14 ) ) = op2( h( e11 ), h( e14 ) ) }.
% 0.69/1.11 { h( op1( e12, e10 ) ) = op2( h( e12 ), h( e10 ) ) }.
% 0.69/1.11 { h( op1( e12, e11 ) ) = op2( h( e12 ), h( e11 ) ) }.
% 0.69/1.11 { h( op1( e12, e12 ) ) = op2( h( e12 ), h( e12 ) ) }.
% 0.69/1.11 { h( op1( e12, e13 ) ) = op2( h( e12 ), h( e13 ) ) }.
% 0.69/1.11 { h( op1( e12, e14 ) ) = op2( h( e12 ), h( e14 ) ) }.
% 0.69/1.11 { h( op1( e13, e10 ) ) = op2( h( e13 ), h( e10 ) ) }.
% 0.69/1.11 { h( op1( e13, e11 ) ) = op2( h( e13 ), h( e11 ) ) }.
% 0.73/1.36 { h( op1( e13, e12 ) ) = op2( h( e13 ), h( e12 ) ) }.
% 0.73/1.36 { h( op1( e13, e13 ) ) = op2( h( e13 ), h( e13 ) ) }.
% 0.73/1.36 { h( op1( e13, e14 ) ) = op2( h( e13 ), h( e14 ) ) }.
% 0.73/1.36 { h( op1( e14, e10 ) ) = op2( h( e14 ), h( e10 ) ) }.
% 0.73/1.36 { h( op1( e14, e11 ) ) = op2( h( e14 ), h( e11 ) ) }.
% 0.73/1.36 { h( op1( e14, e12 ) ) = op2( h( e14 ), h( e12 ) ) }.
% 0.73/1.36 { h( op1( e14, e13 ) ) = op2( h( e14 ), h( e13 ) ) }.
% 0.73/1.36 { h( op1( e14, e14 ) ) = op2( h( e14 ), h( e14 ) ) }.
% 0.73/1.36 { j( op2( e20, e20 ) ) = op1( j( e20 ), j( e20 ) ) }.
% 0.73/1.36 { j( op2( e20, e21 ) ) = op1( j( e20 ), j( e21 ) ) }.
% 0.73/1.36 { j( op2( e20, e22 ) ) = op1( j( e20 ), j( e22 ) ) }.
% 0.73/1.36 { j( op2( e20, e23 ) ) = op1( j( e20 ), j( e23 ) ) }.
% 0.73/1.36 { j( op2( e20, e24 ) ) = op1( j( e20 ), j( e24 ) ) }.
% 0.73/1.36 { j( op2( e21, e20 ) ) = op1( j( e21 ), j( e20 ) ) }.
% 0.73/1.36 { j( op2( e21, e21 ) ) = op1( j( e21 ), j( e21 ) ) }.
% 0.73/1.36 { j( op2( e21, e22 ) ) = op1( j( e21 ), j( e22 ) ) }.
% 0.73/1.36 { j( op2( e21, e23 ) ) = op1( j( e21 ), j( e23 ) ) }.
% 0.73/1.36 { j( op2( e21, e24 ) ) = op1( j( e21 ), j( e24 ) ) }.
% 0.73/1.36 { j( op2( e22, e20 ) ) = op1( j( e22 ), j( e20 ) ) }.
% 0.73/1.36 { j( op2( e22, e21 ) ) = op1( j( e22 ), j( e21 ) ) }.
% 0.73/1.36 { j( op2( e22, e22 ) ) = op1( j( e22 ), j( e22 ) ) }.
% 0.73/1.36 { j( op2( e22, e23 ) ) = op1( j( e22 ), j( e23 ) ) }.
% 0.73/1.36 { j( op2( e22, e24 ) ) = op1( j( e22 ), j( e24 ) ) }.
% 0.73/1.36 { j( op2( e23, e20 ) ) = op1( j( e23 ), j( e20 ) ) }.
% 0.73/1.36 { j( op2( e23, e21 ) ) = op1( j( e23 ), j( e21 ) ) }.
% 0.73/1.36 { j( op2( e23, e22 ) ) = op1( j( e23 ), j( e22 ) ) }.
% 0.73/1.36 { j( op2( e23, e23 ) ) = op1( j( e23 ), j( e23 ) ) }.
% 0.73/1.36 { j( op2( e23, e24 ) ) = op1( j( e23 ), j( e24 ) ) }.
% 0.73/1.36 { j( op2( e24, e20 ) ) = op1( j( e24 ), j( e20 ) ) }.
% 0.73/1.36 { j( op2( e24, e21 ) ) = op1( j( e24 ), j( e21 ) ) }.
% 0.73/1.36 { j( op2( e24, e22 ) ) = op1( j( e24 ), j( e22 ) ) }.
% 0.73/1.36 { j( op2( e24, e23 ) ) = op1( j( e24 ), j( e23 ) ) }.
% 0.73/1.36 { j( op2( e24, e24 ) ) = op1( j( e24 ), j( e24 ) ) }.
% 0.73/1.36 { h( j( e20 ) ) = e20 }.
% 0.73/1.36 { h( j( e21 ) ) = e21 }.
% 0.73/1.36 { h( j( e22 ) ) = e22 }.
% 0.73/1.36 { h( j( e23 ) ) = e23 }.
% 0.73/1.36 { h( j( e24 ) ) = e24 }.
% 0.73/1.36 { j( h( e10 ) ) = e10 }.
% 0.73/1.36 { j( h( e11 ) ) = e11 }.
% 0.73/1.36 { j( h( e12 ) ) = e12 }.
% 0.73/1.36 { j( h( e13 ) ) = e13 }.
% 0.73/1.36 { j( h( e14 ) ) = e14 }.
% 0.73/1.36
% 0.73/1.36 percentage equality = 1.000000, percentage horn = 0.939394
% 0.73/1.36 This is a pure equality problem
% 0.73/1.36
% 0.73/1.36
% 0.73/1.36
% 0.73/1.36 Options Used:
% 0.73/1.36
% 0.73/1.36 useres = 1
% 0.73/1.36 useparamod = 1
% 0.73/1.36 useeqrefl = 1
% 0.73/1.36 useeqfact = 1
% 0.73/1.36 usefactor = 1
% 0.73/1.36 usesimpsplitting = 0
% 0.73/1.36 usesimpdemod = 5
% 0.73/1.36 usesimpres = 3
% 0.73/1.36
% 0.73/1.36 resimpinuse = 1000
% 0.73/1.36 resimpclauses = 20000
% 0.73/1.36 substype = eqrewr
% 0.73/1.36 backwardsubs = 1
% 0.73/1.36 selectoldest = 5
% 0.73/1.36
% 0.73/1.36 litorderings [0] = split
% 0.73/1.36 litorderings [1] = extend the termordering, first sorting on arguments
% 0.73/1.36
% 0.73/1.36 termordering = kbo
% 0.73/1.36
% 0.73/1.36 litapriori = 0
% 0.73/1.36 termapriori = 1
% 0.73/1.36 litaposteriori = 0
% 0.73/1.36 termaposteriori = 0
% 0.73/1.36 demodaposteriori = 0
% 0.73/1.36 ordereqreflfact = 0
% 0.73/1.36
% 0.73/1.36 litselect = negord
% 0.73/1.36
% 0.73/1.36 maxweight = 15
% 0.73/1.36 maxdepth = 30000
% 0.73/1.36 maxlength = 115
% 0.73/1.36 maxnrvars = 195
% 0.73/1.36 excuselevel = 1
% 0.73/1.36 increasemaxweight = 1
% 0.73/1.36
% 0.73/1.36 maxselected = 10000000
% 0.73/1.36 maxnrclauses = 10000000
% 0.73/1.36
% 0.73/1.36 showgenerated = 0
% 0.73/1.36 showkept = 0
% 0.73/1.36 showselected = 0
% 0.73/1.36 showdeleted = 0
% 0.73/1.36 showresimp = 1
% 0.73/1.36 showstatus = 2000
% 0.73/1.36
% 0.73/1.36 prologoutput = 0
% 0.73/1.36 nrgoals = 5000000
% 0.73/1.36 totalproof = 1
% 0.73/1.36
% 0.73/1.36 Symbols occurring in the translation:
% 0.73/1.36
% 0.73/1.36 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.73/1.36 . [1, 2] (w:1, o:23, a:1, s:1, b:0),
% 0.73/1.36 ! [4, 1] (w:0, o:16, a:1, s:1, b:0),
% 0.73/1.36 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.73/1.36 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.73/1.36 e10 [35, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.73/1.36 e11 [36, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.73/1.36 e12 [37, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.73/1.36 e13 [38, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.73/1.36 e14 [39, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.73/1.36 e20 [40, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.73/1.36 e21 [41, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.73/1.36 e22 [42, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.73/1.36 e23 [43, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.73/1.36 e24 [44, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.73/1.36 op1 [45, 2] (w:1, o:47, a:1, s:1, b:0),
% 0.73/1.36 op2 [46, 2] (w:1, o:48, a:1, s:1, b:0),
% 0.73/1.36 h [47, 1] (w:1, o:21, a:1, s:1, b:0),
% 0.73/1.36 j [48, 1] (w:1, o:22, a:1, s:1, b:0).
% 0.73/1.36
% 0.73/1.36
% 0.73/1.36 Starting Search:
% 0.73/1.36
% 0.73/1.36 *** allocated 15000 integers for clauses
% 0.73/1.36 Resimplifying inuse:
% 0.73/1.36 Done
% 0.73/1.36
% 0.73/1.36 Failed to find proof!
% 0.73/1.36 maxweight = 15
% 0.73/1.36 maxnrclauses = 10000000
% 0.73/1.36 Generated: 14585
% 0.73/1.36 Kept: 215
% 0.73/1.36
% 0.73/1.36
% 0.73/1.36 The strategy used was not complete!
% 0.73/1.36
% 0.73/1.36 Increased maxweight to 16
% 0.73/1.36
% 0.73/1.36 Starting Search:
% 0.73/1.36
% 0.73/1.36 *** allocated 22500 integers for clauses
% 0.73/1.36
% 0.73/1.36 Bliksems!, er is een bewijs:
% 0.73/1.36 % SZS status Theorem
% 0.73/1.36 % SZS output start Refutation
% 0.73/1.36
% 0.73/1.36 (8) {G0,W3,D2,L1,V0,M1} I { ! e14 ==> e12 }.
% 0.73/1.36 (11) {G0,W3,D2,L1,V0,M1} I { ! e22 ==> e20 }.
% 0.73/1.36 (12) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e20 }.
% 0.73/1.36 (13) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e20 }.
% 0.73/1.36 (17) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e22 }.
% 0.73/1.36 (18) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e22 }.
% 0.73/1.36 (57) {G0,W5,D3,L1,V0,M1} I { op1( e12, e12 ) ==> e12 }.
% 0.73/1.36 (67) {G0,W5,D3,L1,V0,M1} I { op1( e14, e12 ) ==> e14 }.
% 0.73/1.36 (70) {G0,W5,D3,L1,V0,M1} I { op2( e20, e20 ) ==> e24 }.
% 0.73/1.36 (71) {G0,W5,D3,L1,V0,M1} I { op2( e20, e21 ) ==> e22 }.
% 0.73/1.36 (81) {G0,W5,D3,L1,V0,M1} I { op2( e22, e21 ) ==> e24 }.
% 0.73/1.36 (82) {G0,W5,D3,L1,V0,M1} I { op2( e22, e22 ) ==> e23 }.
% 0.73/1.36 (86) {G0,W5,D3,L1,V0,M1} I { op2( e23, e21 ) ==> e20 }.
% 0.73/1.36 (88) {G0,W5,D3,L1,V0,M1} I { op2( e23, e23 ) ==> e22 }.
% 0.73/1.36 (91) {G0,W5,D3,L1,V0,M1} I { op2( e24, e21 ) ==> e23 }.
% 0.73/1.36 (94) {G0,W5,D3,L1,V0,M1} I { op2( e24, e24 ) ==> e20 }.
% 0.73/1.36 (97) {G0,W20,D3,L5,V0,M5} I { h( e12 ) ==> e20, h( e12 ) ==> e21, h( e12 )
% 0.73/1.36 ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 0.73/1.36 (99) {G0,W20,D3,L5,V0,M5} I { h( e14 ) ==> e20, h( e14 ) ==> e21, h( e14 )
% 0.73/1.36 ==> e22, h( e14 ) ==> e23, h( e14 ) ==> e24 }.
% 0.73/1.36 (117) {G1,W8,D4,L1,V0,M1} I;d(57) { op2( h( e12 ), h( e12 ) ) ==> h( e12 )
% 0.73/1.36 }.
% 0.73/1.36 (127) {G1,W8,D4,L1,V0,M1} I;d(67) { op2( h( e14 ), h( e12 ) ) ==> h( e14 )
% 0.73/1.36 }.
% 0.73/1.36 (162) {G0,W5,D4,L1,V0,M1} I { j( h( e12 ) ) ==> e12 }.
% 0.73/1.36 (164) {G0,W5,D4,L1,V0,M1} I { j( h( e14 ) ) ==> e14 }.
% 0.73/1.36 (220) {G2,W16,D3,L4,V0,M4} P(97,117);d(70);r(13) { h( e12 ) ==> e21, h( e12
% 0.73/1.36 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 0.73/1.36 (222) {G3,W15,D3,L4,V0,M4} P(97,117);d(88);d(220);r(12) { h( e12 ) ==> e21
% 0.73/1.36 , h( e12 ) ==> e22, h( e12 ) ==> e24, e23 ==> e22 }.
% 0.73/1.36 (224) {G4,W12,D3,L3,V0,M3} E(220);d(222);q { h( e12 ) ==> e21, h( e12 ) ==>
% 0.73/1.36 e22, h( e12 ) ==> e24 }.
% 0.73/1.36 (237) {G5,W8,D3,L2,V0,M2} P(224,117);d(82);r(17) { h( e12 ) ==> e21, h( e12
% 0.73/1.36 ) ==> e24 }.
% 0.73/1.36 (238) {G6,W7,D3,L2,V0,M2} P(224,117);d(94);d(237);r(18) { h( e12 ) ==> e21
% 0.73/1.36 , e24 ==> e20 }.
% 0.73/1.36 (249) {G7,W4,D3,L1,V0,M1} S(238);r(13) { h( e12 ) ==> e21 }.
% 0.73/1.36 (257) {G8,W7,D4,L1,V0,M1} P(249,127) { op2( h( e14 ), e21 ) ==> h( e14 )
% 0.73/1.36 }.
% 0.73/1.36 (258) {G8,W4,D3,L1,V0,M1} P(249,162) { j( e21 ) ==> e12 }.
% 0.73/1.36 (311) {G9,W16,D3,L4,V0,M4} P(99,257);d(71);r(11) { h( e14 ) ==> e21, h( e14
% 0.73/1.36 ) ==> e22, h( e14 ) ==> e23, h( e14 ) ==> e24 }.
% 0.73/1.36 (314) {G10,W15,D3,L4,V0,M4} P(99,257);d(91);d(311);r(13) { h( e14 ) ==> e21
% 0.73/1.36 , h( e14 ) ==> e22, h( e14 ) ==> e23, e24 ==> e23 }.
% 0.73/1.36 (315) {G11,W12,D3,L3,V0,M3} E(311);d(314);q { h( e14 ) ==> e21, h( e14 )
% 0.73/1.36 ==> e22, h( e14 ) ==> e23 }.
% 0.73/1.36 (316) {G12,W8,D3,L2,V0,M2} P(315,257);d(81);r(18) { h( e14 ) ==> e21, h(
% 0.73/1.36 e14 ) ==> e23 }.
% 0.73/1.36 (317) {G13,W7,D3,L2,V0,M2} P(315,257);d(86);d(316);r(17) { h( e14 ) ==> e21
% 0.73/1.36 , e23 ==> e20 }.
% 0.73/1.36 (325) {G14,W4,D3,L1,V0,M1} S(317);r(12) { h( e14 ) ==> e21 }.
% 0.73/1.36 (329) {G15,W3,D2,L1,V0,M1} P(325,164);d(258) { e14 ==> e12 }.
% 0.73/1.36 (330) {G16,W0,D0,L0,V0,M0} S(329);r(8) { }.
% 0.73/1.36
% 0.73/1.36
% 0.73/1.36 % SZS output end Refutation
% 0.73/1.36 found a proof!
% 0.73/1.36
% 0.73/1.36 *** allocated 33750 integers for clauses
% 0.73/1.36
% 0.73/1.36 Unprocessed initial clauses:
% 0.73/1.36
% 0.73/1.36 (332) {G0,W3,D2,L1,V0,M1} { ! e10 = e11 }.
% 0.73/1.36 (333) {G0,W3,D2,L1,V0,M1} { ! e10 = e12 }.
% 0.73/1.36 (334) {G0,W3,D2,L1,V0,M1} { ! e10 = e13 }.
% 0.73/1.36 (335) {G0,W3,D2,L1,V0,M1} { ! e10 = e14 }.
% 0.73/1.36 (336) {G0,W3,D2,L1,V0,M1} { ! e11 = e12 }.
% 0.73/1.36 (337) {G0,W3,D2,L1,V0,M1} { ! e11 = e13 }.
% 0.73/1.36 (338) {G0,W3,D2,L1,V0,M1} { ! e11 = e14 }.
% 0.73/1.36 (339) {G0,W3,D2,L1,V0,M1} { ! e12 = e13 }.
% 0.73/1.36 (340) {G0,W3,D2,L1,V0,M1} { ! e12 = e14 }.
% 0.73/1.36 (341) {G0,W3,D2,L1,V0,M1} { ! e13 = e14 }.
% 0.73/1.36 (342) {G0,W3,D2,L1,V0,M1} { ! e20 = e21 }.
% 0.73/1.36 (343) {G0,W3,D2,L1,V0,M1} { ! e20 = e22 }.
% 0.73/1.36 (344) {G0,W3,D2,L1,V0,M1} { ! e20 = e23 }.
% 0.73/1.36 (345) {G0,W3,D2,L1,V0,M1} { ! e20 = e24 }.
% 0.73/1.36 (346) {G0,W3,D2,L1,V0,M1} { ! e21 = e22 }.
% 0.73/1.36 (347) {G0,W3,D2,L1,V0,M1} { ! e21 = e23 }.
% 0.73/1.36 (348) {G0,W3,D2,L1,V0,M1} { ! e21 = e24 }.
% 0.73/1.36 (349) {G0,W3,D2,L1,V0,M1} { ! e22 = e23 }.
% 0.73/1.36 (350) {G0,W3,D2,L1,V0,M1} { ! e22 = e24 }.
% 0.73/1.36 (351) {G0,W3,D2,L1,V0,M1} { ! e23 = e24 }.
% 0.73/1.36 (352) {G0,W3,D2,L1,V0,M1} { ! e10 = e20 }.
% 0.73/1.36 (353) {G0,W3,D2,L1,V0,M1} { ! e10 = e21 }.
% 0.73/1.36 (354) {G0,W3,D2,L1,V0,M1} { ! e10 = e22 }.
% 0.73/1.36 (355) {G0,W3,D2,L1,V0,M1} { ! e10 = e23 }.
% 0.73/1.36 (356) {G0,W3,D2,L1,V0,M1} { ! e10 = e24 }.
% 0.73/1.36 (357) {G0,W3,D2,L1,V0,M1} { ! e11 = e20 }.
% 0.73/1.36 (358) {G0,W3,D2,L1,V0,M1} { ! e11 = e21 }.
% 0.73/1.36 (359) {G0,W3,D2,L1,V0,M1} { ! e11 = e22 }.
% 0.73/1.36 (360) {G0,W3,D2,L1,V0,M1} { ! e11 = e23 }.
% 0.73/1.36 (361) {G0,W3,D2,L1,V0,M1} { ! e11 = e24 }.
% 0.73/1.36 (362) {G0,W3,D2,L1,V0,M1} { ! e12 = e20 }.
% 0.73/1.36 (363) {G0,W3,D2,L1,V0,M1} { ! e12 = e21 }.
% 0.73/1.36 (364) {G0,W3,D2,L1,V0,M1} { ! e12 = e22 }.
% 0.73/1.36 (365) {G0,W3,D2,L1,V0,M1} { ! e12 = e23 }.
% 0.73/1.36 (366) {G0,W3,D2,L1,V0,M1} { ! e12 = e24 }.
% 0.73/1.36 (367) {G0,W3,D2,L1,V0,M1} { ! e13 = e20 }.
% 0.73/1.36 (368) {G0,W3,D2,L1,V0,M1} { ! e13 = e21 }.
% 0.73/1.36 (369) {G0,W3,D2,L1,V0,M1} { ! e13 = e22 }.
% 0.73/1.36 (370) {G0,W3,D2,L1,V0,M1} { ! e13 = e23 }.
% 0.73/1.36 (371) {G0,W3,D2,L1,V0,M1} { ! e13 = e24 }.
% 0.73/1.36 (372) {G0,W3,D2,L1,V0,M1} { ! e14 = e20 }.
% 0.73/1.36 (373) {G0,W3,D2,L1,V0,M1} { ! e14 = e21 }.
% 0.73/1.36 (374) {G0,W3,D2,L1,V0,M1} { ! e14 = e22 }.
% 0.73/1.36 (375) {G0,W3,D2,L1,V0,M1} { ! e14 = e23 }.
% 0.73/1.36 (376) {G0,W3,D2,L1,V0,M1} { ! e14 = e24 }.
% 0.73/1.36 (377) {G0,W5,D3,L1,V0,M1} { op1( e10, e10 ) = e13 }.
% 0.73/1.36 (378) {G0,W5,D3,L1,V0,M1} { op1( e10, e11 ) = e12 }.
% 0.73/1.36 (379) {G0,W5,D3,L1,V0,M1} { op1( e10, e12 ) = e10 }.
% 0.73/1.36 (380) {G0,W5,D3,L1,V0,M1} { op1( e10, e13 ) = e11 }.
% 0.73/1.36 (381) {G0,W5,D3,L1,V0,M1} { op1( e10, e14 ) = e14 }.
% 0.73/1.36 (382) {G0,W5,D3,L1,V0,M1} { op1( e11, e10 ) = e10 }.
% 0.73/1.36 (383) {G0,W5,D3,L1,V0,M1} { op1( e11, e11 ) = e14 }.
% 0.73/1.36 (384) {G0,W5,D3,L1,V0,M1} { op1( e11, e12 ) = e11 }.
% 0.73/1.36 (385) {G0,W5,D3,L1,V0,M1} { op1( e11, e13 ) = e12 }.
% 0.73/1.36 (386) {G0,W5,D3,L1,V0,M1} { op1( e11, e14 ) = e13 }.
% 0.73/1.36 (387) {G0,W5,D3,L1,V0,M1} { op1( e12, e10 ) = e11 }.
% 0.73/1.36 (388) {G0,W5,D3,L1,V0,M1} { op1( e12, e11 ) = e13 }.
% 0.73/1.36 (389) {G0,W5,D3,L1,V0,M1} { op1( e12, e12 ) = e12 }.
% 0.73/1.36 (390) {G0,W5,D3,L1,V0,M1} { op1( e12, e13 ) = e14 }.
% 0.73/1.36 (391) {G0,W5,D3,L1,V0,M1} { op1( e12, e14 ) = e10 }.
% 0.73/1.36 (392) {G0,W5,D3,L1,V0,M1} { op1( e13, e10 ) = e14 }.
% 0.73/1.36 (393) {G0,W5,D3,L1,V0,M1} { op1( e13, e11 ) = e11 }.
% 0.73/1.36 (394) {G0,W5,D3,L1,V0,M1} { op1( e13, e12 ) = e13 }.
% 0.73/1.36 (395) {G0,W5,D3,L1,V0,M1} { op1( e13, e13 ) = e10 }.
% 0.73/1.36 (396) {G0,W5,D3,L1,V0,M1} { op1( e13, e14 ) = e12 }.
% 0.73/1.36 (397) {G0,W5,D3,L1,V0,M1} { op1( e14, e10 ) = e12 }.
% 0.73/1.36 (398) {G0,W5,D3,L1,V0,M1} { op1( e14, e11 ) = e10 }.
% 0.73/1.36 (399) {G0,W5,D3,L1,V0,M1} { op1( e14, e12 ) = e14 }.
% 0.73/1.36 (400) {G0,W5,D3,L1,V0,M1} { op1( e14, e13 ) = e13 }.
% 0.73/1.36 (401) {G0,W5,D3,L1,V0,M1} { op1( e14, e14 ) = e11 }.
% 0.73/1.36 (402) {G0,W5,D3,L1,V0,M1} { op2( e20, e20 ) = e24 }.
% 0.73/1.36 (403) {G0,W5,D3,L1,V0,M1} { op2( e20, e21 ) = e22 }.
% 0.73/1.36 (404) {G0,W5,D3,L1,V0,M1} { op2( e20, e22 ) = e20 }.
% 0.73/1.36 (405) {G0,W5,D3,L1,V0,M1} { op2( e20, e23 ) = e21 }.
% 0.73/1.36 (406) {G0,W5,D3,L1,V0,M1} { op2( e20, e24 ) = e23 }.
% 0.73/1.36 (407) {G0,W5,D3,L1,V0,M1} { op2( e21, e20 ) = e20 }.
% 0.73/1.36 (408) {G0,W5,D3,L1,V0,M1} { op2( e21, e21 ) = e21 }.
% 0.73/1.36 (409) {G0,W5,D3,L1,V0,M1} { op2( e21, e22 ) = e22 }.
% 0.73/1.36 (410) {G0,W5,D3,L1,V0,M1} { op2( e21, e23 ) = e23 }.
% 0.73/1.36 (411) {G0,W5,D3,L1,V0,M1} { op2( e21, e24 ) = e24 }.
% 0.73/1.36 (412) {G0,W5,D3,L1,V0,M1} { op2( e22, e20 ) = e21 }.
% 0.73/1.36 (413) {G0,W5,D3,L1,V0,M1} { op2( e22, e21 ) = e24 }.
% 0.73/1.36 (414) {G0,W5,D3,L1,V0,M1} { op2( e22, e22 ) = e23 }.
% 0.73/1.36 (415) {G0,W5,D3,L1,V0,M1} { op2( e22, e23 ) = e20 }.
% 0.73/1.36 (416) {G0,W5,D3,L1,V0,M1} { op2( e22, e24 ) = e22 }.
% 0.73/1.36 (417) {G0,W5,D3,L1,V0,M1} { op2( e23, e20 ) = e23 }.
% 0.73/1.36 (418) {G0,W5,D3,L1,V0,M1} { op2( e23, e21 ) = e20 }.
% 0.73/1.36 (419) {G0,W5,D3,L1,V0,M1} { op2( e23, e22 ) = e24 }.
% 0.73/1.36 (420) {G0,W5,D3,L1,V0,M1} { op2( e23, e23 ) = e22 }.
% 0.73/1.36 (421) {G0,W5,D3,L1,V0,M1} { op2( e23, e24 ) = e21 }.
% 0.73/1.36 (422) {G0,W5,D3,L1,V0,M1} { op2( e24, e20 ) = e22 }.
% 0.73/1.36 (423) {G0,W5,D3,L1,V0,M1} { op2( e24, e21 ) = e23 }.
% 0.73/1.36 (424) {G0,W5,D3,L1,V0,M1} { op2( e24, e22 ) = e21 }.
% 0.73/1.36 (425) {G0,W5,D3,L1,V0,M1} { op2( e24, e23 ) = e24 }.
% 0.73/1.36 (426) {G0,W5,D3,L1,V0,M1} { op2( e24, e24 ) = e20 }.
% 0.73/1.36 (427) {G0,W20,D3,L5,V0,M5} { h( e10 ) = e20, h( e10 ) = e21, h( e10 ) =
% 0.73/1.36 e22, h( e10 ) = e23, h( e10 ) = e24 }.
% 0.73/1.36 (428) {G0,W20,D3,L5,V0,M5} { h( e11 ) = e20, h( e11 ) = e21, h( e11 ) =
% 0.73/1.36 e22, h( e11 ) = e23, h( e11 ) = e24 }.
% 0.73/1.36 (429) {G0,W20,D3,L5,V0,M5} { h( e12 ) = e20, h( e12 ) = e21, h( e12 ) =
% 0.73/1.36 e22, h( e12 ) = e23, h( e12 ) = e24 }.
% 0.73/1.36 (430) {G0,W20,D3,L5,V0,M5} { h( e13 ) = e20, h( e13 ) = e21, h( e13 ) =
% 0.73/1.36 e22, h( e13 ) = e23, h( e13 ) = e24 }.
% 0.73/1.36 (431) {G0,W20,D3,L5,V0,M5} { h( e14 ) = e20, h( e14 ) = e21, h( e14 ) =
% 0.73/1.36 e22, h( e14 ) = e23, h( e14 ) = e24 }.
% 0.73/1.36 (432) {G0,W20,D3,L5,V0,M5} { j( e20 ) = e10, j( e20 ) = e11, j( e20 ) =
% 0.73/1.36 e12, j( e20 ) = e13, j( e20 ) = e14 }.
% 0.73/1.36 (433) {G0,W20,D3,L5,V0,M5} { j( e21 ) = e10, j( e21 ) = e11, j( e21 ) =
% 0.73/1.36 e12, j( e21 ) = e13, j( e21 ) = e14 }.
% 0.73/1.36 (434) {G0,W20,D3,L5,V0,M5} { j( e22 ) = e10, j( e22 ) = e11, j( e22 ) =
% 0.73/1.36 e12, j( e22 ) = e13, j( e22 ) = e14 }.
% 0.73/1.36 (435) {G0,W20,D3,L5,V0,M5} { j( e23 ) = e10, j( e23 ) = e11, j( e23 ) =
% 0.73/1.36 e12, j( e23 ) = e13, j( e23 ) = e14 }.
% 0.73/1.36 (436) {G0,W20,D3,L5,V0,M5} { j( e24 ) = e10, j( e24 ) = e11, j( e24 ) =
% 0.73/1.36 e12, j( e24 ) = e13, j( e24 ) = e14 }.
% 0.73/1.36 (437) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e10 ) ) = op2( h( e10 ), h( e10
% 0.73/1.36 ) ) }.
% 0.73/1.36 (438) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e11 ) ) = op2( h( e10 ), h( e11
% 0.73/1.36 ) ) }.
% 0.73/1.36 (439) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e12 ) ) = op2( h( e10 ), h( e12
% 0.73/1.36 ) ) }.
% 0.73/1.36 (440) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e13 ) ) = op2( h( e10 ), h( e13
% 0.73/1.36 ) ) }.
% 0.73/1.36 (441) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e14 ) ) = op2( h( e10 ), h( e14
% 0.73/1.36 ) ) }.
% 0.73/1.36 (442) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e10 ) ) = op2( h( e11 ), h( e10
% 0.73/1.36 ) ) }.
% 0.73/1.36 (443) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e11 ) ) = op2( h( e11 ), h( e11
% 0.73/1.36 ) ) }.
% 0.73/1.36 (444) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e12 ) ) = op2( h( e11 ), h( e12
% 0.73/1.36 ) ) }.
% 0.73/1.36 (445) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e13 ) ) = op2( h( e11 ), h( e13
% 0.73/1.36 ) ) }.
% 0.73/1.36 (446) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e14 ) ) = op2( h( e11 ), h( e14
% 0.73/1.36 ) ) }.
% 0.73/1.36 (447) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e10 ) ) = op2( h( e12 ), h( e10
% 0.73/1.36 ) ) }.
% 0.73/1.36 (448) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e11 ) ) = op2( h( e12 ), h( e11
% 0.73/1.36 ) ) }.
% 0.73/1.36 (449) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e12 ) ) = op2( h( e12 ), h( e12
% 0.73/1.36 ) ) }.
% 0.73/1.36 (450) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e13 ) ) = op2( h( e12 ), h( e13
% 0.73/1.36 ) ) }.
% 0.73/1.36 (451) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e14 ) ) = op2( h( e12 ), h( e14
% 0.73/1.36 ) ) }.
% 0.73/1.36 (452) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e10 ) ) = op2( h( e13 ), h( e10
% 0.73/1.36 ) ) }.
% 0.73/1.36 (453) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e11 ) ) = op2( h( e13 ), h( e11
% 0.73/1.36 ) ) }.
% 0.73/1.36 (454) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e12 ) ) = op2( h( e13 ), h( e12
% 0.73/1.36 ) ) }.
% 0.73/1.36 (455) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e13 ) ) = op2( h( e13 ), h( e13
% 0.73/1.36 ) ) }.
% 0.73/1.36 (456) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e14 ) ) = op2( h( e13 ), h( e14
% 0.73/1.36 ) ) }.
% 0.73/1.36 (457) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e10 ) ) = op2( h( e14 ), h( e10
% 0.73/1.36 ) ) }.
% 0.73/1.36 (458) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e11 ) ) = op2( h( e14 ), h( e11
% 0.73/1.36 ) ) }.
% 0.73/1.36 (459) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e12 ) ) = op2( h( e14 ), h( e12
% 0.73/1.36 ) ) }.
% 0.73/1.36 (460) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e13 ) ) = op2( h( e14 ), h( e13
% 0.73/1.36 ) ) }.
% 0.73/1.36 (461) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e14 ) ) = op2( h( e14 ), h( e14
% 0.73/1.36 ) ) }.
% 0.73/1.36 (462) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e20 ) ) = op1( j( e20 ), j( e20
% 0.73/1.36 ) ) }.
% 0.73/1.36 (463) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e21 ) ) = op1( j( e20 ), j( e21
% 0.73/1.36 ) ) }.
% 0.73/1.36 (464) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e22 ) ) = op1( j( e20 ), j( e22
% 0.73/1.36 ) ) }.
% 0.73/1.36 (465) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e23 ) ) = op1( j( e20 ), j( e23
% 0.73/1.36 ) ) }.
% 0.73/1.36 (466) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e24 ) ) = op1( j( e20 ), j( e24
% 0.73/1.36 ) ) }.
% 0.73/1.36 (467) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e20 ) ) = op1( j( e21 ), j( e20
% 0.73/1.36 ) ) }.
% 0.73/1.36 (468) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e21 ) ) = op1( j( e21 ), j( e21
% 0.73/1.36 ) ) }.
% 0.73/1.36 (469) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e22 ) ) = op1( j( e21 ), j( e22
% 0.73/1.36 ) ) }.
% 0.73/1.36 (470) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e23 ) ) = op1( j( e21 ), j( e23
% 0.73/1.36 ) ) }.
% 0.73/1.36 (471) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e24 ) ) = op1( j( e21 ), j( e24
% 0.73/1.36 ) ) }.
% 0.73/1.36 (472) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e20 ) ) = op1( j( e22 ), j( e20
% 0.73/1.36 ) ) }.
% 0.73/1.36 (473) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e21 ) ) = op1( j( e22 ), j( e21
% 0.73/1.36 ) ) }.
% 0.73/1.36 (474) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e22 ) ) = op1( j( e22 ), j( e22
% 0.73/1.36 ) ) }.
% 0.73/1.36 (475) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e23 ) ) = op1( j( e22 ), j( e23
% 0.73/1.36 ) ) }.
% 0.73/1.36 (476) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e24 ) ) = op1( j( e22 ), j( e24
% 0.73/1.36 ) ) }.
% 0.73/1.36 (477) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e20 ) ) = op1( j( e23 ), j( e20
% 0.73/1.36 ) ) }.
% 0.73/1.36 (478) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e21 ) ) = op1( j( e23 ), j( e21
% 0.73/1.36 ) ) }.
% 0.73/1.36 (479) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e22 ) ) = op1( j( e23 ), j( e22
% 0.73/1.36 ) ) }.
% 0.73/1.36 (480) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e23 ) ) = op1( j( e23 ), j( e23
% 0.73/1.36 ) ) }.
% 0.73/1.36 (481) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e24 ) ) = op1( j( e23 ), j( e24
% 0.73/1.36 ) ) }.
% 0.73/1.36 (482) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e20 ) ) = op1( j( e24 ), j( e20
% 0.73/1.36 ) ) }.
% 0.73/1.36 (483) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e21 ) ) = op1( j( e24 ), j( e21
% 0.73/1.36 ) ) }.
% 0.73/1.36 (484) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e22 ) ) = op1( j( e24 ), j( e22
% 0.73/1.36 ) ) }.
% 0.73/1.36 (485) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e23 ) ) = op1( j( e24 ), j( e23
% 0.73/1.36 ) ) }.
% 0.73/1.36 (486) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e24 ) ) = op1( j( e24 ), j( e24
% 0.73/1.36 ) ) }.
% 0.73/1.36 (487) {G0,W5,D4,L1,V0,M1} { h( j( e20 ) ) = e20 }.
% 0.73/1.36 (488) {G0,W5,D4,L1,V0,M1} { h( j( e21 ) ) = e21 }.
% 0.73/1.36 (489) {G0,W5,D4,L1,V0,M1} { h( j( e22 ) ) = e22 }.
% 0.73/1.36 (490) {G0,W5,D4,L1,V0,M1} { h( j( e23 ) ) = e23 }.
% 0.73/1.36 (491) {G0,W5,D4,L1,V0,M1} { h( j( e24 ) ) = e24 }.
% 0.73/1.36 (492) {G0,W5,D4,L1,V0,M1} { j( h( e10 ) ) = e10 }.
% 0.73/1.36 (493) {G0,W5,D4,L1,V0,M1} { j( h( e11 ) ) = e11 }.
% 0.73/1.36 (494) {G0,W5,D4,L1,V0,M1} { j( h( e12 ) ) = e12 }.
% 0.73/1.36 (495) {G0,W5,D4,L1,V0,M1} { j( h( e13 ) ) = e13 }.
% 0.73/1.36 (496) {G0,W5,D4,L1,V0,M1} { j( h( e14 ) ) = e14 }.
% 0.73/1.36
% 0.73/1.36
% 0.73/1.36 Total Proof:
% 0.73/1.36
% 0.73/1.36 eqswap: (505) {G0,W3,D2,L1,V0,M1} { ! e14 = e12 }.
% 0.73/1.36 parent0[0]: (340) {G0,W3,D2,L1,V0,M1} { ! e12 = e14 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (8) {G0,W3,D2,L1,V0,M1} I { ! e14 ==> e12 }.
% 0.73/1.36 parent0: (505) {G0,W3,D2,L1,V0,M1} { ! e14 = e12 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 eqswap: (517) {G0,W3,D2,L1,V0,M1} { ! e22 = e20 }.
% 0.73/1.36 parent0[0]: (343) {G0,W3,D2,L1,V0,M1} { ! e20 = e22 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (11) {G0,W3,D2,L1,V0,M1} I { ! e22 ==> e20 }.
% 0.73/1.36 parent0: (517) {G0,W3,D2,L1,V0,M1} { ! e22 = e20 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 eqswap: (530) {G0,W3,D2,L1,V0,M1} { ! e23 = e20 }.
% 0.73/1.36 parent0[0]: (344) {G0,W3,D2,L1,V0,M1} { ! e20 = e23 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (12) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e20 }.
% 0.73/1.36 parent0: (530) {G0,W3,D2,L1,V0,M1} { ! e23 = e20 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 eqswap: (544) {G0,W3,D2,L1,V0,M1} { ! e24 = e20 }.
% 0.73/1.36 parent0[0]: (345) {G0,W3,D2,L1,V0,M1} { ! e20 = e24 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (13) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e20 }.
% 0.73/1.36 parent0: (544) {G0,W3,D2,L1,V0,M1} { ! e24 = e20 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 eqswap: (562) {G0,W3,D2,L1,V0,M1} { ! e23 = e22 }.
% 0.73/1.36 parent0[0]: (349) {G0,W3,D2,L1,V0,M1} { ! e22 = e23 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (17) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e22 }.
% 0.73/1.36 parent0: (562) {G0,W3,D2,L1,V0,M1} { ! e23 = e22 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 eqswap: (581) {G0,W3,D2,L1,V0,M1} { ! e24 = e22 }.
% 0.73/1.36 parent0[0]: (350) {G0,W3,D2,L1,V0,M1} { ! e22 = e24 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (18) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e22 }.
% 0.73/1.36 parent0: (581) {G0,W3,D2,L1,V0,M1} { ! e24 = e22 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (57) {G0,W5,D3,L1,V0,M1} I { op1( e12, e12 ) ==> e12 }.
% 0.73/1.36 parent0: (389) {G0,W5,D3,L1,V0,M1} { op1( e12, e12 ) = e12 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (67) {G0,W5,D3,L1,V0,M1} I { op1( e14, e12 ) ==> e14 }.
% 0.73/1.36 parent0: (399) {G0,W5,D3,L1,V0,M1} { op1( e14, e12 ) = e14 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (70) {G0,W5,D3,L1,V0,M1} I { op2( e20, e20 ) ==> e24 }.
% 0.73/1.36 parent0: (402) {G0,W5,D3,L1,V0,M1} { op2( e20, e20 ) = e24 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (71) {G0,W5,D3,L1,V0,M1} I { op2( e20, e21 ) ==> e22 }.
% 0.73/1.36 parent0: (403) {G0,W5,D3,L1,V0,M1} { op2( e20, e21 ) = e22 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (81) {G0,W5,D3,L1,V0,M1} I { op2( e22, e21 ) ==> e24 }.
% 1.62/2.02 parent0: (413) {G0,W5,D3,L1,V0,M1} { op2( e22, e21 ) = e24 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 permutation0:
% 1.62/2.02 0 ==> 0
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 subsumption: (82) {G0,W5,D3,L1,V0,M1} I { op2( e22, e22 ) ==> e23 }.
% 1.62/2.02 parent0: (414) {G0,W5,D3,L1,V0,M1} { op2( e22, e22 ) = e23 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 permutation0:
% 1.62/2.02 0 ==> 0
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 *** allocated 50625 integers for clauses
% 1.62/2.02 *** allocated 15000 integers for termspace/termends
% 1.62/2.02 subsumption: (86) {G0,W5,D3,L1,V0,M1} I { op2( e23, e21 ) ==> e20 }.
% 1.62/2.02 parent0: (418) {G0,W5,D3,L1,V0,M1} { op2( e23, e21 ) = e20 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 permutation0:
% 1.62/2.02 0 ==> 0
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 subsumption: (88) {G0,W5,D3,L1,V0,M1} I { op2( e23, e23 ) ==> e22 }.
% 1.62/2.02 parent0: (420) {G0,W5,D3,L1,V0,M1} { op2( e23, e23 ) = e22 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 permutation0:
% 1.62/2.02 0 ==> 0
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 subsumption: (91) {G0,W5,D3,L1,V0,M1} I { op2( e24, e21 ) ==> e23 }.
% 1.62/2.02 parent0: (423) {G0,W5,D3,L1,V0,M1} { op2( e24, e21 ) = e23 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 permutation0:
% 1.62/2.02 0 ==> 0
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 subsumption: (94) {G0,W5,D3,L1,V0,M1} I { op2( e24, e24 ) ==> e20 }.
% 1.62/2.02 parent0: (426) {G0,W5,D3,L1,V0,M1} { op2( e24, e24 ) = e20 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 permutation0:
% 1.62/2.02 0 ==> 0
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 subsumption: (97) {G0,W20,D3,L5,V0,M5} I { h( e12 ) ==> e20, h( e12 ) ==>
% 1.62/2.02 e21, h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 1.62/2.02 parent0: (429) {G0,W20,D3,L5,V0,M5} { h( e12 ) = e20, h( e12 ) = e21, h(
% 1.62/2.02 e12 ) = e22, h( e12 ) = e23, h( e12 ) = e24 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 permutation0:
% 1.62/2.02 0 ==> 0
% 1.62/2.02 1 ==> 1
% 1.62/2.02 2 ==> 2
% 1.62/2.02 3 ==> 3
% 1.62/2.02 4 ==> 4
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 *** allocated 22500 integers for termspace/termends
% 1.62/2.02 *** allocated 75937 integers for clauses
% 1.62/2.02 subsumption: (99) {G0,W20,D3,L5,V0,M5} I { h( e14 ) ==> e20, h( e14 ) ==>
% 1.62/2.02 e21, h( e14 ) ==> e22, h( e14 ) ==> e23, h( e14 ) ==> e24 }.
% 1.62/2.02 parent0: (431) {G0,W20,D3,L5,V0,M5} { h( e14 ) = e20, h( e14 ) = e21, h(
% 1.62/2.02 e14 ) = e22, h( e14 ) = e23, h( e14 ) = e24 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 permutation0:
% 1.62/2.02 0 ==> 0
% 1.62/2.02 1 ==> 1
% 1.62/2.02 2 ==> 2
% 1.62/2.02 3 ==> 3
% 1.62/2.02 4 ==> 4
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 *** allocated 33750 integers for termspace/termends
% 1.62/2.02 paramod: (2355) {G1,W8,D4,L1,V0,M1} { h( e12 ) = op2( h( e12 ), h( e12 ) )
% 1.62/2.02 }.
% 1.62/2.02 parent0[0]: (57) {G0,W5,D3,L1,V0,M1} I { op1( e12, e12 ) ==> e12 }.
% 1.62/2.02 parent1[0; 2]: (449) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e12 ) ) = op2( h
% 1.62/2.02 ( e12 ), h( e12 ) ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 substitution1:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 eqswap: (2356) {G1,W8,D4,L1,V0,M1} { op2( h( e12 ), h( e12 ) ) = h( e12 )
% 1.62/2.02 }.
% 1.62/2.02 parent0[0]: (2355) {G1,W8,D4,L1,V0,M1} { h( e12 ) = op2( h( e12 ), h( e12
% 1.62/2.02 ) ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 subsumption: (117) {G1,W8,D4,L1,V0,M1} I;d(57) { op2( h( e12 ), h( e12 ) )
% 1.62/2.02 ==> h( e12 ) }.
% 1.62/2.02 parent0: (2356) {G1,W8,D4,L1,V0,M1} { op2( h( e12 ), h( e12 ) ) = h( e12 )
% 1.62/2.02 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 permutation0:
% 1.62/2.02 0 ==> 0
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 paramod: (2915) {G1,W8,D4,L1,V0,M1} { h( e14 ) = op2( h( e14 ), h( e12 ) )
% 1.62/2.02 }.
% 1.62/2.02 parent0[0]: (67) {G0,W5,D3,L1,V0,M1} I { op1( e14, e12 ) ==> e14 }.
% 1.62/2.02 parent1[0; 2]: (459) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e12 ) ) = op2( h
% 1.62/2.02 ( e14 ), h( e12 ) ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 substitution1:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 eqswap: (2916) {G1,W8,D4,L1,V0,M1} { op2( h( e14 ), h( e12 ) ) = h( e14 )
% 1.62/2.02 }.
% 1.62/2.02 parent0[0]: (2915) {G1,W8,D4,L1,V0,M1} { h( e14 ) = op2( h( e14 ), h( e12
% 1.62/2.02 ) ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 subsumption: (127) {G1,W8,D4,L1,V0,M1} I;d(67) { op2( h( e14 ), h( e12 ) )
% 1.62/2.02 ==> h( e14 ) }.
% 1.62/2.02 parent0: (2916) {G1,W8,D4,L1,V0,M1} { op2( h( e14 ), h( e12 ) ) = h( e14 )
% 1.62/2.02 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 permutation0:
% 1.62/2.02 0 ==> 0
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 *** allocated 113905 integers for clauses
% 1.62/2.02 *** allocated 50625 integers for termspace/termends
% 1.62/2.02 subsumption: (162) {G0,W5,D4,L1,V0,M1} I { j( h( e12 ) ) ==> e12 }.
% 1.62/2.02 parent0: (494) {G0,W5,D4,L1,V0,M1} { j( h( e12 ) ) = e12 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 permutation0:
% 1.62/2.02 0 ==> 0
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 subsumption: (164) {G0,W5,D4,L1,V0,M1} I { j( h( e14 ) ) ==> e14 }.
% 1.62/2.02 parent0: (496) {G0,W5,D4,L1,V0,M1} { j( h( e14 ) ) = e14 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 permutation0:
% 1.62/2.02 0 ==> 0
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 *** allocated 75937 integers for termspace/termends
% 1.62/2.02 *** allocated 170857 integers for clauses
% 1.62/2.02 *** allocated 113905 integers for termspace/termends
% 1.62/2.02 eqswap: (3849) {G0,W20,D3,L5,V0,M5} { e24 ==> h( e12 ), h( e12 ) ==> e20,
% 1.62/2.02 h( e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 1.62/2.02 parent0[4]: (97) {G0,W20,D3,L5,V0,M5} I { h( e12 ) ==> e20, h( e12 ) ==>
% 1.62/2.02 e21, h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 eqswap: (3853) {G0,W20,D3,L5,V0,M5} { e23 ==> h( e12 ), e24 ==> h( e12 ),
% 1.62/2.02 h( e12 ) ==> e20, h( e12 ) ==> e21, h( e12 ) ==> e22 }.
% 1.62/2.02 parent0[4]: (3849) {G0,W20,D3,L5,V0,M5} { e24 ==> h( e12 ), h( e12 ) ==>
% 1.62/2.02 e20, h( e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 eqswap: (3856) {G0,W20,D3,L5,V0,M5} { e22 ==> h( e12 ), e23 ==> h( e12 ),
% 1.62/2.02 e24 ==> h( e12 ), h( e12 ) ==> e20, h( e12 ) ==> e21 }.
% 1.62/2.02 parent0[4]: (3853) {G0,W20,D3,L5,V0,M5} { e23 ==> h( e12 ), e24 ==> h( e12
% 1.62/2.02 ), h( e12 ) ==> e20, h( e12 ) ==> e21, h( e12 ) ==> e22 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 eqswap: (3859) {G0,W20,D3,L5,V0,M5} { e21 ==> h( e12 ), e22 ==> h( e12 ),
% 1.62/2.02 e23 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e20 }.
% 1.62/2.02 parent0[4]: (3856) {G0,W20,D3,L5,V0,M5} { e22 ==> h( e12 ), e23 ==> h( e12
% 1.62/2.02 ), e24 ==> h( e12 ), h( e12 ) ==> e20, h( e12 ) ==> e21 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 eqswap: (3860) {G0,W20,D3,L5,V0,M5} { h( e12 ) ==> e23, e21 ==> h( e12 ),
% 1.62/2.02 e22 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e20 }.
% 1.62/2.02 parent0[2]: (3859) {G0,W20,D3,L5,V0,M5} { e21 ==> h( e12 ), e22 ==> h( e12
% 1.62/2.02 ), e23 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e20 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 eqswap: (3876) {G1,W8,D4,L1,V0,M1} { h( e12 ) ==> op2( h( e12 ), h( e12 )
% 1.62/2.02 ) }.
% 1.62/2.02 parent0[0]: (117) {G1,W8,D4,L1,V0,M1} I;d(57) { op2( h( e12 ), h( e12 ) )
% 1.62/2.02 ==> h( e12 ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 paramod: (21274) {G1,W23,D4,L5,V0,M5} { h( e12 ) ==> op2( h( e12 ), e20 )
% 1.62/2.02 , h( e12 ) ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 )
% 1.62/2.02 }.
% 1.62/2.02 parent0[4]: (3860) {G0,W20,D3,L5,V0,M5} { h( e12 ) ==> e23, e21 ==> h( e12
% 1.62/2.02 ), e22 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e20 }.
% 1.62/2.02 parent1[0; 6]: (3876) {G1,W8,D4,L1,V0,M1} { h( e12 ) ==> op2( h( e12 ), h
% 1.62/2.02 ( e12 ) ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 substitution1:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 paramod: (21286) {G1,W38,D4,L9,V0,M9} { e24 ==> e20, h( e12 ) ==> e23, e21
% 1.62/2.02 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> op2( h(
% 1.62/2.02 e12 ), e20 ), h( e12 ) ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ) }.
% 1.62/2.02 parent0[4]: (3860) {G0,W20,D3,L5,V0,M5} { h( e12 ) ==> e23, e21 ==> h( e12
% 1.62/2.02 ), e22 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e20 }.
% 1.62/2.02 parent1[4; 2]: (21274) {G1,W23,D4,L5,V0,M5} { h( e12 ) ==> op2( h( e12 ),
% 1.62/2.02 e20 ), h( e12 ) ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h(
% 1.62/2.02 e12 ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 substitution1:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 paramod: (21298) {G1,W53,D3,L13,V0,M13} { h( e12 ) ==> op2( e20, e20 ), h
% 1.62/2.02 ( e12 ) ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ),
% 1.62/2.02 e24 ==> e20, h( e12 ) ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24
% 1.62/2.02 ==> h( e12 ), h( e12 ) ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ) }.
% 1.62/2.02 parent0[4]: (3860) {G0,W20,D3,L5,V0,M5} { h( e12 ) ==> e23, e21 ==> h( e12
% 1.62/2.02 ), e22 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e20 }.
% 1.62/2.02 parent1[5; 4]: (21286) {G1,W38,D4,L9,V0,M9} { e24 ==> e20, h( e12 ) ==>
% 1.62/2.02 e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==>
% 1.62/2.02 op2( h( e12 ), e20 ), h( e12 ) ==> e23, e21 ==> h( e12 ), e22 ==> h( e12
% 1.62/2.02 ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 substitution1:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 paramod: (21801) {G1,W51,D3,L13,V0,M13} { h( e12 ) ==> e24, h( e12 ) ==>
% 1.62/2.02 e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e24 ==> e20, h
% 1.62/2.02 ( e12 ) ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), h
% 1.62/2.02 ( e12 ) ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ) }.
% 1.62/2.02 parent0[0]: (70) {G0,W5,D3,L1,V0,M1} I { op2( e20, e20 ) ==> e24 }.
% 1.62/2.02 parent1[0; 3]: (21298) {G1,W53,D3,L13,V0,M13} { h( e12 ) ==> op2( e20, e20
% 1.62/2.02 ), h( e12 ) ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12
% 1.62/2.02 ), e24 ==> e20, h( e12 ) ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ),
% 1.62/2.02 e24 ==> h( e12 ), h( e12 ) ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 )
% 1.62/2.02 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 substitution1:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 factor: (21802) {G1,W47,D3,L12,V0,M12} { h( e12 ) ==> e24, h( e12 ) ==>
% 1.62/2.02 e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e24 ==> e20,
% 1.62/2.02 e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e23,
% 1.62/2.02 e21 ==> h( e12 ), e22 ==> h( e12 ) }.
% 1.62/2.02 parent0[1, 6]: (21801) {G1,W51,D3,L13,V0,M13} { h( e12 ) ==> e24, h( e12 )
% 1.62/2.02 ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e24 ==>
% 1.62/2.02 e20, h( e12 ) ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12
% 1.62/2.02 ), h( e12 ) ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 factor: (21803) {G1,W43,D3,L11,V0,M11} { h( e12 ) ==> e24, h( e12 ) ==>
% 1.62/2.02 e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e24 ==> e20,
% 1.62/2.02 e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e21 ==> h( e12 ),
% 1.62/2.02 e22 ==> h( e12 ) }.
% 1.62/2.02 parent0[1, 9]: (21802) {G1,W47,D3,L12,V0,M12} { h( e12 ) ==> e24, h( e12 )
% 1.62/2.02 ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e24 ==>
% 1.62/2.02 e20, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==>
% 1.62/2.02 e23, e21 ==> h( e12 ), e22 ==> h( e12 ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 factor: (21804) {G1,W39,D3,L10,V0,M10} { h( e12 ) ==> e24, h( e12 ) ==>
% 1.62/2.02 e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e24 ==> e20,
% 1.62/2.02 e22 ==> h( e12 ), e24 ==> h( e12 ), e21 ==> h( e12 ), e22 ==> h( e12 )
% 1.62/2.02 }.
% 1.62/2.02 parent0[2, 6]: (21803) {G1,W43,D3,L11,V0,M11} { h( e12 ) ==> e24, h( e12 )
% 1.62/2.02 ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e24 ==>
% 1.62/2.02 e20, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e21 ==> h( e12
% 1.62/2.02 ), e22 ==> h( e12 ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 factor: (21805) {G1,W35,D3,L9,V0,M9} { h( e12 ) ==> e24, h( e12 ) ==> e23
% 1.62/2.02 , e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e24 ==> e20, e22
% 1.62/2.02 ==> h( e12 ), e24 ==> h( e12 ), e22 ==> h( e12 ) }.
% 1.62/2.02 parent0[2, 8]: (21804) {G1,W39,D3,L10,V0,M10} { h( e12 ) ==> e24, h( e12 )
% 1.62/2.02 ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e24 ==>
% 1.62/2.02 e20, e22 ==> h( e12 ), e24 ==> h( e12 ), e21 ==> h( e12 ), e22 ==> h( e12
% 1.62/2.02 ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 factor: (21806) {G1,W31,D3,L8,V0,M8} { h( e12 ) ==> e24, h( e12 ) ==> e23
% 1.62/2.02 , e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e24 ==> e20, e24
% 1.62/2.02 ==> h( e12 ), e22 ==> h( e12 ) }.
% 1.62/2.02 parent0[3, 6]: (21805) {G1,W35,D3,L9,V0,M9} { h( e12 ) ==> e24, h( e12 )
% 1.62/2.02 ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e24 ==>
% 1.62/2.02 e20, e22 ==> h( e12 ), e24 ==> h( e12 ), e22 ==> h( e12 ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 factor: (21807) {G1,W27,D3,L7,V0,M7} { h( e12 ) ==> e24, h( e12 ) ==> e23
% 1.62/2.02 , e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e24 ==> e20, e24
% 1.62/2.02 ==> h( e12 ) }.
% 1.62/2.02 parent0[3, 7]: (21806) {G1,W31,D3,L8,V0,M8} { h( e12 ) ==> e24, h( e12 )
% 1.62/2.02 ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e24 ==>
% 1.62/2.02 e20, e24 ==> h( e12 ), e22 ==> h( e12 ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 factor: (21808) {G1,W23,D3,L6,V0,M6} { h( e12 ) ==> e24, h( e12 ) ==> e23
% 1.62/2.02 , e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e24 ==> e20 }.
% 1.62/2.02 parent0[4, 6]: (21807) {G1,W27,D3,L7,V0,M7} { h( e12 ) ==> e24, h( e12 )
% 1.62/2.02 ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e24 ==>
% 1.62/2.02 e20, e24 ==> h( e12 ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 resolution: (21809) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e24, h( e12 ) ==>
% 1.62/2.02 e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ) }.
% 1.62/2.02 parent0[0]: (13) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e20 }.
% 1.62/2.02 parent1[5]: (21808) {G1,W23,D3,L6,V0,M6} { h( e12 ) ==> e24, h( e12 ) ==>
% 1.62/2.02 e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e24 ==> e20
% 1.62/2.02 }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02 substitution1:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 eqswap: (21814) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e24, h( e12 ) ==> e24
% 1.62/2.02 , h( e12 ) ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ) }.
% 1.62/2.02 parent0[4]: (21809) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e24, h( e12 ) ==>
% 1.62/2.02 e23, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 eqswap: (21817) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e22, h( e12 ) ==> e24
% 1.62/2.02 , h( e12 ) ==> e24, h( e12 ) ==> e23, e21 ==> h( e12 ) }.
% 1.62/2.02 parent0[4]: (21814) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e24, h( e12 ) ==>
% 1.62/2.02 e24, h( e12 ) ==> e23, e21 ==> h( e12 ), e22 ==> h( e12 ) }.
% 1.62/2.02 substitution0:
% 1.62/2.02 end
% 1.62/2.02
% 1.62/2.02 eqswap: (21819) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e21, h( e12 ) ==> e22
% 1.93/2.35 , h( e12 ) ==> e24, h( e12 ) ==> e24, h( e12 ) ==> e23 }.
% 1.93/2.35 parent0[4]: (21817) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e22, h( e12 ) ==>
% 1.93/2.35 e24, h( e12 ) ==> e24, h( e12 ) ==> e23, e21 ==> h( e12 ) }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 factor: (21842) {G1,W16,D3,L4,V0,M4} { h( e12 ) ==> e21, h( e12 ) ==> e22
% 1.93/2.35 , h( e12 ) ==> e24, h( e12 ) ==> e23 }.
% 1.93/2.35 parent0[2, 3]: (21819) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e21, h( e12 )
% 1.93/2.35 ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e24, h( e12 ) ==> e23 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 subsumption: (220) {G2,W16,D3,L4,V0,M4} P(97,117);d(70);r(13) { h( e12 )
% 1.93/2.35 ==> e21, h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 1.93/2.35 parent0: (21842) {G1,W16,D3,L4,V0,M4} { h( e12 ) ==> e21, h( e12 ) ==> e22
% 1.93/2.35 , h( e12 ) ==> e24, h( e12 ) ==> e23 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35 permutation0:
% 1.93/2.35 0 ==> 0
% 1.93/2.35 1 ==> 1
% 1.93/2.35 2 ==> 3
% 1.93/2.35 3 ==> 2
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 *** allocated 170857 integers for termspace/termends
% 1.93/2.35 *** allocated 15000 integers for justifications
% 1.93/2.35 eqswap: (21849) {G0,W20,D3,L5,V0,M5} { e24 ==> h( e12 ), h( e12 ) ==> e20
% 1.93/2.35 , h( e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 1.93/2.35 parent0[4]: (97) {G0,W20,D3,L5,V0,M5} I { h( e12 ) ==> e20, h( e12 ) ==>
% 1.93/2.35 e21, h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 eqswap: (21850) {G0,W20,D3,L5,V0,M5} { e20 ==> h( e12 ), e24 ==> h( e12 )
% 1.93/2.35 , h( e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 1.93/2.35 parent0[1]: (21849) {G0,W20,D3,L5,V0,M5} { e24 ==> h( e12 ), h( e12 ) ==>
% 1.93/2.35 e20, h( e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 eqswap: (21876) {G1,W8,D4,L1,V0,M1} { h( e12 ) ==> op2( h( e12 ), h( e12 )
% 1.93/2.35 ) }.
% 1.93/2.35 parent0[0]: (117) {G1,W8,D4,L1,V0,M1} I;d(57) { op2( h( e12 ), h( e12 ) )
% 1.93/2.35 ==> h( e12 ) }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 eqswap: (21878) {G2,W16,D3,L4,V0,M4} { e21 ==> h( e12 ), h( e12 ) ==> e22
% 1.93/2.35 , h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 1.93/2.35 parent0[0]: (220) {G2,W16,D3,L4,V0,M4} P(97,117);d(70);r(13) { h( e12 ) ==>
% 1.93/2.35 e21, h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 eqswap: (21893) {G0,W3,D2,L1,V0,M1} { ! e20 ==> e23 }.
% 1.93/2.35 parent0[0]: (12) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e20 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 paramod: (30214) {G1,W23,D4,L5,V0,M5} { h( e12 ) ==> op2( h( e12 ), e23 )
% 1.93/2.35 , e20 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, h( e12 ) ==> e22
% 1.93/2.35 }.
% 1.93/2.35 parent0[4]: (21850) {G0,W20,D3,L5,V0,M5} { e20 ==> h( e12 ), e24 ==> h(
% 1.93/2.35 e12 ), h( e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 1.93/2.35 parent1[0; 6]: (21876) {G1,W8,D4,L1,V0,M1} { h( e12 ) ==> op2( h( e12 ), h
% 1.93/2.35 ( e12 ) ) }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35 substitution1:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 paramod: (30232) {G1,W38,D4,L9,V0,M9} { e23 ==> e22, e20 ==> h( e12 ), e24
% 1.93/2.35 ==> h( e12 ), h( e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==> op2( h(
% 1.93/2.35 e12 ), e23 ), e20 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21 }.
% 1.93/2.35 parent0[4]: (21850) {G0,W20,D3,L5,V0,M5} { e20 ==> h( e12 ), e24 ==> h(
% 1.93/2.35 e12 ), h( e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 1.93/2.35 parent1[4; 1]: (30214) {G1,W23,D4,L5,V0,M5} { h( e12 ) ==> op2( h( e12 ),
% 1.93/2.35 e23 ), e20 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, h( e12 ) ==>
% 1.93/2.35 e22 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35 substitution1:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 paramod: (30250) {G1,W53,D3,L13,V0,M13} { h( e12 ) ==> op2( e23, e23 ),
% 1.93/2.35 e20 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, h( e12 ) ==> e22,
% 1.93/2.35 e23 ==> e22, e20 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, h( e12
% 1.93/2.35 ) ==> e22, e20 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21 }.
% 1.93/2.35 parent0[4]: (21850) {G0,W20,D3,L5,V0,M5} { e20 ==> h( e12 ), e24 ==> h(
% 1.93/2.35 e12 ), h( e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 1.93/2.35 parent1[5; 4]: (30232) {G1,W38,D4,L9,V0,M9} { e23 ==> e22, e20 ==> h( e12
% 1.93/2.35 ), e24 ==> h( e12 ), h( e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==>
% 1.93/2.35 op2( h( e12 ), e23 ), e20 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==>
% 1.93/2.35 e21 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35 substitution1:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 paramod: (30991) {G1,W51,D3,L13,V0,M13} { h( e12 ) ==> e22, e20 ==> h( e12
% 1.93/2.35 ), e24 ==> h( e12 ), h( e12 ) ==> e21, h( e12 ) ==> e22, e23 ==> e22,
% 1.93/2.35 e20 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, h( e12 ) ==> e22,
% 1.93/2.35 e20 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21 }.
% 1.93/2.35 parent0[0]: (88) {G0,W5,D3,L1,V0,M1} I { op2( e23, e23 ) ==> e22 }.
% 1.93/2.35 parent1[0; 3]: (30250) {G1,W53,D3,L13,V0,M13} { h( e12 ) ==> op2( e23, e23
% 1.93/2.35 ), e20 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, h( e12 ) ==>
% 1.93/2.35 e22, e23 ==> e22, e20 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, h
% 1.93/2.35 ( e12 ) ==> e22, e20 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35 substitution1:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 factor: (30992) {G1,W47,D3,L12,V0,M12} { h( e12 ) ==> e22, e20 ==> h( e12
% 1.93/2.35 ), e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22, e20 ==> h( e12 ),
% 1.93/2.35 e24 ==> h( e12 ), h( e12 ) ==> e21, h( e12 ) ==> e22, e20 ==> h( e12 ),
% 1.93/2.35 e24 ==> h( e12 ), h( e12 ) ==> e21 }.
% 1.93/2.35 parent0[0, 4]: (30991) {G1,W51,D3,L13,V0,M13} { h( e12 ) ==> e22, e20 ==>
% 1.93/2.35 h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, h( e12 ) ==> e22, e23 ==>
% 1.93/2.35 e22, e20 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, h( e12 ) ==>
% 1.93/2.35 e22, e20 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 factor: (30993) {G1,W43,D3,L11,V0,M11} { h( e12 ) ==> e22, e20 ==> h( e12
% 1.93/2.35 ), e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22, e20 ==> h( e12 ),
% 1.93/2.35 e24 ==> h( e12 ), h( e12 ) ==> e21, e20 ==> h( e12 ), e24 ==> h( e12 ), h
% 1.93/2.35 ( e12 ) ==> e21 }.
% 1.93/2.35 parent0[0, 8]: (30992) {G1,W47,D3,L12,V0,M12} { h( e12 ) ==> e22, e20 ==>
% 1.93/2.35 h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22, e20 ==> h( e12
% 1.93/2.35 ), e24 ==> h( e12 ), h( e12 ) ==> e21, h( e12 ) ==> e22, e20 ==> h( e12
% 1.93/2.35 ), e24 ==> h( e12 ), h( e12 ) ==> e21 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 factor: (30994) {G1,W39,D3,L10,V0,M10} { h( e12 ) ==> e22, e20 ==> h( e12
% 1.93/2.35 ), e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22, e24 ==> h( e12 ), h
% 1.93/2.35 ( e12 ) ==> e21, e20 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21 }.
% 1.93/2.35 parent0[1, 5]: (30993) {G1,W43,D3,L11,V0,M11} { h( e12 ) ==> e22, e20 ==>
% 1.93/2.35 h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22, e20 ==> h( e12
% 1.93/2.35 ), e24 ==> h( e12 ), h( e12 ) ==> e21, e20 ==> h( e12 ), e24 ==> h( e12
% 1.93/2.35 ), h( e12 ) ==> e21 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 factor: (30995) {G1,W35,D3,L9,V0,M9} { h( e12 ) ==> e22, e20 ==> h( e12 )
% 1.93/2.35 , e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22, e24 ==> h( e12 ), h(
% 1.93/2.35 e12 ) ==> e21, e24 ==> h( e12 ), h( e12 ) ==> e21 }.
% 1.93/2.35 parent0[1, 7]: (30994) {G1,W39,D3,L10,V0,M10} { h( e12 ) ==> e22, e20 ==>
% 1.93/2.35 h( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22, e24 ==> h( e12
% 1.93/2.35 ), h( e12 ) ==> e21, e20 ==> h( e12 ), e24 ==> h( e12 ), h( e12 ) ==>
% 1.93/2.35 e21 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 factor: (30996) {G1,W31,D3,L8,V0,M8} { h( e12 ) ==> e22, e20 ==> h( e12 )
% 1.93/2.35 , e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22, h( e12 ) ==> e21, e24
% 1.93/2.35 ==> h( e12 ), h( e12 ) ==> e21 }.
% 1.93/2.35 parent0[2, 5]: (30995) {G1,W35,D3,L9,V0,M9} { h( e12 ) ==> e22, e20 ==> h
% 1.93/2.35 ( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22, e24 ==> h( e12
% 1.93/2.35 ), h( e12 ) ==> e21, e24 ==> h( e12 ), h( e12 ) ==> e21 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 factor: (30997) {G1,W27,D3,L7,V0,M7} { h( e12 ) ==> e22, e20 ==> h( e12 )
% 1.93/2.35 , e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22, h( e12 ) ==> e21, h(
% 1.93/2.35 e12 ) ==> e21 }.
% 1.93/2.35 parent0[2, 6]: (30996) {G1,W31,D3,L8,V0,M8} { h( e12 ) ==> e22, e20 ==> h
% 1.93/2.35 ( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22, h( e12 ) ==>
% 1.93/2.35 e21, e24 ==> h( e12 ), h( e12 ) ==> e21 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 factor: (30998) {G1,W23,D3,L6,V0,M6} { h( e12 ) ==> e22, e20 ==> h( e12 )
% 1.93/2.35 , e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22, h( e12 ) ==> e21 }.
% 1.93/2.35 parent0[3, 5]: (30997) {G1,W27,D3,L7,V0,M7} { h( e12 ) ==> e22, e20 ==> h
% 1.93/2.35 ( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22, h( e12 ) ==>
% 1.93/2.35 e21, h( e12 ) ==> e21 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 factor: (30999) {G1,W19,D3,L5,V0,M5} { h( e12 ) ==> e22, e20 ==> h( e12 )
% 1.93/2.35 , e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22 }.
% 1.93/2.35 parent0[3, 5]: (30998) {G1,W23,D3,L6,V0,M6} { h( e12 ) ==> e22, e20 ==> h
% 1.93/2.35 ( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22, h( e12 ) ==>
% 1.93/2.35 e21 }.
% 1.93/2.35 substitution0:
% 1.93/2.35 end
% 1.93/2.35
% 1.93/2.35 paramod: (31005) {G2,W30,D3,L8,V0,M8} { e20 ==> e23, e21 ==> h( e12 ), h(
% 1.93/2.35 e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e22, e24 ==> h( e12 ), h(
% 1.93/2.36 e12 ) ==> e21, e23 ==> e22 }.
% 1.93/2.36 parent0[2]: (21878) {G2,W16,D3,L4,V0,M4} { e21 ==> h( e12 ), h( e12 ) ==>
% 1.93/2.36 e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 1.93/2.36 parent1[1; 2]: (30999) {G1,W19,D3,L5,V0,M5} { h( e12 ) ==> e22, e20 ==> h
% 1.93/2.36 ( e12 ), e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22 }.
% 1.93/2.36 substitution0:
% 1.93/2.36 end
% 1.93/2.36 substitution1:
% 1.93/2.36 end
% 1.93/2.36
% 1.93/2.36 factor: (31071) {G2,W26,D3,L7,V0,M7} { e20 ==> e23, e21 ==> h( e12 ), h(
% 1.93/2.36 e12 ) ==> e22, h( e12 ) ==> e24, e24 ==> h( e12 ), h( e12 ) ==> e21, e23
% 1.93/2.36 ==> e22 }.
% 1.93/2.36 parent0[2, 4]: (31005) {G2,W30,D3,L8,V0,M8} { e20 ==> e23, e21 ==> h( e12
% 1.93/2.36 ), h( e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e22, e24 ==> h( e12
% 1.93/2.36 ), h( e12 ) ==> e21, e23 ==> e22 }.
% 1.93/2.36 substitution0:
% 1.93/2.36 end
% 1.93/2.36
% 1.93/2.36 resolution: (32462) {G1,W23,D3,L6,V0,M6} { e21 ==> h( e12 ), h( e12 ) ==>
% 1.93/2.36 e22, h( e12 ) ==> e24, e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22
% 1.93/2.36 }.
% 1.93/2.36 parent0[0]: (21893) {G0,W3,D2,L1,V0,M1} { ! e20 ==> e23 }.
% 1.93/2.36 parent1[0]: (31071) {G2,W26,D3,L7,V0,M7} { e20 ==> e23, e21 ==> h( e12 ),
% 1.93/2.36 h( e12 ) ==> e22, h( e12 ) ==> e24, e24 ==> h( e12 ), h( e12 ) ==> e21,
% 1.93/2.36 e23 ==> e22 }.
% 1.93/2.36 substitution0:
% 1.93/2.36 end
% 1.93/2.36 substitution1:
% 1.93/2.36 end
% 1.93/2.36
% 1.93/2.36 eqswap: (32468) {G1,W23,D3,L6,V0,M6} { e22 ==> e23, e21 ==> h( e12 ), h(
% 1.93/2.36 e12 ) ==> e22, h( e12 ) ==> e24, e24 ==> h( e12 ), h( e12 ) ==> e21 }.
% 1.93/2.36 parent0[5]: (32462) {G1,W23,D3,L6,V0,M6} { e21 ==> h( e12 ), h( e12 ) ==>
% 1.93/2.36 e22, h( e12 ) ==> e24, e24 ==> h( e12 ), h( e12 ) ==> e21, e23 ==> e22
% 1.93/2.36 }.
% 1.93/2.36 substitution0:
% 1.93/2.36 end
% 1.93/2.36
% 1.93/2.36 eqswap: (32472) {G1,W23,D3,L6,V0,M6} { h( e12 ) ==> e24, e22 ==> e23, e21
% 1.93/2.36 ==> h( e12 ), h( e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e21 }.
% 1.93/2.36 parent0[4]: (32468) {G1,W23,D3,L6,V0,M6} { e22 ==> e23, e21 ==> h( e12 ),
% 1.93/2.36 h( e12 ) ==> e22, h( e12 ) ==> e24, e24 ==> h( e12 ), h( e12 ) ==> e21
% 1.93/2.36 }.
% 1.93/2.36 substitution0:
% 1.93/2.36 end
% 1.93/2.36
% 1.93/2.36 eqswap: (32483) {G1,W23,D3,L6,V0,M6} { h( e12 ) ==> e21, h( e12 ) ==> e24
% 1.93/2.36 , e22 ==> e23, h( e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e21 }.
% 1.93/2.36 parent0[2]: (32472) {G1,W23,D3,L6,V0,M6} { h( e12 ) ==> e24, e22 ==> e23,
% 1.93/2.36 e21 ==> h( e12 ), h( e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e21
% 1.93/2.36 }.
% 1.93/2.36 substitution0:
% 1.93/2.36 end
% 1.93/2.36
% 1.93/2.36 eqswap: (32484) {G1,W23,D3,L6,V0,M6} { e23 ==> e22, h( e12 ) ==> e21, h(
% 1.93/2.36 e12 ) ==> e24, h( e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e21 }.
% 1.93/2.36 parent0[2]: (32483) {G1,W23,D3,L6,V0,M6} { h( e12 ) ==> e21, h( e12 ) ==>
% 1.93/2.36 e24, e22 ==> e23, h( e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e21
% 1.93/2.36 }.
% 1.93/2.36 substitution0:
% 1.93/2.36 end
% 1.93/2.36
% 1.93/2.36 factor: (32504) {G1,W19,D3,L5,V0,M5} { e23 ==> e22, h( e12 ) ==> e21, h(
% 1.93/2.36 e12 ) ==> e24, h( e12 ) ==> e22, h( e12 ) ==> e24 }.
% 1.93/2.36 parent0[1, 5]: (32484) {G1,W23,D3,L6,V0,M6} { e23 ==> e22, h( e12 ) ==>
% 1.93/2.36 e21, h( e12 ) ==> e24, h( e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==>
% 1.93/2.36 e21 }.
% 1.93/2.36 substitution0:
% 1.93/2.36 end
% 1.93/2.36
% 1.93/2.36 factor: (32505) {G1,W15,D3,L4,V0,M4} { e23 ==> e22, h( e12 ) ==> e21, h(
% 1.93/2.36 e12 ) ==> e24, h( e12 ) ==> e22 }.
% 1.93/2.36 parent0[2, 4]: (32504) {G1,W19,D3,L5,V0,M5} { e23 ==> e22, h( e12 ) ==>
% 1.93/2.36 e21, h( e12 ) ==> e24, h( e12 ) ==> e22, h( e12 ) ==> e24 }.
% 1.93/2.36 substitution0:
% 1.93/2.36 end
% 1.93/2.36
% 1.93/2.36 subsumption: (222) {G3,W15,D3,L4,V0,M4} P(97,117);d(88);d(220);r(12) { h(
% 1.93/2.36 e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==> e24, e23 ==> e22 }.
% 1.93/2.36 parent0: (32505) {G1,W15,D3,L4,V0,M4} { e23 ==> e22, h( e12 ) ==> e21, h(
% 1.93/2.36 e12 ) ==> e24, h( e12 ) ==> e22 }.
% 1.93/2.36 substitution0:
% 1.93/2.36 end
% 1.93/2.36 permutation0:
% 1.93/2.36 0 ==> 3
% 1.93/2.36 1 ==> 0
% 1.93/2.36 2 ==> 2
% 1.93/2.36 3 ==> 1
% 1.93/2.36 end
% 1.93/2.36
% 1.93/2.36 *** allocated 256285 integers for clauses
% 1.93/2.36 eqswap: (32529) {G2,W16,D3,L4,V0,M4} { e21 ==> h( e12 ), h( e12 ) ==> e22
% 1.93/2.36 , h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 1.93/2.36 parent0[0]: (220) {G2,W16,D3,L4,V0,M4} P(97,117);d(70);r(13) { h( e12 ) ==>
% 1.93/2.36 e21, h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 1.93/2.36 substitution0:
% 1.93/2.36 end
% 1.93/2.36
% 1.93/2.36 eqswap: (32544) {G3,W15,D3,L4,V0,M4} { e21 ==> h( e12 ), h( e12 ) ==> e22
% 1.93/2.36 , h( e12 ) ==> e24, e23 ==> e22 }.
% 1.93/2.36 parent0[0]: (222) {G3,W15,D3,L4,V0,M4} P(97,117);d(88);d(220);r(12) { h(
% 1.93/2.36 e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==> e24, e23 ==> e22 }.
% 1.93/2.36 substitution0:
% 1.93/2.36 end
% 1.93/2.36
% 1.93/2.36 eqfact: (32559) {G0,W15,D3,L4,V0,M4} { ! e22 = e23, e21 ==> h( e12 ), h(
% 1.93/2.36 e12 ) ==> e23, h( e12 ) ==> e24 }.
% 1.93/2.36 parent0[1, 2]: (32529) {G2,W16,D3,L4,V0,M4} { e21 ==> h( e12 ), h( e12 )
% 4.09/4.47 ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 4.09/4.47 substitution0:
% 4.09/4.47 end
% 4.09/4.47
% 4.09/4.47 paramod: (32572) {G1,W27,D3,L7,V0,M7} { h( e12 ) ==> e22, e21 ==> h( e12 )
% 4.09/4.47 , h( e12 ) ==> e22, h( e12 ) ==> e24, ! e22 = e23, e21 ==> h( e12 ), h(
% 4.09/4.47 e12 ) ==> e24 }.
% 4.09/4.47 parent0[3]: (32544) {G3,W15,D3,L4,V0,M4} { e21 ==> h( e12 ), h( e12 ) ==>
% 4.09/4.47 e22, h( e12 ) ==> e24, e23 ==> e22 }.
% 4.09/4.47 parent1[2; 3]: (32559) {G0,W15,D3,L4,V0,M4} { ! e22 = e23, e21 ==> h( e12
% 4.09/4.47 ), h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 4.09/4.47 substitution0:
% 4.09/4.47 end
% 4.09/4.47 substitution1:
% 4.09/4.47 end
% 4.09/4.47
% 4.09/4.47 paramod: (32579) {G2,W39,D3,L10,V0,M10} { ! e22 = e22, e21 ==> h( e12 ), h
% 4.09/4.47 ( e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e22, e21 ==> h( e12 ), h
% 4.09/4.47 ( e12 ) ==> e22, h( e12 ) ==> e24, e21 ==> h( e12 ), h( e12 ) ==> e24 }.
% 4.09/4.47 parent0[3]: (32544) {G3,W15,D3,L4,V0,M4} { e21 ==> h( e12 ), h( e12 ) ==>
% 4.09/4.47 e22, h( e12 ) ==> e24, e23 ==> e22 }.
% 4.09/4.47 parent1[4; 3]: (32572) {G1,W27,D3,L7,V0,M7} { h( e12 ) ==> e22, e21 ==> h
% 4.09/4.47 ( e12 ), h( e12 ) ==> e22, h( e12 ) ==> e24, ! e22 = e23, e21 ==> h( e12
% 4.09/4.47 ), h( e12 ) ==> e24 }.
% 4.09/4.47 substitution0:
% 4.09/4.47 end
% 4.09/4.47 substitution1:
% 4.09/4.47 end
% 4.09/4.47
% 4.09/4.47 factor: (32869) {G2,W35,D3,L9,V0,M9} { ! e22 = e22, e21 ==> h( e12 ), h(
% 4.09/4.47 e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e22, h( e12 ) ==> e22, h(
% 4.09/4.47 e12 ) ==> e24, e21 ==> h( e12 ), h( e12 ) ==> e24 }.
% 4.09/4.47 parent0[1, 5]: (32579) {G2,W39,D3,L10,V0,M10} { ! e22 = e22, e21 ==> h(
% 4.09/4.47 e12 ), h( e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e22, e21 ==> h(
% 4.09/4.47 e12 ), h( e12 ) ==> e22, h( e12 ) ==> e24, e21 ==> h( e12 ), h( e12 ) ==>
% 4.09/4.47 e24 }.
% 4.09/4.47 substitution0:
% 4.09/4.47 end
% 4.09/4.47
% 4.09/4.47 factor: (32870) {G2,W31,D3,L8,V0,M8} { ! e22 = e22, e21 ==> h( e12 ), h(
% 4.09/4.47 e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e22, h( e12 ) ==> e22, h(
% 4.09/4.47 e12 ) ==> e24, h( e12 ) ==> e24 }.
% 4.09/4.47 parent0[1, 7]: (32869) {G2,W35,D3,L9,V0,M9} { ! e22 = e22, e21 ==> h( e12
% 4.09/4.47 ), h( e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e22, h( e12 ) ==>
% 4.09/4.47 e22, h( e12 ) ==> e24, e21 ==> h( e12 ), h( e12 ) ==> e24 }.
% 4.09/4.47 substitution0:
% 4.09/4.47 end
% 4.09/4.47
% 4.09/4.47 factor: (32871) {G2,W27,D3,L7,V0,M7} { ! e22 = e22, e21 ==> h( e12 ), h(
% 4.09/4.47 e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e22, h( e12 ) ==> e24, h(
% 4.09/4.47 e12 ) ==> e24 }.
% 4.09/4.47 parent0[2, 4]: (32870) {G2,W31,D3,L8,V0,M8} { ! e22 = e22, e21 ==> h( e12
% 4.09/4.47 ), h( e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e22, h( e12 ) ==>
% 4.09/4.47 e22, h( e12 ) ==> e24, h( e12 ) ==> e24 }.
% 4.09/4.47 substitution0:
% 4.09/4.47 end
% 4.09/4.47
% 4.09/4.47 factor: (32872) {G2,W23,D3,L6,V0,M6} { ! e22 = e22, e21 ==> h( e12 ), h(
% 4.09/4.47 e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e24, h( e12 ) ==> e24 }.
% 4.09/4.47 parent0[2, 4]: (32871) {G2,W27,D3,L7,V0,M7} { ! e22 = e22, e21 ==> h( e12
% 4.09/4.47 ), h( e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e22, h( e12 ) ==>
% 4.09/4.47 e24, h( e12 ) ==> e24 }.
% 4.09/4.47 substitution0:
% 4.09/4.47 end
% 4.09/4.47
% 4.09/4.47 factor: (32873) {G2,W19,D3,L5,V0,M5} { ! e22 = e22, e21 ==> h( e12 ), h(
% 4.09/4.47 e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e24 }.
% 4.09/4.47 parent0[3, 4]: (32872) {G2,W23,D3,L6,V0,M6} { ! e22 = e22, e21 ==> h( e12
% 4.09/4.47 ), h( e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e24, h( e12 ) ==>
% 4.09/4.47 e24 }.
% 4.09/4.47 substitution0:
% 4.09/4.47 end
% 4.09/4.47
% 4.09/4.47 factor: (32874) {G2,W15,D3,L4,V0,M4} { ! e22 = e22, e21 ==> h( e12 ), h(
% 4.09/4.47 e12 ) ==> e22, h( e12 ) ==> e24 }.
% 4.09/4.47 parent0[3, 4]: (32873) {G2,W19,D3,L5,V0,M5} { ! e22 = e22, e21 ==> h( e12
% 4.09/4.47 ), h( e12 ) ==> e22, h( e12 ) ==> e24, h( e12 ) ==> e24 }.
% 4.09/4.47 substitution0:
% 4.09/4.47 end
% 4.09/4.47
% 4.09/4.47 eqrefl: (32878) {G0,W12,D3,L3,V0,M3} { e21 ==> h( e12 ), h( e12 ) ==> e22
% 4.09/4.47 , h( e12 ) ==> e24 }.
% 4.09/4.47 parent0[0]: (32874) {G2,W15,D3,L4,V0,M4} { ! e22 = e22, e21 ==> h( e12 ),
% 4.09/4.47 h( e12 ) ==> e22, h( e12 ) ==> e24 }.
% 4.09/4.47 substitution0:
% 4.09/4.47 end
% 4.09/4.47
% 4.09/4.47 eqswap: (32879) {G0,W12,D3,L3,V0,M3} { h( e12 ) ==> e21, h( e12 ) ==> e22
% 4.09/4.47 , h( e12 ) ==> e24 }.
% 4.09/4.47 parent0[0]: (32878) {G0,W12,D3,L3,V0,M3} { e21 ==> h( e12 ), h( e12 ) ==>
% 4.09/4.47 e22, h( e12 ) ==> e24 }.
% 4.09/4.47 substitution0:
% 4.09/4.47 end
% 4.09/4.47
% 4.09/4.47 subsumption: (224) {G4,W12,D3,L3,V0,M3} E(220);d(222);q { h( e12 ) ==> e21
% 4.09/4.47 , h( e12 ) ==> e22, h( e12 ) ==> e24 }.
% 4.09/4.47 parent0: (32879) {G0,W12,D3,L3,V0,M3} { h( e12 ) ==> e21, h( e12 ) ==> e22
% 4.09/4.47 , h( e12 ) ==> e24 }.
% 4.09/4.47 substitution0:
% 4.09/4.47 end
% 4.09/4.47 permutation0:
% 4.09/4.47 0 ==> 0
% 4.09/4.47 1 ==> 1
% 4.09/4.47 2 ==> 2
% 4.09/4.47 end
% 4.09/4.47
% 4.09/4.47 *** allocated 256285 integers for termspace/termends
% 4.09/4.47
% 4.09/4.47 ==> (237) {G5,W8,D3,L2,V0,M2} P(224,117);d(82);r(17) { h( e12 ) ==> e21, h
% 4.09/4.47 ( e12 ) ==> e24 }.
% 4.09/4.47
% 4.09/4.47
% 4.09/4.47
% 4.09/4.47 !!! Internal Problem: OH, OH, COULD NOT DERIVE GOAL !!!
% 4.09/4.47
% 4.09/4.47 Bliksem ended
%------------------------------------------------------------------------------