%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : KRS101+1 : TPTP v8.1.0. Released v3.1.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 : Sun Jul 17 02:42:14 EDT 2022
% Result : Unsatisfiable 1.30s 1.71s
% Output : Refutation 1.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : KRS101+1 : TPTP v8.1.0. Released v3.1.0.
% 0.03/0.12 % Command : bliksem %s
% 0.11/0.33 % Computer : n029.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % DateTime : Tue Jun 7 20:52:20 EDT 2022
% 0.11/0.33 % CPUTime :
% 1.30/1.70 *** allocated 10000 integers for termspace/termends
% 1.30/1.70 *** allocated 10000 integers for clauses
% 1.30/1.70 *** allocated 10000 integers for justifications
% 1.30/1.70 Bliksem 1.12
% 1.30/1.70
% 1.30/1.70
% 1.30/1.70 Automatic Strategy Selection
% 1.30/1.70
% 1.30/1.70
% 1.30/1.70 Clauses:
% 1.30/1.70
% 1.30/1.70 { ! Y = X, ! cUnsatisfiable( Y ), cUnsatisfiable( X ) }.
% 1.30/1.70 { ! Y = X, ! cc( Y ), cc( X ) }.
% 1.30/1.70 { ! Y = X, ! cd( Y ), cd( X ) }.
% 1.30/1.70 { ! Y = X, ! cowlNothing( Y ), cowlNothing( X ) }.
% 1.30/1.70 { ! Y = X, ! cowlThing( Y ), cowlThing( X ) }.
% 1.30/1.70 { ! Z = X, ! rr( Z, Y ), rr( X, Y ) }.
% 1.30/1.70 { ! Z = X, ! rr( Y, Z ), rr( Y, X ) }.
% 1.30/1.70 { ! Z = X, ! rs( Z, Y ), rs( X, Y ) }.
% 1.30/1.70 { ! Z = X, ! rs( Y, Z ), rs( Y, X ) }.
% 1.30/1.70 { ! Y = X, ! xsd_integer( Y ), xsd_integer( X ) }.
% 1.30/1.70 { ! Y = X, ! xsd_string( Y ), xsd_string( X ) }.
% 1.30/1.70 { cowlThing( X ) }.
% 1.30/1.70 { ! cowlNothing( X ) }.
% 1.30/1.70 { ! xsd_string( X ), ! xsd_integer( X ) }.
% 1.30/1.70 { xsd_integer( X ), xsd_string( X ) }.
% 1.30/1.70 { ! cUnsatisfiable( X ), alpha1( X ) }.
% 1.30/1.70 { ! cUnsatisfiable( X ), alpha2( X ) }.
% 1.30/1.70 { ! alpha1( X ), ! alpha2( X ), cUnsatisfiable( X ) }.
% 1.30/1.70 { ! alpha2( X ), alpha3( X ) }.
% 1.30/1.70 { ! alpha2( X ), alpha4( X ) }.
% 1.30/1.70 { ! alpha3( X ), ! alpha4( X ), alpha2( X ) }.
% 1.30/1.70 { ! alpha4( X ), alpha6( skol1( Y ) ) }.
% 1.30/1.70 { ! alpha4( X ), rr( X, skol1( X ) ) }.
% 1.30/1.70 { ! rr( X, Y ), ! alpha6( Y ), alpha4( X ) }.
% 1.30/1.70 { ! alpha6( X ), alpha8( X, skol2( X ), skol7( X ) ) }.
% 1.30/1.70 { ! alpha6( X ), ! skol2( X ) = skol7( X ) }.
% 1.30/1.70 { ! alpha8( X, Y, Z ), Y = Z, alpha6( X ) }.
% 1.30/1.70 { ! alpha8( X, Y, Z ), rs( X, Y ) }.
% 1.30/1.70 { ! alpha8( X, Y, Z ), rs( X, Z ) }.
% 1.30/1.70 { ! rs( X, Y ), ! rs( X, Z ), alpha8( X, Y, Z ) }.
% 1.30/1.70 { ! alpha3( X ), ! rr( X, Y ), alpha5( Y ) }.
% 1.30/1.70 { ! alpha5( skol3( Y ) ), alpha3( X ) }.
% 1.30/1.70 { rr( X, skol3( X ) ), alpha3( X ) }.
% 1.30/1.70 { ! alpha5( X ), alpha7( X ), cc( X ) }.
% 1.30/1.70 { ! alpha7( X ), alpha5( X ) }.
% 1.30/1.70 { ! cc( X ), alpha5( X ) }.
% 1.30/1.70 { ! alpha7( X ), ! rs( X, Y ), ! alpha9( X, Y ) }.
% 1.30/1.70 { rs( X, skol4( X ) ), alpha7( X ) }.
% 1.30/1.70 { alpha9( X, skol4( X ) ), alpha7( X ) }.
% 1.30/1.70 { ! alpha9( X, Y ), ! Y = skol5( Z, Y ) }.
% 1.30/1.70 { ! alpha9( X, Y ), rs( X, skol5( X, Y ) ) }.
% 1.30/1.70 { ! rs( X, Z ), Y = Z, alpha9( X, Y ) }.
% 1.30/1.70 { ! alpha1( X ), ! rr( X, Y ), cd( Y ) }.
% 1.30/1.70 { ! cd( skol6( Y ) ), alpha1( X ) }.
% 1.30/1.70 { rr( X, skol6( X ) ), alpha1( X ) }.
% 1.30/1.70 { ! cc( X ), ! cd( X ) }.
% 1.30/1.70 { cUnsatisfiable( i2003_11_14_17_20_36582 ) }.
% 1.30/1.70
% 1.30/1.70 percentage equality = 0.133929, percentage horn = 0.829787
% 1.30/1.70 This is a problem with some equality
% 1.30/1.70
% 1.30/1.70
% 1.30/1.70
% 1.30/1.70 Options Used:
% 1.30/1.70
% 1.30/1.70 useres = 1
% 1.30/1.70 useparamod = 1
% 1.30/1.70 useeqrefl = 1
% 1.30/1.70 useeqfact = 1
% 1.30/1.70 usefactor = 1
% 1.30/1.70 usesimpsplitting = 0
% 1.30/1.70 usesimpdemod = 5
% 1.30/1.70 usesimpres = 3
% 1.30/1.70
% 1.30/1.70 resimpinuse = 1000
% 1.30/1.70 resimpclauses = 20000
% 1.30/1.70 substype = eqrewr
% 1.30/1.70 backwardsubs = 1
% 1.30/1.70 selectoldest = 5
% 1.30/1.70
% 1.30/1.70 litorderings [0] = split
% 1.30/1.70 litorderings [1] = extend the termordering, first sorting on arguments
% 1.30/1.70
% 1.30/1.70 termordering = kbo
% 1.30/1.70
% 1.30/1.70 litapriori = 0
% 1.30/1.70 termapriori = 1
% 1.30/1.70 litaposteriori = 0
% 1.30/1.70 termaposteriori = 0
% 1.30/1.70 demodaposteriori = 0
% 1.30/1.70 ordereqreflfact = 0
% 1.30/1.70
% 1.30/1.70 litselect = negord
% 1.30/1.70
% 1.30/1.70 maxweight = 15
% 1.30/1.70 maxdepth = 30000
% 1.30/1.70 maxlength = 115
% 1.30/1.70 maxnrvars = 195
% 1.30/1.70 excuselevel = 1
% 1.30/1.70 increasemaxweight = 1
% 1.30/1.70
% 1.30/1.70 maxselected = 10000000
% 1.30/1.70 maxnrclauses = 10000000
% 1.30/1.70
% 1.30/1.70 showgenerated = 0
% 1.30/1.70 showkept = 0
% 1.30/1.70 showselected = 0
% 1.30/1.71 showdeleted = 0
% 1.30/1.71 showresimp = 1
% 1.30/1.71 showstatus = 2000
% 1.30/1.71
% 1.30/1.71 prologoutput = 0
% 1.30/1.71 nrgoals = 5000000
% 1.30/1.71 totalproof = 1
% 1.30/1.71
% 1.30/1.71 Symbols occurring in the translation:
% 1.30/1.71
% 1.30/1.71 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 1.30/1.71 . [1, 2] (w:1, o:39, a:1, s:1, b:0),
% 1.30/1.71 ! [4, 1] (w:0, o:14, a:1, s:1, b:0),
% 1.30/1.71 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.30/1.71 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 1.30/1.71 cUnsatisfiable [37, 1] (w:1, o:19, a:1, s:1, b:0),
% 1.30/1.71 cc [38, 1] (w:1, o:20, a:1, s:1, b:0),
% 1.30/1.71 cd [39, 1] (w:1, o:21, a:1, s:1, b:0),
% 1.30/1.71 cowlNothing [40, 1] (w:1, o:22, a:1, s:1, b:0),
% 1.30/1.71 cowlThing [41, 1] (w:1, o:23, a:1, s:1, b:0),
% 1.30/1.71 rr [43, 2] (w:1, o:63, a:1, s:1, b:0),
% 1.30/1.71 rs [44, 2] (w:1, o:64, a:1, s:1, b:0),
% 1.30/1.71 xsd_integer [45, 1] (w:1, o:24, a:1, s:1, b:0),
% 1.30/1.71 xsd_string [46, 1] (w:1, o:25, a:1, s:1, b:0),
% 1.30/1.71 i2003_11_14_17_20_36582 [51, 0] (w:1, o:13, a:1, s:1, b:0),
% 1.30/1.71 alpha1 [52, 1] (w:1, o:26, a:1, s:1, b:1),
% 1.30/1.71 alpha2 [53, 1] (w:1, o:27, a:1, s:1, b:1),
% 1.30/1.71 alpha3 [54, 1] (w:1, o:28, a:1, s:1, b:1),
% 1.30/1.71 alpha4 [55, 1] (w:1, o:29, a:1, s:1, b:1),
% 1.30/1.71 alpha5 [56, 1] (w:1, o:30, a:1, s:1, b:1),
% 1.30/1.71 alpha6 [57, 1] (w:1, o:31, a:1, s:1, b:1),
% 1.30/1.71 alpha7 [58, 1] (w:1, o:32, a:1, s:1, b:1),
% 1.30/1.71 alpha8 [59, 3] (w:1, o:67, a:1, s:1, b:1),
% 1.30/1.71 alpha9 [60, 2] (w:1, o:65, a:1, s:1, b:1),
% 1.30/1.71 skol1 [61, 1] (w:1, o:33, a:1, s:1, b:1),
% 1.30/1.71 skol2 [62, 1] (w:1, o:34, a:1, s:1, b:1),
% 1.30/1.71 skol3 [63, 1] (w:1, o:35, a:1, s:1, b:1),
% 1.30/1.71 skol4 [64, 1] (w:1, o:36, a:1, s:1, b:1),
% 1.30/1.71 skol5 [65, 2] (w:1, o:66, a:1, s:1, b:1),
% 1.30/1.71 skol6 [66, 1] (w:1, o:37, a:1, s:1, b:1),
% 1.30/1.71 skol7 [67, 1] (w:1, o:38, a:1, s:1, b:1).
% 1.30/1.71
% 1.30/1.71
% 1.30/1.71 Starting Search:
% 1.30/1.71
% 1.30/1.71 *** allocated 15000 integers for clauses
% 1.30/1.71 *** allocated 22500 integers for clauses
% 1.30/1.71 *** allocated 33750 integers for clauses
% 1.30/1.71 *** allocated 15000 integers for termspace/termends
% 1.30/1.71 *** allocated 50625 integers for clauses
% 1.30/1.71 Resimplifying inuse:
% 1.30/1.71 Done
% 1.30/1.71
% 1.30/1.71 *** allocated 22500 integers for termspace/termends
% 1.30/1.71 *** allocated 75937 integers for clauses
% 1.30/1.71 *** allocated 33750 integers for termspace/termends
% 1.30/1.71
% 1.30/1.71 Intermediate Status:
% 1.30/1.71 Generated: 5718
% 1.30/1.71 Kept: 2003
% 1.30/1.71 Inuse: 214
% 1.30/1.71 Deleted: 7
% 1.30/1.71 Deletedinuse: 1
% 1.30/1.71
% 1.30/1.71 Resimplifying inuse:
% 1.30/1.71 Done
% 1.30/1.71
% 1.30/1.71 *** allocated 113905 integers for clauses
% 1.30/1.71 *** allocated 50625 integers for termspace/termends
% 1.30/1.71 Resimplifying inuse:
% 1.30/1.71 Done
% 1.30/1.71
% 1.30/1.71 *** allocated 170857 integers for clauses
% 1.30/1.71 *** allocated 75937 integers for termspace/termends
% 1.30/1.71
% 1.30/1.71 Intermediate Status:
% 1.30/1.71 Generated: 11927
% 1.30/1.71 Kept: 4005
% 1.30/1.71 Inuse: 338
% 1.30/1.71 Deleted: 9
% 1.30/1.71 Deletedinuse: 1
% 1.30/1.71
% 1.30/1.71 Resimplifying inuse:
% 1.30/1.71 Done
% 1.30/1.71
% 1.30/1.71 *** allocated 256285 integers for clauses
% 1.30/1.71 Resimplifying inuse:
% 1.30/1.71 Done
% 1.30/1.71
% 1.30/1.71 *** allocated 113905 integers for termspace/termends
% 1.30/1.71
% 1.30/1.71 Intermediate Status:
% 1.30/1.71 Generated: 19027
% 1.30/1.71 Kept: 6022
% 1.30/1.71 Inuse: 421
% 1.30/1.71 Deleted: 17
% 1.30/1.71 Deletedinuse: 1
% 1.30/1.71
% 1.30/1.71 Resimplifying inuse:
% 1.30/1.71 Done
% 1.30/1.71
% 1.30/1.71 Resimplifying inuse:
% 1.30/1.71 Done
% 1.30/1.71
% 1.30/1.71 *** allocated 384427 integers for clauses
% 1.30/1.71 *** allocated 170857 integers for termspace/termends
% 1.30/1.71
% 1.30/1.71 Intermediate Status:
% 1.30/1.71 Generated: 26259
% 1.30/1.71 Kept: 8237
% 1.30/1.71 Inuse: 480
% 1.30/1.71 Deleted: 18
% 1.30/1.71 Deletedinuse: 2
% 1.30/1.71
% 1.30/1.71 Resimplifying inuse:
% 1.30/1.71 Done
% 1.30/1.71
% 1.30/1.71 Resimplifying inuse:
% 1.30/1.71 Done
% 1.30/1.71
% 1.30/1.71
% 1.30/1.71 Intermediate Status:
% 1.30/1.71 Generated: 32486
% 1.30/1.71 Kept: 10384
% 1.30/1.71 Inuse: 514
% 1.30/1.71 Deleted: 18
% 1.30/1.71 Deletedinuse: 2
% 1.30/1.71
% 1.30/1.71 Resimplifying inuse:
% 1.30/1.71
% 1.30/1.71 Bliksems!, er is een bewijs:
% 1.30/1.71 % SZS status Unsatisfiable
% 1.30/1.71 % SZS output start Refutation
% 1.30/1.71
% 1.30/1.71 (15) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha1( X ) }.
% 1.30/1.71 (16) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha2( X ) }.
% 1.30/1.71 (18) {G0,W4,D2,L2,V1,M2} I { ! alpha2( X ), alpha3( X ) }.
% 1.30/1.71 (19) {G0,W4,D2,L2,V1,M2} I { ! alpha2( X ), alpha4( X ) }.
% 1.30/1.71 (21) {G0,W5,D3,L2,V2,M2} I { ! alpha4( X ), alpha6( skol1( Y ) ) }.
% 1.30/1.71 (22) {G0,W6,D3,L2,V1,M2} I { ! alpha4( X ), rr( X, skol1( X ) ) }.
% 1.30/1.71 (24) {G0,W8,D3,L2,V1,M2} I { ! alpha6( X ), alpha8( X, skol2( X ), skol7( X
% 1.30/1.71 ) ) }.
% 1.30/1.71 (25) {G0,W7,D3,L2,V1,M2} I { ! alpha6( X ), ! skol7( X ) ==> skol2( X ) }.
% 1.30/1.71 (27) {G0,W7,D2,L2,V3,M2} I { ! alpha8( X, Y, Z ), rs( X, Y ) }.
% 1.30/1.71 (28) {G0,W7,D2,L2,V3,M2} I { ! alpha8( X, Y, Z ), rs( X, Z ) }.
% 1.30/1.71 (30) {G0,W7,D2,L3,V2,M3} I { ! alpha3( X ), ! rr( X, Y ), alpha5( Y ) }.
% 1.30/1.71 (33) {G0,W6,D2,L3,V1,M3} I { ! alpha5( X ), alpha7( X ), cc( X ) }.
% 1.30/1.71 (36) {G0,W8,D2,L3,V2,M3} I { ! alpha7( X ), ! rs( X, Y ), ! alpha9( X, Y )
% 1.30/1.71 }.
% 1.30/1.71 (41) {G0,W9,D2,L3,V3,M3} I { ! rs( X, Z ), Y = Z, alpha9( X, Y ) }.
% 1.30/1.71 (42) {G0,W7,D2,L3,V2,M3} I { ! alpha1( X ), ! rr( X, Y ), cd( Y ) }.
% 1.30/1.71 (45) {G0,W4,D2,L2,V1,M2} I { ! cc( X ), ! cd( X ) }.
% 1.30/1.71 (46) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable( i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 (53) {G1,W2,D2,L1,V0,M1} R(16,46) { alpha2( i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 (57) {G2,W2,D2,L1,V0,M1} R(53,18) { alpha3( i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 (58) {G2,W2,D2,L1,V0,M1} R(53,19) { alpha4( i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 (63) {G1,W2,D2,L1,V0,M1} R(15,46) { alpha1( i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 (76) {G3,W3,D3,L1,V1,M1} R(21,58) { alpha6( skol1( X ) ) }.
% 1.30/1.71 (81) {G1,W6,D2,L3,V1,M3} R(33,45) { ! alpha5( X ), alpha7( X ), ! cd( X )
% 1.30/1.71 }.
% 1.30/1.71 (114) {G3,W4,D3,L1,V0,M1} R(22,58) { rr( i2003_11_14_17_20_36582, skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 (153) {G1,W6,D3,L2,V1,M2} R(24,27) { ! alpha6( X ), rs( X, skol2( X ) ) }.
% 1.30/1.71 (154) {G1,W6,D3,L2,V1,M2} R(24,28) { ! alpha6( X ), rs( X, skol7( X ) ) }.
% 1.30/1.71 (159) {G4,W6,D4,L1,V1,M1} R(153,76) { rs( skol1( X ), skol2( skol1( X ) ) )
% 1.30/1.71 }.
% 1.30/1.71 (163) {G4,W6,D4,L1,V1,M1} R(154,76) { rs( skol1( X ), skol7( skol1( X ) ) )
% 1.30/1.71 }.
% 1.30/1.71 (170) {G4,W7,D4,L1,V1,M1} R(25,76) { ! skol7( skol1( X ) ) ==> skol2( skol1
% 1.30/1.71 ( X ) ) }.
% 1.30/1.71 (266) {G4,W3,D3,L1,V0,M1} R(42,114);r(63) { cd( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 (344) {G4,W3,D3,L1,V0,M1} R(30,114);r(57) { alpha5( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 (360) {G5,W3,D3,L1,V0,M1} R(344,81);r(266) { alpha7( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 (371) {G6,W8,D3,L2,V1,M2} R(36,360) { ! rs( skol1( i2003_11_14_17_20_36582
% 1.30/1.71 ), X ), ! alpha9( skol1( i2003_11_14_17_20_36582 ), X ) }.
% 1.30/1.71 (468) {G2,W9,D3,L3,V2,M3} R(41,154) { X = skol7( Y ), alpha9( Y, X ), !
% 1.30/1.71 alpha6( Y ) }.
% 1.30/1.71 (1580) {G7,W6,D4,L1,V0,M1} R(371,159) { ! alpha9( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), skol2( skol1( i2003_11_14_17_20_36582 ) ) )
% 1.30/1.71 }.
% 1.30/1.71 (1581) {G7,W6,D4,L1,V0,M1} R(371,163) { ! alpha9( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), skol7( skol1( i2003_11_14_17_20_36582 ) ) )
% 1.30/1.71 }.
% 1.30/1.71 (10058) {G8,W7,D4,L1,V0,M1} R(468,1580);r(76) { skol7( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) ==> skol2( skol1( i2003_11_14_17_20_36582 ) )
% 1.30/1.71 }.
% 1.30/1.71 (10334) {G5,W9,D4,L2,V2,M2} P(468,170);r(76) { ! Y = skol2( skol1( X ) ),
% 1.30/1.71 alpha9( skol1( X ), Y ) }.
% 1.30/1.71 (10376) {G6,W6,D4,L1,V1,M1} Q(10334) { alpha9( skol1( X ), skol2( skol1( X
% 1.30/1.71 ) ) ) }.
% 1.30/1.71 (10390) {G9,W0,D0,L0,V0,M0} S(1581);d(10058);r(10376) { }.
% 1.30/1.71
% 1.30/1.71
% 1.30/1.71 % SZS output end Refutation
% 1.30/1.71 found a proof!
% 1.30/1.71
% 1.30/1.71
% 1.30/1.71 Unprocessed initial clauses:
% 1.30/1.71
% 1.30/1.71 (10392) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cUnsatisfiable( Y ),
% 1.30/1.71 cUnsatisfiable( X ) }.
% 1.30/1.71 (10393) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cc( Y ), cc( X ) }.
% 1.30/1.71 (10394) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cd( Y ), cd( X ) }.
% 1.30/1.71 (10395) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cowlNothing( Y ), cowlNothing( X
% 1.30/1.71 ) }.
% 1.30/1.71 (10396) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cowlThing( Y ), cowlThing( X )
% 1.30/1.71 }.
% 1.30/1.71 (10397) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rr( Z, Y ), rr( X, Y ) }.
% 1.30/1.71 (10398) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rr( Y, Z ), rr( Y, X ) }.
% 1.30/1.71 (10399) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rs( Z, Y ), rs( X, Y ) }.
% 1.30/1.71 (10400) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rs( Y, Z ), rs( Y, X ) }.
% 1.30/1.71 (10401) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! xsd_integer( Y ), xsd_integer( X
% 1.30/1.71 ) }.
% 1.30/1.71 (10402) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! xsd_string( Y ), xsd_string( X )
% 1.30/1.71 }.
% 1.30/1.71 (10403) {G0,W2,D2,L1,V1,M1} { cowlThing( X ) }.
% 1.30/1.71 (10404) {G0,W2,D2,L1,V1,M1} { ! cowlNothing( X ) }.
% 1.30/1.71 (10405) {G0,W4,D2,L2,V1,M2} { ! xsd_string( X ), ! xsd_integer( X ) }.
% 1.30/1.71 (10406) {G0,W4,D2,L2,V1,M2} { xsd_integer( X ), xsd_string( X ) }.
% 1.30/1.71 (10407) {G0,W4,D2,L2,V1,M2} { ! cUnsatisfiable( X ), alpha1( X ) }.
% 1.30/1.71 (10408) {G0,W4,D2,L2,V1,M2} { ! cUnsatisfiable( X ), alpha2( X ) }.
% 1.30/1.71 (10409) {G0,W6,D2,L3,V1,M3} { ! alpha1( X ), ! alpha2( X ), cUnsatisfiable
% 1.30/1.71 ( X ) }.
% 1.30/1.71 (10410) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), alpha3( X ) }.
% 1.30/1.71 (10411) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), alpha4( X ) }.
% 1.30/1.71 (10412) {G0,W6,D2,L3,V1,M3} { ! alpha3( X ), ! alpha4( X ), alpha2( X )
% 1.30/1.71 }.
% 1.30/1.71 (10413) {G0,W5,D3,L2,V2,M2} { ! alpha4( X ), alpha6( skol1( Y ) ) }.
% 1.30/1.71 (10414) {G0,W6,D3,L2,V1,M2} { ! alpha4( X ), rr( X, skol1( X ) ) }.
% 1.30/1.71 (10415) {G0,W7,D2,L3,V2,M3} { ! rr( X, Y ), ! alpha6( Y ), alpha4( X ) }.
% 1.30/1.71 (10416) {G0,W8,D3,L2,V1,M2} { ! alpha6( X ), alpha8( X, skol2( X ), skol7
% 1.30/1.71 ( X ) ) }.
% 1.30/1.71 (10417) {G0,W7,D3,L2,V1,M2} { ! alpha6( X ), ! skol2( X ) = skol7( X ) }.
% 1.30/1.71 (10418) {G0,W9,D2,L3,V3,M3} { ! alpha8( X, Y, Z ), Y = Z, alpha6( X ) }.
% 1.30/1.71 (10419) {G0,W7,D2,L2,V3,M2} { ! alpha8( X, Y, Z ), rs( X, Y ) }.
% 1.30/1.71 (10420) {G0,W7,D2,L2,V3,M2} { ! alpha8( X, Y, Z ), rs( X, Z ) }.
% 1.30/1.71 (10421) {G0,W10,D2,L3,V3,M3} { ! rs( X, Y ), ! rs( X, Z ), alpha8( X, Y, Z
% 1.30/1.71 ) }.
% 1.30/1.71 (10422) {G0,W7,D2,L3,V2,M3} { ! alpha3( X ), ! rr( X, Y ), alpha5( Y ) }.
% 1.30/1.71 (10423) {G0,W5,D3,L2,V2,M2} { ! alpha5( skol3( Y ) ), alpha3( X ) }.
% 1.30/1.71 (10424) {G0,W6,D3,L2,V1,M2} { rr( X, skol3( X ) ), alpha3( X ) }.
% 1.30/1.71 (10425) {G0,W6,D2,L3,V1,M3} { ! alpha5( X ), alpha7( X ), cc( X ) }.
% 1.30/1.71 (10426) {G0,W4,D2,L2,V1,M2} { ! alpha7( X ), alpha5( X ) }.
% 1.30/1.71 (10427) {G0,W4,D2,L2,V1,M2} { ! cc( X ), alpha5( X ) }.
% 1.30/1.71 (10428) {G0,W8,D2,L3,V2,M3} { ! alpha7( X ), ! rs( X, Y ), ! alpha9( X, Y
% 1.30/1.71 ) }.
% 1.30/1.71 (10429) {G0,W6,D3,L2,V1,M2} { rs( X, skol4( X ) ), alpha7( X ) }.
% 1.30/1.71 (10430) {G0,W6,D3,L2,V1,M2} { alpha9( X, skol4( X ) ), alpha7( X ) }.
% 1.30/1.71 (10431) {G0,W8,D3,L2,V3,M2} { ! alpha9( X, Y ), ! Y = skol5( Z, Y ) }.
% 1.30/1.71 (10432) {G0,W8,D3,L2,V2,M2} { ! alpha9( X, Y ), rs( X, skol5( X, Y ) ) }.
% 1.30/1.71 (10433) {G0,W9,D2,L3,V3,M3} { ! rs( X, Z ), Y = Z, alpha9( X, Y ) }.
% 1.30/1.71 (10434) {G0,W7,D2,L3,V2,M3} { ! alpha1( X ), ! rr( X, Y ), cd( Y ) }.
% 1.30/1.71 (10435) {G0,W5,D3,L2,V2,M2} { ! cd( skol6( Y ) ), alpha1( X ) }.
% 1.30/1.71 (10436) {G0,W6,D3,L2,V1,M2} { rr( X, skol6( X ) ), alpha1( X ) }.
% 1.30/1.71 (10437) {G0,W4,D2,L2,V1,M2} { ! cc( X ), ! cd( X ) }.
% 1.30/1.71 (10438) {G0,W2,D2,L1,V0,M1} { cUnsatisfiable( i2003_11_14_17_20_36582 )
% 1.30/1.71 }.
% 1.30/1.71
% 1.30/1.71
% 1.30/1.71 Total Proof:
% 1.30/1.71
% 1.30/1.71 subsumption: (15) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha1( X
% 1.30/1.71 ) }.
% 1.30/1.71 parent0: (10407) {G0,W4,D2,L2,V1,M2} { ! cUnsatisfiable( X ), alpha1( X )
% 1.30/1.71 }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (16) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha2( X
% 1.30/1.71 ) }.
% 1.30/1.71 parent0: (10408) {G0,W4,D2,L2,V1,M2} { ! cUnsatisfiable( X ), alpha2( X )
% 1.30/1.71 }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (18) {G0,W4,D2,L2,V1,M2} I { ! alpha2( X ), alpha3( X ) }.
% 1.30/1.71 parent0: (10410) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), alpha3( X ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (19) {G0,W4,D2,L2,V1,M2} I { ! alpha2( X ), alpha4( X ) }.
% 1.30/1.71 parent0: (10411) {G0,W4,D2,L2,V1,M2} { ! alpha2( X ), alpha4( X ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (21) {G0,W5,D3,L2,V2,M2} I { ! alpha4( X ), alpha6( skol1( Y )
% 1.30/1.71 ) }.
% 1.30/1.71 parent0: (10413) {G0,W5,D3,L2,V2,M2} { ! alpha4( X ), alpha6( skol1( Y ) )
% 1.30/1.71 }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 Y := Y
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (22) {G0,W6,D3,L2,V1,M2} I { ! alpha4( X ), rr( X, skol1( X )
% 1.30/1.71 ) }.
% 1.30/1.71 parent0: (10414) {G0,W6,D3,L2,V1,M2} { ! alpha4( X ), rr( X, skol1( X ) )
% 1.30/1.71 }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (24) {G0,W8,D3,L2,V1,M2} I { ! alpha6( X ), alpha8( X, skol2(
% 1.30/1.71 X ), skol7( X ) ) }.
% 1.30/1.71 parent0: (10416) {G0,W8,D3,L2,V1,M2} { ! alpha6( X ), alpha8( X, skol2( X
% 1.30/1.71 ), skol7( X ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 eqswap: (10527) {G0,W7,D3,L2,V1,M2} { ! skol7( X ) = skol2( X ), ! alpha6
% 1.30/1.71 ( X ) }.
% 1.30/1.71 parent0[1]: (10417) {G0,W7,D3,L2,V1,M2} { ! alpha6( X ), ! skol2( X ) =
% 1.30/1.71 skol7( X ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (25) {G0,W7,D3,L2,V1,M2} I { ! alpha6( X ), ! skol7( X ) ==>
% 1.30/1.71 skol2( X ) }.
% 1.30/1.71 parent0: (10527) {G0,W7,D3,L2,V1,M2} { ! skol7( X ) = skol2( X ), ! alpha6
% 1.30/1.71 ( X ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 1
% 1.30/1.71 1 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (27) {G0,W7,D2,L2,V3,M2} I { ! alpha8( X, Y, Z ), rs( X, Y )
% 1.30/1.71 }.
% 1.30/1.71 parent0: (10419) {G0,W7,D2,L2,V3,M2} { ! alpha8( X, Y, Z ), rs( X, Y ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 Y := Y
% 1.30/1.71 Z := Z
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (28) {G0,W7,D2,L2,V3,M2} I { ! alpha8( X, Y, Z ), rs( X, Z )
% 1.30/1.71 }.
% 1.30/1.71 parent0: (10420) {G0,W7,D2,L2,V3,M2} { ! alpha8( X, Y, Z ), rs( X, Z ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 Y := Y
% 1.30/1.71 Z := Z
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (30) {G0,W7,D2,L3,V2,M3} I { ! alpha3( X ), ! rr( X, Y ),
% 1.30/1.71 alpha5( Y ) }.
% 1.30/1.71 parent0: (10422) {G0,W7,D2,L3,V2,M3} { ! alpha3( X ), ! rr( X, Y ), alpha5
% 1.30/1.71 ( Y ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 Y := Y
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 2 ==> 2
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (33) {G0,W6,D2,L3,V1,M3} I { ! alpha5( X ), alpha7( X ), cc( X
% 1.30/1.71 ) }.
% 1.30/1.71 parent0: (10425) {G0,W6,D2,L3,V1,M3} { ! alpha5( X ), alpha7( X ), cc( X )
% 1.30/1.71 }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 2 ==> 2
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (36) {G0,W8,D2,L3,V2,M3} I { ! alpha7( X ), ! rs( X, Y ), !
% 1.30/1.71 alpha9( X, Y ) }.
% 1.30/1.71 parent0: (10428) {G0,W8,D2,L3,V2,M3} { ! alpha7( X ), ! rs( X, Y ), !
% 1.30/1.71 alpha9( X, Y ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 Y := Y
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 2 ==> 2
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (41) {G0,W9,D2,L3,V3,M3} I { ! rs( X, Z ), Y = Z, alpha9( X, Y
% 1.30/1.71 ) }.
% 1.30/1.71 parent0: (10433) {G0,W9,D2,L3,V3,M3} { ! rs( X, Z ), Y = Z, alpha9( X, Y )
% 1.30/1.71 }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 Y := Y
% 1.30/1.71 Z := Z
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 2 ==> 2
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (42) {G0,W7,D2,L3,V2,M3} I { ! alpha1( X ), ! rr( X, Y ), cd(
% 1.30/1.71 Y ) }.
% 1.30/1.71 parent0: (10434) {G0,W7,D2,L3,V2,M3} { ! alpha1( X ), ! rr( X, Y ), cd( Y
% 1.30/1.71 ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 Y := Y
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 2 ==> 2
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (45) {G0,W4,D2,L2,V1,M2} I { ! cc( X ), ! cd( X ) }.
% 1.30/1.71 parent0: (10437) {G0,W4,D2,L2,V1,M2} { ! cc( X ), ! cd( X ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (46) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable(
% 1.30/1.71 i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 parent0: (10438) {G0,W2,D2,L1,V0,M1} { cUnsatisfiable(
% 1.30/1.71 i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10660) {G1,W2,D2,L1,V0,M1} { alpha2( i2003_11_14_17_20_36582
% 1.30/1.71 ) }.
% 1.30/1.71 parent0[0]: (16) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha2( X )
% 1.30/1.71 }.
% 1.30/1.71 parent1[0]: (46) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable(
% 1.30/1.71 i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := i2003_11_14_17_20_36582
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (53) {G1,W2,D2,L1,V0,M1} R(16,46) { alpha2(
% 1.30/1.71 i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 parent0: (10660) {G1,W2,D2,L1,V0,M1} { alpha2( i2003_11_14_17_20_36582 )
% 1.30/1.71 }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10661) {G1,W2,D2,L1,V0,M1} { alpha3( i2003_11_14_17_20_36582
% 1.30/1.71 ) }.
% 1.30/1.71 parent0[0]: (18) {G0,W4,D2,L2,V1,M2} I { ! alpha2( X ), alpha3( X ) }.
% 1.30/1.71 parent1[0]: (53) {G1,W2,D2,L1,V0,M1} R(16,46) { alpha2(
% 1.30/1.71 i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := i2003_11_14_17_20_36582
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (57) {G2,W2,D2,L1,V0,M1} R(53,18) { alpha3(
% 1.30/1.71 i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 parent0: (10661) {G1,W2,D2,L1,V0,M1} { alpha3( i2003_11_14_17_20_36582 )
% 1.30/1.71 }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10662) {G1,W2,D2,L1,V0,M1} { alpha4( i2003_11_14_17_20_36582
% 1.30/1.71 ) }.
% 1.30/1.71 parent0[0]: (19) {G0,W4,D2,L2,V1,M2} I { ! alpha2( X ), alpha4( X ) }.
% 1.30/1.71 parent1[0]: (53) {G1,W2,D2,L1,V0,M1} R(16,46) { alpha2(
% 1.30/1.71 i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := i2003_11_14_17_20_36582
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (58) {G2,W2,D2,L1,V0,M1} R(53,19) { alpha4(
% 1.30/1.71 i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 parent0: (10662) {G1,W2,D2,L1,V0,M1} { alpha4( i2003_11_14_17_20_36582 )
% 1.30/1.71 }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10663) {G1,W2,D2,L1,V0,M1} { alpha1( i2003_11_14_17_20_36582
% 1.30/1.71 ) }.
% 1.30/1.71 parent0[0]: (15) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha1( X )
% 1.30/1.71 }.
% 1.30/1.71 parent1[0]: (46) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable(
% 1.30/1.71 i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := i2003_11_14_17_20_36582
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (63) {G1,W2,D2,L1,V0,M1} R(15,46) { alpha1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 parent0: (10663) {G1,W2,D2,L1,V0,M1} { alpha1( i2003_11_14_17_20_36582 )
% 1.30/1.71 }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10664) {G1,W3,D3,L1,V1,M1} { alpha6( skol1( X ) ) }.
% 1.30/1.71 parent0[0]: (21) {G0,W5,D3,L2,V2,M2} I { ! alpha4( X ), alpha6( skol1( Y )
% 1.30/1.71 ) }.
% 1.30/1.71 parent1[0]: (58) {G2,W2,D2,L1,V0,M1} R(53,19) { alpha4(
% 1.30/1.71 i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := i2003_11_14_17_20_36582
% 1.30/1.71 Y := X
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (76) {G3,W3,D3,L1,V1,M1} R(21,58) { alpha6( skol1( X ) ) }.
% 1.30/1.71 parent0: (10664) {G1,W3,D3,L1,V1,M1} { alpha6( skol1( X ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10665) {G1,W6,D2,L3,V1,M3} { ! cd( X ), ! alpha5( X ), alpha7
% 1.30/1.71 ( X ) }.
% 1.30/1.71 parent0[0]: (45) {G0,W4,D2,L2,V1,M2} I { ! cc( X ), ! cd( X ) }.
% 1.30/1.71 parent1[2]: (33) {G0,W6,D2,L3,V1,M3} I { ! alpha5( X ), alpha7( X ), cc( X
% 1.30/1.71 ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (81) {G1,W6,D2,L3,V1,M3} R(33,45) { ! alpha5( X ), alpha7( X )
% 1.30/1.71 , ! cd( X ) }.
% 1.30/1.71 parent0: (10665) {G1,W6,D2,L3,V1,M3} { ! cd( X ), ! alpha5( X ), alpha7( X
% 1.30/1.71 ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 2
% 1.30/1.71 1 ==> 0
% 1.30/1.71 2 ==> 1
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10666) {G1,W4,D3,L1,V0,M1} { rr( i2003_11_14_17_20_36582,
% 1.30/1.71 skol1( i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 parent0[0]: (22) {G0,W6,D3,L2,V1,M2} I { ! alpha4( X ), rr( X, skol1( X ) )
% 1.30/1.71 }.
% 1.30/1.71 parent1[0]: (58) {G2,W2,D2,L1,V0,M1} R(53,19) { alpha4(
% 1.30/1.71 i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := i2003_11_14_17_20_36582
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (114) {G3,W4,D3,L1,V0,M1} R(22,58) { rr(
% 1.30/1.71 i2003_11_14_17_20_36582, skol1( i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 parent0: (10666) {G1,W4,D3,L1,V0,M1} { rr( i2003_11_14_17_20_36582, skol1
% 1.30/1.71 ( i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10667) {G1,W6,D3,L2,V1,M2} { rs( X, skol2( X ) ), ! alpha6( X
% 1.30/1.71 ) }.
% 1.30/1.71 parent0[0]: (27) {G0,W7,D2,L2,V3,M2} I { ! alpha8( X, Y, Z ), rs( X, Y )
% 1.30/1.71 }.
% 1.30/1.71 parent1[1]: (24) {G0,W8,D3,L2,V1,M2} I { ! alpha6( X ), alpha8( X, skol2( X
% 1.30/1.71 ), skol7( X ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 Y := skol2( X )
% 1.30/1.71 Z := skol7( X )
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (153) {G1,W6,D3,L2,V1,M2} R(24,27) { ! alpha6( X ), rs( X,
% 1.30/1.71 skol2( X ) ) }.
% 1.30/1.71 parent0: (10667) {G1,W6,D3,L2,V1,M2} { rs( X, skol2( X ) ), ! alpha6( X )
% 1.30/1.71 }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 1
% 1.30/1.71 1 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10668) {G1,W6,D3,L2,V1,M2} { rs( X, skol7( X ) ), ! alpha6( X
% 1.30/1.71 ) }.
% 1.30/1.71 parent0[0]: (28) {G0,W7,D2,L2,V3,M2} I { ! alpha8( X, Y, Z ), rs( X, Z )
% 1.30/1.71 }.
% 1.30/1.71 parent1[1]: (24) {G0,W8,D3,L2,V1,M2} I { ! alpha6( X ), alpha8( X, skol2( X
% 1.30/1.71 ), skol7( X ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 Y := skol2( X )
% 1.30/1.71 Z := skol7( X )
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (154) {G1,W6,D3,L2,V1,M2} R(24,28) { ! alpha6( X ), rs( X,
% 1.30/1.71 skol7( X ) ) }.
% 1.30/1.71 parent0: (10668) {G1,W6,D3,L2,V1,M2} { rs( X, skol7( X ) ), ! alpha6( X )
% 1.30/1.71 }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 1
% 1.30/1.71 1 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10669) {G2,W6,D4,L1,V1,M1} { rs( skol1( X ), skol2( skol1( X
% 1.30/1.71 ) ) ) }.
% 1.30/1.71 parent0[0]: (153) {G1,W6,D3,L2,V1,M2} R(24,27) { ! alpha6( X ), rs( X,
% 1.30/1.71 skol2( X ) ) }.
% 1.30/1.71 parent1[0]: (76) {G3,W3,D3,L1,V1,M1} R(21,58) { alpha6( skol1( X ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := skol1( X )
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (159) {G4,W6,D4,L1,V1,M1} R(153,76) { rs( skol1( X ), skol2(
% 1.30/1.71 skol1( X ) ) ) }.
% 1.30/1.71 parent0: (10669) {G2,W6,D4,L1,V1,M1} { rs( skol1( X ), skol2( skol1( X ) )
% 1.30/1.71 ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10670) {G2,W6,D4,L1,V1,M1} { rs( skol1( X ), skol7( skol1( X
% 1.30/1.71 ) ) ) }.
% 1.30/1.71 parent0[0]: (154) {G1,W6,D3,L2,V1,M2} R(24,28) { ! alpha6( X ), rs( X,
% 1.30/1.71 skol7( X ) ) }.
% 1.30/1.71 parent1[0]: (76) {G3,W3,D3,L1,V1,M1} R(21,58) { alpha6( skol1( X ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := skol1( X )
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (163) {G4,W6,D4,L1,V1,M1} R(154,76) { rs( skol1( X ), skol7(
% 1.30/1.71 skol1( X ) ) ) }.
% 1.30/1.71 parent0: (10670) {G2,W6,D4,L1,V1,M1} { rs( skol1( X ), skol7( skol1( X ) )
% 1.30/1.71 ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 eqswap: (10671) {G0,W7,D3,L2,V1,M2} { ! skol2( X ) ==> skol7( X ), !
% 1.30/1.71 alpha6( X ) }.
% 1.30/1.71 parent0[1]: (25) {G0,W7,D3,L2,V1,M2} I { ! alpha6( X ), ! skol7( X ) ==>
% 1.30/1.71 skol2( X ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10672) {G1,W7,D4,L1,V1,M1} { ! skol2( skol1( X ) ) ==> skol7
% 1.30/1.71 ( skol1( X ) ) }.
% 1.30/1.71 parent0[1]: (10671) {G0,W7,D3,L2,V1,M2} { ! skol2( X ) ==> skol7( X ), !
% 1.30/1.71 alpha6( X ) }.
% 1.30/1.71 parent1[0]: (76) {G3,W3,D3,L1,V1,M1} R(21,58) { alpha6( skol1( X ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := skol1( X )
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 eqswap: (10673) {G1,W7,D4,L1,V1,M1} { ! skol7( skol1( X ) ) ==> skol2(
% 1.30/1.71 skol1( X ) ) }.
% 1.30/1.71 parent0[0]: (10672) {G1,W7,D4,L1,V1,M1} { ! skol2( skol1( X ) ) ==> skol7
% 1.30/1.71 ( skol1( X ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (170) {G4,W7,D4,L1,V1,M1} R(25,76) { ! skol7( skol1( X ) ) ==>
% 1.30/1.71 skol2( skol1( X ) ) }.
% 1.30/1.71 parent0: (10673) {G1,W7,D4,L1,V1,M1} { ! skol7( skol1( X ) ) ==> skol2(
% 1.30/1.71 skol1( X ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10674) {G1,W5,D3,L2,V0,M2} { ! alpha1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), cd( skol1( i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 parent0[1]: (42) {G0,W7,D2,L3,V2,M3} I { ! alpha1( X ), ! rr( X, Y ), cd( Y
% 1.30/1.71 ) }.
% 1.30/1.71 parent1[0]: (114) {G3,W4,D3,L1,V0,M1} R(22,58) { rr(
% 1.30/1.71 i2003_11_14_17_20_36582, skol1( i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := i2003_11_14_17_20_36582
% 1.30/1.71 Y := skol1( i2003_11_14_17_20_36582 )
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10675) {G2,W3,D3,L1,V0,M1} { cd( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 parent0[0]: (10674) {G1,W5,D3,L2,V0,M2} { ! alpha1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), cd( skol1( i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 parent1[0]: (63) {G1,W2,D2,L1,V0,M1} R(15,46) { alpha1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (266) {G4,W3,D3,L1,V0,M1} R(42,114);r(63) { cd( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 parent0: (10675) {G2,W3,D3,L1,V0,M1} { cd( skol1( i2003_11_14_17_20_36582
% 1.30/1.71 ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10676) {G1,W5,D3,L2,V0,M2} { ! alpha3(
% 1.30/1.71 i2003_11_14_17_20_36582 ), alpha5( skol1( i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 parent0[1]: (30) {G0,W7,D2,L3,V2,M3} I { ! alpha3( X ), ! rr( X, Y ),
% 1.30/1.71 alpha5( Y ) }.
% 1.30/1.71 parent1[0]: (114) {G3,W4,D3,L1,V0,M1} R(22,58) { rr(
% 1.30/1.71 i2003_11_14_17_20_36582, skol1( i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := i2003_11_14_17_20_36582
% 1.30/1.71 Y := skol1( i2003_11_14_17_20_36582 )
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10677) {G2,W3,D3,L1,V0,M1} { alpha5( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 parent0[0]: (10676) {G1,W5,D3,L2,V0,M2} { ! alpha3(
% 1.30/1.71 i2003_11_14_17_20_36582 ), alpha5( skol1( i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 parent1[0]: (57) {G2,W2,D2,L1,V0,M1} R(53,18) { alpha3(
% 1.30/1.71 i2003_11_14_17_20_36582 ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (344) {G4,W3,D3,L1,V0,M1} R(30,114);r(57) { alpha5( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 parent0: (10677) {G2,W3,D3,L1,V0,M1} { alpha5( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10678) {G2,W6,D3,L2,V0,M2} { alpha7( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ), ! cd( skol1( i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 parent0[0]: (81) {G1,W6,D2,L3,V1,M3} R(33,45) { ! alpha5( X ), alpha7( X )
% 1.30/1.71 , ! cd( X ) }.
% 1.30/1.71 parent1[0]: (344) {G4,W3,D3,L1,V0,M1} R(30,114);r(57) { alpha5( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := skol1( i2003_11_14_17_20_36582 )
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10679) {G3,W3,D3,L1,V0,M1} { alpha7( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 parent0[1]: (10678) {G2,W6,D3,L2,V0,M2} { alpha7( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ), ! cd( skol1( i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 parent1[0]: (266) {G4,W3,D3,L1,V0,M1} R(42,114);r(63) { cd( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (360) {G5,W3,D3,L1,V0,M1} R(344,81);r(266) { alpha7( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 parent0: (10679) {G3,W3,D3,L1,V0,M1} { alpha7( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10680) {G1,W8,D3,L2,V1,M2} { ! rs( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), X ), ! alpha9( skol1( i2003_11_14_17_20_36582
% 1.30/1.71 ), X ) }.
% 1.30/1.71 parent0[0]: (36) {G0,W8,D2,L3,V2,M3} I { ! alpha7( X ), ! rs( X, Y ), !
% 1.30/1.71 alpha9( X, Y ) }.
% 1.30/1.71 parent1[0]: (360) {G5,W3,D3,L1,V0,M1} R(344,81);r(266) { alpha7( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := skol1( i2003_11_14_17_20_36582 )
% 1.30/1.71 Y := X
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (371) {G6,W8,D3,L2,V1,M2} R(36,360) { ! rs( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), X ), ! alpha9( skol1( i2003_11_14_17_20_36582
% 1.30/1.71 ), X ) }.
% 1.30/1.71 parent0: (10680) {G1,W8,D3,L2,V1,M2} { ! rs( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), X ), ! alpha9( skol1( i2003_11_14_17_20_36582
% 1.30/1.71 ), X ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 eqswap: (10681) {G0,W9,D2,L3,V3,M3} { Y = X, ! rs( Z, Y ), alpha9( Z, X )
% 1.30/1.71 }.
% 1.30/1.71 parent0[1]: (41) {G0,W9,D2,L3,V3,M3} I { ! rs( X, Z ), Y = Z, alpha9( X, Y
% 1.30/1.71 ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := Z
% 1.30/1.71 Y := X
% 1.30/1.71 Z := Y
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10682) {G1,W9,D3,L3,V2,M3} { skol7( X ) = Y, alpha9( X, Y ),
% 1.30/1.71 ! alpha6( X ) }.
% 1.30/1.71 parent0[1]: (10681) {G0,W9,D2,L3,V3,M3} { Y = X, ! rs( Z, Y ), alpha9( Z,
% 1.30/1.71 X ) }.
% 1.30/1.71 parent1[1]: (154) {G1,W6,D3,L2,V1,M2} R(24,28) { ! alpha6( X ), rs( X,
% 1.30/1.71 skol7( X ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := Y
% 1.30/1.71 Y := skol7( X )
% 1.30/1.71 Z := X
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 eqswap: (10683) {G1,W9,D3,L3,V2,M3} { Y = skol7( X ), alpha9( X, Y ), !
% 1.30/1.71 alpha6( X ) }.
% 1.30/1.71 parent0[0]: (10682) {G1,W9,D3,L3,V2,M3} { skol7( X ) = Y, alpha9( X, Y ),
% 1.30/1.71 ! alpha6( X ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 Y := Y
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (468) {G2,W9,D3,L3,V2,M3} R(41,154) { X = skol7( Y ), alpha9(
% 1.30/1.71 Y, X ), ! alpha6( Y ) }.
% 1.30/1.71 parent0: (10683) {G1,W9,D3,L3,V2,M3} { Y = skol7( X ), alpha9( X, Y ), !
% 1.30/1.71 alpha6( X ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := Y
% 1.30/1.71 Y := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 2 ==> 2
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10684) {G5,W6,D4,L1,V0,M1} { ! alpha9( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), skol2( skol1( i2003_11_14_17_20_36582 ) ) )
% 1.30/1.71 }.
% 1.30/1.71 parent0[0]: (371) {G6,W8,D3,L2,V1,M2} R(36,360) { ! rs( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), X ), ! alpha9( skol1( i2003_11_14_17_20_36582
% 1.30/1.71 ), X ) }.
% 1.30/1.71 parent1[0]: (159) {G4,W6,D4,L1,V1,M1} R(153,76) { rs( skol1( X ), skol2(
% 1.30/1.71 skol1( X ) ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := skol2( skol1( i2003_11_14_17_20_36582 ) )
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 X := i2003_11_14_17_20_36582
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (1580) {G7,W6,D4,L1,V0,M1} R(371,159) { ! alpha9( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), skol2( skol1( i2003_11_14_17_20_36582 ) ) )
% 1.30/1.71 }.
% 1.30/1.71 parent0: (10684) {G5,W6,D4,L1,V0,M1} { ! alpha9( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), skol2( skol1( i2003_11_14_17_20_36582 ) ) )
% 1.30/1.71 }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10685) {G5,W6,D4,L1,V0,M1} { ! alpha9( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), skol7( skol1( i2003_11_14_17_20_36582 ) ) )
% 1.30/1.71 }.
% 1.30/1.71 parent0[0]: (371) {G6,W8,D3,L2,V1,M2} R(36,360) { ! rs( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), X ), ! alpha9( skol1( i2003_11_14_17_20_36582
% 1.30/1.71 ), X ) }.
% 1.30/1.71 parent1[0]: (163) {G4,W6,D4,L1,V1,M1} R(154,76) { rs( skol1( X ), skol7(
% 1.30/1.71 skol1( X ) ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := skol7( skol1( i2003_11_14_17_20_36582 ) )
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 X := i2003_11_14_17_20_36582
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (1581) {G7,W6,D4,L1,V0,M1} R(371,163) { ! alpha9( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), skol7( skol1( i2003_11_14_17_20_36582 ) ) )
% 1.30/1.71 }.
% 1.30/1.71 parent0: (10685) {G5,W6,D4,L1,V0,M1} { ! alpha9( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), skol7( skol1( i2003_11_14_17_20_36582 ) ) )
% 1.30/1.71 }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 eqswap: (10686) {G2,W9,D3,L3,V2,M3} { skol7( Y ) = X, alpha9( Y, X ), !
% 1.30/1.71 alpha6( Y ) }.
% 1.30/1.71 parent0[0]: (468) {G2,W9,D3,L3,V2,M3} R(41,154) { X = skol7( Y ), alpha9( Y
% 1.30/1.71 , X ), ! alpha6( Y ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 Y := Y
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10687) {G3,W10,D4,L2,V0,M2} { skol7( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) = skol2( skol1( i2003_11_14_17_20_36582 ) ),
% 1.30/1.71 ! alpha6( skol1( i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 parent0[0]: (1580) {G7,W6,D4,L1,V0,M1} R(371,159) { ! alpha9( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), skol2( skol1( i2003_11_14_17_20_36582 ) ) )
% 1.30/1.71 }.
% 1.30/1.71 parent1[1]: (10686) {G2,W9,D3,L3,V2,M3} { skol7( Y ) = X, alpha9( Y, X ),
% 1.30/1.71 ! alpha6( Y ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 X := skol2( skol1( i2003_11_14_17_20_36582 ) )
% 1.30/1.71 Y := skol1( i2003_11_14_17_20_36582 )
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10688) {G4,W7,D4,L1,V0,M1} { skol7( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) = skol2( skol1( i2003_11_14_17_20_36582 ) )
% 1.30/1.71 }.
% 1.30/1.71 parent0[1]: (10687) {G3,W10,D4,L2,V0,M2} { skol7( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) = skol2( skol1( i2003_11_14_17_20_36582 ) ),
% 1.30/1.71 ! alpha6( skol1( i2003_11_14_17_20_36582 ) ) }.
% 1.30/1.71 parent1[0]: (76) {G3,W3,D3,L1,V1,M1} R(21,58) { alpha6( skol1( X ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 X := i2003_11_14_17_20_36582
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (10058) {G8,W7,D4,L1,V0,M1} R(468,1580);r(76) { skol7( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) ==> skol2( skol1( i2003_11_14_17_20_36582 ) )
% 1.30/1.71 }.
% 1.30/1.71 parent0: (10688) {G4,W7,D4,L1,V0,M1} { skol7( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) = skol2( skol1( i2003_11_14_17_20_36582 ) )
% 1.30/1.71 }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 eqswap: (10690) {G2,W9,D3,L3,V2,M3} { skol7( Y ) = X, alpha9( Y, X ), !
% 1.30/1.71 alpha6( Y ) }.
% 1.30/1.71 parent0[0]: (468) {G2,W9,D3,L3,V2,M3} R(41,154) { X = skol7( Y ), alpha9( Y
% 1.30/1.71 , X ), ! alpha6( Y ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 Y := Y
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 eqswap: (10691) {G4,W7,D4,L1,V1,M1} { ! skol2( skol1( X ) ) ==> skol7(
% 1.30/1.71 skol1( X ) ) }.
% 1.30/1.71 parent0[0]: (170) {G4,W7,D4,L1,V1,M1} R(25,76) { ! skol7( skol1( X ) ) ==>
% 1.30/1.71 skol2( skol1( X ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 paramod: (10692) {G3,W12,D4,L3,V2,M3} { ! skol2( skol1( X ) ) ==> Y,
% 1.30/1.71 alpha9( skol1( X ), Y ), ! alpha6( skol1( X ) ) }.
% 1.30/1.71 parent0[0]: (10690) {G2,W9,D3,L3,V2,M3} { skol7( Y ) = X, alpha9( Y, X ),
% 1.30/1.71 ! alpha6( Y ) }.
% 1.30/1.71 parent1[0; 5]: (10691) {G4,W7,D4,L1,V1,M1} { ! skol2( skol1( X ) ) ==>
% 1.30/1.71 skol7( skol1( X ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := Y
% 1.30/1.71 Y := skol1( X )
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10693) {G4,W9,D4,L2,V2,M2} { ! skol2( skol1( X ) ) ==> Y,
% 1.30/1.71 alpha9( skol1( X ), Y ) }.
% 1.30/1.71 parent0[2]: (10692) {G3,W12,D4,L3,V2,M3} { ! skol2( skol1( X ) ) ==> Y,
% 1.30/1.71 alpha9( skol1( X ), Y ), ! alpha6( skol1( X ) ) }.
% 1.30/1.71 parent1[0]: (76) {G3,W3,D3,L1,V1,M1} R(21,58) { alpha6( skol1( X ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 Y := Y
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 eqswap: (10694) {G4,W9,D4,L2,V2,M2} { ! Y ==> skol2( skol1( X ) ), alpha9
% 1.30/1.71 ( skol1( X ), Y ) }.
% 1.30/1.71 parent0[0]: (10693) {G4,W9,D4,L2,V2,M2} { ! skol2( skol1( X ) ) ==> Y,
% 1.30/1.71 alpha9( skol1( X ), Y ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 Y := Y
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (10334) {G5,W9,D4,L2,V2,M2} P(468,170);r(76) { ! Y = skol2(
% 1.30/1.71 skol1( X ) ), alpha9( skol1( X ), Y ) }.
% 1.30/1.71 parent0: (10694) {G4,W9,D4,L2,V2,M2} { ! Y ==> skol2( skol1( X ) ), alpha9
% 1.30/1.71 ( skol1( X ), Y ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 Y := Y
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 1 ==> 1
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 eqswap: (10695) {G5,W9,D4,L2,V2,M2} { ! skol2( skol1( Y ) ) = X, alpha9(
% 1.30/1.71 skol1( Y ), X ) }.
% 1.30/1.71 parent0[0]: (10334) {G5,W9,D4,L2,V2,M2} P(468,170);r(76) { ! Y = skol2(
% 1.30/1.71 skol1( X ) ), alpha9( skol1( X ), Y ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := Y
% 1.30/1.71 Y := X
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 eqrefl: (10696) {G0,W6,D4,L1,V1,M1} { alpha9( skol1( X ), skol2( skol1( X
% 1.30/1.71 ) ) ) }.
% 1.30/1.71 parent0[0]: (10695) {G5,W9,D4,L2,V2,M2} { ! skol2( skol1( Y ) ) = X,
% 1.30/1.71 alpha9( skol1( Y ), X ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := skol2( skol1( X ) )
% 1.30/1.71 Y := X
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (10376) {G6,W6,D4,L1,V1,M1} Q(10334) { alpha9( skol1( X ),
% 1.30/1.71 skol2( skol1( X ) ) ) }.
% 1.30/1.71 parent0: (10696) {G0,W6,D4,L1,V1,M1} { alpha9( skol1( X ), skol2( skol1( X
% 1.30/1.71 ) ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 X := X
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 0 ==> 0
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 paramod: (10698) {G8,W6,D4,L1,V0,M1} { ! alpha9( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), skol2( skol1( i2003_11_14_17_20_36582 ) ) )
% 1.30/1.71 }.
% 1.30/1.71 parent0[0]: (10058) {G8,W7,D4,L1,V0,M1} R(468,1580);r(76) { skol7( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ) ) ==> skol2( skol1( i2003_11_14_17_20_36582 ) )
% 1.30/1.71 }.
% 1.30/1.71 parent1[0; 4]: (1581) {G7,W6,D4,L1,V0,M1} R(371,163) { ! alpha9( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), skol7( skol1( i2003_11_14_17_20_36582 ) ) )
% 1.30/1.71 }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 resolution: (10699) {G7,W0,D0,L0,V0,M0} { }.
% 1.30/1.71 parent0[0]: (10698) {G8,W6,D4,L1,V0,M1} { ! alpha9( skol1(
% 1.30/1.71 i2003_11_14_17_20_36582 ), skol2( skol1( i2003_11_14_17_20_36582 ) ) )
% 1.30/1.71 }.
% 1.30/1.71 parent1[0]: (10376) {G6,W6,D4,L1,V1,M1} Q(10334) { alpha9( skol1( X ),
% 1.30/1.71 skol2( skol1( X ) ) ) }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 substitution1:
% 1.30/1.71 X := i2003_11_14_17_20_36582
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 subsumption: (10390) {G9,W0,D0,L0,V0,M0} S(1581);d(10058);r(10376) { }.
% 1.30/1.71 parent0: (10699) {G7,W0,D0,L0,V0,M0} { }.
% 1.30/1.71 substitution0:
% 1.30/1.71 end
% 1.30/1.71 permutation0:
% 1.30/1.71 end
% 1.30/1.71
% 1.30/1.71 Proof check complete!
% 1.30/1.71
% 1.30/1.71 Memory use:
% 1.30/1.71
% 1.30/1.71 space for terms: 157147
% 1.30/1.71 space for clauses: 370055
% 1.30/1.71
% 1.30/1.71
% 1.30/1.71 clauses generated: 32498
% 1.30/1.71 clauses kept: 10391
% 1.30/1.71 clauses selected: 514
% 1.30/1.71 clauses deleted: 46
% 1.30/1.71 clauses inuse deleted: 30
% 1.30/1.71
% 1.30/1.71 subsentry: 126640
% 1.30/1.71 literals s-matched: 83615
% 1.30/1.71 literals matched: 76550
% 1.30/1.71 full subsumption: 36502
% 1.30/1.71
% 1.30/1.71 checksum: 46990702
% 1.30/1.71
% 1.30/1.71
% 1.30/1.71 Bliksem ended
%------------------------------------------------------------------------------