%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SYN551+1 : TPTP v8.1.0. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n005.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 21 02:52:54 EDT 2022
% Result : Theorem 1.18s 1.59s
% Output : Refutation 1.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SYN551+1 : TPTP v8.1.0. Bugfixed v3.1.0.
% 0.06/0.12 % Command : bliksem %s
% 0.13/0.33 % Computer : n005.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 : Mon Jul 11 22:59:36 EDT 2022
% 0.13/0.33 % CPUTime :
% 1.18/1.59 *** allocated 10000 integers for termspace/termends
% 1.18/1.59 *** allocated 10000 integers for clauses
% 1.18/1.59 *** allocated 10000 integers for justifications
% 1.18/1.59 Bliksem 1.12
% 1.18/1.59
% 1.18/1.59
% 1.18/1.59 Automatic Strategy Selection
% 1.18/1.59
% 1.18/1.59
% 1.18/1.59 Clauses:
% 1.18/1.59
% 1.18/1.59 { alpha6, skol1 = g( f( skol1 ) ) }.
% 1.18/1.59 { alpha6, alpha2 }.
% 1.18/1.59 { alpha6, ! alpha1 }.
% 1.18/1.59 { ! alpha6, alpha1 }.
% 1.18/1.59 { ! alpha6, ! X = g( f( X ) ), ! alpha2 }.
% 1.18/1.59 { ! alpha1, skol2 = g( f( skol2 ) ), alpha6 }.
% 1.18/1.59 { ! alpha1, alpha2, alpha6 }.
% 1.18/1.59 { ! alpha2, ! alpha4( X, Y ), X = Y }.
% 1.18/1.59 { alpha4( skol3, skol6 ), alpha2 }.
% 1.18/1.59 { ! skol3 = skol6, alpha2 }.
% 1.18/1.59 { ! alpha4( X, Y ), X = g( f( X ) ) }.
% 1.18/1.59 { ! alpha4( X, Y ), Y = g( f( Y ) ) }.
% 1.18/1.59 { ! X = g( f( X ) ), ! Y = g( f( Y ) ), alpha4( X, Y ) }.
% 1.18/1.59 { ! alpha1, skol4 = f( g( skol4 ) ) }.
% 1.18/1.59 { ! alpha1, alpha3 }.
% 1.18/1.59 { ! X = f( g( X ) ), ! alpha3, alpha1 }.
% 1.18/1.59 { ! alpha3, ! alpha5( X, Y ), X = Y }.
% 1.18/1.59 { alpha5( skol5, skol7 ), alpha3 }.
% 1.18/1.59 { ! skol5 = skol7, alpha3 }.
% 1.18/1.59 { ! alpha5( X, Y ), X = f( g( X ) ) }.
% 1.18/1.59 { ! alpha5( X, Y ), Y = f( g( Y ) ) }.
% 1.18/1.59 { ! X = f( g( X ) ), ! Y = f( g( Y ) ), alpha5( X, Y ) }.
% 1.18/1.59
% 1.18/1.59 percentage equality = 0.347826, percentage horn = 0.800000
% 1.18/1.59 This is a problem with some equality
% 1.18/1.59
% 1.18/1.59
% 1.18/1.59
% 1.18/1.59 Options Used:
% 1.18/1.59
% 1.18/1.59 useres = 1
% 1.18/1.59 useparamod = 1
% 1.18/1.59 useeqrefl = 1
% 1.18/1.59 useeqfact = 1
% 1.18/1.59 usefactor = 1
% 1.18/1.59 usesimpsplitting = 0
% 1.18/1.59 usesimpdemod = 5
% 1.18/1.59 usesimpres = 3
% 1.18/1.59
% 1.18/1.59 resimpinuse = 1000
% 1.18/1.59 resimpclauses = 20000
% 1.18/1.59 substype = eqrewr
% 1.18/1.59 backwardsubs = 1
% 1.18/1.59 selectoldest = 5
% 1.18/1.59
% 1.18/1.59 litorderings [0] = split
% 1.18/1.59 litorderings [1] = extend the termordering, first sorting on arguments
% 1.18/1.59
% 1.18/1.59 termordering = kbo
% 1.18/1.59
% 1.18/1.59 litapriori = 0
% 1.18/1.59 termapriori = 1
% 1.18/1.59 litaposteriori = 0
% 1.18/1.59 termaposteriori = 0
% 1.18/1.59 demodaposteriori = 0
% 1.18/1.59 ordereqreflfact = 0
% 1.18/1.59
% 1.18/1.59 litselect = negord
% 1.18/1.59
% 1.18/1.59 maxweight = 15
% 1.18/1.59 maxdepth = 30000
% 1.18/1.59 maxlength = 115
% 1.18/1.59 maxnrvars = 195
% 1.18/1.59 excuselevel = 1
% 1.18/1.59 increasemaxweight = 1
% 1.18/1.59
% 1.18/1.59 maxselected = 10000000
% 1.18/1.59 maxnrclauses = 10000000
% 1.18/1.59
% 1.18/1.59 showgenerated = 0
% 1.18/1.59 showkept = 0
% 1.18/1.59 showselected = 0
% 1.18/1.59 showdeleted = 0
% 1.18/1.59 showresimp = 1
% 1.18/1.59 showstatus = 2000
% 1.18/1.59
% 1.18/1.59 prologoutput = 0
% 1.18/1.59 nrgoals = 5000000
% 1.18/1.59 totalproof = 1
% 1.18/1.59
% 1.18/1.59 Symbols occurring in the translation:
% 1.18/1.59
% 1.18/1.59 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 1.18/1.59 . [1, 2] (w:1, o:27, a:1, s:1, b:0),
% 1.18/1.59 ! [4, 1] (w:0, o:20, a:1, s:1, b:0),
% 1.18/1.59 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.18/1.59 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.18/1.59 g [36, 1] (w:1, o:26, a:1, s:1, b:0),
% 1.18/1.59 f [37, 1] (w:1, o:25, a:1, s:1, b:0),
% 1.18/1.59 alpha1 [40, 0] (w:1, o:9, a:1, s:1, b:1),
% 1.18/1.59 alpha2 [41, 0] (w:1, o:10, a:1, s:1, b:1),
% 1.18/1.59 alpha3 [42, 0] (w:1, o:11, a:1, s:1, b:1),
% 1.18/1.59 alpha4 [43, 2] (w:1, o:51, a:1, s:1, b:1),
% 1.18/1.59 alpha5 [44, 2] (w:1, o:52, a:1, s:1, b:1),
% 1.18/1.59 alpha6 [45, 0] (w:1, o:12, a:1, s:1, b:1),
% 1.18/1.59 skol1 [46, 0] (w:1, o:13, a:1, s:1, b:1),
% 1.18/1.59 skol2 [47, 0] (w:1, o:14, a:1, s:1, b:1),
% 1.18/1.59 skol3 [48, 0] (w:1, o:15, a:1, s:1, b:1),
% 1.18/1.59 skol4 [49, 0] (w:1, o:16, a:1, s:1, b:1),
% 1.18/1.59 skol5 [50, 0] (w:1, o:17, a:1, s:1, b:1),
% 1.18/1.59 skol6 [51, 0] (w:1, o:18, a:1, s:1, b:1),
% 1.18/1.59 skol7 [52, 0] (w:1, o:19, a:1, s:1, b:1).
% 1.18/1.59
% 1.18/1.59
% 1.18/1.59 Starting Search:
% 1.18/1.59
% 1.18/1.59 *** allocated 15000 integers for clauses
% 1.18/1.59 *** allocated 22500 integers for clauses
% 1.18/1.59 *** allocated 33750 integers for clauses
% 1.18/1.59 *** allocated 50625 integers for clauses
% 1.18/1.59 *** allocated 15000 integers for termspace/termends
% 1.18/1.59 Resimplifying inuse:
% 1.18/1.59 Done
% 1.18/1.59
% 1.18/1.59 *** allocated 75937 integers for clauses
% 1.18/1.59 *** allocated 22500 integers for termspace/termends
% 1.18/1.59 *** allocated 33750 integers for termspace/termends
% 1.18/1.59 *** allocated 113905 integers for clauses
% 1.18/1.59
% 1.18/1.59 Intermediate Status:
% 1.18/1.59 Generated: 12785
% 1.18/1.59 Kept: 2000
% 1.18/1.59 Inuse: 265
% 1.18/1.59 Deleted: 21
% 1.18/1.59 Deletedinuse: 2
% 1.18/1.59
% 1.18/1.59 Resimplifying inuse:
% 1.18/1.59 Done
% 1.18/1.59
% 1.18/1.59 *** allocated 50625 integers for termspace/termends
% 1.18/1.59 *** allocated 170857 integers for clauses
% 1.18/1.59 Resimplifying inuse:
% 1.18/1.59 Done
% 1.18/1.59
% 1.18/1.59 *** allocated 75937 integers for termspace/termends
% 1.18/1.59
% 1.18/1.59 Intermediate Status:
% 1.18/1.59 Generated: 28471
% 1.18/1.59 Kept: 4006
% 1.18/1.59 Inuse: 399
% 1.18/1.59 Deleted: 52
% 1.18/1.59 Deletedinuse: 2
% 1.18/1.59
% 1.18/1.59
% 1.18/1.59 Bliksems!, er is een bewijs:
% 1.18/1.59 % SZS status Theorem
% 1.18/1.59 % SZS output start Refutation
% 1.18/1.59
% 1.18/1.59 (0) {G0,W6,D4,L2,V0,M2} I { alpha6, g( f( skol1 ) ) ==> skol1 }.
% 1.18/1.59 (1) {G0,W2,D1,L2,V0,M2} I { alpha6, alpha2 }.
% 1.18/1.59 (2) {G0,W2,D1,L2,V0,M2} I { alpha6, ! alpha1 }.
% 1.18/1.59 (3) {G0,W2,D1,L2,V0,M2} I { ! alpha6, alpha1 }.
% 1.18/1.59 (4) {G0,W7,D4,L3,V1,M3} I { ! alpha6, ! g( f( X ) ) ==> X, ! alpha2 }.
% 1.18/1.59 (5) {G0,W7,D2,L3,V2,M3} I { ! alpha2, ! alpha4( X, Y ), X = Y }.
% 1.18/1.59 (6) {G0,W4,D2,L2,V0,M2} I { alpha4( skol3, skol6 ), alpha2 }.
% 1.18/1.59 (7) {G0,W4,D2,L2,V0,M2} I { ! skol6 ==> skol3, alpha2 }.
% 1.18/1.59 (8) {G0,W8,D4,L2,V2,M2} I { ! alpha4( X, Y ), g( f( X ) ) ==> X }.
% 1.18/1.59 (9) {G0,W8,D4,L2,V2,M2} I { ! alpha4( X, Y ), g( f( Y ) ) ==> Y }.
% 1.18/1.59 (10) {G0,W13,D4,L3,V2,M3} I { ! g( f( X ) ) ==> X, ! g( f( Y ) ) ==> Y,
% 1.18/1.59 alpha4( X, Y ) }.
% 1.18/1.59 (11) {G0,W6,D4,L2,V0,M2} I { ! alpha1, f( g( skol4 ) ) ==> skol4 }.
% 1.18/1.59 (12) {G0,W2,D1,L2,V0,M2} I { ! alpha1, alpha3 }.
% 1.18/1.59 (13) {G0,W7,D4,L3,V1,M3} I { ! f( g( X ) ) ==> X, ! alpha3, alpha1 }.
% 1.18/1.59 (14) {G0,W7,D2,L3,V2,M3} I { ! alpha3, ! alpha5( X, Y ), X = Y }.
% 1.18/1.59 (15) {G0,W4,D2,L2,V0,M2} I { alpha5( skol5, skol7 ), alpha3 }.
% 1.18/1.59 (16) {G0,W4,D2,L2,V0,M2} I { ! skol7 ==> skol5, alpha3 }.
% 1.18/1.59 (17) {G0,W8,D4,L2,V2,M2} I { ! alpha5( X, Y ), f( g( X ) ) ==> X }.
% 1.18/1.59 (18) {G0,W8,D4,L2,V2,M2} I { ! alpha5( X, Y ), f( g( Y ) ) ==> Y }.
% 1.18/1.59 (19) {G0,W13,D4,L3,V2,M3} I { ! f( g( X ) ) ==> X, ! f( g( Y ) ) ==> Y,
% 1.18/1.59 alpha5( X, Y ) }.
% 1.18/1.59 (22) {G1,W2,D1,L2,V0,M2} R(3,12) { ! alpha6, alpha3 }.
% 1.18/1.59 (26) {G1,W6,D4,L2,V0,M2} R(0,3) { g( f( skol1 ) ) ==> skol1, alpha1 }.
% 1.18/1.59 (35) {G1,W7,D2,L3,V2,M3} R(5,1) { ! alpha4( X, Y ), X = Y, alpha6 }.
% 1.18/1.59 (61) {G1,W2,D1,L2,V0,M2} P(11,4);q;r(2) { ! alpha2, ! alpha1 }.
% 1.18/1.59 (65) {G2,W2,D1,L2,V0,M2} R(61,3) { ! alpha2, ! alpha6 }.
% 1.18/1.59 (72) {G3,W4,D2,L2,V0,M2} R(65,6) { ! alpha6, alpha4( skol3, skol6 ) }.
% 1.18/1.59 (73) {G3,W4,D2,L2,V0,M2} R(65,7) { ! alpha6, ! skol6 ==> skol3 }.
% 1.18/1.59 (74) {G4,W6,D4,L2,V0,M2} R(72,8) { ! alpha6, g( f( skol3 ) ) ==> skol3 }.
% 1.18/1.59 (79) {G4,W6,D4,L2,V0,M2} R(9,72) { g( f( skol6 ) ) ==> skol6, ! alpha6 }.
% 1.18/1.59 (104) {G2,W9,D4,L3,V1,M3} R(10,26) { ! g( f( X ) ) ==> X, alpha4( skol1, X
% 1.18/1.59 ), alpha1 }.
% 1.18/1.59 (105) {G2,W9,D4,L3,V1,M3} R(10,26) { ! g( f( X ) ) ==> X, alpha4( X, skol1
% 1.18/1.59 ), alpha1 }.
% 1.18/1.59 (154) {G1,W2,D1,L2,V0,M2} P(0,13);q;r(2) { ! alpha3, alpha6 }.
% 1.18/1.59 (171) {G2,W4,D2,L2,V0,M2} R(154,16) { alpha6, ! skol7 ==> skol5 }.
% 1.18/1.59 (183) {G2,W7,D2,L3,V2,M3} R(14,22) { ! alpha5( X, Y ), X = Y, ! alpha6 }.
% 1.18/1.59 (238) {G1,W6,D4,L2,V0,M2} R(17,15) { f( g( skol5 ) ) ==> skol5, alpha3 }.
% 1.18/1.59 (259) {G1,W6,D4,L2,V0,M2} R(18,15) { f( g( skol7 ) ) ==> skol7, alpha3 }.
% 1.18/1.59 (3507) {G3,W5,D3,L2,V0,M2} P(238,104);q;r(12) { alpha4( skol1, g( skol5 ) )
% 1.18/1.59 , alpha3 }.
% 1.18/1.59 (3579) {G4,W5,D3,L2,V0,M2} R(3507,35);r(154) { g( skol5 ) ==> skol1, alpha6
% 1.18/1.59 }.
% 1.18/1.59 (3648) {G5,W5,D3,L2,V0,M2} P(3579,238);r(154) { f( skol1 ) ==> skol5,
% 1.18/1.59 alpha6 }.
% 1.18/1.59 (3702) {G3,W5,D3,L2,V0,M2} P(259,105);q;r(12) { alpha4( g( skol7 ), skol1 )
% 1.18/1.59 , alpha3 }.
% 1.18/1.59 (3769) {G4,W5,D3,L2,V0,M2} R(3702,35);r(154) { g( skol7 ) ==> skol1, alpha6
% 1.18/1.59 }.
% 1.18/1.59 (3838) {G6,W4,D2,L2,V0,M2} P(3769,259);d(3648);r(154) { alpha6, skol7 ==>
% 1.18/1.59 skol5 }.
% 1.18/1.59 (3853) {G7,W1,D1,L1,V0,M1} S(3838);r(171) { alpha6 }.
% 1.18/1.59 (3867) {G8,W6,D2,L2,V2,M2} R(3853,183) { ! alpha5( X, Y ), X = Y }.
% 1.18/1.59 (3877) {G8,W5,D4,L1,V0,M1} R(3853,74) { g( f( skol3 ) ) ==> skol3 }.
% 1.18/1.59 (3878) {G8,W5,D4,L1,V0,M1} R(3853,79) { g( f( skol6 ) ) ==> skol6 }.
% 1.18/1.59 (3879) {G8,W3,D2,L1,V0,M1} R(3853,73) { ! skol6 ==> skol3 }.
% 1.18/1.59 (3924) {G9,W8,D3,L2,V1,M2} P(3867,3878) { g( X ) ==> skol6, ! alpha5( f(
% 1.18/1.59 skol6 ), X ) }.
% 1.18/1.59 (4039) {G10,W5,D3,L1,V0,M1} P(3924,3877);r(3879) { ! alpha5( f( skol6 ), f
% 1.18/1.59 ( skol3 ) ) }.
% 1.18/1.59 (4049) {G11,W0,D0,L0,V0,M0} R(4039,19);d(3878);d(3877);q;q { }.
% 1.18/1.59
% 1.18/1.59
% 1.18/1.59 % SZS output end Refutation
% 1.18/1.59 found a proof!
% 1.18/1.59
% 1.18/1.59
% 1.18/1.59 Unprocessed initial clauses:
% 1.18/1.59
% 1.18/1.59 (4051) {G0,W6,D4,L2,V0,M2} { alpha6, skol1 = g( f( skol1 ) ) }.
% 1.18/1.59 (4052) {G0,W2,D1,L2,V0,M2} { alpha6, alpha2 }.
% 1.18/1.59 (4053) {G0,W2,D1,L2,V0,M2} { alpha6, ! alpha1 }.
% 1.18/1.59 (4054) {G0,W2,D1,L2,V0,M2} { ! alpha6, alpha1 }.
% 1.18/1.59 (4055) {G0,W7,D4,L3,V1,M3} { ! alpha6, ! X = g( f( X ) ), ! alpha2 }.
% 1.18/1.59 (4056) {G0,W7,D4,L3,V0,M3} { ! alpha1, skol2 = g( f( skol2 ) ), alpha6 }.
% 1.18/1.59 (4057) {G0,W3,D1,L3,V0,M3} { ! alpha1, alpha2, alpha6 }.
% 1.18/1.59 (4058) {G0,W7,D2,L3,V2,M3} { ! alpha2, ! alpha4( X, Y ), X = Y }.
% 1.18/1.59 (4059) {G0,W4,D2,L2,V0,M2} { alpha4( skol3, skol6 ), alpha2 }.
% 1.18/1.59 (4060) {G0,W4,D2,L2,V0,M2} { ! skol3 = skol6, alpha2 }.
% 1.18/1.59 (4061) {G0,W8,D4,L2,V2,M2} { ! alpha4( X, Y ), X = g( f( X ) ) }.
% 1.18/1.59 (4062) {G0,W8,D4,L2,V2,M2} { ! alpha4( X, Y ), Y = g( f( Y ) ) }.
% 1.18/1.59 (4063) {G0,W13,D4,L3,V2,M3} { ! X = g( f( X ) ), ! Y = g( f( Y ) ), alpha4
% 1.18/1.59 ( X, Y ) }.
% 1.18/1.59 (4064) {G0,W6,D4,L2,V0,M2} { ! alpha1, skol4 = f( g( skol4 ) ) }.
% 1.18/1.59 (4065) {G0,W2,D1,L2,V0,M2} { ! alpha1, alpha3 }.
% 1.18/1.59 (4066) {G0,W7,D4,L3,V1,M3} { ! X = f( g( X ) ), ! alpha3, alpha1 }.
% 1.18/1.59 (4067) {G0,W7,D2,L3,V2,M3} { ! alpha3, ! alpha5( X, Y ), X = Y }.
% 1.18/1.59 (4068) {G0,W4,D2,L2,V0,M2} { alpha5( skol5, skol7 ), alpha3 }.
% 1.18/1.59 (4069) {G0,W4,D2,L2,V0,M2} { ! skol5 = skol7, alpha3 }.
% 1.18/1.59 (4070) {G0,W8,D4,L2,V2,M2} { ! alpha5( X, Y ), X = f( g( X ) ) }.
% 1.18/1.59 (4071) {G0,W8,D4,L2,V2,M2} { ! alpha5( X, Y ), Y = f( g( Y ) ) }.
% 1.18/1.59 (4072) {G0,W13,D4,L3,V2,M3} { ! X = f( g( X ) ), ! Y = f( g( Y ) ), alpha5
% 1.18/1.59 ( X, Y ) }.
% 1.18/1.59
% 1.18/1.59
% 1.18/1.59 Total Proof:
% 1.18/1.59
% 1.18/1.59 eqswap: (4073) {G0,W6,D4,L2,V0,M2} { g( f( skol1 ) ) = skol1, alpha6 }.
% 1.18/1.59 parent0[1]: (4051) {G0,W6,D4,L2,V0,M2} { alpha6, skol1 = g( f( skol1 ) )
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (0) {G0,W6,D4,L2,V0,M2} I { alpha6, g( f( skol1 ) ) ==> skol1
% 1.18/1.59 }.
% 1.18/1.59 parent0: (4073) {G0,W6,D4,L2,V0,M2} { g( f( skol1 ) ) = skol1, alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (1) {G0,W2,D1,L2,V0,M2} I { alpha6, alpha2 }.
% 1.18/1.59 parent0: (4052) {G0,W2,D1,L2,V0,M2} { alpha6, alpha2 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (2) {G0,W2,D1,L2,V0,M2} I { alpha6, ! alpha1 }.
% 1.18/1.59 parent0: (4053) {G0,W2,D1,L2,V0,M2} { alpha6, ! alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (3) {G0,W2,D1,L2,V0,M2} I { ! alpha6, alpha1 }.
% 1.18/1.59 parent0: (4054) {G0,W2,D1,L2,V0,M2} { ! alpha6, alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4078) {G0,W7,D4,L3,V1,M3} { ! g( f( X ) ) = X, ! alpha6, ! alpha2
% 1.18/1.59 }.
% 1.18/1.59 parent0[1]: (4055) {G0,W7,D4,L3,V1,M3} { ! alpha6, ! X = g( f( X ) ), !
% 1.18/1.59 alpha2 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (4) {G0,W7,D4,L3,V1,M3} I { ! alpha6, ! g( f( X ) ) ==> X, !
% 1.18/1.59 alpha2 }.
% 1.18/1.59 parent0: (4078) {G0,W7,D4,L3,V1,M3} { ! g( f( X ) ) = X, ! alpha6, !
% 1.18/1.59 alpha2 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 2 ==> 2
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (5) {G0,W7,D2,L3,V2,M3} I { ! alpha2, ! alpha4( X, Y ), X = Y
% 1.18/1.59 }.
% 1.18/1.59 parent0: (4058) {G0,W7,D2,L3,V2,M3} { ! alpha2, ! alpha4( X, Y ), X = Y
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 2 ==> 2
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (6) {G0,W4,D2,L2,V0,M2} I { alpha4( skol3, skol6 ), alpha2 }.
% 1.18/1.59 parent0: (4059) {G0,W4,D2,L2,V0,M2} { alpha4( skol3, skol6 ), alpha2 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4091) {G0,W4,D2,L2,V0,M2} { ! skol6 = skol3, alpha2 }.
% 1.18/1.59 parent0[0]: (4060) {G0,W4,D2,L2,V0,M2} { ! skol3 = skol6, alpha2 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (7) {G0,W4,D2,L2,V0,M2} I { ! skol6 ==> skol3, alpha2 }.
% 1.18/1.59 parent0: (4091) {G0,W4,D2,L2,V0,M2} { ! skol6 = skol3, alpha2 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4097) {G0,W8,D4,L2,V2,M2} { g( f( X ) ) = X, ! alpha4( X, Y ) }.
% 1.18/1.59 parent0[1]: (4061) {G0,W8,D4,L2,V2,M2} { ! alpha4( X, Y ), X = g( f( X ) )
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (8) {G0,W8,D4,L2,V2,M2} I { ! alpha4( X, Y ), g( f( X ) ) ==>
% 1.18/1.59 X }.
% 1.18/1.59 parent0: (4097) {G0,W8,D4,L2,V2,M2} { g( f( X ) ) = X, ! alpha4( X, Y )
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4104) {G0,W8,D4,L2,V2,M2} { g( f( X ) ) = X, ! alpha4( Y, X ) }.
% 1.18/1.59 parent0[1]: (4062) {G0,W8,D4,L2,V2,M2} { ! alpha4( X, Y ), Y = g( f( Y ) )
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := Y
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (9) {G0,W8,D4,L2,V2,M2} I { ! alpha4( X, Y ), g( f( Y ) ) ==>
% 1.18/1.59 Y }.
% 1.18/1.59 parent0: (4104) {G0,W8,D4,L2,V2,M2} { g( f( X ) ) = X, ! alpha4( Y, X )
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := Y
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4113) {G0,W13,D4,L3,V2,M3} { ! g( f( X ) ) = X, ! Y = g( f( Y ) )
% 1.18/1.59 , alpha4( Y, X ) }.
% 1.18/1.59 parent0[1]: (4063) {G0,W13,D4,L3,V2,M3} { ! X = g( f( X ) ), ! Y = g( f( Y
% 1.18/1.59 ) ), alpha4( X, Y ) }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := Y
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4114) {G0,W13,D4,L3,V2,M3} { ! g( f( X ) ) = X, ! g( f( Y ) ) = Y
% 1.18/1.59 , alpha4( X, Y ) }.
% 1.18/1.59 parent0[1]: (4113) {G0,W13,D4,L3,V2,M3} { ! g( f( X ) ) = X, ! Y = g( f( Y
% 1.18/1.59 ) ), alpha4( Y, X ) }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := Y
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (10) {G0,W13,D4,L3,V2,M3} I { ! g( f( X ) ) ==> X, ! g( f( Y )
% 1.18/1.59 ) ==> Y, alpha4( X, Y ) }.
% 1.18/1.59 parent0: (4114) {G0,W13,D4,L3,V2,M3} { ! g( f( X ) ) = X, ! g( f( Y ) ) =
% 1.18/1.59 Y, alpha4( X, Y ) }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 2 ==> 2
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4129) {G0,W6,D4,L2,V0,M2} { f( g( skol4 ) ) = skol4, ! alpha1 }.
% 1.18/1.59 parent0[1]: (4064) {G0,W6,D4,L2,V0,M2} { ! alpha1, skol4 = f( g( skol4 ) )
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (11) {G0,W6,D4,L2,V0,M2} I { ! alpha1, f( g( skol4 ) ) ==>
% 1.18/1.59 skol4 }.
% 1.18/1.59 parent0: (4129) {G0,W6,D4,L2,V0,M2} { f( g( skol4 ) ) = skol4, ! alpha1
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (12) {G0,W2,D1,L2,V0,M2} I { ! alpha1, alpha3 }.
% 1.18/1.59 parent0: (4065) {G0,W2,D1,L2,V0,M2} { ! alpha1, alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4156) {G0,W7,D4,L3,V1,M3} { ! f( g( X ) ) = X, ! alpha3, alpha1
% 1.18/1.59 }.
% 1.18/1.59 parent0[0]: (4066) {G0,W7,D4,L3,V1,M3} { ! X = f( g( X ) ), ! alpha3,
% 1.18/1.59 alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (13) {G0,W7,D4,L3,V1,M3} I { ! f( g( X ) ) ==> X, ! alpha3,
% 1.18/1.59 alpha1 }.
% 1.18/1.59 parent0: (4156) {G0,W7,D4,L3,V1,M3} { ! f( g( X ) ) = X, ! alpha3, alpha1
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 2 ==> 2
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (14) {G0,W7,D2,L3,V2,M3} I { ! alpha3, ! alpha5( X, Y ), X = Y
% 1.18/1.59 }.
% 1.18/1.59 parent0: (4067) {G0,W7,D2,L3,V2,M3} { ! alpha3, ! alpha5( X, Y ), X = Y
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 2 ==> 2
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (15) {G0,W4,D2,L2,V0,M2} I { alpha5( skol5, skol7 ), alpha3
% 1.18/1.59 }.
% 1.18/1.59 parent0: (4068) {G0,W4,D2,L2,V0,M2} { alpha5( skol5, skol7 ), alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4202) {G0,W4,D2,L2,V0,M2} { ! skol7 = skol5, alpha3 }.
% 1.18/1.59 parent0[0]: (4069) {G0,W4,D2,L2,V0,M2} { ! skol5 = skol7, alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (16) {G0,W4,D2,L2,V0,M2} I { ! skol7 ==> skol5, alpha3 }.
% 1.18/1.59 parent0: (4202) {G0,W4,D2,L2,V0,M2} { ! skol7 = skol5, alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4219) {G0,W8,D4,L2,V2,M2} { f( g( X ) ) = X, ! alpha5( X, Y ) }.
% 1.18/1.59 parent0[1]: (4070) {G0,W8,D4,L2,V2,M2} { ! alpha5( X, Y ), X = f( g( X ) )
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (17) {G0,W8,D4,L2,V2,M2} I { ! alpha5( X, Y ), f( g( X ) ) ==>
% 1.18/1.59 X }.
% 1.18/1.59 parent0: (4219) {G0,W8,D4,L2,V2,M2} { f( g( X ) ) = X, ! alpha5( X, Y )
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4237) {G0,W8,D4,L2,V2,M2} { f( g( X ) ) = X, ! alpha5( Y, X ) }.
% 1.18/1.59 parent0[1]: (4071) {G0,W8,D4,L2,V2,M2} { ! alpha5( X, Y ), Y = f( g( Y ) )
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := Y
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (18) {G0,W8,D4,L2,V2,M2} I { ! alpha5( X, Y ), f( g( Y ) ) ==>
% 1.18/1.59 Y }.
% 1.18/1.59 parent0: (4237) {G0,W8,D4,L2,V2,M2} { f( g( X ) ) = X, ! alpha5( Y, X )
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := Y
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4257) {G0,W13,D4,L3,V2,M3} { ! f( g( X ) ) = X, ! Y = f( g( Y ) )
% 1.18/1.59 , alpha5( Y, X ) }.
% 1.18/1.59 parent0[1]: (4072) {G0,W13,D4,L3,V2,M3} { ! X = f( g( X ) ), ! Y = f( g( Y
% 1.18/1.59 ) ), alpha5( X, Y ) }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := Y
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4258) {G0,W13,D4,L3,V2,M3} { ! f( g( X ) ) = X, ! f( g( Y ) ) = Y
% 1.18/1.59 , alpha5( X, Y ) }.
% 1.18/1.59 parent0[1]: (4257) {G0,W13,D4,L3,V2,M3} { ! f( g( X ) ) = X, ! Y = f( g( Y
% 1.18/1.59 ) ), alpha5( Y, X ) }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := Y
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (19) {G0,W13,D4,L3,V2,M3} I { ! f( g( X ) ) ==> X, ! f( g( Y )
% 1.18/1.59 ) ==> Y, alpha5( X, Y ) }.
% 1.18/1.59 parent0: (4258) {G0,W13,D4,L3,V2,M3} { ! f( g( X ) ) = X, ! f( g( Y ) ) =
% 1.18/1.59 Y, alpha5( X, Y ) }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 2 ==> 2
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4261) {G1,W2,D1,L2,V0,M2} { alpha3, ! alpha6 }.
% 1.18/1.59 parent0[0]: (12) {G0,W2,D1,L2,V0,M2} I { ! alpha1, alpha3 }.
% 1.18/1.59 parent1[1]: (3) {G0,W2,D1,L2,V0,M2} I { ! alpha6, alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (22) {G1,W2,D1,L2,V0,M2} R(3,12) { ! alpha6, alpha3 }.
% 1.18/1.59 parent0: (4261) {G1,W2,D1,L2,V0,M2} { alpha3, ! alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4262) {G0,W6,D4,L2,V0,M2} { skol1 ==> g( f( skol1 ) ), alpha6 }.
% 1.18/1.59 parent0[1]: (0) {G0,W6,D4,L2,V0,M2} I { alpha6, g( f( skol1 ) ) ==> skol1
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4263) {G1,W6,D4,L2,V0,M2} { alpha1, skol1 ==> g( f( skol1 ) )
% 1.18/1.59 }.
% 1.18/1.59 parent0[0]: (3) {G0,W2,D1,L2,V0,M2} I { ! alpha6, alpha1 }.
% 1.18/1.59 parent1[1]: (4262) {G0,W6,D4,L2,V0,M2} { skol1 ==> g( f( skol1 ) ), alpha6
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4264) {G1,W6,D4,L2,V0,M2} { g( f( skol1 ) ) ==> skol1, alpha1 }.
% 1.18/1.59 parent0[1]: (4263) {G1,W6,D4,L2,V0,M2} { alpha1, skol1 ==> g( f( skol1 ) )
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (26) {G1,W6,D4,L2,V0,M2} R(0,3) { g( f( skol1 ) ) ==> skol1,
% 1.18/1.59 alpha1 }.
% 1.18/1.59 parent0: (4264) {G1,W6,D4,L2,V0,M2} { g( f( skol1 ) ) ==> skol1, alpha1
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4265) {G0,W7,D2,L3,V2,M3} { Y = X, ! alpha2, ! alpha4( X, Y ) }.
% 1.18/1.59 parent0[2]: (5) {G0,W7,D2,L3,V2,M3} I { ! alpha2, ! alpha4( X, Y ), X = Y
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4266) {G1,W7,D2,L3,V2,M3} { X = Y, ! alpha4( Y, X ), alpha6
% 1.18/1.59 }.
% 1.18/1.59 parent0[1]: (4265) {G0,W7,D2,L3,V2,M3} { Y = X, ! alpha2, ! alpha4( X, Y )
% 1.18/1.59 }.
% 1.18/1.59 parent1[1]: (1) {G0,W2,D1,L2,V0,M2} I { alpha6, alpha2 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := Y
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4267) {G1,W7,D2,L3,V2,M3} { Y = X, ! alpha4( Y, X ), alpha6 }.
% 1.18/1.59 parent0[0]: (4266) {G1,W7,D2,L3,V2,M3} { X = Y, ! alpha4( Y, X ), alpha6
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (35) {G1,W7,D2,L3,V2,M3} R(5,1) { ! alpha4( X, Y ), X = Y,
% 1.18/1.59 alpha6 }.
% 1.18/1.59 parent0: (4267) {G1,W7,D2,L3,V2,M3} { Y = X, ! alpha4( Y, X ), alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := Y
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 2 ==> 2
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4269) {G0,W7,D4,L3,V1,M3} { ! X ==> g( f( X ) ), ! alpha6, !
% 1.18/1.59 alpha2 }.
% 1.18/1.59 parent0[1]: (4) {G0,W7,D4,L3,V1,M3} I { ! alpha6, ! g( f( X ) ) ==> X, !
% 1.18/1.59 alpha2 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 paramod: (4270) {G1,W8,D3,L4,V0,M4} { ! g( skol4 ) ==> g( skol4 ), !
% 1.18/1.59 alpha1, ! alpha6, ! alpha2 }.
% 1.18/1.59 parent0[1]: (11) {G0,W6,D4,L2,V0,M2} I { ! alpha1, f( g( skol4 ) ) ==>
% 1.18/1.59 skol4 }.
% 1.18/1.59 parent1[0; 5]: (4269) {G0,W7,D4,L3,V1,M3} { ! X ==> g( f( X ) ), ! alpha6
% 1.18/1.59 , ! alpha2 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 X := g( skol4 )
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqrefl: (4271) {G0,W3,D1,L3,V0,M3} { ! alpha1, ! alpha6, ! alpha2 }.
% 1.18/1.59 parent0[0]: (4270) {G1,W8,D3,L4,V0,M4} { ! g( skol4 ) ==> g( skol4 ), !
% 1.18/1.59 alpha1, ! alpha6, ! alpha2 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4272) {G1,W3,D1,L3,V0,M3} { ! alpha1, ! alpha2, ! alpha1 }.
% 1.18/1.59 parent0[1]: (4271) {G0,W3,D1,L3,V0,M3} { ! alpha1, ! alpha6, ! alpha2 }.
% 1.18/1.59 parent1[0]: (2) {G0,W2,D1,L2,V0,M2} I { alpha6, ! alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 factor: (4273) {G1,W2,D1,L2,V0,M2} { ! alpha1, ! alpha2 }.
% 1.18/1.59 parent0[0, 2]: (4272) {G1,W3,D1,L3,V0,M3} { ! alpha1, ! alpha2, ! alpha1
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (61) {G1,W2,D1,L2,V0,M2} P(11,4);q;r(2) { ! alpha2, ! alpha1
% 1.18/1.59 }.
% 1.18/1.59 parent0: (4273) {G1,W2,D1,L2,V0,M2} { ! alpha1, ! alpha2 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4274) {G1,W2,D1,L2,V0,M2} { ! alpha2, ! alpha6 }.
% 1.18/1.59 parent0[1]: (61) {G1,W2,D1,L2,V0,M2} P(11,4);q;r(2) { ! alpha2, ! alpha1
% 1.18/1.59 }.
% 1.18/1.59 parent1[1]: (3) {G0,W2,D1,L2,V0,M2} I { ! alpha6, alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (65) {G2,W2,D1,L2,V0,M2} R(61,3) { ! alpha2, ! alpha6 }.
% 1.18/1.59 parent0: (4274) {G1,W2,D1,L2,V0,M2} { ! alpha2, ! alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4275) {G1,W4,D2,L2,V0,M2} { ! alpha6, alpha4( skol3, skol6 )
% 1.18/1.59 }.
% 1.18/1.59 parent0[0]: (65) {G2,W2,D1,L2,V0,M2} R(61,3) { ! alpha2, ! alpha6 }.
% 1.18/1.59 parent1[1]: (6) {G0,W4,D2,L2,V0,M2} I { alpha4( skol3, skol6 ), alpha2 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (72) {G3,W4,D2,L2,V0,M2} R(65,6) { ! alpha6, alpha4( skol3,
% 1.18/1.59 skol6 ) }.
% 1.18/1.59 parent0: (4275) {G1,W4,D2,L2,V0,M2} { ! alpha6, alpha4( skol3, skol6 ) }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4276) {G0,W4,D2,L2,V0,M2} { ! skol3 ==> skol6, alpha2 }.
% 1.18/1.59 parent0[0]: (7) {G0,W4,D2,L2,V0,M2} I { ! skol6 ==> skol3, alpha2 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4277) {G1,W4,D2,L2,V0,M2} { ! alpha6, ! skol3 ==> skol6 }.
% 1.18/1.59 parent0[0]: (65) {G2,W2,D1,L2,V0,M2} R(61,3) { ! alpha2, ! alpha6 }.
% 1.18/1.59 parent1[1]: (4276) {G0,W4,D2,L2,V0,M2} { ! skol3 ==> skol6, alpha2 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4278) {G1,W4,D2,L2,V0,M2} { ! skol6 ==> skol3, ! alpha6 }.
% 1.18/1.59 parent0[1]: (4277) {G1,W4,D2,L2,V0,M2} { ! alpha6, ! skol3 ==> skol6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (73) {G3,W4,D2,L2,V0,M2} R(65,7) { ! alpha6, ! skol6 ==> skol3
% 1.18/1.59 }.
% 1.18/1.59 parent0: (4278) {G1,W4,D2,L2,V0,M2} { ! skol6 ==> skol3, ! alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4279) {G0,W8,D4,L2,V2,M2} { X ==> g( f( X ) ), ! alpha4( X, Y )
% 1.18/1.59 }.
% 1.18/1.59 parent0[1]: (8) {G0,W8,D4,L2,V2,M2} I { ! alpha4( X, Y ), g( f( X ) ) ==> X
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4280) {G1,W6,D4,L2,V0,M2} { skol3 ==> g( f( skol3 ) ), !
% 1.18/1.59 alpha6 }.
% 1.18/1.59 parent0[1]: (4279) {G0,W8,D4,L2,V2,M2} { X ==> g( f( X ) ), ! alpha4( X, Y
% 1.18/1.59 ) }.
% 1.18/1.59 parent1[1]: (72) {G3,W4,D2,L2,V0,M2} R(65,6) { ! alpha6, alpha4( skol3,
% 1.18/1.59 skol6 ) }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := skol3
% 1.18/1.59 Y := skol6
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4281) {G1,W6,D4,L2,V0,M2} { g( f( skol3 ) ) ==> skol3, ! alpha6
% 1.18/1.59 }.
% 1.18/1.59 parent0[0]: (4280) {G1,W6,D4,L2,V0,M2} { skol3 ==> g( f( skol3 ) ), !
% 1.18/1.59 alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (74) {G4,W6,D4,L2,V0,M2} R(72,8) { ! alpha6, g( f( skol3 ) )
% 1.18/1.59 ==> skol3 }.
% 1.18/1.59 parent0: (4281) {G1,W6,D4,L2,V0,M2} { g( f( skol3 ) ) ==> skol3, ! alpha6
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4282) {G0,W8,D4,L2,V2,M2} { X ==> g( f( X ) ), ! alpha4( Y, X )
% 1.18/1.59 }.
% 1.18/1.59 parent0[1]: (9) {G0,W8,D4,L2,V2,M2} I { ! alpha4( X, Y ), g( f( Y ) ) ==> Y
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := Y
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4283) {G1,W6,D4,L2,V0,M2} { skol6 ==> g( f( skol6 ) ), !
% 1.18/1.59 alpha6 }.
% 1.18/1.59 parent0[1]: (4282) {G0,W8,D4,L2,V2,M2} { X ==> g( f( X ) ), ! alpha4( Y, X
% 1.18/1.59 ) }.
% 1.18/1.59 parent1[1]: (72) {G3,W4,D2,L2,V0,M2} R(65,6) { ! alpha6, alpha4( skol3,
% 1.18/1.59 skol6 ) }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := skol6
% 1.18/1.59 Y := skol3
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4284) {G1,W6,D4,L2,V0,M2} { g( f( skol6 ) ) ==> skol6, ! alpha6
% 1.18/1.59 }.
% 1.18/1.59 parent0[0]: (4283) {G1,W6,D4,L2,V0,M2} { skol6 ==> g( f( skol6 ) ), !
% 1.18/1.59 alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (79) {G4,W6,D4,L2,V0,M2} R(9,72) { g( f( skol6 ) ) ==> skol6,
% 1.18/1.59 ! alpha6 }.
% 1.18/1.59 parent0: (4284) {G1,W6,D4,L2,V0,M2} { g( f( skol6 ) ) ==> skol6, ! alpha6
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4285) {G0,W13,D4,L3,V2,M3} { ! X ==> g( f( X ) ), ! g( f( Y ) )
% 1.18/1.59 ==> Y, alpha4( X, Y ) }.
% 1.18/1.59 parent0[0]: (10) {G0,W13,D4,L3,V2,M3} I { ! g( f( X ) ) ==> X, ! g( f( Y )
% 1.18/1.59 ) ==> Y, alpha4( X, Y ) }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4288) {G1,W6,D4,L2,V0,M2} { skol1 ==> g( f( skol1 ) ), alpha1 }.
% 1.18/1.59 parent0[0]: (26) {G1,W6,D4,L2,V0,M2} R(0,3) { g( f( skol1 ) ) ==> skol1,
% 1.18/1.59 alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4289) {G1,W9,D4,L3,V1,M3} { ! g( f( X ) ) ==> X, alpha4(
% 1.18/1.59 skol1, X ), alpha1 }.
% 1.18/1.59 parent0[0]: (4285) {G0,W13,D4,L3,V2,M3} { ! X ==> g( f( X ) ), ! g( f( Y )
% 1.18/1.59 ) ==> Y, alpha4( X, Y ) }.
% 1.18/1.59 parent1[0]: (4288) {G1,W6,D4,L2,V0,M2} { skol1 ==> g( f( skol1 ) ), alpha1
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := skol1
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (104) {G2,W9,D4,L3,V1,M3} R(10,26) { ! g( f( X ) ) ==> X,
% 1.18/1.59 alpha4( skol1, X ), alpha1 }.
% 1.18/1.59 parent0: (4289) {G1,W9,D4,L3,V1,M3} { ! g( f( X ) ) ==> X, alpha4( skol1,
% 1.18/1.59 X ), alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 2 ==> 2
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4291) {G0,W13,D4,L3,V2,M3} { ! X ==> g( f( X ) ), ! g( f( Y ) )
% 1.18/1.59 ==> Y, alpha4( X, Y ) }.
% 1.18/1.59 parent0[0]: (10) {G0,W13,D4,L3,V2,M3} I { ! g( f( X ) ) ==> X, ! g( f( Y )
% 1.18/1.59 ) ==> Y, alpha4( X, Y ) }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4297) {G1,W9,D4,L3,V1,M3} { ! X ==> g( f( X ) ), alpha4( X,
% 1.18/1.59 skol1 ), alpha1 }.
% 1.18/1.59 parent0[1]: (4291) {G0,W13,D4,L3,V2,M3} { ! X ==> g( f( X ) ), ! g( f( Y )
% 1.18/1.59 ) ==> Y, alpha4( X, Y ) }.
% 1.18/1.59 parent1[0]: (26) {G1,W6,D4,L2,V0,M2} R(0,3) { g( f( skol1 ) ) ==> skol1,
% 1.18/1.59 alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := skol1
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4298) {G1,W9,D4,L3,V1,M3} { ! g( f( X ) ) ==> X, alpha4( X, skol1
% 1.18/1.59 ), alpha1 }.
% 1.18/1.59 parent0[0]: (4297) {G1,W9,D4,L3,V1,M3} { ! X ==> g( f( X ) ), alpha4( X,
% 1.18/1.59 skol1 ), alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (105) {G2,W9,D4,L3,V1,M3} R(10,26) { ! g( f( X ) ) ==> X,
% 1.18/1.59 alpha4( X, skol1 ), alpha1 }.
% 1.18/1.59 parent0: (4298) {G1,W9,D4,L3,V1,M3} { ! g( f( X ) ) ==> X, alpha4( X,
% 1.18/1.59 skol1 ), alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 2 ==> 2
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4300) {G0,W7,D4,L3,V1,M3} { ! X ==> f( g( X ) ), ! alpha3, alpha1
% 1.18/1.59 }.
% 1.18/1.59 parent0[0]: (13) {G0,W7,D4,L3,V1,M3} I { ! f( g( X ) ) ==> X, ! alpha3,
% 1.18/1.59 alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 paramod: (4301) {G1,W8,D3,L4,V0,M4} { ! f( skol1 ) ==> f( skol1 ), alpha6
% 1.18/1.59 , ! alpha3, alpha1 }.
% 1.18/1.59 parent0[1]: (0) {G0,W6,D4,L2,V0,M2} I { alpha6, g( f( skol1 ) ) ==> skol1
% 1.18/1.59 }.
% 1.18/1.59 parent1[0; 5]: (4300) {G0,W7,D4,L3,V1,M3} { ! X ==> f( g( X ) ), ! alpha3
% 1.18/1.59 , alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 X := f( skol1 )
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqrefl: (4302) {G0,W3,D1,L3,V0,M3} { alpha6, ! alpha3, alpha1 }.
% 1.18/1.59 parent0[0]: (4301) {G1,W8,D3,L4,V0,M4} { ! f( skol1 ) ==> f( skol1 ),
% 1.18/1.59 alpha6, ! alpha3, alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4303) {G1,W3,D1,L3,V0,M3} { alpha6, alpha6, ! alpha3 }.
% 1.18/1.59 parent0[1]: (2) {G0,W2,D1,L2,V0,M2} I { alpha6, ! alpha1 }.
% 1.18/1.59 parent1[2]: (4302) {G0,W3,D1,L3,V0,M3} { alpha6, ! alpha3, alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 factor: (4304) {G1,W2,D1,L2,V0,M2} { alpha6, ! alpha3 }.
% 1.18/1.59 parent0[0, 1]: (4303) {G1,W3,D1,L3,V0,M3} { alpha6, alpha6, ! alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (154) {G1,W2,D1,L2,V0,M2} P(0,13);q;r(2) { ! alpha3, alpha6
% 1.18/1.59 }.
% 1.18/1.59 parent0: (4304) {G1,W2,D1,L2,V0,M2} { alpha6, ! alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4305) {G0,W4,D2,L2,V0,M2} { ! skol5 ==> skol7, alpha3 }.
% 1.18/1.59 parent0[0]: (16) {G0,W4,D2,L2,V0,M2} I { ! skol7 ==> skol5, alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4306) {G1,W4,D2,L2,V0,M2} { alpha6, ! skol5 ==> skol7 }.
% 1.18/1.59 parent0[0]: (154) {G1,W2,D1,L2,V0,M2} P(0,13);q;r(2) { ! alpha3, alpha6 }.
% 1.18/1.59 parent1[1]: (4305) {G0,W4,D2,L2,V0,M2} { ! skol5 ==> skol7, alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4307) {G1,W4,D2,L2,V0,M2} { ! skol7 ==> skol5, alpha6 }.
% 1.18/1.59 parent0[1]: (4306) {G1,W4,D2,L2,V0,M2} { alpha6, ! skol5 ==> skol7 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (171) {G2,W4,D2,L2,V0,M2} R(154,16) { alpha6, ! skol7 ==>
% 1.18/1.59 skol5 }.
% 1.18/1.59 parent0: (4307) {G1,W4,D2,L2,V0,M2} { ! skol7 ==> skol5, alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4308) {G0,W7,D2,L3,V2,M3} { Y = X, ! alpha3, ! alpha5( X, Y ) }.
% 1.18/1.59 parent0[2]: (14) {G0,W7,D2,L3,V2,M3} I { ! alpha3, ! alpha5( X, Y ), X = Y
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4309) {G1,W7,D2,L3,V2,M3} { X = Y, ! alpha5( Y, X ), ! alpha6
% 1.18/1.59 }.
% 1.18/1.59 parent0[1]: (4308) {G0,W7,D2,L3,V2,M3} { Y = X, ! alpha3, ! alpha5( X, Y )
% 1.18/1.59 }.
% 1.18/1.59 parent1[1]: (22) {G1,W2,D1,L2,V0,M2} R(3,12) { ! alpha6, alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := Y
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4310) {G1,W7,D2,L3,V2,M3} { Y = X, ! alpha5( Y, X ), ! alpha6 }.
% 1.18/1.59 parent0[0]: (4309) {G1,W7,D2,L3,V2,M3} { X = Y, ! alpha5( Y, X ), ! alpha6
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (183) {G2,W7,D2,L3,V2,M3} R(14,22) { ! alpha5( X, Y ), X = Y,
% 1.18/1.59 ! alpha6 }.
% 1.18/1.59 parent0: (4310) {G1,W7,D2,L3,V2,M3} { Y = X, ! alpha5( Y, X ), ! alpha6
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := Y
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 2 ==> 2
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4311) {G0,W8,D4,L2,V2,M2} { X ==> f( g( X ) ), ! alpha5( X, Y )
% 1.18/1.59 }.
% 1.18/1.59 parent0[1]: (17) {G0,W8,D4,L2,V2,M2} I { ! alpha5( X, Y ), f( g( X ) ) ==>
% 1.18/1.59 X }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4312) {G1,W6,D4,L2,V0,M2} { skol5 ==> f( g( skol5 ) ), alpha3
% 1.18/1.59 }.
% 1.18/1.59 parent0[1]: (4311) {G0,W8,D4,L2,V2,M2} { X ==> f( g( X ) ), ! alpha5( X, Y
% 1.18/1.59 ) }.
% 1.18/1.59 parent1[0]: (15) {G0,W4,D2,L2,V0,M2} I { alpha5( skol5, skol7 ), alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := skol5
% 1.18/1.59 Y := skol7
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4313) {G1,W6,D4,L2,V0,M2} { f( g( skol5 ) ) ==> skol5, alpha3 }.
% 1.18/1.59 parent0[0]: (4312) {G1,W6,D4,L2,V0,M2} { skol5 ==> f( g( skol5 ) ), alpha3
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (238) {G1,W6,D4,L2,V0,M2} R(17,15) { f( g( skol5 ) ) ==> skol5
% 1.18/1.59 , alpha3 }.
% 1.18/1.59 parent0: (4313) {G1,W6,D4,L2,V0,M2} { f( g( skol5 ) ) ==> skol5, alpha3
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4314) {G0,W8,D4,L2,V2,M2} { X ==> f( g( X ) ), ! alpha5( Y, X )
% 1.18/1.59 }.
% 1.18/1.59 parent0[1]: (18) {G0,W8,D4,L2,V2,M2} I { ! alpha5( X, Y ), f( g( Y ) ) ==>
% 1.18/1.59 Y }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := Y
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4315) {G1,W6,D4,L2,V0,M2} { skol7 ==> f( g( skol7 ) ), alpha3
% 1.18/1.59 }.
% 1.18/1.59 parent0[1]: (4314) {G0,W8,D4,L2,V2,M2} { X ==> f( g( X ) ), ! alpha5( Y, X
% 1.18/1.59 ) }.
% 1.18/1.59 parent1[0]: (15) {G0,W4,D2,L2,V0,M2} I { alpha5( skol5, skol7 ), alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := skol7
% 1.18/1.59 Y := skol5
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4316) {G1,W6,D4,L2,V0,M2} { f( g( skol7 ) ) ==> skol7, alpha3 }.
% 1.18/1.59 parent0[0]: (4315) {G1,W6,D4,L2,V0,M2} { skol7 ==> f( g( skol7 ) ), alpha3
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (259) {G1,W6,D4,L2,V0,M2} R(18,15) { f( g( skol7 ) ) ==> skol7
% 1.18/1.59 , alpha3 }.
% 1.18/1.59 parent0: (4316) {G1,W6,D4,L2,V0,M2} { f( g( skol7 ) ) ==> skol7, alpha3
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4318) {G2,W9,D4,L3,V1,M3} { ! X ==> g( f( X ) ), alpha4( skol1, X
% 1.18/1.59 ), alpha1 }.
% 1.18/1.59 parent0[0]: (104) {G2,W9,D4,L3,V1,M3} R(10,26) { ! g( f( X ) ) ==> X,
% 1.18/1.59 alpha4( skol1, X ), alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 paramod: (4319) {G2,W11,D3,L4,V0,M4} { ! g( skol5 ) ==> g( skol5 ), alpha3
% 1.18/1.59 , alpha4( skol1, g( skol5 ) ), alpha1 }.
% 1.18/1.59 parent0[0]: (238) {G1,W6,D4,L2,V0,M2} R(17,15) { f( g( skol5 ) ) ==> skol5
% 1.18/1.59 , alpha3 }.
% 1.18/1.59 parent1[0; 5]: (4318) {G2,W9,D4,L3,V1,M3} { ! X ==> g( f( X ) ), alpha4(
% 1.18/1.59 skol1, X ), alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 X := g( skol5 )
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqrefl: (4320) {G0,W6,D3,L3,V0,M3} { alpha3, alpha4( skol1, g( skol5 ) ),
% 1.18/1.59 alpha1 }.
% 1.18/1.59 parent0[0]: (4319) {G2,W11,D3,L4,V0,M4} { ! g( skol5 ) ==> g( skol5 ),
% 1.18/1.59 alpha3, alpha4( skol1, g( skol5 ) ), alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4321) {G1,W6,D3,L3,V0,M3} { alpha3, alpha3, alpha4( skol1, g
% 1.18/1.59 ( skol5 ) ) }.
% 1.18/1.59 parent0[0]: (12) {G0,W2,D1,L2,V0,M2} I { ! alpha1, alpha3 }.
% 1.18/1.59 parent1[2]: (4320) {G0,W6,D3,L3,V0,M3} { alpha3, alpha4( skol1, g( skol5 )
% 1.18/1.59 ), alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 factor: (4322) {G1,W5,D3,L2,V0,M2} { alpha3, alpha4( skol1, g( skol5 ) )
% 1.18/1.59 }.
% 1.18/1.59 parent0[0, 1]: (4321) {G1,W6,D3,L3,V0,M3} { alpha3, alpha3, alpha4( skol1
% 1.18/1.59 , g( skol5 ) ) }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (3507) {G3,W5,D3,L2,V0,M2} P(238,104);q;r(12) { alpha4( skol1
% 1.18/1.59 , g( skol5 ) ), alpha3 }.
% 1.18/1.59 parent0: (4322) {G1,W5,D3,L2,V0,M2} { alpha3, alpha4( skol1, g( skol5 ) )
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4323) {G1,W7,D2,L3,V2,M3} { Y = X, ! alpha4( X, Y ), alpha6 }.
% 1.18/1.59 parent0[1]: (35) {G1,W7,D2,L3,V2,M3} R(5,1) { ! alpha4( X, Y ), X = Y,
% 1.18/1.59 alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4324) {G2,W6,D3,L3,V0,M3} { g( skol5 ) = skol1, alpha6,
% 1.18/1.59 alpha3 }.
% 1.18/1.59 parent0[1]: (4323) {G1,W7,D2,L3,V2,M3} { Y = X, ! alpha4( X, Y ), alpha6
% 1.18/1.59 }.
% 1.18/1.59 parent1[0]: (3507) {G3,W5,D3,L2,V0,M2} P(238,104);q;r(12) { alpha4( skol1,
% 1.18/1.59 g( skol5 ) ), alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := skol1
% 1.18/1.59 Y := g( skol5 )
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4325) {G2,W6,D3,L3,V0,M3} { alpha6, g( skol5 ) = skol1,
% 1.18/1.59 alpha6 }.
% 1.18/1.59 parent0[0]: (154) {G1,W2,D1,L2,V0,M2} P(0,13);q;r(2) { ! alpha3, alpha6 }.
% 1.18/1.59 parent1[2]: (4324) {G2,W6,D3,L3,V0,M3} { g( skol5 ) = skol1, alpha6,
% 1.18/1.59 alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 factor: (4328) {G2,W5,D3,L2,V0,M2} { alpha6, g( skol5 ) = skol1 }.
% 1.18/1.59 parent0[0, 2]: (4325) {G2,W6,D3,L3,V0,M3} { alpha6, g( skol5 ) = skol1,
% 1.18/1.59 alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (3579) {G4,W5,D3,L2,V0,M2} R(3507,35);r(154) { g( skol5 ) ==>
% 1.18/1.59 skol1, alpha6 }.
% 1.18/1.59 parent0: (4328) {G2,W5,D3,L2,V0,M2} { alpha6, g( skol5 ) = skol1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4330) {G1,W6,D4,L2,V0,M2} { skol5 ==> f( g( skol5 ) ), alpha3 }.
% 1.18/1.59 parent0[0]: (238) {G1,W6,D4,L2,V0,M2} R(17,15) { f( g( skol5 ) ) ==> skol5
% 1.18/1.59 , alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 paramod: (4331) {G2,W6,D3,L3,V0,M3} { skol5 ==> f( skol1 ), alpha6, alpha3
% 1.18/1.59 }.
% 1.18/1.59 parent0[0]: (3579) {G4,W5,D3,L2,V0,M2} R(3507,35);r(154) { g( skol5 ) ==>
% 1.18/1.59 skol1, alpha6 }.
% 1.18/1.59 parent1[0; 3]: (4330) {G1,W6,D4,L2,V0,M2} { skol5 ==> f( g( skol5 ) ),
% 1.18/1.59 alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4332) {G2,W6,D3,L3,V0,M3} { alpha6, skol5 ==> f( skol1 ),
% 1.18/1.59 alpha6 }.
% 1.18/1.59 parent0[0]: (154) {G1,W2,D1,L2,V0,M2} P(0,13);q;r(2) { ! alpha3, alpha6 }.
% 1.18/1.59 parent1[2]: (4331) {G2,W6,D3,L3,V0,M3} { skol5 ==> f( skol1 ), alpha6,
% 1.18/1.59 alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4333) {G2,W6,D3,L3,V0,M3} { f( skol1 ) ==> skol5, alpha6, alpha6
% 1.18/1.59 }.
% 1.18/1.59 parent0[1]: (4332) {G2,W6,D3,L3,V0,M3} { alpha6, skol5 ==> f( skol1 ),
% 1.18/1.59 alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 factor: (4334) {G2,W5,D3,L2,V0,M2} { f( skol1 ) ==> skol5, alpha6 }.
% 1.18/1.59 parent0[1, 2]: (4333) {G2,W6,D3,L3,V0,M3} { f( skol1 ) ==> skol5, alpha6,
% 1.18/1.59 alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (3648) {G5,W5,D3,L2,V0,M2} P(3579,238);r(154) { f( skol1 ) ==>
% 1.18/1.59 skol5, alpha6 }.
% 1.18/1.59 parent0: (4334) {G2,W5,D3,L2,V0,M2} { f( skol1 ) ==> skol5, alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4337) {G2,W9,D4,L3,V1,M3} { ! X ==> g( f( X ) ), alpha4( X, skol1
% 1.18/1.59 ), alpha1 }.
% 1.18/1.59 parent0[0]: (105) {G2,W9,D4,L3,V1,M3} R(10,26) { ! g( f( X ) ) ==> X,
% 1.18/1.59 alpha4( X, skol1 ), alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 paramod: (4338) {G2,W11,D3,L4,V0,M4} { ! g( skol7 ) ==> g( skol7 ), alpha3
% 1.18/1.59 , alpha4( g( skol7 ), skol1 ), alpha1 }.
% 1.18/1.59 parent0[0]: (259) {G1,W6,D4,L2,V0,M2} R(18,15) { f( g( skol7 ) ) ==> skol7
% 1.18/1.59 , alpha3 }.
% 1.18/1.59 parent1[0; 5]: (4337) {G2,W9,D4,L3,V1,M3} { ! X ==> g( f( X ) ), alpha4( X
% 1.18/1.59 , skol1 ), alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 X := g( skol7 )
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqrefl: (4339) {G0,W6,D3,L3,V0,M3} { alpha3, alpha4( g( skol7 ), skol1 ),
% 1.18/1.59 alpha1 }.
% 1.18/1.59 parent0[0]: (4338) {G2,W11,D3,L4,V0,M4} { ! g( skol7 ) ==> g( skol7 ),
% 1.18/1.59 alpha3, alpha4( g( skol7 ), skol1 ), alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4340) {G1,W6,D3,L3,V0,M3} { alpha3, alpha3, alpha4( g( skol7
% 1.18/1.59 ), skol1 ) }.
% 1.18/1.59 parent0[0]: (12) {G0,W2,D1,L2,V0,M2} I { ! alpha1, alpha3 }.
% 1.18/1.59 parent1[2]: (4339) {G0,W6,D3,L3,V0,M3} { alpha3, alpha4( g( skol7 ), skol1
% 1.18/1.59 ), alpha1 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 factor: (4341) {G1,W5,D3,L2,V0,M2} { alpha3, alpha4( g( skol7 ), skol1 )
% 1.18/1.59 }.
% 1.18/1.59 parent0[0, 1]: (4340) {G1,W6,D3,L3,V0,M3} { alpha3, alpha3, alpha4( g(
% 1.18/1.59 skol7 ), skol1 ) }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (3702) {G3,W5,D3,L2,V0,M2} P(259,105);q;r(12) { alpha4( g(
% 1.18/1.59 skol7 ), skol1 ), alpha3 }.
% 1.18/1.59 parent0: (4341) {G1,W5,D3,L2,V0,M2} { alpha3, alpha4( g( skol7 ), skol1 )
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4342) {G1,W7,D2,L3,V2,M3} { Y = X, ! alpha4( X, Y ), alpha6 }.
% 1.18/1.59 parent0[1]: (35) {G1,W7,D2,L3,V2,M3} R(5,1) { ! alpha4( X, Y ), X = Y,
% 1.18/1.59 alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4343) {G2,W6,D3,L3,V0,M3} { skol1 = g( skol7 ), alpha6,
% 1.18/1.59 alpha3 }.
% 1.18/1.59 parent0[1]: (4342) {G1,W7,D2,L3,V2,M3} { Y = X, ! alpha4( X, Y ), alpha6
% 1.18/1.59 }.
% 1.18/1.59 parent1[0]: (3702) {G3,W5,D3,L2,V0,M2} P(259,105);q;r(12) { alpha4( g(
% 1.18/1.59 skol7 ), skol1 ), alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := g( skol7 )
% 1.18/1.59 Y := skol1
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4344) {G2,W6,D3,L3,V0,M3} { alpha6, skol1 = g( skol7 ),
% 1.18/1.59 alpha6 }.
% 1.18/1.59 parent0[0]: (154) {G1,W2,D1,L2,V0,M2} P(0,13);q;r(2) { ! alpha3, alpha6 }.
% 1.18/1.59 parent1[2]: (4343) {G2,W6,D3,L3,V0,M3} { skol1 = g( skol7 ), alpha6,
% 1.18/1.59 alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4345) {G2,W6,D3,L3,V0,M3} { g( skol7 ) = skol1, alpha6, alpha6
% 1.18/1.59 }.
% 1.18/1.59 parent0[1]: (4344) {G2,W6,D3,L3,V0,M3} { alpha6, skol1 = g( skol7 ),
% 1.18/1.59 alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 factor: (4346) {G2,W5,D3,L2,V0,M2} { g( skol7 ) = skol1, alpha6 }.
% 1.18/1.59 parent0[1, 2]: (4345) {G2,W6,D3,L3,V0,M3} { g( skol7 ) = skol1, alpha6,
% 1.18/1.59 alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (3769) {G4,W5,D3,L2,V0,M2} R(3702,35);r(154) { g( skol7 ) ==>
% 1.18/1.59 skol1, alpha6 }.
% 1.18/1.59 parent0: (4346) {G2,W5,D3,L2,V0,M2} { g( skol7 ) = skol1, alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4349) {G1,W6,D4,L2,V0,M2} { skol7 ==> f( g( skol7 ) ), alpha3 }.
% 1.18/1.59 parent0[0]: (259) {G1,W6,D4,L2,V0,M2} R(18,15) { f( g( skol7 ) ) ==> skol7
% 1.18/1.59 , alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 paramod: (4351) {G2,W6,D3,L3,V0,M3} { skol7 ==> f( skol1 ), alpha6, alpha3
% 1.18/1.59 }.
% 1.18/1.59 parent0[0]: (3769) {G4,W5,D3,L2,V0,M2} R(3702,35);r(154) { g( skol7 ) ==>
% 1.18/1.59 skol1, alpha6 }.
% 1.18/1.59 parent1[0; 3]: (4349) {G1,W6,D4,L2,V0,M2} { skol7 ==> f( g( skol7 ) ),
% 1.18/1.59 alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 paramod: (4352) {G3,W6,D2,L4,V0,M4} { skol7 ==> skol5, alpha6, alpha6,
% 1.18/1.59 alpha3 }.
% 1.18/1.59 parent0[0]: (3648) {G5,W5,D3,L2,V0,M2} P(3579,238);r(154) { f( skol1 ) ==>
% 1.18/1.59 skol5, alpha6 }.
% 1.18/1.59 parent1[0; 2]: (4351) {G2,W6,D3,L3,V0,M3} { skol7 ==> f( skol1 ), alpha6,
% 1.18/1.59 alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 factor: (4353) {G3,W5,D2,L3,V0,M3} { skol7 ==> skol5, alpha6, alpha3 }.
% 1.18/1.59 parent0[1, 2]: (4352) {G3,W6,D2,L4,V0,M4} { skol7 ==> skol5, alpha6,
% 1.18/1.59 alpha6, alpha3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4354) {G2,W5,D2,L3,V0,M3} { alpha6, skol7 ==> skol5, alpha6
% 1.18/1.59 }.
% 1.18/1.59 parent0[0]: (154) {G1,W2,D1,L2,V0,M2} P(0,13);q;r(2) { ! alpha3, alpha6 }.
% 1.18/1.59 parent1[2]: (4353) {G3,W5,D2,L3,V0,M3} { skol7 ==> skol5, alpha6, alpha3
% 1.18/1.59 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 factor: (4357) {G2,W4,D2,L2,V0,M2} { alpha6, skol7 ==> skol5 }.
% 1.18/1.59 parent0[0, 2]: (4354) {G2,W5,D2,L3,V0,M3} { alpha6, skol7 ==> skol5,
% 1.18/1.59 alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (3838) {G6,W4,D2,L2,V0,M2} P(3769,259);d(3648);r(154) { alpha6
% 1.18/1.59 , skol7 ==> skol5 }.
% 1.18/1.59 parent0: (4357) {G2,W4,D2,L2,V0,M2} { alpha6, skol7 ==> skol5 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 1 ==> 1
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4360) {G3,W2,D1,L2,V0,M2} { alpha6, alpha6 }.
% 1.18/1.59 parent0[1]: (171) {G2,W4,D2,L2,V0,M2} R(154,16) { alpha6, ! skol7 ==> skol5
% 1.18/1.59 }.
% 1.18/1.59 parent1[1]: (3838) {G6,W4,D2,L2,V0,M2} P(3769,259);d(3648);r(154) { alpha6
% 1.18/1.59 , skol7 ==> skol5 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 factor: (4361) {G3,W1,D1,L1,V0,M1} { alpha6 }.
% 1.18/1.59 parent0[0, 1]: (4360) {G3,W2,D1,L2,V0,M2} { alpha6, alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (3853) {G7,W1,D1,L1,V0,M1} S(3838);r(171) { alpha6 }.
% 1.18/1.59 parent0: (4361) {G3,W1,D1,L1,V0,M1} { alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4362) {G2,W7,D2,L3,V2,M3} { Y = X, ! alpha5( X, Y ), ! alpha6 }.
% 1.18/1.59 parent0[1]: (183) {G2,W7,D2,L3,V2,M3} R(14,22) { ! alpha5( X, Y ), X = Y, !
% 1.18/1.59 alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4363) {G3,W6,D2,L2,V2,M2} { X = Y, ! alpha5( Y, X ) }.
% 1.18/1.59 parent0[2]: (4362) {G2,W7,D2,L3,V2,M3} { Y = X, ! alpha5( X, Y ), ! alpha6
% 1.18/1.59 }.
% 1.18/1.59 parent1[0]: (3853) {G7,W1,D1,L1,V0,M1} S(3838);r(171) { alpha6 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := Y
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59 substitution1:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4364) {G3,W6,D2,L2,V2,M2} { Y = X, ! alpha5( Y, X ) }.
% 1.18/1.59 parent0[0]: (4363) {G3,W6,D2,L2,V2,M2} { X = Y, ! alpha5( Y, X ) }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := X
% 1.18/1.59 Y := Y
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 subsumption: (3867) {G8,W6,D2,L2,V2,M2} R(3853,183) { ! alpha5( X, Y ), X =
% 1.18/1.59 Y }.
% 1.18/1.59 parent0: (4364) {G3,W6,D2,L2,V2,M2} { Y = X, ! alpha5( Y, X ) }.
% 1.18/1.59 substitution0:
% 1.18/1.59 X := Y
% 1.18/1.59 Y := X
% 1.18/1.59 end
% 1.18/1.59 permutation0:
% 1.18/1.59 0 ==> 1
% 1.18/1.59 1 ==> 0
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 eqswap: (4365) {G4,W6,D4,L2,V0,M2} { skol3 ==> g( f( skol3 ) ), ! alpha6
% 1.18/1.59 }.
% 1.18/1.59 parent0[1]: (74) {G4,W6,D4,L2,V0,M2} R(72,8) { ! alpha6, g( f( skol3 ) )
% 1.18/1.59 ==> skol3 }.
% 1.18/1.59 substitution0:
% 1.18/1.59 end
% 1.18/1.59
% 1.18/1.59 resolution: (4366) {G5,W5,D4,L1,V0,M1} { skol3 ==> g( f( skol3 ) ) }.
% 1.18/1.59 parent0[1]: (4365) {G4,W6,D4,L2,V0,M2} { skol3 ==Cputime limit exceeded (core dumped)
%------------------------------------------------------------------------------