%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : ALG085+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Thu Jul 14 12:09:24 EDT 2022
% Result : Theorem 0.75s 1.37s
% Output : Refutation 0.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : ALG085+1 : TPTP v8.1.0. Released v2.7.0.
% 0.04/0.13 % Command : bliksem %s
% 0.13/0.33 % Computer : n020.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Thu Jun 9 05:52:36 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.71/1.13 *** allocated 10000 integers for termspace/termends
% 0.71/1.13 *** allocated 10000 integers for clauses
% 0.71/1.13 *** allocated 10000 integers for justifications
% 0.71/1.13 Bliksem 1.12
% 0.71/1.13
% 0.71/1.13
% 0.71/1.13 Automatic Strategy Selection
% 0.71/1.13
% 0.71/1.13
% 0.71/1.13 Clauses:
% 0.71/1.13
% 0.71/1.13 { ! e10 = e11 }.
% 0.71/1.13 { ! e10 = e12 }.
% 0.71/1.13 { ! e10 = e13 }.
% 0.71/1.13 { ! e10 = e14 }.
% 0.71/1.13 { ! e11 = e12 }.
% 0.71/1.13 { ! e11 = e13 }.
% 0.71/1.13 { ! e11 = e14 }.
% 0.71/1.13 { ! e12 = e13 }.
% 0.71/1.13 { ! e12 = e14 }.
% 0.71/1.13 { ! e13 = e14 }.
% 0.71/1.13 { ! e20 = e21 }.
% 0.71/1.13 { ! e20 = e22 }.
% 0.71/1.13 { ! e20 = e23 }.
% 0.71/1.13 { ! e20 = e24 }.
% 0.71/1.13 { ! e21 = e22 }.
% 0.71/1.13 { ! e21 = e23 }.
% 0.71/1.13 { ! e21 = e24 }.
% 0.71/1.13 { ! e22 = e23 }.
% 0.71/1.13 { ! e22 = e24 }.
% 0.71/1.13 { ! e23 = e24 }.
% 0.71/1.13 { ! e10 = e20 }.
% 0.71/1.13 { ! e10 = e21 }.
% 0.71/1.13 { ! e10 = e22 }.
% 0.71/1.13 { ! e10 = e23 }.
% 0.71/1.13 { ! e10 = e24 }.
% 0.71/1.13 { ! e11 = e20 }.
% 0.71/1.13 { ! e11 = e21 }.
% 0.71/1.13 { ! e11 = e22 }.
% 0.71/1.13 { ! e11 = e23 }.
% 0.71/1.13 { ! e11 = e24 }.
% 0.71/1.13 { ! e12 = e20 }.
% 0.71/1.13 { ! e12 = e21 }.
% 0.71/1.13 { ! e12 = e22 }.
% 0.71/1.13 { ! e12 = e23 }.
% 0.71/1.13 { ! e12 = e24 }.
% 0.71/1.13 { ! e13 = e20 }.
% 0.71/1.13 { ! e13 = e21 }.
% 0.71/1.13 { ! e13 = e22 }.
% 0.71/1.13 { ! e13 = e23 }.
% 0.71/1.13 { ! e13 = e24 }.
% 0.71/1.13 { ! e14 = e20 }.
% 0.71/1.13 { ! e14 = e21 }.
% 0.71/1.13 { ! e14 = e22 }.
% 0.71/1.13 { ! e14 = e23 }.
% 0.71/1.13 { ! e14 = e24 }.
% 0.71/1.13 { op1( e10, e10 ) = e10 }.
% 0.71/1.13 { op1( e10, e11 ) = e11 }.
% 0.71/1.13 { op1( e10, e12 ) = e12 }.
% 0.71/1.13 { op1( e10, e13 ) = e13 }.
% 0.71/1.13 { op1( e10, e14 ) = e14 }.
% 0.71/1.13 { op1( e11, e10 ) = e11 }.
% 0.71/1.13 { op1( e11, e11 ) = e14 }.
% 0.71/1.13 { op1( e11, e12 ) = e10 }.
% 0.71/1.13 { op1( e11, e13 ) = e12 }.
% 0.71/1.13 { op1( e11, e14 ) = e13 }.
% 0.71/1.13 { op1( e12, e10 ) = e12 }.
% 0.71/1.13 { op1( e12, e11 ) = e10 }.
% 0.71/1.13 { op1( e12, e12 ) = e13 }.
% 0.71/1.13 { op1( e12, e13 ) = e14 }.
% 0.71/1.13 { op1( e12, e14 ) = e11 }.
% 0.71/1.13 { op1( e13, e10 ) = e13 }.
% 0.71/1.13 { op1( e13, e11 ) = e12 }.
% 0.71/1.13 { op1( e13, e12 ) = e14 }.
% 0.71/1.13 { op1( e13, e13 ) = e11 }.
% 0.71/1.13 { op1( e13, e14 ) = e10 }.
% 0.71/1.13 { op1( e14, e10 ) = e14 }.
% 0.71/1.13 { op1( e14, e11 ) = e13 }.
% 0.71/1.13 { op1( e14, e12 ) = e11 }.
% 0.71/1.13 { op1( e14, e13 ) = e10 }.
% 0.71/1.13 { op1( e14, e14 ) = e12 }.
% 0.71/1.13 { op2( e20, e20 ) = e20 }.
% 0.71/1.13 { op2( e20, e21 ) = e21 }.
% 0.71/1.13 { op2( e20, e22 ) = e22 }.
% 0.71/1.13 { op2( e20, e23 ) = e23 }.
% 0.71/1.13 { op2( e20, e24 ) = e24 }.
% 0.71/1.13 { op2( e21, e20 ) = e21 }.
% 0.71/1.13 { op2( e21, e21 ) = e22 }.
% 0.71/1.13 { op2( e21, e22 ) = e24 }.
% 0.71/1.13 { op2( e21, e23 ) = e20 }.
% 0.71/1.13 { op2( e21, e24 ) = e23 }.
% 0.71/1.13 { op2( e22, e20 ) = e22 }.
% 0.71/1.13 { op2( e22, e21 ) = e20 }.
% 0.71/1.13 { op2( e22, e22 ) = e23 }.
% 0.71/1.13 { op2( e22, e23 ) = e24 }.
% 0.71/1.13 { op2( e22, e24 ) = e21 }.
% 0.71/1.13 { op2( e23, e20 ) = e23 }.
% 0.71/1.13 { op2( e23, e21 ) = e24 }.
% 0.71/1.13 { op2( e23, e22 ) = e20 }.
% 0.71/1.13 { op2( e23, e23 ) = e21 }.
% 0.71/1.13 { op2( e23, e24 ) = e22 }.
% 0.71/1.13 { op2( e24, e20 ) = e24 }.
% 0.71/1.13 { op2( e24, e21 ) = e23 }.
% 0.71/1.13 { op2( e24, e22 ) = e21 }.
% 0.71/1.13 { op2( e24, e23 ) = e22 }.
% 0.71/1.13 { op2( e24, e24 ) = e20 }.
% 0.71/1.13 { h( e10 ) = e20, h( e10 ) = e21, h( e10 ) = e22, h( e10 ) = e23, h( e10 )
% 0.71/1.13 = e24 }.
% 0.71/1.13 { h( e11 ) = e20, h( e11 ) = e21, h( e11 ) = e22, h( e11 ) = e23, h( e11 )
% 0.71/1.13 = e24 }.
% 0.71/1.13 { h( e12 ) = e20, h( e12 ) = e21, h( e12 ) = e22, h( e12 ) = e23, h( e12 )
% 0.71/1.13 = e24 }.
% 0.71/1.13 { h( e13 ) = e20, h( e13 ) = e21, h( e13 ) = e22, h( e13 ) = e23, h( e13 )
% 0.71/1.13 = e24 }.
% 0.71/1.13 { h( e14 ) = e20, h( e14 ) = e21, h( e14 ) = e22, h( e14 ) = e23, h( e14 )
% 0.71/1.13 = e24 }.
% 0.71/1.13 { j( e20 ) = e10, j( e20 ) = e11, j( e20 ) = e12, j( e20 ) = e13, j( e20 )
% 0.71/1.13 = e14 }.
% 0.71/1.13 { j( e21 ) = e10, j( e21 ) = e11, j( e21 ) = e12, j( e21 ) = e13, j( e21 )
% 0.71/1.13 = e14 }.
% 0.71/1.13 { j( e22 ) = e10, j( e22 ) = e11, j( e22 ) = e12, j( e22 ) = e13, j( e22 )
% 0.71/1.13 = e14 }.
% 0.71/1.13 { j( e23 ) = e10, j( e23 ) = e11, j( e23 ) = e12, j( e23 ) = e13, j( e23 )
% 0.71/1.13 = e14 }.
% 0.71/1.13 { j( e24 ) = e10, j( e24 ) = e11, j( e24 ) = e12, j( e24 ) = e13, j( e24 )
% 0.71/1.13 = e14 }.
% 0.71/1.13 { h( op1( e10, e10 ) ) = op2( h( e10 ), h( e10 ) ) }.
% 0.71/1.13 { h( op1( e10, e11 ) ) = op2( h( e10 ), h( e11 ) ) }.
% 0.71/1.13 { h( op1( e10, e12 ) ) = op2( h( e10 ), h( e12 ) ) }.
% 0.71/1.13 { h( op1( e10, e13 ) ) = op2( h( e10 ), h( e13 ) ) }.
% 0.71/1.13 { h( op1( e10, e14 ) ) = op2( h( e10 ), h( e14 ) ) }.
% 0.71/1.13 { h( op1( e11, e10 ) ) = op2( h( e11 ), h( e10 ) ) }.
% 0.71/1.13 { h( op1( e11, e11 ) ) = op2( h( e11 ), h( e11 ) ) }.
% 0.71/1.13 { h( op1( e11, e12 ) ) = op2( h( e11 ), h( e12 ) ) }.
% 0.71/1.13 { h( op1( e11, e13 ) ) = op2( h( e11 ), h( e13 ) ) }.
% 0.71/1.13 { h( op1( e11, e14 ) ) = op2( h( e11 ), h( e14 ) ) }.
% 0.71/1.13 { h( op1( e12, e10 ) ) = op2( h( e12 ), h( e10 ) ) }.
% 0.71/1.13 { h( op1( e12, e11 ) ) = op2( h( e12 ), h( e11 ) ) }.
% 0.71/1.13 { h( op1( e12, e12 ) ) = op2( h( e12 ), h( e12 ) ) }.
% 0.71/1.13 { h( op1( e12, e13 ) ) = op2( h( e12 ), h( e13 ) ) }.
% 0.71/1.13 { h( op1( e12, e14 ) ) = op2( h( e12 ), h( e14 ) ) }.
% 0.71/1.13 { h( op1( e13, e10 ) ) = op2( h( e13 ), h( e10 ) ) }.
% 0.71/1.13 { h( op1( e13, e11 ) ) = op2( h( e13 ), h( e11 ) ) }.
% 0.75/1.37 { h( op1( e13, e12 ) ) = op2( h( e13 ), h( e12 ) ) }.
% 0.75/1.37 { h( op1( e13, e13 ) ) = op2( h( e13 ), h( e13 ) ) }.
% 0.75/1.37 { h( op1( e13, e14 ) ) = op2( h( e13 ), h( e14 ) ) }.
% 0.75/1.37 { h( op1( e14, e10 ) ) = op2( h( e14 ), h( e10 ) ) }.
% 0.75/1.37 { h( op1( e14, e11 ) ) = op2( h( e14 ), h( e11 ) ) }.
% 0.75/1.37 { h( op1( e14, e12 ) ) = op2( h( e14 ), h( e12 ) ) }.
% 0.75/1.37 { h( op1( e14, e13 ) ) = op2( h( e14 ), h( e13 ) ) }.
% 0.75/1.37 { h( op1( e14, e14 ) ) = op2( h( e14 ), h( e14 ) ) }.
% 0.75/1.37 { j( op2( e20, e20 ) ) = op1( j( e20 ), j( e20 ) ) }.
% 0.75/1.37 { j( op2( e20, e21 ) ) = op1( j( e20 ), j( e21 ) ) }.
% 0.75/1.37 { j( op2( e20, e22 ) ) = op1( j( e20 ), j( e22 ) ) }.
% 0.75/1.37 { j( op2( e20, e23 ) ) = op1( j( e20 ), j( e23 ) ) }.
% 0.75/1.37 { j( op2( e20, e24 ) ) = op1( j( e20 ), j( e24 ) ) }.
% 0.75/1.37 { j( op2( e21, e20 ) ) = op1( j( e21 ), j( e20 ) ) }.
% 0.75/1.37 { j( op2( e21, e21 ) ) = op1( j( e21 ), j( e21 ) ) }.
% 0.75/1.37 { j( op2( e21, e22 ) ) = op1( j( e21 ), j( e22 ) ) }.
% 0.75/1.37 { j( op2( e21, e23 ) ) = op1( j( e21 ), j( e23 ) ) }.
% 0.75/1.37 { j( op2( e21, e24 ) ) = op1( j( e21 ), j( e24 ) ) }.
% 0.75/1.37 { j( op2( e22, e20 ) ) = op1( j( e22 ), j( e20 ) ) }.
% 0.75/1.37 { j( op2( e22, e21 ) ) = op1( j( e22 ), j( e21 ) ) }.
% 0.75/1.37 { j( op2( e22, e22 ) ) = op1( j( e22 ), j( e22 ) ) }.
% 0.75/1.37 { j( op2( e22, e23 ) ) = op1( j( e22 ), j( e23 ) ) }.
% 0.75/1.37 { j( op2( e22, e24 ) ) = op1( j( e22 ), j( e24 ) ) }.
% 0.75/1.37 { j( op2( e23, e20 ) ) = op1( j( e23 ), j( e20 ) ) }.
% 0.75/1.37 { j( op2( e23, e21 ) ) = op1( j( e23 ), j( e21 ) ) }.
% 0.75/1.37 { j( op2( e23, e22 ) ) = op1( j( e23 ), j( e22 ) ) }.
% 0.75/1.37 { j( op2( e23, e23 ) ) = op1( j( e23 ), j( e23 ) ) }.
% 0.75/1.37 { j( op2( e23, e24 ) ) = op1( j( e23 ), j( e24 ) ) }.
% 0.75/1.37 { j( op2( e24, e20 ) ) = op1( j( e24 ), j( e20 ) ) }.
% 0.75/1.37 { j( op2( e24, e21 ) ) = op1( j( e24 ), j( e21 ) ) }.
% 0.75/1.37 { j( op2( e24, e22 ) ) = op1( j( e24 ), j( e22 ) ) }.
% 0.75/1.37 { j( op2( e24, e23 ) ) = op1( j( e24 ), j( e23 ) ) }.
% 0.75/1.37 { j( op2( e24, e24 ) ) = op1( j( e24 ), j( e24 ) ) }.
% 0.75/1.37 { h( j( e20 ) ) = e20 }.
% 0.75/1.37 { h( j( e21 ) ) = e21 }.
% 0.75/1.37 { h( j( e22 ) ) = e22 }.
% 0.75/1.37 { h( j( e23 ) ) = e23 }.
% 0.75/1.37 { h( j( e24 ) ) = e24 }.
% 0.75/1.37 { j( h( e10 ) ) = e10 }.
% 0.75/1.37 { j( h( e11 ) ) = e11 }.
% 0.75/1.37 { j( h( e12 ) ) = e12 }.
% 0.75/1.37 { j( h( e13 ) ) = e13 }.
% 0.75/1.37 { j( h( e14 ) ) = e14 }.
% 0.75/1.37
% 0.75/1.37 percentage equality = 1.000000, percentage horn = 0.939394
% 0.75/1.37 This is a pure equality problem
% 0.75/1.37
% 0.75/1.37
% 0.75/1.37
% 0.75/1.37 Options Used:
% 0.75/1.37
% 0.75/1.37 useres = 1
% 0.75/1.37 useparamod = 1
% 0.75/1.37 useeqrefl = 1
% 0.75/1.37 useeqfact = 1
% 0.75/1.37 usefactor = 1
% 0.75/1.37 usesimpsplitting = 0
% 0.75/1.37 usesimpdemod = 5
% 0.75/1.37 usesimpres = 3
% 0.75/1.37
% 0.75/1.37 resimpinuse = 1000
% 0.75/1.37 resimpclauses = 20000
% 0.75/1.37 substype = eqrewr
% 0.75/1.37 backwardsubs = 1
% 0.75/1.37 selectoldest = 5
% 0.75/1.37
% 0.75/1.37 litorderings [0] = split
% 0.75/1.37 litorderings [1] = extend the termordering, first sorting on arguments
% 0.75/1.37
% 0.75/1.37 termordering = kbo
% 0.75/1.37
% 0.75/1.37 litapriori = 0
% 0.75/1.37 termapriori = 1
% 0.75/1.37 litaposteriori = 0
% 0.75/1.37 termaposteriori = 0
% 0.75/1.37 demodaposteriori = 0
% 0.75/1.37 ordereqreflfact = 0
% 0.75/1.37
% 0.75/1.37 litselect = negord
% 0.75/1.37
% 0.75/1.37 maxweight = 15
% 0.75/1.37 maxdepth = 30000
% 0.75/1.37 maxlength = 115
% 0.75/1.37 maxnrvars = 195
% 0.75/1.37 excuselevel = 1
% 0.75/1.37 increasemaxweight = 1
% 0.75/1.37
% 0.75/1.37 maxselected = 10000000
% 0.75/1.37 maxnrclauses = 10000000
% 0.75/1.37
% 0.75/1.37 showgenerated = 0
% 0.75/1.37 showkept = 0
% 0.75/1.37 showselected = 0
% 0.75/1.37 showdeleted = 0
% 0.75/1.37 showresimp = 1
% 0.75/1.37 showstatus = 2000
% 0.75/1.37
% 0.75/1.37 prologoutput = 0
% 0.75/1.37 nrgoals = 5000000
% 0.75/1.37 totalproof = 1
% 0.75/1.37
% 0.75/1.37 Symbols occurring in the translation:
% 0.75/1.37
% 0.75/1.37 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.75/1.37 . [1, 2] (w:1, o:23, a:1, s:1, b:0),
% 0.75/1.37 ! [4, 1] (w:0, o:16, a:1, s:1, b:0),
% 0.75/1.37 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.75/1.37 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.75/1.37 e10 [35, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.75/1.37 e11 [36, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.75/1.37 e12 [37, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.75/1.37 e13 [38, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.75/1.37 e14 [39, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.75/1.37 e20 [40, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.75/1.37 e21 [41, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.75/1.37 e22 [42, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.75/1.37 e23 [43, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.75/1.37 e24 [44, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.75/1.37 op1 [45, 2] (w:1, o:47, a:1, s:1, b:0),
% 0.75/1.37 op2 [46, 2] (w:1, o:48, a:1, s:1, b:0),
% 0.75/1.37 h [47, 1] (w:1, o:21, a:1, s:1, b:0),
% 0.75/1.37 j [48, 1] (w:1, o:22, a:1, s:1, b:0).
% 0.75/1.37
% 0.75/1.37
% 0.75/1.37 Starting Search:
% 0.75/1.37
% 0.75/1.37 *** allocated 15000 integers for clauses
% 0.75/1.37 Resimplifying inuse:
% 0.75/1.37 Done
% 0.75/1.37
% 0.75/1.37 Failed to find proof!
% 0.75/1.37 maxweight = 15
% 0.75/1.37 maxnrclauses = 10000000
% 0.75/1.37 Generated: 14585
% 0.75/1.37 Kept: 215
% 0.75/1.37
% 0.75/1.37
% 0.75/1.37 The strategy used was not complete!
% 0.75/1.37
% 0.75/1.37 Increased maxweight to 16
% 0.75/1.37
% 0.75/1.37 Starting Search:
% 0.75/1.37
% 0.75/1.37 *** allocated 22500 integers for clauses
% 0.75/1.37
% 0.75/1.37 Bliksems!, er is een bewijs:
% 0.75/1.37 % SZS status Theorem
% 0.75/1.37 % SZS output start Refutation
% 0.75/1.37
% 0.75/1.37 (3) {G0,W3,D2,L1,V0,M1} I { ! e14 ==> e10 }.
% 0.75/1.37 (6) {G0,W3,D2,L1,V0,M1} I { ! e14 ==> e11 }.
% 0.75/1.37 (13) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e20 }.
% 0.75/1.37 (14) {G0,W3,D2,L1,V0,M1} I { ! e22 ==> e21 }.
% 0.75/1.37 (15) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e21 }.
% 0.75/1.37 (16) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e21 }.
% 0.75/1.37 (17) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e22 }.
% 0.75/1.37 (45) {G0,W5,D3,L1,V0,M1} I { op1( e10, e10 ) ==> e10 }.
% 0.75/1.37 (47) {G0,W5,D3,L1,V0,M1} I { op1( e10, e12 ) ==> e12 }.
% 0.75/1.37 (48) {G0,W5,D3,L1,V0,M1} I { op1( e10, e13 ) ==> e13 }.
% 0.75/1.37 (51) {G0,W5,D3,L1,V0,M1} I { op1( e11, e11 ) ==> e14 }.
% 0.75/1.37 (52) {G0,W5,D3,L1,V0,M1} I { op1( e11, e12 ) ==> e10 }.
% 0.75/1.37 (53) {G0,W5,D3,L1,V0,M1} I { op1( e11, e13 ) ==> e12 }.
% 0.75/1.37 (54) {G0,W5,D3,L1,V0,M1} I { op1( e11, e14 ) ==> e13 }.
% 0.75/1.37 (63) {G0,W5,D3,L1,V0,M1} I { op1( e13, e13 ) ==> e11 }.
% 0.75/1.37 (70) {G0,W5,D3,L1,V0,M1} I { op2( e20, e20 ) ==> e20 }.
% 0.75/1.37 (76) {G0,W5,D3,L1,V0,M1} I { op2( e21, e21 ) ==> e22 }.
% 0.75/1.37 (77) {G0,W5,D3,L1,V0,M1} I { op2( e21, e22 ) ==> e24 }.
% 0.75/1.37 (82) {G0,W5,D3,L1,V0,M1} I { op2( e22, e22 ) ==> e23 }.
% 0.75/1.37 (83) {G0,W5,D3,L1,V0,M1} I { op2( e22, e23 ) ==> e24 }.
% 0.75/1.37 (86) {G0,W5,D3,L1,V0,M1} I { op2( e23, e21 ) ==> e24 }.
% 0.75/1.37 (88) {G0,W5,D3,L1,V0,M1} I { op2( e23, e23 ) ==> e21 }.
% 0.75/1.37 (94) {G0,W5,D3,L1,V0,M1} I { op2( e24, e24 ) ==> e20 }.
% 0.75/1.37 (95) {G0,W20,D3,L5,V0,M5} I { h( e10 ) ==> e20, h( e10 ) ==> e21, h( e10 )
% 0.75/1.37 ==> e22, h( e10 ) ==> e23, h( e10 ) ==> e24 }.
% 0.75/1.37 (96) {G0,W20,D3,L5,V0,M5} I { h( e11 ) ==> e20, h( e11 ) ==> e21, h( e11 )
% 0.75/1.37 ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 0.75/1.37 (105) {G1,W8,D4,L1,V0,M1} I;d(45) { op2( h( e10 ), h( e10 ) ) ==> h( e10 )
% 0.75/1.37 }.
% 0.75/1.37 (107) {G1,W8,D4,L1,V0,M1} I;d(47) { op2( h( e10 ), h( e12 ) ) ==> h( e12 )
% 0.75/1.37 }.
% 0.75/1.37 (108) {G1,W8,D4,L1,V0,M1} I;d(48) { op2( h( e10 ), h( e13 ) ) ==> h( e13 )
% 0.75/1.37 }.
% 0.75/1.37 (111) {G1,W8,D4,L1,V0,M1} I;d(51) { op2( h( e11 ), h( e11 ) ) ==> h( e14 )
% 0.75/1.37 }.
% 0.75/1.37 (112) {G1,W8,D4,L1,V0,M1} I;d(52) { op2( h( e11 ), h( e12 ) ) ==> h( e10 )
% 0.75/1.37 }.
% 0.75/1.37 (113) {G1,W8,D4,L1,V0,M1} I;d(53) { op2( h( e11 ), h( e13 ) ) ==> h( e12 )
% 0.75/1.37 }.
% 0.75/1.37 (114) {G1,W8,D4,L1,V0,M1} I;d(54) { op2( h( e11 ), h( e14 ) ) ==> h( e13 )
% 0.75/1.37 }.
% 0.75/1.37 (123) {G1,W8,D4,L1,V0,M1} I;d(63) { op2( h( e13 ), h( e13 ) ) ==> h( e11 )
% 0.75/1.37 }.
% 0.75/1.37 (130) {G1,W8,D4,L1,V0,M1} I;d(70) { op1( j( e20 ), j( e20 ) ) ==> j( e20 )
% 0.75/1.37 }.
% 0.75/1.37 (154) {G1,W8,D4,L1,V0,M1} I;d(94) { op1( j( e24 ), j( e24 ) ) ==> j( e20 )
% 0.75/1.37 }.
% 0.75/1.37 (160) {G0,W5,D4,L1,V0,M1} I { j( h( e10 ) ) ==> e10 }.
% 0.75/1.37 (161) {G0,W5,D4,L1,V0,M1} I { j( h( e11 ) ) ==> e11 }.
% 0.75/1.37 (165) {G1,W20,D3,L5,V0,M5} P(96,161) { j( e20 ) ==> e11, h( e11 ) ==> e21,
% 0.75/1.37 h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 0.75/1.37 (169) {G1,W20,D3,L5,V0,M5} P(96,161) { j( e24 ) ==> e11, h( e11 ) ==> e20,
% 0.75/1.37 h( e11 ) ==> e21, h( e11 ) ==> e22, h( e11 ) ==> e23 }.
% 0.75/1.37 (220) {G2,W16,D3,L4,V0,M4} P(95,105);d(76);r(14) { h( e10 ) ==> e20, h( e10
% 0.75/1.37 ) ==> e22, h( e10 ) ==> e23, h( e10 ) ==> e24 }.
% 0.75/1.37 (223) {G3,W15,D3,L4,V0,M4} P(95,105);d(94);d(220);r(16) { h( e10 ) ==> e20
% 0.75/1.37 , h( e10 ) ==> e22, h( e10 ) ==> e23, e24 ==> e20 }.
% 0.75/1.37 (224) {G4,W12,D3,L3,V0,M3} E(220);d(223);q { h( e10 ) ==> e20, h( e10 ) ==>
% 0.75/1.37 e22, h( e10 ) ==> e23 }.
% 0.75/1.37 (225) {G2,W16,D3,L4,V0,M4} P(165,130);d(51);r(6) { h( e11 ) ==> e21, h( e11
% 0.75/1.37 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 0.75/1.37 (247) {G5,W8,D3,L2,V0,M2} P(224,105);d(82);r(17) { h( e10 ) ==> e20, h( e10
% 0.75/1.37 ) ==> e23 }.
% 0.75/1.37 (248) {G6,W7,D3,L2,V0,M2} P(224,105);d(88);d(247);r(17) { h( e10 ) ==> e20
% 0.75/1.37 , e23 ==> e21 }.
% 0.75/1.37 (253) {G7,W4,D3,L1,V0,M1} S(248);r(15) { h( e10 ) ==> e20 }.
% 0.75/1.37 (256) {G8,W7,D4,L1,V0,M1} P(253,108) { op2( e20, h( e13 ) ) ==> h( e13 )
% 0.75/1.37 }.
% 0.75/1.37 (258) {G8,W7,D4,L1,V0,M1} P(253,107) { op2( e20, h( e12 ) ) ==> h( e12 )
% 0.75/1.37 }.
% 0.75/1.37 (262) {G8,W4,D3,L1,V0,M1} P(253,160) { j( e20 ) ==> e10 }.
% 0.75/1.37 (274) {G3,W16,D3,L4,V0,M4} S(169);d(225);r(13) { j( e24 ) ==> e11, h( e11 )
% 0.75/1.37 ==> e21, h( e11 ) ==> e22, h( e11 ) ==> e23 }.
% 0.75/1.37 (275) {G4,W16,D3,L4,V0,M4} P(274,111);d(76) { j( e24 ) ==> e11, h( e11 )
% 0.75/1.37 ==> e22, h( e11 ) ==> e23, h( e14 ) ==> e22 }.
% 0.75/1.37 (276) {G4,W16,D3,L4,V0,M4} P(274,111);d(82) { j( e24 ) ==> e11, h( e11 )
% 0.75/1.37 ==> e21, h( e11 ) ==> e23, h( e14 ) ==> e23 }.
% 0.75/1.37 (277) {G4,W16,D3,L4,V0,M4} P(274,111);d(88) { j( e24 ) ==> e11, h( e11 )
% 0.75/1.37 ==> e21, h( e11 ) ==> e22, h( e14 ) ==> e21 }.
% 0.75/1.37 (278) {G5,W16,D3,L4,V0,M4} P(274,114);d(275);d(77) { j( e24 ) ==> e11, h(
% 0.75/1.37 e11 ) ==> e22, h( e11 ) ==> e23, h( e13 ) ==> e24 }.
% 0.75/1.37 (279) {G6,W12,D3,L3,V0,M3} P(274,114);d(276);d(83);d(278);r(14) { j( e24 )
% 0.75/1.37 ==> e11, h( e11 ) ==> e23, h( e13 ) ==> e24 }.
% 0.75/1.37 (280) {G7,W11,D3,L3,V0,M3} P(274,114);d(277);d(86);d(278);d(279);r(15) { j
% 0.75/1.37 ( e24 ) ==> e11, h( e13 ) ==> e24, e23 ==> e22 }.
% 0.75/1.37 (290) {G8,W8,D3,L2,V0,M2} S(280);r(17) { j( e24 ) ==> e11, h( e13 ) ==> e24
% 0.75/1.37 }.
% 0.75/1.37 (304) {G9,W4,D3,L1,V0,M1} P(290,154);d(51);d(262);r(3) { h( e13 ) ==> e24
% 0.75/1.37 }.
% 0.75/1.37 (311) {G10,W4,D3,L1,V0,M1} P(304,123);d(94) { h( e11 ) ==> e20 }.
% 0.75/1.37 (317) {G11,W4,D3,L1,V0,M1} P(311,112);d(258);d(253) { h( e12 ) ==> e20 }.
% 0.75/1.37 (318) {G12,W0,D0,L0,V0,M0} P(311,113);d(256);d(304);d(317);r(13) { }.
% 0.75/1.37
% 0.75/1.37
% 0.75/1.37 % SZS output end Refutation
% 0.75/1.37 found a proof!
% 0.75/1.37
% 0.75/1.37 *** allocated 33750 integers for clauses
% 0.75/1.37
% 0.75/1.37 Unprocessed initial clauses:
% 0.75/1.37
% 0.75/1.37 (320) {G0,W3,D2,L1,V0,M1} { ! e10 = e11 }.
% 0.75/1.37 (321) {G0,W3,D2,L1,V0,M1} { ! e10 = e12 }.
% 0.75/1.37 (322) {G0,W3,D2,L1,V0,M1} { ! e10 = e13 }.
% 0.75/1.37 (323) {G0,W3,D2,L1,V0,M1} { ! e10 = e14 }.
% 0.75/1.37 (324) {G0,W3,D2,L1,V0,M1} { ! e11 = e12 }.
% 0.75/1.37 (325) {G0,W3,D2,L1,V0,M1} { ! e11 = e13 }.
% 0.75/1.37 (326) {G0,W3,D2,L1,V0,M1} { ! e11 = e14 }.
% 0.75/1.37 (327) {G0,W3,D2,L1,V0,M1} { ! e12 = e13 }.
% 0.75/1.37 (328) {G0,W3,D2,L1,V0,M1} { ! e12 = e14 }.
% 0.75/1.37 (329) {G0,W3,D2,L1,V0,M1} { ! e13 = e14 }.
% 0.75/1.37 (330) {G0,W3,D2,L1,V0,M1} { ! e20 = e21 }.
% 0.75/1.37 (331) {G0,W3,D2,L1,V0,M1} { ! e20 = e22 }.
% 0.75/1.37 (332) {G0,W3,D2,L1,V0,M1} { ! e20 = e23 }.
% 0.75/1.37 (333) {G0,W3,D2,L1,V0,M1} { ! e20 = e24 }.
% 0.75/1.37 (334) {G0,W3,D2,L1,V0,M1} { ! e21 = e22 }.
% 0.75/1.37 (335) {G0,W3,D2,L1,V0,M1} { ! e21 = e23 }.
% 0.75/1.37 (336) {G0,W3,D2,L1,V0,M1} { ! e21 = e24 }.
% 0.75/1.37 (337) {G0,W3,D2,L1,V0,M1} { ! e22 = e23 }.
% 0.75/1.37 (338) {G0,W3,D2,L1,V0,M1} { ! e22 = e24 }.
% 0.75/1.37 (339) {G0,W3,D2,L1,V0,M1} { ! e23 = e24 }.
% 0.75/1.37 (340) {G0,W3,D2,L1,V0,M1} { ! e10 = e20 }.
% 0.75/1.37 (341) {G0,W3,D2,L1,V0,M1} { ! e10 = e21 }.
% 0.75/1.37 (342) {G0,W3,D2,L1,V0,M1} { ! e10 = e22 }.
% 0.75/1.37 (343) {G0,W3,D2,L1,V0,M1} { ! e10 = e23 }.
% 0.75/1.37 (344) {G0,W3,D2,L1,V0,M1} { ! e10 = e24 }.
% 0.75/1.37 (345) {G0,W3,D2,L1,V0,M1} { ! e11 = e20 }.
% 0.75/1.37 (346) {G0,W3,D2,L1,V0,M1} { ! e11 = e21 }.
% 0.75/1.37 (347) {G0,W3,D2,L1,V0,M1} { ! e11 = e22 }.
% 0.75/1.37 (348) {G0,W3,D2,L1,V0,M1} { ! e11 = e23 }.
% 0.75/1.37 (349) {G0,W3,D2,L1,V0,M1} { ! e11 = e24 }.
% 0.75/1.37 (350) {G0,W3,D2,L1,V0,M1} { ! e12 = e20 }.
% 0.75/1.37 (351) {G0,W3,D2,L1,V0,M1} { ! e12 = e21 }.
% 0.75/1.37 (352) {G0,W3,D2,L1,V0,M1} { ! e12 = e22 }.
% 0.75/1.37 (353) {G0,W3,D2,L1,V0,M1} { ! e12 = e23 }.
% 0.75/1.37 (354) {G0,W3,D2,L1,V0,M1} { ! e12 = e24 }.
% 0.75/1.37 (355) {G0,W3,D2,L1,V0,M1} { ! e13 = e20 }.
% 0.75/1.37 (356) {G0,W3,D2,L1,V0,M1} { ! e13 = e21 }.
% 0.75/1.37 (357) {G0,W3,D2,L1,V0,M1} { ! e13 = e22 }.
% 0.75/1.37 (358) {G0,W3,D2,L1,V0,M1} { ! e13 = e23 }.
% 0.75/1.37 (359) {G0,W3,D2,L1,V0,M1} { ! e13 = e24 }.
% 0.75/1.37 (360) {G0,W3,D2,L1,V0,M1} { ! e14 = e20 }.
% 0.75/1.37 (361) {G0,W3,D2,L1,V0,M1} { ! e14 = e21 }.
% 0.75/1.37 (362) {G0,W3,D2,L1,V0,M1} { ! e14 = e22 }.
% 0.75/1.37 (363) {G0,W3,D2,L1,V0,M1} { ! e14 = e23 }.
% 0.75/1.37 (364) {G0,W3,D2,L1,V0,M1} { ! e14 = e24 }.
% 0.75/1.37 (365) {G0,W5,D3,L1,V0,M1} { op1( e10, e10 ) = e10 }.
% 0.75/1.37 (366) {G0,W5,D3,L1,V0,M1} { op1( e10, e11 ) = e11 }.
% 0.75/1.37 (367) {G0,W5,D3,L1,V0,M1} { op1( e10, e12 ) = e12 }.
% 0.75/1.37 (368) {G0,W5,D3,L1,V0,M1} { op1( e10, e13 ) = e13 }.
% 0.75/1.37 (369) {G0,W5,D3,L1,V0,M1} { op1( e10, e14 ) = e14 }.
% 0.75/1.37 (370) {G0,W5,D3,L1,V0,M1} { op1( e11, e10 ) = e11 }.
% 0.75/1.37 (371) {G0,W5,D3,L1,V0,M1} { op1( e11, e11 ) = e14 }.
% 0.75/1.37 (372) {G0,W5,D3,L1,V0,M1} { op1( e11, e12 ) = e10 }.
% 0.75/1.37 (373) {G0,W5,D3,L1,V0,M1} { op1( e11, e13 ) = e12 }.
% 0.75/1.37 (374) {G0,W5,D3,L1,V0,M1} { op1( e11, e14 ) = e13 }.
% 0.75/1.37 (375) {G0,W5,D3,L1,V0,M1} { op1( e12, e10 ) = e12 }.
% 0.75/1.37 (376) {G0,W5,D3,L1,V0,M1} { op1( e12, e11 ) = e10 }.
% 0.75/1.37 (377) {G0,W5,D3,L1,V0,M1} { op1( e12, e12 ) = e13 }.
% 0.75/1.37 (378) {G0,W5,D3,L1,V0,M1} { op1( e12, e13 ) = e14 }.
% 0.75/1.37 (379) {G0,W5,D3,L1,V0,M1} { op1( e12, e14 ) = e11 }.
% 0.75/1.37 (380) {G0,W5,D3,L1,V0,M1} { op1( e13, e10 ) = e13 }.
% 0.75/1.37 (381) {G0,W5,D3,L1,V0,M1} { op1( e13, e11 ) = e12 }.
% 0.75/1.37 (382) {G0,W5,D3,L1,V0,M1} { op1( e13, e12 ) = e14 }.
% 0.75/1.37 (383) {G0,W5,D3,L1,V0,M1} { op1( e13, e13 ) = e11 }.
% 0.75/1.37 (384) {G0,W5,D3,L1,V0,M1} { op1( e13, e14 ) = e10 }.
% 0.75/1.37 (385) {G0,W5,D3,L1,V0,M1} { op1( e14, e10 ) = e14 }.
% 0.75/1.37 (386) {G0,W5,D3,L1,V0,M1} { op1( e14, e11 ) = e13 }.
% 0.75/1.37 (387) {G0,W5,D3,L1,V0,M1} { op1( e14, e12 ) = e11 }.
% 0.75/1.37 (388) {G0,W5,D3,L1,V0,M1} { op1( e14, e13 ) = e10 }.
% 0.75/1.37 (389) {G0,W5,D3,L1,V0,M1} { op1( e14, e14 ) = e12 }.
% 0.75/1.37 (390) {G0,W5,D3,L1,V0,M1} { op2( e20, e20 ) = e20 }.
% 0.75/1.37 (391) {G0,W5,D3,L1,V0,M1} { op2( e20, e21 ) = e21 }.
% 0.75/1.37 (392) {G0,W5,D3,L1,V0,M1} { op2( e20, e22 ) = e22 }.
% 0.75/1.37 (393) {G0,W5,D3,L1,V0,M1} { op2( e20, e23 ) = e23 }.
% 0.75/1.37 (394) {G0,W5,D3,L1,V0,M1} { op2( e20, e24 ) = e24 }.
% 0.75/1.37 (395) {G0,W5,D3,L1,V0,M1} { op2( e21, e20 ) = e21 }.
% 0.75/1.37 (396) {G0,W5,D3,L1,V0,M1} { op2( e21, e21 ) = e22 }.
% 0.75/1.37 (397) {G0,W5,D3,L1,V0,M1} { op2( e21, e22 ) = e24 }.
% 0.75/1.37 (398) {G0,W5,D3,L1,V0,M1} { op2( e21, e23 ) = e20 }.
% 0.75/1.37 (399) {G0,W5,D3,L1,V0,M1} { op2( e21, e24 ) = e23 }.
% 0.75/1.37 (400) {G0,W5,D3,L1,V0,M1} { op2( e22, e20 ) = e22 }.
% 0.75/1.37 (401) {G0,W5,D3,L1,V0,M1} { op2( e22, e21 ) = e20 }.
% 0.75/1.37 (402) {G0,W5,D3,L1,V0,M1} { op2( e22, e22 ) = e23 }.
% 0.75/1.37 (403) {G0,W5,D3,L1,V0,M1} { op2( e22, e23 ) = e24 }.
% 0.75/1.37 (404) {G0,W5,D3,L1,V0,M1} { op2( e22, e24 ) = e21 }.
% 0.75/1.37 (405) {G0,W5,D3,L1,V0,M1} { op2( e23, e20 ) = e23 }.
% 0.75/1.37 (406) {G0,W5,D3,L1,V0,M1} { op2( e23, e21 ) = e24 }.
% 0.75/1.37 (407) {G0,W5,D3,L1,V0,M1} { op2( e23, e22 ) = e20 }.
% 0.75/1.37 (408) {G0,W5,D3,L1,V0,M1} { op2( e23, e23 ) = e21 }.
% 0.75/1.37 (409) {G0,W5,D3,L1,V0,M1} { op2( e23, e24 ) = e22 }.
% 0.75/1.37 (410) {G0,W5,D3,L1,V0,M1} { op2( e24, e20 ) = e24 }.
% 0.75/1.37 (411) {G0,W5,D3,L1,V0,M1} { op2( e24, e21 ) = e23 }.
% 0.75/1.37 (412) {G0,W5,D3,L1,V0,M1} { op2( e24, e22 ) = e21 }.
% 0.75/1.37 (413) {G0,W5,D3,L1,V0,M1} { op2( e24, e23 ) = e22 }.
% 0.75/1.37 (414) {G0,W5,D3,L1,V0,M1} { op2( e24, e24 ) = e20 }.
% 0.75/1.37 (415) {G0,W20,D3,L5,V0,M5} { h( e10 ) = e20, h( e10 ) = e21, h( e10 ) =
% 0.75/1.37 e22, h( e10 ) = e23, h( e10 ) = e24 }.
% 0.75/1.37 (416) {G0,W20,D3,L5,V0,M5} { h( e11 ) = e20, h( e11 ) = e21, h( e11 ) =
% 0.75/1.37 e22, h( e11 ) = e23, h( e11 ) = e24 }.
% 0.75/1.37 (417) {G0,W20,D3,L5,V0,M5} { h( e12 ) = e20, h( e12 ) = e21, h( e12 ) =
% 0.75/1.37 e22, h( e12 ) = e23, h( e12 ) = e24 }.
% 0.75/1.37 (418) {G0,W20,D3,L5,V0,M5} { h( e13 ) = e20, h( e13 ) = e21, h( e13 ) =
% 0.75/1.37 e22, h( e13 ) = e23, h( e13 ) = e24 }.
% 0.75/1.37 (419) {G0,W20,D3,L5,V0,M5} { h( e14 ) = e20, h( e14 ) = e21, h( e14 ) =
% 0.75/1.37 e22, h( e14 ) = e23, h( e14 ) = e24 }.
% 0.75/1.37 (420) {G0,W20,D3,L5,V0,M5} { j( e20 ) = e10, j( e20 ) = e11, j( e20 ) =
% 0.75/1.37 e12, j( e20 ) = e13, j( e20 ) = e14 }.
% 0.75/1.37 (421) {G0,W20,D3,L5,V0,M5} { j( e21 ) = e10, j( e21 ) = e11, j( e21 ) =
% 0.75/1.37 e12, j( e21 ) = e13, j( e21 ) = e14 }.
% 0.75/1.37 (422) {G0,W20,D3,L5,V0,M5} { j( e22 ) = e10, j( e22 ) = e11, j( e22 ) =
% 0.75/1.37 e12, j( e22 ) = e13, j( e22 ) = e14 }.
% 0.75/1.37 (423) {G0,W20,D3,L5,V0,M5} { j( e23 ) = e10, j( e23 ) = e11, j( e23 ) =
% 0.75/1.37 e12, j( e23 ) = e13, j( e23 ) = e14 }.
% 0.75/1.37 (424) {G0,W20,D3,L5,V0,M5} { j( e24 ) = e10, j( e24 ) = e11, j( e24 ) =
% 0.75/1.37 e12, j( e24 ) = e13, j( e24 ) = e14 }.
% 0.75/1.37 (425) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e10 ) ) = op2( h( e10 ), h( e10
% 0.75/1.37 ) ) }.
% 0.75/1.37 (426) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e11 ) ) = op2( h( e10 ), h( e11
% 0.75/1.37 ) ) }.
% 0.75/1.37 (427) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e12 ) ) = op2( h( e10 ), h( e12
% 0.75/1.37 ) ) }.
% 0.75/1.37 (428) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e13 ) ) = op2( h( e10 ), h( e13
% 0.75/1.37 ) ) }.
% 0.75/1.37 (429) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e14 ) ) = op2( h( e10 ), h( e14
% 0.75/1.37 ) ) }.
% 0.75/1.37 (430) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e10 ) ) = op2( h( e11 ), h( e10
% 0.75/1.37 ) ) }.
% 0.75/1.37 (431) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e11 ) ) = op2( h( e11 ), h( e11
% 0.75/1.37 ) ) }.
% 0.75/1.37 (432) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e12 ) ) = op2( h( e11 ), h( e12
% 0.75/1.37 ) ) }.
% 0.75/1.37 (433) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e13 ) ) = op2( h( e11 ), h( e13
% 0.75/1.37 ) ) }.
% 0.75/1.37 (434) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e14 ) ) = op2( h( e11 ), h( e14
% 0.75/1.37 ) ) }.
% 0.75/1.37 (435) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e10 ) ) = op2( h( e12 ), h( e10
% 0.75/1.37 ) ) }.
% 0.75/1.37 (436) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e11 ) ) = op2( h( e12 ), h( e11
% 0.75/1.37 ) ) }.
% 0.75/1.37 (437) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e12 ) ) = op2( h( e12 ), h( e12
% 0.75/1.37 ) ) }.
% 0.75/1.37 (438) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e13 ) ) = op2( h( e12 ), h( e13
% 0.75/1.37 ) ) }.
% 0.75/1.37 (439) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e14 ) ) = op2( h( e12 ), h( e14
% 0.75/1.37 ) ) }.
% 0.75/1.37 (440) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e10 ) ) = op2( h( e13 ), h( e10
% 0.75/1.37 ) ) }.
% 0.75/1.37 (441) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e11 ) ) = op2( h( e13 ), h( e11
% 0.75/1.37 ) ) }.
% 0.75/1.37 (442) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e12 ) ) = op2( h( e13 ), h( e12
% 0.75/1.37 ) ) }.
% 0.75/1.37 (443) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e13 ) ) = op2( h( e13 ), h( e13
% 0.75/1.37 ) ) }.
% 0.75/1.37 (444) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e14 ) ) = op2( h( e13 ), h( e14
% 0.75/1.37 ) ) }.
% 0.75/1.37 (445) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e10 ) ) = op2( h( e14 ), h( e10
% 0.75/1.37 ) ) }.
% 0.75/1.37 (446) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e11 ) ) = op2( h( e14 ), h( e11
% 0.75/1.37 ) ) }.
% 0.75/1.37 (447) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e12 ) ) = op2( h( e14 ), h( e12
% 0.75/1.37 ) ) }.
% 0.75/1.37 (448) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e13 ) ) = op2( h( e14 ), h( e13
% 0.75/1.37 ) ) }.
% 0.75/1.37 (449) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e14 ) ) = op2( h( e14 ), h( e14
% 0.75/1.37 ) ) }.
% 0.75/1.37 (450) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e20 ) ) = op1( j( e20 ), j( e20
% 0.75/1.37 ) ) }.
% 0.75/1.37 (451) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e21 ) ) = op1( j( e20 ), j( e21
% 0.75/1.37 ) ) }.
% 0.75/1.37 (452) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e22 ) ) = op1( j( e20 ), j( e22
% 0.75/1.37 ) ) }.
% 0.75/1.37 (453) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e23 ) ) = op1( j( e20 ), j( e23
% 0.75/1.37 ) ) }.
% 0.75/1.37 (454) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e24 ) ) = op1( j( e20 ), j( e24
% 0.75/1.37 ) ) }.
% 0.75/1.37 (455) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e20 ) ) = op1( j( e21 ), j( e20
% 0.75/1.37 ) ) }.
% 0.75/1.37 (456) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e21 ) ) = op1( j( e21 ), j( e21
% 0.75/1.37 ) ) }.
% 0.75/1.37 (457) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e22 ) ) = op1( j( e21 ), j( e22
% 0.75/1.37 ) ) }.
% 0.75/1.37 (458) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e23 ) ) = op1( j( e21 ), j( e23
% 0.75/1.37 ) ) }.
% 0.75/1.37 (459) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e24 ) ) = op1( j( e21 ), j( e24
% 0.75/1.37 ) ) }.
% 0.75/1.37 (460) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e20 ) ) = op1( j( e22 ), j( e20
% 0.75/1.37 ) ) }.
% 0.75/1.37 (461) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e21 ) ) = op1( j( e22 ), j( e21
% 0.75/1.37 ) ) }.
% 0.75/1.37 (462) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e22 ) ) = op1( j( e22 ), j( e22
% 0.75/1.37 ) ) }.
% 0.75/1.37 (463) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e23 ) ) = op1( j( e22 ), j( e23
% 0.75/1.37 ) ) }.
% 0.75/1.37 (464) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e24 ) ) = op1( j( e22 ), j( e24
% 0.75/1.37 ) ) }.
% 0.75/1.37 (465) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e20 ) ) = op1( j( e23 ), j( e20
% 0.75/1.37 ) ) }.
% 0.75/1.37 (466) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e21 ) ) = op1( j( e23 ), j( e21
% 0.75/1.37 ) ) }.
% 0.75/1.37 (467) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e22 ) ) = op1( j( e23 ), j( e22
% 0.75/1.37 ) ) }.
% 0.75/1.37 (468) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e23 ) ) = op1( j( e23 ), j( e23
% 0.75/1.37 ) ) }.
% 0.75/1.37 (469) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e24 ) ) = op1( j( e23 ), j( e24
% 0.75/1.37 ) ) }.
% 0.75/1.37 (470) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e20 ) ) = op1( j( e24 ), j( e20
% 0.75/1.37 ) ) }.
% 0.75/1.37 (471) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e21 ) ) = op1( j( e24 ), j( e21
% 0.75/1.37 ) ) }.
% 0.75/1.37 (472) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e22 ) ) = op1( j( e24 ), j( e22
% 0.75/1.37 ) ) }.
% 0.75/1.37 (473) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e23 ) ) = op1( j( e24 ), j( e23
% 0.75/1.37 ) ) }.
% 0.75/1.37 (474) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e24 ) ) = op1( j( e24 ), j( e24
% 0.75/1.37 ) ) }.
% 0.75/1.37 (475) {G0,W5,D4,L1,V0,M1} { h( j( e20 ) ) = e20 }.
% 0.75/1.37 (476) {G0,W5,D4,L1,V0,M1} { h( j( e21 ) ) = e21 }.
% 0.75/1.37 (477) {G0,W5,D4,L1,V0,M1} { h( j( e22 ) ) = e22 }.
% 0.75/1.37 (478) {G0,W5,D4,L1,V0,M1} { h( j( e23 ) ) = e23 }.
% 0.75/1.37 (479) {G0,W5,D4,L1,V0,M1} { h( j( e24 ) ) = e24 }.
% 0.75/1.37 (480) {G0,W5,D4,L1,V0,M1} { j( h( e10 ) ) = e10 }.
% 0.75/1.37 (481) {G0,W5,D4,L1,V0,M1} { j( h( e11 ) ) = e11 }.
% 0.75/1.37 (482) {G0,W5,D4,L1,V0,M1} { j( h( e12 ) ) = e12 }.
% 0.75/1.37 (483) {G0,W5,D4,L1,V0,M1} { j( h( e13 ) ) = e13 }.
% 0.75/1.37 (484) {G0,W5,D4,L1,V0,M1} { j( h( e14 ) ) = e14 }.
% 0.75/1.37
% 0.75/1.37
% 0.75/1.37 Total Proof:
% 0.75/1.37
% 0.75/1.37 eqswap: (488) {G0,W3,D2,L1,V0,M1} { ! e14 = e10 }.
% 0.75/1.37 parent0[0]: (323) {G0,W3,D2,L1,V0,M1} { ! e10 = e14 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (3) {G0,W3,D2,L1,V0,M1} I { ! e14 ==> e10 }.
% 0.75/1.37 parent0: (488) {G0,W3,D2,L1,V0,M1} { ! e14 = e10 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 eqswap: (495) {G0,W3,D2,L1,V0,M1} { ! e14 = e11 }.
% 0.75/1.37 parent0[0]: (326) {G0,W3,D2,L1,V0,M1} { ! e11 = e14 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (6) {G0,W3,D2,L1,V0,M1} I { ! e14 ==> e11 }.
% 0.75/1.37 parent0: (495) {G0,W3,D2,L1,V0,M1} { ! e14 = e11 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 eqswap: (509) {G0,W3,D2,L1,V0,M1} { ! e24 = e20 }.
% 0.75/1.37 parent0[0]: (333) {G0,W3,D2,L1,V0,M1} { ! e20 = e24 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (13) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e20 }.
% 0.75/1.37 parent0: (509) {G0,W3,D2,L1,V0,M1} { ! e24 = e20 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 eqswap: (524) {G0,W3,D2,L1,V0,M1} { ! e22 = e21 }.
% 0.75/1.37 parent0[0]: (334) {G0,W3,D2,L1,V0,M1} { ! e21 = e22 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (14) {G0,W3,D2,L1,V0,M1} I { ! e22 ==> e21 }.
% 0.75/1.37 parent0: (524) {G0,W3,D2,L1,V0,M1} { ! e22 = e21 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 eqswap: (540) {G0,W3,D2,L1,V0,M1} { ! e23 = e21 }.
% 0.75/1.37 parent0[0]: (335) {G0,W3,D2,L1,V0,M1} { ! e21 = e23 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (15) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e21 }.
% 0.75/1.37 parent0: (540) {G0,W3,D2,L1,V0,M1} { ! e23 = e21 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 eqswap: (557) {G0,W3,D2,L1,V0,M1} { ! e24 = e21 }.
% 0.75/1.37 parent0[0]: (336) {G0,W3,D2,L1,V0,M1} { ! e21 = e24 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (16) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e21 }.
% 0.75/1.37 parent0: (557) {G0,W3,D2,L1,V0,M1} { ! e24 = e21 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 eqswap: (575) {G0,W3,D2,L1,V0,M1} { ! e23 = e22 }.
% 0.75/1.37 parent0[0]: (337) {G0,W3,D2,L1,V0,M1} { ! e22 = e23 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (17) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e22 }.
% 0.75/1.37 parent0: (575) {G0,W3,D2,L1,V0,M1} { ! e23 = e22 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (45) {G0,W5,D3,L1,V0,M1} I { op1( e10, e10 ) ==> e10 }.
% 0.75/1.37 parent0: (365) {G0,W5,D3,L1,V0,M1} { op1( e10, e10 ) = e10 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (47) {G0,W5,D3,L1,V0,M1} I { op1( e10, e12 ) ==> e12 }.
% 0.75/1.37 parent0: (367) {G0,W5,D3,L1,V0,M1} { op1( e10, e12 ) = e12 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (48) {G0,W5,D3,L1,V0,M1} I { op1( e10, e13 ) ==> e13 }.
% 0.75/1.37 parent0: (368) {G0,W5,D3,L1,V0,M1} { op1( e10, e13 ) = e13 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (51) {G0,W5,D3,L1,V0,M1} I { op1( e11, e11 ) ==> e14 }.
% 0.75/1.37 parent0: (371) {G0,W5,D3,L1,V0,M1} { op1( e11, e11 ) = e14 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (52) {G0,W5,D3,L1,V0,M1} I { op1( e11, e12 ) ==> e10 }.
% 0.75/1.37 parent0: (372) {G0,W5,D3,L1,V0,M1} { op1( e11, e12 ) = e10 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (53) {G0,W5,D3,L1,V0,M1} I { op1( e11, e13 ) ==> e12 }.
% 0.75/1.37 parent0: (373) {G0,W5,D3,L1,V0,M1} { op1( e11, e13 ) = e12 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (54) {G0,W5,D3,L1,V0,M1} I { op1( e11, e14 ) ==> e13 }.
% 0.75/1.37 parent0: (374) {G0,W5,D3,L1,V0,M1} { op1( e11, e14 ) = e13 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (63) {G0,W5,D3,L1,V0,M1} I { op1( e13, e13 ) ==> e11 }.
% 0.75/1.37 parent0: (383) {G0,W5,D3,L1,V0,M1} { op1( e13, e13 ) = e11 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 *** allocated 50625 integers for clauses
% 0.75/1.37 subsumption: (70) {G0,W5,D3,L1,V0,M1} I { op2( e20, e20 ) ==> e20 }.
% 0.75/1.37 parent0: (390) {G0,W5,D3,L1,V0,M1} { op2( e20, e20 ) = e20 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 *** allocated 15000 integers for termspace/termends
% 0.75/1.37 subsumption: (76) {G0,W5,D3,L1,V0,M1} I { op2( e21, e21 ) ==> e22 }.
% 0.75/1.37 parent0: (396) {G0,W5,D3,L1,V0,M1} { op2( e21, e21 ) = e22 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (77) {G0,W5,D3,L1,V0,M1} I { op2( e21, e22 ) ==> e24 }.
% 0.75/1.37 parent0: (397) {G0,W5,D3,L1,V0,M1} { op2( e21, e22 ) = e24 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (82) {G0,W5,D3,L1,V0,M1} I { op2( e22, e22 ) ==> e23 }.
% 0.75/1.37 parent0: (402) {G0,W5,D3,L1,V0,M1} { op2( e22, e22 ) = e23 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (83) {G0,W5,D3,L1,V0,M1} I { op2( e22, e23 ) ==> e24 }.
% 0.75/1.37 parent0: (403) {G0,W5,D3,L1,V0,M1} { op2( e22, e23 ) = e24 }.
% 0.75/1.37 substitution0:
% 0.75/1.37 end
% 0.75/1.37 permutation0:
% 0.75/1.37 0 ==> 0
% 0.75/1.37 end
% 0.75/1.37
% 0.75/1.37 subsumption: (86) {G0,W5,D3,L1,V0,M1} I { op2( e23, e21 ) ==> e24 }.
% 0.75/1.37 parent0: (406) {G0,W5,D3,L1,V0,M1} { op2( e23, e21 ) = e24 }.
% 0.75/1.39 substitution0:
% 0.75/1.39 end
% 0.75/1.39 permutation0:
% 0.75/1.39 0 ==> 0
% 0.75/1.39 end
% 0.75/1.39
% 0.75/1.39 subsumption: (88) {G0,W5,D3,L1,V0,M1} I { op2( e23, e23 ) ==> e21 }.
% 0.75/1.39 parent0: (408) {G0,W5,D3,L1,V0,M1} { op2( e23, e23 ) = e21 }.
% 0.75/1.39 substitution0:
% 0.75/1.39 end
% 0.75/1.39 permutation0:
% 0.75/1.39 0 ==> 0
% 0.75/1.39 end
% 0.75/1.39
% 0.75/1.39 subsumption: (94) {G0,W5,D3,L1,V0,M1} I { op2( e24, e24 ) ==> e20 }.
% 0.75/1.39 parent0: (414) {G0,W5,D3,L1,V0,M1} { op2( e24, e24 ) = e20 }.
% 0.75/1.39 substitution0:
% 0.75/1.39 end
% 0.75/1.39 permutation0:
% 0.75/1.39 0 ==> 0
% 0.75/1.39 end
% 0.75/1.39
% 0.75/1.39 subsumption: (95) {G0,W20,D3,L5,V0,M5} I { h( e10 ) ==> e20, h( e10 ) ==>
% 0.75/1.39 e21, h( e10 ) ==> e22, h( e10 ) ==> e23, h( e10 ) ==> e24 }.
% 0.75/1.39 parent0: (415) {G0,W20,D3,L5,V0,M5} { h( e10 ) = e20, h( e10 ) = e21, h(
% 0.75/1.39 e10 ) = e22, h( e10 ) = e23, h( e10 ) = e24 }.
% 0.75/1.39 substitution0:
% 0.75/1.39 end
% 0.75/1.39 permutation0:
% 0.75/1.39 0 ==> 0
% 0.75/1.39 1 ==> 1
% 0.75/1.39 2 ==> 2
% 0.75/1.39 3 ==> 3
% 0.75/1.39 4 ==> 4
% 0.75/1.39 end
% 0.75/1.39
% 0.75/1.39 *** allocated 75937 integers for clauses
% 0.75/1.39 *** allocated 22500 integers for termspace/termends
% 0.75/1.39 subsumption: (96) {G0,W20,D3,L5,V0,M5} I { h( e11 ) ==> e20, h( e11 ) ==>
% 0.75/1.39 e21, h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 0.75/1.39 parent0: (416) {G0,W20,D3,L5,V0,M5} { h( e11 ) = e20, h( e11 ) = e21, h(
% 0.75/1.39 e11 ) = e22, h( e11 ) = e23, h( e11 ) = e24 }.
% 0.75/1.39 substitution0:
% 0.75/1.39 end
% 0.75/1.39 permutation0:
% 0.75/1.39 0 ==> 0
% 0.75/1.39 1 ==> 1
% 0.75/1.39 2 ==> 2
% 0.75/1.39 3 ==> 3
% 0.75/1.39 4 ==> 4
% 0.75/1.39 end
% 0.75/1.39
% 0.75/1.39 paramod: (2458) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e10 ), h( e10 ) )
% 0.75/1.39 }.
% 0.75/1.39 parent0[0]: (45) {G0,W5,D3,L1,V0,M1} I { op1( e10, e10 ) ==> e10 }.
% 0.75/1.39 parent1[0; 2]: (425) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e10 ) ) = op2( h
% 0.75/1.39 ( e10 ), h( e10 ) ) }.
% 0.75/1.39 substitution0:
% 0.75/1.39 end
% 0.75/1.39 substitution1:
% 0.75/1.39 end
% 0.75/1.39
% 0.75/1.39 eqswap: (2459) {G1,W8,D4,L1,V0,M1} { op2( h( e10 ), h( e10 ) ) = h( e10 )
% 0.75/1.39 }.
% 0.75/1.39 parent0[0]: (2458) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e10 ), h( e10
% 0.75/1.39 ) ) }.
% 0.75/1.39 substitution0:
% 0.75/1.39 end
% 0.75/1.39
% 0.75/1.39 subsumption: (105) {G1,W8,D4,L1,V0,M1} I;d(45) { op2( h( e10 ), h( e10 ) )
% 0.75/1.39 ==> h( e10 ) }.
% 0.75/1.39 parent0: (2459) {G1,W8,D4,L1,V0,M1} { op2( h( e10 ), h( e10 ) ) = h( e10 )
% 0.75/1.39 }.
% 0.75/1.39 substitution0:
% 0.75/1.39 end
% 0.75/1.39 permutation0:
% 0.75/1.39 0 ==> 0
% 0.75/1.39 end
% 0.75/1.39
% 0.75/1.39 *** allocated 33750 integers for termspace/termends
% 0.75/1.39 paramod: (2978) {G1,W8,D4,L1,V0,M1} { h( e12 ) = op2( h( e10 ), h( e12 ) )
% 0.75/1.39 }.
% 0.75/1.39 parent0[0]: (47) {G0,W5,D3,L1,V0,M1} I { op1( e10, e12 ) ==> e12 }.
% 0.75/1.39 parent1[0; 2]: (427) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e12 ) ) = op2( h
% 0.75/1.39 ( e10 ), h( e12 ) ) }.
% 0.75/1.39 substitution0:
% 0.75/1.39 end
% 0.75/1.39 substitution1:
% 0.75/1.39 end
% 0.75/1.39
% 0.75/1.39 eqswap: (2979) {G1,W8,D4,L1,V0,M1} { op2( h( e10 ), h( e12 ) ) = h( e12 )
% 0.75/1.39 }.
% 0.75/1.39 parent0[0]: (2978) {G1,W8,D4,L1,V0,M1} { h( e12 ) = op2( h( e10 ), h( e12
% 0.75/1.39 ) ) }.
% 0.75/1.39 substitution0:
% 0.75/1.39 end
% 0.75/1.39
% 0.75/1.39 subsumption: (107) {G1,W8,D4,L1,V0,M1} I;d(47) { op2( h( e10 ), h( e12 ) )
% 0.75/1.39 ==> h( e12 ) }.
% 0.75/1.39 parent0: (2979) {G1,W8,D4,L1,V0,M1} { op2( h( e10 ), h( e12 ) ) = h( e12 )
% 0.75/1.39 }.
% 0.75/1.39 substitution0:
% 0.75/1.39 end
% 0.75/1.39 permutation0:
% 0.75/1.39 0 ==> 0
% 0.75/1.39 end
% 0.75/1.39
% 0.75/1.39 *** allocated 113905 integers for clauses
% 0.75/1.39 *** allocated 50625 integers for termspace/termends
% 0.75/1.39 paramod: (3500) {G1,W8,D4,L1,V0,M1} { h( e13 ) = op2( h( e10 ), h( e13 ) )
% 0.75/1.39 }.
% 0.75/1.39 parent0[0]: (48) {G0,W5,D3,L1,V0,M1} I { op1( e10, e13 ) ==> e13 }.
% 0.75/1.39 parent1[0; 2]: (428) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e13 ) ) = op2( h
% 0.75/1.39 ( e10 ), h( e13 ) ) }.
% 0.75/1.39 substitution0:
% 0.75/1.39 end
% 0.75/1.39 substitution1:
% 0.75/1.39 end
% 0.75/1.39
% 0.75/1.39 eqswap: (3501) {G1,W8,D4,L1,V0,M1} { op2( h( e10 ), h( e13 ) ) = h( e13 )
% 0.75/1.39 }.
% 0.75/1.39 parent0[0]: (3500) {G1,W8,D4,L1,V0,M1} { h( e13 ) = op2( h( e10 ), h( e13
% 0.75/1.39 ) ) }.
% 0.75/1.39 substitution0:
% 0.75/1.39 end
% 0.75/1.39
% 0.75/1.39 subsumption: (108) {G1,W8,D4,L1,V0,M1} I;d(48) { op2( h( e10 ), h( e13 ) )
% 0.75/1.39 ==> h( e13 ) }.
% 0.75/1.39 parent0: (3501) {G1,W8,D4,L1,V0,M1} { op2( h( e10 ), h( e13 ) ) = h( e13 )
% 0.75/1.39 }.
% 0.75/1.39 substitution0:
% 0.75/1.39 end
% 0.75/1.39 permutation0:
% 0.75/1.39 0 ==> 0
% 0.75/1.39 end
% 0.75/1.39
% 0.75/1.39 paramod: (4028) {G1,W8,D4,L1,V0,M1} { h( e14 ) = op2( h( e11 ), h( e11 ) )
% 0.75/1.39 }.
% 0.75/1.39 parent0[0]: (51) {G0,W5,D3,L1,V0,M1} I { op1( e11, e11 ) ==> e14 }.
% 0.75/1.39 parent1[0; 2]: (431) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e11 ) ) = op2( h
% 0.75/1.39 ( e11 ), h( e11 ) ) }.
% 0.75/1.39 substitution0:
% 0.75/1.39 end
% 0.75/1.39 substitution1:
% 0.75/1.39 end
% 0.75/1.39
% 0.75/1.39 eqswap: (4029) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e11 ) ) = h( e14 )
% 0.75/1.39 }.
% 0.75/1.39 parent0[0]: (4028) {G1,W8,D4,L1,V0,M1} { h( e14 ) = op2( h( e11 ), h( e11
% 0.75/1.39 ) ) }.
% 0.75/1.39 substitution0:
% 0.75/1.39 end
% 0.75/1.39
% 0.75/1.39 subsumption: (111) {G1,W8,D4,L1,V0,M1} I;d(51) { op2( h( e11 ), h( e11 ) )
% 0.75/1.39 ==> h( e14 ) }.
% 0.75/1.39 parent0: (4029) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e11 ) ) = h( e14 )
% 0.75/1.41 }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41 permutation0:
% 0.75/1.41 0 ==> 0
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 *** allocated 75937 integers for termspace/termends
% 0.75/1.41 paramod: (4558) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e11 ), h( e12 ) )
% 0.75/1.41 }.
% 0.75/1.41 parent0[0]: (52) {G0,W5,D3,L1,V0,M1} I { op1( e11, e12 ) ==> e10 }.
% 0.75/1.41 parent1[0; 2]: (432) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e12 ) ) = op2( h
% 0.75/1.41 ( e11 ), h( e12 ) ) }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41 substitution1:
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 eqswap: (4559) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e12 ) ) = h( e10 )
% 0.75/1.41 }.
% 0.75/1.41 parent0[0]: (4558) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e11 ), h( e12
% 0.75/1.41 ) ) }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 subsumption: (112) {G1,W8,D4,L1,V0,M1} I;d(52) { op2( h( e11 ), h( e12 ) )
% 0.75/1.41 ==> h( e10 ) }.
% 0.75/1.41 parent0: (4559) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e12 ) ) = h( e10 )
% 0.75/1.41 }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41 permutation0:
% 0.75/1.41 0 ==> 0
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 *** allocated 170857 integers for clauses
% 0.75/1.41 paramod: (5090) {G1,W8,D4,L1,V0,M1} { h( e12 ) = op2( h( e11 ), h( e13 ) )
% 0.75/1.41 }.
% 0.75/1.41 parent0[0]: (53) {G0,W5,D3,L1,V0,M1} I { op1( e11, e13 ) ==> e12 }.
% 0.75/1.41 parent1[0; 2]: (433) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e13 ) ) = op2( h
% 0.75/1.41 ( e11 ), h( e13 ) ) }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41 substitution1:
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 eqswap: (5091) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e13 ) ) = h( e12 )
% 0.75/1.41 }.
% 0.75/1.41 parent0[0]: (5090) {G1,W8,D4,L1,V0,M1} { h( e12 ) = op2( h( e11 ), h( e13
% 0.75/1.41 ) ) }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 subsumption: (113) {G1,W8,D4,L1,V0,M1} I;d(53) { op2( h( e11 ), h( e13 ) )
% 0.75/1.41 ==> h( e12 ) }.
% 0.75/1.41 parent0: (5091) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e13 ) ) = h( e12 )
% 0.75/1.41 }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41 permutation0:
% 0.75/1.41 0 ==> 0
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 paramod: (5624) {G1,W8,D4,L1,V0,M1} { h( e13 ) = op2( h( e11 ), h( e14 ) )
% 0.75/1.41 }.
% 0.75/1.41 parent0[0]: (54) {G0,W5,D3,L1,V0,M1} I { op1( e11, e14 ) ==> e13 }.
% 0.75/1.41 parent1[0; 2]: (434) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e14 ) ) = op2( h
% 0.75/1.41 ( e11 ), h( e14 ) ) }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41 substitution1:
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 eqswap: (5625) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e14 ) ) = h( e13 )
% 0.75/1.41 }.
% 0.75/1.41 parent0[0]: (5624) {G1,W8,D4,L1,V0,M1} { h( e13 ) = op2( h( e11 ), h( e14
% 0.75/1.41 ) ) }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 subsumption: (114) {G1,W8,D4,L1,V0,M1} I;d(54) { op2( h( e11 ), h( e14 ) )
% 0.75/1.41 ==> h( e13 ) }.
% 0.75/1.41 parent0: (5625) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e14 ) ) = h( e13 )
% 0.75/1.41 }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41 permutation0:
% 0.75/1.41 0 ==> 0
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 paramod: (6176) {G1,W8,D4,L1,V0,M1} { h( e11 ) = op2( h( e13 ), h( e13 ) )
% 0.75/1.41 }.
% 0.75/1.41 parent0[0]: (63) {G0,W5,D3,L1,V0,M1} I { op1( e13, e13 ) ==> e11 }.
% 0.75/1.41 parent1[0; 2]: (443) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e13 ) ) = op2( h
% 0.75/1.41 ( e13 ), h( e13 ) ) }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41 substitution1:
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 eqswap: (6177) {G1,W8,D4,L1,V0,M1} { op2( h( e13 ), h( e13 ) ) = h( e11 )
% 0.75/1.41 }.
% 0.75/1.41 parent0[0]: (6176) {G1,W8,D4,L1,V0,M1} { h( e11 ) = op2( h( e13 ), h( e13
% 0.75/1.41 ) ) }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 subsumption: (123) {G1,W8,D4,L1,V0,M1} I;d(63) { op2( h( e13 ), h( e13 ) )
% 0.75/1.41 ==> h( e11 ) }.
% 0.75/1.41 parent0: (6177) {G1,W8,D4,L1,V0,M1} { op2( h( e13 ), h( e13 ) ) = h( e11 )
% 0.75/1.41 }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41 permutation0:
% 0.75/1.41 0 ==> 0
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 *** allocated 113905 integers for termspace/termends
% 0.75/1.41 paramod: (6742) {G1,W8,D4,L1,V0,M1} { j( e20 ) = op1( j( e20 ), j( e20 ) )
% 0.75/1.41 }.
% 0.75/1.41 parent0[0]: (70) {G0,W5,D3,L1,V0,M1} I { op2( e20, e20 ) ==> e20 }.
% 0.75/1.41 parent1[0; 2]: (450) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e20 ) ) = op1( j
% 0.75/1.41 ( e20 ), j( e20 ) ) }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41 substitution1:
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 eqswap: (6743) {G1,W8,D4,L1,V0,M1} { op1( j( e20 ), j( e20 ) ) = j( e20 )
% 0.75/1.41 }.
% 0.75/1.41 parent0[0]: (6742) {G1,W8,D4,L1,V0,M1} { j( e20 ) = op1( j( e20 ), j( e20
% 0.75/1.41 ) ) }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 subsumption: (130) {G1,W8,D4,L1,V0,M1} I;d(70) { op1( j( e20 ), j( e20 ) )
% 0.75/1.41 ==> j( e20 ) }.
% 0.75/1.41 parent0: (6743) {G1,W8,D4,L1,V0,M1} { op1( j( e20 ), j( e20 ) ) = j( e20 )
% 0.75/1.41 }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41 permutation0:
% 0.75/1.41 0 ==> 0
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 *** allocated 256285 integers for clauses
% 0.75/1.41 paramod: (7356) {G1,W8,D4,L1,V0,M1} { j( e20 ) = op1( j( e24 ), j( e24 ) )
% 0.75/1.41 }.
% 0.75/1.41 parent0[0]: (94) {G0,W5,D3,L1,V0,M1} I { op2( e24, e24 ) ==> e20 }.
% 0.75/1.41 parent1[0; 2]: (474) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e24 ) ) = op1( j
% 0.75/1.41 ( e24 ), j( e24 ) ) }.
% 0.75/1.41 substitution0:
% 0.75/1.41 end
% 0.75/1.41 substitution1:
% 0.75/1.41 end
% 0.75/1.41
% 0.75/1.41 eqswap: (7357) {G1,W8,D4,L1,V0,M1} { op1( j( e24 ), j( e24 ) ) = j( e20 )
% 1.60/1.98 }.
% 1.60/1.98 parent0[0]: (7356) {G1,W8,D4,L1,V0,M1} { j( e20 ) = op1( j( e24 ), j( e24
% 1.60/1.98 ) ) }.
% 1.60/1.98 substitution0:
% 1.60/1.98 end
% 1.60/1.98
% 1.60/1.98 subsumption: (154) {G1,W8,D4,L1,V0,M1} I;d(94) { op1( j( e24 ), j( e24 ) )
% 1.60/1.98 ==> j( e20 ) }.
% 1.60/1.98 parent0: (7357) {G1,W8,D4,L1,V0,M1} { op1( j( e24 ), j( e24 ) ) = j( e20 )
% 1.60/1.98 }.
% 1.60/1.98 substitution0:
% 1.60/1.98 end
% 1.60/1.98 permutation0:
% 1.60/1.98 0 ==> 0
% 1.60/1.98 end
% 1.60/1.98
% 1.60/1.98 subsumption: (160) {G0,W5,D4,L1,V0,M1} I { j( h( e10 ) ) ==> e10 }.
% 1.60/1.98 parent0: (480) {G0,W5,D4,L1,V0,M1} { j( h( e10 ) ) = e10 }.
% 1.60/1.98 substitution0:
% 1.60/1.98 end
% 1.60/1.98 permutation0:
% 1.60/1.98 0 ==> 0
% 1.60/1.98 end
% 1.60/1.98
% 1.60/1.98 subsumption: (161) {G0,W5,D4,L1,V0,M1} I { j( h( e11 ) ) ==> e11 }.
% 1.60/1.98 parent0: (481) {G0,W5,D4,L1,V0,M1} { j( h( e11 ) ) = e11 }.
% 1.60/1.98 substitution0:
% 1.60/1.98 end
% 1.60/1.98 permutation0:
% 1.60/1.98 0 ==> 0
% 1.60/1.98 end
% 1.60/1.98
% 1.60/1.98 *** allocated 170857 integers for termspace/termends
% 1.60/1.98 *** allocated 15000 integers for justifications
% 1.60/1.98 *** allocated 256285 integers for termspace/termends
% 1.60/1.98 *** allocated 22500 integers for justifications
% 1.60/1.98 *** allocated 384427 integers for clauses
% 1.60/1.98 eqswap: (8282) {G0,W20,D3,L5,V0,M5} { e21 ==> h( e11 ), h( e11 ) ==> e20,
% 1.60/1.98 h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 1.60/1.98 parent0[1]: (96) {G0,W20,D3,L5,V0,M5} I { h( e11 ) ==> e20, h( e11 ) ==>
% 1.60/1.98 e21, h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 1.60/1.98 substitution0:
% 1.60/1.98 end
% 1.60/1.98
% 1.60/1.98 eqswap: (8312) {G0,W5,D4,L1,V0,M1} { e11 ==> j( h( e11 ) ) }.
% 1.60/1.98 parent0[0]: (161) {G0,W5,D4,L1,V0,M1} I { j( h( e11 ) ) ==> e11 }.
% 1.60/1.98 substitution0:
% 1.60/1.98 end
% 1.60/1.98
% 1.60/1.98 paramod: (12665) {G1,W20,D3,L5,V0,M5} { e11 ==> j( e20 ), e21 ==> h( e11 )
% 1.60/1.98 , h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 1.60/1.98 parent0[1]: (8282) {G0,W20,D3,L5,V0,M5} { e21 ==> h( e11 ), h( e11 ) ==>
% 1.60/1.98 e20, h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 1.60/1.98 parent1[0; 3]: (8312) {G0,W5,D4,L1,V0,M1} { e11 ==> j( h( e11 ) ) }.
% 1.60/1.98 substitution0:
% 1.60/1.98 end
% 1.60/1.98 substitution1:
% 1.60/1.98 end
% 1.60/1.98
% 1.60/1.98 eqswap: (12753) {G1,W20,D3,L5,V0,M5} { e24 ==> h( e11 ), e11 ==> j( e20 )
% 1.60/1.98 , e21 ==> h( e11 ), h( e11 ) ==> e22, h( e11 ) ==> e23 }.
% 1.60/1.98 parent0[4]: (12665) {G1,W20,D3,L5,V0,M5} { e11 ==> j( e20 ), e21 ==> h(
% 1.60/1.98 e11 ), h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 1.60/1.98 substitution0:
% 1.60/1.98 end
% 1.60/1.98
% 1.60/1.98 eqswap: (12757) {G1,W20,D3,L5,V0,M5} { e23 ==> h( e11 ), e24 ==> h( e11 )
% 1.60/1.98 , e11 ==> j( e20 ), e21 ==> h( e11 ), h( e11 ) ==> e22 }.
% 1.60/1.98 parent0[4]: (12753) {G1,W20,D3,L5,V0,M5} { e24 ==> h( e11 ), e11 ==> j(
% 1.60/1.98 e20 ), e21 ==> h( e11 ), h( e11 ) ==> e22, h( e11 ) ==> e23 }.
% 1.60/1.98 substitution0:
% 1.60/1.98 end
% 1.60/1.98
% 1.60/1.98 eqswap: (12760) {G1,W20,D3,L5,V0,M5} { e22 ==> h( e11 ), e23 ==> h( e11 )
% 1.60/1.98 , e24 ==> h( e11 ), e11 ==> j( e20 ), e21 ==> h( e11 ) }.
% 1.60/1.98 parent0[4]: (12757) {G1,W20,D3,L5,V0,M5} { e23 ==> h( e11 ), e24 ==> h(
% 1.60/1.98 e11 ), e11 ==> j( e20 ), e21 ==> h( e11 ), h( e11 ) ==> e22 }.
% 1.60/1.98 substitution0:
% 1.60/1.98 end
% 1.60/1.98
% 1.60/1.98 eqswap: (12763) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e21, e22 ==> h( e11 )
% 1.60/1.98 , e23 ==> h( e11 ), e24 ==> h( e11 ), e11 ==> j( e20 ) }.
% 1.60/1.98 parent0[4]: (12760) {G1,W20,D3,L5,V0,M5} { e22 ==> h( e11 ), e23 ==> h(
% 1.60/1.98 e11 ), e24 ==> h( e11 ), e11 ==> j( e20 ), e21 ==> h( e11 ) }.
% 1.60/1.98 substitution0:
% 1.60/1.98 end
% 1.60/1.98
% 1.60/1.98 eqswap: (12766) {G1,W20,D3,L5,V0,M5} { j( e20 ) ==> e11, h( e11 ) ==> e21
% 1.60/1.98 , e22 ==> h( e11 ), e23 ==> h( e11 ), e24 ==> h( e11 ) }.
% 1.60/1.98 parent0[4]: (12763) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e21, e22 ==> h(
% 1.60/1.98 e11 ), e23 ==> h( e11 ), e24 ==> h( e11 ), e11 ==> j( e20 ) }.
% 1.60/1.98 substitution0:
% 1.60/1.98 end
% 1.60/1.98
% 1.60/1.98 eqswap: (12769) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e24, j( e20 ) ==> e11
% 1.60/1.98 , h( e11 ) ==> e21, e22 ==> h( e11 ), e23 ==> h( e11 ) }.
% 1.60/1.98 parent0[4]: (12766) {G1,W20,D3,L5,V0,M5} { j( e20 ) ==> e11, h( e11 ) ==>
% 1.60/1.98 e21, e22 ==> h( e11 ), e23 ==> h( e11 ), e24 ==> h( e11 ) }.
% 1.60/1.98 substitution0:
% 1.60/1.98 end
% 1.60/1.98
% 1.60/1.98 eqswap: (12772) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e23, h( e11 ) ==> e24
% 1.60/1.98 , j( e20 ) ==> e11, h( e11 ) ==> e21, e22 ==> h( e11 ) }.
% 1.60/1.98 parent0[4]: (12769) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e24, j( e20 ) ==>
% 1.60/1.98 e11, h( e11 ) ==> e21, e22 ==> h( e11 ), e23 ==> h( e11 ) }.
% 1.60/1.98 substitution0:
% 1.60/1.98 end
% 1.60/1.98
% 1.60/1.98 eqswap: (12775) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e22, h( e11 ) ==> e23
% 1.60/1.98 , h( e11 ) ==> e24, j( e20 ) ==> e11, h( e11 ) ==> e21 }.
% 1.60/1.98 parent0[4]: (12772) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e23, h( e11 ) ==>
% 1.60/1.98 e24, j( e20 ) ==> e11, h( e11 ) ==> e21, e22 ==> h( e11 ) }.
% 17.61/17.99 substitution0:
% 17.61/17.99 end
% 17.61/17.99
% 17.61/17.99 subsumption: (165) {G1,W20,D3,L5,V0,M5} P(96,161) { j( e20 ) ==> e11, h(
% 17.61/17.99 e11 ) ==> e21, h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 17.61/17.99 parent0: (12775) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e22, h( e11 ) ==> e23
% 17.61/17.99 , h( e11 ) ==> e24, j( e20 ) ==> e11, h( e11 ) ==> e21 }.
% 17.61/17.99 substitution0:
% 17.61/17.99 end
% 17.61/17.99 permutation0:
% 17.61/17.99 0 ==> 2
% 17.61/17.99 1 ==> 3
% 17.61/17.99 2 ==> 4
% 17.61/17.99 3 ==> 0
% 17.61/17.99 4 ==> 1
% 17.61/17.99 end
% 17.61/17.99
% 17.61/17.99 *** allocated 384427 integers for termspace/termends
% 17.61/17.99 eqswap: (14841) {G0,W20,D3,L5,V0,M5} { e20 ==> h( e11 ), h( e11 ) ==> e21
% 17.61/17.99 , h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 17.61/17.99 parent0[0]: (96) {G0,W20,D3,L5,V0,M5} I { h( e11 ) ==> e20, h( e11 ) ==>
% 17.61/17.99 e21, h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 17.61/17.99 substitution0:
% 17.61/17.99 end
% 17.61/17.99
% 17.61/17.99 eqswap: (14872) {G0,W5,D4,L1,V0,M1} { e11 ==> j( h( e11 ) ) }.
% 17.61/17.99 parent0[0]: (161) {G0,W5,D4,L1,V0,M1} I { j( h( e11 ) ) ==> e11 }.
% 17.61/17.99 substitution0:
% 17.61/17.99 end
% 17.61/17.99
% 17.61/17.99 paramod: (14876) {G1,W20,D3,L5,V0,M5} { e11 ==> j( e24 ), e20 ==> h( e11 )
% 17.61/17.99 , h( e11 ) ==> e21, h( e11 ) ==> e22, h( e11 ) ==> e23 }.
% 17.61/17.99 parent0[4]: (14841) {G0,W20,D3,L5,V0,M5} { e20 ==> h( e11 ), h( e11 ) ==>
% 17.61/17.99 e21, h( e11 ) ==> e22, h( e11 ) ==> e23, h( e11 ) ==> e24 }.
% 17.61/17.99 parent1[0; 3]: (14872) {G0,W5,D4,L1,V0,M1} { e11 ==> j( h( e11 ) ) }.
% 17.61/17.99 substitution0:
% 17.61/17.99 end
% 17.61/17.99 substitution1:
% 17.61/17.99 end
% 17.61/17.99
% 17.61/17.99 eqswap: (15642) {G1,W20,D3,L5,V0,M5} { e23 ==> h( e11 ), e11 ==> j( e24 )
% 17.61/17.99 , e20 ==> h( e11 ), h( e11 ) ==> e21, h( e11 ) ==> e22 }.
% 17.61/17.99 parent0[4]: (14876) {G1,W20,D3,L5,V0,M5} { e11 ==> j( e24 ), e20 ==> h(
% 17.61/17.99 e11 ), h( e11 ) ==> e21, h( e11 ) ==> e22, h( e11 ) ==> e23 }.
% 17.61/17.99 substitution0:
% 17.61/17.99 end
% 17.61/17.99
% 17.61/17.99 eqswap: (15646) {G1,W20,D3,L5,V0,M5} { e22 ==> h( e11 ), e23 ==> h( e11 )
% 17.61/17.99 , e11 ==> j( e24 ), e20 ==> h( e11 ), h( e11 ) ==> e21 }.
% 17.61/17.99 parent0[4]: (15642) {G1,W20,D3,L5,V0,M5} { e23 ==> h( e11 ), e11 ==> j(
% 17.61/17.99 e24 ), e20 ==> h( e11 ), h( e11 ) ==> e21, h( e11 ) ==> e22 }.
% 17.61/17.99 substitution0:
% 17.61/17.99 end
% 17.61/17.99
% 17.61/17.99 eqswap: (15649) {G1,W20,D3,L5,V0,M5} { e21 ==> h( e11 ), e22 ==> h( e11 )
% 17.61/17.99 , e23 ==> h( e11 ), e11 ==> j( e24 ), e20 ==> h( e11 ) }.
% 17.61/17.99 parent0[4]: (15646) {G1,W20,D3,L5,V0,M5} { e22 ==> h( e11 ), e23 ==> h(
% 17.61/17.99 e11 ), e11 ==> j( e24 ), e20 ==> h( e11 ), h( e11 ) ==> e21 }.
% 17.61/17.99 substitution0:
% 17.61/17.99 end
% 17.61/17.99
% 17.61/17.99 eqswap: (15652) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e20, e21 ==> h( e11 )
% 17.61/17.99 , e22 ==> h( e11 ), e23 ==> h( e11 ), e11 ==> j( e24 ) }.
% 17.61/17.99 parent0[4]: (15649) {G1,W20,D3,L5,V0,M5} { e21 ==> h( e11 ), e22 ==> h(
% 17.61/17.99 e11 ), e23 ==> h( e11 ), e11 ==> j( e24 ), e20 ==> h( e11 ) }.
% 17.61/17.99 substitution0:
% 17.61/17.99 end
% 17.61/17.99
% 17.61/17.99 eqswap: (15655) {G1,W20,D3,L5,V0,M5} { j( e24 ) ==> e11, h( e11 ) ==> e20
% 17.61/17.99 , e21 ==> h( e11 ), e22 ==> h( e11 ), e23 ==> h( e11 ) }.
% 17.61/17.99 parent0[4]: (15652) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e20, e21 ==> h(
% 17.61/17.99 e11 ), e22 ==> h( e11 ), e23 ==> h( e11 ), e11 ==> j( e24 ) }.
% 17.61/17.99 substitution0:
% 17.61/17.99 end
% 17.61/17.99
% 17.61/17.99 eqswap: (15658) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e23, j( e24 ) ==> e11
% 17.61/17.99 , h( e11 ) ==> e20, e21 ==> h( e11 ), e22 ==> h( e11 ) }.
% 17.61/17.99 parent0[4]: (15655) {G1,W20,D3,L5,V0,M5} { j( e24 ) ==> e11, h( e11 ) ==>
% 17.61/17.99 e20, e21 ==> h( e11 ), e22 ==> h( e11 ), e23 ==> h( e11 ) }.
% 17.61/17.99 substitution0:
% 17.61/17.99 end
% 17.61/17.99
% 17.61/17.99 eqswap: (15661) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e22, h( e11 ) ==> e23
% 17.61/17.99 , j( e24 ) ==> e11, h( e11 ) ==> e20, e21 ==> h( e11 ) }.
% 17.61/17.99 parent0[4]: (15658) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e23, j( e24 ) ==>
% 17.61/17.99 e11, h( e11 ) ==> e20, e21 ==> h( e11 ), e22 ==> h( e11 ) }.
% 17.61/17.99 substitution0:
% 17.61/17.99 end
% 17.61/17.99
% 17.61/17.99 eqswap: (15664) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e21, h( e11 ) ==> e22
% 17.61/17.99 , h( e11 ) ==> e23, j( e24 ) ==> e11, h( e11 ) ==> e20 }.
% 17.61/17.99 parent0[4]: (15661) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e22, h( e11 ) ==>
% 17.61/17.99 e23, j( e24 ) ==> e11, h( e11 ) ==> e20, e21 ==> h( e11 ) }.
% 17.61/17.99 substitution0:
% 17.61/17.99 end
% 17.61/17.99
% 17.61/17.99 subsumption: (169) {G1,W20,D3,L5,V0,M5} P(96,161) { j( e24 ) ==> e11, h(
% 17.61/17.99 e11 ) ==> e20, h( e11 ) ==> e21, h( e11 ) ==> e22, h( e11 ) ==> e23 }.
% 17.61/17.99 parent0: (15664) {G1,W20,D3,L5,V0,M5} { h( e11 ) ==> e21, h( e11 ) ==> e22
% 17.61/17.99 , h( e11 ) ==> e23, j( e24 ) ==> e11, h( e11 ) ==> e20 }.
% 17.61/17.99 substitution0:
% 17.61/17.99 end
% 17.61/17.99 permutation0:
% 17.61/17.99 0 ==> 2
% 17.61/17.99 1 ==> 3
% 17.61/17.99 2 ==> 4
% 17.61/17.99 3 ==> 0
% 17.61/17.99 4 ==> 1
% 17.61/17.99 end
% 17.61/17.99
% 17.61/17.99
% 17.61/17.99 ==> (220) {G2,W16,D3,L4,V0,M4} P(95,105);d(76);r(14) { h( e10 ) ==> e20, h
% 17.61/17.99 ( e10 ) ==> e22, h( e10 ) ==> e23, h( e10 ) ==> e24 }.
% 17.61/17.99
% 17.61/17.99
% 17.61/17.99
% 17.61/17.99 !!! Internal Problem: OH, OH, COULD NOT DERIVE GOAL !!!
% 17.61/17.99
% 17.61/17.99 Bliksem ended
%------------------------------------------------------------------------------