%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : KRS078+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Sun Jul 17 02:42:09 EDT 2022
% Result : Unsatisfiable 0.91s 1.28s
% Output : Refutation 0.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : KRS078+1 : TPTP v8.1.0. Released v3.1.0.
% 0.07/0.12 % Command : bliksem %s
% 0.12/0.32 % Computer : n022.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % DateTime : Tue Jun 7 13:46:20 EDT 2022
% 0.12/0.32 % CPUTime :
% 0.91/1.28 *** allocated 10000 integers for termspace/termends
% 0.91/1.28 *** allocated 10000 integers for clauses
% 0.91/1.28 *** allocated 10000 integers for justifications
% 0.91/1.28 Bliksem 1.12
% 0.91/1.28
% 0.91/1.28
% 0.91/1.28 Automatic Strategy Selection
% 0.91/1.28
% 0.91/1.28
% 0.91/1.28 Clauses:
% 0.91/1.28
% 0.91/1.28 { ! Y = X, ! cUnsatisfiable( Y ), cUnsatisfiable( X ) }.
% 0.91/1.28 { ! Y = X, ! cowlNothing( Y ), cowlNothing( X ) }.
% 0.91/1.28 { ! Y = X, ! cowlThing( Y ), cowlThing( X ) }.
% 0.91/1.28 { ! Y = X, ! cp( Y ), cp( X ) }.
% 0.91/1.28 { ! Y = X, ! cq( Y ), cq( X ) }.
% 0.91/1.28 { ! Z = X, ! rinvR( Z, Y ), rinvR( X, Y ) }.
% 0.91/1.28 { ! Z = X, ! rinvR( Y, Z ), rinvR( Y, X ) }.
% 0.91/1.28 { ! Z = X, ! rr( Z, Y ), rr( X, Y ) }.
% 0.91/1.28 { ! Z = X, ! rr( Y, Z ), rr( Y, X ) }.
% 0.91/1.28 { ! Z = X, ! rs( Z, Y ), rs( X, Y ) }.
% 0.91/1.28 { ! Z = X, ! rs( Y, Z ), rs( Y, X ) }.
% 0.91/1.28 { ! Y = X, ! xsd_integer( Y ), xsd_integer( X ) }.
% 0.91/1.28 { ! Y = X, ! xsd_string( Y ), xsd_string( X ) }.
% 0.91/1.28 { cowlThing( X ) }.
% 0.91/1.28 { ! cowlNothing( X ) }.
% 0.91/1.28 { ! xsd_string( X ), ! xsd_integer( X ) }.
% 0.91/1.28 { xsd_integer( X ), xsd_string( X ) }.
% 0.91/1.28 { ! cUnsatisfiable( X ), alpha1( X ) }.
% 0.91/1.28 { ! cUnsatisfiable( X ), alpha2( X ) }.
% 0.91/1.28 { ! alpha1( X ), ! alpha2( X ), cUnsatisfiable( X ) }.
% 0.91/1.28 { ! alpha2( X ), alpha4( skol1( Y ) ) }.
% 0.91/1.28 { ! alpha2( X ), rs( X, skol1( X ) ) }.
% 0.91/1.28 { ! rs( X, Y ), ! alpha4( Y ), alpha2( X ) }.
% 0.91/1.28 { ! alpha4( X ), ! cq( X ) }.
% 0.91/1.28 { ! alpha4( X ), ! cp( X ) }.
% 0.91/1.28 { cq( X ), cp( X ), alpha4( X ) }.
% 0.91/1.28 { ! alpha1( X ), alpha3( skol2( Y ) ) }.
% 0.91/1.28 { ! alpha1( X ), rr( X, skol2( X ) ) }.
% 0.91/1.28 { ! rr( X, Y ), ! alpha3( Y ), alpha1( X ) }.
% 0.91/1.28 { ! alpha3( X ), alpha5( X ) }.
% 0.91/1.28 { ! alpha3( X ), alpha6( X ) }.
% 0.91/1.28 { ! alpha5( X ), ! alpha6( X ), alpha3( X ) }.
% 0.91/1.28 { ! alpha6( X ), ! alpha8( X, Y, Z ), Y = Z }.
% 0.91/1.28 { alpha8( X, skol3( X ), skol6( X ) ), alpha6( X ) }.
% 0.91/1.28 { ! skol3( X ) = skol6( X ), alpha6( X ) }.
% 0.91/1.28 { ! alpha8( X, Y, Z ), rinvR( X, Y ) }.
% 0.91/1.28 { ! alpha8( X, Y, Z ), rinvR( X, Z ) }.
% 0.91/1.28 { ! rinvR( X, Y ), ! rinvR( X, Z ), alpha8( X, Y, Z ) }.
% 0.91/1.28 { ! alpha5( X ), alpha7( skol4( Y ) ) }.
% 0.91/1.28 { ! alpha5( X ), rinvR( X, skol4( X ) ) }.
% 0.91/1.28 { ! rinvR( X, Y ), ! alpha7( Y ), alpha5( X ) }.
% 0.91/1.28 { ! alpha7( X ), ! rs( X, Y ), cp( Y ) }.
% 0.91/1.28 { ! cp( skol5( Y ) ), alpha7( X ) }.
% 0.91/1.28 { rs( X, skol5( X ) ), alpha7( X ) }.
% 0.91/1.28 { ! rinvR( X, Y ), rr( Y, X ) }.
% 0.91/1.28 { ! rr( Y, X ), rinvR( X, Y ) }.
% 0.91/1.28 { cUnsatisfiable( i2003_11_14_17_19_13721 ) }.
% 0.91/1.28
% 0.91/1.28 percentage equality = 0.132743, percentage horn = 0.914894
% 0.91/1.28 This is a problem with some equality
% 0.91/1.28
% 0.91/1.28
% 0.91/1.28
% 0.91/1.28 Options Used:
% 0.91/1.28
% 0.91/1.28 useres = 1
% 0.91/1.28 useparamod = 1
% 0.91/1.28 useeqrefl = 1
% 0.91/1.28 useeqfact = 1
% 0.91/1.28 usefactor = 1
% 0.91/1.28 usesimpsplitting = 0
% 0.91/1.28 usesimpdemod = 5
% 0.91/1.28 usesimpres = 3
% 0.91/1.28
% 0.91/1.28 resimpinuse = 1000
% 0.91/1.28 resimpclauses = 20000
% 0.91/1.28 substype = eqrewr
% 0.91/1.28 backwardsubs = 1
% 0.91/1.28 selectoldest = 5
% 0.91/1.28
% 0.91/1.28 litorderings [0] = split
% 0.91/1.28 litorderings [1] = extend the termordering, first sorting on arguments
% 0.91/1.28
% 0.91/1.28 termordering = kbo
% 0.91/1.28
% 0.91/1.28 litapriori = 0
% 0.91/1.28 termapriori = 1
% 0.91/1.28 litaposteriori = 0
% 0.91/1.28 termaposteriori = 0
% 0.91/1.28 demodaposteriori = 0
% 0.91/1.28 ordereqreflfact = 0
% 0.91/1.28
% 0.91/1.28 litselect = negord
% 0.91/1.28
% 0.91/1.28 maxweight = 15
% 0.91/1.28 maxdepth = 30000
% 0.91/1.28 maxlength = 115
% 0.91/1.28 maxnrvars = 195
% 0.91/1.28 excuselevel = 1
% 0.91/1.28 increasemaxweight = 1
% 0.91/1.28
% 0.91/1.28 maxselected = 10000000
% 0.91/1.28 maxnrclauses = 10000000
% 0.91/1.28
% 0.91/1.28 showgenerated = 0
% 0.91/1.28 showkept = 0
% 0.91/1.28 showselected = 0
% 0.91/1.28 showdeleted = 0
% 0.91/1.28 showresimp = 1
% 0.91/1.28 showstatus = 2000
% 0.91/1.28
% 0.91/1.28 prologoutput = 0
% 0.91/1.28 nrgoals = 5000000
% 0.91/1.28 totalproof = 1
% 0.91/1.28
% 0.91/1.28 Symbols occurring in the translation:
% 0.91/1.28
% 0.91/1.28 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.91/1.28 . [1, 2] (w:1, o:41, a:1, s:1, b:0),
% 0.91/1.28 ! [4, 1] (w:0, o:16, a:1, s:1, b:0),
% 0.91/1.28 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.91/1.28 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.91/1.28 cUnsatisfiable [37, 1] (w:1, o:21, a:1, s:1, b:0),
% 0.91/1.28 cowlNothing [38, 1] (w:1, o:22, a:1, s:1, b:0),
% 0.91/1.28 cowlThing [39, 1] (w:1, o:23, a:1, s:1, b:0),
% 0.91/1.28 cp [40, 1] (w:1, o:24, a:1, s:1, b:0),
% 0.91/1.28 cq [41, 1] (w:1, o:25, a:1, s:1, b:0),
% 0.91/1.28 rinvR [43, 2] (w:1, o:65, a:1, s:1, b:0),
% 0.91/1.28 rr [44, 2] (w:1, o:66, a:1, s:1, b:0),
% 0.91/1.28 rs [45, 2] (w:1, o:67, a:1, s:1, b:0),
% 0.91/1.28 xsd_integer [46, 1] (w:1, o:26, a:1, s:1, b:0),
% 0.91/1.28 xsd_string [47, 1] (w:1, o:27, a:1, s:1, b:0),
% 0.91/1.28 i2003_11_14_17_19_13721 [54, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.91/1.28 alpha1 [55, 1] (w:1, o:28, a:1, s:1, b:1),
% 0.91/1.28 alpha2 [56, 1] (w:1, o:29, a:1, s:1, b:1),
% 0.91/1.28 alpha3 [57, 1] (w:1, o:30, a:1, s:1, b:1),
% 0.91/1.28 alpha4 [58, 1] (w:1, o:31, a:1, s:1, b:1),
% 0.91/1.28 alpha5 [59, 1] (w:1, o:32, a:1, s:1, b:1),
% 0.91/1.28 alpha6 [60, 1] (w:1, o:33, a:1, s:1, b:1),
% 0.91/1.28 alpha7 [61, 1] (w:1, o:34, a:1, s:1, b:1),
% 0.91/1.28 alpha8 [62, 3] (w:1, o:68, a:1, s:1, b:1),
% 0.91/1.28 skol1 [63, 1] (w:1, o:35, a:1, s:1, b:1),
% 0.91/1.28 skol2 [64, 1] (w:1, o:36, a:1, s:1, b:1),
% 0.91/1.28 skol3 [65, 1] (w:1, o:37, a:1, s:1, b:1),
% 0.91/1.28 skol4 [66, 1] (w:1, o:38, a:1, s:1, b:1),
% 0.91/1.28 skol5 [67, 1] (w:1, o:39, a:1, s:1, b:1),
% 0.91/1.28 skol6 [68, 1] (w:1, o:40, a:1, s:1, b:1).
% 0.91/1.28
% 0.91/1.28
% 0.91/1.28 Starting Search:
% 0.91/1.28
% 0.91/1.28 *** allocated 15000 integers for clauses
% 0.91/1.28 *** allocated 22500 integers for clauses
% 0.91/1.28 *** allocated 33750 integers for clauses
% 0.91/1.28 *** allocated 15000 integers for termspace/termends
% 0.91/1.28 *** allocated 50625 integers for clauses
% 0.91/1.28 Resimplifying inuse:
% 0.91/1.28 Done
% 0.91/1.28
% 0.91/1.28 *** allocated 22500 integers for termspace/termends
% 0.91/1.28 *** allocated 75937 integers for clauses
% 0.91/1.28 *** allocated 33750 integers for termspace/termends
% 0.91/1.28
% 0.91/1.28 Intermediate Status:
% 0.91/1.28 Generated: 6388
% 0.91/1.28 Kept: 2004
% 0.91/1.28 Inuse: 249
% 0.91/1.28 Deleted: 20
% 0.91/1.28 Deletedinuse: 5
% 0.91/1.28
% 0.91/1.28 Resimplifying inuse:
% 0.91/1.28 Done
% 0.91/1.28
% 0.91/1.28 *** allocated 113905 integers for clauses
% 0.91/1.28 *** allocated 50625 integers for termspace/termends
% 0.91/1.28 Resimplifying inuse:
% 0.91/1.28 Done
% 0.91/1.28
% 0.91/1.28 *** allocated 170857 integers for clauses
% 0.91/1.28 *** allocated 75937 integers for termspace/termends
% 0.91/1.28
% 0.91/1.28 Intermediate Status:
% 0.91/1.28 Generated: 14112
% 0.91/1.28 Kept: 4047
% 0.91/1.28 Inuse: 359
% 0.91/1.28 Deleted: 31
% 0.91/1.28 Deletedinuse: 5
% 0.91/1.28
% 0.91/1.28 Resimplifying inuse:
% 0.91/1.28
% 0.91/1.28 Bliksems!, er is een bewijs:
% 0.91/1.28 % SZS status Unsatisfiable
% 0.91/1.28 % SZS output start Refutation
% 0.91/1.28
% 0.91/1.28 (0) {G0,W7,D2,L3,V2,M3} I { ! Y = X, ! cUnsatisfiable( Y ), cUnsatisfiable
% 0.91/1.28 ( X ) }.
% 0.91/1.28 (17) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha1( X ) }.
% 0.91/1.28 (18) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha2( X ) }.
% 0.91/1.28 (20) {G0,W5,D3,L2,V2,M2} I { ! alpha2( X ), alpha4( skol1( Y ) ) }.
% 0.91/1.28 (21) {G0,W6,D3,L2,V1,M2} I { ! alpha2( X ), rs( X, skol1( X ) ) }.
% 0.91/1.28 (24) {G0,W4,D2,L2,V1,M2} I { ! alpha4( X ), ! cp( X ) }.
% 0.91/1.28 (26) {G0,W5,D3,L2,V2,M2} I { ! alpha1( X ), alpha3( skol2( Y ) ) }.
% 0.91/1.28 (27) {G0,W6,D3,L2,V1,M2} I { ! alpha1( X ), rr( X, skol2( X ) ) }.
% 0.91/1.28 (29) {G0,W4,D2,L2,V1,M2} I { ! alpha3( X ), alpha5( X ) }.
% 0.91/1.28 (30) {G0,W4,D2,L2,V1,M2} I { ! alpha3( X ), alpha6( X ) }.
% 0.91/1.28 (32) {G0,W9,D2,L3,V3,M3} I { ! alpha6( X ), ! alpha8( X, Y, Z ), Y = Z }.
% 0.91/1.28 (37) {G0,W10,D2,L3,V3,M3} I { ! rinvR( X, Y ), ! rinvR( X, Z ), alpha8( X,
% 0.91/1.28 Y, Z ) }.
% 0.91/1.28 (38) {G0,W5,D3,L2,V2,M2} I { ! alpha5( X ), alpha7( skol4( Y ) ) }.
% 0.91/1.28 (39) {G0,W6,D3,L2,V1,M2} I { ! alpha5( X ), rinvR( X, skol4( X ) ) }.
% 0.91/1.28 (41) {G0,W7,D2,L3,V2,M3} I { ! alpha7( X ), ! rs( X, Y ), cp( Y ) }.
% 0.91/1.28 (45) {G0,W6,D2,L2,V2,M2} I { ! rr( Y, X ), rinvR( X, Y ) }.
% 0.91/1.28 (46) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable( i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 (49) {G1,W5,D2,L2,V1,M2} R(0,46) { ! i2003_11_14_17_19_13721 = X,
% 0.91/1.28 cUnsatisfiable( X ) }.
% 0.91/1.28 (51) {G1,W2,D2,L1,V0,M1} R(18,46) { alpha2( i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 (53) {G1,W2,D2,L1,V0,M1} R(17,46) { alpha1( i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 (60) {G1,W5,D3,L2,V2,M2} R(38,29) { alpha7( skol4( X ) ), ! alpha3( Y ) }.
% 0.91/1.28 (63) {G2,W3,D3,L1,V1,M1} R(26,53) { alpha3( skol2( X ) ) }.
% 0.91/1.28 (66) {G3,W3,D3,L1,V1,M1} R(63,60) { alpha7( skol4( X ) ) }.
% 0.91/1.28 (67) {G3,W3,D3,L1,V1,M1} R(63,29) { alpha5( skol2( X ) ) }.
% 0.91/1.28 (68) {G3,W3,D3,L1,V1,M1} R(63,30) { alpha6( skol2( X ) ) }.
% 0.91/1.28 (73) {G2,W3,D3,L1,V1,M1} R(20,51) { alpha4( skol1( X ) ) }.
% 0.91/1.28 (77) {G3,W3,D3,L1,V1,M1} R(73,24) { ! cp( skol1( X ) ) }.
% 0.91/1.28 (104) {G4,W6,D4,L1,V1,M1} R(39,67) { rinvR( skol2( X ), skol4( skol2( X ) )
% 0.91/1.28 ) }.
% 0.91/1.28 (122) {G2,W4,D3,L1,V0,M1} R(27,53) { rr( i2003_11_14_17_19_13721, skol2(
% 0.91/1.28 i2003_11_14_17_19_13721 ) ) }.
% 0.91/1.28 (125) {G3,W4,D3,L1,V0,M1} R(122,45) { rinvR( skol2( i2003_11_14_17_19_13721
% 0.91/1.28 ), i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 (147) {G1,W6,D3,L2,V1,M2} R(21,18) { rs( X, skol1( X ) ), ! cUnsatisfiable
% 0.91/1.28 ( X ) }.
% 0.91/1.28 (435) {G4,W4,D2,L2,V1,M2} R(41,147);r(77) { ! alpha7( X ), ! cUnsatisfiable
% 0.91/1.28 ( X ) }.
% 0.91/1.28 (466) {G5,W3,D3,L1,V1,M1} R(435,66) { ! cUnsatisfiable( skol4( X ) ) }.
% 0.91/1.28 (471) {G6,W4,D3,L1,V1,M1} R(466,49) { ! skol4( X ) ==>
% 0.91/1.28 i2003_11_14_17_19_13721 }.
% 0.91/1.28 (490) {G7,W10,D3,L3,V3,M3} P(32,471) { ! Y = i2003_11_14_17_19_13721, !
% 0.91/1.28 alpha6( Z ), ! alpha8( Z, skol4( X ), Y ) }.
% 0.91/1.28 (493) {G8,W7,D3,L2,V2,M2} Q(490) { ! alpha6( X ), ! alpha8( X, skol4( Y ),
% 0.91/1.28 i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 (648) {G9,W6,D3,L1,V2,M1} R(493,68) { ! alpha8( skol2( X ), skol4( Y ),
% 0.91/1.28 i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 (678) {G10,W9,D3,L2,V2,M2} R(648,37) { ! rinvR( skol2( X ), skol4( Y ) ), !
% 0.91/1.28 rinvR( skol2( X ), i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 (4032) {G11,W4,D3,L1,V1,M1} R(678,104) { ! rinvR( skol2( X ),
% 0.91/1.28 i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 (4047) {G12,W0,D0,L0,V0,M0} S(125);r(4032) { }.
% 0.91/1.28
% 0.91/1.28
% 0.91/1.28 % SZS output end Refutation
% 0.91/1.28 found a proof!
% 0.91/1.28
% 0.91/1.28
% 0.91/1.28 Unprocessed initial clauses:
% 0.91/1.28
% 0.91/1.28 (4049) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cUnsatisfiable( Y ),
% 0.91/1.28 cUnsatisfiable( X ) }.
% 0.91/1.28 (4050) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cowlNothing( Y ), cowlNothing( X )
% 0.91/1.28 }.
% 0.91/1.28 (4051) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cowlThing( Y ), cowlThing( X ) }.
% 0.91/1.28 (4052) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cp( Y ), cp( X ) }.
% 0.91/1.28 (4053) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cq( Y ), cq( X ) }.
% 0.91/1.28 (4054) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rinvR( Z, Y ), rinvR( X, Y ) }.
% 0.91/1.28 (4055) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rinvR( Y, Z ), rinvR( Y, X ) }.
% 0.91/1.28 (4056) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rr( Z, Y ), rr( X, Y ) }.
% 0.91/1.28 (4057) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rr( Y, Z ), rr( Y, X ) }.
% 0.91/1.28 (4058) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rs( Z, Y ), rs( X, Y ) }.
% 0.91/1.28 (4059) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rs( Y, Z ), rs( Y, X ) }.
% 0.91/1.28 (4060) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! xsd_integer( Y ), xsd_integer( X )
% 0.91/1.28 }.
% 0.91/1.28 (4061) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! xsd_string( Y ), xsd_string( X )
% 0.91/1.28 }.
% 0.91/1.28 (4062) {G0,W2,D2,L1,V1,M1} { cowlThing( X ) }.
% 0.91/1.28 (4063) {G0,W2,D2,L1,V1,M1} { ! cowlNothing( X ) }.
% 0.91/1.28 (4064) {G0,W4,D2,L2,V1,M2} { ! xsd_string( X ), ! xsd_integer( X ) }.
% 0.91/1.28 (4065) {G0,W4,D2,L2,V1,M2} { xsd_integer( X ), xsd_string( X ) }.
% 0.91/1.28 (4066) {G0,W4,D2,L2,V1,M2} { ! cUnsatisfiable( X ), alpha1( X ) }.
% 0.91/1.28 (4067) {G0,W4,D2,L2,V1,M2} { ! cUnsatisfiable( X ), alpha2( X ) }.
% 0.91/1.28 (4068) {G0,W6,D2,L3,V1,M3} { ! alpha1( X ), ! alpha2( X ), cUnsatisfiable
% 0.91/1.28 ( X ) }.
% 0.91/1.28 (4069) {G0,W5,D3,L2,V2,M2} { ! alpha2( X ), alpha4( skol1( Y ) ) }.
% 0.91/1.28 (4070) {G0,W6,D3,L2,V1,M2} { ! alpha2( X ), rs( X, skol1( X ) ) }.
% 0.91/1.28 (4071) {G0,W7,D2,L3,V2,M3} { ! rs( X, Y ), ! alpha4( Y ), alpha2( X ) }.
% 0.91/1.28 (4072) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), ! cq( X ) }.
% 0.91/1.28 (4073) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), ! cp( X ) }.
% 0.91/1.28 (4074) {G0,W6,D2,L3,V1,M3} { cq( X ), cp( X ), alpha4( X ) }.
% 0.91/1.28 (4075) {G0,W5,D3,L2,V2,M2} { ! alpha1( X ), alpha3( skol2( Y ) ) }.
% 0.91/1.28 (4076) {G0,W6,D3,L2,V1,M2} { ! alpha1( X ), rr( X, skol2( X ) ) }.
% 0.91/1.28 (4077) {G0,W7,D2,L3,V2,M3} { ! rr( X, Y ), ! alpha3( Y ), alpha1( X ) }.
% 0.91/1.28 (4078) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), alpha5( X ) }.
% 0.91/1.28 (4079) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), alpha6( X ) }.
% 0.91/1.28 (4080) {G0,W6,D2,L3,V1,M3} { ! alpha5( X ), ! alpha6( X ), alpha3( X ) }.
% 0.91/1.28 (4081) {G0,W9,D2,L3,V3,M3} { ! alpha6( X ), ! alpha8( X, Y, Z ), Y = Z }.
% 0.91/1.28 (4082) {G0,W8,D3,L2,V1,M2} { alpha8( X, skol3( X ), skol6( X ) ), alpha6(
% 0.91/1.28 X ) }.
% 0.91/1.28 (4083) {G0,W7,D3,L2,V1,M2} { ! skol3( X ) = skol6( X ), alpha6( X ) }.
% 0.91/1.28 (4084) {G0,W7,D2,L2,V3,M2} { ! alpha8( X, Y, Z ), rinvR( X, Y ) }.
% 0.91/1.28 (4085) {G0,W7,D2,L2,V3,M2} { ! alpha8( X, Y, Z ), rinvR( X, Z ) }.
% 0.91/1.28 (4086) {G0,W10,D2,L3,V3,M3} { ! rinvR( X, Y ), ! rinvR( X, Z ), alpha8( X
% 0.91/1.28 , Y, Z ) }.
% 0.91/1.28 (4087) {G0,W5,D3,L2,V2,M2} { ! alpha5( X ), alpha7( skol4( Y ) ) }.
% 0.91/1.28 (4088) {G0,W6,D3,L2,V1,M2} { ! alpha5( X ), rinvR( X, skol4( X ) ) }.
% 0.91/1.28 (4089) {G0,W7,D2,L3,V2,M3} { ! rinvR( X, Y ), ! alpha7( Y ), alpha5( X )
% 0.91/1.28 }.
% 0.91/1.28 (4090) {G0,W7,D2,L3,V2,M3} { ! alpha7( X ), ! rs( X, Y ), cp( Y ) }.
% 0.91/1.28 (4091) {G0,W5,D3,L2,V2,M2} { ! cp( skol5( Y ) ), alpha7( X ) }.
% 0.91/1.28 (4092) {G0,W6,D3,L2,V1,M2} { rs( X, skol5( X ) ), alpha7( X ) }.
% 0.91/1.28 (4093) {G0,W6,D2,L2,V2,M2} { ! rinvR( X, Y ), rr( Y, X ) }.
% 0.91/1.28 (4094) {G0,W6,D2,L2,V2,M2} { ! rr( Y, X ), rinvR( X, Y ) }.
% 0.91/1.28 (4095) {G0,W2,D2,L1,V0,M1} { cUnsatisfiable( i2003_11_14_17_19_13721 ) }.
% 0.91/1.28
% 0.91/1.28
% 0.91/1.28 Total Proof:
% 0.91/1.28
% 0.91/1.28 subsumption: (0) {G0,W7,D2,L3,V2,M3} I { ! Y = X, ! cUnsatisfiable( Y ),
% 0.91/1.28 cUnsatisfiable( X ) }.
% 0.91/1.28 parent0: (4049) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cUnsatisfiable( Y ),
% 0.91/1.28 cUnsatisfiable( X ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 Y := Y
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 2 ==> 2
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (17) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha1( X
% 0.91/1.28 ) }.
% 0.91/1.28 parent0: (4066) {G0,W4,D2,L2,V1,M2} { ! cUnsatisfiable( X ), alpha1( X )
% 0.91/1.28 }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (18) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha2( X
% 0.91/1.28 ) }.
% 0.91/1.28 parent0: (4067) {G0,W4,D2,L2,V1,M2} { ! cUnsatisfiable( X ), alpha2( X )
% 0.91/1.28 }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (20) {G0,W5,D3,L2,V2,M2} I { ! alpha2( X ), alpha4( skol1( Y )
% 0.91/1.28 ) }.
% 0.91/1.28 parent0: (4069) {G0,W5,D3,L2,V2,M2} { ! alpha2( X ), alpha4( skol1( Y ) )
% 0.91/1.28 }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 Y := Y
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (21) {G0,W6,D3,L2,V1,M2} I { ! alpha2( X ), rs( X, skol1( X )
% 0.91/1.28 ) }.
% 0.91/1.28 parent0: (4070) {G0,W6,D3,L2,V1,M2} { ! alpha2( X ), rs( X, skol1( X ) )
% 0.91/1.28 }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (24) {G0,W4,D2,L2,V1,M2} I { ! alpha4( X ), ! cp( X ) }.
% 0.91/1.28 parent0: (4073) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), ! cp( X ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (26) {G0,W5,D3,L2,V2,M2} I { ! alpha1( X ), alpha3( skol2( Y )
% 0.91/1.28 ) }.
% 0.91/1.28 parent0: (4075) {G0,W5,D3,L2,V2,M2} { ! alpha1( X ), alpha3( skol2( Y ) )
% 0.91/1.28 }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 Y := Y
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (27) {G0,W6,D3,L2,V1,M2} I { ! alpha1( X ), rr( X, skol2( X )
% 0.91/1.28 ) }.
% 0.91/1.28 parent0: (4076) {G0,W6,D3,L2,V1,M2} { ! alpha1( X ), rr( X, skol2( X ) )
% 0.91/1.28 }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (29) {G0,W4,D2,L2,V1,M2} I { ! alpha3( X ), alpha5( X ) }.
% 0.91/1.28 parent0: (4078) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), alpha5( X ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (30) {G0,W4,D2,L2,V1,M2} I { ! alpha3( X ), alpha6( X ) }.
% 0.91/1.28 parent0: (4079) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), alpha6( X ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (32) {G0,W9,D2,L3,V3,M3} I { ! alpha6( X ), ! alpha8( X, Y, Z
% 0.91/1.28 ), Y = Z }.
% 0.91/1.28 parent0: (4081) {G0,W9,D2,L3,V3,M3} { ! alpha6( X ), ! alpha8( X, Y, Z ),
% 0.91/1.28 Y = Z }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 Y := Y
% 0.91/1.28 Z := Z
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 2 ==> 2
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (37) {G0,W10,D2,L3,V3,M3} I { ! rinvR( X, Y ), ! rinvR( X, Z )
% 0.91/1.28 , alpha8( X, Y, Z ) }.
% 0.91/1.28 parent0: (4086) {G0,W10,D2,L3,V3,M3} { ! rinvR( X, Y ), ! rinvR( X, Z ),
% 0.91/1.28 alpha8( X, Y, Z ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 Y := Y
% 0.91/1.28 Z := Z
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 2 ==> 2
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (38) {G0,W5,D3,L2,V2,M2} I { ! alpha5( X ), alpha7( skol4( Y )
% 0.91/1.28 ) }.
% 0.91/1.28 parent0: (4087) {G0,W5,D3,L2,V2,M2} { ! alpha5( X ), alpha7( skol4( Y ) )
% 0.91/1.28 }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 Y := Y
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (39) {G0,W6,D3,L2,V1,M2} I { ! alpha5( X ), rinvR( X, skol4( X
% 0.91/1.28 ) ) }.
% 0.91/1.28 parent0: (4088) {G0,W6,D3,L2,V1,M2} { ! alpha5( X ), rinvR( X, skol4( X )
% 0.91/1.28 ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (41) {G0,W7,D2,L3,V2,M3} I { ! alpha7( X ), ! rs( X, Y ), cp(
% 0.91/1.28 Y ) }.
% 0.91/1.28 parent0: (4090) {G0,W7,D2,L3,V2,M3} { ! alpha7( X ), ! rs( X, Y ), cp( Y )
% 0.91/1.28 }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 Y := Y
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 2 ==> 2
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (45) {G0,W6,D2,L2,V2,M2} I { ! rr( Y, X ), rinvR( X, Y ) }.
% 0.91/1.28 parent0: (4094) {G0,W6,D2,L2,V2,M2} { ! rr( Y, X ), rinvR( X, Y ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 Y := Y
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (46) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable(
% 0.91/1.28 i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 parent0: (4095) {G0,W2,D2,L1,V0,M1} { cUnsatisfiable(
% 0.91/1.28 i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 eqswap: (4324) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cUnsatisfiable( X ),
% 0.91/1.28 cUnsatisfiable( Y ) }.
% 0.91/1.28 parent0[0]: (0) {G0,W7,D2,L3,V2,M3} I { ! Y = X, ! cUnsatisfiable( Y ),
% 0.91/1.28 cUnsatisfiable( X ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := Y
% 0.91/1.28 Y := X
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 resolution: (4325) {G1,W5,D2,L2,V1,M2} { ! X = i2003_11_14_17_19_13721,
% 0.91/1.28 cUnsatisfiable( X ) }.
% 0.91/1.28 parent0[1]: (4324) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cUnsatisfiable( X ),
% 0.91/1.28 cUnsatisfiable( Y ) }.
% 0.91/1.28 parent1[0]: (46) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable(
% 0.91/1.28 i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := i2003_11_14_17_19_13721
% 0.91/1.28 Y := X
% 0.91/1.28 end
% 0.91/1.28 substitution1:
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 eqswap: (4326) {G1,W5,D2,L2,V1,M2} { ! i2003_11_14_17_19_13721 = X,
% 0.91/1.28 cUnsatisfiable( X ) }.
% 0.91/1.28 parent0[0]: (4325) {G1,W5,D2,L2,V1,M2} { ! X = i2003_11_14_17_19_13721,
% 0.91/1.28 cUnsatisfiable( X ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (49) {G1,W5,D2,L2,V1,M2} R(0,46) { ! i2003_11_14_17_19_13721 =
% 0.91/1.28 X, cUnsatisfiable( X ) }.
% 0.91/1.28 parent0: (4326) {G1,W5,D2,L2,V1,M2} { ! i2003_11_14_17_19_13721 = X,
% 0.91/1.28 cUnsatisfiable( X ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 resolution: (4327) {G1,W2,D2,L1,V0,M1} { alpha2( i2003_11_14_17_19_13721 )
% 0.91/1.28 }.
% 0.91/1.28 parent0[0]: (18) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha2( X )
% 0.91/1.28 }.
% 0.91/1.28 parent1[0]: (46) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable(
% 0.91/1.28 i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := i2003_11_14_17_19_13721
% 0.91/1.28 end
% 0.91/1.28 substitution1:
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (51) {G1,W2,D2,L1,V0,M1} R(18,46) { alpha2(
% 0.91/1.28 i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 parent0: (4327) {G1,W2,D2,L1,V0,M1} { alpha2( i2003_11_14_17_19_13721 )
% 0.91/1.28 }.
% 0.91/1.28 substitution0:
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 resolution: (4328) {G1,W2,D2,L1,V0,M1} { alpha1( i2003_11_14_17_19_13721 )
% 0.91/1.28 }.
% 0.91/1.28 parent0[0]: (17) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha1( X )
% 0.91/1.28 }.
% 0.91/1.28 parent1[0]: (46) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable(
% 0.91/1.28 i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := i2003_11_14_17_19_13721
% 0.91/1.28 end
% 0.91/1.28 substitution1:
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (53) {G1,W2,D2,L1,V0,M1} R(17,46) { alpha1(
% 0.91/1.28 i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 parent0: (4328) {G1,W2,D2,L1,V0,M1} { alpha1( i2003_11_14_17_19_13721 )
% 0.91/1.28 }.
% 0.91/1.28 substitution0:
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 resolution: (4329) {G1,W5,D3,L2,V2,M2} { alpha7( skol4( Y ) ), ! alpha3( X
% 0.91/1.28 ) }.
% 0.91/1.28 parent0[0]: (38) {G0,W5,D3,L2,V2,M2} I { ! alpha5( X ), alpha7( skol4( Y )
% 0.91/1.28 ) }.
% 0.91/1.28 parent1[1]: (29) {G0,W4,D2,L2,V1,M2} I { ! alpha3( X ), alpha5( X ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 Y := Y
% 0.91/1.28 end
% 0.91/1.28 substitution1:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (60) {G1,W5,D3,L2,V2,M2} R(38,29) { alpha7( skol4( X ) ), !
% 0.91/1.28 alpha3( Y ) }.
% 0.91/1.28 parent0: (4329) {G1,W5,D3,L2,V2,M2} { alpha7( skol4( Y ) ), ! alpha3( X )
% 0.91/1.28 }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := Y
% 0.91/1.28 Y := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 resolution: (4330) {G1,W3,D3,L1,V1,M1} { alpha3( skol2( X ) ) }.
% 0.91/1.28 parent0[0]: (26) {G0,W5,D3,L2,V2,M2} I { ! alpha1( X ), alpha3( skol2( Y )
% 0.91/1.28 ) }.
% 0.91/1.28 parent1[0]: (53) {G1,W2,D2,L1,V0,M1} R(17,46) { alpha1(
% 0.91/1.28 i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := i2003_11_14_17_19_13721
% 0.91/1.28 Y := X
% 0.91/1.28 end
% 0.91/1.28 substitution1:
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (63) {G2,W3,D3,L1,V1,M1} R(26,53) { alpha3( skol2( X ) ) }.
% 0.91/1.28 parent0: (4330) {G1,W3,D3,L1,V1,M1} { alpha3( skol2( X ) ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 resolution: (4331) {G2,W3,D3,L1,V1,M1} { alpha7( skol4( X ) ) }.
% 0.91/1.28 parent0[1]: (60) {G1,W5,D3,L2,V2,M2} R(38,29) { alpha7( skol4( X ) ), !
% 0.91/1.28 alpha3( Y ) }.
% 0.91/1.28 parent1[0]: (63) {G2,W3,D3,L1,V1,M1} R(26,53) { alpha3( skol2( X ) ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 Y := skol2( Y )
% 0.91/1.28 end
% 0.91/1.28 substitution1:
% 0.91/1.28 X := Y
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (66) {G3,W3,D3,L1,V1,M1} R(63,60) { alpha7( skol4( X ) ) }.
% 0.91/1.28 parent0: (4331) {G2,W3,D3,L1,V1,M1} { alpha7( skol4( X ) ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 resolution: (4332) {G1,W3,D3,L1,V1,M1} { alpha5( skol2( X ) ) }.
% 0.91/1.28 parent0[0]: (29) {G0,W4,D2,L2,V1,M2} I { ! alpha3( X ), alpha5( X ) }.
% 0.91/1.28 parent1[0]: (63) {G2,W3,D3,L1,V1,M1} R(26,53) { alpha3( skol2( X ) ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := skol2( X )
% 0.91/1.28 end
% 0.91/1.28 substitution1:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (67) {G3,W3,D3,L1,V1,M1} R(63,29) { alpha5( skol2( X ) ) }.
% 0.91/1.28 parent0: (4332) {G1,W3,D3,L1,V1,M1} { alpha5( skol2( X ) ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 resolution: (4333) {G1,W3,D3,L1,V1,M1} { alpha6( skol2( X ) ) }.
% 0.91/1.28 parent0[0]: (30) {G0,W4,D2,L2,V1,M2} I { ! alpha3( X ), alpha6( X ) }.
% 0.91/1.28 parent1[0]: (63) {G2,W3,D3,L1,V1,M1} R(26,53) { alpha3( skol2( X ) ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := skol2( X )
% 0.91/1.28 end
% 0.91/1.28 substitution1:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (68) {G3,W3,D3,L1,V1,M1} R(63,30) { alpha6( skol2( X ) ) }.
% 0.91/1.28 parent0: (4333) {G1,W3,D3,L1,V1,M1} { alpha6( skol2( X ) ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 resolution: (4334) {G1,W3,D3,L1,V1,M1} { alpha4( skol1( X ) ) }.
% 0.91/1.28 parent0[0]: (20) {G0,W5,D3,L2,V2,M2} I { ! alpha2( X ), alpha4( skol1( Y )
% 0.91/1.28 ) }.
% 0.91/1.28 parent1[0]: (51) {G1,W2,D2,L1,V0,M1} R(18,46) { alpha2(
% 0.91/1.28 i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := i2003_11_14_17_19_13721
% 0.91/1.28 Y := X
% 0.91/1.28 end
% 0.91/1.28 substitution1:
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (73) {G2,W3,D3,L1,V1,M1} R(20,51) { alpha4( skol1( X ) ) }.
% 0.91/1.28 parent0: (4334) {G1,W3,D3,L1,V1,M1} { alpha4( skol1( X ) ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 resolution: (4335) {G1,W3,D3,L1,V1,M1} { ! cp( skol1( X ) ) }.
% 0.91/1.28 parent0[0]: (24) {G0,W4,D2,L2,V1,M2} I { ! alpha4( X ), ! cp( X ) }.
% 0.91/1.28 parent1[0]: (73) {G2,W3,D3,L1,V1,M1} R(20,51) { alpha4( skol1( X ) ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := skol1( X )
% 0.91/1.28 end
% 0.91/1.28 substitution1:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (77) {G3,W3,D3,L1,V1,M1} R(73,24) { ! cp( skol1( X ) ) }.
% 0.91/1.28 parent0: (4335) {G1,W3,D3,L1,V1,M1} { ! cp( skol1( X ) ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 resolution: (4336) {G1,W6,D4,L1,V1,M1} { rinvR( skol2( X ), skol4( skol2(
% 0.91/1.28 X ) ) ) }.
% 0.91/1.28 parent0[0]: (39) {G0,W6,D3,L2,V1,M2} I { ! alpha5( X ), rinvR( X, skol4( X
% 0.91/1.28 ) ) }.
% 0.91/1.28 parent1[0]: (67) {G3,W3,D3,L1,V1,M1} R(63,29) { alpha5( skol2( X ) ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := skol2( X )
% 0.91/1.28 end
% 0.91/1.28 substitution1:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (104) {G4,W6,D4,L1,V1,M1} R(39,67) { rinvR( skol2( X ), skol4
% 0.91/1.28 ( skol2( X ) ) ) }.
% 0.91/1.28 parent0: (4336) {G1,W6,D4,L1,V1,M1} { rinvR( skol2( X ), skol4( skol2( X )
% 0.91/1.28 ) ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 resolution: (4337) {G1,W4,D3,L1,V0,M1} { rr( i2003_11_14_17_19_13721,
% 0.91/1.28 skol2( i2003_11_14_17_19_13721 ) ) }.
% 0.91/1.28 parent0[0]: (27) {G0,W6,D3,L2,V1,M2} I { ! alpha1( X ), rr( X, skol2( X ) )
% 0.91/1.28 }.
% 0.91/1.28 parent1[0]: (53) {G1,W2,D2,L1,V0,M1} R(17,46) { alpha1(
% 0.91/1.28 i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := i2003_11_14_17_19_13721
% 0.91/1.28 end
% 0.91/1.28 substitution1:
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (122) {G2,W4,D3,L1,V0,M1} R(27,53) { rr(
% 0.91/1.28 i2003_11_14_17_19_13721, skol2( i2003_11_14_17_19_13721 ) ) }.
% 0.91/1.28 parent0: (4337) {G1,W4,D3,L1,V0,M1} { rr( i2003_11_14_17_19_13721, skol2(
% 0.91/1.28 i2003_11_14_17_19_13721 ) ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 resolution: (4338) {G1,W4,D3,L1,V0,M1} { rinvR( skol2(
% 0.91/1.28 i2003_11_14_17_19_13721 ), i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 parent0[0]: (45) {G0,W6,D2,L2,V2,M2} I { ! rr( Y, X ), rinvR( X, Y ) }.
% 0.91/1.28 parent1[0]: (122) {G2,W4,D3,L1,V0,M1} R(27,53) { rr(
% 0.91/1.28 i2003_11_14_17_19_13721, skol2( i2003_11_14_17_19_13721 ) ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := skol2( i2003_11_14_17_19_13721 )
% 0.91/1.28 Y := i2003_11_14_17_19_13721
% 0.91/1.28 end
% 0.91/1.28 substitution1:
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (125) {G3,W4,D3,L1,V0,M1} R(122,45) { rinvR( skol2(
% 0.91/1.28 i2003_11_14_17_19_13721 ), i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 parent0: (4338) {G1,W4,D3,L1,V0,M1} { rinvR( skol2(
% 0.91/1.28 i2003_11_14_17_19_13721 ), i2003_11_14_17_19_13721 ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 resolution: (4339) {G1,W6,D3,L2,V1,M2} { rs( X, skol1( X ) ), !
% 0.91/1.28 cUnsatisfiable( X ) }.
% 0.91/1.28 parent0[0]: (21) {G0,W6,D3,L2,V1,M2} I { ! alpha2( X ), rs( X, skol1( X ) )
% 0.91/1.28 }.
% 0.91/1.28 parent1[1]: (18) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha2( X )
% 0.91/1.28 }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 substitution1:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 subsumption: (147) {G1,W6,D3,L2,V1,M2} R(21,18) { rs( X, skol1( X ) ), !
% 0.91/1.28 cUnsatisfiable( X ) }.
% 0.91/1.28 parent0: (4339) {G1,W6,D3,L2,V1,M2} { rs( X, skol1( X ) ), !
% 0.91/1.28 cUnsatisfiable( X ) }.
% 0.91/1.28 substitution0:
% 0.91/1.28 X := X
% 0.91/1.28 end
% 0.91/1.28 permutation0:
% 0.91/1.28 0 ==> 0
% 0.91/1.28 1 ==> 1
% 0.91/1.28 end
% 0.91/1.28
% 0.91/1.28 resolution: (4340) {G1,W7,D3,L3,V1,M3} { ! alpha7( X ), cp( skol1( X ) ),
% 0.91/1.28 ! cUnsatisfiable( X ) }.
% 0.91/1.28 parent0[1]: (41) {G0,W7,D2,L3,V2,M3} I { ! alphaCputime limit exceeded (core dumped)
%------------------------------------------------------------------------------