%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : KRS114+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n021.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Sun Jul 17 02:42:18 EDT 2022
% Result : Unsatisfiable 0.73s 1.35s
% Output : Refutation 0.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS114+1 : TPTP v8.1.0. Released v3.1.0.
% 0.07/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n021.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Tue Jun 7 07:11:06 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.73/1.35 *** allocated 10000 integers for termspace/termends
% 0.73/1.35 *** allocated 10000 integers for clauses
% 0.73/1.35 *** allocated 10000 integers for justifications
% 0.73/1.35 Bliksem 1.12
% 0.73/1.35
% 0.73/1.35
% 0.73/1.35 Automatic Strategy Selection
% 0.73/1.35
% 0.73/1.35
% 0.73/1.35 Clauses:
% 0.73/1.35
% 0.73/1.35 { ! Y = X, ! cUnsatisfiable( Y ), cUnsatisfiable( X ) }.
% 0.73/1.35 { ! Y = X, ! ca_Ax3( Y ), ca_Ax3( X ) }.
% 0.73/1.35 { ! Y = X, ! ca_Ax4( Y ), ca_Ax4( X ) }.
% 0.73/1.35 { ! Y = X, ! ca_Vx5( Y ), ca_Vx5( X ) }.
% 0.73/1.35 { ! Y = X, ! cowlNothing( Y ), cowlNothing( X ) }.
% 0.73/1.35 { ! Y = X, ! cowlThing( Y ), cowlThing( X ) }.
% 0.73/1.35 { ! Y = X, ! cp( Y ), cp( X ) }.
% 0.73/1.35 { ! Y = X, ! cpxcomp( Y ), cpxcomp( X ) }.
% 0.73/1.35 { ! Y = X, ! cq( Y ), cq( X ) }.
% 0.73/1.35 { ! Y = X, ! cqxcomp( Y ), cqxcomp( X ) }.
% 0.73/1.35 { ! Z = X, ! ra_Px1( Z, Y ), ra_Px1( X, Y ) }.
% 0.73/1.35 { ! Z = X, ! ra_Px1( Y, Z ), ra_Px1( Y, X ) }.
% 0.73/1.35 { ! Z = X, ! ra_Px2( Z, Y ), ra_Px2( X, Y ) }.
% 0.73/1.35 { ! Z = X, ! ra_Px2( Y, Z ), ra_Px2( Y, X ) }.
% 0.73/1.35 { ! Z = X, ! rinvR( Z, Y ), rinvR( X, Y ) }.
% 0.73/1.35 { ! Z = X, ! rinvR( Y, Z ), rinvR( Y, X ) }.
% 0.73/1.35 { ! Z = X, ! rr( Z, Y ), rr( X, Y ) }.
% 0.73/1.35 { ! Z = X, ! rr( Y, Z ), rr( Y, X ) }.
% 0.73/1.35 { ! Z = X, ! rs( Z, Y ), rs( X, Y ) }.
% 0.73/1.35 { ! Z = X, ! rs( Y, Z ), rs( Y, X ) }.
% 0.73/1.35 { ! Y = X, ! xsd_integer( Y ), xsd_integer( X ) }.
% 0.73/1.35 { ! Y = X, ! xsd_string( Y ), xsd_string( X ) }.
% 0.73/1.35 { cowlThing( X ) }.
% 0.73/1.35 { ! cowlNothing( X ) }.
% 0.73/1.35 { ! xsd_string( X ), ! xsd_integer( X ) }.
% 0.73/1.35 { xsd_integer( X ), xsd_string( X ) }.
% 0.73/1.35 { ! cUnsatisfiable( X ), alpha1( X ) }.
% 0.73/1.35 { ! cUnsatisfiable( X ), alpha3( X ) }.
% 0.73/1.35 { ! alpha1( X ), ! alpha3( X ), cUnsatisfiable( X ) }.
% 0.73/1.35 { ! alpha3( X ), ca_Ax3( skol1( Y ) ) }.
% 0.73/1.35 { ! alpha3( X ), rs( X, skol1( X ) ) }.
% 0.73/1.35 { ! rs( X, Y ), ! ca_Ax3( Y ), alpha3( X ) }.
% 0.73/1.35 { ! alpha1( X ), ca_Ax4( skol2( Y ) ) }.
% 0.73/1.35 { ! alpha1( X ), rr( X, skol2( X ) ) }.
% 0.73/1.35 { ! rr( X, Y ), ! ca_Ax4( Y ), alpha1( X ) }.
% 0.73/1.35 { ! cp( X ), ! ra_Px1( X, Y ) }.
% 0.73/1.35 { ra_Px1( X, skol3( X ) ), cp( X ) }.
% 0.73/1.35 { ! cpxcomp( X ), ra_Px1( X, skol4( X ) ) }.
% 0.73/1.35 { ! ra_Px1( X, Y ), cpxcomp( X ) }.
% 0.73/1.35 { ! cq( X ), ra_Px2( X, skol5( X ) ) }.
% 0.73/1.35 { ! ra_Px2( X, Y ), cq( X ) }.
% 0.73/1.35 { ! cqxcomp( X ), ! ra_Px2( X, Y ) }.
% 0.73/1.35 { ra_Px2( X, skol6( X ) ), cqxcomp( X ) }.
% 0.73/1.35 { ! ca_Ax3( X ), cqxcomp( X ) }.
% 0.73/1.35 { ! ca_Ax3( X ), cpxcomp( X ) }.
% 0.73/1.35 { ! cqxcomp( X ), ! cpxcomp( X ), ca_Ax3( X ) }.
% 0.73/1.35 { ! ca_Ax4( X ), alpha2( X ) }.
% 0.73/1.35 { ! ca_Ax4( X ), alpha4( X ) }.
% 0.73/1.35 { ! alpha2( X ), ! alpha4( X ), ca_Ax4( X ) }.
% 0.73/1.35 { ! alpha4( X ), ca_Vx5( skol7( Y ) ) }.
% 0.73/1.35 { ! alpha4( X ), rinvR( X, skol7( X ) ) }.
% 0.73/1.35 { ! rinvR( X, Y ), ! ca_Vx5( Y ), alpha4( X ) }.
% 0.73/1.35 { ! alpha2( X ), ! alpha5( X, Y, Z ), Y = Z }.
% 0.73/1.35 { alpha5( X, skol8( X ), skol10( X ) ), alpha2( X ) }.
% 0.73/1.35 { ! skol8( X ) = skol10( X ), alpha2( X ) }.
% 0.73/1.35 { ! alpha5( X, Y, Z ), rinvR( X, Y ) }.
% 0.73/1.35 { ! alpha5( X, Y, Z ), rinvR( X, Z ) }.
% 0.73/1.35 { ! rinvR( X, Y ), ! rinvR( X, Z ), alpha5( X, Y, Z ) }.
% 0.73/1.35 { ! ca_Vx5( X ), ! rs( X, Y ), cp( Y ) }.
% 0.73/1.35 { ! cp( skol9( Y ) ), ca_Vx5( X ) }.
% 0.73/1.35 { rs( X, skol9( X ) ), ca_Vx5( X ) }.
% 0.73/1.35 { ! rinvR( X, Y ), rr( Y, X ) }.
% 0.73/1.35 { ! rr( Y, X ), rinvR( X, Y ) }.
% 0.73/1.35 { cUnsatisfiable( i2003_11_14_17_21_262 ) }.
% 0.73/1.35
% 0.73/1.35 percentage equality = 0.153846, percentage horn = 0.921875
% 0.73/1.35 This is a problem with some equality
% 0.73/1.35
% 0.73/1.35
% 0.73/1.35
% 0.73/1.35 Options Used:
% 0.73/1.35
% 0.73/1.35 useres = 1
% 0.73/1.35 useparamod = 1
% 0.73/1.35 useeqrefl = 1
% 0.73/1.35 useeqfact = 1
% 0.73/1.35 usefactor = 1
% 0.73/1.35 usesimpsplitting = 0
% 0.73/1.35 usesimpdemod = 5
% 0.73/1.35 usesimpres = 3
% 0.73/1.35
% 0.73/1.35 resimpinuse = 1000
% 0.73/1.35 resimpclauses = 20000
% 0.73/1.35 substype = eqrewr
% 0.73/1.35 backwardsubs = 1
% 0.73/1.35 selectoldest = 5
% 0.73/1.35
% 0.73/1.35 litorderings [0] = split
% 0.73/1.35 litorderings [1] = extend the termordering, first sorting on arguments
% 0.73/1.35
% 0.73/1.35 termordering = kbo
% 0.73/1.35
% 0.73/1.35 litapriori = 0
% 0.73/1.35 termapriori = 1
% 0.73/1.35 litaposteriori = 0
% 0.73/1.35 termaposteriori = 0
% 0.73/1.35 demodaposteriori = 0
% 0.73/1.35 ordereqreflfact = 0
% 0.73/1.35
% 0.73/1.35 litselect = negord
% 0.73/1.35
% 0.73/1.35 maxweight = 15
% 0.73/1.35 maxdepth = 30000
% 0.73/1.35 maxlength = 115
% 0.73/1.35 maxnrvars = 195
% 0.73/1.35 excuselevel = 1
% 0.73/1.35 increasemaxweight = 1
% 0.73/1.35
% 0.73/1.35 maxselected = 10000000
% 0.73/1.35 maxnrclauses = 10000000
% 0.73/1.35
% 0.73/1.35 showgenerated = 0
% 0.73/1.35 showkept = 0
% 0.73/1.35 showselected = 0
% 0.73/1.35 showdeleted = 0
% 0.73/1.35 showresimp = 1
% 0.73/1.35 showstatus = 2000
% 0.73/1.35
% 0.73/1.35 prologoutput = 0
% 0.73/1.35 nrgoals = 5000000
% 0.73/1.35 totalproof = 1
% 0.73/1.35
% 0.73/1.35 Symbols occurring in the translation:
% 0.73/1.35
% 0.73/1.35 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.73/1.35 . [1, 2] (w:1, o:45, a:1, s:1, b:0),
% 0.73/1.35 ! [4, 1] (w:0, o:14, a:1, s:1, b:0),
% 0.73/1.35 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.73/1.35 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.73/1.35 cUnsatisfiable [37, 1] (w:1, o:19, a:1, s:1, b:0),
% 0.73/1.35 ca_Ax3 [38, 1] (w:1, o:20, a:1, s:1, b:0),
% 0.73/1.35 ca_Ax4 [39, 1] (w:1, o:21, a:1, s:1, b:0),
% 0.73/1.35 ca_Vx5 [40, 1] (w:1, o:22, a:1, s:1, b:0),
% 0.73/1.35 cowlNothing [41, 1] (w:1, o:23, a:1, s:1, b:0),
% 0.73/1.35 cowlThing [42, 1] (w:1, o:24, a:1, s:1, b:0),
% 0.73/1.35 cp [43, 1] (w:1, o:25, a:1, s:1, b:0),
% 0.73/1.35 cpxcomp [44, 1] (w:1, o:26, a:1, s:1, b:0),
% 0.73/1.35 cq [45, 1] (w:1, o:27, a:1, s:1, b:0),
% 0.73/1.35 cqxcomp [46, 1] (w:1, o:28, a:1, s:1, b:0),
% 0.73/1.35 ra_Px1 [48, 2] (w:1, o:69, a:1, s:1, b:0),
% 0.73/1.35 ra_Px2 [49, 2] (w:1, o:70, a:1, s:1, b:0),
% 0.73/1.35 rinvR [50, 2] (w:1, o:71, a:1, s:1, b:0),
% 0.73/1.35 rr [51, 2] (w:1, o:72, a:1, s:1, b:0),
% 0.73/1.35 rs [52, 2] (w:1, o:73, a:1, s:1, b:0),
% 0.73/1.35 xsd_integer [53, 1] (w:1, o:29, a:1, s:1, b:0),
% 0.73/1.35 xsd_string [54, 1] (w:1, o:30, a:1, s:1, b:0),
% 0.73/1.35 i2003_11_14_17_21_262 [59, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.73/1.35 alpha1 [60, 1] (w:1, o:31, a:1, s:1, b:1),
% 0.73/1.35 alpha2 [61, 1] (w:1, o:32, a:1, s:1, b:1),
% 0.73/1.35 alpha3 [62, 1] (w:1, o:33, a:1, s:1, b:1),
% 0.73/1.35 alpha4 [63, 1] (w:1, o:34, a:1, s:1, b:1),
% 0.73/1.35 alpha5 [64, 3] (w:1, o:74, a:1, s:1, b:1),
% 0.73/1.35 skol1 [65, 1] (w:1, o:35, a:1, s:1, b:1),
% 0.73/1.35 skol2 [66, 1] (w:1, o:37, a:1, s:1, b:1),
% 0.73/1.35 skol3 [67, 1] (w:1, o:38, a:1, s:1, b:1),
% 0.73/1.35 skol4 [68, 1] (w:1, o:39, a:1, s:1, b:1),
% 0.73/1.35 skol5 [69, 1] (w:1, o:40, a:1, s:1, b:1),
% 0.73/1.35 skol6 [70, 1] (w:1, o:41, a:1, s:1, b:1),
% 0.73/1.35 skol7 [71, 1] (w:1, o:42, a:1, s:1, b:1),
% 0.73/1.35 skol8 [72, 1] (w:1, o:43, a:1, s:1, b:1),
% 0.73/1.35 skol9 [73, 1] (w:1, o:44, a:1, s:1, b:1),
% 0.73/1.35 skol10 [74, 1] (w:1, o:36, a:1, s:1, b:1).
% 0.73/1.35
% 0.73/1.35
% 0.73/1.35 Starting Search:
% 0.73/1.35
% 0.73/1.35 *** allocated 15000 integers for clauses
% 0.73/1.35 *** allocated 22500 integers for clauses
% 0.73/1.35 *** allocated 33750 integers for clauses
% 0.73/1.35 *** allocated 15000 integers for termspace/termends
% 0.73/1.35 *** allocated 50625 integers for clauses
% 0.73/1.35 Resimplifying inuse:
% 0.73/1.35 Done
% 0.73/1.35
% 0.73/1.35 *** allocated 22500 integers for termspace/termends
% 0.73/1.35 *** allocated 75937 integers for clauses
% 0.73/1.35 *** allocated 33750 integers for termspace/termends
% 0.73/1.35 *** allocated 113905 integers for clauses
% 0.73/1.35
% 0.73/1.35 Intermediate Status:
% 0.73/1.35 Generated: 6121
% 0.73/1.35 Kept: 2006
% 0.73/1.35 Inuse: 290
% 0.73/1.35 Deleted: 22
% 0.73/1.35 Deletedinuse: 6
% 0.73/1.35
% 0.73/1.35 Resimplifying inuse:
% 0.73/1.35 Done
% 0.73/1.35
% 0.73/1.35 *** allocated 50625 integers for termspace/termends
% 0.73/1.35 *** allocated 170857 integers for clauses
% 0.73/1.35 Resimplifying inuse:
% 0.73/1.35 Done
% 0.73/1.35
% 0.73/1.35 *** allocated 75937 integers for termspace/termends
% 0.73/1.35
% 0.73/1.35 Intermediate Status:
% 0.73/1.35 Generated: 13098
% 0.73/1.35 Kept: 4011
% 0.73/1.35 Inuse: 396
% 0.73/1.35 Deleted: 39
% 0.73/1.35 Deletedinuse: 6
% 0.73/1.35
% 0.73/1.35 Resimplifying inuse:
% 0.73/1.35 Done
% 0.73/1.35
% 0.73/1.35 *** allocated 256285 integers for clauses
% 0.73/1.35
% 0.73/1.35 Bliksems!, er is een bewijs:
% 0.73/1.35 % SZS status Unsatisfiable
% 0.73/1.35 % SZS output start Refutation
% 0.73/1.35
% 0.73/1.35 (3) {G0,W7,D2,L3,V2,M3} I { ! Y = X, ! ca_Vx5( Y ), ca_Vx5( X ) }.
% 0.73/1.35 (15) {G0,W9,D2,L3,V3,M3} I { ! Z = X, ! rinvR( Y, Z ), rinvR( Y, X ) }.
% 0.73/1.35 (26) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha1( X ) }.
% 0.73/1.35 (27) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha3( X ) }.
% 0.73/1.35 (29) {G0,W5,D3,L2,V2,M2} I { ! alpha3( X ), ca_Ax3( skol1( Y ) ) }.
% 0.73/1.35 (30) {G0,W6,D3,L2,V1,M2} I { ! alpha3( X ), rs( X, skol1( X ) ) }.
% 0.73/1.35 (32) {G0,W5,D3,L2,V2,M2} I { ! alpha1( X ), ca_Ax4( skol2( Y ) ) }.
% 0.73/1.35 (33) {G0,W6,D3,L2,V1,M2} I { ! alpha1( X ), rr( X, skol2( X ) ) }.
% 0.73/1.35 (35) {G0,W5,D2,L2,V2,M2} I { ! cp( X ), ! ra_Px1( X, Y ) }.
% 0.73/1.35 (37) {G0,W6,D3,L2,V1,M2} I { ! cpxcomp( X ), ra_Px1( X, skol4( X ) ) }.
% 0.73/1.35 (44) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax3( X ), cpxcomp( X ) }.
% 0.73/1.35 (46) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax4( X ), alpha2( X ) }.
% 0.73/1.35 (47) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax4( X ), alpha4( X ) }.
% 0.73/1.35 (49) {G0,W5,D3,L2,V2,M2} I { ! alpha4( X ), ca_Vx5( skol7( Y ) ) }.
% 0.73/1.35 (50) {G0,W6,D3,L2,V1,M2} I { ! alpha4( X ), rinvR( X, skol7( X ) ) }.
% 0.73/1.35 (52) {G0,W9,D2,L3,V3,M3} I { ! alpha2( X ), ! alpha5( X, Y, Z ), Y = Z }.
% 0.73/1.35 (57) {G0,W10,D2,L3,V3,M3} I { ! rinvR( X, Y ), ! rinvR( X, Z ), alpha5( X,
% 0.73/1.35 Y, Z ) }.
% 0.73/1.35 (58) {G0,W7,D2,L3,V2,M3} I { ! ca_Vx5( X ), ! rs( X, Y ), cp( Y ) }.
% 0.73/1.35 (62) {G0,W6,D2,L2,V2,M2} I { ! rr( Y, X ), rinvR( X, Y ) }.
% 0.73/1.35 (63) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable( i2003_11_14_17_21_262 ) }.
% 0.73/1.35 (68) {G1,W2,D2,L1,V0,M1} R(27,63) { alpha3( i2003_11_14_17_21_262 ) }.
% 0.73/1.35 (73) {G1,W2,D2,L1,V0,M1} R(26,63) { alpha1( i2003_11_14_17_21_262 ) }.
% 0.73/1.35 (84) {G1,W5,D3,L2,V2,M2} R(49,47) { ca_Vx5( skol7( X ) ), ! ca_Ax4( Y ) }.
% 0.73/1.35 (89) {G2,W3,D3,L1,V1,M1} R(32,73) { ca_Ax4( skol2( X ) ) }.
% 0.73/1.35 (92) {G3,W3,D3,L1,V1,M1} R(89,84) { ca_Vx5( skol7( X ) ) }.
% 0.73/1.35 (94) {G3,W3,D3,L1,V1,M1} R(89,46) { alpha2( skol2( X ) ) }.
% 0.73/1.35 (95) {G3,W3,D3,L1,V1,M1} R(89,47) { alpha4( skol2( X ) ) }.
% 0.73/1.35 (96) {G4,W6,D3,L2,V2,M2} R(92,3) { ! skol7( X ) = Y, ca_Vx5( Y ) }.
% 0.73/1.35 (103) {G2,W3,D3,L1,V1,M1} R(29,68) { ca_Ax3( skol1( X ) ) }.
% 0.73/1.35 (111) {G3,W3,D3,L1,V1,M1} R(103,44) { cpxcomp( skol1( X ) ) }.
% 0.73/1.35 (140) {G4,W6,D4,L1,V1,M1} R(50,95) { rinvR( skol2( X ), skol7( skol2( X ) )
% 0.73/1.35 ) }.
% 0.73/1.35 (202) {G1,W4,D2,L2,V1,M2} R(37,35) { ! cpxcomp( X ), ! cp( X ) }.
% 0.73/1.35 (206) {G4,W3,D3,L1,V1,M1} R(202,111) { ! cp( skol1( X ) ) }.
% 0.73/1.35 (265) {G2,W4,D3,L1,V0,M1} R(33,73) { rr( i2003_11_14_17_21_262, skol2(
% 0.73/1.35 i2003_11_14_17_21_262 ) ) }.
% 0.73/1.35 (269) {G3,W4,D3,L1,V0,M1} R(265,62) { rinvR( skol2( i2003_11_14_17_21_262 )
% 0.73/1.35 , i2003_11_14_17_21_262 ) }.
% 0.73/1.35 (273) {G4,W7,D3,L2,V1,M2} R(269,15) { ! i2003_11_14_17_21_262 = X, rinvR(
% 0.73/1.35 skol2( i2003_11_14_17_21_262 ), X ) }.
% 0.73/1.35 (289) {G2,W4,D3,L1,V0,M1} R(30,68) { rs( i2003_11_14_17_21_262, skol1(
% 0.73/1.35 i2003_11_14_17_21_262 ) ) }.
% 0.73/1.35 (654) {G5,W2,D2,L1,V0,M1} R(58,289);r(206) { ! ca_Vx5(
% 0.73/1.35 i2003_11_14_17_21_262 ) }.
% 0.73/1.35 (671) {G6,W4,D3,L1,V1,M1} R(654,96) { ! skol7( X ) ==>
% 0.73/1.35 i2003_11_14_17_21_262 }.
% 0.73/1.35 (712) {G7,W10,D3,L3,V3,M3} P(52,671) { ! Y = i2003_11_14_17_21_262, !
% 0.73/1.35 alpha2( Z ), ! alpha5( Z, skol7( X ), Y ) }.
% 0.73/1.35 (715) {G8,W7,D3,L2,V2,M2} Q(712) { ! alpha2( X ), ! alpha5( X, skol7( Y ),
% 0.73/1.35 i2003_11_14_17_21_262 ) }.
% 0.73/1.35 (945) {G9,W6,D3,L1,V2,M1} R(715,94) { ! alpha5( skol2( X ), skol7( Y ),
% 0.73/1.35 i2003_11_14_17_21_262 ) }.
% 0.73/1.35 (947) {G10,W9,D3,L2,V2,M2} R(945,57) { ! rinvR( skol2( X ), skol7( Y ) ), !
% 0.73/1.35 rinvR( skol2( X ), i2003_11_14_17_21_262 ) }.
% 0.73/1.35 (5108) {G11,W4,D3,L1,V1,M1} R(947,140) { ! rinvR( skol2( X ),
% 0.73/1.35 i2003_11_14_17_21_262 ) }.
% 0.73/1.35 (5135) {G12,W0,D0,L0,V0,M0} R(5108,273);q { }.
% 0.73/1.35
% 0.73/1.35
% 0.73/1.35 % SZS output end Refutation
% 0.73/1.35 found a proof!
% 0.73/1.35
% 0.73/1.35
% 0.73/1.35 Unprocessed initial clauses:
% 0.73/1.35
% 0.73/1.35 (5137) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cUnsatisfiable( Y ),
% 0.73/1.35 cUnsatisfiable( X ) }.
% 0.73/1.35 (5138) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! ca_Ax3( Y ), ca_Ax3( X ) }.
% 0.73/1.35 (5139) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! ca_Ax4( Y ), ca_Ax4( X ) }.
% 0.73/1.35 (5140) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! ca_Vx5( Y ), ca_Vx5( X ) }.
% 0.73/1.35 (5141) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cowlNothing( Y ), cowlNothing( X )
% 0.73/1.35 }.
% 0.73/1.35 (5142) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cowlThing( Y ), cowlThing( X ) }.
% 0.73/1.35 (5143) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cp( Y ), cp( X ) }.
% 0.73/1.35 (5144) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cpxcomp( Y ), cpxcomp( X ) }.
% 0.73/1.35 (5145) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cq( Y ), cq( X ) }.
% 0.73/1.35 (5146) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cqxcomp( Y ), cqxcomp( X ) }.
% 0.73/1.35 (5147) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px1( Z, Y ), ra_Px1( X, Y ) }.
% 0.73/1.35 (5148) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px1( Y, Z ), ra_Px1( Y, X ) }.
% 0.73/1.35 (5149) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px2( Z, Y ), ra_Px2( X, Y ) }.
% 0.73/1.35 (5150) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px2( Y, Z ), ra_Px2( Y, X ) }.
% 0.73/1.35 (5151) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rinvR( Z, Y ), rinvR( X, Y ) }.
% 0.73/1.35 (5152) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rinvR( Y, Z ), rinvR( Y, X ) }.
% 0.73/1.35 (5153) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rr( Z, Y ), rr( X, Y ) }.
% 0.73/1.35 (5154) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rr( Y, Z ), rr( Y, X ) }.
% 0.73/1.35 (5155) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rs( Z, Y ), rs( X, Y ) }.
% 0.73/1.35 (5156) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rs( Y, Z ), rs( Y, X ) }.
% 0.73/1.35 (5157) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! xsd_integer( Y ), xsd_integer( X )
% 0.73/1.35 }.
% 0.73/1.35 (5158) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! xsd_string( Y ), xsd_string( X )
% 0.73/1.35 }.
% 0.73/1.35 (5159) {G0,W2,D2,L1,V1,M1} { cowlThing( X ) }.
% 0.73/1.35 (5160) {G0,W2,D2,L1,V1,M1} { ! cowlNothing( X ) }.
% 0.73/1.35 (5161) {G0,W4,D2,L2,V1,M2} { ! xsd_string( X ), ! xsd_integer( X ) }.
% 0.73/1.35 (5162) {G0,W4,D2,L2,V1,M2} { xsd_integer( X ), xsd_string( X ) }.
% 0.73/1.35 (5163) {G0,W4,D2,L2,V1,M2} { ! cUnsatisfiable( X ), alpha1( X ) }.
% 0.73/1.35 (5164) {G0,W4,D2,L2,V1,M2} { ! cUnsatisfiable( X ), alpha3( X ) }.
% 0.73/1.35 (5165) {G0,W6,D2,L3,V1,M3} { ! alpha1( X ), ! alpha3( X ), cUnsatisfiable
% 0.73/1.35 ( X ) }.
% 0.73/1.35 (5166) {G0,W5,D3,L2,V2,M2} { ! alpha3( X ), ca_Ax3( skol1( Y ) ) }.
% 0.73/1.35 (5167) {G0,W6,D3,L2,V1,M2} { ! alpha3( X ), rs( X, skol1( X ) ) }.
% 0.73/1.35 (5168) {G0,W7,D2,L3,V2,M3} { ! rs( X, Y ), ! ca_Ax3( Y ), alpha3( X ) }.
% 0.73/1.35 (5169) {G0,W5,D3,L2,V2,M2} { ! alpha1( X ), ca_Ax4( skol2( Y ) ) }.
% 0.73/1.35 (5170) {G0,W6,D3,L2,V1,M2} { ! alpha1( X ), rr( X, skol2( X ) ) }.
% 0.73/1.35 (5171) {G0,W7,D2,L3,V2,M3} { ! rr( X, Y ), ! ca_Ax4( Y ), alpha1( X ) }.
% 0.73/1.35 (5172) {G0,W5,D2,L2,V2,M2} { ! cp( X ), ! ra_Px1( X, Y ) }.
% 0.73/1.35 (5173) {G0,W6,D3,L2,V1,M2} { ra_Px1( X, skol3( X ) ), cp( X ) }.
% 0.73/1.35 (5174) {G0,W6,D3,L2,V1,M2} { ! cpxcomp( X ), ra_Px1( X, skol4( X ) ) }.
% 0.73/1.35 (5175) {G0,W5,D2,L2,V2,M2} { ! ra_Px1( X, Y ), cpxcomp( X ) }.
% 0.73/1.35 (5176) {G0,W6,D3,L2,V1,M2} { ! cq( X ), ra_Px2( X, skol5( X ) ) }.
% 0.73/1.35 (5177) {G0,W5,D2,L2,V2,M2} { ! ra_Px2( X, Y ), cq( X ) }.
% 0.73/1.35 (5178) {G0,W5,D2,L2,V2,M2} { ! cqxcomp( X ), ! ra_Px2( X, Y ) }.
% 0.73/1.35 (5179) {G0,W6,D3,L2,V1,M2} { ra_Px2( X, skol6( X ) ), cqxcomp( X ) }.
% 0.73/1.35 (5180) {G0,W4,D2,L2,V1,M2} { ! ca_Ax3( X ), cqxcomp( X ) }.
% 0.73/1.35 (5181) {G0,W4,D2,L2,V1,M2} { ! ca_Ax3( X ), cpxcomp( X ) }.
% 0.73/1.35 (5182) {G0,W6,D2,L3,V1,M3} { ! cqxcomp( X ), ! cpxcomp( X ), ca_Ax3( X )
% 0.73/1.35 }.
% 0.73/1.35 (5183) {G0,W4,D2,L2,V1,M2} { ! ca_Ax4( X ), alpha2( X ) }.
% 0.73/1.35 (5184) {G0,W4,D2,L2,V1,M2} { ! ca_Ax4( X ), alpha4( X ) }.
% 0.73/1.35 (5185) {G0,W6,D2,L3,V1,M3} { ! alpha2( X ), ! alpha4( X ), ca_Ax4( X ) }.
% 0.73/1.35 (5186) {G0,W5,D3,L2,V2,M2} { ! alpha4( X ), ca_Vx5( skol7( Y ) ) }.
% 0.73/1.35 (5187) {G0,W6,D3,L2,V1,M2} { ! alpha4( X ), rinvR( X, skol7( X ) ) }.
% 0.73/1.35 (5188) {G0,W7,D2,L3,V2,M3} { ! rinvR( X, Y ), ! ca_Vx5( Y ), alpha4( X )
% 0.73/1.35 }.
% 0.73/1.35 (5189) {G0,W9,D2,L3,V3,M3} { ! alpha2( X ), ! alpha5( X, Y, Z ), Y = Z }.
% 0.73/1.35 (5190) {G0,W8,D3,L2,V1,M2} { alpha5( X, skol8( X ), skol10( X ) ), alpha2
% 0.73/1.35 ( X ) }.
% 0.73/1.35 (5191) {G0,W7,D3,L2,V1,M2} { ! skol8( X ) = skol10( X ), alpha2( X ) }.
% 0.73/1.35 (5192) {G0,W7,D2,L2,V3,M2} { ! alpha5( X, Y, Z ), rinvR( X, Y ) }.
% 0.73/1.35 (5193) {G0,W7,D2,L2,V3,M2} { ! alpha5( X, Y, Z ), rinvR( X, Z ) }.
% 0.73/1.35 (5194) {G0,W10,D2,L3,V3,M3} { ! rinvR( X, Y ), ! rinvR( X, Z ), alpha5( X
% 0.73/1.35 , Y, Z ) }.
% 0.73/1.35 (5195) {G0,W7,D2,L3,V2,M3} { ! ca_Vx5( X ), ! rs( X, Y ), cp( Y ) }.
% 0.73/1.35 (5196) {G0,W5,D3,L2,V2,M2} { ! cp( skol9( Y ) ), ca_Vx5( X ) }.
% 0.73/1.35 (5197) {G0,W6,D3,L2,V1,M2} { rs( X, skol9( X ) ), ca_Vx5( X ) }.
% 0.73/1.35 (5198) {G0,W6,D2,L2,V2,M2} { ! rinvR( X, Y ), rr( Y, X ) }.
% 0.73/1.35 (5199) {G0,W6,D2,L2,V2,M2} { ! rr( Y, X ), rinvR( X, Y ) }.
% 0.73/1.35 (5200) {G0,W2,D2,L1,V0,M1} { cUnsatisfiable( i2003_11_14_17_21_262 ) }.
% 0.73/1.35
% 0.73/1.35
% 0.73/1.35 Total Proof:
% 0.73/1.35
% 0.73/1.35 subsumption: (3) {G0,W7,D2,L3,V2,M3} I { ! Y = X, ! ca_Vx5( Y ), ca_Vx5( X
% 0.73/1.35 ) }.
% 0.73/1.35 parent0: (5140) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! ca_Vx5( Y ), ca_Vx5( X )
% 0.73/1.35 }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 Y := Y
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 2 ==> 2
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (15) {G0,W9,D2,L3,V3,M3} I { ! Z = X, ! rinvR( Y, Z ), rinvR(
% 0.73/1.35 Y, X ) }.
% 0.73/1.35 parent0: (5152) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rinvR( Y, Z ), rinvR( Y,
% 0.73/1.35 X ) }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 Y := Y
% 0.73/1.35 Z := Z
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 2 ==> 2
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 *** allocated 113905 integers for termspace/termends
% 0.73/1.35 subsumption: (26) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha1( X
% 0.73/1.35 ) }.
% 0.73/1.35 parent0: (5163) {G0,W4,D2,L2,V1,M2} { ! cUnsatisfiable( X ), alpha1( X )
% 0.73/1.35 }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (27) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha3( X
% 0.73/1.35 ) }.
% 0.73/1.35 parent0: (5164) {G0,W4,D2,L2,V1,M2} { ! cUnsatisfiable( X ), alpha3( X )
% 0.73/1.35 }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (29) {G0,W5,D3,L2,V2,M2} I { ! alpha3( X ), ca_Ax3( skol1( Y )
% 0.73/1.35 ) }.
% 0.73/1.35 parent0: (5166) {G0,W5,D3,L2,V2,M2} { ! alpha3( X ), ca_Ax3( skol1( Y ) )
% 0.73/1.35 }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 Y := Y
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (30) {G0,W6,D3,L2,V1,M2} I { ! alpha3( X ), rs( X, skol1( X )
% 0.73/1.35 ) }.
% 0.73/1.35 parent0: (5167) {G0,W6,D3,L2,V1,M2} { ! alpha3( X ), rs( X, skol1( X ) )
% 0.73/1.35 }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (32) {G0,W5,D3,L2,V2,M2} I { ! alpha1( X ), ca_Ax4( skol2( Y )
% 0.73/1.35 ) }.
% 0.73/1.35 parent0: (5169) {G0,W5,D3,L2,V2,M2} { ! alpha1( X ), ca_Ax4( skol2( Y ) )
% 0.73/1.35 }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 Y := Y
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (33) {G0,W6,D3,L2,V1,M2} I { ! alpha1( X ), rr( X, skol2( X )
% 0.73/1.35 ) }.
% 0.73/1.35 parent0: (5170) {G0,W6,D3,L2,V1,M2} { ! alpha1( X ), rr( X, skol2( X ) )
% 0.73/1.35 }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (35) {G0,W5,D2,L2,V2,M2} I { ! cp( X ), ! ra_Px1( X, Y ) }.
% 0.73/1.35 parent0: (5172) {G0,W5,D2,L2,V2,M2} { ! cp( X ), ! ra_Px1( X, Y ) }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 Y := Y
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (37) {G0,W6,D3,L2,V1,M2} I { ! cpxcomp( X ), ra_Px1( X, skol4
% 0.73/1.35 ( X ) ) }.
% 0.73/1.35 parent0: (5174) {G0,W6,D3,L2,V1,M2} { ! cpxcomp( X ), ra_Px1( X, skol4( X
% 0.73/1.35 ) ) }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (44) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax3( X ), cpxcomp( X ) }.
% 0.73/1.35 parent0: (5181) {G0,W4,D2,L2,V1,M2} { ! ca_Ax3( X ), cpxcomp( X ) }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (46) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax4( X ), alpha2( X ) }.
% 0.73/1.35 parent0: (5183) {G0,W4,D2,L2,V1,M2} { ! ca_Ax4( X ), alpha2( X ) }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (47) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax4( X ), alpha4( X ) }.
% 0.73/1.35 parent0: (5184) {G0,W4,D2,L2,V1,M2} { ! ca_Ax4( X ), alpha4( X ) }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (49) {G0,W5,D3,L2,V2,M2} I { ! alpha4( X ), ca_Vx5( skol7( Y )
% 0.73/1.35 ) }.
% 0.73/1.35 parent0: (5186) {G0,W5,D3,L2,V2,M2} { ! alpha4( X ), ca_Vx5( skol7( Y ) )
% 0.73/1.35 }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 Y := Y
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (50) {G0,W6,D3,L2,V1,M2} I { ! alpha4( X ), rinvR( X, skol7( X
% 0.73/1.35 ) ) }.
% 0.73/1.35 parent0: (5187) {G0,W6,D3,L2,V1,M2} { ! alpha4( X ), rinvR( X, skol7( X )
% 0.73/1.35 ) }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (52) {G0,W9,D2,L3,V3,M3} I { ! alpha2( X ), ! alpha5( X, Y, Z
% 0.73/1.35 ), Y = Z }.
% 0.73/1.35 parent0: (5189) {G0,W9,D2,L3,V3,M3} { ! alpha2( X ), ! alpha5( X, Y, Z ),
% 0.73/1.35 Y = Z }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 Y := Y
% 0.73/1.35 Z := Z
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 2 ==> 2
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (57) {G0,W10,D2,L3,V3,M3} I { ! rinvR( X, Y ), ! rinvR( X, Z )
% 0.73/1.35 , alpha5( X, Y, Z ) }.
% 0.73/1.35 parent0: (5194) {G0,W10,D2,L3,V3,M3} { ! rinvR( X, Y ), ! rinvR( X, Z ),
% 0.73/1.35 alpha5( X, Y, Z ) }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 Y := Y
% 0.73/1.35 Z := Z
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 2 ==> 2
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (58) {G0,W7,D2,L3,V2,M3} I { ! ca_Vx5( X ), ! rs( X, Y ), cp(
% 0.73/1.35 Y ) }.
% 0.73/1.35 parent0: (5195) {G0,W7,D2,L3,V2,M3} { ! ca_Vx5( X ), ! rs( X, Y ), cp( Y )
% 0.73/1.35 }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 Y := Y
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 2 ==> 2
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (62) {G0,W6,D2,L2,V2,M2} I { ! rr( Y, X ), rinvR( X, Y ) }.
% 0.73/1.35 parent0: (5199) {G0,W6,D2,L2,V2,M2} { ! rr( Y, X ), rinvR( X, Y ) }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 Y := Y
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (63) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable(
% 0.73/1.35 i2003_11_14_17_21_262 ) }.
% 0.73/1.35 parent0: (5200) {G0,W2,D2,L1,V0,M1} { cUnsatisfiable(
% 0.73/1.35 i2003_11_14_17_21_262 ) }.
% 0.73/1.35 substitution0:
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 resolution: (5630) {G1,W2,D2,L1,V0,M1} { alpha3( i2003_11_14_17_21_262 )
% 0.73/1.35 }.
% 0.73/1.35 parent0[0]: (27) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha3( X )
% 0.73/1.35 }.
% 0.73/1.35 parent1[0]: (63) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable(
% 0.73/1.35 i2003_11_14_17_21_262 ) }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := i2003_11_14_17_21_262
% 0.73/1.35 end
% 0.73/1.35 substitution1:
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (68) {G1,W2,D2,L1,V0,M1} R(27,63) { alpha3(
% 0.73/1.35 i2003_11_14_17_21_262 ) }.
% 0.73/1.35 parent0: (5630) {G1,W2,D2,L1,V0,M1} { alpha3( i2003_11_14_17_21_262 ) }.
% 0.73/1.35 substitution0:
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 resolution: (5631) {G1,W2,D2,L1,V0,M1} { alpha1( i2003_11_14_17_21_262 )
% 0.73/1.35 }.
% 0.73/1.35 parent0[0]: (26) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha1( X )
% 0.73/1.35 }.
% 0.73/1.35 parent1[0]: (63) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable(
% 0.73/1.35 i2003_11_14_17_21_262 ) }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := i2003_11_14_17_21_262
% 0.73/1.35 end
% 0.73/1.35 substitution1:
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (73) {G1,W2,D2,L1,V0,M1} R(26,63) { alpha1(
% 0.73/1.35 i2003_11_14_17_21_262 ) }.
% 0.73/1.35 parent0: (5631) {G1,W2,D2,L1,V0,M1} { alpha1( i2003_11_14_17_21_262 ) }.
% 0.73/1.35 substitution0:
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 resolution: (5632) {G1,W5,D3,L2,V2,M2} { ca_Vx5( skol7( Y ) ), ! ca_Ax4( X
% 0.73/1.35 ) }.
% 0.73/1.35 parent0[0]: (49) {G0,W5,D3,L2,V2,M2} I { ! alpha4( X ), ca_Vx5( skol7( Y )
% 0.73/1.35 ) }.
% 0.73/1.35 parent1[1]: (47) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax4( X ), alpha4( X ) }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := X
% 0.73/1.35 Y := Y
% 0.73/1.35 end
% 0.73/1.35 substitution1:
% 0.73/1.35 X := X
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 subsumption: (84) {G1,W5,D3,L2,V2,M2} R(49,47) { ca_Vx5( skol7( X ) ), !
% 0.73/1.35 ca_Ax4( Y ) }.
% 0.73/1.35 parent0: (5632) {G1,W5,D3,L2,V2,M2} { ca_Vx5( skol7( Y ) ), ! ca_Ax4( X )
% 0.73/1.35 }.
% 0.73/1.35 substitution0:
% 0.73/1.35 X := Y
% 0.73/1.35 Y := X
% 0.73/1.35 end
% 0.73/1.35 permutation0:
% 0.73/1.35 0 ==> 0
% 0.73/1.35 1 ==> 1
% 0.73/1.35 end
% 0.73/1.35
% 0.73/1.35 resolution: (5633) {G1,W3,D3,L1,V1,M1} { ca_Ax4( skol2( X ) ) }.
% 0.73/1.35 parent0[0]: (32) {G0,W5,D3,L2,V2,M2} I { ! alpha1( X ), ca_Ax4( skol2( Y )
% 0.73/1.36 ) }.
% 0.73/1.36 parent1[0]: (73) {G1,W2,D2,L1,V0,M1} R(26,63) { alpha1(
% 0.73/1.36 i2003_11_14_17_21_262 ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := i2003_11_14_17_21_262
% 0.73/1.36 Y := X
% 0.73/1.36 end
% 0.73/1.36 substitution1:
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (89) {G2,W3,D3,L1,V1,M1} R(32,73) { ca_Ax4( skol2( X ) ) }.
% 0.73/1.36 parent0: (5633) {G1,W3,D3,L1,V1,M1} { ca_Ax4( skol2( X ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := X
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 resolution: (5634) {G2,W3,D3,L1,V1,M1} { ca_Vx5( skol7( X ) ) }.
% 0.73/1.36 parent0[1]: (84) {G1,W5,D3,L2,V2,M2} R(49,47) { ca_Vx5( skol7( X ) ), !
% 0.73/1.36 ca_Ax4( Y ) }.
% 0.73/1.36 parent1[0]: (89) {G2,W3,D3,L1,V1,M1} R(32,73) { ca_Ax4( skol2( X ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := X
% 0.73/1.36 Y := skol2( Y )
% 0.73/1.36 end
% 0.73/1.36 substitution1:
% 0.73/1.36 X := Y
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (92) {G3,W3,D3,L1,V1,M1} R(89,84) { ca_Vx5( skol7( X ) ) }.
% 0.73/1.36 parent0: (5634) {G2,W3,D3,L1,V1,M1} { ca_Vx5( skol7( X ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := X
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 resolution: (5635) {G1,W3,D3,L1,V1,M1} { alpha2( skol2( X ) ) }.
% 0.73/1.36 parent0[0]: (46) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax4( X ), alpha2( X ) }.
% 0.73/1.36 parent1[0]: (89) {G2,W3,D3,L1,V1,M1} R(32,73) { ca_Ax4( skol2( X ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := skol2( X )
% 0.73/1.36 end
% 0.73/1.36 substitution1:
% 0.73/1.36 X := X
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (94) {G3,W3,D3,L1,V1,M1} R(89,46) { alpha2( skol2( X ) ) }.
% 0.73/1.36 parent0: (5635) {G1,W3,D3,L1,V1,M1} { alpha2( skol2( X ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := X
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 resolution: (5636) {G1,W3,D3,L1,V1,M1} { alpha4( skol2( X ) ) }.
% 0.73/1.36 parent0[0]: (47) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax4( X ), alpha4( X ) }.
% 0.73/1.36 parent1[0]: (89) {G2,W3,D3,L1,V1,M1} R(32,73) { ca_Ax4( skol2( X ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := skol2( X )
% 0.73/1.36 end
% 0.73/1.36 substitution1:
% 0.73/1.36 X := X
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (95) {G3,W3,D3,L1,V1,M1} R(89,47) { alpha4( skol2( X ) ) }.
% 0.73/1.36 parent0: (5636) {G1,W3,D3,L1,V1,M1} { alpha4( skol2( X ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := X
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 eqswap: (5637) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! ca_Vx5( X ), ca_Vx5( Y )
% 0.73/1.36 }.
% 0.73/1.36 parent0[0]: (3) {G0,W7,D2,L3,V2,M3} I { ! Y = X, ! ca_Vx5( Y ), ca_Vx5( X )
% 0.73/1.36 }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := Y
% 0.73/1.36 Y := X
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 resolution: (5638) {G1,W6,D3,L2,V2,M2} { ! X = skol7( Y ), ca_Vx5( X ) }.
% 0.73/1.36 parent0[1]: (5637) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! ca_Vx5( X ), ca_Vx5( Y
% 0.73/1.36 ) }.
% 0.73/1.36 parent1[0]: (92) {G3,W3,D3,L1,V1,M1} R(89,84) { ca_Vx5( skol7( X ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := skol7( Y )
% 0.73/1.36 Y := X
% 0.73/1.36 end
% 0.73/1.36 substitution1:
% 0.73/1.36 X := Y
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 eqswap: (5639) {G1,W6,D3,L2,V2,M2} { ! skol7( Y ) = X, ca_Vx5( X ) }.
% 0.73/1.36 parent0[0]: (5638) {G1,W6,D3,L2,V2,M2} { ! X = skol7( Y ), ca_Vx5( X ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := X
% 0.73/1.36 Y := Y
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (96) {G4,W6,D3,L2,V2,M2} R(92,3) { ! skol7( X ) = Y, ca_Vx5( Y
% 0.73/1.36 ) }.
% 0.73/1.36 parent0: (5639) {G1,W6,D3,L2,V2,M2} { ! skol7( Y ) = X, ca_Vx5( X ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := Y
% 0.73/1.36 Y := X
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 1 ==> 1
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 resolution: (5640) {G1,W3,D3,L1,V1,M1} { ca_Ax3( skol1( X ) ) }.
% 0.73/1.36 parent0[0]: (29) {G0,W5,D3,L2,V2,M2} I { ! alpha3( X ), ca_Ax3( skol1( Y )
% 0.73/1.36 ) }.
% 0.73/1.36 parent1[0]: (68) {G1,W2,D2,L1,V0,M1} R(27,63) { alpha3(
% 0.73/1.36 i2003_11_14_17_21_262 ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := i2003_11_14_17_21_262
% 0.73/1.36 Y := X
% 0.73/1.36 end
% 0.73/1.36 substitution1:
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (103) {G2,W3,D3,L1,V1,M1} R(29,68) { ca_Ax3( skol1( X ) ) }.
% 0.73/1.36 parent0: (5640) {G1,W3,D3,L1,V1,M1} { ca_Ax3( skol1( X ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := X
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 resolution: (5641) {G1,W3,D3,L1,V1,M1} { cpxcomp( skol1( X ) ) }.
% 0.73/1.36 parent0[0]: (44) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax3( X ), cpxcomp( X ) }.
% 0.73/1.36 parent1[0]: (103) {G2,W3,D3,L1,V1,M1} R(29,68) { ca_Ax3( skol1( X ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := skol1( X )
% 0.73/1.36 end
% 0.73/1.36 substitution1:
% 0.73/1.36 X := X
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (111) {G3,W3,D3,L1,V1,M1} R(103,44) { cpxcomp( skol1( X ) )
% 0.73/1.36 }.
% 0.73/1.36 parent0: (5641) {G1,W3,D3,L1,V1,M1} { cpxcomp( skol1( X ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := X
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 resolution: (5642) {G1,W6,D4,L1,V1,M1} { rinvR( skol2( X ), skol7( skol2(
% 0.73/1.36 X ) ) ) }.
% 0.73/1.36 parent0[0]: (50) {G0,W6,D3,L2,V1,M2} I { ! alpha4( X ), rinvR( X, skol7( X
% 0.73/1.36 ) ) }.
% 0.73/1.36 parent1[0]: (95) {G3,W3,D3,L1,V1,M1} R(89,47) { alpha4( skol2( X ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := skol2( X )
% 0.73/1.36 end
% 0.73/1.36 substitution1:
% 0.73/1.36 X := X
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (140) {G4,W6,D4,L1,V1,M1} R(50,95) { rinvR( skol2( X ), skol7
% 0.73/1.36 ( skol2( X ) ) ) }.
% 0.73/1.36 parent0: (5642) {G1,W6,D4,L1,V1,M1} { rinvR( skol2( X ), skol7( skol2( X )
% 0.73/1.36 ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := X
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 resolution: (5643) {G1,W4,D2,L2,V1,M2} { ! cp( X ), ! cpxcomp( X ) }.
% 0.73/1.36 parent0[1]: (35) {G0,W5,D2,L2,V2,M2} I { ! cp( X ), ! ra_Px1( X, Y ) }.
% 0.73/1.36 parent1[1]: (37) {G0,W6,D3,L2,V1,M2} I { ! cpxcomp( X ), ra_Px1( X, skol4(
% 0.73/1.36 X ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := X
% 0.73/1.36 Y := skol4( X )
% 0.73/1.36 end
% 0.73/1.36 substitution1:
% 0.73/1.36 X := X
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (202) {G1,W4,D2,L2,V1,M2} R(37,35) { ! cpxcomp( X ), ! cp( X )
% 0.73/1.36 }.
% 0.73/1.36 parent0: (5643) {G1,W4,D2,L2,V1,M2} { ! cp( X ), ! cpxcomp( X ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := X
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 1
% 0.73/1.36 1 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 resolution: (5644) {G2,W3,D3,L1,V1,M1} { ! cp( skol1( X ) ) }.
% 0.73/1.36 parent0[0]: (202) {G1,W4,D2,L2,V1,M2} R(37,35) { ! cpxcomp( X ), ! cp( X )
% 0.73/1.36 }.
% 0.73/1.36 parent1[0]: (111) {G3,W3,D3,L1,V1,M1} R(103,44) { cpxcomp( skol1( X ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := skol1( X )
% 0.73/1.36 end
% 0.73/1.36 substitution1:
% 0.73/1.36 X := X
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (206) {G4,W3,D3,L1,V1,M1} R(202,111) { ! cp( skol1( X ) ) }.
% 0.73/1.36 parent0: (5644) {G2,W3,D3,L1,V1,M1} { ! cp( skol1( X ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := X
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 resolution: (5645) {G1,W4,D3,L1,V0,M1} { rr( i2003_11_14_17_21_262, skol2
% 0.73/1.36 ( i2003_11_14_17_21_262 ) ) }.
% 0.73/1.36 parent0[0]: (33) {G0,W6,D3,L2,V1,M2} I { ! alpha1( X ), rr( X, skol2( X ) )
% 0.73/1.36 }.
% 0.73/1.36 parent1[0]: (73) {G1,W2,D2,L1,V0,M1} R(26,63) { alpha1(
% 0.73/1.36 i2003_11_14_17_21_262 ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := i2003_11_14_17_21_262
% 0.73/1.36 end
% 0.73/1.36 substitution1:
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (265) {G2,W4,D3,L1,V0,M1} R(33,73) { rr( i2003_11_14_17_21_262
% 0.73/1.36 , skol2( i2003_11_14_17_21_262 ) ) }.
% 0.73/1.36 parent0: (5645) {G1,W4,D3,L1,V0,M1} { rr( i2003_11_14_17_21_262, skol2(
% 0.73/1.36 i2003_11_14_17_21_262 ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 resolution: (5646) {G1,W4,D3,L1,V0,M1} { rinvR( skol2(
% 0.73/1.36 i2003_11_14_17_21_262 ), i2003_11_14_17_21_262 ) }.
% 0.73/1.36 parent0[0]: (62) {G0,W6,D2,L2,V2,M2} I { ! rr( Y, X ), rinvR( X, Y ) }.
% 0.73/1.36 parent1[0]: (265) {G2,W4,D3,L1,V0,M1} R(33,73) { rr( i2003_11_14_17_21_262
% 0.73/1.36 , skol2( i2003_11_14_17_21_262 ) ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := skol2( i2003_11_14_17_21_262 )
% 0.73/1.36 Y := i2003_11_14_17_21_262
% 0.73/1.36 end
% 0.73/1.36 substitution1:
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 subsumption: (269) {G3,W4,D3,L1,V0,M1} R(265,62) { rinvR( skol2(
% 0.73/1.36 i2003_11_14_17_21_262 ), i2003_11_14_17_21_262 ) }.
% 0.73/1.36 parent0: (5646) {G1,W4,D3,L1,V0,M1} { rinvR( skol2( i2003_11_14_17_21_262
% 0.73/1.36 ), i2003_11_14_17_21_262 ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 end
% 0.73/1.36 permutation0:
% 0.73/1.36 0 ==> 0
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 eqswap: (5647) {G0,W9,D2,L3,V3,M3} { ! Y = X, ! rinvR( Z, X ), rinvR( Z, Y
% 0.73/1.36 ) }.
% 0.73/1.36 parent0[0]: (15) {G0,W9,D2,L3,V3,M3} I { ! Z = X, ! rinvR( Y, Z ), rinvR( Y
% 0.73/1.36 , X ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := Y
% 0.73/1.36 Y := Z
% 0.73/1.36 Z := X
% 0.73/1.36 end
% 0.73/1.36
% 0.73/1.36 resolution: (5648) {G1,W7,D3,L2,V1,M2} { ! X = i2003_11_14_17_21_262,
% 0.73/1.36 rinvR( skol2( i2003_11_14_17_21_262 ), X ) }.
% 0.73/1.36 parent0[1]: (5647) {G0,W9,D2,L3,V3,M3} { ! Y = X, ! rinvR( Z, X ), rinvR(
% 0.73/1.36 Z, Y ) }.
% 0.73/1.36 parent1[0]: (269) {G3,W4,D3,L1,V0,M1} R(265,62) { rinvR( skol2(
% 0.73/1.36 i2003_11_14_17_21_262 ), i2003_11_14_17_21_262 ) }.
% 0.73/1.36 substitution0:
% 0.73/1.36 X := i2003_11_14_17_21_262
% 32.79/33.17 Y := X
% 32.79/33.17 Z := skol2( i2003_11_14_17_21_262 )
% 32.79/33.17 end
% 32.79/33.17 substitution1:
% 32.79/33.17 end
% 32.79/33.17
% 32.79/33.17 eqswap: (5649) {G1,W7,D3,L2,V1,M2} { ! i2003_11_14_17_21_262 = X, rinvR(
% 32.79/33.17 skol2( i2003_11_14_17_21_262 ), X ) }.
% 32.79/33.17 parent0[0]: (5648) {G1,W7,D3,L2,V1,M2} { ! X = i2003_11_14_17_21_262,
% 32.79/33.17 rinvR( skol2( i2003_11_14_17_21_262 ), X ) }.
% 32.79/33.17 substitution0:
% 32.79/33.17 X := X
% 32.79/33.17 end
% 32.79/33.17
% 32.79/33.17 subsumption: (273) {G4,W7,D3,L2,V1,M2} R(269,15) { ! i2003_11_14_17_21_262
% 32.79/33.17 = X, rinvR( skol2( i2003_11_14_17_21_262 ), X ) }.
% 32.79/33.17 parent0: (5649) {G1,W7,D3,L2,V1,M2} { ! i2003_11_14_17_21_262 = X, rinvR(
% 32.79/33.17 skol2( i2003_11_14_17_21_262 ), X ) }.
% 32.79/33.17 substitution0:
% 32.79/33.17 X := X
% 32.79/33.17 end
% 32.79/33.17 permutation0:
% 32.79/33.17 0 ==> 0
% 32.79/33.17 1 ==> 1
% 32.79/33.17 end
% 32.79/33.17
% 32.79/33.17 resolution: (5650) {G1,W4,D3,L1,V0,M1} { rs( i2003_11_14_17_21_262, skol1
% 32.79/33.17 ( i2003_11_14_17_21_262 ) ) }.
% 32.79/33.17 parent0[0]: (30) {G0,W6,D3,L2,V1,M2} I { ! alpha3( X ), rs( X, skol1( X ) )
% 32.79/33.17 }.
% 32.79/33.17 parent1[0]: (68) {G1,W2,D2,L1,V0,M1} R(27,63) { alpha3(
% 32.79/33.17 i2003_11_14_17_21_262 ) }.
% 32.79/33.17 substitution0:
% 32.79/33.17 X := i2003_11_14_17_21_262
% 32.79/33.17 end
% 32.79/33.17 substitution1:
% 32.79/33.17 end
% 32.79/33.17
% 32.79/33.17 subsumption: (289) {G2,W4,D3,L1,V0,M1} R(30,68) { rs( i2003_11_14_17_21_262
% 32.79/33.17 , skol1( i2003_11_14_17_21_262 ) ) }.
% 32.79/33.17 parent0: (5650) {G1,W4,D3,L1,V0,M1} { rs( i2003_11_14_17_21_262, skol1(
% 32.79/33.17 i2003_11_14_17_21_262 ) ) }.
% 32.79/33.17 substitution0:
% 32.79/33.17 end
% 32.79/33.17 permutation0:
% 32.79/33.17 0 ==> 0
% 32.79/33.17 end
% 32.79/33.17
% 32.79/33.17 resolution: (5651) {G1,W5,D3,L2,V0,M2} { ! ca_Vx5( i2003_11_14_17_21_262 )
% 32.79/33.17 , cp( skol1( i2003_11_14_17_21_262 ) ) }.
% 32.79/33.17 parent0[1]: (58) {G0,W7,D2,L3,V2,M3} I { ! ca_Vx5( X ), ! rs( X, Y ), cp( Y
% 32.79/33.17 ) }.
% 32.79/33.17 parent1[0]: (289) {G2,W4,D3,L1,V0,M1} R(30,68) { rs( i2003_11_14_17_21_262
% 32.79/33.17 , skol1( i2003_11_14_17_21_262 ) ) }.
% 32.79/33.17 substitution0:
% 32.79/33.17 X := i2003_11_14_17_21_262
% 32.79/33.17 Y := skol1( i2003_11_14_17_21_262 )
% 32.79/33.17 end
% 32.79/33.17 substitution1:
% 32.79/33.17 end
% 32.79/33.17
% 32.79/33.17 resolution: (5652) {G2,W2,D2,L1,V0,M1} { ! ca_Vx5( i2003_11_14_17_21_262 )
% 32.79/33.17 }.
% 32.79/33.17 parent0[0]: (206) {G4,W3,D3,L1,V1,M1} R(202,111) { ! cp( skol1( X ) ) }.
% 32.79/33.17 parent1[1]: (5651) {G1,W5,D3,L2,V0,M2} { ! ca_Vx5( i2003_11_14_17_21_262 )
% 32.79/33.17 , cp( skol1( i2003_11_14_17_21_262 ) ) }.
% 32.79/33.17 substitution0:
% 32.79/33.17 X := i2003_11_14_17_21_262
% 32.79/33.17 end
% 32.79/33.17 substitution1:
% 32.79/33.17 end
% 32.79/33.17
% 32.79/33.17 subsumption: (654) {G5,W2,D2,L1,V0,M1} R(58,289);r(206) { ! ca_Vx5(
% 32.79/33.17 i2003_11_14_17_21_262 ) }.
% 32.79/33.17 parent0: (5652) {G2,W2,D2,L1,V0,M1} { ! ca_Vx5( i2003_11_14_17_21_262 )
% 32.79/33.17 }.
% 32.79/33.17 substitution0:
% 32.79/33.17 end
% 32.79/33.17 permutation0:
% 32.79/33.17 0 ==> 0
% 32.79/33.17 end
% 32.79/33.17
% 32.79/33.17 eqswap: (5653) {G4,W6,D3,L2,V2,M2} { ! Y = skol7( X ), ca_Vx5( Y ) }.
% 32.79/33.17 parent0[0]: (96) {G4,W6,D3,L2,V2,M2} R(92,3) { ! skol7( X ) = Y, ca_Vx5( Y
% 32.79/33.17 ) }.
% 32.79/33.17 substitution0:
% 32.79/33.17 X := X
% 32.79/33.17 Y := Y
% 32.79/33.17 end
% 32.79/33.17
% 32.79/33.17 resolution: (5654) {G5,W4,D3,L1,V1,M1} { ! i2003_11_14_17_21_262 = skol7(
% 32.79/33.17 X ) }.
% 32.79/33.17 parent0[0]: (654) {G5,W2,D2,L1,V0,M1} R(58,289);r(206) { ! ca_Vx5(
% 32.79/33.17 i2003_11_14_17_21_262 ) }.
% 32.79/33.17 parent1[1]: (5653) {G4,W6,D3,L2,V2,M2} { ! Y = skol7( X ), ca_Vx5( Y ) }.
% 32.79/33.17 substitution0:
% 32.79/33.17 end
% 32.79/33.17 substitution1:
% 32.79/33.17 X := X
% 32.79/33.17 Y := i2003_11_14_17_21_262
% 32.79/33.17 end
% 32.79/33.17
% 32.79/33.17 eqswap: (5655) {G5,W4,D3,L1,V1,M1} { ! skol7( X ) = i2003_11_14_17_21_262
% 32.79/33.17 }.
% 32.79/33.17 parent0[0]: (5654) {G5,W4,D3,L1,V1,M1} { ! i2003_11_14_17_21_262 = skol7(
% 32.79/33.17 X ) }.
% 32.79/33.17 substitution0:
% 32.79/33.17 X := X
% 32.79/33.17 end
% 32.79/33.17
% 32.79/33.17 subsumption: (671) {G6,W4,D3,L1,V1,M1} R(654,96) { ! skol7( X ) ==>
% 32.79/33.17 i2003_11_14_17_21_262 }.
% 32.79/33.17 parent0: (5655) {G5,W4,D3,L1,V1,M1} { ! skol7( X ) = i2003_11_14_17_21_262
% 32.79/33.17 }.
% 32.79/33.17 substitution0:
% 32.79/33.17 X := X
% 32.79/33.17 end
% 32.79/33.17 permutation0:
% 32.79/33.17 0 ==> 0
% 32.79/33.17 end
% 32.79/33.17
% 32.79/33.17 *** allocated 15000 integers for justifications
% 32.79/33.17 *** allocated 22500 integers for justifications
% 32.79/33.17 *** allocated 33750 integers for justifications
% 32.79/33.17 *** allocated 50625 integers for justifications
% 32.79/33.17 *** allocated 170857 integers for termspace/termends
% 32.79/33.17 *** allocated 75937 integers for justifications
% 32.79/33.17 *** allocated 113905 integers for justifications
% 32.79/33.17 *** allocated 384427 integers for clauses
% 32.79/33.17 *** allocated 256285 integers for termspace/termends
% 32.79/33.17 *** allocated 170857 integers for justifications
% 32.79/33.17 *** allocated 256285 integers for justifications
% 32.79/33.17 *** allocated 384427 integers for termspace/termends
% 32.79/33.17 *** allocated 384427 integers for justifications
% 32.79/33.17 *** allocated 576640 integers for clauses
% 32.79/33.17 *** allocated 576640 integers for termspace/termends
% 32.79/33.17 *** allocated 576640 integers for justifications
% 32.79/33.17 *** allocated 864960 integers for termspace/termends
% 32.79/33.17 *** aCputime limit exceeded (core dumped)
%------------------------------------------------------------------------------