%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : ALG088+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n021.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.73s 1.36s
% Output : Refutation 0.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ALG088+1 : TPTP v8.1.0. Released v2.7.0.
% 0.03/0.12 % Command : bliksem %s
% 0.13/0.33 % Computer : n021.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.33 % CPULimit : 300
% 0.13/0.33 % DateTime : Wed Jun 8 01:18:51 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.73/1.10 *** allocated 10000 integers for termspace/termends
% 0.73/1.10 *** allocated 10000 integers for clauses
% 0.73/1.10 *** allocated 10000 integers for justifications
% 0.73/1.10 Bliksem 1.12
% 0.73/1.10
% 0.73/1.10
% 0.73/1.10 Automatic Strategy Selection
% 0.73/1.10
% 0.73/1.10
% 0.73/1.10 Clauses:
% 0.73/1.10
% 0.73/1.10 { ! e10 = e11 }.
% 0.73/1.10 { ! e10 = e12 }.
% 0.73/1.10 { ! e10 = e13 }.
% 0.73/1.10 { ! e10 = e14 }.
% 0.73/1.10 { ! e11 = e12 }.
% 0.73/1.10 { ! e11 = e13 }.
% 0.73/1.10 { ! e11 = e14 }.
% 0.73/1.10 { ! e12 = e13 }.
% 0.73/1.10 { ! e12 = e14 }.
% 0.73/1.10 { ! e13 = e14 }.
% 0.73/1.10 { ! e20 = e21 }.
% 0.73/1.10 { ! e20 = e22 }.
% 0.73/1.10 { ! e20 = e23 }.
% 0.73/1.10 { ! e20 = e24 }.
% 0.73/1.10 { ! e21 = e22 }.
% 0.73/1.10 { ! e21 = e23 }.
% 0.73/1.10 { ! e21 = e24 }.
% 0.73/1.10 { ! e22 = e23 }.
% 0.73/1.10 { ! e22 = e24 }.
% 0.73/1.10 { ! e23 = e24 }.
% 0.73/1.10 { ! e10 = e20 }.
% 0.73/1.10 { ! e10 = e21 }.
% 0.73/1.10 { ! e10 = e22 }.
% 0.73/1.10 { ! e10 = e23 }.
% 0.73/1.10 { ! e10 = e24 }.
% 0.73/1.10 { ! e11 = e20 }.
% 0.73/1.10 { ! e11 = e21 }.
% 0.73/1.10 { ! e11 = e22 }.
% 0.73/1.10 { ! e11 = e23 }.
% 0.73/1.10 { ! e11 = e24 }.
% 0.73/1.10 { ! e12 = e20 }.
% 0.73/1.10 { ! e12 = e21 }.
% 0.73/1.10 { ! e12 = e22 }.
% 0.73/1.10 { ! e12 = e23 }.
% 0.73/1.10 { ! e12 = e24 }.
% 0.73/1.10 { ! e13 = e20 }.
% 0.73/1.10 { ! e13 = e21 }.
% 0.73/1.10 { ! e13 = e22 }.
% 0.73/1.10 { ! e13 = e23 }.
% 0.73/1.10 { ! e13 = e24 }.
% 0.73/1.10 { ! e14 = e20 }.
% 0.73/1.10 { ! e14 = e21 }.
% 0.73/1.10 { ! e14 = e22 }.
% 0.73/1.10 { ! e14 = e23 }.
% 0.73/1.10 { ! e14 = e24 }.
% 0.73/1.10 { op1( e10, e10 ) = e10 }.
% 0.73/1.10 { op1( e10, e11 ) = e11 }.
% 0.73/1.10 { op1( e10, e12 ) = e12 }.
% 0.73/1.10 { op1( e10, e13 ) = e13 }.
% 0.73/1.10 { op1( e10, e14 ) = e14 }.
% 0.73/1.10 { op1( e11, e10 ) = e11 }.
% 0.73/1.10 { op1( e11, e11 ) = e10 }.
% 0.73/1.10 { op1( e11, e12 ) = e13 }.
% 0.73/1.10 { op1( e11, e13 ) = e14 }.
% 0.73/1.10 { op1( e11, e14 ) = e12 }.
% 0.73/1.10 { op1( e12, e10 ) = e12 }.
% 0.73/1.10 { op1( e12, e11 ) = e14 }.
% 0.73/1.10 { op1( e12, e12 ) = e10 }.
% 0.73/1.10 { op1( e12, e13 ) = e11 }.
% 0.73/1.10 { op1( e12, e14 ) = e13 }.
% 0.73/1.10 { op1( e13, e10 ) = e13 }.
% 0.73/1.10 { op1( e13, e11 ) = e12 }.
% 0.73/1.10 { op1( e13, e12 ) = e14 }.
% 0.73/1.10 { op1( e13, e13 ) = e10 }.
% 0.73/1.10 { op1( e13, e14 ) = e11 }.
% 0.73/1.10 { op1( e14, e10 ) = e14 }.
% 0.73/1.10 { op1( e14, e11 ) = e13 }.
% 0.73/1.10 { op1( e14, e12 ) = e11 }.
% 0.73/1.10 { op1( e14, e13 ) = e12 }.
% 0.73/1.10 { op1( e14, e14 ) = e10 }.
% 0.73/1.10 { op2( e20, e20 ) = e20 }.
% 0.73/1.10 { op2( e20, e21 ) = e21 }.
% 0.73/1.10 { op2( e20, e22 ) = e22 }.
% 0.73/1.10 { op2( e20, e23 ) = e23 }.
% 0.73/1.10 { op2( e20, e24 ) = e24 }.
% 0.73/1.10 { op2( e21, e20 ) = e21 }.
% 0.73/1.10 { op2( e21, e21 ) = e22 }.
% 0.73/1.10 { op2( e21, e22 ) = e23 }.
% 0.73/1.10 { op2( e21, e23 ) = e24 }.
% 0.73/1.10 { op2( e21, e24 ) = e20 }.
% 0.73/1.10 { op2( e22, e20 ) = e22 }.
% 0.73/1.10 { op2( e22, e21 ) = e24 }.
% 0.73/1.10 { op2( e22, e22 ) = e21 }.
% 0.73/1.10 { op2( e22, e23 ) = e20 }.
% 0.73/1.10 { op2( e22, e24 ) = e23 }.
% 0.73/1.10 { op2( e23, e20 ) = e23 }.
% 0.73/1.10 { op2( e23, e21 ) = e20 }.
% 0.73/1.10 { op2( e23, e22 ) = e24 }.
% 0.73/1.10 { op2( e23, e23 ) = e21 }.
% 0.73/1.10 { op2( e23, e24 ) = e22 }.
% 0.73/1.10 { op2( e24, e20 ) = e24 }.
% 0.73/1.10 { op2( e24, e21 ) = e23 }.
% 0.73/1.10 { op2( e24, e22 ) = e20 }.
% 0.73/1.10 { op2( e24, e23 ) = e22 }.
% 0.73/1.10 { op2( e24, e24 ) = e21 }.
% 0.73/1.10 { h( e10 ) = e20, h( e10 ) = e21, h( e10 ) = e22, h( e10 ) = e23, h( e10 )
% 0.73/1.10 = e24 }.
% 0.73/1.10 { h( e11 ) = e20, h( e11 ) = e21, h( e11 ) = e22, h( e11 ) = e23, h( e11 )
% 0.73/1.10 = e24 }.
% 0.73/1.10 { h( e12 ) = e20, h( e12 ) = e21, h( e12 ) = e22, h( e12 ) = e23, h( e12 )
% 0.73/1.10 = e24 }.
% 0.73/1.10 { h( e13 ) = e20, h( e13 ) = e21, h( e13 ) = e22, h( e13 ) = e23, h( e13 )
% 0.73/1.10 = e24 }.
% 0.73/1.10 { h( e14 ) = e20, h( e14 ) = e21, h( e14 ) = e22, h( e14 ) = e23, h( e14 )
% 0.73/1.10 = e24 }.
% 0.73/1.10 { j( e20 ) = e10, j( e20 ) = e11, j( e20 ) = e12, j( e20 ) = e13, j( e20 )
% 0.73/1.10 = e14 }.
% 0.73/1.10 { j( e21 ) = e10, j( e21 ) = e11, j( e21 ) = e12, j( e21 ) = e13, j( e21 )
% 0.73/1.10 = e14 }.
% 0.73/1.10 { j( e22 ) = e10, j( e22 ) = e11, j( e22 ) = e12, j( e22 ) = e13, j( e22 )
% 0.73/1.10 = e14 }.
% 0.73/1.10 { j( e23 ) = e10, j( e23 ) = e11, j( e23 ) = e12, j( e23 ) = e13, j( e23 )
% 0.73/1.10 = e14 }.
% 0.73/1.10 { j( e24 ) = e10, j( e24 ) = e11, j( e24 ) = e12, j( e24 ) = e13, j( e24 )
% 0.73/1.10 = e14 }.
% 0.73/1.10 { h( op1( e10, e10 ) ) = op2( h( e10 ), h( e10 ) ) }.
% 0.73/1.10 { h( op1( e10, e11 ) ) = op2( h( e10 ), h( e11 ) ) }.
% 0.73/1.10 { h( op1( e10, e12 ) ) = op2( h( e10 ), h( e12 ) ) }.
% 0.73/1.10 { h( op1( e10, e13 ) ) = op2( h( e10 ), h( e13 ) ) }.
% 0.73/1.10 { h( op1( e10, e14 ) ) = op2( h( e10 ), h( e14 ) ) }.
% 0.73/1.10 { h( op1( e11, e10 ) ) = op2( h( e11 ), h( e10 ) ) }.
% 0.73/1.10 { h( op1( e11, e11 ) ) = op2( h( e11 ), h( e11 ) ) }.
% 0.73/1.10 { h( op1( e11, e12 ) ) = op2( h( e11 ), h( e12 ) ) }.
% 0.73/1.10 { h( op1( e11, e13 ) ) = op2( h( e11 ), h( e13 ) ) }.
% 0.73/1.10 { h( op1( e11, e14 ) ) = op2( h( e11 ), h( e14 ) ) }.
% 0.73/1.10 { h( op1( e12, e10 ) ) = op2( h( e12 ), h( e10 ) ) }.
% 0.73/1.10 { h( op1( e12, e11 ) ) = op2( h( e12 ), h( e11 ) ) }.
% 0.73/1.10 { h( op1( e12, e12 ) ) = op2( h( e12 ), h( e12 ) ) }.
% 0.73/1.10 { h( op1( e12, e13 ) ) = op2( h( e12 ), h( e13 ) ) }.
% 0.73/1.10 { h( op1( e12, e14 ) ) = op2( h( e12 ), h( e14 ) ) }.
% 0.73/1.10 { h( op1( e13, e10 ) ) = op2( h( e13 ), h( e10 ) ) }.
% 0.73/1.10 { h( op1( e13, e11 ) ) = op2( h( e13 ), h( e11 ) ) }.
% 0.73/1.36 { h( op1( e13, e12 ) ) = op2( h( e13 ), h( e12 ) ) }.
% 0.73/1.36 { h( op1( e13, e13 ) ) = op2( h( e13 ), h( e13 ) ) }.
% 0.73/1.36 { h( op1( e13, e14 ) ) = op2( h( e13 ), h( e14 ) ) }.
% 0.73/1.36 { h( op1( e14, e10 ) ) = op2( h( e14 ), h( e10 ) ) }.
% 0.73/1.36 { h( op1( e14, e11 ) ) = op2( h( e14 ), h( e11 ) ) }.
% 0.73/1.36 { h( op1( e14, e12 ) ) = op2( h( e14 ), h( e12 ) ) }.
% 0.73/1.36 { h( op1( e14, e13 ) ) = op2( h( e14 ), h( e13 ) ) }.
% 0.73/1.36 { h( op1( e14, e14 ) ) = op2( h( e14 ), h( e14 ) ) }.
% 0.73/1.36 { j( op2( e20, e20 ) ) = op1( j( e20 ), j( e20 ) ) }.
% 0.73/1.36 { j( op2( e20, e21 ) ) = op1( j( e20 ), j( e21 ) ) }.
% 0.73/1.36 { j( op2( e20, e22 ) ) = op1( j( e20 ), j( e22 ) ) }.
% 0.73/1.36 { j( op2( e20, e23 ) ) = op1( j( e20 ), j( e23 ) ) }.
% 0.73/1.36 { j( op2( e20, e24 ) ) = op1( j( e20 ), j( e24 ) ) }.
% 0.73/1.36 { j( op2( e21, e20 ) ) = op1( j( e21 ), j( e20 ) ) }.
% 0.73/1.36 { j( op2( e21, e21 ) ) = op1( j( e21 ), j( e21 ) ) }.
% 0.73/1.36 { j( op2( e21, e22 ) ) = op1( j( e21 ), j( e22 ) ) }.
% 0.73/1.36 { j( op2( e21, e23 ) ) = op1( j( e21 ), j( e23 ) ) }.
% 0.73/1.36 { j( op2( e21, e24 ) ) = op1( j( e21 ), j( e24 ) ) }.
% 0.73/1.36 { j( op2( e22, e20 ) ) = op1( j( e22 ), j( e20 ) ) }.
% 0.73/1.36 { j( op2( e22, e21 ) ) = op1( j( e22 ), j( e21 ) ) }.
% 0.73/1.36 { j( op2( e22, e22 ) ) = op1( j( e22 ), j( e22 ) ) }.
% 0.73/1.36 { j( op2( e22, e23 ) ) = op1( j( e22 ), j( e23 ) ) }.
% 0.73/1.36 { j( op2( e22, e24 ) ) = op1( j( e22 ), j( e24 ) ) }.
% 0.73/1.36 { j( op2( e23, e20 ) ) = op1( j( e23 ), j( e20 ) ) }.
% 0.73/1.36 { j( op2( e23, e21 ) ) = op1( j( e23 ), j( e21 ) ) }.
% 0.73/1.36 { j( op2( e23, e22 ) ) = op1( j( e23 ), j( e22 ) ) }.
% 0.73/1.36 { j( op2( e23, e23 ) ) = op1( j( e23 ), j( e23 ) ) }.
% 0.73/1.36 { j( op2( e23, e24 ) ) = op1( j( e23 ), j( e24 ) ) }.
% 0.73/1.36 { j( op2( e24, e20 ) ) = op1( j( e24 ), j( e20 ) ) }.
% 0.73/1.36 { j( op2( e24, e21 ) ) = op1( j( e24 ), j( e21 ) ) }.
% 0.73/1.36 { j( op2( e24, e22 ) ) = op1( j( e24 ), j( e22 ) ) }.
% 0.73/1.36 { j( op2( e24, e23 ) ) = op1( j( e24 ), j( e23 ) ) }.
% 0.73/1.36 { j( op2( e24, e24 ) ) = op1( j( e24 ), j( e24 ) ) }.
% 0.73/1.36 { h( j( e20 ) ) = e20 }.
% 0.73/1.36 { h( j( e21 ) ) = e21 }.
% 0.73/1.36 { h( j( e22 ) ) = e22 }.
% 0.73/1.36 { h( j( e23 ) ) = e23 }.
% 0.73/1.36 { h( j( e24 ) ) = e24 }.
% 0.73/1.36 { j( h( e10 ) ) = e10 }.
% 0.73/1.36 { j( h( e11 ) ) = e11 }.
% 0.73/1.36 { j( h( e12 ) ) = e12 }.
% 0.73/1.36 { j( h( e13 ) ) = e13 }.
% 0.73/1.36 { j( h( e14 ) ) = e14 }.
% 0.73/1.36
% 0.73/1.36 percentage equality = 1.000000, percentage horn = 0.939394
% 0.73/1.36 This is a pure equality problem
% 0.73/1.36
% 0.73/1.36
% 0.73/1.36
% 0.73/1.36 Options Used:
% 0.73/1.36
% 0.73/1.36 useres = 1
% 0.73/1.36 useparamod = 1
% 0.73/1.36 useeqrefl = 1
% 0.73/1.36 useeqfact = 1
% 0.73/1.36 usefactor = 1
% 0.73/1.36 usesimpsplitting = 0
% 0.73/1.36 usesimpdemod = 5
% 0.73/1.36 usesimpres = 3
% 0.73/1.36
% 0.73/1.36 resimpinuse = 1000
% 0.73/1.36 resimpclauses = 20000
% 0.73/1.36 substype = eqrewr
% 0.73/1.36 backwardsubs = 1
% 0.73/1.36 selectoldest = 5
% 0.73/1.36
% 0.73/1.36 litorderings [0] = split
% 0.73/1.36 litorderings [1] = extend the termordering, first sorting on arguments
% 0.73/1.36
% 0.73/1.36 termordering = kbo
% 0.73/1.36
% 0.73/1.36 litapriori = 0
% 0.73/1.36 termapriori = 1
% 0.73/1.36 litaposteriori = 0
% 0.73/1.36 termaposteriori = 0
% 0.73/1.36 demodaposteriori = 0
% 0.73/1.36 ordereqreflfact = 0
% 0.73/1.36
% 0.73/1.36 litselect = negord
% 0.73/1.36
% 0.73/1.36 maxweight = 15
% 0.73/1.36 maxdepth = 30000
% 0.73/1.36 maxlength = 115
% 0.73/1.36 maxnrvars = 195
% 0.73/1.36 excuselevel = 1
% 0.73/1.36 increasemaxweight = 1
% 0.73/1.36
% 0.73/1.36 maxselected = 10000000
% 0.73/1.36 maxnrclauses = 10000000
% 0.73/1.36
% 0.73/1.36 showgenerated = 0
% 0.73/1.36 showkept = 0
% 0.73/1.36 showselected = 0
% 0.73/1.36 showdeleted = 0
% 0.73/1.36 showresimp = 1
% 0.73/1.36 showstatus = 2000
% 0.73/1.36
% 0.73/1.36 prologoutput = 0
% 0.73/1.36 nrgoals = 5000000
% 0.73/1.36 totalproof = 1
% 0.73/1.36
% 0.73/1.36 Symbols occurring in the translation:
% 0.73/1.36
% 0.73/1.36 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.73/1.36 . [1, 2] (w:1, o:23, a:1, s:1, b:0),
% 0.73/1.36 ! [4, 1] (w:0, o:16, a:1, s:1, b:0),
% 0.73/1.36 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.73/1.36 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.73/1.36 e10 [35, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.73/1.36 e11 [36, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.73/1.36 e12 [37, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.73/1.36 e13 [38, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.73/1.36 e14 [39, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.73/1.36 e20 [40, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.73/1.36 e21 [41, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.73/1.36 e22 [42, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.73/1.36 e23 [43, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.73/1.36 e24 [44, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.73/1.36 op1 [45, 2] (w:1, o:47, a:1, s:1, b:0),
% 0.73/1.36 op2 [46, 2] (w:1, o:48, a:1, s:1, b:0),
% 0.73/1.36 h [47, 1] (w:1, o:21, a:1, s:1, b:0),
% 0.73/1.36 j [48, 1] (w:1, o:22, a:1, s:1, b:0).
% 0.73/1.36
% 0.73/1.36
% 0.73/1.36 Starting Search:
% 0.73/1.36
% 0.73/1.36 *** allocated 15000 integers for clauses
% 0.73/1.36 Resimplifying inuse:
% 0.73/1.36 Done
% 0.73/1.36
% 0.73/1.36 Failed to find proof!
% 0.73/1.36 maxweight = 15
% 0.73/1.36 maxnrclauses = 10000000
% 0.73/1.36 Generated: 14585
% 0.73/1.36 Kept: 215
% 0.73/1.36
% 0.73/1.36
% 0.73/1.36 The strategy used was not complete!
% 0.73/1.36
% 0.73/1.36 Increased maxweight to 16
% 0.73/1.36
% 0.73/1.36 Starting Search:
% 0.73/1.36
% 0.73/1.36 *** allocated 22500 integers for clauses
% 0.73/1.36
% 0.73/1.36 Bliksems!, er is een bewijs:
% 0.73/1.36 % SZS status Theorem
% 0.73/1.36 % SZS output start Refutation
% 0.73/1.36
% 0.73/1.36 (1) {G0,W3,D2,L1,V0,M1} I { ! e12 ==> e10 }.
% 0.73/1.36 (10) {G0,W3,D2,L1,V0,M1} I { ! e21 ==> e20 }.
% 0.73/1.36 (11) {G0,W3,D2,L1,V0,M1} I { ! e22 ==> e20 }.
% 0.73/1.36 (14) {G0,W3,D2,L1,V0,M1} I { ! e22 ==> e21 }.
% 0.73/1.36 (16) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e21 }.
% 0.73/1.36 (18) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e22 }.
% 0.73/1.36 (19) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e23 }.
% 0.73/1.36 (45) {G0,W5,D3,L1,V0,M1} I { op1( e10, e10 ) ==> e10 }.
% 0.73/1.36 (57) {G0,W5,D3,L1,V0,M1} I { op1( e12, e12 ) ==> e10 }.
% 0.73/1.36 (72) {G0,W5,D3,L1,V0,M1} I { op2( e20, e22 ) ==> e22 }.
% 0.73/1.36 (76) {G0,W5,D3,L1,V0,M1} I { op2( e21, e21 ) ==> e22 }.
% 0.73/1.36 (77) {G0,W5,D3,L1,V0,M1} I { op2( e21, e22 ) ==> e23 }.
% 0.73/1.36 (82) {G0,W5,D3,L1,V0,M1} I { op2( e22, e22 ) ==> e21 }.
% 0.73/1.36 (88) {G0,W5,D3,L1,V0,M1} I { op2( e23, e23 ) ==> e21 }.
% 0.73/1.36 (94) {G0,W5,D3,L1,V0,M1} I { op2( e24, e24 ) ==> e21 }.
% 0.73/1.36 (95) {G0,W20,D3,L5,V0,M5} I { h( e10 ) ==> e20, h( e10 ) ==> e21, h( e10 )
% 0.73/1.36 ==> e22, h( e10 ) ==> e23, h( e10 ) ==> e24 }.
% 0.73/1.36 (97) {G0,W20,D3,L5,V0,M5} I { h( e12 ) ==> e20, h( e12 ) ==> e21, h( e12 )
% 0.73/1.36 ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 0.73/1.36 (105) {G1,W8,D4,L1,V0,M1} I;d(45) { op2( h( e10 ), h( e10 ) ) ==> h( e10 )
% 0.73/1.36 }.
% 0.73/1.36 (117) {G1,W8,D4,L1,V0,M1} I;d(57) { op2( h( e12 ), h( e12 ) ) ==> h( e10 )
% 0.73/1.36 }.
% 0.73/1.36 (132) {G1,W8,D4,L1,V0,M1} I;d(72) { op1( j( e20 ), j( e22 ) ) ==> j( e22 )
% 0.73/1.36 }.
% 0.73/1.36 (136) {G1,W8,D4,L1,V0,M1} I;d(76) { op1( j( e21 ), j( e21 ) ) ==> j( e22 )
% 0.73/1.36 }.
% 0.73/1.36 (137) {G1,W8,D4,L1,V0,M1} I;d(77) { op1( j( e21 ), j( e22 ) ) ==> j( e23 )
% 0.73/1.36 }.
% 0.73/1.36 (148) {G1,W8,D4,L1,V0,M1} I;d(88) { op1( j( e23 ), j( e23 ) ) ==> j( e21 )
% 0.73/1.36 }.
% 0.73/1.36 (156) {G0,W5,D4,L1,V0,M1} I { h( j( e21 ) ) ==> e21 }.
% 0.73/1.36 (157) {G0,W5,D4,L1,V0,M1} I { h( j( e22 ) ) ==> e22 }.
% 0.73/1.36 (160) {G0,W5,D4,L1,V0,M1} I { j( h( e10 ) ) ==> e10 }.
% 0.73/1.36 (162) {G0,W5,D4,L1,V0,M1} I { j( h( e12 ) ) ==> e12 }.
% 0.73/1.36 (178) {G1,W20,D3,L5,V0,M5} P(97,162) { j( e23 ) ==> e12, h( e12 ) ==> e20,
% 0.73/1.36 h( e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==> e24 }.
% 0.73/1.36 (215) {G2,W16,D3,L4,V0,M4} P(95,105);d(76);r(14) { h( e10 ) ==> e20, h( e10
% 0.73/1.36 ) ==> e22, h( e10 ) ==> e23, h( e10 ) ==> e24 }.
% 0.73/1.36 (216) {G3,W15,D3,L4,V0,M4} P(95,105);d(82);d(215);r(14) { h( e10 ) ==> e20
% 0.73/1.36 , h( e10 ) ==> e23, h( e10 ) ==> e24, e22 ==> e21 }.
% 0.73/1.36 (219) {G4,W12,D3,L3,V0,M3} S(216);r(14) { h( e10 ) ==> e20, h( e10 ) ==>
% 0.73/1.36 e23, h( e10 ) ==> e24 }.
% 0.73/1.36 (241) {G5,W11,D3,L3,V0,M3} P(219,105);d(88) { h( e10 ) ==> e20, h( e10 )
% 0.73/1.36 ==> e24, e23 ==> e21 }.
% 0.73/1.36 (242) {G5,W11,D3,L3,V0,M3} P(219,105);d(94) { h( e10 ) ==> e20, h( e10 )
% 0.73/1.36 ==> e23, e24 ==> e21 }.
% 0.73/1.36 (247) {G6,W12,D3,L3,V0,M3} P(219,160);d(241) { h( e10 ) ==> e20, h( e10 )
% 0.73/1.36 ==> e24, j( e21 ) ==> e10 }.
% 0.73/1.36 (248) {G7,W8,D3,L2,V0,M2} P(219,160);d(242);d(247);r(19) { h( e10 ) ==> e20
% 0.73/1.36 , j( e21 ) ==> e10 }.
% 0.73/1.36 (259) {G8,W8,D3,L2,V0,M2} P(248,136);d(45) { h( e10 ) ==> e20, j( e22 ) ==>
% 0.73/1.36 e10 }.
% 0.73/1.36 (263) {G8,W8,D3,L2,V0,M2} P(248,156) { h( e10 ) ==> e21, h( e10 ) ==> e20
% 0.73/1.36 }.
% 0.73/1.36 (273) {G9,W7,D3,L2,V0,M2} P(259,157);d(263) { h( e10 ) ==> e20, e22 ==> e21
% 0.73/1.36 }.
% 0.73/1.36 (275) {G10,W4,D3,L1,V0,M1} S(273);r(14) { h( e10 ) ==> e20 }.
% 0.73/1.36 (284) {G11,W4,D3,L1,V0,M1} P(275,160) { j( e20 ) ==> e10 }.
% 0.73/1.36 (287) {G12,W7,D4,L1,V0,M1} P(284,132) { op1( e10, j( e22 ) ) ==> j( e22 )
% 0.73/1.36 }.
% 0.73/1.36 (307) {G11,W16,D3,L4,V0,M4} P(178,117);d(76);d(275);r(11) { j( e23 ) ==>
% 0.73/1.36 e12, h( e12 ) ==> e20, h( e12 ) ==> e22, h( e12 ) ==> e24 }.
% 0.73/1.36 (308) {G12,W15,D3,L4,V0,M4} P(178,117);d(82);d(307);d(275);r(14) { j( e23 )
% 0.73/1.36 ==> e12, h( e12 ) ==> e20, h( e12 ) ==> e24, e21 ==> e20 }.
% 0.73/1.36 (309) {G13,W14,D3,L4,V0,M4} P(178,117);d(94);d(307);d(275);d(308);r(16) { j
% 0.73/1.36 ( e23 ) ==> e12, h( e12 ) ==> e20, e21 ==> e20, e24 ==> e22 }.
% 0.73/1.36 (311) {G14,W8,D3,L2,V0,M2} S(309);r(10);r(18) { j( e23 ) ==> e12, h( e12 )
% 0.73/1.36 ==> e20 }.
% 0.73/1.36 (322) {G15,W7,D3,L2,V0,M2} P(311,162);d(284) { j( e23 ) ==> e12, e12 ==>
% 0.73/1.36 e10 }.
% 0.73/1.36 (323) {G16,W4,D3,L1,V0,M1} S(322);r(1) { j( e23 ) ==> e12 }.
% 0.73/1.36 (328) {G17,W4,D3,L1,V0,M1} P(323,148);d(57) { j( e21 ) ==> e10 }.
% 0.73/1.36 (333) {G18,W4,D3,L1,V0,M1} P(328,136);d(45) { j( e22 ) ==> e10 }.
% 0.73/1.36 (334) {G19,W3,D2,L1,V0,M1} P(328,137);d(287);d(333);d(323) { e12 ==> e10
% 0.73/1.36 }.
% 0.73/1.36 (337) {G20,W0,D0,L0,V0,M0} S(334);r(1) { }.
% 0.73/1.36
% 0.73/1.36
% 0.73/1.36 % SZS output end Refutation
% 0.73/1.36 found a proof!
% 0.73/1.36
% 0.73/1.36 *** allocated 33750 integers for clauses
% 0.73/1.36
% 0.73/1.36 Unprocessed initial clauses:
% 0.73/1.36
% 0.73/1.36 (339) {G0,W3,D2,L1,V0,M1} { ! e10 = e11 }.
% 0.73/1.36 (340) {G0,W3,D2,L1,V0,M1} { ! e10 = e12 }.
% 0.73/1.36 (341) {G0,W3,D2,L1,V0,M1} { ! e10 = e13 }.
% 0.73/1.36 (342) {G0,W3,D2,L1,V0,M1} { ! e10 = e14 }.
% 0.73/1.36 (343) {G0,W3,D2,L1,V0,M1} { ! e11 = e12 }.
% 0.73/1.36 (344) {G0,W3,D2,L1,V0,M1} { ! e11 = e13 }.
% 0.73/1.36 (345) {G0,W3,D2,L1,V0,M1} { ! e11 = e14 }.
% 0.73/1.36 (346) {G0,W3,D2,L1,V0,M1} { ! e12 = e13 }.
% 0.73/1.36 (347) {G0,W3,D2,L1,V0,M1} { ! e12 = e14 }.
% 0.73/1.36 (348) {G0,W3,D2,L1,V0,M1} { ! e13 = e14 }.
% 0.73/1.36 (349) {G0,W3,D2,L1,V0,M1} { ! e20 = e21 }.
% 0.73/1.36 (350) {G0,W3,D2,L1,V0,M1} { ! e20 = e22 }.
% 0.73/1.36 (351) {G0,W3,D2,L1,V0,M1} { ! e20 = e23 }.
% 0.73/1.36 (352) {G0,W3,D2,L1,V0,M1} { ! e20 = e24 }.
% 0.73/1.36 (353) {G0,W3,D2,L1,V0,M1} { ! e21 = e22 }.
% 0.73/1.36 (354) {G0,W3,D2,L1,V0,M1} { ! e21 = e23 }.
% 0.73/1.36 (355) {G0,W3,D2,L1,V0,M1} { ! e21 = e24 }.
% 0.73/1.36 (356) {G0,W3,D2,L1,V0,M1} { ! e22 = e23 }.
% 0.73/1.36 (357) {G0,W3,D2,L1,V0,M1} { ! e22 = e24 }.
% 0.73/1.36 (358) {G0,W3,D2,L1,V0,M1} { ! e23 = e24 }.
% 0.73/1.36 (359) {G0,W3,D2,L1,V0,M1} { ! e10 = e20 }.
% 0.73/1.36 (360) {G0,W3,D2,L1,V0,M1} { ! e10 = e21 }.
% 0.73/1.36 (361) {G0,W3,D2,L1,V0,M1} { ! e10 = e22 }.
% 0.73/1.36 (362) {G0,W3,D2,L1,V0,M1} { ! e10 = e23 }.
% 0.73/1.36 (363) {G0,W3,D2,L1,V0,M1} { ! e10 = e24 }.
% 0.73/1.36 (364) {G0,W3,D2,L1,V0,M1} { ! e11 = e20 }.
% 0.73/1.36 (365) {G0,W3,D2,L1,V0,M1} { ! e11 = e21 }.
% 0.73/1.36 (366) {G0,W3,D2,L1,V0,M1} { ! e11 = e22 }.
% 0.73/1.36 (367) {G0,W3,D2,L1,V0,M1} { ! e11 = e23 }.
% 0.73/1.36 (368) {G0,W3,D2,L1,V0,M1} { ! e11 = e24 }.
% 0.73/1.36 (369) {G0,W3,D2,L1,V0,M1} { ! e12 = e20 }.
% 0.73/1.36 (370) {G0,W3,D2,L1,V0,M1} { ! e12 = e21 }.
% 0.73/1.36 (371) {G0,W3,D2,L1,V0,M1} { ! e12 = e22 }.
% 0.73/1.36 (372) {G0,W3,D2,L1,V0,M1} { ! e12 = e23 }.
% 0.73/1.36 (373) {G0,W3,D2,L1,V0,M1} { ! e12 = e24 }.
% 0.73/1.36 (374) {G0,W3,D2,L1,V0,M1} { ! e13 = e20 }.
% 0.73/1.36 (375) {G0,W3,D2,L1,V0,M1} { ! e13 = e21 }.
% 0.73/1.36 (376) {G0,W3,D2,L1,V0,M1} { ! e13 = e22 }.
% 0.73/1.36 (377) {G0,W3,D2,L1,V0,M1} { ! e13 = e23 }.
% 0.73/1.36 (378) {G0,W3,D2,L1,V0,M1} { ! e13 = e24 }.
% 0.73/1.36 (379) {G0,W3,D2,L1,V0,M1} { ! e14 = e20 }.
% 0.73/1.36 (380) {G0,W3,D2,L1,V0,M1} { ! e14 = e21 }.
% 0.73/1.36 (381) {G0,W3,D2,L1,V0,M1} { ! e14 = e22 }.
% 0.73/1.36 (382) {G0,W3,D2,L1,V0,M1} { ! e14 = e23 }.
% 0.73/1.36 (383) {G0,W3,D2,L1,V0,M1} { ! e14 = e24 }.
% 0.73/1.36 (384) {G0,W5,D3,L1,V0,M1} { op1( e10, e10 ) = e10 }.
% 0.73/1.36 (385) {G0,W5,D3,L1,V0,M1} { op1( e10, e11 ) = e11 }.
% 0.73/1.36 (386) {G0,W5,D3,L1,V0,M1} { op1( e10, e12 ) = e12 }.
% 0.73/1.36 (387) {G0,W5,D3,L1,V0,M1} { op1( e10, e13 ) = e13 }.
% 0.73/1.36 (388) {G0,W5,D3,L1,V0,M1} { op1( e10, e14 ) = e14 }.
% 0.73/1.36 (389) {G0,W5,D3,L1,V0,M1} { op1( e11, e10 ) = e11 }.
% 0.73/1.36 (390) {G0,W5,D3,L1,V0,M1} { op1( e11, e11 ) = e10 }.
% 0.73/1.36 (391) {G0,W5,D3,L1,V0,M1} { op1( e11, e12 ) = e13 }.
% 0.73/1.36 (392) {G0,W5,D3,L1,V0,M1} { op1( e11, e13 ) = e14 }.
% 0.73/1.36 (393) {G0,W5,D3,L1,V0,M1} { op1( e11, e14 ) = e12 }.
% 0.73/1.36 (394) {G0,W5,D3,L1,V0,M1} { op1( e12, e10 ) = e12 }.
% 0.73/1.36 (395) {G0,W5,D3,L1,V0,M1} { op1( e12, e11 ) = e14 }.
% 0.73/1.36 (396) {G0,W5,D3,L1,V0,M1} { op1( e12, e12 ) = e10 }.
% 0.73/1.36 (397) {G0,W5,D3,L1,V0,M1} { op1( e12, e13 ) = e11 }.
% 0.73/1.36 (398) {G0,W5,D3,L1,V0,M1} { op1( e12, e14 ) = e13 }.
% 0.73/1.36 (399) {G0,W5,D3,L1,V0,M1} { op1( e13, e10 ) = e13 }.
% 0.73/1.36 (400) {G0,W5,D3,L1,V0,M1} { op1( e13, e11 ) = e12 }.
% 0.73/1.36 (401) {G0,W5,D3,L1,V0,M1} { op1( e13, e12 ) = e14 }.
% 0.73/1.36 (402) {G0,W5,D3,L1,V0,M1} { op1( e13, e13 ) = e10 }.
% 0.73/1.36 (403) {G0,W5,D3,L1,V0,M1} { op1( e13, e14 ) = e11 }.
% 0.73/1.36 (404) {G0,W5,D3,L1,V0,M1} { op1( e14, e10 ) = e14 }.
% 0.73/1.36 (405) {G0,W5,D3,L1,V0,M1} { op1( e14, e11 ) = e13 }.
% 0.73/1.36 (406) {G0,W5,D3,L1,V0,M1} { op1( e14, e12 ) = e11 }.
% 0.73/1.36 (407) {G0,W5,D3,L1,V0,M1} { op1( e14, e13 ) = e12 }.
% 0.73/1.36 (408) {G0,W5,D3,L1,V0,M1} { op1( e14, e14 ) = e10 }.
% 0.73/1.36 (409) {G0,W5,D3,L1,V0,M1} { op2( e20, e20 ) = e20 }.
% 0.73/1.36 (410) {G0,W5,D3,L1,V0,M1} { op2( e20, e21 ) = e21 }.
% 0.73/1.36 (411) {G0,W5,D3,L1,V0,M1} { op2( e20, e22 ) = e22 }.
% 0.73/1.36 (412) {G0,W5,D3,L1,V0,M1} { op2( e20, e23 ) = e23 }.
% 0.73/1.36 (413) {G0,W5,D3,L1,V0,M1} { op2( e20, e24 ) = e24 }.
% 0.73/1.36 (414) {G0,W5,D3,L1,V0,M1} { op2( e21, e20 ) = e21 }.
% 0.73/1.36 (415) {G0,W5,D3,L1,V0,M1} { op2( e21, e21 ) = e22 }.
% 0.73/1.36 (416) {G0,W5,D3,L1,V0,M1} { op2( e21, e22 ) = e23 }.
% 0.73/1.36 (417) {G0,W5,D3,L1,V0,M1} { op2( e21, e23 ) = e24 }.
% 0.73/1.36 (418) {G0,W5,D3,L1,V0,M1} { op2( e21, e24 ) = e20 }.
% 0.73/1.36 (419) {G0,W5,D3,L1,V0,M1} { op2( e22, e20 ) = e22 }.
% 0.73/1.36 (420) {G0,W5,D3,L1,V0,M1} { op2( e22, e21 ) = e24 }.
% 0.73/1.36 (421) {G0,W5,D3,L1,V0,M1} { op2( e22, e22 ) = e21 }.
% 0.73/1.36 (422) {G0,W5,D3,L1,V0,M1} { op2( e22, e23 ) = e20 }.
% 0.73/1.36 (423) {G0,W5,D3,L1,V0,M1} { op2( e22, e24 ) = e23 }.
% 0.73/1.36 (424) {G0,W5,D3,L1,V0,M1} { op2( e23, e20 ) = e23 }.
% 0.73/1.36 (425) {G0,W5,D3,L1,V0,M1} { op2( e23, e21 ) = e20 }.
% 0.73/1.36 (426) {G0,W5,D3,L1,V0,M1} { op2( e23, e22 ) = e24 }.
% 0.73/1.36 (427) {G0,W5,D3,L1,V0,M1} { op2( e23, e23 ) = e21 }.
% 0.73/1.36 (428) {G0,W5,D3,L1,V0,M1} { op2( e23, e24 ) = e22 }.
% 0.73/1.36 (429) {G0,W5,D3,L1,V0,M1} { op2( e24, e20 ) = e24 }.
% 0.73/1.36 (430) {G0,W5,D3,L1,V0,M1} { op2( e24, e21 ) = e23 }.
% 0.73/1.36 (431) {G0,W5,D3,L1,V0,M1} { op2( e24, e22 ) = e20 }.
% 0.73/1.36 (432) {G0,W5,D3,L1,V0,M1} { op2( e24, e23 ) = e22 }.
% 0.73/1.36 (433) {G0,W5,D3,L1,V0,M1} { op2( e24, e24 ) = e21 }.
% 0.73/1.36 (434) {G0,W20,D3,L5,V0,M5} { h( e10 ) = e20, h( e10 ) = e21, h( e10 ) =
% 0.73/1.36 e22, h( e10 ) = e23, h( e10 ) = e24 }.
% 0.73/1.36 (435) {G0,W20,D3,L5,V0,M5} { h( e11 ) = e20, h( e11 ) = e21, h( e11 ) =
% 0.73/1.36 e22, h( e11 ) = e23, h( e11 ) = e24 }.
% 0.73/1.36 (436) {G0,W20,D3,L5,V0,M5} { h( e12 ) = e20, h( e12 ) = e21, h( e12 ) =
% 0.73/1.36 e22, h( e12 ) = e23, h( e12 ) = e24 }.
% 0.73/1.36 (437) {G0,W20,D3,L5,V0,M5} { h( e13 ) = e20, h( e13 ) = e21, h( e13 ) =
% 0.73/1.36 e22, h( e13 ) = e23, h( e13 ) = e24 }.
% 0.73/1.36 (438) {G0,W20,D3,L5,V0,M5} { h( e14 ) = e20, h( e14 ) = e21, h( e14 ) =
% 0.73/1.36 e22, h( e14 ) = e23, h( e14 ) = e24 }.
% 0.73/1.36 (439) {G0,W20,D3,L5,V0,M5} { j( e20 ) = e10, j( e20 ) = e11, j( e20 ) =
% 0.73/1.36 e12, j( e20 ) = e13, j( e20 ) = e14 }.
% 0.73/1.36 (440) {G0,W20,D3,L5,V0,M5} { j( e21 ) = e10, j( e21 ) = e11, j( e21 ) =
% 0.73/1.36 e12, j( e21 ) = e13, j( e21 ) = e14 }.
% 0.73/1.36 (441) {G0,W20,D3,L5,V0,M5} { j( e22 ) = e10, j( e22 ) = e11, j( e22 ) =
% 0.73/1.36 e12, j( e22 ) = e13, j( e22 ) = e14 }.
% 0.73/1.36 (442) {G0,W20,D3,L5,V0,M5} { j( e23 ) = e10, j( e23 ) = e11, j( e23 ) =
% 0.73/1.36 e12, j( e23 ) = e13, j( e23 ) = e14 }.
% 0.73/1.36 (443) {G0,W20,D3,L5,V0,M5} { j( e24 ) = e10, j( e24 ) = e11, j( e24 ) =
% 0.73/1.36 e12, j( e24 ) = e13, j( e24 ) = e14 }.
% 0.73/1.36 (444) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e10 ) ) = op2( h( e10 ), h( e10
% 0.73/1.36 ) ) }.
% 0.73/1.36 (445) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e11 ) ) = op2( h( e10 ), h( e11
% 0.73/1.36 ) ) }.
% 0.73/1.36 (446) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e12 ) ) = op2( h( e10 ), h( e12
% 0.73/1.36 ) ) }.
% 0.73/1.36 (447) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e13 ) ) = op2( h( e10 ), h( e13
% 0.73/1.36 ) ) }.
% 0.73/1.36 (448) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e14 ) ) = op2( h( e10 ), h( e14
% 0.73/1.36 ) ) }.
% 0.73/1.36 (449) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e10 ) ) = op2( h( e11 ), h( e10
% 0.73/1.36 ) ) }.
% 0.73/1.36 (450) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e11 ) ) = op2( h( e11 ), h( e11
% 0.73/1.36 ) ) }.
% 0.73/1.36 (451) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e12 ) ) = op2( h( e11 ), h( e12
% 0.73/1.36 ) ) }.
% 0.73/1.36 (452) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e13 ) ) = op2( h( e11 ), h( e13
% 0.73/1.36 ) ) }.
% 0.73/1.36 (453) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e14 ) ) = op2( h( e11 ), h( e14
% 0.73/1.36 ) ) }.
% 0.73/1.36 (454) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e10 ) ) = op2( h( e12 ), h( e10
% 0.73/1.36 ) ) }.
% 0.73/1.36 (455) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e11 ) ) = op2( h( e12 ), h( e11
% 0.73/1.36 ) ) }.
% 0.73/1.36 (456) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e12 ) ) = op2( h( e12 ), h( e12
% 0.73/1.36 ) ) }.
% 0.73/1.36 (457) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e13 ) ) = op2( h( e12 ), h( e13
% 0.73/1.36 ) ) }.
% 0.73/1.36 (458) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e14 ) ) = op2( h( e12 ), h( e14
% 0.73/1.36 ) ) }.
% 0.73/1.36 (459) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e10 ) ) = op2( h( e13 ), h( e10
% 0.73/1.36 ) ) }.
% 0.73/1.36 (460) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e11 ) ) = op2( h( e13 ), h( e11
% 0.73/1.36 ) ) }.
% 0.73/1.36 (461) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e12 ) ) = op2( h( e13 ), h( e12
% 0.73/1.36 ) ) }.
% 0.73/1.36 (462) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e13 ) ) = op2( h( e13 ), h( e13
% 0.73/1.36 ) ) }.
% 0.73/1.36 (463) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e14 ) ) = op2( h( e13 ), h( e14
% 0.73/1.36 ) ) }.
% 0.73/1.36 (464) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e10 ) ) = op2( h( e14 ), h( e10
% 0.73/1.36 ) ) }.
% 0.73/1.36 (465) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e11 ) ) = op2( h( e14 ), h( e11
% 0.73/1.36 ) ) }.
% 0.73/1.36 (466) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e12 ) ) = op2( h( e14 ), h( e12
% 0.73/1.36 ) ) }.
% 0.73/1.36 (467) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e13 ) ) = op2( h( e14 ), h( e13
% 0.73/1.36 ) ) }.
% 0.73/1.36 (468) {G0,W10,D4,L1,V0,M1} { h( op1( e14, e14 ) ) = op2( h( e14 ), h( e14
% 0.73/1.36 ) ) }.
% 0.73/1.36 (469) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e20 ) ) = op1( j( e20 ), j( e20
% 0.73/1.36 ) ) }.
% 0.73/1.36 (470) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e21 ) ) = op1( j( e20 ), j( e21
% 0.73/1.36 ) ) }.
% 0.73/1.36 (471) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e22 ) ) = op1( j( e20 ), j( e22
% 0.73/1.36 ) ) }.
% 0.73/1.36 (472) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e23 ) ) = op1( j( e20 ), j( e23
% 0.73/1.36 ) ) }.
% 0.73/1.36 (473) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e24 ) ) = op1( j( e20 ), j( e24
% 0.73/1.36 ) ) }.
% 0.73/1.36 (474) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e20 ) ) = op1( j( e21 ), j( e20
% 0.73/1.36 ) ) }.
% 0.73/1.36 (475) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e21 ) ) = op1( j( e21 ), j( e21
% 0.73/1.36 ) ) }.
% 0.73/1.36 (476) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e22 ) ) = op1( j( e21 ), j( e22
% 0.73/1.36 ) ) }.
% 0.73/1.36 (477) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e23 ) ) = op1( j( e21 ), j( e23
% 0.73/1.36 ) ) }.
% 0.73/1.36 (478) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e24 ) ) = op1( j( e21 ), j( e24
% 0.73/1.36 ) ) }.
% 0.73/1.36 (479) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e20 ) ) = op1( j( e22 ), j( e20
% 0.73/1.36 ) ) }.
% 0.73/1.36 (480) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e21 ) ) = op1( j( e22 ), j( e21
% 0.73/1.36 ) ) }.
% 0.73/1.36 (481) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e22 ) ) = op1( j( e22 ), j( e22
% 0.73/1.36 ) ) }.
% 0.73/1.36 (482) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e23 ) ) = op1( j( e22 ), j( e23
% 0.73/1.36 ) ) }.
% 0.73/1.36 (483) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e24 ) ) = op1( j( e22 ), j( e24
% 0.73/1.36 ) ) }.
% 0.73/1.36 (484) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e20 ) ) = op1( j( e23 ), j( e20
% 0.73/1.36 ) ) }.
% 0.73/1.36 (485) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e21 ) ) = op1( j( e23 ), j( e21
% 0.73/1.36 ) ) }.
% 0.73/1.36 (486) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e22 ) ) = op1( j( e23 ), j( e22
% 0.73/1.36 ) ) }.
% 0.73/1.36 (487) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e23 ) ) = op1( j( e23 ), j( e23
% 0.73/1.36 ) ) }.
% 0.73/1.36 (488) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e24 ) ) = op1( j( e23 ), j( e24
% 0.73/1.36 ) ) }.
% 0.73/1.36 (489) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e20 ) ) = op1( j( e24 ), j( e20
% 0.73/1.36 ) ) }.
% 0.73/1.36 (490) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e21 ) ) = op1( j( e24 ), j( e21
% 0.73/1.36 ) ) }.
% 0.73/1.36 (491) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e22 ) ) = op1( j( e24 ), j( e22
% 0.73/1.36 ) ) }.
% 0.73/1.36 (492) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e23 ) ) = op1( j( e24 ), j( e23
% 0.73/1.36 ) ) }.
% 0.73/1.36 (493) {G0,W10,D4,L1,V0,M1} { j( op2( e24, e24 ) ) = op1( j( e24 ), j( e24
% 0.73/1.36 ) ) }.
% 0.73/1.36 (494) {G0,W5,D4,L1,V0,M1} { h( j( e20 ) ) = e20 }.
% 0.73/1.36 (495) {G0,W5,D4,L1,V0,M1} { h( j( e21 ) ) = e21 }.
% 0.73/1.36 (496) {G0,W5,D4,L1,V0,M1} { h( j( e22 ) ) = e22 }.
% 0.73/1.36 (497) {G0,W5,D4,L1,V0,M1} { h( j( e23 ) ) = e23 }.
% 0.73/1.36 (498) {G0,W5,D4,L1,V0,M1} { h( j( e24 ) ) = e24 }.
% 0.73/1.36 (499) {G0,W5,D4,L1,V0,M1} { j( h( e10 ) ) = e10 }.
% 0.73/1.36 (500) {G0,W5,D4,L1,V0,M1} { j( h( e11 ) ) = e11 }.
% 0.73/1.36 (501) {G0,W5,D4,L1,V0,M1} { j( h( e12 ) ) = e12 }.
% 0.73/1.36 (502) {G0,W5,D4,L1,V0,M1} { j( h( e13 ) ) = e13 }.
% 0.73/1.36 (503) {G0,W5,D4,L1,V0,M1} { j( h( e14 ) ) = e14 }.
% 0.73/1.36
% 0.73/1.36
% 0.73/1.36 Total Proof:
% 0.73/1.36
% 0.73/1.36 eqswap: (505) {G0,W3,D2,L1,V0,M1} { ! e12 = e10 }.
% 0.73/1.36 parent0[0]: (340) {G0,W3,D2,L1,V0,M1} { ! e10 = e12 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (1) {G0,W3,D2,L1,V0,M1} I { ! e12 ==> e10 }.
% 0.73/1.36 parent0: (505) {G0,W3,D2,L1,V0,M1} { ! e12 = e10 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 eqswap: (516) {G0,W3,D2,L1,V0,M1} { ! e21 = e20 }.
% 0.73/1.36 parent0[0]: (349) {G0,W3,D2,L1,V0,M1} { ! e20 = e21 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (10) {G0,W3,D2,L1,V0,M1} I { ! e21 ==> e20 }.
% 0.73/1.36 parent0: (516) {G0,W3,D2,L1,V0,M1} { ! e21 = e20 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 eqswap: (528) {G0,W3,D2,L1,V0,M1} { ! e22 = e20 }.
% 0.73/1.36 parent0[0]: (350) {G0,W3,D2,L1,V0,M1} { ! e20 = e22 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (11) {G0,W3,D2,L1,V0,M1} I { ! e22 ==> e20 }.
% 0.73/1.36 parent0: (528) {G0,W3,D2,L1,V0,M1} { ! e22 = e20 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 eqswap: (543) {G0,W3,D2,L1,V0,M1} { ! e22 = e21 }.
% 0.73/1.36 parent0[0]: (353) {G0,W3,D2,L1,V0,M1} { ! e21 = e22 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (14) {G0,W3,D2,L1,V0,M1} I { ! e22 ==> e21 }.
% 0.73/1.36 parent0: (543) {G0,W3,D2,L1,V0,M1} { ! e22 = e21 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 eqswap: (560) {G0,W3,D2,L1,V0,M1} { ! e24 = e21 }.
% 0.73/1.36 parent0[0]: (355) {G0,W3,D2,L1,V0,M1} { ! e21 = e24 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (16) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e21 }.
% 0.73/1.38 parent0: (560) {G0,W3,D2,L1,V0,M1} { ! e24 = e21 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 eqswap: (579) {G0,W3,D2,L1,V0,M1} { ! e24 = e22 }.
% 0.73/1.38 parent0[0]: (357) {G0,W3,D2,L1,V0,M1} { ! e22 = e24 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (18) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e22 }.
% 0.73/1.38 parent0: (579) {G0,W3,D2,L1,V0,M1} { ! e24 = e22 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 eqswap: (599) {G0,W3,D2,L1,V0,M1} { ! e24 = e23 }.
% 0.73/1.38 parent0[0]: (358) {G0,W3,D2,L1,V0,M1} { ! e23 = e24 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (19) {G0,W3,D2,L1,V0,M1} I { ! e24 ==> e23 }.
% 0.73/1.38 parent0: (599) {G0,W3,D2,L1,V0,M1} { ! e24 = e23 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (45) {G0,W5,D3,L1,V0,M1} I { op1( e10, e10 ) ==> e10 }.
% 0.73/1.38 parent0: (384) {G0,W5,D3,L1,V0,M1} { op1( e10, e10 ) = e10 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (57) {G0,W5,D3,L1,V0,M1} I { op1( e12, e12 ) ==> e10 }.
% 0.73/1.38 parent0: (396) {G0,W5,D3,L1,V0,M1} { op1( e12, e12 ) = e10 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (72) {G0,W5,D3,L1,V0,M1} I { op2( e20, e22 ) ==> e22 }.
% 0.73/1.38 parent0: (411) {G0,W5,D3,L1,V0,M1} { op2( e20, e22 ) = e22 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (76) {G0,W5,D3,L1,V0,M1} I { op2( e21, e21 ) ==> e22 }.
% 0.73/1.38 parent0: (415) {G0,W5,D3,L1,V0,M1} { op2( e21, e21 ) = e22 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (77) {G0,W5,D3,L1,V0,M1} I { op2( e21, e22 ) ==> e23 }.
% 0.73/1.38 parent0: (416) {G0,W5,D3,L1,V0,M1} { op2( e21, e22 ) = e23 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 *** allocated 50625 integers for clauses
% 0.73/1.38 subsumption: (82) {G0,W5,D3,L1,V0,M1} I { op2( e22, e22 ) ==> e21 }.
% 0.73/1.38 parent0: (421) {G0,W5,D3,L1,V0,M1} { op2( e22, e22 ) = e21 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 *** allocated 15000 integers for termspace/termends
% 0.73/1.38 subsumption: (88) {G0,W5,D3,L1,V0,M1} I { op2( e23, e23 ) ==> e21 }.
% 0.73/1.38 parent0: (427) {G0,W5,D3,L1,V0,M1} { op2( e23, e23 ) = e21 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (94) {G0,W5,D3,L1,V0,M1} I { op2( e24, e24 ) ==> e21 }.
% 0.73/1.38 parent0: (433) {G0,W5,D3,L1,V0,M1} { op2( e24, e24 ) = e21 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (95) {G0,W20,D3,L5,V0,M5} I { h( e10 ) ==> e20, h( e10 ) ==>
% 0.73/1.38 e21, h( e10 ) ==> e22, h( e10 ) ==> e23, h( e10 ) ==> e24 }.
% 0.73/1.38 parent0: (434) {G0,W20,D3,L5,V0,M5} { h( e10 ) = e20, h( e10 ) = e21, h(
% 0.73/1.38 e10 ) = e22, h( e10 ) = e23, h( e10 ) = e24 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 1 ==> 1
% 0.73/1.38 2 ==> 2
% 0.73/1.38 3 ==> 3
% 0.73/1.38 4 ==> 4
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (97) {G0,W20,D3,L5,V0,M5} I { h( e12 ) ==> e20, h( e12 ) ==>
% 0.73/1.38 e21, h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 0.73/1.38 parent0: (436) {G0,W20,D3,L5,V0,M5} { h( e12 ) = e20, h( e12 ) = e21, h(
% 0.73/1.38 e12 ) = e22, h( e12 ) = e23, h( e12 ) = e24 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 1 ==> 1
% 0.73/1.38 2 ==> 2
% 0.73/1.38 3 ==> 3
% 0.73/1.38 4 ==> 4
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 *** allocated 22500 integers for termspace/termends
% 0.73/1.38 *** allocated 75937 integers for clauses
% 0.73/1.38 paramod: (2027) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e10 ), h( e10 ) )
% 0.73/1.38 }.
% 0.73/1.38 parent0[0]: (45) {G0,W5,D3,L1,V0,M1} I { op1( e10, e10 ) ==> e10 }.
% 0.73/1.38 parent1[0; 2]: (444) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e10 ) ) = op2( h
% 0.73/1.38 ( e10 ), h( e10 ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 eqswap: (2028) {G1,W8,D4,L1,V0,M1} { op2( h( e10 ), h( e10 ) ) = h( e10 )
% 0.73/1.38 }.
% 0.73/1.38 parent0[0]: (2027) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e10 ), h( e10
% 0.73/1.38 ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 subsumption: (105) {G1,W8,D4,L1,V0,M1} I;d(45) { op2( h( e10 ), h( e10 ) )
% 0.73/1.38 ==> h( e10 ) }.
% 0.73/1.38 parent0: (2028) {G1,W8,D4,L1,V0,M1} { op2( h( e10 ), h( e10 ) ) = h( e10 )
% 0.73/1.38 }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 permutation0:
% 0.73/1.38 0 ==> 0
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 *** allocated 33750 integers for termspace/termends
% 0.73/1.38 paramod: (2567) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e12 ), h( e12 ) )
% 0.73/1.38 }.
% 0.73/1.38 parent0[0]: (57) {G0,W5,D3,L1,V0,M1} I { op1( e12, e12 ) ==> e10 }.
% 0.73/1.38 parent1[0; 2]: (456) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e12 ) ) = op2( h
% 0.73/1.38 ( e12 ), h( e12 ) ) }.
% 0.73/1.38 substitution0:
% 0.73/1.38 end
% 0.73/1.38 substitution1:
% 0.73/1.38 end
% 0.73/1.38
% 0.73/1.38 eqswap: (2568) {G1,W8,D4,L1,V0,M1} { op2( h( e12 ), h( e12 ) ) = h( e10 )
% 0.73/1.43 }.
% 0.73/1.43 parent0[0]: (2567) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e12 ), h( e12
% 0.73/1.43 ) ) }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 subsumption: (117) {G1,W8,D4,L1,V0,M1} I;d(57) { op2( h( e12 ), h( e12 ) )
% 0.73/1.43 ==> h( e10 ) }.
% 0.73/1.43 parent0: (2568) {G1,W8,D4,L1,V0,M1} { op2( h( e12 ), h( e12 ) ) = h( e10 )
% 0.73/1.43 }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43 permutation0:
% 0.73/1.43 0 ==> 0
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 *** allocated 113905 integers for clauses
% 0.73/1.43 *** allocated 50625 integers for termspace/termends
% 0.73/1.43 paramod: (3137) {G1,W8,D4,L1,V0,M1} { j( e22 ) = op1( j( e20 ), j( e22 ) )
% 0.73/1.43 }.
% 0.73/1.43 parent0[0]: (72) {G0,W5,D3,L1,V0,M1} I { op2( e20, e22 ) ==> e22 }.
% 0.73/1.43 parent1[0; 2]: (471) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e22 ) ) = op1( j
% 0.73/1.43 ( e20 ), j( e22 ) ) }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43 substitution1:
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 eqswap: (3138) {G1,W8,D4,L1,V0,M1} { op1( j( e20 ), j( e22 ) ) = j( e22 )
% 0.73/1.43 }.
% 0.73/1.43 parent0[0]: (3137) {G1,W8,D4,L1,V0,M1} { j( e22 ) = op1( j( e20 ), j( e22
% 0.73/1.43 ) ) }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 subsumption: (132) {G1,W8,D4,L1,V0,M1} I;d(72) { op1( j( e20 ), j( e22 ) )
% 0.73/1.43 ==> j( e22 ) }.
% 0.73/1.43 parent0: (3138) {G1,W8,D4,L1,V0,M1} { op1( j( e20 ), j( e22 ) ) = j( e22 )
% 0.73/1.43 }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43 permutation0:
% 0.73/1.43 0 ==> 0
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 paramod: (3715) {G1,W8,D4,L1,V0,M1} { j( e22 ) = op1( j( e21 ), j( e21 ) )
% 0.73/1.43 }.
% 0.73/1.43 parent0[0]: (76) {G0,W5,D3,L1,V0,M1} I { op2( e21, e21 ) ==> e22 }.
% 0.73/1.43 parent1[0; 2]: (475) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e21 ) ) = op1( j
% 0.73/1.43 ( e21 ), j( e21 ) ) }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43 substitution1:
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 eqswap: (3716) {G1,W8,D4,L1,V0,M1} { op1( j( e21 ), j( e21 ) ) = j( e22 )
% 0.73/1.43 }.
% 0.73/1.43 parent0[0]: (3715) {G1,W8,D4,L1,V0,M1} { j( e22 ) = op1( j( e21 ), j( e21
% 0.73/1.43 ) ) }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 subsumption: (136) {G1,W8,D4,L1,V0,M1} I;d(76) { op1( j( e21 ), j( e21 ) )
% 0.73/1.43 ==> j( e22 ) }.
% 0.73/1.43 parent0: (3716) {G1,W8,D4,L1,V0,M1} { op1( j( e21 ), j( e21 ) ) = j( e22 )
% 0.73/1.43 }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43 permutation0:
% 0.73/1.43 0 ==> 0
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 *** allocated 75937 integers for termspace/termends
% 0.73/1.43 paramod: (4295) {G1,W8,D4,L1,V0,M1} { j( e23 ) = op1( j( e21 ), j( e22 ) )
% 0.73/1.43 }.
% 0.73/1.43 parent0[0]: (77) {G0,W5,D3,L1,V0,M1} I { op2( e21, e22 ) ==> e23 }.
% 0.73/1.43 parent1[0; 2]: (476) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e22 ) ) = op1( j
% 0.73/1.43 ( e21 ), j( e22 ) ) }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43 substitution1:
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 eqswap: (4296) {G1,W8,D4,L1,V0,M1} { op1( j( e21 ), j( e22 ) ) = j( e23 )
% 0.73/1.43 }.
% 0.73/1.43 parent0[0]: (4295) {G1,W8,D4,L1,V0,M1} { j( e23 ) = op1( j( e21 ), j( e22
% 0.73/1.43 ) ) }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 subsumption: (137) {G1,W8,D4,L1,V0,M1} I;d(77) { op1( j( e21 ), j( e22 ) )
% 0.73/1.43 ==> j( e23 ) }.
% 0.73/1.43 parent0: (4296) {G1,W8,D4,L1,V0,M1} { op1( j( e21 ), j( e22 ) ) = j( e23 )
% 0.73/1.43 }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43 permutation0:
% 0.73/1.43 0 ==> 0
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 *** allocated 170857 integers for clauses
% 0.73/1.43 paramod: (4897) {G1,W8,D4,L1,V0,M1} { j( e21 ) = op1( j( e23 ), j( e23 ) )
% 0.73/1.43 }.
% 0.73/1.43 parent0[0]: (88) {G0,W5,D3,L1,V0,M1} I { op2( e23, e23 ) ==> e21 }.
% 0.73/1.43 parent1[0; 2]: (487) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e23 ) ) = op1( j
% 0.73/1.43 ( e23 ), j( e23 ) ) }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43 substitution1:
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 eqswap: (4898) {G1,W8,D4,L1,V0,M1} { op1( j( e23 ), j( e23 ) ) = j( e21 )
% 0.73/1.43 }.
% 0.73/1.43 parent0[0]: (4897) {G1,W8,D4,L1,V0,M1} { j( e21 ) = op1( j( e23 ), j( e23
% 0.73/1.43 ) ) }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 subsumption: (148) {G1,W8,D4,L1,V0,M1} I;d(88) { op1( j( e23 ), j( e23 ) )
% 0.73/1.43 ==> j( e21 ) }.
% 0.73/1.43 parent0: (4898) {G1,W8,D4,L1,V0,M1} { op1( j( e23 ), j( e23 ) ) = j( e21 )
% 0.73/1.43 }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43 permutation0:
% 0.73/1.43 0 ==> 0
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 subsumption: (156) {G0,W5,D4,L1,V0,M1} I { h( j( e21 ) ) ==> e21 }.
% 0.73/1.43 parent0: (495) {G0,W5,D4,L1,V0,M1} { h( j( e21 ) ) = e21 }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43 permutation0:
% 0.73/1.43 0 ==> 0
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 subsumption: (157) {G0,W5,D4,L1,V0,M1} I { h( j( e22 ) ) ==> e22 }.
% 0.73/1.43 parent0: (496) {G0,W5,D4,L1,V0,M1} { h( j( e22 ) ) = e22 }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43 permutation0:
% 0.73/1.43 0 ==> 0
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 *** allocated 113905 integers for termspace/termends
% 0.73/1.43 subsumption: (160) {G0,W5,D4,L1,V0,M1} I { j( h( e10 ) ) ==> e10 }.
% 0.73/1.43 parent0: (499) {G0,W5,D4,L1,V0,M1} { j( h( e10 ) ) = e10 }.
% 0.73/1.43 substitution0:
% 0.73/1.43 end
% 0.73/1.43 permutation0:
% 0.73/1.43 0 ==> 0
% 0.73/1.43 end
% 0.73/1.43
% 0.73/1.43 subsumption: (162) {G0,W5,D4,L1,V0,M1} I { j( h( e12 ) ) ==> e12 }.
% 0.73/1.43 parent0: (501) {G0,W5,D4,L1,V0,M1} { j( h( e12 ) ) = e12 }.
% 0.73/1.43 substitution0:
% 16.99/17.42 end
% 16.99/17.42 permutation0:
% 16.99/17.42 0 ==> 0
% 16.99/17.42 end
% 16.99/17.42
% 16.99/17.42 *** allocated 256285 integers for clauses
% 16.99/17.42 *** allocated 170857 integers for termspace/termends
% 16.99/17.42 *** allocated 15000 integers for justifications
% 16.99/17.42 *** allocated 256285 integers for termspace/termends
% 16.99/17.42 *** allocated 22500 integers for justifications
% 16.99/17.42 eqswap: (6738) {G0,W20,D3,L5,V0,M5} { e20 ==> h( e12 ), h( e12 ) ==> e21,
% 16.99/17.42 h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 16.99/17.42 parent0[0]: (97) {G0,W20,D3,L5,V0,M5} I { h( e12 ) ==> e20, h( e12 ) ==>
% 16.99/17.42 e21, h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 16.99/17.42 substitution0:
% 16.99/17.42 end
% 16.99/17.42
% 16.99/17.42 eqswap: (6769) {G0,W5,D4,L1,V0,M1} { e12 ==> j( h( e12 ) ) }.
% 16.99/17.42 parent0[0]: (162) {G0,W5,D4,L1,V0,M1} I { j( h( e12 ) ) ==> e12 }.
% 16.99/17.42 substitution0:
% 16.99/17.42 end
% 16.99/17.42
% 16.99/17.42 paramod: (6772) {G1,W20,D3,L5,V0,M5} { e12 ==> j( e23 ), e20 ==> h( e12 )
% 16.99/17.42 , h( e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==> e24 }.
% 16.99/17.42 parent0[3]: (6738) {G0,W20,D3,L5,V0,M5} { e20 ==> h( e12 ), h( e12 ) ==>
% 16.99/17.42 e21, h( e12 ) ==> e22, h( e12 ) ==> e23, h( e12 ) ==> e24 }.
% 16.99/17.42 parent1[0; 3]: (6769) {G0,W5,D4,L1,V0,M1} { e12 ==> j( h( e12 ) ) }.
% 16.99/17.42 substitution0:
% 16.99/17.42 end
% 16.99/17.42 substitution1:
% 16.99/17.42 end
% 16.99/17.42
% 16.99/17.42 eqswap: (6920) {G1,W20,D3,L5,V0,M5} { e24 ==> h( e12 ), e12 ==> j( e23 ),
% 16.99/17.42 e20 ==> h( e12 ), h( e12 ) ==> e21, h( e12 ) ==> e22 }.
% 16.99/17.42 parent0[4]: (6772) {G1,W20,D3,L5,V0,M5} { e12 ==> j( e23 ), e20 ==> h( e12
% 16.99/17.42 ), h( e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==> e24 }.
% 16.99/17.42 substitution0:
% 16.99/17.42 end
% 16.99/17.42
% 16.99/17.42 eqswap: (6924) {G1,W20,D3,L5,V0,M5} { e22 ==> h( e12 ), e24 ==> h( e12 ),
% 16.99/17.42 e12 ==> j( e23 ), e20 ==> h( e12 ), h( e12 ) ==> e21 }.
% 16.99/17.42 parent0[4]: (6920) {G1,W20,D3,L5,V0,M5} { e24 ==> h( e12 ), e12 ==> j( e23
% 16.99/17.42 ), e20 ==> h( e12 ), h( e12 ) ==> e21, h( e12 ) ==> e22 }.
% 16.99/17.42 substitution0:
% 16.99/17.42 end
% 16.99/17.42
% 16.99/17.42 eqswap: (6927) {G1,W20,D3,L5,V0,M5} { e21 ==> h( e12 ), e22 ==> h( e12 ),
% 16.99/17.42 e24 ==> h( e12 ), e12 ==> j( e23 ), e20 ==> h( e12 ) }.
% 16.99/17.42 parent0[4]: (6924) {G1,W20,D3,L5,V0,M5} { e22 ==> h( e12 ), e24 ==> h( e12
% 16.99/17.42 ), e12 ==> j( e23 ), e20 ==> h( e12 ), h( e12 ) ==> e21 }.
% 16.99/17.42 substitution0:
% 16.99/17.42 end
% 16.99/17.42
% 16.99/17.42 eqswap: (6930) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e20, e21 ==> h( e12 ),
% 16.99/17.42 e22 ==> h( e12 ), e24 ==> h( e12 ), e12 ==> j( e23 ) }.
% 16.99/17.42 parent0[4]: (6927) {G1,W20,D3,L5,V0,M5} { e21 ==> h( e12 ), e22 ==> h( e12
% 16.99/17.42 ), e24 ==> h( e12 ), e12 ==> j( e23 ), e20 ==> h( e12 ) }.
% 16.99/17.42 substitution0:
% 16.99/17.42 end
% 16.99/17.42
% 16.99/17.42 eqswap: (6933) {G1,W20,D3,L5,V0,M5} { j( e23 ) ==> e12, h( e12 ) ==> e20,
% 16.99/17.42 e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ) }.
% 16.99/17.42 parent0[4]: (6930) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e20, e21 ==> h( e12
% 16.99/17.42 ), e22 ==> h( e12 ), e24 ==> h( e12 ), e12 ==> j( e23 ) }.
% 16.99/17.42 substitution0:
% 16.99/17.42 end
% 16.99/17.42
% 16.99/17.42 eqswap: (6936) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e24, j( e23 ) ==> e12,
% 16.99/17.42 h( e12 ) ==> e20, e21 ==> h( e12 ), e22 ==> h( e12 ) }.
% 16.99/17.42 parent0[4]: (6933) {G1,W20,D3,L5,V0,M5} { j( e23 ) ==> e12, h( e12 ) ==>
% 16.99/17.42 e20, e21 ==> h( e12 ), e22 ==> h( e12 ), e24 ==> h( e12 ) }.
% 16.99/17.42 substitution0:
% 16.99/17.42 end
% 16.99/17.42
% 16.99/17.42 eqswap: (6939) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e22, h( e12 ) ==> e24,
% 16.99/17.42 j( e23 ) ==> e12, h( e12 ) ==> e20, e21 ==> h( e12 ) }.
% 16.99/17.42 parent0[4]: (6936) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e24, j( e23 ) ==>
% 16.99/17.42 e12, h( e12 ) ==> e20, e21 ==> h( e12 ), e22 ==> h( e12 ) }.
% 16.99/17.42 substitution0:
% 16.99/17.42 end
% 16.99/17.42
% 16.99/17.42 eqswap: (6942) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e21, h( e12 ) ==> e22,
% 16.99/17.42 h( e12 ) ==> e24, j( e23 ) ==> e12, h( e12 ) ==> e20 }.
% 16.99/17.42 parent0[4]: (6939) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e22, h( e12 ) ==>
% 16.99/17.42 e24, j( e23 ) ==> e12, h( e12 ) ==> e20, e21 ==> h( e12 ) }.
% 16.99/17.42 substitution0:
% 16.99/17.42 end
% 16.99/17.42
% 16.99/17.42 subsumption: (178) {G1,W20,D3,L5,V0,M5} P(97,162) { j( e23 ) ==> e12, h(
% 16.99/17.42 e12 ) ==> e20, h( e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==> e24 }.
% 16.99/17.42 parent0: (6942) {G1,W20,D3,L5,V0,M5} { h( e12 ) ==> e21, h( e12 ) ==> e22
% 16.99/17.42 , h( e12 ) ==> e24, j( e23 ) ==> e12, h( e12 ) ==> e20 }.
% 16.99/17.42 substitution0:
% 16.99/17.42 end
% 16.99/17.42 permutation0:
% 16.99/17.42 0 ==> 2
% 16.99/17.42 1 ==> 3
% 16.99/17.42 2 ==> 4
% 16.99/17.42 3 ==> 0
% 16.99/17.42 4 ==> 1
% 16.99/17.42 end
% 16.99/17.42
% 16.99/17.42 *** allocated 384427 integers for clauses
% 16.99/17.42
% 16.99/17.42 ==> (215) {G2,W16,D3,L4,V0,M4} P(95,105);d(76);r(14) { h( e10 ) ==> e20, h
% 16.99/17.42 ( e10 ) ==> e22, h( e10 ) ==> e23, h( e10 ) ==> e24 }.
% 16.99/17.42
% 16.99/17.42
% 16.99/17.42
% 16.99/17.42 !!! Internal Problem: OH, OH, COULD NOT DERIVE GOAL !!!
% 16.99/17.42
% 16.99/17.42 Bliksem ended
%------------------------------------------------------------------------------