%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : KRS108+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n028.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:17 EDT 2022
% Result : Unsatisfiable 13.32s 13.72s
% Output : Refutation 13.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : KRS108+1 : TPTP v8.1.0. Released v3.1.0.
% 0.06/0.12 % Command : bliksem %s
% 0.13/0.33 % Computer : n028.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % DateTime : Tue Jun 7 12:24:45 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.73/1.08 *** allocated 10000 integers for termspace/termends
% 0.73/1.08 *** allocated 10000 integers for clauses
% 0.73/1.08 *** allocated 10000 integers for justifications
% 0.73/1.08 Bliksem 1.12
% 0.73/1.08
% 0.73/1.08
% 0.73/1.08 Automatic Strategy Selection
% 0.73/1.08
% 0.73/1.08
% 0.73/1.08 Clauses:
% 0.73/1.08
% 0.73/1.08 { ! Y = X, ! cUnsatisfiable( Y ), cUnsatisfiable( X ) }.
% 0.73/1.08 { ! Y = X, ! ca_Ax14( Y ), ca_Ax14( X ) }.
% 0.73/1.08 { ! Y = X, ! ca_Cx1( Y ), ca_Cx1( X ) }.
% 0.73/1.08 { ! Y = X, ! ca_Cx1xcomp( Y ), ca_Cx1xcomp( X ) }.
% 0.73/1.08 { ! Y = X, ! ca_Cx2( Y ), ca_Cx2( X ) }.
% 0.73/1.08 { ! Y = X, ! ca_Cx2xcomp( Y ), ca_Cx2xcomp( X ) }.
% 0.73/1.08 { ! Y = X, ! ca_Cx3( Y ), ca_Cx3( X ) }.
% 0.73/1.08 { ! Y = X, ! ca_Cx3xcomp( Y ), ca_Cx3xcomp( X ) }.
% 0.73/1.08 { ! Y = X, ! cowlNothing( Y ), cowlNothing( X ) }.
% 0.73/1.08 { ! Y = X, ! cowlThing( Y ), cowlThing( X ) }.
% 0.73/1.08 { ! Y = X, ! cp1( Y ), cp1( X ) }.
% 0.73/1.08 { ! Y = X, ! cp2( Y ), cp2( X ) }.
% 0.73/1.08 { ! Y = X, ! cp2xcomp( Y ), cp2xcomp( X ) }.
% 0.73/1.08 { ! Y = X, ! cp3( Y ), cp3( X ) }.
% 0.73/1.08 { ! Y = X, ! cp3xcomp( Y ), cp3xcomp( X ) }.
% 0.73/1.08 { ! Y = X, ! cp4( Y ), cp4( X ) }.
% 0.73/1.08 { ! Y = X, ! cp4xcomp( Y ), cp4xcomp( X ) }.
% 0.73/1.08 { ! Y = X, ! cp5( Y ), cp5( X ) }.
% 0.73/1.08 { ! Y = X, ! cp5xcomp( Y ), cp5xcomp( X ) }.
% 0.73/1.08 { ! Z = X, ! ra_Px1( Z, Y ), ra_Px1( X, Y ) }.
% 0.73/1.08 { ! Z = X, ! ra_Px1( Y, Z ), ra_Px1( Y, X ) }.
% 0.73/1.08 { ! Z = X, ! ra_Px2( Z, Y ), ra_Px2( X, Y ) }.
% 0.73/1.08 { ! Z = X, ! ra_Px2( Y, Z ), ra_Px2( Y, X ) }.
% 0.73/1.08 { ! Z = X, ! ra_Px3( Z, Y ), ra_Px3( X, Y ) }.
% 0.73/1.08 { ! Z = X, ! ra_Px3( Y, Z ), ra_Px3( Y, X ) }.
% 0.73/1.08 { ! Z = X, ! ra_Px4( Z, Y ), ra_Px4( X, Y ) }.
% 0.73/1.08 { ! Z = X, ! ra_Px4( Y, Z ), ra_Px4( Y, X ) }.
% 0.73/1.08 { ! Z = X, ! ra_Px5( Z, Y ), ra_Px5( X, Y ) }.
% 0.73/1.08 { ! Z = X, ! ra_Px5( Y, Z ), ra_Px5( Y, X ) }.
% 0.73/1.08 { ! Z = X, ! ra_Px6( Z, Y ), ra_Px6( X, Y ) }.
% 0.73/1.08 { ! Z = X, ! ra_Px6( Y, Z ), ra_Px6( Y, X ) }.
% 0.73/1.08 { ! Z = X, ! ra_Px7( Z, Y ), ra_Px7( X, Y ) }.
% 0.73/1.08 { ! Z = X, ! ra_Px7( Y, Z ), ra_Px7( Y, X ) }.
% 0.73/1.08 { ! Z = X, ! rinvR( Z, Y ), rinvR( X, Y ) }.
% 0.73/1.08 { ! Z = X, ! rinvR( Y, Z ), rinvR( Y, X ) }.
% 0.73/1.08 { ! Z = X, ! rr( Z, Y ), rr( X, Y ) }.
% 0.73/1.08 { ! Z = X, ! rr( Y, Z ), rr( Y, X ) }.
% 0.73/1.08 { ! Y = X, ! xsd_integer( Y ), xsd_integer( X ) }.
% 0.73/1.08 { ! Y = X, ! xsd_string( Y ), xsd_string( X ) }.
% 0.73/1.08 { cowlThing( X ) }.
% 0.73/1.08 { ! cowlNothing( X ) }.
% 0.73/1.08 { ! xsd_string( X ), ! xsd_integer( X ) }.
% 0.73/1.08 { xsd_integer( X ), xsd_string( X ) }.
% 0.73/1.08 { ! cUnsatisfiable( X ), alpha1( X ) }.
% 0.73/1.08 { ! cUnsatisfiable( X ), cp2( X ) }.
% 0.73/1.08 { ! alpha1( X ), ! cp2( X ), cUnsatisfiable( X ) }.
% 0.73/1.08 { ! alpha1( X ), ca_Ax14( skol1( Y ) ) }.
% 0.73/1.08 { ! alpha1( X ), rinvR( X, skol1( X ) ) }.
% 0.73/1.08 { ! rinvR( X, Y ), ! ca_Ax14( Y ), alpha1( X ) }.
% 0.73/1.08 { ! cp1( X ), ca_Cx1( X ) }.
% 0.73/1.08 { ! cp2( X ), ra_Px5( X, skol2( X ) ) }.
% 0.73/1.08 { ! ra_Px5( X, Y ), cp2( X ) }.
% 0.73/1.08 { ! cp2( X ), ca_Cx2( X ) }.
% 0.73/1.08 { ! cp2xcomp( X ), ! ra_Px5( X, Y ) }.
% 0.73/1.08 { ra_Px5( X, skol3( X ) ), cp2xcomp( X ) }.
% 0.73/1.08 { ! cp3( X ), ra_Px6( X, skol4( X ) ) }.
% 0.73/1.08 { ! ra_Px6( X, Y ), cp3( X ) }.
% 0.73/1.08 { ! cp3( X ), ca_Cx3( X ) }.
% 0.73/1.08 { ! cp3xcomp( X ), ! ra_Px6( X, Y ) }.
% 0.73/1.08 { ra_Px6( X, skol5( X ) ), cp3xcomp( X ) }.
% 0.73/1.08 { ! cp4( X ), ! ra_Px7( X, Y ) }.
% 0.73/1.08 { ra_Px7( X, skol6( X ) ), cp4( X ) }.
% 0.73/1.08 { ! cp4( X ), cp5xcomp( X ) }.
% 0.73/1.08 { ! cp4xcomp( X ), ra_Px7( X, skol7( X ) ) }.
% 0.73/1.08 { ! ra_Px7( X, Y ), cp4xcomp( X ) }.
% 0.73/1.08 { ! cp5( X ), ! ra_Px4( X, Y ) }.
% 0.73/1.08 { ra_Px4( X, skol8( X ) ), cp5( X ) }.
% 0.73/1.08 { ! cp5xcomp( X ), ra_Px4( X, skol9( X ) ) }.
% 0.73/1.08 { ! ra_Px4( X, Y ), cp5xcomp( X ) }.
% 0.73/1.08 { ! ca_Ax14( X ), alpha2( X ) }.
% 0.73/1.08 { ! ca_Ax14( X ), alpha5( X ) }.
% 0.73/1.08 { ! alpha2( X ), ! alpha5( X ), ca_Ax14( X ) }.
% 0.73/1.08 { ! alpha5( X ), ! alpha7( X, Y, Z ), Y = Z }.
% 0.73/1.08 { alpha7( X, skol10( X ), skol18( X ) ), alpha5( X ) }.
% 0.73/1.08 { ! skol10( X ) = skol18( X ), alpha5( X ) }.
% 0.73/1.08 { ! alpha7( X, Y, Z ), rr( X, Y ) }.
% 0.73/1.08 { ! alpha7( X, Y, Z ), rr( X, Z ) }.
% 0.73/1.08 { ! rr( X, Y ), ! rr( X, Z ), alpha7( X, Y, Z ) }.
% 0.73/1.08 { ! alpha2( X ), cp1( skol11( Y ) ) }.
% 0.73/1.08 { ! alpha2( X ), rr( X, skol11( X ) ) }.
% 0.73/1.08 { ! rr( X, Y ), ! cp1( Y ), alpha2( X ) }.
% 0.73/1.08 { ! ca_Cx1( X ), cp2xcomp( X ) }.
% 0.73/1.08 { ! ca_Cx1( X ), alpha3( X ) }.
% 0.73/1.08 { ! cp2xcomp( X ), ! alpha3( X ), ca_Cx1( X ) }.
% 0.73/1.08 { ! alpha3( X ), cp5xcomp( X ) }.
% 0.73/1.08 { ! alpha3( X ), alpha6( X ) }.
% 0.73/1.08 { ! cp5xcomp( X ), ! alpha6( X ), alpha3( X ) }.
% 0.73/1.08 { ! alpha6( X ), cp3xcomp( X ) }.
% 0.73/1.08 { ! alpha6( X ), cp4xcomp( X ) }.
% 0.73/1.08 { ! cp3xcomp( X ), ! cp4xcomp( X ), alpha6( X ) }.
% 0.73/1.08 { ! ca_Cx1( X ), ra_Px1( X, skol12( X ) ) }.
% 0.73/1.08 { ! ra_Px1( X, Y ), ca_Cx1( X ) }.
% 0.73/1.08 { ! ca_Cx1xcomp( X ), ! ra_Px1( X, Y ) }.
% 0.73/1.08 { ra_Px1( X, skol13( X ) ), ca_Cx1xcomp( X ) }.
% 12.61/13.01 { ! ca_Cx2( X ), cp5xcomp( X ) }.
% 12.61/13.01 { ! ca_Cx2( X ), alpha4( X ) }.
% 12.61/13.01 { ! cp5xcomp( X ), ! alpha4( X ), ca_Cx2( X ) }.
% 12.61/13.01 { ! alpha4( X ), cp3xcomp( X ) }.
% 12.61/13.01 { ! alpha4( X ), cp4xcomp( X ) }.
% 12.61/13.01 { ! cp3xcomp( X ), ! cp4xcomp( X ), alpha4( X ) }.
% 12.61/13.01 { ! ca_Cx2( X ), ! ra_Px2( X, Y ) }.
% 12.61/13.01 { ra_Px2( X, skol14( X ) ), ca_Cx2( X ) }.
% 12.61/13.01 { ! ca_Cx2xcomp( X ), ra_Px2( X, skol15( X ) ) }.
% 12.61/13.01 { ! ra_Px2( X, Y ), ca_Cx2xcomp( X ) }.
% 12.61/13.01 { ! ca_Cx3( X ), ! ra_Px3( X, Y ) }.
% 12.61/13.01 { ra_Px3( X, skol16( X ) ), ca_Cx3( X ) }.
% 12.61/13.01 { ! ca_Cx3( X ), cp5xcomp( X ) }.
% 12.61/13.01 { ! ca_Cx3( X ), cp4xcomp( X ) }.
% 12.61/13.01 { ! cp5xcomp( X ), ! cp4xcomp( X ), ca_Cx3( X ) }.
% 12.61/13.01 { ! ca_Cx3xcomp( X ), ra_Px3( X, skol17( X ) ) }.
% 12.61/13.01 { ! ra_Px3( X, Y ), ca_Cx3xcomp( X ) }.
% 12.61/13.01 { ! rinvR( X, Y ), rr( Y, X ) }.
% 12.61/13.01 { ! rr( Y, X ), rinvR( X, Y ) }.
% 12.61/13.01 { cUnsatisfiable( i2003_11_14_17_21_04740 ) }.
% 12.61/13.01
% 12.61/13.01 percentage equality = 0.148551, percentage horn = 0.921053
% 12.61/13.01 This is a problem with some equality
% 12.61/13.01
% 12.61/13.01
% 12.61/13.01
% 12.61/13.01 Options Used:
% 12.61/13.01
% 12.61/13.01 useres = 1
% 12.61/13.01 useparamod = 1
% 12.61/13.01 useeqrefl = 1
% 12.61/13.01 useeqfact = 1
% 12.61/13.01 usefactor = 1
% 12.61/13.01 usesimpsplitting = 0
% 12.61/13.01 usesimpdemod = 5
% 12.61/13.01 usesimpres = 3
% 12.61/13.01
% 12.61/13.01 resimpinuse = 1000
% 12.61/13.01 resimpclauses = 20000
% 12.61/13.01 substype = eqrewr
% 12.61/13.01 backwardsubs = 1
% 12.61/13.01 selectoldest = 5
% 12.61/13.01
% 12.61/13.01 litorderings [0] = split
% 12.61/13.01 litorderings [1] = extend the termordering, first sorting on arguments
% 12.61/13.01
% 12.61/13.01 termordering = kbo
% 12.61/13.01
% 12.61/13.01 litapriori = 0
% 12.61/13.01 termapriori = 1
% 12.61/13.01 litaposteriori = 0
% 12.61/13.01 termaposteriori = 0
% 12.61/13.01 demodaposteriori = 0
% 12.61/13.01 ordereqreflfact = 0
% 12.61/13.01
% 12.61/13.01 litselect = negord
% 12.61/13.01
% 12.61/13.01 maxweight = 15
% 12.61/13.01 maxdepth = 30000
% 12.61/13.01 maxlength = 115
% 12.61/13.01 maxnrvars = 195
% 12.61/13.01 excuselevel = 1
% 12.61/13.01 increasemaxweight = 1
% 12.61/13.01
% 12.61/13.01 maxselected = 10000000
% 12.61/13.01 maxnrclauses = 10000000
% 12.61/13.01
% 12.61/13.01 showgenerated = 0
% 12.61/13.01 showkept = 0
% 12.61/13.01 showselected = 0
% 12.61/13.01 showdeleted = 0
% 12.61/13.01 showresimp = 1
% 12.61/13.01 showstatus = 2000
% 12.61/13.01
% 12.61/13.01 prologoutput = 0
% 12.61/13.01 nrgoals = 5000000
% 12.61/13.01 totalproof = 1
% 12.61/13.01
% 12.61/13.01 Symbols occurring in the translation:
% 12.61/13.01
% 12.61/13.01 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 12.61/13.01 . [1, 2] (w:1, o:64, a:1, s:1, b:0),
% 12.61/13.01 ! [4, 1] (w:0, o:14, a:1, s:1, b:0),
% 12.61/13.01 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 12.61/13.01 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 12.61/13.01 cUnsatisfiable [37, 1] (w:1, o:19, a:1, s:1, b:0),
% 12.61/13.01 ca_Ax14 [38, 1] (w:1, o:20, a:1, s:1, b:0),
% 12.61/13.01 ca_Cx1 [39, 1] (w:1, o:21, a:1, s:1, b:0),
% 12.61/13.01 ca_Cx1xcomp [40, 1] (w:1, o:22, a:1, s:1, b:0),
% 12.61/13.01 ca_Cx2 [41, 1] (w:1, o:23, a:1, s:1, b:0),
% 12.61/13.01 ca_Cx2xcomp [42, 1] (w:1, o:24, a:1, s:1, b:0),
% 12.61/13.01 ca_Cx3 [43, 1] (w:1, o:25, a:1, s:1, b:0),
% 12.61/13.01 ca_Cx3xcomp [44, 1] (w:1, o:26, a:1, s:1, b:0),
% 12.61/13.01 cowlNothing [45, 1] (w:1, o:27, a:1, s:1, b:0),
% 12.61/13.01 cowlThing [46, 1] (w:1, o:28, a:1, s:1, b:0),
% 12.61/13.01 cp1 [47, 1] (w:1, o:29, a:1, s:1, b:0),
% 12.61/13.01 cp2 [48, 1] (w:1, o:30, a:1, s:1, b:0),
% 12.61/13.01 cp2xcomp [49, 1] (w:1, o:31, a:1, s:1, b:0),
% 12.61/13.01 cp3 [50, 1] (w:1, o:32, a:1, s:1, b:0),
% 12.61/13.01 cp3xcomp [51, 1] (w:1, o:33, a:1, s:1, b:0),
% 12.61/13.01 cp4 [52, 1] (w:1, o:34, a:1, s:1, b:0),
% 12.61/13.01 cp4xcomp [53, 1] (w:1, o:35, a:1, s:1, b:0),
% 12.61/13.01 cp5 [54, 1] (w:1, o:36, a:1, s:1, b:0),
% 12.61/13.01 cp5xcomp [55, 1] (w:1, o:37, a:1, s:1, b:0),
% 12.61/13.01 ra_Px1 [57, 2] (w:1, o:88, a:1, s:1, b:0),
% 12.61/13.01 ra_Px2 [58, 2] (w:1, o:89, a:1, s:1, b:0),
% 12.61/13.01 ra_Px3 [59, 2] (w:1, o:90, a:1, s:1, b:0),
% 12.61/13.01 ra_Px4 [60, 2] (w:1, o:91, a:1, s:1, b:0),
% 12.61/13.01 ra_Px5 [61, 2] (w:1, o:92, a:1, s:1, b:0),
% 12.61/13.01 ra_Px6 [62, 2] (w:1, o:93, a:1, s:1, b:0),
% 12.61/13.01 ra_Px7 [63, 2] (w:1, o:94, a:1, s:1, b:0),
% 12.61/13.01 rinvR [64, 2] (w:1, o:95, a:1, s:1, b:0),
% 12.61/13.01 rr [65, 2] (w:1, o:96, a:1, s:1, b:0),
% 12.61/13.01 xsd_integer [66, 1] (w:1, o:38, a:1, s:1, b:0),
% 12.61/13.01 xsd_string [67, 1] (w:1, o:39, a:1, s:1, b:0),
% 12.61/13.01 i2003_11_14_17_21_04740 [72, 0] (w:1, o:13, a:1, s:1, b:0),
% 12.61/13.01 alpha1 [73, 1] (w:1, o:40, a:1, s:1, b:1),
% 12.61/13.01 alpha2 [74, 1] (w:1, o:41, a:1, s:1, b:1),
% 12.61/13.01 alpha3 [75, 1] (w:1, o:42, a:1, s:1, b:1),
% 12.61/13.01 alpha4 [76, 1] (w:1, o:43, a:1, s:1, b:1),
% 12.61/13.01 alpha5 [77, 1] (w:1, o:44, a:1, s:1, b:1),
% 12.61/13.01 alpha6 [78, 1] (w:1, o:45, a:1, s:1, b:1),
% 12.61/13.01 alpha7 [79, 3] (w:1, o:97, a:1, s:1, b:1),
% 13.32/13.72 skol1 [80, 1] (w:1, o:46, a:1, s:1, b:1),
% 13.32/13.72 skol2 [81, 1] (w:1, o:56, a:1, s:1, b:1),
% 13.32/13.72 skol3 [82, 1] (w:1, o:57, a:1, s:1, b:1),
% 13.32/13.72 skol4 [83, 1] (w:1, o:58, a:1, s:1, b:1),
% 13.32/13.72 skol5 [84, 1] (w:1, o:59, a:1, s:1, b:1),
% 13.32/13.72 skol6 [85, 1] (w:1, o:60, a:1, s:1, b:1),
% 13.32/13.72 skol7 [86, 1] (w:1, o:61, a:1, s:1, b:1),
% 13.32/13.72 skol8 [87, 1] (w:1, o:62, a:1, s:1, b:1),
% 13.32/13.72 skol9 [88, 1] (w:1, o:63, a:1, s:1, b:1),
% 13.32/13.72 skol10 [89, 1] (w:1, o:47, a:1, s:1, b:1),
% 13.32/13.72 skol11 [90, 1] (w:1, o:48, a:1, s:1, b:1),
% 13.32/13.72 skol12 [91, 1] (w:1, o:49, a:1, s:1, b:1),
% 13.32/13.72 skol13 [92, 1] (w:1, o:50, a:1, s:1, b:1),
% 13.32/13.72 skol14 [93, 1] (w:1, o:51, a:1, s:1, b:1),
% 13.32/13.72 skol15 [94, 1] (w:1, o:52, a:1, s:1, b:1),
% 13.32/13.72 skol16 [95, 1] (w:1, o:53, a:1, s:1, b:1),
% 13.32/13.72 skol17 [96, 1] (w:1, o:54, a:1, s:1, b:1),
% 13.32/13.72 skol18 [97, 1] (w:1, o:55, a:1, s:1, b:1).
% 13.32/13.72
% 13.32/13.72
% 13.32/13.72 Starting Search:
% 13.32/13.72
% 13.32/13.72 *** allocated 15000 integers for clauses
% 13.32/13.72 *** allocated 22500 integers for clauses
% 13.32/13.72 *** allocated 33750 integers for clauses
% 13.32/13.72 *** allocated 50625 integers for clauses
% 13.32/13.72 *** allocated 15000 integers for termspace/termends
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 *** allocated 75937 integers for clauses
% 13.32/13.72 *** allocated 22500 integers for termspace/termends
% 13.32/13.72 *** allocated 113905 integers for clauses
% 13.32/13.72
% 13.32/13.72 Intermediate Status:
% 13.32/13.72 Generated: 8553
% 13.32/13.72 Kept: 2012
% 13.32/13.72 Inuse: 511
% 13.32/13.72 Deleted: 30
% 13.32/13.72 Deletedinuse: 17
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 *** allocated 33750 integers for termspace/termends
% 13.32/13.72 *** allocated 170857 integers for clauses
% 13.32/13.72 *** allocated 50625 integers for termspace/termends
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72
% 13.32/13.72 Intermediate Status:
% 13.32/13.72 Generated: 25100
% 13.32/13.72 Kept: 4020
% 13.32/13.72 Inuse: 818
% 13.32/13.72 Deleted: 51
% 13.32/13.72 Deletedinuse: 18
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 *** allocated 75937 integers for termspace/termends
% 13.32/13.72 *** allocated 256285 integers for clauses
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 *** allocated 113905 integers for termspace/termends
% 13.32/13.72
% 13.32/13.72 Intermediate Status:
% 13.32/13.72 Generated: 48908
% 13.32/13.72 Kept: 6032
% 13.32/13.72 Inuse: 1164
% 13.32/13.72 Deleted: 75
% 13.32/13.72 Deletedinuse: 18
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 *** allocated 384427 integers for clauses
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72
% 13.32/13.72 Intermediate Status:
% 13.32/13.72 Generated: 60527
% 13.32/13.72 Kept: 8043
% 13.32/13.72 Inuse: 1329
% 13.32/13.72 Deleted: 75
% 13.32/13.72 Deletedinuse: 18
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 *** allocated 170857 integers for termspace/termends
% 13.32/13.72
% 13.32/13.72 Intermediate Status:
% 13.32/13.72 Generated: 69679
% 13.32/13.72 Kept: 10076
% 13.32/13.72 Inuse: 1379
% 13.32/13.72 Deleted: 75
% 13.32/13.72 Deletedinuse: 18
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 *** allocated 576640 integers for clauses
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72
% 13.32/13.72 Intermediate Status:
% 13.32/13.72 Generated: 87710
% 13.32/13.72 Kept: 12076
% 13.32/13.72 Inuse: 1472
% 13.32/13.72 Deleted: 75
% 13.32/13.72 Deletedinuse: 18
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 *** allocated 256285 integers for termspace/termends
% 13.32/13.72
% 13.32/13.72 Intermediate Status:
% 13.32/13.72 Generated: 92686
% 13.32/13.72 Kept: 14112
% 13.32/13.72 Inuse: 1514
% 13.32/13.72 Deleted: 75
% 13.32/13.72 Deletedinuse: 18
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 *** allocated 864960 integers for clauses
% 13.32/13.72
% 13.32/13.72 Intermediate Status:
% 13.32/13.72 Generated: 100966
% 13.32/13.72 Kept: 16121
% 13.32/13.72 Inuse: 1583
% 13.32/13.72 Deleted: 75
% 13.32/13.72 Deletedinuse: 18
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 *** allocated 384427 integers for termspace/termends
% 13.32/13.72
% 13.32/13.72 Intermediate Status:
% 13.32/13.72 Generated: 117156
% 13.32/13.72 Kept: 18139
% 13.32/13.72 Inuse: 1668
% 13.32/13.72 Deleted: 75
% 13.32/13.72 Deletedinuse: 18
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 Resimplifying clauses:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72
% 13.32/13.72 Intermediate Status:
% 13.32/13.72 Generated: 132060
% 13.32/13.72 Kept: 20166
% 13.32/13.72 Inuse: 1768
% 13.32/13.72 Deleted: 560
% 13.32/13.72 Deletedinuse: 18
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72
% 13.32/13.72 Intermediate Status:
% 13.32/13.72 Generated: 157330
% 13.32/13.72 Kept: 22169
% 13.32/13.72 Inuse: 1874
% 13.32/13.72 Deleted: 560
% 13.32/13.72 Deletedinuse: 18
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 *** allocated 1297440 integers for clauses
% 13.32/13.72
% 13.32/13.72 Intermediate Status:
% 13.32/13.72 Generated: 180570
% 13.32/13.72 Kept: 24962
% 13.32/13.72 Inuse: 1954
% 13.32/13.72 Deleted: 560
% 13.32/13.72 Deletedinuse: 18
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 *** allocated 576640 integers for termspace/termends
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72
% 13.32/13.72 Intermediate Status:
% 13.32/13.72 Generated: 195215
% 13.32/13.72 Kept: 27057
% 13.32/13.72 Inuse: 2010
% 13.32/13.72 Deleted: 560
% 13.32/13.72 Deletedinuse: 18
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72 Resimplifying inuse:
% 13.32/13.72 Done
% 13.32/13.72
% 13.32/13.72
% 13.32/13.72 Intermediate Status:
% 13.32/13.72 Generated: 202671
% 13.32/13.72 Kept: 29452
% 13.32/13.72 Inuse: 2025
% 13.32/13.72 Deleted: 560
% 13.32/13.72 Deletedinuse: 18
% 13.32/13.72
% 13.32/13.72
% 13.32/13.72 Bliksems!, er is een bewijs:
% 13.32/13.72 % SZS status Unsatisfiable
% 13.32/13.72 % SZS output start Refutation
% 13.32/13.72
% 13.32/13.72 (3) {G0,W7,D2,L3,V2,M3} I { ! Y = X, ! ca_Cx1xcomp( Y ), ca_Cx1xcomp( X )
% 13.32/13.72 }.
% 13.32/13.72 (43) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha1( X ) }.
% 13.32/13.72 (44) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), cp2( X ) }.
% 13.32/13.72 (46) {G0,W5,D3,L2,V2,M2} I { ! alpha1( X ), ca_Ax14( skol1( Y ) ) }.
% 13.32/13.72 (47) {G0,W6,D3,L2,V1,M2} I { ! alpha1( X ), rinvR( X, skol1( X ) ) }.
% 13.32/13.72 (49) {G0,W4,D2,L2,V1,M2} I { ! cp1( X ), ca_Cx1( X ) }.
% 13.32/13.72 (50) {G0,W6,D3,L2,V1,M2} I { ! cp2( X ), ra_Px5( X, skol2( X ) ) }.
% 13.32/13.72 (53) {G0,W5,D2,L2,V2,M2} I { ! cp2xcomp( X ), ! ra_Px5( X, Y ) }.
% 13.32/13.72 (69) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax14( X ), alpha2( X ) }.
% 13.32/13.72 (70) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax14( X ), alpha5( X ) }.
% 13.32/13.72 (72) {G0,W9,D2,L3,V3,M3} I { ! alpha5( X ), ! alpha7( X, Y, Z ), Y = Z }.
% 13.32/13.72 (77) {G0,W10,D2,L3,V3,M3} I { ! rr( X, Y ), ! rr( X, Z ), alpha7( X, Y, Z )
% 13.32/13.72 }.
% 13.32/13.72 (78) {G0,W5,D3,L2,V2,M2} I { ! alpha2( X ), cp1( skol11( Y ) ) }.
% 13.32/13.72 (79) {G0,W6,D3,L2,V1,M2} I { ! alpha2( X ), rr( X, skol11( X ) ) }.
% 13.32/13.72 (81) {G0,W4,D2,L2,V1,M2} I { ! ca_Cx1( X ), cp2xcomp( X ) }.
% 13.32/13.72 (90) {G0,W6,D3,L2,V1,M2} I { ! ca_Cx1( X ), ra_Px1( X, skol12( X ) ) }.
% 13.32/13.72 (91) {G0,W5,D2,L2,V2,M2} I { ! ra_Px1( X, Y ), ca_Cx1( X ) }.
% 13.32/13.72 (92) {G0,W5,D2,L2,V2,M2} I { ! ca_Cx1xcomp( X ), ! ra_Px1( X, Y ) }.
% 13.32/13.72 (93) {G0,W6,D3,L2,V1,M2} I { ra_Px1( X, skol13( X ) ), ca_Cx1xcomp( X ) }.
% 13.32/13.72 (111) {G0,W6,D2,L2,V2,M2} I { ! rinvR( X, Y ), rr( Y, X ) }.
% 13.32/13.72 (113) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable( i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 (167) {G1,W2,D2,L1,V0,M1} R(44,113) { cp2( i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 (194) {G1,W2,D2,L1,V0,M1} R(43,113) { alpha1( i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 (276) {G1,W5,D2,L2,V2,M2} R(53,81) { ! ra_Px5( X, Y ), ! ca_Cx1( X ) }.
% 13.32/13.72 (317) {G1,W5,D3,L2,V2,M2} R(78,49) { ! alpha2( X ), ca_Cx1( skol11( Y ) )
% 13.32/13.72 }.
% 13.32/13.72 (347) {G2,W5,D3,L2,V2,M2} R(317,69) { ca_Cx1( skol11( X ) ), ! ca_Ax14( Y )
% 13.32/13.72 }.
% 13.32/13.72 (360) {G2,W3,D3,L1,V1,M1} R(46,194) { ca_Ax14( skol1( X ) ) }.
% 13.32/13.72 (368) {G3,W3,D3,L1,V1,M1} R(360,347) { ca_Cx1( skol11( X ) ) }.
% 13.32/13.72 (375) {G3,W3,D3,L1,V1,M1} R(360,69) { alpha2( skol1( X ) ) }.
% 13.32/13.72 (376) {G3,W3,D3,L1,V1,M1} R(360,70) { alpha5( skol1( X ) ) }.
% 13.32/13.72 (458) {G2,W4,D3,L1,V0,M1} R(47,194) { rinvR( i2003_11_14_17_21_04740, skol1
% 13.32/13.72 ( i2003_11_14_17_21_04740 ) ) }.
% 13.32/13.72 (465) {G3,W4,D3,L1,V0,M1} R(458,111) { rr( skol1( i2003_11_14_17_21_04740 )
% 13.32/13.72 , i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 (487) {G2,W4,D2,L2,V1,M2} R(50,276) { ! cp2( X ), ! ca_Cx1( X ) }.
% 13.32/13.72 (499) {G3,W2,D2,L1,V0,M1} R(487,167) { ! ca_Cx1( i2003_11_14_17_21_04740 )
% 13.32/13.72 }.
% 13.32/13.72 (501) {G4,W3,D2,L1,V1,M1} R(499,91) { ! ra_Px1( i2003_11_14_17_21_04740, X
% 13.32/13.72 ) }.
% 13.32/13.72 (899) {G1,W11,D2,L4,V3,M4} R(77,72) { ! rr( X, Y ), ! rr( X, Z ), ! alpha5
% 13.32/13.72 ( X ), Y = Z }.
% 13.32/13.72 (922) {G4,W6,D4,L1,V1,M1} R(79,375) { rr( skol1( X ), skol11( skol1( X ) )
% 13.32/13.72 ) }.
% 13.32/13.72 (1046) {G1,W4,D2,L2,V1,M2} R(90,92) { ! ca_Cx1( X ), ! ca_Cx1xcomp( X ) }.
% 13.32/13.72 (1052) {G4,W3,D3,L1,V1,M1} R(1046,368) { ! ca_Cx1xcomp( skol11( X ) ) }.
% 13.32/13.72 (1055) {G5,W6,D3,L2,V2,M2} R(1052,3) { ! X = skol11( Y ), ! ca_Cx1xcomp( X
% 13.32/13.72 ) }.
% 13.32/13.72 (2529) {G6,W8,D3,L2,V2,M2} R(1055,93) { ! X = skol11( Y ), ra_Px1( X,
% 13.32/13.72 skol13( X ) ) }.
% 13.32/13.72 (28430) {G4,W7,D3,L2,V1,M2} R(899,465);r(376) { ! rr( skol1(
% 13.32/13.72 i2003_11_14_17_21_04740 ), X ), i2003_11_14_17_21_04740 = X }.
% 13.32/13.72 (28812) {G7,W5,D3,L1,V1,M1} R(28430,2529);r(501) { ! rr( skol1(
% 13.32/13.72 i2003_11_14_17_21_04740 ), skol11( X ) ) }.
% 13.32/13.72 (29468) {G8,W0,D0,L0,V0,M0} R(28812,922) { }.
% 13.32/13.72
% 13.32/13.72
% 13.32/13.72 % SZS output end Refutation
% 13.32/13.72 found a proof!
% 13.32/13.72
% 13.32/13.72
% 13.32/13.72 Unprocessed initial clauses:
% 13.32/13.72
% 13.32/13.72 (29470) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cUnsatisfiable( Y ),
% 13.32/13.72 cUnsatisfiable( X ) }.
% 13.32/13.72 (29471) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! ca_Ax14( Y ), ca_Ax14( X ) }.
% 13.32/13.72 (29472) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! ca_Cx1( Y ), ca_Cx1( X ) }.
% 13.32/13.72 (29473) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! ca_Cx1xcomp( Y ), ca_Cx1xcomp( X
% 13.32/13.72 ) }.
% 13.32/13.72 (29474) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! ca_Cx2( Y ), ca_Cx2( X ) }.
% 13.32/13.72 (29475) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! ca_Cx2xcomp( Y ), ca_Cx2xcomp( X
% 13.32/13.72 ) }.
% 13.32/13.72 (29476) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! ca_Cx3( Y ), ca_Cx3( X ) }.
% 13.32/13.72 (29477) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! ca_Cx3xcomp( Y ), ca_Cx3xcomp( X
% 13.32/13.72 ) }.
% 13.32/13.72 (29478) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cowlNothing( Y ), cowlNothing( X
% 13.32/13.72 ) }.
% 13.32/13.72 (29479) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cowlThing( Y ), cowlThing( X )
% 13.32/13.72 }.
% 13.32/13.72 (29480) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cp1( Y ), cp1( X ) }.
% 13.32/13.72 (29481) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cp2( Y ), cp2( X ) }.
% 13.32/13.72 (29482) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cp2xcomp( Y ), cp2xcomp( X ) }.
% 13.32/13.72 (29483) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cp3( Y ), cp3( X ) }.
% 13.32/13.72 (29484) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cp3xcomp( Y ), cp3xcomp( X ) }.
% 13.32/13.72 (29485) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cp4( Y ), cp4( X ) }.
% 13.32/13.72 (29486) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cp4xcomp( Y ), cp4xcomp( X ) }.
% 13.32/13.72 (29487) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cp5( Y ), cp5( X ) }.
% 13.32/13.72 (29488) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! cp5xcomp( Y ), cp5xcomp( X ) }.
% 13.32/13.72 (29489) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px1( Z, Y ), ra_Px1( X, Y )
% 13.32/13.72 }.
% 13.32/13.72 (29490) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px1( Y, Z ), ra_Px1( Y, X )
% 13.32/13.72 }.
% 13.32/13.72 (29491) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px2( Z, Y ), ra_Px2( X, Y )
% 13.32/13.72 }.
% 13.32/13.72 (29492) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px2( Y, Z ), ra_Px2( Y, X )
% 13.32/13.72 }.
% 13.32/13.72 (29493) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px3( Z, Y ), ra_Px3( X, Y )
% 13.32/13.72 }.
% 13.32/13.72 (29494) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px3( Y, Z ), ra_Px3( Y, X )
% 13.32/13.72 }.
% 13.32/13.72 (29495) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px4( Z, Y ), ra_Px4( X, Y )
% 13.32/13.72 }.
% 13.32/13.72 (29496) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px4( Y, Z ), ra_Px4( Y, X )
% 13.32/13.72 }.
% 13.32/13.72 (29497) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px5( Z, Y ), ra_Px5( X, Y )
% 13.32/13.72 }.
% 13.32/13.72 (29498) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px5( Y, Z ), ra_Px5( Y, X )
% 13.32/13.72 }.
% 13.32/13.72 (29499) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px6( Z, Y ), ra_Px6( X, Y )
% 13.32/13.72 }.
% 13.32/13.72 (29500) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px6( Y, Z ), ra_Px6( Y, X )
% 13.32/13.72 }.
% 13.32/13.72 (29501) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px7( Z, Y ), ra_Px7( X, Y )
% 13.32/13.72 }.
% 13.32/13.72 (29502) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! ra_Px7( Y, Z ), ra_Px7( Y, X )
% 13.32/13.72 }.
% 13.32/13.72 (29503) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rinvR( Z, Y ), rinvR( X, Y ) }.
% 13.32/13.72 (29504) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rinvR( Y, Z ), rinvR( Y, X ) }.
% 13.32/13.72 (29505) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rr( Z, Y ), rr( X, Y ) }.
% 13.32/13.72 (29506) {G0,W9,D2,L3,V3,M3} { ! Z = X, ! rr( Y, Z ), rr( Y, X ) }.
% 13.32/13.72 (29507) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! xsd_integer( Y ), xsd_integer( X
% 13.32/13.72 ) }.
% 13.32/13.72 (29508) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! xsd_string( Y ), xsd_string( X )
% 13.32/13.72 }.
% 13.32/13.72 (29509) {G0,W2,D2,L1,V1,M1} { cowlThing( X ) }.
% 13.32/13.72 (29510) {G0,W2,D2,L1,V1,M1} { ! cowlNothing( X ) }.
% 13.32/13.72 (29511) {G0,W4,D2,L2,V1,M2} { ! xsd_string( X ), ! xsd_integer( X ) }.
% 13.32/13.72 (29512) {G0,W4,D2,L2,V1,M2} { xsd_integer( X ), xsd_string( X ) }.
% 13.32/13.72 (29513) {G0,W4,D2,L2,V1,M2} { ! cUnsatisfiable( X ), alpha1( X ) }.
% 13.32/13.72 (29514) {G0,W4,D2,L2,V1,M2} { ! cUnsatisfiable( X ), cp2( X ) }.
% 13.32/13.72 (29515) {G0,W6,D2,L3,V1,M3} { ! alpha1( X ), ! cp2( X ), cUnsatisfiable( X
% 13.32/13.72 ) }.
% 13.32/13.72 (29516) {G0,W5,D3,L2,V2,M2} { ! alpha1( X ), ca_Ax14( skol1( Y ) ) }.
% 13.32/13.72 (29517) {G0,W6,D3,L2,V1,M2} { ! alpha1( X ), rinvR( X, skol1( X ) ) }.
% 13.32/13.72 (29518) {G0,W7,D2,L3,V2,M3} { ! rinvR( X, Y ), ! ca_Ax14( Y ), alpha1( X )
% 13.32/13.72 }.
% 13.32/13.72 (29519) {G0,W4,D2,L2,V1,M2} { ! cp1( X ), ca_Cx1( X ) }.
% 13.32/13.72 (29520) {G0,W6,D3,L2,V1,M2} { ! cp2( X ), ra_Px5( X, skol2( X ) ) }.
% 13.32/13.72 (29521) {G0,W5,D2,L2,V2,M2} { ! ra_Px5( X, Y ), cp2( X ) }.
% 13.32/13.72 (29522) {G0,W4,D2,L2,V1,M2} { ! cp2( X ), ca_Cx2( X ) }.
% 13.32/13.72 (29523) {G0,W5,D2,L2,V2,M2} { ! cp2xcomp( X ), ! ra_Px5( X, Y ) }.
% 13.32/13.72 (29524) {G0,W6,D3,L2,V1,M2} { ra_Px5( X, skol3( X ) ), cp2xcomp( X ) }.
% 13.32/13.72 (29525) {G0,W6,D3,L2,V1,M2} { ! cp3( X ), ra_Px6( X, skol4( X ) ) }.
% 13.32/13.72 (29526) {G0,W5,D2,L2,V2,M2} { ! ra_Px6( X, Y ), cp3( X ) }.
% 13.32/13.72 (29527) {G0,W4,D2,L2,V1,M2} { ! cp3( X ), ca_Cx3( X ) }.
% 13.32/13.72 (29528) {G0,W5,D2,L2,V2,M2} { ! cp3xcomp( X ), ! ra_Px6( X, Y ) }.
% 13.32/13.72 (29529) {G0,W6,D3,L2,V1,M2} { ra_Px6( X, skol5( X ) ), cp3xcomp( X ) }.
% 13.32/13.72 (29530) {G0,W5,D2,L2,V2,M2} { ! cp4( X ), ! ra_Px7( X, Y ) }.
% 13.32/13.72 (29531) {G0,W6,D3,L2,V1,M2} { ra_Px7( X, skol6( X ) ), cp4( X ) }.
% 13.32/13.72 (29532) {G0,W4,D2,L2,V1,M2} { ! cp4( X ), cp5xcomp( X ) }.
% 13.32/13.72 (29533) {G0,W6,D3,L2,V1,M2} { ! cp4xcomp( X ), ra_Px7( X, skol7( X ) ) }.
% 13.32/13.72 (29534) {G0,W5,D2,L2,V2,M2} { ! ra_Px7( X, Y ), cp4xcomp( X ) }.
% 13.32/13.72 (29535) {G0,W5,D2,L2,V2,M2} { ! cp5( X ), ! ra_Px4( X, Y ) }.
% 13.32/13.72 (29536) {G0,W6,D3,L2,V1,M2} { ra_Px4( X, skol8( X ) ), cp5( X ) }.
% 13.32/13.72 (29537) {G0,W6,D3,L2,V1,M2} { ! cp5xcomp( X ), ra_Px4( X, skol9( X ) ) }.
% 13.32/13.72 (29538) {G0,W5,D2,L2,V2,M2} { ! ra_Px4( X, Y ), cp5xcomp( X ) }.
% 13.32/13.72 (29539) {G0,W4,D2,L2,V1,M2} { ! ca_Ax14( X ), alpha2( X ) }.
% 13.32/13.72 (29540) {G0,W4,D2,L2,V1,M2} { ! ca_Ax14( X ), alpha5( X ) }.
% 13.32/13.72 (29541) {G0,W6,D2,L3,V1,M3} { ! alpha2( X ), ! alpha5( X ), ca_Ax14( X )
% 13.32/13.72 }.
% 13.32/13.72 (29542) {G0,W9,D2,L3,V3,M3} { ! alpha5( X ), ! alpha7( X, Y, Z ), Y = Z
% 13.32/13.72 }.
% 13.32/13.72 (29543) {G0,W8,D3,L2,V1,M2} { alpha7( X, skol10( X ), skol18( X ) ),
% 13.32/13.72 alpha5( X ) }.
% 13.32/13.72 (29544) {G0,W7,D3,L2,V1,M2} { ! skol10( X ) = skol18( X ), alpha5( X ) }.
% 13.32/13.72 (29545) {G0,W7,D2,L2,V3,M2} { ! alpha7( X, Y, Z ), rr( X, Y ) }.
% 13.32/13.72 (29546) {G0,W7,D2,L2,V3,M2} { ! alpha7( X, Y, Z ), rr( X, Z ) }.
% 13.32/13.72 (29547) {G0,W10,D2,L3,V3,M3} { ! rr( X, Y ), ! rr( X, Z ), alpha7( X, Y, Z
% 13.32/13.72 ) }.
% 13.32/13.72 (29548) {G0,W5,D3,L2,V2,M2} { ! alpha2( X ), cp1( skol11( Y ) ) }.
% 13.32/13.72 (29549) {G0,W6,D3,L2,V1,M2} { ! alpha2( X ), rr( X, skol11( X ) ) }.
% 13.32/13.72 (29550) {G0,W7,D2,L3,V2,M3} { ! rr( X, Y ), ! cp1( Y ), alpha2( X ) }.
% 13.32/13.72 (29551) {G0,W4,D2,L2,V1,M2} { ! ca_Cx1( X ), cp2xcomp( X ) }.
% 13.32/13.72 (29552) {G0,W4,D2,L2,V1,M2} { ! ca_Cx1( X ), alpha3( X ) }.
% 13.32/13.72 (29553) {G0,W6,D2,L3,V1,M3} { ! cp2xcomp( X ), ! alpha3( X ), ca_Cx1( X )
% 13.32/13.72 }.
% 13.32/13.72 (29554) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), cp5xcomp( X ) }.
% 13.32/13.72 (29555) {G0,W4,D2,L2,V1,M2} { ! alpha3( X ), alpha6( X ) }.
% 13.32/13.72 (29556) {G0,W6,D2,L3,V1,M3} { ! cp5xcomp( X ), ! alpha6( X ), alpha3( X )
% 13.32/13.72 }.
% 13.32/13.72 (29557) {G0,W4,D2,L2,V1,M2} { ! alpha6( X ), cp3xcomp( X ) }.
% 13.32/13.72 (29558) {G0,W4,D2,L2,V1,M2} { ! alpha6( X ), cp4xcomp( X ) }.
% 13.32/13.72 (29559) {G0,W6,D2,L3,V1,M3} { ! cp3xcomp( X ), ! cp4xcomp( X ), alpha6( X
% 13.32/13.72 ) }.
% 13.32/13.72 (29560) {G0,W6,D3,L2,V1,M2} { ! ca_Cx1( X ), ra_Px1( X, skol12( X ) ) }.
% 13.32/13.72 (29561) {G0,W5,D2,L2,V2,M2} { ! ra_Px1( X, Y ), ca_Cx1( X ) }.
% 13.32/13.72 (29562) {G0,W5,D2,L2,V2,M2} { ! ca_Cx1xcomp( X ), ! ra_Px1( X, Y ) }.
% 13.32/13.72 (29563) {G0,W6,D3,L2,V1,M2} { ra_Px1( X, skol13( X ) ), ca_Cx1xcomp( X )
% 13.32/13.72 }.
% 13.32/13.72 (29564) {G0,W4,D2,L2,V1,M2} { ! ca_Cx2( X ), cp5xcomp( X ) }.
% 13.32/13.72 (29565) {G0,W4,D2,L2,V1,M2} { ! ca_Cx2( X ), alpha4( X ) }.
% 13.32/13.72 (29566) {G0,W6,D2,L3,V1,M3} { ! cp5xcomp( X ), ! alpha4( X ), ca_Cx2( X )
% 13.32/13.72 }.
% 13.32/13.72 (29567) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), cp3xcomp( X ) }.
% 13.32/13.72 (29568) {G0,W4,D2,L2,V1,M2} { ! alpha4( X ), cp4xcomp( X ) }.
% 13.32/13.72 (29569) {G0,W6,D2,L3,V1,M3} { ! cp3xcomp( X ), ! cp4xcomp( X ), alpha4( X
% 13.32/13.72 ) }.
% 13.32/13.72 (29570) {G0,W5,D2,L2,V2,M2} { ! ca_Cx2( X ), ! ra_Px2( X, Y ) }.
% 13.32/13.72 (29571) {G0,W6,D3,L2,V1,M2} { ra_Px2( X, skol14( X ) ), ca_Cx2( X ) }.
% 13.32/13.72 (29572) {G0,W6,D3,L2,V1,M2} { ! ca_Cx2xcomp( X ), ra_Px2( X, skol15( X ) )
% 13.32/13.72 }.
% 13.32/13.72 (29573) {G0,W5,D2,L2,V2,M2} { ! ra_Px2( X, Y ), ca_Cx2xcomp( X ) }.
% 13.32/13.72 (29574) {G0,W5,D2,L2,V2,M2} { ! ca_Cx3( X ), ! ra_Px3( X, Y ) }.
% 13.32/13.72 (29575) {G0,W6,D3,L2,V1,M2} { ra_Px3( X, skol16( X ) ), ca_Cx3( X ) }.
% 13.32/13.72 (29576) {G0,W4,D2,L2,V1,M2} { ! ca_Cx3( X ), cp5xcomp( X ) }.
% 13.32/13.72 (29577) {G0,W4,D2,L2,V1,M2} { ! ca_Cx3( X ), cp4xcomp( X ) }.
% 13.32/13.72 (29578) {G0,W6,D2,L3,V1,M3} { ! cp5xcomp( X ), ! cp4xcomp( X ), ca_Cx3( X
% 13.32/13.72 ) }.
% 13.32/13.72 (29579) {G0,W6,D3,L2,V1,M2} { ! ca_Cx3xcomp( X ), ra_Px3( X, skol17( X ) )
% 13.32/13.72 }.
% 13.32/13.72 (29580) {G0,W5,D2,L2,V2,M2} { ! ra_Px3( X, Y ), ca_Cx3xcomp( X ) }.
% 13.32/13.72 (29581) {G0,W6,D2,L2,V2,M2} { ! rinvR( X, Y ), rr( Y, X ) }.
% 13.32/13.72 (29582) {G0,W6,D2,L2,V2,M2} { ! rr( Y, X ), rinvR( X, Y ) }.
% 13.32/13.72 (29583) {G0,W2,D2,L1,V0,M1} { cUnsatisfiable( i2003_11_14_17_21_04740 )
% 13.32/13.72 }.
% 13.32/13.72
% 13.32/13.72
% 13.32/13.72 Total Proof:
% 13.32/13.72
% 13.32/13.72 subsumption: (3) {G0,W7,D2,L3,V2,M3} I { ! Y = X, ! ca_Cx1xcomp( Y ),
% 13.32/13.72 ca_Cx1xcomp( X ) }.
% 13.32/13.72 parent0: (29473) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! ca_Cx1xcomp( Y ),
% 13.32/13.72 ca_Cx1xcomp( X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := Y
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 2 ==> 2
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (43) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha1( X
% 13.32/13.72 ) }.
% 13.32/13.72 parent0: (29513) {G0,W4,D2,L2,V1,M2} { ! cUnsatisfiable( X ), alpha1( X )
% 13.32/13.72 }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (44) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), cp2( X )
% 13.32/13.72 }.
% 13.32/13.72 parent0: (29514) {G0,W4,D2,L2,V1,M2} { ! cUnsatisfiable( X ), cp2( X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (46) {G0,W5,D3,L2,V2,M2} I { ! alpha1( X ), ca_Ax14( skol1( Y
% 13.32/13.72 ) ) }.
% 13.32/13.72 parent0: (29516) {G0,W5,D3,L2,V2,M2} { ! alpha1( X ), ca_Ax14( skol1( Y )
% 13.32/13.72 ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := Y
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (47) {G0,W6,D3,L2,V1,M2} I { ! alpha1( X ), rinvR( X, skol1( X
% 13.32/13.72 ) ) }.
% 13.32/13.72 parent0: (29517) {G0,W6,D3,L2,V1,M2} { ! alpha1( X ), rinvR( X, skol1( X )
% 13.32/13.72 ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (49) {G0,W4,D2,L2,V1,M2} I { ! cp1( X ), ca_Cx1( X ) }.
% 13.32/13.72 parent0: (29519) {G0,W4,D2,L2,V1,M2} { ! cp1( X ), ca_Cx1( X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (50) {G0,W6,D3,L2,V1,M2} I { ! cp2( X ), ra_Px5( X, skol2( X )
% 13.32/13.72 ) }.
% 13.32/13.72 parent0: (29520) {G0,W6,D3,L2,V1,M2} { ! cp2( X ), ra_Px5( X, skol2( X ) )
% 13.32/13.72 }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (53) {G0,W5,D2,L2,V2,M2} I { ! cp2xcomp( X ), ! ra_Px5( X, Y )
% 13.32/13.72 }.
% 13.32/13.72 parent0: (29523) {G0,W5,D2,L2,V2,M2} { ! cp2xcomp( X ), ! ra_Px5( X, Y )
% 13.32/13.72 }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := Y
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (69) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax14( X ), alpha2( X ) }.
% 13.32/13.72 parent0: (29539) {G0,W4,D2,L2,V1,M2} { ! ca_Ax14( X ), alpha2( X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (70) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax14( X ), alpha5( X ) }.
% 13.32/13.72 parent0: (29540) {G0,W4,D2,L2,V1,M2} { ! ca_Ax14( X ), alpha5( X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (72) {G0,W9,D2,L3,V3,M3} I { ! alpha5( X ), ! alpha7( X, Y, Z
% 13.32/13.72 ), Y = Z }.
% 13.32/13.72 parent0: (29542) {G0,W9,D2,L3,V3,M3} { ! alpha5( X ), ! alpha7( X, Y, Z )
% 13.32/13.72 , Y = Z }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := Y
% 13.32/13.72 Z := Z
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 2 ==> 2
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (77) {G0,W10,D2,L3,V3,M3} I { ! rr( X, Y ), ! rr( X, Z ),
% 13.32/13.72 alpha7( X, Y, Z ) }.
% 13.32/13.72 parent0: (29547) {G0,W10,D2,L3,V3,M3} { ! rr( X, Y ), ! rr( X, Z ), alpha7
% 13.32/13.72 ( X, Y, Z ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := Y
% 13.32/13.72 Z := Z
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 2 ==> 2
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (78) {G0,W5,D3,L2,V2,M2} I { ! alpha2( X ), cp1( skol11( Y ) )
% 13.32/13.72 }.
% 13.32/13.72 parent0: (29548) {G0,W5,D3,L2,V2,M2} { ! alpha2( X ), cp1( skol11( Y ) )
% 13.32/13.72 }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := Y
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (79) {G0,W6,D3,L2,V1,M2} I { ! alpha2( X ), rr( X, skol11( X )
% 13.32/13.72 ) }.
% 13.32/13.72 parent0: (29549) {G0,W6,D3,L2,V1,M2} { ! alpha2( X ), rr( X, skol11( X ) )
% 13.32/13.72 }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (81) {G0,W4,D2,L2,V1,M2} I { ! ca_Cx1( X ), cp2xcomp( X ) }.
% 13.32/13.72 parent0: (29551) {G0,W4,D2,L2,V1,M2} { ! ca_Cx1( X ), cp2xcomp( X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (90) {G0,W6,D3,L2,V1,M2} I { ! ca_Cx1( X ), ra_Px1( X, skol12
% 13.32/13.72 ( X ) ) }.
% 13.32/13.72 parent0: (29560) {G0,W6,D3,L2,V1,M2} { ! ca_Cx1( X ), ra_Px1( X, skol12( X
% 13.32/13.72 ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (91) {G0,W5,D2,L2,V2,M2} I { ! ra_Px1( X, Y ), ca_Cx1( X ) }.
% 13.32/13.72 parent0: (29561) {G0,W5,D2,L2,V2,M2} { ! ra_Px1( X, Y ), ca_Cx1( X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := Y
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (92) {G0,W5,D2,L2,V2,M2} I { ! ca_Cx1xcomp( X ), ! ra_Px1( X,
% 13.32/13.72 Y ) }.
% 13.32/13.72 parent0: (29562) {G0,W5,D2,L2,V2,M2} { ! ca_Cx1xcomp( X ), ! ra_Px1( X, Y
% 13.32/13.72 ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := Y
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (93) {G0,W6,D3,L2,V1,M2} I { ra_Px1( X, skol13( X ) ),
% 13.32/13.72 ca_Cx1xcomp( X ) }.
% 13.32/13.72 parent0: (29563) {G0,W6,D3,L2,V1,M2} { ra_Px1( X, skol13( X ) ),
% 13.32/13.72 ca_Cx1xcomp( X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (111) {G0,W6,D2,L2,V2,M2} I { ! rinvR( X, Y ), rr( Y, X ) }.
% 13.32/13.72 parent0: (29581) {G0,W6,D2,L2,V2,M2} { ! rinvR( X, Y ), rr( Y, X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := Y
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (113) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable(
% 13.32/13.72 i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 parent0: (29583) {G0,W2,D2,L1,V0,M1} { cUnsatisfiable(
% 13.32/13.72 i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30399) {G1,W2,D2,L1,V0,M1} { cp2( i2003_11_14_17_21_04740 )
% 13.32/13.72 }.
% 13.32/13.72 parent0[0]: (44) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), cp2( X )
% 13.32/13.72 }.
% 13.32/13.72 parent1[0]: (113) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable(
% 13.32/13.72 i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := i2003_11_14_17_21_04740
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (167) {G1,W2,D2,L1,V0,M1} R(44,113) { cp2(
% 13.32/13.72 i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 parent0: (30399) {G1,W2,D2,L1,V0,M1} { cp2( i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30400) {G1,W2,D2,L1,V0,M1} { alpha1( i2003_11_14_17_21_04740
% 13.32/13.72 ) }.
% 13.32/13.72 parent0[0]: (43) {G0,W4,D2,L2,V1,M2} I { ! cUnsatisfiable( X ), alpha1( X )
% 13.32/13.72 }.
% 13.32/13.72 parent1[0]: (113) {G0,W2,D2,L1,V0,M1} I { cUnsatisfiable(
% 13.32/13.72 i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := i2003_11_14_17_21_04740
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (194) {G1,W2,D2,L1,V0,M1} R(43,113) { alpha1(
% 13.32/13.72 i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 parent0: (30400) {G1,W2,D2,L1,V0,M1} { alpha1( i2003_11_14_17_21_04740 )
% 13.32/13.72 }.
% 13.32/13.72 substitution0:
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30401) {G1,W5,D2,L2,V2,M2} { ! ra_Px5( X, Y ), ! ca_Cx1( X )
% 13.32/13.72 }.
% 13.32/13.72 parent0[0]: (53) {G0,W5,D2,L2,V2,M2} I { ! cp2xcomp( X ), ! ra_Px5( X, Y )
% 13.32/13.72 }.
% 13.32/13.72 parent1[1]: (81) {G0,W4,D2,L2,V1,M2} I { ! ca_Cx1( X ), cp2xcomp( X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := Y
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (276) {G1,W5,D2,L2,V2,M2} R(53,81) { ! ra_Px5( X, Y ), !
% 13.32/13.72 ca_Cx1( X ) }.
% 13.32/13.72 parent0: (30401) {G1,W5,D2,L2,V2,M2} { ! ra_Px5( X, Y ), ! ca_Cx1( X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := Y
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30402) {G1,W5,D3,L2,V2,M2} { ca_Cx1( skol11( X ) ), ! alpha2
% 13.32/13.72 ( Y ) }.
% 13.32/13.72 parent0[0]: (49) {G0,W4,D2,L2,V1,M2} I { ! cp1( X ), ca_Cx1( X ) }.
% 13.32/13.72 parent1[1]: (78) {G0,W5,D3,L2,V2,M2} I { ! alpha2( X ), cp1( skol11( Y ) )
% 13.32/13.72 }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := skol11( X )
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := Y
% 13.32/13.72 Y := X
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (317) {G1,W5,D3,L2,V2,M2} R(78,49) { ! alpha2( X ), ca_Cx1(
% 13.32/13.72 skol11( Y ) ) }.
% 13.32/13.72 parent0: (30402) {G1,W5,D3,L2,V2,M2} { ca_Cx1( skol11( X ) ), ! alpha2( Y
% 13.32/13.72 ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := Y
% 13.32/13.72 Y := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 1
% 13.32/13.72 1 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30403) {G1,W5,D3,L2,V2,M2} { ca_Cx1( skol11( Y ) ), ! ca_Ax14
% 13.32/13.72 ( X ) }.
% 13.32/13.72 parent0[0]: (317) {G1,W5,D3,L2,V2,M2} R(78,49) { ! alpha2( X ), ca_Cx1(
% 13.32/13.72 skol11( Y ) ) }.
% 13.32/13.72 parent1[1]: (69) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax14( X ), alpha2( X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := Y
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (347) {G2,W5,D3,L2,V2,M2} R(317,69) { ca_Cx1( skol11( X ) ), !
% 13.32/13.72 ca_Ax14( Y ) }.
% 13.32/13.72 parent0: (30403) {G1,W5,D3,L2,V2,M2} { ca_Cx1( skol11( Y ) ), ! ca_Ax14( X
% 13.32/13.72 ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := Y
% 13.32/13.72 Y := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30404) {G1,W3,D3,L1,V1,M1} { ca_Ax14( skol1( X ) ) }.
% 13.32/13.72 parent0[0]: (46) {G0,W5,D3,L2,V2,M2} I { ! alpha1( X ), ca_Ax14( skol1( Y )
% 13.32/13.72 ) }.
% 13.32/13.72 parent1[0]: (194) {G1,W2,D2,L1,V0,M1} R(43,113) { alpha1(
% 13.32/13.72 i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := i2003_11_14_17_21_04740
% 13.32/13.72 Y := X
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (360) {G2,W3,D3,L1,V1,M1} R(46,194) { ca_Ax14( skol1( X ) )
% 13.32/13.72 }.
% 13.32/13.72 parent0: (30404) {G1,W3,D3,L1,V1,M1} { ca_Ax14( skol1( X ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30405) {G3,W3,D3,L1,V1,M1} { ca_Cx1( skol11( X ) ) }.
% 13.32/13.72 parent0[1]: (347) {G2,W5,D3,L2,V2,M2} R(317,69) { ca_Cx1( skol11( X ) ), !
% 13.32/13.72 ca_Ax14( Y ) }.
% 13.32/13.72 parent1[0]: (360) {G2,W3,D3,L1,V1,M1} R(46,194) { ca_Ax14( skol1( X ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := skol1( Y )
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := Y
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (368) {G3,W3,D3,L1,V1,M1} R(360,347) { ca_Cx1( skol11( X ) )
% 13.32/13.72 }.
% 13.32/13.72 parent0: (30405) {G3,W3,D3,L1,V1,M1} { ca_Cx1( skol11( X ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30406) {G1,W3,D3,L1,V1,M1} { alpha2( skol1( X ) ) }.
% 13.32/13.72 parent0[0]: (69) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax14( X ), alpha2( X ) }.
% 13.32/13.72 parent1[0]: (360) {G2,W3,D3,L1,V1,M1} R(46,194) { ca_Ax14( skol1( X ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := skol1( X )
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (375) {G3,W3,D3,L1,V1,M1} R(360,69) { alpha2( skol1( X ) ) }.
% 13.32/13.72 parent0: (30406) {G1,W3,D3,L1,V1,M1} { alpha2( skol1( X ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30407) {G1,W3,D3,L1,V1,M1} { alpha5( skol1( X ) ) }.
% 13.32/13.72 parent0[0]: (70) {G0,W4,D2,L2,V1,M2} I { ! ca_Ax14( X ), alpha5( X ) }.
% 13.32/13.72 parent1[0]: (360) {G2,W3,D3,L1,V1,M1} R(46,194) { ca_Ax14( skol1( X ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := skol1( X )
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (376) {G3,W3,D3,L1,V1,M1} R(360,70) { alpha5( skol1( X ) ) }.
% 13.32/13.72 parent0: (30407) {G1,W3,D3,L1,V1,M1} { alpha5( skol1( X ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30408) {G1,W4,D3,L1,V0,M1} { rinvR( i2003_11_14_17_21_04740,
% 13.32/13.72 skol1( i2003_11_14_17_21_04740 ) ) }.
% 13.32/13.72 parent0[0]: (47) {G0,W6,D3,L2,V1,M2} I { ! alpha1( X ), rinvR( X, skol1( X
% 13.32/13.72 ) ) }.
% 13.32/13.72 parent1[0]: (194) {G1,W2,D2,L1,V0,M1} R(43,113) { alpha1(
% 13.32/13.72 i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := i2003_11_14_17_21_04740
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (458) {G2,W4,D3,L1,V0,M1} R(47,194) { rinvR(
% 13.32/13.72 i2003_11_14_17_21_04740, skol1( i2003_11_14_17_21_04740 ) ) }.
% 13.32/13.72 parent0: (30408) {G1,W4,D3,L1,V0,M1} { rinvR( i2003_11_14_17_21_04740,
% 13.32/13.72 skol1( i2003_11_14_17_21_04740 ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30409) {G1,W4,D3,L1,V0,M1} { rr( skol1(
% 13.32/13.72 i2003_11_14_17_21_04740 ), i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 parent0[0]: (111) {G0,W6,D2,L2,V2,M2} I { ! rinvR( X, Y ), rr( Y, X ) }.
% 13.32/13.72 parent1[0]: (458) {G2,W4,D3,L1,V0,M1} R(47,194) { rinvR(
% 13.32/13.72 i2003_11_14_17_21_04740, skol1( i2003_11_14_17_21_04740 ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := i2003_11_14_17_21_04740
% 13.32/13.72 Y := skol1( i2003_11_14_17_21_04740 )
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (465) {G3,W4,D3,L1,V0,M1} R(458,111) { rr( skol1(
% 13.32/13.72 i2003_11_14_17_21_04740 ), i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 parent0: (30409) {G1,W4,D3,L1,V0,M1} { rr( skol1( i2003_11_14_17_21_04740
% 13.32/13.72 ), i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30410) {G1,W4,D2,L2,V1,M2} { ! ca_Cx1( X ), ! cp2( X ) }.
% 13.32/13.72 parent0[0]: (276) {G1,W5,D2,L2,V2,M2} R(53,81) { ! ra_Px5( X, Y ), ! ca_Cx1
% 13.32/13.72 ( X ) }.
% 13.32/13.72 parent1[1]: (50) {G0,W6,D3,L2,V1,M2} I { ! cp2( X ), ra_Px5( X, skol2( X )
% 13.32/13.72 ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := skol2( X )
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (487) {G2,W4,D2,L2,V1,M2} R(50,276) { ! cp2( X ), ! ca_Cx1( X
% 13.32/13.72 ) }.
% 13.32/13.72 parent0: (30410) {G1,W4,D2,L2,V1,M2} { ! ca_Cx1( X ), ! cp2( X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 1
% 13.32/13.72 1 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30411) {G2,W2,D2,L1,V0,M1} { ! ca_Cx1(
% 13.32/13.72 i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 parent0[0]: (487) {G2,W4,D2,L2,V1,M2} R(50,276) { ! cp2( X ), ! ca_Cx1( X )
% 13.32/13.72 }.
% 13.32/13.72 parent1[0]: (167) {G1,W2,D2,L1,V0,M1} R(44,113) { cp2(
% 13.32/13.72 i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := i2003_11_14_17_21_04740
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (499) {G3,W2,D2,L1,V0,M1} R(487,167) { ! ca_Cx1(
% 13.32/13.72 i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 parent0: (30411) {G2,W2,D2,L1,V0,M1} { ! ca_Cx1( i2003_11_14_17_21_04740 )
% 13.32/13.72 }.
% 13.32/13.72 substitution0:
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30412) {G1,W3,D2,L1,V1,M1} { ! ra_Px1(
% 13.32/13.72 i2003_11_14_17_21_04740, X ) }.
% 13.32/13.72 parent0[0]: (499) {G3,W2,D2,L1,V0,M1} R(487,167) { ! ca_Cx1(
% 13.32/13.72 i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 parent1[1]: (91) {G0,W5,D2,L2,V2,M2} I { ! ra_Px1( X, Y ), ca_Cx1( X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := i2003_11_14_17_21_04740
% 13.32/13.72 Y := X
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (501) {G4,W3,D2,L1,V1,M1} R(499,91) { ! ra_Px1(
% 13.32/13.72 i2003_11_14_17_21_04740, X ) }.
% 13.32/13.72 parent0: (30412) {G1,W3,D2,L1,V1,M1} { ! ra_Px1( i2003_11_14_17_21_04740,
% 13.32/13.72 X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 eqswap: (30413) {G0,W9,D2,L3,V3,M3} { Y = X, ! alpha5( Z ), ! alpha7( Z, X
% 13.32/13.72 , Y ) }.
% 13.32/13.72 parent0[2]: (72) {G0,W9,D2,L3,V3,M3} I { ! alpha5( X ), ! alpha7( X, Y, Z )
% 13.32/13.72 , Y = Z }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := Z
% 13.32/13.72 Y := X
% 13.32/13.72 Z := Y
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30414) {G1,W11,D2,L4,V3,M4} { X = Y, ! alpha5( Z ), ! rr( Z,
% 13.32/13.72 Y ), ! rr( Z, X ) }.
% 13.32/13.72 parent0[2]: (30413) {G0,W9,D2,L3,V3,M3} { Y = X, ! alpha5( Z ), ! alpha7(
% 13.32/13.72 Z, X, Y ) }.
% 13.32/13.72 parent1[2]: (77) {G0,W10,D2,L3,V3,M3} I { ! rr( X, Y ), ! rr( X, Z ),
% 13.32/13.72 alpha7( X, Y, Z ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := Y
% 13.32/13.72 Y := X
% 13.32/13.72 Z := Z
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := Z
% 13.32/13.72 Y := Y
% 13.32/13.72 Z := X
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (899) {G1,W11,D2,L4,V3,M4} R(77,72) { ! rr( X, Y ), ! rr( X, Z
% 13.32/13.72 ), ! alpha5( X ), Y = Z }.
% 13.32/13.72 parent0: (30414) {G1,W11,D2,L4,V3,M4} { X = Y, ! alpha5( Z ), ! rr( Z, Y )
% 13.32/13.72 , ! rr( Z, X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := Y
% 13.32/13.72 Y := Z
% 13.32/13.72 Z := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 3
% 13.32/13.72 1 ==> 2
% 13.32/13.72 2 ==> 1
% 13.32/13.72 3 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30416) {G1,W6,D4,L1,V1,M1} { rr( skol1( X ), skol11( skol1( X
% 13.32/13.72 ) ) ) }.
% 13.32/13.72 parent0[0]: (79) {G0,W6,D3,L2,V1,M2} I { ! alpha2( X ), rr( X, skol11( X )
% 13.32/13.72 ) }.
% 13.32/13.72 parent1[0]: (375) {G3,W3,D3,L1,V1,M1} R(360,69) { alpha2( skol1( X ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := skol1( X )
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (922) {G4,W6,D4,L1,V1,M1} R(79,375) { rr( skol1( X ), skol11(
% 13.32/13.72 skol1( X ) ) ) }.
% 13.32/13.72 parent0: (30416) {G1,W6,D4,L1,V1,M1} { rr( skol1( X ), skol11( skol1( X )
% 13.32/13.72 ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30417) {G1,W4,D2,L2,V1,M2} { ! ca_Cx1xcomp( X ), ! ca_Cx1( X
% 13.32/13.72 ) }.
% 13.32/13.72 parent0[1]: (92) {G0,W5,D2,L2,V2,M2} I { ! ca_Cx1xcomp( X ), ! ra_Px1( X, Y
% 13.32/13.72 ) }.
% 13.32/13.72 parent1[1]: (90) {G0,W6,D3,L2,V1,M2} I { ! ca_Cx1( X ), ra_Px1( X, skol12(
% 13.32/13.72 X ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := skol12( X )
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (1046) {G1,W4,D2,L2,V1,M2} R(90,92) { ! ca_Cx1( X ), !
% 13.32/13.72 ca_Cx1xcomp( X ) }.
% 13.32/13.72 parent0: (30417) {G1,W4,D2,L2,V1,M2} { ! ca_Cx1xcomp( X ), ! ca_Cx1( X )
% 13.32/13.72 }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 1
% 13.32/13.72 1 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30418) {G2,W3,D3,L1,V1,M1} { ! ca_Cx1xcomp( skol11( X ) ) }.
% 13.32/13.72 parent0[0]: (1046) {G1,W4,D2,L2,V1,M2} R(90,92) { ! ca_Cx1( X ), !
% 13.32/13.72 ca_Cx1xcomp( X ) }.
% 13.32/13.72 parent1[0]: (368) {G3,W3,D3,L1,V1,M1} R(360,347) { ca_Cx1( skol11( X ) )
% 13.32/13.72 }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := skol11( X )
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (1052) {G4,W3,D3,L1,V1,M1} R(1046,368) { ! ca_Cx1xcomp( skol11
% 13.32/13.72 ( X ) ) }.
% 13.32/13.72 parent0: (30418) {G2,W3,D3,L1,V1,M1} { ! ca_Cx1xcomp( skol11( X ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 eqswap: (30419) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! ca_Cx1xcomp( X ),
% 13.32/13.72 ca_Cx1xcomp( Y ) }.
% 13.32/13.72 parent0[0]: (3) {G0,W7,D2,L3,V2,M3} I { ! Y = X, ! ca_Cx1xcomp( Y ),
% 13.32/13.72 ca_Cx1xcomp( X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := Y
% 13.32/13.72 Y := X
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30420) {G1,W6,D3,L2,V2,M2} { ! skol11( X ) = Y, ! ca_Cx1xcomp
% 13.32/13.72 ( Y ) }.
% 13.32/13.72 parent0[0]: (1052) {G4,W3,D3,L1,V1,M1} R(1046,368) { ! ca_Cx1xcomp( skol11
% 13.32/13.72 ( X ) ) }.
% 13.32/13.72 parent1[2]: (30419) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! ca_Cx1xcomp( X ),
% 13.32/13.72 ca_Cx1xcomp( Y ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := Y
% 13.32/13.72 Y := skol11( X )
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 eqswap: (30421) {G1,W6,D3,L2,V2,M2} { ! Y = skol11( X ), ! ca_Cx1xcomp( Y
% 13.32/13.72 ) }.
% 13.32/13.72 parent0[0]: (30420) {G1,W6,D3,L2,V2,M2} { ! skol11( X ) = Y, ! ca_Cx1xcomp
% 13.32/13.72 ( Y ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := Y
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (1055) {G5,W6,D3,L2,V2,M2} R(1052,3) { ! X = skol11( Y ), !
% 13.32/13.72 ca_Cx1xcomp( X ) }.
% 13.32/13.72 parent0: (30421) {G1,W6,D3,L2,V2,M2} { ! Y = skol11( X ), ! ca_Cx1xcomp( Y
% 13.32/13.72 ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := Y
% 13.32/13.72 Y := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 eqswap: (30422) {G5,W6,D3,L2,V2,M2} { ! skol11( Y ) = X, ! ca_Cx1xcomp( X
% 13.32/13.72 ) }.
% 13.32/13.72 parent0[0]: (1055) {G5,W6,D3,L2,V2,M2} R(1052,3) { ! X = skol11( Y ), !
% 13.32/13.72 ca_Cx1xcomp( X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := Y
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30423) {G1,W8,D3,L2,V2,M2} { ! skol11( X ) = Y, ra_Px1( Y,
% 13.32/13.72 skol13( Y ) ) }.
% 13.32/13.72 parent0[1]: (30422) {G5,W6,D3,L2,V2,M2} { ! skol11( Y ) = X, ! ca_Cx1xcomp
% 13.32/13.72 ( X ) }.
% 13.32/13.72 parent1[1]: (93) {G0,W6,D3,L2,V1,M2} I { ra_Px1( X, skol13( X ) ),
% 13.32/13.72 ca_Cx1xcomp( X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := Y
% 13.32/13.72 Y := X
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := Y
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 eqswap: (30424) {G1,W8,D3,L2,V2,M2} { ! Y = skol11( X ), ra_Px1( Y, skol13
% 13.32/13.72 ( Y ) ) }.
% 13.32/13.72 parent0[0]: (30423) {G1,W8,D3,L2,V2,M2} { ! skol11( X ) = Y, ra_Px1( Y,
% 13.32/13.72 skol13( Y ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := Y
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (2529) {G6,W8,D3,L2,V2,M2} R(1055,93) { ! X = skol11( Y ),
% 13.32/13.72 ra_Px1( X, skol13( X ) ) }.
% 13.32/13.72 parent0: (30424) {G1,W8,D3,L2,V2,M2} { ! Y = skol11( X ), ra_Px1( Y,
% 13.32/13.72 skol13( Y ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := Y
% 13.32/13.72 Y := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30425) {G2,W10,D3,L3,V1,M3} { ! rr( skol1(
% 13.32/13.72 i2003_11_14_17_21_04740 ), X ), ! alpha5( skol1( i2003_11_14_17_21_04740
% 13.32/13.72 ) ), i2003_11_14_17_21_04740 = X }.
% 13.32/13.72 parent0[0]: (899) {G1,W11,D2,L4,V3,M4} R(77,72) { ! rr( X, Y ), ! rr( X, Z
% 13.32/13.72 ), ! alpha5( X ), Y = Z }.
% 13.32/13.72 parent1[0]: (465) {G3,W4,D3,L1,V0,M1} R(458,111) { rr( skol1(
% 13.32/13.72 i2003_11_14_17_21_04740 ), i2003_11_14_17_21_04740 ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := skol1( i2003_11_14_17_21_04740 )
% 13.32/13.72 Y := i2003_11_14_17_21_04740
% 13.32/13.72 Z := X
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30427) {G3,W7,D3,L2,V1,M2} { ! rr( skol1(
% 13.32/13.72 i2003_11_14_17_21_04740 ), X ), i2003_11_14_17_21_04740 = X }.
% 13.32/13.72 parent0[1]: (30425) {G2,W10,D3,L3,V1,M3} { ! rr( skol1(
% 13.32/13.72 i2003_11_14_17_21_04740 ), X ), ! alpha5( skol1( i2003_11_14_17_21_04740
% 13.32/13.72 ) ), i2003_11_14_17_21_04740 = X }.
% 13.32/13.72 parent1[0]: (376) {G3,W3,D3,L1,V1,M1} R(360,70) { alpha5( skol1( X ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := i2003_11_14_17_21_04740
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (28430) {G4,W7,D3,L2,V1,M2} R(899,465);r(376) { ! rr( skol1(
% 13.32/13.72 i2003_11_14_17_21_04740 ), X ), i2003_11_14_17_21_04740 = X }.
% 13.32/13.72 parent0: (30427) {G3,W7,D3,L2,V1,M2} { ! rr( skol1(
% 13.32/13.72 i2003_11_14_17_21_04740 ), X ), i2003_11_14_17_21_04740 = X }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 1 ==> 1
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 eqswap: (30429) {G4,W7,D3,L2,V1,M2} { X = i2003_11_14_17_21_04740, ! rr(
% 13.32/13.72 skol1( i2003_11_14_17_21_04740 ), X ) }.
% 13.32/13.72 parent0[1]: (28430) {G4,W7,D3,L2,V1,M2} R(899,465);r(376) { ! rr( skol1(
% 13.32/13.72 i2003_11_14_17_21_04740 ), X ), i2003_11_14_17_21_04740 = X }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 eqswap: (30430) {G6,W8,D3,L2,V2,M2} { ! skol11( Y ) = X, ra_Px1( X, skol13
% 13.32/13.72 ( X ) ) }.
% 13.32/13.72 parent0[0]: (2529) {G6,W8,D3,L2,V2,M2} R(1055,93) { ! X = skol11( Y ),
% 13.32/13.72 ra_Px1( X, skol13( X ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 Y := Y
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30431) {G5,W9,D3,L2,V1,M2} { ra_Px1( i2003_11_14_17_21_04740
% 13.32/13.72 , skol13( i2003_11_14_17_21_04740 ) ), ! rr( skol1(
% 13.32/13.72 i2003_11_14_17_21_04740 ), skol11( X ) ) }.
% 13.32/13.72 parent0[0]: (30430) {G6,W8,D3,L2,V2,M2} { ! skol11( Y ) = X, ra_Px1( X,
% 13.32/13.72 skol13( X ) ) }.
% 13.32/13.72 parent1[0]: (30429) {G4,W7,D3,L2,V1,M2} { X = i2003_11_14_17_21_04740, !
% 13.32/13.72 rr( skol1( i2003_11_14_17_21_04740 ), X ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := i2003_11_14_17_21_04740
% 13.32/13.72 Y := X
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := skol11( X )
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30432) {G5,W5,D3,L1,V1,M1} { ! rr( skol1(
% 13.32/13.72 i2003_11_14_17_21_04740 ), skol11( X ) ) }.
% 13.32/13.72 parent0[0]: (501) {G4,W3,D2,L1,V1,M1} R(499,91) { ! ra_Px1(
% 13.32/13.72 i2003_11_14_17_21_04740, X ) }.
% 13.32/13.72 parent1[0]: (30431) {G5,W9,D3,L2,V1,M2} { ra_Px1( i2003_11_14_17_21_04740
% 13.32/13.72 , skol13( i2003_11_14_17_21_04740 ) ), ! rr( skol1(
% 13.32/13.72 i2003_11_14_17_21_04740 ), skol11( X ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := skol13( i2003_11_14_17_21_04740 )
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (28812) {G7,W5,D3,L1,V1,M1} R(28430,2529);r(501) { ! rr( skol1
% 13.32/13.72 ( i2003_11_14_17_21_04740 ), skol11( X ) ) }.
% 13.32/13.72 parent0: (30432) {G5,W5,D3,L1,V1,M1} { ! rr( skol1(
% 13.32/13.72 i2003_11_14_17_21_04740 ), skol11( X ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := X
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 0 ==> 0
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 resolution: (30433) {G5,W0,D0,L0,V0,M0} { }.
% 13.32/13.72 parent0[0]: (28812) {G7,W5,D3,L1,V1,M1} R(28430,2529);r(501) { ! rr( skol1
% 13.32/13.72 ( i2003_11_14_17_21_04740 ), skol11( X ) ) }.
% 13.32/13.72 parent1[0]: (922) {G4,W6,D4,L1,V1,M1} R(79,375) { rr( skol1( X ), skol11(
% 13.32/13.72 skol1( X ) ) ) }.
% 13.32/13.72 substitution0:
% 13.32/13.72 X := skol1( i2003_11_14_17_21_04740 )
% 13.32/13.72 end
% 13.32/13.72 substitution1:
% 13.32/13.72 X := i2003_11_14_17_21_04740
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 subsumption: (29468) {G8,W0,D0,L0,V0,M0} R(28812,922) { }.
% 13.32/13.72 parent0: (30433) {G5,W0,D0,L0,V0,M0} { }.
% 13.32/13.72 substitution0:
% 13.32/13.72 end
% 13.32/13.72 permutation0:
% 13.32/13.72 end
% 13.32/13.72
% 13.32/13.72 Proof check complete!
% 13.32/13.72
% 13.32/13.72 Memory use:
% 13.32/13.72
% 13.32/13.72 space for terms: 445804
% 13.32/13.72 space for clauses: 1041810
% 13.32/13.72
% 13.32/13.72
% 13.32/13.72 clauses generated: 202691
% 13.32/13.72 clauses kept: 29469
% 13.32/13.72 clauses selected: 2026
% 13.32/13.72 clauses deleted: 560
% 13.32/13.72 clauses inuse deleted: 18
% 13.32/13.72
% 13.32/13.72 subsentry: 949748
% 13.32/13.72 literals s-matched: 618249
% 13.32/13.72 literals matched: 591363
% 13.32/13.72 full subsumption: 350810
% 13.32/13.72
% 13.32/13.72 checksum: -1317995524
% 13.32/13.72
% 13.32/13.72
% 13.32/13.72 Bliksem ended
%------------------------------------------------------------------------------