%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : ALG075+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n017.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:23 EDT 2022
% Result : Theorem 0.74s 1.33s
% Output : Refutation 0.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ALG075+1 : TPTP v8.1.0. Released v2.7.0.
% 0.03/0.13 % Command : bliksem %s
% 0.14/0.34 % Computer : n017.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % DateTime : Wed Jun 8 17:32:18 EDT 2022
% 0.14/0.34 % CPUTime :
% 0.72/1.11 *** allocated 10000 integers for termspace/termends
% 0.72/1.11 *** allocated 10000 integers for clauses
% 0.72/1.11 *** allocated 10000 integers for justifications
% 0.72/1.11 Bliksem 1.12
% 0.72/1.11
% 0.72/1.11
% 0.72/1.11 Automatic Strategy Selection
% 0.72/1.11
% 0.72/1.11
% 0.72/1.11 Clauses:
% 0.72/1.11
% 0.72/1.11 { ! e10 = e11 }.
% 0.72/1.11 { ! e10 = e12 }.
% 0.72/1.11 { ! e10 = e13 }.
% 0.72/1.11 { ! e10 = e14 }.
% 0.72/1.11 { ! e11 = e12 }.
% 0.72/1.11 { ! e11 = e13 }.
% 0.72/1.11 { ! e11 = e14 }.
% 0.72/1.11 { ! e12 = e13 }.
% 0.72/1.11 { ! e12 = e14 }.
% 0.72/1.11 { ! e13 = e14 }.
% 0.72/1.11 { ! e20 = e21 }.
% 0.72/1.11 { ! e20 = e22 }.
% 0.72/1.11 { ! e20 = e23 }.
% 0.72/1.11 { ! e20 = e24 }.
% 0.72/1.11 { ! e21 = e22 }.
% 0.72/1.11 { ! e21 = e23 }.
% 0.72/1.11 { ! e21 = e24 }.
% 0.72/1.11 { ! e22 = e23 }.
% 0.72/1.11 { ! e22 = e24 }.
% 0.72/1.11 { ! e23 = e24 }.
% 0.72/1.11 { ! e10 = e20 }.
% 0.72/1.11 { ! e10 = e21 }.
% 0.72/1.11 { ! e10 = e22 }.
% 0.72/1.11 { ! e10 = e23 }.
% 0.72/1.11 { ! e10 = e24 }.
% 0.72/1.11 { ! e11 = e20 }.
% 0.72/1.11 { ! e11 = e21 }.
% 0.72/1.11 { ! e11 = e22 }.
% 0.72/1.11 { ! e11 = e23 }.
% 0.72/1.11 { ! e11 = e24 }.
% 0.72/1.11 { ! e12 = e20 }.
% 0.72/1.11 { ! e12 = e21 }.
% 0.72/1.11 { ! e12 = e22 }.
% 0.72/1.11 { ! e12 = e23 }.
% 0.72/1.11 { ! e12 = e24 }.
% 0.72/1.11 { ! e13 = e20 }.
% 0.72/1.11 { ! e13 = e21 }.
% 0.72/1.11 { ! e13 = e22 }.
% 0.72/1.11 { ! e13 = e23 }.
% 0.72/1.11 { ! e13 = e24 }.
% 0.72/1.11 { ! e14 = e20 }.
% 0.72/1.11 { ! e14 = e21 }.
% 0.72/1.11 { ! e14 = e22 }.
% 0.72/1.11 { ! e14 = e23 }.
% 0.72/1.11 { ! e14 = e24 }.
% 0.72/1.11 { op1( e10, e10 ) = e10 }.
% 0.72/1.11 { op1( e10, e11 ) = e11 }.
% 0.72/1.11 { op1( e10, e12 ) = e12 }.
% 0.72/1.11 { op1( e10, e13 ) = e13 }.
% 0.72/1.11 { op1( e10, e14 ) = e14 }.
% 0.72/1.11 { op1( e11, e10 ) = e11 }.
% 0.72/1.11 { op1( e11, e11 ) = e14 }.
% 0.72/1.11 { op1( e11, e12 ) = e10 }.
% 0.72/1.11 { op1( e11, e13 ) = e12 }.
% 0.72/1.11 { op1( e11, e14 ) = e13 }.
% 0.72/1.11 { op1( e12, e10 ) = e12 }.
% 0.72/1.11 { op1( e12, e11 ) = e10 }.
% 0.72/1.11 { op1( e12, e12 ) = e13 }.
% 0.72/1.11 { op1( e12, e13 ) = e14 }.
% 0.72/1.11 { op1( e12, e14 ) = e11 }.
% 0.72/1.11 { op1( e13, e10 ) = e13 }.
% 0.72/1.11 { op1( e13, e11 ) = e12 }.
% 0.72/1.11 { op1( e13, e12 ) = e14 }.
% 0.72/1.11 { op1( e13, e13 ) = e11 }.
% 0.72/1.11 { op1( e13, e14 ) = e10 }.
% 0.72/1.11 { op1( e14, e10 ) = e14 }.
% 0.72/1.11 { op1( e14, e11 ) = e13 }.
% 0.72/1.11 { op1( e14, e12 ) = e11 }.
% 0.72/1.11 { op1( e14, e13 ) = e10 }.
% 0.72/1.11 { op1( e14, e14 ) = e12 }.
% 0.72/1.11 { op2( e20, e20 ) = e20 }.
% 0.72/1.11 { op2( e20, e21 ) = e21 }.
% 0.72/1.11 { op2( e20, e22 ) = e22 }.
% 0.72/1.11 { op2( e20, e23 ) = e23 }.
% 0.72/1.11 { op2( e20, e24 ) = e24 }.
% 0.72/1.11 { op2( e21, e20 ) = e21 }.
% 0.72/1.11 { op2( e21, e21 ) = e20 }.
% 0.72/1.11 { op2( e21, e22 ) = e23 }.
% 0.72/1.11 { op2( e21, e23 ) = e24 }.
% 0.72/1.11 { op2( e21, e24 ) = e22 }.
% 0.72/1.11 { op2( e22, e20 ) = e22 }.
% 0.72/1.11 { op2( e22, e21 ) = e24 }.
% 0.72/1.11 { op2( e22, e22 ) = e20 }.
% 0.72/1.11 { op2( e22, e23 ) = e21 }.
% 0.72/1.11 { op2( e22, e24 ) = e23 }.
% 0.72/1.11 { op2( e23, e20 ) = e23 }.
% 0.72/1.11 { op2( e23, e21 ) = e22 }.
% 0.72/1.11 { op2( e23, e22 ) = e24 }.
% 0.72/1.11 { op2( e23, e23 ) = e20 }.
% 0.72/1.11 { op2( e23, e24 ) = e21 }.
% 0.72/1.11 { op2( e24, e20 ) = e24 }.
% 0.72/1.11 { op2( e24, e21 ) = e23 }.
% 0.72/1.11 { op2( e24, e22 ) = e21 }.
% 0.72/1.11 { op2( e24, e23 ) = e22 }.
% 0.72/1.11 { op2( e24, e24 ) = e20 }.
% 0.72/1.11 { h( e10 ) = e20, h( e10 ) = e21, h( e10 ) = e22, h( e10 ) = e23, h( e10 )
% 0.72/1.11 = e24 }.
% 0.72/1.11 { h( e11 ) = e20, h( e11 ) = e21, h( e11 ) = e22, h( e11 ) = e23, h( e11 )
% 0.72/1.11 = e24 }.
% 0.72/1.11 { h( e12 ) = e20, h( e12 ) = e21, h( e12 ) = e22, h( e12 ) = e23, h( e12 )
% 0.72/1.11 = e24 }.
% 0.72/1.11 { h( e13 ) = e20, h( e13 ) = e21, h( e13 ) = e22, h( e13 ) = e23, h( e13 )
% 0.72/1.11 = e24 }.
% 0.72/1.11 { h( e14 ) = e20, h( e14 ) = e21, h( e14 ) = e22, h( e14 ) = e23, h( e14 )
% 0.72/1.11 = e24 }.
% 0.72/1.11 { j( e20 ) = e10, j( e20 ) = e11, j( e20 ) = e12, j( e20 ) = e13, j( e20 )
% 0.72/1.11 = e14 }.
% 0.72/1.11 { j( e21 ) = e10, j( e21 ) = e11, j( e21 ) = e12, j( e21 ) = e13, j( e21 )
% 0.72/1.11 = e14 }.
% 0.72/1.11 { j( e22 ) = e10, j( e22 ) = e11, j( e22 ) = e12, j( e22 ) = e13, j( e22 )
% 0.72/1.11 = e14 }.
% 0.72/1.11 { j( e23 ) = e10, j( e23 ) = e11, j( e23 ) = e12, j( e23 ) = e13, j( e23 )
% 0.72/1.11 = e14 }.
% 0.72/1.11 { j( e24 ) = e10, j( e24 ) = e11, j( e24 ) = e12, j( e24 ) = e13, j( e24 )
% 0.72/1.11 = e14 }.
% 0.72/1.11 { h( op1( e10, e10 ) ) = op2( h( e10 ), h( e10 ) ) }.
% 0.72/1.11 { h( op1( e10, e11 ) ) = op2( h( e10 ), h( e11 ) ) }.
% 0.72/1.11 { h( op1( e10, e12 ) ) = op2( h( e10 ), h( e12 ) ) }.
% 0.72/1.11 { h( op1( e10, e13 ) ) = op2( h( e10 ), h( e13 ) ) }.
% 0.72/1.11 { h( op1( e10, e14 ) ) = op2( h( e10 ), h( e14 ) ) }.
% 0.72/1.11 { h( op1( e11, e10 ) ) = op2( h( e11 ), h( e10 ) ) }.
% 0.72/1.11 { h( op1( e11, e11 ) ) = op2( h( e11 ), h( e11 ) ) }.
% 0.72/1.11 { h( op1( e11, e12 ) ) = op2( h( e11 ), h( e12 ) ) }.
% 0.72/1.11 { h( op1( e11, e13 ) ) = op2( h( e11 ), h( e13 ) ) }.
% 0.72/1.11 { h( op1( e11, e14 ) ) = op2( h( e11 ), h( e14 ) ) }.
% 0.72/1.11 { h( op1( e12, e10 ) ) = op2( h( e12 ), h( e10 ) ) }.
% 0.72/1.11 { h( op1( e12, e11 ) ) = op2( h( e12 ), h( e11 ) ) }.
% 0.72/1.11 { h( op1( e12, e12 ) ) = op2( h( e12 ), h( e12 ) ) }.
% 0.72/1.11 { h( op1( e12, e13 ) ) = op2( h( e12 ), h( e13 ) ) }.
% 0.72/1.11 { h( op1( e12, e14 ) ) = op2( h( e12 ), h( e14 ) ) }.
% 0.72/1.11 { h( op1( e13, e10 ) ) = op2( h( e13 ), h( e10 ) ) }.
% 0.72/1.11 { h( op1( e13, e11 ) ) = op2( h( e13 ), h( e11 ) ) }.
% 0.74/1.33 { h( op1( e13, e12 ) ) = op2( h( e13 ), h( e12 ) ) }.
% 0.74/1.33 { h( op1( e13, e13 ) ) = op2( h( e13 ), h( e13 ) ) }.
% 0.74/1.33 { h( op1( e13, e14 ) ) = op2( h( e13 ), h( e14 ) ) }.
% 0.74/1.33 { h( op1( e14, e10 ) ) = op2( h( e14 ), h( e10 ) ) }.
% 0.74/1.33 { h( op1( e14, e11 ) ) = op2( h( e14 ), h( e11 ) ) }.
% 0.74/1.33 { h( op1( e14, e12 ) ) = op2( h( e14 ), h( e12 ) ) }.
% 0.74/1.33 { h( op1( e14, e13 ) ) = op2( h( e14 ), h( e13 ) ) }.
% 0.74/1.33 { h( op1( e14, e14 ) ) = op2( h( e14 ), h( e14 ) ) }.
% 0.74/1.33 { j( op2( e20, e20 ) ) = op1( j( e20 ), j( e20 ) ) }.
% 0.74/1.33 { j( op2( e20, e21 ) ) = op1( j( e20 ), j( e21 ) ) }.
% 0.74/1.33 { j( op2( e20, e22 ) ) = op1( j( e20 ), j( e22 ) ) }.
% 0.74/1.33 { j( op2( e20, e23 ) ) = op1( j( e20 ), j( e23 ) ) }.
% 0.74/1.33 { j( op2( e20, e24 ) ) = op1( j( e20 ), j( e24 ) ) }.
% 0.74/1.33 { j( op2( e21, e20 ) ) = op1( j( e21 ), j( e20 ) ) }.
% 0.74/1.33 { j( op2( e21, e21 ) ) = op1( j( e21 ), j( e21 ) ) }.
% 0.74/1.33 { j( op2( e21, e22 ) ) = op1( j( e21 ), j( e22 ) ) }.
% 0.74/1.33 { j( op2( e21, e23 ) ) = op1( j( e21 ), j( e23 ) ) }.
% 0.74/1.33 { j( op2( e21, e24 ) ) = op1( j( e21 ), j( e24 ) ) }.
% 0.74/1.33 { j( op2( e22, e20 ) ) = op1( j( e22 ), j( e20 ) ) }.
% 0.74/1.33 { j( op2( e22, e21 ) ) = op1( j( e22 ), j( e21 ) ) }.
% 0.74/1.33 { j( op2( e22, e22 ) ) = op1( j( e22 ), j( e22 ) ) }.
% 0.74/1.33 { j( op2( e22, e23 ) ) = op1( j( e22 ), j( e23 ) ) }.
% 0.74/1.33 { j( op2( e22, e24 ) ) = op1( j( e22 ), j( e24 ) ) }.
% 0.74/1.33 { j( op2( e23, e20 ) ) = op1( j( e23 ), j( e20 ) ) }.
% 0.74/1.33 { j( op2( e23, e21 ) ) = op1( j( e23 ), j( e21 ) ) }.
% 0.74/1.33 { j( op2( e23, e22 ) ) = op1( j( e23 ), j( e22 ) ) }.
% 0.74/1.33 { j( op2( e23, e23 ) ) = op1( j( e23 ), j( e23 ) ) }.
% 0.74/1.33 { j( op2( e23, e24 ) ) = op1( j( e23 ), j( e24 ) ) }.
% 0.74/1.33 { j( op2( e24, e20 ) ) = op1( j( e24 ), j( e20 ) ) }.
% 0.74/1.33 { j( op2( e24, e21 ) ) = op1( j( e24 ), j( e21 ) ) }.
% 0.74/1.33 { j( op2( e24, e22 ) ) = op1( j( e24 ), j( e22 ) ) }.
% 0.74/1.33 { j( op2( e24, e23 ) ) = op1( j( e24 ), j( e23 ) ) }.
% 0.74/1.33 { j( op2( e24, e24 ) ) = op1( j( e24 ), j( e24 ) ) }.
% 0.74/1.33 { h( j( e20 ) ) = e20 }.
% 0.74/1.33 { h( j( e21 ) ) = e21 }.
% 0.74/1.33 { h( j( e22 ) ) = e22 }.
% 0.74/1.33 { h( j( e23 ) ) = e23 }.
% 0.74/1.33 { h( j( e24 ) ) = e24 }.
% 0.74/1.33 { j( h( e10 ) ) = e10 }.
% 0.74/1.33 { j( h( e11 ) ) = e11 }.
% 0.74/1.33 { j( h( e12 ) ) = e12 }.
% 0.74/1.33 { j( h( e13 ) ) = e13 }.
% 0.74/1.33 { j( h( e14 ) ) = e14 }.
% 0.74/1.33
% 0.74/1.33 percentage equality = 1.000000, percentage horn = 0.939394
% 0.74/1.33 This is a pure equality problem
% 0.74/1.33
% 0.74/1.33
% 0.74/1.33
% 0.74/1.33 Options Used:
% 0.74/1.33
% 0.74/1.33 useres = 1
% 0.74/1.33 useparamod = 1
% 0.74/1.33 useeqrefl = 1
% 0.74/1.33 useeqfact = 1
% 0.74/1.33 usefactor = 1
% 0.74/1.33 usesimpsplitting = 0
% 0.74/1.33 usesimpdemod = 5
% 0.74/1.33 usesimpres = 3
% 0.74/1.33
% 0.74/1.33 resimpinuse = 1000
% 0.74/1.33 resimpclauses = 20000
% 0.74/1.33 substype = eqrewr
% 0.74/1.33 backwardsubs = 1
% 0.74/1.33 selectoldest = 5
% 0.74/1.33
% 0.74/1.33 litorderings [0] = split
% 0.74/1.33 litorderings [1] = extend the termordering, first sorting on arguments
% 0.74/1.33
% 0.74/1.33 termordering = kbo
% 0.74/1.33
% 0.74/1.33 litapriori = 0
% 0.74/1.33 termapriori = 1
% 0.74/1.33 litaposteriori = 0
% 0.74/1.33 termaposteriori = 0
% 0.74/1.33 demodaposteriori = 0
% 0.74/1.33 ordereqreflfact = 0
% 0.74/1.33
% 0.74/1.33 litselect = negord
% 0.74/1.33
% 0.74/1.33 maxweight = 15
% 0.74/1.33 maxdepth = 30000
% 0.74/1.33 maxlength = 115
% 0.74/1.33 maxnrvars = 195
% 0.74/1.33 excuselevel = 1
% 0.74/1.33 increasemaxweight = 1
% 0.74/1.33
% 0.74/1.33 maxselected = 10000000
% 0.74/1.33 maxnrclauses = 10000000
% 0.74/1.33
% 0.74/1.33 showgenerated = 0
% 0.74/1.33 showkept = 0
% 0.74/1.33 showselected = 0
% 0.74/1.33 showdeleted = 0
% 0.74/1.33 showresimp = 1
% 0.74/1.33 showstatus = 2000
% 0.74/1.33
% 0.74/1.33 prologoutput = 0
% 0.74/1.33 nrgoals = 5000000
% 0.74/1.33 totalproof = 1
% 0.74/1.33
% 0.74/1.33 Symbols occurring in the translation:
% 0.74/1.33
% 0.74/1.33 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.74/1.33 . [1, 2] (w:1, o:23, a:1, s:1, b:0),
% 0.74/1.33 ! [4, 1] (w:0, o:16, a:1, s:1, b:0),
% 0.74/1.33 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.74/1.33 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.74/1.33 e10 [35, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.74/1.33 e11 [36, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.74/1.33 e12 [37, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.74/1.33 e13 [38, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.74/1.33 e14 [39, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.74/1.33 e20 [40, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.74/1.33 e21 [41, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.74/1.33 e22 [42, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.74/1.33 e23 [43, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.74/1.33 e24 [44, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.74/1.33 op1 [45, 2] (w:1, o:47, a:1, s:1, b:0),
% 0.74/1.33 op2 [46, 2] (w:1, o:48, a:1, s:1, b:0),
% 0.74/1.33 h [47, 1] (w:1, o:21, a:1, s:1, b:0),
% 0.74/1.33 j [48, 1] (w:1, o:22, a:1, s:1, b:0).
% 0.74/1.33
% 0.74/1.33
% 0.74/1.33 Starting Search:
% 0.74/1.33
% 0.74/1.33 *** allocated 15000 integers for clauses
% 0.74/1.33 Resimplifying inuse:
% 0.74/1.33 Done
% 0.74/1.33
% 0.74/1.33 Failed to find proof!
% 0.74/1.33 maxweight = 15
% 0.74/1.33 maxnrclauses = 10000000
% 0.74/1.33 Generated: 14585
% 0.74/1.33 Kept: 215
% 0.74/1.33
% 0.74/1.33
% 0.74/1.33 The strategy used was not complete!
% 0.74/1.33
% 0.74/1.33 Increased maxweight to 16
% 0.74/1.33
% 0.74/1.33 Starting Search:
% 0.74/1.33
% 0.74/1.33 *** allocated 22500 integers for clauses
% 0.74/1.33
% 0.74/1.33 Bliksems!, er is een bewijs:
% 0.74/1.33 % SZS status Theorem
% 0.74/1.33 % SZS output start Refutation
% 0.74/1.33
% 0.74/1.33 (3) {G0,W3,D2,L1,V0,M1} I { ! e14 ==> e10 }.
% 0.74/1.33 (5) {G0,W3,D2,L1,V0,M1} I { ! e13 ==> e11 }.
% 0.74/1.33 (6) {G0,W3,D2,L1,V0,M1} I { ! e14 ==> e11 }.
% 0.74/1.33 (7) {G0,W3,D2,L1,V0,M1} I { ! e13 ==> e12 }.
% 0.74/1.33 (13) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e20 }.
% 0.74/1.33 (14) {G0,W3,D2,L1,V0,M1} I { ! e22 ==> e21 }.
% 0.74/1.33 (15) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e21 }.
% 0.74/1.33 (17) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e22 }.
% 0.74/1.33 (51) {G0,W5,D3,L1,V0,M1} I { op1( e11, e11 ) ==> e14 }.
% 0.74/1.33 (57) {G0,W5,D3,L1,V0,M1} I { op1( e12, e12 ) ==> e13 }.
% 0.74/1.33 (63) {G0,W5,D3,L1,V0,M1} I { op1( e13, e13 ) ==> e11 }.
% 0.74/1.33 (69) {G0,W5,D3,L1,V0,M1} I { op1( e14, e14 ) ==> e12 }.
% 0.74/1.33 (70) {G0,W5,D3,L1,V0,M1} I { op2( e20, e20 ) ==> e20 }.
% 0.74/1.33 (76) {G0,W5,D3,L1,V0,M1} I { op2( e21, e21 ) ==> e20 }.
% 0.74/1.33 (82) {G0,W5,D3,L1,V0,M1} I { op2( e22, e22 ) ==> e20 }.
% 0.74/1.33 (88) {G0,W5,D3,L1,V0,M1} I { op2( e23, e23 ) ==> e20 }.
% 0.74/1.33 (94) {G0,W5,D3,L1,V0,M1} I { op2( e24, e24 ) ==> e20 }.
% 0.74/1.33 (96) {G0,W20,D3,L5,V0,M5} I { h( e11 ) ==> e20, h( e11 ) ==> e21, h( e11 )
% 0.74/1.33 ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 0.74/1.33 (100) {G0,W20,D3,L5,V0,M5} I { j( e20 ) ==> e10, j( e20 ) ==> e11, j( e20 )
% 0.74/1.33 ==> e12, j( e20 ) ==> e13, j( e20 ) ==> e14 }.
% 0.74/1.33 (111) {G1,W8,D4,L1,V0,M1} I;d(51) { op2( h( e11 ), h( e11 ) ) ==> h( e14 )
% 0.74/1.33 }.
% 0.74/1.33 (130) {G1,W8,D4,L1,V0,M1} I;d(70) { op1( j( e20 ), j( e20 ) ) ==> j( e20 )
% 0.74/1.33 }.
% 0.74/1.33 (154) {G1,W8,D4,L1,V0,M1} I;d(94) { op1( j( e24 ), j( e24 ) ) ==> j( e20 )
% 0.74/1.33 }.
% 0.74/1.33 (161) {G0,W5,D4,L1,V0,M1} I { j( h( e11 ) ) ==> e11 }.
% 0.74/1.33 (164) {G0,W5,D4,L1,V0,M1} I { j( h( e14 ) ) ==> e14 }.
% 0.74/1.33 (165) {G1,W20,D3,L5,V0,M5} P(96,161) { j( e20 ) ==> e11, h( e11 ) ==> e21,
% 0.74/1.33 h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 0.74/1.33 (169) {G1,W20,D3,L5,V0,M5} P(96,161) { j( e24 ) ==> e11, h( e11 ) ==> e20,
% 0.74/1.33 h( e11 ) ==> e21, h( e11 ) ==> e22, h( e11 ) ==> e23 }.
% 0.74/1.33 (210) {G2,W16,D3,L4,V0,M4} P(100,130);d(51);r(6) { j( e20 ) ==> e10, j( e20
% 0.74/1.33 ) ==> e12, j( e20 ) ==> e13, j( e20 ) ==> e14 }.
% 0.74/1.33 (213) {G3,W15,D3,L4,V0,M4} P(100,130);d(69);d(210);r(6) { j( e20 ) ==> e10
% 0.74/1.33 , j( e20 ) ==> e12, j( e20 ) ==> e13, e14 ==> e12 }.
% 0.74/1.33 (214) {G4,W12,D3,L3,V0,M3} E(210);d(213);q { j( e20 ) ==> e10, j( e20 ) ==>
% 0.74/1.33 e12, j( e20 ) ==> e13 }.
% 0.74/1.33 (220) {G2,W16,D3,L4,V0,M4} P(165,130);d(51);r(6) { h( e11 ) ==> e21, h( e11
% 0.74/1.33 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 0.74/1.33 (221) {G5,W8,D3,L2,V0,M2} P(214,130);d(57);r(7) { j( e20 ) ==> e10, j( e20
% 0.74/1.33 ) ==> e13 }.
% 0.74/1.33 (222) {G6,W7,D3,L2,V0,M2} P(214,130);d(63);d(221);r(7) { j( e20 ) ==> e10,
% 0.74/1.33 e13 ==> e11 }.
% 0.74/1.33 (241) {G7,W4,D3,L1,V0,M1} S(222);r(5) { j( e20 ) ==> e10 }.
% 0.74/1.33 (262) {G3,W16,D3,L4,V0,M4} S(169);d(220);r(13) { j( e24 ) ==> e11, h( e11 )
% 0.74/1.33 ==> e21, h( e11 ) ==> e22, h( e11 ) ==> e23 }.
% 0.74/1.33 (263) {G4,W16,D3,L4,V0,M4} P(262,111);d(76) { j( e24 ) ==> e11, h( e11 )
% 0.74/1.33 ==> e22, h( e11 ) ==> e23, h( e14 ) ==> e20 }.
% 0.74/1.33 (264) {G5,W12,D3,L3,V0,M3} P(262,111);d(82);d(263);r(14) { j( e24 ) ==> e11
% 0.74/1.33 , h( e11 ) ==> e23, h( e14 ) ==> e20 }.
% 0.74/1.33 (265) {G6,W11,D3,L3,V0,M3} P(262,111);d(88);d(263);d(264);r(15) { j( e24 )
% 0.74/1.33 ==> e11, h( e14 ) ==> e20, e23 ==> e22 }.
% 0.74/1.33 (274) {G7,W8,D3,L2,V0,M2} S(265);r(17) { j( e24 ) ==> e11, h( e14 ) ==> e20
% 0.74/1.33 }.
% 0.74/1.33 (285) {G8,W4,D3,L1,V0,M1} P(274,154);d(51);d(241);r(3) { h( e14 ) ==> e20
% 0.74/1.33 }.
% 0.74/1.33 (290) {G9,W3,D2,L1,V0,M1} P(285,164);d(241) { e14 ==> e10 }.
% 0.74/1.33 (291) {G10,W0,D0,L0,V0,M0} S(290);r(3) { }.
% 0.74/1.33
% 0.74/1.33
% 0.74/1.33 % SZS output end Refutation
% 0.74/1.33 found a proof!
% 0.74/1.33
% 0.74/1.33
% 0.74/1.33 Unprocessed initial clauses:
% 0.74/1.33
% 0.74/1.33 (293) {G0,W3,D2,L1,V0,M1} { ! e10 = e11 }.
% 0.74/1.33 (294) {G0,W3,D2,L1,V0,M1} { ! e10 = e12 }.
% 0.74/1.33 (295) {G0,W3,D2,L1,V0,M1} { ! e10 = e13 }.
% 0.74/1.33 (296) {G0,W3,D2,L1,V0,M1} { ! e10 = e14 }.
% 0.74/1.33 (297) {G0,W3,D2,L1,V0,M1} { ! e11 = e12 }.
% 0.74/1.33 (298) {G0,W3,D2,L1,V0,M1} { ! e11 = e13 }.
% 0.74/1.33 (299) {G0,W3,D2,L1,V0,M1} { ! e11 = e14 }.
% 0.74/1.33 (300) {G0,W3,D2,L1,V0,M1} { ! e12 = e13 }.
% 0.74/1.33 (301) {G0,W3,D2,L1,V0,M1} { ! e12 = e14 }.
% 0.74/1.33 (302) {G0,W3,D2,L1,V0,M1} { ! e13 = e14 }.
% 0.74/1.33 (303) {G0,W3,D2,L1,V0,M1} { ! e20 = e21 }.
% 0.74/1.33 (304) {G0,W3,D2,L1,V0,M1} { ! e20 = e22 }.
% 0.74/1.33 (305) {G0,W3,D2,L1,V0,M1} { ! e20 = e23 }.
% 0.74/1.33 (306) {G0,W3,D2,L1,V0,M1} { ! e20 = e24 }.
% 0.74/1.33 (307) {G0,W3,D2,L1,V0,M1} { ! e21 = e22 }.
% 0.74/1.33 (308) {G0,W3,D2,L1,V0,M1} { ! e21 = e23 }.
% 0.74/1.33 (309) {G0,W3,D2,L1,V0,M1} { ! e21 = e24 }.
% 0.74/1.33 (310) {G0,W3,D2,L1,V0,M1} { ! e22 = e23 }.
% 0.74/1.33 (311) {G0,W3,D2,L1,V0,M1} { ! e22 = e24 }.
% 0.74/1.33 (312) {G0,W3,D2,L1,V0,M1} { ! e23 = e24 }.
% 0.74/1.33 (313) {G0,W3,D2,L1,V0,M1} { ! e10 = e20 }.
% 0.74/1.33 (314) {G0,W3,D2,L1,V0,M1} { ! e10 = e21 }.
% 0.74/1.33 (315) {G0,W3,D2,L1,V0,M1} { ! e10 = e22 }.
% 0.74/1.33 (316) {G0,W3,D2,L1,V0,M1} { ! e10 = e23 }.
% 0.74/1.33 (317) {G0,W3,D2,L1,V0,M1} { ! e10 = e24 }.
% 0.74/1.33 (318) {G0,W3,D2,L1,V0,M1} { ! e11 = e20 }.
% 0.74/1.33 (319) {G0,W3,D2,L1,V0,M1} { ! e11 = e21 }.
% 0.74/1.33 (320) {G0,W3,D2,L1,V0,M1} { ! e11 = e22 }.
% 0.74/1.33 (321) {G0,W3,D2,L1,V0,M1} { ! e11 = e23 }.
% 0.74/1.33 (322) {G0,W3,D2,L1,V0,M1} { ! e11 = e24 }.
% 0.74/1.33 (323) {G0,W3,D2,L1,V0,M1} { ! e12 = e20 }.
% 0.74/1.33 (324) {G0,W3,D2,L1,V0,M1} { ! e12 = e21 }.
% 0.74/1.33 (325) {G0,W3,D2,L1,V0,M1} { ! e12 = e22 }.
% 0.74/1.33 (326) {G0,W3,D2,L1,V0,M1} { ! e12 = e23 }.
% 0.74/1.33 (327) {G0,W3,D2,L1,V0,M1} { ! e12 = e24 }.
% 0.74/1.33 (328) {G0,W3,D2,L1,V0,M1} { ! e13 = e20 }.
% 0.74/1.33 (329) {G0,W3,D2,L1,V0,M1} { ! e13 = e21 }.
% 0.74/1.33 (330) {G0,W3,D2,L1,V0,M1} { ! e13 = e22 }.
% 0.74/1.33 (331) {G0,W3,D2,L1,V0,M1} { ! e13 = e23 }.
% 0.74/1.33 (332) {G0,W3,D2,L1,V0,M1} { ! e13 = e24 }.
% 0.74/1.33 (333) {G0,W3,D2,L1,V0,M1} { ! e14 = e20 }.
% 0.74/1.33 (334) {G0,W3,D2,L1,V0,M1} { ! e14 = e21 }.
% 0.74/1.33 (335) {G0,W3,D2,L1,V0,M1} { ! e14 = e22 }.
% 0.74/1.33 (336) {G0,W3,D2,L1,V0,M1} { ! e14 = e23 }.
% 0.74/1.33 (337) {G0,W3,D2,L1,V0,M1} { ! e14 = e24 }.
% 0.74/1.33 (338) {G0,W5,D3,L1,V0,M1} { op1( e10, e10 ) = e10 }.
% 0.74/1.33 (339) {G0,W5,D3,L1,V0,M1} { op1( e10, e11 ) = e11 }.
% 0.74/1.33 (340) {G0,W5,D3,L1,V0,M1} { op1( e10, e12 ) = e12 }.
% 0.74/1.33 (341) {G0,W5,D3,L1,V0,M1} { op1( e10, e13 ) = e13 }.
% 0.74/1.33 (342) {G0,W5,D3,L1,V0,M1} { op1( e10, e14 ) = e14 }.
% 0.74/1.33 (343) {G0,W5,D3,L1,V0,M1} { op1( e11, e10 ) = e11 }.
% 0.74/1.33 (344) {G0,W5,D3,L1,V0,M1} { op1( e11, e11 ) = e14 }.
% 0.74/1.33 (345) {G0,W5,D3,L1,V0,M1} { op1( e11, e12 ) = e10 }.
% 0.74/1.33 (346) {G0,W5,D3,L1,V0,M1} { op1( e11, e13 ) = e12 }.
% 0.74/1.33 (347) {G0,W5,D3,L1,V0,M1} { op1( e11, e14 ) = e13 }.
% 0.74/1.33 (348) {G0,W5,D3,L1,V0,M1} { op1( e12, e10 ) = e12 }.
% 0.74/1.33 (349) {G0,W5,D3,L1,V0,M1} { op1( e12, e11 ) = e10 }.
% 0.74/1.33 (350) {G0,W5,D3,L1,V0,M1} { op1( e12, e12 ) = e13 }.
% 0.74/1.33 (351) {G0,W5,D3,L1,V0,M1} { op1( e12, e13 ) = e14 }.
% 0.74/1.33 (352) {G0,W5,D3,L1,V0,M1} { op1( e12, e14 ) = e11 }.
% 0.74/1.33 (353) {G0,W5,D3,L1,V0,M1} { op1( e13, e10 ) = e13 }.
% 0.74/1.33 (354) {G0,W5,D3,L1,V0,M1} { op1( e13, e11 ) = e12 }.
% 0.74/1.33 (355) {G0,W5,D3,L1,V0,M1} { op1( e13, e12 ) = e14 }.
% 0.74/1.33 (356) {G0,W5,D3,L1,V0,M1} { op1( e13, e13 ) = e11 }.
% 0.74/1.33 (357) {G0,W5,D3,L1,V0,M1} { op1( e13, e14 ) = e10 }.
% 0.74/1.33 (358) {G0,W5,D3,L1,V0,M1} { op1( e14, e10 ) = e14 }.
% 0.74/1.33 (359) {G0,W5,D3,L1,V0,M1} { op1( e14, e11 ) = e13 }.
% 0.74/1.33 (360) {G0,W5,D3,L1,V0,M1} { op1( e14, e12 ) = e11 }.
% 0.74/1.33 (361) {G0,W5,D3,L1,V0,M1} { op1( e14, e13 ) = e10 }.
% 0.74/1.33 (362) {G0,W5,D3,L1,V0,M1} { op1( e14, e14 ) = e12 }.
% 0.74/1.33 (363) {G0,W5,D3,L1,V0,M1} { op2( e20, e20 ) = e20 }.
% 0.74/1.33 (364) {G0,W5,D3,L1,V0,M1} { op2( e20, e21 ) = e21 }.
% 0.74/1.33 (365) {G0,W5,D3,L1,V0,M1} { op2( e20, e22 ) = e22 }.
% 0.74/1.33 (366) {G0,W5,D3,L1,V0,M1} { op2( e20, e23 ) = e23 }.
% 0.74/1.33 (367) {G0,W5,D3,L1,V0,M1} { op2( e20, e24 ) = e24 }.
% 0.74/1.33 (368) {G0,W5,D3,L1,V0,M1} { op2( e21, e20 ) = e21 }.
% 0.74/1.33 (369) {G0,W5,D3,L1,V0,M1} { op2( e21, e21 ) = e20 }.
% 0.74/1.33 (370) {G0,W5,D3,L1,V0,M1} { op2( e21, e22 ) = e23 }.
% 0.74/1.33 (371) {G0,W5,D3,L1,V0,M1} { op2( e21, e23 ) = e24 }.
% 0.74/1.33 (372) {G0,W5,D3,L1,V0,M1} { op2( e21, e24 ) = e22 }.
% 0.74/1.33 (373) {G0,W5,D3,L1,V0,M1} { op2( e22, e20 ) = e22 }.
% 0.74/1.33 (374) {G0,W5,D3,L1,V0,M1} { op2( e22, e21 ) = e24 }.
% 0.74/1.33 (375) {G0,W5,D3,L1,V0,M1} { op2( e22, e22 ) = e20 }.
% 0.74/1.33 (376) {G0,W5,D3,L1,V0,M1} { op2( e22, e23 ) = e21 }.
% 0.74/1.33 (377) {G0,W5,D3,L1,V0,M1} { op2( e22, e24 ) = e23 }.
% 0.74/1.33 (378) {G0,W5,D3,L1,V0,M1} { op2( e23, e20 ) = e23 }.
% 0.74/1.33 (379) {G0,W5,D3,L1,V0,M1} { op2( e23, e21 ) = e22 }.
% 0.74/1.33 (380) {G0,W5,D3,L1,V0,M1} { op2( e23, e22 ) = e24 }.
% 0.74/1.33 (381) {G0,W5,D3,L1,V0,M1} { op2( e23, e23 ) = e20 }.
% 0.74/1.33 (382) {G0,W5,D3,L1,V0,M1} { op2( e23, e24 ) = e21 }.
% 0.74/1.33 (383) {G0,W5,D3,L1,V0,M1} { op2( e24, e20 ) = e24 }.
% 0.74/1.33 (384) {G0,W5,D3,L1,V0,M1} { op2( e24, e21 ) = e23 }.
% 0.74/1.33 (385) {G0,W5,D3,L1,V0,M1} { op2( e24, e22 ) = e21 }.
% 0.74/1.33 (386) {G0,W5,D3,L1,V0,M1} { op2( e24, e23 ) = e22 }.
% 0.74/1.33 (387) {G0,W5,D3,L1,V0,M1} { op2( e24, e24 ) = e20 }.
% 0.74/1.33 (388) {G0,W20,D3,L5,V0,M5} { h( e10 ) = e20, h( e10 ) = e21, h( e10 ) =
% 0.74/1.33 e22, h( e10 ) = e23, h( e10 ) = e24 }.
% 0.74/1.33 (389) {G0,W20,D3,L5,V0,M5} { h( e11 ) = e20, h( e11 ) = e21, h( e11 ) =
% 0.74/1.33 e22, h( e11 ) = e23, h( e11 ) = e24 }.
% 0.74/1.33 (390) {G0,W20,D3,L5,V0,M5} { h( e12 ) = e20, h( e12 ) = e21, h( e12 ) =
% 0.74/1.33 e22, h( e12 ) = e23, h( e12 ) = e24 }.
% 0.74/1.33 (391) {G0,W20,D3,L5,V0,M5} { h( e13 ) = e20, h( e13 ) = e21, h( e13 ) =
% 0.74/1.33 e22, h( e13 ) = e23, h( e13 ) = e24 }.
% 0.74/1.33 (392) {G0,W20,D3,L5,V0,M5} { h( e14 ) = e20, h( e14 ) = e21, h( e14 ) =
% 0.74/1.33 e22, h( e14 ) = e23, h( e14 ) = e24 }.
% 0.74/1.33 (393) {G0,W20,D3,L5,V0,M5} { j( e20 ) = e10, j( e20 ) = e11, j( e20 ) =
% 0.74/1.33 e12, j( e20 ) = e13, j( e20 ) = e14 }.
% 0.74/1.33 (394) {G0,W20,D3,L5,V0,M5} { j( e21 ) = e10, j( e21 ) = e11, j( e21 ) =
% 0.74/1.33 e12, j( e21 ) = e13, j( e21 ) = e14 }.
% 0.74/1.33 (395) {G0,W20,D3,L5,V0,M5} { j( e22 ) = e10, j( e22 ) = e11, j( e22 ) =
% 0.74/1.33 e12, j( e22 ) = e13, j( e22 ) = e14 }.
% 0.74/1.33 (396) {G0,W20,D3,L5,V0,M5} { j( e23 ) = e10, j( e23 ) = e11, j( e23 ) =
% 0.74/1.33 e12, j( e23 ) = e13, j( e23 ) = e14 }.
% 0.74/1.33 (397) {G0,W20,D3,L5,V0,M5} { j( e24 ) = e10, j( e24 ) = e11, j( e24 ) =
% 0.74/1.33 e12, j( e24 ) = e13, j( e24 ) = e14 }.
% 0.74/1.33 (398) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e10 ) ) = op2( h( e10 ), h( e10
% 0.74/1.33 ) ) }.
% 0.74/1.33 (399) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e11 ) ) = op2( h( e10 ), h( e11
% 0.74/1.33 ) ) }.
% 0.74/1.33 (400) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e12 ) ) = op2( h( e10 ), h( e12
% 0.74/1.33 ) ) }.
% 0.74/1.33 (401) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e13 ) ) = op2( h( e10 ), h( e13
% 0.74/1.33 ) ) }.
% 0.74/1.33 (402) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e14 ) ) = op2( h( e10 ), h( e14
% 0.74/1.33 ) ) }.
% 0.74/1.33 (403) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e10 ) ) = op2( h( e11 ), h( e10
% 0.74/1.33 ) ) }.
% 0.74/1.33 (404) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e11 ) ) = op2( h( e11 ), h( e11
% 0.74/1.33 ) ) }.
% 0.74/1.33 (405) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e12 ) ) = op2( h( e11 ), h( e12
% 0.74/1.33 ) ) }.
% 0.74/1.33 (406) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e13 ) ) = op2( h( e11 ), h( e13
% 0.74/1.33 ) ) }.
% 0.74/1.33 (407) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e14 ) ) = op2( h( e11 ), h( e14
% 0.74/1.33 ) ) }.
% 0.74/1.33 (408) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e10 ) ) = op2( h( e12 ), h( e10
% 0.74/1.33 ) ) }.
% 0.74/1.33 (409) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e11 ) ) = op2( h( e12 ), h( e11
% 0.74/1.33 ) ) }.
% 0.74/1.33 (410) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e12 ) ) = op2( h( e12 ), h( e12
% 0.74/1.33 ) ) }.
% 0.74/1.33 (411) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e13 ) ) = op2( h( e12 ), h( e13
% 0.74/1.33 ) ) }.
% 0.74/1.33 (412) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e14 ) ) = op2( h( e12 ), h( e14
% 0.74/1.33 ) ) }.
% 0.74/1.33 (413) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e10 ) ) = op2( h( e13 ), h( e10
% 0.74/1.33 ) ) }.
% 0.74/1.33 (414) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e11 ) ) = op2( h( e13 ), h( e11
% 0.74/1.33 ) ) }.
% 0.74/1.33 (415) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e12 ) ) = op2( h( e13 ), h( e12
% 0.74/1.33 ) ) }.
% 0.74/1.33 (416) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e13 ) ) = op2( h( e13 ), h( e13
% 0.74/1.33 ) ) }.
% 0.74/1.33 (417) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e14 ) ) = op2( h( e13 ), h( e14
% 0.74/1.33 ) ) }.
% 0.74/1.33 (418) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e10 ) ) = op2( h( e14 ), h( e10
% 0.74/1.33 ) ) }.
% 0.74/1.33 (419) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e11 ) ) = op2( h( e14 ), h( e11
% 0.74/1.33 ) ) }.
% 0.74/1.33 (420) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e12 ) ) = op2( h( e14 ), h( e12
% 0.74/1.33 ) ) }.
% 0.74/1.33 (421) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e13 ) ) = op2( h( e14 ), h( e13
% 0.74/1.33 ) ) }.
% 0.74/1.33 (422) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e14 ) ) = op2( h( e14 ), h( e14
% 0.74/1.33 ) ) }.
% 0.74/1.33 (423) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e20 ) ) = op1( j( e20 ), j( e20
% 0.74/1.33 ) ) }.
% 0.74/1.33 (424) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e21 ) ) = op1( j( e20 ), j( e21
% 0.74/1.33 ) ) }.
% 0.74/1.33 (425) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e22 ) ) = op1( j( e20 ), j( e22
% 0.74/1.33 ) ) }.
% 0.74/1.33 (426) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e23 ) ) = op1( j( e20 ), j( e23
% 0.74/1.33 ) ) }.
% 0.74/1.33 (427) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e24 ) ) = op1( j( e20 ), j( e24
% 0.74/1.33 ) ) }.
% 0.74/1.33 (428) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e20 ) ) = op1( j( e21 ), j( e20
% 0.74/1.33 ) ) }.
% 0.74/1.33 (429) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e21 ) ) = op1( j( e21 ), j( e21
% 0.74/1.33 ) ) }.
% 0.74/1.33 (430) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e22 ) ) = op1( j( e21 ), j( e22
% 0.74/1.33 ) ) }.
% 0.74/1.33 (431) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e23 ) ) = op1( j( e21 ), j( e23
% 0.74/1.33 ) ) }.
% 0.74/1.33 (432) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e24 ) ) = op1( j( e21 ), j( e24
% 0.74/1.33 ) ) }.
% 0.74/1.33 (433) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e20 ) ) = op1( j( e22 ), j( e20
% 0.74/1.33 ) ) }.
% 0.74/1.33 (434) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e21 ) ) = op1( j( e22 ), j( e21
% 0.74/1.33 ) ) }.
% 0.74/1.33 (435) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e22 ) ) = op1( j( e22 ), j( e22
% 0.74/1.33 ) ) }.
% 0.74/1.33 (436) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e23 ) ) = op1( j( e22 ), j( e23
% 0.74/1.33 ) ) }.
% 0.74/1.33 (437) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e24 ) ) = op1( j( e22 ), j( e24
% 0.74/1.33 ) ) }.
% 0.74/1.33 (438) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e20 ) ) = op1( j( e23 ), j( e20
% 0.74/1.33 ) ) }.
% 0.74/1.33 (439) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e21 ) ) = op1( j( e23 ), j( e21
% 0.74/1.33 ) ) }.
% 0.74/1.33 (440) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e22 ) ) = op1( j( e23 ), j( e22
% 0.74/1.33 ) ) }.
% 0.74/1.33 (441) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e23 ) ) = op1( j( e23 ), j( e23
% 0.74/1.33 ) ) }.
% 0.74/1.33 (442) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e24 ) ) = op1( j( e23 ), j( e24
% 0.74/1.33 ) ) }.
% 0.74/1.33 (443) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e20 ) ) = op1( j( e24 ), j( e20
% 0.74/1.33 ) ) }.
% 0.74/1.33 (444) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e21 ) ) = op1( j( e24 ), j( e21
% 0.74/1.33 ) ) }.
% 0.74/1.33 (445) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e22 ) ) = op1( j( e24 ), j( e22
% 0.74/1.33 ) ) }.
% 0.74/1.33 (446) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e23 ) ) = op1( j( e24 ), j( e23
% 0.74/1.33 ) ) }.
% 0.74/1.33 (447) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e24 ) ) = op1( j( e24 ), j( e24
% 0.74/1.33 ) ) }.
% 0.74/1.33 (448) {G0,W5,D4,L1,V0,M1} { h( j( e20 ) ) = e20 }.
% 0.74/1.33 (449) {G0,W5,D4,L1,V0,M1} { h( j( e21 ) ) = e21 }.
% 0.74/1.33 (450) {G0,W5,D4,L1,V0,M1} { h( j( e22 ) ) = e22 }.
% 0.74/1.33 (451) {G0,W5,D4,L1,V0,M1} { h( j( e23 ) ) = e23 }.
% 0.74/1.33 (452) {G0,W5,D4,L1,V0,M1} { h( j( e24 ) ) = e24 }.
% 0.74/1.33 (453) {G0,W5,D4,L1,V0,M1} { j( h( e10 ) ) = e10 }.
% 0.74/1.33 (454) {G0,W5,D4,L1,V0,M1} { j( h( e11 ) ) = e11 }.
% 0.74/1.33 (455) {G0,W5,D4,L1,V0,M1} { j( h( e12 ) ) = e12 }.
% 0.74/1.33 (456) {G0,W5,D4,L1,V0,M1} { j( h( e13 ) ) = e13 }.
% 0.74/1.33 (457) {G0,W5,D4,L1,V0,M1} { j( h( e14 ) ) = e14 }.
% 0.74/1.33
% 0.74/1.33
% 0.74/1.33 Total Proof:
% 0.74/1.33
% 0.74/1.33 eqswap: (461) {G0,W3,D2,L1,V0,M1} { ! e14 = e10 }.
% 0.74/1.33 parent0[0]: (296) {G0,W3,D2,L1,V0,M1} { ! e10 = e14 }.
% 0.74/1.33 substitution0:
% 0.74/1.33 end
% 0.74/1.33
% 0.74/1.33 subsumption: (3) {G0,W3,D2,L1,V0,M1} I { ! e14 ==> e10 }.
% 0.74/1.33 parent0: (461) {G0,W3,D2,L1,V0,M1} { ! e14 = e10 }.
% 0.74/1.33 substitution0:
% 0.74/1.33 end
% 0.74/1.33 permutation0:
% 0.74/1.33 0 ==> 0
% 0.74/1.33 end
% 0.74/1.33
% 0.74/1.33 eqswap: (467) {G0,W3,D2,L1,V0,M1} { ! e13 = e11 }.
% 0.74/1.33 parent0[0]: (298) {G0,W3,D2,L1,V0,M1} { ! e11 = e13 }.
% 0.74/1.33 substitution0:
% 0.74/1.33 end
% 0.74/1.33
% 0.74/1.33 subsumption: (5) {G0,W3,D2,L1,V0,M1} I { ! e13 ==> e11 }.
% 0.74/1.33 parent0: (467) {G0,W3,D2,L1,V0,M1} { ! e13 = e11 }.
% 0.74/1.33 substitution0:
% 0.74/1.33 end
% 0.74/1.33 permutation0:
% 0.74/1.33 0 ==> 0
% 0.74/1.33 end
% 0.74/1.33
% 0.74/1.33 eqswap: (474) {G0,W3,D2,L1,V0,M1} { ! e14 = e11 }.
% 0.74/1.33 parent0[0]: (299) {G0,W3,D2,L1,V0,M1} { ! e11 = e14 }.
% 0.74/1.33 substitution0:
% 0.74/1.33 end
% 0.74/1.33
% 0.74/1.33 subsumption: (6) {G0,W3,D2,L1,V0,M1} I { ! e14 ==> e11 }.
% 0.74/1.33 parent0: (474) {G0,W3,D2,L1,V0,M1} { ! e14 = e11 }.
% 0.74/1.33 substitution0:
% 0.74/1.33 end
% 0.74/1.33 permutation0:
% 0.74/1.33 0 ==> 0
% 0.74/1.33 end
% 0.74/1.33
% 0.74/1.33 eqswap: (482) {G0,W3,D2,L1,V0,M1} { ! e13 = e12 }.
% 0.74/1.33 parent0[0]: (300) {G0,W3,D2,L1,V0,M1} { ! e12 = e13 }.
% 0.74/1.33 substitution0:
% 0.74/1.33 end
% 0.74/1.33
% 0.74/1.33 subsumption: (7) {G0,W3,D2,L1,V0,M1} I { ! e13 ==> e12 }.
% 0.74/1.33 parent0: (482) {G0,W3,D2,L1,V0,M1} { ! e13 = e12 }.
% 0.74/1.33 substitution0:
% 0.74/1.33 end
% 0.74/1.33 permutation0:
% 0.74/1.33 0 ==> 0
% 0.74/1.33 end
% 0.74/1.33
% 0.74/1.33 eqswap: (496) {G0,W3,D2,L1,V0,M1} { ! e24 = e20 }.
% 0.74/1.33 parent0[0]: (306) {G0,W3,D2,L1,V0,M1} { ! e20 = e24 }.
% 0.74/1.33 substitution0:
% 0.74/1.33 end
% 0.74/1.33
% 0.74/1.33 subsumption: (13) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e20 }.
% 0.74/1.33 parent0: (496) {G0,W3,D2,L1,V0,M1} { ! e24 = e20 }.
% 0.74/1.33 substitution0:
% 0.74/1.33 end
% 0.74/1.33 permutation0:
% 0.74/1.33 0 ==> 0
% 0.74/1.33 end
% 0.74/1.33
% 0.74/1.33 eqswap: (511) {G0,W3,D2,L1,V0,M1} { ! e22 = e21 }.
% 0.74/1.33 parent0[0]: (307) {G0,W3,D2,L1,V0,M1} { ! e21 = e22 }.
% 0.74/1.33 substitution0:
% 0.74/1.33 end
% 0.74/1.33
% 0.74/1.33 subsumption: (14) {G0,W3,D2,L1,V0,M1} I { ! e22 ==> e21 }.
% 0.74/1.33 parent0: (511) {G0,W3,D2,L1,V0,M1} { ! e22 = e21 }.
% 0.74/1.33 substitution0:
% 0.74/1.33 end
% 0.74/1.33 permutation0:
% 0.74/1.33 0 ==> 0
% 0.74/1.33 end
% 0.74/1.33
% 0.74/1.33 eqswap: (527) {G0,W3,D2,L1,V0,M1} { ! e23 = e21 }.
% 0.74/1.33 parent0[0]: (308) {G0,W3,D2,L1,V0,M1} { ! e21 = e23 }.
% 0.74/1.33 substitution0:
% 0.74/1.33 end
% 0.74/1.33
% 0.74/1.33 subsumption: (15) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e21 }.
% 0.74/1.33 parent0: (527) {G0,W3,D2,L1,V0,M1} { ! e23 = e21 }.
% 0.74/1.33 substitution0:
% 0.74/1.33 end
% 0.74/1.33 permutation0:
% 0.74/1.33 0 ==> 0
% 0.74/1.33 end
% 0.74/1.33
% 0.74/1.33 *** allocated 33750 integers for clauses
% 0.74/1.33 eqswap: (545) {G0,W3,D2,L1,V0,M1} { ! e23 = e22 }.
% 0.74/1.33 parent0[0]: (310) {G0,W3,D2,L1,V0,M1} { ! e22 = e23 }.
% 0.74/1.34 substitution0:
% 0.74/1.34 end
% 0.74/1.34
% 0.74/1.34 subsumption: (17) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e22 }.
% 0.74/1.34 parent0: (545) {G0,W3,D2,L1,V0,M1} { ! e23 = e22 }.
% 0.74/1.34 substitution0:
% 0.74/1.34 end
% 0.74/1.34 permutation0:
% 0.74/1.34 0 ==> 0
% 0.74/1.34 end
% 0.74/1.34
% 0.74/1.34 subsumption: (51) {G0,W5,D3,L1,V0,M1} I { op1( e11, e11 ) ==> e14 }.
% 0.74/1.34 parent0: (344) {G0,W5,D3,L1,V0,M1} { op1( e11, e11 ) = e14 }.
% 0.74/1.34 substitution0:
% 0.74/1.34 end
% 0.74/1.34 permutation0:
% 0.74/1.34 0 ==> 0
% 0.74/1.34 end
% 0.74/1.34
% 0.74/1.34 subsumption: (57) {G0,W5,D3,L1,V0,M1} I { op1( e12, e12 ) ==> e13 }.
% 0.74/1.34 parent0: (350) {G0,W5,D3,L1,V0,M1} { op1( e12, e12 ) = e13 }.
% 0.74/1.34 substitution0:
% 0.74/1.34 end
% 0.74/1.34 permutation0:
% 0.74/1.34 0 ==> 0
% 0.74/1.34 end
% 0.74/1.34
% 0.74/1.34 subsumption: (63) {G0,W5,D3,L1,V0,M1} I { op1( e13, e13 ) ==> e11 }.
% 0.74/1.34 parent0: (356) {G0,W5,D3,L1,V0,M1} { op1( e13, e13 ) = e11 }.
% 0.74/1.34 substitution0:
% 0.74/1.34 end
% 0.74/1.34 permutation0:
% 0.74/1.34 0 ==> 0
% 0.74/1.34 end
% 0.74/1.34
% 0.74/1.34 subsumption: (69) {G0,W5,D3,L1,V0,M1} I { op1( e14, e14 ) ==> e12 }.
% 0.74/1.34 parent0: (362) {G0,W5,D3,L1,V0,M1} { op1( e14, e14 ) = e12 }.
% 0.74/1.34 substitution0:
% 0.74/1.34 end
% 0.74/1.34 permutation0:
% 0.74/1.34 0 ==> 0
% 0.74/1.34 end
% 0.74/1.34
% 0.74/1.34 subsumption: (70) {G0,W5,D3,L1,V0,M1} I { op2( e20, e20 ) ==> e20 }.
% 0.74/1.34 parent0: (363) {G0,W5,D3,L1,V0,M1} { op2( e20, e20 ) = e20 }.
% 0.74/1.34 substitution0:
% 0.74/1.34 end
% 0.74/1.34 permutation0:
% 0.74/1.34 0 ==> 0
% 0.74/1.34 end
% 0.74/1.34
% 0.74/1.34 subsumption: (76) {G0,W5,D3,L1,V0,M1} I { op2( e21, e21 ) ==> e20 }.
% 0.74/1.34 parent0: (369) {G0,W5,D3,L1,V0,M1} { op2( e21, e21 ) = e20 }.
% 0.74/1.34 substitution0:
% 0.74/1.34 end
% 0.74/1.34 permutation0:
% 0.74/1.34 0 ==> 0
% 0.74/1.34 end
% 0.74/1.34
% 0.74/1.34 subsumption: (82) {G0,W5,D3,L1,V0,M1} I { op2( e22, e22 ) ==> e20 }.
% 0.74/1.34 parent0: (375) {G0,W5,D3,L1,V0,M1} { op2( e22, e22 ) = e20 }.
% 0.74/1.34 substitution0:
% 0.74/1.34 end
% 0.74/1.34 permutation0:
% 0.74/1.34 0 ==> 0
% 0.74/1.34 end
% 0.74/1.34
% 0.74/1.34 *** allocated 50625 integers for clauses
% 0.74/1.34 subsumption: (88) {G0,W5,D3,L1,V0,M1} I { op2( e23, e23 ) ==> e20 }.
% 0.74/1.34 parent0: (381) {G0,W5,D3,L1,V0,M1} { op2( e23, e23 ) = e20 }.
% 0.74/1.34 substitution0:
% 0.74/1.34 end
% 0.74/1.34 permutation0:
% 0.74/1.34 0 ==> 0
% 0.74/1.34 end
% 0.74/1.34
% 0.74/1.34 *** allocated 15000 integers for termspace/termends
% 0.74/1.34 subsumption: (94) {G0,W5,D3,L1,V0,M1} I { op2( e24, e24 ) ==> e20 }.
% 0.74/1.34 parent0: (387) {G0,W5,D3,L1,V0,M1} { op2( e24, e24 ) = e20 }.
% 0.74/1.34 substitution0:
% 0.74/1.34 end
% 0.74/1.34 permutation0:
% 0.74/1.34 0 ==> 0
% 0.74/1.34 end
% 0.74/1.34
% 0.74/1.34 subsumption: (96) {G0,W20,D3,L5,V0,M5} I { h( e11 ) ==> e20, h( e11 ) ==>
% 0.74/1.34 e21, h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 0.74/1.35 parent0: (389) {G0,W20,D3,L5,V0,M5} { h( e11 ) = e20, h( e11 ) = e21, h(
% 0.74/1.35 e11 ) = e22, h( e11 ) = e23, h( e11 ) = e24 }.
% 0.74/1.35 substitution0:
% 0.74/1.35 end
% 0.74/1.35 permutation0:
% 0.74/1.35 0 ==> 0
% 0.74/1.35 1 ==> 1
% 0.74/1.35 2 ==> 2
% 0.74/1.35 3 ==> 3
% 0.74/1.35 4 ==> 4
% 0.74/1.35 end
% 0.74/1.35
% 0.74/1.35 *** allocated 22500 integers for termspace/termends
% 0.74/1.35 subsumption: (100) {G0,W20,D3,L5,V0,M5} I { j( e20 ) ==> e10, j( e20 ) ==>
% 0.74/1.35 e11, j( e20 ) ==> e12, j( e20 ) ==> e13, j( e20 ) ==> e14 }.
% 0.74/1.35 parent0: (393) {G0,W20,D3,L5,V0,M5} { j( e20 ) = e10, j( e20 ) = e11, j(
% 0.74/1.35 e20 ) = e12, j( e20 ) = e13, j( e20 ) = e14 }.
% 0.74/1.35 substitution0:
% 0.74/1.35 end
% 0.74/1.35 permutation0:
% 0.74/1.35 0 ==> 0
% 0.74/1.35 1 ==> 1
% 0.74/1.35 2 ==> 2
% 0.74/1.35 3 ==> 3
% 0.74/1.35 4 ==> 4
% 0.74/1.35 end
% 0.74/1.35
% 0.74/1.35 *** allocated 75937 integers for clauses
% 0.74/1.35 *** allocated 33750 integers for termspace/termends
% 0.74/1.35 paramod: (2169) {G1,W8,D4,L1,V0,M1} { h( e14 ) = op2( h( e11 ), h( e11 ) )
% 0.74/1.35 }.
% 0.74/1.35 parent0[0]: (51) {G0,W5,D3,L1,V0,M1} I { op1( e11, e11 ) ==> e14 }.
% 0.74/1.35 parent1[0; 2]: (404) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e11 ) ) = op2( h
% 0.74/1.35 ( e11 ), h( e11 ) ) }.
% 0.74/1.35 substitution0:
% 0.74/1.35 end
% 0.74/1.35 substitution1:
% 0.74/1.35 end
% 0.74/1.35
% 0.74/1.35 eqswap: (2170) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e11 ) ) = h( e14 )
% 0.74/1.35 }.
% 0.74/1.35 parent0[0]: (2169) {G1,W8,D4,L1,V0,M1} { h( e14 ) = op2( h( e11 ), h( e11
% 0.74/1.35 ) ) }.
% 0.74/1.35 substitution0:
% 0.74/1.35 end
% 0.74/1.35
% 0.74/1.35 subsumption: (111) {G1,W8,D4,L1,V0,M1} I;d(51) { op2( h( e11 ), h( e11 ) )
% 0.74/1.35 ==> h( e14 ) }.
% 0.74/1.35 parent0: (2170) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e11 ) ) = h( e14 )
% 0.74/1.35 }.
% 0.74/1.35 substitution0:
% 0.74/1.35 end
% 0.74/1.35 permutation0:
% 0.74/1.35 0 ==> 0
% 0.74/1.35 end
% 0.74/1.35
% 0.74/1.35 paramod: (2735) {G1,W8,D4,L1,V0,M1} { j( e20 ) = op1( j( e20 ), j( e20 ) )
% 0.74/1.35 }.
% 0.74/1.35 parent0[0]: (70) {G0,W5,D3,L1,V0,M1} I { op2( e20, e20 ) ==> e20 }.
% 0.74/1.35 parent1[0; 2]: (423) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e20 ) ) = op1( j
% 0.74/1.35 ( e20 ), j( e20 ) ) }.
% 0.74/1.35 substitution0:
% 0.74/1.35 end
% 0.74/1.35 substitution1:
% 0.74/1.35 end
% 0.74/1.35
% 0.74/1.35 eqswap: (2736) {G1,W8,D4,L1,V0,M1} { op1( j( e20 ), j( e20 ) ) = j( e20 )
% 0.74/1.35 }.
% 0.74/1.35 parent0[0]: (2735) {G1,W8,D4,L1,V0,M1} { j( e20 ) = op1( j( e20 ), j( e20
% 0.74/1.35 ) ) }.
% 0.74/1.35 substitution0:
% 0.74/1.35 end
% 0.74/1.35
% 0.74/1.35 subsumption: (130) {G1,W8,D4,L1,V0,M1} I;d(70) { op1( j( e20 ), j( e20 ) )
% 0.74/1.35 ==> j( e20 ) }.
% 0.74/1.35 parent0: (2736) {G1,W8,D4,L1,V0,M1} { op1( j( e20 ), j( e20 ) ) = j( e20 )
% 1.47/1.90 }.
% 1.47/1.90 substitution0:
% 1.47/1.90 end
% 1.47/1.90 permutation0:
% 1.47/1.90 0 ==> 0
% 1.47/1.90 end
% 1.47/1.90
% 1.47/1.90 *** allocated 113905 integers for clauses
% 1.47/1.90 *** allocated 50625 integers for termspace/termends
% 1.47/1.90 paramod: (3349) {G1,W8,D4,L1,V0,M1} { j( e20 ) = op1( j( e24 ), j( e24 ) )
% 1.47/1.90 }.
% 1.47/1.90 parent0[0]: (94) {G0,W5,D3,L1,V0,M1} I { op2( e24, e24 ) ==> e20 }.
% 1.47/1.90 parent1[0; 2]: (447) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e24 ) ) = op1( j
% 1.47/1.90 ( e24 ), j( e24 ) ) }.
% 1.47/1.90 substitution0:
% 1.47/1.90 end
% 1.47/1.90 substitution1:
% 1.47/1.90 end
% 1.47/1.90
% 1.47/1.90 eqswap: (3350) {G1,W8,D4,L1,V0,M1} { op1( j( e24 ), j( e24 ) ) = j( e20 )
% 1.47/1.90 }.
% 1.47/1.90 parent0[0]: (3349) {G1,W8,D4,L1,V0,M1} { j( e20 ) = op1( j( e24 ), j( e24
% 1.47/1.90 ) ) }.
% 1.47/1.90 substitution0:
% 1.47/1.90 end
% 1.47/1.90
% 1.47/1.90 subsumption: (154) {G1,W8,D4,L1,V0,M1} I;d(94) { op1( j( e24 ), j( e24 ) )
% 1.47/1.90 ==> j( e20 ) }.
% 1.47/1.90 parent0: (3350) {G1,W8,D4,L1,V0,M1} { op1( j( e24 ), j( e24 ) ) = j( e20 )
% 1.47/1.90 }.
% 1.47/1.90 substitution0:
% 1.47/1.90 end
% 1.47/1.90 permutation0:
% 1.47/1.90 0 ==> 0
% 1.47/1.90 end
% 1.47/1.90
% 1.47/1.90 subsumption: (161) {G0,W5,D4,L1,V0,M1} I { j( h( e11 ) ) ==> e11 }.
% 1.47/1.90 parent0: (454) {G0,W5,D4,L1,V0,M1} { j( h( e11 ) ) = e11 }.
% 1.47/1.90 substitution0:
% 1.47/1.90 end
% 1.47/1.90 permutation0:
% 1.47/1.90 0 ==> 0
% 1.47/1.90 end
% 1.47/1.90
% 1.47/1.90 *** allocated 75937 integers for termspace/termends
% 1.47/1.90 subsumption: (164) {G0,W5,D4,L1,V0,M1} I { j( h( e14 ) ) ==> e14 }.
% 1.47/1.90 parent0: (457) {G0,W5,D4,L1,V0,M1} { j( h( e14 ) ) = e14 }.
% 1.47/1.90 substitution0:
% 1.47/1.90 end
% 1.47/1.90 permutation0:
% 1.47/1.90 0 ==> 0
% 1.47/1.90 end
% 1.47/1.90
% 1.47/1.90 *** allocated 170857 integers for clauses
% 1.47/1.90 *** allocated 113905 integers for termspace/termends
% 1.47/1.90 *** allocated 170857 integers for termspace/termends
% 1.47/1.90 *** allocated 15000 integers for justifications
% 1.47/1.90 *** allocated 22500 integers for justifications
% 1.47/1.90 eqswap: (4279) {G0,W20,D3,L5,V0,M5} { e21 ==> h( e11 ), h( e11 ) ==> e20,
% 1.47/1.90 h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 1.47/1.90 parent0[1]: (96) {G0,W20,D3,L5,V0,M5} I { h( e11 ) ==> e20, h( e11 ) ==>
% 1.47/1.90 e21, h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 1.47/1.90 substitution0:
% 1.47/1.90 end
% 1.47/1.90
% 1.47/1.90 eqswap: (4309) {G0,W5,D4,L1,V0,M1} { e11 ==> j( h( e11 ) ) }.
% 1.47/1.90 parent0[0]: (161) {G0,W5,D4,L1,V0,M1} I { j( h( e11 ) ) ==> e11 }.
% 1.47/1.90 substitution0:
% 1.47/1.90 end
% 1.47/1.90
% 1.47/1.90 paramod: (8662) {G1,W20,D3,L5,V0,M5} { e11 ==> j( e20 ), e21 ==> h( e11 )
% 1.47/1.90 , h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 1.47/1.90 parent0[1]: (4279) {G0,W20,D3,L5,V0,M5} { e21 ==> h( e11 ), h( e11 ) ==>
% 1.47/1.90 e20, h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 1.47/1.90 parent1[0; 3]: (4309) {G0,W5,D4,L1,V0,M1} { e11 ==> j( h( e11 ) ) }.
% 1.47/1.90 substitution0:
% 1.47/1.90 end
% 1.47/1.90 substitution1:
% 1.47/1.90 end
% 1.47/1.90
% 1.47/1.90 eqswap: (8750) {G1,W20,D3,L5,V0,M5} { e24 ==> h( e11 ), e11 ==> j( e20 ),
% 1.47/1.90 e21 ==> h( e11 ), h( e11 ) ==> e22, h( e11 ) ==> e23 }.
% 1.47/1.90 parent0[4]: (8662) {G1,W20,D3,L5,V0,M5} { e11 ==> j( e20 ), e21 ==> h( e11
% 1.47/1.90 ), h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 1.47/1.90 substitution0:
% 1.47/1.90 end
% 1.47/1.90
% 1.47/1.90 eqswap: (8754) {G1,W20,D3,L5,V0,M5} { e23 ==> h( e11 ), e24 ==> h( e11 ),
% 1.47/1.90 e11 ==> j( e20 ), e21 ==> h( e11 ), h( e11 ) ==> e22 }.
% 1.47/1.90 parent0[4]: (8750) {G1,W20,D3,L5,V0,M5} { e24 ==> h( e11 ), e11 ==> j( e20
% 1.47/1.90 ), e21 ==> h( e11 ), h( e11 ) ==> e22, h( e11 ) ==> e23 }.
% 1.47/1.90 substitution0:
% 1.47/1.90 end
% 1.47/1.90
% 1.47/1.90 eqswap: (8757) {G1,W20,D3,L5,V0,M5} { e22 ==> h( e11 ), e23 ==> h( e11 ),
% 1.47/1.90 e24 ==> h( e11 ), e11 ==> j( e20 ), e21 ==> h( e11 ) }.
% 1.47/1.90 parent0[4]: (8754) {G1,W20,D3,L5,V0,M5} { e23 ==> h( e11 ), e24 ==> h( e11
% 1.47/1.90 ), e11 ==> j( e20 ), e21 ==> h( e11 ), h( e11 ) ==> e22 }.
% 1.47/1.90 substitution0:
% 1.47/1.90 end
% 1.47/1.90
% 1.47/1.90 eqswap: (8760) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e21, e22 ==> h( e11 ),
% 1.47/1.90 e23 ==> h( e11 ), e24 ==> h( e11 ), e11 ==> j( e20 ) }.
% 1.47/1.90 parent0[4]: (8757) {G1,W20,D3,L5,V0,M5} { e22 ==> h( e11 ), e23 ==> h( e11
% 1.47/1.90 ), e24 ==> h( e11 ), e11 ==> j( e20 ), e21 ==> h( e11 ) }.
% 1.47/1.90 substitution0:
% 1.47/1.90 end
% 1.47/1.90
% 1.47/1.90 eqswap: (8763) {G1,W20,D3,L5,V0,M5} { j( e20 ) ==> e11, h( e11 ) ==> e21,
% 1.47/1.90 e22 ==> h( e11 ), e23 ==> h( e11 ), e24 ==> h( e11 ) }.
% 1.47/1.90 parent0[4]: (8760) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e21, e22 ==> h( e11
% 1.47/1.90 ), e23 ==> h( e11 ), e24 ==> h( e11 ), e11 ==> j( e20 ) }.
% 1.47/1.90 substitution0:
% 1.47/1.90 end
% 1.47/1.90
% 1.47/1.90 eqswap: (8766) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e24, j( e20 ) ==> e11,
% 1.47/1.90 h( e11 ) ==> e21, e22 ==> h( e11 ), e23 ==> h( e11 ) }.
% 1.47/1.90 parent0[4]: (8763) {G1,W20,D3,L5,V0,M5} { j( e20 ) ==> e11, h( e11 ) ==>
% 1.47/1.90 e21, e22 ==> h( e11 ), e23 ==> h( e11 ), e24 ==> h( e11 ) }.
% 1.71/2.08 substitution0:
% 1.71/2.08 end
% 1.71/2.08
% 1.71/2.08 eqswap: (8769) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e23, h( e11 ) ==> e24,
% 1.71/2.08 j( e20 ) ==> e11, h( e11 ) ==> e21, e22 ==> h( e11 ) }.
% 1.71/2.08 parent0[4]: (8766) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e24, j( e20 ) ==>
% 1.71/2.08 e11, h( e11 ) ==> e21, e22 ==> h( e11 ), e23 ==> h( e11 ) }.
% 1.71/2.08 substitution0:
% 1.71/2.08 end
% 1.71/2.08
% 1.71/2.08 eqswap: (8772) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e22, h( e11 ) ==> e23,
% 1.71/2.08 h( e11 ) ==> e24, j( e20 ) ==> e11, h( e11 ) ==> e21 }.
% 1.71/2.08 parent0[4]: (8769) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e23, h( e11 ) ==>
% 1.71/2.08 e24, j( e20 ) ==> e11, h( e11 ) ==> e21, e22 ==> h( e11 ) }.
% 1.71/2.08 substitution0:
% 1.71/2.08 end
% 1.71/2.08
% 1.71/2.08 subsumption: (165) {G1,W20,D3,L5,V0,M5} P(96,161) { j( e20 ) ==> e11, h(
% 1.71/2.08 e11 ) ==> e21, h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 1.71/2.08 parent0: (8772) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e22, h( e11 ) ==> e23
% 1.71/2.08 , h( e11 ) ==> e24, j( e20 ) ==> e11, h( e11 ) ==> e21 }.
% 1.71/2.08 substitution0:
% 1.71/2.08 end
% 1.71/2.08 permutation0:
% 1.71/2.08 0 ==> 2
% 1.71/2.08 1 ==> 3
% 1.71/2.08 2 ==> 4
% 1.71/2.08 3 ==> 0
% 1.71/2.08 4 ==> 1
% 1.71/2.08 end
% 1.71/2.08
% 1.71/2.08 *** allocated 256285 integers for clauses
% 1.71/2.08 *** allocated 256285 integers for termspace/termends
% 1.71/2.08 eqswap: (10838) {G0,W20,D3,L5,V0,M5} { e20 ==> h( e11 ), h( e11 ) ==> e21
% 1.71/2.08 , h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 1.71/2.08 parent0[0]: (96) {G0,W20,D3,L5,V0,M5} I { h( e11 ) ==> e20, h( e11 ) ==>
% 1.71/2.08 e21, h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 1.71/2.08 substitution0:
% 1.71/2.08 end
% 1.71/2.08
% 1.71/2.08 eqswap: (10869) {G0,W5,D4,L1,V0,M1} { e11 ==> j( h( e11 ) ) }.
% 1.71/2.08 parent0[0]: (161) {G0,W5,D4,L1,V0,M1} I { j( h( e11 ) ) ==> e11 }.
% 1.71/2.08 substitution0:
% 1.71/2.08 end
% 1.71/2.08
% 1.71/2.08 paramod: (10873) {G1,W20,D3,L5,V0,M5} { e11 ==> j( e24 ), e20 ==> h( e11 )
% 1.71/2.08 , h( e11 ) ==> e21, h( e11 ) ==> e22, h( e11 ) ==> e23 }.
% 1.71/2.08 parent0[4]: (10838) {G0,W20,D3,L5,V0,M5} { e20 ==> h( e11 ), h( e11 ) ==>
% 1.71/2.08 e21, h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 1.71/2.08 parent1[0; 3]: (10869) {G0,W5,D4,L1,V0,M1} { e11 ==> j( h( e11 ) ) }.
% 1.71/2.08 substitution0:
% 1.71/2.08 end
% 1.71/2.08 substitution1:
% 1.71/2.08 end
% 1.71/2.08
% 1.71/2.08 eqswap: (11639) {G1,W20,D3,L5,V0,M5} { e23 ==> h( e11 ), e11 ==> j( e24 )
% 1.71/2.08 , e20 ==> h( e11 ), h( e11 ) ==> e21, h( e11 ) ==> e22 }.
% 1.71/2.08 parent0[4]: (10873) {G1,W20,D3,L5,V0,M5} { e11 ==> j( e24 ), e20 ==> h(
% 1.71/2.08 e11 ), h( e11 ) ==> e21, h( e11 ) ==> e22, h( e11 ) ==> e23 }.
% 1.71/2.08 substitution0:
% 1.71/2.08 end
% 1.71/2.08
% 1.71/2.08 eqswap: (11643) {G1,W20,D3,L5,V0,M5} { e22 ==> h( e11 ), e23 ==> h( e11 )
% 1.71/2.08 , e11 ==> j( e24 ), e20 ==> h( e11 ), h( e11 ) ==> e21 }.
% 1.71/2.08 parent0[4]: (11639) {G1,W20,D3,L5,V0,M5} { e23 ==> h( e11 ), e11 ==> j(
% 1.71/2.08 e24 ), e20 ==> h( e11 ), h( e11 ) ==> e21, h( e11 ) ==> e22 }.
% 1.71/2.08 substitution0:
% 1.71/2.08 end
% 1.71/2.08
% 1.71/2.08 eqswap: (11646) {G1,W20,D3,L5,V0,M5} { e21 ==> h( e11 ), e22 ==> h( e11 )
% 1.71/2.08 , e23 ==> h( e11 ), e11 ==> j( e24 ), e20 ==> h( e11 ) }.
% 1.71/2.08 parent0[4]: (11643) {G1,W20,D3,L5,V0,M5} { e22 ==> h( e11 ), e23 ==> h(
% 1.71/2.08 e11 ), e11 ==> j( e24 ), e20 ==> h( e11 ), h( e11 ) ==> e21 }.
% 1.71/2.08 substitution0:
% 1.71/2.08 end
% 1.71/2.08
% 1.71/2.08 eqswap: (11649) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e20, e21 ==> h( e11 )
% 1.71/2.08 , e22 ==> h( e11 ), e23 ==> h( e11 ), e11 ==> j( e24 ) }.
% 1.71/2.08 parent0[4]: (11646) {G1,W20,D3,L5,V0,M5} { e21 ==> h( e11 ), e22 ==> h(
% 1.71/2.08 e11 ), e23 ==> h( e11 ), e11 ==> j( e24 ), e20 ==> h( e11 ) }.
% 1.71/2.08 substitution0:
% 1.71/2.08 end
% 1.71/2.08
% 1.71/2.08 eqswap: (11652) {G1,W20,D3,L5,V0,M5} { j( e24 ) ==> e11, h( e11 ) ==> e20
% 1.71/2.08 , e21 ==> h( e11 ), e22 ==> h( e11 ), e23 ==> h( e11 ) }.
% 1.71/2.08 parent0[4]: (11649) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e20, e21 ==> h(
% 1.71/2.08 e11 ), e22 ==> h( e11 ), e23 ==> h( e11 ), e11 ==> j( e24 ) }.
% 1.71/2.08 substitution0:
% 1.71/2.08 end
% 1.71/2.08
% 1.71/2.08 eqswap: (11655) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e23, j( e24 ) ==> e11
% 1.71/2.08 , h( e11 ) ==> e20, e21 ==> h( e11 ), e22 ==> h( e11 ) }.
% 1.71/2.08 parent0[4]: (11652) {G1,W20,D3,L5,V0,M5} { j( e24 ) ==> e11, h( e11 ) ==>
% 1.71/2.08 e20, e21 ==> h( e11 ), e22 ==> h( e11 ), e23 ==> h( e11 ) }.
% 1.71/2.08 substitution0:
% 1.71/2.08 end
% 1.71/2.08
% 1.71/2.08 eqswap: (11658) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e22, h( e11 ) ==> e23
% 1.71/2.08 , j( e24 ) ==> e11, h( e11 ) ==> e20, e21 ==> h( e11 ) }.
% 1.71/2.08 parent0[4]: (11655) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e23, j( e24 ) ==>
% 1.71/2.08 e11, h( e11 ) ==> e20, e21 ==> h( e11 ), e22 ==> h( e11 ) }.
% 1.71/2.08 substitution0:
% 1.71/2.08 end
% 1.71/2.08
% 1.71/2.08 eqswap: (11661) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e21, h( e11 ) ==> e22
% 1.71/2.08 , h( e11 ) ==> e23, j( e24 ) ==> e11, h( e11 ) ==> e20 }.
% 9.28/9.67 parent0[4]: (11658) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e22, h( e11 ) ==>
% 9.28/9.67 e23, j( e24 ) ==> e11, h( e11 ) ==> e20, e21 ==> h( e11 ) }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 subsumption: (169) {G1,W20,D3,L5,V0,M5} P(96,161) { j( e24 ) ==> e11, h(
% 9.28/9.67 e11 ) ==> e20, h( e11 ) ==> e21, h( e11 ) ==> e22, h( e11 ) ==> e23 }.
% 9.28/9.67 parent0: (11661) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e21, h( e11 ) ==> e22
% 9.28/9.67 , h( e11 ) ==> e23, j( e24 ) ==> e11, h( e11 ) ==> e20 }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67 permutation0:
% 9.28/9.67 0 ==> 2
% 9.28/9.67 1 ==> 3
% 9.28/9.67 2 ==> 4
% 9.28/9.67 3 ==> 0
% 9.28/9.67 4 ==> 1
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 *** allocated 384427 integers for termspace/termends
% 9.28/9.67 *** allocated 384427 integers for clauses
% 9.28/9.67 eqswap: (13050) {G0,W20,D3,L5,V0,M5} { e14 ==> j( e20 ), j( e20 ) ==> e10
% 9.28/9.67 , j( e20 ) ==> e11, j( e20 ) ==> e12, j( e20 ) ==> e13 }.
% 9.28/9.67 parent0[4]: (100) {G0,W20,D3,L5,V0,M5} I { j( e20 ) ==> e10, j( e20 ) ==>
% 9.28/9.67 e11, j( e20 ) ==> e12, j( e20 ) ==> e13, j( e20 ) ==> e14 }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 eqswap: (13054) {G0,W20,D3,L5,V0,M5} { e13 ==> j( e20 ), e14 ==> j( e20 )
% 9.28/9.67 , j( e20 ) ==> e10, j( e20 ) ==> e11, j( e20 ) ==> e12 }.
% 9.28/9.67 parent0[4]: (13050) {G0,W20,D3,L5,V0,M5} { e14 ==> j( e20 ), j( e20 ) ==>
% 9.28/9.67 e10, j( e20 ) ==> e11, j( e20 ) ==> e12, j( e20 ) ==> e13 }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 eqswap: (13057) {G0,W20,D3,L5,V0,M5} { e12 ==> j( e20 ), e13 ==> j( e20 )
% 9.28/9.67 , e14 ==> j( e20 ), j( e20 ) ==> e10, j( e20 ) ==> e11 }.
% 9.28/9.67 parent0[4]: (13054) {G0,W20,D3,L5,V0,M5} { e13 ==> j( e20 ), e14 ==> j(
% 9.28/9.67 e20 ), j( e20 ) ==> e10, j( e20 ) ==> e11, j( e20 ) ==> e12 }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 eqswap: (13059) {G0,W20,D3,L5,V0,M5} { e10 ==> j( e20 ), e12 ==> j( e20 )
% 9.28/9.67 , e13 ==> j( e20 ), e14 ==> j( e20 ), j( e20 ) ==> e11 }.
% 9.28/9.67 parent0[3]: (13057) {G0,W20,D3,L5,V0,M5} { e12 ==> j( e20 ), e13 ==> j(
% 9.28/9.67 e20 ), e14 ==> j( e20 ), j( e20 ) ==> e10, j( e20 ) ==> e11 }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 eqswap: (13077) {G1,W8,D4,L1,V0,M1} { j( e20 ) ==> op1( j( e20 ), j( e20 )
% 9.28/9.67 ) }.
% 9.28/9.67 parent0[0]: (130) {G1,W8,D4,L1,V0,M1} I;d(70) { op1( j( e20 ), j( e20 ) )
% 9.28/9.67 ==> j( e20 ) }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 paramod: (475047) {G1,W23,D4,L5,V0,M5} { j( e20 ) ==> op1( j( e20 ), e11 )
% 9.28/9.67 , e10 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 )
% 9.28/9.67 }.
% 9.28/9.67 parent0[4]: (13059) {G0,W20,D3,L5,V0,M5} { e10 ==> j( e20 ), e12 ==> j(
% 9.28/9.67 e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), j( e20 ) ==> e11 }.
% 9.28/9.67 parent1[0; 6]: (13077) {G1,W8,D4,L1,V0,M1} { j( e20 ) ==> op1( j( e20 ), j
% 9.28/9.67 ( e20 ) ) }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67 substitution1:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 paramod: (475053) {G1,W38,D4,L9,V0,M9} { e14 ==> e11, e10 ==> j( e20 ),
% 9.28/9.67 e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), j( e20 ) ==> op1( j
% 9.28/9.67 ( e20 ), e11 ), e10 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ) }.
% 9.28/9.67 parent0[4]: (13059) {G0,W20,D3,L5,V0,M5} { e10 ==> j( e20 ), e12 ==> j(
% 9.28/9.67 e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), j( e20 ) ==> e11 }.
% 9.28/9.67 parent1[4; 2]: (475047) {G1,W23,D4,L5,V0,M5} { j( e20 ) ==> op1( j( e20 )
% 9.28/9.67 , e11 ), e10 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j
% 9.28/9.67 ( e20 ) }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67 substitution1:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 paramod: (475059) {G1,W53,D3,L13,V0,M13} { j( e20 ) ==> op1( e11, e11 ),
% 9.28/9.67 e10 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ),
% 9.28/9.67 e14 ==> e11, e10 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14
% 9.28/9.67 ==> j( e20 ), e10 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ) }.
% 9.28/9.67 parent0[4]: (13059) {G0,W20,D3,L5,V0,M5} { e10 ==> j( e20 ), e12 ==> j(
% 9.28/9.67 e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), j( e20 ) ==> e11 }.
% 9.28/9.67 parent1[5; 4]: (475053) {G1,W38,D4,L9,V0,M9} { e14 ==> e11, e10 ==> j( e20
% 9.28/9.67 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), j( e20 ) ==>
% 9.28/9.67 op1( j( e20 ), e11 ), e10 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20
% 9.28/9.67 ) }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67 substitution1:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 paramod: (475382) {G1,W51,D3,L13,V0,M13} { j( e20 ) ==> e14, e10 ==> j(
% 9.28/9.67 e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e14 ==> e11
% 9.28/9.67 , e10 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 )
% 9.28/9.67 , e10 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ) }.
% 9.28/9.67 parent0[0]: (51) {G0,W5,D3,L1,V0,M1} I { op1( e11, e11 ) ==> e14 }.
% 9.28/9.67 parent1[0; 3]: (475059) {G1,W53,D3,L13,V0,M13} { j( e20 ) ==> op1( e11,
% 9.28/9.67 e11 ), e10 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j(
% 9.28/9.67 e20 ), e14 ==> e11, e10 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 )
% 9.28/9.67 , e14 ==> j( e20 ), e10 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 )
% 9.28/9.67 }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67 substitution1:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 factor: (475383) {G1,W47,D3,L12,V0,M12} { j( e20 ) ==> e14, e10 ==> j( e20
% 9.28/9.67 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e14 ==> e11,
% 9.28/9.67 e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e10 ==> j( e20 ),
% 9.28/9.67 e12 ==> j( e20 ), e13 ==> j( e20 ) }.
% 9.28/9.67 parent0[1, 6]: (475382) {G1,W51,D3,L13,V0,M13} { j( e20 ) ==> e14, e10 ==>
% 9.28/9.67 j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e14 ==>
% 9.28/9.67 e11, e10 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20
% 9.28/9.67 ), e10 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ) }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 factor: (475384) {G1,W43,D3,L11,V0,M11} { j( e20 ) ==> e14, e10 ==> j( e20
% 9.28/9.67 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e14 ==> e11,
% 9.28/9.67 e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e12 ==> j( e20 ),
% 9.28/9.67 e13 ==> j( e20 ) }.
% 9.28/9.67 parent0[1, 9]: (475383) {G1,W47,D3,L12,V0,M12} { j( e20 ) ==> e14, e10 ==>
% 9.28/9.67 j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e14 ==>
% 9.28/9.67 e11, e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e10 ==> j( e20
% 9.28/9.67 ), e12 ==> j( e20 ), e13 ==> j( e20 ) }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 factor: (475385) {G1,W39,D3,L10,V0,M10} { j( e20 ) ==> e14, e10 ==> j( e20
% 9.28/9.67 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e14 ==> e11,
% 9.28/9.67 e13 ==> j( e20 ), e14 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 )
% 9.28/9.67 }.
% 9.28/9.67 parent0[2, 6]: (475384) {G1,W43,D3,L11,V0,M11} { j( e20 ) ==> e14, e10 ==>
% 9.28/9.67 j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e14 ==>
% 9.28/9.67 e11, e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e12 ==> j( e20
% 9.28/9.67 ), e13 ==> j( e20 ) }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 factor: (475386) {G1,W35,D3,L9,V0,M9} { j( e20 ) ==> e14, e10 ==> j( e20 )
% 9.28/9.67 , e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e14 ==> e11, e13
% 9.28/9.67 ==> j( e20 ), e14 ==> j( e20 ), e13 ==> j( e20 ) }.
% 9.28/9.67 parent0[2, 8]: (475385) {G1,W39,D3,L10,V0,M10} { j( e20 ) ==> e14, e10 ==>
% 9.28/9.67 j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e14 ==>
% 9.28/9.67 e11, e13 ==> j( e20 ), e14 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20
% 9.28/9.67 ) }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 factor: (475387) {G1,W31,D3,L8,V0,M8} { j( e20 ) ==> e14, e10 ==> j( e20 )
% 9.28/9.67 , e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e14 ==> e11, e14
% 9.28/9.67 ==> j( e20 ), e13 ==> j( e20 ) }.
% 9.28/9.67 parent0[3, 6]: (475386) {G1,W35,D3,L9,V0,M9} { j( e20 ) ==> e14, e10 ==> j
% 9.28/9.67 ( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e14 ==>
% 9.28/9.67 e11, e13 ==> j( e20 ), e14 ==> j( e20 ), e13 ==> j( e20 ) }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 factor: (475388) {G1,W27,D3,L7,V0,M7} { j( e20 ) ==> e14, e10 ==> j( e20 )
% 9.28/9.67 , e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e14 ==> e11, e14
% 9.28/9.67 ==> j( e20 ) }.
% 9.28/9.67 parent0[3, 7]: (475387) {G1,W31,D3,L8,V0,M8} { j( e20 ) ==> e14, e10 ==> j
% 9.28/9.67 ( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e14 ==>
% 9.28/9.67 e11, e14 ==> j( e20 ), e13 ==> j( e20 ) }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 factor: (475389) {G1,W23,D3,L6,V0,M6} { j( e20 ) ==> e14, e10 ==> j( e20 )
% 9.28/9.67 , e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e14 ==> e11 }.
% 9.28/9.67 parent0[4, 6]: (475388) {G1,W27,D3,L7,V0,M7} { j( e20 ) ==> e14, e10 ==> j
% 9.28/9.67 ( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e14 ==>
% 9.28/9.67 e11, e14 ==> j( e20 ) }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 resolution: (475390) {G1,W20,D3,L5,V0,M5} { j( e20 ) ==> e14, e10 ==> j(
% 9.28/9.67 e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ) }.
% 9.28/9.67 parent0[0]: (6) {G0,W3,D2,L1,V0,M1} I { ! e14 ==> e11 }.
% 9.28/9.67 parent1[5]: (475389) {G1,W23,D3,L6,V0,M6} { j( e20 ) ==> e14, e10 ==> j(
% 9.28/9.67 e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ), e14 ==> j( e20 ), e14 ==> e11
% 9.28/9.67 }.
% 9.28/9.67 substitution0:
% 9.28/9.67 end
% 9.28/9.67 substitution1:
% 9.28/9.67 end
% 9.28/9.67
% 9.28/9.67 eqswap: (475395) {G1,W20,D3,L5,V0,M5} { j( e20 ) ==> e14, j( e20 ) ==> e14
% 9.28/9.67 , e10 ==> j( e20 ), e12 ==> j( e20 ), e13 ==> j( e20 ) }.
% 9.28/9.67 parent0[4]: (475390) {G1,W20,D3,LCputime limit exceeded (core dumped)
%------------------------------------------------------------------------------