%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : ALG087+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n022.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:25 EDT 2022
% Result : Theorem 0.74s 1.38s
% Output : Refutation 0.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ALG087+1 : TPTP v8.1.0. Released v2.7.0.
% 0.03/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n022.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Wed Jun 8 03:30:50 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.70/1.10 *** allocated 10000 integers for termspace/termends
% 0.70/1.10 *** allocated 10000 integers for clauses
% 0.70/1.10 *** allocated 10000 integers for justifications
% 0.70/1.10 Bliksem 1.12
% 0.70/1.10
% 0.70/1.10
% 0.70/1.10 Automatic Strategy Selection
% 0.70/1.10
% 0.70/1.10
% 0.70/1.10 Clauses:
% 0.70/1.10
% 0.70/1.10 { ! e10 = e11 }.
% 0.70/1.10 { ! e10 = e12 }.
% 0.70/1.10 { ! e10 = e13 }.
% 0.70/1.10 { ! e10 = e14 }.
% 0.70/1.10 { ! e11 = e12 }.
% 0.70/1.10 { ! e11 = e13 }.
% 0.70/1.10 { ! e11 = e14 }.
% 0.70/1.10 { ! e12 = e13 }.
% 0.70/1.10 { ! e12 = e14 }.
% 0.70/1.10 { ! e13 = e14 }.
% 0.70/1.10 { ! e20 = e21 }.
% 0.70/1.10 { ! e20 = e22 }.
% 0.70/1.10 { ! e20 = e23 }.
% 0.70/1.10 { ! e20 = e24 }.
% 0.70/1.10 { ! e21 = e22 }.
% 0.70/1.10 { ! e21 = e23 }.
% 0.70/1.10 { ! e21 = e24 }.
% 0.70/1.10 { ! e22 = e23 }.
% 0.70/1.10 { ! e22 = e24 }.
% 0.70/1.10 { ! e23 = e24 }.
% 0.70/1.10 { ! e10 = e20 }.
% 0.70/1.10 { ! e10 = e21 }.
% 0.70/1.10 { ! e10 = e22 }.
% 0.70/1.10 { ! e10 = e23 }.
% 0.70/1.10 { ! e10 = e24 }.
% 0.70/1.10 { ! e11 = e20 }.
% 0.70/1.10 { ! e11 = e21 }.
% 0.70/1.10 { ! e11 = e22 }.
% 0.70/1.10 { ! e11 = e23 }.
% 0.70/1.10 { ! e11 = e24 }.
% 0.70/1.10 { ! e12 = e20 }.
% 0.70/1.10 { ! e12 = e21 }.
% 0.70/1.10 { ! e12 = e22 }.
% 0.70/1.10 { ! e12 = e23 }.
% 0.70/1.10 { ! e12 = e24 }.
% 0.70/1.10 { ! e13 = e20 }.
% 0.70/1.10 { ! e13 = e21 }.
% 0.70/1.10 { ! e13 = e22 }.
% 0.70/1.10 { ! e13 = e23 }.
% 0.70/1.10 { ! e13 = e24 }.
% 0.70/1.10 { ! e14 = e20 }.
% 0.70/1.10 { ! e14 = e21 }.
% 0.70/1.10 { ! e14 = e22 }.
% 0.70/1.10 { ! e14 = e23 }.
% 0.70/1.10 { ! e14 = e24 }.
% 0.70/1.10 { op1( e10, e10 ) = e10 }.
% 0.70/1.10 { op1( e10, e11 ) = e11 }.
% 0.70/1.10 { op1( e10, e12 ) = e12 }.
% 0.70/1.10 { op1( e10, e13 ) = e13 }.
% 0.70/1.10 { op1( e10, e14 ) = e14 }.
% 0.70/1.10 { op1( e11, e10 ) = e11 }.
% 0.70/1.10 { op1( e11, e11 ) = e10 }.
% 0.70/1.10 { op1( e11, e12 ) = e13 }.
% 0.70/1.10 { op1( e11, e13 ) = e14 }.
% 0.70/1.10 { op1( e11, e14 ) = e12 }.
% 0.70/1.10 { op1( e12, e10 ) = e12 }.
% 0.70/1.10 { op1( e12, e11 ) = e14 }.
% 0.70/1.10 { op1( e12, e12 ) = e10 }.
% 0.70/1.10 { op1( e12, e13 ) = e11 }.
% 0.70/1.10 { op1( e12, e14 ) = e13 }.
% 0.70/1.10 { op1( e13, e10 ) = e13 }.
% 0.70/1.10 { op1( e13, e11 ) = e12 }.
% 0.70/1.10 { op1( e13, e12 ) = e14 }.
% 0.70/1.10 { op1( e13, e13 ) = e10 }.
% 0.70/1.10 { op1( e13, e14 ) = e11 }.
% 0.70/1.10 { op1( e14, e10 ) = e14 }.
% 0.70/1.10 { op1( e14, e11 ) = e13 }.
% 0.70/1.10 { op1( e14, e12 ) = e11 }.
% 0.70/1.10 { op1( e14, e13 ) = e12 }.
% 0.70/1.10 { op1( e14, e14 ) = e10 }.
% 0.70/1.10 { op2( e20, e20 ) = e20 }.
% 0.70/1.10 { op2( e20, e21 ) = e21 }.
% 0.70/1.10 { op2( e20, e22 ) = e22 }.
% 0.70/1.10 { op2( e20, e23 ) = e23 }.
% 0.70/1.10 { op2( e20, e24 ) = e24 }.
% 0.70/1.10 { op2( e21, e20 ) = e21 }.
% 0.70/1.10 { op2( e21, e21 ) = e20 }.
% 0.70/1.10 { op2( e21, e22 ) = e24 }.
% 0.70/1.10 { op2( e21, e23 ) = e22 }.
% 0.70/1.10 { op2( e21, e24 ) = e23 }.
% 0.70/1.10 { op2( e22, e20 ) = e22 }.
% 0.70/1.10 { op2( e22, e21 ) = e24 }.
% 0.70/1.10 { op2( e22, e22 ) = e23 }.
% 0.70/1.10 { op2( e22, e23 ) = e20 }.
% 0.70/1.10 { op2( e22, e24 ) = e21 }.
% 0.70/1.10 { op2( e23, e20 ) = e23 }.
% 0.70/1.10 { op2( e23, e21 ) = e22 }.
% 0.70/1.10 { op2( e23, e22 ) = e21 }.
% 0.70/1.10 { op2( e23, e23 ) = e24 }.
% 0.70/1.10 { op2( e23, e24 ) = e20 }.
% 0.70/1.10 { op2( e24, e20 ) = e24 }.
% 0.70/1.10 { op2( e24, e21 ) = e23 }.
% 0.70/1.10 { op2( e24, e22 ) = e20 }.
% 0.70/1.10 { op2( e24, e23 ) = e21 }.
% 0.70/1.10 { op2( e24, e24 ) = e22 }.
% 0.70/1.10 { h( e10 ) = e20, h( e10 ) = e21, h( e10 ) = e22, h( e10 ) = e23, h( e10 )
% 0.70/1.10 = e24 }.
% 0.70/1.10 { h( e11 ) = e20, h( e11 ) = e21, h( e11 ) = e22, h( e11 ) = e23, h( e11 )
% 0.70/1.10 = e24 }.
% 0.70/1.10 { h( e12 ) = e20, h( e12 ) = e21, h( e12 ) = e22, h( e12 ) = e23, h( e12 )
% 0.70/1.10 = e24 }.
% 0.70/1.10 { h( e13 ) = e20, h( e13 ) = e21, h( e13 ) = e22, h( e13 ) = e23, h( e13 )
% 0.70/1.10 = e24 }.
% 0.70/1.10 { h( e14 ) = e20, h( e14 ) = e21, h( e14 ) = e22, h( e14 ) = e23, h( e14 )
% 0.70/1.10 = e24 }.
% 0.70/1.10 { j( e20 ) = e10, j( e20 ) = e11, j( e20 ) = e12, j( e20 ) = e13, j( e20 )
% 0.70/1.10 = e14 }.
% 0.70/1.10 { j( e21 ) = e10, j( e21 ) = e11, j( e21 ) = e12, j( e21 ) = e13, j( e21 )
% 0.70/1.10 = e14 }.
% 0.70/1.10 { j( e22 ) = e10, j( e22 ) = e11, j( e22 ) = e12, j( e22 ) = e13, j( e22 )
% 0.70/1.10 = e14 }.
% 0.70/1.10 { j( e23 ) = e10, j( e23 ) = e11, j( e23 ) = e12, j( e23 ) = e13, j( e23 )
% 0.70/1.10 = e14 }.
% 0.70/1.10 { j( e24 ) = e10, j( e24 ) = e11, j( e24 ) = e12, j( e24 ) = e13, j( e24 )
% 0.70/1.10 = e14 }.
% 0.70/1.10 { h( op1( e10, e10 ) ) = op2( h( e10 ), h( e10 ) ) }.
% 0.70/1.10 { h( op1( e10, e11 ) ) = op2( h( e10 ), h( e11 ) ) }.
% 0.70/1.10 { h( op1( e10, e12 ) ) = op2( h( e10 ), h( e12 ) ) }.
% 0.70/1.10 { h( op1( e10, e13 ) ) = op2( h( e10 ), h( e13 ) ) }.
% 0.70/1.10 { h( op1( e10, e14 ) ) = op2( h( e10 ), h( e14 ) ) }.
% 0.70/1.10 { h( op1( e11, e10 ) ) = op2( h( e11 ), h( e10 ) ) }.
% 0.70/1.10 { h( op1( e11, e11 ) ) = op2( h( e11 ), h( e11 ) ) }.
% 0.70/1.10 { h( op1( e11, e12 ) ) = op2( h( e11 ), h( e12 ) ) }.
% 0.70/1.10 { h( op1( e11, e13 ) ) = op2( h( e11 ), h( e13 ) ) }.
% 0.70/1.10 { h( op1( e11, e14 ) ) = op2( h( e11 ), h( e14 ) ) }.
% 0.70/1.10 { h( op1( e12, e10 ) ) = op2( h( e12 ), h( e10 ) ) }.
% 0.70/1.10 { h( op1( e12, e11 ) ) = op2( h( e12 ), h( e11 ) ) }.
% 0.70/1.10 { h( op1( e12, e12 ) ) = op2( h( e12 ), h( e12 ) ) }.
% 0.70/1.10 { h( op1( e12, e13 ) ) = op2( h( e12 ), h( e13 ) ) }.
% 0.70/1.10 { h( op1( e12, e14 ) ) = op2( h( e12 ), h( e14 ) ) }.
% 0.70/1.10 { h( op1( e13, e10 ) ) = op2( h( e13 ), h( e10 ) ) }.
% 0.70/1.10 { h( op1( e13, e11 ) ) = op2( h( e13 ), h( e11 ) ) }.
% 0.74/1.38 { h( op1( e13, e12 ) ) = op2( h( e13 ), h( e12 ) ) }.
% 0.74/1.38 { h( op1( e13, e13 ) ) = op2( h( e13 ), h( e13 ) ) }.
% 0.74/1.38 { h( op1( e13, e14 ) ) = op2( h( e13 ), h( e14 ) ) }.
% 0.74/1.38 { h( op1( e14, e10 ) ) = op2( h( e14 ), h( e10 ) ) }.
% 0.74/1.38 { h( op1( e14, e11 ) ) = op2( h( e14 ), h( e11 ) ) }.
% 0.74/1.38 { h( op1( e14, e12 ) ) = op2( h( e14 ), h( e12 ) ) }.
% 0.74/1.38 { h( op1( e14, e13 ) ) = op2( h( e14 ), h( e13 ) ) }.
% 0.74/1.38 { h( op1( e14, e14 ) ) = op2( h( e14 ), h( e14 ) ) }.
% 0.74/1.38 { j( op2( e20, e20 ) ) = op1( j( e20 ), j( e20 ) ) }.
% 0.74/1.38 { j( op2( e20, e21 ) ) = op1( j( e20 ), j( e21 ) ) }.
% 0.74/1.38 { j( op2( e20, e22 ) ) = op1( j( e20 ), j( e22 ) ) }.
% 0.74/1.38 { j( op2( e20, e23 ) ) = op1( j( e20 ), j( e23 ) ) }.
% 0.74/1.38 { j( op2( e20, e24 ) ) = op1( j( e20 ), j( e24 ) ) }.
% 0.74/1.38 { j( op2( e21, e20 ) ) = op1( j( e21 ), j( e20 ) ) }.
% 0.74/1.38 { j( op2( e21, e21 ) ) = op1( j( e21 ), j( e21 ) ) }.
% 0.74/1.38 { j( op2( e21, e22 ) ) = op1( j( e21 ), j( e22 ) ) }.
% 0.74/1.38 { j( op2( e21, e23 ) ) = op1( j( e21 ), j( e23 ) ) }.
% 0.74/1.38 { j( op2( e21, e24 ) ) = op1( j( e21 ), j( e24 ) ) }.
% 0.74/1.38 { j( op2( e22, e20 ) ) = op1( j( e22 ), j( e20 ) ) }.
% 0.74/1.38 { j( op2( e22, e21 ) ) = op1( j( e22 ), j( e21 ) ) }.
% 0.74/1.38 { j( op2( e22, e22 ) ) = op1( j( e22 ), j( e22 ) ) }.
% 0.74/1.38 { j( op2( e22, e23 ) ) = op1( j( e22 ), j( e23 ) ) }.
% 0.74/1.38 { j( op2( e22, e24 ) ) = op1( j( e22 ), j( e24 ) ) }.
% 0.74/1.38 { j( op2( e23, e20 ) ) = op1( j( e23 ), j( e20 ) ) }.
% 0.74/1.38 { j( op2( e23, e21 ) ) = op1( j( e23 ), j( e21 ) ) }.
% 0.74/1.38 { j( op2( e23, e22 ) ) = op1( j( e23 ), j( e22 ) ) }.
% 0.74/1.38 { j( op2( e23, e23 ) ) = op1( j( e23 ), j( e23 ) ) }.
% 0.74/1.38 { j( op2( e23, e24 ) ) = op1( j( e23 ), j( e24 ) ) }.
% 0.74/1.38 { j( op2( e24, e20 ) ) = op1( j( e24 ), j( e20 ) ) }.
% 0.74/1.38 { j( op2( e24, e21 ) ) = op1( j( e24 ), j( e21 ) ) }.
% 0.74/1.38 { j( op2( e24, e22 ) ) = op1( j( e24 ), j( e22 ) ) }.
% 0.74/1.38 { j( op2( e24, e23 ) ) = op1( j( e24 ), j( e23 ) ) }.
% 0.74/1.38 { j( op2( e24, e24 ) ) = op1( j( e24 ), j( e24 ) ) }.
% 0.74/1.38 { h( j( e20 ) ) = e20 }.
% 0.74/1.38 { h( j( e21 ) ) = e21 }.
% 0.74/1.38 { h( j( e22 ) ) = e22 }.
% 0.74/1.38 { h( j( e23 ) ) = e23 }.
% 0.74/1.38 { h( j( e24 ) ) = e24 }.
% 0.74/1.38 { j( h( e10 ) ) = e10 }.
% 0.74/1.38 { j( h( e11 ) ) = e11 }.
% 0.74/1.38 { j( h( e12 ) ) = e12 }.
% 0.74/1.38 { j( h( e13 ) ) = e13 }.
% 0.74/1.38 { j( h( e14 ) ) = e14 }.
% 0.74/1.38
% 0.74/1.38 percentage equality = 1.000000, percentage horn = 0.939394
% 0.74/1.38 This is a pure equality problem
% 0.74/1.38
% 0.74/1.38
% 0.74/1.38
% 0.74/1.38 Options Used:
% 0.74/1.38
% 0.74/1.38 useres = 1
% 0.74/1.38 useparamod = 1
% 0.74/1.38 useeqrefl = 1
% 0.74/1.38 useeqfact = 1
% 0.74/1.38 usefactor = 1
% 0.74/1.38 usesimpsplitting = 0
% 0.74/1.38 usesimpdemod = 5
% 0.74/1.38 usesimpres = 3
% 0.74/1.38
% 0.74/1.38 resimpinuse = 1000
% 0.74/1.38 resimpclauses = 20000
% 0.74/1.38 substype = eqrewr
% 0.74/1.38 backwardsubs = 1
% 0.74/1.38 selectoldest = 5
% 0.74/1.38
% 0.74/1.38 litorderings [0] = split
% 0.74/1.38 litorderings [1] = extend the termordering, first sorting on arguments
% 0.74/1.38
% 0.74/1.38 termordering = kbo
% 0.74/1.38
% 0.74/1.38 litapriori = 0
% 0.74/1.38 termapriori = 1
% 0.74/1.38 litaposteriori = 0
% 0.74/1.38 termaposteriori = 0
% 0.74/1.38 demodaposteriori = 0
% 0.74/1.38 ordereqreflfact = 0
% 0.74/1.38
% 0.74/1.38 litselect = negord
% 0.74/1.38
% 0.74/1.38 maxweight = 15
% 0.74/1.38 maxdepth = 30000
% 0.74/1.38 maxlength = 115
% 0.74/1.38 maxnrvars = 195
% 0.74/1.38 excuselevel = 1
% 0.74/1.38 increasemaxweight = 1
% 0.74/1.38
% 0.74/1.38 maxselected = 10000000
% 0.74/1.38 maxnrclauses = 10000000
% 0.74/1.38
% 0.74/1.38 showgenerated = 0
% 0.74/1.38 showkept = 0
% 0.74/1.38 showselected = 0
% 0.74/1.38 showdeleted = 0
% 0.74/1.38 showresimp = 1
% 0.74/1.38 showstatus = 2000
% 0.74/1.38
% 0.74/1.38 prologoutput = 0
% 0.74/1.38 nrgoals = 5000000
% 0.74/1.38 totalproof = 1
% 0.74/1.38
% 0.74/1.38 Symbols occurring in the translation:
% 0.74/1.38
% 0.74/1.38 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.74/1.38 . [1, 2] (w:1, o:23, a:1, s:1, b:0),
% 0.74/1.38 ! [4, 1] (w:0, o:16, a:1, s:1, b:0),
% 0.74/1.38 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.74/1.38 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.74/1.38 e10 [35, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.74/1.38 e11 [36, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.74/1.38 e12 [37, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.74/1.38 e13 [38, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.74/1.38 e14 [39, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.74/1.38 e20 [40, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.74/1.38 e21 [41, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.74/1.38 e22 [42, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.74/1.38 e23 [43, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.74/1.38 e24 [44, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.74/1.38 op1 [45, 2] (w:1, o:47, a:1, s:1, b:0),
% 0.74/1.38 op2 [46, 2] (w:1, o:48, a:1, s:1, b:0),
% 0.74/1.38 h [47, 1] (w:1, o:21, a:1, s:1, b:0),
% 0.74/1.38 j [48, 1] (w:1, o:22, a:1, s:1, b:0).
% 0.74/1.38
% 0.74/1.38
% 0.74/1.38 Starting Search:
% 0.74/1.38
% 0.74/1.38 *** allocated 15000 integers for clauses
% 0.74/1.38 Resimplifying inuse:
% 0.74/1.38 Done
% 0.74/1.38
% 0.74/1.38 Failed to find proof!
% 0.74/1.38 maxweight = 15
% 0.74/1.38 maxnrclauses = 10000000
% 0.74/1.38 Generated: 14585
% 0.74/1.38 Kept: 215
% 0.74/1.38
% 0.74/1.38
% 0.74/1.38 The strategy used was not complete!
% 0.74/1.38
% 0.74/1.38 Increased maxweight to 16
% 0.74/1.38
% 0.74/1.38 Starting Search:
% 0.74/1.38
% 0.74/1.38 *** allocated 22500 integers for clauses
% 0.74/1.38 *** allocated 33750 integers for clauses
% 0.74/1.38
% 0.74/1.38 Bliksems!, er is een bewijs:
% 0.74/1.38 % SZS status Theorem
% 0.74/1.38 % SZS output start Refutation
% 0.74/1.38
% 0.74/1.38 (1) {G0,W3,D2,L1,V0,M1} I { ! e12 ==> e10 }.
% 0.74/1.38 (10) {G0,W3,D2,L1,V0,M1} I { ! e21 ==> e20 }.
% 0.74/1.38 (11) {G0,W3,D2,L1,V0,M1} I { ! e22 ==> e20 }.
% 0.74/1.38 (12) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e20 }.
% 0.74/1.38 (13) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e20 }.
% 0.74/1.38 (17) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e22 }.
% 0.74/1.38 (18) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e22 }.
% 0.74/1.38 (19) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e23 }.
% 0.74/1.38 (45) {G0,W5,D3,L1,V0,M1} I { op1( e10, e10 ) ==> e10 }.
% 0.74/1.38 (52) {G0,W5,D3,L1,V0,M1} I { op1( e11, e12 ) ==> e13 }.
% 0.74/1.38 (53) {G0,W5,D3,L1,V0,M1} I { op1( e11, e13 ) ==> e14 }.
% 0.74/1.38 (54) {G0,W5,D3,L1,V0,M1} I { op1( e11, e14 ) ==> e12 }.
% 0.74/1.38 (57) {G0,W5,D3,L1,V0,M1} I { op1( e12, e12 ) ==> e10 }.
% 0.74/1.38 (59) {G0,W5,D3,L1,V0,M1} I { op1( e12, e14 ) ==> e13 }.
% 0.74/1.38 (62) {G0,W5,D3,L1,V0,M1} I { op1( e13, e12 ) ==> e14 }.
% 0.74/1.38 (63) {G0,W5,D3,L1,V0,M1} I { op1( e13, e13 ) ==> e10 }.
% 0.74/1.38 (68) {G0,W5,D3,L1,V0,M1} I { op1( e14, e13 ) ==> e12 }.
% 0.74/1.38 (71) {G0,W5,D3,L1,V0,M1} I { op2( e20, e21 ) ==> e21 }.
% 0.74/1.38 (76) {G0,W5,D3,L1,V0,M1} I { op2( e21, e21 ) ==> e20 }.
% 0.74/1.38 (82) {G0,W5,D3,L1,V0,M1} I { op2( e22, e22 ) ==> e23 }.
% 0.74/1.38 (83) {G0,W5,D3,L1,V0,M1} I { op2( e22, e23 ) ==> e20 }.
% 0.74/1.38 (86) {G0,W5,D3,L1,V0,M1} I { op2( e23, e21 ) ==> e22 }.
% 0.74/1.38 (88) {G0,W5,D3,L1,V0,M1} I { op2( e23, e23 ) ==> e24 }.
% 0.74/1.38 (94) {G0,W5,D3,L1,V0,M1} I { op2( e24, e24 ) ==> e22 }.
% 0.74/1.38 (95) {G0,W20,D3,L5,V0,M5} I { h( e10 ) ==> e20, h( e10 ) ==> e21, h( e10 )
% 0.74/1.38 ==> e22, h( e10 ) ==> e23, h( e10 ) ==> e24 }.
% 0.74/1.38 (97) {G0,W20,D3,L5,V0,M5} I { h( e12 ) ==> e20, h( e12 ) ==> e21, h( e12 )
% 0.74/1.38 ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 0.74/1.38 (98) {G0,W20,D3,L5,V0,M5} I { h( e13 ) ==> e20, h( e13 ) ==> e21, h( e13 )
% 0.74/1.38 ==> e22, h( e13 ) ==> e23, h( e13 ) ==> e24 }.
% 0.74/1.38 (105) {G1,W8,D4,L1,V0,M1} I;d(45) { op2( h( e10 ), h( e10 ) ) ==> h( e10 )
% 0.74/1.38 }.
% 0.74/1.38 (112) {G1,W8,D4,L1,V0,M1} I;d(52) { op2( h( e11 ), h( e12 ) ) ==> h( e13 )
% 0.74/1.38 }.
% 0.74/1.38 (113) {G1,W8,D4,L1,V0,M1} I;d(53) { op2( h( e11 ), h( e13 ) ) ==> h( e14 )
% 0.74/1.38 }.
% 0.74/1.38 (114) {G1,W8,D4,L1,V0,M1} I;d(54) { op2( h( e11 ), h( e14 ) ) ==> h( e12 )
% 0.74/1.38 }.
% 0.74/1.38 (117) {G1,W8,D4,L1,V0,M1} I;d(57) { op2( h( e12 ), h( e12 ) ) ==> h( e10 )
% 0.74/1.38 }.
% 0.74/1.38 (119) {G1,W8,D4,L1,V0,M1} I;d(59) { op2( h( e12 ), h( e14 ) ) ==> h( e13 )
% 0.74/1.38 }.
% 0.74/1.38 (122) {G1,W8,D4,L1,V0,M1} I;d(62) { op2( h( e13 ), h( e12 ) ) ==> h( e14 )
% 0.74/1.38 }.
% 0.74/1.38 (123) {G1,W8,D4,L1,V0,M1} I;d(63) { op2( h( e13 ), h( e13 ) ) ==> h( e10 )
% 0.74/1.38 }.
% 0.74/1.38 (143) {G1,W8,D4,L1,V0,M1} I;d(83) { op1( j( e22 ), j( e23 ) ) ==> j( e20 )
% 0.74/1.38 }.
% 0.74/1.38 (146) {G1,W8,D4,L1,V0,M1} I;d(86) { op1( j( e23 ), j( e21 ) ) ==> j( e22 )
% 0.74/1.38 }.
% 0.74/1.38 (155) {G0,W5,D4,L1,V0,M1} I { h( j( e20 ) ) ==> e20 }.
% 0.74/1.38 (156) {G0,W5,D4,L1,V0,M1} I { h( j( e21 ) ) ==> e21 }.
% 0.74/1.38 (160) {G0,W5,D4,L1,V0,M1} I { j( h( e10 ) ) ==> e10 }.
% 0.74/1.38 (162) {G0,W5,D4,L1,V0,M1} I { j( h( e12 ) ) ==> e12 }.
% 0.74/1.38 (163) {G0,W5,D4,L1,V0,M1} I { j( h( e13 ) ) ==> e13 }.
% 0.74/1.38 (176) {G1,W20,D3,L5,V0,M5} P(97,162) { j( e21 ) ==> e12, h( e12 ) ==> e20,
% 0.74/1.38 h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 0.74/1.38 (183) {G1,W20,D3,L5,V0,M5} P(98,163) { j( e23 ) ==> e13, h( e13 ) ==> e20,
% 0.74/1.38 h( e13 ) ==> e21, h( e13 ) ==> e22, h( e13 ) ==> e24 }.
% 0.74/1.38 (215) {G2,W16,D3,L4,V0,M4} P(95,105);d(82);r(17) { h( e10 ) ==> e20, h( e10
% 0.74/1.38 ) ==> e21, h( e10 ) ==> e23, h( e10 ) ==> e24 }.
% 0.74/1.38 (216) {G3,W15,D3,L4,V0,M4} P(95,105);d(88);d(215);r(19) { h( e10 ) ==> e20
% 0.74/1.38 , h( e10 ) ==> e21, h( e10 ) ==> e24, e23 ==> e22 }.
% 0.74/1.38 (218) {G4,W12,D3,L3,V0,M3} S(216);r(17) { h( e10 ) ==> e20, h( e10 ) ==>
% 0.74/1.38 e21, h( e10 ) ==> e24 }.
% 0.74/1.38 (240) {G5,W11,D3,L3,V0,M3} P(218,105);d(76) { h( e10 ) ==> e20, h( e10 )
% 0.74/1.38 ==> e24, e21 ==> e20 }.
% 0.74/1.38 (245) {G5,W12,D3,L3,V0,M3} P(218,160) { j( e20 ) ==> e10, h( e10 ) ==> e21
% 0.74/1.38 , h( e10 ) ==> e24 }.
% 0.74/1.38 (246) {G6,W8,D3,L2,V0,M2} P(218,160);d(240);d(245);r(10) { h( e10 ) ==> e24
% 0.74/1.38 , j( e20 ) ==> e10 }.
% 0.74/1.38 (255) {G7,W7,D3,L2,V0,M2} P(246,105);d(94) { j( e20 ) ==> e10, e24 ==> e22
% 0.74/1.38 }.
% 0.74/1.38 (267) {G8,W4,D3,L1,V0,M1} S(255);r(18) { j( e20 ) ==> e10 }.
% 0.74/1.38 (277) {G9,W4,D3,L1,V0,M1} P(267,155) { h( e10 ) ==> e20 }.
% 0.74/1.38 (289) {G10,W16,D3,L4,V0,M4} P(176,117);d(82);d(277);r(12) { j( e21 ) ==>
% 0.74/1.38 e12, h( e12 ) ==> e20, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 0.74/1.38 (290) {G11,W15,D3,L4,V0,M4} P(176,117);d(88);d(289);d(277);r(17) { j( e21 )
% 0.74/1.38 ==> e12, h( e12 ) ==> e20, h( e12 ) ==> e24, e24 ==> e20 }.
% 0.74/1.38 (294) {G12,W12,D3,L3,V0,M3} S(290);r(13) { j( e21 ) ==> e12, h( e12 ) ==>
% 0.74/1.38 e20, h( e12 ) ==> e24 }.
% 0.74/1.38 (299) {G13,W8,D3,L2,V0,M2} P(294,117);d(94);d(277);r(11) { j( e21 ) ==> e12
% 0.74/1.38 , h( e12 ) ==> e20 }.
% 0.74/1.38 (318) {G14,W7,D3,L2,V0,M2} P(299,162);d(267) { j( e21 ) ==> e12, e12 ==>
% 0.74/1.38 e10 }.
% 0.74/1.38 (319) {G15,W4,D3,L1,V0,M1} S(318);r(1) { j( e21 ) ==> e12 }.
% 0.74/1.38 (325) {G16,W7,D4,L1,V0,M1} P(319,146) { op1( j( e23 ), e12 ) ==> j( e22 )
% 0.74/1.38 }.
% 0.74/1.38 (327) {G16,W4,D3,L1,V0,M1} P(319,156) { h( e12 ) ==> e21 }.
% 0.74/1.38 (328) {G17,W7,D4,L1,V0,M1} P(327,112) { op2( h( e11 ), e21 ) ==> h( e13 )
% 0.74/1.38 }.
% 0.74/1.38 (331) {G17,W7,D4,L1,V0,M1} P(327,119) { op2( e21, h( e14 ) ) ==> h( e13 )
% 0.74/1.38 }.
% 0.74/1.38 (332) {G17,W7,D4,L1,V0,M1} P(327,122) { op2( h( e13 ), e21 ) ==> h( e14 )
% 0.74/1.38 }.
% 0.74/1.38 (352) {G10,W16,D3,L4,V0,M4} P(183,123);d(82);d(277);r(12) { j( e23 ) ==>
% 0.74/1.38 e13, h( e13 ) ==> e20, h( e13 ) ==> e21, h( e13 ) ==> e24 }.
% 0.74/1.38 (353) {G11,W15,D3,L4,V0,M4} P(183,123);d(94);d(352);d(277);r(18) { j( e23 )
% 0.74/1.38 ==> e13, h( e13 ) ==> e20, h( e13 ) ==> e21, e22 ==> e20 }.
% 0.74/1.38 (356) {G12,W12,D3,L3,V0,M3} S(353);r(11) { j( e23 ) ==> e13, h( e13 ) ==>
% 0.74/1.38 e20, h( e13 ) ==> e21 }.
% 0.74/1.38 (359) {G18,W12,D3,L3,V0,M3} P(356,332);d(71) { j( e23 ) ==> e13, h( e13 )
% 0.74/1.38 ==> e21, h( e14 ) ==> e21 }.
% 0.74/1.38 (363) {G19,W8,D3,L2,V0,M2} P(356,113);d(328);d(356);d(359);r(10) { j( e23 )
% 0.74/1.38 ==> e13, h( e14 ) ==> e21 }.
% 0.74/1.38 (369) {G20,W8,D3,L2,V0,M2} P(363,325);d(62) { h( e14 ) ==> e21, j( e22 )
% 0.74/1.38 ==> e14 }.
% 0.74/1.38 (373) {G21,W4,D3,L1,V0,M1} P(363,143);d(369);d(68);d(267);r(1) { h( e14 )
% 0.74/1.38 ==> e21 }.
% 0.74/1.38 (376) {G22,W4,D3,L1,V0,M1} P(373,331);d(76) { h( e13 ) ==> e20 }.
% 0.74/1.38 (377) {G23,W3,D2,L1,V0,M1} P(373,114);d(328);d(376);d(327) { e21 ==> e20
% 0.74/1.38 }.
% 0.74/1.38 (379) {G24,W0,D0,L0,V0,M0} S(377);r(10) { }.
% 0.74/1.38
% 0.74/1.38
% 0.74/1.38 % SZS output end Refutation
% 0.74/1.38 found a proof!
% 0.74/1.38
% 0.74/1.38
% 0.74/1.38 Unprocessed initial clauses:
% 0.74/1.38
% 0.74/1.38 (381) {G0,W3,D2,L1,V0,M1} { ! e10 = e11 }.
% 0.74/1.38 (382) {G0,W3,D2,L1,V0,M1} { ! e10 = e12 }.
% 0.74/1.38 (383) {G0,W3,D2,L1,V0,M1} { ! e10 = e13 }.
% 0.74/1.38 (384) {G0,W3,D2,L1,V0,M1} { ! e10 = e14 }.
% 0.74/1.38 (385) {G0,W3,D2,L1,V0,M1} { ! e11 = e12 }.
% 0.74/1.38 (386) {G0,W3,D2,L1,V0,M1} { ! e11 = e13 }.
% 0.74/1.38 (387) {G0,W3,D2,L1,V0,M1} { ! e11 = e14 }.
% 0.74/1.38 (388) {G0,W3,D2,L1,V0,M1} { ! e12 = e13 }.
% 0.74/1.38 (389) {G0,W3,D2,L1,V0,M1} { ! e12 = e14 }.
% 0.74/1.38 (390) {G0,W3,D2,L1,V0,M1} { ! e13 = e14 }.
% 0.74/1.38 (391) {G0,W3,D2,L1,V0,M1} { ! e20 = e21 }.
% 0.74/1.38 (392) {G0,W3,D2,L1,V0,M1} { ! e20 = e22 }.
% 0.74/1.38 (393) {G0,W3,D2,L1,V0,M1} { ! e20 = e23 }.
% 0.74/1.38 (394) {G0,W3,D2,L1,V0,M1} { ! e20 = e24 }.
% 0.74/1.38 (395) {G0,W3,D2,L1,V0,M1} { ! e21 = e22 }.
% 0.74/1.38 (396) {G0,W3,D2,L1,V0,M1} { ! e21 = e23 }.
% 0.74/1.38 (397) {G0,W3,D2,L1,V0,M1} { ! e21 = e24 }.
% 0.74/1.38 (398) {G0,W3,D2,L1,V0,M1} { ! e22 = e23 }.
% 0.74/1.38 (399) {G0,W3,D2,L1,V0,M1} { ! e22 = e24 }.
% 0.74/1.38 (400) {G0,W3,D2,L1,V0,M1} { ! e23 = e24 }.
% 0.74/1.38 (401) {G0,W3,D2,L1,V0,M1} { ! e10 = e20 }.
% 0.74/1.38 (402) {G0,W3,D2,L1,V0,M1} { ! e10 = e21 }.
% 0.74/1.38 (403) {G0,W3,D2,L1,V0,M1} { ! e10 = e22 }.
% 0.74/1.38 (404) {G0,W3,D2,L1,V0,M1} { ! e10 = e23 }.
% 0.74/1.38 (405) {G0,W3,D2,L1,V0,M1} { ! e10 = e24 }.
% 0.74/1.38 (406) {G0,W3,D2,L1,V0,M1} { ! e11 = e20 }.
% 0.74/1.38 (407) {G0,W3,D2,L1,V0,M1} { ! e11 = e21 }.
% 0.74/1.38 (408) {G0,W3,D2,L1,V0,M1} { ! e11 = e22 }.
% 0.74/1.38 (409) {G0,W3,D2,L1,V0,M1} { ! e11 = e23 }.
% 0.74/1.38 (410) {G0,W3,D2,L1,V0,M1} { ! e11 = e24 }.
% 0.74/1.38 (411) {G0,W3,D2,L1,V0,M1} { ! e12 = e20 }.
% 0.74/1.38 (412) {G0,W3,D2,L1,V0,M1} { ! e12 = e21 }.
% 0.74/1.38 (413) {G0,W3,D2,L1,V0,M1} { ! e12 = e22 }.
% 0.74/1.38 (414) {G0,W3,D2,L1,V0,M1} { ! e12 = e23 }.
% 0.74/1.38 (415) {G0,W3,D2,L1,V0,M1} { ! e12 = e24 }.
% 0.74/1.38 (416) {G0,W3,D2,L1,V0,M1} { ! e13 = e20 }.
% 0.74/1.38 (417) {G0,W3,D2,L1,V0,M1} { ! e13 = e21 }.
% 0.74/1.38 (418) {G0,W3,D2,L1,V0,M1} { ! e13 = e22 }.
% 0.74/1.38 (419) {G0,W3,D2,L1,V0,M1} { ! e13 = e23 }.
% 0.74/1.38 (420) {G0,W3,D2,L1,V0,M1} { ! e13 = e24 }.
% 0.74/1.38 (421) {G0,W3,D2,L1,V0,M1} { ! e14 = e20 }.
% 0.74/1.38 (422) {G0,W3,D2,L1,V0,M1} { ! e14 = e21 }.
% 0.74/1.38 (423) {G0,W3,D2,L1,V0,M1} { ! e14 = e22 }.
% 0.74/1.38 (424) {G0,W3,D2,L1,V0,M1} { ! e14 = e23 }.
% 0.74/1.38 (425) {G0,W3,D2,L1,V0,M1} { ! e14 = e24 }.
% 0.74/1.38 (426) {G0,W5,D3,L1,V0,M1} { op1( e10, e10 ) = e10 }.
% 0.74/1.38 (427) {G0,W5,D3,L1,V0,M1} { op1( e10, e11 ) = e11 }.
% 0.74/1.38 (428) {G0,W5,D3,L1,V0,M1} { op1( e10, e12 ) = e12 }.
% 0.74/1.38 (429) {G0,W5,D3,L1,V0,M1} { op1( e10, e13 ) = e13 }.
% 0.74/1.38 (430) {G0,W5,D3,L1,V0,M1} { op1( e10, e14 ) = e14 }.
% 0.74/1.38 (431) {G0,W5,D3,L1,V0,M1} { op1( e11, e10 ) = e11 }.
% 0.74/1.38 (432) {G0,W5,D3,L1,V0,M1} { op1( e11, e11 ) = e10 }.
% 0.74/1.38 (433) {G0,W5,D3,L1,V0,M1} { op1( e11, e12 ) = e13 }.
% 0.74/1.38 (434) {G0,W5,D3,L1,V0,M1} { op1( e11, e13 ) = e14 }.
% 0.74/1.38 (435) {G0,W5,D3,L1,V0,M1} { op1( e11, e14 ) = e12 }.
% 0.74/1.38 (436) {G0,W5,D3,L1,V0,M1} { op1( e12, e10 ) = e12 }.
% 0.74/1.38 (437) {G0,W5,D3,L1,V0,M1} { op1( e12, e11 ) = e14 }.
% 0.74/1.38 (438) {G0,W5,D3,L1,V0,M1} { op1( e12, e12 ) = e10 }.
% 0.74/1.38 (439) {G0,W5,D3,L1,V0,M1} { op1( e12, e13 ) = e11 }.
% 0.74/1.38 (440) {G0,W5,D3,L1,V0,M1} { op1( e12, e14 ) = e13 }.
% 0.74/1.38 (441) {G0,W5,D3,L1,V0,M1} { op1( e13, e10 ) = e13 }.
% 0.74/1.38 (442) {G0,W5,D3,L1,V0,M1} { op1( e13, e11 ) = e12 }.
% 0.74/1.38 (443) {G0,W5,D3,L1,V0,M1} { op1( e13, e12 ) = e14 }.
% 0.74/1.38 (444) {G0,W5,D3,L1,V0,M1} { op1( e13, e13 ) = e10 }.
% 0.74/1.38 (445) {G0,W5,D3,L1,V0,M1} { op1( e13, e14 ) = e11 }.
% 0.74/1.38 (446) {G0,W5,D3,L1,V0,M1} { op1( e14, e10 ) = e14 }.
% 0.74/1.38 (447) {G0,W5,D3,L1,V0,M1} { op1( e14, e11 ) = e13 }.
% 0.74/1.38 (448) {G0,W5,D3,L1,V0,M1} { op1( e14, e12 ) = e11 }.
% 0.74/1.38 (449) {G0,W5,D3,L1,V0,M1} { op1( e14, e13 ) = e12 }.
% 0.74/1.38 (450) {G0,W5,D3,L1,V0,M1} { op1( e14, e14 ) = e10 }.
% 0.74/1.38 (451) {G0,W5,D3,L1,V0,M1} { op2( e20, e20 ) = e20 }.
% 0.74/1.38 (452) {G0,W5,D3,L1,V0,M1} { op2( e20, e21 ) = e21 }.
% 0.74/1.38 (453) {G0,W5,D3,L1,V0,M1} { op2( e20, e22 ) = e22 }.
% 0.74/1.38 (454) {G0,W5,D3,L1,V0,M1} { op2( e20, e23 ) = e23 }.
% 0.74/1.38 (455) {G0,W5,D3,L1,V0,M1} { op2( e20, e24 ) = e24 }.
% 0.74/1.38 (456) {G0,W5,D3,L1,V0,M1} { op2( e21, e20 ) = e21 }.
% 0.74/1.38 (457) {G0,W5,D3,L1,V0,M1} { op2( e21, e21 ) = e20 }.
% 0.74/1.38 (458) {G0,W5,D3,L1,V0,M1} { op2( e21, e22 ) = e24 }.
% 0.74/1.38 (459) {G0,W5,D3,L1,V0,M1} { op2( e21, e23 ) = e22 }.
% 0.74/1.38 (460) {G0,W5,D3,L1,V0,M1} { op2( e21, e24 ) = e23 }.
% 0.74/1.38 (461) {G0,W5,D3,L1,V0,M1} { op2( e22, e20 ) = e22 }.
% 0.74/1.38 (462) {G0,W5,D3,L1,V0,M1} { op2( e22, e21 ) = e24 }.
% 0.74/1.38 (463) {G0,W5,D3,L1,V0,M1} { op2( e22, e22 ) = e23 }.
% 0.74/1.38 (464) {G0,W5,D3,L1,V0,M1} { op2( e22, e23 ) = e20 }.
% 0.74/1.38 (465) {G0,W5,D3,L1,V0,M1} { op2( e22, e24 ) = e21 }.
% 0.74/1.38 (466) {G0,W5,D3,L1,V0,M1} { op2( e23, e20 ) = e23 }.
% 0.74/1.38 (467) {G0,W5,D3,L1,V0,M1} { op2( e23, e21 ) = e22 }.
% 0.74/1.38 (468) {G0,W5,D3,L1,V0,M1} { op2( e23, e22 ) = e21 }.
% 0.74/1.38 (469) {G0,W5,D3,L1,V0,M1} { op2( e23, e23 ) = e24 }.
% 0.74/1.38 (470) {G0,W5,D3,L1,V0,M1} { op2( e23, e24 ) = e20 }.
% 0.74/1.38 (471) {G0,W5,D3,L1,V0,M1} { op2( e24, e20 ) = e24 }.
% 0.74/1.38 (472) {G0,W5,D3,L1,V0,M1} { op2( e24, e21 ) = e23 }.
% 0.74/1.38 (473) {G0,W5,D3,L1,V0,M1} { op2( e24, e22 ) = e20 }.
% 0.74/1.38 (474) {G0,W5,D3,L1,V0,M1} { op2( e24, e23 ) = e21 }.
% 0.74/1.38 (475) {G0,W5,D3,L1,V0,M1} { op2( e24, e24 ) = e22 }.
% 0.74/1.38 (476) {G0,W20,D3,L5,V0,M5} { h( e10 ) = e20, h( e10 ) = e21, h( e10 ) =
% 0.74/1.38 e22, h( e10 ) = e23, h( e10 ) = e24 }.
% 0.74/1.38 (477) {G0,W20,D3,L5,V0,M5} { h( e11 ) = e20, h( e11 ) = e21, h( e11 ) =
% 0.74/1.38 e22, h( e11 ) = e23, h( e11 ) = e24 }.
% 0.74/1.38 (478) {G0,W20,D3,L5,V0,M5} { h( e12 ) = e20, h( e12 ) = e21, h( e12 ) =
% 0.74/1.38 e22, h( e12 ) = e23, h( e12 ) = e24 }.
% 0.74/1.38 (479) {G0,W20,D3,L5,V0,M5} { h( e13 ) = e20, h( e13 ) = e21, h( e13 ) =
% 0.74/1.38 e22, h( e13 ) = e23, h( e13 ) = e24 }.
% 0.74/1.38 (480) {G0,W20,D3,L5,V0,M5} { h( e14 ) = e20, h( e14 ) = e21, h( e14 ) =
% 0.74/1.38 e22, h( e14 ) = e23, h( e14 ) = e24 }.
% 0.74/1.38 (481) {G0,W20,D3,L5,V0,M5} { j( e20 ) = e10, j( e20 ) = e11, j( e20 ) =
% 0.74/1.38 e12, j( e20 ) = e13, j( e20 ) = e14 }.
% 0.74/1.38 (482) {G0,W20,D3,L5,V0,M5} { j( e21 ) = e10, j( e21 ) = e11, j( e21 ) =
% 0.74/1.38 e12, j( e21 ) = e13, j( e21 ) = e14 }.
% 0.74/1.38 (483) {G0,W20,D3,L5,V0,M5} { j( e22 ) = e10, j( e22 ) = e11, j( e22 ) =
% 0.74/1.38 e12, j( e22 ) = e13, j( e22 ) = e14 }.
% 0.74/1.38 (484) {G0,W20,D3,L5,V0,M5} { j( e23 ) = e10, j( e23 ) = e11, j( e23 ) =
% 0.74/1.38 e12, j( e23 ) = e13, j( e23 ) = e14 }.
% 0.74/1.38 (485) {G0,W20,D3,L5,V0,M5} { j( e24 ) = e10, j( e24 ) = e11, j( e24 ) =
% 0.74/1.38 e12, j( e24 ) = e13, j( e24 ) = e14 }.
% 0.74/1.38 (486) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e10 ) ) = op2( h( e10 ), h( e10
% 0.74/1.38 ) ) }.
% 0.74/1.38 (487) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e11 ) ) = op2( h( e10 ), h( e11
% 0.74/1.38 ) ) }.
% 0.74/1.38 (488) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e12 ) ) = op2( h( e10 ), h( e12
% 0.74/1.38 ) ) }.
% 0.74/1.38 (489) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e13 ) ) = op2( h( e10 ), h( e13
% 0.74/1.38 ) ) }.
% 0.74/1.38 (490) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e14 ) ) = op2( h( e10 ), h( e14
% 0.74/1.38 ) ) }.
% 0.74/1.38 (491) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e10 ) ) = op2( h( e11 ), h( e10
% 0.74/1.38 ) ) }.
% 0.74/1.38 (492) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e11 ) ) = op2( h( e11 ), h( e11
% 0.74/1.38 ) ) }.
% 0.74/1.38 (493) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e12 ) ) = op2( h( e11 ), h( e12
% 0.74/1.38 ) ) }.
% 0.74/1.38 (494) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e13 ) ) = op2( h( e11 ), h( e13
% 0.74/1.38 ) ) }.
% 0.74/1.38 (495) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e14 ) ) = op2( h( e11 ), h( e14
% 0.74/1.38 ) ) }.
% 0.74/1.38 (496) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e10 ) ) = op2( h( e12 ), h( e10
% 0.74/1.38 ) ) }.
% 0.74/1.38 (497) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e11 ) ) = op2( h( e12 ), h( e11
% 0.74/1.38 ) ) }.
% 0.74/1.38 (498) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e12 ) ) = op2( h( e12 ), h( e12
% 0.74/1.38 ) ) }.
% 0.74/1.38 (499) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e13 ) ) = op2( h( e12 ), h( e13
% 0.74/1.38 ) ) }.
% 0.74/1.38 (500) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e14 ) ) = op2( h( e12 ), h( e14
% 0.74/1.38 ) ) }.
% 0.74/1.38 (501) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e10 ) ) = op2( h( e13 ), h( e10
% 0.74/1.38 ) ) }.
% 0.74/1.38 (502) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e11 ) ) = op2( h( e13 ), h( e11
% 0.74/1.38 ) ) }.
% 0.74/1.38 (503) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e12 ) ) = op2( h( e13 ), h( e12
% 0.74/1.38 ) ) }.
% 0.74/1.38 (504) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e13 ) ) = op2( h( e13 ), h( e13
% 0.74/1.38 ) ) }.
% 0.74/1.38 (505) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e14 ) ) = op2( h( e13 ), h( e14
% 0.74/1.38 ) ) }.
% 0.74/1.38 (506) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e10 ) ) = op2( h( e14 ), h( e10
% 0.74/1.38 ) ) }.
% 0.74/1.38 (507) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e11 ) ) = op2( h( e14 ), h( e11
% 0.74/1.38 ) ) }.
% 0.74/1.38 (508) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e12 ) ) = op2( h( e14 ), h( e12
% 0.74/1.38 ) ) }.
% 0.74/1.38 (509) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e13 ) ) = op2( h( e14 ), h( e13
% 0.74/1.38 ) ) }.
% 0.74/1.38 (510) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e14 ) ) = op2( h( e14 ), h( e14
% 0.74/1.38 ) ) }.
% 0.74/1.38 (511) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e20 ) ) = op1( j( e20 ), j( e20
% 0.74/1.38 ) ) }.
% 0.74/1.38 (512) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e21 ) ) = op1( j( e20 ), j( e21
% 0.74/1.38 ) ) }.
% 0.74/1.38 (513) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e22 ) ) = op1( j( e20 ), j( e22
% 0.74/1.38 ) ) }.
% 0.74/1.38 (514) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e23 ) ) = op1( j( e20 ), j( e23
% 0.74/1.38 ) ) }.
% 0.74/1.38 (515) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e24 ) ) = op1( j( e20 ), j( e24
% 0.74/1.38 ) ) }.
% 0.74/1.38 (516) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e20 ) ) = op1( j( e21 ), j( e20
% 0.74/1.38 ) ) }.
% 0.74/1.38 (517) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e21 ) ) = op1( j( e21 ), j( e21
% 0.74/1.38 ) ) }.
% 0.74/1.38 (518) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e22 ) ) = op1( j( e21 ), j( e22
% 0.74/1.38 ) ) }.
% 0.74/1.38 (519) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e23 ) ) = op1( j( e21 ), j( e23
% 0.74/1.38 ) ) }.
% 0.74/1.38 (520) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e24 ) ) = op1( j( e21 ), j( e24
% 0.74/1.38 ) ) }.
% 0.74/1.38 (521) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e20 ) ) = op1( j( e22 ), j( e20
% 0.74/1.38 ) ) }.
% 0.74/1.38 (522) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e21 ) ) = op1( j( e22 ), j( e21
% 0.74/1.38 ) ) }.
% 0.74/1.38 (523) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e22 ) ) = op1( j( e22 ), j( e22
% 0.74/1.38 ) ) }.
% 0.74/1.38 (524) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e23 ) ) = op1( j( e22 ), j( e23
% 0.74/1.38 ) ) }.
% 0.74/1.38 (525) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e24 ) ) = op1( j( e22 ), j( e24
% 0.74/1.38 ) ) }.
% 0.74/1.38 (526) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e20 ) ) = op1( j( e23 ), j( e20
% 0.74/1.38 ) ) }.
% 0.74/1.38 (527) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e21 ) ) = op1( j( e23 ), j( e21
% 0.74/1.38 ) ) }.
% 0.74/1.38 (528) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e22 ) ) = op1( j( e23 ), j( e22
% 0.74/1.38 ) ) }.
% 0.74/1.38 (529) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e23 ) ) = op1( j( e23 ), j( e23
% 0.74/1.38 ) ) }.
% 0.74/1.38 (530) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e24 ) ) = op1( j( e23 ), j( e24
% 0.74/1.38 ) ) }.
% 0.74/1.38 (531) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e20 ) ) = op1( j( e24 ), j( e20
% 0.74/1.38 ) ) }.
% 0.74/1.38 (532) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e21 ) ) = op1( j( e24 ), j( e21
% 0.74/1.38 ) ) }.
% 0.74/1.38 (533) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e22 ) ) = op1( j( e24 ), j( e22
% 0.74/1.38 ) ) }.
% 0.74/1.38 (534) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e23 ) ) = op1( j( e24 ), j( e23
% 0.74/1.38 ) ) }.
% 0.74/1.38 (535) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e24 ) ) = op1( j( e24 ), j( e24
% 0.74/1.38 ) ) }.
% 0.74/1.38 (536) {G0,W5,D4,L1,V0,M1} { h( j( e20 ) ) = e20 }.
% 0.74/1.38 (537) {G0,W5,D4,L1,V0,M1} { h( j( e21 ) ) = e21 }.
% 0.74/1.38 (538) {G0,W5,D4,L1,V0,M1} { h( j( e22 ) ) = e22 }.
% 0.74/1.38 (539) {G0,W5,D4,L1,V0,M1} { h( j( e23 ) ) = e23 }.
% 0.74/1.38 (540) {G0,W5,D4,L1,V0,M1} { h( j( e24 ) ) = e24 }.
% 0.74/1.38 (541) {G0,W5,D4,L1,V0,M1} { j( h( e10 ) ) = e10 }.
% 0.74/1.38 (542) {G0,W5,D4,L1,V0,M1} { j( h( e11 ) ) = e11 }.
% 0.74/1.38 (543) {G0,W5,D4,L1,V0,M1} { j( h( e12 ) ) = e12 }.
% 0.74/1.38 (544) {G0,W5,D4,L1,V0,M1} { j( h( e13 ) ) = e13 }.
% 0.74/1.38 (545) {G0,W5,D4,L1,V0,M1} { j( h( e14 ) ) = e14 }.
% 0.74/1.38
% 0.74/1.38
% 0.74/1.38 Total Proof:
% 0.74/1.38
% 0.74/1.38 eqswap: (547) {G0,W3,D2,L1,V0,M1} { ! e12 = e10 }.
% 0.74/1.38 parent0[0]: (382) {G0,W3,D2,L1,V0,M1} { ! e10 = e12 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 subsumption: (1) {G0,W3,D2,L1,V0,M1} I { ! e12 ==> e10 }.
% 0.74/1.38 parent0: (547) {G0,W3,D2,L1,V0,M1} { ! e12 = e10 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38 permutation0:
% 0.74/1.38 0 ==> 0
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 eqswap: (558) {G0,W3,D2,L1,V0,M1} { ! e21 = e20 }.
% 0.74/1.38 parent0[0]: (391) {G0,W3,D2,L1,V0,M1} { ! e20 = e21 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 subsumption: (10) {G0,W3,D2,L1,V0,M1} I { ! e21 ==> e20 }.
% 0.74/1.38 parent0: (558) {G0,W3,D2,L1,V0,M1} { ! e21 = e20 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38 permutation0:
% 0.74/1.38 0 ==> 0
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 eqswap: (570) {G0,W3,D2,L1,V0,M1} { ! e22 = e20 }.
% 0.74/1.38 parent0[0]: (392) {G0,W3,D2,L1,V0,M1} { ! e20 = e22 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 subsumption: (11) {G0,W3,D2,L1,V0,M1} I { ! e22 ==> e20 }.
% 0.74/1.38 parent0: (570) {G0,W3,D2,L1,V0,M1} { ! e22 = e20 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38 permutation0:
% 0.74/1.38 0 ==> 0
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 eqswap: (583) {G0,W3,D2,L1,V0,M1} { ! e23 = e20 }.
% 0.74/1.38 parent0[0]: (393) {G0,W3,D2,L1,V0,M1} { ! e20 = e23 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 subsumption: (12) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e20 }.
% 0.74/1.38 parent0: (583) {G0,W3,D2,L1,V0,M1} { ! e23 = e20 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38 permutation0:
% 0.74/1.38 0 ==> 0
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 eqswap: (597) {G0,W3,D2,L1,V0,M1} { ! e24 = e20 }.
% 0.74/1.38 parent0[0]: (394) {G0,W3,D2,L1,V0,M1} { ! e20 = e24 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 subsumption: (13) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e20 }.
% 0.74/1.38 parent0: (597) {G0,W3,D2,L1,V0,M1} { ! e24 = e20 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38 permutation0:
% 0.74/1.38 0 ==> 0
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 eqswap: (615) {G0,W3,D2,L1,V0,M1} { ! e23 = e22 }.
% 0.74/1.38 parent0[0]: (398) {G0,W3,D2,L1,V0,M1} { ! e22 = e23 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 subsumption: (17) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e22 }.
% 0.74/1.38 parent0: (615) {G0,W3,D2,L1,V0,M1} { ! e23 = e22 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38 permutation0:
% 0.74/1.38 0 ==> 0
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 eqswap: (634) {G0,W3,D2,L1,V0,M1} { ! e24 = e22 }.
% 0.74/1.38 parent0[0]: (399) {G0,W3,D2,L1,V0,M1} { ! e22 = e24 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 subsumption: (18) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e22 }.
% 0.74/1.38 parent0: (634) {G0,W3,D2,L1,V0,M1} { ! e24 = e22 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38 permutation0:
% 0.74/1.38 0 ==> 0
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 eqswap: (654) {G0,W3,D2,L1,V0,M1} { ! e24 = e23 }.
% 0.74/1.38 parent0[0]: (400) {G0,W3,D2,L1,V0,M1} { ! e23 = e24 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 subsumption: (19) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e23 }.
% 0.74/1.38 parent0: (654) {G0,W3,D2,L1,V0,M1} { ! e24 = e23 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38 permutation0:
% 0.74/1.38 0 ==> 0
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 subsumption: (45) {G0,W5,D3,L1,V0,M1} I { op1( e10, e10 ) ==> e10 }.
% 0.74/1.38 parent0: (426) {G0,W5,D3,L1,V0,M1} { op1( e10, e10 ) = e10 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38 permutation0:
% 0.74/1.38 0 ==> 0
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 subsumption: (52) {G0,W5,D3,L1,V0,M1} I { op1( e11, e12 ) ==> e13 }.
% 0.74/1.38 parent0: (433) {G0,W5,D3,L1,V0,M1} { op1( e11, e12 ) = e13 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38 permutation0:
% 0.74/1.38 0 ==> 0
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 subsumption: (53) {G0,W5,D3,L1,V0,M1} I { op1( e11, e13 ) ==> e14 }.
% 0.74/1.38 parent0: (434) {G0,W5,D3,L1,V0,M1} { op1( e11, e13 ) = e14 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38 permutation0:
% 0.74/1.38 0 ==> 0
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 subsumption: (54) {G0,W5,D3,L1,V0,M1} I { op1( e11, e14 ) ==> e12 }.
% 0.74/1.38 parent0: (435) {G0,W5,D3,L1,V0,M1} { op1( e11, e14 ) = e12 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38 permutation0:
% 0.74/1.38 0 ==> 0
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 subsumption: (57) {G0,W5,D3,L1,V0,M1} I { op1( e12, e12 ) ==> e10 }.
% 0.74/1.38 parent0: (438) {G0,W5,D3,L1,V0,M1} { op1( e12, e12 ) = e10 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38 permutation0:
% 0.74/1.38 0 ==> 0
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 *** allocated 50625 integers for clauses
% 0.74/1.38 subsumption: (59) {G0,W5,D3,L1,V0,M1} I { op1( e12, e14 ) ==> e13 }.
% 0.74/1.38 parent0: (440) {G0,W5,D3,L1,V0,M1} { op1( e12, e14 ) = e13 }.
% 0.74/1.38 substitution0:
% 0.74/1.38 end
% 0.74/1.38 permutation0:
% 0.74/1.38 0 ==> 0
% 0.74/1.38 end
% 0.74/1.38
% 0.74/1.38 *** allocated 15000 integers for termspace/termends
% 0.74/1.38 subsumption: (62) {G0,W5,D3,L1,V0,M1} I { op1( e13, e12 ) ==> e14 }.
% 0.74/1.38 parent0: (443) {G0,W5,D3,L1,V0,M1} { op1( e13, e12 ) = e14 }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40 permutation0:
% 0.74/1.40 0 ==> 0
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 subsumption: (63) {G0,W5,D3,L1,V0,M1} I { op1( e13, e13 ) ==> e10 }.
% 0.74/1.40 parent0: (444) {G0,W5,D3,L1,V0,M1} { op1( e13, e13 ) = e10 }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40 permutation0:
% 0.74/1.40 0 ==> 0
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 subsumption: (68) {G0,W5,D3,L1,V0,M1} I { op1( e14, e13 ) ==> e12 }.
% 0.74/1.40 parent0: (449) {G0,W5,D3,L1,V0,M1} { op1( e14, e13 ) = e12 }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40 permutation0:
% 0.74/1.40 0 ==> 0
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 subsumption: (71) {G0,W5,D3,L1,V0,M1} I { op2( e20, e21 ) ==> e21 }.
% 0.74/1.40 parent0: (452) {G0,W5,D3,L1,V0,M1} { op2( e20, e21 ) = e21 }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40 permutation0:
% 0.74/1.40 0 ==> 0
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 subsumption: (76) {G0,W5,D3,L1,V0,M1} I { op2( e21, e21 ) ==> e20 }.
% 0.74/1.40 parent0: (457) {G0,W5,D3,L1,V0,M1} { op2( e21, e21 ) = e20 }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40 permutation0:
% 0.74/1.40 0 ==> 0
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 subsumption: (82) {G0,W5,D3,L1,V0,M1} I { op2( e22, e22 ) ==> e23 }.
% 0.74/1.40 parent0: (463) {G0,W5,D3,L1,V0,M1} { op2( e22, e22 ) = e23 }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40 permutation0:
% 0.74/1.40 0 ==> 0
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 subsumption: (83) {G0,W5,D3,L1,V0,M1} I { op2( e22, e23 ) ==> e20 }.
% 0.74/1.40 parent0: (464) {G0,W5,D3,L1,V0,M1} { op2( e22, e23 ) = e20 }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40 permutation0:
% 0.74/1.40 0 ==> 0
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 subsumption: (86) {G0,W5,D3,L1,V0,M1} I { op2( e23, e21 ) ==> e22 }.
% 0.74/1.40 parent0: (467) {G0,W5,D3,L1,V0,M1} { op2( e23, e21 ) = e22 }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40 permutation0:
% 0.74/1.40 0 ==> 0
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 subsumption: (88) {G0,W5,D3,L1,V0,M1} I { op2( e23, e23 ) ==> e24 }.
% 0.74/1.40 parent0: (469) {G0,W5,D3,L1,V0,M1} { op2( e23, e23 ) = e24 }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40 permutation0:
% 0.74/1.40 0 ==> 0
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 subsumption: (94) {G0,W5,D3,L1,V0,M1} I { op2( e24, e24 ) ==> e22 }.
% 0.74/1.40 parent0: (475) {G0,W5,D3,L1,V0,M1} { op2( e24, e24 ) = e22 }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40 permutation0:
% 0.74/1.40 0 ==> 0
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 *** allocated 75937 integers for clauses
% 0.74/1.40 subsumption: (95) {G0,W20,D3,L5,V0,M5} I { h( e10 ) ==> e20, h( e10 ) ==>
% 0.74/1.40 e21, h( e10 ) ==> e22, h( e10 ) ==> e23, h( e10 ) ==> e24 }.
% 0.74/1.40 parent0: (476) {G0,W20,D3,L5,V0,M5} { h( e10 ) = e20, h( e10 ) = e21, h(
% 0.74/1.40 e10 ) = e22, h( e10 ) = e23, h( e10 ) = e24 }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40 permutation0:
% 0.74/1.40 0 ==> 0
% 0.74/1.40 1 ==> 1
% 0.74/1.40 2 ==> 2
% 0.74/1.40 3 ==> 3
% 0.74/1.40 4 ==> 4
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 *** allocated 22500 integers for termspace/termends
% 0.74/1.40 subsumption: (97) {G0,W20,D3,L5,V0,M5} I { h( e12 ) ==> e20, h( e12 ) ==>
% 0.74/1.40 e21, h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 0.74/1.40 parent0: (478) {G0,W20,D3,L5,V0,M5} { h( e12 ) = e20, h( e12 ) = e21, h(
% 0.74/1.40 e12 ) = e22, h( e12 ) = e23, h( e12 ) = e24 }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40 permutation0:
% 0.74/1.40 0 ==> 0
% 0.74/1.40 1 ==> 1
% 0.74/1.40 2 ==> 2
% 0.74/1.40 3 ==> 3
% 0.74/1.40 4 ==> 4
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 subsumption: (98) {G0,W20,D3,L5,V0,M5} I { h( e13 ) ==> e20, h( e13 ) ==>
% 0.74/1.40 e21, h( e13 ) ==> e22, h( e13 ) ==> e23, h( e13 ) ==> e24 }.
% 0.74/1.40 parent0: (479) {G0,W20,D3,L5,V0,M5} { h( e13 ) = e20, h( e13 ) = e21, h(
% 0.74/1.40 e13 ) = e22, h( e13 ) = e23, h( e13 ) = e24 }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40 permutation0:
% 0.74/1.40 0 ==> 0
% 0.74/1.40 1 ==> 1
% 0.74/1.40 2 ==> 2
% 0.74/1.40 3 ==> 3
% 0.74/1.40 4 ==> 4
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 *** allocated 33750 integers for termspace/termends
% 0.74/1.40 paramod: (2811) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e10 ), h( e10 ) )
% 0.74/1.40 }.
% 0.74/1.40 parent0[0]: (45) {G0,W5,D3,L1,V0,M1} I { op1( e10, e10 ) ==> e10 }.
% 0.74/1.40 parent1[0; 2]: (486) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e10 ) ) = op2( h
% 0.74/1.40 ( e10 ), h( e10 ) ) }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40 substitution1:
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 eqswap: (2812) {G1,W8,D4,L1,V0,M1} { op2( h( e10 ), h( e10 ) ) = h( e10 )
% 0.74/1.40 }.
% 0.74/1.40 parent0[0]: (2811) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e10 ), h( e10
% 0.74/1.40 ) ) }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 subsumption: (105) {G1,W8,D4,L1,V0,M1} I;d(45) { op2( h( e10 ), h( e10 ) )
% 0.74/1.40 ==> h( e10 ) }.
% 0.74/1.40 parent0: (2812) {G1,W8,D4,L1,V0,M1} { op2( h( e10 ), h( e10 ) ) = h( e10 )
% 0.74/1.40 }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40 permutation0:
% 0.74/1.40 0 ==> 0
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 *** allocated 113905 integers for clauses
% 0.74/1.40 *** allocated 50625 integers for termspace/termends
% 0.74/1.40 paramod: (3341) {G1,W8,D4,L1,V0,M1} { h( e13 ) = op2( h( e11 ), h( e12 ) )
% 0.74/1.40 }.
% 0.74/1.40 parent0[0]: (52) {G0,W5,D3,L1,V0,M1} I { op1( e11, e12 ) ==> e13 }.
% 0.74/1.40 parent1[0; 2]: (493) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e12 ) ) = op2( h
% 0.74/1.40 ( e11 ), h( e12 ) ) }.
% 0.74/1.40 substitution0:
% 0.74/1.40 end
% 0.74/1.40 substitution1:
% 0.74/1.40 end
% 0.74/1.40
% 0.74/1.40 eqswap: (3342) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e12 ) ) = h( e13 )
% 0.74/1.40 }.
% 0.74/1.40 parent0[0]: (3341) {G1,W8,D4,L1,V0,M1} { h( e13 ) = op2( h( e11 ), h( e12
% 0.74/1.42 ) ) }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 subsumption: (112) {G1,W8,D4,L1,V0,M1} I;d(52) { op2( h( e11 ), h( e12 ) )
% 0.74/1.42 ==> h( e13 ) }.
% 0.74/1.42 parent0: (3342) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e12 ) ) = h( e13 )
% 0.74/1.42 }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42 permutation0:
% 0.74/1.42 0 ==> 0
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 paramod: (3873) {G1,W8,D4,L1,V0,M1} { h( e14 ) = op2( h( e11 ), h( e13 ) )
% 0.74/1.42 }.
% 0.74/1.42 parent0[0]: (53) {G0,W5,D3,L1,V0,M1} I { op1( e11, e13 ) ==> e14 }.
% 0.74/1.42 parent1[0; 2]: (494) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e13 ) ) = op2( h
% 0.74/1.42 ( e11 ), h( e13 ) ) }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42 substitution1:
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 eqswap: (3874) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e13 ) ) = h( e14 )
% 0.74/1.42 }.
% 0.74/1.42 parent0[0]: (3873) {G1,W8,D4,L1,V0,M1} { h( e14 ) = op2( h( e11 ), h( e13
% 0.74/1.42 ) ) }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 subsumption: (113) {G1,W8,D4,L1,V0,M1} I;d(53) { op2( h( e11 ), h( e13 ) )
% 0.74/1.42 ==> h( e14 ) }.
% 0.74/1.42 parent0: (3874) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e13 ) ) = h( e14 )
% 0.74/1.42 }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42 permutation0:
% 0.74/1.42 0 ==> 0
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 paramod: (4407) {G1,W8,D4,L1,V0,M1} { h( e12 ) = op2( h( e11 ), h( e14 ) )
% 0.74/1.42 }.
% 0.74/1.42 parent0[0]: (54) {G0,W5,D3,L1,V0,M1} I { op1( e11, e14 ) ==> e12 }.
% 0.74/1.42 parent1[0; 2]: (495) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e14 ) ) = op2( h
% 0.74/1.42 ( e11 ), h( e14 ) ) }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42 substitution1:
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 eqswap: (4408) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e14 ) ) = h( e12 )
% 0.74/1.42 }.
% 0.74/1.42 parent0[0]: (4407) {G1,W8,D4,L1,V0,M1} { h( e12 ) = op2( h( e11 ), h( e14
% 0.74/1.42 ) ) }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 subsumption: (114) {G1,W8,D4,L1,V0,M1} I;d(54) { op2( h( e11 ), h( e14 ) )
% 0.74/1.42 ==> h( e12 ) }.
% 0.74/1.42 parent0: (4408) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e14 ) ) = h( e12 )
% 0.74/1.42 }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42 permutation0:
% 0.74/1.42 0 ==> 0
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 *** allocated 170857 integers for clauses
% 0.74/1.42 *** allocated 75937 integers for termspace/termends
% 0.74/1.42 paramod: (4947) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e12 ), h( e12 ) )
% 0.74/1.42 }.
% 0.74/1.42 parent0[0]: (57) {G0,W5,D3,L1,V0,M1} I { op1( e12, e12 ) ==> e10 }.
% 0.74/1.42 parent1[0; 2]: (498) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e12 ) ) = op2( h
% 0.74/1.42 ( e12 ), h( e12 ) ) }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42 substitution1:
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 eqswap: (4948) {G1,W8,D4,L1,V0,M1} { op2( h( e12 ), h( e12 ) ) = h( e10 )
% 0.74/1.42 }.
% 0.74/1.42 parent0[0]: (4947) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e12 ), h( e12
% 0.74/1.42 ) ) }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 subsumption: (117) {G1,W8,D4,L1,V0,M1} I;d(57) { op2( h( e12 ), h( e12 ) )
% 0.74/1.42 ==> h( e10 ) }.
% 0.74/1.42 parent0: (4948) {G1,W8,D4,L1,V0,M1} { op2( h( e12 ), h( e12 ) ) = h( e10 )
% 0.74/1.42 }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42 permutation0:
% 0.74/1.42 0 ==> 0
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 paramod: (5491) {G1,W8,D4,L1,V0,M1} { h( e13 ) = op2( h( e12 ), h( e14 ) )
% 0.74/1.42 }.
% 0.74/1.42 parent0[0]: (59) {G0,W5,D3,L1,V0,M1} I { op1( e12, e14 ) ==> e13 }.
% 0.74/1.42 parent1[0; 2]: (500) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e14 ) ) = op2( h
% 0.74/1.42 ( e12 ), h( e14 ) ) }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42 substitution1:
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 eqswap: (5492) {G1,W8,D4,L1,V0,M1} { op2( h( e12 ), h( e14 ) ) = h( e13 )
% 0.74/1.42 }.
% 0.74/1.42 parent0[0]: (5491) {G1,W8,D4,L1,V0,M1} { h( e13 ) = op2( h( e12 ), h( e14
% 0.74/1.42 ) ) }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 subsumption: (119) {G1,W8,D4,L1,V0,M1} I;d(59) { op2( h( e12 ), h( e14 ) )
% 0.74/1.42 ==> h( e13 ) }.
% 0.74/1.42 parent0: (5492) {G1,W8,D4,L1,V0,M1} { op2( h( e12 ), h( e14 ) ) = h( e13 )
% 0.74/1.42 }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42 permutation0:
% 0.74/1.42 0 ==> 0
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 paramod: (6041) {G1,W8,D4,L1,V0,M1} { h( e14 ) = op2( h( e13 ), h( e12 ) )
% 0.74/1.42 }.
% 0.74/1.42 parent0[0]: (62) {G0,W5,D3,L1,V0,M1} I { op1( e13, e12 ) ==> e14 }.
% 0.74/1.42 parent1[0; 2]: (503) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e12 ) ) = op2( h
% 0.74/1.42 ( e13 ), h( e12 ) ) }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42 substitution1:
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 eqswap: (6042) {G1,W8,D4,L1,V0,M1} { op2( h( e13 ), h( e12 ) ) = h( e14 )
% 0.74/1.42 }.
% 0.74/1.42 parent0[0]: (6041) {G1,W8,D4,L1,V0,M1} { h( e14 ) = op2( h( e13 ), h( e12
% 0.74/1.42 ) ) }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 subsumption: (122) {G1,W8,D4,L1,V0,M1} I;d(62) { op2( h( e13 ), h( e12 ) )
% 0.74/1.42 ==> h( e14 ) }.
% 0.74/1.42 parent0: (6042) {G1,W8,D4,L1,V0,M1} { op2( h( e13 ), h( e12 ) ) = h( e14 )
% 0.74/1.42 }.
% 0.74/1.42 substitution0:
% 0.74/1.42 end
% 0.74/1.42 permutation0:
% 0.74/1.42 0 ==> 0
% 0.74/1.42 end
% 0.74/1.42
% 0.74/1.42 *** allocated 113905 integers for termspace/termends
% 0.74/1.42 paramod: (6593) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e13 ), h( e13 ) )
% 0.74/1.42 }.
% 0.74/1.42 parent0[0]: (63) {G0,W5,D3,L1,V0,M1} I { op1( e13, e13 ) ==> e10 }.
% 1.27/1.68 parent1[0; 2]: (504) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e13 ) ) = op2( h
% 1.27/1.68 ( e13 ), h( e13 ) ) }.
% 1.27/1.68 substitution0:
% 1.27/1.68 end
% 1.27/1.68 substitution1:
% 1.27/1.68 end
% 1.27/1.68
% 1.27/1.68 eqswap: (6594) {G1,W8,D4,L1,V0,M1} { op2( h( e13 ), h( e13 ) ) = h( e10 )
% 1.27/1.68 }.
% 1.27/1.68 parent0[0]: (6593) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e13 ), h( e13
% 1.27/1.68 ) ) }.
% 1.27/1.68 substitution0:
% 1.27/1.68 end
% 1.27/1.68
% 1.27/1.68 subsumption: (123) {G1,W8,D4,L1,V0,M1} I;d(63) { op2( h( e13 ), h( e13 ) )
% 1.27/1.68 ==> h( e10 ) }.
% 1.27/1.68 parent0: (6594) {G1,W8,D4,L1,V0,M1} { op2( h( e13 ), h( e13 ) ) = h( e10 )
% 1.27/1.68 }.
% 1.27/1.68 substitution0:
% 1.27/1.68 end
% 1.27/1.68 permutation0:
% 1.27/1.68 0 ==> 0
% 1.27/1.68 end
% 1.27/1.68
% 1.27/1.68 paramod: (7185) {G1,W8,D4,L1,V0,M1} { j( e20 ) = op1( j( e22 ), j( e23 ) )
% 1.27/1.68 }.
% 1.27/1.68 parent0[0]: (83) {G0,W5,D3,L1,V0,M1} I { op2( e22, e23 ) ==> e20 }.
% 1.27/1.68 parent1[0; 2]: (524) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e23 ) ) = op1( j
% 1.27/1.68 ( e22 ), j( e23 ) ) }.
% 1.27/1.68 substitution0:
% 1.27/1.68 end
% 1.27/1.68 substitution1:
% 1.27/1.68 end
% 1.27/1.68
% 1.27/1.68 eqswap: (7186) {G1,W8,D4,L1,V0,M1} { op1( j( e22 ), j( e23 ) ) = j( e20 )
% 1.27/1.68 }.
% 1.27/1.68 parent0[0]: (7185) {G1,W8,D4,L1,V0,M1} { j( e20 ) = op1( j( e22 ), j( e23
% 1.27/1.68 ) ) }.
% 1.27/1.68 substitution0:
% 1.27/1.68 end
% 1.27/1.68
% 1.27/1.68 subsumption: (143) {G1,W8,D4,L1,V0,M1} I;d(83) { op1( j( e22 ), j( e23 ) )
% 1.27/1.68 ==> j( e20 ) }.
% 1.27/1.68 parent0: (7186) {G1,W8,D4,L1,V0,M1} { op1( j( e22 ), j( e23 ) ) = j( e20 )
% 1.27/1.68 }.
% 1.27/1.68 substitution0:
% 1.27/1.68 end
% 1.27/1.68 permutation0:
% 1.27/1.68 0 ==> 0
% 1.27/1.68 end
% 1.27/1.68
% 1.27/1.68 *** allocated 256285 integers for clauses
% 1.27/1.68 paramod: (7783) {G1,W8,D4,L1,V0,M1} { j( e22 ) = op1( j( e23 ), j( e21 ) )
% 1.27/1.68 }.
% 1.27/1.68 parent0[0]: (86) {G0,W5,D3,L1,V0,M1} I { op2( e23, e21 ) ==> e22 }.
% 1.27/1.68 parent1[0; 2]: (527) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e21 ) ) = op1( j
% 1.27/1.68 ( e23 ), j( e21 ) ) }.
% 1.27/1.68 substitution0:
% 1.27/1.68 end
% 1.27/1.68 substitution1:
% 1.27/1.68 end
% 1.27/1.68
% 1.27/1.68 eqswap: (7784) {G1,W8,D4,L1,V0,M1} { op1( j( e23 ), j( e21 ) ) = j( e22 )
% 1.27/1.68 }.
% 1.27/1.68 parent0[0]: (7783) {G1,W8,D4,L1,V0,M1} { j( e22 ) = op1( j( e23 ), j( e21
% 1.27/1.68 ) ) }.
% 1.27/1.68 substitution0:
% 1.27/1.68 end
% 1.27/1.68
% 1.27/1.68 subsumption: (146) {G1,W8,D4,L1,V0,M1} I;d(86) { op1( j( e23 ), j( e21 ) )
% 1.27/1.68 ==> j( e22 ) }.
% 1.27/1.68 parent0: (7784) {G1,W8,D4,L1,V0,M1} { op1( j( e23 ), j( e21 ) ) = j( e22 )
% 1.27/1.68 }.
% 1.27/1.68 substitution0:
% 1.27/1.68 end
% 1.27/1.68 permutation0:
% 1.27/1.68 0 ==> 0
% 1.27/1.68 end
% 1.27/1.68
% 1.27/1.68 subsumption: (155) {G0,W5,D4,L1,V0,M1} I { h( j( e20 ) ) ==> e20 }.
% 1.33/1.68 parent0: (536) {G0,W5,D4,L1,V0,M1} { h( j( e20 ) ) = e20 }.
% 1.33/1.68 substitution0:
% 1.33/1.68 end
% 1.33/1.68 permutation0:
% 1.33/1.68 0 ==> 0
% 1.33/1.68 end
% 1.33/1.68
% 1.33/1.68 subsumption: (156) {G0,W5,D4,L1,V0,M1} I { h( j( e21 ) ) ==> e21 }.
% 1.33/1.68 parent0: (537) {G0,W5,D4,L1,V0,M1} { h( j( e21 ) ) = e21 }.
% 1.33/1.68 substitution0:
% 1.33/1.68 end
% 1.33/1.68 permutation0:
% 1.33/1.68 0 ==> 0
% 1.33/1.68 end
% 1.33/1.68
% 1.33/1.68 *** allocated 170857 integers for termspace/termends
% 1.33/1.68 subsumption: (160) {G0,W5,D4,L1,V0,M1} I { j( h( e10 ) ) ==> e10 }.
% 1.33/1.68 parent0: (541) {G0,W5,D4,L1,V0,M1} { j( h( e10 ) ) = e10 }.
% 1.33/1.68 substitution0:
% 1.33/1.68 end
% 1.33/1.68 permutation0:
% 1.33/1.68 0 ==> 0
% 1.33/1.68 end
% 1.33/1.68
% 1.33/1.68 subsumption: (162) {G0,W5,D4,L1,V0,M1} I { j( h( e12 ) ) ==> e12 }.
% 1.33/1.68 parent0: (543) {G0,W5,D4,L1,V0,M1} { j( h( e12 ) ) = e12 }.
% 1.33/1.68 substitution0:
% 1.33/1.68 end
% 1.33/1.68 permutation0:
% 1.33/1.68 0 ==> 0
% 1.33/1.68 end
% 1.33/1.68
% 1.33/1.68 subsumption: (163) {G0,W5,D4,L1,V0,M1} I { j( h( e13 ) ) ==> e13 }.
% 1.33/1.68 parent0: (544) {G0,W5,D4,L1,V0,M1} { j( h( e13 ) ) = e13 }.
% 1.33/1.68 substitution0:
% 1.33/1.68 end
% 1.33/1.68 permutation0:
% 1.33/1.68 0 ==> 0
% 1.33/1.68 end
% 1.33/1.68
% 1.33/1.68 *** allocated 384427 integers for clauses
% 1.33/1.68 *** allocated 256285 integers for termspace/termends
% 1.33/1.68 *** allocated 15000 integers for justifications
% 1.33/1.68 *** allocated 22500 integers for justifications
% 1.33/1.68 eqswap: (10086) {G0,W20,D3,L5,V0,M5} { e20 ==> h( e12 ), h( e12 ) ==> e21
% 1.33/1.68 , h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 1.33/1.68 parent0[0]: (97) {G0,W20,D3,L5,V0,M5} I { h( e12 ) ==> e20, h( e12 ) ==>
% 1.33/1.68 e21, h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 1.33/1.68 substitution0:
% 1.33/1.68 end
% 1.33/1.68
% 1.33/1.68 eqswap: (10117) {G0,W5,D4,L1,V0,M1} { e12 ==> j( h( e12 ) ) }.
% 1.33/1.68 parent0[0]: (162) {G0,W5,D4,L1,V0,M1} I { j( h( e12 ) ) ==> e12 }.
% 1.33/1.68 substitution0:
% 1.33/1.68 end
% 1.33/1.68
% 1.33/1.68 paramod: (10118) {G1,W20,D3,L5,V0,M5} { e12 ==> j( e21 ), e20 ==> h( e12 )
% 1.33/1.68 , h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 1.33/1.68 parent0[1]: (10086) {G0,W20,D3,L5,V0,M5} { e20 ==> h( e12 ), h( e12 ) ==>
% 1.33/1.68 e21, h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 1.33/1.68 parent1[0; 3]: (10117) {G0,W5,D4,L1,V0,M1} { e12 ==> j( h( e12 ) ) }.
% 1.33/1.68 substitution0:
% 1.33/1.68 end
% 1.33/1.68 substitution1:
% 1.33/1.68 end
% 1.33/1.68
% 1.33/1.68 eqswap: (10206) {G1,W20,D3,L5,V0,M5} { e24 ==> h( e12 ), e12 ==> j( e21 )
% 1.33/1.68 , e20 ==> h( e12 ), h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 1.33/1.68 parent0[4]: (10118) {G1,W20,D3,L5,V0,M5} { e12 ==> j( e21 ), e20 ==> h(
% 1.48/1.86 e12 ), h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 1.48/1.86 substitution0:
% 1.48/1.86 end
% 1.48/1.86
% 1.48/1.86 eqswap: (10210) {G1,W20,D3,L5,V0,M5} { e23 ==> h( e12 ), e24 ==> h( e12 )
% 1.48/1.86 , e12 ==> j( e21 ), e20 ==> h( e12 ), h( e12 ) ==> e22 }.
% 1.48/1.86 parent0[4]: (10206) {G1,W20,D3,L5,V0,M5} { e24 ==> h( e12 ), e12 ==> j(
% 1.48/1.86 e21 ), e20 ==> h( e12 ), h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 1.48/1.86 substitution0:
% 1.48/1.86 end
% 1.48/1.86
% 1.48/1.86 eqswap: (10213) {G1,W20,D3,L5,V0,M5} { e22 ==> h( e12 ), e23 ==> h( e12 )
% 1.48/1.86 , e24 ==> h( e12 ), e12 ==> j( e21 ), e20 ==> h( e12 ) }.
% 1.48/1.86 parent0[4]: (10210) {G1,W20,D3,L5,V0,M5} { e23 ==> h( e12 ), e24 ==> h(
% 1.48/1.86 e12 ), e12 ==> j( e21 ), e20 ==> h( e12 ), h( e12 ) ==> e22 }.
% 1.48/1.86 substitution0:
% 1.48/1.86 end
% 1.48/1.86
% 1.48/1.86 eqswap: (10216) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e20, e22 ==> h( e12 )
% 1.48/1.86 , e23 ==> h( e12 ), e24 ==> h( e12 ), e12 ==> j( e21 ) }.
% 1.48/1.86 parent0[4]: (10213) {G1,W20,D3,L5,V0,M5} { e22 ==> h( e12 ), e23 ==> h(
% 1.48/1.86 e12 ), e24 ==> h( e12 ), e12 ==> j( e21 ), e20 ==> h( e12 ) }.
% 1.48/1.86 substitution0:
% 1.48/1.86 end
% 1.48/1.86
% 1.48/1.86 eqswap: (10219) {G1,W20,D3,L5,V0,M5} { j( e21 ) ==> e12, h( e12 ) ==> e20
% 1.48/1.86 , e22 ==> h( e12 ), e23 ==> h( e12 ), e24 ==> h( e12 ) }.
% 1.48/1.86 parent0[4]: (10216) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e20, e22 ==> h(
% 1.48/1.86 e12 ), e23 ==> h( e12 ), e24 ==> h( e12 ), e12 ==> j( e21 ) }.
% 1.48/1.86 substitution0:
% 1.48/1.86 end
% 1.48/1.86
% 1.48/1.86 eqswap: (10222) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e24, j( e21 ) ==> e12
% 1.48/1.86 , h( e12 ) ==> e20, e22 ==> h( e12 ), e23 ==> h( e12 ) }.
% 1.48/1.86 parent0[4]: (10219) {G1,W20,D3,L5,V0,M5} { j( e21 ) ==> e12, h( e12 ) ==>
% 1.48/1.86 e20, e22 ==> h( e12 ), e23 ==> h( e12 ), e24 ==> h( e12 ) }.
% 1.48/1.86 substitution0:
% 1.48/1.86 end
% 1.48/1.86
% 1.48/1.86 eqswap: (10225) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e23, h( e12 ) ==> e24
% 1.48/1.86 , j( e21 ) ==> e12, h( e12 ) ==> e20, e22 ==> h( e12 ) }.
% 1.48/1.86 parent0[4]: (10222) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e24, j( e21 ) ==>
% 1.48/1.86 e12, h( e12 ) ==> e20, e22 ==> h( e12 ), e23 ==> h( e12 ) }.
% 1.48/1.86 substitution0:
% 1.48/1.86 end
% 1.48/1.86
% 1.48/1.86 eqswap: (10228) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e22, h( e12 ) ==> e23
% 1.48/1.86 , h( e12 ) ==> e24, j( e21 ) ==> e12, h( e12 ) ==> e20 }.
% 1.48/1.86 parent0[4]: (10225) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e23, h( e12 ) ==>
% 1.48/1.86 e24, j( e21 ) ==> e12, h( e12 ) ==> e20, e22 ==> h( e12 ) }.
% 1.48/1.86 substitution0:
% 1.48/1.86 end
% 1.48/1.86
% 1.48/1.86 subsumption: (176) {G1,W20,D3,L5,V0,M5} P(97,162) { j( e21 ) ==> e12, h(
% 1.48/1.86 e12 ) ==> e20, h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 1.48/1.86 parent0: (10228) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e22, h( e12 ) ==> e23
% 1.48/1.86 , h( e12 ) ==> e24, j( e21 ) ==> e12, h( e12 ) ==> e20 }.
% 1.48/1.86 substitution0:
% 1.48/1.86 end
% 1.48/1.86 permutation0:
% 1.48/1.86 0 ==> 2
% 1.48/1.86 1 ==> 3
% 1.48/1.86 2 ==> 4
% 1.48/1.86 3 ==> 0
% 1.48/1.86 4 ==> 1
% 1.48/1.86 end
% 1.48/1.86
% 1.48/1.86 *** allocated 384427 integers for termspace/termends
% 1.48/1.86 eqswap: (12294) {G0,W20,D3,L5,V0,M5} { e20 ==> h( e13 ), h( e13 ) ==> e21
% 1.48/1.86 , h( e13 ) ==> e22, h( e13 ) ==> e23, h( e13 ) ==> e24 }.
% 1.48/1.86 parent0[0]: (98) {G0,W20,D3,L5,V0,M5} I { h( e13 ) ==> e20, h( e13 ) ==>
% 1.48/1.86 e21, h( e13 ) ==> e22, h( e13 ) ==> e23, h( e13 ) ==> e24 }.
% 1.48/1.86 substitution0:
% 1.48/1.86 end
% 1.48/1.86
% 1.48/1.86 eqswap: (12325) {G0,W5,D4,L1,V0,M1} { e13 ==> j( h( e13 ) ) }.
% 1.48/1.86 parent0[0]: (163) {G0,W5,D4,L1,V0,M1} I { j( h( e13 ) ) ==> e13 }.
% 1.48/1.86 substitution0:
% 1.48/1.86 end
% 1.48/1.86
% 1.48/1.86 paramod: (12328) {G1,W20,D3,L5,V0,M5} { e13 ==> j( e23 ), e20 ==> h( e13 )
% 1.48/1.86 , h( e13 ) ==> e21, h( e13 ) ==> e22, h( e13 ) ==> e24 }.
% 1.48/1.86 parent0[3]: (12294) {G0,W20,D3,L5,V0,M5} { e20 ==> h( e13 ), h( e13 ) ==>
% 1.48/1.86 e21, h( e13 ) ==> e22, h( e13 ) ==> e23, h( e13 ) ==> e24 }.
% 1.48/1.86 parent1[0; 3]: (12325) {G0,W5,D4,L1,V0,M1} { e13 ==> j( h( e13 ) ) }.
% 1.48/1.86 substitution0:
% 1.48/1.86 end
% 1.48/1.86 substitution1:
% 1.48/1.86 end
% 1.48/1.86
% 1.48/1.86 eqswap: (12476) {G1,W20,D3,L5,V0,M5} { e24 ==> h( e13 ), e13 ==> j( e23 )
% 1.48/1.86 , e20 ==> h( e13 ), h( e13 ) ==> e21, h( e13 ) ==> e22 }.
% 1.48/1.86 parent0[4]: (12328) {G1,W20,D3,L5,V0,M5} { e13 ==> j( e23 ), e20 ==> h(
% 1.48/1.86 e13 ), h( e13 ) ==> e21, h( e13 ) ==> e22, h( e13 ) ==> e24 }.
% 1.48/1.86 substitution0:
% 1.48/1.86 end
% 1.48/1.86
% 1.48/1.86 eqswap: (12480) {G1,W20,D3,L5,V0,M5} { e22 ==> h( e13 ), e24 ==> h( e13 )
% 1.48/1.86 , e13 ==> j( e23 ), e20 ==> h( e13 ), h( e13 ) ==> e21 }.
% 1.48/1.86 parent0[4]: (12476) {G1,W20,D3,L5,V0,M5} { e24 ==> h( e13 ), e13 ==> j(
% 1.48/1.86 e23 ), e20 ==> h( e13 ), h( e13 ) ==> e21, h( e13 ) ==> e22 }.
% 1.48/1.86 substitution0:
% 1.48/1.86 end
% 1.48/1.86
% 1.48/1.86 eqswap: (12483) {G1,W20,D3,L5,V0,M5} { e21 ==> h( e13 ), e22 ==> h( e13 )
% 20.31/20.72 , e24 ==> h( e13 ), e13 ==> j( e23 ), e20 ==> h( e13 ) }.
% 20.31/20.72 parent0[4]: (12480) {G1,W20,D3,L5,V0,M5} { e22 ==> h( e13 ), e24 ==> h(
% 20.31/20.72 e13 ), e13 ==> j( e23 ), e20 ==> h( e13 ), h( e13 ) ==> e21 }.
% 20.31/20.72 substitution0:
% 20.31/20.72 end
% 20.31/20.72
% 20.31/20.72 eqswap: (12486) {G1,W20,D3,L5,V0,M5} { h( e13 ) ==> e20, e21 ==> h( e13 )
% 20.31/20.72 , e22 ==> h( e13 ), e24 ==> h( e13 ), e13 ==> j( e23 ) }.
% 20.31/20.72 parent0[4]: (12483) {G1,W20,D3,L5,V0,M5} { e21 ==> h( e13 ), e22 ==> h(
% 20.31/20.72 e13 ), e24 ==> h( e13 ), e13 ==> j( e23 ), e20 ==> h( e13 ) }.
% 20.31/20.72 substitution0:
% 20.31/20.72 end
% 20.31/20.72
% 20.31/20.72 eqswap: (12489) {G1,W20,D3,L5,V0,M5} { j( e23 ) ==> e13, h( e13 ) ==> e20
% 20.31/20.72 , e21 ==> h( e13 ), e22 ==> h( e13 ), e24 ==> h( e13 ) }.
% 20.31/20.72 parent0[4]: (12486) {G1,W20,D3,L5,V0,M5} { h( e13 ) ==> e20, e21 ==> h(
% 20.31/20.72 e13 ), e22 ==> h( e13 ), e24 ==> h( e13 ), e13 ==> j( e23 ) }.
% 20.31/20.72 substitution0:
% 20.31/20.72 end
% 20.31/20.72
% 20.31/20.72 eqswap: (12492) {G1,W20,D3,L5,V0,M5} { h( e13 ) ==> e24, j( e23 ) ==> e13
% 20.31/20.72 , h( e13 ) ==> e20, e21 ==> h( e13 ), e22 ==> h( e13 ) }.
% 20.31/20.72 parent0[4]: (12489) {G1,W20,D3,L5,V0,M5} { j( e23 ) ==> e13, h( e13 ) ==>
% 20.31/20.72 e20, e21 ==> h( e13 ), e22 ==> h( e13 ), e24 ==> h( e13 ) }.
% 20.31/20.72 substitution0:
% 20.31/20.72 end
% 20.31/20.72
% 20.31/20.72 eqswap: (12495) {G1,W20,D3,L5,V0,M5} { h( e13 ) ==> e22, h( e13 ) ==> e24
% 20.31/20.72 , j( e23 ) ==> e13, h( e13 ) ==> e20, e21 ==> h( e13 ) }.
% 20.31/20.72 parent0[4]: (12492) {G1,W20,D3,L5,V0,M5} { h( e13 ) ==> e24, j( e23 ) ==>
% 20.31/20.72 e13, h( e13 ) ==> e20, e21 ==> h( e13 ), e22 ==> h( e13 ) }.
% 20.31/20.72 substitution0:
% 20.31/20.72 end
% 20.31/20.72
% 20.31/20.72 eqswap: (12498) {G1,W20,D3,L5,V0,M5} { h( e13 ) ==> e21, h( e13 ) ==> e22
% 20.31/20.72 , h( e13 ) ==> e24, j( e23 ) ==> e13, h( e13 ) ==> e20 }.
% 20.31/20.72 parent0[4]: (12495) {G1,W20,D3,L5,V0,M5} { h( e13 ) ==> e22, h( e13 ) ==>
% 20.31/20.72 e24, j( e23 ) ==> e13, h( e13 ) ==> e20, e21 ==> h( e13 ) }.
% 20.31/20.72 substitution0:
% 20.31/20.72 end
% 20.31/20.72
% 20.31/20.72 subsumption: (183) {G1,W20,D3,L5,V0,M5} P(98,163) { j( e23 ) ==> e13, h(
% 20.31/20.72 e13 ) ==> e20, h( e13 ) ==> e21, h( e13 ) ==> e22, h( e13 ) ==> e24 }.
% 20.31/20.72 parent0: (12498) {G1,W20,D3,L5,V0,M5} { h( e13 ) ==> e21, h( e13 ) ==> e22
% 20.31/20.72 , h( e13 ) ==> e24, j( e23 ) ==> e13, h( e13 ) ==> e20 }.
% 20.31/20.72 substitution0:
% 20.31/20.72 end
% 20.31/20.72 permutation0:
% 20.31/20.72 0 ==> 2
% 20.31/20.72 1 ==> 3
% 20.31/20.72 2 ==> 4
% 20.31/20.72 3 ==> 0
% 20.31/20.72 4 ==> 1
% 20.31/20.72 end
% 20.31/20.72
% 20.31/20.72 *** allocated 576640 integers for clauses
% 20.31/20.72
% 20.31/20.72 ==> (215) {G2,W16,D3,L4,V0,M4} P(95,105);d(82);r(17) { h( e10 ) ==> e20, h
% 20.31/20.72 ( e10 ) ==> e21, h( e10 ) ==> e23, h( e10 ) ==> e24 }.
% 20.31/20.72
% 20.31/20.72
% 20.31/20.72
% 20.31/20.72 !!! Internal Problem: OH, OH, COULD NOT DERIVE GOAL !!!
% 20.31/20.72
% 20.31/20.72 Bliksem ended
%------------------------------------------------------------------------------