%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : ALG042+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n029.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:14 EDT 2022
% Result : Theorem 0.72s 1.11s
% Output : Refutation 0.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : ALG042+1 : TPTP v8.1.0. Released v2.7.0.
% 0.06/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n029.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Wed Jun 8 14:47:06 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.72/1.11 *** allocated 10000 integers for termspace/termends
% 0.72/1.11 *** allocated 10000 integers for clauses
% 0.72/1.11 *** allocated 10000 integers for justifications
% 0.72/1.11 Bliksem 1.12
% 0.72/1.11
% 0.72/1.11
% 0.72/1.11 Automatic Strategy Selection
% 0.72/1.11
% 0.72/1.11
% 0.72/1.11 Clauses:
% 0.72/1.11
% 0.72/1.11 { ! e10 = e11 }.
% 0.72/1.11 { ! e10 = e12 }.
% 0.72/1.11 { ! e10 = e13 }.
% 0.72/1.11 { ! e11 = e12 }.
% 0.72/1.11 { ! e11 = e13 }.
% 0.72/1.11 { ! e12 = e13 }.
% 0.72/1.11 { ! e20 = e21 }.
% 0.72/1.11 { ! e20 = e22 }.
% 0.72/1.11 { ! e20 = e23 }.
% 0.72/1.11 { ! e21 = e22 }.
% 0.72/1.11 { ! e21 = e23 }.
% 0.72/1.11 { ! e22 = e23 }.
% 0.72/1.11 { ! e10 = e20 }.
% 0.72/1.11 { ! e10 = e21 }.
% 0.72/1.11 { ! e10 = e22 }.
% 0.72/1.11 { ! e10 = e23 }.
% 0.72/1.11 { ! e11 = e20 }.
% 0.72/1.11 { ! e11 = e21 }.
% 0.72/1.11 { ! e11 = e22 }.
% 0.72/1.11 { ! e11 = e23 }.
% 0.72/1.11 { ! e12 = e20 }.
% 0.72/1.11 { ! e12 = e21 }.
% 0.72/1.11 { ! e12 = e22 }.
% 0.72/1.11 { ! e12 = e23 }.
% 0.72/1.11 { ! e13 = e20 }.
% 0.72/1.11 { ! e13 = e21 }.
% 0.72/1.11 { ! e13 = e22 }.
% 0.72/1.11 { ! e13 = e23 }.
% 0.72/1.11 { op1( e10, e10 ) = e10 }.
% 0.72/1.11 { op1( e10, e11 ) = e11 }.
% 0.72/1.11 { op1( e10, e12 ) = e12 }.
% 0.72/1.11 { op1( e10, e13 ) = e13 }.
% 0.72/1.11 { op1( e11, e10 ) = e11 }.
% 0.72/1.11 { op1( e11, e11 ) = e10 }.
% 0.72/1.11 { op1( e11, e12 ) = e13 }.
% 0.72/1.11 { op1( e11, e13 ) = e12 }.
% 0.72/1.11 { op1( e12, e10 ) = e12 }.
% 0.72/1.11 { op1( e12, e11 ) = e13 }.
% 0.72/1.11 { op1( e12, e12 ) = e10 }.
% 0.72/1.11 { op1( e12, e13 ) = e11 }.
% 0.72/1.11 { op1( e13, e10 ) = e13 }.
% 0.72/1.11 { op1( e13, e11 ) = e12 }.
% 0.72/1.11 { op1( e13, e12 ) = e11 }.
% 0.72/1.11 { op1( e13, e13 ) = e10 }.
% 0.72/1.11 { op2( e20, e20 ) = e20 }.
% 0.72/1.11 { op2( e20, e21 ) = e21 }.
% 0.72/1.11 { op2( e20, e22 ) = e22 }.
% 0.72/1.11 { op2( e20, e23 ) = e23 }.
% 0.72/1.11 { op2( e21, e20 ) = e21 }.
% 0.72/1.11 { op2( e21, e21 ) = e23 }.
% 0.72/1.11 { op2( e21, e22 ) = e20 }.
% 0.72/1.11 { op2( e21, e23 ) = e22 }.
% 0.72/1.11 { op2( e22, e20 ) = e22 }.
% 0.72/1.11 { op2( e22, e21 ) = e20 }.
% 0.72/1.11 { op2( e22, e22 ) = e23 }.
% 0.72/1.11 { op2( e22, e23 ) = e21 }.
% 0.72/1.11 { op2( e23, e20 ) = e23 }.
% 0.72/1.11 { op2( e23, e21 ) = e22 }.
% 0.72/1.11 { op2( e23, e22 ) = e21 }.
% 0.72/1.11 { op2( e23, e23 ) = e20 }.
% 0.72/1.11 { h( e10 ) = e20, h( e10 ) = e21, h( e10 ) = e22, h( e10 ) = e23 }.
% 0.72/1.11 { h( e11 ) = e20, h( e11 ) = e21, h( e11 ) = e22, h( e11 ) = e23 }.
% 0.72/1.11 { h( e12 ) = e20, h( e12 ) = e21, h( e12 ) = e22, h( e12 ) = e23 }.
% 0.72/1.11 { h( e13 ) = e20, h( e13 ) = e21, h( e13 ) = e22, h( e13 ) = e23 }.
% 0.72/1.11 { j( e20 ) = e10, j( e20 ) = e11, j( e20 ) = e12, j( e20 ) = e13 }.
% 0.72/1.11 { j( e21 ) = e10, j( e21 ) = e11, j( e21 ) = e12, j( e21 ) = e13 }.
% 0.72/1.11 { j( e22 ) = e10, j( e22 ) = e11, j( e22 ) = e12, j( e22 ) = e13 }.
% 0.72/1.11 { j( e23 ) = e10, j( e23 ) = e11, j( e23 ) = e12, j( e23 ) = e13 }.
% 0.72/1.11 { h( op1( e10, e10 ) ) = op2( h( e10 ), h( e10 ) ) }.
% 0.72/1.11 { h( op1( e10, e11 ) ) = op2( h( e10 ), h( e11 ) ) }.
% 0.72/1.11 { h( op1( e10, e12 ) ) = op2( h( e10 ), h( e12 ) ) }.
% 0.72/1.11 { h( op1( e10, e13 ) ) = op2( h( e10 ), h( e13 ) ) }.
% 0.72/1.11 { h( op1( e11, e10 ) ) = op2( h( e11 ), h( e10 ) ) }.
% 0.72/1.11 { h( op1( e11, e11 ) ) = op2( h( e11 ), h( e11 ) ) }.
% 0.72/1.11 { h( op1( e11, e12 ) ) = op2( h( e11 ), h( e12 ) ) }.
% 0.72/1.11 { h( op1( e11, e13 ) ) = op2( h( e11 ), h( e13 ) ) }.
% 0.72/1.11 { h( op1( e12, e10 ) ) = op2( h( e12 ), h( e10 ) ) }.
% 0.72/1.11 { h( op1( e12, e11 ) ) = op2( h( e12 ), h( e11 ) ) }.
% 0.72/1.11 { h( op1( e12, e12 ) ) = op2( h( e12 ), h( e12 ) ) }.
% 0.72/1.11 { h( op1( e12, e13 ) ) = op2( h( e12 ), h( e13 ) ) }.
% 0.72/1.11 { h( op1( e13, e10 ) ) = op2( h( e13 ), h( e10 ) ) }.
% 0.72/1.11 { h( op1( e13, e11 ) ) = op2( h( e13 ), h( e11 ) ) }.
% 0.72/1.11 { h( op1( e13, e12 ) ) = op2( h( e13 ), h( e12 ) ) }.
% 0.72/1.11 { h( op1( e13, e13 ) ) = op2( h( e13 ), h( e13 ) ) }.
% 0.72/1.11 { j( op2( e20, e20 ) ) = op1( j( e20 ), j( e20 ) ) }.
% 0.72/1.11 { j( op2( e20, e21 ) ) = op1( j( e20 ), j( e21 ) ) }.
% 0.72/1.11 { j( op2( e20, e22 ) ) = op1( j( e20 ), j( e22 ) ) }.
% 0.72/1.11 { j( op2( e20, e23 ) ) = op1( j( e20 ), j( e23 ) ) }.
% 0.72/1.11 { j( op2( e21, e20 ) ) = op1( j( e21 ), j( e20 ) ) }.
% 0.72/1.11 { j( op2( e21, e21 ) ) = op1( j( e21 ), j( e21 ) ) }.
% 0.72/1.11 { j( op2( e21, e22 ) ) = op1( j( e21 ), j( e22 ) ) }.
% 0.72/1.11 { j( op2( e21, e23 ) ) = op1( j( e21 ), j( e23 ) ) }.
% 0.72/1.11 { j( op2( e22, e20 ) ) = op1( j( e22 ), j( e20 ) ) }.
% 0.72/1.11 { j( op2( e22, e21 ) ) = op1( j( e22 ), j( e21 ) ) }.
% 0.72/1.11 { j( op2( e22, e22 ) ) = op1( j( e22 ), j( e22 ) ) }.
% 0.72/1.11 { j( op2( e22, e23 ) ) = op1( j( e22 ), j( e23 ) ) }.
% 0.72/1.11 { j( op2( e23, e20 ) ) = op1( j( e23 ), j( e20 ) ) }.
% 0.72/1.11 { j( op2( e23, e21 ) ) = op1( j( e23 ), j( e21 ) ) }.
% 0.72/1.11 { j( op2( e23, e22 ) ) = op1( j( e23 ), j( e22 ) ) }.
% 0.72/1.11 { j( op2( e23, e23 ) ) = op1( j( e23 ), j( e23 ) ) }.
% 0.72/1.11 { h( j( e20 ) ) = e20 }.
% 0.72/1.11 { h( j( e21 ) ) = e21 }.
% 0.72/1.11 { h( j( e22 ) ) = e22 }.
% 0.72/1.11 { h( j( e23 ) ) = e23 }.
% 0.72/1.11 { j( h( e10 ) ) = e10 }.
% 0.72/1.11 { j( h( e11 ) ) = e11 }.
% 0.72/1.11 { j( h( e12 ) ) = e12 }.
% 0.72/1.11 { j( h( e13 ) ) = e13 }.
% 0.72/1.11
% 0.72/1.11 percentage equality = 1.000000, percentage horn = 0.925926
% 0.72/1.11 This is a pure equality problem
% 0.72/1.11
% 0.72/1.11
% 0.72/1.11
% 0.72/1.11 Options Used:
% 0.72/1.11
% 0.72/1.11 useres = 1
% 0.72/1.11 useparamod = 1
% 0.72/1.11 useeqrefl = 1
% 0.72/1.11 useeqfact = 1
% 0.72/1.11 usefactor = 1
% 0.72/1.11 usesimpsplitting = 0
% 0.72/1.11 usesimpdemod = 5
% 0.72/1.11 usesimpres = 3
% 0.72/1.11
% 0.72/1.11 resimpinuse = 1000
% 0.72/1.11 resimpclauses = 20000
% 0.72/1.11 substype = eqrewr
% 0.72/1.11 backwardsubs = 1
% 0.72/1.11 selectoldest = 5
% 0.72/1.11
% 0.72/1.11 litorderings [0] = split
% 0.72/1.11 litorderings [1] = extend the termordering, first sorting on arguments
% 0.72/1.11
% 0.72/1.11 termordering = kbo
% 0.72/1.11
% 0.72/1.11 litapriori = 0
% 0.72/1.11 termapriori = 1
% 0.72/1.11 litaposteriori = 0
% 0.72/1.11 termaposteriori = 0
% 0.72/1.11 demodaposteriori = 0
% 0.72/1.11 ordereqreflfact = 0
% 0.72/1.11
% 0.72/1.11 litselect = negord
% 0.72/1.11
% 0.72/1.11 maxweight = 15
% 0.72/1.11 maxdepth = 30000
% 0.72/1.11 maxlength = 115
% 0.72/1.11 maxnrvars = 195
% 0.72/1.11 excuselevel = 1
% 0.72/1.11 increasemaxweight = 1
% 0.72/1.11
% 0.72/1.11 maxselected = 10000000
% 0.72/1.11 maxnrclauses = 10000000
% 0.72/1.11
% 0.72/1.11 showgenerated = 0
% 0.72/1.11 showkept = 0
% 0.72/1.11 showselected = 0
% 0.72/1.11 showdeleted = 0
% 0.72/1.11 showresimp = 1
% 0.72/1.11 showstatus = 2000
% 0.72/1.11
% 0.72/1.11 prologoutput = 0
% 0.72/1.11 nrgoals = 5000000
% 0.72/1.11 totalproof = 1
% 0.72/1.11
% 0.72/1.11 Symbols occurring in the translation:
% 0.72/1.11
% 0.72/1.11 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.72/1.11 . [1, 2] (w:1, o:21, a:1, s:1, b:0),
% 0.72/1.11 ! [4, 1] (w:0, o:14, a:1, s:1, b:0),
% 0.72/1.11 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.72/1.11 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.72/1.11 e10 [35, 0] (w:1, o:6, a:1, s:1, b:0),
% 0.72/1.11 e11 [36, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.72/1.11 e12 [37, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.72/1.11 e13 [38, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.72/1.11 e20 [39, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.72/1.11 e21 [40, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.72/1.11 e22 [41, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.72/1.11 e23 [42, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.72/1.11 op1 [43, 2] (w:1, o:45, a:1, s:1, b:0),
% 0.72/1.11 op2 [44, 2] (w:1, o:46, a:1, s:1, b:0),
% 0.72/1.11 h [45, 1] (w:1, o:19, a:1, s:1, b:0),
% 0.72/1.11 j [46, 1] (w:1, o:20, a:1, s:1, b:0).
% 0.72/1.11
% 0.72/1.11
% 0.72/1.11 Starting Search:
% 0.72/1.11
% 0.72/1.11 *** allocated 15000 integers for clauses
% 0.72/1.11
% 0.72/1.11 Bliksems!, er is een bewijs:
% 0.72/1.11 % SZS status Theorem
% 0.72/1.11 % SZS output start Refutation
% 0.72/1.11
% 0.72/1.11 (0) {G0,W3,D2,L1,V0,M1} I { ! e11 ==> e10 }.
% 0.72/1.11 (1) {G0,W3,D2,L1,V0,M1} I { ! e12 ==> e10 }.
% 0.72/1.11 (3) {G0,W3,D2,L1,V0,M1} I { ! e12 ==> e11 }.
% 0.72/1.11 (8) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e20 }.
% 0.72/1.11 (9) {G0,W3,D2,L1,V0,M1} I { ! e22 ==> e21 }.
% 0.72/1.11 (10) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e21 }.
% 0.72/1.11 (11) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e22 }.
% 0.72/1.11 (28) {G0,W5,D3,L1,V0,M1} I { op1( e10, e10 ) ==> e10 }.
% 0.72/1.11 (33) {G0,W5,D3,L1,V0,M1} I { op1( e11, e11 ) ==> e10 }.
% 0.72/1.11 (38) {G0,W5,D3,L1,V0,M1} I { op1( e12, e12 ) ==> e10 }.
% 0.72/1.11 (49) {G0,W5,D3,L1,V0,M1} I { op2( e21, e21 ) ==> e23 }.
% 0.72/1.11 (54) {G0,W5,D3,L1,V0,M1} I { op2( e22, e22 ) ==> e23 }.
% 0.72/1.11 (59) {G0,W5,D3,L1,V0,M1} I { op2( e23, e23 ) ==> e20 }.
% 0.72/1.11 (60) {G0,W16,D3,L4,V0,M4} I { h( e10 ) ==> e20, h( e10 ) ==> e21, h( e10 )
% 0.72/1.11 ==> e22, h( e10 ) ==> e23 }.
% 0.72/1.11 (61) {G0,W16,D3,L4,V0,M4} I { h( e11 ) ==> e20, h( e11 ) ==> e21, h( e11 )
% 0.72/1.11 ==> e22, h( e11 ) ==> e23 }.
% 0.72/1.11 (62) {G0,W16,D3,L4,V0,M4} I { h( e12 ) ==> e20, h( e12 ) ==> e21, h( e12 )
% 0.72/1.11 ==> e22, h( e12 ) ==> e23 }.
% 0.72/1.11 (68) {G1,W8,D4,L1,V0,M1} I;d(28) { op2( h( e10 ), h( e10 ) ) ==> h( e10 )
% 0.72/1.11 }.
% 0.72/1.11 (73) {G1,W8,D4,L1,V0,M1} I;d(33) { op2( h( e11 ), h( e11 ) ) ==> h( e10 )
% 0.72/1.11 }.
% 0.72/1.11 (78) {G1,W8,D4,L1,V0,M1} I;d(38) { op2( h( e12 ), h( e12 ) ) ==> h( e10 )
% 0.72/1.11 }.
% 0.72/1.11 (104) {G0,W5,D4,L1,V0,M1} I { j( h( e10 ) ) ==> e10 }.
% 0.72/1.11 (105) {G0,W5,D4,L1,V0,M1} I { j( h( e11 ) ) ==> e11 }.
% 0.72/1.11 (106) {G0,W5,D4,L1,V0,M1} I { j( h( e12 ) ) ==> e12 }.
% 0.72/1.11 (116) {G1,W16,D3,L4,V0,M4} P(62,106) { j( e20 ) ==> e12, h( e12 ) ==> e21,
% 0.72/1.11 h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 0.72/1.11 (143) {G2,W12,D3,L3,V0,M3} P(60,68);d(49);r(10) { h( e10 ) ==> e20, h( e10
% 0.72/1.11 ) ==> e22, h( e10 ) ==> e23 }.
% 0.72/1.11 (145) {G3,W11,D3,L3,V0,M3} P(60,68);d(59);d(143);r(10) { h( e10 ) ==> e20,
% 0.72/1.11 h( e10 ) ==> e22, e23 ==> e20 }.
% 0.72/1.11 (146) {G4,W8,D3,L2,V0,M2} E(143);d(145);q { h( e10 ) ==> e20, h( e10 ) ==>
% 0.72/1.11 e22 }.
% 0.72/1.11 (147) {G5,W4,D3,L1,V0,M1} P(146,68);d(54);r(11) { h( e10 ) ==> e20 }.
% 0.72/1.11 (153) {G6,W4,D3,L1,V0,M1} P(147,104) { j( e20 ) ==> e10 }.
% 0.72/1.11 (164) {G6,W7,D4,L1,V0,M1} S(73);d(147) { op2( h( e11 ), h( e11 ) ) ==> e20
% 0.72/1.11 }.
% 0.72/1.11 (165) {G7,W12,D3,L3,V0,M3} P(61,164);d(49);r(8) { h( e11 ) ==> e20, h( e11
% 0.72/1.11 ) ==> e22, h( e11 ) ==> e23 }.
% 0.72/1.11 (166) {G8,W11,D3,L3,V0,M3} P(61,164);d(54);d(165);r(8) { h( e11 ) ==> e20,
% 0.72/1.11 h( e11 ) ==> e23, e22 ==> e21 }.
% 0.72/1.11 (167) {G9,W8,D3,L2,V0,M2} S(166);r(9) { h( e11 ) ==> e20, h( e11 ) ==> e23
% 0.72/1.11 }.
% 0.72/1.11 (173) {G10,W7,D3,L2,V0,M2} P(167,105);d(153) { h( e11 ) ==> e23, e11 ==>
% 0.72/1.11 e10 }.
% 0.72/1.11 (175) {G11,W4,D3,L1,V0,M1} S(173);r(0) { h( e11 ) ==> e23 }.
% 0.72/1.11 (180) {G12,W4,D3,L1,V0,M1} P(175,105) { j( e23 ) ==> e11 }.
% 0.72/1.11 (185) {G7,W15,D3,L4,V0,M4} S(116);d(153) { h( e12 ) ==> e21, h( e12 ) ==>
% 0.72/1.11 e22, h( e12 ) ==> e23, e12 ==> e10 }.
% 0.72/1.11 (186) {G8,W12,D3,L3,V0,M3} S(185);r(1) { h( e12 ) ==> e21, h( e12 ) ==> e22
% 0.72/1.11 , h( e12 ) ==> e23 }.
% 0.72/1.11 (190) {G9,W8,D3,L2,V0,M2} P(186,78);d(49);d(147);r(8) { h( e12 ) ==> e22, h
% 0.72/1.11 ( e12 ) ==> e23 }.
% 0.72/1.11 (191) {G10,W7,D3,L2,V0,M2} P(186,78);d(54);d(190);d(147);r(9) { h( e12 )
% 0.72/1.11 ==> e23, e23 ==> e20 }.
% 0.72/1.11 (194) {G11,W4,D3,L1,V0,M1} S(191);r(8) { h( e12 ) ==> e23 }.
% 0.72/1.11 (196) {G13,W3,D2,L1,V0,M1} P(194,106);d(180) { e12 ==> e11 }.
% 0.72/1.11 (197) {G14,W0,D0,L0,V0,M0} S(196);r(3) { }.
% 0.72/1.11
% 0.72/1.11
% 0.72/1.11 % SZS output end Refutation
% 0.72/1.11 found a proof!
% 0.72/1.11
% 0.72/1.11
% 0.72/1.11 Unprocessed initial clauses:
% 0.72/1.11
% 0.72/1.11 (199) {G0,W3,D2,L1,V0,M1} { ! e10 = e11 }.
% 0.72/1.11 (200) {G0,W3,D2,L1,V0,M1} { ! e10 = e12 }.
% 0.72/1.11 (201) {G0,W3,D2,L1,V0,M1} { ! e10 = e13 }.
% 0.72/1.11 (202) {G0,W3,D2,L1,V0,M1} { ! e11 = e12 }.
% 0.72/1.11 (203) {G0,W3,D2,L1,V0,M1} { ! e11 = e13 }.
% 0.72/1.11 (204) {G0,W3,D2,L1,V0,M1} { ! e12 = e13 }.
% 0.72/1.11 (205) {G0,W3,D2,L1,V0,M1} { ! e20 = e21 }.
% 0.72/1.11 (206) {G0,W3,D2,L1,V0,M1} { ! e20 = e22 }.
% 0.72/1.11 (207) {G0,W3,D2,L1,V0,M1} { ! e20 = e23 }.
% 0.72/1.11 (208) {G0,W3,D2,L1,V0,M1} { ! e21 = e22 }.
% 0.72/1.11 (209) {G0,W3,D2,L1,V0,M1} { ! e21 = e23 }.
% 0.72/1.11 (210) {G0,W3,D2,L1,V0,M1} { ! e22 = e23 }.
% 0.72/1.11 (211) {G0,W3,D2,L1,V0,M1} { ! e10 = e20 }.
% 0.72/1.11 (212) {G0,W3,D2,L1,V0,M1} { ! e10 = e21 }.
% 0.72/1.11 (213) {G0,W3,D2,L1,V0,M1} { ! e10 = e22 }.
% 0.72/1.11 (214) {G0,W3,D2,L1,V0,M1} { ! e10 = e23 }.
% 0.72/1.11 (215) {G0,W3,D2,L1,V0,M1} { ! e11 = e20 }.
% 0.72/1.11 (216) {G0,W3,D2,L1,V0,M1} { ! e11 = e21 }.
% 0.72/1.11 (217) {G0,W3,D2,L1,V0,M1} { ! e11 = e22 }.
% 0.72/1.11 (218) {G0,W3,D2,L1,V0,M1} { ! e11 = e23 }.
% 0.72/1.11 (219) {G0,W3,D2,L1,V0,M1} { ! e12 = e20 }.
% 0.72/1.11 (220) {G0,W3,D2,L1,V0,M1} { ! e12 = e21 }.
% 0.72/1.11 (221) {G0,W3,D2,L1,V0,M1} { ! e12 = e22 }.
% 0.72/1.11 (222) {G0,W3,D2,L1,V0,M1} { ! e12 = e23 }.
% 0.72/1.11 (223) {G0,W3,D2,L1,V0,M1} { ! e13 = e20 }.
% 0.72/1.11 (224) {G0,W3,D2,L1,V0,M1} { ! e13 = e21 }.
% 0.72/1.11 (225) {G0,W3,D2,L1,V0,M1} { ! e13 = e22 }.
% 0.72/1.11 (226) {G0,W3,D2,L1,V0,M1} { ! e13 = e23 }.
% 0.72/1.11 (227) {G0,W5,D3,L1,V0,M1} { op1( e10, e10 ) = e10 }.
% 0.72/1.11 (228) {G0,W5,D3,L1,V0,M1} { op1( e10, e11 ) = e11 }.
% 0.72/1.11 (229) {G0,W5,D3,L1,V0,M1} { op1( e10, e12 ) = e12 }.
% 0.72/1.11 (230) {G0,W5,D3,L1,V0,M1} { op1( e10, e13 ) = e13 }.
% 0.72/1.11 (231) {G0,W5,D3,L1,V0,M1} { op1( e11, e10 ) = e11 }.
% 0.72/1.11 (232) {G0,W5,D3,L1,V0,M1} { op1( e11, e11 ) = e10 }.
% 0.72/1.11 (233) {G0,W5,D3,L1,V0,M1} { op1( e11, e12 ) = e13 }.
% 0.72/1.11 (234) {G0,W5,D3,L1,V0,M1} { op1( e11, e13 ) = e12 }.
% 0.72/1.11 (235) {G0,W5,D3,L1,V0,M1} { op1( e12, e10 ) = e12 }.
% 0.72/1.11 (236) {G0,W5,D3,L1,V0,M1} { op1( e12, e11 ) = e13 }.
% 0.72/1.11 (237) {G0,W5,D3,L1,V0,M1} { op1( e12, e12 ) = e10 }.
% 0.72/1.11 (238) {G0,W5,D3,L1,V0,M1} { op1( e12, e13 ) = e11 }.
% 0.72/1.11 (239) {G0,W5,D3,L1,V0,M1} { op1( e13, e10 ) = e13 }.
% 0.72/1.11 (240) {G0,W5,D3,L1,V0,M1} { op1( e13, e11 ) = e12 }.
% 0.72/1.11 (241) {G0,W5,D3,L1,V0,M1} { op1( e13, e12 ) = e11 }.
% 0.72/1.11 (242) {G0,W5,D3,L1,V0,M1} { op1( e13, e13 ) = e10 }.
% 0.72/1.11 (243) {G0,W5,D3,L1,V0,M1} { op2( e20, e20 ) = e20 }.
% 0.72/1.11 (244) {G0,W5,D3,L1,V0,M1} { op2( e20, e21 ) = e21 }.
% 0.72/1.11 (245) {G0,W5,D3,L1,V0,M1} { op2( e20, e22 ) = e22 }.
% 0.72/1.11 (246) {G0,W5,D3,L1,V0,M1} { op2( e20, e23 ) = e23 }.
% 0.72/1.11 (247) {G0,W5,D3,L1,V0,M1} { op2( e21, e20 ) = e21 }.
% 0.72/1.11 (248) {G0,W5,D3,L1,V0,M1} { op2( e21, e21 ) = e23 }.
% 0.72/1.11 (249) {G0,W5,D3,L1,V0,M1} { op2( e21, e22 ) = e20 }.
% 0.72/1.11 (250) {G0,W5,D3,L1,V0,M1} { op2( e21, e23 ) = e22 }.
% 0.72/1.11 (251) {G0,W5,D3,L1,V0,M1} { op2( e22, e20 ) = e22 }.
% 0.72/1.11 (252) {G0,W5,D3,L1,V0,M1} { op2( e22, e21 ) = e20 }.
% 0.72/1.11 (253) {G0,W5,D3,L1,V0,M1} { op2( e22, e22 ) = e23 }.
% 0.72/1.11 (254) {G0,W5,D3,L1,V0,M1} { op2( e22, e23 ) = e21 }.
% 0.72/1.11 (255) {G0,W5,D3,L1,V0,M1} { op2( e23, e20 ) = e23 }.
% 0.72/1.11 (256) {G0,W5,D3,L1,V0,M1} { op2( e23, e21 ) = e22 }.
% 0.72/1.11 (257) {G0,W5,D3,L1,V0,M1} { op2( e23, e22 ) = e21 }.
% 0.72/1.11 (258) {G0,W5,D3,L1,V0,M1} { op2( e23, e23 ) = e20 }.
% 0.72/1.11 (259) {G0,W16,D3,L4,V0,M4} { h( e10 ) = e20, h( e10 ) = e21, h( e10 ) =
% 0.72/1.11 e22, h( e10 ) = e23 }.
% 0.72/1.11 (260) {G0,W16,D3,L4,V0,M4} { h( e11 ) = e20, h( e11 ) = e21, h( e11 ) =
% 0.72/1.11 e22, h( e11 ) = e23 }.
% 0.72/1.11 (261) {G0,W16,D3,L4,V0,M4} { h( e12 ) = e20, h( e12 ) = e21, h( e12 ) =
% 0.72/1.11 e22, h( e12 ) = e23 }.
% 0.72/1.11 (262) {G0,W16,D3,L4,V0,M4} { h( e13 ) = e20, h( e13 ) = e21, h( e13 ) =
% 0.72/1.11 e22, h( e13 ) = e23 }.
% 0.72/1.11 (263) {G0,W16,D3,L4,V0,M4} { j( e20 ) = e10, j( e20 ) = e11, j( e20 ) =
% 0.72/1.11 e12, j( e20 ) = e13 }.
% 0.72/1.11 (264) {G0,W16,D3,L4,V0,M4} { j( e21 ) = e10, j( e21 ) = e11, j( e21 ) =
% 0.72/1.11 e12, j( e21 ) = e13 }.
% 0.72/1.11 (265) {G0,W16,D3,L4,V0,M4} { j( e22 ) = e10, j( e22 ) = e11, j( e22 ) =
% 0.72/1.11 e12, j( e22 ) = e13 }.
% 0.72/1.11 (266) {G0,W16,D3,L4,V0,M4} { j( e23 ) = e10, j( e23 ) = e11, j( e23 ) =
% 0.72/1.11 e12, j( e23 ) = e13 }.
% 0.72/1.11 (267) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e10 ) ) = op2( h( e10 ), h( e10
% 0.72/1.11 ) ) }.
% 0.72/1.11 (268) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e11 ) ) = op2( h( e10 ), h( e11
% 0.72/1.11 ) ) }.
% 0.72/1.11 (269) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e12 ) ) = op2( h( e10 ), h( e12
% 0.72/1.11 ) ) }.
% 0.72/1.11 (270) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e13 ) ) = op2( h( e10 ), h( e13
% 0.72/1.11 ) ) }.
% 0.72/1.11 (271) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e10 ) ) = op2( h( e11 ), h( e10
% 0.72/1.11 ) ) }.
% 0.72/1.11 (272) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e11 ) ) = op2( h( e11 ), h( e11
% 0.72/1.11 ) ) }.
% 0.72/1.11 (273) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e12 ) ) = op2( h( e11 ), h( e12
% 0.72/1.11 ) ) }.
% 0.72/1.11 (274) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e13 ) ) = op2( h( e11 ), h( e13
% 0.72/1.11 ) ) }.
% 0.72/1.11 (275) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e10 ) ) = op2( h( e12 ), h( e10
% 0.72/1.11 ) ) }.
% 0.72/1.11 (276) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e11 ) ) = op2( h( e12 ), h( e11
% 0.72/1.11 ) ) }.
% 0.72/1.11 (277) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e12 ) ) = op2( h( e12 ), h( e12
% 0.72/1.11 ) ) }.
% 0.72/1.11 (278) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e13 ) ) = op2( h( e12 ), h( e13
% 0.72/1.11 ) ) }.
% 0.72/1.11 (279) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e10 ) ) = op2( h( e13 ), h( e10
% 0.72/1.11 ) ) }.
% 0.72/1.11 (280) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e11 ) ) = op2( h( e13 ), h( e11
% 0.72/1.11 ) ) }.
% 0.72/1.11 (281) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e12 ) ) = op2( h( e13 ), h( e12
% 0.72/1.11 ) ) }.
% 0.72/1.11 (282) {G0,W10,D4,L1,V0,M1} { h( op1( e13, e13 ) ) = op2( h( e13 ), h( e13
% 0.72/1.11 ) ) }.
% 0.72/1.11 (283) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e20 ) ) = op1( j( e20 ), j( e20
% 0.72/1.11 ) ) }.
% 0.72/1.11 (284) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e21 ) ) = op1( j( e20 ), j( e21
% 0.72/1.11 ) ) }.
% 0.72/1.11 (285) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e22 ) ) = op1( j( e20 ), j( e22
% 0.72/1.11 ) ) }.
% 0.72/1.11 (286) {G0,W10,D4,L1,V0,M1} { j( op2( e20, e23 ) ) = op1( j( e20 ), j( e23
% 0.72/1.11 ) ) }.
% 0.72/1.11 (287) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e20 ) ) = op1( j( e21 ), j( e20
% 0.72/1.11 ) ) }.
% 0.72/1.11 (288) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e21 ) ) = op1( j( e21 ), j( e21
% 0.72/1.11 ) ) }.
% 0.72/1.11 (289) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e22 ) ) = op1( j( e21 ), j( e22
% 0.72/1.11 ) ) }.
% 0.72/1.11 (290) {G0,W10,D4,L1,V0,M1} { j( op2( e21, e23 ) ) = op1( j( e21 ), j( e23
% 0.72/1.11 ) ) }.
% 0.72/1.11 (291) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e20 ) ) = op1( j( e22 ), j( e20
% 0.72/1.11 ) ) }.
% 0.72/1.11 (292) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e21 ) ) = op1( j( e22 ), j( e21
% 0.72/1.11 ) ) }.
% 0.72/1.11 (293) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e22 ) ) = op1( j( e22 ), j( e22
% 0.72/1.11 ) ) }.
% 0.72/1.11 (294) {G0,W10,D4,L1,V0,M1} { j( op2( e22, e23 ) ) = op1( j( e22 ), j( e23
% 0.72/1.11 ) ) }.
% 0.72/1.11 (295) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e20 ) ) = op1( j( e23 ), j( e20
% 0.72/1.11 ) ) }.
% 0.72/1.11 (296) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e21 ) ) = op1( j( e23 ), j( e21
% 0.72/1.11 ) ) }.
% 0.72/1.11 (297) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e22 ) ) = op1( j( e23 ), j( e22
% 0.72/1.11 ) ) }.
% 0.72/1.11 (298) {G0,W10,D4,L1,V0,M1} { j( op2( e23, e23 ) ) = op1( j( e23 ), j( e23
% 0.72/1.11 ) ) }.
% 0.72/1.11 (299) {G0,W5,D4,L1,V0,M1} { h( j( e20 ) ) = e20 }.
% 0.72/1.11 (300) {G0,W5,D4,L1,V0,M1} { h( j( e21 ) ) = e21 }.
% 0.72/1.11 (301) {G0,W5,D4,L1,V0,M1} { h( j( e22 ) ) = e22 }.
% 0.72/1.11 (302) {G0,W5,D4,L1,V0,M1} { h( j( e23 ) ) = e23 }.
% 0.72/1.11 (303) {G0,W5,D4,L1,V0,M1} { j( h( e10 ) ) = e10 }.
% 0.72/1.11 (304) {G0,W5,D4,L1,V0,M1} { j( h( e11 ) ) = e11 }.
% 0.72/1.11 (305) {G0,W5,D4,L1,V0,M1} { j( h( e12 ) ) = e12 }.
% 0.72/1.11 (306) {G0,W5,D4,L1,V0,M1} { j( h( e13 ) ) = e13 }.
% 0.72/1.11
% 0.72/1.11
% 0.72/1.11 Total Proof:
% 0.72/1.11
% 0.72/1.11 eqswap: (307) {G0,W3,D2,L1,V0,M1} { ! e11 = e10 }.
% 0.72/1.11 parent0[0]: (199) {G0,W3,D2,L1,V0,M1} { ! e10 = e11 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 subsumption: (0) {G0,W3,D2,L1,V0,M1} I { ! e11 ==> e10 }.
% 0.72/1.11 parent0: (307) {G0,W3,D2,L1,V0,M1} { ! e11 = e10 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11 permutation0:
% 0.72/1.11 0 ==> 0
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 eqswap: (309) {G0,W3,D2,L1,V0,M1} { ! e12 = e10 }.
% 0.72/1.11 parent0[0]: (200) {G0,W3,D2,L1,V0,M1} { ! e10 = e12 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 subsumption: (1) {G0,W3,D2,L1,V0,M1} I { ! e12 ==> e10 }.
% 0.72/1.11 parent0: (309) {G0,W3,D2,L1,V0,M1} { ! e12 = e10 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11 permutation0:
% 0.72/1.11 0 ==> 0
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 eqswap: (313) {G0,W3,D2,L1,V0,M1} { ! e12 = e11 }.
% 0.72/1.11 parent0[0]: (202) {G0,W3,D2,L1,V0,M1} { ! e11 = e12 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 subsumption: (3) {G0,W3,D2,L1,V0,M1} I { ! e12 ==> e11 }.
% 0.72/1.11 parent0: (313) {G0,W3,D2,L1,V0,M1} { ! e12 = e11 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11 permutation0:
% 0.72/1.11 0 ==> 0
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 eqswap: (322) {G0,W3,D2,L1,V0,M1} { ! e23 = e20 }.
% 0.72/1.11 parent0[0]: (207) {G0,W3,D2,L1,V0,M1} { ! e20 = e23 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 subsumption: (8) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e20 }.
% 0.72/1.11 parent0: (322) {G0,W3,D2,L1,V0,M1} { ! e23 = e20 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11 permutation0:
% 0.72/1.11 0 ==> 0
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 eqswap: (332) {G0,W3,D2,L1,V0,M1} { ! e22 = e21 }.
% 0.72/1.11 parent0[0]: (208) {G0,W3,D2,L1,V0,M1} { ! e21 = e22 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 subsumption: (9) {G0,W3,D2,L1,V0,M1} I { ! e22 ==> e21 }.
% 0.72/1.11 parent0: (332) {G0,W3,D2,L1,V0,M1} { ! e22 = e21 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11 permutation0:
% 0.72/1.11 0 ==> 0
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 eqswap: (343) {G0,W3,D2,L1,V0,M1} { ! e23 = e21 }.
% 0.72/1.11 parent0[0]: (209) {G0,W3,D2,L1,V0,M1} { ! e21 = e23 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 subsumption: (10) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e21 }.
% 0.72/1.11 parent0: (343) {G0,W3,D2,L1,V0,M1} { ! e23 = e21 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11 permutation0:
% 0.72/1.11 0 ==> 0
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 eqswap: (355) {G0,W3,D2,L1,V0,M1} { ! e23 = e22 }.
% 0.72/1.11 parent0[0]: (210) {G0,W3,D2,L1,V0,M1} { ! e22 = e23 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 subsumption: (11) {G0,W3,D2,L1,V0,M1} I { ! e23 ==> e22 }.
% 0.72/1.11 parent0: (355) {G0,W3,D2,L1,V0,M1} { ! e23 = e22 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11 permutation0:
% 0.72/1.11 0 ==> 0
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 *** allocated 22500 integers for clauses
% 0.72/1.11 subsumption: (28) {G0,W5,D3,L1,V0,M1} I { op1( e10, e10 ) ==> e10 }.
% 0.72/1.11 parent0: (227) {G0,W5,D3,L1,V0,M1} { op1( e10, e10 ) = e10 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11 permutation0:
% 0.72/1.11 0 ==> 0
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 subsumption: (33) {G0,W5,D3,L1,V0,M1} I { op1( e11, e11 ) ==> e10 }.
% 0.72/1.11 parent0: (232) {G0,W5,D3,L1,V0,M1} { op1( e11, e11 ) = e10 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11 permutation0:
% 0.72/1.11 0 ==> 0
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 subsumption: (38) {G0,W5,D3,L1,V0,M1} I { op1( e12, e12 ) ==> e10 }.
% 0.72/1.11 parent0: (237) {G0,W5,D3,L1,V0,M1} { op1( e12, e12 ) = e10 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11 permutation0:
% 0.72/1.11 0 ==> 0
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 subsumption: (49) {G0,W5,D3,L1,V0,M1} I { op2( e21, e21 ) ==> e23 }.
% 0.72/1.11 parent0: (248) {G0,W5,D3,L1,V0,M1} { op2( e21, e21 ) = e23 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11 permutation0:
% 0.72/1.11 0 ==> 0
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 subsumption: (54) {G0,W5,D3,L1,V0,M1} I { op2( e22, e22 ) ==> e23 }.
% 0.72/1.11 parent0: (253) {G0,W5,D3,L1,V0,M1} { op2( e22, e22 ) = e23 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11 permutation0:
% 0.72/1.11 0 ==> 0
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 subsumption: (59) {G0,W5,D3,L1,V0,M1} I { op2( e23, e23 ) ==> e20 }.
% 0.72/1.11 parent0: (258) {G0,W5,D3,L1,V0,M1} { op2( e23, e23 ) = e20 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11 permutation0:
% 0.72/1.11 0 ==> 0
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 subsumption: (60) {G0,W16,D3,L4,V0,M4} I { h( e10 ) ==> e20, h( e10 ) ==>
% 0.72/1.11 e21, h( e10 ) ==> e22, h( e10 ) ==> e23 }.
% 0.72/1.11 parent0: (259) {G0,W16,D3,L4,V0,M4} { h( e10 ) = e20, h( e10 ) = e21, h(
% 0.72/1.11 e10 ) = e22, h( e10 ) = e23 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11 permutation0:
% 0.72/1.11 0 ==> 0
% 0.72/1.11 1 ==> 1
% 0.72/1.11 2 ==> 2
% 0.72/1.11 3 ==> 3
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 *** allocated 33750 integers for clauses
% 0.72/1.11 subsumption: (61) {G0,W16,D3,L4,V0,M4} I { h( e11 ) ==> e20, h( e11 ) ==>
% 0.72/1.11 e21, h( e11 ) ==> e22, h( e11 ) ==> e23 }.
% 0.72/1.11 parent0: (260) {G0,W16,D3,L4,V0,M4} { h( e11 ) = e20, h( e11 ) = e21, h(
% 0.72/1.11 e11 ) = e22, h( e11 ) = e23 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11 permutation0:
% 0.72/1.11 0 ==> 0
% 0.72/1.11 1 ==> 1
% 0.72/1.11 2 ==> 2
% 0.72/1.11 3 ==> 3
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 subsumption: (62) {G0,W16,D3,L4,V0,M4} I { h( e12 ) ==> e20, h( e12 ) ==>
% 0.72/1.11 e21, h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 0.72/1.11 parent0: (261) {G0,W16,D3,L4,V0,M4} { h( e12 ) = e20, h( e12 ) = e21, h(
% 0.72/1.11 e12 ) = e22, h( e12 ) = e23 }.
% 0.72/1.11 substitution0:
% 0.72/1.11 end
% 0.72/1.11 permutation0:
% 0.72/1.11 0 ==> 0
% 0.72/1.11 1 ==> 1
% 0.72/1.11 2 ==> 2
% 0.72/1.11 3 ==> 3
% 0.72/1.11 end
% 0.72/1.11
% 0.72/1.11 *** allocated 15000 integers for termspace/termends
% 0.72/1.11 paramod: (1145) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e10 ), h( e10 ) )
% 0.72/1.11 }.
% 0.72/1.11 parent0[0]: (28) {G0,W5,D3,L1,V0,M1} I { op1( e10, e10 ) ==> e10 }.
% 0.72/1.11 parent1[0; 2]: (267) {G0,W10,D4,L1,V0,M1} { h( op1( e10, e10 ) ) = op2( h
% 1.27/1.65 ( e10 ), h( e10 ) ) }.
% 1.27/1.65 substitution0:
% 1.27/1.65 end
% 1.27/1.65 substitution1:
% 1.27/1.65 end
% 1.27/1.65
% 1.27/1.65 eqswap: (1146) {G1,W8,D4,L1,V0,M1} { op2( h( e10 ), h( e10 ) ) = h( e10 )
% 1.27/1.65 }.
% 1.27/1.65 parent0[0]: (1145) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e10 ), h( e10
% 1.27/1.65 ) ) }.
% 1.27/1.65 substitution0:
% 1.27/1.65 end
% 1.27/1.65
% 1.27/1.65 subsumption: (68) {G1,W8,D4,L1,V0,M1} I;d(28) { op2( h( e10 ), h( e10 ) )
% 1.27/1.65 ==> h( e10 ) }.
% 1.27/1.65 parent0: (1146) {G1,W8,D4,L1,V0,M1} { op2( h( e10 ), h( e10 ) ) = h( e10 )
% 1.27/1.65 }.
% 1.27/1.65 substitution0:
% 1.27/1.65 end
% 1.27/1.65 permutation0:
% 1.27/1.65 0 ==> 0
% 1.27/1.65 end
% 1.27/1.65
% 1.27/1.65 *** allocated 50625 integers for clauses
% 1.27/1.65 paramod: (1409) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e11 ), h( e11 ) )
% 1.27/1.65 }.
% 1.27/1.65 parent0[0]: (33) {G0,W5,D3,L1,V0,M1} I { op1( e11, e11 ) ==> e10 }.
% 1.27/1.65 parent1[0; 2]: (272) {G0,W10,D4,L1,V0,M1} { h( op1( e11, e11 ) ) = op2( h
% 1.27/1.65 ( e11 ), h( e11 ) ) }.
% 1.27/1.65 substitution0:
% 1.27/1.65 end
% 1.27/1.65 substitution1:
% 1.27/1.65 end
% 1.27/1.65
% 1.27/1.65 eqswap: (1410) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e11 ) ) = h( e10 )
% 1.27/1.65 }.
% 1.27/1.65 parent0[0]: (1409) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e11 ), h( e11
% 1.27/1.65 ) ) }.
% 1.27/1.65 substitution0:
% 1.27/1.65 end
% 1.27/1.65
% 1.27/1.65 subsumption: (73) {G1,W8,D4,L1,V0,M1} I;d(33) { op2( h( e11 ), h( e11 ) )
% 1.27/1.65 ==> h( e10 ) }.
% 1.27/1.65 parent0: (1410) {G1,W8,D4,L1,V0,M1} { op2( h( e11 ), h( e11 ) ) = h( e10 )
% 1.27/1.65 }.
% 1.27/1.65 substitution0:
% 1.27/1.65 end
% 1.27/1.65 permutation0:
% 1.27/1.65 0 ==> 0
% 1.27/1.65 end
% 1.27/1.65
% 1.27/1.65 *** allocated 22500 integers for termspace/termends
% 1.27/1.65 paramod: (1683) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e12 ), h( e12 ) )
% 1.27/1.65 }.
% 1.27/1.65 parent0[0]: (38) {G0,W5,D3,L1,V0,M1} I { op1( e12, e12 ) ==> e10 }.
% 1.27/1.65 parent1[0; 2]: (277) {G0,W10,D4,L1,V0,M1} { h( op1( e12, e12 ) ) = op2( h
% 1.27/1.65 ( e12 ), h( e12 ) ) }.
% 1.27/1.65 substitution0:
% 1.27/1.65 end
% 1.27/1.65 substitution1:
% 1.27/1.65 end
% 1.27/1.65
% 1.27/1.65 eqswap: (1684) {G1,W8,D4,L1,V0,M1} { op2( h( e12 ), h( e12 ) ) = h( e10 )
% 1.27/1.65 }.
% 1.27/1.65 parent0[0]: (1683) {G1,W8,D4,L1,V0,M1} { h( e10 ) = op2( h( e12 ), h( e12
% 1.27/1.65 ) ) }.
% 1.27/1.65 substitution0:
% 1.27/1.65 end
% 1.27/1.65
% 1.27/1.65 subsumption: (78) {G1,W8,D4,L1,V0,M1} I;d(38) { op2( h( e12 ), h( e12 ) )
% 1.27/1.65 ==> h( e10 ) }.
% 1.27/1.65 parent0: (1684) {G1,W8,D4,L1,V0,M1} { op2( h( e12 ), h( e12 ) ) = h( e10 )
% 1.27/1.65 }.
% 1.27/1.65 substitution0:
% 1.27/1.65 end
% 1.27/1.65 permutation0:
% 1.27/1.65 0 ==> 0
% 1.27/1.65 end
% 1.27/1.65
% 1.27/1.65 subsumption: (104) {G0,W5,D4,L1,V0,M1} I { j( h( e10 ) ) ==> e10 }.
% 1.27/1.65 parent0: (303) {G0,W5,D4,L1,V0,M1} { j( h( e10 ) ) = e10 }.
% 1.27/1.65 substitution0:
% 1.27/1.65 end
% 1.27/1.65 permutation0:
% 1.27/1.65 0 ==> 0
% 1.27/1.65 end
% 1.27/1.65
% 1.27/1.65 *** allocated 75937 integers for clauses
% 1.27/1.65 subsumption: (105) {G0,W5,D4,L1,V0,M1} I { j( h( e11 ) ) ==> e11 }.
% 1.27/1.65 parent0: (304) {G0,W5,D4,L1,V0,M1} { j( h( e11 ) ) = e11 }.
% 1.27/1.65 substitution0:
% 1.27/1.65 end
% 1.27/1.65 permutation0:
% 1.27/1.65 0 ==> 0
% 1.27/1.65 end
% 1.27/1.65
% 1.27/1.65 *** allocated 33750 integers for termspace/termends
% 1.27/1.65 subsumption: (106) {G0,W5,D4,L1,V0,M1} I { j( h( e12 ) ) ==> e12 }.
% 1.27/1.65 parent0: (305) {G0,W5,D4,L1,V0,M1} { j( h( e12 ) ) = e12 }.
% 1.27/1.65 substitution0:
% 1.27/1.65 end
% 1.27/1.65 permutation0:
% 1.27/1.65 0 ==> 0
% 1.27/1.65 end
% 1.27/1.65
% 1.27/1.65 *** allocated 50625 integers for termspace/termends
% 1.27/1.65 *** allocated 75937 integers for termspace/termends
% 1.27/1.65 *** allocated 113905 integers for clauses
% 1.27/1.65 *** allocated 113905 integers for termspace/termends
% 1.27/1.65 eqswap: (2340) {G0,W16,D3,L4,V0,M4} { e21 ==> h( e12 ), h( e12 ) ==> e20,
% 1.27/1.65 h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 1.27/1.65 parent0[1]: (62) {G0,W16,D3,L4,V0,M4} I { h( e12 ) ==> e20, h( e12 ) ==>
% 1.27/1.65 e21, h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 1.27/1.65 substitution0:
% 1.27/1.65 end
% 1.27/1.65
% 1.27/1.65 eqswap: (2354) {G0,W5,D4,L1,V0,M1} { e12 ==> j( h( e12 ) ) }.
% 1.27/1.65 parent0[0]: (106) {G0,W5,D4,L1,V0,M1} I { j( h( e12 ) ) ==> e12 }.
% 1.27/1.65 substitution0:
% 1.27/1.65 end
% 1.27/1.65
% 1.27/1.65 paramod: (4831) {G1,W16,D3,L4,V0,M4} { e12 ==> j( e20 ), e21 ==> h( e12 )
% 1.27/1.65 , h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 1.27/1.65 parent0[1]: (2340) {G0,W16,D3,L4,V0,M4} { e21 ==> h( e12 ), h( e12 ) ==>
% 1.27/1.65 e20, h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 1.27/1.65 parent1[0; 3]: (2354) {G0,W5,D4,L1,V0,M1} { e12 ==> j( h( e12 ) ) }.
% 1.27/1.65 substitution0:
% 1.27/1.65 end
% 1.27/1.65 substitution1:
% 1.27/1.65 end
% 1.27/1.65
% 1.27/1.65 eqswap: (4900) {G1,W16,D3,L4,V0,M4} { e23 ==> h( e12 ), e12 ==> j( e20 ),
% 1.27/1.65 e21 ==> h( e12 ), h( e12 ) ==> e22 }.
% 1.27/1.65 parent0[3]: (4831) {G1,W16,D3,L4,V0,M4} { e12 ==> j( e20 ), e21 ==> h( e12
% 1.27/1.65 ), h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 1.27/1.65 substitution0:
% 1.27/1.65 end
% 1.27/1.65
% 1.27/1.65 eqswap: (4903) {G1,W16,D3,L4,V0,M4} { e22 ==> h( e12 ), e23 ==> h( e12 ),
% 1.27/1.65 e12 ==> j( e20 ), e21 ==> h( e12 ) }.
% 1.27/1.65 parent0[3]: (4900) {G1,W16,D3,L4,V0,M4} { e23 ==> h( e12 ), e12 ==> j( e20
% 1.27/1.65 ), e21 ==> h( e12 ), h( e12 ) ==> e22 }.
% 1.27/1.65 substitution0:
% 1.49/1.85 end
% 1.49/1.85
% 1.49/1.85 eqswap: (4905) {G1,W16,D3,L4,V0,M4} { h( e12 ) ==> e21, e22 ==> h( e12 ),
% 1.49/1.85 e23 ==> h( e12 ), e12 ==> j( e20 ) }.
% 1.49/1.85 parent0[3]: (4903) {G1,W16,D3,L4,V0,M4} { e22 ==> h( e12 ), e23 ==> h( e12
% 1.49/1.85 ), e12 ==> j( e20 ), e21 ==> h( e12 ) }.
% 1.49/1.85 substitution0:
% 1.49/1.85 end
% 1.49/1.85
% 1.49/1.85 eqswap: (4907) {G1,W16,D3,L4,V0,M4} { j( e20 ) ==> e12, h( e12 ) ==> e21,
% 1.49/1.85 e22 ==> h( e12 ), e23 ==> h( e12 ) }.
% 1.49/1.85 parent0[3]: (4905) {G1,W16,D3,L4,V0,M4} { h( e12 ) ==> e21, e22 ==> h( e12
% 1.49/1.85 ), e23 ==> h( e12 ), e12 ==> j( e20 ) }.
% 1.49/1.85 substitution0:
% 1.49/1.85 end
% 1.49/1.85
% 1.49/1.85 eqswap: (4909) {G1,W16,D3,L4,V0,M4} { h( e12 ) ==> e23, j( e20 ) ==> e12,
% 1.49/1.85 h( e12 ) ==> e21, e22 ==> h( e12 ) }.
% 1.49/1.85 parent0[3]: (4907) {G1,W16,D3,L4,V0,M4} { j( e20 ) ==> e12, h( e12 ) ==>
% 1.49/1.85 e21, e22 ==> h( e12 ), e23 ==> h( e12 ) }.
% 1.49/1.85 substitution0:
% 1.49/1.85 end
% 1.49/1.85
% 1.49/1.85 eqswap: (4911) {G1,W16,D3,L4,V0,M4} { h( e12 ) ==> e22, h( e12 ) ==> e23,
% 1.49/1.85 j( e20 ) ==> e12, h( e12 ) ==> e21 }.
% 1.49/1.85 parent0[3]: (4909) {G1,W16,D3,L4,V0,M4} { h( e12 ) ==> e23, j( e20 ) ==>
% 1.49/1.85 e12, h( e12 ) ==> e21, e22 ==> h( e12 ) }.
% 1.49/1.85 substitution0:
% 1.49/1.85 end
% 1.49/1.85
% 1.49/1.85 subsumption: (116) {G1,W16,D3,L4,V0,M4} P(62,106) { j( e20 ) ==> e12, h(
% 1.49/1.85 e12 ) ==> e21, h( e12 ) ==> e22, h( e12 ) ==> e23 }.
% 1.49/1.85 parent0: (4911) {G1,W16,D3,L4,V0,M4} { h( e12 ) ==> e22, h( e12 ) ==> e23
% 1.49/1.85 , j( e20 ) ==> e12, h( e12 ) ==> e21 }.
% 1.49/1.85 substitution0:
% 1.49/1.85 end
% 1.49/1.85 permutation0:
% 1.49/1.85 0 ==> 2
% 1.49/1.85 1 ==> 3
% 1.49/1.85 2 ==> 0
% 1.49/1.85 3 ==> 1
% 1.49/1.85 end
% 1.49/1.85
% 1.49/1.85 *** allocated 170857 integers for clauses
% 1.49/1.85 eqswap: (6072) {G0,W16,D3,L4,V0,M4} { e23 ==> h( e10 ), h( e10 ) ==> e20,
% 1.49/1.85 h( e10 ) ==> e21, h( e10 ) ==> e22 }.
% 1.49/1.85 parent0[3]: (60) {G0,W16,D3,L4,V0,M4} I { h( e10 ) ==> e20, h( e10 ) ==>
% 1.49/1.85 e21, h( e10 ) ==> e22, h( e10 ) ==> e23 }.
% 1.49/1.85 substitution0:
% 1.49/1.85 end
% 1.49/1.85
% 1.49/1.85 eqswap: (6075) {G0,W16,D3,L4,V0,M4} { e22 ==> h( e10 ), e23 ==> h( e10 ),
% 1.49/1.85 h( e10 ) ==> e20, h( e10 ) ==> e21 }.
% 1.49/1.85 parent0[3]: (6072) {G0,W16,D3,L4,V0,M4} { e23 ==> h( e10 ), h( e10 ) ==>
% 1.49/1.85 e20, h( e10 ) ==> e21, h( e10 ) ==> e22 }.
% 1.49/1.85 substitution0:
% 1.49/1.85 end
% 1.49/1.85
% 1.49/1.85 eqswap: (6076) {G0,W16,D3,L4,V0,M4} { e20 ==> h( e10 ), e22 ==> h( e10 ),
% 1.49/1.85 e23 ==> h( e10 ), h( e10 ) ==> e21 }.
% 1.49/1.85 parent0[2]: (6075) {G0,W16,D3,L4,V0,M4} { e22 ==> h( e10 ), e23 ==> h( e10
% 1.49/1.85 ), h( e10 ) ==> e20, h( e10 ) ==> e21 }.
% 1.49/1.85 substitution0:
% 1.49/1.85 end
% 1.49/1.85
% 1.49/1.85 eqswap: (6084) {G1,W8,D4,L1,V0,M1} { h( e10 ) ==> op2( h( e10 ), h( e10 )
% 1.49/1.85 ) }.
% 1.49/1.85 parent0[0]: (68) {G1,W8,D4,L1,V0,M1} I;d(28) { op2( h( e10 ), h( e10 ) )
% 1.49/1.85 ==> h( e10 ) }.
% 1.49/1.85 substitution0:
% 1.49/1.85 end
% 1.49/1.85
% 1.49/1.85 paramod: (12255) {G1,W19,D4,L4,V0,M4} { h( e10 ) ==> op2( h( e10 ), e21 )
% 1.49/1.85 , e20 ==> h( e10 ), e22 ==> h( e10 ), e23 ==> h( e10 ) }.
% 1.49/1.85 parent0[3]: (6076) {G0,W16,D3,L4,V0,M4} { e20 ==> h( e10 ), e22 ==> h( e10
% 1.49/1.85 ), e23 ==> h( e10 ), h( e10 ) ==> e21 }.
% 1.49/1.85 parent1[0; 6]: (6084) {G1,W8,D4,L1,V0,M1} { h( e10 ) ==> op2( h( e10 ), h
% 1.49/1.85 ( e10 ) ) }.
% 1.49/1.85 substitution0:
% 1.49/1.85 end
% 1.49/1.85 substitution1:
% 1.49/1.85 end
% 1.49/1.85
% 1.49/1.85 paramod: (12260) {G1,W30,D4,L7,V0,M7} { e23 ==> e21, e20 ==> h( e10 ), e22
% 1.49/1.85 ==> h( e10 ), e23 ==> h( e10 ), h( e10 ) ==> op2( h( e10 ), e21 ), e20
% 1.49/1.85 ==> h( e10 ), e22 ==> h( e10 ) }.
% 1.49/1.85 parent0[3]: (6076) {G0,W16,D3,L4,V0,M4} { e20 ==> h( e10 ), e22 ==> h( e10
% 1.49/1.85 ), e23 ==> h( e10 ), h( e10 ) ==> e21 }.
% 1.49/1.85 parent1[3; 2]: (12255) {G1,W19,D4,L4,V0,M4} { h( e10 ) ==> op2( h( e10 ),
% 1.49/1.85 e21 ), e20 ==> h( e10 ), e22 ==> h( e10 ), e23 ==> h( e10 ) }.
% 1.49/1.85 substitution0:
% 1.49/1.85 end
% 1.49/1.85 substitution1:
% 1.49/1.85 end
% 1.49/1.85
% 1.49/1.85 paramod: (12265) {G1,W41,D3,L10,V0,M10} { h( e10 ) ==> op2( e21, e21 ),
% 1.49/1.85 e20 ==> h( e10 ), e22 ==> h( e10 ), e23 ==> h( e10 ), e23 ==> e21, e20
% 1.49/1.85 ==> h( e10 ), e22 ==> h( e10 ), e23 ==> h( e10 ), e20 ==> h( e10 ), e22
% 1.49/1.85 ==> h( e10 ) }.
% 1.49/1.85 parent0[3]: (6076) {G0,W16,D3,L4,V0,M4} { e20 ==> h( e10 ), e22 ==> h( e10
% 1.49/1.85 ), e23 ==> h( e10 ), h( e10 ) ==> e21 }.
% 1.49/1.85 parent1[4; 4]: (12260) {G1,W30,D4,L7,V0,M7} { e23 ==> e21, e20 ==> h( e10
% 1.49/1.85 ), e22 ==> h( e10 ), e23 ==> h( e10 ), h( e10 ) ==> op2( h( e10 ), e21 )
% 1.49/1.85 , e20 ==> h( e10 ), e22 ==> h( e10 ) }.
% 1.49/1.85 substitution0:
% 1.49/1.85 end
% 1.49/1.85 substitution1:
% 1.49/1.85 end
% 1.49/1.85
% 1.49/1.85 paramod: (12493) {G1,W39,D3,L10,V0,M10} { h( e10 ) ==> e23, e20 ==> h( e10
% 1.49/1.85 ), e22 ==> h( e10 ), e23 ==> h( e10 ), e23 ==> e21, e20 ==> h( e10 ),
% 1.49/1.85 e22 ==> h( e10 ), e23 ==> h( e10 ), e20 ==> h( e10 ), e22 ==> h( e10 )
% 1.49/1.85 }.
% 1.49/1.85 parent0[0]: (49) {G0,W5,D3,L1,V0,M1}Cputime limit exceeded (core dumped) (core dumped)
% 300.05/300.43 Bliksem ended
% 300.05/300.43 Cputime limit exceeded (core dumped)
%------------------------------------------------------------------------------